Understanding SLDNF-forest
To answer your first question: SLDNF resolution employs negation as failure to deal with negation.

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.