предваренная форма (мат логика)

[lenar]

в плане решения есть такой пункт:
переменовать (если не обходимо) связанные переменные таким образом, чтобы  никакая переменная не имела бы одновременно  свободных и связанных вхождений

об этом можно поподробнее