iProver --- an instantiation-based theorem prover for first-order logic

iProver v3 (post CASC-27, 2020) (GNU GPL)
iProver is implemented in OCaml.
Features and supported input formats:
Easy to install and run:

Installing OCaml using opam >= 2.0.0 (https://opam.ocaml.org/) on e.g. Ubuntu:
Major contributors:

Project leader: Konstantin Korovin (konstantin.korovin[@]manchester.ac.uk), The University of Manchester, UK
Please email (konstantin.korovin[@]manchester.ac.uk) for comments, suggestions, bug reports, or if you would like to join the project.
We are keen to hear about your experience with iProver, so please drop us a line.

iProver won the EPR and first-order satisfiability (FNT) divisions at several recent CASC competitions.

References:
External libraries:
iProver is currently distributed under GNU GPL if you require a different license please contact: korovincs.man.ac.uk
maintained by Konstantin Korovin, this research is supported by The Royal Society and the University of Manchester