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

8. tpget


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

8.1 NAME

tpget - selects problems from a library


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

8.2 SYNOPSIS

tpget [-l libdir] file_1 ... file_n target


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

8.3 DESCRIPTION

tpget reads lists of theorem proving problems in TPTP format (TPTP scripts) and assembles the problem files specifying these problems into a target directory . The problem files are taken from the library specified by the -l option (see example below). If a problem file already exists in the target directory it is not copied again.

The files file_1 ... file_n have to contain one short problem name per line. Examples for short problem names are `SYN313-1.001:002' or `LCL354+1'.


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

8.4 Options

The following option is required by tpget:

-l
Specifies the library where problem files are taken from.


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

8.5 EXAMPLES

To assemble all problem files specified by file into Dir, using the library /foo/bar:
tpget -l /foo/bar file Dir


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

8.6 AUTHORS

Thorsten Engel
Christian Theobalt
Enno Keen
Contact : Thomas Hillenbrand <hillen@mpi-sb.mpg.de>
Christoph Weidenbach <weidenb@mpi-sb.mpg.de>


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

8.7 SEE ALSO

checkstat(1), filestat(1), pcs(1), pgen(1), rescmp(1), tpform(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