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

iProver v2.5 (CASC-J8, 2016) iProver is implemented in OCaml.
Features and supported input formats:
Easy to install and use:

Major contributors: Project manager: Konstantin Korovin (korovin[@]cs.man.ac.uk), the University of Manchester, UK.
Please email us for comments, questions, 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.

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