MACE 20 Reference Manual and Guide
<|reference_start|>MACE 20 Reference Manual and Guide: MACE is a program that searches for finite models of first-order statements. The statement to be modeled is first translated to clauses, then to relational clauses; finally for the given domain size, the ground instances are constructed. A Davis-Putnam-Loveland-Logeman procedure decides the propositional problem, and any models found are translated to first-order models. MACE is a useful complement to the theorem prover Otter, with Otter searching for proofs and MACE looking for countermodels.<|reference_end|>
@article{mccune2001mace,
    title={MACE 2.0 Reference Manual and Guide},
    author={William McCune},
    journal={arXiv preprint arXiv:cs/0106042},
    year={2001},
    number={ANL/MCS-TM-249},
    archivePrefix={arXiv},
    eprint={cs/0106042},
    primaryClass={cs.LO cs.SC}
}