I have just released MACE 1.2.0. MACE (formerly called ANL-DP) is a program that searches for small finite models of first-order statements. It can also test satisfiability of propositional statements. See the MACE page for an introduction.
To run this version of MACE, you need Otter 3.0.4, which parses the input and does some translation.
You can obtain MACE by anonymous ftp .
MACE is not available for DOS or Macintosh computers.
Bill McCune