Построить множество дизъюнктов для рассуждения

-3238513614400В формализованном выше рассуждении из двух посылок следует заключение:
∀x((Px→Bx)∧(Cx→PX)
∃xP(x)
∃x(Cx→Bx)
Докажем рассуждение «от противного», построив логическое произведение посылок и отрицания заключения.
Посылка 1: ∀x(Px→Bx∧Cx→PX=∀x(¬Px∨Bx∧¬Cx∨PX=∀x(¬Px∨Bx∧¬Cx∨PX формула преобразована к ПНФ.
Посылка 2: ∃xP(x) формула преобразована к ПНФ.
Отрицание заключения: ¬∃xCx→Bx=¬∃x¬Cx∨Bx=∀x¬¬Cx∧¬Bx=∀xCx∧¬Bx формула преобразована к ПНФ.
Преобразование Сколема и получение множества дизъюнктов.
Посылка 1: ПНФ ∀x(¬Px∨Bx∧¬Cx∨PX) при отсутствии кванторов существования совпадает со Сколемовской стандартной формой