============================== Prover9 =============================== Prover9 (32) version Dec-2007, Dec 2007. Process 6345 was started by peterhoefner on callisto.dynhost.nicta.com.au, Thu Mar 26 12:06:42 2015 The command was "prover9 -f Prover9Lemma3.3.in". ============================== end of head =========================== ============================== INPUT ================================= % Reading from file Prover9Lemma3.3.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. x <= z & y <= z -> x \/ y <= z. 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 (symmetric(z) & irreflexive(z) & (x ^ * z) * p != L & coloringProperty(x,z) & point(p) & point(q) & q <= ((x ^ * z) * p)' -> ((p * q ^) * q) * p ^ <= z')). 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 x <= z & y <= z -> x \/ y <= z # label(non_clause). [assumption]. 11 point(x) <-> x * L = x & L * x = L & x * x ^ <= I # label(non_clause). [assumption]. 12 irreflexive(x) <-> x <= I' # label(non_clause). [assumption]. 13 symmetric(x) <-> x = x ^ # label(non_clause). [assumption]. 14 univalent(x) <-> x ^ * x <= I # label(non_clause). [assumption]. 15 coloringProperty(x,z) <-> x * x ^ <= z' # label(non_clause). [assumption]. 16 (all p all q (symmetric(z) & irreflexive(z) & (x ^ * z) * p != L & coloringProperty(x,z) & point(p) & point(q) & q <= ((x ^ * z) * p)' -> ((p * q ^) * q) * p ^ <= z')) # 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]. -(x <= y) | -(z <= y) | x \/ z <= y. [clausify(10)]. -point(x) | x * L = x. [clausify(11)]. -point(x) | L * x = L. [clausify(11)]. -point(x) | x * x ^ <= I. [clausify(11)]. point(x) | x * L != x | L * x != L | -(x * x ^ <= I). [clausify(11)]. -irreflexive(x) | x <= I'. [clausify(12)]. irreflexive(x) | -(x <= I'). [clausify(12)]. -symmetric(x) | x ^ = x. [clausify(13)]. symmetric(x) | x ^ != x. [clausify(13)]. -univalent(x) | x ^ * x <= I. [clausify(14)]. univalent(x) | -(x ^ * x <= I). [clausify(14)]. -coloringProperty(x,y) | x * x ^ <= y'. [clausify(15)]. coloringProperty(x,y) | -(x * x ^ <= y'). [clausify(15)]. symmetric(c1). [deny(16)]. irreflexive(c1). [deny(16)]. (c2 ^ * c1) * c3 != L. [deny(16)]. coloringProperty(c2,c1). [deny(16)]. point(c3). [deny(16)]. point(c4). [deny(16)]. c4 <= ((c2 ^ * c1) * c3)'. [deny(16)]. -(((c3 * c4 ^) * c4) * c3 ^ <= c1'). [deny(16)]. end_of_list. formulas(demodulators). end_of_list. ============================== PREDICATE ELIMINATION ================= Eliminating point/1 17 point(x) | x * L != x | L * x != L | -(x * x ^ <= I). [clausify(11)]. 18 -point(x) | x * L = x. [clausify(11)]. 19 -point(x) | L * x = L. [clausify(11)]. 20 -point(x) | x * x ^ <= I. [clausify(11)]. 21 point(c3). [deny(16)]. Derived: c3 * L = c3. [resolve(21,a,18,a)]. Derived: L * c3 = L. [resolve(21,a,19,a)]. Derived: c3 * c3 ^ <= I. [resolve(21,a,20,a)]. 22 point(c4). [deny(16)]. Derived: c4 * L = c4. [resolve(22,a,18,a)]. Derived: L * c4 = L. [resolve(22,a,19,a)]. Derived: c4 * c4 ^ <= I. [resolve(22,a,20,a)]. Eliminating irreflexive/1 23 irreflexive(x) | -(x <= I'). [clausify(12)]. 24 -irreflexive(x) | x <= I'. [clausify(12)]. 25 irreflexive(c1). [deny(16)]. Derived: c1 <= I'. [resolve(25,a,24,a)]. Eliminating symmetric/1 26 symmetric(x) | x ^ != x. [clausify(13)]. 27 -symmetric(x) | x ^ = x. [clausify(13)]. 28 symmetric(c1). [deny(16)]. Derived: c1 ^ = c1. [resolve(28,a,27,a)]. Eliminating univalent/1 29 univalent(x) | -(x ^ * x <= I). [clausify(14)]. 30 -univalent(x) | x ^ * x <= I. [clausify(14)]. Eliminating coloringProperty/2 31 coloringProperty(x,y) | -(x * x ^ <= y'). [clausify(15)]. 32 -coloringProperty(x,y) | x * x ^ <= y'. [clausify(15)]. 33 coloringProperty(c2,c1). [deny(16)]. Derived: c2 * c2 ^ <= c1'. [resolve(33,a,32,a)]. ============================== 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, c4, *, \/, /\, ^, ' ]). After inverse_order: Function symbol precedence: function_order([ L, O, I, c1, c2, c3, c4, \/, /\, ', *, ^ ]). 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). 34 x \/ y = y \/ x. [assumption]. 35 x /\ y = y /\ x. [assumption]. 37 (x \/ y) \/ z = x \/ (y \/ z). [copy(36),flip(a)]. 39 (x /\ y) /\ z = x /\ (y /\ z). [copy(38),flip(a)]. 40 x \/ (y /\ x) = x. [assumption]. 42 -(x <= y) | x \/ y = y. [clausify(1)]. 43 x <= y | x \/ y != y. [clausify(1)]. 44 -(x <= y) | x /\ y = x. [clausify(2)]. 45 x <= y | x /\ y != x. [clausify(2)]. 46 x /\ (y \/ z) = (x /\ y) \/ (x /\ z). [assumption]. 48 (x /\ x) \/ ((x /\ y) \/ ((x \/ y) /\ z)) = x \/ (y /\ z). [copy(47),rewrite([46(5),35(4),46(4),37(8)]),flip(a)]. 50 x \/ x' = L. [copy(49),flip(a)]. 52 x /\ x' = O. [copy(51),flip(a)]. 54 (x * y) * z = x * (y * z). [copy(53),flip(a)]. 55 x * I = x. [assumption]. 56 I * x = x. [assumption]. 57 x * y /\ z <= (x /\ z * y ^) * (y /\ x ^ * z). [assumption]. 58 -(x * y <= z) | x ^ * z' <= y'. [clausify(3)]. 59 x * y <= z | -(x ^ * z' <= y'). [clausify(3)]. 60 -(x * y <= z) | z' * y ^ <= x'. [clausify(4)]. 61 x * y <= z | -(z' * y ^ <= x'). [clausify(4)]. 63 O = x | L * (x * L) = L. [copy(62),rewrite([54(6)])]. 65 O != x | L * (x * L) != L. [copy(64),rewrite([54(6)])]. 66 (x \/ y) * z = x * z \/ y * z. [assumption]. 67 x * (y \/ z) = x * y \/ x * z. [assumption]. 68 (x * y) ^ = y ^ * x ^. [assumption]. 69 (x \/ y) ^ = x ^ \/ y ^. [assumption]. 70 (x /\ y) ^ = x ^ /\ y ^. [assumption]. 71 -(x <= y) | x * z <= y * z. [clausify(6)]. 72 -(x <= y) | z * x <= z * y. [clausify(7)]. 73 -(x <= y) | x \/ z <= y \/ z. [clausify(8)]. 74 -(x <= y) | x /\ z <= y /\ z. [clausify(9)]. 75 x ^ ^ = x. [assumption]. 76 O <= x. [assumption]. 77 x <= L. [assumption]. 78 O * x = O. [assumption]. 79 x * O = O. [assumption]. 80 -(x <= y) | -(z <= y) | x \/ z <= y. [clausify(10)]. 82 c2 ^ * (c1 * c3) != L. [copy(81),rewrite([54(6)])]. 84 c4 <= (c2 ^ * (c1 * c3))'. [copy(83),rewrite([54(7)])]. 86 -(c3 * (c4 ^ * (c4 * c3 ^)) <= c1'). [copy(85),rewrite([54(6),54(9),54(8)])]. 87 c3 * L = c3. [resolve(21,a,18,a)]. 88 L * c3 = L. [resolve(21,a,19,a)]. 89 c3 * c3 ^ <= I. [resolve(21,a,20,a)]. 90 c4 * L = c4. [resolve(22,a,18,a)]. 91 L * c4 = L. [resolve(22,a,19,a)]. 92 c4 * c4 ^ <= I. [resolve(22,a,20,a)]. 93 c1 <= I'. [resolve(25,a,24,a)]. 94 c1 ^ = c1. [resolve(28,a,27,a)]. 95 c2 * c2 ^ <= c1'. [resolve(33,a,32,a)]. 96 (x /\ y) \/ (x /\ x) = x. [back_rewrite(41),rewrite([46(2)])]. 97 -(x <= y) | x \/ x <= y. [factor(80,a,b)]. end_of_list. formulas(demodulators). 34 x \/ y = y \/ x. [assumption]. % (lex-dep) 35 x /\ y = y /\ x. [assumption]. % (lex-dep) 37 (x \/ y) \/ z = x \/ (y \/ z). [copy(36),flip(a)]. 39 (x /\ y) /\ z = x /\ (y /\ z). [copy(38),flip(a)]. 40 x \/ (y /\ x) = x. [assumption]. 46 x /\ (y \/ z) = (x /\ y) \/ (x /\ z). [assumption]. 48 (x /\ x) \/ ((x /\ y) \/ ((x \/ y) /\ z)) = x \/ (y /\ z). [copy(47),rewrite([46(5),35(4),46(4),37(8)]),flip(a)]. 50 x \/ x' = L. [copy(49),flip(a)]. 52 x /\ x' = O. [copy(51),flip(a)]. 54 (x * y) * z = x * (y * z). [copy(53),flip(a)]. 55 x * I = x. [assumption]. 56 I * x = x. [assumption]. 66 (x \/ y) * z = x * z \/ y * z. [assumption]. 67 x * (y \/ z) = x * y \/ x * z. [assumption]. 68 (x * y) ^ = y ^ * x ^. [assumption]. 69 (x \/ y) ^ = x ^ \/ y ^. [assumption]. 70 (x /\ y) ^ = x ^ /\ y ^. [assumption]. 75 x ^ ^ = x. [assumption]. 78 O * x = O. [assumption]. 79 x * O = O. [assumption]. 87 c3 * L = c3. [resolve(21,a,18,a)]. 88 L * c3 = L. [resolve(21,a,19,a)]. 90 c4 * L = c4. [resolve(22,a,18,a)]. 91 L * c4 = L. [resolve(22,a,19,a)]. 94 c1 ^ = c1. [resolve(28,a,27,a)]. 96 (x /\ y) \/ (x /\ x) = x. [back_rewrite(41),rewrite([46(2)])]. end_of_list. ============================== end of clauses for search ============= ============================== SEARCH ================================ % Starting search at 0.01 seconds. given #1 (I,wt=7): 34 x \/ y = y \/ x. [assumption]. given #2 (I,wt=7): 35 x /\ y = y /\ x. [assumption]. given #3 (I,wt=11): 37 (x \/ y) \/ z = x \/ (y \/ z). [copy(36),flip(a)]. % Operation \/ is associative-commutative; CAC redundancy checks enabled. % back CAC tautology: 98 x \/ (y \/ z) = z \/ (x \/ y). [para(37(a,1),34(a,1))]. given #4 (I,wt=11): 39 (x /\ y) /\ z = x /\ (y /\ z). [copy(38),flip(a)]. % Operation /\ is associative-commutative; CAC redundancy checks enabled. % back CAC tautology: 100 x /\ (y /\ z) = z /\ (x /\ y). [para(39(a,1),35(a,1))]. given #5 (I,wt=7): 40 x \/ (y /\ x) = x. [assumption]. given #6 (I,wt=8): 42 -(x <= y) | x \/ y = y. [clausify(1)]. given #7 (I,wt=8): 43 x <= y | x \/ y != y. [clausify(1)]. given #8 (I,wt=8): 44 -(x <= y) | x /\ y = x. [clausify(2)]. given #9 (I,wt=8): 45 x <= y | x /\ y != x. [clausify(2)]. given #10 (I,wt=13): 46 x /\ (y \/ z) = (x /\ y) \/ (x /\ z). [assumption]. given #11 (I,wt=19): 48 (x /\ x) \/ ((x /\ y) \/ ((x \/ y) /\ z)) = x \/ (y /\ z). [copy(47),rewrite([46(5),35(4),46(4),37(8)]),flip(a)]. given #12 (I,wt=6): 50 x \/ x' = L. [copy(49),flip(a)]. given #13 (I,wt=6): 52 x /\ x' = O. [copy(51),flip(a)]. given #14 (I,wt=11): 54 (x * y) * z = x * (y * z). [copy(53),flip(a)]. given #15 (I,wt=5): 55 x * I = x. [assumption]. given #16 (I,wt=5): 56 I * x = x. [assumption]. given #17 (I,wt=19): 57 x * y /\ z <= (x /\ z * y ^) * (y /\ x ^ * z). [assumption]. given #18 (I,wt=13): 58 -(x * y <= z) | x ^ * z' <= y'. [clausify(3)]. given #19 (I,wt=13): 59 x * y <= z | -(x ^ * z' <= y'). [clausify(3)]. given #20 (I,wt=13): 60 -(x * y <= z) | z' * y ^ <= x'. [clausify(4)]. given #21 (I,wt=13): 61 x * y <= z | -(z' * y ^ <= x'). [clausify(4)]. given #22 (I,wt=10): 63 O = x | L * (x * L) = L. [copy(62),rewrite([54(6)])]. given #23 (I,wt=10): 65 O != x | L * (x * L) != L. [copy(64),rewrite([54(6)])]. given #24 (I,wt=13): 66 (x \/ y) * z = x * z \/ y * z. [assumption]. given #25 (I,wt=13): 67 x * (y \/ z) = x * y \/ x * z. [assumption]. given #26 (I,wt=10): 68 (x * y) ^ = y ^ * x ^. [assumption]. given #27 (I,wt=10): 69 (x \/ y) ^ = x ^ \/ y ^. [assumption]. given #28 (I,wt=10): 70 (x /\ y) ^ = x ^ /\ y ^. [assumption]. given #29 (I,wt=10): 71 -(x <= y) | x * z <= y * z. [clausify(6)]. given #30 (I,wt=10): 72 -(x <= y) | z * x <= z * y. [clausify(7)]. given #31 (I,wt=10): 73 -(x <= y) | x \/ z <= y \/ z. [clausify(8)]. given #32 (I,wt=10): 74 -(x <= y) | x /\ z <= y /\ z. [clausify(9)]. given #33 (I,wt=5): 75 x ^ ^ = x. [assumption]. given #34 (I,wt=3): 76 O <= x. [assumption]. given #35 (I,wt=3): 77 x <= L. [assumption]. given #36 (I,wt=5): 78 O * x = O. [assumption]. given #37 (I,wt=5): 79 x * O = O. [assumption]. given #38 (I,wt=11): 80 -(x <= y) | -(z <= y) | x \/ z <= y. [clausify(10)]. given #39 (I,wt=8): 82 c2 ^ * (c1 * c3) != L. [copy(81),rewrite([54(6)])]. given #40 (I,wt=9): 84 c4 <= (c2 ^ * (c1 * c3))'. [copy(83),rewrite([54(7)])]. given #41 (I,wt=12): 86 -(c3 * (c4 ^ * (c4 * c3 ^)) <= c1'). [copy(85),rewrite([54(6),54(9),54(8)])]. given #42 (I,wt=5): 87 c3 * L = c3. [resolve(21,a,18,a)]. given #43 (I,wt=5): 88 L * c3 = L. [resolve(21,a,19,a)]. given #44 (I,wt=6): 89 c3 * c3 ^ <= I. [resolve(21,a,20,a)]. given #45 (I,wt=5): 90 c4 * L = c4. [resolve(22,a,18,a)]. given #46 (I,wt=5): 91 L * c4 = L. [resolve(22,a,19,a)]. given #47 (I,wt=6): 92 c4 * c4 ^ <= I. [resolve(22,a,20,a)]. given #48 (I,wt=4): 93 c1 <= I'. [resolve(25,a,24,a)]. given #49 (I,wt=4): 94 c1 ^ = c1. [resolve(28,a,27,a)]. given #50 (I,wt=7): 95 c2 * c2 ^ <= c1'. [resolve(33,a,32,a)]. given #51 (I,wt=9): 96 (x /\ y) \/ (x /\ x) = x. [back_rewrite(41),rewrite([46(2)])]. given #52 (A,wt=11): 99 x \/ (y \/ z) = y \/ (x \/ z). [para(34(a,1),37(a,1,1)),rewrite([37(2)])]. given #53 (F,wt=3): 165 O != L. [ur(65,a,56,a(flip)),rewrite([79(4),78(4),79(3)])]. given #54 (F,wt=3): 248 c3 != O. [para(87(a,1),65(b,1,2)),rewrite([88(6)]),flip(a),xx(b)]. given #55 (F,wt=3): 271 c4 != O. [para(90(a,1),65(b,1,2)),rewrite([91(6)]),flip(a),xx(b)]. given #56 (F,wt=8): 167 I != O | L * L != L. [para(56(a,1),65(b,1,2)),flip(a)]. given #57 (T,wt=5): 208 O /\ x = O. [resolve(76,a,44,a)]. given #58 (T,wt=5): 209 O \/ x = x. [resolve(76,a,42,a)]. given #59 (T,wt=4): 346 O' = L. [para(209(a,1),50(a,1))]. given #60 (T,wt=5): 211 x <= y \/ x. [back_rewrite(207),rewrite([209(2)])]. given #61 (A,wt=11): 101 x /\ (y /\ z) = y /\ (x /\ z). [para(35(a,1),39(a,1,1)),rewrite([39(2)])]. given #62 (F,wt=13): 240 -(c1'' * (c3 * (c4 ^ * c4)) <= c3'). [ur(61,a,86,a),rewrite([68(11),68(8),75(6),75(10),54(9)])]. given #63 (F,wt=14): 166 x * y != O | L * (x * (y * L)) != L. [para(54(a,1),65(b,1,2)),flip(a)]. given #64 (F,wt=12): 372 x * c3 != O | L * (x * c3) != L. [para(87(a,1),166(b,1,2,2))]. given #65 (F,wt=12): 373 x * c4 != O | L * (x * c4) != L. [para(90(a,1),166(b,1,2,2))]. given #66 (T,wt=3): 360 x <= x. [para(209(a,1),211(a,2))]. given #67 (T,wt=5): 220 x /\ L = x. [resolve(77,a,44,a)]. given #68 (T,wt=5): 221 x \/ L = L. [resolve(77,a,42,a)]. given #69 (T,wt=5): 319 x /\ x = x. [para(52(a,1),96(a,1,1)),rewrite([209(3)])]. given #70 (A,wt=7): 102 x \/ (x /\ y) = x. [para(35(a,1),40(a,1,2))]. given #71 (F,wt=15): 241 -(c3 ^ * c1'' <= (c4 ^ * (c4 * c3 ^))'). [ur(59,a,86,a)]. given #72 (F,wt=15): 243 c1' \/ c3 * (c4 ^ * (c4 * c3 ^)) != c1'. [ur(43,a,86,a),rewrite([34(12)])]. given #73 (F,wt=16): 364 -(c3'' * (c4 ^ * (c4 * c3 ^)) <= c1'''). [ur(61,a,240,a),rewrite([68(10),68(8),75(8),54(10)])]. given #74 (F,wt=16): 365 -(c1'' ^ * c3'' <= (c3 * (c4 ^ * c4))'). [ur(59,a,240,a)]. given #75 (T,wt=5): 323 x \/ x = x. [back_rewrite(123),rewrite([319(1),319(2),102(3),34(2),102(2)])]. given #76 (T,wt=5): 326 x /\ y <= x. [back_rewrite(316),rewrite([319(2),319(3)]),xx(b)]. given #77 (T,wt=5): 343 x /\ O = O. [para(208(a,1),35(a,1)),flip(a)]. given #78 (T,wt=5): 344 x \/ O = x. [para(208(a,1),40(a,1,2))]. given #79 (A,wt=11): 103 x \/ ((y /\ x) \/ z) = x \/ z. [para(40(a,1),37(a,1,1)),flip(a)]. given #80 (F,wt=16): 367 c3' \/ c1'' * (c3 * (c4 ^ * c4)) != c3'. [ur(43,a,240,a),rewrite([34(13)])]. given #81 (F,wt=16): 374 x * (y * c3) != O | L * (x * (y * c3)) != L. [para(54(a,1),372(b,1,2)),rewrite([54(3)])]. given #82 (F,wt=12): 448 x * L != O | L * (x * L) != L. [para(88(a,1),374(b,1,2,2)),rewrite([88(3)])]. given #83 (F,wt=16): 376 x * (y * c4) != O | L * (x * (y * c4)) != L. [para(54(a,1),373(b,1,2)),rewrite([54(3)])]. given #84 (T,wt=5): 356 x <= x \/ y. [para(34(a,1),211(a,2))]. given #85 (T,wt=5): 358 x /\ y <= y. [para(40(a,1),211(a,2))]. given #86 (T,wt=5): 382 L /\ x = x. [para(220(a,1),35(a,1)),flip(a)]. given #87 (T,wt=4): 469 L' = O. [para(382(a,1),52(a,1))]. given #88 (A,wt=9): 105 x \/ (y /\ (z /\ x)) = x. [para(39(a,1),40(a,1,2))]. given #89 (F,wt=16): 411 -(c3 * (c4 ^ * (c4 * c3 ^))'' <= c1'''). [ur(59,a,241,a),rewrite([75(3)])]. given #90 (F,wt=16): 450 x * (y * L) != O | L * (x * (y * L)) != L. [para(54(a,1),448(b,1,2)),rewrite([54(3)])]. given #91 (F,wt=17): 414 -(c1'''' * (c3 * (c4 ^ * c4)) <= c3'''). [ur(61,a,364,a),rewrite([68(13),68(10),75(8),75(12),54(11)])]. given #92 (F,wt=17): 419 -(c1'' * (c3 * (c4 ^ * c4))'' <= c3'''). [ur(59,a,365,a),rewrite([75(5)])]. given #93 (T,wt=5): 383 L \/ x = L. [para(220(a,1),40(a,1,2))]. given #94 (T,wt=6): 296 c1 /\ I' = c1. [resolve(93,a,44,a)]. given #95 (T,wt=6): 432 x <= O | O != x. [para(343(a,1),45(b,1))]. given #96 (T,wt=6): 468 L <= x | L != x. [para(382(a,1),45(b,1)),flip(b)]. given #97 (A,wt=8): 106 x <= y | y \/ x != y. [para(34(a,1),43(b,1))]. given #98 (F,wt=18): 177 x \/ y != O | L * (x * L) \/ L * (y * L) != L. [para(66(a,1),65(b,1,2)),rewrite([67(10)]),flip(a)]. given #99 (F,wt=5): 525 c3 \/ x != O. [para(87(a,1),177(b,1,1,2)),rewrite([88(7),383(10)]),xx(b)]. given #100 (F,wt=3): 529 -(c3 <= O). [ur(42,b,525,a)]. given #101 (F,wt=5): 526 x \/ c3 != O. [para(87(a,1),177(b,1,2,2)),rewrite([88(11),34(10),383(10)]),xx(b)]. given #102 (T,wt=7): 137 x <= x' | O != x. [para(52(a,1),45(b,1))]. given #103 (T,wt=7): 216 x * y <= x * L. [resolve(77,a,72,a)]. given #104 (T,wt=5): 541 x <= x * L. [para(55(a,1),216(a,1))]. given #105 (T,wt=5): 544 c3 * x <= c3. [para(87(a,1),216(a,2))]. given #106 (A,wt=12): 107 x \/ y <= z | x \/ (y \/ z) != z. [para(37(a,1),43(b,1))]. given #107 (F,wt=5): 527 c4 \/ x != O. [para(90(a,1),177(b,1,1,2)),rewrite([91(7),383(10)]),xx(b)]. given #108 (F,wt=3): 578 -(c4 <= O). [ur(42,b,527,a)]. given #109 (F,wt=5): 528 x \/ c4 != O. [para(90(a,1),177(b,1,2,2)),rewrite([91(11),34(10),383(10)]),xx(b)]. given #110 (F,wt=7): 530 x \/ (c3 \/ y) != O. [para(99(a,1),525(a,1))]. given #111 (T,wt=5): 545 c4 * x <= c4. [para(90(a,1),216(a,2))]. given #112 (T,wt=7): 217 x * y <= L * y. [resolve(77,a,71,a)]. given #113 (T,wt=5): 600 x <= L * x. [para(56(a,1),217(a,1))]. given #114 (T,wt=5): 603 c3 <= L * L. [para(87(a,1),217(a,1))]. given #115 (A,wt=10): 108 x <= y /\ x | y /\ x != x. [para(40(a,1),43(b,1)),flip(b)]. given #116 (F,wt=7): 531 x \/ (y \/ c3) != O. [para(37(a,1),526(a,1))]. given #117 (F,wt=7): 579 x \/ (c4 \/ y) != O. [para(99(a,1),527(a,1))]. given #118 (F,wt=7): 580 x \/ (y \/ c4) != O. [para(37(a,1),528(a,1))]. given #119 (F,wt=9): 581 x \/ (y \/ (c3 \/ z)) != O. [para(37(a,1),530(a,1))]. given #120 (T,wt=5): 604 c4 <= L * L. [para(90(a,1),217(a,1))]. given #121 (T,wt=7): 249 c3 \/ c3 * x = c3. [para(87(a,1),67(a,2,2)),rewrite([221(3),87(3),34(5)]),flip(a)]. given #122 (T,wt=7): 263 I' * c3 <= c3'. [resolve(89,a,60,a),rewrite([75(5)])]. given #123 (T,wt=7): 272 c4 \/ c4 * x = c4. [para(90(a,1),67(a,2,2)),rewrite([221(3),90(3),34(5)]),flip(a)]. given #124 (A,wt=8): 109 x <= y | y /\ x != x. [para(35(a,1),45(b,1))]. given #125 (F,wt=9): 627 x \/ (y \/ (z \/ c3)) != O. [para(37(a,1),531(a,1,2))]. given #126 (F,wt=9): 628 x \/ (y \/ (c4 \/ z)) != O. [para(37(a,1),579(a,1))]. given #127 (F,wt=9): 629 x \/ (y \/ (z \/ c4)) != O. [para(37(a,1),580(a,1,2))]. given #128 (F,wt=10): 520 I \/ x != O | L * L != L. [para(56(a,1),177(b,1,1,2)),rewrite([505(12)])]. given #129 (T,wt=7): 286 I' * c4 <= c4'. [resolve(92,a,60,a),rewrite([75(5)])]. given #130 (T,wt=7): 297 c1 \/ I' = I'. [resolve(93,a,42,a)]. given #131 (T,wt=7): 357 x <= y \/ (z \/ x). [para(37(a,1),211(a,2))]. given #132 (T,wt=7): 431 x /\ (y /\ z) <= y. [para(101(a,1),326(a,1))]. given #133 (A,wt=14): 110 x /\ y <= z | x /\ (y /\ z) != x /\ y. [para(39(a,1),45(b,1))]. given #134 (F,wt=10): 521 x \/ I != O | L * L != L. [para(56(a,1),177(b,1,2,2)),rewrite([34(12),505(12)])]. given #135 (F,wt=11): 630 x \/ (y \/ (z \/ (c3 \/ u))) != O. [para(37(a,1),581(a,1,2))]. given #136 (F,wt=11): 669 x \/ (y \/ (z \/ (u \/ c3))) != O. [para(37(a,1),627(a,1,2,2))]. given #137 (F,wt=11): 670 x \/ (y \/ (z \/ (c4 \/ u))) != O. [para(37(a,1),628(a,1,2))]. given #138 (T,wt=6): 723 x /\ c1 <= I'. [para(296(a,1),110(b,1,2)),xx(b)]. given #139 (T,wt=6): 735 c1 /\ x <= I'. [para(35(a,1),723(a,1))]. given #140 (T,wt=7): 461 x <= y \/ (x \/ z). [para(99(a,1),356(a,2))]. given #141 (T,wt=6): 755 c1 <= x \/ I'. [para(297(a,1),461(a,2,2))]. given #142 (A,wt=13): 111 (x \/ y) /\ z = (z /\ x) \/ (z /\ y). [para(46(a,1),35(a,1)),flip(a)]. given #143 (F,wt=11): 671 x \/ (y \/ (z \/ (u \/ c4))) != O. [para(37(a,1),629(a,1,2,2))]. given #144 (F,wt=12): 672 x \/ (I \/ y) != O | L * L != L. [para(99(a,1),520(a,1))]. given #145 (F,wt=12): 724 x \/ (y \/ I) != O | L * L != L. [para(37(a,1),521(a,1))]. given #146 (F,wt=13): 725 x \/ (y \/ (z \/ (u \/ (c3 \/ w)))) != O. [para(37(a,1),630(a,1,2,2))]. given #147 (T,wt=6): 762 c1 <= I' \/ x. [para(34(a,1),755(a,2))]. given #148 (T,wt=7): 466 x /\ (y /\ z) <= z. [para(39(a,1),358(a,1))]. given #149 (T,wt=7): 508 c1 /\ I' ^ = c1. [para(296(a,1),70(a,1,1)),rewrite([94(2),94(3)]),flip(a)]. given #150 (T,wt=5): 816 c1 <= I' ^. [resolve(508,a,45,b)]. given #151 (A,wt=17): 112 ((x /\ y) \/ (x /\ z)) /\ u = x /\ ((y \/ z) /\ u). [para(46(a,1),39(a,1,1))]. given #152 (F,wt=13): 726 x \/ (y \/ (z \/ (u \/ (w \/ c3)))) != O. [para(37(a,1),669(a,1,2,2,2))]. given #153 (F,wt=13): 727 x \/ (y \/ (z \/ (u \/ (c4 \/ w)))) != O. [para(37(a,1),670(a,1,2,2))]. given #154 (F,wt=13): 798 x \/ (y \/ (z \/ (u \/ (w \/ c4)))) != O. [para(37(a,1),671(a,1,2,2,2))]. given #155 (F,wt=14): 799 x \/ (y \/ (I \/ z)) != O | L * L != L. [para(37(a,1),672(a,1))]. given #156 (T,wt=7): 514 x' <= x | L != x. [para(50(a,1),106(b,1))]. given #157 (T,wt=7): 554 x /\ x * L = x. [resolve(541,a,44,a)]. given #158 (T,wt=5): 897 L * L = L. [para(554(a,1),382(a,1)),flip(a)]. given #159 (T,wt=7): 611 x /\ L * x = x. [resolve(600,a,44,a)]. given #160 (A,wt=13): 113 (x /\ y) \/ (x /\ (z /\ y)) = x /\ y. [para(40(a,1),46(a,1,2)),flip(a)]. given #161 (F,wt=3): 910 I != O. [back_rewrite(167),rewrite([897(6)]),xx(b)]. given #162 (F,wt=5): 906 x \/ I != O. [back_rewrite(521),rewrite([897(7)]),xx(b)]. given #163 (F,wt=5): 907 I \/ x != O. [back_rewrite(520),rewrite([897(7)]),xx(b)]. given #164 (F,wt=3): 939 -(I <= O). [ur(42,b,907,a)]. given #165 (T,wt=7): 696 x /\ y <= z \/ y. [para(40(a,1),357(a,2,2))]. given #166 (T,wt=7): 698 x /\ y <= z \/ x. [para(102(a,1),357(a,2,2))]. given #167 (T,wt=7): 701 c3 * x <= y \/ c3. [para(249(a,1),357(a,2,2))]. given #168 (T,wt=7): 702 c4 * x <= y \/ c4. [para(272(a,1),357(a,2,2))]. given #169 (A,wt=14): 114 x <= y \/ z | (x /\ y) \/ (x /\ z) != x. [para(46(a,1),45(b,1))]. given #170 (F,wt=7): 904 x \/ (y \/ I) != O. [back_rewrite(724),rewrite([897(8)]),xx(b)]. given #171 (F,wt=7): 905 x \/ (I \/ y) != O. [back_rewrite(672),rewrite([897(8)]),xx(b)]. given #172 (F,wt=9): 902 x \/ (y \/ (z \/ I)) != O. [back_rewrite(800),rewrite([897(9)]),xx(b)]. given #173 (F,wt=9): 903 x \/ (y \/ (I \/ z)) != O. [back_rewrite(799),rewrite([897(9)]),xx(b)]. given #174 (T,wt=7): 754 x /\ y <= y \/ z. [para(103(a,1),461(a,2))]. given #175 (T,wt=7): 822 x /\ c1 <= I' ^. [para(508(a,1),110(b,1,2)),xx(b)]. given #176 (T,wt=7): 900 x /\ y <= y * L. [para(554(a,1),110(b,1,2)),xx(b)]. given #177 (T,wt=6): 1037 c1 <= I' * L. [para(296(a,1),900(a,1))]. given #178 (A,wt=10): 130 x \/ (y \/ (x \/ y)') = L. [para(50(a,1),37(a,1)),flip(a)]. given #179 (F,wt=11): 901 x \/ (y \/ (z \/ (I \/ u))) != O. [back_rewrite(888),rewrite([897(10)]),xx(b)]. given #180 (F,wt=11): 1006 x \/ (y \/ (z \/ (u \/ I))) != O. [para(37(a,1),902(a,1,2,2))]. given #181 (F,wt=13): 1061 x \/ (y \/ (z \/ (u \/ (I \/ w)))) != O. [para(37(a,1),901(a,1,2,2))]. given #182 (F,wt=13): 1062 x \/ (y \/ (z \/ (u \/ (w \/ I)))) != O. [para(37(a,1),1006(a,1,2,2,2))]. given #183 (T,wt=7): 924 x /\ y <= L * y. [para(611(a,1),110(b,1,2)),xx(b)]. given #184 (T,wt=6): 1076 c1 <= L * I'. [para(296(a,1),924(a,1))]. given #185 (T,wt=7): 949 x /\ c3 * y <= c3. [para(249(a,1),696(a,2))]. given #186 (T,wt=7): 950 x /\ c4 * y <= c4. [para(272(a,1),696(a,2))]. given #187 (A,wt=8): 131 x <= x' | x' != L. [para(50(a,1),43(b,1)),flip(b)]. given #188 (F,wt=15): 801 x \/ (y \/ (z \/ (u \/ (w \/ (c3 \/ v5))))) != O. [para(37(a,1),725(a,1,2,2,2))]. given #189 (F,wt=15): 885 x \/ (y \/ (z \/ (u \/ (w \/ (v5 \/ c3))))) != O. [para(37(a,1),726(a,1,2,2,2,2))]. given #190 (F,wt=15): 886 x \/ (y \/ (z \/ (u \/ (w \/ (c4 \/ v5))))) != O. [para(37(a,1),727(a,1,2,2,2))]. given #191 (F,wt=15): 887 x \/ (y \/ (z \/ (u \/ (w \/ (v5 \/ c4))))) != O. [para(37(a,1),798(a,1,2,2,2,2))]. given #192 (T,wt=7): 951 c1 <= x \/ I' ^. [para(508(a,1),696(a,1))]. given #193 (T,wt=7): 952 x <= y \/ x * L. [para(554(a,1),696(a,1))]. given #194 (T,wt=7): 953 x <= y \/ L * x. [para(611(a,1),696(a,1))]. given #195 (T,wt=7): 960 x /\ y <= x \/ z. [para(34(a,1),698(a,2))]. given #196 (A,wt=10): 135 x /\ (y /\ (x /\ y)') = O. [para(52(a,1),39(a,1)),flip(a)]. given #197 (F,wt=15): 1063 x \/ (y \/ (z \/ (u \/ (w \/ (I \/ v5))))) != O. [para(37(a,1),1061(a,1,2,2,2))]. given #198 (F,wt=15): 1064 x \/ (y \/ (z \/ (u \/ (w \/ (v5 \/ I))))) != O. [para(37(a,1),1062(a,1,2,2,2,2))]. given #199 (F,wt=17): 1106 x \/ (y \/ (z \/ (u \/ (w \/ (v5 \/ (c3 \/ v6)))))) != O. [para(37(a,1),801(a,1,2,2,2,2))]. given #200 (F,wt=17): 1107 x \/ (y \/ (z \/ (u \/ (w \/ (v5 \/ (v6 \/ c3)))))) != O. [para(37(a,1),885(a,1,2,2,2,2,2))]. given #201 (T,wt=7): 967 c3 * x /\ y <= c3. [para(249(a,1),698(a,2))]. given #202 (T,wt=7): 968 c4 * x /\ y <= c4. [para(272(a,1),698(a,2))]. given #203 (T,wt=7): 979 c3 * x <= c3 \/ y. [para(34(a,1),701(a,2))]. given #204 (T,wt=7): 991 c4 * x <= c4 \/ y. [para(34(a,1),702(a,2))]. given #205 (A,wt=25): 139 x * y /\ (z /\ (x /\ z * y ^) * (y /\ x ^ * z)) = x * y /\ z. [resolve(57,a,44,a),rewrite([39(10)])]. given #206 (F,wt=17): 1108 x \/ (y \/ (z \/ (u \/ (w \/ (v5 \/ (c4 \/ v6)))))) != O. [para(37(a,1),886(a,1,2,2,2,2))]. given #207 (F,wt=17): 1109 x \/ (y \/ (z \/ (u \/ (w \/ (v5 \/ (v6 \/ c4)))))) != O. [para(37(a,1),887(a,1,2,2,2,2,2))]. given #208 (F,wt=17): 1162 x \/ (y \/ (z \/ (u \/ (w \/ (v5 \/ (I \/ v6)))))) != O. [para(37(a,1),1063(a,1,2,2,2,2))]. given #209 (F,wt=17): 1163 x \/ (y \/ (z \/ (u \/ (w \/ (v5 \/ (v6 \/ I)))))) != O. [para(37(a,1),1064(a,1,2,2,2,2,2))]. given #210 (T,wt=7): 1003 c1 <= I' ^ \/ x. [para(508(a,1),114(b,1,1)),rewrite([102(10)]),xx(b)]. given #211 (T,wt=7): 1004 x <= x * L \/ y. [para(554(a,1),114(b,1,1)),rewrite([102(6)]),xx(b)]. given #212 (T,wt=7): 1005 x <= L * x \/ y. [para(611(a,1),114(b,1,1)),rewrite([102(6)]),xx(b)]. given #213 (T,wt=7): 1023 c1 /\ x <= I' ^. [para(35(a,1),822(a,1))]. given #214 (A,wt=33): 140 (x * y /\ z) \/ (x /\ z * y ^) * (y /\ x ^ * z) = (x /\ z * y ^) * (y /\ x ^ * z). [resolve(57,a,42,a)]. given #215 (F,wt=18): 368 x * (y * z) != O | L * (x * (y * (z * L))) != L. [para(54(a,1),166(b,1,2,2))]. given #216 (F,wt=18): 410 -((c4 ^ * (c4 * c3 ^))'' * c1'' ^ <= c3 ^'). [ur(61,a,241,a)]. given #217 (F,wt=18): 517 x \/ y != O | L * (y * L) \/ L * (x * L) != L. [para(34(a,1),177(b,1))]. given #218 (F,wt=18): 1352 O != x | L * (x * L) \/ L * ((y /\ x) * L) != L. [para(40(a,1),517(a,1)),rewrite([34(12)]),flip(a)]. given #219 (T,wt=7): 1032 x /\ y <= x * L. [para(35(a,1),900(a,1))]. given #220 (T,wt=7): 1038 c1 <= I' ^ * L. [para(508(a,1),900(a,1))]. given #221 (T,wt=7): 1039 x <= L * (x * L). [para(611(a,1),900(a,1)),rewrite([54(4)])]. given #222 (T,wt=7): 1072 x /\ y <= L * x. [para(35(a,1),924(a,1))]. given #223 (A,wt=19): 141 x /\ y * z <= (y /\ x * z ^) * (z /\ y ^ * x). [para(35(a,1),57(a,1))]. given #224 (F,wt=12): 1364 x' != O | L * (x' * L) != L. [para(52(a,1),1352(b,1,2,2,1)),rewrite([78(12),79(11),34(10),209(10)]),flip(a)]. given #225 (F,wt=12): 1368 L * x != O | L * (x * L) != L. [para(611(a,1),1352(b,1,2,2,1)),rewrite([54(9),911(10),323(13)]),flip(a)]. given #226 (F,wt=16): 1443 L * (x * y) != O | L * (x * (y * L)) != L. [para(54(a,1),1368(b,1,2))]. given #227 (F,wt=14): 1448 L * (x * c3) != O | L * (x * c3) != L. [para(87(a,1),1443(b,1,2,2))]. given #228 (T,wt=7): 1077 c1 <= L * I' ^. [para(508(a,1),924(a,1))]. given #229 (T,wt=8): 186 I ^ * x ^ = x ^. [para(55(a,1),68(a,1,1)),flip(a)]. given #230 (T,wt=6): 1468 I ^ * x = x. [para(75(a,1),186(a,1,2)),rewrite([75(5)])]. given #231 (T,wt=4): 1483 I ^ = I. [para(1468(a,1),55(a,1)),flip(a)]. given #232 (A,wt=19): 142 x * y /\ z <= (z * y ^ /\ x) * (y /\ x ^ * z). [para(35(a,1),57(a,2,1))]. given #233 (F,wt=14): 1449 L * (x * c4) != O | L * (x * c4) != L. [para(90(a,1),1443(b,1,2,2))]. given #234 (F,wt=14): 1450 L * (x * L) != O | L * (x * L) != L. [para(897(a,1),1443(b,1,2,2))]. given #235 (F,wt=18): 1357 O != x | L * (x * L) \/ L * ((x /\ y) * L) != L. [para(102(a,1),517(a,1)),rewrite([34(12)]),flip(a)]. given #236 (F,wt=10): 1533 c1 != O | L * (c1 * L) != L. [para(296(a,1),1357(b,1,2,2,1)),rewrite([323(14)]),flip(a)]. given #237 (T,wt=8): 210 x /\ (x' /\ y) = O. [back_rewrite(134),rewrite([208(5)])]. given #238 (T,wt=8): 223 O ^ * x' <= y'. [para(78(a,1),58(a,1)),unit_del(a,76)]. given #239 (T,wt=7): 1552 O ^ * L <= x'. [para(346(a,1),223(a,1,2))]. given #240 (T,wt=6): 1563 O ^ * L <= O. [para(469(a,1),1552(a,2))]. given #241 (A,wt=19): 143 x * y /\ z <= (x /\ z * y ^) * (x ^ * z /\ y). [para(35(a,1),57(a,2,2))]. given #242 (F,wt=16): 1541 x' /\ y != O | L * ((x' /\ y) * L) != L. [para(210(a,1),1352(b,1,2,2,1)),rewrite([78(14),79(13),34(12),209(12)]),flip(a)]. given #243 (F,wt=16): 1602 x' /\ y != O | L * ((y /\ x') * L) != L. [para(35(a,1),1541(b,1,2,1))]. given #244 (F,wt=18): 1360 I' != O | L * (c1 * L) \/ L * (I' * L) != L. [para(297(a,1),517(a,1)),rewrite([34(16)])]. given #245 (F,wt=18): 1451 L * (x * (y * c3)) != O | L * (x * (y * c3)) != L. [para(54(a,1),1448(a,1,2)),rewrite([54(11)])]. given #246 (T,wt=6): 1571 O ^ * L = O. [resolve(1563,a,44,a),rewrite([35(6),208(6)]),flip(a)]. given #247 (T,wt=4): 1612 O ^ = O. [para(1571(a,1),63(b,1,2)),rewrite([79(7)]),flip(a),unit_del(b,165)]. given #248 (T,wt=7): 1606 c1 = O | I' != O. [para(63(b,1),1360(b,1,1)),rewrite([383(15)]),flip(a),xx(c)]. given #249 (T,wt=8): 250 L ^ * c3 ^ = c3 ^. [para(87(a,1),68(a,1,1)),flip(a)]. given #250 (A,wt=26): 144 (x /\ y) * z /\ u <= (x /\ (y /\ u * z ^)) * (z /\ (x ^ /\ y ^) * u). [para(39(a,1),57(a,2,1)),rewrite([70(9)])]. given #251 (F,wt=18): 1523 L * (x * (y * c4)) != O | L * (x * (y * c4)) != L. [para(54(a,1),1449(a,1,2)),rewrite([54(11)])]. given #252 (F,wt=18): 1525 L * (x * (y * L)) != O | L * (x * (y * L)) != L. [para(54(a,1),1450(a,1,2)),rewrite([54(11)])]. given #253 (F,wt=19): 415 -(c3'' ^ * c1'''' <= (c4 ^ * (c4 * c3 ^))'). [ur(59,a,364,a)]. given #254 (F,wt=19): 418 -((c3 * (c4 ^ * c4))'' * c3'' ^ <= c1'' ^'). [ur(61,a,365,a)]. given #255 (T,wt=7): 1622 c3 ^ <= L ^ * L. [para(250(a,1),216(a,1))]. given #256 (T,wt=8): 256 c3 ^ * L ^ = L ^. [para(88(a,1),68(a,1,1)),flip(a)]. given #257 (T,wt=7): 1705 L ^ <= c3 ^ * L. [para(256(a,1),216(a,1))]. given #258 (T,wt=8): 261 x * (c3 * c3 ^) <= x. [resolve(89,a,72,a),rewrite([55(7)])]. given #259 (A,wt=26): 145 x * (y /\ z) /\ u <= (x /\ u * (y ^ /\ z ^)) * (y /\ (z /\ x ^ * u)). [para(39(a,1),57(a,2,2)),rewrite([70(5)])]. given #260 (F,wt=19): 488 -(c1'''' * (c4 ^ * (c4 * c3 ^))'' ^ <= c3'). [ur(61,a,411,a)]. given #261 (F,wt=19): 489 -(c3 ^ * c1'''' <= (c4 ^ * (c4 * c3 ^))'''). [ur(59,a,411,a)]. given #262 (F,wt=19): 1164 x \/ (y \/ (z \/ (u \/ (w \/ (v5 \/ (v6 \/ (c3 \/ v7))))))) != O. [para(37(a,1),1106(a,1,2,2,2,2,2))]. given #263 (F,wt=19): 1165 x \/ (y \/ (z \/ (u \/ (w \/ (v5 \/ (v6 \/ (v7 \/ c3))))))) != O. [para(37(a,1),1107(a,1,2,2,2,2,2,2))]. given #264 (T,wt=8): 262 c3 * (c3 ^ * x) <= x. [resolve(89,a,71,a),rewrite([54(5),56(7)])]. given #265 (T,wt=7): 1798 c3 * L ^ <= L ^. [para(256(a,1),262(a,1,2))]. given #266 (T,wt=8): 266 I \/ c3 * c3 ^ = I. [resolve(89,a,42,a),rewrite([34(6)])]. given #267 (T,wt=8): 273 L ^ * c4 ^ = c4 ^. [para(90(a,1),68(a,1,1)),flip(a)]. given #268 (A,wt=67): 146 (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(46(a,1),57(a,1)),rewrite([66(8),46(11),67(15),46(18),67(20),66(16),66(31),37(36)])]. given #269 (F,wt=19): 1260 x \/ (y \/ (z \/ (u \/ (w \/ (v5 \/ (v6 \/ (c4 \/ v7))))))) != O. [para(37(a,1),1108(a,1,2,2,2,2,2))]. given #270 (F,wt=19): 1261 x \/ (y \/ (z \/ (u \/ (w \/ (v5 \/ (v6 \/ (v7 \/ c4))))))) != O. [para(37(a,1),1109(a,1,2,2,2,2,2,2))]. given #271 (F,wt=19): 1262 x \/ (y \/ (z \/ (u \/ (w \/ (v5 \/ (v6 \/ (I \/ v7))))))) != O. [para(37(a,1),1162(a,1,2,2,2,2,2))]. given #272 (F,wt=19): 1263 x \/ (y \/ (z \/ (u \/ (w \/ (v5 \/ (v6 \/ (v7 \/ I))))))) != O. [para(37(a,1),1163(a,1,2,2,2,2,2,2))]. given #273 (T,wt=7): 1823 c4 ^ <= L ^ * L. [para(273(a,1),216(a,1))]. given #274 (T,wt=8): 279 c4 ^ * L ^ = L ^. [para(91(a,1),68(a,1,1)),flip(a)]. given #275 (T,wt=7): 1936 L ^ <= c4 ^ * L. [para(279(a,1),216(a,1))]. given #276 (T,wt=8): 284 x * (c4 * c4 ^) <= x. [resolve(92,a,72,a),rewrite([55(7)])]. given #277 (A,wt=26): 147 x * (y * z) /\ u <= (x * y /\ u * z ^) * (z /\ y ^ * (x ^ * u)). [para(54(a,1),57(a,1,1)),rewrite([68(9),54(11)])]. given #278 (F,wt=19): 1349 -(c3 ^'' * c1'' <= (c4 ^ * (c4 * c3 ^))'''). [ur(61,a,410,a),rewrite([75(9)])]. given #279 (F,wt=20): 445 x * (y * (z * c3)) != O | L * (x * (y * (z * c3))) != L. [para(54(a,1),374(b,1,2,2)),rewrite([54(3)])]. given #280 (F,wt=20): 452 x * (y * (z * c4)) != O | L * (x * (y * (z * c4))) != L. [para(54(a,1),376(b,1,2,2)),rewrite([54(3)])]. given #281 (F,wt=20): 492 x * (y * (z * L)) != O | L * (x * (y * (z * L))) != L. [para(54(a,1),450(b,1,2,2)),rewrite([54(3)])]. given #282 (T,wt=8): 285 c4 * (c4 ^ * x) <= x. [resolve(92,a,71,a),rewrite([54(5),56(7)])]. given #283 (T,wt=7): 2052 c4 * L ^ <= L ^. [para(279(a,1),285(a,1,2))]. given #284 (T,wt=8): 289 I \/ c4 * c4 ^ = I. [resolve(92,a,42,a),rewrite([34(6)])]. given #285 (T,wt=8): 292 c1 /\ x <= I' /\ x. [resolve(93,a,74,a)]. given #286 (A,wt=25): 148 x * y /\ z * u <= (x /\ z * (u * y ^)) * (y /\ x ^ * (z * u)). [para(54(a,1),57(a,2,1,2))]. given #287 (F,wt=20): 496 -(c3'''' * (c4 ^ * (c4 * c3 ^)) <= c1'''''). [ur(61,a,414,a),rewrite([68(12),68(10),75(10),54(12)])]. given #288 (F,wt=20): 497 -(c1'''' ^ * c3'''' <= (c3 * (c4 ^ * c4))'). [ur(59,a,414,a)]. given #289 (F,wt=20): 500 -(c3'''' * (c3 * (c4 ^ * c4))'' ^ <= c1'''). [ur(61,a,419,a)]. given #290 (F,wt=20): 501 -(c1'' ^ * c3'''' <= (c3 * (c4 ^ * c4))'''). [ur(59,a,419,a)]. given #291 (T,wt=7): 2080 c1 /\ I'' <= O. [para(52(a,1),292(a,2))]. given #292 (T,wt=7): 2146 c1 /\ I'' = O. [resolve(2080,a,44,a),rewrite([35(7),208(7)]),flip(a)]. given #293 (T,wt=8): 293 c1 \/ x <= I' \/ x. [resolve(93,a,73,a)]. given #294 (T,wt=7): 2162 L <= I' \/ c1'. [para(50(a,1),293(a,1))]. given #295 (A,wt=15): 150 I /\ x * y <= (x /\ y ^) * (y /\ x ^). [para(55(a,1),57(a,2,2,2)),rewrite([35(3),56(6)])]. given #296 (F,wt=20): 1359 O != x | L * (x * L) \/ L * ((y /\ (z /\ x)) * L) != L. [para(105(a,1),517(a,1)),rewrite([34(13)]),flip(a)]. given #297 (F,wt=20): 1367 I' ^ != O | L * (c1 * L) \/ L * (I' ^ * L) != L. [para(508(a,1),1352(b,1,2,2,1)),rewrite([34(18)]),flip(a)]. given #298 (F,wt=20): 1369 x /\ (y /\ x)' != O | L * ((x /\ (y /\ x)') * L) != L. [para(135(a,1),1352(b,1,2,2,1)),rewrite([78(16),79(15),34(14),209(14)]),flip(a)]. given #299 (F,wt=20): 1445 L * (x * (y * z)) != O | L * (x * (y * (z * L))) != L. [para(54(a,1),1443(b,1,2,2))]. given #300 (T,wt=4): 2199 I <= L ^. [para(897(a,1),150(a,1,2)),rewrite([35(3),382(3),382(5),382(7),915(6)])]. given #301 (T,wt=6): 2229 x <= x * L ^. [resolve(2199,a,72,a),rewrite([55(2)])]. given #302 (T,wt=5): 2244 c3 ^ <= L ^. [para(256(a,1),2229(a,2))]. given #303 (T,wt=5): 2245 c4 ^ <= L ^. [para(279(a,1),2229(a,2))]. given #304 (A,wt=18): 152 -(x * (y * z) <= u) | y ^ * (x ^ * u') <= z'. [para(54(a,1),58(a,1)),rewrite([68(5),54(8)])]. given #305 (F,wt=20): 1532 O != x | L * (x * L) \/ L * ((y /\ (x /\ z)) * L) != L. [para(101(a,1),1357(b,1,2,2,1))]. given #306 (F,wt=18): 2304 c1 != O | L * (c1 * L) \/ L * ((x /\ c1) * L) != L. [para(296(a,1),1532(b,1,2,2,1,2)),flip(a)]. given #307 (F,wt=18): 2305 c1 != O | L * (c1 * L) \/ L * ((c1 /\ x) * L) != L. [para(35(a,1),2304(b,1,2,2,1))]. given #308 (F,wt=20): 1603 x' /\ (y /\ z) != O | L * ((y /\ (x' /\ z)) * L) != L. [para(101(a,1),1541(b,1,2,1))]. given #309 (T,wt=6): 2230 x <= L ^ * x. [resolve(2199,a,71,a),rewrite([56(2)])]. given #310 (T,wt=6): 2231 I /\ L ^ = I. [resolve(2199,a,44,a)]. given #311 (T,wt=6): 2331 x /\ I <= L ^. [para(2231(a,1),110(b,1,2)),xx(b)]. given #312 (T,wt=6): 2333 I <= x \/ L ^. [para(2231(a,1),696(a,1))]. given #313 (A,wt=11): 153 -(x <= y) | x ^ * y' <= I'. [para(55(a,1),58(a,1))]. given #314 (F,wt=4): 2337 L ^ != O. [para(2231(a,1),1352(b,1,2,2,1)),rewrite([56(14),897(13),34(12),383(12)]),flip(a),xx(b)]. given #315 (F,wt=14): 2315 x /\ y != O | L * ((x /\ y) * L) != L. [para(346(a,1),1603(b,1,2,1,2,1)),rewrite([346(2),382(3),382(6)])]. given #316 (F,wt=14): 2427 x /\ y != O | L * ((y /\ x) * L) != L. [para(35(a,1),2315(b,1,2,1))]. given #317 (F,wt=18): 2428 x /\ (y /\ z) != O | L * ((y /\ (x /\ z)) * L) != L. [para(101(a,1),2315(b,1,2,1))]. given #318 (T,wt=6): 2334 I <= L ^ \/ x. [para(2231(a,1),114(b,1,1)),rewrite([102(9)]),xx(b)]. given #319 (T,wt=6): 2335 I <= L ^ * L. [para(2231(a,1),900(a,1))]. given #320 (T,wt=6): 2336 I <= L * L ^. [para(2231(a,1),924(a,1))]. given #321 (T,wt=6): 2345 I /\ x <= L ^. [para(35(a,1),2331(a,1))]. given #322 (A,wt=17): 155 -(x * (y * z) <= u) | u' * z ^ <= (x * y)'. [para(54(a,1),60(a,1))]. given #323 (F,wt=18): 2430 x /\ (y /\ z) != O | L * ((y /\ (z /\ x)) * L) != L. [para(39(a,1),2427(b,1,2,1))]. given #324 (F,wt=12): 2514 L * ((x' /\ (y /\ x)) * L) != L. [ur(2430,a,210,a)]. given #325 (F,wt=11): 2534 L * ((I /\ L ^') * L) != L. [para(2231(a,1),2514(a,1,2,1,2)),rewrite([35(6)])]. given #326 (F,wt=12): 2530 L * ((c1 /\ I' ^') * L) != L. [para(508(a,1),2514(a,1,2,1,2)),rewrite([35(7)])]. given #327 (T,wt=6): 2361 L ^' <= I'. [resolve(153,a,2199,a),rewrite([1483(2),56(5)])]. given #328 (T,wt=7): 2173 I' \/ c1' = L. [resolve(2162,a,44,a),rewrite([46(7),382(4),382(6)])]. given #329 (T,wt=7): 2232 I \/ L ^ = L ^. [resolve(2199,a,42,a)]. given #330 (T,wt=7): 2535 I /\ L ^' = O. [resolve(2534,a,63,b),flip(a)]. given #331 (A,wt=11): 157 -(x <= y) | y' * x ^ <= I'. [para(56(a,1),60(a,1))]. given #332 (F,wt=6): 2556 x \/ L ^ != O. [para(2232(a,1),905(a,1,2))]. given #333 (F,wt=6): 2648 L ^ \/ x != O. [para(34(a,1),2556(a,1))]. given #334 (F,wt=4): 2649 -(L ^ <= O). [ur(42,b,2648,a)]. given #335 (F,wt=8): 2557 x \/ (y \/ L ^) != O. [para(2232(a,1),903(a,1,2,2))]. given #336 (T,wt=8): 294 x * c1 <= x * I'. [resolve(93,a,72,a)]. given #337 (T,wt=8): 295 c1 * x <= I' * x. [resolve(93,a,71,a)]. given #338 (T,wt=8): 308 c1'' * c2 <= c2'. [resolve(95,a,60,a),rewrite([75(6)])]. given #339 (T,wt=8): 342 x \/ (y \/ x') = L. [para(50(a,1),99(a,1,2)),rewrite([221(2)]),flip(a)]. given #340 (A,wt=14): 158 O = x | L * (x * (L * y)) = L * y. [para(63(b,1),54(a,1,1)),rewrite([54(8)]),flip(b)]. given #341 (F,wt=8): 2650 x \/ (L ^ \/ y) != O. [para(99(a,1),2648(a,1))]. given #342 (F,wt=10): 2558 x \/ (y \/ (z \/ L ^)) != O. [para(2232(a,1),901(a,1,2,2,2))]. given #343 (F,wt=10): 2744 x \/ (y \/ (L ^ \/ z)) != O. [para(37(a,1),2650(a,1))]. given #344 (F,wt=12): 2531 L * ((x /\ (x * L)') * L) != L. [para(554(a,1),2514(a,1,2,1,2)),rewrite([35(5)])]. given #345 (T,wt=8): 362 x /\ (y /\ x') = O. [para(52(a,1),101(a,1,2)),rewrite([343(2)]),flip(a)]. given #346 (T,wt=5): 2754 I /\ c1 = O. [para(296(a,1),362(a,1,2))]. given #347 (T,wt=6): 2767 c1 <= O | c1 != O. [para(2754(a,1),108(b,1)),rewrite([2754(4)]),flip(b)]. given #348 (T,wt=6): 2768 c1 <= I | c1 != O. [para(2754(a,1),109(b,1)),flip(b)]. given #349 (A,wt=14): 159 O = x | y * (L * (x * L)) = y * L. [para(63(b,1),54(a,2,2)),rewrite([54(7)])]. given #350 (F,wt=12): 2532 L * ((x /\ (L * x)') * L) != L. [para(611(a,1),2514(a,1,2,1,2)),rewrite([35(5)])]. given #351 (F,wt=12): 2559 x \/ (y \/ (z \/ (u \/ L ^))) != O. [para(2232(a,1),1061(a,1,2,2,2,2))]. given #352 (F,wt=12): 2745 x \/ (y \/ (z \/ (L ^ \/ u))) != O. [para(37(a,1),2744(a,1,2))]. given #353 (F,wt=14): 2527 L * ((x' /\ (y /\ (z /\ x))) * L) != L. [para(39(a,1),2514(a,1,2,1,2))]. given #354 (T,wt=7): 2764 I /\ (c1 /\ x) = O. [para(2754(a,1),39(a,1,1)),rewrite([208(2)]),flip(a)]. given #355 (T,wt=7): 2765 c1 /\ (x /\ I) = O. [para(2754(a,1),39(a,2,2)),rewrite([35(4),343(6)])]. given #356 (T,wt=7): 2766 I /\ (x /\ c1) = O. [para(2754(a,1),101(a,1,2)),rewrite([343(2)]),flip(a)]. given #357 (T,wt=8): 378 -(x <= y) | x \/ y <= y. [resolve(360,a,80,b)]. given #358 (A,wt=14): 160 x * y = O | L * (x * (y * L)) = L. [para(54(a,1),63(b,1,2)),flip(a)]. given #359 (F,wt=13): 2830 L * ((I'' /\ (x /\ c1)) * L) != L. [para(296(a,1),2527(a,1,2,1,2,2))]. given #360 (F,wt=13): 2836 L * ((L ^' /\ (x /\ I)) * L) != L. [para(2231(a,1),2527(a,1,2,1,2,2))]. given #361 (F,wt=14): 2560 x \/ (y \/ (z \/ (u \/ (w \/ L ^)))) != O. [para(2232(a,1),1063(a,1,2,2,2,2,2))]. given #362 (F,wt=14): 2824 x \/ (y \/ (z \/ (u \/ (L ^ \/ w)))) != O. [para(37(a,1),2745(a,1,2,2))]. given #363 (T,wt=8): 379 -(x <= y) | y \/ x <= y. [resolve(360,a,80,a)]. given #364 (T,wt=7): 2900 x \/ y <= y \/ x. [resolve(379,a,754,a),rewrite([37(3),340(3)])]. given #365 (T,wt=8): 385 x ^ /\ L ^ = x ^. [para(220(a,1),70(a,1,1)),flip(a)]. given #366 (T,wt=5): 2910 x ^ <= L ^. [resolve(385,a,45,b)]. given #367 (A,wt=16): 163 O = x | -(L <= y) | L ^ * y' <= (x * L)'. [para(63(b,1),58(a,1))]. given #368 (F,wt=12): 2922 x ^ != O | L * (x ^ * L) != L. [para(385(a,1),1357(b,1,2,2,1)),rewrite([323(14)]),flip(a)]. given #369 (F,wt=14): 2826 L * ((x' /\ (y /\ (x /\ z))) * L) != L. [para(35(a,1),2527(a,1,2,1,2,2))]. given #370 (F,wt=14): 2831 L * ((I' ^' /\ (x /\ c1)) * L) != L. [para(508(a,1),2527(a,1,2,1,2,2))]. given #371 (F,wt=14): 2832 L * (((x * L)' /\ (y /\ x)) * L) != L. [para(554(a,1),2527(a,1,2,1,2,2))]. given #372 (T,wt=4): 3016 x <= L ^. [para(75(a,1),2910(a,1))]. given #373 (T,wt=6): 2913 x /\ L ^ = x. [para(75(a,1),385(a,1,1)),rewrite([75(5)])]. given #374 (T,wt=4): 3048 L ^ = L. [para(2913(a,1),382(a,1)),flip(a)]. given #375 (T,wt=6): 2933 I <= c4 ^ * c4. [back_rewrite(2191),rewrite([2913(7)])]. given #376 (A,wt=13): 168 x * y \/ (z /\ x) * y = x * y. [para(40(a,1),66(a,1,1)),flip(a)]. given #377 (F,wt=3): 3158 -(L <= O). [back_rewrite(2649),rewrite([3048(2)])]. given #378 (F,wt=13): 3031 L * ((c1 /\ (I' * L)') * L) != L. [para(296(a,1),2832(a,1,2,1,2)),rewrite([35(8)])]. given #379 (F,wt=14): 2833 L * (((L * x)' /\ (y /\ x)) * L) != L. [para(611(a,1),2527(a,1,2,1,2,2))]. given #380 (F,wt=13): 3316 L * ((c1 /\ (L * I')') * L) != L. [para(296(a,1),2833(a,1,2,1,2)),rewrite([35(8)])]. given #381 (T,wt=6): 2935 I <= c3 ^ * c3. [back_rewrite(2189),rewrite([2913(7)])]. given #382 (T,wt=6): 3067 c4 ^ * L = L. [back_rewrite(1963),rewrite([3048(2),382(6),3048(6)])]. given #383 (T,wt=6): 3075 c3 ^ * L = L. [back_rewrite(1726),rewrite([3048(2),382(6),3048(6)])]. given #384 (T,wt=6): 3169 L <= I | I != L. [back_rewrite(2330),rewrite([3048(2),3048(5)]),flip(b)]. given #385 (A,wt=12): 170 x * y \/ x' * y = L * y. [para(50(a,1),66(a,1,1)),flip(a)]. given #386 (F,wt=4): 3331 c4 ^ != O. [para(3067(a,1),65(b,1,2)),rewrite([897(7)]),flip(a),xx(b)]. given #387 (F,wt=4): 3339 c3 ^ != O. [para(3075(a,1),65(b,1,2)),rewrite([897(7)]),flip(a),xx(b)]. given #388 (F,wt=6): 3333 c4 ^ \/ x != O. [para(3067(a,1),177(b,1,1,2)),rewrite([897(8),383(11)]),xx(b)]. given #389 (F,wt=4): 3368 -(c4 ^ <= O). [ur(42,b,3333,a)]. given #390 (T,wt=7): 3258 x <= x * (L * x). [back_rewrite(912),rewrite([3048(2),3048(3),911(4)])]. given #391 (T,wt=7): 3266 L * c4 ^ = c4 ^. [back_rewrite(273),rewrite([3048(2)])]. given #392 (T,wt=7): 3269 L * c3 ^ = c3 ^. [back_rewrite(250),rewrite([3048(2)])]. given #393 (T,wt=7): 3385 x * c4 ^ <= c4 ^. [para(3266(a,1),217(a,2))]. given #394 (A,wt=23): 172 -(x * y \/ z * y <= u) | x ^ * u' \/ z ^ * u' <= y'. [para(66(a,1),58(a,1)),rewrite([69(6),66(9)])]. given #395 (F,wt=6): 3334 x \/ c4 ^ != O. [para(3067(a,1),177(b,1,2,2)),rewrite([897(12),34(11),383(11)]),xx(b)]. given #396 (F,wt=6): 3341 c3 ^ \/ x != O. [para(3075(a,1),177(b,1,1,2)),rewrite([897(8),383(11)]),xx(b)]. given #397 (F,wt=4): 3437 -(c3 ^ <= O). [ur(42,b,3341,a)]. given #398 (F,wt=6): 3342 x \/ c3 ^ != O. [para(3075(a,1),177(b,1,2,2)),rewrite([897(12),34(11),383(11)]),xx(b)]. given #399 (T,wt=7): 3389 x * c3 ^ <= c3 ^. [para(3269(a,1),217(a,2))]. given #400 (T,wt=8): 396 x \/ (x' \/ y) = L. [back_rewrite(129),rewrite([383(5)])]. given #401 (T,wt=8): 439 x \/ (y /\ x)' = L. [para(50(a,1),103(a,1,2)),rewrite([221(2)]),flip(a)]. given #402 (T,wt=8): 449 x * L != O | O = x. [resolve(448,b,63,b)]. given #403 (A,wt=19): 173 -(x * y \/ z * y <= u) | u' * y ^ <= (x \/ z)'. [para(66(a,1),60(a,1))]. given #404 (F,wt=8): 3369 x \/ (c4 ^ \/ y) != O. [para(99(a,1),3333(a,1))]. given #405 (F,wt=8): 3436 x \/ (y \/ c4 ^) != O. [para(37(a,1),3334(a,1))]. given #406 (F,wt=8): 3438 x \/ (c3 ^ \/ y) != O. [para(99(a,1),3341(a,1))]. given #407 (F,wt=8): 3439 x \/ (y \/ c3 ^) != O. [para(37(a,1),3342(a,1))]. given #408 (T,wt=8): 522 O = x | x \/ y != O. [para(63(b,1),177(b,1,1)),rewrite([383(11)]),xx(c)]. given #409 (T,wt=8): 523 O = x | y \/ x != O. [para(63(b,1),177(b,1,2)),rewrite([34(11),383(11)]),xx(c)]. given #410 (T,wt=8): 563 c3' * x ^ <= c3'. [resolve(544,a,60,a)]. given #411 (T,wt=7): 3539 c3' * x <= c3'. [para(75(a,1),563(a,1,2))]. given #412 (A,wt=18): 174 x \/ y = O | L * (x * L) \/ L * (y * L) = L. [para(66(a,1),63(b,1,2)),rewrite([67(10)]),flip(a)]. given #413 (F,wt=10): 3510 x \/ (y \/ (c4 ^ \/ z)) != O. [para(37(a,1),3369(a,1))]. given #414 (F,wt=10): 3511 x \/ (y \/ (z \/ c4 ^)) != O. [para(37(a,1),3436(a,1,2))]. given #415 (F,wt=10): 3512 x \/ (y \/ (c3 ^ \/ z)) != O. [para(37(a,1),3438(a,1))]. given #416 (F,wt=10): 3513 x \/ (y \/ (z \/ c3 ^)) != O. [para(37(a,1),3439(a,1,2))]. given #417 (T,wt=8): 564 c3 ^ * c3' <= x'. [resolve(544,a,58,a)]. given #418 (T,wt=7): 3587 c3 ^ * c3' <= O. [para(469(a,1),564(a,2))]. given #419 (T,wt=5): 3597 c3 <= c3''. [resolve(3587,a,58,a),rewrite([75(3),346(3),87(3)])]. given #420 (T,wt=7): 3598 c3 ^ * c3' = O. [resolve(3587,a,44,a),rewrite([35(7),208(7)]),flip(a)]. given #421 (A,wt=13): 178 x * y \/ x * (z /\ y) = x * y. [para(40(a,1),67(a,1,2)),flip(a)]. given #422 (F,wt=12): 3569 x \/ (y \/ (z \/ (c4 ^ \/ u))) != O. [ur(523,a,3510,a(flip))]. given #423 (F,wt=12): 3570 x \/ (y \/ (z \/ (u \/ c4 ^))) != O. [ur(523,a,3511,a(flip))]. given #424 (F,wt=12): 3571 x \/ (y \/ (z \/ (c3 ^ \/ u))) != O. [ur(523,a,3512,a(flip))]. given #425 (F,wt=12): 3572 x \/ (y \/ (z \/ (u \/ c3 ^))) != O. [ur(523,a,3513,a(flip))]. given #426 (T,wt=7): 3608 c3 /\ c3'' = c3. [resolve(3597,a,44,a)]. given #427 (T,wt=7): 3615 c3' ^ * c3 = O. [para(3598(a,1),68(a,1,1)),rewrite([1612(2),75(7)]),flip(a)]. given #428 (T,wt=7): 3656 x /\ c3 <= c3''. [para(3608(a,1),110(b,1,2)),xx(b)]. given #429 (T,wt=7): 3658 c3 <= x \/ c3''. [para(3608(a,1),696(a,1))]. given #430 (A,wt=12): 180 x * y \/ x * y' = x * L. [para(50(a,1),67(a,1,2)),flip(a)]. given #431 (F,wt=13): 3332 x * c4 ^ != O | L * (x * L) != L. [para(3067(a,1),166(b,1,2,2))]. given #432 (F,wt=6): 3726 c3 * c4 ^ != O. [para(87(a,1),3332(b,1,2)),rewrite([88(9)]),xx(b)]. given #433 (F,wt=6): 3727 c4 * c4 ^ != O. [para(90(a,1),3332(b,1,2)),rewrite([91(9)]),xx(b)]. given #434 (F,wt=7): 3728 c4 ^ * c4 ^ != O. [para(3067(a,1),3332(b,1,2)),rewrite([897(10)]),xx(b)]. given #435 (T,wt=6): 3722 c3 ^ * c3 = L. [para(3598(a,1),180(a,1,2)),rewrite([34(6),209(6),3075(8)])]. given #436 (T,wt=7): 3659 c3 <= c3'' \/ x. [para(3608(a,1),114(b,1,1)),rewrite([102(10)]),xx(b)]. given #437 (T,wt=7): 3660 c3 <= c3'' * L. [para(3608(a,1),900(a,1))]. given #438 (T,wt=7): 3661 c3 <= L * c3''. [para(3608(a,1),924(a,1))]. given #439 (A,wt=19): 182 -(x * y \/ x * z <= u) | x ^ * u' <= (y \/ z)'. [para(67(a,1),58(a,1))]. given #440 (F,wt=7): 3729 c3 ^ * c4 ^ != O. [para(3075(a,1),3332(b,1,2)),rewrite([897(10)]),xx(b)]. given #441 (F,wt=8): 3730 x \/ c3 * c4 ^ != O. [ur(523,a,3726,a(flip))]. given #442 (F,wt=8): 3731 c3 * c4 ^ \/ x != O. [ur(522,a,3726,a(flip))]. given #443 (F,wt=6): 3861 -(c3 * c4 ^ <= O). [ur(42,b,3731,a)]. given #444 (T,wt=7): 3687 c3 /\ x <= c3''. [para(35(a,1),3656(a,1))]. given #445 (T,wt=8): 588 c4' * x ^ <= c4'. [resolve(545,a,60,a)]. given #446 (T,wt=7): 3893 c4' * x <= c4'. [para(75(a,1),588(a,1,2))]. given #447 (T,wt=8): 589 c4 ^ * c4' <= x'. [resolve(545,a,58,a)]. given #448 (A,wt=23): 183 -(x * y \/ x * z <= u) | u' * y ^ \/ u' * z ^ <= x'. [para(67(a,1),60(a,1)),rewrite([69(7),67(9)])]. given #449 (F,wt=4): 3862 -(L <= c3'). [ur(61,a,3861,a),rewrite([346(2),75(4),91(3)])]. given #450 (F,wt=4): 3965 c3' != L. [ur(468,a,3862,a),flip(a)]. given #451 (F,wt=5): 3863 -(L <= c4 ^'). [ur(59,a,3861,a),rewrite([346(4),3075(4)])]. given #452 (F,wt=5): 3966 c4 ^' != L. [ur(468,a,3863,a),flip(a)]. given #453 (T,wt=7): 3921 c4 ^ * c4' <= O. [para(469(a,1),589(a,2))]. given #454 (T,wt=5): 3976 c4 <= c4''. [resolve(3921,a,58,a),rewrite([75(3),346(3),90(3)])]. given #455 (T,wt=7): 3977 c4 ^ * c4' = O. [resolve(3921,a,44,a),rewrite([35(7),208(7)]),flip(a)]. given #456 (T,wt=6): 4006 c4 ^ * c4 = L. [para(3977(a,1),180(a,1,2)),rewrite([34(6),209(6),3067(8)])]. given #457 (A,wt=26): 188 x * (y * z) /\ u <= (x /\ u * (z ^ * y ^)) * (y * z /\ x ^ * u). [para(68(a,1),57(a,2,1,2,2))]. given #458 (F,wt=7): 4068 -(c3 * c3 ^ <= c1'). [back_rewrite(86),rewrite([4011(8),3269(5)])]. given #459 (F,wt=8): 3732 x \/ c4 * c4 ^ != O. [ur(523,a,3727,a(flip))]. given #460 (F,wt=8): 3733 c4 * c4 ^ \/ x != O. [ur(522,a,3727,a(flip))]. given #461 (F,wt=6): 4115 -(c4 * c4 ^ <= O). [ur(42,b,3733,a)]. given #462 (T,wt=7): 3987 c4 /\ c4'' = c4. [resolve(3976,a,44,a)]. given #463 (T,wt=7): 3994 c4' ^ * c4 = O. [para(3977(a,1),68(a,1,1)),rewrite([1612(2),75(7)]),flip(a)]. given #464 (T,wt=7): 4123 x /\ c4 <= c4''. [para(3987(a,1),110(b,1,2)),xx(b)]. given #465 (T,wt=7): 4125 c4 <= x \/ c4''. [para(3987(a,1),696(a,1))]. given #466 (A,wt=18): 189 x * (y * z) <= u | -(y ^ * (x ^ * u') <= z'). [para(68(a,1),59(b,1,1)),rewrite([54(2),54(8)])]. given #467 (F,wt=4): 4116 -(L <= c4'). [ur(61,a,4115,a),rewrite([346(2),75(4),91(3)])]. given #468 (F,wt=4): 4185 c4' != L. [ur(468,a,4116,a),flip(a)]. given #469 (F,wt=8): 4112 -(c1'' * c3 <= c3'). [ur(61,a,4068,a),rewrite([75(6)])]. given #470 (F,wt=9): 3734 x \/ c4 ^ * c4 ^ != O. [ur(523,a,3728,a(flip))]. given #471 (T,wt=7): 4126 c4 <= c4'' \/ x. [para(3987(a,1),114(b,1,1)),rewrite([102(10)]),xx(b)]. given #472 (T,wt=7): 4127 c4 <= c4'' * L. [para(3987(a,1),900(a,1))]. given #473 (T,wt=7): 4128 c4 <= L * c4''. [para(3987(a,1),924(a,1))]. given #474 (T,wt=7): 4159 c4 /\ x <= c4''. [para(35(a,1),4123(a,1))]. given #475 (A,wt=18): 190 x * (y * z) <= u | -(u' * (z ^ * y ^) <= x'). [para(68(a,1),61(b,1,2))]. given #476 (F,wt=9): 3735 c4 ^ * c4 ^ \/ x != O. [ur(522,a,3728,a(flip))]. given #477 (F,wt=7): 4248 -(c4 ^ * c4 ^ <= O). [ur(42,b,3735,a)]. given #478 (F,wt=5): 4249 -(c4 <= c4 ^'). [ur(59,a,4248,a),rewrite([75(3),346(3),90(3)])]. given #479 (F,wt=7): 4250 c4 /\ c4 ^' != c4. [ur(109,a,4249,a),rewrite([35(5)])]. given #480 (T,wt=8): 624 x' <= O | x' != O. [para(52(a,1),108(b,1)),rewrite([52(3)]),flip(b)]. given #481 (T,wt=8): 626 I' <= c1 | I' != c1. [para(296(a,1),108(b,1)),rewrite([296(6)]),flip(b)]. given #482 (T,wt=8): 667 x' <= x | x' != O. [para(52(a,1),109(b,1)),flip(b)]. given #483 (T,wt=8): 736 x /\ (y /\ c1) <= I'. [para(39(a,1),723(a,1))]. given #484 (A,wt=23): 193 x * y \/ z * y <= u | -(x ^ * u' \/ z ^ * u' <= y'). [para(69(a,1),59(b,1,1)),rewrite([66(2),66(9)])]. given #485 (F,wt=9): 3857 x \/ c3 ^ * c4 ^ != O. [ur(523,a,3729,a(flip))]. given #486 (F,wt=9): 3858 c3 ^ * c4 ^ \/ x != O. [ur(522,a,3729,a(flip))]. given #487 (F,wt=7): 4283 -(c3 ^ * c4 ^ <= O). [ur(42,b,3858,a)]. given #488 (F,wt=5): 4284 -(L <= c3 ^'). [ur(61,a,4283,a),rewrite([346(2),75(4),91(3)])]. given #489 (T,wt=8): 745 x /\ (c1 /\ y) <= I'. [para(101(a,1),735(a,1))]. given #490 (T,wt=8): 763 c1 <= x \/ (y \/ I'). [para(37(a,1),755(a,2))]. given #491 (T,wt=8): 808 c1 <= x \/ (I' \/ y). [para(99(a,1),762(a,2))]. given #492 (T,wt=8): 909 O = x | L * x != O. [back_rewrite(369),rewrite([897(9)]),xx(c)]. given #493 (A,wt=23): 194 x * y \/ x * z <= u | -(u' * y ^ \/ u' * z ^ <= x'). [para(69(a,1),61(b,1,2)),rewrite([67(2),67(9)])]. given #494 (F,wt=5): 4285 -(c3 <= c4 ^'). [ur(59,a,4283,a),rewrite([75(3),346(3),87(3)])]. given #495 (F,wt=5): 4286 c3 ^' != L. [ur(468,a,4284,a),flip(a)]. given #496 (F,wt=7): 4334 c3 /\ c4 ^' != c3. [ur(109,a,4285,a),rewrite([35(5)])]. given #497 (F,wt=9): 4251 c4 \/ c4 ^' != c4 ^'. [ur(106,a,4249,a),rewrite([34(5)])]. given #498 (T,wt=8): 1046 c1 /\ I' * L = c1. [resolve(1037,a,44,a)]. given #499 (T,wt=8): 1084 c1 /\ L * I' = c1. [resolve(1076,a,44,a)]. NOTE: Back_subsumption disabled, ratio of kept to back_subsumed is 25 (0.00 of 0.33 sec). given #500 (T,wt=8): 1366 x /\ y = O | O != y. [para(63(b,1),1352(b,1,2)),rewrite([34(11),383(11)]),flip(a),xx(c)]. given #501 (T,wt=8): 1481 -(x <= y) | y' <= x'. [back_rewrite(154),rewrite([1468(5)])]. given #502 (A,wt=18): 196 (x /\ y) * z <= u | -((x ^ /\ y ^) * u' <= z'). [para(70(a,1),59(b,1,1))]. given #503 (F,wt=9): 4335 c3 \/ c4 ^' != c4 ^'. [ur(106,a,4285,a),rewrite([34(5)])]. given #504 (F,wt=10): 3782 -(c1'' * (c3 * c4) <= c3'). [back_rewrite(240),rewrite([3741(9)])]. given #505 (F,wt=10): 3859 x \/ (y \/ c3 * c4 ^) != O. [ur(523,a,3730,a(flip))]. given #506 (F,wt=10): 3860 x \/ (c3 * c4 ^ \/ y) != O. [ur(522,a,3730,a(flip)),rewrite([37(6)])]. given #507 (T,wt=6): 4461 I'' <= c1'. [resolve(1481,a,93,a)]. given #508 (T,wt=7): 4373 c4''' <= c4'. [resolve(1481,a,3976,a)]. given #509 (T,wt=7): 4381 c3''' <= c3'. [resolve(1481,a,3597,a)]. given #510 (T,wt=7): 4411 I' ^' <= c1'. [resolve(1481,a,816,a)]. given #511 (A,wt=18): 197 x * (y /\ z) <= u | -(u' * (y ^ /\ z ^) <= x'). [para(70(a,1),61(b,1,2))]. given #512 (F,wt=10): 4065 c1' \/ c3 * c3 ^ != c1'. [back_rewrite(243),rewrite([4011(10),3269(7)])]. given #513 (F,wt=10): 4067 -(c3 ^ * c1'' <= c3 ^'). [back_rewrite(241),rewrite([4011(13),3269(10)])]. given #514 (F,wt=10): 4113 x \/ (y \/ c4 * c4 ^) != O. [ur(523,a,3732,a(flip))]. given #515 (F,wt=10): 4114 x \/ (c4 * c4 ^ \/ y) != O. [ur(522,a,3732,a(flip)),rewrite([37(6)])]. given #516 (T,wt=7): 4425 (L * x)' <= x'. [resolve(1481,a,600,a)]. given #517 (T,wt=7): 4426 c4' <= (c4 * x)'. [resolve(1481,a,545,a)]. given #518 (T,wt=7): 4427 c3' <= (c3 * x)'. [resolve(1481,a,544,a)]. given #519 (T,wt=7): 4428 (x * L)' <= x'. [resolve(1481,a,541,a)]. given #520 (A,wt=23): 198 (x * y /\ z) * u <= (x /\ z * y ^) * ((y /\ x ^ * z) * u). [resolve(71,a,57,a),rewrite([54(11)])]. given #521 (F,wt=11): 4062 -(c3 * c3 ^'' <= c1'''). [back_rewrite(411),rewrite([4011(8),3269(5)])]. given #522 (F,wt=11): 4064 -(c3'' * c3 ^ <= c1'''). [back_rewrite(364),rewrite([4011(10),3269(7)])]. given #523 (F,wt=11): 4187 c3' \/ c1'' * c3 != c3'. [ur(106,a,4112,a)]. given #524 (F,wt=11): 4188 -(c1'' ^ * c3'' <= c3'). [ur(59,a,4112,a)]. given #525 (T,wt=7): 4432 x' <= (y /\ x)'. [resolve(1481,a,358,a)]. given #526 (T,wt=7): 4434 (x \/ y)' <= x'. [resolve(1481,a,356,a)]. given #527 (T,wt=7): 4435 x' <= (x /\ y)'. [resolve(1481,a,326,a)]. given #528 (T,wt=7): 4449 (x \/ y)' <= y'. [resolve(1481,a,211,a)]. given #529 (A,wt=23): 199 x * (y * z /\ u) <= x * ((y /\ u * z ^) * (z /\ y ^ * u)). [resolve(72,a,57,a)]. given #530 (F,wt=11): 4189 x \/ (y \/ c4 ^ * c4 ^) != O. [ur(523,a,3734,a(flip))]. given #531 (F,wt=11): 4190 x \/ (c4 ^ * c4 ^ \/ y) != O. [ur(522,a,3734,a(flip)),rewrite([37(7)])]. given #532 (F,wt=11): 4281 x \/ (y \/ c3 ^ * c4 ^) != O. [ur(523,a,3857,a(flip))]. given #533 (F,wt=11): 4282 x \/ (c3 ^ * c4 ^ \/ y) != O. [ur(522,a,3857,a(flip)),rewrite([37(7)])]. given #534 (T,wt=8): 1484 x <= y | -(y' <= x'). [para(1468(a,1),59(b,1)),rewrite([56(2)])]. given #535 (T,wt=7): 4786 x <= O | -(L <= x'). [para(346(a,1),1484(b,1))]. given #536 (T,wt=7): 4787 L <= x | -(x' <= O). [para(469(a,1),1484(b,2))]. given #537 (T,wt=8): 1530 x /\ y = O | O != x. [para(63(b,1),1357(b,1,2)),rewrite([34(11),383(11)]),flip(a),xx(c)]. given #538 (A,wt=23): 200 (x * y /\ z) \/ u <= (x /\ z * y ^) * (y /\ x ^ * z) \/ u. [resolve(73,a,57,a)]. given #539 (F,wt=4): 4785 -(L <= I'). [ur(1484,a,939,a),rewrite([346(2)])]. given #540 (F,wt=4): 4850 I' != L. [ur(468,a,4785,a),flip(a)]. given #541 (F,wt=5): 4774 -(c4'' <= O). [ur(1484,a,4116,a),rewrite([469(5)])]. given #542 (F,wt=5): 4782 -(c3'' <= O). [ur(1484,a,3862,a),rewrite([469(5)])]. given #543 (T,wt=8): 1615 x ^ /\ x' ^ = O. [back_rewrite(195),rewrite([1612(6)])]. given #544 (T,wt=7): 4860 c1 /\ c1' ^ = O. [para(94(a,1),1615(a,1,1))]. given #545 (T,wt=7): 4867 I /\ I' ^ = O. [para(1483(a,1),1615(a,1,1))]. given #546 (T,wt=8): 1814 c3 * c3 ^ <= x \/ I. [para(266(a,1),357(a,2,2))]. given #547 (A,wt=23): 201 x * y /\ (z /\ u) <= (x /\ z * y ^) * (y /\ x ^ * z) /\ u. [resolve(74,a,57,a),rewrite([39(3)])]. given #548 (F,wt=5): 4849 -(I'' <= O). [ur(4787,a,4785,a)]. given #549 (F,wt=5): 4852 c4'' != O. [ur(624,a,4774,a)]. given #550 (F,wt=5): 4854 c3'' != O. [ur(624,a,4782,a)]. given #551 (F,wt=5): 4964 I'' != O. [ur(624,a,4849,a)]. given #552 (T,wt=8): 1815 x /\ c3 * c3 ^ <= I. [para(266(a,1),696(a,2))]. given #553 (T,wt=8): 1816 c3 * c3 ^ /\ x <= I. [para(266(a,1),698(a,2))]. given #554 (T,wt=8): 2068 c4 * c4 ^ <= x \/ I. [para(289(a,1),357(a,2,2))]. given #555 (T,wt=8): 2069 x /\ c4 * c4 ^ <= I. [para(289(a,1),696(a,2))]. given #556 (A,wt=20): 202 x * y ^ /\ z <= (x /\ z * y) * (y ^ /\ x ^ * z). [para(75(a,1),57(a,2,1,2,2))]. given #557 (F,wt=6): 4769 -(c3 ^'' <= O). [ur(1484,a,4284,a),rewrite([469(6)])]. given #558 (F,wt=6): 4781 -(c4 ^'' <= O). [ur(1484,a,3863,a),rewrite([469(6)])]. given #559 (F,wt=6): 4851 -(L <= c4'''). [ur(4786,a,4774,a)]. given #560 (F,wt=6): 4853 -(L <= c3'''). [ur(4786,a,4782,a)]. given #561 (T,wt=8): 2070 c4 * c4 ^ /\ x <= I. [para(289(a,1),698(a,2))]. given #562 (T,wt=8): 2077 x /\ c1 <= I' /\ x. [para(35(a,1),292(a,1))]. given #563 (T,wt=8): 2078 c1 /\ x <= x /\ I'. [para(35(a,1),292(a,2))]. given #564 (T,wt=8): 2083 c1 <= I' /\ I' ^. [para(508(a,1),292(a,1))]. given #565 (A,wt=20): 203 x ^ * y /\ z <= (x ^ /\ z * y ^) * (y /\ x * z). [para(75(a,1),57(a,2,2,2,1))]. given #566 (F,wt=6): 4963 -(L <= I'''). [ur(4786,a,4849,a)]. given #567 (F,wt=6): 5074 c3 ^'' != O. [ur(624,a,4769,a)]. given #568 (F,wt=6): 5076 c4 ^'' != O. [ur(624,a,4781,a)]. given #569 (F,wt=6): 5078 c4''' != L. [ur(468,a,4851,a),flip(a)]. given #570 (T,wt=8): 2084 c1 <= I' /\ c1 * L. [para(554(a,1),292(a,1))]. given #571 (T,wt=8): 2085 c1 <= I' /\ L * c1. [para(611(a,1),292(a,1))]. given #572 (T,wt=8): 2148 c1 <= I'' | c1 != O. [para(2146(a,1),45(b,1)),flip(b)]. given #573 (T,wt=8): 2149 c1 /\ I'' ^ = O. [para(2146(a,1),70(a,1,1)),rewrite([1612(2),94(3)]),flip(a)]. given #574 (A,wt=13): 204 x ^ * y <= z | -(x * z' <= y'). [para(75(a,1),59(b,1,1))]. given #575 (F,wt=6): 5080 c3''' != L. [ur(468,a,4853,a),flip(a)]. given #576 (F,wt=6): 5165 I''' != L. [ur(468,a,4963,a),flip(a)]. given #577 (F,wt=7): 4768 -(c4 ^'' <= c3'). [ur(1484,a,4285,a)]. given #578 (F,wt=7): 4771 -(c4 ^'' <= c4'). [ur(1484,a,4249,a)]. given #579 (T,wt=8): 2159 x \/ c1 <= I' \/ x. [para(34(a,1),293(a,1))]. given #580 (T,wt=8): 2160 c1 \/ x <= x \/ I'. [para(34(a,1),293(a,2))]. given #581 (T,wt=8): 2214 c1 = O | I' ^ != O. [para(63(b,1),1367(b,1,1)),rewrite([383(17)]),flip(a),xx(c)]. given #582 (T,wt=8): 2246 x <= x * (x ^ * x). [back_rewrite(1441),rewrite([2241(4)])]. given #583 (A,wt=13): 205 x * y ^ <= z | -(z' * y <= x'). [para(75(a,1),61(b,1,2))]. given #584 (F,wt=7): 4775 -(L <= (c4 * c4 ^)'). [ur(1484,a,4115,a),rewrite([346(2)])]. given #585 (F,wt=7): 4783 -(L <= (c3 * c4 ^)'). [ur(1484,a,3861,a),rewrite([346(2)])]. given #586 (F,wt=7): 4965 L * c4'' != O. [ur(909,a,4852,a(flip))]. given #587 (F,wt=7): 4966 x \/ c4'' != O. [ur(523,a,4852,a(flip))]. given #588 (T,wt=7): 5255 c1 <= c1 * (c1 * c1). [para(94(a,1),2246(a,2,2,1))]. given #589 (T,wt=8): 2307 x /\ c1 = O | c1 != O. [para(63(b,1),2304(b,1,2)),rewrite([34(14),383(14)]),flip(a),xx(c)]. given #590 (T,wt=8): 2309 c1 /\ x = O | c1 != O. [para(63(b,1),2305(b,1,2)),rewrite([34(14),383(14)]),flip(a),xx(c)]. given #591 (T,wt=8): 2400 x ^ * x' <= I'. [resolve(153,a,360,a)]. given #592 (A,wt=10): 222 (x /\ y) \/ (x /\ y') = x. [back_rewrite(132),rewrite([220(6)])]. given #593 (F,wt=7): 4967 c4'' \/ x != O. [ur(522,a,4852,a(flip))]. given #594 (F,wt=7): 4968 c4'' * L != O. [ur(449,b,4852,a(flip))]. given #595 (F,wt=7): 4969 L * c3'' != O. [ur(909,a,4854,a(flip))]. given #596 (F,wt=7): 4970 x \/ c3'' != O. [ur(523,a,4854,a(flip))]. given #597 (T,wt=6): 5323 I /\ c1' = I. [para(2754(a,1),222(a,1,1)),rewrite([209(6)])]. given #598 (T,wt=4): 5370 I <= c1'. [resolve(5323,a,45,b)]. given #599 (T,wt=6): 5378 x /\ I <= c1'. [para(5323(a,1),110(b,1,2)),xx(b)]. given #600 (T,wt=6): 5380 I <= x \/ c1'. [para(5323(a,1),696(a,1))]. given #601 (A,wt=36): 229 -(x <= (y /\ z * u ^) * (u /\ y ^ * z)) | (y * u /\ z) \/ x <= (y /\ z * u ^) * (u /\ y ^ * z). [resolve(80,a,57,a)]. given #602 (F,wt=7): 4971 c3'' \/ x != O. [ur(522,a,4854,a(flip))]. given #603 (F,wt=7): 4972 c3'' * L != O. [ur(449,b,4854,a(flip))]. given #604 (F,wt=7): 4973 L * I'' != O. [ur(909,a,4964,a(flip))]. given #605 (F,wt=7): 4974 x \/ I'' != O. [ur(523,a,4964,a(flip))]. given #606 (T,wt=6): 5381 I <= c1' \/ x. [para(5323(a,1),114(b,1,1)),rewrite([102(9)]),xx(b)]. given #607 (T,wt=6): 5382 I <= c1' * L. [para(5323(a,1),900(a,1))]. given #608 (T,wt=6): 5383 I <= L * c1'. [para(5323(a,1),924(a,1))]. given #609 (T,wt=6): 5388 c1'' <= I'. [para(5323(a,1),4432(a,2,1))]. given #610 (A,wt=36): 231 -(x <= (y /\ z * u ^) * (u /\ y ^ * z)) | x \/ (y * u /\ z) <= (y /\ z * u ^) * (u /\ y ^ * z). [resolve(80,b,57,a)]. given #611 (F,wt=7): 4975 I'' \/ x != O. [ur(522,a,4964,a(flip))]. given #612 (F,wt=7): 4976 I'' * L != O. [ur(449,b,4964,a(flip))]. given #613 (F,wt=7): 5073 -(L <= c3 ^'''). [ur(4786,a,4769,a)]. given #614 (F,wt=7): 5075 -(L <= c4 ^'''). [ur(4786,a,4781,a)]. given #615 (T,wt=6): 5394 x <= x * c1'. [resolve(5370,a,72,a),rewrite([55(2)])]. given #616 (T,wt=6): 5395 x <= c1' * x. [resolve(5370,a,71,a),rewrite([56(2)])]. given #617 (T,wt=6): 5407 I /\ x <= c1'. [para(35(a,1),5378(a,1))]. given #618 (T,wt=7): 5301 c1 * c1' <= I'. [para(94(a,1),2400(a,1,1))]. given #619 (A,wt=20): 232 -(x <= (c2 ^ * (c1 * c3))') | x \/ c4 <= (c2 ^ * (c1 * c3))'. [resolve(84,a,80,b)]. given #620 (F,wt=7): 5164 -(I'''' <= O). [ur(4787,a,4963,a)]. given #621 (F,wt=7): 5262 (c4 * c4 ^)' != L. [ur(468,a,4775,a),flip(a)]. given #622 (F,wt=7): 5264 (c3 * c4 ^)' != L. [ur(468,a,4783,a),flip(a)]. given #623 (F,wt=7): 5505 c3 ^''' != L. [ur(468,a,5073,a),flip(a)]. given #624 (T,wt=7): 5307 x /\ x'' = x. [para(52(a,1),222(a,1,1)),rewrite([209(5)])]. given #625 (T,wt=5): 5580 x <= x''. [resolve(5307,a,45,b)]. given #626 (T,wt=5): 5617 x'' <= x. [resolve(5580,a,1484,b)]. given #627 (T,wt=5): 5654 x'' = x. [resolve(5617,a,44,a),rewrite([35(3),5307(3)]),flip(a)]. given #628 (A,wt=20): 233 -(x <= (c2 ^ * (c1 * c3))') | c4 \/ x <= (c2 ^ * (c1 * c3))'. [resolve(84,a,80,a)]. given #629 (F,wt=5): 5689 -(c4 ^ <= c4'). [back_rewrite(4771),rewrite([5654(4)])]. given #630 (F,wt=5): 5690 -(c4 ^ <= c3'). [back_rewrite(4768),rewrite([5654(4)])]. given #631 (F,wt=6): 5673 -(c1 * c3 <= c3'). [back_rewrite(5335),rewrite([5654(3),5654(3)])]. given #632 (F,wt=6): 5688 -(c3 <= (c1 * c3)'). [back_rewrite(4776),rewrite([5654(3),5654(4)])]. given #633 (T,wt=6): 5655 c1' ^ <= c1'. [back_rewrite(5565),rewrite([5654(3),56(5)])]. given #634 (T,wt=6): 5657 c1 <= (I /\ x)'. [back_rewrite(5545),rewrite([5654(3)])]. given #635 (T,wt=6): 5660 c1 <= (x /\ I)'. [back_rewrite(5396),rewrite([5654(3)])]. given #636 (T,wt=6): 5714 c2 <= (c1 * c2)'. [back_rewrite(4436),rewrite([5654(3),5654(4)])]. given #637 (A,wt=13): 234 c4 /\ x <= (c2 ^ * (c1 * c3))' /\ x. [resolve(84,a,74,a)]. given #638 (F,wt=7): 5686 -(c1 <= (c3 * c3 ^)'). [back_rewrite(4780),rewrite([5654(3),5654(3),5654(6)])]. given #639 (F,wt=8): 4770 -(L <= (c3 ^ * c4 ^)'). [ur(1484,a,4283,a),rewrite([346(2)])]. given #640 (F,wt=8): 4772 -(L <= (c4 ^ * c4 ^)'). [ur(1484,a,4248,a),rewrite([346(2)])]. given #641 (F,wt=8): 5661 -(c1 * (c3 * c4) <= c3'). [back_rewrite(5360),rewrite([5654(3),5654(6),5654(6)])]. given #642 (T,wt=6): 5715 I <= (x /\ c1)'. [back_rewrite(4420),rewrite([5654(3)])]. given #643 (T,wt=6): 5716 I <= (c1 /\ x)'. [back_rewrite(4419),rewrite([5654(3)])]. given #644 (T,wt=6): 5732 c1 * c2 <= c2'. [back_rewrite(2684),rewrite([5654(3),94(2),5654(4)])]. given #645 (T,wt=6): 5784 c1 <= c1' ^'. [resolve(5655,a,1481,a),rewrite([5654(3)])]. given #646 (A,wt=13): 235 c4 \/ x <= (c2 ^ * (c1 * c3))' \/ x. [resolve(84,a,73,a)]. given #647 (F,wt=8): 5670 -(c1 * c3 <= (c3 * c4)'). [back_rewrite(5346),rewrite([5654(3),94(2),5654(4),5654(8)])]. given #648 (F,wt=8): 5672 -(c3 ^ * c1 <= c3 ^'). [back_rewrite(5339),rewrite([5654(3),5654(5),5654(5),5654(5)])]. given #649 (F,wt=8): 5677 c4' \/ c4 ^ != c4'. [back_rewrite(5214),rewrite([5654(6)])]. given #650 (F,wt=8): 5678 c4' /\ c4 ^ != c4 ^. [back_rewrite(5213),rewrite([5654(6),5654(9)])]. given #651 (T,wt=7): 5372 I \/ c1' = c1'. [para(5323(a,1),40(a,1,2)),rewrite([34(4)])]. given #652 (T,wt=7): 5373 I /\ c1' ^ = I. [para(5323(a,1),70(a,1,1)),rewrite([1483(2),1483(3)]),flip(a)]. given #653 (T,wt=5): 5915 I <= c1' ^. [resolve(5373,a,45,b)]. given #654 (T,wt=7): 5656 I <= (c1 * c1')'. [back_rewrite(5557),rewrite([5654(3)])]. given #655 (A,wt=13): 236 x * c4 <= x * (c2 ^ * (c1 * c3))'. [resolve(84,a,72,a)]. given #656 (F,wt=4): 5907 c1' != O. [para(5372(a,1),907(a,1))]. given #657 (F,wt=6): 5908 x \/ c1' != O. [para(5372(a,1),905(a,1,2))]. given #658 (F,wt=6): 5966 L * c1' != O. [ur(909,a,5907,a(flip))]. given #659 (F,wt=6): 5967 c1' \/ x != O. [ur(522,a,5907,a(flip))]. given #660 (T,wt=7): 5674 x' ^ <= x ^'. [back_rewrite(5293),rewrite([5654(3),56(4)])]. given #661 (T,wt=6): 5991 I' ^ <= I'. [para(1483(a,1),5674(a,2,1))]. given #662 (T,wt=6): 5992 I <= I' ^'. [resolve(5991,a,1481,a),rewrite([5654(3)])]. given #663 (T,wt=7): 5711 c1 <= (c2 * c2 ^)'. [back_rewrite(4460),rewrite([5654(3)])]. given #664 (A,wt=13): 237 c4 * x <= (c2 ^ * (c1 * c3))' * x. [resolve(84,a,71,a)]. given #665 (F,wt=4): 5975 -(c1' <= O). [ur(42,b,5967,a)]. given #666 (F,wt=3): 6037 -(L <= c1). [ur(4786,a,5975,a),rewrite([5654(4)])]. given #667 (F,wt=3): 6038 c1 != L. [ur(468,a,6037,a),flip(a)]. given #668 (F,wt=6): 5968 c1' * L != O. [ur(449,b,5907,a(flip))]. given #669 (T,wt=7): 5712 c3 <= (I' * c3)'. [back_rewrite(4444),rewrite([5654(3)])]. given #670 (T,wt=7): 5713 c4 <= (I' * c4)'. [back_rewrite(4441),rewrite([5654(3)])]. given #671 (T,wt=7): 5719 c3 <= (c3' * x)'. [back_rewrite(4382),rewrite([5654(3)])]. given #672 (T,wt=7): 5720 c4 <= (c4' * x)'. [back_rewrite(4374),rewrite([5654(3)])]. given #673 (A,wt=11): 238 c4 /\ (c2 ^ * (c1 * c3))' = c4. [resolve(84,a,44,a)]. given #674 (F,wt=8): 5679 c3' \/ c4 ^ != c3'. [back_rewrite(5211),rewrite([5654(6)])]. given #675 (F,wt=8): 5680 c3' /\ c4 ^ != c4 ^. [back_rewrite(5210),rewrite([5654(6),5654(9)])]. given #676 (F,wt=8): 5685 -(c3 <= (c1 * (c3 * c4))'). [back_rewrite(4784),rewrite([5654(3),5654(4)])]. given #677 (F,wt=8): 5687 -(c3 ^ <= (c3 ^ * c1)'). [back_rewrite(4778),rewrite([5654(4),5654(7)])]. given #678 (T,wt=7): 5768 (L * x')' <= x. [para(5654(a,1),4425(a,2))]. given #679 (T,wt=7): 5769 (x' * L)' <= x. [para(5654(a,1),4428(a,2))]. given #680 (T,wt=7): 5770 x <= (y /\ x')'. [para(5654(a,1),4432(a,1))]. given #681 (T,wt=7): 5771 (x' \/ y)' <= x. [para(5654(a,1),4434(a,2))]. given #682 (A,wt=17): 239 c4 \/ (c2 ^ * (c1 * c3))' = (c2 ^ * (c1 * c3))'. [resolve(84,a,42,a)]. given #683 (F,wt=8): 5782 c3 /\ (c1 * c3)' != c3. [ur(109,a,5688,a),rewrite([35(6)])]. given #684 (F,wt=8): 5852 (c3 ^ * c4 ^)' != L. [ur(468,a,4770,a),flip(a)]. given #685 (F,wt=8): 5853 (c4 ^ * c4 ^)' != L. [ur(468,a,4772,a),flip(a)]. given #686 (F,wt=8): 5904 -(c3 * c4 <= (c1 * c3)'). [ur(1484,a,5670,a),rewrite([5654(5)])]. given #687 (T,wt=7): 5772 x <= (x' /\ y)'. [para(5654(a,1),4435(a,1))]. given #688 (T,wt=7): 5773 (x \/ y')' <= y. [para(5654(a,1),4449(a,2))]. given #689 (T,wt=7): 5776 x' <= O | -(L <= x). [para(5654(a,1),4786(b,2))]. given #690 (T,wt=7): 5777 L <= x' | -(x <= O). [para(5654(a,1),4787(b,1))]. given #691 (A,wt=9): 244 c3 * (L * x) = c3 * x. [para(87(a,1),54(a,1,1)),flip(a)]. given #692 (F,wt=8): 5909 x \/ (y \/ c1') != O. [para(5372(a,1),903(a,1,2,2))]. given #693 (F,wt=8): 5970 x \/ (c1' \/ y) != O. [ur(522,a,5908,a(flip)),rewrite([37(4)])]. given #694 (F,wt=8): 5972 x \/ L * c1' != O. [ur(523,a,5966,a(flip))]. given #695 (F,wt=8): 5973 L * c1' \/ x != O. [ur(522,a,5966,a(flip))]. given #696 (T,wt=5): 6223 c3 * c3 = c3. [para(88(a,1),244(a,1,2)),rewrite([87(3)]),flip(a)]. given #697 (T,wt=5): 6224 c3 * c4 = c3. [para(91(a,1),244(a,1,2)),rewrite([87(3)]),flip(a)]. given #698 (T,wt=7): 5786 c1' * c1 <= I'. [resolve(5655,a,153,a),rewrite([75(4),5654(5)])]. given #699 (T,wt=7): 5921 x /\ I <= c1' ^. [para(5373(a,1),110(b,1,2)),xx(b)]. given #700 (A,wt=9): 251 L * (c3 * x) = L * x. [para(88(a,1),54(a,1,1)),flip(a)]. given #701 (F,wt=6): 6267 -(L * c1' <= O). [ur(42,b,5973,a)]. given #702 (F,wt=7): 6389 -(L <= (L * c1')'). [ur(4786,a,6267,a)]. given #703 (F,wt=7): 6390 -(L * c1' ^ <= O). [ur(61,a,6267,a),rewrite([346(2),469(7)])]. given #704 (F,wt=6): 6394 -(L <= c1' ^'). [ur(59,a,6390,a),rewrite([3048(2),346(3),897(3)])]. given #705 (T,wt=7): 5923 I <= x \/ c1' ^. [para(5373(a,1),696(a,1))]. given #706 (T,wt=7): 5924 I <= c1' ^ \/ x. [para(5373(a,1),114(b,1,1)),rewrite([102(10)]),xx(b)]. given #707 (T,wt=7): 5925 I <= c1' ^ * L. [para(5373(a,1),900(a,1))]. given #708 (T,wt=7): 5926 I <= L * c1' ^. [para(5373(a,1),924(a,1))]. given #709 (A,wt=11): 257 -(x <= I) | x \/ c3 * c3 ^ <= I. [resolve(89,a,80,b)]. given #710 (F,wt=5): 6395 -(c1' ^ <= O). [ur(5777,a,6394,a)]. given #711 (F,wt=5): 6446 c1' ^ != O. [ur(432,a,6395,a),flip(a)]. given #712 (F,wt=6): 6396 c1' ^' != L. [ur(468,a,6394,a),flip(a)]. given #713 (F,wt=7): 6391 (L * c1')' != L. [ur(468,a,6389,a),flip(a)]. given #714 (T,wt=7): 5932 c1' ^' <= I'. [para(5373(a,1),4432(a,2,1))]. given #715 (T,wt=7): 5938 x <= x * c1' ^. [resolve(5915,a,72,a),rewrite([55(2)])]. given #716 (T,wt=7): 5939 x <= c1' ^ * x. [resolve(5915,a,71,a),rewrite([56(2)])]. given #717 (T,wt=7): 5977 x ^ <= x' ^'. [resolve(5674,a,1481,a),rewrite([5654(3)])]. given #718 (A,wt=11): 258 -(x <= I) | c3 * c3 ^ \/ x <= I. [resolve(89,a,80,a)]. given #719 (F,wt=7): 6393 L * c1' ^ != O. [ur(432,a,6390,a),flip(a)]. given #720 (F,wt=7): 6447 x \/ c1' ^ != O. [ur(523,a,6446,a(flip))]. given #721 (F,wt=7): 6448 c1' ^ \/ x != O. [ur(522,a,6446,a(flip))]. given #722 (F,wt=7): 6449 c1' ^ * L != O. [ur(449,b,6446,a(flip))]. given #723 (T,wt=7): 5990 x ^' ^ <= x'. [para(75(a,1),5674(a,2,1))]. given #724 (T,wt=7): 6218 (c1' * L)' <= O. [resolve(5776,b,5395,a)]. given #725 (T,wt=7): 6219 (L * c1')' <= O. [resolve(5776,b,5394,a)]. given #726 (T,wt=7): 6332 I <= (c1' * c1)'. [resolve(5786,a,1481,a),rewrite([5654(3)])]. given #727 (A,wt=10): 259 c3 * c3 ^ /\ x <= I /\ x. [resolve(89,a,74,a)]. given #728 (F,wt=8): 5974 L * (c1' * L) != O. [ur(449,b,5966,a(flip)),rewrite([54(6)])]. given #729 (F,wt=8): 6039 x \/ c1' * L != O. [ur(523,a,5968,a(flip))]. given #730 (F,wt=8): 6040 c1' * L \/ x != O. [ur(522,a,5968,a(flip))]. given #731 (F,wt=6): 6599 -(c1' * L <= O). [ur(42,b,6040,a)]. given #732 (T,wt=7): 6353 I /\ x <= c1' ^. [para(35(a,1),5921(a,1))]. given #733 (T,wt=7): 6511 x <= x ^' ^'. [para(75(a,1),5977(a,1))]. given #734 (T,wt=7): 6541 x' ^' ^ <= x. [para(5654(a,1),5990(a,2))]. given #735 (T,wt=7): 6550 (c1' * L)' = O. [resolve(6218,a,44,a),rewrite([35(7),208(7)]),flip(a)]. given #736 (A,wt=10): 260 c3 * c3 ^ \/ x <= I \/ x. [resolve(89,a,73,a)]. given #737 (F,wt=7): 6600 -(c1' ^ * L <= O). [ur(59,a,6599,a),rewrite([346(5),469(7)])]. given #738 (F,wt=8): 6392 -(L <= (L * c1' ^)'). [ur(4786,a,6390,a)]. given #739 (F,wt=8): 6678 -(L <= (c1' ^ * L)'). [ur(4786,a,6600,a)]. given #740 (F,wt=8): 6679 (L * c1' ^)' != L. [ur(468,a,6392,a),flip(a)]. given #741 (T,wt=6): 6654 c1' * L = L. [para(6550(a,1),50(a,1,2)),rewrite([34(6),209(6)])]. given #742 (T,wt=7): 6559 (L * c1')' = O. [resolve(6219,a,44,a),rewrite([35(7),208(7)]),flip(a)]. given #743 (T,wt=6): 6712 L * c1' = L. [para(6559(a,1),50(a,1,2)),rewrite([34(6),209(6)])]. given #744 (T,wt=6): 6738 c3 * c1' = c3. [para(6712(a,1),244(a,1,2)),rewrite([87(3)]),flip(a)]. given #745 (A,wt=9): 264 c3 ^ * I' <= c3 ^'. [resolve(89,a,58,a)]. given #746 (F,wt=7): 6704 c1' * c4 ^ != O. [para(6654(a,1),3332(b,1,2)),rewrite([897(10)]),xx(b)]. given #747 (F,wt=9): 5699 c3' \/ c1 * c3 != c3'. [back_rewrite(4658),rewrite([5654(5),94(4),5654(6)])]. given #748 (F,wt=9): 5709 -(c3 ^ * (c1 * c3) <= c4'). [back_rewrite(4481),rewrite([5654(5),94(4),5654(6)])]. given #749 (F,wt=9): 5850 c1 /\ (c3 * c3 ^)' != c1. [ur(109,a,5686,a),rewrite([35(7)])]. given #750 (T,wt=7): 6685 L * c1' ^ = L. [para(6654(a,1),68(a,1,1)),rewrite([3048(2),3048(3)]),flip(a)]. given #751 (T,wt=7): 6717 c1' ^ * L = L. [para(6712(a,1),68(a,1,1)),rewrite([3048(2),3048(6)]),flip(a)]. given #752 (T,wt=7): 6817 c3 * c1' ^ = c3. [para(6685(a,1),244(a,1,2)),rewrite([87(3)]),flip(a)]. given #753 (T,wt=8): 2526 x' /\ (y /\ x) = O. [resolve(2514,a,63,b),flip(a)]. given #754 (A,wt=11): 265 I /\ c3 * c3 ^ = c3 * c3 ^. [resolve(89,a,44,a),rewrite([35(6)])]. ============================== PROOF ================================= % Proof 1 at 0.47 (+ 0.02) seconds. % Length of proof is 79. % Level of proof is 10. % Maximum clause weight is 14. % Given clauses 754. 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]. 7 x <= y -> z * x <= z * y # label(non_clause). [assumption]. 11 point(x) <-> x * L = x & L * x = L & x * x ^ <= I # label(non_clause). [assumption]. 12 irreflexive(x) <-> x <= I' # label(non_clause). [assumption]. 16 (all p all q (symmetric(z) & irreflexive(z) & (x ^ * z) * p != L & coloringProperty(x,z) & point(p) & point(q) & q <= ((x ^ * z) * p)' -> ((p * q ^) * q) * p ^ <= z')) # label(non_clause) # label(goal). [goal]. 18 -point(x) | x * L = x. [clausify(11)]. 19 -point(x) | L * x = L. [clausify(11)]. 20 -point(x) | x * x ^ <= I. [clausify(11)]. 21 point(c3). [deny(16)]. 22 point(c4). [deny(16)]. 24 -irreflexive(x) | x <= I'. [clausify(12)]. 25 irreflexive(c1). [deny(16)]. 34 x \/ y = y \/ x. [assumption]. 35 x /\ y = y /\ x. [assumption]. 38 x /\ (y /\ z) = (x /\ y) /\ z. [assumption]. 39 (x /\ y) /\ z = x /\ (y /\ z). [copy(38),flip(a)]. 42 -(x <= y) | x \/ y = y. [clausify(1)]. 44 -(x <= y) | x /\ y = x. [clausify(2)]. 45 x <= y | x /\ y != x. [clausify(2)]. 46 x /\ (y \/ z) = (x /\ y) \/ (x /\ z). [assumption]. 49 L = x \/ x'. [assumption]. 50 x \/ x' = L. [copy(49),flip(a)]. 51 O = x /\ x'. [assumption]. 52 x /\ x' = O. [copy(51),flip(a)]. 53 x * (y * z) = (x * y) * z. [assumption]. 54 (x * y) * z = x * (y * z). [copy(53),flip(a)]. 58 -(x * y <= z) | x ^ * z' <= y'. [clausify(3)]. 67 x * (y \/ z) = x * y \/ x * z. [assumption]. 68 (x * y) ^ = y ^ * x ^. [assumption]. 70 (x /\ y) ^ = x ^ /\ y ^. [assumption]. 72 -(x <= y) | z * x <= z * y. [clausify(7)]. 75 x ^ ^ = x. [assumption]. 76 O <= x. [assumption]. 77 x <= L. [assumption]. 85 -(((c3 * c4 ^) * c4) * c3 ^ <= c1'). [deny(16)]. 86 -(c3 * (c4 ^ * (c4 * c3 ^)) <= c1'). [copy(85),rewrite([54(6),54(9),54(8)])]. 87 c3 * L = c3. [resolve(21,a,18,a)]. 89 c3 * c3 ^ <= I. [resolve(21,a,20,a)]. 90 c4 * L = c4. [resolve(22,a,18,a)]. 91 L * c4 = L. [resolve(22,a,19,a)]. 93 c1 <= I'. [resolve(25,a,24,a)]. 101 x /\ (y /\ z) = y /\ (x /\ z). [para(35(a,1),39(a,1,1)),rewrite([39(2)])]. 110 x /\ y <= z | x /\ (y /\ z) != x /\ y. [para(39(a,1),45(b,1))]. 132 (x /\ y) \/ (x /\ y') = x /\ L. [para(50(a,1),46(a,1,2)),flip(a)]. 180 x * y \/ x * y' = x * L. [para(50(a,1),67(a,1,2)),flip(a)]. 208 O /\ x = O. [resolve(76,a,44,a)]. 209 O \/ x = x. [resolve(76,a,42,a)]. 216 x * y <= x * L. [resolve(77,a,72,a)]. 220 x /\ L = x. [resolve(77,a,44,a)]. 222 (x /\ y) \/ (x /\ y') = x. [back_rewrite(132),rewrite([220(6)])]. 250 L ^ * c3 ^ = c3 ^. [para(87(a,1),68(a,1,1)),flip(a)]. 265 I /\ c3 * c3 ^ = c3 * c3 ^. [resolve(89,a,44,a),rewrite([35(6)])]. 279 c4 ^ * L ^ = L ^. [para(91(a,1),68(a,1,1)),flip(a)]. 296 c1 /\ I' = c1. [resolve(93,a,44,a)]. 343 x /\ O = O. [para(208(a,1),35(a,1)),flip(a)]. 362 x /\ (y /\ x') = O. [para(52(a,1),101(a,1,2)),rewrite([343(2)]),flip(a)]. 382 L /\ x = x. [para(220(a,1),35(a,1)),flip(a)]. 385 x ^ /\ L ^ = x ^. [para(220(a,1),70(a,1,1)),flip(a)]. 469 L' = O. [para(382(a,1),52(a,1))]. 545 c4 * x <= c4. [para(90(a,1),216(a,2))]. 589 c4 ^ * c4' <= x'. [resolve(545,a,58,a)]. 1936 L ^ <= c4 ^ * L. [para(279(a,1),216(a,1))]. 1963 L ^ /\ c4 ^ * L = L ^. [resolve(1936,a,44,a)]. 2754 I /\ c1 = O. [para(296(a,1),362(a,1,2))]. 2913 x /\ L ^ = x. [para(75(a,1),385(a,1,1)),rewrite([75(5)])]. 3048 L ^ = L. [para(2913(a,1),382(a,1)),flip(a)]. 3067 c4 ^ * L = L. [back_rewrite(1963),rewrite([3048(2),382(6),3048(6)])]. 3269 L * c3 ^ = c3 ^. [back_rewrite(250),rewrite([3048(2)])]. 3921 c4 ^ * c4' <= O. [para(469(a,1),589(a,2))]. 3977 c4 ^ * c4' = O. [resolve(3921,a,44,a),rewrite([35(7),208(7)]),flip(a)]. 4006 c4 ^ * c4 = L. [para(3977(a,1),180(a,1,2)),rewrite([34(6),209(6),3067(8)])]. 4011 c4 ^ * (c4 * x) = L * x. [para(4006(a,1),54(a,1,1)),flip(a)]. 4068 -(c3 * c3 ^ <= c1'). [back_rewrite(86),rewrite([4011(8),3269(5)])]. 5323 I /\ c1' = I. [para(2754(a,1),222(a,1,1)),rewrite([209(6)])]. 5378 x /\ I <= c1'. [para(5323(a,1),110(b,1,2)),xx(b)]. 5407 I /\ x <= c1'. [para(35(a,1),5378(a,1))]. 6914 $F. [para(265(a,1),5407(a,1)),unit_del(a,4068)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=754. Generated=21470. Kept=6869. proofs=1. Usable=545. Sos=4343. Demods=736. Limbo=7, Disabled=2042. Hints=0. Weight_deleted=70. Literals_deleted=0. Forward_subsumed=14530. Back_subsumed=170. Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. New_demodulators=1057 (6 lex), Back_demodulated=1802. Back_unit_deleted=0. Demod_attempts=288377. Demod_rewrites=41135. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=21349. Nonunit_bsub_feature_tests=10163. Megabytes=6.76. User_CPU=0.48, System_CPU=0.02, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED Exiting with 1 proof. Process 6345 exit (max_proofs) Thu Mar 26 12:06:42 2015