- Approaches to proving hard theorems
- There are often unnecessary axioms in problems in rich theories

- Repeatedly
- Remove some axioms to form an
*axiom reduced*problem - Submit the result to ATP

- Remove some axioms to form an
- Brute force and ignorance - Combinatorial removal

- Results from TPTP FOF problems,
3600s limit, 60s per axiom reduced problem
60 SPASS unsolved problems 73 problems rated 1.00 SPASS 2.0 RedAx Vampire 5.0 RedAx Solved 7 14 0 4