The STO problem is NP-complete

We prove that the problem STO of deciding whether or not a finite setEof term equations is subject to occur-check is in NP.Eis subject to occur-check if the execution of the Martelli–Montanari unification algorithm gives for inputEasetE′ {x = t}, wheret ≠ xandxappears int. Aptet al. (1994) proved that STO is NP-hard leaving the problem of NP-completeness open.