The STO-problem is NP-hard

A finite set of term equations E is called subject to the occur-check (STO) if a sequence of actions of the Martelli-Montanari unification algorithm starts with E and ends with a failure due to occur-check. We prove here that the problem of deciding whether E is STO is NP-hard.