e/E equational theorem prover

Information
has gloss	eng: E is a modern, high performance theorem prover for full first-order logic with equality. It is based on the equational superposition calculus and uses a purely equational paradigm. It has been integrated into other theorem provers and it has been among the best-placed systems in several theorem proving competitions. E was developed by Stephan Schulz, originally in the Automated Reasoning Group at TU Munich.
lexicalization	eng: E equational theorem prover
instance of	c/Unix programming tools