Metis is an automatic theorem prover for first order logic with equality.
Metis is being actively maintained: the latest version is Metis 2.3 (release 20120927). Users are encouraged to try out or adapt Metis for their own applications. Metis is free software, released under the MIT License.
To report bugs, request features, or obtain help using Metis, please email firstname.lastname@example.org