6164a2366a9e57e212b8ac4aa01e3c8bcc1ea8e0 6542 0

#2 := false

decl up_6 :: (-> T4 T2 bool)

decl ?x47!7 :: (-> T2 T2)

decl ?x75!20 :: T2

#2146 := ?x75!20

#5823 := (?x47!7 ?x75!20)

decl uf_23 :: T4

#182 := uf_23

#16800 := (up_6 uf_23 #5823)

decl uf_2 :: (-> T1 T2)

decl uf_1 :: (-> T2 T2 T1)

decl uf_3 :: (-> T1 T2)

decl uf_22 :: T2

#174 := uf_22

#4514 := (uf_1 uf_22 uf_22)

#10482 := (uf_3 #4514)

#15059 := (uf_1 #10482 ?x75!20)

#15842 := (uf_3 #15059)

#16792 := (uf_1 #5823 #15842)

#19843 := (uf_2 #16792)

decl uf_7 :: (-> T4 T2 T5 T4)

decl uf_8 :: T5

#33 := uf_8

decl uf_15 :: T4

#110 := uf_15

#11444 := (uf_7 uf_15 #10482 uf_8)

#27073 := (up_6 #11444 #19843)

#27109 := (not #27073)

#16801 := (not #16800)

#27231 := (iff #16801 #27109)

#27229 := (iff #16800 #27073)

#27227 := (iff #27073 #16800)

#27215 := (= #19843 #5823)

#20888 := (= #5823 #19843)

#11 := (:var 0 T2)

#10 := (:var 1 T2)

#12 := (uf_1 #10 #11)

#3981 := (pattern #12)

#16 := (uf_2 #12)

#303 := (= #10 #16)

#3988 := (forall (vars (?x4 T2) (?x5 T2)) (:pat #3981) #303)

#307 := (forall (vars (?x4 T2) (?x5 T2)) #303)

#3991 := (iff #307 #3988)

#3989 := (iff #303 #303)

#3990 := [refl]: #3989

#3992 := [quant-intro #3990]: #3991

#1642 := (~ #307 #307)

#1676 := (~ #303 #303)

#1677 := [refl]: #1676

#1643 := [nnf-pos #1677]: #1642

#17 := (= #16 #10)

#18 := (forall (vars (?x4 T2) (?x5 T2)) #17)

#308 := (iff #18 #307)

#305 := (iff #17 #303)

#306 := [rewrite]: #305

#309 := [quant-intro #306]: #308

#302 := [asserted]: #18

#312 := [mp #302 #309]: #307

#1678 := [mp~ #312 #1643]: #307

#3993 := [mp #1678 #3992]: #3988

#8415 := (not #3988)

#20865 := (or #8415 #20888)

#20879 := [quant-inst]: #20865

#27214 := [unit-resolution #20879 #3993]: #20888

#27216 := [symm #27214]: #27215

#13523 := (= #11444 uf_23)

#183 := (uf_7 uf_15 uf_22 uf_8)

#7113 := (= #183 uf_23)

#184 := (= uf_23 #183)

#2150 := (uf_1 #11 ?x75!20)

#4271 := (pattern #2150)

decl uf_24 :: (-> T2 int)

#191 := (uf_24 #11)

#4211 := (pattern #191)

#201 := (up_6 uf_23 #11)

#4237 := (pattern #201)

#52 := 0::int

decl uf_10 :: (-> T1 int)

#2151 := (uf_10 #2150)

#2147 := (uf_24 ?x75!20)

#1038 := -1::int

#2148 := (* -1::int #2147)

#2745 := (+ #2148 #2151)

#2746 := (+ #191 #2745)

#2749 := (= #2746 0::int)

#3311 := (not #2749)

#2149 := (+ #191 #2148)

#2154 := (>= #2149 0::int)

#208 := (not #201)

#3312 := (or #208 #2154 #3311)

#4272 := (forall (vars (?x76 T2)) (:pat #4237 #4211 #4271) #3312)

#4277 := (not #4272)

#87 := (uf_1 #11 #10)

#4066 := (pattern #87)

#211 := (uf_24 #10)

#1318 := (* -1::int #211)

#1319 := (+ #191 #1318)

#88 := (uf_10 #87)

#1344 := (+ #88 #1319)

#1342 := (>= #1344 0::int)

#1053 := (* -1::int #88)

decl uf_9 :: int

#53 := uf_9

#1054 := (+ uf_9 #1053)

#1055 := (<= #1054 0::int)

#3303 := (or #208 #1055 #1342)

#4263 := (forall (vars (?x71 T2) (?x72 T2)) (:pat #4066) #3303)

#4268 := (not #4263)

decl uf_11 :: T2

#64 := uf_11

#2721 := (= uf_11 ?x75!20)

#2158 := (+ uf_9 #2148)

#2159 := (<= #2158 0::int)

#4280 := (or #2159 #2721 #4268 #4277)

#4283 := (not #4280)

decl ?x71!19 :: T2

#2117 := ?x71!19

decl ?x72!18 :: T2

#2116 := ?x72!18

