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
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
|
(PROOF-CHECKER-ARRAY::UNIQUE-LITERALSP
(7 7 (:REWRITE DEFAULT-CDR))
(5 5 (:REWRITE DEFAULT-CAR))
(4 4 (:REWRITE PROOF-CHECKER-ARRAY::LITERAL-LISTP-IMPLIES-LITERALP-MEMBER))
(4 2 (:DEFINITION TRUE-LISTP))
)
(PROOF-CHECKER-ARRAY::NO-CONFLICTING-LITERALSP
(7 7 (:REWRITE DEFAULT-CDR))
(6 6 (:REWRITE DEFAULT-CAR))
(5 5 (:REWRITE PROOF-CHECKER-ARRAY::LITERAL-LISTP-IMPLIES-LITERALP-MEMBER))
(4 2 (:DEFINITION TRUE-LISTP))
)
(PROOF-CHECKER-ARRAY::REMOVE-DUPLICATE-LITERALS
(7 7 (:REWRITE DEFAULT-CDR))
(5 5 (:REWRITE DEFAULT-CAR))
(4 4 (:REWRITE PROOF-CHECKER-ARRAY::LITERAL-LISTP-IMPLIES-LITERALP-MEMBER))
(4 2 (:DEFINITION TRUE-LISTP))
)
(PROOF-CHECKER-ARRAY::MEMBER-REMOVE-DUPLICATE-LITERALS
(167 160 (:REWRITE DEFAULT-CAR))
(157 157 (:REWRITE PROOF-CHECKER-ARRAY::SUBSETP-MEMBER-IMPLIES-MEMBER))
(157 157 (:REWRITE PROOF-CHECKER-ARRAY::MEMBER-UNION-VARIABLES1))
(152 149 (:REWRITE DEFAULT-CDR))
)
(PROOF-CHECKER-ARRAY::UNIQUE-LITERALSP-REMOVE-DUPLICATE-LITERALS
(36 34 (:REWRITE DEFAULT-CDR))
(28 27 (:REWRITE DEFAULT-CAR))
(24 24 (:REWRITE PROOF-CHECKER-ARRAY::SUBSETP-MEMBER-IMPLIES-MEMBER))
(24 24 (:REWRITE PROOF-CHECKER-ARRAY::MEMBER-UNION-VARIABLES1))
)
(PROOF-CHECKER-ARRAY::LITERAL-LISTP-REMOVE-DUPLICATE-LITERALS
(41 40 (:REWRITE DEFAULT-CAR))
(38 37 (:REWRITE DEFAULT-CDR))
(34 34 (:REWRITE PROOF-CHECKER-ARRAY::SUBSETP-MEMBER-IMPLIES-MEMBER))
(34 34 (:REWRITE PROOF-CHECKER-ARRAY::MEMBER-UNION-VARIABLES1))
)
(PROOF-CHECKER-ARRAY::NO-CONFLICTING-LITERALSP-REMOVE-DUPLICATE-LITERALS
(54 52 (:REWRITE DEFAULT-CDR))
(44 43 (:REWRITE DEFAULT-CAR))
(40 40 (:REWRITE PROOF-CHECKER-ARRAY::SUBSETP-MEMBER-IMPLIES-MEMBER))
(40 40 (:REWRITE PROOF-CHECKER-ARRAY::MEMBER-UNION-VARIABLES1))
(24 24 (:REWRITE PROOF-CHECKER-ARRAY::SUBSET-VARIABLESP-IMPLIES-MEMBER-OR-MEMBER-NEGATE))
)
(PROOF-CHECKER-ARRAY::REMOVE-CONFLICTING-LITERALS
(7 7 (:REWRITE DEFAULT-CDR))
(6 6 (:REWRITE DEFAULT-CAR))
(5 5 (:REWRITE PROOF-CHECKER-ARRAY::LITERAL-LISTP-IMPLIES-LITERALP-MEMBER))
(4 2 (:DEFINITION TRUE-LISTP))
)
(PROOF-CHECKER-ARRAY::NOT-MEMBER-REMOVE-CONFLICTING-LITERALS
(38 38 (:REWRITE PROOF-CHECKER-ARRAY::SUBSETP-MEMBER-IMPLIES-MEMBER))
(38 38 (:REWRITE PROOF-CHECKER-ARRAY::MEMBER-UNION-VARIABLES1))
(32 31 (:REWRITE DEFAULT-CAR))
(29 28 (:REWRITE DEFAULT-CDR))
(16 16 (:REWRITE PROOF-CHECKER-ARRAY::SUBSET-VARIABLESP-IMPLIES-MEMBER-OR-MEMBER-NEGATE))
)
(PROOF-CHECKER-ARRAY::MEMBER-REMOVE-CONFLICTING-LITERALS2
(70 65 (:REWRITE DEFAULT-CAR))
(69 69 (:REWRITE PROOF-CHECKER-ARRAY::SUBSETP-MEMBER-IMPLIES-MEMBER))
(69 69 (:REWRITE PROOF-CHECKER-ARRAY::MEMBER-UNION-VARIABLES1))
(43 42 (:REWRITE DEFAULT-CDR))
(42 42 (:REWRITE PROOF-CHECKER-ARRAY::SUBSET-VARIABLESP-IMPLIES-MEMBER-OR-MEMBER-NEGATE))
(24 6 (:REWRITE PROOF-CHECKER-ARRAY::LITERALP-IMPLIES-NOT-EQUAL-NEGATE))
(12 12 (:TYPE-PRESCRIPTION PROOF-CHECKER-ARRAY::LITERALP))
(10 6 (:REWRITE PROOF-CHECKER-ARRAY::NOT-MEMBER-REMOVE-CONFLICTING-LITERALS))
(6 6 (:REWRITE PROOF-CHECKER-ARRAY::LITERAL-LISTP-IMPLIES-LITERALP-MEMBER))
)
(PROOF-CHECKER-ARRAY::MEMBER-REMOVE-CONFLICTING-LITERALS3
(174 174 (:REWRITE PROOF-CHECKER-ARRAY::SUBSETP-MEMBER-IMPLIES-MEMBER))
(174 174 (:REWRITE PROOF-CHECKER-ARRAY::MEMBER-UNION-VARIABLES1))
(158 149 (:REWRITE DEFAULT-CAR))
(137 137 (:REWRITE PROOF-CHECKER-ARRAY::SUBSET-VARIABLESP-IMPLIES-MEMBER-OR-MEMBER-NEGATE))
(127 124 (:REWRITE DEFAULT-CDR))
(10 10 (:REWRITE PROOF-CHECKER-ARRAY::LITERAL-LISTP-IMPLIES-LITERALP-MEMBER))
)
(PROOF-CHECKER-ARRAY::NO-CONFLICTING-LITERALSP-REMOVE-CONFLICTING-LITERALS
(35 33 (:REWRITE DEFAULT-CDR))
(27 26 (:REWRITE DEFAULT-CAR))
(22 22 (:REWRITE PROOF-CHECKER-ARRAY::SUBSETP-MEMBER-IMPLIES-MEMBER))
(22 22 (:REWRITE PROOF-CHECKER-ARRAY::SUBSET-VARIABLESP-IMPLIES-MEMBER-OR-MEMBER-NEGATE))
(22 22 (:REWRITE PROOF-CHECKER-ARRAY::MEMBER-UNION-VARIABLES1))
(5 1 (:REWRITE PROOF-CHECKER-ARRAY::MEMBER-REMOVE-CONFLICTING-LITERALS3))
(3 1 (:REWRITE PROOF-CHECKER-ARRAY::LITERALP-NEGATE))
(2 2 (:TYPE-PRESCRIPTION PROOF-CHECKER-ARRAY::LITERALP))
(1 1 (:REWRITE PROOF-CHECKER-ARRAY::MEMBER-REMOVE-CONFLICTING-LITERALS2))
(1 1 (:REWRITE PROOF-CHECKER-ARRAY::LITERAL-LISTP-IMPLIES-LITERALP-MEMBER))
)
(PROOF-CHECKER-ARRAY::LITERAL-LISTP-REMOVE-CONFLICTING-LITERALS
(52 4 (:REWRITE PROOF-CHECKER-ARRAY::MEMBER-REMOVE-CONFLICTING-LITERALS2))
(48 47 (:REWRITE DEFAULT-CAR))
(47 47 (:REWRITE PROOF-CHECKER-ARRAY::SUBSETP-MEMBER-IMPLIES-MEMBER))
(47 47 (:REWRITE PROOF-CHECKER-ARRAY::MEMBER-UNION-VARIABLES1))
(44 43 (:REWRITE DEFAULT-CDR))
(40 4 (:REWRITE PROOF-CHECKER-ARRAY::MEMBER-REMOVE-CONFLICTING-LITERALS3))
(16 16 (:REWRITE PROOF-CHECKER-ARRAY::SUBSET-VARIABLESP-IMPLIES-MEMBER-OR-MEMBER-NEGATE))
)
(PROOF-CHECKER-ARRAY::UNIQUE-LITERALSP-REMOVE-CONFLICTING-LITERALS
(53 51 (:REWRITE DEFAULT-CDR))
(43 42 (:REWRITE DEFAULT-CAR))
(38 38 (:REWRITE PROOF-CHECKER-ARRAY::SUBSETP-MEMBER-IMPLIES-MEMBER))
(38 38 (:REWRITE PROOF-CHECKER-ARRAY::MEMBER-UNION-VARIABLES1))
(16 16 (:REWRITE PROOF-CHECKER-ARRAY::SUBSET-VARIABLESP-IMPLIES-MEMBER-OR-MEMBER-NEGATE))
(4 1 (:REWRITE PROOF-CHECKER-ARRAY::MEMBER-REMOVE-CONFLICTING-LITERALS3))
(2 2 (:TYPE-PRESCRIPTION PROOF-CHECKER-ARRAY::LITERALP))
(1 1 (:REWRITE PROOF-CHECKER-ARRAY::MEMBER-REMOVE-CONFLICTING-LITERALS2))
(1 1 (:REWRITE PROOF-CHECKER-ARRAY::LITERAL-LISTP-IMPLIES-LITERALP-MEMBER))
)
(PROOF-CHECKER-ARRAY::UNIQUE-LITERALSP-UNION-VARIABLES
(97 95 (:REWRITE DEFAULT-CAR))
(91 87 (:REWRITE DEFAULT-CDR))
(82 82 (:REWRITE PROOF-CHECKER-ARRAY::SUBSETP-MEMBER-IMPLIES-MEMBER))
(22 22 (:REWRITE PROOF-CHECKER-ARRAY::SUBSET-VARIABLESP-IMPLIES-MEMBER-OR-MEMBER-NEGATE))
(2 2 (:REWRITE PROOF-CHECKER-ARRAY::MEMBER-UNION-VARIABLES3))
(2 2 (:REWRITE PROOF-CHECKER-ARRAY::MEMBER-UNION-VARIABLES2))
)
(PROOF-CHECKER-ARRAY::NO-CONFLICTING-LITERALSP-UNION-VARIABLES
(97 95 (:REWRITE DEFAULT-CAR))
(91 87 (:REWRITE DEFAULT-CDR))
(82 82 (:REWRITE PROOF-CHECKER-ARRAY::SUBSETP-MEMBER-IMPLIES-MEMBER))
(58 58 (:REWRITE PROOF-CHECKER-ARRAY::SUBSET-VARIABLESP-IMPLIES-MEMBER-OR-MEMBER-NEGATE))
(2 2 (:REWRITE PROOF-CHECKER-ARRAY::MEMBER-UNION-VARIABLES3))
(2 2 (:REWRITE PROOF-CHECKER-ARRAY::MEMBER-UNION-VARIABLES2))
)
(PROOF-CHECKER-ARRAY::SUBSETP-REMOVE-DUPLICATE-LITERALS
(85 64 (:REWRITE DEFAULT-CDR))
(70 5 (:DEFINITION PROOF-CHECKER-ARRAY::REMOVE-DUPLICATE-LITERALS))
(51 51 (:REWRITE DEFAULT-CAR))
(46 46 (:REWRITE PROOF-CHECKER-ARRAY::SUBSETP-MEMBER-IMPLIES-MEMBER))
(46 46 (:REWRITE PROOF-CHECKER-ARRAY::MEMBER-UNION-VARIABLES1))
(37 37 (:TYPE-PRESCRIPTION PROOF-CHECKER-ARRAY::REMOVE-DUPLICATE-LITERALS))
)
(PROOF-CHECKER-ARRAY::SUBSETP-LIST-REMOVE-DUPLICATE-LITERALS
(330 50 (:REWRITE PROOF-CHECKER-ARRAY::SUBSETP-CDR))
(82 82 (:REWRITE DEFAULT-CDR))
(70 5 (:DEFINITION PROOF-CHECKER-ARRAY::REMOVE-DUPLICATE-LITERALS))
(65 65 (:REWRITE DEFAULT-CAR))
(50 50 (:REWRITE PROOF-CHECKER-ARRAY::MEMBER-UNION-VARIABLES1))
)
(PROOF-CHECKER-ARRAY::NOT-NO-CONFLICTING-LITERALSP
(74 74 (:REWRITE PROOF-CHECKER-ARRAY::SUBSETP-MEMBER-IMPLIES-MEMBER))
(74 74 (:REWRITE PROOF-CHECKER-ARRAY::MEMBER-UNION-VARIABLES1))
(67 67 (:REWRITE DEFAULT-CAR))
(65 65 (:REWRITE DEFAULT-CDR))
(51 51 (:REWRITE PROOF-CHECKER-ARRAY::SUBSET-VARIABLESP-IMPLIES-MEMBER-OR-MEMBER-NEGATE))
(13 13 (:REWRITE PROOF-CHECKER-ARRAY::LITERAL-LISTP-IMPLIES-LITERALP-MEMBER))
)
(PROOF-CHECKER-ARRAY::FIND-NEGATED-LITERAL
(52 4 (:REWRITE PROOF-CHECKER-ARRAY::LITERAL-LISTP-IMPLIES-LITERALP-MEMBER))
(32 4 (:DEFINITION MEMBER-EQUAL))
(8 8 (:REWRITE PROOF-CHECKER-ARRAY::SUBSETP-MEMBER-IMPLIES-MEMBER))
(8 8 (:REWRITE PROOF-CHECKER-ARRAY::MEMBER-UNION-VARIABLES1))
(8 8 (:REWRITE DEFAULT-CAR))
(7 7 (:REWRITE DEFAULT-CDR))
)
(PROOF-CHECKER-ARRAY::SUBSET-VARIABLESP-NOT-SUBSETP-IMPLIES-FIND-NEGATED-LITERAL
(303 207 (:REWRITE PROOF-CHECKER-ARRAY::SUBSETP-MEMBER-IMPLIES-MEMBER))
(247 80 (:REWRITE PROOF-CHECKER-ARRAY::SUBSET-VARIABLESP-IMPLIES-MEMBER-OR-MEMBER-NEGATE))
(218 218 (:REWRITE DEFAULT-CAR))
(207 207 (:REWRITE PROOF-CHECKER-ARRAY::MEMBER-UNION-VARIABLES1))
(180 180 (:REWRITE DEFAULT-CDR))
(16 16 (:REWRITE PROOF-CHECKER-ARRAY::SUBSET-VARIABLESP-TRANSITIVE))
(16 16 (:REWRITE PROOF-CHECKER-ARRAY::MEMBER-AND-NOT-MEMBER-IMPLIES-NOT-SUBSET-VARIABLESP))
(8 8 (:REWRITE PROOF-CHECKER-ARRAY::LITERAL-LISTP-IMPLIES-LITERALP-MEMBER))
)
(PROOF-CHECKER-ARRAY::FIND-NEGATED-LITERAL-IMPLIES-MEMBER
(1510 9 (:REWRITE PROOF-CHECKER-ARRAY::SUBSET-VARIABLESP-NOT-SUBSETP-IMPLIES-FIND-NEGATED-LITERAL))
(1100 10 (:DEFINITION PROOF-CHECKER-ARRAY::SUBSET-VARIABLESP))
(1094 30 (:REWRITE PROOF-CHECKER-ARRAY::NOT-SET-DIFFERENCE-VARIABLES-IMPLIES-SUBSET-VARIABLESP))
(1009 31 (:DEFINITION PROOF-CHECKER-ARRAY::SET-DIFFERENCE-VARIABLES))
(249 249 (:REWRITE DEFAULT-CAR))
(232 232 (:TYPE-PRESCRIPTION PROOF-CHECKER-ARRAY::SET-DIFFERENCE-VARIABLES))
(214 214 (:REWRITE DEFAULT-CDR))
(205 205 (:REWRITE PROOF-CHECKER-ARRAY::SUBSETP-MEMBER-IMPLIES-MEMBER))
(205 205 (:REWRITE PROOF-CHECKER-ARRAY::MEMBER-UNION-VARIABLES1))
(110 110 (:REWRITE PROOF-CHECKER-ARRAY::SUBSET-VARIABLESP-IMPLIES-MEMBER-OR-MEMBER-NEGATE))
(63 63 (:TYPE-PRESCRIPTION PROOF-CHECKER-ARRAY::SUBSET-VARIABLESP))
(30 30 (:REWRITE PROOF-CHECKER-ARRAY::SUBSET-VARIABLESP-TRANSITIVE))
(2 2 (:TYPE-PRESCRIPTION PROOF-CHECKER-ARRAY::SUBSETP))
(2 1 (:REWRITE PROOF-CHECKER-ARRAY::SUBSETP-CDR))
(1 1 (:DEFINITION PROOF-CHECKER-ARRAY::SUBSETP))
)
(PROOF-CHECKER-ARRAY::FIND-NEGATED-LITERAL-IMPLIES-MEMBER-NEGATE
(1362 8 (:REWRITE PROOF-CHECKER-ARRAY::SUBSET-VARIABLESP-NOT-SUBSETP-IMPLIES-FIND-NEGATED-LITERAL))
(992 9 (:DEFINITION PROOF-CHECKER-ARRAY::SUBSET-VARIABLESP))
(986 27 (:REWRITE PROOF-CHECKER-ARRAY::NOT-SET-DIFFERENCE-VARIABLES-IMPLIES-SUBSET-VARIABLESP))
(910 28 (:DEFINITION PROOF-CHECKER-ARRAY::SET-DIFFERENCE-VARIABLES))
(213 213 (:REWRITE DEFAULT-CAR))
(208 208 (:TYPE-PRESCRIPTION PROOF-CHECKER-ARRAY::SET-DIFFERENCE-VARIABLES))
(195 195 (:REWRITE DEFAULT-CDR))
(186 186 (:REWRITE PROOF-CHECKER-ARRAY::SUBSETP-MEMBER-IMPLIES-MEMBER))
(186 186 (:REWRITE PROOF-CHECKER-ARRAY::MEMBER-UNION-VARIABLES1))
(106 106 (:REWRITE PROOF-CHECKER-ARRAY::SUBSET-VARIABLESP-IMPLIES-MEMBER-OR-MEMBER-NEGATE))
(56 56 (:TYPE-PRESCRIPTION PROOF-CHECKER-ARRAY::SUBSET-VARIABLESP))
(27 27 (:REWRITE PROOF-CHECKER-ARRAY::SUBSET-VARIABLESP-TRANSITIVE))
(2 2 (:TYPE-PRESCRIPTION PROOF-CHECKER-ARRAY::SUBSETP))
(2 1 (:REWRITE PROOF-CHECKER-ARRAY::SUBSETP-CDR))
(1 1 (:DEFINITION PROOF-CHECKER-ARRAY::SUBSETP))
)
(PROOF-CHECKER-ARRAY::SUBSET-VARIABLESP-NOT-SUBSETP-IMPLIES-MEMBER-FIND-NEGATED-LITERAL
(108 3 (:REWRITE PROOF-CHECKER-ARRAY::NOT-SET-DIFFERENCE-VARIABLES-IMPLIES-SUBSET-VARIABLESP))
(101 16 (:DEFINITION MEMBER-EQUAL))
(101 1 (:DEFINITION PROOF-CHECKER-ARRAY::SUBSET-VARIABLESP))
(99 3 (:DEFINITION PROOF-CHECKER-ARRAY::SET-DIFFERENCE-VARIABLES))
(66 2 (:DEFINITION PROOF-CHECKER-ARRAY::FIND-NEGATED-LITERAL))
(46 12 (:REWRITE PROOF-CHECKER-ARRAY::SUBSET-VARIABLESP-IMPLIES-MEMBER-OR-MEMBER-NEGATE))
(38 2 (:DEFINITION PROOF-CHECKER-ARRAY::SUBSETP))
(34 34 (:REWRITE DEFAULT-CAR))
(33 5 (:REWRITE PROOF-CHECKER-ARRAY::SUBSETP-CDR))
(32 32 (:REWRITE DEFAULT-CDR))
(30 30 (:REWRITE PROOF-CHECKER-ARRAY::SUBSETP-MEMBER-IMPLIES-MEMBER))
(30 30 (:REWRITE PROOF-CHECKER-ARRAY::MEMBER-UNION-VARIABLES1))
(24 24 (:TYPE-PRESCRIPTION PROOF-CHECKER-ARRAY::SET-DIFFERENCE-VARIABLES))
(5 1 (:DEFINITION PROOF-CHECKER-ARRAY::LITERAL-LISTP))
(3 3 (:REWRITE PROOF-CHECKER-ARRAY::SUBSET-VARIABLESP-TRANSITIVE))
(3 3 (:REWRITE PROOF-CHECKER-ARRAY::MEMBER-AND-NOT-MEMBER-IMPLIES-NOT-SUBSET-VARIABLESP))
(1 1 (:TYPE-PRESCRIPTION PROOF-CHECKER-ARRAY::LITERALP))
(1 1 (:REWRITE PROOF-CHECKER-ARRAY::LITERAL-LISTP-IMPLIES-LITERALP-MEMBER))
)
(PROOF-CHECKER-ARRAY::SUBSET-VARIABLESP-NOT-SUBSETP-IMPLIES-NOT-NO-CONFLICTING-LITERALSP
(315 7 (:DEFINITION PROOF-CHECKER-ARRAY::FIND-NEGATED-LITERAL))
(188 6 (:REWRITE PROOF-CHECKER-ARRAY::NOT-SET-DIFFERENCE-VARIABLES-IMPLIES-SUBSET-VARIABLESP))
(172 5 (:DEFINITION PROOF-CHECKER-ARRAY::SET-DIFFERENCE-VARIABLES))
(93 93 (:REWRITE PROOF-CHECKER-ARRAY::MEMBER-UNION-VARIABLES1))
(86 86 (:REWRITE DEFAULT-CAR))
(79 6 (:REWRITE PROOF-CHECKER-ARRAY::SUBSET-VARIABLESP-TRANSITIVE))
(71 71 (:REWRITE DEFAULT-CDR))
(66 10 (:REWRITE PROOF-CHECKER-ARRAY::SUBSETP-CDR))
(38 38 (:TYPE-PRESCRIPTION PROOF-CHECKER-ARRAY::SET-DIFFERENCE-VARIABLES))
(4 4 (:REWRITE PROOF-CHECKER-ARRAY::MEMBER-AND-NOT-MEMBER-IMPLIES-NOT-SUBSET-VARIABLESP))
(2 2 (:REWRITE PROOF-CHECKER-ARRAY::NOT-NO-CONFLICTING-LITERALSP))
)
(PROOF-CHECKER-ARRAY::SUBSET-VARIABLESP-REMOVE-CONFLICTING-LITERALS1
(4590 21 (:REWRITE PROOF-CHECKER-ARRAY::NOT-SET-DIFFERENCE-VARIABLES-IMPLIES-SUBSET-VARIABLESP))
(4362 25 (:DEFINITION PROOF-CHECKER-ARRAY::SET-DIFFERENCE-VARIABLES))
(1370 83 (:REWRITE PROOF-CHECKER-ARRAY::MEMBER-REMOVE-CONFLICTING-LITERALS2))
(771 287 (:REWRITE PROOF-CHECKER-ARRAY::SUBSET-VARIABLESP-IMPLIES-MEMBER-OR-MEMBER-NEGATE))
(765 765 (:REWRITE PROOF-CHECKER-ARRAY::MEMBER-UNION-VARIABLES1))
(759 759 (:REWRITE PROOF-CHECKER-ARRAY::SUBSETP-MEMBER-IMPLIES-MEMBER))
(702 78 (:REWRITE PROOF-CHECKER-ARRAY::LITERALP-IMPLIES-NOT-EQUAL-NEGATE))
(561 547 (:REWRITE DEFAULT-CAR))
(447 21 (:REWRITE PROOF-CHECKER-ARRAY::SUBSET-VARIABLESP-TRANSITIVE))
(394 387 (:REWRITE DEFAULT-CDR))
(169 8 (:REWRITE PROOF-CHECKER-ARRAY::EQUAL-SET-DIFFERENCE-VARIABLES-CONS))
(165 165 (:TYPE-PRESCRIPTION PROOF-CHECKER-ARRAY::SET-DIFFERENCE-VARIABLES))
(14 14 (:REWRITE PROOF-CHECKER-ARRAY::MEMBER-AND-NOT-MEMBER-IMPLIES-NOT-SUBSET-VARIABLESP))
)
(PROOF-CHECKER-ARRAY::SUBSET-VARIABLESP-REMOVE-CONFLICTING-LITERALS2
(1958 82 (:REWRITE PROOF-CHECKER-ARRAY::SUBSET-VARIABLESP-TRANSITIVE))
(1551 268 (:REWRITE PROOF-CHECKER-ARRAY::SUBSET-VARIABLESP-IMPLIES-MEMBER-OR-MEMBER-NEGATE))
(652 652 (:REWRITE PROOF-CHECKER-ARRAY::MEMBER-UNION-VARIABLES1))
(650 650 (:REWRITE PROOF-CHECKER-ARRAY::SUBSETP-MEMBER-IMPLIES-MEMBER))
(647 645 (:REWRITE DEFAULT-CDR))
(640 638 (:REWRITE DEFAULT-CAR))
(448 73 (:REWRITE PROOF-CHECKER-ARRAY::MEMBER-REMOVE-CONFLICTING-LITERALS2))
(292 73 (:REWRITE PROOF-CHECKER-ARRAY::MEMBER-REMOVE-CONFLICTING-LITERALS3))
(154 154 (:TYPE-PRESCRIPTION PROOF-CHECKER-ARRAY::LITERALP))
(77 77 (:REWRITE PROOF-CHECKER-ARRAY::LITERAL-LISTP-IMPLIES-LITERALP-MEMBER))
(53 53 (:REWRITE PROOF-CHECKER-ARRAY::MEMBER-AND-NOT-MEMBER-IMPLIES-NOT-SUBSET-VARIABLESP))
(18 6 (:REWRITE PROOF-CHECKER-ARRAY::EQUAL-SET-DIFFERENCE-VARIABLES-CONS))
)
(PROOF-CHECKER-ARRAY::SUBSET-VARIABLESP-AND-SUBSETP-IMPLIES-SUBSETP
(108 3 (:REWRITE PROOF-CHECKER-ARRAY::NOT-SET-DIFFERENCE-VARIABLES-IMPLIES-SUBSET-VARIABLESP))
(101 1 (:DEFINITION PROOF-CHECKER-ARRAY::SUBSET-VARIABLESP))
(99 3 (:DEFINITION PROOF-CHECKER-ARRAY::SET-DIFFERENCE-VARIABLES))
(65 10 (:DEFINITION MEMBER-EQUAL))
(38 2 (:DEFINITION PROOF-CHECKER-ARRAY::SUBSETP))
(33 5 (:REWRITE PROOF-CHECKER-ARRAY::SUBSETP-CDR))
(26 26 (:REWRITE DEFAULT-CDR))
(24 24 (:TYPE-PRESCRIPTION PROOF-CHECKER-ARRAY::SET-DIFFERENCE-VARIABLES))
(24 24 (:REWRITE DEFAULT-CAR))
(20 20 (:REWRITE PROOF-CHECKER-ARRAY::SUBSETP-MEMBER-IMPLIES-MEMBER))
(20 20 (:REWRITE PROOF-CHECKER-ARRAY::MEMBER-UNION-VARIABLES1))
(14 14 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
(8 8 (:TYPE-PRESCRIPTION PROOF-CHECKER-ARRAY::NEGATE))
(8 8 (:REWRITE PROOF-CHECKER-ARRAY::SUBSET-VARIABLESP-IMPLIES-MEMBER-OR-MEMBER-NEGATE))
(5 1 (:DEFINITION PROOF-CHECKER-ARRAY::LITERAL-LISTP))
(3 3 (:REWRITE PROOF-CHECKER-ARRAY::SUBSET-VARIABLESP-TRANSITIVE))
(3 3 (:REWRITE PROOF-CHECKER-ARRAY::MEMBER-AND-NOT-MEMBER-IMPLIES-NOT-SUBSET-VARIABLESP))
(1 1 (:TYPE-PRESCRIPTION PROOF-CHECKER-ARRAY::LITERALP))
(1 1 (:REWRITE PROOF-CHECKER-ARRAY::LITERAL-LISTP-IMPLIES-LITERALP-MEMBER))
)
(PROOF-CHECKER-ARRAY::SUBSETP-AND-SET-EQUAL-VARIABLESP-IMPLIES-SUBSETP
(743 5 (:REWRITE PROOF-CHECKER-ARRAY::SUBSET-VARIABLESP-AND-SUBSETP-IMPLIES-SUBSETP))
(718 20 (:REWRITE PROOF-CHECKER-ARRAY::NOT-SET-DIFFERENCE-VARIABLES-IMPLIES-SUBSET-VARIABLESP))
(707 7 (:DEFINITION PROOF-CHECKER-ARRAY::SUBSET-VARIABLESP))
(658 20 (:DEFINITION PROOF-CHECKER-ARRAY::SET-DIFFERENCE-VARIABLES))
(579 5 (:REWRITE PROOF-CHECKER-ARRAY::SUBSETP-CDR))
(530 2 (:DEFINITION PROOF-CHECKER-ARRAY::SUBSETP))
(386 58 (:DEFINITION MEMBER-EQUAL))
(151 151 (:TYPE-PRESCRIPTION PROOF-CHECKER-ARRAY::SET-DIFFERENCE-VARIABLES))
(146 114 (:REWRITE PROOF-CHECKER-ARRAY::SUBSETP-MEMBER-IMPLIES-MEMBER))
(128 128 (:REWRITE DEFAULT-CAR))
(126 126 (:REWRITE DEFAULT-CDR))
(119 20 (:REWRITE PROOF-CHECKER-ARRAY::SUBSET-VARIABLESP-TRANSITIVE))
(114 114 (:REWRITE PROOF-CHECKER-ARRAY::MEMBER-UNION-VARIABLES1))
(104 104 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
(96 48 (:REWRITE PROOF-CHECKER-ARRAY::SUBSET-VARIABLESP-IMPLIES-MEMBER-OR-MEMBER-NEGATE))
(48 48 (:TYPE-PRESCRIPTION PROOF-CHECKER-ARRAY::NEGATE))
(5 5 (:REWRITE PROOF-CHECKER-ARRAY::MEMBER-AND-NOT-MEMBER-IMPLIES-NOT-SUBSET-VARIABLESP))
(5 1 (:DEFINITION PROOF-CHECKER-ARRAY::LITERAL-LISTP))
(1 1 (:TYPE-PRESCRIPTION PROOF-CHECKER-ARRAY::LITERALP))
(1 1 (:REWRITE PROOF-CHECKER-ARRAY::LITERAL-LISTP-IMPLIES-LITERALP-MEMBER))
)
(PROOF-CHECKER-ARRAY::SUBSETP-AND-SET-EQUAL-VARIABLESP-IMPLIES-SET-EQUALP
(4898 7 (:DEFINITION PROOF-CHECKER-ARRAY::SUBSETP))
(4069 37 (:DEFINITION PROOF-CHECKER-ARRAY::SUBSET-VARIABLESP))
(4068 110 (:REWRITE PROOF-CHECKER-ARRAY::NOT-SET-DIFFERENCE-VARIABLES-IMPLIES-SUBSET-VARIABLESP))
(3738 110 (:DEFINITION PROOF-CHECKER-ARRAY::SET-DIFFERENCE-VARIABLES))
(3196 15 (:REWRITE PROOF-CHECKER-ARRAY::SUBSET-VARIABLESP-AND-SUBSETP-IMPLIES-SUBSETP))
(2354 343 (:DEFINITION MEMBER-EQUAL))
(1640 15 (:REWRITE PROOF-CHECKER-ARRAY::SUBSETP-CDR))
(892 268 (:REWRITE PROOF-CHECKER-ARRAY::SUBSET-VARIABLESP-IMPLIES-MEMBER-OR-MEMBER-NEGATE))
(829 829 (:TYPE-PRESCRIPTION PROOF-CHECKER-ARRAY::SET-DIFFERENCE-VARIABLES))
(734 4 (:REWRITE PROOF-CHECKER-ARRAY::SUBSET-VARIABLESP-NOT-SUBSETP-IMPLIES-NOT-NO-CONFLICTING-LITERALSP))
(725 725 (:REWRITE DEFAULT-CAR))
(720 720 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
(712 712 (:REWRITE DEFAULT-CDR))
(706 670 (:REWRITE PROOF-CHECKER-ARRAY::SUBSETP-MEMBER-IMPLIES-MEMBER))
(670 670 (:REWRITE PROOF-CHECKER-ARRAY::MEMBER-UNION-VARIABLES1))
(268 268 (:TYPE-PRESCRIPTION PROOF-CHECKER-ARRAY::NEGATE))
(82 4 (:DEFINITION PROOF-CHECKER-ARRAY::NO-CONFLICTING-LITERALSP))
(29 2 (:DEFINITION PROOF-CHECKER-ARRAY::LITERAL-LISTP))
(22 2 (:REWRITE PROOF-CHECKER-ARRAY::LITERAL-LISTP-IMPLIES-LITERALP-MEMBER))
(17 17 (:REWRITE PROOF-CHECKER-ARRAY::SET-EQUAL-VARIABLESP-TRANSITIVE))
(5 5 (:REWRITE PROOF-CHECKER-ARRAY::MEMBER-AND-NOT-MEMBER-IMPLIES-NOT-SUBSET-VARIABLESP))
(4 4 (:REWRITE PROOF-CHECKER-ARRAY::NOT-NO-CONFLICTING-LITERALSP))
(1 1 (:TYPE-PRESCRIPTION PROOF-CHECKER-ARRAY::LITERALP))
)
|
