What is the optimal "most general unifier" algorithm?

Baader and Snyder published several unification algorithms, for both syntactic unification and equational unification.

They state that their third syntactic unification algorithm (in section 2.3) runs in O(n×α(n)) where α(n) is the inverse Ackermann function - in practical situations it's equivalent to a small constant.

The simple algorithm that is used in practice (e.g. in Prolog) is exponential for pathological cases.

There is a theoretically more efficient algorithm by [Martelli and Montanari][1] (IIRC it is linear), but it is much slower for the simple cases which occur in practice, so it is not used much.

[1] http://www.nsl.com/misc/papers/martelli-montanari.pdf