Matematyka.pl

Bill i Mark lubią baseball. Bill lubi grę wtedy, gdy grę lubią jego przyjaciele: Mark i Tom.
Czy Tom lubi baseball ? Przeprowadzić wnioskowanie rezolucyjne.

Mam problem z tym przykładem, tj. nie mogę dojść do sprzeczności robiąc to tą metodą. Napiszę co próbowałem:

predykaty:
\(\displaystyle{ likes(Bill, baseball) \\
likes(Mark, baseball) \\
\forall{G} \left( (likes(Mark, G) \wedge likes(Tom, G)) \Rightarrow likes(Bill, G) \right) \\}\)
dokładam zaprzeczenie tego co będę dowodził:
\(\displaystyle{ \neg likes(Tom, baseball)}\)

przekształcam predykaty żeby były klauzulami z samymi dysjunkcjami itp.:
\(\displaystyle{ likes(Bill, baseball) \\
likes(Mark, baseball) \\
\neg likes(Mark, G) \vee \neg likes(Tom, G) \vee likes(Bill, G) \\
\neg likes(Tom, baseball)}\)

no i jak zacznie się tworzyć z tego nowe przesłanki to nie wychodzi 0 ani nic sensownego.

przesłanki:
\(\displaystyle{ \neg likes(Mark, G) \vee \neg likes(Tom, G) \vee likes(Bill, G) \\
likes(Mark, baseball)}\)
unifikator:
\(\displaystyle{ baseball/G}\)
rezolwenta:
\(\displaystyle{ \neg likes(Tom, baseball) \vee likes(Bill, baseball)}\)
I nie wiem co mam dalej począć.
Ktoś coś widzi/podpowie?