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.

[ < ]

[ > ]

[ << ]

[ Up ]

[ >> ]

[Top]

[Contents]

[Index]

[ ? ]

7.4 OPTIONS

The following options are supported by tpform:

-b: Selects simple output format instead of TPTP format
-t: If -b is selected, print SPASS running time at the end of each output line, eg: SteamRoller + 00:00:05.28

[ < ]

[ > ]

[ << ]

[ Up ]

[ >> ]

[Top]

[Contents]

[Index]

[ ? ]

7.5 FORMATS

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]

[ ? ]