Conclusion

Analysis

• N axioms means 2^N-1 axioms reduced problems
• But recall the O(N ^2SearchDepth) search space
• May not remove all unnecessary axioms
  • Results table ...
  • "a few rotten eggs spoil the basket"
• Improved local search

Stengths and Weaknesses

• Different approach to ATP ... work smarter, not harder
• Aims to find proofs of hard theorems, not proofs of more easy theorems
• Selection of axioms to remove is quite stupid