The TPTP Problem Library
for Automated Theorem Proving

by Geoff Sutcliffe and Christian Suttner

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:

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.

If you're new to all this, you might want to start at the TPTP and TSTP Quick Guide.
You could also work your way through the slides of the TPTP World Tutorial.

The TPTP Needs Money  

Recent donors ...   21/11/23 - Nikolaj Bjørner, Microsoft Research    29/09/23 - Anonymous    04/07/23 - Philipp Rümmer, University of Regensburg    23/06/23 - Nikolaj Bjørner, Microsoft Research    03/04/23 - Anonymous    10/05/22 - data experts    04/05/22 - Wolfgang Bibel    24/11/21 - Geoff Alexander, IBM    12/09/21 - Jack McKeown, University of Miami    09/09/21 - Adam Pease, Articulate Software    19/07/21 - André Platzer, Carnegie Mellon University    18/07/21 - Jack Horner, Private    16/07/21 - Pascal Fontaine, Université de Lorraine    15/07/21 - Andrei Voronkov, University of Manchester    15/07/21 - Anonymous    15/07/21 - Konstantin Korovin, University of Manchester    13/07/21 - Michael Rawson, University of Manchester    29/06/21 - Chris Partridge, Brunel University London    10/06/21 - John Hester, University of Florida    20/05/21 - Oscar Contreras, Private    01/12/20 - Pascal Fontaine, Université de Lorraine    02/11/20 - Anonymous    01/06/20 - Anonymous    28/05/20 - Jasmin Blanchette, Vrije Universiteit Amsterdam    22/04/20 - Anonymous    13/02/20 - Laura Kovacs, TU Wien    Today - You (seriously ... do it!)
If your work benefits from use of the TPTP and related projects, consider making an annual cash donation of 100 units of a reasonable currency, to support the TPTP. A donation can be made as an unrestricted gift (tax deductable) to the University of Miami, explicitly to support the TPTP and related projects. Read about the benefits and process of making a donation. A premium support contract is also available.

The current release of the TPTP Library is TPTP-v8.2.0 (Tue Jun 13 15:57:31 EDT 2023)
• TPTP-v8.2.0.tgz Download package, 912MB, expands to 9.7GB. (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
• History and Archive History of changes to the TPTP and the archive of previous versions.
• TPTP2T online Online access to the tptp2T utility.

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 about the TPTP.
• SyntaxBNF The very latest hyperlinked BNF for the TPTP language.

If you would like to cite the TPTP, please use:
        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"
If you would like to cite the TPTP logic languages, please use:
        Author       = "Sutcliffe, G.",
        Year         = "2022",
        Title        = "{The Logic Languages of the TPTP World}",
        Journal      = "Logic Journal of the IGPL",
        DOI          = "10.1093/jigpal/jzac068"

TPTP World Infrastructure
• System on TPTP Services for solving problems and recommending systems.
• 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.
• TMTP The TMTP (Thousands of Models for Theorem Provers) Model Library is a library of models of axiomatizations for automated theorem proving (ATP) systems. In particular, it contains models for TPTP axiomatizations.
• CASC The TPTP is used to supply problems for the CADE ATP System Competition.
• TPTP Tea Party This approximately-annual meeting is used to to discuss the TPTP and related issues.
• TPTP Proposals We are working on new features for the TPTP, as explained in the following proposals. Comments from potential users will be appreciated.
• TPTP Software Many people have written software for processing TPTP format data. These links point to software I know of (please send your link if you have some software to add to the list).
  • Geoff's Service Tools. A bunch of tools for manipulating the TPTP, including the JJ parser for the TPTP language (named after the Spanish software developers, Justo Fernandez Reche and José Taboada Berenguer). The JJ parser will parse TPTP files and build a useful data structure, and there are lots of "useful" API functions for interrogating and manipulating the data structure. There is no documentation for any of this yet, but the sample drivers illustrate how to use the JJ parser API.
  • João Paulo A. Almeida's TPTP Editor as an Eclipse Plugin.
  • Alex Steen's Scala parser for the entire TPTP grammar.
  • Tobias Gleißner's ANTLR4 grammar for the SyntaxBNF-v7.0.0.
  • Guy Shefner's Java class library for parsing, structuring, and basic manipulation of problems in first order logic.
  • Matthias Fuchs' NPM package for the TPTP and SystemOnTPTP.
  • Mark Lemay's Xtext based Java parser for the TPTP grammar.
  • Michael Rawson's Rust parser for the TPTP's FOF and CNF grammars.
• External Projects Other people are collaborating with the TPTP ...

Other people are doing similar things for other types of ATP problems:
• VeriFun Case studies that require induction.
• SV-COMP Benchmark verification tasks in software verification, as used in SV-COMP.
• Larry Wos' Notebooks This website features a series of notebooks presenting some of Larry Wos’s most recent and hitherto unpublished research in automated reasoning (also in 1st order logic).
• SMT-LIB The major goal of SMT-LIB is to establish a library of benchmarks for Satisfiability Modulo Theories, that is, satisfiability of formulas with respect to background theories for which specialized decision procedures exist.
• QMLTP The Quantified Modal Logics Theorem Proving (QMLTP) library provides a platform for testing and benchmarking automated theorem proving (ATP) systems for first-order modal logics.
• DPPD The Dozens of Problems for Partial Deduction (DPPD) Library of Benchmarks aims at being a standard suite of benchmarks for partial deduction.
• Asparagus An environment for submitting and archiving benchmarking Answer-Set Programming (ASP) problems and instances, in which ASP systems can be run under equal and reproducible conditions, leading to independent results.
• ILTP The Intuitionistic Logic Theorem Proving (ILTP) library provides a platform for testing and benchmarking automated theorem proving (ATP) systems for first-order and propositional intuitionistic logic.
• TPBD The Termination Problems Database is a library of test problems for termination provers. Currently, it includes termination problems for term rewrite systems and logic programs.
• CSPLib A benchmark library of problems for the constraints community. The main motivation for CSPLib is to focus research in constraints away from purely random problems and onto more structured problems.
• OR-Library A collection of test data sets for a variety of Operations Research (OR) problems.
• PSPLIB The Project Scheduling Problem Library.
• VFLib The graph matching library, developed mainly to test the VF graph matching algorithm, and to compare it with other known algorithms.
• SATLIB A collection of benchmark problems, solvers, and tools for SAT related research.
• SATEX Experiments and execution traces of SAT solvers, on all benchmarks that are provided.
• QBFLib QBFLIB is a collection of benchmark problems, solvers, and tools related to Quantified Boolean Formula (QBF) satisfiability.

There were 682 unique visitors to the James Cook University site, 1 January 2001 to 21 March 2001. Then the site moved to the University of Miami. Unique visitors to the University of Miami site since 21 March 2001: