This history describes the major differences between versions of the E
equational theorem prover.

Version 3.1.0 -> 3.2.X Puttabong Moondrop

- Added support for $distinct
- Disabled -xAuto and cut out most of the relics of the old auto-mode
  stuff
- Added option to select one of the built-in strategies
- Took out old clausifier
- Updated several options
- Debugged some higher-order problems

Version 3.0.03 -> 3.1.0

- Added disequality decomposition inference
- Fixed various bugs (e.g. in local rewriting)
- Added support for additional statistics
- Enabled printout of all built-in search strategies


Version 3.0 ->3.0.03 Shangri-La

- Fixed bug in activating clause selection heuristics
- Fixed several bugs in the higher-order module, mostly related to the
  difference between shared and unshared terms. This will need further
  work to catch all corner cases.
- Fixed several minor memory leaks and simplified management of parsed
  strings with the clb_permastrings module.

Version 3.0 (pre-release) ->3.0 Shangri-La

- Fixed various bugs in the HO preprocessor
- Fixed various bugs in the HO reasoner
- Improved the multicore scheduler

Version 2.6 ->3.0 Shangri-La (pe-release)

- New option --fw-subsumption-aggressive.
- Fixed bug in negative unit subsumption.
- Added new DAG-based evaluation functions
- Fixed status for incomplete literal weight functions
- Added support for UTF-8 in Strings and single-quoted symbols.
- Added multicore scheduler and schedule generation
- Replaced auto-mode code by new symbolic auto-mode
- Various minor improvements
- Added support for full (monomorphic) higher-order reasoning (PV)


Version 2.5 -> 2.6 Floral Guranse

- Much improved algorithm for finding maximal literals in long clauses
- Much improved algorithm for identifying dual (conflicting) literals
  in long clauses
- Added max literal limit for full equational tautology check (we
  should now really replace that with a congruence closure based
  approach!)
- Added DAGWeight() evaluation function (symbol-counts shared terms
  only once, with different options for sharing regions (terms,
  literals, clauses)
- Improved support for THF: E can now parse most of TH0 syntax
- (notable exceptions are symbols !!, ?? and @+), including lambdas.
  Note that on the reasoning side, E still does not support any
  advanced lambda reasoning, as lambdas are simply lifted and after
  parsing E is not aware of them.
- Improved support for TFX: E now supports $let and $ite expressions.



Version 2.4 -> 2.5 Avongrove

- Clausal problems are now classified before equational definitions
  expansion, which moves equational definition expansion under control
  auf the automatic modes)
- Strong rewrite (optionally instantiating unbound variables of the
  right hand side of equations considered for rewriting) has neem
  fixed and updeted to the sorted case.
- An improvement in strategy scheduling will now aovid repetition of
  the same strategy in cases where the data does not change from one
  level to the next, allowing for meaningful deeper schedules.
- New automatic modes
- Added variants to symbol precedence schemes (prefer/defer
  skolems/defined symbols/axiom-symbols/conjecture symbols).


Version 2.3 -> 2.4 Sandakphu

- Added random clause "evaluation"
- Added Diversity-based clause evaluation
- Added (simplified) transfinite orderings for literal comparision
- New automatic modes
- Support for CASC-27 LTB (with various alternative formalisations per
  problem)
- Slightly finer classificarion of problems (for improved UEQ
  performance)

Version 2.3pre -> 2.3 Gielle

- Made clausification more robust for extreme examples

Version 2.2 -> 2.3pre Gielle

- Merged support for lambda-free higher-order logic.
- Improved fingerprint indexing by excluding one more subcase for
  finding instances

Version 2.1 -> 2.2 Thurbo Moonlight

- Prover now always builds internal proof object (--proof-object only
  controls output)
- As a result, E can now detect ContradictoryAxioms if the proof state
  is unsatisfiable even without the conjecture.
- Moved from eager to lazy orphan deletion. If you don't know what
  this means: It's much cooler and simpler.
- Fixed and simplified processing of unprocessed clauses
- Refactored PicoSAT integration - PicoSAT is now linked into E
  proper, and used via its API. We are back to a single binary
  executable with no dependencies.
