[ < ] [ > ]   [ << ] [ Up ] [ >> ]         [Top] [Contents] [Index] [ ? ]

7. tpform


[ < ] [ > ]   [ << ] [ Up ] [ >> ]         [Top] [Contents] [Index] [ ? ]

7.1 NAME

tpform - transforms SPASS output statements into TPTP style format


[ < ] [ > ]   [ << ] [ Up ] [ >> ]         [Top] [Contents] [Index] [ ? ]

7.2 SYNOPSIS

tpform [ -tb] [infile] [outfile]


[ < ] [ > ]   [ << ] [ Up ] [ >> ]         [Top] [Contents] [Index] [ ? ]

7.3 DESCRIPTION

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] [ ? ]

7.6 AUTHORS

Thorsten Engel
Christian Theobalt
Contact : Christoph Weidenbach <weidenb@mpi-sb.mpg.de>


[ < ] [ > ]   [ << ] [ Up ] [ >> ]         [Top] [Contents] [Index] [ ? ]

7.7 SEE ALSO

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 Renate Schmidt on March, 10 2003 using texi2html