ATP System Implementation

• A shell Script
  • Translation implemented in Prolog
  • Proof by a FOL theorem prover
  • Countermodel by a FOL finite model finder

• Parameters
  • Which translation
  • CPU time limit
  • List of FOL theorem provers (currently Vampire 4.1)
  • List of FOL model finders (currently Paradox 3.0)
  • Percentage of time for each FOL system (currently 80% and 20%)