System Description: E 1.8
                        Stephan Schulz
                      schulz@eprover.org

  E is a theorem prover for full first-order logic with equality. It
  reduces first-order problems to clause normal form and employs a
  saturation algorithm based on the equational superposition
  calculus. E is built on shared terms with cached rewriting, and
  employs several innovations for efficient clause indexing. Major
  strengths of the system are automatic problem analysis and highly
  flexible search heuristics. The prover can provide verifiable proof
  objects and answer substitutions with very little overhead. E
  performs well, solving more than 69% of TPTP-5.4.0 FOF and CNF
  problems in automatic mode.