Shortly after the formulation of the resolution principle, Dan Carson and Larry Wos developed a resolution theorem prover they called P1 (for ``Program 1''). It was based on the closure approach, with forward subsumption only, and used binary resolution with factoring. It also had unit preference[27], an ordering strategy that is one of the few features not carried on into subsequent systems. The set-of-support strategy[29] and demodulation were developed during experimentation with this program. Thus from the very beginning the closure approach was not applied blindly, but in conjunction with a strategy for exploring the more relevant parts of the search space earlier than the less relevant parts. As we will see when we examine it in detail, the closure approach itself makes the application of such strategies quite natural while still maintaining completeness.
It was implemented in IBM 704 assembly language. It could prove, once the set of support strategy was added to the program, that groups in which every element has order 2 are commutative, that 1#1 in a ring, and that (-x)(-y) = xy in a ring, although for this last problem it needed the lemma that 1#1.