Здравствуйте, Дмитрий!
Как я понял из прочитанного
здесь, при сколемизации необходимо исключить из формулы
[$8707$]y [$8704$]x [$966$](x, y) квантор существования. Он связывает переменную
y и является самым левым в кванторной приставке (префиксе формулы). Значит, нужно заменить все вхождения в формулу переменной
y на новую константу
c и вычеркнуть квантор из приставки. В результате получится формула
[$8704$]x [$966$](x, c).
С уважением.
Об авторе:
Facta loquuntur.