============================== Prover9 =============================== Prover9 (32) version August-2006A, August 2006. Process 10672 was started by mccune on cleo.thornwood, Sat Aug 12 20:58:00 2006 The command was "/home/mccune/bin/prover9 -t 10 -f qg2.in". ============================== end of head =========================== ============================== INPUT ================================= % Reading from file qg2.in formulas(sos). (all x all y all z (x * y = x * z -> y = z)). (all x all y all 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 (all x all y all z (x * y = x * z -> y = z)). [assumption]. 2 (all x all y all z (y * x = z * x -> y = z)). [assumption]. 3 y * (y * x) = x * y. [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: Relation symbol precedence: lex([ = ]). Function symbol precedence: lex([ c1, c2, * ]). After inverse_order: (no changes). Unfolding symbols: (none). Auto_inference settings: % set(paramodulation). % (positive equality literals) % set(paramodulation) -> set(back_demod). % set(hyper_resolution). % (nonunit Horn with equality) % set(neg_ur_resolution). % (nonunit Horn with equality) % assign(para_lit_limit, 2). % (nonunit Horn with equality) Auto_process settings: (no changes). ============================== 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.00 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 (T,wt=7): 9 x * (x * x) = x. [hyper(4,a,6,a)]. given #6 (A,wt=14): 10 x * y != z * x | z * (z * x) = y. [para(6(a,1),4(a,1)),flip(a)]. given #7 (F,wt=9): 20 c2 * (c2 * c1) != c1 * c2. [ur(10,b,8,a(flip))]. given #8 (F,wt=13): 15 (c2 * c1) * x != (c1 * (c1 * c2)) * x. [ur(5,b,8,a)]. given #9 (T,wt=9): 14 (x * x) * (x * x) = x. [para(6(a,1),6(a,1,2)),rewrite(9(5))]. given #10 (T,wt=9): 37 (x * x) * x = x * x. [para(14(a,1),9(a,1,2))]. given #11 (A,wt=14): 11 x * (y * (y * z)) != y * z | z = x. [para(6(a,1),5(a,1)),flip(a)]. given #12 (F,wt=13): 16 x * (c2 * c1) != x * (c1 * (c1 * c2)). [ur(4,b,8,a)]. given #13 (F,wt=13): 25 (c2 * (c2 * c1)) * x != (c1 * c2) * x. [ur(5,b,20,a)]. given #14 (T,wt=5): 39 x * x = x. [hyper(5,a,37,a)]. given #15 (T,wt=8): 40 x * y != x | x = y. [para(37(a,1),4(a,1)),rewrite(39(1),39(1)),flip(a)]. given #16 (A,wt=14): 12 x * (y * (y * z)) != y * z | x = z. [para(6(a,1),5(a,2))]. given #17 (F,wt=13): 26 x * (c2 * (c2 * c1)) != x * (c1 * c2). [ur(4,b,20,a)]. given #18 (F,wt=13): 46 (c1 * (c1 * c2)) * (c2 * c1) != c2 * c1. [back_rewrite(33),rewrite(39(12))]. given #19 (T,wt=8): 41 x * y != x | y = x. [para(37(a,1),4(a,2)),rewrite(39(1),39(2))]. given #20 (T,wt=8): 42 x * y != y | y = x. [para(37(a,1),5(a,1)),rewrite(39(1),39(3)),flip(a)]. given #21 (A,wt=15): 13 (x * (x * y)) * (y * (x * y)) = x * y. [para(6(a,1),6(a,1,2,2)),rewrite(6(8))]. given #22 (F,wt=13): 64 (c2 * c1) * (c1 * (c1 * c2)) != c2 * c1. [para(39(a,1),16(a,1)),flip(a)]. given #23 (F,wt=13): 67 (c2 * (c2 * c1)) * (c1 * c2) != c1 * c2. [para(39(a,1),25(a,2))]. given #24 (T,wt=8): 43 x * y != y | x = y. [para(37(a,1),5(a,2)),rewrite(39(2),39(3))]. given #25 (T,wt=12): 44 x * y != y | x * (x * y) = y. [para(37(a,1),10(a,1)),rewrite(39(1),39(1),39(3)),flip(a)]. given #26 (A,wt=18): 21 x * y != z * y | z * (z * y) = x * (x * y). [para(6(a,1),10(a,1))]. given #27 (F,wt=13): 73 (c1 * c2) * (c2 * (c2 * c1)) != c1 * c2. [ur(40,b,20,a(flip))]. given #28 (F,wt=13): 102 (c2 * c1) * (c2 * (c1 * c2)) != c1 * c2. [para(13(a,1),15(a,2))]. given #29 (T,wt=16): 63 x * (x * y) != x * y | x * (x * y) = y. [para(39(a,1),11(a,1)),flip(b)]. given #30 (T,wt=18): 22 (x * (x * y)) * z != x * y | y * (x * y) = z. [para(6(a,1),10(a,2)),rewrite(6(8))]. given #31 (A,wt=19): 27 x * ((c1 * (c1 * c2)) * ((c2 * c1) * x)) != (c2 * c1) * x. [ur(10,b,15,a)]. given #32 (F,wt=13): 104 (c1 * c2) * (c1 * (c2 * c1)) != c2 * c1. [para(13(a,1),25(a,1)),flip(a)]. given #33 (F,wt=15): 45 (c2 * c1) * (c1 * (c1 * c2)) != c1 * (c1 * c2). [back_rewrite(34),rewrite(39(14))]. given #34 (T,wt=18): 51 x * (y * (z * y)) != z * y | z * (z * y) = x. [para(6(a,1),11(a,1,2,2)),rewrite(6(6))]. given #35 (T,wt=19): 99 (x * (y * x)) * ((y * (y * x)) * (y * x)) = y * x. [para(13(a,1),6(a,1,2,2)),rewrite(13(12))]. given #36 (A,wt=17): 28 ((c2 * c1) * x) * y != ((c1 * (c1 * c2)) * x) * y. [ur(5,b,15,a)]. given #37 (F,wt=15): 56 (c1 * c2) * (c1 * (c2 * c1)) != c1 * (c1 * c2). [ur(10,b,16,a(flip))]. given #38 (F,wt=15): 65 (c1 * (c1 * c2)) * (c2 * c1) != c1 * (c1 * c2). [para(39(a,1),16(a,2))]. given #39 (T,wt=20): 105 x * (x * y) != x * y | y * (x * y) = x * (x * y). [para(13(a,1),40(a,1)),flip(a),flip(b)]. given #40 (T,wt=20): 106 x * (y * x) != y * x | x * (y * x) = y * (y * x). [para(13(a,1),42(a,1)),flip(a)]. given #41 (A,wt=17): 29 x * ((c2 * c1) * y) != x * ((c1 * (c1 * c2)) * y). [ur(4,b,15,a)]. given #42 (F,wt=15): 66 (c1 * c2) * (c2 * (c2 * c1)) != c2 * (c2 * c1). [para(39(a,1),25(a,1)),flip(a)]. given #43 (F,wt=15): 69 (c2 * (c2 * c1)) * (c1 * c2) != c2 * (c2 * c1). [ur(40,b,20,a)]. given #44 (T,wt=22): 101 (x * (y * x)) * z != y * x | (y * (y * x)) * (y * x) = z. [para(13(a,1),10(a,2)),rewrite(13(12))]. given #45 (T,wt=22): 103 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 #46 (A,wt=21): 30 x * ((c2 * c1) * ((c1 * (c1 * c2)) * x)) != (c1 * (c1 * c2)) * x. [ur(10,b,15,a(flip))]. given #47 (F,wt=15): 79 (c2 * c1) * (c2 * (c1 * c2)) != c2 * (c2 * c1). [ur(10,b,26,a)]. given #48 (F,wt=15): 178 c2 * ((c2 * c1) * (c1 * (c1 * c2))) != c1 * c2. [ur(10,b,45,a(flip))]. given #49 (T,wt=23): 107 ((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 (T,wt=24): 124 x * (y * x) != y * x | (y * (y * x)) * (y * x) = x * (y * x). [para(13(a,1),44(a,1)),rewrite(13(11)),flip(a)]. given #51 (A,wt=19): 31 (c1 * (c1 * c2)) * (x * (x * (c2 * c1))) != x * (c2 * c1). [para(6(a,1),15(a,1)),flip(a)]. given #52 (F,wt=15): 223 c2 * ((c1 * c2) * (c1 * (c2 * c1))) != c1 * c2. [ur(10,b,56,a(flip))]. given #53 (F,wt=15): 232 c2 * ((c1 * (c1 * c2)) * (c2 * c1)) != c1 * c2. [ur(10,b,65,a(flip))]. given #54 (T,wt=26): 100 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 #55 (T,wt=26): 151 ((x * (x * y)) * (x * y)) * z != x * y | (y * (x * y)) * (x * y) = z. [para(13(a,1),22(a,1,1,2)),rewrite(13(10),13(14))]. given #56 (A,wt=21): 32 (c2 * c1) * (x * (x * (c1 * (c1 * c2)))) != x * (c1 * (c1 * c2)). [para(6(a,1),15(a,2))]. given #57 (F,wt=15): 264 c1 * ((c1 * c2) * (c2 * (c2 * c1))) != c2 * c1. [ur(10,b,66,a(flip))]. given #58 (F,wt=15): 273 c1 * ((c2 * (c2 * c1)) * (c1 * c2)) != c2 * c1. [ur(10,b,69,a(flip))]. given #59 (T,wt=26): 188 x * ((y * (z * y)) * (z * y)) != z * y | (z * (z * y)) * (z * y) = x. [para(13(a,1),51(a,1,2,2)),rewrite(13(10),13(14))]. given #60 (T,wt=27): 189 ((x * (y * x)) * (y * x)) * (((y * (y * x)) * (y * x)) * (y * x)) = y * x. [para(99(a,1),13(a,1,1,2)),rewrite(99(15),99(18))]. given #61 (A,wt=21): 47 (c1 * c2) * (x * (x * (c2 * (c2 * c1)))) != x * (c2 * (c2 * c1)). [ur(11,b,20,a)]. given #62 (F,wt=15): 320 c1 * ((c2 * c1) * (c2 * (c1 * c2))) != c2 * c1. [ur(10,b,79,a(flip))]. given #63 (F,wt=17): 53 (x * (c2 * c1)) * y != (x * (c1 * (c1 * c2))) * y. [ur(5,b,16,a)]. given #64 (T,wt=28): 142 (x * (x * y)) * (x * y) != x * y | (x * (x * y)) * (x * y) = y * (x * y). [para(13(a,1),63(a,1,2)),rewrite(13(9),13(13))]. given #65 (T,wt=30): 125 x * (y * (z * y)) != z * y | (z * (z * y)) * (z * y) = x * (x * (y * (z * y))). [para(13(a,1),21(a,1)),rewrite(13(16)),flip(a),flip(b)]. given #66 (A,wt=25): 48 ((c1 * (c1 * c2)) * x) * (y * (y * ((c2 * c1) * x))) != y * ((c2 * c1) * x). [ur(11,b,15,a)]. given #67 (F,wt=17): 54 x * (y * (c2 * c1)) != x * (y * (c1 * (c1 * c2))). [ur(4,b,16,a)]. given #68 (F,wt=17): 59 ((c2 * (c2 * c1)) * x) * y != ((c1 * c2) * x) * y. [ur(5,b,25,a)]. given #69 (T,wt=30): 193 ((x * (y * x)) * (y * x)) * z != y * x | ((y * (y * x)) * (y * x)) * (y * x) = z. [para(99(a,1),22(a,1,1,2)),rewrite(99(12),99(18))]. given #70 (T,wt=30): 194 x * (((y * (y * z)) * (y * z)) * (y * z)) != y * z | (z * (y * z)) * (y * z) = x. [para(99(a,1),51(a,1,2,2)),rewrite(99(14),99(18))]. given #71 (A,wt=19): 49 (c2 * (c2 * c1)) * (x * (x * (c1 * c2))) != x * (c1 * c2). [ur(11,b,20,a(flip))]. given #72 (F,wt=17): 60 x * ((c2 * (c2 * c1)) * y) != x * ((c1 * c2) * y). [ur(4,b,25,a)]. given #73 (F,wt=17): 80 (x * (c2 * (c2 * c1))) * y != (x * (c1 * c2)) * y. [ur(5,b,26,a)]. given #74 (T,wt=31): 195 (((x * (x * y)) * (x * y)) * (x * y)) * (((y * (x * y)) * (x * y)) * (x * y)) = x * y. [para(99(a,1),99(a,1,1,2)),rewrite(99(15),99(17),99(20))]. given #75 (T,wt=32): 190 (x * (x * y)) * (x * y) != x * y | (y * (x * y)) * (x * y) = (x * (x * y)) * (x * y). [para(99(a,1),44(a,1)),rewrite(99(15)),flip(a)]. given #76 (A,wt=27): 50 ((c2 * c1) * x) * (y * (y * ((c1 * (c1 * c2)) * x))) != y * ((c1 * (c1 * c2)) * x). [ur(11,b,15,a(flip))]. given #77 (F,wt=17): 81 x * (y * (c2 * (c2 * c1))) != x * (y * (c1 * c2)). [ur(4,b,26,a)]. given #78 (F,wt=17): 86 ((c1 * (c1 * c2)) * (c2 * c1)) * x != (c2 * c1) * x. [ur(5,b,46,a)]. given #79 (T,wt=32): 192 (x * (y * x)) * (y * x) != y * x | (x * (y * x)) * (y * x) = (y * (y * x)) * (y * x). [para(99(a,1),63(a,1,2)),rewrite(99(11),99(15))]. given #80 (T,wt=34): 283 (((x * (x * y)) * (x * y)) * (x * y)) * z != x * y | ((y * (x * y)) * (x * y)) * (x * y) = z. [para(99(a,1),101(a,1,1,2)),rewrite(99(14),99(18),99(20))]. given #81 (A,wt=25): 52 (x * (c1 * (c1 * c2))) * (y * (y * (x * (c2 * c1)))) != y * (x * (c2 * c1)). [ur(11,b,16,a)]. given #82 (F,wt=17): 87 x * ((c1 * (c1 * c2)) * (c2 * c1)) != x * (c2 * c1). [ur(4,b,46,a)]. given #83 (F,wt=17): 88 (c2 * c1) * ((c1 * (c1 * c2)) * (c2 * c1)) != c2 * c1. [ur(40,b,46,a(flip))]. given #84 (T,wt=34): 295 x * (((y * (z * y)) * (z * y)) * (z * y)) != z * y | ((z * (z * y)) * (z * y)) * (z * y) = x. [para(99(a,1),103(a,1,2,1,2)),rewrite(99(11),99(14),99(20))]. given #85 (T,wt=35): 330 (((x * (y * x)) * (y * x)) * (y * x)) * ((((y * (y * x)) * (y * x)) * (y * x)) * (y * x)) = y * x. [para(107(a,1),99(a,1,1,2)),rewrite(107(19),107(21),107(24))]. given #86 (A,wt=27): 55 (x * (c2 * c1)) * (y * (y * (x * (c1 * (c1 * c2))))) != y * (x * (c1 * (c1 * c2))). [ur(11,b,16,a(flip))]. given #87 (F,wt=17): 94 ((c1 * (c1 * c2)) * (c2 * c1)) * (c2 * c1) != c2 * c1. [ur(42,b,46,a(flip))]. given #88 (F,wt=17): 109 (c2 * c1) * ((c2 * c1) * (c1 * (c1 * c2))) != c2 * c1. [ur(41,b,64,a)]. given #89 (T,wt=36): 235 (x * (y * x)) * (y * x) != y * x | ((y * (y * x)) * (y * x)) * (y * x) = (x * (y * x)) * (y * x). [para(99(a,1),105(a,1,2)),rewrite(99(11),99(17),99(21))]. given #90 (T,wt=38): 191 x * ((y * (y * z)) * (y * z)) != y * z | (z * (y * z)) * (y * z) = x * (x * ((y * (y * z)) * (y * z))). [para(99(a,1),21(a,1)),rewrite(99(22)),flip(a),flip(b)]. given #91 (A,wt=27): 57 ((c1 * c2) * x) * (y * (y * ((c2 * (c2 * c1)) * x))) != y * ((c2 * (c2 * c1)) * x). [ur(11,b,25,a)]. given #92 (F,wt=17): 113 ((c2 * c1) * (c1 * (c1 * c2))) * x != (c2 * c1) * x. [ur(5,b,64,a)]. given #93 (F,wt=17): 114 x * ((c2 * c1) * (c1 * (c1 * c2))) != x * (c2 * c1). [ur(4,b,64,a)]. given #94 (T,wt=38): 334 (((x * (y * x)) * (y * x)) * (y * x)) * z != y * x | (((y * (y * x)) * (y * x)) * (y * x)) * (y * x) = z. [para(107(a,1),101(a,1,1,2)),rewrite(107(16),107(22),107(24))]. given #95 (T,wt=38): 335 x * ((((y * (y * z)) * (y * z)) * (y * z)) * (y * z)) != y * z | ((z * (y * z)) * (y * z)) * (y * z) = x. [para(107(a,1),103(a,1,2,1,2)),rewrite(107(15),107(18),107(24))]. given #96 (A,wt=21): 58 x * ((c1 * c2) * ((c2 * (c2 * c1)) * x)) != (c2 * (c2 * c1)) * x. [ur(10,b,25,a)]. given #97 (F,wt=17): 115 ((c2 * c1) * (c1 * (c1 * c2))) * (c2 * c1) != c2 * c1. [ur(42,b,64,a(flip))]. given #98 (F,wt=17): 117 (c1 * c2) * ((c2 * (c2 * c1)) * (c1 * c2)) != c1 * c2. [ur(41,b,67,a)]. given #99 (T,wt=39): 336 ((((x * (x * y)) * (x * y)) * (x * y)) * (x * y)) * ((((y * (x * y)) * (x * y)) * (x * y)) * (x * y)) = x * y. [para(107(a,1),107(a,1,1,1,2)),rewrite(107(15),107(21),107(23),107(26))]. given #100 (T,wt=40): 239 ((x * (x * y)) * (x * y)) * (x * y) != x * y | ((x * (x * y)) * (x * y)) * (x * y) = (y * (x * y)) * (x * y). [para(99(a,1),106(a,1,2)),rewrite(99(13),99(19),99(23))]. given #101 (A,wt=25): 61 ((c2 * (c2 * c1)) * x) * (y * (y * ((c1 * c2) * x))) != y * ((c1 * c2) * x). [ur(11,b,25,a(flip))]. given #102 (F,wt=17): 121 ((c2 * (c2 * c1)) * (c1 * c2)) * x != (c1 * c2) * x. [ur(5,b,67,a)]. given #103 (F,wt=17): 122 x * ((c2 * (c2 * c1)) * (c1 * c2)) != x * (c1 * c2). [ur(4,b,67,a)]. given #104 (T,wt=42): 329 x * ((y * (z * y)) * (z * y)) != z * y | ((z * (z * y)) * (z * y)) * (z * y) = x * (x * ((y * (z * y)) * (z * y))). [para(107(a,1),21(a,1)),rewrite(107(26)),flip(a),flip(b)]. given #105 (T,wt=42): 377 ((((x * (x * y)) * (x * y)) * (x * y)) * (x * y)) * z != x * y | (((y * (x * y)) * (x * y)) * (x * y)) * (x * y) = z. [para(107(a,1),151(a,1,1,1,2)),rewrite(107(15),107(18),107(24),107(26))]. given #106 (A,wt=19): 62 x * ((c2 * (c2 * c1)) * ((c1 * c2) * x)) != (c1 * c2) * x. [ur(10,b,25,a(flip))]. given #107 (F,wt=17): 123 ((c2 * (c2 * c1)) * (c1 * c2)) * (c1 * c2) != c1 * c2. [ur(42,b,67,a(flip))]. given #108 (F,wt=17): 126 ((c1 * c2) * (c2 * (c2 * c1))) * (c1 * c2) != c1 * c2. [ur(43,b,73,a)]. given #109 (T,wt=42): 420 x * ((((y * (z * y)) * (z * y)) * (z * y)) * (z * y)) != z * y | (((z * (z * y)) * (z * y)) * (z * y)) * (z * y) = x. [para(107(a,1),188(a,1,2,1,2)),rewrite(107(15),107(18),107(24),107(26))]. given #110 (T,wt=43): 422 ((((x * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (((((y * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) = y * x. [para(189(a,1),107(a,1,1,1,2)),rewrite(189(17),189(25),189(27),189(30))]. given #111 (A,wt=21): 68 ((c2 * (c2 * c1)) * x) * ((c1 * c2) * x) != (c2 * (c2 * c1)) * x. [ur(40,b,25,a)]. given #112 (F,wt=17): 128 (c1 * c2) * ((c1 * c2) * (c2 * (c2 * c1))) != c1 * c2. [ur(41,b,73,a)]. given #113 (F,wt=17): 132 ((c1 * c2) * (c2 * (c2 * c1))) * x != (c1 * c2) * x. [ur(5,b,73,a)]. given #114 (T,wt=44): 332 ((x * (x * y)) * (x * y)) * (x * y) != x * y | ((y * (x * y)) * (x * y)) * (x * y) = ((x * (x * y)) * (x * y)) * (x * y). [para(107(a,1),105(a,1,2)),rewrite(107(15),107(21),107(27))]. given #115 (T,wt=44): 333 ((x * (y * x)) * (y * x)) * (y * x) != y * x | ((x * (y * x)) * (y * x)) * (y * x) = ((y * (y * x)) * (y * x)) * (y * x). [para(107(a,1),106(a,1,2)),rewrite(107(15),107(21),107(27))]. given #116 (A,wt=19): 70 (x * (c2 * c1)) * (x * (c1 * (c1 * c2))) != x * (c2 * c1). [ur(40,b,16,a)]. given #117 (F,wt=17): 133 x * ((c1 * c2) * (c2 * (c2 * c1))) != x * (c1 * c2). [ur(4,b,73,a)]. given #118 (F,wt=17): 134 ((c2 * c1) * (c2 * (c1 * c2))) * (c1 * c2) != c1 * c2. [ur(43,b,102,a)]. given #119 (T,wt=46): 425 ((((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(189(a,1),151(a,1,1,1,2)),rewrite(189(17),189(20),189(28),189(30))]. given #120 (T,wt=46): 426 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(189(a,1),188(a,1,2,1,2)),rewrite(189(19),189(22),189(28),189(30))]. given #121 (A,wt=19): 71 ((c2 * c1) * x) * ((c1 * (c1 * c2)) * x) != (c2 * c1) * x. [ur(40,b,15,a)]. given #122 (F,wt=17): 136 (c1 * c2) * ((c2 * c1) * (c2 * (c1 * c2))) != c1 * c2. [ur(41,b,102,a)]. given #123 (F,wt=17): 140 ((c2 * c1) * (c2 * (c1 * c2))) * x != (c1 * c2) * x. [ur(5,b,102,a)]. given #124 (T,wt=47): 427 (((((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(189(a,1),189(a,1,1,1,2)),rewrite(189(19),189(25),189(27),189(29),189(32))]. given #125 (T,wt=48): 337 ((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(107(a,1),124(a,1,2)),rewrite(107(15),107(21),107(23),107(29))]. given #126 (A,wt=19): 72 ((c1 * c2) * x) * ((c2 * (c2 * c1)) * x) != (c1 * c2) * x. [ur(40,b,25,a(flip))]. given #127 (F,wt=17): 141 x * ((c2 * c1) * (c2 * (c1 * c2))) != x * (c1 * c2). [ur(4,b,102,a)]. given #128 (F,wt=17): 145 (c2 * (c2 * c1)) * (c1 * (c1 * (c1 * c2))) != c2 * c1. [ur(22,b,16,a)]. given #129 (T,wt=50): 367 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(107(a,1),100(a,1,2,2)),rewrite(107(16),107(22),107(28))]. given #130 (T,wt=50): 563 (((((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(189(a,1),193(a,1,1,1,2)),rewrite(189(19),189(22),189(28),189(30),189(32))]. given #131 (A,wt=21): 74 (x * (c1 * (c1 * c2))) * (x * (c2 * c1)) != x * (c1 * (c1 * c2)). [ur(40,b,16,a(flip))]. given #132 (F,wt=17): 147 (c1 * (c1 * c2)) * (c2 * (c2 * (c2 * c1))) != c1 * c2. [ur(22,b,26,a(flip))]. given #133 (F,wt=17): 164 ((c1 * c2) * (c1 * (c2 * c1))) * (c2 * c1) != c2 * c1. [ur(43,b,104,a)]. given #134 (T,wt=50): 580 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(189(a,1),194(a,1,2,1,1,2)),rewrite(189(17),189(19),189(22),189(30),189(32))]. given #135 (T,wt=51): 654 (((((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(195(a,1),189(a,1,1,1,2)),rewrite(195(21),195(29),195(31),195(33),195(36))]. given #136 (A,wt=21): 75 ((c1 * (c1 * c2)) * x) * ((c2 * c1) * x) != (c1 * (c1 * c2)) * x. [ur(40,b,15,a(flip))]. given #137 (F,wt=17): 166 (c2 * c1) * ((c1 * c2) * (c1 * (c2 * c1))) != c2 * c1. [ur(41,b,104,a)]. given #138 (F,wt=17): 170 ((c1 * c2) * (c1 * (c2 * c1))) * x != (c2 * c1) * x. [ur(5,b,104,a)]. given #139 (T,wt=52): 421 (((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(189(a,1),106(a,1,2)),rewrite(189(19),189(27),189(33))]. given #140 (T,wt=54): 424 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(189(a,1),100(a,1,2,2)),rewrite(189(18),189(26),189(32))]. given #141 (A,wt=21): 76 (x * (c2 * (c2 * c1))) * (x * (c1 * c2)) != x * (c2 * (c2 * c1)). [ur(40,b,26,a)]. given #142 (F,wt=17): 171 x * ((c1 * c2) * (c1 * (c2 * c1))) != x * (c2 * c1). [ur(4,b,104,a)]. given #143 (F,wt=17): 256 (c2 * (c1 * c2)) * ((c2 * c1) * (c1 * c2)) != c1 * c2. [para(99(a,1),29(a,2))]. given #144 (T,wt=54): 661 (((((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(195(a,1),193(a,1,1,1,2)),rewrite(195(21),195(24),195(32),195(34),195(36))]. given #145 (T,wt=54): 662 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(195(a,1),194(a,1,2,1,1,2)),rewrite(195(21),195(23),195(26),195(34),195(36))]. given #146 (A,wt=25): 77 (x * (c2 * (c2 * c1))) * (y * (y * (x * (c1 * c2)))) != y * (x * (c1 * c2)). [ur(12,b,26,a)]. given #147 (F,wt=17): 277 (c1 * (c2 * c1)) * ((c1 * c2) * (c2 * c1)) != c2 * c1. [ur(101,b,25,a)]. given #148 (F,wt=17): 808 c1 * (c2 * ((c1 * (c1 * c2)) * (c2 * c1))) != c2 * c1. [ur(10,b,87,a(flip))]. given #149 (T,wt=55): 665 ((((((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(195(a,1),195(a,1,1,1,1,2)),rewrite(195(21),195(23),195(31),195(33),195(35),195(38))]. given #150 (T,wt=56): 423 (((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(189(a,1),124(a,1,2)),rewrite(189(19),189(25),189(27),189(35))]. given #151 (A,wt=27): 78 (x * (c1 * c2)) * (y * (y * (x * (c2 * (c2 * c1))))) != y * (x * (c2 * (c2 * c1))). [ur(11,b,26,a)]. given #152 (F,wt=17): 962 c1 * (c2 * ((c2 * c1) * (c1 * (c1 * c2)))) != c2 * c1. [ur(10,b,114,a(flip))]. given #153 (F,wt=17): 1132 c2 * (c1 * ((c2 * (c2 * c1)) * (c1 * c2))) != c1 * c2. [ur(10,b,122,a(flip))]. given #154 (T,wt=56): 479 (((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(189(a,1),142(a,1,1,2)),rewrite(189(17),189(19),189(25),189(27),189(35))]. given #155 (T,wt=58): 760 ((((((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(195(a,1),283(a,1,1,1,1,2)),rewrite(195(21),195(23),195(26),195(34),195(36),195(38))]. given #156 (A,wt=19): 82 (x * (c1 * c2)) * (x * (c2 * (c2 * c1))) != x * (c1 * c2). [ur(40,b,26,a(flip))]. given #157 (F,wt=17): 1326 c2 * (c1 * ((c1 * c2) * (c2 * (c2 * c1)))) != c1 * c2. [ur(10,b,133,a(flip))]. given #158 (F,wt=17): 1481 c2 * (c1 * ((c2 * c1) * (c2 * (c1 * c2)))) != c1 * c2. [ur(10,b,141,a(flip))]. given #159 (T,wt=58): 839 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(195(a,1),295(a,1,2,1,1,2)),rewrite(195(21),195(23),195(26),195(34),195(36),195(38))]. given #160 (T,wt=59): 846 ((((((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(330(a,1),195(a,1,1,1,1,2)),rewrite(330(23),330(25),330(35),330(37),330(39),330(42))]. given #161 (A,wt=23): 84 ((c1 * (c1 * c2)) * (c2 * c1)) * (x * (x * (c2 * c1))) != x * (c2 * c1). [ur(12,b,46,a)]. given #162 (F,wt=17): 1687 c1 * (c2 * ((c1 * c2) * (c1 * (c2 * c1)))) != c2 * c1. [ur(10,b,171,a(flip))]. given #163 (F,wt=19): 92 (x * (c1 * (c1 * c2))) * (x * (c2 * c1)) != x * (c2 * c1). [ur(42,b,16,a)]. given #164 (T,wt=60): 653 (((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(195(a,1),124(a,1,2)),rewrite(195(21),195(29),195(31),195(39))]. given #165 (T,wt=62): 480 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(189(a,1),125(a,1,2,2)),rewrite(189(20),189(26),189(28),189(36))]. given #166 (A,wt=29): 85 (c2 * c1) * (x * (x * ((c1 * (c1 * c2)) * (c2 * c1)))) != x * ((c1 * (c1 * c2)) * (c2 * c1)). [ur(11,b,46,a)]. given #167 (F,wt=19): 93 ((c1 * (c1 * c2)) * x) * ((c2 * c1) * x) != (c2 * c1) * x. [ur(42,b,15,a)]. given #168 (F,wt=19): 95 (x * (c2 * (c2 * c1))) * (x * (c1 * c2)) != x * (c1 * c2). [ur(42,b,26,a(flip))]. given #169 (T,wt=62): 851 ((((((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(330(a,1),283(a,1,1,1,1,2)),rewrite(330(23),330(25),330(28),330(38),330(40),330(42))]. given #170 (T,wt=62): 853 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(330(a,1),295(a,1,2,1,1,2)),rewrite(330(25),330(27),330(30),330(38),330(40),330(42))]. given #171 (A,wt=23): 89 (c2 * c1) * ((c1 * (c1 * c2)) * (c2 * c1)) != (c1 * (c1 * c2)) * (c2 * c1). [ur(42,b,46,a)]. given #172 (F,wt=19): 96 ((c2 * (c2 * c1)) * x) * ((c1 * c2) * x) != (c1 * c2) * x. [ur(42,b,25,a(flip))]. given #173 (F,wt=19): 176 ((c2 * c1) * (c1 * (c1 * c2))) * x != (c1 * (c1 * c2)) * x. [ur(5,b,45,a)]. given #174 (T,wt=63): 854 (((((((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(330(a,1),330(a,1,1,1,1,2)),rewrite(330(25),330(27),330(35),330(37),330(39),330(41),330(44))]. given #175 (T,wt=64): 657 ((((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(195(a,1),142(a,1,1,2)),rewrite(195(21),195(23),195(31),195(33),195(41))]. given #176 (A,wt=21): 90 (x * (c1 * c2)) * (x * (c2 * (c2 * c1))) != x * (c2 * (c2 * c1)). [ur(42,b,26,a)]. given #177 (F,wt=19): 177 x * ((c2 * c1) * (c1 * (c1 * c2))) != x * (c1 * (c1 * c2)). [ur(4,b,45,a)]. given #178 (F,wt=19): 183 ((c2 * c1) * (c1 * (c1 * c2))) * (c2 * (c1 * c2)) != c1 * c2. [ur(51,b,45,a(flip))]. given #179 (T,wt=66): 658 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(195(a,1),125(a,1,2,2)),rewrite(195(22),195(30),195(32),195(40))]. given #180 (T,wt=66): 985 (((((((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(330(a,1),334(a,1,1,1,1,2)),rewrite(330(25),330(27),330(30),330(38),330(40),330(42),330(44))]. given #181 (A,wt=21): 91 ((c1 * c2) * x) * ((c2 * (c2 * c1)) * x) != (c2 * (c2 * c1)) * x. [ur(42,b,25,a)]. given #182 (F,wt=19): 220 ((c1 * c2) * (c1 * (c2 * c1))) * x != (c1 * (c1 * c2)) * x. [ur(5,b,56,a)]. given #183 (F,wt=19): 221 x * ((c1 * c2) * (c1 * (c2 * c1))) != x * (c1 * (c1 * c2)). [ur(4,b,56,a)]. given #184 (T,wt=66): 1011 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(330(a,1),335(a,1,2,1,1,1,2)),rewrite(330(23),330(25),330(27),330(30),330(40),330(42),330(44))]. given #185 (T,wt=67): 1052 (((((((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(336(a,1),330(a,1,1,1,1,2)),rewrite(336(27),336(29),336(39),336(41),336(43),336(45),336(48))]. given #186 (A,wt=21): 97 (x * (c2 * c1)) * (x * (c1 * (c1 * c2))) != x * (c1 * (c1 * c2)). [ur(42,b,16,a(flip))]. given #187 (F,wt=19): 222 ((c1 * c2) * (c1 * (c2 * c1))) * (c2 * (c1 * c2)) != c1 * c2. [ur(51,b,56,a(flip))]. given #188 (F,wt=19): 229 ((c1 * (c1 * c2)) * (c2 * c1)) * x != (c1 * (c1 * c2)) * x. [ur(5,b,65,a)]. given #189 (T,wt=68): 670 ((((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(195(a,1),190(a,1,1,2)),rewrite(195(21),195(23),195(31),195(33),195(41),195(43))]. given #190 (T,wt=68): 741 ((((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(195(a,1),192(a,1,1,2)),rewrite(195(21),195(23),195(31),195(33),195(41),195(43))]. given #191 (A,wt=21): 98 ((c2 * c1) * x) * ((c1 * (c1 * c2)) * x) != (c1 * (c1 * c2)) * x. [ur(42,b,15,a(flip))]. given #192 (F,wt=19): 230 x * ((c1 * (c1 * c2)) * (c2 * c1)) != x * (c1 * (c1 * c2)). [ur(4,b,65,a)]. given #193 (F,wt=19): 231 ((c1 * (c1 * c2)) * (c2 * c1)) * (c2 * (c1 * c2)) != c1 * c2. [ur(51,b,65,a(flip))]. given #194 (T,wt=70): 1056 (((((((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(336(a,1),334(a,1,1,1,1,2)),rewrite(336(27),336(29),336(32),336(42),336(44),336(46),336(48))]. given #195 (T,wt=70): 1057 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(336(a,1),335(a,1,2,1,1,1,2)),rewrite(336(27),336(29),336(31),336(34),336(44),336(46),336(48))]. given #196 (A,wt=23): 110 ((c2 * c1) * (c1 * (c1 * c2))) * (c2 * c1) != (c2 * c1) * (c1 * (c1 * c2)). [ur(40,b,64,a)]. given #197 (F,wt=19): 248 x * ((c2 * c1) * ((c1 * (c1 * c2)) * x)) != (c2 * c1) * x. [ur(10,b,29,a)]. given #198 (F,wt=19): 261 ((c1 * c2) * (c2 * (c2 * c1))) * x != (c2 * (c2 * c1)) * x. [ur(5,b,66,a)]. given #199 (T,wt=71): 1058 ((((((((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(336(a,1),336(a,1,1,1,1,1,2)),rewrite(336(27),336(29),336(31),336(41),336(43),336(45),336(47),336(50))]. given #200 (T,wt=72): 847 ((((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(330(a,1),190(a,1,1,2)),rewrite(330(23),330(25),330(35),330(37),330(45),330(47))]. given #201 (A,wt=23): 111 ((c2 * c1) * (c1 * (c1 * c2))) * (x * (x * (c2 * c1))) != x * (c2 * c1). [ur(12,b,64,a)]. given #202 (F,wt=19): 262 x * ((c1 * c2) * (c2 * (c2 * c1))) != x * (c2 * (c2 * c1)). [ur(4,b,66,a)]. given #203 (F,wt=19): 263 ((c1 * c2) * (c2 * (c2 * c1))) * (c1 * (c2 * c1)) != c2 * c1. [ur(51,b,66,a(flip))]. given #204 (T,wt=74): 841 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(330(a,1),125(a,1,2,2)),rewrite(330(26),330(34),330(36),330(46))]. given #205 (T,wt=74): 1159 ((((((((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(336(a,1),377(a,1,1,1,1,1,2)),rewrite(336(27),336(29),336(31),336(34),336(44),336(46),336(48),336(50))]. given #206 (A,wt=29): 112 (c2 * c1) * (x * (x * ((c2 * c1) * (c1 * (c1 * c2))))) != x * ((c2 * c1) * (c1 * (c1 * c2))). [ur(11,b,64,a)]. given #207 (F,wt=19): 270 ((c2 * (c2 * c1)) * (c1 * c2)) * x != (c2 * (c2 * c1)) * x. [ur(5,b,69,a)]. given #208 (F,wt=19): 271 x * ((c2 * (c2 * c1)) * (c1 * c2)) != x * (c2 * (c2 * c1)). [ur(4,b,69,a)]. given #209 (T,wt=74): 1214 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(336(a,1),420(a,1,2,1,1,1,2)),rewrite(336(27),336(29),336(31),336(34),336(44),336(46),336(48),336(50))]. given #210 (T,wt=75): 1224 ((((((((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(422(a,1),336(a,1,1,1,1,1,2)),rewrite(422(29),422(31),422(33),422(45),422(47),422(49),422(51),422(54))]. given #211 (A,wt=23): 116 (c1 * c2) * ((c2 * (c2 * c1)) * (c1 * c2)) != (c2 * (c2 * c1)) * (c1 * c2). [ur(42,b,67,a)]. given #212 (F,wt=19): 272 ((c2 * (c2 * c1)) * (c1 * c2)) * (c1 * (c2 * c1)) != c2 * c1. [ur(51,b,69,a(flip))]. given #213 (F,wt=19): 317 ((c2 * c1) * (c2 * (c1 * c2))) * x != (c2 * (c2 * c1)) * x. [ur(5,b,79,a)]. given #214 (T,wt=76): 850 (((((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(330(a,1),192(a,1,1,2)),rewrite(330(25),330(27),330(37),330(39),330(47),330(49))]. given #215 (T,wt=78): 894 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(330(a,1),191(a,1,2,1,2)),rewrite(330(23),330(26),330(36),330(38),330(46),330(48))]. given #216 (A,wt=23): 119 ((c2 * (c2 * c1)) * (c1 * c2)) * (x * (x * (c1 * c2))) != x * (c1 * c2). [ur(12,b,67,a)]. given #217 (F,wt=19): 318 x * ((c2 * c1) * (c2 * (c1 * c2))) != x * (c2 * (c2 * c1)). [ur(4,b,79,a)]. given #218 (F,wt=19): 319 ((c2 * c1) * (c2 * (c1 * c2))) * (c1 * (c2 * c1)) != c2 * c1. [ur(51,b,79,a(flip))]. given #219 (T,wt=78): 1227 ((((((((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(422(a,1),377(a,1,1,1,1,1,2)),rewrite(422(29),422(31),422(33),422(36),422(48),422(50),422(52),422(54))]. given #220 (T,wt=78): 1228 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(422(a,1),420(a,1,2,1,1,1,2)),rewrite(422(31),422(33),422(35),422(38),422(48),422(50),422(52),422(54))]. given #221 (A,wt=29): 120 (c1 * c2) * (x * (x * ((c2 * (c2 * c1)) * (c1 * c2)))) != x * ((c2 * (c2 * c1)) * (c1 * c2)). [ur(11,b,67,a)]. given #222 (F,wt=19): 321 (c2 * ((c2 * c1) * (c1 * (c1 * c2)))) * (c1 * c2) != c1 * c2. [ur(43,b,178,a)]. given #223 (F,wt=19): 323 (c1 * c2) * (c2 * ((c2 * c1) * (c1 * (c1 * c2)))) != c1 * c2. [ur(41,b,178,a)]. given #224 (T,wt=79): 1229 (((((((((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(422(a,1),422(a,1,1,1,1,1,2)),rewrite(422(31),422(33),422(35),422(45),422(47),422(49),422(51),422(53),422(56))]. given #225 (T,wt=80): 893 (((((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(330(a,1),235(a,1,1,2)),rewrite(330(25),330(27),330(35),330(37),330(39),330(49),330(51))]. given #226 (A,wt=23): 129 ((c1 * c2) * (c2 * (c2 * c1))) * (c1 * c2) != (c1 * c2) * (c2 * (c2 * c1)). [ur(40,b,73,a)]. given #227 (F,wt=19): 327 (c2 * ((c2 * c1) * (c1 * (c1 * c2)))) * x != (c1 * c2) * x. [ur(5,b,178,a)]. given #228 (F,wt=19): 328 x * (c2 * ((c2 * c1) * (c1 * (c1 * c2)))) != x * (c1 * c2). [ur(4,b,178,a)]. given #229 (T,wt=80): 1050 (((((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(336(a,1),192(a,1,1,2)),rewrite(336(27),336(29),336(39),336(41),336(51),336(53))]. given #230 (T,wt=82): 1357 (((((((((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(422(a,1),425(a,1,1,1,1,1,2)),rewrite(422(31),422(33),422(35),422(38),422(48),422(50),422(52),422(54),422(56))]. given #231 (A,wt=23): 130 ((c1 * c2) * (c2 * (c2 * c1))) * (x * (x * (c1 * c2))) != x * (c1 * c2). [ur(12,b,73,a)]. given #232 (F,wt=19): 350 c1 * ((c1 * (c1 * c2)) * (c2 * (c2 * (c2 * c1)))) != c2 * c1. [ur(10,b,31,a(flip))]. given #233 (F,wt=19): 351 (c2 * ((c1 * c2) * (c1 * (c2 * c1)))) * (c1 * c2) != c1 * c2. [ur(43,b,223,a)]. given #234 (T,wt=82): 1382 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(422(a,1),426(a,1,2,1,1,1,1,2)),rewrite(422(29),422(31),422(33),422(35),422(38),422(50),422(52),422(54),422(56))]. given #235 (T,wt=83): 1427 (((((((((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(427(a,1),422(a,1,1,1,1,1,2)),rewrite(427(33),427(35),427(37),427(49),427(51),427(53),427(55),427(57),427(60))]. given #236 (A,wt=29): 131 (c1 * c2) * (x * (x * ((c1 * c2) * (c2 * (c2 * c1))))) != x * ((c1 * c2) * (c2 * (c2 * c1))). [ur(11,b,73,a)]. given #237 (F,wt=19): 353 (c1 * c2) * (c2 * ((c1 * c2) * (c1 * (c2 * c1)))) != c1 * c2. [ur(41,b,223,a)]. given #238 (F,wt=19): 357 (c2 * ((c1 * c2) * (c1 * (c2 * c1)))) * x != (c1 * c2) * x. [ur(5,b,223,a)]. given #239 (T,wt=84): 1054 (((((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(336(a,1),235(a,1,1,2)),rewrite(336(27),336(29),336(39),336(41),336(43),336(53),336(55))]. given #240 (T,wt=86): 1055 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(336(a,1),191(a,1,2,1,2)),rewrite(336(27),336(30),336(40),336(42),336(52),336(54))]. given #241 (A,wt=23): 135 (c1 * c2) * ((c2 * c1) * (c2 * (c1 * c2))) != (c2 * c1) * (c2 * (c1 * c2)). [ur(42,b,102,a)]. given #242 (F,wt=19): 358 x * (c2 * ((c1 * c2) * (c1 * (c2 * c1)))) != x * (c1 * c2). [ur(4,b,223,a)]. given #243 (F,wt=19): 359 (c2 * ((c1 * (c1 * c2)) * (c2 * c1))) * (c1 * c2) != c1 * c2. [ur(43,b,232,a)]. given #244 (T,wt=86): 1428 (((((((((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(427(a,1),425(a,1,1,1,1,1,2)),rewrite(427(33),427(35),427(37),427(40),427(52),427(54),427(56),427(58),427(60))]. given #245 (T,wt=86): 1429 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(427(a,1),426(a,1,2,1,1,1,1,2)),rewrite(427(33),427(35),427(37),427(39),427(42),427(54),427(56),427(58),427(60))]. given #246 (A,wt=23): 137 ((c2 * c1) * (c2 * (c1 * c2))) * (c1 * c2) != (c2 * c1) * (c2 * (c1 * c2)). [ur(40,b,102,a)]. given #247 (F,wt=19): 361 (c1 * c2) * (c2 * ((c1 * (c1 * c2)) * (c2 * c1))) != c1 * c2. [ur(41,b,232,a)]. given #248 (F,wt=19): 365 (c2 * ((c1 * (c1 * c2)) * (c2 * c1))) * x != (c1 * c2) * x. [ur(5,b,232,a)]. given #249 (T,wt=87): 1430 ((((((((((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(427(a,1),427(a,1,1,1,1,1,1,2)),rewrite(427(33),427(35),427(37),427(39),427(51),427(53),427(55),427(57),427(59),427(62))]. given #250 (T,wt=88): 1059 ((((((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(336(a,1),239(a,1,1,1,2)),rewrite(336(27),336(29),336(31),336(41),336(43),336(45),336(55),336(57))]. given #251 (A,wt=23): 138 ((c2 * c1) * (c2 * (c1 * c2))) * (x * (x * (c1 * c2))) != x * (c1 * c2). [ur(12,b,102,a)]. given #252 (F,wt=19): 366 x * (c2 * ((c1 * (c1 * c2)) * (c2 * c1))) != x * (c1 * c2). [ur(4,b,232,a)]. given #253 (F,wt=19): 392 (c1 * ((c1 * c2) * (c2 * (c2 * c1)))) * (c2 * c1) != c2 * c1. [ur(43,b,264,a)]. given #254 (T,wt=90): 1133 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(336(a,1),329(a,1,2,1,2)),rewrite(336(27),336(30),336(40),336(42),336(44),336(54),336(56))]. given #255 (T,wt=90): 1510 ((((((((((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(427(a,1),563(a,1,1,1,1,1,1,2)),rewrite(427(33),427(35),427(37),427(39),427(42),427(54),427(56),427(58),427(60),427(62))]. given #256 (A,wt=29): 139 (c1 * c2) * (x * (x * ((c2 * c1) * (c2 * (c1 * c2))))) != x * ((c2 * c1) * (c2 * (c1 * c2))). [ur(11,b,102,a)]. given #257 (F,wt=19): 394 (c2 * c1) * (c1 * ((c1 * c2) * (c2 * (c2 * c1)))) != c2 * c1. [ur(41,b,264,a)]. given #258 (F,wt=19): 398 (c1 * ((c1 * c2) * (c2 * (c2 * c1)))) * x != (c2 * c1) * x. [ur(5,b,264,a)]. given #259 (T,wt=90): 1571 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(427(a,1),580(a,1,2,1,1,1,1,2)),rewrite(427(33),427(35),427(37),427(39),427(42),427(54),427(56),427(58),427(60),427(62))]. given #260 (T,wt=91): 1580 ((((((((((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(654(a,1),427(a,1,1,1,1,1,1,2)),rewrite(654(35),654(37),654(39),654(41),654(55),654(57),654(59),654(61),654(63),654(66))]. given #261 (A,wt=21): 143 (c2 * (c2 * (c2 * c1))) * ((c2 * c1) * (c1 * c2)) != c2 * (c2 * c1). [ur(22,b,26,a)]. given #262 (F,wt=19): 399 x * (c1 * ((c1 * c2) * (c2 * (c2 * c1)))) != x * (c2 * c1). [ur(4,b,264,a)]. given #263 (F,wt=19): 400 (c1 * ((c2 * (c2 * c1)) * (c1 * c2))) * (c2 * c1) != c2 * c1. [ur(43,b,273,a)]. given #264 (T,wt=92): 1223 ((((((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(422(a,1),235(a,1,1,2)),rewrite(422(31),422(33),422(43),422(45),422(47),422(59),422(61))]. given #265 (T,wt=92): 1225 ((((((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(422(a,1),239(a,1,1,1,2)),rewrite(422(29),422(31),422(33),422(43),422(45),422(47),422(59),422(61))]. given #266 (A,wt=29): 144 (x * (x * (c2 * (c2 * c1)))) * ((c1 * c2) * (x * (c2 * (c2 * c1)))) != x * (c2 * (c2 * c1)). [ur(22,b,25,a)]. given #267 (F,wt=19): 402 (c2 * c1) * (c1 * ((c2 * (c2 * c1)) * (c1 * c2))) != c2 * c1. [ur(41,b,273,a)]. given #268 (F,wt=19): 406 (c1 * ((c2 * (c2 * c1)) * (c1 * c2))) * x != (c2 * c1) * x. [ur(5,b,273,a)]. given #269 (T,wt=94): 1581 ((((((((((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(654(a,1),563(a,1,1,1,1,1,1,2)),rewrite(654(35),654(37),654(39),654(41),654(44),654(58),654(60),654(62),654(64),654(66))]. given #270 (T,wt=94): 1582 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(654(a,1),580(a,1,2,1,1,1,1,2)),rewrite(654(37),654(39),654(41),654(43),654(46),654(58),654(60),654(62),654(64),654(66))]. given #271 (A,wt=25): 146 (x * (x * (c2 * c1))) * ((c1 * (c1 * c2)) * (x * (c2 * c1))) != x * (c2 * c1). [ur(22,b,15,a)]. given #272 (F,wt=19): 407 x * (c1 * ((c2 * (c2 * c1)) * (c1 * c2))) != x * (c2 * c1). [ur(4,b,273,a)]. given #273 (F,wt=19): 445 (c1 * ((c2 * c1) * (c2 * (c1 * c2)))) * (c2 * c1) != c2 * c1. [ur(43,b,320,a)]. given #274 (T,wt=95): 1583 (((((((((((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(654(a,1),654(a,1,1,1,1,1,1,2)),rewrite(654(37),654(39),654(41),654(43),654(55),654(57),654(59),654(61),654(63),654(65),654(68))]. given #275 (T,wt=96): 1269 ((((((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(422(a,1),332(a,1,1,1,2)),rewrite(422(29),422(31),422(33),422(45),422(47),422(49),422(59),422(61),422(63))]. given #276 (A,wt=25): 148 (x * (x * (c1 * c2))) * ((c2 * (c2 * c1)) * (x * (c1 * c2))) != x * (c1 * c2). [ur(22,b,25,a(flip))]. given #277 (F,wt=19): 447 (c2 * c1) * (c1 * ((c2 * c1) * (c2 * (c1 * c2)))) != c2 * c1. [ur(41,b,320,a)]. given #278 (F,wt=19): 451 (c1 * ((c2 * c1) * (c2 * (c1 * c2)))) * x != (c2 * c1) * x. [ur(5,b,320,a)]. given #279 (T,wt=98): 1226 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(422(a,1),329(a,1,2,1,2)),rewrite(422(31),422(34),422(44),422(46),422(48),422(60),422(62))]. given #280 (T,wt=98): 1713 (((((((((((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(654(a,1),661(a,1,1,1,1,1,1,2)),rewrite(654(37),654(39),654(41),654(43),654(46),654(58),654(60),654(62),654(64),654(66),654(68))]. given #281 (A,wt=21): 149 (c1 * (c1 * (c1 * c2))) * ((c1 * c2) * (c2 * c1)) != c1 * (c1 * c2). [ur(22,b,16,a(flip))]. given #282 (F,wt=19): 452 x * (c1 * ((c2 * c1) * (c2 * (c1 * c2)))) != x * (c2 * c1). [ur(4,b,320,a)]. given #283 (F,wt=19): 510 (c2 * c1) * (x * (x * (c1 * (c1 * c2)))) != x * (c2 * c1). [ur(10,b,54,a)]. given #284 (T,wt=98): 1731 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(654(a,1),662(a,1,2,1,1,1,1,1,2)),rewrite(654(35),654(37),654(39),654(41),654(43),654(46),654(60),654(62),654(64),654(66),654(68))]. given #285 (T,wt=99): 1783 (((((((((((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(665(a,1),654(a,1,1,1,1,1,1,2)),rewrite(665(39),665(41),665(43),665(45),665(59),665(61),665(63),665(65),665(67),665(69),665(72))]. given #286 (A,wt=29): 150 (x * (x * (c1 * (c1 * c2)))) * ((c2 * c1) * (x * (c1 * (c1 * c2)))) != x * (c1 * (c1 * c2)). [ur(22,b,15,a(flip))]. given #287 (F,wt=19): 598 c2 * ((c2 * (c2 * c1)) * (c1 * (c1 * (c1 * c2)))) != c1 * c2. [ur(10,b,49,a(flip))]. given #288 (F,wt=19): 624 x * ((c1 * c2) * ((c2 * (c2 * c1)) * x)) != (c1 * c2) * x. [ur(10,b,60,a(flip))]. given #289 (T,wt=100): 1270 (((((((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(422(a,1),333(a,1,1,1,2)),rewrite(422(31),422(33),422(35),422(47),422(49),422(51),422(61),422(63),422(65))]. given #290 (T,wt=19): 715 (c1 * c2) * (x * (x * (c2 * (c2 * c1)))) != x * (c1 * c2). [ur(10,b,81,a(flip))]. given #291 (A,wt=37): 152 (c1 * (c1 * c2)) * ((c1 * (c1 * c2)) * ((c2 * c1) * (c1 * (c1 * c2)))) != (c1 * (c1 * c2)) * ((c2 * c1) * (c1 * (c1 * c2))). [ur(63,b,27,a)]. given #292 (F,wt=19): 890 (c2 * c1) * (c1 * (c1 * c2)) != (c1 * (c1 * c2)) * (c2 * c1). [ur(10,b,109,a),flip(a)]. given #293 (F,wt=19): 1249 (c2 * (c2 * c1)) * (c1 * c2) != (c1 * c2) * (c2 * (c2 * c1)). [ur(10,b,128,a)]. given #294 (T,wt=19): 2988 c2 * (c1 * (c2 * ((c2 * c1) * (c1 * (c1 * c2))))) != c1 * c2. [ur(10,b,328,a(flip))]. given #295 (T,wt=19): 3169 c2 * (c1 * (c2 * ((c1 * c2) * (c1 * (c2 * c1))))) != c1 * c2. [ur(10,b,358,a(flip))]. given #296 (A,wt=25): 153 (c1 * (c1 * c2)) * ((c2 * c1) * (c1 * (c1 * c2))) != (c2 * c1) * (c1 * (c1 * c2)). [ur(44,b,27,a)]. given #297 (F,wt=19): 3328 c2 * (c1 * (c2 * ((c1 * (c1 * c2)) * (c2 * c1)))) != c1 * c2. [ur(10,b,366,a(flip))]. given #298 (F,wt=19): 3476 c1 * (c2 * (c1 * ((c1 * c2) * (c2 * (c2 * c1))))) != c2 * c1. [ur(10,b,399,a(flip))]. given #299 (T,wt=19): 3643 c1 * (c2 * (c1 * ((c2 * (c2 * c1)) * (c1 * c2)))) != c2 * c1. [ur(10,b,407,a(flip))]. given #300 (T,wt=19): 3780 c1 * (c2 * (c1 * ((c2 * c1) * (c2 * (c1 * c2))))) != c2 * c1. [ur(10,b,452,a(flip))]. given #301 (A,wt=25): 154 (x * ((c1 * (c1 * c2)) * ((c2 * c1) * x))) * ((c2 * c1) * x) != (c2 * c1) * x. [ur(43,b,27,a)]. given #302 (F,wt=21): 172 ((c2 * c1) * (c1 * (c1 * c2))) * (c1 * (c1 * c2)) != c1 * (c1 * c2). [ur(43,b,45,a)]. given #303 (F,wt=21): 173 (c1 * (c1 * c2)) * ((c2 * c1) * (c1 * (c1 * c2))) != c1 * (c1 * c2). [ur(41,b,45,a)]. given #304 (T,wt=21): 180 (c2 * (c1 * c2)) * ((c2 * c1) * (c2 * (c2 * c1))) != c2 * (c2 * c1). [ur(51,b,26,a)]. given #305 (T,wt=21): 186 (c1 * (c2 * c1)) * ((c1 * c2) * (c1 * (c1 * c2))) != c1 * (c1 * c2). [ur(51,b,16,a(flip))]. given #306 (A,wt=33): 155 ((c2 * c1) * x) * (x * ((c1 * (c1 * c2)) * ((c2 * c1) * x))) != x * ((c1 * (c1 * c2)) * ((c2 * c1) * x)). [ur(42,b,27,a)]. given #307 (F,wt=21): 205 (((c2 * c1) * x) * y) * z != (((c1 * (c1 * c2)) * x) * y) * z. [ur(5,b,28,a)]. given #308 (F,wt=21): 206 x * (((c2 * c1) * y) * z) != x * (((c1 * (c1 * c2)) * y) * z). [ur(4,b,28,a)]. given #309 (T,wt=21): 214 ((c1 * c2) * (c1 * (c2 * c1))) * (c1 * (c1 * c2)) != c1 * (c1 * c2). [ur(43,b,56,a)]. given #310 (T,wt=21): 216 (c1 * (c1 * c2)) * ((c1 * c2) * (c1 * (c2 * c1))) != c1 * (c1 * c2). [ur(41,b,56,a)]. given #311 (A,wt=25): 156 ((c2 * c1) * x) * (x * ((c1 * (c1 * c2)) * ((c2 * c1) * x))) != (c2 * c1) * x. [ur(41,b,27,a)]. given #312 (F,wt=21): 224 ((c1 * (c1 * c2)) * (c2 * c1)) * (c1 * (c1 * c2)) != c1 * (c1 * c2). [ur(43,b,65,a)]. given #313 (F,wt=21): 225 (c1 * (c1 * c2)) * ((c1 * (c1 * c2)) * (c2 * c1)) != c1 * (c1 * c2). [ur(41,b,65,a)]. given #314 (T,wt=21): 249 (x * ((c2 * c1) * y)) * z != (x * ((c1 * (c1 * c2)) * y)) * z. [ur(5,b,29,a)]. given #315 (T,wt=21): 250 x * (y * ((c2 * c1) * z)) != x * (y * ((c1 * (c1 * c2)) * z)). [ur(4,b,29,a)]. given #316 (A,wt=33): 157 (x * ((c1 * (c1 * c2)) * ((c2 * c1) * x))) * ((c2 * c1) * x) != x * ((c1 * (c1 * c2)) * ((c2 * c1) * x)). [ur(40,b,27,a)]. given #317 (F,wt=21): 253 x * ((c1 * (c1 * c2)) * ((c2 * c1) * x)) != (c1 * (c1 * c2)) * x. [ur(10,b,29,a(flip))]. given #318 (F,wt=21): 257 ((c1 * c2) * (c2 * (c2 * c1))) * (c2 * (c2 * c1)) != c2 * (c2 * c1). [ur(43,b,66,a)]. given #319 (T,wt=21): 258 (c2 * (c2 * c1)) * ((c1 * c2) * (c2 * (c2 * c1))) != c2 * (c2 * c1). [ur(41,b,66,a)]. given #320 (T,wt=21): 265 ((c2 * (c2 * c1)) * (c1 * c2)) * (c2 * (c2 * c1)) != c2 * (c2 * c1). [ur(43,b,69,a)]. given #321 (A,wt=31): 158 (x * ((c1 * (c1 * c2)) * ((c2 * c1) * x))) * (y * (y * ((c2 * c1) * x))) != y * ((c2 * c1) * x). [ur(12,b,27,a)]. given #322 (F,wt=21): 266 (c2 * (c2 * c1)) * ((c2 * (c2 * c1)) * (c1 * c2)) != c2 * (c2 * c1). [ur(41,b,69,a)]. given #323 (F,wt=21): 278 (c1 * (c2 * c1)) * ((c2 * (c2 * c1)) * (c1 * (c1 * c2))) != c2 * c1. [ur(101,b,16,a)]. given #324 (T,wt=21): 281 (c2 * (c1 * c2)) * ((c1 * (c1 * c2)) * (c2 * (c2 * c1))) != c1 * c2. [ur(101,b,26,a(flip))]. given #325 (T,wt=21): 288 (c1 * (c1 * (c1 * c2))) * ((c2 * (c2 * c1)) * (c2 * c1)) != c2 * c1. [ur(103,b,16,a)]. given #326 (A,wt=39): 159 ((c2 * c1) * x) * (y * (y * (x * ((c1 * (c1 * c2)) * ((c2 * c1) * x))))) != y * (x * ((c1 * (c1 * c2)) * ((c2 * c1) * x))). [ur(11,b,27,a)]. given #327 (F,wt=21): 292 (c2 * (c2 * (c2 * c1))) * ((c1 * (c1 * c2)) * (c1 * c2)) != c1 * c2. [ur(103,b,26,a(flip))]. given #328 (F,wt=21): 311 ((c2 * c1) * (c2 * (c1 * c2))) * (c2 * (c2 * c1)) != c2 * (c2 * c1). [ur(43,b,79,a)]. given #329 (T,wt=21): 313 (c2 * (c2 * c1)) * ((c2 * c1) * (c2 * (c1 * c2))) != c2 * (c2 * c1). [ur(41,b,79,a)]. given #330 (T,wt=21): 331 ((c2 * c1) * (c1 * c2)) * ((c2 * (c1 * c2)) * (c1 * c2)) != c1 * c2. [para(107(a,1),28(a,2))]. given #331 (A,wt=23): 160 (x * ((c1 * (c1 * c2)) * ((c2 * c1) * x))) * y != ((c2 * c1) * x) * y. [ur(5,b,27,a)]. given #332 (F,wt=21): 411 ((c1 * c2) * (c2 * c1)) * ((c1 * (c2 * c1)) * (c2 * c1)) != c2 * c1. [ur(188,b,25,a)]. given #333 (F,wt=21): 466 ((x * (c2 * c1)) * y) * z != ((x * (c1 * (c1 * c2))) * y) * z. [ur(5,b,53,a)]. given #334 (T,wt=21): 467 x * ((y * (c2 * c1)) * z) != x * ((y * (c1 * (c1 * c2))) * z). [ur(4,b,53,a)]. given #335 (T,wt=21): 511 (x * (y * (c2 * c1))) * z != (x * (y * (c1 * (c1 * c2)))) * z. [ur(5,b,54,a)]. given #336 (A,wt=23): 161 x * (y * ((c1 * (c1 * c2)) * ((c2 * c1) * y))) != x * ((c2 * c1) * y). [ur(4,b,27,a)]. given #337 (F,wt=21): 512 x * (y * (z * (c2 * c1))) != x * (y * (z * (c1 * (c1 * c2)))). [ur(4,b,54,a)]. given #338 (F,wt=21): 519 (c1 * (c1 * c2)) * (x * (x * (c2 * c1))) != x * (c1 * (c1 * c2)). [ur(10,b,54,a(flip))]. given #339 (T,wt=21): 537 (((c2 * (c2 * c1)) * x) * y) * z != (((c1 * c2) * x) * y) * z. [ur(5,b,59,a)]. given #340 (T,wt=21): 538 x * (((c2 * (c2 * c1)) * y) * z) != x * (((c1 * c2) * y) * z). [ur(4,b,59,a)]. given #341 (A,wt=35): 162 (x * (x * (c2 * c1))) * ((x * (c2 * c1)) * ((c1 * (c1 * c2)) * ((c2 * c1) * (x * (c2 * c1))))) != x * (c2 * c1). [ur(22,b,27,a(flip))]. given #342 (F,wt=21): 613 x * ((c2 * (c2 * c1)) * ((c1 * c2) * x)) != (c2 * (c2 * c1)) * x. [ur(10,b,60,a)]. given #343 (F,wt=21): 614 (x * ((c2 * (c2 * c1)) * y)) * z != (x * ((c1 * c2) * y)) * z. [ur(5,b,60,a)]. given #344 (T,wt=21): 615 x * (y * ((c2 * (c2 * c1)) * z)) != x * (y * ((c1 * c2) * z)). [ur(4,b,60,a)]. given #345 (T,wt=21): 642 ((x * (c2 * (c2 * c1))) * y) * z != ((x * (c1 * c2)) * y) * z. [ur(5,b,80,a)]. given #346 (A,wt=29): 163 x * (((c2 * c1) * x) * ((c1 * (c1 * c2)) * ((c2 * c1) * ((c2 * c1) * x)))) != (c2 * c1) * x. [ur(10,b,27,a(flip))]. given #347 (F,wt=21): 643 x * ((y * (c2 * (c2 * c1))) * z) != x * ((y * (c1 * c2)) * z). [ur(4,b,80,a)]. given #348 (F,wt=21): 704 (c2 * (c2 * c1)) * (x * (x * (c1 * c2))) != x * (c2 * (c2 * c1)). [ur(10,b,81,a)]. given #349 (T,wt=21): 705 (x * (y * (c2 * (c2 * c1)))) * z != (x * (y * (c1 * c2))) * z. [ur(5,b,81,a)]. given #350 (T,wt=21): 706 x * (y * (z * (c2 * (c2 * c1)))) != x * (y * (z * (c1 * c2))). [ur(4,b,81,a)]. given #351 (A,wt=23): 165 (c2 * c1) * ((c1 * c2) * (c1 * (c2 * c1))) != (c1 * c2) * (c1 * (c2 * c1)). [ur(42,b,104,a)]. given #352 (F,wt=21): 729 (((c1 * (c1 * c2)) * (c2 * c1)) * x) * y != ((c2 * c1) * x) * y. [ur(5,b,86,a)]. given #353 (F,wt=21): 730 x * (((c1 * (c1 * c2)) * (c2 * c1)) * y) != x * ((c2 * c1) * y). [ur(4,b,86,a)]. given #354 (T,wt=21): 797 (x * ((c1 * (c1 * c2)) * (c2 * c1))) * y != (x * (c2 * c1)) * y. [ur(5,b,87,a)]. given #355 (T,wt=21): 798 x * (y * ((c1 * (c1 * c2)) * (c2 * c1))) != x * (y * (c2 * c1)). [ur(4,b,87,a)]. given #356 (A,wt=23): 167 ((c1 * c2) * (c1 * (c2 * c1))) * (c2 * c1) != (c1 * c2) * (c1 * (c2 * c1)). [ur(40,b,104,a)]. given #357 (F,wt=21): 806 (c2 * ((c1 * (c1 * c2)) * (c2 * c1))) * (c1 * (c2 * c1)) != c2 * c1. [ur(51,b,87,a(flip))]. given #358 (F,wt=21): 807 (c2 * (c2 * c1)) * (c1 * ((c1 * (c1 * c2)) * (c2 * c1))) != c2 * c1. [ur(22,b,87,a(flip))]. given #359 (T,wt=21): 809 ((c2 * c1) * ((c1 * (c1 * c2)) * (c2 * c1))) * (c2 * c1) != c2 * c1. [ur(43,b,88,a)]. given #360 (T,wt=21): 810 (c2 * c1) * ((c2 * c1) * ((c1 * (c1 * c2)) * (c2 * c1))) != c2 * c1. [ur(41,b,88,a)]. given #361 (A,wt=23): 168 ((c1 * c2) * (c1 * (c2 * c1))) * (x * (x * (c2 * c1))) != x * (c2 * c1). [ur(12,b,104,a)]. given #362 (F,wt=21): 814 ((c2 * c1) * ((c1 * (c1 * c2)) * (c2 * c1))) * x != (c2 * c1) * x. [ur(5,b,88,a)]. given #363 (F,wt=21): 815 x * ((c2 * c1) * ((c1 * (c1 * c2)) * (c2 * c1))) != x * (c2 * c1). [ur(4,b,88,a)]. given #364 (T,wt=21): 877 (((c1 * (c1 * c2)) * (c2 * c1)) * (c2 * c1)) * (c2 * c1) != c2 * c1. [ur(43,b,94,a)]. given #365 (T,wt=21): 878 (c2 * c1) * (((c1 * (c1 * c2)) * (c2 * c1)) * (c2 * c1)) != c2 * c1. [ur(41,b,94,a)]. given #366 (A,wt=29): 169 (c2 * c1) * (x * (x * ((c1 * c2) * (c1 * (c2 * c1))))) != x * ((c1 * c2) * (c1 * (c2 * c1))). [ur(11,b,104,a)]. given #367 (F,wt=21): 882 (((c1 * (c1 * c2)) * (c2 * c1)) * (c2 * c1)) * x != (c2 * c1) * x. [ur(5,b,94,a)]. given #368 (F,wt=21): 883 x * (((c1 * (c1 * c2)) * (c2 * c1)) * (c2 * c1)) != x * (c2 * c1). [ur(4,b,94,a)]. given #369 (T,wt=21): 885 ((c2 * c1) * ((c2 * c1) * (c1 * (c1 * c2)))) * (c2 * c1) != c2 * c1. [ur(43,b,109,a)]. given #370 (T,wt=21): 886 (c2 * c1) * ((c2 * c1) * ((c2 * c1) * (c1 * (c1 * c2)))) != c2 * c1. [ur(41,b,109,a)]. given #371 (A,wt=27): 174 ((c2 * c1) * (c1 * (c1 * c2))) * (x * (x * (c1 * (c1 * c2)))) != x * (c1 * (c1 * c2)). [ur(12,b,45,a)]. given #372 (F,wt=21): 891 ((c2 * c1) * ((c2 * c1) * (c1 * (c1 * c2)))) * x != (c2 * c1) * x. [ur(5,b,109,a)]. given #373 (F,wt=21): 892 x * ((c2 * c1) * ((c2 * c1) * (c1 * (c1 * c2)))) != x * (c2 * c1). [ur(4,b,109,a)]. given #374 (T,wt=21): 927 (((c2 * c1) * (c1 * (c1 * c2))) * x) * y != ((c2 * c1) * x) * y. [ur(5,b,113,a)]. given #375 (T,wt=21): 928 x * (((c2 * c1) * (c1 * (c1 * c2))) * y) != x * ((c2 * c1) * y). [ur(4,b,113,a)]. given #376 (A,wt=31): 175 (c1 * (c1 * c2)) * (x * (x * ((c2 * c1) * (c1 * (c1 * c2))))) != x * ((c2 * c1) * (c1 * (c1 * c2))). [ur(11,b,45,a)]. given #377 (F,wt=21): 950 (x * ((c2 * c1) * (c1 * (c1 * c2)))) * y != (x * (c2 * c1)) * y. [ur(5,b,114,a)]. given #378 (F,wt=21): 951 x * (y * ((c2 * c1) * (c1 * (c1 * c2)))) != x * (y * (c2 * c1)). [ur(4,b,114,a)]. given #379 (T,wt=21): 960 (c2 * ((c2 * c1) * (c1 * (c1 * c2)))) * (c1 * (c2 * c1)) != c2 * c1. [ur(51,b,114,a(flip))]. given #380 (T,wt=21): 961 (c2 * (c2 * c1)) * (c1 * ((c2 * c1) * (c1 * (c1 * c2)))) != c2 * c1. [ur(22,b,114,a(flip))]. given #381 (A,wt=29): 181 ((c1 * c2) * ((c2 * (c2 * c1)) * x)) * (x * ((c2 * (c2 * c1)) * x)) != (c2 * (c2 * c1)) * x. [ur(51,b,25,a)]. given #382 (F,wt=21): 1028 (((c2 * c1) * (c1 * (c1 * c2))) * (c2 * c1)) * (c2 * c1) != c2 * c1. [ur(43,b,115,a)]. given #383 (F,wt=21): 1029 (c2 * c1) * (((c2 * c1) * (c1 * (c1 * c2))) * (c2 * c1)) != c2 * c1. [ur(41,b,115,a)]. given #384 (T,wt=21): 1033 (((c2 * c1) * (c1 * (c1 * c2))) * (c2 * c1)) * x != (c2 * c1) * x. [ur(5,b,115,a)]. given #385 (T,wt=21): 1034 x * (((c2 * c1) * (c1 * (c1 * c2))) * (c2 * c1)) != x * (c2 * c1). [ur(4,b,115,a)]. given #386 (A,wt=25): 182 ((c1 * (c1 * c2)) * ((c2 * c1) * x)) * (x * ((c2 * c1) * x)) != (c2 * c1) * x. [ur(51,b,15,a)]. given #387 (F,wt=21): 1036 ((c1 * c2) * ((c2 * (c2 * c1)) * (c1 * c2))) * (c1 * c2) != c1 * c2. [ur(43,b,117,a)]. given #388 (F,wt=21): 1037 (c1 * c2) * ((c1 * c2) * ((c2 * (c2 * c1)) * (c1 * c2))) != c1 * c2. [ur(41,b,117,a)]. given #389 (T,wt=21): 1042 ((c1 * c2) * ((c2 * (c2 * c1)) * (c1 * c2))) * x != (c1 * c2) * x. [ur(5,b,117,a)]. given #390 (T,wt=21): 1043 x * ((c1 * c2) * ((c2 * (c2 * c1)) * (c1 * c2))) != x * (c1 * c2). [ur(4,b,117,a)]. given #391 (A,wt=35): 184 (((c2 * c1) * x) * ((c1 * (c1 * c2)) * ((c2 * c1) * ((c2 * c1) * x)))) * (x * ((c2 * c1) * x)) != (c2 * c1) * x. [ur(51,b,27,a(flip))]. given #392 (F,wt=21): 1094 (((c2 * (c2 * c1)) * (c1 * c2)) * x) * y != ((c1 * c2) * x) * y. [ur(5,b,121,a)]. given #393 (F,wt=21): 1095 x * (((c2 * (c2 * c1)) * (c1 * c2)) * y) != x * ((c1 * c2) * y). [ur(4,b,121,a)]. given #394 (T,wt=21): 1118 (x * ((c2 * (c2 * c1)) * (c1 * c2))) * y != (x * (c1 * c2)) * y. [ur(5,b,122,a)]. given #395 (T,wt=21): 1119 x * (y * ((c2 * (c2 * c1)) * (c1 * c2))) != x * (y * (c1 * c2)). [ur(4,b,122,a)]. given #396 (A,wt=25): 185 ((c2 * (c2 * c1)) * ((c1 * c2) * x)) * (x * ((c1 * c2) * x)) != (c1 * c2) * x. [ur(51,b,25,a(flip))]. given #397 (F,wt=21): 1130 (c1 * ((c2 * (c2 * c1)) * (c1 * c2))) * (c2 * (c1 * c2)) != c1 * c2. [ur(51,b,122,a(flip))]. given #398 (F,wt=21): 1131 (c1 * (c1 * c2)) * (c2 * ((c2 * (c2 * c1)) * (c1 * c2))) != c1 * c2. [ur(22,b,122,a(flip))]. given #399 (T,wt=21): 1174 (((c2 * (c2 * c1)) * (c1 * c2)) * (c1 * c2)) * (c1 * c2) != c1 * c2. [ur(43,b,123,a)]. given #400 (T,wt=21): 1175 (c1 * c2) * (((c2 * (c2 * c1)) * (c1 * c2)) * (c1 * c2)) != c1 * c2. [ur(41,b,123,a)]. given #401 (A,wt=29): 187 ((c2 * c1) * ((c1 * (c1 * c2)) * x)) * (x * ((c1 * (c1 * c2)) * x)) != (c1 * (c1 * c2)) * x. [ur(51,b,15,a(flip))]. given #402 (F,wt=21): 1179 (((c2 * (c2 * c1)) * (c1 * c2)) * (c1 * c2)) * x != (c1 * c2) * x. [ur(5,b,123,a)]. given #403 (F,wt=21): 1180 x * (((c2 * (c2 * c1)) * (c1 * c2)) * (c1 * c2)) != x * (c1 * c2). [ur(4,b,123,a)]. given #404 (T,wt=21): 1181 (((c1 * c2) * (c2 * (c2 * c1))) * (c1 * c2)) * (c1 * c2) != c1 * c2. [ur(43,b,126,a)]. given #405 (T,wt=21): 1183 (c1 * c2) * (((c1 * c2) * (c2 * (c2 * c1))) * (c1 * c2)) != c1 * c2. [ur(41,b,126,a)]. given #406 (A,wt=33): 196 (((c1 * (c1 * c2)) * x) * (((c2 * c1) * x) * y)) * (y * (((c2 * c1) * x) * y)) != ((c2 * c1) * x) * y. [ur(51,b,28,a)]. given #407 (F,wt=21): 1187 (((c1 * c2) * (c2 * (c2 * c1))) * (c1 * c2)) * x != (c1 * c2) * x. [ur(5,b,126,a)]. given #408 (F,wt=21): 1188 x * (((c1 * c2) * (c2 * (c2 * c1))) * (c1 * c2)) != x * (c1 * c2). [ur(4,b,126,a)]. given #409 (T,wt=21): 1244 ((c1 * c2) * ((c1 * c2) * (c2 * (c2 * c1)))) * (c1 * c2) != c1 * c2. [ur(43,b,128,a)]. given #410 (T,wt=21): 1245 (c1 * c2) * ((c1 * c2) * ((c1 * c2) * (c2 * (c2 * c1)))) != c1 * c2. [ur(41,b,128,a)]. given #411 (A,wt=27): 197 (((c2 * c1) * x) * y) * (((c1 * (c1 * c2)) * x) * y) != ((c1 * (c1 * c2)) * x) * y. [ur(43,b,28,a)]. given #412 (F,wt=21): 1250 ((c1 * c2) * ((c1 * c2) * (c2 * (c2 * c1)))) * x != (c1 * c2) * x. [ur(5,b,128,a)]. given #413 (F,wt=21): 1251 x * ((c1 * c2) * ((c1 * c2) * (c2 * (c2 * c1)))) != x * (c1 * c2). [ur(4,b,128,a)]. given #414 (T,wt=21): 1263 (((c1 * c2) * (c2 * (c2 * c1))) * x) * y != ((c1 * c2) * x) * y. [ur(5,b,132,a)]. given #415 (T,wt=21): 1264 x * (((c1 * c2) * (c2 * (c2 * c1))) * y) != x * ((c1 * c2) * y). [ur(4,b,132,a)]. given #416 (A,wt=25): 198 (((c1 * (c1 * c2)) * x) * y) * (((c2 * c1) * x) * y) != ((c2 * c1) * x) * y. [ur(42,b,28,a)]. given #417 (F,wt=21): 1310 (x * ((c1 * c2) * (c2 * (c2 * c1)))) * y != (x * (c1 * c2)) * y. [ur(5,b,133,a)]. given #418 (F,wt=21): 1311 x * (y * ((c1 * c2) * (c2 * (c2 * c1)))) != x * (y * (c1 * c2)). [ur(4,b,133,a)]. given #419 (T,wt=21): 1324 (c1 * ((c1 * c2) * (c2 * (c2 * c1)))) * (c2 * (c1 * c2)) != c1 * c2. [ur(51,b,133,a(flip))]. given #420 (T,wt=21): 1325 (c1 * (c1 * c2)) * (c2 * ((c1 * c2) * (c2 * (c2 * c1)))) != c1 * c2. [ur(22,b,133,a(flip))]. given #421 (A,wt=27): 199 (((c1 * (c1 * c2)) * x) * y) * (((c2 * c1) * x) * y) != ((c1 * (c1 * c2)) * x) * y. [ur(41,b,28,a)]. given #422 (F,wt=21): 1327 (((c2 * c1) * (c2 * (c1 * c2))) * (c1 * c2)) * (c1 * c2) != c1 * c2. [ur(43,b,134,a)]. given #423 (F,wt=21): 1329 (c1 * c2) * (((c2 * c1) * (c2 * (c1 * c2))) * (c1 * c2)) != c1 * c2. [ur(41,b,134,a)]. given #424 (T,wt=21): 1333 (((c2 * c1) * (c2 * (c1 * c2))) * (c1 * c2)) * x != (c1 * c2) * x. [ur(5,b,134,a)]. given #425 (T,wt=21): 1334 x * (((c2 * c1) * (c2 * (c1 * c2))) * (c1 * c2)) != x * (c1 * c2). [ur(4,b,134,a)]. given #426 (A,wt=25): 200 (((c2 * c1) * x) * y) * (((c1 * (c1 * c2)) * x) * y) != ((c2 * c1) * x) * y. [ur(40,b,28,a)]. given #427 (F,wt=21): 1394 ((c1 * c2) * ((c2 * c1) * (c2 * (c1 * c2)))) * (c1 * c2) != c1 * c2. [ur(43,b,136,a)]. given #428 (F,wt=21): 1396 (c1 * c2) * ((c1 * c2) * ((c2 * c1) * (c2 * (c1 * c2)))) != c1 * c2. [ur(41,b,136,a)]. given #429 (T,wt=21): 1400 ((c1 * c2) * ((c2 * c1) * (c2 * (c1 * c2)))) * x != (c1 * c2) * x. [ur(5,b,136,a)]. given #430 (T,wt=21): 1401 x * ((c1 * c2) * ((c2 * c1) * (c2 * (c1 * c2)))) != x * (c1 * c2). [ur(4,b,136,a)]. given #431 (A,wt=33): 201 (x * (x * ((c2 * c1) * y))) * (((c1 * (c1 * c2)) * y) * (x * ((c2 * c1) * y))) != x * ((c2 * c1) * y). [ur(22,b,28,a)]. given #432 (F,wt=21): 1413 (((c2 * c1) * (c2 * (c1 * c2))) * x) * y != ((c1 * c2) * x) * y. [ur(5,b,140,a)]. given #433 (F,wt=21): 1414 x * (((c2 * c1) * (c2 * (c1 * c2))) * y) != x * ((c1 * c2) * y). [ur(4,b,140,a)]. given #434 (T,wt=21): 1463 (x * ((c2 * c1) * (c2 * (c1 * c2)))) * y != (x * (c1 * c2)) * y. [ur(5,b,141,a)]. given #435 (T,wt=21): 1464 x * (y * ((c2 * c1) * (c2 * (c1 * c2)))) != x * (y * (c1 * c2)). [ur(4,b,141,a)]. given #436 (A,wt=33): 202 (((c2 * c1) * x) * y) * (z * (z * (((c1 * (c1 * c2)) * x) * y))) != z * (((c1 * (c1 * c2)) * x) * y). [ur(12,b,28,a)]. given #437 (F,wt=21): 1479 (c1 * ((c2 * c1) * (c2 * (c1 * c2)))) * (c2 * (c1 * c2)) != c1 * c2. [ur(51,b,141,a(flip))]. given #438 (F,wt=21): 1480 (c1 * (c1 * c2)) * (c2 * ((c2 * c1) * (c2 * (c1 * c2)))) != c1 * c2. [ur(22,b,141,a(flip))]. given #439 (T,wt=21): 1482 ((c2 * (c2 * c1)) * (c1 * (c1 * (c1 * c2)))) * (c2 * c1) != c2 * c1. [ur(43,b,145,a)]. given #440 (T,wt=21): 1484 (c2 * c1) * ((c2 * (c2 * c1)) * (c1 * (c1 * (c1 * c2)))) != c2 * c1. [ur(41,b,145,a)]. given #441 (A,wt=31): 203 (((c1 * (c1 * c2)) * x) * y) * (z * (z * (((c2 * c1) * x) * y))) != z * (((c2 * c1) * x) * y). [ur(11,b,28,a)]. given #442 (F,wt=21): 1488 ((c2 * (c2 * c1)) * (c1 * (c1 * (c1 * c2)))) * x != (c2 * c1) * x. [ur(5,b,145,a)]. given #443 (F,wt=21): 1489 x * ((c2 * (c2 * c1)) * (c1 * (c1 * (c1 * c2)))) != x * (c2 * c1). [ur(4,b,145,a)]. given #444 (T,wt=21): 1535 ((c1 * (c1 * c2)) * (c2 * (c2 * (c2 * c1)))) * (c1 * c2) != c1 * c2. [ur(43,b,147,a)]. given #445 (T,wt=21): 1537 (c1 * c2) * ((c1 * (c1 * c2)) * (c2 * (c2 * (c2 * c1)))) != c1 * c2. [ur(41,b,147,a)]. given #446 (A,wt=25): 204 x * (((c1 * (c1 * c2)) * y) * (((c2 * c1) * y) * x)) != ((c2 * c1) * y) * x. [ur(10,b,28,a)]. given #447 (F,wt=21): 1541 ((c1 * (c1 * c2)) * (c2 * (c2 * (c2 * c1)))) * x != (c1 * c2) * x. [ur(5,b,147,a)]. given #448 (F,wt=21): 1542 x * ((c1 * (c1 * c2)) * (c2 * (c2 * (c2 * c1)))) != x * (c1 * c2). [ur(4,b,147,a)]. given #449 (T,wt=21): 1543 (((c1 * c2) * (c1 * (c2 * c1))) * (c2 * c1)) * (c2 * c1) != c2 * c1. [ur(43,b,164,a)]. given #450 (T,wt=21): 1545 (c2 * c1) * (((c1 * c2) * (c1 * (c2 * c1))) * (c2 * c1)) != c2 * c1. [ur(41,b,164,a)]. given #451 (A,wt=37): 207 (((c2 * c1) * x) * (((c1 * (c1 * c2)) * x) * y)) * (y * (((c1 * (c1 * c2)) * x) * y)) != ((c1 * (c1 * c2)) * x) * y. [ur(51,b,28,a(flip))]. given #452 (F,wt=21): 1549 (((c1 * c2) * (c1 * (c2 * c1))) * (c2 * c1)) * x != (c2 * c1) * x. [ur(5,b,164,a)]. given #453 (F,wt=21): 1550 x * (((c1 * c2) * (c1 * (c2 * c1))) * (c2 * c1)) != x * (c2 * c1). [ur(4,b,164,a)]. given #454 (T,wt=21): 1597 ((c2 * c1) * ((c1 * c2) * (c1 * (c2 * c1)))) * (c2 * c1) != c2 * c1. [ur(43,b,166,a)]. given #455 (T,wt=21): 1599 (c2 * c1) * ((c2 * c1) * ((c1 * c2) * (c1 * (c2 * c1)))) != c2 * c1. [ur(41,b,166,a)]. given #456 (A,wt=37): 208 (x * (x * ((c1 * (c1 * c2)) * y))) * (((c2 * c1) * y) * (x * ((c1 * (c1 * c2)) * y))) != x * ((c1 * (c1 * c2)) * y). [ur(22,b,28,a(flip))]. given #457 (F,wt=21): 1603 ((c2 * c1) * ((c1 * c2) * (c1 * (c2 * c1)))) * x != (c2 * c1) * x. [ur(5,b,166,a)]. given #458 (F,wt=21): 1604 x * ((c2 * c1) * ((c1 * c2) * (c1 * (c2 * c1)))) != x * (c2 * c1). [ur(4,b,166,a)]. given #459 (T,wt=21): 1616 (((c1 * c2) * (c1 * (c2 * c1))) * x) * y != ((c2 * c1) * x) * y. [ur(5,b,170,a)]. given #460 (T,wt=21): 1617 x * (((c1 * c2) * (c1 * (c2 * c1))) * y) != x * ((c2 * c1) * y). [ur(4,b,170,a)]. given #461 (A,wt=27): 209 x * (((c2 * c1) * y) * (((c1 * (c1 * c2)) * y) * x)) != ((c1 * (c1 * c2)) * y) * x. [ur(10,b,28,a(flip))]. given #462 (F,wt=21): 1667 (x * ((c1 * c2) * (c1 * (c2 * c1)))) * y != (x * (c2 * c1)) * y. [ur(5,b,171,a)]. given #463 (F,wt=21): 1668 x * (y * ((c1 * c2) * (c1 * (c2 * c1)))) != x * (y * (c2 * c1)). [ur(4,b,171,a)]. given #464 (T,wt=21): 1685 (c2 * ((c1 * c2) * (c1 * (c2 * c1)))) * (c1 * (c2 * c1)) != c2 * c1. [ur(51,b,171,a(flip))]. given #465 (T,wt=21): 1686 (c2 * (c2 * c1)) * (c1 * ((c1 * c2) * (c1 * (c2 * c1)))) != c2 * c1. [ur(22,b,171,a(flip))]. given #466 (A,wt=23): 210 ((c1 * (c1 * c2)) * (x * (x * (c2 * c1)))) * y != (x * (c2 * c1)) * y. [para(6(a,1),28(a,1,1)),flip(a)]. given #467 (F,wt=21): 1688 ((c2 * (c1 * c2)) * ((c2 * c1) * (c1 * c2))) * (c1 * c2) != c1 * c2. [ur(43,b,256,a)]. given #468 (F,wt=21): 1690 (c1 * c2) * ((c2 * (c1 * c2)) * ((c2 * c1) * (c1 * c2))) != c1 * c2. [ur(41,b,256,a)]. given #469 (T,wt=21): 1694 ((c2 * (c1 * c2)) * ((c2 * c1) * (c1 * c2))) * x != (c1 * c2) * x. [ur(5,b,256,a)]. given #470 (T,wt=21): 1695 x * ((c2 * (c1 * c2)) * ((c2 * c1) * (c1 * c2))) != x * (c1 * c2). [ur(4,b,256,a)]. given #471 (A,wt=25): 211 ((c2 * c1) * (x * (x * (c1 * (c1 * c2))))) * y != (x * (c1 * (c1 * c2))) * y. [para(6(a,1),28(a,2,1))]. given #472 (F,wt=21): 1760 ((c1 * (c2 * c1)) * ((c1 * c2) * (c2 * c1))) * (c2 * c1) != c2 * c1. [ur(43,b,277,a)]. given #473 (F,wt=21): 1762 (c2 * c1) * ((c1 * (c2 * c1)) * ((c1 * c2) * (c2 * c1))) != c2 * c1. [ur(41,b,277,a)]. given #474 (T,wt=21): 1766 ((c1 * (c2 * c1)) * ((c1 * c2) * (c2 * c1))) * x != (c2 * c1) * x. [ur(5,b,277,a)]. given #475 (T,wt=21): 1767 x * ((c1 * (c2 * c1)) * ((c1 * c2) * (c2 * c1))) != x * (c2 * c1). [ur(4,b,277,a)]. given #476 (A,wt=31): 212 ((c1 * (c1 * c2)) * (x * (c2 * c1))) * ((x * (x * (c2 * c1))) * (x * (c2 * c1))) != x * (c2 * c1). [para(99(a,1),28(a,1)),flip(a)]. given #477 (F,wt=21): 1768 (c1 * (c2 * ((c1 * (c1 * c2)) * (c2 * c1)))) * (c2 * c1) != c2 * c1. [ur(43,b,808,a)]. given #478 (F,wt=21): 1770 (c2 * c1) * (c1 * (c2 * ((c1 * (c1 * c2)) * (c2 * c1)))) != c2 * c1. [ur(41,b,808,a)]. given #479 (T,wt=21): 1774 (c1 * (c2 * ((c1 * (c1 * c2)) * (c2 * c1)))) * x != (c2 * c1) * x. [ur(5,b,808,a)]. given #480 (T,wt=21): 1775 x * (c1 * (c2 * ((c1 * (c1 * c2)) * (c2 * c1)))) != x * (c2 * c1). [ur(4,b,808,a)]. given #481 (A,wt=37): 213 ((c2 * c1) * (x * (c1 * (c1 * c2)))) * ((x * (x * (c1 * (c1 * c2)))) * (x * (c1 * (c1 * c2)))) != x * (c1 * (c1 * c2)). [para(99(a,1),28(a,2))]. given #482 (F,wt=21): 1808 (c1 * (c2 * ((c2 * c1) * (c1 * (c1 * c2))))) * (c2 * c1) != c2 * c1. [ur(43,b,962,a)]. given #483 (F,wt=21): 1810 (c2 * c1) * (c1 * (c2 * ((c2 * c1) * (c1 * (c1 * c2))))) != c2 * c1. [ur(41,b,962,a)]. given #484 (T,wt=21): 1814 (c1 * (c2 * ((c2 * c1) * (c1 * (c1 * c2))))) * x != (c2 * c1) * x. [ur(5,b,962,a)]. given #485 (T,wt=21): 1815 x * (c1 * (c2 * ((c2 * c1) * (c1 * (c1 * c2))))) != x * (c2 * c1). [ur(4,b,962,a)]. given #486 (A,wt=25): 215 (c1 * (c1 * c2)) * ((c1 * c2) * (c1 * (c2 * c1))) != (c1 * c2) * (c1 * (c2 * c1)). [ur(42,b,56,a)]. given #487 (F,wt=21): 1816 (c2 * (c1 * ((c2 * (c2 * c1)) * (c1 * c2)))) * (c1 * c2) != c1 * c2. [ur(43,b,1132,a)]. given #488 (F,wt=21): 1818 (c1 * c2) * (c2 * (c1 * ((c2 * (c2 * c1)) * (c1 * c2)))) != c1 * c2. [ur(41,b,1132,a)]. given #489 (T,wt=21): 1822 (c2 * (c1 * ((c2 * (c2 * c1)) * (c1 * c2)))) * x != (c1 * c2) * x. [ur(5,b,1132,a)]. given #490 (T,wt=21): 1823 x * (c2 * (c1 * ((c2 * (c2 * c1)) * (c1 * c2)))) != x * (c1 * c2). [ur(4,b,1132,a)]. given #491 (A,wt=25): 217 ((c1 * c2) * (c1 * (c2 * c1))) * (c1 * (c1 * c2)) != (c1 * c2) * (c1 * (c2 * c1)). [ur(40,b,56,a)]. given #492 (F,wt=21): 1868 (c2 * (c1 * ((c1 * c2) * (c2 * (c2 * c1))))) * (c1 * c2) != c1 * c2. [ur(43,b,1326,a)]. given #493 (F,wt=21): 1870 (c1 * c2) * (c2 * (c1 * ((c1 * c2) * (c2 * (c2 * c1))))) != c1 * c2. [ur(41,b,1326,a)]. given #494 (T,wt=21): 1874 (c2 * (c1 * ((c1 * c2) * (c2 * (c2 * c1))))) * x != (c1 * c2) * x. [ur(5,b,1326,a)]. given #495 (T,wt=21): 1875 x * (c2 * (c1 * ((c1 * c2) * (c2 * (c2 * c1))))) != x * (c1 * c2). [ur(4,b,1326,a)]. given #496 (A,wt=27): 218 ((c1 * c2) * (c1 * (c2 * c1))) * (x * (x * (c1 * (c1 * c2)))) != x * (c1 * (c1 * c2)). [ur(12,b,56,a)]. given #497 (F,wt=21): 1876 (c2 * (c1 * ((c2 * c1) * (c2 * (c1 * c2))))) * (c1 * c2) != c1 * c2. [ur(43,b,1481,a)]. given #498 (F,wt=21): 1878 (c1 * c2) * (c2 * (c1 * ((c2 * c1) * (c2 * (c1 * c2))))) != c1 * c2. [ur(41,b,1481,a)]. given #499 (T,wt=21): 1882 (c2 * (c1 * ((c2 * c1) * (c2 * (c1 * c2))))) * x != (c1 * c2) * x. [ur(5,b,1481,a)]. NOTE: Back_subsumption disabled, ratio of kept to back_subsumed is 103 (0.00 of 9.29 sec). given #500 (T,wt=21): 1883 x * (c2 * (c1 * ((c2 * c1) * (c2 * (c1 * c2))))) != x * (c1 * c2). [ur(4,b,1481,a)]. given #501 (A,wt=31): 219 (c1 * (c1 * c2)) * (x * (x * ((c1 * c2) * (c1 * (c2 * c1))))) != x * ((c1 * c2) * (c1 * (c2 * c1))). [ur(11,b,56,a)]. given #502 (F,wt=21): 1945 (c1 * (c2 * ((c1 * c2) * (c1 * (c2 * c1))))) * (c2 * c1) != c2 * c1. [ur(43,b,1687,a)]. given #503 (F,wt=21): 1947 (c2 * c1) * (c1 * (c2 * ((c1 * c2) * (c1 * (c2 * c1))))) != c2 * c1. [ur(41,b,1687,a)]. given #504 (T,wt=21): 1951 (c1 * (c2 * ((c1 * c2) * (c1 * (c2 * c1))))) * x != (c2 * c1) * x. [ur(5,b,1687,a)]. given #505 (T,wt=21): 1952 x * (c1 * (c2 * ((c1 * c2) * (c1 * (c2 * c1))))) != x * (c2 * c1). [ur(4,b,1687,a)]. given #506 (A,wt=25): 226 ((c1 * (c1 * c2)) * (c2 * c1)) * (c1 * (c1 * c2)) != (c1 * (c1 * c2)) * (c2 * c1). [ur(40,b,65,a)]. given #507 (F,wt=21): 2189 (c1 * c2) * (c1 * ((c2 * c1) * (c1 * (c1 * c2)))) != c1 * (c1 * c2). [ur(10,b,177,a(flip))]. given #508 (F,wt=21): 2302 (c1 * c2) * (c1 * ((c1 * c2) * (c1 * (c2 * c1)))) != c1 * (c1 * c2). [ur(10,b,221,a(flip))]. given #509 (T,wt=21): 2442 (c1 * c2) * (c1 * ((c1 * (c1 * c2)) * (c2 * c1))) != c1 * (c1 * c2). [ur(10,b,230,a(flip))]. given #510 (T,wt=21): 2608 (c2 * c1) * (c2 * ((c1 * c2) * (c2 * (c2 * c1)))) != c2 * (c2 * c1). [ur(10,b,262,a(flip))]. given #511 (A,wt=27): 227 ((c1 * (c1 * c2)) * (c2 * c1)) * (x * (x * (c1 * (c1 * c2)))) != x * (c1 * (c1 * c2)). [ur(12,b,65,a)]. given #512 (F,wt=21): 2711 (c2 * c1) * (c2 * ((c2 * (c2 * c1)) * (c1 * c2))) != c2 * (c2 * c1). [ur(10,b,271,a(flip))]. given #513 (F,wt=21): 2847 (c2 * c1) * (c2 * ((c2 * c1) * (c2 * (c1 * c2)))) != c2 * (c2 * c1). [ur(10,b,318,a(flip))]. given #514 (T,wt=21): 3416 c1 * ((c2 * (c2 * (c2 * c1))) * ((c2 * c1) * (c1 * c2))) != c2 * c1. [ur(10,b,143,a(flip))]. given #515 (T,wt=21): 3718 c2 * ((c1 * (c1 * (c1 * c2))) * ((c1 * c2) * (c2 * c1))) != c1 * c2. [ur(10,b,149,a(flip))]. given #516 (A,wt=31): 228 (c1 * (c1 * c2)) * (x * (x * ((c1 * (c1 * c2)) * (c2 * c1)))) != x * ((c1 * (c1 * c2)) * (c2 * c1)). [ur(11,b,65,a)]. given #517 (F,wt=21): 3999 c2 * (((c2 * c1) * (c1 * (c1 * c2))) * (c1 * (c1 * c2))) != c1 * c2. [ur(10,b,172,a(flip))]. given #518 (F,wt=21): 4008 c2 * ((c1 * (c1 * c2)) * ((c2 * c1) * (c1 * (c1 * c2)))) != c1 * c2. [ur(10,b,173,a(flip))]. given #519 (T,wt=21): 4018 c1 * ((c2 * (c1 * c2)) * ((c2 * c1) * (c2 * (c2 * c1)))) != c2 * c1. [ur(10,b,180,a(flip))]. given #520 (T,wt=21): 4028 c2 * ((c1 * (c2 * c1)) * ((c1 * c2) * (c1 * (c1 * c2)))) != c1 * c2. [ur(10,b,186,a(flip))]. given #521 (A,wt=33): 236 ((c2 * c1) * x) * (((c1 * (c1 * c2)) * x) * ((c2 * c1) * x)) != ((c1 * (c1 * c2)) * x) * ((c2 * c1) * x). [ur(106,b,28,a)]. given #522 (F,wt=21): 4147 c2 * (((c1 * c2) * (c1 * (c2 * c1))) * (c1 * (c1 * c2))) != c1 * c2. [ur(10,b,214,a(flip))]. given #523 (F,wt=21): 4156 c2 * ((c1 * (c1 * c2)) * ((c1 * c2) * (c1 * (c2 * c1)))) != c1 * c2. [ur(10,b,216,a(flip))]. given #524 (T,wt=21): 4176 c2 * (((c1 * (c1 * c2)) * (c2 * c1)) * (c1 * (c1 * c2))) != c1 * c2. [ur(10,b,224,a(flip))]. given #525 (T,wt=21): 4185 c2 * ((c1 * (c1 * c2)) * ((c1 * (c1 * c2)) * (c2 * c1))) != c1 * c2. [ur(10,b,225,a(flip))]. given #526 (A,wt=25): 237 (c2 * (c2 * c1)) * ((c1 * c2) * (c2 * (c2 * c1))) != (c1 * c2) * (c2 * (c2 * c1)). [ur(106,b,25,a)]. given #527 (F,wt=21): 4324 c1 * (((c1 * c2) * (c2 * (c2 * c1))) * (c2 * (c2 * c1))) != c2 * c1. [ur(10,b,257,a(flip))]. given #528 (F,wt=21): 4333 c1 * ((c2 * (c2 * c1)) * ((c1 * c2) * (c2 * (c2 * c1)))) != c2 * c1. [ur(10,b,258,a(flip))]. given #529 (T,wt=21): 4342 c1 * (((c2 * (c2 * c1)) * (c1 * c2)) * (c2 * (c2 * c1))) != c2 * c1. [ur(10,b,265,a(flip))]. given #530 (T,wt=21): 4376 c1 * ((c2 * (c2 * c1)) * ((c2 * (c2 * c1)) * (c1 * c2))) != c2 * c1. [ur(10,b,266,a(flip))]. given #531 (A,wt=35): 238 ((c1 * (c1 * c2)) * x) * (((c2 * c1) * x) * ((c1 * (c1 * c2)) * x)) != ((c2 * c1) * x) * ((c1 * (c1 * c2)) * x). [ur(106,b,28,a(flip))]. given #532 (F,wt=21): 4432 c1 * (((c2 * c1) * (c2 * (c1 * c2))) * (c2 * (c2 * c1))) != c2 * c1. [ur(10,b,311,a(flip))]. given #533 (F,wt=21): 4441 c1 * ((c2 * (c2 * c1)) * ((c2 * c1) * (c2 * (c1 * c2)))) != c2 * c1. [ur(10,b,313,a(flip))]. given #534 (T,wt=21): 5855 c1 * (c2 * ((c2 * c1) * ((c1 * (c1 * c2)) * (c2 * c1)))) != c2 * c1. [ur(10,b,815,a(flip))]. given #535 (T,wt=21): 5957 c1 * (c2 * (((c1 * (c1 * c2)) * (c2 * c1)) * (c2 * c1))) != c2 * c1. [ur(10,b,883,a(flip))]. given #536 (A,wt=25): 240 ((c2 * c1) * ((c1 * (c1 * c2)) * x)) * (x * ((c2 * c1) * x)) != (c2 * c1) * x. [ur(51,b,29,a)]. given #537 (F,wt=21): 6066 c1 * (c2 * ((c2 * c1) * ((c2 * c1) * (c1 * (c1 * c2))))) != c2 * c1. [ur(10,b,892,a(flip))]. given #538 (F,wt=21): 6357 c1 * (c2 * (((c2 * c1) * (c1 * (c1 * c2))) * (c2 * c1))) != c2 * c1. [ur(10,b,1034,a(flip))]. given #539 (T,wt=21): 6447 c2 * (c1 * ((c1 * c2) * ((c2 * (c2 * c1)) * (c1 * c2)))) != c1 * c2. [ur(10,b,1043,a(flip))]. given #540 (T,wt=21): 6738 c2 * (c1 * (((c2 * (c2 * c1)) * (c1 * c2)) * (c1 * c2))) != c1 * c2. [ur(10,b,1180,a(flip))]. given #541 (A,wt=27): 241 (x * ((c2 * c1) * y)) * (x * ((c1 * (c1 * c2)) * y)) != x * ((c1 * (c1 * c2)) * y). [ur(43,b,29,a)]. given #542 (F,wt=21): 6833 c2 * (c1 * (((c1 * c2) * (c2 * (c2 * c1))) * (c1 * c2))) != c1 * c2. [ur(10,b,1188,a(flip))]. given #543 (F,wt=21): 6929 c2 * (c1 * ((c1 * c2) * ((c1 * c2) * (c2 * (c2 * c1))))) != c1 * c2. [ur(10,b,1251,a(flip))]. given #544 (T,wt=21): 7204 c2 * (c1 * (((c2 * c1) * (c2 * (c1 * c2))) * (c1 * c2))) != c1 * c2. [ur(10,b,1334,a(flip))]. given #545 (T,wt=21): 7293 c2 * (c1 * ((c1 * c2) * ((c2 * c1) * (c2 * (c1 * c2))))) != c1 * c2. [ur(10,b,1401,a(flip))]. given #546 (A,wt=25): 242 (x * ((c1 * (c1 * c2)) * y)) * (x * ((c2 * c1) * y)) != x * ((c2 * c1) * y). [ur(42,b,29,a)]. given #547 (F,wt=21): 7573 c1 * (c2 * ((c2 * (c2 * c1)) * (c1 * (c1 * (c1 * c2))))) != c2 * c1. [ur(10,b,1489,a(flip))]. given #548 (F,wt=21): 7660 c2 * (c1 * ((c1 * (c1 * c2)) * (c2 * (c2 * (c2 * c1))))) != c1 * c2. [ur(10,b,1542,a(flip))]. given #549 (T,wt=21): 7739 c1 * (c2 * (((c1 * c2) * (c1 * (c2 * c1))) * (c2 * c1))) != c2 * c1. [ur(10,b,1550,a(flip))]. given #550 (T,wt=21): 7819 c1 * (c2 * ((c2 * c1) * ((c1 * c2) * (c1 * (c2 * c1))))) != c2 * c1. [ur(10,b,1604,a(flip))]. given #551 (A,wt=27): 243 (x * ((c1 * (c1 * c2)) * y)) * (x * ((c2 * c1) * y)) != x * ((c1 * (c1 * c2)) * y). [ur(41,b,29,a)]. given #552 (F,wt=21): 8060 c2 * (c1 * ((c2 * (c1 * c2)) * ((c2 * c1) * (c1 * c2)))) != c1 * c2. [ur(10,b,1695,a(flip))]. given #553 (F,wt=21): 8138 c1 * (c2 * ((c1 * (c2 * c1)) * ((c1 * c2) * (c2 * c1)))) != c2 * c1. [ur(10,b,1767,a(flip))]. given #554 (T,wt=21): 8210 c1 * (c2 * (c1 * (c2 * ((c1 * (c1 * c2)) * (c2 * c1))))) != c2 * c1. [ur(10,b,1775,a(flip))]. given #555 (T,wt=21): 8278 c1 * (c2 * (c1 * (c2 * ((c2 * c1) * (c1 * (c1 * c2)))))) != c2 * c1. [ur(10,b,1815,a(flip))]. given #556 (A,wt=25): 244 (x * ((c2 * c1) * y)) * (x * ((c1 * (c1 * c2)) * y)) != x * ((c2 * c1) * y). [ur(40,b,29,a)]. given #557 (F,wt=21): 8346 c2 * (c1 * (c2 * (c1 * ((c2 * (c2 * c1)) * (c1 * c2))))) != c1 * c2. [ur(10,b,1823,a(flip))]. given #558 (F,wt=21): 8415 c2 * (c1 * (c2 * (c1 * ((c1 * c2) * (c2 * (c2 * c1)))))) != c1 * c2. [ur(10,b,1875,a(flip))]. given #559 (T,wt=21): 8490 c2 * (c1 * (c2 * (c1 * ((c2 * c1) * (c2 * (c1 * c2)))))) != c1 * c2. [ur(10,b,1883,a(flip))]. given #560 (T,wt=21): 8561 c1 * (c2 * (c1 * (c2 * ((c1 * c2) * (c1 * (c2 * c1)))))) != c2 * c1. [ur(10,b,1952,a(flip))]. given #561 (A,wt=25): 245 ((c2 * c1) * ((c2 * c1) * x)) * (x * ((c1 * (c1 * c2)) * x)) != (c2 * c1) * x. [ur(22,b,29,a)]. given #562 (F,wt=21): 8578 c2 * ((c1 * c2) * (c1 * ((c2 * c1) * (c1 * (c1 * c2))))) != c1 * c2. [ur(10,b,2189,a(flip))]. given #563 (F,wt=21): 8588 c2 * ((c1 * c2) * (c1 * ((c1 * c2) * (c1 * (c2 * c1))))) != c1 * c2. [ur(10,b,2302,a(flip))]. given #564 (T,wt=21): 8598 c2 * ((c1 * c2) * (c1 * ((c1 * (c1 * c2)) * (c2 * c1)))) != c1 * c2. [ur(10,b,2442,a(flip))]. given #565 (T,wt=21): 8608 c1 * ((c2 * c1) * (c2 * ((c1 * c2) * (c2 * (c2 * c1))))) != c2 * c1. [ur(10,b,2608,a(flip))]. given #566 (A,wt=33): 246 (x * ((c2 * c1) * y)) * (z * (z * (x * ((c1 * (c1 * c2)) * y)))) != z * (x * ((c1 * (c1 * c2)) * y)). [ur(12,b,29,a)]. given #567 (F,wt=21): 8632 c1 * ((c2 * c1) * (c2 * ((c2 * (c2 * c1)) * (c1 * c2)))) != c2 * c1. [ur(10,b,2711,a(flip))]. given #568 (F,wt=21): 8642 c1 * ((c2 * c1) * (c2 * ((c2 * c1) * (c2 * (c1 * c2))))) != c2 * c1. [ur(10,b,2847,a(flip))]. given #569 (T,wt=23): 254 x * ((c1 * (c1 * c2)) * (y * (y * (c2 * c1)))) != x * (y * (c2 * c1)). [para(6(a,1),29(a,1,2)),flip(a)]. given #570 (T,wt=23): 348 ((c1 * (c1 * c2)) * (c2 * (c2 * (c2 * c1)))) * (c1 * (c2 * c1)) != c2 * c1. [ur(51,b,31,a(flip))]. given #571 (A,wt=31): 247 (x * ((c1 * (c1 * c2)) * y)) * (z * (z * (x * ((c2 * c1) * y)))) != z * (x * ((c2 * c1) * y)). [ur(11,b,29,a)]. given #572 (F,wt=23): 349 (c2 * (c2 * c1)) * ((c1 * (c1 * c2)) * (c1 * (c1 * (c2 * c1)))) != c2 * c1. [ur(22,b,31,a(flip))]. given #573 (F,wt=23): 391 (c1 * c2) * ((c2 * c1) * (c1 * (c1 * (c1 * (c1 * c2))))) != c1 * (c1 * c2). [ur(10,b,32,a(flip))]. given #574 (T,wt=23): 444 (c2 * c1) * ((c1 * c2) * (c2 * (c2 * (c2 * (c2 * c1))))) != c2 * (c2 * c1). [ur(10,b,47,a(flip))]. given #575 (T,wt=23): 548 ((c2 * (c2 * c1)) * (x * (x * (c1 * c2)))) * y != (x * (c1 * c2)) * y. [para(6(a,1),59(a,2,1))]. given #576 (A,wt=29): 251 ((c1 * (c1 * c2)) * ((c2 * c1) * x)) * (x * ((c1 * (c1 * c2)) * x)) != (c1 * (c1 * c2)) * x. [ur(51,b,29,a(flip))]. given #577 (F,wt=23): 589 x * ((c2 * (c2 * c1)) * (y * (y * (c1 * c2)))) != x * (y * (c1 * c2)). [ur(4,b,49,a)]. given #578 (F,wt=23): 596 ((c2 * (c2 * c1)) * (c1 * (c1 * (c1 * c2)))) * (c2 * (c1 * c2)) != c1 * c2. [ur(51,b,49,a(flip))]. given #579 (T,wt=23): 597 (c1 * (c1 * c2)) * ((c2 * (c2 * c1)) * (c2 * (c2 * (c1 * c2)))) != c1 * c2. [ur(22,b,49,a(flip))]. given #580 (T,wt=23): 721 (((c1 * (c1 * c2)) * (c2 * c1)) * x) * ((c2 * c1) * x) != (c2 * c1) * x. [ur(43,b,86,a)]. given #581 (A,wt=29): 252 ((c1 * (c1 * c2)) * ((c1 * (c1 * c2)) * x)) * (x * ((c2 * c1) * x)) != (c1 * (c1 * c2)) * x. [ur(22,b,29,a(flip))]. given #582 (F,wt=23): 723 ((c2 * c1) * x) * (((c1 * (c1 * c2)) * (c2 * c1)) * x) != (c2 * c1) * x. [ur(41,b,86,a)]. given #583 (F,wt=23): 736 x * (((c1 * (c1 * c2)) * (c2 * c1)) * ((c2 * c1) * x)) != (c2 * c1) * x. [ur(10,b,86,a(flip))]. given #584 (T,wt=23): 790 (x * ((c1 * (c1 * c2)) * (c2 * c1))) * (x * (c2 * c1)) != x * (c2 * c1). [ur(43,b,87,a)]. given #585 (T,wt=23): 792 (x * (c2 * c1)) * (x * ((c1 * (c1 * c2)) * (c2 * c1))) != x * (c2 * c1). [ur(41,b,87,a)]. given #586 (A,wt=25): 255 x * ((c2 * c1) * (y * (y * (c1 * (c1 * c2))))) != x * (y * (c1 * (c1 * c2))). [para(6(a,1),29(a,2,2))]. given #587 (F,wt=23): 919 (((c2 * c1) * (c1 * (c1 * c2))) * x) * ((c2 * c1) * x) != (c2 * c1) * x. [ur(43,b,113,a)]. given #588 (F,wt=23): 921 ((c2 * c1) * x) * (((c2 * c1) * (c1 * (c1 * c2))) * x) != (c2 * c1) * x. [ur(41,b,113,a)]. given #589 (T,wt=23): 934 x * (((c2 * c1) * (c1 * (c1 * c2))) * ((c2 * c1) * x)) != (c2 * c1) * x. [ur(10,b,113,a(flip))]. given #590 (T,wt=23): 943 (x * ((c2 * c1) * (c1 * (c1 * c2)))) * (x * (c2 * c1)) != x * (c2 * c1). [ur(43,b,114,a)]. given #591 (A,wt=27): 259 ((c1 * c2) * (c2 * (c2 * c1))) * (x * (x * (c2 * (c2 * c1)))) != x * (c2 * (c2 * c1)). [ur(12,b,66,a)]. given #592 (F,wt=23): 945 (x * (c2 * c1)) * (x * ((c2 * c1) * (c1 * (c1 * c2)))) != x * (c2 * c1). [ur(41,b,114,a)]. given #593 (F,wt=23): 1086 (((c2 * (c2 * c1)) * (c1 * c2)) * x) * ((c1 * c2) * x) != (c1 * c2) * x. [ur(43,b,121,a)]. given #594 (T,wt=23): 1088 ((c1 * c2) * x) * (((c2 * (c2 * c1)) * (c1 * c2)) * x) != (c1 * c2) * x. [ur(41,b,121,a)]. given #595 (T,wt=23): 1101 x * (((c2 * (c2 * c1)) * (c1 * c2)) * ((c1 * c2) * x)) != (c1 * c2) * x. [ur(10,b,121,a(flip))]. given #596 (A,wt=31): 260 (c2 * (c2 * c1)) * (x * (x * ((c1 * c2) * (c2 * (c2 * c1))))) != x * ((c1 * c2) * (c2 * (c2 * c1))). [ur(11,b,66,a)]. given #597 (F,wt=23): 1112 (x * ((c2 * (c2 * c1)) * (c1 * c2))) * (x * (c1 * c2)) != x * (c1 * c2). [ur(43,b,122,a)]. given #598 (F,wt=23): 1114 (x * (c1 * c2)) * (x * ((c2 * (c2 * c1)) * (c1 * c2))) != x * (c1 * c2). [ur(41,b,122,a)]. given #599 (T,wt=23): 1168 (x * ((c2 * (c2 * c1)) * ((c1 * c2) * x))) * y != ((c1 * c2) * x) * y. [ur(5,b,62,a)]. given #600 (T,wt=23): 1169 x * (y * ((c2 * (c2 * c1)) * ((c1 * c2) * y))) != x * ((c1 * c2) * y). [ur(4,b,62,a)]. given #601 (A,wt=25): 267 ((c2 * (c2 * c1)) * (c1 * c2)) * (c2 * (c2 * c1)) != (c2 * (c2 * c1)) * (c1 * c2). [ur(40,b,69,a)]. given #602 (F,wt=23): 1255 (((c1 * c2) * (c2 * (c2 * c1))) * x) * ((c1 * c2) * x) != (c1 * c2) * x. [ur(43,b,132,a)]. given #603 (F,wt=23): 1257 ((c1 * c2) * x) * (((c1 * c2) * (c2 * (c2 * c1))) * x) != (c1 * c2) * x. [ur(41,b,132,a)]. given #604 (T,wt=23): 1268 x * (((c1 * c2) * (c2 * (c2 * c1))) * ((c1 * c2) * x)) != (c1 * c2) * x. [ur(10,b,132,a(flip))]. given #605 (T,wt=23): 1276 ((x * (c2 * c1)) * (x * (c1 * (c1 * c2)))) * y != (x * (c2 * c1)) * y. [ur(5,b,70,a)]. given #606 (A,wt=27): 268 ((c2 * (c2 * c1)) * (c1 * c2)) * (x * (x * (c2 * (c2 * c1)))) != x * (c2 * (c2 * c1)). [ur(12,b,69,a)]. given #607 (F,wt=23): 1277 x * ((y * (c2 * c1)) * (y * (c1 * (c1 * c2)))) != x * (y * (c2 * c1)). [ur(4,b,70,a)]. given #608 (F,wt=23): 1290 (c2 * (c2 * c1)) * ((c1 * (c2 * c1)) * (c1 * (c1 * (c1 * c2)))) != c2 * c1. [ur(22,b,70,a(flip))]. given #609 (T,wt=23): 1303 (x * ((c1 * c2) * (c2 * (c2 * c1)))) * (x * (c1 * c2)) != x * (c1 * c2). [ur(43,b,133,a)]. given #610 (T,wt=23): 1305 (x * (c1 * c2)) * (x * ((c1 * c2) * (c2 * (c2 * c1)))) != x * (c1 * c2). [ur(41,b,133,a)]. given #611 (A,wt=31): 269 (c2 * (c2 * c1)) * (x * (x * ((c2 * (c2 * c1)) * (c1 * c2)))) != x * ((c2 * (c2 * c1)) * (c1 * c2)). [ur(11,b,69,a)]. given #612 (F,wt=23): 1388 (((c2 * c1) * x) * ((c1 * (c1 * c2)) * x)) * y != ((c2 * c1) * x) * y. [ur(5,b,71,a)]. given #613 (F,wt=23): 1389 x * (((c2 * c1) * y) * ((c1 * (c1 * c2)) * y)) != x * ((c2 * c1) * y). [ur(4,b,71,a)]. given #614 (T,wt=23): 1405 (((c2 * c1) * (c2 * (c1 * c2))) * x) * ((c1 * c2) * x) != (c1 * c2) * x. [ur(43,b,140,a)]. given #615 (T,wt=23): 1407 ((c1 * c2) * x) * (((c2 * c1) * (c2 * (c1 * c2))) * x) != (c1 * c2) * x. [ur(41,b,140,a)]. given #616 (A,wt=31): 274 (x * ((c2 * c1) * x)) * (((c2 * c1) * ((c2 * c1) * x)) * ((c1 * (c1 * c2)) * x)) != (c2 * c1) * x. [ur(101,b,29,a)]. given #617 (F,wt=23): 1418 x * (((c2 * c1) * (c2 * (c1 * c2))) * ((c1 * c2) * x)) != (c1 * c2) * x. [ur(10,b,140,a(flip))]. given #618 (F,wt=23): 1436 (((c1 * c2) * x) * ((c2 * (c2 * c1)) * x)) * y != ((c1 * c2) * x) * y. [ur(5,b,72,a)]. given #619 (T,wt=23): 1437 x * (((c1 * c2) * y) * ((c2 * (c2 * c1)) * y)) != x * ((c1 * c2) * y). [ur(4,b,72,a)]. given #620 (T,wt=23): 1455 (x * ((c2 * c1) * (c2 * (c1 * c2)))) * (x * (c1 * c2)) != x * (c1 * c2). [ur(43,b,141,a)]. given #621 (A,wt=31): 275 (x * ((c2 * c1) * x)) * (((c1 * (c1 * c2)) * ((c2 * c1) * x)) * ((c2 * c1) * x)) != (c2 * c1) * x. [ur(101,b,28,a)]. given #622 (F,wt=23): 1457 (x * (c1 * c2)) * (x * ((c2 * c1) * (c2 * (c1 * c2)))) != x * (c1 * c2). [ur(41,b,141,a)]. given #623 (F,wt=23): 1462 (c2 * (c1 * c2)) * ((c2 * c1) * (c1 * c2)) != (c2 * c1) * (c2 * (c1 * c2)). [ur(10,b,141,a)]. given #624 (T,wt=23): 1534 (c1 * c2) * ((c1 * (c1 * (c1 * c2))) * (c1 * (c2 * c1))) != c1 * (c1 * c2). [ur(10,b,74,a(flip))]. given #625 (T,wt=23): 1608 (((c1 * c2) * (c1 * (c2 * c1))) * x) * ((c2 * c1) * x) != (c2 * c1) * x. [ur(43,b,170,a)]. given #626 (A,wt=27): 276 ((c2 * c1) * (c2 * (c2 * c1))) * ((c2 * (c2 * (c2 * c1))) * (c1 * c2)) != c2 * (c2 * c1). [ur(101,b,26,a)]. given #627 (F,wt=23): 1610 ((c2 * c1) * x) * (((c1 * c2) * (c1 * (c2 * c1))) * x) != (c2 * c1) * x. [ur(41,b,170,a)]. given #628 (F,wt=23): 1621 x * (((c1 * c2) * (c1 * (c2 * c1))) * ((c2 * c1) * x)) != (c2 * c1) * x. [ur(10,b,170,a(flip))]. given #629 (T,wt=23): 1645 (c2 * c1) * ((c2 * (c2 * (c2 * c1))) * (c2 * (c1 * c2))) != c2 * (c2 * c1). [ur(10,b,76,a(flip))]. given #630 (T,wt=23): 1659 (x * ((c1 * c2) * (c1 * (c2 * c1)))) * (x * (c2 * c1)) != x * (c2 * c1). [ur(43,b,171,a)]. given #631 (A,wt=37): 279 (x * ((c1 * (c1 * c2)) * x)) * (((c1 * (c1 * c2)) * ((c1 * (c1 * c2)) * x)) * ((c2 * c1) * x)) != (c1 * (c1 * c2)) * x. [ur(101,b,29,a(flip))]. given #632 (F,wt=23): 1661 (x * (c2 * c1)) * (x * ((c1 * c2) * (c1 * (c2 * c1)))) != x * (c2 * c1). [ur(41,b,171,a)]. given #633 (F,wt=23): 1666 (c1 * (c2 * c1)) * ((c1 * c2) * (c2 * c1)) != (c1 * c2) * (c1 * (c2 * c1)). [ur(10,b,171,a)]. given #634 (T,wt=23): 1846 ((x * (c1 * c2)) * (x * (c2 * (c2 * c1)))) * y != (x * (c1 * c2)) * y. [ur(5,b,82,a)]. given #635 (T,wt=23): 1847 x * ((y * (c1 * c2)) * (y * (c2 * (c2 * c1)))) != x * (y * (c1 * c2)). [ur(4,b,82,a)]. given #636 (A,wt=37): 280 (x * ((c1 * (c1 * c2)) * x)) * (((c2 * c1) * ((c1 * (c1 * c2)) * x)) * ((c1 * (c1 * c2)) * x)) != (c1 * (c1 * c2)) * x. [ur(101,b,28,a(flip))]. given #637 (F,wt=23): 1867 (c1 * (c1 * c2)) * ((c2 * (c1 * c2)) * (c2 * (c2 * (c2 * c1)))) != c1 * c2. [ur(22,b,82,a(flip))]. given #638 (F,wt=23): 1944 c1 * (((c1 * (c1 * c2)) * (c2 * c1)) * (c2 * (c2 * (c2 * c1)))) != c2 * c1. [ur(10,b,84,a(flip))]. given #639 (T,wt=23): 1957 ((x * (c1 * (c1 * c2))) * (x * (c2 * c1))) * y != (x * (c2 * c1)) * y. [ur(5,b,92,a)]. given #640 (T,wt=23): 1958 x * ((y * (c1 * (c1 * c2))) * (y * (c2 * c1))) != x * (y * (c2 * c1)). [ur(4,b,92,a)]. given #641 (A,wt=27): 282 ((c1 * c2) * (c1 * (c1 * c2))) * ((c1 * (c1 * (c1 * c2))) * (c2 * c1)) != c1 * (c1 * c2). [ur(101,b,16,a(flip))]. given #642 (F,wt=23): 1979 (c2 * (c2 * c1)) * ((c1 * (c1 * (c1 * c2))) * (c1 * (c2 * c1))) != c2 * c1. [ur(22,b,92,a(flip))]. given #643 (F,wt=23): 2003 (((c1 * (c1 * c2)) * x) * ((c2 * c1) * x)) * y != ((c2 * c1) * x) * y. [ur(5,b,93,a)]. given #644 (T,wt=23): 2004 x * (((c1 * (c1 * c2)) * y) * ((c2 * c1) * y)) != x * ((c2 * c1) * y). [ur(4,b,93,a)]. given #645 (T,wt=23): 2013 ((x * (c2 * (c2 * c1))) * (x * (c1 * c2))) * y != (x * (c1 * c2)) * y. [ur(5,b,95,a)]. given #646 (A,wt=31): 284 (x * ((c1 * (c1 * c2)) * x)) * (((c2 * c1) * ((c2 * c1) * x)) * ((c2 * c1) * x)) != (c2 * c1) * x. [ur(103,b,29,a)]. given #647 (F,wt=23): 2014 x * ((y * (c2 * (c2 * c1))) * (y * (c1 * c2))) != x * (y * (c1 * c2)). [ur(4,b,95,a)]. given #648 (F,wt=23): 2035 (c1 * (c1 * c2)) * ((c2 * (c2 * (c2 * c1))) * (c2 * (c1 * c2))) != c1 * c2. [ur(22,b,95,a(flip))]. given #649 (T,wt=23): 2087 (((c2 * (c2 * c1)) * x) * ((c1 * c2) * x)) * y != ((c1 * c2) * x) * y. [ur(5,b,96,a)]. given #650 (T,wt=23): 2088 x * (((c2 * (c2 * c1)) * y) * ((c1 * c2) * y)) != x * ((c1 * c2) * y). [ur(4,b,96,a)]. given #651 (A,wt=41): 285 (((c1 * (c1 * c2)) * x) * (y * ((c2 * c1) * x))) * ((y * (y * ((c2 * c1) * x))) * (y * ((c2 * c1) * x))) != y * ((c2 * c1) * x). [ur(103,b,28,a)]. given #652 (F,wt=23): 2104 (((c2 * c1) * (c1 * (c1 * c2))) * x) * y != ((c1 * (c1 * c2)) * x) * y. [ur(5,b,176,a)]. given #653 (F,wt=23): 2105 x * (((c2 * c1) * (c1 * (c1 * c2))) * y) != x * ((c1 * (c1 * c2)) * y). [ur(4,b,176,a)]. given #654 (T,wt=23): 2109 (c2 * (c1 * c2)) * (((c2 * c1) * (c1 * (c1 * c2))) * (c1 * c2)) != c1 * c2. [ur(101,b,176,a(flip))]. given #655 (T,wt=23): 2143 (c2 * c1) * ((c2 * (c1 * c2)) * (c2 * (c2 * (c2 * c1)))) != c2 * (c2 * c1). [ur(10,b,90,a(flip))]. given #656 (A,wt=27): 286 ((c2 * c1) * (c1 * c2)) * ((c2 * (c2 * (c2 * c1))) * (c2 * (c2 * c1))) != c2 * (c2 * c1). [ur(103,b,26,a)]. given #657 (F,wt=23): 2163 (x * ((c2 * c1) * (c1 * (c1 * c2)))) * y != (x * (c1 * (c1 * c2))) * y. [ur(5,b,177,a)]. given #658 (F,wt=23): 2164 x * (y * ((c2 * c1) * (c1 * (c1 * c2)))) != x * (y * (c1 * (c1 * c2))). [ur(4,b,177,a)]. given #659 (T,wt=23): 2190 (((c2 * c1) * (c1 * (c1 * c2))) * (c2 * (c1 * c2))) * (c1 * c2) != c1 * c2. [ur(43,b,183,a)]. given #660 (T,wt=23): 2192 (c1 * c2) * (((c2 * c1) * (c1 * (c1 * c2))) * (c2 * (c1 * c2))) != c1 * c2. [ur(41,b,183,a)]. given #661 (A,wt=37): 287 ((c1 * c2) * (x * (c2 * (c2 * c1)))) * ((x * (x * (c2 * (c2 * c1)))) * (x * (c2 * (c2 * c1)))) != x * (c2 * (c2 * c1)). [ur(103,b,25,a)]. given #662 (F,wt=23): 2196 (((c2 * c1) * (c1 * (c1 * c2))) * (c2 * (c1 * c2))) * x != (c1 * c2) * x. [ur(5,b,183,a)]. given #663 (F,wt=23): 2197 x * (((c2 * c1) * (c1 * (c1 * c2))) * (c2 * (c1 * c2))) != x * (c1 * c2). [ur(4,b,183,a)]. given #664 (T,wt=23): 2244 (((c1 * c2) * (c1 * (c2 * c1))) * x) * y != ((c1 * (c1 * c2)) * x) * y. [ur(5,b,220,a)]. given #665 (T,wt=23): 2245 x * (((c1 * c2) * (c1 * (c2 * c1))) * y) != x * ((c1 * (c1 * c2)) * y). [ur(4,b,220,a)]. given #666 (A,wt=37): 289 (x * ((c2 * c1) * x)) * (((c1 * (c1 * c2)) * ((c1 * (c1 * c2)) * x)) * ((c1 * (c1 * c2)) * x)) != (c1 * (c1 * c2)) * x. [ur(103,b,29,a(flip))]. given #667 (F,wt=23): 2250 (c2 * (c1 * c2)) * (((c1 * c2) * (c1 * (c2 * c1))) * (c1 * c2)) != c1 * c2. [ur(101,b,220,a(flip))]. given #668 (F,wt=23): 2275 (x * ((c1 * c2) * (c1 * (c2 * c1)))) * y != (x * (c1 * (c1 * c2))) * y. [ur(5,b,221,a)]. given #669 (T,wt=23): 2276 x * (y * ((c1 * c2) * (c1 * (c2 * c1)))) != x * (y * (c1 * (c1 * c2))). [ur(4,b,221,a)]. given #670 (T,wt=23): 2354 (c1 * c2) * ((c1 * (c2 * c1)) * (c1 * (c1 * (c1 * c2)))) != c1 * (c1 * c2). [ur(10,b,97,a(flip))]. given #671 (A,wt=47): 290 (((c2 * c1) * x) * (y * ((c1 * (c1 * c2)) * x))) * ((y * (y * ((c1 * (c1 * c2)) * x))) * (y * ((c1 * (c1 * c2)) * x))) != y * ((c1 * (c1 * c2)) * x). [ur(103,b,28,a(flip))]. given #672 (F,wt=23): 2355 (((c1 * c2) * (c1 * (c2 * c1))) * (c2 * (c1 * c2))) * (c1 * c2) != c1 * c2. [ur(43,b,222,a)]. given #673 (F,wt=23): 2357 (c1 * c2) * (((c1 * c2) * (c1 * (c2 * c1))) * (c2 * (c1 * c2))) != c1 * c2. [ur(41,b,222,a)]. given #674 (T,wt=23): 2361 (((c1 * c2) * (c1 * (c2 * c1))) * (c2 * (c1 * c2))) * x != (c1 * c2) * x. [ur(5,b,222,a)]. given #675 (T,wt=23): 2362 x * (((c1 * c2) * (c1 * (c2 * c1))) * (c2 * (c1 * c2))) != x * (c1 * c2). [ur(4,b,222,a)]. given #676 (A,wt=41): 291 ((x * (c2 * c1)) * ((c1 * (c1 * c2)) * ((c2 * c1) * (x * (c2 * c1))))) * ((x * (x * (c2 * c1))) * (x * (c2 * c1))) != x * (c2 * c1). [ur(103,b,27,a(flip))]. given #677 (F,wt=23): 2373 (((c1 * (c1 * c2)) * (c2 * c1)) * x) * y != ((c1 * (c1 * c2)) * x) * y. [ur(5,b,229,a)]. given #678 (F,wt=23): 2374 x * (((c1 * (c1 * c2)) * (c2 * c1)) * y) != x * ((c1 * (c1 * c2)) * y). [ur(4,b,229,a)]. given #679 (T,wt=23): 2379 (c2 * (c1 * c2)) * (((c1 * (c1 * c2)) * (c2 * c1)) * (c1 * c2)) != c1 * c2. [ur(101,b,229,a(flip))]. given #680 (T,wt=23): 2414 (x * ((c1 * (c1 * c2)) * (c2 * c1))) * y != (x * (c1 * (c1 * c2))) * y. [ur(5,b,230,a)]. given #681 (A,wt=31): 293 ((c2 * (c2 * c1)) * (x * (c1 * c2))) * ((x * (x * (c1 * c2))) * (x * (c1 * c2))) != x * (c1 * c2). [ur(103,b,25,a(flip))]. given #682 (F,wt=23): 2415 x * (y * ((c1 * (c1 * c2)) * (c2 * c1))) != x * (y * (c1 * (c1 * c2))). [ur(4,b,230,a)]. given #683 (F,wt=23): 2443 (((c1 * (c1 * c2)) * (c2 * c1)) * (c2 * (c1 * c2))) * (c1 * c2) != c1 * c2. [ur(43,b,231,a)]. given #684 (T,wt=23): 2445 (c1 * c2) * (((c1 * (c1 * c2)) * (c2 * c1)) * (c2 * (c1 * c2))) != c1 * c2. [ur(41,b,231,a)]. given #685 (T,wt=23): 2449 (((c1 * (c1 * c2)) * (c2 * c1)) * (c2 * (c1 * c2))) * x != (c1 * c2) * x. [ur(5,b,231,a)]. given #686 (A,wt=27): 294 ((c1 * c2) * (c2 * c1)) * ((c1 * (c1 * (c1 * c2))) * (c1 * (c1 * c2))) != c1 * (c1 * c2). [ur(103,b,16,a(flip))]. given #687 (F,wt=23): 2450 x * (((c1 * (c1 * c2)) * (c2 * c1)) * (c2 * (c1 * c2))) != x * (c1 * c2). [ur(4,b,231,a)]. given #688 (F,wt=23): 2492 (x * ((c2 * c1) * ((c1 * (c1 * c2)) * x))) * y != ((c2 * c1) * x) * y. [ur(5,b,248,a)]. given #689 (T,wt=23): 2493 x * (y * ((c2 * c1) * ((c1 * (c1 * c2)) * y))) != x * ((c2 * c1) * y). [ur(4,b,248,a)]. given #690 (T,wt=23): 2511 (((c1 * c2) * (c2 * (c2 * c1))) * x) * y != ((c2 * (c2 * c1)) * x) * y. [ur(5,b,261,a)]. given #691 (A,wt=29): 298 (x * ((c2 * c1) * ((c1 * (c1 * c2)) * x))) * ((c1 * (c1 * c2)) * x) != (c1 * (c1 * c2)) * x. [ur(43,b,30,a)]. given #692 (F,wt=23): 2512 x * (((c1 * c2) * (c2 * (c2 * c1))) * y) != x * ((c2 * (c2 * c1)) * y). [ur(4,b,261,a)]. given #693 (F,wt=23): 2516 (c1 * (c2 * c1)) * (((c1 * c2) * (c2 * (c2 * c1))) * (c2 * c1)) != c2 * c1. [ur(101,b,261,a(flip))]. given #694 (T,wt=23): 2560 c1 * (((c2 * c1) * (c1 * (c1 * c2))) * (c2 * (c2 * (c2 * c1)))) != c2 * c1. [ur(10,b,111,a(flip))]. given #695 (T,wt=23): 2580 (x * ((c1 * c2) * (c2 * (c2 * c1)))) * y != (x * (c2 * (c2 * c1))) * y. [ur(5,b,262,a)]. given #696 (A,wt=35): 299 ((c1 * (c1 * c2)) * x) * (x * ((c2 * c1) * ((c1 * (c1 * c2)) * x))) != x * ((c2 * c1) * ((c1 * (c1 * c2)) * x)). [ur(42,b,30,a)]. given #697 (F,wt=23): 2581 x * (y * ((c1 * c2) * (c2 * (c2 * c1)))) != x * (y * (c2 * (c2 * c1))). [ur(4,b,262,a)]. given #698 (F,wt=23): 2609 (((c1 * c2) * (c2 * (c2 * c1))) * (c1 * (c2 * c1))) * (c2 * c1) != c2 * c1. [ur(43,b,263,a)]. given #699 (T,wt=23): 2611 (c2 * c1) * (((c1 * c2) * (c2 * (c2 * c1))) * (c1 * (c2 * c1))) != c2 * c1. [ur(41,b,263,a)]. given #700 (T,wt=23): 2615 (((c1 * c2) * (c2 * (c2 * c1))) * (c1 * (c2 * c1))) * x != (c2 * c1) * x. [ur(5,b,263,a)]. given #701 (A,wt=29): 300 ((c1 * (c1 * c2)) * x) * (x * ((c2 * c1) * ((c1 * (c1 * c2)) * x))) != (c1 * (c1 * c2)) * x. [ur(41,b,30,a)]. given #702 (F,wt=23): 2616 x * (((c1 * c2) * (c2 * (c2 * c1))) * (c1 * (c2 * c1))) != x * (c2 * c1). [ur(4,b,263,a)]. given #703 (F,wt=23): 2654 (((c2 * (c2 * c1)) * (c1 * c2)) * x) * y != ((c2 * (c2 * c1)) * x) * y. [ur(5,b,270,a)]. given #704 (T,wt=23): 2655 x * (((c2 * (c2 * c1)) * (c1 * c2)) * y) != x * ((c2 * (c2 * c1)) * y). [ur(4,b,270,a)]. given #705 (T,wt=23): 2660 (c1 * (c2 * c1)) * (((c2 * (c2 * c1)) * (c1 * c2)) * (c2 * c1)) != c2 * c1. [ur(101,b,270,a(flip))]. given #706 (A,wt=35): 301 (x * ((c2 * c1) * ((c1 * (c1 * c2)) * x))) * ((c1 * (c1 * c2)) * x) != x * ((c2 * c1) * ((c1 * (c1 * c2)) * x)). [ur(40,b,30,a)]. given #707 (F,wt=23): 2683 (x * ((c2 * (c2 * c1)) * (c1 * c2))) * y != (x * (c2 * (c2 * c1))) * y. [ur(5,b,271,a)]. given #708 (F,wt=23): 2684 x * (y * ((c2 * (c2 * c1)) * (c1 * c2))) != x * (y * (c2 * (c2 * c1))). [ur(4,b,271,a)]. given #709 (T,wt=23): 2729 (((c2 * (c2 * c1)) * (c1 * c2)) * (c1 * (c2 * c1))) * (c2 * c1) != c2 * c1. [ur(43,b,272,a)]. given #710 (T,wt=23): 2731 (c2 * c1) * (((c2 * (c2 * c1)) * (c1 * c2)) * (c1 * (c2 * c1))) != c2 * c1. [ur(41,b,272,a)]. given #711 (A,wt=35): 302 (x * ((c2 * c1) * ((c1 * (c1 * c2)) * x))) * (y * (y * ((c1 * (c1 * c2)) * x))) != y * ((c1 * (c1 * c2)) * x). [ur(12,b,30,a)]. given #712 (F,wt=23): 2735 (((c2 * (c2 * c1)) * (c1 * c2)) * (c1 * (c2 * c1))) * x != (c2 * c1) * x. [ur(5,b,272,a)]. given #713 (F,wt=23): 2736 x * (((c2 * (c2 * c1)) * (c1 * c2)) * (c1 * (c2 * c1))) != x * (c2 * c1). [ur(4,b,272,a)]. given #714 (T,wt=23): 2749 (((c2 * c1) * (c2 * (c1 * c2))) * x) * y != ((c2 * (c2 * c1)) * x) * y. [ur(5,b,317,a)]. given #715 (T,wt=23): 2750 x * (((c2 * c1) * (c2 * (c1 * c2))) * y) != x * ((c2 * (c2 * c1)) * y). [ur(4,b,317,a)]. given #716 (A,wt=41): 303 ((c1 * (c1 * c2)) * x) * (y * (y * (x * ((c2 * c1) * ((c1 * (c1 * c2)) * x))))) != y * (x * ((c2 * c1) * ((c1 * (c1 * c2)) * x))). [ur(11,b,30,a)]. given #717 (F,wt=23): 2755 (c1 * (c2 * c1)) * (((c2 * c1) * (c2 * (c1 * c2))) * (c2 * c1)) != c2 * c1. [ur(101,b,317,a(flip))]. given #718 (F,wt=23): 2797 c2 * (((c2 * (c2 * c1)) * (c1 * c2)) * (c1 * (c1 * (c1 * c2)))) != c1 * c2. [ur(10,b,119,a(flip))]. given #719 (T,wt=23): 2819 (x * ((c2 * c1) * (c2 * (c1 * c2)))) * y != (x * (c2 * (c2 * c1))) * y. [ur(5,b,318,a)]. given #720 (T,wt=23): 2820 x * (y * ((c2 * c1) * (c2 * (c1 * c2)))) != x * (y * (c2 * (c2 * c1))). [ur(4,b,318,a)]. given #721 (A,wt=25): 304 (x * ((c2 * c1) * ((c1 * (c1 * c2)) * x))) * y != ((c1 * (c1 * c2)) * x) * y. [ur(5,b,30,a)]. given #722 (F,wt=23): 2848 (((c2 * c1) * (c2 * (c1 * c2))) * (c1 * (c2 * c1))) * (c2 * c1) != c2 * c1. [ur(43,b,319,a)]. given #723 (F,wt=23): 2850 (c2 * c1) * (((c2 * c1) * (c2 * (c1 * c2))) * (c1 * (c2 * c1))) != c2 * c1. [ur(41,b,319,a)]. given #724 (T,wt=23): 2854 (((c2 * c1) * (c2 * (c1 * c2))) * (c1 * (c2 * c1))) * x != (c2 * c1) * x. [ur(5,b,319,a)]. given #725 (T,wt=23): 2855 x * (((c2 * c1) * (c2 * (c1 * c2))) * (c1 * (c2 * c1))) != x * (c2 * c1). [ur(4,b,319,a)]. given #726 (A,wt=25): 305 x * (y * ((c2 * c1) * ((c1 * (c1 * c2)) * y))) != x * ((c1 * (c1 * c2)) * y). [ur(4,b,30,a)]. given #727 (F,wt=23): 2891 ((c2 * ((c2 * c1) * (c1 * (c1 * c2)))) * (c1 * c2)) * (c1 * c2) != c1 * c2. [ur(43,b,321,a)]. given #728 (F,wt=23): 2893 (c1 * c2) * ((c2 * ((c2 * c1) * (c1 * (c1 * c2)))) * (c1 * c2)) != c1 * c2. [ur(41,b,321,a)]. given #729 (T,wt=23): 2897 ((c2 * ((c2 * c1) * (c1 * (c1 * c2)))) * (c1 * c2)) * x != (c1 * c2) * x. [ur(5,b,321,a)]. given #730 (T,wt=23): 2898 x * ((c2 * ((c2 * c1) * (c1 * (c1 * c2)))) * (c1 * c2)) != x * (c1 * c2). [ur(4,b,321,a)]. given #731 (A,wt=51): 306 ((x * (c1 * (c1 * c2))) * ((c2 * c1) * ((c1 * (c1 * c2)) * (x * (c1 * (c1 * c2)))))) * ((x * (x * (c1 * (c1 * c2)))) * (x * (c1 * (c1 * c2)))) != x * (c1 * (c1 * c2)). [ur(103,b,30,a(flip))]. given #732 (F,wt=23): 2899 ((c1 * c2) * (c2 * ((c2 * c1) * (c1 * (c1 * c2))))) * (c1 * c2) != c1 * c2. [ur(43,b,323,a)]. given #733 (F,wt=23): 2901 (c1 * c2) * ((c1 * c2) * (c2 * ((c2 * c1) * (c1 * (c1 * c2))))) != c1 * c2. [ur(41,b,323,a)]. given #734 (T,wt=23): 2905 ((c1 * c2) * (c2 * ((c2 * c1) * (c1 * (c1 * c2))))) * x != (c1 * c2) * x. [ur(5,b,323,a)]. given #735 (T,wt=23): 2906 x * ((c1 * c2) * (c2 * ((c2 * c1) * (c1 * (c1 * c2))))) != x * (c1 * c2). [ur(4,b,323,a)]. given #736 (A,wt=27): 307 (c2 * (c1 * c2)) * ((c1 * c2) * ((c2 * c1) * ((c1 * (c1 * c2)) * (c1 * c2)))) != c1 * c2. [ur(101,b,30,a(flip))]. given #737 (F,wt=23): 2929 ((c2 * ((c2 * c1) * (c1 * (c1 * c2)))) * x) * y != ((c1 * c2) * x) * y. [ur(5,b,327,a)]. given #738 (F,wt=23): 2930 x * ((c2 * ((c2 * c1) * (c1 * (c1 * c2)))) * y) != x * ((c1 * c2) * y). [ur(4,b,327,a)]. given #739 (T,wt=23): 2954 (x * (c2 * ((c2 * c1) * (c1 * (c1 * c2))))) * y != (x * (c1 * c2)) * y. [ur(5,b,328,a)]. given #740 (T,wt=23): 2955 x * (y * (c2 * ((c2 * c1) * (c1 * (c1 * c2))))) != x * (y * (c1 * c2)). [ur(4,b,328,a)]. given #741 (A,wt=43): 308 (((c1 * (c1 * c2)) * x) * ((c2 * c1) * ((c1 * (c1 * c2)) * ((c1 * (c1 * c2)) * x)))) * (x * ((c1 * (c1 * c2)) * x)) != (c1 * (c1 * c2)) * x. [ur(51,b,30,a(flip))]. given #742 (F,wt=23): 2986 (c1 * (c2 * ((c2 * c1) * (c1 * (c1 * c2))))) * (c2 * (c1 * c2)) != c1 * c2. [ur(51,b,328,a(flip))]. given #743 (F,wt=23): 2987 (c1 * (c1 * c2)) * (c2 * (c2 * ((c2 * c1) * (c1 * (c1 * c2))))) != c1 * c2. [ur(22,b,328,a(flip))]. given #744 (T,wt=23): 3034 c2 * (((c1 * c2) * (c2 * (c2 * c1))) * (c1 * (c1 * (c1 * c2)))) != c1 * c2. [ur(10,b,130,a(flip))]. given #745 (T,wt=23): 3035 (c1 * ((c1 * (c1 * c2)) * (c2 * (c2 * (c2 * c1))))) * (c2 * c1) != c2 * c1. [ur(43,b,350,a)]. given #746 (A,wt=43): 309 (x * (x * (c1 * (c1 * c2)))) * ((x * (c1 * (c1 * c2))) * ((c2 * c1) * ((c1 * (c1 * c2)) * (x * (c1 * (c1 * c2)))))) != x * (c1 * (c1 * c2)). [ur(22,b,30,a(flip))]. given #747 (F,wt=23): 3037 (c2 * c1) * (c1 * ((c1 * (c1 * c2)) * (c2 * (c2 * (c2 * c1))))) != c2 * c1. [ur(41,b,350,a)]. given #748 (F,wt=23): 3041 (c1 * ((c1 * (c1 * c2)) * (c2 * (c2 * (c2 * c1))))) * x != (c2 * c1) * x. [ur(5,b,350,a)]. given #749 (T,wt=23): 3042 x * (c1 * ((c1 * (c1 * c2)) * (c2 * (c2 * (c2 * c1))))) != x * (c2 * c1). [ur(4,b,350,a)]. given #750 (T,wt=23): 3043 ((c2 * ((c1 * c2) * (c1 * (c2 * c1)))) * (c1 * c2)) * (c1 * c2) != c1 * c2. [ur(43,b,351,a)]. given #751 (A,wt=35): 310 x * (((c1 * (c1 * c2)) * x) * ((c2 * c1) * ((c1 * (c1 * c2)) * ((c1 * (c1 * c2)) * x)))) != (c1 * (c1 * c2)) * x. [ur(10,b,30,a(flip))]. given #752 (F,wt=23): 3045 (c1 * c2) * ((c2 * ((c1 * c2) * (c1 * (c2 * c1)))) * (c1 * c2)) != c1 * c2. [ur(41,b,351,a)]. given #753 (F,wt=23): 3049 ((c2 * ((c1 * c2) * (c1 * (c2 * c1)))) * (c1 * c2)) * x != (c1 * c2) * x. [ur(5,b,351,a)]. given #754 (T,wt=23): 3050 x * ((c2 * ((c1 * c2) * (c1 * (c2 * c1)))) * (c1 * c2)) != x * (c1 * c2). [ur(4,b,351,a)]. given #755 (T,wt=23): 3083 ((c1 * c2) * (c2 * ((c1 * c2) * (c1 * (c2 * c1))))) * (c1 * c2) != c1 * c2. [ur(43,b,353,a)]. given #756 (A,wt=25): 312 (c2 * (c2 * c1)) * ((c2 * c1) * (c2 * (c1 * c2))) != (c2 * c1) * (c2 * (c1 * c2)). [ur(42,b,79,a)]. given #757 (F,wt=23): 3085 (c1 * c2) * ((c1 * c2) * (c2 * ((c1 * c2) * (c1 * (c2 * c1))))) != c1 * c2. [ur(41,b,353,a)]. given #758 (F,wt=23): 3089 ((c1 * c2) * (c2 * ((c1 * c2) * (c1 * (c2 * c1))))) * x != (c1 * c2) * x. [ur(5,b,353,a)]. given #759 (T,wt=23): 3090 x * ((c1 * c2) * (c2 * ((c1 * c2) * (c1 * (c2 * c1))))) != x * (c1 * c2). [ur(4,b,353,a)]. given #760 (T,wt=23): 3102 ((c2 * ((c1 * c2) * (c1 * (c2 * c1)))) * x) * y != ((c1 * c2) * x) * y. [ur(5,b,357,a)]. low water: id=5985, wt=91 low water: id=6119, wt=89 given #761 (A,wt=25): 314 ((c2 * c1) * (c2 * (c1 * c2))) * (c2 * (c2 * c1)) != (c2 * c1) * (c2 * (c1 * c2)). [ur(40,b,79,a)]. given #762 (F,wt=23): 3103 x * ((c2 * ((c1 * c2) * (c1 * (c2 * c1)))) * y) != x * ((c1 * c2) * y). [ur(4,b,357,a)]. low water: id=6018, wt=87 low water: id=6416, wt=85 given #763 (F,wt=23): 3133 (x * (c2 * ((c1 * c2) * (c1 * (c2 * c1))))) * y != (x * (c1 * c2)) * y. [ur(5,b,358,a)]. low water: id=6603, wt=83 given #764 (T,wt=23): 3134 x * (y * (c2 * ((c1 * c2) * (c1 * (c2 * c1))))) != x * (y * (c1 * c2)). [ur(4,b,358,a)]. given #765 (T,wt=23): 3167 (c1 * (c2 * ((c1 * c2) * (c1 * (c2 * c1))))) * (c2 * (c1 * c2)) != c1 * c2. [ur(51,b,358,a(flip))]. low water: id=6709, wt=81 given #766 (A,wt=27): 315 ((c2 * c1) * (c2 * (c1 * c2))) * (x * (x * (c2 * (c2 * c1)))) != x * (c2 * (c2 * c1)). [ur(12,b,79,a)]. given #767 (F,wt=23): 3168 (c1 * (c1 * c2)) * (c2 * (c2 * ((c1 * c2) * (c1 * (c2 * c1))))) != c1 * c2. [ur(22,b,358,a(flip))]. given #768 (F,wt=23): 3170 ((c2 * ((c1 * (c1 * c2)) * (c2 * c1))) * (c1 * c2)) * (c1 * c2) != c1 * c2. [ur(43,b,359,a)]. low water: id=6149, wt=79 given #769 (T,wt=23): 3172 (c1 * c2) * ((c2 * ((c1 * (c1 * c2)) * (c2 * c1))) * (c1 * c2)) != c1 * c2. [ur(41,b,359,a)]. low water: id=6930, wt=77 given #770 (T,wt=23): 3176 ((c2 * ((c1 * (c1 * c2)) * (c2 * c1))) * (c1 * c2)) * x != (c1 * c2) * x. [ur(5,b,359,a)]. given #771 (A,wt=31): 316 (c2 * (c2 * c1)) * (x * (x * ((c2 * c1) * (c2 * (c1 * c2))))) != x * ((c2 * c1) * (c2 * (c1 * c2))). [ur(11,b,79,a)]. given #772 (F,wt=23): 3177 x * ((c2 * ((c1 * (c1 * c2)) * (c2 * c1))) * (c1 * c2)) != x * (c1 * c2). [ur(4,b,359,a)]. given #773 (F,wt=23): 3205 ((c1 * c2) * (c2 * ((c1 * (c1 * c2)) * (c2 * c1)))) * (c1 * c2) != c1 * c2. [ur(43,b,361,a)]. given #774 (T,wt=23): 3207 (c1 * c2) * ((c1 * c2) * (c2 * ((c1 * (c1 * c2)) * (c2 * c1)))) != c1 * c2. [ur(41,b,361,a)]. given #775 (T,wt=23): 3211 ((c1 * c2) * (c2 * ((c1 * (c1 * c2)) * (c2 * c1)))) * x != (c1 * c2) * x. [ur(5,b,361,a)]. given #776 (A,wt=27): 322 (c1 * c2) * (c2 * ((c2 * c1) * (c1 * (c1 * c2)))) != c2 * ((c2 * c1) * (c1 * (c1 * c2))). [ur(42,b,178,a)]. given #777 (F,wt=23): 3212 x * ((c1 * c2) * (c2 * ((c1 * (c1 * c2)) * (c2 * c1)))) != x * (c1 * c2). [ur(4,b,361,a)]. low water: id=7118, wt=75 low water: id=7179, wt=73 given #778 (F,wt=23): 3224 ((c2 * ((c1 * (c1 * c2)) * (c2 * c1))) * x) * y != ((c1 * c2) * x) * y. [ur(5,b,365,a)]. given #779 (T,wt=23): 3225 x * ((c2 * ((c1 * (c1 * c2)) * (c2 * c1))) * y) != x * ((c1 * c2) * y). [ur(4,b,365,a)]. given #780 (T,wt=23): 3270 c2 * (((c2 * c1) * (c2 * (c1 * c2))) * (c1 * (c1 * (c1 * c2)))) != c1 * c2. [ur(10,b,138,a(flip))]. given #781 (A,wt=27): 324 (c2 * ((c2 * c1) * (c1 * (c1 * c2)))) * (c1 * c2) != c2 * ((c2 * c1) * (c1 * (c1 * c2))). [ur(40,b,178,a)]. given #782 (F,wt=23): 3290 (x * (c2 * ((c1 * (c1 * c2)) * (c2 * c1)))) * y != (x * (c1 * c2)) * y. [ur(5,b,366,a)]. given #783 (F,wt=23): 3291 x * (y * (c2 * ((c1 * (c1 * c2)) * (c2 * c1)))) != x * (y * (c1 * c2)). [ur(4,b,366,a)]. low water: id=7438, wt=71 given #784 (T,wt=23): 3326 (c1 * (c2 * ((c1 * (c1 * c2)) * (c2 * c1)))) * (c2 * (c1 * c2)) != c1 * c2. [ur(51,b,366,a(flip))]. given #785 (T,wt=23): 3327 (c1 * (c1 * c2)) * (c2 * (c2 * ((c1 * (c1 * c2)) * (c2 * c1)))) != c1 * c2. [ur(22,b,366,a(flip))]. given #786 (A,wt=25): 325 (c2 * ((c2 * c1) * (c1 * (c1 * c2)))) * (x * (x * (c1 * c2))) != x * (c1 * c2). [ur(12,b,178,a)]. low water: id=7522, wt=69 given #787 (F,wt=23): 3329 ((c1 * ((c1 * c2) * (c2 * (c2 * c1)))) * (c2 * c1)) * (c2 * c1) != c2 * c1. [ur(43,b,392,a)]. given #788 (F,wt=23): 3331 (c2 * c1) * ((c1 * ((c1 * c2) * (c2 * (c2 * c1)))) * (c2 * c1)) != c2 * c1. [ur(41,b,392,a)]. given #789 (T,wt=23): 3335 ((c1 * ((c1 * c2) * (c2 * (c2 * c1)))) * (c2 * c1)) * x != (c2 * c1) * x. [ur(5,b,392,a)]. given #790 (T,wt=23): 3336 x * ((c1 * ((c1 * c2) * (c2 * (c2 * c1)))) * (c2 * c1)) != x * (c2 * c1). [ur(4,b,392,a)]. given #791 (A,wt=33): 326 (c1 * c2) * (x * (x * (c2 * ((c2 * c1) * (c1 * (c1 * c2)))))) != x * (c2 * ((c2 * c1) * (c1 * (c1 * c2)))). [ur(11,b,178,a)]. given #792 (F,wt=23): 3367 ((c2 * c1) * (c1 * ((c1 * c2) * (c2 * (c2 * c1))))) * (c2 * c1) != c2 * c1. [ur(43,b,394,a)]. given #793 (F,wt=23): 3369 (c2 * c1) * ((c2 * c1) * (c1 * ((c1 * c2) * (c2 * (c2 * c1))))) != c2 * c1. [ur(41,b,394,a)]. given #794 (T,wt=23): 3373 ((c2 * c1) * (c1 * ((c1 * c2) * (c2 * (c2 * c1))))) * x != (c2 * c1) * x. [ur(5,b,394,a)]. low water: id=7512, wt=67 given #795 (T,wt=23): 3374 x * ((c2 * c1) * (c1 * ((c1 * c2) * (c2 * (c2 * c1))))) != x * (c2 * c1). [ur(4,b,394,a)]. low water: id=7798, wt=65 given #796 (A,wt=25): 340 ((c1 * (c1 * c2)) * (x * (x * (c2 * c1)))) * (x * (c2 * c1)) != x * (c2 * c1). [ur(43,b,31,a)]. given #797 (F,wt=23): 3386 ((c1 * ((c1 * c2) * (c2 * (c2 * c1)))) * x) * y != ((c2 * c1) * x) * y. [ur(5,b,398,a)]. given #798 (F,wt=23): 3387 x * ((c1 * ((c1 * c2) * (c2 * (c2 * c1)))) * y) != x * ((c2 * c1) * y). [ur(4,b,398,a)]. given #799 (T,wt=23): 3436 (x * (c1 * ((c1 * c2) * (c2 * (c2 * c1))))) * y != (x * (c2 * c1)) * y. [ur(5,b,399,a)]. given #800 (T,wt=23): 3437 x * (y * (c1 * ((c1 * c2) * (c2 * (c2 * c1))))) != x * (y * (c2 * c1)). [ur(4,b,399,a)]. given #801 (A,wt=33): 341 (x * (c2 * c1)) * ((c1 * (c1 * c2)) * (x * (x * (c2 * c1)))) != (c1 * (c1 * c2)) * (x * (x * (c2 * c1))). [ur(42,b,31,a)]. given #802 (F,wt=23): 3474 (c2 * (c1 * ((c1 * c2) * (c2 * (c2 * c1))))) * (c1 * (c2 * c1)) != c2 * c1. [ur(51,b,399,a(flip))]. given #803 (F,wt=23): 3475 (c2 * (c2 * c1)) * (c1 * (c1 * ((c1 * c2) * (c2 * (c2 * c1))))) != c2 * c1. [ur(22,b,399,a(flip))]. given #804 (T,wt=23): 3477 ((c1 * ((c2 * (c2 * c1)) * (c1 * c2))) * (c2 * c1)) * (c2 * c1) != c2 * c1. [ur(43,b,400,a)]. given #805 (T,wt=23): 3479 (c2 * c1) * ((c1 * ((c2 * (c2 * c1)) * (c1 * c2))) * (c2 * c1)) != c2 * c1. [ur(41,b,400,a)]. given #806 (A,wt=25): 342 (x * (c2 * c1)) * ((c1 * (c1 * c2)) * (x * (x * (c2 * c1)))) != x * (c2 * c1). [ur(41,b,31,a)]. given #807 (F,wt=23): 3483 ((c1 * ((c2 * (c2 * c1)) * (c1 * c2))) * (c2 * c1)) * x != (c2 * c1) * x. [ur(5,b,400,a)]. given #808 (F,wt=23): 3484 x * ((c1 * ((c2 * (c2 * c1)) * (c1 * c2))) * (c2 * c1)) != x * (c2 * c1). [ur(4,b,400,a)]. low water: id=7980, wt=63 given #809 (T,wt=23): 3505 ((c2 * c1) * (c1 * ((c2 * (c2 * c1)) * (c1 * c2)))) * (c2 * c1) != c2 * c1. [ur(43,b,402,a)]. given #810 (T,wt=23): 3507 (c2 * c1) * ((c2 * c1) * (c1 * ((c2 * (c2 * c1)) * (c1 * c2)))) != c2 * c1. [ur(41,b,402,a)]. given #811 (A,wt=33): 343 ((c1 * (c1 * c2)) * (x * (x * (c2 * c1)))) * (x * (c2 * c1)) != (c1 * (c1 * c2)) * (x * (x * (c2 * c1))). [ur(40,b,31,a)]. given #812 (F,wt=23): 3511 ((c2 * c1) * (c1 * ((c2 * (c2 * c1)) * (c1 * c2)))) * x != (c2 * c1) * x. [ur(5,b,402,a)]. given #813 (F,wt=23): 3512 x * ((c2 * c1) * (c1 * ((c2 * (c2 * c1)) * (c1 * c2)))) != x * (c2 * c1). [ur(4,b,402,a)]. low water: id=8119, wt=61 given #814 (T,wt=23): 3524 ((c1 * ((c2 * (c2 * c1)) * (c1 * c2))) * x) * y != ((c2 * c1) * x) * y. [ur(5,b,406,a)]. given #815 (T,wt=23): 3525 x * ((c1 * ((c2 * (c2 * c1)) * (c1 * c2))) * y) != x * ((c2 * c1) * y). [ur(4,b,406,a)]. given #816 (A,wt=31): 344 ((c1 * (c1 * c2)) * (x * (x * (c2 * c1)))) * (y * (y * (x * (c2 * c1)))) != y * (x * (c2 * c1)). [ur(12,b,31,a)]. given #817 (F,wt=23): 3601 (x * (c1 * ((c2 * (c2 * c1)) * (c1 * c2)))) * y != (x * (c2 * c1)) * y. [ur(5,b,407,a)]. given #818 (F,wt=23): 3602 x * (y * (c1 * ((c2 * (c2 * c1)) * (c1 * c2)))) != x * (y * (c2 * c1)). [ur(4,b,407,a)]. given #819 (T,wt=23): 3641 (c2 * (c1 * ((c2 * (c2 * c1)) * (c1 * c2)))) * (c1 * (c2 * c1)) != c2 * c1. [ur(51,b,407,a(flip))]. given #820 (T,wt=23): 3642 (c2 * (c2 * c1)) * (c1 * (c1 * ((c2 * (c2 * c1)) * (c1 * c2)))) != c2 * c1. [ur(22,b,407,a(flip))]. low water: id=8248, wt=59 given #821 (A,wt=39): 345 (x * (c2 * c1)) * (y * (y * ((c1 * (c1 * c2)) * (x * (x * (c2 * c1)))))) != y * ((c1 * (c1 * c2)) * (x * (x * (c2 * c1)))). [ur(11,b,31,a)]. given #822 (F,wt=23): 3644 ((c1 * ((c2 * c1) * (c2 * (c1 * c2)))) * (c2 * c1)) * (c2 * c1) != c2 * c1. [ur(43,b,445,a)]. given #823 (F,wt=23): 3646 (c2 * c1) * ((c1 * ((c2 * c1) * (c2 * (c1 * c2)))) * (c2 * c1)) != c2 * c1. [ur(41,b,445,a)]. given #824 (T,wt=23): 3650 ((c1 * ((c2 * c1) * (c2 * (c1 * c2)))) * (c2 * c1)) * x != (c2 * c1) * x. [ur(5,b,445,a)]. given #825 (T,wt=23): 3651 x * ((c1 * ((c2 * c1) * (c2 * (c1 * c2)))) * (c2 * c1)) != x * (c2 * c1). [ur(4,b,445,a)]. given #826 (A,wt=27): 346 ((c1 * (c1 * c2)) * (c1 * (c1 * (c2 * c1)))) * ((c2 * (c2 * c1)) * (c2 * c1)) != c2 * c1. [ur(103,b,31,a(flip))]. given #827 (F,wt=23): 3682 ((c2 * c1) * (c1 * ((c2 * c1) * (c2 * (c1 * c2))))) * (c2 * c1) != c2 * c1. [ur(43,b,447,a)]. given #828 (F,wt=23): 3684 (c2 * c1) * ((c2 * c1) * (c1 * ((c2 * c1) * (c2 * (c1 * c2))))) != c2 * c1. [ur(41,b,447,a)]. given #829 (T,wt=23): 3688 ((c2 * c1) * (c1 * ((c2 * c1) * (c2 * (c1 * c2))))) * x != (c2 * c1) * x. [ur(5,b,447,a)]. given #830 (T,wt=23): 3689 x * ((c2 * c1) * (c1 * ((c2 * c1) * (c2 * (c1 * c2))))) != x * (c2 * c1). [ur(4,b,447,a)]. given #831 (A,wt=31): 347 (c1 * (c2 * c1)) * ((c1 * (c1 * c2)) * ((c2 * (c2 * c1)) * ((c2 * (c2 * c1)) * (c2 * c1)))) != c2 * c1. [ur(101,b,31,a(flip))]. given #832 (F,wt=23): 3701 ((c1 * ((c2 * c1) * (c2 * (c1 * c2)))) * x) * y != ((c2 * c1) * x) * y. [ur(5,b,451,a)]. low water: id=8398, wt=57 given #833 (F,wt=23): 3702 x * ((c1 * ((c2 * c1) * (c2 * (c1 * c2)))) * y) != x * ((c2 * c1) * y). [ur(4,b,451,a)]. given #834 (T,wt=23): 3738 (x * (c1 * ((c2 * c1) * (c2 * (c1 * c2))))) * y != (x * (c2 * c1)) * y. [ur(5,b,452,a)]. given #835 (T,wt=23): 3739 x * (y * (c1 * ((c2 * c1) * (c2 * (c1 * c2))))) != x * (y * (c2 * c1)). [ur(4,b,452,a)]. given #836 (A,wt=27): 352 (c1 * c2) * (c2 * ((c1 * c2) * (c1 * (c2 * c1)))) != c2 * ((c1 * c2) * (c1 * (c2 * c1))). [ur(42,b,223,a)]. given #837 (F,wt=23): 3778 (c2 * (c1 * ((c2 * c1) * (c2 * (c1 * c2))))) * (c1 * (c2 * c1)) != c2 * c1. [ur(51,b,452,a(flip))]. given #838 (F,wt=23): 3779 (c2 * (c2 * c1)) * (c1 * (c1 * ((c2 * c1) * (c2 * (c1 * c2))))) != c2 * c1. [ur(22,b,452,a(flip))]. given #839 (T,wt=23): 3789 ((c2 * c1) * (x * (x * (c1 * (c1 * c2))))) * y != (x * (c2 * c1)) * y. [ur(5,b,510,a)]. given #840 (T,wt=23): 3790 x * ((c2 * c1) * (y * (y * (c1 * (c1 * c2))))) != x * (y * (c2 * c1)). [ur(4,b,510,a)]. given #841 (A,wt=27): 354 (c2 * ((c1 * c2) * (c1 * (c2 * c1)))) * (c1 * c2) != c2 * ((c1 * c2) * (c1 * (c2 * c1))). [ur(40,b,223,a)]. given #842 (F,wt=23): 3816 (c2 * (c2 * c1)) * ((c2 * c1) * (c1 * (c1 * (c1 * (c1 * c2))))) != c2 * c1. [ur(22,b,510,a(flip))]. given #843 (F,wt=23): 3839 (c2 * ((c2 * (c2 * c1)) * (c1 * (c1 * (c1 * c2))))) * (c1 * c2) != c1 * c2. [ur(43,b,598,a)]. given #844 (T,wt=23): 3841 (c1 * c2) * (c2 * ((c2 * (c2 * c1)) * (c1 * (c1 * (c1 * c2))))) != c1 * c2. [ur(41,b,598,a)]. given #845 (T,wt=23): 3845 (c2 * ((c2 * (c2 * c1)) * (c1 * (c1 * (c1 * c2))))) * x != (c1 * c2) * x. [ur(5,b,598,a)]. low water: id=8425, wt=55 given #846 (A,wt=25): 355 (c2 * ((c1 * c2) * (c1 * (c2 * c1)))) * (x * (x * (c1 * c2))) != x * (c1 * c2). [ur(12,b,223,a)]. given #847 (F,wt=23): 3846 x * (c2 * ((c2 * (c2 * c1)) * (c1 * (c1 * (c1 * c2))))) != x * (c1 * c2). [ur(4,b,598,a)]. given #848 (F,wt=23): 3855 (x * ((c1 * c2) * ((c2 * (c2 * c1)) * x))) * y != ((c1 * c2) * x) * y. [ur(5,b,624,a)]. given #849 (T,wt=23): 3856 x * (y * ((c1 * c2) * ((c2 * (c2 * c1)) * y))) != x * ((c1 * c2) * y). [ur(4,b,624,a)]. low water: id=8704, wt=53 given #850 (T,wt=23): 3871 ((c1 * c2) * (x * (x * (c2 * (c2 * c1))))) * y != (x * (c1 * c2)) * y. [ur(5,b,715,a)]. given #851 (A,wt=33): 356 (c1 * c2) * (x * (x * (c2 * ((c1 * c2) * (c1 * (c2 * c1)))))) != x * (c2 * ((c1 * c2) * (c1 * (c2 * c1)))). [ur(11,b,223,a)]. given #852 (F,wt=23): 3872 x * ((c1 * c2) * (y * (y * (c2 * (c2 * c1))))) != x * (y * (c1 * c2)). [ur(4,b,715,a)]. given #853 (F,wt=23): 3898 (c1 * (c1 * c2)) * ((c1 * c2) * (c2 * (c2 * (c2 * (c2 * c1))))) != c1 * c2. [ur(22,b,715,a(flip))]. given #854 (T,wt=23): 3916 ((c2 * c1) * (c1 * (c1 * c2))) * x != ((c1 * (c1 * c2)) * (c2 * c1)) * x. [ur(5,b,890,a)]. given #855 (T,wt=23): 3917 x * ((c2 * c1) * (c1 * (c1 * c2))) != x * ((c1 * (c1 * c2)) * (c2 * c1)). [ur(4,b,890,a)]. given #856 (A,wt=27): 360 (c1 * c2) * (c2 * ((c1 * (c1 * c2)) * (c2 * c1))) != c2 * ((c1 * (c1 * c2)) * (c2 * c1)). [ur(42,b,232,a)]. given #857 (F,wt=23): 3924 ((c2 * (c2 * c1)) * (c1 * c2)) * x != ((c1 * c2) * (c2 * (c2 * c1))) * x. [ur(5,b,1249,a)]. given #858 (F,wt=23): 3925 x * ((c2 * (c2 * c1)) * (c1 * c2)) != x * ((c1 * c2) * (c2 * (c2 * c1))). [ur(4,b,1249,a)]. given #859 (T,wt=23): 3926 (c2 * (c1 * (c2 * ((c2 * c1) * (c1 * (c1 * c2)))))) * (c1 * c2) != c1 * c2. [ur(43,b,2988,a)]. given #860 (T,wt=23): 3928 (c1 * c2) * (c2 * (c1 * (c2 * ((c2 * c1) * (c1 * (c1 * c2)))))) != c1 * c2. [ur(41,b,2988,a)]. given #861 (A,wt=27): 362 (c2 * ((c1 * (c1 * c2)) * (c2 * c1))) * (c1 * c2) != c2 * ((c1 * (c1 * c2)) * (c2 * c1)). [ur(40,b,232,a)]. given #862 (F,wt=23): 3932 (c2 * (c1 * (c2 * ((c2 * c1) * (c1 * (c1 * c2)))))) * x != (c1 * c2) * x. [ur(5,b,2988,a)]. given #863 (F,wt=23): 3933 x * (c2 * (c1 * (c2 * ((c2 * c1) * (c1 * (c1 * c2)))))) != x * (c1 * c2). [ur(4,b,2988,a)]. given #864 (T,wt=23): 3934 (c2 * (c1 * (c2 * ((c1 * c2) * (c1 * (c2 * c1)))))) * (c1 * c2) != c1 * c2. [ur(43,b,3169,a)]. given #865 (T,wt=23): 3936 (c1 * c2) * (c2 * (c1 * (c2 * ((c1 * c2) * (c1 * (c2 * c1)))))) != c1 * c2. [ur(41,b,3169,a)]. given #866 (A,wt=25): 363 (c2 * ((c1 * (c1 * c2)) * (c2 * c1))) * (x * (x * (c1 * c2))) != x * (c1 * c2). [ur(12,b,232,a)]. given #867 (F,wt=23): 3940 (c2 * (c1 * (c2 * ((c1 * c2) * (c1 * (c2 * c1)))))) * x != (c1 * c2) * x. [ur(5,b,3169,a)]. given #868 (F,wt=23): 3941 x * (c2 * (c1 * (c2 * ((c1 * c2) * (c1 * (c2 * c1)))))) != x * (c1 * c2). [ur(4,b,3169,a)]. given #869 (T,wt=23): 3948 (c2 * (c1 * (c2 * ((c1 * (c1 * c2)) * (c2 * c1))))) * (c1 * c2) != c1 * c2. [ur(43,b,3328,a)]. given #870 (T,wt=23): 3950 (c1 * c2) * (c2 * (c1 * (c2 * ((c1 * (c1 * c2)) * (c2 * c1))))) != c1 * c2. [ur(41,b,3328,a)]. given #871 (A,wt=33): 364 (c1 * c2) * (x * (x * (c2 * ((c1 * (c1 * c2)) * (c2 * c1))))) != x * (c2 * ((c1 * (c1 * c2)) * (c2 * c1))). [ur(11,b,232,a)]. given #872 (F,wt=23): 3954 (c2 * (c1 * (c2 * ((c1 * (c1 * c2)) * (c2 * c1))))) * x != (c1 * c2) * x. [ur(5,b,3328,a)]. given #873 (F,wt=23): 3955 x * (c2 * (c1 * (c2 * ((c1 * (c1 * c2)) * (c2 * c1))))) != x * (c1 * c2). [ur(4,b,3328,a)]. given #874 (T,wt=23): 3956 (c1 * (c2 * (c1 * ((c1 * c2) * (c2 * (c2 * c1)))))) * (c2 * c1) != c2 * c1. [ur(43,b,3476,a)]. given #875 (T,wt=23): 3958 (c2 * c1) * (c1 * (c2 * (c1 * ((c1 * c2) * (c2 * (c2 * c1)))))) != c2 * c1. [ur(41,b,3476,a)]. given #876 (A,wt=37): 368 (((c2 * c1) * ((c2 * c1) * x)) * ((c2 * c1) * x)) * ((x * ((c2 * c1) * x)) * ((c1 * (c1 * c2)) * x)) != (c2 * c1) * x. [ur(151,b,29,a)]. given #877 (F,wt=23): 3962 (c1 * (c2 * (c1 * ((c1 * c2) * (c2 * (c2 * c1)))))) * x != (c2 * c1) * x. [ur(5,b,3476,a)]. given #878 (F,wt=23): 3963 x * (c1 * (c2 * (c1 * ((c1 * c2) * (c2 * (c2 * c1)))))) != x * (c2 * c1). [ur(4,b,3476,a)]. given #879 (T,wt=23): 3964 (c1 * (c2 * (c1 * ((c2 * (c2 * c1)) * (c1 * c2))))) * (c2 * c1) != c2 * c1. [ur(43,b,3643,a)]. given #880 (T,wt=23): 3966 (c2 * c1) * (c1 * (c2 * (c1 * ((c2 * (c2 * c1)) * (c1 * c2))))) != c2 * c1. [ur(41,b,3643,a)]. given #881 (A,wt=37): 369 ((x * (x * (c2 * c1))) * (x * (c2 * c1))) * (((c1 * (c1 * c2)) * (x * (c2 * c1))) * (x * (c2 * c1))) != x * (c2 * c1). [ur(151,b,28,a)]. given #882 (F,wt=23): 3970 (c1 * (c2 * (c1 * ((c2 * (c2 * c1)) * (c1 * c2))))) * x != (c2 * c1) * x. [ur(5,b,3643,a)]. low water: id=8953, wt=51 given #883 (F,wt=23): 3971 x * (c1 * (c2 * (c1 * ((c2 * (c2 * c1)) * (c1 * c2))))) != x * (c2 * c1). [ur(4,b,3643,a)]. ============================== STATISTICS ============================ Given=883. Generated=61228. Kept=11674. proofs=0. Usable=879. Sos=9999. Demods=24. Limbo=0, Disabled=800. Hints=0. Weight_deleted=24224. Literals_deleted=0. Forward_subsumed=17724. Back_subsumed=82. Sos_limit_deleted=7606. Sos_displaced=701. Sos_removed=0. New_demodulators=28 (0 lex), Back_demodulated=13. Back_unit_deleted=0. Demod_attempts=11508133. Demod_rewrites=458163. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=219118. Nonunit_bsub_feature_tests=225. Megabytes=21.88. User_CPU=11.00, System_CPU=0.05, Wall_clock=11. ============================== end of statistics ===================== ============================== end of search ========================= SEARCH FAILED Exiting with failure. Process 10672 exit (max_seconds) Sat Aug 12 20:58:11 2006