-------------------------------------------------------------------------------
Release v3.0.1, Wed Dec 8 08:58:57 EST 2004
 
Changes from v3.0.0 to v3.0.1 for FOF problems
  0 new abstract problems.
  0 new problems.
  0 new generators.
  3 bugfixes done, in the domains SYN.
  0 ratings changed.
Changes from v3.0.0 to v3.0.1 for CNF problems
  0 new abstract problems.
  0 new problems.
  0 new generators.
  0 bugfixes done.
  0 ratings changed.

+ In tptp2X:
  - Fixed shortening of $false and $true
  - Fixed output of $false and $true in various formats

+ In SyntaxBNF:
  - Removed HTML formatting
  - Replaced reference to <parent source> by <source>
  - Replaced <logic formula> by <fol formula>
-------------------------------------------------------------------------------
Release v3.0.0, Thu Nov 11 12:55:48 EST 2004
 
Changes from v2.7.0 to v3.0.0 for FOF problems
  0 new abstract problems.
  0 new problems.
  0 new generators.
 53 bugfixes done, in the domains AGT SYN.
  0 ratings changed.
Changes from v2.7.0 to v3.0.0 for CNF problems
  0 new abstract problems.
  0 new problems.
  0 new generators.
  1 bugfixes done, in the domains SWC.
  0 ratings changed.

+ The library has been translated to the new TPTP syntax (aka the TSTP syntax). 
  - The BNF for the new TPTP syntax has been added to the Documents directory.
  - Equality is now written in infix, using = and !=
  - CNF "conjecture"s have been changed to "negated_conjecture"
  - $true and $false are now reserved constants, and have been used as expected.
+ Equality is now assumed to be builtin, and all equality axioms have been 
  removed from all problems.
+ Problem status values have been updated to the SZS problem status ontology:
  - The ontology has been added to the Documents directory.
  - FOF problems with conjectures are one of: Theorem, CounterSatisfiable,
    Unknown, Open.
  - FOF problems without conjectures are one of: Unsatisfiable, Satisfiable,
    Unknown, Open.
  - CNF problems are one of: Unsatisfiable, Satisfiable, Unknown, Open.
+ tptp1T has been updated to understand the new status values.
+ No numbers appear in any problems - numbers are now reserved for future 
  builtin treatment.
+ The tptp2X utility has been extended and improved :
  - The new TPTP syntax (aka the TSTP syntax) is the default output format
  - The old TPTP syntax is available as the oldtptp format
  - rm_equality with no selection removes all
  - add_equality has been parameterized like rm_equality
  - New set_equality transform 
  - New prefix format 
  - FOF files with multiple conjecture formulae are expanded to multiple
    files each with a single conjecture and all the other formulae.
  - Searches for include files:
    - No search for absolute names
    - Relative names are searched for under the $TPTP environment variable
      and if not found then under the current working directory
  - Explicit support for YAP Prolog
  - Installation is done by editing the *.uninstalled files and creating
    the final files. This solves some CVS problems.
-------------------------------------------------------------------------------
Release v2.7.0, Sun Aug 15 10:46:43 EDT 2004
 
Changes from v2.6.0 to v2.7.0 for FOF problems
222 new abstract problems, in the domains AGT ALG.
248 new problems, in the domains AGT ALG.
  0 new generators.
  5 bugfixes done, in the domains SET.
1121 ratings changed

Changes from v2.6.0 to v2.7.0 for CNF problems
 31 new abstract problems, in the domains ALG COL COM GEO PUZ SET SWV SYN.
 51 new problems, in the domains ALG COL COM GEO HWV PUZ SET SWV SYN.
  0 new generators.
 65 bugfixes done, in the domains FLD GRP HWV.
2888 ratings changed

+ One new domain has been added:
  - AGT (Agents)
+ The tptp2X utility has been extended and improved :
  - New formats omdoc, mace4, math
-------------------------------------------------------------------------------
Release v2.6.0, Wed Aug 20 22:22:22 EST 2003
 
Changes from v2.5.0 to v2.6.0 for FOF problems
  6 new abstract problems, in the domains HAL.
  9 new problems, in the domains HAL.
  0 new generators.
  0 bugfixes done.
786 ratings changed.

Changes from v2.5.0 to v2.6.0 for CNF problems
292 new abstract problems, in the domains BOO COL GRP LAT PUZ.
293 new problems, in the domains BOO COL GRP LAT PUZ.
  0 new generators.
 21 bugfixes done.
2932 ratings changed.

+ One new domain has been added: 
  - HAL (Homological Algebra)
+ The tptp2X utility has been extended and improved :
  - New formats tstp, carine
  - New options for old formats finder, otter, sem
  - Selective include directives allow inclusion of named formulae
-------------------------------------------------------------------------------
Release v2.5.0, Sun Jul 28 00:14:00 EST 2002
 
