E is a modern, high performance theorem prover for clausal logic with equality. It is available under the GNU GPL.

External Link

E home page