The general form of Resolution with variables presented here is not complete as it stands, even for deriving the empty clause. In particular, note that the two clauses [P(x), P( y)] and [¬P(u), ¬P(v)] are together unsatisfiable. (a) Argue that the empty clause cannot be derived from these two clauses. A slightly more general rule of Resolution handles cases such as these: Suppose that C1 and C2 are clauses with disjoint atoms. Suppose that there are sets of literals D1 ⊆ C1 and D2 ⊆ C2 and a substitution θ such that D1θ = {ρ} and D2θ = {ρ}. Then, we conclude by Resolution the clause (C1 − D1)θ ∪ (C2 − D2)θ. The form of Resolution considered in the text simply took D1 and D2 to be singleton sets. (b) Show a refutation of the two clauses with this generalized form of Resolution. (c) Another way to obtain completeness is to leave the Resolution rule unchanged (that is, dealing with pairs of literals rather than pairs of sets of literals), but to add a second rule of inference, sometimes called factoring, to make up the difference. Present such a rule of inference and show that it properly handles the earlier example. In the remaining exercises of this chapter we consider a number of procedures for determining whether or not a set of propositional clauses is satisfiable. In most cases, we also would like to return a satisfying interpretation, if one exists.