In [23], Slaney presents a system for generating small finite models, called FINDER. The system is very fast, using sophisticated data structures and intelligent backtracking. We (Slaney, Lusk, and McCune) are currently incorporating FINDER into OTTER. Finite models fit neatly into the closure algorithm as a filter on allowable inferences. FINDER is so fast that it can generate new models during the OTTER run and test every newly derived formula to ascertain whether or not it is true in the current model. Preliminary experiments show that dynamic model generation and testing allow proofs to be obtained with far fewer generated clauses than OTTER on its own would generate, although more work is needed before this can be translated into a more than a modest gain in speed. It also remains unclear just how to apply this idea in the parallel setting. We call this system SCOTT (for Semantically Constrained OTTER).