MPTP Challenge Results

The MPTP Challenge

• Generalization of the Bolzano-Weierstrass theorem, from Mizar
• 252 bushy problems, 252 chainy problems
• Chainy problems have lemmas, thus many more superfluous axioms

System Configuration

• Initial Proof attempts in 30s
• Batch Selection of 3 axioms per iteration
• Limited Selection of 10 axioms per method
• No Final Proof attempt to construct proof
• Overall CPU limit 300s

Results

• In the bushy division
  • E finds theoremhood for 141
  • SRASS finds theoremhood for 171
• In the chainy division
  • E finds theoremhood for 91
  • SRASS finds theoremhood for 127
• Leading the challenge