We use finite interpretations to guide searches in first-order and equational theorem provers. The interpretations are carefully chosen and based on expert knowledge of the problem area of the conjecture. The method has been implemented in the Prover9 system, and equational examples are given the areas of lattice theory, Boolean algebras, and modular ortholattices.