Prover9 Manual |  | Version 2009-02A

# The Inference Loop

The main loop for inferring and processing clauses and searching for a proof is sometimes called the given clause algorithm. It operates mainly on the `sos` and `usable` lists.

    While the sos list is not empty:
        1. Select a given clause from sos and move it to the usable list;
        2. Infer new clauses using the inference rules in effect;
           each new clause must have the given clause as one of its
           parents and members of the usable list as its other parents;
        3. process each new clause;
        4. append new clauses that pass the retention tests to the sos list.
    end of while loop.

## Two Frequently Asked Questions

> At some point in the search, Prover9 has all of the clauses needed to make an important inference, and one of the potential parents is selected as the given clause. But Prover9 fails to make the inference. Why is that?

> Why do all parents have to be in the `usable` list?

The answer to both questions is the same, and it has to do with redundancy. Assume

- clause C can be inferred from clauses A and B;
- both A and B are in the `sos` list; and
- A is selected first.

According to the algorithm, C is not derived until B has also been selected. Otherwise, C would be derived twice from A and B.

## Variations of the Loop

There are two common versions of the given clause algorithm that differ in how and when simplification (i.e., rewriting) occurs.

In the Otter loop, which Prover9 uses, clauses in the `sos` list can simplify new clauses, and new simplifiers are applied immediately to all clauses, including `sos` clauses.

In the Discount loop, clauses in the `sos` list (also called the passive list) cannot simplify or be simplified until they are selected as given clauses.

The tradeoff between the two versions is straightforward --- the Otter loop spends much more time simplifying with the possible benefit of making an important simplification sooner.

Next Section: Select Given