============================== Prover9 =============================== Prover9 (32) version Dec-2007, Dec 2007. Process 6769 was started by peterhoefner on callisto.dynhost.nicta.com.au, Fri Mar 27 10:49:16 2015 The command was "prover9 -f Prover9Theorem3.4.in". ============================== end of head =========================== ============================== INPUT ================================= % Reading from file Prover9Theorem3.4.in op(500,infix,"\/"). op(500,infix,"/\"). op(300,postfix,"'"). op(450,infix,"*"). op(300,postfix,"^"). if(Prover9). % Conditional input included. assign(max_seconds,3000). end_if. if(Mace4). % Conditional input omitted. end_if. formulas(assumptions). x \/ y = y \/ x. x /\ y = y /\ x. x \/ (y \/ z) = (x \/ y) \/ z. x /\ (y /\ z) = (x /\ y) /\ z. x \/ (y /\ x) = x. x /\ (y \/ x) = x. x <= y <-> x \/ y = y. x <= y <-> x /\ y = x. x /\ (y \/ z) = (x /\ y) \/ (x /\ z). x \/ (y /\ z) = (x \/ y) /\ (x \/ z). L = x \/ x'. O = x /\ x'. x * (y * z) = (x * y) * z. x * I = x. I * x = x. x * y /\ z <= (x /\ z * y ^) * (y /\ x ^ * z). x * y <= z <-> x ^ * z' <= y'. x * y <= z <-> z' * y ^ <= x'. x != O <-> (L * x) * L = L. (x \/ y) * z = x * z \/ y * z. z * (x \/ y) = z * x \/ z * y. (x * y) ^ = y ^ * x ^. (x \/ y) ^ = x ^ \/ y ^. (x /\ y) ^ = x ^ /\ y ^. x <= y -> x * z <= y * z. x <= y -> z * x <= z * y. x <= y -> x \/ z <= y \/ z. x <= y -> x /\ z <= y /\ z. x ^ ^ = x. O <= x. x <= L. O * x = O. x * O = O. point(x) <-> x * L = x & L * x = L & x * x ^ <= I. irreflexive(x) <-> x <= I'. symmetric(x) <-> x = x ^. univalent(x) <-> x ^ * x <= I. coloringProperty(x,z) <-> x * x ^ <= z'. end_of_list. formulas(goals). (all p all q (x * L != L & point(p) & point(q) & p <= (x * L)' -> x <= x \/ p * q ^ & x != x \/ p * q ^)). end_of_list. ============================== end of input ========================== ============================== PROCESS NON-CLAUSAL FORMULAS ========== % Formulas that are not ordinary clauses: 1 x <= y <-> x \/ y = y # label(non_clause). [assumption]. 2 x <= y <-> x /\ y = x # label(non_clause). [assumption]. 3 x * y <= z <-> x ^ * z' <= y' # label(non_clause). [assumption]. 4 x * y <= z <-> z' * y ^ <= x' # label(non_clause). [assumption]. 5 x != O <-> (L * x) * L = L # label(non_clause). [assumption]. 6 x <= y -> x * z <= y * z # label(non_clause). [assumption]. 7 x <= y -> z * x <= z * y # label(non_clause). [assumption]. 8 x <= y -> x \/ z <= y \/ z # label(non_clause). [assumption]. 9 x <= y -> x /\ z <= y /\ z # label(non_clause). [assumption]. 10 point(x) <-> x * L = x & L * x = L & x * x ^ <= I # label(non_clause). [assumption]. 11 irreflexive(x) <-> x <= I' # label(non_clause). [assumption]. 12 symmetric(x) <-> x = x ^ # label(non_clause). [assumption]. 13 univalent(x) <-> x ^ * x <= I # label(non_clause). [assumption]. 14 coloringProperty(x,z) <-> x * x ^ <= z' # label(non_clause). [assumption]. 15 (all p all q (x * L != L & point(p) & point(q) & p <= (x * L)' -> x <= x \/ p * q ^ & x != x \/ p * q ^)) # label(non_clause) # 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 /\ y = y /\ x. [assumption]. x \/ (y \/ z) = (x \/ y) \/ z. [assumption]. x /\ (y /\ z) = (x /\ y) /\ z. [assumption]. x \/ (y /\ x) = x. [assumption]. x /\ (y \/ x) = x. [assumption]. -(x <= y) | x \/ y = y. [clausify(1)]. x <= y | x \/ y != y. [clausify(1)]. -(x <= y) | x /\ y = x. [clausify(2)]. x <= y | x /\ y != x. [clausify(2)]. x /\ (y \/ z) = (x /\ y) \/ (x /\ z). [assumption]. x \/ (y /\ z) = (x \/ y) /\ (x \/ z). [assumption]. L = x \/ x'. [assumption]. O = x /\ x'. [assumption]. x * (y * z) = (x * y) * z. [assumption]. x * I = x. [assumption]. I * x = x. [assumption]. x * y /\ z <= (x /\ z * y ^) * (y /\ x ^ * z). [assumption]. -(x * y <= z) | x ^ * z' <= y'. [clausify(3)]. x * y <= z | -(x ^ * z' <= y'). [clausify(3)]. -(x * y <= z) | z' * y ^ <= x'. [clausify(4)]. x * y <= z | -(z' * y ^ <= x'). [clausify(4)]. O = x | (L * x) * L = L. [clausify(5)]. O != x | (L * x) * L != L. [clausify(5)]. (x \/ y) * z = x * z \/ y * z. [assumption]. x * (y \/ z) = x * y \/ x * z. [assumption]. (x * y) ^ = y ^ * x ^. [assumption]. (x \/ y) ^ = x ^ \/ y ^. [assumption]. (x /\ y) ^ = x ^ /\ y ^. [assumption]. -(x <= y) | x * z <= y * z. [clausify(6)]. -(x <= y) | z * x <= z * y. [clausify(7)]. -(x <= y) | x \/ z <= y \/ z. [clausify(8)]. -(x <= y) | x /\ z <= y /\ z. [clausify(9)]. x ^ ^ = x. [assumption]. O <= x. [assumption]. x <= L. [assumption]. O * x = O. [assumption]. x * O = O. [assumption]. -point(x) | x * L = x. [clausify(10)]. -point(x) | L * x = L. [clausify(10)]. -point(x) | x * x ^ <= I. [clausify(10)]. point(x) | x * L != x | L * x != L | -(x * x ^ <= I). [clausify(10)]. -irreflexive(x) | x <= I'. [clausify(11)]. irreflexive(x) | -(x <= I'). [clausify(11)]. -symmetric(x) | x ^ = x. [clausify(12)]. symmetric(x) | x ^ != x. [clausify(12)]. -univalent(x) | x ^ * x <= I. [clausify(13)]. univalent(x) | -(x ^ * x <= I). [clausify(13)]. -coloringProperty(x,y) | x * x ^ <= y'. [clausify(14)]. coloringProperty(x,y) | -(x * x ^ <= y'). [clausify(14)]. c1 * L != L. [deny(15)]. point(c2). [deny(15)]. point(c3). [deny(15)]. c2 <= (c1 * L)'. [deny(15)]. -(c1 <= c1 \/ c2 * c3 ^) | c1 \/ c2 * c3 ^ = c1. [deny(15)]. end_of_list. formulas(demodulators). end_of_list. ============================== PREDICATE ELIMINATION ================= Eliminating point/1 16 point(x) | x * L != x | L * x != L | -(x * x ^ <= I). [clausify(10)]. 17 -point(x) | x * L = x. [clausify(10)]. 18 -point(x) | L * x = L. [clausify(10)]. 19 -point(x) | x * x ^ <= I. [clausify(10)]. 20 point(c2). [deny(15)]. Derived: c2 * L = c2. [resolve(20,a,17,a)]. Derived: L * c2 = L. [resolve(20,a,18,a)]. Derived: c2 * c2 ^ <= I. [resolve(20,a,19,a)]. 21 point(c3). [deny(15)]. Derived: c3 * L = c3. [resolve(21,a,17,a)]. Derived: L * c3 = L. [resolve(21,a,18,a)]. Derived: c3 * c3 ^ <= I. [resolve(21,a,19,a)]. Eliminating irreflexive/1 22 irreflexive(x) | -(x <= I'). [clausify(11)]. 23 -irreflexive(x) | x <= I'. [clausify(11)]. Eliminating symmetric/1 24 symmetric(x) | x ^ != x. [clausify(12)]. 25 -symmetric(x) | x ^ = x. [clausify(12)]. Eliminating univalent/1 26 univalent(x) | -(x ^ * x <= I). [clausify(13)]. 27 -univalent(x) | x ^ * x <= I. [clausify(13)]. Eliminating coloringProperty/2 28 coloringProperty(x,y) | -(x * x ^ <= y'). [clausify(14)]. 29 -coloringProperty(x,y) | x * x ^ <= y'. [clausify(14)]. ============================== end predicate elimination ============= Auto_denials: (non-Horn, no changes). Term ordering decisions: Predicate symbol precedence: predicate_order([ =, <= ]). Function symbol precedence: function_order([ L, O, I, c1, c2, c3, *, \/, /\, ^, ' ]). After inverse_order: Function symbol precedence: function_order([ L, O, I, c1, c2, c3, \/, /\, ', *, ^ ]). Unfolding symbols: (none). Auto_inference settings: % set(paramodulation). % (positive equality literals) % set(binary_resolution). % (non-Horn) % set(neg_ur_resolution). % (non-Horn, less than 100 clauses) Auto_process settings: % set(factor). % (non-Horn) % set(unit_deletion). % (non-Horn) % Operation \/ is commutative; C redundancy checks enabled. % 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). 30 x \/ y = y \/ x. [assumption]. 31 x /\ y = y /\ x. [assumption]. 33 (x \/ y) \/ z = x \/ (y \/ z). [copy(32),flip(a)]. 35 (x /\ y) /\ z = x /\ (y /\ z). [copy(34),flip(a)]. 36 x \/ (y /\ x) = x. [assumption]. 38 -(x <= y) | x \/ y = y. [clausify(1)]. 39 x <= y | x \/ y != y. [clausify(1)]. 40 -(x <= y) | x /\ y = x. [clausify(2)]. 41 x <= y | x /\ y != x. [clausify(2)]. 42 x /\ (y \/ z) = (x /\ y) \/ (x /\ z). [assumption]. 44 (x /\ x) \/ ((x /\ y) \/ ((x \/ y) /\ z)) = x \/ (y /\ z). [copy(43),rewrite([42(5),31(4),42(4),33(8)]),flip(a)]. 46 x \/ x' = L. [copy(45),flip(a)]. 48 x /\ x' = O. [copy(47),flip(a)]. 50 (x * y) * z = x * (y * z). [copy(49),flip(a)]. 51 x * I = x. [assumption]. 52 I * x = x. [assumption]. 53 x * y /\ z <= (x /\ z * y ^) * (y /\ x ^ * z). [assumption]. 54 -(x * y <= z) | x ^ * z' <= y'. [clausify(3)]. 55 x * y <= z | -(x ^ * z' <= y'). [clausify(3)]. 56 -(x * y <= z) | z' * y ^ <= x'. [clausify(4)]. 57 x * y <= z | -(z' * y ^ <= x'). [clausify(4)]. 59 O = x | L * (x * L) = L. [copy(58),rewrite([50(6)])]. 61 O != x | L * (x * L) != L. [copy(60),rewrite([50(6)])]. 62 (x \/ y) * z = x * z \/ y * z. [assumption]. 63 x * (y \/ z) = x * y \/ x * z. [assumption]. 64 (x * y) ^ = y ^ * x ^. [assumption]. 65 (x \/ y) ^ = x ^ \/ y ^. [assumption]. 66 (x /\ y) ^ = x ^ /\ y ^. [assumption]. 67 -(x <= y) | x * z <= y * z. [clausify(6)]. 68 -(x <= y) | z * x <= z * y. [clausify(7)]. 69 -(x <= y) | x \/ z <= y \/ z. [clausify(8)]. 70 -(x <= y) | x /\ z <= y /\ z. [clausify(9)]. 71 x ^ ^ = x. [assumption]. 72 O <= x. [assumption]. 73 x <= L. [assumption]. 74 O * x = O. [assumption]. 75 x * O = O. [assumption]. 76 c1 * L != L. [deny(15)]. 77 c2 <= (c1 * L)'. [deny(15)]. 78 -(c1 <= c1 \/ c2 * c3 ^) | c1 \/ c2 * c3 ^ = c1. [deny(15)]. 79 c2 * L = c2. [resolve(20,a,17,a)]. 80 L * c2 = L. [resolve(20,a,18,a)]. 81 c2 * c2 ^ <= I. [resolve(20,a,19,a)]. 82 c3 * L = c3. [resolve(21,a,17,a)]. 83 L * c3 = L. [resolve(21,a,18,a)]. 84 c3 * c3 ^ <= I. [resolve(21,a,19,a)]. 85 (x /\ y) \/ (x /\ x) = x. [back_rewrite(37),rewrite([42(2)])]. end_of_list. formulas(demodulators). 30 x \/ y = y \/ x. [assumption]. % (lex-dep) 31 x /\ y = y /\ x. [assumption]. % (lex-dep) 33 (x \/ y) \/ z = x \/ (y \/ z). [copy(32),flip(a)]. 35 (x /\ y) /\ z = x /\ (y /\ z). [copy(34),flip(a)]. 36 x \/ (y /\ x) = x. [assumption]. 42 x /\ (y \/ z) = (x /\ y) \/ (x /\ z). [assumption]. 44 (x /\ x) \/ ((x /\ y) \/ ((x \/ y) /\ z)) = x \/ (y /\ z). [copy(43),rewrite([42(5),31(4),42(4),33(8)]),flip(a)]. 46 x \/ x' = L. [copy(45),flip(a)]. 48 x /\ x' = O. [copy(47),flip(a)]. 50 (x * y) * z = x * (y * z). [copy(49),flip(a)]. 51 x * I = x. [assumption]. 52 I * x = x. [assumption]. 62 (x \/ y) * z = x * z \/ y * z. [assumption]. 63 x * (y \/ z) = x * y \/ x * z. [assumption]. 64 (x * y) ^ = y ^ * x ^. [assumption]. 65 (x \/ y) ^ = x ^ \/ y ^. [assumption]. 66 (x /\ y) ^ = x ^ /\ y ^. [assumption]. 71 x ^ ^ = x. [assumption]. 74 O * x = O. [assumption]. 75 x * O = O. [assumption]. 79 c2 * L = c2. [resolve(20,a,17,a)]. 80 L * c2 = L. [resolve(20,a,18,a)]. 82 c3 * L = c3. [resolve(21,a,17,a)]. 83 L * c3 = L. [resolve(21,a,18,a)]. 85 (x /\ y) \/ (x /\ x) = x. [back_rewrite(37),rewrite([42(2)])]. end_of_list. ============================== end of clauses for search ============= ============================== SEARCH ================================ % Starting search at 0.01 seconds. given #1 (I,wt=7): 30 x \/ y = y \/ x. [assumption]. given #2 (I,wt=7): 31 x /\ y = y /\ x. [assumption]. given #3 (I,wt=11): 33 (x \/ y) \/ z = x \/ (y \/ z). [copy(32),flip(a)]. % Operation \/ is associative-commutative; CAC redundancy checks enabled. % back CAC tautology: 86 x \/ (y \/ z) = z \/ (x \/ y). [para(33(a,1),30(a,1))]. given #4 (I,wt=11): 35 (x /\ y) /\ z = x /\ (y /\ z). [copy(34),flip(a)]. % Operation /\ is associative-commutative; CAC redundancy checks enabled. % back CAC tautology: 88 x /\ (y /\ z) = z /\ (x /\ y). [para(35(a,1),31(a,1))]. given #5 (I,wt=7): 36 x \/ (y /\ x) = x. [assumption]. given #6 (I,wt=8): 38 -(x <= y) | x \/ y = y. [clausify(1)]. given #7 (I,wt=8): 39 x <= y | x \/ y != y. [clausify(1)]. given #8 (I,wt=8): 40 -(x <= y) | x /\ y = x. [clausify(2)]. given #9 (I,wt=8): 41 x <= y | x /\ y != x. [clausify(2)]. given #10 (I,wt=13): 42 x /\ (y \/ z) = (x /\ y) \/ (x /\ z). [assumption]. given #11 (I,wt=19): 44 (x /\ x) \/ ((x /\ y) \/ ((x \/ y) /\ z)) = x \/ (y /\ z). [copy(43),rewrite([42(5),31(4),42(4),33(8)]),flip(a)]. given #12 (I,wt=6): 46 x \/ x' = L. [copy(45),flip(a)]. given #13 (I,wt=6): 48 x /\ x' = O. [copy(47),flip(a)]. given #14 (I,wt=11): 50 (x * y) * z = x * (y * z). [copy(49),flip(a)]. given #15 (I,wt=5): 51 x * I = x. [assumption]. given #16 (I,wt=5): 52 I * x = x. [assumption]. given #17 (I,wt=19): 53 x * y /\ z <= (x /\ z * y ^) * (y /\ x ^ * z). [assumption]. given #18 (I,wt=13): 54 -(x * y <= z) | x ^ * z' <= y'. [clausify(3)]. given #19 (I,wt=13): 55 x * y <= z | -(x ^ * z' <= y'). [clausify(3)]. given #20 (I,wt=13): 56 -(x * y <= z) | z' * y ^ <= x'. [clausify(4)]. given #21 (I,wt=13): 57 x * y <= z | -(z' * y ^ <= x'). [clausify(4)]. given #22 (I,wt=10): 59 O = x | L * (x * L) = L. [copy(58),rewrite([50(6)])]. given #23 (I,wt=10): 61 O != x | L * (x * L) != L. [copy(60),rewrite([50(6)])]. given #24 (I,wt=13): 62 (x \/ y) * z = x * z \/ y * z. [assumption]. given #25 (I,wt=13): 63 x * (y \/ z) = x * y \/ x * z. [assumption]. given #26 (I,wt=10): 64 (x * y) ^ = y ^ * x ^. [assumption]. given #27 (I,wt=10): 65 (x \/ y) ^ = x ^ \/ y ^. [assumption]. given #28 (I,wt=10): 66 (x /\ y) ^ = x ^ /\ y ^. [assumption]. given #29 (I,wt=10): 67 -(x <= y) | x * z <= y * z. [clausify(6)]. given #30 (I,wt=10): 68 -(x <= y) | z * x <= z * y. [clausify(7)]. given #31 (I,wt=10): 69 -(x <= y) | x \/ z <= y \/ z. [clausify(8)]. given #32 (I,wt=10): 70 -(x <= y) | x /\ z <= y /\ z. [clausify(9)]. given #33 (I,wt=5): 71 x ^ ^ = x. [assumption]. given #34 (I,wt=3): 72 O <= x. [assumption]. given #35 (I,wt=3): 73 x <= L. [assumption]. given #36 (I,wt=5): 74 O * x = O. [assumption]. given #37 (I,wt=5): 75 x * O = O. [assumption]. given #38 (I,wt=5): 76 c1 * L != L. [deny(15)]. given #39 (I,wt=6): 77 c2 <= (c1 * L)'. [deny(15)]. given #40 (I,wt=16): 78 -(c1 <= c1 \/ c2 * c3 ^) | c1 \/ c2 * c3 ^ = c1. [deny(15)]. given #41 (I,wt=5): 79 c2 * L = c2. [resolve(20,a,17,a)]. given #42 (I,wt=5): 80 L * c2 = L. [resolve(20,a,18,a)]. given #43 (I,wt=6): 81 c2 * c2 ^ <= I. [resolve(20,a,19,a)]. given #44 (I,wt=5): 82 c3 * L = c3. [resolve(21,a,17,a)]. given #45 (I,wt=5): 83 L * c3 = L. [resolve(21,a,18,a)]. given #46 (I,wt=6): 84 c3 * c3 ^ <= I. [resolve(21,a,19,a)]. given #47 (I,wt=9): 85 (x /\ y) \/ (x /\ x) = x. [back_rewrite(37),rewrite([42(2)])]. given #48 (A,wt=11): 87 x \/ (y \/ z) = y \/ (x \/ z). [para(30(a,1),33(a,1,1)),rewrite([33(2)])]. given #49 (F,wt=3): 153 O != L. [ur(61,a,52,a(flip)),rewrite([75(4),74(4),75(3)])]. given #50 (F,wt=3): 227 c2 != O. [para(79(a,1),61(b,1,2)),rewrite([80(6)]),flip(a),xx(b)]. given #51 (F,wt=3): 248 c3 != O. [para(82(a,1),61(b,1,2)),rewrite([83(6)]),flip(a),xx(b)]. given #52 (F,wt=8): 155 I != O | L * L != L. [para(52(a,1),61(b,1,2)),flip(a)]. given #53 (T,wt=5): 196 O /\ x = O. [resolve(72,a,40,a)]. given #54 (T,wt=5): 197 O \/ x = x. [resolve(72,a,38,a)]. given #55 (T,wt=4): 299 O' = L. [para(197(a,1),46(a,1))]. given #56 (T,wt=5): 199 x <= y \/ x. [back_rewrite(195),rewrite([197(2)])]. given #57 (A,wt=11): 89 x /\ (y /\ z) = y /\ (x /\ z). [para(31(a,1),35(a,1,1)),rewrite([35(2)])]. given #58 (F,wt=14): 154 x * y != O | L * (x * (y * L)) != L. [para(50(a,1),61(b,1,2)),flip(a)]. given #59 (F,wt=12): 320 x * c2 != O | L * (x * c2) != L. [para(79(a,1),154(b,1,2,2))]. given #60 (F,wt=12): 321 x * c3 != O | L * (x * c3) != L. [para(82(a,1),154(b,1,2,2))]. given #61 (F,wt=16): 322 x * (y * c2) != O | L * (x * (y * c2)) != L. [para(50(a,1),320(b,1,2)),rewrite([50(3)])]. given #62 (T,wt=3): 311 x <= x. [para(197(a,1),199(a,2))]. given #63 (T,wt=5): 208 x /\ L = x. [resolve(73,a,40,a)]. given #64 (T,wt=5): 209 x \/ L = L. [resolve(73,a,38,a)]. given #65 (T,wt=5): 272 x /\ x = x. [para(48(a,1),85(a,1,1)),rewrite([197(3)])]. given #66 (A,wt=7): 90 x \/ (x /\ y) = x. [para(31(a,1),36(a,1,2))]. given #67 (F,wt=12): 329 x * L != O | L * (x * L) != L. [para(80(a,1),322(b,1,2,2)),rewrite([80(3)])]. given #68 (F,wt=16): 324 x * (y * c3) != O | L * (x * (y * c3)) != L. [para(50(a,1),321(b,1,2)),rewrite([50(3)])]. given #69 (F,wt=16): 361 x * (y * L) != O | L * (x * (y * L)) != L. [para(50(a,1),329(b,1,2)),rewrite([50(3)])]. given #70 (F,wt=18): 165 x \/ y != O | L * (x * L) \/ L * (y * L) != L. [para(62(a,1),61(b,1,2)),rewrite([63(10)]),flip(a)]. given #71 (T,wt=5): 276 x \/ x = x. [back_rewrite(111),rewrite([272(1),272(2),90(3),30(2),90(2)])]. given #72 (T,wt=5): 279 x /\ y <= x. [back_rewrite(269),rewrite([272(2),272(3)]),xx(b)]. given #73 (T,wt=5): 296 x /\ O = O. [para(196(a,1),31(a,1)),flip(a)]. given #74 (T,wt=5): 297 x \/ O = x. [para(196(a,1),36(a,1,2))]. given #75 (A,wt=11): 91 x \/ ((y /\ x) \/ z) = x \/ z. [para(36(a,1),33(a,1,1)),flip(a)]. given #76 (F,wt=5): 378 c2 \/ x != O. [para(79(a,1),165(b,1,1,2)),rewrite([80(7),333(10)]),xx(b)]. given #77 (F,wt=3): 403 -(c2 <= O). [ur(38,b,378,a)]. given #78 (F,wt=5): 379 x \/ c2 != O. [para(79(a,1),165(b,1,2,2)),rewrite([80(11),30(10),333(10)]),xx(b)]. given #79 (F,wt=5): 380 c3 \/ x != O. [para(82(a,1),165(b,1,1,2)),rewrite([83(7),333(10)]),xx(b)]. given #80 (T,wt=5): 307 x <= x \/ y. [para(30(a,1),199(a,2))]. given #81 (T,wt=5): 309 x /\ y <= y. [para(36(a,1),199(a,2))]. given #82 (T,wt=5): 332 L /\ x = x. [para(208(a,1),31(a,1)),flip(a)]. given #83 (T,wt=4): 418 L' = O. [para(332(a,1),48(a,1))]. given #84 (A,wt=9): 93 x \/ (y /\ (z /\ x)) = x. [para(35(a,1),36(a,1,2))]. given #85 (F,wt=3): 406 -(c3 <= O). [ur(38,b,380,a)]. given #86 (F,wt=5): 381 x \/ c3 != O. [para(82(a,1),165(b,1,2,2)),rewrite([83(11),30(10),333(10)]),xx(b)]. given #87 (F,wt=7): 404 x \/ (c2 \/ y) != O. [para(87(a,1),378(a,1))]. given #88 (F,wt=7): 405 x \/ (y \/ c2) != O. [para(33(a,1),379(a,1))]. given #89 (T,wt=5): 333 L \/ x = L. [para(208(a,1),36(a,1,2))]. given #90 (T,wt=6): 390 x <= O | O != x. [para(296(a,1),41(b,1))]. given #91 (T,wt=6): 417 L <= x | L != x. [para(332(a,1),41(b,1)),flip(b)]. given #92 (T,wt=7): 125 x <= x' | O != x. [para(48(a,1),41(b,1))]. given #93 (A,wt=8): 94 x <= y | y \/ x != y. [para(30(a,1),39(b,1))]. given #94 (F,wt=7): 407 x \/ (c3 \/ y) != O. [para(87(a,1),380(a,1))]. given #95 (F,wt=7): 437 x \/ (y \/ c3) != O. [para(33(a,1),381(a,1))]. given #96 (F,wt=9): 438 x \/ (y \/ (c2 \/ z)) != O. [para(33(a,1),404(a,1))]. given #97 (F,wt=9): 439 x \/ (y \/ (z \/ c2)) != O. [para(33(a,1),405(a,1,2))]. given #98 (T,wt=7): 204 x * y <= x * L. [resolve(73,a,68,a)]. given #99 (T,wt=5): 461 x <= x * L. [para(51(a,1),204(a,1))]. given #100 (T,wt=5): 464 c2 * x <= c2. [para(79(a,1),204(a,2))]. given #101 (T,wt=5): 465 c3 * x <= c3. [para(82(a,1),204(a,2))]. given #102 (A,wt=12): 95 x \/ y <= z | x \/ (y \/ z) != z. [para(33(a,1),39(b,1))]. given #103 (F,wt=9): 450 x \/ (y \/ (c3 \/ z)) != O. [para(33(a,1),407(a,1))]. given #104 (F,wt=9): 451 x \/ (y \/ (z \/ c3)) != O. [para(33(a,1),437(a,1,2))]. given #105 (F,wt=10): 443 x \/ I != O | L * L != L. [back_rewrite(374),rewrite([441(12)])]. given #106 (F,wt=10): 444 I \/ x != O | L * L != L. [back_rewrite(373),rewrite([441(12)])]. given #107 (T,wt=7): 205 x * y <= L * y. [resolve(73,a,67,a)]. given #108 (T,wt=5): 512 x <= L * x. [para(52(a,1),205(a,1))]. given #109 (T,wt=5): 515 c2 <= L * L. [para(79(a,1),205(a,1))]. given #110 (T,wt=5): 516 c3 <= L * L. [para(82(a,1),205(a,1))]. given #111 (A,wt=10): 96 x <= y /\ x | y /\ x != x. [para(36(a,1),39(b,1)),flip(b)]. given #112 (F,wt=11): 452 x \/ (y \/ (z \/ (c2 \/ u))) != O. [para(33(a,1),438(a,1,2))]. given #113 (F,wt=11): 453 x \/ (y \/ (z \/ (u \/ c2))) != O. [para(33(a,1),439(a,1,2,2))]. given #114 (F,wt=11): 502 x \/ (y \/ (z \/ (c3 \/ u))) != O. [para(33(a,1),450(a,1,2))]. given #115 (F,wt=11): 503 x \/ (y \/ (z \/ (u \/ c3))) != O. [para(33(a,1),451(a,1,2,2))]. given #116 (T,wt=7): 228 c2 \/ c2 * x = c2. [para(79(a,1),63(a,2,2)),rewrite([209(3),79(3),30(5)]),flip(a)]. given #117 (T,wt=7): 240 I' * c2 <= c2'. [resolve(81,a,56,a),rewrite([71(5)])]. given #118 (T,wt=7): 249 c3 \/ c3 * x = c3. [para(82(a,1),63(a,2,2)),rewrite([209(3),82(3),30(5)]),flip(a)]. given #119 (T,wt=7): 261 I' * c3 <= c3'. [resolve(84,a,56,a),rewrite([71(5)])]. given #120 (A,wt=8): 97 x <= y | y /\ x != x. [para(31(a,1),41(b,1))]. given #121 (F,wt=12): 504 x \/ (y \/ I) != O | L * L != L. [para(33(a,1),443(a,1))]. given #122 (F,wt=12): 505 x \/ (I \/ y) != O | L * L != L. [para(87(a,1),444(a,1))]. given #123 (F,wt=13): 540 x \/ (y \/ (z \/ (u \/ (c2 \/ w)))) != O. [para(33(a,1),452(a,1,2,2))]. given #124 (F,wt=13): 541 x \/ (y \/ (z \/ (u \/ (w \/ c2)))) != O. [para(33(a,1),453(a,1,2,2,2))]. given #125 (T,wt=7): 308 x <= y \/ (z \/ x). [para(33(a,1),199(a,2))]. given #126 (T,wt=7): 389 x /\ (y /\ z) <= y. [para(89(a,1),279(a,1))]. given #127 (T,wt=7): 412 x <= y \/ (x \/ z). [para(87(a,1),307(a,2))]. given #128 (T,wt=7): 415 x /\ (y /\ z) <= z. [para(35(a,1),309(a,1))]. given #129 (A,wt=14): 98 x /\ y <= z | x /\ (y /\ z) != x /\ y. [para(35(a,1),41(b,1))]. given #130 (F,wt=13): 542 x \/ (y \/ (z \/ (u \/ (c3 \/ w)))) != O. [para(33(a,1),502(a,1,2,2))]. given #131 (F,wt=13): 543 x \/ (y \/ (z \/ (u \/ (w \/ c3)))) != O. [para(33(a,1),503(a,1,2,2,2))]. given #132 (F,wt=14): 580 x \/ (y \/ (z \/ I)) != O | L * L != L. [para(33(a,1),504(a,1,2))]. given #133 (F,wt=14): 581 x \/ (y \/ (I \/ z)) != O | L * L != L. [para(33(a,1),505(a,1))]. given #134 (T,wt=7): 447 x' <= x | L != x. [para(46(a,1),94(b,1))]. given #135 (T,wt=7): 472 x /\ x * L = x. [resolve(461,a,40,a)]. given #136 (T,wt=5): 640 L * L = L. [para(472(a,1),332(a,1)),flip(a)]. given #137 (T,wt=7): 521 x /\ L * x = x. [resolve(512,a,40,a)]. given #138 (A,wt=13): 99 (x \/ y) /\ z = (z /\ x) \/ (z /\ y). [para(42(a,1),31(a,1)),flip(a)]. given #139 (F,wt=3): 654 I != O. [back_rewrite(155),rewrite([640(6)]),xx(b)]. given #140 (F,wt=5): 650 I \/ x != O. [back_rewrite(444),rewrite([640(7)]),xx(b)]. given #141 (F,wt=3): 703 -(I <= O). [ur(38,b,650,a)]. given #142 (F,wt=5): 651 x \/ I != O. [back_rewrite(443),rewrite([640(7)]),xx(b)]. given #143 (T,wt=7): 589 x /\ y <= z \/ y. [para(36(a,1),308(a,2,2))]. given #144 (T,wt=7): 591 x /\ y <= z \/ x. [para(90(a,1),308(a,2,2))]. given #145 (T,wt=7): 594 c2 * x <= y \/ c2. [para(228(a,1),308(a,2,2))]. given #146 (T,wt=7): 595 c3 * x <= y \/ c3. [para(249(a,1),308(a,2,2))]. given #147 (A,wt=17): 100 ((x /\ y) \/ (x /\ z)) /\ u = x /\ ((y \/ z) /\ u). [para(42(a,1),35(a,1,1))]. given #148 (F,wt=7): 648 x \/ (I \/ y) != O. [back_rewrite(505),rewrite([640(8)]),xx(b)]. given #149 (F,wt=7): 649 x \/ (y \/ I) != O. [back_rewrite(504),rewrite([640(8)]),xx(b)]. given #150 (F,wt=9): 646 x \/ (y \/ (I \/ z)) != O. [back_rewrite(581),rewrite([640(9)]),xx(b)]. given #151 (F,wt=9): 647 x \/ (y \/ (z \/ I)) != O. [back_rewrite(580),rewrite([640(9)]),xx(b)]. given #152 (T,wt=7): 610 x /\ y <= y \/ z. [para(91(a,1),412(a,2))]. given #153 (T,wt=7): 643 x /\ y <= y * L. [para(472(a,1),415(a,1,2))]. given #154 (T,wt=7): 669 x /\ y <= L * y. [para(521(a,1),415(a,1,2))]. given #155 (T,wt=7): 713 x /\ c2 * y <= c2. [para(228(a,1),589(a,2))]. given #156 (A,wt=13): 101 (x /\ y) \/ (x /\ (z /\ y)) = x /\ y. [para(36(a,1),42(a,1,2)),flip(a)]. given #157 (F,wt=11): 644 x \/ (y \/ (z \/ (I \/ u))) != O. [back_rewrite(630),rewrite([640(10)]),xx(b)]. given #158 (F,wt=11): 645 x \/ (y \/ (z \/ (u \/ I))) != O. [back_rewrite(629),rewrite([640(10)]),xx(b)]. given #159 (F,wt=13): 868 x \/ (y \/ (z \/ (u \/ (I \/ w)))) != O. [para(33(a,1),644(a,1,2,2))]. given #160 (F,wt=13): 869 x \/ (y \/ (z \/ (u \/ (w \/ I)))) != O. [para(33(a,1),645(a,1,2,2,2))]. given #161 (T,wt=7): 714 x /\ c3 * y <= c3. [para(249(a,1),589(a,2))]. given #162 (T,wt=7): 715 x <= y \/ x * L. [para(472(a,1),589(a,1))]. given #163 (T,wt=7): 716 x <= y \/ L * x. [para(521(a,1),589(a,1))]. given #164 (T,wt=7): 724 x /\ y <= x \/ z. [para(30(a,1),591(a,2))]. given #165 (A,wt=14): 102 x <= y \/ z | (x /\ y) \/ (x /\ z) != x. [para(42(a,1),41(b,1))]. given #166 (F,wt=15): 582 x \/ (y \/ (z \/ (u \/ (w \/ (c2 \/ v5))))) != O. [para(33(a,1),540(a,1,2,2,2))]. given #167 (F,wt=15): 583 x \/ (y \/ (z \/ (u \/ (w \/ (v5 \/ c2))))) != O. [para(33(a,1),541(a,1,2,2,2,2))]. given #168 (F,wt=15): 627 x \/ (y \/ (z \/ (u \/ (w \/ (c3 \/ v5))))) != O. [para(33(a,1),542(a,1,2,2,2))]. given #169 (F,wt=15): 628 x \/ (y \/ (z \/ (u \/ (w \/ (v5 \/ c3))))) != O. [para(33(a,1),543(a,1,2,2,2,2))]. given #170 (T,wt=7): 730 c2 * x /\ y <= c2. [para(228(a,1),591(a,2))]. given #171 (T,wt=7): 731 c3 * x /\ y <= c3. [para(249(a,1),591(a,2))]. given #172 (T,wt=7): 740 c2 * x <= c2 \/ y. [para(30(a,1),594(a,2))]. given #173 (T,wt=7): 750 c3 * x <= c3 \/ y. [para(30(a,1),595(a,2))]. given #174 (A,wt=10): 118 x \/ (y \/ (x \/ y)') = L. [para(46(a,1),33(a,1)),flip(a)]. given #175 (F,wt=15): 870 x \/ (y \/ (z \/ (u \/ (w \/ (I \/ v5))))) != O. [para(33(a,1),868(a,1,2,2,2))]. given #176 (F,wt=15): 871 x \/ (y \/ (z \/ (u \/ (w \/ (v5 \/ I))))) != O. [para(33(a,1),869(a,1,2,2,2,2))]. given #177 (F,wt=17): 915 x \/ (y \/ (z \/ (u \/ (w \/ (v5 \/ (c2 \/ v6)))))) != O. [para(33(a,1),582(a,1,2,2,2,2))]. given #178 (F,wt=17): 916 x \/ (y \/ (z \/ (u \/ (w \/ (v5 \/ (v6 \/ c2)))))) != O. [para(33(a,1),583(a,1,2,2,2,2,2))]. given #179 (T,wt=7): 825 x <= x * L \/ y. [para(472(a,1),610(a,1))]. given #180 (T,wt=7): 826 x <= L * x \/ y. [para(521(a,1),610(a,1))]. given #181 (T,wt=7): 832 x /\ y <= x * L. [para(31(a,1),643(a,1))]. given #182 (T,wt=7): 837 x <= L * (x * L). [para(521(a,1),643(a,1)),rewrite([50(4)])]. given #183 (A,wt=8): 119 x <= x' | x' != L. [para(46(a,1),39(b,1)),flip(b)]. given #184 (F,wt=17): 917 x \/ (y \/ (z \/ (u \/ (w \/ (v5 \/ (c3 \/ v6)))))) != O. [para(33(a,1),627(a,1,2,2,2,2))]. given #185 (F,wt=17): 918 x \/ (y \/ (z \/ (u \/ (w \/ (v5 \/ (v6 \/ c3)))))) != O. [para(33(a,1),628(a,1,2,2,2,2,2))]. given #186 (F,wt=17): 966 x \/ (y \/ (z \/ (u \/ (w \/ (v5 \/ (I \/ v6)))))) != O. [para(33(a,1),870(a,1,2,2,2,2))]. given #187 (F,wt=17): 967 x \/ (y \/ (z \/ (u \/ (w \/ (v5 \/ (v6 \/ I)))))) != O. [para(33(a,1),871(a,1,2,2,2,2,2))]. given #188 (T,wt=7): 843 x /\ y <= L * x. [para(31(a,1),669(a,1))]. given #189 (T,wt=8): 174 I ^ * x ^ = x ^. [para(51(a,1),64(a,1,1)),flip(a)]. given #190 (T,wt=6): 1026 I ^ * x = x. [para(71(a,1),174(a,1,2)),rewrite([71(5)])]. given #191 (T,wt=4): 1029 I ^ = I. [para(1026(a,1),51(a,1)),flip(a)]. given #192 (A,wt=10): 123 x /\ (y /\ (x /\ y)') = O. [para(48(a,1),35(a,1)),flip(a)]. given #193 (F,wt=18): 316 x * (y * z) != O | L * (x * (y * (z * L))) != L. [para(50(a,1),154(b,1,2,2))]. given #194 (F,wt=18): 370 x \/ y != O | L * (y * L) \/ L * (x * L) != L. [para(30(a,1),165(b,1))]. given #195 (F,wt=18): 1052 O != x | L * (x * L) \/ L * ((y /\ x) * L) != L. [para(36(a,1),370(a,1)),rewrite([30(12)]),flip(a)]. given #196 (F,wt=12): 1062 x' != O | L * (x' * L) != L. [para(48(a,1),1052(b,1,2,2,1)),rewrite([74(12),75(11),30(10),197(10)]),flip(a)]. given #197 (T,wt=8): 198 x /\ (x' /\ y) = O. [back_rewrite(122),rewrite([196(5)])]. given #198 (T,wt=8): 211 O ^ * x' <= y'. [para(74(a,1),54(a,1)),unit_del(a,72)]. given #199 (T,wt=7): 1082 O ^ * L <= x'. [para(299(a,1),211(a,1,2))]. given #200 (T,wt=6): 1091 O ^ * L <= O. [para(418(a,1),1082(a,2))]. given #201 (A,wt=25): 127 x * y /\ (z /\ (x /\ z * y ^) * (y /\ x ^ * z)) = x * y /\ z. [resolve(53,a,40,a),rewrite([35(10)])]. given #202 (F,wt=12): 1065 L * x != O | L * (x * L) != L. [para(521(a,1),1052(b,1,2,2,1)),rewrite([50(9),655(10),276(13)]),flip(a)]. given #203 (F,wt=16): 1074 x' /\ y != O | L * ((x' /\ y) * L) != L. [para(198(a,1),1052(b,1,2,2,1)),rewrite([74(14),75(13),30(12),197(12)]),flip(a)]. given #204 (F,wt=16): 1149 L * (x * y) != O | L * (x * (y * L)) != L. [para(50(a,1),1065(b,1,2))]. given #205 (F,wt=14): 1156 L * (x * c2) != O | L * (x * c2) != L. [para(79(a,1),1149(b,1,2,2))]. given #206 (T,wt=6): 1097 O ^ * L = O. [resolve(1091,a,40,a),rewrite([31(6),196(6)]),flip(a)]. given #207 (T,wt=4): 1163 O ^ = O. [para(1097(a,1),59(b,1,2)),rewrite([75(7)]),flip(a),unit_del(b,153)]. given #208 (T,wt=8): 221 c2 /\ (c1 * L)' = c2. [resolve(77,a,40,a)]. given #209 (T,wt=8): 229 L ^ * c2 ^ = c2 ^. [para(79(a,1),64(a,1,1)),flip(a)]. given #210 (A,wt=33): 128 (x * y /\ z) \/ (x /\ z * y ^) * (y /\ x ^ * z) = (x /\ z * y ^) * (y /\ x ^ * z). [resolve(53,a,38,a)]. given #211 (F,wt=6): 1179 (c1 * L)' != O. [para(221(a,1),1052(b,1,2,2,1)),rewrite([79(18),80(17),30(16),333(16)]),flip(a),xx(b)]. given #212 (F,wt=14): 1157 L * (x * c3) != O | L * (x * c3) != L. [para(82(a,1),1149(b,1,2,2))]. given #213 (F,wt=14): 1158 L * (x * L) != O | L * (x * L) != L. [para(640(a,1),1149(b,1,2,2))]. given #214 (F,wt=16): 1151 x' /\ y != O | L * ((y /\ x') * L) != L. [para(31(a,1),1074(b,1,2,1))]. given #215 (T,wt=7): 1186 c2 ^ <= L ^ * L. [para(229(a,1),204(a,1))]. given #216 (T,wt=8): 235 c2 ^ * L ^ = L ^. [para(80(a,1),64(a,1,1)),flip(a)]. given #217 (T,wt=7): 1252 L ^ <= c2 ^ * L. [para(235(a,1),204(a,1))]. given #218 (T,wt=8): 238 x * (c2 * c2 ^) <= x. [resolve(81,a,68,a),rewrite([51(7)])]. given #219 (A,wt=19): 129 x /\ y * z <= (y /\ x * z ^) * (z /\ y ^ * x). [para(31(a,1),53(a,1))]. given #220 (F,wt=18): 1057 O != x | L * (x * L) \/ L * ((x /\ y) * L) != L. [para(90(a,1),370(a,1)),rewrite([30(12)]),flip(a)]. given #221 (F,wt=18): 1159 L * (x * (y * c2)) != O | L * (x * (y * c2)) != L. [para(50(a,1),1156(a,1,2)),rewrite([50(11)])]. given #222 (F,wt=18): 1234 L * (x * (y * c3)) != O | L * (x * (y * c3)) != L. [para(50(a,1),1157(a,1,2)),rewrite([50(11)])]. given #223 (F,wt=18): 1236 L * (x * (y * L)) != O | L * (x * (y * L)) != L. [para(50(a,1),1158(a,1,2)),rewrite([50(11)])]. given #224 (T,wt=8): 239 c2 * (c2 ^ * x) <= x. [resolve(81,a,67,a),rewrite([50(5),52(7)])]. given #225 (T,wt=7): 1326 c2 * L ^ <= L ^. [para(235(a,1),239(a,1,2))]. given #226 (T,wt=8): 243 I \/ c2 * c2 ^ = I. [resolve(81,a,38,a),rewrite([30(6)])]. given #227 (T,wt=8): 250 L ^ * c3 ^ = c3 ^. [para(82(a,1),64(a,1,1)),flip(a)]. given #228 (A,wt=19): 130 x * y /\ z <= (z * y ^ /\ x) * (y /\ x ^ * z). [para(31(a,1),53(a,2,1))]. given #229 (F,wt=19): 968 x \/ (y \/ (z \/ (u \/ (w \/ (v5 \/ (v6 \/ (c2 \/ v7))))))) != O. [para(33(a,1),915(a,1,2,2,2,2,2))]. given #230 (F,wt=19): 969 x \/ (y \/ (z \/ (u \/ (w \/ (v5 \/ (v6 \/ (v7 \/ c2))))))) != O. [para(33(a,1),916(a,1,2,2,2,2,2,2))]. given #231 (F,wt=19): 1006 x \/ (y \/ (z \/ (u \/ (w \/ (v5 \/ (v6 \/ (c3 \/ v7))))))) != O. [para(33(a,1),917(a,1,2,2,2,2,2))]. given #232 (F,wt=19): 1007 x \/ (y \/ (z \/ (u \/ (w \/ (v5 \/ (v6 \/ (v7 \/ c3))))))) != O. [para(33(a,1),918(a,1,2,2,2,2,2,2))]. given #233 (T,wt=7): 1349 c3 ^ <= L ^ * L. [para(250(a,1),204(a,1))]. given #234 (T,wt=8): 256 c3 ^ * L ^ = L ^. [para(83(a,1),64(a,1,1)),flip(a)]. given #235 (T,wt=7): 1408 L ^ <= c3 ^ * L. [para(256(a,1),204(a,1))]. given #236 (T,wt=8): 259 x * (c3 * c3 ^) <= x. [resolve(84,a,68,a),rewrite([51(7)])]. given #237 (A,wt=19): 131 x * y /\ z <= (x /\ z * y ^) * (x ^ * z /\ y). [para(31(a,1),53(a,2,2))]. given #238 (F,wt=19): 1008 x \/ (y \/ (z \/ (u \/ (w \/ (v5 \/ (v6 \/ (I \/ v7))))))) != O. [para(33(a,1),966(a,1,2,2,2,2,2))]. given #239 (F,wt=19): 1009 x \/ (y \/ (z \/ (u \/ (w \/ (v5 \/ (v6 \/ (v7 \/ I))))))) != O. [para(33(a,1),967(a,1,2,2,2,2,2,2))]. given #240 (F,wt=20): 326 x * (y * (z * c2)) != O | L * (x * (y * (z * c2))) != L. [para(50(a,1),322(b,1,2,2)),rewrite([50(3)])]. given #241 (F,wt=20): 363 x * (y * (z * c3)) != O | L * (x * (y * (z * c3))) != L. [para(50(a,1),324(b,1,2,2)),rewrite([50(3)])]. given #242 (T,wt=8): 260 c3 * (c3 ^ * x) <= x. [resolve(84,a,67,a),rewrite([50(5),52(7)])]. given #243 (T,wt=7): 1486 c3 * L ^ <= L ^. [para(256(a,1),260(a,1,2))]. given #244 (T,wt=8): 264 I \/ c3 * c3 ^ = I. [resolve(84,a,38,a),rewrite([30(6)])]. given #245 (T,wt=8): 295 x \/ (y \/ x') = L. [para(46(a,1),87(a,1,2)),rewrite([209(2)]),flip(a)]. given #246 (A,wt=26): 132 (x /\ y) * z /\ u <= (x /\ (y /\ u * z ^)) * (z /\ (x ^ /\ y ^) * u). [para(35(a,1),53(a,2,1)),rewrite([66(9)])]. given #247 (F,wt=20): 366 x * (y * (z * L)) != O | L * (x * (y * (z * L))) != L. [para(50(a,1),361(b,1,2,2)),rewrite([50(3)])]. given #248 (F,wt=20): 1059 O != x | L * (x * L) \/ L * ((y /\ (z /\ x)) * L) != L. [para(93(a,1),370(a,1)),rewrite([30(13)]),flip(a)]. given #249 (F,wt=20): 1066 x /\ (y /\ x)' != O | L * ((x /\ (y /\ x)') * L) != L. [para(123(a,1),1052(b,1,2,2,1)),rewrite([74(16),75(15),30(14),197(14)]),flip(a)]. given #250 (F,wt=20): 1152 x' /\ (y /\ z) != O | L * ((y /\ (x' /\ z)) * L) != L. [para(89(a,1),1074(b,1,2,1))]. given #251 (T,wt=8): 312 c1 \/ c2 * c3 ^ = c1. [back_unit_del(78),unit_del(a,307)]. given #252 (T,wt=6): 1577 c2 * c3 ^ <= c1. [resolve(312,a,94,b)]. given #253 (T,wt=7): 1594 c1' * c3 <= c2'. [resolve(1577,a,56,a),rewrite([71(5)])]. given #254 (T,wt=8): 314 x /\ (y /\ x') = O. [para(48(a,1),89(a,1,2)),rewrite([296(2)]),flip(a)]. given #255 (A,wt=26): 133 x * (y /\ z) /\ u <= (x /\ u * (y ^ /\ z ^)) * (y /\ (z /\ x ^ * u)). [para(35(a,1),53(a,2,2)),rewrite([66(5)])]. given #256 (F,wt=14): 1576 x /\ y != O | L * ((x /\ y) * L) != L. [para(299(a,1),1152(b,1,2,1,2,1)),rewrite([299(2),332(3),332(6)])]. given #257 (F,wt=14): 1656 x /\ y != O | L * ((y /\ x) * L) != L. [para(31(a,1),1576(b,1,2,1))]. given #258 (F,wt=17): 1589 c1 != O | L * (c1 * L) \/ L * (c3 ^ * L) != L. [para(312(a,1),370(a,1)),rewrite([50(10),230(11),30(15)])]. given #259 (F,wt=18): 1657 x /\ (y /\ z) != O | L * ((y /\ (x /\ z)) * L) != L. [para(89(a,1),1576(b,1,2,1))]. given #260 (T,wt=7): 1614 c2 /\ c1 * L = O. [para(221(a,1),314(a,1,2)),rewrite([31(5)])]. given #261 (T,wt=7): 1662 c3 ^ = O | c1 != O. [para(59(b,1),1589(b,1,2)),rewrite([30(14),333(14)]),flip(a),xx(c)]. given #262 (T,wt=8): 335 x ^ /\ L ^ = x ^. [para(208(a,1),66(a,1,1)),flip(a)]. given #263 (T,wt=5): 1675 x ^ <= L ^. [resolve(335,a,41,b)]. given #264 (A,wt=67): 134 (x * y /\ z) \/ (x * y /\ u) <= (x /\ z * y ^) * (y /\ x ^ * z) \/ ((x /\ u * y ^) * (y /\ x ^ * z) \/ ((x /\ z * y ^) * (y /\ x ^ * u) \/ (x /\ u * y ^) * (y /\ x ^ * u))). [para(42(a,1),53(a,1)),rewrite([62(8),42(11),63(15),42(18),63(20),62(16),62(31),33(36)])]. given #265 (F,wt=12): 1688 x ^ != O | L * (x ^ * L) != L. [para(335(a,1),1057(b,1,2,2,1)),rewrite([276(14)]),flip(a)]. given #266 (F,wt=18): 1659 x /\ (y /\ z) != O | L * ((y /\ (z /\ x)) * L) != L. [para(35(a,1),1656(b,1,2,1))]. given #267 (F,wt=12): 1822 L * ((x' /\ (y /\ x)) * L) != L. [ur(1659,a,198,a)]. given #268 (F,wt=12): 1836 L * ((x /\ (x * L)') * L) != L. [para(472(a,1),1822(a,1,2,1,2)),rewrite([31(5)])]. given #269 (T,wt=4): 1740 x <= L ^. [para(71(a,1),1675(a,1))]. given #270 (T,wt=6): 1678 x /\ L ^ = x. [para(71(a,1),335(a,1,1)),rewrite([71(5)])]. given #271 (T,wt=4): 1854 L ^ = L. [para(1678(a,1),332(a,1)),flip(a)]. given #272 (T,wt=6): 1873 c3 ^ * L = L. [back_rewrite(1424),rewrite([1854(2),332(6),1854(6)])]. given #273 (A,wt=26): 135 x * (y * z) /\ u <= (x * y /\ u * z ^) * (z /\ y ^ * (x ^ * u)). [para(50(a,1),53(a,1,1)),rewrite([64(9),50(11)])]. given #274 (F,wt=3): 1979 c1 != O. [back_rewrite(1589),rewrite([1873(13),640(11),30(10),333(10)]),xx(b)]. given #275 (F,wt=4): 1982 c3 ^ != O. [para(1873(a,1),61(b,1,2)),rewrite([640(7)]),flip(a),xx(b)]. given #276 (F,wt=6): 1984 c3 ^ \/ x != O. [para(1873(a,1),165(b,1,1,2)),rewrite([640(8),333(11)]),xx(b)]. given #277 (F,wt=4): 2025 -(c3 ^ <= O). [ur(38,b,1984,a)]. given #278 (T,wt=6): 1880 c2 ^ * L = L. [back_rewrite(1263),rewrite([1854(2),332(6),1854(6)])]. given #279 (T,wt=7): 1963 x <= x * (L * x). [back_rewrite(656),rewrite([1854(2),1854(3),655(4)])]. given #280 (T,wt=7): 1971 L * c3 ^ = c3 ^. [back_rewrite(250),rewrite([1854(2)])]. given #281 (T,wt=7): 1974 L * c2 ^ = c2 ^. [back_rewrite(229),rewrite([1854(2)])]. given #282 (A,wt=25): 136 x * y /\ z * u <= (x /\ z * (u * y ^)) * (y /\ x ^ * (z * u)). [para(50(a,1),53(a,2,1,2))]. given #283 (F,wt=4): 2027 c2 ^ != O. [para(1880(a,1),61(b,1,2)),rewrite([640(7)]),flip(a),xx(b)]. given #284 (F,wt=6): 1985 x \/ c3 ^ != O. [para(1873(a,1),165(b,1,2,2)),rewrite([640(12),30(11),333(11)]),xx(b)]. given #285 (F,wt=6): 2029 c2 ^ \/ x != O. [para(1880(a,1),165(b,1,1,2)),rewrite([640(8),333(11)]),xx(b)]. given #286 (F,wt=4): 2085 -(c2 ^ <= O). [ur(38,b,2029,a)]. given #287 (T,wt=7): 2044 x * c3 ^ <= c3 ^. [para(1971(a,1),205(a,2))]. given #288 (T,wt=7): 2049 x * c2 ^ <= c2 ^. [para(1974(a,1),205(a,2))]. given #289 (T,wt=8): 346 x \/ (x' \/ y) = L. [back_rewrite(117),rewrite([333(5)])]. given #290 (T,wt=8): 360 x * L != O | O = x. [resolve(329,b,59,b)]. given #291 (A,wt=15): 138 I /\ x * y <= (x /\ y ^) * (y /\ x ^). [para(51(a,1),53(a,2,2,2)),rewrite([31(3),52(6)])]. given #292 (F,wt=5): 2113 c1 * L != O. [ur(360,b,1979,a(flip))]. given #293 (F,wt=6): 2030 x \/ c2 ^ != O. [para(1880(a,1),165(b,1,2,2)),rewrite([640(12),30(11),333(11)]),xx(b)]. given #294 (F,wt=8): 2026 x \/ (c3 ^ \/ y) != O. [para(87(a,1),1984(a,1))]. given #295 (F,wt=8): 2084 x \/ (y \/ c3 ^) != O. [para(33(a,1),1985(a,1))]. given #296 (T,wt=6): 2130 I <= c2 ^ * c2. [para(80(a,1),138(a,1,2)),rewrite([31(3),332(3),332(5),1854(6),31(6),332(6)])]. given #297 (T,wt=6): 2132 I <= c3 ^ * c3. [para(83(a,1),138(a,1,2)),rewrite([31(3),332(3),332(5),1854(6),31(6),332(6)])]. given #298 (T,wt=8): 375 O = x | x \/ y != O. [para(59(b,1),165(b,1,1)),rewrite([333(11)]),xx(c)]. given #299 (T,wt=8): 376 O = x | y \/ x != O. [para(59(b,1),165(b,1,2)),rewrite([30(11),333(11)]),xx(c)]. given #300 (A,wt=18): 140 -(x * (y * z) <= u) | y ^ * (x ^ * u') <= z'. [para(50(a,1),54(a,1)),rewrite([64(5),50(8)])]. given #301 (F,wt=5): 2153 c1 \/ x != O. [ur(375,a,1979,a(flip))]. given #302 (F,wt=3): 2204 -(c1 <= O). [ur(38,b,2153,a)]. given #303 (F,wt=5): 2159 x \/ c1 != O. [ur(376,a,1979,a(flip))]. given #304 (F,wt=7): 2152 c1 * L \/ x != O. [ur(375,a,2113,a(flip))]. given #305 (T,wt=8): 397 x \/ (y /\ x)' = L. [para(46(a,1),91(a,1,2)),rewrite([209(2)]),flip(a)]. given #306 (T,wt=8): 479 c2' * x ^ <= c2'. [resolve(464,a,56,a)]. given #307 (T,wt=7): 2235 c2' * x <= c2'. [para(71(a,1),479(a,1,2))]. given #308 (T,wt=8): 480 c2 ^ * c2' <= x'. [resolve(464,a,54,a)]. given #309 (A,wt=11): 141 -(x <= y) | x ^ * y' <= I'. [para(51(a,1),54(a,1))]. given #310 (F,wt=5): 2207 -(c1 * L <= O). [ur(38,b,2152,a)]. given #311 (F,wt=4): 2306 -(L <= c1'). [ur(57,a,2207,a),rewrite([299(2),1854(3),640(3)])]. given #312 (F,wt=4): 2308 c1' != L. [ur(417,a,2306,a),flip(a)]. given #313 (F,wt=6): 2307 -(c1 ^ * L <= O). [ur(55,a,2207,a),rewrite([299(4),418(6)])]. given #314 (T,wt=7): 2253 c2 ^ * c2' <= O. [para(418(a,1),480(a,2))]. given #315 (T,wt=5): 2317 c2 <= c2''. [resolve(2253,a,54,a),rewrite([71(3),299(3),79(3)])]. given #316 (T,wt=7): 2318 c2 ^ * c2' = O. [resolve(2253,a,40,a),rewrite([31(7),196(7)]),flip(a)]. given #317 (T,wt=7): 2324 c2 /\ c2'' = c2. [resolve(2317,a,40,a)]. given #318 (A,wt=17): 143 -(x * (y * z) <= u) | u' * z ^ <= (x * y)'. [para(50(a,1),56(a,1))]. given #319 (F,wt=5): 2310 -(L <= c1 ^'). [ur(57,a,2307,a),rewrite([299(2),1854(3),640(3)])]. given #320 (F,wt=5): 2347 c2'' != O. [para(2324(a,1),1052(b,1,2,2,1)),rewrite([79(16),80(15),30(14),333(14)]),flip(a),xx(b)]. given #321 (F,wt=5): 2391 c1 ^' != L. [ur(417,a,2310,a),flip(a)]. given #322 (F,wt=6): 2309 c1 ^ * L != O. [ur(390,a,2307,a),flip(a)]. given #323 (T,wt=7): 2331 c2' ^ * c2 = O. [para(2318(a,1),64(a,1,1)),rewrite([1163(2),71(7)]),flip(a)]. given #324 (T,wt=7): 2341 x /\ c2 <= c2''. [para(2324(a,1),415(a,1,2))]. given #325 (T,wt=7): 2342 c2 <= x \/ c2''. [para(2324(a,1),589(a,1))]. given #326 (T,wt=7): 2343 c2 <= c2'' \/ x. [para(2324(a,1),610(a,1))]. given #327 (A,wt=11): 145 -(x <= y) | y' * x ^ <= I'. [para(52(a,1),56(a,1))]. given #328 (F,wt=7): 2158 x \/ c1 * L != O. [ur(376,a,2113,a(flip))]. given #329 (F,wt=7): 2205 x \/ (c1 \/ y) != O. [ur(376,a,2153,a(flip))]. given #330 (F,wt=7): 2206 x \/ (y \/ c1) != O. [ur(376,a,2159,a(flip))]. given #331 (F,wt=7): 2392 x \/ c2'' != O. [ur(376,a,2347,a(flip))]. given #332 (T,wt=7): 2344 c2 <= c2'' * L. [para(2324(a,1),643(a,1))]. given #333 (T,wt=7): 2345 c2 <= L * c2''. [para(2324(a,1),669(a,1))]. given #334 (T,wt=7): 2408 c2 /\ x <= c2''. [para(31(a,1),2341(a,1))]. given #335 (T,wt=8): 487 c3' * x ^ <= c3'. [resolve(465,a,56,a)]. given #336 (A,wt=14): 146 O = x | L * (x * (L * y)) = L * y. [para(59(b,1),50(a,1,1)),rewrite([50(8)]),flip(b)]. given #337 (F,wt=7): 2393 c2'' \/ x != O. [ur(375,a,2347,a(flip))]. given #338 (F,wt=5): 2578 -(c2'' <= O). [ur(38,b,2393,a)]. given #339 (F,wt=7): 2394 c2'' * L != O. [ur(360,b,2347,a(flip))]. given #340 (F,wt=8): 2086 x \/ (c2 ^ \/ y) != O. [para(87(a,1),2029(a,1))]. given #341 (T,wt=7): 2528 c3' * x <= c3'. [para(71(a,1),487(a,1,2))]. given #342 (T,wt=8): 488 c3 ^ * c3' <= x'. [resolve(465,a,54,a)]. given #343 (T,wt=7): 2603 c3 ^ * c3' <= O. [para(418(a,1),488(a,2))]. given #344 (T,wt=5): 2611 c3 <= c3''. [resolve(2603,a,54,a),rewrite([71(3),299(3),82(3)])]. given #345 (A,wt=14): 147 O = x | y * (L * (x * L)) = y * L. [para(59(b,1),50(a,2,2)),rewrite([50(7)])]. given #346 (F,wt=8): 2114 (c1 * L)' * L != O. [ur(360,b,1179,a(flip))]. given #347 (F,wt=8): 2137 x \/ (y \/ c2 ^) != O. [para(33(a,1),2030(a,1))]. given #348 (F,wt=8): 2154 (c1 * L)' \/ x != O. [ur(375,a,1179,a(flip))]. given #349 (F,wt=6): 2669 -((c1 * L)' <= O). [ur(38,b,2154,a)]. given #350 (T,wt=7): 2612 c3 ^ * c3' = O. [resolve(2603,a,40,a),rewrite([31(7),196(7)]),flip(a)]. given #351 (T,wt=7): 2619 c3 /\ c3'' = c3. [resolve(2611,a,40,a)]. given #352 (T,wt=7): 2676 c3' ^ * c3 = O. [para(2612(a,1),64(a,1,1)),rewrite([1163(2),71(7)]),flip(a)]. given #353 (T,wt=7): 2687 x /\ c3 <= c3''. [para(2619(a,1),415(a,1,2))]. given #354 (A,wt=14): 148 x * y = O | L * (x * (y * L)) = L. [para(50(a,1),59(b,1,2)),flip(a)]. given #355 (F,wt=5): 2693 c3'' != O. [para(2619(a,1),1052(b,1,2,2,1)),rewrite([82(16),83(15),30(14),333(14)]),flip(a),xx(b)]. given #356 (F,wt=7): 2747 x \/ c3'' != O. [ur(376,a,2693,a(flip))]. given #357 (F,wt=7): 2748 c3'' \/ x != O. [ur(375,a,2693,a(flip))]. given #358 (F,wt=5): 2753 -(c3'' <= O). [ur(38,b,2748,a)]. given #359 (T,wt=7): 2688 c3 <= x \/ c3''. [para(2619(a,1),589(a,1))]. given #360 (T,wt=7): 2689 c3 <= c3'' \/ x. [para(2619(a,1),610(a,1))]. given #361 (T,wt=7): 2690 c3 <= c3'' * L. [para(2619(a,1),643(a,1))]. given #362 (T,wt=7): 2691 c3 <= L * c3''. [para(2619(a,1),669(a,1))]. given #363 (A,wt=13): 156 x * y \/ (z /\ x) * y = x * y. [para(36(a,1),62(a,1,1)),flip(a)]. given #364 (F,wt=7): 2749 c3'' * L != O. [ur(360,b,2693,a(flip))]. given #365 (F,wt=8): 2160 x \/ (c1 * L)' != O. [ur(376,a,1179,a(flip))]. given #366 (F,wt=8): 2395 x \/ c1 ^ * L != O. [ur(376,a,2309,a(flip))]. given #367 (F,wt=8): 2396 c1 ^ * L \/ x != O. [ur(375,a,2309,a(flip))]. given #368 (T,wt=7): 2707 c3 /\ x <= c3''. [para(31(a,1),2687(a,1))]. given #369 (T,wt=8): 538 x' <= O | x' != O. [para(48(a,1),96(b,1)),rewrite([48(3)]),flip(b)]. given #370 (T,wt=8): 578 x' <= x | x' != O. [para(48(a,1),97(b,1)),flip(b)]. given #371 (T,wt=8): 653 O = x | L * x != O. [back_rewrite(317),rewrite([640(9)]),xx(c)]. given #372 (A,wt=12): 158 x * y \/ x' * y = L * y. [para(46(a,1),62(a,1,1)),flip(a)]. given #373 (F,wt=5): 2848 L * c1 != O. [ur(653,a,1979,a(flip))]. given #374 (F,wt=7): 2830 L * c3'' != O. [ur(653,a,2693,a(flip))]. given #375 (F,wt=7): 2836 L * c2'' != O. [ur(653,a,2347,a(flip))]. given #376 (F,wt=7): 2847 L * (c1 * L) != O. [ur(653,a,2113,a(flip))]. given #377 (T,wt=8): 1027 -(x <= y) | y' <= x'. [back_rewrite(142),rewrite([1026(5)])]. given #378 (T,wt=7): 2892 c3''' <= c3'. [resolve(1027,a,2611,a)]. given #379 (T,wt=7): 2900 c2''' <= c2'. [resolve(1027,a,2317,a)]. given #380 (T,wt=7): 2928 (L * x)' <= x'. [resolve(1027,a,512,a)]. given #381 (A,wt=23): 160 -(x * y \/ z * y <= u) | x ^ * u' \/ z ^ * u' <= y'. [para(62(a,1),54(a,1)),rewrite([65(6),62(9)])]. given #382 (F,wt=7): 2878 x \/ L * c1 != O. [ur(376,a,2848,a(flip))]. given #383 (F,wt=7): 2879 L * c1 \/ x != O. [ur(375,a,2848,a(flip))]. given #384 (F,wt=5): 3026 -(L * c1 <= O). [ur(38,b,2879,a)]. given #385 (F,wt=6): 3027 -(L * c1 ^ <= O). [ur(57,a,3026,a),rewrite([299(2),418(6)])]. given #386 (T,wt=7): 2929 c3' <= (c3 * x)'. [resolve(1027,a,465,a)]. given #387 (T,wt=7): 2930 c2' <= (c2 * x)'. [resolve(1027,a,464,a)]. given #388 (T,wt=7): 2931 (x * L)' <= x'. [resolve(1027,a,461,a)]. given #389 (T,wt=7): 2935 x' <= (y /\ x)'. [resolve(1027,a,309,a)]. given #390 (A,wt=19): 161 -(x * y \/ z * y <= u) | u' * y ^ <= (x \/ z)'. [para(62(a,1),56(a,1))]. given #391 (F,wt=6): 3028 L * c1 ^ != O. [ur(390,a,3027,a),flip(a)]. given #392 (F,wt=8): 2837 L * (c1 ^ * L) != O. [ur(653,a,2309,a(flip))]. given #393 (F,wt=8): 2849 L * (c1 * L)' != O. [ur(653,a,1179,a(flip))]. given #394 (F,wt=8): 3112 x \/ L * c1 ^ != O. [ur(376,a,3028,a(flip))]. given #395 (T,wt=7): 2937 (x \/ y)' <= x'. [resolve(1027,a,307,a)]. given #396 (T,wt=7): 2938 x' <= (x /\ y)'. [resolve(1027,a,279,a)]. given #397 (T,wt=7): 2947 (x \/ y)' <= y'. [resolve(1027,a,199,a)]. given #398 (T,wt=8): 1030 x <= y | -(y' <= x'). [para(1026(a,1),55(b,1)),rewrite([52(2)])]. given #399 (A,wt=18): 162 x \/ y = O | L * (x * L) \/ L * (y * L) = L. [para(62(a,1),59(b,1,2)),rewrite([63(10)]),flip(a)]. given #400 (F,wt=4): 3164 -(L <= I'). [ur(1030,a,703,a),rewrite([299(2)])]. given #401 (F,wt=4): 3165 -(L <= c3'). [ur(1030,a,406,a),rewrite([299(2)])]. given #402 (F,wt=4): 3166 -(L <= c2'). [ur(1030,a,403,a),rewrite([299(2)])]. given #403 (F,wt=4): 3185 I' != L. [ur(417,a,3164,a),flip(a)]. given #404 (T,wt=7): 3167 x <= O | -(L <= x'). [para(299(a,1),1030(b,1))]. given #405 (T,wt=7): 3168 L <= x | -(x' <= O). [para(418(a,1),1030(b,2))]. given #406 (T,wt=8): 1064 x /\ y = O | O != y. [para(59(b,1),1052(b,1,2)),rewrite([30(11),333(11)]),flip(a),xx(c)]. given #407 (T,wt=8): 1166 x ^ /\ x' ^ = O. [back_rewrite(183),rewrite([1163(6)])]. given #408 (A,wt=13): 166 x * y \/ x * (z /\ y) = x * y. [para(36(a,1),63(a,1,2)),flip(a)]. given #409 (F,wt=4): 3186 c3' != L. [ur(417,a,3165,a),flip(a)]. given #410 (F,wt=4): 3187 c2' != L. [ur(417,a,3166,a),flip(a)]. given #411 (F,wt=5): 3160 -(c1'' <= O). [ur(1030,a,2306,a),rewrite([418(5)])]. given #412 (F,wt=5): 3162 -(L <= c2 ^'). [ur(1030,a,2085,a),rewrite([299(2)])]. given #413 (T,wt=7): 3199 I /\ I' ^ = O. [para(1029(a,1),1166(a,1,1))]. given #414 (T,wt=8): 1173 x /\ c2 <= (c1 * L)'. [para(221(a,1),415(a,1,2))]. given #415 (T,wt=8): 1174 c2 <= x \/ (c1 * L)'. [para(221(a,1),589(a,1))]. given #416 (T,wt=8): 1175 c2 <= (c1 * L)' \/ x. [para(221(a,1),610(a,1))]. given #417 (A,wt=12): 168 x * y \/ x * y' = x * L. [para(46(a,1),63(a,1,2)),flip(a)]. given #418 (F,wt=5): 3163 -(L <= c3 ^'). [ur(1030,a,2025,a),rewrite([299(2)])]. given #419 (F,wt=5): 3184 -(I'' <= O). [ur(1030,a,3164,a),rewrite([418(5)])]. given #420 (F,wt=5): 3230 c1'' != O. [ur(538,a,3160,a)]. given #421 (F,wt=5): 3232 c2 ^' != L. [ur(417,a,3162,a),flip(a)]. given #422 (T,wt=6): 3287 c2 ^ * c2 = L. [para(2318(a,1),168(a,1,2)),rewrite([30(6),197(6),1880(8)])]. given #423 (T,wt=6): 3291 c3 ^ * c3 = L. [para(2612(a,1),168(a,1,2)),rewrite([30(6),197(6),1873(8)])]. given #424 (T,wt=8): 1176 c2 <= (c1 * L)' * L. [para(221(a,1),643(a,1))]. given #425 (T,wt=8): 1177 c2 <= L * (c1 * L)'. [para(221(a,1),669(a,1))]. given #426 (A,wt=19): 170 -(x * y \/ x * z <= u) | x ^ * u' <= (y \/ z)'. [para(63(a,1),54(a,1))]. given #427 (F,wt=5): 3294 c3 ^' != L. [ur(417,a,3163,a),flip(a)]. given #428 (F,wt=5): 3296 I'' != O. [ur(538,a,3184,a)]. given #429 (F,wt=6): 3154 -(L <= (L * c1)'). [ur(1030,a,3026,a),rewrite([299(2)])]. given #430 (F,wt=6): 3155 -(L <= c3'''). [ur(1030,a,2753,a),rewrite([299(2)])]. given #431 (T,wt=8): 1307 x /\ y = O | O != x. [para(59(b,1),1057(b,1,2)),rewrite([30(11),333(11)]),flip(a),xx(c)]. given #432 (T,wt=8): 1340 c2 * c2 ^ <= x \/ I. [para(243(a,1),308(a,2,2))]. given #433 (T,wt=8): 1341 x /\ c2 * c2 ^ <= I. [para(243(a,1),589(a,2))]. given #434 (T,wt=8): 1342 c2 * c2 ^ /\ x <= I. [para(243(a,1),591(a,2))]. given #435 (A,wt=23): 171 -(x * y \/ x * z <= u) | u' * y ^ \/ u' * z ^ <= x'. [para(63(a,1),56(a,1)),rewrite([65(7),63(9)])]. given #436 (F,wt=6): 3157 -(L <= c2'''). [ur(1030,a,2578,a),rewrite([299(2)])]. given #437 (F,wt=6): 3158 -(c1 ^'' <= O). [ur(1030,a,2310,a),rewrite([418(6)])]. given #438 (F,wt=6): 3161 -(L <= (c1 * L)'). [ur(1030,a,2207,a),rewrite([299(2)])]. given #439 (F,wt=6): 3229 -(L <= c1'''). [ur(3167,a,3160,a)]. given #440 (T,wt=8): 1500 c3 * c3 ^ <= x \/ I. [para(264(a,1),308(a,2,2))]. given #441 (T,wt=8): 1501 x /\ c3 * c3 ^ <= I. [para(264(a,1),589(a,2))]. given #442 (T,wt=8): 1502 c3 * c3 ^ /\ x <= I. [para(264(a,1),591(a,2))]. given #443 (T,wt=8): 1586 c2 * c3 ^ <= x \/ c1. [para(312(a,1),308(a,2,2))]. given #444 (A,wt=26): 176 x * (y * z) /\ u <= (x /\ u * (z ^ * y ^)) * (y * z /\ x ^ * u). [para(64(a,1),53(a,2,1,2,2))]. given #445 (F,wt=6): 3231 -(c2 ^'' <= O). [ur(3168,a,3162,a)]. given #446 (F,wt=6): 3293 -(c3 ^'' <= O). [ur(3168,a,3163,a)]. given #447 (F,wt=6): 3295 -(L <= I'''). [ur(3167,a,3184,a)]. given #448 (F,wt=6): 3402 (L * c1)' != L. [ur(417,a,3154,a),flip(a)]. given #449 (T,wt=8): 1587 x /\ c2 * c3 ^ <= c1. [para(312(a,1),589(a,2))]. given #450 (T,wt=8): 1588 c2 * c3 ^ /\ x <= c1. [para(312(a,1),591(a,2))]. given #451 (T,wt=8): 1832 x' /\ (y /\ x) = O. [resolve(1822,a,59,b),flip(a)]. given #452 (T,wt=8): 1840 x /\ (x * L)' = O. [resolve(1836,a,59,b),flip(a)]. given #453 (A,wt=18): 177 x * (y * z) <= u | -(y ^ * (x ^ * u') <= z'). [para(64(a,1),55(b,1,1)),rewrite([50(2),50(8)])]. given #454 (F,wt=6): 3404 c3''' != L. [ur(417,a,3155,a),flip(a)]. given #455 (F,wt=6): 3487 c2''' != L. [ur(417,a,3157,a),flip(a)]. given #456 (F,wt=6): 3489 c1 ^'' != O. [ur(538,a,3158,a)]. given #457 (F,wt=6): 3491 (c1 * L)' != L. [ur(417,a,3161,a),flip(a)]. given #458 (T,wt=8): 1914 L <= x ^ | x ^ != L. [back_rewrite(1681),rewrite([1854(2),1854(5)]),flip(b)]. given #459 (T,wt=6): 3651 L <= I | I != L. [para(1029(a,1),1914(b,1)),rewrite([1029(3)])]. given #460 (T,wt=8): 1932 x <= x * (x ^ * x). [back_rewrite(1297),rewrite([1854(3),521(4)])]. given #461 (T,wt=8): 1976 x ^ \/ x' ^ = L. [back_rewrite(180),rewrite([1854(6)])]. given #462 (A,wt=18): 178 x * (y * z) <= u | -(u' * (z ^ * y ^) <= x'). [para(64(a,1),57(b,1,2))]. given #463 (F,wt=6): 3493 c1''' != L. [ur(417,a,3229,a),flip(a)]. given #464 (F,wt=6): 3579 c2 ^'' != O. [ur(538,a,3231,a)]. given #465 (F,wt=6): 3581 c3 ^'' != O. [ur(538,a,3293,a)]. given #466 (F,wt=6): 3583 I''' != L. [ur(417,a,3295,a),flip(a)]. given #467 (T,wt=7): 3682 I \/ I' ^ = L. [para(1029(a,1),1976(a,1,1))]. given #468 (T,wt=8): 2047 c3 ^ <= c3 ^ * c3 ^. [para(1971(a,1),1963(a,2,2))]. given #469 (T,wt=8): 2052 c2 ^ <= c2 ^ * c2 ^. [para(1974(a,1),1963(a,2,2))]. given #470 (T,wt=8): 2091 c3 ^' * c3 <= x'. [resolve(2044,a,56,a),rewrite([71(6)])]. given #471 (A,wt=23): 181 x * y \/ z * y <= u | -(x ^ * u' \/ z ^ * u' <= y'). [para(65(a,1),55(b,1,1)),rewrite([62(2),62(9)])]. given #472 (F,wt=7): 3153 -(L <= (L * c1 ^)'). [ur(1030,a,3027,a),rewrite([299(2)])]. given #473 (F,wt=7): 3156 -(L <= (c1 * L)''). [ur(1030,a,2669,a),rewrite([299(2)])]. given #474 (F,wt=7): 3159 -(L <= (c1 ^ * L)'). [ur(1030,a,2307,a),rewrite([299(2)])]. given #475 (F,wt=7): 3297 L * c1'' != O. [ur(653,a,3230,a(flip))]. given #476 (T,wt=7): 3741 c3 ^' * c3 <= O. [para(418(a,1),2091(a,2))]. given #477 (T,wt=7): 3773 c3 ^ <= c3 ^''. [resolve(3741,a,56,a),rewrite([299(2),1971(4)])]. given #478 (T,wt=7): 3775 c3 ^' * c3 = O. [resolve(3741,a,40,a),rewrite([31(7),196(7)]),flip(a)]. given #479 (T,wt=8): 2100 c2 ^' * c2 <= x'. [resolve(2049,a,56,a),rewrite([71(6)])]. given #480 (A,wt=23): 182 x * y \/ x * z <= u | -(u' * y ^ \/ u' * z ^ <= x'). [para(65(a,1),57(b,1,2)),rewrite([63(2),63(9)])]. given #481 (F,wt=7): 3298 x \/ c1'' != O. [ur(376,a,3230,a(flip))]. given #482 (F,wt=7): 3299 c1'' \/ x != O. [ur(375,a,3230,a(flip))]. given #483 (F,wt=7): 3300 c1'' * L != O. [ur(360,b,3230,a(flip))]. given #484 (F,wt=7): 3397 L * I'' != O. [ur(653,a,3296,a(flip))]. given #485 (T,wt=7): 3814 c2 ^' * c2 <= O. [para(418(a,1),2100(a,2))]. given #486 (T,wt=7): 3842 c2 ^ <= c2 ^''. [resolve(3814,a,56,a),rewrite([299(2),1974(4)])]. given #487 (T,wt=7): 3844 c2 ^' * c2 = O. [resolve(3814,a,40,a),rewrite([31(7),196(7)]),flip(a)]. given #488 (T,wt=8): 2129 I /\ c2 <= c2 * c2 ^. [para(79(a,1),138(a,1,2)),rewrite([1854(6),31(6),332(6),332(8)])]. given #489 (A,wt=18): 184 (x /\ y) * z <= u | -((x ^ /\ y ^) * u' <= z'). [para(66(a,1),55(b,1,1))]. given #490 (F,wt=7): 3398 x \/ I'' != O. [ur(376,a,3296,a(flip))]. given #491 (F,wt=7): 3399 I'' \/ x != O. [ur(375,a,3296,a(flip))]. given #492 (F,wt=7): 3400 I'' * L != O. [ur(360,b,3296,a(flip))]. given #493 (F,wt=7): 3401 -((L * c1)'' <= O). [ur(3168,a,3154,a)]. given #494 (T,wt=7): 3900 x * (I /\ c2) <= x. [back_rewrite(238),rewrite([3879(4)])]. given #495 (T,wt=8): 2131 I /\ c3 <= c3 * c3 ^. [para(82(a,1),138(a,1,2)),rewrite([1854(6),31(6),332(6),332(8)])]. given #496 (T,wt=7): 3953 x * (I /\ c3) <= x. [back_rewrite(259),rewrite([3932(4)])]. given #497 (T,wt=8): 2209 x \/ (x /\ y)' = L. [para(31(a,1),397(a,1,2,1))]. given #498 (A,wt=18): 185 x * (y /\ z) <= u | -(u' * (y ^ /\ z ^) <= x'). [para(66(a,1),57(b,1,2))]. given #499 (F,wt=7): 3403 -(c3'''' <= O). [ur(3168,a,3155,a)]. NOTE: Back_subsumption disabled, ratio of kept to back_subsumed is 27 (0.00 of 0.29 sec). given #500 (F,wt=7): 3486 -(c2'''' <= O). [ur(3168,a,3157,a)]. given #501 (F,wt=7): 3488 -(L <= c1 ^'''). [ur(3167,a,3158,a)]. given #502 (F,wt=7): 3490 -((c1 * L)'' <= O). [ur(3168,a,3161,a)]. given #503 (T,wt=8): 2220 x' \/ x * L = L. [para(472(a,1),397(a,1,2,1)),rewrite([30(4)])]. given #504 (T,wt=8): 2221 x' \/ L * x = L. [para(521(a,1),397(a,1,2,1)),rewrite([30(4)])]. given #505 (T,wt=8): 2283 x ^ * x' <= I'. [resolve(141,a,311,a)]. given #506 (T,wt=8): 2329 c2 * x' <= c2''. [para(2318(a,1),54(a,1)),rewrite([71(5)]),unit_del(a,72)]. given #507 (A,wt=23): 186 (x * y /\ z) * u <= (x /\ z * y ^) * ((y /\ x ^ * z) * u). [resolve(67,a,53,a),rewrite([50(11)])]. given #508 (F,wt=7): 3492 -(c1'''' <= O). [ur(3168,a,3229,a)]. given #509 (F,wt=7): 3578 -(L <= c2 ^'''). [ur(3167,a,3231,a)]. given #510 (F,wt=7): 3580 -(L <= c3 ^'''). [ur(3167,a,3293,a)]. given #511 (F,wt=7): 3582 -(I'''' <= O). [ur(3168,a,3295,a)]. given #512 (T,wt=8): 2332 c2' /\ c2 * x = O. [para(2318(a,1),127(a,1,2,2,2,2)),rewrite([296(12),75(12),31(6),196(6),31(4),196(4),31(6)]),flip(a)]. given #513 (T,wt=8): 2400 c2 /\ c2' * x = O. [para(2331(a,1),127(a,1,2,2,2,2)),rewrite([2332(10),296(7),75(7),31(6),196(6),31(5),196(5),31(6)]),flip(a)]. given #514 (T,wt=8): 2460 x' * x ^ <= I'. [resolve(145,a,311,a)]. given #515 (T,wt=8): 2674 c3 * x' <= c3''. [para(2612(a,1),54(a,1)),rewrite([71(5)]),unit_del(a,72)]. given #516 (A,wt=23): 187 x * (y * z /\ u) <= x * ((y /\ u * z ^) * (z /\ y ^ * u)). [resolve(68,a,53,a)]. given #517 (F,wt=7): 3758 (L * c1 ^)' != L. [ur(417,a,3153,a),flip(a)]. given #518 (F,wt=7): 3760 (c1 * L)'' != L. [ur(417,a,3156,a),flip(a)]. given #519 (F,wt=7): 3762 (c1 ^ * L)' != L. [ur(417,a,3159,a),flip(a)]. given #520 (F,wt=7): 3920 (L * c1)'' != O. [ur(538,a,3401,a)]. given #521 (T,wt=8): 2677 c3' /\ c3 * x = O. [para(2612(a,1),127(a,1,2,2,2,2)),rewrite([296(12),75(12),31(6),196(6),31(4),196(4),31(6)]),flip(a)]. given #522 (T,wt=8): 2698 c3 /\ c3' * x = O. [para(2676(a,1),127(a,1,2,2,2,2)),rewrite([2677(10),296(7),75(7),31(6),196(6),31(5),196(5),31(6)]),flip(a)]. given #523 (T,wt=8): 2860 c2 \/ c2' * L = L. [para(79(a,1),158(a,1,1)),rewrite([640(9)])]. given #524 (T,wt=8): 2861 c3 \/ c3' * L = L. [para(82(a,1),158(a,1,1)),rewrite([640(9)])]. given #525 (A,wt=23): 188 (x * y /\ z) \/ u <= (x /\ z * y ^) * (y /\ x ^ * z) \/ u. [resolve(69,a,53,a)]. given #526 (F,wt=7): 3984 c3'''' != O. [ur(538,a,3403,a)]. given #527 (F,wt=7): 3986 c2'''' != O. [ur(538,a,3486,a)]. given #528 (F,wt=7): 3988 c1 ^''' != L. [ur(417,a,3488,a),flip(a)]. given #529 (F,wt=7): 3990 (c1 * L)'' != O. [ur(538,a,3490,a)]. given #530 (T,wt=8): 2873 c2' ^' * c2 = L. [para(2331(a,1),158(a,1,1)),rewrite([197(8),80(9)])]. given #531 (T,wt=8): 2877 c3' ^' * c3 = L. [para(2676(a,1),158(a,1,1)),rewrite([197(8),83(9)])]. given #532 (T,wt=8): 2906 c1' <= (c2 * c3 ^)'. [resolve(1027,a,1577,a)]. given #533 (T,wt=8): 2959 (c1 * L)'' <= c2'. [resolve(1027,a,77,a)]. given #534 (A,wt=23): 189 x * y /\ (z /\ u) <= (x /\ z * y ^) * (y /\ x ^ * z) /\ u. [resolve(70,a,53,a),rewrite([35(3)])]. given #535 (F,wt=7): 4089 c1'''' != O. [ur(538,a,3492,a)]. given #536 (F,wt=7): 4091 c2 ^''' != L. [ur(417,a,3578,a),flip(a)]. given #537 (F,wt=7): 4093 c3 ^''' != L. [ur(417,a,3580,a),flip(a)]. given #538 (F,wt=7): 4095 I'''' != O. [ur(538,a,3582,a)]. given #539 (T,wt=8): 3192 x /\ x ^' ^ = O. [para(71(a,1),1166(a,1,1))]. given #540 (T,wt=8): 3247 c2 /\ x <= (c1 * L)'. [para(31(a,1),1173(a,1))]. given #541 (T,wt=8): 3286 c2 ^ * c2'' = L. [para(2318(a,1),168(a,1,1)),rewrite([197(8),1880(10)])]. given #542 (T,wt=7): 4484 L * c2'' = L. [para(3286(a,1),158(a,1,1)),rewrite([333(9)]),flip(a)]. given #543 (A,wt=20): 190 x * y ^ /\ z <= (x /\ z * y) * (y ^ /\ x ^ * z). [para(71(a,1),53(a,2,1,2,2))]. given #544 (F,wt=8): 3113 L * c1 ^ \/ x != O. [ur(375,a,3028,a(flip))]. given #545 (F,wt=8): 3645 L * c1 ^'' != O. [ur(653,a,3489,a(flip))]. given #546 (F,wt=8): 3646 x \/ c1 ^'' != O. [ur(376,a,3489,a(flip))]. given #547 (F,wt=8): 3647 c1 ^'' \/ x != O. [ur(375,a,3489,a(flip))]. given #548 (T,wt=5): 4548 c1 /\ c2 <= O. [para(1614(a,1),190(a,2,1)),rewrite([1854(3),79(3),31(3),1854(6),332(10),74(9)])]. given #549 (T,wt=5): 4584 c1 /\ c2 = O. [resolve(4548,a,40,a),rewrite([31(5),196(5)]),flip(a)]. given #550 (T,wt=7): 4585 c1 /\ (c2 /\ x) = O. [para(4584(a,1),35(a,1,1)),rewrite([196(2)]),flip(a)]. given #551 (T,wt=7): 4586 c2 /\ (x /\ c1) = O. [para(4584(a,1),35(a,2,2)),rewrite([31(4),296(6)])]. given #552 (A,wt=20): 191 x ^ * y /\ z <= (x ^ /\ z * y ^) * (y /\ x * z). [para(71(a,1),53(a,2,2,2,1))]. given #553 (F,wt=8): 3648 c1 ^'' * L != O. [ur(360,b,3489,a(flip))]. given #554 (F,wt=8): 3696 L * c2 ^'' != O. [ur(653,a,3579,a(flip))]. given #555 (F,wt=8): 3697 x \/ c2 ^'' != O. [ur(376,a,3579,a(flip))]. given #556 (F,wt=8): 3698 c2 ^'' \/ x != O. [ur(375,a,3579,a(flip))]. given #557 (T,wt=6): 4626 c1 ^ * c2 <= O. [para(1614(a,1),191(a,2,2)),rewrite([31(6),332(6),1974(10),4587(9),75(7)])]. given #558 (T,wt=6): 4654 c2 ^ <= c1 ^'. [resolve(4626,a,56,a),rewrite([299(2),1974(4)])]. given #559 (T,wt=6): 4655 c1 * L <= c2'. [resolve(4626,a,54,a),rewrite([71(3),299(3)])]. given #560 (T,wt=6): 4656 c1 ^ * c2 = O. [resolve(4626,a,40,a),rewrite([31(6),196(6)]),flip(a)]. given #561 (A,wt=13): 192 x ^ * y <= z | -(x * z' <= y'). [para(71(a,1),55(b,1,1))]. given #562 (F,wt=8): 3699 c2 ^'' * L != O. [ur(360,b,3579,a(flip))]. given #563 (F,wt=8): 3700 L * c3 ^'' != O. [ur(653,a,3581,a(flip))]. given #564 (F,wt=8): 3701 x \/ c3 ^'' != O. [ur(376,a,3581,a(flip))]. given #565 (F,wt=8): 3702 c3 ^'' \/ x != O. [ur(375,a,3581,a(flip))]. given #566 (T,wt=6): 4681 c2 ^ * c1 = O. [para(4656(a,1),64(a,1,1)),rewrite([1163(2),71(6)]),flip(a)]. ============================== PROOF ================================= % Proof 1 at 0.34 (+ 0.01) seconds. % Length of proof is 111. % Level of proof is 13. % Maximum clause weight is 20. % Given clauses 566. 1 x <= y <-> x \/ y = y # label(non_clause). [assumption]. 2 x <= y <-> x /\ y = x # label(non_clause). [assumption]. 3 x * y <= z <-> x ^ * z' <= y' # label(non_clause). [assumption]. 5 x != O <-> (L * x) * L = L # label(non_clause). [assumption]. 7 x <= y -> z * x <= z * y # label(non_clause). [assumption]. 8 x <= y -> x \/ z <= y \/ z # label(non_clause). [assumption]. 10 point(x) <-> x * L = x & L * x = L & x * x ^ <= I # label(non_clause). [assumption]. 15 (all p all q (x * L != L & point(p) & point(q) & p <= (x * L)' -> x <= x \/ p * q ^ & x != x \/ p * q ^)) # label(non_clause) # label(goal). [goal]. 17 -point(x) | x * L = x. [clausify(10)]. 18 -point(x) | L * x = L. [clausify(10)]. 20 point(c2). [deny(15)]. 21 point(c3). [deny(15)]. 30 x \/ y = y \/ x. [assumption]. 31 x /\ y = y /\ x. [assumption]. 34 x /\ (y /\ z) = (x /\ y) /\ z. [assumption]. 35 (x /\ y) /\ z = x /\ (y /\ z). [copy(34),flip(a)]. 36 x \/ (y /\ x) = x. [assumption]. 38 -(x <= y) | x \/ y = y. [clausify(1)]. 39 x <= y | x \/ y != y. [clausify(1)]. 40 -(x <= y) | x /\ y = x. [clausify(2)]. 45 L = x \/ x'. [assumption]. 46 x \/ x' = L. [copy(45),flip(a)]. 47 O = x /\ x'. [assumption]. 48 x /\ x' = O. [copy(47),flip(a)]. 49 x * (y * z) = (x * y) * z. [assumption]. 50 (x * y) * z = x * (y * z). [copy(49),flip(a)]. 51 x * I = x. [assumption]. 52 I * x = x. [assumption]. 53 x * y /\ z <= (x /\ z * y ^) * (y /\ x ^ * z). [assumption]. 54 -(x * y <= z) | x ^ * z' <= y'. [clausify(3)]. 55 x * y <= z | -(x ^ * z' <= y'). [clausify(3)]. 58 O = x | (L * x) * L = L. [clausify(5)]. 59 O = x | L * (x * L) = L. [copy(58),rewrite([50(6)])]. 60 O != x | (L * x) * L != L. [clausify(5)]. 61 O != x | L * (x * L) != L. [copy(60),rewrite([50(6)])]. 62 (x \/ y) * z = x * z \/ y * z. [assumption]. 63 x * (y \/ z) = x * y \/ x * z. [assumption]. 64 (x * y) ^ = y ^ * x ^. [assumption]. 66 (x /\ y) ^ = x ^ /\ y ^. [assumption]. 68 -(x <= y) | z * x <= z * y. [clausify(7)]. 69 -(x <= y) | x \/ z <= y \/ z. [clausify(8)]. 71 x ^ ^ = x. [assumption]. 72 O <= x. [assumption]. 73 x <= L. [assumption]. 74 O * x = O. [assumption]. 75 x * O = O. [assumption]. 77 c2 <= (c1 * L)'. [deny(15)]. 78 -(c1 <= c1 \/ c2 * c3 ^) | c1 \/ c2 * c3 ^ = c1. [deny(15)]. 79 c2 * L = c2. [resolve(20,a,17,a)]. 80 L * c2 = L. [resolve(20,a,18,a)]. 83 L * c3 = L. [resolve(21,a,18,a)]. 89 x /\ (y /\ z) = y /\ (x /\ z). [para(31(a,1),35(a,1,1)),rewrite([35(2)])]. 94 x <= y | y \/ x != y. [para(30(a,1),39(b,1))]. 153 O != L. [ur(61,a,52,a(flip)),rewrite([75(4),74(4),75(3)])]. 165 x \/ y != O | L * (x * L) \/ L * (y * L) != L. [para(62(a,1),61(b,1,2)),rewrite([63(10)]),flip(a)]. 168 x * y \/ x * y' = x * L. [para(46(a,1),63(a,1,2)),flip(a)]. 174 I ^ * x ^ = x ^. [para(51(a,1),64(a,1,1)),flip(a)]. 190 x * y ^ /\ z <= (x /\ z * y) * (y ^ /\ x ^ * z). [para(71(a,1),53(a,2,1,2,2))]. 191 x ^ * y /\ z <= (x ^ /\ z * y ^) * (y /\ x * z). [para(71(a,1),53(a,2,2,2,1))]. 195 O \/ x <= y \/ x. [resolve(72,a,69,a)]. 196 O /\ x = O. [resolve(72,a,40,a)]. 197 O \/ x = x. [resolve(72,a,38,a)]. 199 x <= y \/ x. [back_rewrite(195),rewrite([197(2)])]. 204 x * y <= x * L. [resolve(73,a,68,a)]. 208 x /\ L = x. [resolve(73,a,40,a)]. 211 O ^ * x' <= y'. [para(74(a,1),54(a,1)),unit_del(a,72)]. 221 c2 /\ (c1 * L)' = c2. [resolve(77,a,40,a)]. 229 L ^ * c2 ^ = c2 ^. [para(79(a,1),64(a,1,1)),flip(a)]. 235 c2 ^ * L ^ = L ^. [para(80(a,1),64(a,1,1)),flip(a)]. 256 c3 ^ * L ^ = L ^. [para(83(a,1),64(a,1,1)),flip(a)]. 296 x /\ O = O. [para(196(a,1),31(a,1)),flip(a)]. 299 O' = L. [para(197(a,1),46(a,1))]. 307 x <= x \/ y. [para(30(a,1),199(a,2))]. 312 c1 \/ c2 * c3 ^ = c1. [back_unit_del(78),unit_del(a,307)]. 314 x /\ (y /\ x') = O. [para(48(a,1),89(a,1,2)),rewrite([296(2)]),flip(a)]. 332 L /\ x = x. [para(208(a,1),31(a,1)),flip(a)]. 333 L \/ x = L. [para(208(a,1),36(a,1,2))]. 335 x ^ /\ L ^ = x ^. [para(208(a,1),66(a,1,1)),flip(a)]. 418 L' = O. [para(332(a,1),48(a,1))]. 461 x <= x * L. [para(51(a,1),204(a,1))]. 472 x /\ x * L = x. [resolve(461,a,40,a)]. 640 L * L = L. [para(472(a,1),332(a,1)),flip(a)]. 1026 I ^ * x = x. [para(71(a,1),174(a,1,2)),rewrite([71(5)])]. 1030 x <= y | -(y' <= x'). [para(1026(a,1),55(b,1)),rewrite([52(2)])]. 1082 O ^ * L <= x'. [para(299(a,1),211(a,1,2))]. 1091 O ^ * L <= O. [para(418(a,1),1082(a,2))]. 1097 O ^ * L = O. [resolve(1091,a,40,a),rewrite([31(6),196(6)]),flip(a)]. 1163 O ^ = O. [para(1097(a,1),59(b,1,2)),rewrite([75(7)]),flip(a),unit_del(b,153)]. 1252 L ^ <= c2 ^ * L. [para(235(a,1),204(a,1))]. 1263 L ^ /\ c2 ^ * L = L ^. [resolve(1252,a,40,a)]. 1408 L ^ <= c3 ^ * L. [para(256(a,1),204(a,1))]. 1424 L ^ /\ c3 ^ * L = L ^. [resolve(1408,a,40,a)]. 1577 c2 * c3 ^ <= c1. [resolve(312,a,94,b)]. 1595 c2 ^ * c1' <= c3 ^'. [resolve(1577,a,54,a)]. 1614 c2 /\ c1 * L = O. [para(221(a,1),314(a,1,2)),rewrite([31(5)])]. 1678 x /\ L ^ = x. [para(71(a,1),335(a,1,1)),rewrite([71(5)])]. 1854 L ^ = L. [para(1678(a,1),332(a,1)),flip(a)]. 1873 c3 ^ * L = L. [back_rewrite(1424),rewrite([1854(2),332(6),1854(6)])]. 1880 c2 ^ * L = L. [back_rewrite(1263),rewrite([1854(2),332(6),1854(6)])]. 1974 L * c2 ^ = c2 ^. [back_rewrite(229),rewrite([1854(2)])]. 1984 c3 ^ \/ x != O. [para(1873(a,1),165(b,1,1,2)),rewrite([640(8),333(11)]),xx(b)]. 2025 -(c3 ^ <= O). [ur(38,b,1984,a)]. 3163 -(L <= c3 ^'). [ur(1030,a,2025,a),rewrite([299(2)])]. 4548 c1 /\ c2 <= O. [para(1614(a,1),190(a,2,1)),rewrite([1854(3),79(3),31(3),1854(6),332(10),74(9)])]. 4584 c1 /\ c2 = O. [resolve(4548,a,40,a),rewrite([31(5),196(5)]),flip(a)]. 4587 c1 ^ /\ c2 ^ = O. [para(4584(a,1),66(a,1,1)),rewrite([1163(2)]),flip(a)]. 4626 c1 ^ * c2 <= O. [para(1614(a,1),191(a,2,2)),rewrite([31(6),332(6),1974(10),4587(9),75(7)])]. 4656 c1 ^ * c2 = O. [resolve(4626,a,40,a),rewrite([31(6),196(6)]),flip(a)]. 4681 c2 ^ * c1 = O. [para(4656(a,1),64(a,1,1)),rewrite([1163(2),71(6)]),flip(a)]. 4727 c2 ^ * c1' = L. [para(4681(a,1),168(a,1,1)),rewrite([197(7),1880(9)])]. 4736 $F. [back_rewrite(1595),rewrite([4727(5)]),unit_del(a,3163)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=566. Generated=15452. Kept=4698. proofs=1. Usable=490. Sos=3316. Demods=667. Limbo=9, Disabled=944. Hints=0. Weight_deleted=54. Literals_deleted=0. Forward_subsumed=10699. Back_subsumed=143. Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. New_demodulators=907 (6 lex), Back_demodulated=737. Back_unit_deleted=1. Demod_attempts=213429. Demod_rewrites=33483. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=11590. Nonunit_bsub_feature_tests=6659. Megabytes=5.06. User_CPU=0.34, System_CPU=0.01, Wall_clock=1. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED Exiting with 1 proof. Process 6769 exit (max_proofs) Fri Mar 27 10:49:17 2015