src/HOL/Multivariate_Analysis/Integration.certs

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