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