We describe a method for learning formulas in firstorder logic using a brute-force, smallest-first search. The method is exceedingly simple. It generates all irreducible well-formed formulas up to a fixed size and tests them against a set of examples. Although the method has some obvious limitations due to its computational complexity, it performs surprisingly well on some tasks. This paper describes experiments with two applications of the method in the MULTI-TACsystem, a program synthesizer for constraint satisfaction problems. In the first application, axioms are learned, and in the second application, search control rules are learned. We describe these experiments, and consider why searching the space of small formulas makes sense in our applications.