Where, What, and How? Lessons from the Evolution of E
                        Stephan Schulz

E is a theorem prover for first-order logic with equality. It has
evolved over the last 15 years from a basic implementation of the
superposition calculus to a fully-featured theorem prover supporting a
rich language, an efficient inference engine, and several levels of
manual and automatic control.

Most of the changes to the prover have been conservative
extensions. This allows us to take a virtual step back in time and to
evaluate which features have had how much of an influence on the power
of the system, and thus maybe inform us where future research is
particularly promising.