#2122 := (uf_1 ?x72!18 ?x71!19)

#2123 := (uf_10 #2122)

#2126 := (* -1::int #2123)

#2120 := (uf_24 ?x72!18)

#2707 := (* -1::int #2120)

#2708 := (+ #2707 #2126)

#2118 := (uf_24 ?x71!19)

#2709 := (+ #2118 #2708)

#2710 := (<= #2709 0::int)

#2130 := (up_6 uf_23 ?x72!18)

#3266 := (not #2130)

#2127 := (+ uf_9 #2126)

#2128 := (<= #2127 0::int)

#3281 := (or #2128 #3266 #2710)

#3286 := (not #3281)

#4286 := (or #3286 #4283)

#4289 := (not #4286)

#4254 := (pattern #191 #211)

#1317 := (>= #1319 0::int)

#209 := (up_6 uf_23 #10)

#3243 := (not #209)

#3258 := (or #201 #3243 #1317)

#4255 := (forall (vars (?x67 T2) (?x68 T2)) (:pat #4254) #3258)

#4260 := (not #4255)

#4292 := (or #4260 #4289)

#4295 := (not #4292)

decl ?x68!16 :: T2

#2091 := ?x68!16

#2095 := (uf_24 ?x68!16)

#2681 := (* -1::int #2095)

decl ?x67!17 :: T2

#2092 := ?x67!17

#2093 := (uf_24 ?x67!17)

#2682 := (+ #2093 #2681)

#2683 := (<= #2682 0::int)

#2099 := (up_6 uf_23 ?x68!16)

#2098 := (up_6 uf_23 ?x67!17)

#3220 := (not #2098)

#3235 := (or #3220 #2099 #2683)

#3240 := (not #3235)

#4298 := (or #3240 #4295)

#4301 := (not #4298)

#1308 := (>= #191 0::int)

#4246 := (forall (vars (?x65 T2)) (:pat #4211) #1308)

#4251 := (not #4246)

#4304 := (or #4251 #4301)

#4307 := (not #4304)

decl ?x65!15 :: T2

#2076 := ?x65!15

#2077 := (uf_24 ?x65!15)

#2078 := (>= #2077 0::int)

#2079 := (not #2078)

#4310 := (or #2079 #4307)

#4313 := (not #4310)

#204 := (uf_24 uf_11)

#205 := (= #204 0::int)

#1305 := (not #205)

#4316 := (or #1305 #4313)

#4319 := (not #4316)

#4322 := (or #1305 #4319)

#4325 := (not #4322)

decl uf_4 :: (-> T3 T2 int)

decl uf_14 :: T3

#104 := uf_14

#107 := (uf_4 uf_14 #11)

#4090 := (pattern #107)

#645 := (= #107 #191)

#662 := (or #208 #645)

#4238 := (forall (vars (?x63 T2)) (:pat #4237 #4090 #4211) #662)

#4243 := (not #4238)

#4328 := (or #4243 #4325)

#4331 := (not #4328)

decl ?x63!14 :: T2

#2052 := ?x63!14

#2054 := (uf_4 uf_14 ?x63!14)

#2053 := (uf_24 ?x63!14)

#2658 := (= #2053 #2054)

#2056 := (up_6 uf_23 ?x63!14)

#2057 := (not #2056)

#2661 := (or #2057 #2658)

#2664 := (not #2661)

#4334 := (or #2664 #4331)

#4337 := (not #4334)

#1293 := (* -1::int #191)

#1294 := (+ #107 #1293)

#1292 := (>= #1294 0::int)

#4229 := (forall (vars (?x61 T2)) (:pat #4090 #4211) #1292)

#4234 := (not #4229)

#4340 := (or #4234 #4337)

#4343 := (not #4340)

decl ?x61!13 :: T2

#2034 := ?x61!13

#2037 := (uf_4 uf_14 ?x61!13)

#2648 := (* -1::int #2037)

#2035 := (uf_24 ?x61!13)

#2649 := (+ #2035 #2648)

#2650 := (<= #2649 0::int)

#2655 := (not #2650)

#4346 := (or #2655 #4343)

#4349 := (not #4346)

#185 := (uf_1 uf_22 #11)

#4212 := (pattern #185)

#186 := (uf_10 #185)

#1431 := (+ #186 #1293)

#177 := (uf_4 uf_14 uf_22)

#1432 := (+ #177 #1431)

#1433 := (= #1432 0::int)

#1262 := (* -1::int #186)

#1268 := (* -1::int #177)

#1269 := (+ #1268 #1262)

#1270 := (+ #107 #1269)

#1271 := (<= #1270 0::int)

#1263 := (+ uf_9 #1262)

#1264 := (<= #1263 0::int)

#3212 := (or #1264 #1271 #1433)

#4221 := (forall (vars (?x59 T2)) (:pat #4212 #4090 #4211) #3212)

#4226 := (not #4221)

#3192 := (or #1264 #1271)

#3193 := (not #3192)

#3196 := (or #645 #3193)

#4213 := (forall (vars (?x60 T2)) (:pat #4090 #4211 #4212) #3196)

