"Factoring always focuses on one clause at a time and on two literals in that clause. An application of factoring yields a conclusion if and only if the two literals in focus are alike in sign and if there exists a unifier (substitution of terms for variables) whose use makes the two literals identical. The conclusion is obtained by applying the unifier to the clause and merging the identical literals. In Otter, factoring is implemented in two ways: as an inference rule as described in the preceding paragraph, and as a simplification rule, which applies when the conclusion is logically equivalent to the original clause."