# Predicate resolution, some questions.

we have to clauses: $$\{\neg A(y_1, z_1), A(x_1, z_1) \} \\ \{\neg A(x_2, z_2), A(y_2, z_2)\}$$

1. can I resolve it to an empty clause? Exactly, I would like to know whether I can make a resolvent removing two negated literals from every set.

2. Is set of clauses $\{A(z_1, z_2), A(z_3, z_4)\}$ equivalent to $\{A(z_1, z_2)\}$ in the sense of resolution proof?