Evaluation Setup

The MPTP Challenge

• Two sets of 252 problems from the Mizar
• "Bushy" problems have MPTP selected axioms - still many unnecessary
• "Chainy" problems have all preceding Mizar knowledge - very many unnecessary
• See tptp.org/Challenges/MPTPChallenge/

Configuration

• E and Fampire to find proofs (why?)
  Paradox to establish countersatifiability
• 300s CPU limit, initial 60s attempt with all axioms
• Dividing down to eigths
• 2.8GHz Intel Xeon, 1GB memory, Linux