| [ << ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |
tpform - transforms SPASS output statements into TPTP style format
tpform [ -tb] [infile] [outfile]
The tpform script transforms a list of SPASS outputs into a TPTP result file or another simple file format. Both formats are a list of problem file names annotated with information, like the logical status of the problem and time needed to decide the status etc.
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.
The following options are supported by tpform:
Selects simple output format instead of TPTP format
If -b is selected, print SPASS running time at the end of each output line, eg:
SteamRoller + 00:00:05.28
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.
Thorsten Engel and Christian Theobalt.
Contact : spass@mpi-inf.mpg.de
checkstat(1), filestat(1), pcs(1), pgen(1), rescmp(1), tpget(1), deprose(1), dfg2otter(1), dfg2otterpl(1), SPASS(1)
| [ << ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |
This document was generated by Christoph Weidenbach on February, 23 2010 using texi2html 1.78.