 Resolution proofs, more precisely refutations, are constructed by deriving the empty clause [ ] from Γ ∪ {~α} using resolution; this will always be possible if Γ ∪ {~α} is unsatisfiable since resolution is refutation complete (Robinson 1965a). As an example of a resolution proof, we show that the set {∀x(P(x) ∨ Q(x)), ∀x(P(x) ⊃ R(x)),∀x(Q(x) ⊃ R(x))}, denoted by Γ, entails the formula ∃xR(x). The first step is to find the clausal form of Γ ∪ {~∃xR(x)}; the resulting clause set, denoted by S0, is shown in steps 1 to 4 in the refutation below. The refutation is constructed by using a level-saturation method: Compute all the resolvents of the initial set, S0, add them to the set and repeat the process until the empty clause is derived. (This produces the sequence of increasingly larger sets: S0, S1, S2,…) The only constraint that we impose is that we do not resolve the same two clauses more than once.