In case anybody feels like trying the latest Version of E (via sledgehammer).
Tobias -------- Original Message -------- > From: Stephan Schulz <schulz at informatik.tu-muenchen.de> > Date: 23 October 2008 00:41:54 BST > To: undisclosed-recipients: ; > Subject: E Equational Theorem Prover 1.0 "Temi" released > > > E 1.0 "Temi" is the latest version of the successful automated theorem > prover. > > E is a theorem prover for full first order logic with equality. It has > successfully competed in several CASC competitions and is generally > considered a friendly and powerful system (as theorem provers go). > > The new version improves clausification, has a more GNU-like > installation system, and has been updated to comply with the latest > TPTP-3 syntax. > > E is available as a source distribution for UNIX-variants. It installs > cleanly under all UNIX variants I could get my hands on: Various > versions of GNU/Linux for Intel and SPARC, Solaris, HPUX and > MacOS-X. Users have reported successful builds on a large number of > other systems, including Windows/Cygwin. > > The system is distributed under the GNU General Public License. > > You can find the source distribution and additional information at > http://www.eprover.org > > > Have fun! > > > Stephan > > -- > -------------------------- It can be done! > --------------------------------- > Please email me as schulz at eprover.org (Stephan Schulz) > ----------------------------------------------------------------------------