H. Fassbender and H. Vogler, “A universal unification algorithm based on unification-driven leftmost outermost narrowing”, Acta Cybern, vol. 11, no. 3, pp. 139-167, Jan. 1994.