- Prover now enforces that fof, tff and tcf formulas are closed (no
  free variables allowed)
- Fixed condensation (somewhat).
- New automatic modes (but with very few current test results)


Version 2.0 -> 2.1 Maharani Hills

- Added type output for CNFed TFFs
- Added tcf sublanguage for clause-form TFFs
- Combined consecutive applications of the same quantifier into a
  single quantifier
- Improved stability and performance on TFF problems
- Changed internal workflow of unprocessed clauses so that they can be
  batch-evaluated (e.g. by a Deep Neural Network).
- Added PicoSAT and the ability to use PicoSAT as a SAT terminator
- Added support for flexible-arity derivation operations
- Removed obsolete eproof-scripts. Use --proof-object to generate a
  checkable proof.

Version 1.9.1 -> 2.0 Turzum

- Support for TFF (typed first-order form), thanks to Simon Cruanes
- Improved clausification (faster, with graceful degradation if
  miniscoping becomes too expensive)
- Improved auto-modes
- Improved Set-of-Support simulation
- Parsing and pruning preprocessing FOF now, even for CNF input
- Input clauses/formulas keep their original name (if any)
- Added options  --generated-limit and --tb-insert-limit to more
  closely limit effort by the prover in a deterministic way.

Version 1.9 -> 1.9.1 Sungma

- Improved proof object output
- Added optional recording of selected given clauses in the proof
  object
- New auto modes (including one bred heuristic)
- Fixed bug in formula simplification involving P=><=>$false
- Added given clause recording and training example generation
- Various cleanups and additional compile time warnings
- More detailed proof graphs
- Automatic determination of input format if no format is
  specified. If input format is determined as TPTP-3, output format is
  automatically set to TPTP-3/TSTP, too.
- Various fixes to watchlist code. Again. And again. If you use this
  feature and have been using a pre-release, you want to upgrade!


Version 1.9pre016 -> 1.9 Sourenee

- Fixed Auto-SInE to never SInE if there is no seed to SInE on
- Added output of proof graphs in GraphViz/dot format (coloured, too!)
- Added derivation output for CNFization
- Fixed minor bug in proof output


Version 1.8 -> 1.9pre016

- Fixed bug that caused proof output to fail in rare cases when the
  proof was found in preprocessing.
- Took out "theory(equality)" from TSTP-output, since FOL-EQ is now
  assumed the default logic.
- Improved proof objects (taking out empty "quote" steps).
- Added plenty of new literal selection functions.
- Updated auto-modes


Version 1.7 -> 1.8 Gopaldhara

- Added support for internal proof objects (and option --proof-object)
- Added experimental support for strategy scheduling (--auto-schedule)
- Minor cleanup and improved auto-mode(s)

Version 1.6 -> 1.7 Jun Chiabari

- Added prototypical condensing
- Significantly improved auto-mode (note that AutoDev mode is, at the
  moment, intentionally inferior to normal auto mode - use only if you
  want to compare the effect of inferior ordering implementations!)
- Fixed non-critical (but annoying) bug in SOS strategies
- Updated eground to support FOF input (if it clausifies to EPR) and
  to handle unexpected behaviour from MiniSAT
- Added interactive batch mode to e_ltb_runner (load large spec once,
  then keep asking for the status of different theorems via
  stdin/stdout)
- Added enormalize for normalization of terms, clauses and formulas
  with an oriented rule set without regard for orderings.
- Various minor updates and bugfixes

Version 1.5 -> 1.6 Tiger Hill

- Incorporated minor improvements to the scripts suggested by Jasmin
  Blanchette
- Added support for "Shell" PCL (a more compact form that only records
  the dependency graph, but not the actual clauses for intermediate
  results)
- Added SInE-axiom filtering and automatic mode for SInE.
- Much better heuristics and new auto mode(s)
- Even better AutoDev-Mode (use at your own risk ;-)
- More convenient command line interface:
  "eprover --auto" will be good for most people.
- Updated manual

Version 1.4 -> 1.5 Pussimbing

- Fixed bug stopping miniscoping from ever being used
- Implemented non-perfect discrimination tree indexing (mostly for
  comparison with FP indexing)
