The TPTP Problem Library

A Library of Test Problems

• Aim
  • A simple, unambiguous, source and reference mechanism
  • Centralize problem collection and maintenance
  • Improve ATP system testing and evaluation

• Motivation
  • Statistically significant results
  • Repeatability of testing
  • Meaningful system evaluations and comparisons

Features

• First released Fri Nov 12 15:30:54 +1000 1993
• TPTP v9.0.0 - 55 domains, 25779 problems
• Six logics families: PRP, FOF, TFF, TXF, THF, NTF
• Documented: References, Status, Rating, Statistics,
• Human and computer readable: Name, Role, Logic, Annotations
• include directives
• A key - the TPTP language

Tarball and browsing available online at tptp.org