Showing that a knowledge base leads to empty clause

Question

Using the resolution method, I want show that the following knowledge leads to the empty clause.

1. $∃x (q(f(x))∧s(f(x),A))$
2. $∀x∀y¬∃z (p(x, y)∧s(x,z))$
3. $∀x (q(x)∧ ∃y s(x, y)) ⇒ (∃z (r(z)∧ p(x,z)))$

What I did so far :

4. $¬(q(x)∧ ∃y s(x, y)) ∨ (∃z (r(z)∧ p(x,z)))$ from 3 as $∀x, A⇒B = ¬A ∨ B$

Then I'm stuck ...

Answer 1

See Resolution method :

1) produce clauses, using Skolemization if needed.

E.g. $q(f(B))$ and $s(f(B),A))$ from 1. and $¬p(x, y) \lor ¬s(x,z)$ from 2.

Note : from 3. (presumably : it depends on the scope of the leading quantifier) we get : $∀x[¬(q(x)∧∃ys(x,y)) \lor ∃z(r(z)∧p(x,z))]$.

Thus, using the rules for Prnex Normal Form we have :

$∀x∃z∀y[¬q(x) \lor ¬s(x,y) \lor (r(z)∧p(x,z))]$

that means : $¬q(x) \lor ¬s(x,y) \lor (r(g(x))∧p(x,g(x)))$, i.e. two new clauses.

2) Find two clauses containing the same predicate, where it is negated in one clause but not in the other and perform unification on the two predicates.

E.g. use the subst $\{ x \leftarrow f(B), z \leftarrow A \}$ to unify $s(f(B),A))$ with $¬p(x, y) \lor ¬s(x,z)$.

3) apply the Resolution rule, discarding the unified predicates, and combine the remaining ones from the two clauses into a new clause.

Applying resolution to the two clauses above (after unification) we get the new caluse : $\lnot p(f(B),y)$.