Changes from v2.4.1 to v2.5.0 for FOF problems
 29 new abstract problems, in the domains GEO GRP LCL MGT PLA PUZ SET SWC SYN.
 29 new problems, in the domains GEO GRP LCL MGT PLA PUZ SET SWC SYN.
  0 new generators.
  5 bugfixes done, in the domains PLA.
854 ratings changed.

Changes from v2.4.1 to v2.5.0 for CNF problems
697 new abstract problems, in the domains ALG ANA BOO CAT COL GEO GRP HEN 
    HWC HWV LAT LCL MGT NUM PLA PUZ RNG ROB SET SWC SWV SYN.
763 new problems, in the domains ALG ANA BOO CAT COL GEO GRP HEN HWC HWV 
    LAT LCL MGT NUM PLA PUZ RNG ROB SET SWC SWV SYN.
  0 new generators.
 18 bugfixes done, in the domains ALG GEO LAT SYN.
2620 ratings changed.

+ A subdirectory Documents/VerySimilarProblemLists has been added, with
  files containing names of problems that are "very similar".
+ The tptp2X utility has been extended and improved:
  - Upgraded for Eclipse 5.X
  - Explicit support for SWI Prolog
  - A -l option has been added, to specify the name of a file containing 
    the names of the files to be manipulated.
-------------------------------------------------------------------------------
Release v2.4.1, Sun Jun 24 16:33:23 EST 2001
 
Changes from v2.3.0 to v2.4.0 for FOF problems
792 new abstract problems, in the domains GEO MGT NLP PLA SWC SWV.
792 new problems, in the domains GEO MGT NLP PLA SWC SWV.
  0 new generators.
  0 bugfixes done.
1216 ratings changed

Changes from v2.3.0 to v2.4.0 for CNF problems
806 new abstract problems, in the domains GEO GRP LAT LCL MGT NLP PUZ SWC SWV.
860 new problems, in the domains GEO GRP LAT LCL MGT NLP PUZ SWC SWV.
  0 new generators.
  2 bugfixes done, in the domains LCL RNG.
1939 ratings changed

