Vorobyov, Sergei Computational Biology and Applied Algorithmics, MPI for Informatics, Max Planck Society; Programming Logics, MPI for Informatics, Max Planck Society;
Vorobyov, S. (2002). $\forall\exists^5$-equational theory of context unification is undecidable. Theoretical Computer Science, 275, 463-479.