src/HOL/Boogie/Examples/Boogie_Max.certs
author hoelzl
Thu Sep 02 10:14:32 2010 +0200 (2010-09-02)
changeset 39072 1030b1a166ef
parent 37156 42c53229800d
child 40163 a462d5207aa6
permissions -rw-r--r--
Add lessThan_Suc_eq_insert_0
     1 3e8da1e086888bc525192984192051f1e39c6752 2224 0
     2 #2 := false
     3 #8 := 0::int
     4 decl f5 :: (-> int int)
     5 decl ?v0!3 :: int
     6 #1153 := ?v0!3
     7 #1154 := (f5 ?v0!3)
     8 #652 := -1::int
     9 #1356 := (* -1::int #1154)
    10 decl f7 :: int
    11 #31 := f7
    12 #68 := (f5 f7)
    13 #2646 := (+ #68 #1356)
    14 #2648 := (>= #2646 0::int)
    15 #2645 := (= #68 #1154)
    16 #2494 := (= f7 ?v0!3)
    17 #1334 := (* -1::int ?v0!3)
    18 #2380 := (+ f7 #1334)
    19 #2496 := (>= #2380 0::int)
    20 decl f15 :: int
    21 #79 := f15
    22 #1335 := (+ f15 #1334)
    23 #1336 := (<= #1335 0::int)
    24 #1341 := (not #1336)
    25 decl f14 :: int
    26 #75 := f14
    27 #1357 := (+ f14 #1356)
    28 #1358 := (>= #1357 0::int)
    29 #1160 := (>= ?v0!3 0::int)
    30 #1609 := (not #1160)
    31 #1624 := (or #1609 #1336 #1358)
    32 #1629 := (not #1624)
    33 #20 := (:var 0 int)
    34 #24 := (f5 #20)
    35 #2199 := (pattern #24)
    36 #777 := (* -1::int f14)
    37 #778 := (+ #24 #777)
    38 #779 := (<= #778 0::int)
    39 #766 := (* -1::int f15)
    40 #767 := (+ #20 #766)
    41 #765 := (>= #767 0::int)
    42 #641 := (>= #20 0::int)
    43 #1440 := (not #641)
    44 #1591 := (or #1440 #765 #779)
    45 #2216 := (forall (vars (?v0 int)) (:pat #2199) #1591)
    46 #2221 := (not #2216)
    47 decl f13 :: int
    48 #73 := f13
    49 #90 := (f5 f13)
    50 #307 := (= f14 #90)
    51 #2224 := (or #307 #2221)
    52 #2227 := (not #2224)
    53 #2230 := (or #2227 #1629)
    54 #2233 := (not #2230)
    55 #820 := (* -1::int #68)
    56 decl f8 :: int
    57 #36 := f8
    58 #821 := (+ f8 #820)
    59 #819 := (>= #821 0::int)
    60 #818 := (not #819)
    61 #803 := (+ f7 #766)
    62 #802 := (= #803 -1::int)
    63 #806 := (not #802)
    64 #82 := 2::int
    65 #757 := (>= f15 2::int)
    66 #1639 := (not #757)
    67 #754 := (>= f13 0::int)
    68 #1638 := (not #754)
    69 #15 := 1::int
    70 #671 := (>= f7 1::int)
    71 #815 := (not #671)
    72 decl f6 :: int
    73 #29 := f6
    74 #668 := (>= f6 0::int)
    75 #1569 := (not #668)
    76 #426 := (= f8 f14)
    77 #432 := (not #426)
    78 #423 := (= f6 f13)
    79 #441 := (not #423)
    80 #2242 := (or #441 #432 #1569 #815 #1638 #1639 #806 #818 #2233)
    81 #2245 := (not #2242)
    82 decl f12 :: int
    83 #70 := f12
    84 #288 := (= f12 f14)
    85 #366 := (not #288)
    86 #285 := (= f7 f13)
    87 #375 := (not #285)
    88 #280 := (= #68 f12)
    89 #393 := (not #280)
    90 #2236 := (or #393 #375 #366 #1569 #815 #1638 #1639 #806 #819 #2233)
    91 #2239 := (not #2236)
    92 #2248 := (or #2239 #2245)
    93 #2251 := (not #2248)
    94 #722 := (* -1::int f7)
    95 decl f3 :: int
    96 #9 := f3
    97 #723 := (+ f3 #722)
    98 #724 := (<= #723 0::int)
    99 #2254 := (or #1569 #815 #724 #2251)
   100 #2257 := (not #2254)
   101 decl ?v0!1 :: int
   102 #1086 := ?v0!1
   103 #1094 := (f5 ?v0!1)
   104 decl f10 :: int
   105 #45 := f10
   106 #1267 := (= f10 #1094)
   107 #1091 := (>= ?v0!1 0::int)
   108 #1510 := (not #1091)
   109 #1087 := (* -1::int ?v0!1)
   110 #1088 := (+ f3 #1087)
   111 #1089 := (<= #1088 0::int)
   112 #1525 := (or #1089 #1510 #1267)
   113 #1556 := (not #1525)
   114 decl ?v0!2 :: int
   115 #1104 := ?v0!2
   116 #1105 := (f5 ?v0!2)
   117 #1291 := (* -1::int #1105)
   118 #1292 := (+ f10 #1291)
   119 #1293 := (>= #1292 0::int)
   120 #1112 := (>= ?v0!2 0::int)
   121 #1530 := (not #1112)
   122 #1108 := (* -1::int ?v0!2)
   123 #1109 := (+ f3 #1108)
   124 #1110 := (<= #1109 0::int)
   125 #1687 := (or #1110 #1530 #1293 #1556)
   126 #1690 := (not #1687)
   127 #679 := (* -1::int #20)
   128 #680 := (+ f3 #679)
   129 #681 := (<= #680 0::int)
   130 #51 := (= #24 f10)
   131 #1499 := (or #51 #1440 #681)
   132 #1504 := (not #1499)
   133 #2260 := (forall (vars (?v0 int)) (:pat #2199) #1504)
   134 #2265 := (or #2260 #1690)
   135 #2268 := (not #2265)
   136 #727 := (not #724)
   137 decl f11 :: int
   138 #47 := f11
   139 #185 := (= f7 f11)
   140 #223 := (not #185)
   141 #182 := (= f8 f10)
   142 #232 := (not #182)
   143 decl f9 :: int
   144 #43 := f9
   145 #179 := (= f6 f9)
   146 #241 := (not #179)
   147 #2271 := (or #241 #232 #223 #1569 #815 #727 #2268)
   148 #927 := (* -1::int f8)
   149 #928 := (+ #24 #927)
   150 #929 := (<= #928 0::int)
   151 #917 := (+ #20 #722)
   152 #916 := (>= #917 0::int)
   153 #1477 := (or #1440 #916 #929)
   154 #2208 := (forall (vars (?v0 int)) (:pat #2199) #1477)
   155 #2274 := (not #2271)
   156 #2277 := (or #2257 #2274)
   157 #2280 := (not #2277)
   158 #2213 := (not #2208)
   159 #655 := (* -1::int #24)
   160 decl f4 :: int
   161 #11 := f4
   162 #656 := (+ f4 #655)
   163 #654 := (>= #656 0::int)
   164 #644 := (>= #20 1::int)
   165 #1455 := (or #1440 #644 #654)
   166 #2200 := (forall (vars (?v0 int)) (:pat #2199) #1455)
   167 #2205 := (not #2200)
   168 #40 := (f5 f6)
   169 #176 := (= f8 #40)
   170 #528 := (not #176)
   171 #2283 := (or #528 #1569 #815 #2205 #2213 #2280)
   172 #2286 := (not #2283)
   173 decl ?v0!0 :: int
   174 #1046 := ?v0!0
   175 #1049 := (>= ?v0!0 0::int)
   176 #1167 := (not #1049)
   177 #1047 := (f5 ?v0!0)
   178 #1044 := (* -1::int #1047)
   179 #1045 := (+ f4 #1044)
   180 #1007 := (>= #1045 0::int)
   181 #1005 := (>= ?v0!0 1::int)
   182 #1432 := (or #1005 #1007 #1167)
   183 #2072 := (= f4 #1047)
   184 #12 := (f5 0::int)
   185 #2053 := (= #12 #1047)
   186 #1941 := (= #1047 #12)
   187 #2071 := (= ?v0!0 0::int)
   188 #1048 := (not #1005)
   189 #1437 := (not #1432)
   190 #2073 := [hypothesis]: #1437
   191 #1785 := (or #1432 #1048)
   192 #1870 := [def-axiom]: #1785
   193 #2046 := [unit-resolution #1870 #2073]: #1048
   194 #1863 := (or #1432 #1049)
   195 #1874 := [def-axiom]: #1863
   196 #2047 := [unit-resolution #1874 #2073]: #1049
   197 #2048 := [th-lemma #2047 #2046]: #2071
   198 #2052 := [monotonicity #2048]: #1941
   199 #2054 := [symm #2052]: #2053
   200 #13 := (= f4 #12)
   201 #970 := (<= f3 0::int)
   202 #918 := (not #916)
   203 #921 := (and #641 #918)
   204 #924 := (not #921)
   205 #932 := (or #924 #929)
   206 #935 := (forall (vars (?v0 int)) #932)
   207 #938 := (not #935)
   208 #809 := (and #671 #754)
   209 #812 := (not #809)
   210 #768 := (not #765)
   211 #771 := (and #641 #768)
   212 #774 := (not #771)
   213 #782 := (or #774 #779)
   214 #785 := (forall (vars (?v0 int)) #782)
   215 #788 := (not #785)
   216 #794 := (or #307 #788)
   217 #799 := (and #785 #794)
   218 #759 := (and #754 #757)
   219 #762 := (not #759)
   220 #673 := (and #668 #671)
   221 #676 := (not #673)
   222 #882 := (or #441 #432 #676 #762 #799 #806 #812 #818)
   223 #858 := (or #393 #375 #366 #815 #676 #762 #799 #806 #812 #819)
   224 #887 := (and #858 #882)
   225 #908 := (or #676 #724 #887)
   226 #705 := (* -1::int f10)
   227 #706 := (+ #24 #705)
   228 #707 := (<= #706 0::int)
   229 #682 := (not #681)
   230 #685 := (and #641 #682)
   231 #688 := (not #685)
   232 #710 := (or #688 #707)
   233 #713 := (forall (vars (?v0 int)) #710)
   234 #694 := (or #51 #688)
   235 #699 := (exists (vars (?v0 int)) #694)
   236 #702 := (not #699)
   237 #716 := (or #702 #713)
   238 #719 := (and #699 #716)
   239 #748 := (or #241 #232 #223 #676 #719 #727)
   240 #913 := (and #748 #908)
   241 #561 := (not #13)
   242 #956 := (or #561 #528 #676 #913 #938)
   243 #961 := (and #13 #956)
   244 #642 := (not #644)
   245 #646 := (and #641 #642)
   246 #649 := (not #646)
   247 #658 := (or #649 #654)
   248 #661 := (forall (vars (?v0 int)) #658)
   249 #664 := (not #661)
   250 #964 := (or #664 #961)
   251 #967 := (and #661 #964)
   252 #990 := (or #561 #967 #970)
   253 #995 := (not #990)
   254 #1 := true
   255 #91 := (= #90 f14)
   256 #92 := (and #91 true)
   257 #87 := (<= #24 f14)
   258 #85 := (< #20 f15)
   259 #21 := (<= 0::int #20)
   260 #86 := (and #21 #85)
   261 #88 := (implies #86 #87)
   262 #89 := (forall (vars (?v0 int)) #88)
   263 #93 := (implies #89 #92)
   264 #94 := (and #89 #93)
   265 #83 := (<= 2::int f15)
   266 #77 := (<= 0::int f13)
   267 #84 := (and #77 #83)
   268 #95 := (implies #84 #94)
   269 #80 := (+ f7 1::int)
   270 #81 := (= f15 #80)
   271 #96 := (implies #81 #95)
   272 #32 := (<= 1::int f7)
   273 #78 := (and #77 #32)
   274 #97 := (implies #78 #96)
   275 #98 := (implies true #97)
   276 #108 := (= f14 f8)
   277 #109 := (implies #108 #98)
   278 #107 := (= f13 f6)
   279 #110 := (implies #107 #109)
   280 #30 := (<= 0::int f6)
   281 #33 := (and #30 #32)
   282 #111 := (implies #33 #110)
   283 #106 := (<= #68 f8)
   284 #112 := (implies #106 #111)
   285 #113 := (implies #33 #112)
   286 #114 := (implies true #113)
   287 #76 := (= f14 f12)
   288 #99 := (implies #76 #98)
   289 #74 := (= f13 f7)
   290 #100 := (implies #74 #99)
   291 #72 := (and #32 #32)
   292 #101 := (implies #72 #100)
   293 #71 := (= f12 #68)
   294 #102 := (implies #71 #101)
   295 #69 := (< f8 #68)
   296 #103 := (implies #69 #102)
   297 #104 := (implies #33 #103)
   298 #105 := (implies true #104)
   299 #115 := (and #105 #114)
   300 #116 := (implies #33 #115)
   301 #67 := (< f7 f3)
   302 #117 := (implies #67 #116)
   303 #118 := (implies #33 #117)
   304 #119 := (implies true #118)
   305 #54 := (<= #24 f10)
   306 #49 := (< #20 f3)
   307 #50 := (and #21 #49)
   308 #55 := (implies #50 #54)
   309 #56 := (forall (vars (?v0 int)) #55)
   310 #57 := (and #56 true)
   311 #52 := (implies #50 #51)
   312 #53 := (exists (vars (?v0 int)) #52)
   313 #58 := (implies #53 #57)
   314 #59 := (and #53 #58)
   315 #48 := (= f11 f7)
   316 #60 := (implies #48 #59)
   317 #46 := (= f10 f8)
   318 #61 := (implies #46 #60)
   319 #44 := (= f9 f6)
   320 #62 := (implies #44 #61)
   321 #63 := (implies #33 #62)
   322 #42 := (<= f3 f7)
   323 #64 := (implies #42 #63)
   324 #65 := (implies #33 #64)
   325 #66 := (implies true #65)
   326 #120 := (and #66 #119)
   327 #121 := (implies #33 #120)
   328 #41 := (= #40 f8)
   329 #122 := (implies #41 #121)
   330 #37 := (<= #24 f8)
   331 #34 := (< #20 f7)
   332 #35 := (and #21 #34)
   333 #38 := (implies #35 #37)
   334 #39 := (forall (vars (?v0 int)) #38)
   335 #123 := (implies #39 #122)
   336 #124 := (implies #33 #123)
   337 #125 := (implies true #124)
   338 #28 := (= #12 f4)
   339 #126 := (implies #28 #125)
   340 #127 := (and #28 #126)
   341 #25 := (<= #24 f4)
   342 #22 := (< #20 1::int)
   343 #23 := (and #21 #22)
   344 #26 := (implies #23 #25)
   345 #27 := (forall (vars (?v0 int)) #26)
   346 #128 := (implies #27 #127)
   347 #129 := (and #27 #128)
   348 #16 := (<= 1::int 1::int)
   349 #17 := (and #16 #16)
   350 #14 := (<= 0::int 0::int)
   351 #18 := (and #14 #17)
   352 #19 := (and #14 #18)
   353 #130 := (implies #19 #129)
   354 #131 := (implies #13 #130)
   355 #10 := (< 0::int f3)
   356 #132 := (implies #10 #131)
   357 #133 := (implies true #132)
   358 #134 := (not #133)
   359 #998 := (iff #134 #995)
   360 #300 := (not #86)
   361 #301 := (or #300 #87)
   362 #304 := (forall (vars (?v0 int)) #301)
   363 #320 := (not #304)
   364 #321 := (or #320 #307)
   365 #326 := (and #304 #321)
   366 #332 := (not #84)
   367 #333 := (or #332 #326)
   368 #294 := (+ 1::int f7)
   369 #297 := (= f15 #294)
   370 #341 := (not #297)
   371 #342 := (or #341 #333)
   372 #291 := (and #32 #77)
   373 #350 := (not #291)
   374 #351 := (or #350 #342)
   375 #433 := (or #351 #432)
   376 #442 := (or #441 #433)
   377 #250 := (not #33)
   378 #450 := (or #250 #442)
   379 #458 := (not #106)
   380 #459 := (or #458 #450)
   381 #467 := (or #250 #459)
   382 #367 := (or #366 #351)
   383 #376 := (or #375 #367)
   384 #384 := (not #32)
   385 #385 := (or #384 #376)
   386 #394 := (or #393 #385)
   387 #402 := (not #69)
   388 #403 := (or #402 #394)
   389 #411 := (or #250 #403)
   390 #479 := (and #411 #467)
   391 #485 := (or #250 #479)
   392 #493 := (not #67)
   393 #494 := (or #493 #485)
   394 #502 := (or #250 #494)
   395 #188 := (not #50)
   396 #195 := (or #188 #54)
   397 #198 := (forall (vars (?v0 int)) #195)
   398 #189 := (or #188 #51)
   399 #192 := (exists (vars (?v0 int)) #189)
   400 #211 := (not #192)
   401 #212 := (or #211 #198)
   402 #217 := (and #192 #212)
   403 #224 := (or #223 #217)
   404 #233 := (or #232 #224)
   405 #242 := (or #241 #233)
   406 #251 := (or #250 #242)
   407 #259 := (not #42)
   408 #260 := (or #259 #251)
   409 #268 := (or #250 #260)
   410 #514 := (and #268 #502)
   411 #520 := (or #250 #514)
   412 #529 := (or #528 #520)
   413 #169 := (not #35)
   414 #170 := (or #169 #37)
   415 #173 := (forall (vars (?v0 int)) #170)
   416 #537 := (not #173)
   417 #538 := (or #537 #529)
   418 #546 := (or #250 #538)
   419 #562 := (or #561 #546)
   420 #567 := (and #13 #562)
   421 #160 := (not #23)
   422 #161 := (or #160 #25)
   423 #164 := (forall (vars (?v0 int)) #161)
   424 #573 := (not #164)
   425 #574 := (or #573 #567)
   426 #579 := (and #164 #574)
   427 #154 := (and #14 #16)
   428 #157 := (and #14 #154)
   429 #585 := (not #157)
   430 #586 := (or #585 #579)
   431 #594 := (or #561 #586)
   432 #602 := (not #10)
   433 #603 := (or #602 #594)
   434 #615 := (not #603)
   435 #996 := (iff #615 #995)
   436 #993 := (iff #603 #990)
   437 #981 := (or false #967)
   438 #984 := (or #561 #981)
   439 #987 := (or #970 #984)
   440 #991 := (iff #987 #990)
   441 #992 := [rewrite]: #991
   442 #988 := (iff #603 #987)
   443 #985 := (iff #594 #984)
   444 #982 := (iff #586 #981)
   445 #968 := (iff #579 #967)
   446 #965 := (iff #574 #964)
   447 #962 := (iff #567 #961)
   448 #959 := (iff #562 #956)
   449 #941 := (or #676 #913)
   450 #944 := (or #528 #941)
   451 #947 := (or #938 #944)
   452 #950 := (or #676 #947)
   453 #953 := (or #561 #950)
   454 #957 := (iff #953 #956)
   455 #958 := [rewrite]: #957
   456 #954 := (iff #562 #953)
   457 #951 := (iff #546 #950)
   458 #948 := (iff #538 #947)
   459 #945 := (iff #529 #944)
   460 #942 := (iff #520 #941)
   461 #914 := (iff #514 #913)
   462 #911 := (iff #502 #908)
   463 #899 := (or #676 #887)
   464 #902 := (or #724 #899)
   465 #905 := (or #676 #902)
   466 #909 := (iff #905 #908)
   467 #910 := [rewrite]: #909
   468 #906 := (iff #502 #905)
   469 #903 := (iff #494 #902)
   470 #900 := (iff #485 #899)
   471 #888 := (iff #479 #887)
   472 #885 := (iff #467 #882)
   473 #831 := (or #762 #799)
   474 #834 := (or #806 #831)
   475 #837 := (or #812 #834)
   476 #867 := (or #837 #432)
   477 #870 := (or #441 #867)
   478 #873 := (or #676 #870)
   479 #876 := (or #818 #873)
   480 #879 := (or #676 #876)
   481 #883 := (iff #879 #882)
   482 #884 := [rewrite]: #883
   483 #880 := (iff #467 #879)
   484 #877 := (iff #459 #876)
   485 #874 := (iff #450 #873)
   486 #871 := (iff #442 #870)
   487 #868 := (iff #433 #867)
   488 #838 := (iff #351 #837)
   489 #835 := (iff #342 #834)
   490 #832 := (iff #333 #831)
   491 #800 := (iff #326 #799)
   492 #797 := (iff #321 #794)
   493 #791 := (or #788 #307)
   494 #795 := (iff #791 #794)
   495 #796 := [rewrite]: #795
   496 #792 := (iff #321 #791)
   497 #789 := (iff #320 #788)
   498 #786 := (iff #304 #785)
   499 #783 := (iff #301 #782)
   500 #780 := (iff #87 #779)
   501 #781 := [rewrite]: #780
   502 #775 := (iff #300 #774)
   503 #772 := (iff #86 #771)
   504 #769 := (iff #85 #768)
   505 #770 := [rewrite]: #769
   506 #639 := (iff #21 #641)
   507 #640 := [rewrite]: #639
   508 #773 := [monotonicity #640 #770]: #772
   509 #776 := [monotonicity #773]: #775
   510 #784 := [monotonicity #776 #781]: #783
   511 #787 := [quant-intro #784]: #786
   512 #790 := [monotonicity #787]: #789
   513 #793 := [monotonicity #790]: #792
   514 #798 := [trans #793 #796]: #797
   515 #801 := [monotonicity #787 #798]: #800
   516 #763 := (iff #332 #762)
   517 #760 := (iff #84 #759)
   518 #756 := (iff #83 #757)
   519 #758 := [rewrite]: #756
   520 #753 := (iff #77 #754)
   521 #755 := [rewrite]: #753
   522 #761 := [monotonicity #755 #758]: #760
   523 #764 := [monotonicity #761]: #763
   524 #833 := [monotonicity #764 #801]: #832
   525 #807 := (iff #341 #806)
   526 #804 := (iff #297 #802)
   527 #805 := [rewrite]: #804
   528 #808 := [monotonicity #805]: #807
   529 #836 := [monotonicity #808 #833]: #835
   530 #813 := (iff #350 #812)
   531 #810 := (iff #291 #809)
   532 #670 := (iff #32 #671)
   533 #672 := [rewrite]: #670
   534 #811 := [monotonicity #672 #755]: #810
   535 #814 := [monotonicity #811]: #813
   536 #839 := [monotonicity #814 #836]: #838
   537 #869 := [monotonicity #839]: #868
   538 #872 := [monotonicity #869]: #871
   539 #677 := (iff #250 #676)
   540 #674 := (iff #33 #673)
   541 #667 := (iff #30 #668)
   542 #669 := [rewrite]: #667
   543 #675 := [monotonicity #669 #672]: #674
   544 #678 := [monotonicity #675]: #677
   545 #875 := [monotonicity #678 #872]: #874
   546 #865 := (iff #458 #818)
   547 #863 := (iff #106 #819)
   548 #864 := [rewrite]: #863
   549 #866 := [monotonicity #864]: #865
   550 #878 := [monotonicity #866 #875]: #877
   551 #881 := [monotonicity #678 #878]: #880
   552 #886 := [trans #881 #884]: #885
   553 #861 := (iff #411 #858)
   554 #840 := (or #366 #837)
   555 #843 := (or #375 #840)
   556 #846 := (or #815 #843)
   557 #849 := (or #393 #846)
   558 #852 := (or #819 #849)
   559 #855 := (or #676 #852)
   560 #859 := (iff #855 #858)
   561 #860 := [rewrite]: #859
   562 #856 := (iff #411 #855)
   563 #853 := (iff #403 #852)
   564 #850 := (iff #394 #849)
   565 #847 := (iff #385 #846)
   566 #844 := (iff #376 #843)
   567 #841 := (iff #367 #840)
   568 #842 := [monotonicity #839]: #841
   569 #845 := [monotonicity #842]: #844
   570 #816 := (iff #384 #815)
   571 #817 := [monotonicity #672]: #816
   572 #848 := [monotonicity #817 #845]: #847
   573 #851 := [monotonicity #848]: #850
   574 #829 := (iff #402 #819)
   575 #824 := (not #818)
   576 #827 := (iff #824 #819)
   577 #828 := [rewrite]: #827
   578 #825 := (iff #402 #824)
   579 #822 := (iff #69 #818)
   580 #823 := [rewrite]: #822
   581 #826 := [monotonicity #823]: #825
   582 #830 := [trans #826 #828]: #829
   583 #854 := [monotonicity #830 #851]: #853
   584 #857 := [monotonicity #678 #854]: #856
   585 #862 := [trans #857 #860]: #861
   586 #889 := [monotonicity #862 #886]: #888
   587 #901 := [monotonicity #678 #889]: #900
   588 #897 := (iff #493 #724)
   589 #892 := (not #727)
   590 #895 := (iff #892 #724)
   591 #896 := [rewrite]: #895
   592 #893 := (iff #493 #892)
   593 #890 := (iff #67 #727)
   594 #891 := [rewrite]: #890
   595 #894 := [monotonicity #891]: #893
   596 #898 := [trans #894 #896]: #897
   597 #904 := [monotonicity #898 #901]: #903
   598 #907 := [monotonicity #678 #904]: #906
   599 #912 := [trans #907 #910]: #911
   600 #751 := (iff #268 #748)
   601 #730 := (or #223 #719)
   602 #733 := (or #232 #730)
   603 #736 := (or #241 #733)
   604 #739 := (or #676 #736)
   605 #742 := (or #727 #739)
   606 #745 := (or #676 #742)
   607 #749 := (iff #745 #748)
   608 #750 := [rewrite]: #749
   609 #746 := (iff #268 #745)
   610 #743 := (iff #260 #742)
   611 #740 := (iff #251 #739)
   612 #737 := (iff #242 #736)
   613 #734 := (iff #233 #733)
   614 #731 := (iff #224 #730)
   615 #720 := (iff #217 #719)
   616 #717 := (iff #212 #716)
   617 #714 := (iff #198 #713)
   618 #711 := (iff #195 #710)
   619 #708 := (iff #54 #707)
   620 #709 := [rewrite]: #708
   621 #689 := (iff #188 #688)
   622 #686 := (iff #50 #685)
   623 #683 := (iff #49 #682)
   624 #684 := [rewrite]: #683
   625 #687 := [monotonicity #640 #684]: #686
   626 #690 := [monotonicity #687]: #689
   627 #712 := [monotonicity #690 #709]: #711
   628 #715 := [quant-intro #712]: #714
   629 #703 := (iff #211 #702)
   630 #700 := (iff #192 #699)
   631 #697 := (iff #189 #694)
   632 #691 := (or #688 #51)
   633 #695 := (iff #691 #694)
   634 #696 := [rewrite]: #695
   635 #692 := (iff #189 #691)
   636 #693 := [monotonicity #690]: #692
   637 #698 := [trans #693 #696]: #697
   638 #701 := [quant-intro #698]: #700
   639 #704 := [monotonicity #701]: #703
   640 #718 := [monotonicity #704 #715]: #717
   641 #721 := [monotonicity #701 #718]: #720
   642 #732 := [monotonicity #721]: #731
   643 #735 := [monotonicity #732]: #734
   644 #738 := [monotonicity #735]: #737
   645 #741 := [monotonicity #678 #738]: #740
   646 #728 := (iff #259 #727)
   647 #725 := (iff #42 #724)
   648 #726 := [rewrite]: #725
   649 #729 := [monotonicity #726]: #728
   650 #744 := [monotonicity #729 #741]: #743
   651 #747 := [monotonicity #678 #744]: #746
   652 #752 := [trans #747 #750]: #751
   653 #915 := [monotonicity #752 #912]: #914
   654 #943 := [monotonicity #678 #915]: #942
   655 #946 := [monotonicity #943]: #945
   656 #939 := (iff #537 #938)
   657 #936 := (iff #173 #935)
   658 #933 := (iff #170 #932)
   659 #930 := (iff #37 #929)
   660 #931 := [rewrite]: #930
   661 #925 := (iff #169 #924)
   662 #922 := (iff #35 #921)
   663 #919 := (iff #34 #918)
   664 #920 := [rewrite]: #919
   665 #923 := [monotonicity #640 #920]: #922
   666 #926 := [monotonicity #923]: #925
   667 #934 := [monotonicity #926 #931]: #933
   668 #937 := [quant-intro #934]: #936
   669 #940 := [monotonicity #937]: #939
   670 #949 := [monotonicity #940 #946]: #948
   671 #952 := [monotonicity #678 #949]: #951
   672 #955 := [monotonicity #952]: #954
   673 #960 := [trans #955 #958]: #959
   674 #963 := [monotonicity #960]: #962
   675 #665 := (iff #573 #664)
   676 #662 := (iff #164 #661)
   677 #659 := (iff #161 #658)
   678 #653 := (iff #25 #654)
   679 #657 := [rewrite]: #653
   680 #650 := (iff #160 #649)
   681 #647 := (iff #23 #646)
   682 #643 := (iff #22 #642)
   683 #645 := [rewrite]: #643
   684 #648 := [monotonicity #640 #645]: #647
   685 #651 := [monotonicity #648]: #650
   686 #660 := [monotonicity #651 #657]: #659
   687 #663 := [quant-intro #660]: #662
   688 #666 := [monotonicity #663]: #665
   689 #966 := [monotonicity #666 #963]: #965
   690 #969 := [monotonicity #663 #966]: #968
   691 #637 := (iff #585 false)
   692 #632 := (not true)
   693 #635 := (iff #632 false)
   694 #636 := [rewrite]: #635
   695 #633 := (iff #585 #632)
   696 #630 := (iff #157 true)
   697 #622 := (and true true)
   698 #625 := (and true #622)
   699 #628 := (iff #625 true)
   700 #629 := [rewrite]: #628
   701 #626 := (iff #157 #625)
   702 #623 := (iff #154 #622)
   703 #620 := (iff #16 true)
   704 #621 := [rewrite]: #620
   705 #618 := (iff #14 true)
   706 #619 := [rewrite]: #618
   707 #624 := [monotonicity #619 #621]: #623
   708 #627 := [monotonicity #619 #624]: #626
   709 #631 := [trans #627 #629]: #630
   710 #634 := [monotonicity #631]: #633
   711 #638 := [trans #634 #636]: #637
   712 #983 := [monotonicity #638 #969]: #982
   713 #986 := [monotonicity #983]: #985
   714 #979 := (iff #602 #970)
   715 #971 := (not #970)
   716 #974 := (not #971)
   717 #977 := (iff #974 #970)
   718 #978 := [rewrite]: #977
   719 #975 := (iff #602 #974)
   720 #972 := (iff #10 #971)
   721 #973 := [rewrite]: #972
   722 #976 := [monotonicity #973]: #975
   723 #980 := [trans #976 #978]: #979
   724 #989 := [monotonicity #980 #986]: #988
   725 #994 := [trans #989 #992]: #993
   726 #997 := [monotonicity #994]: #996
   727 #616 := (iff #134 #615)
   728 #613 := (iff #133 #603)
   729 #608 := (implies true #603)
   730 #611 := (iff #608 #603)
   731 #612 := [rewrite]: #611
   732 #609 := (iff #133 #608)
   733 #606 := (iff #132 #603)
   734 #599 := (implies #10 #594)
   735 #604 := (iff #599 #603)
   736 #605 := [rewrite]: #604
   737 #600 := (iff #132 #599)
   738 #597 := (iff #131 #594)
   739 #591 := (implies #13 #586)
   740 #595 := (iff #591 #594)
   741 #596 := [rewrite]: #595
   742 #592 := (iff #131 #591)
   743 #589 := (iff #130 #586)
   744 #582 := (implies #157 #579)
   745 #587 := (iff #582 #586)
   746 #588 := [rewrite]: #587
   747 #583 := (iff #130 #582)
   748 #580 := (iff #129 #579)
   749 #577 := (iff #128 #574)
   750 #570 := (implies #164 #567)
   751 #575 := (iff #570 #574)
   752 #576 := [rewrite]: #575
   753 #571 := (iff #128 #570)
   754 #568 := (iff #127 #567)
   755 #565 := (iff #126 #562)
   756 #558 := (implies #13 #546)
   757 #563 := (iff #558 #562)
   758 #564 := [rewrite]: #563
   759 #559 := (iff #126 #558)
   760 #556 := (iff #125 #546)
   761 #551 := (implies true #546)
   762 #554 := (iff #551 #546)
   763 #555 := [rewrite]: #554
   764 #552 := (iff #125 #551)
   765 #549 := (iff #124 #546)
   766 #543 := (implies #33 #538)
   767 #547 := (iff #543 #546)
   768 #548 := [rewrite]: #547
   769 #544 := (iff #124 #543)
   770 #541 := (iff #123 #538)
   771 #534 := (implies #173 #529)
   772 #539 := (iff #534 #538)
   773 #540 := [rewrite]: #539
   774 #535 := (iff #123 #534)
   775 #532 := (iff #122 #529)
   776 #525 := (implies #176 #520)
   777 #530 := (iff #525 #529)
   778 #531 := [rewrite]: #530
   779 #526 := (iff #122 #525)
   780 #523 := (iff #121 #520)
   781 #517 := (implies #33 #514)
   782 #521 := (iff #517 #520)
   783 #522 := [rewrite]: #521
   784 #518 := (iff #121 #517)
   785 #515 := (iff #120 #514)
   786 #512 := (iff #119 #502)
   787 #507 := (implies true #502)
   788 #510 := (iff #507 #502)
   789 #511 := [rewrite]: #510
   790 #508 := (iff #119 #507)
   791 #505 := (iff #118 #502)
   792 #499 := (implies #33 #494)
   793 #503 := (iff #499 #502)
   794 #504 := [rewrite]: #503
   795 #500 := (iff #118 #499)
   796 #497 := (iff #117 #494)
   797 #490 := (implies #67 #485)
   798 #495 := (iff #490 #494)
   799 #496 := [rewrite]: #495
   800 #491 := (iff #117 #490)
   801 #488 := (iff #116 #485)
   802 #482 := (implies #33 #479)
   803 #486 := (iff #482 #485)
   804 #487 := [rewrite]: #486
   805 #483 := (iff #116 #482)
   806 #480 := (iff #115 #479)
   807 #477 := (iff #114 #467)
   808 #472 := (implies true #467)
   809 #475 := (iff #472 #467)
   810 #476 := [rewrite]: #475
   811 #473 := (iff #114 #472)
   812 #470 := (iff #113 #467)
   813 #464 := (implies #33 #459)
   814 #468 := (iff #464 #467)
   815 #469 := [rewrite]: #468
   816 #465 := (iff #113 #464)
   817 #462 := (iff #112 #459)
   818 #455 := (implies #106 #450)
   819 #460 := (iff #455 #459)
   820 #461 := [rewrite]: #460
   821 #456 := (iff #112 #455)
   822 #453 := (iff #111 #450)
   823 #447 := (implies #33 #442)
   824 #451 := (iff #447 #450)
   825 #452 := [rewrite]: #451
   826 #448 := (iff #111 #447)
   827 #445 := (iff #110 #442)
   828 #438 := (implies #423 #433)
   829 #443 := (iff #438 #442)
   830 #444 := [rewrite]: #443
   831 #439 := (iff #110 #438)
   832 #436 := (iff #109 #433)
   833 #429 := (implies #426 #351)
   834 #434 := (iff #429 #433)
   835 #435 := [rewrite]: #434
   836 #430 := (iff #109 #429)
   837 #361 := (iff #98 #351)
   838 #356 := (implies true #351)
   839 #359 := (iff #356 #351)
   840 #360 := [rewrite]: #359
   841 #357 := (iff #98 #356)
   842 #354 := (iff #97 #351)
   843 #347 := (implies #291 #342)
   844 #352 := (iff #347 #351)
   845 #353 := [rewrite]: #352
   846 #348 := (iff #97 #347)
   847 #345 := (iff #96 #342)
   848 #338 := (implies #297 #333)
   849 #343 := (iff #338 #342)
   850 #344 := [rewrite]: #343
   851 #339 := (iff #96 #338)
   852 #336 := (iff #95 #333)
   853 #329 := (implies #84 #326)
   854 #334 := (iff #329 #333)
   855 #335 := [rewrite]: #334
   856 #330 := (iff #95 #329)
   857 #327 := (iff #94 #326)
   858 #324 := (iff #93 #321)
   859 #317 := (implies #304 #307)
   860 #322 := (iff #317 #321)
   861 #323 := [rewrite]: #322
   862 #318 := (iff #93 #317)
   863 #315 := (iff #92 #307)
   864 #310 := (and #307 true)
   865 #313 := (iff #310 #307)
   866 #314 := [rewrite]: #313
   867 #311 := (iff #92 #310)
   868 #308 := (iff #91 #307)
   869 #309 := [rewrite]: #308
   870 #312 := [monotonicity #309]: #311
   871 #316 := [trans #312 #314]: #315
   872 #305 := (iff #89 #304)
   873 #302 := (iff #88 #301)
   874 #303 := [rewrite]: #302
   875 #306 := [quant-intro #303]: #305
   876 #319 := [monotonicity #306 #316]: #318
   877 #325 := [trans #319 #323]: #324
   878 #328 := [monotonicity #306 #325]: #327
   879 #331 := [monotonicity #328]: #330
   880 #337 := [trans #331 #335]: #336
   881 #298 := (iff #81 #297)
   882 #295 := (= #80 #294)
   883 #296 := [rewrite]: #295
   884 #299 := [monotonicity #296]: #298
   885 #340 := [monotonicity #299 #337]: #339
   886 #346 := [trans #340 #344]: #345
   887 #292 := (iff #78 #291)
   888 #293 := [rewrite]: #292
   889 #349 := [monotonicity #293 #346]: #348
   890 #355 := [trans #349 #353]: #354
   891 #358 := [monotonicity #355]: #357
   892 #362 := [trans #358 #360]: #361
   893 #427 := (iff #108 #426)
   894 #428 := [rewrite]: #427
   895 #431 := [monotonicity #428 #362]: #430
   896 #437 := [trans #431 #435]: #436
   897 #424 := (iff #107 #423)
   898 #425 := [rewrite]: #424
   899 #440 := [monotonicity #425 #437]: #439
   900 #446 := [trans #440 #444]: #445
   901 #449 := [monotonicity #446]: #448
   902 #454 := [trans #449 #452]: #453
   903 #457 := [monotonicity #454]: #456
   904 #463 := [trans #457 #461]: #462
   905 #466 := [monotonicity #463]: #465
   906 #471 := [trans #466 #469]: #470
   907 #474 := [monotonicity #471]: #473
   908 #478 := [trans #474 #476]: #477
   909 #421 := (iff #105 #411)
   910 #416 := (implies true #411)
   911 #419 := (iff #416 #411)
   912 #420 := [rewrite]: #419
   913 #417 := (iff #105 #416)
   914 #414 := (iff #104 #411)
   915 #408 := (implies #33 #403)
   916 #412 := (iff #408 #411)
   917 #413 := [rewrite]: #412
   918 #409 := (iff #104 #408)
   919 #406 := (iff #103 #403)
   920 #399 := (implies #69 #394)
   921 #404 := (iff #399 #403)
   922 #405 := [rewrite]: #404
   923 #400 := (iff #103 #399)
   924 #397 := (iff #102 #394)
   925 #390 := (implies #280 #385)
   926 #395 := (iff #390 #394)
   927 #396 := [rewrite]: #395
   928 #391 := (iff #102 #390)
   929 #388 := (iff #101 #385)
   930 #381 := (implies #32 #376)
   931 #386 := (iff #381 #385)
   932 #387 := [rewrite]: #386
   933 #382 := (iff #101 #381)
   934 #379 := (iff #100 #376)
   935 #372 := (implies #285 #367)
   936 #377 := (iff #372 #376)
   937 #378 := [rewrite]: #377
   938 #373 := (iff #100 #372)
   939 #370 := (iff #99 #367)
   940 #363 := (implies #288 #351)
   941 #368 := (iff #363 #367)
   942 #369 := [rewrite]: #368
   943 #364 := (iff #99 #363)
   944 #289 := (iff #76 #288)
   945 #290 := [rewrite]: #289
   946 #365 := [monotonicity #290 #362]: #364
   947 #371 := [trans #365 #369]: #370
   948 #286 := (iff #74 #285)
   949 #287 := [rewrite]: #286
   950 #374 := [monotonicity #287 #371]: #373
   951 #380 := [trans #374 #378]: #379
   952 #283 := (iff #72 #32)
   953 #284 := [rewrite]: #283
   954 #383 := [monotonicity #284 #380]: #382
   955 #389 := [trans #383 #387]: #388
   956 #281 := (iff #71 #280)
   957 #282 := [rewrite]: #281
   958 #392 := [monotonicity #282 #389]: #391
   959 #398 := [trans #392 #396]: #397
   960 #401 := [monotonicity #398]: #400
   961 #407 := [trans #401 #405]: #406
   962 #410 := [monotonicity #407]: #409
   963 #415 := [trans #410 #413]: #414
   964 #418 := [monotonicity #415]: #417
   965 #422 := [trans #418 #420]: #421
   966 #481 := [monotonicity #422 #478]: #480
   967 #484 := [monotonicity #481]: #483
   968 #489 := [trans #484 #487]: #488
   969 #492 := [monotonicity #489]: #491
   970 #498 := [trans #492 #496]: #497
   971 #501 := [monotonicity #498]: #500
   972 #506 := [trans #501 #504]: #505
   973 #509 := [monotonicity #506]: #508
   974 #513 := [trans #509 #511]: #512
   975 #278 := (iff #66 #268)
   976 #273 := (implies true #268)
   977 #276 := (iff #273 #268)
   978 #277 := [rewrite]: #276
   979 #274 := (iff #66 #273)
   980 #271 := (iff #65 #268)
   981 #265 := (implies #33 #260)
   982 #269 := (iff #265 #268)
   983 #270 := [rewrite]: #269
   984 #266 := (iff #65 #265)
   985 #263 := (iff #64 #260)
   986 #256 := (implies #42 #251)
   987 #261 := (iff #256 #260)
   988 #262 := [rewrite]: #261
   989 #257 := (iff #64 #256)
   990 #254 := (iff #63 #251)
   991 #247 := (implies #33 #242)
   992 #252 := (iff #247 #251)
   993 #253 := [rewrite]: #252
   994 #248 := (iff #63 #247)
   995 #245 := (iff #62 #242)
   996 #238 := (implies #179 #233)
   997 #243 := (iff #238 #242)
   998 #244 := [rewrite]: #243
   999 #239 := (iff #62 #238)
  1000 #236 := (iff #61 #233)
  1001 #229 := (implies #182 #224)
  1002 #234 := (iff #229 #233)
  1003 #235 := [rewrite]: #234
  1004 #230 := (iff #61 #229)
  1005 #227 := (iff #60 #224)
  1006 #220 := (implies #185 #217)
  1007 #225 := (iff #220 #224)
  1008 #226 := [rewrite]: #225
  1009 #221 := (iff #60 #220)
  1010 #218 := (iff #59 #217)
  1011 #215 := (iff #58 #212)
  1012 #208 := (implies #192 #198)
  1013 #213 := (iff #208 #212)
  1014 #214 := [rewrite]: #213
  1015 #209 := (iff #58 #208)
  1016 #206 := (iff #57 #198)
  1017 #201 := (and #198 true)
  1018 #204 := (iff #201 #198)
  1019 #205 := [rewrite]: #204
  1020 #202 := (iff #57 #201)
  1021 #199 := (iff #56 #198)
  1022 #196 := (iff #55 #195)
  1023 #197 := [rewrite]: #196
  1024 #200 := [quant-intro #197]: #199
  1025 #203 := [monotonicity #200]: #202
  1026 #207 := [trans #203 #205]: #206
  1027 #193 := (iff #53 #192)
  1028 #190 := (iff #52 #189)
  1029 #191 := [rewrite]: #190
  1030 #194 := [quant-intro #191]: #193
  1031 #210 := [monotonicity #194 #207]: #209
  1032 #216 := [trans #210 #214]: #215
  1033 #219 := [monotonicity #194 #216]: #218
  1034 #186 := (iff #48 #185)
  1035 #187 := [rewrite]: #186
  1036 #222 := [monotonicity #187 #219]: #221
  1037 #228 := [trans #222 #226]: #227
  1038 #183 := (iff #46 #182)
  1039 #184 := [rewrite]: #183
  1040 #231 := [monotonicity #184 #228]: #230
  1041 #237 := [trans #231 #235]: #236
  1042 #180 := (iff #44 #179)
  1043 #181 := [rewrite]: #180
  1044 #240 := [monotonicity #181 #237]: #239
  1045 #246 := [trans #240 #244]: #245
  1046 #249 := [monotonicity #246]: #248
  1047 #255 := [trans #249 #253]: #254
  1048 #258 := [monotonicity #255]: #257
  1049 #264 := [trans #258 #262]: #263
  1050 #267 := [monotonicity #264]: #266
  1051 #272 := [trans #267 #270]: #271
  1052 #275 := [monotonicity #272]: #274
  1053 #279 := [trans #275 #277]: #278
  1054 #516 := [monotonicity #279 #513]: #515
  1055 #519 := [monotonicity #516]: #518
  1056 #524 := [trans #519 #522]: #523
  1057 #177 := (iff #41 #176)
  1058 #178 := [rewrite]: #177
  1059 #527 := [monotonicity #178 #524]: #526
  1060 #533 := [trans #527 #531]: #532
  1061 #174 := (iff #39 #173)
  1062 #171 := (iff #38 #170)
  1063 #172 := [rewrite]: #171
  1064 #175 := [quant-intro #172]: #174
  1065 #536 := [monotonicity #175 #533]: #535
  1066 #542 := [trans #536 #540]: #541
  1067 #545 := [monotonicity #542]: #544
  1068 #550 := [trans #545 #548]: #549
  1069 #553 := [monotonicity #550]: #552
  1070 #557 := [trans #553 #555]: #556
  1071 #167 := (iff #28 #13)
  1072 #168 := [rewrite]: #167
  1073 #560 := [monotonicity #168 #557]: #559
  1074 #566 := [trans #560 #564]: #565
  1075 #569 := [monotonicity #168 #566]: #568
  1076 #165 := (iff #27 #164)
  1077 #162 := (iff #26 #161)
  1078 #163 := [rewrite]: #162
  1079 #166 := [quant-intro #163]: #165
  1080 #572 := [monotonicity #166 #569]: #571
  1081 #578 := [trans #572 #576]: #577
  1082 #581 := [monotonicity #166 #578]: #580
  1083 #158 := (iff #19 #157)
  1084 #155 := (iff #18 #154)
  1085 #152 := (iff #17 #16)
  1086 #153 := [rewrite]: #152
  1087 #156 := [monotonicity #153]: #155
  1088 #159 := [monotonicity #156]: #158
  1089 #584 := [monotonicity #159 #581]: #583
  1090 #590 := [trans #584 #588]: #589
  1091 #593 := [monotonicity #590]: #592
  1092 #598 := [trans #593 #596]: #597
  1093 #601 := [monotonicity #598]: #600
  1094 #607 := [trans #601 #605]: #606
  1095 #610 := [monotonicity #607]: #609
  1096 #614 := [trans #610 #612]: #613
  1097 #617 := [monotonicity #614]: #616
  1098 #999 := [trans #617 #997]: #998
  1099 #151 := [asserted]: #134
  1100 #1000 := [mp #151 #999]: #995
  1101 #1001 := [not-or-elim #1000]: #13
  1102 #2045 := [trans #1001 #2054]: #2072
  1103 #1786 := (not #1007)
  1104 #1871 := (or #1432 #1786)
  1105 #1872 := [def-axiom]: #1871
  1106 #2051 := [unit-resolution #1872 #2073]: #1786
  1107 #2050 := (not #2072)
  1108 #2019 := (or #2050 #1007)
  1109 #2026 := [th-lemma]: #2019
  1110 #1985 := [unit-resolution #2026 #2051 #2045]: false
  1111 #2016 := [lemma #1985]: #1432
  1112 #2289 := (or #1437 #2286)
  1113 #1507 := (forall (vars (?v0 int)) #1504)
  1114 #1693 := (or #1507 #1690)
  1115 #1696 := (not #1693)
  1116 #1699 := (or #241 #232 #223 #1569 #815 #727 #1696)
  1117 #1702 := (not #1699)
  1118 #1596 := (forall (vars (?v0 int)) #1591)
  1119 #1602 := (not #1596)
  1120 #1603 := (or #307 #1602)
  1121 #1604 := (not #1603)
  1122 #1632 := (or #1604 #1629)
  1123 #1640 := (not #1632)
  1124 #1650 := (or #441 #432 #1569 #815 #1638 #1639 #806 #818 #1640)
  1125 #1651 := (not #1650)
  1126 #1641 := (or #393 #375 #366 #1569 #815 #1638 #1639 #806 #819 #1640)
  1127 #1642 := (not #1641)
  1128 #1656 := (or #1642 #1651)
  1129 #1662 := (not #1656)
  1130 #1663 := (or #1569 #815 #724 #1662)
  1131 #1664 := (not #1663)
  1132 #1708 := (or #1664 #1702)
  1133 #1713 := (not #1708)
  1134 #1482 := (forall (vars (?v0 int)) #1477)
  1135 #1676 := (not #1482)
  1136 #1460 := (forall (vars (?v0 int)) #1455)
  1137 #1675 := (not #1460)
  1138 #1716 := (or #528 #1569 #815 #1675 #1676 #1713)
  1139 #1719 := (not #1716)
  1140 #1722 := (or #1437 #1719)
  1141 #2290 := (iff #1722 #2289)
  1142 #2287 := (iff #1719 #2286)
  1143 #2284 := (iff #1716 #2283)
  1144 #2281 := (iff #1713 #2280)
  1145 #2278 := (iff #1708 #2277)
  1146 #2275 := (iff #1702 #2274)
  1147 #2272 := (iff #1699 #2271)
  1148 #2269 := (iff #1696 #2268)
  1149 #2266 := (iff #1693 #2265)
  1150 #2263 := (iff #1507 #2260)
  1151 #2261 := (iff #1504 #1504)
  1152 #2262 := [refl]: #2261
  1153 #2264 := [quant-intro #2262]: #2263
  1154 #2267 := [monotonicity #2264]: #2266
  1155 #2270 := [monotonicity #2267]: #2269
  1156 #2273 := [monotonicity #2270]: #2272
  1157 #2276 := [monotonicity #2273]: #2275
  1158 #2258 := (iff #1664 #2257)
  1159 #2255 := (iff #1663 #2254)
  1160 #2252 := (iff #1662 #2251)
  1161 #2249 := (iff #1656 #2248)
  1162 #2246 := (iff #1651 #2245)
  1163 #2243 := (iff #1650 #2242)
  1164 #2234 := (iff #1640 #2233)
  1165 #2231 := (iff #1632 #2230)
  1166 #2228 := (iff #1604 #2227)
  1167 #2225 := (iff #1603 #2224)
  1168 #2222 := (iff #1602 #2221)
  1169 #2219 := (iff #1596 #2216)
  1170 #2217 := (iff #1591 #1591)
  1171 #2218 := [refl]: #2217
  1172 #2220 := [quant-intro #2218]: #2219
  1173 #2223 := [monotonicity #2220]: #2222
  1174 #2226 := [monotonicity #2223]: #2225
  1175 #2229 := [monotonicity #2226]: #2228
  1176 #2232 := [monotonicity #2229]: #2231
  1177 #2235 := [monotonicity #2232]: #2234
  1178 #2244 := [monotonicity #2235]: #2243
  1179 #2247 := [monotonicity #2244]: #2246
  1180 #2240 := (iff #1642 #2239)
  1181 #2237 := (iff #1641 #2236)
  1182 #2238 := [monotonicity #2235]: #2237
  1183 #2241 := [monotonicity #2238]: #2240
  1184 #2250 := [monotonicity #2241 #2247]: #2249
  1185 #2253 := [monotonicity #2250]: #2252
  1186 #2256 := [monotonicity #2253]: #2255
  1187 #2259 := [monotonicity #2256]: #2258
  1188 #2279 := [monotonicity #2259 #2276]: #2278
  1189 #2282 := [monotonicity #2279]: #2281
  1190 #2214 := (iff #1676 #2213)
  1191 #2211 := (iff #1482 #2208)
  1192 #2209 := (iff #1477 #1477)
  1193 #2210 := [refl]: #2209
  1194 #2212 := [quant-intro #2210]: #2211
  1195 #2215 := [monotonicity #2212]: #2214
  1196 #2206 := (iff #1675 #2205)
  1197 #2203 := (iff #1460 #2200)
  1198 #2201 := (iff #1455 #1455)
  1199 #2202 := [refl]: #2201
  1200 #2204 := [quant-intro #2202]: #2203
  1201 #2207 := [monotonicity #2204]: #2206
  1202 #2285 := [monotonicity #2207 #2215 #2282]: #2284
  1203 #2288 := [monotonicity #2285]: #2287
  1204 #2291 := [monotonicity #2288]: #2290
  1205 #1344 := (and #1160 #1341)
  1206 #1347 := (not #1344)
  1207 #1363 := (or #1347 #1358)
  1208 #1366 := (not #1363)
  1209 #1169 := (not #307)
  1210 #1179 := (and #1169 #785)
  1211 #1372 := (or #1179 #1366)
  1212 #1396 := (and #423 #426 #668 #671 #754 #757 #802 #819 #1372)
  1213 #1384 := (and #280 #285 #288 #668 #671 #754 #757 #802 #818 #1372)
  1214 #1401 := (or #1384 #1396)
  1215 #1407 := (and #668 #671 #727 #1401)
  1216 #1111 := (not #1110)
  1217 #1279 := (and #1111 #1112)
  1218 #1282 := (not #1279)
  1219 #1298 := (or #1282 #1293)
  1220 #1301 := (not #1298)
  1221 #1090 := (not #1089)
  1222 #1270 := (and #1090 #1091)
  1223 #1273 := (not #1270)
  1224 #1276 := (or #1267 #1273)
  1225 #1304 := (and #1276 #1301)
  1226 #1080 := (not #694)
  1227 #1083 := (forall (vars (?v0 int)) #1080)
  1228 #1307 := (or #1083 #1304)
  1229 #1313 := (and #179 #182 #185 #668 #671 #724 #1307)
  1230 #1412 := (or #1313 #1407)
  1231 #1418 := (and #176 #661 #668 #671 #935 #1412)
  1232 #1240 := (and #1048 #1049)
  1233 #1243 := (not #1240)
  1234 #1249 := (or #1007 #1243)
  1235 #1254 := (not #1249)
  1236 #1423 := (or #1254 #1418)
  1237 #1725 := (iff #1423 #1722)
  1238 #1545 := (or #1110 #1530 #1293)
  1239 #1557 := (or #1556 #1545)
  1240 #1558 := (not #1557)
  1241 #1563 := (or #1507 #1558)
  1242 #1570 := (not #1563)
  1243 #1571 := (or #241 #232 #223 #1569 #815 #727 #1570)
  1244 #1572 := (not #1571)
  1245 #1669 := (or #1572 #1664)
  1246 #1677 := (not #1669)
  1247 #1678 := (or #528 #1569 #815 #1675 #1676 #1677)
  1248 #1679 := (not #1678)
  1249 #1684 := (or #1437 #1679)
  1250 #1723 := (iff #1684 #1722)
  1251 #1720 := (iff #1679 #1719)
  1252 #1717 := (iff #1678 #1716)
  1253 #1714 := (iff #1677 #1713)
  1254 #1711 := (iff #1669 #1708)
  1255 #1705 := (or #1702 #1664)
  1256 #1709 := (iff #1705 #1708)
  1257 #1710 := [rewrite]: #1709
  1258 #1706 := (iff #1669 #1705)
  1259 #1703 := (iff #1572 #1702)
  1260 #1700 := (iff #1571 #1699)
  1261 #1697 := (iff #1570 #1696)
  1262 #1694 := (iff #1563 #1693)
  1263 #1691 := (iff #1558 #1690)
  1264 #1688 := (iff #1557 #1687)
  1265 #1689 := [rewrite]: #1688
  1266 #1692 := [monotonicity #1689]: #1691
  1267 #1695 := [monotonicity #1692]: #1694
  1268 #1698 := [monotonicity #1695]: #1697
  1269 #1701 := [monotonicity #1698]: #1700
  1270 #1704 := [monotonicity #1701]: #1703
  1271 #1707 := [monotonicity #1704]: #1706
  1272 #1712 := [trans #1707 #1710]: #1711
  1273 #1715 := [monotonicity #1712]: #1714
  1274 #1718 := [monotonicity #1715]: #1717
  1275 #1721 := [monotonicity #1718]: #1720
  1276 #1724 := [monotonicity #1721]: #1723
  1277 #1685 := (iff #1423 #1684)
  1278 #1682 := (iff #1418 #1679)
  1279 #1672 := (and #176 #1460 #668 #671 #1482 #1669)
  1280 #1680 := (iff #1672 #1679)
  1281 #1681 := [rewrite]: #1680
  1282 #1673 := (iff #1418 #1672)
  1283 #1670 := (iff #1412 #1669)
  1284 #1667 := (iff #1407 #1664)
  1285 #1659 := (and #668 #671 #727 #1656)
  1286 #1665 := (iff #1659 #1664)
  1287 #1666 := [rewrite]: #1665
  1288 #1660 := (iff #1407 #1659)
  1289 #1657 := (iff #1401 #1656)
  1290 #1654 := (iff #1396 #1651)
  1291 #1647 := (and #423 #426 #668 #671 #754 #757 #802 #819 #1632)
  1292 #1652 := (iff #1647 #1651)
  1293 #1653 := [rewrite]: #1652
  1294 #1648 := (iff #1396 #1647)
  1295 #1633 := (iff #1372 #1632)
  1296 #1630 := (iff #1366 #1629)
  1297 #1627 := (iff #1363 #1624)
  1298 #1610 := (or #1609 #1336)
  1299 #1621 := (or #1610 #1358)
  1300 #1625 := (iff #1621 #1624)
  1301 #1626 := [rewrite]: #1625
  1302 #1622 := (iff #1363 #1621)
  1303 #1619 := (iff #1347 #1610)
  1304 #1611 := (not #1610)
  1305 #1614 := (not #1611)
  1306 #1617 := (iff #1614 #1610)
  1307 #1618 := [rewrite]: #1617
  1308 #1615 := (iff #1347 #1614)
  1309 #1612 := (iff #1344 #1611)
  1310 #1613 := [rewrite]: #1612
  1311 #1616 := [monotonicity #1613]: #1615
  1312 #1620 := [trans #1616 #1618]: #1619
  1313 #1623 := [monotonicity #1620]: #1622
  1314 #1628 := [trans #1623 #1626]: #1627
  1315 #1631 := [monotonicity #1628]: #1630
  1316 #1607 := (iff #1179 #1604)
  1317 #1599 := (and #1169 #1596)
  1318 #1605 := (iff #1599 #1604)
  1319 #1606 := [rewrite]: #1605
  1320 #1600 := (iff #1179 #1599)
  1321 #1597 := (iff #785 #1596)
  1322 #1594 := (iff #782 #1591)
  1323 #1577 := (or #1440 #765)
  1324 #1588 := (or #1577 #779)
  1325 #1592 := (iff #1588 #1591)
  1326 #1593 := [rewrite]: #1592
  1327 #1589 := (iff #782 #1588)
  1328 #1586 := (iff #774 #1577)
  1329 #1578 := (not #1577)
  1330 #1581 := (not #1578)
  1331 #1584 := (iff #1581 #1577)
  1332 #1585 := [rewrite]: #1584
  1333 #1582 := (iff #774 #1581)
  1334 #1579 := (iff #771 #1578)
  1335 #1580 := [rewrite]: #1579
  1336 #1583 := [monotonicity #1580]: #1582
  1337 #1587 := [trans #1583 #1585]: #1586
  1338 #1590 := [monotonicity #1587]: #1589
  1339 #1595 := [trans #1590 #1593]: #1594
  1340 #1598 := [quant-intro #1595]: #1597
  1341 #1601 := [monotonicity #1598]: #1600
  1342 #1608 := [trans #1601 #1606]: #1607
  1343 #1634 := [monotonicity #1608 #1631]: #1633
  1344 #1649 := [monotonicity #1634]: #1648
  1345 #1655 := [trans #1649 #1653]: #1654
  1346 #1645 := (iff #1384 #1642)
  1347 #1635 := (and #280 #285 #288 #668 #671 #754 #757 #802 #818 #1632)
  1348 #1643 := (iff #1635 #1642)
  1349 #1644 := [rewrite]: #1643
  1350 #1636 := (iff #1384 #1635)
  1351 #1637 := [monotonicity #1634]: #1636
  1352 #1646 := [trans #1637 #1644]: #1645
  1353 #1658 := [monotonicity #1646 #1655]: #1657
  1354 #1661 := [monotonicity #1658]: #1660
  1355 #1668 := [trans #1661 #1666]: #1667
  1356 #1575 := (iff #1313 #1572)
  1357 #1566 := (and #179 #182 #185 #668 #671 #724 #1563)
  1358 #1573 := (iff #1566 #1572)
  1359 #1574 := [rewrite]: #1573
  1360 #1567 := (iff #1313 #1566)
  1361 #1564 := (iff #1307 #1563)
  1362 #1561 := (iff #1304 #1558)
  1363 #1550 := (not #1545)
  1364 #1553 := (and #1525 #1550)
  1365 #1559 := (iff #1553 #1558)
  1366 #1560 := [rewrite]: #1559
  1367 #1554 := (iff #1304 #1553)
  1368 #1551 := (iff #1301 #1550)
  1369 #1548 := (iff #1298 #1545)
  1370 #1531 := (or #1110 #1530)
  1371 #1542 := (or #1531 #1293)
  1372 #1546 := (iff #1542 #1545)
  1373 #1547 := [rewrite]: #1546
  1374 #1543 := (iff #1298 #1542)
  1375 #1540 := (iff #1282 #1531)
  1376 #1532 := (not #1531)
  1377 #1535 := (not #1532)
  1378 #1538 := (iff #1535 #1531)
  1379 #1539 := [rewrite]: #1538
  1380 #1536 := (iff #1282 #1535)
  1381 #1533 := (iff #1279 #1532)
  1382 #1534 := [rewrite]: #1533
  1383 #1537 := [monotonicity #1534]: #1536
  1384 #1541 := [trans #1537 #1539]: #1540
  1385 #1544 := [monotonicity #1541]: #1543
  1386 #1549 := [trans #1544 #1547]: #1548
  1387 #1552 := [monotonicity #1549]: #1551
  1388 #1528 := (iff #1276 #1525)
  1389 #1511 := (or #1089 #1510)
  1390 #1522 := (or #1267 #1511)
  1391 #1526 := (iff #1522 #1525)
  1392 #1527 := [rewrite]: #1526
  1393 #1523 := (iff #1276 #1522)
  1394 #1520 := (iff #1273 #1511)
  1395 #1512 := (not #1511)
  1396 #1515 := (not #1512)
  1397 #1518 := (iff #1515 #1511)
  1398 #1519 := [rewrite]: #1518
  1399 #1516 := (iff #1273 #1515)
  1400 #1513 := (iff #1270 #1512)
  1401 #1514 := [rewrite]: #1513
  1402 #1517 := [monotonicity #1514]: #1516
  1403 #1521 := [trans #1517 #1519]: #1520
  1404 #1524 := [monotonicity #1521]: #1523
  1405 #1529 := [trans #1524 #1527]: #1528
  1406 #1555 := [monotonicity #1529 #1552]: #1554
  1407 #1562 := [trans #1555 #1560]: #1561
  1408 #1508 := (iff #1083 #1507)
  1409 #1505 := (iff #1080 #1504)
  1410 #1502 := (iff #694 #1499)
  1411 #1485 := (or #1440 #681)
  1412 #1496 := (or #51 #1485)
  1413 #1500 := (iff #1496 #1499)
  1414 #1501 := [rewrite]: #1500
  1415 #1497 := (iff #694 #1496)
  1416 #1494 := (iff #688 #1485)
  1417 #1486 := (not #1485)
  1418 #1489 := (not #1486)
  1419 #1492 := (iff #1489 #1485)
  1420 #1493 := [rewrite]: #1492
  1421 #1490 := (iff #688 #1489)
  1422 #1487 := (iff #685 #1486)
  1423 #1488 := [rewrite]: #1487
  1424 #1491 := [monotonicity #1488]: #1490
  1425 #1495 := [trans #1491 #1493]: #1494
  1426 #1498 := [monotonicity #1495]: #1497
  1427 #1503 := [trans #1498 #1501]: #1502
  1428 #1506 := [monotonicity #1503]: #1505
  1429 #1509 := [quant-intro #1506]: #1508
  1430 #1565 := [monotonicity #1509 #1562]: #1564
  1431 #1568 := [monotonicity #1565]: #1567
  1432 #1576 := [trans #1568 #1574]: #1575
  1433 #1671 := [monotonicity #1576 #1668]: #1670
  1434 #1483 := (iff #935 #1482)
  1435 #1480 := (iff #932 #1477)
  1436 #1463 := (or #1440 #916)
  1437 #1474 := (or #1463 #929)
  1438 #1478 := (iff #1474 #1477)
  1439 #1479 := [rewrite]: #1478
  1440 #1475 := (iff #932 #1474)
  1441 #1472 := (iff #924 #1463)
  1442 #1464 := (not #1463)
  1443 #1467 := (not #1464)
  1444 #1470 := (iff #1467 #1463)
  1445 #1471 := [rewrite]: #1470
  1446 #1468 := (iff #924 #1467)
  1447 #1465 := (iff #921 #1464)
  1448 #1466 := [rewrite]: #1465
  1449 #1469 := [monotonicity #1466]: #1468
  1450 #1473 := [trans #1469 #1471]: #1472
  1451 #1476 := [monotonicity #1473]: #1475
  1452 #1481 := [trans #1476 #1479]: #1480
  1453 #1484 := [quant-intro #1481]: #1483
  1454 #1461 := (iff #661 #1460)
  1455 #1458 := (iff #658 #1455)
  1456 #1441 := (or #1440 #644)
  1457 #1452 := (or #1441 #654)
  1458 #1456 := (iff #1452 #1455)
  1459 #1457 := [rewrite]: #1456
  1460 #1453 := (iff #658 #1452)
  1461 #1450 := (iff #649 #1441)
  1462 #1442 := (not #1441)
  1463 #1445 := (not #1442)
  1464 #1448 := (iff #1445 #1441)
  1465 #1449 := [rewrite]: #1448
  1466 #1446 := (iff #649 #1445)
  1467 #1443 := (iff #646 #1442)
  1468 #1444 := [rewrite]: #1443
  1469 #1447 := [monotonicity #1444]: #1446
  1470 #1451 := [trans #1447 #1449]: #1450
  1471 #1454 := [monotonicity #1451]: #1453
  1472 #1459 := [trans #1454 #1457]: #1458
  1473 #1462 := [quant-intro #1459]: #1461
  1474 #1674 := [monotonicity #1462 #1484 #1671]: #1673
  1475 #1683 := [trans #1674 #1681]: #1682
  1476 #1438 := (iff #1254 #1437)
  1477 #1435 := (iff #1249 #1432)
  1478 #1168 := (or #1005 #1167)
  1479 #1429 := (or #1007 #1168)
  1480 #1433 := (iff #1429 #1432)
  1481 #1434 := [rewrite]: #1433
  1482 #1430 := (iff #1249 #1429)
  1483 #1427 := (iff #1243 #1168)
  1484 #1099 := (not #1168)
  1485 #1057 := (not #1099)
  1486 #1239 := (iff #1057 #1168)
  1487 #1426 := [rewrite]: #1239
  1488 #1120 := (iff #1243 #1057)
  1489 #1100 := (iff #1240 #1099)
  1490 #1056 := [rewrite]: #1100
  1491 #1121 := [monotonicity #1056]: #1120
  1492 #1428 := [trans #1121 #1426]: #1427
  1493 #1431 := [monotonicity #1428]: #1430
  1494 #1436 := [trans #1431 #1434]: #1435
  1495 #1439 := [monotonicity #1436]: #1438
  1496 #1686 := [monotonicity #1439 #1683]: #1685
  1497 #1726 := [trans #1686 #1724]: #1725
  1498 #1190 := (not #812)
  1499 #1187 := (not #806)
  1500 #1155 := (+ #1154 #777)
  1501 #1156 := (<= #1155 0::int)
  1502 #1157 := (+ ?v0!3 #766)
  1503 #1158 := (>= #1157 0::int)
  1504 #1159 := (not #1158)
  1505 #1161 := (and #1160 #1159)
  1506 #1162 := (not #1161)
  1507 #1163 := (or #1162 #1156)
  1508 #1164 := (not #1163)
  1509 #1183 := (or #1164 #1179)
  1510 #1150 := (not #762)
  1511 #1068 := (not #676)
  1512 #1202 := (not #432)
  1513 #1199 := (not #441)
  1514 #1207 := (and #1199 #1202 #1068 #1150 #1183 #1187 #1190 #824)
  1515 #1147 := (not #815)
  1516 #1144 := (not #366)
  1517 #1141 := (not #375)
  1518 #1138 := (not #393)
  1519 #1195 := (and #1138 #1141 #1144 #1147 #1068 #1150 #1183 #1187 #1190 #818)
  1520 #1211 := (or #1195 #1207)
  1521 #1215 := (and #1068 #727 #1211)
  1522 #1106 := (+ #1105 #705)
  1523 #1107 := (<= #1106 0::int)
  1524 #1113 := (and #1112 #1111)
  1525 #1114 := (not #1113)
  1526 #1115 := (or #1114 #1107)
  1527 #1116 := (not #1115)
  1528 #1092 := (and #1091 #1090)
  1529 #1093 := (not #1092)
  1530 #1095 := (= #1094 f10)
  1531 #1096 := (or #1095 #1093)
  1532 #1122 := (and #1096 #1116)
  1533 #1126 := (or #1083 #1122)
  1534 #1077 := (not #223)
  1535 #1074 := (not #232)
  1536 #1071 := (not #241)
  1537 #1132 := (and #1071 #1074 #1077 #1068 #1126 #892)
  1538 #1219 := (or #1132 #1215)
  1539 #1058 := (not #528)
  1540 #1230 := (and #1058 #661 #1068 #1219 #935)
  1541 #1050 := (and #1049 #1048)
  1542 #1051 := (not #1050)
  1543 #1052 := (or #1051 #1007)
  1544 #1053 := (not #1052)
  1545 #1234 := (or #1053 #1230)
  1546 #1424 := (iff #1234 #1423)
  1547 #1421 := (iff #1230 #1418)
  1548 #1415 := (and #176 #661 #673 #1412 #935)
  1549 #1419 := (iff #1415 #1418)
  1550 #1420 := [rewrite]: #1419
  1551 #1416 := (iff #1230 #1415)
  1552 #1413 := (iff #1219 #1412)
  1553 #1410 := (iff #1215 #1407)
  1554 #1404 := (and #673 #727 #1401)
  1555 #1408 := (iff #1404 #1407)
  1556 #1409 := [rewrite]: #1408
  1557 #1405 := (iff #1215 #1404)
  1558 #1402 := (iff #1211 #1401)
  1559 #1399 := (iff #1207 #1396)
  1560 #1393 := (and #423 #426 #673 #759 #1372 #802 #809 #819)
  1561 #1397 := (iff #1393 #1396)
  1562 #1398 := [rewrite]: #1397
  1563 #1394 := (iff #1207 #1393)
  1564 #1379 := (iff #1190 #809)
  1565 #1380 := [rewrite]: #1379
  1566 #1377 := (iff #1187 #802)
  1567 #1378 := [rewrite]: #1377
  1568 #1375 := (iff #1183 #1372)
  1569 #1369 := (or #1366 #1179)
  1570 #1373 := (iff #1369 #1372)
  1571 #1374 := [rewrite]: #1373
  1572 #1370 := (iff #1183 #1369)
  1573 #1367 := (iff #1164 #1366)
  1574 #1364 := (iff #1163 #1363)
  1575 #1361 := (iff #1156 #1358)
  1576 #1350 := (+ #777 #1154)
  1577 #1353 := (<= #1350 0::int)
  1578 #1359 := (iff #1353 #1358)
  1579 #1360 := [rewrite]: #1359
  1580 #1354 := (iff #1156 #1353)
  1581 #1351 := (= #1155 #1350)
  1582 #1352 := [rewrite]: #1351
  1583 #1355 := [monotonicity #1352]: #1354
  1584 #1362 := [trans #1355 #1360]: #1361
  1585 #1348 := (iff #1162 #1347)
  1586 #1345 := (iff #1161 #1344)
  1587 #1342 := (iff #1159 #1341)
  1588 #1339 := (iff #1158 #1336)
  1589 #1328 := (+ #766 ?v0!3)
  1590 #1331 := (>= #1328 0::int)
  1591 #1337 := (iff #1331 #1336)
  1592 #1338 := [rewrite]: #1337
  1593 #1332 := (iff #1158 #1331)
  1594 #1329 := (= #1157 #1328)
  1595 #1330 := [rewrite]: #1329
  1596 #1333 := [monotonicity #1330]: #1332
  1597 #1340 := [trans #1333 #1338]: #1339
  1598 #1343 := [monotonicity #1340]: #1342
  1599 #1346 := [monotonicity #1343]: #1345
  1600 #1349 := [monotonicity #1346]: #1348
  1601 #1365 := [monotonicity #1349 #1362]: #1364
  1602 #1368 := [monotonicity #1365]: #1367
  1603 #1371 := [monotonicity #1368]: #1370
  1604 #1376 := [trans #1371 #1374]: #1375
  1605 #1326 := (iff #1150 #759)
  1606 #1327 := [rewrite]: #1326
  1607 #1259 := (iff #1068 #673)
  1608 #1260 := [rewrite]: #1259
  1609 #1391 := (iff #1202 #426)
  1610 #1392 := [rewrite]: #1391
  1611 #1389 := (iff #1199 #423)
  1612 #1390 := [rewrite]: #1389
  1613 #1395 := [monotonicity #1390 #1392 #1260 #1327 #1376 #1378 #1380 #828]: #1394
  1614 #1400 := [trans #1395 #1398]: #1399
  1615 #1387 := (iff #1195 #1384)
  1616 #1381 := (and #280 #285 #288 #671 #673 #759 #1372 #802 #809 #818)
  1617 #1385 := (iff #1381 #1384)
  1618 #1386 := [rewrite]: #1385
  1619 #1382 := (iff #1195 #1381)
  1620 #1324 := (iff #1147 #671)
  1621 #1325 := [rewrite]: #1324
  1622 #1322 := (iff #1144 #288)
  1623 #1323 := [rewrite]: #1322
  1624 #1320 := (iff #1141 #285)
  1625 #1321 := [rewrite]: #1320
  1626 #1318 := (iff #1138 #280)
  1627 #1319 := [rewrite]: #1318
  1628 #1383 := [monotonicity #1319 #1321 #1323 #1325 #1260 #1327 #1376 #1378 #1380]: #1382
  1629 #1388 := [trans #1383 #1386]: #1387
  1630 #1403 := [monotonicity #1388 #1400]: #1402
  1631 #1406 := [monotonicity #1260 #1403]: #1405
  1632 #1411 := [trans #1406 #1409]: #1410
  1633 #1316 := (iff #1132 #1313)
  1634 #1310 := (and #179 #182 #185 #673 #1307 #724)
  1635 #1314 := (iff #1310 #1313)
  1636 #1315 := [rewrite]: #1314
  1637 #1311 := (iff #1132 #1310)
  1638 #1308 := (iff #1126 #1307)
  1639 #1305 := (iff #1122 #1304)
  1640 #1302 := (iff #1116 #1301)
  1641 #1299 := (iff #1115 #1298)
  1642 #1296 := (iff #1107 #1293)
  1643 #1285 := (+ #705 #1105)
  1644 #1288 := (<= #1285 0::int)
  1645 #1294 := (iff #1288 #1293)
  1646 #1295 := [rewrite]: #1294
  1647 #1289 := (iff #1107 #1288)
  1648 #1286 := (= #1106 #1285)
  1649 #1287 := [rewrite]: #1286
  1650 #1290 := [monotonicity #1287]: #1289
  1651 #1297 := [trans #1290 #1295]: #1296
  1652 #1283 := (iff #1114 #1282)
  1653 #1280 := (iff #1113 #1279)
  1654 #1281 := [rewrite]: #1280
  1655 #1284 := [monotonicity #1281]: #1283
  1656 #1300 := [monotonicity #1284 #1297]: #1299
  1657 #1303 := [monotonicity #1300]: #1302
  1658 #1277 := (iff #1096 #1276)
  1659 #1274 := (iff #1093 #1273)
  1660 #1271 := (iff #1092 #1270)
  1661 #1272 := [rewrite]: #1271
  1662 #1275 := [monotonicity #1272]: #1274
  1663 #1268 := (iff #1095 #1267)
  1664 #1269 := [rewrite]: #1268
  1665 #1278 := [monotonicity #1269 #1275]: #1277
  1666 #1306 := [monotonicity #1278 #1303]: #1305
  1667 #1309 := [monotonicity #1306]: #1308
  1668 #1265 := (iff #1077 #185)
  1669 #1266 := [rewrite]: #1265
  1670 #1263 := (iff #1074 #182)
  1671 #1264 := [rewrite]: #1263
  1672 #1261 := (iff #1071 #179)
  1673 #1262 := [rewrite]: #1261
  1674 #1312 := [monotonicity #1262 #1264 #1266 #1260 #1309 #896]: #1311
  1675 #1317 := [trans #1312 #1315]: #1316
  1676 #1414 := [monotonicity #1317 #1411]: #1413
  1677 #1257 := (iff #1058 #176)
  1678 #1258 := [rewrite]: #1257
  1679 #1417 := [monotonicity #1258 #1260 #1414]: #1416
  1680 #1422 := [trans #1417 #1420]: #1421
  1681 #1255 := (iff #1053 #1254)
  1682 #1252 := (iff #1052 #1249)
  1683 #1246 := (or #1243 #1007)
  1684 #1250 := (iff #1246 #1249)
  1685 #1251 := [rewrite]: #1250
  1686 #1247 := (iff #1052 #1246)
  1687 #1244 := (iff #1051 #1243)
  1688 #1241 := (iff #1050 #1240)
  1689 #1242 := [rewrite]: #1241
  1690 #1245 := [monotonicity #1242]: #1244
  1691 #1248 := [monotonicity #1245]: #1247
  1692 #1253 := [trans #1248 #1251]: #1252
  1693 #1256 := [monotonicity #1253]: #1255
  1694 #1425 := [monotonicity #1256 #1422]: #1424
  1695 #1032 := (or #528 #664 #676 #913 #938)
  1696 #1037 := (and #661 #1032)
  1697 #1040 := (not #1037)
  1698 #1235 := (~ #1040 #1234)
  1699 #1231 := (not #1032)
  1700 #1232 := (~ #1231 #1230)
  1701 #1227 := (not #938)
  1702 #1228 := (~ #1227 #935)
  1703 #1225 := (~ #935 #935)
  1704 #1223 := (~ #932 #932)
  1705 #1224 := [refl]: #1223
  1706 #1226 := [nnf-pos #1224]: #1225
  1707 #1229 := [nnf-neg #1226]: #1228
  1708 #1220 := (not #913)
  1709 #1221 := (~ #1220 #1219)
  1710 #1216 := (not #908)
  1711 #1217 := (~ #1216 #1215)
  1712 #1212 := (not #887)
  1713 #1213 := (~ #1212 #1211)
  1714 #1208 := (not #882)
  1715 #1209 := (~ #1208 #1207)
  1716 #1205 := (~ #824 #824)
  1717 #1206 := [refl]: #1205
  1718 #1191 := (~ #1190 #1190)
  1719 #1192 := [refl]: #1191
  1720 #1188 := (~ #1187 #1187)
  1721 #1189 := [refl]: #1188
  1722 #1184 := (not #799)
  1723 #1185 := (~ #1184 #1183)
  1724 #1180 := (not #794)
  1725 #1181 := (~ #1180 #1179)
  1726 #1176 := (not #788)
  1727 #1177 := (~ #1176 #785)
  1728 #1174 := (~ #785 #785)
  1729 #1172 := (~ #782 #782)
  1730 #1173 := [refl]: #1172
  1731 #1175 := [nnf-pos #1173]: #1174
  1732 #1178 := [nnf-neg #1175]: #1177
  1733 #1170 := (~ #1169 #1169)
  1734 #1171 := [refl]: #1170
  1735 #1182 := [nnf-neg #1171 #1178]: #1181
  1736 #1165 := (~ #788 #1164)
  1737 #1166 := [sk]: #1165
  1738 #1186 := [nnf-neg #1166 #1182]: #1185
  1739 #1151 := (~ #1150 #1150)
  1740 #1152 := [refl]: #1151
  1741 #1069 := (~ #1068 #1068)
  1742 #1070 := [refl]: #1069
  1743 #1203 := (~ #1202 #1202)
  1744 #1204 := [refl]: #1203
  1745 #1200 := (~ #1199 #1199)
  1746 #1201 := [refl]: #1200
  1747 #1210 := [nnf-neg #1201 #1204 #1070 #1152 #1186 #1189 #1192 #1206]: #1209
  1748 #1196 := (not #858)
  1749 #1197 := (~ #1196 #1195)
  1750 #1193 := (~ #818 #818)
  1751 #1194 := [refl]: #1193
  1752 #1148 := (~ #1147 #1147)
  1753 #1149 := [refl]: #1148
  1754 #1145 := (~ #1144 #1144)
  1755 #1146 := [refl]: #1145
  1756 #1142 := (~ #1141 #1141)
  1757 #1143 := [refl]: #1142
  1758 #1139 := (~ #1138 #1138)
  1759 #1140 := [refl]: #1139
  1760 #1198 := [nnf-neg #1140 #1143 #1146 #1149 #1070 #1152 #1186 #1189 #1192 #1194]: #1197
  1761 #1214 := [nnf-neg #1198 #1210]: #1213
  1762 #1136 := (~ #727 #727)
  1763 #1137 := [refl]: #1136
  1764 #1218 := [nnf-neg #1070 #1137 #1214]: #1217
  1765 #1133 := (not #748)
  1766 #1134 := (~ #1133 #1132)
  1767 #1130 := (~ #892 #892)
  1768 #1131 := [refl]: #1130
  1769 #1127 := (not #719)
  1770 #1128 := (~ #1127 #1126)
  1771 #1123 := (not #716)
  1772 #1124 := (~ #1123 #1122)
  1773 #1117 := (not #713)
  1774 #1118 := (~ #1117 #1116)
  1775 #1119 := [sk]: #1118
  1776 #1101 := (not #702)
  1777 #1102 := (~ #1101 #1096)
  1778 #1097 := (~ #699 #1096)
  1779 #1098 := [sk]: #1097
  1780 #1103 := [nnf-neg #1098]: #1102
  1781 #1125 := [nnf-neg #1103 #1119]: #1124
  1782 #1084 := (~ #702 #1083)
  1783 #1081 := (~ #1080 #1080)
  1784 #1082 := [refl]: #1081
  1785 #1085 := [nnf-neg #1082]: #1084
  1786 #1129 := [nnf-neg #1085 #1125]: #1128
  1787 #1078 := (~ #1077 #1077)
  1788 #1079 := [refl]: #1078
  1789 #1075 := (~ #1074 #1074)
  1790 #1076 := [refl]: #1075
  1791 #1072 := (~ #1071 #1071)
  1792 #1073 := [refl]: #1072
  1793 #1135 := [nnf-neg #1073 #1076 #1079 #1070 #1129 #1131]: #1134
  1794 #1222 := [nnf-neg #1135 #1218]: #1221
  1795 #1065 := (not #664)
  1796 #1066 := (~ #1065 #661)
  1797 #1063 := (~ #661 #661)
  1798 #1061 := (~ #658 #658)
  1799 #1062 := [refl]: #1061
  1800 #1064 := [nnf-pos #1062]: #1063
  1801 #1067 := [nnf-neg #1064]: #1066
  1802 #1059 := (~ #1058 #1058)
  1803 #1060 := [refl]: #1059
  1804 #1233 := [nnf-neg #1060 #1067 #1070 #1222 #1229]: #1232
  1805 #1054 := (~ #664 #1053)
  1806 #1055 := [sk]: #1054
  1807 #1236 := [nnf-neg #1055 #1233]: #1235
  1808 #1002 := (not #967)
  1809 #1041 := (iff #1002 #1040)
  1810 #1038 := (iff #967 #1037)
  1811 #1035 := (iff #964 #1032)
  1812 #1017 := (or #528 #676 #913 #938)
  1813 #1029 := (or #664 #1017)
  1814 #1033 := (iff #1029 #1032)
  1815 #1034 := [rewrite]: #1033
  1816 #1030 := (iff #964 #1029)
  1817 #1027 := (iff #961 #1017)
  1818 #1022 := (and true #1017)
  1819 #1025 := (iff #1022 #1017)
  1820 #1026 := [rewrite]: #1025
  1821 #1023 := (iff #961 #1022)
  1822 #1020 := (iff #956 #1017)
  1823 #1014 := (or false #528 #676 #913 #938)
  1824 #1018 := (iff #1014 #1017)
  1825 #1019 := [rewrite]: #1018
  1826 #1015 := (iff #956 #1014)
  1827 #1012 := (iff #561 false)
  1828 #1010 := (iff #561 #632)
  1829 #1008 := (iff #13 true)
  1830 #1009 := [iff-true #1001]: #1008
  1831 #1011 := [monotonicity #1009]: #1010
  1832 #1013 := [trans #1011 #636]: #1012
  1833 #1016 := [monotonicity #1013]: #1015
  1834 #1021 := [trans #1016 #1019]: #1020
  1835 #1024 := [monotonicity #1009 #1021]: #1023
  1836 #1028 := [trans #1024 #1026]: #1027
  1837 #1031 := [monotonicity #1028]: #1030
  1838 #1036 := [trans #1031 #1034]: #1035
  1839 #1039 := [monotonicity #1036]: #1038
  1840 #1042 := [monotonicity #1039]: #1041
  1841 #1003 := [not-or-elim #1000]: #1002
  1842 #1043 := [mp #1003 #1042]: #1040
  1843 #1237 := [mp~ #1043 #1236]: #1234
  1844 #1238 := [mp #1237 #1425]: #1423
  1845 #1727 := [mp #1238 #1726]: #1722
  1846 #2292 := [mp #1727 #2291]: #2289
  1847 #2556 := [unit-resolution #2292 #2016]: #2286
  1848 #2111 := (or #2283 #2208)
  1849 #2097 := [def-axiom]: #2111
  1850 #2557 := [unit-resolution #2097 #2556]: #2208
  1851 #2120 := (or #2283 #176)
  1852 #2104 := [def-axiom]: #2120
  1853 #2620 := [unit-resolution #2104 #2556]: #176
  1854 #2352 := (or #2271 #528 #2213)
  1855 #1791 := (f5 f9)
  1856 #2296 := (= f10 #1791)
  1857 #2346 := (= #40 #1791)
  1858 #2344 := (= #1791 #40)
  1859 #2329 := [hypothesis]: #2274
  1860 #2037 := (or #2271 #179)
  1861 #2038 := [def-axiom]: #2037
  1862 #2340 := [unit-resolution #2038 #2329]: #179
  1863 #2341 := [symm #2340]: #44
  1864 #2345 := [monotonicity #2341]: #2344
  1865 #2347 := [symm #2345]: #2346
  1866 #2348 := (= f10 #40)
  1867 #2342 := [hypothesis]: #176
  1868 #2039 := (or #2271 #182)
  1869 #2040 := [def-axiom]: #2039
  1870 #2331 := [unit-resolution #2040 #2329]: #182
  1871 #2343 := [symm #2331]: #46
  1872 #2349 := [trans #2343 #2342]: #2348
  1873 #2350 := [trans #2349 #2347]: #2296
  1874 #2324 := (not #2296)
  1875 #1790 := (>= f9 0::int)
  1876 #1788 := (not #1790)
  1877 #1800 := (* -1::int f9)
  1878 #1787 := (+ f3 #1800)
  1879 #1789 := (<= #1787 0::int)
  1880 #2302 := (or #1789 #1788 #2296)
  1881 #2307 := (not #2302)
  1882 #2124 := (or #2271 #2265)
  1883 #2125 := [def-axiom]: #2124
  1884 #2330 := [unit-resolution #2125 #2329]: #2265
  1885 #1958 := (+ f8 #705)
  1886 #1959 := (<= #1958 0::int)
  1887 #2332 := (or #232 #1959)
  1888 #2333 := [th-lemma]: #2332
  1889 #2334 := [unit-resolution #2333 #2331]: #1959
  1890 #1836 := [hypothesis]: #2208
  1891 #2112 := (or #2271 #724)
  1892 #2114 := [def-axiom]: #2112
  1893 #2335 := [unit-resolution #2114 #2329]: #724
  1894 #1867 := (not #1959)
  1895 #1846 := (or #1687 #727 #2213 #1867)
  1896 #1869 := [hypothesis]: #724
  1897 #1948 := (+ f7 #1108)
  1898 #1949 := (<= #1948 0::int)
  1899 #1927 := (+ f8 #1291)
  1900 #1928 := (>= #1927 0::int)
  1901 #1866 := (not #1928)
  1902 #1860 := [hypothesis]: #1959
  1903 #2023 := (not #1293)
  1904 #1852 := [hypothesis]: #1690
  1905 #2024 := (or #1687 #2023)
  1906 #1983 := [def-axiom]: #2024
  1907 #1854 := [unit-resolution #1983 #1852]: #2023
  1908 #1868 := (or #1866 #1293 #1867)
  1909 #1851 := [hypothesis]: #2023
  1910 #1864 := [hypothesis]: #1928
  1911 #1865 := [th-lemma #1864 #1851 #1860]: false
  1912 #1858 := [lemma #1865]: #1868
  1913 #1855 := [unit-resolution #1858 #1854 #1860]: #1866
  1914 #1841 := (or #1928 #1949)
  1915 #2140 := (or #1687 #1112)
  1916 #2022 := [def-axiom]: #2140
  1917 #1834 := [unit-resolution #2022 #1852]: #1112
  1918 #1917 := (or #2213 #1530 #1928 #1949)
  1919 #1960 := (+ #1105 #927)
  1920 #1950 := (<= #1960 0::int)
  1921 #1940 := (+ ?v0!2 #722)
  1922 #1942 := (>= #1940 0::int)
  1923 #1943 := (or #1530 #1942 #1950)
  1924 #1918 := (or #2213 #1943)
  1925 #1909 := (iff #1918 #1917)
  1926 #1911 := (or #1530 #1928 #1949)
  1927 #1912 := (or #2213 #1911)
  1928 #1906 := (iff #1912 #1917)
  1929 #1907 := [rewrite]: #1906
  1930 #1920 := (iff #1918 #1912)
  1931 #1915 := (iff #1943 #1911)
  1932 #1933 := (or #1530 #1949 #1928)
  1933 #1913 := (iff #1933 #1911)
  1934 #1914 := [rewrite]: #1913
  1935 #1922 := (iff #1943 #1933)
  1936 #1931 := (iff #1950 #1928)
  1937 #1939 := (+ #927 #1105)
  1938 #1924 := (<= #1939 0::int)
  1939 #1929 := (iff #1924 #1928)
  1940 #1930 := [rewrite]: #1929
  1941 #1925 := (iff #1950 #1924)
  1942 #1921 := (= #1960 #1939)
  1943 #1923 := [rewrite]: #1921
  1944 #1926 := [monotonicity #1923]: #1925
  1945 #1932 := [trans #1926 #1930]: #1931
  1946 #1938 := (iff #1942 #1949)
  1947 #1946 := (+ #722 ?v0!2)
  1948 #1944 := (>= #1946 0::int)
  1949 #1935 := (iff #1944 #1949)
  1950 #1937 := [rewrite]: #1935
  1951 #1952 := (iff #1942 #1944)
  1952 #1947 := (= #1940 #1946)
  1953 #1951 := [rewrite]: #1947
  1954 #1945 := [monotonicity #1951]: #1952
  1955 #1936 := [trans #1945 #1937]: #1938
  1956 #1934 := [monotonicity #1936 #1932]: #1922
  1957 #1916 := [trans #1934 #1914]: #1915
  1958 #1905 := [monotonicity #1916]: #1920
  1959 #1908 := [trans #1905 #1907]: #1909
  1960 #1919 := [quant-inst]: #1918
  1961 #1910 := [mp #1919 #1908]: #1917
  1962 #1842 := [unit-resolution #1910 #1836 #1834]: #1841
  1963 #1843 := [unit-resolution #1842 #1855]: #1949
  1964 #2139 := (or #1687 #1111)
  1965 #2137 := [def-axiom]: #2139
  1966 #1844 := [unit-resolution #2137 #1852]: #1111
  1967 #1845 := [th-lemma #1844 #1843 #1869]: false
  1968 #1835 := [lemma #1845]: #1846
  1969 #2336 := [unit-resolution #1835 #2335 #1836 #2334]: #1687
  1970 #2028 := (or #2268 #2260 #1690)
  1971 #2036 := [def-axiom]: #2028
  1972 #2337 := [unit-resolution #2036 #2336 #2330]: #2260
  1973 #2132 := (not #2260)
  1974 #2310 := (or #2132 #2307)
  1975 #2293 := (= #1791 f10)
  1976 #2294 := (or #2293 #1788 #1789)
  1977 #2295 := (not #2294)
  1978 #2311 := (or #2132 #2295)
  1979 #2313 := (iff #2311 #2310)
  1980 #2315 := (iff #2310 #2310)
  1981 #2316 := [rewrite]: #2315
  1982 #2308 := (iff #2295 #2307)
  1983 #2305 := (iff #2294 #2302)
  1984 #2299 := (or #2296 #1788 #1789)
  1985 #2303 := (iff #2299 #2302)
  1986 #2304 := [rewrite]: #2303
  1987 #2300 := (iff #2294 #2299)
  1988 #2297 := (iff #2293 #2296)
  1989 #2298 := [rewrite]: #2297
  1990 #2301 := [monotonicity #2298]: #2300
  1991 #2306 := [trans #2301 #2304]: #2305
  1992 #2309 := [monotonicity #2306]: #2308
  1993 #2314 := [monotonicity #2309]: #2313
  1994 #2317 := [trans #2314 #2316]: #2313
  1995 #2312 := [quant-inst]: #2311
  1996 #2318 := [mp #2312 #2317]: #2310
  1997 #2338 := [unit-resolution #2318 #2337]: #2307
  1998 #2325 := (or #2302 #2324)
  1999 #2326 := [def-axiom]: #2325
  2000 #2339 := [unit-resolution #2326 #2338]: #2324
  2001 #2351 := [unit-resolution #2339 #2350]: false
  2002 #2353 := [lemma #2351]: #2352
  2003 #2621 := [unit-resolution #2353 #2620 #2557]: #2271
  2004 #2098 := (or #2283 #2277)
  2005 #2100 := [def-axiom]: #2098
  2006 #2622 := [unit-resolution #2100 #2556]: #2277
  2007 #2119 := (or #2280 #2257 #2274)
  2008 #2113 := [def-axiom]: #2119
  2009 #2623 := [unit-resolution #2113 #2622 #2621]: #2257
  2010 #2147 := (or #2254 #2248)
  2011 #2141 := [def-axiom]: #2147
  2012 #2624 := [unit-resolution #2141 #2623]: #2248
  2013 #1793 := [hypothesis]: #2239
  2014 #2183 := (or #2236 #2230)
  2015 #2186 := [def-axiom]: #2183
  2016 #2528 := [unit-resolution #2186 #1793]: #2230
  2017 #2319 := (or #2236 #307)
  2018 #1818 := (= #68 #90)
  2019 #1795 := (= #90 #68)
  2020 #1838 := (or #2236 #285)
  2021 #1839 := [def-axiom]: #1838
  2022 #1798 := [unit-resolution #1839 #1793]: #285
  2023 #1799 := [symm #1798]: #74
  2024 #1817 := [monotonicity #1799]: #1795
  2025 #1801 := [symm #1817]: #1818
  2026 #1804 := (= f14 #68)
  2027 #2174 := (or #2236 #280)
  2028 #1837 := [def-axiom]: #2174
  2029 #1797 := [unit-resolution #1837 #1793]: #280
  2030 #1815 := [symm #1797]: #71
  2031 #1840 := (or #2236 #288)
  2032 #2176 := [def-axiom]: #1840
  2033 #1794 := [unit-resolution #2176 #1793]: #288
  2034 #1813 := [symm #1794]: #76
  2035 #1805 := [trans #1813 #1815]: #1804
  2036 #1808 := [trans #1805 #1801]: #307
  2037 #1796 := [hypothesis]: #1169
  2038 #1809 := [unit-resolution #1796 #1808]: false
  2039 #2320 := [lemma #1809]: #2319
  2040 #2529 := [unit-resolution #2320 #1793]: #307
  2041 #1856 := (or #2224 #1169)
  2042 #2191 := [def-axiom]: #1856
  2043 #2530 := [unit-resolution #2191 #2529]: #2224
  2044 #2190 := (or #2233 #2227 #1629)
  2045 #1833 := [def-axiom]: #2190
  2046 #2531 := [unit-resolution #1833 #2530 #2528]: #1629
  2047 #2194 := (or #1624 #1341)
  2048 #2195 := [def-axiom]: #2194
  2049 #2532 := [unit-resolution #2195 #2531]: #1341
  2050 #1877 := (>= #803 -1::int)
  2051 #2184 := (or #2236 #802)
  2052 #1824 := [def-axiom]: #2184
  2053 #2533 := [unit-resolution #1824 #1793]: #802
  2054 #2534 := (or #806 #1877)
  2055 #2535 := [th-lemma]: #2534
  2056 #2536 := [unit-resolution #2535 #2533]: #1877
  2057 #2562 := (not #2496)
  2058 #2525 := (not #2494)
  2059 #2495 := (= #90 #1154)
  2060 #2499 := (not #2495)
  2061 #2502 := (+ #90 #1356)
  2062 #2504 := (>= #2502 0::int)
  2063 #2509 := (not #2504)
  2064 #2196 := (not #1358)
  2065 #2197 := (or #1624 #2196)
  2066 #2192 := [def-axiom]: #2197
  2067 #2537 := [unit-resolution #2192 #2531]: #2196
  2068 #2451 := (* -1::int #90)
  2069 #2490 := (+ f14 #2451)
  2070 #2492 := (>= #2490 0::int)
  2071 #2538 := (or #1169 #2492)
  2072 #2539 := [th-lemma]: #2538
  2073 #2540 := [unit-resolution #2539 #2529]: #2492
  2074 #2510 := (not #2492)
  2075 #2511 := (or #2509 #2510 #1358)
  2076 #2505 := [hypothesis]: #2504
  2077 #2506 := [hypothesis]: #2196
  2078 #2507 := [hypothesis]: #2492
  2079 #2508 := [th-lemma #2507 #2506 #2505]: false
  2080 #2512 := [lemma #2508]: #2511
  2081 #2541 := [unit-resolution #2512 #2540 #2537]: #2509
  2082 #2500 := (or #2499 #2504)
  2083 #2501 := [th-lemma]: #2500
  2084 #2542 := [unit-resolution #2501 #2541]: #2499
  2085 #2526 := (or #2525 #2495 #375)
  2086 #2521 := (= #1154 #90)
  2087 #2519 := (= ?v0!3 f13)
  2088 #2515 := [hypothesis]: #285
  2089 #2517 := (= ?v0!3 f7)
  2090 #2516 := [hypothesis]: #2494
  2091 #2518 := [symm #2516]: #2517
  2092 #2520 := [trans #2518 #2515]: #2519
  2093 #2522 := [monotonicity #2520]: #2521
  2094 #2523 := [symm #2522]: #2495
  2095 #2514 := [hypothesis]: #2499
  2096 #2524 := [unit-resolution #2514 #2523]: false
  2097 #2527 := [lemma #2524]: #2526
  2098 #2543 := [unit-resolution #2527 #2542 #1798]: #2525
  2099 #2565 := (or #2494 #2562)
  2100 #2381 := (<= #2380 0::int)
  2101 #2392 := (+ f8 #1356)
  2102 #2393 := (>= #2392 0::int)
  2103 #2550 := (not #2393)
  2104 #1825 := (or #2236 #818)
  2105 #2185 := [def-axiom]: #1825
  2106 #2544 := [unit-resolution #2185 #1793]: #818
  2107 #2366 := (+ #68 #777)
  2108 #2367 := (<= #2366 0::int)
  2109 #2365 := (= #68 f14)
  2110 #2545 := [trans #1797 #1794]: #2365
  2111 #2546 := (not #2365)
  2112 #2547 := (or #2546 #2367)
  2113 #2548 := [th-lemma]: #2547
  2114 #2549 := [unit-resolution #2548 #2545]: #2367
  2115 #2551 := (not #2367)
  2116 #2552 := (or #2550 #1358 #2551 #819)
  2117 #2553 := [th-lemma]: #2552
  2118 #2554 := [unit-resolution #2553 #2537 #2549 #2544]: #2550
  2119 #2558 := (or #2381 #2393)
  2120 #1861 := (or #1624 #1160)
  2121 #1862 := [def-axiom]: #1861
  2122 #2555 := [unit-resolution #1862 #2531]: #1160
  2123 #2401 := (or #2213 #1609 #2381 #2393)
  2124 #2369 := (+ #1154 #927)
  2125 #2370 := (<= #2369 0::int)
  2126 #2371 := (+ ?v0!3 #722)
  2127 #2372 := (>= #2371 0::int)
  2128 #2373 := (or #1609 #2372 #2370)
  2129 #2402 := (or #2213 #2373)
  2130 #2409 := (iff #2402 #2401)
  2131 #2398 := (or #1609 #2381 #2393)
  2132 #2404 := (or #2213 #2398)
  2133 #2407 := (iff #2404 #2401)
  2134 #2408 := [rewrite]: #2407
  2135 #2405 := (iff #2402 #2404)
  2136 #2399 := (iff #2373 #2398)
  2137 #2396 := (iff #2370 #2393)
  2138 #2386 := (+ #927 #1154)
  2139 #2389 := (<= #2386 0::int)
  2140 #2394 := (iff #2389 #2393)
  2141 #2395 := [rewrite]: #2394
  2142 #2390 := (iff #2370 #2389)
  2143 #2387 := (= #2369 #2386)
  2144 #2388 := [rewrite]: #2387
  2145 #2391 := [monotonicity #2388]: #2390
  2146 #2397 := [trans #2391 #2395]: #2396
  2147 #2384 := (iff #2372 #2381)
  2148 #2374 := (+ #722 ?v0!3)
  2149 #2377 := (>= #2374 0::int)
  2150 #2382 := (iff #2377 #2381)
  2151 #2383 := [rewrite]: #2382
  2152 #2378 := (iff #2372 #2377)
  2153 #2375 := (= #2371 #2374)
  2154 #2376 := [rewrite]: #2375
  2155 #2379 := [monotonicity #2376]: #2378
  2156 #2385 := [trans #2379 #2383]: #2384
  2157 #2400 := [monotonicity #2385 #2397]: #2399
  2158 #2406 := [monotonicity #2400]: #2405
  2159 #2410 := [trans #2406 #2408]: #2409
  2160 #2403 := [quant-inst]: #2402
  2161 #2411 := [mp #2403 #2410]: #2401
  2162 #2559 := [unit-resolution #2411 #2557 #2555]: #2558
  2163 #2560 := [unit-resolution #2559 #2554]: #2381
  2164 #2561 := (not #2381)
  2165 #2563 := (or #2494 #2561 #2562)
  2166 #2564 := [th-lemma]: #2563
  2167 #2566 := [unit-resolution #2564 #2560]: #2565
  2168 #2567 := [unit-resolution #2566 #2543]: #2562
  2169 #2568 := [th-lemma #2567 #2536 #2532]: false
  2170 #2569 := [lemma #2568]: #2236
  2171 #2153 := (or #2251 #2239 #2245)
  2172 #2159 := [def-axiom]: #2153
  2173 #2625 := [unit-resolution #2159 #2569 #2624]: #2245
  2174 #2165 := (or #2242 #2230)
  2175 #2154 := [def-axiom]: #2165
  2176 #2626 := [unit-resolution #2154 #2625]: #2230
  2177 #2421 := (= #40 #90)
  2178 #2631 := (= #90 #40)
  2179 #1891 := (or #2242 #423)
  2180 #1892 := [def-axiom]: #1891
  2181 #2627 := [unit-resolution #1892 #2625]: #423
  2182 #2628 := [symm #2627]: #107
  2183 #2632 := [monotonicity #2628]: #2631
  2184 #2633 := [symm #2632]: #2421
  2185 #2634 := (= f14 #40)
  2186 #2166 := (or #2242 #426)
  2187 #2170 := [def-axiom]: #2166
  2188 #2629 := [unit-resolution #2170 #2625]: #426
  2189 #2630 := [symm #2629]: #108
  2190 #2635 := [trans #2630 #2620]: #2634
  2191 #2636 := [trans #2635 #2633]: #307
  2192 #2637 := [unit-resolution #2191 #2636]: #2224
  2193 #2638 := [unit-resolution #1833 #2637 #2626]: #1629
  2194 #2639 := [unit-resolution #2195 #2638]: #1341
  2195 #1878 := (or #2242 #802)
  2196 #2160 := [def-axiom]: #1878
  2197 #2640 := [unit-resolution #2160 #2625]: #802
  2198 #2641 := [unit-resolution #2535 #2640]: #1877
  2199 #2642 := [hypothesis]: #2562
  2200 #2643 := [th-lemma #2642 #2641 #2639]: false
  2201 #2644 := [lemma #2643]: #2496
  2202 #2649 := [unit-resolution #2192 #2638]: #2196
  2203 #1792 := (+ f8 #777)
  2204 #2168 := (<= #1792 0::int)
  2205 #2650 := (or #432 #2168)
  2206 #2651 := [th-lemma]: #2650
  2207 #2652 := [unit-resolution #2651 #2629]: #2168
  2208 #2653 := (not #2168)
  2209 #2654 := (or #2550 #1358 #2653)
  2210 #2655 := [th-lemma]: #2654
  2211 #2656 := [unit-resolution #2655 #2652 #2649]: #2550
  2212 #2657 := [unit-resolution #1862 #2638]: #1160
  2213 #2658 := [unit-resolution #2411 #2557 #2657 #2656]: #2381
  2214 #2659 := [unit-resolution #2564 #2658]: #2565
  2215 #2660 := [unit-resolution #2659 #2644]: #2494
  2216 #2661 := [monotonicity #2660]: #2645
  2217 #2662 := (not #2645)
  2218 #2663 := (or #2662 #2648)
  2219 #2664 := [th-lemma]: #2663
  2220 #2665 := [unit-resolution #2664 #2661]: #2648
  2221 #2164 := (or #2242 #819)
  2222 #2161 := [def-axiom]: #2164
  2223 #2666 := [unit-resolution #2161 #2625]: #819
  2224 [th-lemma #2666 #2649 #2652 #2665]: false
  2225 unsat