E-Darvin

E-Darwin is an automated theorem prover for first-order clausal logic with equality. It accepts problems in tptp or tme syntax. Non-clausal input is clausified using the eprover (or soon a built-in clausifier). E-Darwin implements the Model Evolution calculus and several variants thereof which include equality reasoning, see the papers. The system is a based on the Darwin prover. As Darwin is no longer actively maintained, E-Darwin will eventually subsume all of its functions. The development of E-Darwin forked off from Darwin 1.3, so at the moment E-Darwin still needs to catch up on the changes made between Darwin 1.3 and its last version, Darwin 1.4.5.