- Fixed indexed paramodulation (no more inefficient top-level overlaps
  of non-equational literals)
- Added further instrumentation for profiling
- Implemented (prototypically) folded feature vector indexing and made
  it the default
- Fixed Makefiles to cleanly work with more modern gcc versions
- Some more executables are now installed as part of the standard
  installation.
- New auto mode


Version 1.3 -> 1.4 Namring

- Adapted e_ltb_runner for CASC-23
- Various minor fixes, in particular to proof and answer output
- New literal selection function
- New auto-modec

Version 1.2 -> 1.3 Ringtong

- Fixed redundant output resulting in broken proof extraction.
- Fixed sub-optimal CNFing (slow, not incorrect)
- Implemented e_axfilter as a stand-alone program for pre-processing
  large problems, and adapted/extended the corresponging libraries.
- Added clause evaluation functions that allow the manipulation of the
  weight based on the pre-sence and frequency of invidual function
  symbols.
- Added answer instantiation output.

Version 1.1 -> 1.2 Badamtam

- Made stack limit increase fail gracefully (run with default)
- Fixed (most) problems with C stream output and signals. The core
  prover should be clean now.
- Cleaned up variable handling and got rid of the ugly second term
  bank for the given clause
- Implemented Bernd Loechner's linear time version of KBO (JAR
  36(4):289-310, 2006).
- Fixed a serious bug with mixed CNF/FOF input (now it works,
  previously it did not).
- Implemented fingerprint indexing for paramodulation/superposition
  and backwards rewriting.
- Implemented e_ltb_runner for CASC-J5. Probably not generally useful,
  but comes with extended SinE-like functionality that will be used in
  the main prover eventually.

Version 1.0 -> 1.1 Balasun

- Added --help output to eproof
- Improved eproof script signal handling.
- Fixed automatic memory determination bug on large-memory Macs.
- Fixed a number of warnings with the latest gcc version.
- Updated proof objects to latest SZS ontology.
- Removed some C99-style comments that bothered ancient compilers
- Improves TPTP-3/TSTP output (fof sometimes used prefix equal, not
  infix =).
- Fixed bug in the output of symbols with an embedded %.
- Added man pages for the major binaries
- Added various goal-directed heuristics
- Improved pre-processing (cut-off-limit for eq-def-expansion)
- Better auto-mode
- Optional pre-saturation simplificaton


Version 0.999-004->1.0 Temi

- Removed old style formulas and CNF algorithm.
- Fixed a number of bugs in backwards rewriting.
- Made parser more compliant to TPTP 3.5.0 (stricter checking of
  formula roles)
- New GNU-like build and installation system
- Fixed one completeness bug in CNF, fixed two serious performance
  bugs for very large formula CNFization.
- Removed dependency on bash (only POSIX Bourne Shell required, I
  hope)

Version 0.999 -> 0.999-004

- Fixed string overflow bug sometimes corrupting auto mode
  classification (Thanks to Josef Urban for finding it)
- Fixed illegal memory access in term formula building
  (Thanks to Josef Urban for pointing it out).
- Updated TPTP-3 parser.
- Cleanup of eproof script (thanks to Larry Paulson for bugging me
  over and over again).

Version 0.99 -> 0.999 Longview

- Finally got to eliminate the ugly duplicate term cells for terms
  with rewrite restrictions. This lead to a rather simpler term bank
  structure, too.
- Added better syntactic support for integers and floats.
- Removed old '--interprete-numbers' option and associated dead code.
- Fixed (hopefully) the learning module, which had suffered from bit
  rot. It works now, although it ignores FOF axioms for similarity
  measures. This does not affect the default heuristics.
- Made some minor changes to SZS output to make Geoff happy.
- Fixed some bugs in the eproof script to make Larry happy.


Version 0.91 -> 0.99 Singtom

- Introduced new and (maybe) better clause evaluation data type.
- Updated install scripts to handle OSes with UCB tail.
- Found (and fixed) mismatch between split handling and split
  documentation (argh!).
- New splitting via (reusable) definitions introduced and tested.
- Spell-checked manual and (prover) help output.
- Better Auto-Mode
- Some cleanup.

