TPTP and TSTP Quick Guide
The TPTP Language
The TPTP Problem Library
The TPTP (Thousands of Problems for Theorem Provers) is a
library of test problems for ATP systems.
The TSTP Solution Library
The TSTP (Thousands of Solutions from Theorem Provers) is a
library of solutions to TPTP problems.
Test Problems
The SYN000* problem files are contrived to use most features of the TPTP language, and
are thus suitable for testing parsers, etc.
- 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
- TFF problem contrived to use non-classical parts of the TPTP language:
SYN000_6
- THF problem contrived to use non-classical parts of the TPTP language:
SYN000^6
Here are some 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)