src/HOL/Multivariate_Analysis/Integration.certs

updated SMT certificates

8d81ff6f41bc1cff9f5c6454ee204d147f8e27b7 272 0
#2 := false
#48 := 0::Real
decl f17 :: (-> S3 S10 Real)
decl f18 :: S10
#43 := f18
decl f4 :: S3
#8 := f4
#58 := (f17 f4 f18)
#94 := -1::Real
#138 := (* -1::Real #58)
decl f5 :: (-> S4 S5 Real)
decl f8 :: S5
#14 := f8
decl f20 :: S4
#54 := f20
#55 := (f5 f20 f8)
#139 := (+ #55 #138)
#122 := (* -1::Real #55)
#129 := (+ #122 #58)
#189 := (<= #139 0::Real)
#196 := (ite #189 #129 #139)
#372 := (* -1::Real #196)
#373 := (+ #129 #372)
#374 := (<= #373 0::Real)
#356 := (= #129 #196)
decl f19 :: S4
#45 := f19
#46 := (f5 f19 f8)
decl f9 :: S3
#18 := f9
#44 := (f17 f9 f18)
#105 := (* -1::Real #44)
#106 := (+ #105 #46)
#95 := (* -1::Real #46)
#96 := (+ #44 #95)
#224 := (>= #96 0::Real)
#231 := (ite #224 #96 #106)
#368 := (* -1::Real #231)
#371 := (+ #106 #368)
#375 := (<= #371 0::Real)
#363 := (= #106 #231)
#225 := (not #224)
#376 := [hypothesis]: #224
#182 := (+ #44 #138)
#183 := (<= #182 0::Real)
#207 := -3::Real
#242 := (* -3::Real #231)
#243 := (+ #122 #242)
#244 := (+ #46 #243)
#245 := (<= #244 0::Real)
#208 := (* -3::Real #196)
#209 := (+ #122 #208)
#210 := (+ #46 #209)
#211 := (<= #210 0::Real)
#186 := (not #183)
#264 := (or #186 #211 #245)
#269 := (not #264)
#65 := (<= #44 #58)
#66 := (implies #65 false)
#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)
#67 := (implies #64 #66)
#47 := (- #44 #46)
#50 := (- #47)
#49 := (< #47 0::Real)
#51 := (ite #49 #50 #47)
#53 := (* #51 3::Real)
#57 := (< #53 #56)
#68 := (implies #57 #67)
#69 := (not #68)
#272 := (iff #69 #269)
#123 := (+ #46 #122)
#132 := (< #129 0::Real)
#144 := (ite #132 #139 #129)
#150 := (* 3::Real #144)
#155 := (< #150 #123)
#164 := (not #155)
#158 := (not #65)
#165 := (or #158 #164)
#99 := (< #96 0::Real)
#111 := (ite #99 #106 #96)
#117 := (* 3::Real #111)
#126 := (< #117 #123)
#173 := (not #126)
#174 := (or #173 #165)
#179 := (not #174)
#270 := (iff #179 #269)
#267 := (iff #174 #264)
#258 := (or #186 #211)
#261 := (or #245 #258)
#265 := (iff #261 #264)
#266 := [rewrite]: #265
#262 := (iff #174 #261)
#259 := (iff #165 #258)
#222 := (iff #164 #211)
#212 := (not #211)
#217 := (not #212)
#220 := (iff #217 #211)
#221 := [rewrite]: #220
#218 := (iff #164 #217)
#215 := (iff #155 #212)
#201 := (* 3::Real #196)
#204 := (< #201 #123)
#213 := (iff #204 #212)
#214 := [rewrite]: #213
#205 := (iff #155 #204)
#202 := (= #150 #201)
#199 := (= #144 #196)
#190 := (not #189)
#193 := (ite #190 #139 #129)
#197 := (= #193 #196)
#198 := [rewrite]: #197
#194 := (= #144 #193)
#191 := (iff #132 #190)
#192 := [rewrite]: #191
#195 := [monotonicity #192]: #194
#200 := [trans #195 #198]: #199
#203 := [monotonicity #200]: #202
#206 := [monotonicity #203]: #205
#216 := [trans #206 #214]: #215
#219 := [monotonicity #216]: #218
#223 := [trans #219 #221]: #222
#187 := (iff #158 #186)
#184 := (iff #65 #183)
#185 := [rewrite]: #184
#188 := [monotonicity #185]: #187
#260 := [monotonicity #188 #223]: #259
#256 := (iff #173 #245)
#246 := (not #245)
#251 := (not #246)
#254 := (iff #251 #245)
#255 := [rewrite]: #254
#252 := (iff #173 #251)
#249 := (iff #126 #246)
#236 := (* 3::Real #231)
#239 := (< #236 #123)
#247 := (iff #239 #246)
#248 := [rewrite]: #247
#240 := (iff #126 #239)
#237 := (= #117 #236)
#234 := (= #111 #231)
#228 := (ite #225 #106 #96)
#232 := (= #228 #231)
#233 := [rewrite]: #232
#229 := (= #111 #228)
#226 := (iff #99 #225)
#227 := [rewrite]: #226
#230 := [monotonicity #227]: #229
#235 := [trans #230 #233]: #234
#238 := [monotonicity #235]: #237
#241 := [monotonicity #238]: #240
#250 := [trans #241 #248]: #249
#253 := [monotonicity #250]: #252
#257 := [trans #253 #255]: #256
#263 := [monotonicity #257 #260]: #262
#268 := [trans #263 #266]: #267
#271 := [monotonicity #268]: #270
#180 := (iff #69 #179)
#177 := (iff #68 #174)
#170 := (implies #126 #165)
#175 := (iff #170 #174)
#176 := [rewrite]: #175
#171 := (iff #68 #170)
#168 := (iff #67 #165)
#161 := (implies #155 #158)
#166 := (iff #161 #165)
#167 := [rewrite]: #166
#162 := (iff #67 #161)
#159 := (iff #66 #158)
#160 := [rewrite]: #159
#156 := (iff #64 #155)
#124 := (= #56 #123)
#125 := [rewrite]: #124
#153 := (= #63 #150)
#147 := (* #144 3::Real)
#151 := (= #147 #150)
#152 := [rewrite]: #151
#148 := (= #63 #147)
#145 := (= #62 #144)
#130 := (= #59 #129)
#131 := [rewrite]: #130
#142 := (= #61 #139)
#135 := (- #129)
#140 := (= #135 #139)
#141 := [rewrite]: #140
#136 := (= #61 #135)
#137 := [monotonicity #131]: #136
#143 := [trans #137 #141]: #142
#133 := (iff #60 #132)
#134 := [monotonicity #131]: #133
#146 := [monotonicity #134 #143 #131]: #145
#149 := [monotonicity #146]: #148
#154 := [trans #149 #152]: #153
#157 := [monotonicity #154 #125]: #156
#163 := [monotonicity #157 #160]: #162
#169 := [trans #163 #167]: #168
#127 := (iff #57 #126)
#120 := (= #53 #117)
#114 := (* #111 3::Real)
#118 := (= #114 #117)
#119 := [rewrite]: #118
#115 := (= #53 #114)
#112 := (= #51 #111)
#97 := (= #47 #96)
#98 := [rewrite]: #97
#109 := (= #50 #106)
#102 := (- #96)
#107 := (= #102 #106)
#108 := [rewrite]: #107
#103 := (= #50 #102)
#104 := [monotonicity #98]: #103
#110 := [trans #104 #108]: #109
#100 := (iff #49 #99)
#101 := [monotonicity #98]: #100
#113 := [monotonicity #101 #110 #98]: #112
#116 := [monotonicity #113]: #115
#121 := [trans #116 #119]: #120
#128 := [monotonicity #121 #125]: #127
#172 := [monotonicity #128 #169]: #171
#178 := [trans #172 #176]: #177
#181 := [monotonicity #178]: #180
#273 := [trans #181 #271]: #272
#93 := [asserted]: #69
#274 := [mp #93 #273]: #269
#275 := [not-or-elim #274]: #183
#277 := [not-or-elim #274]: #246
#369 := (+ #96 #368)
#370 := (<= #369 0::Real)
#362 := (= #96 #231)
#364 := (or #225 #362)
#365 := [def-axiom]: #364
#388 := [unit-resolution #365 #376]: #362
#389 := (not #362)
#390 := (or #389 #370)
#391 := [th-lemma arith triangle-eq]: #390
#392 := [unit-resolution #391 #388]: #370
#384 := (or #190 #225)
#377 := [hypothesis]: #189
#276 := [not-or-elim #274]: #212
#358 := (or #190 #356)
#359 := [def-axiom]: #358
#378 := [unit-resolution #359 #377]: #356
#379 := (not #356)
#380 := (or #379 #374)
#381 := [th-lemma arith triangle-eq]: #380
#382 := [unit-resolution #381 #378]: #374
#383 := [th-lemma arith farkas -1 -3 1 -2 1 #275 #382 #276 #377 #376]: false
#385 := [lemma #383]: #384
#393 := [unit-resolution #385 #376]: #190
#394 := [th-lemma arith farkas 1/4 -3/4 1/4 -1/4 1 #393 #392 #277 #275 #376]: false
#395 := [lemma #394]: #225
#366 := (or #224 #363)
#367 := [def-axiom]: #366
#396 := [unit-resolution #367 #395]: #363
#397 := (not #363)
#398 := (or #397 #375)
#399 := [th-lemma arith triangle-eq]: #398
#400 := [unit-resolution #399 #396]: #375
#401 := (not #375)
#402 := (or #189 #401 #245 #186 #224)
#403 := [th-lemma arith assign-bounds 3 1 1 2]: #402
#404 := [unit-resolution #403 #275 #395 #277 #400]: #189
#405 := [unit-resolution #359 #404]: #356
#406 := [unit-resolution #381 #405]: #374
[th-lemma arith farkas 2 2/3 1 1 1/3 1 #400 #277 #275 #395 #276 #406]: false
unsat
a66e77fbacece8ec9b71617769b478381e4da6e9 349 0
#2 := false
#11 := 0::Real
decl ?v3!0 :: Real
#227 := ?v3!0
decl ?v0!3 :: Real
#226 := ?v0!3
#48 := -1::Real
#229 := (* -1::Real ?v0!3)
#230 := (+ #229 ?v3!0)
#231 := (* -1::Real ?v3!0)
#232 := (+ ?v0!3 #231)
#233 := (>= #232 0::Real)
#234 := (ite #233 #232 #230)
#235 := (* -1::Real #234)
#394 := (+ #230 #235)
#395 := (<= #394 0::Real)
#378 := (= #230 #234)
#379 := (not #233)
decl ?v2!1 :: Real
#228 := ?v2!1
decl ?v1!2 :: Real
#225 := ?v1!2
#241 := (* -1::Real ?v1!2)
#278 := (+ #241 ?v2!1)
#243 := (* -1::Real ?v2!1)
#284 := (+ ?v1!2 #243)
#285 := (>= #284 0::Real)
#292 := (ite #285 #284 #278)
#295 := (* -1::Real #292)
#393 := (+ #278 #295)
#396 := (<= #393 0::Real)
#385 := (= #278 #292)
#386 := (not #285)
#397 := [hypothesis]: #285
#405 := (or #379 #386)
#77 := -1/3::Real
#236 := (* -1/3::Real ?v2!1)
#298 := (+ #236 #295)
#75 := 1/3::Real
#238 := (* 1/3::Real ?v3!0)
#301 := (+ #238 #298)
#304 := (<= #301 0::Real)
#320 := (not #304)
#269 := (+ ?v1!2 #229)
#270 := (>= #269 0::Real)
#275 := (not #270)
#237 := (+ #236 #235)
#239 := (+ #238 #237)
#240 := (<= #239 0::Real)
#310 := (or #240 #275 #304)
#315 := (not #310)
#242 := (+ ?v2!1 #241)
#244 := (+ #243 ?v1!2)
#245 := (<= #242 0::Real)
#246 := (ite #245 #244 #242)
#247 := (* -1::Real #246)
#248 := (+ #236 #247)
#249 := (+ #238 #248)
#250 := (<= #249 0::Real)
#251 := (+ ?v0!3 #241)
#252 := (<= #251 0::Real)
#253 := (not #252)
#254 := (or #253 #250 #240)
#255 := (not #254)
#316 := (iff #255 #315)
#313 := (iff #254 #310)
#307 := (or #275 #304 #240)
#311 := (iff #307 #310)
#312 := [rewrite]: #311
#308 := (iff #254 #307)
#305 := (iff #250 #304)
#302 := (= #249 #301)
#299 := (= #248 #298)
#296 := (= #247 #295)
#293 := (= #246 #292)
#279 := (= #242 #278)
#280 := [rewrite]: #279
#290 := (= #244 #284)
#291 := [rewrite]: #290
#288 := (iff #245 #285)
#281 := (<= #278 0::Real)
#286 := (iff #281 #285)
#287 := [rewrite]: #286
#282 := (iff #245 #281)
#283 := [monotonicity #280]: #282
#289 := [trans #283 #287]: #288
#294 := [monotonicity #289 #291 #280]: #293
#297 := [monotonicity #294]: #296
#300 := [monotonicity #297]: #299
#303 := [monotonicity #300]: #302
#306 := [monotonicity #303]: #305
#276 := (iff #253 #275)
#273 := (iff #252 #270)
#263 := (+ #241 ?v0!3)
#266 := (<= #263 0::Real)
#271 := (iff #266 #270)
#272 := [rewrite]: #271
#267 := (iff #252 #266)
#264 := (= #251 #263)
#265 := [rewrite]: #264
#268 := [monotonicity #265]: #267
#274 := [trans #268 #272]: #273
#277 := [monotonicity #274]: #276
#309 := [monotonicity #277 #306]: #308
#314 := [trans #309 #312]: #313
#317 := [monotonicity #314]: #316
#9 := (:var 0 Real)
#8 := (:var 3 Real)
#59 := (* -1::Real #8)
#60 := (+ #59 #9)
#49 := (* -1::Real #9)
#50 := (+ #8 #49)
#173 := (>= #50 0::Real)
#180 := (ite #173 #50 #60)
#188 := (* -1::Real #180)
#15 := (:var 1 Real)
#78 := (* -1/3::Real #15)
#189 := (+ #78 #188)
#76 := (* 1/3::Real #9)
#190 := (+ #76 #189)
#191 := (<= #190 0::Real)
#20 := (:var 2 Real)
#96 := (* -1::Real #20)
#97 := (+ #15 #96)
#68 := (* -1::Real #15)
#87 := (+ #68 #20)
#142 := (<= #97 0::Real)
#149 := (ite #142 #87 #97)
#157 := (* -1::Real #149)
#158 := (+ #78 #157)
#159 := (+ #76 #158)
#160 := (<= #159 0::Real)
#135 := (+ #8 #96)
#136 := (<= #135 0::Real)
#139 := (not #136)
#210 := (or #139 #160 #191)
#215 := (forall (vars (?v0 Real) (?v1 Real) (?v2 Real) (?v3 Real)) #210)
#218 := (not #215)
#256 := (~ #218 #255)
#257 := [sk]: #256
#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)
#221 := (iff #31 #218)
#79 := (+ #76 #78)
#90 := (< #87 0::Real)
#102 := (ite #90 #97 #87)
#105 := (< #102 #79)
#114 := (not #105)
#108 := (not #26)
#115 := (or #108 #114)
#53 := (< #50 0::Real)
#65 := (ite #53 #60 #50)
#84 := (< #65 #79)
#123 := (not #84)
#124 := (or #123 #115)
#129 := (forall (vars (?v0 Real) (?v1 Real) (?v2 Real) (?v3 Real)) #124)
#132 := (not #129)
#219 := (iff #132 #218)
#216 := (iff #129 #215)
#213 := (iff #124 #210)
#204 := (or #139 #160)
#207 := (or #191 #204)
#211 := (iff #207 #210)
#212 := [rewrite]: #211
#208 := (iff #124 #207)
#205 := (iff #115 #204)
#171 := (iff #114 #160)
#161 := (not #160)
#166 := (not #161)
#169 := (iff #166 #160)
#170 := [rewrite]: #169
#167 := (iff #114 #166)
#164 := (iff #105 #161)
#154 := (< #149 #79)
#162 := (iff #154 #161)
#163 := [rewrite]: #162
#155 := (iff #105 #154)
#152 := (= #102 #149)
#143 := (not #142)
#146 := (ite #143 #97 #87)
#150 := (= #146 #149)
#151 := [rewrite]: #150
#147 := (= #102 #146)
#144 := (iff #90 #143)
#145 := [rewrite]: #144
#148 := [monotonicity #145]: #147
#153 := [trans #148 #151]: #152
#156 := [monotonicity #153]: #155
#165 := [trans #156 #163]: #164
#168 := [monotonicity #165]: #167
#172 := [trans #168 #170]: #171
#140 := (iff #108 #139)
#137 := (iff #26 #136)
#138 := [rewrite]: #137
#141 := [monotonicity #138]: #140
#206 := [monotonicity #141 #172]: #205
#202 := (iff #123 #191)
#192 := (not #191)
#197 := (not #192)
#200 := (iff #197 #191)
#201 := [rewrite]: #200
#198 := (iff #123 #197)
#195 := (iff #84 #192)
#185 := (< #180 #79)
#193 := (iff #185 #192)
#194 := [rewrite]: #193
#186 := (iff #84 #185)
#183 := (= #65 #180)
#174 := (not #173)
#177 := (ite #174 #60 #50)
#181 := (= #177 #180)
#182 := [rewrite]: #181
#178 := (= #65 #177)
#175 := (iff #53 #174)
#176 := [rewrite]: #175
#179 := [monotonicity #176]: #178
#184 := [trans #179 #182]: #183
#187 := [monotonicity #184]: #186
#196 := [trans #187 #194]: #195
#199 := [monotonicity #196]: #198
#203 := [trans #199 #201]: #202
#209 := [monotonicity #203 #206]: #208
#214 := [trans #209 #212]: #213
#217 := [quant-intro #214]: #216
#220 := [monotonicity #217]: #219
#133 := (iff #31 #132)
#130 := (iff #30 #129)
#127 := (iff #29 #124)
#120 := (implies #84 #115)
#125 := (iff #120 #124)
#126 := [rewrite]: #125
#121 := (iff #29 #120)
#118 := (iff #28 #115)
#111 := (implies #105 #108)
#116 := (iff #111 #115)
#117 := [rewrite]: #116
#112 := (iff #28 #111)
#109 := (iff #27 #108)
#110 := [rewrite]: #109
#106 := (iff #25 #105)
#82 := (= #18 #79)
#69 := (+ #9 #68)
#72 := (/ #69 3::Real)
#80 := (= #72 #79)
#81 := [rewrite]: #80
#73 := (= #18 #72)
#70 := (= #16 #69)
#71 := [rewrite]: #70
#74 := [monotonicity #71]: #73
#83 := [trans #74 #81]: #82
#103 := (= #24 #102)
#88 := (= #21 #87)
#89 := [rewrite]: #88
#100 := (= #23 #97)
#93 := (- #87)
#98 := (= #93 #97)
#99 := [rewrite]: #98
#94 := (= #23 #93)
#95 := [monotonicity #89]: #94
#101 := [trans #95 #99]: #100
#91 := (iff #22 #90)
#92 := [monotonicity #89]: #91
#104 := [monotonicity #92 #101 #89]: #103
#107 := [monotonicity #104 #83]: #106
#113 := [monotonicity #107 #110]: #112
#119 := [trans #113 #117]: #118
#85 := (iff #19 #84)
#66 := (= #14 #65)
#51 := (= #10 #50)
#52 := [rewrite]: #51
#63 := (= #13 #60)
#56 := (- #50)
#61 := (= #56 #60)
#62 := [rewrite]: #61
#57 := (= #13 #56)
#58 := [monotonicity #52]: #57
#64 := [trans #58 #62]: #63
#54 := (iff #12 #53)
#55 := [monotonicity #52]: #54
#67 := [monotonicity #55 #64 #52]: #66
#86 := [monotonicity #67 #83]: #85
#122 := [monotonicity #86 #119]: #121
#128 := [trans #122 #126]: #127
#131 := [quant-intro #128]: #130
#134 := [monotonicity #131]: #133
#222 := [trans #134 #220]: #221
#47 := [asserted]: #31
#223 := [mp #47 #222]: #218
#260 := [mp~ #223 #257]: #255
#261 := [mp #260 #317]: #315
#321 := [not-or-elim #261]: #320
#391 := (+ #284 #295)
#392 := (<= #391 0::Real)
#384 := (= #284 #292)
#387 := (or #386 #384)
#388 := [def-axiom]: #387
#398 := [unit-resolution #388 #397]: #384
#399 := (not #384)
#400 := (or #399 #392)
#401 := [th-lemma arith triangle-eq]: #400
#402 := [unit-resolution #401 #398]: #392
#403 := [hypothesis]: #233
#319 := [not-or-elim #261]: #270
#404 := [th-lemma arith farkas 1/2 1/2 3/2 3/2 1 #319 #403 #402 #321 #397]: false
#406 := [lemma #404]: #405
#407 := [unit-resolution #406 #397]: #379
#262 := (not #240)
#318 := [not-or-elim #261]: #262
#382 := (or #233 #378)
#383 := [def-axiom]: #382
#408 := [unit-resolution #383 #407]: #378
#409 := (not #378)
#410 := (or #409 #395)
#411 := [th-lemma arith triangle-eq]: #410
#412 := [unit-resolution #411 #408]: #395
#413 := [th-lemma arith farkas 2 2 1 1 1 1 #412 #318 #402 #321 #319 #407]: false
#414 := [lemma #413]: #386
#389 := (or #285 #385)
#390 := [def-axiom]: #389
#417 := [unit-resolution #390 #414]: #385
#418 := (not #385)
#419 := (or #418 #396)
#420 := [th-lemma arith triangle-eq]: #419
#421 := [unit-resolution #420 #417]: #396
#422 := (not #396)
#423 := (or #379 #422 #275 #304 #285)
#424 := [th-lemma arith assign-bounds 3 1 3 4]: #423
#425 := [unit-resolution #424 #319 #414 #321 #421]: #379
#426 := [unit-resolution #383 #425]: #378
#427 := [unit-resolution #411 #426]: #395
[th-lemma arith farkas 2 1 2 3 1 1 #421 #319 #321 #414 #318 #427]: false
unsat
f26ffd00d169b6b4684265a03d23c9e0efe94a58 57 0
#2 := false
#37 := 0::Real
decl f12 :: (-> S5 Real)
decl f13 :: (-> S4 S4 S5)
decl f14 :: (-> S3 S4)
decl f10 :: S3
#25 := f10
#45 := (f14 f10)
decl f4 :: S3
#8 := f4
#44 := (f14 f4)
#46 := (f13 #44 #45)
#47 := (f12 #46)
#258 := (>= #47 0::Real)
#260 := (not #258)
#49 := (= #47 0::Real)
#50 := (not #49)
#134 := [asserted]: #50
#266 := (or #49 #260)
#48 := (<= #47 0::Real)
#114 := [asserted]: #48
#259 := (not #48)
#264 := (or #49 #259 #260)
#265 := [th-lemma arith triangle-eq]: #264
#267 := [unit-resolution #265 #114]: #266
#268 := [unit-resolution #267 #134]: #260
#39 := (:var 0 S4)
#38 := (:var 1 S4)
#40 := (f13 #38 #39)
#251 := (pattern #40)
#41 := (f12 #40)
#136 := (>= #41 0::Real)
#252 := (forall (vars (?v0 S4) (?v1 S4)) (:pat #251) #136)
#138 := (forall (vars (?v0 S4) (?v1 S4)) #136)
#255 := (iff #138 #252)
#253 := (iff #136 #136)
#254 := [refl]: #253
#256 := [quant-intro #254]: #255
#165 := (~ #138 #138)
#153 := (~ #136 #136)
#154 := [refl]: #153
#166 := [nnf-pos #154]: #165
#42 := (<= 0::Real #41)
#43 := (forall (vars (?v0 S4) (?v1 S4)) #42)
#139 := (iff #43 #138)
#135 := (iff #42 #136)
#137 := [rewrite]: #135
#140 := [quant-intro #137]: #139
#113 := [asserted]: #43
#141 := [mp #113 #140]: #138
#167 := [mp~ #141 #166]: #138
#257 := [mp #167 #256]: #252
#261 := (not #252)
#262 := (or #261 #258)
#263 := [quant-inst #44 #45]: #262
[unit-resolution #263 #257 #268]: false
unsat
fe6d352e9186ccd9319b5d4bd3ff26ab342ba6c4 351 0
#2 := false
#8 := 0::Real
decl f7 :: (-> S4 S2 Real)
decl f10 :: S2
#25 := f10
decl f8 :: S4
#17 := f8
#32 := (f7 f8 f10)
decl f11 :: S4
#29 := f11
#30 := (f7 f11 f10)
#100 := -1::Real
#136 := (* -1::Real #30)
#137 := (+ #136 #32)
decl f3 :: Real
#9 := f3
#197 := (* -1::Real #32)
#198 := (+ #30 #197)
#199 := (+ f3 #198)
#200 := (<= #199 0::Real)
#203 := (ite #200 f3 #137)
#630 := (* -1::Real #203)
#631 := (+ f3 #630)
#632 := (<= #631 0::Real)
#639 := (not #632)
#127 := 1/2::Real
#206 := (* 1/2::Real #203)
#494 := (<= #206 0::Real)
#217 := (= #206 0::Real)
#234 := (<= #198 0::Real)
decl f9 :: S4
#19 := f9
#28 := (f7 f9 f10)
#230 := (+ #28 #136)
#231 := (<= #230 0::Real)
#237 := (and #231 #234)
#53 := 0::Int
decl f4 :: (-> S2 Int)
#26 := (f4 f10)
#93 := -1::Int
#117 := (* -1::Int #26)
decl f5 :: (-> S3 S2)
decl f6 :: S3
#13 := f6
#14 := (f5 f6)
#15 := (f4 #14)
#118 := (+ #15 #117)
#119 := (<= #118 0::Int)
#240 := (or #119 #237)
#243 := (not #240)
#220 := (not #217)
#129 := (* 1/2::Real #32)
#194 := (+ #136 #129)
#128 := (* 1/2::Real #28)
#195 := (+ #128 #194)
#192 := (>= #195 0::Real)
#190 := (not #192)
#252 := (or #190 #220 #243)
#257 := (not #252)
#37 := 2::Real
#40 := (- #32 #30)
#41 := (<= f3 #40)
#42 := (ite #41 f3 #40)
#43 := (/ #42 2::Real)
#44 := (+ #30 #43)
#45 := (= #44 #30)
#46 := (not #45)
#36 := (+ #28 #32)
#38 := (/ #36 2::Real)
#39 := (<= #30 #38)
#47 := (implies #39 #46)
#33 := (<= #30 #32)
#31 := (<= #28 #30)
#34 := (and #31 #33)
#27 := (< #26 #15)
#35 := (implies #27 #34)
#48 := (implies #35 #47)
#49 := (not #48)
#260 := (iff #49 #257)
#140 := (<= f3 #137)
#143 := (ite #140 f3 #137)
#149 := (* 1/2::Real #143)
#154 := (+ #30 #149)
#160 := (= #30 #154)
#165 := (not #160)
#130 := (+ #128 #129)
#133 := (<= #30 #130)
#171 := (not #133)
#172 := (or #171 #165)
#116 := (not #27)
#124 := (or #116 #34)
#180 := (not #124)
#181 := (or #180 #172)
#186 := (not #181)
#258 := (iff #186 #257)
#255 := (iff #181 #252)
#246 := (or #190 #220)
#249 := (or #243 #246)
#253 := (iff #249 #252)
#254 := [rewrite]: #253
#250 := (iff #181 #249)
#247 := (iff #172 #246)
#221 := (iff #165 #220)
#218 := (iff #160 #217)
#209 := (+ #30 #206)
#212 := (= #30 #209)
#215 := (iff #212 #217)
#216 := [rewrite]: #215
#213 := (iff #160 #212)
#210 := (= #154 #209)
#207 := (= #149 #206)
#204 := (= #143 #203)
#201 := (iff #140 #200)
#202 := [rewrite]: #201
#205 := [monotonicity #202]: #204
#208 := [monotonicity #205]: #207
#211 := [monotonicity #208]: #210
#214 := [monotonicity #211]: #213
#219 := [trans #214 #216]: #218
#222 := [monotonicity #219]: #221
#193 := (iff #171 #190)
#189 := (iff #133 #192)
#191 := [rewrite]: #189
#196 := [monotonicity #191]: #193
#248 := [monotonicity #196 #222]: #247
#244 := (iff #180 #243)
#241 := (iff #124 #240)
#238 := (iff #34 #237)
#235 := (iff #33 #234)
#236 := [rewrite]: #235
#232 := (iff #31 #231)
#233 := [rewrite]: #232
#239 := [monotonicity #233 #236]: #238
#228 := (iff #116 #119)
#120 := (not #119)
#223 := (not #120)
#226 := (iff #223 #119)
#227 := [rewrite]: #226
#224 := (iff #116 #223)
#121 := (iff #27 #120)
#122 := [rewrite]: #121
#225 := [monotonicity #122]: #224
#229 := [trans #225 #227]: #228
#242 := [monotonicity #229 #239]: #241
#245 := [monotonicity #242]: #244
#251 := [monotonicity #245 #248]: #250
#256 := [trans #251 #254]: #255
#259 := [monotonicity #256]: #258
#187 := (iff #49 #186)
#184 := (iff #48 #181)
#177 := (implies #124 #172)
#182 := (iff #177 #181)
#183 := [rewrite]: #182
#178 := (iff #48 #177)
#175 := (iff #47 #172)
#168 := (implies #133 #165)
#173 := (iff #168 #172)
#174 := [rewrite]: #173
#169 := (iff #47 #168)
#166 := (iff #46 #165)
#163 := (iff #45 #160)
#157 := (= #154 #30)
#161 := (iff #157 #160)
#162 := [rewrite]: #161
#158 := (iff #45 #157)
#155 := (= #44 #154)
#152 := (= #43 #149)
#146 := (/ #143 2::Real)
#150 := (= #146 #149)
#151 := [rewrite]: #150
#147 := (= #43 #146)
#144 := (= #42 #143)
#138 := (= #40 #137)
#139 := [rewrite]: #138
#141 := (iff #41 #140)
#142 := [monotonicity #139]: #141
#145 := [monotonicity #142 #139]: #144
#148 := [monotonicity #145]: #147
#153 := [trans #148 #151]: #152
#156 := [monotonicity #153]: #155
#159 := [monotonicity #156]: #158
#164 := [trans #159 #162]: #163
#167 := [monotonicity #164]: #166
#134 := (iff #39 #133)
#131 := (= #38 #130)
#132 := [rewrite]: #131
#135 := [monotonicity #132]: #134
#170 := [monotonicity #135 #167]: #169
#176 := [trans #170 #174]: #175
#125 := (iff #35 #124)
#126 := [rewrite]: #125
#179 := [monotonicity #126 #176]: #178
#185 := [trans #179 #183]: #184
#188 := [monotonicity #185]: #187
#261 := [trans #188 #259]: #260
#92 := [asserted]: #49
#262 := [mp #92 #261]: #257
#264 := [not-or-elim #262]: #217
#634 := (or #220 #494)
#635 := [th-lemma arith triangle-eq]: #634
#636 := [unit-resolution #635 #264]: #494
#637 := [hypothesis]: #632
#87 := (<= f3 0::Real)
#88 := (not #87)
#10 := (< 0::Real f3)
#89 := (iff #10 #88)
#90 := [rewrite]: #89
#84 := [asserted]: #10
#91 := [mp #84 #90]: #88
#638 := [th-lemma arith farkas -1/2 1/2 1 #91 #637 #636]: false
#640 := [lemma #638]: #639
#487 := (= f3 #203)
#488 := (= #137 #203)
#649 := (not #488)
#633 := (+ #137 #630)
#641 := (<= #633 0::Real)
#646 := (not #641)
#565 := (+ #28 #197)
#566 := (>= #565 0::Real)
#571 := (not #566)
#86 := [asserted]: #27
#123 := [mp #86 #122]: #120
#11 := (:var 0 S2)
#20 := (f7 f9 #11)
#461 := (pattern #20)
#18 := (f7 f8 #11)
#460 := (pattern #18)
#12 := (f4 #11)
#459 := (pattern #12)
#101 := (* -1::Real #20)
#102 := (+ #18 #101)
#103 := (<= #102 0::Real)
#386 := (not #103)
#96 := (* -1::Int #15)
#97 := (+ #12 #96)
#95 := (>= #97 0::Int)
#387 := (or #95 #386)
#462 := (forall (vars (?v0 S2)) (:pat #459 #460 #461) #387)
#398 := (forall (vars (?v0 S2)) #387)
#465 := (iff #398 #462)
#463 := (iff #387 #387)
#464 := [refl]: #463
#466 := [quant-intro #464]: #465
#94 := (not #95)
#106 := (and #94 #103)
#378 := (not #106)
#377 := (forall (vars (?v0 S2)) #378)
#399 := (iff #377 #398)
#396 := (iff #378 #387)
#388 := (not #387)
#391 := (not #388)
#394 := (iff #391 #387)
#395 := [rewrite]: #394
#392 := (iff #378 #391)
#389 := (iff #106 #388)
#390 := [rewrite]: #389
#393 := [monotonicity #390]: #392
#397 := [trans #393 #395]: #396
#400 := [quant-intro #397]: #399
#109 := (exists (vars (?v0 S2)) #106)
#112 := (not #109)
#374 := (~ #112 #377)
#379 := (~ #378 #378)
#376 := [refl]: #379
#375 := [nnf-neg #376]: #374
#21 := (<= #18 #20)
#16 := (< #12 #15)
#22 := (and #16 #21)
#23 := (exists (vars (?v0 S2)) #22)
#24 := (not #23)
#113 := (iff #24 #112)
#110 := (iff #23 #109)
#107 := (iff #22 #106)
#104 := (iff #21 #103)
#105 := [rewrite]: #104
#98 := (iff #16 #94)
#99 := [rewrite]: #98
#108 := [monotonicity #99 #105]: #107
#111 := [quant-intro #108]: #110
#114 := [monotonicity #111]: #113
#85 := [asserted]: #24
#115 := [mp #85 #114]: #112
#372 := [mp~ #115 #375]: #377
#401 := [mp #372 #400]: #398
#467 := [mp #401 #466]: #462
#577 := (not #462)
#578 := (or #577 #119 #571)
#539 := (* -1::Real #28)
#540 := (+ #32 #539)
#544 := (<= #540 0::Real)
#545 := (not #544)
#546 := (+ #26 #96)
#547 := (>= #546 0::Int)
#548 := (or #547 #545)
#579 := (or #577 #548)
#586 := (iff #579 #578)
#574 := (or #119 #571)
#581 := (or #577 #574)
#584 := (iff #581 #578)
#585 := [rewrite]: #584
#582 := (iff #579 #581)
#575 := (iff #548 #574)
#572 := (iff #545 #571)
#569 := (iff #544 #566)
#559 := (+ #539 #32)
#562 := (<= #559 0::Real)
#567 := (iff #562 #566)
#568 := [rewrite]: #567
#563 := (iff #544 #562)
#560 := (= #540 #559)
#561 := [rewrite]: #560
#564 := [monotonicity #561]: #563
#570 := [trans #564 #568]: #569
#573 := [monotonicity #570]: #572
#557 := (iff #547 #119)
#549 := (+ #96 #26)
#552 := (>= #549 0::Int)
#555 := (iff #552 #119)
#556 := [rewrite]: #555
#553 := (iff #547 #552)
#550 := (= #546 #549)
#551 := [rewrite]: #550
#554 := [monotonicity #551]: #553
#558 := [trans #554 #556]: #557
#576 := [monotonicity #558 #573]: #575
#583 := [monotonicity #576]: #582
#587 := [trans #583 #585]: #586
#580 := [quant-inst #25]: #579
#588 := [mp #580 #587]: #578
#643 := [unit-resolution #588 #467 #123]: #571
#263 := [not-or-elim #262]: #192
#644 := [hypothesis]: #641
#645 := [th-lemma arith farkas 1/2 -1/2 1/4 1 #644 #263 #643 #636]: false
#647 := [lemma #645]: #646
#648 := [hypothesis]: #488
#650 := (or #649 #641)
#651 := [th-lemma arith triangle-eq]: #650
#652 := [unit-resolution #651 #648 #647]: false
#653 := [lemma #652]: #649
#492 := (or #200 #488)
#493 := [def-axiom]: #492
#654 := [unit-resolution #493 #653]: #200
#489 := (not #200)
#490 := (or #489 #487)
#491 := [def-axiom]: #490
#655 := [unit-resolution #491 #654]: #487
#656 := (not #487)
#657 := (or #656 #632)
#658 := [th-lemma arith triangle-eq]: #657
[unit-resolution #658 #655 #640]: false
unsat
7b7b29f11f061c77d0fa2db9bb640b09f44da643 331 0
#2 := false
#8 := 0::Real
decl f7 :: (-> S4 S2 Real)
decl f10 :: S2
#25 := f10
decl f11 :: S4
#29 := f11
#30 := (f7 f11 f10)
decl f9 :: S4
#19 := f9
#28 := (f7 f9 f10)
#107 := -1::Real
#167 := (* -1::Real #28)
#168 := (+ #167 #30)
decl f3 :: Real
#9 := f3
#146 := (* -1::Real #30)
#260 := (+ #28 #146)
#261 := (+ f3 #260)
#262 := (<= #261 0::Real)
#265 := (ite #262 f3 #168)
#707 := (* -1::Real #265)
#708 := (+ f3 #707)
#709 := (<= #708 0::Real)
#717 := (not #709)
#134 := 1/2::Real
#431 := (* 1/2::Real #265)
#572 := (<= #431 0::Real)
#432 := (= #431 0::Real)
#188 := -1/2::Real
#268 := (* -1/2::Real #265)
#271 := (+ #30 #268)
decl f8 :: S4
#17 := f8
#32 := (f7 f8 f10)
#147 := (+ #146 #32)
#245 := (* -1::Real #32)
#246 := (+ #30 #245)
#247 := (+ f3 #246)
#248 := (<= #247 0::Real)
#251 := (ite #248 f3 #147)
#254 := (* 1/2::Real #251)
#257 := (+ #30 #254)
#136 := (* 1/2::Real #32)
#234 := (+ #146 #136)
#135 := (* 1/2::Real #28)
#235 := (+ #135 #234)
#232 := (>= #235 0::Real)
#274 := (ite #232 #257 #271)
#277 := (= #30 #274)
#435 := (iff #277 #432)
#428 := (= #30 #271)
#433 := (iff #428 #432)
#434 := [rewrite]: #433
#429 := (iff #277 #428)
#426 := (= #274 #271)
#421 := (ite false #257 #271)
#424 := (= #421 #271)
#425 := [rewrite]: #424
#422 := (= #274 #421)
#419 := (iff #232 false)
#231 := (not #232)
#293 := (<= #246 0::Real)
#290 := (<= #260 0::Real)
#296 := (and #290 #293)
#60 := 0::Int
decl f4 :: (-> S2 Int)
#26 := (f4 f10)
#100 := -1::Int
#124 := (* -1::Int #26)
decl f5 :: (-> S3 S2)
decl f6 :: S3
#13 := f6
#14 := (f5 f6)
#15 := (f4 #14)
#125 := (+ #15 #124)
#126 := (<= #125 0::Int)
#299 := (or #126 #296)
#302 := (not #299)
#280 := (not #277)
#311 := (or #232 #280 #302)
#316 := (not #311)
#37 := 2::Real
#46 := (- #30 #28)
#47 := (<= f3 #46)
#48 := (ite #47 f3 #46)
#49 := (/ #48 2::Real)
#50 := (- #30 #49)
#41 := (- #32 #30)
#42 := (<= f3 #41)
#43 := (ite #42 f3 #41)
#44 := (/ #43 2::Real)
#45 := (+ #30 #44)
#36 := (+ #28 #32)
#38 := (/ #36 2::Real)
#40 := (<= #30 #38)
#51 := (ite #40 #45 #50)
#52 := (= #51 #30)
#53 := (not #52)
#39 := (< #38 #30)
#54 := (implies #39 #53)
#33 := (<= #30 #32)
#31 := (<= #28 #30)
#34 := (and #31 #33)
#27 := (< #26 #15)
#35 := (implies #27 #34)
#55 := (implies #35 #54)
#56 := (not #55)
#319 := (iff #56 #316)
#171 := (<= f3 #168)
#174 := (ite #171 f3 #168)
#189 := (* -1/2::Real #174)
#190 := (+ #30 #189)
#150 := (<= f3 #147)
#153 := (ite #150 f3 #147)
#159 := (* 1/2::Real #153)
#164 := (+ #30 #159)
#137 := (+ #135 #136)
#143 := (<= #30 #137)
#195 := (ite #143 #164 #190)
#201 := (= #30 #195)
#206 := (not #201)
#140 := (< #137 #30)
#212 := (not #140)
#213 := (or #212 #206)
#123 := (not #27)
#131 := (or #123 #34)
#221 := (not #131)
#222 := (or #221 #213)
#227 := (not #222)
#317 := (iff #227 #316)
#314 := (iff #222 #311)
#305 := (or #232 #280)
#308 := (or #302 #305)
#312 := (iff #308 #311)
#313 := [rewrite]: #312
#309 := (iff #222 #308)
#306 := (iff #213 #305)
#281 := (iff #206 #280)
#278 := (iff #201 #277)
#275 := (= #195 #274)
#272 := (= #190 #271)
#269 := (= #189 #268)
#266 := (= #174 #265)
#263 := (iff #171 #262)
#264 := [rewrite]: #263
#267 := [monotonicity #264]: #266
#270 := [monotonicity #267]: #269
#273 := [monotonicity #270]: #272
#258 := (= #164 #257)
#255 := (= #159 #254)
#252 := (= #153 #251)
#249 := (iff #150 #248)
#250 := [rewrite]: #249
#253 := [monotonicity #250]: #252
#256 := [monotonicity #253]: #255
#259 := [monotonicity #256]: #258
#244 := (iff #143 #232)
#243 := [rewrite]: #244
#276 := [monotonicity #243 #259 #273]: #275
#279 := [monotonicity #276]: #278
#282 := [monotonicity #279]: #281
#241 := (iff #212 #232)
#236 := (not #231)
#239 := (iff #236 #232)
#240 := [rewrite]: #239
#237 := (iff #212 #236)
#230 := (iff #140 #231)
#233 := [rewrite]: #230
#238 := [monotonicity #233]: #237
#242 := [trans #238 #240]: #241
#307 := [monotonicity #242 #282]: #306
#303 := (iff #221 #302)
#300 := (iff #131 #299)
#297 := (iff #34 #296)
#294 := (iff #33 #293)
#295 := [rewrite]: #294
#291 := (iff #31 #290)
#292 := [rewrite]: #291
#298 := [monotonicity #292 #295]: #297
#288 := (iff #123 #126)
#127 := (not #126)
#283 := (not #127)
#286 := (iff #283 #126)
#287 := [rewrite]: #286
#284 := (iff #123 #283)
#128 := (iff #27 #127)
#129 := [rewrite]: #128
#285 := [monotonicity #129]: #284
#289 := [trans #285 #287]: #288
#301 := [monotonicity #289 #298]: #300
#304 := [monotonicity #301]: #303
#310 := [monotonicity #304 #307]: #309
#315 := [trans #310 #313]: #314
#318 := [monotonicity #315]: #317
#228 := (iff #56 #227)
#225 := (iff #55 #222)
#218 := (implies #131 #213)
#223 := (iff #218 #222)
#224 := [rewrite]: #223
#219 := (iff #55 #218)
#216 := (iff #54 #213)
#209 := (implies #140 #206)
#214 := (iff #209 #213)
#215 := [rewrite]: #214
#210 := (iff #54 #209)
#207 := (iff #53 #206)
#204 := (iff #52 #201)
#198 := (= #195 #30)
#202 := (iff #198 #201)
#203 := [rewrite]: #202
#199 := (iff #52 #198)
#196 := (= #51 #195)
#193 := (= #50 #190)
#180 := (* 1/2::Real #174)
#185 := (- #30 #180)
#191 := (= #185 #190)
#192 := [rewrite]: #191
#186 := (= #50 #185)
#183 := (= #49 #180)
#177 := (/ #174 2::Real)
#181 := (= #177 #180)
#182 := [rewrite]: #181
#178 := (= #49 #177)
#175 := (= #48 #174)
#169 := (= #46 #168)
#170 := [rewrite]: #169
#172 := (iff #47 #171)
#173 := [monotonicity #170]: #172
#176 := [monotonicity #173 #170]: #175
#179 := [monotonicity #176]: #178
#184 := [trans #179 #182]: #183
#187 := [monotonicity #184]: #186
#194 := [trans #187 #192]: #193
#165 := (= #45 #164)
#162 := (= #44 #159)