TPTP-v4.0.1 ReadMe
------------------ Mon Nov 16 13:13:18 EST 2009.

(Please read the TPTP technical report for full details about the TPTP.)

Description
-----------
The TPTP  (Thousands  of Problems  for Theorem  Provers)  Problem Library  is a
library of test problems for automated theorem proving (ATP) systems.  The TPTP
supplies the ATP community with:
+ A comprehensive library of the ATP test problems that are available today, in
  order to provide an overview and a simple, unambiguous reference mechanism.
+ A comprehensive list of references and other interesting information for each
  problem.
+ Arbitary size instances of generic problems (e.g., the N-queens problem).
+ A utility to convert the problems to existing ATP systems' formats.
+ General guidelines outlining the requirements for ATP system evaluation.
+ Standards for input and output for ATP systems.

The principal motivation  for the TPTP is to support the testing and evaluation
of ATP systems,  to help ensure that performance results accurately reflect the
capabilities of the ATP system  being considered.  A common library of problems
is necessary for meaningful system evaluations,  meaningful system comparisons,
repeatability  of testing,  and  the  production of  statistically  significant
results. The TPTP is such a library.

The TPTP  is the work  of Geoff Sutcliffe  and Christian  Suttner.  The TPTP is
maintained and  distributed from the Department of Computer Science, University
of Miami, USA.

The TPTP  is regularly updated.  If you would like to  become a registered TPTP
user  and be  kept informed  of developments,  please email Geoff Sutcliffe  at
geoff@cs.miami.edu.

Simple  instructions for  obtaining and installing  the TPTP  are given in  the
Quick Installation Guide at the end of this ReadMe file.

Files
-----
The  TPTP  files  are kept  in various  directories,  as described  below.  The
directory structure  should not  be changed,  as the TPTP  software is coded to
work in the structure as distributed.

ReadMe-v4.0.1 - This file.
TPTP-v4.0.1.tgz - The TPTP problem library, which expands to :
+ Axioms     - The axiom files directory.  Axiom files are  merged into problem
               files.
+ Problems   - The problem files directory with subdirectories for each domain.
               The  subdirectories  contain  problem  files  with  the formulae
               specific to each problem.
+ Generators - The  generator files  directory.  Generator files  are  used  to
               generate  instances  of  generic  problems,  according  to  user
               supplied size parameters.
+ Documents  - A  directory containing  documents that relate to the TPTP.  The
               files  contain comprehensive  online information about the TPTP,
               and provide  quick access  to data that is  useful for using the
               TPTP, using standard system tools (e.g., grep, awk).
+ TPTP2X     - The directory containing the tptp2X utility. The tptp2X utility:
               * Converts from  the TPTP format to formats used by existing ATP
                 systems.
               * Applies transformations to the clauses of TPTP problems.
               * Controls  the  generation  of  TPTP  problem  files  from TPTP
                 generator files.
+ Scripts    - A directory containing  shell scripts that  may be used with the
               TPTP.
BuggedProblems-v4.0.1 - A list  of bugs in  the current TPTP  (bugs found after
               release).

Conditions of use
-----------------
By providing  this library  of ATP problems,  and a specification  of how these
problems should  be presented to ATP systems,  it is our intention to place the
testing,  evaluation,  and comparison of  ATP systems onto a firm footing.  For
this reason,  you should  abide  by the  following conditions  when using  TPTP
problems and presenting your results.
+ The TPTP release number must be stated.
+ Each problem must be referenced by its unambiguous name.
+ The problem formulae should, as far as is possible, not be changed in any way.
  Any changes made (addition,  removal, reordering, reformatting, etc.) must be
  explicitly noted.
+ Any information  given to the  ATP system,  other than  that in the formulae, 
  must be explicitly noted.  All system switches and settings must be recorded.
  The header information  in TPTP  problems may not  be used  by the ATP system 
  without explicit notice.

Please email Geoff if :
-----------------------
+ You find any mistakes in the TPTP.
+ You are able to provide further information for a TPTP problem.
+ You want to contribute a problem to the TPTP. Please use the problem template
  that comes  with the distribution,  and fill in header information  as far as
  possible. Any unambiguous representation will do for the formulae.
+ You have any suggestions for improving the TPTP library.

General Disclaimer
------------------
Every effort has been made to ensure that the TPTP problems have been correctly
presented, and that appropriate acknowledgments have been made.  However, we do
not guarantee that we have succeeded,  and accept  no  responsibility  for  any
errors or omissions.  We will gratefully receive comments and  corrections.

Copyright
---------
The TPTP is copyrighted (c) 1993-2009,  by Geoff Sutcliffe & Christian Suttner.
Use and verbatim redistribution of the TPTP are permitted.  Distribution of any
modified version or modified part of the TPTP requires permission.

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

                         TPTP Quick Installation Guide
                         -----------------------------

This explains how to obtain, install, and syntax-convert the TPTP problems. For
more details, explanations, and further options, see the TPTP technical report.

1. Obtaining the TPTP

   Use the World Wide Web (WWW) with the following URL :
      http://www.tptp.org


2. Installing the TPTP

   prompt> tar xzf TPTP-v4.0.1.tgz
   prompt> cd TPTP-v4.0.1
   prompt> ./Scripts/tptp2T_install
           <... the script will then ask for required information>
   prompt> ./TPTP2X/tptp2X_install
           <... the script will then ask for required information>

   If you don't have any Prolog installed, you need to get one first.
   Both utilities can be installed in a default configuration by appending a
   -default flag to the install command.


3. Converting all the TPTP problems to the syntax of other ATP systems

   prompt> ./TPTP2X/tptp2X -f<Format>

   where  the  available  <Format>s  can  be  seen  as  the  extensions  of the 
   TPTP2X/format.* files.

   Some of the formats cannot cope with certain types of problems, e.g., dimacs
   format  is for  only  propositional  CNF problems.  The  tptp format  simply
   expands include directives, producing files in the TPTP Prolog-style syntax.
   tptp2X  offers MUCH  more than  this.  See the  TPTP technical  report for a
   detailed description of the utility, including information on how to produce
   output in your own syntax.

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