The TPTP (Thousands of Problems for Theorem Provers) 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.

• Arbitrary size instances of generic problems (e.g., the N-queens problem).

• A utility to convert the problems to existing ATP systems' formats.

• General guidelines outlining the requirements for ATP system evaluation.

• Standards for input and output for ATP systems.

The principal motivation for the TPTP is to support the testing and evaluation of ATP systems, to help ensure that performance results accurately reflect capabilities of the ATP systems 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 Problem Library is TPTP-v9.3.1 (Fri Aug 21 07:42:58 AM UTC 2026).

• TPTP-v9.3.1.tgz
  Download package, 893MB, expands to 10.5GB. 

Online access to:

• ReadMe
  Basic information.

• Problems and Axiom sets
  Individual problems and axiom sets.

• Documents
  All the TPTP documents

• History and Archive
  History of changes to the TPTP and the archive of previous versions.

• SystemB4TPTP and SystemOnTPTP
  Online access to problem preparation and solving.

• TPTP2T online
  Online access to TPTP2T problem and solution selection.

Current information, available only online:

• Bug list
  Bugged problems list (Bugs found in the current version)

• Technical manual
  Details about the TPTP. Read this whenever you have a question.

• SyntaxBNF
  The very latest hyperlinked BNF for the TPTP language.

If you would like to cite the TPTP problem library, please use:

@Article{Sut17,

    Author       = "Sutcliffe, G.",

    Year         = "2017",

    Title        = "{The TPTP Problem Library and Associated Infrastructure.

                    From CNF to TH0, TPTP v6.4.0}",

    Journal      = "Journal of Automated Reasoning",

    Volume       = "59",

    Number       = "4",

    Pages        = "483-502",

    DOI          = "10.1007/s10817-017-9407-7"

}

If you would like to cite the TPTP logic languages, please use:

@Article{Sut22,

    Author       = "Sutcliffe, G.",

    Year         = "2022",

    Title        = "{The Logic Languages of the TPTP World}",

    Journal      = "Logic Journal of the IGPL",

    DOI          = "10.1093/jigpal/jzac068"

}

Other people are doing similar things for other types of ATP problems:

• SUMO
  The Suggested Upper Merged Ontology in TPTP format

• Mizar-TPTP
  Semantic Presentation

• VeriFun
  Case studies that require induction.

• SV-COMP
  Benchmark verification tasks in software verification, as used in SV-COMP.

• Larry Wos' Notebooks
  A series of notebooks presenting some of Larry Wos's unpublished research

• SMT-LIB
  A library of benchmarks for Satisfiability Modulo Theories.

• QMLTP
  The Quantified Modal Logics Theorem Proving library for first-order modal logics.

• ILTP
  The Intuitionistic Logic Theorem Proving library intuitionistic logic.

• TPBD
  The Termination Problems Database for termination provers.

• CSPLib
  A library of problems for the constraints community.

• OR-Library
  Test data sets for a variety of Operations Research problems.

• SATLIB
  Benchmark problems, solvers, and tools for SAT related research.

• QBFLib
  Benchmark problems, solvers, and tools for Quantified Boolean Formulae.