This history list describes the major differences between versions of the E equational theorem prover. 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