"Paramodulation always focuses on two clauses, requiring that one of the clauses contain at least one literal asserting the equality of two expressions. For an application of paramodulation to succeed, there must exist a unifier (substitution of terms for variables) that, when used, makes identical one argument of a chosen positive equality literal in one clause and one chosen term in the other clause. If r is the chosen argument, s the other argument of the positive equality literal, t the chosen term, and U the unifier, the conclusion is obtained by applying U to both clauses, then replacing U(t) with U(s), and finally, except for the positive equality literal, taking the union of the transformed remaining literals. (With the exception of reflexivity, x = x, the nature of paramodulation permits the omission of the usual axioms for equality.) Because of the potential fecundity of using paramodulation (from being term-oriented rather than literal-oriented), various restriction strategies are recommended. They include restricting the choice of argument (in the positive equality literal) to just the lefthand argument, to just the righthand argument, and to arguments that are not merely a variable. Also recommended is restricting the chosen term to one that is not merely a variable. " Suppose we have as axioms the following clauses: <pre> (or (not (author Moby-Dick ?x)) (= Melville ?x)) (American Melville) </pre> Paramodulation allows us to conclude: <pre> (or (not (author Moby-Dick ?x)) (American ?x)) </pre>