#4218 := (not #4213)

decl ?x48!12 :: T2

#2011 := ?x48!12

#2017 := (up_6 uf_15 ?x48!12)

#2012 := (uf_4 uf_14 ?x48!12)

#2013 := (* -1::int #2012)

#2014 := (+ uf_9 #2013)

#2015 := (<= #2014 0::int)

#1458 := (+ uf_9 #1268)

#1459 := (<= #1458 0::int)

#111 := (up_6 uf_15 #11)

#4132 := (pattern #111)

#1446 := (+ #107 #1268)

#1445 := (>= #1446 0::int)

#1449 := (or #111 #1445)

#4203 := (forall (vars (?x58 T2)) (:pat #4132 #4090) #1449)

#4208 := (not #4203)

#825 := (not #184)

#175 := (up_6 uf_15 uf_22)

#4352 := (or #175 #825 #4208 #1459 #2015 #2017 #4218 #4226 #4349)

#4355 := (not #4352)

decl ?x53!11 :: T2

#1945 := ?x53!11

decl ?x54!10 :: T2

#1944 := ?x54!10

#1950 := (uf_1 ?x54!10 ?x53!11)

#1951 := (uf_10 #1950)

#1958 := (* -1::int #1951)

decl uf_19 :: T3

#141 := uf_19

#1948 := (uf_4 uf_19 ?x54!10)

#1954 := (* -1::int #1948)

#2605 := (+ #1954 #1958)

#1946 := (uf_4 uf_19 ?x53!11)

#2606 := (+ #1946 #2605)

#2607 := (<= #2606 0::int)

#1959 := (+ uf_9 #1958)

#1960 := (<= #1959 0::int)

#1955 := (+ uf_9 #1954)

#1956 := (<= #1955 0::int)

#3156 := (or #1956 #1960 #2607)

#3161 := (not #3156)

#149 := (uf_4 uf_19 #10)

#1175 := (* -1::int #149)

#146 := (uf_4 uf_19 #11)

#1176 := (+ #146 #1175)

#1182 := (+ #88 #1176)

#1205 := (>= #1182 0::int)

#1162 := (* -1::int #146)

#1163 := (+ uf_9 #1162)

#1164 := (<= #1163 0::int)

#3124 := (or #1055 #1164 #1205)

#4165 := (forall (vars (?x53 T2) (?x54 T2)) (:pat #4066) #3124)

#4170 := (not #4165)

#161 := (uf_4 uf_19 uf_11)

#162 := (= #161 0::int)

#4173 := (or #162 #4170)

#4176 := (not #4173)

#4179 := (or #4176 #3161)

#4182 := (not #4179)

#4141 := (pattern #146)

decl ?x50!9 :: (-> T2 T2)

#1921 := (?x50!9 #11)

#1924 := (uf_1 #1921 #11)

#1925 := (uf_10 #1924)

#2575 := (* -1::int #1925)

#1922 := (uf_4 uf_19 #1921)

#2558 := (* -1::int #1922)

#2576 := (+ #2558 #2575)

#2577 := (+ #146 #2576)

#2578 := (= #2577 0::int)

#3094 := (not #2578)

#2559 := (+ #146 #2558)

#2560 := (<= #2559 0::int)

#3095 := (or #2560 #3094)

#3096 := (not #3095)

#65 := (= #11 uf_11)

#3102 := (or #65 #1164 #3096)

#4157 := (forall (vars (?x49 T2)) (:pat #4141) #3102)

#4162 := (not #4157)

#4185 := (or #4162 #4182)

#4188 := (not #4185)

decl ?x49!8 :: T2

#1881 := ?x49!8

#1885 := (uf_1 #11 ?x49!8)

#4142 := (pattern #1885)

#1886 := (uf_10 #1885)

#1882 := (uf_4 uf_19 ?x49!8)

#1883 := (* -1::int #1882)

#2528 := (+ #1883 #1886)

#2529 := (+ #146 #2528)

#2532 := (= #2529 0::int)

#3058 := (not #2532)

#1884 := (+ #146 #1883)

#1889 := (>= #1884 0::int)

#3059 := (or #1889 #3058)

#4143 := (forall (vars (?x50 T2)) (:pat #4141 #4142) #3059)

#4148 := (not #4143)

#2504 := (= uf_11 ?x49!8)

#1893 := (+ uf_9 #1883)

#1894 := (<= #1893 0::int)

#4151 := (or #1894 #2504 #4148)

#4154 := (not #4151)

#4191 := (or #4154 #4188)

#4194 := (not #4191)

#1117 := (* -1::int #107)

#1118 := (+ uf_9 #1117)

#1119 := (<= #1118 0::int)

#3044 := (or #111 #1119)

#4133 := (forall (vars (?x48 T2)) (:pat #4132 #4090) #3044)

#4138 := (not #4133)

#495 := (= uf_14 uf_19)

#586 := (not #495)

decl uf_16 :: T4

#136 := uf_16

#492 := (= uf_15 uf_16)

#604 := (not #492)

decl uf_21 :: T3

