Resolution in First Order Logic

Question

i have problem with resolution in first order logic

i have :

C1  :
¬ Loves(x,F(x) ) or Loves ( G(x) , x )

and

C2 : 

¬ Animal ( X) or Loves ( jack , x ) 

can some one help me why the answer ( after Resolve C1,C2 ) is :

¬ Animal(F(jack) ) or Loves ( G(jack) , jack )

because my answer is :

x/ jack

then i will have :

C1 : 
¬ Loves ( jack , F(jack ) ) or Loves ( G(jack),jack ) 

C2 : 

¬ Animal ( jack ) or Loves ( jack,jack ) 

and i cant use resolution with Loves (jack,jack) and ¬ Loves (jack,F(jack))

thank you all !!

Answer 1

If you want to resolve C1 with C2, then the only option is for Loves(jack, x) (in C2) to match ¬Loves(x, F(x)) (in C1), and so as you state, you should substitute x=jack in C1 and x=F(jack) in C2. Upon making these substitutions, C1 and C2 become:

C1[x/jack] = ¬Loves(jack, F(jack)) or Loves(G(jack), jack)

C2[x/F(jack)] = ¬Animal(F(jack)) or Loves(jack, F(jack))

Resolving the two, we get:

¬Animal(F(jack)) or Loves(G(jack), jack)