8. tpget
8.1 NAME
tpget - selects problems from a library
8.2 SYNOPSIS
tpget [-l libdir] file_1 ... file_n target
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'.
8.4 Options
The following option is required by tpget:
- -l
- Specifies the library where problem files are taken from.
8.5 EXAMPLES
To assemble all problem files specified by file into Dir, using the library /foo/bar:
- tpget -l /foo/bar file Dir
8.6 AUTHORS
Thorsten Engel
Christian Theobalt
Enno Keen
Contact : Thomas Hillenbrand <hillen@mpi-sb.mpg.de>
Christoph Weidenbach <weidenb@mpi-sb.mpg.de>
8.7 SEE ALSO
checkstat(1), filestat(1), pcs(1), pgen(1), rescmp(1), tpform(1), deprose(1), dfg2otter(1), dfg2otterpl(1), SPASS(1)
This document was generated
by Renate Schmidt on March, 10 2003
using texi2html