Логика предикатов, правильное ли решение?

Доказать справедливость, используя метод резолюций:

Ни один республиканец или демократ не является социалистом. Норман Томас — социалист. Следовательно, он не республиканец.

Я решил следующим образом:

P(x) = "x - республиканец"
Q(x) = "x - демократ"
S(x) = "x - социалист"

F1: ∀x∀y∀z ( (P(x) v Q(y)) → !S(z) ) = (КНФ) = ( !S(z) v !P(x) ) ^ ( !S(z) v !Q(y) )
F2: S(Норман Томас)
-----------------------------------
R: !Р(Норман Томас)

Тогда мн-во дизъюнктов:
{ !S(z) v !P(x), !S(z) v !Q(y), S(НТ), Р (НТ) }

1) !S(z) v !P(x)
2) !S(z) v !Q(y)
3) S(НТ)
4) Р (НТ)
-----------------
5) !P(НТ) (соединили 1 и 3)
6) F (соединили 5 и 4)

т. к. пришли к противоречию, то исходное предположение было верно.

Скажите пожалуйста, правильное это решение или нет (и как тогда должно решаться)