#144 := uf_21

decl uf_20 :: T3

#143 := uf_20

#145 := (= uf_20 uf_21)

#577 := (not #145)

decl uf_18 :: T2

#139 := uf_18

decl uf_17 :: T2

#138 := uf_17

#140 := (= uf_17 uf_18)

#595 := (not #140)

#4197 := (or #595 #577 #604 #586 #4138 #4194)

#4200 := (not #4197)

#4358 := (or #4200 #4355)

#4361 := (not #4358)

#1845 := (?x47!7 #11)

#1846 := (uf_4 uf_14 #1845)

#2463 := (* -1::int #1846)

#2478 := (+ #107 #2463)

#2479 := (<= #2478 0::int)

#1850 := (uf_1 #1845 #11)

#1851 := (uf_10 #1850)

#2464 := (* -1::int #1851)

#2465 := (+ #2463 #2464)

#2466 := (+ #107 #2465)

#2467 := (= #2466 0::int)

#3028 := (not #2467)

#1854 := (up_6 uf_15 #1845)

#3027 := (not #1854)

#3029 := (or #3027 #3028 #2479)

#3030 := (not #3029)

#3036 := (or #65 #1119 #3030)

#4124 := (forall (vars (?x46 T2)) (:pat #4090) #3036)

#4129 := (not #4124)

decl uf_12 :: (-> T2 int)

#66 := (uf_12 #11)

#4042 := (pattern #66)

decl ?x38!6 :: (-> T2 T2)

#1818 := (?x38!6 #11)

#1822 := (uf_12 #1818)

#2422 := (* -1::int #1822)

#1819 := (uf_1 #1818 #11)

#1820 := (uf_10 #1819)

#2439 := (* -1::int #1820)

#2440 := (+ #2439 #2422)

#2441 := (+ #66 #2440)

#2442 := (= #2441 0::int)

#3000 := (not #2442)

#2423 := (+ #66 #2422)

#2424 := (<= #2423 0::int)

decl up_13 :: (-> T2 bool)

#1828 := (up_13 #1818)

#2999 := (not #1828)

#3001 := (or #2999 #2424 #3000)

#3002 := (not #3001)

#1079 := (* -1::int #66)

#1080 := (+ uf_9 #1079)

#1081 := (<= #1080 0::int)

#3008 := (or #65 #1081 #3002)

#4116 := (forall (vars (?x37 T2)) (:pat #4042) #3008)

#4121 := (not #4116)

#113 := (up_6 uf_15 #10)

#4107 := (pattern #111 #113)

#115 := (uf_4 uf_14 #10)

#1131 := (* -1::int #115)

#1132 := (+ #107 #1131)

#1135 := (>= #1132 0::int)

#2965 := (not #113)

#2980 := (or #111 #2965 #1135)

#4108 := (forall (vars (?x42 T2) (?x43 T2)) (:pat #4107) #2980)

#4113 := (not #4108)

#1133 := (+ #88 #1132)

#1513 := (>= #1133 0::int)

#112 := (not #111)

#2957 := (or #112 #1055 #1513)

#4099 := (forall (vars (?x44 T2) (?x45 T2)) (:pat #4066) #2957)

#4104 := (not #4099)

#1536 := (>= #107 0::int)

#4091 := (forall (vars (?x41 T2)) (:pat #4090) #1536)

#4096 := (not #4091)

#105 := (uf_4 uf_14 uf_11)

#106 := (= #105 0::int)

#1547 := (not #106)

#4364 := (or #1547 #4096 #4104 #4113 #4121 #4129 #4361)

#4367 := (not #4364)

decl ?x37!5 :: T2

#1774 := ?x37!5

#1775 := (uf_1 #11 ?x37!5)

#4075 := (pattern #1775)

#74 := (up_13 #11)

#4035 := (pattern #74)

#1777 := (uf_12 ?x37!5)

#1778 := (* -1::int #1777)

#1776 := (uf_10 #1775)

#2390 := (+ #1776 #1778)

#2391 := (+ #66 #2390)

#2394 := (= #2391 0::int)

#2918 := (not #2394)

#1782 := (+ #66 #1778)

#1783 := (>= #1782 0::int)

#75 := (not #74)

#2919 := (or #75 #1783 #2918)

#4076 := (forall (vars (?x38 T2)) (:pat #4035 #4042 #4075) #2919)

#4081 := (not #4076)

#2366 := (= uf_11 ?x37!5)

#1787 := (+ uf_9 #1778)

#1788 := (<= #1787 0::int)

#4084 := (or #1788 #2366 #4081)

#4087 := (not #4084)

#4370 := (or #4087 #4367)

#4373 := (not #4370)

#83 := (uf_12 #10)

#1041 := (* -1::int #83)

#1068 := (+ #1041 #88)

#1069 := (+ #66 #1068)

#1066 := (>= #1069 0::int)

#2910 := (or #75 #1055 #1066)

#4067 := (forall (vars (?x33 T2) (?x34 T2)) (:pat #4066) #2910)

#4072 := (not #4067)

