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 TSTP Solution Library

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

The TPTP Language and Standards

Basic Test Problems

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)