src/HOL/Multivariate_Analysis/Integration.certs

make tracing an option

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
9e23136a6273b9d99bb60a03d2e785bc24c9efdf 59 0
#2 := false
#42 := 0::Real
decl f12 :: (-> S5 Real)
decl f13 :: (-> S4 S4 S5)
decl f14 :: (-> S6 S3 S4)
decl f4 :: S3
#8 := f4
decl f15 :: S6
#37 := f15
#39 := (f14 f15 f4)
decl f10 :: S3
#25 := f10
#38 := (f14 f15 f10)
#40 := (f13 #38 #39)
#41 := (f12 #40)
#249 := (>= #41 0::Real)
#251 := (not #249)
#50 := (= #41 0::Real)
#51 := (not #50)
#135 := [asserted]: #51
#257 := (or #50 #251)
#43 := (<= #41 0::Real)
#133 := [asserted]: #43
#250 := (not #43)
#255 := (or #50 #250 #251)
#256 := [th-lemma arith triangle-eq]: #255
#258 := [unit-resolution #256 #133]: #257
#259 := [unit-resolution #258 #135]: #251
#45 := (:var 0 S4)
#44 := (:var 1 S4)
#46 := (f13 #44 #45)
#242 := (pattern #46)
#47 := (f12 #46)
#138 := (>= #47 0::Real)
#243 := (forall (vars (?v0 S4) (?v1 S4)) (:pat #242) #138)
#140 := (forall (vars (?v0 S4) (?v1 S4)) #138)
#246 := (iff #140 #243)
#244 := (iff #138 #138)
#245 := [refl]: #244
#247 := [quant-intro #245]: #246
#156 := (~ #140 #140)
#144 := (~ #138 #138)
#145 := [refl]: #144
#157 := [nnf-pos #145]: #156
#48 := (<= 0::Real #47)
#49 := (forall (vars (?v0 S4) (?v1 S4)) #48)
#141 := (iff #49 #140)
#137 := (iff #48 #138)
#139 := [rewrite]: #137
#142 := [quant-intro #139]: #141
#134 := [asserted]: #49
#143 := [mp #134 #142]: #140
#158 := [mp~ #143 #157]: #140
#248 := [mp #158 #247]: #243
#252 := (not #243)
#253 := (or #252 #249)
#254 := [quant-inst #38 #39]: #253
[unit-resolution #254 #248 #259]: false
unsat
10ecdce54c6fd7d6b28756c68a32c55633241d44 222 0
#2 := false
#33 := 0::Real
decl f3 :: (-> S2 S3 Real)
decl f5 :: S3
#9 := f5
decl f12 :: S2
#25 := f12
#36 := (f3 f12 f5)
#105 := -1::Real
#351 := (* -1::Real #36)
decl f6 :: S2
#11 := f6
#12 := (f3 f6 f5)
#377 := (+ #12 #351)
#378 := (>= #377 0::Real)
#383 := (not #378)
decl f4 :: S2
#8 := f4
#10 := (f3 f4 f5)
#352 := (+ #10 #351)
#353 := (<= #352 0::Real)
#354 := (not #353)
#386 := (or #354 #383)
#389 := (not #386)
#21 := (:var 0 S3)
#28 := (f3 f6 #21)
#321 := (pattern #28)
#26 := (f3 f12 #21)
#320 := (pattern #26)
#24 := (f3 f4 #21)
#319 := (pattern #24)
decl f7 :: (-> S4 S3 Int)
decl f8 :: S4
#14 := f8
#22 := (f7 f8 #21)
#318 := (pattern #22)
#111 := (* -1::Real #28)
#112 := (+ #26 #111)
#113 := (<= #112 0::Real)
#249 := (not #113)
#106 := (* -1::Real #26)
#107 := (+ #24 #106)
#108 := (<= #107 0::Real)
#248 := (not #108)
#250 := (or #248 #249)
#251 := (not #250)
#43 := 0::Int
#78 := -1::Int
#92 := (* -1::Int #22)
decl f9 :: (-> S5 S6 S3)
decl f11 :: S6
#17 := f11
decl f10 :: S5
#16 := f10
#18 := (f9 f10 f11)
#19 := (f7 f8 #18)
#93 := (+ #19 #92)
#94 := (<= #93 0::Int)
#254 := (or #94 #251)
#322 := (forall (vars (?v0 S3)) (:pat #318 #319 #320 #321) #254)
#257 := (forall (vars (?v0 S3)) #254)
#325 := (iff #257 #322)
#323 := (iff #254 #254)
#324 := [refl]: #323
#326 := [quant-intro #324]: #325
#116 := (and #108 #113)
#119 := (or #94 #116)
#122 := (forall (vars (?v0 S3)) #119)
#258 := (iff #122 #257)
#255 := (iff #119 #254)
#252 := (iff #116 #251)
#253 := [rewrite]: #252
#256 := [monotonicity #253]: #255
#259 := [quant-intro #256]: #258
#242 := (~ #122 #122)
#244 := (~ #119 #119)
#245 := [refl]: #244
#243 := [nnf-pos #245]: #242
#29 := (<= #26 #28)
#27 := (<= #24 #26)
#30 := (and #27 #29)
#23 := (< #22 #19)
#31 := (implies #23 #30)
#32 := (forall (vars (?v0 S3)) #31)
#125 := (iff #32 #122)
#77 := (not #23)
#86 := (or #77 #30)
#89 := (forall (vars (?v0 S3)) #86)
#123 := (iff #89 #122)
#120 := (iff #86 #119)
#117 := (iff #30 #116)
#114 := (iff #29 #113)
#115 := [rewrite]: #114
#109 := (iff #27 #108)
#110 := [rewrite]: #109
#118 := [monotonicity #110 #115]: #117
#103 := (iff #77 #94)
#95 := (not #94)
#98 := (not #95)
#101 := (iff #98 #94)
#102 := [rewrite]: #101
#99 := (iff #77 #98)
#96 := (iff #23 #95)
#97 := [rewrite]: #96
#100 := [monotonicity #97]: #99
#104 := [trans #100 #102]: #103
#121 := [monotonicity #104 #118]: #120
#124 := [quant-intro #121]: #123
#90 := (iff #32 #89)
#87 := (iff #31 #86)
#88 := [rewrite]: #87
#91 := [quant-intro #88]: #90
#126 := [trans #91 #124]: #125
#76 := [asserted]: #32
#127 := [mp #76 #126]: #122
#240 := [mp~ #127 #243]: #122
#260 := [mp #240 #259]: #257
#327 := [mp #260 #326]: #322
#81 := (* -1::Int #19)
#15 := (f7 f8 f5)
#82 := (+ #15 #81)
#80 := (>= #82 0::Int)
#79 := (not #80)
#20 := (< #15 #19)
#83 := (iff #20 #79)
#84 := [rewrite]: #83
#75 := [asserted]: #20
#85 := [mp #75 #84]: #79
#395 := (not #322)
#396 := (or #395 #80 #389)
#347 := (* -1::Real #12)
#348 := (+ #36 #347)
#349 := (<= #348 0::Real)
#350 := (not #349)
#355 := (or #354 #350)
#356 := (not #355)
#357 := (* -1::Int #15)
#358 := (+ #19 #357)
#359 := (<= #358 0::Int)
#360 := (or #359 #356)
#397 := (or #395 #360)
#404 := (iff #397 #396)
#392 := (or #80 #389)
#399 := (or #395 #392)
#402 := (iff #399 #396)
#403 := [rewrite]: #402
#400 := (iff #397 #399)
#393 := (iff #360 #392)
#390 := (iff #356 #389)
#387 := (iff #355 #386)
#384 := (iff #350 #383)
#381 := (iff #349 #378)
#371 := (+ #347 #36)
#374 := (<= #371 0::Real)
#379 := (iff #374 #378)
#380 := [rewrite]: #379
#375 := (iff #349 #374)
#372 := (= #348 #371)
#373 := [rewrite]: #372
#376 := [monotonicity #373]: #375
#382 := [trans #376 #380]: #381
#385 := [monotonicity #382]: #384
#388 := [monotonicity #385]: #387
#391 := [monotonicity #388]: #390
#369 := (iff #359 #80)
#361 := (+ #357 #19)
#364 := (<= #361 0::Int)
#367 := (iff #364 #80)
#368 := [rewrite]: #367
#365 := (iff #359 #364)
#362 := (= #358 #361)
#363 := [rewrite]: #362
#366 := [monotonicity #363]: #365
#370 := [trans #366 #368]: #369
#394 := [monotonicity #370 #391]: #393
#401 := [monotonicity #394]: #400
#405 := [trans #401 #403]: #404
#398 := [quant-inst #9]: #397
#406 := [mp #398 #405]: #396
#533 := [unit-resolution #406 #85 #327]: #389
#409 := (or #386 #378)
#410 := [def-axiom]: #409
#534 := [unit-resolution #410 #533]: #378
#495 := (>= #352 0::Real)
#544 := (not #495)
#494 := (= #10 #36)
#539 := (not #494)
#130 := (= #12 #36)
#138 := (not #130)
#540 := (iff #138 #539)
#537 := (iff #130 #494)
#535 := (iff #494 #130)
#13 := (= #10 #12)
#74 := [asserted]: #13
#536 := [monotonicity #74]: #535
#538 := [symm #536]: #537
#541 := [monotonicity #538]: #540
#37 := (= #36 #12)
#38 := (not #37)
#139 := (iff #38 #138)
#136 := (iff #37 #130)
#137 := [rewrite]: #136
#140 := [monotonicity #137]: #139
#129 := [asserted]: #38
#143 := [mp #129 #140]: #138
#542 := [mp #143 #541]: #539
#547 := (or #494 #544)
#407 := (or #386 #353)
#408 := [def-axiom]: #407
#543 := [unit-resolution #408 #533]: #353
#545 := (or #494 #354 #544)
#546 := [th-lemma arith triangle-eq]: #545
#548 := [unit-resolution #546 #543]: #547
#549 := [unit-resolution #548 #542]: #544
#489 := (+ #10 #347)
#493 := (>= #489 0::Real)
#550 := (not #13)
#551 := (or #550 #493)
#552 := [th-lemma arith triangle-eq]: #551
#553 := [unit-resolution #552 #74]: #493
[th-lemma arith farkas 1 -1 1 #553 #549 #534]: false
unsat
c1e03e8f48834847dc1db09cf1e1405081da91b1 355 0
#2 := false
#8 := 0::Real
decl f9 :: (-> S6 S2 Real)
decl f12 :: S2
#27 := f12
decl f10 :: S6
#19 := f10
#34 := (f9 f10 f12)
decl f13 :: S6
#31 := f13
#32 := (f9 f13 f12)
#103 := -1::Real
#139 := (* -1::Real #32)
#140 := (+ #139 #34)
decl f3 :: Real
#9 := f3
#200 := (* -1::Real #34)
#201 := (+ #32 #200)
#202 := (+ f3 #201)
#203 := (<= #202 0::Real)
#206 := (ite #203 f3 #140)
#633 := (* -1::Real #206)
#634 := (+ f3 #633)
#635 := (<= #634 0::Real)
#642 := (not #635)
#130 := 1/2::Real
#209 := (* 1/2::Real #206)
#497 := (<= #209 0::Real)
#220 := (= #209 0::Real)
#237 := (<= #201 0::Real)
decl f11 :: S6
#21 := f11
#30 := (f9 f11 f12)
#233 := (+ #30 #139)
#234 := (<= #233 0::Real)
#240 := (and #234 #237)
#56 := 0::Int
decl f4 :: (-> S3 S2 Int)
decl f5 :: S3
#11 := f5
#28 := (f4 f5 f12)
#96 := -1::Int
#120 := (* -1::Int #28)
decl f6 :: (-> S4 S5 S2)
decl f8 :: S5
#15 := f8
decl f7 :: S4
#14 := f7
#16 := (f6 f7 f8)
#17 := (f4 f5 #16)
#121 := (+ #17 #120)
#122 := (<= #121 0::Int)
#243 := (or #122 #240)
#246 := (not #243)
#223 := (not #220)
#132 := (* 1/2::Real #34)
#197 := (+ #139 #132)
#131 := (* 1/2::Real #30)
#198 := (+ #131 #197)
#195 := (>= #198 0::Real)
#193 := (not #195)
#255 := (or #193 #223 #246)
#260 := (not #255)
#39 := 2::Real
#42 := (- #34 #32)
#43 := (<= f3 #42)
#44 := (ite #43 f3 #42)
#45 := (/ #44 2::Real)
#46 := (+ #32 #45)
#47 := (= #46 #32)
#48 := (not #47)
#38 := (+ #30 #34)
#40 := (/ #38 2::Real)
#41 := (<= #32 #40)
#49 := (implies #41 #48)
#35 := (<= #32 #34)
#33 := (<= #30 #32)
#36 := (and #33 #35)
#29 := (< #28 #17)
#37 := (implies #29 #36)
#50 := (implies #37 #49)
#51 := (not #50)
#263 := (iff #51 #260)
#143 := (<= f3 #140)
#146 := (ite #143 f3 #140)
#152 := (* 1/2::Real #146)
#157 := (+ #32 #152)
#163 := (= #32 #157)
#168 := (not #163)
#133 := (+ #131 #132)
#136 := (<= #32 #133)
#174 := (not #136)
#175 := (or #174 #168)
#119 := (not #29)
#127 := (or #119 #36)
#183 := (not #127)
#184 := (or #183 #175)
#189 := (not #184)
#261 := (iff #189 #260)
#258 := (iff #184 #255)
#249 := (or #193 #223)
#252 := (or #246 #249)
#256 := (iff #252 #255)
#257 := [rewrite]: #256
#253 := (iff #184 #252)
#250 := (iff #175 #249)
#224 := (iff #168 #223)
#221 := (iff #163 #220)
#212 := (+ #32 #209)
#215 := (= #32 #212)
#218 := (iff #215 #220)
#219 := [rewrite]: #218
#216 := (iff #163 #215)
#213 := (= #157 #212)
#210 := (= #152 #209)
#207 := (= #146 #206)
#204 := (iff #143 #203)
#205 := [rewrite]: #204
#208 := [monotonicity #205]: #207
#211 := [monotonicity #208]: #210
#214 := [monotonicity #211]: #213
#217 := [monotonicity #214]: #216
#222 := [trans #217 #219]: #221
#225 := [monotonicity #222]: #224
#196 := (iff #174 #193)
#192 := (iff #136 #195)
#194 := [rewrite]: #192
#199 := [monotonicity #194]: #196
#251 := [monotonicity #199 #225]: #250
#247 := (iff #183 #246)
#244 := (iff #127 #243)
#241 := (iff #36 #240)
#238 := (iff #35 #237)
#239 := [rewrite]: #238
#235 := (iff #33 #234)
#236 := [rewrite]: #235
#242 := [monotonicity #236 #239]: #241
#231 := (iff #119 #122)
#123 := (not #122)
#226 := (not #123)
#229 := (iff #226 #122)
#230 := [rewrite]: #229
#227 := (iff #119 #226)
#124 := (iff #29 #123)
#125 := [rewrite]: #124
#228 := [monotonicity #125]: #227
#232 := [trans #228 #230]: #231
#245 := [monotonicity #232 #242]: #244
#248 := [monotonicity #245]: #247
#254 := [monotonicity #248 #251]: #253
#259 := [trans #254 #257]: #258
#262 := [monotonicity #259]: #261
#190 := (iff #51 #189)
#187 := (iff #50 #184)
#180 := (implies #127 #175)
#185 := (iff #180 #184)
#186 := [rewrite]: #185
#181 := (iff #50 #180)
#178 := (iff #49 #175)
#171 := (implies #136 #168)
#176 := (iff #171 #175)
#177 := [rewrite]: #176
#172 := (iff #49 #171)
#169 := (iff #48 #168)
#166 := (iff #47 #163)
#160 := (= #157 #32)
#164 := (iff #160 #163)
#165 := [rewrite]: #164
#161 := (iff #47 #160)
#158 := (= #46 #157)
#155 := (= #45 #152)
#149 := (/ #146 2::Real)
#153 := (= #149 #152)
#154 := [rewrite]: #153
#150 := (= #45 #149)
#147 := (= #44 #146)
#141 := (= #42 #140)
#142 := [rewrite]: #141
#144 := (iff #43 #143)
#145 := [monotonicity #142]: #144
#148 := [monotonicity #145 #142]: #147
#151 := [monotonicity #148]: #150
#156 := [trans #151 #154]: #155
#159 := [monotonicity #156]: #158
#162 := [monotonicity #159]: #161
#167 := [trans #162 #165]: #166
#170 := [monotonicity #167]: #169
#137 := (iff #41 #136)
#134 := (= #40 #133)
#135 := [rewrite]: #134
#138 := [monotonicity #135]: #137
#173 := [monotonicity #138 #170]: #172
#179 := [trans #173 #177]: #178
#128 := (iff #37 #127)
#129 := [rewrite]: #128
#182 := [monotonicity #129 #179]: #181
#188 := [trans #182 #186]: #187
#191 := [monotonicity #188]: #190
#264 := [trans #191 #262]: #263
#95 := [asserted]: #51
#265 := [mp #95 #264]: #260
#267 := [not-or-elim #265]: #220
#637 := (or #223 #497)
#638 := [th-lemma arith triangle-eq]: #637
#639 := [unit-resolution #638 #267]: #497
#640 := [hypothesis]: #635
#90 := (<= f3 0::Real)
#91 := (not #90)
#10 := (< 0::Real f3)
#92 := (iff #10 #91)
#93 := [rewrite]: #92
#87 := [asserted]: #10
#94 := [mp #87 #93]: #91
#641 := [th-lemma arith farkas -1/2 1/2 1 #94 #640 #639]: false
#643 := [lemma #641]: #642
#490 := (= f3 #206)
#491 := (= #140 #206)
#652 := (not #491)
#636 := (+ #140 #633)
#644 := (<= #636 0::Real)
#649 := (not #644)
#568 := (+ #30 #200)
#569 := (>= #568 0::Real)
#574 := (not #569)
#89 := [asserted]: #29
#126 := [mp #89 #125]: #123
#12 := (:var 0 S2)
#22 := (f9 f11 #12)
#464 := (pattern #22)
#20 := (f9 f10 #12)
#463 := (pattern #20)
#13 := (f4 f5 #12)
#462 := (pattern #13)
#104 := (* -1::Real #22)
#105 := (+ #20 #104)
#106 := (<= #105 0::Real)
#389 := (not #106)
#99 := (* -1::Int #17)
#100 := (+ #13 #99)
#98 := (>= #100 0::Int)
#390 := (or #98 #389)
#465 := (forall (vars (?v0 S2)) (:pat #462 #463 #464) #390)
#401 := (forall (vars (?v0 S2)) #390)
#468 := (iff #401 #465)
#466 := (iff #390 #390)
#467 := [refl]: #466
#469 := [quant-intro #467]: #468
#97 := (not #98)
#109 := (and #97 #106)
#381 := (not #109)
#380 := (forall (vars (?v0 S2)) #381)
#402 := (iff #380 #401)
#399 := (iff #381 #390)
#391 := (not #390)
#394 := (not #391)
#397 := (iff #394 #390)
#398 := [rewrite]: #397
#395 := (iff #381 #394)
#392 := (iff #109 #391)
#393 := [rewrite]: #392
#396 := [monotonicity #393]: #395
#400 := [trans #396 #398]: #399
#403 := [quant-intro #400]: #402
#112 := (exists (vars (?v0 S2)) #109)
#115 := (not #112)
#377 := (~ #115 #380)
#382 := (~ #381 #381)
#379 := [refl]: #382
#378 := [nnf-neg #379]: #377
#23 := (<= #20 #22)
#18 := (< #13 #17)
#24 := (and #18 #23)
#25 := (exists (vars (?v0 S2)) #24)
#26 := (not #25)
#116 := (iff #26 #115)
#113 := (iff #25 #112)
#110 := (iff #24 #109)
#107 := (iff #23 #106)
#108 := [rewrite]: #107
#101 := (iff #18 #97)
#102 := [rewrite]: #101
#111 := [monotonicity #102 #108]: #110
#114 := [quant-intro #111]: #113
#117 := [monotonicity #114]: #116
#88 := [asserted]: #26
#118 := [mp #88 #117]: #115
#375 := [mp~ #118 #378]: #380
#404 := [mp #375 #403]: #401
#470 := [mp #404 #469]: #465
#580 := (not #465)
#581 := (or #580 #122 #574)
#542 := (* -1::Real #30)
#543 := (+ #34 #542)
#547 := (<= #543 0::Real)
#548 := (not #547)
#549 := (+ #28 #99)
#550 := (>= #549 0::Int)
#551 := (or #550 #548)
#582 := (or #580 #551)
#589 := (iff #582 #581)
#577 := (or #122 #574)
#584 := (or #580 #577)
#587 := (iff #584 #581)
#588 := [rewrite]: #587
#585 := (iff #582 #584)
#578 := (iff #551 #577)
#575 := (iff #548 #574)
#572 := (iff #547 #569)
#562 := (+ #542 #34)
#565 := (<= #562 0::Real)
#570 := (iff #565 #569)
#571 := [rewrite]: #570
#566 := (iff #547 #565)
#563 := (= #543 #562)
#564 := [rewrite]: #563
#567 := [monotonicity #564]: #566
#573 := [trans #567 #571]: #572
#576 := [monotonicity #573]: #575
#560 := (iff #550 #122)
#552 := (+ #99 #28)
#555 := (>= #552 0::Int)
#558 := (iff #555 #122)
#559 := [rewrite]: #558
#556 := (iff #550 #555)
#553 := (= #549 #552)
#554 := [rewrite]: #553
#557 := [monotonicity #554]: #556
#561 := [trans #557 #559]: #560
#579 := [monotonicity #561 #576]: #578
#586 := [monotonicity #579]: #585
#590 := [trans #586 #588]: #589
#583 := [quant-inst #27]: #582
#591 := [mp #583 #590]: #581
#646 := [unit-resolution #591 #470 #126]: #574
#266 := [not-or-elim #265]: #195
#647 := [hypothesis]: #644
#648 := [th-lemma arith farkas 1/2 -1/2 1/4 1 #647 #266 #646 #639]: false
#650 := [lemma #648]: #649
#651 := [hypothesis]: #491
#653 := (or #652 #644)
#654 := [th-lemma arith triangle-eq]: #653
#655 := [unit-resolution #654 #651 #650]: false
#656 := [lemma #655]: #652
#495 := (or #203 #491)
#496 := [def-axiom]: #495
#657 := [unit-resolution #496 #656]: #203
#492 := (not #203)
#493 := (or #492 #490)
#494 := [def-axiom]: #493
#658 := [unit-resolution #494 #657]: #490
#659 := (not #490)
#660 := (or #659 #635)
#661 := [th-lemma arith triangle-eq]: #660
[unit-resolution #661 #658 #643]: false
unsat
a7c1eea206143dd61561c7993b895cfbb2daa5bc 335 0
#2 := false
#8 := 0::Real
decl f9 :: (-> S6 S2 Real)
decl f12 :: S2
#27 := f12
decl f13 :: S6
#31 := f13
#32 := (f9 f13 f12)
decl f11 :: S6
#21 := f11
#30 := (f9 f11 f12)
#110 := -1::Real
#170 := (* -1::Real #30)
#171 := (+ #170 #32)
decl f3 :: Real
#9 := f3
#149 := (* -1::Real #32)
#263 := (+ #30 #149)
#264 := (+ f3 #263)
#265 := (<= #264 0::Real)
#268 := (ite #265 f3 #171)
#710 := (* -1::Real #268)
#711 := (+ f3 #710)
#712 := (<= #711 0::Real)
#720 := (not #712)
#137 := 1/2::Real
#434 := (* 1/2::Real #268)
#575 := (<= #434 0::Real)
#435 := (= #434 0::Real)
#191 := -1/2::Real
#271 := (* -1/2::Real #268)
#274 := (+ #32 #271)
decl f10 :: S6
#19 := f10
#34 := (f9 f10 f12)
#150 := (+ #149 #34)
#248 := (* -1::Real #34)
#249 := (+ #32 #248)
#250 := (+ f3 #249)
#251 := (<= #250 0::Real)
#254 := (ite #251 f3 #150)
#257 := (* 1/2::Real #254)
#260 := (+ #32 #257)
#139 := (* 1/2::Real #34)
#237 := (+ #149 #139)
#138 := (* 1/2::Real #30)
#238 := (+ #138 #237)
#235 := (>= #238 0::Real)
#277 := (ite #235 #260 #274)
#280 := (= #32 #277)
#438 := (iff #280 #435)
#431 := (= #32 #274)
#436 := (iff #431 #435)
#437 := [rewrite]: #436
#432 := (iff #280 #431)
#429 := (= #277 #274)
#424 := (ite false #260 #274)
#427 := (= #424 #274)
#428 := [rewrite]: #427
#425 := (= #277 #424)
#422 := (iff #235 false)
#234 := (not #235)
#296 := (<= #249 0::Real)
#293 := (<= #263 0::Real)
#299 := (and #293 #296)
#63 := 0::Int
decl f4 :: (-> S3 S2 Int)
decl f5 :: S3
#11 := f5
#28 := (f4 f5 f12)
#103 := -1::Int
#127 := (* -1::Int #28)
decl f6 :: (-> S4 S5 S2)
decl f8 :: S5
#15 := f8
decl f7 :: S4
#14 := f7
#16 := (f6 f7 f8)
#17 := (f4 f5 #16)
#128 := (+ #17 #127)
#129 := (<= #128 0::Int)
#302 := (or #129 #299)
#305 := (not #302)
#283 := (not #280)
#314 := (or #235 #283 #305)
#319 := (not #314)
#39 := 2::Real
#48 := (- #32 #30)
#49 := (<= f3 #48)
#50 := (ite #49 f3 #48)
#51 := (/ #50 2::Real)
#52 := (- #32 #51)
#43 := (- #34 #32)
#44 := (<= f3 #43)
#45 := (ite #44 f3 #43)
#46 := (/ #45 2::Real)
#47 := (+ #32 #46)
#38 := (+ #30 #34)
#40 := (/ #38 2::Real)
#42 := (<= #32 #40)
#53 := (ite #42 #47 #52)
#54 := (= #53 #32)
#55 := (not #54)
#41 := (< #40 #32)
#56 := (implies #41 #55)
#35 := (<= #32 #34)
#33 := (<= #30 #32)
#36 := (and #33 #35)
#29 := (< #28 #17)
#37 := (implies #29 #36)
#57 := (implies #37 #56)
#58 := (not #57)
#322 := (iff #58 #319)
#174 := (<= f3 #171)
#177 := (ite #174 f3 #171)
#192 := (* -1/2::Real #177)
#193 := (+ #32 #192)
#153 := (<= f3 #150)
#156 := (ite #153 f3 #150)
#162 := (* 1/2::Real #156)
#167 := (+ #32 #162)
#140 := (+ #138 #139)
#146 := (<= #32 #140)
#198 := (ite #146 #167 #193)
#204 := (= #32 #198)
#209 := (not #204)
#143 := (< #140 #32)
#215 := (not #143)
#216 := (or #215 #209)
#126 := (not #29)
#134 := (or #126 #36)
#224 := (not #134)
#225 := (or #224 #216)
#230 := (not #225)
#320 := (iff #230 #319)
#317 := (iff #225 #314)
#308 := (or #235 #283)
#311 := (or #305 #308)
#315 := (iff #311 #314)
#316 := [rewrite]: #315
#312 := (iff #225 #311)
#309 := (iff #216 #308)
#284 := (iff #209 #283)
#281 := (iff #204 #280)
#278 := (= #198 #277)
#275 := (= #193 #274)
#272 := (= #192 #271)
#269 := (= #177 #268)
#266 := (iff #174 #265)
#267 := [rewrite]: #266
#270 := [monotonicity #267]: #269
#273 := [monotonicity #270]: #272
#276 := [monotonicity #273]: #275
#261 := (= #167 #260)
#258 := (= #162 #257)
#255 := (= #156 #254)
#252 := (iff #153 #251)
#253 := [rewrite]: #252
#256 := [monotonicity #253]: #255
#259 := [monotonicity #256]: #258
#262 := [monotonicity #259]: #261
#247 := (iff #146 #235)
#246 := [rewrite]: #247
#279 := [monotonicity #246 #262 #276]: #278
#282 := [monotonicity #279]: #281
#285 := [monotonicity #282]: #284
#244 := (iff #215 #235)
#239 := (not #234)
#242 := (iff #239 #235)
#243 := [rewrite]: #242
#240 := (iff #215 #239)
#233 := (iff #143 #234)
#236 := [rewrite]: #233
#241 := [monotonicity #236]: #240
#245 := [trans #241 #243]: #244
#310 := [monotonicity #245 #285]: #309
#306 := (iff #224 #305)
#303 := (iff #134 #302)
#300 := (iff #36 #299)
#297 := (iff #35 #296)
#298 := [rewrite]: #297
#294 := (iff #33 #293)
#295 := [rewrite]: #294
#301 := [monotonicity #295 #298]: #300
#291 := (iff #126 #129)
#130 := (not #129)
#286 := (not #130)
#289 := (iff #286 #129)
#290 := [rewrite]: #289
#287 := (iff #126 #286)
#131 := (iff #29 #130)
#132 := [rewrite]: #131
#288 := [monotonicity #132]: #287
#292 := [trans #288 #290]: #291
#304 := [monotonicity #292 #301]: #303
#307 := [monotonicity #304]: #306
#313 := [monotonicity #307 #310]: #312
#318 := [trans #313 #316]: #317
#321 := [monotonicity #318]: #320
#231 := (iff #58 #230)
#228 := (iff #57 #225)
#221 := (implies #134 #216)
#226 := (iff #221 #225)
#227 := [rewrite]: #226
#222 := (iff #57 #221)
#219 := (iff #56 #216)
#212 := (implies #143 #209)
#217 := (iff #212 #216)
#218 := [rewrite]: #217
#213 := (iff #56 #212)
#210 := (iff #55 #209)
#207 := (iff #54 #204)
#201 := (= #198 #32)
#205 := (iff #201 #204)
#206 := [rewrite]: #205
#202 := (iff #54 #201)
#199 := (= #53 #198)
#196 := (= #52 #193)
#183 := (* 1/2::Real #177)
#188 := (- #32 #183)
#194 := (= #188 #193)
#195 := [rewrite]: #194
#189 := (= #52 #188)
#186 := (= #51 #183)
#180 := (/ #177 2::Real)
#184 := (= #180 #183)
#185 := [rewrite]: #184
#181 := (= #51 #180)
#178 := (= #50 #177)
#172 := (= #48 #171)
#173 := [rewrite]: #172
#175 := (iff #49 #174)
#176 := [monotonicity #173]: #175
#179 := [monotonicity #176 #173]: #178
#182 := [monotonicity #179]: #181
#187 := [trans #182 #185]: #186
#190 := [monotonicity #187]: #189
#197 := [trans #190 #195]: #196
#168 := (= #47 #167)
#165 := (= #46 #162)
#159 := (/ #156 2::Real)
#163 := (= #159 #162)
#164 := [rewrite]: #163
#160 := (= #46 #159)
#157 := (= #45 #156)
#151 := (= #43 #150)
#152 := [rewrite]: #151
#154 := (iff #44 #153)
#155 := [monotonicity #152]: #154
#158 := [monotonicity #155 #152]: #157
#161 := [monotonicity #158]: #160
#166 := [trans #161 #164]: #165
#169 := [monotonicity #166]: #168
#147 := (iff #42 #146)
#141 := (= #40 #140)
#142 := [rewrite]: #141
#148 := [monotonicity #142]: #147
#200 := [monotonicity #148 #169 #197]: #199
#203 := [monotonicity #200]: #202
#208 := [trans #203 #206]: #207
#211 := [monotonicity #208]: #210
#144 := (iff #41 #143)
#145 := [monotonicity #142]: #144
#214 := [monotonicity #145 #211]: #213
#220 := [trans #214 #218]: #219
#135 := (iff #37 #134)
#136 := [rewrite]: #135
#223 := [monotonicity #136 #220]: #222
#229 := [trans #223 #227]: #228
#232 := [monotonicity #229]: #231
#323 := [trans #232 #321]: #322
#102 := [asserted]: #58
#324 := [mp #102 #323]: #319
#325 := [not-or-elim #324]: #234
#423 := [iff-false #325]: #422
#426 := [monotonicity #423]: #425
#430 := [trans #426 #428]: #429
#433 := [monotonicity #430]: #432
#439 := [trans #433 #437]: #438
#326 := [not-or-elim #324]: #280
#440 := [mp #326 #439]: #435
#714 := (not #435)
#715 := (or #714 #575)
#716 := [th-lemma arith triangle-eq]: #715
#717 := [unit-resolution #716 #440]: #575
#718 := [hypothesis]: #712
#97 := (<= f3 0::Real)
#98 := (not #97)
#10 := (< 0::Real f3)
#99 := (iff #10 #98)
#100 := [rewrite]: #99
#94 := [asserted]: #10
#101 := [mp #94 #100]: #98
#719 := [th-lemma arith farkas -1/2 1/2 1 #101 #718 #717]: false
#721 := [lemma #719]: #720
#568 := (= f3 #268)
#569 := (= #171 #268)
#729 := (not #569)
#713 := (+ #171 #710)
#722 := (<= #713 0::Real)
#726 := (not #722)
#448 := (iff #302 #299)
#443 := (or false #299)
#446 := (iff #443 #299)
#447 := [rewrite]: #446
#444 := (iff #302 #443)
#420 := (iff #129 false)
#96 := [asserted]: #29
#133 := [mp #96 #132]: #130
#421 := [iff-false #133]: #420
#445 := [monotonicity #421]: #444
#449 := [trans #445 #447]: #448
#327 := [not-or-elim #324]: #302
#450 := [mp #327 #449]: #299
#442 := [and-elim #450]: #296
#724 := [hypothesis]: #722
#725 := [th-lemma arith farkas 1/2 1/2 1 1 #724 #442 #325 #717]: false
#727 := [lemma #725]: #726
#728 := [hypothesis]: #569
#730 := (or #729 #722)
#731 := [th-lemma arith triangle-eq]: #730
#732 := [unit-resolution #731 #728 #727]: false
#733 := [lemma #732]: #729
#573 := (or #265 #569)
#574 := [def-axiom]: #573
#734 := [unit-resolution #574 #733]: #265
#570 := (not #265)
#571 := (or #570 #568)
#572 := [def-axiom]: #571
#735 := [unit-resolution #572 #734]: #568
#736 := (not #568)
#737 := (or #736 #712)
#738 := [th-lemma arith triangle-eq]: #737
[unit-resolution #738 #735 #721]: 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