#4376 := (or #4072 #4373)

#4379 := (not #4376)

decl ?x34!3 :: T2

#1744 := ?x34!3

#1751 := (uf_12 ?x34!3)

decl ?x33!4 :: T2

#1745 := ?x33!4

#1748 := (uf_12 ?x33!4)

#1749 := (* -1::int #1748)

#2353 := (+ #1749 #1751)

#1746 := (uf_1 ?x34!3 ?x33!4)

#1747 := (uf_10 #1746)

#2354 := (+ #1747 #2353)

#2357 := (>= #2354 0::int)

#1758 := (up_13 ?x34!3)

#2873 := (not #1758)

#1754 := (* -1::int #1747)

#1755 := (+ uf_9 #1754)

#1756 := (<= #1755 0::int)

#2888 := (or #1756 #2873 #2357)

#8152 := [hypothesis]: #1758

#4036 := (forall (vars (?x26 T2)) (:pat #4035) #75)

#76 := (forall (vars (?x26 T2)) #75)

#4039 := (iff #76 #4036)

#4037 := (iff #75 #75)

#4038 := [refl]: #4037

#4040 := [quant-intro #4038]: #4039

#1658 := (~ #76 #76)

#1695 := (~ #75 #75)

#1696 := [refl]: #1695

#1659 := [nnf-pos #1696]: #1658

#67 := (= #66 0::int)

#70 := (not #65)

#1605 := (or #70 #67)

#1608 := (forall (vars (?x24 T2)) #1605)

#1611 := (not #1608)

#1539 := (forall (vars (?x41 T2)) #1536)

#1542 := (not #1539)

#114 := (and #112 #113)

#440 := (not #114)

#1527 := (or #440 #1135)

#1530 := (forall (vars (?x42 T2) (?x43 T2)) #1527)

#1533 := (not #1530)

#1056 := (not #1055)

#1505 := (and #111 #1056)

#1510 := (not #1505)

#1516 := (or #1510 #1513)

#1519 := (forall (vars (?x44 T2) (?x45 T2)) #1516)

#1522 := (not #1519)

#1452 := (forall (vars (?x58 T2)) #1449)

#1455 := (not #1452)

#1272 := (not #1271)

#1265 := (not #1264)

#1275 := (and #1265 #1272)

#1428 := (not #1275)

#1436 := (or #1428 #1433)

#1439 := (forall (vars (?x59 T2)) #1436)

#1442 := (not #1439)

#1366 := (= #1344 0::int)

#1369 := (not #1317)

#1378 := (and #201 #1369 #1366)

#1383 := (exists (vars (?x76 T2)) #1378)

#1355 := (+ uf_9 #1293)

#1356 := (<= #1355 0::int)

#1357 := (not #1356)

#1360 := (and #70 #1357)

#1363 := (not #1360)

#1386 := (or #1363 #1383)

#1389 := (forall (vars (?x75 T2)) #1386)

#1334 := (and #201 #1056)

#1339 := (not #1334)

#1346 := (or #1339 #1342)

#1349 := (forall (vars (?x71 T2) (?x72 T2)) #1346)

#1352 := (not #1349)

#1392 := (or #1352 #1389)

#1395 := (and #1349 #1392)

#210 := (and #208 #209)

#673 := (not #210)

#1322 := (or #673 #1317)

#1325 := (forall (vars (?x67 T2) (?x68 T2)) #1322)

#1328 := (not #1325)

#1398 := (or #1328 #1395)

#1401 := (and #1325 #1398)

#1311 := (forall (vars (?x65 T2)) #1308)

#1314 := (not #1311)

#1404 := (or #1314 #1401)

#1407 := (and #1311 #1404)

#1410 := (or #1305 #1407)

#1413 := (and #205 #1410)

#667 := (forall (vars (?x63 T2)) #662)

#783 := (not #667)

#1416 := (or #783 #1413)

#1419 := (and #667 #1416)

#1297 := (forall (vars (?x61 T2)) #1292)

#1300 := (not #1297)

#1422 := (or #1300 #1419)

#1425 := (and #1297 #1422)

#1281 := (or #645 #1275)

#1286 := (forall (vars (?x60 T2)) #1281)

#1289 := (not #1286)

#1120 := (not #1119)

#1236 := (and #112 #1120)

#1239 := (exists (vars (?x48 T2)) #1236)

#1470 := (not #1239)

#1494 := (or #175 #825 #1470 #1289 #1425 #1442 #1455 #1459)

#1165 := (not #1164)

#1199 := (and #1056 #1165)

#1202 := (not #1199)

#1208 := (or #1202 #1205)

#1211 := (forall (vars (?x53 T2) (?x54 T2)) #1208)

#1214 := (not #1211)

#1222 := (or #162 #1214)

#1227 := (and #1211 #1222)

#1180 := (= #1182 0::int)

#1174 := (>= #1176 0::int)

#1177 := (not #1174)

#1184 := (and #1177 #1180)

#1187 := (exists (vars (?x50 T2)) #1184)

#1168 := (and #70 #1165)

#1171 := (not #1168)

