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