Thousands of Problems for
Theorem Provers

• Aim
  • Provide a simple, unambiguous, source and reference mechanism for ATP problems
  • Centralize the burden of problem collection and maintenance

• Motivation
  • The Bad Old Days

Features

• Currently 5880 problems
• 30 Domains
• Header and formulae in FOF or CNF
• Available from http://www.cs.miami.edu/~tptp