# Show by Resolution that a set of clauses is unsatisfiable

Im trying to show by resolution that the following set of clauses is unsatisfiable:

$$\{ p(x,f(y)) \lor p(c,z), ¬p(y,f(f(y))) \lor ¬p(c,x) \}$$.

Now, I know that to show the unsatisfiability I need to derive an empty clause from the original clause set. So far Ive only done exercises with at least one clause having just one literal. This time I dont understand how I can end up with empty clause when theres always two literals.

Step 1) : use the substitution $$z \leftarrow x$$ with $$¬p(c,x)$$ to get $$¬p(c,z)$$ and resolve with: $$p(x,f(y)) \lor p(c,z)$$ to get
$$p(x,f(y))$$.
Now you have to clauses : $$p(x,f(y))$$ and $$¬p(y,f(f(y)))$$.
Find a suitable substitution to unify them and you wll get the empty clause : $$\square$$.