-------------------------------------------------------------------------------
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. 
  Throughtout 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.
-------------------------------------------------------------------------------
