Exceptional Cases

Inconsistent Axioms

• No model of the selected axioms
• Last selected may or may not be consistent with the conjecture

Redundant Axioms

• Check true unselected axioms for redundancy
• Check previously selected axioms for redundancy
• Axioms can be superfluous but not redundant

CounterSatisfiable Conjecture

• All unselected axioms true in the model