The TPTP Language
How to write problems
How to write derivations
How to write interpretations
The SZS ontology for problem and solution status
The TPTP (Thousands of Problems for Theorem Provers) is a library of test problems for ATP systems.
The WWW page is tptp.tptp.org
You can browse the TPTP problems online.
Se the FOF problem PUZ001+1
Here are some fun examples using the various logic languages of the TPTP World:
CNF FOF TF0 TF1 TX0 TX1 TH0 TH1 NX0 NX1 NH0 NH1
The TSTP (Thousands of Solutions from Theorem Provers) is a library of solutions to TPTP problems.
The WWW page is tstp.tptp.org.
You can browse the TSTP solutions online.
See proofs (mostly refutations) for the FOF problem PUZ001+1
The SYN000* problem files are contrived to use most features of the TPTP language, and are thus suitable for testing parsers, etc.
Here are some easy test problems that should be solved with the given SZS result:
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
TF0 Theorem: PUZ131_1
TF0 CounterSatisfiable: NUM870_1
TFA Theorem: DAT001_1
TFA CounterSatisfiable: ARI086_1
TX0 Theorem: PUZ082_8
TX0 CounterSatisfiable: SYO934_1
NX0 Theorem: SYO886_1.111
TH0 Theorem: LCL580^1
TH0 CounterSatisfiable: NUM803^5
NH0 Theorem: PHI002^8
DH0 Theorem: CAT039^1
DH0 CounterSatisfiable: SEV600^1
These are hard test problems. If you solve any of these then either your system is very good, or your system is unsound.