============================== Prover9 =============================== Prover9 (32) version Dec-2007, Dec 2007. Process 6344 was started by peterhoefner on callisto.dynhost.nicta.com.au, Thu Mar 26 12:06:31 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 ^) * x ^ <= 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 ^) * x ^ <= 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 ^) * c2 ^ <= 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 ^ * c2 ^) <= c1'). [copy(85),rewrite([54(7)])]. 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=10): 86 -(c3 * (c4 ^ * c2 ^) <= c1'). [copy(85),rewrite([54(7)])]. 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=10): 240 -(c1'' * (c2 * c4) <= c3'). [ur(61,a,86,a),rewrite([68(9),75(6),75(7)])]. given #63 (F,wt=13): 241 -(c3 ^ * c1'' <= (c4 ^ * c2 ^)'). [ur(59,a,86,a)]. given #64 (F,wt=13): 243 c1' \/ c3 * (c4 ^ * c2 ^) != c1'. [ur(43,a,86,a),rewrite([34(10)])]. given #65 (F,wt=13): 365 -(c1'' ^ * c3'' <= (c2 * c4)'). [ur(59,a,240,a)]. 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=13): 367 c3' \/ c1'' * (c2 * c4) != c3'. [ur(43,a,240,a),rewrite([34(10)])]. given #72 (F,wt=14): 166 x * y != O | L * (x * (y * L)) != L. [para(54(a,1),65(b,1,2)),flip(a)]. given #73 (F,wt=12): 412 x * c3 != O | L * (x * c3) != L. [para(87(a,1),166(b,1,2,2))]. given #74 (F,wt=12): 413 x * c4 != O | L * (x * c4) != L. [para(90(a,1),166(b,1,2,2))]. 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=14): 364 -(c3'' * (c4 ^ * c2 ^) <= c1'''). [ur(61,a,240,a),rewrite([68(7)])]. given #81 (F,wt=14): 369 -(c3 * (c4 ^ * c2 ^)'' <= c1'''). [ur(59,a,241,a),rewrite([75(3)])]. given #82 (F,wt=14): 373 -(c1'' * (c2 * c4)'' <= c3'''). [ur(59,a,365,a),rewrite([75(5)])]. given #83 (F,wt=14): 441 -(c1'''' * (c2 * c4) <= c3'''). [ur(61,a,364,a),rewrite([68(11),75(8),75(9)])]. 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): 380 L /\ x = x. [para(220(a,1),35(a,1)),flip(a)]. given #87 (T,wt=4): 471 L' = O. [para(380(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): 368 -((c4 ^ * c2 ^)'' * c1'' ^ <= c3 ^'). [ur(61,a,241,a)]. given #90 (F,wt=16): 372 -((c2 * c4)'' * c3'' ^ <= c1'' ^'). [ur(61,a,365,a)]. given #91 (F,wt=16): 414 x * (y * c3) != O | L * (x * (y * c3)) != L. [para(54(a,1),412(b,1,2)),rewrite([54(3)])]. given #92 (F,wt=12): 501 x * L != O | L * (x * L) != L. [para(88(a,1),414(b,1,2,2)),rewrite([88(3)])]. given #93 (T,wt=5): 381 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): 428 x <= O | O != x. [para(343(a,1),45(b,1))]. given #96 (T,wt=6): 470 L <= x | L != x. [para(380(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=16): 416 x * (y * c4) != O | L * (x * (y * c4)) != L. [para(54(a,1),413(b,1,2)),rewrite([54(3)])]. given #99 (F,wt=16): 503 x * (y * L) != O | L * (x * (y * L)) != L. [para(54(a,1),501(b,1,2)),rewrite([54(3)])]. given #100 (F,wt=17): 442 -(c3'' ^ * c1'''' <= (c4 ^ * c2 ^)'). [ur(59,a,364,a)]. given #101 (F,wt=17): 445 -(c1'''' * (c4 ^ * c2 ^)'' ^ <= c3'). [ur(61,a,369,a)]. 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=17): 446 -(c3 ^ * c1'''' <= (c4 ^ * c2 ^)'''). [ur(59,a,369,a)]. given #108 (F,wt=17): 449 -(c3'''' * (c2 * c4)'' ^ <= c1'''). [ur(61,a,373,a)]. given #109 (F,wt=17): 450 -(c1'' ^ * c3'''' <= (c2 * c4)'''). [ur(59,a,373,a)]. given #110 (F,wt=17): 454 -(c1'''' ^ * c3'''' <= (c2 * c4)'). [ur(59,a,441,a)]. 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): 611 x <= L * x. [para(56(a,1),217(a,1))]. given #114 (T,wt=5): 614 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=17): 490 -(c3 ^'' * c1'' <= (c4 ^ * c2 ^)'''). [ur(61,a,368,a),rewrite([75(9)])]. given #117 (F,wt=17): 494 -(c1'' ^'' * c3'' <= (c2 * c4)'''). [ur(61,a,372,a),rewrite([75(11)])]. given #118 (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 #119 (F,wt=5): 654 c3 \/ x != O. [para(87(a,1),177(b,1,1,2)),rewrite([88(7),381(10)]),xx(b)]. given #120 (T,wt=5): 615 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=3): 658 -(c3 <= O). [ur(42,b,654,a)]. given #126 (F,wt=5): 655 x \/ c3 != O. [para(87(a,1),177(b,1,2,2)),rewrite([88(11),34(10),381(10)]),xx(b)]. given #127 (F,wt=5): 656 c4 \/ x != O. [para(90(a,1),177(b,1,1,2)),rewrite([91(7),381(10)]),xx(b)]. given #128 (F,wt=3): 699 -(c4 <= O). [ur(42,b,656,a)]. 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): 427 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=5): 657 x \/ c4 != O. [para(90(a,1),177(b,1,2,2)),rewrite([91(11),34(10),381(10)]),xx(b)]. given #135 (F,wt=7): 659 x \/ (c3 \/ y) != O. [para(99(a,1),654(a,1))]. given #136 (F,wt=7): 698 x \/ (y \/ c3) != O. [para(37(a,1),655(a,1))]. given #137 (F,wt=7): 700 x \/ (c4 \/ y) != O. [para(99(a,1),656(a,1))]. given #138 (T,wt=6): 751 x /\ c1 <= I'. [para(296(a,1),110(b,1,2)),xx(b)]. given #139 (T,wt=6): 763 c1 /\ x <= I'. [para(35(a,1),751(a,1))]. given #140 (T,wt=7): 463 x <= y \/ (x \/ z). [para(99(a,1),356(a,2))]. given #141 (T,wt=6): 783 c1 <= x \/ I'. [para(297(a,1),463(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=7): 752 x \/ (y \/ c4) != O. [para(37(a,1),657(a,1))]. given #144 (F,wt=9): 753 x \/ (y \/ (c3 \/ z)) != O. [para(37(a,1),659(a,1))]. given #145 (F,wt=9): 754 x \/ (y \/ (z \/ c3)) != O. [para(37(a,1),698(a,1,2))]. given #146 (F,wt=9): 755 x \/ (y \/ (c4 \/ z)) != O. [para(37(a,1),700(a,1))]. given #147 (T,wt=6): 790 c1 <= I' \/ x. [para(34(a,1),783(a,2))]. given #148 (T,wt=7): 468 x /\ (y /\ z) <= z. [para(39(a,1),358(a,1))]. given #149 (T,wt=7): 509 c1 /\ I' ^ = c1. [para(296(a,1),70(a,1,1)),rewrite([94(2),94(3)]),flip(a)]. given #150 (T,wt=5): 844 c1 <= I' ^. [resolve(509,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=9): 826 x \/ (y \/ (z \/ c4)) != O. [para(37(a,1),752(a,1,2))]. given #153 (F,wt=10): 649 I \/ x != O | L * L != L. [para(56(a,1),177(b,1,1,2)),rewrite([506(12)])]. given #154 (F,wt=10): 650 x \/ I != O | L * L != L. [para(56(a,1),177(b,1,2,2)),rewrite([34(12),506(12)])]. given #155 (F,wt=11): 827 x \/ (y \/ (z \/ (c3 \/ u))) != O. [para(37(a,1),753(a,1,2))]. given #156 (T,wt=7): 515 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): 925 L * L = L. [para(554(a,1),380(a,1)),flip(a)]. given #159 (T,wt=7): 622 x /\ L * x = x. [resolve(611,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): 935 I != O. [back_rewrite(167),rewrite([925(6)]),xx(b)]. given #162 (F,wt=5): 931 x \/ I != O. [back_rewrite(650),rewrite([925(7)]),xx(b)]. given #163 (F,wt=5): 932 I \/ x != O. [back_rewrite(649),rewrite([925(7)]),xx(b)]. given #164 (F,wt=3): 964 -(I <= O). [ur(42,b,932,a)]. given #165 (T,wt=7): 724 x /\ y <= z \/ y. [para(40(a,1),357(a,2,2))]. given #166 (T,wt=7): 726 x /\ y <= z \/ x. [para(102(a,1),357(a,2,2))]. given #167 (T,wt=7): 729 c3 * x <= y \/ c3. [para(249(a,1),357(a,2,2))]. given #168 (T,wt=7): 730 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): 929 x \/ (y \/ I) != O. [back_rewrite(915),rewrite([925(8)]),xx(b)]. given #171 (F,wt=7): 930 x \/ (I \/ y) != O. [back_rewrite(914),rewrite([925(8)]),xx(b)]. given #172 (F,wt=9): 1031 x \/ (y \/ (z \/ I)) != O. [para(37(a,1),929(a,1,2))]. given #173 (F,wt=9): 1032 x \/ (y \/ (I \/ z)) != O. [para(37(a,1),930(a,1))]. given #174 (T,wt=7): 782 x /\ y <= y \/ z. [para(103(a,1),463(a,2))]. given #175 (T,wt=7): 850 x /\ c1 <= I' ^. [para(509(a,1),110(b,1,2)),xx(b)]. given #176 (T,wt=7): 928 x /\ y <= y * L. [para(554(a,1),110(b,1,2)),xx(b)]. given #177 (T,wt=6): 1065 c1 <= I' * L. [para(296(a,1),928(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): 828 x \/ (y \/ (z \/ (u \/ c3))) != O. [para(37(a,1),754(a,1,2,2))]. given #180 (F,wt=11): 829 x \/ (y \/ (z \/ (c4 \/ u))) != O. [para(37(a,1),755(a,1,2))]. given #181 (F,wt=11): 913 x \/ (y \/ (z \/ (u \/ c4))) != O. [para(37(a,1),826(a,1,2,2))]. given #182 (F,wt=11): 1033 x \/ (y \/ (z \/ (u \/ I))) != O. [para(37(a,1),1031(a,1,2,2))]. given #183 (T,wt=7): 949 x /\ y <= L * y. [para(622(a,1),110(b,1,2)),xx(b)]. given #184 (T,wt=6): 1104 c1 <= L * I'. [para(296(a,1),949(a,1))]. given #185 (T,wt=7): 974 x /\ c3 * y <= c3. [para(249(a,1),724(a,2))]. given #186 (T,wt=7): 975 x /\ c4 * y <= c4. [para(272(a,1),724(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=11): 1034 x \/ (y \/ (z \/ (I \/ u))) != O. [para(37(a,1),1032(a,1,2))]. given #189 (F,wt=13): 916 x \/ (y \/ (z \/ (u \/ (c3 \/ w)))) != O. [para(37(a,1),827(a,1,2,2))]. given #190 (F,wt=13): 1089 x \/ (y \/ (z \/ (u \/ (w \/ c3)))) != O. [para(37(a,1),828(a,1,2,2,2))]. given #191 (F,wt=13): 1090 x \/ (y \/ (z \/ (u \/ (c4 \/ w)))) != O. [para(37(a,1),829(a,1,2,2))]. given #192 (T,wt=7): 976 c1 <= x \/ I' ^. [para(509(a,1),724(a,1))]. given #193 (T,wt=7): 977 x <= y \/ x * L. [para(554(a,1),724(a,1))]. given #194 (T,wt=7): 978 x <= y \/ L * x. [para(622(a,1),724(a,1))]. given #195 (T,wt=7): 985 x /\ y <= x \/ z. [para(34(a,1),726(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=13): 1091 x \/ (y \/ (z \/ (u \/ (w \/ c4)))) != O. [para(37(a,1),913(a,1,2,2,2))]. given #198 (F,wt=13): 1092 x \/ (y \/ (z \/ (u \/ (w \/ I)))) != O. [para(37(a,1),1033(a,1,2,2,2))]. given #199 (F,wt=13): 1134 x \/ (y \/ (z \/ (u \/ (I \/ w)))) != O. [para(37(a,1),1034(a,1,2,2))]. given #200 (F,wt=15): 1135 x \/ (y \/ (z \/ (u \/ (w \/ (c3 \/ v5))))) != O. [para(37(a,1),916(a,1,2,2,2))]. given #201 (T,wt=7): 992 c3 * x /\ y <= c3. [para(249(a,1),726(a,2))]. given #202 (T,wt=7): 993 c4 * x /\ y <= c4. [para(272(a,1),726(a,2))]. given #203 (T,wt=7): 1004 c3 * x <= c3 \/ y. [para(34(a,1),729(a,2))]. given #204 (T,wt=7): 1016 c4 * x <= c4 \/ y. [para(34(a,1),730(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=15): 1136 x \/ (y \/ (z \/ (u \/ (w \/ (v5 \/ c3))))) != O. [para(37(a,1),1089(a,1,2,2,2,2))]. given #207 (F,wt=15): 1137 x \/ (y \/ (z \/ (u \/ (w \/ (c4 \/ v5))))) != O. [para(37(a,1),1090(a,1,2,2,2))]. given #208 (F,wt=15): 1190 x \/ (y \/ (z \/ (u \/ (w \/ (v5 \/ c4))))) != O. [para(37(a,1),1091(a,1,2,2,2,2))]. given #209 (F,wt=15): 1191 x \/ (y \/ (z \/ (u \/ (w \/ (v5 \/ I))))) != O. [para(37(a,1),1092(a,1,2,2,2,2))]. given #210 (T,wt=7): 1028 c1 <= I' ^ \/ x. [para(509(a,1),114(b,1,1)),rewrite([102(10)]),xx(b)]. given #211 (T,wt=7): 1029 x <= x * L \/ y. [para(554(a,1),114(b,1,1)),rewrite([102(6)]),xx(b)]. given #212 (T,wt=7): 1030 x <= L * x \/ y. [para(622(a,1),114(b,1,1)),rewrite([102(6)]),xx(b)]. given #213 (T,wt=7): 1051 c1 /\ x <= I' ^. [para(35(a,1),850(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=15): 1192 x \/ (y \/ (z \/ (u \/ (w \/ (I \/ v5))))) != O. [para(37(a,1),1134(a,1,2,2,2))]. given #216 (F,wt=17): 1193 x \/ (y \/ (z \/ (u \/ (w \/ (v5 \/ (c3 \/ v6)))))) != O. [para(37(a,1),1135(a,1,2,2,2,2))]. given #217 (F,wt=17): 1288 x \/ (y \/ (z \/ (u \/ (w \/ (v5 \/ (v6 \/ c3)))))) != O. [para(37(a,1),1136(a,1,2,2,2,2,2))]. given #218 (F,wt=17): 1289 x \/ (y \/ (z \/ (u \/ (w \/ (v5 \/ (c4 \/ v6)))))) != O. [para(37(a,1),1137(a,1,2,2,2,2))]. given #219 (T,wt=7): 1060 x /\ y <= x * L. [para(35(a,1),928(a,1))]. given #220 (T,wt=7): 1066 c1 <= I' ^ * L. [para(509(a,1),928(a,1))]. given #221 (T,wt=7): 1067 x <= L * (x * L). [para(622(a,1),928(a,1)),rewrite([54(4)])]. given #222 (T,wt=7): 1100 x /\ y <= L * x. [para(35(a,1),949(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=17): 1290 x \/ (y \/ (z \/ (u \/ (w \/ (v5 \/ (v6 \/ c4)))))) != O. [para(37(a,1),1190(a,1,2,2,2,2,2))]. given #225 (F,wt=17): 1291 x \/ (y \/ (z \/ (u \/ (w \/ (v5 \/ (v6 \/ I)))))) != O. [para(37(a,1),1191(a,1,2,2,2,2,2))]. given #226 (F,wt=17): 1370 x \/ (y \/ (z \/ (u \/ (w \/ (v5 \/ (I \/ v6)))))) != O. [para(37(a,1),1192(a,1,2,2,2,2))]. given #227 (F,wt=18): 242 c1' /\ c3 * (c4 ^ * c2 ^) != c3 * (c4 ^ * c2 ^). [ur(45,a,86,a),rewrite([35(10)])]. given #228 (T,wt=7): 1105 c1 <= L * I' ^. [para(509(a,1),949(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): 1464 I ^ * x = x. [para(75(a,1),186(a,1,2)),rewrite([75(5)])]. given #231 (T,wt=4): 1479 I ^ = I. [para(1464(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=18): 366 c3' /\ c1'' * (c2 * c4) != c1'' * (c2 * c4). [ur(45,a,240,a),rewrite([35(10)])]. given #234 (F,wt=18): 375 (c2 * c4)' \/ c1'' ^ * c3'' != (c2 * c4)'. [ur(43,a,365,a),rewrite([34(13)])]. given #235 (F,wt=18): 408 x * (y * z) != O | L * (x * (y * (z * L))) != L. [para(54(a,1),166(b,1,2,2))]. given #236 (F,wt=18): 453 -(c3'''' * (c4 ^ * c2 ^) <= c1'''''). [ur(61,a,441,a),rewrite([68(9)])]. 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): 1545 O ^ * L <= x'. [para(346(a,1),223(a,1,2))]. given #240 (T,wt=6): 1556 O ^ * L <= O. [para(471(a,1),1545(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=18): 527 -(c3'' * (c4 ^ * c2 ^)'' <= c1'''''). [ur(59,a,442,a),rewrite([75(5)])]. given #243 (F,wt=18): 580 -(c3 * (c4 ^ * c2 ^)'''' <= c1'''''). [ur(59,a,446,a),rewrite([75(3)])]. given #244 (F,wt=18): 583 -(c1'''' * (c2 * c4)'' <= c3'''''). [ur(61,a,449,a),rewrite([75(12)])]. given #245 (F,wt=18): 588 -(c1'' * (c2 * c4)'''' <= c3'''''). [ur(59,a,450,a),rewrite([75(5)])]. given #246 (T,wt=6): 1564 O ^ * L = O. [resolve(1556,a,44,a),rewrite([35(6),208(6)]),flip(a)]. given #247 (T,wt=4): 1613 O ^ = O. [para(1564(a,1),63(b,1,2)),rewrite([79(7)]),flip(a),unit_del(b,165)]. given #248 (T,wt=8): 250 L ^ * c3 ^ = c3 ^. [para(87(a,1),68(a,1,1)),flip(a)]. given #249 (T,wt=7): 1623 c3 ^ <= L ^ * L. [para(250(a,1),216(a,1))]. 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): 646 x \/ y != O | L * (y * L) \/ L * (x * L) != L. [para(34(a,1),177(b,1))]. given #252 (F,wt=18): 1526 -(c1'''''' * (c2 * c4) <= c3'''''). [ur(61,a,453,a),rewrite([68(13),75(10),75(11)])]. given #253 (F,wt=18): 1687 O != x | L * (x * L) \/ L * ((y /\ x) * L) != L. [para(40(a,1),646(a,1)),rewrite([34(12)]),flip(a)]. given #254 (F,wt=12): 1703 x' != O | L * (x' * L) != L. [para(52(a,1),1687(b,1,2,2,1)),rewrite([78(12),79(11),34(10),209(10)]),flip(a)]. given #255 (T,wt=8): 256 c3 ^ * L ^ = L ^. [para(88(a,1),68(a,1,1)),flip(a)]. given #256 (T,wt=7): 1717 L ^ <= c3 ^ * L. [para(256(a,1),216(a,1))]. given #257 (T,wt=8): 261 x * (c3 * c3 ^) <= x. [resolve(89,a,72,a),rewrite([55(7)])]. given #258 (T,wt=8): 262 c3 * (c3 ^ * x) <= x. [resolve(89,a,71,a),rewrite([54(5),56(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=12): 1707 L * x != O | L * (x * L) != L. [para(622(a,1),1687(b,1,2,2,1)),rewrite([54(9),936(10),323(13)]),flip(a)]. given #261 (F,wt=16): 1710 x' /\ y != O | L * ((x' /\ y) * L) != L. [para(210(a,1),1687(b,1,2,2,1)),rewrite([78(14),79(13),34(12),209(12)]),flip(a)]. given #262 (F,wt=16): 1802 L * (x * y) != O | L * (x * (y * L)) != L. [para(54(a,1),1707(b,1,2))]. given #263 (F,wt=14): 1809 L * (x * c3) != O | L * (x * c3) != L. [para(87(a,1),1802(b,1,2,2))]. given #264 (T,wt=7): 1759 c3 * L ^ <= L ^. [para(256(a,1),262(a,1,2))]. given #265 (T,wt=8): 266 I \/ c3 * c3 ^ = I. [resolve(89,a,42,a),rewrite([34(6)])]. given #266 (T,wt=8): 273 L ^ * c4 ^ = c4 ^. [para(90(a,1),68(a,1,1)),flip(a)]. given #267 (T,wt=7): 1838 c4 ^ <= L ^ * L. [para(273(a,1),216(a,1))]. 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=14): 1810 L * (x * c4) != O | L * (x * c4) != L. [para(90(a,1),1802(b,1,2,2))]. given #270 (F,wt=14): 1811 L * (x * L) != O | L * (x * L) != L. [para(925(a,1),1802(b,1,2,2))]. given #271 (F,wt=16): 1804 x' /\ y != O | L * ((y /\ x') * L) != L. [para(35(a,1),1710(b,1,2,1))]. given #272 (F,wt=10): 1947 c1 != O | L * (c1 * L) != L. [para(296(a,1),1804(b,1,2,1)),rewrite([35(4),296(4)])]. given #273 (T,wt=8): 279 c4 ^ * L ^ = L ^. [para(91(a,1),68(a,1,1)),flip(a)]. given #274 (T,wt=7): 1954 L ^ <= c4 ^ * L. [para(279(a,1),216(a,1))]. given #275 (T,wt=8): 284 x * (c4 * c4 ^) <= x. [resolve(92,a,72,a),rewrite([55(7)])]. given #276 (T,wt=8): 285 c4 * (c4 ^ * x) <= x. [resolve(92,a,71,a),rewrite([54(5),56(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=18): 1692 O != x | L * (x * L) \/ L * ((x /\ y) * L) != L. [para(102(a,1),646(a,1)),rewrite([34(12)]),flip(a)]. given #279 (F,wt=18): 1695 I' != O | L * (c1 * L) \/ L * (I' * L) != L. [para(297(a,1),646(a,1)),rewrite([34(16)])]. given #280 (F,wt=18): 1812 L * (x * (y * c3)) != O | L * (x * (y * c3)) != L. [para(54(a,1),1809(a,1,2)),rewrite([54(11)])]. given #281 (F,wt=18): 1941 L * (x * (y * c4)) != O | L * (x * (y * c4)) != L. [para(54(a,1),1810(a,1,2)),rewrite([54(11)])]. given #282 (T,wt=7): 2002 c4 * L ^ <= L ^. [para(279(a,1),285(a,1,2))]. given #283 (T,wt=7): 2060 c1 = O | I' != O. [para(63(b,1),1695(b,1,1)),rewrite([381(15)]),flip(a),xx(c)]. 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=18): 1943 L * (x * (y * L)) != O | L * (x * (y * L)) != L. [para(54(a,1),1811(a,1,2)),rewrite([54(11)])]. given #288 (F,wt=19): 444 c1''' \/ c3'' * (c4 ^ * c2 ^) != c1'''. [ur(43,a,364,a),rewrite([34(14)])]. given #289 (F,wt=19): 448 c1''' \/ c3 * (c4 ^ * c2 ^)'' != c1'''. [ur(43,a,369,a),rewrite([34(14)])]. given #290 (F,wt=19): 452 c3''' \/ c1'' * (c2 * c4)'' != c3'''. [ur(43,a,373,a),rewrite([34(14)])]. given #291 (T,wt=7): 2094 c1 /\ I'' <= O. [para(52(a,1),292(a,2))]. given #292 (T,wt=7): 2148 c1 /\ I'' = O. [resolve(2094,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): 2164 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=19): 456 c3''' \/ c1'''' * (c2 * c4) != c3'''. [ur(43,a,441,a),rewrite([34(14)])]. given #297 (F,wt=19): 491 -((c4 ^ * c2 ^)'' ^ * c3 ^'' <= c1'' ^'). [ur(59,a,368,a)]. given #298 (F,wt=19): 495 -((c2 * c4)'' ^ * c1'' ^'' <= c3'' ^'). [ur(59,a,372,a)]. given #299 (F,wt=19): 1371 x \/ (y \/ (z \/ (u \/ (w \/ (v5 \/ (v6 \/ (c3 \/ v7))))))) != O. [para(37(a,1),1193(a,1,2,2,2,2,2))]. given #300 (T,wt=4): 2201 I <= L ^. [para(925(a,1),150(a,1,2)),rewrite([35(3),380(3),380(5),380(7),940(6)])]. given #301 (T,wt=6): 2219 x <= x * L ^. [resolve(2201,a,72,a),rewrite([55(2)])]. given #302 (T,wt=5): 2234 c3 ^ <= L ^. [para(256(a,1),2219(a,2))]. given #303 (T,wt=5): 2235 c4 ^ <= L ^. [para(279(a,1),2219(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=19): 1372 x \/ (y \/ (z \/ (u \/ (w \/ (v5 \/ (v6 \/ (v7 \/ c3))))))) != O. [para(37(a,1),1288(a,1,2,2,2,2,2,2))]. given #306 (F,wt=19): 1373 x \/ (y \/ (z \/ (u \/ (w \/ (v5 \/ (v6 \/ (c4 \/ v7))))))) != O. [para(37(a,1),1289(a,1,2,2,2,2,2))]. given #307 (F,wt=19): 1446 x \/ (y \/ (z \/ (u \/ (w \/ (v5 \/ (v6 \/ (v7 \/ c4))))))) != O. [para(37(a,1),1290(a,1,2,2,2,2,2,2))]. given #308 (F,wt=19): 1447 x \/ (y \/ (z \/ (u \/ (w \/ (v5 \/ (v6 \/ (v7 \/ I))))))) != O. [para(37(a,1),1291(a,1,2,2,2,2,2,2))]. given #309 (T,wt=6): 2220 x <= L ^ * x. [resolve(2201,a,71,a),rewrite([56(2)])]. given #310 (T,wt=6): 2221 I /\ L ^ = I. [resolve(2201,a,44,a)]. given #311 (T,wt=6): 2307 x /\ I <= L ^. [para(2221(a,1),110(b,1,2)),xx(b)]. given #312 (T,wt=6): 2309 I <= x \/ L ^. [para(2221(a,1),724(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): 2313 L ^ != O. [para(2221(a,1),1687(b,1,2,2,1)),rewrite([56(14),925(13),34(12),381(12)]),flip(a),xx(b)]. given #315 (F,wt=19): 1448 x \/ (y \/ (z \/ (u \/ (w \/ (v5 \/ (v6 \/ (I \/ v7))))))) != O. [para(37(a,1),1370(a,1,2,2,2,2,2))]. given #316 (F,wt=20): 370 c3 ^ * c1'' /\ (c4 ^ * c2 ^)' != c3 ^ * c1''. [ur(45,a,241,a)]. given #317 (F,wt=20): 371 c3 ^ * c1'' \/ (c4 ^ * c2 ^)' != (c4 ^ * c2 ^)'. [ur(43,a,241,a)]. given #318 (T,wt=6): 2310 I <= L ^ \/ x. [para(2221(a,1),114(b,1,1)),rewrite([102(9)]),xx(b)]. given #319 (T,wt=6): 2311 I <= L ^ * L. [para(2221(a,1),928(a,1))]. given #320 (T,wt=6): 2312 I <= L * L ^. [para(2221(a,1),949(a,1))]. given #321 (T,wt=6): 2321 I /\ x <= L ^. [para(35(a,1),2307(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=20): 493 c3 ^' \/ (c4 ^ * c2 ^)'' * c1'' ^ != c3 ^'. [ur(43,a,368,a),rewrite([34(16)])]. given #324 (F,wt=20): 498 x * (y * (z * c3)) != O | L * (x * (y * (z * c3))) != L. [para(54(a,1),414(b,1,2,2)),rewrite([54(3)])]. given #325 (F,wt=20): 518 x * (y * (z * c4)) != O | L * (x * (y * (z * c4))) != L. [para(54(a,1),416(b,1,2,2)),rewrite([54(3)])]. given #326 (F,wt=20): 521 x * (y * (z * L)) != O | L * (x * (y * (z * L))) != L. [para(54(a,1),503(b,1,2,2)),rewrite([54(3)])]. given #327 (T,wt=6): 2337 L ^' <= I'. [resolve(153,a,2201,a),rewrite([1479(2),56(5)])]. given #328 (T,wt=7): 2175 I' \/ c1' = L. [resolve(2164,a,44,a),rewrite([46(7),380(4),380(6)])]. given #329 (T,wt=7): 2222 I \/ L ^ = L ^. [resolve(2201,a,42,a)]. given #330 (T,wt=8): 294 x * c1 <= x * I'. [resolve(93,a,72,a)]. given #331 (A,wt=11): 157 -(x <= y) | y' * x ^ <= I'. [para(56(a,1),60(a,1))]. given #332 (F,wt=6): 2512 x \/ L ^ != O. [para(2222(a,1),930(a,1,2))]. given #333 (F,wt=6): 2609 L ^ \/ x != O. [para(34(a,1),2512(a,1))]. given #334 (F,wt=4): 2610 -(L ^ <= O). [ur(42,b,2609,a)]. given #335 (F,wt=8): 2513 x \/ (y \/ L ^) != O. [para(2222(a,1),1032(a,1,2,2))]. given #336 (T,wt=8): 295 c1 * x <= I' * x. [resolve(93,a,71,a)]. given #337 (T,wt=8): 308 c1'' * c2 <= c2'. [resolve(95,a,60,a),rewrite([75(6)])]. given #338 (T,wt=8): 342 x \/ (y \/ x') = L. [para(50(a,1),99(a,1,2)),rewrite([221(2)]),flip(a)]. given #339 (T,wt=8): 362 x /\ (y /\ x') = O. [para(52(a,1),101(a,1,2)),rewrite([343(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): 2611 x \/ (L ^ \/ y) != O. [para(99(a,1),2609(a,1))]. given #342 (F,wt=10): 2514 x \/ (y \/ (z \/ L ^)) != O. [para(2222(a,1),1034(a,1,2,2,2))]. given #343 (F,wt=10): 2707 x \/ (y \/ (L ^ \/ z)) != O. [para(37(a,1),2611(a,1))]. given #344 (F,wt=12): 2515 x \/ (y \/ (z \/ (u \/ L ^))) != O. [para(2222(a,1),1134(a,1,2,2,2,2))]. given #345 (T,wt=5): 2652 I /\ c1 = O. [para(296(a,1),362(a,1,2))]. given #346 (T,wt=6): 2712 c1 <= O | c1 != O. [para(2652(a,1),108(b,1)),rewrite([2652(4)]),flip(b)]. given #347 (T,wt=6): 2713 c1 <= I | c1 != O. [para(2652(a,1),109(b,1)),flip(b)]. given #348 (T,wt=7): 2709 I /\ (c1 /\ x) = O. [para(2652(a,1),39(a,1,1)),rewrite([208(2)]),flip(a)]. 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): 2708 x \/ (y \/ (z \/ (L ^ \/ u))) != O. [para(37(a,1),2707(a,1,2))]. given #351 (F,wt=14): 2516 x \/ (y \/ (z \/ (u \/ (w \/ L ^)))) != O. [para(2222(a,1),1192(a,1,2,2,2,2,2))]. given #352 (F,wt=14): 2723 c1 /\ x != O | L * ((c1 /\ x) * L) != L. [para(2709(a,1),1687(b,1,2,2,1)),rewrite([78(14),79(13),34(12),209(12)]),flip(a)]. given #353 (F,wt=14): 2772 x \/ (y \/ (z \/ (u \/ (L ^ \/ w)))) != O. [para(37(a,1),2708(a,1,2,2))]. given #354 (T,wt=7): 2710 c1 /\ (x /\ I) = O. [para(2652(a,1),39(a,2,2)),rewrite([35(4),343(6)])]. given #355 (T,wt=7): 2711 I /\ (x /\ c1) = O. [para(2652(a,1),101(a,1,2)),rewrite([343(2)]),flip(a)]. given #356 (T,wt=8): 376 -(x <= y) | x \/ y <= y. [resolve(360,a,80,b)]. given #357 (T,wt=8): 377 -(x <= y) | y \/ x <= y. [resolve(360,a,80,a)]. 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=14): 2773 c1 /\ x != O | L * ((x /\ c1) * L) != L. [para(35(a,1),2723(b,1,2,1))]. given #360 (F,wt=14): 2781 x /\ I != O | L * ((x /\ I) * L) != L. [para(2710(a,1),1687(b,1,2,2,1)),rewrite([78(14),79(13),34(12),209(12)]),flip(a)]. given #361 (F,wt=14): 2788 x /\ c1 != O | L * ((x /\ c1) * L) != L. [para(2711(a,1),1687(b,1,2,2,1)),rewrite([78(14),79(13),34(12),209(12)]),flip(a)]. given #362 (F,wt=14): 2834 x /\ I != O | L * ((I /\ x) * L) != L. [para(35(a,1),2781(b,1,2,1))]. given #363 (T,wt=7): 2795 x \/ y <= y \/ x. [resolve(377,a,782,a),rewrite([37(3),340(3)])]. given #364 (T,wt=8): 383 x ^ /\ L ^ = x ^. [para(220(a,1),70(a,1,1)),flip(a)]. given #365 (T,wt=5): 2847 x ^ <= L ^. [resolve(383,a,45,b)]. given #366 (T,wt=4): 2951 x <= L ^. [para(75(a,1),2847(a,1))]. 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): 2859 x ^ != O | L * (x ^ * L) != L. [para(383(a,1),1692(b,1,2,2,1)),rewrite([323(14)]),flip(a)]. given #369 (F,wt=14): 2836 x /\ c1 != O | L * ((c1 /\ x) * L) != L. [para(35(a,1),2788(b,1,2,1))]. given #370 (F,wt=16): 2660 x /\ y' != O | L * ((x /\ y') * L) != L. [para(362(a,1),1687(b,1,2,2,1)),rewrite([78(14),79(13),34(12),209(12)]),flip(a)]. given #371 (F,wt=16): 2775 x \/ (y \/ (z \/ (u \/ (w \/ (L ^ \/ v5))))) != O. [para(37(a,1),2772(a,1,2,2,2))]. given #372 (T,wt=6): 2850 x /\ L ^ = x. [para(75(a,1),383(a,1,1)),rewrite([75(5)])]. given #373 (T,wt=4): 2971 L ^ = L. [para(2850(a,1),380(a,1)),flip(a)]. given #374 (T,wt=6): 2868 I <= c4 ^ * c4. [back_rewrite(2193),rewrite([2850(7)])]. given #375 (T,wt=6): 2870 I <= c3 ^ * c3. [back_rewrite(2191),rewrite([2850(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): 3081 -(L <= O). [back_rewrite(2610),rewrite([2971(2)])]. given #378 (F,wt=16): 2965 x /\ y' != O | L * ((y' /\ x) * L) != L. [para(35(a,1),2660(b,1,2,1))]. given #379 (F,wt=18): 2774 c1 /\ (x /\ y) != O | L * ((x /\ (c1 /\ y)) * L) != L. [para(101(a,1),2723(b,1,2,1))]. given #380 (F,wt=18): 2833 c1 /\ (x /\ y) != O | L * ((x /\ (y /\ c1)) * L) != L. [para(39(a,1),2773(b,1,2,1))]. given #381 (T,wt=6): 2990 c4 ^ * L = L. [back_rewrite(1981),rewrite([2971(2),380(6),2971(6)])]. given #382 (T,wt=6): 2998 c3 ^ * L = L. [back_rewrite(1738),rewrite([2971(2),380(6),2971(6)])]. given #383 (T,wt=6): 3092 L <= I | I != L. [back_rewrite(2306),rewrite([2971(2),2971(5)]),flip(b)]. given #384 (T,wt=7): 3181 x <= x * (L * x). [back_rewrite(937),rewrite([2971(2),2971(3),936(4)])]. 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): 3255 c4 ^ != O. [para(2990(a,1),65(b,1,2)),rewrite([925(7)]),flip(a),xx(b)]. given #387 (F,wt=4): 3262 c3 ^ != O. [para(2998(a,1),65(b,1,2)),rewrite([925(7)]),flip(a),xx(b)]. given #388 (F,wt=6): 3257 c4 ^ \/ x != O. [para(2990(a,1),177(b,1,1,2)),rewrite([925(8),381(11)]),xx(b)]. given #389 (F,wt=4): 3304 -(c4 ^ <= O). [ur(42,b,3257,a)]. given #390 (T,wt=7): 3189 L * c4 ^ = c4 ^. [back_rewrite(273),rewrite([2971(2)])]. given #391 (T,wt=7): 3192 L * c3 ^ = c3 ^. [back_rewrite(250),rewrite([2971(2)])]. given #392 (T,wt=7): 3307 x * c4 ^ <= c4 ^. [para(3189(a,1),217(a,2))]. given #393 (T,wt=7): 3311 x * c3 ^ <= c3 ^. [para(3192(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): 3258 x \/ c4 ^ != O. [para(2990(a,1),177(b,1,2,2)),rewrite([925(12),34(11),381(11)]),xx(b)]. given #396 (F,wt=6): 3264 c3 ^ \/ x != O. [para(2998(a,1),177(b,1,1,2)),rewrite([925(8),381(11)]),xx(b)]. given #397 (F,wt=4): 3372 -(c3 ^ <= O). [ur(42,b,3264,a)]. given #398 (F,wt=6): 3265 x \/ c3 ^ != O. [para(2998(a,1),177(b,1,2,2)),rewrite([925(12),34(11),381(11)]),xx(b)]. given #399 (T,wt=8): 394 x \/ (x' \/ y) = L. [back_rewrite(129),rewrite([381(5)])]. given #400 (T,wt=8): 435 x \/ (y /\ x)' = L. [para(50(a,1),103(a,1,2)),rewrite([221(2)]),flip(a)]. given #401 (T,wt=8): 502 x * L != O | O = x. [resolve(501,b,63,b)]. given #402 (T,wt=8): 563 c3' * x ^ <= c3'. [resolve(544,a,60,a)]. 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): 3305 x \/ (c4 ^ \/ y) != O. [para(99(a,1),3257(a,1))]. given #405 (F,wt=8): 3371 x \/ (y \/ c4 ^) != O. [para(37(a,1),3258(a,1))]. given #406 (F,wt=8): 3373 x \/ (c3 ^ \/ y) != O. [para(99(a,1),3264(a,1))]. given #407 (F,wt=8): 3374 x \/ (y \/ c3 ^) != O. [para(37(a,1),3265(a,1))]. given #408 (T,wt=7): 3415 c3' * x <= c3'. [para(75(a,1),563(a,1,2))]. given #409 (T,wt=8): 564 c3 ^ * c3' <= x'. [resolve(544,a,58,a)]. given #410 (T,wt=7): 3480 c3 ^ * c3' <= O. [para(471(a,1),564(a,2))]. given #411 (T,wt=5): 3490 c3 <= c3''. [resolve(3480,a,58,a),rewrite([75(3),346(3),87(3)])]. 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): 3449 x \/ (y \/ (c4 ^ \/ z)) != O. [para(37(a,1),3305(a,1))]. given #414 (F,wt=10): 3450 x \/ (y \/ (z \/ c4 ^)) != O. [para(37(a,1),3371(a,1,2))]. given #415 (F,wt=10): 3451 x \/ (y \/ (c3 ^ \/ z)) != O. [para(37(a,1),3373(a,1))]. given #416 (F,wt=10): 3452 x \/ (y \/ (z \/ c3 ^)) != O. [para(37(a,1),3374(a,1,2))]. given #417 (T,wt=7): 3491 c3 ^ * c3' = O. [resolve(3480,a,44,a),rewrite([35(7),208(7)]),flip(a)]. given #418 (T,wt=7): 3501 c3 /\ c3'' = c3. [resolve(3490,a,44,a)]. given #419 (T,wt=7): 3528 c3' ^ * c3 = O. [para(3491(a,1),68(a,1,1)),rewrite([1613(2),75(7)]),flip(a)]. given #420 (T,wt=7): 3544 x /\ c3 <= c3''. [para(3501(a,1),110(b,1,2)),xx(b)]. 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): 3251 L * ((c1' /\ (x /\ c1)) * L) != L. [ur(2833,a,210,a)]. given #423 (F,wt=12): 3519 x \/ (y \/ (z \/ (c4 ^ \/ u))) != O. [para(37(a,1),3449(a,1,2))]. given #424 (F,wt=12): 3520 x \/ (y \/ (z \/ (u \/ c4 ^))) != O. [para(37(a,1),3450(a,1,2,2))]. given #425 (F,wt=12): 3521 x \/ (y \/ (z \/ (c3 ^ \/ u))) != O. [para(37(a,1),3451(a,1,2))]. given #426 (T,wt=7): 3546 c3 <= x \/ c3''. [para(3501(a,1),724(a,1))]. given #427 (T,wt=7): 3547 c3 <= c3'' \/ x. [para(3501(a,1),114(b,1,1)),rewrite([102(10)]),xx(b)]. given #428 (T,wt=7): 3548 c3 <= c3'' * L. [para(3501(a,1),928(a,1))]. given #429 (T,wt=7): 3549 c3 <= L * c3''. [para(3501(a,1),949(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=12): 3522 x \/ (y \/ (z \/ (u \/ c3 ^))) != O. [para(37(a,1),3452(a,1,2,2))]. given #432 (F,wt=13): 3256 x * c4 ^ != O | L * (x * L) != L. [para(2990(a,1),166(b,1,2,2))]. given #433 (F,wt=6): 3668 c3 * c4 ^ != O. [para(87(a,1),3256(b,1,2)),rewrite([88(9)]),xx(b)]. given #434 (F,wt=6): 3669 c4 * c4 ^ != O. [para(90(a,1),3256(b,1,2)),rewrite([91(9)]),xx(b)]. given #435 (T,wt=6): 3663 c3 ^ * c3 = L. [para(3491(a,1),180(a,1,2)),rewrite([34(6),209(6),2998(8)])]. given #436 (T,wt=7): 3571 c3 /\ x <= c3''. [para(35(a,1),3544(a,1))]. given #437 (T,wt=8): 599 c4' * x ^ <= c4'. [resolve(545,a,60,a)]. given #438 (T,wt=7): 3716 c4' * x <= c4'. [para(75(a,1),599(a,1,2))]. 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): 3670 c4 ^ * c4 ^ != O. [para(2990(a,1),3256(b,1,2)),rewrite([925(10)]),xx(b)]. given #441 (F,wt=7): 3671 c3 ^ * c4 ^ != O. [para(2998(a,1),3256(b,1,2)),rewrite([925(10)]),xx(b)]. given #442 (F,wt=13): 3263 x * c3 ^ != O | L * (x * L) != L. [para(2998(a,1),166(b,1,2,2))]. given #443 (F,wt=6): 3775 c3 * c3 ^ != O. [para(87(a,1),3263(b,1,2)),rewrite([88(9)]),xx(b)]. given #444 (T,wt=8): 600 c4 ^ * c4' <= x'. [resolve(545,a,58,a)]. given #445 (T,wt=7): 3793 c4 ^ * c4' <= O. [para(471(a,1),600(a,2))]. given #446 (T,wt=5): 3803 c4 <= c4''. [resolve(3793,a,58,a),rewrite([75(3),346(3),90(3)])]. given #447 (T,wt=7): 3804 c4 ^ * c4' = O. [resolve(3793,a,44,a),rewrite([35(7),208(7)]),flip(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=6): 3776 c4 * c3 ^ != O. [para(90(a,1),3263(b,1,2)),rewrite([91(9)]),xx(b)]. given #450 (F,wt=7): 3777 c4 ^ * c3 ^ != O. [para(2990(a,1),3263(b,1,2)),rewrite([925(10)]),xx(b)]. given #451 (F,wt=7): 3778 c3 ^ * c3 ^ != O. [para(2998(a,1),3263(b,1,2)),rewrite([925(10)]),xx(b)]. given #452 (F,wt=14): 3596 L * ((c1' /\ (x /\ (y /\ c1))) * L) != L. [para(39(a,1),3251(a,1,2,1,2))]. given #453 (T,wt=6): 3833 c4 ^ * c4 = L. [para(3804(a,1),180(a,1,2)),rewrite([34(6),209(6),2990(8)])]. given #454 (T,wt=7): 3814 c4 /\ c4'' = c4. [resolve(3803,a,44,a)]. given #455 (T,wt=7): 3821 c4' ^ * c4 = O. [para(3804(a,1),68(a,1,1)),rewrite([1613(2),75(7)]),flip(a)]. given #456 (T,wt=7): 3909 x /\ c4 <= c4''. [para(3814(a,1),110(b,1,2)),xx(b)]. 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=14): 3597 x \/ (y \/ (z \/ (u \/ (c4 ^ \/ w)))) != O. [para(37(a,1),3519(a,1,2,2))]. given #459 (F,wt=14): 3598 x \/ (y \/ (z \/ (u \/ (w \/ c4 ^)))) != O. [para(37(a,1),3520(a,1,2,2,2))]. given #460 (F,wt=14): 3599 x \/ (y \/ (z \/ (u \/ (c3 ^ \/ w)))) != O. [para(37(a,1),3521(a,1,2,2))]. given #461 (F,wt=14): 3665 x \/ (y \/ (z \/ (u \/ (w \/ c3 ^)))) != O. [para(37(a,1),3522(a,1,2,2,2))]. given #462 (T,wt=7): 3911 c4 <= x \/ c4''. [para(3814(a,1),724(a,1))]. given #463 (T,wt=7): 3912 c4 <= c4'' \/ x. [para(3814(a,1),114(b,1,1)),rewrite([102(10)]),xx(b)]. given #464 (T,wt=7): 3913 c4 <= c4'' * L. [para(3814(a,1),928(a,1))]. given #465 (T,wt=7): 3914 c4 <= L * c4''. [para(3814(a,1),949(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=12): 4039 -(c4 * (c3 ^ * c1'') <= c2 ^'). [ur(189,a,86,a),rewrite([75(3)])]. given #468 (F,wt=14): 3882 L * ((c1' /\ (x /\ (c1 /\ y))) * L) != L. [para(35(a,1),3596(a,1,2,1,2,2))]. given #469 (F,wt=14): 4038 -(c2 ^ * (c1'' ^ * c3'') <= c4'). [ur(189,a,240,a)]. given #470 (F,wt=14): 4053 -(c3 * (c4 ^ * c2 ^'') <= c1'''). [ur(189,a,4039,a),rewrite([75(3)])]. given #471 (T,wt=7): 3943 c4 /\ x <= c4''. [para(35(a,1),3909(a,1))]. given #472 (T,wt=8): 635 x' <= O | x' != O. [para(52(a,1),108(b,1)),rewrite([52(3)]),flip(b)]. given #473 (T,wt=8): 637 I' <= c1 | I' != c1. [para(296(a,1),108(b,1)),rewrite([296(6)]),flip(b)]. given #474 (T,wt=8): 651 O = x | x \/ y != O. [para(63(b,1),177(b,1,1)),rewrite([381(11)]),xx(c)]. 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=8): 4085 c4 * c3 ^ \/ x != O. [ur(651,a,3776,a(flip))]. given #477 (F,wt=6): 4109 -(c4 * c3 ^ <= O). [ur(42,b,4085,a)]. given #478 (F,wt=4): 4112 -(L <= c4'). [ur(61,a,4109,a),rewrite([346(2),75(4),88(3)])]. given #479 (F,wt=4): 4114 c4' != L. [ur(470,a,4112,a),flip(a)]. given #480 (T,wt=8): 652 O = x | y \/ x != O. [para(63(b,1),177(b,1,2)),rewrite([34(11),381(11)]),xx(c)]. given #481 (T,wt=8): 696 x' <= x | x' != O. [para(52(a,1),109(b,1)),flip(b)]. given #482 (T,wt=8): 764 x /\ (y /\ c1) <= I'. [para(39(a,1),751(a,1))]. given #483 (T,wt=8): 773 x /\ (c1 /\ y) <= I'. [para(101(a,1),763(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=5): 4113 -(L <= c3 ^'). [ur(59,a,4109,a),rewrite([346(4),2990(4)])]. given #486 (F,wt=5): 4168 c3 ^' != L. [ur(470,a,4113,a),flip(a)]. given #487 (F,wt=8): 4086 c3 * c3 ^ \/ x != O. [ur(651,a,3775,a(flip))]. given #488 (F,wt=6): 4169 -(c3 * c3 ^ <= O). [ur(42,b,4086,a)]. given #489 (T,wt=8): 791 c1 <= x \/ (y \/ I'). [para(37(a,1),783(a,2))]. given #490 (T,wt=8): 836 c1 <= x \/ (I' \/ y). [para(99(a,1),790(a,2))]. given #491 (T,wt=8): 934 O = x | L * x != O. [back_rewrite(409),rewrite([925(9)]),xx(c)]. given #492 (T,wt=8): 1074 c1 /\ I' * L = c1. [resolve(1065,a,44,a)]. 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=4): 4171 -(L <= c3'). [ur(61,a,4169,a),rewrite([346(2),75(4),88(3)])]. given #495 (F,wt=4): 4223 c3' != L. [ur(470,a,4171,a),flip(a)]. given #496 (F,wt=8): 4089 c4 * c4 ^ \/ x != O. [ur(651,a,3669,a(flip))]. given #497 (F,wt=6): 4224 -(c4 * c4 ^ <= O). [ur(42,b,4089,a)]. given #498 (T,wt=8): 1112 c1 /\ L * I' = c1. [resolve(1104,a,44,a)]. given #499 (T,wt=8): 1477 -(x <= y) | y' <= x'. [back_rewrite(154),rewrite([1464(5)])]. NOTE: Back_subsumption disabled, ratio of kept to back_subsumed is 27 (0.00 of 0.33 sec). given #500 (T,wt=6): 4334 I'' <= c1'. [resolve(1477,a,93,a)]. given #501 (T,wt=7): 4246 c4''' <= c4'. [resolve(1477,a,3803,a)]. 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=5): 4226 -(L <= c4 ^'). [ur(59,a,4224,a),rewrite([346(4),2990(4)])]. given #504 (F,wt=5): 4377 c4 ^' != L. [ur(470,a,4226,a),flip(a)]. given #505 (F,wt=8): 4090 c3 * c4 ^ \/ x != O. [ur(651,a,3668,a(flip))]. given #506 (F,wt=6): 4378 -(c3 * c4 ^ <= O). [ur(42,b,4090,a)]. given #507 (T,wt=7): 4254 c3''' <= c3'. [resolve(1477,a,3490,a)]. given #508 (T,wt=7): 4284 I' ^' <= c1'. [resolve(1477,a,844,a)]. given #509 (T,wt=7): 4298 (L * x)' <= x'. [resolve(1477,a,611,a)]. given #510 (T,wt=7): 4299 c4' <= (c4 * x)'. [resolve(1477,a,545,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=8): 4110 x \/ c4 * c3 ^ != O. [para(34(a,1),4085(a,1))]. given #513 (F,wt=8): 4117 x \/ c3 * c3 ^ != O. [ur(652,a,3775,a(flip))]. given #514 (F,wt=8): 4120 x \/ c4 * c4 ^ != O. [ur(652,a,3669,a(flip))]. given #515 (F,wt=8): 4121 x \/ c3 * c4 ^ != O. [ur(652,a,3668,a(flip))]. given #516 (T,wt=7): 4300 c3' <= (c3 * x)'. [resolve(1477,a,544,a)]. given #517 (T,wt=7): 4301 (x * L)' <= x'. [resolve(1477,a,541,a)]. given #518 (T,wt=7): 4305 x' <= (y /\ x)'. [resolve(1477,a,358,a)]. given #519 (T,wt=7): 4307 (x \/ y)' <= x'. [resolve(1477,a,356,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=9): 4083 c3 ^ * c3 ^ \/ x != O. [ur(651,a,3778,a(flip))]. given #522 (F,wt=7): 4558 -(c3 ^ * c3 ^ <= O). [ur(42,b,4083,a)]. given #523 (F,wt=5): 4560 -(c3 <= c3 ^'). [ur(59,a,4558,a),rewrite([75(3),346(3),87(3)])]. given #524 (F,wt=7): 4561 c3 /\ c3 ^' != c3. [ur(109,a,4560,a),rewrite([35(5)])]. given #525 (T,wt=7): 4308 x' <= (x /\ y)'. [resolve(1477,a,326,a)]. given #526 (T,wt=7): 4322 (x \/ y)' <= y'. [resolve(1477,a,211,a)]. given #527 (T,wt=8): 1480 x <= y | -(y' <= x'). [para(1464(a,1),59(b,1)),rewrite([56(2)])]. given #528 (T,wt=7): 4633 x <= O | -(L <= x'). [para(346(a,1),1480(b,1))]. 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=4): 4607 -(L <= I'). [ur(1480,a,964,a),rewrite([346(2)])]. given #531 (F,wt=4): 4681 I' != L. [ur(470,a,4607,a),flip(a)]. given #532 (F,wt=5): 4598 -(c3'' <= O). [ur(1480,a,4171,a),rewrite([471(5)])]. given #533 (F,wt=5): 4601 -(c4'' <= O). [ur(1480,a,4112,a),rewrite([471(5)])]. given #534 (T,wt=7): 4634 L <= x | -(x' <= O). [para(471(a,1),1480(b,2))]. given #535 (T,wt=8): 1616 x ^ /\ x' ^ = O. [back_rewrite(195),rewrite([1613(6)])]. given #536 (T,wt=7): 4691 c1 /\ c1' ^ = O. [para(94(a,1),1616(a,1,1))]. given #537 (T,wt=7): 4698 I /\ I' ^ = O. [para(1479(a,1),1616(a,1,1))]. 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=5): 4680 -(I'' <= O). [ur(1480,a,4607,a),rewrite([471(5)])]. given #540 (F,wt=5): 4683 c3'' != O. [ur(635,a,4598,a)]. given #541 (F,wt=5): 4685 c4'' != O. [ur(635,a,4601,a)]. given #542 (F,wt=5): 4778 I'' != O. [ur(635,a,4680,a)]. given #543 (T,wt=8): 1705 x /\ y = O | O != y. [para(63(b,1),1687(b,1,2)),rewrite([34(11),381(11)]),flip(a),xx(c)]. given #544 (T,wt=8): 1829 c3 * c3 ^ <= x \/ I. [para(266(a,1),357(a,2,2))]. given #545 (T,wt=8): 1830 x /\ c3 * c3 ^ <= I. [para(266(a,1),724(a,2))]. given #546 (T,wt=8): 1831 c3 * c3 ^ /\ x <= I. [para(266(a,1),726(a,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=6): 4596 -(c4 ^'' <= O). [ur(1480,a,4226,a),rewrite([471(6)])]. given #549 (F,wt=6): 4600 -(c3 ^'' <= O). [ur(1480,a,4113,a),rewrite([471(6)])]. given #550 (F,wt=6): 4682 -(L <= c3'''). [ur(4633,a,4598,a)]. given #551 (F,wt=6): 4684 -(L <= c4'''). [ur(4633,a,4601,a)]. given #552 (T,wt=8): 2057 x /\ y = O | O != x. [para(63(b,1),1692(b,1,2)),rewrite([34(11),381(11)]),flip(a),xx(c)]. given #553 (T,wt=8): 2082 c4 * c4 ^ <= x \/ I. [para(289(a,1),357(a,2,2))]. given #554 (T,wt=8): 2083 x /\ c4 * c4 ^ <= I. [para(289(a,1),724(a,2))]. given #555 (T,wt=8): 2084 c4 * c4 ^ /\ x <= I. [para(289(a,1),726(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): 4777 -(L <= I'''). [ur(4633,a,4680,a)]. given #558 (F,wt=6): 4897 c4 ^'' != O. [ur(635,a,4596,a)]. given #559 (F,wt=6): 4899 c3 ^'' != O. [ur(635,a,4600,a)]. given #560 (F,wt=6): 4901 c3''' != L. [ur(470,a,4682,a),flip(a)]. given #561 (T,wt=8): 2091 x /\ c1 <= I' /\ x. [para(35(a,1),292(a,1))]. given #562 (T,wt=8): 2092 c1 /\ x <= x /\ I'. [para(35(a,1),292(a,2))]. given #563 (T,wt=8): 2097 c1 <= I' /\ I' ^. [para(509(a,1),292(a,1))]. given #564 (T,wt=8): 2098 c1 <= I' /\ c1 * L. [para(554(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): 4903 c4''' != L. [ur(470,a,4684,a),flip(a)]. given #567 (F,wt=6): 4988 I''' != L. [ur(470,a,4777,a),flip(a)]. given #568 (F,wt=7): 4593 -(c3 ^'' <= c3'). [ur(1480,a,4560,a)]. given #569 (F,wt=7): 4595 -(L <= (c3 * c4 ^)'). [ur(1480,a,4378,a),rewrite([346(2)])]. given #570 (T,wt=8): 2099 c1 <= I' /\ L * c1. [para(622(a,1),292(a,1))]. given #571 (T,wt=8): 2150 c1 <= I'' | c1 != O. [para(2148(a,1),45(b,1)),flip(b)]. given #572 (T,wt=8): 2151 c1 /\ I'' ^ = O. [para(2148(a,1),70(a,1,1)),rewrite([1613(2),94(3)]),flip(a)]. given #573 (T,wt=8): 2161 x \/ c1 <= I' \/ x. [para(34(a,1),293(a,1))]. given #574 (A,wt=13): 204 x ^ * y <= z | -(x * z' <= y'). [para(75(a,1),59(b,1,1))]. given #575 (F,wt=7): 4597 -(L <= (c4 * c4 ^)'). [ur(1480,a,4224,a),rewrite([346(2)])]. given #576 (F,wt=7): 4599 -(L <= (c3 * c3 ^)'). [ur(1480,a,4169,a),rewrite([346(2)])]. given #577 (F,wt=7): 4602 -(L <= (c4 * c3 ^)'). [ur(1480,a,4109,a),rewrite([346(2)])]. given #578 (F,wt=7): 4779 L * c3'' != O. [ur(934,a,4683,a(flip))]. given #579 (T,wt=8): 2162 c1 \/ x <= x \/ I'. [para(34(a,1),293(a,2))]. given #580 (T,wt=8): 2236 x <= x * (x ^ * x). [back_rewrite(1444),rewrite([2231(4)])]. given #581 (T,wt=7): 5155 c1 <= c1 * (c1 * c1). [para(94(a,1),2236(a,2,2,1))]. given #582 (T,wt=8): 2376 x ^ * x' <= I'. [resolve(153,a,360,a)]. 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): 4780 x \/ c3'' != O. [ur(652,a,4683,a(flip))]. given #585 (F,wt=7): 4781 c3'' \/ x != O. [ur(651,a,4683,a(flip))]. given #586 (F,wt=7): 4782 c3'' * L != O. [ur(502,b,4683,a(flip))]. given #587 (F,wt=7): 4783 L * c4'' != O. [ur(934,a,4685,a(flip))]. given #588 (T,wt=7): 5187 c1 * c1' <= I'. [para(94(a,1),2376(a,1,1))]. given #589 (T,wt=8): 2400 c1 * I'' <= I'. [resolve(153,a,93,a),rewrite([94(2)])]. given #590 (T,wt=8): 2580 x' * x ^ <= I'. [resolve(157,a,360,a)]. given #591 (T,wt=7): 5244 c1' * c1 <= I'. [para(94(a,1),2580(a,1,2))]. given #592 (A,wt=10): 222 (x /\ y) \/ (x /\ y') = x. [back_rewrite(132),rewrite([220(6)])]. given #593 (F,wt=7): 4784 x \/ c4'' != O. [ur(652,a,4685,a(flip))]. given #594 (F,wt=7): 4785 c4'' \/ x != O. [ur(651,a,4685,a(flip))]. given #595 (F,wt=7): 4786 c4'' * L != O. [ur(502,b,4685,a(flip))]. given #596 (F,wt=7): 4787 L * I'' != O. [ur(934,a,4778,a(flip))]. given #597 (T,wt=6): 5277 I /\ c1' = I. [para(2652(a,1),222(a,1,1)),rewrite([209(6)])]. given #598 (T,wt=4): 5349 I <= c1'. [resolve(5277,a,45,b)]. given #599 (T,wt=6): 5357 x /\ I <= c1'. [para(5277(a,1),110(b,1,2)),xx(b)]. given #600 (T,wt=6): 5359 I <= x \/ c1'. [para(5277(a,1),724(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): 4788 x \/ I'' != O. [ur(652,a,4778,a(flip))]. given #603 (F,wt=7): 4789 I'' \/ x != O. [ur(651,a,4778,a(flip))]. given #604 (F,wt=7): 4790 I'' * L != O. [ur(502,b,4778,a(flip))]. given #605 (F,wt=7): 4896 -(L <= c4 ^'''). [ur(4633,a,4596,a)]. given #606 (T,wt=6): 5360 I <= c1' \/ x. [para(5277(a,1),114(b,1,1)),rewrite([102(9)]),xx(b)]. given #607 (T,wt=6): 5361 I <= c1' * L. [para(5277(a,1),928(a,1))]. given #608 (T,wt=6): 5362 I <= L * c1'. [para(5277(a,1),949(a,1))]. given #609 (T,wt=6): 5365 c1'' <= I'. [para(5277(a,1),4305(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): 4898 -(L <= c3 ^'''). [ur(4633,a,4600,a)]. given #612 (F,wt=7): 4987 -(I'''' <= O). [ur(4634,a,4777,a)]. given #613 (F,wt=7): 5081 (c3 * c4 ^)' != L. [ur(470,a,4595,a),flip(a)]. given #614 (F,wt=7): 5115 (c4 * c4 ^)' != L. [ur(470,a,4597,a),flip(a)]. given #615 (T,wt=6): 5371 x <= x * c1'. [resolve(5349,a,72,a),rewrite([55(2)])]. given #616 (T,wt=6): 5372 x <= c1' * x. [resolve(5349,a,71,a),rewrite([56(2)])]. given #617 (T,wt=6): 5384 I /\ x <= c1'. [para(35(a,1),5357(a,1))]. given #618 (T,wt=7): 5261 x /\ x'' = x. [para(52(a,1),222(a,1,1)),rewrite([209(5)])]. 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): 5117 (c3 * c3 ^)' != L. [ur(470,a,4599,a),flip(a)]. given #621 (F,wt=7): 5119 (c4 * c3 ^)' != L. [ur(470,a,4602,a),flip(a)]. given #622 (F,wt=7): 5422 c4 ^''' != L. [ur(470,a,4896,a),flip(a)]. given #623 (F,wt=7): 5478 c3 ^''' != L. [ur(470,a,4898,a),flip(a)]. given #624 (T,wt=5): 5530 x <= x''. [resolve(5261,a,45,b)]. given #625 (T,wt=5): 5575 x'' <= x. [resolve(5530,a,1480,b)]. ============================== PROOF ================================= % Proof 1 at 0.40 (+ 0.01) seconds. % Length of proof is 48. % Level of proof is 8. % Maximum clause weight is 18. % Given clauses 625. 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]. 13 symmetric(x) <-> x = x ^ # 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 ^) * x ^ <= z')) # label(non_clause) # label(goal). [goal]. 27 -symmetric(x) | x ^ = x. [clausify(13)]. 28 symmetric(c1). [deny(16)]. 35 x /\ y = y /\ x. [assumption]. 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)]. 55 x * I = x. [assumption]. 56 I * x = x. [assumption]. 59 x * y <= z | -(x ^ * z' <= y'). [clausify(3)]. 61 x * y <= z | -(z' * y ^ <= x'). [clausify(4)]. 68 (x * y) ^ = y ^ * x ^. [assumption]. 75 x ^ ^ = x. [assumption]. 76 O <= x. [assumption]. 77 x <= L. [assumption]. 83 c4 <= ((c2 ^ * c1) * c3)'. [deny(16)]. 84 c4 <= (c2 ^ * (c1 * c3))'. [copy(83),rewrite([54(7)])]. 85 -((c3 * c4 ^) * c2 ^ <= c1'). [deny(16)]. 86 -(c3 * (c4 ^ * c2 ^) <= c1'). [copy(85),rewrite([54(7)])]. 94 c1 ^ = c1. [resolve(28,a,27,a)]. 132 (x /\ y) \/ (x /\ y') = x /\ L. [para(50(a,1),46(a,1,2)),flip(a)]. 186 I ^ * x ^ = x ^. [para(55(a,1),68(a,1,1)),flip(a)]. 189 x * (y * z) <= u | -(y ^ * (x ^ * u') <= z'). [para(68(a,1),59(b,1,1)),rewrite([54(2),54(8)])]. 209 O \/ x = x. [resolve(76,a,42,a)]. 220 x /\ L = x. [resolve(77,a,44,a)]. 222 (x /\ y) \/ (x /\ y') = x. [back_rewrite(132),rewrite([220(6)])]. 240 -(c1'' * (c2 * c4) <= c3'). [ur(61,a,86,a),rewrite([68(9),75(6),75(7)])]. 1464 I ^ * x = x. [para(75(a,1),186(a,1,2)),rewrite([75(5)])]. 1480 x <= y | -(y' <= x'). [para(1464(a,1),59(b,1)),rewrite([56(2)])]. 4038 -(c2 ^ * (c1'' ^ * c3'') <= c4'). [ur(189,a,240,a)]. 4605 -(c4'' <= (c2 ^ * (c1'' ^ * c3''))'). [ur(1480,a,4038,a)]. 5261 x /\ x'' = x. [para(52(a,1),222(a,1,1)),rewrite([209(5)])]. 5530 x <= x''. [resolve(5261,a,45,b)]. 5575 x'' <= x. [resolve(5530,a,1480,b)]. 5612 x'' = x. [resolve(5575,a,44,a),rewrite([35(3),5261(3)]),flip(a)]. 5647 $F. [back_rewrite(4605),rewrite([5612(3),5612(6),94(5),5612(7)]),unit_del(a,84)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=625. Generated=17414. Kept=5602. proofs=1. Usable=506. Sos=3632. Demods=611. Limbo=35, Disabled=1497. Hints=0. Weight_deleted=70. Literals_deleted=0. Forward_subsumed=11741. Back_subsumed=157. Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. New_demodulators=891 (6 lex), Back_demodulated=1270. Back_unit_deleted=0. Demod_attempts=233417. Demod_rewrites=33398. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=16662. Nonunit_bsub_feature_tests=10287. Megabytes=5.76. User_CPU=0.40, System_CPU=0.01, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED Exiting with 1 proof. Process 6344 exit (max_proofs) Thu Mar 26 12:06:31 2015