E is a high-performance theorem prover for full first-order logic with equality.
E is developed by Stephan Schulz, originally in the Automated Reasoning Group at TU Munich, now at Baden-Württemberg Cooperative State University Stuttgart.
Significant innovations include shared term rewriting (where many possible equational simplifications are carried out in a single operation),[2] several efficient term indexing data structures for speeding up inferences, advanced inference literal selection strategies, and various uses of machine learning techniques to improve the search behaviour.
[9] It repeated the performance in FOF and CNF in 2010, and won a special award as "overall best" system.
[10] In the 2011 CASC-23 E won the CNF division and achieved second places in UEQ and LTB.