где F и G— сколемовские функции. Общее правило состоит в том, что все параметры сколемовской функции должны быть переменными, на которые распространяются кванторы всеобщности, в область действия которых попадает соответствующий квантор существования. Как и при использовании конкретизации с помощью квантора существования, сколемизированное высказывание является выполнимым тогда и только тогда, когда выполнимо первоначальное высказывание.

•    Удаление кванторов всеобщности. В данный момент на все оставшиеся переменные должны распространяться кванторы всеобщности. Кроме того, данное высказывание эквивалентно тому, в котором все кванторы всеобщности перенесены влево. Поэтому кванторы всеобщности могут быть удалены следующим образом:

• Распределение связкипо:

На этом этапе может также потребоваться выполнить раскрытие скобок во вложенных конъюнкциях и дизъюнкциях.

Теперь рассматриваемое высказывание находится в форме CNF и состоит из двух выражений. Оно полностью недоступно для восприятия. (Помочь его понять может такое пояснение, что сколемовская функция F(x) указывает на животное, которое потенциально может быть нелюбимым лицом х, a G(x) указывает на кого-то, кто может любить лицо х.) К счастью, людям редко приходится изучать высказывания в форме CNF, поскольку показанный выше процесс преобразования может быть легко автоматизирован.