Доказательство логической теоремы первого порядка с использованием Prover9

Question

Я пытаюсь доказать проблему с помощью Prover9, он постоянно говорит «Исчерпаны» (что означает, что моя логика неверна), я не знаю, что я делаю неправильно в переводе.

Проблема:

1. Коровы - это животные, которые едят траву.

2. Я не ем траву.

3. Кроме меня, единственные животные в моем доме - кошачьи.
4. Никакие животные никогда не берут меня, кроме тех, кто в моем доме.
5. Я ненавижу животных, которые меня не берут.
6. Когда я ненавижу животное, я избегаю его.
7. Каждое животное, которое любит смотреть на луну, подходит для домашнее животное.
8. Животные не являются плотоядными, если они не бродят ночью.
9. Каждый котенок ест какое-то животное меньше своего.
10. Я не самое маленькое животное в моем доме.
11. Животных едят только плотоядные животные.
12. Коровы не подходят для домашних животных.
13. Животные, которые бродят ночью, всегда любят смотреть на луну.
14. Я избегаю коров.

Мое решение:

% 1. Коровы - животные, которые едят траву.

all x (Cow(x) -> Animal(x) & eats(x, Grass)).

% 2. Я не ем траву.

- eats(me,Grass).

3%. Кроме меня, единственные животные в моем доме - кошачьи.

- (exists x (x != (me)) | ((Animal(x) & In(x) & -Feline(x)))).

% 4. Никто из животных не забирает меня, кроме тех, которые находятся в моем доме.

all x (Animal(x) & -(In(x)) -> -talk(x,me)).

% 5. Я ненавижу животных, которые меня не берут.

all x ( Animal(x) & -talk(x,me) -> detest(me,x)).

% 6. Когда я ненавижу животное, я избегаю его.

all x (Animal(x) & detest(me,x) -> avoid(me,x)).

% 7. Каждое животное, которое любит смотреть на луну, % подходит для домашнего животного.

all x (Animal(x) & gaze(x, Moon) -> Pet(x)).

% 8. Животные не плотоядные, если они не бродят ночью.

all x (Animal(x) & prawl(x) -> Carn(x)).

% 9. Каждый котенок ест какое-то животное меньше своего.

all x exists y (Feline(x) & Animal(y) & smaller(y,x) -> eats(x,y) ).

% 10. Я не самое маленькое животное в моем доме.

exists x (Animal(x) & smaller(x,me)).

% 11. Животных едят только плотоядные животные.

-(all x all y (Animal(y) & Animal(x) & (-Carn(x)) -> eats(x,y))).

% 12. Коровы не подходят для домашних животных.

all x (Cow(x) -> -Pet(x)).

% 13. Животные, которые бродят ночью, всегда любят смотреть на луну.

all x (Animal(x) & prawl(x) -> gaze(x, Moon)).

****% ЦЕЛЬ: Я ИЗБЕГАЮ КОРОВ. ****

все х (Корова (х) -> избегать (я, х)).