src/HOL/Multivariate_Analysis/Integration.certs

more robust default font -- user might have switched jEdit TextArea to another font that lacks glyphs;

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