Prover9 генерирует неверное доказательство

Question

Я пытаюсь найти решение логической задачи первого порядка с помощью prover9, вопрос в следующем:

1. Кто-то, кто живет в Maniac Mansion, убил тетю Агату.
2. Агата, дворецкий и Чарльз живут в Особняке Маньяков и являются единственными людьми, которые там живут.
3. Убийца всегда ненавидит свою жертву и никогда не бывает богаче своей жертвы.
4. Чарльз не ненавидит никого, кого ненавидит тетя Агата.
5. Агата ненавидит всех, кроме дворецкого.
6. Дворецкий ненавидит всех, кто не богаче, чем тетя Агата.
7. Дворецкий ненавидит всех, кого ненавидит тетя Агата.
8. Никто не ненавидит всех.
9. Агата не дворецкий.

Мне нужно сгенерировать доказательство, которое решает тайну того, кто убил Агату, введя соответствующую формулу в поле цели программного обеспечения Prover9.

Я перевел эти утверждения в логические операторы первого порядка в форме проверки 9 и поставил цель найти убийцу. И когда он бежит, он говорит, что дворецкий является убийцей Агаты, но в следующем вопросе объясняется, кто дворецкий не может быть убийцей Агаты, основываясь на предоставленных фактах.

%% 1. Someone who lives in Maniac Mansion killed Aunt Agatha.
exists x (LivesMM(x) & Killed(x,agatha)).

%% 2. Agatha, the butler, and Charles live in Maniac Mansion, and are the only people who live there.
LivesMM(agatha) & LivesMM(charles) & LivesMM(butler) & (all x (LivesMM(x) -> ((x=agatha) | (x=charles) | (x=butler)))).

%% 3. A killer always hates his victim, and is never richer than his victim.
all x all y (Killed(x,y) -> (Hates(x,y) & -(Richer(x,y)))).

%% 4. Charles hates no one that Aunt Agatha hates.
all x (Hates(agatha,x) -> -Hates(charles,x)).

%% 5. Agatha hates everyone except the butler.
all x (-(x=butler) -> Hates(agatha,x)).

%% 6. The butler hates everyone not richer than Aunt Agatha.
all x (-Richer(x,agatha) -> Hates(butler,x)).

%% 7. The butler hates everyone Aunt Agatha hates.
all x (Hates(agatha,x) -> Hates(butler,x)).

%% 8. No one hates everyone.
(all x exists y (-Hates(x,y))).

%% 9. Agatha is not the butler.
-(agatha=butler).

end_of_list.

formulas(goals).

%% Who killed Aunt Agatha?

exists x((x=agatha | x=charles | x=butler) & Killed(x,agatha)).

end_of_list.

Проблема:

Я ожидал, что программа докажет, что убийцей был Агата или Чарльз, но не дворецкий, поскольку следующий вопрос объясняет, почему дворецкий не может быть убийцей, основываясь напредоставленные факты выше. Я не знаю, чего не хватает, или я неправильно преобразовал утверждения в логику первого порядка.