Proof
1
axiom
\( \exists \mathit{X}\, \mathrm{grain}(\mathit{X}) \)
pel47_6_1  |  Problems/PUZ/PUZ031+1.p
2
axiom
\( \forall \mathit{X1}\, \left(\mathrm{grain}(\mathit{X1}) \to \mathrm{plant}(\mathit{X1})\right) \)
pel47_6_2  |  Problems/PUZ/PUZ031+1.p
3
axiom
\( \exists \mathit{X1}\, \mathrm{wolf}(\mathit{X1}) \)
pel47_1_2  |  Problems/PUZ/PUZ031+1.p
4
axiom
\( \exists \mathit{X1}\, \mathrm{fox}(\mathit{X1}) \)
pel47_2_2  |  Problems/PUZ/PUZ031+1.p
5
axiom
\( \exists \mathit{X1}\, \mathrm{snail}(\mathit{X1}) \)
pel47_5_2  |  Problems/PUZ/PUZ031+1.p
6
axiom
\( \forall \mathit{X}\, \left(\mathrm{caterpillar}(\mathit{X}) \lor \mathrm{snail}(\mathit{X}) \to \exists \mathit{Y}\, \left(\mathrm{plant}(\mathit{Y}) \land \mathrm{eats}(\mathit{X}, \mathit{Y})\right)\right) \)
pel47_14  |  Problems/PUZ/PUZ031+1.p
7
axiom
\( \exists \mathit{X1}\, \mathrm{bird}(\mathit{X1}) \)
pel47_3_2  |  Problems/PUZ/PUZ031+1.p
8
axiom
\( \forall \mathit{X}\, \forall \mathit{Y}\, \left(\mathrm{bird}(\mathit{Y}) \land \left(\mathrm{snail}(\mathit{X}) \lor \mathrm{caterpillar}(\mathit{X})\right) \to \mathrm{much\_smaller}(\mathit{X}, \mathit{Y})\right) \)
pel47_8  |  Problems/PUZ/PUZ031+1.p
9
axiom
\( \forall \mathit{X}\, \left(\mathrm{animal}(\mathit{X}) \to \forall \mathit{Y}\, \left(\mathrm{plant}(\mathit{Y}) \to \mathrm{eats}(\mathit{X}, \mathit{Y})\right) \lor \forall \mathit{Y1}\, \left(\mathrm{animal}(\mathit{Y1}) \land \mathrm{much\_smaller}(\mathit{Y1}, \mathit{X}) \land \exists \mathit{Z}\, \left(\mathrm{plant}(\mathit{Z}) \land \mathrm{eats}(\mathit{Y1}, \mathit{Z})\right) \to \mathrm{eats}(\mathit{X}, \mathit{Y1})\right)\right) \)
pel47_7  |  Problems/PUZ/PUZ031+1.p
10
axiom
\( \forall \mathit{X}\, \left(\mathrm{snail}(\mathit{X}) \to \mathrm{animal}(\mathit{X})\right) \)
pel47_5_1  |  Problems/PUZ/PUZ031+1.p
11
axiom
\( \forall \mathit{X}\, \left(\mathrm{bird}(\mathit{X}) \to \mathrm{animal}(\mathit{X})\right) \)
pel47_3_1  |  Problems/PUZ/PUZ031+1.p
12
axiom
\( \forall \mathit{X}\, \forall \mathit{Y}\, \left(\mathrm{bird}(\mathit{X}) \land \mathrm{fox}(\mathit{Y}) \to \mathrm{much\_smaller}(\mathit{X}, \mathit{Y})\right) \)
pel47_9  |  Problems/PUZ/PUZ031+1.p
13
axiom
\( \forall \mathit{X}\, \left(\mathrm{fox}(\mathit{X}) \to \mathrm{animal}(\mathit{X})\right) \)
pel47_2_1  |  Problems/PUZ/PUZ031+1.p
14
axiom
\( \forall \mathit{X}\, \forall \mathit{Y}\, \left(\mathrm{bird}(\mathit{X}) \land \mathrm{snail}(\mathit{Y}) \to \neg \mathrm{eats}(\mathit{X}, \mathit{Y})\right) \)
pel47_13  |  Problems/PUZ/PUZ031+1.p
15
axiom
\( \forall \mathit{X}\, \forall \mathit{Y}\, \left(\mathrm{fox}(\mathit{X}) \land \mathrm{wolf}(\mathit{Y}) \to \mathrm{much\_smaller}(\mathit{X}, \mathit{Y})\right) \)
pel47_10  |  Problems/PUZ/PUZ031+1.p
16
axiom
\( \forall \mathit{X}\, \left(\mathrm{wolf}(\mathit{X}) \to \mathrm{animal}(\mathit{X})\right) \)
pel47_1_1  |  Problems/PUZ/PUZ031+1.p
17
conjecture
\( \exists \mathit{X}\, \exists \mathit{Y}\, \left(\mathrm{animal}(\mathit{X}) \land \mathrm{animal}(\mathit{Y}) \land \exists \mathit{Z}\, \left(\mathrm{grain}(\mathit{Z}) \land \mathrm{eats}(\mathit{Y}, \mathit{Z}) \land \mathrm{eats}(\mathit{X}, \mathit{Y})\right)\right) \)
pel47  |  Problems/PUZ/PUZ031+1.p
18
axiom
\( \forall \mathit{X}\, \forall \mathit{Y}\, \left(\mathrm{wolf}(\mathit{X}) \land \left(\mathrm{fox}(\mathit{Y}) \lor \mathrm{grain}(\mathit{Y})\right) \to \neg \mathrm{eats}(\mathit{X}, \mathit{Y})\right) \)
pel47_11  |  Problems/PUZ/PUZ031+1.p
19
plain
\( \mathrm{grain}(\mathrm{sk6}) \)
cnf_transformation [ 1 ]
20
plain
\( \neg \mathrm{grain}(\mathit{X1}) \lor \mathrm{plant}(\mathit{X1}) \)
cnf_transformation [ 2 ]
21
plain
\( \mathrm{wolf}(\mathrm{sk1}) \)
cnf_transformation [ 3 ]
22
plain
\( \mathrm{fox}(\mathrm{sk2}) \)
cnf_transformation [ 4 ]
23
plain
\( \mathrm{snail}(\mathrm{sk5}) \)
cnf_transformation [ 5 ]
24
plain
\( \neg \mathrm{snail}(\mathit{X}) \lor \mathrm{plant}(\mathrm{sk7}(\mathit{X})) \)
cnf_transformation [ 6 ]
25
plain
\( \mathrm{plant}(\mathrm{sk7}(\mathrm{sk5})) \)
resolution [ 23, 24 ]
26
plain
\( \mathrm{bird}(\mathrm{sk3}) \)
cnf_transformation [ 7 ]
27
plain
\( \neg \mathrm{snail}(\mathit{X}) \lor \mathrm{eats}(\mathit{X}, \mathrm{sk7}(\mathit{X})) \)
cnf_transformation [ 6 ]
28
plain
\( \neg \mathrm{bird}(\mathit{Y}) \lor \neg \mathrm{snail}(\mathit{X}) \lor \mathrm{much\_smaller}(\mathit{X}, \mathit{Y}) \)
cnf_transformation [ 8 ]
29
plain
\( \neg \mathrm{animal}(\mathit{X}) \lor \neg \mathrm{plant}(\mathit{Y}) \lor \mathrm{eats}(\mathit{X}, \mathit{Y}) \lor \neg \mathrm{animal}(\mathit{Y1}) \lor \neg \mathrm{much\_smaller}(\mathit{Y1}, \mathit{X}) \lor \neg \mathrm{plant}(\mathit{Z}) \lor \neg \mathrm{eats}(\mathit{Y1}, \mathit{Z}) \lor \mathrm{eats}(\mathit{X}, \mathit{Y1}) \)
cnf_transformation [ 9 ]
30
plain
\( \neg \mathrm{bird}(\mathit{V34}) \lor \neg \mathrm{snail}(\mathit{V35}) \lor \neg \mathrm{animal}(\mathit{V34}) \lor \neg \mathrm{plant}(\mathit{V36}) \lor \mathrm{eats}(\mathit{V34}, \mathit{V36}) \lor \neg \mathrm{animal}(\mathit{V35}) \lor \neg \mathrm{plant}(\mathit{V37}) \lor \neg \mathrm{eats}(\mathit{V35}, \mathit{V37}) \lor \mathrm{eats}(\mathit{V34}, \mathit{V35}) \)
resolution [ 28, 29 ]
31
plain
\( \neg \mathrm{snail}(\mathit{V75}) \lor \neg \mathrm{bird}(\mathit{V76}) \lor \neg \mathrm{snail}(\mathit{V75}) \lor \neg \mathrm{animal}(\mathit{V76}) \lor \neg \mathrm{plant}(\mathit{V77}) \lor \mathrm{eats}(\mathit{V76}, \mathit{V77}) \lor \neg \mathrm{animal}(\mathit{V75}) \lor \neg \mathrm{plant}(\mathrm{sk7}(\mathit{V75})) \lor \mathrm{eats}(\mathit{V76}, \mathit{V75}) \)
resolution [ 27, 30 ]
32
plain
\( \neg \mathrm{snail}(\mathit{V75}) \lor \neg \mathrm{bird}(\mathit{V76}) \lor \neg \mathrm{animal}(\mathit{V76}) \lor \neg \mathrm{plant}(\mathit{V77}) \lor \mathrm{eats}(\mathit{V76}, \mathit{V77}) \lor \neg \mathrm{animal}(\mathit{V75}) \lor \neg \mathrm{plant}(\mathrm{sk7}(\mathit{V75})) \lor \mathrm{eats}(\mathit{V76}, \mathit{V75}) \)
deletion_of_duplicate_literals [ 31 ]
33
plain
\( \neg \mathrm{snail}(\mathrm{sk5}) \lor \neg \mathrm{bird}(\mathit{V105}) \lor \neg \mathrm{animal}(\mathit{V105}) \lor \neg \mathrm{plant}(\mathit{V106}) \lor \mathrm{eats}(\mathit{V105}, \mathit{V106}) \lor \neg \mathrm{animal}(\mathrm{sk5}) \lor \mathrm{eats}(\mathit{V105}, \mathrm{sk5}) \)
resolution [ 25, 32 ]
34
plain
\( \neg \mathrm{bird}(\mathit{V105}) \lor \neg \mathrm{animal}(\mathit{V105}) \lor \neg \mathrm{plant}(\mathit{V106}) \lor \mathrm{eats}(\mathit{V105}, \mathit{V106}) \lor \neg \mathrm{animal}(\mathrm{sk5}) \lor \mathrm{eats}(\mathit{V105}, \mathrm{sk5}) \)
predicate_unit_simplification [ 33, 23 ]
35
plain
\( \neg \mathrm{snail}(\mathit{X}) \lor \mathrm{animal}(\mathit{X}) \)
cnf_transformation [ 10 ]
36
plain
\( \mathrm{animal}(\mathrm{sk5}) \)
resolution [ 23, 35 ]
37
plain
\( \neg \mathrm{bird}(\mathit{V105}) \lor \neg \mathrm{animal}(\mathit{V105}) \lor \neg \mathrm{plant}(\mathit{V106}) \lor \mathrm{eats}(\mathit{V105}, \mathit{V106}) \lor \mathrm{eats}(\mathit{V105}, \mathrm{sk5}) \)
predicate_unit_simplification [ 34, 36 ]
38
plain
\( \neg \mathrm{animal}(\mathrm{sk3}) \lor \neg \mathrm{plant}(\mathit{V110}) \lor \mathrm{eats}(\mathrm{sk3}, \mathit{V110}) \lor \mathrm{eats}(\mathrm{sk3}, \mathrm{sk5}) \)
resolution [ 26, 37 ]
39
plain
\( \neg \mathrm{bird}(\mathit{X}) \lor \mathrm{animal}(\mathit{X}) \)
cnf_transformation [ 11 ]
40
plain
\( \mathrm{animal}(\mathrm{sk3}) \)
resolution [ 26, 39 ]
41
plain
\( \neg \mathrm{plant}(\mathit{V110}) \lor \mathrm{eats}(\mathrm{sk3}, \mathit{V110}) \lor \mathrm{eats}(\mathrm{sk3}, \mathrm{sk5}) \)
predicate_unit_simplification [ 38, 40 ]
42
plain
\( \mathrm{eats}(\mathrm{sk3}, \mathrm{sk7}(\mathrm{sk5})) \lor \mathrm{eats}(\mathrm{sk3}, \mathrm{sk5}) \)
resolution [ 25, 41 ]
43
plain
\( \neg \mathrm{bird}(\mathit{X}) \lor \neg \mathrm{fox}(\mathit{Y}) \lor \mathrm{much\_smaller}(\mathit{X}, \mathit{Y}) \)
cnf_transformation [ 12 ]
44
plain
\( \neg \mathrm{bird}(\mathit{V42}) \lor \neg \mathrm{fox}(\mathit{V43}) \lor \neg \mathrm{animal}(\mathit{V43}) \lor \neg \mathrm{plant}(\mathit{V44}) \lor \mathrm{eats}(\mathit{V43}, \mathit{V44}) \lor \neg \mathrm{animal}(\mathit{V42}) \lor \neg \mathrm{plant}(\mathit{V45}) \lor \neg \mathrm{eats}(\mathit{V42}, \mathit{V45}) \lor \mathrm{eats}(\mathit{V43}, \mathit{V42}) \)
resolution [ 43, 29 ]
45
plain
\( \mathrm{eats}(\mathrm{sk3}, \mathrm{sk5}) \lor \neg \mathrm{bird}(\mathrm{sk3}) \lor \neg \mathrm{fox}(\mathit{V127}) \lor \neg \mathrm{animal}(\mathit{V127}) \lor \neg \mathrm{plant}(\mathit{V128}) \lor \mathrm{eats}(\mathit{V127}, \mathit{V128}) \lor \neg \mathrm{animal}(\mathrm{sk3}) \lor \neg \mathrm{plant}(\mathrm{sk7}(\mathrm{sk5})) \lor \mathrm{eats}(\mathit{V127}, \mathrm{sk3}) \)
resolution [ 42, 44 ]
46
plain
\( \mathrm{eats}(\mathrm{sk3}, \mathrm{sk5}) \lor \neg \mathrm{fox}(\mathit{V127}) \lor \neg \mathrm{animal}(\mathit{V127}) \lor \neg \mathrm{plant}(\mathit{V128}) \lor \mathrm{eats}(\mathit{V127}, \mathit{V128}) \lor \neg \mathrm{animal}(\mathrm{sk3}) \lor \neg \mathrm{plant}(\mathrm{sk7}(\mathrm{sk5})) \lor \mathrm{eats}(\mathit{V127}, \mathrm{sk3}) \)
predicate_unit_simplification [ 45, 26 ]
47
plain
\( \mathrm{eats}(\mathrm{sk3}, \mathrm{sk5}) \lor \neg \mathrm{fox}(\mathit{V127}) \lor \neg \mathrm{animal}(\mathit{V127}) \lor \neg \mathrm{plant}(\mathit{V128}) \lor \mathrm{eats}(\mathit{V127}, \mathit{V128}) \lor \neg \mathrm{plant}(\mathrm{sk7}(\mathrm{sk5})) \lor \mathrm{eats}(\mathit{V127}, \mathrm{sk3}) \)
predicate_unit_simplification [ 46, 40 ]
48
plain
\( \mathrm{eats}(\mathrm{sk3}, \mathrm{sk5}) \lor \neg \mathrm{fox}(\mathit{V127}) \lor \neg \mathrm{animal}(\mathit{V127}) \lor \neg \mathrm{plant}(\mathit{V128}) \lor \mathrm{eats}(\mathit{V127}, \mathit{V128}) \lor \mathrm{eats}(\mathit{V127}, \mathrm{sk3}) \)
predicate_unit_simplification [ 47, 25 ]
49
plain
\( \mathrm{eats}(\mathrm{sk3}, \mathrm{sk5}) \lor \neg \mathrm{animal}(\mathrm{sk2}) \lor \neg \mathrm{plant}(\mathit{V245}) \lor \mathrm{eats}(\mathrm{sk2}, \mathit{V245}) \lor \mathrm{eats}(\mathrm{sk2}, \mathrm{sk3}) \)
resolution [ 22, 48 ]
50
plain
\( \neg \mathrm{fox}(\mathit{X}) \lor \mathrm{animal}(\mathit{X}) \)
cnf_transformation [ 13 ]
51
plain
\( \mathrm{animal}(\mathrm{sk2}) \)
resolution [ 22, 50 ]
52
plain
\( \mathrm{eats}(\mathrm{sk3}, \mathrm{sk5}) \lor \neg \mathrm{plant}(\mathit{V245}) \lor \mathrm{eats}(\mathrm{sk2}, \mathit{V245}) \lor \mathrm{eats}(\mathrm{sk2}, \mathrm{sk3}) \)
predicate_unit_simplification [ 49, 51 ]
53
plain
\( \neg \mathrm{grain}(\mathit{V246}) \lor \mathrm{eats}(\mathrm{sk3}, \mathrm{sk5}) \lor \mathrm{eats}(\mathrm{sk2}, \mathit{V246}) \lor \mathrm{eats}(\mathrm{sk2}, \mathrm{sk3}) \)
resolution [ 20, 52 ]
54
plain
\( \mathrm{eats}(\mathrm{sk3}, \mathrm{sk5}) \lor \mathrm{eats}(\mathrm{sk2}, \mathrm{sk6}) \lor \mathrm{eats}(\mathrm{sk2}, \mathrm{sk3}) \)
resolution [ 19, 53 ]
55
plain
\( \neg \mathrm{bird}(\mathit{X}) \lor \neg \mathrm{snail}(\mathit{Y}) \lor \neg \mathrm{eats}(\mathit{X}, \mathit{Y}) \)
cnf_transformation [ 14 ]
56
plain
\( \mathrm{eats}(\mathrm{sk2}, \mathrm{sk6}) \lor \mathrm{eats}(\mathrm{sk2}, \mathrm{sk3}) \lor \neg \mathrm{bird}(\mathrm{sk3}) \lor \neg \mathrm{snail}(\mathrm{sk5}) \)
resolution [ 54, 55 ]
57
plain
\( \mathrm{eats}(\mathrm{sk2}, \mathrm{sk6}) \lor \mathrm{eats}(\mathrm{sk2}, \mathrm{sk3}) \lor \neg \mathrm{snail}(\mathrm{sk5}) \)
predicate_unit_simplification [ 56, 26 ]
58
plain
\( \mathrm{eats}(\mathrm{sk2}, \mathrm{sk6}) \lor \mathrm{eats}(\mathrm{sk2}, \mathrm{sk3}) \)
predicate_unit_simplification [ 57, 23 ]
59
plain
\( \neg \mathrm{fox}(\mathit{X}) \lor \neg \mathrm{wolf}(\mathit{Y}) \lor \mathrm{much\_smaller}(\mathit{X}, \mathit{Y}) \)
cnf_transformation [ 15 ]
60
plain
\( \neg \mathrm{fox}(\mathit{V46}) \lor \neg \mathrm{wolf}(\mathit{V47}) \lor \neg \mathrm{animal}(\mathit{V47}) \lor \neg \mathrm{plant}(\mathit{V48}) \lor \mathrm{eats}(\mathit{V47}, \mathit{V48}) \lor \neg \mathrm{animal}(\mathit{V46}) \lor \neg \mathrm{plant}(\mathit{V49}) \lor \neg \mathrm{eats}(\mathit{V46}, \mathit{V49}) \lor \mathrm{eats}(\mathit{V47}, \mathit{V46}) \)
resolution [ 59, 29 ]
61
plain
\( \mathrm{eats}(\mathrm{sk2}, \mathrm{sk3}) \lor \neg \mathrm{fox}(\mathrm{sk2}) \lor \neg \mathrm{wolf}(\mathit{V270}) \lor \neg \mathrm{animal}(\mathit{V270}) \lor \neg \mathrm{plant}(\mathit{V271}) \lor \mathrm{eats}(\mathit{V270}, \mathit{V271}) \lor \neg \mathrm{animal}(\mathrm{sk2}) \lor \neg \mathrm{plant}(\mathrm{sk6}) \lor \mathrm{eats}(\mathit{V270}, \mathrm{sk2}) \)
resolution [ 58, 60 ]
62
plain
\( \mathrm{eats}(\mathrm{sk2}, \mathrm{sk3}) \lor \neg \mathrm{wolf}(\mathit{V270}) \lor \neg \mathrm{animal}(\mathit{V270}) \lor \neg \mathrm{plant}(\mathit{V271}) \lor \mathrm{eats}(\mathit{V270}, \mathit{V271}) \lor \neg \mathrm{animal}(\mathrm{sk2}) \lor \neg \mathrm{plant}(\mathrm{sk6}) \lor \mathrm{eats}(\mathit{V270}, \mathrm{sk2}) \)
predicate_unit_simplification [ 61, 22 ]
63
plain
\( \mathrm{eats}(\mathrm{sk2}, \mathrm{sk3}) \lor \neg \mathrm{wolf}(\mathit{V270}) \lor \neg \mathrm{animal}(\mathit{V270}) \lor \neg \mathrm{plant}(\mathit{V271}) \lor \mathrm{eats}(\mathit{V270}, \mathit{V271}) \lor \neg \mathrm{plant}(\mathrm{sk6}) \lor \mathrm{eats}(\mathit{V270}, \mathrm{sk2}) \)
predicate_unit_simplification [ 62, 51 ]
64
plain
\( \neg \mathrm{grain}(\mathrm{sk6}) \lor \mathrm{eats}(\mathrm{sk2}, \mathrm{sk3}) \lor \neg \mathrm{wolf}(\mathit{V321}) \lor \neg \mathrm{animal}(\mathit{V321}) \lor \neg \mathrm{plant}(\mathit{V322}) \lor \mathrm{eats}(\mathit{V321}, \mathit{V322}) \lor \mathrm{eats}(\mathit{V321}, \mathrm{sk2}) \)
resolution [ 20, 63 ]
65
plain
\( \mathrm{eats}(\mathrm{sk2}, \mathrm{sk3}) \lor \neg \mathrm{wolf}(\mathit{V321}) \lor \neg \mathrm{animal}(\mathit{V321}) \lor \neg \mathrm{plant}(\mathit{V322}) \lor \mathrm{eats}(\mathit{V321}, \mathit{V322}) \lor \mathrm{eats}(\mathit{V321}, \mathrm{sk2}) \)
predicate_unit_simplification [ 64, 19 ]
66
plain
\( \mathrm{eats}(\mathrm{sk2}, \mathrm{sk3}) \lor \neg \mathrm{animal}(\mathrm{sk1}) \lor \neg \mathrm{plant}(\mathit{V323}) \lor \mathrm{eats}(\mathrm{sk1}, \mathit{V323}) \lor \mathrm{eats}(\mathrm{sk1}, \mathrm{sk2}) \)
resolution [ 21, 65 ]
67
plain
\( \neg \mathrm{wolf}(\mathit{X}) \lor \mathrm{animal}(\mathit{X}) \)
cnf_transformation [ 16 ]
68
plain
\( \mathrm{animal}(\mathrm{sk1}) \)
resolution [ 21, 67 ]
69
plain
\( \mathrm{eats}(\mathrm{sk2}, \mathrm{sk3}) \lor \neg \mathrm{plant}(\mathit{V323}) \lor \mathrm{eats}(\mathrm{sk1}, \mathit{V323}) \lor \mathrm{eats}(\mathrm{sk1}, \mathrm{sk2}) \)
predicate_unit_simplification [ 66, 68 ]
70
plain
\( \neg \mathrm{grain}(\mathit{V324}) \lor \mathrm{eats}(\mathrm{sk2}, \mathrm{sk3}) \lor \mathrm{eats}(\mathrm{sk1}, \mathit{V324}) \lor \mathrm{eats}(\mathrm{sk1}, \mathrm{sk2}) \)
resolution [ 20, 69 ]
71
plain
\( \mathrm{eats}(\mathrm{sk2}, \mathrm{sk3}) \lor \mathrm{eats}(\mathrm{sk1}, \mathrm{sk6}) \lor \mathrm{eats}(\mathrm{sk1}, \mathrm{sk2}) \)
resolution [ 19, 70 ]
72
plain
\( \neg \mathrm{grain}(\mathit{V121}) \lor \mathrm{eats}(\mathrm{sk3}, \mathit{V121}) \lor \mathrm{eats}(\mathrm{sk3}, \mathrm{sk5}) \)
resolution [ 20, 41 ]
73
plain
\( \mathrm{eats}(\mathrm{sk3}, \mathrm{sk6}) \lor \mathrm{eats}(\mathrm{sk3}, \mathrm{sk5}) \)
resolution [ 19, 72 ]
74
negated_conjecture
\( \neg \exists \mathit{X}\, \exists \mathit{Y}\, \left(\mathrm{animal}(\mathit{X}) \land \mathrm{animal}(\mathit{Y}) \land \exists \mathit{Z}\, \left(\mathrm{grain}(\mathit{Z}) \land \mathrm{eats}(\mathit{Y}, \mathit{Z}) \land \mathrm{eats}(\mathit{X}, \mathit{Y})\right)\right) \)
negate_conjecture [ 17 ]
75
plain
\( \neg \mathrm{animal}(\mathit{X}) \lor \neg \mathrm{animal}(\mathit{Y}) \lor \neg \mathrm{grain}(\mathit{Z}) \lor \neg \mathrm{eats}(\mathit{Y}, \mathit{Z}) \lor \neg \mathrm{eats}(\mathit{X}, \mathit{Y}) \)
cnf_transformation [ 74 ]
76
plain
\( \mathrm{eats}(\mathrm{sk3}, \mathrm{sk5}) \lor \neg \mathrm{animal}(\mathit{V142}) \lor \neg \mathrm{animal}(\mathrm{sk3}) \lor \neg \mathrm{grain}(\mathrm{sk6}) \lor \neg \mathrm{eats}(\mathit{V142}, \mathrm{sk3}) \)
resolution [ 73, 75 ]
77
plain
\( \mathrm{eats}(\mathrm{sk3}, \mathrm{sk5}) \lor \neg \mathrm{animal}(\mathit{V142}) \lor \neg \mathrm{animal}(\mathrm{sk3}) \lor \neg \mathrm{eats}(\mathit{V142}, \mathrm{sk3}) \)
predicate_unit_simplification [ 76, 19 ]
78
plain
\( \mathrm{eats}(\mathrm{sk3}, \mathrm{sk5}) \lor \neg \mathrm{animal}(\mathit{V142}) \lor \neg \mathrm{eats}(\mathit{V142}, \mathrm{sk3}) \)
predicate_unit_simplification [ 77, 40 ]
79
plain
\( \mathrm{eats}(\mathrm{sk1}, \mathrm{sk6}) \lor \mathrm{eats}(\mathrm{sk1}, \mathrm{sk2}) \lor \mathrm{eats}(\mathrm{sk3}, \mathrm{sk5}) \lor \neg \mathrm{animal}(\mathrm{sk2}) \)
resolution [ 71, 78 ]
80
plain
\( \mathrm{eats}(\mathrm{sk1}, \mathrm{sk6}) \lor \mathrm{eats}(\mathrm{sk1}, \mathrm{sk2}) \lor \mathrm{eats}(\mathrm{sk3}, \mathrm{sk5}) \)
predicate_unit_simplification [ 79, 51 ]
81
plain
\( \mathrm{eats}(\mathrm{sk1}, \mathrm{sk6}) \lor \mathrm{eats}(\mathrm{sk1}, \mathrm{sk2}) \lor \neg \mathrm{bird}(\mathrm{sk3}) \lor \neg \mathrm{snail}(\mathrm{sk5}) \)
resolution [ 80, 55 ]
82
plain
\( \mathrm{eats}(\mathrm{sk1}, \mathrm{sk6}) \lor \mathrm{eats}(\mathrm{sk1}, \mathrm{sk2}) \lor \neg \mathrm{snail}(\mathrm{sk5}) \)
predicate_unit_simplification [ 81, 26 ]
83
plain
\( \mathrm{eats}(\mathrm{sk1}, \mathrm{sk6}) \lor \mathrm{eats}(\mathrm{sk1}, \mathrm{sk2}) \)
predicate_unit_simplification [ 82, 23 ]
84
plain
\( \neg \mathrm{wolf}(\mathit{X}) \lor \neg \mathrm{grain}(\mathit{Y}) \lor \neg \mathrm{eats}(\mathit{X}, \mathit{Y}) \)
cnf_transformation [ 18 ]
85
plain
\( \mathrm{eats}(\mathrm{sk1}, \mathrm{sk2}) \lor \neg \mathrm{wolf}(\mathrm{sk1}) \lor \neg \mathrm{grain}(\mathrm{sk6}) \)
resolution [ 83, 84 ]
86
plain
\( \mathrm{eats}(\mathrm{sk1}, \mathrm{sk2}) \lor \neg \mathrm{grain}(\mathrm{sk6}) \)
predicate_unit_simplification [ 85, 21 ]
87
plain
\( \mathrm{eats}(\mathrm{sk1}, \mathrm{sk2}) \)
predicate_unit_simplification [ 86, 19 ]
88
plain
\( \neg \mathrm{wolf}(\mathit{X}) \lor \neg \mathrm{fox}(\mathit{Y}) \lor \neg \mathrm{eats}(\mathit{X}, \mathit{Y}) \)
cnf_transformation [ 18 ]
89
plain
\( \neg \mathrm{wolf}(\mathrm{sk1}) \lor \neg \mathrm{fox}(\mathrm{sk2}) \)
resolution [ 87, 88 ]
90
plain
\( \neg \mathrm{fox}(\mathrm{sk2}) \)
predicate_unit_simplification [ 89, 21 ]
91
plain
\( \bot \)
predicate_unit_simplification [ 90, 22 ]