How do I use resolution to prove a formula

Question

$F_1 = ∀x∃y \, R(x,y)$

$F_2 = ∀x \, (∀y \, R(x,y) \to ∃z \, S(x,z))$

$F_3 = ∀x∀y∀z \, (R(x,y) \to (S(x,z) \to S(y,z)))$

$G = ∀x∃y \, S(x,y)$

Using resolution show that $F_1,F_2,F_3 \models G$.

So far I have done the following

a)Prenex form of the formula

b)Skolem form of the formula

1= Prenex $∃x∀y \, R(x,y)$

1= Skolem $∀y \, R(f(y),y)$

2= Prenex $∀x∃y∃z \, (¬R(x,y) \lor S(x,z))$

2= Skolem $∀x \, (¬R(x,f(x)) \lor S(x,g(x)))$

3= Prenex $∀x∀y∀z \, (¬R(x,y) \lor (¬S(x,z) \lor S(y,z)))$

3= Skolem $∀x∀y∀z \, (¬R(x,y) \lor (¬S(x,z) \lor S(y,z)))$

Now how do I go about going on to show that $F_1,F_2,F_3 \models G$ using resolution?

Answer 1

$F_1, F_2, F_3 \models G$ is equivalent to the fact that the set $\{F_1, F_2, F_3,\lnot G\}$ is contradictory.

To prove that $\{F_1, F_2, F_3,\lnot G\}$ is contradictory using the resolution method, you have to put $F_1, F_2, F_3, \lnot G$ in a prenex, Skolem form without quantifiers. Hence:

\begin{align*} F_1' &= R(f(y),y) \\ F_2' &= ¬R(x,f(x)) \lor S(x,g(x)) \\ F_3' &= ¬R(x',y') \lor ¬S(x',z') \lor S(y',z') \\ ¬G' &= ¬S(a,z) \end{align*}

Now we apply the resolution method to find a contradiction:

(the label on the right of every inference rule is the most general unifier).