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.