- The WWW page is
`tptp.org/TPTP`. - Here's a brief overview of how to use the TPTP language to write problems.
- 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 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`

- Sample derivation (a refutation):
E on
- Here's a brief overview of how to use the TPTP language to
record finite interpretations.
- Sample finite interpretation:
DarwinFM on
`MGT031-1`

- Sample finite interpretation:
DarwinFM on
- There is no technical manual for the TSTP (yet).
- You can browse the TSTP solutions online.

- The TPTP language grammar in BNF.
- The SZS ontology of results that a system may establish for a problem.

- CNF Unsatisfiable:
`SYN075-1` - CNF Satisfiable:
`MGT031-1` - EPR Unsatisfiable:
`MGT041-2` - EPR Satisfiable:
`NLP114-1` - UEQ Unsatisfiable:
`BOO003-4` - UEQ Satisfiable:
`BOO027-1` - FOF Theorem:
`SYN075+1` - FOF CounterSatisfiable:
`MGT019+2` - FOF Unsatisfiable:
`KRS063+1` - FOF Satisfiable:
`KRS018+1` - TFF Theorem:
`PUZ131_1` - TFF CounterSatisfiable: No example
- TFA Theorem:
`DAT001=1` - TFA CounterSatisfiable:
`ARI086=1` - THF Theorem (in Henkin semantics):
`LCL580^1` - THF CounterSatisfiable (in Henkin semantics):
`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.

- CNF Timeout:
`LDA014-1` - EPR Timeout:
`MSC015-1.025` - UEQ Timeout:
`ROB032-1` - FOF Timeout:
`GEO090+1` - TFF Timeout:
`COM003_1` - TFA Timeout:
`SYO522=1` - THF Timeout:
`LCL634^1`