 However, an algorithm has been devised (Huet 1975, Jensen &amp; Pietrzykowski 1976), called pre-unification, which will find a unifier for a set of pairs of wffs if one exists. The pre-unifiers computed by Huet’s procedure are substitutions that can reduce the original unification problem to one involving only so called flex-flex unification pairs. Flex-flex pairs have variable head symbols in both terms to be unified and they are known to always have a solution. The concrete computation of these solutions can thus be postponed or omitted. Pre-unification is utilized in all the resolution based theorem provers mentioned in  Section 4.  