Version 0.9 -> 0.91 Kanyam


- Alternative CNF translator with configurable renaming finally done
  (still needs more testing) (use option --definitional-cnf)
- More goal-directed heuristics, and better evaluation of same
- Fixed classification bug in auto mode
- Result: Better auto-mode
- Added option --order-weights for user-defined KBO
- Fixed and updated a number of tools, all of which should now work
  with full FOF format
- Fixed TSTP parser to conform to new parenthesizing/precedence
  handling.

Version 0.82 -> 0.9 Soom

- Small improvement in unification
- Reworked parser
- Rebuild indexing data structures with IntMaps (should be much more
  memory efficient for large signatures)
- Added preliminary support for distinct objects and numbers (only
  ground case so far)
- Added support for stronger rewriting (instantiating unbound
  variables in potential right hand sides)
- Implemented TPTP style includes for TPTP/TSTP syntax
- Made groundness a stored invariant in term banks (enables more
  efficient inserting of gorund terms, also helps with literal
  selection).
- Reworked the watchlist (needs more work).
- Reworked subsumption by ordering clauses (still need to look at the
  effect this has on search).
- Got rid of ancient options restricting paramodulation (dating back
  to METOP, and never used)
- Modified/rewrote some literal selection functions, taking the AHP
  (Avoid Head Predicates) property into account (solves some of the
  interference of the new literal order with heuristic search)
- Added simultaneous paramodulation (very useful)
- Added goal-directed heuristics.
- New auto-mode taking some of the new features into account.
- Cleaned up output (--tptp3-out will now also work for output levels
  <=2 and for final clause sets).
- Removed old Auto071 mode (it did not work well with the new
  internals anyways) and added AutoCASC mode (corresponding to E
  0.9pre003 as used in CASC-20).

Version 0.81 -> 0.82 Lung Ching

- Fixed a bug in find_spec_literal() pointed out by Flavio
  Ribeira. Might improve performance for large problems with a lot of
  subsumption.
- Added LPO4 variant from Bernd Loechners paper. Much faster
- Cleanup of feature stuff (needs more cleaning)
- Added support for full first-order logic and clausification
- Optimized automatic mode and fixed some ancient automatic mode bugs

Version 0.8 -> 0.81 Tumsong

- Fixed the SOS propagation bug in splitting.
- Overhauled feature vector indexing and added a lot of bells and
  whistles
- Added support for the watch list and watch list based heuristics
- Added support for multiple auto modes, including the 0.71 auto mode
- (-xAuto071 -tAuto071), the current one, and a developer auto mode
  (-xAutoDev -tAutoDev, the last two are identical for official
  release versions, but allow experiments while keeping behavior
  stable for in-between versions).
- Much improved automatic mode (knows more about contextual literal
  cutting and SOS now)
- Improved support for TSTP input and full TSTP output
- Added some things to the manual. Yes, really!

Version 0.71 -> 0.8 Steinthal

- Finally fixed that SOS bug. There still is an SOS problem with
  splitting (split clauses do not inherit SOS status) that will be
  fixed for the next release
- Added PrioFunDeferSOS
- Changed the order of arguments of PCL expression for paramod
  inferences (seen as a conditional lazy speculative rewrite step now
  is consistent, i.e. the second one is being applied to an instance
  of the first one).
- Changed the main loop to a more conservative version (_all_
  simplified clauses are scheduled for reprocessing) giving a much
  nicer invariant
- Added Defaultweight() and a number of evaluation- and priority
  functions to improve FIFO (ByDerivationDate, StaggeredWeight(),
  ...)
- Added feature vector indexing for non-unit subsumption
- Added contextual simplify-reflect (may change that name - what about
  contextual equational literal cutting?)
- New auto mode, still mostly based on pre-subsumption-indexing test
  runs
- Added epcllemma program that will use various heuristics to suggest
  lemmata in PCL protocols.

Version 0.7 -> 0.71 Puttabong

- Added preprocessing of clause sets: Demodulation to get rid of fully
  defined function symbols, tautology elemination, sorting of clauses
