The TPTP Problem Library
for Automated Theorem Proving

The TPTP (Thousands of Problems for Theorem Provers) Problem Library is a library of test problems for automated theorem proving (ATP) systems. The TPTP supplies the ATP community with:

• A comprehensive library of the ATP test problems that are available today, in order to provide an overview and a simple, unambiguous reference mechanism.
• A comprehensive list of references and other interesting information for each problem.
• New generalized variants of problems whose original presentation is hand-tailored towards a particular automated proof.
• Arbitrary size instances of generic problems (e.g., the N-queens problem).
• A utility to convert the problems to existing ATP formats. Currently the Bliksem, CARINE, CLIN-S, Dedam, DFG, DIMACS, FINDER, ILF, KIF, leanTAP, 3TAP, METEOR, MGTP, OSCAR, OTTER, PROTEIN, PTTP, Satchmo, SCOTT, SEM, SETHEO, SPRFN, THINKER, Waldmeister formats are supported, and other formats can be easily produced.
• General guidelines outlining the requirements for ATP system evaluation.

The principal motivation for the TPTP is to move the testing and evaluation of ATP systems from the previously ad hoc situation onto a firm footing. This became necessary, as results being published do not always accurately reflect the capabilities of the ATP system being considered. A common library of problems is necessary for meaningful system evaluations, meaningful system comparisons, repeatability of testing, and the production of statistically significant results. The TPTP is such a library.

The current release of the TPTP Library is TPTP-v3.0.1, containing 7267 test problems.
TPTP-v3.0.1.tar.gz	Download package, 7.7 Mbytes. (Contains the problems, axiom sets, documents, and utilities.)
Online access to:
ReadMe	Basic information.
Problems	Individual problems.
Axiom sets	Individual axiom sets.
Documents	All the TPTP documents (now including the BNF specification of the new TPTP syntax, and the SZS problem status ontology)
History and Archive	History of changes to the TPTP and the archive of previous versions.
Current information, available only online:
BuggedProblems-v3.0.1	Bugged problems list (Bugs found in the current version)
Technical Manual	Details about the TPTP. Read this whenever you have a question about the TPTP.
There are several TPTP subprojects:
System on TPTP	For TPTP problems, and other problems in TPTP syntax, we provide recommendations for systems we think are likely to succeed. We can also attempt to solve the problem for you, on our machine, using a prover of your choice or one that we recommend!
TSTP	The TSTP (Thousands of Solutions from Theorem Provers) Solution Library is a library of solutions to test problems for automated theorem proving (ATP) systems. In particular, it contains solutions to TPTP problems.
CASC	The TPTP is used to supply problems for the CADE ATP System Competition.
TPTP Citations	We are collecting references for papers that cite the TPTP. If you have cited the TPTP in any of your work that is not yet included, we'd like to add your reference. If you would like to cite the TPTP, please use: @Article{SS98, Author = "Sutcliffe, G. and Suttner, C.B.", Year = "1998", Title = "{The TPTP Problem Library: CNF Release v1.2.1}", Journal = "Journal of Automated Reasoning", Volume = "21", Number = "2", Pages = "177-203", Comment = "REAL,ATPProgress,SystemOnTPTP,TPTPCite" }
Sorted FOF TPTP	We are working on a syntax for FOF problems with sorts. Comments from potential users will be appreciated.
The TPTP Tea Party is a meeting to discuss the TPTP and related issues.
2005	Organized with Josef Urban as part of CADE-20.
2004	Hosted by Simon Colton at Imperial College London.
Other people are doing similar things for other types of ATP problems:
Termination Problems Database	TPDB is a library of test problems for termination provers. Currently, it includes termination problems for Term rewrite systems and logic programs.
Induction Challenge Problems	Louise Dennis maintains a collection of induction challenge problems.
Induction Problems	Ian Green maintains the Dream corpus of inductive conjectures. This is a corpus of approximately 1000 conjectures and associated definitions.
Propositional Problems	Holger Hoos and Thomas Stuetzle maintain a collection of benchmark problems, solvers, and tools for SAT related research.
Propositional Problems	Laurent Simon is gathering experiments and providing execution traces of provers on all benchmarks that are provided.
Constraint Satisfaction Problems	Toby Walsh, Ian Gent, and Bart Selman are putting together a benchmark library of problems for the constraints community, called CSPLib. The main motivation for CSPLib is to focus research in constraints away from purely random problems and onto more structured problems.