"E is a theorem prover for full first-order logic with equality. It
accepts a problem specification, typically consisting of a number of
first-order clauses or formulas, and a conjecture, again either in
clausal or full first-order form. The system will then try to find a
formal proof for the conjecture, assuming the axioms."
[http://www4.informatik.tu-muenchen.de/~schulz/E/E.html]
Signed-off-by: Adam Vandenberg <flangy@gmail.com>
Brett Koonce
Libor Wagner