О сложности проблемы эквивалентности хорновским формулам

Изучается сложность проблемы существования хорновского предложения (тождества, квазитождества, $\forall$-предложения, $\exists$-предложения), эквивалентного данному предложению. Доказывается, что если сигнатура содержит хотя бы один символ местности $k\geqslant 2$, то каждая из указанных проблем является $m$-полным $\Sigma^0_1$-множеством.