+ There have been some domain name changes:
  - PRV (Program Verification) renamed to SWV (Software Verification)
  - CID (Circuit Design) renamed to HWC (Hardware Creation)
  - CIV (Circuit Verification) renamed to HWV ((Hardware Verification)
+ Two new domains have been added: 
  - NLP (Natural Language Processing)
  - SWC (Software Creation)
+ The tptp2X utility has been extended and improved :
  - New transform propify for CNF problems, which converts 1st order problems
    with a finite Herbrand Universe into propositional problems, preserving
    satisfiability.
+ v2.4.0 was an internal released used for CASC-JC. The only difference is
  that v2.4.1 contains one extra bugfix, in LCL206-3.
-------------------------------------------------------------------------------
Release v2.3.0, Tue Nov 16 08:18:25 EST 1999
 
Changes from v2.2.1 to v2.3.0 for FOF problems
  1 new abstract problems, in the domains LCL.
  1 new problems, in the domains LCL.
  0 new generators.
  3 bugfixes done, in the domains SYN.
  4 ratings changed.

Changes from v2.2.1 to v2.3.0 for CNF problems
151 new abstract problems, in the domains GRP LCL PUZ SYN.
232 new problems, in the domains GRP LCL PUZ SYN.
  0 new generators.
 80 bugfixes done, in the domains COL GRP LCL RNG.
450 ratings changed.

+ The tptp2X utility has been extended and improved :
  - Five new CNF output formats: CoDe, Dedam, Satchmo, SCOTT, SEM
+ All problem ratings are now based on performance data from at least three 
  systems.
-------------------------------------------------------------------------------
Release v2.2.1, Thu May 13 08:50:59 EST 1999
 
Changes from v2.2.0 to v2.2.1 for FOF problems
  0 new abstract problems.
  0 new problems.
  0 new generators.
 58 bugfixes done, in the domains SET.
 59 ratings changed

Changes from v2.2.0 to v2.2.1 for CNF problems
  0 new abstract problems.
  0 new problems.
  0 new generators.
  3 bugfixes done, in the domains LAT.
617 ratings changed

+ This release is a patch, to be used in CASC-16
-------------------------------------------------------------------------------
Release v2.2.0, Thu Feb 11 10:54:02 EST 1999
 
Changes from v2.1.0 to v2.2.0 for FOF problems
208 new abstract problems, in the domains SET SYN.
323 new problems, in the domains PUZ SET SYN.
  0 new generators.
  1 bugfixes done, in the domains COM.
384 ratings changed.

Changes from v2.1.0 to v2.2.0 for CNF problems
 57 new abstract problems, in the domains ALG BOO GRP LAT.
 58 new problems, in the domains ALG BOO GRP LAT.
  0 new generators.
  4 bugfixes done, in the domains BOO CIV SET.
1108 ratings changed.

+ Two new reserved constants, true and false, are used in FOF problems.
+ The tptp2X utility has been extended and improved :
  - One new CNF output format: Bliksem
  - One new FOF output format: KIF
  - The Otter format module has been extended to translate true to $T and false
    to $F. The Otter format module now includes set(tptp_eq) by default.
  - The PTTP format module now selects a negative conjecture as top clause, if
    possible.
  - The FOF to CNF transformations in transform.clausify remove the constants
    true and false.
  - The stdfof transformation has been added transform.clausify. It removes 
    <=, <~>, ~|, and ~& from FOF problems, by rewriting formulae to use the 
    other connectives.
  - Input file names no longer have to be in TPTP format, except that generator
    files must have a .g extension.
+ The tptp1T utility has been extended and improved.
-------------------------------------------------------------------------------
Release v2.1.0, Wed Dec 17 13:41:02 EST 1997
+ This is the seventh public release.
+ This release is available from only Australia.
 
Changes from v2.0.0 to v2.1.0 for FOF problems
130 new abstract problems, in the domains SYN.
130 new problems, in the domains SYN.
  0 new generators.
  1 bugfixes done, in the domains SYN.
132 ratings changed.

Changes from v2.0.0 to v2.1.0 for CNF problems
134 new abstract problems, in the domains CIV SYN.
163 new problems, in the domains CIV COL SYN.
  0 new generators.
1172 bugfixes done, in the domains ALG FLD NUM SET (Most of these are due to 
    Johan Belinfante finding a typo in the SET004-0.ax file, subsequent to a 
    discussion we had regarding his AAR newsletter articles.).
2321 ratings changed, 0.03 average over 901 known changes.

+ The problem ratings have been updated. (Due to an improvement in the way
  the ratings are calculated, some problems now appear harder than before.)
+ The specific sizes of generic problems included in the TPTP have been 
  reviewed. Non-theorem as well as theorem sizes are now also included in the 
  problem set.
+ The tptp2X utility has been extended and improved :
  - Three new CNF output formats: FINDER, PROTEIN, Waldmeister.
  - One new FOF output format: THINKER.
  - Installation has been refined to select which output formats are required.
    Those not required are not loaded at runtime.
  - The "er" and "ran_er" transformations now reverse the arguments of equality
    literals in all types of problems (not only unit equality problems).
+ tptp1T arguments can now be negated with a leading "-". As a result some
  previously possible argument values are not needed, and have been disabled.
+ A BibTeX file containing entries for all material referenced in the TPTP has
  been added to the Documents directory. The % Refs entries in problem, axiom,
  and generator files have been reduced to a single line that includes a key
  for the bibliography file.
+ The TPTP technical report has been updated.
===============================================================================
Release v2.0.0, Thu Jun 5 15:06:26 EST 1997

v2.0.0 is the second version of the TPTP. The major changes in this version
are :
+ FOF (First Order Form) problems have been added.
+ Three new domains have been added: FLD (Field theory), KRS (Knowledge
  Representation), and MGT (Management).
+ Difficulty ratings have been assigned to those problems for which sufficient
  performance data from state-of-the-art ATP systems is available. The ratings
  are given in a new % Rating field in the problem headers.
+ A new utility called tptp1T, for finding problems with certain user specified
  characteristics, has been added.

Other changes are given below.
===============================================================================
Changes from v1.2.1 to v2.0.0 for FOF problems
110 new abstract problems, in the domains COM GRP LCL MGT MSC PUZ SET SYN.
217 new problems, in the domains COM GRP LCL MGT MSC PUZ SET SYN.
  1 new generators.
  0 bugfixes done.

Changes from v1.2.1 to v2.0.0 for CNF problems
120 new abstract problems, in the domains FLD KRS LCL PUZ.
309 new problems, in the domains FLD KRS LCL PUZ.
  1 new generators, in the domains PUZ.
  3 bugfixes done, in the domains GRP SYN.

+ This is the sixth public release.
+ The % Version fields have been reviewed. Problems that are "Special" have
  been explicitly labelled as such.
+ The % Syntax field of CNF problems has been extended to include the average
  number of literals per clause and the average term depth.
+ The tptp2X utility has been extended and improved :
  - Four new CNF output formats: CLIN-S, DFG, DIMACS, ILF.
  - Four FOF output formats: TPTP, DFG, Otter, OSCAR.
  - Nine new transformations: clausify (4 FOF to CNF transformations), simplify
    (simplifies a set of clauses), cnf (clausify then simplify), er (reverses
    arguments in the clauses of unit equality problems), ran_er (does the er 
    transformation to randomly selected clauses).
  - The format modules now receive an extra argument containing the file
    header information. This information may be used only for supplementary
    documentation of the problem.
+ The TPTP technical report has been updated.
===============================================================================
Release v1.2.1, Wed Jun 12 08:53:00 MET DST 1996

Changes from v1.2.0 to v1.2.1
0 new abstract problems.
0 new problems.
233 bugfixes done, in the domains BOO GEO GRP HEN NUM PUZ RNG SET SYN.

+ This is the fifth public release, and will be used in the CADE-13 ATP System
  Competition.
+ If the axiomatization used in a problem has been formed by reducing and
  augmenting an existing axiomatization, and the result is complete but also
  non-standard due to redundancy, this is noted with "(Non-standard)" in the
  % Version field.
+ The % Syntax field has been extended to include counts of range restricted
  clauses, and the arity ranges of the predicate and function symbols.
+ The tptp2X utility has been extended and improved :
  - One new output format: SPASS.
  - Two new transformations: to_equality and add_equality.
  - The equality removal transformation has been renamed to rm_equality, and
    now fails if the equality axiomatization is incomplete.
  - The shorten transformation no longer shortens equal to eq (i.e., equal/2
    always remains as the equality predicate).
+ In problems where the equality axiomatization was incomplete, the equal/2
  predicate has been renamed to equalish/2.
+ The clause type information has been reviewed and four corrections were made.
  Throughout the TPTP the "theorem" type has been replaced by "conjecture".
-------------------------------------------------------------------------------
Release v1.2.0, Wed Aug 30 08:03:11 +1000 1995

Changes from v1.1.3 to v1.2.0
245 new abstract problems, in the domains BOO COL GRP SYN.
267 new problems, in the domains BOO COL GRP MSC PUZ ROB SYN.
49 bugfixes done, in the domains COL LCL PUZ ROB SYN.

+ This is the fourth public release.
+ Generic problems (e.g., the N-queens problem) are now handled by problem
  generators:
  - This allows the automatic generation of any desired problem size.
  - For each generic problem, a particular size is in the problem set.
  - 159 problem sizes previously in the problem set have been removed.
+ The % Syntax field has been reordered in all files.
+ The tptp2X utility has been extended and improved in various ways :
  - Installation and use of tptp2X have been simplified.
  - tptp2X now updates the % Syntax field after transformations.
  - There are three new output formats: 3TAP, KIF, and leanTAP.
  - Problem generation has been integrated into tptp2X.
  - The syntax for specifying equality axiom removal has changed.
  - The syntax for specifying OTTER format output has changed.
+ The TPTP technical report has been substantially revised.
-------------------------------------------------------------------------------
Release v1.1.3, Thu Aug 25 08:53:57 +1000 1994

Changes from v1.1.2 to v1.1.3
1 bugfixes done, in the domains PUZ.

+ This is the third public release.
+ Some more changes done to the tptp2X utility and tptp_convert
-------------------------------------------------------------------------------
Release v1.1.2, Fri Aug 12 09:04:47 +1000 1994

Changes from v1.1.1 to v1.1.2
1 bugfixes done, in the domains PUZ.

+ This is an intermediate non-official release.
+ The tptp2X utility was broken in v1.1.1. That's been fixed, and is the
  motivation for this release.
+ The tptp_convert script has been improved substantially.
-------------------------------------------------------------------------------
Release v1.1.1, Tue Jul 5 05:14:27 +1000 1994

Changes from v1.1.0 to v1.1.1
3 bugfixes done, in the domains CID LCL.

+ This is the second public release.
+ Problems SYN04[23]-1 noted to be versions of LCL181 and LCL230. SYN04[23]-1
  have therefore been moved to LCL181-2 and LCL230-2.
-------------------------------------------------------------------------------
Release v1.1.0, Fri Apr 8 12:12:45 +1000 1994

Changes from v1.0.0 to v1.1.0
357 new problems (320 new abstract problems), in the domains ANA BOO CID CIV
    COM GEO GRP LAT LCL NUM PLA PUZ SYN.
736 bugfixes done, in the domains ALG ANA BOO COM GEO GRP NUM PUZ SET.

+ This version has been released to registered TPTP users only.
+ Some critical bugfixes have been done.
+ Two new domains have been introduced : CID = Circuit design
                                     and CIV = Circuit verification
  both in the field of Engineering.
+ The tptp2X utility has been substantially overhauled. The utility can now
  apply a sequence of transformations to clauses, and installation has been
  simplified. See the tptp2X ReadMe file for details.
+ A list of known users is included in the Documents directory.
+ The TPTP release and the release of the last bugfix are now given in the
  % File field of each problem and axiom set.
-------------------------------------------------------------------------------
Release v1.0.0, Fri Nov 12 15:30:54 +1000 1993

+ This is the first public release.
-------------------------------------------------------------------------------
