Suppose that we have formulas such as the following:

* A *

* B *

* D *

* ¬ A &or ¬ B &or C * (same as * A &and B &rarr C *)

* ¬ C &or ¬ D &or E * (same as * C &and D &rarr E *)

A desired conclusion, say * E *, is negated to form the hypothetical fact
* ¬ E * ; then the following algorithm is executed:

- Choose two clauses that have
*exactly one*pair of literals that are complementary (have different signs). - Produce a new clause by deleting the complementary literals
and combining the remaining literals.
- If the resulting clause is empty (``box''), stop; the theorem is proved by contradiction. (If the negation of the theorem leads to a contradiction, then the theorem must be true.)