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
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
|
(PROOF-CHECKER-ARRAY::IS-UNIT-CLAUSE
(13 1 (:REWRITE PROOF-CHECKER-ARRAY::ASSIGNMENTP-LITERALP-MEMBER))
(8 1 (:DEFINITION MEMBER-EQUAL))
(5 5 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
(3 1 (:REWRITE PROOF-CHECKER-ARRAY::ASSIGNMENTP-CONJUNCTION))
(2 2 (:REWRITE PROOF-CHECKER-ARRAY::SUBSETP-MEMBER-IMPLIES-MEMBER))
(2 2 (:REWRITE PROOF-CHECKER-ARRAY::MEMBER-UNION-VARIABLES1))
(2 2 (:REWRITE DEFAULT-CAR))
(1 1 (:REWRITE PROOF-CHECKER-ARRAY::LITERAL-LISTP-IMPLIES-LITERALP-MEMBER))
(1 1 (:REWRITE DEFAULT-CDR))
(1 1 (:REWRITE PROOF-CHECKER-ARRAY::CLAUSEP-MEMBER))
)
(PROOF-CHECKER-ARRAY::LITERALP-IS-UNIT-CLAUSE
(812 14 (:DEFINITION PROOF-CHECKER-ARRAY::EVALUATE-CLAUSE))
(376 376 (:REWRITE PROOF-CHECKER-ARRAY::SUBSETP-MEMBER-IMPLIES-MEMBER))
(376 376 (:REWRITE PROOF-CHECKER-ARRAY::MEMBER-UNION-VARIABLES1))
(332 332 (:REWRITE DEFAULT-CAR))
(260 260 (:REWRITE DEFAULT-CDR))
(156 156 (:REWRITE PROOF-CHECKER-ARRAY::SUBSET-VARIABLESP-IMPLIES-MEMBER-OR-MEMBER-NEGATE))
(156 46 (:REWRITE PROOF-CHECKER-ARRAY::ASSIGNMENTP-CONJUNCTION))
(118 24 (:REWRITE PROOF-CHECKER-ARRAY::LITERAL-LISTP-IMPLIES-LITERALP-MEMBER))
(104 104 (:TYPE-PRESCRIPTION PROOF-CHECKER-ARRAY::ASSIGNMENTP))
(86 86 (:REWRITE PROOF-CHECKER-ARRAY::SET-EQUALP-IMPLIES-EQUAL-EVALUATE-LITERAL))
(24 24 (:REWRITE PROOF-CHECKER-ARRAY::CLAUSEP-MEMBER))
(24 24 (:REWRITE PROOF-CHECKER-ARRAY::ASSIGNMENTP-LITERALP-MEMBER))
(18 6 (:REWRITE PROOF-CHECKER-ARRAY::ASSIGNMENTP-CDR))
(15 15 (:REWRITE PROOF-CHECKER-ARRAY::SUBSET-VARIABLESP-NOT-SUBSETP-IMPLIES-NOT-NO-CONFLICTING-LITERALSP))
(15 15 (:REWRITE PROOF-CHECKER-ARRAY::NOT-NO-CONFLICTING-LITERALSP))
(14 14 (:REWRITE PROOF-CHECKER-ARRAY::SET-EQUALP-IMPLIES-EQUAL-EVALUATE-CLAUSE))
)
(PROOF-CHECKER-ARRAY::MEMBER-IS-UNIT-CLAUSE-CLAUSE
(1334 23 (:DEFINITION PROOF-CHECKER-ARRAY::EVALUATE-CLAUSE))
(497 497 (:REWRITE PROOF-CHECKER-ARRAY::SUBSETP-MEMBER-IMPLIES-MEMBER))
(497 497 (:REWRITE PROOF-CHECKER-ARRAY::MEMBER-UNION-VARIABLES1))
(409 409 (:REWRITE DEFAULT-CAR))
(294 294 (:REWRITE DEFAULT-CDR))
(196 196 (:REWRITE PROOF-CHECKER-ARRAY::SUBSET-VARIABLESP-IMPLIES-MEMBER-OR-MEMBER-NEGATE))
(134 134 (:REWRITE PROOF-CHECKER-ARRAY::SET-EQUALP-IMPLIES-EQUAL-EVALUATE-LITERAL))
(23 23 (:REWRITE PROOF-CHECKER-ARRAY::SET-EQUALP-IMPLIES-EQUAL-EVALUATE-CLAUSE))
)
(PROOF-CHECKER-ARRAY::NOT-MEMBER-IS-UNIT-CLAUSE-ASSIGNMENT
(812 14 (:DEFINITION PROOF-CHECKER-ARRAY::EVALUATE-CLAUSE))
(312 312 (:REWRITE PROOF-CHECKER-ARRAY::SUBSETP-MEMBER-IMPLIES-MEMBER))
(312 312 (:REWRITE PROOF-CHECKER-ARRAY::MEMBER-UNION-VARIABLES1))
(250 250 (:REWRITE DEFAULT-CAR))
(188 188 (:REWRITE DEFAULT-CDR))
(124 124 (:REWRITE PROOF-CHECKER-ARRAY::SUBSET-VARIABLESP-IMPLIES-MEMBER-OR-MEMBER-NEGATE))
(86 86 (:REWRITE PROOF-CHECKER-ARRAY::SET-EQUALP-IMPLIES-EQUAL-EVALUATE-LITERAL))
(14 14 (:REWRITE PROOF-CHECKER-ARRAY::SET-EQUALP-IMPLIES-EQUAL-EVALUATE-CLAUSE))
)
(PROOF-CHECKER-ARRAY::NOT-MEMBER-NEGATE-IS-UNIT-CLAUSE-ASSIGNMENT
(812 14 (:DEFINITION PROOF-CHECKER-ARRAY::EVALUATE-CLAUSE))
(312 312 (:REWRITE PROOF-CHECKER-ARRAY::SUBSETP-MEMBER-IMPLIES-MEMBER))
(312 312 (:REWRITE PROOF-CHECKER-ARRAY::MEMBER-UNION-VARIABLES1))
(250 250 (:REWRITE DEFAULT-CAR))
(188 188 (:REWRITE DEFAULT-CDR))
(140 140 (:REWRITE PROOF-CHECKER-ARRAY::SUBSET-VARIABLESP-IMPLIES-MEMBER-OR-MEMBER-NEGATE))
(86 86 (:REWRITE PROOF-CHECKER-ARRAY::SET-EQUALP-IMPLIES-EQUAL-EVALUATE-LITERAL))
(14 14 (:REWRITE PROOF-CHECKER-ARRAY::SET-EQUALP-IMPLIES-EQUAL-EVALUATE-CLAUSE))
)
(PROOF-CHECKER-ARRAY::MEMBER-IS-UNIT-CLAUSE-ALL-LITERALS)
(PROOF-CHECKER-ARRAY::IS-UNIT-CLAUSE-IMPLIES-UNDEFP-EVALUATE-CLAUSE
(208 208 (:REWRITE PROOF-CHECKER-ARRAY::SUBSETP-MEMBER-IMPLIES-MEMBER))
(208 208 (:REWRITE PROOF-CHECKER-ARRAY::MEMBER-UNION-VARIABLES1))
(169 169 (:REWRITE DEFAULT-CAR))
(116 116 (:REWRITE DEFAULT-CDR))
(86 86 (:REWRITE PROOF-CHECKER-ARRAY::SUBSET-VARIABLESP-IMPLIES-MEMBER-OR-MEMBER-NEGATE))
(61 61 (:REWRITE PROOF-CHECKER-ARRAY::SET-EQUALP-IMPLIES-EQUAL-EVALUATE-LITERAL))
(8 8 (:REWRITE PROOF-CHECKER-ARRAY::SET-EQUALP-IMPLIES-EQUAL-EVALUATE-CLAUSE))
)
(PROOF-CHECKER-ARRAY::FIND-UNIT-CLAUSE)
(PROOF-CHECKER-ARRAY::LITERALP-MV-NTH-0-FIND-UNIT-CLAUSE
(720 12 (:DEFINITION PROOF-CHECKER-ARRAY::EVALUATE-CLAUSE))
(552 132 (:REWRITE PROOF-CHECKER-ARRAY::TERNARYP-NOT-TRUE-NOT-UNDEF))
(516 96 (:REWRITE PROOF-CHECKER-ARRAY::TERNARYP-NOT-FALSE-NOT-UNDEF))
(293 66 (:REWRITE PROOF-CHECKER-ARRAY::ASSIGNMENTP-CONJUNCTION))
(241 241 (:REWRITE PROOF-CHECKER-ARRAY::SUBSETP-MEMBER-IMPLIES-MEMBER))
(241 241 (:REWRITE PROOF-CHECKER-ARRAY::MEMBER-UNION-VARIABLES1))
(237 237 (:REWRITE DEFAULT-CAR))
(222 222 (:REWRITE DEFAULT-CDR))
(194 194 (:TYPE-PRESCRIPTION PROOF-CHECKER-ARRAY::ASSIGNMENTP))
(192 96 (:REWRITE PROOF-CHECKER-ARRAY::TERNARYP-NOT-TRUE-NOT-FALSE))
(168 168 (:REWRITE PROOF-CHECKER-ARRAY::TERNARYP-EVALUATE-CLAUSE))
(144 72 (:REWRITE PROOF-CHECKER-ARRAY::FALSEP-IMPLIES-NOT-TRUEP))
(132 72 (:REWRITE PROOF-CHECKER-ARRAY::UNDEFP-IMPLIES-NOT-TRUEP))
(118 118 (:TYPE-PRESCRIPTION PROOF-CHECKER-ARRAY::NEGATE))
(118 118 (:REWRITE PROOF-CHECKER-ARRAY::SUBSET-VARIABLESP-IMPLIES-MEMBER-OR-MEMBER-NEGATE))
(99 33 (:REWRITE PROOF-CHECKER-ARRAY::ASSIGNMENTP-CDR))
(96 48 (:REWRITE PROOF-CHECKER-ARRAY::TRUEP-IMPLIES-NOT-FALSEP))
(96 48 (:REWRITE PROOF-CHECKER-ARRAY::FALSEP-IMPLIES-NOT-UNDEFP))
(84 48 (:REWRITE PROOF-CHECKER-ARRAY::UNDEFP-IMPLIES-NOT-FALSEP))
(48 48 (:REWRITE PROOF-CHECKER-ARRAY::SET-EQUALP-IMPLIES-EQUAL-EVALUATE-LITERAL))
(48 48 (:REWRITE PROOF-CHECKER-ARRAY::IS-UNIT-CLAUSE-IMPLIES-UNDEFP-EVALUATE-CLAUSE))
(36 36 (:REWRITE PROOF-CHECKER-ARRAY::TRUEP-IMPLIES-NOT-UNDEFP))
(23 11 (:REWRITE PROOF-CHECKER-ARRAY::FORMULAP-MEMBER))
(15 15 (:REWRITE PROOF-CHECKER-ARRAY::CLAUSEP-MEMBER))
(15 15 (:REWRITE PROOF-CHECKER-ARRAY::ASSIGNMENTP-LITERALP-MEMBER))
(12 12 (:REWRITE PROOF-CHECKER-ARRAY::SUBSET-VARIABLESP-NOT-SUBSETP-IMPLIES-NOT-NO-CONFLICTING-LITERALSP))
(12 12 (:REWRITE PROOF-CHECKER-ARRAY::SET-EQUALP-IMPLIES-EQUAL-EVALUATE-CLAUSE))
(12 12 (:REWRITE PROOF-CHECKER-ARRAY::NOT-NO-CONFLICTING-LITERALSP))
(8 2 (:REWRITE PROOF-CHECKER-ARRAY::FORMULAP-CDR))
)
(PROOF-CHECKER-ARRAY::CLAUSEP-MV-NTH-1-FIND-UNIT-CLAUSE
(1020 17 (:DEFINITION PROOF-CHECKER-ARRAY::EVALUATE-CLAUSE))
(782 187 (:REWRITE PROOF-CHECKER-ARRAY::TERNARYP-NOT-TRUE-NOT-UNDEF))
(731 136 (:REWRITE PROOF-CHECKER-ARRAY::TERNARYP-NOT-FALSE-NOT-UNDEF))
(541 122 (:REWRITE PROOF-CHECKER-ARRAY::ASSIGNMENTP-CONJUNCTION))
(370 370 (:REWRITE PROOF-CHECKER-ARRAY::SUBSETP-MEMBER-IMPLIES-MEMBER))
(370 370 (:REWRITE PROOF-CHECKER-ARRAY::MEMBER-UNION-VARIABLES1))
(366 366 (:REWRITE DEFAULT-CAR))
(358 358 (:TYPE-PRESCRIPTION PROOF-CHECKER-ARRAY::ASSIGNMENTP))
(357 357 (:REWRITE DEFAULT-CDR))
(272 136 (:REWRITE PROOF-CHECKER-ARRAY::TERNARYP-NOT-TRUE-NOT-FALSE))
(238 238 (:REWRITE PROOF-CHECKER-ARRAY::TERNARYP-EVALUATE-CLAUSE))
(204 102 (:REWRITE PROOF-CHECKER-ARRAY::FALSEP-IMPLIES-NOT-TRUEP))
(187 102 (:REWRITE PROOF-CHECKER-ARRAY::UNDEFP-IMPLIES-NOT-TRUEP))
(183 61 (:REWRITE PROOF-CHECKER-ARRAY::ASSIGNMENTP-CDR))
(178 178 (:TYPE-PRESCRIPTION PROOF-CHECKER-ARRAY::NEGATE))
(178 178 (:REWRITE PROOF-CHECKER-ARRAY::SUBSET-VARIABLESP-IMPLIES-MEMBER-OR-MEMBER-NEGATE))
(136 68 (:REWRITE PROOF-CHECKER-ARRAY::TRUEP-IMPLIES-NOT-FALSEP))
(136 68 (:REWRITE PROOF-CHECKER-ARRAY::FALSEP-IMPLIES-NOT-UNDEFP))
(119 68 (:REWRITE PROOF-CHECKER-ARRAY::UNDEFP-IMPLIES-NOT-FALSEP))
(78 19 (:REWRITE PROOF-CHECKER-ARRAY::FORMULAP-MEMBER))
(68 68 (:REWRITE PROOF-CHECKER-ARRAY::SET-EQUALP-IMPLIES-EQUAL-EVALUATE-LITERAL))
(68 68 (:REWRITE PROOF-CHECKER-ARRAY::IS-UNIT-CLAUSE-IMPLIES-UNDEFP-EVALUATE-CLAUSE))
(51 51 (:REWRITE PROOF-CHECKER-ARRAY::TRUEP-IMPLIES-NOT-UNDEFP))
(30 30 (:REWRITE PROOF-CHECKER-ARRAY::SUBSET-VARIABLESP-NOT-SUBSETP-IMPLIES-NOT-NO-CONFLICTING-LITERALSP))
(30 30 (:REWRITE PROOF-CHECKER-ARRAY::NOT-NO-CONFLICTING-LITERALSP))
(24 24 (:TYPE-PRESCRIPTION PROOF-CHECKER-ARRAY::LITERALP))
(21 21 (:REWRITE PROOF-CHECKER-ARRAY::CLAUSEP-MEMBER))
(21 21 (:REWRITE PROOF-CHECKER-ARRAY::ASSIGNMENTP-LITERALP-MEMBER))
(20 5 (:REWRITE PROOF-CHECKER-ARRAY::FORMULAP-CDR))
(17 17 (:REWRITE PROOF-CHECKER-ARRAY::SET-EQUALP-IMPLIES-EQUAL-EVALUATE-CLAUSE))
)
(PROOF-CHECKER-ARRAY::NOT-MEMBER-MV-NTH-0-FIND-UNIT-CLAUSE-ASSIGNMENT
(720 12 (:DEFINITION PROOF-CHECKER-ARRAY::EVALUATE-CLAUSE))
(552 132 (:REWRITE PROOF-CHECKER-ARRAY::TERNARYP-NOT-TRUE-NOT-UNDEF))
(516 96 (:REWRITE PROOF-CHECKER-ARRAY::TERNARYP-NOT-FALSE-NOT-UNDEF))
(200 200 (:REWRITE PROOF-CHECKER-ARRAY::SUBSETP-MEMBER-IMPLIES-MEMBER))
(200 200 (:REWRITE PROOF-CHECKER-ARRAY::MEMBER-UNION-VARIABLES1))
(192 96 (:REWRITE PROOF-CHECKER-ARRAY::TERNARYP-NOT-TRUE-NOT-FALSE))
(172 172 (:REWRITE DEFAULT-CAR))
(168 168 (:REWRITE PROOF-CHECKER-ARRAY::TERNARYP-EVALUATE-CLAUSE))
(145 145 (:REWRITE DEFAULT-CDR))
(144 72 (:REWRITE PROOF-CHECKER-ARRAY::FALSEP-IMPLIES-NOT-TRUEP))
(132 72 (:REWRITE PROOF-CHECKER-ARRAY::UNDEFP-IMPLIES-NOT-TRUEP))
(96 96 (:TYPE-PRESCRIPTION PROOF-CHECKER-ARRAY::NEGATE))
(96 96 (:REWRITE PROOF-CHECKER-ARRAY::SUBSET-VARIABLESP-IMPLIES-MEMBER-OR-MEMBER-NEGATE))
(96 48 (:REWRITE PROOF-CHECKER-ARRAY::TRUEP-IMPLIES-NOT-FALSEP))
(96 48 (:REWRITE PROOF-CHECKER-ARRAY::FALSEP-IMPLIES-NOT-UNDEFP))
(84 48 (:REWRITE PROOF-CHECKER-ARRAY::UNDEFP-IMPLIES-NOT-FALSEP))
(48 48 (:REWRITE PROOF-CHECKER-ARRAY::SET-EQUALP-IMPLIES-EQUAL-EVALUATE-LITERAL))
(48 48 (:REWRITE PROOF-CHECKER-ARRAY::IS-UNIT-CLAUSE-IMPLIES-UNDEFP-EVALUATE-CLAUSE))
(36 36 (:REWRITE PROOF-CHECKER-ARRAY::TRUEP-IMPLIES-NOT-UNDEFP))
(12 12 (:REWRITE PROOF-CHECKER-ARRAY::SET-EQUALP-IMPLIES-EQUAL-EVALUATE-CLAUSE))
)
(PROOF-CHECKER-ARRAY::NOT-MEMBER-NEGATE-MV-NTH-0-FIND-UNIT-CLAUSE-ASSIGNMENT
(720 12 (:DEFINITION PROOF-CHECKER-ARRAY::EVALUATE-CLAUSE))
(552 132 (:REWRITE PROOF-CHECKER-ARRAY::TERNARYP-NOT-TRUE-NOT-UNDEF))
(516 96 (:REWRITE PROOF-CHECKER-ARRAY::TERNARYP-NOT-FALSE-NOT-UNDEF))
(200 200 (:REWRITE PROOF-CHECKER-ARRAY::SUBSETP-MEMBER-IMPLIES-MEMBER))
(200 200 (:REWRITE PROOF-CHECKER-ARRAY::MEMBER-UNION-VARIABLES1))
(192 96 (:REWRITE PROOF-CHECKER-ARRAY::TERNARYP-NOT-TRUE-NOT-FALSE))
(172 172 (:REWRITE DEFAULT-CAR))
(168 168 (:REWRITE PROOF-CHECKER-ARRAY::TERNARYP-EVALUATE-CLAUSE))
(145 145 (:REWRITE DEFAULT-CDR))
(144 72 (:REWRITE PROOF-CHECKER-ARRAY::FALSEP-IMPLIES-NOT-TRUEP))
(132 72 (:REWRITE PROOF-CHECKER-ARRAY::UNDEFP-IMPLIES-NOT-TRUEP))
(104 104 (:REWRITE PROOF-CHECKER-ARRAY::SUBSET-VARIABLESP-IMPLIES-MEMBER-OR-MEMBER-NEGATE))
(96 48 (:REWRITE PROOF-CHECKER-ARRAY::TRUEP-IMPLIES-NOT-FALSEP))
(96 48 (:REWRITE PROOF-CHECKER-ARRAY::FALSEP-IMPLIES-NOT-UNDEFP))
(84 48 (:REWRITE PROOF-CHECKER-ARRAY::UNDEFP-IMPLIES-NOT-FALSEP))
(48 48 (:REWRITE PROOF-CHECKER-ARRAY::SET-EQUALP-IMPLIES-EQUAL-EVALUATE-LITERAL))
(48 48 (:REWRITE PROOF-CHECKER-ARRAY::IS-UNIT-CLAUSE-IMPLIES-UNDEFP-EVALUATE-CLAUSE))
(36 36 (:REWRITE PROOF-CHECKER-ARRAY::TRUEP-IMPLIES-NOT-UNDEFP))
(12 12 (:REWRITE PROOF-CHECKER-ARRAY::SET-EQUALP-IMPLIES-EQUAL-EVALUATE-CLAUSE))
)
(PROOF-CHECKER-ARRAY::MEMBER-MV-NTH-0-FIND-UNIT-CLAUSE-MV-NTH-1-FIND-UNIT-CLAUSE
(960 16 (:DEFINITION PROOF-CHECKER-ARRAY::EVALUATE-CLAUSE))
(736 176 (:REWRITE PROOF-CHECKER-ARRAY::TERNARYP-NOT-TRUE-NOT-UNDEF))
(688 128 (:REWRITE PROOF-CHECKER-ARRAY::TERNARYP-NOT-FALSE-NOT-UNDEF))
(264 264 (:REWRITE PROOF-CHECKER-ARRAY::SUBSETP-MEMBER-IMPLIES-MEMBER))
(264 264 (:REWRITE PROOF-CHECKER-ARRAY::MEMBER-UNION-VARIABLES1))
(256 128 (:REWRITE PROOF-CHECKER-ARRAY::TERNARYP-NOT-TRUE-NOT-FALSE))
(228 228 (:REWRITE DEFAULT-CAR))
(224 224 (:REWRITE PROOF-CHECKER-ARRAY::TERNARYP-EVALUATE-CLAUSE))
(193 193 (:REWRITE DEFAULT-CDR))
(192 96 (:REWRITE PROOF-CHECKER-ARRAY::FALSEP-IMPLIES-NOT-TRUEP))
(176 96 (:REWRITE PROOF-CHECKER-ARRAY::UNDEFP-IMPLIES-NOT-TRUEP))
(128 128 (:TYPE-PRESCRIPTION PROOF-CHECKER-ARRAY::NEGATE))
(128 128 (:REWRITE PROOF-CHECKER-ARRAY::SUBSET-VARIABLESP-IMPLIES-MEMBER-OR-MEMBER-NEGATE))
(128 64 (:REWRITE PROOF-CHECKER-ARRAY::TRUEP-IMPLIES-NOT-FALSEP))
(128 64 (:REWRITE PROOF-CHECKER-ARRAY::FALSEP-IMPLIES-NOT-UNDEFP))
(112 64 (:REWRITE PROOF-CHECKER-ARRAY::UNDEFP-IMPLIES-NOT-FALSEP))
(64 64 (:REWRITE PROOF-CHECKER-ARRAY::SET-EQUALP-IMPLIES-EQUAL-EVALUATE-LITERAL))
(64 64 (:REWRITE PROOF-CHECKER-ARRAY::IS-UNIT-CLAUSE-IMPLIES-UNDEFP-EVALUATE-CLAUSE))
(48 48 (:REWRITE PROOF-CHECKER-ARRAY::TRUEP-IMPLIES-NOT-UNDEFP))
(16 16 (:REWRITE PROOF-CHECKER-ARRAY::SET-EQUALP-IMPLIES-EQUAL-EVALUATE-CLAUSE))
)
(PROOF-CHECKER-ARRAY::MEMBER-MV-NTH-1-FIND-UNIT-CLAUSE-FORMULA
(1500 25 (:DEFINITION PROOF-CHECKER-ARRAY::EVALUATE-CLAUSE))
(1150 275 (:REWRITE PROOF-CHECKER-ARRAY::TERNARYP-NOT-TRUE-NOT-UNDEF))
(1075 200 (:REWRITE PROOF-CHECKER-ARRAY::TERNARYP-NOT-FALSE-NOT-UNDEF))
(411 411 (:REWRITE PROOF-CHECKER-ARRAY::SUBSETP-MEMBER-IMPLIES-MEMBER))
(411 411 (:REWRITE PROOF-CHECKER-ARRAY::MEMBER-UNION-VARIABLES1))
(400 200 (:REWRITE PROOF-CHECKER-ARRAY::TERNARYP-NOT-TRUE-NOT-FALSE))
(364 364 (:REWRITE DEFAULT-CAR))
(350 350 (:REWRITE PROOF-CHECKER-ARRAY::TERNARYP-EVALUATE-CLAUSE))
(306 306 (:REWRITE DEFAULT-CDR))
(300 150 (:REWRITE PROOF-CHECKER-ARRAY::FALSEP-IMPLIES-NOT-TRUEP))
(275 150 (:REWRITE PROOF-CHECKER-ARRAY::UNDEFP-IMPLIES-NOT-TRUEP))
(200 200 (:TYPE-PRESCRIPTION PROOF-CHECKER-ARRAY::NEGATE))
(200 200 (:REWRITE PROOF-CHECKER-ARRAY::SUBSET-VARIABLESP-IMPLIES-MEMBER-OR-MEMBER-NEGATE))
(200 100 (:REWRITE PROOF-CHECKER-ARRAY::TRUEP-IMPLIES-NOT-FALSEP))
(200 100 (:REWRITE PROOF-CHECKER-ARRAY::FALSEP-IMPLIES-NOT-UNDEFP))
(175 100 (:REWRITE PROOF-CHECKER-ARRAY::UNDEFP-IMPLIES-NOT-FALSEP))
(100 100 (:REWRITE PROOF-CHECKER-ARRAY::SET-EQUALP-IMPLIES-EQUAL-EVALUATE-LITERAL))
(100 100 (:REWRITE PROOF-CHECKER-ARRAY::IS-UNIT-CLAUSE-IMPLIES-UNDEFP-EVALUATE-CLAUSE))
(75 75 (:REWRITE PROOF-CHECKER-ARRAY::TRUEP-IMPLIES-NOT-UNDEFP))
(25 25 (:REWRITE PROOF-CHECKER-ARRAY::SET-EQUALP-IMPLIES-EQUAL-EVALUATE-CLAUSE))
)
(PROOF-CHECKER-ARRAY::MEMBER-MV-NTH-0-FIND-UNIT-CLAUSE-ALL-LITERALS)
|
