src/HOL/Multivariate_Analysis/Integration.certs

non-executable source files;

2e15025784d0676586e79b418a67bcb9811380a1 238 0
#2 := false
#48 := 0::real
decl f19 :: (-> S3 S10 real)
decl f20 :: S10
#43 := f20
decl f4 :: S3
#8 := f4
#58 := (f19 f4 f20)
#109 := -1::real
#153 := (* -1::real #58)
decl f5 :: (-> S4 S5 real)
decl f8 :: S5
#13 := f8
decl f22 :: S4
#54 := f22
#55 := (f5 f22 f8)
#154 := (+ #55 #153)
#137 := (* -1::real #55)
#144 := (+ #137 #58)
#188 := (<= #154 0::real)
#195 := (ite #188 #144 #154)
#451 := (* -1::real #195)
#452 := (+ #144 #451)
#453 := (<= #452 0::real)
#435 := (= #144 #195)
decl f21 :: S4
#45 := f21
#46 := (f5 f21 f8)
decl f9 :: S3
#17 := f9
#44 := (f19 f9 f20)
#120 := (* -1::real #44)
#121 := (+ #120 #46)
#110 := (* -1::real #46)
#111 := (+ #44 #110)
#216 := (>= #111 0::real)
#223 := (ite #216 #111 #121)
#447 := (* -1::real #223)
#450 := (+ #121 #447)
#454 := (<= #450 0::real)
#442 := (= #121 #223)
#217 := (not #216)
#455 := [hypothesis]: #216
#184 := (+ #44 #153)
#185 := (<= #184 0::real)
#206 := -3::real
#234 := (* -3::real #223)
#235 := (+ #137 #234)
#236 := (+ #46 #235)
#237 := (<= #236 0::real)
#238 := (not #237)
#207 := (* -3::real #195)
#208 := (+ #137 #207)
#209 := (+ #46 #208)
#210 := (<= #209 0::real)
#211 := (not #210)
#249 := (and #185 #211 #238)
#65 := (<= #44 #58)
#56 := (- #46 #55)
#52 := 3::real
#59 := (- #58 #55)
#61 := (- #59)
#60 := (< #59 0::real)
#62 := (ite #60 #61 #59)
#63 := (* #62 3::real)
#64 := (< #63 #56)
#66 := (and #64 #65)
#47 := (- #44 #46)
#50 := (- #47)
#49 := (< #47 0::real)
#51 := (ite #49 #50 #47)
#53 := (* #51 3::real)
#57 := (< #53 #56)
#67 := (and #57 #66)
#254 := (iff #67 #249)
#138 := (+ #46 #137)
#147 := (< #144 0::real)
#159 := (ite #147 #154 #144)
#165 := (* 3::real #159)
#170 := (< #165 #138)
#176 := (and #65 #170)
#114 := (< #111 0::real)
#126 := (ite #114 #121 #111)
#132 := (* 3::real #126)
#141 := (< #132 #138)
#181 := (and #141 #176)
#252 := (iff #181 #249)
#243 := (and #185 #211)
#246 := (and #238 #243)
#250 := (iff #246 #249)
#251 := [rewrite]: #250
#247 := (iff #181 #246)
#244 := (iff #176 #243)
#214 := (iff #170 #211)
#200 := (* 3::real #195)
#203 := (< #200 #138)
#212 := (iff #203 #211)
#213 := [rewrite]: #212
#204 := (iff #170 #203)
#201 := (= #165 #200)
#198 := (= #159 #195)
#189 := (not #188)
#192 := (ite #189 #154 #144)
#196 := (= #192 #195)
#197 := [rewrite]: #196
#193 := (= #159 #192)
#190 := (iff #147 #189)
#191 := [rewrite]: #190
#194 := [monotonicity #191]: #193
#199 := [trans #194 #197]: #198
#202 := [monotonicity #199]: #201
#205 := [monotonicity #202]: #204
#215 := [trans #205 #213]: #214
#186 := (iff #65 #185)
#187 := [rewrite]: #186
#245 := [monotonicity #187 #215]: #244
#241 := (iff #141 #238)
#228 := (* 3::real #223)
#231 := (< #228 #138)
#239 := (iff #231 #238)
#240 := [rewrite]: #239
#232 := (iff #141 #231)
#229 := (= #132 #228)
#226 := (= #126 #223)
#220 := (ite #217 #121 #111)
#224 := (= #220 #223)
#225 := [rewrite]: #224
#221 := (= #126 #220)
#218 := (iff #114 #217)
#219 := [rewrite]: #218
#222 := [monotonicity #219]: #221
#227 := [trans #222 #225]: #226
#230 := [monotonicity #227]: #229
#233 := [monotonicity #230]: #232
#242 := [trans #233 #240]: #241
#248 := [monotonicity #242 #245]: #247
#253 := [trans #248 #251]: #252
#182 := (iff #67 #181)
#179 := (iff #66 #176)
#173 := (and #170 #65)
#177 := (iff #173 #176)
#178 := [rewrite]: #177
#174 := (iff #66 #173)
#171 := (iff #64 #170)
#139 := (= #56 #138)
#140 := [rewrite]: #139
#168 := (= #63 #165)
#162 := (* #159 3::real)
#166 := (= #162 #165)
#167 := [rewrite]: #166
#163 := (= #63 #162)
#160 := (= #62 #159)
#145 := (= #59 #144)
#146 := [rewrite]: #145
#157 := (= #61 #154)
#150 := (- #144)
#155 := (= #150 #154)
#156 := [rewrite]: #155
#151 := (= #61 #150)
#152 := [monotonicity #146]: #151
#158 := [trans #152 #156]: #157
#148 := (iff #60 #147)
#149 := [monotonicity #146]: #148
#161 := [monotonicity #149 #158 #146]: #160
#164 := [monotonicity #161]: #163
#169 := [trans #164 #167]: #168
#172 := [monotonicity #169 #140]: #171
#175 := [monotonicity #172]: #174
#180 := [trans #175 #178]: #179
#142 := (iff #57 #141)
#135 := (= #53 #132)
#129 := (* #126 3::real)
#133 := (= #129 #132)
#134 := [rewrite]: #133
#130 := (= #53 #129)
#127 := (= #51 #126)
#112 := (= #47 #111)
#113 := [rewrite]: #112
#124 := (= #50 #121)
#117 := (- #111)
#122 := (= #117 #121)
#123 := [rewrite]: #122
#118 := (= #50 #117)
#119 := [monotonicity #113]: #118
#125 := [trans #119 #123]: #124
#115 := (iff #49 #114)
#116 := [monotonicity #113]: #115
#128 := [monotonicity #116 #125 #113]: #127
#131 := [monotonicity #128]: #130
#136 := [trans #131 #134]: #135
#143 := [monotonicity #136 #140]: #142
#183 := [monotonicity #143 #180]: #182
#255 := [trans #183 #253]: #254
#108 := [asserted]: #67
#256 := [mp #108 #255]: #249
#257 := [and-elim #256]: #185
#259 := [and-elim #256]: #238
#448 := (+ #111 #447)
#449 := (<= #448 0::real)
#441 := (= #111 #223)
#443 := (or #217 #441)
#444 := [def-axiom]: #443
#467 := [unit-resolution #444 #455]: #441
#468 := (not #441)
#469 := (or #468 #449)
#470 := [th-lemma]: #469
#471 := [unit-resolution #470 #467]: #449
#463 := (or #189 #217)
#456 := [hypothesis]: #188
#258 := [and-elim #256]: #211
#437 := (or #189 #435)
#438 := [def-axiom]: #437
#457 := [unit-resolution #438 #456]: #435
#458 := (not #435)
#459 := (or #458 #453)
#460 := [th-lemma]: #459
#461 := [unit-resolution #460 #457]: #453
#462 := [th-lemma #257 #461 #258 #456 #455]: false
#464 := [lemma #462]: #463
#472 := [unit-resolution #464 #455]: #189
#473 := [th-lemma #472 #471 #259 #257 #455]: false
#474 := [lemma #473]: #217
#445 := (or #216 #442)
#446 := [def-axiom]: #445
#475 := [unit-resolution #446 #474]: #442
#476 := (not #442)
#477 := (or #476 #454)
#478 := [th-lemma]: #477
#479 := [unit-resolution #478 #475]: #454
#481 := (not #185)
#480 := (not #454)
#482 := (or #188 #480 #237 #481 #216)
#483 := [th-lemma]: #482
#484 := [unit-resolution #483 #257 #474 #259 #479]: #188
#485 := [unit-resolution #438 #484]: #435
#486 := [unit-resolution #460 #485]: #453
[th-lemma #479 #259 #257 #474 #258 #486]: false
unsat
4c0d1f43a6268b5d3a850361d3ff86d073eaf489 333 0
#2 := false
#11 := 0::real
decl ?v2!1 :: real
#225 := ?v2!1
decl ?v1!2 :: real
#223 := ?v1!2
#45 := -1::real
#238 := (* -1::real ?v1!2)
#260 := (+ #238 ?v2!1)
#240 := (* -1::real ?v2!1)
#266 := (+ ?v1!2 #240)
#267 := (>= #266 0::real)
#274 := (ite #267 #266 #260)
#277 := (* -1::real #274)
#74 := -1/3::real
#233 := (* -1/3::real ?v2!1)
#280 := (+ #233 #277)
decl ?v3!0 :: real
#224 := ?v3!0
#72 := 1/3::real
#235 := (* 1/3::real ?v3!0)
#283 := (+ #235 #280)
#286 := (<= #283 0::real)
#302 := (not #286)
decl ?v0!3 :: real
#221 := ?v0!3
#248 := (+ ?v0!3 #238)
#249 := (<= #248 0::real)
#250 := (not #249)
#226 := (* -1::real ?v0!3)
#227 := (+ #226 ?v3!0)
#228 := (* -1::real ?v3!0)
#229 := (+ ?v0!3 #228)
#230 := (>= #229 0::real)
#231 := (ite #230 #229 #227)
#232 := (* -1::real #231)
#234 := (+ #233 #232)
#236 := (+ #235 #234)
#237 := (<= #236 0::real)
#292 := (or #237 #250 #286)
#297 := (not #292)
#239 := (+ ?v2!1 #238)
#241 := (+ #240 ?v1!2)
#242 := (<= #239 0::real)
#243 := (ite #242 #241 #239)
#244 := (* -1::real #243)
#245 := (+ #233 #244)
#246 := (+ #235 #245)
#247 := (<= #246 0::real)
#251 := (or #250 #247 #237)
#252 := (not #251)
#298 := (iff #252 #297)
#295 := (iff #251 #292)
#289 := (or #250 #286 #237)
#293 := (iff #289 #292)
#294 := [rewrite]: #293
#290 := (iff #251 #289)
#287 := (iff #247 #286)
#284 := (= #246 #283)
#281 := (= #245 #280)
#278 := (= #244 #277)
#275 := (= #243 #274)
#261 := (= #239 #260)
#262 := [rewrite]: #261
#272 := (= #241 #266)
#273 := [rewrite]: #272
#270 := (iff #242 #267)
#263 := (<= #260 0::real)
#268 := (iff #263 #267)
#269 := [rewrite]: #268
#264 := (iff #242 #263)
#265 := [monotonicity #262]: #264
#271 := [trans #265 #269]: #270
#276 := [monotonicity #271 #273 #262]: #275
#279 := [monotonicity #276]: #278
#282 := [monotonicity #279]: #281
#285 := [monotonicity #282]: #284
#288 := [monotonicity #285]: #287
#291 := [monotonicity #288]: #290
#296 := [trans #291 #294]: #295
#299 := [monotonicity #296]: #298
#9 := (:var 0 real)
#8 := (:var 3 real)
#56 := (* -1::real #8)
#57 := (+ #56 #9)
#46 := (* -1::real #9)
#47 := (+ #8 #46)
#170 := (>= #47 0::real)
#177 := (ite #170 #47 #57)
#185 := (* -1::real #177)
#15 := (:var 1 real)
#75 := (* -1/3::real #15)
#186 := (+ #75 #185)
#73 := (* 1/3::real #9)
#187 := (+ #73 #186)
#188 := (<= #187 0::real)
#20 := (:var 2 real)
#93 := (* -1::real #20)
#94 := (+ #15 #93)
#65 := (* -1::real #15)
#84 := (+ #65 #20)
#139 := (<= #94 0::real)
#146 := (ite #139 #84 #94)
#154 := (* -1::real #146)
#155 := (+ #75 #154)
#156 := (+ #73 #155)
#157 := (<= #156 0::real)
#132 := (+ #8 #93)
#133 := (<= #132 0::real)
#136 := (not #133)
#207 := (or #136 #157 #188)
#212 := (forall (vars (?v0 real) (?v1 real) (?v2 real) (?v3 real)) #207)
#215 := (not #212)
#253 := (~ #215 #252)
#254 := [sk]: #253
#26 := (<= #8 #20)
#27 := (implies #26 false)
#17 := 3::real
#16 := (- #9 #15)
#18 := (/ #16 3::real)
#21 := (- #20 #15)
#23 := (- #21)
#22 := (< #21 0::real)
#24 := (ite #22 #23 #21)
#25 := (< #24 #18)
#28 := (implies #25 #27)
#10 := (- #8 #9)
#13 := (- #10)
#12 := (< #10 0::real)
#14 := (ite #12 #13 #10)
#19 := (< #14 #18)
#29 := (implies #19 #28)
#30 := (forall (vars (?v0 real) (?v1 real) (?v2 real) (?v3 real)) #29)
#31 := (not #30)
#218 := (iff #31 #215)
#76 := (+ #73 #75)
#87 := (< #84 0::real)
#99 := (ite #87 #94 #84)
#102 := (< #99 #76)
#111 := (not #102)
#105 := (not #26)
#112 := (or #105 #111)
#50 := (< #47 0::real)
#62 := (ite #50 #57 #47)
#81 := (< #62 #76)
#120 := (not #81)
#121 := (or #120 #112)
#126 := (forall (vars (?v0 real) (?v1 real) (?v2 real) (?v3 real)) #121)
#129 := (not #126)
#216 := (iff #129 #215)
#213 := (iff #126 #212)
#210 := (iff #121 #207)
#201 := (or #136 #157)
#204 := (or #188 #201)
#208 := (iff #204 #207)
#209 := [rewrite]: #208
#205 := (iff #121 #204)
#202 := (iff #112 #201)
#168 := (iff #111 #157)
#158 := (not #157)
#163 := (not #158)
#166 := (iff #163 #157)
#167 := [rewrite]: #166
#164 := (iff #111 #163)
#161 := (iff #102 #158)
#151 := (< #146 #76)
#159 := (iff #151 #158)
#160 := [rewrite]: #159
#152 := (iff #102 #151)
#149 := (= #99 #146)
#140 := (not #139)
#143 := (ite #140 #94 #84)
#147 := (= #143 #146)
#148 := [rewrite]: #147
#144 := (= #99 #143)
#141 := (iff #87 #140)
#142 := [rewrite]: #141
#145 := [monotonicity #142]: #144
#150 := [trans #145 #148]: #149
#153 := [monotonicity #150]: #152
#162 := [trans #153 #160]: #161
#165 := [monotonicity #162]: #164
#169 := [trans #165 #167]: #168
#137 := (iff #105 #136)
#134 := (iff #26 #133)
#135 := [rewrite]: #134
#138 := [monotonicity #135]: #137
#203 := [monotonicity #138 #169]: #202
#199 := (iff #120 #188)
#189 := (not #188)
#194 := (not #189)
#197 := (iff #194 #188)
#198 := [rewrite]: #197
#195 := (iff #120 #194)
#192 := (iff #81 #189)
#182 := (< #177 #76)
#190 := (iff #182 #189)
#191 := [rewrite]: #190
#183 := (iff #81 #182)
#180 := (= #62 #177)
#171 := (not #170)
#174 := (ite #171 #57 #47)
#178 := (= #174 #177)
#179 := [rewrite]: #178
#175 := (= #62 #174)
#172 := (iff #50 #171)
#173 := [rewrite]: #172
#176 := [monotonicity #173]: #175
#181 := [trans #176 #179]: #180
#184 := [monotonicity #181]: #183
#193 := [trans #184 #191]: #192
#196 := [monotonicity #193]: #195
#200 := [trans #196 #198]: #199
#206 := [monotonicity #200 #203]: #205
#211 := [trans #206 #209]: #210
#214 := [quant-intro #211]: #213
#217 := [monotonicity #214]: #216
#130 := (iff #31 #129)
#127 := (iff #30 #126)
#124 := (iff #29 #121)
#117 := (implies #81 #112)
#122 := (iff #117 #121)
#123 := [rewrite]: #122
#118 := (iff #29 #117)
#115 := (iff #28 #112)
#108 := (implies #102 #105)
#113 := (iff #108 #112)
#114 := [rewrite]: #113
#109 := (iff #28 #108)
#106 := (iff #27 #105)
#107 := [rewrite]: #106
#103 := (iff #25 #102)
#79 := (= #18 #76)
#66 := (+ #9 #65)
#69 := (/ #66 3::real)
#77 := (= #69 #76)
#78 := [rewrite]: #77
#70 := (= #18 #69)
#67 := (= #16 #66)
#68 := [rewrite]: #67
#71 := [monotonicity #68]: #70
#80 := [trans #71 #78]: #79
#100 := (= #24 #99)
#85 := (= #21 #84)
#86 := [rewrite]: #85
#97 := (= #23 #94)
#90 := (- #84)
#95 := (= #90 #94)
#96 := [rewrite]: #95
#91 := (= #23 #90)
#92 := [monotonicity #86]: #91
#98 := [trans #92 #96]: #97
#88 := (iff #22 #87)
#89 := [monotonicity #86]: #88
#101 := [monotonicity #89 #98 #86]: #100
#104 := [monotonicity #101 #80]: #103
#110 := [monotonicity #104 #107]: #109
#116 := [trans #110 #114]: #115
#82 := (iff #19 #81)
#63 := (= #14 #62)
#48 := (= #10 #47)
#49 := [rewrite]: #48
#60 := (= #13 #57)
#53 := (- #47)
#58 := (= #53 #57)
#59 := [rewrite]: #58
#54 := (= #13 #53)
#55 := [monotonicity #49]: #54
#61 := [trans #55 #59]: #60
#51 := (iff #12 #50)
#52 := [monotonicity #49]: #51
#64 := [monotonicity #52 #61 #49]: #63
#83 := [monotonicity #64 #80]: #82
#119 := [monotonicity #83 #116]: #118
#125 := [trans #119 #123]: #124
#128 := [quant-intro #125]: #127
#131 := [monotonicity #128]: #130
#219 := [trans #131 #217]: #218
#44 := [asserted]: #31
#220 := [mp #44 #219]: #215
#257 := [mp~ #220 #254]: #252
#258 := [mp #257 #299]: #297
#303 := [not-or-elim #258]: #302
#301 := [not-or-elim #258]: #249
#259 := (not #237)
#300 := [not-or-elim #258]: #259
#376 := (+ #227 #232)
#377 := (<= #376 0::real)
#360 := (= #227 #231)
#361 := (not #230)
#368 := (not #267)
#379 := [hypothesis]: #368
#387 := (or #361 #267)
#373 := (+ #260 #277)
#374 := (<= #373 0::real)
#367 := (= #260 #274)
#371 := (or #267 #367)
#372 := [def-axiom]: #371
#380 := [unit-resolution #372 #379]: #367
#381 := (not #367)
#382 := (or #381 #374)
#383 := [th-lemma]: #382
#384 := [unit-resolution #383 #380]: #374
#385 := [hypothesis]: #230
#386 := [th-lemma #385 #384 #303 #379 #301]: false
#388 := [lemma #386]: #387
#389 := [unit-resolution #388 #379]: #361
#364 := (or #230 #360)
#365 := [def-axiom]: #364
#390 := [unit-resolution #365 #389]: #360
#391 := (not #360)
#392 := (or #391 #377)
#393 := [th-lemma]: #392
#394 := [unit-resolution #393 #390]: #377
#395 := [th-lemma #384 #303 #379 #394 #300 #301]: false
#396 := [lemma #395]: #267
#399 := [hypothesis]: #361
#400 := [unit-resolution #365 #399]: #360
#401 := [unit-resolution #393 #400]: #377
#375 := (+ #266 #277)
#378 := (<= #375 0::real)
#366 := (= #266 #274)
#369 := (or #368 #366)
#370 := [def-axiom]: #369
#402 := [unit-resolution #370 #396]: #366
#403 := (not #366)
#404 := (or #403 #378)
#405 := [th-lemma]: #404
#406 := [unit-resolution #405 #402]: #378
#407 := [th-lemma #406 #301 #401 #300 #399 #303]: false
#408 := [lemma #407]: #230
[th-lemma #406 #301 #408 #396 #303]: false
unsat
40822b724c71d6702c01ad1e865c13dca0ab3c21 57 0
#2 := false
decl f13 :: (-> S4 S4 S5)
#44 := (:var 0 S4)
#43 := (:var 1 S4)
#45 := (f13 #43 #44)
#252 := (pattern #45)
#39 := 0::real
decl f12 :: (-> S5 real)
#46 := (f12 #45)
#133 := (>= #46 0::real)
#253 := (forall (vars (?v0 S4) (?v1 S4)) (:pat #252) #133)
#135 := (forall (vars (?v0 S4) (?v1 S4)) #133)
#256 := (iff #135 #253)
#254 := (iff #133 #133)
#255 := [refl]: #254
#257 := [quant-intro #255]: #256
#150 := (~ #135 #135)
#139 := (~ #133 #133)
#130 := [refl]: #139
#151 := [nnf-pos #130]: #150
#47 := (<= 0::real #46)
#48 := (forall (vars (?v0 S4) (?v1 S4)) #47)
#136 := (iff #48 #135)
#132 := (iff #47 #133)
#134 := [rewrite]: #132
#137 := [quant-intro #134]: #136
#129 := [asserted]: #48
#138 := [mp #129 #137]: #135
#152 := [mp~ #138 #151]: #135
#258 := [mp #152 #257]: #253
decl f14 :: (-> S3 S4)
decl f4 :: S3
#8 := f4
#36 := (f14 f4)
decl f10 :: S3
#24 := f10
#35 := (f14 f10)
#37 := (f13 #35 #36)
#38 := (f12 #37)
#259 := (>= #38 0::real)
#261 := (not #259)
#41 := (= #38 0::real)
#42 := (not #41)
#128 := [asserted]: #42
#267 := (or #41 #261)
#40 := (<= #38 0::real)
#127 := [asserted]: #40
#260 := (not #40)
#265 := (or #41 #260 #261)
#266 := [th-lemma]: #265
#268 := [unit-resolution #266 #127]: #267
#269 := [unit-resolution #268 #128]: #261
#262 := (not #253)
#263 := (or #262 #259)
#264 := [quant-inst]: #263
[unit-resolution #264 #269 #258]: false
unsat
ae79dfdacb760a3554ce388b846d335064f674de 318 0
#2 := false
#25 := 0::real
decl f8 :: (-> S4 S2 real)
decl f11 :: S2
#40 := f11
decl f9 :: S4
#32 := f9
#47 := (f8 f9 f11)
decl f12 :: S4
#44 := f12
#45 := (f8 f12 f11)
#192 := -1::real
#232 := (* -1::real #45)
#233 := (+ #232 #47)
decl f5 :: real
#26 := f5
#268 := (* -1::real #47)
#271 := (+ #45 #268)
#274 := (+ f5 #271)
#275 := (<= #274 0::real)
#278 := (ite #275 f5 #233)
#593 := (* -1::real #278)
#594 := (+ f5 #593)
#595 := (<= #594 0::real)
#603 := (not #595)
#223 := 1/2::real
#281 := (* 1/2::real #278)
#457 := (<= #281 0::real)
#292 := (= #281 0::real)
#306 := (<= #271 0::real)
decl f10 :: S4
#34 := f10
#43 := (f8 f10 f11)
#302 := (+ #43 #232)
#303 := (<= #302 0::real)
#309 := (and #303 #306)
#13 := 0::int
decl f4 :: (-> S2 int)
#41 := (f4 f11)
#178 := -1::int
#213 := (* -1::int #41)
decl f6 :: (-> S3 S2)
decl f7 :: S3
#28 := f7
#29 := (f6 f7)
#30 := (f4 #29)
#214 := (+ #30 #213)
#215 := (<= #214 0::int)
#312 := (or #215 #309)
#225 := (* 1/2::real #47)
#272 := (+ #232 #225)
#224 := (* 1/2::real #43)
#273 := (+ #224 #272)
#270 := (>= #273 0::real)
#321 := (and #270 #292 #312)
#52 := 2::real
#55 := (- #47 #45)
#56 := (<= f5 #55)
#57 := (ite #56 f5 #55)
#58 := (/ #57 2::real)
#59 := (+ #45 #58)
#60 := (= #59 #45)
#51 := (+ #43 #47)
#53 := (/ #51 2::real)
#54 := (<= #45 #53)
#61 := (and #54 #60)
#48 := (<= #45 #47)
#46 := (<= #43 #45)
#49 := (and #46 #48)
#42 := (< #41 #30)
#50 := (implies #42 #49)
#62 := (and #50 #61)
#326 := (iff #62 #321)
#236 := (<= f5 #233)
#239 := (ite #236 f5 #233)
#245 := (* 1/2::real #239)
#250 := (+ #45 #245)
#256 := (= #45 #250)
#226 := (+ #224 #225)
#229 := (<= #45 #226)
#261 := (and #229 #256)
#212 := (not #42)
#220 := (or #212 #49)
#264 := (and #220 #261)
#324 := (iff #264 #321)
#315 := (and #270 #292)
#318 := (and #312 #315)
#322 := (iff #318 #321)
#323 := [rewrite]: #322
#319 := (iff #264 #318)
#316 := (iff #261 #315)
#293 := (iff #256 #292)
#284 := (+ #45 #281)
#287 := (= #45 #284)
#290 := (iff #287 #292)
#291 := [rewrite]: #290
#288 := (iff #256 #287)
#285 := (= #250 #284)
#282 := (= #245 #281)
#279 := (= #239 #278)
#276 := (iff #236 #275)
#277 := [rewrite]: #276
#280 := [monotonicity #277]: #279
#283 := [monotonicity #280]: #282
#286 := [monotonicity #283]: #285
#289 := [monotonicity #286]: #288
#294 := [trans #289 #291]: #293
#267 := (iff #229 #270)
#269 := [rewrite]: #267
#317 := [monotonicity #269 #294]: #316
#313 := (iff #220 #312)
#310 := (iff #49 #309)
#307 := (iff #48 #306)
#308 := [rewrite]: #307
#304 := (iff #46 #303)
#305 := [rewrite]: #304
#311 := [monotonicity #305 #308]: #310
#300 := (iff #212 #215)
#216 := (not #215)
#295 := (not #216)
#298 := (iff #295 #215)
#299 := [rewrite]: #298
#296 := (iff #212 #295)
#217 := (iff #42 #216)
#218 := [rewrite]: #217
#297 := [monotonicity #218]: #296
#301 := [trans #297 #299]: #300
#314 := [monotonicity #301 #311]: #313
#320 := [monotonicity #314 #317]: #319
#325 := [trans #320 #323]: #324
#265 := (iff #62 #264)
#262 := (iff #61 #261)
#259 := (iff #60 #256)
#253 := (= #250 #45)
#257 := (iff #253 #256)
#258 := [rewrite]: #257
#254 := (iff #60 #253)
#251 := (= #59 #250)
#248 := (= #58 #245)
#242 := (/ #239 2::real)
#246 := (= #242 #245)
#247 := [rewrite]: #246
#243 := (= #58 #242)
#240 := (= #57 #239)
#234 := (= #55 #233)
#235 := [rewrite]: #234
#237 := (iff #56 #236)
#238 := [monotonicity #235]: #237
#241 := [monotonicity #238 #235]: #240
#244 := [monotonicity #241]: #243
#249 := [trans #244 #247]: #248
#252 := [monotonicity #249]: #251
#255 := [monotonicity #252]: #254
#260 := [trans #255 #258]: #259
#230 := (iff #54 #229)
#227 := (= #53 #226)
#228 := [rewrite]: #227
#231 := [monotonicity #228]: #230
#263 := [monotonicity #231 #260]: #262
#221 := (iff #50 #220)
#222 := [rewrite]: #221
#266 := [monotonicity #222 #263]: #265
#327 := [trans #266 #325]: #326
#211 := [asserted]: #62
#328 := [mp #211 #327]: #321
#330 := [and-elim #328]: #292
#597 := (not #292)
#598 := (or #597 #457)
#599 := [th-lemma]: #598
#600 := [unit-resolution #599 #330]: #457
#601 := [hypothesis]: #595
#167 := (<= f5 0::real)
#168 := (not #167)
#27 := (< 0::real f5)
#169 := (iff #27 #168)
#170 := [rewrite]: #169
#164 := [asserted]: #27
#171 := [mp #164 #170]: #168
#602 := [th-lemma #171 #601 #600]: false
#604 := [lemma #602]: #603
#450 := (= f5 #278)
#451 := (= #233 #278)
#613 := (not #451)
#596 := (+ #233 #593)
#605 := (<= #596 0::real)
#610 := (not #605)
#532 := (+ #43 #268)
#533 := (>= #532 0::real)
#538 := (not #533)
#210 := [asserted]: #42
#219 := [mp #210 #218]: #216
#8 := (:var 0 S2)
#35 := (f8 f10 #8)
#443 := (pattern #35)
#33 := (f8 f9 #8)
#442 := (pattern #33)
#9 := (f4 #8)
#422 := (pattern #9)
#193 := (* -1::real #35)
#194 := (+ #33 #193)
#195 := (<= #194 0::real)
#198 := (not #195)
#181 := (* -1::int #30)
#182 := (+ #9 #181)
#180 := (>= #182 0::int)
#201 := (or #180 #198)
#444 := (forall (vars (?v0 S2)) (:pat #422 #442 #443) #201)
#204 := (forall (vars (?v0 S2)) #201)
#447 := (iff #204 #444)
#445 := (iff #201 #201)
#446 := [refl]: #445
#448 := [quant-intro #446]: #447
#362 := (~ #204 #204)
#332 := (~ #201 #201)
#361 := [refl]: #332
#363 := [nnf-pos #361]: #362
#36 := (<= #33 #35)
#37 := (not #36)
#31 := (< #9 #30)
#38 := (implies #31 #37)
#39 := (forall (vars (?v0 S2)) #38)
#207 := (iff #39 #204)
#166 := (not #31)
#172 := (or #166 #37)
#175 := (forall (vars (?v0 S2)) #172)
#205 := (iff #175 #204)
#202 := (iff #172 #201)
#199 := (iff #37 #198)
#196 := (iff #36 #195)
#197 := [rewrite]: #196
#200 := [monotonicity #197]: #199
#190 := (iff #166 #180)
#179 := (not #180)
#185 := (not #179)
#188 := (iff #185 #180)
#189 := [rewrite]: #188
#186 := (iff #166 #185)
#183 := (iff #31 #179)
#184 := [rewrite]: #183
#187 := [monotonicity #184]: #186
#191 := [trans #187 #189]: #190
#203 := [monotonicity #191 #200]: #202
#206 := [quant-intro #203]: #205
#176 := (iff #39 #175)
#173 := (iff #38 #172)
#174 := [rewrite]: #173
#177 := [quant-intro #174]: #176
#208 := [trans #177 #206]: #207
#165 := [asserted]: #39
#209 := [mp #165 #208]: #204
#364 := [mp~ #209 #363]: #204
#449 := [mp #364 #448]: #444
#544 := (not #444)
#545 := (or #544 #215 #538)
#507 := (* -1::real #43)
#508 := (+ #47 #507)
#511 := (<= #508 0::real)
#512 := (not #511)
#513 := (+ #41 #181)
#514 := (>= #513 0::int)
#515 := (or #514 #512)
#546 := (or #544 #515)
#553 := (iff #546 #545)
#541 := (or #215 #538)
#548 := (or #544 #541)
#551 := (iff #548 #545)
#552 := [rewrite]: #551
#549 := (iff #546 #548)
#542 := (iff #515 #541)
#539 := (iff #512 #538)
#536 := (iff #511 #533)
#526 := (+ #507 #47)
#529 := (<= #526 0::real)
#534 := (iff #529 #533)
#535 := [rewrite]: #534
#530 := (iff #511 #529)
#527 := (= #508 #526)
#528 := [rewrite]: #527
#531 := [monotonicity #528]: #530
#537 := [trans #531 #535]: #536
#540 := [monotonicity #537]: #539
#524 := (iff #514 #215)
#516 := (+ #181 #41)
#519 := (>= #516 0::int)
#522 := (iff #519 #215)
#523 := [rewrite]: #522
#520 := (iff #514 #519)
#517 := (= #513 #516)
#518 := [rewrite]: #517
#521 := [monotonicity #518]: #520
#525 := [trans #521 #523]: #524
#543 := [monotonicity #525 #540]: #542
#550 := [monotonicity #543]: #549
#554 := [trans #550 #552]: #553
#547 := [quant-inst]: #546
#555 := [mp #547 #554]: #545
#607 := [unit-resolution #555 #449 #219]: #538
#329 := [and-elim #328]: #270
#608 := [hypothesis]: #605
#609 := [th-lemma #608 #329 #607 #600]: false
#611 := [lemma #609]: #610
#612 := [hypothesis]: #451
#614 := (or #613 #605)
#615 := [th-lemma]: #614
#616 := [unit-resolution #615 #612 #611]: false
#617 := [lemma #616]: #613
#455 := (or #275 #451)
#456 := [def-axiom]: #455
#618 := [unit-resolution #456 #617]: #275
#452 := (not #275)
#453 := (or #452 #450)
#454 := [def-axiom]: #453
#619 := [unit-resolution #454 #618]: #450
#620 := (not #450)
#621 := (or #620 #595)
#622 := [th-lemma]: #621
[unit-resolution #622 #619 #604]: false
unsat
4c36877468848170cffdf0ddcda5eb522e99ab42 295 0
#2 := false
#25 := 0::real
decl f8 :: (-> S4 S2 real)
decl f11 :: S2
#40 := f11
decl f12 :: S4
#44 := f12
#45 := (f8 f12 f11)
decl f10 :: S4
#34 := f10
#43 := (f8 f10 f11)
#199 := -1::real
#263 := (* -1::real #43)
#264 := (+ #263 #45)
decl f5 :: real
#26 := f5
#242 := (* -1::real #45)
#331 := (+ #43 #242)
#332 := (+ f5 #331)
#333 := (<= #332 0::real)
#336 := (ite #333 f5 #264)
#666 := (* -1::real #336)
#667 := (+ f5 #666)
#668 := (<= #667 0::real)
#676 := (not #668)
#230 := 1/2::real
#414 := (* 1/2::real #336)
#531 := (<= #414 0::real)
#415 := (= #414 0::real)
#284 := -1/2::real
#339 := (* -1/2::real #336)
#342 := (+ #45 #339)
decl f9 :: S4
#32 := f9
#47 := (f8 f9 f11)
#243 := (+ #242 #47)
#316 := (* -1::real #47)
#317 := (+ #45 #316)
#318 := (+ f5 #317)
#319 := (<= #318 0::real)
#322 := (ite #319 f5 #243)
#325 := (* 1/2::real #322)
#328 := (+ #45 #325)
#232 := (* 1/2::real #47)
#312 := (+ #242 #232)
#231 := (* 1/2::real #43)
#313 := (+ #231 #312)
#310 := (>= #313 0::real)
#345 := (ite #310 #328 #342)
#348 := (= #45 #345)
#418 := (iff #348 #415)
#411 := (= #45 #342)
#416 := (iff #411 #415)
#417 := [rewrite]: #416
#412 := (iff #348 #411)
#409 := (= #345 #342)
#404 := (ite false #328 #342)
#407 := (= #404 #342)
#408 := [rewrite]: #407
#405 := (= #345 #404)
#402 := (iff #310 false)
#309 := (not #310)
#361 := (<= #317 0::real)
#358 := (<= #331 0::real)
#364 := (and #358 #361)
#13 := 0::int
decl f4 :: (-> S2 int)
#41 := (f4 f11)
#185 := -1::int
#220 := (* -1::int #41)
decl f6 :: (-> S3 S2)
decl f7 :: S3
#28 := f7
#29 := (f6 f7)
#30 := (f4 #29)
#221 := (+ #30 #220)
#222 := (<= #221 0::int)
#367 := (or #222 #364)
#376 := (and #309 #348 #367)
#52 := 2::real
#61 := (- #45 #43)
#62 := (<= f5 #61)
#63 := (ite #62 f5 #61)
#64 := (/ #63 2::real)
#65 := (- #45 #64)
#56 := (- #47 #45)
#57 := (<= f5 #56)
#58 := (ite #57 f5 #56)
#59 := (/ #58 2::real)
#60 := (+ #45 #59)
#51 := (+ #43 #47)
#53 := (/ #51 2::real)
#55 := (<= #45 #53)
#66 := (ite #55 #60 #65)
#67 := (= #66 #45)
#54 := (< #53 #45)
#68 := (and #54 #67)
#48 := (<= #45 #47)
#46 := (<= #43 #45)
#49 := (and #46 #48)
#42 := (< #41 #30)
#50 := (implies #42 #49)
#69 := (and #50 #68)
#381 := (iff #69 #376)
#267 := (<= f5 #264)
#270 := (ite #267 f5 #264)
#285 := (* -1/2::real #270)
#286 := (+ #45 #285)
#246 := (<= f5 #243)
#249 := (ite #246 f5 #243)
#255 := (* 1/2::real #249)
#260 := (+ #45 #255)
#233 := (+ #231 #232)
#239 := (<= #45 #233)
#291 := (ite #239 #260 #286)
#297 := (= #45 #291)
#236 := (< #233 #45)
#302 := (and #236 #297)
#219 := (not #42)
#227 := (or #219 #49)
#305 := (and #227 #302)
#379 := (iff #305 #376)
#370 := (and #309 #348)
#373 := (and #367 #370)
#377 := (iff #373 #376)
#378 := [rewrite]: #377
#374 := (iff #305 #373)
#371 := (iff #302 #370)
#349 := (iff #297 #348)
#346 := (= #291 #345)
#343 := (= #286 #342)
#340 := (= #285 #339)
#337 := (= #270 #336)
#334 := (iff #267 #333)
#335 := [rewrite]: #334
#338 := [monotonicity #335]: #337
#341 := [monotonicity #338]: #340
#344 := [monotonicity #341]: #343
#329 := (= #260 #328)
#326 := (= #255 #325)
#323 := (= #249 #322)
#320 := (iff #246 #319)
#321 := [rewrite]: #320
#324 := [monotonicity #321]: #323
#327 := [monotonicity #324]: #326
#330 := [monotonicity #327]: #329
#315 := (iff #239 #310)
#314 := [rewrite]: #315
#347 := [monotonicity #314 #330 #344]: #346
#350 := [monotonicity #347]: #349
#308 := (iff #236 #309)
#311 := [rewrite]: #308
#372 := [monotonicity #311 #350]: #371
#368 := (iff #227 #367)
#365 := (iff #49 #364)
#362 := (iff #48 #361)
#363 := [rewrite]: #362
#359 := (iff #46 #358)
#360 := [rewrite]: #359
#366 := [monotonicity #360 #363]: #365
#356 := (iff #219 #222)
#223 := (not #222)
#351 := (not #223)
#354 := (iff #351 #222)
#355 := [rewrite]: #354
#352 := (iff #219 #351)
#224 := (iff #42 #223)
#225 := [rewrite]: #224
#353 := [monotonicity #225]: #352
#357 := [trans #353 #355]: #356
#369 := [monotonicity #357 #366]: #368
#375 := [monotonicity #369 #372]: #374
#380 := [trans #375 #378]: #379
#306 := (iff #69 #305)
#303 := (iff #68 #302)
#300 := (iff #67 #297)
#294 := (= #291 #45)
#298 := (iff #294 #297)
#299 := [rewrite]: #298
#295 := (iff #67 #294)
#292 := (= #66 #291)
#289 := (= #65 #286)
#276 := (* 1/2::real #270)
#281 := (- #45 #276)
#287 := (= #281 #286)
#288 := [rewrite]: #287
#282 := (= #65 #281)
#279 := (= #64 #276)
#273 := (/ #270 2::real)
#277 := (= #273 #276)
#278 := [rewrite]: #277
#274 := (= #64 #273)
#271 := (= #63 #270)
#265 := (= #61 #264)
#266 := [rewrite]: #265
#268 := (iff #62 #267)
#269 := [monotonicity #266]: #268
#272 := [monotonicity #269 #266]: #271
#275 := [monotonicity #272]: #274
#280 := [trans #275 #278]: #279
#283 := [monotonicity #280]: #282
#290 := [trans #283 #288]: #289
#261 := (= #60 #260)
#258 := (= #59 #255)
#252 := (/ #249 2::real)
#256 := (= #252 #255)
#257 := [rewrite]: #256
#253 := (= #59 #252)
#250 := (= #58 #249)
#244 := (= #56 #243)
#245 := [rewrite]: #244
#247 := (iff #57 #246)
#248 := [monotonicity #245]: #247
#251 := [monotonicity #248 #245]: #250
#254 := [monotonicity #251]: #253
#259 := [trans #254 #257]: #258
#262 := [monotonicity #259]: #261
#240 := (iff #55 #239)
#234 := (= #53 #233)
#235 := [rewrite]: #234
#241 := [monotonicity #235]: #240
#293 := [monotonicity #241 #262 #290]: #292
#296 := [monotonicity #293]: #295
#301 := [trans #296 #299]: #300
#237 := (iff #54 #236)
#238 := [monotonicity #235]: #237
#304 := [monotonicity #238 #301]: #303
#228 := (iff #50 #227)
#229 := [rewrite]: #228
#307 := [monotonicity #229 #304]: #306
#382 := [trans #307 #380]: #381
#218 := [asserted]: #69
#383 := [mp #218 #382]: #376
#384 := [and-elim #383]: #309
#403 := [iff-false #384]: #402
#406 := [monotonicity #403]: #405
#410 := [trans #406 #408]: #409
#413 := [monotonicity #410]: #412
#419 := [trans #413 #417]: #418
#385 := [and-elim #383]: #348
#420 := [mp #385 #419]: #415
#670 := (not #415)
#671 := (or #670 #531)
#672 := [th-lemma]: #671
#673 := [unit-resolution #672 #420]: #531
#674 := [hypothesis]: #668
#174 := (<= f5 0::real)
#175 := (not #174)
#27 := (< 0::real f5)
#176 := (iff #27 #175)
#177 := [rewrite]: #176
#171 := [asserted]: #27
#178 := [mp #171 #177]: #175
#675 := [th-lemma #178 #674 #673]: false
#677 := [lemma #675]: #676
#524 := (= f5 #336)
#525 := (= #264 #336)
#685 := (not #525)
#669 := (+ #264 #666)
#678 := (<= #669 0::real)
#682 := (not #678)
#428 := (iff #367 #364)
#423 := (or false #364)
#426 := (iff #423 #364)
#427 := [rewrite]: #426
#424 := (iff #367 #423)
#400 := (iff #222 false)
#217 := [asserted]: #42
#226 := [mp #217 #225]: #223
#401 := [iff-false #226]: #400
#425 := [monotonicity #401]: #424
#429 := [trans #425 #427]: #428
#386 := [and-elim #383]: #367
#430 := [mp #386 #429]: #364
#422 := [and-elim #430]: #361
#680 := [hypothesis]: #678
#681 := [th-lemma #680 #422 #384 #673]: false
#683 := [lemma #681]: #682
#684 := [hypothesis]: #525
#686 := (or #685 #678)
#687 := [th-lemma]: #686
#688 := [unit-resolution #687 #684 #683]: false
#689 := [lemma #688]: #685
#529 := (or #333 #525)
#530 := [def-axiom]: #529
#690 := [unit-resolution #530 #689]: #333
#526 := (not #333)
#527 := (or #526 #524)
#528 := [def-axiom]: #527
#691 := [unit-resolution #528 #690]: #524
#692 := (not #524)
#693 := (or #692 #668)
#694 := [th-lemma]: #693
[unit-resolution #694 #691 #677]: false
unsat
f2fb6a78bd5ef0d3bd81c73f0edb01f05b9ead4b 204 0
#2 := false
#46 := 0::real
decl f5 :: (-> S3 S2 real)
decl f7 :: S2
#26 := f7
decl f11 :: S3
#38 := f11
#49 := (f5 f11 f7)
#183 := -1::real
#349 := (* -1::real #49)
decl f8 :: S3
#28 := f8
#29 := (f5 f8 f7)
#362 := (+ #29 #349)
#363 := (>= #362 0::real)
#368 := (not #363)
decl f6 :: S3
#25 := f6
#27 := (f5 f6 f7)
#350 := (+ #27 #349)
#351 := (<= #350 0::real)
#352 := (not #351)
#371 := (or #352 #368)
#374 := (not #371)
#8 := (:var 0 S2)
#41 := (f5 f8 #8)
#333 := (pattern #41)
#39 := (f5 f11 #8)
#332 := (pattern #39)
#37 := (f5 f6 #8)
#331 := (pattern #37)
decl f4 :: (-> S2 int)
#9 := (f4 #8)
#311 := (pattern #9)
#189 := (* -1::real #41)
#190 := (+ #39 #189)
#191 := (<= #190 0::real)
#242 := (not #191)
#184 := (* -1::real #39)
#185 := (+ #37 #184)
#186 := (<= #185 0::real)
#241 := (not #186)
#243 := (or #241 #242)
#244 := (not #243)
#13 := 0::int
decl f9 :: (-> S4 S2)
decl f10 :: S4
#32 := f10
#33 := (f9 f10)
#34 := (f4 #33)
#157 := -1::int
#160 := (* -1::int #34)
#173 := (+ #9 #160)
#172 := (>= #173 0::int)
#247 := (or #172 #244)
#334 := (forall (vars (?v0 S2)) (:pat #311 #331 #332 #333) #247)
#250 := (forall (vars (?v0 S2)) #247)
#337 := (iff #250 #334)
#335 := (iff #247 #247)
#336 := [refl]: #335
#338 := [quant-intro #336]: #337
#194 := (and #186 #191)
#197 := (or #172 #194)
#200 := (forall (vars (?v0 S2)) #197)
#251 := (iff #200 #250)
#248 := (iff #197 #247)
#245 := (iff #194 #244)
#246 := [rewrite]: #245
#249 := [monotonicity #246]: #248
#252 := [quant-intro #249]: #251
#219 := (~ #200 #200)
#224 := (~ #197 #197)
#222 := [refl]: #224
#239 := [nnf-pos #222]: #219
#42 := (<= #39 #41)
#40 := (<= #37 #39)
#43 := (and #40 #42)
#36 := (< #9 #34)
#44 := (implies #36 #43)
#45 := (forall (vars (?v0 S2)) #44)
#203 := (iff #45 #200)
#156 := (not #36)
#165 := (or #156 #43)
#168 := (forall (vars (?v0 S2)) #165)
#201 := (iff #168 #200)
#198 := (iff #165 #197)
#195 := (iff #43 #194)
#192 := (iff #42 #191)
#193 := [rewrite]: #192
#187 := (iff #40 #186)
#188 := [rewrite]: #187
#196 := [monotonicity #188 #193]: #195
#181 := (iff #156 #172)
#171 := (not #172)
#176 := (not #171)
#179 := (iff #176 #172)
#180 := [rewrite]: #179
#177 := (iff #156 #176)
#174 := (iff #36 #171)
#175 := [rewrite]: #174
#178 := [monotonicity #175]: #177
#182 := [trans #178 #180]: #181
#199 := [monotonicity #182 #196]: #198
#202 := [quant-intro #199]: #201
#169 := (iff #45 #168)
#166 := (iff #44 #165)
#167 := [rewrite]: #166
#170 := [quant-intro #167]: #169
#204 := [trans #170 #202]: #203
#155 := [asserted]: #45
#205 := [mp #155 #204]: #200
#240 := [mp~ #205 #239]: #200
#253 := [mp #240 #252]: #250
#339 := [mp #253 #338]: #334
#31 := (f4 f7)
#161 := (+ #31 #160)
#159 := (>= #161 0::int)
#158 := (not #159)
#35 := (< #31 #34)
#162 := (iff #35 #158)
#163 := [rewrite]: #162
#154 := [asserted]: #35
#164 := [mp #154 #163]: #158
#380 := (not #334)
#381 := (or #380 #159 #374)
#342 := (* -1::real #29)
#343 := (+ #49 #342)
#347 := (<= #343 0::real)
#348 := (not #347)
#353 := (or #352 #348)
#354 := (not #353)
#355 := (or #159 #354)
#382 := (or #380 #355)
#389 := (iff #382 #381)
#377 := (or #159 #374)
#384 := (or #380 #377)
#387 := (iff #384 #381)
#388 := [rewrite]: #387
#385 := (iff #382 #384)
#378 := (iff #355 #377)
#375 := (iff #354 #374)
#372 := (iff #353 #371)
#369 := (iff #348 #368)
#366 := (iff #347 #363)
#356 := (+ #342 #49)
#359 := (<= #356 0::real)
#364 := (iff #359 #363)
#365 := [rewrite]: #364
#360 := (iff #347 #359)
#357 := (= #343 #356)
#358 := [rewrite]: #357
#361 := [monotonicity #358]: #360
#367 := [trans #361 #365]: #366
#370 := [monotonicity #367]: #369
#373 := [monotonicity #370]: #372
#376 := [monotonicity #373]: #375
#379 := [monotonicity #376]: #378
#386 := [monotonicity #379]: #385
#390 := [trans #386 #388]: #389
#383 := [quant-inst]: #382
#391 := [mp #383 #390]: #381
#513 := [unit-resolution #391 #164 #339]: #374
#394 := (or #371 #363)
#395 := [def-axiom]: #394
#514 := [unit-resolution #395 #513]: #363
#475 := (>= #350 0::real)
#524 := (not #475)
#474 := (= #27 #49)
#519 := (not #474)
#208 := (= #29 #49)
#216 := (not #208)
#520 := (iff #216 #519)
#517 := (iff #208 #474)
#515 := (iff #474 #208)
#30 := (= #27 #29)
#153 := [asserted]: #30
#516 := [monotonicity #153]: #515
#518 := [symm #516]: #517
#521 := [monotonicity #518]: #520
#50 := (= #49 #29)
#51 := (not #50)
#217 := (iff #51 #216)
#214 := (iff #50 #208)
#215 := [rewrite]: #214
#218 := [monotonicity #215]: #217
#207 := [asserted]: #51
#221 := [mp #207 #218]: #216
#522 := [mp #221 #521]: #519
#527 := (or #474 #524)
#392 := (or #371 #351)
#393 := [def-axiom]: #392
#523 := [unit-resolution #393 #513]: #351
#525 := (or #474 #352 #524)
#526 := [th-lemma]: #525
#528 := [unit-resolution #526 #523]: #527
#529 := [unit-resolution #528 #522]: #524
#471 := (+ #27 #342)
#473 := (>= #471 0::real)
#530 := (not #30)
#531 := (or #530 #473)
#532 := [th-lemma]: #531
#533 := [unit-resolution #532 #153]: #473
[th-lemma #533 #529 #514]: false
unsat
c57edc9b53558e5e0a7337a056a91568e455bc48 870 0
#2 := false
#11 := 0::real
decl f5 :: real
#26 := f5
decl f3 :: real
#9 := f3
#76 := -1::real
#77 := (* -1::real f3)
#176 := (+ #77 f5)
#124 := (* -1::real f5)
#167 := (+ f3 #124)
#260 := (>= #167 0::real)
#267 := (ite #260 #167 #176)
#275 := (* -1::real #267)
decl f4 :: real
#15 := f4
#96 := 1/3::real
#97 := (* 1/3::real f4)
#276 := (+ #97 #275)
#277 := (<= #276 0::real)
#278 := (not #277)
decl ?v0!5 :: real
#448 := ?v0!5
#459 := (* -1::real ?v0!5)
#573 := (+ f3 #459)
#567 := (+ #77 ?v0!5)
#574 := (<= #573 0::real)
#581 := (ite #574 #567 #573)
#584 := (* -1::real #581)
#587 := (+ #97 #584)
#590 := (<= #587 0::real)
#593 := (not #590)
decl ?v2!3 :: real
#442 := ?v2!3
#477 := (* -1::real ?v2!3)
#544 := (+ f5 #477)
#538 := (+ #124 ?v2!3)
#545 := (<= #544 0::real)
#552 := (ite #545 #538 #544)
#555 := (* -1::real #552)
#558 := (+ #97 #555)
#561 := (<= #558 0::real)
#564 := (not #561)
decl ?v4!1 :: real
#446 := ?v4!1
#532 := (+ ?v4!1 #459)
#533 := (>= #532 0::real)
decl ?v1!4 :: real
#447 := ?v1!4
#468 := (* -1::real ?v1!4)
decl ?v5!0 :: real
#445 := ?v5!0
#520 := (+ ?v5!0 #468)
#521 := (>= #520 0::real)
#451 := (* -1::real ?v5!0)
decl ?v3!2 :: real
#444 := ?v3!2
#499 := (+ ?v3!2 #451)
#500 := (>= #499 0::real)
#449 := (* -1::real ?v4!1)
#497 := (+ ?v2!3 #449)
#498 := (>= #497 0::real)
#486 := (* -1::real ?v3!2)
#487 := (+ f5 #486)
#488 := (+ #124 ?v3!2)
#489 := (<= #487 0::real)
#490 := (ite #489 #488 #487)
#491 := (* -1::real #490)
#492 := (+ #97 #491)
#493 := (<= #492 0::real)
#494 := (not #493)
#469 := (+ f3 #468)
#470 := (+ #77 ?v1!4)
#471 := (<= #469 0::real)
#472 := (ite #471 #470 #469)
#473 := (* -1::real #472)
#474 := (+ #97 #473)
#475 := (<= #474 0::real)
#476 := (not #475)
#599 := (and #278 #476 #494 #498 #500 #521 #533 #564 #593)
#613 := (+ ?v5!0 #449)
#607 := (+ #451 ?v4!1)
#614 := (<= #613 0::real)
#621 := (ite #614 #607 #613)
#624 := (* -1::real #621)
#627 := (+ f4 #624)
#630 := (<= #627 0::real)
#633 := (not #630)
#604 := (not #599)
#636 := (or #604 #633)
#639 := (not #636)
#450 := (+ #449 ?v5!0)
#452 := (+ ?v4!1 #451)
#453 := (>= #452 0::real)
#454 := (ite #453 #452 #450)
#455 := (* -1::real #454)
#456 := (+ f4 #455)
#457 := (<= #456 0::real)
#458 := (not #457)
#460 := (+ #459 f3)
#461 := (+ ?v0!5 #77)
#462 := (>= #461 0::real)
#463 := (ite #462 #461 #460)
#464 := (* -1::real #463)
#465 := (+ #97 #464)
#466 := (<= #465 0::real)
#467 := (not #466)
#478 := (+ #477 f5)
#479 := (+ ?v2!3 #124)
#480 := (>= #479 0::real)
#481 := (ite #480 #479 #478)
#482 := (* -1::real #481)
#483 := (+ #97 #482)
#484 := (<= #483 0::real)
#485 := (not #484)
#495 := (+ ?v0!5 #449)
#496 := (<= #495 0::real)
#501 := (+ ?v1!4 #451)
#502 := (<= #501 0::real)
#503 := (and #502 #500 #498 #496 #278 #494 #485 #476 #467)
#504 := (not #503)
#505 := (or #504 #458)
#506 := (not #505)
#640 := (iff #506 #639)
#637 := (iff #505 #636)
#634 := (iff #458 #633)
#631 := (iff #457 #630)
#628 := (= #456 #627)
#625 := (= #455 #624)
#622 := (= #454 #621)
#619 := (= #450 #613)
#620 := [rewrite]: #619
#608 := (= #452 #607)
#609 := [rewrite]: #608
#617 := (iff #453 #614)
#610 := (>= #607 0::real)
#615 := (iff #610 #614)
#616 := [rewrite]: #615
#611 := (iff #453 #610)
#612 := [monotonicity #609]: #611
#618 := [trans #612 #616]: #617
#623 := [monotonicity #618 #609 #620]: #622
#626 := [monotonicity #623]: #625
#629 := [monotonicity #626]: #628
#632 := [monotonicity #629]: #631
#635 := [monotonicity #632]: #634
#605 := (iff #504 #604)
#602 := (iff #503 #599)
#596 := (and #521 #500 #498 #533 #278 #494 #564 #476 #593)
#600 := (iff #596 #599)
#601 := [rewrite]: #600
#597 := (iff #503 #596)
#594 := (iff #467 #593)
#591 := (iff #466 #590)
#588 := (= #465 #587)
#585 := (= #464 #584)
#582 := (= #463 #581)
#579 := (= #460 #573)
#580 := [rewrite]: #579
#568 := (= #461 #567)
#569 := [rewrite]: #568
#577 := (iff #462 #574)
#570 := (>= #567 0::real)
#575 := (iff #570 #574)
#576 := [rewrite]: #575
#571 := (iff #462 #570)
#572 := [monotonicity #569]: #571
#578 := [trans #572 #576]: #577
#583 := [monotonicity #578 #569 #580]: #582
#586 := [monotonicity #583]: #585
#589 := [monotonicity #586]: #588
#592 := [monotonicity #589]: #591
#595 := [monotonicity #592]: #594
#565 := (iff #485 #564)
#562 := (iff #484 #561)
#559 := (= #483 #558)
#556 := (= #482 #555)
#553 := (= #481 #552)
#550 := (= #478 #544)
#551 := [rewrite]: #550
#539 := (= #479 #538)
#540 := [rewrite]: #539
#548 := (iff #480 #545)
#541 := (>= #538 0::real)
#546 := (iff #541 #545)
#547 := [rewrite]: #546
#542 := (iff #480 #541)
#543 := [monotonicity #540]: #542
#549 := [trans #543 #547]: #548
#554 := [monotonicity #549 #540 #551]: #553
#557 := [monotonicity #554]: #556
#560 := [monotonicity #557]: #559
#563 := [monotonicity #560]: #562
#566 := [monotonicity #563]: #565
#536 := (iff #496 #533)
#526 := (+ #449 ?v0!5)
#529 := (<= #526 0::real)
#534 := (iff #529 #533)
#535 := [rewrite]: #534
#530 := (iff #496 #529)
#527 := (= #495 #526)
#528 := [rewrite]: #527
#531 := [monotonicity #528]: #530
#537 := [trans #531 #535]: #536
#524 := (iff #502 #521)
#514 := (+ #451 ?v1!4)
#517 := (<= #514 0::real)
#522 := (iff #517 #521)
#523 := [rewrite]: #522
#518 := (iff #502 #517)
#515 := (= #501 #514)
#516 := [rewrite]: #515
#519 := [monotonicity #516]: #518
#525 := [trans #519 #523]: #524
#598 := [monotonicity #525 #537 #566 #595]: #597
#603 := [trans #598 #601]: #602
#606 := [monotonicity #603]: #605
#638 := [monotonicity #606 #635]: #637
#641 := [monotonicity #638]: #640
#46 := (:var 0 real)
#43 := (:var 1 real)
#217 := (* -1::real #43)
#218 := (+ #217 #46)
#207 := (* -1::real #46)
#208 := (+ #43 #207)
#407 := (>= #208 0::real)
#414 := (ite #407 #208 #218)
#422 := (* -1::real #414)
#423 := (+ f4 #422)
#424 := (<= #423 0::real)
#425 := (not #424)
#8 := (:var 5 real)
#87 := (* -1::real #8)
#88 := (+ #87 f3)
#78 := (+ #8 #77)
#352 := (>= #78 0::real)
#359 := (ite #352 #78 #88)
#367 := (* -1::real #359)
#368 := (+ #97 #367)
#369 := (<= #368 0::real)
#370 := (not #369)
#19 := (:var 4 real)
#112 := (* -1::real #19)
#113 := (+ f3 #112)
#103 := (+ #77 #19)
#329 := (<= #113 0::real)
#336 := (ite #329 #103 #113)
#344 := (* -1::real #336)
#345 := (+ #97 #344)
#346 := (<= #345 0::real)
#347 := (not #346)
#25 := (:var 3 real)
#134 := (* -1::real #25)
#135 := (+ #134 f5)
#125 := (+ #25 #124)
#306 := (>= #125 0::real)
#313 := (ite #306 #125 #135)
#321 := (* -1::real #313)
#322 := (+ #97 #321)
#323 := (<= #322 0::real)
#324 := (not #323)
#32 := (:var 2 real)
#155 := (* -1::real #32)
#156 := (+ f5 #155)
#146 := (+ #124 #32)
#283 := (<= #156 0::real)
#290 := (ite #283 #146 #156)
#298 := (* -1::real #290)
#299 := (+ #97 #298)
#300 := (<= #299 0::real)
#301 := (not #300)
#256 := (+ #8 #217)
#257 := (<= #256 0::real)
#253 := (+ #25 #217)
#252 := (>= #253 0::real)
#249 := (+ #32 #207)
#248 := (>= #249 0::real)
#244 := (+ #19 #207)
#245 := (<= #244 0::real)
#399 := (and #245 #248 #252 #257 #278 #301 #324 #347 #370)
#404 := (not #399)
#430 := (or #404 #425)
#433 := (forall (vars (?v0 real) (?v1 real) (?v2 real) (?v3 real) (?v4 real) (?v5 real)) #430)
#436 := (not #433)
#507 := (~ #436 #506)
#508 := [sk]: #507
#57 := (- #43 #46)
#59 := (- #57)
#58 := (< #57 0::real)
#60 := (ite #58 #59 #57)
#61 := (< #60 f4)
#48 := (<= #46 #32)
#47 := (<= #19 #46)
#49 := (and #47 #48)
#45 := (<= #43 #25)
#50 := (and #45 #49)
#44 := (<= #8 #43)
#51 := (and #44 #50)
#16 := 3::real
#17 := (/ f4 3::real)
#38 := (- f3 f5)
#40 := (- #38)
#39 := (< #38 0::real)
#41 := (ite #39 #40 #38)
#42 := (< #41 #17)
#52 := (and #42 #51)
#33 := (- #32 f5)
#35 := (- #33)
#34 := (< #33 0::real)
#36 := (ite #34 #35 #33)
#37 := (< #36 #17)
#53 := (and #37 #52)
#27 := (- #25 f5)
#29 := (- #27)
#28 := (< #27 0::real)
#30 := (ite #28 #29 #27)
#31 := (< #30 #17)
#54 := (and #31 #53)
#20 := (- #19 f3)
#22 := (- #20)
#21 := (< #20 0::real)
#23 := (ite #21 #22 #20)
#24 := (< #23 #17)
#55 := (and #24 #54)
#10 := (- #8 f3)
#13 := (- #10)
#12 := (< #10 0::real)
#14 := (ite #12 #13 #10)
#18 := (< #14 #17)
#56 := (and #18 #55)
#62 := (implies #56 #61)
#63 := (forall (vars (?v0 real) (?v1 real) (?v2 real) (?v3 real) (?v4 real) (?v5 real)) #62)
#64 := (not #63)
#439 := (iff #64 #436)
#211 := (< #208 0::real)
#223 := (ite #211 #218 #208)
#226 := (< #223 f4)
#170 := (< #167 0::real)
#181 := (ite #170 #176 #167)
#184 := (< #181 #97)
#190 := (and #51 #184)
#149 := (< #146 0::real)
#161 := (ite #149 #156 #146)
#164 := (< #161 #97)
#195 := (and #164 #190)
#128 := (< #125 0::real)
#140 := (ite #128 #135 #125)
#143 := (< #140 #97)
#198 := (and #143 #195)
#106 := (< #103 0::real)
#118 := (ite #106 #113 #103)
#121 := (< #118 #97)
#201 := (and #121 #198)
#81 := (< #78 0::real)
#93 := (ite #81 #88 #78)
#100 := (< #93 #97)
#204 := (and #100 #201)
#232 := (not #204)
#233 := (or #232 #226)
#238 := (forall (vars (?v0 real) (?v1 real) (?v2 real) (?v3 real) (?v4 real) (?v5 real)) #233)
#241 := (not #238)
#437 := (iff #241 #436)
#434 := (iff #238 #433)
#431 := (iff #233 #430)
#428 := (iff #226 #425)
#419 := (< #414 f4)
#426 := (iff #419 #425)
#427 := [rewrite]: #426
#420 := (iff #226 #419)
#417 := (= #223 #414)
#408 := (not #407)
#411 := (ite #408 #218 #208)
#415 := (= #411 #414)
#416 := [rewrite]: #415
#412 := (= #223 #411)
#409 := (iff #211 #408)
#410 := [rewrite]: #409
#413 := [monotonicity #410]: #412
#418 := [trans #413 #416]: #417
#421 := [monotonicity #418]: #420
#429 := [trans #421 #427]: #428
#405 := (iff #232 #404)
#402 := (iff #204 #399)
#375 := (and #245 #248)
#378 := (and #252 #375)
#381 := (and #257 #378)
#384 := (and #381 #278)
#387 := (and #301 #384)
#390 := (and #324 #387)
#393 := (and #347 #390)
#396 := (and #370 #393)
#400 := (iff #396 #399)
#401 := [rewrite]: #400
#397 := (iff #204 #396)
#394 := (iff #201 #393)
#391 := (iff #198 #390)
#388 := (iff #195 #387)
#385 := (iff #190 #384)
#281 := (iff #184 #278)
#272 := (< #267 #97)
#279 := (iff #272 #278)
#280 := [rewrite]: #279
#273 := (iff #184 #272)
#270 := (= #181 #267)
#261 := (not #260)
#264 := (ite #261 #176 #167)
#268 := (= #264 #267)
#269 := [rewrite]: #268
#265 := (= #181 #264)
#262 := (iff #170 #261)
#263 := [rewrite]: #262
#266 := [monotonicity #263]: #265
#271 := [trans #266 #269]: #270
#274 := [monotonicity #271]: #273
#282 := [trans #274 #280]: #281
#382 := (iff #51 #381)
#379 := (iff #50 #378)
#376 := (iff #49 #375)
#250 := (iff #48 #248)
#251 := [rewrite]: #250
#246 := (iff #47 #245)
#247 := [rewrite]: #246
#377 := [monotonicity #247 #251]: #376
#254 := (iff #45 #252)
#255 := [rewrite]: #254
#380 := [monotonicity #255 #377]: #379
#258 := (iff #44 #257)
#259 := [rewrite]: #258
#383 := [monotonicity #259 #380]: #382
#386 := [monotonicity #383 #282]: #385
#304 := (iff #164 #301)
#295 := (< #290 #97)
#302 := (iff #295 #301)
#303 := [rewrite]: #302
#296 := (iff #164 #295)
#293 := (= #161 #290)
#284 := (not #283)
#287 := (ite #284 #156 #146)
#291 := (= #287 #290)
#292 := [rewrite]: #291
#288 := (= #161 #287)
#285 := (iff #149 #284)
#286 := [rewrite]: #285
#289 := [monotonicity #286]: #288
#294 := [trans #289 #292]: #293
#297 := [monotonicity #294]: #296
#305 := [trans #297 #303]: #304
#389 := [monotonicity #305 #386]: #388
#327 := (iff #143 #324)
#318 := (< #313 #97)
#325 := (iff #318 #324)
#326 := [rewrite]: #325
#319 := (iff #143 #318)
#316 := (= #140 #313)
#307 := (not #306)
#310 := (ite #307 #135 #125)
#314 := (= #310 #313)
#315 := [rewrite]: #314
#311 := (= #140 #310)
#308 := (iff #128 #307)
#309 := [rewrite]: #308
#312 := [monotonicity #309]: #311
#317 := [trans #312 #315]: #316
#320 := [monotonicity #317]: #319
#328 := [trans #320 #326]: #327
#392 := [monotonicity #328 #389]: #391
#350 := (iff #121 #347)
#341 := (< #336 #97)
#348 := (iff #341 #347)
#349 := [rewrite]: #348
#342 := (iff #121 #341)
#339 := (= #118 #336)
#330 := (not #329)
#333 := (ite #330 #113 #103)
#337 := (= #333 #336)
#338 := [rewrite]: #337
#334 := (= #118 #333)
#331 := (iff #106 #330)
#332 := [rewrite]: #331
#335 := [monotonicity #332]: #334
#340 := [trans #335 #338]: #339
#343 := [monotonicity #340]: #342
#351 := [trans #343 #349]: #350
#395 := [monotonicity #351 #392]: #394
#373 := (iff #100 #370)
#364 := (< #359 #97)
#371 := (iff #364 #370)
#372 := [rewrite]: #371
#365 := (iff #100 #364)
#362 := (= #93 #359)
#353 := (not #352)
#356 := (ite #353 #88 #78)
#360 := (= #356 #359)
#361 := [rewrite]: #360
#357 := (= #93 #356)
#354 := (iff #81 #353)
#355 := [rewrite]: #354
#358 := [monotonicity #355]: #357
#363 := [trans #358 #361]: #362
#366 := [monotonicity #363]: #365
#374 := [trans #366 #372]: #373
#398 := [monotonicity #374 #395]: #397
#403 := [trans #398 #401]: #402
#406 := [monotonicity #403]: #405
#432 := [monotonicity #406 #429]: #431
#435 := [quant-intro #432]: #434
#438 := [monotonicity #435]: #437
#242 := (iff #64 #241)
#239 := (iff #63 #238)
#236 := (iff #62 #233)
#229 := (implies #204 #226)
#234 := (iff #229 #233)
#235 := [rewrite]: #234
#230 := (iff #62 #229)
#227 := (iff #61 #226)
#224 := (= #60 #223)
#209 := (= #57 #208)
#210 := [rewrite]: #209
#221 := (= #59 #218)
#214 := (- #208)
#219 := (= #214 #218)
#220 := [rewrite]: #219
#215 := (= #59 #214)
#216 := [monotonicity #210]: #215
#222 := [trans #216 #220]: #221
#212 := (iff #58 #211)
#213 := [monotonicity #210]: #212
#225 := [monotonicity #213 #222 #210]: #224
#228 := [monotonicity #225]: #227
#205 := (iff #56 #204)
#202 := (iff #55 #201)
#199 := (iff #54 #198)
#196 := (iff #53 #195)
#193 := (iff #52 #190)
#187 := (and #184 #51)
#191 := (iff #187 #190)
#192 := [rewrite]: #191
#188 := (iff #52 #187)
#185 := (iff #42 #184)
#98 := (= #17 #97)
#99 := [rewrite]: #98
#182 := (= #41 #181)
#168 := (= #38 #167)
#169 := [rewrite]: #168
#179 := (= #40 #176)
#173 := (- #167)
#177 := (= #173 #176)
#178 := [rewrite]: #177
#174 := (= #40 #173)
#175 := [monotonicity #169]: #174
#180 := [trans #175 #178]: #179
#171 := (iff #39 #170)
#172 := [monotonicity #169]: #171
#183 := [monotonicity #172 #180 #169]: #182
#186 := [monotonicity #183 #99]: #185
#189 := [monotonicity #186]: #188
#194 := [trans #189 #192]: #193
#165 := (iff #37 #164)
#162 := (= #36 #161)
#147 := (= #33 #146)
#148 := [rewrite]: #147
#159 := (= #35 #156)
#152 := (- #146)
#157 := (= #152 #156)
#158 := [rewrite]: #157
#153 := (= #35 #152)
#154 := [monotonicity #148]: #153
#160 := [trans #154 #158]: #159
#150 := (iff #34 #149)
#151 := [monotonicity #148]: #150
#163 := [monotonicity #151 #160 #148]: #162
#166 := [monotonicity #163 #99]: #165
#197 := [monotonicity #166 #194]: #196
#144 := (iff #31 #143)
#141 := (= #30 #140)
#126 := (= #27 #125)
#127 := [rewrite]: #126
#138 := (= #29 #135)
#131 := (- #125)
#136 := (= #131 #135)
#137 := [rewrite]: #136
#132 := (= #29 #131)
#133 := [monotonicity #127]: #132
#139 := [trans #133 #137]: #138
#129 := (iff #28 #128)
#130 := [monotonicity #127]: #129
#142 := [monotonicity #130 #139 #127]: #141
#145 := [monotonicity #142 #99]: #144
#200 := [monotonicity #145 #197]: #199
#122 := (iff #24 #121)
#119 := (= #23 #118)
#104 := (= #20 #103)
#105 := [rewrite]: #104
#116 := (= #22 #113)
#109 := (- #103)
#114 := (= #109 #113)
#115 := [rewrite]: #114
#110 := (= #22 #109)
#111 := [monotonicity #105]: #110
#117 := [trans #111 #115]: #116
#107 := (iff #21 #106)
#108 := [monotonicity #105]: #107
#120 := [monotonicity #108 #117 #105]: #119
#123 := [monotonicity #120 #99]: #122
#203 := [monotonicity #123 #200]: #202
#101 := (iff #18 #100)
#94 := (= #14 #93)
#79 := (= #10 #78)
#80 := [rewrite]: #79
#91 := (= #13 #88)
#84 := (- #78)
#89 := (= #84 #88)
#90 := [rewrite]: #89
#85 := (= #13 #84)
#86 := [monotonicity #80]: #85
#92 := [trans #86 #90]: #91
#82 := (iff #12 #81)
#83 := [monotonicity #80]: #82
#95 := [monotonicity #83 #92 #80]: #94
#102 := [monotonicity #95 #99]: #101
#206 := [monotonicity #102 #203]: #205
#231 := [monotonicity #206 #228]: #230
#237 := [trans #231 #235]: #236
#240 := [quant-intro #237]: #239
#243 := [monotonicity #240]: #242
#440 := [trans #243 #438]: #439
#75 := [asserted]: #64
#441 := [mp #75 #440]: #436
#511 := [mp~ #441 #508]: #506
#512 := [mp #511 #641]: #639
#513 := [not-or-elim #512]: #599
#642 := [and-elim #513]: #278
#644 := [and-elim #513]: #494
#891 := (+ #488 #491)
#892 := (<= #891 0::real)
#720 := (= #488 #490)
#743 := (not #614)
#741 := (= #607 #621)
#884 := (not #741)
#748 := (+ #607 #624)
#750 := (>= #748 0::real)
#778 := (not #750)
#754 := (+ #538 #555)
#755 := (<= #754 0::real)
#777 := (not #755)
#753 := (+ #573 #584)
#756 := (<= #753 0::real)
#735 := (= #573 #581)
#736 := (not #574)
#773 := [hypothesis]: #750
#837 := (or #736 #778)
#648 := [and-elim #513]: #533
#645 := [and-elim #513]: #498
#729 := (not #545)
#727 := (= #538 #552)
#814 := (not #727)
#767 := [hypothesis]: #574
#802 := (or #777 #778 #736)
#763 := (+ #176 #275)
#764 := (<= #763 0::real)
#708 := (= #176 #267)
#757 := (+ #469 #473)
#758 := (<= #757 0::real)
#714 := (= #469 #472)
#715 := (not #471)
#774 := [hypothesis]: #755
#788 := (or #715 #777 #778 #736)
#766 := [hypothesis]: #471
#779 := (or #261 #736 #777 #778 #715)
#649 := [and-elim #513]: #564
#650 := [and-elim #513]: #593
#751 := (+ #567 #584)
#752 := (<= #751 0::real)
#734 := (= #567 #581)
#737 := (or #736 #734)
#738 := [def-axiom]: #737
#768 := [unit-resolution #738 #767]: #734
#769 := (not #734)
#770 := (or #769 #752)
#771 := [th-lemma]: #770
#772 := [unit-resolution #771 #768]: #752
#651 := [not-or-elim #512]: #630
#775 := [hypothesis]: #260
#647 := [and-elim #513]: #521
#776 := [th-lemma #767 #647 #775 #774 #645 #773 #651 #772 #650 #649 #766]: false
#780 := [lemma #776]: #779
#781 := [unit-resolution #780 #766 #774 #773 #767]: #261
#711 := (or #260 #708)
#712 := [def-axiom]: #711
#782 := [unit-resolution #712 #781]: #708
#783 := (not #708)
#784 := (or #783 #764)
#785 := [th-lemma]: #784
#786 := [unit-resolution #785 #782]: #764
#787 := [th-lemma #647 #774 #645 #773 #651 #649 #786 #642 #781 #766]: false
#789 := [lemma #787]: #788
#761 := [unit-resolution #789 #774 #773 #767]: #715
#718 := (or #471 #714)
#719 := [def-axiom]: #718
#762 := [unit-resolution #719 #761]: #714
#765 := (not #714)
#790 := (or #765 #758)
#791 := [th-lemma]: #790
#792 := [unit-resolution #791 #762]: #758
#643 := [and-elim #513]: #476
#795 := (not #758)
#794 := (not #498)
#793 := (not #521)
#796 := (or #261 #471 #793 #777 #794 #778 #633 #561 #795 #475)
#797 := [th-lemma]: #796
#798 := [unit-resolution #797 #761 #643 #645 #647 #649 #651 #773 #774 #792]: #261
#799 := [unit-resolution #712 #798]: #708
#800 := [unit-resolution #785 #799]: #764
#801 := [th-lemma #647 #774 #645 #773 #651 #649 #792 #643 #642 #800]: false
#803 := [lemma #801]: #802
#826 := [unit-resolution #803 #767 #773]: #777
#815 := (or #814 #755)
#804 := [hypothesis]: #777
#805 := [hypothesis]: #727
#816 := [th-lemma]: #815
#817 := [unit-resolution #816 #805 #804]: false
#818 := [lemma #817]: #815
#833 := [unit-resolution #818 #826]: #814
#730 := (or #729 #727)
#731 := [def-axiom]: #730
#834 := [unit-resolution #731 #833]: #729
#831 := (or #260 #545 #778)
#806 := [hypothesis]: #261
#810 := [hypothesis]: #729
#812 := (or #545 #795 #778 #260)
#807 := [unit-resolution #712 #806]: #708
#808 := [unit-resolution #785 #807]: #764
#809 := [hypothesis]: #758
#811 := [th-lemma #810 #645 #809 #643 #647 #773 #651 #808 #642 #806]: false
#813 := [lemma #811]: #812
#827 := [unit-resolution #813 #806 #773 #810]: #795
#821 := [hypothesis]: #795
#822 := [hypothesis]: #714
#823 := [unit-resolution #791 #822 #821]: false
#824 := [lemma #823]: #790
#828 := [unit-resolution #824 #827]: #765
#829 := [unit-resolution #719 #828]: #471
#830 := [th-lemma #808 #642 #829 #810 #645 #647 #773 #651 #806]: false
#832 := [lemma #830]: #831
#835 := [unit-resolution #832 #834 #773]: #260
#836 := [th-lemma #767 #835 #834 #645 #648]: false
#838 := [lemma #836]: #837
#863 := [unit-resolution #838 #773]: #736
#739 := (or #574 #735)
#740 := [def-axiom]: #739
#864 := [unit-resolution #740 #863]: #735
#865 := (not #735)
#866 := (or #865 #756)
#867 := [th-lemma]: #866
#868 := [unit-resolution #867 #864]: #756
#852 := (or #260 #778)
#845 := [unit-resolution #832 #806 #773]: #545
#846 := [unit-resolution #731 #845]: #727
#847 := [unit-resolution #818 #846]: #755
#840 := (not #764)
#841 := (or #795 #777 #778 #840)
#825 := [hypothesis]: #764
#839 := [th-lemma #774 #645 #647 #773 #651 #809 #643 #825 #642 #649]: false
#842 := [lemma #839]: #841
#848 := [unit-resolution #842 #847 #773 #808]: #795
#849 := [unit-resolution #824 #848]: #765
#850 := [unit-resolution #719 #849]: #471
#851 := [th-lemma #847 #649 #645 #647 #773 #651 #808 #850 #806 #642]: false
#853 := [lemma #851]: #852
#859 := [unit-resolution #853 #773]: #260
#870 := (or #471 #778)
#856 := [hypothesis]: #715
#857 := [unit-resolution #719 #856]: #714
#858 := [unit-resolution #824 #857]: #758
#860 := [unit-resolution #797 #858 #643 #645 #647 #649 #651 #773 #859 #856]: #777
#861 := [unit-resolution #818 #860]: #814
#862 := [unit-resolution #731 #861]: #729
#869 := [th-lemma #643 #650 #863 #868 #859 #862 #645 #647 #773 #651 #858]: false
#871 := [lemma #869]: #870
#855 := [unit-resolution #871 #773]: #471
#872 := (not #756)
#873 := (or #777 #590 #574 #872 #561 #261 #794 #793 #778 #633 #715)
#874 := [th-lemma]: #873
#875 := [unit-resolution #874 #855 #645 #647 #649 #863 #650 #651 #773 #859 #868]: #777
#876 := (or #545 #261 #794 #793 #778 #633 #715 #590 #574 #872)
#877 := [th-lemma]: #876
#878 := [unit-resolution #877 #855 #645 #647 #859 #863 #650 #651 #773 #868]: #545
#879 := [unit-resolution #731 #878]: #727
#880 := [unit-resolution #818 #879 #875]: false
#881 := [lemma #880]: #778
#883 := [hypothesis]: #741
#885 := (or #884 #750)
#886 := [th-lemma]: #885
#887 := [unit-resolution #886 #883 #881]: false
#888 := [lemma #887]: #884
#744 := (or #743 #741)
#745 := [def-axiom]: #744
#894 := [unit-resolution #745 #888]: #743
#930 := [hypothesis]: #736
#935 := (or #489 #574)
#931 := [unit-resolution #740 #930]: #735
#893 := [hypothesis]: #872
#915 := [hypothesis]: #735
#916 := [unit-resolution #867 #915 #893]: false
#917 := [lemma #916]: #866
#932 := [unit-resolution #917 #931]: #756
#749 := (+ #613 #624)
#844 := (>= #749 0::real)
#742 := (= #613 #621)
#746 := (or #614 #742)
#747 := [def-axiom]: #746
#895 := [unit-resolution #747 #894]: #742
#896 := (not #742)
#897 := (or #896 #844)
#898 := [th-lemma]: #897
#899 := [unit-resolution #898 #895]: #844
#913 := (or #872 #260)
#900 := [hypothesis]: #756
#646 := [and-elim #513]: #500
#903 := (not #844)
#902 := (not #533)
#901 := (not #500)
#904 := (or #489 #901 #260 #872 #840 #277 #590 #902 #903 #633)
#905 := [th-lemma]: #904
#906 := [unit-resolution #905 #900 #806 #646 #648 #650 #651 #808 #642 #899]: #489
#722 := (not #489)
#723 := (or #722 #720)
#724 := [def-axiom]: #723
#907 := [unit-resolution #724 #906]: #720
#908 := (not #720)
#909 := (or #908 #892)
#910 := [th-lemma]: #909
#911 := [unit-resolution #910 #907]: #892
#912 := [th-lemma #911 #646 #900 #808 #650 #648 #899 #651 #644 #642]: false
#914 := [lemma #912]: #913
#890 := [unit-resolution #914 #806]: #872
#918 := [unit-resolution #917 #890]: #865
#919 := [unit-resolution #740 #918]: #574
#920 := (or #489 #901 #260 #902 #903 #633 #840 #277 #736)
#921 := [th-lemma]: #920
#922 := [unit-resolution #921 #806 #642 #646 #648 #919 #651 #808 #899]: #489
#923 := [unit-resolution #724 #922]: #720
#924 := [unit-resolution #910 #923]: #892
#925 := [th-lemma #924 #646 #806 #648 #899 #651 #808 #919 #644 #642]: false
#926 := [lemma #925]: #260
#933 := [hypothesis]: #722
#934 := [th-lemma #646 #933 #926 #648 #899 #651 #932 #650 #930]: false
#936 := [lemma #934]: #935
#927 := [unit-resolution #936 #930]: #489
#928 := [unit-resolution #724 #927]: #720
#929 := [unit-resolution #910 #928]: #892
#937 := [th-lemma #929 #644 #926 #932 #650 #646 #648 #899 #651 #927]: false
#938 := [lemma #937]: #574
#940 := (or #489 #261 #614 #901 #902 #736)
#941 := [th-lemma]: #940
#942 := [unit-resolution #941 #926 #646 #648 #938 #894]: #489
#943 := [unit-resolution #724 #942]: #720
#944 := [unit-resolution #910 #943]: #892
#760 := (+ #167 #275)
#819 := (<= #760 0::real)
#707 := (= #167 #267)
#709 := (or #261 #707)
#710 := [def-axiom]: #709
#945 := [unit-resolution #710 #926]: #707
#946 := (not #707)
#947 := (or #946 #819)
#948 := [th-lemma]: #947
#949 := [unit-resolution #948 #945]: #819
[th-lemma #926 #949 #646 #648 #899 #651 #938 #944 #644 #642]: false
unsat