[ < ] | [ > ] | [ << ] | [ Up ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |
[ < ] | [ > ] | [ << ] | [ Up ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |
[ < ] | [ > ] | [ << ] | [ Up ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |
[ < ] | [ > ] | [ << ] | [ Up ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |
If no file arguments are given, tpform reads from stdin and writes to stdout. If one file argument is given, tpform read from that file, and if a second argument is present, tpform writes to it.
[ < ] | [ > ] | [ << ] | [ Up ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |
SteamRoller + 00:00:05.28
[ < ] | [ > ] | [ << ] | [ Up ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |
We take the following SPASS output as an example:
SPASS V0.78 SPASS beiseite: Proof found. Problem: Tests/Pelletier/problem1.dfg SPASS derived 0 clauses, backtracked 0 clauses and kept 3 clauses. SPASS allocated 165 KBytes. SPASS spent 0:00:00.01 on the problem. 0:00:00.00 for the input. 0:00:00.00 for the FLOTTER CNF translation. 0:00:00.00 for inferences. 0:00:00.00 for the backtracking. |
The TPTP format for this information is:
problem1.dfg P 1 0.01 165 3 - - ^ ^ ^^^^ ^^^ ^ ^ ^ P/M # proofs time memory clauses proof proof or error length depth message |
The simple format is for this example:
problem1.dfg + |
and in general:
filename {+|-|0} [time] |
where '+' marks problems for which SPASS found a proof, '0' stands for found completions and '--' marks undecided problems. The time information is given if the -t option is used.
[ < ] | [ > ] | [ << ] | [ Up ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |
[ < ] | [ > ] | [ << ] | [ Up ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |
[ << ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |