Faster, Higher, Stronger: E 2.3

                    Stephan Schulz
                    Simon Cruanes
                    Petar Vukmirovic

E 2.3 is a theorem prover for many-sorted first-order logic with
equality. We describe the basic logical and software architecture of
the system, as well as core features of the implementation. We
particularly discuss recently added features and extensions, including
the ex- tension to many-sorted logic, optional limited support for
higher-order logic, and the integration of SAT techniques via
PicoSAT. Minor additions include improved support for TPTP standard
features, always-on internal proof objects, and lazy orphan
removal. The paper also gives an overview of the performance of the
system, and describes ongoing and future work.