Binary Resolution "Binary resolution always focuses on two clauses and one literal in each. To admit a conclusion, the literals must be opposite in sign and alike in predicate, and there must exist a unifier (substitution of terms for variables) to otherwise make them identical. If a conclusion results, it is obtained by applying the unifier to the two clauses excluding the two literals in focus, and taking the union of the transformed literals." Suppose we have as axioms the following clauses: <pre> (or (mortal ?x) (not (human ?x))) (human Socrates) </pre> By substituting "Socrates" for "?x", the second literal of the first clause is made identical with the negation of the sole literal of the second clause. The opposed literals are resolved, leaving as a conclusion the resolvent <pre> (mortal Socrates) </pre> '(or ' A ')'; '(or' B ')' |- '(or ' A + B - A.i - B.j ')';; (Lit A B) ; (= {A.i} {'(not ' B.j ')'})