The TPTP problem library and associated infrastructure: ttthe FOF and CNF Parts, v3.5.0

Research output: Contribution to journalArticlepeer-review

263 Scopus citations


This paper describes the First-Order Form (FOF) and Clause Normal Form (CNF) parts of the TPTP problem library, and the associated infrastructure. TPTP v3.5.0 was the last release containing only FOF and CNF problems, and thus serves as the exemplar. This paper summarizes the history and development of the TPTP, describes the structure and contents of the TPTP, and gives an overview of TPTP related projects and tools.

Original languageEnglish (US)
Pages (from-to)337-362
Number of pages26
JournalJournal of Automated Reasoning
Issue number4
StatePublished - Jan 2009


  • ATP system evaluation
  • TPTP

ASJC Scopus subject areas

  • Software
  • Computational Theory and Mathematics
  • Artificial Intelligence

Cite this