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 v8.1.0 - 55 domains, 25257 problems
• Five layers of logic CNF, FOF, TFF, TXF, THF ... sixth layer coming NTF
• Documented: References, Status, Rating, Statistics,
• Human and computer readable: Name, Role, Logic, Annotations
• A key - the TPTP language

Tarball and browsing available online at tptp.org