============================== Prover9 =============================== Prover9 (32) version April-2007, April 2007. Process 6906 was started by hoefnepe on europa, Mon Oct 1 08:01:50 2007 The command was "../../../kleene/Prover9/bin/prover9 -f lmA1short.in". ============================== end of head =========================== ============================== INPUT ================================= % Reading from file lmA1short.in op(500,infix_left,"+"). op(490,infix_left,";"). op(480,postfix,"*"). op(450,postfix,"^"). formulas(sos). x + y = y + x. x + 0 = x. x + (y + z) = x + y + z. x ; 1 = x & 1 ; x = x. x ; (y ; z) = x ; y ; z. 0 ; x = 0. x + x = x. (x + y) ; z = x ; z + y ; z. x <= y -> z ; x <= z ; y. 1 + x ; x * = x *. x ; y + z <= y -> x * ; z <= y. x ; x ^ = x ^. y <= x ; y + z -> y <= x ^ + x * ; z. y <= x ; y -> y <= x ^. x <= x. x <= y & y <= z -> x <= z. x <= y -> x ; z <= y ; z. x <= y -> x + z <= y + z. x <= y -> x * <= y *. x <= y -> x ^ <= y ^. (x ; y) ^ <= (x + y) ^. (x ; y ; z) ^ <= (x + y + z) ^. (all p (p <= 1 & p ; p = p -> p ; (p ; x) ^ = (p ; x) ^)). end_of_list. formulas(goals). (all p all q all r (p <= 1 & p ; p = p & q <= 1 & q ; q = q & r <= 1 & r ; r = r -> (p ; x ; q ; y ; r ; z) ^ <= p ; (p ; x ; q + q ; y ; r + r ; z) ^)). end_of_list. ============================== end of input ========================== ============================== PROCESS NON-CLAUSAL FORMULAS ========== % Formulas that are not ordinary clauses: 1 x ; 1 = x & 1 ; x = x. [assumption]. 2 x <= y -> z ; x <= z ; y. [assumption]. 3 x ; y + z <= y -> x * ; z <= y. [assumption]. 4 y <= x ; y + z -> y <= x ^ + x * ; z. [assumption]. 5 y <= x ; y -> y <= x ^. [assumption]. 6 x <= y & y <= z -> x <= z. [assumption]. 7 x <= y -> x ; z <= y ; z. [assumption]. 8 x <= y -> x + z <= y + z. [assumption]. 9 x <= y -> x * <= y *. [assumption]. 10 x <= y -> x ^ <= y ^. [assumption]. 11 (all p (p <= 1 & p ; p = p -> p ; (p ; x) ^ = (p ; x) ^)). [assumption]. 12 (all p all q all r (p <= 1 & p ; p = p & q <= 1 & q ; q = q & r <= 1 & r ; r = r -> (p ; x ; q ; y ; r ; z) ^ <= p ; (p ; x ; q + q ; y ; r + r ; z) ^)) # label(goal). [goal]. ============================== end of process non-clausal formulas === ============================== PROCESS INITIAL CLAUSES =============== % Clauses before input processing: formulas(usable). end_of_list. formulas(sos). x + y = y + x. [assumption]. x + 0 = x. [assumption]. x + (y + z) = x + y + z. [assumption]. x ; 1 = x. [clausify(1)]. 1 ; x = x. [clausify(1)]. x ; (y ; z) = x ; y ; z. [assumption]. 0 ; x = 0. [assumption]. x + x = x. [assumption]. (x + y) ; z = x ; z + y ; z. [assumption]. -(x <= y) | z ; x <= z ; y. [clausify(2)]. 1 + x ; x * = x *. [assumption]. -(x ; y + z <= y) | x * ; z <= y. [clausify(3)]. x ; x ^ = x ^. [assumption]. -(x <= y ; x + z) | x <= y ^ + y * ; z. [clausify(4)]. -(x <= y ; x) | x <= y ^. [clausify(5)]. x <= x. [assumption]. -(x <= y) | -(y <= z) | x <= z. [clausify(6)]. -(x <= y) | x ; z <= y ; z. [clausify(7)]. -(x <= y) | x + z <= y + z. [clausify(8)]. -(x <= y) | x * <= y *. [clausify(9)]. -(x <= y) | x ^ <= y ^. [clausify(10)]. (x ; y) ^ <= (x + y) ^. [assumption]. (x ; y ; z) ^ <= (x + y + z) ^. [assumption]. -(x <= 1) | x ; x != x | (x ; y) ^ = x ; (x ; y) ^. [clausify(11)]. c4 <= 1. [deny(12)]. c4 ; c4 = c4. [deny(12)]. c5 <= 1. [deny(12)]. c5 ; c5 = c5. [deny(12)]. c6 <= 1. [deny(12)]. c6 ; c6 = c6. [deny(12)]. -((c4 ; c1 ; c5 ; c2 ; c6 ; c3) ^ <= c4 ; (c4 ; c1 ; c5 + c5 ; c2 ; c6 + c6 ; c3) ^). [deny(12)]. end_of_list. formulas(demodulators). end_of_list. ============================== PREDICATE ELIMINATION ================= No predicates eliminated. ============================== end predicate elimination ============= Auto_denials: (no changes). Term ordering decisions: Relation symbol precedence: lex([ <=, = ]). Function symbol precedence: lex([ 1, 0, c1, c2, c3, c4, c5, c6, ;, +, ^, * ]). After inverse_order: (no changes). Unfolding symbols: (none). Auto_inference settings: % set(paramodulation). % (positive equality literals) % set(paramodulation) -> set(back_demod). % set(hyper_resolution). % (nonunit Horn with equality) % set(neg_ur_resolution). % (nonunit Horn with equality) % assign(para_lit_limit, 3). % (nonunit Horn with equality) Auto_process settings: (no changes). % Operation + is commutative; C redundancy checks enabled. ============================== end of process initial clauses ======== ============================== CLAUSES FOR SEARCH ==================== % Clauses after input processing: formulas(usable). end_of_list. formulas(sos). 13 x + y = y + x. [assumption]. 14 x + 0 = x. [assumption]. 16 x + y + z = x + (y + z). [copy(15),flip(a)]. 17 x ; 1 = x. [clausify(1)]. 18 1 ; x = x. [clausify(1)]. 20 x ; y ; z = x ; (y ; z). [copy(19),flip(a)]. 21 0 ; x = 0. [assumption]. 22 x + x = x. [assumption]. 24 x ; y + z ; y = (x + z) ; y. [copy(23),flip(a)]. 25 -(x <= y) | z ; x <= z ; y. [clausify(2)]. 26 1 + x ; x * = x *. [assumption]. 27 -(x ; y + z <= y) | x * ; z <= y. [clausify(3)]. 28 x ; x ^ = x ^. [assumption]. 29 -(x <= y ; x + z) | x <= y ^ + y * ; z. [clausify(4)]. 30 -(x <= y ; x) | x <= y ^. [clausify(5)]. 31 x <= x. [assumption]. 32 -(x <= y) | -(y <= z) | x <= z. [clausify(6)]. 33 -(x <= y) | x ; z <= y ; z. [clausify(7)]. 34 -(x <= y) | x + z <= y + z. [clausify(8)]. 35 -(x <= y) | x * <= y *. [clausify(9)]. 36 -(x <= y) | x ^ <= y ^. [clausify(10)]. 37 (x ; y) ^ <= (x + y) ^. [assumption]. 39 (x ; (y ; z)) ^ <= (x + (y + z)) ^. [copy(38),rewrite(20(2),16(5))]. 41 -(x <= 1) | x ; x != x | x ; (x ; y) ^ = (x ; y) ^. [copy(40),flip(c)]. 42 c4 <= 1. [deny(12)]. 43 c4 ; c4 = c4. [deny(12)]. 44 c5 <= 1. [deny(12)]. 45 c5 ; c5 = c5. [deny(12)]. 46 c6 <= 1. [deny(12)]. 47 c6 ; c6 = c6. [deny(12)]. 49 -((c4 ; (c1 ; (c5 ; (c2 ; (c6 ; c3))))) ^ <= c4 ; (c6 ; c3 + (c4 ; (c1 ; c5) + c5 ; (c2 ; c6))) ^). [copy(48),rewrite(20(5),20(7),20(6),20(9),20(8),20(7),20(11),20(10),20(9),20(8),20(18),20(23),13(28))]. end_of_list. formulas(demodulators). 13 x + y = y + x. [assumption]. % (lex-dep) 14 x + 0 = x. [assumption]. 16 x + y + z = x + (y + z). [copy(15),flip(a)]. 17 x ; 1 = x. [clausify(1)]. 18 1 ; x = x. [clausify(1)]. 20 x ; y ; z = x ; (y ; z). [copy(19),flip(a)]. 21 0 ; x = 0. [assumption]. 22 x + x = x. [assumption]. 24 x ; y + z ; y = (x + z) ; y. [copy(23),flip(a)]. 26 1 + x ; x * = x *. [assumption]. 28 x ; x ^ = x ^. [assumption]. 43 c4 ; c4 = c4. [deny(12)]. 45 c5 ; c5 = c5. [deny(12)]. 47 c6 ; c6 = c6. [deny(12)]. end_of_list. ============================== end of clauses for search ============= ============================== SEARCH ================================ % Starting search at 0.01 seconds. given #1 (I,wt=7): 13 x + y = y + x. [assumption]. given #2 (I,wt=5): 14 x + 0 = x. [assumption]. given #3 (I,wt=11): 16 x + y + z = x + (y + z). [copy(15),flip(a)]. % Operation + is associative-commutative; CAC redundancy checks enabled. % back CAC tautology: 51 x + (y + z) = z + (x + y). [para(16(a,1),13(a,1))]. given #4 (I,wt=5): 17 x ; 1 = x. [clausify(1)]. given #5 (I,wt=5): 18 1 ; x = x. [clausify(1)]. given #6 (I,wt=11): 20 x ; y ; z = x ; (y ; z). [copy(19),flip(a)]. given #7 (I,wt=5): 21 0 ; x = 0. [assumption]. given #8 (I,wt=5): 22 x + x = x. [assumption]. given #9 (I,wt=13): 24 x ; y + z ; y = (x + z) ; y. [copy(23),flip(a)]. given #10 (I,wt=10): 25 -(x <= y) | z ; x <= z ; y. [clausify(2)]. given #11 (I,wt=9): 26 1 + x ; x * = x *. [assumption]. given #12 (I,wt=13): 27 -(x ; y + z <= y) | x * ; z <= y. [clausify(3)]. given #13 (I,wt=7): 28 x ; x ^ = x ^. [assumption]. given #14 (I,wt=16): 29 -(x <= y ; x + z) | x <= y ^ + y * ; z. [clausify(4)]. given #15 (I,wt=9): 30 -(x <= y ; x) | x <= y ^. [clausify(5)]. given #16 (I,wt=3): 31 x <= x. [assumption]. given #17 (I,wt=9): 32 -(x <= y) | -(y <= z) | x <= z. [clausify(6)]. given #18 (I,wt=10): 33 -(x <= y) | x ; z <= y ; z. [clausify(7)]. given #19 (I,wt=10): 34 -(x <= y) | x + z <= y + z. [clausify(8)]. given #20 (I,wt=8): 35 -(x <= y) | x * <= y *. [clausify(9)]. given #21 (I,wt=8): 36 -(x <= y) | x ^ <= y ^. [clausify(10)]. given #22 (I,wt=9): 37 (x ; y) ^ <= (x + y) ^. [assumption]. given #23 (I,wt=13): 39 (x ; (y ; z)) ^ <= (x + (y + z)) ^. [copy(38),rewrite(20(2),16(5))]. given #24 (I,wt=19): 41 -(x <= 1) | x ; x != x | x ; (x ; y) ^ = (x ; y) ^. [copy(40),flip(c)]. given #25 (I,wt=3): 42 c4 <= 1. [deny(12)]. given #26 (I,wt=5): 43 c4 ; c4 = c4. [deny(12)]. given #27 (I,wt=3): 44 c5 <= 1. [deny(12)]. given #28 (I,wt=5): 45 c5 ; c5 = c5. [deny(12)]. given #29 (I,wt=3): 46 c6 <= 1. [deny(12)]. given #30 (I,wt=5): 47 c6 ; c6 = c6. [deny(12)]. given #31 (A,wt=5): 50 0 + x = x. [para(14(a,1),13(a,1)),flip(a)]. given #32 (F,wt=31): 53 -((c4 ; (c1 ; (c5 ; (c2 ; (c6 ; c3))))) ^ <= c4 ; (c4 ; (c1 ; c5) + (c5 ; (c2 ; c6) + c6 ; c3)) ^). [back_rewrite(49),rewrite(51(28),13(27),52(28))]. given #33 (F,wt=31): 165 -((c1 + (c4 + c5 ; (c2 ; (c6 ; c3)))) ^ <= c4 ; (c4 ; (c1 ; c5) + (c5 ; (c2 ; c6) + c6 ; c3)) ^). [ur(32,a,39,a,c,53,a),rewrite(52(11))]. given #34 (F,wt=31): 166 -((c4 + c1 ; (c5 ; (c2 ; (c6 ; c3)))) ^ <= c4 ; (c4 ; (c1 ; c5) + (c5 ; (c2 ; c6) + c6 ; c3)) ^). [ur(32,a,37,a,c,53,a)]. given #35 (T,wt=4): 65 0 * = 1. [para(21(a,1),26(a,1,2)),rewrite(14(3)),flip(a)]. given #36 (T,wt=4): 76 0 ^ = 0. [para(28(a,1),21(a,1))]. given #37 (T,wt=4): 102 0 <= x ^. [para(21(a,1),37(a,1,1)),rewrite(76(2),50(3))]. given #38 (T,wt=5): 129 c4 ^ <= 1 ^. [hyper(36,a,42,a)]. given #39 (A,wt=11): 52 x + (y + z) = y + (x + z). [para(13(a,1),16(a,1,1)),rewrite(16(2))]. given #40 (T,wt=5): 130 c4 * <= 1 *. [hyper(35,a,42,a)]. given #41 (T,wt=5): 132 c4 ; x <= x. [hyper(33,a,42,a),rewrite(18(4))]. given #42 (T,wt=5): 133 x ; c4 <= x. [hyper(25,a,42,a),rewrite(17(4))]. given #43 (T,wt=5): 141 c5 ^ <= 1 ^. [hyper(36,a,44,a)]. given #44 (A,wt=9): 54 x + (x + y) = x + y. [para(22(a,1),16(a,1,1)),flip(a)]. given #45 (F,wt=33): 209 -((c4 + c1 ; (c5 ; (c2 ; (c6 ; c3)))) ^ <= c4 ; ((c4 ; (c1 ; c5) + (c5 ; (c2 ; c6) + c6 ; c3)) ^ ; c4)). [ur(32,b,133,a,c,166,a),rewrite(20(32))]. given #46 (F,wt=33): 210 -((c1 + (c4 + c5 ; (c2 ; (c6 ; c3)))) ^ <= c4 ; ((c4 ; (c1 ; c5) + (c5 ; (c2 ; c6) + c6 ; c3)) ^ ; c4)). [ur(32,b,133,a,c,165,a),rewrite(20(32))]. given #47 (F,wt=33): 211 -((c4 ; (c1 ; (c5 ; (c2 ; (c6 ; c3))))) ^ <= c4 ; ((c4 ; (c1 ; c5) + (c5 ; (c2 ; c6) + c6 ; c3)) ^ ; c4)). [ur(32,b,133,a,c,53,a),rewrite(20(32))]. given #48 (T,wt=5): 142 c5 * <= 1 *. [hyper(35,a,44,a)]. given #49 (T,wt=5): 144 c5 ; x <= x. [hyper(33,a,44,a),rewrite(18(4))]. given #50 (T,wt=5): 145 x ; c5 <= x. [hyper(25,a,44,a),rewrite(17(4))]. given #51 (T,wt=5): 153 c6 ^ <= 1 ^. [hyper(36,a,46,a)]. given #52 (A,wt=9): 56 x + (y + x) = y + x. [para(22(a,1),16(a,2,2)),rewrite(13(2))]. given #53 (F,wt=33): 251 -((c4 + c1 ; (c5 ; (c2 ; (c6 ; c3)))) ^ <= c5 ; (c4 ; (c4 ; (c1 ; c5) + (c5 ; (c2 ; c6) + c6 ; c3)) ^)). [ur(32,b,144,a,c,166,a)]. given #54 (F,wt=33): 252 -((c1 + (c4 + c5 ; (c2 ; (c6 ; c3)))) ^ <= c5 ; (c4 ; (c4 ; (c1 ; c5) + (c5 ; (c2 ; c6) + c6 ; c3)) ^)). [ur(32,b,144,a,c,165,a)]. given #55 (F,wt=33): 253 -((c4 ; (c1 ; (c5 ; (c2 ; (c6 ; c3))))) ^ <= c5 ; (c4 ; (c4 ; (c1 ; c5) + (c5 ; (c2 ; c6) + c6 ; c3)) ^)). [ur(32,b,144,a,c,53,a)]. given #56 (F,wt=33): 272 -((c4 + c1 ; (c5 ; (c2 ; (c6 ; c3)))) ^ <= c4 ; ((c4 ; (c1 ; c5) + (c5 ; (c2 ; c6) + c6 ; c3)) ^ ; c5)). [ur(32,b,145,a,c,166,a),rewrite(20(32))]. given #57 (T,wt=5): 154 c6 * <= 1 *. [hyper(35,a,46,a)]. given #58 (T,wt=5): 156 c6 ; x <= x. [hyper(33,a,46,a),rewrite(18(4))]. given #59 (T,wt=5): 157 x ; c6 <= x. [hyper(25,a,46,a),rewrite(17(4))]. given #60 (T,wt=5): 167 1 <= x ^ *. [hyper(35,a,102,a),rewrite(65(2))]. given #61 (A,wt=17): 57 (x + y) ; z + u = x ; z + (y ; z + u). [para(24(a,1),16(a,1,1))]. given #62 (F,wt=33): 273 -((c1 + (c4 + c5 ; (c2 ; (c6 ; c3)))) ^ <= c4 ; ((c4 ; (c1 ; c5) + (c5 ; (c2 ; c6) + c6 ; c3)) ^ ; c5)). [ur(32,b,145,a,c,165,a),rewrite(20(32))]. given #63 (F,wt=33): 274 -((c4 ; (c1 ; (c5 ; (c2 ; (c6 ; c3))))) ^ <= c4 ; ((c4 ; (c1 ; c5) + (c5 ; (c2 ; c6) + c6 ; c3)) ^ ; c5)). [ur(32,b,145,a,c,53,a),rewrite(20(32))]. given #64 (F,wt=33): 333 -((c4 + c1 ; (c5 ; (c2 ; (c6 ; c3)))) ^ <= c6 ; (c4 ; (c4 ; (c1 ; c5) + (c5 ; (c2 ; c6) + c6 ; c3)) ^)). [ur(32,b,156,a,c,166,a)]. given #65 (F,wt=33): 334 -((c1 + (c4 + c5 ; (c2 ; (c6 ; c3)))) ^ <= c6 ; (c4 ; (c4 ; (c1 ; c5) + (c5 ; (c2 ; c6) + c6 ; c3)) ^)). [ur(32,b,156,a,c,165,a)]. given #66 (T,wt=5): 193 c4 ; c6 <= 1. [hyper(32,a,132,a,b,46,a)]. given #67 (T,wt=5): 194 c4 ; c5 <= 1. [hyper(32,a,132,a,b,44,a)]. given #68 (T,wt=5): 204 c6 ; c4 <= 1. [hyper(32,a,133,a,b,46,a)]. given #69 (T,wt=5): 205 c5 ; c4 <= 1. [hyper(32,a,133,a,b,44,a)]. given #70 (A,wt=11): 58 (1 + x) ; y = y + x ; y. [para(18(a,1),24(a,1,1)),flip(a)]. given #71 (F,wt=33): 335 -((c4 ; (c1 ; (c5 ; (c2 ; (c6 ; c3))))) ^ <= c6 ; (c4 ; (c4 ; (c1 ; c5) + (c5 ; (c2 ; c6) + c6 ; c3)) ^)). [ur(32,b,156,a,c,53,a)]. given #72 (F,wt=33): 362 -((c4 + c1 ; (c5 ; (c2 ; (c6 ; c3)))) ^ <= c4 ; ((c4 ; (c1 ; c5) + (c5 ; (c2 ; c6) + c6 ; c3)) ^ ; c6)). [ur(32,b,157,a,c,166,a),rewrite(20(32))]. given #73 (F,wt=33): 363 -((c1 + (c4 + c5 ; (c2 ; (c6 ; c3)))) ^ <= c4 ; ((c4 ; (c1 ; c5) + (c5 ; (c2 ; c6) + c6 ; c3)) ^ ; c6)). [ur(32,b,157,a,c,165,a),rewrite(20(32))]. given #74 (F,wt=33): 364 -((c4 ; (c1 ; (c5 ; (c2 ; (c6 ; c3))))) ^ <= c4 ; ((c4 ; (c1 ; c5) + (c5 ; (c2 ; c6) + c6 ; c3)) ^ ; c6)). [ur(32,b,157,a,c,53,a),rewrite(20(32))]. given #75 (T,wt=5): 244 c5 ; c6 <= 1. [hyper(32,a,144,a,b,46,a)]. given #76 (T,wt=5): 265 c6 ; c5 <= 1. [hyper(32,a,145,a,b,46,a)]. given #77 (T,wt=5): 369 c6 <= x ^ *. [hyper(32,a,157,a,b,167,a),rewrite(18(3))]. given #78 (T,wt=5): 370 c5 <= x ^ *. [hyper(32,a,145,a,b,167,a),rewrite(18(3))]. given #79 (A,wt=11): 59 (x + 1) ; y = y + x ; y. [para(18(a,1),24(a,1,2)),rewrite(13(2)),flip(a)]. given #80 (F,wt=35): 248 -((c4 ; (c1 ; (c5 ; (c2 ; (c6 ; c3))))) ^ <= c5 ; (c4 ; ((c4 ; (c1 ; c5) + (c5 ; (c2 ; c6) + c6 ; c3)) ^ ; c4))). [ur(32,b,144,a,c,211,a)]. given #81 (F,wt=35): 249 -((c1 + (c4 + c5 ; (c2 ; (c6 ; c3)))) ^ <= c5 ; (c4 ; ((c4 ; (c1 ; c5) + (c5 ; (c2 ; c6) + c6 ; c3)) ^ ; c4))). [ur(32,b,144,a,c,210,a)]. given #82 (F,wt=35): 250 -((c4 + c1 ; (c5 ; (c2 ; (c6 ; c3)))) ^ <= c5 ; (c4 ; ((c4 ; (c1 ; c5) + (c5 ; (c2 ; c6) + c6 ; c3)) ^ ; c4))). [ur(32,b,144,a,c,209,a)]. given #83 (F,wt=35): 269 -((c4 ; (c1 ; (c5 ; (c2 ; (c6 ; c3))))) ^ <= c4 ; ((c4 ; (c1 ; c5) + (c5 ; (c2 ; c6) + c6 ; c3)) ^ ; (c4 ; c5))). [ur(32,b,145,a,c,211,a),rewrite(20(34),20(33))]. given #84 (T,wt=5): 371 c4 <= x ^ *. [hyper(32,a,133,a,b,167,a),rewrite(18(3))]. given #85 (T,wt=6): 168 x <= y ^ + x. [hyper(34,a,102,a),rewrite(50(2))]. given #86 (T,wt=6): 169 0 <= x ^ ; y. [hyper(33,a,102,a),rewrite(21(2))]. given #87 (T,wt=6): 192 c4 ; 0 <= x ^. [hyper(32,a,132,a,b,102,a)]. given #88 (A,wt=17): 60 x ; (y ; z) + u ; z = (x ; y + u) ; z. [para(20(a,1),24(a,1,1))]. given #89 (F,wt=34): 569 -(x ^ + (c4 + c1 ; (c5 ; (c2 ; (c6 ; c3)))) ^ <= c4 ; (c4 ; (c1 ; c5) + (c5 ; (c2 ; c6) + c6 ; c3)) ^). [ur(32,a,168,a,c,166,a)]. given #90 (F,wt=34): 570 -(x ^ + (c1 + (c4 + c5 ; (c2 ; (c6 ; c3)))) ^ <= c4 ; (c4 ; (c1 ; c5) + (c5 ; (c2 ; c6) + c6 ; c3)) ^). [ur(32,a,168,a,c,165,a)]. given #91 (F,wt=34): 571 -(x ^ + (c4 ; (c1 ; (c5 ; (c2 ; (c6 ; c3))))) ^ <= c4 ; (c4 ; (c1 ; c5) + (c5 ; (c2 ; c6) + c6 ; c3)) ^). [ur(32,a,168,a,c,53,a)]. given #92 (F,wt=34): 609 -((c4 + c1 ; (c5 ; (c2 ; (c6 ; c3)))) ^ + x ^ <= c4 ; (c4 ; (c1 ; c5) + (c5 ; (c2 ; c6) + c6 ; c3)) ^). [para(13(a,1),569(a,1))]. given #93 (T,wt=6): 243 c5 ; 0 <= x ^. [hyper(32,a,144,a,b,102,a)]. given #94 (T,wt=6): 322 c6 ; 0 <= x ^. [hyper(32,a,156,a,b,102,a)]. given #95 (T,wt=6): 544 c6 <= 1 + x ^. [hyper(32,a,46,a,b,168,a),rewrite(13(4))]. given #96 (T,wt=6): 545 c5 <= 1 + x ^. [hyper(32,a,44,a,b,168,a),rewrite(13(4))]. given #97 (A,wt=17): 61 x ; y + z ; (u ; y) = (x + z ; u) ; y. [para(20(a,1),24(a,1,2))]. given #98 (F,wt=34): 611 -((c1 + (c4 + c5 ; (c2 ; (c6 ; c3)))) ^ + x ^ <= c4 ; (c4 ; (c1 ; c5) + (c5 ; (c2 ; c6) + c6 ; c3)) ^). [para(13(a,1),570(a,1))]. given #99 (F,wt=34): 613 -((c4 ; (c1 ; (c5 ; (c2 ; (c6 ; c3))))) ^ + x ^ <= c4 ; (c4 ; (c1 ; c5) + (c5 ; (c2 ; c6) + c6 ; c3)) ^). [para(13(a,1),571(a,1))]. given #100 (F,wt=35): 270 -((c1 + (c4 + c5 ; (c2 ; (c6 ; c3)))) ^ <= c4 ; ((c4 ; (c1 ; c5) + (c5 ; (c2 ; c6) + c6 ; c3)) ^ ; (c4 ; c5))). [ur(32,b,145,a,c,210,a),rewrite(20(34),20(33))]. given #101 (F,wt=35): 271 -((c4 + c1 ; (c5 ; (c2 ; (c6 ; c3)))) ^ <= c4 ; ((c4 ; (c1 ; c5) + (c5 ; (c2 ; c6) + c6 ; c3)) ^ ; (c4 ; c5))). [ur(32,b,145,a,c,209,a),rewrite(20(34),20(33))]. given #102 (T,wt=6): 546 c4 <= 1 + x ^. [hyper(32,a,42,a,b,168,a),rewrite(13(4))]. given #103 (T,wt=6): 572 x <= x + y ^. [para(13(a,1),168(a,2))]. given #104 (T,wt=7): 88 -(1 <= x) | 1 <= x ^. [para(17(a,1),30(a,2))]. given #105 (T,wt=4): 723 1 <= 1 ^. [hyper(88,a,31,a)]. given #106 (A,wt=13): 62 1 + (x ; x * + y) = x * + y. [para(26(a,1),16(a,1,1)),flip(a)]. given #107 (F,wt=35): 292 -((c4 + c1 ; (c5 ; (c2 ; (c6 ; c3)))) ^ <= c5 ; (c4 ; ((c4 ; (c1 ; c5) + (c5 ; (c2 ; c6) + c6 ; c3)) ^ ; c5))). [ur(32,b,145,a,c,251,a),rewrite(20(34),20(33))]. given #108 (F,wt=35): 293 -((c4 + c1 ; (c5 ; (c2 ; (c6 ; c3)))) ^ <= c4 ; (c5 ; (c4 ; (c4 ; (c1 ; c5) + (c5 ; (c2 ; c6) + c6 ; c3)) ^))). [ur(32,b,132,a,c,251,a)]. given #109 (F,wt=35): 294 -((c1 + (c4 + c5 ; (c2 ; (c6 ; c3)))) ^ <= c5 ; (c4 ; ((c4 ; (c1 ; c5) + (c5 ; (c2 ; c6) + c6 ; c3)) ^ ; c5))). [ur(32,b,145,a,c,252,a),rewrite(20(34),20(33))]. given #110 (F,wt=35): 295 -((c1 + (c4 + c5 ; (c2 ; (c6 ; c3)))) ^ <= c4 ; (c5 ; (c4 ; (c4 ; (c1 ; c5) + (c5 ; (c2 ; c6) + c6 ; c3)) ^))). [ur(32,b,132,a,c,252,a)]. given #111 (T,wt=4): 735 c6 <= 1 ^. [hyper(32,a,157,a,b,723,a),rewrite(18(3))]. given #112 (T,wt=4): 736 c5 <= 1 ^. [hyper(32,a,145,a,b,723,a),rewrite(18(3))]. given #113 (T,wt=4): 737 c4 <= 1 ^. [hyper(32,a,133,a,b,723,a),rewrite(18(3))]. given #114 (T,wt=5): 724 1 <= 1 ^ ^. [hyper(88,a,723,a)]. given #115 (A,wt=15): 64 1 + x ; (y ; (x ; y) *) = (x ; y) *. [para(20(a,1),26(a,1,2))]. given #116 (F,wt=35): 296 -((c4 ; (c1 ; (c5 ; (c2 ; (c6 ; c3))))) ^ <= c5 ; (c4 ; ((c4 ; (c1 ; c5) + (c5 ; (c2 ; c6) + c6 ; c3)) ^ ; c5))). [ur(32,b,145,a,c,253,a),rewrite(20(34),20(33))]. given #117 (F,wt=35): 297 -((c4 ; (c1 ; (c5 ; (c2 ; (c6 ; c3))))) ^ <= c4 ; (c5 ; (c4 ; (c4 ; (c1 ; c5) + (c5 ; (c2 ; c6) + c6 ; c3)) ^))). [ur(32,b,132,a,c,253,a)]. given #118 (F,wt=35): 298 -((c4 + c1 ; (c5 ; (c2 ; (c6 ; c3)))) ^ <= c4 ; ((c4 ; (c1 ; c5) + (c5 ; (c2 ; c6) + c6 ; c3)) ^ ; (c5 ; c4))). [ur(32,b,133,a,c,272,a),rewrite(20(34),20(33))]. given #119 (F,wt=35): 326 -((c4 + c1 ; (c5 ; (c2 ; (c6 ; c3)))) ^ <= c6 ; (c4 ; ((c4 ; (c1 ; c5) + (c5 ; (c2 ; c6) + c6 ; c3)) ^ ; c5))). [ur(32,b,156,a,c,272,a)]. given #120 (T,wt=5): 812 c6 <= 1 ^ ^. [hyper(32,a,157,a,b,724,a),rewrite(18(3))]. given #121 (T,wt=5): 813 c5 <= 1 ^ ^. [hyper(32,a,145,a,b,724,a),rewrite(18(3))]. given #122 (T,wt=5): 814 c4 <= 1 ^ ^. [hyper(32,a,133,a,b,724,a),rewrite(18(3))]. given #123 (T,wt=6): 722 1 <= (x ^ *) ^. [hyper(88,a,167,a)]. given #124 (A,wt=13): 66 x + y ; (y * ; x) = y * ; x. [para(26(a,1),24(a,2,1)),rewrite(18(2),20(3))]. given #125 (F,wt=35): 327 -((c4 ; (c1 ; (c5 ; (c2 ; (c6 ; c3))))) ^ <= c6 ; (c5 ; (c4 ; (c4 ; (c1 ; c5) + (c5 ; (c2 ; c6) + c6 ; c3)) ^))). [ur(32,b,156,a,c,253,a)]. given #126 (F,wt=35): 328 -((c1 + (c4 + c5 ; (c2 ; (c6 ; c3)))) ^ <= c6 ; (c5 ; (c4 ; (c4 ; (c1 ; c5) + (c5 ; (c2 ; c6) + c6 ; c3)) ^))). [ur(32,b,156,a,c,252,a)]. given #127 (F,wt=35): 329 -((c4 + c1 ; (c5 ; (c2 ; (c6 ; c3)))) ^ <= c6 ; (c5 ; (c4 ; (c4 ; (c1 ; c5) + (c5 ; (c2 ; c6) + c6 ; c3)) ^))). [ur(32,b,156,a,c,251,a)]. given #128 (F,wt=35): 330 -((c4 ; (c1 ; (c5 ; (c2 ; (c6 ; c3))))) ^ <= c6 ; (c4 ; ((c4 ; (c1 ; c5) + (c5 ; (c2 ; c6) + c6 ; c3)) ^ ; c4))). [ur(32,b,156,a,c,211,a)]. given #129 (T,wt=6): 725 1 ^ <= 1 ^ ^. [hyper(36,a,723,a)]. given #130 (T,wt=6): 726 1 * <= 1 ^ *. [hyper(35,a,723,a)]. given #131 (T,wt=6): 728 x <= 1 ^ ; x. [hyper(33,a,723,a),rewrite(18(2))]. given #132 (T,wt=5): 985 x <= 1 ^ ^. [hyper(30,a,728,a)]. given #133 (A,wt=13): 67 -(x + y ; z <= z) | y * ; x <= z. [para(13(a,1),27(a,1))]. given #134 (F,wt=22): 1036 -(1 ^ ^ <= c4 ; (c4 ; (c1 ; c5) + (c5 ; (c2 ; c6) + c6 ; c3)) ^). [ur(32,a,985,a,c,613,a)]. given #135 (F,wt=24): 1037 -(1 ^ ^ <= c4 ; ((c4 ; (c1 ; c5) + (c5 ; (c2 ; c6) + c6 ; c3)) ^ ; c6)). [ur(32,a,985,a,c,364,a)]. given #136 (F,wt=24): 1038 -(1 ^ ^ <= c6 ; (c4 ; (c4 ; (c1 ; c5) + (c5 ; (c2 ; c6) + c6 ; c3)) ^)). [ur(32,a,985,a,c,335,a)]. given #137 (F,wt=24): 1045 -(1 ^ ^ <= c4 ; ((c4 ; (c1 ; c5) + (c5 ; (c2 ; c6) + c6 ; c3)) ^ ; c5)). [ur(32,a,985,a,c,274,a)]. given #138 (T,wt=6): 729 c6 ; c5 <= 1 ^. [hyper(32,a,265,a,b,723,a)]. given #139 (T,wt=6): 730 c5 ; c6 <= 1 ^. [hyper(32,a,244,a,b,723,a)]. given #140 (T,wt=6): 731 c5 ; c4 <= 1 ^. [hyper(32,a,205,a,b,723,a)]. given #141 (T,wt=6): 732 c6 ; c4 <= 1 ^. [hyper(32,a,204,a,b,723,a)]. given #142 (A,wt=11): 68 -(x ; y <= y) | x * ; 0 <= y. [para(14(a,1),27(a,1))]. given #143 (F,wt=24): 1047 -(1 ^ ^ <= c5 ; (c4 ; (c4 ; (c1 ; c5) + (c5 ; (c2 ; c6) + c6 ; c3)) ^)). [ur(32,a,985,a,c,253,a)]. given #144 (F,wt=24): 1049 -(1 ^ ^ <= c4 ; ((c4 ; (c1 ; c5) + (c5 ; (c2 ; c6) + c6 ; c3)) ^ ; c4)). [ur(32,a,985,a,c,211,a)]. given #145 (F,wt=25): 1067 -(1 ^ ^ + x ^ <= c4 ; (c4 ; (c1 ; c5) + (c5 ; (c2 ; c6) + c6 ; c3)) ^). [ur(32,a,572,a,c,1036,a)]. given #146 (F,wt=25): 1068 -(x ^ + 1 ^ ^ <= c4 ; (c4 ; (c1 ; c5) + (c5 ; (c2 ; c6) + c6 ; c3)) ^). [ur(32,a,168,a,c,1036,a)]. given #147 (T,wt=6): 733 c4 ; c5 <= 1 ^. [hyper(32,a,194,a,b,723,a)]. given #148 (T,wt=6): 734 c4 ; c6 <= 1 ^. [hyper(32,a,193,a,b,723,a)]. given #149 (T,wt=6): 740 x <= x ; 1 ^. [hyper(25,a,723,a),rewrite(17(2))]. given #150 (T,wt=6): 781 c6 * <= 1 ^ *. [hyper(35,a,735,a)]. given #151 (A,wt=11): 69 -(x + y <= 1) | x * ; y <= 1. [para(17(a,1),27(a,1,1))]. given #152 (F,wt=25): 1193 -(1 ^ ^ ; 1 ^ <= c4 ; (c4 ; (c1 ; c5) + (c5 ; (c2 ; c6) + c6 ; c3)) ^). [ur(32,a,740,a,c,1036,a)]. given #153 (F,wt=26): 1039 -(1 ^ ^ <= c6 ; (c4 ; ((c4 ; (c1 ; c5) + (c5 ; (c2 ; c6) + c6 ; c3)) ^ ; c4))). [ur(32,a,985,a,c,330,a)]. given #154 (F,wt=26): 1040 -(1 ^ ^ <= c6 ; (c5 ; (c4 ; (c4 ; (c1 ; c5) + (c5 ; (c2 ; c6) + c6 ; c3)) ^))). [ur(32,a,985,a,c,329,a)]. given #155 (F,wt=26): 1041 -(1 ^ ^ <= c6 ; (c4 ; ((c4 ; (c1 ; c5) + (c5 ; (c2 ; c6) + c6 ; c3)) ^ ; c5))). [ur(32,a,985,a,c,326,a)]. given #156 (T,wt=6): 788 c5 * <= 1 ^ *. [hyper(35,a,736,a)]. given #157 (T,wt=6): 795 c4 * <= 1 ^ *. [hyper(35,a,737,a)]. given #158 (T,wt=6): 801 1 <= 1 ^ ^ ^. [hyper(88,a,724,a)]. given #159 (T,wt=6): 887 c6 <= (x ^ *) ^. [hyper(32,a,157,a,b,722,a),rewrite(18(3))]. given #160 (A,wt=11): 70 -(x + y <= x) | 1 * ; y <= x. [para(18(a,1),27(a,1,1))]. given #161 (F,wt=26): 1042 -(1 ^ ^ <= c4 ; ((c4 ; (c1 ; c5) + (c5 ; (c2 ; c6) + c6 ; c3)) ^ ; (c5 ; c4))). [ur(32,a,985,a,c,298,a)]. given #162 (F,wt=26): 1043 -(1 ^ ^ <= c4 ; (c5 ; (c4 ; (c4 ; (c1 ; c5) + (c5 ; (c2 ; c6) + c6 ; c3)) ^))). [ur(32,a,985,a,c,297,a)]. given #163 (F,wt=26): 1044 -(1 ^ ^ <= c5 ; (c4 ; ((c4 ; (c1 ; c5) + (c5 ; (c2 ; c6) + c6 ; c3)) ^ ; c5))). [ur(32,a,985,a,c,296,a)]. given #164 (F,wt=26): 1046 -(1 ^ ^ <= c4 ; ((c4 ; (c1 ; c5) + (c5 ; (c2 ; c6) + c6 ; c3)) ^ ; (c4 ; c5))). [ur(32,a,985,a,c,271,a)]. given #165 (T,wt=6): 888 c5 <= (x ^ *) ^. [hyper(32,a,145,a,b,722,a),rewrite(18(3))]. given #166 (T,wt=6): 889 c4 <= (x ^ *) ^. [hyper(32,a,133,a,b,722,a),rewrite(18(3))]. given #167 (T,wt=6): 1123 c6 * ; 0 <= x. [hyper(68,a,156,a)]. given #168 (T,wt=6): 1125 c5 * ; 0 <= x. [hyper(68,a,144,a)]. given #169 (A,wt=17): 71 -(x ; (y ; z) + u <= z) | (x ; y) * ; u <= z. [para(20(a,1),27(a,1,1))]. given #170 (F,wt=8): 1413 -(1 ^ ^ <= c6 * ; 0). [ur(32,b,1123,a,c,1049,a)]. given #171 (F,wt=8): 1433 -(1 ^ ^ <= c5 * ; 0). [ur(32,b,1125,a,c,1049,a)]. given #172 (F,wt=10): 1463 -(1 ^ ^ <= c5 ; (c6 * ; 0)). [ur(32,b,144,a,c,1413,a)]. given #173 (F,wt=10): 1464 -(1 ^ ^ <= c4 ; (c6 * ; 0)). [ur(32,b,132,a,c,1413,a)]. given #174 (T,wt=6): 1127 c4 * ; 0 <= x. [hyper(68,a,132,a)]. given #175 (T,wt=6): 1333 c6 <= 1 ^ ^ ^. [hyper(32,a,157,a,b,801,a),rewrite(18(3))]. given #176 (T,wt=6): 1334 c5 <= 1 ^ ^ ^. [hyper(32,a,145,a,b,801,a),rewrite(18(3))]. given #177 (T,wt=6): 1335 c4 <= 1 ^ ^ ^. [hyper(32,a,133,a,b,801,a),rewrite(18(3))]. given #178 (A,wt=13): 72 -(x ; y <= y) | x * ; (x ; y) <= y. [para(22(a,1),27(a,1))]. given #179 (F,wt=8): 1484 -(1 ^ ^ <= c4 * ; 0). [ur(32,b,1127,a,c,1464,a)]. given #180 (F,wt=10): 1465 -(1 ^ ^ <= c6 ; (c5 * ; 0)). [ur(32,b,156,a,c,1433,a)]. given #181 (F,wt=10): 1466 -(1 ^ ^ <= c4 ; (c5 * ; 0)). [ur(32,b,132,a,c,1433,a)]. given #182 (F,wt=10): 1536 -(1 ^ ^ <= c6 ; (c4 * ; 0)). [ur(32,b,156,a,c,1484,a)]. given #183 (T,wt=6): 1527 c6 * ; c6 <= c6. [hyper(72,a,157,a),rewrite(47(5))]. given #184 (T,wt=6): 1529 c5 * ; c5 <= c5. [hyper(72,a,145,a),rewrite(45(5))]. given #185 (T,wt=6): 1531 c4 * ; c4 <= c4. [hyper(72,a,133,a),rewrite(43(5))]. given #186 (T,wt=6): 1572 c6 * ; c6 <= 1. [hyper(32,a,1527,a,b,46,a)]. given #187 (A,wt=15): 73 -((x + y) ; z <= z) | x * ; (y ; z) <= z. [para(24(a,1),27(a,1))]. given #188 (F,wt=10): 1537 -(1 ^ ^ <= c5 ; (c4 * ; 0)). [ur(32,b,144,a,c,1484,a)]. given #189 (F,wt=11): 1410 -(1 ^ ^ ; 1 ^ <= c6 * ; 0). [ur(32,b,1123,a,c,1193,a)]. given #190 (F,wt=11): 1411 -(x ^ + 1 ^ ^ <= c6 * ; 0). [ur(32,b,1123,a,c,1068,a)]. given #191 (F,wt=11): 1412 -(1 ^ ^ + x ^ <= c6 * ; 0). [ur(32,b,1123,a,c,1067,a)]. given #192 (T,wt=6): 1593 c5 * ; c5 <= 1. [hyper(32,a,1529,a,b,44,a)]. given #193 (T,wt=6): 1614 c4 * ; c4 <= 1. [hyper(32,a,1531,a,b,42,a)]. given #194 (T,wt=7): 89 -(x <= x) | x <= 1 ^. [para(18(a,1),30(a,2))]. given #195 (T,wt=4): 1668 x <= 1 ^. [hyper(89,a,31,a)]. given #196 (A,wt=11): 74 x ; (x ^ ; y) = x ^ ; y. [para(28(a,1),20(a,1,1)),flip(a)]. given #197 (F,wt=7): 1678 -(1 ^ <= c4 * ; 0). [ur(32,a,1668,a,c,1484,a)]. given #198 (F,wt=7): 1683 -(1 ^ <= c5 * ; 0). [ur(32,a,1668,a,c,1433,a)]. given #199 (F,wt=7): 1684 -(1 ^ <= c6 * ; 0). [ur(32,a,1668,a,c,1413,a)]. given #200 (F,wt=9): 1676 -(1 ^ <= c5 ; (c4 * ; 0)). [ur(32,a,1668,a,c,1537,a)]. given #201 (T,wt=6): 1669 x * <= 1 ^ *. [hyper(35,a,1668,a)]. given #202 (T,wt=7): 97 (x ; 0) ^ <= x ^. [para(14(a,1),37(a,2,1))]. given #203 (T,wt=7): 99 x ^ <= (x + 1) ^. [para(17(a,1),37(a,1,1))]. given #204 (T,wt=7): 100 x ^ <= (1 + x) ^. [para(18(a,1),37(a,1,1))]. given #205 (A,wt=13): 75 x ; (y ; (x ; y) ^) = (x ; y) ^. [para(28(a,1),20(a,1)),flip(a)]. given #206 (F,wt=9): 1677 -(1 ^ <= c6 ; (c4 * ; 0)). [ur(32,a,1668,a,c,1536,a)]. given #207 (F,wt=9): 1679 -(1 ^ <= c4 ; (c5 * ; 0)). [ur(32,a,1668,a,c,1466,a)]. given #208 (F,wt=9): 1680 -(1 ^ <= c6 ; (c5 * ; 0)). [ur(32,a,1668,a,c,1465,a)]. given #209 (F,wt=9): 1681 -(1 ^ <= c4 ; (c6 * ; 0)). [ur(32,a,1668,a,c,1464,a)]. given #210 (T,wt=6): 1906 x ; 0 <= x ^. [back_rewrite(1759),rewrite(1865(3),20(4),21(3))]. given #211 (T,wt=7): 103 (x ; x) ^ <= x ^. [para(22(a,1),37(a,2,1))]. given #212 (T,wt=7): 131 c4 + x <= 1 + x. [hyper(34,a,42,a)]. given #213 (T,wt=5): 1974 c4 <= 1 + c4. [para(22(a,1),131(a,1))]. given #214 (A,wt=13): 77 (1 + x) ; y ^ = (y + x) ; y ^. [para(28(a,1),24(a,1,1)),rewrite(58(4,R))]. given #215 (F,wt=9): 1682 -(1 ^ <= c5 ; (c6 * ; 0)). [ur(32,a,1668,a,c,1463,a)]. given #216 (F,wt=10): 1722 -(1 ^ ; 1 ^ <= c4 * ; 0). [ur(32,a,740,a,c,1678,a)]. given #217 (F,wt=10): 1723 -(1 ^ + x ^ <= c4 * ; 0). [ur(32,a,572,a,c,1678,a)]. given #218 (F,wt=10): 1724 -(x ^ + 1 ^ <= c4 * ; 0). [ur(32,a,168,a,c,1678,a)]. given #219 (T,wt=5): 1975 1 + c4 <= 1. [para(22(a,1),131(a,2)),rewrite(13(3))]. given #220 (T,wt=6): 2061 1 * ; c4 <= 1. [hyper(70,a,1975,a)]. given #221 (T,wt=7): 140 -(c4 <= c4) | c4 <= c4 ^. [para(43(a,1),30(a,2))]. given #222 (T,wt=4): 2087 c4 <= c4 ^. [hyper(140,a,31,a)]. given #223 (A,wt=13): 78 (1 + x) ; y ^ = (x + y) ; y ^. [para(28(a,1),24(a,1,2)),rewrite(13(4),58(4,R))]. given #224 (F,wt=10): 1725 -(1 ^ ; 1 ^ <= c5 * ; 0). [ur(32,a,740,a,c,1683,a)]. given #225 (F,wt=10): 1726 -(1 ^ + x ^ <= c5 * ; 0). [ur(32,a,572,a,c,1683,a)]. given #226 (F,wt=10): 1727 -(x ^ + 1 ^ <= c5 * ; 0). [ur(32,a,168,a,c,1683,a)]. given #227 (F,wt=10): 1728 -(1 ^ ; 1 ^ <= c6 * ; 0). [ur(32,a,740,a,c,1684,a)]. given #228 (T,wt=6): 2088 c4 ^ <= c4 ^ ^. [hyper(36,a,2087,a)]. given #229 (T,wt=5): 2165 c4 <= c4 ^ ^. [hyper(32,a,2087,a,b,2088,a)]. given #230 (T,wt=6): 2089 c4 * <= c4 ^ *. [hyper(35,a,2087,a)]. given #231 (T,wt=6): 2093 c4 ; c6 <= c4 ^. [hyper(32,a,157,a,b,2087,a)]. given #232 (A,wt=14): 79 -(x ^ + y <= x ^) | x * ; y <= x ^. [para(28(a,1),27(a,1,1))]. given #233 (F,wt=10): 1729 -(1 ^ + x ^ <= c6 * ; 0). [ur(32,a,572,a,c,1684,a)]. given #234 (F,wt=10): 1730 -(x ^ + 1 ^ <= c6 * ; 0). [ur(32,a,168,a,c,1684,a)]. given #235 (F,wt=10): 1791 -((1 + 1 ^) ^ <= c4 * ; 0). [ur(32,a,99,a,c,1484,a),rewrite(13(4))]. given #236 (F,wt=10): 1796 -((1 + 1 ^) ^ <= c5 * ; 0). [ur(32,a,99,a,c,1433,a),rewrite(13(4))]. given #237 (T,wt=6): 2094 c6 ; c4 <= c4 ^. [hyper(32,a,156,a,b,2087,a)]. given #238 (T,wt=6): 2095 c4 ; c5 <= c4 ^. [hyper(32,a,145,a,b,2087,a)]. given #239 (T,wt=6): 2096 c5 ; c4 <= c4 ^. [hyper(32,a,144,a,b,2087,a)]. given #240 (T,wt=6): 2101 c4 <= (1 + c4) ^. [hyper(32,a,2087,a,b,100,a)]. given #241 (A,wt=16): 80 -(x <= y + z ; x) | x <= z ^ + z * ; y. [para(13(a,1),29(a,2))]. given #242 (F,wt=10): 1797 -((1 + 1 ^) ^ <= c6 * ; 0). [ur(32,a,99,a,c,1413,a),rewrite(13(4))]. given #243 (F,wt=11): 1430 -(1 ^ ^ ; 1 ^ <= c5 * ; 0). [ur(32,b,1125,a,c,1193,a)]. given #244 (F,wt=11): 1431 -(x ^ + 1 ^ ^ <= c5 * ; 0). [ur(32,b,1125,a,c,1068,a)]. given #245 (F,wt=11): 1432 -(1 ^ ^ + x ^ <= c5 * ; 0). [ur(32,b,1125,a,c,1067,a)]. given #246 (T,wt=7): 143 c5 + x <= 1 + x. [hyper(34,a,44,a)]. given #247 (T,wt=5): 2330 c4 + c5 <= 1. [hyper(32,a,143,a,b,1975,a),rewrite(13(3))]. given #248 (T,wt=5): 2337 c5 <= 1 + c5. [para(22(a,1),143(a,1))]. given #249 (T,wt=5): 2338 1 + c5 <= 1. [para(22(a,1),143(a,2)),rewrite(13(3))]. given #250 (A,wt=14): 81 -(x <= y ; x) | x <= y ^ + y * ; 0. [para(14(a,1),29(a,2))]. given #251 (F,wt=11): 1485 -(1 ^ ^ ; 1 ^ <= c4 * ; 0). [ur(32,b,1127,a,c,1193,a)]. given #252 (F,wt=11): 1486 -(x ^ + 1 ^ ^ <= c4 * ; 0). [ur(32,b,1127,a,c,1068,a)]. given #253 (F,wt=11): 1487 -(1 ^ ^ + x ^ <= c4 * ; 0). [ur(32,b,1127,a,c,1067,a)]. given #254 (F,wt=11): 1731 -(1 ^ <= c6 ; (c5 ; (c4 * ; 0))). [ur(32,b,156,a,c,1676,a)]. given #255 (T,wt=6): 2351 c4 * ; c5 <= 1. [hyper(69,a,2330,a)]. given #256 (T,wt=6): 2376 1 * ; c5 <= 1. [hyper(70,a,2338,a)]. given #257 (T,wt=7): 152 -(c5 <= c5) | c5 <= c5 ^. [para(45(a,1),30(a,2))]. given #258 (T,wt=4): 2447 c5 <= c5 ^. [hyper(152,a,31,a)]. given #259 (A,wt=14): 82 -(1 <= x + y) | 1 <= x ^ + x * ; y. [para(17(a,1),29(a,2,1))]. given #260 (F,wt=11): 1732 -(1 ^ <= c4 ; (c5 ; (c4 * ; 0))). [ur(32,b,132,a,c,1676,a)]. given #261 (F,wt=11): 1914 -(1 ^ <= c5 ; (c6 ; (c4 * ; 0))). [ur(32,b,144,a,c,1677,a)]. given #262 (F,wt=11): 1915 -(1 ^ <= c4 ; (c6 ; (c4 * ; 0))). [ur(32,b,132,a,c,1677,a)]. given #263 (F,wt=11): 1919 -(1 ^ <= c6 ; (c4 ; (c5 * ; 0))). [ur(32,b,156,a,c,1679,a)]. given #264 (T,wt=6): 2448 c5 ^ <= c5 ^ ^. [hyper(36,a,2447,a)]. given #265 (T,wt=5): 2503 c5 <= c5 ^ ^. [hyper(32,a,2447,a,b,2448,a)]. given #266 (T,wt=6): 2449 c5 * <= c5 ^ *. [hyper(35,a,2447,a)]. given #267 (T,wt=6): 2453 c5 ; c6 <= c5 ^. [hyper(32,a,157,a,b,2447,a)]. given #268 (A,wt=14): 83 -(x <= x + y) | x <= 1 ^ + 1 * ; y. [para(18(a,1),29(a,2,1))]. given #269 (F,wt=11): 1920 -(1 ^ <= c5 ; (c4 ; (c5 * ; 0))). [ur(32,b,144,a,c,1679,a)]. given #270 (F,wt=11): 1924 -(1 ^ <= c5 ; (c6 ; (c5 * ; 0))). [ur(32,b,144,a,c,1680,a)]. given #271 (F,wt=11): 1925 -(1 ^ <= c4 ; (c6 ; (c5 * ; 0))). [ur(32,b,132,a,c,1680,a)]. given #272 (F,wt=11): 1929 -(1 ^ <= c6 ; (c4 ; (c6 * ; 0))). [ur(32,b,156,a,c,1681,a)]. given #273 (T,wt=6): 2454 c6 ; c5 <= c5 ^. [hyper(32,a,156,a,b,2447,a)]. given #274 (T,wt=6): 2455 c5 ; c4 <= c5 ^. [hyper(32,a,133,a,b,2447,a)]. given #275 (T,wt=6): 2456 c4 ; c5 <= c5 ^. [hyper(32,a,132,a,b,2447,a)]. given #276 (T,wt=6): 2461 c5 <= (1 + c5) ^. [hyper(32,a,2447,a,b,100,a)]. given #277 (A,wt=22): 84 -(x <= y ; (z ; x) + u) | x <= (y ; z) ^ + (y ; z) * ; u. [para(20(a,1),29(a,2,1))]. given #278 (F,wt=11): 1930 -(1 ^ <= c5 ; (c4 ; (c6 * ; 0))). [ur(32,b,144,a,c,1681,a)]. given #279 (F,wt=11): 2046 -(1 ^ <= c6 ; (c5 ; (c6 * ; 0))). [ur(32,b,156,a,c,1682,a)]. given #280 (F,wt=11): 2047 -(1 ^ <= c4 ; (c5 ; (c6 * ; 0))). [ur(32,b,132,a,c,1682,a)]. given #281 (F,wt=12): 1467 -(1 ^ ^ <= c6 ; (c5 ; (c6 * ; 0))). [ur(32,b,156,a,c,1463,a)]. given #282 (T,wt=7): 155 c6 + x <= 1 + x. [hyper(34,a,46,a)]. given #283 (T,wt=5): 2690 c5 + c6 <= 1. [hyper(32,a,155,a,b,2338,a),rewrite(13(3))]. given #284 (T,wt=5): 2691 c4 + c6 <= 1. [hyper(32,a,155,a,b,1975,a),rewrite(13(3))]. given #285 (T,wt=5): 2698 c6 <= 1 + c6. [para(22(a,1),155(a,1))]. given #286 (A,wt=16): 85 -(x <= y ; x) | x <= y ^ + y * ; (y ; x). [para(22(a,1),29(a,2))]. given #287 (F,wt=12): 1468 -(1 ^ ^ <= c4 ; (c5 ; (c6 * ; 0))). [ur(32,b,132,a,c,1463,a)]. given #288 (F,wt=12): 1472 -(1 ^ ^ <= c6 ; (c4 ; (c6 * ; 0))). [ur(32,b,156,a,c,1464,a)]. given #289 (F,wt=12): 1473 -(1 ^ ^ <= c5 ; (c4 ; (c6 * ; 0))). [ur(32,b,144,a,c,1464,a)]. given #290 (F,wt=12): 1538 -(1 ^ ^ <= c5 ; (c6 ; (c5 * ; 0))). [ur(32,b,144,a,c,1465,a)]. given #291 (T,wt=5): 2699 1 + c6 <= 1. [para(22(a,1),155(a,2)),rewrite(13(3))]. given #292 (T,wt=6): 2712 c5 * ; c6 <= 1. [hyper(69,a,2690,a)]. given #293 (T,wt=6): 2726 c4 * ; c6 <= 1. [hyper(69,a,2691,a)]. given #294 (T,wt=6): 2790 1 * ; c6 <= 1. [hyper(70,a,2699,a)]. given #295 (A,wt=18): 86 -(x <= (y + z) ; x) | x <= y ^ + y * ; (z ; x). [para(24(a,1),29(a,2))]. given #296 (F,wt=12): 1539 -(1 ^ ^ <= c4 ; (c6 ; (c5 * ; 0))). [ur(32,b,132,a,c,1465,a)]. given #297 (F,wt=12): 1543 -(1 ^ ^ <= c6 ; (c4 ; (c5 * ; 0))). [ur(32,b,156,a,c,1466,a)]. given #298 (F,wt=12): 1544 -(1 ^ ^ <= c5 ; (c4 ; (c5 * ; 0))). [ur(32,b,144,a,c,1466,a)]. given #299 (F,wt=12): 1548 -(1 ^ ^ <= c5 ; (c6 ; (c4 * ; 0))). [ur(32,b,144,a,c,1536,a)]. given #300 (T,wt=7): 164 -(c6 <= c6) | c6 <= c6 ^. [para(47(a,1),30(a,2))]. given #301 (T,wt=4): 2878 c6 <= c6 ^. [hyper(164,a,31,a)]. given #302 (T,wt=6): 2879 c6 ^ <= c6 ^ ^. [hyper(36,a,2878,a)]. given #303 (T,wt=5): 2898 c6 <= c6 ^ ^. [hyper(32,a,2878,a,b,2879,a)]. given #304 (A,wt=17): 87 -(x ^ <= x ^ + y) | x ^ <= x ^ + x * ; y. [para(28(a,1),29(a,2,1))]. given #305 (F,wt=12): 1549 -(1 ^ ^ <= c4 ; (c6 ; (c4 * ; 0))). [ur(32,b,132,a,c,1536,a)]. given #306 (F,wt=12): 1634 -(1 ^ ^ <= c6 ; (c5 ; (c4 * ; 0))). [ur(32,b,156,a,c,1537,a)]. given #307 (F,wt=12): 1635 -(1 ^ ^ <= c4 ; (c5 ; (c4 * ; 0))). [ur(32,b,132,a,c,1537,a)]. given #308 (F,wt=12): 1733 -(1 ^ ; 1 ^ <= c5 ; (c4 * ; 0)). [ur(32,a,740,a,c,1676,a)]. given #309 (T,wt=6): 2880 c6 * <= c6 ^ *. [hyper(35,a,2878,a)]. given #310 (T,wt=6): 2884 c6 ; c5 <= c6 ^. [hyper(32,a,145,a,b,2878,a)]. given #311 (T,wt=6): 2885 c5 ; c6 <= c6 ^. [hyper(32,a,144,a,b,2878,a)]. given #312 (T,wt=6): 2886 c6 ; c4 <= c6 ^. [hyper(32,a,133,a,b,2878,a)]. given #313 (A,wt=13): 90 -(x <= y ; (z ; x)) | x <= (y ; z) ^. [para(20(a,1),30(a,2))]. given #314 (F,wt=12): 1734 -(1 ^ + x ^ <= c5 ; (c4 * ; 0)). [ur(32,a,572,a,c,1676,a)]. given #315 (F,wt=12): 1735 -(x ^ + 1 ^ <= c5 ; (c4 * ; 0)). [ur(32,a,168,a,c,1676,a)]. given #316 (F,wt=12): 1789 -((1 + 1 ^) ^ <= c5 ; (c4 * ; 0)). [ur(32,a,99,a,c,1537,a),rewrite(13(4))]. given #317 (F,wt=12): 1790 -((1 + 1 ^) ^ <= c6 ; (c4 * ; 0)). [ur(32,a,99,a,c,1536,a),rewrite(13(4))]. given #318 (T,wt=6): 2887 c4 ; c6 <= c6 ^. [hyper(32,a,132,a,b,2878,a)]. given #319 (T,wt=6): 2892 c6 <= (1 + c6) ^. [hyper(32,a,2878,a,b,100,a)]. given #320 (T,wt=7): 183 (c4 *) ^ <= (1 *) ^. [hyper(36,a,130,a)]. given #321 (T,wt=7): 184 c4 * * <= 1 * *. [hyper(35,a,130,a)]. given #322 (A,wt=11): 91 (x ; y) ^ ^ <= (x + y) ^ ^. [hyper(36,a,37,a)]. given #323 (F,wt=12): 1792 -((1 + 1 ^) ^ <= c4 ; (c5 * ; 0)). [ur(32,a,99,a,c,1466,a),rewrite(13(4))]. given #324 (F,wt=12): 1793 -((1 + 1 ^) ^ <= c6 ; (c5 * ; 0)). [ur(32,a,99,a,c,1465,a),rewrite(13(4))]. given #325 (F,wt=12): 1794 -((1 + 1 ^) ^ <= c4 ; (c6 * ; 0)). [ur(32,a,99,a,c,1464,a),rewrite(13(4))]. given #326 (F,wt=12): 1795 -((1 + 1 ^) ^ <= c5 ; (c6 * ; 0)). [ur(32,a,99,a,c,1463,a),rewrite(13(4))]. given #327 (T,wt=7): 188 (c4 ; x) ^ <= x ^. [hyper(36,a,132,a)]. given #328 (T,wt=7): 189 (c4 ; x) * <= x *. [hyper(35,a,132,a)]. given #329 (T,wt=7): 191 c4 ; c4 * <= 1 *. [hyper(32,a,132,a,b,130,a)]. given #330 (T,wt=7): 198 (x ; c4) ^ <= x ^. [hyper(36,a,133,a)]. given #331 (A,wt=11): 92 (x ; y) ^ * <= (x + y) ^ *. [hyper(35,a,37,a)]. given #332 (F,wt=12): 1916 -(1 ^ ; 1 ^ <= c6 ; (c4 * ; 0)). [ur(32,a,740,a,c,1677,a)]. given #333 (F,wt=12): 1917 -(1 ^ + x ^ <= c6 ; (c4 * ; 0)). [ur(32,a,572,a,c,1677,a)]. given #334 (F,wt=12): 1918 -(x ^ + 1 ^ <= c6 ; (c4 * ; 0)). [ur(32,a,168,a,c,1677,a)]. given #335 (F,wt=12): 1921 -(1 ^ ; 1 ^ <= c4 ; (c5 * ; 0)). [ur(32,a,740,a,c,1679,a)]. given #336 (T,wt=7): 199 (x ; c4) * <= x *. [hyper(35,a,133,a)]. given #337 (T,wt=7): 201 c4 ; (x ; c4) <= x. [hyper(32,a,132,a,b,133,a)]. given #338 (T,wt=7): 202 c4 * ; c4 <= 1 *. [hyper(32,a,133,a,b,130,a)]. given #339 (T,wt=7): 221 1 + x * = x *. [para(26(a,1),54(a,1,2)),rewrite(26(7))]. given #340 (A,wt=13): 93 (x ; y) ^ + z <= (x + y) ^ + z. [hyper(34,a,37,a)]. given #341 (F,wt=12): 1922 -(1 ^ + x ^ <= c4 ; (c5 * ; 0)). [ur(32,a,572,a,c,1679,a)]. given #342 (F,wt=12): 1923 -(x ^ + 1 ^ <= c4 ; (c5 * ; 0)). [ur(32,a,168,a,c,1679,a)]. given #343 (F,wt=12): 1926 -(1 ^ ; 1 ^ <= c6 ; (c5 * ; 0)). [ur(32,a,740,a,c,1680,a)]. given #344 (F,wt=12): 1927 -(1 ^ + x ^ <= c6 ; (c5 * ; 0)). [ur(32,a,572,a,c,1680,a)]. given #345 (T,wt=7): 227 (c5 *) ^ <= (1 *) ^. [hyper(36,a,142,a)]. given #346 (T,wt=7): 228 c5 * * <= 1 * *. [hyper(35,a,142,a)]. given #347 (T,wt=7): 231 c5 * ; c4 <= 1 *. [hyper(32,a,133,a,b,142,a)]. given #348 (T,wt=7): 232 c4 ; c5 * <= 1 *. [hyper(32,a,132,a,b,142,a)]. given #349 (A,wt=13): 94 (x ; y) ^ ; z <= (x + y) ^ ; z. [hyper(33,a,37,a)]. given #350 (F,wt=12): 1928 -(x ^ + 1 ^ <= c6 ; (c5 * ; 0)). [ur(32,a,168,a,c,1680,a)]. given #351 (F,wt=12): 1931 -(1 ^ ; 1 ^ <= c4 ; (c6 * ; 0)). [ur(32,a,740,a,c,1681,a)]. given #352 (F,wt=12): 1932 -(1 ^ + x ^ <= c4 ; (c6 * ; 0)). [ur(32,a,572,a,c,1681,a)]. given #353 (F,wt=12): 1933 -(x ^ + 1 ^ <= c4 ; (c6 * ; 0)). [ur(32,a,168,a,c,1681,a)]. given #354 (T,wt=7): 234 (c5 ; x) ^ <= x ^. [hyper(36,a,144,a)]. given #355 (T,wt=7): 235 (c5 ; x) * <= x *. [hyper(35,a,144,a)]. given #356 (T,wt=7): 237 c5 ; (x ; c4) <= x. [hyper(32,a,133,a,b,144,a),rewrite(20(4))]. given #357 (T,wt=7): 238 c4 ; (c5 ; x) <= x. [hyper(32,a,132,a,b,144,a)]. given #358 (A,wt=13): 95 x ; (y ; z) ^ <= x ; (y + z) ^. [hyper(25,a,37,a)]. given #359 (F,wt=12): 2048 -(1 ^ ; 1 ^ <= c5 ; (c6 * ; 0)). [ur(32,a,740,a,c,1682,a)]. given #360 (F,wt=12): 2049 -(1 ^ + x ^ <= c5 ; (c6 * ; 0)). [ur(32,a,572,a,c,1682,a)]. given #361 (F,wt=12): 2050 -(x ^ + 1 ^ <= c5 ; (c6 * ; 0)). [ur(32,a,168,a,c,1682,a)]. given #362 (F,wt=13): 1469 -(1 ^ ^ ; 1 ^ <= c5 ; (c6 * ; 0)). [ur(32,a,740,a,c,1463,a)]. given #363 (T,wt=7): 239 c5 ; c5 * <= 1 *. [hyper(32,a,144,a,b,142,a)]. given #364 (T,wt=7): 240 c5 ; (c4 ; x) <= x. [hyper(32,a,144,a,b,132,a)]. given #365 (T,wt=7): 241 c5 ; c4 * <= 1 *. [hyper(32,a,144,a,b,130,a)]. given #366 (T,wt=7): 254 (x ; c5) ^ <= x ^. [hyper(36,a,145,a)]. given #367 (A,wt=9): 96 (x ; y) ^ <= (y + x) ^. [para(13(a,1),37(a,2,1))]. given #368 (F,wt=13): 1470 -(1 ^ ^ + x ^ <= c5 ; (c6 * ; 0)). [ur(32,a,572,a,c,1463,a)]. given #369 (F,wt=13): 1471 -(x ^ + 1 ^ ^ <= c5 ; (c6 * ; 0)). [ur(32,a,168,a,c,1463,a)]. given #370 (F,wt=13): 1474 -(1 ^ ^ ; 1 ^ <= c4 ; (c6 * ; 0)). [ur(32,a,740,a,c,1464,a)]. given #371 (F,wt=13): 1475 -(1 ^ ^ + x ^ <= c4 ; (c6 * ; 0)). [ur(32,a,572,a,c,1464,a)]. given #372 (T,wt=7): 255 (x ; c5) * <= x *. [hyper(35,a,145,a)]. given #373 (T,wt=7): 257 c5 ; (x ; c5) <= x. [hyper(32,a,144,a,b,145,a)]. given #374 (T,wt=7): 258 x ; (c5 ; c4) <= x. [hyper(32,a,133,a,b,145,a),rewrite(20(4))]. given #375 (T,wt=7): 259 c4 ; (x ; c5) <= x. [hyper(32,a,132,a,b,145,a)]. given #376 (A,wt=13): 98 ((x + y) ; z) ^ <= (x + (y + z)) ^. [para(16(a,1),37(a,2,1))]. given #377 (F,wt=13): 1476 -(x ^ + 1 ^ ^ <= c4 ; (c6 * ; 0)). [ur(32,a,168,a,c,1464,a)]. given #378 (F,wt=13): 1540 -(1 ^ ^ ; 1 ^ <= c6 ; (c5 * ; 0)). [ur(32,a,740,a,c,1465,a)]. given #379 (F,wt=13): 1541 -(1 ^ ^ + x ^ <= c6 ; (c5 * ; 0)). [ur(32,a,572,a,c,1465,a)]. given #380 (F,wt=13): 1542 -(x ^ + 1 ^ ^ <= c6 ; (c5 * ; 0)). [ur(32,a,168,a,c,1465,a)]. given #381 (T,wt=7): 260 c5 * ; c5 <= 1 *. [hyper(32,a,145,a,b,142,a)]. given #382 (T,wt=7): 262 x ; (c4 ; c5) <= x. [hyper(32,a,145,a,b,133,a),rewrite(20(4))]. given #383 (T,wt=7): 263 c4 * ; c5 <= 1 *. [hyper(32,a,145,a,b,130,a)]. given #384 (T,wt=7): 299 (c6 *) ^ <= (1 *) ^. [hyper(36,a,154,a)]. given #385 (A,wt=13): 101 (x ; (y ; z)) ^ <= (x ; y + z) ^. [para(20(a,1),37(a,1,1))]. given #386 (F,wt=13): 1545 -(1 ^ ^ ; 1 ^ <= c4 ; (c5 * ; 0)). [ur(32,a,740,a,c,1466,a)]. given #387 (F,wt=13): 1546 -(1 ^ ^ + x ^ <= c4 ; (c5 * ; 0)). [ur(32,a,572,a,c,1466,a)]. given #388 (F,wt=13): 1547 -(x ^ + 1 ^ ^ <= c4 ; (c5 * ; 0)). [ur(32,a,168,a,c,1466,a)]. given #389 (F,wt=13): 1550 -(1 ^ ^ ; 1 ^ <= c6 ; (c4 * ; 0)). [ur(32,a,740,a,c,1536,a)]. given #390 (T,wt=7): 300 c6 * * <= 1 * *. [hyper(35,a,154,a)]. given #391 (T,wt=7): 303 c6 * ; c5 <= 1 *. [hyper(32,a,145,a,b,154,a)]. given #392 (T,wt=7): 304 c5 ; c6 * <= 1 *. [hyper(32,a,144,a,b,154,a)]. given #393 (T,wt=7): 305 c6 * ; c4 <= 1 *. [hyper(32,a,133,a,b,154,a)]. given #394 (A,wt=15): 104 (x ; (y ; (z ; y))) ^ <= ((x + z) ; y) ^. [para(24(a,1),37(a,2,1)),rewrite(20(3))]. given #395 (F,wt=13): 1551 -(1 ^ ^ + x ^ <= c6 ; (c4 * ; 0)). [ur(32,a,572,a,c,1536,a)]. given #396 (F,wt=13): 1552 -(x ^ + 1 ^ ^ <= c6 ; (c4 * ; 0)). [ur(32,a,168,a,c,1536,a)]. given #397 (F,wt=13): 1636 -(1 ^ ^ ; 1 ^ <= c5 ; (c4 * ; 0)). [ur(32,a,740,a,c,1537,a)]. given #398 (F,wt=13): 1637 -(1 ^ ^ + x ^ <= c5 ; (c4 * ; 0)). [ur(32,a,572,a,c,1537,a)]. given #399 (T,wt=7): 306 c4 ; c6 * <= 1 *. [hyper(32,a,132,a,b,154,a)]. given #400 (T,wt=7): 308 (c6 ; x) ^ <= x ^. [hyper(36,a,156,a)]. given #401 (T,wt=7): 309 (c6 ; x) * <= x *. [hyper(35,a,156,a)]. given #402 (T,wt=7): 311 c6 ; (x ; c5) <= x. [hyper(32,a,145,a,b,156,a),rewrite(20(4))]. given #403 (A,wt=9): 105 (x ; x *) ^ <= (x *) ^. [para(26(a,1),37(a,2,1)),rewrite(18(4))]. given #404 (F,wt=13): 1638 -(x ^ + 1 ^ ^ <= c5 ; (c4 * ; 0)). [ur(32,a,168,a,c,1537,a)]. given #405 (F,wt=13): 2051 -(1 ^ ; (1 ^ ; 1 ^) <= c4 * ; 0). [ur(32,a,740,a,c,1722,a),rewrite(20(8))]. given #406 (F,wt=13): 2052 -(1 ^ ; 1 ^ + x ^ <= c4 * ; 0). [ur(32,a,572,a,c,1722,a)]. given #407 (F,wt=13): 2053 -(x ^ + 1 ^ ; 1 ^ <= c4 * ; 0). [ur(32,a,168,a,c,1722,a)]. given #408 (T,wt=7): 312 c5 ; (c6 ; x) <= x. [hyper(32,a,144,a,b,156,a)]. given #409 (T,wt=7): 313 c6 ; (x ; c4) <= x. [hyper(32,a,133,a,b,156,a),rewrite(20(4))]. given #410 (T,wt=7): 314 c4 ; (c6 ; x) <= x. [hyper(32,a,132,a,b,156,a)]. given #411 (T,wt=7): 315 c6 ; c6 * <= 1 *. [hyper(32,a,156,a,b,154,a)]. given #412 (A,wt=9): 106 x ^ ^ <= (x + x ^) ^. [para(28(a,1),37(a,1,1))]. given #413 (F,wt=12): 5193 -((1 + 1 ^) ; 1 ^ <= c4 * ; 0). [para(58(a,2),2053(a,1))]. given #414 (F,wt=12): 5703 -((1 + 1 ^) ; 1 ^ <= c5 * ; 0). [ur(32,b,1125,a,c,5193,a)]. given #415 (F,wt=12): 5704 -((1 + 1 ^) ; 1 ^ <= c6 * ; 0). [ur(32,b,1123,a,c,5193,a)]. given #416 (F,wt=13): 2054 -((1 ^ + x ^) ; 1 ^ <= c4 * ; 0). [ur(32,a,740,a,c,1723,a)]. given #417 (T,wt=7): 316 c6 ; (c5 ; x) <= x. [hyper(32,a,156,a,b,144,a)]. given #418 (T,wt=7): 317 c6 ; c5 * <= 1 *. [hyper(32,a,156,a,b,142,a)]. given #419 (T,wt=7): 319 c6 ; (c4 ; x) <= x. [hyper(32,a,156,a,b,132,a)]. given #420 (T,wt=7): 320 c6 ; c4 * <= 1 *. [hyper(32,a,156,a,b,130,a)]. given #421 (A,wt=15): 107 (x ; (y ; z)) ^ ^ <= (x + (y + z)) ^ ^. [hyper(36,a,39,a)]. given #422 (F,wt=13): 2055 -(1 ^ ; (1 ^ + x ^) <= c4 * ; 0). [ur(32,a,728,a,c,1723,a)]. given #423 (F,wt=13): 2056 -(1 ^ + (x ^ + y ^) <= c4 * ; 0). [ur(32,a,572,a,c,1723,a),rewrite(16(6))]. given #424 (F,wt=13): 2057 -(x ^ + (1 ^ + y ^) <= c4 * ; 0). [ur(32,a,168,a,c,1723,a)]. given #425 (F,wt=13): 2058 -((x ^ + 1 ^) ; 1 ^ <= c4 * ; 0). [ur(32,a,740,a,c,1724,a)]. given #426 (T,wt=7): 336 (x ; c6) ^ <= x ^. [hyper(36,a,157,a)]. given #427 (T,wt=7): 337 (x ; c6) * <= x *. [hyper(35,a,157,a)]. given #428 (T,wt=7): 339 c6 ; (x ; c6) <= x. [hyper(32,a,156,a,b,157,a)]. given #429 (T,wt=7): 340 x ; (c6 ; c5) <= x. [hyper(32,a,145,a,b,157,a),rewrite(20(4))]. given #430 (A,wt=15): 108 (x ; (y ; z)) ^ * <= (x + (y + z)) ^ *. [hyper(35,a,39,a)]. given #431 (F,wt=13): 2059 -(1 ^ ; (x ^ + 1 ^) <= c4 * ; 0). [ur(32,a,728,a,c,1724,a)]. given #432 (F,wt=13): 2060 -(x ^ + (y ^ + 1 ^) <= c4 * ; 0). [ur(32,a,168,a,c,1724,a)]. given #433 (F,wt=13): 2148 -(1 ^ ; (1 ^ ; 1 ^) <= c5 * ; 0). [ur(32,a,740,a,c,1725,a),rewrite(20(8))]. given #434 (F,wt=13): 2149 -(1 ^ ; 1 ^ + x ^ <= c5 * ; 0). [ur(32,a,572,a,c,1725,a)]. given #435 (T,wt=7): 341 c5 ; (x ; c6) <= x. [hyper(32,a,144,a,b,157,a)]. given #436 (T,wt=7): 342 x ; (c6 ; c4) <= x. [hyper(32,a,133,a,b,157,a),rewrite(20(4))]. given #437 (T,wt=7): 343 c4 ; (x ; c6) <= x. [hyper(32,a,132,a,b,157,a)]. given #438 (T,wt=7): 344 c6 * ; c6 <= 1 *. [hyper(32,a,157,a,b,154,a)]. given #439 (A,wt=17): 109 (x ; (y ; z)) ^ + u <= (x + (y + z)) ^ + u. [hyper(34,a,39,a)]. given #440 (F,wt=13): 2150 -(x ^ + 1 ^ ; 1 ^ <= c5 * ; 0). [ur(32,a,168,a,c,1725,a)]. given #441 (F,wt=13): 2151 -((1 ^ + x ^) ; 1 ^ <= c5 * ; 0). [ur(32,a,740,a,c,1726,a)]. given #442 (F,wt=13): 2152 -(1 ^ ; (1 ^ + x ^) <= c5 * ; 0). [ur(32,a,728,a,c,1726,a)]. given #443 (F,wt=13): 2153 -(1 ^ + (x ^ + y ^) <= c5 * ; 0). [ur(32,a,572,a,c,1726,a),rewrite(16(6))]. given #444 (T,wt=7): 346 x ; (c5 ; c6) <= x. [hyper(32,a,157,a,b,145,a),rewrite(20(4))]. given #445 (T,wt=7): 347 c5 * ; c6 <= 1 *. [hyper(32,a,157,a,b,142,a)]. given #446 (T,wt=7): 349 x ; (c4 ; c6) <= x. [hyper(32,a,157,a,b,133,a),rewrite(20(4))]. given #447 (T,wt=7): 350 c4 * ; c6 <= 1 *. [hyper(32,a,157,a,b,130,a)]. given #448 (A,wt=17): 110 (x ; (y ; z)) ^ ; u <= (x + (y + z)) ^ ; u. [hyper(33,a,39,a)]. given #449 (F,wt=13): 2154 -(x ^ + (1 ^ + y ^) <= c5 * ; 0). [ur(32,a,168,a,c,1726,a)]. given #450 (F,wt=13): 2155 -((x ^ + 1 ^) ; 1 ^ <= c5 * ; 0). [ur(32,a,740,a,c,1727,a)]. given #451 (F,wt=13): 2156 -(1 ^ ; (x ^ + 1 ^) <= c5 * ; 0). [ur(32,a,728,a,c,1727,a)]. given #452 (F,wt=13): 2157 -(x ^ + (y ^ + 1 ^) <= c5 * ; 0). [ur(32,a,168,a,c,1727,a)]. given #453 (T,wt=7): 365 1 ^ <= (x ^ *) ^. [hyper(36,a,167,a)]. given #454 (T,wt=6): 7523 x <= (y ^ *) ^. [hyper(32,a,1668,a,b,365,a)]. given #455 (T,wt=7): 366 1 * <= x ^ * *. [hyper(35,a,167,a)]. given #456 (T,wt=7): 368 x <= y ^ * ; x. [hyper(33,a,167,a),rewrite(18(2))]. given #457 (A,wt=17): 111 x ; (y ; (z ; u)) ^ <= x ; (y + (z + u)) ^. [hyper(25,a,39,a)]. ============================== PROOF ================================= % Proof 1 at 1.07 (+ 0.02) seconds. % Length of proof is 31. % Level of proof is 5. % Maximum clause weight is 31. % Given clauses 457. 2 x <= y -> z ; x <= z ; y # label(non_clause). [assumption]. 6 x <= y & y <= z -> x <= z # label(non_clause). [assumption]. 11 (all p (p <= 1 & p ; p = p -> p ; (p ; x) ^ = (p ; x) ^)) # label(non_clause). [assumption]. 12 (all p all q all r (p <= 1 & p ; p = p & q <= 1 & q ; q = q & r <= 1 & r ; r = r -> (p ; x ; q ; y ; r ; z) ^ <= p ; (p ; x ; q + q ; y ; r + r ; z) ^)) # label(goal). [goal]. 13 x + y = y + x. [assumption]. 15 x + (y + z) = x + y + z. [assumption]. 16 x + y + z = x + (y + z). [copy(15),flip(a)]. 19 x ; (y ; z) = x ; y ; z. [assumption]. 20 x ; y ; z = x ; (y ; z). [copy(19),flip(a)]. 25 -(x <= y) | z ; x <= z ; y. [clausify(2)]. 31 x <= x. [assumption]. 32 -(x <= y) | -(y <= z) | x <= z. [clausify(6)]. 38 (x ; y ; z) ^ <= (x + y + z) ^. [assumption]. 39 (x ; (y ; z)) ^ <= (x + (y + z)) ^. [copy(38),rewrite(20(2),16(5))]. 40 -(x <= 1) | x ; x != x | (x ; y) ^ = x ; (x ; y) ^. [clausify(11)]. 41 -(x <= 1) | x ; x != x | x ; (x ; y) ^ = (x ; y) ^. [copy(40),flip(c)]. 42 c4 <= 1. [deny(12)]. 43 c4 ; c4 = c4. [deny(12)]. 45 c5 ; c5 = c5. [deny(12)]. 47 c6 ; c6 = c6. [deny(12)]. 48 -((c4 ; c1 ; c5 ; c2 ; c6 ; c3) ^ <= c4 ; (c4 ; c1 ; c5 + c5 ; c2 ; c6 + c6 ; c3) ^). [deny(12)]. 49 -((c4 ; (c1 ; (c5 ; (c2 ; (c6 ; c3))))) ^ <= c4 ; (c6 ; c3 + (c4 ; (c1 ; c5) + c5 ; (c2 ; c6))) ^). [copy(48),rewrite(20(5),20(7),20(6),20(9),20(8),20(7),20(11),20(10),20(9),20(8),20(18),20(23),13(28))]. 51 x + (y + z) = z + (x + y). [para(16(a,1),13(a,1))]. 52 x + (y + z) = y + (x + z). [para(13(a,1),16(a,1,1)),rewrite(16(2))]. 53 -((c4 ; (c1 ; (c5 ; (c2 ; (c6 ; c3))))) ^ <= c4 ; (c4 ; (c1 ; c5) + (c5 ; (c2 ; c6) + c6 ; c3)) ^). [back_rewrite(49),rewrite(51(28),13(27),52(28))]. 111 x ; (y ; (z ; u)) ^ <= x ; (y + (z + u)) ^. [hyper(25,a,39,a)]. 134 c4 ; (c4 ; x) ^ = (c4 ; x) ^. [hyper(41,a,42,a,b,43,a)]. 147 c5 ; (c5 ; x) = c5 ; x. [para(45(a,1),20(a,1,1)),flip(a)]. 159 c6 ; (c6 ; x) = c6 ; x. [para(47(a,1),20(a,1,1)),flip(a)]. 8017 -((c4 ; (c1 ; (c5 ; (c2 ; (c6 ; c3))))) ^ <= (c4 ; (c1 ; (c5 ; (c2 ; (c6 ; c3))))) ^). [ur(32,b,111,a,c,53,a),rewrite(20(27),20(26),159(25),20(26),20(25),147(24),134(26))]. 8018 $F. [resolve(8017,a,31,a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=457. Generated=20518. Kept=7999. proofs=1. Usable=425. Sos=7106. Demods=146. Limbo=50, Disabled=448. Hints=0. Weight_deleted=0. Literals_deleted=0. Forward_subsumed=12519. Back_subsumed=377. Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. New_demodulators=156 (8 lex), Back_demodulated=39. Back_unit_deleted=0. Demod_attempts=296544. Demod_rewrites=17853. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=5041. Nonunit_bsub_feature_tests=2366. Megabytes=6.55. User_CPU=1.07, System_CPU=0.02, Wall_clock=1. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED Exiting with 1 proof. Process 6906 exit (max_proofs) Mon Oct 1 08:01:51 2007