- Fixed some bugs, including a bug in subsumption.
- Made function symbol ordering more stable by adding more and better
  secondary criteria (number of occurences in formula...)
- Ported to MacOS X, fixed some small portability problems
- Fixed bug in compressed PCL output (output of inital clauses came
  from a different term bank, yielding wrong abbreviations)
- Fixed bug in eground (number of clauses in printed DIMACS format was
  potentially different from stored number of clauses)
- Added new and better term ordering schemes and literal selection
  functions.
- Added new weight functions and priority functions to get a better
  grip on FIFO.
- New and better auto-mode (surprise ;-)
- Modified the prover to make it run consistently on different
  architectures. Compile with CONSTANT_MEM_ESTIMATE to get the most
  from this (see Makefile.vars for documentation).
- Added putative TSTP exit status (as a compile time option, on by
  default).

Version 0.63 --> 0.7 Dhajea

+ Changed rewriting implementation from destructive global to cached
  global.
+ Changed memory estimator, all limit-based options now use
  (estimated) bytes as memory units.
+ New literal selection functions, in particular those avoiding type
  literals
+ Rewrote and simplified splitting, added aggressive splitting
  (splitting of unprocessed clauses)
+ Added aggressive equality resolution
+ Added optional unit cutting with unprocessed clauses
+ New and improved automatic mode
+ Fixed a bug with --prefer-initial-clauses. Now it works (and often
  is quite helpful)
+ Changed output format to native PCL2, optionally with compressed
  terms. Output level 4 will now print all real inference steps,
  output level 6 will also print given clause selection, evaluation
  steps, and subsumption. Implemented epclextract for proof object
  generation. Note that pattern-based learning now is temporarily
  broken.

  After CASC-18 prerelease:

+ Full virtualization of the core prover - it should now be possible
  to run several logically independent copies inside one process space
  (they still share some inference counters and output variables, but
  nothing that should affect proof search).
+ Added improved SoS support. You can now specify the SoS by using
  --sos-uses-input-types and choosing TPTP clause type conjecture or
  E-LOP query format. Note that there still is a small bug in SoS
  implementation -- non-SoS clauses simplified with a SoS clause do
  not enter SoS, but probably should. Since we only simulate SoS
  anyways, this bug does not lead to a hard incompleteness (but
  possibly to infinite runs for unsatisfiable problems). It will
  (hopefully) be fixed for the next release.
+ Worked on the manual. It is still very incomplete.


Version 0.62 --> 0.63 Nuwara Eliya

+ Added explicit code for the occur-check (shoud be faster than the
  general TermIsSubTerm())
+ Improved interreduction and 1-1-matching (should also help for
  Subsumption)
+ Added hooks and code to generate a version with proprietary
  extensions (under a separate license)
+ Added SymbolTypeweight heuristic (assigns different weight to
  non-constant function symbols, constants, predicates, and
  variables).
+ Addded support for HPUX again.
+ Added some new literal selection functions.
+ Implemented epclanalyse to easily determine certain properties of
  proofs.
+ Significantly improved eground, in particular by implementing
  non-ground splitting (and several pure performance hacks)
+ New Automatic mode for unit problems (non-Units still use old
  auto-mode, which probably is sub-optimal with the new calculus
  refinements)


Version 0.61 --> 0.62 Mullootar

+ Added clause splitting (not yet very good)
+ Added PNweight clause weight, which assigns different values to
  symbols and variables in positive and negative literals
+ Added new features for auto mode (maximum function symnbol arity),
  very useful for UEQ
+ New auto mode
+ Implemented eground (grounds near-propositional proof problems)

Version 0.6 --> 0.61 North Tukvar

+ Added priority function PrioFunPreferNonEqUnits
+ Addded more literal selection functions
+ Added option --precedence to allow the user to select partial
  precedences for the term ordering
+ Added precedence-generation scheme "const_min", simplified some of
  the precedence code
+ Added Waldmeister-like AC handling (on by default), with options
  --ac-handling and --ac-non-aggressive (read their documentation to
  see what they do).
+ Updated proof analysis tools to deal with AC handling, fixed some
  other annoying things with them (SR was encoded as a generating
  rule).
