1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
|
; COMMAND-LINE: --finite-model-find --no-check-proofs --no-check-unsat-core
; EXPECT: unsat
;%------------------------------------------------------------------------------
;% File : PUZ001+1 : TPTP v5.4.0. Released v2.0.0.
;% Domain : Puzzles
;% Problem : Dreadbury Mansion
;% Version : Especial.
;% Theorem formulation : Reduced > Complete.
;% English : Someone who lives in Dreadbury Mansion killed Aunt Agatha.
;% Agatha, the butler, and Charles live in Dreadbury Mansion,
;% and are the only people who live therein. A killer always
;% hates his victim, and is never richer than his victim.
;% Charles hates no one that Aunt Agatha hates. Agatha hates
;% everyone except the butler. The butler hates everyone not
;% richer than Aunt Agatha. The butler hates everyone Aunt
;% Agatha hates. No one hates everyone. Agatha is not the
;% butler. Therefore : Agatha killed herself.
;% Refs : [Pel86] Pelletier (1986), Seventy-five Problems for Testing Au
;% : [Hah94] Haehnle (1994), Email to G. Sutcliffe
;% Source : [Hah94]
;% Names : Pelletier 55 [Pel86]
;% Status : Theorem
;% Rating : 0.07 v5.3.0, 0.19 v5.2.0, 0.00 v5.0.0, 0.08 v4.1.0, 0.13 v4.0.0, 0.12 v3.7.0, 0.14 v3.5.0, 0.00 v3.4.0, 0.08 v3.3.0, 0.11 v3.2.0, 0.22 v3.1.0, 0.17 v2.7.0, 0.00 v2.5.0, 0.33 v2.4.0, 0.33 v2.2.1, 0.00 v2.1.0
;% Syntax : Number of formulae : 14 ( 6 unit)
;% Number of atoms : 24 ( 5 equality)
;% Maximal formula depth : 5 ( 3 average)
;% Number of connectives : 16 ( 6 ~; 2 |; 1 &)
;% ( 0 <=>; 7 =>; 0 <=; 0 <~>)
;% ( 0 ~|; 0 ~&)
;% Number of predicates : 5 ( 0 propositional; 1-2 arity)
;% Number of functors : 3 ( 3 constant; 0-0 arity)
;% Number of variables : 12 ( 0 sgn; 10 !; 2 ?)
;% Maximal term depth : 1 ( 1 average)
;% SPC : FOF_THM_RFO_SEQ
;% Comments : Modified by Geoff Sutcliffe.
;% : Also known as "Who killed Aunt Agatha"
;%------------------------------------------------------------------------------
;%----Problem axioms
(set-logic UF)
(set-info :status unsat)
(declare-sort sort__smt2 0)
; functions
(declare-fun agatha__smt2_0 ( ) sort__smt2)
(declare-fun butler__smt2_0 ( ) sort__smt2)
(declare-fun charles__smt2_0 ( ) sort__smt2)
; predicates
(declare-fun lives__smt2_1 ( sort__smt2 ) Bool)
(declare-fun killed__smt2_2 ( sort__smt2 sort__smt2 ) Bool)
(declare-fun hates__smt2_2 ( sort__smt2 sort__smt2 ) Bool)
(declare-fun richer__smt2_2 ( sort__smt2 sort__smt2 ) Bool)
; pel55_1 axiom
(assert (exists ((?X sort__smt2))
(and (lives__smt2_1 ?X)
(killed__smt2_2 ?X agatha__smt2_0))))
; pel55_2_1 axiom
(assert (lives__smt2_1 agatha__smt2_0))
; pel55_2_2 axiom
(assert (lives__smt2_1 butler__smt2_0))
; pel55_2_3 axiom
(assert (lives__smt2_1 charles__smt2_0))
; pel55_3 axiom
(assert (forall ((?X sort__smt2))
(=> (lives__smt2_1 ?X)
(or (= ?X agatha__smt2_0)
(= ?X butler__smt2_0)
(= ?X charles__smt2_0)))))
; pel55_4 axiom
(assert (forall ((?X sort__smt2) (?Y sort__smt2))
(=> (killed__smt2_2 ?X ?Y)
(hates__smt2_2 ?X ?Y))))
; pel55_5 axiom
(assert (forall ((?X sort__smt2) (?Y sort__smt2))
(=> (killed__smt2_2 ?X ?Y)
(not (richer__smt2_2 ?X ?Y)))))
; pel55_6 axiom
(assert (forall ((?X sort__smt2))
(=> (hates__smt2_2 agatha__smt2_0 ?X)
(not (hates__smt2_2 charles__smt2_0 ?X)))))
; pel55_7 axiom
(assert (forall ((?X sort__smt2))
(=> (not (= ?X butler__smt2_0))
(hates__smt2_2 agatha__smt2_0 ?X))))
; pel55_8 axiom
(assert (forall ((?X sort__smt2))
(=> (not (richer__smt2_2 ?X agatha__smt2_0))
(hates__smt2_2 butler__smt2_0 ?X))))
; pel55_9 axiom
(assert (forall ((?X sort__smt2))
(=> (hates__smt2_2 agatha__smt2_0 ?X)
(hates__smt2_2 butler__smt2_0 ?X))))
; pel55_10 axiom
(assert (forall ((?X sort__smt2))
(exists ((?Y sort__smt2)) (not (hates__smt2_2 ?X ?Y)))))
; pel55_11 axiom
(assert (not (= agatha__smt2_0 butler__smt2_0)))
;----This is the conjecture with negated conjecture
; pel55 conjecture
(assert (not (killed__smt2_2 agatha__smt2_0 agatha__smt2_0)))
(check-sat)
|
