35172
|
1 |
tB2Atlor9W4pSnrAz5nHpw 907 0
|
|
2 |
#2 := false
|
|
3 |
#299 := 0::real
|
|
4 |
decl uf_1 :: (-> T3 T2 real)
|
|
5 |
decl uf_10 :: (-> T4 T2)
|
|
6 |
decl uf_7 :: T4
|
|
7 |
#15 := uf_7
|
|
8 |
#22 := (uf_10 uf_7)
|
|
9 |
decl uf_2 :: (-> T1 T3)
|
|
10 |
decl uf_4 :: T1
|
|
11 |
#11 := uf_4
|
|
12 |
#91 := (uf_2 uf_4)
|
|
13 |
#902 := (uf_1 #91 #22)
|
|
14 |
#297 := -1::real
|
|
15 |
#1084 := (* -1::real #902)
|
|
16 |
decl uf_16 :: T1
|
|
17 |
#50 := uf_16
|
|
18 |
#78 := (uf_2 uf_16)
|
|
19 |
#799 := (uf_1 #78 #22)
|
|
20 |
#1267 := (+ #799 #1084)
|
|
21 |
#1272 := (>= #1267 0::real)
|
|
22 |
#1266 := (= #799 #902)
|
|
23 |
decl uf_9 :: T3
|
|
24 |
#21 := uf_9
|
|
25 |
#23 := (uf_1 uf_9 #22)
|
|
26 |
#905 := (= #23 #902)
|
|
27 |
decl uf_11 :: T3
|
|
28 |
#24 := uf_11
|
|
29 |
#850 := (uf_1 uf_11 #22)
|
|
30 |
#904 := (= #850 #902)
|
|
31 |
decl uf_6 :: (-> T2 T4)
|
|
32 |
#74 := (uf_6 #22)
|
|
33 |
#281 := (= uf_7 #74)
|
|
34 |
#922 := (ite #281 #905 #904)
|
|
35 |
decl uf_8 :: T3
|
|
36 |
#18 := uf_8
|
|
37 |
#848 := (uf_1 uf_8 #22)
|
|
38 |
#903 := (= #848 #902)
|
|
39 |
#60 := 0::int
|
|
40 |
decl uf_5 :: (-> T4 int)
|
|
41 |
#803 := (uf_5 #74)
|
|
42 |
#117 := -1::int
|
|
43 |
#813 := (* -1::int #803)
|
|
44 |
#16 := (uf_5 uf_7)
|
|
45 |
#916 := (+ #16 #813)
|
|
46 |
#917 := (<= #916 0::int)
|
|
47 |
#925 := (ite #917 #922 #903)
|
|
48 |
#6 := (:var 0 T2)
|
|
49 |
#19 := (uf_1 uf_8 #6)
|
|
50 |
#544 := (pattern #19)
|
|
51 |
#25 := (uf_1 uf_11 #6)
|
|
52 |
#543 := (pattern #25)
|
|
53 |
#92 := (uf_1 #91 #6)
|
|
54 |
#542 := (pattern #92)
|
|
55 |
#13 := (uf_6 #6)
|
|
56 |
#541 := (pattern #13)
|
|
57 |
#447 := (= #19 #92)
|
|
58 |
#445 := (= #25 #92)
|
|
59 |
#444 := (= #23 #92)
|
|
60 |
#20 := (= #13 uf_7)
|
|
61 |
#446 := (ite #20 #444 #445)
|
|
62 |
#120 := (* -1::int #16)
|
|
63 |
#14 := (uf_5 #13)
|
|
64 |
#121 := (+ #14 #120)
|
|
65 |
#119 := (>= #121 0::int)
|
|
66 |
#448 := (ite #119 #446 #447)
|
|
67 |
#545 := (forall (vars (?x3 T2)) (:pat #541 #542 #543 #544) #448)
|
|
68 |
#451 := (forall (vars (?x3 T2)) #448)
|
|
69 |
#548 := (iff #451 #545)
|
|
70 |
#546 := (iff #448 #448)
|
|
71 |
#547 := [refl]: #546
|
|
72 |
#549 := [quant-intro #547]: #548
|
|
73 |
#26 := (ite #20 #23 #25)
|
|
74 |
#127 := (ite #119 #26 #19)
|
|
75 |
#368 := (= #92 #127)
|
|
76 |
#369 := (forall (vars (?x3 T2)) #368)
|
|
77 |
#452 := (iff #369 #451)
|
|
78 |
#449 := (iff #368 #448)
|
|
79 |
#450 := [rewrite]: #449
|
|
80 |
#453 := [quant-intro #450]: #452
|
|
81 |
#392 := (~ #369 #369)
|
|
82 |
#390 := (~ #368 #368)
|
|
83 |
#391 := [refl]: #390
|
|
84 |
#366 := [nnf-pos #391]: #392
|
|
85 |
decl uf_3 :: (-> T1 T2 real)
|
|
86 |
#12 := (uf_3 uf_4 #6)
|
|
87 |
#132 := (= #12 #127)
|
|
88 |
#135 := (forall (vars (?x3 T2)) #132)
|
|
89 |
#370 := (iff #135 #369)
|
|
90 |
#4 := (:var 1 T1)
|
|
91 |
#8 := (uf_3 #4 #6)
|
|
92 |
#5 := (uf_2 #4)
|
|
93 |
#7 := (uf_1 #5 #6)
|
|
94 |
#9 := (= #7 #8)
|
|
95 |
#10 := (forall (vars (?x1 T1) (?x2 T2)) #9)
|
|
96 |
#113 := [asserted]: #10
|
|
97 |
#371 := [rewrite* #113]: #370
|
|
98 |
#17 := (< #14 #16)
|
|
99 |
#27 := (ite #17 #19 #26)
|
|
100 |
#28 := (= #12 #27)
|
|
101 |
#29 := (forall (vars (?x3 T2)) #28)
|
|
102 |
#136 := (iff #29 #135)
|
|
103 |
#133 := (iff #28 #132)
|
|
104 |
#130 := (= #27 #127)
|
|
105 |
#118 := (not #119)
|
|
106 |
#124 := (ite #118 #19 #26)
|
|
107 |
#128 := (= #124 #127)
|
|
108 |
#129 := [rewrite]: #128
|
|
109 |
#125 := (= #27 #124)
|
|
110 |
#122 := (iff #17 #118)
|
|
111 |
#123 := [rewrite]: #122
|
|
112 |
#126 := [monotonicity #123]: #125
|
|
113 |
#131 := [trans #126 #129]: #130
|
|
114 |
#134 := [monotonicity #131]: #133
|
|
115 |
#137 := [quant-intro #134]: #136
|
|
116 |
#114 := [asserted]: #29
|
|
117 |
#138 := [mp #114 #137]: #135
|
|
118 |
#372 := [mp #138 #371]: #369
|
|
119 |
#367 := [mp~ #372 #366]: #369
|
|
120 |
#454 := [mp #367 #453]: #451
|
|
121 |
#550 := [mp #454 #549]: #545
|
|
122 |
#738 := (not #545)
|
|
123 |
#928 := (or #738 #925)
|
|
124 |
#75 := (= #74 uf_7)
|
|
125 |
#906 := (ite #75 #905 #904)
|
|
126 |
#907 := (+ #803 #120)
|
|
127 |
#908 := (>= #907 0::int)
|
|
128 |
#909 := (ite #908 #906 #903)
|
|
129 |
#929 := (or #738 #909)
|
|
130 |
#931 := (iff #929 #928)
|
|
131 |
#933 := (iff #928 #928)
|
|
132 |
#934 := [rewrite]: #933
|
|
133 |
#926 := (iff #909 #925)
|
|
134 |
#923 := (iff #906 #922)
|
|
135 |
#283 := (iff #75 #281)
|
|
136 |
#284 := [rewrite]: #283
|
|
137 |
#924 := [monotonicity #284]: #923
|
|
138 |
#920 := (iff #908 #917)
|
|
139 |
#910 := (+ #120 #803)
|
|
140 |
#913 := (>= #910 0::int)
|
|
141 |
#918 := (iff #913 #917)
|
|
142 |
#919 := [rewrite]: #918
|
|
143 |
#914 := (iff #908 #913)
|
|
144 |
#911 := (= #907 #910)
|
|
145 |
#912 := [rewrite]: #911
|
|
146 |
#915 := [monotonicity #912]: #914
|
|
147 |
#921 := [trans #915 #919]: #920
|
|
148 |
#927 := [monotonicity #921 #924]: #926
|
|
149 |
#932 := [monotonicity #927]: #931
|
|
150 |
#935 := [trans #932 #934]: #931
|
|
151 |
#930 := [quant-inst]: #929
|
|
152 |
#936 := [mp #930 #935]: #928
|
|
153 |
#1300 := [unit-resolution #936 #550]: #925
|
|
154 |
#989 := (= #16 #803)
|
|
155 |
#1277 := (= #803 #16)
|
|
156 |
#280 := [asserted]: #75
|
|
157 |
#287 := [mp #280 #284]: #281
|
|
158 |
#1276 := [symm #287]: #75
|
|
159 |
#1278 := [monotonicity #1276]: #1277
|
|
160 |
#1301 := [symm #1278]: #989
|
|
161 |
#1302 := (not #989)
|
|
162 |
#1303 := (or #1302 #917)
|
|
163 |
#1304 := [th-lemma]: #1303
|
|
164 |
#1305 := [unit-resolution #1304 #1301]: #917
|
|
165 |
#950 := (not #917)
|
|
166 |
#949 := (not #925)
|
|
167 |
#951 := (or #949 #950 #922)
|
|
168 |
#952 := [def-axiom]: #951
|
|
169 |
#1306 := [unit-resolution #952 #1305 #1300]: #922
|
|
170 |
#937 := (not #922)
|
|
171 |
#1307 := (or #937 #905)
|
|
172 |
#938 := (not #281)
|
|
173 |
#939 := (or #937 #938 #905)
|
|
174 |
#940 := [def-axiom]: #939
|
|
175 |
#1308 := [unit-resolution #940 #287]: #1307
|
|
176 |
#1309 := [unit-resolution #1308 #1306]: #905
|
|
177 |
#1356 := (= #799 #23)
|
|
178 |
#800 := (= #23 #799)
|
|
179 |
decl uf_15 :: T4
|
|
180 |
#40 := uf_15
|
|
181 |
#41 := (uf_5 uf_15)
|
|
182 |
#814 := (+ #41 #813)
|
|
183 |
#815 := (<= #814 0::int)
|
|
184 |
#836 := (not #815)
|
|
185 |
#158 := (* -1::int #41)
|
|
186 |
#1270 := (+ #16 #158)
|
|
187 |
#1265 := (>= #1270 0::int)
|
|
188 |
#1339 := (not #1265)
|
|
189 |
#1269 := (= #16 #41)
|
|
190 |
#1298 := (not #1269)
|
|
191 |
#286 := (= uf_7 uf_15)
|
|
192 |
#44 := (uf_10 uf_15)
|
|
193 |
#72 := (uf_6 #44)
|
|
194 |
#73 := (= #72 uf_15)
|
|
195 |
#277 := (= uf_15 #72)
|
|
196 |
#278 := (iff #73 #277)
|
|
197 |
#279 := [rewrite]: #278
|
|
198 |
#276 := [asserted]: #73
|
|
199 |
#282 := [mp #276 #279]: #277
|
|
200 |
#1274 := [symm #282]: #73
|
|
201 |
#729 := (= uf_7 #72)
|
|
202 |
decl uf_17 :: (-> int T4)
|
|
203 |
#611 := (uf_5 #72)
|
|
204 |
#991 := (uf_17 #611)
|
|
205 |
#1289 := (= #991 #72)
|
|
206 |
#992 := (= #72 #991)
|
|
207 |
#55 := (:var 0 T4)
|
|
208 |
#56 := (uf_5 #55)
|
|
209 |
#574 := (pattern #56)
|
|
210 |
#57 := (uf_17 #56)
|
|
211 |
#177 := (= #55 #57)
|
|
212 |
#575 := (forall (vars (?x7 T4)) (:pat #574) #177)
|
|
213 |
#195 := (forall (vars (?x7 T4)) #177)
|
|
214 |
#578 := (iff #195 #575)
|
|
215 |
#576 := (iff #177 #177)
|
|
216 |
#577 := [refl]: #576
|
|
217 |
#579 := [quant-intro #577]: #578
|
|
218 |
#405 := (~ #195 #195)
|
|
219 |
#403 := (~ #177 #177)
|
|
220 |
#404 := [refl]: #403
|
|
221 |
#406 := [nnf-pos #404]: #405
|
|
222 |
#58 := (= #57 #55)
|
|
223 |
#59 := (forall (vars (?x7 T4)) #58)
|
|
224 |
#196 := (iff #59 #195)
|
|
225 |
#193 := (iff #58 #177)
|
|
226 |
#194 := [rewrite]: #193
|
|
227 |
#197 := [quant-intro #194]: #196
|
|
228 |
#155 := [asserted]: #59
|
|
229 |
#200 := [mp #155 #197]: #195
|
|
230 |
#407 := [mp~ #200 #406]: #195
|
|
231 |
#580 := [mp #407 #579]: #575
|
|
232 |
#995 := (not #575)
|
|
233 |
#996 := (or #995 #992)
|
|
234 |
#997 := [quant-inst]: #996
|
|
235 |
#1273 := [unit-resolution #997 #580]: #992
|
|
236 |
#1290 := [symm #1273]: #1289
|
|
237 |
#1293 := (= uf_7 #991)
|
|
238 |
#993 := (uf_17 #803)
|
|
239 |
#1287 := (= #993 #991)
|
|
240 |
#1284 := (= #803 #611)
|
|
241 |
#987 := (= #41 #611)
|
|
242 |
#1279 := (= #611 #41)
|
|
243 |
#1280 := [monotonicity #1274]: #1279
|
|
244 |
#1281 := [symm #1280]: #987
|
|
245 |
#1282 := (= #803 #41)
|
|
246 |
#1275 := [hypothesis]: #1269
|
|
247 |
#1283 := [trans #1278 #1275]: #1282
|
|
248 |
#1285 := [trans #1283 #1281]: #1284
|
|
249 |
#1288 := [monotonicity #1285]: #1287
|
|
250 |
#1291 := (= uf_7 #993)
|
|
251 |
#994 := (= #74 #993)
|
|
252 |
#1000 := (or #995 #994)
|
|
253 |
#1001 := [quant-inst]: #1000
|
|
254 |
#1286 := [unit-resolution #1001 #580]: #994
|
|
255 |
#1292 := [trans #287 #1286]: #1291
|
|
256 |
#1294 := [trans #1292 #1288]: #1293
|
|
257 |
#1295 := [trans #1294 #1290]: #729
|
|
258 |
#1296 := [trans #1295 #1274]: #286
|
|
259 |
#290 := (not #286)
|
|
260 |
#76 := (= uf_15 uf_7)
|
|
261 |
#77 := (not #76)
|
|
262 |
#291 := (iff #77 #290)
|
|
263 |
#288 := (iff #76 #286)
|
|
264 |
#289 := [rewrite]: #288
|
|
265 |
#292 := [monotonicity #289]: #291
|
|
266 |
#285 := [asserted]: #77
|
|
267 |
#295 := [mp #285 #292]: #290
|
|
268 |
#1297 := [unit-resolution #295 #1296]: false
|
|
269 |
#1299 := [lemma #1297]: #1298
|
|
270 |
#1342 := (or #1269 #1339)
|
|
271 |
#1271 := (<= #1270 0::int)
|
|
272 |
#621 := (* -1::int #611)
|
|
273 |
#723 := (+ #16 #621)
|
|
274 |
#724 := (<= #723 0::int)
|
|
275 |
decl uf_12 :: T1
|
|
276 |
#30 := uf_12
|
|
277 |
#88 := (uf_2 uf_12)
|
|
278 |
#771 := (uf_1 #88 #44)
|
|
279 |
#45 := (uf_1 uf_9 #44)
|
|
280 |
#772 := (= #45 #771)
|
|
281 |
#796 := (not #772)
|
|
282 |
decl uf_14 :: T1
|
|
283 |
#38 := uf_14
|
|
284 |
#83 := (uf_2 uf_14)
|
|
285 |
#656 := (uf_1 #83 #44)
|
|
286 |
#1239 := (= #656 #771)
|
|
287 |
#1252 := (not #1239)
|
|
288 |
#1324 := (iff #1252 #796)
|
|
289 |
#1322 := (iff #1239 #772)
|
|
290 |
#1320 := (= #656 #45)
|
|
291 |
#661 := (= #45 #656)
|
|
292 |
#659 := (uf_1 uf_11 #44)
|
|
293 |
#664 := (= #656 #659)
|
|
294 |
#667 := (ite #277 #661 #664)
|
|
295 |
#657 := (uf_1 uf_8 #44)
|
|
296 |
#670 := (= #656 #657)
|
|
297 |
#622 := (+ #41 #621)
|
|
298 |
#623 := (<= #622 0::int)
|
|
299 |
#673 := (ite #623 #667 #670)
|
|
300 |
#84 := (uf_1 #83 #6)
|
|
301 |
#560 := (pattern #84)
|
|
302 |
#467 := (= #19 #84)
|
|
303 |
#465 := (= #25 #84)
|
|
304 |
#464 := (= #45 #84)
|
|
305 |
#43 := (= #13 uf_15)
|
|
306 |
#466 := (ite #43 #464 #465)
|
|
307 |
#159 := (+ #14 #158)
|
|
308 |
#157 := (>= #159 0::int)
|
|
309 |
#468 := (ite #157 #466 #467)
|
|
310 |
#561 := (forall (vars (?x5 T2)) (:pat #541 #560 #543 #544) #468)
|
|
311 |
#471 := (forall (vars (?x5 T2)) #468)
|
|
312 |
#564 := (iff #471 #561)
|
|
313 |
#562 := (iff #468 #468)
|
|
314 |
#563 := [refl]: #562
|
|
315 |
#565 := [quant-intro #563]: #564
|
|
316 |
#46 := (ite #43 #45 #25)
|
|
317 |
#165 := (ite #157 #46 #19)
|
|
318 |
#378 := (= #84 #165)
|
|
319 |
#379 := (forall (vars (?x5 T2)) #378)
|
|
320 |
#472 := (iff #379 #471)
|
|
321 |
#469 := (iff #378 #468)
|
|
322 |
#470 := [rewrite]: #469
|
|
323 |
#473 := [quant-intro #470]: #472
|
|
324 |
#359 := (~ #379 #379)
|
|
325 |
#361 := (~ #378 #378)
|
|
326 |
#358 := [refl]: #361
|
|
327 |
#356 := [nnf-pos #358]: #359
|
|
328 |
#39 := (uf_3 uf_14 #6)
|
|
329 |
#170 := (= #39 #165)
|
|
330 |
#173 := (forall (vars (?x5 T2)) #170)
|
|
331 |
#380 := (iff #173 #379)
|
|
332 |
#381 := [rewrite* #113]: #380
|
|
333 |
#42 := (< #14 #41)
|
|
334 |
#47 := (ite #42 #19 #46)
|
|
335 |
#48 := (= #39 #47)
|
|
336 |
#49 := (forall (vars (?x5 T2)) #48)
|
|
337 |
#174 := (iff #49 #173)
|
|
338 |
#171 := (iff #48 #170)
|
|
339 |
#168 := (= #47 #165)
|
|
340 |
#156 := (not #157)
|
|
341 |
#162 := (ite #156 #19 #46)
|
|
342 |
#166 := (= #162 #165)
|
|
343 |
#167 := [rewrite]: #166
|
|
344 |
#163 := (= #47 #162)
|
|
345 |
#160 := (iff #42 #156)
|
|
346 |
#161 := [rewrite]: #160
|
|
347 |
#164 := [monotonicity #161]: #163
|
|
348 |
#169 := [trans #164 #167]: #168
|
|
349 |
#172 := [monotonicity #169]: #171
|
|
350 |
#175 := [quant-intro #172]: #174
|
|
351 |
#116 := [asserted]: #49
|
|
352 |
#176 := [mp #116 #175]: #173
|
|
353 |
#382 := [mp #176 #381]: #379
|
|
354 |
#357 := [mp~ #382 #356]: #379
|
|
355 |
#474 := [mp #357 #473]: #471
|
|
356 |
#566 := [mp #474 #565]: #561
|
|
357 |
#676 := (not #561)
|
|
358 |
#677 := (or #676 #673)
|
|
359 |
#658 := (= #657 #656)
|
|
360 |
#660 := (= #659 #656)
|
|
361 |
#662 := (ite #73 #661 #660)
|
|
362 |
#612 := (+ #611 #158)
|
|
363 |
#613 := (>= #612 0::int)
|
|
364 |
#663 := (ite #613 #662 #658)
|
|
365 |
#678 := (or #676 #663)
|
|
366 |
#680 := (iff #678 #677)
|
|
367 |
#682 := (iff #677 #677)
|
|
368 |
#683 := [rewrite]: #682
|
|
369 |
#674 := (iff #663 #673)
|
|
370 |
#671 := (iff #658 #670)
|
|
371 |
#672 := [rewrite]: #671
|
|
372 |
#668 := (iff #662 #667)
|
|
373 |
#665 := (iff #660 #664)
|
|
374 |
#666 := [rewrite]: #665
|
|
375 |
#669 := [monotonicity #279 #666]: #668
|
|
376 |
#626 := (iff #613 #623)
|
|
377 |
#615 := (+ #158 #611)
|
|
378 |
#618 := (>= #615 0::int)
|
|
379 |
#624 := (iff #618 #623)
|
|
380 |
#625 := [rewrite]: #624
|
|
381 |
#619 := (iff #613 #618)
|
|
382 |
#616 := (= #612 #615)
|
|
383 |
#617 := [rewrite]: #616
|
|
384 |
#620 := [monotonicity #617]: #619
|
|
385 |
#627 := [trans #620 #625]: #626
|
|
386 |
#675 := [monotonicity #627 #669 #672]: #674
|
|
387 |
#681 := [monotonicity #675]: #680
|
|
388 |
#684 := [trans #681 #683]: #680
|
|
389 |
#679 := [quant-inst]: #678
|
|
390 |
#685 := [mp #679 #684]: #677
|
|
391 |
#1311 := [unit-resolution #685 #566]: #673
|
|
392 |
#1312 := (not #987)
|
|
393 |
#1313 := (or #1312 #623)
|
|
394 |
#1314 := [th-lemma]: #1313
|
|
395 |
#1315 := [unit-resolution #1314 #1281]: #623
|
|
396 |
#645 := (not #623)
|
|
397 |
#698 := (not #673)
|
|
398 |
#699 := (or #698 #645 #667)
|
|
399 |
#700 := [def-axiom]: #699
|
|
400 |
#1316 := [unit-resolution #700 #1315 #1311]: #667
|
|
401 |
#686 := (not #667)
|
|
402 |
#1317 := (or #686 #661)
|
|
403 |
#687 := (not #277)
|
|
404 |
#688 := (or #686 #687 #661)
|
|
405 |
#689 := [def-axiom]: #688
|
|
406 |
#1318 := [unit-resolution #689 #282]: #1317
|
|
407 |
#1319 := [unit-resolution #1318 #1316]: #661
|
|
408 |
#1321 := [symm #1319]: #1320
|
|
409 |
#1323 := [monotonicity #1321]: #1322
|
|
410 |
#1325 := [monotonicity #1323]: #1324
|
|
411 |
#1145 := (* -1::real #771)
|
|
412 |
#1240 := (+ #656 #1145)
|
|
413 |
#1241 := (<= #1240 0::real)
|
|
414 |
#1249 := (not #1241)
|
|
415 |
#1243 := [hypothesis]: #1241
|
|
416 |
decl uf_18 :: T3
|
|
417 |
#80 := uf_18
|
|
418 |
#1040 := (uf_1 uf_18 #44)
|
|
419 |
#1043 := (* -1::real #1040)
|
|
420 |
#1156 := (+ #771 #1043)
|
|
421 |
#1157 := (>= #1156 0::real)
|
|
422 |
#1189 := (not #1157)
|
|
423 |
#708 := (uf_1 #91 #44)
|
|
424 |
#1168 := (+ #708 #1043)
|
|
425 |
#1169 := (<= #1168 0::real)
|
|
426 |
#1174 := (or #1157 #1169)
|
|
427 |
#1177 := (not #1174)
|
|
428 |
#89 := (uf_1 #88 #6)
|
|
429 |
#552 := (pattern #89)
|
|
430 |
#81 := (uf_1 uf_18 #6)
|
|
431 |
#594 := (pattern #81)
|
|
432 |
#324 := (* -1::real #92)
|
|
433 |
#325 := (+ #81 #324)
|
|
434 |
#323 := (>= #325 0::real)
|
|
435 |
#317 := (* -1::real #89)
|
|
436 |
#318 := (+ #81 #317)
|
|
437 |
#319 := (<= #318 0::real)
|
|
438 |
#436 := (or #319 #323)
|
|
439 |
#437 := (not #436)
|
|
440 |
#601 := (forall (vars (?x11 T2)) (:pat #594 #552 #542) #437)
|
|
441 |
#440 := (forall (vars (?x11 T2)) #437)
|
|
442 |
#604 := (iff #440 #601)
|
|
443 |
#602 := (iff #437 #437)
|
|
444 |
#603 := [refl]: #602
|
|
445 |
#605 := [quant-intro #603]: #604
|
|
446 |
#326 := (not #323)
|
|
447 |
#320 := (not #319)
|
|
448 |
#329 := (and #320 #326)
|
|
449 |
#332 := (forall (vars (?x11 T2)) #329)
|
|
450 |
#441 := (iff #332 #440)
|
|
451 |
#438 := (iff #329 #437)
|
|
452 |
#439 := [rewrite]: #438
|
|
453 |
#442 := [quant-intro #439]: #441
|
|
454 |
#425 := (~ #332 #332)
|
|
455 |
#423 := (~ #329 #329)
|
|
456 |
#424 := [refl]: #423
|
|
457 |
#426 := [nnf-pos #424]: #425
|
|
458 |
#306 := (* -1::real #84)
|
|
459 |
#307 := (+ #81 #306)
|
|
460 |
#305 := (>= #307 0::real)
|
|
461 |
#308 := (not #305)
|
|
462 |
#301 := (* -1::real #81)
|
|
463 |
#79 := (uf_1 #78 #6)
|
|
464 |
#302 := (+ #79 #301)
|
|
465 |
#300 := (>= #302 0::real)
|
|
466 |
#298 := (not #300)
|
|
467 |
#311 := (and #298 #308)
|
|
468 |
#314 := (forall (vars (?x10 T2)) #311)
|
|
469 |
#335 := (and #314 #332)
|
|
470 |
#93 := (< #81 #92)
|
|
471 |
#90 := (< #89 #81)
|
|
472 |
#94 := (and #90 #93)
|
|
473 |
#95 := (forall (vars (?x11 T2)) #94)
|
|
474 |
#85 := (< #81 #84)
|
|
475 |
#82 := (< #79 #81)
|
|
476 |
#86 := (and #82 #85)
|
|
477 |
#87 := (forall (vars (?x10 T2)) #86)
|
|
478 |
#96 := (and #87 #95)
|
|
479 |
#336 := (iff #96 #335)
|
|
480 |
#333 := (iff #95 #332)
|
|
481 |
#330 := (iff #94 #329)
|
|
482 |
#327 := (iff #93 #326)
|
|
483 |
#328 := [rewrite]: #327
|
|
484 |
#321 := (iff #90 #320)
|
|
485 |
#322 := [rewrite]: #321
|
|
486 |
#331 := [monotonicity #322 #328]: #330
|
|
487 |
#334 := [quant-intro #331]: #333
|
|
488 |
#315 := (iff #87 #314)
|
|
489 |
#312 := (iff #86 #311)
|
|
490 |
#309 := (iff #85 #308)
|
|
491 |
#310 := [rewrite]: #309
|
|
492 |
#303 := (iff #82 #298)
|
|
493 |
#304 := [rewrite]: #303
|
|
494 |
#313 := [monotonicity #304 #310]: #312
|
|
495 |
#316 := [quant-intro #313]: #315
|
|
496 |
#337 := [monotonicity #316 #334]: #336
|
|
497 |
#293 := [asserted]: #96
|
|
498 |
#338 := [mp #293 #337]: #335
|
|
499 |
#340 := [and-elim #338]: #332
|
|
500 |
#427 := [mp~ #340 #426]: #332
|
|
501 |
#443 := [mp #427 #442]: #440
|
|
502 |
#606 := [mp #443 #605]: #601
|
|
503 |
#1124 := (not #601)
|
|
504 |
#1180 := (or #1124 #1177)
|
|
505 |
#1142 := (* -1::real #708)
|
|
506 |
#1143 := (+ #1040 #1142)
|
|
507 |
#1144 := (>= #1143 0::real)
|
|
508 |
#1146 := (+ #1040 #1145)
|
|
509 |
#1147 := (<= #1146 0::real)
|
|
510 |
#1148 := (or #1147 #1144)
|
|
511 |
#1149 := (not #1148)
|
|
512 |
#1181 := (or #1124 #1149)
|
|
513 |
#1183 := (iff #1181 #1180)
|
|
514 |
#1185 := (iff #1180 #1180)
|
|
515 |
#1186 := [rewrite]: #1185
|
|
516 |
#1178 := (iff #1149 #1177)
|
|
517 |
#1175 := (iff #1148 #1174)
|
|
518 |
#1172 := (iff #1144 #1169)
|
|
519 |
#1162 := (+ #1142 #1040)
|
|
520 |
#1165 := (>= #1162 0::real)
|
|
521 |
#1170 := (iff #1165 #1169)
|
|
522 |
#1171 := [rewrite]: #1170
|
|
523 |
#1166 := (iff #1144 #1165)
|
|
524 |
#1163 := (= #1143 #1162)
|
|
525 |
#1164 := [rewrite]: #1163
|
|
526 |
#1167 := [monotonicity #1164]: #1166
|
|
527 |
#1173 := [trans #1167 #1171]: #1172
|
|
528 |
#1160 := (iff #1147 #1157)
|
|
529 |
#1150 := (+ #1145 #1040)
|
|
530 |
#1153 := (<= #1150 0::real)
|
|
531 |
#1158 := (iff #1153 #1157)
|
|
532 |
#1159 := [rewrite]: #1158
|
|
533 |
#1154 := (iff #1147 #1153)
|
|
534 |
#1151 := (= #1146 #1150)
|
|
535 |
#1152 := [rewrite]: #1151
|
|
536 |
#1155 := [monotonicity #1152]: #1154
|
|
537 |
#1161 := [trans #1155 #1159]: #1160
|
|
538 |
#1176 := [monotonicity #1161 #1173]: #1175
|
|
539 |
#1179 := [monotonicity #1176]: #1178
|
|
540 |
#1184 := [monotonicity #1179]: #1183
|
|
541 |
#1187 := [trans #1184 #1186]: #1183
|
|
542 |
#1182 := [quant-inst]: #1181
|
|
543 |
#1188 := [mp #1182 #1187]: #1180
|
|
544 |
#1244 := [unit-resolution #1188 #606]: #1177
|
|
545 |
#1190 := (or #1174 #1189)
|
|
546 |
#1191 := [def-axiom]: #1190
|
|
547 |
#1245 := [unit-resolution #1191 #1244]: #1189
|
|
548 |
#1054 := (+ #656 #1043)
|
|
549 |
#1055 := (<= #1054 0::real)
|
|
550 |
#1079 := (not #1055)
|
|
551 |
#607 := (uf_1 #78 #44)
|
|
552 |
#1044 := (+ #607 #1043)
|
|
553 |
#1045 := (>= #1044 0::real)
|
|
554 |
#1060 := (or #1045 #1055)
|
|
555 |
#1063 := (not #1060)
|
|
556 |
#567 := (pattern #79)
|
|
557 |
#428 := (or #300 #305)
|
|
558 |
#429 := (not #428)
|
|
559 |
#595 := (forall (vars (?x10 T2)) (:pat #567 #594 #560) #429)
|
|
560 |
#432 := (forall (vars (?x10 T2)) #429)
|
|
561 |
#598 := (iff #432 #595)
|
|
562 |
#596 := (iff #429 #429)
|
|
563 |
#597 := [refl]: #596
|
|
564 |
#599 := [quant-intro #597]: #598
|
|
565 |
#433 := (iff #314 #432)
|
|
566 |
#430 := (iff #311 #429)
|
|
567 |
#431 := [rewrite]: #430
|
|
568 |
#434 := [quant-intro #431]: #433
|
|
569 |
#420 := (~ #314 #314)
|
|
570 |
#418 := (~ #311 #311)
|
|
571 |
#419 := [refl]: #418
|
|
572 |
#421 := [nnf-pos #419]: #420
|
|
573 |
#339 := [and-elim #338]: #314
|
|
574 |
#422 := [mp~ #339 #421]: #314
|
|
575 |
#435 := [mp #422 #434]: #432
|
|
576 |
#600 := [mp #435 #599]: #595
|
|
577 |
#1066 := (not #595)
|
|
578 |
#1067 := (or #1066 #1063)
|
|
579 |
#1039 := (* -1::real #656)
|
|
580 |
#1041 := (+ #1040 #1039)
|
|
581 |
#1042 := (>= #1041 0::real)
|
|
582 |
#1046 := (or #1045 #1042)
|
|
583 |
#1047 := (not #1046)
|
|
584 |
#1068 := (or #1066 #1047)
|
|
585 |
#1070 := (iff #1068 #1067)
|
|
586 |
#1072 := (iff #1067 #1067)
|
|
587 |
#1073 := [rewrite]: #1072
|
|
588 |
#1064 := (iff #1047 #1063)
|
|
589 |
#1061 := (iff #1046 #1060)
|
|
590 |
#1058 := (iff #1042 #1055)
|
|
591 |
#1048 := (+ #1039 #1040)
|
|
592 |
#1051 := (>= #1048 0::real)
|
|
593 |
#1056 := (iff #1051 #1055)
|
|
594 |
#1057 := [rewrite]: #1056
|
|
595 |
#1052 := (iff #1042 #1051)
|
|
596 |
#1049 := (= #1041 #1048)
|
|
597 |
#1050 := [rewrite]: #1049
|
|
598 |
#1053 := [monotonicity #1050]: #1052
|
|
599 |
#1059 := [trans #1053 #1057]: #1058
|
|
600 |
#1062 := [monotonicity #1059]: #1061
|
|
601 |
#1065 := [monotonicity #1062]: #1064
|
|
602 |
#1071 := [monotonicity #1065]: #1070
|
|
603 |
#1074 := [trans #1071 #1073]: #1070
|
|
604 |
#1069 := [quant-inst]: #1068
|
|
605 |
#1075 := [mp #1069 #1074]: #1067
|
|
606 |
#1246 := [unit-resolution #1075 #600]: #1063
|
|
607 |
#1080 := (or #1060 #1079)
|
|
608 |
#1081 := [def-axiom]: #1080
|
|
609 |
#1247 := [unit-resolution #1081 #1246]: #1079
|
|
610 |
#1248 := [th-lemma #1247 #1245 #1243]: false
|
|
611 |
#1250 := [lemma #1248]: #1249
|
|
612 |
#1253 := (or #1252 #1241)
|
|
613 |
#1254 := [th-lemma]: #1253
|
|
614 |
#1310 := [unit-resolution #1254 #1250]: #1252
|
|
615 |
#1326 := [mp #1310 #1325]: #796
|
|
616 |
#1328 := (or #724 #772)
|
|
617 |
decl uf_13 :: T3
|
|
618 |
#33 := uf_13
|
|
619 |
#609 := (uf_1 uf_13 #44)
|
|
620 |
#773 := (= #609 #771)
|
|
621 |
#775 := (ite #724 #773 #772)
|
|
622 |
#32 := (uf_1 uf_9 #6)
|
|
623 |
#553 := (pattern #32)
|
|
624 |
#34 := (uf_1 uf_13 #6)
|
|
625 |
#551 := (pattern #34)
|
|
626 |
#456 := (= #32 #89)
|
|
627 |
#455 := (= #34 #89)
|
|
628 |
#457 := (ite #119 #455 #456)
|
|
629 |
#554 := (forall (vars (?x4 T2)) (:pat #541 #551 #552 #553) #457)
|
|
630 |
#460 := (forall (vars (?x4 T2)) #457)
|
|
631 |
#557 := (iff #460 #554)
|
|
632 |
#555 := (iff #457 #457)
|
|
633 |
#556 := [refl]: #555
|
|
634 |
#558 := [quant-intro #556]: #557
|
|
635 |
#143 := (ite #119 #34 #32)
|
|
636 |
#373 := (= #89 #143)
|
|
637 |
#374 := (forall (vars (?x4 T2)) #373)
|
|
638 |
#461 := (iff #374 #460)
|
|
639 |
#458 := (iff #373 #457)
|
|
640 |
#459 := [rewrite]: #458
|
|
641 |
#462 := [quant-intro #459]: #461
|
|
642 |
#362 := (~ #374 #374)
|
|
643 |
#364 := (~ #373 #373)
|
|
644 |
#365 := [refl]: #364
|
|
645 |
#363 := [nnf-pos #365]: #362
|
|
646 |
#31 := (uf_3 uf_12 #6)
|
|
647 |
#148 := (= #31 #143)
|
|
648 |
#151 := (forall (vars (?x4 T2)) #148)
|
|
649 |
#375 := (iff #151 #374)
|
|
650 |
#376 := [rewrite* #113]: #375
|
|
651 |
#35 := (ite #17 #32 #34)
|
|
652 |
#36 := (= #31 #35)
|
|
653 |
#37 := (forall (vars (?x4 T2)) #36)
|
|
654 |
#152 := (iff #37 #151)
|
|
655 |
#149 := (iff #36 #148)
|
|
656 |
#146 := (= #35 #143)
|
|
657 |
#140 := (ite #118 #32 #34)
|
|
658 |
#144 := (= #140 #143)
|
|
659 |
#145 := [rewrite]: #144
|
|
660 |
#141 := (= #35 #140)
|
|
661 |
#142 := [monotonicity #123]: #141
|
|
662 |
#147 := [trans #142 #145]: #146
|
|
663 |
#150 := [monotonicity #147]: #149
|
|
664 |
#153 := [quant-intro #150]: #152
|
|
665 |
#115 := [asserted]: #37
|
|
666 |
#154 := [mp #115 #153]: #151
|
|
667 |
#377 := [mp #154 #376]: #374
|
|
668 |
#360 := [mp~ #377 #363]: #374
|
|
669 |
#463 := [mp #360 #462]: #460
|
|
670 |
#559 := [mp #463 #558]: #554
|
|
671 |
#778 := (not #554)
|
|
672 |
#779 := (or #778 #775)
|
|
673 |
#714 := (+ #611 #120)
|
|
674 |
#715 := (>= #714 0::int)
|
|
675 |
#774 := (ite #715 #773 #772)
|
|
676 |
#780 := (or #778 #774)
|
|
677 |
#782 := (iff #780 #779)
|
|
678 |
#784 := (iff #779 #779)
|
|
679 |
#785 := [rewrite]: #784
|
|
680 |
#776 := (iff #774 #775)
|
|
681 |
#727 := (iff #715 #724)
|
|
682 |
#717 := (+ #120 #611)
|
|
683 |
#720 := (>= #717 0::int)
|
|
684 |
#725 := (iff #720 #724)
|
|
685 |
#726 := [rewrite]: #725
|
|
686 |
#721 := (iff #715 #720)
|
|
687 |
#718 := (= #714 #717)
|
|
688 |
#719 := [rewrite]: #718
|
|
689 |
#722 := [monotonicity #719]: #721
|
|
690 |
#728 := [trans #722 #726]: #727
|
|
691 |
#777 := [monotonicity #728]: #776
|
|
692 |
#783 := [monotonicity #777]: #782
|
|
693 |
#786 := [trans #783 #785]: #782
|
|
694 |
#781 := [quant-inst]: #780
|
|
695 |
#787 := [mp #781 #786]: #779
|
|
696 |
#1327 := [unit-resolution #787 #559]: #775
|
|
697 |
#788 := (not #775)
|
|
698 |
#791 := (or #788 #724 #772)
|
|
699 |
#792 := [def-axiom]: #791
|
|
700 |
#1329 := [unit-resolution #792 #1327]: #1328
|
|
701 |
#1330 := [unit-resolution #1329 #1326]: #724
|
|
702 |
#988 := (>= #622 0::int)
|
|
703 |
#1331 := (or #1312 #988)
|
|
704 |
#1332 := [th-lemma]: #1331
|
|
705 |
#1333 := [unit-resolution #1332 #1281]: #988
|
|
706 |
#761 := (not #724)
|
|
707 |
#1334 := (not #988)
|
|
708 |
#1335 := (or #1271 #1334 #761)
|
|
709 |
#1336 := [th-lemma]: #1335
|
|
710 |
#1337 := [unit-resolution #1336 #1333 #1330]: #1271
|
|
711 |
#1338 := (not #1271)
|
|
712 |
#1340 := (or #1269 #1338 #1339)
|
|
713 |
#1341 := [th-lemma]: #1340
|
|
714 |
#1343 := [unit-resolution #1341 #1337]: #1342
|
|
715 |
#1344 := [unit-resolution #1343 #1299]: #1339
|
|
716 |
#990 := (>= #916 0::int)
|
|
717 |
#1345 := (or #1302 #990)
|
|
718 |
#1346 := [th-lemma]: #1345
|
|
719 |
#1347 := [unit-resolution #1346 #1301]: #990
|
|
720 |
#1348 := (not #990)
|
|
721 |
#1349 := (or #836 #1348 #1265)
|
|
722 |
#1350 := [th-lemma]: #1349
|
|
723 |
#1351 := [unit-resolution #1350 #1347 #1344]: #836
|
|
724 |
#1353 := (or #815 #800)
|
|
725 |
#801 := (uf_1 uf_13 #22)
|
|
726 |
#820 := (= #799 #801)
|
|
727 |
#823 := (ite #815 #820 #800)
|
|
728 |
#476 := (= #32 #79)
|
|
729 |
#475 := (= #34 #79)
|
|
730 |
#477 := (ite #157 #475 #476)
|
|
731 |
#568 := (forall (vars (?x6 T2)) (:pat #541 #551 #567 #553) #477)
|
|
732 |
#480 := (forall (vars (?x6 T2)) #477)
|
|
733 |
#571 := (iff #480 #568)
|
|
734 |
#569 := (iff #477 #477)
|
|
735 |
#570 := [refl]: #569
|
|
736 |
#572 := [quant-intro #570]: #571
|
|
737 |
#181 := (ite #157 #34 #32)
|
|
738 |
#383 := (= #79 #181)
|
|
739 |
#384 := (forall (vars (?x6 T2)) #383)
|
|
740 |
#481 := (iff #384 #480)
|
|
741 |
#478 := (iff #383 #477)
|
|
742 |
#479 := [rewrite]: #478
|
|
743 |
#482 := [quant-intro #479]: #481
|
|
744 |
#352 := (~ #384 #384)
|
|
745 |
#354 := (~ #383 #383)
|
|
746 |
#355 := [refl]: #354
|
|
747 |
#353 := [nnf-pos #355]: #352
|
|
748 |
#51 := (uf_3 uf_16 #6)
|
|
749 |
#186 := (= #51 #181)
|
|
750 |
#189 := (forall (vars (?x6 T2)) #186)
|
|
751 |
#385 := (iff #189 #384)
|
|
752 |
#386 := [rewrite* #113]: #385
|
|
753 |
#52 := (ite #42 #32 #34)
|
|
754 |
#53 := (= #51 #52)
|
|
755 |
#54 := (forall (vars (?x6 T2)) #53)
|
|
756 |
#190 := (iff #54 #189)
|
|
757 |
#187 := (iff #53 #186)
|
|
758 |
#184 := (= #52 #181)
|
|
759 |
#178 := (ite #156 #32 #34)
|
|
760 |
#182 := (= #178 #181)
|
|
761 |
#183 := [rewrite]: #182
|
|
762 |
#179 := (= #52 #178)
|
|
763 |
#180 := [monotonicity #161]: #179
|
|
764 |
#185 := [trans #180 #183]: #184
|
|
765 |
#188 := [monotonicity #185]: #187
|
|
766 |
#191 := [quant-intro #188]: #190
|
|
767 |
#139 := [asserted]: #54
|
|
768 |
#192 := [mp #139 #191]: #189
|
|
769 |
#387 := [mp #192 #386]: #384
|
|
770 |
#402 := [mp~ #387 #353]: #384
|
|
771 |
#483 := [mp #402 #482]: #480
|
|
772 |
#573 := [mp #483 #572]: #568
|
|
773 |
#634 := (not #568)
|
|
774 |
#826 := (or #634 #823)
|
|
775 |
#802 := (= #801 #799)
|
|
776 |
#804 := (+ #803 #158)
|
|
777 |
#805 := (>= #804 0::int)
|
|
778 |
#806 := (ite #805 #802 #800)
|
|
779 |
#827 := (or #634 #806)
|
|
780 |
#829 := (iff #827 #826)
|
|
781 |
#831 := (iff #826 #826)
|
|
782 |
#832 := [rewrite]: #831
|
|
783 |
#824 := (iff #806 #823)
|
|
784 |
#821 := (iff #802 #820)
|
|
785 |
#822 := [rewrite]: #821
|
|
786 |
#818 := (iff #805 #815)
|
|
787 |
#807 := (+ #158 #803)
|
|
788 |
#810 := (>= #807 0::int)
|
|
789 |
#816 := (iff #810 #815)
|
|
790 |
#817 := [rewrite]: #816
|
|
791 |
#811 := (iff #805 #810)
|
|
792 |
#808 := (= #804 #807)
|
|
793 |
#809 := [rewrite]: #808
|
|
794 |
#812 := [monotonicity #809]: #811
|
|
795 |
#819 := [trans #812 #817]: #818
|
|
796 |
#825 := [monotonicity #819 #822]: #824
|
|
797 |
#830 := [monotonicity #825]: #829
|
|
798 |
#833 := [trans #830 #832]: #829
|
|
799 |
#828 := [quant-inst]: #827
|
|
800 |
#834 := [mp #828 #833]: #826
|
|
801 |
#1352 := [unit-resolution #834 #573]: #823
|
|
802 |
#835 := (not #823)
|
|
803 |
#839 := (or #835 #815 #800)
|
|
804 |
#840 := [def-axiom]: #839
|
|
805 |
#1354 := [unit-resolution #840 #1352]: #1353
|
|
806 |
#1355 := [unit-resolution #1354 #1351]: #800
|
|
807 |
#1357 := [symm #1355]: #1356
|
|
808 |
#1358 := [trans #1357 #1309]: #1266
|
|
809 |
#1359 := (not #1266)
|
|
810 |
#1360 := (or #1359 #1272)
|
|
811 |
#1361 := [th-lemma]: #1360
|
|
812 |
#1362 := [unit-resolution #1361 #1358]: #1272
|
|
813 |
#1085 := (uf_1 uf_18 #22)
|
|
814 |
#1099 := (* -1::real #1085)
|
|
815 |
#1112 := (+ #902 #1099)
|
|
816 |
#1113 := (<= #1112 0::real)
|
|
817 |
#1137 := (not #1113)
|
|
818 |
#960 := (uf_1 #88 #22)
|
|
819 |
#1100 := (+ #960 #1099)
|
|
820 |
#1101 := (>= #1100 0::real)
|
|
821 |
#1118 := (or #1101 #1113)
|
|
822 |
#1121 := (not #1118)
|
|
823 |
#1125 := (or #1124 #1121)
|
|
824 |
#1086 := (+ #1085 #1084)
|
|
825 |
#1087 := (>= #1086 0::real)
|
|
826 |
#1088 := (* -1::real #960)
|
|
827 |
#1089 := (+ #1085 #1088)
|
|
828 |
#1090 := (<= #1089 0::real)
|
|
829 |
#1091 := (or #1090 #1087)
|
|
830 |
#1092 := (not #1091)
|
|
831 |
#1126 := (or #1124 #1092)
|
|
832 |
#1128 := (iff #1126 #1125)
|
|
833 |
#1130 := (iff #1125 #1125)
|
|
834 |
#1131 := [rewrite]: #1130
|
|
835 |
#1122 := (iff #1092 #1121)
|
|
836 |
#1119 := (iff #1091 #1118)
|
|
837 |
#1116 := (iff #1087 #1113)
|
|
838 |
#1106 := (+ #1084 #1085)
|
|
839 |
#1109 := (>= #1106 0::real)
|
|
840 |
#1114 := (iff #1109 #1113)
|
|
841 |
#1115 := [rewrite]: #1114
|
|
842 |
#1110 := (iff #1087 #1109)
|
|
843 |
#1107 := (= #1086 #1106)
|
|
844 |
#1108 := [rewrite]: #1107
|
|
845 |
#1111 := [monotonicity #1108]: #1110
|
|
846 |
#1117 := [trans #1111 #1115]: #1116
|
|
847 |
#1104 := (iff #1090 #1101)
|
|
848 |
#1093 := (+ #1088 #1085)
|
|
849 |
#1096 := (<= #1093 0::real)
|
|
850 |
#1102 := (iff #1096 #1101)
|
|
851 |
#1103 := [rewrite]: #1102
|
|
852 |
#1097 := (iff #1090 #1096)
|
|
853 |
#1094 := (= #1089 #1093)
|
|
854 |
#1095 := [rewrite]: #1094
|
|
855 |
#1098 := [monotonicity #1095]: #1097
|
|
856 |
#1105 := [trans #1098 #1103]: #1104
|
|
857 |
#1120 := [monotonicity #1105 #1117]: #1119
|
|
858 |
#1123 := [monotonicity #1120]: #1122
|
|
859 |
#1129 := [monotonicity #1123]: #1128
|
|
860 |
#1132 := [trans #1129 #1131]: #1128
|
|
861 |
#1127 := [quant-inst]: #1126
|
|
862 |
#1133 := [mp #1127 #1132]: #1125
|
|
863 |
#1363 := [unit-resolution #1133 #606]: #1121
|
|
864 |
#1138 := (or #1118 #1137)
|
|
865 |
#1139 := [def-axiom]: #1138
|
|
866 |
#1364 := [unit-resolution #1139 #1363]: #1137
|
|
867 |
#1200 := (+ #799 #1099)
|
|
868 |
#1201 := (>= #1200 0::real)
|
|
869 |
#1231 := (not #1201)
|
|
870 |
#847 := (uf_1 #83 #22)
|
|
871 |
#1210 := (+ #847 #1099)
|
|
872 |
#1211 := (<= #1210 0::real)
|
|
873 |
#1216 := (or #1201 #1211)
|
|
874 |
#1219 := (not #1216)
|
|
875 |
#1222 := (or #1066 #1219)
|
|
876 |
#1197 := (* -1::real #847)
|
|
877 |
#1198 := (+ #1085 #1197)
|
|
878 |
#1199 := (>= #1198 0::real)
|
|
879 |
#1202 := (or #1201 #1199)
|
|
880 |
#1203 := (not #1202)
|
|
881 |
#1223 := (or #1066 #1203)
|
|
882 |
#1225 := (iff #1223 #1222)
|
|
883 |
#1227 := (iff #1222 #1222)
|
|
884 |
#1228 := [rewrite]: #1227
|
|
885 |
#1220 := (iff #1203 #1219)
|
|
886 |
#1217 := (iff #1202 #1216)
|
|
887 |
#1214 := (iff #1199 #1211)
|
|
888 |
#1204 := (+ #1197 #1085)
|
|
889 |
#1207 := (>= #1204 0::real)
|
|
890 |
#1212 := (iff #1207 #1211)
|
|
891 |
#1213 := [rewrite]: #1212
|
|
892 |
#1208 := (iff #1199 #1207)
|
|
893 |
#1205 := (= #1198 #1204)
|
|
894 |
#1206 := [rewrite]: #1205
|
|
895 |
#1209 := [monotonicity #1206]: #1208
|
|
896 |
#1215 := [trans #1209 #1213]: #1214
|
|
897 |
#1218 := [monotonicity #1215]: #1217
|
|
898 |
#1221 := [monotonicity #1218]: #1220
|
|
899 |
#1226 := [monotonicity #1221]: #1225
|
|
900 |
#1229 := [trans #1226 #1228]: #1225
|
|
901 |
#1224 := [quant-inst]: #1223
|
|
902 |
#1230 := [mp #1224 #1229]: #1222
|
|
903 |
#1365 := [unit-resolution #1230 #600]: #1219
|
|
904 |
#1232 := (or #1216 #1231)
|
|
905 |
#1233 := [def-axiom]: #1232
|
|
906 |
#1366 := [unit-resolution #1233 #1365]: #1231
|
|
907 |
[th-lemma #1366 #1364 #1362]: false
|
|
908 |
unsat
|
|
909 |
NQHwTeL311Tq3wf2s5BReA 419 0
|
|
910 |
#2 := false
|
|
911 |
#194 := 0::real
|
|
912 |
decl uf_4 :: (-> T2 T3 real)
|
|
913 |
decl uf_6 :: (-> T1 T3)
|
|
914 |
decl uf_3 :: T1
|
|
915 |
#21 := uf_3
|
|
916 |
#25 := (uf_6 uf_3)
|
|
917 |
decl uf_5 :: T2
|
|
918 |
#24 := uf_5
|
|
919 |
#26 := (uf_4 uf_5 #25)
|
|
920 |
decl uf_7 :: T2
|
|
921 |
#27 := uf_7
|
|
922 |
#28 := (uf_4 uf_7 #25)
|
|
923 |
decl uf_10 :: T1
|
|
924 |
#38 := uf_10
|
|
925 |
#42 := (uf_6 uf_10)
|
|
926 |
decl uf_9 :: T2
|
|
927 |
#33 := uf_9
|
|
928 |
#43 := (uf_4 uf_9 #42)
|
|
929 |
#41 := (= uf_3 uf_10)
|
|
930 |
#44 := (ite #41 #43 #28)
|
|
931 |
#9 := 0::int
|
|
932 |
decl uf_2 :: (-> T1 int)
|
|
933 |
#39 := (uf_2 uf_10)
|
|
934 |
#226 := -1::int
|
|
935 |
#229 := (* -1::int #39)
|
|
936 |
#22 := (uf_2 uf_3)
|
|
937 |
#230 := (+ #22 #229)
|
|
938 |
#228 := (>= #230 0::int)
|
|
939 |
#236 := (ite #228 #44 #26)
|
|
940 |
#192 := -1::real
|
|
941 |
#244 := (* -1::real #236)
|
|
942 |
#642 := (+ #26 #244)
|
|
943 |
#643 := (<= #642 0::real)
|
|
944 |
#567 := (= #26 #236)
|
|
945 |
#227 := (not #228)
|
|
946 |
decl uf_1 :: (-> int T1)
|
|
947 |
#593 := (uf_1 #39)
|
|
948 |
#660 := (= #593 uf_10)
|
|
949 |
#594 := (= uf_10 #593)
|
|
950 |
#4 := (:var 0 T1)
|
|
951 |
#5 := (uf_2 #4)
|
|
952 |
#546 := (pattern #5)
|
|
953 |
#6 := (uf_1 #5)
|
|
954 |
#93 := (= #4 #6)
|
|
955 |
#547 := (forall (vars (?x1 T1)) (:pat #546) #93)
|
|
956 |
#96 := (forall (vars (?x1 T1)) #93)
|
|
957 |
#550 := (iff #96 #547)
|
|
958 |
#548 := (iff #93 #93)
|
|
959 |
#549 := [refl]: #548
|
|
960 |
#551 := [quant-intro #549]: #550
|
|
961 |
#448 := (~ #96 #96)
|
|
962 |
#450 := (~ #93 #93)
|
|
963 |
#451 := [refl]: #450
|
|
964 |
#449 := [nnf-pos #451]: #448
|
|
965 |
#7 := (= #6 #4)
|
|
966 |
#8 := (forall (vars (?x1 T1)) #7)
|
|
967 |
#97 := (iff #8 #96)
|
|
968 |
#94 := (iff #7 #93)
|
|
969 |
#95 := [rewrite]: #94
|
|
970 |
#98 := [quant-intro #95]: #97
|
|
971 |
#92 := [asserted]: #8
|
|
972 |
#101 := [mp #92 #98]: #96
|
|
973 |
#446 := [mp~ #101 #449]: #96
|
|
974 |
#552 := [mp #446 #551]: #547
|
|
975 |
#595 := (not #547)
|
|
976 |
#600 := (or #595 #594)
|
|
977 |
#601 := [quant-inst]: #600
|
|
978 |
#654 := [unit-resolution #601 #552]: #594
|
|
979 |
#680 := [symm #654]: #660
|
|
980 |
#681 := (= uf_3 #593)
|
|
981 |
#591 := (uf_1 #22)
|
|
982 |
#658 := (= #591 #593)
|
|
983 |
#656 := (= #593 #591)
|
|
984 |
#652 := (= #39 #22)
|
|
985 |
#647 := (= #22 #39)
|
|
986 |
#290 := (<= #230 0::int)
|
|
987 |
#70 := (<= #22 #39)
|
|
988 |
#388 := (iff #70 #290)
|
|
989 |
#389 := [rewrite]: #388
|
|
990 |
#341 := [asserted]: #70
|
|
991 |
#390 := [mp #341 #389]: #290
|
|
992 |
#646 := [hypothesis]: #228
|
|
993 |
#648 := [th-lemma #646 #390]: #647
|
|
994 |
#653 := [symm #648]: #652
|
|
995 |
#657 := [monotonicity #653]: #656
|
|
996 |
#659 := [symm #657]: #658
|
|
997 |
#592 := (= uf_3 #591)
|
|
998 |
#596 := (or #595 #592)
|
|
999 |
#597 := [quant-inst]: #596
|
|
1000 |
#655 := [unit-resolution #597 #552]: #592
|
|
1001 |
#682 := [trans #655 #659]: #681
|
|
1002 |
#683 := [trans #682 #680]: #41
|
|
1003 |
#570 := (not #41)
|
|
1004 |
decl uf_11 :: T2
|
|
1005 |
#47 := uf_11
|
|
1006 |
#59 := (uf_4 uf_11 #42)
|
|
1007 |
#278 := (ite #41 #26 #59)
|
|
1008 |
#459 := (* -1::real #278)
|
|
1009 |
#637 := (+ #26 #459)
|
|
1010 |
#639 := (>= #637 0::real)
|
|
1011 |
#585 := (= #26 #278)
|
|
1012 |
#661 := [hypothesis]: #41
|
|
1013 |
#587 := (or #570 #585)
|
|
1014 |
#588 := [def-axiom]: #587
|
|
1015 |
#662 := [unit-resolution #588 #661]: #585
|
|
1016 |
#663 := (not #585)
|
|
1017 |
#664 := (or #663 #639)
|
|
1018 |
#665 := [th-lemma]: #664
|
|
1019 |
#666 := [unit-resolution #665 #662]: #639
|
|
1020 |
decl uf_8 :: T2
|
|
1021 |
#30 := uf_8
|
|
1022 |
#56 := (uf_4 uf_8 #42)
|
|
1023 |
#357 := (* -1::real #56)
|
|
1024 |
#358 := (+ #43 #357)
|
|
1025 |
#356 := (>= #358 0::real)
|
|
1026 |
#355 := (not #356)
|
|
1027 |
#374 := (* -1::real #59)
|
|
1028 |
#375 := (+ #56 #374)
|
|
1029 |
#373 := (>= #375 0::real)
|
|
1030 |
#376 := (not #373)
|
|
1031 |
#381 := (and #355 #376)
|
|
1032 |
#64 := (< #39 #39)
|
|
1033 |
#67 := (ite #64 #43 #59)
|
|
1034 |
#68 := (< #56 #67)
|
|
1035 |
#53 := (uf_4 uf_5 #42)
|
|
1036 |
#65 := (ite #64 #53 #43)
|
|
1037 |
#66 := (< #65 #56)
|
|
1038 |
#69 := (and #66 #68)
|
|
1039 |
#382 := (iff #69 #381)
|
|
1040 |
#379 := (iff #68 #376)
|
|
1041 |
#370 := (< #56 #59)
|
|
1042 |
#377 := (iff #370 #376)
|
|
1043 |
#378 := [rewrite]: #377
|
|
1044 |
#371 := (iff #68 #370)
|
|
1045 |
#368 := (= #67 #59)
|
|
1046 |
#363 := (ite false #43 #59)
|
|
1047 |
#366 := (= #363 #59)
|
|
1048 |
#367 := [rewrite]: #366
|
|
1049 |
#364 := (= #67 #363)
|
|
1050 |
#343 := (iff #64 false)
|
|
1051 |
#344 := [rewrite]: #343
|
|
1052 |
#365 := [monotonicity #344]: #364
|
|
1053 |
#369 := [trans #365 #367]: #368
|
|
1054 |
#372 := [monotonicity #369]: #371
|
|
1055 |
#380 := [trans #372 #378]: #379
|
|
1056 |
#361 := (iff #66 #355)
|
|
1057 |
#352 := (< #43 #56)
|
|
1058 |
#359 := (iff #352 #355)
|
|
1059 |
#360 := [rewrite]: #359
|
|
1060 |
#353 := (iff #66 #352)
|
|
1061 |
#350 := (= #65 #43)
|
|
1062 |
#345 := (ite false #53 #43)
|
|
1063 |
#348 := (= #345 #43)
|
|
1064 |
#349 := [rewrite]: #348
|
|
1065 |
#346 := (= #65 #345)
|
|
1066 |
#347 := [monotonicity #344]: #346
|
|
1067 |
#351 := [trans #347 #349]: #350
|
|
1068 |
#354 := [monotonicity #351]: #353
|
|
1069 |
#362 := [trans #354 #360]: #361
|
|
1070 |
#383 := [monotonicity #362 #380]: #382
|
|
1071 |
#340 := [asserted]: #69
|
|
1072 |
#384 := [mp #340 #383]: #381
|
|
1073 |
#385 := [and-elim #384]: #355
|
|
1074 |
#394 := (* -1::real #53)
|
|
1075 |
#395 := (+ #43 #394)
|
|
1076 |
#393 := (>= #395 0::real)
|
|
1077 |
#54 := (uf_4 uf_7 #42)
|
|
1078 |
#402 := (* -1::real #54)
|
|
1079 |
#403 := (+ #53 #402)
|
|
1080 |
#401 := (>= #403 0::real)
|
|
1081 |
#397 := (+ #43 #374)
|
|
1082 |
#398 := (<= #397 0::real)
|
|
1083 |
#412 := (and #393 #398 #401)
|
|
1084 |
#73 := (<= #43 #59)
|
|
1085 |
#72 := (<= #53 #43)
|
|
1086 |
#74 := (and #72 #73)
|
|
1087 |
#71 := (<= #54 #53)
|
|
1088 |
#75 := (and #71 #74)
|
|
1089 |
#415 := (iff #75 #412)
|
|
1090 |
#406 := (and #393 #398)
|
|
1091 |
#409 := (and #401 #406)
|
|
1092 |
#413 := (iff #409 #412)
|
|
1093 |
#414 := [rewrite]: #413
|
|
1094 |
#410 := (iff #75 #409)
|
|
1095 |
#407 := (iff #74 #406)
|
|
1096 |
#399 := (iff #73 #398)
|
|
1097 |
#400 := [rewrite]: #399
|
|
1098 |
#392 := (iff #72 #393)
|
|
1099 |
#396 := [rewrite]: #392
|
|
1100 |
#408 := [monotonicity #396 #400]: #407
|
|
1101 |
#404 := (iff #71 #401)
|
|
1102 |
#405 := [rewrite]: #404
|
|
1103 |
#411 := [monotonicity #405 #408]: #410
|
|
1104 |
#416 := [trans #411 #414]: #415
|
|
1105 |
#342 := [asserted]: #75
|
|
1106 |
#417 := [mp #342 #416]: #412
|
|
1107 |
#418 := [and-elim #417]: #393
|
|
1108 |
#650 := (+ #26 #394)
|
|
1109 |
#651 := (<= #650 0::real)
|
|
1110 |
#649 := (= #26 #53)
|
|
1111 |
#671 := (= #53 #26)
|
|
1112 |
#669 := (= #42 #25)
|
|
1113 |
#667 := (= #25 #42)
|
|
1114 |
#668 := [monotonicity #661]: #667
|
|
1115 |
#670 := [symm #668]: #669
|
|
1116 |
#672 := [monotonicity #670]: #671
|
|
1117 |
#673 := [symm #672]: #649
|
|
1118 |
#674 := (not #649)
|
|
1119 |
#675 := (or #674 #651)
|
|
1120 |
#676 := [th-lemma]: #675
|
|
1121 |
#677 := [unit-resolution #676 #673]: #651
|
|
1122 |
#462 := (+ #56 #459)
|
|
1123 |
#465 := (>= #462 0::real)
|
|
1124 |
#438 := (not #465)
|
|
1125 |
#316 := (ite #290 #278 #43)
|
|
1126 |
#326 := (* -1::real #316)
|
|
1127 |
#327 := (+ #56 #326)
|
|
1128 |
#325 := (>= #327 0::real)
|
|
1129 |
#324 := (not #325)
|
|
1130 |
#439 := (iff #324 #438)
|
|
1131 |
#466 := (iff #325 #465)
|
|
1132 |
#463 := (= #327 #462)
|
|
1133 |
#460 := (= #326 #459)
|
|
1134 |
#457 := (= #316 #278)
|
|
1135 |
#1 := true
|
|
1136 |
#452 := (ite true #278 #43)
|
|
1137 |
#455 := (= #452 #278)
|
|
1138 |
#456 := [rewrite]: #455
|
|
1139 |
#453 := (= #316 #452)
|
|
1140 |
#444 := (iff #290 true)
|
|
1141 |
#445 := [iff-true #390]: #444
|
|
1142 |
#454 := [monotonicity #445]: #453
|
|
1143 |
#458 := [trans #454 #456]: #457
|
|
1144 |
#461 := [monotonicity #458]: #460
|
|
1145 |
#464 := [monotonicity #461]: #463
|
|
1146 |
#467 := [monotonicity #464]: #466
|
|
1147 |
#468 := [monotonicity #467]: #439
|
|
1148 |
#297 := (ite #290 #54 #53)
|
|
1149 |
#305 := (* -1::real #297)
|
|
1150 |
#306 := (+ #56 #305)
|
|
1151 |
#307 := (<= #306 0::real)
|
|
1152 |
#308 := (not #307)
|
|
1153 |
#332 := (and #308 #324)
|
|
1154 |
#58 := (= uf_10 uf_3)
|
|
1155 |
#60 := (ite #58 #26 #59)
|
|
1156 |
#52 := (< #39 #22)
|
|
1157 |
#61 := (ite #52 #43 #60)
|
|
1158 |
#62 := (< #56 #61)
|
|
1159 |
#55 := (ite #52 #53 #54)
|
|
1160 |
#57 := (< #55 #56)
|
|
1161 |
#63 := (and #57 #62)
|
|
1162 |
#335 := (iff #63 #332)
|
|
1163 |
#281 := (ite #52 #43 #278)
|
|
1164 |
#284 := (< #56 #281)
|
|
1165 |
#287 := (and #57 #284)
|
|
1166 |
#333 := (iff #287 #332)
|
|
1167 |
#330 := (iff #284 #324)
|
|
1168 |
#321 := (< #56 #316)
|
|
1169 |
#328 := (iff #321 #324)
|
|
1170 |
#329 := [rewrite]: #328
|
|
1171 |
#322 := (iff #284 #321)
|
|
1172 |
#319 := (= #281 #316)
|
|
1173 |
#291 := (not #290)
|
|
1174 |
#313 := (ite #291 #43 #278)
|
|
1175 |
#317 := (= #313 #316)
|
|
1176 |
#318 := [rewrite]: #317
|
|
1177 |
#314 := (= #281 #313)
|
|
1178 |
#292 := (iff #52 #291)
|
|
1179 |
#293 := [rewrite]: #292
|
|
1180 |
#315 := [monotonicity #293]: #314
|
|
1181 |
#320 := [trans #315 #318]: #319
|
|
1182 |
#323 := [monotonicity #320]: #322
|
|
1183 |
#331 := [trans #323 #329]: #330
|
|
1184 |
#311 := (iff #57 #308)
|
|
1185 |
#302 := (< #297 #56)
|
|
1186 |
#309 := (iff #302 #308)
|
|
1187 |
#310 := [rewrite]: #309
|
|
1188 |
#303 := (iff #57 #302)
|
|
1189 |
#300 := (= #55 #297)
|
|
1190 |
#294 := (ite #291 #53 #54)
|
|
1191 |
#298 := (= #294 #297)
|
|
1192 |
#299 := [rewrite]: #298
|
|
1193 |
#295 := (= #55 #294)
|
|
1194 |
#296 := [monotonicity #293]: #295
|
|
1195 |
#301 := [trans #296 #299]: #300
|
|
1196 |
#304 := [monotonicity #301]: #303
|
|
1197 |
#312 := [trans #304 #310]: #311
|
|
1198 |
#334 := [monotonicity #312 #331]: #333
|
|
1199 |
#288 := (iff #63 #287)
|
|
1200 |
#285 := (iff #62 #284)
|
|
1201 |
#282 := (= #61 #281)
|
|
1202 |
#279 := (= #60 #278)
|
|
1203 |
#225 := (iff #58 #41)
|
|
1204 |
#277 := [rewrite]: #225
|
|
1205 |
#280 := [monotonicity #277]: #279
|
|
1206 |
#283 := [monotonicity #280]: #282
|
|
1207 |
#286 := [monotonicity #283]: #285
|
|
1208 |
#289 := [monotonicity #286]: #288
|
|
1209 |
#336 := [trans #289 #334]: #335
|
|
1210 |
#179 := [asserted]: #63
|
|
1211 |
#337 := [mp #179 #336]: #332
|
|
1212 |
#339 := [and-elim #337]: #324
|
|
1213 |
#469 := [mp #339 #468]: #438
|
|
1214 |
#678 := [th-lemma #469 #677 #418 #385 #666]: false
|
|
1215 |
#679 := [lemma #678]: #570
|
|
1216 |
#684 := [unit-resolution #679 #683]: false
|
|
1217 |
#685 := [lemma #684]: #227
|
|
1218 |
#577 := (or #228 #567)
|
|
1219 |
#578 := [def-axiom]: #577
|
|
1220 |
#645 := [unit-resolution #578 #685]: #567
|
|
1221 |
#686 := (not #567)
|
|
1222 |
#687 := (or #686 #643)
|
|
1223 |
#688 := [th-lemma]: #687
|
|
1224 |
#689 := [unit-resolution #688 #645]: #643
|
|
1225 |
#31 := (uf_4 uf_8 #25)
|
|
1226 |
#245 := (+ #31 #244)
|
|
1227 |
#246 := (<= #245 0::real)
|
|
1228 |
#247 := (not #246)
|
|
1229 |
#34 := (uf_4 uf_9 #25)
|
|
1230 |
#48 := (uf_4 uf_11 #25)
|
|
1231 |
#255 := (ite #228 #48 #34)
|
|
1232 |
#264 := (* -1::real #255)
|
|
1233 |
#265 := (+ #31 #264)
|
|
1234 |
#263 := (>= #265 0::real)
|
|
1235 |
#266 := (not #263)
|
|
1236 |
#271 := (and #247 #266)
|
|
1237 |
#40 := (< #22 #39)
|
|
1238 |
#49 := (ite #40 #34 #48)
|
|
1239 |
#50 := (< #31 #49)
|
|
1240 |
#45 := (ite #40 #26 #44)
|
|
1241 |
#46 := (< #45 #31)
|
|
1242 |
#51 := (and #46 #50)
|
|
1243 |
#272 := (iff #51 #271)
|
|
1244 |
#269 := (iff #50 #266)
|
|
1245 |
#260 := (< #31 #255)
|
|
1246 |
#267 := (iff #260 #266)
|
|
1247 |
#268 := [rewrite]: #267
|
|
1248 |
#261 := (iff #50 #260)
|
|
1249 |
#258 := (= #49 #255)
|
|
1250 |
#252 := (ite #227 #34 #48)
|
|
1251 |
#256 := (= #252 #255)
|
|
1252 |
#257 := [rewrite]: #256
|
|
1253 |
#253 := (= #49 #252)
|
|
1254 |
#231 := (iff #40 #227)
|
|
1255 |
#232 := [rewrite]: #231
|
|
1256 |
#254 := [monotonicity #232]: #253
|
|
1257 |
#259 := [trans #254 #257]: #258
|
|
1258 |
#262 := [monotonicity #259]: #261
|
|
1259 |
#270 := [trans #262 #268]: #269
|
|
1260 |
#250 := (iff #46 #247)
|
|
1261 |
#241 := (< #236 #31)
|
|
1262 |
#248 := (iff #241 #247)
|
|
1263 |
#249 := [rewrite]: #248
|
|
1264 |
#242 := (iff #46 #241)
|
|
1265 |
#239 := (= #45 #236)
|
|
1266 |
#233 := (ite #227 #26 #44)
|
|
1267 |
#237 := (= #233 #236)
|
|
1268 |
#238 := [rewrite]: #237
|
|
1269 |
#234 := (= #45 #233)
|
|
1270 |
#235 := [monotonicity #232]: #234
|
|
1271 |
#240 := [trans #235 #238]: #239
|
|
1272 |
#243 := [monotonicity #240]: #242
|
|
1273 |
#251 := [trans #243 #249]: #250
|
|
1274 |
#273 := [monotonicity #251 #270]: #272
|
|
1275 |
#178 := [asserted]: #51
|
|
1276 |
#274 := [mp #178 #273]: #271
|
|
1277 |
#275 := [and-elim #274]: #247
|
|
1278 |
#196 := (* -1::real #31)
|
|
1279 |
#212 := (+ #26 #196)
|
|
1280 |
#213 := (<= #212 0::real)
|
|
1281 |
#214 := (not #213)
|
|
1282 |
#197 := (+ #28 #196)
|
|
1283 |
#195 := (>= #197 0::real)
|
|
1284 |
#193 := (not #195)
|
|
1285 |
#219 := (and #193 #214)
|
|
1286 |
#23 := (< #22 #22)
|
|
1287 |
#35 := (ite #23 #34 #26)
|
|
1288 |
#36 := (< #31 #35)
|
|
1289 |
#29 := (ite #23 #26 #28)
|
|
1290 |
#32 := (< #29 #31)
|
|
1291 |
#37 := (and #32 #36)
|
|
1292 |
#220 := (iff #37 #219)
|
|
1293 |
#217 := (iff #36 #214)
|
|
1294 |
#209 := (< #31 #26)
|
|
1295 |
#215 := (iff #209 #214)
|
|
1296 |
#216 := [rewrite]: #215
|
|
1297 |
#210 := (iff #36 #209)
|
|
1298 |
#207 := (= #35 #26)
|
|
1299 |
#202 := (ite false #34 #26)
|
|
1300 |
#205 := (= #202 #26)
|
|
1301 |
#206 := [rewrite]: #205
|
|
1302 |
#203 := (= #35 #202)
|
|
1303 |
#180 := (iff #23 false)
|
|
1304 |
#181 := [rewrite]: #180
|
|
1305 |
#204 := [monotonicity #181]: #203
|
|
1306 |
#208 := [trans #204 #206]: #207
|
|
1307 |
#211 := [monotonicity #208]: #210
|
|
1308 |
#218 := [trans #211 #216]: #217
|
|
1309 |
#200 := (iff #32 #193)
|
|
1310 |
#189 := (< #28 #31)
|
|
1311 |
#198 := (iff #189 #193)
|
|
1312 |
#199 := [rewrite]: #198
|
|
1313 |
#190 := (iff #32 #189)
|
|
1314 |
#187 := (= #29 #28)
|
|
1315 |
#182 := (ite false #26 #28)
|
|
1316 |
#185 := (= #182 #28)
|
|
1317 |
#186 := [rewrite]: #185
|
|
1318 |
#183 := (= #29 #182)
|
|
1319 |
#184 := [monotonicity #181]: #183
|
|
1320 |
#188 := [trans #184 #186]: #187
|
|
1321 |
#191 := [monotonicity #188]: #190
|
|
1322 |
#201 := [trans #191 #199]: #200
|
|
1323 |
#221 := [monotonicity #201 #218]: #220
|
|
1324 |
#177 := [asserted]: #37
|
|
1325 |
#222 := [mp #177 #221]: #219
|
|
1326 |
#224 := [and-elim #222]: #214
|
|
1327 |
[th-lemma #224 #275 #689]: false
|
|
1328 |
unsat
|
|
1329 |
NX/HT1QOfbspC2LtZNKpBA 428 0
|
|
1330 |
#2 := false
|
|
1331 |
decl uf_10 :: T1
|
|
1332 |
#38 := uf_10
|
|
1333 |
decl uf_3 :: T1
|
|
1334 |
#21 := uf_3
|
|
1335 |
#45 := (= uf_3 uf_10)
|
|
1336 |
decl uf_1 :: (-> int T1)
|
|
1337 |
decl uf_2 :: (-> T1 int)
|
|
1338 |
#39 := (uf_2 uf_10)
|
|
1339 |
#588 := (uf_1 #39)
|
|
1340 |
#686 := (= #588 uf_10)
|
|
1341 |
#589 := (= uf_10 #588)
|
|
1342 |
#4 := (:var 0 T1)
|
|
1343 |
#5 := (uf_2 #4)
|
|
1344 |
#541 := (pattern #5)
|
|
1345 |
#6 := (uf_1 #5)
|
|
1346 |
#93 := (= #4 #6)
|
|
1347 |
#542 := (forall (vars (?x1 T1)) (:pat #541) #93)
|
|
1348 |
#96 := (forall (vars (?x1 T1)) #93)
|
|
1349 |
#545 := (iff #96 #542)
|
|
1350 |
#543 := (iff #93 #93)
|
|
1351 |
#544 := [refl]: #543
|
|
1352 |
#546 := [quant-intro #544]: #545
|
|
1353 |
#454 := (~ #96 #96)
|
|
1354 |
#456 := (~ #93 #93)
|
|
1355 |
#457 := [refl]: #456
|
|
1356 |
#455 := [nnf-pos #457]: #454
|
|
1357 |
#7 := (= #6 #4)
|
|
1358 |
#8 := (forall (vars (?x1 T1)) #7)
|
|
1359 |
#97 := (iff #8 #96)
|
|
1360 |
#94 := (iff #7 #93)
|
|
1361 |
#95 := [rewrite]: #94
|
|
1362 |
#98 := [quant-intro #95]: #97
|
|
1363 |
#92 := [asserted]: #8
|
|
1364 |
#101 := [mp #92 #98]: #96
|
|
1365 |
#452 := [mp~ #101 #455]: #96
|
|
1366 |
#547 := [mp #452 #546]: #542
|
|
1367 |
#590 := (not #542)
|
|
1368 |
#595 := (or #590 #589)
|
|
1369 |
#596 := [quant-inst]: #595
|
|
1370 |
#680 := [unit-resolution #596 #547]: #589
|
|
1371 |
#687 := [symm #680]: #686
|
|
1372 |
#688 := (= uf_3 #588)
|
|
1373 |
#22 := (uf_2 uf_3)
|
|
1374 |
#586 := (uf_1 #22)
|
|
1375 |
#684 := (= #586 #588)
|
|
1376 |
#682 := (= #588 #586)
|
|
1377 |
#678 := (= #39 #22)
|
|
1378 |
#676 := (= #22 #39)
|
|
1379 |
#9 := 0::int
|
|
1380 |
#227 := -1::int
|
|
1381 |
#230 := (* -1::int #39)
|
|
1382 |
#231 := (+ #22 #230)
|
|
1383 |
#296 := (<= #231 0::int)
|
|
1384 |
#70 := (<= #22 #39)
|
|
1385 |
#393 := (iff #70 #296)
|
|
1386 |
#394 := [rewrite]: #393
|
|
1387 |
#347 := [asserted]: #70
|
|
1388 |
#395 := [mp #347 #394]: #296
|
|
1389 |
#229 := (>= #231 0::int)
|
|
1390 |
decl uf_4 :: (-> T2 T3 real)
|
|
1391 |
decl uf_6 :: (-> T1 T3)
|
|
1392 |
#25 := (uf_6 uf_3)
|
|
1393 |
decl uf_7 :: T2
|
|
1394 |
#27 := uf_7
|
|
1395 |
#28 := (uf_4 uf_7 #25)
|
|
1396 |
decl uf_9 :: T2
|
|
1397 |
#33 := uf_9
|
|
1398 |
#34 := (uf_4 uf_9 #25)
|
|
1399 |
#46 := (uf_6 uf_10)
|
|
1400 |
decl uf_5 :: T2
|
|
1401 |
#24 := uf_5
|
|
1402 |
#47 := (uf_4 uf_5 #46)
|
|
1403 |
#48 := (ite #45 #47 #34)
|
|
1404 |
#256 := (ite #229 #48 #28)
|
|
1405 |
#568 := (= #28 #256)
|
|
1406 |
#648 := (not #568)
|
|
1407 |
#194 := 0::real
|
|
1408 |
#192 := -1::real
|
|
1409 |
#265 := (* -1::real #256)
|
|
1410 |
#640 := (+ #28 #265)
|
|
1411 |
#642 := (>= #640 0::real)
|
|
1412 |
#645 := (not #642)
|
|
1413 |
#643 := [hypothesis]: #642
|
|
1414 |
decl uf_8 :: T2
|
|
1415 |
#30 := uf_8
|
|
1416 |
#31 := (uf_4 uf_8 #25)
|
|
1417 |
#266 := (+ #31 #265)
|
|
1418 |
#264 := (>= #266 0::real)
|
|
1419 |
#267 := (not #264)
|
|
1420 |
#26 := (uf_4 uf_5 #25)
|
|
1421 |
decl uf_11 :: T2
|
|
1422 |
#41 := uf_11
|
|
1423 |
#42 := (uf_4 uf_11 #25)
|
|
1424 |
#237 := (ite #229 #42 #26)
|
|
1425 |
#245 := (* -1::real #237)
|
|
1426 |
#246 := (+ #31 #245)
|
|
1427 |
#247 := (<= #246 0::real)
|
|
1428 |
#248 := (not #247)
|
|
1429 |
#272 := (and #248 #267)
|
|
1430 |
#40 := (< #22 #39)
|
|
1431 |
#49 := (ite #40 #28 #48)
|
|
1432 |
#50 := (< #31 #49)
|
|
1433 |
#43 := (ite #40 #26 #42)
|
|
1434 |
#44 := (< #43 #31)
|
|
1435 |
#51 := (and #44 #50)
|
|
1436 |
#273 := (iff #51 #272)
|
|
1437 |
#270 := (iff #50 #267)
|
|
1438 |
#261 := (< #31 #256)
|
|
1439 |
#268 := (iff #261 #267)
|
|
1440 |
#269 := [rewrite]: #268
|
|
1441 |
#262 := (iff #50 #261)
|
|
1442 |
#259 := (= #49 #256)
|
|
1443 |
#228 := (not #229)
|
|
1444 |
#253 := (ite #228 #28 #48)
|
|
1445 |
#257 := (= #253 #256)
|
|
1446 |
#258 := [rewrite]: #257
|
|
1447 |
#254 := (= #49 #253)
|
|
1448 |
#232 := (iff #40 #228)
|
|
1449 |
#233 := [rewrite]: #232
|
|
1450 |
#255 := [monotonicity #233]: #254
|
|
1451 |
#260 := [trans #255 #258]: #259
|
|
1452 |
#263 := [monotonicity #260]: #262
|
|
1453 |
#271 := [trans #263 #269]: #270
|
|
1454 |
#251 := (iff #44 #248)
|
|
1455 |
#242 := (< #237 #31)
|
|
1456 |
#249 := (iff #242 #248)
|
|
1457 |
#250 := [rewrite]: #249
|
|
1458 |
#243 := (iff #44 #242)
|
|
1459 |
#240 := (= #43 #237)
|
|
1460 |
#234 := (ite #228 #26 #42)
|
|
1461 |
#238 := (= #234 #237)
|
|
1462 |
#239 := [rewrite]: #238
|
|
1463 |
#235 := (= #43 #234)
|
|
1464 |
#236 := [monotonicity #233]: #235
|
|
1465 |
#241 := [trans #236 #239]: #240
|
|
1466 |
#244 := [monotonicity #241]: #243
|
|
1467 |
#252 := [trans #244 #250]: #251
|
|
1468 |
#274 := [monotonicity #252 #271]: #273
|
|
1469 |
#178 := [asserted]: #51
|
|
1470 |
#275 := [mp #178 #274]: #272
|
|
1471 |
#277 := [and-elim #275]: #267
|
|
1472 |
#196 := (* -1::real #31)
|
|
1473 |
#197 := (+ #28 #196)
|
|
1474 |
#195 := (>= #197 0::real)
|
|
1475 |
#193 := (not #195)
|
|
1476 |
#213 := (* -1::real #34)
|
|
1477 |
#214 := (+ #31 #213)
|
|
1478 |
#212 := (>= #214 0::real)
|
|
1479 |
#215 := (not #212)
|
|
1480 |
#220 := (and #193 #215)
|
|
1481 |
#23 := (< #22 #22)
|
|
1482 |
#35 := (ite #23 #28 #34)
|
|
1483 |
#36 := (< #31 #35)
|
|
1484 |
#29 := (ite #23 #26 #28)
|
|
1485 |
#32 := (< #29 #31)
|
|
1486 |
#37 := (and #32 #36)
|
|
1487 |
#221 := (iff #37 #220)
|
|
1488 |
#218 := (iff #36 #215)
|
|
1489 |
#209 := (< #31 #34)
|
|
1490 |
#216 := (iff #209 #215)
|
|
1491 |
#217 := [rewrite]: #216
|
|
1492 |
#210 := (iff #36 #209)
|
|
1493 |
#207 := (= #35 #34)
|
|
1494 |
#202 := (ite false #28 #34)
|
|
1495 |
#205 := (= #202 #34)
|
|
1496 |
#206 := [rewrite]: #205
|
|
1497 |
#203 := (= #35 #202)
|
|
1498 |
#180 := (iff #23 false)
|
|
1499 |
#181 := [rewrite]: #180
|
|
1500 |
#204 := [monotonicity #181]: #203
|
|
1501 |
#208 := [trans #204 #206]: #207
|
|
1502 |
#211 := [monotonicity #208]: #210
|
|
1503 |
#219 := [trans #211 #217]: #218
|
|
1504 |
#200 := (iff #32 #193)
|
|
1505 |
#189 := (< #28 #31)
|
|
1506 |
#198 := (iff #189 #193)
|
|
1507 |
#199 := [rewrite]: #198
|
|
1508 |
#190 := (iff #32 #189)
|
|
1509 |
#187 := (= #29 #28)
|
|
1510 |
#182 := (ite false #26 #28)
|
|
1511 |
#185 := (= #182 #28)
|
|
1512 |
#186 := [rewrite]: #185
|
|
1513 |
#183 := (= #29 #182)
|
|
1514 |
#184 := [monotonicity #181]: #183
|
|
1515 |
#188 := [trans #184 #186]: #187
|
|
1516 |
#191 := [monotonicity #188]: #190
|
|
1517 |
#201 := [trans #191 #199]: #200
|
|
1518 |
#222 := [monotonicity #201 #219]: #221
|
|
1519 |
#177 := [asserted]: #37
|
|
1520 |
#223 := [mp #177 #222]: #220
|
|
1521 |
#224 := [and-elim #223]: #193
|
|
1522 |
#644 := [th-lemma #224 #277 #643]: false
|
|
1523 |
#646 := [lemma #644]: #645
|
|
1524 |
#647 := [hypothesis]: #568
|
|
1525 |
#649 := (or #648 #642)
|
|
1526 |
#650 := [th-lemma]: #649
|
|
1527 |
#651 := [unit-resolution #650 #647 #646]: false
|
|
1528 |
#652 := [lemma #651]: #648
|
|
1529 |
#578 := (or #229 #568)
|
|
1530 |
#579 := [def-axiom]: #578
|
|
1531 |
#675 := [unit-resolution #579 #652]: #229
|
|
1532 |
#677 := [th-lemma #675 #395]: #676
|
|
1533 |
#679 := [symm #677]: #678
|
|
1534 |
#683 := [monotonicity #679]: #682
|
|
1535 |
#685 := [symm #683]: #684
|
|
1536 |
#587 := (= uf_3 #586)
|
|
1537 |
#591 := (or #590 #587)
|
|
1538 |
#592 := [quant-inst]: #591
|
|
1539 |
#681 := [unit-resolution #592 #547]: #587
|
|
1540 |
#689 := [trans #681 #685]: #688
|
|
1541 |
#690 := [trans #689 #687]: #45
|
|
1542 |
#571 := (not #45)
|
|
1543 |
#54 := (uf_4 uf_11 #46)
|
|
1544 |
#279 := (ite #45 #28 #54)
|
|
1545 |
#465 := (* -1::real #279)
|
|
1546 |
#632 := (+ #28 #465)
|
|
1547 |
#633 := (<= #632 0::real)
|
|
1548 |
#580 := (= #28 #279)
|
|
1549 |
#656 := [hypothesis]: #45
|
|
1550 |
#582 := (or #571 #580)
|
|
1551 |
#583 := [def-axiom]: #582
|
|
1552 |
#657 := [unit-resolution #583 #656]: #580
|
|
1553 |
#658 := (not #580)
|
|
1554 |
#659 := (or #658 #633)
|
|
1555 |
#660 := [th-lemma]: #659
|
|
1556 |
#661 := [unit-resolution #660 #657]: #633
|
|
1557 |
#57 := (uf_4 uf_8 #46)
|
|
1558 |
#363 := (* -1::real #57)
|
|
1559 |
#379 := (+ #47 #363)
|
|
1560 |
#380 := (<= #379 0::real)
|
|
1561 |
#381 := (not #380)
|
|
1562 |
#364 := (+ #54 #363)
|
|
1563 |
#362 := (>= #364 0::real)
|
|
1564 |
#361 := (not #362)
|
|
1565 |
#386 := (and #361 #381)
|
|
1566 |
#59 := (uf_4 uf_7 #46)
|
|
1567 |
#64 := (< #39 #39)
|
|
1568 |
#67 := (ite #64 #59 #47)
|
|
1569 |
#68 := (< #57 #67)
|
|
1570 |
#65 := (ite #64 #47 #54)
|
|
1571 |
#66 := (< #65 #57)
|
|
1572 |
#69 := (and #66 #68)
|
|
1573 |
#387 := (iff #69 #386)
|
|
1574 |
#384 := (iff #68 #381)
|
|
1575 |
#376 := (< #57 #47)
|
|
1576 |
#382 := (iff #376 #381)
|
|
1577 |
#383 := [rewrite]: #382
|
|
1578 |
#377 := (iff #68 #376)
|
|
1579 |
#374 := (= #67 #47)
|
|
1580 |
#369 := (ite false #59 #47)
|
|
1581 |
#372 := (= #369 #47)
|
|
1582 |
#373 := [rewrite]: #372
|
|
1583 |
#370 := (= #67 #369)
|
|
1584 |
#349 := (iff #64 false)
|
|
1585 |
#350 := [rewrite]: #349
|
|
1586 |
#371 := [monotonicity #350]: #370
|
|
1587 |
#375 := [trans #371 #373]: #374
|
|
1588 |
#378 := [monotonicity #375]: #377
|
|
1589 |
#385 := [trans #378 #383]: #384
|
|
1590 |
#367 := (iff #66 #361)
|
|
1591 |
#358 := (< #54 #57)
|
|
1592 |
#365 := (iff #358 #361)
|
|
1593 |
#366 := [rewrite]: #365
|
|
1594 |
#359 := (iff #66 #358)
|
|
1595 |
#356 := (= #65 #54)
|
|
1596 |
#351 := (ite false #47 #54)
|
|
1597 |
#354 := (= #351 #54)
|
|
1598 |
#355 := [rewrite]: #354
|
|
1599 |
#352 := (= #65 #351)
|
|
1600 |
#353 := [monotonicity #350]: #352
|
|
1601 |
#357 := [trans #353 #355]: #356
|
|
1602 |
#360 := [monotonicity #357]: #359
|
|
1603 |
#368 := [trans #360 #366]: #367
|
|
1604 |
#388 := [monotonicity #368 #385]: #387
|
|
1605 |
#346 := [asserted]: #69
|
|
1606 |
#389 := [mp #346 #388]: #386
|
|
1607 |
#391 := [and-elim #389]: #381
|
|
1608 |
#397 := (* -1::real #59)
|
|
1609 |
#398 := (+ #47 #397)
|
|
1610 |
#399 := (<= #398 0::real)
|
|
1611 |
#409 := (* -1::real #54)
|
|
1612 |
#410 := (+ #47 #409)
|
|
1613 |
#408 := (>= #410 0::real)
|
|
1614 |
#60 := (uf_4 uf_9 #46)
|
|
1615 |
#402 := (* -1::real #60)
|
|
1616 |
#403 := (+ #59 #402)
|
|
1617 |
#404 := (<= #403 0::real)
|
|
1618 |
#418 := (and #399 #404 #408)
|
|
1619 |
#73 := (<= #59 #60)
|
|
1620 |
#72 := (<= #47 #59)
|
|
1621 |
#74 := (and #72 #73)
|
|
1622 |
#71 := (<= #54 #47)
|
|
1623 |
#75 := (and #71 #74)
|
|
1624 |
#421 := (iff #75 #418)
|
|
1625 |
#412 := (and #399 #404)
|
|
1626 |
#415 := (and #408 #412)
|
|
1627 |
#419 := (iff #415 #418)
|
|
1628 |
#420 := [rewrite]: #419
|
|
1629 |
#416 := (iff #75 #415)
|
|
1630 |
#413 := (iff #74 #412)
|
|
1631 |
#405 := (iff #73 #404)
|
|
1632 |
#406 := [rewrite]: #405
|
|
1633 |
#400 := (iff #72 #399)
|
|
1634 |
#401 := [rewrite]: #400
|
|
1635 |
#414 := [monotonicity #401 #406]: #413
|
|
1636 |
#407 := (iff #71 #408)
|
|
1637 |
#411 := [rewrite]: #407
|
|
1638 |
#417 := [monotonicity #411 #414]: #416
|
|
1639 |
#422 := [trans #417 #420]: #421
|
|
1640 |
#348 := [asserted]: #75
|
|
1641 |
#423 := [mp #348 #422]: #418
|
|
1642 |
#424 := [and-elim #423]: #399
|
|
1643 |
#637 := (+ #28 #397)
|
|
1644 |
#639 := (>= #637 0::real)
|
|
1645 |
#636 := (= #28 #59)
|
|
1646 |
#666 := (= #59 #28)
|
|
1647 |
#664 := (= #46 #25)
|
|
1648 |
#662 := (= #25 #46)
|
|
1649 |
#663 := [monotonicity #656]: #662
|
|
1650 |
#665 := [symm #663]: #664
|
|
1651 |
#667 := [monotonicity #665]: #666
|
|
1652 |
#668 := [symm #667]: #636
|
|
1653 |
#669 := (not #636)
|
|
1654 |
#670 := (or #669 #639)
|
|
1655 |
#671 := [th-lemma]: #670
|
|
1656 |
#672 := [unit-resolution #671 #668]: #639
|
|
1657 |
#468 := (+ #57 #465)
|
|
1658 |
#471 := (<= #468 0::real)
|
|
1659 |
#444 := (not #471)
|
|
1660 |
#322 := (ite #296 #279 #47)
|
|
1661 |
#330 := (* -1::real #322)
|
|
1662 |
#331 := (+ #57 #330)
|
|
1663 |
#332 := (<= #331 0::real)
|
|
1664 |
#333 := (not #332)
|
|
1665 |
#445 := (iff #333 #444)
|
|
1666 |
#472 := (iff #332 #471)
|
|
1667 |
#469 := (= #331 #468)
|
|
1668 |
#466 := (= #330 #465)
|
|
1669 |
#463 := (= #322 #279)
|
|
1670 |
#1 := true
|
|
1671 |
#458 := (ite true #279 #47)
|
|
1672 |
#461 := (= #458 #279)
|
|
1673 |
#462 := [rewrite]: #461
|
|
1674 |
#459 := (= #322 #458)
|
|
1675 |
#450 := (iff #296 true)
|
|
1676 |
#451 := [iff-true #395]: #450
|
|
1677 |
#460 := [monotonicity #451]: #459
|
|
1678 |
#464 := [trans #460 #462]: #463
|
|
1679 |
#467 := [monotonicity #464]: #466
|
|
1680 |
#470 := [monotonicity #467]: #469
|
|
1681 |
#473 := [monotonicity #470]: #472
|
|
1682 |
#474 := [monotonicity #473]: #445
|
|
1683 |
#303 := (ite #296 #60 #59)
|
|
1684 |
#313 := (* -1::real #303)
|
|
1685 |
#314 := (+ #57 #313)
|
|
1686 |
#312 := (>= #314 0::real)
|
|
1687 |
#311 := (not #312)
|
|
1688 |
#338 := (and #311 #333)
|
|
1689 |
#52 := (< #39 #22)
|
|
1690 |
#61 := (ite #52 #59 #60)
|
|
1691 |
#62 := (< #57 #61)
|
|
1692 |
#53 := (= uf_10 uf_3)
|
|
1693 |
#55 := (ite #53 #28 #54)
|
|
1694 |
#56 := (ite #52 #47 #55)
|
|
1695 |
#58 := (< #56 #57)
|
|
1696 |
#63 := (and #58 #62)
|
|
1697 |
#341 := (iff #63 #338)
|
|
1698 |
#282 := (ite #52 #47 #279)
|
|
1699 |
#285 := (< #282 #57)
|
|
1700 |
#291 := (and #62 #285)
|
|
1701 |
#339 := (iff #291 #338)
|
|
1702 |
#336 := (iff #285 #333)
|
|
1703 |
#327 := (< #322 #57)
|
|
1704 |
#334 := (iff #327 #333)
|
|
1705 |
#335 := [rewrite]: #334
|
|
1706 |
#328 := (iff #285 #327)
|
|
1707 |
#325 := (= #282 #322)
|
|
1708 |
#297 := (not #296)
|
|
1709 |
#319 := (ite #297 #47 #279)
|
|
1710 |
#323 := (= #319 #322)
|
|
1711 |
#324 := [rewrite]: #323
|
|
1712 |
#320 := (= #282 #319)
|
|
1713 |
#298 := (iff #52 #297)
|
|
1714 |
#299 := [rewrite]: #298
|
|
1715 |
#321 := [monotonicity #299]: #320
|
|
1716 |
#326 := [trans #321 #324]: #325
|
|
1717 |
#329 := [monotonicity #326]: #328
|
|
1718 |
#337 := [trans #329 #335]: #336
|
|
1719 |
#317 := (iff #62 #311)
|
|
1720 |
#308 := (< #57 #303)
|
|
1721 |
#315 := (iff #308 #311)
|
|
1722 |
#316 := [rewrite]: #315
|
|
1723 |
#309 := (iff #62 #308)
|
|
1724 |
#306 := (= #61 #303)
|
|
1725 |
#300 := (ite #297 #59 #60)
|
|
1726 |
#304 := (= #300 #303)
|
|
1727 |
#305 := [rewrite]: #304
|
|
1728 |
#301 := (= #61 #300)
|
|
1729 |
#302 := [monotonicity #299]: #301
|
|
1730 |
#307 := [trans #302 #305]: #306
|
|
1731 |
#310 := [monotonicity #307]: #309
|
|
1732 |
#318 := [trans #310 #316]: #317
|
|
1733 |
#340 := [monotonicity #318 #337]: #339
|
|
1734 |
#294 := (iff #63 #291)
|
|
1735 |
#288 := (and #285 #62)
|
|
1736 |
#292 := (iff #288 #291)
|
|
1737 |
#293 := [rewrite]: #292
|
|
1738 |
#289 := (iff #63 #288)
|
|
1739 |
#286 := (iff #58 #285)
|
|
1740 |
#283 := (= #56 #282)
|
|
1741 |
#280 := (= #55 #279)
|
|
1742 |
#226 := (iff #53 #45)
|
|
1743 |
#278 := [rewrite]: #226
|
|
1744 |
#281 := [monotonicity #278]: #280
|
|
1745 |
#284 := [monotonicity #281]: #283
|
|
1746 |
#287 := [monotonicity #284]: #286
|
|
1747 |
#290 := [monotonicity #287]: #289
|
|
1748 |
#295 := [trans #290 #293]: #294
|
|
1749 |
#342 := [trans #295 #340]: #341
|
|
1750 |
#179 := [asserted]: #63
|
|
1751 |
#343 := [mp #179 #342]: #338
|
|
1752 |
#345 := [and-elim #343]: #333
|
|
1753 |
#475 := [mp #345 #474]: #444
|
|
1754 |
#673 := [th-lemma #475 #672 #424 #391 #661]: false
|
|
1755 |
#674 := [lemma #673]: #571
|
|
1756 |
[unit-resolution #674 #690]: false
|
|
1757 |
unsat
|
|
1758 |
IL2powemHjRpCJYwmXFxyw 211 0
|
|
1759 |
#2 := false
|
|
1760 |
#33 := 0::real
|
|
1761 |
decl uf_11 :: (-> T5 T6 real)
|
|
1762 |
decl uf_15 :: T6
|
|
1763 |
#28 := uf_15
|
|
1764 |
decl uf_16 :: T5
|
|
1765 |
#30 := uf_16
|
|
1766 |
#31 := (uf_11 uf_16 uf_15)
|
|
1767 |
decl uf_12 :: (-> T7 T8 T5)
|
|
1768 |
decl uf_14 :: T8
|
|
1769 |
#26 := uf_14
|
|
1770 |
decl uf_13 :: (-> T1 T7)
|
|
1771 |
decl uf_8 :: T1
|
|
1772 |
#16 := uf_8
|
|
1773 |
#25 := (uf_13 uf_8)
|
|
1774 |
#27 := (uf_12 #25 uf_14)
|
|
1775 |
#29 := (uf_11 #27 uf_15)
|
|
1776 |
#73 := -1::real
|
|
1777 |
#84 := (* -1::real #29)
|
|
1778 |
#85 := (+ #84 #31)
|
|
1779 |
#74 := (* -1::real #31)
|
|
1780 |
#75 := (+ #29 #74)
|
|
1781 |
#112 := (>= #75 0::real)
|
|
1782 |
#119 := (ite #112 #75 #85)
|
|
1783 |
#127 := (* -1::real #119)
|
|
1784 |
decl uf_17 :: T5
|
|
1785 |
#37 := uf_17
|
|
1786 |
#38 := (uf_11 uf_17 uf_15)
|
|
1787 |
#102 := -1/3::real
|
|
1788 |
#103 := (* -1/3::real #38)
|
|
1789 |
#128 := (+ #103 #127)
|
|
1790 |
#100 := 1/3::real
|
|
1791 |
#101 := (* 1/3::real #31)
|
|
1792 |
#129 := (+ #101 #128)
|
|
1793 |
#130 := (<= #129 0::real)
|
|
1794 |
#131 := (not #130)
|
|
1795 |
#40 := 3::real
|
|
1796 |
#39 := (- #31 #38)
|
|
1797 |
#41 := (/ #39 3::real)
|
|
1798 |
#32 := (- #29 #31)
|
|
1799 |
#35 := (- #32)
|
|
1800 |
#34 := (< #32 0::real)
|
|
1801 |
#36 := (ite #34 #35 #32)
|
|
1802 |
#42 := (< #36 #41)
|
|
1803 |
#136 := (iff #42 #131)
|
|
1804 |
#104 := (+ #101 #103)
|
|
1805 |
#78 := (< #75 0::real)
|
|
1806 |
#90 := (ite #78 #85 #75)
|
|
1807 |
#109 := (< #90 #104)
|
|
1808 |
#134 := (iff #109 #131)
|
|
1809 |
#124 := (< #119 #104)
|
|
1810 |
#132 := (iff #124 #131)
|
|
1811 |
#133 := [rewrite]: #132
|
|
1812 |
#125 := (iff #109 #124)
|
|
1813 |
#122 := (= #90 #119)
|
|
1814 |
#113 := (not #112)
|
|
1815 |
#116 := (ite #113 #85 #75)
|
|
1816 |
#120 := (= #116 #119)
|
|
1817 |
#121 := [rewrite]: #120
|
|
1818 |
#117 := (= #90 #116)
|
|
1819 |
#114 := (iff #78 #113)
|
|
1820 |
#115 := [rewrite]: #114
|
|
1821 |
#118 := [monotonicity #115]: #117
|
|
1822 |
#123 := [trans #118 #121]: #122
|
|
1823 |
#126 := [monotonicity #123]: #125
|
|
1824 |
#135 := [trans #126 #133]: #134
|
|
1825 |
#110 := (iff #42 #109)
|
|
1826 |
#107 := (= #41 #104)
|
|
1827 |
#93 := (* -1::real #38)
|
|
1828 |
#94 := (+ #31 #93)
|
|
1829 |
#97 := (/ #94 3::real)
|
|
1830 |
#105 := (= #97 #104)
|
|
1831 |
#106 := [rewrite]: #105
|
|
1832 |
#98 := (= #41 #97)
|
|
1833 |
#95 := (= #39 #94)
|
|
1834 |
#96 := [rewrite]: #95
|
|
1835 |
#99 := [monotonicity #96]: #98
|
|
1836 |
#108 := [trans #99 #106]: #107
|
|
1837 |
#91 := (= #36 #90)
|
|
1838 |
#76 := (= #32 #75)
|
|
1839 |
#77 := [rewrite]: #76
|
|
1840 |
#88 := (= #35 #85)
|
|
1841 |
#81 := (- #75)
|
|
1842 |
#86 := (= #81 #85)
|
|
1843 |
#87 := [rewrite]: #86
|
|
1844 |
#82 := (= #35 #81)
|
|
1845 |
#83 := [monotonicity #77]: #82
|
|
1846 |
#89 := [trans #83 #87]: #88
|
|
1847 |
#79 := (iff #34 #78)
|
|
1848 |
#80 := [monotonicity #77]: #79
|
|
1849 |
#92 := [monotonicity #80 #89 #77]: #91
|
|
1850 |
#111 := [monotonicity #92 #108]: #110
|
|
1851 |
#137 := [trans #111 #135]: #136
|
|
1852 |
#72 := [asserted]: #42
|
|
1853 |
#138 := [mp #72 #137]: #131
|
|
1854 |
decl uf_1 :: T1
|
|
1855 |
#4 := uf_1
|
|
1856 |
#43 := (uf_13 uf_1)
|
|
1857 |
#44 := (uf_12 #43 uf_14)
|
|
1858 |
#45 := (uf_11 #44 uf_15)
|
|
1859 |
#149 := (* -1::real #45)
|
|
1860 |
#150 := (+ #38 #149)
|
|
1861 |
#140 := (+ #93 #45)
|
|
1862 |
#161 := (<= #150 0::real)
|
|
1863 |
#168 := (ite #161 #140 #150)
|
|
1864 |
#176 := (* -1::real #168)
|
|
1865 |
#177 := (+ #103 #176)
|
|
1866 |
#178 := (+ #101 #177)
|
|
1867 |
#179 := (<= #178 0::real)
|
|
1868 |
#180 := (not #179)
|
|
1869 |
#46 := (- #45 #38)
|
|
1870 |
#48 := (- #46)
|
|
1871 |
#47 := (< #46 0::real)
|
|
1872 |
#49 := (ite #47 #48 #46)
|
|
1873 |
#50 := (< #49 #41)
|
|
1874 |
#185 := (iff #50 #180)
|
|
1875 |
#143 := (< #140 0::real)
|
|
1876 |
#155 := (ite #143 #150 #140)
|
|
1877 |
#158 := (< #155 #104)
|
|
1878 |
#183 := (iff #158 #180)
|
|
1879 |
#173 := (< #168 #104)
|
|
1880 |
#181 := (iff #173 #180)
|
|
1881 |
#182 := [rewrite]: #181
|
|
1882 |
#174 := (iff #158 #173)
|
|
1883 |
#171 := (= #155 #168)
|
|
1884 |
#162 := (not #161)
|
|
1885 |
#165 := (ite #162 #150 #140)
|
|
1886 |
#169 := (= #165 #168)
|
|
1887 |
#170 := [rewrite]: #169
|
|
1888 |
#166 := (= #155 #165)
|
|
1889 |
#163 := (iff #143 #162)
|
|
1890 |
#164 := [rewrite]: #163
|
|
1891 |
#167 := [monotonicity #164]: #166
|
|
1892 |
#172 := [trans #167 #170]: #171
|
|
1893 |
#175 := [monotonicity #172]: #174
|
|
1894 |
#184 := [trans #175 #182]: #183
|
|
1895 |
#159 := (iff #50 #158)
|
|
1896 |
#156 := (= #49 #155)
|
|
1897 |
#141 := (= #46 #140)
|
|
1898 |
#142 := [rewrite]: #141
|
|
1899 |
#153 := (= #48 #150)
|
|
1900 |
#146 := (- #140)
|
|
1901 |
#151 := (= #146 #150)
|
|
1902 |
#152 := [rewrite]: #151
|
|
1903 |
#147 := (= #48 #146)
|
|
1904 |
#148 := [monotonicity #142]: #147
|
|
1905 |
#154 := [trans #148 #152]: #153
|
|
1906 |
#144 := (iff #47 #143)
|
|
1907 |
#145 := [monotonicity #142]: #144
|
|
1908 |
#157 := [monotonicity #145 #154 #142]: #156
|
|
1909 |
#160 := [monotonicity #157 #108]: #159
|
|
1910 |
#186 := [trans #160 #184]: #185
|
|
1911 |
#139 := [asserted]: #50
|
|
1912 |
#187 := [mp #139 #186]: #180
|
|
1913 |
#299 := (+ #140 #176)
|
|
1914 |
#300 := (<= #299 0::real)
|
|
1915 |
#290 := (= #140 #168)
|
|
1916 |
#329 := [hypothesis]: #162
|
|
1917 |
#191 := (+ #29 #149)
|
|
1918 |
#192 := (<= #191 0::real)
|
|
1919 |
#51 := (<= #29 #45)
|
|
1920 |
#193 := (iff #51 #192)
|
|
1921 |
#194 := [rewrite]: #193
|
|
1922 |
#188 := [asserted]: #51
|
|
1923 |
#195 := [mp #188 #194]: #192
|
|
1924 |
#298 := (+ #75 #127)
|
|
1925 |
#301 := (<= #298 0::real)
|
|
1926 |
#284 := (= #75 #119)
|
|
1927 |
#302 := [hypothesis]: #113
|
|
1928 |
#296 := (+ #85 #127)
|
|
1929 |
#297 := (<= #296 0::real)
|
|
1930 |
#285 := (= #85 #119)
|
|
1931 |
#288 := (or #112 #285)
|
|
1932 |
#289 := [def-axiom]: #288
|
|
1933 |
#303 := [unit-resolution #289 #302]: #285
|
|
1934 |
#304 := (not #285)
|
|
1935 |
#305 := (or #304 #297)
|
|
1936 |
#306 := [th-lemma]: #305
|
|
1937 |
#307 := [unit-resolution #306 #303]: #297
|
|
1938 |
#315 := (not #290)
|
|
1939 |
#310 := (not #300)
|
|
1940 |
#311 := (or #310 #112)
|
|
1941 |
#308 := [hypothesis]: #300
|
|
1942 |
#309 := [th-lemma #308 #307 #138 #302 #187 #195]: false
|
|
1943 |
#312 := [lemma #309]: #311
|
|
1944 |
#322 := [unit-resolution #312 #302]: #310
|
|
1945 |
#316 := (or #315 #300)
|
|
1946 |
#313 := [hypothesis]: #310
|
|
1947 |
#314 := [hypothesis]: #290
|
|
1948 |
#317 := [th-lemma]: #316
|
|
1949 |
#318 := [unit-resolution #317 #314 #313]: false
|
|
1950 |
#319 := [lemma #318]: #316
|
|
1951 |
#323 := [unit-resolution #319 #322]: #315
|
|
1952 |
#292 := (or #162 #290)
|
|
1953 |
#293 := [def-axiom]: #292
|
|
1954 |
#324 := [unit-resolution #293 #323]: #162
|
|
1955 |
#325 := [th-lemma #324 #307 #138 #302 #195]: false
|
|
1956 |
#326 := [lemma #325]: #112
|
|
1957 |
#286 := (or #113 #284)
|
|
1958 |
#287 := [def-axiom]: #286
|
|
1959 |
#330 := [unit-resolution #287 #326]: #284
|
|
1960 |
#331 := (not #284)
|
|
1961 |
#332 := (or #331 #301)
|
|
1962 |
#333 := [th-lemma]: #332
|
|
1963 |
#334 := [unit-resolution #333 #330]: #301
|
|
1964 |
#335 := [th-lemma #326 #334 #195 #329 #138]: false
|
|
1965 |
#336 := [lemma #335]: #161
|
|
1966 |
#327 := [unit-resolution #293 #336]: #290
|
|
1967 |
#328 := [unit-resolution #319 #327]: #300
|
|
1968 |
[th-lemma #326 #334 #195 #328 #187 #138]: false
|
|
1969 |
unsat
|
|
1970 |
GX51o3DUO/UBS3eNP2P9kA 285 0
|
|
1971 |
#2 := false
|
|
1972 |
#7 := 0::real
|
|
1973 |
decl uf_4 :: real
|
|
1974 |
#16 := uf_4
|
|
1975 |
#40 := -1::real
|
|
1976 |
#116 := (* -1::real uf_4)
|
|
1977 |
decl uf_3 :: real
|
|
1978 |
#11 := uf_3
|
|
1979 |
#117 := (+ uf_3 #116)
|
|
1980 |
#128 := (<= #117 0::real)
|
|
1981 |
#129 := (not #128)
|
|
1982 |
#220 := 2/3::real
|
|
1983 |
#221 := (* 2/3::real uf_3)
|
|
1984 |
#222 := (+ #221 #116)
|
|
1985 |
decl uf_2 :: real
|
|
1986 |
#5 := uf_2
|
|
1987 |
#67 := 1/3::real
|
|
1988 |
#68 := (* 1/3::real uf_2)
|
|
1989 |
#233 := (+ #68 #222)
|
|
1990 |
#243 := (<= #233 0::real)
|
|
1991 |
#268 := (not #243)
|
|
1992 |
#287 := [hypothesis]: #268
|
|
1993 |
#41 := (* -1::real uf_2)
|
|
1994 |
decl uf_1 :: real
|
|
1995 |
#4 := uf_1
|
|
1996 |
#42 := (+ uf_1 #41)
|
|
1997 |
#79 := (>= #42 0::real)
|
|
1998 |
#80 := (not #79)
|
|
1999 |
#297 := (or #80 #243)
|
|
2000 |
#158 := (+ uf_1 #116)
|
|
2001 |
#159 := (<= #158 0::real)
|
|
2002 |
#22 := (<= uf_1 uf_4)
|
|
2003 |
#160 := (iff #22 #159)
|
|
2004 |
#161 := [rewrite]: #160
|
|
2005 |
#155 := [asserted]: #22
|
|
2006 |
#162 := [mp #155 #161]: #159
|
|
2007 |
#200 := (* 1/3::real uf_3)
|
|
2008 |
#198 := -4/3::real
|
|
2009 |
#199 := (* -4/3::real uf_2)
|
|
2010 |
#201 := (+ #199 #200)
|
|
2011 |
#202 := (+ uf_1 #201)
|
|
2012 |
#203 := (>= #202 0::real)
|
|
2013 |
#258 := (not #203)
|
|
2014 |
#292 := [hypothesis]: #79
|
|
2015 |
#293 := (or #80 #258)
|
|
2016 |
#69 := -1/3::real
|
|
2017 |
#70 := (* -1/3::real uf_3)
|
|
2018 |
#186 := -2/3::real
|
|
2019 |
#187 := (* -2/3::real uf_2)
|
|
2020 |
#188 := (+ #187 #70)
|
|
2021 |
#189 := (+ uf_1 #188)
|
|
2022 |
#204 := (<= #189 0::real)
|
|
2023 |
#205 := (ite #79 #203 #204)
|
|
2024 |
#210 := (not #205)
|
|
2025 |
#51 := (* -1::real uf_1)
|
|
2026 |
#52 := (+ #51 uf_2)
|
|
2027 |
#86 := (ite #79 #42 #52)
|
|
2028 |
#94 := (* -1::real #86)
|
|
2029 |
#95 := (+ #70 #94)
|
|
2030 |
#96 := (+ #68 #95)
|
|
2031 |
#97 := (<= #96 0::real)
|
|
2032 |
#98 := (not #97)
|
|
2033 |
#211 := (iff #98 #210)
|
|
2034 |
#208 := (iff #97 #205)
|
|
2035 |
#182 := 4/3::real
|
|
2036 |
#183 := (* 4/3::real uf_2)
|
|
2037 |
#184 := (+ #183 #70)
|
|
2038 |
#185 := (+ #51 #184)
|
|
2039 |
#190 := (ite #79 #185 #189)
|
|
2040 |
#195 := (<= #190 0::real)
|
|
2041 |
#206 := (iff #195 #205)
|
|
2042 |
#207 := [rewrite]: #206
|
|
2043 |
#196 := (iff #97 #195)
|
|
2044 |
#193 := (= #96 #190)
|
|
2045 |
#172 := (+ #41 #70)
|
|
2046 |
#173 := (+ uf_1 #172)
|
|
2047 |
#170 := (+ uf_2 #70)
|
|
2048 |
#171 := (+ #51 #170)
|
|
2049 |
#174 := (ite #79 #171 #173)
|
|
2050 |
#179 := (+ #68 #174)
|
|
2051 |
#191 := (= #179 #190)
|
|
2052 |
#192 := [rewrite]: #191
|
|
2053 |
#180 := (= #96 #179)
|
|
2054 |
#177 := (= #95 #174)
|
|
2055 |
#164 := (ite #79 #52 #42)
|
|
2056 |
#167 := (+ #70 #164)
|
|
2057 |
#175 := (= #167 #174)
|
|
2058 |
#176 := [rewrite]: #175
|
|
2059 |
#168 := (= #95 #167)
|
|
2060 |
#156 := (= #94 #164)
|
|
2061 |
#165 := [rewrite]: #156
|
|
2062 |
#169 := [monotonicity #165]: #168
|
|
2063 |
#178 := [trans #169 #176]: #177
|
|
2064 |
#181 := [monotonicity #178]: #180
|
|
2065 |
#194 := [trans #181 #192]: #193
|
|
2066 |
#197 := [monotonicity #194]: #196
|
|
2067 |
#209 := [trans #197 #207]: #208
|
|
2068 |
#212 := [monotonicity #209]: #211
|
|
2069 |
#13 := 3::real
|
|
2070 |
#12 := (- uf_2 uf_3)
|
|
2071 |
#14 := (/ #12 3::real)
|
|
2072 |
#6 := (- uf_1 uf_2)
|
|
2073 |
#9 := (- #6)
|
|
2074 |
#8 := (< #6 0::real)
|
|
2075 |
#10 := (ite #8 #9 #6)
|
|
2076 |
#15 := (< #10 #14)
|
|
2077 |
#103 := (iff #15 #98)
|
|
2078 |
#71 := (+ #68 #70)
|
|
2079 |
#45 := (< #42 0::real)
|
|
2080 |
#57 := (ite #45 #52 #42)
|
|
2081 |
#76 := (< #57 #71)
|
|
2082 |
#101 := (iff #76 #98)
|
|
2083 |
#91 := (< #86 #71)
|
|
2084 |
#99 := (iff #91 #98)
|
|
2085 |
#100 := [rewrite]: #99
|
|
2086 |
#92 := (iff #76 #91)
|
|
2087 |
#89 := (= #57 #86)
|
|
2088 |
#83 := (ite #80 #52 #42)
|
|
2089 |
#87 := (= #83 #86)
|
|
2090 |
#88 := [rewrite]: #87
|
|
2091 |
#84 := (= #57 #83)
|
|
2092 |
#81 := (iff #45 #80)
|
|
2093 |
#82 := [rewrite]: #81
|
|
2094 |
#85 := [monotonicity #82]: #84
|
|
2095 |
#90 := [trans #85 #88]: #89
|
|
2096 |
#93 := [monotonicity #90]: #92
|
|
2097 |
#102 := [trans #93 #100]: #101
|
|
2098 |
#77 := (iff #15 #76)
|
|
2099 |
#74 := (= #14 #71)
|
|
2100 |
#60 := (* -1::real uf_3)
|
|
2101 |
#61 := (+ uf_2 #60)
|
|
2102 |
#64 := (/ #61 3::real)
|
|
2103 |
#72 := (= #64 #71)
|
|
2104 |
#73 := [rewrite]: #72
|
|
2105 |
#65 := (= #14 #64)
|
|
2106 |
#62 := (= #12 #61)
|
|
2107 |
#63 := [rewrite]: #62
|
|
2108 |
#66 := [monotonicity #63]: #65
|
|
2109 |
#75 := [trans #66 #73]: #74
|
|
2110 |
#58 := (= #10 #57)
|
|
2111 |
#43 := (= #6 #42)
|
|
2112 |
#44 := [rewrite]: #43
|
|
2113 |
#55 := (= #9 #52)
|
|
2114 |
#48 := (- #42)
|
|
2115 |
#53 := (= #48 #52)
|
|
2116 |
#54 := [rewrite]: #53
|
|
2117 |
#49 := (= #9 #48)
|
|
2118 |
#50 := [monotonicity #44]: #49
|
|
2119 |
#56 := [trans #50 #54]: #55
|
|
2120 |
#46 := (iff #8 #45)
|
|
2121 |
#47 := [monotonicity #44]: #46
|
|
2122 |
#59 := [monotonicity #47 #56 #44]: #58
|
|
2123 |
#78 := [monotonicity #59 #75]: #77
|
|
2124 |
#104 := [trans #78 #102]: #103
|
|
2125 |
#39 := [asserted]: #15
|
|
2126 |
#105 := [mp #39 #104]: #98
|
|
2127 |
#213 := [mp #105 #212]: #210
|
|
2128 |
#259 := (or #205 #80 #258)
|
|
2129 |
#260 := [def-axiom]: #259
|
|
2130 |
#294 := [unit-resolution #260 #213]: #293
|
|
2131 |
#295 := [unit-resolution #294 #292]: #258
|
|
2132 |
#296 := [th-lemma #287 #292 #295 #162]: false
|
|
2133 |
#298 := [lemma #296]: #297
|
|
2134 |
#299 := [unit-resolution #298 #287]: #80
|
|
2135 |
#261 := (not #204)
|
|
2136 |
#281 := (or #79 #261)
|
|
2137 |
#262 := (or #205 #79 #261)
|
|
2138 |
#263 := [def-axiom]: #262
|
|
2139 |
#282 := [unit-resolution #263 #213]: #281
|
|
2140 |
#300 := [unit-resolution #282 #299]: #261
|
|
2141 |
#290 := (or #79 #204 #243)
|
|
2142 |
#276 := [hypothesis]: #261
|
|
2143 |
#288 := [hypothesis]: #80
|
|
2144 |
#289 := [th-lemma #288 #276 #162 #287]: false
|
|
2145 |
#291 := [lemma #289]: #290
|
|
2146 |
#301 := [unit-resolution #291 #300 #299 #287]: false
|
|
2147 |
#302 := [lemma #301]: #243
|
|
2148 |
#303 := (or #129 #268)
|
|
2149 |
#223 := (* -4/3::real uf_3)
|
|
2150 |
#224 := (+ #223 uf_4)
|
|
2151 |
#234 := (+ #68 #224)
|
|
2152 |
#244 := (<= #234 0::real)
|
|
2153 |
#245 := (ite #128 #243 #244)
|
|
2154 |
#250 := (not #245)
|
|
2155 |
#107 := (+ #60 uf_4)
|
|
2156 |
#135 := (ite #128 #107 #117)
|
|
2157 |
#143 := (* -1::real #135)
|
|
2158 |
#144 := (+ #70 #143)
|
|
2159 |
#145 := (+ #68 #144)
|
|
2160 |
#146 := (<= #145 0::real)
|
|
2161 |
#147 := (not #146)
|
|
2162 |
#251 := (iff #147 #250)
|
|
2163 |
#248 := (iff #146 #245)
|
|
2164 |
#235 := (ite #128 #233 #234)
|
|
2165 |
#240 := (<= #235 0::real)
|
|
2166 |
#246 := (iff #240 #245)
|
|
2167 |
#247 := [rewrite]: #246
|
|
2168 |
#241 := (iff #146 #240)
|
|
2169 |
#238 := (= #145 #235)
|
|
2170 |
#225 := (ite #128 #222 #224)
|
|
2171 |
#230 := (+ #68 #225)
|
|
2172 |
#236 := (= #230 #235)
|
|
2173 |
#237 := [rewrite]: #236
|
|
2174 |
#231 := (= #145 #230)
|
|
2175 |
#228 := (= #144 #225)
|
|
2176 |
#214 := (ite #128 #117 #107)
|
|
2177 |
#217 := (+ #70 #214)
|
|
2178 |
#226 := (= #217 #225)
|
|
2179 |
#227 := [rewrite]: #226
|
|
2180 |
#218 := (= #144 #217)
|
|
2181 |
#215 := (= #143 #214)
|
|
2182 |
#216 := [rewrite]: #215
|
|
2183 |
#219 := [monotonicity #216]: #218
|
|
2184 |
#229 := [trans #219 #227]: #228
|
|
2185 |
#232 := [monotonicity #229]: #231
|
|
2186 |
#239 := [trans #232 #237]: #238
|
|
2187 |
#242 := [monotonicity #239]: #241
|
|
2188 |
#249 := [trans #242 #247]: #248
|
|
2189 |
#252 := [monotonicity #249]: #251
|
|
2190 |
#17 := (- uf_4 uf_3)
|
|
2191 |
#19 := (- #17)
|
|
2192 |
#18 := (< #17 0::real)
|
|
2193 |
#20 := (ite #18 #19 #17)
|
|
2194 |
#21 := (< #20 #14)
|
|
2195 |
#152 := (iff #21 #147)
|
|
2196 |
#110 := (< #107 0::real)
|
|
2197 |
#122 := (ite #110 #117 #107)
|
|
2198 |
#125 := (< #122 #71)
|
|
2199 |
#150 := (iff #125 #147)
|
|
2200 |
#140 := (< #135 #71)
|
|
2201 |
#148 := (iff #140 #147)
|
|
2202 |
#149 := [rewrite]: #148
|
|
2203 |
#141 := (iff #125 #140)
|
|
2204 |
#138 := (= #122 #135)
|
|
2205 |
#132 := (ite #129 #117 #107)
|
|
2206 |
#136 := (= #132 #135)
|
|
2207 |
#137 := [rewrite]: #136
|
|
2208 |
#133 := (= #122 #132)
|
|
2209 |
#130 := (iff #110 #129)
|
|
2210 |
#131 := [rewrite]: #130
|
|
2211 |
#134 := [monotonicity #131]: #133
|
|
2212 |
#139 := [trans #134 #137]: #138
|
|
2213 |
#142 := [monotonicity #139]: #141
|
|
2214 |
#151 := [trans #142 #149]: #150
|
|
2215 |
#126 := (iff #21 #125)
|
|
2216 |
#123 := (= #20 #122)
|
|
2217 |
#108 := (= #17 #107)
|
|
2218 |
#109 := [rewrite]: #108
|
|
2219 |
#120 := (= #19 #117)
|
|
2220 |
#113 := (- #107)
|
|
2221 |
#118 := (= #113 #117)
|
|
2222 |
#119 := [rewrite]: #118
|
|
2223 |
#114 := (= #19 #113)
|
|
2224 |
#115 := [monotonicity #109]: #114
|
|
2225 |
#121 := [trans #115 #119]: #120
|
|
2226 |
#111 := (iff #18 #110)
|
|
2227 |
#112 := [monotonicity #109]: #111
|
|
2228 |
#124 := [monotonicity #112 #121 #109]: #123
|
|
2229 |
#127 := [monotonicity #124 #75]: #126
|
|
2230 |
#153 := [trans #127 #151]: #152
|
|
2231 |
#106 := [asserted]: #21
|
|
2232 |
#154 := [mp #106 #153]: #147
|
|
2233 |
#253 := [mp #154 #252]: #250
|
|
2234 |
#269 := (or #245 #129 #268)
|
|
2235 |
#270 := [def-axiom]: #269
|
|
2236 |
#304 := [unit-resolution #270 #253]: #303
|
|
2237 |
#305 := [unit-resolution #304 #302]: #129
|
|
2238 |
#271 := (not #244)
|
|
2239 |
#306 := (or #128 #271)
|
|
2240 |
#272 := (or #245 #128 #271)
|
|
2241 |
#273 := [def-axiom]: #272
|
|
2242 |
#307 := [unit-resolution #273 #253]: #306
|
|
2243 |
#308 := [unit-resolution #307 #305]: #271
|
|
2244 |
#285 := (or #128 #244)
|
|
2245 |
#274 := [hypothesis]: #271
|
|
2246 |
#275 := [hypothesis]: #129
|
|
2247 |
#278 := (or #204 #128 #244)
|
|
2248 |
#277 := [th-lemma #276 #275 #274 #162]: false
|
|
2249 |
#279 := [lemma #277]: #278
|
|
2250 |
#280 := [unit-resolution #279 #275 #274]: #204
|
|
2251 |
#283 := [unit-resolution #282 #280]: #79
|
|
2252 |
#284 := [th-lemma #275 #274 #283 #162]: false
|
|
2253 |
#286 := [lemma #284]: #285
|
|
2254 |
[unit-resolution #286 #308 #305]: false
|
|
2255 |
unsat
|
|
2256 |
cebG074uorSr8ODzgTmcKg 97 0
|
|
2257 |
#2 := false
|
|
2258 |
#18 := 0::real
|
|
2259 |
decl uf_1 :: (-> T2 T1 real)
|
|
2260 |
decl uf_5 :: T1
|
|
2261 |
#11 := uf_5
|
|
2262 |
decl uf_2 :: T2
|
|
2263 |
#4 := uf_2
|
|
2264 |
#20 := (uf_1 uf_2 uf_5)
|
|
2265 |
#42 := -1::real
|
|
2266 |
#53 := (* -1::real #20)
|
|
2267 |
decl uf_3 :: T2
|
|
2268 |
#7 := uf_3
|
|
2269 |
#19 := (uf_1 uf_3 uf_5)
|
|
2270 |
#54 := (+ #19 #53)
|
|
2271 |
#63 := (<= #54 0::real)
|
|
2272 |
#21 := (- #19 #20)
|
|
2273 |
#22 := (< 0::real #21)
|
|
2274 |
#23 := (not #22)
|
|
2275 |
#74 := (iff #23 #63)
|
|
2276 |
#57 := (< 0::real #54)
|
|
2277 |
#60 := (not #57)
|
|
2278 |
#72 := (iff #60 #63)
|
|
2279 |
#64 := (not #63)
|
|
2280 |
#67 := (not #64)
|
|
2281 |
#70 := (iff #67 #63)
|
|
2282 |
#71 := [rewrite]: #70
|
|
2283 |
#68 := (iff #60 #67)
|
|
2284 |
#65 := (iff #57 #64)
|
|
2285 |
#66 := [rewrite]: #65
|
|
2286 |
#69 := [monotonicity #66]: #68
|
|
2287 |
#73 := [trans #69 #71]: #72
|
|
2288 |
#61 := (iff #23 #60)
|
|
2289 |
#58 := (iff #22 #57)
|
|
2290 |
#55 := (= #21 #54)
|
|
2291 |
#56 := [rewrite]: #55
|
|
2292 |
#59 := [monotonicity #56]: #58
|
|
2293 |
#62 := [monotonicity #59]: #61
|
|
2294 |
#75 := [trans #62 #73]: #74
|
|
2295 |
#41 := [asserted]: #23
|
|
2296 |
#76 := [mp #41 #75]: #63
|
|
2297 |
#5 := (:var 0 T1)
|
|
2298 |
#8 := (uf_1 uf_3 #5)
|
|
2299 |
#141 := (pattern #8)
|
|
2300 |
#6 := (uf_1 uf_2 #5)
|
|
2301 |
#140 := (pattern #6)
|
|
2302 |
#45 := (* -1::real #8)
|
|
2303 |
#46 := (+ #6 #45)
|
|
2304 |
#44 := (>= #46 0::real)
|
|
2305 |
#43 := (not #44)
|
|
2306 |
#142 := (forall (vars (?x1 T1)) (:pat #140 #141) #43)
|
|
2307 |
#49 := (forall (vars (?x1 T1)) #43)
|
|
2308 |
#145 := (iff #49 #142)
|
|
2309 |
#143 := (iff #43 #43)
|
|
2310 |
#144 := [refl]: #143
|
|
2311 |
#146 := [quant-intro #144]: #145
|
|
2312 |
#80 := (~ #49 #49)
|
|
2313 |
#82 := (~ #43 #43)
|
|
2314 |
#83 := [refl]: #82
|
|
2315 |
#81 := [nnf-pos #83]: #80
|
|
2316 |
#9 := (< #6 #8)
|
|
2317 |
#10 := (forall (vars (?x1 T1)) #9)
|
|
2318 |
#50 := (iff #10 #49)
|
|
2319 |
#47 := (iff #9 #43)
|
|
2320 |
#48 := [rewrite]: #47
|
|
2321 |
#51 := [quant-intro #48]: #50
|
|
2322 |
#39 := [asserted]: #10
|
|
2323 |
#52 := [mp #39 #51]: #49
|
|
2324 |
#79 := [mp~ #52 #81]: #49
|
|
2325 |
#147 := [mp #79 #146]: #142
|
|
2326 |
#164 := (not #142)
|
|
2327 |
#165 := (or #164 #64)
|
|
2328 |
#148 := (* -1::real #19)
|
|
2329 |
#149 := (+ #20 #148)
|
|
2330 |
#150 := (>= #149 0::real)
|
|
2331 |
#151 := (not #150)
|
|
2332 |
#166 := (or #164 #151)
|
|
2333 |
#168 := (iff #166 #165)
|
|
2334 |
#170 := (iff #165 #165)
|
|
2335 |
#171 := [rewrite]: #170
|
|
2336 |
#162 := (iff #151 #64)
|
|
2337 |
#160 := (iff #150 #63)
|
|
2338 |
#152 := (+ #148 #20)
|
|
2339 |
#155 := (>= #152 0::real)
|
|
2340 |
#158 := (iff #155 #63)
|
|
2341 |
#159 := [rewrite]: #158
|
|
2342 |
#156 := (iff #150 #155)
|
|
2343 |
#153 := (= #149 #152)
|
|
2344 |
#154 := [rewrite]: #153
|
|
2345 |
#157 := [monotonicity #154]: #156
|
|
2346 |
#161 := [trans #157 #159]: #160
|
|
2347 |
#163 := [monotonicity #161]: #162
|
|
2348 |
#169 := [monotonicity #163]: #168
|
|
2349 |
#172 := [trans #169 #171]: #168
|
|
2350 |
#167 := [quant-inst]: #166
|
|
2351 |
#173 := [mp #167 #172]: #165
|
|
2352 |
[unit-resolution #173 #147 #76]: false
|
|
2353 |
unsat
|
|
2354 |
DKRtrJ2XceCkITuNwNViRw 57 0
|
|
2355 |
#2 := false
|
|
2356 |
#4 := 0::real
|
|
2357 |
decl uf_1 :: (-> T2 real)
|
|
2358 |
decl uf_2 :: (-> T1 T1 T2)
|
|
2359 |
decl uf_12 :: (-> T4 T1)
|
|
2360 |
decl uf_4 :: T4
|
|
2361 |
#11 := uf_4
|
|
2362 |
#39 := (uf_12 uf_4)
|
|
2363 |
decl uf_10 :: T4
|
|
2364 |
#27 := uf_10
|
|
2365 |
#38 := (uf_12 uf_10)
|
|
2366 |
#40 := (uf_2 #38 #39)
|
|
2367 |
#41 := (uf_1 #40)
|
|
2368 |
#264 := (>= #41 0::real)
|
|
2369 |
#266 := (not #264)
|
|
2370 |
#43 := (= #41 0::real)
|
|
2371 |
#44 := (not #43)
|
|
2372 |
#131 := [asserted]: #44
|
|
2373 |
#272 := (or #43 #266)
|
|
2374 |
#42 := (<= #41 0::real)
|
|
2375 |
#130 := [asserted]: #42
|
|
2376 |
#265 := (not #42)
|
|
2377 |
#270 := (or #43 #265 #266)
|
|
2378 |
#271 := [th-lemma]: #270
|
|
2379 |
#273 := [unit-resolution #271 #130]: #272
|
|
2380 |
#274 := [unit-resolution #273 #131]: #266
|
|
2381 |
#6 := (:var 0 T1)
|
|
2382 |
#5 := (:var 1 T1)
|
|
2383 |
#7 := (uf_2 #5 #6)
|
|
2384 |
#241 := (pattern #7)
|
|
2385 |
#8 := (uf_1 #7)
|
|
2386 |
#65 := (>= #8 0::real)
|
|
2387 |
#242 := (forall (vars (?x1 T1) (?x2 T1)) (:pat #241) #65)
|
|
2388 |
#66 := (forall (vars (?x1 T1) (?x2 T1)) #65)
|
|
2389 |
#245 := (iff #66 #242)
|
|
2390 |
#243 := (iff #65 #65)
|
|
2391 |
#244 := [refl]: #243
|
|
2392 |
#246 := [quant-intro #244]: #245
|
|
2393 |
#149 := (~ #66 #66)
|
|
2394 |
#151 := (~ #65 #65)
|
|
2395 |
#152 := [refl]: #151
|
|
2396 |
#150 := [nnf-pos #152]: #149
|
|
2397 |
#9 := (<= 0::real #8)
|
|
2398 |
#10 := (forall (vars (?x1 T1) (?x2 T1)) #9)
|
|
2399 |
#67 := (iff #10 #66)
|
|
2400 |
#63 := (iff #9 #65)
|
|
2401 |
#64 := [rewrite]: #63
|
|
2402 |
#68 := [quant-intro #64]: #67
|
|
2403 |
#60 := [asserted]: #10
|
|
2404 |
#69 := [mp #60 #68]: #66
|
|
2405 |
#147 := [mp~ #69 #150]: #66
|
|
2406 |
#247 := [mp #147 #246]: #242
|
|
2407 |
#267 := (not #242)
|
|
2408 |
#268 := (or #267 #264)
|
|
2409 |
#269 := [quant-inst]: #268
|
|
2410 |
[unit-resolution #269 #247 #274]: false
|
|
2411 |
unsat
|
|
2412 |
97KJAJfUio+nGchEHWvgAw 91 0
|
|
2413 |
#2 := false
|
|
2414 |
#38 := 0::real
|
|
2415 |
decl uf_1 :: (-> T1 T2 real)
|
|
2416 |
decl uf_3 :: T2
|
|
2417 |
#5 := uf_3
|
|
2418 |
decl uf_4 :: T1
|
|
2419 |
#7 := uf_4
|
|
2420 |
#8 := (uf_1 uf_4 uf_3)
|
|
2421 |
#35 := -1::real
|
|
2422 |
#36 := (* -1::real #8)
|
|
2423 |
decl uf_2 :: T1
|
|
2424 |
#4 := uf_2
|
|
2425 |
#6 := (uf_1 uf_2 uf_3)
|
|
2426 |
#37 := (+ #6 #36)
|
|
2427 |
#130 := (>= #37 0::real)
|
|
2428 |
#155 := (not #130)
|
|
2429 |
#43 := (= #6 #8)
|
|
2430 |
#55 := (not #43)
|
|
2431 |
#15 := (= #8 #6)
|
|
2432 |
#16 := (not #15)
|
|
2433 |
#56 := (iff #16 #55)
|
|
2434 |
#53 := (iff #15 #43)
|
|
2435 |
#54 := [rewrite]: #53
|
|
2436 |
#57 := [monotonicity #54]: #56
|
|
2437 |
#34 := [asserted]: #16
|
|
2438 |
#60 := [mp #34 #57]: #55
|
|
2439 |
#158 := (or #43 #155)
|
|
2440 |
#39 := (<= #37 0::real)
|
|
2441 |
#9 := (<= #6 #8)
|
|
2442 |
#40 := (iff #9 #39)
|
|
2443 |
#41 := [rewrite]: #40
|
|
2444 |
#32 := [asserted]: #9
|
|
2445 |
#42 := [mp #32 #41]: #39
|
|
2446 |
#154 := (not #39)
|
|
2447 |
#156 := (or #43 #154 #155)
|
|
2448 |
#157 := [th-lemma]: #156
|
|
2449 |
#159 := [unit-resolution #157 #42]: #158
|
|
2450 |
#160 := [unit-resolution #159 #60]: #155
|
|
2451 |
#10 := (:var 0 T2)
|
|
2452 |
#12 := (uf_1 uf_2 #10)
|
|
2453 |
#123 := (pattern #12)
|
|
2454 |
#11 := (uf_1 uf_4 #10)
|
|
2455 |
#122 := (pattern #11)
|
|
2456 |
#44 := (* -1::real #12)
|
|
2457 |
#45 := (+ #11 #44)
|
|
2458 |
#46 := (<= #45 0::real)
|
|
2459 |
#124 := (forall (vars (?x1 T2)) (:pat #122 #123) #46)
|
|
2460 |
#49 := (forall (vars (?x1 T2)) #46)
|
|
2461 |
#127 := (iff #49 #124)
|
|
2462 |
#125 := (iff #46 #46)
|
|
2463 |
#126 := [refl]: #125
|
|
2464 |
#128 := [quant-intro #126]: #127
|
|
2465 |
#62 := (~ #49 #49)
|
|
2466 |
#64 := (~ #46 #46)
|
|
2467 |
#65 := [refl]: #64
|
|
2468 |
#63 := [nnf-pos #65]: #62
|
|
2469 |
#13 := (<= #11 #12)
|
|
2470 |
#14 := (forall (vars (?x1 T2)) #13)
|
|
2471 |
#50 := (iff #14 #49)
|
|
2472 |
#47 := (iff #13 #46)
|
|
2473 |
#48 := [rewrite]: #47
|
|
2474 |
#51 := [quant-intro #48]: #50
|
|
2475 |
#33 := [asserted]: #14
|
|
2476 |
#52 := [mp #33 #51]: #49
|
|
2477 |
#61 := [mp~ #52 #63]: #49
|
|
2478 |
#129 := [mp #61 #128]: #124
|
|
2479 |
#144 := (not #124)
|
|
2480 |
#145 := (or #144 #130)
|
|
2481 |
#131 := (* -1::real #6)
|
|
2482 |
#132 := (+ #8 #131)
|
|
2483 |
#133 := (<= #132 0::real)
|
|
2484 |
#146 := (or #144 #133)
|
|
2485 |
#148 := (iff #146 #145)
|
|
2486 |
#150 := (iff #145 #145)
|
|
2487 |
#151 := [rewrite]: #150
|
|
2488 |
#142 := (iff #133 #130)
|
|
2489 |
#134 := (+ #131 #8)
|
|
2490 |
#137 := (<= #134 0::real)
|
|
2491 |
#140 := (iff #137 #130)
|
|
2492 |
#141 := [rewrite]: #140
|
|
2493 |
#138 := (iff #133 #137)
|
|
2494 |
#135 := (= #132 #134)
|
|
2495 |
#136 := [rewrite]: #135
|
|
2496 |
#139 := [monotonicity #136]: #138
|
|
2497 |
#143 := [trans #139 #141]: #142
|
|
2498 |
#149 := [monotonicity #143]: #148
|
|
2499 |
#152 := [trans #149 #151]: #148
|
|
2500 |
#147 := [quant-inst]: #146
|
|
2501 |
#153 := [mp #147 #152]: #145
|
|
2502 |
[unit-resolution #153 #129 #160]: false
|
|
2503 |
unsat
|
|
2504 |
flJYbeWfe+t2l/zsRqdujA 149 0
|
|
2505 |
#2 := false
|
|
2506 |
#19 := 0::real
|
|
2507 |
decl uf_1 :: (-> T1 T2 real)
|
|
2508 |
decl uf_3 :: T2
|
|
2509 |
#5 := uf_3
|
|
2510 |
decl uf_4 :: T1
|
|
2511 |
#7 := uf_4
|
|
2512 |
#8 := (uf_1 uf_4 uf_3)
|
|
2513 |
#44 := -1::real
|
|
2514 |
#156 := (* -1::real #8)
|
|
2515 |
decl uf_2 :: T1
|
|
2516 |
#4 := uf_2
|
|
2517 |
#6 := (uf_1 uf_2 uf_3)
|
|
2518 |
#203 := (+ #6 #156)
|
|
2519 |
#205 := (>= #203 0::real)
|
|
2520 |
#9 := (= #6 #8)
|
|
2521 |
#40 := [asserted]: #9
|
|
2522 |
#208 := (not #9)
|
|
2523 |
#209 := (or #208 #205)
|
|
2524 |
#210 := [th-lemma]: #209
|
|
2525 |
#211 := [unit-resolution #210 #40]: #205
|
|
2526 |
decl uf_5 :: T1
|
|
2527 |
#12 := uf_5
|
|
2528 |
#22 := (uf_1 uf_5 uf_3)
|
|
2529 |
#160 := (* -1::real #22)
|
|
2530 |
#161 := (+ #6 #160)
|
|
2531 |
#207 := (>= #161 0::real)
|
|
2532 |
#222 := (not #207)
|
|
2533 |
#206 := (= #6 #22)
|
|
2534 |
#216 := (not #206)
|
|
2535 |
#62 := (= #8 #22)
|
|
2536 |
#70 := (not #62)
|
|
2537 |
#217 := (iff #70 #216)
|
|
2538 |
#214 := (iff #62 #206)
|
|
2539 |
#212 := (iff #206 #62)
|
|
2540 |
#213 := [monotonicity #40]: #212
|
|
2541 |
#215 := [symm #213]: #214
|
|
2542 |
#218 := [monotonicity #215]: #217
|
|
2543 |
#23 := (= #22 #8)
|
|
2544 |
#24 := (not #23)
|
|
2545 |
#71 := (iff #24 #70)
|
|
2546 |
#68 := (iff #23 #62)
|
|
2547 |
#69 := [rewrite]: #68
|
|
2548 |
#72 := [monotonicity #69]: #71
|
|
2549 |
#43 := [asserted]: #24
|
|
2550 |
#75 := [mp #43 #72]: #70
|
|
2551 |
#219 := [mp #75 #218]: #216
|
|
2552 |
#225 := (or #206 #222)
|
|
2553 |
#162 := (<= #161 0::real)
|
|
2554 |
#172 := (+ #8 #160)
|
|
2555 |
#173 := (>= #172 0::real)
|
|
2556 |
#178 := (not #173)
|
|
2557 |
#163 := (not #162)
|
|
2558 |
#181 := (or #163 #178)
|
|
2559 |
#184 := (not #181)
|
|
2560 |
#10 := (:var 0 T2)
|
|
2561 |
#15 := (uf_1 uf_4 #10)
|
|
2562 |
#149 := (pattern #15)
|
|
2563 |
#13 := (uf_1 uf_5 #10)
|
|
2564 |
#148 := (pattern #13)
|
|
2565 |
#11 := (uf_1 uf_2 #10)
|
|
2566 |
#147 := (pattern #11)
|
|
2567 |
#50 := (* -1::real #15)
|
|
2568 |
#51 := (+ #13 #50)
|
|
2569 |
#52 := (<= #51 0::real)
|
|
2570 |
#76 := (not #52)
|
|
2571 |
#45 := (* -1::real #13)
|
|
2572 |
#46 := (+ #11 #45)
|
|
2573 |
#47 := (<= #46 0::real)
|
|
2574 |
#78 := (not #47)
|
|
2575 |
#73 := (or #78 #76)
|
|
2576 |
#83 := (not #73)
|
|
2577 |
#150 := (forall (vars (?x1 T2)) (:pat #147 #148 #149) #83)
|
|
2578 |
#86 := (forall (vars (?x1 T2)) #83)
|
|
2579 |
#153 := (iff #86 #150)
|
|
2580 |
#151 := (iff #83 #83)
|
|
2581 |
#152 := [refl]: #151
|
|
2582 |
#154 := [quant-intro #152]: #153
|
|
2583 |
#55 := (and #47 #52)
|
|
2584 |
#58 := (forall (vars (?x1 T2)) #55)
|
|
2585 |
#87 := (iff #58 #86)
|
|
2586 |
#84 := (iff #55 #83)
|
|
2587 |
#85 := [rewrite]: #84
|
|
2588 |
#88 := [quant-intro #85]: #87
|
|
2589 |
#79 := (~ #58 #58)
|
|
2590 |
#81 := (~ #55 #55)
|
|
2591 |
#82 := [refl]: #81
|
|
2592 |
#80 := [nnf-pos #82]: #79
|
|
2593 |
#16 := (<= #13 #15)
|
|
2594 |
#14 := (<= #11 #13)
|
|
2595 |
#17 := (and #14 #16)
|
|
2596 |
#18 := (forall (vars (?x1 T2)) #17)
|
|
2597 |
#59 := (iff #18 #58)
|
|
2598 |
#56 := (iff #17 #55)
|
|
2599 |
#53 := (iff #16 #52)
|
|
2600 |
#54 := [rewrite]: #53
|
|
2601 |
#48 := (iff #14 #47)
|
|
2602 |
#49 := [rewrite]: #48
|
|
2603 |
#57 := [monotonicity #49 #54]: #56
|
|
2604 |
#60 := [quant-intro #57]: #59
|
|
2605 |
#41 := [asserted]: #18
|
|
2606 |
#61 := [mp #41 #60]: #58
|
|
2607 |
#77 := [mp~ #61 #80]: #58
|
|
2608 |
#89 := [mp #77 #88]: #86
|
|
2609 |
#155 := [mp #89 #154]: #150
|
|
2610 |
#187 := (not #150)
|
|
2611 |
#188 := (or #187 #184)
|
|
2612 |
#157 := (+ #22 #156)
|
|
2613 |
#158 := (<= #157 0::real)
|
|
2614 |
#159 := (not #158)
|
|
2615 |
#164 := (or #163 #159)
|
|
2616 |
#165 := (not #164)
|
|
2617 |
#189 := (or #187 #165)
|
|
2618 |
#191 := (iff #189 #188)
|
|
2619 |
#193 := (iff #188 #188)
|
|
2620 |
#194 := [rewrite]: #193
|
|
2621 |
#185 := (iff #165 #184)
|
|
2622 |
#182 := (iff #164 #181)
|
|
2623 |
#179 := (iff #159 #178)
|
|
2624 |
#176 := (iff #158 #173)
|
|
2625 |
#166 := (+ #156 #22)
|
|
2626 |
#169 := (<= #166 0::real)
|
|
2627 |
#174 := (iff #169 #173)
|
|
2628 |
#175 := [rewrite]: #174
|
|
2629 |
#170 := (iff #158 #169)
|
|
2630 |
#167 := (= #157 #166)
|
|
2631 |
#168 := [rewrite]: #167
|
|
2632 |
#171 := [monotonicity #168]: #170
|
|
2633 |
#177 := [trans #171 #175]: #176
|
|
2634 |
#180 := [monotonicity #177]: #179
|
|
2635 |
#183 := [monotonicity #180]: #182
|
|
2636 |
#186 := [monotonicity #183]: #185
|
|
2637 |
#192 := [monotonicity #186]: #191
|
|
2638 |
#195 := [trans #192 #194]: #191
|
|
2639 |
#190 := [quant-inst]: #189
|
|
2640 |
#196 := [mp #190 #195]: #188
|
|
2641 |
#220 := [unit-resolution #196 #155]: #184
|
|
2642 |
#197 := (or #181 #162)
|
|
2643 |
#198 := [def-axiom]: #197
|
|
2644 |
#221 := [unit-resolution #198 #220]: #162
|
|
2645 |
#223 := (or #206 #163 #222)
|
|
2646 |
#224 := [th-lemma]: #223
|
|
2647 |
#226 := [unit-resolution #224 #221]: #225
|
|
2648 |
#227 := [unit-resolution #226 #219]: #222
|
|
2649 |
#199 := (or #181 #173)
|
|
2650 |
#200 := [def-axiom]: #199
|
|
2651 |
#228 := [unit-resolution #200 #220]: #173
|
|
2652 |
[th-lemma #228 #227 #211]: false
|
|
2653 |
unsat
|
|
2654 |
rbrrQuQfaijtLkQizgEXnQ 222 0
|
|
2655 |
#2 := false
|
|
2656 |
#4 := 0::real
|
|
2657 |
decl uf_2 :: (-> T2 T1 real)
|
|
2658 |
decl uf_5 :: T1
|
|
2659 |
#15 := uf_5
|
|
2660 |
decl uf_3 :: T2
|
|
2661 |
#7 := uf_3
|
|
2662 |
#20 := (uf_2 uf_3 uf_5)
|
|
2663 |
decl uf_6 :: T2
|
|
2664 |
#17 := uf_6
|
|
2665 |
#18 := (uf_2 uf_6 uf_5)
|
|
2666 |
#59 := -1::real
|
|
2667 |
#73 := (* -1::real #18)
|
|
2668 |
#106 := (+ #73 #20)
|
|
2669 |
decl uf_1 :: real
|
|
2670 |
#5 := uf_1
|
|
2671 |
#78 := (* -1::real #20)
|
|
2672 |
#79 := (+ #18 #78)
|
|
2673 |
#144 := (+ uf_1 #79)
|
|
2674 |
#145 := (<= #144 0::real)
|
|
2675 |
#148 := (ite #145 uf_1 #106)
|
|
2676 |
#279 := (* -1::real #148)
|
|
2677 |
#280 := (+ uf_1 #279)
|
|
2678 |
#281 := (<= #280 0::real)
|
|
2679 |
#289 := (not #281)
|
|
2680 |
#72 := 1/2::real
|
|
2681 |
#151 := (* 1/2::real #148)
|
|
2682 |
#248 := (<= #151 0::real)
|
|
2683 |
#162 := (= #151 0::real)
|
|
2684 |
#24 := 2::real
|
|
2685 |
#27 := (- #20 #18)
|
|
2686 |
#28 := (<= uf_1 #27)
|
|
2687 |
#29 := (ite #28 uf_1 #27)
|
|
2688 |
#30 := (/ #29 2::real)
|
|
2689 |
#31 := (+ #18 #30)
|
|
2690 |
#32 := (= #31 #18)
|
|
2691 |
#33 := (not #32)
|
|
2692 |
#34 := (not #33)
|
|
2693 |
#165 := (iff #34 #162)
|
|
2694 |
#109 := (<= uf_1 #106)
|
|
2695 |
#112 := (ite #109 uf_1 #106)
|
|
2696 |
#118 := (* 1/2::real #112)
|
|
2697 |
#123 := (+ #18 #118)
|
|
2698 |
#129 := (= #18 #123)
|
|
2699 |
#163 := (iff #129 #162)
|
|
2700 |
#154 := (+ #18 #151)
|
|
2701 |
#157 := (= #18 #154)
|
|
2702 |
#160 := (iff #157 #162)
|
|
2703 |
#161 := [rewrite]: #160
|
|
2704 |
#158 := (iff #129 #157)
|
|
2705 |
#155 := (= #123 #154)
|
|
2706 |
#152 := (= #118 #151)
|
|
2707 |
#149 := (= #112 #148)
|
|
2708 |
#146 := (iff #109 #145)
|
|
2709 |
#147 := [rewrite]: #146
|
|
2710 |
#150 := [monotonicity #147]: #149
|
|
2711 |
#153 := [monotonicity #150]: #152
|
|
2712 |
#156 := [monotonicity #153]: #155
|
|
2713 |
#159 := [monotonicity #156]: #158
|
|
2714 |
#164 := [trans #159 #161]: #163
|
|
2715 |
#142 := (iff #34 #129)
|
|
2716 |
#134 := (not #129)
|
|
2717 |
#137 := (not #134)
|
|
2718 |
#140 := (iff #137 #129)
|
|
2719 |
#141 := [rewrite]: #140
|
|
2720 |
#138 := (iff #34 #137)
|
|
2721 |
#135 := (iff #33 #134)
|
|
2722 |
#132 := (iff #32 #129)
|
|
2723 |
#126 := (= #123 #18)
|
|
2724 |
#130 := (iff #126 #129)
|
|
2725 |
#131 := [rewrite]: #130
|
|
2726 |
#127 := (iff #32 #126)
|
|
2727 |
#124 := (= #31 #123)
|
|
2728 |
#121 := (= #30 #118)
|
|
2729 |
#115 := (/ #112 2::real)
|
|
2730 |
#119 := (= #115 #118)
|
|
2731 |
#120 := [rewrite]: #119
|
|
2732 |
#116 := (= #30 #115)
|
|
2733 |
#113 := (= #29 #112)
|
|
2734 |
#107 := (= #27 #106)
|
|
2735 |
#108 := [rewrite]: #107
|
|
2736 |
#110 := (iff #28 #109)
|
|
2737 |
#111 := [monotonicity #108]: #110
|
|
2738 |
#114 := [monotonicity #111 #108]: #113
|
|
2739 |
#117 := [monotonicity #114]: #116
|
|
2740 |
#122 := [trans #117 #120]: #121
|
|
2741 |
#125 := [monotonicity #122]: #124
|
|
2742 |
#128 := [monotonicity #125]: #127
|
|
2743 |
#133 := [trans #128 #131]: #132
|
|
2744 |
#136 := [monotonicity #133]: #135
|
|
2745 |
#139 := [monotonicity #136]: #138
|
|
2746 |
#143 := [trans #139 #141]: #142
|
|
2747 |
#166 := [trans #143 #164]: #165
|
|
2748 |
#105 := [asserted]: #34
|
|
2749 |
#167 := [mp #105 #166]: #162
|
|
2750 |
#283 := (not #162)
|
|
2751 |
#284 := (or #283 #248)
|
|
2752 |
#285 := [th-lemma]: #284
|
|
2753 |
#286 := [unit-resolution #285 #167]: #248
|
|
2754 |
#287 := [hypothesis]: #281
|
|
2755 |
#53 := (<= uf_1 0::real)
|
|
2756 |
#54 := (not #53)
|
|
2757 |
#6 := (< 0::real uf_1)
|
|
2758 |
#55 := (iff #6 #54)
|
|
2759 |
#56 := [rewrite]: #55
|
|
2760 |
#50 := [asserted]: #6
|
|
2761 |
#57 := [mp #50 #56]: #54
|
|
2762 |
#288 := [th-lemma #57 #287 #286]: false
|
|
2763 |
#290 := [lemma #288]: #289
|
|
2764 |
#241 := (= uf_1 #148)
|
|
2765 |
#242 := (= #106 #148)
|
|
2766 |
#299 := (not #242)
|
|
2767 |
#282 := (+ #106 #279)
|
|
2768 |
#291 := (<= #282 0::real)
|
|
2769 |
#296 := (not #291)
|
|
2770 |
decl uf_4 :: T2
|
|
2771 |
#10 := uf_4
|
|
2772 |
#16 := (uf_2 uf_4 uf_5)
|
|
2773 |
#260 := (+ #16 #78)
|
|
2774 |
#261 := (>= #260 0::real)
|
|
2775 |
#266 := (not #261)
|
|
2776 |
#8 := (:var 0 T1)
|
|
2777 |
#11 := (uf_2 uf_4 #8)
|
|
2778 |
#234 := (pattern #11)
|
|
2779 |
#9 := (uf_2 uf_3 #8)
|
|
2780 |
#233 := (pattern #9)
|
|
2781 |
#60 := (* -1::real #11)
|
|
2782 |
#61 := (+ #9 #60)
|
|
2783 |
#62 := (<= #61 0::real)
|
|
2784 |
#179 := (not #62)
|
|
2785 |
#235 := (forall (vars (?x1 T1)) (:pat #233 #234) #179)
|
|
2786 |
#178 := (forall (vars (?x1 T1)) #179)
|
|
2787 |
#238 := (iff #178 #235)
|
|
2788 |
#236 := (iff #179 #179)
|
|
2789 |
#237 := [refl]: #236
|
|
2790 |
#239 := [quant-intro #237]: #238
|
|
2791 |
#65 := (exists (vars (?x1 T1)) #62)
|
|
2792 |
#68 := (not #65)
|
|
2793 |
#175 := (~ #68 #178)
|
|
2794 |
#180 := (~ #179 #179)
|
|
2795 |
#177 := [refl]: #180
|
|
2796 |
#176 := [nnf-neg #177]: #175
|
|
2797 |
#12 := (<= #9 #11)
|
|
2798 |
#13 := (exists (vars (?x1 T1)) #12)
|
|
2799 |
#14 := (not #13)
|
|
2800 |
#69 := (iff #14 #68)
|
|
2801 |
#66 := (iff #13 #65)
|
|
2802 |
#63 := (iff #12 #62)
|
|
2803 |
#64 := [rewrite]: #63
|
|
2804 |
#67 := [quant-intro #64]: #66
|
|
2805 |
#70 := [monotonicity #67]: #69
|
|
2806 |
#51 := [asserted]: #14
|
|
2807 |
#71 := [mp #51 #70]: #68
|
|
2808 |
#173 := [mp~ #71 #176]: #178
|
|
2809 |
#240 := [mp #173 #239]: #235
|
|
2810 |
#269 := (not #235)
|
|
2811 |
#270 := (or #269 #266)
|
|
2812 |
#250 := (* -1::real #16)
|
|
2813 |
#251 := (+ #20 #250)
|
|
2814 |
#252 := (<= #251 0::real)
|
|
2815 |
#253 := (not #252)
|
|
2816 |
#271 := (or #269 #253)
|
|
2817 |
#273 := (iff #271 #270)
|
|
2818 |
#275 := (iff #270 #270)
|
|
2819 |
#276 := [rewrite]: #275
|
|
2820 |
#267 := (iff #253 #266)
|
|
2821 |
#264 := (iff #252 #261)
|
|
2822 |
#254 := (+ #250 #20)
|
|
2823 |
#257 := (<= #254 0::real)
|
|
2824 |
#262 := (iff #257 #261)
|
|
2825 |
#263 := [rewrite]: #262
|
|
2826 |
#258 := (iff #252 #257)
|
|
2827 |
#255 := (= #251 #254)
|
|
2828 |
#256 := [rewrite]: #255
|
|
2829 |
#259 := [monotonicity #256]: #258
|
|
2830 |
#265 := [trans #259 #263]: #264
|
|
2831 |
#268 := [monotonicity #265]: #267
|
|
2832 |
#274 := [monotonicity #268]: #273
|
|
2833 |
#277 := [trans #274 #276]: #273
|
|
2834 |
#272 := [quant-inst]: #271
|
|
2835 |
#278 := [mp #272 #277]: #270
|
|
2836 |
#293 := [unit-resolution #278 #240]: #266
|
|
2837 |
#90 := (* 1/2::real #20)
|
|
2838 |
#102 := (+ #73 #90)
|
|
2839 |
#89 := (* 1/2::real #16)
|
|
2840 |
#103 := (+ #89 #102)
|
|
2841 |
#100 := (>= #103 0::real)
|
|
2842 |
#23 := (+ #16 #20)
|
|
2843 |
#25 := (/ #23 2::real)
|
|
2844 |
#26 := (<= #18 #25)
|
|
2845 |
#98 := (iff #26 #100)
|
|
2846 |
#91 := (+ #89 #90)
|
|
2847 |
#94 := (<= #18 #91)
|
|
2848 |
#97 := (iff #94 #100)
|
|
2849 |
#99 := [rewrite]: #97
|
|
2850 |
#95 := (iff #26 #94)
|
|
2851 |
#92 := (= #25 #91)
|
|
2852 |
#93 := [rewrite]: #92
|
|
2853 |
#96 := [monotonicity #93]: #95
|
|
2854 |
#101 := [trans #96 #99]: #98
|
|
2855 |
#58 := [asserted]: #26
|
|
2856 |
#104 := [mp #58 #101]: #100
|
|
2857 |
#294 := [hypothesis]: #291
|
|
2858 |
#295 := [th-lemma #294 #104 #293 #286]: false
|
|
2859 |
#297 := [lemma #295]: #296
|
|
2860 |
#298 := [hypothesis]: #242
|
|
2861 |
#300 := (or #299 #291)
|
|
2862 |
#301 := [th-lemma]: #300
|
|
2863 |
#302 := [unit-resolution #301 #298 #297]: false
|
|
2864 |
#303 := [lemma #302]: #299
|
|
2865 |
#246 := (or #145 #242)
|
|
2866 |
#247 := [def-axiom]: #246
|
|
2867 |
#304 := [unit-resolution #247 #303]: #145
|
|
2868 |
#243 := (not #145)
|
|
2869 |
#244 := (or #243 #241)
|
|
2870 |
#245 := [def-axiom]: #244
|
|
2871 |
#305 := [unit-resolution #245 #304]: #241
|
|
2872 |
#306 := (not #241)
|
|
2873 |
#307 := (or #306 #281)
|
|
2874 |
#308 := [th-lemma]: #307
|
|
2875 |
[unit-resolution #308 #305 #290]: false
|
|
2876 |
unsat
|
|
2877 |
hwh3oeLAWt56hnKIa8Wuow 248 0
|
|
2878 |
#2 := false
|
|
2879 |
#4 := 0::real
|
|
2880 |
decl uf_2 :: (-> T2 T1 real)
|
|
2881 |
decl uf_5 :: T1
|
|
2882 |
#15 := uf_5
|
|
2883 |
decl uf_6 :: T2
|
|
2884 |
#17 := uf_6
|
|
2885 |
#18 := (uf_2 uf_6 uf_5)
|
|
2886 |
decl uf_4 :: T2
|
|
2887 |
#10 := uf_4
|
|
2888 |
#16 := (uf_2 uf_4 uf_5)
|
|
2889 |
#66 := -1::real
|
|
2890 |
#137 := (* -1::real #16)
|
|
2891 |
#138 := (+ #137 #18)
|
|
2892 |
decl uf_1 :: real
|
|
2893 |
#5 := uf_1
|
|
2894 |
#80 := (* -1::real #18)
|
|
2895 |
#81 := (+ #16 #80)
|
|
2896 |
#201 := (+ uf_1 #81)
|
|
2897 |
#202 := (<= #201 0::real)
|
|
2898 |
#205 := (ite #202 uf_1 #138)
|
|
2899 |
#352 := (* -1::real #205)
|
|
2900 |
#353 := (+ uf_1 #352)
|
|
2901 |
#354 := (<= #353 0::real)
|
|
2902 |
#362 := (not #354)
|
|
2903 |
#79 := 1/2::real
|
|
2904 |
#244 := (* 1/2::real #205)
|
|
2905 |
#322 := (<= #244 0::real)
|
|
2906 |
#245 := (= #244 0::real)
|
|
2907 |
#158 := -1/2::real
|
|
2908 |
#208 := (* -1/2::real #205)
|
|
2909 |
#211 := (+ #18 #208)
|
|
2910 |
decl uf_3 :: T2
|
|
2911 |
#7 := uf_3
|
|
2912 |
#20 := (uf_2 uf_3 uf_5)
|
|
2913 |
#117 := (+ #80 #20)
|
|
2914 |
#85 := (* -1::real #20)
|
|
2915 |
#86 := (+ #18 #85)
|
|
2916 |
#188 := (+ uf_1 #86)
|
|
2917 |
#189 := (<= #188 0::real)
|
|
2918 |
#192 := (ite #189 uf_1 #117)
|
|
2919 |
#195 := (* 1/2::real #192)
|
|
2920 |
#198 := (+ #18 #195)
|
|
2921 |
#97 := (* 1/2::real #20)
|
|
2922 |
#109 := (+ #80 #97)
|
|
2923 |
#96 := (* 1/2::real #16)
|
|
2924 |
#110 := (+ #96 #109)
|
|
2925 |
#107 := (>= #110 0::real)
|
|
2926 |
#214 := (ite #107 #198 #211)
|
|
2927 |
#217 := (= #18 #214)
|
|
2928 |
#248 := (iff #217 #245)
|
|
2929 |
#241 := (= #18 #211)
|
|
2930 |
#246 := (iff #241 #245)
|
|
2931 |
#247 := [rewrite]: #246
|
|
2932 |
#242 := (iff #217 #241)
|
|
2933 |
#239 := (= #214 #211)
|
|
2934 |
#234 := (ite false #198 #211)
|
|
2935 |
#237 := (= #234 #211)
|
|
2936 |
#238 := [rewrite]: #237
|
|
2937 |
#235 := (= #214 #234)
|
|
2938 |
#232 := (iff #107 false)
|
|
2939 |
#104 := (not #107)
|
|
2940 |
#24 := 2::real
|
|
2941 |
#23 := (+ #16 #20)
|
|
2942 |
#25 := (/ #23 2::real)
|
|
2943 |
#26 := (< #25 #18)
|
|
2944 |
#108 := (iff #26 #104)
|
|
2945 |
#98 := (+ #96 #97)
|
|
2946 |
#101 := (< #98 #18)
|
|
2947 |
#106 := (iff #101 #104)
|
|
2948 |
#105 := [rewrite]: #106
|
|
2949 |
#102 := (iff #26 #101)
|
|
2950 |
#99 := (= #25 #98)
|
|
2951 |
#100 := [rewrite]: #99
|
|
2952 |
#103 := [monotonicity #100]: #102
|
|
2953 |
#111 := [trans #103 #105]: #108
|
|
2954 |
#65 := [asserted]: #26
|
|
2955 |
#112 := [mp #65 #111]: #104
|
|
2956 |
#233 := [iff-false #112]: #232
|
|
2957 |
#236 := [monotonicity #233]: #235
|
|
2958 |
#240 := [trans #236 #238]: #239
|
|
2959 |
#243 := [monotonicity #240]: #242
|
|
2960 |
#249 := [trans #243 #247]: #248
|
|
2961 |
#33 := (- #18 #16)
|
|
2962 |
#34 := (<= uf_1 #33)
|
|
2963 |
#35 := (ite #34 uf_1 #33)
|
|
2964 |
#36 := (/ #35 2::real)
|
|
2965 |
#37 := (- #18 #36)
|
|
2966 |
#28 := (- #20 #18)
|
|
2967 |
#29 := (<= uf_1 #28)
|
|
2968 |
#30 := (ite #29 uf_1 #28)
|
|
2969 |
#31 := (/ #30 2::real)
|
|
2970 |
#32 := (+ #18 #31)
|
|
2971 |
#27 := (<= #18 #25)
|
|
2972 |
#38 := (ite #27 #32 #37)
|
|
2973 |
#39 := (= #38 #18)
|
|
2974 |
#40 := (not #39)
|
|
2975 |
#41 := (not #40)
|
|
2976 |
#220 := (iff #41 #217)
|
|
2977 |
#141 := (<= uf_1 #138)
|
|
2978 |
#144 := (ite #141 uf_1 #138)
|
|
2979 |
#159 := (* -1/2::real #144)
|
|
2980 |
#160 := (+ #18 #159)
|
|
2981 |
#120 := (<= uf_1 #117)
|
|
2982 |
#123 := (ite #120 uf_1 #117)
|
|
2983 |
#129 := (* 1/2::real #123)
|
|
2984 |
#134 := (+ #18 #129)
|
|
2985 |
#114 := (<= #18 #98)
|
|
2986 |
#165 := (ite #114 #134 #160)
|
|
2987 |
#171 := (= #18 #165)
|
|
2988 |
#218 := (iff #171 #217)
|
|
2989 |
#215 := (= #165 #214)
|
|
2990 |
#212 := (= #160 #211)
|
|
2991 |
#209 := (= #159 #208)
|
|
2992 |
#206 := (= #144 #205)
|
|
2993 |
#203 := (iff #141 #202)
|
|
2994 |
#204 := [rewrite]: #203
|
|
2995 |
#207 := [monotonicity #204]: #206
|
|
2996 |
#210 := [monotonicity #207]: #209
|
|
2997 |
#213 := [monotonicity #210]: #212
|
|
2998 |
#199 := (= #134 #198)
|
|
2999 |
#196 := (= #129 #195)
|
|
3000 |
#193 := (= #123 #192)
|
|
3001 |
#190 := (iff #120 #189)
|
|
3002 |
#191 := [rewrite]: #190
|
|
3003 |
#194 := [monotonicity #191]: #193
|
|
3004 |
#197 := [monotonicity #194]: #196
|
|
3005 |
#200 := [monotonicity #197]: #199
|
|
3006 |
#187 := (iff #114 #107)
|
|
3007 |
#186 := [rewrite]: #187
|
|
3008 |
#216 := [monotonicity #186 #200 #213]: #215
|
|
3009 |
#219 := [monotonicity #216]: #218
|
|
3010 |
#184 := (iff #41 #171)
|
|
3011 |
#176 := (not #171)
|
|
3012 |
#179 := (not #176)
|
|
3013 |
#182 := (iff #179 #171)
|
|
3014 |
#183 := [rewrite]: #182
|
|
3015 |
#180 := (iff #41 #179)
|
|
3016 |
#177 := (iff #40 #176)
|
|
3017 |
#174 := (iff #39 #171)
|
|
3018 |
#168 := (= #165 #18)
|
|
3019 |
#172 := (iff #168 #171)
|
|
3020 |
#173 := [rewrite]: #172
|
|
3021 |
#169 := (iff #39 #168)
|
|
3022 |
#166 := (= #38 #165)
|
|
3023 |
#163 := (= #37 #160)
|
|
3024 |
#150 := (* 1/2::real #144)
|
|
3025 |
#155 := (- #18 #150)
|
|
3026 |
#161 := (= #155 #160)
|
|
3027 |
#162 := [rewrite]: #161
|
|
3028 |
#156 := (= #37 #155)
|
|
3029 |
#153 := (= #36 #150)
|
|
3030 |
#147 := (/ #144 2::real)
|
|
3031 |
#151 := (= #147 #150)
|
|
3032 |
#152 := [rewrite]: #151
|
|
3033 |
#148 := (= #36 #147)
|
|
3034 |
#145 := (= #35 #144)
|
|
3035 |
#139 := (= #33 #138)
|
|
3036 |
#140 := [rewrite]: #139
|
|
3037 |
#142 := (iff #34 #141)
|
|
3038 |
#143 := [monotonicity #140]: #142
|
|
3039 |
#146 := [monotonicity #143 #140]: #145
|
|
3040 |
#149 := [monotonicity #146]: #148
|
|
3041 |
#154 := [trans #149 #152]: #153
|
|
3042 |
#157 := [monotonicity #154]: #156
|
|
3043 |
#164 := [trans #157 #162]: #163
|
|
3044 |
#135 := (= #32 #134)
|
|
3045 |
#132 := (= #31 #129)
|
|
3046 |
#126 := (/ #123 2::real)
|
|
3047 |
#130 := (= #126 #129)
|
|
3048 |
#131 := [rewrite]: #130
|
|
3049 |
#127 := (= #31 #126)
|
|
3050 |
#124 := (= #30 #123)
|
|
3051 |
#118 := (= #28 #117)
|
|
3052 |
#119 := [rewrite]: #118
|
|
3053 |
#121 := (iff #29 #120)
|
|
3054 |
#122 := [monotonicity #119]: #121
|
|
3055 |
#125 := [monotonicity #122 #119]: #124
|
|
3056 |
#128 := [monotonicity #125]: #127
|
|
3057 |
#133 := [trans #128 #131]: #132
|
|
3058 |
#136 := [monotonicity #133]: #135
|
|
3059 |
#115 := (iff #27 #114)
|
|
3060 |
#116 := [monotonicity #100]: #115
|
|
3061 |
#167 := [monotonicity #116 #136 #164]: #166
|
|
3062 |
#170 := [monotonicity #167]: #169
|
|
3063 |
#175 := [trans #170 #173]: #174
|
|
3064 |
#178 := [monotonicity #175]: #177
|
|
3065 |
#181 := [monotonicity #178]: #180
|
|
3066 |
#185 := [trans #181 #183]: #184
|
|
3067 |
#221 := [trans #185 #219]: #220
|
|
3068 |
#113 := [asserted]: #41
|
|
3069 |
#222 := [mp #113 #221]: #217
|
|
3070 |
#250 := [mp #222 #249]: #245
|
|
3071 |
#356 := (not #245)
|
|
3072 |
#357 := (or #356 #322)
|
|
3073 |
#358 := [th-lemma]: #357
|
|
3074 |
#359 := [unit-resolution #358 #250]: #322
|
|
3075 |
#360 := [hypothesis]: #354
|
|
3076 |
#60 := (<= uf_1 0::real)
|
|
3077 |
#61 := (not #60)
|
|
3078 |
#6 := (< 0::real uf_1)
|
|
3079 |
#62 := (iff #6 #61)
|
|
3080 |
#63 := [rewrite]: #62
|
|
3081 |
#57 := [asserted]: #6
|
|
3082 |
#64 := [mp #57 #63]: #61
|
|
3083 |
#361 := [th-lemma #64 #360 #359]: false
|
|
3084 |
#363 := [lemma #361]: #362
|
|
3085 |
#315 := (= uf_1 #205)
|
|
3086 |
#316 := (= #138 #205)
|
|
3087 |
#371 := (not #316)
|
|
3088 |
#355 := (+ #138 #352)
|
|
3089 |
#364 := (<= #355 0::real)
|
|
3090 |
#368 := (not #364)
|
|
3091 |
#87 := (<= #86 0::real)
|
|
3092 |
#82 := (<= #81 0::real)
|
|
3093 |
#90 := (and #82 #87)
|
|
3094 |
#21 := (<= #18 #20)
|
|
3095 |
#19 := (<= #16 #18)
|
|
3096 |
#22 := (and #19 #21)
|
|
3097 |
#91 := (iff #22 #90)
|
|
3098 |
#88 := (iff #21 #87)
|
|
3099 |
#89 := [rewrite]: #88
|
|
3100 |
#83 := (iff #19 #82)
|
|
3101 |
#84 := [rewrite]: #83
|
|
3102 |
#92 := [monotonicity #84 #89]: #91
|
|
3103 |
#59 := [asserted]: #22
|
|
3104 |
#93 := [mp #59 #92]: #90
|
|
3105 |
#95 := [and-elim #93]: #87
|
|
3106 |
#366 := [hypothesis]: #364
|
|
3107 |
#367 := [th-lemma #366 #95 #112 #359]: false
|
|
3108 |
#369 := [lemma #367]: #368
|
|
3109 |
#370 := [hypothesis]: #316
|
|
3110 |
#372 := (or #371 #364)
|
|
3111 |
#373 := [th-lemma]: #372
|
|
3112 |
#374 := [unit-resolution #373 #370 #369]: false
|
|
3113 |
#375 := [lemma #374]: #371
|
|
3114 |
#320 := (or #202 #316)
|
|
3115 |
#321 := [def-axiom]: #320
|
|
3116 |
#376 := [unit-resolution #321 #375]: #202
|
|
3117 |
#317 := (not #202)
|
|
3118 |
#318 := (or #317 #315)
|
|
3119 |
#319 := [def-axiom]: #318
|
|
3120 |
#377 := [unit-resolution #319 #376]: #315
|
|
3121 |
#378 := (not #315)
|
|
3122 |
#379 := (or #378 #354)
|
|
3123 |
#380 := [th-lemma]: #379
|
|
3124 |
[unit-resolution #380 #377 #363]: false
|
|
3125 |
unsat
|
|
3126 |
WdMJH3tkMv/rps8y9Ukq5Q 86 0
|
|
3127 |
#2 := false
|
|
3128 |
#37 := 0::real
|
|
3129 |
decl uf_2 :: (-> T2 T1 real)
|
|
3130 |
decl uf_4 :: T1
|
|
3131 |
#12 := uf_4
|
|
3132 |
decl uf_3 :: T2
|
|
3133 |
#5 := uf_3
|
|
3134 |
#13 := (uf_2 uf_3 uf_4)
|
|
3135 |
#34 := -1::real
|
|
3136 |
#140 := (* -1::real #13)
|
|
3137 |
decl uf_1 :: real
|
|
3138 |
#4 := uf_1
|
|
3139 |
#141 := (+ uf_1 #140)
|
|
3140 |
#143 := (>= #141 0::real)
|
|
3141 |
#6 := (:var 0 T1)
|
|
3142 |
#7 := (uf_2 uf_3 #6)
|
|
3143 |
#127 := (pattern #7)
|
|
3144 |
#35 := (* -1::real #7)
|
|
3145 |
#36 := (+ uf_1 #35)
|
|
3146 |
#47 := (>= #36 0::real)
|
|
3147 |
#134 := (forall (vars (?x2 T1)) (:pat #127) #47)
|
|
3148 |
#49 := (forall (vars (?x2 T1)) #47)
|
|
3149 |
#137 := (iff #49 #134)
|
|
3150 |
#135 := (iff #47 #47)
|
|
3151 |
#136 := [refl]: #135
|
|
3152 |
#138 := [quant-intro #136]: #137
|
|
3153 |
#67 := (~ #49 #49)
|
|
3154 |
#58 := (~ #47 #47)
|
|
3155 |
#66 := [refl]: #58
|
|
3156 |
#68 := [nnf-pos #66]: #67
|
|
3157 |
#10 := (<= #7 uf_1)
|
|
3158 |
#11 := (forall (vars (?x2 T1)) #10)
|
|
3159 |
#50 := (iff #11 #49)
|
|
3160 |
#46 := (iff #10 #47)
|
|
3161 |
#48 := [rewrite]: #46
|
|
3162 |
#51 := [quant-intro #48]: #50
|
|
3163 |
#32 := [asserted]: #11
|
|
3164 |
#52 := [mp #32 #51]: #49
|
|
3165 |
#69 := [mp~ #52 #68]: #49
|
|
3166 |
#139 := [mp #69 #138]: #134
|
|
3167 |
#149 := (not #134)
|
|
3168 |
#150 := (or #149 #143)
|
|
3169 |
#151 := [quant-inst]: #150
|
|
3170 |
#144 := [unit-resolution #151 #139]: #143
|
|
3171 |
#142 := (<= #141 0::real)
|
|
3172 |
#38 := (<= #36 0::real)
|
|
3173 |
#128 := (forall (vars (?x1 T1)) (:pat #127) #38)
|
|
3174 |
#41 := (forall (vars (?x1 T1)) #38)
|
|
3175 |
#131 := (iff #41 #128)
|
|
3176 |
#129 := (iff #38 #38)
|
|
3177 |
#130 := [refl]: #129
|
|
3178 |
#132 := [quant-intro #130]: #131
|
|
3179 |
#62 := (~ #41 #41)
|
|
3180 |
#64 := (~ #38 #38)
|
|
3181 |
#65 := [refl]: #64
|
|
3182 |
#63 := [nnf-pos #65]: #62
|
|
3183 |
#8 := (<= uf_1 #7)
|
|
3184 |
#9 := (forall (vars (?x1 T1)) #8)
|
|
3185 |
#42 := (iff #9 #41)
|
|
3186 |
#39 := (iff #8 #38)
|
|
3187 |
#40 := [rewrite]: #39
|
|
3188 |
#43 := [quant-intro #40]: #42
|
|
3189 |
#31 := [asserted]: #9
|
|
3190 |
#44 := [mp #31 #43]: #41
|
|
3191 |
#61 := [mp~ #44 #63]: #41
|
|
3192 |
#133 := [mp #61 #132]: #128
|
|
3193 |
#145 := (not #128)
|
|
3194 |
#146 := (or #145 #142)
|
|
3195 |
#147 := [quant-inst]: #146
|
|
3196 |
#148 := [unit-resolution #147 #133]: #142
|
|
3197 |
#45 := (= uf_1 #13)
|
|
3198 |
#55 := (not #45)
|
|
3199 |
#14 := (= #13 uf_1)
|
|
3200 |
#15 := (not #14)
|
|
3201 |
#56 := (iff #15 #55)
|
|
3202 |
#53 := (iff #14 #45)
|
|
3203 |
#54 := [rewrite]: #53
|
|
3204 |
#57 := [monotonicity #54]: #56
|
|
3205 |
#33 := [asserted]: #15
|
|
3206 |
#60 := [mp #33 #57]: #55
|
|
3207 |
#153 := (not #143)
|
|
3208 |
#152 := (not #142)
|
|
3209 |
#154 := (or #45 #152 #153)
|
|
3210 |
#155 := [th-lemma]: #154
|
|
3211 |
[unit-resolution #155 #60 #148 #144]: false
|
|
3212 |
unsat
|
|
3213 |
V+IAyBZU/6QjYs6JkXx8LQ 57 0
|
|
3214 |
#2 := false
|
|
3215 |
#4 := 0::real
|
|
3216 |
decl uf_1 :: (-> T2 real)
|
|
3217 |
decl uf_2 :: (-> T1 T1 T2)
|
|
3218 |
decl uf_12 :: (-> T4 T1)
|
|
3219 |
decl uf_4 :: T4
|
|
3220 |
#11 := uf_4
|
|
3221 |
#39 := (uf_12 uf_4)
|
|
3222 |
decl uf_10 :: T4
|
|
3223 |
#27 := uf_10
|
|
3224 |
#38 := (uf_12 uf_10)
|
|
3225 |
#40 := (uf_2 #38 #39)
|
|
3226 |
#41 := (uf_1 #40)
|
|
3227 |
#264 := (>= #41 0::real)
|
|
3228 |
#266 := (not #264)
|
|
3229 |
#43 := (= #41 0::real)
|
|
3230 |
#44 := (not #43)
|
|
3231 |
#131 := [asserted]: #44
|
|
3232 |
#272 := (or #43 #266)
|
|
3233 |
#42 := (<= #41 0::real)
|
|
3234 |
#130 := [asserted]: #42
|
|
3235 |
#265 := (not #42)
|
|
3236 |
#270 := (or #43 #265 #266)
|
|
3237 |
#271 := [th-lemma]: #270
|
|
3238 |
#273 := [unit-resolution #271 #130]: #272
|
|
3239 |
#274 := [unit-resolution #273 #131]: #266
|
|
3240 |
#6 := (:var 0 T1)
|
|
3241 |
#5 := (:var 1 T1)
|
|
3242 |
#7 := (uf_2 #5 #6)
|
|
3243 |
#241 := (pattern #7)
|
|
3244 |
#8 := (uf_1 #7)
|
|
3245 |
#65 := (>= #8 0::real)
|
|
3246 |
#242 := (forall (vars (?x1 T1) (?x2 T1)) (:pat #241) #65)
|
|
3247 |
#66 := (forall (vars (?x1 T1) (?x2 T1)) #65)
|
|
3248 |
#245 := (iff #66 #242)
|
|
3249 |
#243 := (iff #65 #65)
|
|
3250 |
#244 := [refl]: #243
|
|
3251 |
#246 := [quant-intro #244]: #245
|
|
3252 |
#149 := (~ #66 #66)
|
|
3253 |
#151 := (~ #65 #65)
|
|
3254 |
#152 := [refl]: #151
|
|
3255 |
#150 := [nnf-pos #152]: #149
|
|
3256 |
#9 := (<= 0::real #8)
|
|
3257 |
#10 := (forall (vars (?x1 T1) (?x2 T1)) #9)
|
|
3258 |
#67 := (iff #10 #66)
|
|
3259 |
#63 := (iff #9 #65)
|
|
3260 |
#64 := [rewrite]: #63
|
|
3261 |
#68 := [quant-intro #64]: #67
|
|
3262 |
#60 := [asserted]: #10
|
|
3263 |
#69 := [mp #60 #68]: #66
|
|
3264 |
#147 := [mp~ #69 #150]: #66
|
|
3265 |
#247 := [mp #147 #246]: #242
|
|
3266 |
#267 := (not #242)
|
|
3267 |
#268 := (or #267 #264)
|
|
3268 |
#269 := [quant-inst]: #268
|
|
3269 |
[unit-resolution #269 #247 #274]: false
|
|
3270 |
unsat
|