PTTP+GLiDeS is a linear deduction theorem prover that uses semantics to
guided its search for a proof. The semantics are automatically generated by
using MACE to find a model for a subset of the input clause set. Results
have shown that where an ``effective'' model is found, the guidance it
provides is of great benefit. This paper discusses how MACE is used in
PTTP+GLiDeS, and what properties are desirable in models and model generators
for this application.