Satchmo is an automated theorem prover for first-order predicate logic implemented in Prolog. Its reasoning paradigm, model generation, is more powerful than the traditional refutation paradigm. It enabled the development of a novel and efficient technique to compute minimal Herbrand models, which prevents the generation of non-minimal models that would later have to be filtered out in a post-processing step. It also encouraged the development of several advanced efficiency enhancing techniques that result in a highly competitive performance on standard benchmark problems.