# Understanding SLDNF-forest

I am trying to understand this program and the respective forest. This is from the book Logic,Programming and Prolog by Ulf Nilsson.

Question:

• In the main tree, why from ←off_gound(a) can you derive ⧠ ?

• In the main tree, why was chosed on(b,a) first instead of on(c,b)?

So from ←$$\neg$$off_ground(a) we derive ⧠ by trying to derive ←off_ground(a) and failing (i.e. deriving FF). This is done in the upper tree on the right hand side.