+ Implemented NLweight clause weight, giving different weight to the
  first occurrence of a variable in a term and later (i.e. non-linear)
  ones.
+ Fixed bug in TSM-based weight functions (introduced by
  pseudo-optimizing me....aaargh!)
+ Modified frequency-based ordering generation - will now use arity as
  tie-breaker.
+ Added new weight generation schemes modarity and modaritymax0
+ Fixed some problems with evaluation comparisons on Intel Itanium
  systems (thanks to Compaqs Test Drive program for access to the
  hardware!) (in fact, did _not_ yet fix all of them...strange stuff
  happens!)
+ Added literal selection functions selecting literals based on
  orientability.
+ Rewrote term indexing - can now cope with growing signatures
+ Added M-literal-selection functions (select positive literals in
  Non-Horn clauses, not in Horn clauses)
+ Added --inherit-goal-pm-literals to inherit paramod-literals in
  goals only
+ New auto mode once more
+ Fixed minor bug in RR-literal selection functions

Version 0.6 (prerelease) --> 0.6 (Kanchanjangha)

+ Updated (some) documentation, in particular the help texts of the
  programs.
+ Overhauled the manual - it's still very incomplete, but at least not
  outrightly false anymore (I hope)
+ Several changes to the CSSCPA code in the EXTERNAL directory (does
  not affect main prover)

Version  0.51 --> 0.6 prerelease

+ Added various learning heuristics (but documentation is still
  missing)
+ Added new literal selection functions taking the ordering into
  account (and reorganized parts of the proof procedure to allow
  this).
+ Added relatively naive LPO cache
+ Reimplemented LPO for better performance - now faster without the
  cache
+ Added support for SOS strategy (with priority function SimulateSOS,
  does not seem to do very well at the moment)
+ Enabled soft- and hard cpu time limits simultanously.
+ Removed legacy option --paramod-strategy (use
  --literal-selection-strategy instead)
+ Added option --error-on-empty to allow the catching of certain
  errors in E-SETHEO
+ Implemented e2pcl, translating E output to UPCL2 language.
+ Implemented proof checker for UPCL2.
+ Eliminated option --no-pdt-indexing (and associated code)
+ Removed option --discount-vars and associated code (nobody used it
  anyways, and it lead to code bloat).
+ Changed option --memory-limit to require an argument.


Version 0.5 --> 0.51 (Mim)

+ Added more literal selection functions playing with
  range-restriction variations
+ Moved input format description to scanner object and generalized
  concept.
+ Moved signal handling from CONTROL.a to INOUT.a
+ Included handling for temorary files, abstracted some of the other
  file stuff
+ Removed a minor problem from rewriting (affected only proof analysis
  tools)
+ Fixed bugs in reproduction and analysis tools
+ Completed knowledge base management with ekb_create, ekb_ginsert and
  ekb_delete
+ Fixed nasty bug in implementation of SimplifyReflect
+ Added learning heuristics (prototypical)

Version 0.5 (prerelease) --> 0.5 (Phuguri)

+ Fixed a minor bug in clause weight precalculation
+ Added new literal selection function that does not select literals
  in range-restricted clauses.

Version 0.32 --> 0.5  (prerelease, this is the CASC-16-Version)

+ Added new weight functions and literal selection functions
+ Changed an off-by-one error in Saturate...if said to process 0
  clauses the prover will now stopp immediately instead of processing
  one clause.
+ Added syntax check after clause set has been read - will now
  complain about additional garbage.
+ Added option to restrict selection by clause weight and to perform
  selection only when processing, not when evaluating.
+ Improved Auto-mode again, based on lots of new test data.
+ Added another classification to classify_problem (Few, some or many
  positive ground clauses). Does not seem to help much.
+ Changed the auto-mode generation tool chain by cutting me and my
  stupid mistakes out of it. Only che_[HGU]*.c need to be modified now
  to change the auto mode, and generate_auto.awk will collect all
  necessary information.

Version 0.31a --> 0.32 (Lingia)

+ Added support to use the prover as a clause set normalizer
  (basically doing interreduction and subsumption).
