Proof
1
axiom
\( \exists \mathit{X}\, \left(\mathrm{lives}(\mathit{X}) \land \mathrm{killed}(\mathit{X}, \mathrm{agatha})\right) \)
pel55_1  |  Problems/PUZ/PUZ001+1.p
2
axiom
\( \forall \mathit{X}\, \left(\mathrm{lives}(\mathit{X}) \to \mathit{X} = \mathrm{agatha} \lor \mathit{X} = \mathrm{butler} \lor \mathit{X} = \mathrm{charles}\right) \)
pel55_3  |  Problems/PUZ/PUZ001+1.p
3
axiom
\( \forall \mathit{X}\, \forall \mathit{Y}\, \left(\mathrm{killed}(\mathit{X}, \mathit{Y}) \to \mathrm{hates}(\mathit{X}, \mathit{Y})\right) \)
pel55_4  |  Problems/PUZ/PUZ001+1.p
4
axiom
\( \forall \mathit{X}\, \left(\neg \left(\mathit{X} = \mathrm{butler}\right) \to \mathrm{hates}(\mathrm{agatha}, \mathit{X})\right) \)
pel55_7  |  Problems/PUZ/PUZ001+1.p
5
axiom
\( \forall \mathit{X}\, \left(\mathrm{hates}(\mathrm{agatha}, \mathit{X}) \to \neg \mathrm{hates}(\mathrm{charles}, \mathit{X})\right) \)
pel55_6  |  Problems/PUZ/PUZ001+1.p
6
axiom
\( \neg \left(\mathrm{agatha} = \mathrm{butler}\right) \)
pel55_11  |  Problems/PUZ/PUZ001+1.p
7
axiom
\( \forall \mathit{X}\, \left(\neg \mathrm{richer}(\mathit{X}, \mathrm{agatha}) \to \mathrm{hates}(\mathrm{butler}, \mathit{X})\right) \)
pel55_8  |  Problems/PUZ/PUZ001+1.p
8
axiom
\( \forall \mathit{X}\, \forall \mathit{Y}\, \left(\mathrm{killed}(\mathit{X}, \mathit{Y}) \to \neg \mathrm{richer}(\mathit{X}, \mathit{Y})\right) \)
pel55_5  |  Problems/PUZ/PUZ001+1.p
9
axiom
\( \forall \mathit{X}\, \left(\mathrm{hates}(\mathrm{agatha}, \mathit{X}) \to \mathrm{hates}(\mathrm{butler}, \mathit{X})\right) \)
pel55_9  |  Problems/PUZ/PUZ001+1.p
10
axiom
\( \forall \mathit{X}\, \exists \mathit{Y}\, \neg \mathrm{hates}(\mathit{X}, \mathit{Y}) \)
pel55_10  |  Problems/PUZ/PUZ001+1.p
11
conjecture
\( \mathrm{killed}(\mathrm{agatha}, \mathrm{agatha}) \)
pel55  |  Problems/PUZ/PUZ001+1.p
12
plain
\( \mathrm{killed}(\mathrm{sk1}, \mathrm{agatha}) \)
cnf_transformation [ 1 ]
13
plain
\( \mathrm{lives}(\mathrm{sk1}) \)
cnf_transformation [ 1 ]
14
plain
\( \neg \mathrm{lives}(\mathit{X}) \lor \mathit{X} = \mathrm{agatha} \lor \mathit{X} = \mathrm{butler} \lor \mathit{X} = \mathrm{charles} \)
cnf_transformation [ 2 ]
15
plain
\( \mathrm{sk1} = \mathrm{agatha} \lor \mathrm{sk1} = \mathrm{butler} \lor \mathrm{sk1} = \mathrm{charles} \)
resolution [ 13, 14 ]
16
plain
\( \neg \mathrm{killed}(\mathit{X}, \mathit{Y}) \lor \mathrm{hates}(\mathit{X}, \mathit{Y}) \)
cnf_transformation [ 3 ]
17
plain
\( \mathrm{hates}(\mathrm{sk1}, \mathrm{agatha}) \)
resolution [ 12, 16 ]
18
plain
\( \mathrm{sk1} = \mathrm{agatha} \lor \mathrm{sk1} = \mathrm{butler} \lor \mathrm{hates}(\mathrm{charles}, \mathrm{agatha}) \)
superposition [ 15, 17 ]
19
plain
\( \mathit{X} = \mathrm{butler} \lor \mathrm{hates}(\mathrm{agatha}, \mathit{X}) \)
cnf_transformation [ 4 ]
20
plain
\( \neg \mathrm{hates}(\mathrm{agatha}, \mathit{X}) \lor \neg \mathrm{hates}(\mathrm{charles}, \mathit{X}) \)
cnf_transformation [ 5 ]
21
plain
\( \mathit{V11} = \mathrm{butler} \lor \neg \mathrm{hates}(\mathrm{charles}, \mathit{V11}) \)
resolution [ 19, 20 ]
22
plain
\( \mathrm{sk1} = \mathrm{agatha} \lor \mathrm{sk1} = \mathrm{butler} \lor \mathrm{agatha} = \mathrm{butler} \)
resolution [ 18, 21 ]
23
plain
\( \neg \left(\mathrm{agatha} = \mathrm{butler}\right) \)
cnf_transformation [ 6 ]
24
plain
\( \mathrm{sk1} = \mathrm{agatha} \lor \mathrm{sk1} = \mathrm{butler} \)
negative_simplify-reflect [ 22, 23 ]
25
plain
\( \mathrm{richer}(\mathit{X}, \mathrm{agatha}) \lor \mathrm{hates}(\mathrm{butler}, \mathit{X}) \)
cnf_transformation [ 7 ]
26
plain
\( \neg \mathrm{killed}(\mathit{X}, \mathit{Y}) \lor \neg \mathrm{richer}(\mathit{X}, \mathit{Y}) \)
cnf_transformation [ 8 ]
27
plain
\( \neg \mathrm{richer}(\mathrm{sk1}, \mathrm{agatha}) \)
resolution [ 12, 26 ]
28
plain
\( \mathrm{hates}(\mathrm{butler}, \mathrm{sk1}) \)
resolution [ 25, 27 ]
29
plain
\( \mathrm{sk1} = \mathrm{agatha} \lor \mathrm{hates}(\mathrm{butler}, \mathrm{butler}) \)
superposition [ 24, 28 ]
30
plain
\( \neg \mathrm{hates}(\mathrm{agatha}, \mathit{X}) \lor \mathrm{hates}(\mathrm{butler}, \mathit{X}) \)
cnf_transformation [ 9 ]
31
plain
\( \neg \mathrm{hates}(\mathit{X}, \mathrm{sk2}(\mathit{X})) \)
cnf_transformation [ 10 ]
32
plain
\( \neg \mathrm{hates}(\mathrm{agatha}, \mathrm{sk2}(\mathrm{butler})) \)
resolution [ 30, 31 ]
33
plain
\( \mathrm{sk2}(\mathrm{butler}) = \mathrm{butler} \)
resolution [ 19, 32 ]
34
plain
\( \neg \mathrm{hates}(\mathrm{butler}, \mathrm{butler}) \)
superposition [ 33, 31 ]
35
plain
\( \mathrm{sk1} = \mathrm{agatha} \)
predicate_unit_simplification [ 29, 34 ]
36
plain
\( \mathrm{killed}(\mathrm{agatha}, \mathrm{agatha}) \)
demodulation [ 12, 35 ]
37
negated_conjecture
\( \neg \mathrm{killed}(\mathrm{agatha}, \mathrm{agatha}) \)
negate_conjecture [ 11 ]
38
plain
\( \neg \mathrm{killed}(\mathrm{agatha}, \mathrm{agatha}) \)
cnf_transformation [ 37 ]
39
plain
\( \bot \)
predicate_unit_simplification [ 36, 38 ]