33010
|
1 |
#2 := false
|
|
2 |
#169 := 0::int
|
|
3 |
decl uf_2 :: int
|
|
4 |
#5 := uf_2
|
|
5 |
#166 := -1::int
|
|
6 |
#202 := (* -1::int uf_2)
|
|
7 |
decl uf_1 :: int
|
|
8 |
#4 := uf_1
|
|
9 |
#203 := (+ uf_1 #202)
|
|
10 |
#218 := (>= #203 0::int)
|
|
11 |
decl uf_3 :: int
|
|
12 |
#7 := uf_3
|
|
13 |
#167 := (* -1::int uf_3)
|
|
14 |
#168 := (+ uf_1 #167)
|
|
15 |
#178 := (>= #168 0::int)
|
|
16 |
#217 := (not #218)
|
|
17 |
#204 := (<= #203 0::int)
|
|
18 |
#205 := (not #204)
|
|
19 |
#692 := [hypothesis]: #205
|
|
20 |
#177 := (not #178)
|
|
21 |
#693 := (or #177 #204)
|
|
22 |
#170 := (<= #168 0::int)
|
|
23 |
#191 := (+ uf_2 #167)
|
|
24 |
#237 := (<= #191 0::int)
|
|
25 |
#238 := (not #237)
|
|
26 |
#171 := (not #170)
|
|
27 |
#685 := [hypothesis]: #171
|
|
28 |
#190 := (>= #191 0::int)
|
|
29 |
#455 := (or #170 #190)
|
|
30 |
#189 := (not #190)
|
|
31 |
#197 := (and #171 #189)
|
|
32 |
#354 := (not #197)
|
|
33 |
#464 := (iff #354 #455)
|
|
34 |
#456 := (not #455)
|
|
35 |
#459 := (not #456)
|
|
36 |
#462 := (iff #459 #455)
|
|
37 |
#463 := [rewrite]: #462
|
|
38 |
#460 := (iff #354 #459)
|
|
39 |
#457 := (iff #197 #456)
|
|
40 |
#458 := [rewrite]: #457
|
|
41 |
#461 := [monotonicity #458]: #460
|
|
42 |
#465 := [trans #461 #463]: #464
|
|
43 |
#287 := (and #189 #217)
|
|
44 |
#10 := (= uf_2 uf_3)
|
|
45 |
#279 := (and #10 #217)
|
|
46 |
#273 := (and #177 #238)
|
|
47 |
#15 := (= uf_1 uf_3)
|
|
48 |
#268 := (and #15 #238)
|
|
49 |
#17 := (= uf_1 uf_2)
|
|
50 |
#260 := (and #17 #189)
|
|
51 |
#252 := (and #205 #238)
|
|
52 |
#244 := (and #17 #238)
|
|
53 |
#232 := (and #171 #217)
|
|
54 |
#224 := (and #15 #217)
|
|
55 |
#214 := (and #10 #205)
|
|
56 |
#211 := (and #177 #205)
|
|
57 |
#208 := (and #15 #205)
|
|
58 |
#184 := (and #17 #177)
|
|
59 |
#174 := (and #10 #171)
|
|
60 |
#115 := (and #10 #17)
|
|
61 |
#337 := (or #115 #174 #184 #197 #208 #211 #214 #224 #232 #244 #252 #260 #268 #273 #279 #287)
|
|
62 |
#342 := (not #337)
|
|
63 |
#21 := (= uf_2 uf_1)
|
|
64 |
#27 := (= uf_3 uf_2)
|
|
65 |
#34 := (and #27 #21)
|
|
66 |
#23 := (< uf_3 uf_1)
|
|
67 |
#33 := (and #10 #23)
|
|
68 |
#35 := (or #33 #34)
|
|
69 |
#12 := (< uf_1 uf_3)
|
|
70 |
#32 := (and #21 #12)
|
|
71 |
#36 := (or #32 #35)
|
|
72 |
#8 := (< uf_2 uf_3)
|
|
73 |
#31 := (and #8 #23)
|
|
74 |
#37 := (or #31 #36)
|
|
75 |
#25 := (= uf_3 uf_1)
|
|
76 |
#19 := (< uf_2 uf_1)
|
|
77 |
#30 := (and #19 #25)
|
|
78 |
#38 := (or #30 #37)
|
|
79 |
#29 := (and #19 #12)
|
|
80 |
#39 := (or #29 #38)
|
|
81 |
#28 := (and #27 #19)
|
|
82 |
#40 := (or #28 #39)
|
|
83 |
#6 := (< uf_1 uf_2)
|
|
84 |
#26 := (and #25 #6)
|
|
85 |
#41 := (or #26 #40)
|
|
86 |
#24 := (and #23 #6)
|
|
87 |
#42 := (or #24 #41)
|
|
88 |
#13 := (< uf_3 uf_2)
|
|
89 |
#22 := (and #13 #21)
|
|
90 |
#43 := (or #22 #42)
|
|
91 |
#20 := (and #13 #19)
|
|
92 |
#44 := (or #20 #43)
|
|
93 |
#18 := (and #17 #8)
|
|
94 |
#45 := (or #18 #44)
|
|
95 |
#16 := (and #15 #13)
|
|
96 |
#46 := (or #16 #45)
|
|
97 |
#14 := (and #12 #13)
|
|
98 |
#47 := (or #14 #46)
|
|
99 |
#11 := (and #6 #10)
|
|
100 |
#48 := (or #11 #47)
|
|
101 |
#9 := (and #6 #8)
|
|
102 |
#49 := (or #9 #48)
|
|
103 |
#50 := (not #49)
|
|
104 |
#345 := (iff #50 #342)
|
|
105 |
#118 := (or #33 #115)
|
|
106 |
#110 := (and #12 #17)
|
|
107 |
#121 := (or #110 #118)
|
|
108 |
#124 := (or #31 #121)
|
|
109 |
#102 := (and #15 #19)
|
|
110 |
#127 := (or #102 #124)
|
|
111 |
#96 := (and #12 #19)
|
|
112 |
#130 := (or #96 #127)
|
|
113 |
#93 := (and #10 #19)
|
|
114 |
#133 := (or #93 #130)
|
|
115 |
#86 := (and #6 #15)
|
|
116 |
#136 := (or #86 #133)
|
|
117 |
#78 := (and #6 #23)
|
|
118 |
#139 := (or #78 #136)
|
|
119 |
#75 := (and #13 #17)
|
|
120 |
#142 := (or #75 #139)
|
|
121 |
#145 := (or #20 #142)
|
|
122 |
#70 := (and #8 #17)
|
|
123 |
#148 := (or #70 #145)
|
|
124 |
#67 := (and #13 #15)
|
|
125 |
#151 := (or #67 #148)
|
|
126 |
#154 := (or #14 #151)
|
|
127 |
#157 := (or #11 #154)
|
|
128 |
#160 := (or #9 #157)
|
|
129 |
#163 := (not #160)
|
|
130 |
#343 := (iff #163 #342)
|
|
131 |
#340 := (iff #160 #337)
|
|
132 |
#292 := (or #174 #115)
|
|
133 |
#295 := (or #184 #292)
|
|
134 |
#298 := (or #197 #295)
|
|
135 |
#301 := (or #208 #298)
|
|
136 |
#304 := (or #211 #301)
|
|
137 |
#307 := (or #214 #304)
|
|
138 |
#310 := (or #224 #307)
|
|
139 |
#313 := (or #232 #310)
|
|
140 |
#316 := (or #244 #313)
|
|
141 |
#319 := (or #252 #316)
|
|
142 |
#322 := (or #260 #319)
|
|
143 |
#325 := (or #268 #322)
|
|
144 |
#328 := (or #273 #325)
|
|
145 |
#331 := (or #279 #328)
|
|
146 |
#334 := (or #287 #331)
|
|
147 |
#338 := (iff #334 #337)
|
|
148 |
#339 := [rewrite]: #338
|
|
149 |
#335 := (iff #160 #334)
|
|
150 |
#332 := (iff #157 #331)
|
|
151 |
#329 := (iff #154 #328)
|
|
152 |
#326 := (iff #151 #325)
|
|
153 |
#323 := (iff #148 #322)
|
|
154 |
#320 := (iff #145 #319)
|
|
155 |
#317 := (iff #142 #316)
|
|
156 |
#314 := (iff #139 #313)
|
|
157 |
#311 := (iff #136 #310)
|
|
158 |
#308 := (iff #133 #307)
|
|
159 |
#305 := (iff #130 #304)
|
|
160 |
#302 := (iff #127 #301)
|
|
161 |
#299 := (iff #124 #298)
|
|
162 |
#296 := (iff #121 #295)
|
|
163 |
#293 := (iff #118 #292)
|
|
164 |
#175 := (iff #33 #174)
|
|
165 |
#172 := (iff #23 #171)
|
|
166 |
#173 := [rewrite]: #172
|
|
167 |
#176 := [monotonicity #173]: #175
|
|
168 |
#294 := [monotonicity #176]: #293
|
|
169 |
#187 := (iff #110 #184)
|
|
170 |
#181 := (and #177 #17)
|
|
171 |
#185 := (iff #181 #184)
|
|
172 |
#186 := [rewrite]: #185
|
|
173 |
#182 := (iff #110 #181)
|
|
174 |
#179 := (iff #12 #177)
|
|
175 |
#180 := [rewrite]: #179
|
|
176 |
#183 := [monotonicity #180]: #182
|
|
177 |
#188 := [trans #183 #186]: #187
|
|
178 |
#297 := [monotonicity #188 #294]: #296
|
|
179 |
#200 := (iff #31 #197)
|
|
180 |
#194 := (and #189 #171)
|
|
181 |
#198 := (iff #194 #197)
|
|
182 |
#199 := [rewrite]: #198
|
|
183 |
#195 := (iff #31 #194)
|
|
184 |
#192 := (iff #8 #189)
|
|
185 |
#193 := [rewrite]: #192
|
|
186 |
#196 := [monotonicity #193 #173]: #195
|
|
187 |
#201 := [trans #196 #199]: #200
|
|
188 |
#300 := [monotonicity #201 #297]: #299
|
|
189 |
#209 := (iff #102 #208)
|
|
190 |
#206 := (iff #19 #205)
|
|
191 |
#207 := [rewrite]: #206
|
|
192 |
#210 := [monotonicity #207]: #209
|
|
193 |
#303 := [monotonicity #210 #300]: #302
|
|
194 |
#212 := (iff #96 #211)
|
|
195 |
#213 := [monotonicity #180 #207]: #212
|
|
196 |
#306 := [monotonicity #213 #303]: #305
|
|
197 |
#215 := (iff #93 #214)
|
|
198 |
#216 := [monotonicity #207]: #215
|
|
199 |
#309 := [monotonicity #216 #306]: #308
|
|
200 |
#227 := (iff #86 #224)
|
|
201 |
#221 := (and #217 #15)
|
|
202 |
#225 := (iff #221 #224)
|
|
203 |
#226 := [rewrite]: #225
|
|
204 |
#222 := (iff #86 #221)
|
|
205 |
#219 := (iff #6 #217)
|
|
206 |
#220 := [rewrite]: #219
|
|
207 |
#223 := [monotonicity #220]: #222
|
|
208 |
#228 := [trans #223 #226]: #227
|
|
209 |
#312 := [monotonicity #228 #309]: #311
|
|
210 |
#235 := (iff #78 #232)
|
|
211 |
#229 := (and #217 #171)
|
|
212 |
#233 := (iff #229 #232)
|
|
213 |
#234 := [rewrite]: #233
|
|
214 |
#230 := (iff #78 #229)
|
|
215 |
#231 := [monotonicity #220 #173]: #230
|
|
216 |
#236 := [trans #231 #234]: #235
|
|
217 |
#315 := [monotonicity #236 #312]: #314
|
|
218 |
#247 := (iff #75 #244)
|
|
219 |
#241 := (and #238 #17)
|
|
220 |
#245 := (iff #241 #244)
|
|
221 |
#246 := [rewrite]: #245
|
|
222 |
#242 := (iff #75 #241)
|
|
223 |
#239 := (iff #13 #238)
|
|
224 |
#240 := [rewrite]: #239
|
|
225 |
#243 := [monotonicity #240]: #242
|
|
226 |
#248 := [trans #243 #246]: #247
|
|
227 |
#318 := [monotonicity #248 #315]: #317
|
|
228 |
#255 := (iff #20 #252)
|
|
229 |
#249 := (and #238 #205)
|
|
230 |
#253 := (iff #249 #252)
|
|
231 |
#254 := [rewrite]: #253
|
|
232 |
#250 := (iff #20 #249)
|
|
233 |
#251 := [monotonicity #240 #207]: #250
|
|
234 |
#256 := [trans #251 #254]: #255
|
|
235 |
#321 := [monotonicity #256 #318]: #320
|
|
236 |
#263 := (iff #70 #260)
|
|
237 |
#257 := (and #189 #17)
|
|
238 |
#261 := (iff #257 #260)
|
|
239 |
#262 := [rewrite]: #261
|
|
240 |
#258 := (iff #70 #257)
|
|
241 |
#259 := [monotonicity #193]: #258
|
|
242 |
#264 := [trans #259 #262]: #263
|
|
243 |
#324 := [monotonicity #264 #321]: #323
|
|
244 |
#271 := (iff #67 #268)
|
|
245 |
#265 := (and #238 #15)
|
|
246 |
#269 := (iff #265 #268)
|
|
247 |
#270 := [rewrite]: #269
|
|
248 |
#266 := (iff #67 #265)
|
|
249 |
#267 := [monotonicity #240]: #266
|
|
250 |
#272 := [trans #267 #270]: #271
|
|
251 |
#327 := [monotonicity #272 #324]: #326
|
|
252 |
#274 := (iff #14 #273)
|
|
253 |
#275 := [monotonicity #180 #240]: #274
|
|
254 |
#330 := [monotonicity #275 #327]: #329
|
|
255 |
#282 := (iff #11 #279)
|
|
256 |
#276 := (and #217 #10)
|
|
257 |
#280 := (iff #276 #279)
|
|
258 |
#281 := [rewrite]: #280
|
|
259 |
#277 := (iff #11 #276)
|
|
260 |
#278 := [monotonicity #220]: #277
|
|
261 |
#283 := [trans #278 #281]: #282
|
|
262 |
#333 := [monotonicity #283 #330]: #332
|
|
263 |
#290 := (iff #9 #287)
|
|
264 |
#284 := (and #217 #189)
|
|
265 |
#288 := (iff #284 #287)
|
|
266 |
#289 := [rewrite]: #288
|
|
267 |
#285 := (iff #9 #284)
|
|
268 |
#286 := [monotonicity #220 #193]: #285
|
|
269 |
#291 := [trans #286 #289]: #290
|
|
270 |
#336 := [monotonicity #291 #333]: #335
|
|
271 |
#341 := [trans #336 #339]: #340
|
|
272 |
#344 := [monotonicity #341]: #343
|
|
273 |
#164 := (iff #50 #163)
|
|
274 |
#161 := (iff #49 #160)
|
|
275 |
#158 := (iff #48 #157)
|
|
276 |
#155 := (iff #47 #154)
|
|
277 |
#152 := (iff #46 #151)
|
|
278 |
#149 := (iff #45 #148)
|
|
279 |
#146 := (iff #44 #145)
|
|
280 |
#143 := (iff #43 #142)
|
|
281 |
#140 := (iff #42 #139)
|
|
282 |
#137 := (iff #41 #136)
|
|
283 |
#134 := (iff #40 #133)
|
|
284 |
#131 := (iff #39 #130)
|
|
285 |
#128 := (iff #38 #127)
|
|
286 |
#125 := (iff #37 #124)
|
|
287 |
#122 := (iff #36 #121)
|
|
288 |
#119 := (iff #35 #118)
|
|
289 |
#116 := (iff #34 #115)
|
|
290 |
#73 := (iff #21 #17)
|
|
291 |
#74 := [rewrite]: #73
|
|
292 |
#91 := (iff #27 #10)
|
|
293 |
#92 := [rewrite]: #91
|
|
294 |
#117 := [monotonicity #92 #74]: #116
|
|
295 |
#120 := [monotonicity #117]: #119
|
|
296 |
#113 := (iff #32 #110)
|
|
297 |
#107 := (and #17 #12)
|
|
298 |
#111 := (iff #107 #110)
|
|
299 |
#112 := [rewrite]: #111
|
|
300 |
#108 := (iff #32 #107)
|
|
301 |
#109 := [monotonicity #74]: #108
|
|
302 |
#114 := [trans #109 #112]: #113
|
|
303 |
#123 := [monotonicity #114 #120]: #122
|
|
304 |
#126 := [monotonicity #123]: #125
|
|
305 |
#105 := (iff #30 #102)
|
|
306 |
#99 := (and #19 #15)
|
|
307 |
#103 := (iff #99 #102)
|
|
308 |
#104 := [rewrite]: #103
|
|
309 |
#100 := (iff #30 #99)
|
|
310 |
#81 := (iff #25 #15)
|
|
311 |
#82 := [rewrite]: #81
|
|
312 |
#101 := [monotonicity #82]: #100
|
|
313 |
#106 := [trans #101 #104]: #105
|
|
314 |
#129 := [monotonicity #106 #126]: #128
|
|
315 |
#97 := (iff #29 #96)
|
|
316 |
#98 := [rewrite]: #97
|
|
317 |
#132 := [monotonicity #98 #129]: #131
|
|
318 |
#94 := (iff #28 #93)
|
|
319 |
#95 := [monotonicity #92]: #94
|
|
320 |
#135 := [monotonicity #95 #132]: #134
|
|
321 |
#89 := (iff #26 #86)
|
|
322 |
#83 := (and #15 #6)
|
|
323 |
#87 := (iff #83 #86)
|
|
324 |
#88 := [rewrite]: #87
|
|
325 |
#84 := (iff #26 #83)
|
|
326 |
#85 := [monotonicity #82]: #84
|
|
327 |
#90 := [trans #85 #88]: #89
|
|
328 |
#138 := [monotonicity #90 #135]: #137
|
|
329 |
#79 := (iff #24 #78)
|
|
330 |
#80 := [rewrite]: #79
|
|
331 |
#141 := [monotonicity #80 #138]: #140
|
|
332 |
#76 := (iff #22 #75)
|
|
333 |
#77 := [monotonicity #74]: #76
|
|
334 |
#144 := [monotonicity #77 #141]: #143
|
|
335 |
#147 := [monotonicity #144]: #146
|
|
336 |
#71 := (iff #18 #70)
|
|
337 |
#72 := [rewrite]: #71
|
|
338 |
#150 := [monotonicity #72 #147]: #149
|
|
339 |
#68 := (iff #16 #67)
|
|
340 |
#69 := [rewrite]: #68
|
|
341 |
#153 := [monotonicity #69 #150]: #152
|
|
342 |
#156 := [monotonicity #153]: #155
|
|
343 |
#159 := [monotonicity #156]: #158
|
|
344 |
#162 := [monotonicity #159]: #161
|
|
345 |
#165 := [monotonicity #162]: #164
|
|
346 |
#346 := [trans #165 #344]: #345
|
|
347 |
#66 := [asserted]: #50
|
|
348 |
#347 := [mp #66 #346]: #342
|
|
349 |
#355 := [not-or-elim #347]: #354
|
|
350 |
#466 := [mp #355 #465]: #455
|
|
351 |
#686 := [unit-resolution #466 #685]: #190
|
|
352 |
#427 := (or #170 #189 #238)
|
|
353 |
#350 := (not #174)
|
|
354 |
#430 := (iff #350 #427)
|
|
355 |
#382 := (or #189 #238)
|
|
356 |
#414 := (or #170 #382)
|
|
357 |
#428 := (iff #414 #427)
|
|
358 |
#429 := [rewrite]: #428
|
|
359 |
#425 := (iff #350 #414)
|
|
360 |
#415 := (not #414)
|
|
361 |
#420 := (not #415)
|
|
362 |
#423 := (iff #420 #414)
|
|
363 |
#424 := [rewrite]: #423
|
|
364 |
#421 := (iff #350 #420)
|
|
365 |
#418 := (iff #174 #415)
|
|
366 |
#380 := (not #382)
|
|
367 |
#411 := (and #380 #171)
|
|
368 |
#416 := (iff #411 #415)
|
|
369 |
#417 := [rewrite]: #416
|
|
370 |
#412 := (iff #174 #411)
|
|
371 |
#383 := (iff #10 #380)
|
|
372 |
#384 := [rewrite]: #383
|
|
373 |
#413 := [monotonicity #384]: #412
|
|
374 |
#419 := [trans #413 #417]: #418
|
|
375 |
#422 := [monotonicity #419]: #421
|
|
376 |
#426 := [trans #422 #424]: #425
|
|
377 |
#431 := [trans #426 #429]: #430
|
|
378 |
#351 := [not-or-elim #347]: #350
|
|
379 |
#432 := [mp #351 #431]: #427
|
|
380 |
#687 := [unit-resolution #432 #686 #685]: #238
|
|
381 |
#549 := (or #170 #218)
|
|
382 |
#364 := (not #232)
|
|
383 |
#558 := (iff #364 #549)
|
|
384 |
#550 := (not #549)
|
|
385 |
#553 := (not #550)
|
|
386 |
#556 := (iff #553 #549)
|
|
387 |
#557 := [rewrite]: #556
|
|
388 |
#554 := (iff #364 #553)
|
|
389 |
#551 := (iff #232 #550)
|
|
390 |
#552 := [rewrite]: #551
|
|
391 |
#555 := [monotonicity #552]: #554
|
|
392 |
#559 := [trans #555 #557]: #558
|
|
393 |
#365 := [not-or-elim #347]: #364
|
|
394 |
#560 := [mp #365 #559]: #549
|
|
395 |
#688 := [unit-resolution #560 #685]: #218
|
|
396 |
#577 := (or #205 #217 #237)
|
|
397 |
#366 := (not #244)
|
|
398 |
#580 := (iff #366 #577)
|
|
399 |
#385 := (or #205 #217)
|
|
400 |
#564 := (or #237 #385)
|
|
401 |
#578 := (iff #564 #577)
|
|
402 |
#579 := [rewrite]: #578
|
|
403 |
#575 := (iff #366 #564)
|
|
404 |
#565 := (not #564)
|
|
405 |
#570 := (not #565)
|
|
406 |
#573 := (iff #570 #564)
|
|
407 |
#574 := [rewrite]: #573
|
|
408 |
#571 := (iff #366 #570)
|
|
409 |
#568 := (iff #244 #565)
|
|
410 |
#386 := (not #385)
|
|
411 |
#561 := (and #386 #238)
|
|
412 |
#566 := (iff #561 #565)
|
|
413 |
#567 := [rewrite]: #566
|
|
414 |
#562 := (iff #244 #561)
|
|
415 |
#387 := (iff #17 #386)
|
|
416 |
#388 := [rewrite]: #387
|
|
417 |
#563 := [monotonicity #388]: #562
|
|
418 |
#569 := [trans #563 #567]: #568
|
|
419 |
#572 := [monotonicity #569]: #571
|
|
420 |
#576 := [trans #572 #574]: #575
|
|
421 |
#581 := [trans #576 #579]: #580
|
|
422 |
#367 := [not-or-elim #347]: #366
|
|
423 |
#582 := [mp #367 #581]: #577
|
|
424 |
#689 := [unit-resolution #582 #688 #687]: #205
|
|
425 |
#583 := (or #204 #237)
|
|
426 |
#368 := (not #252)
|
|
427 |
#592 := (iff #368 #583)
|
|
428 |
#584 := (not #583)
|
|
429 |
#587 := (not #584)
|
|
430 |
#590 := (iff #587 #583)
|
|
431 |
#591 := [rewrite]: #590
|
|
432 |
#588 := (iff #368 #587)
|
|
433 |
#585 := (iff #252 #584)
|
|
434 |
#586 := [rewrite]: #585
|
|
435 |
#589 := [monotonicity #586]: #588
|
|
436 |
#593 := [trans #589 #591]: #592
|
|
437 |
#369 := [not-or-elim #347]: #368
|
|
438 |
#594 := [mp #369 #593]: #583
|
|
439 |
#690 := [unit-resolution #594 #689 #687]: false
|
|
440 |
#691 := [lemma #690]: #170
|
|
441 |
#487 := (or #171 #177 #204)
|
|
442 |
#356 := (not #208)
|
|
443 |
#490 := (iff #356 #487)
|
|
444 |
#467 := (or #171 #177)
|
|
445 |
#474 := (or #204 #467)
|
|
446 |
#488 := (iff #474 #487)
|
|
447 |
#489 := [rewrite]: #488
|
|
448 |
#485 := (iff #356 #474)
|
|
449 |
#475 := (not #474)
|
|
450 |
#480 := (not #475)
|
|
451 |
#483 := (iff #480 #474)
|
|
452 |
#484 := [rewrite]: #483
|
|
453 |
#481 := (iff #356 #480)
|
|
454 |
#478 := (iff #208 #475)
|
|
455 |
#468 := (not #467)
|
|
456 |
#471 := (and #468 #205)
|
|
457 |
#476 := (iff #471 #475)
|
|
458 |
#477 := [rewrite]: #476
|
|
459 |
#472 := (iff #208 #471)
|
|
460 |
#469 := (iff #15 #468)
|
|
461 |
#470 := [rewrite]: #469
|
|
462 |
#473 := [monotonicity #470]: #472
|
|
463 |
#479 := [trans #473 #477]: #478
|
|
464 |
#482 := [monotonicity #479]: #481
|
|
465 |
#486 := [trans #482 #484]: #485
|
|
466 |
#491 := [trans #486 #489]: #490
|
|
467 |
#357 := [not-or-elim #347]: #356
|
|
468 |
#492 := [mp #357 #491]: #487
|
|
469 |
#694 := [unit-resolution #492 #691]: #693
|
|
470 |
#695 := [unit-resolution #694 #692]: #177
|
|
471 |
#493 := (or #178 #204)
|
|
472 |
#358 := (not #211)
|
|
473 |
#502 := (iff #358 #493)
|
|
474 |
#494 := (not #493)
|
|
475 |
#497 := (not #494)
|
|
476 |
#500 := (iff #497 #493)
|
|
477 |
#501 := [rewrite]: #500
|
|
478 |
#498 := (iff #358 #497)
|
|
479 |
#495 := (iff #211 #494)
|
|
480 |
#496 := [rewrite]: #495
|
|
481 |
#499 := [monotonicity #496]: #498
|
|
482 |
#503 := [trans #499 #501]: #502
|
|
483 |
#359 := [not-or-elim #347]: #358
|
|
484 |
#504 := [mp #359 #503]: #493
|
|
485 |
#696 := [unit-resolution #504 #695 #692]: false
|
|
486 |
#697 := [lemma #696]: #204
|
|
487 |
#698 := [hypothesis]: #177
|
|
488 |
#449 := (or #178 #205 #217)
|
|
489 |
#352 := (not #184)
|
|
490 |
#452 := (iff #352 #449)
|
|
491 |
#436 := (or #178 #385)
|
|
492 |
#450 := (iff #436 #449)
|
|
493 |
#451 := [rewrite]: #450
|
|
494 |
#447 := (iff #352 #436)
|
|
495 |
#437 := (not #436)
|
|
496 |
#442 := (not #437)
|
|
497 |
#445 := (iff #442 #436)
|
|
498 |
#446 := [rewrite]: #445
|
|
499 |
#443 := (iff #352 #442)
|
|
500 |
#440 := (iff #184 #437)
|
|
501 |
#433 := (and #386 #177)
|
|
502 |
#438 := (iff #433 #437)
|
|
503 |
#439 := [rewrite]: #438
|
|
504 |
#434 := (iff #184 #433)
|
|
505 |
#435 := [monotonicity #388]: #434
|
|
506 |
#441 := [trans #435 #439]: #440
|
|
507 |
#444 := [monotonicity #441]: #443
|
|
508 |
#448 := [trans #444 #446]: #447
|
|
509 |
#453 := [trans #448 #451]: #452
|
|
510 |
#353 := [not-or-elim #347]: #352
|
|
511 |
#454 := [mp #353 #453]: #449
|
|
512 |
#699 := [unit-resolution #454 #698 #697]: #217
|
|
513 |
#639 := (or #178 #237)
|
|
514 |
#374 := (not #273)
|
|
515 |
#648 := (iff #374 #639)
|
|
516 |
#640 := (not #639)
|
|
517 |
#643 := (not #640)
|
|
518 |
#646 := (iff #643 #639)
|
|
519 |
#647 := [rewrite]: #646
|
|
520 |
#644 := (iff #374 #643)
|
|
521 |
#641 := (iff #273 #640)
|
|
522 |
#642 := [rewrite]: #641
|
|
523 |
#645 := [monotonicity #642]: #644
|
|
524 |
#649 := [trans #645 #647]: #648
|
|
525 |
#375 := [not-or-elim #347]: #374
|
|
526 |
#650 := [mp #375 #649]: #639
|
|
527 |
#700 := [unit-resolution #650 #698]: #237
|
|
528 |
#667 := (or #189 #218 #238)
|
|
529 |
#376 := (not #279)
|
|
530 |
#670 := (iff #376 #667)
|
|
531 |
#654 := (or #218 #382)
|
|
532 |
#668 := (iff #654 #667)
|
|
533 |
#669 := [rewrite]: #668
|
|
534 |
#665 := (iff #376 #654)
|
|
535 |
#655 := (not #654)
|
|
536 |
#660 := (not #655)
|
|
537 |
#663 := (iff #660 #654)
|
|
538 |
#664 := [rewrite]: #663
|
|
539 |
#661 := (iff #376 #660)
|
|
540 |
#658 := (iff #279 #655)
|
|
541 |
#651 := (and #380 #217)
|
|
542 |
#656 := (iff #651 #655)
|
|
543 |
#657 := [rewrite]: #656
|
|
544 |
#652 := (iff #279 #651)
|
|
545 |
#653 := [monotonicity #384]: #652
|
|
546 |
#659 := [trans #653 #657]: #658
|
|
547 |
#662 := [monotonicity #659]: #661
|
|
548 |
#666 := [trans #662 #664]: #665
|
|
549 |
#671 := [trans #666 #669]: #670
|
|
550 |
#377 := [not-or-elim #347]: #376
|
|
551 |
#672 := [mp #377 #671]: #667
|
|
552 |
#701 := [unit-resolution #672 #699 #700]: #189
|
|
553 |
#673 := (or #190 #218)
|
|
554 |
#378 := (not #287)
|
|
555 |
#682 := (iff #378 #673)
|
|
556 |
#674 := (not #673)
|
|
557 |
#677 := (not #674)
|
|
558 |
#680 := (iff #677 #673)
|
|
559 |
#681 := [rewrite]: #680
|
|
560 |
#678 := (iff #378 #677)
|
|
561 |
#675 := (iff #287 #674)
|
|
562 |
#676 := [rewrite]: #675
|
|
563 |
#679 := [monotonicity #676]: #678
|
|
564 |
#683 := [trans #679 #681]: #682
|
|
565 |
#379 := [not-or-elim #347]: #378
|
|
566 |
#684 := [mp #379 #683]: #673
|
|
567 |
#702 := [unit-resolution #684 #701 #699]: false
|
|
568 |
#703 := [lemma #702]: #178
|
|
569 |
#704 := (or #177 #218)
|
|
570 |
#543 := (or #171 #177 #218)
|
|
571 |
#362 := (not #224)
|
|
572 |
#546 := (iff #362 #543)
|
|
573 |
#530 := (or #218 #467)
|
|
574 |
#544 := (iff #530 #543)
|
|
575 |
#545 := [rewrite]: #544
|
|
576 |
#541 := (iff #362 #530)
|
|
577 |
#531 := (not #530)
|
|
578 |
#536 := (not #531)
|
|
579 |
#539 := (iff #536 #530)
|
|
580 |
#540 := [rewrite]: #539
|
|
581 |
#537 := (iff #362 #536)
|
|
582 |
#534 := (iff #224 #531)
|
|
583 |
#527 := (and #468 #217)
|
|
584 |
#532 := (iff #527 #531)
|
|
585 |
#533 := [rewrite]: #532
|
|
586 |
#528 := (iff #224 #527)
|
|
587 |
#529 := [monotonicity #470]: #528
|
|
588 |
#535 := [trans #529 #533]: #534
|
|
589 |
#538 := [monotonicity #535]: #537
|
|
590 |
#542 := [trans #538 #540]: #541
|
|
591 |
#547 := [trans #542 #545]: #546
|
|
592 |
#363 := [not-or-elim #347]: #362
|
|
593 |
#548 := [mp #363 #547]: #543
|
|
594 |
#705 := [unit-resolution #548 #691]: #704
|
|
595 |
#706 := [unit-resolution #705 #703]: #218
|
|
596 |
#707 := (or #177 #237)
|
|
597 |
#633 := (or #171 #177 #237)
|
|
598 |
#372 := (not #268)
|
|
599 |
#636 := (iff #372 #633)
|
|
600 |
#620 := (or #237 #467)
|
|
601 |
#634 := (iff #620 #633)
|
|
602 |
#635 := [rewrite]: #634
|
|
603 |
#631 := (iff #372 #620)
|
|
604 |
#621 := (not #620)
|
|
605 |
#626 := (not #621)
|
|
606 |
#629 := (iff #626 #620)
|
|
607 |
#630 := [rewrite]: #629
|
|
608 |
#627 := (iff #372 #626)
|
|
609 |
#624 := (iff #268 #621)
|
|
610 |
#617 := (and #468 #238)
|
|
611 |
#622 := (iff #617 #621)
|
|
612 |
#623 := [rewrite]: #622
|
|
613 |
#618 := (iff #268 #617)
|
|
614 |
#619 := [monotonicity #470]: #618
|
|
615 |
#625 := [trans #619 #623]: #624
|
|
616 |
#628 := [monotonicity #625]: #627
|
|
617 |
#632 := [trans #628 #630]: #631
|
|
618 |
#637 := [trans #632 #635]: #636
|
|
619 |
#373 := [not-or-elim #347]: #372
|
|
620 |
#638 := [mp #373 #637]: #633
|
|
621 |
#708 := [unit-resolution #638 #691]: #707
|
|
622 |
#709 := [unit-resolution #708 #703]: #237
|
|
623 |
#611 := (or #190 #205 #217)
|
|
624 |
#370 := (not #260)
|
|
625 |
#614 := (iff #370 #611)
|
|
626 |
#598 := (or #190 #385)
|
|
627 |
#612 := (iff #598 #611)
|
|
628 |
#613 := [rewrite]: #612
|
|
629 |
#609 := (iff #370 #598)
|
|
630 |
#599 := (not #598)
|
|
631 |
#604 := (not #599)
|
|
632 |
#607 := (iff #604 #598)
|
|
633 |
#608 := [rewrite]: #607
|
|
634 |
#605 := (iff #370 #604)
|
|
635 |
#602 := (iff #260 #599)
|
|
636 |
#595 := (and #386 #189)
|
|
637 |
#600 := (iff #595 #599)
|
|
638 |
#601 := [rewrite]: #600
|
|
639 |
#596 := (iff #260 #595)
|
|
640 |
#597 := [monotonicity #388]: #596
|
|
641 |
#603 := [trans #597 #601]: #602
|
|
642 |
#606 := [monotonicity #603]: #605
|
|
643 |
#610 := [trans #606 #608]: #609
|
|
644 |
#615 := [trans #610 #613]: #614
|
|
645 |
#371 := [not-or-elim #347]: #370
|
|
646 |
#616 := [mp #371 #615]: #611
|
|
647 |
#710 := [unit-resolution #616 #706 #697]: #190
|
|
648 |
#405 := (or #189 #205 #217 #238)
|
|
649 |
#348 := (not #115)
|
|
650 |
#408 := (iff #348 #405)
|
|
651 |
#392 := (or #382 #385)
|
|
652 |
#406 := (iff #392 #405)
|
|
653 |
#407 := [rewrite]: #406
|
|
654 |
#403 := (iff #348 #392)
|
|
655 |
#393 := (not #392)
|
|
656 |
#398 := (not #393)
|
|
657 |
#401 := (iff #398 #392)
|
|
658 |
#402 := [rewrite]: #401
|
|
659 |
#399 := (iff #348 #398)
|
|
660 |
#396 := (iff #115 #393)
|
|
661 |
#389 := (and #380 #386)
|
|
662 |
#394 := (iff #389 #393)
|
|
663 |
#395 := [rewrite]: #394
|
|
664 |
#390 := (iff #115 #389)
|
|
665 |
#391 := [monotonicity #384 #388]: #390
|
|
666 |
#397 := [trans #391 #395]: #396
|
|
667 |
#400 := [monotonicity #397]: #399
|
|
668 |
#404 := [trans #400 #402]: #403
|
|
669 |
#409 := [trans #404 #407]: #408
|
|
670 |
#349 := [not-or-elim #347]: #348
|
|
671 |
#410 := [mp #349 #409]: #405
|
|
672 |
[unit-resolution #410 #710 #709 #697 #706]: false
|
|
673 |
unsat
|