Efficient and Greedy Termination

Efficient Termination

• Solved if selected axioms and negated conjecture have no model
• Use different tools to test for unsatisfiability

Greedy Termination

• Select a counter theorem of the selected axioms and negated conjecture
• Reminiscent of unit conflict strategy
• Succeeds only for last axiom - expensive!