Метод резолюций. Второй день убил, решить не могу

[ZhenyaKa]

1,2) Ни поэты, ни отшельники не могут быть палачами.
3) Палач будет художником только в том случае, если он китаец.
4) Если человек не китаец, то он не станет хорошим палачом.
5) Кроме этого китайцы являются хорошими поэтами.
6) Все китайцы в мире становятся либо художниками, либо поэтами.
7) Все хорошие люди либо поэты, либо отшельники.
8) Палачи не могут быть хорошими людьми.
9) Не отшельники являются либо палачами, либо китайцами.
10) Следовательно, некоторые поэты в мире хорошие люди.


$\[\begin{gathered} 1)\,\overline {\exists x(P{\text{(}}x) \cap Y(x))} \leftrightarrow \forall x(\overline {P(x)} \cup \overline {Y(x)} ) \hfill \\ 2)\,\overline {\exists x(O{\text{(}}x) \cap Y(x))} \leftrightarrow \forall x(\overline {O(x)} \cup \overline {Y(x)} ) \hfill \\ 3)\,\forall x(Y{\text{(}}x) \cap K(x) \to X(x)) \hfill \\ 4)\,\forall x(K{\text{(}}x) \to P(x)) \hfill \\ 5)\,\overline {\exists x(\overline {K{\text{(}}x)} \cap Y(x))} \leftrightarrow \forall x(K(x) \cup \overline {Y(x)} ) \hfill \\ 6)\,\forall x(K{\text{(}}x) \to (X(x) \cup P(x))) \hfill \\ 7)\,\forall x(L{\text{(}}x) \to (O(x) \cup P(x))) \hfill \\ 8)\,\overline {\exists x(L{\text{(}}x) \cap Y{\text{(}}x))} \leftrightarrow \forall x(\overline {L(x)} \cup \overline {Y(x)} ) \hfill \\ 9)\,\forall x(O{\text{(}}x) \to (Y(x) \cup K(x))) \hfill \\ \to \hfill \\ 10)\,\exists x(P{\text{(}}x) \cap L{\text{(}}x)) \hfill \\ \end{gathered} \]$

затем беру от противного 10й пункт.

$\[\overline {\exists x(P{\text{(}}x) \cap L{\text{(}}x))} \leftrightarrow \forall x(\overline {P{\text{(}}x) \cap L{\text{(}}x)} ) \leftrightarrow \forall x(\overline {P{\text{(}}x)} \cup \overline {L{\text{(}}x)} )\]$

избавляюсь от импликаций:

$\[\begin{gathered} 3)\,\forall x(Y{\text{(}}x) \cap K(x) \to X(x)) \leftrightarrow \forall x(\overline {Y{\text{(}}x) \cap K(x)} \cup X(x)) \leftrightarrow \forall x(\overline {Y{\text{(}}x)} \cup \overline {K(x)} \cup X(x)) \hfill \\ 4)\,\forall x(K{\text{(}}x) \to P(x)) \leftrightarrow \forall x(\overline {K{\text{(}}x)} \cup P(x)) \hfill \\ 6)\,\forall x(K{\text{(}}x) \to (X(x) \cup P(x))) \leftrightarrow \,\forall x(\overline {K{\text{(}}x)} \cup X(x) \cup P(x)) \hfill \\ 7)\,\forall x(L{\text{(}}x) \to (O(x) \cup P(x))) \leftrightarrow \forall x(\overline {L{\text{(}}x)} \cup O(x) \cup P(x)) \hfill \\ 9)\,\forall x(O{\text{(}}x) \to (Y(x) \cup K(x))) \leftrightarrow \forall x(\overline {O{\text{(}}x)} \cup Y(x) \cup K(x)) \hfill \\ \end{gathered} \]$

и получаю следующие дизъюнкты:

$\[\begin{gathered} 1)\,\overline {P(x)} \cup \overline {Y(x)} \hfill \\ 2)\,\overline {O(x)} \cup \overline {Y(x)} \hfill \\ 3)\,\overline {Y{\text{(}}x)} \cup \overline {K(x)} \cup X(x) \hfill \\ 4)\,\overline {K{\text{(}}x)} \cup P(x) \hfill \\ 5)\,K(x) \cup \overline {Y(x)} \hfill \\ 6)\,\overline {K{\text{(}}x)} \cup X(x) \cup P(x) \hfill \\ 7)\,\overline {L{\text{(}}x)} \cup O(x) \cup P(x) \hfill \\ 8)\,\overline {L(x)} \cup \overline {Y(x)} \hfill \\ 9)\,\overline {O{\text{(}}x)} \cup Y(x) \cup K(x) \hfill \\ 10)\,\overline {P{\text{(}}x)} \cup \overline {L{\text{(}}x)} \hfill \\ \end{gathered} \]$


и все. дальше тупик. далее не выходит получения одинарных дизъюнктов для получения противоречий.
2 дня убил. все никак :(

как к этой сотоняке подступиться, может не учел чего.

[JMH]

Мне не совсем понятна Ваша система записи, например Вы используете теоретико-множественные операции вместо логических, это случайность или я чего-то не понимаю? Далее, не все условия у Вас записаны верно, например:

ZhenyaKa в сообщении #310517 писал(а):

...
4) Если человек не китаец, то он не станет хорошим палачом.
...
4)$\forall x(K{\text{(}}x) \to P(x))$

следует записывать так: $\overline K \to \overline P$ что эквивалентно $P \to K$. Вобщем, советую хорошенько проверить, как Вы записали условия.

[ZhenyaKa]

JMH в сообщении #311091 писал(а):

Мне не совсем понятна Ваша система записи, например Вы используете теоретико-множественные операции вместо логических, это случайность или я чего-то не понимаю? Далее, не все условия у Вас записаны верно, например:

ZhenyaKa в сообщении #310517 писал(а):

...
4) Если человек не китаец, то он не станет хорошим палачом.
...
4)$\forall x(K{\text{(}}x) \to P(x))$

следует записывать так: $\overline K \to \overline P$ что эквивалентно $P \to K$. Вобщем, советую хорошенько проверить, как Вы записали условия.

4 и 5 просто местами перепутаны