+ Implemented stronger tautology detection (should now eliminate _all_
  tautologies. Does e.g. remove equality axioms). Thanks to Roberto
  Nieuwenhuis for the suggestion. Needs testing!
+ Removed obsolete option "--paramod-with-units-only", eliminated
  paramodulation strategies and replaced them with literal selection
  strategies (once more, thanks to Roberto for pointing out the
  relationship forcefully enough for me to believe in it
  ;-). "--paramod-strategy" remains for the moment for backward
  compatibility, but is mapped to set the corresponding selection
  strategy. Introduced option "--literal-selection-strategy".
+ Removed a bug (might have caused incompleteness) from detection of
  backward-rewritable clauses.
+ Changed output of result line. Thanks to the literal selection
  strategy, E will now never terminate with indeterminate result
  unless the calculus is restricted (and in this case it will say
  so).
+ Added more literal selection strategies and option --nogeneration.
+ Fixed bug in EqnListEqnIs[Strictly]Maximal().
+ Removed test for maximality of instantiated negative literals into
  which the prover paramodulates - it never yielded false anyways in
  practice.
+ Added output of the empty clause whenever --print-saturated is
  selected and the empty clause has been derived.
+ Added evaluations functions reminiscent of DISCOUNT's MaxWeight.
+ Added options to control selection (don't yet know if it helps)
+ Optimized non-unit subsumption and made all stack functions inline -
  not nice, but that helps a lot.
+ Made some more stuff inline and optimized matching
+ Updated automatic mode

Version 0.31 --> 0.31a (Jungpana II)

+ Fixed proofanalyse (prints dependency graph and selects clauses on
  and near to the proof path as examples) and generate_examples
  (generates external representations of selected clauses from the -l3
  or -l4 protocol
+ Improved auto-mode once more (only change to the main prover)

Version 0.3 --> 0.31 Jungpana

+ Added TPTP format parser and output routines.
+ Did some more hacks for evaluation.
+ Restructured EXAMPLE_PROBLEMS subdirectory (now has the
  non-obfuscated TPTP and LOP versions of the CASC-15 problems).
+ Ripped out AVL trees and plugged in Splay trees in
  clb_ptrees.c. Should save significant amounts of memory, definitly
  speeds things up. Also reduces code size seriously. I will probably
  replace some more AVL trees with Splay trees.
+ Did that: Term Trees and Evaluation Trees now also use Splay
  trees. The remaning AVL's should be cleaned up sometimes, but are
  definitly uncritical.
+ Made $true-term special, it will now no longer carry ext-ref
  information. Not nice, but saves time and lot's of memory (3 words +
  Overhead per non-equational literal).
+ Added options for intermediate filtering of unprocessed clauses,
  including deletion of (possibly) non-redundant clauses to keep
  memory consumption in check. The prover no works quite well with
  whatever memory is offered (but 10 MB is about a rational minimum
  for non-trivial problems, with 128 MB suggested).
+ Made all boolean options NoArg options (instead of options with
  optional argument).
+ Following a hint by Roberto Nieuwenhuis, implemented real
  PosUnit-Strategy. I'll have to learn to read sometime...
+ Added soft cpu limit.
+ Debugged filtering of unprocessed clauses...first time I ever had to
  deal with a long overflow (due to my stupidity, no doubt).
+ Fixed bugs with long option handling and auto-mode (introduced by
  the changes necessary to support multiple paramod-strategies)
+ Added filtering for clause copies.
+ Added removing of clauses in cases of tight memory
+ Added new weight functions (Sigweight, Proofweight)
+ Removed entry-index in term banks
+ Changed rewrite machinery to stop replaced term from being
  reinserted as super-terms
+ Brought depanalyze up to working state (it currently prints a
  dependency graph for clauses, including demodulators). As a side
  effect, the -l3 option should now work and really print a complete
  protocol.
+ Fixed a bug in Equality factoring (it allowed unification between
  variable and predicate term).
+ Improved Auto-Mode for heuristic selection, now optimized for
  standard term ordering (no need for -tAuto anymore).

Version 0.24 --> 0.3 "Castleton"

+ Tested signal handling under HPUX - works fine.
+ Added a simple auto-mode, changed WFCB interface and added
  WFCB-Administration for new heuristics-management.
+ BIG ONE: The command line semantics of the prover
  changed. Previously, "eprover p1 p2 p3" was equivalent to "eprover
  p1; eprover p2; eprover p3", but that did not make to much sense and
  complicated quite some things. Now it is equivalent to "cat p1 p2
  p3| eprover". This allows you to modularize your specifications to a
  certain degree.
+ Added HCB-Administration and interface, rewrote
  heuristics-code. Does now need user-level documentation badly!
+ Wrote some of this documentation ;-) See CLIB/DOC/eprover.tex
+ Added proof output (machine friendly only, will need tools to
  post-process).
