By not utilizing the reasoning results derivable whenever refutations are found at nodes in proof trees, UNSEARCHMO might repeat some reasoning that has been made before. Addressing this problem, this paper presents a refinement on UNSEARCHMO, called R-UNSEARCHMO, by summarizing the derived refutations as lemmas and utilizing them in the further reasoning. In this way, R-UNSEARCHMO can avoid repeated reasoning and always search a subspace of that UNSEARCHMO does. Somewhat surprisingly, our refinement almost takes no additional cost. We describe the refinement, present the implementation and provide examples to demonstrate the power of our refinement.