NOTE: There is a new model searcher called MACE4, which is not quite backward compatible with MACE2. MACE4 usually performs much better on equational problems, and MACE2 does better when many of the clauses are multiliteral.
MACE2's engine is a Davis-Putnam-Loveland-Logemann (DPLL) propositional decision procedure. It is available in the Otter-3.3/MACE-2.2 package as a standalone program called ANLDP. Some details of the DPLL implementation can be found in a 1994 report A Davis-Putnam Program and Its Application to Finite First-Order Model Search: Quasigroup Existence Problems.
MACE 2.2 for is bundled with Otter 3.3
For a better introduction, see the MACE 2.0 User Manual and Guide.
Here are the example inputs from the distribution package.
These activities are projects of the Mathematics and Computer Science Division of Argonne National Laboratory.