#1190 := (or #1171 #1187)

#1193 := (forall (vars (?x49 T2)) #1190)

#1196 := (not #1193)

#1230 := (or #1196 #1227)

#1233 := (and #1193 #1230)

#1257 := (or #595 #577 #604 #586 #1233 #1239)

#1499 := (and #1257 #1494)

#1136 := (not #1135)

#1129 := (= #1133 0::int)

#1145 := (and #111 #1129 #1136)

#1150 := (exists (vars (?x47 T2)) #1145)

#1123 := (and #70 #1120)

#1126 := (not #1123)

#1153 := (or #1126 #1150)

#1156 := (forall (vars (?x46 T2)) #1153)

#1159 := (not #1156)

#1091 := (= #1069 0::int)

#1042 := (+ #66 #1041)

#1040 := (>= #1042 0::int)

#1094 := (not #1040)

#1103 := (and #74 #1094 #1091)

#1108 := (exists (vars (?x38 T2)) #1103)

#1082 := (not #1081)

#1085 := (and #70 #1082)

#1088 := (not #1085)

#1111 := (or #1088 #1108)

#1114 := (forall (vars (?x37 T2)) #1111)

#1550 := (not #1114)

#1571 := (or #1547 #1550 #1159 #1499 #1522 #1533 #1542)

#1576 := (and #1114 #1571)

#1059 := (and #74 #1056)

#1062 := (not #1059)

#1070 := (or #1062 #1066)

#1073 := (forall (vars (?x33 T2) (?x34 T2)) #1070)

#1076 := (not #1073)

#1579 := (or #1076 #1576)

#1582 := (and #1073 #1579)

#81 := (up_13 #10)

#82 := (and #75 #81)

#416 := (not #82)

#1044 := (or #416 #1040)

#1047 := (forall (vars (?x29 T2) (?x30 T2)) #1044)

#1050 := (not #1047)

#1585 := (or #1050 #1582)

#1588 := (and #1047 #1585)

#1031 := (>= #66 0::int)

#1032 := (forall (vars (?x27 T2)) #1031)

#1035 := (not #1032)

#1591 := (or #1035 #1588)

#1594 := (and #1032 #1591)

#77 := (uf_12 uf_11)

#78 := (= #77 0::int)

#1026 := (not #78)

#1597 := (or #1026 #1594)

#1600 := (and #78 #1597)

#399 := (= uf_9 #66)

#405 := (or #65 #399)

#410 := (forall (vars (?x25 T2)) #405)

#999 := (not #410)

#990 := (not #76)

#1623 := (or #990 #999 #1600 #1611)

#1628 := (not #1623)

#1 := true

#216 := (+ #191 #88)

#223 := (= #211 #216)

#224 := (and #201 #223)

#222 := (< #191 #211)

#225 := (and #222 #224)

#226 := (exists (vars (?x76 T2)) #225)

#220 := (< #191 uf_9)

#221 := (and #70 #220)

#227 := (implies #221 #226)

#228 := (forall (vars (?x75 T2)) #227)

#229 := (and #228 true)

#217 := (<= #211 #216)

#89 := (< #88 uf_9)

#215 := (and #201 #89)

#218 := (implies #215 #217)

#219 := (forall (vars (?x71 T2) (?x72 T2)) #218)

#230 := (implies #219 #229)

#231 := (and #219 #230)

#212 := (<= #211 #191)

#213 := (implies #210 #212)

#214 := (forall (vars (?x67 T2) (?x68 T2)) #213)

#232 := (implies #214 #231)

#233 := (and #214 #232)

#206 := (<= 0::int #191)

#207 := (forall (vars (?x65 T2)) #206)

#234 := (implies #207 #233)

#235 := (and #207 #234)

#236 := (implies #205 #235)

#237 := (and #205 #236)

#196 := (= #191 #107)

#202 := (implies #201 #196)

#203 := (forall (vars (?x63 T2)) #202)

#238 := (implies #203 #237)

#239 := (and #203 #238)

#199 := (<= #191 #107)

#200 := (forall (vars (?x61 T2)) #199)

#240 := (implies #200 #239)

#241 := (and #200 #240)

#188 := (+ #177 #186)

#189 := (< #188 #107)

#187 := (< #186 uf_9)

#190 := (and #187 #189)

#195 := (not #190)

#197 := (implies #195 #196)

#198 := (forall (vars (?x60 T2)) #197)

#242 := (implies #198 #241)

#192 := (= #191 #188)

#193 := (implies #190 #192)

#194 := (forall (vars (?x59 T2)) #193)

#243 := (implies #194 #242)

#244 := (implies #184 #243)

#179 := (<= #177 #107)

#180 := (implies #112 #179)

#181 := (forall (vars (?x58 T2)) #180)

#245 := (implies #181 #244)

#178 := (< #177 uf_9)

#246 := (implies #178 #245)

#176 := (not #175)

#247 := (implies #176 #246)

#124 := (< #107 uf_9)

#133 := (and #112 #124)

#134 := (exists (vars (?x48 T2)) #133)

#248 := (implies #134 #247)

