Explaining the Example

Give a proof, using the domain theory, that the (positive) training satisfies the target concept.
In our ongoing example the positive example of SafeToStack(o1,o2) can be explained by using the domain theory, as such:
1. Volume(o1,2) ∧ Density(o1,0.3) ∧ Equal(0.6, 2*0.3) → Weight(o1,0.6)
2. Type(o2,endtable) → Weight(o2,5)
3. Weight(o1, 0.6) ∧ LessThan(0.6, 5) ∧ Weight(o2,5) → Lighter(o1,o2)
4. Lighter(o1, o2) → SafeToStack(o1,o2)
In Prolog-EGB this explanation is generated using backward chaining search, as done by Prolog.
Like Prolog, it halts when it finds a proof.