b95bf7adc1e2b959cf13db317b64554768249b2e 7790 0

 #2 := false

 decl uf_110 :: (-> T4 T5 int)

 decl uf_66 :: (-> T5 int T3 T5)

 decl uf_7 :: T3

 #10 := uf_7

 decl ?x785!14 :: int

 #18296 := ?x785!14

 decl uf_43 :: (-> T3 int T5)

 decl uf_288 :: int

 #2978 := uf_288

 #2979 := (uf_43 uf_7 uf_288)

 #18301 := (uf_66 #2979 ?x785!14 uf_7)

 decl uf_287 :: T4

 #2976 := uf_287

 #18302 := (uf_110 uf_287 #18301)

 decl uf_298 :: int

 #3069 := uf_298

 #3181 := (uf_66 #2979 uf_298 uf_7)

 #3190 := (uf_110 uf_287 #3181)

 #30497 := (= #3190 #18302)

 #30502 := (not #30497)

 #121 := 0::int

 #4044 := -1::int

 #18623 := (* -1::int #18302)

 #30501 := (+ #3190 #18623)

 #30503 := (>= #30501 0::int)

 #30513 := (not #30503)

 decl uf_304 :: int

 #3197 := uf_304

 #13279 := (* -1::int uf_304)

 #30155 := (+ #3190 #13279)

 #30108 := (<= #30155 0::int)

 #30154 := (= #3190 uf_304)

 decl uf_303 :: int

 #3192 := uf_303

 #12313 := (= uf_303 uf_304)

 #18624 := (+ uf_304 #18623)

 #18625 := (>= #18624 0::int)

 #18610 := (* -1::int ?x785!14)

 decl uf_306 :: int

 #3207 := uf_306

 #18611 := (+ uf_306 #18610)

 #18612 := (<= #18611 0::int)

 #18298 := (>= ?x785!14 0::int)

 #22078 := (not #18298)

 #7473 := 4294967295::int

 #18297 := (<= ?x785!14 4294967295::int)

 #22077 := (not #18297)

 #22093 := (or #22077 #22078 #18612 #18625)

 #22098 := (not #22093)

 #161 := (:var 0 int)

 #3053 := (uf_66 #2979 #161 uf_7)

 #23000 := (pattern #3053)

 #14916 := (<= #161 4294967295::int)

 #19295 := (not #14916)

 #3054 := (uf_110 uf_287 #3053)

 #13280 := (+ #3054 #13279)

 #13281 := (<= #13280 0::int)

 #13260 := (* -1::int uf_306)

 #13268 := (+ #161 #13260)

 #13267 := (>= #13268 0::int)

 #4043 := (>= #161 0::int)

 #4965 := (not #4043)

 #22059 := (or #4965 #13267 #13281 #19295)

 #23017 := (forall (vars (?x785 int)) (:pat #23000) #22059)

 #23022 := (not #23017)

 decl uf_305 :: int

 #3199 := uf_305

 #13301 := (* -1::int uf_305)

 decl uf_286 :: int

 #2973 := uf_286

 #13302 := (+ uf_286 #13301)

 #13303 := (<= #13302 0::int)

 #3219 := (uf_66 #2979 uf_305 uf_7)

 #3220 := (uf_110 uf_287 #3219)

 #12352 := (= uf_304 #3220)

 #22044 := (not #12352)

 #22045 := (or #22044 #13303)

 #22046 := (not #22045)

 #23025 := (or #22046 #23022)

 #23028 := (not #23025)

 #23031 := (or #23028 #22098)

 #23034 := (not #23031)

 #13261 := (+ uf_286 #13260)

 #13259 := (>= #13261 0::int)

 #13264 := (not #13259)

 #23037 := (or #13264 #23034)

 #23040 := (not #23037)

 #23043 := (or #13264 #23040)

 #23046 := (not #23043)

 #15608 := 4294967294::int

 #15609 := (<= uf_298 4294967294::int)

 #18279 := (not #15609)

 #13328 := (+ uf_298 #13260)

 #13327 := (= #13328 -1::int)

 #13331 := (not #13327)

 #892 := 2::int

 #13251 := (>= uf_306 2::int)

 #22121 := (not #13251)

 #13243 := (>= uf_298 -1::int)

 #18276 := (not #13243)

 #13234 := (>= uf_305 0::int)

 #22120 := (not #13234)

 decl up_291 :: (-> T4 T1 T1 int T3 bool)

 decl uf_4 :: T3

 #7 := uf_4

 decl uf_273 :: T1

 #2946 := uf_273

 decl uf_269 :: T1

 #2942 := uf_269

 #3209 := (up_291 uf_287 uf_269 uf_273 uf_306 uf_4)

 #12401 := (not #3209)

 #23049 := (or #12401 #22120 #18276 #22121 #13331 #18279 #23046)

 #23052 := (not #23049)

 #23055 := (or #18276 #18279 #23052)

 #23058 := (not #23055)

 #4 := 1::int

 #13225 := (>= uf_298 1::int)

 #13365 := (not #13225)

 #12316 := (= uf_298 uf_305)

 #12440 := (not #12316)

 #12449 := (not #12313)

 #12308 := (= #3190 uf_303)

 #12485 := (not #12308)

 decl uf_68 :: (-> T4 T5 T2)

 #3187 := (uf_68 uf_287 #3181)

 decl uf_9 :: T2

 #19 := uf_9

 #12302 := (= uf_9 #3187)

 #18247 := (not #12302)

 decl uf_48 :: (-> T5 T3 T2)

 #3182 := (uf_48 #3181 uf_7)

 #12293 := (= uf_9 #3182)

 #18238 := (not #12293)

 decl uf_275 :: T1

 #2948 := uf_275

 decl uf_270 :: T1

 #2943 := uf_270

 #3195 := (up_291 uf_287 uf_270 uf_275 uf_298 uf_4)

 #12467 := (not #3195)

 decl uf_277 :: T1

 #2950 := uf_277

 decl uf_271 :: T1

 #2944 := uf_271

 #3194 := (up_291 uf_287 uf_271 uf_277 uf_303 uf_7)

 #12476 := (not #3194)

 #23061 := (or #12476 #12467 #18238 #18247 #12485 #12449 #12440 #13365 #22120 #23058)

 #23064 := (not #23061)

 #13418 := (* -1::int #3190)

 decl uf_296 :: int

 #3061 := uf_296

 #13419 := (+ uf_296 #13418)

 #13417 := (>= #13419 0::int)

 #13416 := (not #13417)

 decl uf_297 :: int

 #3065 := uf_297

 #13222 := (>= uf_297 0::int)

 #22161 := (not #13222)

 #12551 := (= uf_297 uf_305)

 #12557 := (not #12551)

 #12548 := (= uf_296 uf_304)

 #12566 := (not #12548)

 #23091 := (or #12566 #12557 #22161 #13365 #22120 #13416 #23058)

 #23094 := (not #23091)

 #23067 := (or #18238 #18247 #23064)

 #23070 := (not #23067)

 decl uf_24 :: (-> T4 T5 T2)

 #3184 := (uf_24 uf_287 #3181)

 #12296 := (= uf_9 #3184)

 #18241 := (not #12296)

 #23073 := (or #18238 #18241 #23070)

 #23076 := (not #23073)

 #23079 := (or #18238 #18241 #23076)

 #23082 := (not #23079)

 #23085 := (or #22161 #13365 #13417 #23082)

 #23088 := (not #23085)

 #23097 := (or #23088 #23094)

 #23100 := (not #23097)

 #23103 := (or #18238 #18247 #22161 #13365 #23100)

 #23106 := (not #23103)

 decl uf_25 :: (-> T4 T5 T5)

 decl uf_135 :: (-> T14 T5)

 decl uf_58 :: (-> T13 T5 T14)

 decl uf_59 :: (-> T4 T13)

 #3150 := (uf_59 uf_287)

 #27629 := (uf_58 #3150 #3181)

 #29089 := (uf_135 #27629)

 #29092 := (uf_25 uf_287 #29089)

 decl uf_26 :: T5

 #77 := uf_26

 #29093 := (= uf_26 #29092)

 decl uf_210 :: (-> T4 T5 T2)

 #29090 := (uf_210 uf_287 #29089)

 #29091 := (= uf_9 #29090)

 #29149 := (or #29091 #29093)

 #29152 := (not #29149)

 decl uf_136 :: (-> T14 T2)

 #29102 := (uf_136 #27629)

 #29103 := (= uf_9 #29102)

 #29104 := (not #29103)

 decl uf_27 :: (-> T4 T5 T2)

 #29099 := (uf_27 uf_287 #29089)

 #29100 := (= uf_9 #29099)

 #29101 := (not #29100)

 #29143 := (or #29101 #29104)

 #29146 := (not #29143)

 decl uf_12 :: (-> T3 T8)

 decl uf_13 :: (-> T5 T3)

 #27885 := (uf_13 #3181)

 #29107 := (uf_12 #27885)

 decl uf_14 :: T8

 #28 := uf_14

 #29125 := (= uf_14 #29107)

 #29140 := (not #29125)

 #29096 := (uf_13 #29089)

 #29097 := (uf_12 #29096)

 #29098 := (= uf_14 #29097)

 #29158 := (or #29098 #29140 #29146 #29152)

 #29163 := (not #29158)

 #29114 := (uf_25 uf_287 #3181)

 #29115 := (= uf_26 #29114)

 #29112 := (uf_210 uf_287 #3181)

 #29113 := (= uf_9 #29112)

 #29128 := (or #29113 #29115)

 #29131 := (not #29128)

 #29134 := (or #29125 #29131)

 #29137 := (not #29134)

 #29166 := (or #29137 #29163)

 #29169 := (not #29166)

 #29172 := (or #18241 #29169)

 #29175 := (not #29172)

 #29178 := (iff #12302 #29175)

 #29750 := (not #29178)

 #29945 := [hypothesis]: #29750

 #23 := (:var 0 T5)

 #47 := (:var 1 T4)

 #2381 := (uf_68 #47 #23)

 #2382 := (pattern #2381)

 #282 := (uf_59 #47)

 #2384 := (uf_58 #282 #23)

 #2388 := (uf_135 #2384)

 #2399 := (uf_210 #47 #2388)

 #10480 := (= uf_9 #2399)

 #2397 := (uf_25 #47 #2388)

 #10477 := (= uf_26 #2397)

 #10483 := (or #10477 #10480)

 #21752 := (not #10483)

 #2393 := (uf_13 #2388)

 #2394 := (uf_12 #2393)

 #10471 := (= uf_14 #2394)

 #2389 := (uf_27 #47 #2388)

 #10462 := (= uf_9 #2389)

 #10465 := (not #10462)

 #2385 := (uf_136 #2384)

 #10456 := (= uf_9 #2385)

 #10459 := (not #10456)

 #10468 := (or #10459 #10465)

 #21751 := (not #10468)

 #26 := (uf_13 #23)

 #27 := (uf_12 #26)

 #29 := (= #27 uf_14)

 #52 := (not #29)

 #21753 := (or #52 #21751 #10471 #21752)

 #21754 := (not #21753)

 #2405 := (uf_210 #47 #23)

 #10495 := (= uf_9 #2405)

 #142 := (uf_25 #47 #23)

 #3617 := (= uf_26 #142)

 #10498 := (or #3617 #10495)

 #21746 := (not #10498)

 #21747 := (or #29 #21746)

 #21748 := (not #21747)

 #21757 := (or #21748 #21754)

 #21763 := (not #21757)

 #146 := (uf_24 #47 #23)

 #3623 := (= uf_9 #146)

 #11068 := (not #3623)

 #21764 := (or #11068 #21763)

 #21765 := (not #21764)

 #10452 := (= uf_9 #2381)

 #21770 := (iff #10452 #21765)

 #21773 := (forall (vars (?x632 T4) (?x633 T5)) (:pat #2382) #21770)

 #10474 := (not #10471)

 #10516 := (and #29 #10468 #10474 #10483)

 #10501 := (and #52 #10498)

 #10522 := (or #10501 #10516)

 #10527 := (and #3623 #10522)

 #10530 := (iff #10452 #10527)

 #10533 := (forall (vars (?x632 T4) (?x633 T5)) (:pat #2382) #10530)

 #21774 := (iff #10533 #21773)

 #21771 := (iff #10530 #21770)

 #21768 := (iff #10527 #21765)

 #21760 := (and #3623 #21757)

 #21766 := (iff #21760 #21765)

 #21767 := [rewrite]: #21766

 #21761 := (iff #10527 #21760)

 #21758 := (iff #10522 #21757)

 #21755 := (iff #10516 #21754)

 #21756 := [rewrite]: #21755

 #21749 := (iff #10501 #21748)

 #21750 := [rewrite]: #21749

 #21759 := [monotonicity #21750 #21756]: #21758

 #21762 := [monotonicity #21759]: #21761

 #21769 := [trans #21762 #21767]: #21768

 #21772 := [monotonicity #21769]: #21771

 #21775 := [quant-intro #21772]: #21774

 #17696 := (~ #10533 #10533)

 #17694 := (~ #10530 #10530)

 #17695 := [refl]: #17694

 #17697 := [nnf-pos #17695]: #17696

 #2406 := (= #2405 uf_9)

 #143 := (= #142 uf_26)

 #2407 := (or #143 #2406)

 #2408 := (and #52 #2407)

 #2400 := (= #2399 uf_9)

 #2398 := (= #2397 uf_26)

 #2401 := (or #2398 #2400)

 #2395 := (= #2394 uf_14)

 #2396 := (not #2395)

 #2402 := (and #2396 #2401)

 #2390 := (= #2389 uf_9)

 #2391 := (not #2390)

 #2386 := (= #2385 uf_9)

 #2387 := (not #2386)

 #2392 := (or #2387 #2391)

 #2403 := (and #2392 #2402)

 #2404 := (and #29 #2403)

 #2409 := (or #2404 #2408)

 #147 := (= #146 uf_9)

 #2410 := (and #147 #2409)

 #2383 := (= #2381 uf_9)

 #2411 := (iff #2383 #2410)

 #2412 := (forall (vars (?x632 T4) (?x633 T5)) (:pat #2382) #2411)

 #10536 := (iff #2412 #10533)

 #10486 := (and #10474 #10483)

 #10489 := (and #10468 #10486)

 #10492 := (and #29 #10489)

 #10504 := (or #10492 #10501)

 #10507 := (and #3623 #10504)

 #10510 := (iff #10452 #10507)

 #10513 := (forall (vars (?x632 T4) (?x633 T5)) (:pat #2382) #10510)

 #10534 := (iff #10513 #10533)

 #10531 := (iff #10510 #10530)

 #10528 := (iff #10507 #10527)

 #10525 := (iff #10504 #10522)

 #10519 := (or #10516 #10501)

 #10523 := (iff #10519 #10522)

 #10524 := [rewrite]: #10523

 #10520 := (iff #10504 #10519)

 #10517 := (iff #10492 #10516)

 #10518 := [rewrite]: #10517

 #10521 := [monotonicity #10518]: #10520

 #10526 := [trans #10521 #10524]: #10525

 #10529 := [monotonicity #10526]: #10528

 #10532 := [monotonicity #10529]: #10531

 #10535 := [quant-intro #10532]: #10534

 #10514 := (iff #2412 #10513)

 #10511 := (iff #2411 #10510)

 #10508 := (iff #2410 #10507)

 #10505 := (iff #2409 #10504)

 #10502 := (iff #2408 #10501)

 #10499 := (iff #2407 #10498)

 #10496 := (iff #2406 #10495)

 #10497 := [rewrite]: #10496

 #3618 := (iff #143 #3617)

 #3619 := [rewrite]: #3618

 #10500 := [monotonicity #3619 #10497]: #10499

 #10503 := [monotonicity #10500]: #10502

 #10493 := (iff #2404 #10492)

 #10490 := (iff #2403 #10489)

 #10487 := (iff #2402 #10486)

 #10484 := (iff #2401 #10483)

 #10481 := (iff #2400 #10480)

 #10482 := [rewrite]: #10481

 #10478 := (iff #2398 #10477)

 #10479 := [rewrite]: #10478

 #10485 := [monotonicity #10479 #10482]: #10484

 #10475 := (iff #2396 #10474)

 #10472 := (iff #2395 #10471)

 #10473 := [rewrite]: #10472

 #10476 := [monotonicity #10473]: #10475

 #10488 := [monotonicity #10476 #10485]: #10487

 #10469 := (iff #2392 #10468)

 #10466 := (iff #2391 #10465)

 #10463 := (iff #2390 #10462)

 #10464 := [rewrite]: #10463

 #10467 := [monotonicity #10464]: #10466

 #10460 := (iff #2387 #10459)

 #10457 := (iff #2386 #10456)

 #10458 := [rewrite]: #10457

 #10461 := [monotonicity #10458]: #10460

 #10470 := [monotonicity #10461 #10467]: #10469

 #10491 := [monotonicity #10470 #10488]: #10490

 #10494 := [monotonicity #10491]: #10493

 #10506 := [monotonicity #10494 #10503]: #10505

 #3624 := (iff #147 #3623)

 #3625 := [rewrite]: #3624

 #10509 := [monotonicity #3625 #10506]: #10508

 #10454 := (iff #2383 #10452)

 #10455 := [rewrite]: #10454

 #10512 := [monotonicity #10455 #10509]: #10511

 #10515 := [quant-intro #10512]: #10514

 #10537 := [trans #10515 #10535]: #10536

 #10451 := [asserted]: #2412

 #10538 := [mp #10451 #10537]: #10533

 #17698 := [mp~ #10538 #17697]: #10533

 #21776 := [mp #17698 #21775]: #21773

 #27259 := (not #21773)

 #29859 := (or #27259 #29178)

 #29094 := (or #29093 #29091)

 #29095 := (not #29094)

 #29105 := (or #29104 #29101)

 #29106 := (not #29105)

 #29108 := (= #29107 uf_14)

 #29109 := (not #29108)

 #29110 := (or #29109 #29106 #29098 #29095)

 #29111 := (not #29110)

 #29116 := (or #29115 #29113)

 #29117 := (not #29116)

 #29118 := (or #29108 #29117)

 #29119 := (not #29118)

 #29120 := (or #29119 #29111)

 #29121 := (not #29120)

 #29122 := (or #18241 #29121)

 #29123 := (not #29122)

 #29124 := (iff #12302 #29123)

 #29860 := (or #27259 #29124)

 #29862 := (iff #29860 #29859)

 #29690 := (iff #29859 #29859)

 #29691 := [rewrite]: #29690

 #29179 := (iff #29124 #29178)

 #29176 := (iff #29123 #29175)

 #29173 := (iff #29122 #29172)

 #29170 := (iff #29121 #29169)

 #29167 := (iff #29120 #29166)

 #29164 := (iff #29111 #29163)

 #29161 := (iff #29110 #29158)

 #29155 := (or #29140 #29146 #29098 #29152)

 #29159 := (iff #29155 #29158)

 #29160 := [rewrite]: #29159

 #29156 := (iff #29110 #29155)

 #29153 := (iff #29095 #29152)

 #29150 := (iff #29094 #29149)

 #29151 := [rewrite]: #29150

 #29154 := [monotonicity #29151]: #29153

 #29147 := (iff #29106 #29146)

 #29144 := (iff #29105 #29143)

 #29145 := [rewrite]: #29144

 #29148 := [monotonicity #29145]: #29147

 #29141 := (iff #29109 #29140)

 #29126 := (iff #29108 #29125)

 #29127 := [rewrite]: #29126

 #29142 := [monotonicity #29127]: #29141

 #29157 := [monotonicity #29142 #29148 #29154]: #29156

 #29162 := [trans #29157 #29160]: #29161

 #29165 := [monotonicity #29162]: #29164

 #29138 := (iff #29119 #29137)

 #29135 := (iff #29118 #29134)

 #29132 := (iff #29117 #29131)

 #29129 := (iff #29116 #29128)

 #29130 := [rewrite]: #29129

 #29133 := [monotonicity #29130]: #29132

 #29136 := [monotonicity #29127 #29133]: #29135

 #29139 := [monotonicity #29136]: #29138

 #29168 := [monotonicity #29139 #29165]: #29167

 #29171 := [monotonicity #29168]: #29170

 #29174 := [monotonicity #29171]: #29173

 #29177 := [monotonicity #29174]: #29176

 #29180 := [monotonicity #29177]: #29179

 #29689 := [monotonicity #29180]: #29862

 #29674 := [trans #29689 #29691]: #29862

 #29861 := [quant-inst]: #29860

 #29675 := [mp #29861 #29674]: #29859

 #29979 := [unit-resolution #29675 #21776 #29945]: false

 #29980 := [lemma #29979]: #29178

 #30580 := (or #29750 #12302)

 #29847 := [hypothesis]: #29158

 decl uf_116 :: (-> T5 int)

 #2980 := (uf_116 #2979)

 decl uf_124 :: (-> T3 int T3)

 #2977 := (uf_124 uf_7 uf_286)

 #2981 := (uf_43 #2977 #2980)

 #2984 := (uf_25 uf_287 #2981)

 #29898 := (= #2984 #29092)

 #29899 := (= #29092 #2984)

 #30393 := (= #29089 #2981)

 decl uf_143 :: (-> T3 int)

 #24645 := (uf_143 #2977)

 decl uf_144 :: (-> T3 T3)

 #24643 := (uf_144 #2977)

 #26925 := (uf_124 #24643 #24645)

 #26926 := (uf_43 #26925 #2980)

 #28291 := (= #26926 #2981)

 #28289 := (= #26925 #2977)

 #28287 := (= #24645 uf_286)

 #24646 := (= uf_286 #24645)

 #326 := (:var 1 T3)

 #1358 := (uf_124 #326 #161)

 #1592 := (pattern #1358)

 #1602 := (uf_143 #1358)

 #8266 := (= #161 #1602)

 #8269 := (forall (vars (?x386 T3) (?x387 int)) (:pat #1592) #8266)

 #17072 := (~ #8269 #8269)

 #17070 := (~ #8266 #8266)

 #17071 := [refl]: #17070

 #17073 := [nnf-pos #17071]: #17072

 #1603 := (= #1602 #161)

 #1604 := (forall (vars (?x386 T3) (?x387 int)) (:pat #1592) #1603)

 #8270 := (iff #1604 #8269)

 #8267 := (iff #1603 #8266)

 #8268 := [rewrite]: #8267

 #8271 := [quant-intro #8268]: #8270

 #8265 := [asserted]: #1604

 #8274 := [mp #8265 #8271]: #8269

 #17074 := [mp~ #8274 #17073]: #8269

 #24652 := (not #8269)

 #24653 := (or #24652 #24646)

 #24654 := [quant-inst]: #24653

 #28210 := [unit-resolution #24654 #17074]: #24646

 #28288 := [symm #28210]: #28287

 #28189 := (= #24643 uf_7)

 #24644 := (= uf_7 #24643)

 #1605 := (uf_144 #1358)

 #8273 := (= #326 #1605)

 #8277 := (forall (vars (?x388 T3) (?x389 int)) (:pat #1592) #8273)

 #17077 := (~ #8277 #8277)

 #17075 := (~ #8273 #8273)

 #17076 := [refl]: #17075

 #17078 := [nnf-pos #17076]: #17077

 #1606 := (= #1605 #326)

 #1607 := (forall (vars (?x388 T3) (?x389 int)) (:pat #1592) #1606)

 #8278 := (iff #1607 #8277)

 #8275 := (iff #1606 #8273)

 #8276 := [rewrite]: #8275

 #8279 := [quant-intro #8276]: #8278

 #8272 := [asserted]: #1607

 #8282 := [mp #8272 #8279]: #8277

 #17079 := [mp~ #8282 #17078]: #8277

 #24647 := (not #8277)

 #24648 := (or #24647 #24644)

 #24649 := [quant-inst]: #24648

 #28188 := [unit-resolution #24649 #17079]: #24644

 #28190 := [symm #28188]: #28189

 #28290 := [monotonicity #28190 #28288]: #28289

 #28292 := [monotonicity #28290]: #28291

 #30391 := (= #29089 #26926)

 decl uf_125 :: (-> T5 T5 int)

 decl uf_28 :: (-> int T5)

 decl uf_29 :: (-> T5 int)

 #3013 := (uf_29 #2979)

 #24470 := (uf_28 #3013)

 #26903 := (uf_13 #24470)

 #28922 := (uf_66 #24470 uf_298 #26903)

 #28923 := (uf_125 #28922 #24470)

 #28947 := (uf_66 #26926 #28923 #24643)

 #28951 := (uf_58 #3150 #28947)

 #28954 := (uf_135 #28951)

 #30390 := (= #28954 #26926)

 #28955 := (= #26926 #28954)

 decl up_67 :: (-> T14 bool)

 #28957 := (up_67 #28951)

 #28958 := (not #28957)

 #28956 := (not #28955)

 #28952 := (uf_136 #28951)

 #28953 := (= uf_9 #28952)

 #28948 := (uf_24 uf_287 #28947)

 #28949 := (= uf_9 #28948)

 #28950 := (not #28949)

 #28979 := (or #28950 #28953 #28956 #28958)

 #28982 := (not #28979)

 #28972 := (* -1::int #28923)

 #28973 := (+ #24645 #28972)

 #28974 := (<= #28973 0::int)

 #30321 := (not #28974)

 #29082 := (+ uf_298 #28972)

 #29084 := (>= #29082 0::int)

 #28924 := (= uf_298 #28923)

 #15 := (:var 1 T5)

 #1390 := (uf_13 #15)

 #1391 := (uf_66 #15 #161 #1390)

 #1392 := (pattern #1391)

 #1393 := (uf_125 #1391 #15)

 #7665 := (= #161 #1393)

 #7669 := (forall (vars (?x319 T5) (?x320 int)) (:pat #1392) #7665)

 #16789 := (~ #7669 #7669)

 #16787 := (~ #7665 #7665)

 #16788 := [refl]: #16787

 #16790 := [nnf-pos #16788]: #16789

 #1394 := (= #1393 #161)

 #1395 := (forall (vars (?x319 T5) (?x320 int)) (:pat #1392) #1394)

 #7670 := (iff #1395 #7669)

 #7667 := (iff #1394 #7665)

 #7668 := [rewrite]: #7667

 #7671 := [quant-intro #7668]: #7670

 #7664 := [asserted]: #1395

 #7674 := [mp #7664 #7671]: #7669

 #16791 := [mp~ #7674 #16790]: #7669

 #26910 := (not #7669)

 #28927 := (or #26910 #28924)

 #28928 := [quant-inst]: #28927

 #29280 := [unit-resolution #28928 #16791]: #28924

 #29281 := (not #28924)

 #30320 := (or #29281 #29084)

 #30315 := [th-lemma]: #30320

 #30316 := [unit-resolution #30315 #29280]: #29084

 #13246 := (* -1::int uf_298)

 #13509 := (+ uf_286 #13246)

 #13510 := (<= #13509 0::int)

 #13511 := (not #13510)

 #23109 := (or #18238 #18247 #23106)

 #23112 := (not #23109)

 #23115 := (or #18238 #18241 #23112)

 #23118 := (not #23115)

 #23121 := (or #18238 #18241 #23118)

 #23124 := (not #23121)

 #23127 := (or #22161 #13365 #13510 #23124)

 #23130 := (not #23127)

 decl ?x776!15 :: int

 #18420 := ?x776!15

 #18425 := (uf_66 #2979 ?x776!15 uf_7)

 #18426 := (uf_110 uf_287 #18425)

 #18771 := (* -1::int #18426)

 decl uf_302 :: int

 #3096 := uf_302

 #18772 := (+ uf_302 #18771)

 #18773 := (>= #18772 0::int)

 #18758 := (* -1::int ?x776!15)

 #18759 := (+ uf_286 #18758)

 #18760 := (<= #18759 0::int)

 #18422 := (>= ?x776!15 0::int)

 #22255 := (not #18422)

 #18421 := (<= ?x776!15 4294967295::int)

 #22254 := (not #18421)

 #22270 := (or #22254 #22255 #18760 #18773)

 #22275 := (not #22270)

 #13151 := (* -1::int uf_286)

 #13539 := (+ #161 #13151)

 #13538 := (>= #13539 0::int)

 #3103 := (= #3054 uf_302)

 #22228 := (not #3103)

 #22229 := (or #22228 #4965 #13538 #19295)

 #23141 := (forall (vars (?x778 int)) (:pat #23000) #22229)

 #23146 := (not #23141)

 #13550 := (* -1::int uf_302)

 #13551 := (+ #3054 #13550)

 #13552 := (<= #13551 0::int)

 #22220 := (or #4965 #13538 #13552 #19295)

 #23133 := (forall (vars (?x776 int)) (:pat #23000) #22220)

 #23138 := (not #23133)

 #23149 := (or #23138 #23146)

 #23152 := (not #23149)

 #23155 := (or #23152 #22275)

 #23158 := (not #23155)

 #12017 := (= uf_296 uf_302)

 #12052 := (not #12017)

 decl uf_301 :: int

 #3094 := uf_301

 #12014 := (= uf_297 uf_301)

 #12061 := (not #12014)

 decl uf_300 :: int

 #3092 := uf_300

 #12011 := (= uf_298 uf_300)

 #12070 := (not #12011)

 decl uf_299 :: int

 #3090 := uf_299

 #12008 := (= uf_296 uf_299)

 #12079 := (not #12008)

 #23161 := (or #12079 #12070 #12061 #12052 #22161 #13365 #13511 #23158)

 #23164 := (not #23161)

 #23167 := (or #23130 #23164)

 #23170 := (not #23167)

 #13715 := (* -1::int uf_296)

 #13716 := (+ #3054 #13715)

 #13717 := (<= #13716 0::int)

 #13704 := (+ #161 #13246)

 #13703 := (>= #13704 0::int)

 #22036 := (or #4965 #13703 #13717 #19295)

 #23009 := (forall (vars (?x775 int)) (:pat #23000) #22036)

 #23014 := (not #23009)

 #1331 := 255::int

 #15594 := (<= uf_296 255::int)

 #22305 := (not #15594)

 #15577 := (<= uf_297 4294967295::int)

 #22304 := (not #15577)

 #15560 := (<= uf_298 4294967295::int)

 #22303 := (not #15560)

 #13765 := (>= uf_296 0::int)

 #22301 := (not #13765)

 #13743 := (>= uf_298 0::int)

 #22300 := (not #13743)

 #13737 := (>= #13509 0::int)

 #13740 := (not #13737)

 #13686 := (* -1::int uf_297)

 #13687 := (+ uf_286 #13686)

 #13688 := (<= #13687 0::int)

 #13217 := (<= uf_286 0::int)

 decl uf_178 :: (-> T4 T4 T2)

 #3162 := (uf_178 uf_287 uf_287)

 #12254 := (= uf_9 #3162)

 #13683 := (not #12254)

 decl uf_202 :: (-> T1 T4 T2)

 decl uf_272 :: T1

 #2945 := uf_272

 #3087 := (uf_202 uf_272 uf_287)

 #11997 := (= uf_9 #3087)

 #14996 := (not #11997)

 #3082 := (uf_66 #2979 uf_297 uf_7)

 #3083 := (uf_110 uf_287 #3082)

 #11989 := (= uf_296 #3083)

 #22299 := (not #11989)

 decl up_292 :: (-> T4 T1 T1 T5 T3 bool)

 decl uf_6 :: (-> T3 T3)

 #11 := (uf_6 uf_7)

 decl uf_280 :: T1

 #2953 := uf_280

 #3175 := (up_292 uf_287 uf_272 uf_280 #2979 #11)

 #22298 := (not #3175)

 #3174 := (up_291 uf_287 uf_272 uf_280 #3013 #11)

 #22297 := (not #3174)

 decl uf_279 :: T1

 #2952 := uf_279

 #3173 := (up_291 uf_287 uf_272 uf_279 uf_286 uf_4)

 #12742 := (not #3173)

 #3172 := (up_291 uf_287 uf_272 uf_277 uf_296 uf_7)

 #12751 := (not #3172)

 #3171 := (up_291 uf_287 uf_272 uf_275 uf_297 uf_4)

 #12760 := (not #3171)

 #3170 := (up_291 uf_287 uf_272 uf_273 uf_298 uf_4)

 #12769 := (not #3170)

 #3031 := (uf_66 #2979 0::int uf_7)

 #3041 := (uf_110 uf_287 #3031)

 decl uf_295 :: int

 #3040 := uf_295

 #3042 := (= uf_295 #3041)

 #12976 := (not #3042)

 #23173 := (or #12976 #12769 #12760 #12751 #12742 #22297 #22298 #22299 #14996 #13683 #13217 #22161 #13365 #13688 #13740 #22300 #22301 #22303 #22304 #22305 #23014 #23170)

 #23176 := (not #23173)

 #23179 := (or #12976 #13217 #23176)

 #23182 := (not #23179)

 #13197 := (* -1::int #3054)

 #13198 := (+ uf_295 #13197)

 #13196 := (>= #13198 0::int)

 #13184 := (>= #161 1::int)

 #22025 := (or #4965 #13184 #13196 #19295)

 #23001 := (forall (vars (?x773 int)) (:pat #23000) #22025)

 #23006 := (not #23001)

 #23185 := (or #23006 #23182)

 #23188 := (not #23185)

 decl ?x773!13 :: int

 #18159 := ?x773!13

 #18169 := (>= ?x773!13 1::int)

 #18164 := (uf_66 #2979 ?x773!13 uf_7)

 #18165 := (uf_110 uf_287 #18164)

 #18166 := (* -1::int #18165)

 #18167 := (+ uf_295 #18166)

 #18168 := (>= #18167 0::int)

 #18161 := (>= ?x773!13 0::int)

 #21999 := (not #18161)

 #18160 := (<= ?x773!13 4294967295::int)

 #21998 := (not #18160)

 #22014 := (or #21998 #21999 #18168 #18169)

 #22019 := (not #22014)

 #23191 := (or #22019 #23188)

 #23194 := (not #23191)

 #13178 := (>= uf_286 1::int)

 #13181 := (not #13178)

 #23197 := (or #13181 #23194)

 #23200 := (not #23197)

 #23203 := (or #13181 #23200)

 #23206 := (not #23203)

 #3037 := (uf_68 uf_287 #3031)

 #11937 := (= uf_9 #3037)

 #18136 := (not #11937)

 #3032 := (uf_48 #3031 uf_7)

 #11928 := (= uf_9 #3032)

 #18127 := (not #11928)

 decl uf_274 :: T1

 #2947 := uf_274

 #3045 := (up_291 uf_287 uf_274 uf_273 1::int uf_4)

 #12949 := (not #3045)

 decl uf_276 :: T1

 #2949 := uf_276

 #3044 := (up_291 uf_287 uf_276 uf_275 0::int uf_4)

 #12958 := (not #3044)

 decl uf_278 :: T1

 #2951 := uf_278

 #3043 := (up_291 uf_287 uf_278 uf_277 uf_295 uf_7)

 #12967 := (not #3043)

 #23209 := (or #12976 #12967 #12958 #12949 #18127 #18136 #23206)

 #23212 := (not #23209)

 #23215 := (or #18127 #18136 #23212)

 #23218 := (not #23215)

 #3034 := (uf_24 uf_287 #3031)

 #11931 := (= uf_9 #3034)

 #18130 := (not #11931)

 #23221 := (or #18127 #18130 #23218)

 #23224 := (not #23221)

 #23227 := (or #18127 #18130 #23224)

 #23230 := (not #23227)

 decl uf_200 :: (-> T4 T5 T5 T16 T2)

 decl uf_282 :: T16

 #2957 := uf_282

 #3029 := (uf_200 uf_287 #2981 #2981 uf_282)

 #11925 := (= uf_9 #3029)

 #13009 := (not #11925)

 #23233 := (or #13009 #23230)

 #23236 := (not #23233)

 #24545 := (uf_116 #2981)

 #25933 := (uf_43 #2977 #24545)

 #26480 := (uf_200 uf_287 #25933 #25933 uf_282)

 #26725 := (= #26480 #3029)

 #26728 := (= #3029 #26480)

 #25940 := (= #2981 #25933)

 #2986 := (uf_48 #2981 #2977)

 #11869 := (= uf_9 #2986)

 decl uf_23 :: (-> T3 T2)

 #2993 := (uf_23 #2977)

 #11881 := (= uf_9 #2993)

 #2990 := (uf_12 #2977)

 #11875 := (= uf_14 #2990)

 #11878 := (not #11875)

 #2988 := (uf_24 uf_287 #2981)

 #11872 := (= uf_9 #2988)

 #11866 := (= uf_26 #2984)

 #2982 := (uf_27 uf_287 #2981)

 #11862 := (= uf_9 #2982)

 #13937 := (and #11862 #11866 #11869 #11872 #11878 #11881)

 decl uf_283 :: int

 #2961 := uf_283

 #13993 := (* -1::int uf_283)

 decl uf_78 :: int

 #429 := uf_78

 #13994 := (+ uf_78 #13993)

 #13992 := (>= #13994 0::int)

 #13990 := (>= uf_283 0::int)

 #13997 := (and #13990 #13992)

 #14000 := (not #13997)

 decl uf_284 :: int

 #2965 := uf_284

 #13979 := (* -1::int uf_284)

 decl uf_76 :: int

 #409 := uf_76

 #13980 := (+ uf_76 #13979)

 #13978 := (>= #13980 0::int)

 #13976 := (>= uf_284 0::int)

 #13983 := (and #13976 #13978)

 #13986 := (not #13983)

 decl uf_285 :: int

 #2969 := uf_285

 #13965 := (* -1::int uf_285)

 #13966 := (+ uf_76 #13965)

 #13964 := (>= #13966 0::int)

 #13962 := (>= uf_285 0::int)

 #13969 := (and #13962 #13964)

 #13972 := (not #13969)

 #1042 := 1099511627776::int

 #13950 := (>= uf_286 1099511627776::int)

 #13940 := (not #13937)

 decl uf_289 :: (-> T19 int)

 #3007 := (:var 0 T19)

 #3008 := (uf_289 #3007)

 #3009 := (pattern #3008)

 decl uf_290 :: int

 #3010 := uf_290

 #13927 := (* -1::int uf_290)

 #13928 := (+ #3008 #13927)

 #13926 := (>= #13928 0::int)

 #13925 := (not #13926)

 #13931 := (forall (vars (?x771 T19)) (:pat #3009) #13925)

 #13934 := (not #13931)

 #13218 := (not #13217)

 #13781 := (and #3042 #13218)

 #13786 := (not #13781)

 #13769 := (+ uf_78 #13715)

 #13768 := (>= #13769 0::int)

 #13772 := (and #13765 #13768)

 #13775 := (not #13772)

 #13756 := (+ uf_76 #13686)

 #13755 := (>= #13756 0::int)

 #13759 := (and #13222 #13755)

 #13762 := (not #13759)

 #13247 := (+ uf_76 #13246)

 #13746 := (>= #13247 0::int)

 #13749 := (and #13743 #13746)

 #13752 := (not #13749)

 #4355 := (* -1::int uf_76)

 #4356 := (+ #161 #4355)

 #4357 := (<= #4356 0::int)

 #4364 := (and #4043 #4357)

 #5579 := (not #4364)

 #13726 := (or #5579 #13703 #13717)

 #13731 := (forall (vars (?x775 int)) #13726)

 #13734 := (not #13731)

 #13689 := (not #13688)

 #13695 := (and #11989 #13689)

 #13700 := (not #13695)

 #13540 := (not #13538)

 #13578 := (and #3103 #4043 #4357 #13540)

 #13583 := (exists (vars (?x778 int)) #13578)

 #13561 := (or #5579 #13538 #13552)

 #13566 := (forall (vars (?x776 int)) #13561)

 #13586 := (not #13566)

 #13592 := (or #13586 #13583)

 #13597 := (and #13566 #13592)

 #13227 := (and #13222 #13225)

 #13230 := (not #13227)

 decl up_216 :: bool

 #2482 := up_216

 #12113 := (not up_216)

 #13624 := (or #12113 #12079 #12070 #12061 #12052 #13230 #13597)

 #13629 := (and up_216 #13624)

 #13654 := (or #13230 #13511 #13629)

 #13245 := (>= #13247 1::int)

 #13334 := (and #13243 #13245)

 #13337 := (not #13334)

 #13304 := (not #13303)

 #13310 := (and #12352 #13304)

 #13290 := (or #5579 #13267 #13281)

 #13295 := (forall (vars (?x785 int)) #13290)

 #13298 := (not #13295)

 #13315 := (or #13298 #13310)

 #13318 := (and #13295 #13315)

 #13321 := (or #13264 #13318)

 #13324 := (and #13259 #13321)

 #13253 := (and #13234 #13251)

 #13256 := (not #13253)

 #13352 := (or #12401 #13256 #13324 #13331 #13337)

 #13360 := (and #13243 #13245 #13352)

 #13236 := (and #13225 #13234)

 #13239 := (not #13236)

 #13471 := (or #12566 #12557 #13230 #13239 #13360 #13416)

 #12305 := (and #12293 #12302)

 #12494 := (not #12305)

 #13392 := (or #12476 #12467 #12494 #12485 #12449 #12440 #13365 #13239 #13360)

 #13400 := (and #12293 #12302 #13392)

 #12299 := (and #12293 #12296)

 #12506 := (not #12299)

 #13405 := (or #12506 #13400)

 #13411 := (and #12293 #12296 #13405)

 #13441 := (or #13230 #13411 #13417)

 #13476 := (and #13441 #13471)

 #13485 := (or #12494 #13230 #13476)

 #13493 := (and #12293 #12302 #13485)

 #13498 := (or #12506 #13493)

 #13504 := (and #12293 #12296 #13498)

 #13533 := (or #13230 #13504 #13510)

 #13659 := (and #13533 #13654)

 decl uf_55 :: (-> T4 T2)

 #3004 := (uf_55 uf_287)

 #11905 := (= uf_9 #3004)

 #12003 := (and #11905 #11997)

 #12141 := (not #12003)

 #3176 := (and #3174 #3175)

 #12733 := (not #3176)

 #13852 := (or #12769 #12760 #12751 #12742 #12733 #12141 #13683 #13230 #13659 #13700 #13734 #13740 #13752 #13762 #13775 #13786)

 #13860 := (and #3042 #13218 #13852)

 #13206 := (or #5579 #13184 #13196)

 #13211 := (forall (vars (?x773 int)) #13206)

 #13214 := (not #13211)

 #13865 := (or #13214 #13860)

 #13868 := (and #13211 #13865)

 #13871 := (or #13181 #13868)

 #13874 := (and #13178 #13871)

 #11940 := (and #11928 #11937)

 #12985 := (not #11940)

 #13895 := (or #12976 #12967 #12958 #12949 #12985 #13874)

 #13903 := (and #11928 #11937 #13895)

 #11934 := (and #11928 #11931)

 #12997 := (not #11934)

 #13908 := (or #12997 #13903)

 #13914 := (and #11928 #11931 #13908)

 #13919 := (or #13009 #13914)

 #13922 := (and #11925 #13919)

 #13152 := (+ uf_76 #13151)

 #13150 := (>= #13152 0::int)

 #13148 := (>= uf_286 0::int)

 #13155 := (and #13148 #13150)

 #13158 := (not #13155)

 decl uf_294 :: (-> int T5 T2)

 decl uf_293 :: int

 #3018 := uf_293

 #3021 := (uf_294 uf_293 #23)

 #3022 := (pattern #3021)

 #11911 := (= uf_9 #3021)

 #11917 := (not #11911)

 #11922 := (forall (vars (?x772 T5)) (:pat #3022) #11917)

 #13030 := (not #11922)

 decl uf_281 :: T1

 #2954 := uf_281

 #3002 := (uf_202 uf_281 uf_287)

 #11902 := (= uf_9 #3002)

 #11908 := (and #11902 #11905)

 #13075 := (not #11908)

 decl uf_203 :: (-> T4 T2)

 #3000 := (uf_203 uf_287)

 #11899 := (= uf_9 #3000)

 #13084 := (not #11899)

 decl uf_173 :: (-> T4 int)

 #3019 := (uf_173 uf_287)

 #3020 := (= uf_293 #3019)

 #13039 := (not #3020)

 #3017 := (up_291 uf_287 uf_281 uf_279 uf_286 uf_4)

 #13048 := (not #3017)

 #3015 := (up_292 uf_287 uf_281 uf_280 #2979 #11)

 #3014 := (up_291 uf_287 uf_281 uf_280 #3013 #11)

 #3016 := (and #3014 #3015)

 #13057 := (not #3016)

 #14045 := (or #13057 #13048 #13039 #13084 #13075 #13030 #13158 #13217 #13922 #13934 #13940 #13950 #13972 #13986 #14000)

 #14050 := (not #14045)

 #1 := true

 #3098 := (< #161 uf_286)

 #3104 := (and #3098 #3103)

 #411 := (<= #161 uf_76)

 #3105 := (and #411 #3104)

 #285 := (<= 0::int #161)

 #3106 := (and #285 #3105)

 #3107 := (exists (vars (?x778 int)) #3106)

 #3108 := (and #3107 true)

 #3099 := (<= #3054 uf_302)

 #3100 := (implies #3098 #3099)

 #412 := (and #285 #411)

 #3101 := (implies #412 #3100)

 #3102 := (forall (vars (?x776 int)) #3101)

 #3109 := (implies #3102 #3108)

 #3110 := (and #3102 #3109)

 #3097 := (= uf_302 uf_296)

 #3111 := (implies #3097 #3110)

 #3095 := (= uf_301 uf_297)

 #3112 := (implies #3095 #3111)

 #3093 := (= uf_300 uf_298)

 #3113 := (implies #3093 #3112)

 #3091 := (= uf_299 uf_296)

 #3114 := (implies #3091 #3113)

 #3066 := (<= 0::int uf_297)

 #3073 := (<= 1::int uf_298)

 #3074 := (and #3073 #3066)

 #3115 := (implies #3074 #3114)

 #3116 := (implies #3074 #3115)

 #3117 := (implies #3074 #3116)

 #3118 := (implies up_216 #3117)

 #3119 := (and up_216 #3118)

 #3120 := (implies #3074 #3119)

 #3121 := (implies #3074 #3120)

 #3269 := (implies #3074 #3121)

 #3270 := (implies #3074 #3269)

 #3268 := (<= uf_286 uf_298)

 #3271 := (implies #3268 #3270)

 #3272 := (implies #3074 #3271)

 #3221 := (= #3220 uf_304)

 #3218 := (< uf_305 uf_286)

 #3222 := (and #3218 #3221)

 #3223 := (and #3222 true)

 #3214 := (<= #3054 uf_304)

 #3213 := (< #161 uf_306)

 #3215 := (implies #3213 #3214)

 #3216 := (implies #412 #3215)

 #3217 := (forall (vars (?x785 int)) #3216)

 #3224 := (implies #3217 #3223)

 #3225 := (and #3217 #3224)

 #3212 := (<= uf_306 uf_286)

 #3226 := (implies #3212 #3225)

 #3227 := (and #3212 #3226)

 #3201 := (<= 0::int uf_305)

 #3210 := (<= 2::int uf_306)

 #3211 := (and #3210 #3201)

 #3228 := (implies #3211 #3227)

 #3229 := (implies #3209 #3228)

 #3203 := (+ uf_298 1::int)

 #3208 := (= uf_306 #3203)

 #3230 := (implies #3208 #3229)

 #3205 := (<= #3203 uf_76)

 #3204 := (<= 0::int #3203)

 #3206 := (and #3204 #3205)

 #3231 := (implies #3206 #3230)

 #3232 := (and #3206 #3231)

 #3202 := (and #3073 #3201)

 #3233 := (implies #3202 #3232)

 #3250 := (= uf_305 uf_297)

 #3251 := (implies #3250 #3233)

 #3249 := (= uf_304 uf_296)

 #3252 := (implies #3249 #3251)

 #3253 := (implies #3074 #3252)

 #3254 := (implies #3074 #3253)

 #3255 := (implies #3074 #3254)

 #3248 := (<= #3190 uf_296)

 #3256 := (implies #3248 #3255)

 #3257 := (implies #3074 #3256)

 #3200 := (= uf_305 uf_298)

 #3234 := (implies #3200 #3233)

 #3198 := (= uf_304 uf_303)

 #3235 := (implies #3198 #3234)

 #3196 := (and #3073 #3073)

 #3236 := (implies #3196 #3235)

 #3237 := (implies #3195 #3236)

 #3238 := (implies #3194 #3237)

 #3193 := (= uf_303 #3190)

 #3239 := (implies #3193 #3238)

 #3188 := (= #3187 uf_9)

 #3183 := (= #3182 uf_9)

 #3189 := (and #3183 #3188)

 #3240 := (implies #3189 #3239)

 #3241 := (and #3189 #3240)

 #3185 := (= #3184 uf_9)

 #3186 := (and #3183 #3185)

 #3242 := (implies #3186 #3241)

 #3243 := (and #3186 #3242)

 #3244 := (implies #3074 #3243)

 #3245 := (implies #3074 #3244)

 #3191 := (< uf_296 #3190)

 #3246 := (implies #3191 #3245)

 #3247 := (implies #3074 #3246)

 #3258 := (and #3247 #3257)

 #3259 := (implies #3074 #3258)

 #3260 := (implies #3189 #3259)

 #3261 := (and #3189 #3260)

 #3262 := (implies #3186 #3261)

 #3263 := (and #3186 #3262)

 #3264 := (implies #3074 #3263)

 #3265 := (implies #3074 #3264)

 #3180 := (< uf_298 uf_286)

 #3266 := (implies #3180 #3265)

 #3267 := (implies #3074 #3266)

 #3273 := (and #3267 #3272)

 #3274 := (implies #3074 #3273)

 decl uf_41 :: (-> T4 T12)

 #3127 := (uf_41 uf_287)

 #3178 := (= #3127 #3127)

 #3177 := (= #3150 #3150)

 #3179 := (and #3177 #3178)

 #3275 := (implies #3179 #3274)

 #3276 := (implies #3176 #3275)

 #3277 := (implies #3173 #3276)

 #3278 := (implies #3172 #3277)

 #3279 := (implies #3171 #3278)

 #3280 := (implies #3170 #3279)

 #3005 := (= #3004 uf_9)

 #3088 := (= #3087 uf_9)

 #3089 := (and #3088 #3005)

 #3281 := (implies #3089 #3280)

 #3163 := (= #3162 uf_9)

 decl uf_172 :: (-> T4 T5 int)

 #3158 := (uf_172 uf_287 #23)

 #3159 := (pattern #3158)

 #3160 := (<= #3158 #3158)

 #3161 := (forall (vars (?x783 T5)) (:pat #3159) #3160)

 #3164 := (and #3161 #3163)

 #3157 := (<= #3019 #3019)

 #3165 := (and #3157 #3164)

 #3282 := (implies #3165 #3281)

 #3151 := (uf_58 #3150 #23)

 #3152 := (pattern #3151)

 #3140 := (uf_68 uf_287 #23)

 #3141 := (= #3140 uf_9)

 #3153 := (= #3151 #3151)

 #3154 := (and #3153 #3141)

 #3155 := (implies #3141 #3154)

 #3156 := (forall (vars (?x782 T5)) (:pat #3152) #3155)

 #3166 := (and #3156 #3165)

 decl uf_40 :: (-> T12 T5 T11)

 #3128 := (uf_40 #3127 #23)

 #3129 := (pattern #3128)

 #3146 := (= #3128 #3128)

 #3147 := (and #3146 #3141)

 #3148 := (implies #3141 #3147)

 #3149 := (forall (vars (?x781 T5)) (:pat #3129) #3148)

 #3167 := (and #3149 #3166)

 decl uf_19 :: (-> T9 T5 int)

 decl uf_20 :: (-> T4 T9)

 #3137 := (uf_20 uf_287)

 #3138 := (uf_19 #3137 #23)

 #3139 := (pattern #3138)

 #3142 := (= #3138 #3138)

 #3143 := (and #3142 #3141)

 #3144 := (implies #3141 #3143)

 #3145 := (forall (vars (?x780 T5)) (:pat #3139) #3144)

 #3168 := (and #3145 #3167)

 decl uf_261 :: T8

 #2837 := uf_261

 #3130 := (uf_25 uf_287 #23)

 #3131 := (uf_13 #3130)

 #3132 := (uf_12 #3131)

 #3133 := (= #3132 uf_261)

 #3134 := (not #3133)

 #3135 := (implies #3134 #3134)

 #3136 := (forall (vars (?x779 T5)) (:pat #3129) #3135)

 #3169 := (and #3136 #3168)

 #3283 := (implies #3169 #3282)

 #3284 := (implies #3074 #3283)

 #3285 := (implies #3074 #3284)

 #3286 := (implies #3074 #3285)

 #3122 := (implies #3089 #3121)

 #3123 := (implies #3074 #3122)

 #3124 := (implies #3074 #3123)

 #3086 := (not true)

 #3125 := (implies #3086 #3124)

 #3126 := (implies #3074 #3125)

 #3287 := (and #3126 #3286)

 #3288 := (implies #3074 #3287)

 #3084 := (= #3083 uf_296)

 #3081 := (< uf_297 uf_286)

 #3085 := (and #3081 #3084)

 #3289 := (implies #3085 #3288)

 #3077 := (<= #3054 uf_296)

 #3076 := (< #161 uf_298)

 #3078 := (implies #3076 #3077)

 #3079 := (implies #412 #3078)

 #3080 := (forall (vars (?x775 int)) #3079)

 #3290 := (implies #3080 #3289)

 #3075 := (<= uf_298 uf_286)

 #3291 := (implies #3075 #3290)

 #3292 := (implies #3074 #3291)

 #3071 := (<= uf_298 uf_76)

 #3070 := (<= 0::int uf_298)

 #3072 := (and #3070 #3071)

 #3293 := (implies #3072 #3292)

 #3067 := (<= uf_297 uf_76)

 #3068 := (and #3066 #3067)

 #3294 := (implies #3068 #3293)

 #3063 := (<= uf_296 uf_78)

 #3062 := (<= 0::int uf_296)

 #3064 := (and #3062 #3063)

 #3295 := (implies #3064 #3294)

 #3059 := (= #3041 uf_295)

 #2975 := (< 0::int uf_286)

 #3060 := (and #2975 #3059)

 #3296 := (implies #3060 #3295)

 #3297 := (and #3060 #3296)

 #3055 := (<= #3054 uf_295)

 #3052 := (< #161 1::int)

 #3056 := (implies #3052 #3055)

 #3057 := (implies #412 #3056)

 #3058 := (forall (vars (?x773 int)) #3057)

 #3298 := (implies #3058 #3297)

 #3299 := (and #3058 #3298)

 #3051 := (<= 1::int uf_286)

 #3300 := (implies #3051 #3299)

 #3301 := (and #3051 #3300)

 #3047 := (<= 0::int 0::int)

 #3048 := (and #3047 #3047)

 #3046 := (<= 1::int 1::int)

 #3049 := (and #3046 #3048)

 #3050 := (and #3046 #3049)

 #3302 := (implies #3050 #3301)

 #3303 := (implies #3045 #3302)

 #3304 := (implies #3044 #3303)

 #3305 := (implies #3043 #3304)

 #3306 := (implies #3042 #3305)

 #3038 := (= #3037 uf_9)

 #3033 := (= #3032 uf_9)

 #3039 := (and #3033 #3038)

 #3307 := (implies #3039 #3306)

 #3308 := (and #3039 #3307)

 #3035 := (= #3034 uf_9)

 #3036 := (and #3033 #3035)

 #3309 := (implies #3036 #3308)

 #3310 := (and #3036 #3309)

 #3030 := (= #3029 uf_9)

 #3311 := (implies #3030 #3310)

 #3312 := (and #3030 #3311)

 #3027 := (<= uf_286 uf_76)

 #3026 := (<= 0::int uf_286)

 #3028 := (and #3026 #3027)

 #3313 := (implies #3028 #3312)

 #3023 := (= #3021 uf_9)

 #3024 := (iff #3023 false)

 #3025 := (forall (vars (?x772 T5)) (:pat #3022) #3024)

 #3314 := (implies #3025 #3313)

 #3315 := (implies #3020 #3314)

 #3316 := (implies #3017 #3315)

 #3317 := (implies #3016 #3316)

 #3011 := (< #3008 uf_290)

 #3012 := (forall (vars (?x771 T19)) (:pat #3009) #3011)

 #3318 := (implies #3012 #3317)

 #3003 := (= #3002 uf_9)

 #3006 := (and #3003 #3005)

 #3319 := (implies #3006 #3318)

 #3001 := (= #3000 uf_9)

 #3320 := (implies #3001 #3319)

 #2994 := (= #2993 uf_9)

 #2991 := (= #2990 uf_14)

 #2992 := (not #2991)

 #2995 := (and #2992 #2994)

 #2989 := (= #2988 uf_9)

 #2996 := (and #2989 #2995)

 #2987 := (= #2986 uf_9)

 #2997 := (and #2987 #2996)

 #2985 := (= #2984 uf_26)

 #2998 := (and #2985 #2997)

 #2983 := (= #2982 uf_9)

 #2999 := (and #2983 #2998)

 #3321 := (implies #2999 #3320)

 #3322 := (implies #2975 #3321)

 #2974 := (< uf_286 1099511627776::int)

 #3323 := (implies #2974 #3322)

 #2971 := (<= uf_285 uf_76)

 #2970 := (<= 0::int uf_285)

 #2972 := (and #2970 #2971)

 #3324 := (implies #2972 #3323)

 #2967 := (<= uf_284 uf_76)

 #2966 := (<= 0::int uf_284)

 #2968 := (and #2966 #2967)

 #3325 := (implies #2968 #3324)

 #2963 := (<= uf_283 uf_78)

 #2962 := (<= 0::int uf_283)

 #2964 := (and #2962 #2963)

 #3326 := (implies #2964 #3325)

 #3327 := (not #3326)

 #14053 := (iff #3327 #14050)

 #12020 := (not #3098)

 #12021 := (or #12020 #3099)

 #5570 := (not #412)

 #12027 := (or #5570 #12021)

 #12032 := (forall (vars (?x776 int)) #12027)

 #12040 := (not #12032)

 #12041 := (or #3107 #12040)

 #12046 := (and #12032 #12041)

 #12053 := (or #12052 #12046)

 #12062 := (or #12061 #12053)

 #12071 := (or #12070 #12062)

 #12080 := (or #12079 #12071)

 #11971 := (and #3066 #3073)

 #12088 := (not #11971)

 #12089 := (or #12088 #12080)

 #12097 := (or #12088 #12089)

 #12105 := (or #12088 #12097)

 #12114 := (or #12113 #12105)

 #12119 := (and up_216 #12114)

 #12125 := (or #12088 #12119)

 #12133 := (or #12088 #12125)

 #12682 := (or #12088 #12133)

 #12690 := (or #12088 #12682)

 #12698 := (not #3268)

 #12699 := (or #12698 #12690)

 #12707 := (or #12088 #12699)

 #12355 := (and #3218 #12352)

 #12337 := (not #3213)

 #12338 := (or #12337 #3214)

 #12344 := (or #5570 #12338)

 #12349 := (forall (vars (?x785 int)) #12344)

 #12368 := (not #12349)

 #12369 := (or #12368 #12355)

 #12374 := (and #12349 #12369)

 #12380 := (not #3212)

 #12381 := (or #12380 #12374)

 #12386 := (and #3212 #12381)

 #12334 := (and #3201 #3210)

 #12392 := (not #12334)

 #12393 := (or #12392 #12386)

 #12402 := (or #12401 #12393)

 #12319 := (+ 1::int uf_298)

 #12331 := (= uf_306 #12319)

 #12410 := (not #12331)

 #12411 := (or #12410 #12402)

 #12325 := (<= #12319 uf_76)

 #12322 := (<= 0::int #12319)

 #12328 := (and #12322 #12325)

 #12419 := (not #12328)

 #12420 := (or #12419 #12411)

 #12425 := (and #12328 #12420)

 #12431 := (not #3202)

 #12432 := (or #12431 #12425)

 #12558 := (or #12432 #12557)

 #12567 := (or #12566 #12558)

 #12575 := (or #12088 #12567)

 #12583 := (or #12088 #12575)

 #12591 := (or #12088 #12583)

 #12599 := (not #3248)

 #12600 := (or #12599 #12591)

 #12608 := (or #12088 #12600)

 #12441 := (or #12440 #12432)

 #12450 := (or #12449 #12441)

 #12458 := (not #3073)

 #12459 := (or #12458 #12450)

 #12468 := (or #12467 #12459)

 #12477 := (or #12476 #12468)

 #12486 := (or #12485 #12477)

 #12495 := (or #12494 #12486)

 #12500 := (and #12305 #12495)

 #12507 := (or #12506 #12500)

 #12512 := (and #12299 #12507)

 #12518 := (or #12088 #12512)

 #12526 := (or #12088 #12518)

 #12534 := (not #3191)

 #12535 := (or #12534 #12526)

 #12543 := (or #12088 #12535)

 #12613 := (and #12543 #12608)

 #12619 := (or #12088 #12613)

 #12627 := (or #12494 #12619)

 #12632 := (and #12305 #12627)

 #12638 := (or #12506 #12632)

 #12643 := (and #12299 #12638)

 #12649 := (or #12088 #12643)

 #12657 := (or #12088 #12649)

 #12665 := (not #3180)

 #12666 := (or #12665 #12657)

 #12674 := (or #12088 #12666)

 #12712 := (and #12674 #12707)

 #12718 := (or #12088 #12712)

 #12734 := (or #12733 #12718)

 #12743 := (or #12742 #12734)

 #12752 := (or #12751 #12743)

 #12761 := (or #12760 #12752)

 #12770 := (or #12769 #12761)

 #12778 := (or #12141 #12770)

 #12257 := (and #3161 #12254)

 #12260 := (and #3157 #12257)

 #12786 := (not #12260)

 #12787 := (or #12786 #12778)

 #12795 := (or #12786 #12787)

 #12803 := (or #12088 #12795)

 #12811 := (or #12088 #12803)

 #12819 := (or #12088 #12811)

 #12834 := (or #12088 #12819)

 #11992 := (and #3081 #11989)

 #12842 := (not #11992)

 #12843 := (or #12842 #12834)

 #11974 := (not #3076)

 #11975 := (or #11974 #3077)

 #11981 := (or #5570 #11975)

 #11986 := (forall (vars (?x775 int)) #11981)

 #12851 := (not #11986)

 #12852 := (or #12851 #12843)

 #12860 := (not #3075)

 #12861 := (or #12860 #12852)

 #12869 := (or #12088 #12861)

 #12877 := (not #3072)

 #12878 := (or #12877 #12869)

 #12886 := (not #3068)

 #12887 := (or #12886 #12878)

 #12895 := (not #3064)

 #12896 := (or #12895 #12887)

 #11968 := (and #2975 #3042)

 #12904 := (not #11968)

 #12905 := (or #12904 #12896)

 #12910 := (and #11968 #12905)

 #11951 := (not #3052)

 #11952 := (or #11951 #3055)

 #11958 := (or #5570 #11952)

 #11963 := (forall (vars (?x773 int)) #11958)

 #12916 := (not #11963)

 #12917 := (or #12916 #12910)

 #12922 := (and #11963 #12917)

 #12928 := (not #3051)

 #12929 := (or #12928 #12922)

 #12934 := (and #3051 #12929)

 #11945 := (and #3046 #3047)

 #11948 := (and #3046 #11945)

 #12940 := (not #11948)

 #12941 := (or #12940 #12934)

 #12950 := (or #12949 #12941)

 #12959 := (or #12958 #12950)

 #12968 := (or #12967 #12959)

 #12977 := (or #12976 #12968)

 #12986 := (or #12985 #12977)

 #12991 := (and #11940 #12986)

 #12998 := (or #12997 #12991)

 #13003 := (and #11934 #12998)

 #13010 := (or #13009 #13003)

 #13015 := (and #11925 #13010)

 #13021 := (not #3028)

 #13022 := (or #13021 #13015)

 #13031 := (or #13030 #13022)

 #13040 := (or #13039 #13031)

 #13049 := (or #13048 #13040)

 #13058 := (or #13057 #13049)

 #13066 := (not #3012)

 #13067 := (or #13066 #13058)

 #13076 := (or #13075 #13067)

 #13085 := (or #13084 #13076)

 #11884 := (and #11878 #11881)

 #11887 := (and #11872 #11884)

 #11890 := (and #11869 #11887)

 #11893 := (and #11866 #11890)

 #11896 := (and #11862 #11893)

 #13093 := (not #11896)

 #13094 := (or #13093 #13085)

 #13102 := (not #2975)

 #13103 := (or #13102 #13094)

 #13111 := (not #2974)

 #13112 := (or #13111 #13103)

 #13120 := (not #2972)

 #13121 := (or #13120 #13112)

 #13129 := (not #2968)

 #13130 := (or #13129 #13121)

 #13138 := (not #2964)

 #13139 := (or #13138 #13130)

 #13144 := (not #13139)

 #14051 := (iff #13144 #14050)

 #14048 := (iff #13139 #14045)

 #14003 := (or #13158 #13922)

 #14006 := (or #13030 #14003)

 #14009 := (or #13039 #14006)

 #14012 := (or #13048 #14009)

 #14015 := (or #13057 #14012)

 #14018 := (or #13934 #14015)

 #14021 := (or #13075 #14018)

 #14024 := (or #13084 #14021)

 #14027 := (or #13940 #14024)

 #14030 := (or #13217 #14027)

 #14033 := (or #13950 #14030)

 #14036 := (or #13972 #14033)

 #14039 := (or #13986 #14036)

 #14042 := (or #14000 #14039)

 #14046 := (iff #14042 #14045)

 #14047 := [rewrite]: #14046

 #14043 := (iff #13139 #14042)

 #14040 := (iff #13130 #14039)

 #14037 := (iff #13121 #14036)

 #14034 := (iff #13112 #14033)

 #14031 := (iff #13103 #14030)

 #14028 := (iff #13094 #14027)

 #14025 := (iff #13085 #14024)

 #14022 := (iff #13076 #14021)

 #14019 := (iff #13067 #14018)

 #14016 := (iff #13058 #14015)

 #14013 := (iff #13049 #14012)

 #14010 := (iff #13040 #14009)

 #14007 := (iff #13031 #14006)

 #14004 := (iff #13022 #14003)

 #13923 := (iff #13015 #13922)

 #13920 := (iff #13010 #13919)

 #13917 := (iff #13003 #13914)

 #13911 := (and #11934 #13908)

 #13915 := (iff #13911 #13914)

 #13916 := [rewrite]: #13915

 #13912 := (iff #13003 #13911)

 #13909 := (iff #12998 #13908)

 #13906 := (iff #12991 #13903)

 #13900 := (and #11940 #13895)

 #13904 := (iff #13900 #13903)

 #13905 := [rewrite]: #13904

 #13901 := (iff #12991 #13900)

 #13898 := (iff #12986 #13895)

 #13877 := (or false #13874)

 #13880 := (or #12949 #13877)

 #13883 := (or #12958 #13880)

 #13886 := (or #12967 #13883)

 #13889 := (or #12976 #13886)

 #13892 := (or #12985 #13889)

 #13896 := (iff #13892 #13895)

 #13897 := [rewrite]: #13896

 #13893 := (iff #12986 #13892)

 #13890 := (iff #12977 #13889)

 #13887 := (iff #12968 #13886)

 #13884 := (iff #12959 #13883)

 #13881 := (iff #12950 #13880)

 #13878 := (iff #12941 #13877)

 #13875 := (iff #12934 #13874)

 #13872 := (iff #12929 #13871)

 #13869 := (iff #12922 #13868)

 #13866 := (iff #12917 #13865)

 #13863 := (iff #12910 #13860)

 #13778 := (and #13218 #3042)

 #13857 := (and #13778 #13852)

 #13861 := (iff #13857 #13860)

 #13862 := [rewrite]: #13861

 #13858 := (iff #12910 #13857)

 #13855 := (iff #12905 #13852)

 #13789 := (or #13230 #13659)

 #13792 := (or #12733 #13789)

 #13795 := (or #12742 #13792)

 #13798 := (or #12751 #13795)

 #13801 := (or #12760 #13798)

 #13804 := (or #12769 #13801)

 #13807 := (or #12141 #13804)

 #13810 := (or #13683 #13807)

 #13813 := (or #13683 #13810)

 #13816 := (or #13230 #13813)

 #13819 := (or #13230 #13816)

 #13822 := (or #13230 #13819)

 #13825 := (or #13230 #13822)

 #13828 := (or #13700 #13825)

 #13831 := (or #13734 #13828)

 #13834 := (or #13740 #13831)

 #13837 := (or #13230 #13834)

 #13840 := (or #13752 #13837)

 #13843 := (or #13762 #13840)

 #13846 := (or #13775 #13843)

 #13849 := (or #13786 #13846)

 #13853 := (iff #13849 #13852)

 #13854 := [rewrite]: #13853

 #13850 := (iff #12905 #13849)

 #13847 := (iff #12896 #13846)

 #13844 := (iff #12887 #13843)

 #13841 := (iff #12878 #13840)

 #13838 := (iff #12869 #13837)

 #13835 := (iff #12861 #13834)

 #13832 := (iff #12852 #13831)

 #13829 := (iff #12843 #13828)

 #13826 := (iff #12834 #13825)

 #13823 := (iff #12819 #13822)

 #13820 := (iff #12811 #13819)

 #13817 := (iff #12803 #13816)

 #13814 := (iff #12795 #13813)

 #13811 := (iff #12787 #13810)

 #13808 := (iff #12778 #13807)

 #13805 := (iff #12770 #13804)

 #13802 := (iff #12761 #13801)

 #13799 := (iff #12752 #13798)

 #13796 := (iff #12743 #13795)

 #13793 := (iff #12734 #13792)

 #13790 := (iff #12718 #13789)

 #13660 := (iff #12712 #13659)

 #13657 := (iff #12707 #13654)

 #13636 := (or #13230 #13629)

 #13639 := (or #13230 #13636)

 #13642 := (or #13230 #13639)

 #13645 := (or #13230 #13642)

 #13648 := (or #13511 #13645)

 #13651 := (or #13230 #13648)

 #13655 := (iff #13651 #13654)

 #13656 := [rewrite]: #13655

 #13652 := (iff #12707 #13651)

 #13649 := (iff #12699 #13648)

 #13646 := (iff #12690 #13645)

 #13643 := (iff #12682 #13642)

 #13640 := (iff #12133 #13639)

 #13637 := (iff #12125 #13636)

 #13630 := (iff #12119 #13629)

 #13627 := (iff #12114 #13624)

 #13600 := (or #12052 #13597)

 #13603 := (or #12061 #13600)

 #13606 := (or #12070 #13603)

 #13609 := (or #12079 #13606)

 #13612 := (or #13230 #13609)

 #13615 := (or #13230 #13612)

 #13618 := (or #13230 #13615)

 #13621 := (or #12113 #13618)

 #13625 := (iff #13621 #13624)

 #13626 := [rewrite]: #13625

 #13622 := (iff #12114 #13621)

 #13619 := (iff #12105 #13618)

 #13616 := (iff #12097 #13615)

 #13613 := (iff #12089 #13612)

 #13610 := (iff #12080 #13609)

 #13607 := (iff #12071 #13606)

 #13604 := (iff #12062 #13603)

 #13601 := (iff #12053 #13600)

 #13598 := (iff #12046 #13597)

 #13595 := (iff #12041 #13592)

 #13589 := (or #13583 #13586)

 #13593 := (iff #13589 #13592)

 #13594 := [rewrite]: #13593

 #13590 := (iff #12041 #13589)

 #13587 := (iff #12040 #13586)

 #13567 := (iff #12032 #13566)

 #13564 := (iff #12027 #13561)

 #13555 := (or #13538 #13552)

 #13558 := (or #5579 #13555)

 #13562 := (iff #13558 #13561)

 #13563 := [rewrite]: #13562

 #13559 := (iff #12027 #13558)

 #13556 := (iff #12021 #13555)

 #13553 := (iff #3099 #13552)

 #13554 := [rewrite]: #13553

 #13548 := (iff #12020 #13538)

 #13543 := (not #13540)

 #13546 := (iff #13543 #13538)

 #13547 := [rewrite]: #13546

 #13544 := (iff #12020 #13543)

 #13541 := (iff #3098 #13540)

 #13542 := [rewrite]: #13541

 #13545 := [monotonicity #13542]: #13544

 #13549 := [trans #13545 #13547]: #13548

 #13557 := [monotonicity #13549 #13554]: #13556

 #5580 := (iff #5570 #5579)

 #4365 := (iff #412 #4364)

 #4358 := (iff #411 #4357)

 #4359 := [rewrite]: #4358

 #4041 := (iff #285 #4043)

 #4042 := [rewrite]: #4041

 #4366 := [monotonicity #4042 #4359]: #4365

 #5581 := [monotonicity #4366]: #5580

 #13560 := [monotonicity #5581 #13557]: #13559

 #13565 := [trans #13560 #13563]: #13564

 #13568 := [quant-intro #13565]: #13567

 #13588 := [monotonicity #13568]: #13587

 #13584 := (iff #3107 #13583)

 #13581 := (iff #3106 #13578)

 #13569 := (and #13540 #3103)

 #13572 := (and #4357 #13569)

 #13575 := (and #4043 #13572)

 #13579 := (iff #13575 #13578)

 #13580 := [rewrite]: #13579

 #13576 := (iff #3106 #13575)

 #13573 := (iff #3105 #13572)

 #13570 := (iff #3104 #13569)

 #13571 := [monotonicity #13542]: #13570

 #13574 := [monotonicity #4359 #13571]: #13573

 #13577 := [monotonicity #4042 #13574]: #13576

 #13582 := [trans #13577 #13580]: #13581

 #13585 := [quant-intro #13582]: #13584

 #13591 := [monotonicity #13585 #13588]: #13590

 #13596 := [trans #13591 #13594]: #13595

 #13599 := [monotonicity #13568 #13596]: #13598

 #13602 := [monotonicity #13599]: #13601

 #13605 := [monotonicity #13602]: #13604

 #13608 := [monotonicity #13605]: #13607

 #13611 := [monotonicity #13608]: #13610

 #13231 := (iff #12088 #13230)

 #13228 := (iff #11971 #13227)

 #13224 := (iff #3073 #13225)

 #13226 := [rewrite]: #13224

 #13221 := (iff #3066 #13222)

 #13223 := [rewrite]: #13221

 #13229 := [monotonicity #13223 #13226]: #13228

 #13232 := [monotonicity #13229]: #13231

 #13614 := [monotonicity #13232 #13611]: #13613

 #13617 := [monotonicity #13232 #13614]: #13616

 #13620 := [monotonicity #13232 #13617]: #13619

 #13623 := [monotonicity #13620]: #13622

 #13628 := [trans #13623 #13626]: #13627

 #13631 := [monotonicity #13628]: #13630

 #13638 := [monotonicity #13232 #13631]: #13637

 #13641 := [monotonicity #13232 #13638]: #13640

 #13644 := [monotonicity #13232 #13641]: #13643

 #13647 := [monotonicity #13232 #13644]: #13646

 #13634 := (iff #12698 #13511)

 #13632 := (iff #3268 #13510)

 #13633 := [rewrite]: #13632

 #13635 := [monotonicity #13633]: #13634

 #13650 := [monotonicity #13635 #13647]: #13649

 #13653 := [monotonicity #13232 #13650]: #13652

 #13658 := [trans #13653 #13656]: #13657

 #13536 := (iff #12674 #13533)

 #13521 := (or #13230 #13504)

 #13524 := (or #13230 #13521)

 #13527 := (or #13510 #13524)

 #13530 := (or #13230 #13527)

 #13534 := (iff #13530 #13533)

 #13535 := [rewrite]: #13534

 #13531 := (iff #12674 #13530)

 #13528 := (iff #12666 #13527)

 #13525 := (iff #12657 #13524)

 #13522 := (iff #12649 #13521)

 #13507 := (iff #12643 #13504)

 #13501 := (and #12299 #13498)

 #13505 := (iff #13501 #13504)

 #13506 := [rewrite]: #13505

 #13502 := (iff #12643 #13501)

 #13499 := (iff #12638 #13498)

 #13496 := (iff #12632 #13493)

 #13490 := (and #12305 #13485)

 #13494 := (iff #13490 #13493)

 #13495 := [rewrite]: #13494

 #13491 := (iff #12632 #13490)

 #13488 := (iff #12627 #13485)

 #13479 := (or #13230 #13476)

 #13482 := (or #12494 #13479)

 #13486 := (iff #13482 #13485)

 #13487 := [rewrite]: #13486

 #13483 := (iff #12627 #13482)

 #13480 := (iff #12619 #13479)

 #13477 := (iff #12613 #13476)

 #13474 := (iff #12608 #13471)

 #13368 := (or #13239 #13360)

 #13450 := (or #13368 #12557)

 #13453 := (or #12566 #13450)

 #13456 := (or #13230 #13453)

 #13459 := (or #13230 #13456)

 #13462 := (or #13230 #13459)

 #13465 := (or #13416 #13462)

 #13468 := (or #13230 #13465)

 #13472 := (iff #13468 #13471)

 #13473 := [rewrite]: #13472

 #13469 := (iff #12608 #13468)

 #13466 := (iff #12600 #13465)

 #13463 := (iff #12591 #13462)

 #13460 := (iff #12583 #13459)

 #13457 := (iff #12575 #13456)

 #13454 := (iff #12567 #13453)

 #13451 := (iff #12558 #13450)

 #13369 := (iff #12432 #13368)

 #13363 := (iff #12425 #13360)

 #13357 := (and #13334 #13352)

 #13361 := (iff #13357 #13360)

 #13362 := [rewrite]: #13361

 #13358 := (iff #12425 #13357)

 #13355 := (iff #12420 #13352)

 #13340 := (or #13256 #13324)

 #13343 := (or #12401 #13340)

 #13346 := (or #13331 #13343)

 #13349 := (or #13337 #13346)

 #13353 := (iff #13349 #13352)

 #13354 := [rewrite]: #13353

 #13350 := (iff #12420 #13349)

 #13347 := (iff #12411 #13346)

 #13344 := (iff #12402 #13343)

 #13341 := (iff #12393 #13340)

 #13325 := (iff #12386 #13324)

 #13322 := (iff #12381 #13321)

 #13319 := (iff #12374 #13318)

 #13316 := (iff #12369 #13315)

 #13313 := (iff #12355 #13310)

 #13307 := (and #13304 #12352)

 #13311 := (iff #13307 #13310)

 #13312 := [rewrite]: #13311

 #13308 := (iff #12355 #13307)

 #13305 := (iff #3218 #13304)

 #13306 := [rewrite]: #13305

 #13309 := [monotonicity #13306]: #13308

 #13314 := [trans #13309 #13312]: #13313

 #13299 := (iff #12368 #13298)

 #13296 := (iff #12349 #13295)

 #13293 := (iff #12344 #13290)

 #13284 := (or #13267 #13281)

 #13287 := (or #5579 #13284)

 #13291 := (iff #13287 #13290)

 #13292 := [rewrite]: #13291

 #13288 := (iff #12344 #13287)

 #13285 := (iff #12338 #13284)

 #13282 := (iff #3214 #13281)

 #13283 := [rewrite]: #13282

 #13277 := (iff #12337 #13267)

 #13269 := (not #13267)

 #13272 := (not #13269)

 #13275 := (iff #13272 #13267)

 #13276 := [rewrite]: #13275

 #13273 := (iff #12337 #13272)

 #13270 := (iff #3213 #13269)

 #13271 := [rewrite]: #13270

 #13274 := [monotonicity #13271]: #13273

 #13278 := [trans #13274 #13276]: #13277

 #13286 := [monotonicity #13278 #13283]: #13285

 #13289 := [monotonicity #5581 #13286]: #13288

 #13294 := [trans #13289 #13292]: #13293

 #13297 := [quant-intro #13294]: #13296

 #13300 := [monotonicity #13297]: #13299

 #13317 := [monotonicity #13300 #13314]: #13316

 #13320 := [monotonicity #13297 #13317]: #13319

 #13265 := (iff #12380 #13264)

 #13262 := (iff #3212 #13259)

 #13263 := [rewrite]: #13262

 #13266 := [monotonicity #13263]: #13265

 #13323 := [monotonicity #13266 #13320]: #13322

 #13326 := [monotonicity #13263 #13323]: #13325

 #13257 := (iff #12392 #13256)

 #13254 := (iff #12334 #13253)

 #13250 := (iff #3210 #13251)

 #13252 := [rewrite]: #13250

 #13233 := (iff #3201 #13234)

 #13235 := [rewrite]: #13233

 #13255 := [monotonicity #13235 #13252]: #13254

 #13258 := [monotonicity #13255]: #13257

 #13342 := [monotonicity #13258 #13326]: #13341

 #13345 := [monotonicity #13342]: #13344

 #13332 := (iff #12410 #13331)

 #13329 := (iff #12331 #13327)

 #13330 := [rewrite]: #13329

 #13333 := [monotonicity #13330]: #13332

 #13348 := [monotonicity #13333 #13345]: #13347

 #13338 := (iff #12419 #13337)

 #13335 := (iff #12328 #13334)

 #13248 := (iff #12325 #13245)

 #13249 := [rewrite]: #13248

 #13242 := (iff #12322 #13243)

 #13244 := [rewrite]: #13242

 #13336 := [monotonicity #13244 #13249]: #13335

 #13339 := [monotonicity #13336]: #13338

 #13351 := [monotonicity #13339 #13348]: #13350

 #13356 := [trans #13351 #13354]: #13355

 #13359 := [monotonicity #13336 #13356]: #13358

 #13364 := [trans #13359 #13362]: #13363

 #13240 := (iff #12431 #13239)

 #13237 := (iff #3202 #13236)

 #13238 := [monotonicity #13226 #13235]: #13237

 #13241 := [monotonicity #13238]: #13240

 #13370 := [monotonicity #13241 #13364]: #13369

 #13452 := [monotonicity #13370]: #13451

 #13455 := [monotonicity #13452]: #13454

 #13458 := [monotonicity #13232 #13455]: #13457

 #13461 := [monotonicity #13232 #13458]: #13460

 #13464 := [monotonicity #13232 #13461]: #13463

 #13448 := (iff #12599 #13416)

 #13446 := (iff #3248 #13417)

 #13447 := [rewrite]: #13446

 #13449 := [monotonicity #13447]: #13448

 #13467 := [monotonicity #13449 #13464]: #13466

 #13470 := [monotonicity #13232 #13467]: #13469

 #13475 := [trans #13470 #13473]: #13474

 #13444 := (iff #12543 #13441)

 #13429 := (or #13230 #13411)

 #13432 := (or #13230 #13429)

 #13435 := (or #13417 #13432)

 #13438 := (or #13230 #13435)

 #13442 := (iff #13438 #13441)

 #13443 := [rewrite]: #13442

 #13439 := (iff #12543 #13438)

 #13436 := (iff #12535 #13435)

 #13433 := (iff #12526 #13432)

 #13430 := (iff #12518 #13429)

 #13414 := (iff #12512 #13411)

 #13408 := (and #12299 #13405)

 #13412 := (iff #13408 #13411)

 #13413 := [rewrite]: #13412

 #13409 := (iff #12512 #13408)

 #13406 := (iff #12507 #13405)

 #13403 := (iff #12500 #13400)

 #13397 := (and #12305 #13392)

 #13401 := (iff #13397 #13400)

 #13402 := [rewrite]: #13401

 #13398 := (iff #12500 #13397)

 #13395 := (iff #12495 #13392)

 #13371 := (or #12440 #13368)

 #13374 := (or #12449 #13371)

 #13377 := (or #13365 #13374)

 #13380 := (or #12467 #13377)

 #13383 := (or #12476 #13380)

 #13386 := (or #12485 #13383)

 #13389 := (or #12494 #13386)

 #13393 := (iff #13389 #13392)

 #13394 := [rewrite]: #13393

 #13390 := (iff #12495 #13389)

 #13387 := (iff #12486 #13386)

 #13384 := (iff #12477 #13383)

 #13381 := (iff #12468 #13380)

 #13378 := (iff #12459 #13377)

 #13375 := (iff #12450 #13374)

 #13372 := (iff #12441 #13371)

 #13373 := [monotonicity #13370]: #13372

 #13376 := [monotonicity #13373]: #13375

 #13366 := (iff #12458 #13365)

 #13367 := [monotonicity #13226]: #13366

 #13379 := [monotonicity #13367 #13376]: #13378

 #13382 := [monotonicity #13379]: #13381

 #13385 := [monotonicity #13382]: #13384

 #13388 := [monotonicity #13385]: #13387

 #13391 := [monotonicity #13388]: #13390

 #13396 := [trans #13391 #13394]: #13395

 #13399 := [monotonicity #13396]: #13398

 #13404 := [trans #13399 #13402]: #13403

 #13407 := [monotonicity #13404]: #13406

 #13410 := [monotonicity #13407]: #13409

 #13415 := [trans #13410 #13413]: #13414

 #13431 := [monotonicity #13232 #13415]: #13430

 #13434 := [monotonicity #13232 #13431]: #13433

 #13427 := (iff #12534 #13417)

 #13422 := (not #13416)

 #13425 := (iff #13422 #13417)

 #13426 := [rewrite]: #13425

 #13423 := (iff #12534 #13422)

 #13420 := (iff #3191 #13416)

 #13421 := [rewrite]: #13420

 #13424 := [monotonicity #13421]: #13423

 #13428 := [trans #13424 #13426]: #13427

 #13437 := [monotonicity #13428 #13434]: #13436

 #13440 := [monotonicity #13232 #13437]: #13439

 #13445 := [trans #13440 #13443]: #13444

 #13478 := [monotonicity #13445 #13475]: #13477

 #13481 := [monotonicity #13232 #13478]: #13480

 #13484 := [monotonicity #13481]: #13483

 #13489 := [trans #13484 #13487]: #13488

 #13492 := [monotonicity #13489]: #13491

 #13497 := [trans #13492 #13495]: #13496

 #13500 := [monotonicity #13497]: #13499

 #13503 := [monotonicity #13500]: #13502

 #13508 := [trans #13503 #13506]: #13507

 #13523 := [monotonicity #13232 #13508]: #13522

 #13526 := [monotonicity #13232 #13523]: #13525

 #13519 := (iff #12665 #13510)

 #13514 := (not #13511)

 #13517 := (iff #13514 #13510)

 #13518 := [rewrite]: #13517

 #13515 := (iff #12665 #13514)

 #13512 := (iff #3180 #13511)

 #13513 := [rewrite]: #13512

 #13516 := [monotonicity #13513]: #13515

 #13520 := [trans #13516 #13518]: #13519

 #13529 := [monotonicity #13520 #13526]: #13528

 #13532 := [monotonicity #13232 #13529]: #13531

 #13537 := [trans #13532 #13535]: #13536

 #13661 := [monotonicity #13537 #13658]: #13660

 #13791 := [monotonicity #13232 #13661]: #13790

 #13794 := [monotonicity #13791]: #13793

 #13797 := [monotonicity #13794]: #13796

 #13800 := [monotonicity #13797]: #13799

 #13803 := [monotonicity #13800]: #13802

 #13806 := [monotonicity #13803]: #13805

 #13809 := [monotonicity #13806]: #13808

 #13684 := (iff #12786 #13683)

 #13681 := (iff #12260 #12254)

 #13673 := (and true #12254)

 #13676 := (and true #13673)

 #13679 := (iff #13676 #12254)

 #13680 := [rewrite]: #13679

 #13677 := (iff #12260 #13676)

 #13674 := (iff #12257 #13673)

 #13669 := (iff #3161 true)

 #13664 := (forall (vars (?x783 T5)) (:pat #3159) true)

 #13667 := (iff #13664 true)

 #13668 := [elim-unused]: #13667

 #13665 := (iff #3161 #13664)

 #13662 := (iff #3160 true)

 #13663 := [rewrite]: #13662

 #13666 := [quant-intro #13663]: #13665

 #13670 := [trans #13666 #13668]: #13669

 #13675 := [monotonicity #13670]: #13674

 #13671 := (iff #3157 true)

 #13672 := [rewrite]: #13671

 #13678 := [monotonicity #13672 #13675]: #13677

 #13682 := [trans #13678 #13680]: #13681

 #13685 := [monotonicity #13682]: #13684

 #13812 := [monotonicity #13685 #13809]: #13811

 #13815 := [monotonicity #13685 #13812]: #13814

 #13818 := [monotonicity #13232 #13815]: #13817

 #13821 := [monotonicity #13232 #13818]: #13820

 #13824 := [monotonicity #13232 #13821]: #13823

 #13827 := [monotonicity #13232 #13824]: #13826

 #13701 := (iff #12842 #13700)

 #13698 := (iff #11992 #13695)

 #13692 := (and #13689 #11989)

 #13696 := (iff #13692 #13695)

 #13697 := [rewrite]: #13696

 #13693 := (iff #11992 #13692)

 #13690 := (iff #3081 #13689)

 #13691 := [rewrite]: #13690

 #13694 := [monotonicity #13691]: #13693

 #13699 := [trans #13694 #13697]: #13698

 #13702 := [monotonicity #13699]: #13701

 #13830 := [monotonicity #13702 #13827]: #13829

 #13735 := (iff #12851 #13734)

 #13732 := (iff #11986 #13731)

 #13729 := (iff #11981 #13726)

 #13720 := (or #13703 #13717)

 #13723 := (or #5579 #13720)

 #13727 := (iff #13723 #13726)

 #13728 := [rewrite]: #13727

 #13724 := (iff #11981 #13723)

 #13721 := (iff #11975 #13720)

 #13718 := (iff #3077 #13717)

 #13719 := [rewrite]: #13718

 #13713 := (iff #11974 #13703)

 #13705 := (not #13703)

 #13708 := (not #13705)

 #13711 := (iff #13708 #13703)

 #13712 := [rewrite]: #13711

 #13709 := (iff #11974 #13708)

 #13706 := (iff #3076 #13705)

 #13707 := [rewrite]: #13706

 #13710 := [monotonicity #13707]: #13709

 #13714 := [trans #13710 #13712]: #13713

 #13722 := [monotonicity #13714 #13719]: #13721

 #13725 := [monotonicity #5581 #13722]: #13724

 #13730 := [trans #13725 #13728]: #13729

 #13733 := [quant-intro #13730]: #13732

 #13736 := [monotonicity #13733]: #13735

 #13833 := [monotonicity #13736 #13830]: #13832

 #13741 := (iff #12860 #13740)

 #13738 := (iff #3075 #13737)

 #13739 := [rewrite]: #13738

 #13742 := [monotonicity #13739]: #13741

 #13836 := [monotonicity #13742 #13833]: #13835

 #13839 := [monotonicity #13232 #13836]: #13838

 #13753 := (iff #12877 #13752)

 #13750 := (iff #3072 #13749)

 #13747 := (iff #3071 #13746)

 #13748 := [rewrite]: #13747

 #13744 := (iff #3070 #13743)

 #13745 := [rewrite]: #13744

 #13751 := [monotonicity #13745 #13748]: #13750

 #13754 := [monotonicity #13751]: #13753

 #13842 := [monotonicity #13754 #13839]: #13841

 #13763 := (iff #12886 #13762)

 #13760 := (iff #3068 #13759)

 #13757 := (iff #3067 #13755)

 #13758 := [rewrite]: #13757

 #13761 := [monotonicity #13223 #13758]: #13760

 #13764 := [monotonicity #13761]: #13763

 #13845 := [monotonicity #13764 #13842]: #13844

 #13776 := (iff #12895 #13775)

 #13773 := (iff #3064 #13772)

 #13770 := (iff #3063 #13768)

 #13771 := [rewrite]: #13770

 #13766 := (iff #3062 #13765)

 #13767 := [rewrite]: #13766

 #13774 := [monotonicity #13767 #13771]: #13773

 #13777 := [monotonicity #13774]: #13776

 #13848 := [monotonicity #13777 #13845]: #13847

 #13787 := (iff #12904 #13786)

 #13784 := (iff #11968 #13781)

 #13782 := (iff #13778 #13781)

 #13783 := [rewrite]: #13782

 #13779 := (iff #11968 #13778)

 #13219 := (iff #2975 #13218)

 #13220 := [rewrite]: #13219

 #13780 := [monotonicity #13220]: #13779

 #13785 := [trans #13780 #13783]: #13784

 #13788 := [monotonicity #13785]: #13787

 #13851 := [monotonicity #13788 #13848]: #13850

 #13856 := [trans #13851 #13854]: #13855

 #13859 := [monotonicity #13780 #13856]: #13858

 #13864 := [trans #13859 #13862]: #13863

 #13215 := (iff #12916 #13214)

 #13212 := (iff #11963 #13211)

 #13209 := (iff #11958 #13206)

 #13200 := (or #13184 #13196)

 #13203 := (or #5579 #13200)

 #13207 := (iff #13203 #13206)

 #13208 := [rewrite]: #13207

 #13204 := (iff #11958 #13203)

 #13201 := (iff #11952 #13200)

 #13195 := (iff #3055 #13196)

 #13199 := [rewrite]: #13195

 #13193 := (iff #11951 #13184)

 #13185 := (not #13184)

 #13188 := (not #13185)

 #13191 := (iff #13188 #13184)

 #13192 := [rewrite]: #13191

 #13189 := (iff #11951 #13188)

 #13186 := (iff #3052 #13185)

 #13187 := [rewrite]: #13186

 #13190 := [monotonicity #13187]: #13189

 #13194 := [trans #13190 #13192]: #13193

 #13202 := [monotonicity #13194 #13199]: #13201

 #13205 := [monotonicity #5581 #13202]: #13204

 #13210 := [trans #13205 #13208]: #13209

 #13213 := [quant-intro #13210]: #13212

 #13216 := [monotonicity #13213]: #13215

 #13867 := [monotonicity #13216 #13864]: #13866

 #13870 := [monotonicity #13213 #13867]: #13869

 #13182 := (iff #12928 #13181)

 #13179 := (iff #3051 #13178)

 #13180 := [rewrite]: #13179

 #13183 := [monotonicity #13180]: #13182

 #13873 := [monotonicity #13183 #13870]: #13872

 #13876 := [monotonicity #13180 #13873]: #13875

 #13176 := (iff #12940 false)

 #11995 := (iff #3086 false)

 #11996 := [rewrite]: #11995

 #13174 := (iff #12940 #3086)

 #13172 := (iff #11948 true)

 #12286 := (and true true)

 #13167 := (and true #12286)

 #13170 := (iff #13167 true)

 #13171 := [rewrite]: #13170

 #13168 := (iff #11948 #13167)

 #13165 := (iff #11945 #12286)

 #13163 := (iff #3047 true)

 #13164 := [rewrite]: #13163

 #13161 := (iff #3046 true)

 #13162 := [rewrite]: #13161

 #13166 := [monotonicity #13162 #13164]: #13165

 #13169 := [monotonicity #13162 #13166]: #13168

 #13173 := [trans #13169 #13171]: #13172

 #13175 := [monotonicity #13173]: #13174

 #13177 := [trans #13175 #11996]: #13176

 #13879 := [monotonicity #13177 #13876]: #13878

 #13882 := [monotonicity #13879]: #13881

 #13885 := [monotonicity #13882]: #13884

 #13888 := [monotonicity #13885]: #13887

 #13891 := [monotonicity #13888]: #13890

 #13894 := [monotonicity #13891]: #13893

 #13899 := [trans #13894 #13897]: #13898

 #13902 := [monotonicity #13899]: #13901

 #13907 := [trans #13902 #13905]: #13906

 #13910 := [monotonicity #13907]: #13909

 #13913 := [monotonicity #13910]: #13912

 #13918 := [trans #13913 #13916]: #13917

 #13921 := [monotonicity #13918]: #13920

 #13924 := [monotonicity #13921]: #13923

 #13159 := (iff #13021 #13158)

 #13156 := (iff #3028 #13155)

 #13153 := (iff #3027 #13150)

 #13154 := [rewrite]: #13153

 #13147 := (iff #3026 #13148)

 #13149 := [rewrite]: #13147

 #13157 := [monotonicity #13149 #13154]: #13156

 #13160 := [monotonicity #13157]: #13159

 #14005 := [monotonicity #13160 #13924]: #14004

 #14008 := [monotonicity #14005]: #14007

 #14011 := [monotonicity #14008]: #14010

 #14014 := [monotonicity #14011]: #14013

 #14017 := [monotonicity #14014]: #14016

 #13935 := (iff #13066 #13934)

 #13932 := (iff #3012 #13931)

 #13929 := (iff #3011 #13925)

 #13930 := [rewrite]: #13929

 #13933 := [quant-intro #13930]: #13932

 #13936 := [monotonicity #13933]: #13935

 #14020 := [monotonicity #13936 #14017]: #14019

 #14023 := [monotonicity #14020]: #14022

 #14026 := [monotonicity #14023]: #14025

 #13941 := (iff #13093 #13940)

 #13938 := (iff #11896 #13937)

 #13939 := [rewrite]: #13938

 #13942 := [monotonicity #13939]: #13941

 #14029 := [monotonicity #13942 #14026]: #14028

 #13948 := (iff #13102 #13217)

 #13943 := (not #13218)

 #13946 := (iff #13943 #13217)

 #13947 := [rewrite]: #13946

 #13944 := (iff #13102 #13943)

 #13945 := [monotonicity #13220]: #13944

 #13949 := [trans #13945 #13947]: #13948

 #14032 := [monotonicity #13949 #14029]: #14031

 #13959 := (iff #13111 #13950)

 #13951 := (not #13950)

 #13954 := (not #13951)

 #13957 := (iff #13954 #13950)

 #13958 := [rewrite]: #13957

 #13955 := (iff #13111 #13954)

 #13952 := (iff #2974 #13951)

 #13953 := [rewrite]: #13952

 #13956 := [monotonicity #13953]: #13955

 #13960 := [trans #13956 #13958]: #13959

 #14035 := [monotonicity #13960 #14032]: #14034

 #13973 := (iff #13120 #13972)

 #13970 := (iff #2972 #13969)

 #13967 := (iff #2971 #13964)

 #13968 := [rewrite]: #13967

 #13961 := (iff #2970 #13962)

 #13963 := [rewrite]: #13961

 #13971 := [monotonicity #13963 #13968]: #13970

 #13974 := [monotonicity #13971]: #13973

 #14038 := [monotonicity #13974 #14035]: #14037

 #13987 := (iff #13129 #13986)

 #13984 := (iff #2968 #13983)

 #13981 := (iff #2967 #13978)

 #13982 := [rewrite]: #13981

 #13975 := (iff #2966 #13976)

 #13977 := [rewrite]: #13975

 #13985 := [monotonicity #13977 #13982]: #13984

 #13988 := [monotonicity #13985]: #13987

 #14041 := [monotonicity #13988 #14038]: #14040

 #14001 := (iff #13138 #14000)

 #13998 := (iff #2964 #13997)

 #13995 := (iff #2963 #13992)

 #13996 := [rewrite]: #13995

 #13989 := (iff #2962 #13990)

 #13991 := [rewrite]: #13989

 #13999 := [monotonicity #13991 #13996]: #13998

 #14002 := [monotonicity #13999]: #14001

 #14044 := [monotonicity #14002 #14041]: #14043

 #14049 := [trans #14044 #14047]: #14048

 #14052 := [monotonicity #14049]: #14051

 #13145 := (iff #3327 #13144)

 #13142 := (iff #3326 #13139)

 #13135 := (implies #2964 #13130)

 #13140 := (iff #13135 #13139)

 #13141 := [rewrite]: #13140

 #13136 := (iff #3326 #13135)

 #13133 := (iff #3325 #13130)

 #13126 := (implies #2968 #13121)

 #13131 := (iff #13126 #13130)

 #13132 := [rewrite]: #13131

 #13127 := (iff #3325 #13126)

 #13124 := (iff #3324 #13121)

 #13117 := (implies #2972 #13112)

 #13122 := (iff #13117 #13121)

 #13123 := [rewrite]: #13122

 #13118 := (iff #3324 #13117)

 #13115 := (iff #3323 #13112)

 #13108 := (implies #2974 #13103)

 #13113 := (iff #13108 #13112)

 #13114 := [rewrite]: #13113

 #13109 := (iff #3323 #13108)

 #13106 := (iff #3322 #13103)

 #13099 := (implies #2975 #13094)

 #13104 := (iff #13099 #13103)

 #13105 := [rewrite]: #13104

 #13100 := (iff #3322 #13099)

 #13097 := (iff #3321 #13094)

 #13090 := (implies #11896 #13085)

 #13095 := (iff #13090 #13094)

 #13096 := [rewrite]: #13095

 #13091 := (iff #3321 #13090)

 #13088 := (iff #3320 #13085)

 #13081 := (implies #11899 #13076)

 #13086 := (iff #13081 #13085)

 #13087 := [rewrite]: #13086

 #13082 := (iff #3320 #13081)

 #13079 := (iff #3319 #13076)

 #13072 := (implies #11908 #13067)

 #13077 := (iff #13072 #13076)

 #13078 := [rewrite]: #13077

 #13073 := (iff #3319 #13072)

 #13070 := (iff #3318 #13067)

 #13063 := (implies #3012 #13058)

 #13068 := (iff #13063 #13067)

 #13069 := [rewrite]: #13068

 #13064 := (iff #3318 #13063)

 #13061 := (iff #3317 #13058)

 #13054 := (implies #3016 #13049)

 #13059 := (iff #13054 #13058)

 #13060 := [rewrite]: #13059

 #13055 := (iff #3317 #13054)

 #13052 := (iff #3316 #13049)

 #13045 := (implies #3017 #13040)

 #13050 := (iff #13045 #13049)

 #13051 := [rewrite]: #13050

 #13046 := (iff #3316 #13045)

 #13043 := (iff #3315 #13040)

 #13036 := (implies #3020 #13031)

 #13041 := (iff #13036 #13040)

 #13042 := [rewrite]: #13041

 #13037 := (iff #3315 #13036)

 #13034 := (iff #3314 #13031)

 #13027 := (implies #11922 #13022)

 #13032 := (iff #13027 #13031)

 #13033 := [rewrite]: #13032

 #13028 := (iff #3314 #13027)

 #13025 := (iff #3313 #13022)

 #13018 := (implies #3028 #13015)

 #13023 := (iff #13018 #13022)

 #13024 := [rewrite]: #13023

 #13019 := (iff #3313 #13018)

 #13016 := (iff #3312 #13015)

 #13013 := (iff #3311 #13010)

 #13006 := (implies #11925 #13003)

 #13011 := (iff #13006 #13010)

 #13012 := [rewrite]: #13011

 #13007 := (iff #3311 #13006)

 #13004 := (iff #3310 #13003)

 #13001 := (iff #3309 #12998)

 #12994 := (implies #11934 #12991)

 #12999 := (iff #12994 #12998)

 #13000 := [rewrite]: #12999

 #12995 := (iff #3309 #12994)

 #12992 := (iff #3308 #12991)

 #12989 := (iff #3307 #12986)

 #12982 := (implies #11940 #12977)

 #12987 := (iff #12982 #12986)

 #12988 := [rewrite]: #12987

 #12983 := (iff #3307 #12982)

 #12980 := (iff #3306 #12977)

 #12973 := (implies #3042 #12968)

 #12978 := (iff #12973 #12977)

 #12979 := [rewrite]: #12978

 #12974 := (iff #3306 #12973)

 #12971 := (iff #3305 #12968)

 #12964 := (implies #3043 #12959)

 #12969 := (iff #12964 #12968)

 #12970 := [rewrite]: #12969

 #12965 := (iff #3305 #12964)

 #12962 := (iff #3304 #12959)

 #12955 := (implies #3044 #12950)

 #12960 := (iff #12955 #12959)

 #12961 := [rewrite]: #12960

 #12956 := (iff #3304 #12955)

 #12953 := (iff #3303 #12950)

 #12946 := (implies #3045 #12941)

 #12951 := (iff #12946 #12950)

 #12952 := [rewrite]: #12951

 #12947 := (iff #3303 #12946)

 #12944 := (iff #3302 #12941)

 #12937 := (implies #11948 #12934)

 #12942 := (iff #12937 #12941)

 #12943 := [rewrite]: #12942

 #12938 := (iff #3302 #12937)

 #12935 := (iff #3301 #12934)

 #12932 := (iff #3300 #12929)

 #12925 := (implies #3051 #12922)

 #12930 := (iff #12925 #12929)

 #12931 := [rewrite]: #12930

 #12926 := (iff #3300 #12925)

 #12923 := (iff #3299 #12922)

 #12920 := (iff #3298 #12917)

 #12913 := (implies #11963 #12910)

 #12918 := (iff #12913 #12917)

 #12919 := [rewrite]: #12918

 #12914 := (iff #3298 #12913)

 #12911 := (iff #3297 #12910)

 #12908 := (iff #3296 #12905)

 #12901 := (implies #11968 #12896)

 #12906 := (iff #12901 #12905)

 #12907 := [rewrite]: #12906

 #12902 := (iff #3296 #12901)

 #12899 := (iff #3295 #12896)

 #12892 := (implies #3064 #12887)

 #12897 := (iff #12892 #12896)

 #12898 := [rewrite]: #12897

 #12893 := (iff #3295 #12892)

 #12890 := (iff #3294 #12887)

 #12883 := (implies #3068 #12878)

 #12888 := (iff #12883 #12887)

 #12889 := [rewrite]: #12888

 #12884 := (iff #3294 #12883)

 #12881 := (iff #3293 #12878)

 #12874 := (implies #3072 #12869)

 #12879 := (iff #12874 #12878)

 #12880 := [rewrite]: #12879

 #12875 := (iff #3293 #12874)

 #12872 := (iff #3292 #12869)

 #12866 := (implies #11971 #12861)

 #12870 := (iff #12866 #12869)

 #12871 := [rewrite]: #12870

 #12867 := (iff #3292 #12866)

 #12864 := (iff #3291 #12861)

 #12857 := (implies #3075 #12852)

 #12862 := (iff #12857 #12861)

 #12863 := [rewrite]: #12862

 #12858 := (iff #3291 #12857)

 #12855 := (iff #3290 #12852)

 #12848 := (implies #11986 #12843)

 #12853 := (iff #12848 #12852)

 #12854 := [rewrite]: #12853

 #12849 := (iff #3290 #12848)

 #12846 := (iff #3289 #12843)

 #12839 := (implies #11992 #12834)

 #12844 := (iff #12839 #12843)

 #12845 := [rewrite]: #12844

 #12840 := (iff #3289 #12839)

 #12837 := (iff #3288 #12834)

 #12831 := (implies #11971 #12819)

 #12835 := (iff #12831 #12834)

 #12836 := [rewrite]: #12835

 #12832 := (iff #3288 #12831)

 #12829 := (iff #3287 #12819)

 #12824 := (and true #12819)

 #12827 := (iff #12824 #12819)

 #12828 := [rewrite]: #12827

 #12825 := (iff #3287 #12824)

 #12822 := (iff #3286 #12819)

 #12816 := (implies #11971 #12811)

 #12820 := (iff #12816 #12819)

 #12821 := [rewrite]: #12820

 #12817 := (iff #3286 #12816)

 #12814 := (iff #3285 #12811)

 #12808 := (implies #11971 #12803)

 #12812 := (iff #12808 #12811)

 #12813 := [rewrite]: #12812

 #12809 := (iff #3285 #12808)

 #12806 := (iff #3284 #12803)

 #12800 := (implies #11971 #12795)

 #12804 := (iff #12800 #12803)

 #12805 := [rewrite]: #12804

 #12801 := (iff #3284 #12800)

 #12798 := (iff #3283 #12795)

 #12792 := (implies #12260 #12787)

 #12796 := (iff #12792 #12795)

 #12797 := [rewrite]: #12796

 #12793 := (iff #3283 #12792)

 #12790 := (iff #3282 #12787)

 #12783 := (implies #12260 #12778)

 #12788 := (iff #12783 #12787)

 #12789 := [rewrite]: #12788

 #12784 := (iff #3282 #12783)

 #12781 := (iff #3281 #12778)

 #12775 := (implies #12003 #12770)

 #12779 := (iff #12775 #12778)

 #12780 := [rewrite]: #12779

 #12776 := (iff #3281 #12775)

 #12773 := (iff #3280 #12770)

 #12766 := (implies #3170 #12761)

 #12771 := (iff #12766 #12770)

 #12772 := [rewrite]: #12771

 #12767 := (iff #3280 #12766)

 #12764 := (iff #3279 #12761)

 #12757 := (implies #3171 #12752)

 #12762 := (iff #12757 #12761)

 #12763 := [rewrite]: #12762

 #12758 := (iff #3279 #12757)

 #12755 := (iff #3278 #12752)

 #12748 := (implies #3172 #12743)

 #12753 := (iff #12748 #12752)

 #12754 := [rewrite]: #12753

 #12749 := (iff #3278 #12748)

 #12746 := (iff #3277 #12743)

 #12739 := (implies #3173 #12734)

 #12744 := (iff #12739 #12743)

 #12745 := [rewrite]: #12744

 #12740 := (iff #3277 #12739)

 #12737 := (iff #3276 #12734)

 #12730 := (implies #3176 #12718)

 #12735 := (iff #12730 #12734)

 #12736 := [rewrite]: #12735

 #12731 := (iff #3276 #12730)

 #12728 := (iff #3275 #12718)

 #12723 := (implies true #12718)

 #12726 := (iff #12723 #12718)

 #12727 := [rewrite]: #12726

 #12724 := (iff #3275 #12723)

 #12721 := (iff #3274 #12718)

 #12715 := (implies #11971 #12712)

 #12719 := (iff #12715 #12718)

 #12720 := [rewrite]: #12719

 #12716 := (iff #3274 #12715)

 #12713 := (iff #3273 #12712)

 #12710 := (iff #3272 #12707)

 #12704 := (implies #11971 #12699)

 #12708 := (iff #12704 #12707)

 #12709 := [rewrite]: #12708

 #12705 := (iff #3272 #12704)

 #12702 := (iff #3271 #12699)

 #12695 := (implies #3268 #12690)

 #12700 := (iff #12695 #12699)

 #12701 := [rewrite]: #12700

 #12696 := (iff #3271 #12695)

 #12693 := (iff #3270 #12690)

 #12687 := (implies #11971 #12682)

 #12691 := (iff #12687 #12690)

 #12692 := [rewrite]: #12691

 #12688 := (iff #3270 #12687)

 #12685 := (iff #3269 #12682)

 #12679 := (implies #11971 #12133)

 #12683 := (iff #12679 #12682)

 #12684 := [rewrite]: #12683

 #12680 := (iff #3269 #12679)

 #12136 := (iff #3121 #12133)

 #12130 := (implies #11971 #12125)

 #12134 := (iff #12130 #12133)

 #12135 := [rewrite]: #12134

 #12131 := (iff #3121 #12130)

 #12128 := (iff #3120 #12125)

 #12122 := (implies #11971 #12119)

 #12126 := (iff #12122 #12125)

 #12127 := [rewrite]: #12126

 #12123 := (iff #3120 #12122)

 #12120 := (iff #3119 #12119)

 #12117 := (iff #3118 #12114)

 #12110 := (implies up_216 #12105)

 #12115 := (iff #12110 #12114)

 #12116 := [rewrite]: #12115

 #12111 := (iff #3118 #12110)

 #12108 := (iff #3117 #12105)

 #12102 := (implies #11971 #12097)

 #12106 := (iff #12102 #12105)

 #12107 := [rewrite]: #12106

 #12103 := (iff #3117 #12102)

 #12100 := (iff #3116 #12097)

 #12094 := (implies #11971 #12089)

 #12098 := (iff #12094 #12097)

 #12099 := [rewrite]: #12098

 #12095 := (iff #3116 #12094)

 #12092 := (iff #3115 #12089)

 #12085 := (implies #11971 #12080)

 #12090 := (iff #12085 #12089)

 #12091 := [rewrite]: #12090

 #12086 := (iff #3115 #12085)

 #12083 := (iff #3114 #12080)

 #12076 := (implies #12008 #12071)

 #12081 := (iff #12076 #12080)

 #12082 := [rewrite]: #12081

 #12077 := (iff #3114 #12076)

 #12074 := (iff #3113 #12071)

 #12067 := (implies #12011 #12062)

 #12072 := (iff #12067 #12071)

 #12073 := [rewrite]: #12072

 #12068 := (iff #3113 #12067)

 #12065 := (iff #3112 #12062)

 #12058 := (implies #12014 #12053)

 #12063 := (iff #12058 #12062)

 #12064 := [rewrite]: #12063

 #12059 := (iff #3112 #12058)

 #12056 := (iff #3111 #12053)

 #12049 := (implies #12017 #12046)

 #12054 := (iff #12049 #12053)

 #12055 := [rewrite]: #12054

 #12050 := (iff #3111 #12049)

 #12047 := (iff #3110 #12046)

 #12044 := (iff #3109 #12041)

 #12037 := (implies #12032 #3107)

 #12042 := (iff #12037 #12041)

 #12043 := [rewrite]: #12042

 #12038 := (iff #3109 #12037)

 #12035 := (iff #3108 #3107)

 #12036 := [rewrite]: #12035

 #12033 := (iff #3102 #12032)

 #12030 := (iff #3101 #12027)

 #12024 := (implies #412 #12021)

 #12028 := (iff #12024 #12027)

 #12029 := [rewrite]: #12028

 #12025 := (iff #3101 #12024)

 #12022 := (iff #3100 #12021)

 #12023 := [rewrite]: #12022

 #12026 := [monotonicity #12023]: #12025

 #12031 := [trans #12026 #12029]: #12030

 #12034 := [quant-intro #12031]: #12033

 #12039 := [monotonicity #12034 #12036]: #12038

 #12045 := [trans #12039 #12043]: #12044

 #12048 := [monotonicity #12034 #12045]: #12047

 #12018 := (iff #3097 #12017)

 #12019 := [rewrite]: #12018

 #12051 := [monotonicity #12019 #12048]: #12050

 #12057 := [trans #12051 #12055]: #12056

 #12015 := (iff #3095 #12014)

 #12016 := [rewrite]: #12015

 #12060 := [monotonicity #12016 #12057]: #12059

 #12066 := [trans #12060 #12064]: #12065

 #12012 := (iff #3093 #12011)

 #12013 := [rewrite]: #12012

 #12069 := [monotonicity #12013 #12066]: #12068

 #12075 := [trans #12069 #12073]: #12074

 #12009 := (iff #3091 #12008)

 #12010 := [rewrite]: #12009

 #12078 := [monotonicity #12010 #12075]: #12077

 #12084 := [trans #12078 #12082]: #12083

 #11972 := (iff #3074 #11971)

 #11973 := [rewrite]: #11972

 #12087 := [monotonicity #11973 #12084]: #12086

 #12093 := [trans #12087 #12091]: #12092

 #12096 := [monotonicity #11973 #12093]: #12095

 #12101 := [trans #12096 #12099]: #12100

 #12104 := [monotonicity #11973 #12101]: #12103

 #12109 := [trans #12104 #12107]: #12108

 #12112 := [monotonicity #12109]: #12111

 #12118 := [trans #12112 #12116]: #12117

 #12121 := [monotonicity #12118]: #12120

 #12124 := [monotonicity #11973 #12121]: #12123

 #12129 := [trans #12124 #12127]: #12128

 #12132 := [monotonicity #11973 #12129]: #12131

 #12137 := [trans #12132 #12135]: #12136

 #12681 := [monotonicity #11973 #12137]: #12680

 #12686 := [trans #12681 #12684]: #12685

 #12689 := [monotonicity #11973 #12686]: #12688

 #12694 := [trans #12689 #12692]: #12693

 #12697 := [monotonicity #12694]: #12696

 #12703 := [trans #12697 #12701]: #12702

 #12706 := [monotonicity #11973 #12703]: #12705

 #12711 := [trans #12706 #12709]: #12710

 #12677 := (iff #3267 #12674)

 #12671 := (implies #11971 #12666)

 #12675 := (iff #12671 #12674)

 #12676 := [rewrite]: #12675

 #12672 := (iff #3267 #12671)

 #12669 := (iff #3266 #12666)

 #12662 := (implies #3180 #12657)

 #12667 := (iff #12662 #12666)

 #12668 := [rewrite]: #12667

 #12663 := (iff #3266 #12662)

 #12660 := (iff #3265 #12657)

 #12654 := (implies #11971 #12649)

 #12658 := (iff #12654 #12657)

 #12659 := [rewrite]: #12658

 #12655 := (iff #3265 #12654)

 #12652 := (iff #3264 #12649)

 #12646 := (implies #11971 #12643)

 #12650 := (iff #12646 #12649)

 #12651 := [rewrite]: #12650

 #12647 := (iff #3264 #12646)

 #12644 := (iff #3263 #12643)

 #12641 := (iff #3262 #12638)

 #12635 := (implies #12299 #12632)

 #12639 := (iff #12635 #12638)

 #12640 := [rewrite]: #12639

 #12636 := (iff #3262 #12635)

 #12633 := (iff #3261 #12632)

 #12630 := (iff #3260 #12627)

 #12624 := (implies #12305 #12619)

 #12628 := (iff #12624 #12627)

 #12629 := [rewrite]: #12628

 #12625 := (iff #3260 #12624)

 #12622 := (iff #3259 #12619)

 #12616 := (implies #11971 #12613)

 #12620 := (iff #12616 #12619)

 #12621 := [rewrite]: #12620

 #12617 := (iff #3259 #12616)

 #12614 := (iff #3258 #12613)

 #12611 := (iff #3257 #12608)