============================== Prover9 =============================== Prover9 (32) version March-2007, March 2007. Process 21033 was started by mccune on cleo, Mon Mar 19 17:02:23 2007 The command was "/home/mccune/bin/prover9 -f quot-xy3b.in". ============================== end of head =========================== ============================== INPUT ================================= % Reading from file quot-xy3b.in op(400,infix_right,*). set(restrict_denials). assign(max_weight,35). formulas(sos). (x * y) * z = x * y * z # label(associativity). x * y != u | x * z != u | y = z # label(left_cancellation_extended). y * x != u | z * x != u | y = z # label(right_cancellation_extended). x * y * x * y * x * y = y * x * y * x * y * x # label("(xy)^3 = (yx)^3"). b * b0 = a * a0. d * b0 = c * a0. b * d0 = a * c0. d * d0 != c * c0. end_of_list. ============================== end of input ========================== ============================== PROCESS NON-CLAUSAL FORMULAS ========== % Formulas that are not ordinary clauses: ============================== end of process non-clausal formulas === ============================== PROCESS INITIAL CLAUSES =============== % Clauses before input processing: formulas(usable). end_of_list. formulas(sos). (x * y) * z = x * y * z # label(associativity). [assumption]. x * y != z | x * u != z | y = u # label(left_cancellation_extended). [assumption]. x * y != z | u * y != z | x = u # label(right_cancellation_extended). [assumption]. x * y * x * y * x * y = y * x * y * x * y * x # label("(xy)^3 = (yx)^3"). [assumption]. b * b0 = a * a0. [assumption]. d * b0 = c * a0. [assumption]. b * d0 = a * c0. [assumption]. d * d0 != c * c0. [assumption]. 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([ a, a0, b, b0, c, c0, d, d0, * ]). 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, 3). % (nonunit Horn with equality) Auto_process settings: (no changes). restricted denial: (wt=7): 8 d * d0 != c * c0. [assumption]. ============================== end of process initial clauses ======== ============================== CLAUSES FOR SEARCH ==================== % Clauses after input processing: formulas(usable). 8 d * d0 != c * c0. [assumption]. end_of_list. formulas(sos). 1 (x * y) * z = x * y * z # label(associativity). [assumption]. 2 x * y != z | x * u != z | y = u # label(left_cancellation_extended). [assumption]. 3 x * y != z | u * y != z | x = u # label(right_cancellation_extended). [assumption]. 4 x * y * x * y * x * y = y * x * y * x * y * x # label("(xy)^3 = (yx)^3"). [assumption]. 5 b * b0 = a * a0. [assumption]. 6 d * b0 = c * a0. [assumption]. 7 b * d0 = a * c0. [assumption]. end_of_list. formulas(demodulators). 1 (x * y) * z = x * y * z # label(associativity). [assumption]. 5 b * b0 = a * a0. [assumption]. 6 d * b0 = c * a0. [assumption]. 7 b * d0 = a * c0. [assumption]. end_of_list. ============================== end of clauses for search ============= ============================== SEARCH ================================ % Starting search at 0.00 seconds. given #1 (I,wt=11): 1 (x * y) * z = x * y * z # label(associativity). [assumption]. given #2 (I,wt=13): 2 x * y != z | x * u != z | y = u # label(left_cancellation_extended). [assumption]. given #3 (I,wt=13): 3 x * y != z | u * y != z | x = u # label(right_cancellation_extended). [assumption]. given #4 (I,wt=23): 4 x * y * x * y * x * y = y * x * y * x * y * x # label("(xy)^3 = (yx)^3"). [assumption]. given #5 (I,wt=7): 5 b * b0 = a * a0. [assumption]. given #6 (I,wt=7): 6 d * b0 = c * a0. [assumption]. given #7 (I,wt=7): 7 b * d0 = a * c0. [assumption]. given #8 (A,wt=17): 9 x * y * z != u | x * y * v != u | z = v. [para(1(a,1),2(a,1)),rewrite(1(5))]. given #9 (T,wt=11): 18 b * b0 * x = a * a0 * x. [para(5(a,1),1(a,1,1)),rewrite(1(4)),flip(a)]. given #10 (T,wt=11): 22 d * b0 * x = c * a0 * x. [para(6(a,1),1(a,1,1)),rewrite(1(4)),flip(a)]. given #11 (T,wt=11): 26 b * d0 * x = a * c0 * x. [para(7(a,1),1(a,1,1)),rewrite(1(4)),flip(a)]. given #12 (T,wt=13): 19 a * a0 != x | b * y != x | b0 = y. [para(5(a,1),2(a,1))]. given #13 (A,wt=17): 10 x * y * z != u | v * z != u | x * y = v. [para(1(a,1),3(a,1))]. given #14 (T,wt=13): 20 a * a0 != x | y * b0 != x | b = y. [para(5(a,1),3(a,1))]. given #15 (T,wt=13): 23 c * a0 != x | d * y != x | b0 = y. [para(6(a,1),2(a,1))]. given #16 (T,wt=13): 24 c * a0 != x | y * b0 != x | d = y. [para(6(a,1),3(a,1))]. given #17 (T,wt=13): 27 a * c0 != x | b * y != x | d0 = y. [para(7(a,1),2(a,1))]. given #18 (A,wt=31): 11 x * y * y * x * y * y * x * y = y * x * y * y * x * y * y * x. [hyper(2,a,1,a(flip),b,4,a),rewrite(1(3),1(5),1(12),1(14))]. given #19 (T,wt=13): 28 a * c0 != x | y * d0 != x | b = y. [para(7(a,1),3(a,1))]. given #20 (T,wt=13): 53 a * a0 != x | a * c0 != x | d0 = b0. [para(7(a,1),19(b,1)),flip(c)]. given #21 (T,wt=13): 73 a * a0 != x | c * a0 != x | d = b. [para(6(a,1),20(b,1)),flip(c)]. given #22 (T,wt=17): 33 x * a * a0 != y | x * b * z != y | b0 = z. [para(5(a,1),9(a,1,2))]. given #23 (A,wt=27): 12 x * y * x * y * x * y * z = y * x * y * x * y * x * z. [para(4(a,1),1(a,1,1)),rewrite(1(6),1(5),1(4),1(3),1(2),1(11),1(10),1(9),1(8))]. given #24 (T,wt=17): 34 x * c * a0 != y | x * d * z != y | b0 = z. [para(6(a,1),9(a,1,2))]. given #25 (T,wt=17): 35 x * a * c0 != y | x * b * z != y | d0 = z. [para(7(a,1),9(a,1,2))]. given #26 (T,wt=17): 36 a * a0 * x != y | b * z != y | b0 * x = z. [para(18(a,1),2(a,1))]. given #27 (T,wt=17): 37 a * a0 * x != y | z * b0 * x != y | b = z. [para(18(a,1),3(a,1))]. given #28 (A,wt=35): 13 x * y * z * x * y * z * x * y * z = z * x * y * z * x * y * z * x * y. [para(4(a,1),1(a,1)),rewrite(1(5),1(7),1(11),1(13)),flip(a)]. given #29 (T,wt=17): 41 c * a0 * x != y | d * z != y | b0 * x = z. [para(22(a,1),2(a,1))]. given #30 (T,wt=17): 42 c * a0 * x != y | z * b0 * x != y | d = z. [para(22(a,1),3(a,1))]. given #31 (T,wt=17): 47 a * c0 * x != y | b * z != y | d0 * x = z. [para(26(a,1),2(a,1))]. given #32 (T,wt=17): 48 a * c0 * x != y | z * d0 * x != y | b = z. [para(26(a,1),3(a,1))]. given #33 (A,wt=27): 14 x * y * z * y * z * y * z = x * z * y * z * y * z * y. [para(4(a,1),1(a,2,2)),rewrite(1(6))]. given #34 (T,wt=17): 54 a * a0 != x | a * a0 * y != x | b0 * y = b0. [para(18(a,1),19(b,1)),flip(c)]. given #35 (T,wt=17): 55 a * a0 != x | a * c0 * y != x | d0 * y = b0. [para(26(a,1),19(b,1)),flip(c)]. given #36 (T,wt=17): 61 x * a * a0 != y | z * b0 != y | x * b = z. [para(5(a,1),10(a,1,2))]. given #37 (T,wt=17): 62 x * y * b0 != z | a * a0 != z | x * y = b. [para(5(a,1),10(b,1))]. given #38 (A,wt=29): 15 x * y * x * y * x * y != z | y * u != z | x * y * x * y * x = u. [para(4(a,1),2(a,1))]. given #39 (T,wt=17): 63 x * c * a0 != y | z * b0 != y | x * d = z. [para(6(a,1),10(a,1,2))]. given #40 (T,wt=17): 64 x * y * b0 != z | c * a0 != z | x * y = d. [para(6(a,1),10(b,1))]. given #41 (T,wt=17): 65 x * a * c0 != y | z * d0 != y | x * b = z. [para(7(a,1),10(a,1,2))]. given #42 (T,wt=17): 66 x * y * d0 != z | a * c0 != z | x * y = b. [para(7(a,1),10(b,1))]. given #43 (A,wt=29): 16 x * y * x * y * x * y != z | u * x * y * x * y * x != z | y = u. [para(4(a,1),3(a,1))]. given #44 (T,wt=17): 75 c * a0 != x | c * a0 * y != x | b0 * y = b0. [para(22(a,1),23(b,1)),flip(c)]. given #45 (T,wt=17): 77 a * c0 != x | a * a0 * y != x | b0 * y = d0. [para(18(a,1),27(b,1)),flip(c)]. given #46 (T,wt=17): 78 a * c0 != x | a * c0 * y != x | d0 * y = d0. [para(26(a,1),27(b,1)),flip(c)]. given #47 (T,wt=17): 102 x * a * a0 != y | x * a * c0 != y | d0 = b0. [para(7(a,1),33(b,1,2)),flip(c)]. given #48 (A,wt=29): 17 x * y * z * y * z * y != u | y * z * y * z * y * z != u | x = z. [para(4(a,1),3(b,1))]. given #49 (T,wt=17): 154 a * a0 * x != y | c * a0 * x != y | d = b. [para(22(a,1),37(b,1)),flip(c)]. given #50 (T,wt=17): 199 x * a * a0 != y | a * a0 != y | x * b = b. [para(5(a,1),61(b,1))]. given #51 (T,wt=17): 200 x * a * a0 != y | c * a0 != y | x * b = d. [para(6(a,1),61(b,1))]. given #52 (T,wt=17): 202 x * c * a0 != y | a * a0 != y | x * d = b. [para(6(a,1),62(a,1,2))]. given #53 (A,wt=23): 21 b0 * a * a0 * a * a0 * b = a * a0 * a * a0 * a * a0. [para(5(a,1),4(a,1,2,2,2,2)),rewrite(18(9),18(11),18(19),18(21)),flip(a)]. given #54 (T,wt=17): 208 x * c * a0 != y | c * a0 != y | x * d = d. [para(6(a,1),63(b,1))]. given #55 (T,wt=17): 212 x * a * c0 != y | a * c0 != y | x * b = b. [para(7(a,1),65(b,1))]. given #56 (T,wt=21): 30 x * y * z * u != v | x * y * z * w != v | u = w. [para(1(a,1),9(a,1,2)),rewrite(1(6))]. given #57 (T,wt=21): 40 x * a * a0 * y != z | x * b * u != z | b0 * y = u. [para(18(a,1),9(a,1,2))]. given #58 (A,wt=23): 29 d0 * a * c0 * a * c0 * b = a * c0 * a * c0 * a * c0. [para(7(a,1),4(a,1,2,2,2,2)),rewrite(26(9),26(11),26(19),26(21)),flip(a)]. given #59 (T,wt=21): 46 x * c * a0 * y != z | x * d * u != z | b0 * y = u. [para(22(a,1),9(a,1,2))]. given #60 (T,wt=21): 51 x * a * c0 * y != z | x * b * u != z | d0 * y = u. [para(26(a,1),9(a,1,2))]. given #61 (T,wt=21): 56 x * y * z * u != v | w * u != v | x * y * z = w. [para(1(a,1),10(a,1,2))]. given #62 (T,wt=21): 57 x * y * z != u | v * w * z != u | x * y = v * w. [para(1(a,1),10(b,1))]. given #63 (A,wt=33): 31 x * y * z * y * z * y * z != u | x * z * v != u | y * z * y * z * y = v. [para(4(a,1),9(a,1,2))]. given #64 (T,wt=21): 67 x * a * a0 * y != z | u * b0 * y != z | x * b = u. [para(18(a,1),10(a,1,2))]. given #65 (T,wt=21): 68 x * y * b0 * z != u | a * a0 * z != u | x * y = b. [para(18(a,1),10(b,1))]. given #66 (T,wt=21): 69 x * c * a0 * y != z | u * b0 * y != z | x * d = u. [para(22(a,1),10(a,1,2))]. given #67 (T,wt=21): 70 x * y * b0 * z != u | c * a0 * z != u | x * y = d. [para(22(a,1),10(b,1))]. given #68 (A,wt=29): 32 x * y * x * y * x * y != z | y * x * u != z | y * x * y * x = u. [para(4(a,1),9(a,1))]. given #69 (T,wt=21): 71 x * a * c0 * y != z | u * d0 * y != z | x * b = u. [para(26(a,1),10(a,1,2))]. given #70 (T,wt=21): 72 x * y * d0 * z != u | a * c0 * z != u | x * y = b. [para(26(a,1),10(b,1))]. given #71 (T,wt=21): 99 x * y * a * a0 != z | x * y * b * u != z | b0 = u. [para(1(a,1),33(a,1)),rewrite(1(10))]. given #72 (T,wt=21): 103 x * a * a0 != y | x * a * a0 * z != y | b0 * z = b0. [para(18(a,1),33(b,1,2)),flip(c)]. given #73 (A,wt=35): 38 b0 * x * a * a0 * x * a * a0 * x * b = a * a0 * x * a * a0 * x * a * a0 * x. [para(18(a,1),4(a,1,2,2,2,2)),rewrite(1(11),18(12),1(13),18(14),1(24),18(25),1(26),18(27),1(28)),flip(a)]. given #74 (T,wt=21): 104 x * a * a0 != y | x * a * c0 * z != y | d0 * z = b0. [para(26(a,1),33(b,1,2)),flip(c)]. given #75 (T,wt=21): 132 x * y * c * a0 != z | x * y * d * u != z | b0 = u. [para(1(a,1),34(a,1)),rewrite(1(10))]. given #76 (T,wt=21): 135 x * c * a0 != y | x * c * a0 * z != y | b0 * z = b0. [para(22(a,1),34(b,1,2)),flip(c)]. given #77 (T,wt=21): 137 x * y * a * c0 != z | x * y * b * u != z | d0 = u. [para(1(a,1),35(a,1)),rewrite(1(10))]. given #78 (A,wt=27): 39 b * x * b0 * x * b0 * x * b0 = a * a0 * x * b0 * x * b0 * x. [para(4(a,1),18(a,1,2))]. given #79 (T,wt=21): 140 x * a * c0 != y | x * a * a0 * z != y | b0 * z = d0. [para(18(a,1),35(b,1,2)),flip(c)]. given #80 (T,wt=21): 141 x * a * c0 != y | x * a * c0 * z != y | d0 * z = d0. [para(26(a,1),35(b,1,2)),flip(c)]. given #81 (T,wt=21): 147 a * a0 * x != y | a * a0 * z != y | b0 * x = b0 * z. [para(18(a,1),36(b,1))]. given #82 (T,wt=21): 148 a * a0 * x != y | a * c0 * z != y | d0 * z = b0 * x. [para(26(a,1),36(b,1)),flip(c)]. given #83 (A,wt=35): 43 c * a0 * x * c * a0 * x * c * a0 * x = b0 * x * c * a0 * x * c * a0 * x * d. [para(22(a,1),4(a,1,2,2,2,2)),rewrite(1(11),22(12),1(13),22(14),1(24),22(25),1(26),22(27),1(28))]. given #84 (T,wt=21): 164 c * a0 * x != y | c * a0 * z != y | b0 * x = b0 * z. [para(22(a,1),41(b,1))]. given #85 (T,wt=21): 176 a * c0 * x != y | a * c0 * z != y | d0 * x = d0 * z. [para(26(a,1),47(b,1))]. given #86 (T,wt=21): 197 x * y * a * a0 != z | u * b0 != z | x * y * b = u. [para(1(a,1),61(a,1)),rewrite(1(12))]. given #87 (T,wt=21): 198 x * a * a0 != y | z * u * b0 != y | x * b = z * u. [para(1(a,1),61(b,1))]. given #88 (A,wt=27): 44 d * x * b0 * x * b0 * x * b0 = c * a0 * x * b0 * x * b0 * x. [para(4(a,1),22(a,1,2))]. given #89 (T,wt=21): 201 x * y * z * b0 != u | a * a0 != u | x * y * z = b. [para(1(a,1),62(a,1,2))]. given #90 (T,wt=21): 206 x * y * c * a0 != z | u * b0 != z | x * y * d = u. [para(1(a,1),63(a,1)),rewrite(1(12))]. given #91 (T,wt=21): 207 x * c * a0 != y | z * u * b0 != y | x * d = z * u. [para(1(a,1),63(b,1))]. given #92 (T,wt=21): 209 x * y * z * b0 != u | c * a0 != u | x * y * z = d. [para(1(a,1),64(a,1,2))]. given #93 (A,wt=23): 45 b0 * c * a0 * c * a0 * d = a0 * c * a0 * c * a0 * c. [para(4(a,1),22(a,2)),rewrite(22(11),25(11))]. given #94 (T,wt=21): 210 x * y * a * c0 != z | u * d0 != z | x * y * b = u. [para(1(a,1),65(a,1)),rewrite(1(12))]. given #95 (T,wt=21): 211 x * a * c0 != y | z * u * d0 != y | x * b = z * u. [para(1(a,1),65(b,1))]. given #96 (T,wt=21): 213 x * y * z * d0 != u | a * c0 != u | x * y * z = b. [para(1(a,1),66(a,1,2))]. given #97 (T,wt=21): 226 x * y * a * a0 != z | x * y * a * c0 != z | d0 = b0. [para(1(a,1),102(a,1)),rewrite(1(11))]. given #98 (A,wt=35): 49 d0 * x * a * c0 * x * a * c0 * x * b = a * c0 * x * a * c0 * x * a * c0 * x. [para(26(a,1),4(a,1,2,2,2,2)),rewrite(1(11),26(12),1(13),26(14),1(24),26(25),1(26),26(27),1(28)),flip(a)]. given #99 (T,wt=21): 233 x * y * a * a0 != z | a * a0 != z | x * y * b = b. [para(1(a,1),199(a,1)),rewrite(1(13))]. given #100 (T,wt=21): 234 x * y * a * a0 != z | c * a0 != z | x * y * b = d. [para(1(a,1),200(a,1)),rewrite(1(13))]. given #101 (T,wt=21): 235 x * y * c * a0 != z | a * a0 != z | x * y * d = b. [para(1(a,1),202(a,1)),rewrite(1(13))]. given #102 (T,wt=21): 245 x * y * c * a0 != z | c * a0 != z | x * y * d = d. [para(1(a,1),208(a,1)),rewrite(1(13))]. given #103 (A,wt=27): 50 a * c0 * x * d0 * x * d0 * x = b * x * d0 * x * d0 * x * d0. [para(4(a,1),26(a,1,2)),flip(a)]. given #104 (T,wt=21): 246 x * y * a * c0 != z | a * c0 != z | x * y * b = b. [para(1(a,1),212(a,1)),rewrite(1(13))]. given #105 (T,wt=21): 313 x * a * a0 * y != z | a * a0 * y != z | x * b = b. [para(18(a,1),67(b,1))]. given #106 (T,wt=21): 314 x * a * a0 * y != z | c * a0 * y != z | x * b = d. [para(22(a,1),67(b,1))]. given #107 (T,wt=21): 320 x * c * a0 * y != z | a * a0 * y != z | x * d = b. [para(22(a,1),68(a,1,2))]. given #108 (A,wt=29): 52 a * a0 != x | y * b * y * b * y * b != x | y * b * y * b * y = b0. [para(4(a,1),19(b,1)),flip(c)]. given #109 (T,wt=21): 325 x * c * a0 * y != z | c * a0 * y != z | x * d = d. [para(22(a,1),69(b,1))]. given #110 (T,wt=21): 335 x * a * c0 * y != z | a * c0 * y != z | x * b = b. [para(26(a,1),71(b,1))]. given #111 (T,wt=21): 401 x * a * a0 != y | z * a * a0 != y | x * b = z * b. [para(5(a,1),198(b,1,2))]. given #112 (T,wt=21): 402 x * a * a0 != y | z * c * a0 != y | z * d = x * b. [para(6(a,1),198(b,1,2)),flip(c)]. given #113 (A,wt=33): 58 x * y * z * y * z * y * z != u | v * y * z * y * z * y != u | x * z = v. [para(4(a,1),10(a,1,2))]. given #114 (T,wt=21): 403 x * a * a0 != y | a * a0 * b0 != y | a * a0 = x * b. [para(18(a,1),198(b,1)),rewrite(5(16)),flip(c)]. given #115 (T,wt=21): 404 x * a * a0 != y | c * a0 * b0 != y | c * a0 = x * b. [para(22(a,1),198(b,1)),rewrite(6(16)),flip(c)]. given #116 (T,wt=21): 405 x * a * a0 != y | a * c0 * b0 != y | a * c0 = x * b. [para(26(a,1),198(b,1)),rewrite(7(16)),flip(c)]. given #117 (T,wt=21): 422 x * c * a0 != y | z * c * a0 != y | x * d = z * d. [para(6(a,1),207(b,1,2))]. given #118 (A,wt=29): 59 x * y * x * y * x * y != z | u * y * x * y * x != z | y * x = u. [para(4(a,1),10(a,1))]. given #119 (T,wt=21): 423 x * c * a0 != y | a * a0 * b0 != y | a * a0 = x * d. [para(18(a,1),207(b,1)),rewrite(5(16)),flip(c)]. given #120 (T,wt=21): 424 x * c * a0 != y | c * a0 * b0 != y | c * a0 = x * d. [para(22(a,1),207(b,1)),rewrite(6(16)),flip(c)]. given #121 (T,wt=21): 425 x * c * a0 != y | a * c0 * b0 != y | a * c0 = x * d. [para(26(a,1),207(b,1)),rewrite(7(16)),flip(c)]. given #122 (T,wt=21): 448 x * a * c0 != y | z * a * c0 != y | x * b = z * b. [para(7(a,1),211(b,1,2))]. given #123 (A,wt=33): 60 x * y * z * u * z * u * z != v | z * u * z * u * z * u != v | x * y = u. [para(4(a,1),10(b,1))]. given #124 (T,wt=21): 449 x * a * c0 != y | a * a0 * d0 != y | a * a0 = x * b. [para(18(a,1),211(b,1)),rewrite(5(16)),flip(c)]. given #125 (T,wt=21): 450 x * a * c0 != y | c * a0 * d0 != y | c * a0 = x * b. [para(22(a,1),211(b,1)),rewrite(6(16)),flip(c)]. given #126 (T,wt=21): 451 x * a * c0 != y | a * c0 * d0 != y | a * c0 = x * b. [para(26(a,1),211(b,1)),rewrite(7(16)),flip(c)]. given #127 (T,wt=23): 184 d0 * a0 * c0 * a0 * c0 * a0 = b0 * c0 * a0 * c0 * a0 * c0. [hyper(47,a,14,a,b,18,a)]. given #128 (A,wt=29): 74 c * a0 != x | y * d * y * d * y * d != x | y * d * y * d * y = b0. [para(4(a,1),23(b,1)),flip(c)]. given #129 (T,wt=23): 370 a0 * d0 * b0 * d0 * b0 * d0 = c0 * b0 * d0 * b0 * d0 * b0. [hyper(2,a,26,a(flip),b,39,a(flip)),flip(a)]. given #130 (T,wt=25): 247 x * y * z * u * v != w | x * y * z * u * v6 != w | v = v6. [para(1(a,1),30(a,1,2,2)),rewrite(1(7))]. given #131 (T,wt=25): 250 x * y * a * a0 * z != u | x * y * b * v != u | b0 * z = v. [para(18(a,1),30(a,1,2,2))]. given #132 (T,wt=25): 251 x * y * c * a0 * z != u | x * y * d * v != u | b0 * z = v. [para(22(a,1),30(a,1,2,2))]. given #133 (A,wt=29): 76 a * c0 != x | y * b * y * b * y * b != x | y * b * y * b * y = d0. [para(4(a,1),27(b,1)),flip(c)]. given #134 (T,wt=25): 252 x * y * a * c0 * z != u | x * y * b * v != u | d0 * z = v. [para(26(a,1),30(a,1,2,2))]. given #135 (T,wt=25): 259 x * a * a0 * y != z | x * a * a0 * u != z | b0 * y = b0 * u. [para(18(a,1),40(b,1,2))]. given #136 (T,wt=25): 260 x * a * a0 * y != z | x * a * c0 * u != z | d0 * u = b0 * y. [para(26(a,1),40(b,1,2)),flip(c)]. given #137 (T,wt=25): 274 x * c * a0 * y != z | x * c * a0 * u != z | b0 * y = b0 * u. [para(22(a,1),46(b,1,2))]. given #138 (A,wt=35): 79 x * y * y * x * y * y * x * y * z = y * x * y * y * x * y * y * x * z. [para(11(a,1),1(a,1,1)),rewrite(1(8),1(7),1(6),1(5),1(4),1(3),1(2),1(15),1(14),1(13),1(12),1(11),1(10)),flip(a)]. given #139 (T,wt=25): 279 x * a * c0 * y != z | x * a * c0 * u != z | d0 * y = d0 * u. [para(26(a,1),51(b,1,2))]. given #140 (T,wt=25): 282 x * y * z * u * v != w | v6 * v != w | x * y * z * u = v6. [para(1(a,1),56(a,1,2,2))]. given #141 (T,wt=25): 283 x * y * z * u != v | w * v6 * u != v | x * y * z = w * v6. [para(1(a,1),56(b,1))]. given #142 (T,wt=25): 286 x * y * a * a0 * z != u | v * b0 * z != u | x * y * b = v. [para(18(a,1),56(a,1,2,2))]. given #143 (A,wt=35): 80 x * y * z * z * y * z * z * y * z = x * z * y * z * z * y * z * z * y. [para(11(a,1),1(a,2,2)),rewrite(1(8))]. given #144 (T,wt=25): 287 x * y * z * b0 * u != v | a * a0 * u != v | x * y * z = b. [para(18(a,1),56(b,1))]. given #145 (T,wt=25): 288 x * y * c * a0 * z != u | v * b0 * z != u | x * y * d = v. [para(22(a,1),56(a,1,2,2))]. given #146 (T,wt=25): 289 x * y * z * b0 * u != v | c * a0 * u != v | x * y * z = d. [para(22(a,1),56(b,1))]. given #147 (T,wt=25): 290 x * y * a * c0 * z != u | v * d0 * z != u | x * y * b = v. [para(26(a,1),56(a,1,2,2))]. given #148 (A,wt=31): 81 b0 * a * a0 * b0 * a * a0 * b0 * b = a * a0 * b0 * a * a0 * b0 * a * a0. [para(5(a,1),11(a,1,2,2,2,2,2,2)),rewrite(18(12),18(15),18(26),18(29)),flip(a)]. given #149 (T,wt=25): 291 x * y * z * d0 * u != v | a * c0 * u != v | x * y * z = b. [para(26(a,1),56(b,1))]. given #150 (T,wt=25): 299 x * a * a0 * y != z | u * v * b0 * y != z | x * b = u * v. [para(18(a,1),57(a,1,2))]. given #151 (T,wt=25): 300 x * c * a0 * y != z | u * v * b0 * y != z | x * d = u * v. [para(22(a,1),57(a,1,2))]. given #152 (T,wt=25): 301 x * a * c0 * y != z | u * v * d0 * y != z | x * b = u * v. [para(26(a,1),57(a,1,2))]. given #153 (A,wt=31): 82 b0 * b * a * a0 * b * a * a0 * b = a * a0 * b * a * a0 * b * a * a0. [para(5(a,1),11(a,2,2,2,2,2,2,2)),rewrite(18(10),18(13),18(27),18(30))]. given #154 (T,wt=25): 342 x * y * z * a * a0 != u | x * y * z * b * v != u | b0 = v. [para(1(a,1),99(a,1,2)),rewrite(1(11))]. given #155 (T,wt=25): 345 x * y * a * a0 != z | x * y * a * a0 * u != z | b0 * u = b0. [para(18(a,1),99(b,1,2,2)),flip(c)]. given #156 (T,wt=25): 346 x * y * a * a0 != z | x * y * a * c0 * u != z | d0 * u = b0. [para(26(a,1),99(b,1,2,2)),flip(c)]. given #157 (T,wt=25): 356 x * y * z * c * a0 != u | x * y * z * d * v != u | b0 = v. [para(1(a,1),132(a,1,2)),rewrite(1(11))]. given #158 (A,wt=31): 83 c * a0 * b0 * c * a0 * b0 * c * a0 = b0 * c * a0 * b0 * c * a0 * b0 * d. [para(6(a,1),11(a,1,2,2,2,2,2,2)),rewrite(22(12),22(15),22(26),22(29))]. given #159 (T,wt=25): 359 x * y * c * a0 != z | x * y * c * a0 * u != z | b0 * u = b0. [para(22(a,1),132(b,1,2,2)),flip(c)]. given #160 (T,wt=25): 364 x * y * z * a * c0 != u | x * y * z * b * v != u | d0 = v. [para(1(a,1),137(a,1,2)),rewrite(1(11))]. given #161 (T,wt=25): 367 x * y * a * c0 != z | x * y * a * a0 * u != z | b0 * u = d0. [para(18(a,1),137(b,1,2,2)),flip(c)]. given #162 (T,wt=25): 368 x * y * a * c0 != z | x * y * a * c0 * u != z | d0 * u = d0. [para(26(a,1),137(b,1,2,2)),flip(c)]. given #163 (A,wt=31): 84 b0 * d * c * a0 * d * c * a0 * d = c * a0 * d * c * a0 * d * c * a0. [para(6(a,1),11(a,2,2,2,2,2,2,2)),rewrite(22(10),22(13),22(27),22(30))]. given #164 (T,wt=25): 398 x * y * z * a * a0 != u | v * b0 != u | x * y * z * b = v. [para(1(a,1),197(a,1,2)),rewrite(1(13))]. given #165 (T,wt=25): 399 x * y * a * a0 != z | u * v * b0 != z | x * y * b = u * v. [para(1(a,1),197(b,1))]. given #166 (T,wt=25): 400 x * a * a0 != y | z * u * v * b0 != y | z * u * v = x * b. [para(1(a,1),198(b,1,2)),flip(c)]. given #167 (T,wt=25): 418 x * y * z * u * b0 != v | a * a0 != v | x * y * z * u = b. [para(1(a,1),201(a,1,2,2))]. given #168 (A,wt=31): 85 d0 * a * c0 * d0 * a * c0 * d0 * b = a * c0 * d0 * a * c0 * d0 * a * c0. [para(7(a,1),11(a,1,2,2,2,2,2,2)),rewrite(26(12),26(15),26(26),26(29)),flip(a)]. given #169 (T,wt=25): 419 x * y * z * c * a0 != u | v * b0 != u | x * y * z * d = v. [para(1(a,1),206(a,1,2)),rewrite(1(13))]. given #170 (T,wt=25): 420 x * y * c * a0 != z | u * v * b0 != z | x * y * d = u * v. [para(1(a,1),206(b,1))]. given #171 (T,wt=25): 421 x * c * a0 != y | z * u * v * b0 != y | z * u * v = x * d. [para(1(a,1),207(b,1,2)),flip(c)]. given #172 (T,wt=25): 426 x * y * z * u * b0 != v | c * a0 != v | x * y * z * u = d. [para(1(a,1),209(a,1,2,2))]. given #173 (A,wt=31): 86 d0 * b * a * c0 * b * a * c0 * b = a * c0 * b * a * c0 * b * a * c0. [para(7(a,1),11(a,2,2,2,2,2,2,2)),rewrite(26(10),26(13),26(27),26(30))]. given #174 (T,wt=25): 445 x * y * z * a * c0 != u | v * d0 != u | x * y * z * b = v. [para(1(a,1),210(a,1,2)),rewrite(1(13))]. given #175 (T,wt=25): 446 x * y * a * c0 != z | u * v * d0 != z | x * y * b = u * v. [para(1(a,1),210(b,1))]. given #176 (T,wt=25): 447 x * a * c0 != y | z * u * v * d0 != y | z * u * v = x * b. [para(1(a,1),211(b,1,2)),flip(c)]. given #177 (T,wt=25): 452 x * y * z * u * d0 != v | a * c0 != v | x * y * z * u = b. [para(1(a,1),213(a,1,2,2))]. given #178 (A,wt=35): 87 a * a0 * x * x * b0 * x * x * b0 * x = b * x * b0 * x * x * b0 * x * x * b0. [para(11(a,1),18(a,1,2)),flip(a)]. given #179 (T,wt=25): 453 x * y * z * a * a0 != u | x * y * z * a * c0 != u | d0 = b0. [para(1(a,1),226(a,1,2)),rewrite(1(12))]. given #180 (T,wt=25): 454 x * y * z * a * a0 != u | a * a0 != u | x * y * z * b = b. [para(1(a,1),233(a,1,2)),rewrite(1(14))]. given #181 (T,wt=25): 455 x * y * z * a * a0 != u | c * a0 != u | x * y * z * b = d. [para(1(a,1),234(a,1,2)),rewrite(1(14))]. given #182 (T,wt=25): 456 x * y * z * c * a0 != u | a * a0 != u | x * y * z * d = b. [para(1(a,1),235(a,1,2)),rewrite(1(14))]. given #183 (A,wt=35): 88 b * x * b0 * b0 * x * b0 * b0 * x * b0 = a * a0 * x * b0 * b0 * x * b0 * b0 * x. [para(11(a,2),18(a,1,2))]. given #184 (T,wt=25): 457 x * y * z * c * a0 != u | c * a0 != u | x * y * z * d = d. [para(1(a,1),245(a,1,2)),rewrite(1(14))]. given #185 (T,wt=25): 475 x * y * z * a * c0 != u | a * c0 != u | x * y * z * b = b. [para(1(a,1),246(a,1,2)),rewrite(1(14))]. given #186 (T,wt=25): 476 x * y * a * a0 * z != u | a * a0 * z != u | x * y * b = b. [para(1(a,1),313(a,1)),rewrite(1(15))]. given #187 (T,wt=25): 482 x * y * a * a0 * z != u | c * a0 * z != u | x * y * b = d. [para(1(a,1),314(a,1)),rewrite(1(15))]. given #188 (A,wt=31): 89 a0 * a * a0 * a0 * a * a0 * a0 * a = a * a0 * a0 * a * a0 * a0 * a * a0. [para(11(a,1),18(a,2)),rewrite(18(15)),flip(a)]. given #189 (T,wt=25): 488 x * y * c * a0 * z != u | a * a0 * z != u | x * y * d = b. [para(1(a,1),320(a,1)),rewrite(1(15))]. given #190 (T,wt=25): 495 x * y * c * a0 * z != u | c * a0 * z != u | x * y * d = d. [para(1(a,1),325(a,1)),rewrite(1(15))]. given #191 (T,wt=25): 501 x * y * a * c0 * z != u | a * c0 * z != u | x * y * b = b. [para(1(a,1),335(a,1)),rewrite(1(15))]. given #192 (T,wt=25): 507 x * y * a * a0 != z | u * a * a0 != z | x * y * b = u * b. [para(1(a,1),401(a,1)),rewrite(1(14))]. given #193 (A,wt=35): 90 a * a0 * x * a0 * a0 * x * a0 * a0 * x = a * x * a0 * a0 * x * a0 * a0 * x * a0. [para(11(a,2),18(a,2,2)),rewrite(18(14))]. given #194 (T,wt=25): 508 x * y * a * a0 != z | u * c * a0 != z | x * y * b = u * d. [para(1(a,1),402(a,1)),rewrite(1(16)),flip(c)]. given #195 (T,wt=25): 509 x * a * a0 != y | z * u * c * a0 != y | z * u * d = x * b. [para(1(a,1),402(b,1)),rewrite(1(14))]. given #196 (T,wt=25): 513 x * y * a * a0 != z | a * a0 * b0 != z | a * a0 = x * y * b. [para(1(a,1),403(a,1)),rewrite(1(18))]. given #197 (T,wt=25): 514 x * y * a * a0 != z | c * a0 * b0 != z | c * a0 = x * y * b. [para(1(a,1),404(a,1)),rewrite(1(18))]. given #198 (A,wt=35): 91 c * a0 * x * x * b0 * x * x * b0 * x = d * x * b0 * x * x * b0 * x * x * b0. [para(11(a,1),22(a,1,2)),flip(a)]. given #199 (T,wt=25): 515 x * y * a * a0 != z | a * c0 * b0 != z | a * c0 = x * y * b. [para(1(a,1),405(a,1)),rewrite(1(18))]. given #200 (T,wt=25): 516 x * y * c * a0 != z | u * c * a0 != z | x * y * d = u * d. [para(1(a,1),422(a,1)),rewrite(1(14))]. given #201 (T,wt=25): 518 x * y * c * a0 != z | a * a0 * b0 != z | a * a0 = x * y * d. [para(1(a,1),423(a,1)),rewrite(1(18))]. given #202 (T,wt=25): 519 x * y * c * a0 != z | c * a0 * b0 != z | c * a0 = x * y * d. [para(1(a,1),424(a,1)),rewrite(1(18))]. given #203 (A,wt=35): 92 d * x * b0 * b0 * x * b0 * b0 * x * b0 = c * a0 * x * b0 * b0 * x * b0 * b0 * x. [para(11(a,2),22(a,1,2))]. given #204 (T,wt=25): 520 x * y * c * a0 != z | a * c0 * b0 != z | a * c0 = x * y * d. [para(1(a,1),425(a,1)),rewrite(1(18))]. given #205 (T,wt=25): 521 x * y * a * c0 != z | u * a * c0 != z | x * y * b = u * b. [para(1(a,1),448(a,1)),rewrite(1(14))]. given #206 (T,wt=25): 528 x * y * a * c0 != z | a * a0 * d0 != z | a * a0 = x * y * b. [para(1(a,1),449(a,1)),rewrite(1(18))]. given #207 (T,wt=25): 529 x * y * a * c0 != z | c * a0 * d0 != z | c * a0 = x * y * b. [para(1(a,1),450(a,1)),rewrite(1(18))]. given #208 (A,wt=35): 93 c * a0 * x * a0 * a0 * x * a0 * a0 * x = c * x * a0 * a0 * x * a0 * a0 * x * a0. [para(11(a,2),22(a,2,2)),rewrite(22(14))]. given #209 (T,wt=25): 530 x * y * a * c0 != z | a * c0 * d0 != z | a * c0 = x * y * b. [para(1(a,1),451(a,1)),rewrite(1(18))]. given #210 (T,wt=25): 664 x * y * z * u != v | a * a0 * u != v | a * a0 = x * y * z. [para(18(a,1),283(b,1)),rewrite(5(14)),flip(c)]. given #211 (T,wt=25): 667 x * y * z * u != v | c * a0 * u != v | c * a0 = x * y * z. [para(22(a,1),283(b,1)),rewrite(6(14)),flip(c)]. given #212 (T,wt=25): 670 x * y * z * u != v | a * c0 * u != v | a * c0 = x * y * z. [para(26(a,1),283(b,1)),rewrite(7(14)),flip(c)]. given #213 (A,wt=31): 94 c * a0 * c * c * a0 * c * c * a0 = a0 * c * c * a0 * c * c * a0 * c. [para(11(a,2),22(a,2)),rewrite(22(15))]. given #214 (T,wt=25): 713 x * a * a0 * y != z | u * a * a0 * y != z | x * b = u * b. [para(18(a,1),299(b,1,2))]. given #215 (T,wt=25): 714 x * a * a0 * y != z | a * a0 * b0 * y != z | a * a0 = x * b. [para(18(a,1),299(b,1)),rewrite(5(18)),flip(c)]. given #216 (T,wt=25): 715 x * a * a0 * y != z | u * c * a0 * y != z | u * d = x * b. [para(22(a,1),299(b,1,2)),flip(c)]. given #217 (T,wt=25): 716 x * a * a0 * y != z | c * a0 * b0 * y != z | c * a0 = x * b. [para(22(a,1),299(b,1)),rewrite(6(18)),flip(c)]. given #218 (A,wt=35): 95 a * c0 * x * x * d0 * x * x * d0 * x = b * x * d0 * x * x * d0 * x * x * d0. [para(11(a,1),26(a,1,2)),flip(a)]. given #219 (T,wt=25): 717 x * a * a0 * y != z | a * c0 * b0 * y != z | a * c0 = x * b. [para(26(a,1),299(b,1)),rewrite(7(18)),flip(c)]. given #220 (T,wt=25): 722 x * c * a0 * y != z | a * a0 * b0 * y != z | a * a0 = x * d. [para(18(a,1),300(b,1)),rewrite(5(18)),flip(c)]. given #221 (T,wt=25): 723 x * c * a0 * y != z | u * c * a0 * y != z | x * d = u * d. [para(22(a,1),300(b,1,2))]. given #222 (T,wt=25): 724 x * c * a0 * y != z | c * a0 * b0 * y != z | c * a0 = x * d. [para(22(a,1),300(b,1)),rewrite(6(18)),flip(c)]. given #223 (A,wt=35): 96 a * c0 * x * d0 * d0 * x * d0 * d0 * x = b * x * d0 * d0 * x * d0 * d0 * x * d0. [para(11(a,2),26(a,1,2)),flip(a)]. given #224 (T,wt=25): 725 x * c * a0 * y != z | a * c0 * b0 * y != z | a * c0 = x * d. [para(26(a,1),300(b,1)),rewrite(7(18)),flip(c)]. given #225 (T,wt=25): 730 x * a * c0 * y != z | a * a0 * d0 * y != z | a * a0 = x * b. [para(18(a,1),301(b,1)),rewrite(5(18)),flip(c)]. given #226 (T,wt=25): 731 x * a * c0 * y != z | c * a0 * d0 * y != z | c * a0 = x * b. [para(22(a,1),301(b,1)),rewrite(6(18)),flip(c)]. given #227 (T,wt=25): 732 x * a * c0 * y != z | u * a * c0 * y != z | x * b = u * b. [para(26(a,1),301(b,1,2))]. given #228 (A,wt=31): 97 c0 * a * c0 * c0 * a * c0 * c0 * a = a * c0 * c0 * a * c0 * c0 * a * c0. [para(11(a,1),26(a,2)),rewrite(26(15)),flip(a)]. given #229 (T,wt=25): 733 x * a * c0 * y != z | a * c0 * d0 * y != z | a * c0 = x * b. [para(26(a,1),301(b,1)),rewrite(7(18)),flip(c)]. given #230 (T,wt=27): 111 x * y * x * y * x * y * y = y * y * x * y * x * y * x. [para(4(a,1),12(a,1,2)),flip(a)]. given #231 (T,wt=27): 112 b * x * b * x * b * x * b0 = x * b * x * b * x * a * a0. [para(5(a,1),12(a,1,2,2,2,2,2)),flip(a)]. given #232 (T,wt=27): 113 d * x * d * x * d * x * b0 = x * d * x * d * x * c * a0. [para(6(a,1),12(a,1,2,2,2,2,2)),flip(a)]. given #233 (A,wt=35): 98 a * c0 * x * c0 * c0 * x * c0 * c0 * x = a * x * c0 * c0 * x * c0 * c0 * x * c0. [para(11(a,2),26(a,2,2)),rewrite(26(14))]. given #234 (T,wt=27): 114 b * x * b * x * b * x * d0 = x * b * x * b * x * a * c0. [para(7(a,1),12(a,1,2,2,2,2,2)),flip(a)]. given #235 (T,wt=27): 117 b0 * a * a0 * a * a0 * b * x = a * a0 * a * a0 * a * a0 * x. [para(12(a,1),18(a,1)),rewrite(18(9),18(11),18(20),18(22))]. given #236 (T,wt=27): 120 b0 * c * a0 * c * a0 * d * x = c * a0 * c * a0 * c * a0 * x. [para(12(a,1),22(a,1)),rewrite(22(9),22(11),22(20),22(22))]. given #237 (T,wt=27): 123 d0 * a * c0 * a * c0 * b * x = a * c0 * a * c0 * a * c0 * x. [para(12(a,1),26(a,1)),rewrite(26(9),26(11),26(20),26(22))]. given #238 (A,wt=33): 100 x * a * a0 != y | x * z * b * z * b * z * b != y | z * b * z * b * z = b0. [para(4(a,1),33(b,1,2)),flip(c)]. given #239 (T,wt=27): 238 b * a * a0 * a * a0 * a * a0 = a * a0 * a * a0 * a * a0 * b. [para(21(a,1),18(a,1,2))]. given #240 (T,wt=27): 239 d * a * a0 * a * a0 * a * a0 = c * a0 * a * a0 * a * a0 * b. [para(21(a,1),22(a,1,2))]. given #241 (T,wt=27): 265 a * c0 * a * c0 * a * c0 * b = b * a * c0 * a * c0 * a * c0. [para(29(a,1),26(a,1,2)),flip(a)]. given #242 (T,wt=27): 407 d * c * a0 * c * a0 * c * a0 = c * a0 * c * a0 * c * a0 * d. [para(6(a,1),44(a,1,2,2,2,2,2)),rewrite(22(10),22(12),22(22),22(24))]. given #243 (A,wt=29): 101 x * a * a0 != y | b * x * b * x * b * x != y | x * b * x * b = b0. [para(4(a,1),33(b,1)),flip(c)]. given #244 (T,wt=27): 431 a * a0 * c * a0 * c * a0 * d = b * a0 * c * a0 * c * a0 * c. [para(45(a,1),18(a,1,2)),flip(a)]. given #245 (T,wt=27): 432 d * a0 * c * a0 * c * a0 * c = c * a0 * c * a0 * c * a0 * d. [para(45(a,1),22(a,1,2))]. given #246 (T,wt=27): 531 d0 * a0 * c0 * a0 * c0 * a0 * x = b0 * c0 * a0 * c0 * a0 * c0 * x. [para(184(a,1),1(a,1,1)),rewrite(1(12),1(11),1(10),1(9),1(8),1(23),1(22),1(21),1(20)),flip(a)]. given #247 (T,wt=27): 548 a0 * d0 * b0 * d0 * b0 * d0 * x = c0 * b0 * d0 * b0 * d0 * b0 * x. [para(370(a,1),1(a,1,1)),rewrite(1(12),1(11),1(10),1(9),1(8),1(23),1(22),1(21),1(20)),flip(a)]. given #248 (A,wt=31): 105 x * y * z * y * z * y * z * u = x * z * y * z * y * z * y * u. [para(12(a,1),1(a,2,2)),rewrite(1(7))]. given #249 (T,wt=27): 896 b0 * a * a0 * a * a0 * a * a0 = a * a0 * a * a0 * a * a0 * b0. [para(111(a,1),18(a,1)),rewrite(18(9),18(11),21(12),18(22),18(24))]. given #250 (T,wt=27): 897 a0 * a0 * a * a0 * a * a0 * a = a * a0 * a * a0 * a * a0 * a0. [para(111(a,1),18(a,2)),rewrite(18(13)),flip(a)]. given #251 (T,wt=27): 900 c * a0 * c * a0 * c * a0 * b0 = b0 * a0 * c * a0 * c * a0 * c. [para(111(a,1),22(a,1)),rewrite(22(9),22(11),45(12),22(22),22(24)),flip(a)]. given #252 (T,wt=27): 903 d0 * a * c0 * a * c0 * a * c0 = a * c0 * a * c0 * a * c0 * d0. [para(111(a,1),26(a,1)),rewrite(26(9),26(11),29(12),26(22),26(24))]. given #253 (A,wt=33): 106 x * y * x * y * x * y * z != u | y * v != u | x * y * x * y * x * z = v. [para(12(a,1),2(a,1))]. given #254 (T,wt=27): 905 c0 * c0 * a * c0 * a * c0 * a = a * c0 * a * c0 * a * c0 * c0. [para(111(a,1),26(a,2)),rewrite(26(13)),flip(a)]. given #255 (T,wt=27): 1025 d * b * d * b * d * a * a0 = b * d * b * d * b * c * a0. [para(6(a,1),112(a,1,2,2,2,2,2)),flip(a)]. given #256 (T,wt=27): 1030 d0 * a * c0 * a * c0 * a * a0 = a * c0 * a * c0 * a * c0 * b0. [para(112(a,1),26(a,1)),rewrite(26(10),26(12),26(22),26(24))]. given #257 (T,wt=27): 1127 b0 * a * a0 * a * a0 * a * c0 = a * a0 * a * a0 * a * a0 * d0. [para(114(a,1),18(a,1)),rewrite(18(10),18(12),18(22),18(24))]. given #258 (A,wt=33): 107 x * y * x * y * x * y * z != u | v * x * y * x * y * x * z != u | y = v. [para(12(a,1),3(a,1))]. given #259 (T,wt=27): 1231 b * a0 * a * a0 * a * a0 * a = a * a0 * a * a0 * a * a0 * b. [para(4(a,1),238(a,1,2))]. given #260 (T,wt=27): 1248 d * a0 * a * a0 * a * a0 * a = c * a0 * a * a0 * a * a0 * b. [para(4(a,1),239(a,1,2))]. given #261 (T,wt=27): 1269 c0 * a * c0 * a * c0 * a * b = b * a * c0 * a * c0 * a * c0. [para(265(a,1),12(a,1)),flip(a)]. given #262 (T,wt=27): 1327 d0 * c0 * a0 * c0 * a0 * c0 * a0 = b0 * c0 * a0 * c0 * a0 * c0 * c0. [para(4(a,1),531(a,1,2))]. given #263 (A,wt=33): 108 x * y * z * y * z * y * u != v | y * z * y * z * y * z * u != v | x = z. [para(12(a,1),3(b,1))]. given #264 (T,wt=27): 1348 a0 * b0 * d0 * b0 * d0 * b0 * d0 = c0 * b0 * d0 * b0 * d0 * b0 * b0. [para(4(a,1),548(a,1,2))]. given #265 (T,wt=27): 1384 b0 * a0 * a * a0 * a * a0 * a = a * a0 * a * a0 * a * a0 * b0. [para(4(a,1),896(a,1,2))]. given #266 (T,wt=27): 1405 a0 * c * a0 * c * a0 * c * b0 = b0 * a0 * c * a0 * c * a0 * c. [para(900(a,1),12(a,1)),flip(a)]. given #267 (T,wt=27): 1421 d0 * c0 * a * c0 * a * c0 * a = a * c0 * a * c0 * a * c0 * d0. [para(4(a,1),903(a,1,2))]. given #268 (A,wt=35): 109 x * y * x * y * x * y * y * x * y = y * x * y * y * x * y * x * y * x. [para(4(a,1),12(a,1,2,2,2)),flip(a)]. given #269 (T,wt=29): 134 x * c * a0 != y | d * x * d * x * d * x != y | x * d * x * d = b0. [para(4(a,1),34(b,1)),flip(c)]. given #270 (T,wt=29): 139 x * a * c0 != y | b * x * b * x * b * x != y | x * b * x * b = d0. [para(4(a,1),35(b,1)),flip(c)]. given #271 (T,wt=29): 145 a0 * a * a0 * a * a0 * a != x | b * y != x | b0 * a * a0 * a * a0 = y. [para(4(a,1),36(a,1))]. given #272 (T,wt=29): 151 a0 * a * a0 * a * a0 * a != x | y * b0 * a * a0 * a * a0 != x | b = y. [para(4(a,1),37(a,1))]. given #273 (A,wt=31): 110 x * y * y * x * y * x * y * x = y * x * y * x * y * x * x * y. [para(4(a,1),12(a,1,2,2))]. given #274 (T,wt=29): 153 a * a0 * x * b0 * x * b0 != y | b0 * x * b0 * x * b0 * x != y | b = x. [para(4(a,1),37(b,1))]. given #275 (T,wt=29): 162 a0 * c * a0 * c * a0 * c != x | d * y != x | b0 * c * a0 * c * a0 = y. [para(4(a,1),41(a,1))]. given #276 (T,wt=29): 167 a0 * c * a0 * c * a0 * c != x | y * b0 * c * a0 * c * a0 != x | d = y. [para(4(a,1),42(a,1))]. given #277 (T,wt=29): 169 c * a0 * x * b0 * x * b0 != y | b0 * x * b0 * x * b0 * x != y | d = x. [para(4(a,1),42(b,1))]. given #278 (A,wt=33): 115 x * y * x * y * x * y * z != u | y * x * v != u | y * x * y * x * z = v. [para(12(a,1),9(a,1))]. given #279 (T,wt=29): 174 c0 * a * c0 * a * c0 * a != x | b * y != x | d0 * a * c0 * a * c0 = y. [para(4(a,1),47(a,1))]. given #280 (T,wt=29): 179 c0 * a * c0 * a * c0 * a != x | y * d0 * a * c0 * a * c0 != x | b = y. [para(4(a,1),48(a,1))]. given #281 (T,wt=29): 181 a * c0 * x * d0 * x * d0 != y | d0 * x * d0 * x * d0 * x != y | b = x. [para(4(a,1),48(b,1))]. given #282 (T,wt=29): 192 a * a0 != x | a0 * a * a0 * a * a0 * a != x | b0 * a * a0 * a * a0 = b0. [para(4(a,1),54(b,1))]. given #283 (A,wt=31): 116 b * x * b0 * x * b0 * x * b0 * y = a * a0 * x * b0 * x * b0 * x * y. [para(12(a,1),18(a,1,2))]. given #284 (T,wt=29): 195 a * a0 != x | c0 * a * c0 * a * c0 * a != x | d0 * a * c0 * a * c0 = b0. [para(4(a,1),55(b,1))]. given #285 (T,wt=29): 203 a * a0 * a * a0 * a * a0 != x | b0 * y != x | a * a0 * a * a0 * b = y. [para(5(a,1),15(a,1,2,2,2,2)),rewrite(18(9),18(11),18(22),18(24))]. given #286 (T,wt=29): 204 c * a0 * c * a0 * c * a0 != x | b0 * y != x | c * a0 * c * a0 * d = y. [para(6(a,1),15(a,1,2,2,2,2)),rewrite(22(9),22(11),22(22),22(24))]. given #287 (T,wt=29): 205 a * c0 * a * c0 * a * c0 != x | d0 * y != x | a * c0 * a * c0 * b = y. [para(7(a,1),15(a,1,2,2,2,2)),rewrite(26(9),26(11),26(22),26(24))]. given #288 (A,wt=31): 118 b * x * b * x * b * x * b0 * y = x * b * x * b * x * a * a0 * y. [para(18(a,1),12(a,1,2,2,2,2,2)),flip(a)]. given #289 (T,wt=29): 214 a * a0 * a * a0 * a * a0 != x | y * a * a0 * a * a0 * b != x | b0 = y. [para(5(a,1),16(a,1,2,2,2,2)),rewrite(18(9),18(11),18(19),18(21))]. given #290 (T,wt=29): 215 c * a0 * c * a0 * c * a0 != x | y * c * a0 * c * a0 * d != x | b0 = y. [para(6(a,1),16(a,1,2,2,2,2)),rewrite(22(9),22(11),22(19),22(21))]. given #291 (T,wt=29): 216 a * c0 * a * c0 * a * c0 != x | y * a * c0 * a * c0 * b != x | d0 = y. [para(7(a,1),16(a,1,2,2,2,2)),rewrite(26(9),26(11),26(19),26(21))]. given #292 (T,wt=29): 218 c * a0 != x | a0 * c * a0 * c * a0 * c != x | b0 * c * a0 * c * a0 = b0. [para(4(a,1),75(b,1))]. given #293 (A,wt=31): 119 d * x * b0 * x * b0 * x * b0 * y = c * a0 * x * b0 * x * b0 * x * y. [para(12(a,1),22(a,1,2))]. given #294 (T,wt=29): 221 a * c0 != x | a0 * a * a0 * a * a0 * a != x | b0 * a * a0 * a * a0 = d0. [para(4(a,1),77(b,1))]. given #295 (T,wt=29): 224 a * c0 != x | c0 * a * c0 * a * c0 * a != x | d0 * a * c0 * a * c0 = d0. [para(4(a,1),78(b,1))]. given #296 (T,wt=29): 228 a0 * a * a0 * a * a0 * a != x | c * a0 * a * a0 * a * a0 != x | d = b. [para(4(a,1),154(a,1))]. given #297 (T,wt=29): 230 a * a0 * c * a0 * c * a0 != x | a0 * c * a0 * c * a0 * c != x | d = b. [para(4(a,1),154(b,1))]. given #298 (A,wt=31): 121 d * x * d * x * d * x * b0 * y = x * d * x * d * x * c * a0 * y. [para(22(a,1),12(a,1,2,2,2,2,2)),flip(a)]. given #299 (T,wt=29): 237 a * a0 * a * a0 * a * a0 != x | b0 * a * y != x | a0 * a * a0 * b = y. [para(21(a,1),9(a,1))]. given #300 (T,wt=29): 241 a * a0 * a * a0 * a * a0 != x | y * a0 * a * a0 * b != x | b0 * a = y. [para(21(a,1),10(a,1))]. given #301 (T,wt=29): 249 x * y * x * y * x * y != z | y * x * y * u != z | x * y * x = u. [para(4(a,1),30(a,1))]. given #302 (T,wt=29): 255 a * a0 * a * a0 * a * a0 != x | b0 * a * a0 * y != x | a * a0 * b = y. [para(21(a,1),30(a,1))]. given #303 (A,wt=31): 122 a * c0 * x * d0 * x * d0 * x * y = b * x * d0 * x * d0 * x * d0 * y. [para(12(a,1),26(a,1,2)),flip(a)]. given #304 (T,wt=29): 257 a * a0 * a * a0 * a * a0 != x | a0 * b * y != x | b0 * a * a0 * a = y. [para(4(a,1),40(a,1))]. given #305 (T,wt=29): 262 a * a0 * a * a0 * a * a0 != x | b0 * b * y != x | b0 * a * a0 * b = y. [para(21(a,1),40(a,1))]. given #306 (T,wt=29): 264 a * c0 * a * c0 * a * c0 != x | d0 * a * y != x | c0 * a * c0 * b = y. [para(29(a,1),9(a,1))]. given #307 (T,wt=29): 267 a * c0 * a * c0 * a * c0 != x | y * c0 * a * c0 * b != x | d0 * a = y. [para(29(a,1),10(a,1))]. given #308 (A,wt=31): 124 b * x * b * x * b * x * d0 * y = x * b * x * b * x * a * c0 * y. [para(26(a,1),12(a,1,2,2,2,2,2)),flip(a)]. given #309 (T,wt=29): 270 a * c0 * a * c0 * a * c0 != x | d0 * a * c0 * y != x | a * c0 * b = y. [para(29(a,1),30(a,1))]. given #310 (T,wt=29): 272 c * a0 * c * a0 * c * a0 != x | a0 * d * y != x | b0 * c * a0 * c = y. [para(4(a,1),46(a,1))]. given #311 (T,wt=29): 277 a * c0 * a * c0 * a * c0 != x | c0 * b * y != x | d0 * a * c0 * a = y. [para(4(a,1),51(a,1))]. given #312 (T,wt=29): 281 a * c0 * a * c0 * a * c0 != x | d0 * b * y != x | d0 * a * c0 * b = y. [para(29(a,1),51(a,1))]. given #313 (A,wt=33): 125 a * a0 != x | y * b * y * b * y * b * z != x | y * b * y * b * y * z = b0. [para(12(a,1),19(b,1)),flip(c)]. given #314 (T,wt=29): 285 x * y * x * y * x * y != z | u * x * y * x != z | y * x * y = u. [para(4(a,1),56(a,1))]. given #315 (T,wt=29): 294 a * a0 * a * a0 * a * a0 != x | y * a * a0 * b != x | b0 * a * a0 = y. [para(21(a,1),56(a,1))]. given #316 (T,wt=29): 296 a * c0 * a * c0 * a * c0 != x | y * a * c0 * b != x | d0 * a * c0 = y. [para(29(a,1),56(a,1))]. given #317 (T,wt=29): 311 a * a0 * a * a0 * a * a0 != x | y * b0 * a * a0 * a != x | a0 * b = y. [para(4(a,1),67(a,1))]. given #318 (A,wt=33): 126 x * y * x * y * x * y * z != u | v * y * x * y * x * z != u | y * x = v. [para(12(a,1),10(a,1))]. given #319 (T,wt=29): 316 a * a0 * a * a0 * a * a0 != x | y * b0 * a * a0 * b != x | b0 * b = y. [para(21(a,1),67(a,1))]. given #320 (T,wt=29): 318 x * b0 * x * b0 * x * b0 != y | a * a0 * x * b0 * x != y | b0 * x = b. [para(4(a,1),68(a,1))]. given #321 (T,wt=29): 323 c * a0 * c * a0 * c * a0 != x | y * b0 * c * a0 * c != x | a0 * d = y. [para(4(a,1),69(a,1))]. given #322 (T,wt=29): 328 x * b0 * x * b0 * x * b0 != y | c * a0 * x * b0 * x != y | b0 * x = d. [para(4(a,1),70(a,1))]. given #323 (A,wt=33): 127 c * a0 != x | y * d * y * d * y * d * z != x | y * d * y * d * y * z = b0. [para(12(a,1),23(b,1)),flip(c)]. given #324 (T,wt=29): 331 c * a0 * c * a0 * c * a0 != x | b0 * d * y != x | b0 * c * a0 * d = y. [para(6(a,1),32(a,1,2,2,2,2)),rewrite(22(9),22(11),22(23))]. given #325 (T,wt=29): 333 a * c0 * a * c0 * a * c0 != x | y * d0 * a * c0 * a != x | c0 * b = y. [para(4(a,1),71(a,1))]. given #326 (T,wt=29): 337 a * c0 * a * c0 * a * c0 != x | y * d0 * a * c0 * b != x | d0 * b = y. [para(29(a,1),71(a,1))]. given #327 (T,wt=29): 339 x * d0 * x * d0 * x * d0 != y | a * c0 * x * d0 * x != y | d0 * x = b. [para(4(a,1),72(a,1))]. given #328 (A,wt=33): 128 a * c0 != x | y * b * y * b * y * b * z != x | y * b * y * b * y * z = d0. [para(12(a,1),27(b,1)),flip(c)]. given #329 (T,wt=29): 344 b * x * a * a0 != y | x * b * x * b * x * b != y | x * b * x = b0. [para(4(a,1),99(b,1)),flip(c)]. given #330 (T,wt=29): 349 a0 * a * a0 != x | a * a0 * a * a0 * a * a0 != x | b0 * a * a0 * a = b0. [para(4(a,1),103(b,1))]. given #331 (T,wt=29): 351 b0 * a * a0 != x | a * a0 * a * a0 * a * a0 != x | b0 * a * a0 * b = b0. [para(21(a,1),103(b,1))]. given #332 (T,wt=29): 353 c0 * a * a0 != x | a * c0 * a * c0 * a * c0 != x | d0 * a * c0 * a = b0. [para(4(a,1),104(b,1))]. given #333 (A,wt=33): 129 x * a * a0 != y | b * x * b * x * b * x * z != y | x * b * x * b * z = b0. [para(12(a,1),33(b,1)),flip(c)]. given #334 (T,wt=29): 355 d0 * a * a0 != x | a * c0 * a * c0 * a * c0 != x | d0 * a * c0 * b = b0. [para(29(a,1),104(b,1))]. given #335 (T,wt=29): 358 d * x * c * a0 != y | x * d * x * d * x * d != y | x * d * x = b0. [para(4(a,1),132(b,1)),flip(c)]. given #336 (T,wt=29): 362 a0 * c * a0 != x | c * a0 * c * a0 * c * a0 != x | b0 * c * a0 * c = b0. [para(4(a,1),135(b,1))]. given #337 (T,wt=29): 366 b * x * a * c0 != y | x * b * x * b * x * b != y | x * b * x = d0. [para(4(a,1),137(b,1)),flip(c)]. given #338 (A,wt=35): 130 x * y * y * x * y * x * y * x * z = y * x * y * x * y * x * x * y * z. [para(12(a,1),12(a,1,2,2))]. given #339 (T,wt=29): 384 a0 * a * c0 != x | a * a0 * a * a0 * a * a0 != x | b0 * a * a0 * a = d0. [para(4(a,1),140(b,1))]. given #340 (T,wt=29): 386 b0 * a * c0 != x | a * a0 * a * a0 * a * a0 != x | b0 * a * a0 * b = d0. [para(21(a,1),140(b,1))]. given #341 (T,wt=29): 388 c0 * a * c0 != x | a * c0 * a * c0 * a * c0 != x | d0 * a * c0 * a = d0. [para(4(a,1),141(b,1))]. given #342 (T,wt=29): 390 d0 * a * c0 != x | a * c0 * a * c0 * a * c0 != x | d0 * a * c0 * b = d0. [para(29(a,1),141(b,1))]. given #343 (A,wt=31): 131 x * y * x * y * x * y * y * z = y * y * x * y * x * y * x * z. [para(12(a,1),12(a,1,2)),flip(a)]. given #344 (T,wt=29): 427 a0 * c * a0 * c * a0 * c != x | b0 * y != x | c * a0 * c * a0 * d = y. [para(45(a,1),2(a,1))]. given #345 (T,wt=29): 428 a0 * c * a0 * c * a0 * c != x | y * c * a0 * c * a0 * d != x | b0 = y. [para(45(a,1),3(a,1))]. given #346 (T,wt=29): 430 a0 * c * a0 * c * a0 * c != x | b0 * c * y != x | a0 * c * a0 * d = y. [para(45(a,1),9(a,1))]. given #347 (T,wt=29): 434 a0 * c * a0 * c * a0 * c != x | y * a0 * c * a0 * d != x | b0 * c = y. [para(45(a,1),10(a,1))]. given #348 (A,wt=33): 133 x * c * a0 != y | x * z * d * z * d * z * d != y | z * d * z * d * z = b0. [para(4(a,1),34(b,1,2)),flip(c)]. given #349 (T,wt=29): 438 a0 * c * a0 * c * a0 * c != x | b0 * c * a0 * y != x | c * a0 * d = y. [para(45(a,1),30(a,1))]. given #350 (T,wt=29): 439 a0 * c * a0 * c * a0 * c != x | b0 * d * y != x | b0 * c * a0 * d = y. [para(45(a,1),46(a,1))]. given #351 (T,wt=29): 441 a0 * c * a0 * c * a0 * c != x | y * c * a0 * d != x | b0 * c * a0 = y. [para(45(a,1),56(a,1))]. given #352 (T,wt=29): 443 a0 * c * a0 * c * a0 * c != x | y * b0 * c * a0 * d != x | b0 * d = y. [para(45(a,1),69(a,1))]. given #353 (A,wt=33): 136 x * c * a0 != y | d * x * d * x * d * x * z != y | x * d * x * d * z = b0. [para(12(a,1),34(b,1)),flip(c)]. given #354 (T,wt=29): 444 b0 * c * a0 != x | a0 * c * a0 * c * a0 * c != x | b0 * c * a0 * d = b0. [para(45(a,1),135(b,1))]. given #355 (T,wt=29): 478 a * a0 * a * a0 * a * a0 != x | a * a0 * a * a0 * a != x | a0 * b = b. [para(4(a,1),313(a,1))]. given #356 (T,wt=29): 481 a * a0 * a * a0 * a * a0 != x | a * a0 * a * a0 * b != x | b0 * b = b. [para(21(a,1),313(a,1))]. given #357 (T,wt=29): 484 a * a0 * a * a0 * a * a0 != x | c * a0 * a * a0 * a != x | a0 * b = d. [para(4(a,1),314(a,1))]. given #358 (A,wt=33): 138 x * a * c0 != y | x * z * b * z * b * z * b != y | z * b * z * b * z = d0. [para(4(a,1),35(b,1,2)),flip(c)]. given #359 (T,wt=29): 487 a * a0 * a * a0 * a * a0 != x | c * a0 * a * a0 * b != x | b0 * b = d. [para(21(a,1),314(a,1))]. given #360 (T,wt=29): 490 c * a0 * c * a0 * c * a0 != x | a * a0 * c * a0 * c != x | a0 * d = b. [para(4(a,1),320(a,1))]. given #361 (T,wt=29): 493 a0 * c * a0 * c * a0 * c != x | a * a0 * c * a0 * d != x | b0 * d = b. [para(45(a,1),320(a,1))]. given #362 (T,wt=29): 494 a * a0 != x | b * y * b * y * b * y != x | y * b * y * b * y = b0. [para(4(a,1),52(b,1))]. given #363 (A,wt=33): 142 x * a * c0 != y | b * x * b * x * b * x * z != y | x * b * x * b * z = d0. [para(12(a,1),35(b,1)),flip(c)]. given #364 (T,wt=29): 497 c * a0 * c * a0 * c * a0 != x | c * a0 * c * a0 * c != x | a0 * d = d. [para(4(a,1),325(a,1))]. given #365 (T,wt=29): 500 a0 * c * a0 * c * a0 * c != x | c * a0 * c * a0 * d != x | b0 * d = d. [para(45(a,1),325(a,1))]. given #366 (T,wt=29): 503 a * c0 * a * c0 * a * c0 != x | a * c0 * a * c0 * a != x | c0 * b = b. [para(4(a,1),335(a,1))]. given #367 (T,wt=29): 506 a * c0 * a * c0 * a * c0 != x | a * c0 * a * c0 * b != x | d0 * b = b. [para(29(a,1),335(a,1))]. given #368 (A,wt=35): 143 b0 * b * a * a0 * b * a * a0 * b * x = a * a0 * b * a * a0 * b * a * a0 * x. [hyper(36,a,1,a(flip),b,12,a),rewrite(1(12),1(14),1(28),1(30),1(32))]. given #369 (T,wt=29): 517 c * a0 * c * a0 * c * a0 != x | y * b0 * c * a0 * d != x | b0 * d = y. [para(6(a,1),59(a,1,2,2,2,2)),rewrite(22(9),22(11),22(18))]. given #370 (T,wt=29): 532 b0 * c0 * a0 * c0 * a0 * c0 != x | d0 * y != x | a0 * c0 * a0 * c0 * a0 = y. [para(184(a,1),2(a,1))]. given #371 (T,wt=29): 533 b0 * c0 * a0 * c0 * a0 * c0 != x | y * a0 * c0 * a0 * c0 * a0 != x | d0 = y. [para(184(a,1),3(a,1))]. given #372 (T,wt=29): 535 b0 * c0 * a0 * c0 * a0 * c0 != x | d0 * a0 * y != x | c0 * a0 * c0 * a0 = y. [para(184(a,1),9(a,1))]. given #373 (A,wt=33): 144 a * x * a0 * x * a0 * x * a0 != y | b * z != y | b0 * x * a0 * x * a0 * x = z. [para(4(a,1),36(a,1,2))]. given #374 (T,wt=29): 537 b0 * c0 * a0 * c0 * a0 * c0 != x | y * c0 * a0 * c0 * a0 != x | d0 * a0 = y. [para(184(a,1),10(a,1))]. given #375 (T,wt=29): 539 a0 * c0 * a0 * c0 * a0 * c0 != x | b0 * c0 * a0 * c0 * a0 * c0 != x | d0 = c0. [para(184(a,1),16(b,1)),flip(c)]. given #376 (T,wt=29): 541 b0 * c0 * a0 * c0 * a0 * c0 != x | d0 * a0 * c0 * y != x | a0 * c0 * a0 = y. [para(184(a,1),30(a,1))]. given #377 (T,wt=29): 543 b0 * c0 * a0 * c0 * a0 * c0 != x | y * a0 * c0 * a0 != x | d0 * a0 * c0 = y. [para(184(a,1),56(a,1))]. given #378 (A,wt=33): 146 a * a0 * x != y | z * b * z * b * z * b != y | b0 * x = z * b * z * b * z. [para(4(a,1),36(b,1))]. given #379 (T,wt=29): 547 c * a0 != x | d * y * d * y * d * y != x | y * d * y * d * y = b0. [para(4(a,1),74(b,1))]. given #380 (T,wt=29): 549 c0 * b0 * d0 * b0 * d0 * b0 != x | a0 * y != x | d0 * b0 * d0 * b0 * d0 = y. [para(370(a,1),2(a,1))]. given #381 (T,wt=29): 550 c0 * b0 * d0 * b0 * d0 * b0 != x | y * d0 * b0 * d0 * b0 * d0 != x | a0 = y. [para(370(a,1),3(a,1))]. given #382 (T,wt=29): 552 c0 * b0 * d0 * b0 * d0 * b0 != x | a0 * d0 * y != x | b0 * d0 * b0 * d0 = y. [para(370(a,1),9(a,1))]. given #383 (A,wt=33): 149 a0 * a * a0 * a * a0 * a * x != y | b * z != y | b0 * a * a0 * a * a0 * x = z. [para(12(a,1),36(a,1))]. given #384 (T,wt=29): 554 c0 * b0 * d0 * b0 * d0 * b0 != x | y * b0 * d0 * b0 * d0 != x | a0 * d0 = y. [para(370(a,1),10(a,1))]. given #385 (T,wt=29): 558 a * c0 * b0 * d0 * b0 * d0 != x | c0 * b0 * d0 * b0 * d0 * b0 != x | b = a0. [para(370(a,1),48(b,1))]. given #386 (T,wt=29): 559 d0 * b0 * d0 * b0 * d0 * b0 != x | c0 * b0 * d0 * b0 * d0 * b0 != x | b0 = a0. [para(370(a,1),16(b,1))]. given #387 (T,wt=29): 562 c0 * b0 * d0 * b0 * d0 * b0 != x | a0 * d0 * b0 * y != x | d0 * b0 * d0 = y. [para(370(a,1),30(a,1))]. given #388 (A,wt=33): 150 a * x * a0 * x * a0 * x * a0 != y | z * b0 * x * a0 * x * a0 * x != y | b = z. [para(4(a,1),37(a,1,2))]. given #389 (T,wt=29): 564 c0 * b0 * d0 * b0 * d0 * b0 != x | y * d0 * b0 * d0 != x | a0 * d0 * b0 = y. [para(370(a,1),56(a,1))]. given #390 (T,wt=29): 566 c0 * b0 * d0 * b0 * d0 * b0 != x | a * a0 * d0 * b0 * d0 != x | a0 * d0 = b. [para(370(a,1),68(a,1))]. given #391 (T,wt=29): 567 c0 * b0 * d0 * b0 * d0 * b0 != x | c * a0 * d0 * b0 * d0 != x | a0 * d0 = d. [para(370(a,1),70(a,1))]. given #392 (T,wt=29): 572 x * y * z * u * v * w != v6 | x * y * z * u * v * v7 != v6 | w = v7. [para(1(a,1),247(a,1,2,2,2)),rewrite(1(8))]. given #393 (A,wt=33): 152 a * a0 * x * b0 * x * b0 * x != y | z * x * b0 * x * b0 * x * b0 != y | b = z. [para(4(a,1),37(b,1,2))]. given #394 (T,wt=29): 574 x * y * x * y * x * y != z | y * x * y * x * u != z | y * x = u. [para(4(a,1),247(a,1))]. given #395 (T,wt=29): 575 x * y * z * a * a0 * u != v | x * y * z * b * w != v | b0 * u = w. [para(18(a,1),247(a,1,2,2,2))]. given #396 (T,wt=29): 576 x * y * z * c * a0 * u != v | x * y * z * d * w != v | b0 * u = w. [para(22(a,1),247(a,1,2,2,2))]. given #397 (T,wt=29): 577 x * y * z * a * c0 * u != v | x * y * z * b * w != v | d0 * u = w. [para(26(a,1),247(a,1,2,2,2))]. given #398 (A,wt=33): 155 a0 * a * a0 * a * a0 * a * x != y | z * b0 * a * a0 * a * a0 * x != y | b = z. [para(12(a,1),37(a,1))]. given #399 (T,wt=29): 580 a * a0 * a * a0 * a * a0 != x | b0 * a * a0 * a * y != x | a0 * b = y. [para(21(a,1),247(a,1))]. given #400 (T,wt=29): 582 a * c0 * a * c0 * a * c0 != x | d0 * a * c0 * a * y != x | c0 * b = y. [para(29(a,1),247(a,1))]. given #401 (T,wt=29): 586 a0 * c * a0 * c * a0 * c != x | b0 * c * a0 * c * y != x | a0 * d = y. [para(45(a,1),247(a,1))]. given #402 (T,wt=29): 590 b0 * c0 * a0 * c0 * a0 * c0 != x | d0 * a0 * c0 * a0 * y != x | c0 * a0 = y. [para(184(a,1),247(a,1))]. given #403 (A,wt=33): 156 a * a0 * x * b0 * x * b0 * y != z | b0 * x * b0 * x * b0 * x * y != z | b = x. [para(12(a,1),37(b,1))]. given #404 (T,wt=29): 592 c0 * b0 * d0 * b0 * d0 * b0 != x | a0 * d0 * b0 * d0 * y != x | b0 * d0 = y. [para(370(a,1),247(a,1))]. given #405 (T,wt=29): 594 a0 * a * a0 * a * a0 * a != x | a * a0 * b * y != x | b0 * a * a0 = y. [para(4(a,1),250(a,1))]. given #406 (T,wt=29): 596 x * y * a * a0 * z != u | x * y * a * a0 * v != u | b0 * z = b0 * v. [para(18(a,1),250(b,1,2,2))]. given #407 (T,wt=29): 597 x * y * a * a0 * z != u | x * y * a * c0 * v != u | d0 * v = b0 * z. [para(26(a,1),250(b,1,2,2)),flip(c)]. given #408 (A,wt=35): 158 c * a0 * x * c * a0 * x * c * a0 * x = a0 * x * c * a0 * x * c * a0 * x * c. [para(13(a,2),22(a,2)),rewrite(22(14))]. given #409 (T,wt=29): 601 a0 * c * a0 * c * a0 * c != x | c * a0 * d * y != x | b0 * c * a0 = y. [para(4(a,1),251(a,1))]. given #410 (T,wt=29): 603 x * y * c * a0 * z != u | x * y * c * a0 * v != u | b0 * z = b0 * v. [para(22(a,1),251(b,1,2,2))]. given #411 (T,wt=29): 606 a * c0 != x | b * y * b * y * b * y != x | y * b * y * b * y = d0. [para(4(a,1),76(b,1))]. given #412 (T,wt=29): 608 c0 * a * c0 * a * c0 * a != x | a * c0 * b * y != x | d0 * a * c0 = y. [para(4(a,1),252(a,1))]. given #413 (A,wt=35): 159 x * y * y * x * y * y * x * y * y = y * y * x * y * y * x * y * y * x. [para(11(a,1),13(a,2,2))]. given #414 (T,wt=29): 610 x * y * a * c0 * z != u | x * y * a * c0 * v != u | d0 * z = d0 * v. [para(26(a,1),252(b,1,2,2))]. given #415 (T,wt=29): 635 x * y * z * u * v * w != v6 | v7 * w != v6 | x * y * z * u * v = v7. [para(1(a,1),282(a,1,2,2,2))]. given #416 (T,wt=29): 636 x * y * z * u * v != w | v6 * v7 * v != w | x * y * z * u = v6 * v7. [para(1(a,1),282(b,1))]. given #417 (T,wt=29): 638 x * y * x * y * x * y != z | u * y * x != z | y * x * y * x = u. [para(4(a,1),282(a,1))]. given #418 (A,wt=35): 160 b0 * d * c * a0 * d * c * a0 * d * x = c * a0 * d * c * a0 * d * c * a0 * x. [hyper(41,a,1,a(flip),b,12,a),rewrite(1(12),1(14),1(28),1(30),1(32))]. given #419 (T,wt=29): 639 x * y * z * a * a0 * u != v | w * b0 * u != v | x * y * z * b = w. [para(18(a,1),282(a,1,2,2,2))]. given #420 (T,wt=29): 640 x * y * z * u * b0 * v != w | a * a0 * v != w | x * y * z * u = b. [para(18(a,1),282(b,1))]. given #421 (T,wt=29): 641 x * y * z * c * a0 * u != v | w * b0 * u != v | x * y * z * d = w. [para(22(a,1),282(a,1,2,2,2))]. given #422 (T,wt=29): 642 x * y * z * u * b0 * v != w | c * a0 * v != w | x * y * z * u = d. [para(22(a,1),282(b,1))]. given #423 (A,wt=33): 161 c * x * a0 * x * a0 * x * a0 != y | d * z != y | b0 * x * a0 * x * a0 * x = z. [para(4(a,1),41(a,1,2))]. given #424 (T,wt=29): 643 x * y * z * a * c0 * u != v | w * d0 * u != v | x * y * z * b = w. [para(26(a,1),282(a,1,2,2,2))]. given #425 (T,wt=29): 644 x * y * z * u * d0 * v != w | a * c0 * v != w | x * y * z * u = b. [para(26(a,1),282(b,1))]. given #426 (T,wt=29): 647 a * a0 * a * a0 * a * a0 != x | y * a0 * b != x | b0 * a * a0 * a = y. [para(21(a,1),282(a,1))]. given #427 (T,wt=29): 649 a * c0 * a * c0 * a * c0 != x | y * c0 * b != x | d0 * a * c0 * a = y. [para(29(a,1),282(a,1))]. given #428 (A,wt=33): 163 c * a0 * x != y | z * d * z * d * z * d != y | b0 * x = z * d * z * d * z. [para(4(a,1),41(b,1))]. given #429 (T,wt=29): 653 a0 * c * a0 * c * a0 * c != x | y * a0 * d != x | b0 * c * a0 * c = y. [para(45(a,1),282(a,1))]. given #430 (T,wt=29): 657 b0 * c0 * a0 * c0 * a0 * c0 != x | y * c0 * a0 != x | d0 * a0 * c0 * a0 = y. [para(184(a,1),282(a,1))]. given #431 (T,wt=29): 659 c0 * b0 * d0 * b0 * d0 * b0 != x | y * b0 * d0 != x | a0 * d0 * b0 * d0 = y. [para(370(a,1),282(a,1))]. given #432 (T,wt=29): 660 x * y * z * u != v | w * v6 * v7 * u != v | x * y * z = w * v6 * v7. [para(1(a,1),283(b,1,2))]. given #433 (A,wt=33): 165 a0 * c * a0 * c * a0 * c * x != y | d * z != y | b0 * c * a0 * c * a0 * x = z. [para(12(a,1),41(a,1))]. given #434 (T,wt=29): 662 x * y * a * a0 * z != u | v * w * b0 * z != u | x * y * b = v * w. [para(18(a,1),283(a,1,2,2))]. given #435 (T,wt=29): 663 x * y * z * b0 * u != v | w * a * a0 * u != v | x * y * z = w * b. [para(18(a,1),283(b,1,2))]. given #436 (T,wt=29): 665 x * y * c * a0 * z != u | v * w * b0 * z != u | x * y * d = v * w. [para(22(a,1),283(a,1,2,2))]. given #437 (T,wt=29): 666 x * y * z * b0 * u != v | w * c * a0 * u != v | x * y * z = w * d. [para(22(a,1),283(b,1,2))]. given #438 (A,wt=33): 166 c * x * a0 * x * a0 * x * a0 != y | z * b0 * x * a0 * x * a0 * x != y | d = z. [para(4(a,1),42(a,1,2))]. given #439 (T,wt=29): 668 x * y * a * c0 * z != u | v * w * d0 * z != u | x * y * b = v * w. [para(26(a,1),283(a,1,2,2))]. given #440 (T,wt=29): 669 x * y * z * d0 * u != v | w * a * c0 * u != v | x * y * z = w * b. [para(26(a,1),283(b,1,2))]. given #441 (T,wt=29): 677 a0 * a * a0 * a * a0 * a != x | y * b0 * a * a0 != x | a * a0 * b = y. [para(4(a,1),286(a,1))]. given #442 (T,wt=29): 685 b0 * x * b0 * x * b0 * x != y | a * a0 * x * b0 != y | x * b0 * x = b. [para(4(a,1),287(a,1))]. given #443 (A,wt=33): 168 c * a0 * x * b0 * x * b0 * x != y | z * x * b0 * x * b0 * x * b0 != y | d = z. [para(4(a,1),42(b,1,2))]. given #444 (T,wt=29): 690 a0 * c * a0 * c * a0 * c != x | y * b0 * c * a0 != x | c * a0 * d = y. [para(4(a,1),288(a,1))]. given #445 (T,wt=29): 694 b0 * x * b0 * x * b0 * x != y | c * a0 * x * b0 != y | x * b0 * x = d. [para(4(a,1),289(a,1))]. given #446 (T,wt=29): 699 c0 * a * c0 * a * c0 * a != x | y * d0 * a * c0 != x | a * c0 * b = y. [para(4(a,1),290(a,1))]. given #447 (T,wt=29): 706 d0 * x * d0 * x * d0 * x != y | a * c0 * x * d0 != y | x * d0 * x = b. [para(4(a,1),291(a,1))]. given #448 (A,wt=33): 170 a0 * c * a0 * c * a0 * c * x != y | z * b0 * c * a0 * c * a0 * x != y | d = z. [para(12(a,1),42(a,1))]. given #449 (T,wt=29): 710 c0 * b0 * d0 * b0 * d0 * b0 != x | a * c0 * b0 * d0 != x | a0 * d0 * b0 = b. [para(370(a,1),291(a,1))]. given #450 (T,wt=29): 737 x * y * z * u * a * a0 != v | x * y * z * u * b * w != v | b0 = w. [para(1(a,1),342(a,1,2,2)),rewrite(1(12))]. given #451 (T,wt=29): 739 x * b * x * a * a0 != y | b * x * b * x * b * x != y | x * b = b0. [para(4(a,1),342(b,1)),flip(c)]. given #452 (T,wt=29): 740 x * y * z * a * a0 != u | x * y * z * a * a0 * v != u | b0 * v = b0. [para(18(a,1),342(b,1,2,2,2)),flip(c)]. given #453 (A,wt=33): 171 c * a0 * x * b0 * x * b0 * y != z | b0 * x * b0 * x * b0 * x * y != z | d = x. [para(12(a,1),42(b,1))]. given #454 (T,wt=29): 741 x * y * z * a * a0 != u | x * y * z * a * c0 * v != u | d0 * v = b0. [para(26(a,1),342(b,1,2,2,2)),flip(c)]. given #455 (T,wt=29): 746 a * a0 * a * a0 != x | a0 * a * a0 * a * a0 * a != x | b0 * a * a0 = b0. [para(4(a,1),345(b,1))]. given #456 (T,wt=29): 750 a * c0 * a * a0 != x | c0 * a * c0 * a * c0 * a != x | d0 * a * c0 = b0. [para(4(a,1),346(b,1))]. given #457 (T,wt=29): 753 x * y * z * u * c * a0 != v | x * y * z * u * d * w != v | b0 = w. [para(1(a,1),356(a,1,2,2)),rewrite(1(12))]. given #458 (A,wt=35): 172 d0 * b * a * c0 * b * a * c0 * b * x = a * c0 * b * a * c0 * b * a * c0 * x. [hyper(47,a,1,a(flip),b,12,a),rewrite(1(12),1(14),1(28),1(30),1(32))]. given #459 (T,wt=29): 755 x * d * x * c * a0 != y | d * x * d * x * d * x != y | x * d = b0. [para(4(a,1),356(b,1)),flip(c)]. given #460 (T,wt=29): 756 x * y * z * c * a0 != u | x * y * z * c * a0 * v != u | b0 * v = b0. [para(22(a,1),356(b,1,2,2,2)),flip(c)]. given #461 (T,wt=29): 762 c * a0 * c * a0 != x | a0 * c * a0 * c * a0 * c != x | b0 * c * a0 = b0. [para(4(a,1),359(b,1))]. given #462 (T,wt=29): 765 x * y * z * u * a * c0 != v | x * y * z * u * b * w != v | d0 = w. [para(1(a,1),364(a,1,2,2)),rewrite(1(12))]. given #463 (A,wt=33): 173 a * x * c0 * x * c0 * x * c0 != y | b * z != y | d0 * x * c0 * x * c0 * x = z. [para(4(a,1),47(a,1,2))]. given #464 (T,wt=29): 767 x * b * x * a * c0 != y | b * x * b * x * b * x != y | x * b = d0. [para(4(a,1),364(b,1)),flip(c)]. given #465 (T,wt=29): 768 x * y * z * a * c0 != u | x * y * z * a * a0 * v != u | b0 * v = d0. [para(18(a,1),364(b,1,2,2,2)),flip(c)]. given #466 (T,wt=29): 769 x * y * z * a * c0 != u | x * y * z * a * c0 * v != u | d0 * v = d0. [para(26(a,1),364(b,1,2,2,2)),flip(c)]. given #467 (T,wt=29): 774 a * a0 * a * c0 != x | a0 * a * a0 * a * a0 * a != x | b0 * a * a0 = d0. [para(4(a,1),367(b,1))]. given #468 (A,wt=33): 175 a * c0 * x != y | z * b * z * b * z * b != y | d0 * x = z * b * z * b * z. [para(4(a,1),47(b,1))]. given #469 (T,wt=29): 778 a * c0 * a * c0 != x | c0 * a * c0 * a * c0 * a != x | d0 * a * c0 = d0. [para(4(a,1),368(b,1))]. given #470 (T,wt=29): 783 x * y * z * u * a * a0 != v | w * b0 != v | x * y * z * u * b = w. [para(1(a,1),398(a,1,2,2)),rewrite(1(14))]. given #471 (T,wt=29): 784 x * y * z * a * a0 != u | v * w * b0 != u | x * y * z * b = v * w. [para(1(a,1),398(b,1))]. given #472 (T,wt=29): 785 x * y * a * a0 != z | u * v * w * b0 != z | x * y * b = u * v * w. [para(1(a,1),399(b,1,2))]. given #473 (A,wt=33): 177 c0 * a * c0 * a * c0 * a * x != y | b * z != y | d0 * a * c0 * a * c0 * x = z. [para(12(a,1),47(a,1))]. given #474 (T,wt=29): 786 x * a * a0 != y | z * u * v * w * b0 != y | z * u * v * w = x * b. [para(1(a,1),400(b,1,2,2))]. given #475 (T,wt=29): 787 x * y * z * u * v * b0 != w | a * a0 != w | x * y * z * u * v = b. [para(1(a,1),418(a,1,2,2,2))]. given #476 (T,wt=29): 790 x * y * z * u * c * a0 != v | w * b0 != v | x * y * z * u * d = w. [para(1(a,1),419(a,1,2,2)),rewrite(1(14))]. given #477 (T,wt=29): 791 x * y * z * c * a0 != u | v * w * b0 != u | x * y * z * d = v * w. [para(1(a,1),419(b,1))]. given #478 (A,wt=33): 178 a * x * c0 * x * c0 * x * c0 != y | z * d0 * x * c0 * x * c0 * x != y | b = z. [para(4(a,1),48(a,1,2))]. given #479 (T,wt=29): 792 x * y * c * a0 != z | u * v * w * b0 != z | x * y * d = u * v * w. [para(1(a,1),420(b,1,2))]. given #480 (T,wt=29): 793 x * c * a0 != y | z * u * v * w * b0 != y | z * u * v * w = x * d. [para(1(a,1),421(b,1,2,2))]. given #481 (T,wt=29): 794 x * y * z * u * v * b0 != w | c * a0 != w | x * y * z * u * v = d. [para(1(a,1),426(a,1,2,2,2))]. given #482 (T,wt=29): 795 x * y * z * u * a * c0 != v | w * d0 != v | x * y * z * u * b = w. [para(1(a,1),445(a,1,2,2)),rewrite(1(14))]. given #483 (A,wt=33): 180 a * c0 * x * d0 * x * d0 * x != y | z * x * d0 * x * d0 * x * d0 != y | b = z. [para(4(a,1),48(b,1,2))]. given #484 (T,wt=29): 796 x * y * z * a * c0 != u | v * w * d0 != u | x * y * z * b = v * w. [para(1(a,1),445(b,1))]. given #485 (T,wt=29): 797 x * y * a * c0 != z | u * v * w * d0 != z | x * y * b = u * v * w. [para(1(a,1),446(b,1,2))]. given #486 (T,wt=29): 798 x * a * c0 != y | z * u * v * w * d0 != y | z * u * v * w = x * b. [para(1(a,1),447(b,1,2,2))]. given #487 (T,wt=29): 799 x * y * z * u * v * d0 != w | a * c0 != w | x * y * z * u * v = b. [para(1(a,1),452(a,1,2,2,2))]. given #488 (A,wt=33): 182 c0 * a * c0 * a * c0 * a * x != y | z * d0 * a * c0 * a * c0 * x != y | b = z. [para(12(a,1),48(a,1))]. given #489 (T,wt=29): 801 x * y * z * u * a * a0 != v | x * y * z * u * a * c0 != v | d0 = b0. [para(1(a,1),453(a,1,2,2)),rewrite(1(13))]. given #490 (T,wt=29): 802 x * y * z * u * a * a0 != v | a * a0 != v | x * y * z * u * b = b. [para(1(a,1),454(a,1,2,2)),rewrite(1(15))]. given #491 (T,wt=29): 803 x * y * z * u * a * a0 != v | c * a0 != v | x * y * z * u * b = d. [para(1(a,1),455(a,1,2,2)),rewrite(1(15))]. given #492 (T,wt=29): 804 x * y * z * u * c * a0 != v | a * a0 != v | x * y * z * u * d = b. [para(1(a,1),456(a,1,2,2)),rewrite(1(15))]. given #493 (A,wt=33): 183 a * c0 * x * d0 * x * d0 * y != z | d0 * x * d0 * x * d0 * x * y != z | b = x. [para(12(a,1),48(b,1))]. given #494 (T,wt=29): 806 x * y * z * u * c * a0 != v | c * a0 != v | x * y * z * u * d = d. [para(1(a,1),457(a,1,2,2)),rewrite(1(15))]. given #495 (T,wt=29): 807 x * y * z * u * a * c0 != v | a * c0 != v | x * y * z * u * b = b. [para(1(a,1),475(a,1,2,2)),rewrite(1(15))]. given #496 (T,wt=29): 808 x * y * z * a * a0 * u != v | a * a0 * u != v | x * y * z * b = b. [para(1(a,1),476(a,1,2)),rewrite(1(16))]. given #497 (T,wt=29): 810 a0 * a * a0 * a * a0 * a != x | a * a0 * a * a0 != x | a * a0 * b = b. [para(4(a,1),476(a,1))]. given #498 (A,wt=31): 185 x * y * z * u * z * u * z * u = x * y * u * z * u * z * u * z. [para(14(a,1),1(a,1)),rewrite(1(7))]. given #499 (T,wt=27): 2150 d0 * d0 * x * d0 * x * d0 * x = x * d0 * x * d0 * x * d0 * d0. [hyper(47,a,185,a,b,122,a(flip))]. NOTE: Back_subsumption disabled, ratio of kept to back_subsumed is 52 (0.00 of 8.66 sec). given #500 (T,wt=27): 2151 b0 * b0 * x * b0 * x * b0 * x = x * b0 * x * b0 * x * b0 * b0. [hyper(41,a,185,a,b,119,a)]. given #501 (T,wt=29): 813 x * y * z * a * a0 * u != v | c * a0 * u != v | x * y * z * b = d. [para(1(a,1),482(a,1,2)),rewrite(1(16))]. given #502 (T,wt=29): 815 a0 * a * a0 * a * a0 * a != x | c * a0 * a * a0 != x | a * a0 * b = d. [para(4(a,1),482(a,1))]. given #503 (A,wt=33): 186 x * y * z * y * z * y * z != u | x * v != u | z * y * z * y * z * y = v. [para(14(a,1),2(a,1))]. given #504 (T,wt=29): 818 x * y * z * c * a0 * u != v | a * a0 * u != v | x * y * z * d = b. [para(1(a,1),488(a,1,2)),rewrite(1(16))]. given #505 (T,wt=29): 820 a0 * c * a0 * c * a0 * c != x | a * a0 * c * a0 != x | c * a0 * d = b. [para(4(a,1),488(a,1))]. given #506 (T,wt=29): 823 x * y * z * c * a0 * u != v | c * a0 * u != v | x * y * z * d = d. [para(1(a,1),495(a,1,2)),rewrite(1(16))]. given #507 (T,wt=29): 825 a0 * c * a0 * c * a0 * c != x | c * a0 * c * a0 != x | c * a0 * d = d. [para(4(a,1),495(a,1))]. given #508 (A,wt=33): 187 x * y * z * y * z * y * z != u | v * z * y * z * y * z * y != u | x = v. [para(14(a,1),3(a,1))]. given #509 (T,wt=29): 828 x * y * z * a * c0 * u != v | a * c0 * u != v | x * y * z * b = b. [para(1(a,1),501(a,1,2)),rewrite(1(16))]. given #510 (T,wt=29): 830 c0 * a * c0 * a * c0 * a != x | a * c0 * a * c0 != x | a * c0 * b = b. [para(4(a,1),501(a,1))]. given #511 (T,wt=29): 833 x * y * z * a * a0 != u | v * a * a0 != u | x * y * z * b = v * b. [para(1(a,1),507(a,1,2)),rewrite(1(15))]. given #512 (T,wt=29): 834 x * y * a * a0 != z | u * v * a * a0 != z | x * y * b = u * v * b. [para(1(a,1),507(b,1)),rewrite(1(18))]. given #513 (A,wt=33): 188 a * a0 != x | b * y * z * y * z * y * z != x | z * y * z * y * z * y = b0. [para(14(a,1),19(b,1)),flip(c)]. given #514 (T,wt=29): 836 x * y * z * a * a0 != u | v * c * a0 != u | x * y * z * b = v * d. [para(1(a,1),508(a,1,2)),rewrite(1(15))]. given #515 (T,wt=29): 837 x * y * a * a0 != z | u * v * c * a0 != z | u * v * d = x * y * b. [para(1(a,1),508(b,1)),rewrite(1(18)),flip(c)]. given #516 (T,wt=29): 838 x * a * a0 != y | z * u * v * c * a0 != y | z * u * v * d = x * b. [para(1(a,1),509(b,1,2)),rewrite(1(15))]. given #517 (T,wt=29): 839 x * y * z * a * a0 != u | a * a0 * b0 != u | a * a0 = x * y * z * b. [para(1(a,1),513(a,1,2)),rewrite(1(19))]. given #518 (A,wt=33): 189 c * a0 != x | d * y * z * y * z * y * z != x | z * y * z * y * z * y = b0. [para(14(a,1),23(b,1)),flip(c)]. given #519 (T,wt=29): 840 x * y * z * a * a0 != u | c * a0 * b0 != u | c * a0 = x * y * z * b. [para(1(a,1),514(a,1,2)),rewrite(1(19))]. given #520 (T,wt=29): 841 x * y * z * a * a0 != u | a * c0 * b0 != u | a * c0 = x * y * z * b. [para(1(a,1),515(a,1,2)),rewrite(1(19))]. given #521 (T,wt=29): 842 x * y * z * c * a0 != u | v * c * a0 != u | x * y * z * d = v * d. [para(1(a,1),516(a,1,2)),rewrite(1(15))]. given #522 (T,wt=29): 843 x * y * c * a0 != z | u * v * c * a0 != z | x * y * d = u * v * d. [para(1(a,1),516(b,1)),rewrite(1(18))]. given #523 (A,wt=33): 190 a * c0 != x | b * y * z * y * z * y * z != x | z * y * z * y * z * y = d0. [para(14(a,1),27(b,1)),flip(c)]. given #524 (T,wt=29): 844 x * y * z * c * a0 != u | a * a0 * b0 != u | a * a0 = x * y * z * d. [para(1(a,1),518(a,1,2)),rewrite(1(19))]. given #525 (T,wt=29): 845 x * y * z * c * a0 != u | c * a0 * b0 != u | c * a0 = x * y * z * d. [para(1(a,1),519(a,1,2)),rewrite(1(19))]. given #526 (T,wt=29): 846 x * y * z * c * a0 != u | a * c0 * b0 != u | a * c0 = x * y * z * d. [para(1(a,1),520(a,1,2)),rewrite(1(19))]. given #527 (T,wt=29): 847 x * y * z * a * c0 != u | v * a * c0 != u | x * y * z * b = v * b. [para(1(a,1),521(a,1,2)),rewrite(1(15))]. given #528 (A,wt=33): 191 a * a0 != x | a * y * a0 * y * a0 * y * a0 != x | b0 * y * a0 * y * a0 * y = b0. [para(4(a,1),54(b,1,2))]. given #529 (T,wt=29): 848 x * y * a * c0 != z | u * v * a * c0 != z | x * y * b = u * v * b. [para(1(a,1),521(b,1)),rewrite(1(18))]. given #530 (T,wt=29): 849 x * y * z * a * c0 != u | a * a0 * d0 != u | a * a0 = x * y * z * b. [para(1(a,1),528(a,1,2)),rewrite(1(19))]. given #531 (T,wt=29): 850 x * y * z * a * c0 != u | c * a0 * d0 != u | c * a0 = x * y * z * b. [para(1(a,1),529(a,1,2)),rewrite(1(19))]. given #532 (T,wt=29): 851 x * y * z * a * c0 != u | a * c0 * d0 != u | a * c0 = x * y * z * b. [para(1(a,1),530(a,1,2)),rewrite(1(19))]. given #533 (A,wt=33): 193 a * a0 != x | a0 * a * a0 * a * a0 * a * y != x | b0 * a * a0 * a * a0 * y = b0. [para(12(a,1),54(b,1))]. given #534 (T,wt=29): 852 x * y * z * u * v != w | a * a0 * v != w | a * a0 = x * y * z * u. [para(1(a,1),664(a,1,2,2))]. given #535 (T,wt=29): 854 x * y * a * a0 * z != u | a * a0 * b0 * z != u | a * a0 = x * y * b. [para(18(a,1),664(a,1,2,2))]. given #536 (T,wt=29): 855 x * y * c * a0 * z != u | a * a0 * b0 * z != u | a * a0 = x * y * d. [para(22(a,1),664(a,1,2,2))]. given #537 (T,wt=29): 856 x * y * a * c0 * z != u | a * a0 * d0 * z != u | a * a0 = x * y * b. [para(26(a,1),664(a,1,2,2))]. given #538 (A,wt=33): 194 a * a0 != x | a * y * c0 * y * c0 * y * c0 != x | d0 * y * c0 * y * c0 * y = b0. [para(4(a,1),55(b,1,2))]. given #539 (T,wt=29): 857 x * y * z * u * v != w | c * a0 * v != w | c * a0 = x * y * z * u. [para(1(a,1),667(a,1,2,2))]. given #540 (T,wt=29): 859 x * y * a * a0 * z != u | c * a0 * b0 * z != u | c * a0 = x * y * b. [para(18(a,1),667(a,1,2,2))]. given #541 (T,wt=29): 860 x * y * c * a0 * z != u | c * a0 * b0 * z != u | c * a0 = x * y * d. [para(22(a,1),667(a,1,2,2))]. given #542 (T,wt=29): 861 x * y * a * c0 * z != u | c * a0 * d0 * z != u | c * a0 = x * y * b. [para(26(a,1),667(a,1,2,2))]. given #543 (A,wt=33): 196 a * a0 != x | c0 * a * c0 * a * c0 * a * y != x | d0 * a * c0 * a * c0 * y = b0. [para(12(a,1),55(b,1))]. given #544 (T,wt=29): 863 x * y * z * u * v != w | a * c0 * v != w | a * c0 = x * y * z * u. [para(1(a,1),670(a,1,2,2))]. given #545 (T,wt=29): 865 x * y * a * a0 * z != u | a * c0 * b0 * z != u | a * c0 = x * y * b. [para(18(a,1),670(a,1,2,2))]. given #546 (T,wt=29): 866 x * y * c * a0 * z != u | a * c0 * b0 * z != u | a * c0 = x * y * d. [para(22(a,1),670(a,1,2,2))]. given #547 (T,wt=29): 867 x * y * a * c0 * z != u | a * c0 * d0 * z != u | a * c0 = x * y * b. [para(26(a,1),670(a,1,2,2))]. given #548 (A,wt=33): 217 c * a0 != x | c * y * a0 * y * a0 * y * a0 != x | b0 * y * a0 * y * a0 * y = b0. [para(4(a,1),75(b,1,2))]. given #549 (T,wt=29): 868 x * y * a * a0 * z != u | v * a * a0 * z != u | x * y * b = v * b. [para(1(a,1),713(a,1)),rewrite(1(16))]. given #550 (T,wt=29): 871 x * y * a * a0 * z != u | v * c * a0 * z != u | x * y * b = v * d. [para(1(a,1),715(a,1)),rewrite(1(18)),flip(c)]. given #551 (T,wt=29): 872 x * a * a0 * y != z | u * v * c * a0 * y != z | u * v * d = x * b. [para(1(a,1),715(b,1)),rewrite(1(16))]. given #552 (T,wt=29): 879 x * y * c * a0 * z != u | v * c * a0 * z != u | x * y * d = v * d. [para(1(a,1),723(a,1)),rewrite(1(16))]. given #553 (A,wt=33): 219 c * a0 != x | a0 * c * a0 * c * a0 * c * y != x | b0 * c * a0 * c * a0 * y = b0. [para(12(a,1),75(b,1))]. given #554 (T,wt=29): 884 x * y * a * c0 * z != u | v * a * c0 * z != u | x * y * b = v * b. [para(1(a,1),732(a,1)),rewrite(1(16))]. given #555 (T,wt=29): 1294 x * a * a0 != y | x * b * x * b * x * b != y | x * b * x * b = b0. [para(4(a,1),101(b,1))]. given #556 (T,wt=29): 1604 x * c * a0 != y | x * d * x * d * x * d != y | x * d * x * d = b0. [para(4(a,1),134(b,1))]. given #557 (T,wt=29): 1605 b0 * c * a0 != x | c * a0 * c * a0 * c * a0 != x | b0 * c * a0 * d = b0. [para(6(a,1),134(b,1,2,2,2,2)),rewrite(22(15),22(17),22(24))]. given #558 (A,wt=33): 220 a * c0 != x | a * y * a0 * y * a0 * y * a0 != x | b0 * y * a0 * y * a0 * y = d0. [para(4(a,1),77(b,1,2))]. given #559 (T,wt=29): 1606 x * a * c0 != y | x * b * x * b * x * b != y | x * b * x * b = d0. [para(4(a,1),139(b,1))]. given #560 (T,wt=29): 1630 a0 * a * a0 * a * a0 * a != x | b0 * y != x | a * a0 * a * a0 * b = y. [para(4(a,1),203(a,1))]. given #561 (T,wt=29): 1631 c0 * a * c0 * a * c0 * a != x | d0 * y != x | a * c0 * a * c0 * b = y. [para(4(a,1),205(a,1))]. given #562 (T,wt=29): 1633 a0 * a * a0 * a * a0 * a != x | y * a * a0 * a * a0 * b != x | b0 = y. [para(4(a,1),214(a,1))]. given #563 (A,wt=33): 222 a * c0 != x | a0 * a * a0 * a * a0 * a * y != x | b0 * a * a0 * a * a0 * y = d0. [para(12(a,1),77(b,1))]. given #564 (T,wt=29): 1634 c0 * a * c0 * a * c0 * a != x | y * a * c0 * a * c0 * b != x | d0 = y. [para(4(a,1),216(a,1))]. given #565 (T,wt=29): 1643 a0 * a * a0 * a * a0 * a != x | b0 * a * y != x | a0 * a * a0 * b = y. [para(4(a,1),237(a,1))]. given #566 (T,wt=29): 1644 a0 * a * a0 * a * a0 * a != x | y * a0 * a * a0 * b != x | b0 * a = y. [para(4(a,1),241(a,1))]. given #567 (T,wt=29): 1645 c * a0 * c * a0 * c * a0 != x | b0 * c * a0 * y != x | c * a0 * d = y. [para(6(a,1),249(a,1,2,2,2,2)),rewrite(22(9),22(11),22(17),22(24))]. given #568 (A,wt=33): 223 a * c0 != x | a * y * c0 * y * c0 * y * c0 != x | d0 * y * c0 * y * c0 * y = d0. [para(4(a,1),78(b,1,2))]. given #569 (T,wt=29): 1646 a0 * a * a0 * a * a0 * a != x | b0 * a * a0 * y != x | a * a0 * b = y. [para(4(a,1),255(a,1))]. given #570 (T,wt=29): 1658 a0 * a * a0 * a * a0 * a != x | b0 * b * y != x | b0 * a * a0 * b = y. [para(4(a,1),262(a,1))]. given #571 (T,wt=29): 1659 c0 * a * c0 * a * c0 * a != x | d0 * a * y != x | c0 * a * c0 * b = y. [para(4(a,1),264(a,1))]. given #572 (T,wt=29): 1660 c0 * a * c0 * a * c0 * a != x | y * c0 * a * c0 * b != x | d0 * a = y. [para(4(a,1),267(a,1))]. given #573 (A,wt=33): 225 a * c0 != x | c0 * a * c0 * a * c0 * a * y != x | d0 * a * c0 * a * c0 * y = d0. [para(12(a,1),78(b,1))]. given #574 (T,wt=29): 1662 c0 * a * c0 * a * c0 * a != x | d0 * a * c0 * y != x | a * c0 * b = y. [para(4(a,1),270(a,1))]. given #575 (T,wt=29): 1663 c0 * a * c0 * a * c0 * a != x | d0 * b * y != x | d0 * a * c0 * b = y. [para(4(a,1),281(a,1))]. given #576 (T,wt=29): 1665 c * a0 * c * a0 * c * a0 != x | y * c * a0 * d != x | b0 * c * a0 = y. [para(6(a,1),285(a,1,2,2,2,2)),rewrite(22(9),22(11),22(17),6(23))]. given #577 (T,wt=29): 1666 a0 * a * a0 * a * a0 * a != x | y * a * a0 * b != x | b0 * a * a0 = y. [para(4(a,1),294(a,1))]. given #578 (A,wt=33): 227 a * x * a0 * x * a0 * x * a0 != y | c * a0 * x * a0 * x * a0 * x != y | d = b. [para(4(a,1),154(a,1,2))]. given #579 (T,wt=29): 1667 c0 * a * c0 * a * c0 * a != x | y * a * c0 * b != x | d0 * a * c0 = y. [para(4(a,1),296(a,1))]. given #580 (T,wt=29): 1673 a0 * a * a0 * a * a0 * a != x | y * b0 * a * a0 * b != x | b0 * b = y. [para(4(a,1),316(a,1))]. given #581 (T,wt=29): 1674 c * a0 * c * a0 * c * a0 != x | a * a0 * c * a0 * d != x | b0 * d = b. [para(6(a,1),318(a,1,2,2,2,2)),rewrite(22(9),22(11),22(19))]. given #582 (T,wt=29): 1675 c * a0 * c * a0 * c * a0 != x | c * a0 * c * a0 * d != x | b0 * d = d. [para(6(a,1),328(a,1,2,2,2,2)),rewrite(22(9),22(11),22(19))]. given #583 (A,wt=33): 229 a * a0 * x * a0 * x * a0 * x != y | c * x * a0 * x * a0 * x * a0 != y | d = b. [para(4(a,1),154(b,1,2))]. given #584 (T,wt=29): 1679 c0 * a * c0 * a * c0 * a != x | y * d0 * a * c0 * b != x | d0 * b = y. [para(4(a,1),337(a,1))]. given #585 (T,wt=29): 1681 b * x * a * a0 != y | b * x * b * x * b * x != y | x * b * x = b0. [para(4(a,1),344(b,1))]. given #586 (T,wt=29): 1682 b0 * a * a0 != x | a0 * a * a0 * a * a0 * a != x | b0 * a * a0 * b = b0. [para(4(a,1),351(b,1))]. given #587 (T,wt=29): 1686 d0 * a * a0 != x | c0 * a * c0 * a * c0 * a != x | d0 * a * c0 * b = b0. [para(4(a,1),355(b,1))]. given #588 (A,wt=33): 231 a0 * a * a0 * a * a0 * a * x != y | c * a0 * a * a0 * a * a0 * x != y | d = b. [para(12(a,1),154(a,1))]. given #589 (T,wt=29): 1687 d * x * c * a0 != y | d * x * d * x * d * x != y | x * d * x = b0. [para(4(a,1),358(b,1))]. given #590 (T,wt=29): 1688 b * x * a * c0 != y | b * x * b * x * b * x != y | x * b * x = d0. [para(4(a,1),366(b,1))]. given #591 (T,wt=29): 1696 b0 * a * c0 != x | a0 * a * a0 * a * a0 * a != x | b0 * a * a0 * b = d0. [para(4(a,1),386(b,1))]. given #592 (T,wt=29): 1697 d0 * a * c0 != x | c0 * a * c0 * a * c0 * a != x | d0 * a * c0 * b = d0. [para(4(a,1),390(b,1))]. given #593 (A,wt=33): 232 a * a0 * c * a0 * c * a0 * x != y | a0 * c * a0 * c * a0 * c * x != y | d = b. [para(12(a,1),154(b,1))]. given #594 (T,wt=29): 1724 c * a0 * c * a0 * c * a0 != x | b0 * c * y != x | a0 * c * a0 * d = y. [para(4(a,1),430(a,1))]. given #595 (T,wt=29): 1725 c * a0 * c * a0 * c * a0 != x | y * a0 * c * a0 * d != x | b0 * c = y. [para(4(a,1),434(a,1))]. given #596 (T,wt=29): 1729 a0 * a * a0 * a * a0 * a != x | a * a0 * a * a0 * b != x | b0 * b = b. [para(4(a,1),481(a,1))]. given #597 (T,wt=29): 1731 a0 * a * a0 * a * a0 * a != x | c * a0 * a * a0 * b != x | b0 * b = d. [para(4(a,1),487(a,1))]. given #598 (A,wt=33): 236 x * a * a0 * a * a0 * a * a0 != y | x * b0 * z != y | a * a0 * a * a0 * b = z. [para(21(a,1),9(a,1,2))]. given #599 (T,wt=29): 1735 c0 * a * c0 * a * c0 * a != x | a * c0 * a * c0 * b != x | d0 * b = b. [para(4(a,1),506(a,1))]. given #600 (T,wt=29): 1737 b0 * d0 * b0 * d0 * b0 * d0 != x | c0 * b0 * d0 * b0 * d0 * b0 != x | b0 = a0. [para(4(a,1),559(a,1))]. given #601 (T,wt=29): 1740 x * y * x * y * x * y != z | y * x * y * x * y * u != z | x = u. [para(4(a,1),572(a,1))]. given #602 (T,wt=29): 1741 x * y * x * y * x * z != u | y * x * y * x * y * x != u | z = y. [para(4(a,1),572(b,1))]. given #603 (A,wt=33): 240 x * a * a0 * a * a0 * a * a0 != y | z * a * a0 * a * a0 * b != y | x * b0 = z. [para(21(a,1),10(a,1,2))]. given #604 (T,wt=29): 1747 a * a0 * a * a0 * a * a0 != x | b0 * a * a0 * a * a0 * y != x | b = y. [para(21(a,1),572(a,1))]. given #605 (T,wt=29): 1749 a * c0 * a * c0 * a * c0 != x | d0 * a * c0 * a * c0 * y != x | b = y. [para(29(a,1),572(a,1))]. given #606 (T,wt=29): 1753 a0 * c * a0 * c * a0 * c != x | b0 * c * a0 * c * a0 * y != x | d = y. [para(45(a,1),572(a,1))]. given #607 (T,wt=29): 1757 b0 * c0 * a0 * c0 * a0 * c0 != x | d0 * a0 * c0 * a0 * c0 * y != x | a0 = y. [para(184(a,1),572(a,1))]. given #608 (A,wt=33): 242 x * y * a * a0 * a * a0 * b != z | a * a0 * a * a0 * a * a0 != z | x * y = b0. [para(21(a,1),10(b,1))]. given #609 (T,wt=29): 1759 c0 * b0 * d0 * b0 * d0 * b0 != x | a0 * d0 * b0 * d0 * b0 * y != x | d0 = y. [para(370(a,1),572(a,1))]. given #610 (T,wt=29): 1793 a * a0 * a * a0 * a * a0 != x | b0 * a * a0 * b * y != x | b0 * b = y. [para(5(a,1),574(a,1,2,2,2,2)),rewrite(18(9),18(11),18(19))]. given #611 (T,wt=29): 1794 c * a0 * c * a0 * c * a0 != x | b0 * c * a0 * d * y != x | b0 * d = y. [para(6(a,1),574(a,1,2,2,2,2)),rewrite(22(9),22(11),22(19))]. given #612 (T,wt=29): 1795 a * c0 * a * c0 * a * c0 != x | d0 * a * c0 * b * y != x | d0 * b = y. [para(7(a,1),574(a,1,2,2,2,2)),rewrite(26(9),26(11),26(19))]. given #613 (A,wt=33): 243 a * a0 * a * a0 * a * a0 * b != x | y * a * a0 * a * a0 * a * a0 != x | b = y. [para(21(a,1),37(b,1,2))]. given #614 (T,wt=29): 1800 a * a0 * a * a0 * a * a0 != x | a0 * a * a0 * b * y != x | b0 * a = y. [para(4(a,1),575(a,1))]. given #615 (T,wt=29): 1812 c * a0 * c * a0 * c * a0 != x | a0 * c * a0 * d * y != x | b0 * c = y. [para(4(a,1),576(a,1))]. given #616 (T,wt=29): 1815 a0 * c * a0 * c * a0 * c != x | b0 * c * a0 * d * y != x | b0 * d = y. [para(45(a,1),576(a,1))]. given #617 (T,wt=29): 1822 a * c0 * a * c0 * a * c0 != x | c0 * a * c0 * b * y != x | d0 * a = y. [para(4(a,1),577(a,1))]. given #618 (A,wt=33): 244 c * a0 * a * a0 * a * a0 * b != x | y * a * a0 * a * a0 * a * a0 != x | d = y. [para(21(a,1),42(b,1,2))]. given #619 (T,wt=29): 1832 a0 * a * a0 * a * a0 * a != x | b0 * a * a0 * a * y != x | a0 * b = y. [para(4(a,1),580(a,1))]. given #620 (T,wt=29): 1833 c0 * a * c0 * a * c0 * a != x | d0 * a * c0 * a * y != x | c0 * b = y. [para(4(a,1),582(a,1))]. given #621 (T,wt=29): 1834 c * a0 * c * a0 * c * a0 != x | b0 * c * a0 * c * y != x | a0 * d = y. [para(4(a,1),586(a,1))]. given #622 (T,wt=29): 1843 x * y * x * y * x * y != z | u * x != z | y * x * y * x * y = u. [para(4(a,1),635(a,1))]. given #623 (A,wt=33): 248 x * y * z * y * z * y * z != u | x * z * y * v != u | z * y * z * y = v. [para(4(a,1),30(a,1,2))]. given #624 (T,wt=29): 1852 a * a0 * a * a0 * a * a0 != x | y * b != x | b0 * a * a0 * a * a0 = y. [para(21(a,1),635(a,1))]. given #625 (T,wt=29): 1854 a * c0 * a * c0 * a * c0 != x | y * b != x | d0 * a * c0 * a * c0 = y. [para(29(a,1),635(a,1))]. given #626 (T,wt=29): 1858 a0 * c * a0 * c * a0 * c != x | y * d != x | b0 * c * a0 * c * a0 = y. [para(45(a,1),635(a,1))]. given #627 (T,wt=29): 1862 b0 * c0 * a0 * c0 * a0 * c0 != x | y * a0 != x | d0 * a0 * c0 * a0 * c0 = y. [para(184(a,1),635(a,1))]. given #628 (A,wt=33): 253 x * y * x * y * x * y * z != u | y * x * y * v != u | x * y * x * z = v. [para(12(a,1),30(a,1))]. given #629 (T,wt=29): 1864 c0 * b0 * d0 * b0 * d0 * b0 != x | y * d0 != x | a0 * d0 * b0 * d0 * b0 = y. [para(370(a,1),635(a,1))]. given #630 (T,wt=29): 1911 a * a0 * a * a0 * a * a0 != x | y * b0 * b != x | b0 * a * a0 * b = y. [para(5(a,1),638(a,1,2,2,2,2)),rewrite(18(9),18(11),18(23))]. given #631 (T,wt=29): 1912 c * a0 * c * a0 * c * a0 != x | y * b0 * d != x | b0 * c * a0 * d = y. [para(6(a,1),638(a,1,2,2,2,2)),rewrite(22(9),22(11),22(23))]. given #632 (T,wt=29): 1913 a * c0 * a * c0 * a * c0 != x | y * d0 * b != x | d0 * a * c0 * b = y. [para(7(a,1),638(a,1,2,2,2,2)),rewrite(26(9),26(11),26(23))]. given #633 (A,wt=33): 254 x * a * a0 * a * a0 * a * a0 != y | x * b0 * a * z != y | a0 * a * a0 * b = z. [para(21(a,1),30(a,1,2))]. given #634 (T,wt=29): 1914 x * b0 * x * b0 * x * b0 != y | a * a0 * x != y | b0 * x * b0 * x = b. [para(18(a,1),638(b,1))]. given #635 (T,wt=29): 1915 x * b0 * x * b0 * x * b0 != y | c * a0 * x != y | b0 * x * b0 * x = d. [para(22(a,1),638(b,1))]. given #636 (T,wt=29): 1916 x * d0 * x * d0 * x * d0 != y | a * c0 * x != y | d0 * x * d0 * x = b. [para(26(a,1),638(b,1))]. given #637 (T,wt=29): 1918 a * a0 * a * a0 * a * a0 != x | y * b0 * a != x | a0 * a * a0 * b = y. [para(4(a,1),639(a,1))]. given #638 (A,wt=33): 256 x * a0 * a * a0 * a * a0 * a != y | x * b * z != y | b0 * a * a0 * a * a0 = z. [para(4(a,1),40(a,1,2))]. given #639 (T,wt=29): 1931 c0 * b0 * d0 * b0 * d0 * b0 != x | a * a0 * d0 != x | a0 * d0 * b0 * d0 = b. [para(370(a,1),640(a,1))]. given #640 (T,wt=29): 1939 c * a0 * c * a0 * c * a0 != x | y * b0 * c != x | a0 * c * a0 * d = y. [para(4(a,1),641(a,1))]. given #641 (T,wt=29): 1941 a0 * c * a0 * c * a0 * c != x | y * b0 * d != x | b0 * c * a0 * d = y. [para(45(a,1),641(a,1))]. given #642 (T,wt=29): 1951 c0 * b0 * d0 * b0 * d0 * b0 != x | c * a0 * d0 != x | a0 * d0 * b0 * d0 = d. [para(370(a,1),642(a,1))]. given #643 (A,wt=33): 258 x * a * a0 * y != z | b * x * b * x * b * x != z | b0 * y = x * b * x * b. [para(4(a,1),40(b,1))]. given #644 (T,wt=29): 1959 a * c0 * a * c0 * a * c0 != x | y * d0 * a != x | c0 * a * c0 * b = y. [para(4(a,1),643(a,1))]. given #645 (T,wt=29): 1977 a0 * a * a0 * a * a0 * a != x | y * a0 * b != x | b0 * a * a0 * a = y. [para(4(a,1),647(a,1))]. given #646 (T,wt=29): 1978 c0 * a * c0 * a * c0 * a != x | y * c0 * b != x | d0 * a * c0 * a = y. [para(4(a,1),649(a,1))]. given #647 (T,wt=29): 1979 c * a0 * c * a0 * c * a0 != x | y * a0 * d != x | b0 * c * a0 * c = y. [para(4(a,1),653(a,1))]. given #648 (A,wt=33): 261 a * a0 * a * a0 * a * a0 * x != y | a0 * b * z != y | b0 * a * a0 * a * x = z. [para(12(a,1),40(a,1))]. given #649 (T,wt=29): 1993 a0 * a * a0 * a * a0 * a != x | a * a0 * a * a0 * b * y != x | b0 = y. [para(4(a,1),737(a,1))]. given #650 (T,wt=29): 1995 b * x * b * x * a * a0 != y | x * b * x * b * x * b != y | b0 = x. [para(4(a,1),737(b,1))]. given #651 (T,wt=29): 2007 x * b * x * a * a0 != y | x * b * x * b * x * b != y | x * b = b0. [para(4(a,1),739(b,1))]. given #652 (T,wt=29): 2008 b0 * a * a0 * a * a0 != x | a * a0 * a * a0 * a * a0 != x | b0 * b = b0. [para(5(a,1),739(b,1,2,2,2,2)),rewrite(18(8),18(19),18(21))]. given #653 (A,wt=33): 263 x * a * c0 * a * c0 * a * c0 != y | x * d0 * z != y | a * c0 * a * c0 * b = z. [para(29(a,1),9(a,1,2))]. given #654 (T,wt=29): 2009 d0 * a * c0 * a * a0 != x | a * c0 * a * c0 * a * c0 != x | d0 * b = b0. [para(7(a,1),739(b,1,2,2,2,2)),rewrite(26(8),26(19),26(21))]. given #655 (T,wt=29): 2011 a0 * a * a0 * a * a0 != x | a * a0 * a * a0 * a * a0 != x | b0 * a = b0. [para(4(a,1),740(b,1))]. given #656 (T,wt=29): 2019 c0 * a * c0 * a * a0 != x | a * c0 * a * c0 * a * c0 != x | d0 * a = b0. [para(4(a,1),741(b,1))]. given #657 (T,wt=29): 2028 a0 * c * a0 * c * a0 * c != x | c * a0 * c * a0 * d * y != x | b0 = y. [para(4(a,1),753(a,1))]. given #658 (A,wt=33): 266 x * a * c0 * a * c0 * a * c0 != y | z * a * c0 * a * c0 * b != y | x * d0 = z. [para(29(a,1),10(a,1,2))]. given #659 (T,wt=29): 2030 d * x * d * x * c * a0 != y | x * d * x * d * x * d != y | b0 = x. [para(4(a,1),753(b,1))]. given #660 (T,wt=29): 2040 x * d * x * c * a0 != y | x * d * x * d * x * d != y | x * d = b0. [para(4(a,1),755(b,1))]. given #661 (T,wt=29): 2041 b0 * c * a0 * c * a0 != x | c * a0 * c * a0 * c * a0 != x | b0 * d = b0. [para(6(a,1),755(b,1,2,2,2,2)),rewrite(22(8),22(19),22(21))]. given #662 (T,wt=29): 2043 a0 * c * a0 * c * a0 != x | c * a0 * c * a0 * c * a0 != x | b0 * c = b0. [para(4(a,1),756(b,1))]. given #663 (A,wt=33): 268 x * y * a * c0 * a * c0 * b != z | a * c0 * a * c0 * a * c0 != z | x * y = d0. [para(29(a,1),10(b,1))]. given #664 (T,wt=29): 2045 b0 * c * a0 * c * a0 != x | a0 * c * a0 * c * a0 * c != x | b0 * d = b0. [para(45(a,1),756(b,1))]. given #665 (T,wt=29): 2051 c0 * a * c0 * a * c0 * a != x | a * c0 * a * c0 * b * y != x | d0 = y. [para(4(a,1),765(a,1))]. given #666 (T,wt=29): 2053 b * x * b * x * a * c0 != y | x * b * x * b * x * b != y | d0 = x. [para(4(a,1),765(b,1))]. given #667 (T,wt=29): 2065 x * b * x * a * c0 != y | x * b * x * b * x * b != y | x * b = d0. [para(4(a,1),767(b,1))]. given #668 (A,wt=33): 269 x * a * c0 * a * c0 * a * c0 != y | x * d0 * a * z != y | c0 * a * c0 * b = z. [para(29(a,1),30(a,1,2))]. given #669 (T,wt=29): 2066 b0 * a * a0 * a * c0 != x | a * a0 * a * a0 * a * a0 != x | b0 * b = d0. [para(5(a,1),767(b,1,2,2,2,2)),rewrite(18(8),18(19),18(21))]. given #670 (T,wt=29): 2067 d0 * a * c0 * a * c0 != x | a * c0 * a * c0 * a * c0 != x | d0 * b = d0. [para(7(a,1),767(b,1,2,2,2,2)),rewrite(26(8),26(19),26(21))]. given #671 (T,wt=29): 2069 a0 * a * a0 * a * c0 != x | a * a0 * a * a0 * a * a0 != x | b0 * a = d0. [para(4(a,1),768(b,1))]. given #672 (T,wt=29): 2077 c0 * a * c0 * a * c0 != x | a * c0 * a * c0 * a * c0 != x | d0 * a = d0. [para(4(a,1),769(b,1))]. given #673 (A,wt=33): 271 x * a0 * c * a0 * c * a0 * c != y | x * d * z != y | b0 * c * a0 * c * a0 = z. [para(4(a,1),46(a,1,2))]. given #674 (T,wt=29): 2086 a0 * a * a0 * a * a0 * a != x | y * b0 != x | a * a0 * a * a0 * b = y. [para(4(a,1),783(a,1))]. given #675 (T,wt=29): 2089 x * y * a * a0 != z | u * a * a0 * b0 != z | u * a * a0 = x * y * b. [para(18(a,1),785(b,1,2)),rewrite(5(19)),flip(c)]. given #676 (T,wt=29): 2090 x * y * a * a0 != z | a * a0 * u * b0 != z | a * a0 * u = x * y * b. [para(18(a,1),785(b,1)),rewrite(18(20)),flip(c)]. given #677 (T,wt=29): 2091 x * y * a * a0 != z | u * c * a0 * b0 != z | u * c * a0 = x * y * b. [para(22(a,1),785(b,1,2)),rewrite(6(19)),flip(c)]. given #678 (A,wt=33): 273 x * c * a0 * y != z | d * x * d * x * d * x != z | b0 * y = x * d * x * d. [para(4(a,1),46(b,1))]. given #679 (T,wt=29): 2092 x * y * a * a0 != z | c * a0 * u * b0 != z | c * a0 * u = x * y * b. [para(22(a,1),785(b,1)),rewrite(22(20)),flip(c)]. given #680 (T,wt=29): 2093 x * y * a * a0 != z | u * a * c0 * b0 != z | u * a * c0 = x * y * b. [para(26(a,1),785(b,1,2)),rewrite(7(19)),flip(c)]. given #681 (T,wt=29): 2094 x * y * a * a0 != z | a * c0 * u * b0 != z | a * c0 * u = x * y * b. [para(26(a,1),785(b,1)),rewrite(26(20)),flip(c)]. given #682 (T,wt=29): 2097 b0 * x * b0 * x * b0 * x != y | a * a0 != y | x * b0 * x * b0 * x = b. [para(4(a,1),787(a,1))]. given #683 (A,wt=33): 275 c * a0 * c * a0 * c * a0 * x != y | a0 * d * z != y | b0 * c * a0 * c * x = z. [para(12(a,1),46(a,1))]. given #684 (T,wt=29): 2100 a0 * c * a0 * c * a0 * c != x | y * b0 != x | c * a0 * c * a0 * d = y. [para(4(a,1),790(a,1))]. given #685 (T,wt=29): 2103 x * y * c * a0 != z | u * a * a0 * b0 != z | u * a * a0 = x * y * d. [para(18(a,1),792(b,1,2)),rewrite(5(19)),flip(c)]. given #686 (T,wt=29): 2104 x * y * c * a0 != z | a * a0 * u * b0 != z | a * a0 * u = x * y * d. [para(18(a,1),792(b,1)),rewrite(18(20)),flip(c)]. given #687 (T,wt=29): 2105 x * y * c * a0 != z | u * c * a0 * b0 != z | u * c * a0 = x * y * d. [para(22(a,1),792(b,1,2)),rewrite(6(19)),flip(c)]. given #688 (A,wt=33): 276 x * c0 * a * c0 * a * c0 * a != y | x * b * z != y | d0 * a * c0 * a * c0 = z. [para(4(a,1),51(a,1,2))]. given #689 (T,wt=29): 2106 x * y * c * a0 != z | c * a0 * u * b0 != z | c * a0 * u = x * y * d. [para(22(a,1),792(b,1)),rewrite(22(20)),flip(c)]. given #690 (T,wt=29): 2107 x * y * c * a0 != z | u * a * c0 * b0 != z | u * a * c0 = x * y * d. [para(26(a,1),792(b,1,2)),rewrite(7(19)),flip(c)]. given #691 (T,wt=29): 2108 x * y * c * a0 != z | a * c0 * u * b0 != z | a * c0 * u = x * y * d. [para(26(a,1),792(b,1)),rewrite(26(20)),flip(c)]. given #692 (T,wt=29): 2111 b0 * x * b0 * x * b0 * x != y | c * a0 != y | x * b0 * x * b0 * x = d. [para(4(a,1),794(a,1))]. given #693 (A,wt=33): 278 x * a * c0 * y != z | b * x * b * x * b * x != z | d0 * y = x * b * x * b. [para(4(a,1),51(b,1))]. given #694 (T,wt=29): 2114 c0 * a * c0 * a * c0 * a != x | y * d0 != x | a * c0 * a * c0 * b = y. [para(4(a,1),795(a,1))]. given #695 (T,wt=29): 2117 x * y * a * c0 != z | u * a * a0 * d0 != z | u * a * a0 = x * y * b. [para(18(a,1),797(b,1,2)),rewrite(5(19)),flip(c)]. given #696 (T,wt=29): 2118 x * y * a * c0 != z | a * a0 * u * d0 != z | a * a0 * u = x * y * b. [para(18(a,1),797(b,1)),rewrite(18(20)),flip(c)]. given #697 (T,wt=29): 2119 x * y * a * c0 != z | u * c * a0 * d0 != z | u * c * a0 = x * y * b. [para(22(a,1),797(b,1,2)),rewrite(6(19)),flip(c)]. given #698 (A,wt=33): 280 a * c0 * a * c0 * a * c0 * x != y | c0 * b * z != y | d0 * a * c0 * a * x = z. [para(12(a,1),51(a,1))]. given #699 (T,wt=29): 2120 x * y * a * c0 != z | c * a0 * u * d0 != z | c * a0 * u = x * y * b. [para(22(a,1),797(b,1)),rewrite(22(20)),flip(c)]. given #700 (T,wt=29): 2121 x * y * a * c0 != z | u * a * c0 * d0 != z | u * a * c0 = x * y * b. [para(26(a,1),797(b,1,2)),rewrite(7(19)),flip(c)]. given #701 (T,wt=29): 2122 x * y * a * c0 != z | a * c0 * u * d0 != z | a * c0 * u = x * y * b. [para(26(a,1),797(b,1)),rewrite(26(20)),flip(c)]. given #702 (T,wt=29): 2125 d0 * x * d0 * x * d0 * x != y | a * c0 != y | x * d0 * x * d0 * x = b. [para(4(a,1),799(a,1))]. given #703 (A,wt=33): 284 x * y * z * y * z * y * z != u | v * z * y * z * y != u | x * z * y = v. [para(4(a,1),56(a,1,2))]. given #704 (T,wt=29): 2126 c0 * b0 * d0 * b0 * d0 * b0 != x | a * c0 != x | a0 * d0 * b0 * d0 * b0 = b. [para(370(a,1),799(a,1))]. given #705 (T,wt=29): 2128 a0 * a * a0 * a * a0 * a != x | a * a0 * a * a0 * a * c0 != x | d0 = b0. [para(4(a,1),801(a,1))]. given #706 (T,wt=29): 2129 a * c0 * a * c0 * a * a0 != x | c0 * a * c0 * a * c0 * a != x | d0 = b0. [para(4(a,1),801(b,1))]. given #707 (T,wt=29): 2131 a0 * a * a0 * a * a0 * a != x | a * a0 != x | a * a0 * a * a0 * b = b. [para(4(a,1),802(a,1))]. given #708 (A,wt=33): 292 x * y * x * y * x * y * z != u | v * x * y * x * z != u | y * x * y = v. [para(12(a,1),56(a,1))]. given #709 (T,wt=29): 2133 a0 * a * a0 * a * a0 * a != x | c * a0 != x | a * a0 * a * a0 * b = d. [para(4(a,1),803(a,1))]. given #710 (T,wt=29): 2135 a0 * c * a0 * c * a0 * c != x | a * a0 != x | c * a0 * c * a0 * d = b. [para(4(a,1),804(a,1))]. given #711 (T,wt=29): 2137 a0 * c * a0 * c * a0 * c != x | c * a0 != x | c * a0 * c * a0 * d = d. [para(4(a,1),806(a,1))]. given #712 (T,wt=29): 2139 c0 * a * c0 * a * c0 * a != x | a * c0 != x | a * c0 * a * c0 * b = b. [para(4(a,1),807(a,1))]. given #713 (A,wt=33): 293 x * a * a0 * a * a0 * a * a0 != y | z * a0 * a * a0 * b != y | x * b0 * a = z. [para(21(a,1),56(a,1,2))]. given #714 (T,wt=29): 2142 a * a0 * a * a0 * a * a0 != x | a * a0 * a != x | a0 * a * a0 * b = b. [para(4(a,1),808(a,1))]. given #715 (T,wt=29): 2144 a * a0 * a * a0 * a * a0 != x | a * a0 * b != x | b0 * a * a0 * b = b. [para(21(a,1),808(a,1))]. given #716 (T,wt=29): 2183 a * a0 * a * a0 * a * a0 != x | c * a0 * a != x | a0 * a * a0 * b = d. [para(4(a,1),813(a,1))]. given #717 (T,wt=29): 2185 a * a0 * a * a0 * a * a0 != x | c * a0 * b != x | b0 * a * a0 * b = d. [para(21(a,1),813(a,1))]. given #718 (A,wt=33): 295 x * a * c0 * a * c0 * a * c0 != y | z * c0 * a * c0 * b != y | x * d0 * a = z. [para(29(a,1),56(a,1,2))]. given #719 (T,wt=29): 2195 c * a0 * c * a0 * c * a0 != x | a * a0 * c != x | a0 * c * a0 * d = b. [para(4(a,1),818(a,1))]. given #720 (T,wt=29): 2197 a0 * c * a0 * c * a0 * c != x | a * a0 * d != x | b0 * c * a0 * d = b. [para(45(a,1),818(a,1))]. given #721 (T,wt=29): 2205 c * a0 * c * a0 * c * a0 != x | c * a0 * c != x | a0 * c * a0 * d = d. [para(4(a,1),823(a,1))]. given #722 (T,wt=29): 2207 a0 * c * a0 * c * a0 * c != x | c * a0 * d != x | b0 * c * a0 * d = d. [para(45(a,1),823(a,1))]. given #723 (A,wt=33): 297 x * y * x * y * x * y != z | u * v * y * x * y * x != z | y * x = u * v. [para(4(a,1),57(a,1))]. given #724 (T,wt=29): 2215 a * c0 * a * c0 * a * c0 != x | a * c0 * a != x | c0 * a * c0 * b = b. [para(4(a,1),828(a,1))]. given #725 (T,wt=29): 2217 a * c0 * a * c0 * a * c0 != x | a * c0 * b != x | d0 * a * c0 * b = b. [para(29(a,1),828(a,1))]. given #726 (T,wt=29): 2227 a * a0 * a * a0 != x | y * z * c * a0 != x | a * a0 * b = y * z * d. [para(18(a,1),837(a,1)),rewrite(18(22)),flip(c)]. given #727 (T,wt=29): 2228 c * a0 * a * a0 != x | y * z * c * a0 != x | c * a0 * b = y * z * d. [para(22(a,1),837(a,1)),rewrite(22(22)),flip(c)]. given #728 (A,wt=33): 298 x * y * z * u * z * u != v | u * z * u * z * u * z != v | x * y = z * u. [para(4(a,1),57(b,1))]. given #729 (T,wt=29): 2229 a * c0 * a * a0 != x | y * z * c * a0 != x | a * c0 * b = y * z * d. [para(26(a,1),837(a,1)),rewrite(26(22)),flip(c)]. given #730 (T,wt=29): 2299 c * a0 * c * a0 * c * a0 != x | b0 * c * a0 * c * a0 * y != x | d = y. [para(6(a,1),1740(a,1,2,2,2,2)),rewrite(22(9),22(11),22(19),22(21))]. given #731 (T,wt=29): 2320 a0 * a * a0 * a * a0 * a != x | b0 * a * a0 * a * a0 * y != x | b = y. [para(4(a,1),1747(a,1))]. given #732 (T,wt=29): 2324 c0 * a * c0 * a * c0 * a != x | d0 * a * c0 * a * c0 * y != x | b = y. [para(4(a,1),1749(a,1))]. given #733 (A,wt=33): 302 a * a0 * a * a0 * a * a0 != x | y * z * a0 * a * a0 * b != x | b0 * a = y * z. [para(21(a,1),57(a,1))]. given #734 (T,wt=29): 2334 a0 * a * a0 * a * a0 * a != x | b0 * a * a0 * b * y != x | b0 * b = y. [para(4(a,1),1793(a,1))]. given #735 (T,wt=29): 2338 c0 * a * c0 * a * c0 * a != x | d0 * a * c0 * b * y != x | d0 * b = y. [para(4(a,1),1795(a,1))]. given #736 (T,wt=29): 2349 c * a0 * c * a0 * c * a0 != x | y * d != x | b0 * c * a0 * c * a0 = y. [para(6(a,1),1843(a,1,2,2,2,2)),rewrite(22(9),22(11),6(21),22(23))]. given #737 (T,wt=29): 2352 a0 * a * a0 * a * a0 * a != x | y * b != x | b0 * a * a0 * a * a0 = y. [para(4(a,1),1852(a,1))]. given #738 (A,wt=33): 303 a * c0 * a * c0 * a * c0 != x | y * z * c0 * a * c0 * b != x | d0 * a = y * z. [para(29(a,1),57(a,1))]. given #739 (T,wt=29): 2354 c0 * a * c0 * a * c0 * a != x | y * b != x | d0 * a * c0 * a * c0 = y. [para(4(a,1),1854(a,1))]. given #740 (T,wt=29): 2359 a0 * a * a0 * a * a0 * a != x | y * b0 * b != x | b0 * a * a0 * b = y. [para(4(a,1),1911(a,1))]. given #741 (T,wt=29): 2361 c * a0 * c * a0 * c * a0 != x | a * a0 * d != x | b0 * c * a0 * d = b. [para(18(a,1),1912(b,1))]. given #742 (T,wt=29): 2362 c * a0 * c * a0 * c * a0 != x | c * a0 * d != x | b0 * c * a0 * d = d. [para(22(a,1),1912(b,1))]. given #743 (A,wt=33): 304 x * c * a0 * c * a0 * c * a0 != y | x * b0 * z != y | c * a0 * c * a0 * d = z. [para(6(a,1),31(a,1,2,2,2,2,2)),rewrite(22(9),22(11),22(24),22(26))]. given #744 (T,wt=29): 2364 c0 * a * c0 * a * c0 * a != x | y * d0 * b != x | d0 * a * c0 * b = y. [para(4(a,1),1913(a,1))]. given #745 (T,wt=29): 2378 b0 * a * a0 * a * a0 != x | a0 * a * a0 * a * a0 * a != x | b0 * b = b0. [para(4(a,1),2008(b,1))]. given #746 (T,wt=29): 2383 d0 * a * c0 * a * a0 != x | c0 * a * c0 * a * c0 * a != x | d0 * b = b0. [para(4(a,1),2009(b,1))]. given #747 (T,wt=29): 2396 b0 * a * a0 * a * c0 != x | a0 * a * a0 * a * a0 * a != x | b0 * b = d0. [para(4(a,1),2066(b,1))]. given #748 (A,wt=33): 305 a * a0 * x * b0 * x * b0 * x != y | b * x * z != y | b0 * x * b0 * x * b0 = z. [para(18(a,1),31(a,1))]. given #749 (T,wt=29): 2397 d0 * a * c0 * a * c0 != x | c0 * a * c0 * a * c0 * a != x | d0 * b = d0. [para(4(a,1),2067(b,1))]. given #750 (T,wt=29): 2424 a0 * a * a0 * a * a0 * a != x | a * a0 * b != x | b0 * a * a0 * b = b. [para(4(a,1),2144(a,1))]. given #751 (T,wt=29): 2425 a0 * a * a0 * a * a0 * a != x | c * a0 * b != x | b0 * a * a0 * b = d. [para(4(a,1),2185(a,1))]. given #752 (T,wt=29): 2432 c0 * a * c0 * a * c0 * a != x | a * c0 * b != x | d0 * a * c0 * b = b. [para(4(a,1),2217(a,1))]. given #753 (A,wt=33): 306 c * a0 * x * b0 * x * b0 * x != y | d * x * z != y | b0 * x * b0 * x * b0 = z. [para(22(a,1),31(a,1))]. given #754 (T,wt=31): 458 x * a * c0 * y * d0 * y * d0 * y = x * b * y * d0 * y * d0 * y * d0. [para(50(a,1),1(a,2,2)),rewrite(1(11))]. given #755 (T,wt=31): 680 d0 * a0 * a0 * c0 * a0 * a0 * c0 * a0 = b0 * c0 * a0 * a0 * c0 * a0 * a0 * c0. [hyper(148,a,xx,b,80,a)]. given #756 (T,wt=31): 681 d0 * a0 * c0 * c0 * a0 * c0 * c0 * a0 = b0 * c0 * c0 * a0 * c0 * c0 * a0 * c0. [hyper(148,a,80,a,b,xx)]. given #757 (T,wt=31): 682 d0 * x * d0 * d0 * x * d0 * d0 * x = x * d0 * d0 * x * d0 * d0 * x * d0. [hyper(47,a,26,a(flip),b,80,a)]. given #758 (A,wt=33): 307 a * c0 * x * d0 * x * d0 * x != y | b * x * z != y | d0 * x * d0 * x * d0 = z. [para(26(a,1),31(a,1))]. given #759 (T,wt=31): 683 b0 * x * b0 * b0 * x * b0 * b0 * x = x * b0 * b0 * x * b0 * b0 * x * b0. [hyper(41,a,22,a(flip),b,80,a)]. given #760 (T,wt=31): 800 a0 * d0 * d0 * b0 * d0 * d0 * b0 * d0 = c0 * b0 * d0 * d0 * b0 * d0 * d0 * b0. [hyper(2,a,26,a(flip),b,87,a),flip(a)]. given #761 (T,wt=31): 805 a0 * d0 * b0 * b0 * d0 * b0 * b0 * d0 = c0 * b0 * b0 * d0 * b0 * b0 * d0 * b0. [hyper(2,a,26,a(flip),b,88,a(flip)),flip(a)]. given #762 (T,wt=31): 835 a0 * x * a0 * a0 * x * a0 * a0 * x = x * a0 * a0 * x * a0 * a0 * x * a0. [hyper(2,a,xx,b,90,a),flip(a)]. given #763 (A,wt=33): 308 b * x * d0 * x * d0 * x * d0 != y | a * c0 * z != y | x * d0 * x * d0 * x = z. [para(26(a,1),31(b,1))]. given #764 (T,wt=31): 887 x * y * z * y * z * y * z * z = x * z * z * y * z * y * z * y. [para(111(a,1),1(a,2,2)),rewrite(1(7))]. given #765 (T,wt=31): 895 a * a0 * x * b0 * x * b0 * x * x = b * x * x * b0 * x * b0 * x * b0. [para(111(a,1),18(a,1,2)),flip(a)]. given #766 (T,wt=31): 898 a * a0 * a0 * x * a0 * x * a0 * x = a * x * a0 * x * a0 * x * a0 * a0. [para(111(a,2),18(a,2,2)),rewrite(18(12))]. given #767 (T,wt=27): 2475 a0 * a0 * x * a0 * x * a0 * x = x * a0 * x * a0 * x * a0 * a0. [hyper(2,a,xx,b,898,a),flip(a)]. given #768 (A,wt=33): 309 x * y * x * y * x * y * y != z | y * y * u != z | x * y * x * y * x = u. [para(12(a,1),31(a,1))]. given #769 (T,wt=31): 899 c * a0 * x * b0 * x * b0 * x * x = d * x * x * b0 * x * b0 * x * b0. [para(111(a,1),22(a,1,2)),flip(a)]. given #770 (T,wt=31): 901 c * a0 * a0 * x * a0 * x * a0 * x = c * x * a0 * x * a0 * x * a0 * a0. [para(111(a,2),22(a,2,2)),rewrite(22(12))]. given #771 (T,wt=31): 902 a * c0 * x * d0 * x * d0 * x * x = b * x * x * d0 * x * d0 * x * d0. [para(111(a,1),26(a,1,2)),flip(a)]. given #772 (T,wt=31): 904 a * c0 * d0 * x * d0 * x * d0 * x = b * x * d0 * x * d0 * x * d0 * d0. [para(111(a,2),26(a,1,2)),flip(a)]. given #773 (A,wt=33): 310 x * a0 * a * a0 * a * a0 * a != y | z * b0 * a * a0 * a * a0 != y | x * b = z. [para(4(a,1),67(a,1,2))]. given #774 (T,wt=31): 906 a * c0 * c0 * x * c0 * x * c0 * x = a * x * c0 * x * c0 * x * c0 * c0. [para(111(a,2),26(a,2,2)),rewrite(26(12))]. given #775 (T,wt=27): 2493 c0 * c0 * x * c0 * x * c0 * x = x * c0 * x * c0 * x * c0 * c0. [hyper(2,a,xx,b,906,a),flip(a)]. given #776 (T,wt=31): 917 x * y * x * y * x * y * y * y = y * y * y * x * y * x * y * x. [para(111(a,1),12(a,1,2)),flip(a)]. given #777 (T,wt=31): 1019 x * b * y * b * y * b * y * b0 = x * y * b * y * b * y * a * a0. [para(112(a,1),1(a,2,2)),rewrite(1(11))]. given #778 (A,wt=33): 312 x * a * a0 * y * b0 * y * b0 != z | b0 * y * b0 * y * b0 * y != z | x * b = y. [para(4(a,1),67(b,1))]. given #779 (T,wt=31): 1031 a * c0 * a * c0 * a * c0 * a * a0 = b * a * c0 * a * c0 * a * c0 * b0. [para(112(a,2),26(a,1,2)),rewrite(26(10),26(12),26(14),26(26),26(28)),flip(a)]. given #780 (T,wt=31): 1032 a * c0 * b * c0 * b * c0 * a * a0 = a * b * c0 * b * c0 * b * c0 * b0. [para(112(a,2),26(a,2,2)),rewrite(26(15))]. given #781 (T,wt=27): 2521 c0 * b * c0 * b * c0 * a * a0 = b * c0 * b * c0 * b * c0 * b0. [hyper(2,a,xx,b,1032,a),flip(a)]. given #782 (T,wt=31): 1043 b * x * b * x * b * x * x * b0 = x * x * b * x * b * x * a * a0. [para(112(a,1),12(a,1,2)),flip(a)]. given #783 (A,wt=33): 315 a * a0 * a * a0 * a * a0 * x != y | z * b0 * a * a0 * a * x != y | a0 * b = z. [para(12(a,1),67(a,1))]. given #784 (T,wt=31): 1045 b * b * x * b * x * b * x * b0 = x * b * x * b * x * b * a * a0. [para(112(a,2),12(a,1,2))]. given #785 (T,wt=31): 1071 x * d * y * d * y * d * y * b0 = x * y * d * y * d * y * c * a0. [para(113(a,1),1(a,2,2)),rewrite(1(11))]. given #786 (T,wt=27): 2524 d0 * d * d0 * d * d0 * c * a0 = d * d0 * d * d0 * d * d0 * b0. [hyper(47,a,26,a(flip),b,1071,a)]. given #787 (T,wt=31): 1079 b * d * d0 * d * d0 * d * d0 * b0 = a * c0 * d * d0 * d * d0 * c * a0. [para(113(a,2),26(a,1,2))]. given #788 (A,wt=33): 317 x * b0 * y * b0 * y * b0 * y != z | a * a0 * y * b0 * y * b0 != z | x * y = b. [para(4(a,1),68(a,1,2))]. given #789 (T,wt=31): 1088 d * x * d * x * d * x * x * b0 = x * x * d * x * d * x * c * a0. [para(113(a,1),12(a,1,2)),flip(a)]. given #790 (T,wt=31): 1090 d * d * x * d * x * d * x * b0 = x * d * x * d * x * d * c * a0. [para(113(a,2),12(a,1,2))]. given #791 (T,wt=31): 1116 c0 * x * c0 * c0 * x * c0 * c0 * x = x * c0 * c0 * x * c0 * c0 * x * c0. [hyper(2,a,xx,b,98,a),flip(a)]. given #792 (T,wt=31): 1119 x * b * y * b * y * b * y * d0 = x * y * b * y * b * y * a * c0. [para(114(a,1),1(a,2,2)),rewrite(1(11))]. given #793 (A,wt=33): 319 x * y * b0 * a * a0 * a * a0 != z | a0 * a * a0 * a * a0 * a != z | x * y = b. [para(4(a,1),68(b,1))]. given #794 (T,wt=31): 1131 a * c0 * b * c0 * b * c0 * a * c0 = a * b * c0 * b * c0 * b * c0 * d0. [para(114(a,2),26(a,2,2)),rewrite(26(15))]. given #795 (T,wt=27): 2537 c0 * b * c0 * b * c0 * a * c0 = b * c0 * b * c0 * b * c0 * d0. [hyper(2,a,xx,b,1131,a),flip(a)]. given #796 (T,wt=31): 1142 b * x * b * x * b * x * x * d0 = x * x * b * x * b * x * a * c0. [para(114(a,1),12(a,1,2)),flip(a)]. given #797 (T,wt=31): 1144 b * b * x * b * x * b * x * d0 = x * b * x * b * x * b * a * c0. [para(114(a,2),12(a,1,2))]. given #798 (A,wt=33): 321 x * b0 * x * b0 * x * b0 * y != z | a * a0 * x * b0 * x * y != z | b0 * x = b. [para(12(a,1),68(a,1))]. given #799 (T,wt=31): 1173 b * a * a0 * a * a0 * a * a0 * x = a * a0 * a * a0 * a * a0 * b * x. [para(117(a,1),18(a,1,2))]. given #800 (T,wt=31): 1174 b0 * a * a0 * a * a0 * a * a0 * x = a * a0 * a * a0 * a * a0 * b0 * x. [para(18(a,1),117(a,1,2,2,2,2,2))]. given #801 (T,wt=31): 1175 d * a * a0 * a * a0 * a * a0 * x = c * a0 * a * a0 * a * a0 * b * x. [para(117(a,1),22(a,1,2))]. given #802 (T,wt=31): 1176 a * a0 * a * a0 * a * a0 * d0 * x = b0 * a * a0 * a * a0 * a * c0 * x. [para(26(a,1),117(a,1,2,2,2,2,2)),flip(a)]. given #803 (A,wt=33): 322 x * a0 * c * a0 * c * a0 * c != y | z * b0 * c * a0 * c * a0 != y | x * d = z. [para(4(a,1),69(a,1,2))]. given #804 (T,wt=31): 1193 a * a0 * c * a0 * c * a0 * d * x = b * c * a0 * c * a0 * c * a0 * x. [para(120(a,1),18(a,1,2)),flip(a)]. given #805 (T,wt=31): 1194 d * c * a0 * c * a0 * c * a0 * x = c * a0 * c * a0 * c * a0 * d * x. [para(120(a,1),22(a,1,2))]. given #806 (T,wt=31): 1195 c * a0 * c * a0 * c * a0 * b0 * x = b0 * c * a0 * c * a0 * c * a0 * x. [para(22(a,1),120(a,1,2,2,2,2,2)),flip(a)]. given #807 (T,wt=31): 1208 c * c * c * a0 * c * a0 * c * a0 = c * a0 * c * a0 * c * a0 * c * c. [para(111(a,1),120(a,2,2)),rewrite(120(15)),flip(a)]. given #808 (A,wt=33): 324 x * c * a0 * y * b0 * y * b0 != z | b0 * y * b0 * y * b0 * y != z | x * d = y. [para(4(a,1),69(b,1))]. given #809 (T,wt=27): 2567 c * c * a0 * c * a0 * c * a0 = a0 * c * a0 * c * a0 * c * c. [hyper(106,a,12,a,b,1208,a),flip(a)]. given #810 (T,wt=31): 1213 b * a * c0 * a * c0 * a * c0 * d0 = a * a * c0 * a * c0 * a * c0 * c0. [para(4(a,1),123(a,2,2,2)),rewrite(123(15),1130(15),905(29))]. given #811 (T,wt=31): 1215 d0 * a * c0 * a * c0 * a * a0 * x = a * c0 * a * c0 * a * c0 * b0 * x. [para(18(a,1),123(a,1,2,2,2,2,2))]. given #812 (T,wt=31): 1216 a * c0 * a * c0 * a * c0 * b * x = b * a * c0 * a * c0 * a * c0 * x. [para(123(a,1),26(a,1,2)),flip(a)]. given #813 (A,wt=33): 326 c * a0 * c * a0 * c * a0 * x != y | z * b0 * c * a0 * c * x != y | a0 * d = z. [para(12(a,1),69(a,1))]. given #814 (T,wt=31): 1217 d0 * a * c0 * a * c0 * a * c0 * x = a * c0 * a * c0 * a * c0 * d0 * x. [para(26(a,1),123(a,1,2,2,2,2,2))]. given #815 (T,wt=31): 1268 a * c0 * a * c0 * a * c0 * c0 * b = c0 * b * a * c0 * a * c0 * a * c0. [para(265(a,1),12(a,1,2)),flip(a)]. given #816 (T,wt=31): 1310 d * a0 * c * a0 * c * a0 * c * x = c * a0 * c * a0 * c * a0 * d * x. [para(432(a,1),1(a,1,1)),rewrite(1(14),1(13),1(12),1(11),1(10),1(9),1(27),1(26),1(25),1(24),1(23)),flip(a)]. given #817 (T,wt=31): 1326 d0 * a0 * a0 * c0 * a0 * c0 * a0 * c0 = b0 * c0 * a0 * c0 * a0 * c0 * c0 * a0. [para(4(a,1),531(a,1,2,2))]. given #818 (A,wt=33): 327 x * b0 * y * b0 * y * b0 * y != z | c * a0 * y * b0 * y * b0 != z | x * y = d. [para(4(a,1),70(a,1,2))]. given #819 (T,wt=31): 1332 d0 * c0 * a0 * c0 * a0 * c0 * a0 * x = b0 * c0 * a0 * c0 * a0 * c0 * c0 * x. [para(12(a,1),531(a,1,2))]. given #820 (T,wt=31): 1342 d0 * c0 * c0 * a0 * c0 * a0 * c0 * a0 = b0 * c0 * a0 * c0 * a0 * c0 * c0 * c0. [para(111(a,1),531(a,1,2))]. given #821 (T,wt=31): 1347 a0 * d0 * d0 * b0 * d0 * b0 * d0 * b0 = c0 * b0 * d0 * b0 * d0 * b0 * b0 * d0. [para(4(a,1),548(a,1,2,2))]. given #822 (T,wt=31): 1353 a0 * b0 * d0 * b0 * d0 * b0 * d0 * x = c0 * b0 * d0 * b0 * d0 * b0 * b0 * x. [para(12(a,1),548(a,1,2))]. given #823 (A,wt=33): 329 x * y * b0 * c * a0 * c * a0 != z | a0 * c * a0 * c * a0 * c != z | x * y = d. [para(4(a,1),70(b,1))]. given #824 (T,wt=31): 1367 c0 * b0 * d0 * b0 * d0 * b0 * b0 * b0 = a0 * b0 * b0 * d0 * b0 * d0 * b0 * d0. [para(111(a,1),548(a,1,2)),flip(a)]. given #825 (T,wt=31): 1398 a0 * a0 * a * a0 * a * a0 * a * x = a * a0 * a * a0 * a * a0 * a0 * x. [para(897(a,1),1(a,1,1)),rewrite(1(14),1(13),1(12),1(11),1(10),1(9),1(27),1(26),1(25),1(24),1(23)),flip(a)]. given #826 (T,wt=31): 1404 c * a0 * c * a0 * c * a0 * a0 * b0 = a0 * b0 * a0 * c * a0 * c * a0 * c. [para(900(a,1),12(a,1,2)),flip(a)]. given #827 (T,wt=31): 1437 c0 * c0 * a * c0 * a * c0 * a * x = a * c0 * a * c0 * a * c0 * c0 * x. [para(905(a,1),1(a,1,1)),rewrite(1(14),1(13),1(12),1(11),1(10),1(9),1(27),1(26),1(25),1(24),1(23)),flip(a)]. given #828 (A,wt=33): 330 x * b0 * x * b0 * x * b0 * y != z | c * a0 * x * b0 * x * y != z | b0 * x = d. [para(12(a,1),70(a,1))]. given #829 (T,wt=31): 1438 d * b * d * b * d * a * a0 * x = b * d * b * d * b * c * a0 * x. [para(1025(a,1),1(a,1,1)),rewrite(1(14),1(13),1(12),1(11),1(10),1(9),1(27),1(26),1(25),1(24),1(23)),flip(a)]. given #830 (T,wt=31): 1444 d * b * d * b * d * b * a * a0 = b * b * d * b * d * b * c * a0. [para(1025(a,1),12(a,1,2)),flip(a)]. given #831 (T,wt=31): 1487 b * a0 * a * a0 * a * a0 * a * x = a * a0 * a * a0 * a * a0 * b * x. [para(1231(a,1),1(a,1,1)),rewrite(1(14),1(13),1(12),1(11),1(10),1(9),1(27),1(26),1(25),1(24),1(23)),flip(a)]. given #832 (T,wt=31): 1504 d * a0 * a * a0 * a * a0 * a * x = c * a0 * a * a0 * a * a0 * b * x. [para(1248(a,1),1(a,1,1)),rewrite(1(14),1(13),1(12),1(11),1(10),1(9),1(27),1(26),1(25),1(24),1(23)),flip(a)]. given #833 (A,wt=33): 332 x * c0 * a * c0 * a * c0 * a != y | z * d0 * a * c0 * a * c0 != y | x * b = z. [para(4(a,1),71(a,1,2))]. given #834 (T,wt=31): 1520 c0 * a * c0 * a * c0 * a * b * x = b * a * c0 * a * c0 * a * c0 * x. [para(1269(a,1),1(a,1,1)),rewrite(1(14),1(13),1(12),1(11),1(10),1(9),1(27),1(26),1(25),1(24),1(23)),flip(a)]. given #835 (T,wt=31): 1524 c0 * a * c0 * a * c0 * a * a * b = a * b * a * c0 * a * c0 * a * c0. [para(1269(a,1),12(a,1,2)),flip(a)]. given #836 (T,wt=31): 1554 b0 * a0 * a * a0 * a * a0 * a * x = a * a0 * a * a0 * a * a0 * b0 * x. [para(1384(a,1),1(a,1,1)),rewrite(1(14),1(13),1(12),1(11),1(10),1(9),1(27),1(26),1(25),1(24),1(23)),flip(a)]. given #837 (T,wt=31): 1568 a0 * c * a0 * c * a0 * c * b0 * x = b0 * a0 * c * a0 * c * a0 * c * x. [para(1405(a,1),1(a,1,1)),rewrite(1(14),1(13),1(12),1(11),1(10),1(9),1(27),1(26),1(25),1(24),1(23)),flip(a)]. given #838 (A,wt=33): 334 x * a * c0 * y * d0 * y * d0 != z | d0 * y * d0 * y * d0 * y != z | x * b = y. [para(4(a,1),71(b,1))]. given #839 (T,wt=31): 1572 a0 * c * a0 * c * a0 * c * c * b0 = c * b0 * a0 * c * a0 * c * a0 * c. [para(1405(a,1),12(a,1,2)),flip(a)]. given #840 (T,wt=31): 1582 d0 * c0 * a * c0 * a * c0 * a * x = a * c0 * a * c0 * a * c0 * d0 * x. [para(1421(a,1),1(a,1,1)),rewrite(1(14),1(13),1(12),1(11),1(10),1(9),1(27),1(26),1(25),1(24),1(23)),flip(a)]. given #841 (T,wt=31): 1595 d0 * a * a * c0 * a * c0 * a * c0 = a * c0 * a * c0 * a * c0 * d0 * a. [hyper(176,a,12,a,b,109,a(flip)),rewrite(1217(15)),flip(a)]. given #842 (T,wt=31): 1596 b0 * a * a * a0 * a * a0 * a * a0 = a * a0 * a * a0 * a * a0 * b0 * a. [hyper(147,a,12,a,b,109,a(flip)),rewrite(1174(15)),flip(a)]. given #843 (A,wt=33): 336 a * c0 * a * c0 * a * c0 * x != y | z * d0 * a * c0 * a * x != y | c0 * b = z. [para(12(a,1),71(a,1))]. given #844 (T,wt=31): 1607 d0 * b * a * c0 * a * c0 * a * c0 = a * c0 * a * c0 * a * c0 * d0 * b. [para(7(a,1),110(a,1,2,2,2,2,2,2)),rewrite(26(11),26(13),26(26),26(28),26(30))]. given #845 (T,wt=31): 1611 a * a0 * a * a0 * a * a0 * a0 * a = a0 * a * a * a0 * a * a0 * a * a0. [para(110(a,2),18(a,2)),rewrite(18(15))]. given #846 (T,wt=31): 1614 a0 * c * a0 * c * a0 * c * c * a0 = c * a0 * a0 * c * a0 * c * a0 * c. [para(110(a,1),22(a,2)),rewrite(22(15)),flip(a)]. given #847 (T,wt=31): 1619 a * c0 * a * c0 * a * c0 * c0 * a = c0 * a * a * c0 * a * c0 * a * c0. [para(110(a,2),26(a,2)),rewrite(26(15))]. given #848 (A,wt=33): 338 x * d0 * y * d0 * y * d0 * y != z | a * c0 * y * d0 * y * d0 != z | x * y = b. [para(4(a,1),72(a,1,2))]. given #849 (T,wt=31): 1653 a * d0 * c0 * d0 * c0 * d0 * c0 * c0 = b * c0 * d0 * c0 * d0 * c0 * d0 * d0. [para(111(a,2),122(a,1,2))]. given #850 (T,wt=31): 1690 x * y * y * x * y * x * y * x = x * x * y * x * y * x * y * y. [hyper(2,a,109,a(flip),b,130,a)]. given #851 (T,wt=31): 1703 b * b * a * b * a * b * a * b0 = a * a * b * a * b * a * b * a0. [para(112(a,2),131(a,1,2))]. given #852 (T,wt=31): 1706 d * d * c * d * c * d * c * b0 = c * c * d * c * d * c * d * a0. [para(113(a,2),131(a,1,2))]. given #853 (A,wt=33): 340 x * y * d0 * a * c0 * a * c0 != z | c0 * a * c0 * a * c0 * a != z | x * y = b. [para(4(a,1),72(b,1))]. given #854 (T,wt=31): 1709 b * b * a * b * a * b * a * d0 = a * a * b * a * b * a * b * c0. [para(114(a,2),131(a,1,2))]. given #855 (T,wt=31): 2153 d0 * d0 * x * d0 * x * d0 * x * y = x * d0 * x * d0 * x * d0 * d0 * y. [para(2150(a,1),1(a,1,1)),rewrite(1(11),1(10),1(9),1(8),1(7),1(6),1(21),1(20),1(19),1(18),1(17)),flip(a)]. given #856 (T,wt=31): 2154 x * d0 * d0 * y * d0 * y * d0 * y = x * y * d0 * y * d0 * y * d0 * d0. [para(2150(a,1),1(a,2,2)),rewrite(1(11))]. given #857 (T,wt=31): 2155 d * d0 * d0 * b0 * d0 * b0 * d0 * b0 = c * c0 * b0 * d0 * b0 * d0 * b0 * d0. [para(2150(a,2),22(a,1,2)),rewrite(548(29))]. ============================== PROOF ================================= % Proof 1 at 29.37 (+ 0.03) seconds. % Length of proof is 25. % Level of proof is 7. % Maximum clause weight is 31. % Given clauses 857. 1 (x * y) * z = x * y * z # label(associativity). [assumption]. 2 x * y != z | x * u != z | y = u # label(left_cancellation_extended). [assumption]. 3 x * y != z | u * y != z | x = u # label(right_cancellation_extended). [assumption]. 4 x * y * x * y * x * y = y * x * y * x * y * x # label("(xy)^3 = (yx)^3"). [assumption]. 5 b * b0 = a * a0. [assumption]. 6 d * b0 = c * a0. [assumption]. 7 b * d0 = a * c0. [assumption]. 8 d * d0 != c * c0. [assumption]. 10 x * y * z != u | v * z != u | x * y = v. [para(1(a,1),3(a,1))]. 12 x * y * x * y * x * y * z = y * x * y * x * y * x * z. [para(4(a,1),1(a,1,1)),rewrite(1(6),1(5),1(4),1(3),1(2),1(11),1(10),1(9),1(8))]. 14 x * y * z * y * z * y * z = x * z * y * z * y * z * y. [para(4(a,1),1(a,2,2)),rewrite(1(6))]. 18 b * b0 * x = a * a0 * x. [para(5(a,1),1(a,1,1)),rewrite(1(4)),flip(a)]. 22 d * b0 * x = c * a0 * x. [para(6(a,1),1(a,1,1)),rewrite(1(4)),flip(a)]. 26 b * d0 * x = a * c0 * x. [para(7(a,1),1(a,1,1)),rewrite(1(4)),flip(a)]. 39 b * x * b0 * x * b0 * x * b0 = a * a0 * x * b0 * x * b0 * x. [para(4(a,1),18(a,1,2))]. 47 a * c0 * x != y | b * z != y | d0 * x = z. [para(26(a,1),2(a,1))]. 57 x * y * z != u | v * w * z != u | x * y = v * w. [para(1(a,1),10(b,1))]. 122 a * c0 * x * d0 * x * d0 * x * y = b * x * d0 * x * d0 * x * d0 * y. [para(12(a,1),26(a,1,2)),flip(a)]. 185 x * y * z * u * z * u * z * u = x * y * u * z * u * z * u * z. [para(14(a,1),1(a,1)),rewrite(1(7))]. 370 a0 * d0 * b0 * d0 * b0 * d0 = c0 * b0 * d0 * b0 * d0 * b0. [hyper(2,a,26,a(flip),b,39,a(flip)),flip(a)]. 548 a0 * d0 * b0 * d0 * b0 * d0 * x = c0 * b0 * d0 * b0 * d0 * b0 * x. [para(370(a,1),1(a,1,1)),rewrite(1(12),1(11),1(10),1(9),1(8),1(23),1(22),1(21),1(20)),flip(a)]. 2150 d0 * d0 * x * d0 * x * d0 * x = x * d0 * x * d0 * x * d0 * d0. [hyper(47,a,185,a,b,122,a(flip))]. 2155 d * d0 * d0 * b0 * d0 * b0 * d0 * b0 = c * c0 * b0 * d0 * b0 * d0 * b0 * d0. [para(2150(a,2),22(a,1,2)),rewrite(548(29))]. 2590 d * d0 = c * c0. [hyper(57,a,185,a,b,2155,a),flip(a)]. 2591 $F. [resolve(2590,a,8,a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=857. Generated=199034. Kept=2590. proofs=1. Usable=850. Sos=1652. Demods=234. Limbo=1, Disabled=94. Hints=0. Weight_deleted=140381. Literals_deleted=0. Forward_subsumed=56063. Back_subsumed=41. Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. New_demodulators=284 (0 lex), Back_demodulated=45. Back_unit_deleted=0. Demod_attempts=10270269. Demod_rewrites=814794. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=170465. Nonunit_bsub_feature_tests=9945. Megabytes=3.89. User_CPU=29.37, System_CPU=0.03, Wall_clock=32. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED Exiting with 1 proof. Process 21033 exit (max_proofs) Mon Mar 19 17:02:55 2007