Download Archive

See the main download page for the current release!

E 3.0.03 Shangri-La (2023-11-26)

E 3.0 Shangri-La is the latest release of E. The main changes compared to E 2.6 are support for full higher order logic and much improved multicore-scheduling. This release is the cleaned up and debugged version of both the 3.0 and 3.1 pre-release versions that performed well in CASC-J11 and CASC-29 (with some additional extra work). Release 3.0.03 fixes additional bugs in the higher-order part, as well as a significant performance bug in the automatic modes.

E 3.0 Shangri-La (2023-11-15)

E 3.0 Shangri-La is the latest release of E. The main changes compared to E 2.6 are support for full higher order logic and much improved multicore-scheduling. This release is the cleaned up and debugged version of both the 3.0 and 3.1 pre-release versions that performed well in CASC-J11 and CASC-29 (with some additional extra work).

E 2.6 Floral Guranse (2021-06-23)

E 2.6 Floral Guranse is the latest release of E. The main changes over E 2.5 are full support for TFX, nearly full support for TH0 syntax (and some support for higher-order reasoning), more search heuristics, some faster algorithms, and improved automatic modes.

E 2.5 Avongrove (2020-07-25)

E 2.5 Avongrove is the latest release of E. The main changes over E 2.4 are stronger rewriting, better search heuristics, and improved automatic modes.

E 2.4 Sandakphu (2019-10-23)

E 2.4 Sandakphu is the latest release of E. The main changes are support for additional calculus variants, better search heuristics, and much improved automatic modes.

E 2.3 Gielle (2019-03-12)

E 2.3 Gielle is the latest release of E. The main change is the optional support for lambda-free higher-order logic. This definite 2.3 release also features more robust clausification for some large formulas of unusual structure.

E 2.2 Thurbo Moonlight (2018-10-23)

E 2.2 Thurbo Moonlight is the latest release of E. The main changes are an internal reorganisation of orphan-handling and proof objects, a much improved integration of PicoSAT, and improvements in input validation and proof status reporting. As usual, automatic modes are also improved.

E 2.1 Maharani Hills (2018-06-25)

E 2.1 Maharani Hills is the latest release of E. The main changes are more robust implementation of certain TFF features and an experimental integration of PicoSAT. Also, the internal workflow for new clauses has been changed in a way that makes it easier to batch-evaluate new clauses. As usual, automatic modes are also improved.

E 2.0 Turzum (2017-07-04)

E 2.0 Turzum is the latest release of E. The main change is support for many-sorted logic, i.e. support for the TPTP TFF format (kindly contributed by Simon Cruanes), although currently without interpreted arithmetic. Other changes include performance improvements in clausification, better automatic modes, and proof objects which keep input formula names intact.

E 1.9.1 Sungma (2016-08-31)

E 1.9.1 Sungma is the latest release of E. The main user-visible changes are automatic format detection, improved automatic modes, very much improved support for using the watchlist to provide hints, and a bug-fix in clausification.

E 1.9 Sourenee (2015-07-14)

E 1.9 Sourenee is the latest release of E. The main user-visible changes are better automatic modes and slightly more compact proof objects, now also available for clausification and in Graphviz format for easy visualisation.

E 1.8 Gopaldhara (2013-07-29)

E 1.8 Gopaldhara is the latest release of E. The main user-visible changes are internal (and low-overhead) proof object generation and an alternative automatic mode with strategy scheduling.

E 1.7 Jun Chiabari(2013-03-24)

E 1.7 Jun Chiabari is the latest release of E. It integrates condensing, various minor performance improvements, an updated automatic mode and comes with a normalizer and interactive query support via the LTB batch runner.

E 1.6 Tiger Hill(2012-07-10)

E 1.6 Tiger Hill is the latest release of E.It integrates SInE-like preprocessing for large specifications, various minor performance improvements, and has an updated and simplified automatic mode.

E 1.5 Pussimbing(2012-05-05)

E 1.5 Pussimbing is the latest release of E. It features significant speedups in the inference engine (in particular superposition and subsumption), fixes various minor bugs, and has an updated automatic mode.

E 1.4 Namring(2011-08-20)

E 1.4 Namring is the latest release of E. It features an improved automatic mode, some more heuristic changes, fixing of minor bugs, and general cleanup.

E 1.3 Ringtong (2011-06-27)

E 1.3 Ringtong is the latest release of E. It features an improved automatic mode, adds answer substitution output, and other minor improvements.

E 1.2 Badamtam (2010-09-24)

E 1.2 Badamtam is the latest release of E. It provides a number of significant performance improvements.

Old archive

Versions of E older than E 1.2 are available from the old archive page.
Stephan Schulz, schulz@eprover.org