Does a system that is nonoverlapping under unification with infinite terms have unique normal forms?

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

Does a system that is nonoverlapping under unification with infinite terms (unification without ``occur-check'' [Ogawa, 1995]) have unique normal forms? This conjecture was originally proposed in [Ogawa, 1995] with an incomplete proof, as an extension of the result on strongly nonoverlapping systems [Ogawa, 1995]. Related results appear in [Ogawa, 1995], but the original conjecture is still open. This is related to Problem 58. This problem is also related with modularity of confluence of systems sharing constructors, see [Ogawa, 1995].

Recorded progress.

The answer is yes if the system is also nonduplicating [Ogawa, 1995]. A direct technique is given in [Ogawa, 1995]. The nonduplicating condition can be relaxed under a certain technical condition [Ogawa, 1995]. Some extensions to handle root overlaps are given in [Ogawa, 1995] and a restricted version of the result in [Ogawa, 1995] is also proved using the direct technique in [Ogawa, 1995].