--- a/src/HOL/SMT/Examples/SMT_Examples.certs Tue Feb 16 15:25:36 2010 +0100
+++ b/src/HOL/SMT/Examples/SMT_Examples.certs Tue Feb 16 15:26:24 2010 +0100
@@ -1,4 +1,4 @@
-yknPpoG47N1CXnUaEL9RvQ 133
+yknPpoG47N1CXnUaEL9RvQ 8 0
#2 := false
#1 := true
#4 := (not true)
@@ -7,8 +7,7 @@
#20 := [asserted]: #4
[mp #20 #22]: false
unsat
-
-ymB2ZiCSl9aUjMXP3tIpZA 359
+ymB2ZiCSl9aUjMXP3tIpZA 19 0
#2 := false
decl up_1 :: bool
#4 := up_1
@@ -28,8 +27,7 @@
#23 := [asserted]: #7
[mp #23 #32]: false
unsat
-
-XC3j0tGm4Y5klDm8sMkzVg 510
+XC3j0tGm4Y5klDm8sMkzVg 25 0
#2 := false
decl up_1 :: bool
#4 := up_1
@@ -55,8 +53,7 @@
#23 := [asserted]: #7
[mp #23 #38]: false
unsat
-
-y5d/Jtt47lXm/wUEvH5fHw 794
+y5d/Jtt47lXm/wUEvH5fHw 38 0
#2 := false
decl up_2 :: bool
#5 := up_2
@@ -95,11 +92,9 @@
#30 := [and-elim #31]: #6
[mp #30 #52]: false
unsat
-
-mDaukNkyA4glYbkfEOtcAw 7
-unsat
-
-TmB9YjKjdtDMIh0j9rMVPw 1530
+mDaukNkyA4glYbkfEOtcAw 1 0
+unsat
+TmB9YjKjdtDMIh0j9rMVPw 71 0
#2 := false
decl up_1 :: bool
#4 := up_1
@@ -171,8 +166,7 @@
#31 := [asserted]: #15
[mp #31 #82]: false
unsat
-
-olufSxMlwMAAqyArYWPVOA 1300
+olufSxMlwMAAqyArYWPVOA 57 0
#2 := false
decl up_1 :: bool
#4 := up_1
@@ -230,8 +224,7 @@
#30 := [asserted]: #14
[mp #30 #70]: false
unsat
-
-agKJ550QwZ1mvlK8gw+tjQ 4627
+agKJ550QwZ1mvlK8gw+tjQ 194 0
#2 := false
decl up_1 :: bool
#4 := up_1
@@ -426,8 +419,7 @@
#237 := [mp #83 #236]: #75
[mp #237 #247]: false
unsat
-
-+R/oj2I+uFZAw/Eu+3ULdw 1160
++R/oj2I+uFZAw/Eu+3ULdw 52 0
#2 := false
decl uf_1 :: (-> T1 T1 T1)
decl uf_2 :: T1
@@ -480,8 +472,7 @@
#113 := [quant-inst]: #199
[unit-resolution #113 #536 #49]: false
unsat
-
-c67Ar5f1aFkzAZ2wYy62Wg 56943
+c67Ar5f1aFkzAZ2wYy62Wg 1667 0
#2 := false
decl up_54 :: bool
#126 := up_54
@@ -2149,8 +2140,7 @@
#2371 := [unit-resolution #891 #2369]: #166
[unit-resolution #2159 #2371 #2370 #2358 #2357]: false
unsat
-
-NdJwa8pysYWhn57eCXiqFA 1731
+NdJwa8pysYWhn57eCXiqFA 78 0
#2 := false
decl up_1 :: (-> int bool)
decl ?x1!0 :: int
@@ -2229,8 +2219,7 @@
#82 := [and-elim #81]: #55
[unit-resolution #82 #95]: false
unsat
-
-dWWXDEA5bUZjEafLPXbSkA 3321
+dWWXDEA5bUZjEafLPXbSkA 135 0
#2 := false
decl up_1 :: (-> T1 T2 bool)
#5 := (:var 0 T2)
@@ -2366,9 +2355,7 @@
#176 := [quant-inst]: #538
[unit-resolution #176 #252 #535]: false
unsat
-
-iGZ7b2jaCnn82lPL6oIDZA 3465
-WARNING: failed to find a pattern for quantifier (quantifier id: k!11)
+iGZ7b2jaCnn82lPL6oIDZA 135 2
#2 := false
decl up_1 :: (-> T1 T2 bool)
#5 := (:var 0 T2)
@@ -2504,8 +2491,9 @@
#235 := [quant-inst]: #597
[unit-resolution #235 #311 #594]: false
unsat
+WARNING: failed to find a pattern for quantifier (quantifier id: k!11)
-eTjcfu6S5eyz+xNJ7SVluw 1246
+eTjcfu6S5eyz+xNJ7SVluw 56 0
#2 := false
decl up_1 :: (-> T1 bool)
decl uf_2 :: T1
@@ -2562,8 +2550,7 @@
#120 := [quant-inst]: #206
[unit-resolution #120 #542 #41]: false
unsat
-
-anG1bKU/YVTHEmc1Eh/ZXw 331
+anG1bKU/YVTHEmc1Eh/ZXw 17 0
#2 := false
#4 := 3::int
#5 := (= 3::int 3::int)
@@ -2581,8 +2568,7 @@
#22 := [asserted]: #6
[mp #22 #31]: false
unsat
-
-lHpRCTa744ODgmii2zARAw 334
+lHpRCTa744ODgmii2zARAw 17 0
#2 := false
#4 := 3::real
#5 := (= 3::real 3::real)
@@ -2600,8 +2586,7 @@
#22 := [asserted]: #6
[mp #22 #31]: false
unsat
-
-AinXomcY4W1L/t0ZtkDhBg 524
+AinXomcY4W1L/t0ZtkDhBg 26 0
#2 := false
#7 := 4::int
#5 := 1::int
@@ -2628,8 +2613,7 @@
#25 := [asserted]: #9
[mp #25 #40]: false
unsat
-
-WxMdOusjxqQwBPorpXBkFQ 815
+WxMdOusjxqQwBPorpXBkFQ 41 0
#2 := false
decl uf_1 :: int
#4 := uf_1
@@ -2671,8 +2655,7 @@
#28 := [asserted]: #12
[mp #28 #52]: false
unsat
-
-K7g37p4yZoVyQcabYS4I2w 754
+K7g37p4yZoVyQcabYS4I2w 35 0
#2 := false
#5 := 3::int
#6 := 8::int
@@ -2708,8 +2691,7 @@
#26 := [asserted]: #10
[mp #26 #51]: false
unsat
-
-eCmVy21SUmWImXZDJNOfzA 6496
+eCmVy21SUmWImXZDJNOfzA 250 0
#2 := false
#7 := 0::real
decl uf_2 :: real
@@ -2960,8 +2942,7 @@
#294 := [unit-resolution #190 #293]: #188
[th-lemma #280 #294]: false
unsat
-
-eBRZKSXriNPK3BNu3AWMmQ 3017
+eBRZKSXriNPK3BNu3AWMmQ 124 0
#2 := false
decl uf_1 :: (-> T1 T2)
decl uf_3 :: T1
@@ -3086,8 +3067,7 @@
#34 := [asserted]: #11
[unit-resolution #34 #536]: false
unsat
-
-CjDkjvq1e9i+SJ3L9ESARg 1146
+CjDkjvq1e9i+SJ3L9ESARg 54 0
#2 := false
#9 := 1::int
decl uf_1 :: int
@@ -3142,8 +3122,7 @@
#28 := [asserted]: #12
[mp #28 #67]: false
unsat
-
-nonk4MmmwlBqL8YtiJY/Qw 1339
+nonk4MmmwlBqL8YtiJY/Qw 63 0
#2 := false
#11 := 0::int
decl uf_2 :: int
@@ -3207,8 +3186,7 @@
#76 := [mp #52 #75]: #63
[mp #76 #84]: false
unsat
-
-dCX9jxibjKl6gmr8okzk0w 727
+dCX9jxibjKl6gmr8okzk0w 35 0
#2 := false
#6 := 5::int
#4 := 2::int
@@ -3244,8 +3222,7 @@
#25 := [asserted]: #9
[mp #25 #49]: false
unsat
-
-/kLzs8f/jQjEM38PdppYPA 912
+/kLzs8f/jQjEM38PdppYPA 45 0
#2 := false
#11 := 4::real
decl uf_2 :: real
@@ -3291,8 +3268,7 @@
#60 := [mp #36 #59]: #51
[th-lemma #60 #47 #38]: false
unsat
-
-iT8vKYi503k30rQLczD7yw 1245
+iT8vKYi503k30rQLczD7yw 59 0
#2 := false
#16 := (not false)
decl uf_2 :: int
@@ -3352,8 +3328,7 @@
#34 := [asserted]: #18
[mp #34 #71]: false
unsat
-
-6R4JcV7tL9QRH7WWPAKM5g 5413
+6R4JcV7tL9QRH7WWPAKM5g 212 0
#2 := false
decl uf_4 :: T1
#13 := uf_4
@@ -3566,8 +3541,7 @@
#519 := [unit-resolution #521 #518]: #547
[unit-resolution #519 #522]: false
unsat
-
-eOXl5Nf4A2Sq4Q+Wh5XNfA 2026
+eOXl5Nf4A2Sq4Q+Wh5XNfA 86 0
#2 := false
decl uf_1 :: int
#5 := uf_1
@@ -3654,8 +3628,7 @@
#99 := [unit-resolution #77 #98 #91 #82]: #54
[unit-resolution #99 #112]: false
unsat
-
-TwJgkTydtls9Q94iw4a3jw 17377
+TwJgkTydtls9Q94iw4a3jw 673 0
#2 := false
#169 := 0::int
decl uf_2 :: int
@@ -4329,8 +4302,7 @@
#410 := [mp #349 #409]: #405
[unit-resolution #410 #710 #709 #697 #706]: false
unsat
-
-ib5n9nvBAC5jXuKIpV/54g 82870
+ib5n9nvBAC5jXuKIpV/54g 2291 0
#2 := false
#6 := 0::int
decl z3name!0 :: int
@@ -6622,8 +6594,7 @@
#2323 := [unit-resolution #918 #2322]: #100
[unit-resolution #917 #2323 #2318]: false
unsat
-
-SqgPFdiZeq8SOFuTISQN5g 1109
+SqgPFdiZeq8SOFuTISQN5g 52 0
#2 := false
#8 := 1::real
decl uf_1 :: real
@@ -6676,26 +6647,15 @@
#29 := [asserted]: #13
[mp #29 #65]: false
unsat
-
-rOkYPs+Q++z/M3OPR/88JQ 1654
+rOkYPs+Q++z/M3OPR/88JQ 59 0
#2 := false
#55 := 0::int
#7 := 2::int
decl uf_1 :: int
#4 := uf_1
#8 := (mod uf_1 2::int)
-#67 := (>= #8 0::int)
-#1 := true
-#156 := (iff #67 true)
-#158 := (iff #156 #67)
-#159 := [rewrite]: #158
-#28 := [true-axiom]: true
-#153 := (or false #67)
-#154 := [th-lemma]: #153
-#155 := [unit-resolution #154 #28]: #67
-#157 := [iff-true #155]: #156
-#160 := [mp #157 #159]: #67
-#70 := (not #67)
+#58 := (>= #8 0::int)
+#61 := (not #58)
#5 := 1::int
#9 := (* 2::int #8)
#10 := (+ #9 1::int)
@@ -6703,35 +6663,24 @@
#6 := (+ uf_1 1::int)
#12 := (<= #6 #11)
#13 := (not #12)
-#77 := (iff #13 #70)
+#66 := (iff #13 #61)
#39 := (+ uf_1 #9)
#40 := (+ 1::int #39)
#30 := (+ 1::int uf_1)
#45 := (<= #30 #40)
#48 := (not #45)
-#75 := (iff #48 #70)
-#58 := (* 1::int #8)
-#59 := (>= #58 0::int)
-#62 := (not #59)
-#71 := (iff #62 #70)
-#68 := (iff #59 #67)
-#65 := (= #58 #8)
-#66 := [rewrite]: #65
-#69 := [monotonicity #66]: #68
-#72 := [monotonicity #69]: #71
-#73 := (iff #48 #62)
+#64 := (iff #48 #61)
#56 := (>= #9 0::int)
#51 := (not #56)
-#63 := (iff #51 #62)
-#60 := (iff #56 #59)
-#61 := [rewrite]: #60
-#64 := [monotonicity #61]: #63
+#62 := (iff #51 #61)
+#59 := (iff #56 #58)
+#60 := [rewrite]: #59
+#63 := [monotonicity #60]: #62
#52 := (iff #48 #51)
#53 := (iff #45 #56)
#54 := [rewrite]: #53
#57 := [monotonicity #54]: #52
-#74 := [trans #57 #64]: #73
-#76 := [trans #74 #72]: #75
+#65 := [trans #57 #63]: #64
#49 := (iff #13 #48)
#46 := (iff #12 #45)
#43 := (= #11 #40)
@@ -6748,38 +6697,39 @@
#32 := [rewrite]: #31
#47 := [monotonicity #32 #44]: #46
#50 := [monotonicity #47]: #49
-#78 := [trans #50 #76]: #77
+#67 := [trans #50 #65]: #66
#29 := [asserted]: #13
-#79 := [mp #29 #78]: #70
-[unit-resolution #79 #160]: false
-unsat
-
-oSBTeiF6GKDeHPsMxXHXtQ 1064
+#68 := [mp #29 #67]: #61
+#1 := true
+#28 := [true-axiom]: true
+#142 := (or false #58)
+#143 := [th-lemma]: #142
+#144 := [unit-resolution #143 #28]: #58
+[unit-resolution #144 #68]: false
+unsat
+oSBTeiF6GKDeHPsMxXHXtQ 54 0
#2 := false
#5 := 2::int
decl uf_1 :: int
#4 := uf_1
#6 := (mod uf_1 2::int)
-#122 := (>= #6 2::int)
-#123 := (not #122)
-#1 := true
-#27 := [true-axiom]: true
-#133 := (or false #123)
-#134 := [th-lemma]: #133
-#135 := [unit-resolution #134 #27]: #123
+#55 := (>= #6 2::int)
#9 := 3::int
-#29 := (* 2::int #6)
-#48 := (>= #29 3::int)
#10 := (+ uf_1 3::int)
#7 := (+ #6 #6)
#8 := (+ uf_1 #7)
#11 := (< #8 #10)
#12 := (not #11)
-#55 := (iff #12 #48)
+#60 := (iff #12 #55)
#35 := (+ 3::int uf_1)
+#29 := (* 2::int #6)
#32 := (+ uf_1 #29)
#38 := (< #32 #35)
#41 := (not #38)
+#58 := (iff #41 #55)
+#48 := (>= #29 3::int)
+#56 := (iff #48 #55)
+#57 := [rewrite]: #56
#53 := (iff #41 #48)
#46 := (not #48)
#45 := (not #46)
@@ -6790,6 +6740,7 @@
#44 := [rewrite]: #47
#50 := [monotonicity #44]: #49
#54 := [trans #50 #52]: #53
+#59 := [trans #54 #57]: #58
#42 := (iff #12 #41)
#39 := (iff #11 #38)
#36 := (= #10 #35)
@@ -6800,13 +6751,18 @@
#34 := [monotonicity #31]: #33
#40 := [monotonicity #34 #37]: #39
#43 := [monotonicity #40]: #42
-#56 := [trans #43 #54]: #55
+#61 := [trans #43 #59]: #60
#28 := [asserted]: #12
-#57 := [mp #28 #56]: #48
-[th-lemma #57 #135]: false
-unsat
-
-hqH9yBHvmZgES3pBkvsqVQ 2715
+#62 := [mp #28 #61]: #55
+#127 := (not #55)
+#1 := true
+#27 := [true-axiom]: true
+#137 := (or false #127)
+#138 := [th-lemma]: #137
+#139 := [unit-resolution #138 #27]: #127
+[unit-resolution #139 #62]: false
+unsat
+hqH9yBHvmZgES3pBkvsqVQ 118 0
#2 := false
#5 := 0::real
decl uf_1 :: real
@@ -6925,8 +6881,7 @@
#126 := [mp #101 #125]: #115
[unit-resolution #126 #132 #129]: false
unsat
-
-ar4IlNF9IylWgGSPOf9paw 5159
+ar4IlNF9IylWgGSPOf9paw 208 0
#2 := false
#9 := 0::int
#11 := 4::int
@@ -7135,8 +7090,7 @@
#418 := [unit-resolution #417 #36]: #298
[th-lemma #418 #415 #412 #411 #99 #400 #397 #396]: false
unsat
-
-o9WM91Nq0O5f08PEA0qA6w 515
+o9WM91Nq0O5f08PEA0qA6w 24 0
#2 := false
#4 := (exists (vars (?x1 int)) false)
#5 := (not #4)
@@ -7161,8 +7115,7 @@
#22 := [asserted]: #6
[mp #22 #38]: false
unsat
-
-SJxvvXYE4z1G4iLRBCPerg 516
+SJxvvXYE4z1G4iLRBCPerg 24 0
#2 := false
#4 := (exists (vars (?x1 real)) false)
#5 := (not #4)
@@ -7187,17 +7140,13 @@
#22 := [asserted]: #6
[mp #22 #38]: false
unsat
-
-Fr3hfDrqfMuGDpDYbXAHwg 7
-unsat
-
-bFuFCRUoQSRWyp0iCwo+PA 7
-unsat
-
-NJEgv3p5NO4/yEATNBBDNw 7
-unsat
-
-RC1LWjyqEEsh1xhocCgPmQ 1633
+Fr3hfDrqfMuGDpDYbXAHwg 1 0
+unsat
+bFuFCRUoQSRWyp0iCwo+PA 1 0
+unsat
+NJEgv3p5NO4/yEATNBBDNw 1 0
+unsat
+RC1LWjyqEEsh1xhocCgPmQ 73 0
#2 := false
#5 := 0::int
#8 := 1::int
@@ -7271,8 +7220,7 @@
#144 := [trans #142 #82]: #143
[mp #144 #146]: false
unsat
-
-6pnpFuE9SN6Jr5Upml9T0A 1896
+6pnpFuE9SN6Jr5Upml9T0A 82 0
#2 := false
#5 := (:var 0 int)
#7 := 0::int
@@ -7355,100 +7303,52 @@
#30 := [asserted]: #14
[mp #30 #96]: false
unsat
-
-sHpY0IFBgZUNhP56aRB+/w 2968
+sHpY0IFBgZUNhP56aRB+/w 78 0
#2 := false
-#9 := 1::int
-decl ?x1!1 :: int
-#91 := ?x1!1
-#68 := -2::int
-#129 := (* -2::int ?x1!1)
-decl ?x2!0 :: int
-#90 := ?x2!0
+#5 := (:var 0 int)
#7 := 2::int
-#128 := (* 2::int ?x2!0)
-#130 := (+ #128 #129)
-#131 := (<= #130 1::int)
-#136 := (not #131)
-#55 := 0::int
-#53 := -1::int
-#115 := (* -1::int ?x1!1)
-#116 := (+ ?x2!0 #115)
-#117 := (<= #116 0::int)
-#139 := (or #117 #136)
-#142 := (not #139)
-#92 := (* -2::int ?x2!0)
-#93 := (* 2::int ?x1!1)
-#94 := (+ #93 #92)
-#95 := (>= #94 -1::int)
-#96 := (not #95)
-#97 := (* -1::int ?x2!0)
-#98 := (+ ?x1!1 #97)
-#99 := (>= #98 0::int)
-#100 := (or #99 #96)
-#101 := (not #100)
-#143 := (iff #101 #142)
-#140 := (iff #100 #139)
-#137 := (iff #96 #136)
-#134 := (iff #95 #131)
-#122 := (+ #92 #93)
-#125 := (>= #122 -1::int)
-#132 := (iff #125 #131)
-#133 := [rewrite]: #132
-#126 := (iff #95 #125)
-#123 := (= #94 #122)
-#124 := [rewrite]: #123
-#127 := [monotonicity #124]: #126
-#135 := [trans #127 #133]: #134
-#138 := [monotonicity #135]: #137
-#120 := (iff #99 #117)
-#109 := (+ #97 ?x1!1)
-#112 := (>= #109 0::int)
-#118 := (iff #112 #117)
-#119 := [rewrite]: #118
-#113 := (iff #99 #112)
-#110 := (= #98 #109)
-#111 := [rewrite]: #110
-#114 := [monotonicity #111]: #113
-#121 := [trans #114 #119]: #120
-#141 := [monotonicity #121 #138]: #140
-#144 := [monotonicity #141]: #143
-#5 := (:var 0 int)
-#71 := (* -2::int #5)
+#11 := (* 2::int #5)
+#9 := 1::int
#4 := (:var 1 int)
#8 := (* 2::int #4)
-#72 := (+ #8 #71)
-#70 := (>= #72 -1::int)
-#69 := (not #70)
-#57 := (* -1::int #5)
-#58 := (+ #4 #57)
-#56 := (>= #58 0::int)
-#75 := (or #56 #69)
-#78 := (forall (vars (?x1 int) (?x2 int)) #75)
-#81 := (not #78)
-#102 := (~ #81 #101)
-#103 := [sk]: #102
-#11 := (* 2::int #5)
#10 := (+ #8 1::int)
#12 := (< #10 #11)
#6 := (< #4 #5)
#13 := (implies #6 #12)
#14 := (forall (vars (?x1 int) (?x2 int)) #13)
#15 := (not #14)
-#84 := (iff #15 #81)
+#91 := (iff #15 false)
#32 := (+ 1::int #8)
#35 := (< #32 #11)
#41 := (not #6)
#42 := (or #41 #35)
#47 := (forall (vars (?x1 int) (?x2 int)) #42)
#50 := (not #47)
-#82 := (iff #50 #81)
-#79 := (iff #47 #78)
-#76 := (iff #42 #75)
-#73 := (iff #35 #69)
+#89 := (iff #50 false)
+#1 := true
+#84 := (not true)
+#87 := (iff #84 false)
+#88 := [rewrite]: #87
+#85 := (iff #50 #84)
+#82 := (iff #47 true)
+#77 := (forall (vars (?x1 int) (?x2 int)) true)
+#80 := (iff #77 true)
+#81 := [elim-unused]: #80
+#78 := (iff #47 #77)
+#75 := (iff #42 true)
+#55 := 0::int
+#53 := -1::int
+#57 := (* -1::int #5)
+#58 := (+ #4 #57)
+#56 := (>= #58 0::int)
+#54 := (not #56)
+#69 := (or #56 #54)
+#73 := (iff #69 true)
#74 := [rewrite]: #73
+#71 := (iff #42 #69)
+#70 := (iff #35 #54)
+#68 := [rewrite]: #70
#66 := (iff #41 #56)
-#54 := (not #56)
#61 := (not #54)
#64 := (iff #61 #56)
#65 := [rewrite]: #64
@@ -7457,9 +7357,12 @@
#60 := [rewrite]: #59
#63 := [monotonicity #60]: #62
#67 := [trans #63 #65]: #66
-#77 := [monotonicity #67 #74]: #76
-#80 := [quant-intro #77]: #79
-#83 := [monotonicity #80]: #82
+#72 := [monotonicity #67 #68]: #71
+#76 := [trans #72 #74]: #75
+#79 := [quant-intro #76]: #78
+#83 := [trans #79 #81]: #82
+#86 := [monotonicity #83]: #85
+#90 := [trans #86 #88]: #89
#51 := (iff #15 #50)
#48 := (iff #14 #47)
#45 := (iff #13 #42)
@@ -7475,89 +7378,53 @@
#46 := [trans #40 #44]: #45
#49 := [quant-intro #46]: #48
#52 := [monotonicity #49]: #51
-#85 := [trans #52 #83]: #84
+#92 := [trans #52 #90]: #91
#31 := [asserted]: #15
-#86 := [mp #31 #85]: #81
-#106 := [mp~ #86 #103]: #101
-#107 := [mp #106 #144]: #142
-#146 := [not-or-elim #107]: #131
-#108 := (not #117)
-#145 := [not-or-elim #107]: #108
-[th-lemma #145 #146]: false
-unsat
-
-7GSX+dyn9XwHWNcjJ4X1ww 2292
+[mp #31 #92]: false
+unsat
+7GSX+dyn9XwHWNcjJ4X1ww 61 0
#2 := false
-#7 := 1::int
-decl ?x1!1 :: int
-#74 := ?x1!1
-#51 := -2::int
-#96 := (* -2::int ?x1!1)
-decl ?x2!0 :: int
-#73 := ?x2!0
+#9 := (:var 0 int)
#4 := 2::int
-#95 := (* 2::int ?x2!0)
-#97 := (+ #95 #96)
-#166 := (<= #97 1::int)
-#94 := (= #97 1::int)
-#53 := -1::int
-#75 := (* -2::int ?x2!0)
-#76 := (* 2::int ?x1!1)
-#77 := (+ #76 #75)
-#78 := (= #77 -1::int)
-#79 := (not #78)
-#80 := (not #79)
-#110 := (iff #80 #94)
-#102 := (not #94)
-#105 := (not #102)
-#108 := (iff #105 #94)
-#109 := [rewrite]: #108
-#106 := (iff #80 #105)
-#103 := (iff #79 #102)
-#100 := (iff #78 #94)
-#88 := (+ #75 #76)
-#91 := (= #88 -1::int)
-#98 := (iff #91 #94)
-#99 := [rewrite]: #98
-#92 := (iff #78 #91)
-#89 := (= #77 #88)
-#90 := [rewrite]: #89
-#93 := [monotonicity #90]: #92
-#101 := [trans #93 #99]: #100
-#104 := [monotonicity #101]: #103
-#107 := [monotonicity #104]: #106
-#111 := [trans #107 #109]: #110
-#9 := (:var 0 int)
-#55 := (* -2::int #9)
+#10 := (* 2::int #9)
+#7 := 1::int
#5 := (:var 1 int)
#6 := (* 2::int #5)
-#56 := (+ #6 #55)
-#54 := (= #56 -1::int)
-#58 := (not #54)
-#61 := (forall (vars (?x1 int) (?x2 int)) #58)
-#64 := (not #61)
-#81 := (~ #64 #80)
-#82 := [sk]: #81
-#10 := (* 2::int #9)
#8 := (+ #6 1::int)
#11 := (= #8 #10)
#12 := (not #11)
#13 := (forall (vars (?x1 int) (?x2 int)) #12)
#14 := (not #13)
-#67 := (iff #14 #64)
+#74 := (iff #14 false)
#31 := (+ 1::int #6)
#37 := (= #10 #31)
#42 := (not #37)
#45 := (forall (vars (?x1 int) (?x2 int)) #42)
#48 := (not #45)
-#65 := (iff #48 #64)
-#62 := (iff #45 #61)
-#59 := (iff #42 #58)
-#52 := (iff #37 #54)
-#57 := [rewrite]: #52
-#60 := [monotonicity #57]: #59
-#63 := [quant-intro #60]: #62
-#66 := [monotonicity #63]: #65
+#72 := (iff #48 false)
+#1 := true
+#67 := (not true)
+#70 := (iff #67 false)
+#71 := [rewrite]: #70
+#68 := (iff #48 #67)
+#65 := (iff #45 true)
+#60 := (forall (vars (?x1 int) (?x2 int)) true)
+#63 := (iff #60 true)
+#64 := [elim-unused]: #63
+#61 := (iff #45 #60)
+#58 := (iff #42 true)
+#51 := (not false)
+#56 := (iff #51 true)
+#57 := [rewrite]: #56
+#52 := (iff #42 #51)
+#53 := (iff #37 false)
+#54 := [rewrite]: #53
+#55 := [monotonicity #54]: #52
+#59 := [trans #55 #57]: #58
+#62 := [quant-intro #59]: #61
+#66 := [trans #62 #64]: #65
+#69 := [monotonicity #66]: #68
+#73 := [trans #69 #71]: #72
#49 := (iff #14 #48)
#46 := (iff #13 #45)
#43 := (iff #12 #42)
@@ -7573,22 +7440,11 @@
#44 := [monotonicity #41]: #43
#47 := [quant-intro #44]: #46
#50 := [monotonicity #47]: #49
-#68 := [trans #50 #66]: #67
+#75 := [trans #50 #73]: #74
#30 := [asserted]: #14
-#69 := [mp #30 #68]: #64
-#85 := [mp~ #69 #82]: #80
-#86 := [mp #85 #111]: #94
-#168 := (or #102 #166)
-#169 := [th-lemma]: #168
-#170 := [unit-resolution #169 #86]: #166
-#167 := (>= #97 1::int)
-#171 := (or #102 #167)
-#172 := [th-lemma]: #171
-#173 := [unit-resolution #172 #86]: #167
-[th-lemma #173 #170]: false
-unsat
-
-oieid3+1h5s04LTQ9d796Q 2636
+[mp #30 #75]: false
+unsat
+oieid3+1h5s04LTQ9d796Q 111 0
#2 := false
#4 := 2::int
decl ?x1!1 :: int
@@ -7700,8 +7556,7 @@
#184 := [th-lemma]: #183
[unit-resolution #184 #127 #125 #126]: false
unsat
-
-+RiWXCcHPvuSeYUjZ4Ky/g 2113
++RiWXCcHPvuSeYUjZ4Ky/g 89 0
#2 := false
#4 := 0::int
decl ?x1!0 :: int
@@ -7791,9 +7646,7 @@
#167 := [unit-resolution #154 #90]: #166
[unit-resolution #167 #165 #162]: false
unsat
-
-hlG1vHDJCcXbyvxKYDWifg 2036
-WARNING: failed to find a pattern for quantifier (quantifier id: k!1)
+hlG1vHDJCcXbyvxKYDWifg 83 2
#2 := false
#5 := 0::int
#4 := (:var 0 int)
@@ -7877,9 +7730,9 @@
#62 := [mp~ #54 #61]: #49
[unit-resolution #62 #174]: false
unsat
+WARNING: failed to find a pattern for quantifier (quantifier id: k!1)
-oOC8ghGUYboMezGio2exAg 4464
-WARNING: failed to find a pattern for quantifier (quantifier id: k!1)
+oOC8ghGUYboMezGio2exAg 180 2
#2 := false
#4 := 0::int
#5 := (:var 0 int)
@@ -8060,63 +7913,40 @@
#585 := [unit-resolution #128 #581]: #55
[unit-resolution #585 #307]: false
unsat
+WARNING: failed to find a pattern for quantifier (quantifier id: k!1)
-4Dtb5Y1TTRPWZcHG9Griog 2407
+4Dtb5Y1TTRPWZcHG9Griog 68 0
#2 := false
-#104 := -1::int
-decl ?x1!1 :: int
-#86 := ?x1!1
-#106 := -4::int
-#107 := (* -4::int ?x1!1)
-decl ?x2!0 :: int
-#85 := ?x2!0
-#7 := 6::int
-#105 := (* 6::int ?x2!0)
-#108 := (+ #105 #107)
-#168 := (<= #108 -1::int)
-#109 := (= #108 -1::int)
#12 := 1::int
-#33 := -6::int
-#87 := (* -6::int ?x2!0)
-#4 := 4::int
-#88 := (* 4::int ?x1!1)
-#89 := (+ #88 #87)
-#90 := (= #89 1::int)
-#112 := (iff #90 #109)
-#98 := (+ #87 #88)
-#101 := (= #98 1::int)
-#110 := (iff #101 #109)
-#111 := [rewrite]: #110
-#102 := (iff #90 #101)
-#99 := (= #89 #98)
-#100 := [rewrite]: #99
-#103 := [monotonicity #100]: #102
-#113 := [trans #103 #111]: #112
-#53 := (:var 0 int)
-#54 := (* -6::int #53)
#9 := (:var 1 int)
-#55 := (* 4::int #9)
-#56 := (+ #55 #54)
-#76 := (= #56 1::int)
-#74 := (exists (vars (?x1 int) (?x2 int)) #76)
-#91 := (~ #74 #90)
-#92 := [sk]: #91
+#7 := 6::int
#8 := (- 6::int)
#10 := (* #8 #9)
#5 := (:var 2 int)
+#4 := 4::int
#6 := (* 4::int #5)
#11 := (+ #6 #10)
#13 := (= #11 1::int)
#14 := (exists (vars (?x1 int) (?x2 int) (?x3 int)) #13)
#15 := (not #14)
#16 := (not #15)
-#79 := (iff #16 #74)
+#82 := (iff #16 false)
+#53 := (:var 0 int)
+#33 := -6::int
+#54 := (* -6::int #53)
+#55 := (* 4::int #9)
+#56 := (+ #55 #54)
#57 := (= 1::int #56)
#58 := (exists (vars (?x1 int) (?x2 int)) #57)
-#77 := (iff #58 #74)
-#75 := (iff #57 #76)
-#73 := [rewrite]: #75
-#78 := [quant-intro #73]: #77
+#80 := (iff #58 false)
+#76 := (exists (vars (?x1 int) (?x2 int)) false)
+#78 := (iff #76 false)
+#79 := [elim-unused]: #78
+#77 := (iff #58 #76)
+#73 := (iff #57 false)
+#74 := [rewrite]: #73
+#75 := [quant-intro #74]: #77
+#81 := [trans #75 #79]: #80
#71 := (iff #16 #58)
#63 := (not #58)
#66 := (not #63)
@@ -8150,23 +7980,11 @@
#65 := [monotonicity #62]: #64
#68 := [monotonicity #65]: #67
#72 := [trans #68 #70]: #71
-#80 := [trans #72 #78]: #79
+#83 := [trans #72 #81]: #82
#32 := [asserted]: #16
-#81 := [mp #32 #80]: #74
-#95 := [mp~ #81 #92]: #90
-#96 := [mp #95 #113]: #109
-#170 := (not #109)
-#171 := (or #170 #168)
-#172 := [th-lemma]: #171
-#173 := [unit-resolution #172 #96]: #168
-#169 := (>= #108 -1::int)
-#174 := (or #170 #169)
-#175 := [th-lemma]: #174
-#176 := [unit-resolution #175 #96]: #169
-[th-lemma #176 #173]: false
-unsat
-
-dbOre63OdVavsqL3lG2ttw 2516
+[mp #32 #83]: false
+unsat
+dbOre63OdVavsqL3lG2ttw 107 0
#2 := false
#4 := 0::int
decl ?x2!1 :: int
@@ -8274,8 +8092,7 @@
#123 := [and-elim #101]: #88
[th-lemma #123 #124 #125]: false
unsat
-
-LtM5szEGH9QAF1TwsVtH4w 2764
+LtM5szEGH9QAF1TwsVtH4w 117 0
#2 := false
#4 := 0::int
decl ?x2!1 :: int
@@ -8393,8 +8210,7 @@
#188 := [unit-resolution #187 #110]: #98
[unit-resolution #188 #130]: false
unsat
-
-ibIqbnIUB+oyERADdbFW6w 3631
+ibIqbnIUB+oyERADdbFW6w 148 0
#2 := false
#144 := (not false)
#7 := 0::int
@@ -8543,8 +8359,7 @@
#158 := [mp #126 #157]: #153
[mp #158 #181]: false
unsat
-
-1HbJvLWS/aG8IZEVLDIWyA 1506
+1HbJvLWS/aG8IZEVLDIWyA 67 0
#2 := false
#4 := (:var 0 int)
#5 := (pattern #4)
@@ -8581,12 +8396,12 @@
#46 := (+ #4 #45)
#44 := (>= #46 0::int)
#42 := (not #44)
-#60 := (or #44 #42)
-#61 := (iff #60 true)
+#57 := (or #44 #42)
+#61 := (iff #57 true)
#62 := [rewrite]: #61
-#56 := (iff #32 #60)
+#59 := (iff #32 #57)
#58 := (iff #11 #42)
-#59 := [rewrite]: #58
+#56 := [rewrite]: #58
#54 := (iff #31 #44)
#49 := (not #42)
#52 := (iff #49 #44)
@@ -8596,8 +8411,8 @@
#48 := [rewrite]: #47
#51 := [monotonicity #48]: #50
#55 := [trans #51 #53]: #54
-#57 := [monotonicity #55 #59]: #56
-#64 := [trans #57 #62]: #63
+#60 := [monotonicity #55 #56]: #59
+#64 := [trans #60 #62]: #63
#67 := [quant-intro #64]: #66
#71 := [trans #67 #69]: #70
#74 := [monotonicity #71]: #73
@@ -8612,11 +8427,9 @@
#30 := [asserted]: #14
[mp #30 #80]: false
unsat
-
-K7kWge9RT44bPFRy+hxaqg 7
-unsat
-
-+rwKUm5bOzD9paEkmogLyw 1562
+K7kWge9RT44bPFRy+hxaqg 1 0
+unsat
++rwKUm5bOzD9paEkmogLyw 75 0
#2 := false
#6 := 1::int
decl uf_3 :: int
@@ -8692,8 +8505,7 @@
#32 := [asserted]: #16
[mp #32 #86]: false
unsat
-
-iRJ30NP1Enylq9tZfpCPTA 1288
+iRJ30NP1Enylq9tZfpCPTA 62 0
#2 := false
decl uf_2 :: real
#6 := uf_2
@@ -8756,8 +8568,7 @@
#32 := [asserted]: #16
[mp #32 #74]: false
unsat
-
-Ff1vqDiuUnet19j/x+mXkA 3029
+Ff1vqDiuUnet19j/x+mXkA 141 0
#2 := false
decl uf_4 :: int
#9 := uf_4
@@ -8899,8 +8710,7 @@
#45 := [asserted]: #29
[mp #45 #150]: false
unsat
-
-iPZ87GNdi7uQw4ehEpbTPQ 7012
+iPZ87GNdi7uQw4ehEpbTPQ 252 0
#2 := false
#9 := 0::int
decl uf_2 :: (-> T1 int)
@@ -8915,19 +8725,19 @@
#295 := -1::int
#274 := (* -1::int #293)
#610 := (+ #24 #274)
-#315 := (<= #610 0::int)
+#594 := (<= #610 0::int)
#612 := (= #610 0::int)
-#255 := (>= #23 0::int)
-#317 := (= #293 0::int)
-#522 := (not #317)
-#577 := (<= #293 0::int)
-#519 := (not #577)
+#606 := (>= #23 0::int)
+#237 := (= #293 0::int)
+#549 := (not #237)
+#588 := (<= #293 0::int)
+#457 := (not #588)
#26 := 1::int
-#553 := (>= #293 1::int)
-#552 := (= #293 1::int)
+#558 := (>= #293 1::int)
+#555 := (= #293 1::int)
#27 := (uf_1 1::int)
-#420 := (uf_2 #27)
-#565 := (= #420 1::int)
+#589 := (uf_2 #27)
+#301 := (= #589 1::int)
#10 := (:var 0 int)
#12 := (uf_1 #10)
#626 := (pattern #12)
@@ -8983,57 +8793,57 @@
#87 := [mp #51 #86]: #82
#146 := [mp~ #87 #130]: #82
#632 := [mp #146 #631]: #627
-#237 := (not #627)
-#442 := (or #237 #565)
-#578 := (>= 1::int 0::int)
-#419 := (not #578)
-#421 := (= 1::int #420)
-#563 := (or #421 #419)
-#443 := (or #237 #563)
-#550 := (iff #443 #442)
-#547 := (iff #442 #442)
-#548 := [rewrite]: #547
-#559 := (iff #563 #565)
-#554 := (or #565 false)
-#558 := (iff #554 #565)
-#556 := [rewrite]: #558
-#555 := (iff #563 #554)
-#400 := (iff #419 false)
+#609 := (not #627)
+#578 := (or #609 #301)
+#311 := (>= 1::int 0::int)
+#585 := (not #311)
+#586 := (= 1::int #589)
+#590 := (or #586 #585)
+#419 := (or #609 #590)
+#421 := (iff #419 #578)
+#564 := (iff #578 #578)
+#565 := [rewrite]: #564
+#577 := (iff #590 #301)
+#574 := (or #301 false)
+#571 := (iff #574 #301)
+#576 := [rewrite]: #571
+#575 := (iff #590 #574)
+#584 := (iff #585 false)
#1 := true
-#567 := (not true)
-#569 := (iff #567 false)
-#398 := [rewrite]: #569
-#568 := (iff #419 #567)
-#560 := (iff #578 true)
-#561 := [rewrite]: #560
-#562 := [monotonicity #561]: #568
-#401 := [trans #562 #398]: #400
-#564 := (iff #421 #565)
-#566 := [rewrite]: #564
-#557 := [monotonicity #566 #401]: #555
-#441 := [trans #557 #556]: #559
-#452 := [monotonicity #441]: #550
-#551 := [trans #452 #548]: #550
-#402 := [quant-inst]: #443
-#436 := [mp #402 #551]: #442
-#524 := [unit-resolution #436 #632]: #565
-#526 := (= #293 #420)
+#582 := (not true)
+#583 := (iff #582 false)
+#580 := [rewrite]: #583
+#296 := (iff #585 #582)
+#303 := (iff #311 true)
+#581 := [rewrite]: #303
+#579 := [monotonicity #581]: #296
+#573 := [trans #579 #580]: #584
+#300 := (iff #586 #301)
+#302 := [rewrite]: #300
+#570 := [monotonicity #302 #573]: #575
+#572 := [trans #570 #576]: #577
+#563 := [monotonicity #572]: #421
+#566 := [trans #563 #565]: #421
+#420 := [quant-inst]: #419
+#560 := [mp #420 #566]: #578
+#442 := [unit-resolution #560 #632]: #301
+#443 := (= #293 #589)
#28 := (= #25 #27)
#129 := [asserted]: #28
-#527 := [monotonicity #129]: #526
-#528 := [trans #527 #524]: #552
-#529 := (not #552)
-#525 := (or #529 #553)
-#530 := [th-lemma]: #525
-#516 := [unit-resolution #530 #528]: #553
-#517 := (not #553)
-#520 := (or #517 #519)
-#521 := [th-lemma]: #520
-#518 := [unit-resolution #521 #516]: #519
-#502 := (or #522 #577)
-#503 := [th-lemma]: #502
-#505 := [unit-resolution #503 #518]: #522
-#300 := (or #255 #317)
+#436 := [monotonicity #129]: #443
+#451 := [trans #436 #442]: #555
+#453 := (not #555)
+#454 := (or #453 #558)
+#447 := [th-lemma]: #454
+#455 := [unit-resolution #447 #451]: #558
+#456 := (not #558)
+#458 := (or #456 #457)
+#459 := [th-lemma]: #458
+#552 := [unit-resolution #459 #455]: #457
+#553 := (or #549 #588)
+#540 := [th-lemma]: #553
+#542 := [unit-resolution #540 #552]: #549
+#603 := (or #237 #606)
#18 := (= #13 0::int)
#118 := (or #18 #70)
#633 := (forall (vars (?x3 int)) (:pat #626) #118)
@@ -9090,95 +8900,70 @@
#128 := [mp #88 #127]: #123
#149 := [mp~ #128 #134]: #123
#638 := [mp #149 #637]: #633
-#582 := (not #633)
-#296 := (or #582 #255 #317)
+#604 := (not #633)
+#602 := (or #604 #237 #606)
#204 := (>= #24 0::int)
-#210 := (or #317 #204)
-#579 := (or #582 #210)
-#570 := (iff #579 #296)
-#580 := (or #582 #300)
-#574 := (iff #580 #296)
-#575 := [rewrite]: #574
-#584 := (iff #579 #580)
-#303 := (iff #210 #300)
-#606 := (* 1::int #23)
-#279 := (>= #606 0::int)
-#311 := (or #279 #317)
-#301 := (iff #311 #300)
-#256 := (iff #279 #255)
-#251 := (= #606 #23)
-#593 := [rewrite]: #251
-#257 := [monotonicity #593]: #256
-#302 := [monotonicity #257]: #301
-#586 := (iff #210 #311)
-#587 := (or #317 #279)
-#585 := (iff #587 #311)
-#589 := [rewrite]: #585
-#588 := (iff #210 #587)
-#280 := (iff #204 #279)
-#613 := [rewrite]: #280
-#310 := [monotonicity #613]: #588
-#590 := [trans #310 #589]: #586
-#581 := [trans #590 #302]: #303
-#573 := [monotonicity #581]: #584
-#571 := [trans #573 #575]: #570
-#583 := [quant-inst]: #579
-#576 := [mp #583 #571]: #296
-#506 := [unit-resolution #576 #638]: #300
-#507 := [unit-resolution #506 #505]: #255
-#258 := (not #255)
-#597 := (or #258 #612)
-#601 := (or #237 #258 #612)
+#601 := (or #237 #204)
+#605 := (or #604 #601)
+#317 := (iff #605 #602)
+#592 := (or #604 #603)
+#315 := (iff #592 #602)
+#316 := [rewrite]: #315
+#299 := (iff #605 #592)
+#242 := (iff #601 #603)
+#279 := (iff #204 #606)
+#280 := [rewrite]: #279
+#243 := [monotonicity #280]: #242
+#314 := [monotonicity #243]: #299
+#210 := [trans #314 #316]: #317
+#591 := [quant-inst]: #605
+#587 := [mp #591 #210]: #602
+#534 := [unit-resolution #587 #638]: #603
+#531 := [unit-resolution #534 #542]: #606
+#613 := (not #606)
+#607 := (or #613 #612)
+#251 := (or #609 #613 #612)
#289 := (not #204)
#294 := (= #24 #293)
#291 := (or #294 #289)
-#603 := (or #237 #291)
-#592 := (iff #603 #601)
-#243 := (or #237 #597)
-#605 := (iff #243 #601)
-#591 := [rewrite]: #605
-#604 := (iff #603 #243)
-#594 := (iff #291 #597)
-#614 := (not #279)
-#266 := (or #614 #612)
-#598 := (iff #266 #597)
-#595 := (iff #614 #258)
-#596 := [monotonicity #257]: #595
-#599 := [monotonicity #596]: #598
-#267 := (iff #291 #266)
-#611 := (or #612 #614)
-#271 := (iff #611 #266)
-#608 := [rewrite]: #271
-#617 := (iff #291 #611)
-#615 := (iff #289 #614)
-#616 := [monotonicity #613]: #615
+#593 := (or #609 #291)
+#597 := (iff #593 #251)
+#256 := (or #609 #607)
+#595 := (iff #256 #251)
+#596 := [rewrite]: #595
+#257 := (iff #593 #256)
+#608 := (iff #291 #607)
+#616 := (or #612 #613)
+#266 := (iff #616 #607)
+#271 := [rewrite]: #266
+#611 := (iff #291 #616)
+#614 := (iff #289 #613)
+#615 := [monotonicity #280]: #614
#268 := (iff #294 #612)
#399 := [rewrite]: #268
-#607 := [monotonicity #399 #616]: #617
-#609 := [trans #607 #608]: #267
-#600 := [trans #609 #599]: #594
-#602 := [monotonicity #600]: #604
-#299 := [trans #602 #591]: #592
-#242 := [quant-inst]: #603
-#314 := [mp #242 #299]: #601
-#508 := [unit-resolution #314 #632]: #597
-#509 := [unit-resolution #508 #507]: #612
-#510 := (not #612)
-#511 := (or #510 #315)
-#512 := [th-lemma]: #511
-#513 := [unit-resolution #512 #509]: #315
-#316 := (>= #610 0::int)
-#514 := (or #510 #316)
-#504 := [th-lemma]: #514
-#515 := [unit-resolution #504 #509]: #316
-#549 := (<= #293 1::int)
-#493 := (or #529 #549)
-#494 := [th-lemma]: #493
-#496 := [unit-resolution #494 #528]: #549
-[th-lemma #516 #496 #515 #513]: false
-unsat
-
-kDuOn7kAggfP4Um8ghhv5A 6068
+#617 := [monotonicity #399 #615]: #611
+#267 := [trans #617 #271]: #608
+#258 := [monotonicity #267]: #257
+#598 := [trans #258 #596]: #597
+#255 := [quant-inst]: #593
+#599 := [mp #255 #598]: #251
+#533 := [unit-resolution #599 #632]: #607
+#543 := [unit-resolution #533 #531]: #612
+#544 := (not #612)
+#545 := (or #544 #594)
+#541 := [th-lemma]: #545
+#546 := [unit-resolution #541 #543]: #594
+#600 := (>= #610 0::int)
+#535 := (or #544 #600)
+#536 := [th-lemma]: #535
+#537 := [unit-resolution #536 #543]: #600
+#557 := (<= #293 1::int)
+#538 := (or #453 #557)
+#532 := [th-lemma]: #538
+#539 := [unit-resolution #532 #451]: #557
+[th-lemma #455 #539 #537 #546]: false
+unsat
+kDuOn7kAggfP4Um8ghhv5A 223 0
#2 := false
#23 := 3::int
decl uf_2 :: (-> T1 int)
@@ -9201,13 +8986,13 @@
#632 := -1::int
#634 := (* -1::int #28)
#290 := (+ #26 #634)
-#609 := (>= #290 0::int)
+#623 := (>= #290 0::int)
#421 := (= #290 0::int)
-#273 := (>= #22 0::int)
-#610 := (= #28 0::int)
-#588 := (not #610)
-#441 := (<= #28 0::int)
-#443 := (not #441)
+#302 := (>= #22 0::int)
+#625 := (= #28 0::int)
+#318 := (not #625)
+#322 := (<= #28 0::int)
+#324 := (not #322)
#29 := 7::int
#143 := (>= #28 7::int)
#30 := (< #28 7::int)
@@ -9224,12 +9009,12 @@
#151 := [trans #147 #149]: #150
#133 := [asserted]: #31
#152 := [mp #133 #151]: #143
-#585 := (or #443 #141)
-#586 := [th-lemma]: #585
-#587 := [unit-resolution #586 #152]: #443
-#582 := (or #588 #441)
-#583 := [th-lemma]: #582
-#589 := [unit-resolution #583 #587]: #588
+#325 := (or #324 #141)
+#603 := [th-lemma]: #325
+#604 := [unit-resolution #603 #152]: #324
+#601 := (or #318 #322)
+#605 := [th-lemma]: #601
+#602 := [unit-resolution #605 #604]: #318
#10 := (:var 0 int)
#12 := (uf_1 #10)
#648 := (pattern #12)
@@ -9292,45 +9077,33 @@
#131 := [mp #91 #130]: #126
#172 := [mp~ #131 #155]: #126
#660 := [mp #172 #659]: #655
-#605 := (not #655)
-#602 := (or #605 #273 #610)
+#337 := (not #655)
+#338 := (or #337 #302 #625)
#315 := (>= #26 0::int)
-#332 := (or #610 #315)
-#606 := (or #605 #332)
-#599 := (iff #606 #602)
-#323 := (or #273 #610)
-#596 := (or #605 #323)
-#593 := (iff #596 #602)
-#598 := [rewrite]: #593
-#597 := (iff #606 #596)
-#318 := (iff #332 #323)
-#302 := 1::int
-#635 := (* 1::int #22)
-#636 := (>= #635 0::int)
-#333 := (or #610 #636)
-#603 := (iff #333 #323)
-#608 := (or #610 #273)
-#324 := (iff #608 #323)
-#325 := [rewrite]: #324
-#612 := (iff #333 #608)
-#615 := (iff #636 #273)
-#289 := (= #635 #22)
-#631 := [rewrite]: #289
-#277 := [monotonicity #631]: #615
-#322 := [monotonicity #277]: #612
-#604 := [trans #322 #325]: #603
-#607 := (iff #332 #333)
-#637 := (iff #315 #636)
-#638 := [rewrite]: #637
-#611 := [monotonicity #638]: #607
-#601 := [trans #611 #604]: #318
-#592 := [monotonicity #601]: #597
-#594 := [trans #592 #598]: #599
-#595 := [quant-inst]: #606
-#600 := [mp #595 #594]: #602
-#590 := [unit-resolution #600 #660 #589]: #273
-#278 := (not #273)
-#620 := (or #278 #421)
+#264 := (or #625 #315)
+#339 := (or #337 #264)
+#611 := (iff #339 #338)
+#627 := (or #302 #625)
+#609 := (or #337 #627)
+#333 := (iff #609 #338)
+#607 := [rewrite]: #333
+#610 := (iff #339 #609)
+#321 := (iff #264 #627)
+#265 := (or #625 #302)
+#613 := (iff #265 #627)
+#614 := [rewrite]: #613
+#626 := (iff #264 #265)
+#635 := (iff #315 #302)
+#636 := [rewrite]: #635
+#624 := [monotonicity #636]: #626
+#336 := [trans #624 #614]: #321
+#332 := [monotonicity #336]: #610
+#608 := [trans #332 #607]: #611
+#231 := [quant-inst]: #339
+#612 := [mp #231 #608]: #338
+#606 := [unit-resolution #612 #660 #602]: #302
+#637 := (not #302)
+#293 := (or #637 #421)
#55 := (= #10 #13)
#80 := (or #55 #74)
#649 := (forall (vars (?x2 int)) (:pat #648) #80)
@@ -9380,50 +9153,41 @@
#90 := [mp #54 #89]: #85
#169 := [mp~ #90 #134]: #85
#654 := [mp #169 #653]: #649
-#264 := (not #649)
-#265 := (or #264 #278 #421)
+#615 := (not #649)
+#277 := (or #615 #637 #421)
#243 := (not #315)
#317 := (= #26 #28)
#296 := (or #317 #243)
-#626 := (or #264 #296)
-#337 := (iff #626 #265)
-#627 := (or #264 #620)
-#321 := (iff #627 #265)
-#336 := [rewrite]: #321
-#613 := (iff #626 #627)
-#623 := (iff #296 #620)
-#633 := (not #636)
-#288 := (or #421 #633)
-#622 := (iff #288 #620)
-#617 := (or #421 #278)
-#621 := (iff #617 #620)
-#616 := [rewrite]: #621
-#618 := (iff #288 #617)
-#279 := (iff #633 #278)
-#280 := [monotonicity #277]: #279
-#619 := [monotonicity #280]: #618
-#259 := [trans #619 #616]: #622
-#293 := (iff #296 #288)
-#639 := (iff #243 #633)
-#629 := [monotonicity #638]: #639
+#278 := (or #615 #296)
+#621 := (iff #278 #277)
+#280 := (or #615 #293)
+#619 := (iff #280 #277)
+#620 := [rewrite]: #619
+#617 := (iff #278 #280)
+#631 := (iff #296 #293)
+#639 := (or #421 #637)
+#630 := (iff #639 #293)
+#289 := [rewrite]: #630
+#629 := (iff #296 #639)
+#638 := (iff #243 #637)
+#633 := [monotonicity #636]: #638
#628 := (iff #317 #421)
#301 := [rewrite]: #628
-#630 := [monotonicity #301 #629]: #293
-#625 := [trans #630 #259]: #623
-#614 := [monotonicity #625]: #613
-#338 := [trans #614 #336]: #337
-#624 := [quant-inst]: #626
-#339 := [mp #624 #338]: #265
-#584 := [unit-resolution #339 #654]: #620
-#591 := [unit-resolution #584 #590]: #421
-#420 := (not #421)
-#422 := (or #420 #609)
-#423 := [th-lemma]: #422
-#576 := [unit-resolution #423 #591]: #609
-[th-lemma #152 #576 #139]: false
-unsat
-
-aiB004AWADNjynNrqCDsxw 9284
+#288 := [monotonicity #301 #633]: #629
+#273 := [trans #288 #289]: #631
+#618 := [monotonicity #273]: #617
+#616 := [trans #618 #620]: #621
+#279 := [quant-inst]: #278
+#622 := [mp #279 #616]: #277
+#595 := [unit-resolution #622 #654]: #293
+#596 := [unit-resolution #595 #606]: #421
+#597 := (not #421)
+#592 := (or #597 #623)
+#593 := [th-lemma]: #592
+#598 := [unit-resolution #593 #596]: #623
+[th-lemma #152 #598 #139]: false
+unsat
+aiB004AWADNjynNrqCDsxw 367 0
#2 := false
#9 := 0::int
decl uf_2 :: (-> T1 int)
@@ -9791,8 +9555,7 @@
#456 := [th-lemma]: #455
[unit-resolution #456 #464 #452]: false
unsat
-
-twoPNF2RBLeff4yYfubpfg 7634
+twoPNF2RBLeff4yYfubpfg 302 0
#2 := false
#9 := 0::int
decl uf_2 :: (-> T1 int)
@@ -10095,8 +9858,7 @@
#601 := [unit-resolution #615 #613]: #683
[th-lemma #623 #188 #601 #628]: false
unsat
-
-ZcLxnpFewGGQ0H47MfRXGw 12389
+ZcLxnpFewGGQ0H47MfRXGw 458 0
#2 := false
#9 := 0::int
decl uf_2 :: (-> T1 int)
@@ -10110,8 +9872,8 @@
#297 := (uf_2 #141)
#357 := (= #297 0::int)
#166 := (uf_1 0::int)
-#454 := (uf_2 #166)
-#515 := (= #454 0::int)
+#531 := (uf_2 #166)
+#537 := (= #531 0::int)
#10 := (:var 0 int)
#12 := (uf_1 #10)
#672 := (pattern #12)
@@ -10168,40 +9930,40 @@
#192 := [mp~ #95 #175]: #90
#678 := [mp #192 #677]: #673
#650 := (not #673)
-#468 := (or #650 #515)
-#528 := (>= 0::int 0::int)
-#508 := (not #528)
-#509 := (= 0::int #454)
-#490 := (or #509 #508)
-#469 := (or #650 #490)
-#471 := (iff #469 #468)
-#473 := (iff #468 #468)
-#474 := [rewrite]: #473
-#462 := (iff #490 #515)
-#495 := (or #515 false)
-#486 := (iff #495 #515)
-#507 := [rewrite]: #486
-#496 := (iff #490 #495)
-#492 := (iff #508 false)
+#528 := (or #650 #537)
+#529 := (>= 0::int 0::int)
+#530 := (not #529)
+#534 := (= 0::int #531)
+#535 := (or #534 #530)
+#508 := (or #650 #535)
+#509 := (iff #508 #528)
+#514 := (iff #528 #528)
+#515 := [rewrite]: #514
+#527 := (iff #535 #537)
+#520 := (or #537 false)
+#525 := (iff #520 #537)
+#526 := [rewrite]: #525
+#521 := (iff #535 #520)
+#519 := (iff #530 false)
#1 := true
-#491 := (not true)
-#483 := (iff #491 false)
-#485 := [rewrite]: #483
-#450 := (iff #508 #491)
-#516 := (iff #528 true)
-#484 := [rewrite]: #516
-#481 := [monotonicity #484]: #450
-#494 := [trans #481 #485]: #492
-#514 := (iff #509 #515)
-#510 := [rewrite]: #514
-#506 := [monotonicity #510 #494]: #496
-#463 := [trans #506 #507]: #462
-#472 := [monotonicity #463]: #471
-#475 := [trans #472 #474]: #471
-#470 := [quant-inst]: #469
-#476 := [mp #470 #475]: #468
-#351 := [unit-resolution #476 #678]: #515
-#287 := (= #297 #454)
+#512 := (not true)
+#517 := (iff #512 false)
+#518 := [rewrite]: #517
+#513 := (iff #530 #512)
+#538 := (iff #529 true)
+#511 := [rewrite]: #538
+#406 := [monotonicity #511]: #513
+#524 := [trans #406 #518]: #519
+#536 := (iff #534 #537)
+#532 := [rewrite]: #536
+#522 := [monotonicity #532 #524]: #521
+#523 := [trans #522 #526]: #527
+#490 := [monotonicity #523]: #509
+#510 := [trans #490 #515]: #509
+#454 := [quant-inst]: #508
+#516 := [mp #454 #510]: #528
+#394 := [unit-resolution #516 #678]: #537
+#355 := (= #297 #531)
#250 := (= #141 #166)
#26 := 2::int
#144 := (* 2::int #22)
@@ -10212,24 +9974,29 @@
#161 := (uf_1 #156)
#336 := (= #161 #166)
#327 := (not #336)
-#568 := (uf_2 #161)
-#537 := (= #568 0::int)
-#354 := (= #568 #454)
-#352 := [hypothesis]: #336
-#344 := [monotonicity #352]: #354
-#355 := [trans #344 #351]: #537
-#368 := (not #537)
-#527 := (<= #568 0::int)
-#375 := (not #527)
-#566 := (>= #150 0::int)
-#447 := (>= #22 0::int)
-#421 := (= #22 0::int)
+#588 := (uf_2 #161)
+#555 := (= #588 0::int)
+#398 := (= #588 #531)
+#395 := [hypothesis]: #336
+#387 := [monotonicity #395]: #398
+#399 := [trans #387 #394]: #555
+#390 := (not #555)
+#547 := (<= #588 0::int)
+#403 := (not #547)
+#595 := (>= #150 0::int)
+#302 := -1::int
+#618 := (* -1::int #150)
+#624 := (+ #144 #618)
+#488 := (<= #624 0::int)
+#465 := (= #624 0::int)
+#609 := (>= #22 0::int)
+#442 := (= #22 0::int)
#660 := (uf_1 #22)
-#451 := (uf_2 #660)
-#452 := (= #451 0::int)
-#603 := (not #447)
-#424 := [hypothesis]: #603
-#455 := (or #447 #452)
+#495 := (uf_2 #660)
+#496 := (= #495 0::int)
+#612 := (not #609)
+#451 := [hypothesis]: #612
+#506 := (or #496 #609)
#18 := (= #13 0::int)
#126 := (or #18 #78)
#679 := (forall (vars (?x3 int)) (:pat #672) #126)
@@ -10287,23 +10054,15 @@
#195 := [mp~ #136 #180]: #131
#684 := [mp #195 #683]: #679
#346 := (not #679)
-#458 := (or #346 #447 #452)
-#453 := (or #452 #447)
-#459 := (or #346 #453)
-#434 := (iff #459 #458)
-#443 := (or #346 #455)
-#432 := (iff #443 #458)
-#433 := [rewrite]: #432
-#461 := (iff #459 #443)
-#456 := (iff #453 #455)
-#457 := [rewrite]: #456
-#431 := [monotonicity #457]: #461
-#436 := [trans #431 #433]: #434
-#460 := [quant-inst]: #459
-#437 := [mp #460 #436]: #458
-#420 := [unit-resolution #437 #684]: #455
-#425 := [unit-resolution #420 #424]: #452
-#405 := (= #22 #451)
+#462 := (or #346 #496 #609)
+#463 := (or #346 #506)
+#469 := (iff #463 #462)
+#470 := [rewrite]: #469
+#468 := [quant-inst]: #463
+#471 := [mp #468 #470]: #462
+#452 := [unit-resolution #471 #684]: #506
+#453 := [unit-resolution #452 #451]: #496
+#456 := (= #22 #495)
#661 := (= uf_3 #660)
#4 := (:var 0 T1)
#5 := (uf_2 #4)
@@ -10334,136 +10093,117 @@
#663 := (not #665)
#653 := (or #663 #661)
#312 := [quant-inst]: #653
-#415 := [unit-resolution #312 #671]: #661
-#407 := [monotonicity #415]: #405
-#408 := [trans #407 #425]: #421
-#411 := (not #421)
-#412 := (or #411 #447)
-#416 := [th-lemma]: #412
-#409 := [unit-resolution #416 #424 #408]: false
-#417 := [lemma #409]: #447
-#302 := -1::int
-#618 := (* -1::int #150)
-#624 := (+ #144 #618)
-#595 := (<= #624 0::int)
-#465 := (= #624 0::int)
-#489 := (or #603 #465)
-#482 := (or #650 #603 #465)
+#455 := [unit-resolution #312 #671]: #661
+#457 := [monotonicity #455]: #456
+#458 := [trans #457 #453]: #442
+#459 := (not #442)
+#460 := (or #459 #609)
+#443 := [th-lemma]: #460
+#461 := [unit-resolution #443 #451 #458]: false
+#431 := [lemma #461]: #609
+#613 := (or #465 #612)
+#615 := (or #650 #465 #612)
#616 := (>= #144 0::int)
#617 := (not #616)
#622 := (= #144 #150)
#623 := (or #622 #617)
-#497 := (or #650 #623)
-#504 := (iff #497 #482)
-#500 := (or #650 #489)
-#502 := (iff #500 #482)
-#503 := [rewrite]: #502
-#493 := (iff #497 #500)
-#594 := (iff #623 #489)
-#609 := (* 1::int #22)
-#610 := (>= #609 0::int)
-#606 := (not #610)
-#614 := (or #465 #606)
-#498 := (iff #614 #489)
-#605 := (or #465 #603)
-#448 := (iff #605 #489)
-#596 := [rewrite]: #448
-#487 := (iff #614 #605)
-#604 := (iff #606 #603)
-#600 := (iff #610 #447)
-#444 := (= #609 #22)
-#446 := [rewrite]: #444
-#601 := [monotonicity #446]: #600
-#602 := [monotonicity #601]: #604
-#488 := [monotonicity #602]: #487
-#593 := [trans #488 #596]: #498
-#608 := (iff #623 #614)
-#607 := (iff #617 #606)
-#611 := (iff #616 #610)
-#612 := [rewrite]: #611
-#613 := [monotonicity #612]: #607
+#444 := (or #650 #623)
+#602 := (iff #444 #615)
+#447 := (or #650 #613)
+#603 := (iff #447 #615)
+#604 := [rewrite]: #603
+#600 := (iff #444 #447)
+#614 := (iff #623 #613)
+#606 := (iff #617 #612)
+#610 := (iff #616 #609)
+#611 := [rewrite]: #610
+#607 := [monotonicity #611]: #606
#466 := (iff #622 #465)
#467 := [rewrite]: #466
-#615 := [monotonicity #467 #613]: #608
-#597 := [trans #615 #593]: #594
-#501 := [monotonicity #597]: #493
-#505 := [trans #501 #503]: #504
-#499 := [quant-inst]: #497
-#598 := [mp #499 #505]: #482
-#404 := [unit-resolution #598 #678]: #489
-#386 := [unit-resolution #404 #417]: #465
-#388 := (not #465)
-#389 := (or #388 #595)
-#390 := [th-lemma]: #389
-#391 := [unit-resolution #390 #386]: #595
-#395 := (not #595)
-#413 := (or #566 #603 #395)
-#403 := [th-lemma]: #413
-#373 := [unit-resolution #403 #391 #417]: #566
-#553 := -3::int
-#551 := (* -1::int #568)
-#552 := (+ #150 #551)
-#535 := (<= #552 -3::int)
-#554 := (= #552 -3::int)
-#557 := (>= #150 -3::int)
+#608 := [monotonicity #467 #607]: #614
+#601 := [monotonicity #608]: #600
+#605 := [trans #601 #604]: #602
+#446 := [quant-inst]: #444
+#487 := [mp #446 #605]: #615
+#439 := [unit-resolution #487 #678]: #613
+#435 := [unit-resolution #439 #431]: #465
+#440 := (not #465)
+#419 := (or #440 #488)
+#422 := [th-lemma]: #419
+#426 := [unit-resolution #422 #435]: #488
+#430 := (not #488)
+#433 := (or #595 #612 #430)
+#438 := [th-lemma]: #433
+#402 := [unit-resolution #438 #431 #426]: #595
+#590 := -3::int
+#579 := (* -1::int #588)
+#589 := (+ #150 #579)
+#553 := (<= #589 -3::int)
+#591 := (= #589 -3::int)
+#581 := (>= #150 -3::int)
#644 := (>= #22 -1::int)
-#392 := (or #603 #644)
-#393 := [th-lemma]: #392
-#394 := [unit-resolution #393 #417]: #644
+#428 := (or #612 #644)
+#429 := [th-lemma]: #428
+#427 := [unit-resolution #429 #431]: #644
#646 := (not #644)
-#396 := (or #557 #646 #395)
-#397 := [th-lemma]: #396
-#398 := [unit-resolution #397 #391 #394]: #557
-#560 := (not #557)
-#539 := (or #554 #560)
-#543 := (or #650 #554 #560)
-#567 := (>= #156 0::int)
-#564 := (not #567)
-#548 := (= #156 #568)
-#549 := (or #548 #564)
-#544 := (or #650 #549)
-#530 := (iff #544 #543)
-#546 := (or #650 #539)
-#533 := (iff #546 #543)
-#529 := [rewrite]: #533
-#541 := (iff #544 #546)
-#540 := (iff #549 #539)
-#550 := (iff #564 #560)
-#558 := (iff #567 #557)
-#559 := [rewrite]: #558
-#561 := [monotonicity #559]: #550
-#555 := (iff #548 #554)
-#556 := [rewrite]: #555
-#542 := [monotonicity #556 #561]: #540
-#547 := [monotonicity #542]: #541
-#531 := [trans #547 #529]: #530
-#545 := [quant-inst]: #544
-#534 := [mp #545 #531]: #543
-#387 := [unit-resolution #534 #678]: #539
-#399 := [unit-resolution #387 #398]: #554
-#376 := (not #554)
-#378 := (or #376 #535)
-#379 := [th-lemma]: #378
-#380 := [unit-resolution #379 #399]: #535
-#365 := (not #535)
-#364 := (not #566)
-#366 := (or #375 #364 #365)
-#358 := [th-lemma]: #366
-#367 := [unit-resolution #358 #380 #373]: #375
-#359 := (or #368 #527)
-#369 := [th-lemma]: #359
-#350 := [unit-resolution #369 #367]: #368
-#321 := [unit-resolution #350 #355]: false
-#323 := [lemma #321]: #327
+#418 := (or #581 #646 #430)
+#421 := [th-lemma]: #418
+#423 := [unit-resolution #421 #426 #427]: #581
+#584 := (not #581)
+#573 := (or #584 #591)
+#562 := (or #650 #584 #591)
+#599 := (>= #156 0::int)
+#586 := (not #599)
+#580 := (= #156 #588)
+#577 := (or #580 #586)
+#563 := (or #650 #577)
+#549 := (iff #563 #562)
+#566 := (or #650 #573)
+#568 := (iff #566 #562)
+#548 := [rewrite]: #568
+#567 := (iff #563 #566)
+#571 := (iff #577 #573)
+#569 := (or #591 #584)
+#574 := (iff #569 #573)
+#575 := [rewrite]: #574
+#570 := (iff #577 #569)
+#578 := (iff #586 #584)
+#582 := (iff #599 #581)
+#583 := [rewrite]: #582
+#585 := [monotonicity #583]: #578
+#587 := (iff #580 #591)
+#592 := [rewrite]: #587
+#572 := [monotonicity #592 #585]: #570
+#576 := [trans #572 #575]: #571
+#564 := [monotonicity #576]: #567
+#551 := [trans #564 #548]: #549
+#565 := [quant-inst]: #563
+#552 := [mp #565 #551]: #562
+#424 := [unit-resolution #552 #678]: #573
+#420 := [unit-resolution #424 #423]: #591
+#425 := (not #591)
+#415 := (or #425 #553)
+#405 := [th-lemma]: #415
+#407 := [unit-resolution #405 #420]: #553
+#404 := (not #553)
+#401 := (not #595)
+#386 := (or #403 #401 #404)
+#388 := [th-lemma]: #386
+#389 := [unit-resolution #388 #407 #402]: #403
+#391 := (or #390 #547)
+#392 := [th-lemma]: #391
+#393 := [unit-resolution #392 #389]: #390
+#376 := [unit-resolution #393 #399]: false
+#378 := [lemma #376]: #327
#249 := (= #141 #161)
#334 := (not #249)
-#343 := (= #297 #568)
-#322 := [hypothesis]: #249
-#333 := [monotonicity #322]: #343
-#315 := (not #343)
-#414 := (+ #297 #551)
-#401 := (>= #414 0::int)
-#372 := (not #401)
+#396 := (= #297 #588)
+#385 := [hypothesis]: #249
+#370 := [monotonicity #385]: #396
+#380 := (not #396)
+#434 := (+ #297 #579)
+#280 := (>= #434 0::int)
+#414 := (not #280)
#303 := (* -1::int #297)
#304 := (+ #22 #303)
#356 := (>= #304 -1::int)
@@ -10492,21 +10232,21 @@
#256 := [trans #360 #362]: #363
#637 := [quant-inst]: #651
#633 := [mp #637 #256]: #648
-#381 := [unit-resolution #633 #678]: #649
-#382 := [unit-resolution #381 #394]: #641
-#383 := (not #641)
-#384 := (or #383 #356)
-#377 := [th-lemma]: #384
-#385 := [unit-resolution #377 #382]: #356
-#370 := [hypothesis]: #401
-#371 := [th-lemma #398 #370 #385 #380 #391]: false
-#374 := [lemma #371]: #372
-#328 := (or #315 #401)
-#329 := [th-lemma]: #328
-#332 := [unit-resolution #329 #374]: #315
-#316 := [unit-resolution #332 #333]: false
-#318 := [lemma #316]: #334
-#295 := (or #249 #250 #336)
+#408 := [unit-resolution #633 #678]: #649
+#411 := [unit-resolution #408 #427]: #641
+#412 := (not #641)
+#416 := (or #412 #356)
+#409 := [th-lemma]: #416
+#417 := [unit-resolution #409 #411]: #356
+#410 := [hypothesis]: #280
+#413 := [th-lemma #423 #410 #417 #407 #426]: false
+#400 := [lemma #413]: #414
+#381 := (or #380 #280)
+#382 := [th-lemma]: #381
+#377 := [unit-resolution #382 #400]: #380
+#371 := [unit-resolution #377 #370]: false
+#372 := [lemma #371]: #334
+#352 := (or #249 #250 #336)
#335 := (not #250)
#338 := (and #334 #335 #327)
#339 := (not #338)
@@ -10554,31 +10294,30 @@
#177 := [mp #137 #174]: #172
#326 := (or #169 #339)
#659 := [def-axiom]: #326
-#294 := [unit-resolution #659 #177]: #339
+#351 := [unit-resolution #659 #177]: #339
#314 := (or #338 #249 #250 #336)
#445 := [def-axiom]: #314
-#293 := [unit-resolution #445 #294]: #295
-#296 := [unit-resolution #293 #318 #323]: #250
-#290 := [monotonicity #296]: #287
-#285 := [trans #290 #351]: #357
-#310 := (not #357)
+#343 := [unit-resolution #445 #351]: #352
+#353 := [unit-resolution #343 #372 #378]: #250
+#321 := [monotonicity #353]: #355
+#323 := [trans #321 #394]: #357
+#368 := (not #357)
#620 := (<= #297 0::int)
-#305 := (not #620)
+#364 := (not #620)
#634 := (<= #304 -1::int)
-#319 := (or #383 #634)
-#298 := [th-lemma]: #319
-#300 := [unit-resolution #298 #382]: #634
-#306 := (not #634)
-#307 := (or #305 #603 #306)
-#308 := [th-lemma]: #307
-#309 := [unit-resolution #308 #300 #417]: #305
-#299 := (or #310 #620)
-#311 := [th-lemma]: #299
-#292 := [unit-resolution #311 #309]: #310
-[unit-resolution #292 #285]: false
-unsat
-
-ipe8HUL/t33OoeNl/z0smQ 4011
+#374 := (or #412 #634)
+#373 := [th-lemma]: #374
+#375 := [unit-resolution #373 #411]: #634
+#365 := (not #634)
+#366 := (or #364 #612 #365)
+#358 := [th-lemma]: #366
+#367 := [unit-resolution #358 #375 #431]: #364
+#359 := (or #368 #620)
+#369 := [th-lemma]: #359
+#350 := [unit-resolution #369 #367]: #368
+[unit-resolution #350 #323]: false
+unsat
+ipe8HUL/t33OoeNl/z0smQ 161 0
#2 := false
#9 := 0::int
decl uf_3 :: int
@@ -10740,8 +10479,7 @@
#361 := [unit-resolution #639 #655]: #647
[th-lemma #656 #361 #261]: false
unsat
-
-9FrZeHP8ZKJM+JmhfAjimQ 14889
+9FrZeHP8ZKJM+JmhfAjimQ 557 0
#2 := false
#9 := 0::int
decl uf_2 :: (-> T1 int)
@@ -10753,46 +10491,46 @@
#38 := (* 4::int #37)
#39 := (uf_1 #38)
#40 := (uf_2 #39)
-#504 := (= #40 0::int)
-#995 := (not #504)
-#475 := (<= #40 0::int)
-#990 := (not #475)
+#527 := (= #40 0::int)
+#976 := (not #527)
+#502 := (<= #40 0::int)
+#971 := (not #502)
#22 := 1::int
#186 := (+ 1::int #40)
#189 := (uf_1 #186)
-#467 := (uf_2 #189)
-#380 := (<= #467 1::int)
-#893 := (not #380)
+#506 := (uf_2 #189)
+#407 := (<= #506 1::int)
+#876 := (not #407)
decl up_4 :: (-> T1 T1 bool)
#4 := (:var 0 T1)
-#386 := (up_4 #4 #189)
-#374 := (pattern #386)
-#382 := (not #386)
-#385 := (= #4 #189)
+#408 := (up_4 #4 #189)
+#393 := (pattern #408)
+#413 := (= #4 #189)
+#414 := (not #408)
#26 := (uf_1 1::int)
#27 := (= #4 #26)
-#845 := (or #27 #385 #382)
-#848 := (forall (vars (?x5 T1)) (:pat #374) #845)
-#851 := (not #848)
-#854 := (or #380 #851)
-#857 := (not #854)
+#392 := (or #27 #414 #413)
+#397 := (forall (vars (?x5 T1)) (:pat #393) #392)
+#383 := (not #397)
+#382 := (or #383 #407)
+#375 := (not #382)
decl up_3 :: (-> T1 bool)
#192 := (up_3 #189)
-#840 := (not #192)
-#860 := (or #840 #857)
+#404 := (not #192)
+#841 := (or #404 #375)
decl ?x5!0 :: (-> T1 T1)
-#392 := (?x5!0 #189)
-#397 := (up_4 #392 #189)
-#390 := (not #397)
-#396 := (= #26 #392)
-#395 := (= #189 #392)
-#866 := (or #395 #396 #390)
-#869 := (not #866)
-#872 := (or #192 #380 #869)
-#875 := (not #872)
-#863 := (not #860)
-#878 := (or #863 #875)
-#881 := (not #878)
+#422 := (?x5!0 #189)
+#434 := (= #189 #422)
+#417 := (up_4 #422 #189)
+#418 := (not #417)
+#415 := (= #26 #422)
+#847 := (or #415 #418 #434)
+#850 := (not #847)
+#853 := (or #192 #407 #850)
+#856 := (not #853)
+#844 := (not #841)
+#859 := (or #844 #856)
+#862 := (not #859)
#5 := (uf_2 #4)
#787 := (pattern #5)
#21 := (up_3 #4)
@@ -10971,59 +10709,64 @@
#314 := [mp #267 #313]: #311
#839 := [mp #314 #838]: #836
#589 := (not #836)
-#884 := (or #589 #881)
-#398 := (or #390 #396 #395)
-#383 := (not #398)
-#381 := (or #192 #380 #383)
-#384 := (not #381)
-#387 := (or #382 #27 #385)
-#376 := (forall (vars (?x5 T1)) (:pat #374) #387)
-#377 := (not #376)
-#375 := (or #380 #377)
-#378 := (not #375)
-#841 := (or #840 #378)
-#842 := (not #841)
-#843 := (or #842 #384)
-#844 := (not #843)
-#885 := (or #589 #844)
-#887 := (iff #885 #884)
-#889 := (iff #884 #884)
-#890 := [rewrite]: #889
-#882 := (iff #844 #881)
-#879 := (iff #843 #878)
-#876 := (iff #384 #875)
-#873 := (iff #381 #872)
-#870 := (iff #383 #869)
-#867 := (iff #398 #866)
-#868 := [rewrite]: #867
-#871 := [monotonicity #868]: #870
-#874 := [monotonicity #871]: #873
-#877 := [monotonicity #874]: #876
-#864 := (iff #842 #863)
-#861 := (iff #841 #860)
-#858 := (iff #378 #857)
-#855 := (iff #375 #854)
-#852 := (iff #377 #851)
-#849 := (iff #376 #848)
-#846 := (iff #387 #845)
-#847 := [rewrite]: #846
-#850 := [quant-intro #847]: #849
-#853 := [monotonicity #850]: #852
-#856 := [monotonicity #853]: #855
-#859 := [monotonicity #856]: #858
-#862 := [monotonicity #859]: #861
-#865 := [monotonicity #862]: #864
-#880 := [monotonicity #865 #877]: #879
-#883 := [monotonicity #880]: #882
-#888 := [monotonicity #883]: #887
-#891 := [trans #888 #890]: #887
-#886 := [quant-inst]: #885
-#892 := [mp #886 #891]: #884
-#966 := [unit-resolution #892 #839]: #881
-#924 := (or #878 #860)
-#925 := [def-axiom]: #924
-#967 := [unit-resolution #925 #966]: #860
-#970 := (or #863 #857)
+#865 := (or #589 #862)
+#416 := (or #418 #415 #434)
+#419 := (not #416)
+#409 := (or #192 #407 #419)
+#410 := (not #409)
+#389 := (or #414 #27 #413)
+#394 := (forall (vars (?x5 T1)) (:pat #393) #389)
+#399 := (not #394)
+#401 := (or #407 #399)
+#402 := (not #401)
+#400 := (or #404 #402)
+#405 := (not #400)
+#388 := (or #405 #410)
+#391 := (not #388)
+#866 := (or #589 #391)
+#868 := (iff #866 #865)
+#870 := (iff #865 #865)
+#871 := [rewrite]: #870
+#863 := (iff #391 #862)
+#860 := (iff #388 #859)
+#857 := (iff #410 #856)
+#854 := (iff #409 #853)
+#851 := (iff #419 #850)
+#848 := (iff #416 #847)
+#849 := [rewrite]: #848
+#852 := [monotonicity #849]: #851
+#855 := [monotonicity #852]: #854
+#858 := [monotonicity #855]: #857
+#845 := (iff #405 #844)
+#842 := (iff #400 #841)
+#378 := (iff #402 #375)
+#376 := (iff #401 #382)
+#384 := (or #407 #383)
+#387 := (iff #384 #382)
+#374 := [rewrite]: #387
+#385 := (iff #401 #384)
+#380 := (iff #399 #383)
+#390 := (iff #394 #397)
+#395 := (iff #389 #392)
+#396 := [rewrite]: #395
+#398 := [quant-intro #396]: #390
+#381 := [monotonicity #398]: #380
+#386 := [monotonicity #381]: #385
+#377 := [trans #386 #374]: #376
+#840 := [monotonicity #377]: #378
+#843 := [monotonicity #840]: #842
+#846 := [monotonicity #843]: #845
+#861 := [monotonicity #846 #858]: #860
+#864 := [monotonicity #861]: #863
+#869 := [monotonicity #864]: #868
+#872 := [trans #869 #871]: #868
+#867 := [quant-inst]: #866
+#873 := [mp #867 #872]: #865
+#947 := [unit-resolution #873 #839]: #862
+#905 := (or #859 #841)
+#906 := [def-axiom]: #905
+#948 := [unit-resolution #906 #947]: #841
+#951 := (or #844 #375)
#41 := (+ #40 1::int)
#42 := (uf_1 #41)
#43 := (up_3 #42)
@@ -11035,30 +10778,30 @@
#194 := [monotonicity #191]: #193
#185 := [asserted]: #43
#197 := [mp #185 #194]: #192
-#904 := (or #863 #840 #857)
-#905 := [def-axiom]: #904
-#971 := [unit-resolution #905 #197]: #970
-#972 := [unit-resolution #971 #967]: #857
-#894 := (or #854 #893)
-#895 := [def-axiom]: #894
-#973 := [unit-resolution #895 #972]: #893
+#885 := (or #844 #404 #375)
+#886 := [def-axiom]: #885
+#952 := [unit-resolution #886 #197]: #951
+#953 := [unit-resolution #952 #948]: #375
+#877 := (or #382 #876)
+#878 := [def-axiom]: #877
+#954 := [unit-resolution #878 #953]: #876
#542 := -1::int
-#446 := (* -1::int #467)
-#447 := (+ #40 #446)
-#416 := (>= #447 -1::int)
-#438 := (= #447 -1::int)
-#453 := (>= #40 -1::int)
-#419 := (= #467 0::int)
-#978 := (not #419)
-#388 := (<= #467 0::int)
-#974 := (not #388)
-#975 := (or #974 #380)
-#976 := [th-lemma]: #975
-#977 := [unit-resolution #976 #973]: #974
-#979 := (or #978 #388)
-#980 := [th-lemma]: #979
-#981 := [unit-resolution #980 #977]: #978
-#409 := (or #419 #453)
+#508 := (* -1::int #506)
+#493 := (+ #40 #508)
+#438 := (>= #493 -1::int)
+#494 := (= #493 -1::int)
+#496 := (>= #40 -1::int)
+#451 := (= #506 0::int)
+#959 := (not #451)
+#432 := (<= #506 0::int)
+#955 := (not #432)
+#956 := (or #955 #407)
+#957 := [th-lemma]: #956
+#958 := [unit-resolution #957 #954]: #955
+#960 := (or #959 #432)
+#961 := [th-lemma]: #960
+#962 := [unit-resolution #961 #958]: #959
+#453 := (or #451 #496)
#10 := (:var 0 int)
#12 := (uf_1 #10)
#795 := (pattern #12)
@@ -11121,28 +10864,28 @@
#145 := [mp #105 #144]: #140
#227 := [mp~ #145 #208]: #140
#807 := [mp #227 #806]: #802
-#496 := (not #802)
-#408 := (or #496 #419 #453)
-#476 := (>= #186 0::int)
-#407 := (or #419 #476)
-#414 := (or #496 #407)
-#404 := (iff #414 #408)
-#393 := (or #496 #409)
-#401 := (iff #393 #408)
-#402 := [rewrite]: #401
-#394 := (iff #414 #393)
-#410 := (iff #407 #409)
-#454 := (iff #476 #453)
-#455 := [rewrite]: #454
-#413 := [monotonicity #455]: #410
-#399 := [monotonicity #413]: #394
-#400 := [trans #399 #402]: #404
-#389 := [quant-inst]: #414
-#405 := [mp #389 #400]: #408
-#982 := [unit-resolution #405 #807]: #409
-#983 := [unit-resolution #982 #981]: #453
-#445 := (not #453)
-#441 := (or #438 #445)
+#514 := (not #802)
+#445 := (or #514 #451 #496)
+#504 := (>= #186 0::int)
+#452 := (or #451 #504)
+#456 := (or #514 #452)
+#429 := (iff #456 #445)
+#441 := (or #514 #453)
+#423 := (iff #441 #445)
+#428 := [rewrite]: #423
+#442 := (iff #456 #441)
+#454 := (iff #452 #453)
+#498 := (iff #504 #496)
+#487 := [rewrite]: #498
+#455 := [monotonicity #487]: #454
+#421 := [monotonicity #455]: #442
+#430 := [trans #421 #428]: #429
+#439 := [quant-inst]: #456
+#431 := [mp #439 #430]: #445
+#963 := [unit-resolution #431 #807]: #453
+#964 := [unit-resolution #963 #962]: #496
+#488 := (not #496)
+#490 := (or #494 #488)
#69 := (= #10 #13)
#94 := (or #69 #88)
#796 := (forall (vars (?x2 int)) (:pat #795) #94)
@@ -11192,48 +10935,48 @@
#104 := [mp #68 #103]: #99
#224 := [mp~ #104 #196]: #99
#801 := [mp #224 #800]: #796
-#514 := (not #796)
-#423 := (or #514 #438 #445)
-#477 := (not #476)
-#478 := (= #186 #467)
-#444 := (or #478 #477)
-#428 := (or #514 #444)
-#434 := (iff #428 #423)
-#430 := (or #514 #441)
-#433 := (iff #430 #423)
-#422 := [rewrite]: #433
-#431 := (iff #428 #430)
-#442 := (iff #444 #441)
-#456 := (iff #477 #445)
-#439 := [monotonicity #455]: #456
-#451 := (iff #478 #438)
-#452 := [rewrite]: #451
-#421 := [monotonicity #452 #439]: #442
-#432 := [monotonicity #421]: #431
-#415 := [trans #432 #422]: #434
-#429 := [quant-inst]: #428
-#417 := [mp #429 #415]: #423
-#984 := [unit-resolution #417 #801]: #441
-#985 := [unit-resolution #984 #983]: #438
-#986 := (not #438)
-#987 := (or #986 #416)
-#988 := [th-lemma]: #987
-#989 := [unit-resolution #988 #985]: #416
-#991 := (not #416)
-#992 := (or #990 #380 #991)
-#993 := [th-lemma]: #992
-#994 := [unit-resolution #993 #989 #973]: #990
-#996 := (or #995 #475)
-#997 := [th-lemma]: #996
-#998 := [unit-resolution #997 #994]: #995
-#536 := (>= #37 0::int)
-#525 := (not #536)
+#530 := (not #796)
+#492 := (or #530 #494 #488)
+#505 := (not #504)
+#507 := (= #186 #506)
+#500 := (or #507 #505)
+#473 := (or #530 #500)
+#478 := (iff #473 #492)
+#475 := (or #530 #490)
+#477 := (iff #475 #492)
+#467 := [rewrite]: #477
+#466 := (iff #473 #475)
+#491 := (iff #500 #490)
+#489 := (iff #505 #488)
+#481 := [monotonicity #487]: #489
+#495 := (iff #507 #494)
+#497 := [rewrite]: #495
+#482 := [monotonicity #497 #481]: #491
+#476 := [monotonicity #482]: #466
+#444 := [trans #476 #467]: #478
+#474 := [quant-inst]: #473
+#446 := [mp #474 #444]: #492
+#965 := [unit-resolution #446 #801]: #490
+#966 := [unit-resolution #965 #964]: #494
+#967 := (not #494)
+#968 := (or #967 #438)
+#969 := [th-lemma]: #968
+#970 := [unit-resolution #969 #966]: #438
+#972 := (not #438)
+#973 := (or #971 #407 #972)
+#974 := [th-lemma]: #973
+#975 := [unit-resolution #974 #970 #954]: #971
+#977 := (or #976 #502)
+#978 := [th-lemma]: #977
+#979 := [unit-resolution #978 #975]: #976
+#553 := (>= #37 0::int)
+#546 := (not #553)
#545 := (* -1::int #40)
#549 := (+ #38 #545)
#551 := (= #549 0::int)
-#1003 := (not #551)
-#503 := (>= #549 0::int)
-#999 := (not #503)
+#984 := (not #551)
+#524 := (>= #549 0::int)
+#980 := (not #524)
#201 := (>= #37 1::int)
#202 := (not #201)
#44 := (<= 1::int #37)
@@ -11244,157 +10987,107 @@
#204 := [monotonicity #200]: #203
#195 := [asserted]: #45
#205 := [mp #195 #204]: #202
-#1000 := (or #999 #201 #380 #991)
-#1001 := [th-lemma]: #1000
-#1002 := [unit-resolution #1001 #205 #989 #973]: #999
-#1004 := (or #1003 #503)
-#1005 := [th-lemma]: #1004
-#1006 := [unit-resolution #1005 #1002]: #1003
-#527 := (or #525 #551)
-#515 := (or #514 #525 #551)
+#981 := (or #980 #201 #407 #972)
+#982 := [th-lemma]: #981
+#983 := [unit-resolution #982 #205 #970 #954]: #980
+#985 := (or #984 #524)
+#986 := [th-lemma]: #985
+#987 := [unit-resolution #986 #983]: #984
+#548 := (or #551 #546)
+#531 := (or #530 #551 #546)
#403 := (>= #38 0::int)
#562 := (not #403)
#558 := (= #38 #40)
#563 := (or #558 #562)
-#516 := (or #514 #563)
+#534 := (or #530 #563)
+#537 := (iff #534 #531)
+#539 := (or #530 #548)
+#533 := (iff #539 #531)
+#536 := [rewrite]: #533
+#532 := (iff #534 #539)
+#538 := (iff #563 #548)
+#547 := (iff #562 #546)
+#541 := (iff #403 #553)
+#544 := [rewrite]: #541
+#543 := [monotonicity #544]: #547
+#552 := (iff #558 #551)
+#550 := [rewrite]: #552
+#528 := [monotonicity #550 #543]: #538
+#540 := [monotonicity #528]: #532
+#523 := [trans #540 #536]: #537
+#535 := [quant-inst]: #534
+#525 := [mp #535 #523]: #531
+#988 := [unit-resolution #525 #801]: #548
+#989 := [unit-resolution #988 #987]: #546
+#511 := (or #527 #553)
+#515 := (or #514 #527 #553)
+#509 := (or #527 #403)
+#516 := (or #514 #509)
#522 := (iff #516 #515)
-#518 := (or #514 #527)
+#518 := (or #514 #511)
#521 := (iff #518 #515)
#510 := [rewrite]: #521
#519 := (iff #516 #518)
-#512 := (iff #563 #527)
-#553 := (* 1::int #37)
-#541 := (>= #553 0::int)
-#547 := (not #541)
-#531 := (or #547 #551)
-#509 := (iff #531 #527)
-#526 := (iff #547 #525)
-#537 := (iff #541 #536)
-#540 := (= #553 #37)
-#533 := [rewrite]: #540
-#523 := [monotonicity #533]: #537
-#524 := [monotonicity #523]: #526
-#511 := [monotonicity #524]: #509
-#539 := (iff #563 #531)
-#538 := (or #551 #547)
-#534 := (iff #538 #531)
-#535 := [rewrite]: #534
-#528 := (iff #563 #538)
-#543 := (iff #562 #547)
-#544 := (iff #403 #541)
-#546 := [rewrite]: #544
-#548 := [monotonicity #546]: #543
-#552 := (iff #558 #551)
-#550 := [rewrite]: #552
-#530 := [monotonicity #550 #548]: #528
-#532 := [trans #530 #535]: #539
-#513 := [trans #532 #511]: #512
+#512 := (iff #509 #511)
+#513 := [monotonicity #544]: #512
#520 := [monotonicity #513]: #519
#499 := [trans #520 #510]: #522
#517 := [quant-inst]: #516
#501 := [mp #517 #499]: #515
-#1007 := [unit-resolution #501 #801]: #527
-#1008 := [unit-resolution #1007 #1006]: #525
-#508 := (or #504 #536)
-#498 := (or #496 #504 #536)
-#505 := (or #504 #403)
-#487 := (or #496 #505)
-#492 := (iff #487 #498)
-#489 := (or #496 #508)
-#491 := (iff #489 #498)
-#482 := [rewrite]: #491
-#481 := (iff #487 #489)
-#495 := (iff #505 #508)
-#506 := (or #504 #541)
-#493 := (iff #506 #508)
-#494 := [monotonicity #523]: #493
-#507 := (iff #505 #506)
-#500 := [monotonicity #546]: #507
-#497 := [trans #500 #494]: #495
-#490 := [monotonicity #497]: #481
-#473 := [trans #490 #482]: #492
-#488 := [quant-inst]: #487
-#474 := [mp #488 #473]: #498
-#1009 := [unit-resolution #474 #807]: #508
-[unit-resolution #1009 #1008 #998]: false
-unsat
-
-uq2MbDTgTG1nxWdwzZtWew 7
-unsat
-
-E5BydeDaPocMMvChMGY+og 7
-unsat
-
-p81EQzqwJrGunGO7GuNt3g 7
-unsat
-
-KpYfvnTcz2WncWNg3dJDCA 7
-unsat
-
-ybGRm230DLO0wH6aROKBBw 7
-unsat
-
-goFtZfJ6kkxA8sqBVpZutw 7
-unsat
-
-0+nmgsMqioeTuwam1ScP7g 7
-unsat
-
-nI63LP/VCL//bjsS1gNB2A 7
-unsat
-
-9+2QHvrRgbKz97Zg0kfybw 7
-unsat
-
-6kquszLXeBUhTwzaw6gd2Q 7
-unsat
-
-j5Z04lpza+N5I1cpno5mtw 7
-unsat
-
-mapbfUM6Ils30x5nEBJmaw 7
-unsat
-
-e8P++0FczY3zhNhEVclACw 7
-unsat
-
-yXMQNOyCylhI+EH8hNYxHA 7
-unsat
-
-GkYN9j7cjrR2KR/lb04/qw 7
-unsat
-
-PajzgNjLWHwVHpjoje+gnA 7
-unsat
-
-URpJYU7D8PO0VRnciRgE5A 7
-unsat
-
-D9ZGhymoV3L6zbWsJlwG2A 7
-unsat
-
-0QLuovrnnANWnCkUY3l10g 7
-unsat
-
-CYprps2G0Au5F3Z7n3KTRg 7
-unsat
-
-iyIMuJd6zijfEao8zKnx2w 7
-unsat
-
-49jzsAwAEfR6NSFBhBEisQ 7
-unsat
-
-T0j6xFgrghxif91jL+2yAw 7
-unsat
-
-md/M3rVve0+8sQ6oqIoL2w 7
-unsat
-
-pY7C8PCf5lVVaim6q7PJcQ 7
-unsat
-
-4zCFLQf4Jrov/gmEvsBm4Q 1036
+#990 := [unit-resolution #501 #807]: #511
+[unit-resolution #990 #989 #979]: false
+unsat
+uq2MbDTgTG1nxWdwzZtWew 1 0
+unsat
+E5BydeDaPocMMvChMGY+og 1 0
+unsat
+p81EQzqwJrGunGO7GuNt3g 1 0
+unsat
+KpYfvnTcz2WncWNg3dJDCA 1 0
+unsat
+ybGRm230DLO0wH6aROKBBw 1 0
+unsat
+goFtZfJ6kkxA8sqBVpZutw 1 0
+unsat
+0+nmgsMqioeTuwam1ScP7g 1 0
+unsat
+nI63LP/VCL//bjsS1gNB2A 1 0
+unsat
+9+2QHvrRgbKz97Zg0kfybw 1 0
+unsat
+6kquszLXeBUhTwzaw6gd2Q 1 0
+unsat
+j5Z04lpza+N5I1cpno5mtw 1 0
+unsat
+mapbfUM6Ils30x5nEBJmaw 1 0
+unsat
+e8P++0FczY3zhNhEVclACw 1 0
+unsat
+yXMQNOyCylhI+EH8hNYxHA 1 0
+unsat
+GkYN9j7cjrR2KR/lb04/qw 1 0
+unsat
+PajzgNjLWHwVHpjoje+gnA 1 0
+unsat
+URpJYU7D8PO0VRnciRgE5A 1 0
+unsat
+D9ZGhymoV3L6zbWsJlwG2A 1 0
+unsat
+0QLuovrnnANWnCkUY3l10g 1 0
+unsat
+CYprps2G0Au5F3Z7n3KTRg 1 0
+unsat
+iyIMuJd6zijfEao8zKnx2w 1 0
+unsat
+49jzsAwAEfR6NSFBhBEisQ 1 0
+unsat
+T0j6xFgrghxif91jL+2yAw 1 0
+unsat
+md/M3rVve0+8sQ6oqIoL2w 1 0
+unsat
+pY7C8PCf5lVVaim6q7PJcQ 1 0
+unsat
+4zCFLQf4Jrov/gmEvsBm4Q 43 0
#2 := false
#6 := 0::int
decl uf_1 :: (-> bv[2] int)
@@ -11438,11 +11131,9 @@
#287 := [th-lemma]: #627
[unit-resolution #287 #47 #635]: false
unsat
-
-czvSLyjMowmFNi82us4N2Q 7
-unsat
-
-aU+7kcyE8oAPbs5RjfuwIw 1160
+czvSLyjMowmFNi82us4N2Q 1 0
+unsat
+aU+7kcyE8oAPbs5RjfuwIw 50 0
#2 := false
decl uf_6 :: T2
#23 := uf_6
@@ -11493,8 +11184,7 @@
#66 := [asserted]: #26
[unit-resolution #66 #235]: false
unsat
-
-dXfueqZAXkudfE6G0VKkwg 2559
+dXfueqZAXkudfE6G0VKkwg 105 0
#2 := false
decl uf_6 :: (-> T4 T2)
decl uf_10 :: T4
@@ -11600,8 +11290,7 @@
#110 := [asserted]: #46
[unit-resolution #110 #238]: false
unsat
-
-Dc/6bNJffjYYplvoitScJQ 4578
+Dc/6bNJffjYYplvoitScJQ 181 0
#2 := false
decl uf_1 :: (-> T1 T2 T3)
decl uf_3 :: T2
@@ -11783,8 +11472,7 @@
#76 := [asserted]: #38
[unit-resolution #76 #489]: false
unsat
-
-jdmsd1j41Osn+WzTtqTUSQ 1352
+jdmsd1j41Osn+WzTtqTUSQ 62 0
#2 := false
decl up_4 :: (-> T1 T2 bool)
decl uf_3 :: T2
@@ -11847,8 +11535,7 @@
#73 := [unit-resolution #71 #68]: #72
[unit-resolution #73 #59 #61]: false
unsat
-
-EA8ecQ7czWL46/C3k7D7tg 2697
+EA8ecQ7czWL46/C3k7D7tg 115 0
#2 := false
decl up_2 :: (-> T2 bool)
decl uf_3 :: T2
@@ -11964,8 +11651,7 @@
#560 := [mp #344 #559]: #557
[unit-resolution #560 #576 #561]: false
unsat
-
-mNfbN3NQCB4ik2xJmLE1UQ 11936
+mNfbN3NQCB4ik2xJmLE1UQ 464 0
#2 := false
decl uf_2 :: (-> T2 T3 T3)
decl uf_4 :: T3
@@ -12430,8 +12116,7 @@
#177 := [asserted]: #53
[unit-resolution #177 #793]: false
unsat
-
-Jtmz+P173L9nRQkQk52h+Q 420
+Jtmz+P173L9nRQkQk52h+Q 21 0
#2 := false
decl up_1 :: (-> T1 bool)
#4 := (:var 0 T1)
@@ -12453,8 +12138,7 @@
#25 := [asserted]: #9
[mp #25 #34]: false
unsat
-
-YG20f6Uf93koN6rVg/alpA 9742
+YG20f6Uf93koN6rVg/alpA 366 0
#2 := false
decl uf_1 :: (-> int T1)
#37 := 6::int
@@ -12469,18 +12153,18 @@
#35 := (uf_1 #34)
#36 := (uf_3 #35)
#39 := (= #36 #38)
-#484 := (uf_3 #38)
-#372 := (= #484 #38)
-#485 := (= #38 #484)
-#592 := (uf_2 #38)
+#476 := (uf_3 #38)
+#403 := (= #476 #38)
+#531 := (= #38 #476)
+#620 := (uf_2 #38)
#142 := -10::int
-#496 := (+ -10::int #592)
-#497 := (uf_1 #496)
-#498 := (uf_3 #497)
-#499 := (= #484 #498)
+#513 := (+ -10::int #620)
+#472 := (uf_1 #513)
+#503 := (uf_3 #472)
+#505 := (= #476 #503)
#22 := 10::int
-#500 := (>= #592 10::int)
-#501 := (ite #500 #499 #485)
+#507 := (>= #620 10::int)
+#514 := (ite #507 #505 #531)
#4 := (:var 0 T1)
#21 := (uf_3 #4)
#707 := (pattern #21)
@@ -12554,12 +12238,12 @@
#212 := [mp #207 #211]: #193
#713 := [mp #212 #712]: #708
#336 := (not #708)
-#463 := (or #336 #501)
-#464 := [quant-inst]: #463
-#444 := [unit-resolution #464 #713]: #501
-#473 := (not #500)
-#453 := (<= #592 6::int)
-#597 := (= #592 6::int)
+#518 := (or #336 #514)
+#528 := [quant-inst]: #518
+#477 := [unit-resolution #528 #713]: #514
+#529 := (not #507)
+#498 := (<= #620 6::int)
+#610 := (= #620 6::int)
#10 := (:var 0 int)
#12 := (uf_1 #10)
#694 := (pattern #12)
@@ -12617,79 +12301,79 @@
#201 := [mp~ #99 #183]: #94
#700 := [mp #201 #699]: #695
#673 := (not #695)
-#576 := (or #673 #597)
-#607 := (>= 6::int 0::int)
-#591 := (not #607)
-#594 := (= 6::int #592)
-#595 := (or #594 #591)
-#577 := (or #673 #595)
-#579 := (iff #577 #576)
-#581 := (iff #576 #576)
-#582 := [rewrite]: #581
-#574 := (iff #595 #597)
-#586 := (or #597 false)
-#571 := (iff #586 #597)
-#573 := [rewrite]: #571
-#590 := (iff #595 #586)
-#588 := (iff #591 false)
+#591 := (or #673 #610)
+#526 := (>= 6::int 0::int)
+#527 := (not #526)
+#617 := (= 6::int #620)
+#621 := (or #617 #527)
+#592 := (or #673 #621)
+#595 := (iff #592 #591)
+#597 := (iff #591 #591)
+#593 := [rewrite]: #597
+#600 := (iff #621 #610)
+#614 := (or #610 false)
+#605 := (iff #614 #610)
+#606 := [rewrite]: #605
+#603 := (iff #621 #614)
+#613 := (iff #527 false)
#1 := true
#663 := (not true)
#666 := (iff #663 false)
#667 := [rewrite]: #666
-#585 := (iff #591 #663)
-#598 := (iff #607 true)
-#584 := [rewrite]: #598
-#587 := [monotonicity #584]: #585
-#589 := [trans #587 #667]: #588
-#596 := (iff #594 #597)
-#593 := [rewrite]: #596
-#570 := [monotonicity #593 #589]: #590
-#575 := [trans #570 #573]: #574
-#580 := [monotonicity #575]: #579
-#572 := [trans #580 #582]: #579
-#578 := [quant-inst]: #577
-#583 := [mp #578 #572]: #576
-#448 := [unit-resolution #583 #700]: #597
-#445 := (not #597)
-#446 := (or #445 #453)
-#442 := [th-lemma]: #446
-#447 := [unit-resolution #442 #448]: #453
-#437 := (not #453)
-#427 := (or #437 #473)
-#429 := [th-lemma]: #427
-#430 := [unit-resolution #429 #447]: #473
-#471 := (not #501)
-#477 := (or #471 #500 #485)
-#478 := [def-axiom]: #477
-#433 := [unit-resolution #478 #430 #444]: #485
-#373 := [symm #433]: #372
-#374 := (= #36 #484)
+#611 := (iff #527 #663)
+#599 := (iff #526 true)
+#601 := [rewrite]: #599
+#612 := [monotonicity #601]: #611
+#609 := [trans #612 #667]: #613
+#608 := (iff #617 #610)
+#602 := [rewrite]: #608
+#604 := [monotonicity #602 #609]: #603
+#607 := [trans #604 #606]: #600
+#596 := [monotonicity #607]: #595
+#598 := [trans #596 #593]: #595
+#594 := [quant-inst]: #592
+#584 := [mp #594 #598]: #591
+#478 := [unit-resolution #584 #700]: #610
+#453 := (not #610)
+#454 := (or #453 #498)
+#455 := [th-lemma]: #454
+#456 := [unit-resolution #455 #478]: #498
+#458 := (not #498)
+#459 := (or #458 #529)
+#460 := [th-lemma]: #459
+#302 := [unit-resolution #460 #456]: #529
+#508 := (not #514)
+#490 := (or #508 #507 #531)
+#491 := [def-axiom]: #490
+#461 := [unit-resolution #491 #302 #477]: #531
+#404 := [symm #461]: #403
+#405 := (= #36 #476)
#649 := (uf_2 #35)
-#554 := (+ -10::int #649)
-#549 := (uf_1 #554)
-#545 := (uf_3 #549)
-#381 := (= #545 #484)
-#395 := (= #549 #38)
-#394 := (= #554 6::int)
+#582 := (+ -10::int #649)
+#553 := (uf_1 #582)
+#556 := (uf_3 #553)
+#401 := (= #556 #476)
+#417 := (= #553 #38)
+#415 := (= #582 6::int)
#335 := (uf_2 #31)
#647 := -1::int
-#459 := (* -1::int #335)
-#460 := (+ #33 #459)
-#302 := (<= #460 0::int)
-#458 := (= #33 #335)
-#426 := (= #32 #31)
-#555 := (= #31 #32)
-#551 := (+ -10::int #335)
-#552 := (uf_1 #551)
-#553 := (uf_3 #552)
-#556 := (= #32 #553)
-#557 := (>= #335 10::int)
-#558 := (ite #557 #556 #555)
-#560 := (or #336 #558)
-#533 := [quant-inst]: #560
-#434 := [unit-resolution #533 #713]: #558
-#535 := (not #557)
-#531 := (<= #335 4::int)
+#502 := (* -1::int #335)
+#463 := (+ #33 #502)
+#464 := (<= #463 0::int)
+#486 := (= #33 #335)
+#445 := (= #32 #31)
+#574 := (= #31 #32)
+#575 := (+ -10::int #335)
+#576 := (uf_1 #575)
+#577 := (uf_3 #576)
+#578 := (= #32 #577)
+#579 := (>= #335 10::int)
+#580 := (ite #579 #578 #574)
+#572 := (or #336 #580)
+#583 := [quant-inst]: #572
+#457 := [unit-resolution #583 #713]: #580
+#562 := (not #579)
+#554 := (<= #335 4::int)
#324 := (= #335 4::int)
#659 := (or #673 #324)
#678 := (>= 4::int 0::int)
@@ -12719,125 +12403,109 @@
#277 := [trans #383 #385]: #382
#367 := [quant-inst]: #660
#655 := [mp #367 #277]: #659
-#438 := [unit-resolution #655 #700]: #324
-#431 := (not #324)
-#439 := (or #431 #531)
-#432 := [th-lemma]: #439
-#435 := [unit-resolution #432 #438]: #531
-#436 := (not #531)
-#422 := (or #436 #535)
-#424 := [th-lemma]: #422
-#425 := [unit-resolution #424 #435]: #535
-#534 := (not #558)
-#540 := (or #534 #557 #555)
-#541 := [def-axiom]: #540
-#423 := [unit-resolution #541 #425 #434]: #555
-#408 := [symm #423]: #426
-#410 := [monotonicity #408]: #458
-#411 := (not #458)
-#412 := (or #411 #302)
-#413 := [th-lemma]: #412
-#414 := [unit-resolution #413 #410]: #302
-#461 := (>= #460 0::int)
-#415 := (or #411 #461)
-#416 := [th-lemma]: #415
-#417 := [unit-resolution #416 #410]: #461
-#512 := (>= #335 4::int)
-#418 := (or #431 #512)
-#419 := [th-lemma]: #418
-#420 := [unit-resolution #419 #438]: #512
+#462 := [unit-resolution #655 #700]: #324
+#441 := (not #324)
+#444 := (or #441 #554)
+#448 := [th-lemma]: #444
+#450 := [unit-resolution #448 #462]: #554
+#451 := (not #554)
+#449 := (or #451 #562)
+#452 := [th-lemma]: #449
+#440 := [unit-resolution #452 #450]: #562
+#561 := (not #580)
+#566 := (or #561 #579 #574)
+#567 := [def-axiom]: #566
+#443 := [unit-resolution #567 #440 #457]: #574
+#446 := [symm #443]: #445
+#442 := [monotonicity #446]: #486
+#447 := (not #486)
+#437 := (or #447 #464)
+#427 := [th-lemma]: #437
+#429 := [unit-resolution #427 #442]: #464
+#471 := (>= #463 0::int)
+#430 := (or #447 #471)
+#433 := [th-lemma]: #430
+#434 := [unit-resolution #433 #442]: #471
+#560 := (>= #335 4::int)
+#438 := (or #441 #560)
+#431 := [th-lemma]: #438
+#439 := [unit-resolution #431 #462]: #560
#651 := (* -1::int #649)
#648 := (+ #34 #651)
-#521 := (<= #648 0::int)
+#625 := (<= #648 0::int)
#652 := (= #648 0::int)
-#630 := (>= #33 0::int)
-#421 := (not #461)
-#409 := (not #512)
-#398 := (or #630 #409 #421)
-#400 := [th-lemma]: #398
-#401 := [unit-resolution #400 #420 #417]: #630
-#468 := (not #630)
-#623 := (or #468 #652)
-#509 := (or #673 #468 #652)
+#643 := (>= #33 0::int)
+#435 := (not #471)
+#432 := (not #560)
+#436 := (or #643 #432 #435)
+#422 := [th-lemma]: #436
+#424 := [unit-resolution #422 #439 #434]: #643
+#644 := (not #643)
+#489 := (or #644 #652)
+#628 := (or #673 #644 #652)
#370 := (>= #34 0::int)
#371 := (not #370)
#650 := (= #34 #649)
#364 := (or #650 #371)
-#510 := (or #673 #364)
-#619 := (iff #510 #509)
-#470 := (or #673 #623)
-#615 := (iff #470 #509)
-#616 := [rewrite]: #615
-#618 := (iff #510 #470)
-#624 := (iff #364 #623)
-#643 := 1::int
-#638 := (* 1::int #33)
-#639 := (>= #638 0::int)
-#640 := (not #639)
-#632 := (or #640 #652)
-#625 := (iff #632 #623)
-#469 := (iff #640 #468)
-#637 := (iff #639 #630)
-#635 := (= #638 #33)
-#636 := [rewrite]: #635
-#466 := [monotonicity #636]: #637
-#622 := [monotonicity #466]: #469
-#626 := [monotonicity #622]: #625
-#628 := (iff #364 #632)
-#488 := (or #652 #640)
-#633 := (iff #488 #632)
-#634 := [rewrite]: #633
-#489 := (iff #364 #488)
-#646 := (iff #371 #640)
-#644 := (iff #370 #639)
-#645 := [rewrite]: #644
-#487 := [monotonicity #645]: #646
+#629 := (or #673 #364)
+#469 := (iff #629 #628)
+#636 := (or #673 #489)
+#466 := (iff #636 #628)
+#468 := [rewrite]: #466
+#630 := (iff #629 #636)
+#633 := (iff #364 #489)
+#646 := (or #652 #644)
+#631 := (iff #646 #489)
+#632 := [rewrite]: #631
+#487 := (iff #364 #646)
+#645 := (iff #371 #644)
+#638 := (iff #370 #643)
+#639 := [rewrite]: #638
+#640 := [monotonicity #639]: #645
#641 := (iff #650 #652)
#642 := [rewrite]: #641
-#631 := [monotonicity #642 #487]: #489
-#629 := [trans #631 #634]: #628
-#627 := [trans #629 #626]: #624
-#520 := [monotonicity #627]: #618
-#504 := [trans #520 #616]: #619
-#511 := [quant-inst]: #510
-#519 := [mp #511 #504]: #509
-#402 := [unit-resolution #519 #700]: #623
-#403 := [unit-resolution #402 #401]: #652
-#404 := (not #652)
-#405 := (or #404 #521)
-#406 := [th-lemma]: #405
-#399 := [unit-resolution #406 #403]: #521
-#522 := (>= #648 0::int)
-#407 := (or #404 #522)
-#392 := [th-lemma]: #407
-#393 := [unit-resolution #392 #403]: #522
-#396 := [th-lemma #393 #399 #420 #435 #417 #414]: #394
-#397 := [monotonicity #396]: #395
-#391 := [monotonicity #397]: #381
-#550 := (= #36 #545)
-#559 := (= #35 #36)
-#530 := (>= #649 10::int)
-#476 := (ite #530 #550 #559)
-#536 := (or #336 #476)
-#537 := [quant-inst]: #536
-#386 := [unit-resolution #537 #713]: #476
-#387 := (not #521)
-#388 := (or #530 #387 #409 #421)
-#380 := [th-lemma]: #388
-#389 := [unit-resolution #380 #399 #420 #417]: #530
-#538 := (not #530)
-#532 := (not #476)
-#506 := (or #532 #538 #550)
-#513 := [def-axiom]: #506
-#390 := [unit-resolution #513 #389 #386]: #550
-#365 := [trans #390 #391]: #374
-#375 := [trans #365 #373]: #39
+#488 := [monotonicity #642 #640]: #487
+#634 := [trans #488 #632]: #633
+#637 := [monotonicity #634]: #630
+#622 := [trans #637 #468]: #469
+#635 := [quant-inst]: #629
+#623 := [mp #635 #622]: #628
+#425 := [unit-resolution #623 #700]: #489
+#423 := [unit-resolution #425 #424]: #652
+#426 := (not #652)
+#408 := (or #426 #625)
+#410 := [th-lemma]: #408
+#411 := [unit-resolution #410 #423]: #625
+#626 := (>= #648 0::int)
+#412 := (or #426 #626)
+#413 := [th-lemma]: #412
+#414 := [unit-resolution #413 #423]: #626
+#416 := [th-lemma #414 #411 #439 #450 #434 #429]: #415
+#418 := [monotonicity #416]: #417
+#402 := [monotonicity #418]: #401
+#557 := (= #36 #556)
+#581 := (= #35 #36)
+#558 := (>= #649 10::int)
+#559 := (ite #558 #557 #581)
+#533 := (or #336 #559)
+#534 := [quant-inst]: #533
+#419 := [unit-resolution #534 #713]: #559
+#420 := (not #625)
+#409 := (or #558 #420 #432 #435)
+#421 := [th-lemma]: #409
+#398 := [unit-resolution #421 #411 #439 #434]: #558
+#428 := (not #558)
+#535 := (not #559)
+#539 := (or #535 #428 #557)
+#540 := [def-axiom]: #539
+#400 := [unit-resolution #540 #398 #419]: #557
+#406 := [trans #400 #402]: #405
+#399 := [trans #406 #404]: #39
#40 := (not #39)
#182 := [asserted]: #40
-[unit-resolution #182 #375]: false
-unsat
-
-/fwo5o8vhLVHyS4oYEs4QA 10902
+[unit-resolution #182 #399]: false
+unsat
+/fwo5o8vhLVHyS4oYEs4QA 408 0
#2 := false
#22 := 0::int
#8 := 2::int
@@ -12913,18 +12581,18 @@
#604 := [trans #593 #597]: #562
#603 := [quant-inst]: #596
#606 := [mp #603 #604]: #628
-#516 := [unit-resolution #606 #817]: #566
-#498 := (not #566)
-#432 := (or #498 #608)
-#411 := [th-lemma]: #432
-#413 := [unit-resolution #411 #516]: #608
+#528 := [unit-resolution #606 #817]: #566
+#521 := (not #566)
+#464 := (or #521 #608)
+#456 := [th-lemma]: #464
+#465 := [unit-resolution #456 #528]: #608
decl uf_10 :: int
#52 := uf_10
#57 := (mod uf_10 2::int)
#243 := (* -1::int #57)
#244 := (+ #56 #243)
#447 := (>= #244 0::int)
-#372 := (not #447)
+#387 := (not #447)
#245 := (= #244 0::int)
#248 := (not #245)
#218 := (* -1::int #55)
@@ -12944,9 +12612,9 @@
#662 := (not #672)
#1 := true
#81 := [true-axiom]: true
-#514 := (or false #662)
-#515 := [th-lemma]: #514
-#513 := [unit-resolution #515 #81]: #662
+#520 := (or false #662)
+#523 := [th-lemma]: #520
+#524 := [unit-resolution #523 #81]: #662
#701 := (* -1::int #613)
#204 := -2::int
#691 := (* -2::int #222)
@@ -12959,58 +12627,82 @@
#546 := [th-lemma]: #545
#548 := [unit-resolution #546 #81]: #692
#549 := (not #692)
-#482 := (or #549 #694)
-#483 := [th-lemma]: #482
-#484 := [unit-resolution #483 #548]: #694
+#497 := (or #549 #694)
+#482 := [th-lemma]: #497
+#483 := [unit-resolution #482 #548]: #694
#536 := (not #448)
-#382 := [hypothesis]: #536
+#395 := [hypothesis]: #536
#555 := (* -1::int uf_10)
#573 := (+ #51 #555)
#543 := (<= #573 0::int)
#53 := (= #51 uf_10)
#256 := (not #253)
#259 := (or #248 #256)
+#502 := 1::int
#731 := (div uf_10 2::int)
-#723 := (* -2::int #731)
-#521 := (* -2::int #624)
-#529 := (+ #521 #723)
+#515 := (* -1::int #731)
+#513 := (+ #640 #515)
#618 := (div #51 2::int)
-#583 := (* -2::int #618)
-#522 := (+ #583 #529)
-#528 := (* -2::int #57)
-#525 := (+ #528 #522)
-#524 := (* 2::int #56)
-#526 := (+ #524 #525)
-#523 := (* 2::int uf_10)
-#512 := (+ #523 #526)
-#520 := (>= #512 2::int)
+#514 := (* -1::int #618)
+#516 := (+ #514 #513)
+#498 := (+ #243 #516)
+#500 := (+ #56 #498)
+#501 := (+ uf_10 #500)
+#503 := (>= #501 1::int)
+#486 := (not #503)
+#361 := (<= #244 0::int)
#453 := (not #259)
-#519 := [hypothesis]: #453
+#517 := [hypothesis]: #453
#440 := (or #259 #245)
#451 := [def-axiom]: #440
-#470 := [unit-resolution #451 #519]: #245
-#465 := (or #248 #447)
-#466 := [th-lemma]: #465
-#457 := [unit-resolution #466 #470]: #447
-#544 := (>= #573 0::int)
-#441 := (not #544)
+#519 := [unit-resolution #451 #517]: #245
+#478 := (or #248 #361)
+#470 := [th-lemma]: #478
+#479 := [unit-resolution #470 #519]: #361
+#449 := (>= #252 0::int)
#452 := (or #259 #253)
#380 := [def-axiom]: #452
-#481 := [unit-resolution #380 #519]: #253
-#467 := (or #256 #448)
-#434 := [th-lemma]: #467
-#436 := [unit-resolution #434 #481]: #448
-#532 := (or #543 #536)
-#695 := (>= #699 0::int)
-#550 := (or #549 #695)
-#393 := [th-lemma]: #550
-#551 := [unit-resolution #393 #548]: #695
-#547 := (not #543)
-#552 := [hypothesis]: #547
+#480 := [unit-resolution #380 #517]: #253
+#471 := (or #256 #449)
+#481 := [th-lemma]: #471
+#462 := [unit-resolution #481 #480]: #449
+#487 := (not #361)
+#485 := (not #449)
+#476 := (or #486 #485 #487)
+#607 := (<= #620 0::int)
+#529 := (or #521 #607)
+#522 := [th-lemma]: #529
+#525 := [unit-resolution #522 #528]: #607
+#723 := (* -2::int #731)
+#724 := (+ #243 #723)
+#718 := (+ uf_10 #724)
+#720 := (<= #718 0::int)
+#722 := (= #718 0::int)
+#526 := (or false #722)
+#512 := [th-lemma]: #526
+#504 := [unit-resolution #512 #81]: #722
+#505 := (not #722)
+#506 := (or #505 #720)
+#507 := [th-lemma]: #506
+#508 := [unit-resolution #507 #504]: #720
+#509 := [hypothesis]: #361
+#583 := (* -2::int #618)
+#584 := (+ #583 #640)
+#585 := (+ #51 #584)
+#587 := (<= #585 0::int)
+#582 := (= #585 0::int)
+#510 := (or false #582)
+#499 := [th-lemma]: #510
+#511 := [unit-resolution #499 #81]: #582
+#488 := (not #582)
+#490 := (or #488 #587)
+#491 := [th-lemma]: #490
+#492 := [unit-resolution #491 #511]: #587
+#493 := [hypothesis]: #503
#649 := (* -2::int #60)
#644 := (+ #218 #649)
#650 := (+ #51 #644)
-#631 := (<= #650 0::int)
+#636 := (>= #650 0::int)
#623 := (= #650 0::int)
#43 := (uf_7 uf_2 #35)
#44 := (uf_6 #34 #43)
@@ -13071,6 +12763,33 @@
#630 := [quant-inst]: #629
#531 := [unit-resolution #630 #824]: #623
#534 := (not #623)
+#494 := (or #534 #636)
+#495 := [th-lemma]: #494
+#496 := [unit-resolution #495 #531]: #636
+#489 := [hypothesis]: #449
+#484 := [th-lemma #483 #489 #496 #493 #492 #509 #508 #525 #524]: false
+#477 := [lemma #484]: #476
+#463 := [unit-resolution #477 #462 #479]: #486
+#727 := (>= #718 0::int)
+#466 := (or #505 #727)
+#457 := [th-lemma]: #466
+#467 := [unit-resolution #457 #504]: #727
+#434 := (or #248 #447)
+#436 := [th-lemma]: #434
+#437 := [unit-resolution #436 #519]: #447
+#544 := (>= #573 0::int)
+#445 := (not #544)
+#428 := (or #256 #448)
+#441 := [th-lemma]: #428
+#442 := [unit-resolution #441 #480]: #448
+#532 := (or #543 #536)
+#695 := (>= #699 0::int)
+#550 := (or #549 #695)
+#393 := [th-lemma]: #550
+#551 := [unit-resolution #393 #548]: #695
+#547 := (not #543)
+#552 := [hypothesis]: #547
+#631 := (<= #650 0::int)
#538 := (or #534 #631)
#540 := [th-lemma]: #538
#541 := [unit-resolution #540 #531]: #631
@@ -13081,8 +12800,8 @@
#533 := [unit-resolution #530 #81]: #666
#535 := [th-lemma #533 #539 #541 #552 #551]: false
#537 := [lemma #535]: #532
-#437 := [unit-resolution #537 #436]: #543
-#444 := (or #547 #441)
+#443 := [unit-resolution #537 #442]: #543
+#429 := (or #547 #445)
#764 := (not #53)
#771 := (or #764 #259)
#262 := (iff #53 #259)
@@ -13135,121 +12854,67 @@
#438 := (or #764 #259 #433)
#439 := [def-axiom]: #438
#772 := [unit-resolution #439 #267]: #771
-#428 := [unit-resolution #772 #519]: #764
-#442 := (or #53 #547 #441)
-#443 := [th-lemma]: #442
-#445 := [unit-resolution #443 #428]: #444
-#435 := [unit-resolution #445 #437]: #441
-#584 := (+ #583 #640)
-#585 := (+ #51 #584)
+#444 := [unit-resolution #772 #517]: #764
+#435 := (or #53 #547 #445)
+#446 := [th-lemma]: #435
+#431 := [unit-resolution #446 #444]: #429
+#432 := [unit-resolution #431 #443]: #445
#588 := (>= #585 0::int)
-#582 := (= #585 0::int)
-#499 := (or false #582)
-#511 := [th-lemma]: #499
-#488 := [unit-resolution #511 #81]: #582
-#490 := (not #582)
-#446 := (or #490 #588)
-#429 := [th-lemma]: #446
-#431 := [unit-resolution #429 #488]: #588
-#724 := (+ #243 #723)
-#718 := (+ uf_10 #724)
-#727 := (>= #718 0::int)
-#722 := (= #718 0::int)
-#503 := (or false #722)
-#504 := [th-lemma]: #503
-#505 := [unit-resolution #504 #81]: #722
-#506 := (not #722)
-#418 := (or #506 #727)
-#419 := [th-lemma]: #418
-#420 := [unit-resolution #419 #505]: #727
-#421 := [th-lemma #420 #413 #431 #435 #457]: #520
-#485 := (not #520)
-#361 := (<= #244 0::int)
-#479 := (or #248 #361)
-#480 := [th-lemma]: #479
-#471 := [unit-resolution #480 #470]: #361
-#449 := (>= #252 0::int)
-#462 := (or #256 #449)
-#463 := [th-lemma]: #462
-#464 := [unit-resolution #463 #481]: #449
-#476 := (not #361)
-#487 := (not #449)
-#477 := (or #485 #487 #476)
-#607 := (<= #620 0::int)
-#500 := (or #498 #607)
-#501 := [th-lemma]: #500
-#502 := [unit-resolution #501 #516]: #607
-#720 := (<= #718 0::int)
-#507 := (or #506 #720)
-#508 := [th-lemma]: #507
-#509 := [unit-resolution #508 #505]: #720
-#510 := [hypothesis]: #361
-#587 := (<= #585 0::int)
-#491 := (or #490 #587)
-#492 := [th-lemma]: #491
-#493 := [unit-resolution #492 #488]: #587
-#494 := [hypothesis]: #520
-#636 := (>= #650 0::int)
-#495 := (or #534 #636)
-#496 := [th-lemma]: #495
-#489 := [unit-resolution #496 #531]: #636
-#497 := [hypothesis]: #449
-#486 := [th-lemma #484 #497 #489 #494 #493 #510 #509 #502 #513]: false
-#478 := [lemma #486]: #477
-#456 := [unit-resolution #478 #464 #471]: #485
-#422 := [unit-resolution #456 #421]: false
-#423 := [lemma #422]: #259
+#411 := (or #488 #588)
+#413 := [th-lemma]: #411
+#418 := [unit-resolution #413 #511]: #588
+#419 := [th-lemma #418 #432 #437 #467 #465 #463]: false
+#420 := [lemma #419]: #259
#427 := (or #53 #453)
#768 := (or #53 #453 #433)
#770 := [def-axiom]: #768
#557 := [unit-resolution #770 #267]: #427
-#399 := [unit-resolution #557 #423]: #53
-#385 := (or #764 #543)
-#386 := [th-lemma]: #385
-#387 := [unit-resolution #386 #399]: #543
-#379 := [th-lemma #489 #387 #382 #484 #513]: false
-#388 := [lemma #379]: #448
-#381 := (or #253 #536)
-#397 := [hypothesis]: #487
-#400 := (or #764 #544)
-#403 := [th-lemma]: #400
-#398 := [unit-resolution #403 #399]: #544
-#404 := [th-lemma #398 #397 #533 #551 #541]: false
-#378 := [lemma #404]: #449
-#395 := (or #253 #536 #487)
-#377 := [th-lemma]: #395
-#658 := [unit-resolution #377 #378]: #381
-#653 := [unit-resolution #658 #388]: #253
+#406 := [unit-resolution #557 #420]: #53
+#377 := (or #764 #543)
+#381 := [th-lemma]: #377
+#382 := [unit-resolution #381 #406]: #543
+#385 := [th-lemma #496 #382 #395 #483 #524]: false
+#386 := [lemma #385]: #448
+#390 := (or #253 #536)
+#408 := [hypothesis]: #485
+#409 := (or #764 #544)
+#397 := [th-lemma]: #409
+#399 := [unit-resolution #397 #406]: #544
+#400 := [th-lemma #399 #408 #533 #551 #541]: false
+#403 := [lemma #400]: #449
+#392 := (or #253 #536 #485)
+#394 := [th-lemma]: #392
+#657 := [unit-resolution #394 #403]: #390
+#658 := [unit-resolution #657 #386]: #253
#450 := (or #453 #248 #256)
#454 := [def-axiom]: #450
-#664 := [unit-resolution #454 #423]: #259
-#665 := [unit-resolution #664 #653]: #248
-#373 := (or #245 #372)
-#708 := (+ #57 #640)
-#705 := (>= #708 0::int)
-#560 := (= #57 #624)
-#408 := (= #624 #57)
-#406 := [monotonicity #399]: #408
-#409 := [symm #406]: #560
-#706 := (not #560)
-#655 := (or #706 #705)
-#569 := [th-lemma]: #655
-#570 := [unit-resolution #569 #409]: #705
-#383 := [hypothesis]: #476
-#384 := [th-lemma #502 #383 #570]: false
-#389 := [lemma #384]: #361
-#369 := (or #245 #476 #372)
-#370 := [th-lemma]: #369
-#374 := [unit-resolution #370 #389]: #373
-#375 := [unit-resolution #374 #665]: #372
-#610 := (<= #708 0::int)
-#371 := (or #706 #610)
-#376 := [th-lemma]: #371
-#363 := [unit-resolution #376 #409]: #610
-[th-lemma #363 #375 #413]: false
-unsat
-
-s8LL71+1HTN+eIuEYeKhUw 1251
+#762 := [unit-resolution #454 #420]: #259
+#664 := [unit-resolution #762 #658]: #248
+#372 := (or #245 #387)
+#560 := (+ #57 #640)
+#610 := (>= #560 0::int)
+#742 := (= #57 #624)
+#424 := (= #624 #57)
+#405 := [monotonicity #406]: #424
+#407 := [symm #405]: #742
+#705 := (not #742)
+#706 := (or #705 #610)
+#568 := [th-lemma]: #706
+#569 := [unit-resolution #568 #407]: #610
+#398 := [hypothesis]: #487
+#404 := [th-lemma #525 #398 #569]: false
+#378 := [lemma #404]: #361
+#379 := (or #245 #487 #387)
+#388 := [th-lemma]: #379
+#369 := [unit-resolution #388 #378]: #372
+#370 := [unit-resolution #369 #664]: #387
+#708 := (<= #560 0::int)
+#373 := (or #705 #708)
+#374 := [th-lemma]: #373
+#375 := [unit-resolution #374 #407]: #708
+[th-lemma #375 #370 #465]: false
+unsat
+s8LL71+1HTN+eIuEYeKhUw 50 0
#2 := false
decl up_35 :: (-> int bool)
#112 := 1::int
@@ -13300,8 +12965,7 @@
#504 := [quant-inst]: #503
[unit-resolution #504 #916 #297]: false
unsat
-
-MZYsU5krlrOK4MkB71Ikeg 12985
+MZYsU5krlrOK4MkB71Ikeg 506 0
#2 := false
decl uf_17 :: (-> T8 T3)
decl uf_18 :: (-> T1 T8)
@@ -13808,4 +13472,3 @@
#325 := [asserted]: #108
[unit-resolution #325 #554]: false
unsat
-