============================== Prover9 =============================== Prover9 (32) version 2009-11A, November 2009. Process 4312 was started by mccune on cleo, Tue Nov 3 09:38:21 2009 The command was "/home/mccune/LADR/bin/prover9 -t 10 -f qg2.in". ============================== end of head =========================== ============================== INPUT ================================= % Reading from file qg2.in formulas(sos). x * y = x * z -> y = z. y * x = z * x -> y = z. end_of_list. formulas(sos). x * (y * (y * x)) = y * x. end_of_list. formulas(goals). y * (y * x) = x * y. end_of_list. ============================== end of input ========================== % From the command line: assign(max_seconds, 10). ============================== PROCESS NON-CLAUSAL FORMULAS ========== % Formulas that are not ordinary clauses: 1 x * y = x * z -> y = z # label(non_clause). [assumption]. 2 y * x = z * x -> y = z # label(non_clause). [assumption]. 3 y * (y * x) = x * y # 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 != x * z | y = z. [clausify(1)]. x * y != z * y | x = z. [clausify(2)]. x * (y * (y * x)) = y * x. [assumption]. c1 * (c1 * c2) != c2 * c1. [deny(3)]. end_of_list. formulas(demodulators). end_of_list. ============================== PREDICATE ELIMINATION ================= No predicates eliminated. ============================== end predicate elimination ============= Auto_denials: (no changes). Term ordering decisions: Predicate symbol precedence: predicate_order([ = ]). Function symbol precedence: function_order([ c1, c2, * ]). After inverse_order: (no changes). Unfolding symbols: (none). Auto_inference settings: % set(paramodulation). % (positive equality literals) % set(hyper_resolution). % (nonunit Horn with equality) % set(hyper_resolution) -> set(pos_hyper_resolution). % set(neg_ur_resolution). % (nonunit Horn with equality) % assign(para_lit_limit, 2). % (nonunit Horn with equality) Auto_process settings: (no changes). kept: 4 x * y != x * z | y = z. [clausify(1)]. kept: 5 x * y != z * y | x = z. [clausify(2)]. kept: 6 x * (y * (y * x)) = y * x. [assumption]. 7 c1 * (c1 * c2) != c2 * c1. [deny(3)]. kept: 8 c2 * c1 != c1 * (c1 * c2). [copy(7),flip(a)]. ============================== end of process initial clauses ======== ============================== CLAUSES FOR SEARCH ==================== % Clauses after input processing: formulas(usable). end_of_list. formulas(sos). 4 x * y != x * z | y = z. [clausify(1)]. 5 x * y != z * y | x = z. [clausify(2)]. 6 x * (y * (y * x)) = y * x. [assumption]. 8 c2 * c1 != c1 * (c1 * c2). [copy(7),flip(a)]. end_of_list. formulas(demodulators). 6 x * (y * (y * x)) = y * x. [assumption]. end_of_list. ============================== end of clauses for search ============= ============================== SEARCH ================================ % Starting search at 0.01 seconds. given #1 (I,wt=10): 4 x * y != x * z | y = z. [clausify(1)]. given #2 (I,wt=10): 5 x * y != z * y | x = z. [clausify(2)]. given #3 (I,wt=11): 6 x * (y * (y * x)) = y * x. [assumption]. given #4 (I,wt=9): 8 c2 * c1 != c1 * (c1 * c2). [copy(7),flip(a)]. given #5 (A,wt=7): 9 x * (x * x) = x. [hyper(4,a,6,a)]. given #6 (F,wt=13): 15 (c2 * c1) * x != (c1 * (c1 * c2)) * x. [ur(5,b,8,a)]. given #7 (F,wt=13): 16 x * (c2 * c1) != x * (c1 * (c1 * c2)). [ur(4,b,8,a)]. given #8 (F,wt=9): 28 c2 * (c2 * c1) != c1 * c2. [para(6(a,1),16(a,2))]. given #9 (F,wt=13): 29 (c2 * (c2 * c1)) * x != (c1 * c2) * x. [ur(5,b,28,a)]. given #10 (T,wt=9): 14 (x * x) * (x * x) = x. [para(6(a,1),6(a,1,2)),rewrite([9(5)])]. given #11 (T,wt=9): 40 (x * x) * x = x * x. [para(14(a,1),9(a,1,2))]. given #12 (T,wt=5): 41 x * x = x. [hyper(5,a,40,a)]. given #13 (T,wt=8): 42 x * y != x | x = y. [para(40(a,1),4(a,1)),rewrite([41(1),41(1)]),flip(a)]. given #14 (A,wt=14): 10 x * y != z * x | z * (z * x) = y. [para(6(a,1),4(a,1)),flip(a)]. given #15 (F,wt=13): 30 x * (c2 * (c2 * c1)) != x * (c1 * c2). [ur(4,b,28,a)]. given #16 (F,wt=13): 46 (c2 * c1) * (c1 * (c1 * c2)) != c2 * c1. [para(40(a,1),16(a,1)),rewrite([41(7),41(10)]),flip(a)]. given #17 (F,wt=13): 48 (c2 * (c2 * c1)) * (c1 * c2) != c1 * c2. [back_rewrite(36),rewrite([41(12)])]. given #18 (F,wt=13): 51 (c1 * (c1 * c2)) * (c2 * c1) != c2 * c1. [back_rewrite(24),rewrite([41(12)])]. given #19 (T,wt=8): 43 x * y != x | y = x. [para(40(a,1),4(a,2)),rewrite([41(1),41(2)])]. given #20 (T,wt=8): 44 x * y != y | y = x. [para(40(a,1),5(a,1)),rewrite([41(1),41(3)]),flip(a)]. given #21 (T,wt=8): 45 x * y != y | x = y. [para(40(a,1),5(a,2)),rewrite([41(2),41(3)])]. given #22 (T,wt=12): 60 x * y != y | x * (x * y) = y. [para(6(a,1),42(a,1)),flip(b)]. given #23 (A,wt=14): 11 x * (y * (y * z)) != y * z | z = x. [para(6(a,1),5(a,1)),flip(a)]. given #24 (F,wt=13): 57 (c1 * c2) * (c2 * (c2 * c1)) != c1 * c2. [ur(42,b,28,a(flip))]. given #25 (F,wt=15): 47 (c1 * (c1 * c2)) * (c2 * c1) != c1 * (c1 * c2). [para(40(a,1),16(a,2)),rewrite([41(11),41(20)])]. given #26 (F,wt=15): 49 (c1 * c2) * (c2 * (c2 * c1)) != c2 * (c2 * c1). [back_rewrite(35),rewrite([41(14)])]. given #27 (F,wt=15): 50 (c2 * c1) * (c1 * (c1 * c2)) != c1 * (c1 * c2). [back_rewrite(25),rewrite([41(14)])]. given #28 (T,wt=14): 12 x * (y * (y * z)) != y * z | x = z. [para(6(a,1),5(a,2))]. given #29 (T,wt=15): 13 (x * (x * y)) * (y * (x * y)) = x * y. [para(6(a,1),6(a,1,2,2)),rewrite([6(8)])]. given #30 (T,wt=16): 99 x * (x * y) != x * y | x * (x * y) = y. [para(6(a,1),44(a,1)),flip(a)]. given #31 (T,wt=18): 66 x * y != z * y | z * (z * y) = x * (x * y). [para(6(a,1),10(a,1))]. given #32 (A,wt=17): 20 ((c2 * c1) * x) * y != ((c1 * (c1 * c2)) * x) * y. [ur(5,b,15,a)]. given #33 (F,wt=13): 149 (c2 * c1) * (c2 * (c1 * c2)) != c1 * c2. [para(13(a,1),15(a,2))]. given #34 (F,wt=13): 150 (c1 * c2) * (c1 * (c2 * c1)) != c2 * c1. [para(13(a,1),29(a,1)),flip(a)]. given #35 (F,wt=15): 53 (c2 * (c2 * c1)) * (c1 * c2) != c2 * (c2 * c1). [ur(42,b,28,a)]. given #36 (F,wt=15): 64 (c1 * c2) * (c1 * (c2 * c1)) != c1 * (c1 * c2). [ur(10,b,16,a(flip))]. given #37 (T,wt=18): 67 (x * (x * y)) * z != x * y | y * (x * y) = z. [para(6(a,1),10(a,2)),rewrite([6(8)])]. given #38 (T,wt=18): 115 x * (y * (z * y)) != z * y | z * (z * y) = x. [para(6(a,1),11(a,1,2,2)),rewrite([6(6)])]. given #39 (T,wt=19): 148 (x * (y * x)) * ((y * (y * x)) * (y * x)) = y * x. [para(13(a,1),6(a,1,2,2)),rewrite([13(12)])]. given #40 (T,wt=20): 100 x * (x * y) != x * y | y * (x * y) = x * (x * y). [para(6(a,1),60(a,1)),rewrite([6(7)]),flip(a)]. given #41 (A,wt=17): 21 x * ((c2 * c1) * y) != x * ((c1 * (c1 * c2)) * y). [ur(4,b,15,a)]. given #42 (F,wt=15): 69 (c2 * c1) * (c2 * (c1 * c2)) != c2 * (c2 * c1). [ur(10,b,30,a)]. given #43 (F,wt=15): 131 c2 * ((c1 * (c1 * c2)) * (c2 * c1)) != c1 * c2. [ur(10,b,47,a(flip))]. given #44 (F,wt=15): 139 c1 * ((c1 * c2) * (c2 * (c2 * c1))) != c2 * c1. [ur(10,b,49,a(flip))]. given #45 (F,wt=15): 147 c2 * ((c2 * c1) * (c1 * (c1 * c2))) != c1 * c2. [ur(10,b,50,a(flip))]. given #46 (T,wt=20): 153 x * (y * x) != y * x | x * (y * x) = y * (y * x). [para(13(a,1),44(a,1)),flip(a)]. given #47 (T,wt=22): 152 (x * (y * x)) * z != y * x | (y * (y * x)) * (y * x) = z. [para(13(a,1),10(a,2)),rewrite([13(12)])]. given #48 (T,wt=22): 155 x * ((y * (y * z)) * (y * z)) != y * z | z * (y * z) = x. [para(13(a,1),11(a,1,2,2)),rewrite([13(10)])]. given #49 (T,wt=23): 156 ((x * (x * y)) * (x * y)) * ((y * (x * y)) * (x * y)) = x * y. [para(13(a,1),13(a,1,1,2)),rewrite([13(11),13(14)])]. given #50 (A,wt=19): 22 (c1 * (c1 * c2)) * (x * (x * (c2 * c1))) != x * (c2 * c1). [para(6(a,1),15(a,1)),flip(a)]. given #51 (F,wt=15): 196 c1 * ((c2 * (c2 * c1)) * (c1 * c2)) != c2 * c1. [ur(10,b,53,a(flip))]. given #52 (F,wt=15): 205 c2 * ((c1 * c2) * (c1 * (c2 * c1))) != c1 * c2. [ur(10,b,64,a(flip))]. given #53 (F,wt=15): 267 c1 * ((c2 * c1) * (c2 * (c1 * c2))) != c2 * c1. [ur(10,b,69,a(flip))]. given #54 (F,wt=17): 26 (x * (c2 * c1)) * y != (x * (c1 * (c1 * c2))) * y. [ur(5,b,16,a)]. given #55 (T,wt=24): 154 x * (y * x) != y * x | (y * (y * x)) * (y * x) = x * (y * x). [para(13(a,1),60(a,1)),rewrite([13(11)]),flip(a)]. given #56 (T,wt=26): 151 x * (y * (y * z)) != y * z | z * (y * z) = x * (x * (y * (y * z))). [para(13(a,1),10(a,1)),flip(a),flip(b)]. given #57 (T,wt=26): 216 ((x * (x * y)) * (x * y)) * z != x * y | (y * (x * y)) * (x * y) = z. [para(13(a,1),67(a,1,1,2)),rewrite([13(10),13(14)])]. given #58 (T,wt=26): 228 x * ((y * (z * y)) * (z * y)) != z * y | (z * (z * y)) * (z * y) = x. [para(13(a,1),115(a,1,2,2)),rewrite([13(10),13(14)])]. given #59 (A,wt=21): 23 (c2 * c1) * (x * (x * (c1 * (c1 * c2)))) != x * (c1 * (c1 * c2)). [para(6(a,1),15(a,2))]. given #60 (F,wt=17): 27 x * (y * (c2 * c1)) != x * (y * (c1 * (c1 * c2))). [ur(4,b,16,a)]. given #61 (F,wt=17): 31 ((c2 * (c2 * c1)) * x) * y != ((c1 * c2) * x) * y. [ur(5,b,29,a)]. given #62 (F,wt=17): 32 x * ((c2 * (c2 * c1)) * y) != x * ((c1 * c2) * y). [ur(4,b,29,a)]. given #63 (F,wt=17): 70 (x * (c2 * (c2 * c1))) * y != (x * (c1 * c2)) * y. [ur(5,b,30,a)]. given #64 (T,wt=27): 230 ((x * (y * x)) * (y * x)) * (((y * (y * x)) * (y * x)) * (y * x)) = y * x. [para(148(a,1),13(a,1,1,2)),rewrite([148(15),148(18)])]. given #65 (T,wt=28): 157 (x * (x * y)) * (x * y) != x * y | (x * (x * y)) * (x * y) = y * (x * y). [para(13(a,1),99(a,1,2)),rewrite([13(9),13(13)])]. given #66 (T,wt=30): 158 x * (y * (z * y)) != z * y | (z * (z * y)) * (z * y) = x * (x * (y * (z * y))). [para(13(a,1),66(a,1)),rewrite([13(16)]),flip(a),flip(b)]. given #67 (T,wt=30): 235 ((x * (y * x)) * (y * x)) * z != y * x | ((y * (y * x)) * (y * x)) * (y * x) = z. [para(148(a,1),67(a,1,1,2)),rewrite([148(12),148(18)])]. given #68 (A,wt=21): 33 (c1 * c2) * (x * (x * (c2 * (c2 * c1)))) != x * (c2 * (c2 * c1)). [para(6(a,1),29(a,1)),flip(a)]. given #69 (F,wt=17): 71 x * (y * (c2 * (c2 * c1))) != x * (y * (c1 * c2)). [ur(4,b,30,a)]. given #70 (F,wt=17): 74 ((c2 * c1) * (c1 * (c1 * c2))) * x != (c2 * c1) * x. [ur(5,b,46,a)]. given #71 (F,wt=17): 75 x * ((c2 * c1) * (c1 * (c1 * c2))) != x * (c2 * c1). [ur(4,b,46,a)]. given #72 (F,wt=17): 76 (c2 * c1) * ((c2 * c1) * (c1 * (c1 * c2))) != c2 * c1. [ur(42,b,46,a(flip))]. given #73 (T,wt=30): 236 x * (((y * (y * z)) * (y * z)) * (y * z)) != y * z | (z * (y * z)) * (y * z) = x. [para(148(a,1),115(a,1,2,2)),rewrite([148(14),148(18)])]. given #74 (T,wt=31): 237 (((x * (x * y)) * (x * y)) * (x * y)) * (((y * (x * y)) * (x * y)) * (x * y)) = x * y. [para(148(a,1),148(a,1,1,2)),rewrite([148(15),148(17),148(20)])]. given #75 (T,wt=32): 229 (x * (x * y)) * (x * y) != x * y | (y * (x * y)) * (x * y) = (x * (x * y)) * (x * y). [para(148(a,1),60(a,1)),rewrite([148(15)]),flip(a)]. given #76 (T,wt=32): 231 (x * (y * x)) * (y * x) != y * x | (x * (y * x)) * (y * x) = (y * (y * x)) * (y * x). [para(148(a,1),99(a,1,2)),rewrite([148(11),148(15)])]. given #77 (A,wt=19): 34 (c2 * (c2 * c1)) * (x * (x * (c1 * c2))) != x * (c1 * c2). [para(6(a,1),29(a,2))]. given #78 (F,wt=17): 78 ((c2 * (c2 * c1)) * (c1 * c2)) * x != (c1 * c2) * x. [ur(5,b,48,a)]. given #79 (F,wt=17): 79 x * ((c2 * (c2 * c1)) * (c1 * c2)) != x * (c1 * c2). [ur(4,b,48,a)]. given #80 (F,wt=17): 80 (c1 * c2) * ((c2 * (c2 * c1)) * (c1 * c2)) != c1 * c2. [ur(42,b,48,a(flip))]. given #81 (F,wt=17): 82 ((c1 * (c1 * c2)) * (c2 * c1)) * x != (c2 * c1) * x. [ur(5,b,51,a)]. given #82 (T,wt=34): 304 (((x * (x * y)) * (x * y)) * (x * y)) * z != x * y | ((y * (x * y)) * (x * y)) * (x * y) = z. [para(148(a,1),152(a,1,1,2)),rewrite([148(14),148(18),148(20)])]. given #83 (T,wt=34): 315 x * (((y * (z * y)) * (z * y)) * (z * y)) != z * y | ((z * (z * y)) * (z * y)) * (z * y) = x. [para(148(a,1),155(a,1,2,1,2)),rewrite([148(11),148(14),148(20)])]. given #84 (T,wt=35): 318 (((x * (y * x)) * (y * x)) * (y * x)) * ((((y * (y * x)) * (y * x)) * (y * x)) * (y * x)) = y * x. [para(156(a,1),148(a,1,1,2)),rewrite([156(19),156(21),156(24)])]. given #85 (T,wt=36): 240 (x * (y * x)) * (y * x) != y * x | ((y * (y * x)) * (y * x)) * (y * x) = (x * (y * x)) * (y * x). [para(148(a,1),100(a,1,2)),rewrite([148(11),148(17),148(21)])]. given #86 (A,wt=21): 52 ((c2 * (c2 * c1)) * x) * ((c1 * c2) * x) != (c2 * (c2 * c1)) * x. [ur(42,b,29,a)]. given #87 (F,wt=17): 83 x * ((c1 * (c1 * c2)) * (c2 * c1)) != x * (c2 * c1). [ur(4,b,51,a)]. given #88 (F,wt=17): 84 (c2 * c1) * ((c1 * (c1 * c2)) * (c2 * c1)) != c2 * c1. [ur(42,b,51,a(flip))]. given #89 (F,wt=17): 92 ((c1 * (c1 * c2)) * (c2 * c1)) * (c2 * c1) != c2 * c1. [ur(44,b,51,a(flip))]. given #90 (F,wt=17): 93 ((c2 * (c2 * c1)) * (c1 * c2)) * (c1 * c2) != c1 * c2. [ur(44,b,48,a(flip))]. given #91 (T,wt=38): 232 x * ((y * (y * z)) * (y * z)) != y * z | (z * (y * z)) * (y * z) = x * (x * ((y * (y * z)) * (y * z))). [para(148(a,1),66(a,1)),rewrite([148(22)]),flip(a),flip(b)]. given #92 (T,wt=38): 321 (((x * (y * x)) * (y * x)) * (y * x)) * z != y * x | (((y * (y * x)) * (y * x)) * (y * x)) * (y * x) = z. [para(156(a,1),152(a,1,1,2)),rewrite([156(16),156(22),156(24)])]. given #93 (T,wt=38): 322 x * ((((y * (y * z)) * (y * z)) * (y * z)) * (y * z)) != y * z | ((z * (y * z)) * (y * z)) * (y * z) = x. [para(156(a,1),155(a,1,2,1,2)),rewrite([156(15),156(18),156(24)])]. given #94 (T,wt=39): 323 ((((x * (x * y)) * (x * y)) * (x * y)) * (x * y)) * ((((y * (x * y)) * (x * y)) * (x * y)) * (x * y)) = x * y. [para(156(a,1),156(a,1,1,1,2)),rewrite([156(15),156(21),156(23),156(26)])]. given #95 (A,wt=19): 54 (x * (c2 * c1)) * (x * (c1 * (c1 * c2))) != x * (c2 * c1). [ur(42,b,16,a)]. given #96 (F,wt=17): 94 ((c2 * c1) * (c1 * (c1 * c2))) * (c2 * c1) != c2 * c1. [ur(44,b,46,a(flip))]. given #97 (F,wt=17): 116 ((c1 * c2) * (c2 * (c2 * c1))) * (c1 * c2) != c1 * c2. [ur(45,b,57,a)]. given #98 (F,wt=17): 118 (c1 * c2) * ((c1 * c2) * (c2 * (c2 * c1))) != c1 * c2. [ur(43,b,57,a)]. given #99 (F,wt=17): 121 ((c1 * c2) * (c2 * (c2 * c1))) * x != (c1 * c2) * x. [ur(5,b,57,a)]. given #100 (T,wt=40): 294 ((x * (x * y)) * (x * y)) * (x * y) != x * y | ((x * (x * y)) * (x * y)) * (x * y) = (y * (x * y)) * (x * y). [para(148(a,1),153(a,1,2)),rewrite([148(13),148(19),148(23)])]. given #101 (T,wt=42): 316 x * ((y * (z * y)) * (z * y)) != z * y | ((z * (z * y)) * (z * y)) * (z * y) = x * (x * ((y * (z * y)) * (z * y))). [para(156(a,1),66(a,1)),rewrite([156(26)]),flip(a),flip(b)]. given #102 (T,wt=42): 397 ((((x * (x * y)) * (x * y)) * (x * y)) * (x * y)) * z != x * y | (((y * (x * y)) * (x * y)) * (x * y)) * (x * y) = z. [para(156(a,1),216(a,1,1,1,2)),rewrite([156(15),156(18),156(24),156(26)])]. given #103 (T,wt=42): 407 x * ((((y * (z * y)) * (z * y)) * (z * y)) * (z * y)) != z * y | (((z * (z * y)) * (z * y)) * (z * y)) * (z * y) = x. [para(156(a,1),228(a,1,2,1,2)),rewrite([156(15),156(18),156(24),156(26)])]. given #104 (A,wt=19): 55 ((c2 * c1) * x) * ((c1 * (c1 * c2)) * x) != (c2 * c1) * x. [ur(42,b,15,a)]. given #105 (F,wt=17): 122 x * ((c1 * c2) * (c2 * (c2 * c1))) != x * (c1 * c2). [ur(4,b,57,a)]. given #106 (F,wt=17): 172 ((c2 * c1) * (c2 * (c1 * c2))) * x != (c1 * c2) * x. [para(13(a,1),20(a,2,1))]. given #107 (F,wt=17): 174 ((c2 * c1) * (c2 * (c1 * c2))) * (c1 * c2) != c1 * c2. [ur(45,b,149,a)]. given #108 (F,wt=17): 176 (c1 * c2) * ((c2 * c1) * (c2 * (c1 * c2))) != c1 * c2. [ur(43,b,149,a)]. given #109 (T,wt=43): 522 ((((x * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (((((y * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) = y * x. [para(230(a,1),156(a,1,1,1,2)),rewrite([230(17),230(25),230(27),230(30)])]. given #110 (T,wt=44): 319 ((x * (x * y)) * (x * y)) * (x * y) != x * y | ((y * (x * y)) * (x * y)) * (x * y) = ((x * (x * y)) * (x * y)) * (x * y). [para(156(a,1),100(a,1,2)),rewrite([156(15),156(21),156(27)])]. given #111 (T,wt=44): 320 ((x * (y * x)) * (y * x)) * (y * x) != y * x | ((x * (y * x)) * (y * x)) * (y * x) = ((y * (y * x)) * (y * x)) * (y * x). [para(156(a,1),153(a,1,2)),rewrite([156(15),156(21),156(27)])]. given #112 (T,wt=46): 527 ((((x * (y * x)) * (y * x)) * (y * x)) * (y * x)) * z != y * x | ((((y * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x) = z. [para(230(a,1),216(a,1,1,1,2)),rewrite([230(17),230(20),230(28),230(30)])]. given #113 (A,wt=19): 56 ((c1 * c2) * x) * ((c2 * (c2 * c1)) * x) != (c1 * c2) * x. [ur(42,b,29,a(flip))]. given #114 (F,wt=17): 180 x * ((c2 * c1) * (c2 * (c1 * c2))) != x * (c1 * c2). [ur(4,b,149,a)]. given #115 (F,wt=17): 181 ((c1 * c2) * (c1 * (c2 * c1))) * (c2 * c1) != c2 * c1. [ur(45,b,150,a)]. given #116 (F,wt=17): 183 (c2 * c1) * ((c1 * c2) * (c1 * (c2 * c1))) != c2 * c1. [ur(43,b,150,a)]. given #117 (F,wt=17): 187 ((c1 * c2) * (c1 * (c2 * c1))) * x != (c2 * c1) * x. [ur(5,b,150,a)]. given #118 (T,wt=46): 528 x * (((((y * (y * z)) * (y * z)) * (y * z)) * (y * z)) * (y * z)) != y * z | (((z * (y * z)) * (y * z)) * (y * z)) * (y * z) = x. [para(230(a,1),228(a,1,2,1,2)),rewrite([230(19),230(22),230(28),230(30)])]. given #119 (T,wt=47): 533 (((((x * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (((((y * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) = x * y. [para(230(a,1),230(a,1,1,1,2)),rewrite([230(19),230(25),230(27),230(29),230(32)])]. given #120 (T,wt=48): 384 ((x * (y * x)) * (y * x)) * (y * x) != y * x | (((y * (y * x)) * (y * x)) * (y * x)) * (y * x) = ((x * (y * x)) * (y * x)) * (y * x). [para(156(a,1),154(a,1,2)),rewrite([156(15),156(21),156(23),156(29)])]. given #121 (T,wt=50): 385 x * (((y * (y * z)) * (y * z)) * (y * z)) != y * z | ((z * (y * z)) * (y * z)) * (y * z) = x * (x * (((y * (y * z)) * (y * z)) * (y * z))). [para(156(a,1),151(a,1,2,2)),rewrite([156(16),156(22),156(28)])]. given #122 (A,wt=21): 58 (x * (c1 * (c1 * c2))) * (x * (c2 * c1)) != x * (c1 * (c1 * c2)). [ur(42,b,16,a(flip))]. given #123 (F,wt=17): 188 x * ((c1 * c2) * (c1 * (c2 * c1))) != x * (c2 * c1). [ur(4,b,150,a)]. given #124 (F,wt=17): 209 (c2 * (c2 * c1)) * (c1 * (c1 * (c1 * c2))) != c2 * c1. [ur(67,b,16,a)]. given #125 (F,wt=17): 211 (c1 * (c1 * c2)) * (c2 * (c2 * (c2 * c1))) != c1 * c2. [ur(67,b,30,a(flip))]. given #126 (F,wt=17): 257 (c2 * (c1 * c2)) * ((c2 * c1) * (c1 * c2)) != c1 * c2. [para(148(a,1),21(a,2))]. given #127 (T,wt=50): 552 (((((x * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * z != x * y | ((((y * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y) = z. [para(230(a,1),235(a,1,1,1,2)),rewrite([230(19),230(22),230(28),230(30),230(32)])]. given #128 (T,wt=50): 664 x * (((((y * (z * y)) * (z * y)) * (z * y)) * (z * y)) * (z * y)) != z * y | ((((z * (z * y)) * (z * y)) * (z * y)) * (z * y)) * (z * y) = x. [para(230(a,1),236(a,1,2,1,1,2)),rewrite([230(17),230(19),230(22),230(30),230(32)])]. given #129 (T,wt=51): 672 (((((x * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * ((((((y * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) = y * x. [para(237(a,1),230(a,1,1,1,2)),rewrite([237(21),237(29),237(31),237(33),237(36)])]. given #130 (T,wt=52): 521 (((x * (x * y)) * (x * y)) * (x * y)) * (x * y) != x * y | (((x * (x * y)) * (x * y)) * (x * y)) * (x * y) = ((y * (x * y)) * (x * y)) * (x * y). [para(230(a,1),153(a,1,2)),rewrite([230(19),230(27),230(33)])]. given #131 (A,wt=21): 59 ((c1 * (c1 * c2)) * x) * ((c2 * c1) * x) != (c1 * (c1 * c2)) * x. [ur(42,b,15,a(flip))]. given #132 (F,wt=17): 296 (c1 * (c2 * c1)) * ((c1 * c2) * (c2 * c1)) != c2 * c1. [ur(152,b,29,a)]. given #133 (F,wt=17): 635 c1 * (c2 * ((c2 * c1) * (c1 * (c1 * c2)))) != c2 * c1. [ur(10,b,75,a(flip))]. given #134 (F,wt=17): 751 c2 * (c1 * ((c2 * (c2 * c1)) * (c1 * c2))) != c1 * c2. [ur(10,b,79,a(flip))]. given #135 (F,wt=17): 880 c1 * (c2 * ((c1 * (c1 * c2)) * (c2 * c1))) != c2 * c1. [ur(10,b,83,a(flip))]. given #136 (T,wt=54): 526 x * (((y * (z * y)) * (z * y)) * (z * y)) != z * y | (((z * (z * y)) * (z * y)) * (z * y)) * (z * y) = x * (x * (((y * (z * y)) * (z * y)) * (z * y))). [para(230(a,1),151(a,1,2,2)),rewrite([230(18),230(26),230(32)])]. given #137 (T,wt=54): 675 (((((x * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * z != y * x | (((((y * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x) = z. [para(237(a,1),235(a,1,1,1,2)),rewrite([237(21),237(24),237(32),237(34),237(36)])]. given #138 (T,wt=54): 678 x * ((((((y * (y * z)) * (y * z)) * (y * z)) * (y * z)) * (y * z)) * (y * z)) != y * z | ((((z * (y * z)) * (y * z)) * (y * z)) * (y * z)) * (y * z) = x. [para(237(a,1),236(a,1,2,1,1,2)),rewrite([237(21),237(23),237(26),237(34),237(36)])]. given #139 (T,wt=55): 679 ((((((x * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * ((((((y * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) = x * y. [para(237(a,1),237(a,1,1,1,1,2)),rewrite([237(21),237(23),237(31),237(33),237(35),237(38)])]. given #140 (A,wt=21): 61 x * ((c1 * c2) * ((c2 * (c2 * c1)) * x)) != (c2 * (c2 * c1)) * x. [ur(10,b,29,a)]. given #141 (F,wt=17): 1119 c2 * (c1 * ((c1 * c2) * (c2 * (c2 * c1)))) != c1 * c2. [ur(10,b,122,a(flip))]. given #142 (F,wt=17): 1242 c2 * (c1 * ((c2 * c1) * (c2 * (c1 * c2)))) != c1 * c2. [ur(10,b,180,a(flip))]. given #143 (F,wt=17): 1374 c1 * (c2 * ((c1 * c2) * (c1 * (c2 * c1)))) != c2 * c1. [ur(10,b,188,a(flip))]. given #144 (F,wt=19): 62 x * ((c1 * (c1 * c2)) * ((c2 * c1) * x)) != (c2 * c1) * x. [ur(10,b,15,a)]. given #145 (T,wt=56): 525 (((x * (x * y)) * (x * y)) * (x * y)) * (x * y) != x * y | (((y * (x * y)) * (x * y)) * (x * y)) * (x * y) = (((x * (x * y)) * (x * y)) * (x * y)) * (x * y). [para(230(a,1),154(a,1,2)),rewrite([230(19),230(25),230(27),230(35)])]. given #146 (T,wt=56): 534 (((x * (y * x)) * (y * x)) * (y * x)) * (y * x) != y * x | (((x * (y * x)) * (y * x)) * (y * x)) * (y * x) = (((y * (y * x)) * (y * x)) * (y * x)) * (y * x). [para(230(a,1),157(a,1,1,2)),rewrite([230(17),230(19),230(25),230(27),230(35)])]. given #147 (T,wt=58): 799 ((((((x * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * z != x * y | (((((y * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y) = z. [para(237(a,1),304(a,1,1,1,1,2)),rewrite([237(21),237(23),237(26),237(34),237(36),237(38)])]. given #148 (T,wt=58): 822 x * ((((((y * (z * y)) * (z * y)) * (z * y)) * (z * y)) * (z * y)) * (z * y)) != z * y | (((((z * (z * y)) * (z * y)) * (z * y)) * (z * y)) * (z * y)) * (z * y) = x. [para(237(a,1),315(a,1,2,1,1,2)),rewrite([237(21),237(23),237(26),237(34),237(36),237(38)])]. given #149 (A,wt=19): 63 x * ((c2 * (c2 * c1)) * ((c1 * c2) * x)) != (c1 * c2) * x. [ur(10,b,29,a(flip))]. given #150 (F,wt=19): 72 (x * (c1 * c2)) * (x * (c2 * (c2 * c1))) != x * (c1 * c2). [ur(42,b,30,a(flip))]. given #151 (F,wt=19): 90 (x * (c1 * (c1 * c2))) * (x * (c2 * c1)) != x * (c2 * c1). [ur(44,b,16,a)]. given #152 (F,wt=19): 91 ((c1 * (c1 * c2)) * x) * ((c2 * c1) * x) != (c2 * c1) * x. [ur(44,b,15,a)]. given #153 (F,wt=19): 95 (x * (c2 * (c2 * c1))) * (x * (c1 * c2)) != x * (c1 * c2). [ur(44,b,30,a(flip))]. given #154 (T,wt=59): 832 ((((((x * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (((((((y * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) = y * x. [para(318(a,1),237(a,1,1,1,1,2)),rewrite([318(23),318(25),318(35),318(37),318(39),318(42)])]. given #155 (T,wt=60): 667 (((x * (y * x)) * (y * x)) * (y * x)) * (y * x) != y * x | ((((y * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x) = (((x * (y * x)) * (y * x)) * (y * x)) * (y * x). [para(237(a,1),154(a,1,2)),rewrite([237(21),237(29),237(31),237(39)])]. given #156 (T,wt=62): 535 x * ((((y * (y * z)) * (y * z)) * (y * z)) * (y * z)) != y * z | (((z * (y * z)) * (y * z)) * (y * z)) * (y * z) = x * (x * ((((y * (y * z)) * (y * z)) * (y * z)) * (y * z))). [para(230(a,1),158(a,1,2,2)),rewrite([230(20),230(26),230(28),230(36)])]. given #157 (T,wt=62): 835 ((((((x * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * z != y * x | ((((((y * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x) = z. [para(318(a,1),304(a,1,1,1,1,2)),rewrite([318(23),318(25),318(28),318(38),318(40),318(42)])]. given #158 (A,wt=21): 65 x * ((c2 * c1) * ((c1 * (c1 * c2)) * x)) != (c1 * (c1 * c2)) * x. [ur(10,b,15,a(flip))]. given #159 (F,wt=19): 96 ((c2 * (c2 * c1)) * x) * ((c1 * c2) * x) != (c1 * c2) * x. [ur(44,b,29,a(flip))]. given #160 (F,wt=19): 128 ((c1 * (c1 * c2)) * (c2 * c1)) * x != (c1 * (c1 * c2)) * x. [ur(5,b,47,a)]. given #161 (F,wt=19): 129 x * ((c1 * (c1 * c2)) * (c2 * c1)) != x * (c1 * (c1 * c2)). [ur(4,b,47,a)]. given #162 (F,wt=19): 136 ((c1 * c2) * (c2 * (c2 * c1))) * x != (c2 * (c2 * c1)) * x. [ur(5,b,49,a)]. given #163 (T,wt=62): 836 x * (((((((y * (y * z)) * (y * z)) * (y * z)) * (y * z)) * (y * z)) * (y * z)) * (y * z)) != y * z | (((((z * (y * z)) * (y * z)) * (y * z)) * (y * z)) * (y * z)) * (y * z) = x. [para(318(a,1),315(a,1,2,1,1,2)),rewrite([318(25),318(27),318(30),318(38),318(40),318(42)])]. given #164 (T,wt=63): 837 (((((((x * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (((((((y * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) = x * y. [para(318(a,1),318(a,1,1,1,1,2)),rewrite([318(25),318(27),318(35),318(37),318(39),318(41),318(44)])]. given #165 (T,wt=64): 673 ((((x * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y) != x * y | ((((x * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y) = (((y * (x * y)) * (x * y)) * (x * y)) * (x * y). [para(237(a,1),157(a,1,1,2)),rewrite([237(21),237(23),237(31),237(33),237(41)])]. given #166 (T,wt=66): 674 x * ((((y * (z * y)) * (z * y)) * (z * y)) * (z * y)) != z * y | ((((z * (z * y)) * (z * y)) * (z * y)) * (z * y)) * (z * y) = x * (x * ((((y * (z * y)) * (z * y)) * (z * y)) * (z * y))). [para(237(a,1),158(a,1,2,2)),rewrite([237(22),237(30),237(32),237(40)])]. given #167 (A,wt=21): 68 (x * (c2 * (c2 * c1))) * (x * (c1 * c2)) != x * (c2 * (c2 * c1)). [ur(42,b,30,a)]. given #168 (F,wt=19): 137 x * ((c1 * c2) * (c2 * (c2 * c1))) != x * (c2 * (c2 * c1)). [ur(4,b,49,a)]. given #169 (F,wt=19): 144 ((c2 * c1) * (c1 * (c1 * c2))) * x != (c1 * (c1 * c2)) * x. [ur(5,b,50,a)]. given #170 (F,wt=19): 145 x * ((c2 * c1) * (c1 * (c1 * c2))) != x * (c1 * (c1 * c2)). [ur(4,b,50,a)]. given #171 (F,wt=19): 194 ((c2 * (c2 * c1)) * (c1 * c2)) * x != (c2 * (c2 * c1)) * x. [ur(5,b,53,a)]. given #172 (T,wt=66): 925 (((((((x * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * z != x * y | ((((((y * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y) = z. [para(318(a,1),321(a,1,1,1,1,2)),rewrite([318(25),318(27),318(30),318(38),318(40),318(42),318(44)])]. given #173 (T,wt=66): 948 x * (((((((y * (z * y)) * (z * y)) * (z * y)) * (z * y)) * (z * y)) * (z * y)) * (z * y)) != z * y | ((((((z * (z * y)) * (z * y)) * (z * y)) * (z * y)) * (z * y)) * (z * y)) * (z * y) = x. [para(318(a,1),322(a,1,2,1,1,1,2)),rewrite([318(23),318(25),318(27),318(30),318(40),318(42),318(44)])]. given #174 (T,wt=67): 958 (((((((x * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * ((((((((y * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) = y * x. [para(323(a,1),318(a,1,1,1,1,2)),rewrite([323(27),323(29),323(39),323(41),323(43),323(45),323(48)])]. given #175 (T,wt=68): 684 ((((x * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y) != x * y | ((((y * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y) = ((((x * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y). [para(237(a,1),229(a,1,1,2)),rewrite([237(21),237(23),237(31),237(33),237(41),237(43)])]. given #176 (A,wt=23): 73 ((c2 * c1) * (c1 * (c1 * c2))) * (c2 * c1) != (c2 * c1) * (c1 * (c1 * c2)). [ur(42,b,46,a)]. given #177 (F,wt=19): 195 x * ((c2 * (c2 * c1)) * (c1 * c2)) != x * (c2 * (c2 * c1)). [ur(4,b,53,a)]. given #178 (F,wt=19): 203 ((c1 * c2) * (c1 * (c2 * c1))) * x != (c1 * (c1 * c2)) * x. [ur(5,b,64,a)]. given #179 (F,wt=19): 204 x * ((c1 * c2) * (c1 * (c2 * c1))) != x * (c1 * (c1 * c2)). [ur(4,b,64,a)]. given #180 (F,wt=19): 220 ((c1 * c2) * (c1 * (c2 * c1))) * (c2 * (c1 * c2)) != c1 * c2. [ur(115,b,64,a(flip))]. given #181 (T,wt=68): 689 ((((x * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x) != y * x | ((((x * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x) = ((((y * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x). [para(237(a,1),231(a,1,1,2)),rewrite([237(21),237(23),237(31),237(33),237(41),237(43)])]. given #182 (T,wt=70): 961 (((((((x * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * z != y * x | (((((((y * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x) = z. [para(323(a,1),321(a,1,1,1,1,2)),rewrite([323(27),323(29),323(32),323(42),323(44),323(46),323(48)])]. given #183 (T,wt=70): 962 x * ((((((((y * (y * z)) * (y * z)) * (y * z)) * (y * z)) * (y * z)) * (y * z)) * (y * z)) * (y * z)) != y * z | ((((((z * (y * z)) * (y * z)) * (y * z)) * (y * z)) * (y * z)) * (y * z)) * (y * z) = x. [para(323(a,1),322(a,1,2,1,1,1,2)),rewrite([323(27),323(29),323(31),323(34),323(44),323(46),323(48)])]. given #184 (T,wt=71): 963 ((((((((x * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * ((((((((y * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) = x * y. [para(323(a,1),323(a,1,1,1,1,1,2)),rewrite([323(27),323(29),323(31),323(41),323(43),323(45),323(47),323(50)])]. given #185 (A,wt=23): 85 (c2 * c1) * ((c1 * (c1 * c2)) * (c2 * c1)) != (c1 * (c1 * c2)) * (c2 * c1). [ur(44,b,51,a)]. given #186 (F,wt=19): 221 ((c2 * (c2 * c1)) * (c1 * c2)) * (c1 * (c2 * c1)) != c2 * c1. [ur(115,b,53,a(flip))]. given #187 (F,wt=19): 222 ((c2 * c1) * (c1 * (c1 * c2))) * (c2 * (c1 * c2)) != c1 * c2. [ur(115,b,50,a(flip))]. given #188 (F,wt=19): 223 ((c1 * c2) * (c2 * (c2 * c1))) * (c1 * (c2 * c1)) != c2 * c1. [ur(115,b,49,a(flip))]. given #189 (F,wt=19): 224 ((c1 * (c1 * c2)) * (c2 * c1)) * (c2 * (c1 * c2)) != c1 * c2. [ur(115,b,47,a(flip))]. given #190 (T,wt=72): 833 ((((x * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x) != y * x | (((((y * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x) = ((((x * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x). [para(318(a,1),229(a,1,1,2)),rewrite([318(23),318(25),318(35),318(37),318(45),318(47)])]. given #191 (T,wt=74): 829 x * (((((y * (y * z)) * (y * z)) * (y * z)) * (y * z)) * (y * z)) != y * z | ((((z * (y * z)) * (y * z)) * (y * z)) * (y * z)) * (y * z) = x * (x * (((((y * (y * z)) * (y * z)) * (y * z)) * (y * z)) * (y * z))). [para(318(a,1),158(a,1,2,2)),rewrite([318(26),318(34),318(36),318(46)])]. given #192 (T,wt=74): 1048 ((((((((x * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * z != x * y | (((((((y * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y) = z. [para(323(a,1),397(a,1,1,1,1,1,2)),rewrite([323(27),323(29),323(31),323(34),323(44),323(46),323(48),323(50)])]. given #193 (T,wt=74): 1072 x * ((((((((y * (z * y)) * (z * y)) * (z * y)) * (z * y)) * (z * y)) * (z * y)) * (z * y)) * (z * y)) != z * y | (((((((z * (z * y)) * (z * y)) * (z * y)) * (z * y)) * (z * y)) * (z * y)) * (z * y)) * (z * y) = x. [para(323(a,1),407(a,1,2,1,1,1,2)),rewrite([323(27),323(29),323(31),323(34),323(44),323(46),323(48),323(50)])]. given #194 (A,wt=23): 86 (c1 * c2) * ((c2 * (c2 * c1)) * (c1 * c2)) != (c2 * (c2 * c1)) * (c1 * c2). [ur(44,b,48,a)]. given #195 (F,wt=19): 249 x * ((c2 * c1) * ((c1 * (c1 * c2)) * x)) != (c2 * c1) * x. [ur(10,b,21,a)]. given #196 (F,wt=19): 264 ((c2 * c1) * (c2 * (c1 * c2))) * x != (c2 * (c2 * c1)) * x. [ur(5,b,69,a)]. given #197 (F,wt=19): 265 x * ((c2 * c1) * (c2 * (c1 * c2))) != x * (c2 * (c2 * c1)). [ur(4,b,69,a)]. given #198 (F,wt=19): 266 ((c2 * c1) * (c2 * (c1 * c2))) * (c1 * (c2 * c1)) != c2 * c1. [ur(115,b,69,a(flip))]. given #199 (T,wt=75): 1163 ((((((((x * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (((((((((y * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) = y * x. [para(522(a,1),323(a,1,1,1,1,1,2)),rewrite([522(29),522(31),522(33),522(45),522(47),522(49),522(51),522(54)])]. given #200 (T,wt=76): 834 (((((x * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y) != x * y | (((((x * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y) = ((((y * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y). [para(318(a,1),231(a,1,1,2)),rewrite([318(25),318(27),318(37),318(39),318(47),318(49)])]. given #201 (T,wt=78): 902 x * (((((y * (z * y)) * (z * y)) * (z * y)) * (z * y)) * (z * y)) != z * y | (((((z * (z * y)) * (z * y)) * (z * y)) * (z * y)) * (z * y)) * (z * y) = x * (x * (((((y * (z * y)) * (z * y)) * (z * y)) * (z * y)) * (z * y))). [para(318(a,1),232(a,1,2,1,2)),rewrite([318(23),318(26),318(36),318(38),318(46),318(48)])]. given #202 (T,wt=78): 1166 ((((((((x * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * z != y * x | ((((((((y * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x) = z. [para(522(a,1),397(a,1,1,1,1,1,2)),rewrite([522(29),522(31),522(33),522(36),522(48),522(50),522(52),522(54)])]. given #203 (A,wt=21): 88 (x * (c1 * c2)) * (x * (c2 * (c2 * c1))) != x * (c2 * (c2 * c1)). [ur(44,b,30,a)]. given #204 (F,wt=19): 268 (c2 * ((c1 * (c1 * c2)) * (c2 * c1))) * (c1 * c2) != c1 * c2. [ur(45,b,131,a)]. given #205 (F,wt=19): 270 (c1 * c2) * (c2 * ((c1 * (c1 * c2)) * (c2 * c1))) != c1 * c2. [ur(43,b,131,a)]. given #206 (F,wt=19): 274 (c2 * ((c1 * (c1 * c2)) * (c2 * c1))) * x != (c1 * c2) * x. [ur(5,b,131,a)]. given #207 (F,wt=19): 275 x * (c2 * ((c1 * (c1 * c2)) * (c2 * c1))) != x * (c1 * c2). [ur(4,b,131,a)]. given #208 (T,wt=78): 1167 x * (((((((((y * (y * z)) * (y * z)) * (y * z)) * (y * z)) * (y * z)) * (y * z)) * (y * z)) * (y * z)) * (y * z)) != y * z | (((((((z * (y * z)) * (y * z)) * (y * z)) * (y * z)) * (y * z)) * (y * z)) * (y * z)) * (y * z) = x. [para(522(a,1),407(a,1,2,1,1,1,2)),rewrite([522(31),522(33),522(35),522(38),522(48),522(50),522(52),522(54)])]. given #209 (T,wt=79): 1168 (((((((((x * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (((((((((y * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) = x * y. [para(522(a,1),522(a,1,1,1,1,1,2)),rewrite([522(31),522(33),522(35),522(45),522(47),522(49),522(51),522(53),522(56)])]. given #210 (T,wt=80): 838 (((((x * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y) != x * y | (((((y * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y) = (((((x * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y). [para(318(a,1),240(a,1,1,2)),rewrite([318(25),318(27),318(35),318(37),318(39),318(49),318(51)])]. given #211 (T,wt=80): 957 (((((x * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x) != y * x | (((((x * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x) = (((((y * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x). [para(323(a,1),231(a,1,1,2)),rewrite([323(27),323(29),323(39),323(41),323(51),323(53)])]. given #212 (A,wt=21): 89 ((c1 * c2) * x) * ((c2 * (c2 * c1)) * x) != (c2 * (c2 * c1)) * x. [ur(44,b,29,a)]. given #213 (F,wt=19): 276 (c1 * ((c1 * c2) * (c2 * (c2 * c1)))) * (c2 * c1) != c2 * c1. [ur(45,b,139,a)]. given #214 (F,wt=19): 278 (c2 * c1) * (c1 * ((c1 * c2) * (c2 * (c2 * c1)))) != c2 * c1. [ur(43,b,139,a)]. given #215 (F,wt=19): 282 (c1 * ((c1 * c2) * (c2 * (c2 * c1)))) * x != (c2 * c1) * x. [ur(5,b,139,a)]. given #216 (F,wt=19): 283 x * (c1 * ((c1 * c2) * (c2 * (c2 * c1)))) != x * (c2 * c1). [ur(4,b,139,a)]. given #217 (T,wt=82): 1192 (((((((((x * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * z != x * y | ((((((((y * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y) = z. [para(522(a,1),527(a,1,1,1,1,1,2)),rewrite([522(31),522(33),522(35),522(38),522(48),522(50),522(52),522(54),522(56)])]. given #218 (T,wt=82): 1298 x * (((((((((y * (z * y)) * (z * y)) * (z * y)) * (z * y)) * (z * y)) * (z * y)) * (z * y)) * (z * y)) * (z * y)) != z * y | ((((((((z * (z * y)) * (z * y)) * (z * y)) * (z * y)) * (z * y)) * (z * y)) * (z * y)) * (z * y)) * (z * y) = x. [para(522(a,1),528(a,1,2,1,1,1,1,2)),rewrite([522(29),522(31),522(33),522(35),522(38),522(50),522(52),522(54),522(56)])]. given #219 (T,wt=83): 1307 (((((((((x * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * ((((((((((y * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) = y * x. [para(533(a,1),522(a,1,1,1,1,1,2)),rewrite([533(33),533(35),533(37),533(49),533(51),533(53),533(55),533(57),533(60)])]. given #220 (T,wt=84): 959 (((((x * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x) != y * x | ((((((y * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x) = (((((x * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x). [para(323(a,1),240(a,1,1,2)),rewrite([323(27),323(29),323(39),323(41),323(43),323(53),323(55)])]. given #221 (A,wt=21): 97 (x * (c2 * c1)) * (x * (c1 * (c1 * c2))) != x * (c1 * (c1 * c2)). [ur(44,b,16,a(flip))]. given #222 (F,wt=19): 284 (c2 * ((c2 * c1) * (c1 * (c1 * c2)))) * (c1 * c2) != c1 * c2. [ur(45,b,147,a)]. given #223 (F,wt=19): 286 (c1 * c2) * (c2 * ((c2 * c1) * (c1 * (c1 * c2)))) != c1 * c2. [ur(43,b,147,a)]. given #224 (F,wt=19): 290 (c2 * ((c2 * c1) * (c1 * (c1 * c2)))) * x != (c1 * c2) * x. [ur(5,b,147,a)]. given #225 (F,wt=19): 291 x * (c2 * ((c2 * c1) * (c1 * (c1 * c2)))) != x * (c1 * c2). [ur(4,b,147,a)]. given #226 (T,wt=86): 960 x * ((((((y * (y * z)) * (y * z)) * (y * z)) * (y * z)) * (y * z)) * (y * z)) != y * z | (((((z * (y * z)) * (y * z)) * (y * z)) * (y * z)) * (y * z)) * (y * z) = x * (x * ((((((y * (y * z)) * (y * z)) * (y * z)) * (y * z)) * (y * z)) * (y * z))). [para(323(a,1),232(a,1,2,1,2)),rewrite([323(27),323(30),323(40),323(42),323(52),323(54)])]. given #227 (T,wt=86): 1308 (((((((((x * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * z != y * x | (((((((((y * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x) = z. [para(533(a,1),527(a,1,1,1,1,1,2)),rewrite([533(33),533(35),533(37),533(40),533(52),533(54),533(56),533(58),533(60)])]. given #228 (T,wt=86): 1309 x * ((((((((((y * (y * z)) * (y * z)) * (y * z)) * (y * z)) * (y * z)) * (y * z)) * (y * z)) * (y * z)) * (y * z)) * (y * z)) != y * z | ((((((((z * (y * z)) * (y * z)) * (y * z)) * (y * z)) * (y * z)) * (y * z)) * (y * z)) * (y * z)) * (y * z) = x. [para(533(a,1),528(a,1,2,1,1,1,1,2)),rewrite([533(33),533(35),533(37),533(39),533(42),533(54),533(56),533(58),533(60)])]. given #229 (T,wt=87): 1310 ((((((((((x * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * ((((((((((y * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) = x * y. [para(533(a,1),533(a,1,1,1,1,1,1,2)),rewrite([533(33),533(35),533(37),533(39),533(51),533(53),533(55),533(57),533(59),533(62)])]. given #230 (A,wt=21): 98 ((c2 * c1) * x) * ((c1 * (c1 * c2)) * x) != (c1 * (c1 * c2)) * x. [ur(44,b,15,a(flip))]. given #231 (F,wt=19): 336 c1 * ((c1 * (c1 * c2)) * (c2 * (c2 * (c2 * c1)))) != c2 * c1. [ur(10,b,22,a(flip))]. given #232 (F,wt=19): 337 (c1 * ((c2 * (c2 * c1)) * (c1 * c2))) * (c2 * c1) != c2 * c1. [ur(45,b,196,a)]. given #233 (F,wt=19): 339 (c2 * c1) * (c1 * ((c2 * (c2 * c1)) * (c1 * c2))) != c2 * c1. [ur(43,b,196,a)]. given #234 (F,wt=19): 343 (c1 * ((c2 * (c2 * c1)) * (c1 * c2))) * x != (c2 * c1) * x. [ur(5,b,196,a)]. given #235 (T,wt=88): 1023 ((((((x * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y) != x * y | ((((((x * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y) = (((((y * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y). [para(323(a,1),294(a,1,1,1,2)),rewrite([323(27),323(29),323(31),323(41),323(43),323(45),323(55),323(57)])]. given #236 (T,wt=90): 1024 x * ((((((y * (z * y)) * (z * y)) * (z * y)) * (z * y)) * (z * y)) * (z * y)) != z * y | ((((((z * (z * y)) * (z * y)) * (z * y)) * (z * y)) * (z * y)) * (z * y)) * (z * y) = x * (x * ((((((y * (z * y)) * (z * y)) * (z * y)) * (z * y)) * (z * y)) * (z * y))). [para(323(a,1),316(a,1,2,1,2)),rewrite([323(27),323(30),323(40),323(42),323(44),323(54),323(56)])]. given #237 (T,wt=90): 1420 ((((((((((x * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * z != x * y | (((((((((y * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y) = z. [para(533(a,1),552(a,1,1,1,1,1,1,2)),rewrite([533(33),533(35),533(37),533(39),533(42),533(54),533(56),533(58),533(60),533(62)])]. given #238 (T,wt=90): 1442 x * ((((((((((y * (z * y)) * (z * y)) * (z * y)) * (z * y)) * (z * y)) * (z * y)) * (z * y)) * (z * y)) * (z * y)) * (z * y)) != z * y | (((((((((z * (z * y)) * (z * y)) * (z * y)) * (z * y)) * (z * y)) * (z * y)) * (z * y)) * (z * y)) * (z * y)) * (z * y) = x. [para(533(a,1),664(a,1,2,1,1,1,1,2)),rewrite([533(33),533(35),533(37),533(39),533(42),533(54),533(56),533(58),533(60),533(62)])]. given #239 (A,wt=29): 101 (c2 * c1) * (x * (x * ((c1 * (c1 * c2)) * (c2 * c1)))) != x * ((c1 * (c1 * c2)) * (c2 * c1)). [ur(11,b,51,a)]. given #240 (F,wt=19): 344 x * (c1 * ((c2 * (c2 * c1)) * (c1 * c2))) != x * (c2 * c1). [ur(4,b,196,a)]. given #241 (F,wt=19): 345 (c2 * ((c1 * c2) * (c1 * (c2 * c1)))) * (c1 * c2) != c1 * c2. [ur(45,b,205,a)]. given #242 (F,wt=19): 347 (c1 * c2) * (c2 * ((c1 * c2) * (c1 * (c2 * c1)))) != c1 * c2. [ur(43,b,205,a)]. given #243 (F,wt=19): 351 (c2 * ((c1 * c2) * (c1 * (c2 * c1)))) * x != (c1 * c2) * x. [ur(5,b,205,a)]. given #244 (T,wt=91): 1451 ((((((((((x * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (((((((((((y * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) = y * x. [para(672(a,1),533(a,1,1,1,1,1,1,2)),rewrite([672(35),672(37),672(39),672(41),672(55),672(57),672(59),672(61),672(63),672(66)])]. given #245 (T,wt=92): 1162 ((((((x * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y) != x * y | ((((((y * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y) = ((((((x * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y). [para(522(a,1),240(a,1,1,2)),rewrite([522(31),522(33),522(43),522(45),522(47),522(59),522(61)])]. given #246 (T,wt=92): 1164 ((((((x * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x) != y * x | ((((((x * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x) = ((((((y * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x). [para(522(a,1),294(a,1,1,1,2)),rewrite([522(29),522(31),522(33),522(43),522(45),522(47),522(59),522(61)])]. given #247 (T,wt=94): 1452 ((((((((((x * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * z != y * x | ((((((((((y * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x) = z. [para(672(a,1),552(a,1,1,1,1,1,1,2)),rewrite([672(35),672(37),672(39),672(41),672(44),672(58),672(60),672(62),672(64),672(66)])]. given #248 (A,wt=29): 102 (c1 * c2) * (x * (x * ((c2 * (c2 * c1)) * (c1 * c2)))) != x * ((c2 * (c2 * c1)) * (c1 * c2)). [ur(11,b,48,a)]. given #249 (F,wt=19): 352 x * (c2 * ((c1 * c2) * (c1 * (c2 * c1)))) != x * (c1 * c2). [ur(4,b,205,a)]. given #250 (F,wt=19): 353 (c1 * ((c2 * c1) * (c2 * (c1 * c2)))) * (c2 * c1) != c2 * c1. [ur(45,b,267,a)]. given #251 (F,wt=19): 355 (c2 * c1) * (c1 * ((c2 * c1) * (c2 * (c1 * c2)))) != c2 * c1. [ur(43,b,267,a)]. given #252 (F,wt=19): 359 (c1 * ((c2 * c1) * (c2 * (c1 * c2)))) * x != (c2 * c1) * x. [ur(5,b,267,a)]. given #253 (T,wt=94): 1453 x * (((((((((((y * (y * z)) * (y * z)) * (y * z)) * (y * z)) * (y * z)) * (y * z)) * (y * z)) * (y * z)) * (y * z)) * (y * z)) * (y * z)) != y * z | (((((((((z * (y * z)) * (y * z)) * (y * z)) * (y * z)) * (y * z)) * (y * z)) * (y * z)) * (y * z)) * (y * z)) * (y * z) = x. [para(672(a,1),664(a,1,2,1,1,1,1,2)),rewrite([672(37),672(39),672(41),672(43),672(46),672(58),672(60),672(62),672(64),672(66)])]. given #254 (T,wt=95): 1454 (((((((((((x * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (((((((((((y * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) = x * y. [para(672(a,1),672(a,1,1,1,1,1,1,2)),rewrite([672(37),672(39),672(41),672(43),672(55),672(57),672(59),672(61),672(63),672(65),672(68)])]. given #255 (T,wt=96): 1169 ((((((x * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x) != y * x | (((((((y * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x) = ((((((x * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x). [para(522(a,1),319(a,1,1,1,2)),rewrite([522(29),522(31),522(33),522(45),522(47),522(49),522(59),522(61),522(63)])]. given #256 (T,wt=98): 1165 x * (((((((y * (y * z)) * (y * z)) * (y * z)) * (y * z)) * (y * z)) * (y * z)) * (y * z)) != y * z | ((((((z * (y * z)) * (y * z)) * (y * z)) * (y * z)) * (y * z)) * (y * z)) * (y * z) = x * (x * (((((((y * (y * z)) * (y * z)) * (y * z)) * (y * z)) * (y * z)) * (y * z)) * (y * z))). [para(522(a,1),316(a,1,2,1,2)),rewrite([522(31),522(34),522(44),522(46),522(48),522(60),522(62)])]. given #257 (A,wt=29): 103 (c2 * c1) * (x * (x * ((c2 * c1) * (c1 * (c1 * c2))))) != x * ((c2 * c1) * (c1 * (c1 * c2))). [ur(11,b,46,a)]. given #258 (F,wt=19): 360 x * (c1 * ((c2 * c1) * (c2 * (c1 * c2)))) != x * (c2 * c1). [ur(4,b,267,a)]. given #259 (F,wt=19): 435 (c2 * c1) * (x * (x * (c1 * (c1 * c2)))) != x * (c2 * c1). [ur(10,b,27,a)]. given #260 (F,wt=19): 494 x * ((c1 * c2) * ((c2 * (c2 * c1)) * x)) != (c1 * c2) * x. [ur(10,b,32,a(flip))]. given #261 (F,wt=19): 592 (c1 * c2) * (x * (x * (c2 * (c2 * c1)))) != x * (c1 * c2). [ur(10,b,71,a(flip))]. given #262 (T,wt=98): 1517 (((((((((((x * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * z != x * y | ((((((((((y * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y) = z. [para(672(a,1),675(a,1,1,1,1,1,1,2)),rewrite([672(37),672(39),672(41),672(43),672(46),672(58),672(60),672(62),672(64),672(66),672(68)])]. given #263 (T,wt=98): 1535 x * (((((((((((y * (z * y)) * (z * y)) * (z * y)) * (z * y)) * (z * y)) * (z * y)) * (z * y)) * (z * y)) * (z * y)) * (z * y)) * (z * y)) != z * y | ((((((((((z * (z * y)) * (z * y)) * (z * y)) * (z * y)) * (z * y)) * (z * y)) * (z * y)) * (z * y)) * (z * y)) * (z * y)) * (z * y) = x. [para(672(a,1),678(a,1,2,1,1,1,1,1,2)),rewrite([672(35),672(37),672(39),672(41),672(43),672(46),672(60),672(62),672(64),672(66),672(68)])]. given #264 (T,wt=99): 1544 (((((((((((x * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * ((((((((((((y * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) = y * x. [para(679(a,1),672(a,1,1,1,1,1,1,2)),rewrite([679(39),679(41),679(43),679(45),679(59),679(61),679(63),679(65),679(67),679(69),679(72)])]. given #265 (T,wt=100): 1170 (((((((x * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y) != x * y | (((((((x * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y) = ((((((y * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y). [para(522(a,1),320(a,1,1,1,2)),rewrite([522(31),522(33),522(35),522(47),522(49),522(51),522(61),522(63),522(65)])]. given #266 (A,wt=27): 104 (x * (c1 * c2)) * (y * (y * (x * (c2 * (c2 * c1))))) != y * (x * (c2 * (c2 * c1))). [ur(11,b,30,a)]. given #267 (F,wt=19): 625 (c2 * c1) * (c1 * (c1 * c2)) != (c1 * (c1 * c2)) * (c2 * c1). [ur(10,b,75,a),rewrite([41(12)]),flip(a)]. given #268 (F,wt=19): 706 c2 * ((c2 * (c2 * c1)) * (c1 * (c1 * (c1 * c2)))) != c1 * c2. [ur(10,b,34,a(flip))]. given #269 (F,wt=19): 1003 (c2 * (c2 * c1)) * (c1 * c2) != (c1 * c2) * (c2 * (c2 * c1)). [ur(10,b,118,a)]. given #270 (F,wt=19): 2553 c2 * (c1 * (c2 * ((c1 * (c1 * c2)) * (c2 * c1)))) != c1 * c2. [ur(10,b,275,a(flip))]. given #271 (A,wt=27): 105 ((c1 * c2) * x) * (y * (y * ((c2 * (c2 * c1)) * x))) != y * ((c2 * (c2 * c1)) * x). [ur(11,b,29,a)]. given #272 (F,wt=19): 2665 c1 * (c2 * (c1 * ((c1 * c2) * (c2 * (c2 * c1))))) != c2 * c1. [ur(10,b,283,a(flip))]. given #273 (F,wt=19): 2801 c2 * (c1 * (c2 * ((c2 * c1) * (c1 * (c1 * c2))))) != c1 * c2. [ur(10,b,291,a(flip))]. given #274 (F,wt=19): 2981 c1 * (c2 * (c1 * ((c2 * (c2 * c1)) * (c1 * c2)))) != c2 * c1. [ur(10,b,344,a(flip))]. given #275 (F,wt=19): 3110 c2 * (c1 * (c2 * ((c1 * c2) * (c1 * (c2 * c1))))) != c1 * c2. [ur(10,b,352,a(flip))]. given #276 (A,wt=25): 106 (x * (c1 * (c1 * c2))) * (y * (y * (x * (c2 * c1)))) != y * (x * (c2 * c1)). [ur(11,b,16,a)]. given #277 (F,wt=19): 3241 c1 * (c2 * (c1 * ((c2 * c1) * (c2 * (c1 * c2))))) != c2 * c1. [ur(10,b,360,a(flip))]. given #278 (F,wt=21): 124 ((c1 * (c1 * c2)) * (c2 * c1)) * (c1 * (c1 * c2)) != c1 * (c1 * c2). [ur(45,b,47,a)]. given #279 (F,wt=21): 125 (c1 * (c1 * c2)) * ((c1 * (c1 * c2)) * (c2 * c1)) != c1 * (c1 * c2). [ur(43,b,47,a)]. given #280 (F,wt=21): 132 ((c1 * c2) * (c2 * (c2 * c1))) * (c2 * (c2 * c1)) != c2 * (c2 * c1). [ur(45,b,49,a)]. given #281 (A,wt=25): 107 ((c1 * (c1 * c2)) * x) * (y * (y * ((c2 * c1) * x))) != y * ((c2 * c1) * x). [ur(11,b,15,a)]. given #282 (F,wt=21): 134 (c2 * (c2 * c1)) * ((c1 * c2) * (c2 * (c2 * c1))) != c2 * (c2 * c1). [ur(43,b,49,a)]. given #283 (F,wt=21): 140 ((c2 * c1) * (c1 * (c1 * c2))) * (c1 * (c1 * c2)) != c1 * (c1 * c2). [ur(45,b,50,a)]. given #284 (F,wt=21): 142 (c1 * (c1 * c2)) * ((c2 * c1) * (c1 * (c1 * c2))) != c1 * (c1 * c2). [ur(43,b,50,a)]. given #285 (F,wt=21): 166 (((c2 * c1) * x) * y) * z != (((c1 * (c1 * c2)) * x) * y) * z. [ur(5,b,20,a)]. given #286 (A,wt=23): 108 ((c1 * (c1 * c2)) * (c2 * c1)) * (x * (x * (c2 * c1))) != x * (c2 * c1). [ur(11,b,51,a(flip))]. given #287 (F,wt=21): 167 x * (((c2 * c1) * y) * z) != x * (((c1 * (c1 * c2)) * y) * z). [ur(4,b,20,a)]. given #288 (F,wt=21): 189 ((c2 * (c2 * c1)) * (c1 * c2)) * (c2 * (c2 * c1)) != c2 * (c2 * c1). [ur(45,b,53,a)]. given #289 (F,wt=21): 190 (c2 * (c2 * c1)) * ((c2 * (c2 * c1)) * (c1 * c2)) != c2 * (c2 * c1). [ur(43,b,53,a)]. given #290 (F,wt=21): 197 ((c1 * c2) * (c1 * (c2 * c1))) * (c1 * (c1 * c2)) != c1 * (c1 * c2). [ur(45,b,64,a)]. given #291 (A,wt=23): 109 ((c2 * (c2 * c1)) * (c1 * c2)) * (x * (x * (c1 * c2))) != x * (c1 * c2). [ur(11,b,48,a(flip))]. given #292 (F,wt=21): 199 (c1 * (c1 * c2)) * ((c1 * c2) * (c1 * (c2 * c1))) != c1 * (c1 * c2). [ur(43,b,64,a)]. given #293 (F,wt=21): 206 (c2 * (c2 * (c2 * c1))) * ((c2 * c1) * (c1 * c2)) != c2 * (c2 * c1). [ur(67,b,30,a)]. given #294 (F,wt=21): 214 (c1 * (c1 * (c1 * c2))) * ((c1 * c2) * (c2 * c1)) != c1 * (c1 * c2). [ur(67,b,16,a(flip))]. given #295 (F,wt=21): 217 (c2 * (c1 * c2)) * ((c2 * c1) * (c2 * (c2 * c1))) != c2 * (c2 * c1). [ur(115,b,30,a)]. given #296 (A,wt=23): 110 ((c2 * c1) * (c1 * (c1 * c2))) * (x * (x * (c2 * c1))) != x * (c2 * c1). [ur(11,b,46,a(flip))]. given #297 (F,wt=21): 227 (c1 * (c2 * c1)) * ((c1 * c2) * (c1 * (c1 * c2))) != c1 * (c1 * c2). [ur(115,b,16,a(flip))]. given #298 (F,wt=21): 250 (x * ((c2 * c1) * y)) * z != (x * ((c1 * (c1 * c2)) * y)) * z. [ur(5,b,21,a)]. given #299 (F,wt=21): 251 x * (y * ((c2 * c1) * z)) != x * (y * ((c1 * (c1 * c2)) * z)). [ur(4,b,21,a)]. given #300 (F,wt=21): 254 x * ((c1 * (c1 * c2)) * ((c2 * c1) * x)) != (c1 * (c1 * c2)) * x. [ur(10,b,21,a(flip))]. given #301 (A,wt=25): 111 (x * (c2 * (c2 * c1))) * (y * (y * (x * (c1 * c2)))) != y * (x * (c1 * c2)). [ur(11,b,30,a(flip))]. given #302 (F,wt=21): 258 ((c2 * c1) * (c2 * (c1 * c2))) * (c2 * (c2 * c1)) != c2 * (c2 * c1). [ur(45,b,69,a)]. given #303 (F,wt=21): 260 (c2 * (c2 * c1)) * ((c2 * c1) * (c2 * (c1 * c2))) != c2 * (c2 * c1). [ur(43,b,69,a)]. given #304 (F,wt=21): 299 (c1 * (c2 * c1)) * ((c2 * (c2 * c1)) * (c1 * (c1 * c2))) != c2 * c1. [ur(152,b,16,a)]. given #305 (F,wt=21): 300 (c2 * (c1 * c2)) * ((c1 * (c1 * c2)) * (c2 * (c2 * c1))) != c1 * c2. [ur(152,b,30,a(flip))]. given #306 (A,wt=25): 112 ((c2 * (c2 * c1)) * x) * (y * (y * ((c1 * c2) * x))) != y * ((c1 * c2) * x). [ur(11,b,29,a(flip))]. given #307 (F,wt=21): 309 (c1 * (c1 * (c1 * c2))) * ((c2 * (c2 * c1)) * (c2 * c1)) != c2 * c1. [ur(155,b,16,a)]. given #308 (F,wt=21): 310 (c2 * (c2 * (c2 * c1))) * ((c1 * (c1 * c2)) * (c1 * c2)) != c1 * c2. [ur(155,b,30,a(flip))]. given #309 (F,wt=21): 317 ((c2 * c1) * (c1 * c2)) * ((c2 * (c1 * c2)) * (c1 * c2)) != c1 * c2. [para(156(a,1),20(a,2))]. given #310 (F,wt=21): 373 ((x * (c2 * c1)) * y) * z != ((x * (c1 * (c1 * c2))) * y) * z. [ur(5,b,26,a)]. given #311 (A,wt=27): 113 (x * (c2 * c1)) * (y * (y * (x * (c1 * (c1 * c2))))) != y * (x * (c1 * (c1 * c2))). [ur(11,b,16,a(flip))]. given #312 (F,wt=21): 374 x * ((y * (c2 * c1)) * z) != x * ((y * (c1 * (c1 * c2))) * z). [ur(4,b,26,a)]. given #313 (F,wt=21): 399 ((c1 * c2) * (c2 * c1)) * ((c1 * (c2 * c1)) * (c2 * c1)) != c2 * c1. [ur(228,b,29,a)]. given #314 (F,wt=21): 436 (x * (y * (c2 * c1))) * z != (x * (y * (c1 * (c1 * c2)))) * z. [ur(5,b,27,a)]. given #315 (F,wt=21): 437 x * (y * (z * (c2 * c1))) != x * (y * (z * (c1 * (c1 * c2)))). [ur(4,b,27,a)]. given #316 (A,wt=27): 114 ((c2 * c1) * x) * (y * (y * ((c1 * (c1 * c2)) * x))) != y * ((c1 * (c1 * c2)) * x). [ur(11,b,15,a(flip))]. given #317 (F,wt=21): 444 (c1 * (c1 * c2)) * (x * (x * (c2 * c1))) != x * (c1 * (c1 * c2)). [ur(10,b,27,a(flip))]. given #318 (F,wt=21): 460 (((c2 * (c2 * c1)) * x) * y) * z != (((c1 * c2) * x) * y) * z. [ur(5,b,31,a)]. given #319 (F,wt=21): 461 x * (((c2 * (c2 * c1)) * y) * z) != x * (((c1 * c2) * y) * z). [ur(4,b,31,a)]. given #320 (F,wt=21): 485 x * ((c2 * (c2 * c1)) * ((c1 * c2) * x)) != (c2 * (c2 * c1)) * x. [ur(10,b,32,a)]. given #321 (A,wt=23): 119 ((c1 * c2) * (c2 * (c2 * c1))) * (c1 * c2) != (c1 * c2) * (c2 * (c2 * c1)). [ur(42,b,57,a)]. given #322 (F,wt=21): 486 (x * ((c2 * (c2 * c1)) * y)) * z != (x * ((c1 * c2) * y)) * z. [ur(5,b,32,a)]. given #323 (F,wt=21): 487 x * (y * ((c2 * (c2 * c1)) * z)) != x * (y * ((c1 * c2) * z)). [ur(4,b,32,a)]. given #324 (F,wt=21): 512 ((x * (c2 * (c2 * c1))) * y) * z != ((x * (c1 * c2)) * y) * z. [ur(5,b,70,a)]. given #325 (F,wt=21): 513 x * ((y * (c2 * (c2 * c1))) * z) != x * ((y * (c1 * c2)) * z). [ur(4,b,70,a)]. given #326 (A,wt=29): 120 (c1 * c2) * (x * (x * ((c1 * c2) * (c2 * (c2 * c1))))) != x * ((c1 * c2) * (c2 * (c2 * c1))). [ur(11,b,57,a)]. given #327 (F,wt=21): 582 (c2 * (c2 * c1)) * (x * (x * (c1 * c2))) != x * (c2 * (c2 * c1)). [ur(10,b,71,a)]. given #328 (F,wt=21): 583 (x * (y * (c2 * (c2 * c1)))) * z != (x * (y * (c1 * c2))) * z. [ur(5,b,71,a)]. given #329 (F,wt=21): 584 x * (y * (z * (c2 * (c2 * c1)))) != x * (y * (z * (c1 * c2))). [ur(4,b,71,a)]. given #330 (F,wt=21): 604 (((c2 * c1) * (c1 * (c1 * c2))) * x) * y != ((c2 * c1) * x) * y. [ur(5,b,74,a)]. given #331 (A,wt=23): 123 ((c1 * c2) * (c2 * (c2 * c1))) * (x * (x * (c1 * c2))) != x * (c1 * c2). [ur(11,b,57,a(flip))]. given #332 (F,wt=21): 605 x * (((c2 * c1) * (c1 * (c1 * c2))) * y) != x * ((c2 * c1) * y). [ur(4,b,74,a)]. given #333 (F,wt=21): 626 (x * ((c2 * c1) * (c1 * (c1 * c2)))) * y != (x * (c2 * c1)) * y. [ur(5,b,75,a)]. given #334 (F,wt=21): 627 x * (y * ((c2 * c1) * (c1 * (c1 * c2)))) != x * (y * (c2 * c1)). [ur(4,b,75,a)]. given #335 (F,wt=21): 633 (c2 * ((c2 * c1) * (c1 * (c1 * c2)))) * (c1 * (c2 * c1)) != c2 * c1. [ur(115,b,75,a(flip))]. given #336 (A,wt=25): 126 ((c1 * (c1 * c2)) * (c2 * c1)) * (c1 * (c1 * c2)) != (c1 * (c1 * c2)) * (c2 * c1). [ur(42,b,47,a)]. given #337 (F,wt=21): 634 (c2 * (c2 * c1)) * (c1 * ((c2 * c1) * (c1 * (c1 * c2)))) != c2 * c1. [ur(67,b,75,a(flip))]. given #338 (F,wt=21): 636 ((c2 * c1) * ((c2 * c1) * (c1 * (c1 * c2)))) * (c2 * c1) != c2 * c1. [ur(45,b,76,a)]. given #339 (F,wt=21): 637 (c2 * c1) * ((c2 * c1) * ((c2 * c1) * (c1 * (c1 * c2)))) != c2 * c1. [ur(43,b,76,a)]. given #340 (F,wt=21): 641 ((c2 * c1) * ((c2 * c1) * (c1 * (c1 * c2)))) * x != (c2 * c1) * x. [ur(5,b,76,a)]. given #341 (A,wt=31): 127 (c1 * (c1 * c2)) * (x * (x * ((c1 * (c1 * c2)) * (c2 * c1)))) != x * ((c1 * (c1 * c2)) * (c2 * c1)). [ur(11,b,47,a)]. given #342 (F,wt=21): 642 x * ((c2 * c1) * ((c2 * c1) * (c1 * (c1 * c2)))) != x * (c2 * c1). [ur(4,b,76,a)]. given #343 (F,wt=21): 719 (((c2 * (c2 * c1)) * (c1 * c2)) * x) * y != ((c1 * c2) * x) * y. [ur(5,b,78,a)]. given #344 (F,wt=21): 720 x * (((c2 * (c2 * c1)) * (c1 * c2)) * y) != x * ((c1 * c2) * y). [ur(4,b,78,a)]. given #345 (F,wt=21): 741 (x * ((c2 * (c2 * c1)) * (c1 * c2))) * y != (x * (c1 * c2)) * y. [ur(5,b,79,a)]. given #346 (A,wt=27): 130 ((c1 * (c1 * c2)) * (c2 * c1)) * (x * (x * (c1 * (c1 * c2)))) != x * (c1 * (c1 * c2)). [ur(11,b,47,a(flip))]. given #347 (F,wt=21): 742 x * (y * ((c2 * (c2 * c1)) * (c1 * c2))) != x * (y * (c1 * c2)). [ur(4,b,79,a)]. given #348 (F,wt=21): 749 (c1 * ((c2 * (c2 * c1)) * (c1 * c2))) * (c2 * (c1 * c2)) != c1 * c2. [ur(115,b,79,a(flip))]. given #349 (F,wt=21): 750 (c1 * (c1 * c2)) * (c2 * ((c2 * (c2 * c1)) * (c1 * c2))) != c1 * c2. [ur(67,b,79,a(flip))]. given #350 (F,wt=21): 752 ((c1 * c2) * ((c2 * (c2 * c1)) * (c1 * c2))) * (c1 * c2) != c1 * c2. [ur(45,b,80,a)]. given #351 (A,wt=25): 133 (c2 * (c2 * c1)) * ((c1 * c2) * (c2 * (c2 * c1))) != (c1 * c2) * (c2 * (c2 * c1)). [ur(44,b,49,a)]. given #352 (F,wt=21): 753 (c1 * c2) * ((c1 * c2) * ((c2 * (c2 * c1)) * (c1 * c2))) != c1 * c2. [ur(43,b,80,a)]. given #353 (F,wt=21): 757 ((c1 * c2) * ((c2 * (c2 * c1)) * (c1 * c2))) * x != (c1 * c2) * x. [ur(5,b,80,a)]. given #354 (F,wt=21): 758 x * ((c1 * c2) * ((c2 * (c2 * c1)) * (c1 * c2))) != x * (c1 * c2). [ur(4,b,80,a)]. given #355 (F,wt=21): 771 (((c1 * (c1 * c2)) * (c2 * c1)) * x) * y != ((c2 * c1) * x) * y. [ur(5,b,82,a)]. given #356 (A,wt=31): 135 (c2 * (c2 * c1)) * (x * (x * ((c1 * c2) * (c2 * (c2 * c1))))) != x * ((c1 * c2) * (c2 * (c2 * c1))). [ur(11,b,49,a)]. given #357 (F,wt=21): 772 x * (((c1 * (c1 * c2)) * (c2 * c1)) * y) != x * ((c2 * c1) * y). [ur(4,b,82,a)]. given #358 (F,wt=21): 868 (x * ((c1 * (c1 * c2)) * (c2 * c1))) * y != (x * (c2 * c1)) * y. [ur(5,b,83,a)]. given #359 (F,wt=21): 869 x * (y * ((c1 * (c1 * c2)) * (c2 * c1))) != x * (y * (c2 * c1)). [ur(4,b,83,a)]. given #360 (F,wt=21): 878 (c2 * ((c1 * (c1 * c2)) * (c2 * c1))) * (c1 * (c2 * c1)) != c2 * c1. [ur(115,b,83,a(flip))]. given #361 (A,wt=27): 138 ((c1 * c2) * (c2 * (c2 * c1))) * (x * (x * (c2 * (c2 * c1)))) != x * (c2 * (c2 * c1)). [ur(11,b,49,a(flip))]. given #362 (F,wt=21): 879 (c2 * (c2 * c1)) * (c1 * ((c1 * (c1 * c2)) * (c2 * c1))) != c2 * c1. [ur(67,b,83,a(flip))]. given #363 (F,wt=21): 881 ((c2 * c1) * ((c1 * (c1 * c2)) * (c2 * c1))) * (c2 * c1) != c2 * c1. [ur(45,b,84,a)]. given #364 (F,wt=21): 882 (c2 * c1) * ((c2 * c1) * ((c1 * (c1 * c2)) * (c2 * c1))) != c2 * c1. [ur(43,b,84,a)]. given #365 (F,wt=21): 886 ((c2 * c1) * ((c1 * (c1 * c2)) * (c2 * c1))) * x != (c2 * c1) * x. [ur(5,b,84,a)]. given #366 (A,wt=25): 141 (c1 * (c1 * c2)) * ((c2 * c1) * (c1 * (c1 * c2))) != (c2 * c1) * (c1 * (c1 * c2)). [ur(44,b,50,a)]. given #367 (F,wt=21): 887 x * ((c2 * c1) * ((c1 * (c1 * c2)) * (c2 * c1))) != x * (c2 * c1). [ur(4,b,84,a)]. given #368 (F,wt=21): 888 (((c1 * (c1 * c2)) * (c2 * c1)) * (c2 * c1)) * (c2 * c1) != c2 * c1. [ur(45,b,92,a)]. given #369 (F,wt=21): 889 (c2 * c1) * (((c1 * (c1 * c2)) * (c2 * c1)) * (c2 * c1)) != c2 * c1. [ur(43,b,92,a)]. given #370 (F,wt=21): 893 (((c1 * (c1 * c2)) * (c2 * c1)) * (c2 * c1)) * x != (c2 * c1) * x. [ur(5,b,92,a)]. given #371 (A,wt=31): 143 (c1 * (c1 * c2)) * (x * (x * ((c2 * c1) * (c1 * (c1 * c2))))) != x * ((c2 * c1) * (c1 * (c1 * c2))). [ur(11,b,50,a)]. given #372 (F,wt=21): 894 x * (((c1 * (c1 * c2)) * (c2 * c1)) * (c2 * c1)) != x * (c2 * c1). [ur(4,b,92,a)]. given #373 (F,wt=21): 895 (((c2 * (c2 * c1)) * (c1 * c2)) * (c1 * c2)) * (c1 * c2) != c1 * c2. [ur(45,b,93,a)]. given #374 (F,wt=21): 896 (c1 * c2) * (((c2 * (c2 * c1)) * (c1 * c2)) * (c1 * c2)) != c1 * c2. [ur(43,b,93,a)]. given #375 (F,wt=21): 900 (((c2 * (c2 * c1)) * (c1 * c2)) * (c1 * c2)) * x != (c1 * c2) * x. [ur(5,b,93,a)]. given #376 (A,wt=27): 146 ((c2 * c1) * (c1 * (c1 * c2))) * (x * (x * (c1 * (c1 * c2)))) != x * (c1 * (c1 * c2)). [ur(11,b,50,a(flip))]. given #377 (F,wt=21): 901 x * (((c2 * (c2 * c1)) * (c1 * c2)) * (c1 * c2)) != x * (c1 * c2). [ur(4,b,93,a)]. given #378 (F,wt=21): 982 (((c2 * c1) * (c1 * (c1 * c2))) * (c2 * c1)) * (c2 * c1) != c2 * c1. [ur(45,b,94,a)]. given #379 (F,wt=21): 983 (c2 * c1) * (((c2 * c1) * (c1 * (c1 * c2))) * (c2 * c1)) != c2 * c1. [ur(43,b,94,a)]. given #380 (F,wt=21): 987 (((c2 * c1) * (c1 * (c1 * c2))) * (c2 * c1)) * x != (c2 * c1) * x. [ur(5,b,94,a)]. given #381 (A,wt=27): 159 (((c2 * c1) * x) * y) * (((c1 * (c1 * c2)) * x) * y) != ((c1 * (c1 * c2)) * x) * y. [ur(45,b,20,a)]. given #382 (F,wt=21): 988 x * (((c2 * c1) * (c1 * (c1 * c2))) * (c2 * c1)) != x * (c2 * c1). [ur(4,b,94,a)]. given #383 (F,wt=21): 989 (((c1 * c2) * (c2 * (c2 * c1))) * (c1 * c2)) * (c1 * c2) != c1 * c2. [ur(45,b,116,a)]. given #384 (F,wt=21): 991 (c1 * c2) * (((c1 * c2) * (c2 * (c2 * c1))) * (c1 * c2)) != c1 * c2. [ur(43,b,116,a)]. given #385 (F,wt=21): 995 (((c1 * c2) * (c2 * (c2 * c1))) * (c1 * c2)) * x != (c1 * c2) * x. [ur(5,b,116,a)]. given #386 (A,wt=25): 160 (((c1 * (c1 * c2)) * x) * y) * (((c2 * c1) * x) * y) != ((c2 * c1) * x) * y. [ur(44,b,20,a)]. given #387 (F,wt=21): 996 x * (((c1 * c2) * (c2 * (c2 * c1))) * (c1 * c2)) != x * (c1 * c2). [ur(4,b,116,a)]. given #388 (F,wt=21): 998 ((c1 * c2) * ((c1 * c2) * (c2 * (c2 * c1)))) * (c1 * c2) != c1 * c2. [ur(45,b,118,a)]. given #389 (F,wt=21): 999 (c1 * c2) * ((c1 * c2) * ((c1 * c2) * (c2 * (c2 * c1)))) != c1 * c2. [ur(43,b,118,a)]. given #390 (F,wt=21): 1004 ((c1 * c2) * ((c1 * c2) * (c2 * (c2 * c1)))) * x != (c1 * c2) * x. [ur(5,b,118,a)]. given #391 (A,wt=27): 161 (((c1 * (c1 * c2)) * x) * y) * (((c2 * c1) * x) * y) != ((c1 * (c1 * c2)) * x) * y. [ur(43,b,20,a)]. given #392 (F,wt=21): 1005 x * ((c1 * c2) * ((c1 * c2) * (c2 * (c2 * c1)))) != x * (c1 * c2). [ur(4,b,118,a)]. given #393 (F,wt=21): 1017 (((c1 * c2) * (c2 * (c2 * c1))) * x) * y != ((c1 * c2) * x) * y. [ur(5,b,121,a)]. given #394 (F,wt=21): 1018 x * (((c1 * c2) * (c2 * (c2 * c1))) * y) != x * ((c1 * c2) * y). [ur(4,b,121,a)]. given #395 (F,wt=21): 1103 (x * ((c1 * c2) * (c2 * (c2 * c1)))) * y != (x * (c1 * c2)) * y. [ur(5,b,122,a)]. given #396 (A,wt=25): 162 (((c2 * c1) * x) * y) * (((c1 * (c1 * c2)) * x) * y) != ((c2 * c1) * x) * y. [ur(42,b,20,a)]. given #397 (F,wt=21): 1104 x * (y * ((c1 * c2) * (c2 * (c2 * c1)))) != x * (y * (c1 * c2)). [ur(4,b,122,a)]. given #398 (F,wt=21): 1117 (c1 * ((c1 * c2) * (c2 * (c2 * c1)))) * (c2 * (c1 * c2)) != c1 * c2. [ur(115,b,122,a(flip))]. given #399 (F,wt=21): 1118 (c1 * (c1 * c2)) * (c2 * ((c1 * c2) * (c2 * (c2 * c1)))) != c1 * c2. [ur(67,b,122,a(flip))]. given #400 (F,wt=21): 1132 (((c2 * c1) * (c2 * (c1 * c2))) * x) * y != ((c1 * c2) * x) * y. [ur(5,b,172,a)]. given #401 (A,wt=33): 163 (((c2 * c1) * x) * y) * (z * (z * (((c1 * (c1 * c2)) * x) * y))) != z * (((c1 * (c1 * c2)) * x) * y). [ur(12,b,20,a)]. given #402 (F,wt=21): 1133 x * (((c2 * c1) * (c2 * (c1 * c2))) * y) != x * ((c1 * c2) * y). [ur(4,b,172,a)]. given #403 (F,wt=21): 1140 (((c2 * c1) * (c2 * (c1 * c2))) * (c1 * c2)) * (c1 * c2) != c1 * c2. [ur(45,b,174,a)]. given #404 (F,wt=21): 1141 (c1 * c2) * (((c2 * c1) * (c2 * (c1 * c2))) * (c1 * c2)) != c1 * c2. [ur(43,b,174,a)]. given #405 (F,wt=21): 1145 (((c2 * c1) * (c2 * (c1 * c2))) * (c1 * c2)) * x != (c1 * c2) * x. [ur(5,b,174,a)]. given #406 (A,wt=31): 164 (((c1 * (c1 * c2)) * x) * y) * (z * (z * (((c2 * c1) * x) * y))) != z * (((c2 * c1) * x) * y). [ur(11,b,20,a)]. given #407 (F,wt=21): 1146 x * (((c2 * c1) * (c2 * (c1 * c2))) * (c1 * c2)) != x * (c1 * c2). [ur(4,b,174,a)]. given #408 (F,wt=21): 1147 ((c1 * c2) * ((c2 * c1) * (c2 * (c1 * c2)))) * (c1 * c2) != c1 * c2. [ur(45,b,176,a)]. given #409 (F,wt=21): 1148 (c1 * c2) * ((c1 * c2) * ((c2 * c1) * (c2 * (c1 * c2)))) != c1 * c2. [ur(43,b,176,a)]. given #410 (F,wt=21): 1152 ((c1 * c2) * ((c2 * c1) * (c2 * (c1 * c2)))) * x != (c1 * c2) * x. [ur(5,b,176,a)]. given #411 (A,wt=25): 165 x * (((c1 * (c1 * c2)) * y) * (((c2 * c1) * y) * x)) != ((c2 * c1) * y) * x. [ur(10,b,20,a)]. given #412 (F,wt=21): 1153 x * ((c1 * c2) * ((c2 * c1) * (c2 * (c1 * c2)))) != x * (c1 * c2). [ur(4,b,176,a)]. given #413 (F,wt=21): 1225 (x * ((c2 * c1) * (c2 * (c1 * c2)))) * y != (x * (c1 * c2)) * y. [ur(5,b,180,a)]. given #414 (F,wt=21): 1226 x * (y * ((c2 * c1) * (c2 * (c1 * c2)))) != x * (y * (c1 * c2)). [ur(4,b,180,a)]. given #415 (F,wt=21): 1240 (c1 * ((c2 * c1) * (c2 * (c1 * c2)))) * (c2 * (c1 * c2)) != c1 * c2. [ur(115,b,180,a(flip))]. given #416 (A,wt=27): 168 x * (((c2 * c1) * y) * (((c1 * (c1 * c2)) * y) * x)) != ((c1 * (c1 * c2)) * y) * x. [ur(10,b,20,a(flip))]. given #417 (F,wt=21): 1241 (c1 * (c1 * c2)) * (c2 * ((c2 * c1) * (c2 * (c1 * c2)))) != c1 * c2. [ur(67,b,180,a(flip))]. given #418 (F,wt=21): 1243 (((c1 * c2) * (c1 * (c2 * c1))) * (c2 * c1)) * (c2 * c1) != c2 * c1. [ur(45,b,181,a)]. given #419 (F,wt=21): 1245 (c2 * c1) * (((c1 * c2) * (c1 * (c2 * c1))) * (c2 * c1)) != c2 * c1. [ur(43,b,181,a)]. given #420 (F,wt=21): 1249 (((c1 * c2) * (c1 * (c2 * c1))) * (c2 * c1)) * x != (c2 * c1) * x. [ur(5,b,181,a)]. given #421 (A,wt=23): 169 ((c1 * (c1 * c2)) * (x * (x * (c2 * c1)))) * y != (x * (c2 * c1)) * y. [para(6(a,1),20(a,1,1)),flip(a)]. given #422 (F,wt=21): 1250 x * (((c1 * c2) * (c1 * (c2 * c1))) * (c2 * c1)) != x * (c2 * c1). [ur(4,b,181,a)]. given #423 (F,wt=21): 1251 ((c2 * c1) * ((c1 * c2) * (c1 * (c2 * c1)))) * (c2 * c1) != c2 * c1. [ur(45,b,183,a)]. given #424 (F,wt=21): 1253 (c2 * c1) * ((c2 * c1) * ((c1 * c2) * (c1 * (c2 * c1)))) != c2 * c1. [ur(43,b,183,a)]. given #425 (F,wt=21): 1257 ((c2 * c1) * ((c1 * c2) * (c1 * (c2 * c1)))) * x != (c2 * c1) * x. [ur(5,b,183,a)]. given #426 (A,wt=25): 170 ((c2 * c1) * (x * (x * (c1 * (c1 * c2))))) * y != (x * (c1 * (c1 * c2))) * y. [para(6(a,1),20(a,2,1))]. given #427 (F,wt=21): 1258 x * ((c2 * c1) * ((c1 * c2) * (c1 * (c2 * c1)))) != x * (c2 * c1). [ur(4,b,183,a)]. given #428 (F,wt=21): 1270 (((c1 * c2) * (c1 * (c2 * c1))) * x) * y != ((c2 * c1) * x) * y. [ur(5,b,187,a)]. given #429 (F,wt=21): 1271 x * (((c1 * c2) * (c1 * (c2 * c1))) * y) != x * ((c2 * c1) * y). [ur(4,b,187,a)]. given #430 (F,wt=21): 1356 (x * ((c1 * c2) * (c1 * (c2 * c1)))) * y != (x * (c2 * c1)) * y. [ur(5,b,188,a)]. given #431 (A,wt=25): 171 ((c1 * (c1 * c2)) * ((c2 * c1) * x)) * (x * ((c2 * c1) * x)) != (c2 * c1) * x. [para(13(a,1),20(a,1)),flip(a)]. given #432 (F,wt=21): 1357 x * (y * ((c1 * c2) * (c1 * (c2 * c1)))) != x * (y * (c2 * c1)). [ur(4,b,188,a)]. given #433 (F,wt=21): 1372 (c2 * ((c1 * c2) * (c1 * (c2 * c1)))) * (c1 * (c2 * c1)) != c2 * c1. [ur(115,b,188,a(flip))]. given #434 (F,wt=21): 1373 (c2 * (c2 * c1)) * (c1 * ((c1 * c2) * (c1 * (c2 * c1)))) != c2 * c1. [ur(67,b,188,a(flip))]. given #435 (F,wt=21): 1375 ((c2 * (c2 * c1)) * (c1 * (c1 * (c1 * c2)))) * (c2 * c1) != c2 * c1. [ur(45,b,209,a)]. given #436 (A,wt=29): 173 ((c2 * c1) * ((c1 * (c1 * c2)) * x)) * (x * ((c1 * (c1 * c2)) * x)) != (c1 * (c1 * c2)) * x. [para(13(a,1),20(a,2))]. given #437 (F,wt=21): 1377 (c2 * c1) * ((c2 * (c2 * c1)) * (c1 * (c1 * (c1 * c2)))) != c2 * c1. [ur(43,b,209,a)]. given #438 (F,wt=21): 1381 ((c2 * (c2 * c1)) * (c1 * (c1 * (c1 * c2)))) * x != (c2 * c1) * x. [ur(5,b,209,a)]. given #439 (F,wt=21): 1382 x * ((c2 * (c2 * c1)) * (c1 * (c1 * (c1 * c2)))) != x * (c2 * c1). [ur(4,b,209,a)]. given #440 (F,wt=21): 1383 ((c1 * (c1 * c2)) * (c2 * (c2 * (c2 * c1)))) * (c1 * c2) != c1 * c2. [ur(45,b,211,a)]. given #441 (A,wt=23): 175 (c1 * c2) * ((c2 * c1) * (c2 * (c1 * c2))) != (c2 * c1) * (c2 * (c1 * c2)). [ur(44,b,149,a)]. given #442 (F,wt=21): 1385 (c1 * c2) * ((c1 * (c1 * c2)) * (c2 * (c2 * (c2 * c1)))) != c1 * c2. [ur(43,b,211,a)]. given #443 (F,wt=21): 1389 ((c1 * (c1 * c2)) * (c2 * (c2 * (c2 * c1)))) * x != (c1 * c2) * x. [ur(5,b,211,a)]. given #444 (F,wt=21): 1390 x * ((c1 * (c1 * c2)) * (c2 * (c2 * (c2 * c1)))) != x * (c1 * c2). [ur(4,b,211,a)]. given #445 (F,wt=21): 1391 ((c2 * (c1 * c2)) * ((c2 * c1) * (c1 * c2))) * (c1 * c2) != c1 * c2. [ur(45,b,257,a)]. given #446 (A,wt=23): 177 ((c2 * c1) * (c2 * (c1 * c2))) * (c1 * c2) != (c2 * c1) * (c2 * (c1 * c2)). [ur(42,b,149,a)]. given #447 (F,wt=21): 1393 (c1 * c2) * ((c2 * (c1 * c2)) * ((c2 * c1) * (c1 * c2))) != c1 * c2. [ur(43,b,257,a)]. given #448 (F,wt=21): 1397 ((c2 * (c1 * c2)) * ((c2 * c1) * (c1 * c2))) * x != (c1 * c2) * x. [ur(5,b,257,a)]. given #449 (F,wt=21): 1398 x * ((c2 * (c1 * c2)) * ((c2 * c1) * (c1 * c2))) != x * (c1 * c2). [ur(4,b,257,a)]. given #450 (F,wt=21): 1468 ((c1 * (c2 * c1)) * ((c1 * c2) * (c2 * c1))) * (c2 * c1) != c2 * c1. [ur(45,b,296,a)]. given #451 (A,wt=23): 178 ((c2 * c1) * (c2 * (c1 * c2))) * (x * (x * (c1 * c2))) != x * (c1 * c2). [ur(12,b,149,a)]. given #452 (F,wt=21): 1470 (c2 * c1) * ((c1 * (c2 * c1)) * ((c1 * c2) * (c2 * c1))) != c2 * c1. [ur(43,b,296,a)]. given #453 (F,wt=21): 1474 ((c1 * (c2 * c1)) * ((c1 * c2) * (c2 * c1))) * x != (c2 * c1) * x. [ur(5,b,296,a)]. given #454 (F,wt=21): 1475 x * ((c1 * (c2 * c1)) * ((c1 * c2) * (c2 * c1))) != x * (c2 * c1). [ur(4,b,296,a)]. given #455 (F,wt=21): 1476 (c1 * (c2 * ((c2 * c1) * (c1 * (c1 * c2))))) * (c2 * c1) != c2 * c1. [ur(45,b,635,a)]. given #456 (A,wt=29): 179 (c1 * c2) * (x * (x * ((c2 * c1) * (c2 * (c1 * c2))))) != x * ((c2 * c1) * (c2 * (c1 * c2))). [ur(11,b,149,a)]. given #457 (F,wt=21): 1478 (c2 * c1) * (c1 * (c2 * ((c2 * c1) * (c1 * (c1 * c2))))) != c2 * c1. [ur(43,b,635,a)]. given #458 (F,wt=21): 1482 (c1 * (c2 * ((c2 * c1) * (c1 * (c1 * c2))))) * x != (c2 * c1) * x. [ur(5,b,635,a)]. given #459 (F,wt=21): 1483 x * (c1 * (c2 * ((c2 * c1) * (c1 * (c1 * c2))))) != x * (c2 * c1). [ur(4,b,635,a)]. given #460 (F,wt=21): 1484 (c2 * (c1 * ((c2 * (c2 * c1)) * (c1 * c2)))) * (c1 * c2) != c1 * c2. [ur(45,b,751,a)]. given #461 (A,wt=23): 182 (c2 * c1) * ((c1 * c2) * (c1 * (c2 * c1))) != (c1 * c2) * (c1 * (c2 * c1)). [ur(44,b,150,a)]. given #462 (F,wt=21): 1486 (c1 * c2) * (c2 * (c1 * ((c2 * (c2 * c1)) * (c1 * c2)))) != c1 * c2. [ur(43,b,751,a)]. given #463 (F,wt=21): 1490 (c2 * (c1 * ((c2 * (c2 * c1)) * (c1 * c2)))) * x != (c1 * c2) * x. [ur(5,b,751,a)]. given #464 (F,wt=21): 1491 x * (c2 * (c1 * ((c2 * (c2 * c1)) * (c1 * c2)))) != x * (c1 * c2). [ur(4,b,751,a)]. given #465 (F,wt=21): 1492 (c1 * (c2 * ((c1 * (c1 * c2)) * (c2 * c1)))) * (c2 * c1) != c2 * c1. [ur(45,b,880,a)]. given #466 (A,wt=23): 184 ((c1 * c2) * (c1 * (c2 * c1))) * (c2 * c1) != (c1 * c2) * (c1 * (c2 * c1)). [ur(42,b,150,a)]. given #467 (F,wt=21): 1494 (c2 * c1) * (c1 * (c2 * ((c1 * (c1 * c2)) * (c2 * c1)))) != c2 * c1. [ur(43,b,880,a)]. given #468 (F,wt=21): 1498 (c1 * (c2 * ((c1 * (c1 * c2)) * (c2 * c1)))) * x != (c2 * c1) * x. [ur(5,b,880,a)]. given #469 (F,wt=21): 1499 x * (c1 * (c2 * ((c1 * (c1 * c2)) * (c2 * c1)))) != x * (c2 * c1). [ur(4,b,880,a)]. given #470 (F,wt=21): 1559 (c2 * (c1 * ((c1 * c2) * (c2 * (c2 * c1))))) * (c1 * c2) != c1 * c2. [ur(45,b,1119,a)]. given #471 (A,wt=23): 185 ((c1 * c2) * (c1 * (c2 * c1))) * (x * (x * (c2 * c1))) != x * (c2 * c1). [ur(12,b,150,a)]. given #472 (F,wt=21): 1561 (c1 * c2) * (c2 * (c1 * ((c1 * c2) * (c2 * (c2 * c1))))) != c1 * c2. [ur(43,b,1119,a)]. given #473 (F,wt=21): 1565 (c2 * (c1 * ((c1 * c2) * (c2 * (c2 * c1))))) * x != (c1 * c2) * x. [ur(5,b,1119,a)]. given #474 (F,wt=21): 1566 x * (c2 * (c1 * ((c1 * c2) * (c2 * (c2 * c1))))) != x * (c1 * c2). [ur(4,b,1119,a)]. given #475 (F,wt=21): 1567 (c2 * (c1 * ((c2 * c1) * (c2 * (c1 * c2))))) * (c1 * c2) != c1 * c2. [ur(45,b,1242,a)]. given #476 (A,wt=29): 186 (c2 * c1) * (x * (x * ((c1 * c2) * (c1 * (c2 * c1))))) != x * ((c1 * c2) * (c1 * (c2 * c1))). [ur(11,b,150,a)]. given #477 (F,wt=21): 1569 (c1 * c2) * (c2 * (c1 * ((c2 * c1) * (c2 * (c1 * c2))))) != c1 * c2. [ur(43,b,1242,a)]. given #478 (F,wt=21): 1573 (c2 * (c1 * ((c2 * c1) * (c2 * (c1 * c2))))) * x != (c1 * c2) * x. [ur(5,b,1242,a)]. given #479 (F,wt=21): 1574 x * (c2 * (c1 * ((c2 * c1) * (c2 * (c1 * c2))))) != x * (c1 * c2). [ur(4,b,1242,a)]. given #480 (F,wt=21): 1575 (c1 * (c2 * ((c1 * c2) * (c1 * (c2 * c1))))) * (c2 * c1) != c2 * c1. [ur(45,b,1374,a)]. given #481 (A,wt=25): 191 ((c2 * (c2 * c1)) * (c1 * c2)) * (c2 * (c2 * c1)) != (c2 * (c2 * c1)) * (c1 * c2). [ur(42,b,53,a)]. given #482 (F,wt=21): 1577 (c2 * c1) * (c1 * (c2 * ((c1 * c2) * (c1 * (c2 * c1))))) != c2 * c1. [ur(43,b,1374,a)]. given #483 (F,wt=21): 1581 (c1 * (c2 * ((c1 * c2) * (c1 * (c2 * c1))))) * x != (c2 * c1) * x. [ur(5,b,1374,a)]. given #484 (F,wt=21): 1582 x * (c1 * (c2 * ((c1 * c2) * (c1 * (c2 * c1))))) != x * (c2 * c1). [ur(4,b,1374,a)]. given #485 (F,wt=21): 1854 (c1 * c2) * (c1 * ((c1 * (c1 * c2)) * (c2 * c1))) != c1 * (c1 * c2). [ur(10,b,129,a(flip))]. given #486 (A,wt=27): 192 ((c2 * (c2 * c1)) * (c1 * c2)) * (x * (x * (c2 * (c2 * c1)))) != x * (c2 * (c2 * c1)). [ur(12,b,53,a)]. given #487 (F,wt=21): 1973 (c2 * c1) * (c2 * ((c1 * c2) * (c2 * (c2 * c1)))) != c2 * (c2 * c1). [ur(10,b,137,a(flip))]. given #488 (F,wt=21): 2039 (c1 * c2) * (c1 * ((c2 * c1) * (c1 * (c1 * c2)))) != c1 * (c1 * c2). [ur(10,b,145,a(flip))]. given #489 (F,wt=21): 2168 (c2 * c1) * (c2 * ((c2 * (c2 * c1)) * (c1 * c2))) != c2 * (c2 * c1). [ur(10,b,195,a(flip))]. given #490 (F,wt=21): 2240 (c1 * c2) * (c1 * ((c1 * c2) * (c1 * (c2 * c1)))) != c1 * (c1 * c2). [ur(10,b,204,a(flip))]. given #491 (A,wt=31): 193 (c2 * (c2 * c1)) * (x * (x * ((c2 * (c2 * c1)) * (c1 * c2)))) != x * ((c2 * (c2 * c1)) * (c1 * c2)). [ur(11,b,53,a)]. given #492 (F,wt=21): 2424 (c2 * c1) * (c2 * ((c2 * c1) * (c2 * (c1 * c2)))) != c2 * (c2 * c1). [ur(10,b,265,a(flip))]. given #493 (F,wt=21): 3485 c2 * (((c1 * (c1 * c2)) * (c2 * c1)) * (c1 * (c1 * c2))) != c1 * c2. [ur(10,b,124,a(flip))]. given #494 (F,wt=21): 3494 c2 * ((c1 * (c1 * c2)) * ((c1 * (c1 * c2)) * (c2 * c1))) != c1 * c2. [ur(10,b,125,a(flip))]. given #495 (F,wt=21): 3502 c1 * (((c1 * c2) * (c2 * (c2 * c1))) * (c2 * (c2 * c1))) != c2 * c1. [ur(10,b,132,a(flip))]. given #496 (A,wt=25): 198 (c1 * (c1 * c2)) * ((c1 * c2) * (c1 * (c2 * c1))) != (c1 * c2) * (c1 * (c2 * c1)). [ur(44,b,64,a)]. given #497 (F,wt=21): 3537 c1 * ((c2 * (c2 * c1)) * ((c1 * c2) * (c2 * (c2 * c1)))) != c2 * c1. [ur(10,b,134,a(flip))]. given #498 (F,wt=21): 3545 c2 * (((c2 * c1) * (c1 * (c1 * c2))) * (c1 * (c1 * c2))) != c1 * c2. [ur(10,b,140,a(flip))]. given #499 (F,wt=21): 3554 c2 * ((c1 * (c1 * c2)) * ((c2 * c1) * (c1 * (c1 * c2)))) != c1 * c2. [ur(10,b,142,a(flip))]. NOTE: Back_subsumption disabled, ratio of kept to back_subsumed is 112 (0.00 of 9.98 sec). given #500 (F,wt=21): 3706 c1 * (((c2 * (c2 * c1)) * (c1 * c2)) * (c2 * (c2 * c1))) != c2 * c1. [ur(10,b,189,a(flip))]. given #501 (A,wt=25): 200 ((c1 * c2) * (c1 * (c2 * c1))) * (c1 * (c1 * c2)) != (c1 * c2) * (c1 * (c2 * c1)). [ur(42,b,64,a)]. given #502 (F,wt=21): 3715 c1 * ((c2 * (c2 * c1)) * ((c2 * (c2 * c1)) * (c1 * c2))) != c2 * c1. [ur(10,b,190,a(flip))]. given #503 (F,wt=21): 3724 c2 * (((c1 * c2) * (c1 * (c2 * c1))) * (c1 * (c1 * c2))) != c1 * c2. [ur(10,b,197,a(flip))]. given #504 (F,wt=21): 3772 c2 * ((c1 * (c1 * c2)) * ((c1 * c2) * (c1 * (c2 * c1)))) != c1 * c2. [ur(10,b,199,a(flip))]. given #505 (F,wt=21): 3782 c1 * ((c2 * (c2 * (c2 * c1))) * ((c2 * c1) * (c1 * c2))) != c2 * c1. [ur(10,b,206,a(flip))]. given #506 (A,wt=27): 201 ((c1 * c2) * (c1 * (c2 * c1))) * (x * (x * (c1 * (c1 * c2)))) != x * (c1 * (c1 * c2)). [ur(12,b,64,a)]. given #507 (F,wt=21): 3792 c2 * ((c1 * (c1 * (c1 * c2))) * ((c1 * c2) * (c2 * c1))) != c1 * c2. [ur(10,b,214,a(flip))]. given #508 (F,wt=21): 3802 c1 * ((c2 * (c1 * c2)) * ((c2 * c1) * (c2 * (c2 * c1)))) != c2 * c1. [ur(10,b,217,a(flip))]. given #509 (F,wt=21): 3849 c2 * ((c1 * (c2 * c1)) * ((c1 * c2) * (c1 * (c1 * c2)))) != c1 * c2. [ur(10,b,227,a(flip))]. given #510 (F,wt=21): 4011 c1 * (((c2 * c1) * (c2 * (c1 * c2))) * (c2 * (c2 * c1))) != c2 * c1. [ur(10,b,258,a(flip))]. given #511 (A,wt=31): 202 (c1 * (c1 * c2)) * (x * (x * ((c1 * c2) * (c1 * (c2 * c1))))) != x * ((c1 * c2) * (c1 * (c2 * c1))). [ur(11,b,64,a)]. ============================== STATISTICS ============================ Given=511. Generated=41079. Kept=9141. proofs=0. Usable=508. Sos=8530. Demods=24. Limbo=10, Disabled=97. Hints=0. Kept_by_rule=0, Deleted_by_rule=18267. Forward_subsumed=13671. Back_subsumed=80. Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. New_demodulators=28 (0 lex), Back_demodulated=13. Back_unit_deleted=0. Demod_attempts=9810464. Demod_rewrites=453525. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=219083. Nonunit_bsub_feature_tests=194. Megabytes=20.83. User_CPU=10.00, System_CPU=0.06, Wall_clock=10. ============================== end of statistics ===================== ============================== end of search ========================= SEARCH FAILED Exiting with failure. Process 4312 exit (max_seconds) Tue Nov 3 09:38:31 2009