The TPTP Problem Library

A Library of Test Problems

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

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

Features

• First released Fri Nov 12 15:30:54 +1000 1993
• TPTP v9.3.1 - 58 domains, 26990 problems
• Seven logics families: PRP, FOF, TFF, TXF, THF, NTF, DHF
• 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.tptp.org