#249 := (implies true #248)

#163 := (and #162 true)

#151 := (+ #146 #88)

#158 := (<= #149 #151)

#147 := (< #146 uf_9)

#157 := (and #147 #89)

#159 := (implies #157 #158)

#160 := (forall (vars (?x53 T2) (?x54 T2)) #159)

#164 := (implies #160 #163)

#165 := (and #160 #164)

#152 := (= #149 #151)

#150 := (< #146 #149)

#153 := (and #150 #152)

#154 := (exists (vars (?x50 T2)) #153)

#148 := (and #70 #147)

#155 := (implies #148 #154)

#156 := (forall (vars (?x49 T2)) #155)

#166 := (implies #156 #165)

#167 := (and #156 #166)

#168 := (implies #145 #167)

#142 := (= uf_19 uf_14)

#169 := (implies #142 #168)

#170 := (implies #140 #169)

#137 := (= uf_16 uf_15)

#171 := (implies #137 #170)

#135 := (not #134)

#172 := (implies #135 #171)

#173 := (implies true #172)

#250 := (and #173 #249)

#120 := (+ #107 #88)

#127 := (= #115 #120)

#128 := (and #111 #127)

#126 := (< #107 #115)

#129 := (and #126 #128)

#130 := (exists (vars (?x47 T2)) #129)

#125 := (and #70 #124)

#131 := (implies #125 #130)

#132 := (forall (vars (?x46 T2)) #131)

#251 := (implies #132 #250)

#121 := (<= #115 #120)

#119 := (and #111 #89)

#122 := (implies #119 #121)

#123 := (forall (vars (?x44 T2) (?x45 T2)) #122)

#252 := (implies #123 #251)

#116 := (<= #115 #107)

#117 := (implies #114 #116)

#118 := (forall (vars (?x42 T2) (?x43 T2)) #117)

#253 := (implies #118 #252)

#108 := (<= 0::int #107)

#109 := (forall (vars (?x41 T2)) #108)

#254 := (implies #109 #253)

#255 := (implies #106 #254)

#256 := (implies true #255)

#91 := (+ #66 #88)

#98 := (= #83 #91)

#99 := (and #74 #98)

#97 := (< #66 #83)

#100 := (and #97 #99)

#101 := (exists (vars (?x38 T2)) #100)

#95 := (< #66 uf_9)

#96 := (and #70 #95)

#102 := (implies #96 #101)

#103 := (forall (vars (?x37 T2)) #102)

#257 := (implies #103 #256)

#258 := (and #103 #257)

#92 := (<= #83 #91)

#90 := (and #74 #89)

#93 := (implies #90 #92)

#94 := (forall (vars (?x33 T2) (?x34 T2)) #93)

#259 := (implies #94 #258)

#260 := (and #94 #259)

#84 := (<= #83 #66)

#85 := (implies #82 #84)

#86 := (forall (vars (?x29 T2) (?x30 T2)) #85)

#261 := (implies #86 #260)

#262 := (and #86 #261)

#79 := (<= 0::int #66)

#80 := (forall (vars (?x27 T2)) #79)

#263 := (implies #80 #262)

#264 := (and #80 #263)

#265 := (implies #78 #264)

#266 := (and #78 #265)

#267 := (implies #76 #266)

#71 := (= #66 uf_9)

#72 := (implies #70 #71)

#73 := (forall (vars (?x25 T2)) #72)

#268 := (implies #73 #267)

#68 := (implies #65 #67)

#69 := (forall (vars (?x24 T2)) #68)

#269 := (implies #69 #268)

#270 := (implies true #269)

#271 := (not #270)

#1631 := (iff #271 #1628)

#683 := (+ #88 #191)

#701 := (= #211 #683)

#704 := (and #201 #701)

#707 := (and #222 #704)

#710 := (exists (vars (?x76 T2)) #707)

#716 := (not #221)

#717 := (or #716 #710)

#722 := (forall (vars (?x75 T2)) #717)

#686 := (<= #211 #683)

#680 := (and #89 #201)

#692 := (not #680)

#693 := (or #692 #686)

#698 := (forall (vars (?x71 T2) (?x72 T2)) #693)

#735 := (not #698)

#736 := (or #735 #722)

#741 := (and #698 #736)

#674 := (or #673 #212)

#677 := (forall (vars (?x67 T2) (?x68 T2)) #674)

#747 := (not #677)

#748 := (or #747 #741)

#753 := (and #677 #748)

#759 := (not #207)

#760 := (or #759 #753)

#765 := (and #207 #760)

#670 := (= 0::int #204)

#771 := (not #670)

#772 := (or #771 #765)

#777 := (and #670 #772)

#784 := (or #783 #777)

#789 := (and #667 #784)

#795 := (not #200)

#796 := (or #795 #789)

#801 := (and #200 #796)

#651 := (or #190 #645)

#656 := (forall (vars (?x60 T2)) #651)

#807 := (not #656)

#808 := (or #807 #801)

#631 := (= #188 #191)

#637 := (or #195 #631)