+ Hacked a lot of scripts for test runs and evaluation.
+ Fixed an extremely stupid bug (4 times over) in precedence
  generation, fixed a lot of bugs in weight generation that were
  masked by this one. Removed TOGenerateDefaultWeights(), as it was
  redundant anyways. Moved TOGenerateDefaultPrecedence() to
  che_to_precgen.[ch], were it belongs.
+ Fixed incompleteness caused by too strong subsumption.
+ Added auto-mode for heuristic selection and ordering selection.

Version 0.23 --> 0.24 "Yunnan"

+ Fixed one more bug (subsumption of negative literals without
  recomputation of maximal literals)
+ Added simple signal handler to make --cpu-limit work on more
  platforms (should now work on all versions of Linux and Solaris,
  untested on other platforms).
+ Restructured part of the code, moved ProofState object deeper to
  allow clean coding of an auto-mode.
+ Variables do not have external references anymore -> saves time and
  space, and fixes half a bug.
+ Did some testing.
  "eprover -x Standard --memory-limit=192 --cpu-limit=300" on a SUN
  Ultra-10 Workstation should be able to solve about 1312 problems
  from the TPTP version 2.1.0.


Version 0.22 --> 0.23 "StopGap"

+ Fixed bugs in LiteralCompare() (main reason for new release)
+ Added paramodulation with maximal variable sides
  (makes the prover more complete ;-)
+ Wrote some simple precedence generation schemes for the orderings
+ Added unit-paramodulation strategy for Horn Clauses form
  [Der91]. Very strong except for the TPTP PLA domain.


Version 0.21 --> 0.22 "Risheehat"

+ Removed rewrite cruft (see last version change)
+ Unified term banks for processed and unprocessed clauses, optimized
  rewriting
+ Optimized unification
+ More verbose and more correct statistics
+ Removed a long-standing (but basically user-invisible) memory
  allocation bug from cto_ocb.c. Yes this is important (to me...)!
+ Optimized rewriting (again) with better use of normal form
  dates. Helps some, but not as much as I would have expected -
  perhaps a lingering bug?
+ Removed some more cruft, cleaned up term type
+ Simplified clause type.
+ Simplified equation type, replaced boolean properties with bit
  properties after profiling showed that shared terms are so efficient
  that clause and equation cells contribute significantly to memory
  consumption.
+ Implemented simple non-unit-subsumption. Prover now works in some
  fashion on non-unit problems (i.e. would not come in as last in
  CASC-15).
+ Did some more profiling on KBO and found out that new implementation
  does help -> it is now the default.
+ Implemented weight-generation schemes for KBO
+ Took variables out of the term trees in the term bank.
+ Implemented pre-hashing for term bank terms. Works great!
+ Changed default weight for terms and variables -> usually better
  performance. Currently, use -i1 -i1 for old default behaviour.
+ Decided to give cool names to releases.
+ Optimized rewriting once more...marginal improvements.

Version 0.2 --> 0.21

+ Rewrote rewrite machinery (still some cruft to remove) and
  simplified proof procedure
+ Added --version option for GNU's sake
+ Fixed still more serious (if seldom occuring) bugs
+ Added --memory-limit option (works only on systems with rational
  setrlimit())
+ Added second implementation of KBO (no improvement *sigh*)
+ Some cleanup

Version 0.1 --> 0.2

+ Improved indexing
+ Stronger unit-subsumption
+ Fixed lots of serious bugs
+ Improved KBO efficiency