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