Inverted First-Order Example

Target concept = GrandChild(x,y)
D = GrandChild(Bob, Shanon)
B = {Father(Shanon,Tom), Father(Tom,Bob)}.
C = GrandChild(Bob,Shanon)
C1 = Father(Shanon, Tom)
L1 = Father(Shanon, Tom)
θ1^-1 = {}
θ2^-1 = {Shanon/x}
Then, the resulting C2 is
GrandChild(Bob,x) ∨ ¬Father(x,Tom)
This inferred clause may now be used as the conclusion C for a second inverse resolution.