TPTP and TSTP Quick Guide

The TPTP Problem Library

The TPTP (Thousands of Problems for Theorem Provers) is a library of test problems for ATP systems.

The WWW page is tptp.org/TPTP.
Here's a brief overview of how to use the TPTP language to write problems.
- Sample CNF problem: MGT031-1
- Sample FOF problem: PUZ001+1
- Sample TFF problem: PUZ131_1
- Sample TFF problem with arithmetic (TFA): DAT001_1
- Sample THF problem: LCL633^1
For lots of details (the converse of this quick guide) read the technical manual.
You can browse the TPTP problems online.
Here is a series of fun examples using the various logic languages of the TPTP World.

The TSTP (Thousands of Solutions from Theorem Provers) is a library of solutions to TPTP problems.

The WWW page is tptp.org/TSTP.
Here's a brief overview of how to use the TPTP language to record derivations.
- Sample derivation (a refutation): E on PUZ001+1
Here's a brief overview of how to use the TPTP language to record finite interpretations.
- Sample finite interpretation: DarwinFM on MGT031-1
There is no technical manual for the TSTP (yet).
You can browse the TSTP solutions online.

The TPTP language grammar in BNF.
- CNF problem contrived to use common parts of the TPTP language: SYN000-1
- FOF problem contrived to use common parts of the TPTP language: SYN000+1
- TFF problem contrived to use common parts of the TPTP language: SYN000_1
- THF problem contrived to use common parts of the TPTP language: SYN000^1
The SZS ontology of results that a system may establish for a problem.

These are easy test problems that should be solved with the given SZS result.

These are hard test problems. If you solve any of these then either your system is very good, or your system is unsound.