TPTP/TSTP Mode
Prover9 reads TPTP FOF/CNF input and produces SZS status lines and TSTP-format proofs, enabling direct integration with the TPTP toolchain, CASC competition, and comparison with other provers (E, Vampire).Invoking TPTP Mode
Input Mode
Any of these invocations enables TPTP input:prover9 problem.p # Auto-detected by .p extension. prover9 -tptp < input # Force TPTP input from stdin. prover9 -tptp -f problem.p # Explicit flag with file argument.The .p extension is matched on the last two characters of the filename.
Output Mode (TSTP/SZS)
- Auto-enabled when TPTP input is detected (any of the above).
- Or manually: -tptp_out flag, or set(tptp_output). in native input.
- Can be disabled in TPTP input via magic comment:
% prover9: clear(tptp_output).
What tptp_output Does
When tptp_output is set to TRUE, the following flags are automatically changed via dependency rules:| Flag | Value |
|---|---|
| default_output | FALSE |
| quiet | TRUE |
| echo_input | FALSE |
| print_initial_clauses | FALSE |
| print_given | FALSE |
| bell | FALSE |
| stats | "none" |
The net effect: native banners, statistics, separators, and clause echo are all suppressed. Only SZS status lines and TSTP proofs appear on stdout.
Users can override any of these after tptp_output is set, e.g.:
% prover9: set(print_given).
When diagnostic flags (print_given, print_gen, print_kept, print_labeled) are enabled in TPTP mode, their output lines are automatically prefixed with "% " so TPTP parsers treat them as comments. For example:
% given #1 (I,wt=6): 9 -hates(agatha,A) | -hates(charles,A). [assumption]. % generated: hates(butler,agatha). [resolve(14,a,11,a)]. % kept: 23 hates(butler,agatha). [resolve(14,a,11,a)].
TPTP Language Support
Formula Types
fof(name, role, formula). % First-order formulas. cnf(name, role, clause). % Clausal normal form.
Include Directives
include('file'). % Include all formulas from file.
include('file', [n1, n2]). % Include only named formulas.
Roles
| Role | Handling |
|---|---|
| conjecture | Goal formula (negated for refutation). |
| axiom | Assumption. |
| hypothesis | Assumption. |
| lemma | Assumption. |
| theorem | Assumption. |
| plain | Assumption. |
| definition | Assumption. |
| assumption | Assumption. |
| negated_conjecture | Assumption (already negated). |
| type | Skipped with warning. |
| unknown | Skipped with warning. |
| (any other) | Treated as assumption with warning. |
Variables
Uppercase (Prolog convention), automatically detected.
Connectives
| Symbol | Meaning | Symbol | Meaning |
|---|---|---|---|
| & | and | | | or |
| ~ | negation | => | implication |
| <=> | biconditional | <~> | exclusive or |
| ~| | nor | ~& | nand |
| ! | universal | ? | existential |
Built-ins
| Symbol | Meaning |
|---|---|
| $true | verum |
| $false | falsum |
Include Path Resolution
Include paths are resolved in this order:- Direct: open filename as given (absolute or relative to cwd).
- TPTP env var: $TPTP/<filename>.
- /Problems/ auto-detect: search the source file path for "/Problems/", extract the TPTP root, and resolve the include relative to that root. If the source path is a bare filename, realpath() is used to get the full path before searching.
Magic Comments (Prover9 Options in TPTP Files)
TPTP files can contain Prover9 option directives in comments:% prover9: set(flag_name). % prover9: clear(flag_name). % prover9: assign(parm_name, value).These are collected during parsing and processed before the search begins. They can override the auto-set tptp_output flag.
Examples:
% prover9: assign(max_seconds, 60). % prover9: set(print_given). % prover9: clear(tptp_output). % prover9: assign(max_megs, 4096).
SZS Status Output
On exit, Prover9 prints an SZS status line:% SZS status <Status> for <problem_name>The problem name is extracted from the .p filename (basename with extension stripped). If no .p file was given, the "for <name>" suffix is omitted.
| Exit Condition | SZS Status |
|---|---|
| Proof found, goals present | Theorem |
| Proof found, no goals | Unsatisfiable |
| SOS empty, goals present | GaveUp |
| SOS empty, no goals | Satisfiable |
| max_seconds exceeded | Timeout |
| max_megs exceeded | MemoryOut |
| max_given exceeded | GaveUp |
| max_kept exceeded | GaveUp |
| action exit | GaveUp |
| SIGSEGV or fatal error | Error |
| SIGINT | User |
| Checkpoint exit | Unknown |
The distinction between Theorem/Unsatisfiable and GaveUp/Satisfiable depends on whether goal or conjecture formulas were present in the input.
TSTP Proof Format
Proofs are wrapped in SZS output delimiters:% SZS output start CNFRefutation for <problem_name> ... TSTP annotated formulas ... % SZS output end CNFRefutation for <problem_name>Each proof step has the form:
cnf(c_ID, role, (literals), source).
Leaf Nodes (Input Clauses)
cnf(c_1, axiom, (p(X) | ~q(X)), introduced(assumption,[])). cnf(c_5, negated_conjecture, ~p(a), introduced(assumption,[])).
Goal Formulas (FOF Conjectures in Non-Flattened Proofs)
fof(c_3, negated_conjecture, formula, introduced(conjecture,[])).
Inference Steps
cnf(c_42, plain, r(a),
inference(resolve, [status(thm)], [c_1, c_5])).
Inference Rule Name Mapping
| Prover9 Internal | TSTP Name |
|---|---|
| BINARY_RES_JUST | resolve |
| HYPER_RES_JUST | hyper |
| UR_RES_JUST | ur |
| PARA_JUST (all) | paramod |
| FACTOR_JUST | factor |
| BACK_DEMOD_JUST | back_demod |
| BACK_UNIT_DEL_JUST | back_unit_del |
| DEMOD_JUST | rewrite |
| UNIT_DEL_JUST | unit_del |
| FLIP_JUST | flip |
| MERGE_JUST | merge |
| COPY_JUST | copy |
| DENY_JUST | assume_negation |
| CLAUSIFY_JUST | clausify |
| NEW_SYMBOL_JUST | new_symbol |
| EXPAND_DEF_JUST | expand_def |
| PROPOSITIONAL_JUST | propositional |
| INSTANCE_JUST | instantiate |
| EVAL_JUST | eval |
| XXRES_JUST | xxres |
Negation symbol: LADR "-" is converted to TPTP "~" in output. Variables are printed in uppercase (Prolog convention) in proof output.
FOF Flattening for GDV Compatibility
When the proof contains FOF entries (axioms or conjectures), the TSTP printer automatically flattens the FOF layer into CNF leaf nodes to avoid GDV verification failures:- FOF axioms are omitted from output. Their clausified CNF children are promoted to axiom leaves.
- FOF conjectures are omitted. Their denial CNF children are promoted to negated_conjecture leaves.
This avoids two GDV failure modes:
- Clausify from FOF axiom: multi-clause Skolemization means individual clauses aren't equisatisfiable with the parent.
- Assume_negation (deny): combines negation + clausification, so the CNF denial is neither equisatisfiable nor a theorem of the FOF conjecture.
The resulting proof is a pure CNF refutation with all leaf nodes either axiom or negated_conjecture, and all inferences status(thm).
GDV Verification
Proofs can be verified with GDV (Global Derivation Verifier).Online via SystemOnTPTP
Save Prover9 output to a file (it is valid TSTP), then submit to SystemOnTPTP for verification.Local GDV
GDV has deep recursion requiring a larger stack:ulimit -s 32768 /path/to/GDV -q2 -t 30 proof_output.pGDV verbosity levels:
| Flag | Output |
|---|---|
| -q0 | Full output |
| -q1 | Results + ATP details |
| -q2 | Results only |
| -q3 | SZS status only |
For Ivy (ACL2) proof verification, use -ladr_out to get native LADR output, then prooftrans ivy to convert to an Ivy proof object. The same LADR output can also be converted to TSTP for GDV via prooftrans tstp.
Examples
Example 1: Simple CNF Problem
File: animals.pcnf(wolves_are_animals, axiom, animal(X) | ~wolf(X)). cnf(there_is_a_wolf, axiom, wolf(fido)). cnf(goal, negated_conjecture, ~animal(fido)).Run:
prover9 animals.pOutput:
% SZS status Unsatisfiable for animals
% SZS output start CNFRefutation for animals
cnf(c_1, axiom, (animal(X) | ~wolf(X)), introduced(assumption,[])).
cnf(c_2, axiom, wolf(fido), introduced(assumption,[])).
cnf(c_3, negated_conjecture, ~animal(fido), introduced(assumption,[])).
cnf(c_4, plain, animal(fido),
inference(resolve, [status(thm)], [c_1, c_2])).
cnf(c_5, plain, $false,
inference(resolve, [status(thm)], [c_3, c_4])).
% SZS output end CNFRefutation for animals
Example 2: FOF Problem with Conjecture
File: mortal.pfof(all_men_mortal, axiom, ! [X] : (man(X) => mortal(X))). fof(socrates_is_man, axiom, man(socrates)). fof(goal, conjecture, mortal(socrates)).Run:
prover9 mortal.pOutput:
% SZS status Theorem for mortal
% SZS output start CNFRefutation for mortal
cnf(c_2, axiom, (mortal(X) | ~man(X)), introduced(assumption,[])).
cnf(c_3, axiom, man(socrates), introduced(assumption,[])).
cnf(c_4, negated_conjecture, ~mortal(socrates), introduced(assumption,[])).
cnf(c_5, plain, mortal(socrates),
inference(resolve, [status(thm)], [c_2, c_3])).
cnf(c_6, plain, $false,
inference(resolve, [status(thm)], [c_4, c_5])).
% SZS output end CNFRefutation for mortal
Note: the FOF axioms and conjecture are flattened away; their CNF
children appear as axiom/negated_conjecture leaves. This is the
"Theorem" status because a conjecture was present.
Example 3: Using Magic Comments for Options
File: hard_problem.p% prover9: assign(max_seconds, 300). % prover9: assign(max_megs, 8192). % prover9: set(print_given). fof(ax1, axiom, ! [X] : (p(X) => q(X))). fof(ax2, axiom, p(a)). fof(goal, conjecture, q(a)).The magic comments set a 5-minute timeout, 8 GB memory limit, and enable printing of given clauses (which tptp_output normally suppresses).
Example 4: Verifying Output with GDV
# Run Prover9 on a TPTP problem, save output prover9 /path/to/TPTP/Problems/PUZ/PUZ001+1.p > proof.p # Verify with local GDV ulimit -s 32768 /path/to/GDV -q2 -t 30 proof.pExpected GDV output:
SZS status Verified for PUZ001+1
Comparison with E Prover
Both Prover9 (with tptp_output) and E produce SZS status lines and TSTP proofs. Key differences:| Feature | Prover9 (tptp_output) | E prover |
|---|---|---|
| Default output level | Suppresses givens, stats, banners. | Silent (level 0). |
| Print given clauses | set(print_given) or magic comment. | eprover -l 1 |
| SZS status format | % SZS status X for Y (with problem name) | % SZS status X (depends on flags) |
| Proof format | CNFRefutation (FOF flattened) | Various (default CNFRefutation) |
| Variables | Uppercase (Prolog) | Uppercase (Prolog) |
SZS status cross-checked against E 3.2.5 on 29 problems across 12 TPTP domains: 100% agreement on all problems where both provers returned a result.
Troubleshooting
- Include files not found.
- Set the TPTP environment variable to your TPTP root directory. Or run from within the TPTP directory tree so /Problems/ auto-detection works.
- GDV segfaults.
- GDV needs a larger stack: ulimit -s 32768 (32 MB).
- Prover9 prints native output instead of TSTP.
- Ensure the file has a .p extension, or use the -tptp flag. Check that clear(tptp_output) is not in a magic comment.
- GDV rejects the proof.
- FOF flattening should be automatic. If not, check that the proof contains the expected CNFRefutation delimiters. Ensure the proof file includes the full Prover9 output (SZS status + proof block).