 Instead of removing redundant clauses, some strategies prevent the generation of useless clauses in the first place. The set-of-support strategy (Wos, Carson &amp; Robinson 1965) is one of the most powerful strategies of this kind. A subset T of the set S, where S is initially Γ ∪ {~α}, is called a set of support of S iff S − T is satisfiable. Set-of-support resolution dictates that the resolved clauses are not both from S − T. The motivation behind set-of-support is that since the set Γ is usually satisfiable it might be wise not to resolve two clauses from Γ against each other. Hyperresolution (Robinson 1965b) reduces the number of intermediate resolvents by combining several resolution steps into a single inference step.