Metis is an automatic theorem prover for first order logic with equality.
Metis is being maintained: the latest version is Metis 2.4 (release 20200713). Metis is free software, released under the MIT License. To adapt Metis for your own application I recommend forking the development version.
To report a bug or request an enhancement, please file an issue at GitHub.