• Check consistency of axioms
  • Techniques for rich theories
    • Incremental lemma addition (ala Quaife, and SET*-6.p)
    • Incremental lemma replacement (ala my HOM stuff)
  • Full FOF argument 
    FOF axioms .......
 |  |   |  |   | |
CNF axioms .......
  \  |  |  |  | /
     Refutation
        tree
         \ /
     CNF theorem
          |
     FOF theorem
  • HOM push and paper