===============================================================================

Introduction
------------
The tptp2X utility is a multi-functional utility for reformating, transforming,
and generating TPTP problem files. In particular, it
+ Converts from the TPTP format to formats used by existing ATP systems.
+ Applies various transformations to the clauses of TPTP problems.
+ Controls the generation of TPTP problem files from TPTP generator files.

Installation
------------
The tptp2X code should run on most Prolog systems**. There is some code that is
specific to the BinProlog,  SICStus 2.1,  Quintus, and Eclipse Prolog dialects.
Before using tptp2X,  it is necessary  to install the  code for the dialect  of
Prolog that is to be used.  Installation of the tptp2X  utility requires simple
changes in the tptp2X script, the tptp2X.config file, and the tptp2X.main file.
These changes  can be made  by running  tptp2X_install,  which will prompt  for
required information. More information about installing tptp2X can  be found in
the TPTP technical report.

** In particular,  the tptp2X code  will run on  BinProlog 3.45.  BinProlog  is
   written  by Paul Tarau of the University  of Moncton (Canada), and is freely
   available by anonymous ftp, from
       clement.info.umoncton.ca:pub/BinProlog
   or from the CMU AI Repository
       ftp.cs.cmu.edu:/user/ai/lang/prolog/impl/prolog/bin_pl/bp

Using tptp2X
------------
The most convenient  way of using the tptp2X utility is  through the tptp2X csh
script. The use of this script is :

tptp2X [-q<Level>][-i][-s<Size>][-t<Transform>][-f<Format>][-d<Dir>] <TPTPFiles>

A common first use of tptp2X is to convert TPTP problems to another format.  To
convert all  TPTP problems  to another  format,  the use  is tptp2X -f<Format>,
where <Format> is one of kif, leantap, tap,  meteor, mgtp, otter, pttp, setheo,
sprfn,  tptp,  e.g. tptp2X -fotter.  To limit  the conversion  to one  or  more
domains,   the   domain  names   are  specified  after  the   <Format>,   e.g.,
tptp2X -fleantap ALG GRP LDA.
***** If you are a new TPTP user, this is probably the use that you want. *****

The  other tptp2X  script flags  give the  user many  options for  reformating,
transforming,  and generating TPTP problem files.  More information about using
the tptp2X script can be found in the TPTP technical report.

===============================================================================
