As usual, you can grab the source distribution below . There are a couple of known bugs in the optimizer of GCC 2.95.1. Check Makefile.vars for the compilation options.
E is a a purely equational theorem prover for clausal logic.
There is a short system description about E 0.6 on the CASC-17 website. If you are like me , you can probably learn the syntax best from examples . There are a variety of them included with the distribution. Performance E 0.6 won the first place in the MIX category of the CASC-17 theorem proving competition. We take this as a sign that E performs relatively well overall.