#642 := (forall (vars (?x59 T2)) #637)

#816 := (not #642)

#817 := (or #816 #808)

#826 := (or #825 #817)

#625 := (or #111 #179)

#628 := (forall (vars (?x58 T2)) #625)

#834 := (not #628)

#835 := (or #834 #826)

#843 := (not #178)

#844 := (or #843 #835)

#852 := (or #175 #844)

#860 := (or #135 #852)

#540 := (= 0::int #161)

#498 := (+ #88 #146)

#525 := (<= #149 #498)

#522 := (and #89 #147)

#531 := (not #522)

#532 := (or #531 #525)

#537 := (forall (vars (?x53 T2) (?x54 T2)) #532)

#553 := (not #537)

#554 := (or #553 #540)

#559 := (and #537 #554)

#501 := (= #149 #498)

#504 := (and #150 #501)

#507 := (exists (vars (?x50 T2)) #504)

#513 := (not #148)

#514 := (or #513 #507)

#519 := (forall (vars (?x49 T2)) #514)

#565 := (not #519)

#566 := (or #565 #559)

#571 := (and #519 #566)

#578 := (or #577 #571)

#587 := (or #586 #578)

#596 := (or #595 #587)

#605 := (or #604 #596)

#613 := (or #134 #605)

#872 := (and #613 #860)

#450 := (+ #88 #107)

#468 := (= #115 #450)

#471 := (and #111 #468)

#474 := (and #126 #471)

#477 := (exists (vars (?x47 T2)) #474)

#483 := (not #125)

#484 := (or #483 #477)

#489 := (forall (vars (?x46 T2)) #484)

#878 := (not #489)

#879 := (or #878 #872)

#453 := (<= #115 #450)

#447 := (and #89 #111)

#459 := (not #447)

#460 := (or #459 #453)

#465 := (forall (vars (?x44 T2) (?x45 T2)) #460)

#887 := (not #465)

#888 := (or #887 #879)

#441 := (or #440 #116)

#444 := (forall (vars (?x42 T2) (?x43 T2)) #441)

#896 := (not #444)

#897 := (or #896 #888)

#905 := (not #109)

#906 := (or #905 #897)

#437 := (= 0::int #105)

#914 := (not #437)

#915 := (or #914 #906)

#430 := (not #96)

#431 := (or #430 #101)

#434 := (forall (vars (?x37 T2)) #431)

#930 := (not #434)

#931 := (or #930 #915)

#936 := (and #434 #931)

#423 := (not #90)

#424 := (or #423 #92)

#427 := (forall (vars (?x33 T2) (?x34 T2)) #424)

#942 := (not #427)

#943 := (or #942 #936)

#948 := (and #427 #943)

#417 := (or #416 #84)

#420 := (forall (vars (?x29 T2) (?x30 T2)) #417)

#954 := (not #420)

#955 := (or #954 #948)

#960 := (and #420 #955)

#966 := (not #80)

#967 := (or #966 #960)

#972 := (and #80 #967)

#413 := (= 0::int #77)

#978 := (not #413)

#979 := (or #978 #972)

#984 := (and #413 #979)

#991 := (or #990 #984)

#1000 := (or #999 #991)

#385 := (= 0::int #66)

#391 := (or #70 #385)

#396 := (forall (vars (?x24 T2)) #391)

#1008 := (not #396)

#1009 := (or #1008 #1000)

#1021 := (not #1009)

#1629 := (iff #1021 #1628)

#1626 := (iff #1009 #1623)

#1614 := (or #990 #1600)

#1617 := (or #999 #1614)

#1620 := (or #1611 #1617)

#1624 := (iff #1620 #1623)

#1625 := [rewrite]: #1624

#1621 := (iff #1009 #1620)

#1618 := (iff #1000 #1617)

#1615 := (iff #991 #1614)

#1601 := (iff #984 #1600)

#1598 := (iff #979 #1597)

#1595 := (iff #972 #1594)

#1592 := (iff #967 #1591)

#1589 := (iff #960 #1588)

#1586 := (iff #955 #1585)

#1583 := (iff #948 #1582)

#1580 := (iff #943 #1579)

#1577 := (iff #936 #1576)

#1574 := (iff #931 #1571)

#1553 := (or #1159 #1499)

#1556 := (or #1522 #1553)

#1559 := (or #1533 #1556)

#1562 := (or #1542 #1559)

#1565 := (or #1547 #1562)

#1568 := (or #1550 #1565)

#1572 := (iff #1568 #1571)

#1573 := [rewrite]: #1572

#1569 := (iff #931 #1568)

#1566 := (iff #915 #1565)

#1563 := (iff #906 #1562)

#1560 := (iff #897 #1559)

#1557 := (iff #888 #1556)

#1554 := (iff #879 #1553)

#1500 := (iff #872 #1499)

#1497 := (iff #860 #1494)

#1473 := (or #1289 #1425)

#1476 := (or #1442 #1473)

#1479 := (or #825 #1476)

#1482 := (or #1455 #1479)

#1485 := (or #1459 #1482)

#1488 := (or #175 #1485)