mace2 binary package in Ubuntu Xenial amd64

 MACE is a program that searches for finite models of first-order and
 equational statements developed at Argonne National Laboratory.
 .
 This package includes ANLDP, which calls the propositional decision
 procedure at the core of MACE directly.
 .
 MACE serves as a complementary companion to OTTER, which
 searches for refutations of the same class of statement. In
 particular, if you have a first-order conjecture, OTTER will search
 for a proof, and MACE will search for a counterexample from the same
 input file.

Source package