²The Post rule for resolution as stated requires that a predicate R be present on the left-hand side of one clause and on the right-hand side of the other. In reality, these occurrences need not be identical; they only need to “match” in the sense of being unifiable according to Robinson’s unification algorithm. The MGU of the two occurrences is then applied throughout the clause in the conclusion of the rule. As we will cover unification in detail in later sections, we will omit discussion of it here in the name of brevity.