fimo is a system for computing finite models of first-order theories
(written in TPTP format)
via incremental Answer Set Programming.
fimo uses iclingo for finding answer sets of the resulting logic program.
An answer set represents a finite model of the input theory.