TPTP and TSTP Quick Guide

The TPTP and TSTP Libraries

The TPTP (Thousands of Problems for Theorem Provers) is a library of test problems for ATP systems.
- Start at the WWW page http://www.tptp.org.
- For lots of details (the converse of this quick guide) read the technical manual.
- You can browse the TPTP problems online.
The TSTP (Thousands of Solutions from Theorem Provers) is a library of solutions to test problems for ATP systems.
- Start at the WWW page http://www.tptp.org/TSTP.
- There is no technical manual for the TSTP (yet).
- You can browse the TSTP solutions online.

How to use the TPTP language to write problems.
- Sample CNF problem: MGT031-1
- Sample FOF problem: PUZ001+1
- Sample THF problem: LCL633^1
How to use the TPTP language to record derivations.
- Sample derivation (a refutation): EP on PUZ001+1
How to use the TPTP language to record finite interpretations.
- Sample finite interpretation: DarwinFM on MGT031-1
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.

(As a cut-and-paste list: SYN075-1 MGT031-1 MGT041-2 NLP114-1 BOO003-4 BOO027-1 SYN075+1 MGT019+2 KRS063+1 KRS018+1 PUZ131_1 DAT001=1 ARI086=1 LCL580^1 LCL582^1)

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

(As a cut-and-paste list: LDA014-1 MSC015-1.025 ROB032-1 GEO090+1 COM003_1 SYO522=1 LCL634^1)