Footnote

Searching is potentially slow, so other techniques are used in the resolution algorithm. If an assumption is contradicted by itself, then it must also be contradicted by another assumption if a resolution exists. Thus, inferences can be made about other assumptions used in its conflict tag, inferences can be made about these assumptions' conflicts, and so on. The resolution algorithm also discovers completely independent sets of assumptions, and searches each set separately. Due to such techniques, assumption resolution has been relatively fast so far.