In this paper, some errors related to substitution and set operations in the proof procedures of lifting lemma and the completeness theorem of deletion strategy, which are in the literatures on resolution-based automated reasoning, are pointed out, analyzed, and corrected.