--- a/src/HOL/SMT_Examples/SMT_Examples.certs Wed Oct 31 11:23:21 2012 +0100
+++ b/src/HOL/SMT_Examples/SMT_Examples.certs Thu Nov 01 11:34:00 2012 +0100
@@ -1,13 +1,14 @@
-8c0dd63633148cae631c41716f59fedf31aaf85f 8 0
+23fa46bae38100075457f16458b7f980b6e9eaaa 8 0
+unsat
#2 := false
#1 := true
#7 := (not true)
-#29 := (iff #7 false)
-#30 := [rewrite]: #29
-#28 := [asserted]: #7
-[mp #28 #30]: false
+#13 := (iff #7 false)
+#14 := [rewrite]: #13
+#9 := [asserted]: #7
+[mp #9 #14]: false
+a659f050ece3306f2b1d4dcfecadbe7f96ac25b7 14 0
unsat
-4e759d02d4de42cc8b917c1ee399e500780bf8d9 22 0
#2 := false
decl f1 :: S1
#3 := f1
@@ -17,20 +18,12 @@
#9 := (not #8)
#10 := (or #8 #9)
#11 := (not #10)
-#40 := (iff #11 false)
-#1 := true
-#35 := (not true)
-#38 := (iff #35 false)
-#39 := [rewrite]: #38
-#36 := (iff #11 #35)
-#33 := (iff #10 true)
-#34 := [rewrite]: #33
-#37 := [monotonicity #34]: #36
-#41 := [trans #37 #39]: #40
-#32 := [asserted]: #11
-[mp #32 #41]: false
+#13 := [asserted]: #11
+#15 := [not-or-elim #13]: #8
+#14 := [not-or-elim #13]: #9
+[unit-resolution #14 #15]: false
+a67531da310682d5a288c23ac8f30257442b6eee 28 0
unsat
-964f9fc947278fe63d579d7e942d63db70d69508 28 0
#2 := false
decl f1 :: S1
#3 := f1
@@ -41,101 +34,141 @@
#9 := (and #8 true)
#10 := (iff #9 #8)
#11 := (not #10)
-#46 := (iff #11 false)
-#41 := (not true)
-#44 := (iff #41 false)
-#45 := [rewrite]: #44
-#42 := (iff #11 #41)
-#39 := (iff #10 true)
-#34 := (iff #8 #8)
-#37 := (iff #34 true)
-#38 := [rewrite]: #37
-#35 := (iff #10 #34)
-#33 := [rewrite]: #10
-#36 := [monotonicity #33]: #35
-#40 := [trans #36 #38]: #39
-#43 := [monotonicity #40]: #42
-#47 := [trans #43 #45]: #46
-#32 := [asserted]: #11
-[mp #32 #47]: false
+#30 := (iff #11 false)
+#25 := (not true)
+#28 := (iff #25 false)
+#29 := [rewrite]: #28
+#26 := (iff #11 #25)
+#23 := (iff #10 true)
+#18 := (iff #8 #8)
+#21 := (iff #18 true)
+#22 := [rewrite]: #21
+#19 := (iff #10 #18)
+#17 := [rewrite]: #10
+#20 := [monotonicity #17]: #19
+#24 := [trans #20 #22]: #23
+#27 := [monotonicity #24]: #26
+#31 := [trans #27 #29]: #30
+#13 := [asserted]: #11
+[mp #13 #31]: false
+d4525927e0ca94e2a8cd999f8854bd810a0a45a9 30 0
unsat
-6f5c195ed8186ea009f805e2f8ea8ad3b1ee6432 41 0
#2 := false
decl f1 :: S1
#3 := f1
-decl f4 :: S1
-#9 := f4
-#10 := (= f4 f1)
decl f3 :: S1
#7 := f3
#8 := (= f3 f1)
+#12 := (not #8)
+decl f4 :: S1
+#9 := f4
+#10 := (= f4 f1)
#11 := (or #8 #10)
-#64 := (iff #11 false)
-#59 := (or false false)
-#62 := (iff #59 false)
-#63 := [rewrite]: #62
-#60 := (iff #11 #59)
-#57 := (iff #10 false)
-#48 := (not #10)
-#12 := (not #8)
#13 := (and #11 #12)
-#37 := (not #13)
-#38 := (or #37 #10)
-#41 := (not #38)
+#21 := (not #13)
+#22 := (or #21 #10)
+#25 := (not #22)
#14 := (implies #13 #10)
#15 := (not #14)
-#42 := (iff #15 #41)
-#39 := (iff #14 #38)
-#40 := [rewrite]: #39
-#43 := [monotonicity #40]: #42
-#36 := [asserted]: #15
-#46 := [mp #36 #43]: #41
-#49 := [not-or-elim #46]: #48
-#58 := [iff-false #49]: #57
-#55 := (iff #8 false)
-#44 := [not-or-elim #46]: #13
-#47 := [and-elim #44]: #12
-#56 := [iff-false #47]: #55
-#61 := [monotonicity #56 #58]: #60
-#65 := [trans #61 #63]: #64
-#45 := [and-elim #44]: #11
-[mp #45 #65]: false
+#26 := (iff #15 #25)
+#23 := (iff #14 #22)
+#24 := [rewrite]: #23
+#27 := [monotonicity #24]: #26
+#17 := [asserted]: #15
+#28 := [mp #17 #27]: #25
+#29 := [not-or-elim #28]: #13
+#31 := [and-elim #29]: #12
+#32 := (not #10)
+#33 := [not-or-elim #28]: #32
+#30 := [and-elim #29]: #11
+[unit-resolution #30 #33 #31]: false
+55b7bd861df00e9621f738450037b0df80372741 84 0
unsat
-bc6de36d6c86b416e91711bb23067cc8250ac153 33 0
#2 := false
decl f1 :: S1
#3 := f1
+decl f5 :: S1
+#12 := f5
+#13 := (= f5 f1)
decl f6 :: S1
#14 := f6
#15 := (= f6 f1)
-decl f5 :: S1
-#12 := f5
-#13 := (= f5 f1)
-#16 := (and #13 #15)
+#64 := (not #15)
+#63 := (not #13)
+#65 := (or #63 #64)
+#66 := (not #65)
decl f4 :: S1
#9 := f4
#10 := (= f4 f1)
+#58 := (not #10)
decl f3 :: S1
#7 := f3
#8 := (= f3 f1)
+#57 := (not #8)
+#59 := (or #57 #58)
+#60 := (not #59)
+#101 := [hypothesis]: #60
+#89 := (or #59 #8)
+#90 := [def-axiom]: #89
+#102 := [unit-resolution #90 #101]: #8
+#91 := (or #59 #10)
+#92 := [def-axiom]: #91
+#103 := [unit-resolution #92 #101]: #10
#11 := (and #8 #10)
+#34 := (not #11)
+#78 := (iff #34 #59)
+#73 := (not #60)
+#76 := (iff #73 #59)
+#77 := [rewrite]: #76
+#74 := (iff #34 #73)
+#61 := (iff #11 #60)
+#62 := [rewrite]: #61
+#75 := [monotonicity #62]: #74
+#79 := [trans #75 #77]: #78
+#16 := (and #13 #15)
#17 := (or #11 #16)
+#25 := (not #17)
+#26 := (or #25 #11 #16)
+#29 := (not #26)
#18 := (implies #17 #17)
#19 := (not #18)
-#48 := (iff #19 false)
-#1 := true
-#43 := (not true)
-#46 := (iff #43 false)
-#47 := [rewrite]: #46
-#44 := (iff #19 #43)
-#41 := (iff #18 true)
-#42 := [rewrite]: #41
-#45 := [monotonicity #42]: #44
-#49 := [trans #45 #47]: #48
-#40 := [asserted]: #19
-[mp #40 #49]: false
+#30 := (iff #19 #29)
+#27 := (iff #18 #26)
+#28 := [rewrite]: #27
+#31 := [monotonicity #28]: #30
+#21 := [asserted]: #19
+#32 := [mp #21 #31]: #29
+#35 := [not-or-elim #32]: #34
+#80 := [mp #35 #79]: #59
+#104 := [unit-resolution #80 #103 #102]: false
+#105 := [lemma #104]: #59
+#69 := (or #60 #66)
+#70 := (iff #17 #69)
+#67 := (iff #16 #66)
+#68 := [rewrite]: #67
+#71 := [monotonicity #62 #68]: #70
+#33 := [not-or-elim #32]: #17
+#72 := [mp #33 #71]: #69
+#106 := [unit-resolution #72 #105]: #66
+#95 := (or #65 #13)
+#96 := [def-axiom]: #95
+#107 := [unit-resolution #96 #106]: #13
+#97 := (or #65 #15)
+#98 := [def-axiom]: #97
+#108 := [unit-resolution #98 #106]: #15
+#36 := (not #16)
+#86 := (iff #36 #65)
+#81 := (not #66)
+#84 := (iff #81 #65)
+#85 := [rewrite]: #84
+#82 := (iff #36 #81)
+#83 := [monotonicity #68]: #82
+#87 := [trans #83 #85]: #86
+#37 := [not-or-elim #32]: #36
+#88 := [mp #37 #87]: #65
+[unit-resolution #88 #108 #107]: false
+ecaaaeb4b508586ee415aaee164d7f38d7fa3191 50 0
unsat
-e334e079d0f61721e404e4ca140ce40c317189ba 55 0
#2 := false
decl f1 :: S1
#3 := f1
@@ -157,41 +190,36 @@
#14 := (or #11 #13)
#20 := (implies #14 #19)
#21 := (not #20)
-#71 := (iff #21 false)
-#43 := (not #8)
-#44 := (or #43 #17)
-#47 := (or #44 #8)
-#53 := (not #14)
-#54 := (or #53 #47)
-#59 := (not #54)
-#69 := (iff #59 false)
+#50 := (iff #21 false)
#1 := true
-#64 := (not true)
-#67 := (iff #64 false)
-#68 := [rewrite]: #67
-#65 := (iff #59 #64)
-#62 := (iff #54 true)
-#63 := [rewrite]: #62
-#66 := [monotonicity #63]: #65
-#70 := [trans #66 #68]: #69
-#60 := (iff #21 #59)
-#57 := (iff #20 #54)
-#50 := (implies #14 #47)
-#55 := (iff #50 #54)
-#56 := [rewrite]: #55
-#51 := (iff #20 #50)
-#48 := (iff #19 #47)
-#45 := (iff #18 #44)
-#46 := [rewrite]: #45
-#49 := [monotonicity #46]: #48
-#52 := [monotonicity #49]: #51
-#58 := [trans #52 #56]: #57
-#61 := [monotonicity #58]: #60
-#72 := [trans #61 #70]: #71
-#42 := [asserted]: #21
-[mp #42 #72]: false
+#45 := (not true)
+#48 := (iff #45 false)
+#49 := [rewrite]: #48
+#46 := (iff #21 #45)
+#43 := (iff #20 true)
+#38 := (implies #14 true)
+#41 := (iff #38 true)
+#42 := [rewrite]: #41
+#39 := (iff #20 #38)
+#36 := (iff #19 true)
+#27 := (not #8)
+#28 := (or #27 #15 #16)
+#31 := (or #28 #8)
+#34 := (iff #31 true)
+#35 := [rewrite]: #34
+#32 := (iff #19 #31)
+#29 := (iff #18 #28)
+#30 := [rewrite]: #29
+#33 := [monotonicity #30]: #32
+#37 := [trans #33 #35]: #36
+#40 := [monotonicity #37]: #39
+#44 := [trans #40 #42]: #43
+#47 := [monotonicity #44]: #46
+#51 := [trans #47 #49]: #50
+#23 := [asserted]: #21
+[mp #23 #51]: false
+01c3def9cab437126fe354f5b2293506994546fd 60 0
unsat
-778009f890fff5d244f6b4e04a54c69b4023bcd7 60 0
#2 := false
decl f1 :: S1
#3 := f1
@@ -208,81 +236,61 @@
#16 := (iff #15 #8)
#17 := (iff #16 #8)
#18 := (not #17)
-#78 := (iff #18 false)
+#62 := (iff #18 false)
#1 := true
-#73 := (not true)
-#76 := (iff #73 false)
-#77 := [rewrite]: #76
-#74 := (iff #18 #73)
-#71 := (iff #17 true)
-#40 := (iff #9 true)
-#41 := [rewrite]: #40
-#69 := (iff #17 #9)
-#42 := (iff true #8)
-#45 := (iff #42 #8)
-#46 := [rewrite]: #45
-#66 := (iff #16 #42)
-#64 := (iff #15 true)
-#62 := (iff #15 #9)
-#59 := (iff #14 #42)
-#57 := (iff #13 true)
-#55 := (iff #13 #9)
-#52 := (iff #12 #42)
-#50 := (iff #11 true)
-#48 := (iff #11 #9)
-#43 := (iff #10 #42)
-#44 := [monotonicity #41]: #43
-#47 := [trans #44 #46]: #11
-#49 := [monotonicity #47]: #48
-#51 := [trans #49 #41]: #50
-#53 := [monotonicity #51]: #52
-#54 := [trans #53 #46]: #13
-#56 := [monotonicity #54]: #55
-#58 := [trans #56 #41]: #57
-#60 := [monotonicity #58]: #59
-#61 := [trans #60 #46]: #15
-#63 := [monotonicity #61]: #62
-#65 := [trans #63 #41]: #64
-#67 := [monotonicity #65]: #66
-#68 := [trans #67 #46]: #17
-#70 := [monotonicity #68]: #69
-#72 := [trans #70 #41]: #71
-#75 := [monotonicity #72]: #74
-#79 := [trans #75 #77]: #78
-#39 := [asserted]: #18
-[mp #39 #79]: false
+#57 := (not true)
+#60 := (iff #57 false)
+#61 := [rewrite]: #60
+#58 := (iff #18 #57)
+#55 := (iff #17 true)
+#24 := (iff #9 true)
+#25 := [rewrite]: #24
+#53 := (iff #17 #9)
+#26 := (iff true #8)
+#29 := (iff #26 #8)
+#30 := [rewrite]: #29
+#50 := (iff #16 #26)
+#48 := (iff #15 true)
+#46 := (iff #15 #9)
+#43 := (iff #14 #26)
+#41 := (iff #13 true)
+#39 := (iff #13 #9)
+#36 := (iff #12 #26)
+#34 := (iff #11 true)
+#32 := (iff #11 #9)
+#27 := (iff #10 #26)
+#28 := [monotonicity #25]: #27
+#31 := [trans #28 #30]: #11
+#33 := [monotonicity #31]: #32
+#35 := [trans #33 #25]: #34
+#37 := [monotonicity #35]: #36
+#38 := [trans #37 #30]: #13
+#40 := [monotonicity #38]: #39
+#42 := [trans #40 #25]: #41
+#44 := [monotonicity #42]: #43
+#45 := [trans #44 #30]: #15
+#47 := [monotonicity #45]: #46
+#49 := [trans #47 #25]: #48
+#51 := [monotonicity #49]: #50
+#52 := [trans #51 #30]: #17
+#54 := [monotonicity #52]: #53
+#56 := [trans #54 #25]: #55
+#59 := [monotonicity #56]: #58
+#63 := [trans #59 #61]: #62
+#20 := [asserted]: #18
+[mp #20 #63]: false
+cd163c8c9afce7b0a8a2f73345db7dfc9e0d1c10 112 0
unsat
-1d6ace6138adeb11b9c9952f896f225452c30f9e 165 0
#2 := false
decl f1 :: S1
#3 := f1
-decl f6 :: S1
-#13 := f6
-#14 := (= f6 f1)
-decl f5 :: S1
-#11 := f5
-#12 := (= f5 f1)
decl f4 :: S1
#9 := f4
#10 := (= f4 f1)
-decl f3 :: S1
-#7 := f3
-#8 := (= f3 f1)
-#75 := (or #8 #10 #12 #14)
-#215 := (iff #75 false)
-#210 := (or false false false false)
-#213 := (iff #210 false)
-#214 := [rewrite]: #213
-#211 := (iff #75 #210)
-#167 := (iff #14 false)
-#119 := (not #14)
-#122 := (or #119 #12)
-#175 := (iff #122 #119)
-#170 := (or #119 false)
-#173 := (iff #170 #119)
-#174 := [rewrite]: #173
-#171 := (iff #122 #170)
-#168 := (iff #12 false)
+#107 := (not #10)
+decl f5 :: S1
+#11 := f5
+#12 := (= f5 f1)
#25 := (not #12)
decl f11 :: S1
#43 := f11
@@ -297,59 +305,9 @@
#48 := (and #42 #47)
#49 := (or #12 #48)
#50 := (not #49)
-#150 := (iff #50 #25)
-#148 := (iff #49 #12)
-#143 := (or #12 false)
-#146 := (iff #143 #12)
-#147 := [rewrite]: #146
-#144 := (iff #49 #143)
-#141 := (iff #48 false)
-#136 := (and #42 #41)
-#139 := (iff #136 false)
-#140 := [rewrite]: #139
-#137 := (iff #48 #136)
-#134 := (iff #47 #41)
-#129 := (or #41 false)
-#132 := (iff #129 #41)
-#133 := [rewrite]: #132
-#130 := (iff #47 #129)
-#126 := (iff #46 false)
-#128 := [rewrite]: #126
-#131 := [monotonicity #128]: #130
-#135 := [trans #131 #133]: #134
-#138 := [monotonicity #135]: #137
-#142 := [trans #138 #140]: #141
-#145 := [monotonicity #142]: #144
-#149 := [trans #145 #147]: #148
-#151 := [monotonicity #149]: #150
-#125 := [asserted]: #50
-#154 := [mp #125 #151]: #25
-#169 := [iff-false #154]: #168
-#172 := [monotonicity #169]: #171
-#176 := [trans #172 #174]: #175
-#37 := (or #14 false)
-#38 := (not #37)
-#39 := (or #38 #12)
-#123 := (iff #39 #122)
-#120 := (iff #38 #119)
-#116 := (iff #37 #14)
-#118 := [rewrite]: #116
-#121 := [monotonicity #118]: #120
-#124 := [monotonicity #121]: #123
-#115 := [asserted]: #39
-#127 := [mp #115 #124]: #122
-#166 := [mp #127 #176]: #119
-#177 := [iff-false #166]: #167
-#165 := (iff #10 false)
-#109 := (not #10)
-#112 := (or #109 #12)
-#183 := (iff #112 #109)
-#178 := (or #109 false)
-#181 := (iff #178 #109)
-#182 := [rewrite]: #181
-#179 := (iff #112 #178)
-#180 := [monotonicity #169]: #179
-#184 := [trans #180 #182]: #183
+#58 := [asserted]: #50
+#59 := [not-or-elim #58]: #25
+#110 := (or #107 #12)
decl f9 :: S1
#30 := f9
#31 := (= f9 f1)
@@ -358,67 +316,84 @@
#34 := (and #10 #33)
#35 := (not #34)
#36 := (or #35 #12)
-#113 := (iff #36 #112)
-#110 := (iff #35 #109)
-#107 := (iff #34 #10)
+#111 := (iff #36 #110)
+#108 := (iff #35 #107)
+#105 := (iff #34 #10)
#1 := true
-#102 := (and #10 true)
-#105 := (iff #102 #10)
-#106 := [rewrite]: #105
-#103 := (iff #34 #102)
-#99 := (iff #33 true)
-#101 := [rewrite]: #99
-#104 := [monotonicity #101]: #103
-#108 := [trans #104 #106]: #107
-#111 := [monotonicity #108]: #110
-#114 := [monotonicity #111]: #113
-#98 := [asserted]: #36
-#117 := [mp #98 #114]: #112
-#164 := [mp #117 #184]: #109
-#185 := [iff-false #164]: #165
-#163 := (iff #8 false)
-#92 := (not #8)
-#95 := (or #92 #10)
-#191 := (iff #95 #92)
-#186 := (or #92 false)
-#189 := (iff #186 #92)
-#190 := [rewrite]: #189
-#187 := (iff #95 #186)
-#188 := [monotonicity #185]: #187
-#192 := [trans #188 #190]: #191
+#100 := (and #10 true)
+#103 := (iff #100 #10)
+#104 := [rewrite]: #103
+#101 := (iff #34 #100)
+#98 := (iff #33 true)
+#99 := [rewrite]: #98
+#102 := [monotonicity #99]: #101
+#106 := [trans #102 #104]: #105
+#109 := [monotonicity #106]: #108
+#112 := [monotonicity #109]: #111
+#56 := [asserted]: #36
+#113 := [mp #56 #112]: #110
+#153 := [unit-resolution #113 #59]: #107
+decl f3 :: S1
+#7 := f3
+#8 := (= f3 f1)
+decl f6 :: S1
+#13 := f6
+#14 := (= f6 f1)
+#116 := (not #14)
+#119 := (or #116 #12)
+#37 := (or #14 false)
+#38 := (not #37)
+#39 := (or #38 #12)
+#120 := (iff #39 #119)
+#117 := (iff #38 #116)
+#114 := (iff #37 #14)
+#115 := [rewrite]: #114
+#118 := [monotonicity #115]: #117
+#121 := [monotonicity #118]: #120
+#57 := [asserted]: #39
+#122 := [mp #57 #121]: #119
+#154 := [unit-resolution #122 #59]: #116
+#72 := (or #8 #10 #12 #14)
+#15 := (or #12 #14)
+#16 := (or #10 #15)
+#17 := (or #8 #16)
+#75 := (iff #17 #72)
+#66 := (or #10 #12 #14)
+#69 := (or #8 #66)
+#73 := (iff #69 #72)
+#74 := [rewrite]: #73
+#70 := (iff #17 #69)
+#67 := (iff #16 #66)
+#68 := [rewrite]: #67
+#71 := [monotonicity #68]: #70
+#76 := [trans #71 #74]: #75
+#53 := [asserted]: #17
+#77 := [mp #53 #76]: #72
+#155 := [unit-resolution #77 #153 #59 #154]: #8
+#91 := (not #8)
+#94 := (or #91 #10)
#26 := (and #12 #25)
#27 := (or #8 #26)
#28 := (not #27)
#29 := (or #28 #10)
-#96 := (iff #29 #95)
-#93 := (iff #28 #92)
-#90 := (iff #27 #8)
-#85 := (or #8 false)
-#88 := (iff #85 #8)
-#89 := [rewrite]: #88
-#86 := (iff #27 #85)
-#79 := (iff #26 false)
-#84 := [rewrite]: #79
-#87 := [monotonicity #84]: #86
-#91 := [trans #87 #89]: #90
-#94 := [monotonicity #91]: #93
-#97 := [monotonicity #94]: #96
-#74 := [asserted]: #29
-#100 := [mp #74 #97]: #95
-#162 := [mp #100 #192]: #92
-#193 := [iff-false #162]: #163
-#212 := [monotonicity #193 #185 #169 #177]: #211
-#216 := [trans #212 #214]: #215
-#15 := (or #12 #14)
-#16 := (or #10 #15)
-#17 := (or #8 #16)
-#76 := (iff #17 #75)
-#77 := [rewrite]: #76
-#72 := [asserted]: #17
-#78 := [mp #72 #77]: #75
-[mp #78 #216]: false
+#95 := (iff #29 #94)
+#92 := (iff #28 #91)
+#89 := (iff #27 #8)
+#84 := (or #8 false)
+#87 := (iff #84 #8)
+#88 := [rewrite]: #87
+#85 := (iff #27 #84)
+#82 := (iff #26 false)
+#83 := [rewrite]: #82
+#86 := [monotonicity #83]: #85
+#90 := [trans #86 #88]: #89
+#93 := [monotonicity #90]: #92
+#96 := [monotonicity #93]: #95
+#55 := [asserted]: #29
+#97 := [mp #55 #96]: #94
+[unit-resolution #97 #155 #153]: false
+bda0de69751a63d54481e3e810bc744b04b03fa3 59 0
unsat
-dd0cba0a17795cc066f8c77647c6bcb52b690616 59 0
#2 := false
decl f3 :: (-> S3 S2 S2)
decl f6 :: S2
@@ -433,84 +408,55 @@
#18 := (f4 f5 f6)
#20 := (f3 #18 f7)
#23 := (= #20 #22)
-#57 := (not #23)
+#41 := (not #23)
#17 := (= f6 f6)
#24 := (and #17 #23)
#25 := (not #24)
-#58 := (iff #25 #57)
-#55 := (iff #24 #23)
+#42 := (iff #25 #41)
+#39 := (iff #24 #23)
#1 := true
-#50 := (and true #23)
-#53 := (iff #50 #23)
-#54 := [rewrite]: #53
-#51 := (iff #24 #50)
-#48 := (iff #17 true)
-#49 := [rewrite]: #48
-#52 := [monotonicity #49]: #51
-#56 := [trans #52 #54]: #55
-#59 := [monotonicity #56]: #58
-#47 := [asserted]: #25
-#62 := [mp #47 #59]: #57
+#34 := (and true #23)
+#37 := (iff #34 #23)
+#38 := [rewrite]: #37
+#35 := (iff #24 #34)
+#32 := (iff #17 true)
+#33 := [rewrite]: #32
+#36 := [monotonicity #33]: #35
+#40 := [trans #36 #38]: #39
+#43 := [monotonicity #40]: #42
+#28 := [asserted]: #25
+#44 := [mp #28 #43]: #41
#8 := (:var 1 S2)
#10 := (:var 0 S2)
#12 := (f4 f5 #10)
#13 := (f3 #12 #8)
-#546 := (pattern #13)
+#487 := (pattern #13)
#9 := (f4 f5 #8)
#11 := (f3 #9 #10)
-#545 := (pattern #11)
+#486 := (pattern #11)
#14 := (= #11 #13)
-#547 := (forall (vars (?v0 S2) (?v1 S2)) (:pat #545 #546) #14)
+#488 := (forall (vars (?v0 S2) (?v1 S2)) (:pat #486 #487) #14)
#15 := (forall (vars (?v0 S2) (?v1 S2)) #14)
-#550 := (iff #15 #547)
-#548 := (iff #14 #14)
-#549 := [refl]: #548
-#551 := [quant-intro #549]: #550
-#70 := (~ #15 #15)
-#68 := (~ #14 #14)
-#69 := [refl]: #68
-#71 := [nnf-pos #69]: #70
-#46 := [asserted]: #15
-#61 := [mp~ #46 #71]: #15
-#552 := [mp #61 #551]: #547
-#130 := (not #547)
-#216 := (or #130 #23)
-#131 := [quant-inst #16 #19]: #216
-[unit-resolution #131 #552 #62]: false
+#491 := (iff #15 #488)
+#489 := (iff #14 #14)
+#490 := [refl]: #489
+#492 := [quant-intro #490]: #491
+#66 := (~ #15 #15)
+#64 := (~ #14 #14)
+#65 := [refl]: #64
+#67 := [nnf-pos #65]: #66
+#27 := [asserted]: #15
+#68 := [mp~ #27 #67]: #15
+#493 := [mp #68 #492]: #488
+#72 := (not #488)
+#157 := (or #72 #23)
+#69 := [quant-inst #16 #19]: #157
+[unit-resolution #69 #493 #44]: false
+01921123e04538e755e19bf1587fc40380f6a26a 1573 0
unsat
-0863329327da9e45e4d77f7bc111e467c5d58d3c 1288 0
#2 := false
decl f1 :: S1
#3 := f1
-decl f9 :: S1
-#25 := f9
-#26 := (= f9 f1)
-decl f20 :: S1
-#59 := f20
-#60 := (= f20 f1)
-decl f21 :: S1
-#61 := f21
-#62 := (= f21 f1)
-#249 := (not #62)
-decl f31 :: S1
-#97 := f31
-#98 := (= f31 f1)
-decl f62 :: S1
-#207 := f62
-#208 := (= f62 f1)
-decl f58 :: S1
-#189 := f58
-#190 := (= f58 f1)
-#388 := (not #190)
-decl f47 :: S1
-#151 := f47
-#152 := (= f47 f1)
-#289 := (not #98)
-#980 := [hypothesis]: #289
-decl f46 :: S1
-#149 := f46
-#150 := (= f46 f1)
-#346 := (not #150)
decl f48 :: S1
#156 := f48
#157 := (= f48 f1)
@@ -522,183 +468,20 @@
#144 := f45
#145 := (= f45 f1)
#339 := (not #145)
-decl f42 :: S1
-#135 := f42
-#136 := (= f42 f1)
-#1467 := (or #136 #98)
-decl f40 :: S1
-#128 := f40
-#129 := (= f40 f1)
-#330 := (not #136)
-#1095 := [hypothesis]: #330
-decl f32 :: S1
-#99 := f32
-#100 := (= f32 f1)
-#290 := (not #100)
-decl f16 :: S1
-#46 := f16
-#47 := (= f16 f1)
-decl f17 :: S1
-#48 := f17
-#49 := (= f17 f1)
-#236 := (not #49)
-decl f28 :: S1
-#86 := f28
-#87 := (= f28 f1)
-#1450 := (or #87 #98 #136)
-decl f29 :: S1
-#90 := f29
-#91 := (= f29 f1)
-#281 := (not #91)
-#322 := (not #129)
-#277 := (not #87)
-#867 := [hypothesis]: #277
-#1427 := (or #322 #87)
-decl f51 :: S1
-#166 := f51
-#167 := (= f51 f1)
-#363 := (not #167)
-decl f54 :: S1
-#175 := f54
-#176 := (= f54 f1)
-decl f56 :: S1
-#182 := f56
-#183 := (= f56 f1)
-#380 := (not #183)
-#372 := (not #176)
-#1160 := [hypothesis]: #372
-#1189 := (or #388 #176)
-decl f18 :: S1
-#52 := f18
-#53 := (= f18 f1)
+decl f34 :: S1
+#106 := f34
+#107 := (= f34 f1)
decl f33 :: S1
#104 := f33
#105 := (= f33 f1)
#297 := (not #105)
-decl f36 :: S1
-#113 := f36
-#114 := (= f36 f1)
-#347 := (not #152)
-#1155 := [hypothesis]: #190
-#393 := (or #388 #347)
-#730 := [asserted]: #393
-#1156 := [unit-resolution #730 #1155]: #347
-#389 := (or #387 #388)
-#726 := [asserted]: #389
-#1157 := [unit-resolution #726 #1155]: #387
-#194 := (or #188 #157)
-decl f6 :: S1
-#16 := f6
-#17 := (= f6 f1)
-#579 := (or #17 #188 #157)
-#840 := (iff #579 #194)
-#835 := (or false #188 #157)
-#838 := (iff #835 #194)
-#839 := [rewrite]: #838
-#836 := (iff #579 #835)
-#759 := (iff #17 false)
-#18 := (not #17)
-#439 := [asserted]: #18
-#760 := [iff-false #439]: #759
-#837 := [monotonicity #760]: #836
-#841 := [trans #837 #839]: #840
-#195 := (or #17 #194)
-#580 := (iff #195 #579)
-#581 := [rewrite]: #580
-#568 := [asserted]: #195
-#582 := [mp #568 #581]: #579
-#842 := [mp #582 #841]: #194
-#1158 := [unit-resolution #842 #1157]: #157
#354 := (not #157)
-#355 := (or #354 #346)
-#702 := [asserted]: #355
-#1159 := [unit-resolution #702 #1158]: #346
-decl f44 :: S1
-#142 := f44
-#143 := (= f44 f1)
-#338 := (not #143)
-decl f61 :: S1
-#203 := f61
-#204 := (= f61 f1)
-decl f60 :: S1
-#199 := f60
-#200 := (= f60 f1)
-#400 := (not #200)
decl f37 :: S1
#118 := f37
#119 := (= f37 f1)
-#313 := (not #119)
-#356 := (or #354 #313)
-#703 := [asserted]: #356
-#1161 := [unit-resolution #703 #1158]: #313
-#983 := (or #400 #150 #152 #119)
-#248 := (not #60)
-decl f23 :: S1
-#68 := f23
-#69 := (= f23 f1)
-decl f34 :: S1
-#106 := f34
-#107 := (= f34 f1)
-#298 := (not #107)
-#1051 := [hypothesis]: #347
-#1052 := [hypothesis]: #346
-#306 := (not #114)
-decl f25 :: S1
-#75 := f25
-#76 := (= f25 f1)
-decl f39 :: S1
-#124 := f39
-#125 := (= f39 f1)
-#318 := (not #125)
-decl f50 :: S1
-#162 := f50
-#163 := (= f50 f1)
-decl f59 :: S1
-#196 := f59
-#197 := (= f59 f1)
-#398 := (not #197)
-#1024 := [hypothesis]: #200
-#401 := (or #400 #398)
-#736 := [asserted]: #401
-#1021 := [unit-resolution #736 #1024]: #398
-#198 := (or #197 #163)
-#573 := [asserted]: #198
-#1022 := [unit-resolution #573 #1021]: #163
-#359 := (not #163)
-#362 := (or #359 #318)
-#707 := [asserted]: #362
-#1019 := [unit-resolution #707 #1022]: #318
decl f26 :: S1
#80 := f26
#81 := (= f26 f1)
-#1153 := [hypothesis]: #313
-decl f35 :: S1
-#111 := f35
-#112 := (= f35 f1)
-#305 := (not #112)
-decl f43 :: S1
-#137 := f43
-#138 := (= f43 f1)
-#331 := (not #138)
-decl f52 :: S1
-#168 := f52
-#169 := (= f52 f1)
-#364 := (not #169)
-#402 := (or #400 #364)
-#737 := [asserted]: #402
-#1020 := [unit-resolution #737 #1024]: #364
-decl f49 :: S1
-#160 := f49
-#161 := (= f49 f1)
-#358 := (not #161)
-#360 := (or #358 #359)
-#705 := [asserted]: #360
-#1017 := [unit-resolution #705 #1022]: #358
-decl f41 :: S1
-#130 := f41
-#131 := (= f41 f1)
-#323 := (not #131)
-#1126 := (or #323 #119 #125)
#272 := (not #81)
decl f15 :: S1
#43 := f15
@@ -707,1089 +490,1566 @@
#37 := f13
#38 := (= f13 f1)
#228 := (not #38)
-decl f11 :: S1
-#31 := f11
-#32 := (= f11 f1)
+decl f14 :: S1
+#39 := f14
+#40 := (= f14 f1)
+decl f27 :: S1
+#84 := f27
+#85 := (= f27 f1)
+decl f29 :: S1
+#90 := f29
+#91 := (= f29 f1)
+#281 := (not #91)
+decl f31 :: S1
+#97 := f31
+#98 := (= f31 f1)
+decl f36 :: S1
+#113 := f36
+#114 := (= f36 f1)
+decl f47 :: S1
+#151 := f47
+#152 := (= f47 f1)
+#347 := (not #152)
+#229 := (not #40)
+#1030 := [hypothesis]: #229
+#1766 := (or #119 #40)
+#313 := (not #119)
+#970 := [hypothesis]: #313
+decl f22 :: S1
+#66 := f22
+#67 := (= f22 f1)
+#256 := (not #67)
+decl f20 :: S1
+#59 := f20
+#60 := (= f20 f1)
+#1740 := (or #60 #40 #119)
+decl f9 :: S1
+#25 := f9
+#26 := (= f9 f1)
#218 := (not #26)
-decl f7 :: S1
-#19 := f7
-#20 := (= f7 f1)
+#248 := (not #60)
+#919 := [hypothesis]: #248
+#1666 := (or #218 #60)
+decl f19 :: S1
+#54 := f19
+#55 := (= f19 f1)
+#241 := (not #55)
decl f8 :: S1
#21 := f8
#22 := (= f8 f1)
+decl f7 :: S1
+#19 := f7
+#20 := (= f7 f1)
+#213 := (not #20)
+#1651 := [hypothesis]: #26
+#221 := (or #218 #213)
+#459 := [asserted]: #221
+#1652 := [unit-resolution #459 #1651]: #213
+#904 := (or #20 #22)
+decl f3 :: S1
+#7 := f3
+#8 := (= f3 f1)
+#9 := (not #8)
+#417 := [asserted]: #9
+#605 := (or #20 #22 #8)
+#23 := (or #22 #8)
+#24 := (or #20 #23)
+#606 := (iff #24 #605)
+#607 := [rewrite]: #606
+#421 := [asserted]: #24
+#608 := [mp #421 #607]: #605
+#905 := [unit-resolution #608 #417]: #904
+#1653 := [unit-resolution #905 #1652]: #22
#214 := (not #22)
-#1154 := [hypothesis]: #318
-decl f38 :: S1
-#122 := f38
-#123 := (= f38 f1)
-#317 := (not #123)
-#1151 := [hypothesis]: #131
-#327 := (or #323 #317)
-#681 := [asserted]: #327
-#1152 := [unit-resolution #681 #1151]: #317
-#524 := (or #123 #125 #87)
-#126 := (or #125 #87)
-#127 := (or #123 #126)
-#525 := (iff #127 #524)
-#526 := [rewrite]: #525
-#513 := [asserted]: #127
-#527 := [mp #513 #526]: #524
-#1149 := [unit-resolution #527 #1152 #1154]: #87
-#280 := (or #277 #236)
-#647 := [asserted]: #280
-#1150 := [unit-resolution #647 #1149]: #236
-#783 := (or #47 #49)
+#246 := (or #241 #214)
+#475 := [asserted]: #246
+#1654 := [unit-resolution #475 #1653]: #241
+decl f21 :: S1
+#61 := f21
+#62 := (= f21 f1)
+decl f10 :: S1
+#27 := f10
+#28 := (= f10 f1)
+#219 := (not #28)
+#220 := (or #218 #219)
+#458 := [asserted]: #220
+#1655 := [unit-resolution #458 #1651]: #219
+decl f18 :: S1
+#52 := f18
+#53 := (= f18 f1)
+#240 := (not #53)
+#244 := (or #240 #214)
+#473 := [asserted]: #244
+#1656 := [unit-resolution #473 #1653]: #240
+#643 := (or #60 #62 #53 #28)
+#63 := (or #53 #28)
+#64 := (or #62 #63)
+#65 := (or #60 #64)
+#646 := (iff #65 #643)
+#637 := (or #62 #53 #28)
+#640 := (or #60 #637)
+#644 := (iff #640 #643)
+#645 := [rewrite]: #644
+#641 := (iff #65 #640)
+#638 := (iff #64 #637)
+#639 := [rewrite]: #638
+#642 := [monotonicity #639]: #641
+#647 := [trans #642 #645]: #646
+#428 := [asserted]: #65
+#648 := [mp #428 #647]: #643
+#1657 := [unit-resolution #648 #1656 #919 #1655]: #62
+#249 := (not #62)
+#296 := (or #281 #249)
+#512 := [asserted]: #296
+#1658 := [unit-resolution #512 #1657]: #281
+#276 := (not #85)
+decl f17 :: S1
+#48 := f17
+#49 := (= f17 f1)
+decl f16 :: S1
+#46 := f16
+#47 := (= f16 f1)
+#235 := (not #47)
+#247 := (or #235 #214)
+#476 := [asserted]: #247
+#1659 := [unit-resolution #476 #1653]: #235
+#915 := (or #47 #49)
decl f4 :: S1
#10 := f4
#11 := (= f4 f1)
-#464 := (or #47 #49 #11)
-#786 := (iff #464 #783)
-#780 := (or #47 #49 false)
-#784 := (iff #780 #783)
-#785 := [rewrite]: #784
-#781 := (iff #464 #780)
-#755 := (iff #11 false)
#12 := (not #11)
-#437 := [asserted]: #12
-#756 := [iff-false #437]: #755
-#782 := [monotonicity #756]: #781
-#787 := [trans #782 #785]: #786
+#418 := [asserted]: #12
+#621 := (or #47 #49 #11)
#50 := (or #49 #11)
#51 := (or #47 #50)
-#465 := (iff #51 #464)
-#466 := [rewrite]: #465
-#457 := [asserted]: #51
-#467 := [mp #457 #466]: #464
-#788 := [mp #467 #787]: #783
-#1147 := [unit-resolution #788 #1150]: #47
-#235 := (not #47)
-#247 := (or #235 #214)
-#623 := [asserted]: #247
-#1148 := [unit-resolution #623 #1147]: #214
-#764 := (or #20 #22)
-decl f3 :: S1
-#7 := f3
-#8 := (= f3 f1)
-#443 := (or #20 #22 #8)
-#767 := (iff #443 #764)
-#761 := (or #20 #22 false)
-#765 := (iff #761 #764)
-#766 := [rewrite]: #765
-#762 := (iff #443 #761)
-#752 := (iff #8 false)
-#9 := (not #8)
-#436 := [asserted]: #9
-#754 := [iff-false #436]: #752
-#763 := [monotonicity #754]: #762
-#768 := [trans #763 #766]: #767
-#23 := (or #22 #8)
-#24 := (or #20 #23)
-#444 := (iff #24 #443)
-#445 := [rewrite]: #444
-#440 := [asserted]: #24
-#446 := [mp #440 #445]: #443
-#769 := [mp #446 #768]: #764
-#1145 := [unit-resolution #769 #1148]: #20
-#213 := (not #20)
-#221 := (or #218 #213)
-#606 := [asserted]: #221
-#1146 := [unit-resolution #606 #1145]: #218
-decl f12 :: S1
-#33 := f12
-#34 := (= f12 f1)
-#224 := (not #34)
+#622 := (iff #51 #621)
+#623 := [rewrite]: #622
+#426 := [asserted]: #51
+#624 := [mp #426 #623]: #621
+#916 := [unit-resolution #624 #418]: #915
+#1660 := [unit-resolution #916 #1659]: #49
+#236 := (not #49)
+#279 := (or #276 #236)
+#499 := [asserted]: #279
+#1661 := [unit-resolution #499 #1660]: #276
+#1663 := (or #91 #85 #55)
decl f30 :: S1
#92 := f30
#93 := (= f30 f1)
#282 := (not #93)
-#328 := (or #323 #282)
-#682 := [asserted]: #328
-#1143 := [unit-resolution #682 #1151]: #282
-decl f27 :: S1
-#84 := f27
-#85 := (= f27 f1)
-#276 := (not #85)
-#278 := (or #276 #277)
-#645 := [asserted]: #278
-#1144 := [unit-resolution #645 #1149]: #276
-decl f19 :: S1
-#54 := f19
-#55 := (= f19 f1)
-#241 := (not #55)
-#245 := (or #241 #235)
-#621 := [asserted]: #245
-#1141 := [unit-resolution #621 #1147]: #241
-#499 := (or #91 #93 #85 #55)
-#94 := (or #85 #55)
-#95 := (or #93 #94)
-#96 := (or #91 #95)
-#500 := (iff #96 #499)
-#501 := [rewrite]: #500
-#488 := [asserted]: #96
-#502 := [mp #488 #501]: #499
-#1142 := [unit-resolution #502 #1141 #1144 #1143]: #91
-#296 := (or #281 #249)
-#659 := [asserted]: #296
-#1139 := [unit-resolution #659 #1142]: #249
-#240 := (not #53)
-#243 := (or #240 #235)
-#619 := [asserted]: #243
-#1140 := [unit-resolution #619 #1147]: #240
-decl f10 :: S1
-#27 := f10
-#28 := (= f10 f1)
-#219 := (not #28)
-#222 := (or #219 #213)
-#607 := [asserted]: #222
-#1137 := [unit-resolution #607 #1145]: #219
-#474 := (or #60 #62 #53 #28)
-#63 := (or #53 #28)
-#64 := (or #62 #63)
-#65 := (or #60 #64)
-#475 := (iff #65 #474)
-#476 := [rewrite]: #475
-#463 := [asserted]: #65
-#477 := [mp #463 #476]: #474
-#1138 := [unit-resolution #477 #1137 #1140 #1139]: #60
-#263 := (or #248 #224)
-#635 := [asserted]: #263
-#1135 := [unit-resolution #635 #1138]: #224
-#453 := (or #32 #34 #26)
-#35 := (or #34 #26)
-#36 := (or #32 #35)
-#454 := (iff #36 #453)
-#455 := [rewrite]: #454
-#442 := [asserted]: #36
-#456 := [mp #442 #455]: #453
-#1136 := [unit-resolution #456 #1135 #1146]: #32
+decl f40 :: S1
+#128 := f40
+#129 := (= f40 f1)
+#289 := (not #98)
+decl f41 :: S1
+#130 := f41
+#131 := (= f41 f1)
+decl f52 :: S1
+#168 := f52
+#169 := (= f52 f1)
+#364 := (not #169)
+decl f60 :: S1
+#199 := f60
+#200 := (= f60 f1)
+decl f61 :: S1
+#203 := f61
+#204 := (= f61 f1)
+#404 := (not #204)
+decl f56 :: S1
+#182 := f56
+#183 := (= f56 f1)
+#322 := (not #129)
+#881 := [hypothesis]: #322
+#1606 := (or #183 #129)
+decl f54 :: S1
+#175 := f54
+#176 := (= f54 f1)
+#372 := (not #176)
+decl f43 :: S1
+#137 := f43
+#138 := (= f43 f1)
+#380 := (not #183)
+#882 := [hypothesis]: #380
+#1359 := (or #387 #129 #183)
+decl f50 :: S1
+#162 := f50
+#163 := (= f50 f1)
+decl f59 :: S1
+#196 := f59
+#197 := (= f59 f1)
+#398 := (not #197)
+decl f62 :: S1
+#207 := f62
+#208 := (= f62 f1)
+decl f58 :: S1
+#189 := f58
+#190 := (= f58 f1)
+#388 := (not #190)
+#1337 := [hypothesis]: #188
+#389 := (or #387 #388)
+#579 := [asserted]: #389
+#1338 := [unit-resolution #579 #1337]: #388
+#211 := (or #208 #190)
+decl f5 :: S1
+#13 := f5
+#14 := (= f5 f1)
+#15 := (not #14)
+#419 := [asserted]: #15
+#857 := (or #14 #208 #190)
+#212 := (or #14 #211)
+#858 := (iff #212 #857)
+#859 := [rewrite]: #858
+#454 := [asserted]: #212
+#860 := [mp #454 #859]: #857
+#1339 := [unit-resolution #860 #419]: #211
+#1340 := [unit-resolution #1339 #1338]: #208
+#408 := (not #208)
+#409 := (or #408 #404)
+#595 := [asserted]: #409
+#1341 := [unit-resolution #595 #1340]: #404
+decl f53 :: S1
+#173 := f53
+#174 := (= f53 f1)
+decl f55 :: S1
+#180 := f55
+#181 := (= f55 f1)
+#379 := (not #181)
+#390 := (or #387 #379)
+#580 := [asserted]: #390
+#1342 := [unit-resolution #580 #1337]: #379
+#391 := (or #387 #347)
+#581 := [asserted]: #391
+#1343 := [unit-resolution #581 #1337]: #347
+#1335 := (or #339 #129 #181 #183 #204 #152)
+decl f39 :: S1
+#124 := f39
+#125 := (= f39 f1)
+#318 := (not #125)
+#969 := [hypothesis]: #404
+#883 := [hypothesis]: #379
+decl f25 :: S1
+#75 := f25
+#76 := (= f25 f1)
+#265 := (not #76)
+#1172 := [hypothesis]: #347
+#1304 := (or #40 #152 #204 #181 #183 #129)
+#1276 := (or #138 #152 #181 #183 #204 #129 #40)
+decl f46 :: S1
+#149 := f46
+#150 := (= f46 f1)
+#346 := (not #150)
+#1152 := (or #119 #129 #181 #183 #204)
+decl f32 :: S1
+#99 := f32
+#100 := (= f32 f1)
+#331 := (not #138)
+#400 := (not #200)
+#359 := (not #163)
+decl f28 :: S1
+#86 := f28
+#87 := (= f28 f1)
+#277 := (not #87)
+decl f11 :: S1
+#31 := f11
+#32 := (= f11 f1)
#223 := (not #32)
-#231 := (or #228 #223)
-#612 := [asserted]: #231
-#1133 := [unit-resolution #612 #1136]: #228
-#45 := (or #44 #38)
-#452 := [asserted]: #45
-#1134 := [unit-resolution #452 #1133]: #44
#233 := (not #44)
+#1008 := (or #233 #129 #181 #183 #204 #119)
+#371 := (not #174)
+decl f51 :: S1
+#166 := f51
+#167 := (= f51 f1)
+decl f35 :: S1
+#111 := f35
+#112 := (= f35 f1)
+#971 := [hypothesis]: #44
#274 := (or #272 #233)
-#643 := [asserted]: #274
-#1131 := [unit-resolution #643 #1134]: #272
-#519 := (or #119 #112 #81)
+#496 := [asserted]: #274
+#972 := [unit-resolution #496 #971]: #272
+#729 := (or #119 #112 #81)
#120 := (or #112 #81)
#121 := (or #119 #120)
-#520 := (iff #121 #519)
-#521 := [rewrite]: #520
-#508 := [asserted]: #121
-#522 := [mp #508 #521]: #519
-#1132 := [unit-resolution #522 #1131 #1153]: #112
-decl f14 :: S1
-#39 := f14
-#40 := (= f14 f1)
-#229 := (not #40)
-#232 := (or #229 #223)
-#613 := [asserted]: #232
-#1129 := [unit-resolution #613 #1136]: #229
-decl f22 :: S1
-#66 := f22
-#67 := (= f22 f1)
-#256 := (not #67)
-#259 := (or #256 #248)
-#631 := [asserted]: #259
-#1130 := [unit-resolution #631 #1138]: #256
+#730 := (iff #121 #729)
+#731 := [rewrite]: #730
+#437 := [asserted]: #121
+#732 := [mp #437 #731]: #729
+#973 := [unit-resolution #732 #972 #970]: #112
+#305 := (not #112)
+#308 := (or #305 #297)
+#520 := [asserted]: #308
+#974 := [unit-resolution #520 #973]: #297
+#309 := (or #305 #265)
+#521 := [asserted]: #309
+#975 := [unit-resolution #521 #973]: #265
decl f24 :: S1
#73 := f24
#74 := (= f24 f1)
#264 := (not #74)
#275 := (or #264 #233)
-#644 := [asserted]: #275
-#1127 := [unit-resolution #644 #1134]: #264
-#484 := (or #74 #76 #67 #40)
-#77 := (or #67 #40)
-#78 := (or #76 #77)
-#79 := (or #74 #78)
-#485 := (iff #79 #484)
-#486 := [rewrite]: #485
-#473 := [asserted]: #79
-#487 := [mp #473 #486]: #484
-#1128 := [unit-resolution #487 #1127 #1130 #1129]: #76
-#265 := (not #76)
-#309 := (or #305 #265)
-#668 := [asserted]: #309
-#1125 := [unit-resolution #668 #1128 #1132]: false
-#1123 := [lemma #1125]: #1126
-#1018 := [unit-resolution #1123 #1019 #1153]: #323
-#559 := (or #167 #169 #161 #131)
-#170 := (or #161 #131)
-#171 := (or #169 #170)
-#172 := (or #167 #171)
-#560 := (iff #172 #559)
-#561 := [rewrite]: #560
-#548 := [asserted]: #172
-#562 := [mp #548 #561]: #559
-#1015 := [unit-resolution #562 #1018 #1017 #1020]: #167
-#378 := (or #363 #331)
-#719 := [asserted]: #378
-#1016 := [unit-resolution #719 #1015]: #331
-#1026 := (or #305 #138 #125 #150 #152)
-#1049 := [hypothesis]: #112
-#307 := (or #305 #306)
-#666 := [asserted]: #307
-#1050 := [unit-resolution #666 #1049]: #306
-#544 := (or #150 #152 #143 #114)
-#153 := (or #143 #114)
-#154 := (or #152 #153)
-#155 := (or #150 #154)
-#545 := (iff #155 #544)
-#546 := [rewrite]: #545
-#533 := [asserted]: #155
-#547 := [mp #533 #546]: #544
-#1047 := [unit-resolution #547 #1050 #1052 #1051]: #143
-#342 := (or #338 #298)
-#692 := [asserted]: #342
-#1048 := [unit-resolution #692 #1047]: #298
-#308 := (or #305 #297)
-#667 := [asserted]: #308
-#1045 := [unit-resolution #667 #1049]: #297
-#341 := (or #338 #330)
-#691 := [asserted]: #341
-#1046 := [unit-resolution #691 #1047]: #330
-#1096 := [hypothesis]: #331
-#1063 := (or #277 #138 #136 #105 #107)
-#1083 := [hypothesis]: #87
-#1084 := [unit-resolution #647 #1083]: #236
-#1081 := [unit-resolution #788 #1084]: #47
-#1082 := [unit-resolution #623 #1081]: #214
-#1079 := [unit-resolution #769 #1082]: #20
-#1080 := [unit-resolution #607 #1079]: #219
-#1077 := [unit-resolution #619 #1081]: #240
-#1078 := [hypothesis]: #298
-#1075 := [hypothesis]: #297
-#1076 := [unit-resolution #621 #1081]: #241
-#1073 := [unit-resolution #645 #1083]: #276
-#1085 := (or #289 #85 #55 #138 #136)
-#1093 := [hypothesis]: #98
-#291 := (or #289 #290)
-#654 := [asserted]: #291
-#1094 := [unit-resolution #654 #1093]: #290
-#534 := (or #136 #138 #129 #100)
-#139 := (or #129 #100)
-#140 := (or #138 #139)
-#141 := (or #136 #140)
-#535 := (iff #141 #534)
-#536 := [rewrite]: #535
-#523 := [asserted]: #141
-#537 := [mp #523 #536]: #534
-#1091 := [unit-resolution #537 #1094 #1096 #1095]: #129
-#1092 := [hypothesis]: #241
-#1089 := [hypothesis]: #276
-#292 := (or #289 #281)
-#655 := [asserted]: #292
-#1090 := [unit-resolution #655 #1093]: #281
-#1087 := [unit-resolution #502 #1090 #1089 #1092]: #93
-#326 := (or #322 #282)
-#680 := [asserted]: #326
-#1088 := [unit-resolution #680 #1087 #1091]: false
-#1086 := [lemma #1088]: #1085
-#1074 := [unit-resolution #1086 #1073 #1076 #1096 #1095]: #289
-#509 := (or #105 #107 #98 #69)
-#108 := (or #98 #69)
-#109 := (or #107 #108)
-#110 := (or #105 #109)
-#510 := (iff #110 #509)
-#511 := [rewrite]: #510
-#498 := [asserted]: #110
-#512 := [mp #498 #511]: #509
-#1071 := [unit-resolution #512 #1074 #1075 #1078]: #69
-#257 := (not #69)
-#261 := (or #257 #248)
-#633 := [asserted]: #261
-#1072 := [unit-resolution #633 #1071]: #248
-#1069 := [unit-resolution #477 #1072 #1077 #1080]: #62
-#295 := (or #290 #249)
-#658 := [asserted]: #295
-#1070 := [unit-resolution #658 #1069]: #290
-#1067 := [unit-resolution #537 #1070 #1096 #1095]: #129
-#1068 := [unit-resolution #659 #1069]: #281
-#1065 := [unit-resolution #502 #1068 #1073 #1076]: #93
-#1066 := [unit-resolution #680 #1065 #1067]: false
-#1064 := [lemma #1066]: #1063
-#1043 := [unit-resolution #1064 #1046 #1096 #1045 #1048]: #277
-#1044 := [unit-resolution #527 #1043 #1154]: #123
-#325 := (or #322 #317)
-#679 := [asserted]: #325
-#1041 := [unit-resolution #679 #1044]: #322
-#1042 := [unit-resolution #537 #1041 #1096 #1046]: #100
-#1039 := [unit-resolution #654 #1042]: #289
-#1040 := [unit-resolution #512 #1039 #1045 #1048]: #69
-#1037 := [unit-resolution #633 #1040]: #248
-#1038 := [unit-resolution #658 #1042]: #249
-#294 := (or #290 #281)
-#657 := [asserted]: #294
-#1035 := [unit-resolution #657 #1042]: #281
-#329 := (or #317 #282)
-#683 := [asserted]: #329
-#1036 := [unit-resolution #683 #1044]: #282
-#1053 := (or #235 #62 #60)
-#1061 := [hypothesis]: #248
-#1062 := [hypothesis]: #249
-#1059 := [hypothesis]: #47
-#1060 := [unit-resolution #619 #1059]: #240
-#1057 := [unit-resolution #477 #1060 #1062 #1061]: #28
-#1058 := [unit-resolution #623 #1059]: #214
-#1055 := [unit-resolution #769 #1058]: #20
-#1056 := [unit-resolution #607 #1055 #1057]: false
-#1054 := [lemma #1056]: #1053
-#1033 := [unit-resolution #1054 #1038 #1037]: #235
-#1034 := [unit-resolution #788 #1033]: #49
-#279 := (or #276 #236)
-#646 := [asserted]: #279
-#1031 := [unit-resolution #646 #1034]: #276
-#1032 := [unit-resolution #502 #1031 #1036 #1035]: #55
-#242 := (or #240 #241)
-#618 := [asserted]: #242
-#1029 := [unit-resolution #618 #1032]: #240
-#1030 := [unit-resolution #477 #1029 #1038 #1037]: #28
-#246 := (or #241 #214)
-#622 := [asserted]: #246
-#1027 := [unit-resolution #622 #1032]: #214
-#1028 := [unit-resolution #769 #1027]: #20
-#1025 := [unit-resolution #607 #1028 #1030]: false
-#1023 := [lemma #1025]: #1026
-#1013 := [unit-resolution #1023 #1016 #1019 #1052 #1051]: #305
-#1014 := [unit-resolution #522 #1013 #1153]: #81
-#1097 := (or #272 #125 #76)
-#1124 := [hypothesis]: #81
-#1121 := [unit-resolution #643 #1124]: #233
-#1122 := [unit-resolution #452 #1121]: #38
-#1119 := [unit-resolution #612 #1122]: #223
-#273 := (or #272 #264)
-#642 := [asserted]: #273
-#1120 := [unit-resolution #642 #1124]: #264
-#1117 := [hypothesis]: #265
-#230 := (or #228 #229)
-#611 := [asserted]: #230
-#1118 := [unit-resolution #611 #1122]: #229
-#1115 := [unit-resolution #487 #1118 #1117 #1120]: #67
-#260 := (or #256 #224)
-#632 := [asserted]: #260
-#1116 := [unit-resolution #632 #1115]: #224
-#1113 := [unit-resolution #456 #1116 #1119]: #26
-#220 := (or #218 #219)
-#605 := [asserted]: #220
-#1114 := [unit-resolution #605 #1113]: #219
-#1111 := [unit-resolution #631 #1115]: #248
-#1112 := [unit-resolution #606 #1113]: #213
-#1109 := [unit-resolution #769 #1112]: #22
-#244 := (or #240 #214)
-#620 := [asserted]: #244
-#1110 := [unit-resolution #620 #1109]: #240
-#1107 := [unit-resolution #477 #1110 #1111 #1114]: #62
-#1108 := [unit-resolution #659 #1107]: #281
-#1105 := [unit-resolution #622 #1109]: #241
-#1106 := [unit-resolution #623 #1109]: #235
-#1103 := [unit-resolution #788 #1106]: #49
-#1104 := [unit-resolution #646 #1103]: #276
-#1101 := [unit-resolution #502 #1104 #1105 #1108]: #93
-#1102 := [unit-resolution #647 #1103]: #277
-#1099 := [unit-resolution #527 #1102 #1154]: #123
-#1100 := [unit-resolution #683 #1099 #1101]: false
-#1098 := [lemma #1100]: #1097
-#1011 := [unit-resolution #1098 #1014 #1019]: #76
-#311 := (or #306 #265)
-#670 := [asserted]: #311
-#1012 := [unit-resolution #670 #1011]: #306
-#1009 := [unit-resolution #547 #1012 #1052 #1051]: #143
-#1010 := [unit-resolution #692 #1009]: #298
-#312 := (or #297 #265)
-#671 := [asserted]: #312
-#1007 := [unit-resolution #671 #1011]: #297
-#1008 := [unit-resolution #691 #1009]: #330
-#1005 := [unit-resolution #1064 #1008 #1016 #1007 #1010]: #277
-#1006 := [unit-resolution #527 #1005 #1019]: #123
-#1003 := [unit-resolution #679 #1006]: #322
-#1004 := [unit-resolution #537 #1003 #1016 #1008]: #100
-#1001 := [unit-resolution #654 #1004]: #289
-#1002 := [unit-resolution #512 #1001 #1007 #1010]: #69
-#999 := [unit-resolution #633 #1002]: #248
-#1000 := [unit-resolution #658 #1004]: #249
-#997 := [unit-resolution #643 #1014]: #233
-#998 := [unit-resolution #452 #997]: #38
-#995 := [unit-resolution #612 #998]: #223
-#262 := (or #257 #224)
-#634 := [asserted]: #262
-#996 := [unit-resolution #634 #1002]: #224
-#993 := [unit-resolution #456 #996 #995]: #26
-#994 := [unit-resolution #605 #993]: #219
-#991 := [unit-resolution #477 #994 #1000 #999]: #53
-#992 := [unit-resolution #657 #1004]: #281
-#989 := [unit-resolution #683 #1006]: #282
-#990 := [unit-resolution #1054 #999 #1000]: #235
-#987 := [unit-resolution #788 #990]: #49
-#988 := [unit-resolution #646 #987]: #276
-#985 := [unit-resolution #502 #988 #989 #992]: #55
-#986 := [unit-resolution #618 #985 #991]: false
-#984 := [lemma #986]: #983
-#1162 := [unit-resolution #984 #1159 #1156 #1161]: #400
-#590 := (or #204 #200 #176)
-#205 := (or #200 #176)
-#206 := (or #204 #205)
-#591 := (iff #206 #590)
-#592 := [rewrite]: #591
-#583 := [asserted]: #206
-#593 := [mp #583 #592]: #590
-#1163 := [unit-resolution #593 #1162 #1160]: #204
-#404 := (not #204)
-#411 := (or #404 #380)
-#744 := [asserted]: #411
-#1164 := [unit-resolution #744 #1163]: #380
-decl f55 :: S1
-#180 := f55
-#181 := (= f55 f1)
-#379 := (not #181)
-#392 := (or #388 #379)
-#729 := [asserted]: #392
-#1165 := [unit-resolution #729 #1155]: #379
-decl f53 :: S1
-#173 := f53
-#174 := (= f53 f1)
-#371 := (not #174)
-#913 := (or #248 #181 #183 #150 #152 #119)
-#937 := [hypothesis]: #60
-#938 := [unit-resolution #631 #937]: #256
-#939 := (or #306 #67 #119)
-#971 := [hypothesis]: #256
-#950 := [hypothesis]: #114
-#947 := [unit-resolution #670 #950]: #265
-#948 := [unit-resolution #666 #950]: #305
-#945 := [unit-resolution #522 #948 #1153]: #81
-#946 := [unit-resolution #642 #945]: #264
-#943 := [unit-resolution #487 #946 #947 #971]: #40
-#944 := [unit-resolution #643 #945]: #233
-#941 := [unit-resolution #452 #944]: #38
-#942 := [unit-resolution #611 #941 #943]: false
-#940 := [lemma #942]: #939
-#935 := [unit-resolution #940 #938 #1153]: #306
-#936 := [unit-resolution #547 #935 #1052 #1051]: #143
-#933 := [unit-resolution #691 #936]: #330
-#934 := [unit-resolution #635 #937]: #224
-#952 := (or #223 #67 #119)
-#959 := [hypothesis]: #32
-#960 := [unit-resolution #612 #959]: #228
-#957 := [unit-resolution #452 #960]: #44
-#958 := [unit-resolution #643 #957]: #272
-#955 := [unit-resolution #522 #958 #1153]: #112
-#956 := [unit-resolution #613 #959]: #229
-#953 := [unit-resolution #644 #957]: #264
-#954 := [unit-resolution #487 #953 #956 #971]: #76
-#951 := [unit-resolution #668 #954 #955]: false
-#949 := [lemma #951]: #952
-#931 := [unit-resolution #949 #938 #1153]: #223
-#932 := [unit-resolution #456 #931 #934]: #26
-#929 := [unit-resolution #606 #932]: #213
-#930 := [unit-resolution #769 #929]: #22
-#927 := [unit-resolution #622 #930]: #241
-#928 := [unit-resolution #623 #930]: #235
-#925 := [unit-resolution #788 #928]: #49
-#926 := [unit-resolution #646 #925]: #276
-#961 := (or #297 #67 #119)
-#972 := [hypothesis]: #105
-#969 := [unit-resolution #671 #972]: #265
-#970 := [unit-resolution #667 #972]: #305
-#967 := [unit-resolution #522 #970 #1153]: #81
-#968 := [unit-resolution #642 #967]: #264
-#965 := [unit-resolution #487 #968 #969 #971]: #40
-#966 := [unit-resolution #643 #967]: #233
-#963 := [unit-resolution #452 #966]: #38
-#964 := [unit-resolution #611 #963 #965]: false
-#962 := [lemma #964]: #961
-#923 := [unit-resolution #962 #938 #1153]: #297
-#924 := [unit-resolution #633 #937]: #257
-#921 := [unit-resolution #692 #936]: #298
-#922 := [unit-resolution #512 #921 #924 #923]: #98
-#919 := [hypothesis]: #380
-#920 := [hypothesis]: #379
-#340 := (or #338 #339)
-#690 := [asserted]: #340
-#917 := [unit-resolution #690 #936]: #339
-#569 := (or #181 #183 #174 #145)
+#497 := [asserted]: #275
+#976 := [unit-resolution #497 #971]: #264
+#908 := (or #372 #74 #76 #105 #129 #181 #183)
+#879 := [hypothesis]: #176
+#377 := (or #372 #331)
+#571 := [asserted]: #377
+#880 := [unit-resolution #571 #879]: #331
+decl f42 :: S1
+#135 := f42
+#136 := (= f42 f1)
+#330 := (not #136)
+#373 := (or #371 #372)
+#567 := [asserted]: #373
+#884 := [unit-resolution #567 #879]: #371
+#823 := (or #181 #183 #174 #145)
#184 := (or #174 #145)
#185 := (or #183 #184)
#186 := (or #181 #185)
-#570 := (iff #186 #569)
-#571 := [rewrite]: #570
-#558 := [asserted]: #186
-#572 := [mp #558 #571]: #569
-#918 := [unit-resolution #572 #917 #920 #919]: #174
-#375 := (or #371 #331)
-#716 := [asserted]: #375
-#915 := [unit-resolution #716 #918]: #331
-#916 := [unit-resolution #1086 #915 #922 #926 #927 #933]: false
-#914 := [lemma #916]: #913
-#1166 := [unit-resolution #914 #1165 #1164 #1159 #1156 #1161]: #248
-#753 := (or #371 #150 #152 #119 #60)
-#793 := [hypothesis]: #174
-#374 := (or #371 #363)
-#715 := [asserted]: #374
-#794 := [unit-resolution #715 #793]: #363
-#791 := [unit-resolution #716 #793]: #331
-#802 := (or #236 #119 #150 #152 #138 #60 #167)
-#881 := [hypothesis]: #363
-#819 := [hypothesis]: #49
-#820 := [unit-resolution #647 #819]: #277
-#834 := (or #322 #167 #87)
-#849 := [hypothesis]: #129
-#324 := (or #322 #323)
-#678 := [asserted]: #324
-#850 := [unit-resolution #678 #849]: #323
-#847 := [unit-resolution #679 #849]: #317
-#848 := [unit-resolution #527 #847 #867]: #125
-#361 := (or #358 #318)
-#706 := [asserted]: #361
-#845 := [unit-resolution #706 #848]: #358
-#846 := [unit-resolution #562 #845 #881 #850]: #169
-#843 := [unit-resolution #707 #848]: #359
-#844 := [unit-resolution #573 #843]: #197
-#403 := (or #398 #364)
-#738 := [asserted]: #403
-#833 := [unit-resolution #738 #844 #846]: false
-#831 := [lemma #833]: #834
-#817 := [unit-resolution #831 #820 #881]: #322
-#818 := [unit-resolution #646 #819]: #276
-#851 := (or #282 #167 #87)
-#869 := [hypothesis]: #93
-#870 := [unit-resolution #682 #869]: #323
-#868 := [unit-resolution #683 #869]: #317
-#865 := [unit-resolution #527 #868 #867]: #125
-#866 := [unit-resolution #706 #865]: #358
-#863 := [unit-resolution #562 #866 #881 #870]: #169
-#864 := [unit-resolution #707 #865]: #359
-#861 := [unit-resolution #573 #864]: #197
-#862 := [unit-resolution #738 #861 #863]: false
-#852 := [lemma #862]: #851
-#815 := [unit-resolution #852 #820 #881]: #282
-#821 := (or #55 #138 #129 #150 #152 #93 #85 #60 #119)
-#832 := [hypothesis]: #322
-#829 := [hypothesis]: #282
-#830 := [unit-resolution #502 #1092 #829 #1089]: #91
-#827 := [unit-resolution #657 #830]: #290
-#891 := (or #67 #55 #85 #138 #60 #150 #152 #119)
-#911 := [unit-resolution #940 #971 #1153]: #306
-#912 := [unit-resolution #547 #911 #1052 #1051]: #143
-#909 := [unit-resolution #691 #912]: #330
-#910 := [unit-resolution #949 #971 #1153]: #223
-#907 := [unit-resolution #962 #971 #1153]: #297
-#908 := [unit-resolution #692 #912]: #298
-#905 := [unit-resolution #1086 #909 #1096 #1089 #1092]: #289
-#906 := [unit-resolution #512 #905 #908 #907]: #69
-#903 := [unit-resolution #634 #906]: #224
-#904 := [unit-resolution #456 #903 #910]: #26
-#901 := [unit-resolution #605 #904]: #219
-#902 := [unit-resolution #606 #904]: #213
-#899 := [unit-resolution #769 #902]: #22
-#900 := [unit-resolution #620 #899]: #240
-#897 := [unit-resolution #477 #900 #1061 #901]: #62
-#898 := [unit-resolution #658 #897]: #290
-#895 := [unit-resolution #537 #898 #1096 #909]: #129
-#896 := [unit-resolution #659 #897]: #281
-#893 := [unit-resolution #502 #896 #1092 #1089]: #93
-#894 := [unit-resolution #680 #893 #895]: false
-#892 := [lemma #894]: #891
-#828 := [unit-resolution #892 #1092 #1089 #1096 #1061 #1052 #1051 #1153]: #67
+#826 := (iff #186 #823)
+#817 := (or #183 #174 #145)
+#820 := (or #181 #817)
+#824 := (iff #820 #823)
+#825 := [rewrite]: #824
+#821 := (iff #186 #820)
+#818 := (iff #185 #817)
+#819 := [rewrite]: #818
+#822 := [monotonicity #819]: #821
+#827 := [trans #822 #825]: #826
+#447 := [asserted]: #186
+#828 := [mp #447 #827]: #823
+#885 := [unit-resolution #828 #884 #883 #882]: #145
+#343 := (or #339 #330)
+#546 := [asserted]: #343
+#886 := [unit-resolution #546 #885]: #330
+#755 := (or #136 #138 #129 #100)
+#139 := (or #129 #100)
+#140 := (or #138 #139)
+#141 := (or #136 #140)
+#758 := (iff #141 #755)
+#749 := (or #138 #129 #100)
+#752 := (or #136 #749)
+#756 := (iff #752 #755)
+#757 := [rewrite]: #756
+#753 := (iff #141 #752)
+#750 := (iff #140 #749)
+#751 := [rewrite]: #750
+#754 := [monotonicity #751]: #753
+#759 := [trans #754 #757]: #758
+#440 := [asserted]: #141
+#760 := [mp #440 #759]: #755
+#887 := [unit-resolution #760 #886 #881 #880]: #100
+#290 := (not #100)
+#295 := (or #290 #249)
+#511 := [asserted]: #295
+#888 := [unit-resolution #511 #887]: #249
+decl f23 :: S1
+#68 := f23
+#69 := (= f23 f1)
+#298 := (not #107)
+#344 := (or #339 #298)
+#547 := [asserted]: #344
+#889 := [unit-resolution #547 #885]: #298
+#890 := [hypothesis]: #297
+#291 := (or #289 #290)
+#507 := [asserted]: #291
+#891 := [unit-resolution #507 #887]: #289
+#711 := (or #105 #107 #98 #69)
+#108 := (or #98 #69)
+#109 := (or #107 #108)
+#110 := (or #105 #109)
+#714 := (iff #110 #711)
+#705 := (or #107 #98 #69)
+#708 := (or #105 #705)
+#712 := (iff #708 #711)
+#713 := [rewrite]: #712
+#709 := (iff #110 #708)
+#706 := (iff #109 #705)
+#707 := [rewrite]: #706
+#710 := [monotonicity #707]: #709
+#715 := [trans #710 #713]: #714
+#435 := [asserted]: #110
+#716 := [mp #435 #715]: #711
+#892 := [unit-resolution #716 #891 #890 #889]: #69
+#257 := (not #69)
+#261 := (or #257 #248)
+#486 := [asserted]: #261
+#893 := [unit-resolution #486 #892]: #248
+decl f12 :: S1
+#33 := f12
+#34 := (= f12 f1)
+#224 := (not #34)
+#262 := (or #257 #224)
+#487 := [asserted]: #262
+#894 := [unit-resolution #487 #892]: #224
+#895 := [hypothesis]: #265
+#896 := [hypothesis]: #264
#258 := (or #256 #257)
-#630 := [asserted]: #258
-#825 := [unit-resolution #630 #828]: #257
-#826 := [unit-resolution #655 #830]: #289
-#973 := (or #330 #69 #98 #150 #152)
-#981 := [hypothesis]: #136
-#982 := [unit-resolution #691 #981]: #338
-#979 := [unit-resolution #547 #982 #1052 #1051]: #114
-#977 := [hypothesis]: #257
-#345 := (or #330 #298)
-#695 := [asserted]: #345
-#978 := [unit-resolution #695 #981]: #298
-#975 := [unit-resolution #512 #978 #977 #980]: #105
-#310 := (or #306 #297)
-#669 := [asserted]: #310
-#976 := [unit-resolution #669 #975 #979]: false
-#974 := [lemma #976]: #973
-#823 := [unit-resolution #974 #826 #825 #1052 #1051]: #330
-#824 := [unit-resolution #537 #823 #827 #1096 #832]: false
-#822 := [lemma #824]: #821
-#816 := [unit-resolution #822 #817 #1096 #1052 #1051 #815 #818 #1061 #1153]: #55
-#813 := [unit-resolution #618 #816]: #240
-#814 := [unit-resolution #622 #816]: #214
-#811 := [unit-resolution #769 #814]: #20
-#812 := [unit-resolution #607 #811]: #219
-#809 := [unit-resolution #477 #812 #1061 #813]: #62
-#810 := [unit-resolution #658 #809]: #290
-#807 := [unit-resolution #537 #810 #1096 #817]: #136
-#808 := [unit-resolution #691 #807]: #338
-#805 := [unit-resolution #547 #808 #1052 #1051]: #114
-#293 := (or #289 #249)
-#656 := [asserted]: #293
-#806 := [unit-resolution #656 #809]: #289
-#803 := [unit-resolution #974 #807 #806 #1052 #1051]: #69
-#804 := [unit-resolution #630 #803]: #256
-#801 := [unit-resolution #940 #804 #805 #1153]: false
-#799 := [lemma #801]: #802
-#792 := [unit-resolution #799 #791 #1052 #1051 #1153 #1061 #794]: #236
-#789 := [unit-resolution #788 #792]: #47
-#790 := [unit-resolution #1054 #789 #1061]: #62
-#778 := [unit-resolution #658 #790]: #290
-#779 := [unit-resolution #656 #790]: #289
-#795 := (or #330 #119 #150 #152 #98)
-#800 := [unit-resolution #974 #981 #980 #1052 #1051]: #69
-#797 := [unit-resolution #630 #800]: #256
-#798 := [unit-resolution #940 #797 #979 #1153]: false
-#796 := [lemma #798]: #795
-#776 := [unit-resolution #796 #779 #1052 #1051 #1153]: #330
-#777 := [unit-resolution #537 #776 #791 #778]: #129
-#774 := [unit-resolution #831 #777 #794]: #87
-#775 := [unit-resolution #659 #790]: #281
-#772 := [unit-resolution #621 #789]: #241
-#773 := [unit-resolution #680 #777]: #282
-#770 := [unit-resolution #502 #773 #772 #775]: #85
-#771 := [unit-resolution #645 #770 #774]: false
-#751 := [lemma #771]: #753
-#1167 := [unit-resolution #751 #1159 #1156 #1161 #1166]: #371
-#1168 := [unit-resolution #572 #1167 #1165 #1164]: #145
-#1169 := [unit-resolution #690 #1168]: #338
-#1170 := [unit-resolution #547 #1169 #1159 #1156]: #114
-#1171 := [unit-resolution #669 #1170]: #297
-#344 := (or #339 #298)
-#694 := [asserted]: #344
-#1172 := [unit-resolution #694 #1168]: #298
-#1173 := [unit-resolution #940 #1170 #1161]: #67
-#1174 := [unit-resolution #630 #1173]: #257
-#1175 := [unit-resolution #512 #1174 #1172 #1171]: #98
-#1176 := [unit-resolution #656 #1175]: #249
-#1177 := [unit-resolution #632 #1173]: #224
-#1178 := [unit-resolution #666 #1170]: #305
-#1179 := [unit-resolution #522 #1178 #1161]: #81
-#1180 := [unit-resolution #643 #1179]: #233
-#1181 := [unit-resolution #452 #1180]: #38
-#1182 := [unit-resolution #612 #1181]: #223
-#1183 := [unit-resolution #456 #1182 #1177]: #26
-#1184 := [unit-resolution #605 #1183]: #219
-#1185 := [unit-resolution #477 #1184 #1166 #1176]: #53
-#1186 := [unit-resolution #606 #1183]: #213
-#1187 := [unit-resolution #769 #1186]: #22
-#1188 := [unit-resolution #620 #1187 #1185]: false
-#1190 := [lemma #1188]: #1189
-#1365 := [unit-resolution #1190 #1160]: #388
-#211 := (or #208 #190)
-decl f5 :: S1
-#13 := f5
-#14 := (= f5 f1)
-#600 := (or #14 #208 #190)
-#858 := (iff #600 #211)
-#853 := (or false #208 #190)
-#856 := (iff #853 #211)
-#857 := [rewrite]: #856
-#854 := (iff #600 #853)
-#757 := (iff #14 false)
-#15 := (not #14)
-#438 := [asserted]: #15
-#758 := [iff-false #438]: #757
-#855 := [monotonicity #758]: #854
-#859 := [trans #855 #857]: #858
-#212 := (or #14 #211)
-#601 := (iff #212 #600)
-#602 := [rewrite]: #601
-#589 := [asserted]: #212
-#603 := [mp #589 #602]: #600
-#860 := [mp #603 #859]: #211
-#1366 := [unit-resolution #860 #1365]: #208
-#408 := (not #208)
-#410 := (or #408 #380)
-#743 := [asserted]: #410
-#1367 := [unit-resolution #743 #1366]: #380
-#409 := (or #408 #404)
-#742 := [asserted]: #409
-#1368 := [unit-resolution #742 #1366]: #404
-#1369 := [unit-resolution #593 #1368 #1160]: #200
-#1239 := (or #119 #183 #400)
-#1224 := [unit-resolution #1123 #1153 #1019]: #323
-#1225 := [unit-resolution #562 #1224 #1017 #1020]: #167
-#1226 := [unit-resolution #715 #1225]: #371
-#1222 := (or #379 #400 #119)
-#1216 := [hypothesis]: #181
-#390 := (or #387 #379)
-#727 := [asserted]: #390
-#1217 := [unit-resolution #727 #1216]: #387
-#1218 := [unit-resolution #842 #1217]: #157
-#394 := (or #379 #347)
-#731 := [asserted]: #394
-#1219 := [unit-resolution #731 #1216]: #347
-#1220 := [unit-resolution #984 #1219 #1024 #1153]: #150
-#1221 := [unit-resolution #702 #1220 #1218]: false
-#1223 := [lemma #1221]: #1222
-#1227 := [unit-resolution #1223 #1153 #1024]: #379
-#1228 := [unit-resolution #572 #1227 #1226 #919]: #145
-#1229 := [unit-resolution #694 #1228]: #298
-#1192 := (or #297 #125 #119)
-#1191 := [unit-resolution #1098 #967 #969 #1154]: false
-#1193 := [lemma #1191]: #1192
-#1230 := [unit-resolution #1193 #1153 #1019]: #297
-#1231 := [unit-resolution #719 #1225]: #331
-#343 := (or #339 #330)
-#693 := [asserted]: #343
-#1232 := [unit-resolution #693 #1228]: #330
-#1233 := [unit-resolution #1064 #1232 #1231 #1230 #1229]: #277
-#1234 := [unit-resolution #527 #1233 #1019]: #123
-#1214 := (or #339 #138 #119 #125 #98)
-#1194 := [hypothesis]: #145
-#1195 := [unit-resolution #693 #1194]: #330
-#1196 := [unit-resolution #694 #1194]: #298
-#1197 := [unit-resolution #1193 #1153 #1154]: #297
-#1198 := [unit-resolution #1064 #1195 #1096 #1197 #1196]: #277
-#1199 := [unit-resolution #527 #1198 #1154]: #123
-#1200 := [unit-resolution #679 #1199]: #322
-#1201 := [unit-resolution #537 #1200 #1096 #1195]: #100
-#1202 := [unit-resolution #658 #1201]: #249
-#1203 := [unit-resolution #512 #1196 #1197 #980]: #69
-#1204 := [unit-resolution #633 #1203]: #248
-#1205 := [unit-resolution #634 #1203]: #224
-#1206 := [unit-resolution #630 #1203]: #256
-#1207 := [unit-resolution #949 #1206 #1153]: #223
-#1208 := [unit-resolution #456 #1207 #1205]: #26
-#1209 := [unit-resolution #605 #1208]: #219
-#1210 := [unit-resolution #477 #1209 #1204 #1202]: #53
-#1211 := [unit-resolution #606 #1208]: #213
-#1212 := [unit-resolution #769 #1211]: #22
-#1213 := [unit-resolution #620 #1212 #1210]: false
-#1215 := [lemma #1213]: #1214
-#1235 := [unit-resolution #1215 #1228 #1153 #1019 #1231]: #98
-#1236 := [unit-resolution #654 #1235]: #290
-#1237 := [unit-resolution #537 #1236 #1231 #1232]: #129
-#1238 := [unit-resolution #679 #1237 #1234]: false
-#1240 := [lemma #1238]: #1239
-#1370 := [unit-resolution #1240 #1367 #1369]: #119
-#1371 := [unit-resolution #703 #1370]: #354
-#1372 := [unit-resolution #842 #1371]: #188
-#1373 := [unit-resolution #727 #1372]: #379
-#1374 := [unit-resolution #737 #1369]: #364
-#1375 := [unit-resolution #736 #1369]: #398
-#1376 := [unit-resolution #573 #1375]: #163
-#1377 := [unit-resolution #705 #1376]: #358
-#1378 := [unit-resolution #707 #1376]: #318
-#391 := (or #387 #347)
-#728 := [asserted]: #391
-#1379 := [unit-resolution #728 #1372]: #347
+#483 := [asserted]: #258
+#897 := [unit-resolution #483 #892]: #256
+#667 := (or #74 #76 #67 #40)
+#77 := (or #67 #40)
+#78 := (or #76 #77)
+#79 := (or #74 #78)
+#670 := (iff #79 #667)
+#661 := (or #76 #67 #40)
+#664 := (or #74 #661)
+#668 := (iff #664 #667)
+#669 := [rewrite]: #668
+#665 := (iff #79 #664)
+#662 := (iff #78 #661)
+#663 := [rewrite]: #662
+#666 := [monotonicity #663]: #665
+#671 := [trans #666 #669]: #670
+#430 := [asserted]: #79
+#672 := [mp #430 #671]: #667
+#898 := [unit-resolution #672 #897 #896 #895]: #40
+#232 := (or #229 #223)
+#466 := [asserted]: #232
+#899 := [unit-resolution #466 #898]: #223
+#613 := (or #32 #34 #26)
+#35 := (or #34 #26)
+#36 := (or #32 #35)
+#614 := (iff #36 #613)
+#615 := [rewrite]: #614
+#423 := [asserted]: #36
+#616 := [mp #423 #615]: #613
+#900 := [unit-resolution #616 #899 #894]: #26
+#901 := [unit-resolution #458 #900]: #219
+#902 := [unit-resolution #648 #901 #893 #888]: #53
+#903 := [unit-resolution #459 #900]: #213
+#906 := [unit-resolution #905 #903]: #22
+#907 := [unit-resolution #473 #906 #902]: false
+#909 := [lemma #907]: #908
+#977 := [unit-resolution #909 #976 #975 #974 #881 #883 #882]: #372
+#849 := (or #204 #200 #176)
+#205 := (or #200 #176)
+#206 := (or #204 #205)
+#850 := (iff #206 #849)
+#851 := [rewrite]: #850
+#452 := [asserted]: #206
+#852 := [mp #452 #851]: #849
+#978 := [unit-resolution #852 #977 #969]: #200
+#402 := (or #400 #364)
+#590 := [asserted]: #402
+#979 := [unit-resolution #590 #978]: #364
+decl f49 :: S1
+#160 := f49
+#161 := (= f49 f1)
+#358 := (not #161)
+#401 := (or #400 #398)
+#589 := [asserted]: #401
+#980 := [unit-resolution #589 #978]: #398
+#198 := (or #197 #163)
+#450 := [asserted]: #198
+#981 := [unit-resolution #450 #980]: #163
+#360 := (or #358 #359)
+#558 := [asserted]: #360
+#982 := [unit-resolution #558 #981]: #358
+#323 := (not #131)
+decl f38 :: S1
+#122 := f38
+#123 := (= f38 f1)
+#362 := (or #359 #318)
+#560 := [asserted]: #362
+#983 := [unit-resolution #560 #981]: #318
+#946 := (or #256 #105 #129 #181 #183 #161 #169 #125)
+#931 := [hypothesis]: #364
+#932 := [hypothesis]: #358
+#910 := [hypothesis]: #318
+#933 := [hypothesis]: #67
+#259 := (or #256 #248)
+#484 := [asserted]: #259
+#934 := [unit-resolution #484 #933]: #248
+#929 := (or #323 #60 #125)
+#317 := (not #123)
+#911 := [hypothesis]: #131
+#327 := (or #323 #317)
+#534 := [asserted]: #327
+#912 := [unit-resolution #534 #911]: #317
+#733 := (or #123 #125 #87)
+#126 := (or #125 #87)
+#127 := (or #123 #126)
+#734 := (iff #127 #733)
+#735 := [rewrite]: #734
+#438 := [asserted]: #127
+#736 := [mp #438 #735]: #733
+#913 := [unit-resolution #736 #912 #910]: #87
+#280 := (or #277 #236)
+#500 := [asserted]: #280
+#914 := [unit-resolution #500 #913]: #236
+#917 := [unit-resolution #916 #914]: #47
+#243 := (or #240 #235)
+#472 := [asserted]: #243
+#918 := [unit-resolution #472 #917]: #240
+#328 := (or #323 #282)
+#535 := [asserted]: #328
+#920 := [unit-resolution #535 #911]: #282
+#278 := (or #276 #277)
+#498 := [asserted]: #278
+#921 := [unit-resolution #498 #913]: #276
+#245 := (or #241 #235)
+#474 := [asserted]: #245
+#922 := [unit-resolution #474 #917]: #241
+#687 := (or #91 #93 #85 #55)
+#94 := (or #85 #55)
+#95 := (or #93 #94)
+#96 := (or #91 #95)
+#690 := (iff #96 #687)
+#681 := (or #93 #85 #55)
+#684 := (or #91 #681)
+#688 := (iff #684 #687)
+#689 := [rewrite]: #688
+#685 := (iff #96 #684)
+#682 := (iff #95 #681)
+#683 := [rewrite]: #682
+#686 := [monotonicity #683]: #685
+#691 := [trans #686 #689]: #690
+#433 := [asserted]: #96
+#692 := [mp #433 #691]: #687
+#923 := [unit-resolution #692 #922 #921 #920]: #91
+#924 := [unit-resolution #512 #923]: #249
+#925 := [unit-resolution #476 #917]: #214
+#926 := [unit-resolution #905 #925]: #20
+#222 := (or #219 #213)
+#460 := [asserted]: #222
+#927 := [unit-resolution #460 #926]: #219
+#928 := [unit-resolution #648 #927 #924 #919 #918]: false
+#930 := [lemma #928]: #929
+#935 := [unit-resolution #930 #934 #910]: #323
+#799 := (or #167 #169 #161 #131)
+#170 := (or #161 #131)
+#171 := (or #169 #170)
+#172 := (or #167 #171)
+#802 := (iff #172 #799)
+#793 := (or #169 #161 #131)
+#796 := (or #167 #793)
+#800 := (iff #796 #799)
+#801 := [rewrite]: #800
+#797 := (iff #172 #796)
+#794 := (iff #171 #793)
+#795 := [rewrite]: #794
+#798 := [monotonicity #795]: #797
+#803 := [trans #798 #801]: #802
+#445 := [asserted]: #172
+#804 := [mp #445 #803]: #799
+#936 := [unit-resolution #804 #935 #932 #931]: #167
+#363 := (not #167)
+#378 := (or #363 #331)
+#572 := [asserted]: #378
+#937 := [unit-resolution #572 #936]: #331
+#374 := (or #371 #363)
+#568 := [asserted]: #374
+#938 := [unit-resolution #568 #936]: #371
+#939 := [unit-resolution #828 #938 #883 #882]: #145
+#940 := [unit-resolution #546 #939]: #330
+#941 := [unit-resolution #760 #940 #881 #937]: #100
+#942 := [unit-resolution #483 #933]: #257
+#943 := [unit-resolution #547 #939]: #298
+#944 := [unit-resolution #716 #943 #890 #942]: #98
+#945 := [unit-resolution #507 #944 #941]: false
+#947 := [lemma #945]: #946
+#984 := [unit-resolution #947 #974 #881 #883 #882 #982 #979 #983]: #256
+#985 := [unit-resolution #672 #984 #976 #975]: #40
+#986 := [unit-resolution #466 #985]: #223
+#967 := (or #60 #32 #105 #129 #181 #183 #161 #169 #125)
+#948 := [unit-resolution #930 #919 #910]: #323
+#949 := [unit-resolution #804 #948 #932 #931]: #167
+#950 := [unit-resolution #572 #949]: #331
+#951 := [unit-resolution #568 #949]: #371
+#952 := [unit-resolution #828 #951 #883 #882]: #145
+#953 := [unit-resolution #546 #952]: #330
+#954 := [unit-resolution #760 #953 #881 #950]: #100
+#955 := [unit-resolution #511 #954]: #249
+#956 := [hypothesis]: #223
+#957 := [unit-resolution #547 #952]: #298
+#958 := [unit-resolution #507 #954]: #289
+#959 := [unit-resolution #716 #958 #890 #957]: #69
+#960 := [unit-resolution #487 #959]: #224
+#961 := [unit-resolution #616 #960 #956]: #26
+#962 := [unit-resolution #458 #961]: #219
+#963 := [unit-resolution #648 #962 #919 #955]: #53
+#964 := [unit-resolution #459 #961]: #213
+#965 := [unit-resolution #905 #964]: #22
+#966 := [unit-resolution #473 #965 #963]: false
+#968 := [lemma #966]: #967
+#987 := [unit-resolution #968 #986 #974 #881 #883 #882 #982 #979 #983]: #60
+#263 := (or #248 #224)
+#488 := [asserted]: #263
+#988 := [unit-resolution #488 #987]: #224
+#989 := [unit-resolution #616 #988 #986]: #26
+#990 := [unit-resolution #459 #989]: #213
+#991 := [unit-resolution #905 #990]: #22
+#992 := [unit-resolution #476 #991]: #235
+#993 := [unit-resolution #916 #992]: #49
+#994 := [unit-resolution #500 #993]: #277
+#995 := [unit-resolution #736 #994 #983]: #123
+#996 := [unit-resolution #534 #995]: #323
+#997 := [unit-resolution #804 #996 #982 #979]: #167
+#998 := [unit-resolution #568 #997]: #371
+#999 := [unit-resolution #828 #998 #883 #882]: #145
+#1000 := [unit-resolution #572 #997]: #331
+#1001 := [unit-resolution #499 #993]: #276
+#1002 := [unit-resolution #475 #991]: #241
+#329 := (or #317 #282)
+#536 := [asserted]: #329
+#1003 := [unit-resolution #536 #995]: #282
+#1004 := [unit-resolution #692 #1003 #1002 #1001]: #91
+#294 := (or #290 #281)
+#510 := [asserted]: #294
+#1005 := [unit-resolution #510 #1004]: #290
+#1006 := [unit-resolution #760 #1005 #881 #1000]: #136
+#1007 := [unit-resolution #546 #1006 #999]: false
+#1009 := [lemma #1007]: #1008
+#1072 := [unit-resolution #1009 #970 #883 #882 #969 #881]: #233
+#45 := (or #44 #38)
+#425 := [asserted]: #45
+#1073 := [unit-resolution #425 #1072]: #38
+#231 := (or #228 #223)
+#465 := [asserted]: #231
+#1075 := [unit-resolution #465 #1073]: #223
+#1100 := (or #60 #119 #129 #181 #183 #204)
+#230 := (or #228 #229)
+#464 := [asserted]: #230
+#1074 := [unit-resolution #464 #1073]: #229
+#1086 := (or #125 #129 #119 #60 #181 #183 #204)
+#1023 := [unit-resolution #930 #910 #919]: #323
+#1020 := (or #371 #131 #204)
+#1010 := [hypothesis]: #174
+#1011 := [unit-resolution #567 #1010]: #372
+#1012 := [unit-resolution #852 #1011 #969]: #200
+#1013 := [unit-resolution #589 #1012]: #398
+#1014 := [unit-resolution #450 #1013]: #163
+#1015 := [unit-resolution #568 #1010]: #363
+#1016 := [hypothesis]: #323
+#1017 := [unit-resolution #590 #1012]: #364
+#1018 := [unit-resolution #804 #1017 #1016 #1015]: #161
+#1019 := [unit-resolution #558 #1018 #1014]: false
+#1021 := [lemma #1019]: #1020
+#1069 := [unit-resolution #1021 #1023 #969]: #371
+#1070 := [unit-resolution #828 #1069 #883 #882]: #145
+#1071 := [unit-resolution #546 #1070]: #330
+#1076 := [unit-resolution #547 #1070]: #298
+#1067 := (or #290 #60 #32 #119 #107 #40)
+#1057 := [hypothesis]: #100
+#1058 := [unit-resolution #511 #1057]: #249
+#1045 := [hypothesis]: #298
+#1059 := [unit-resolution #507 #1057]: #289
+#1055 := (or #224 #40 #119 #107 #98)
+#1044 := [hypothesis]: #289
+#1046 := [hypothesis]: #34
+#1047 := [unit-resolution #487 #1046]: #257
+#1048 := [unit-resolution #716 #1047 #1045 #1044]: #105
+#1049 := [unit-resolution #520 #1048]: #305
+#1050 := [unit-resolution #732 #1049 #970]: #81
+#260 := (or #256 #224)
+#485 := [asserted]: #260
+#1051 := [unit-resolution #485 #1046]: #256
+#312 := (or #297 #265)
+#524 := [asserted]: #312
+#1052 := [unit-resolution #524 #1048]: #265
+#1053 := [unit-resolution #672 #1052 #1030 #1051]: #74
+#273 := (or #272 #264)
+#495 := [asserted]: #273
+#1054 := [unit-resolution #495 #1053 #1050]: false
+#1056 := [lemma #1054]: #1055
+#1060 := [unit-resolution #1056 #1059 #970 #1045 #1030]: #224
+#1061 := [unit-resolution #616 #1060 #956]: #26
+#1062 := [unit-resolution #458 #1061]: #219
+#1063 := [unit-resolution #648 #1062 #919 #1058]: #53
+#1064 := [unit-resolution #459 #1061]: #213
+#1065 := [unit-resolution #905 #1064]: #22
+#1066 := [unit-resolution #473 #1065 #1063]: false
+#1068 := [lemma #1066]: #1067
+#1077 := [unit-resolution #1068 #1076 #1075 #970 #919 #1074]: #290
+#1078 := [unit-resolution #760 #1077 #881 #1071]: #138
+#1079 := [unit-resolution #571 #1078]: #372
+#1080 := [unit-resolution #852 #1079 #969]: #200
+#1081 := [unit-resolution #589 #1080]: #398
+#1082 := [unit-resolution #450 #1081]: #163
+#1083 := [unit-resolution #590 #1080]: #364
+#1042 := (or #161 #60 #32 #40 #129 #136 #119 #169 #181 #183 #125)
+#1022 := [hypothesis]: #330
+#1024 := [unit-resolution #804 #932 #1023 #931]: #167
+#1025 := [unit-resolution #572 #1024]: #331
+#1026 := [unit-resolution #760 #1025 #881 #1022]: #100
+#1027 := [unit-resolution #511 #1026]: #249
+#1028 := [unit-resolution #968 #932 #956 #881 #883 #882 #919 #931 #910]: #105
+#1029 := [unit-resolution #524 #1028]: #265
+#1031 := [unit-resolution #520 #1028]: #305
+#1032 := [unit-resolution #732 #1031 #970]: #81
+#1033 := [unit-resolution #495 #1032]: #264
+#1034 := [unit-resolution #672 #1033 #1030 #1029]: #67
+#1035 := [unit-resolution #485 #1034]: #224
+#1036 := [unit-resolution #616 #1035 #956]: #26
+#1037 := [unit-resolution #458 #1036]: #219
+#1038 := [unit-resolution #648 #1037 #919 #1027]: #53
+#1039 := [unit-resolution #459 #1036]: #213
+#1040 := [unit-resolution #905 #1039]: #22
+#1041 := [unit-resolution #473 #1040 #1038]: false
+#1043 := [lemma #1041]: #1042
+#1084 := [unit-resolution #1043 #1083 #1075 #1074 #881 #1071 #970 #919 #883 #882 #910]: #161
+#1085 := [unit-resolution #558 #1084 #1082]: false
+#1087 := [lemma #1085]: #1086
+#1088 := [unit-resolution #1087 #919 #970 #881 #883 #882 #969]: #125
+#1089 := [unit-resolution #560 #1088]: #359
+#1090 := [unit-resolution #450 #1089]: #197
+#1091 := [unit-resolution #589 #1090]: #400
+#1092 := [unit-resolution #852 #1091 #969]: #176
+#1093 := [unit-resolution #567 #1092]: #371
+#1094 := [unit-resolution #828 #1093 #883 #882]: #145
+#1095 := [unit-resolution #547 #1094]: #298
+#1096 := [unit-resolution #571 #1092]: #331
+#1097 := [unit-resolution #546 #1094]: #330
+#1098 := [unit-resolution #760 #1097 #881 #1096]: #100
+#1099 := [unit-resolution #1068 #1098 #1095 #1075 #970 #919 #1074]: false
+#1101 := [lemma #1099]: #1100
+#1125 := [unit-resolution #1101 #970 #881 #883 #882 #969]: #60
+#1126 := [unit-resolution #488 #1125]: #224
+#1127 := [unit-resolution #616 #1126 #1075]: #26
+#1128 := [unit-resolution #459 #1127]: #213
+#1129 := [unit-resolution #905 #1128]: #22
+#1130 := [unit-resolution #476 #1129]: #235
+#1131 := [unit-resolution #916 #1130]: #49
+#1132 := [unit-resolution #500 #1131]: #277
+#1133 := [unit-resolution #475 #1129]: #241
+#1134 := [unit-resolution #499 #1131]: #276
+#1135 := [unit-resolution #484 #1125]: #256
+#1109 := (or #297 #40 #67 #119)
+#1102 := [hypothesis]: #105
+#1103 := [unit-resolution #520 #1102]: #305
+#1104 := [unit-resolution #732 #1103 #970]: #81
+#1105 := [hypothesis]: #256
+#1106 := [unit-resolution #524 #1102]: #265
+#1107 := [unit-resolution #672 #1106 #1030 #1105]: #74
+#1108 := [unit-resolution #495 #1107 #1104]: false
+#1110 := [lemma #1108]: #1109
+#1136 := [unit-resolution #1110 #1074 #1135 #970]: #297
+#1137 := [unit-resolution #486 #1125]: #257
+#1123 := (or #317 #69 #105 #181 #183 #85 #55 #204)
+#1111 := [hypothesis]: #257
+#1112 := [hypothesis]: #241
+#1113 := [hypothesis]: #276
+#1114 := [hypothesis]: #123
+#1115 := [unit-resolution #536 #1114]: #282
+#1116 := [unit-resolution #692 #1115 #1113 #1112]: #91
+#292 := (or #289 #281)
+#508 := [asserted]: #292
+#1117 := [unit-resolution #508 #1116]: #289
+#1118 := [unit-resolution #534 #1114]: #323
+#1119 := [unit-resolution #1021 #1118 #969]: #371
+#1120 := [unit-resolution #828 #1119 #883 #882]: #145
+#1121 := [unit-resolution #547 #1120]: #298
+#1122 := [unit-resolution #716 #1121 #1117 #1111 #890]: false
+#1124 := [lemma #1122]: #1123
+#1138 := [unit-resolution #1124 #1137 #1136 #883 #882 #1134 #1133 #969]: #317
+#1139 := [unit-resolution #736 #1138 #1132]: #125
+#1140 := [unit-resolution #560 #1139]: #359
+#1141 := [unit-resolution #450 #1140]: #197
+#1142 := [unit-resolution #589 #1141]: #400
+#1143 := [unit-resolution #852 #1142 #969]: #176
+#1144 := [unit-resolution #571 #1143]: #331
+#1145 := [unit-resolution #567 #1143]: #371
+#1146 := [unit-resolution #828 #1145 #883 #882]: #145
+#1147 := [unit-resolution #546 #1146]: #330
+#1148 := [unit-resolution #760 #1147 #881 #1144]: #100
+#1149 := [unit-resolution #547 #1146]: #298
+#1150 := [unit-resolution #716 #1149 #1137 #1136]: #98
+#1151 := [unit-resolution #507 #1150 #1148]: false
+#1153 := [lemma #1151]: #1152
+#1195 := [unit-resolution #1153 #883 #881 #882 #969]: #119
#357 := (or #346 #313)
-#704 := [asserted]: #357
-#1380 := [unit-resolution #704 #1370]: #346
-#1351 := (or #98 #125 #161 #169 #181 #183 #150 #152)
-#1258 := [hypothesis]: #364
-#1259 := [hypothesis]: #358
-#1332 := (or #136 #150 #152 #181 #183 #125 #161 #169 #98)
-#1317 := (or #129 #125 #136 #161 #169 #181 #183 #150 #152 #98)
-#1297 := (or #105 #125 #98 #161 #169 #181 #183 #129 #136)
-#1276 := (or #290 #125 #161 #169 #181 #183 #98 #105)
-#1256 := [hypothesis]: #100
-#1257 := [unit-resolution #657 #1256]: #281
-#1260 := [unit-resolution #658 #1256]: #249
-#1254 := (or #60 #62 #91 #125)
-#1241 := [hypothesis]: #281
-#1242 := [unit-resolution #1054 #1061 #1062]: #235
-#1243 := [unit-resolution #788 #1242]: #49
-#1244 := [unit-resolution #646 #1243]: #276
-#1245 := [unit-resolution #647 #1243]: #277
-#1246 := [unit-resolution #527 #1245 #1154]: #123
-#1247 := [unit-resolution #683 #1246]: #282
-#1248 := [unit-resolution #502 #1247 #1244 #1241]: #55
-#1249 := [unit-resolution #618 #1248]: #240
-#1250 := [unit-resolution #477 #1249 #1061 #1062]: #28
-#1251 := [unit-resolution #622 #1248]: #214
-#1252 := [unit-resolution #769 #1251]: #20
-#1253 := [unit-resolution #607 #1252 #1250]: false
-#1255 := [lemma #1253]: #1254
-#1261 := [unit-resolution #1255 #1260 #1257 #1154]: #60
-#1262 := [unit-resolution #633 #1261]: #257
-#1263 := [unit-resolution #512 #1262 #980 #1075]: #107
-#1264 := [unit-resolution #694 #1263]: #339
-#1265 := [unit-resolution #572 #1264 #920 #919]: #174
-#1266 := [unit-resolution #715 #1265]: #363
-#1267 := [unit-resolution #562 #1266 #1259 #1258]: #131
-#1268 := [unit-resolution #682 #1267]: #282
-#1269 := [unit-resolution #681 #1267]: #317
-#1270 := [unit-resolution #527 #1269 #1154]: #87
-#1271 := [unit-resolution #645 #1270]: #276
-#1272 := [unit-resolution #502 #1271 #1268 #1257]: #55
-#1273 := [unit-resolution #647 #1270]: #236
-#1274 := [unit-resolution #788 #1273]: #47
-#1275 := [unit-resolution #621 #1274 #1272]: false
+#557 := [asserted]: #357
+#1196 := [unit-resolution #557 #1195]: #346
+decl f44 :: S1
+#142 := f44
+#143 := (= f44 f1)
+#338 := (not #143)
+#1207 := (or #60 #204 #181 #183 #40 #129 #152)
+#1165 := (or #331 #60 #204)
+#1154 := [hypothesis]: #138
+#1155 := [unit-resolution #571 #1154]: #372
+#1156 := [unit-resolution #852 #1155 #969]: #200
+#1157 := [unit-resolution #589 #1156]: #398
+#1158 := [unit-resolution #450 #1157]: #163
+#1159 := [unit-resolution #560 #1158]: #318
+#1160 := [unit-resolution #590 #1156]: #364
+#1161 := [unit-resolution #572 #1154]: #363
+#1162 := [unit-resolution #558 #1158]: #358
+#1163 := [unit-resolution #804 #1162 #1161 #1160]: #131
+#1164 := [unit-resolution #930 #1163 #1159 #919]: false
+#1166 := [lemma #1164]: #1165
+#1197 := [unit-resolution #1166 #919 #969]: #331
+#1193 := (or #339 #60 #40 #129 #138 #150 #152)
+#1167 := [hypothesis]: #331
+#1168 := [hypothesis]: #145
+#1169 := [unit-resolution #546 #1168]: #330
+#1170 := [unit-resolution #760 #1169 #881 #1167]: #100
+#1171 := [unit-resolution #511 #1170]: #249
+#1173 := [hypothesis]: #346
+#340 := (or #338 #339)
+#543 := [asserted]: #340
+#1174 := [unit-resolution #543 #1168]: #338
+#779 := (or #150 #152 #143 #114)
+#153 := (or #143 #114)
+#154 := (or #152 #153)
+#155 := (or #150 #154)
+#782 := (iff #155 #779)
+#773 := (or #152 #143 #114)
+#776 := (or #150 #773)
+#780 := (iff #776 #779)
+#781 := [rewrite]: #780
+#777 := (iff #155 #776)
+#774 := (iff #154 #773)
+#775 := [rewrite]: #774
+#778 := [monotonicity #775]: #777
+#783 := [trans #778 #781]: #782
+#442 := [asserted]: #155
+#784 := [mp #442 #783]: #779
+#1175 := [unit-resolution #784 #1174 #1173 #1172]: #114
+#306 := (not #114)
+#310 := (or #306 #297)
+#522 := [asserted]: #310
+#1176 := [unit-resolution #522 #1175]: #297
+#1177 := [unit-resolution #547 #1168]: #298
+#1178 := [unit-resolution #507 #1170]: #289
+#1179 := [unit-resolution #716 #1178 #1177 #1176]: #69
+#1180 := [unit-resolution #487 #1179]: #224
+#311 := (or #306 #265)
+#523 := [asserted]: #311
+#1181 := [unit-resolution #523 #1175]: #265
+#1182 := [unit-resolution #483 #1179]: #256
+#1183 := [unit-resolution #672 #1182 #1030 #1181]: #74
+#1184 := [unit-resolution #497 #1183]: #233
+#1185 := [unit-resolution #425 #1184]: #38
+#1186 := [unit-resolution #465 #1185]: #223
+#1187 := [unit-resolution #616 #1186 #1180]: #26
+#1188 := [unit-resolution #458 #1187]: #219
+#1189 := [unit-resolution #648 #1188 #919 #1171]: #53
+#1190 := [unit-resolution #459 #1187]: #213
+#1191 := [unit-resolution #905 #1190]: #22
+#1192 := [unit-resolution #473 #1191 #1189]: false
+#1194 := [lemma #1192]: #1193
+#1198 := [unit-resolution #1194 #919 #1030 #881 #1197 #1196 #1172]: #339
+#1199 := [unit-resolution #828 #1198 #883 #882]: #174
+#1200 := [unit-resolution #567 #1199]: #372
+#1201 := [unit-resolution #852 #1200 #969]: #200
+#1202 := [unit-resolution #589 #1201]: #398
+#1203 := [unit-resolution #1021 #1199 #969]: #131
+#1204 := [unit-resolution #930 #1203 #919]: #125
+#1205 := [unit-resolution #560 #1204]: #359
+#1206 := [unit-resolution #450 #1205 #1202]: false
+#1208 := [lemma #1206]: #1207
+#1261 := [unit-resolution #1208 #1030 #883 #882 #969 #881 #1172]: #60
+#1262 := [unit-resolution #486 #1261]: #257
+#1218 := (or #281 #69 #150 #152 #129 #138)
+#1209 := [hypothesis]: #91
+#1210 := [unit-resolution #510 #1209]: #290
+#1211 := [unit-resolution #760 #1210 #881 #1167]: #136
+#341 := (or #338 #330)
+#544 := [asserted]: #341
+#1212 := [unit-resolution #544 #1211]: #338
+#1213 := [unit-resolution #784 #1212 #1173 #1172]: #114
+#1214 := [unit-resolution #508 #1209]: #289
+#345 := (or #330 #298)
+#548 := [asserted]: #345
+#1215 := [unit-resolution #548 #1211]: #298
+#1216 := [unit-resolution #716 #1215 #1111 #1214]: #105
+#1217 := [unit-resolution #522 #1216 #1213]: false
+#1219 := [lemma #1217]: #1218
+#1263 := [unit-resolution #1219 #1167 #1196 #1172 #881 #1262]: #281
+#1259 := (or #371 #91 #204)
+#1249 := [unit-resolution #1021 #1010 #969]: #131
+#1250 := [unit-resolution #535 #1249]: #282
+#1236 := [hypothesis]: #281
+#1251 := [unit-resolution #534 #1249]: #317
+#1252 := [unit-resolution #560 #1014]: #318
+#1253 := [unit-resolution #736 #1252 #1251]: #87
+#1254 := [unit-resolution #498 #1253]: #276
+#1255 := [unit-resolution #692 #1254 #1236 #1250]: #55
+#1256 := [unit-resolution #500 #1253]: #236
+#1257 := [unit-resolution #916 #1256]: #47
+#1258 := [unit-resolution #474 #1257 #1255]: false
+#1260 := [lemma #1258]: #1259
+#1264 := [unit-resolution #1260 #1263 #969]: #371
+#1265 := [unit-resolution #828 #1264 #883 #882]: #145
+#1266 := [unit-resolution #543 #1265]: #338
+#1267 := [unit-resolution #784 #1266 #1196 #1172]: #114
+#1268 := [unit-resolution #484 #1261]: #256
+#1269 := [unit-resolution #488 #1261]: #224
+#1247 := (or #330 #91 #34 #204 #40 #67 #181 #183 #150 #152)
+#1220 := [hypothesis]: #224
+#1221 := [hypothesis]: #136
+#1222 := [unit-resolution #544 #1221]: #338
+#1223 := [unit-resolution #784 #1222 #1173 #1172]: #114
+#1224 := [unit-resolution #523 #1223]: #265
+#1225 := [unit-resolution #672 #1224 #1030 #1105]: #74
+#1226 := [unit-resolution #497 #1225]: #233
+#1227 := [unit-resolution #425 #1226]: #38
+#1228 := [unit-resolution #465 #1227]: #223
+#1229 := [unit-resolution #616 #1228 #1220]: #26
+#1230 := [unit-resolution #459 #1229]: #213
+#1231 := [unit-resolution #905 #1230]: #22
+#1232 := [unit-resolution #546 #1221]: #339
+#1233 := [unit-resolution #828 #1232 #883 #882]: #174
+#1234 := [unit-resolution #1021 #1233 #969]: #131
+#1235 := [unit-resolution #535 #1234]: #282
+#1237 := [unit-resolution #534 #1234]: #317
+#1238 := [unit-resolution #567 #1233]: #372
+#1239 := [unit-resolution #852 #1238 #969]: #200
+#1240 := [unit-resolution #589 #1239]: #398
+#1241 := [unit-resolution #450 #1240]: #163
+#1242 := [unit-resolution #560 #1241]: #318
+#1243 := [unit-resolution #736 #1242 #1237]: #87
+#1244 := [unit-resolution #498 #1243]: #276
+#1245 := [unit-resolution #692 #1244 #1236 #1235]: #55
+#1246 := [unit-resolution #475 #1245 #1231]: false
+#1248 := [lemma #1246]: #1247
+#1270 := [unit-resolution #1248 #1263 #1269 #969 #1030 #1268 #883 #882 #1196 #1172]: #330
+#1271 := [unit-resolution #760 #1270 #881 #1167]: #100
+#1272 := [unit-resolution #507 #1271]: #289
+#1273 := [unit-resolution #547 #1265]: #298
+#1274 := [unit-resolution #716 #1273 #1262 #1272]: #105
+#1275 := [unit-resolution #522 #1274 #1267]: false
#1277 := [lemma #1275]: #1276
-#1278 := [unit-resolution #1277 #1075 #1259 #1258 #920 #919 #980 #1154]: #290
-#1279 := [unit-resolution #537 #1278 #832 #1095]: #138
-#1280 := [unit-resolution #716 #1279]: #371
-#1281 := [unit-resolution #572 #1280 #920 #919]: #145
-#1282 := [unit-resolution #694 #1281]: #298
-#1283 := [unit-resolution #512 #1282 #980 #1075]: #69
-#1284 := [unit-resolution #633 #1283]: #248
-#1285 := [unit-resolution #719 #1279]: #363
-#1286 := [unit-resolution #562 #1285 #1259 #1258]: #131
-#1287 := [unit-resolution #681 #1286]: #317
-#1288 := [unit-resolution #527 #1287 #1154]: #87
-#1289 := [unit-resolution #647 #1288]: #236
-#1290 := [unit-resolution #788 #1289]: #47
-#1291 := [unit-resolution #1054 #1290 #1284]: #62
-#1292 := [unit-resolution #645 #1288]: #276
-#1293 := [unit-resolution #682 #1286]: #282
-#1294 := [unit-resolution #621 #1290]: #241
-#1295 := [unit-resolution #502 #1294 #1293 #1292]: #91
-#1296 := [unit-resolution #659 #1295 #1291]: false
-#1298 := [lemma #1296]: #1297
-#1299 := [unit-resolution #1298 #832 #980 #1259 #1258 #920 #919 #1154 #1095]: #105
-#1300 := [unit-resolution #669 #1299]: #306
-#1301 := [unit-resolution #547 #1300 #1052 #1051]: #143
-#1302 := [unit-resolution #690 #1301]: #339
-#1303 := [unit-resolution #572 #1302 #920 #919]: #174
-#1304 := [unit-resolution #716 #1303]: #331
-#1305 := [unit-resolution #537 #1304 #832 #1095]: #100
-#1306 := [unit-resolution #657 #1305]: #281
-#1307 := [unit-resolution #715 #1303]: #363
-#1308 := [unit-resolution #562 #1307 #1259 #1258]: #131
-#1309 := [unit-resolution #682 #1308]: #282
-#1310 := [unit-resolution #681 #1308]: #317
-#1311 := [unit-resolution #527 #1310 #1154]: #87
-#1312 := [unit-resolution #645 #1311]: #276
-#1313 := [unit-resolution #502 #1312 #1309 #1306]: #55
-#1314 := [unit-resolution #647 #1311]: #236
-#1315 := [unit-resolution #788 #1314]: #47
-#1316 := [unit-resolution #621 #1315 #1313]: false
-#1318 := [lemma #1316]: #1317
-#1319 := [unit-resolution #1318 #1095 #1154 #1259 #1258 #920 #919 #1052 #1051 #980]: #129
-#1320 := [unit-resolution #678 #1319]: #323
-#1321 := [unit-resolution #562 #1320 #1259 #1258]: #167
-#1322 := [unit-resolution #715 #1321]: #371
-#1323 := [unit-resolution #572 #1322 #920 #919]: #145
-#1324 := [unit-resolution #690 #1323]: #338
-#1325 := [unit-resolution #547 #1324 #1052 #1051]: #114
-#1326 := [unit-resolution #679 #1319]: #317
-#1327 := [unit-resolution #527 #1326 #1154]: #87
-#335 := (or #331 #322)
-#687 := [asserted]: #335
-#1328 := [unit-resolution #687 #1319]: #331
-#1329 := [unit-resolution #694 #1323]: #298
-#1330 := [unit-resolution #1064 #1329 #1095 #1328 #1327]: #105
-#1331 := [unit-resolution #669 #1330 #1325]: false
-#1333 := [lemma #1331]: #1332
-#1334 := [unit-resolution #1333 #980 #1051 #920 #919 #1154 #1259 #1258 #1052]: #136
-#1335 := [unit-resolution #974 #1334 #980 #1052 #1051]: #69
-#1336 := [unit-resolution #633 #1335]: #248
-#1337 := [unit-resolution #693 #1334]: #339
-#1338 := [unit-resolution #572 #1337 #920 #919]: #174
-#1339 := [unit-resolution #715 #1338]: #363
-#1340 := [unit-resolution #562 #1339 #1259 #1258]: #131
-#1341 := [unit-resolution #681 #1340]: #317
-#1342 := [unit-resolution #527 #1341 #1154]: #87
-#1343 := [unit-resolution #647 #1342]: #236
-#1344 := [unit-resolution #788 #1343]: #47
-#1345 := [unit-resolution #1054 #1344 #1336]: #62
-#1346 := [unit-resolution #645 #1342]: #276
-#1347 := [unit-resolution #682 #1340]: #282
-#1348 := [unit-resolution #621 #1344]: #241
-#1349 := [unit-resolution #502 #1348 #1347 #1346]: #91
-#1350 := [unit-resolution #659 #1349 #1345]: false
-#1352 := [lemma #1350]: #1351
-#1381 := [unit-resolution #1352 #1378 #1377 #1374 #1373 #1367 #1380 #1379]: #98
-#1382 := [unit-resolution #654 #1381]: #290
-#1363 := (or #317 #100 #181 #183 #161 #169)
-#1353 := [hypothesis]: #123
-#1354 := [unit-resolution #681 #1353]: #323
-#1355 := [unit-resolution #562 #1354 #1259 #1258]: #167
-#1356 := [unit-resolution #715 #1355]: #371
-#1357 := [unit-resolution #572 #1356 #920 #919]: #145
-#1358 := [unit-resolution #679 #1353]: #322
-#1359 := [hypothesis]: #290
-#1360 := [unit-resolution #719 #1355]: #331
-#1361 := [unit-resolution #537 #1360 #1359 #1358]: #136
-#1362 := [unit-resolution #693 #1361 #1357]: false
-#1364 := [lemma #1362]: #1363
-#1383 := [unit-resolution #1364 #1382 #1373 #1367 #1377 #1374]: #317
-#1384 := [unit-resolution #527 #1383 #1378]: #87
-#1385 := [unit-resolution #645 #1384]: #276
-#1386 := [unit-resolution #655 #1381]: #281
-#1387 := [unit-resolution #647 #1384]: #236
-#1388 := [unit-resolution #788 #1387]: #47
-#1389 := [unit-resolution #621 #1388]: #241
-#1390 := [unit-resolution #502 #1389 #1386 #1385]: #93
-#1391 := [unit-resolution #682 #1390]: #323
-#1392 := [unit-resolution #562 #1391 #1377 #1374]: #167
-#1393 := [unit-resolution #715 #1392]: #371
-#1394 := [unit-resolution #572 #1393 #1373 #1367]: #145
-#1395 := [unit-resolution #680 #1390]: #322
-#1396 := [unit-resolution #719 #1392]: #331
-#1397 := [unit-resolution #537 #1396 #1382 #1395]: #136
-#1398 := [unit-resolution #693 #1397 #1394]: false
-#1399 := [lemma #1398]: #176
-#376 := (or #372 #363)
-#717 := [asserted]: #376
-#1426 := [unit-resolution #717 #1399]: #363
-#1428 := [unit-resolution #831 #1426]: #1427
-#1429 := [unit-resolution #1428 #867]: #322
-#1431 := (or #136 #129 #100)
-#377 := (or #372 #331)
-#718 := [asserted]: #377
-#1430 := [unit-resolution #718 #1399]: #331
-#1432 := [unit-resolution #537 #1430]: #1431
-#1433 := [unit-resolution #1432 #1429 #1095]: #100
-#1434 := [unit-resolution #657 #1433]: #281
-#1435 := (or #282 #87)
-#1436 := [unit-resolution #852 #1426]: #1435
-#1437 := [unit-resolution #1436 #867]: #282
-#1419 := (or #214 #93 #91)
-#1413 := [hypothesis]: #22
-#1414 := [unit-resolution #622 #1413]: #241
-#1415 := [unit-resolution #502 #1414 #829 #1241]: #85
-#1416 := [unit-resolution #623 #1413]: #235
-#1417 := [unit-resolution #788 #1416]: #49
-#1418 := [unit-resolution #646 #1417 #1415]: false
-#1420 := [lemma #1418]: #1419
-#1438 := [unit-resolution #1420 #1437 #1434]: #214
-#1439 := [unit-resolution #769 #1438]: #20
-#1440 := [unit-resolution #607 #1439]: #219
-#1441 := [unit-resolution #658 #1433]: #249
-#1442 := [unit-resolution #606 #1439]: #218
-#1424 := (or #248 #26 #98)
-#1421 := [hypothesis]: #218
-#1411 := (or #223 #98 #69 #67)
-#1400 := [unit-resolution #949 #959 #971]: #119
-#1401 := [unit-resolution #703 #1400]: #354
-#1402 := [unit-resolution #842 #1401]: #188
-#1403 := [unit-resolution #728 #1402]: #347
-#1404 := [unit-resolution #704 #1400]: #346
-#1405 := [unit-resolution #487 #953 #971 #956]: #76
-#1406 := [unit-resolution #670 #1405]: #306
-#1407 := [unit-resolution #547 #1406 #1404 #1403]: #143
-#1408 := [unit-resolution #671 #1405]: #297
-#1409 := [unit-resolution #512 #1408 #980 #977]: #107
-#1410 := [unit-resolution #692 #1409 #1407]: false
-#1412 := [lemma #1410]: #1411
-#1422 := [unit-resolution #1412 #924 #980 #938]: #223
-#1423 := [unit-resolution #456 #1422 #934 #1421]: false
-#1425 := [lemma #1423]: #1424
-#1443 := [unit-resolution #1425 #1442 #980]: #248
-#1444 := [unit-resolution #477 #1443 #1441 #1440]: #53
-#1445 := [unit-resolution #618 #1444]: #241
-#1446 := [unit-resolution #1054 #1443 #1441]: #235
-#1447 := [unit-resolution #788 #1446]: #49
-#1448 := [unit-resolution #646 #1447]: #276
-#1449 := [unit-resolution #502 #1448 #1445 #1437 #1434]: false
-#1451 := [lemma #1449]: #1450
-#1452 := [unit-resolution #1451 #1095 #980]: #87
-#1453 := [unit-resolution #647 #1452]: #236
-#1454 := [unit-resolution #788 #1453]: #47
-#1455 := [unit-resolution #623 #1454]: #214
-#1456 := [unit-resolution #769 #1455]: #20
-#1457 := [unit-resolution #606 #1456]: #218
-#1458 := [unit-resolution #1425 #1457 #980]: #248
-#1459 := [unit-resolution #1054 #1458 #1454]: #62
-#1460 := [unit-resolution #658 #1459]: #290
-#1461 := [unit-resolution #1432 #1460 #1095]: #129
-#1462 := [unit-resolution #621 #1454]: #241
-#1463 := [unit-resolution #645 #1452]: #276
-#1464 := [unit-resolution #659 #1459]: #281
-#1465 := [unit-resolution #502 #1464 #1463 #1462]: #93
-#1466 := [unit-resolution #680 #1465 #1461]: false
-#1468 := [lemma #1466]: #1467
-#1481 := [unit-resolution #1468 #980]: #136
-#1482 := [unit-resolution #693 #1481]: #339
-#1479 := (or #387 #145)
-#1469 := [hypothesis]: #188
-#1470 := [unit-resolution #726 #1469]: #388
-#1471 := [unit-resolution #860 #1470]: #208
-#1472 := [hypothesis]: #339
-#1473 := [unit-resolution #727 #1469]: #379
-#1475 := (or #181 #183 #145)
-#373 := (or #371 #372)
-#714 := [asserted]: #373
-#1474 := [unit-resolution #714 #1399]: #371
-#1476 := [unit-resolution #572 #1474]: #1475
-#1477 := [unit-resolution #1476 #1473 #1472]: #183
-#1478 := [unit-resolution #743 #1477 #1471]: false
-#1480 := [lemma #1478]: #1479
-#1483 := [unit-resolution #1480 #1482]: #387
-#1484 := [unit-resolution #842 #1483]: #157
-#1485 := [unit-resolution #702 #1484]: #346
-#1486 := [unit-resolution #703 #1484]: #313
-#1487 := [unit-resolution #796 #1486 #1481 #1485 #980]: #152
-#1488 := [unit-resolution #730 #1487]: #388
-#1489 := [unit-resolution #860 #1488]: #208
-#1490 := [unit-resolution #731 #1487]: #379
-#1491 := [unit-resolution #1476 #1490 #1482]: #183
-#1492 := [unit-resolution #743 #1491 #1489]: false
-#1493 := [lemma #1492]: #98
-#1515 := [unit-resolution #656 #1493]: #249
-#1511 := [unit-resolution #655 #1493]: #281
-#1512 := [unit-resolution #1420 #829 #1511]: #214
-#1513 := [unit-resolution #769 #1512]: #20
-#1514 := [unit-resolution #607 #1513]: #219
-#1516 := [unit-resolution #606 #1513]: #218
-#1509 := (or #248 #26)
-#1494 := [unit-resolution #654 #1493]: #290
-#1495 := [unit-resolution #1432 #1095 #1494]: #129
-#300 := (or #297 #289)
-#661 := [asserted]: #300
-#1496 := [unit-resolution #661 #1493]: #297
-#302 := (or #298 #289)
-#663 := [asserted]: #302
-#1497 := [unit-resolution #663 #1493]: #298
-#1498 := (or #277 #136 #105 #107)
-#1499 := [unit-resolution #1064 #1430]: #1498
-#1500 := [unit-resolution #1499 #1095 #1497 #1496]: #277
-#1501 := [unit-resolution #1428 #1500 #1495]: false
-#1502 := [lemma #1501]: #136
-#1503 := [unit-resolution #693 #1502]: #339
-#1504 := [unit-resolution #1480 #1503]: #387
-#1505 := [unit-resolution #842 #1504]: #157
-#1506 := [unit-resolution #703 #1505]: #313
-#1507 := [unit-resolution #949 #938 #1506]: #223
-#1508 := [unit-resolution #456 #1507 #934 #1421]: false
-#1510 := [lemma #1508]: #1509
-#1517 := [unit-resolution #1510 #1516]: #248
-#1518 := [unit-resolution #477 #1517 #1515 #1514]: #53
-#1519 := [unit-resolution #618 #1518]: #241
-#1520 := [unit-resolution #1054 #1517 #1515]: #235
-#1521 := [unit-resolution #788 #1520]: #49
-#1522 := [unit-resolution #646 #1521]: #276
-#1523 := [unit-resolution #502 #1522 #1519 #1511 #829]: false
-#1524 := [lemma #1523]: #93
-#1525 := [unit-resolution #1436 #1524]: #87
-#321 := (or #318 #277)
-#677 := [asserted]: #321
-#1526 := [unit-resolution #677 #1525]: #318
-#1527 := [unit-resolution #1255 #1526 #1511 #1515]: #60
-#1528 := [unit-resolution #1510 #1527]: #26
-#1529 := [unit-resolution #647 #1525]: #236
-#1530 := [unit-resolution #788 #1529]: #47
-#1531 := [unit-resolution #623 #1530]: #214
-#1532 := [unit-resolution #769 #1531]: #20
-[unit-resolution #606 #1532 #1528]: false
+#1278 := [unit-resolution #1277 #1030 #883 #882 #969 #881 #1172]: #138
+#1279 := [unit-resolution #571 #1278]: #372
+#1280 := [unit-resolution #852 #1279 #969]: #200
+#1281 := [unit-resolution #590 #1280]: #364
+#1282 := [unit-resolution #572 #1278]: #363
+#1283 := [unit-resolution #589 #1280]: #398
+#1284 := [unit-resolution #450 #1283]: #163
+#1285 := [unit-resolution #558 #1284]: #358
+#1286 := [unit-resolution #804 #1285 #1282 #1281]: #131
+#1287 := [unit-resolution #535 #1286]: #282
+#375 := (or #371 #331)
+#569 := [asserted]: #375
+#1288 := [unit-resolution #569 #1278]: #371
+#1289 := [unit-resolution #828 #1288 #883 #882]: #145
+#1290 := [unit-resolution #547 #1289]: #298
+#1291 := [unit-resolution #543 #1289]: #338
+#1292 := [unit-resolution #784 #1291 #1196 #1172]: #114
+#1293 := [unit-resolution #522 #1292]: #297
+#1294 := [unit-resolution #716 #1293 #1262 #1290]: #98
+#1295 := [unit-resolution #508 #1294]: #281
+#1296 := [unit-resolution #560 #1284]: #318
+#1297 := [unit-resolution #534 #1286]: #317
+#1298 := [unit-resolution #736 #1297 #1296]: #87
+#1299 := [unit-resolution #498 #1298]: #276
+#1300 := [unit-resolution #692 #1299 #1295 #1287]: #55
+#1301 := [unit-resolution #500 #1298]: #236
+#1302 := [unit-resolution #916 #1301]: #47
+#1303 := [unit-resolution #474 #1302 #1300]: false
+#1305 := [lemma #1303]: #1304
+#1306 := [unit-resolution #1305 #1172 #969 #883 #882 #881]: #40
+#270 := (or #265 #229)
+#493 := [asserted]: #270
+#1307 := [unit-resolution #493 #1306]: #265
+#268 := (or #264 #229)
+#491 := [asserted]: #268
+#1308 := [unit-resolution #491 #1306]: #264
+#1309 := [unit-resolution #784 #1174 #1196 #1172]: #114
+#1310 := [unit-resolution #522 #1309]: #297
+#1311 := [unit-resolution #909 #1310 #1308 #1307 #881 #883 #882]: #372
+#1312 := [unit-resolution #852 #1311 #969]: #200
+#1313 := [unit-resolution #589 #1312]: #398
+#1314 := [unit-resolution #450 #1313]: #163
+#1315 := [unit-resolution #560 #1314]: #318
+#1316 := [unit-resolution #590 #1312]: #364
+#1317 := [unit-resolution #558 #1314]: #358
+#1318 := [unit-resolution #466 #1306]: #223
+#1319 := [unit-resolution #968 #1315 #1317 #881 #883 #882 #1316 #1310 #1318]: #60
+#1320 := [unit-resolution #486 #1319]: #257
+#1321 := [unit-resolution #716 #1320 #1310 #1177]: #98
+#1322 := [unit-resolution #507 #1321]: #290
+#1323 := [unit-resolution #760 #1322 #881 #1169]: #138
+#1324 := [unit-resolution #572 #1323]: #363
+#1325 := [unit-resolution #804 #1324 #1317 #1316]: #131
+#1326 := [unit-resolution #534 #1325]: #317
+#1327 := [unit-resolution #488 #1319]: #224
+#1328 := [unit-resolution #616 #1327 #1318]: #26
+#1329 := [unit-resolution #459 #1328]: #213
+#1330 := [unit-resolution #905 #1329]: #22
+#1331 := [unit-resolution #476 #1330]: #235
+#1332 := [unit-resolution #916 #1331]: #49
+#1333 := [unit-resolution #500 #1332]: #277
+#1334 := [unit-resolution #736 #1333 #1326 #1315]: false
+#1336 := [lemma #1334]: #1335
+#1344 := [unit-resolution #1336 #1342 #881 #882 #1341 #1343]: #339
+#1345 := [unit-resolution #828 #1344 #1342 #882]: #174
+#1346 := [unit-resolution #567 #1345]: #372
+#1347 := [unit-resolution #852 #1346 #1341]: #200
+#1348 := [unit-resolution #589 #1347]: #398
+#1349 := [unit-resolution #450 #1348]: #163
+#1350 := [unit-resolution #1021 #1345 #1341]: #131
+#1351 := [unit-resolution #569 #1345]: #331
+#1352 := [unit-resolution #1153 #1342 #881 #882 #1341]: #119
+#1353 := [unit-resolution #557 #1352]: #346
+#1354 := [unit-resolution #1260 #1345 #1341]: #91
+#1355 := [unit-resolution #1219 #1354 #1353 #1343 #881 #1351]: #69
+#1356 := [unit-resolution #486 #1355]: #248
+#1357 := [unit-resolution #930 #1356 #1350]: #125
+#1358 := [unit-resolution #560 #1357 #1349]: false
+#1360 := [lemma #1358]: #1359
+#1496 := [unit-resolution #1360 #882 #881]: #387
+#194 := (or #188 #157)
+decl f6 :: S1
+#16 := f6
+#17 := (= f6 f1)
+#18 := (not #17)
+#420 := [asserted]: #18
+#841 := (or #17 #188 #157)
+#195 := (or #17 #194)
+#842 := (iff #195 #841)
+#843 := [rewrite]: #842
+#449 := [asserted]: #195
+#844 := [mp #449 #843]: #841
+#1497 := [unit-resolution #844 #420]: #194
+#1498 := [unit-resolution #1497 #1496]: #157
+#356 := (or #354 #313)
+#556 := [asserted]: #356
+#1499 := [unit-resolution #556 #1498]: #313
+#355 := (or #354 #346)
+#555 := [asserted]: #355
+#1564 := [unit-resolution #555 #1498]: #346
+#1503 := (or #347 #129 #183)
+#1493 := [hypothesis]: #152
+#393 := (or #388 #347)
+#583 := [asserted]: #393
+#1494 := [unit-resolution #583 #1493]: #388
+#1495 := [unit-resolution #1339 #1494]: #208
+#394 := (or #379 #347)
+#584 := [asserted]: #394
+#1500 := [unit-resolution #584 #1493]: #379
+#1501 := [unit-resolution #1153 #1500 #881 #882 #1499]: #204
+#1502 := [unit-resolution #595 #1501 #1495]: false
+#1504 := [lemma #1502]: #1503
+#1565 := [unit-resolution #1504 #882 #881]: #347
+#1491 := (or #152 #129 #138 #150 #119)
+#1476 := (or #40 #129 #138 #150 #152 #119)
+#1455 := (or #60 #129 #138 #150 #152 #119)
+#1431 := (or #40 #119 #150 #152 #129 #138 #60)
+#1382 := (or #289 #60 #40 #119 #150 #152 #129 #138)
+#1361 := [hypothesis]: #98
+#293 := (or #289 #249)
+#509 := [asserted]: #293
+#1362 := [unit-resolution #509 #1361]: #249
+#1363 := [unit-resolution #507 #1361]: #290
+#1364 := [unit-resolution #760 #1363 #881 #1167]: #136
+#1365 := [unit-resolution #544 #1364]: #338
+#1366 := [unit-resolution #784 #1365 #1173 #1172]: #114
+#307 := (or #305 #306)
+#519 := [asserted]: #307
+#1367 := [unit-resolution #519 #1366]: #305
+#1368 := [unit-resolution #732 #1367 #970]: #81
+#1369 := [unit-resolution #496 #1368]: #233
+#1370 := [unit-resolution #425 #1369]: #38
+#1371 := [unit-resolution #465 #1370]: #223
+#1372 := [unit-resolution #523 #1366]: #265
+#1373 := [unit-resolution #495 #1368]: #264
+#1374 := [unit-resolution #672 #1373 #1030 #1372]: #67
+#1375 := [unit-resolution #485 #1374]: #224
+#1376 := [unit-resolution #616 #1375 #1371]: #26
+#1377 := [unit-resolution #458 #1376]: #219
+#1378 := [unit-resolution #648 #1377 #919 #1362]: #53
+#1379 := [unit-resolution #459 #1376]: #213
+#1380 := [unit-resolution #905 #1379]: #22
+#1381 := [unit-resolution #473 #1380 #1378]: false
+#1383 := [lemma #1381]: #1382
+#1417 := [unit-resolution #1383 #1030 #919 #970 #1173 #1172 #881 #1167]: #289
+#1415 := (or #290 #60 #40 #119 #150 #152 #98)
+#1395 := (or #107 #40 #98 #119 #60 #290)
+#1384 := [unit-resolution #1068 #1045 #970 #919 #1057 #1030]: #32
+#1385 := [unit-resolution #465 #1384]: #228
+#1386 := [unit-resolution #425 #1385]: #44
+#1387 := [unit-resolution #496 #1386]: #272
+#1388 := [unit-resolution #732 #1387 #970]: #112
+#1389 := [unit-resolution #520 #1388]: #297
+#1390 := [unit-resolution #716 #1389 #1044 #1045]: #69
+#1391 := [unit-resolution #497 #1386]: #264
+#1392 := [unit-resolution #521 #1388]: #265
+#1393 := [unit-resolution #672 #1392 #1030 #1391]: #67
+#1394 := [unit-resolution #483 #1393 #1390]: false
+#1396 := [lemma #1394]: #1395
+#1397 := [unit-resolution #1396 #1057 #1044 #970 #919 #1030]: #107
+#342 := (or #338 #298)
+#545 := [asserted]: #342
+#1398 := [unit-resolution #545 #1397]: #338
+#1399 := [unit-resolution #784 #1398 #1173 #1172]: #114
+#1400 := [unit-resolution #523 #1399]: #265
+#1401 := [unit-resolution #519 #1399]: #305
+#1402 := [unit-resolution #732 #1401 #970]: #81
+#1403 := [unit-resolution #495 #1402]: #264
+#1404 := [unit-resolution #672 #1403 #1030 #1400]: #67
+#1405 := [unit-resolution #485 #1404]: #224
+#1406 := [unit-resolution #496 #1402]: #233
+#1407 := [unit-resolution #425 #1406]: #38
+#1408 := [unit-resolution #465 #1407]: #223
+#1409 := [unit-resolution #616 #1408 #1405]: #26
+#1410 := [unit-resolution #458 #1409]: #219
+#1411 := [unit-resolution #648 #1410 #919 #1058]: #53
+#1412 := [unit-resolution #459 #1409]: #213
+#1413 := [unit-resolution #905 #1412]: #22
+#1414 := [unit-resolution #473 #1413 #1411]: false
+#1416 := [lemma #1414]: #1415
+#1418 := [unit-resolution #1416 #1030 #919 #970 #1173 #1172 #1417]: #290
+#1419 := [unit-resolution #760 #1418 #881 #1167]: #136
+#1420 := [unit-resolution #544 #1419]: #338
+#1421 := [unit-resolution #784 #1420 #1173 #1172]: #114
+#1422 := [unit-resolution #523 #1421]: #265
+#1423 := [unit-resolution #519 #1421]: #305
+#1424 := [unit-resolution #732 #1423 #970]: #81
+#1425 := [unit-resolution #495 #1424]: #264
+#1426 := [unit-resolution #548 #1419]: #298
+#1427 := [unit-resolution #522 #1421]: #297
+#1428 := [unit-resolution #716 #1427 #1417 #1426]: #69
+#1429 := [unit-resolution #483 #1428]: #256
+#1430 := [unit-resolution #672 #1429 #1425 #1030 #1422]: false
+#1432 := [lemma #1430]: #1431
+#1433 := [unit-resolution #1432 #919 #1173 #1172 #881 #1167 #970]: #40
+#1434 := [unit-resolution #464 #1433]: #228
+#1435 := [unit-resolution #425 #1434]: #44
+#1436 := [unit-resolution #496 #1435]: #272
+#1437 := [unit-resolution #732 #1436 #970]: #112
+#1438 := [unit-resolution #519 #1437]: #306
+#1439 := [unit-resolution #784 #1438 #1173 #1172]: #143
+#1440 := [unit-resolution #544 #1439]: #330
+#1441 := [unit-resolution #760 #1440 #881 #1167]: #100
+#1442 := [unit-resolution #511 #1441]: #249
+#1443 := [unit-resolution #466 #1433]: #223
+#1444 := [unit-resolution #545 #1439]: #298
+#1445 := [unit-resolution #520 #1437]: #297
+#1446 := [unit-resolution #507 #1441]: #289
+#1447 := [unit-resolution #716 #1446 #1445 #1444]: #69
+#1448 := [unit-resolution #487 #1447]: #224
+#1449 := [unit-resolution #616 #1448 #1443]: #26
+#1450 := [unit-resolution #458 #1449]: #219
+#1451 := [unit-resolution #648 #1450 #919 #1442]: #53
+#1452 := [unit-resolution #459 #1449]: #213
+#1453 := [unit-resolution #905 #1452]: #22
+#1454 := [unit-resolution #473 #1453 #1451]: false
+#1456 := [lemma #1454]: #1455
+#1465 := [unit-resolution #1456 #1172 #1167 #1173 #881 #970]: #60
+#1466 := [unit-resolution #484 #1465]: #256
+#1463 := (or #306 #67 #40 #119)
+#1457 := [hypothesis]: #114
+#1458 := [unit-resolution #519 #1457]: #305
+#1459 := [unit-resolution #732 #1458 #970]: #81
+#1460 := [unit-resolution #523 #1457]: #265
+#1461 := [unit-resolution #672 #1460 #1105 #1030]: #74
+#1462 := [unit-resolution #495 #1461 #1459]: false
+#1464 := [lemma #1462]: #1463
+#1467 := [unit-resolution #1464 #1030 #1466 #970]: #306
+#1468 := [unit-resolution #784 #1467 #1173 #1172]: #143
+#1469 := [unit-resolution #544 #1468]: #330
+#1470 := [unit-resolution #760 #1469 #881 #1167]: #100
+#1471 := [unit-resolution #1110 #1030 #970 #1466]: #297
+#1472 := [unit-resolution #486 #1465]: #257
+#1473 := [unit-resolution #545 #1468]: #298
+#1474 := [unit-resolution #716 #1473 #1472 #1471]: #98
+#1475 := [unit-resolution #507 #1474 #1470]: false
+#1477 := [lemma #1475]: #1476
+#1478 := [unit-resolution #1477 #1172 #1167 #1173 #881 #970]: #40
+#1479 := [unit-resolution #464 #1478]: #228
+#1480 := [unit-resolution #425 #1479]: #44
+#1481 := [unit-resolution #496 #1480]: #272
+#1482 := [unit-resolution #732 #1481 #970]: #112
+#1483 := [unit-resolution #519 #1482]: #306
+#1484 := [unit-resolution #784 #1483 #1173 #1172]: #143
+#1485 := [unit-resolution #544 #1484]: #330
+#1486 := [unit-resolution #760 #1485 #881 #1167]: #100
+#1487 := [unit-resolution #520 #1482]: #297
+#1488 := [unit-resolution #545 #1484]: #298
+#1489 := [unit-resolution #716 #1488 #1472 #1487]: #98
+#1490 := [unit-resolution #507 #1489 #1486]: false
+#1492 := [lemma #1490]: #1491
+#1566 := [unit-resolution #1492 #1565 #881 #1564 #1499]: #138
+#1567 := [unit-resolution #571 #1566]: #372
+#1568 := [unit-resolution #569 #1566]: #371
+#1562 := (or #40 #183 #150 #152 #119 #331)
+#1505 := [unit-resolution #569 #1154]: #371
+#1531 := (or #60 #119 #40 #150 #152 #183 #331)
+#1506 := [unit-resolution #1166 #919 #1154]: #204
+#1507 := [unit-resolution #595 #1506]: #408
+#1508 := [unit-resolution #1339 #1507]: #190
+#392 := (or #388 #379)
+#582 := [asserted]: #392
+#1509 := [unit-resolution #582 #1508]: #379
+#1510 := [unit-resolution #828 #1509 #1505 #882]: #145
+#1511 := [unit-resolution #543 #1510]: #338
+#1512 := [unit-resolution #784 #1511 #1173 #1172]: #114
+#1513 := [unit-resolution #522 #1512]: #297
+#1514 := [unit-resolution #547 #1510]: #298
+#1515 := [unit-resolution #1464 #1512 #1030 #970]: #67
+#1516 := [unit-resolution #483 #1515]: #257
+#1517 := [unit-resolution #716 #1516 #1514 #1513]: #98
+#1518 := [unit-resolution #509 #1517]: #249
+#1519 := [unit-resolution #485 #1515]: #224
+#1520 := [unit-resolution #519 #1512]: #305
+#1521 := [unit-resolution #732 #1520 #970]: #81
+#1522 := [unit-resolution #496 #1521]: #233
+#1523 := [unit-resolution #425 #1522]: #38
+#1524 := [unit-resolution #465 #1523]: #223
+#1525 := [unit-resolution #616 #1524 #1519]: #26
+#1526 := [unit-resolution #458 #1525]: #219
+#1527 := [unit-resolution #648 #1526 #919 #1518]: #53
+#1528 := [unit-resolution #459 #1525]: #213
+#1529 := [unit-resolution #905 #1528]: #22
+#1530 := [unit-resolution #473 #1529 #1527]: false
+#1532 := [lemma #1530]: #1531
+#1533 := [unit-resolution #1532 #1030 #970 #1173 #1172 #882 #1154]: #60
+#1534 := [unit-resolution #484 #1533]: #256
+#1535 := [unit-resolution #1464 #1534 #1030 #970]: #306
+#1536 := [unit-resolution #784 #1535 #1173 #1172]: #143
+#1537 := [unit-resolution #543 #1536]: #339
+#1538 := [unit-resolution #828 #1537 #1505 #882]: #181
+#1539 := [unit-resolution #582 #1538]: #388
+#1540 := [unit-resolution #1339 #1539]: #208
+#1541 := [unit-resolution #595 #1540]: #404
+#1542 := [unit-resolution #852 #1541 #1155]: #200
+#1543 := [unit-resolution #590 #1542]: #364
+#1544 := [unit-resolution #589 #1542]: #398
+#1545 := [unit-resolution #450 #1544]: #163
+#1546 := [unit-resolution #558 #1545]: #358
+#1547 := [unit-resolution #804 #1546 #1161 #1543]: #131
+#1548 := [unit-resolution #535 #1547]: #282
+#1549 := [unit-resolution #1110 #1534 #970 #1030]: #297
+#1550 := [unit-resolution #486 #1533]: #257
+#1551 := [unit-resolution #545 #1536]: #298
+#1552 := [unit-resolution #716 #1551 #1550 #1549]: #98
+#1553 := [unit-resolution #508 #1552]: #281
+#1554 := [unit-resolution #560 #1545]: #318
+#1555 := [unit-resolution #534 #1547]: #317
+#1556 := [unit-resolution #736 #1555 #1554]: #87
+#1557 := [unit-resolution #498 #1556]: #276
+#1558 := [unit-resolution #692 #1557 #1553 #1548]: #55
+#1559 := [unit-resolution #500 #1556]: #236
+#1560 := [unit-resolution #916 #1559]: #47
+#1561 := [unit-resolution #474 #1560 #1558]: false
+#1563 := [lemma #1561]: #1562
+#1569 := [unit-resolution #1563 #882 #1564 #1565 #1499 #1566]: #40
+#1570 := [unit-resolution #464 #1569]: #228
+#1571 := [unit-resolution #425 #1570]: #44
+#1572 := [unit-resolution #496 #1571]: #272
+#1573 := [unit-resolution #732 #1572 #1499]: #112
+#1574 := [unit-resolution #519 #1573]: #306
+#1575 := [unit-resolution #784 #1574 #1564 #1565]: #143
+#1576 := [unit-resolution #543 #1575]: #339
+#1577 := [unit-resolution #828 #1576 #1568 #882]: #181
+#1578 := [unit-resolution #582 #1577]: #388
+#1579 := [unit-resolution #1339 #1578]: #208
+#1580 := [unit-resolution #595 #1579]: #404
+#1581 := [unit-resolution #852 #1580 #1567]: #200
+#1582 := [unit-resolution #590 #1581]: #364
+#1583 := [unit-resolution #572 #1566]: #363
+#1584 := [unit-resolution #589 #1581]: #398
+#1585 := [unit-resolution #450 #1584]: #163
+#1586 := [unit-resolution #558 #1585]: #358
+#1587 := [unit-resolution #804 #1586 #1583 #1582]: #131
+#1588 := [unit-resolution #535 #1587]: #282
+#1589 := [unit-resolution #520 #1573]: #297
+#1590 := [unit-resolution #545 #1575]: #298
+#1591 := [unit-resolution #1166 #1580 #1566]: #60
+#1592 := [unit-resolution #486 #1591]: #257
+#1593 := [unit-resolution #716 #1592 #1590 #1589]: #98
+#1594 := [unit-resolution #508 #1593]: #281
+#1595 := [unit-resolution #466 #1569]: #223
+#1596 := [unit-resolution #488 #1591]: #224
+#1597 := [unit-resolution #616 #1596 #1595]: #26
+#1598 := [unit-resolution #459 #1597]: #213
+#1599 := [unit-resolution #905 #1598]: #22
+#1600 := [unit-resolution #475 #1599]: #241
+#1601 := [unit-resolution #692 #1600 #1594 #1588]: #85
+#1602 := [unit-resolution #560 #1585]: #318
+#1603 := [unit-resolution #534 #1587]: #317
+#1604 := [unit-resolution #736 #1603 #1602]: #87
+#1605 := [unit-resolution #498 #1604 #1601]: false
+#1607 := [lemma #1605]: #1606
+#1608 := [unit-resolution #1607 #881]: #183
+#411 := (or #404 #380)
+#597 := [asserted]: #411
+#1609 := [unit-resolution #597 #1608]: #404
+#410 := (or #408 #380)
+#596 := [asserted]: #410
+#1610 := [unit-resolution #596 #1608]: #408
+#1611 := [unit-resolution #1339 #1610]: #190
+#1612 := [unit-resolution #579 #1611]: #387
+#1613 := [unit-resolution #1497 #1612]: #157
+#1614 := [unit-resolution #556 #1613]: #313
+#1615 := [unit-resolution #583 #1611]: #347
+#1616 := [unit-resolution #555 #1613]: #346
+#1617 := [unit-resolution #1492 #1616 #881 #1615 #1614]: #138
+#1618 := [unit-resolution #571 #1617]: #372
+#1619 := [unit-resolution #852 #1618 #1609]: #200
+#1620 := [unit-resolution #590 #1619]: #364
+#1621 := [unit-resolution #572 #1617]: #363
+#1622 := [unit-resolution #589 #1619]: #398
+#1623 := [unit-resolution #450 #1622]: #163
+#1624 := [unit-resolution #558 #1623]: #358
+#1625 := [unit-resolution #804 #1624 #1621 #1620]: #131
+#1626 := [unit-resolution #535 #1625]: #282
+#1627 := [unit-resolution #560 #1623]: #318
+#1628 := [unit-resolution #534 #1625]: #317
+#1629 := [unit-resolution #736 #1628 #1627]: #87
+#1630 := [unit-resolution #498 #1629]: #276
+#1631 := [unit-resolution #500 #1629]: #236
+#1632 := [unit-resolution #916 #1631]: #47
+#1633 := [unit-resolution #474 #1632]: #241
+#1634 := [unit-resolution #692 #1633 #1630 #1626]: #91
+#1635 := [unit-resolution #508 #1634]: #289
+#1636 := [unit-resolution #1166 #1617 #1609]: #60
+#1637 := [unit-resolution #486 #1636]: #257
+#1638 := [unit-resolution #484 #1636]: #256
+#1639 := [unit-resolution #488 #1636]: #224
+#1640 := [unit-resolution #476 #1632]: #214
+#1641 := [unit-resolution #905 #1640]: #20
+#1642 := [unit-resolution #459 #1641]: #218
+#1643 := [unit-resolution #616 #1642 #1639]: #32
+#1644 := [unit-resolution #466 #1643]: #229
+#1645 := [unit-resolution #1110 #1644 #1614 #1638]: #297
+#1646 := [unit-resolution #716 #1645 #1637 #1635]: #107
+#1647 := [unit-resolution #1464 #1644 #1638 #1614]: #306
+#1648 := [unit-resolution #784 #1647 #1616 #1615]: #143
+#1649 := [unit-resolution #545 #1648 #1646]: false
+#1650 := [lemma #1649]: #129
+#326 := (or #322 #282)
+#533 := [asserted]: #326
+#1662 := [unit-resolution #533 #1650]: #282
+#1664 := [unit-resolution #692 #1662]: #1663
+#1665 := [unit-resolution #1664 #1661 #1658 #1654]: false
+#1667 := [lemma #1665]: #1666
+#1725 := [unit-resolution #1667 #919]: #218
+#1689 := (or #306 #26 #119 #40)
+#1668 := [hypothesis]: #218
+#1683 := [unit-resolution #1464 #1457 #1030 #970]: #67
+#1684 := [unit-resolution #485 #1683]: #224
+#1685 := [unit-resolution #616 #1684 #1668]: #32
+#1686 := [unit-resolution #496 #1459]: #233
+#1687 := [unit-resolution #425 #1686]: #38
+#1688 := [unit-resolution #465 #1687 #1685]: false
+#1690 := [lemma #1688]: #1689
+#1726 := [unit-resolution #1690 #1725 #970 #1030]: #306
+#1715 := (or #298 #114)
+#1700 := [hypothesis]: #107
+#1701 := [unit-resolution #545 #1700]: #338
+#1702 := [hypothesis]: #306
+#1703 := [unit-resolution #547 #1700]: #339
+#1698 := (or #387 #145)
+#1691 := [hypothesis]: #339
+#1692 := [unit-resolution #596 #1340]: #380
+#1694 := (or #371 #204)
+#324 := (or #322 #323)
+#531 := [asserted]: #324
+#1693 := [unit-resolution #531 #1650]: #323
+#1695 := [unit-resolution #1021 #1693]: #1694
+#1696 := [unit-resolution #1695 #1341]: #371
+#1697 := [unit-resolution #828 #1696 #1692 #1691 #1342]: false
+#1699 := [lemma #1697]: #1698
+#1704 := [unit-resolution #1699 #1703]: #387
+#1705 := [unit-resolution #1497 #1704]: #157
+#1706 := [unit-resolution #555 #1705]: #346
+#1707 := [unit-resolution #784 #1706 #1702 #1701]: #152
+#1708 := [unit-resolution #584 #1707]: #379
+#1709 := [unit-resolution #583 #1707]: #388
+#1710 := [unit-resolution #1339 #1709]: #208
+#1711 := [unit-resolution #596 #1710]: #380
+#1712 := [unit-resolution #595 #1710]: #404
+#1713 := [unit-resolution #1695 #1712]: #371
+#1714 := [unit-resolution #828 #1713 #1711 #1703 #1708]: false
+#1716 := [lemma #1714]: #1715
+#1727 := [unit-resolution #1716 #1726]: #298
+#1681 := (or #107 #40 #98 #119 #26)
+#1669 := [unit-resolution #1056 #1045 #970 #1030 #1044]: #224
+#1670 := [unit-resolution #616 #1669 #1668]: #32
+#1671 := [unit-resolution #465 #1670]: #228
+#1672 := [unit-resolution #425 #1671]: #44
+#1673 := [unit-resolution #496 #1672]: #272
+#1674 := [unit-resolution #732 #1673 #970]: #112
+#1675 := [unit-resolution #520 #1674]: #297
+#1676 := [unit-resolution #716 #1675 #1045 #1044]: #69
+#1677 := [unit-resolution #497 #1672]: #264
+#1678 := [unit-resolution #521 #1674]: #265
+#1679 := [unit-resolution #672 #1678 #1030 #1677]: #67
+#1680 := [unit-resolution #483 #1679 #1676]: false
+#1682 := [lemma #1680]: #1681
+#1728 := [unit-resolution #1682 #1727 #1030 #970 #1725]: #98
+#1729 := [unit-resolution #508 #1728]: #281
+#1730 := [unit-resolution #509 #1728]: #249
+#1723 := (or #240 #91)
+#1717 := [hypothesis]: #53
+#242 := (or #240 #241)
+#471 := [asserted]: #242
+#1718 := [unit-resolution #471 #1717]: #241
+#1719 := [unit-resolution #1664 #1718 #1236]: #85
+#1720 := [unit-resolution #472 #1717]: #235
+#1721 := [unit-resolution #916 #1720]: #49
+#1722 := [unit-resolution #499 #1721 #1719]: false
+#1724 := [lemma #1722]: #1723
+#1731 := [unit-resolution #1724 #1729]: #240
+#1732 := [unit-resolution #648 #1731 #919 #1730]: #28
+#1733 := [unit-resolution #460 #1732]: #213
+#1734 := [unit-resolution #905 #1733]: #22
+#1735 := [unit-resolution #475 #1734]: #241
+#1736 := [unit-resolution #1664 #1735 #1729]: #85
+#1737 := [unit-resolution #476 #1734]: #235
+#1738 := [unit-resolution #916 #1737]: #49
+#1739 := [unit-resolution #499 #1738 #1736]: false
+#1741 := [lemma #1739]: #1740
+#1742 := [unit-resolution #1741 #970 #1030]: #60
+#1743 := [unit-resolution #484 #1742]: #256
+#1748 := [unit-resolution #1110 #1743 #1030 #970]: #297
+#1749 := [unit-resolution #486 #1742]: #257
+#1750 := [unit-resolution #1464 #1743 #1030 #970]: #306
+#1751 := [unit-resolution #1716 #1750]: #298
+#1752 := [unit-resolution #716 #1751 #1749 #1748]: #98
+#1753 := [unit-resolution #508 #1752]: #281
+#1754 := [unit-resolution #488 #1742]: #224
+#1746 := (or #233 #40 #119)
+#1744 := [unit-resolution #672 #976 #1030 #1743]: #76
+#1745 := [unit-resolution #521 #1744 #973]: false
+#1747 := [lemma #1745]: #1746
+#1755 := [unit-resolution #1747 #970 #1030]: #233
+#1756 := [unit-resolution #425 #1755]: #38
+#1757 := [unit-resolution #465 #1756]: #223
+#1758 := [unit-resolution #616 #1757 #1754]: #26
+#1759 := [unit-resolution #459 #1758]: #213
+#1760 := [unit-resolution #905 #1759]: #22
+#1761 := [unit-resolution #475 #1760]: #241
+#1762 := [unit-resolution #1664 #1761 #1753]: #85
+#1763 := [unit-resolution #476 #1760]: #235
+#1764 := [unit-resolution #916 #1763]: #49
+#1765 := [unit-resolution #499 #1764 #1762]: false
+#1767 := [lemma #1765]: #1766
+#1768 := [unit-resolution #1767 #1030]: #119
+#1769 := [unit-resolution #556 #1768]: #354
+#1770 := [unit-resolution #1497 #1769]: #188
+#1771 := [unit-resolution #581 #1770]: #347
+#1772 := [unit-resolution #557 #1768]: #346
+#1773 := [unit-resolution #1699 #1770]: #145
+#1774 := [unit-resolution #543 #1773]: #338
+#1775 := [unit-resolution #784 #1774 #1772 #1771]: #114
+#1787 := [unit-resolution #522 #1775]: #297
+#1788 := [unit-resolution #547 #1773]: #298
+#1802 := (or #60 #40)
+#1785 := (or #257 #26 #40)
+#1776 := [unit-resolution #523 #1775]: #265
+#1777 := [hypothesis]: #69
+#1778 := [unit-resolution #483 #1777]: #256
+#1779 := [unit-resolution #672 #1778 #1030 #1776]: #74
+#1780 := [unit-resolution #497 #1779]: #233
+#1781 := [unit-resolution #487 #1777]: #224
+#1782 := [unit-resolution #616 #1781 #1668]: #32
+#1783 := [unit-resolution #465 #1782]: #228
+#1784 := [unit-resolution #425 #1783 #1780]: false
+#1786 := [lemma #1784]: #1785
+#1789 := [unit-resolution #1786 #1725 #1030]: #257
+#1790 := [unit-resolution #716 #1789 #1788 #1787]: #98
+#1791 := [unit-resolution #508 #1790]: #281
+#1792 := [unit-resolution #509 #1790]: #249
+#1793 := [unit-resolution #1724 #1791]: #240
+#1794 := [unit-resolution #648 #1793 #919 #1792]: #28
+#1795 := [unit-resolution #460 #1794]: #213
+#1796 := [unit-resolution #905 #1795]: #22
+#1797 := [unit-resolution #475 #1796]: #241
+#1798 := [unit-resolution #1664 #1797 #1791]: #85
+#1799 := [unit-resolution #476 #1796]: #235
+#1800 := [unit-resolution #916 #1799]: #49
+#1801 := [unit-resolution #499 #1800 #1798]: false
+#1803 := [lemma #1801]: #1802
+#1804 := [unit-resolution #1803 #1030]: #60
+#1805 := [unit-resolution #486 #1804]: #257
+#1806 := [unit-resolution #716 #1805 #1788 #1787]: #98
+#1807 := [unit-resolution #508 #1806]: #281
+#1808 := [unit-resolution #488 #1804]: #224
+#1809 := [unit-resolution #484 #1804]: #256
+#1810 := [unit-resolution #672 #1809 #1030 #1776]: #74
+#1811 := [unit-resolution #497 #1810]: #233
+#1812 := [unit-resolution #425 #1811]: #38
+#1813 := [unit-resolution #465 #1812]: #223
+#1814 := [unit-resolution #616 #1813 #1808]: #26
+#1815 := [unit-resolution #459 #1814]: #213
+#1816 := [unit-resolution #905 #1815]: #22
+#1817 := [unit-resolution #475 #1816]: #241
+#1818 := [unit-resolution #1664 #1817 #1807]: #85
+#1819 := [unit-resolution #476 #1816]: #235
+#1820 := [unit-resolution #916 #1819]: #49
+#1821 := [unit-resolution #499 #1820 #1818]: false
+#1822 := [lemma #1821]: #40
+#1855 := [unit-resolution #464 #1822]: #228
+#1856 := [unit-resolution #425 #1855]: #44
+#1857 := [unit-resolution #496 #1856]: #272
+#1858 := [unit-resolution #732 #1103 #1857]: #119
+#1859 := [unit-resolution #556 #1858]: #354
+#1860 := [unit-resolution #1497 #1859]: #188
+#1861 := [unit-resolution #1699 #1860]: #145
+#1862 := [unit-resolution #557 #1858]: #346
+#1863 := [unit-resolution #522 #1102]: #306
+#1864 := [unit-resolution #581 #1860]: #347
+#1865 := [unit-resolution #784 #1864 #1863 #1862]: #143
+#1866 := [unit-resolution #543 #1865 #1861]: false
+#1867 := [lemma #1866]: #297
+#1853 := (or #105 #107)
+#1838 := (or #60 #107 #105)
+#1823 := [unit-resolution #466 #1822]: #223
+#1824 := [unit-resolution #616 #1725 #1823]: #34
+#1825 := [unit-resolution #487 #1824]: #257
+#1826 := [unit-resolution #716 #1825 #1045 #890]: #98
+#1827 := [unit-resolution #508 #1826]: #281
+#1828 := [unit-resolution #509 #1826]: #249
+#1829 := [unit-resolution #1724 #1827]: #240
+#1830 := [unit-resolution #648 #1829 #919 #1828]: #28
+#1831 := [unit-resolution #460 #1830]: #213
+#1832 := [unit-resolution #905 #1831]: #22
+#1833 := [unit-resolution #475 #1832]: #241
+#1834 := [unit-resolution #1664 #1833 #1827]: #85
+#1835 := [unit-resolution #476 #1832]: #235
+#1836 := [unit-resolution #916 #1835]: #49
+#1837 := [unit-resolution #499 #1836 #1834]: false
+#1839 := [lemma #1837]: #1838
+#1840 := [unit-resolution #1839 #890 #1045]: #60
+#1841 := [unit-resolution #486 #1840]: #257
+#1842 := [unit-resolution #716 #1841 #1045 #890]: #98
+#1843 := [unit-resolution #508 #1842]: #281
+#1844 := [unit-resolution #488 #1840]: #224
+#1845 := [unit-resolution #616 #1844 #1823]: #26
+#1846 := [unit-resolution #459 #1845]: #213
+#1847 := [unit-resolution #905 #1846]: #22
+#1848 := [unit-resolution #475 #1847]: #241
+#1849 := [unit-resolution #1664 #1848 #1843]: #85
+#1850 := [unit-resolution #476 #1847]: #235
+#1851 := [unit-resolution #916 #1850]: #49
+#1852 := [unit-resolution #499 #1851 #1849]: false
+#1854 := [lemma #1852]: #1853
+#1868 := [unit-resolution #1854 #1867]: #107
+#1869 := [unit-resolution #547 #1868]: #339
+#1870 := [unit-resolution #1699 #1869]: #387
+#1871 := [unit-resolution #1497 #1870]: #157
+#1872 := [unit-resolution #1716 #1868]: #114
+#1873 := [unit-resolution #519 #1872]: #305
+#1874 := [unit-resolution #732 #1873 #1857]: #119
+[unit-resolution #556 #1874 #1871]: false
+4981f4ce905ff5bd45aa1d26b0e079fee17e6b28 67 0
unsat
-0020560a0c4fa3058b0174abbbe01bb65cb5b25a 67 0
#2 := false
decl f1 :: S1
#3 := f1
decl f3 :: (-> Int S1)
decl ?v0!0 :: Int
-#55 := ?v0!0
-#56 := (f3 ?v0!0)
-#57 := (= #56 f1)
-#58 := (not #57)
+#53 := ?v0!0
+#54 := (f3 ?v0!0)
+#55 := (= #54 f1)
+#56 := (not #55)
decl ?v1!1 :: Int
#66 := ?v1!1
#67 := (f3 ?v1!1)
#68 := (= #67 f1)
-#69 := (or #57 #68)
+#69 := (or #55 #68)
#70 := (not #69)
-#86 := (and #57 #70)
-#63 := (not #58)
-#76 := (and #63 #70)
-#87 := (iff #76 #86)
-#84 := (iff #63 #57)
-#85 := [rewrite]: #84
-#88 := [monotonicity #85]: #87
+#84 := (and #55 #70)
+#63 := (not #56)
+#74 := (and #63 #70)
+#85 := (iff #74 #84)
+#82 := (iff #63 #55)
+#83 := [rewrite]: #82
+#86 := [monotonicity #83]: #85
#7 := (:var 0 Int)
#8 := (f3 #7)
#9 := (= #8 f1)
@@ -1798,44 +2058,44 @@
#12 := (= #11 f1)
#13 := (or #12 #9)
#14 := (forall (vars (?v1 Int)) #13)
-#39 := (not #9)
-#40 := (or #39 #14)
-#43 := (forall (vars (?v0 Int)) #40)
-#46 := (not #43)
-#79 := (~ #46 #76)
-#50 := (or #57 #9)
-#52 := (forall (vars (?v1 Int)) #50)
-#59 := (or #58 #52)
+#23 := (not #9)
+#24 := (or #23 #14)
+#27 := (forall (vars (?v0 Int)) #24)
+#30 := (not #27)
+#77 := (~ #30 #74)
+#57 := (or #55 #9)
+#58 := (forall (vars (?v1 Int)) #57)
+#59 := (or #56 #58)
#60 := (not #59)
-#77 := (~ #60 #76)
-#71 := (not #52)
+#75 := (~ #60 #74)
+#71 := (not #58)
#72 := (~ #71 #70)
#73 := [sk]: #72
#64 := (~ #63 #63)
#65 := [refl]: #64
-#78 := [nnf-neg #65 #73]: #77
-#61 := (~ #46 #60)
+#76 := [nnf-neg #65 #73]: #75
+#61 := (~ #30 #60)
#62 := [sk]: #61
-#80 := [trans #62 #78]: #79
+#78 := [trans #62 #76]: #77
#15 := (implies #9 #14)
#16 := (forall (vars (?v0 Int)) #15)
#17 := (not #16)
-#47 := (iff #17 #46)
-#44 := (iff #16 #43)
-#41 := (iff #15 #40)
-#42 := [rewrite]: #41
-#45 := [quant-intro #42]: #44
-#48 := [monotonicity #45]: #47
-#38 := [asserted]: #17
-#51 := [mp #38 #48]: #46
-#81 := [mp~ #51 #80]: #76
-#82 := [mp #81 #88]: #86
-#89 := [and-elim #82]: #70
-#90 := [not-or-elim #89]: #58
-#83 := [and-elim #82]: #57
-[unit-resolution #83 #90]: false
+#31 := (iff #17 #30)
+#28 := (iff #16 #27)
+#25 := (iff #15 #24)
+#26 := [rewrite]: #25
+#29 := [quant-intro #26]: #28
+#32 := [monotonicity #29]: #31
+#19 := [asserted]: #17
+#33 := [mp #19 #32]: #30
+#79 := [mp~ #33 #78]: #74
+#80 := [mp #79 #86]: #84
+#87 := [and-elim #80]: #70
+#88 := [not-or-elim #87]: #56
+#81 := [and-elim #80]: #55
+[unit-resolution #81 #88]: false
+4467e2bf3cf901d999549d9b67e78dac1d5ecf0f 117 0
unsat
-71f21c0a5d88cb94f60cf796ba4f0c3c95e6bff5 117 0
#2 := false
decl f3 :: (-> S3 S2 S1)
#10 := (:var 0 S2)
@@ -1846,120 +2106,120 @@
#7 := f5
#17 := (f4 f5 f6)
#18 := (f3 #17 #10)
-#573 := (pattern #18)
+#512 := (pattern #18)
decl f1 :: S1
#3 := f1
#19 := (= #18 f1)
-#76 := (not #19)
-#574 := (forall (vars (?v0 S2)) (:pat #573) #76)
+#57 := (not #19)
+#513 := (forall (vars (?v0 S2)) (:pat #512) #57)
decl f7 :: S2
#21 := f7
#22 := (f3 #17 f7)
#23 := (= #22 f1)
-#150 := (= f6 f1)
-#151 := (iff #23 #150)
+#86 := (= f6 f1)
+#87 := (iff #23 #86)
#8 := (:var 1 S1)
#9 := (f4 f5 #8)
#11 := (f3 #9 #10)
-#566 := (pattern #11)
+#505 := (pattern #11)
#13 := (= #8 f1)
#12 := (= #11 f1)
#14 := (iff #12 #13)
-#567 := (forall (vars (?v0 S1) (?v1 S2)) (:pat #566) #14)
+#506 := (forall (vars (?v0 S1) (?v1 S2)) (:pat #505) #14)
#15 := (forall (vars (?v0 S1) (?v1 S2)) #14)
-#570 := (iff #15 #567)
-#568 := (iff #14 #14)
-#569 := [refl]: #568
-#571 := [quant-intro #569]: #570
-#62 := (~ #15 #15)
+#509 := (iff #15 #506)
+#507 := (iff #14 #14)
+#508 := [refl]: #507
+#510 := [quant-intro #508]: #509
+#58 := (~ #15 #15)
#60 := (~ #14 #14)
#61 := [refl]: #60
-#63 := [nnf-pos #61]: #62
-#46 := [asserted]: #15
-#53 := [mp~ #46 #63]: #15
-#572 := [mp #53 #571]: #567
-#152 := (not #567)
-#228 := (or #152 #151)
-#561 := [quant-inst #16 #21]: #228
-#237 := [unit-resolution #561 #572]: #151
+#59 := [nnf-pos #61]: #58
+#27 := [asserted]: #15
+#56 := [mp~ #27 #59]: #15
+#511 := [mp #56 #510]: #506
+#90 := (not #506)
+#167 := (or #90 #87)
+#500 := [quant-inst #16 #21]: #167
+#176 := [unit-resolution #500 #511]: #87
decl ?v0!0 :: S2
-#66 := ?v0!0
-#67 := (f3 #17 ?v0!0)
-#68 := (= #67 f1)
-#236 := (iff #68 #150)
-#238 := (or #152 #236)
-#229 := [quant-inst #16 #66]: #238
-#227 := [unit-resolution #229 #572]: #236
-#240 := (not #236)
-#199 := (or #240 #150)
-#55 := (not #23)
-#215 := [hypothesis]: #55
-#83 := (or #68 #23)
-#79 := (forall (vars (?v0 S2)) #76)
-#82 := (or #79 #55)
-#84 := (and #83 #82)
+#67 := ?v0!0
+#68 := (f3 #17 ?v0!0)
+#69 := (= #68 f1)
+#175 := (iff #69 #86)
+#177 := (or #90 #175)
+#168 := [quant-inst #16 #67]: #177
+#166 := [unit-resolution #168 #511]: #175
+#179 := (not #175)
+#138 := (or #179 #86)
+#77 := (not #23)
+#154 := [hypothesis]: #77
+#81 := (or #69 #23)
+#64 := (forall (vars (?v0 S2)) #57)
+#80 := (or #64 #77)
+#82 := (and #81 #80)
#20 := (exists (vars (?v0 S2)) #19)
-#48 := (not #20)
-#49 := (iff #48 #23)
-#85 := (~ #49 #84)
-#57 := (~ #23 #23)
-#65 := [refl]: #57
-#64 := (~ #55 #55)
-#56 := [refl]: #64
-#80 := (~ #48 #79)
-#77 := (~ #76 #76)
-#78 := [refl]: #77
-#81 := [nnf-neg #78]: #80
-#73 := (not #48)
-#74 := (~ #73 #68)
-#69 := (~ #20 #68)
-#70 := [sk]: #69
-#75 := [nnf-neg #70]: #74
-#86 := [nnf-pos #75 #81 #56 #65]: #85
+#32 := (not #20)
+#33 := (iff #32 #23)
+#83 := (~ #33 #82)
+#78 := (~ #77 #77)
+#79 := [refl]: #78
+#75 := (~ #23 #23)
+#76 := [refl]: #75
+#72 := (not #32)
+#73 := (~ #72 #69)
+#70 := (~ #20 #69)
+#71 := [sk]: #70
+#74 := [nnf-neg #71]: #73
+#65 := (~ #32 #64)
+#62 := (~ #57 #57)
+#63 := [refl]: #62
+#66 := [nnf-neg #63]: #65
+#84 := [nnf-pos #66 #74 #76 #79]: #83
#24 := (iff #20 #23)
#25 := (not #24)
-#50 := (iff #25 #49)
-#51 := [rewrite]: #50
-#47 := [asserted]: #25
-#54 := [mp #47 #51]: #49
-#87 := [mp~ #54 #86]: #84
-#90 := [and-elim #87]: #83
-#557 := [unit-resolution #90 #215]: #68
-#243 := (not #68)
-#222 := (or #240 #243 #150)
-#558 := [def-axiom]: #222
-#541 := [unit-resolution #558 #557]: #199
-#203 := [unit-resolution #541 #227]: #150
-#241 := (not #150)
-#562 := (not #151)
-#204 := (or #562 #241)
-#563 := (or #562 #23 #241)
-#564 := [def-axiom]: #563
-#205 := [unit-resolution #564 #215]: #204
-#206 := [unit-resolution #205 #203 #237]: false
-#543 := [lemma #206]: #23
-#579 := (or #574 #55)
-#580 := (iff #82 #579)
-#577 := (iff #79 #574)
-#575 := (iff #76 #76)
-#576 := [refl]: #575
-#578 := [quant-intro #576]: #577
-#581 := [monotonicity #578]: #580
-#91 := [and-elim #87]: #82
-#582 := [mp #91 #581]: #579
-#242 := [unit-resolution #582 #543]: #574
-#555 := (not #574)
-#214 := (or #555 #55)
-#219 := [quant-inst #21]: #214
-[unit-resolution #219 #543 #242]: false
+#34 := (iff #25 #33)
+#35 := [rewrite]: #34
+#28 := [asserted]: #25
+#36 := [mp #28 #35]: #33
+#85 := [mp~ #36 #84]: #82
+#88 := [and-elim #85]: #81
+#496 := [unit-resolution #88 #154]: #69
+#182 := (not #69)
+#161 := (or #179 #182 #86)
+#497 := [def-axiom]: #161
+#480 := [unit-resolution #497 #496]: #138
+#142 := [unit-resolution #480 #166]: #86
+#180 := (not #86)
+#501 := (not #87)
+#143 := (or #501 #180)
+#502 := (or #501 #23 #180)
+#503 := [def-axiom]: #502
+#144 := [unit-resolution #503 #154]: #143
+#145 := [unit-resolution #144 #142 #176]: false
+#482 := [lemma #145]: #23
+#518 := (or #513 #77)
+#519 := (iff #80 #518)
+#516 := (iff #64 #513)
+#514 := (iff #57 #57)
+#515 := [refl]: #514
+#517 := [quant-intro #515]: #516
+#520 := [monotonicity #517]: #519
+#89 := [and-elim #85]: #80
+#521 := [mp #89 #520]: #518
+#181 := [unit-resolution #521 #482]: #513
+#494 := (not #513)
+#153 := (or #494 #77)
+#158 := [quant-inst #21]: #153
+[unit-resolution #158 #482 #181]: false
+03b722cb2eea463c8897e294f3d4d3f3f1ac4061 117 0
unsat
-ae3e0f78fcdef723f102d089b42d97f098766d9e 117 0
#2 := false
decl f1 :: S1
#3 := f1
decl f7 :: S1
#25 := f7
-#206 := (= f7 f1)
+#140 := (= f7 f1)
decl f3 :: (-> S3 S2 S1)
decl f6 :: S2
#20 := f6
@@ -1969,109 +2229,109 @@
#26 := (f4 f5 f7)
#30 := (f3 #26 f6)
#31 := (= #30 f1)
-#292 := (iff #31 #206)
+#229 := (iff #31 #140)
#10 := (:var 0 S2)
#8 := (:var 1 S1)
#9 := (f4 f5 #8)
#11 := (f3 #9 #10)
-#622 := (pattern #11)
+#559 := (pattern #11)
#13 := (= #8 f1)
#12 := (= #11 f1)
#14 := (iff #12 #13)
-#623 := (forall (vars (?v0 S1) (?v1 S2)) (:pat #622) #14)
+#560 := (forall (vars (?v0 S1) (?v1 S2)) (:pat #559) #14)
#15 := (forall (vars (?v0 S1) (?v1 S2)) #14)
-#626 := (iff #15 #623)
-#624 := (iff #14 #14)
-#625 := [refl]: #624
-#627 := [quant-intro #625]: #626
-#73 := (~ #15 #15)
-#71 := (~ #14 #14)
-#72 := [refl]: #71
-#74 := [nnf-pos #72]: #73
-#54 := [asserted]: #15
-#62 := [mp~ #54 #74]: #15
-#628 := [mp #62 #627]: #623
-#295 := (not #623)
-#611 := (or #295 #292)
-#270 := [quant-inst #25 #20]: #611
-#297 := [unit-resolution #270 #628]: #292
+#563 := (iff #15 #560)
+#561 := (iff #14 #14)
+#562 := [refl]: #561
+#564 := [quant-intro #562]: #563
+#71 := (~ #15 #15)
+#67 := (~ #14 #14)
+#68 := [refl]: #67
+#72 := [nnf-pos #68]: #71
+#35 := [asserted]: #15
+#65 := [mp~ #35 #72]: #15
+#565 := [mp #65 #564]: #560
+#232 := (not #560)
+#548 := (or #232 #229)
+#207 := [quant-inst #25 #20]: #548
+#234 := [unit-resolution #207 #565]: #229
decl ?v0!3 :: S2
-#120 := ?v0!3
-#123 := (f3 #26 ?v0!3)
-#124 := (= #123 f1)
-#296 := (iff #124 #206)
-#299 := (or #295 #296)
-#278 := [quant-inst #25 #120]: #299
-#298 := [unit-resolution #278 #628]: #296
-#614 := (not #296)
-#599 := (or #614 #206)
-#108 := (not #31)
+#121 := ?v0!3
+#122 := (f3 #26 ?v0!3)
+#123 := (= #122 f1)
+#233 := (iff #123 #140)
+#236 := (or #232 #233)
+#215 := [quant-inst #25 #121]: #236
+#235 := [unit-resolution #215 #565]: #233
+#551 := (not #233)
+#536 := (or #551 #140)
+#131 := (not #31)
#27 := (f3 #26 #10)
-#654 := (pattern #27)
+#591 := (pattern #27)
#28 := (= #27 f1)
-#132 := (not #28)
-#655 := (forall (vars (?v0 S2)) (:pat #654) #132)
-#207 := [hypothesis]: #31
-#660 := (or #655 #108)
-#135 := (forall (vars (?v0 S2)) #132)
-#138 := (or #135 #108)
-#661 := (iff #138 #660)
-#658 := (iff #135 #655)
-#656 := (iff #132 #132)
-#657 := [refl]: #656
-#659 := [quant-intro #657]: #658
-#662 := [monotonicity #659]: #661
-#139 := (or #124 #31)
-#140 := (and #139 #138)
+#113 := (not #28)
+#592 := (forall (vars (?v0 S2)) (:pat #591) #113)
+#141 := [hypothesis]: #31
+#597 := (or #592 #131)
+#118 := (forall (vars (?v0 S2)) #113)
+#134 := (or #118 #131)
+#598 := (iff #134 #597)
+#595 := (iff #118 #592)
+#593 := (iff #113 #113)
+#594 := [refl]: #593
+#596 := [quant-intro #594]: #595
+#599 := [monotonicity #596]: #598
+#135 := (or #123 #31)
+#136 := (and #135 #134)
#29 := (exists (vars (?v0 S2)) #28)
-#57 := (not #29)
-#58 := (iff #57 #31)
-#141 := (~ #58 #140)
-#81 := (~ #31 #31)
-#119 := [refl]: #81
-#109 := (~ #108 #108)
-#80 := [refl]: #109
-#136 := (~ #57 #135)
-#133 := (~ #132 #132)
-#134 := [refl]: #133
-#137 := [nnf-neg #134]: #136
-#129 := (not #57)
-#130 := (~ #129 #124)
-#125 := (~ #29 #124)
-#126 := [sk]: #125
-#131 := [nnf-neg #126]: #130
-#142 := [nnf-pos #131 #137 #80 #119]: #141
+#41 := (not #29)
+#42 := (iff #41 #31)
+#137 := (~ #42 #136)
+#132 := (~ #131 #131)
+#133 := [refl]: #132
+#129 := (~ #31 #31)
+#130 := [refl]: #129
+#126 := (not #41)
+#127 := (~ #126 #123)
+#124 := (~ #29 #123)
+#125 := [sk]: #124
+#128 := [nnf-neg #125]: #127
+#119 := (~ #41 #118)
+#114 := (~ #113 #113)
+#117 := [refl]: #114
+#120 := [nnf-neg #117]: #119
+#138 := [nnf-pos #120 #128 #130 #133]: #137
#32 := (iff #29 #31)
#33 := (not #32)
-#59 := (iff #33 #58)
-#60 := [rewrite]: #59
-#56 := [asserted]: #33
-#63 := [mp #56 #60]: #58
-#143 := [mp~ #63 #142]: #140
-#147 := [and-elim #143]: #138
-#663 := [mp #147 #662]: #660
-#293 := [unit-resolution #663 #207]: #655
-#610 := (not #655)
-#283 := (or #610 #108)
-#284 := [quant-inst #20]: #283
-#617 := [unit-resolution #284 #207 #293]: false
-#618 := [lemma #617]: #108
-#146 := [and-elim #143]: #139
-#262 := [unit-resolution #146 #618]: #124
-#208 := (not #124)
-#294 := (or #614 #208 #206)
-#285 := [def-axiom]: #294
-#600 := [unit-resolution #285 #262]: #599
-#601 := [unit-resolution #600 #298]: #206
-#616 := (not #206)
-#275 := (not #292)
-#602 := (or #275 #616)
-#612 := (or #275 #31 #616)
-#271 := [def-axiom]: #612
-#603 := [unit-resolution #271 #618]: #602
-[unit-resolution #603 #601 #297]: false
+#43 := (iff #33 #42)
+#44 := [rewrite]: #43
+#37 := [asserted]: #33
+#45 := [mp #37 #44]: #42
+#139 := [mp~ #45 #138]: #136
+#143 := [and-elim #139]: #134
+#600 := [mp #143 #599]: #597
+#230 := [unit-resolution #600 #141]: #592
+#547 := (not #592)
+#220 := (or #547 #131)
+#221 := [quant-inst #20]: #220
+#554 := [unit-resolution #221 #141 #230]: false
+#555 := [lemma #554]: #131
+#142 := [and-elim #139]: #135
+#199 := [unit-resolution #142 #555]: #123
+#144 := (not #123)
+#231 := (or #551 #144 #140)
+#222 := [def-axiom]: #231
+#537 := [unit-resolution #222 #199]: #536
+#538 := [unit-resolution #537 #235]: #140
+#553 := (not #140)
+#212 := (not #229)
+#539 := (or #212 #553)
+#549 := (or #212 #31 #553)
+#208 := [def-axiom]: #549
+#540 := [unit-resolution #208 #555]: #539
+[unit-resolution #540 #538 #234]: false
+d52a85a56d8c1a29429987c40f8741cebe859405 61 0
unsat
-5dc6f25776aabe70ad45ce325942b3a138a1974d 61 0
#2 := false
decl f1 :: S1
#3 := f1
@@ -2084,92 +2344,92 @@
#18 := f5
#19 := (f3 f5)
#20 := (= #19 f1)
-#45 := (not #9)
-#46 := (or #45 #20)
-#49 := (not #46)
+#29 := (not #9)
+#30 := (or #29 #20)
+#33 := (not #30)
#21 := (implies #9 #20)
#22 := (not #21)
-#50 := (iff #22 #49)
-#47 := (iff #21 #46)
-#48 := [rewrite]: #47
-#51 := [monotonicity #48]: #50
-#44 := [asserted]: #22
-#54 := [mp #44 #51]: #49
-#52 := [not-or-elim #54]: #9
+#34 := (iff #22 #33)
+#31 := (iff #21 #30)
+#32 := [rewrite]: #31
+#35 := [monotonicity #32]: #34
+#25 := [asserted]: #22
+#36 := [mp #25 #35]: #33
+#37 := [not-or-elim #36]: #9
#10 := (:var 0 S2)
#11 := (f3 #10)
-#550 := (pattern #11)
+#491 := (pattern #11)
#12 := (= #11 f1)
#15 := (not #12)
-#551 := (forall (vars (?v0 S2)) (:pat #550) #15)
+#492 := (forall (vars (?v0 S2)) (:pat #491) #15)
#16 := (forall (vars (?v0 S2)) #15)
-#554 := (iff #16 #551)
-#552 := (iff #15 #15)
-#553 := [refl]: #552
-#555 := [quant-intro #553]: #554
+#495 := (iff #16 #492)
+#493 := (iff #15 #15)
+#494 := [refl]: #493
+#496 := [quant-intro #494]: #495
#13 := (exists (vars (?v0 S2)) #12)
#14 := (not #13)
-#60 := (~ #14 #16)
-#63 := (~ #15 #15)
-#64 := [refl]: #63
-#72 := [nnf-neg #64]: #60
+#71 := (~ #14 #16)
+#59 := (~ #15 #15)
+#60 := [refl]: #59
+#72 := [nnf-neg #60]: #71
#17 := (if #9 #14 #16)
-#70 := (iff #17 #14)
+#68 := (iff #17 #14)
#1 := true
#65 := (if true #14 #16)
-#68 := (iff #65 #14)
-#69 := [rewrite]: #68
+#62 := (iff #65 #14)
+#67 := [rewrite]: #62
#66 := (iff #17 #65)
-#61 := (iff #9 true)
-#62 := [iff-true #52]: #61
-#67 := [monotonicity #62]: #66
-#71 := [trans #67 #69]: #70
-#43 := [asserted]: #17
-#59 := [mp #43 #71]: #14
-#57 := [mp~ #59 #72]: #16
-#556 := [mp #57 #555]: #551
-#135 := (not #551)
-#221 := (or #135 #45)
-#136 := [quant-inst #7]: #221
-[unit-resolution #136 #556 #52]: false
+#63 := (iff #9 true)
+#64 := [iff-true #37]: #63
+#61 := [monotonicity #64]: #66
+#69 := [trans #61 #67]: #68
+#24 := [asserted]: #17
+#70 := [mp #24 #69]: #14
+#73 := [mp~ #70 #72]: #16
+#497 := [mp #73 #496]: #492
+#75 := (not #492)
+#162 := (or #75 #29)
+#76 := [quant-inst #7]: #162
+[unit-resolution #76 #497 #37]: false
+4ee0a4e3f4c5dbd20f1be18c405a836de5af68d2 17 0
unsat
-29e0fbcf1b3262888237e1fa476aa8a7425443c7 17 0
#2 := false
#7 := 3::Int
#8 := (= 3::Int 3::Int)
#9 := (not #8)
-#38 := (iff #9 false)
+#23 := (iff #9 false)
#1 := true
-#33 := (not true)
-#36 := (iff #33 false)
-#37 := [rewrite]: #36
-#34 := (iff #9 #33)
-#31 := (iff #8 true)
-#32 := [rewrite]: #31
-#35 := [monotonicity #32]: #34
-#39 := [trans #35 #37]: #38
-#30 := [asserted]: #9
-[mp #30 #39]: false
+#18 := (not true)
+#21 := (iff #18 false)
+#22 := [rewrite]: #21
+#19 := (iff #9 #18)
+#16 := (iff #8 true)
+#17 := [rewrite]: #16
+#20 := [monotonicity #17]: #19
+#24 := [trans #20 #22]: #23
+#11 := [asserted]: #9
+[mp #11 #24]: false
+8eb471f821b833f83e55527f320dd341eddcf700 17 0
unsat
-065da226a83f89ade06131ac7b676aff1d33184f 17 0
#2 := false
#7 := 3::Real
#8 := (= 3::Real 3::Real)
#9 := (not #8)
-#38 := (iff #9 false)
+#23 := (iff #9 false)
#1 := true
-#33 := (not true)
-#36 := (iff #33 false)
-#37 := [rewrite]: #36
-#34 := (iff #9 #33)
-#31 := (iff #8 true)
-#32 := [rewrite]: #31
-#35 := [monotonicity #32]: #34
-#39 := [trans #35 #37]: #38
-#30 := [asserted]: #9
-[mp #30 #39]: false
+#18 := (not true)
+#21 := (iff #18 false)
+#22 := [rewrite]: #21
+#19 := (iff #9 #18)
+#16 := (iff #8 true)
+#17 := [rewrite]: #16
+#20 := [monotonicity #17]: #19
+#24 := [trans #20 #22]: #23
+#11 := [asserted]: #9
+[mp #11 #24]: false
+c53677498fbbc0279d49e170ecebacd85ec37066 26 0
unsat
-52cd464fc4027157f69df0b8cc3229ae55ad2079 26 0
#2 := false
#10 := 4::Int
#8 := 1::Int
@@ -2177,26 +2437,26 @@
#9 := (+ 3::Int 1::Int)
#11 := (= #9 4::Int)
#12 := (not #11)
-#47 := (iff #12 false)
+#32 := (iff #12 false)
#1 := true
-#42 := (not true)
-#45 := (iff #42 false)
-#46 := [rewrite]: #45
-#43 := (iff #12 #42)
-#40 := (iff #11 true)
-#35 := (= 4::Int 4::Int)
-#38 := (iff #35 true)
-#39 := [rewrite]: #38
-#36 := (iff #11 #35)
-#34 := [rewrite]: #11
-#37 := [monotonicity #34]: #36
-#41 := [trans #37 #39]: #40
-#44 := [monotonicity #41]: #43
-#48 := [trans #44 #46]: #47
-#33 := [asserted]: #12
-[mp #33 #48]: false
+#27 := (not true)
+#30 := (iff #27 false)
+#31 := [rewrite]: #30
+#28 := (iff #12 #27)
+#25 := (iff #11 true)
+#19 := (= 4::Int 4::Int)
+#23 := (iff #19 true)
+#24 := [rewrite]: #23
+#20 := (iff #11 #19)
+#18 := [rewrite]: #11
+#21 := [monotonicity #18]: #20
+#26 := [trans #21 #24]: #25
+#29 := [monotonicity #26]: #28
+#33 := [trans #29 #31]: #32
+#14 := [asserted]: #12
+[mp #14 #33]: false
+7e6f4869abf700172472e795c9b4c6c255ad1fbe 37 0
unsat
-28b6536c2d4f9dc75412d00f15231ed2ee58fe03 41 0
#2 := false
decl f3 :: Int
#7 := f3
@@ -2210,35 +2470,31 @@
#11 := (+ f3 #10)
#14 := (= #11 #13)
#15 := (not #14)
-#59 := (iff #15 false)
+#40 := (iff #15 false)
#1 := true
-#54 := (not true)
-#57 := (iff #54 false)
-#58 := [rewrite]: #57
-#55 := (iff #15 #54)
-#52 := (iff #14 true)
-#47 := (= #11 #11)
-#50 := (iff #47 true)
-#51 := [rewrite]: #50
-#48 := (iff #14 #47)
-#45 := (= #13 #11)
-#37 := (+ f3 f5)
-#40 := (+ f4 #37)
-#43 := (= #40 #11)
-#44 := [rewrite]: #43
-#41 := (= #13 #40)
-#38 := (= #12 #37)
+#35 := (not true)
+#38 := (iff #35 false)
#39 := [rewrite]: #38
-#42 := [monotonicity #39]: #41
-#46 := [trans #42 #44]: #45
-#49 := [monotonicity #46]: #48
-#53 := [trans #49 #51]: #52
-#56 := [monotonicity #53]: #55
-#60 := [trans #56 #58]: #59
-#36 := [asserted]: #15
-[mp #36 #60]: false
+#36 := (iff #15 #35)
+#33 := (iff #14 true)
+#24 := (+ f4 f5 f3)
+#21 := (+ f3 f4 f5)
+#27 := (= #21 #24)
+#31 := (iff #27 true)
+#32 := [rewrite]: #31
+#28 := (iff #14 #27)
+#25 := (= #13 #24)
+#26 := [rewrite]: #25
+#22 := (= #11 #21)
+#23 := [rewrite]: #22
+#29 := [monotonicity #23 #26]: #28
+#34 := [trans #29 #32]: #33
+#37 := [monotonicity #34]: #36
+#41 := [trans #37 #39]: #40
+#17 := [asserted]: #15
+[mp #17 #41]: false
+a824144d3163a12246d06059fe9af86abcf7fb10 48 0
unsat
-8450cf6a350ba6ec26331e50c3fd5d8f999ad9a0 35 0
#2 := false
#8 := 3::Int
#9 := 8::Int
@@ -2247,34 +2503,46 @@
#7 := 5::Int
#12 := (< 5::Int #11)
#13 := (not #12)
-#58 := (iff #13 false)
+#54 := (iff #13 false)
#1 := true
-#53 := (not true)
-#56 := (iff #53 false)
-#57 := [rewrite]: #56
-#54 := (iff #13 #53)
-#51 := (iff #12 true)
-#46 := (< 5::Int 8::Int)
-#49 := (iff #46 true)
-#50 := [rewrite]: #49
-#47 := (iff #12 #46)
-#44 := (= #11 8::Int)
-#39 := (if true 8::Int 3::Int)
-#42 := (= #39 8::Int)
-#43 := [rewrite]: #42
-#40 := (= #11 #39)
-#37 := (iff #10 true)
-#38 := [rewrite]: #37
-#41 := [monotonicity #38]: #40
-#45 := [trans #41 #43]: #44
-#48 := [monotonicity #45]: #47
-#52 := [trans #48 #50]: #51
-#55 := [monotonicity #52]: #54
-#59 := [trans #55 #57]: #58
-#34 := [asserted]: #13
-[mp #34 #59]: false
-unsat
-6afccd7c6734a9f80c327ff8b0bab36d43ee827b 216 0
+#49 := (not true)
+#52 := (iff #49 false)
+#53 := [rewrite]: #52
+#50 := (iff #13 #49)
+#47 := (iff #12 true)
+#32 := (<= 8::Int 5::Int)
+#33 := (not #32)
+#45 := (iff #33 true)
+#40 := (not false)
+#43 := (iff #40 true)
+#44 := [rewrite]: #43
+#41 := (iff #33 #40)
+#38 := (iff #32 false)
+#39 := [rewrite]: #38
+#42 := [monotonicity #39]: #41
+#46 := [trans #42 #44]: #45
+#36 := (iff #12 #33)
+#29 := (< 5::Int 8::Int)
+#34 := (iff #29 #33)
+#35 := [rewrite]: #34
+#30 := (iff #12 #29)
+#27 := (= #11 8::Int)
+#22 := (if true 8::Int 3::Int)
+#25 := (= #22 8::Int)
+#26 := [rewrite]: #25
+#23 := (= #11 #22)
+#20 := (iff #10 true)
+#21 := [rewrite]: #20
+#24 := [monotonicity #21]: #23
+#28 := [trans #24 #26]: #27
+#31 := [monotonicity #28]: #30
+#37 := [trans #31 #35]: #36
+#48 := [trans #37 #46]: #47
+#51 := [monotonicity #48]: #50
+#55 := [trans #51 #53]: #54
+#15 := [asserted]: #13
+[mp #15 #55]: false
+8b049c9c7421dfc8c62639e17338cbd84ff8a029 216 0
#2 := false
#10 := 0::Real
decl f4 :: Real
@@ -2491,7 +2759,7 @@
#240 := [unit-resolution #189 #239]: #155
[th-lemma arith farkas -1 -1 1 1 #240 #217 #127 #238]: false
unsat
-c722596cfa285e209992f7087932c1ec15fd226b 42 0
+2130c0a211865d32db21d0798ef35056b373441f 42 0
#2 := false
decl f3 :: (-> S1 S2)
decl f1 :: S1
@@ -2534,7 +2802,7 @@
#35 := [asserted]: #14
[mp #35 #61]: false
unsat
-4d8a8a08b49cb28d987bdc1bcdbb3a144907bf45 49 0
+962a57e270a873c5fccc9aa943c37c86be9989bb 49 0
#2 := false
#12 := 1::Int
decl f3 :: Int
@@ -2584,7 +2852,7 @@
#36 := [asserted]: #15
[mp #36 #70]: false
unsat
-8bd98db330c82b711ec70353229651c63b6517b9 63 0
+2afccb348df223d2e9a13eda20d89b37612cbef1 63 0
#2 := false
#14 := 0::Int
decl f4 :: Int
@@ -2648,7 +2916,7 @@
#83 := [mp #59 #82]: #70
[mp #83 #95]: false
unsat
-e799a1569bcb7c90a4ec458d9136d7c6af5e039d 35 0
+b910449e10d880c681c7024f160f5239d3b9f56e 35 0
#2 := false
#9 := 5::Int
#7 := 2::Int
@@ -2684,7 +2952,7 @@
#33 := [asserted]: #12
[mp #33 #57]: false
unsat
-94bbb14edc8e8a8aac37f1ba3711bbb03b5ccb30 45 0
+31cab35b749e92f0f69d54060a3adf77628fdcc3 45 0
#2 := false
#14 := 4::Real
decl f4 :: Real
@@ -2730,7 +2998,7 @@
#67 := [mp #43 #66]: #58
[th-lemma arith farkas 7 3/2 1 #67 #54 #45]: false
unsat
-4588f343772c15f1f661bad429073998929c6598 59 0
+70d100587a22b3aac8b6223ca69d10fc4232fd77 59 0
#2 := false
#19 := (not false)
decl f4 :: Int
@@ -2790,181 +3058,7 @@
#41 := [asserted]: #21
[mp #41 #78]: false
unsat
-78003574b5d95d4c28641909502b0f435784ad24 104 0
-#2 := false
-decl f1 :: S1
-#3 := f1
-decl f2 :: S1
-#4 := f2
-#8 := 3::Int
-decl f3 :: Int
-#7 := f3
-#49 := (>= f3 3::Int)
-#54 := (if #49 f2 f1)
-#76 := (= f1 #54)
-#61 := (if #49 f1 f2)
-#71 := (= f1 #61)
-#118 := (iff #71 #76)
-#116 := (iff #76 #71)
-#64 := (= #54 #61)
-#11 := (<= 3::Int f3)
-#12 := (if #11 f1 f2)
-#9 := (< f3 3::Int)
-#10 := (if #9 f1 f2)
-#13 := (distinct #10 #12)
-#14 := (not #13)
-#67 := (iff #14 #64)
-#36 := (= #10 #12)
-#65 := (iff #36 #64)
-#62 := (= #12 #61)
-#59 := (iff #11 #49)
-#60 := [rewrite]: #59
-#63 := [monotonicity #60]: #62
-#57 := (= #10 #54)
-#47 := (not #49)
-#51 := (if #47 f1 f2)
-#55 := (= #51 #54)
-#56 := [rewrite]: #55
-#52 := (= #10 #51)
-#48 := (iff #9 #47)
-#50 := [rewrite]: #48
-#53 := [monotonicity #50]: #52
-#58 := [trans #53 #56]: #57
-#66 := [monotonicity #58 #63]: #65
-#45 := (iff #14 #36)
-#37 := (not #36)
-#40 := (not #37)
-#43 := (iff #40 #36)
-#44 := [rewrite]: #43
-#41 := (iff #14 #40)
-#38 := (iff #13 #37)
-#39 := [rewrite]: #38
-#42 := [monotonicity #39]: #41
-#46 := [trans #42 #44]: #45
-#68 := [trans #46 #66]: #67
-#35 := [asserted]: #14
-#69 := [mp #35 #68]: #64
-#117 := [monotonicity #69]: #116
-#119 := [symm #117]: #118
-#112 := (not #76)
-#5 := (= f1 f2)
-#72 := (= f2 #61)
-#108 := (iff #72 #5)
-#106 := (iff #5 #72)
-#101 := (= #61 f2)
-#104 := (iff #101 #72)
-#105 := [commutativity]: #104
-#102 := (iff #5 #101)
-#99 := [hypothesis]: #76
-#100 := [trans #99 #69]: #71
-#103 := [monotonicity #100]: #102
-#107 := [trans #103 #105]: #106
-#109 := [symm #107]: #108
-#75 := (= f2 #54)
-#87 := (iff #75 #72)
-#88 := [monotonicity #69]: #87
-#89 := (iff #72 #75)
-#90 := [symm #88]: #89
-#83 := (not #75)
-#84 := [hypothesis]: #83
-#77 := (or #47 #75)
-#78 := [def-axiom]: #77
-#85 := [unit-resolution #78 #84]: #47
-#81 := (or #49 #72)
-#82 := [def-axiom]: #81
-#86 := [unit-resolution #82 #85]: #72
-#91 := [mp #86 #90]: #75
-#92 := [unit-resolution #84 #91]: false
-#93 := [lemma #92]: #75
-#96 := [mp #93 #88]: #72
-#94 := (not #72)
-#95 := [hypothesis]: #94
-#97 := [unit-resolution #95 #96]: false
-#98 := [lemma #97]: #72
-#110 := [mp #98 #109]: #5
-#6 := (not #5)
-#34 := [asserted]: #6
-#111 := [unit-resolution #34 #110]: false
-#113 := [lemma #111]: #112
-#73 := (or #49 #76)
-#74 := [def-axiom]: #73
-#114 := [unit-resolution #74 #113]: #49
-#79 := (or #47 #71)
-#80 := [def-axiom]: #79
-#115 := [unit-resolution #80 #114]: #71
-#120 := [mp #115 #119]: #76
-[unit-resolution #113 #120]: false
-unsat
-5d7df2dbd3da6509a839adcbe280f54ee342d7d8 68 0
-#2 := false
-#7 := 0::Int
-decl f3 :: Int
-#8 := f3
-#10 := 2::Int
-#36 := (* 2::Int f3)
-#58 := (= #36 0::Int)
-#59 := (not #58)
-#62 := (= f3 0::Int)
-#63 := (not #62)
-#60 := (= f3 #36)
-#61 := (not #60)
-#56 := (and #61 #63 #59)
-#69 := (not #56)
-#46 := (distinct f3 #36 0::Int)
-#49 := (not #46)
-#12 := (- f3 f3)
-#11 := (* f3 2::Int)
-#13 := (distinct f3 #11 #12)
-#14 := (not #13)
-#50 := (iff #14 #49)
-#47 := (iff #13 #46)
-#44 := (= #12 0::Int)
-#45 := [rewrite]: #44
-#42 := (= #11 #36)
-#43 := [rewrite]: #42
-#48 := [monotonicity #43 #45]: #47
-#51 := [monotonicity #48]: #50
-#35 := [asserted]: #14
-#54 := [mp #35 #51]: #49
-#80 := (or #46 #69)
-#81 := [def-axiom]: #80
-#82 := [unit-resolution #81 #54]: #69
-#67 := (<= #36 0::Int)
-#83 := (not #67)
-#37 := (<= f3 0::Int)
-#38 := (not #37)
-#9 := (< 0::Int f3)
-#39 := (iff #9 #38)
-#40 := [rewrite]: #39
-#34 := [asserted]: #9
-#41 := [mp #34 #40]: #38
-#84 := (or #83 #37)
-#85 := [th-lemma arith assign-bounds 2]: #84
-#86 := [unit-resolution #85 #41]: #83
-#87 := (or #59 #67)
-#88 := [th-lemma arith triangle-eq]: #87
-#89 := [unit-resolution #88 #86]: #59
-#57 := -1::Int
-#53 := (* -1::Int #36)
-#55 := (+ f3 #53)
-#65 := (>= #55 0::Int)
-#90 := (not #65)
-#91 := (or #90 #37)
-#92 := [th-lemma arith assign-bounds 1]: #91
-#93 := [unit-resolution #92 #41]: #90
-#94 := (or #61 #65)
-#95 := [th-lemma arith triangle-eq]: #94
-#96 := [unit-resolution #95 #93]: #61
-#100 := (or #56 #60 #58)
-#97 := (or #63 #37)
-#98 := [th-lemma arith triangle-eq]: #97
-#99 := [unit-resolution #98 #41]: #63
-#76 := (or #56 #60 #62 #58)
-#77 := [def-axiom]: #76
-#101 := [unit-resolution #77 #99]: #100
-[unit-resolution #101 #96 #89 #82]: false
-unsat
-adcd90d27a640d65adf92b737298d76a88dcb2d7 439 0
+b1114e42b528a3f3368f02584a60d74e21ce36f3 439 0
#2 := false
decl f4 :: Int
#8 := f4
@@ -3404,7 +3498,7 @@
#497 := [unit-resolution #456 #496 #490]: #20
[unit-resolution #497 #501]: false
unsat
-c461f417e01961729e64bc338da8fe68ac7ad70e 2215 0
+85045dafb5b814ffc5cbcd5ff6b6686db0c031a5 2215 0
#2 := false
decl f12 :: Int
#52 := f12
@@ -5620,7 +5714,7 @@
#2264 := [unit-resolution #1544 #2263 #2262]: #65
[unit-resolution #658 #2264 #2259]: false
unsat
-ebb9b9eba458556c3c96e64ab347c2dd794296aa 52 0
+c69d5d4255e8606842bc591eb455581408ecf173 52 0
#2 := false
#11 := 1::Real
decl f3 :: Real
@@ -5673,7 +5767,7 @@
#37 := [asserted]: #16
[mp #37 #73]: false
unsat
-7284d3250d19a32079c86839237365aa695997b1 341 0
+831d28afa9cf941930d32bdaa862b9ddf2a718a5 341 0
#2 := false
#24 := 0::Int
decl f3 :: Int
@@ -6015,7 +6109,7 @@
#652 := [unit-resolution #646 #666]: #755
[unit-resolution #652 #650 #649]: false
unsat
-cf5adef89e3e53946521876e9bc33cdee144fbaf 343 0
+939e3758e2e10d03fb65ec30390e9e486d20dc8e 343 0
#2 := false
#23 := 0::Int
decl f3 :: Int
@@ -6359,7 +6453,7 @@
#635 := [unit-resolution #634 #645]: #750
[unit-resolution #635 #630 #629]: false
unsat
-cfa8a4e8b0964986b89eaf37e6038032e9b8b0d6 101 0
+74ff14110bbb0018e1d9b2bb1ca338d7d58b9ba7 101 0
#2 := false
#8 := 0::Real
decl f3 :: Real
@@ -6461,7 +6555,7 @@
#122 := [th-lemma arith triangle-eq]: #121
[unit-resolution #122 #118 #111 #45]: false
unsat
-0e941ae848fda6bf9dfac1fd97560c61c65c1f6a 916 0
+5d74029d261367c40f523c70d0425e39aa05656a 916 0
#2 := false
#22 := 1::Int
decl f3 :: (-> S2 Int Int)
@@ -7378,7 +7472,7 @@
#1665 := [unit-resolution #1640 #1664 #1654 #1663]: #1266
[unit-resolution #1468 #1665 #1662]: false
unsat
-c04d38458726eb1b2cafd52bd3881d6f8160666f 24 0
+708c54fa92a38587409efdd16c74ec37e20e2b24 24 0
#2 := false
#7 := (exists (vars (?v0 Int)) false)
#8 := (not #7)
@@ -7403,7 +7497,7 @@
#30 := [asserted]: #9
[mp #30 #46]: false
unsat
-b7e68d81e2b1e168216a793b1d4c3fb61e54a4fa 24 0
+fc6d81b59098b37bdb85891cea739cff88a4cdb6 24 0
#2 := false
#7 := (exists (vars (?v0 Real)) false)
#8 := (not #7)
@@ -7428,13 +7522,13 @@
#30 := [asserted]: #9
[mp #30 #46]: false
unsat
-091ba9e3776453f72e577cca020359bfc2bbb1a8 1 0
+0af127c441080d9be87ef936c6f900945a11800e 1 0
unsat
-6b48d925e625c5baa918d61afc02b3d6fa4e46f8 1 0
+39442bd44c6b81734dce64f48a2e8cfe6d7ef53b 1 0
unsat
-7b03d36f70c1cb511c7ddbbd8c6bb360b0e823ac 1 0
+92a9cdc5e3be1caf16415f275672ba72e11bb4d1 1 0
unsat
-770827669678f8e68bf300baf101a56cec1c8d6b 54 0
+75d80d6072d013ed3e949f6837066b1429f3d619 54 0
#2 := false
#11 := 1::Int
#8 := 0::Int
@@ -7489,7 +7583,7 @@
#136 := [trans #134 #72]: #135
[mp #136 #138]: false
unsat
-2d33526ae6f55fa8bf28af8a491289a10023ebc3 82 0
+92fd6555d299024a17bfc17027870ad0919243ff 82 0
#2 := false
#8 := (:var 0 Int)
#10 := 0::Int
@@ -7572,7 +7666,7 @@
#37 := [asserted]: #17
[mp #37 #103]: false
unsat
-faa0ca9568a00467876bf060199376e2ca905359 78 0
+46de1bc1af5e350ddd1b0ad779cbf855c1a471a1 78 0
#2 := false
#8 := (:var 0 Int)
#10 := 2::Int
@@ -7651,7 +7745,7 @@
#39 := [asserted]: #18
[mp #39 #99]: false
unsat
-05a0d5d1100f50948c093c944115de9816b9e0d9 56 0
+b862ad22dd9ecdb24d22ad71d0b47057aeade516 56 0
#2 := false
#12 := (:var 0 Int)
#7 := 2::Int
@@ -7708,7 +7802,7 @@
#38 := [asserted]: #17
[mp #38 #78]: false
unsat
-cb31e6f6a1ecdcd5cb5be0830fe96dcd6a225db2 89 0
+d22de288e1e6fa553e6f3d0d9c4c72eaac8ba9f7 89 0
#2 := false
#7 := 2::Int
decl ?v0!1 :: Int
@@ -7798,7 +7892,7 @@
#174 := [unit-resolution #172 #84]: #173
[unit-resolution #174 #111 #110]: false
unsat
-14c5d2b27aee290cf4e7c2c280797baa69660461 89 0
+bbb79358278efd2f50b5374712065c2bd5509427 89 0
#2 := false
#7 := 0::Int
decl ?v0!0 :: Int
@@ -7888,7 +7982,8 @@
#178 := [unit-resolution #165 #97]: #177
[unit-resolution #178 #176 #173]: false
unsat
-74ffecf155cc435ac1a2bcfe873a84647e4ce6b1 83 2
+f8d6fcfb2c146004937d3e2687f80fb7b9e71e08 84 0
+WARNING: failed to find a pattern for quantifier (quantifier id: k!10)
#2 := false
#8 := 0::Int
#7 := (:var 0 Int)
@@ -7972,9 +8067,8 @@
#63 := [mp~ #61 #70]: #56
[unit-resolution #63 #529]: false
unsat
+98ea18bb7ed4825aeaf82772b27a9684cb2bed9f 165 0
WARNING: failed to find a pattern for quantifier (quantifier id: k!10)
-
-8602f0cbb8a6b885b19d4424fa42859ac2937970 164 2
#2 := false
#7 := 0::Int
#8 := (:var 0 Int)
@@ -8139,9 +8233,7 @@
#563 := [unit-resolution #136 #574]: #62
[unit-resolution #563 #570]: false
unsat
-WARNING: failed to find a pattern for quantifier (quantifier id: k!10)
-
-2f9041ab2507988941f04b373596319a25dbff04 63 0
+41a9dc7919d6df65f060b1b899094fbf1d9ad6ba 63 0
#2 := false
#15 := 1::Int
#12 := (:var 1 Int)
@@ -8205,7 +8297,7 @@
#40 := [asserted]: #19
[mp #40 #87]: false
unsat
-e7e4f914c64da4bb9f5ff1d016939e644d6e9497 101 0
+6912c1751294e15845c5073be78e1e9aebf84cf9 101 0
#2 := false
#7 := 0::Int
decl ?v1!1 :: Int
@@ -8307,7 +8399,7 @@
#125 := [and-elim #108]: #88
[th-lemma arith farkas 1 1 1 #125 #124 #126]: false
unsat
-68c837c3dabb51cfb3fa72be140feeef8d58aa35 99 0
+602658d510491230a33b4d0db4cf9ef889fff5d2 99 0
#2 := false
#39 := -1::Int
decl ?v1!1 :: Int
@@ -8407,7 +8499,7 @@
#180 := [unit-resolution #179 #118]: #107
[unit-resolution #180 #120]: false
unsat
-111e0e11b10e3dfb46a207e5da98c171ac0c63ad 143 0
+985c93e0a5f1ce8a2da959ba74511df9451610ad 143 0
#2 := false
#10 := 0::Int
#8 := (:var 0 Int)
@@ -8551,7 +8643,8 @@
#160 := [mp #128 #159]: #155
[mp #160 #183]: false
unsat
-f97f94cdf9ea1da48e107362c172b39f4b82d4a8 66 2
+63d20accf8ad42641c987f5442607c5721cb43fb 67 0
+ERROR: line 11 column 83: invalid pattern.
#2 := false
decl f3 :: Int
#8 := f3
@@ -8618,9 +8711,7 @@
#37 := [asserted]: #16
[mp #37 #86]: false
unsat
-ERROR: line 11 column 83: invalid pattern.
-
-1953a39a3cc38daf2fde4846aa1d5cbc2ff95785 54 0
+1cfe9564946e052422f3734e258f62595f0a9412 54 0
#2 := false
#10 := 1::Int
decl ?v1!0 :: Int
@@ -8675,9 +8766,9 @@
#139 := [unit-resolution #138 #78]: #62
[unit-resolution #139 #79]: false
unsat
-8f616b17d0807409dc26bfdf9593c5fcd06fb7e7 1 0
+c22c22b3ba012feae782c7385953ed357b59b45c 1 0
unsat
-3eb9cf11ee8774c9212c37c265e7552f3b8f24a9 75 0
+341447bcaf93988f0b7d6678a14d4c50e4db9b7f 75 0
#2 := false
#9 := 1::Int
decl f5 :: Int
@@ -8753,7 +8844,7 @@
#40 := [asserted]: #19
[mp #40 #94]: false
unsat
-741a564e40e4b6610d1d47bdab19a223e004482a 62 0
+d5d80b9320d4c205de1be4e0283a62bbca18eb64 62 0
#2 := false
decl f4 :: Real
#9 := f4
@@ -8816,7 +8907,7 @@
#40 := [asserted]: #19
[mp #40 #82]: false
unsat
-06d1bd5308956fb019ef1c09bf97c6326d872fd6 141 0
+e45dae900e2e0eeb849f9514267495ab98a945b1 141 0
#2 := false
decl f6 :: Int
#12 := f6
@@ -8958,7 +9049,7 @@
#53 := [asserted]: #32
[mp #53 #158]: false
unsat
-d578ad7e6589d737d5b50614f48a1b12ef69c636 37 0
+7e345b8256329432a24c0098659af0d0da3f8b9c 37 0
#2 := false
#10 := 0::Int
decl f3 :: Int
@@ -8996,7 +9087,7 @@
#53 := [not-or-elim #52]: #11
[th-lemma arith farkas 1 1 1 #53 #57 #55]: false
unsat
-33e2bdae82fc59f778e5db15565f1c50c2c2fee4 225 0
+173dcd56c4eb3955c1a0afe5894b9f20d665d5a4 225 0
#2 := false
#24 := 0::Int
decl f5 :: (-> S4 S3 Int)
@@ -9222,7 +9313,7 @@
#527 := [unit-resolution #526 #425]: #550
[th-lemma arith gcd-test -1/2 -1/2 -1/2 -1/2 #529 #527 #515 #524]: false
unsat
-d558048bb276c46209081d2fdff3fd787837bb57 55 0
+10b9b3d3225e279927703a7138fa37357bc1a2b4 55 0
#2 := false
#74 := 4::Int
decl f3 :: (-> S2 S3 Int)
@@ -9278,7 +9369,7 @@
#301 := [unit-resolution #216 #88]: #76
[unit-resolution #301 #89]: false
unsat
-8932fefe7cf3366bddd35470f58d0b1fde78bc6e 270 0
+83084ab04d727810863c900d9684257895074106 270 0
#2 := false
#7 := 0::Int
decl f3 :: (-> S2 S3 Int)
@@ -9549,7 +9640,7 @@
#90 := [mp #57 #89]: #77
[th-lemma arith farkas -1 -1 1 #90 #519 #518]: false
unsat
-68d347fdf181bb23634330d38e10cbe4fff1953a 269 0
+0c91cb6bf3bcb8a10a4871e9ec475b571f03d883 269 0
#2 := false
#7 := 0::Int
decl f3 :: (-> S2 S3 Int)
@@ -9819,382 +9910,7 @@
#580 := [unit-resolution #596 #594]: #654
[th-lemma arith farkas 1 -1 -1 1 #600 #119 #580 #609]: false
unsat
-9bd1c4986d286e4e0abfd70c7740b5ad11395fe6 374 0
-#2 := false
-decl f5 :: (-> S4 S3 Int)
-decl f3 :: (-> S2 Int S3)
-decl f7 :: S3
-#9 := f7
-decl f6 :: S4
-#8 := f6
-#10 := (f5 f6 f7)
-#11 := 1::Int
-#60 := (+ 1::Int #10)
-decl f4 :: S2
-#7 := f4
-#63 := (f3 f4 #60)
-#622 := (f5 f6 #63)
-#14 := 2::Int
-#66 := (* 2::Int #10)
-#16 := 3::Int
-#72 := (+ 3::Int #66)
-#77 := (f3 f4 #72)
-#588 := (f5 f6 #77)
-#399 := (= #588 #622)
-#387 := (= #622 #588)
-#217 := (= #63 #77)
-#28 := 0::Int
-#82 := (f3 f4 0::Int)
-#304 := (= #77 #82)
-#295 := (not #304)
-#573 := (= #588 0::Int)
-#566 := (f5 f6 #82)
-#563 := (= #566 0::Int)
-#29 := (:var 0 Int)
-#31 := (f3 f4 #29)
-#639 := (pattern #31)
-#32 := (f5 f6 #31)
-#33 := (= #32 #29)
-#103 := (>= #29 0::Int)
-#104 := (not #103)
-#107 := (or #104 #33)
-#640 := (forall (vars (?v0 Int)) (:pat #639) #107)
-#110 := (forall (vars (?v0 Int)) #107)
-#643 := (iff #110 #640)
-#641 := (iff #107 #107)
-#642 := [refl]: #641
-#644 := [quant-intro #642]: #643
-#147 := (~ #110 #110)
-#146 := (~ #107 #107)
-#143 := [refl]: #146
-#148 := [nnf-pos #143]: #147
-#30 := (<= 0::Int #29)
-#34 := (implies #30 #33)
-#35 := (forall (vars (?v0 Int)) #34)
-#113 := (iff #35 #110)
-#94 := (not #30)
-#95 := (or #94 #33)
-#98 := (forall (vars (?v0 Int)) #95)
-#111 := (iff #98 #110)
-#108 := (iff #95 #107)
-#105 := (iff #94 #104)
-#101 := (iff #30 #103)
-#102 := [rewrite]: #101
-#106 := [monotonicity #102]: #105
-#109 := [monotonicity #106]: #108
-#112 := [quant-intro #109]: #111
-#99 := (iff #35 #98)
-#96 := (iff #34 #95)
-#97 := [rewrite]: #96
-#100 := [quant-intro #97]: #99
-#114 := [trans #100 #112]: #113
-#92 := [asserted]: #35
-#115 := [mp #92 #114]: #110
-#144 := [mp~ #115 #148]: #110
-#645 := [mp #144 #644]: #640
-#615 := (not #640)
-#537 := (or #615 #563)
-#472 := (>= 0::Int 0::Int)
-#473 := (not #472)
-#567 := (or #473 #563)
-#538 := (or #615 #567)
-#541 := (iff #538 #537)
-#543 := (iff #537 #537)
-#539 := [rewrite]: #543
-#546 := (iff #567 #563)
-#560 := (or false #563)
-#551 := (iff #560 #563)
-#552 := [rewrite]: #551
-#549 := (iff #567 #560)
-#559 := (iff #473 false)
-#1 := true
-#548 := (not true)
-#557 := (iff #548 false)
-#558 := [rewrite]: #557
-#545 := (iff #473 #548)
-#554 := (iff #472 true)
-#556 := [rewrite]: #554
-#547 := [monotonicity #556]: #545
-#555 := [trans #547 #558]: #559
-#550 := [monotonicity #555]: #549
-#553 := [trans #550 #552]: #546
-#542 := [monotonicity #553]: #541
-#544 := [trans #542 #539]: #541
-#540 := [quant-inst #28]: #538
-#530 := [mp #540 #544]: #537
-#443 := [unit-resolution #530 #645]: #563
-#447 := (= #588 #566)
-#444 := [hypothesis]: #304
-#432 := [monotonicity #444]: #447
-#448 := [trans #432 #443]: #573
-#439 := (not #573)
-#470 := (<= #588 0::Int)
-#430 := (not #470)
-#628 := -1::Int
-#265 := (>= #10 -1::Int)
-#519 := (>= #10 0::Int)
-#480 := (= #10 0::Int)
-#629 := (f3 f4 #10)
-#520 := (f5 f6 #629)
-#521 := (= #520 0::Int)
-#374 := (not #519)
-#485 := [hypothesis]: #374
-#522 := (or #519 #521)
-#37 := (= #32 0::Int)
-#133 := (or #103 #37)
-#646 := (forall (vars (?v0 Int)) (:pat #639) #133)
-#136 := (forall (vars (?v0 Int)) #133)
-#649 := (iff #136 #646)
-#647 := (iff #133 #133)
-#648 := [refl]: #647
-#650 := [quant-intro #648]: #649
-#149 := (~ #136 #136)
-#157 := (~ #133 #133)
-#158 := [refl]: #157
-#150 := [nnf-pos #158]: #149
-#36 := (< #29 0::Int)
-#38 := (implies #36 #37)
-#39 := (forall (vars (?v0 Int)) #38)
-#139 := (iff #39 #136)
-#117 := (not #36)
-#118 := (or #117 #37)
-#121 := (forall (vars (?v0 Int)) #118)
-#137 := (iff #121 #136)
-#134 := (iff #118 #133)
-#131 := (iff #117 #103)
-#126 := (not #104)
-#129 := (iff #126 #103)
-#130 := [rewrite]: #129
-#127 := (iff #117 #126)
-#124 := (iff #36 #104)
-#125 := [rewrite]: #124
-#128 := [monotonicity #125]: #127
-#132 := [trans #128 #130]: #131
-#135 := [monotonicity #132]: #134
-#138 := [quant-intro #135]: #137
-#122 := (iff #39 #121)
-#119 := (iff #38 #118)
-#120 := [rewrite]: #119
-#123 := [quant-intro #120]: #122
-#140 := [trans #123 #138]: #139
-#116 := [asserted]: #39
-#141 := [mp #116 #140]: #136
-#159 := [mp~ #141 #150]: #136
-#651 := [mp #159 #650]: #646
-#599 := (not #646)
-#525 := (or #599 #519 #521)
-#526 := (or #599 #522)
-#528 := (iff #526 #525)
-#518 := [rewrite]: #528
-#527 := [quant-inst #10]: #526
-#529 := [mp #527 #518]: #525
-#486 := [unit-resolution #529 #651]: #522
-#487 := [unit-resolution #486 #485]: #521
-#490 := (= #10 #520)
-#488 := (= f7 #629)
-#630 := (= #629 f7)
-#23 := (:var 0 S3)
-#24 := (f5 f6 #23)
-#632 := (pattern #24)
-#25 := (f3 f4 #24)
-#26 := (= #25 #23)
-#633 := (forall (vars (?v0 S3)) (:pat #632) #26)
-#27 := (forall (vars (?v0 S3)) #26)
-#636 := (iff #27 #633)
-#634 := (iff #26 #26)
-#635 := [refl]: #634
-#637 := [quant-intro #635]: #636
-#155 := (~ #27 #27)
-#153 := (~ #26 #26)
-#154 := [refl]: #153
-#156 := [nnf-pos #154]: #155
-#91 := [asserted]: #27
-#145 := [mp~ #91 #156]: #27
-#638 := [mp #145 #637]: #633
-#621 := (not #633)
-#280 := (or #621 #630)
-#285 := [quant-inst #9]: #280
-#492 := [unit-resolution #285 #638]: #630
-#489 := [symm #492]: #488
-#493 := [monotonicity #489]: #490
-#494 := [trans #493 #487]: #480
-#495 := (not #480)
-#491 := (or #495 #519)
-#496 := [th-lemma arith triangle-eq]: #491
-#476 := [unit-resolution #496 #485 #494]: false
-#422 := [lemma #476]: #519
-#418 := (or #374 #265)
-#449 := [th-lemma arith farkas 1 1]: #418
-#474 := [unit-resolution #449 #422]: #265
-#434 := -3::Int
-#435 := (* -1::Int #588)
-#577 := (+ #66 #435)
-#572 := (<= #577 -3::Int)
-#578 := (= #577 -3::Int)
-#270 := (not #265)
-#579 := (or #270 #578)
-#575 := (or #615 #270 #578)
-#589 := (= #588 #72)
-#598 := (>= #72 0::Int)
-#587 := (not #598)
-#584 := (or #587 #589)
-#581 := (or #615 #584)
-#568 := (iff #581 #575)
-#576 := (or #615 #579)
-#414 := (iff #576 #575)
-#415 := [rewrite]: #414
-#583 := (iff #581 #576)
-#580 := (iff #584 #579)
-#592 := (iff #589 #578)
-#433 := [rewrite]: #592
-#591 := (iff #587 #270)
-#585 := (iff #598 #265)
-#590 := [rewrite]: #585
-#586 := [monotonicity #590]: #591
-#574 := [monotonicity #586 #433]: #580
-#412 := [monotonicity #574]: #583
-#569 := [trans #412 #415]: #568
-#582 := [quant-inst #72]: #581
-#571 := [mp #582 #569]: #575
-#511 := [unit-resolution #571 #645]: #579
-#454 := [unit-resolution #511 #474]: #578
-#513 := (not #578)
-#514 := (or #513 #572)
-#509 := [th-lemma arith triangle-eq]: #514
-#475 := [unit-resolution #509 #454]: #572
-#431 := (not #572)
-#436 := (or #430 #431 #270)
-#437 := [th-lemma arith assign-bounds 1 2]: #436
-#438 := [unit-resolution #437 #475 #474]: #430
-#440 := (or #439 #470)
-#441 := [th-lemma arith triangle-eq]: #440
-#442 := [unit-resolution #441 #438]: #439
-#409 := [unit-resolution #442 #448]: false
-#410 := [lemma #409]: #295
-#218 := (= #63 #82)
-#303 := (not #218)
-#224 := (= #622 0::Int)
-#401 := (= #622 #566)
-#429 := [hypothesis]: #218
-#402 := [monotonicity #429]: #401
-#404 := [trans #402 #443]: #224
-#426 := (not #224)
-#597 := (<= #622 0::Int)
-#420 := (not #597)
-#611 := (* -1::Int #622)
-#612 := (+ #10 #611)
-#330 := (<= #612 -1::Int)
-#610 := (= #612 -1::Int)
-#608 := (or #270 #610)
-#617 := (or #615 #270 #610)
-#281 := (= #622 #60)
-#625 := (>= #60 0::Int)
-#631 := (not #625)
-#623 := (or #631 #281)
-#256 := (or #615 #623)
-#313 := (iff #256 #617)
-#618 := (or #615 #608)
-#605 := (iff #618 #617)
-#606 := [rewrite]: #605
-#616 := (iff #256 #618)
-#614 := (iff #623 #608)
-#609 := (iff #281 #610)
-#613 := [rewrite]: #609
-#271 := (iff #631 #270)
-#607 := (iff #625 #265)
-#269 := [rewrite]: #607
-#272 := [monotonicity #269]: #271
-#251 := [monotonicity #272 #613]: #614
-#619 := [monotonicity #251]: #616
-#328 := [trans #619 #606]: #313
-#257 := [quant-inst #60]: #256
-#329 := [mp #257 #328]: #617
-#501 := [unit-resolution #329 #645]: #608
-#445 := [unit-resolution #501 #474]: #610
-#498 := (not #610)
-#446 := (or #498 #330)
-#417 := [th-lemma arith triangle-eq]: #446
-#419 := [unit-resolution #417 #445]: #330
-#421 := (not #330)
-#423 := (or #420 #421 #374)
-#424 := [th-lemma arith assign-bounds 1 -1]: #423
-#425 := [unit-resolution #424 #419 #422]: #420
-#427 := (or #426 #597)
-#428 := [th-lemma arith triangle-eq]: #427
-#411 := [unit-resolution #428 #425]: #426
-#405 := [unit-resolution #411 #404]: false
-#406 := [lemma #405]: #303
-#407 := (or #217 #218 #304)
-#302 := (not #217)
-#306 := (and #302 #303 #295)
-#307 := (not #306)
-#85 := (distinct #63 #77 #82)
-#88 := (not #85)
-#19 := (- #10 #10)
-#20 := (f3 f4 #19)
-#15 := (* #10 2::Int)
-#17 := (+ #15 3::Int)
-#18 := (f3 f4 #17)
-#12 := (+ #10 1::Int)
-#13 := (f3 f4 #12)
-#21 := (distinct #13 #18 #20)
-#22 := (not #21)
-#89 := (iff #22 #88)
-#86 := (iff #21 #85)
-#83 := (= #20 #82)
-#80 := (= #19 0::Int)
-#81 := [rewrite]: #80
-#84 := [monotonicity #81]: #83
-#78 := (= #18 #77)
-#75 := (= #17 #72)
-#69 := (+ #66 3::Int)
-#73 := (= #69 #72)
-#74 := [rewrite]: #73
-#70 := (= #17 #69)
-#67 := (= #15 #66)
-#68 := [rewrite]: #67
-#71 := [monotonicity #68]: #70
-#76 := [trans #71 #74]: #75
-#79 := [monotonicity #76]: #78
-#64 := (= #13 #63)
-#61 := (= #12 #60)
-#62 := [rewrite]: #61
-#65 := [monotonicity #62]: #64
-#87 := [monotonicity #65 #79 #84]: #86
-#90 := [monotonicity #87]: #89
-#59 := [asserted]: #22
-#93 := [mp #59 #90]: #88
-#294 := (or #85 #307)
-#627 := [def-axiom]: #294
-#248 := [unit-resolution #627 #93]: #307
-#282 := (or #306 #217 #218 #304)
-#413 := [def-axiom]: #282
-#403 := [unit-resolution #413 #248]: #407
-#408 := [unit-resolution #403 #406 #410]: #217
-#390 := [monotonicity #408]: #387
-#394 := [symm #390]: #399
-#524 := (+ #588 #611)
-#507 := (<= #524 0::Int)
-#500 := (not #507)
-#506 := (or #270 #500)
-#510 := [hypothesis]: #265
-#512 := [unit-resolution #511 #510]: #578
-#515 := [unit-resolution #509 #512]: #572
-#331 := (>= #612 -1::Int)
-#497 := [unit-resolution #501 #510]: #610
-#499 := (or #498 #331)
-#502 := [th-lemma arith triangle-eq]: #499
-#503 := [unit-resolution #502 #497]: #331
-#504 := [hypothesis]: #507
-#505 := [th-lemma arith farkas -1 1 -1 1 #504 #503 #515 #510]: false
-#479 := [lemma #505]: #506
-#396 := [unit-resolution #479 #474]: #500
-#397 := (not #399)
-#395 := (or #397 #507)
-#398 := [th-lemma arith triangle-eq]: #395
-[unit-resolution #398 #396 #394]: false
-unsat
-b95d641e1affb872027fbe667ba2ad4475fc0039 147 0
+883f0bd08ff2fcce6dafab7dcff61923fd895e14 147 0
#2 := false
#10 := 0::Int
decl f7 :: Int
@@ -10342,7 +10058,8 @@
#338 := [unit-resolution #616 #618]: #641
[th-lemma arith farkas 1 1 1 #338 #262 #629]: false
unsat
-05afc7fcdcf1433af94de36ed38785db528a50f6 430 2
+0f3d54ed51fa30b450e38c23afe57212bbebc6dd 431 0
+WARNING: For problems containing quantifiers, the model finding capabilities of Z3 work better when the formula does not contain nested quantifiers. You can use PULL_NESTED_QUANTIFIERS=true to eliminate nested quantifiers.
#2 := false
#446 := -1::Int
decl f4 :: (-> S3 S2 Int)
@@ -10773,9 +10490,7 @@
#150 := [not-or-elim #147]: #149
[th-lemma arith farkas -4 1 1 #150 #622 #575]: false
unsat
-WARNING: For problems containing quantifiers, the model finding capabilities of Z3 work better when the formula does not contain nested quantifiers. You can use PULL_NESTED_QUANTIFIERS=true to eliminate nested quantifiers.
-
-8bbf55cbd9308f9edfe0203d9100aace31ed1b8b 58 0
+fd4d98b0eed13792693ae0a8136c6836082ab811 58 0
#2 := false
decl f8 :: S2
#18 := f8
@@ -10834,7 +10549,7 @@
#55 := [not-or-elim #54]: #53
[unit-resolution #55 #214]: false
unsat
-995e3c8bb1366c3ddfd69a100721f0bf4e72ec56 106 0
+54ed94e7408ff82930a92d4010c74312402c8de2 106 0
#2 := false
decl f11 :: (-> S9 S5 S3)
decl f16 :: S5
@@ -10941,7 +10656,7 @@
#80 := [not-or-elim #77]: #79
[unit-resolution #80 #217]: false
unsat
-29cfa5c687980cc2eca5b8b3a0340a9f66137754 113 0
+a973ebe0ddefe8f57f45047d94130cd1cb03b18f 113 0
#2 := false
decl f3 :: (-> S2 S3 S4)
decl f8 :: S3
@@ -11055,7 +10770,7 @@
#87 := [not-or-elim #84]: #86
[unit-resolution #87 #529]: false
unsat
-10c4eb4ff6b9f0c880cfc3af0cd433a1ff110114 74 0
+bb72677b6383b269d7de6046448ed8d87d1bc4ef 74 0
#2 := false
decl f1 :: S1
#3 := f1
@@ -11130,121 +10845,114 @@
#80 := [mp #69 #79]: #77
[mp #80 #82]: false
unsat
-8821f61b34007b1fd5b5c2b393b7f6276c9650d7 113 0
+53946fb2c677a4b873691332b928354017b0ad0e 106 0
#2 := false
-decl f7 :: (-> S5 Int S3)
-decl f9 :: (-> Int Int)
-decl f10 :: Int
-#20 := f10
-#21 := (f9 f10)
-#22 := (f9 #21)
-decl f8 :: S5
-#19 := f8
-#23 := (f7 f8 #22)
+decl f7 :: S3
+#19 := f7
decl f5 :: (-> S4 S3 S3)
decl f6 :: S4
#14 := f6
-#24 := (f5 f6 #23)
-#25 := (= #24 #23)
-#78 := (not #25)
+#20 := (f5 f6 f7)
+#21 := (= #20 f7)
+#74 := (not #21)
decl f1 :: S1
#3 := f1
decl f3 :: (-> S2 S1 S1)
decl f4 :: S2
#7 := f4
-#26 := (f3 f4 f1)
-#27 := (= #26 f1)
-#79 := (not #27)
-#562 := [hypothesis]: #79
+#22 := (f3 f4 f1)
+#23 := (= #22 f1)
+#75 := (not #23)
+#558 := [hypothesis]: #75
#8 := (:var 0 S1)
#9 := (f3 f4 #8)
-#566 := (pattern #9)
+#562 := (pattern #9)
#11 := (= #8 f1)
#10 := (= #9 f1)
#12 := (iff #10 #11)
-#567 := (forall (vars (?v0 S1)) (:pat #566) #12)
+#563 := (forall (vars (?v0 S1)) (:pat #562) #12)
#13 := (forall (vars (?v0 S1)) #12)
-#570 := (iff #13 #567)
-#568 := (iff #12 #12)
-#569 := [refl]: #568
-#571 := [quant-intro #569]: #570
-#74 := (~ #13 #13)
-#72 := (~ #12 #12)
-#73 := [refl]: #72
-#75 := [nnf-pos #73]: #74
-#51 := [asserted]: #13
-#63 := [mp~ #51 #75]: #13
-#572 := [mp #63 #571]: #567
-#243 := (not #567)
-#222 := (or #243 #27)
-#150 := (= f1 f1)
-#151 := (iff #27 #150)
-#558 := (or #243 #151)
-#216 := (iff #558 #222)
-#554 := (iff #222 #222)
-#227 := [rewrite]: #554
-#242 := (iff #151 #27)
+#566 := (iff #13 #563)
+#564 := (iff #12 #12)
+#565 := [refl]: #564
+#567 := [quant-intro #565]: #566
+#70 := (~ #13 #13)
+#68 := (~ #12 #12)
+#69 := [refl]: #68
+#71 := [nnf-pos #69]: #70
+#47 := [asserted]: #13
+#59 := [mp~ #47 #71]: #13
+#568 := [mp #59 #567]: #563
+#239 := (not #563)
+#218 := (or #239 #23)
+#146 := (= f1 f1)
+#147 := (iff #23 #146)
+#554 := (or #239 #147)
+#212 := (iff #554 #218)
+#550 := (iff #218 #218)
+#223 := [rewrite]: #550
+#238 := (iff #147 #23)
#1 := true
-#28 := (iff #27 true)
-#54 := (iff #28 #27)
-#55 := [rewrite]: #54
-#240 := (iff #151 #28)
-#236 := (iff #150 true)
-#229 := [rewrite]: #236
-#241 := [monotonicity #229]: #240
-#239 := [trans #241 #55]: #242
-#347 := [monotonicity #239]: #216
-#228 := [trans #347 #227]: #216
-#560 := [quant-inst #3]: #558
-#561 := [mp #560 #228]: #222
-#563 := [unit-resolution #561 #572 #562]: false
-#564 := [lemma #563]: #27
-#68 := (or #78 #79)
-#56 := (and #25 #27)
-#59 := (not #56)
-#85 := (iff #59 #68)
-#69 := (not #68)
-#80 := (not #69)
-#83 := (iff #80 #68)
-#84 := [rewrite]: #83
-#81 := (iff #59 #80)
-#70 := (iff #56 #69)
-#71 := [rewrite]: #70
-#82 := [monotonicity #71]: #81
-#86 := [trans #82 #84]: #85
-#29 := (and #25 #28)
-#30 := (not #29)
-#60 := (iff #30 #59)
-#57 := (iff #29 #56)
-#58 := [monotonicity #55]: #57
-#61 := [monotonicity #58]: #60
-#53 := [asserted]: #30
-#64 := [mp #53 #61]: #59
-#87 := [mp #64 #86]: #68
-#559 := [unit-resolution #87 #564]: #78
+#24 := (iff #23 true)
+#50 := (iff #24 #23)
+#51 := [rewrite]: #50
+#236 := (iff #147 #24)
+#232 := (iff #146 true)
+#225 := [rewrite]: #232
+#237 := [monotonicity #225]: #236
+#235 := [trans #237 #51]: #238
+#343 := [monotonicity #235]: #212
+#224 := [trans #343 #223]: #212
+#556 := [quant-inst #3]: #554
+#557 := [mp #556 #224]: #218
+#559 := [unit-resolution #557 #568 #558]: false
+#560 := [lemma #559]: #23
+#64 := (or #74 #75)
+#52 := (and #21 #23)
+#55 := (not #52)
+#81 := (iff #55 #64)
+#65 := (not #64)
+#76 := (not #65)
+#79 := (iff #76 #64)
+#80 := [rewrite]: #79
+#77 := (iff #55 #76)
+#66 := (iff #52 #65)
+#67 := [rewrite]: #66
+#78 := [monotonicity #67]: #77
+#82 := [trans #78 #80]: #81
+#25 := (and #21 #24)
+#26 := (not #25)
+#56 := (iff #26 #55)
+#53 := (iff #25 #52)
+#54 := [monotonicity #51]: #53
+#57 := [monotonicity #54]: #56
+#49 := [asserted]: #26
+#60 := [mp #49 #57]: #55
+#83 := [mp #60 #82]: #64
+#555 := [unit-resolution #83 #560]: #74
#15 := (:var 0 S3)
#16 := (f5 f6 #15)
-#573 := (pattern #16)
+#569 := (pattern #16)
#17 := (= #16 #15)
-#574 := (forall (vars (?v0 S3)) (:pat #573) #17)
+#570 := (forall (vars (?v0 S3)) (:pat #569) #17)
#18 := (forall (vars (?v0 S3)) #17)
-#577 := (iff #18 #574)
-#575 := (iff #17 #17)
-#576 := [refl]: #575
-#578 := [quant-intro #576]: #577
-#66 := (~ #18 #18)
-#65 := (~ #17 #17)
-#76 := [refl]: #65
-#67 := [nnf-pos #76]: #66
-#52 := [asserted]: #18
-#77 := [mp~ #52 #67]: #18
-#579 := [mp #77 #578]: #574
-#555 := (not #574)
-#214 := (or #555 #25)
-#219 := [quant-inst #23]: #214
-[unit-resolution #219 #579 #559]: false
+#573 := (iff #18 #570)
+#571 := (iff #17 #17)
+#572 := [refl]: #571
+#574 := [quant-intro #572]: #573
+#62 := (~ #18 #18)
+#61 := (~ #17 #17)
+#72 := [refl]: #61
+#63 := [nnf-pos #72]: #62
+#48 := [asserted]: #18
+#73 := [mp~ #48 #63]: #18
+#575 := [mp #73 #574]: #570
+#551 := (not #570)
+#210 := (or #551 #21)
+#215 := [quant-inst #19]: #210
+[unit-resolution #215 #575 #555]: false
unsat
-c2e9404480cb814492148c359fbbbb3b0e606571 29 0
+b9731ef54c4e3499fb2c009710dd563fdc4be6ee 29 0
#2 := false
#1 := true
decl f1 :: S1
@@ -11274,7 +10982,7 @@
#36 := [asserted]: #15
[mp #36 #45]: false
unsat
-343488aeda93da0c02f8ac1558cbc54ab37a2bb9 29 0
+c1459ffeaaac12de208e5b699c20294611368ff4 29 0
#2 := false
#1 := true
decl f1 :: S1
@@ -11304,7 +11012,7 @@
#36 := [asserted]: #15
[mp #36 #45]: false
unsat
-46a14fd6aa65cfd8a30d4b0b44a855a19c19f288 8 0
+bf2cd5b03536b5bd0602eda620854302cd150049 8 0
#2 := false
#1 := true
#23 := (not true)
@@ -11313,7 +11021,7 @@
#46 := [asserted]: #23
[mp #46 #48]: false
unsat
-ad406fc43130e24f380abadc1fc8a246fab490af 113 0
+89bfa27ccdaa7dcf714e523cef143bce280239ad 113 0
#2 := false
decl f1 :: S1
#3 := f1
@@ -11427,7 +11135,7 @@
#71 := [not-or-elim #70]: #69
[unit-resolution #71 #525]: false
unsat
-a5a23002374b3531b57fc274b72111cc0f0bdd3e 424 0
+273bebb141dbf0be0689bc04e07d9801bbd88484 424 0
#2 := false
decl f9 :: (-> S6 S7 S7)
decl f12 :: S7
@@ -11852,7 +11560,7 @@
#145 := [asserted]: #91
[unit-resolution #145 #373]: false
unsat
-b18aa009c5b54d915c2c9feecd9762a9bb0c27b5 24 0
+8ed6ae59787ef073a0f2ee12e54e0a9e18c847b1 24 0
#2 := false
decl f1 :: S1
#3 := f1
@@ -11877,7 +11585,7 @@
#34 := [asserted]: #13
[mp #34 #43]: false
unsat
-6484c4415dc032ed762d879b9df0ebba83c1370d 344 0
+0a480e932cf9544226aa308a652a130c00794519 344 0
#2 := false
decl f7 :: (-> S5 Int S2)
#28 := 6::Int
@@ -12222,9 +11930,9 @@
#107 := [asserted]: #31
[unit-resolution #107 #388]: false
unsat
-f954792d8be81671314fd3cce76fa4be3cd4ee23 1 0
+e9a200a4c01396af8a28649e89651e82c566aea6 1 0
unsat
-6fc5c498589f75255cd22f4154985bdeb92fa551 95 0
+a1b617e98026794f4fabc7b88d3c7c6545b77aeb 95 0
#2 := false
decl f1 :: S1
#3 := f1
@@ -12320,7 +12028,7 @@
#312 := [mp #310 #308]: #298
[unit-resolution #312 #641 #138 #139 #140]: false
unsat
-e776ea3cea49bcb73b17ecdacf5c2db068ae9e28 59 0
+faeea2438f581c39182be7618ceac231cf77a00a 59 0
#2 := false
decl f1 :: S1
#3 := f1
@@ -12380,7 +12088,7 @@
#339 := [quant-inst #70]: #338
[unit-resolution #339 #673 #163]: false
unsat
-2e1ce9e1ff9cb725a3a169498ce8fc405a17724f 394 0
+ed7e0385c3012dbbfdc71724063f8cbb116b4c06 394 0
#2 := false
decl f3 :: (-> S2 S3 S4)
decl f5 :: (-> S1 S3)
@@ -12775,110 +12483,3 @@
#247 := [asserted]: #123
[unit-resolution #247 #633]: false
unsat
-477e29453df08396d997096a4fc4a8771c735880 106 0
-#2 := false
-decl f7 :: S3
-#19 := f7
-decl f5 :: (-> S4 S3 S3)
-decl f6 :: S4
-#14 := f6
-#20 := (f5 f6 f7)
-#21 := (= #20 f7)
-#74 := (not #21)
-decl f1 :: S1
-#3 := f1
-decl f3 :: (-> S2 S1 S1)
-decl f4 :: S2
-#7 := f4
-#22 := (f3 f4 f1)
-#23 := (= #22 f1)
-#75 := (not #23)
-#558 := [hypothesis]: #75
-#8 := (:var 0 S1)
-#9 := (f3 f4 #8)
-#562 := (pattern #9)
-#11 := (= #8 f1)
-#10 := (= #9 f1)
-#12 := (iff #10 #11)
-#563 := (forall (vars (?v0 S1)) (:pat #562) #12)
-#13 := (forall (vars (?v0 S1)) #12)
-#566 := (iff #13 #563)
-#564 := (iff #12 #12)
-#565 := [refl]: #564
-#567 := [quant-intro #565]: #566
-#70 := (~ #13 #13)
-#68 := (~ #12 #12)
-#69 := [refl]: #68
-#71 := [nnf-pos #69]: #70
-#47 := [asserted]: #13
-#59 := [mp~ #47 #71]: #13
-#568 := [mp #59 #567]: #563
-#239 := (not #563)
-#218 := (or #239 #23)
-#146 := (= f1 f1)
-#147 := (iff #23 #146)
-#554 := (or #239 #147)
-#212 := (iff #554 #218)
-#550 := (iff #218 #218)
-#223 := [rewrite]: #550
-#238 := (iff #147 #23)
-#1 := true
-#24 := (iff #23 true)
-#50 := (iff #24 #23)
-#51 := [rewrite]: #50
-#236 := (iff #147 #24)
-#232 := (iff #146 true)
-#225 := [rewrite]: #232
-#237 := [monotonicity #225]: #236
-#235 := [trans #237 #51]: #238
-#343 := [monotonicity #235]: #212
-#224 := [trans #343 #223]: #212
-#556 := [quant-inst #3]: #554
-#557 := [mp #556 #224]: #218
-#559 := [unit-resolution #557 #568 #558]: false
-#560 := [lemma #559]: #23
-#64 := (or #74 #75)
-#52 := (and #21 #23)
-#55 := (not #52)
-#81 := (iff #55 #64)
-#65 := (not #64)
-#76 := (not #65)
-#79 := (iff #76 #64)
-#80 := [rewrite]: #79
-#77 := (iff #55 #76)
-#66 := (iff #52 #65)
-#67 := [rewrite]: #66
-#78 := [monotonicity #67]: #77
-#82 := [trans #78 #80]: #81
-#25 := (and #21 #24)
-#26 := (not #25)
-#56 := (iff #26 #55)
-#53 := (iff #25 #52)
-#54 := [monotonicity #51]: #53
-#57 := [monotonicity #54]: #56
-#49 := [asserted]: #26
-#60 := [mp #49 #57]: #55
-#83 := [mp #60 #82]: #64
-#555 := [unit-resolution #83 #560]: #74
-#15 := (:var 0 S3)
-#16 := (f5 f6 #15)
-#569 := (pattern #16)
-#17 := (= #16 #15)
-#570 := (forall (vars (?v0 S3)) (:pat #569) #17)
-#18 := (forall (vars (?v0 S3)) #17)
-#573 := (iff #18 #570)
-#571 := (iff #17 #17)
-#572 := [refl]: #571
-#574 := [quant-intro #572]: #573
-#62 := (~ #18 #18)
-#61 := (~ #17 #17)
-#72 := [refl]: #61
-#63 := [nnf-pos #72]: #62
-#48 := [asserted]: #18
-#73 := [mp~ #48 #63]: #18
-#575 := [mp #73 #574]: #570
-#551 := (not #570)
-#210 := (or #551 #21)
-#215 := [quant-inst #19]: #210
-[unit-resolution #215 #575 #555]: false
-unsat