Does AC unification terminate under more flexible control?

The source page states the original problem together with its recorded qualifications and progress updates as follows.

Fages [d'Ajol, 1991] proved that associative-commutative unification terminates when ``variable replacement'' is made after each step. Boudet, et al. [d'Ajol, 1991] have proven that it terminates when variable replacement is postponed to the end. Does the same (or similar) set of transformation rules terminate with more flexible control?