============================== Prover9 =============================== Prover9 (32) version 2009-11A, November 2009. Process 5118 was started by mccune on cleo, Tue Nov 3 09:42:26 2009 The command was "/home/mccune/LADR/bin/prover9 -f quot-xy3b.in". ============================== end of head =========================== ============================== INPUT ================================= % Reading from file quot-xy3b.in assign(max_seconds,120). 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: Predicate symbol precedence: predicate_order([ = ]). Function symbol precedence: function_order([ 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(hyper_resolution). % (nonunit Horn with equality) % set(hyper_resolution) -> set(pos_hyper_resolution). % set(neg_ur_resolution). % (nonunit Horn with equality) % assign(para_lit_limit, 3). % (nonunit Horn with equality) Auto_process settings: (no changes). kept: 1 (x * y) * z = x * y * z # label(associativity). [assumption]. kept: 2 x * y != z | x * u != z | y = u # label(left_cancellation_extended). [assumption]. kept: 3 x * y != z | u * y != z | x = u # label(right_cancellation_extended). [assumption]. kept: 4 x * y * x * y * x * y = y * x * y * x * y * x # label("(xy)^3 = (yx)^3"). [assumption]. kept: 5 b * b0 = a * a0. [assumption]. kept: 6 d * b0 = c * a0. [assumption]. kept: 7 b * d0 = a * c0. [assumption]. kept: 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.01 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 * w != u | z = w. [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 | w * z != u | x * y = w. [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): 152 a * a0 * x != y | c * a0 * x != y | d = b. [para(22(a,1),37(b,1)),flip(c)]. given #50 (T,wt=17): 193 x * a * a0 != y | a * a0 != y | x * b = b. [para(5(a,1),61(b,1))]. given #51 (T,wt=17): 194 x * a * a0 != y | c * a0 != y | x * b = d. [para(6(a,1),61(b,1))]. given #52 (T,wt=17): 196 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): 202 x * c * a0 != y | c * a0 != y | x * d = d. [para(6(a,1),63(b,1))]. given #55 (T,wt=17): 206 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 != w | x * y * z * v5 != w | u = v5. [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 != w | v5 * u != w | x * y * z = v5. [para(1(a,1),10(a,1,2))]. given #62 (T,wt=21): 57 x * y * z != u | w * v5 * z != u | x * y = w * v5. [para(1(a,1),10(b,1))]. given #63 (A,wt=33): 31 x * y * z * y * z * y * z != u | x * z * w != u | y * z * y * z * y = w. [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(b,1)),rewrite([1(5)])]. 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(b,1)),rewrite([1(5)])]. 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(b,1)),rewrite([1(5)])]. 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): 161 c * a0 * x != y | c * a0 * z != y | b0 * x = b0 * z. [para(22(a,1),41(b,1))]. given #85 (T,wt=21): 173 a * c0 * x != y | a * c0 * z != y | d0 * x = d0 * z. [para(26(a,1),47(b,1))]. given #86 (T,wt=21): 191 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): 192 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): 195 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): 200 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): 201 x * c * a0 != y | z * u * b0 != y | x * d = z * u. [para(1(a,1),63(b,1))]. given #92 (T,wt=21): 203 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): 204 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): 205 x * a * c0 != y | z * u * d0 != y | x * b = z * u. [para(1(a,1),65(b,1))]. given #96 (T,wt=21): 207 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): 220 x * y * a * a0 != z | x * y * a * c0 != z | d0 = b0. [para(1(a,1),102(b,1)),rewrite([1(5)])]. 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): 224 x * y * a * a0 != z | a * a0 != z | x * y * b = b. [para(1(a,1),193(a,1)),rewrite([1(13)])]. given #100 (T,wt=21): 225 x * y * a * a0 != z | c * a0 != z | x * y * b = d. [para(1(a,1),194(a,1)),rewrite([1(13)])]. given #101 (T,wt=21): 226 x * y * c * a0 != z | a * a0 != z | x * y * d = b. [para(1(a,1),196(a,1)),rewrite([1(13)])]. given #102 (T,wt=21): 236 x * y * c * a0 != z | c * a0 != z | x * y * d = d. [para(1(a,1),202(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): 237 x * y * a * c0 != z | a * c0 != z | x * y * b = b. [para(1(a,1),206(a,1)),rewrite([1(13)])]. given #105 (T,wt=21): 304 x * a * a0 * y != z | a * a0 * y != z | x * b = b. [para(18(a,1),67(b,1))]. given #106 (T,wt=21): 305 x * a * a0 * y != z | c * a0 * y != z | x * b = d. [para(22(a,1),67(b,1))]. given #107 (T,wt=21): 310 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): 315 x * c * a0 * y != z | c * a0 * y != z | x * d = d. [para(22(a,1),69(b,1))]. given #110 (T,wt=21): 325 x * a * c0 * y != z | a * c0 * y != z | x * b = b. [para(26(a,1),71(b,1))]. given #111 (T,wt=21): 390 x * a * a0 != y | z * a * a0 != y | x * b = z * b. [para(5(a,1),192(b,1,2))]. given #112 (T,wt=21): 391 x * a * a0 != y | z * c * a0 != y | z * d = x * b. [para(6(a,1),192(b,1,2)),flip(c)]. given #113 (A,wt=33): 58 x * y * z * y * z * y * z != u | w * y * z * y * z * y != u | x * z = w. [para(4(a,1),10(a,1,2))]. given #114 (T,wt=21): 392 x * a * a0 != y | a * a0 * b0 != y | a * a0 = x * b. [para(18(a,1),192(b,1)),rewrite([5(16)]),flip(c)]. given #115 (T,wt=21): 393 x * a * a0 != y | c * a0 * b0 != y | c * a0 = x * b. [para(22(a,1),192(b,1)),rewrite([6(16)]),flip(c)]. given #116 (T,wt=21): 394 x * a * a0 != y | a * c0 * b0 != y | a * c0 = x * b. [para(26(a,1),192(b,1)),rewrite([7(16)]),flip(c)]. given #117 (T,wt=21): 411 x * c * a0 != y | z * c * a0 != y | x * d = z * d. [para(6(a,1),201(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): 412 x * c * a0 != y | a * a0 * b0 != y | a * a0 = x * d. [para(18(a,1),201(b,1)),rewrite([5(16)]),flip(c)]. given #120 (T,wt=21): 413 x * c * a0 != y | c * a0 * b0 != y | c * a0 = x * d. [para(22(a,1),201(b,1)),rewrite([6(16)]),flip(c)]. given #121 (T,wt=21): 414 x * c * a0 != y | a * c0 * b0 != y | a * c0 = x * d. [para(26(a,1),201(b,1)),rewrite([7(16)]),flip(c)]. given #122 (T,wt=21): 437 x * a * c0 != y | z * a * c0 != y | x * b = z * b. [para(7(a,1),205(b,1,2))]. given #123 (A,wt=33): 60 x * y * z * u * z * u * z != w | z * u * z * u * z * u != w | x * y = u. [para(4(a,1),10(b,1))]. given #124 (T,wt=21): 438 x * a * c0 != y | a * a0 * d0 != y | a * a0 = x * b. [para(18(a,1),205(b,1)),rewrite([5(16)]),flip(c)]. given #125 (T,wt=21): 439 x * a * c0 != y | c * a0 * d0 != y | c * a0 = x * b. [para(22(a,1),205(b,1)),rewrite([6(16)]),flip(c)]. given #126 (T,wt=21): 440 x * a * c0 != y | a * c0 * d0 != y | a * c0 = x * b. [para(26(a,1),205(b,1)),rewrite([7(16)]),flip(c)]. given #127 (T,wt=23): 178 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): 359 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): 238 x * y * z * u * w != v5 | x * y * z * u * v6 != v5 | w = v6. [para(1(a,1),30(a,1,2,2)),rewrite([1(7)])]. given #131 (T,wt=25): 241 x * y * a * a0 * z != u | x * y * b * w != u | b0 * z = w. [para(18(a,1),30(a,1,2,2))]. given #132 (T,wt=25): 242 x * y * c * a0 * z != u | x * y * d * w != u | b0 * z = w. [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): 243 x * y * a * c0 * z != u | x * y * b * w != u | d0 * z = w. [para(26(a,1),30(a,1,2,2))]. given #135 (T,wt=25): 250 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): 251 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): 265 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): 270 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): 273 x * y * z * u * w != v5 | v6 * w != v5 | x * y * z * u = v6. [para(1(a,1),56(a,1,2,2))]. given #141 (T,wt=25): 274 x * y * z * u != w | v5 * v6 * u != w | x * y * z = v5 * v6. [para(1(a,1),56(b,1))]. given #142 (T,wt=25): 277 x * y * a * a0 * z != u | w * b0 * z != u | x * y * b = w. [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): 278 x * y * z * b0 * u != w | a * a0 * u != w | x * y * z = b. [para(18(a,1),56(b,1))]. given #145 (T,wt=25): 279 x * y * c * a0 * z != u | w * b0 * z != u | x * y * d = w. [para(22(a,1),56(a,1,2,2))]. given #146 (T,wt=25): 280 x * y * z * b0 * u != w | c * a0 * u != w | x * y * z = d. [para(22(a,1),56(b,1))]. given #147 (T,wt=25): 281 x * y * a * c0 * z != u | w * d0 * z != u | x * y * b = w. [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): 282 x * y * z * d0 * u != w | a * c0 * u != w | x * y * z = b. [para(26(a,1),56(b,1))]. given #150 (T,wt=25): 290 x * a * a0 * y != z | u * w * b0 * y != z | x * b = u * w. [para(18(a,1),57(a,1,2))]. given #151 (T,wt=25): 291 x * c * a0 * y != z | u * w * b0 * y != z | x * d = u * w. [para(22(a,1),57(a,1,2))]. given #152 (T,wt=25): 292 x * a * c0 * y != z | u * w * d0 * y != z | x * b = u * w. [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): 331 x * y * z * a * a0 != u | x * y * z * b * w != u | b0 = w. [para(1(a,1),99(b,1,2)),rewrite([1(5)])]. given #155 (T,wt=25): 334 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): 335 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): 345 x * y * z * c * a0 != u | x * y * z * d * w != u | b0 = w. [para(1(a,1),132(b,1,2)),rewrite([1(5)])]. 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): 348 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): 353 x * y * z * a * c0 != u | x * y * z * b * w != u | d0 = w. [para(1(a,1),137(b,1,2)),rewrite([1(5)])]. given #161 (T,wt=25): 356 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): 357 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): 387 x * y * z * a * a0 != u | w * b0 != u | x * y * z * b = w. [para(1(a,1),191(a,1,2)),rewrite([1(13)])]. given #165 (T,wt=25): 388 x * y * a * a0 != z | u * w * b0 != z | x * y * b = u * w. [para(1(a,1),191(b,1))]. given #166 (T,wt=25): 389 x * a * a0 != y | z * u * w * b0 != y | z * u * w = x * b. [para(1(a,1),192(b,1,2)),flip(c)]. given #167 (T,wt=25): 407 x * y * z * u * b0 != w | a * a0 != w | x * y * z * u = b. [para(1(a,1),195(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): 408 x * y * z * c * a0 != u | w * b0 != u | x * y * z * d = w. [para(1(a,1),200(a,1,2)),rewrite([1(13)])]. given #170 (T,wt=25): 409 x * y * c * a0 != z | u * w * b0 != z | x * y * d = u * w. [para(1(a,1),200(b,1))]. given #171 (T,wt=25): 410 x * c * a0 != y | z * u * w * b0 != y | z * u * w = x * d. [para(1(a,1),201(b,1,2)),flip(c)]. given #172 (T,wt=25): 415 x * y * z * u * b0 != w | c * a0 != w | x * y * z * u = d. [para(1(a,1),203(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): 434 x * y * z * a * c0 != u | w * d0 != u | x * y * z * b = w. [para(1(a,1),204(a,1,2)),rewrite([1(13)])]. given #175 (T,wt=25): 435 x * y * a * c0 != z | u * w * d0 != z | x * y * b = u * w. [para(1(a,1),204(b,1))]. given #176 (T,wt=25): 436 x * a * c0 != y | z * u * w * d0 != y | z * u * w = x * b. [para(1(a,1),205(b,1,2)),flip(c)]. given #177 (T,wt=25): 441 x * y * z * u * d0 != w | a * c0 != w | x * y * z * u = b. [para(1(a,1),207(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): 442 x * y * z * a * a0 != u | x * y * z * a * c0 != u | d0 = b0. [para(1(a,1),220(b,1,2)),rewrite([1(5)])]. given #180 (T,wt=25): 443 x * y * z * a * a0 != u | a * a0 != u | x * y * z * b = b. [para(1(a,1),224(a,1,2)),rewrite([1(14)])]. given #181 (T,wt=25): 444 x * y * z * a * a0 != u | c * a0 != u | x * y * z * b = d. [para(1(a,1),225(a,1,2)),rewrite([1(14)])]. given #182 (T,wt=25): 445 x * y * z * c * a0 != u | a * a0 != u | x * y * z * d = b. [para(1(a,1),226(a,1,2)),rewrite([1(14)])]. given #183 (A,wt=31): 88 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 #184 (T,wt=25): 446 x * y * z * c * a0 != u | c * a0 != u | x * y * z * d = d. [para(1(a,1),236(a,1,2)),rewrite([1(14)])]. given #185 (T,wt=25): 464 x * y * z * a * c0 != u | a * c0 != u | x * y * z * b = b. [para(1(a,1),237(a,1,2)),rewrite([1(14)])]. given #186 (T,wt=25): 465 x * y * a * a0 * z != u | a * a0 * z != u | x * y * b = b. [para(1(a,1),304(a,1)),rewrite([1(15)])]. given #187 (T,wt=25): 470 x * y * a * a0 * z != u | c * a0 * z != u | x * y * b = d. [para(1(a,1),305(a,1)),rewrite([1(15)])]. given #188 (A,wt=35): 89 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 #189 (T,wt=25): 476 x * y * c * a0 * z != u | a * a0 * z != u | x * y * d = b. [para(1(a,1),310(a,1)),rewrite([1(15)])]. given #190 (T,wt=25): 482 x * y * c * a0 * z != u | c * a0 * z != u | x * y * d = d. [para(1(a,1),315(a,1)),rewrite([1(15)])]. given #191 (T,wt=25): 487 x * y * a * c0 * z != u | a * c0 * z != u | x * y * b = b. [para(1(a,1),325(a,1)),rewrite([1(15)])]. given #192 (T,wt=25): 492 x * y * a * a0 != z | u * a * a0 != z | x * y * b = u * b. [para(1(a,1),390(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): 493 x * y * a * a0 != z | u * c * a0 != z | x * y * b = u * d. [para(1(a,1),391(a,1)),rewrite([1(16)]),flip(c)]. given #195 (T,wt=25): 494 x * a * a0 != y | z * u * c * a0 != y | z * u * d = x * b. [para(1(a,1),391(b,1)),rewrite([1(14)])]. given #196 (T,wt=25): 498 x * y * a * a0 != z | a * a0 * b0 != z | a * a0 = x * y * b. [para(1(a,1),392(a,1)),rewrite([1(18)])]. given #197 (T,wt=25): 499 x * y * a * a0 != z | c * a0 * b0 != z | c * a0 = x * y * b. [para(1(a,1),393(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): 500 x * y * a * a0 != z | a * c0 * b0 != z | a * c0 = x * y * b. [para(1(a,1),394(a,1)),rewrite([1(18)])]. given #200 (T,wt=25): 501 x * y * c * a0 != z | u * c * a0 != z | x * y * d = u * d. [para(1(a,1),411(a,1)),rewrite([1(14)])]. given #201 (T,wt=25): 503 x * y * c * a0 != z | a * a0 * b0 != z | a * a0 = x * y * d. [para(1(a,1),412(a,1)),rewrite([1(18)])]. given #202 (T,wt=25): 504 x * y * c * a0 != z | c * a0 * b0 != z | c * a0 = x * y * d. [para(1(a,1),413(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): 505 x * y * c * a0 != z | a * c0 * b0 != z | a * c0 = x * y * d. [para(1(a,1),414(a,1)),rewrite([1(18)])]. given #205 (T,wt=25): 506 x * y * a * c0 != z | u * a * c0 != z | x * y * b = u * b. [para(1(a,1),437(a,1)),rewrite([1(14)])]. given #206 (T,wt=25): 513 x * y * a * c0 != z | a * a0 * d0 != z | a * a0 = x * y * b. [para(1(a,1),438(a,1)),rewrite([1(18)])]. given #207 (T,wt=25): 514 x * y * a * c0 != z | c * a0 * d0 != z | c * a0 = x * y * b. [para(1(a,1),439(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): 515 x * y * a * c0 != z | a * c0 * d0 != z | a * c0 = x * y * b. [para(1(a,1),440(a,1)),rewrite([1(18)])]. given #210 (T,wt=25): 650 x * y * z * u != w | a * a0 * u != w | a * a0 = x * y * z. [para(18(a,1),274(b,1)),rewrite([5(14)]),flip(c)]. given #211 (T,wt=25): 653 x * y * z * u != w | c * a0 * u != w | c * a0 = x * y * z. [para(22(a,1),274(b,1)),rewrite([6(14)]),flip(c)]. given #212 (T,wt=25): 656 x * y * z * u != w | a * c0 * u != w | a * c0 = x * y * z. [para(26(a,1),274(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): 699 x * a * a0 * y != z | u * a * a0 * y != z | x * b = u * b. [para(18(a,1),290(b,1,2))]. given #215 (T,wt=25): 700 x * a * a0 * y != z | a * a0 * b0 * y != z | a * a0 = x * b. [para(18(a,1),290(b,1)),rewrite([5(18)]),flip(c)]. given #216 (T,wt=25): 701 x * a * a0 * y != z | u * c * a0 * y != z | u * d = x * b. [para(22(a,1),290(b,1,2)),flip(c)]. given #217 (T,wt=25): 702 x * a * a0 * y != z | c * a0 * b0 * y != z | c * a0 = x * b. [para(22(a,1),290(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): 703 x * a * a0 * y != z | a * c0 * b0 * y != z | a * c0 = x * b. [para(26(a,1),290(b,1)),rewrite([7(18)]),flip(c)]. given #220 (T,wt=25): 708 x * c * a0 * y != z | a * a0 * b0 * y != z | a * a0 = x * d. [para(18(a,1),291(b,1)),rewrite([5(18)]),flip(c)]. given #221 (T,wt=25): 709 x * c * a0 * y != z | u * c * a0 * y != z | x * d = u * d. [para(22(a,1),291(b,1,2))]. given #222 (T,wt=25): 710 x * c * a0 * y != z | c * a0 * b0 * y != z | c * a0 = x * d. [para(22(a,1),291(b,1)),rewrite([6(18)]),flip(c)]. given #223 (A,wt=31): 96 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 #224 (T,wt=25): 711 x * c * a0 * y != z | a * c0 * b0 * y != z | a * c0 = x * d. [para(26(a,1),291(b,1)),rewrite([7(18)]),flip(c)]. given #225 (T,wt=25): 716 x * a * c0 * y != z | a * a0 * d0 * y != z | a * a0 = x * b. [para(18(a,1),292(b,1)),rewrite([5(18)]),flip(c)]. given #226 (T,wt=25): 717 x * a * c0 * y != z | c * a0 * d0 * y != z | c * a0 = x * b. [para(22(a,1),292(b,1)),rewrite([6(18)]),flip(c)]. given #227 (T,wt=25): 718 x * a * c0 * y != z | u * a * c0 * y != z | x * b = u * b. [para(26(a,1),292(b,1,2))]. given #228 (A,wt=35): 97 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 #229 (T,wt=25): 719 x * a * c0 * y != z | a * c0 * d0 * y != z | a * c0 = x * b. [para(26(a,1),292(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): 229 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): 230 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): 256 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): 396 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): 420 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): 421 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): 516 d0 * a0 * c0 * a0 * c0 * a0 * x = b0 * c0 * a0 * c0 * a0 * c0 * x. [para(178(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): 534 a0 * d0 * b0 * d0 * b0 * d0 * x = c0 * b0 * d0 * b0 * d0 * b0 * x. [para(359(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): 882 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): 883 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): 886 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): 889 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 * w != u | x * y * x * y * x * z = w. [para(12(a,1),2(a,1))]. given #254 (T,wt=27): 890 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): 1011 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): 1016 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): 1113 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 | w * x * y * x * y * x * z != u | y = w. [para(12(a,1),3(a,1))]. given #259 (T,wt=27): 1217 b * a0 * a * a0 * a * a0 * a = a * a0 * a * a0 * a * a0 * b. [para(4(a,1),229(a,1,2))]. given #260 (T,wt=27): 1234 d * a0 * a * a0 * a * a0 * a = c * a0 * a * a0 * a * a0 * b. [para(4(a,1),230(a,1,2))]. given #261 (T,wt=27): 1255 c0 * a * c0 * a * c0 * a * b = b * a * c0 * a * c0 * a * c0. [para(256(a,1),12(a,1)),flip(a)]. given #262 (T,wt=27): 1313 d0 * c0 * a0 * c0 * a0 * c0 * a0 = b0 * c0 * a0 * c0 * a0 * c0 * c0. [para(4(a,1),516(a,1,2))]. given #263 (A,wt=33): 108 x * y * z * y * z * y * u != w | y * z * y * z * y * z * u != w | x = z. [para(12(a,1),3(b,1))]. given #264 (T,wt=27): 1334 a0 * b0 * d0 * b0 * d0 * b0 * d0 = c0 * b0 * d0 * b0 * d0 * b0 * b0. [para(4(a,1),534(a,1,2))]. given #265 (T,wt=27): 1370 b0 * a0 * a * a0 * a * a0 * a = a * a0 * a * a0 * a * a0 * b0. [para(4(a,1),882(a,1,2))]. given #266 (T,wt=27): 1391 a0 * c * a0 * c * a0 * c * b0 = b0 * a0 * c * a0 * c * a0 * c. [para(886(a,1),12(a,1)),flip(a)]. given #267 (T,wt=27): 1407 d0 * c0 * a * c0 * a * c0 * a = a * c0 * a * c0 * a * c0 * d0. [para(4(a,1),889(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 a * a0 * x * b0 * x * b0 != y | b0 * x * b0 * x * b0 * x != y | b = x. [para(4(a,1),37(b,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): 159 a0 * c * a0 * c * a0 * c != x | d * y != x | b0 * c * a0 * c * a0 = y. [para(4(a,1),41(a,1))]. given #275 (T,wt=29): 164 a0 * c * a0 * c * a0 * c != x | y * b0 * c * a0 * c * a0 != x | d = y. [para(4(a,1),42(a,1))]. given #276 (T,wt=29): 166 c * a0 * x * b0 * x * b0 != y | b0 * x * b0 * x * b0 * x != y | d = x. [para(4(a,1),42(b,1))]. given #277 (T,wt=29): 171 c0 * a * c0 * a * c0 * a != x | b * y != x | d0 * a * c0 * a * c0 = y. [para(4(a,1),47(a,1))]. given #278 (A,wt=33): 115 x * y * x * y * x * y * z != u | y * x * w != u | y * x * y * x * z = w. [para(12(a,1),9(a,1))]. given #279 (T,wt=29): 176 a * c0 * x * d0 * x * d0 != y | d0 * x * d0 * x * d0 * x != y | b = x. [para(4(a,1),48(b,1))]. given #280 (T,wt=29): 186 a * a0 != x | a0 * a * a0 * a * a0 * a != x | b0 * a * a0 * a * a0 = b0. [para(4(a,1),54(b,1))]. given #281 (T,wt=29): 189 a * a0 != x | c0 * a * c0 * a * c0 * a != x | d0 * a * c0 * a * c0 = b0. [para(4(a,1),55(b,1))]. given #282 (T,wt=29): 197 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 #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): 198 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 #285 (T,wt=29): 199 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 #286 (T,wt=29): 208 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 #287 (T,wt=29): 209 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 #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): 210 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 #290 (T,wt=29): 212 c * a0 != x | a0 * c * a0 * c * a0 * c != x | b0 * c * a0 * c * a0 = b0. [para(4(a,1),75(b,1))]. given #291 (T,wt=29): 215 a * c0 != x | a0 * a * a0 * a * a0 * a != x | b0 * a * a0 * a * a0 = d0. [para(4(a,1),77(b,1))]. given #292 (T,wt=29): 218 a * c0 != x | c0 * a * c0 * a * c0 * a != x | d0 * a * c0 * a * c0 = d0. [para(4(a,1),78(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): 222 a * a0 * c * a0 * c * a0 != x | a0 * c * a0 * c * a0 * c != x | d = b. [para(4(a,1),152(b,1))]. given #295 (T,wt=29): 228 a * a0 * a * a0 * a * a0 != x | b0 * a * y != x | a0 * a * a0 * b = y. [para(21(a,1),9(a,1))]. given #296 (T,wt=29): 232 a * a0 * a * a0 * a * a0 != x | y * a0 * a * a0 * b != x | b0 * a = y. [para(21(a,1),10(a,1))]. given #297 (T,wt=29): 240 x * y * x * y * x * y != z | y * x * y * u != z | x * y * x = u. [para(4(a,1),30(a,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): 246 a * a0 * a * a0 * a * a0 != x | b0 * a * a0 * y != x | a * a0 * b = y. [para(21(a,1),30(a,1))]. given #300 (T,wt=29): 248 a * a0 * a * a0 * a * a0 != x | a0 * b * y != x | b0 * a * a0 * a = y. [para(4(a,1),40(a,1))]. given #301 (T,wt=29): 253 a * a0 * a * a0 * a * a0 != x | b0 * b * y != x | b0 * a * a0 * b = y. [para(21(a,1),40(a,1))]. given #302 (T,wt=29): 255 a * c0 * a * c0 * a * c0 != x | d0 * a * y != x | c0 * a * c0 * b = y. [para(29(a,1),9(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): 258 a * c0 * a * c0 * a * c0 != x | y * c0 * a * c0 * b != x | d0 * a = y. [para(29(a,1),10(a,1))]. given #305 (T,wt=29): 261 a * c0 * a * c0 * a * c0 != x | d0 * a * c0 * y != x | a * c0 * b = y. [para(29(a,1),30(a,1))]. given #306 (T,wt=29): 263 c * a0 * c * a0 * c * a0 != x | a0 * d * y != x | b0 * c * a0 * c = y. [para(4(a,1),46(a,1))]. given #307 (T,wt=29): 268 a * c0 * a * c0 * a * c0 != x | c0 * b * y != x | d0 * a * c0 * a = y. [para(4(a,1),51(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): 272 a * c0 * a * c0 * a * c0 != x | d0 * b * y != x | d0 * a * c0 * b = y. [para(29(a,1),51(a,1))]. given #310 (T,wt=29): 276 x * y * x * y * x * y != z | u * x * y * x != z | y * x * y = u. [para(4(a,1),56(a,1))]. given #311 (T,wt=29): 285 a * a0 * a * a0 * a * a0 != x | y * a * a0 * b != x | b0 * a * a0 = y. [para(21(a,1),56(a,1))]. given #312 (T,wt=29): 287 a * c0 * a * c0 * a * c0 != x | y * a * c0 * b != x | d0 * a * c0 = y. [para(29(a,1),56(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): 302 a * a0 * a * a0 * a * a0 != x | y * b0 * a * a0 * a != x | a0 * b = y. [para(4(a,1),67(a,1))]. given #315 (T,wt=29): 307 a * a0 * a * a0 * a * a0 != x | y * b0 * a * a0 * b != x | b0 * b = y. [para(21(a,1),67(a,1))]. given #316 (T,wt=29): 309 x * b0 * x * b0 * x * b0 != y | a * a0 * x * b0 * x != y | b0 * x = b. [para(4(a,1),68(a,1))]. given #317 (T,wt=29): 313 c * a0 * c * a0 * c * a0 != x | y * b0 * c * a0 * c != x | a0 * d = y. [para(4(a,1),69(a,1))]. given #318 (A,wt=33): 126 x * y * x * y * x * y * z != u | w * y * x * y * x * z != u | y * x = w. [para(12(a,1),10(a,1))]. given #319 (T,wt=29): 318 x * b0 * x * b0 * x * b0 != y | c * a0 * x * b0 * x != y | b0 * x = d. [para(4(a,1),70(a,1))]. given #320 (T,wt=29): 321 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 #321 (T,wt=29): 323 a * c0 * a * c0 * a * c0 != x | y * d0 * a * c0 * a != x | c0 * b = y. [para(4(a,1),71(a,1))]. given #322 (T,wt=29): 327 a * c0 * a * c0 * a * c0 != x | y * d0 * a * c0 * b != x | d0 * b = y. [para(29(a,1),71(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): 329 x * d0 * x * d0 * x * d0 != y | a * c0 * x * d0 * x != y | d0 * x = b. [para(4(a,1),72(a,1))]. given #325 (T,wt=29): 333 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 #326 (T,wt=29): 338 a0 * a * a0 != x | a * a0 * a * a0 * a * a0 != x | b0 * a * a0 * a = b0. [para(4(a,1),103(b,1))]. given #327 (T,wt=29): 340 b0 * a * a0 != x | a * a0 * a * a0 * a * a0 != x | b0 * a * a0 * b = b0. [para(21(a,1),103(b,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): 342 c0 * a * a0 != x | a * c0 * a * c0 * a * c0 != x | d0 * a * c0 * a = b0. [para(4(a,1),104(b,1))]. given #330 (T,wt=29): 344 d0 * a * a0 != x | a * c0 * a * c0 * a * c0 != x | d0 * a * c0 * b = b0. [para(29(a,1),104(b,1))]. given #331 (T,wt=29): 347 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 #332 (T,wt=29): 351 a0 * c * a0 != x | c * a0 * c * a0 * c * a0 != x | b0 * c * a0 * c = b0. [para(4(a,1),135(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 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 #335 (T,wt=29): 373 a0 * a * c0 != x | a * a0 * a * a0 * a * a0 != x | b0 * a * a0 * a = d0. [para(4(a,1),140(b,1))]. given #336 (T,wt=29): 375 b0 * a * c0 != x | a * a0 * a * a0 * a * a0 != x | b0 * a * a0 * b = d0. [para(21(a,1),140(b,1))]. given #337 (T,wt=29): 377 c0 * a * c0 != x | a * c0 * a * c0 * a * c0 != x | d0 * a * c0 * a = d0. [para(4(a,1),141(b,1))]. 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): 379 d0 * a * c0 != x | a * c0 * a * c0 * a * c0 != x | d0 * a * c0 * b = d0. [para(29(a,1),141(b,1))]. given #340 (T,wt=29): 416 a0 * c * a0 * c * a0 * c != x | b0 * y != x | c * a0 * c * a0 * d = y. [para(45(a,1),2(a,1))]. given #341 (T,wt=29): 417 a0 * c * a0 * c * a0 * c != x | y * c * a0 * c * a0 * d != x | b0 = y. [para(45(a,1),3(a,1))]. given #342 (T,wt=29): 419 a0 * c * a0 * c * a0 * c != x | b0 * c * y != x | a0 * c * a0 * d = y. [para(45(a,1),9(a,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): 423 a0 * c * a0 * c * a0 * c != x | y * a0 * c * a0 * d != x | b0 * c = y. [para(45(a,1),10(a,1))]. given #345 (T,wt=29): 427 a0 * c * a0 * c * a0 * c != x | b0 * c * a0 * y != x | c * a0 * d = y. [para(45(a,1),30(a,1))]. given #346 (T,wt=29): 428 a0 * c * a0 * c * a0 * c != x | b0 * d * y != x | b0 * c * a0 * d = y. [para(45(a,1),46(a,1))]. given #347 (T,wt=29): 430 a0 * c * a0 * c * a0 * c != x | y * c * a0 * d != x | b0 * c * a0 = y. [para(45(a,1),56(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): 432 a0 * c * a0 * c * a0 * c != x | y * b0 * c * a0 * d != x | b0 * d = y. [para(45(a,1),69(a,1))]. given #350 (T,wt=29): 433 b0 * c * a0 != x | a0 * c * a0 * c * a0 * c != x | b0 * c * a0 * d = b0. [para(45(a,1),135(b,1))]. given #351 (T,wt=29): 467 a * a0 * a * a0 * a * a0 != x | a * a0 * a * a0 * a != x | a0 * b = b. [para(4(a,1),304(a,1))]. given #352 (T,wt=29): 469 a * a0 * a * a0 * a * a0 != x | a * a0 * a * a0 * b != x | b0 * b = b. [para(21(a,1),304(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): 472 a * a0 * a * a0 * a * a0 != x | c * a0 * a * a0 * a != x | a0 * b = d. [para(4(a,1),305(a,1))]. given #355 (T,wt=29): 475 a * a0 * a * a0 * a * a0 != x | c * a0 * a * a0 * b != x | b0 * b = d. [para(21(a,1),305(a,1))]. given #356 (T,wt=29): 478 c * a0 * c * a0 * c * a0 != x | a * a0 * c * a0 * c != x | a0 * d = b. [para(4(a,1),310(a,1))]. given #357 (T,wt=29): 480 a0 * c * a0 * c * a0 * c != x | a * a0 * c * a0 * d != x | b0 * d = b. [para(45(a,1),310(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): 481 a * a0 != x | b * y * b * y * b * y != x | y * b * y * b * y = b0. [para(4(a,1),52(b,1))]. given #360 (T,wt=29): 484 c * a0 * c * a0 * c * a0 != x | c * a0 * c * a0 * c != x | a0 * d = d. [para(4(a,1),315(a,1))]. given #361 (T,wt=29): 486 a0 * c * a0 * c * a0 * c != x | c * a0 * c * a0 * d != x | b0 * d = d. [para(45(a,1),315(a,1))]. given #362 (T,wt=29): 489 a * c0 * a * c0 * a * c0 != x | a * c0 * a * c0 * a != x | c0 * b = b. [para(4(a,1),325(a,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): 491 a * c0 * a * c0 * a * c0 != x | a * c0 * a * c0 * b != x | d0 * b = b. [para(29(a,1),325(a,1))]. given #365 (T,wt=29): 502 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 #366 (T,wt=29): 517 b0 * c0 * a0 * c0 * a0 * c0 != x | d0 * y != x | a0 * c0 * a0 * c0 * a0 = y. [para(178(a,1),2(a,1))]. given #367 (T,wt=29): 518 b0 * c0 * a0 * c0 * a0 * c0 != x | y * a0 * c0 * a0 * c0 * a0 != x | d0 = y. [para(178(a,1),3(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): 520 b0 * c0 * a0 * c0 * a0 * c0 != x | d0 * a0 * y != x | c0 * a0 * c0 * a0 = y. [para(178(a,1),9(a,1))]. given #370 (T,wt=29): 522 b0 * c0 * a0 * c0 * a0 * c0 != x | y * c0 * a0 * c0 * a0 != x | d0 * a0 = y. [para(178(a,1),10(a,1))]. given #371 (T,wt=29): 525 a0 * c0 * a0 * c0 * a0 * c0 != x | b0 * c0 * a0 * c0 * a0 * c0 != x | d0 = c0. [para(178(a,1),16(b,1)),flip(c)]. given #372 (T,wt=29): 527 b0 * c0 * a0 * c0 * a0 * c0 != x | d0 * a0 * c0 * y != x | a0 * c0 * a0 = y. [para(178(a,1),30(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): 529 b0 * c0 * a0 * c0 * a0 * c0 != x | y * a0 * c0 * a0 != x | d0 * a0 * c0 = y. [para(178(a,1),56(a,1))]. given #375 (T,wt=29): 533 c * a0 != x | d * y * d * y * d * y != x | y * d * y * d * y = b0. [para(4(a,1),74(b,1))]. given #376 (T,wt=29): 535 c0 * b0 * d0 * b0 * d0 * b0 != x | a0 * y != x | d0 * b0 * d0 * b0 * d0 = y. [para(359(a,1),2(a,1))]. given #377 (T,wt=29): 536 c0 * b0 * d0 * b0 * d0 * b0 != x | y * d0 * b0 * d0 * b0 * d0 != x | a0 = y. [para(359(a,1),3(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): 538 c0 * b0 * d0 * b0 * d0 * b0 != x | a0 * d0 * y != x | b0 * d0 * b0 * d0 = y. [para(359(a,1),9(a,1))]. given #380 (T,wt=29): 540 c0 * b0 * d0 * b0 * d0 * b0 != x | y * b0 * d0 * b0 * d0 != x | a0 * d0 = y. [para(359(a,1),10(a,1))]. given #381 (T,wt=29): 544 a * c0 * b0 * d0 * b0 * d0 != x | c0 * b0 * d0 * b0 * d0 * b0 != x | b = a0. [para(359(a,1),48(b,1))]. given #382 (T,wt=29): 545 d0 * b0 * d0 * b0 * d0 * b0 != x | c0 * b0 * d0 * b0 * d0 * b0 != x | b0 = a0. [para(359(a,1),16(b,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): 548 c0 * b0 * d0 * b0 * d0 * b0 != x | a0 * d0 * b0 * y != x | d0 * b0 * d0 = y. [para(359(a,1),30(a,1))]. given #385 (T,wt=29): 550 c0 * b0 * d0 * b0 * d0 * b0 != x | y * d0 * b0 * d0 != x | a0 * d0 * b0 = y. [para(359(a,1),56(a,1))]. given #386 (T,wt=29): 552 c0 * b0 * d0 * b0 * d0 * b0 != x | a * a0 * d0 * b0 * d0 != x | a0 * d0 = b. [para(359(a,1),68(a,1))]. given #387 (T,wt=29): 553 c0 * b0 * d0 * b0 * d0 * b0 != x | c * a0 * d0 * b0 * d0 != x | a0 * d0 = d. [para(359(a,1),70(a,1))]. given #388 (A,wt=33): 150 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 #389 (T,wt=29): 558 x * y * z * u * w * v5 != v6 | x * y * z * u * w * v7 != v6 | v5 = v7. [para(1(a,1),238(a,1,2,2,2)),rewrite([1(8)])]. given #390 (T,wt=29): 560 x * y * x * y * x * y != z | y * x * y * x * u != z | y * x = u. [para(4(a,1),238(a,1))]. given #391 (T,wt=29): 561 x * y * z * a * a0 * u != w | x * y * z * b * v5 != w | b0 * u = v5. [para(18(a,1),238(a,1,2,2,2))]. given #392 (T,wt=29): 562 x * y * z * c * a0 * u != w | x * y * z * d * v5 != w | b0 * u = v5. [para(22(a,1),238(a,1,2,2,2))]. given #393 (A,wt=33): 153 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 #394 (T,wt=29): 563 x * y * z * a * c0 * u != w | x * y * z * b * v5 != w | d0 * u = v5. [para(26(a,1),238(a,1,2,2,2))]. given #395 (T,wt=29): 566 a * a0 * a * a0 * a * a0 != x | b0 * a * a0 * a * y != x | a0 * b = y. [para(21(a,1),238(a,1))]. given #396 (T,wt=29): 568 a * c0 * a * c0 * a * c0 != x | d0 * a * c0 * a * y != x | c0 * b = y. [para(29(a,1),238(a,1))]. given #397 (T,wt=29): 572 a0 * c * a0 * c * a0 * c != x | b0 * c * a0 * c * y != x | a0 * d = y. [para(45(a,1),238(a,1))]. given #398 (A,wt=35): 155 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 #399 (T,wt=29): 576 b0 * c0 * a0 * c0 * a0 * c0 != x | d0 * a0 * c0 * a0 * y != x | c0 * a0 = y. [para(178(a,1),238(a,1))]. given #400 (T,wt=29): 578 c0 * b0 * d0 * b0 * d0 * b0 != x | a0 * d0 * b0 * d0 * y != x | b0 * d0 = y. [para(359(a,1),238(a,1))]. given #401 (T,wt=29): 580 a0 * a * a0 * a * a0 * a != x | a * a0 * b * y != x | b0 * a * a0 = y. [para(4(a,1),241(a,1))]. given #402 (T,wt=29): 582 x * y * a * a0 * z != u | x * y * a * a0 * w != u | b0 * z = b0 * w. [para(18(a,1),241(b,1,2,2))]. given #403 (A,wt=35): 156 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 #404 (T,wt=29): 583 x * y * a * a0 * z != u | x * y * a * c0 * w != u | d0 * w = b0 * z. [para(26(a,1),241(b,1,2,2)),flip(c)]. given #405 (T,wt=29): 587 a0 * c * a0 * c * a0 * c != x | c * a0 * d * y != x | b0 * c * a0 = y. [para(4(a,1),242(a,1))]. given #406 (T,wt=29): 589 x * y * c * a0 * z != u | x * y * c * a0 * w != u | b0 * z = b0 * w. [para(22(a,1),242(b,1,2,2))]. given #407 (T,wt=29): 592 a * c0 != x | b * y * b * y * b * y != x | y * b * y * b * y = d0. [para(4(a,1),76(b,1))]. given #408 (A,wt=35): 157 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 #409 (T,wt=29): 594 c0 * a * c0 * a * c0 * a != x | a * c0 * b * y != x | d0 * a * c0 = y. [para(4(a,1),243(a,1))]. given #410 (T,wt=29): 596 x * y * a * c0 * z != u | x * y * a * c0 * w != u | d0 * z = d0 * w. [para(26(a,1),243(b,1,2,2))]. given #411 (T,wt=29): 621 x * y * z * u * w * v5 != v6 | v7 * v5 != v6 | x * y * z * u * w = v7. [para(1(a,1),273(a,1,2,2,2))]. given #412 (T,wt=29): 622 x * y * z * u * w != v5 | v6 * v7 * w != v5 | x * y * z * u = v6 * v7. [para(1(a,1),273(b,1))]. given #413 (A,wt=33): 158 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 #414 (T,wt=29): 624 x * y * x * y * x * y != z | u * y * x != z | y * x * y * x = u. [para(4(a,1),273(a,1))]. given #415 (T,wt=29): 625 x * y * z * a * a0 * u != w | v5 * b0 * u != w | x * y * z * b = v5. [para(18(a,1),273(a,1,2,2,2))]. given #416 (T,wt=29): 626 x * y * z * u * b0 * w != v5 | a * a0 * w != v5 | x * y * z * u = b. [para(18(a,1),273(b,1))]. given #417 (T,wt=29): 627 x * y * z * c * a0 * u != w | v5 * b0 * u != w | x * y * z * d = v5. [para(22(a,1),273(a,1,2,2,2))]. given #418 (A,wt=33): 160 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 #419 (T,wt=29): 628 x * y * z * u * b0 * w != v5 | c * a0 * w != v5 | x * y * z * u = d. [para(22(a,1),273(b,1))]. given #420 (T,wt=29): 629 x * y * z * a * c0 * u != w | v5 * d0 * u != w | x * y * z * b = v5. [para(26(a,1),273(a,1,2,2,2))]. given #421 (T,wt=29): 630 x * y * z * u * d0 * w != v5 | a * c0 * w != v5 | x * y * z * u = b. [para(26(a,1),273(b,1))]. given #422 (T,wt=29): 633 a * a0 * a * a0 * a * a0 != x | y * a0 * b != x | b0 * a * a0 * a = y. [para(21(a,1),273(a,1))]. given #423 (A,wt=33): 162 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 #424 (T,wt=29): 635 a * c0 * a * c0 * a * c0 != x | y * c0 * b != x | d0 * a * c0 * a = y. [para(29(a,1),273(a,1))]. given #425 (T,wt=29): 639 a0 * c * a0 * c * a0 * c != x | y * a0 * d != x | b0 * c * a0 * c = y. [para(45(a,1),273(a,1))]. given #426 (T,wt=29): 643 b0 * c0 * a0 * c0 * a0 * c0 != x | y * c0 * a0 != x | d0 * a0 * c0 * a0 = y. [para(178(a,1),273(a,1))]. given #427 (T,wt=29): 645 c0 * b0 * d0 * b0 * d0 * b0 != x | y * b0 * d0 != x | a0 * d0 * b0 * d0 = y. [para(359(a,1),273(a,1))]. given #428 (A,wt=33): 163 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 #429 (T,wt=29): 646 x * y * z * u != w | v5 * v6 * v7 * u != w | x * y * z = v5 * v6 * v7. [para(1(a,1),274(b,1,2))]. given #430 (T,wt=29): 648 x * y * a * a0 * z != u | w * v5 * b0 * z != u | x * y * b = w * v5. [para(18(a,1),274(a,1,2,2))]. given #431 (T,wt=29): 649 x * y * z * b0 * u != w | v5 * a * a0 * u != w | x * y * z = v5 * b. [para(18(a,1),274(b,1,2))]. given #432 (T,wt=29): 651 x * y * c * a0 * z != u | w * v5 * b0 * z != u | x * y * d = w * v5. [para(22(a,1),274(a,1,2,2))]. given #433 (A,wt=33): 165 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 #434 (T,wt=29): 652 x * y * z * b0 * u != w | v5 * c * a0 * u != w | x * y * z = v5 * d. [para(22(a,1),274(b,1,2))]. given #435 (T,wt=29): 654 x * y * a * c0 * z != u | w * v5 * d0 * z != u | x * y * b = w * v5. [para(26(a,1),274(a,1,2,2))]. given #436 (T,wt=29): 655 x * y * z * d0 * u != w | v5 * a * c0 * u != w | x * y * z = v5 * b. [para(26(a,1),274(b,1,2))]. given #437 (T,wt=29): 663 a0 * a * a0 * a * a0 * a != x | y * b0 * a * a0 != x | a * a0 * b = y. [para(4(a,1),277(a,1))]. given #438 (A,wt=33): 167 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 #439 (T,wt=29): 671 b0 * x * b0 * x * b0 * x != y | a * a0 * x * b0 != y | x * b0 * x = b. [para(4(a,1),278(a,1))]. given #440 (T,wt=29): 676 a0 * c * a0 * c * a0 * c != x | y * b0 * c * a0 != x | c * a0 * d = y. [para(4(a,1),279(a,1))]. given #441 (T,wt=29): 680 b0 * x * b0 * x * b0 * x != y | c * a0 * x * b0 != y | x * b0 * x = d. [para(4(a,1),280(a,1))]. given #442 (T,wt=29): 685 c0 * a * c0 * a * c0 * a != x | y * d0 * a * c0 != x | a * c0 * b = y. [para(4(a,1),281(a,1))]. given #443 (A,wt=33): 168 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 #444 (T,wt=29): 692 d0 * x * d0 * x * d0 * x != y | a * c0 * x * d0 != y | x * d0 * x = b. [para(4(a,1),282(a,1))]. given #445 (T,wt=29): 696 c0 * b0 * d0 * b0 * d0 * b0 != x | a * c0 * b0 * d0 != x | a0 * d0 * b0 = b. [para(359(a,1),282(a,1))]. given #446 (T,wt=29): 723 x * y * z * u * a * a0 != w | x * y * z * u * b * v5 != w | b0 = v5. [para(1(a,1),331(b,1,2,2)),rewrite([1(5)])]. given #447 (T,wt=29): 725 x * b * x * a * a0 != y | b * x * b * x * b * x != y | x * b = b0. [para(4(a,1),331(b,1)),flip(c)]. given #448 (A,wt=35): 169 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 #449 (T,wt=29): 726 x * y * z * a * a0 != u | x * y * z * a * a0 * w != u | b0 * w = b0. [para(18(a,1),331(b,1,2,2,2)),flip(c)]. given #450 (T,wt=29): 727 x * y * z * a * a0 != u | x * y * z * a * c0 * w != u | d0 * w = b0. [para(26(a,1),331(b,1,2,2,2)),flip(c)]. given #451 (T,wt=29): 732 a * a0 * a * a0 != x | a0 * a * a0 * a * a0 * a != x | b0 * a * a0 = b0. [para(4(a,1),334(b,1))]. given #452 (T,wt=29): 736 a * c0 * a * a0 != x | c0 * a * c0 * a * c0 * a != x | d0 * a * c0 = b0. [para(4(a,1),335(b,1))]. given #453 (A,wt=33): 170 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 #454 (T,wt=29): 739 x * y * z * u * c * a0 != w | x * y * z * u * d * v5 != w | b0 = v5. [para(1(a,1),345(b,1,2,2)),rewrite([1(5)])]. given #455 (T,wt=29): 741 x * d * x * c * a0 != y | d * x * d * x * d * x != y | x * d = b0. [para(4(a,1),345(b,1)),flip(c)]. given #456 (T,wt=29): 742 x * y * z * c * a0 != u | x * y * z * c * a0 * w != u | b0 * w = b0. [para(22(a,1),345(b,1,2,2,2)),flip(c)]. given #457 (T,wt=29): 748 c * a0 * c * a0 != x | a0 * c * a0 * c * a0 * c != x | b0 * c * a0 = b0. [para(4(a,1),348(b,1))]. given #458 (A,wt=33): 172 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 #459 (T,wt=29): 751 x * y * z * u * a * c0 != w | x * y * z * u * b * v5 != w | d0 = v5. [para(1(a,1),353(b,1,2,2)),rewrite([1(5)])]. given #460 (T,wt=29): 753 x * b * x * a * c0 != y | b * x * b * x * b * x != y | x * b = d0. [para(4(a,1),353(b,1)),flip(c)]. given #461 (T,wt=29): 754 x * y * z * a * c0 != u | x * y * z * a * a0 * w != u | b0 * w = d0. [para(18(a,1),353(b,1,2,2,2)),flip(c)]. given #462 (T,wt=29): 755 x * y * z * a * c0 != u | x * y * z * a * c0 * w != u | d0 * w = d0. [para(26(a,1),353(b,1,2,2,2)),flip(c)]. given #463 (A,wt=33): 174 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 #464 (T,wt=29): 760 a * a0 * a * c0 != x | a0 * a * a0 * a * a0 * a != x | b0 * a * a0 = d0. [para(4(a,1),356(b,1))]. given #465 (T,wt=29): 764 a * c0 * a * c0 != x | c0 * a * c0 * a * c0 * a != x | d0 * a * c0 = d0. [para(4(a,1),357(b,1))]. given #466 (T,wt=29): 769 x * y * z * u * a * a0 != w | v5 * b0 != w | x * y * z * u * b = v5. [para(1(a,1),387(a,1,2,2)),rewrite([1(14)])]. given #467 (T,wt=29): 770 x * y * z * a * a0 != u | w * v5 * b0 != u | x * y * z * b = w * v5. [para(1(a,1),387(b,1))]. given #468 (A,wt=33): 175 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 #469 (T,wt=29): 771 x * y * a * a0 != z | u * w * v5 * b0 != z | x * y * b = u * w * v5. [para(1(a,1),388(b,1,2))]. given #470 (T,wt=29): 772 x * a * a0 != y | z * u * w * v5 * b0 != y | z * u * w * v5 = x * b. [para(1(a,1),389(b,1,2,2))]. given #471 (T,wt=29): 773 x * y * z * u * w * b0 != v5 | a * a0 != v5 | x * y * z * u * w = b. [para(1(a,1),407(a,1,2,2,2))]. given #472 (T,wt=29): 776 x * y * z * u * c * a0 != w | v5 * b0 != w | x * y * z * u * d = v5. [para(1(a,1),408(a,1,2,2)),rewrite([1(14)])]. given #473 (A,wt=33): 177 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 #474 (T,wt=29): 777 x * y * z * c * a0 != u | w * v5 * b0 != u | x * y * z * d = w * v5. [para(1(a,1),408(b,1))]. given #475 (T,wt=29): 778 x * y * c * a0 != z | u * w * v5 * b0 != z | x * y * d = u * w * v5. [para(1(a,1),409(b,1,2))]. given #476 (T,wt=29): 779 x * c * a0 != y | z * u * w * v5 * b0 != y | z * u * w * v5 = x * d. [para(1(a,1),410(b,1,2,2))]. given #477 (T,wt=29): 780 x * y * z * u * w * b0 != v5 | c * a0 != v5 | x * y * z * u * w = d. [para(1(a,1),415(a,1,2,2,2))]. given #478 (A,wt=31): 179 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 #479 (T,wt=27): 2077 d0 * d0 * x * d0 * x * d0 * x = x * d0 * x * d0 * x * d0 * d0. [hyper(47,a,179,a,b,122,a(flip))]. given #480 (T,wt=27): 2078 b0 * b0 * x * b0 * x * b0 * x = x * b0 * x * b0 * x * b0 * b0. [hyper(41,a,179,a,b,119,a)]. given #481 (T,wt=29): 781 x * y * z * u * a * c0 != w | v5 * d0 != w | x * y * z * u * b = v5. [para(1(a,1),434(a,1,2,2)),rewrite([1(14)])]. given #482 (T,wt=29): 782 x * y * z * a * c0 != u | w * v5 * d0 != u | x * y * z * b = w * v5. [para(1(a,1),434(b,1))]. given #483 (A,wt=33): 180 x * y * z * y * z * y * z != u | x * w != u | z * y * z * y * z * y = w. [para(14(a,1),2(a,1))]. given #484 (T,wt=29): 783 x * y * a * c0 != z | u * w * v5 * d0 != z | x * y * b = u * w * v5. [para(1(a,1),435(b,1,2))]. given #485 (T,wt=29): 784 x * a * c0 != y | z * u * w * v5 * d0 != y | z * u * w * v5 = x * b. [para(1(a,1),436(b,1,2,2))]. given #486 (T,wt=29): 785 x * y * z * u * w * d0 != v5 | a * c0 != v5 | x * y * z * u * w = b. [para(1(a,1),441(a,1,2,2,2))]. given #487 (T,wt=29): 787 x * y * z * u * a * a0 != w | x * y * z * u * a * c0 != w | d0 = b0. [para(1(a,1),442(b,1,2,2)),rewrite([1(5)])]. given #488 (A,wt=33): 181 x * y * z * y * z * y * z != u | w * z * y * z * y * z * y != u | x = w. [para(14(a,1),3(a,1))]. given #489 (T,wt=29): 788 x * y * z * u * a * a0 != w | a * a0 != w | x * y * z * u * b = b. [para(1(a,1),443(a,1,2,2)),rewrite([1(15)])]. given #490 (T,wt=29): 789 x * y * z * u * a * a0 != w | c * a0 != w | x * y * z * u * b = d. [para(1(a,1),444(a,1,2,2)),rewrite([1(15)])]. given #491 (T,wt=29): 790 x * y * z * u * c * a0 != w | a * a0 != w | x * y * z * u * d = b. [para(1(a,1),445(a,1,2,2)),rewrite([1(15)])]. given #492 (T,wt=29): 791 x * y * z * u * c * a0 != w | c * a0 != w | x * y * z * u * d = d. [para(1(a,1),446(a,1,2,2)),rewrite([1(15)])]. given #493 (A,wt=33): 182 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 #494 (T,wt=29): 792 x * y * z * u * a * c0 != w | a * c0 != w | x * y * z * u * b = b. [para(1(a,1),464(a,1,2,2)),rewrite([1(15)])]. given #495 (T,wt=29): 793 x * y * z * a * a0 * u != w | a * a0 * u != w | x * y * z * b = b. [para(1(a,1),465(a,1,2)),rewrite([1(16)])]. given #496 (T,wt=29): 795 a0 * a * a0 * a * a0 * a != x | a * a0 * a * a0 != x | a * a0 * b = b. [para(4(a,1),465(a,1))]. given #497 (T,wt=29): 798 x * y * z * a * a0 * u != w | c * a0 * u != w | x * y * z * b = d. [para(1(a,1),470(a,1,2)),rewrite([1(16)])]. given #498 (A,wt=33): 183 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 #499 (T,wt=29): 800 a0 * a * a0 * a * a0 * a != x | c * a0 * a * a0 != x | a * a0 * b = d. [para(4(a,1),470(a,1))]. NOTE: Back_subsumption disabled, ratio of kept to back_subsumed is 50 (0.00 of 9.34 sec). given #500 (T,wt=29): 804 x * y * z * c * a0 * u != w | a * a0 * u != w | x * y * z * d = b. [para(1(a,1),476(a,1,2)),rewrite([1(16)])]. given #501 (T,wt=29): 806 a0 * c * a0 * c * a0 * c != x | a * a0 * c * a0 != x | c * a0 * d = b. [para(4(a,1),476(a,1))]. given #502 (T,wt=29): 809 x * y * z * c * a0 * u != w | c * a0 * u != w | x * y * z * d = d. [para(1(a,1),482(a,1,2)),rewrite([1(16)])]. given #503 (A,wt=33): 184 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 #504 (T,wt=29): 811 a0 * c * a0 * c * a0 * c != x | c * a0 * c * a0 != x | c * a0 * d = d. [para(4(a,1),482(a,1))]. given #505 (T,wt=29): 814 x * y * z * a * c0 * u != w | a * c0 * u != w | x * y * z * b = b. [para(1(a,1),487(a,1,2)),rewrite([1(16)])]. given #506 (T,wt=29): 816 c0 * a * c0 * a * c0 * a != x | a * c0 * a * c0 != x | a * c0 * b = b. [para(4(a,1),487(a,1))]. given #507 (T,wt=29): 819 x * y * z * a * a0 != u | w * a * a0 != u | x * y * z * b = w * b. [para(1(a,1),492(a,1,2)),rewrite([1(15)])]. given #508 (A,wt=33): 185 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 #509 (T,wt=29): 820 x * y * a * a0 != z | u * w * a * a0 != z | x * y * b = u * w * b. [para(1(a,1),492(b,1)),rewrite([1(18)])]. given #510 (T,wt=29): 822 x * y * z * a * a0 != u | w * c * a0 != u | x * y * z * b = w * d. [para(1(a,1),493(a,1,2)),rewrite([1(15)])]. given #511 (T,wt=29): 823 x * y * a * a0 != z | u * w * c * a0 != z | u * w * d = x * y * b. [para(1(a,1),493(b,1)),rewrite([1(18)]),flip(c)]. given #512 (T,wt=29): 824 x * a * a0 != y | z * u * w * c * a0 != y | z * u * w * d = x * b. [para(1(a,1),494(b,1,2)),rewrite([1(15)])]. given #513 (A,wt=33): 187 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 #514 (T,wt=29): 825 x * y * z * a * a0 != u | a * a0 * b0 != u | a * a0 = x * y * z * b. [para(1(a,1),498(a,1,2)),rewrite([1(19)])]. given #515 (T,wt=29): 826 x * y * z * a * a0 != u | c * a0 * b0 != u | c * a0 = x * y * z * b. [para(1(a,1),499(a,1,2)),rewrite([1(19)])]. given #516 (T,wt=29): 827 x * y * z * a * a0 != u | a * c0 * b0 != u | a * c0 = x * y * z * b. [para(1(a,1),500(a,1,2)),rewrite([1(19)])]. given #517 (T,wt=29): 828 x * y * z * c * a0 != u | w * c * a0 != u | x * y * z * d = w * d. [para(1(a,1),501(a,1,2)),rewrite([1(15)])]. given #518 (A,wt=33): 188 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 #519 (T,wt=29): 829 x * y * c * a0 != z | u * w * c * a0 != z | x * y * d = u * w * d. [para(1(a,1),501(b,1)),rewrite([1(18)])]. given #520 (T,wt=29): 830 x * y * z * c * a0 != u | a * a0 * b0 != u | a * a0 = x * y * z * d. [para(1(a,1),503(a,1,2)),rewrite([1(19)])]. given #521 (T,wt=29): 831 x * y * z * c * a0 != u | c * a0 * b0 != u | c * a0 = x * y * z * d. [para(1(a,1),504(a,1,2)),rewrite([1(19)])]. given #522 (T,wt=29): 832 x * y * z * c * a0 != u | a * c0 * b0 != u | a * c0 = x * y * z * d. [para(1(a,1),505(a,1,2)),rewrite([1(19)])]. given #523 (A,wt=33): 190 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 #524 (T,wt=29): 833 x * y * z * a * c0 != u | w * a * c0 != u | x * y * z * b = w * b. [para(1(a,1),506(a,1,2)),rewrite([1(15)])]. given #525 (T,wt=29): 834 x * y * a * c0 != z | u * w * a * c0 != z | x * y * b = u * w * b. [para(1(a,1),506(b,1)),rewrite([1(18)])]. given #526 (T,wt=29): 835 x * y * z * a * c0 != u | a * a0 * d0 != u | a * a0 = x * y * z * b. [para(1(a,1),513(a,1,2)),rewrite([1(19)])]. given #527 (T,wt=29): 836 x * y * z * a * c0 != u | c * a0 * d0 != u | c * a0 = x * y * z * b. [para(1(a,1),514(a,1,2)),rewrite([1(19)])]. given #528 (A,wt=33): 211 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 #529 (T,wt=29): 837 x * y * z * a * c0 != u | a * c0 * d0 != u | a * c0 = x * y * z * b. [para(1(a,1),515(a,1,2)),rewrite([1(19)])]. given #530 (T,wt=29): 838 x * y * z * u * w != v5 | a * a0 * w != v5 | a * a0 = x * y * z * u. [para(1(a,1),650(a,1,2,2))]. given #531 (T,wt=29): 840 x * y * a * a0 * z != u | a * a0 * b0 * z != u | a * a0 = x * y * b. [para(18(a,1),650(a,1,2,2))]. given #532 (T,wt=29): 841 x * y * c * a0 * z != u | a * a0 * b0 * z != u | a * a0 = x * y * d. [para(22(a,1),650(a,1,2,2))]. given #533 (A,wt=33): 213 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 #534 (T,wt=29): 842 x * y * a * c0 * z != u | a * a0 * d0 * z != u | a * a0 = x * y * b. [para(26(a,1),650(a,1,2,2))]. given #535 (T,wt=29): 843 x * y * z * u * w != v5 | c * a0 * w != v5 | c * a0 = x * y * z * u. [para(1(a,1),653(a,1,2,2))]. given #536 (T,wt=29): 845 x * y * a * a0 * z != u | c * a0 * b0 * z != u | c * a0 = x * y * b. [para(18(a,1),653(a,1,2,2))]. given #537 (T,wt=29): 846 x * y * c * a0 * z != u | c * a0 * b0 * z != u | c * a0 = x * y * d. [para(22(a,1),653(a,1,2,2))]. given #538 (A,wt=33): 214 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 #539 (T,wt=29): 847 x * y * a * c0 * z != u | c * a0 * d0 * z != u | c * a0 = x * y * b. [para(26(a,1),653(a,1,2,2))]. given #540 (T,wt=29): 849 x * y * z * u * w != v5 | a * c0 * w != v5 | a * c0 = x * y * z * u. [para(1(a,1),656(a,1,2,2))]. given #541 (T,wt=29): 851 x * y * a * a0 * z != u | a * c0 * b0 * z != u | a * c0 = x * y * b. [para(18(a,1),656(a,1,2,2))]. given #542 (T,wt=29): 852 x * y * c * a0 * z != u | a * c0 * b0 * z != u | a * c0 = x * y * d. [para(22(a,1),656(a,1,2,2))]. given #543 (A,wt=33): 216 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 #544 (T,wt=29): 853 x * y * a * c0 * z != u | a * c0 * d0 * z != u | a * c0 = x * y * b. [para(26(a,1),656(a,1,2,2))]. given #545 (T,wt=29): 854 x * y * a * a0 * z != u | w * a * a0 * z != u | x * y * b = w * b. [para(1(a,1),699(a,1)),rewrite([1(16)])]. given #546 (T,wt=29): 857 x * y * a * a0 * z != u | w * c * a0 * z != u | x * y * b = w * d. [para(1(a,1),701(a,1)),rewrite([1(18)]),flip(c)]. given #547 (T,wt=29): 858 x * a * a0 * y != z | u * w * c * a0 * y != z | u * w * d = x * b. [para(1(a,1),701(b,1)),rewrite([1(16)])]. given #548 (A,wt=33): 217 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 #549 (T,wt=29): 865 x * y * c * a0 * z != u | w * c * a0 * z != u | x * y * d = w * d. [para(1(a,1),709(a,1)),rewrite([1(16)])]. given #550 (T,wt=29): 870 x * y * a * c0 * z != u | w * a * c0 * z != u | x * y * b = w * b. [para(1(a,1),718(a,1)),rewrite([1(16)])]. given #551 (T,wt=29): 1280 x * a * a0 != y | x * b * x * b * x * b != y | x * b * x * b = b0. [para(4(a,1),101(b,1))]. given #552 (T,wt=29): 1590 x * c * a0 != y | x * d * x * d * x * d != y | x * d * x * d = b0. [para(4(a,1),134(b,1))]. given #553 (A,wt=33): 219 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 #554 (T,wt=29): 1591 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 #555 (T,wt=29): 1592 x * a * c0 != y | x * b * x * b * x * b != y | x * b * x * b = d0. [para(4(a,1),139(b,1))]. given #556 (T,wt=29): 1616 a0 * a * a0 * a * a0 * a != x | y * a * a0 * a * a0 * b != x | b0 = y. [para(4(a,1),208(a,1))]. given #557 (T,wt=29): 1618 c0 * a * c0 * a * c0 * a != x | y * a * c0 * a * c0 * b != x | d0 = y. [para(4(a,1),210(a,1))]. given #558 (A,wt=33): 221 a * a0 * x * a0 * x * a0 * x != y | c * x * a0 * x * a0 * x * a0 != y | d = b. [para(4(a,1),152(b,1,2))]. given #559 (T,wt=29): 1624 a0 * a * a0 * a * a0 * a != x | y * a0 * a * a0 * b != x | b0 * a = y. [para(4(a,1),232(a,1))]. given #560 (T,wt=29): 1625 c * a0 * c * a0 * c * a0 != x | b0 * c * a0 * y != x | c * a0 * d = y. [para(6(a,1),240(a,1,2,2,2,2)),rewrite([22(9),22(11),22(17),22(24)])]. given #561 (T,wt=29): 1640 c0 * a * c0 * a * c0 * a != x | y * c0 * a * c0 * b != x | d0 * a = y. [para(4(a,1),258(a,1))]. given #562 (T,wt=29): 1642 c * a0 * c * a0 * c * a0 != x | y * c * a0 * d != x | b0 * c * a0 = y. [para(6(a,1),276(a,1,2,2,2,2)),rewrite([22(9),22(11),22(17),6(23)])]. given #563 (A,wt=33): 223 a * a0 * c * a0 * c * a0 * x != y | a0 * c * a0 * c * a0 * c * x != y | d = b. [para(12(a,1),152(b,1))]. given #564 (T,wt=29): 1643 a0 * a * a0 * a * a0 * a != x | y * a * a0 * b != x | b0 * a * a0 = y. [para(4(a,1),285(a,1))]. given #565 (T,wt=29): 1644 c0 * a * c0 * a * c0 * a != x | y * a * c0 * b != x | d0 * a * c0 = y. [para(4(a,1),287(a,1))]. given #566 (T,wt=29): 1646 c * a0 * c * a0 * c * a0 != x | a * a0 * c * a0 * d != x | b0 * d = b. [para(6(a,1),309(a,1,2,2,2,2)),rewrite([22(9),22(11),22(19)])]. given #567 (T,wt=29): 1652 c * a0 * c * a0 * c * a0 != x | c * a0 * c * a0 * d != x | b0 * d = d. [para(6(a,1),318(a,1,2,2,2,2)),rewrite([22(9),22(11),22(19)])]. given #568 (A,wt=33): 227 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 #569 (T,wt=29): 1656 b * x * a * a0 != y | b * x * b * x * b * x != y | x * b * x = b0. [para(4(a,1),333(b,1))]. given #570 (T,wt=29): 1658 d * x * c * a0 != y | d * x * d * x * d * x != y | x * d * x = b0. [para(4(a,1),347(b,1))]. given #571 (T,wt=29): 1662 b * x * a * c0 != y | b * x * b * x * b * x != y | x * b * x = d0. [para(4(a,1),355(b,1))]. given #572 (T,wt=29): 1670 c * a0 * c * a0 * c * a0 != x | b0 * c * y != x | a0 * c * a0 * d = y. [para(4(a,1),419(a,1))]. given #573 (A,wt=33): 231 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 #574 (T,wt=29): 1697 c * a0 * c * a0 * c * a0 != x | y * a0 * c * a0 * d != x | b0 * c = y. [para(4(a,1),423(a,1))]. given #575 (T,wt=29): 1699 a0 * a * a0 * a * a0 * a != x | a * a0 * a * a0 * b != x | b0 * b = b. [para(4(a,1),469(a,1))]. given #576 (T,wt=29): 1706 c0 * a * c0 * a * c0 * a != x | a * c0 * a * c0 * b != x | d0 * b = b. [para(4(a,1),491(a,1))]. given #577 (T,wt=29): 1708 b0 * d0 * b0 * d0 * b0 * d0 != x | c0 * b0 * d0 * b0 * d0 * b0 != x | b0 = a0. [para(4(a,1),545(a,1))]. given #578 (A,wt=33): 233 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 #579 (T,wt=29): 1711 x * y * x * y * x * y != z | y * x * y * x * y * u != z | x = u. [para(4(a,1),558(a,1))]. given #580 (T,wt=29): 1712 x * y * x * y * x * z != u | y * x * y * x * y * x != u | z = y. [para(4(a,1),558(b,1))]. given #581 (T,wt=29): 1718 a * a0 * a * a0 * a * a0 != x | b0 * a * a0 * a * a0 * y != x | b = y. [para(21(a,1),558(a,1))]. given #582 (T,wt=29): 1720 a * c0 * a * c0 * a * c0 != x | d0 * a * c0 * a * c0 * y != x | b = y. [para(29(a,1),558(a,1))]. given #583 (A,wt=33): 234 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 #584 (T,wt=29): 1724 a0 * c * a0 * c * a0 * c != x | b0 * c * a0 * c * a0 * y != x | d = y. [para(45(a,1),558(a,1))]. given #585 (T,wt=29): 1728 b0 * c0 * a0 * c0 * a0 * c0 != x | d0 * a0 * c0 * a0 * c0 * y != x | a0 = y. [para(178(a,1),558(a,1))]. given #586 (T,wt=29): 1730 c0 * b0 * d0 * b0 * d0 * b0 != x | a0 * d0 * b0 * d0 * b0 * y != x | d0 = y. [para(359(a,1),558(a,1))]. given #587 (T,wt=29): 1764 a * a0 * a * a0 * a * a0 != x | b0 * a * a0 * b * y != x | b0 * b = y. [para(5(a,1),560(a,1,2,2,2,2)),rewrite([18(9),18(11),18(19)])]. given #588 (A,wt=33): 235 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 #589 (T,wt=29): 1765 c * a0 * c * a0 * c * a0 != x | b0 * c * a0 * d * y != x | b0 * d = y. [para(6(a,1),560(a,1,2,2,2,2)),rewrite([22(9),22(11),22(19)])]. given #590 (T,wt=29): 1766 a * c0 * a * c0 * a * c0 != x | d0 * a * c0 * b * y != x | d0 * b = y. [para(7(a,1),560(a,1,2,2,2,2)),rewrite([26(9),26(11),26(19)])]. given #591 (T,wt=29): 1771 a * a0 * a * a0 * a * a0 != x | a0 * a * a0 * b * y != x | b0 * a = y. [para(4(a,1),561(a,1))]. given #592 (T,wt=29): 1783 c * a0 * c * a0 * c * a0 != x | a0 * c * a0 * d * y != x | b0 * c = y. [para(4(a,1),562(a,1))]. given #593 (A,wt=33): 239 x * y * z * y * z * y * z != u | x * z * y * w != u | z * y * z * y = w. [para(4(a,1),30(a,1,2))]. given #594 (T,wt=29): 1786 a0 * c * a0 * c * a0 * c != x | b0 * c * a0 * d * y != x | b0 * d = y. [para(45(a,1),562(a,1))]. given #595 (T,wt=29): 1793 a * c0 * a * c0 * a * c0 != x | c0 * a * c0 * b * y != x | d0 * a = y. [para(4(a,1),563(a,1))]. given #596 (T,wt=29): 1802 c * a0 * c * a0 * c * a0 != x | b0 * c * a0 * c * y != x | a0 * d = y. [para(4(a,1),572(a,1))]. given #597 (T,wt=29): 1811 x * y * x * y * x * y != z | u * x != z | y * x * y * x * y = u. [para(4(a,1),621(a,1))]. given #598 (A,wt=33): 244 x * y * x * y * x * y * z != u | y * x * y * w != u | x * y * x * z = w. [para(12(a,1),30(a,1))]. given #599 (T,wt=29): 1820 a * a0 * a * a0 * a * a0 != x | y * b != x | b0 * a * a0 * a * a0 = y. [para(21(a,1),621(a,1))]. given #600 (T,wt=29): 1822 a * c0 * a * c0 * a * c0 != x | y * b != x | d0 * a * c0 * a * c0 = y. [para(29(a,1),621(a,1))]. given #601 (T,wt=29): 1826 a0 * c * a0 * c * a0 * c != x | y * d != x | b0 * c * a0 * c * a0 = y. [para(45(a,1),621(a,1))]. given #602 (T,wt=29): 1830 b0 * c0 * a0 * c0 * a0 * c0 != x | y * a0 != x | d0 * a0 * c0 * a0 * c0 = y. [para(178(a,1),621(a,1))]. given #603 (A,wt=33): 245 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 #604 (T,wt=29): 1832 c0 * b0 * d0 * b0 * d0 * b0 != x | y * d0 != x | a0 * d0 * b0 * d0 * b0 = y. [para(359(a,1),621(a,1))]. given #605 (T,wt=29): 1879 a * a0 * a * a0 * a * a0 != x | y * b0 * b != x | b0 * a * a0 * b = y. [para(5(a,1),624(a,1,2,2,2,2)),rewrite([18(9),18(11),18(23)])]. given #606 (T,wt=29): 1880 c * a0 * c * a0 * c * a0 != x | y * b0 * d != x | b0 * c * a0 * d = y. [para(6(a,1),624(a,1,2,2,2,2)),rewrite([22(9),22(11),22(23)])]. given #607 (T,wt=29): 1881 a * c0 * a * c0 * a * c0 != x | y * d0 * b != x | d0 * a * c0 * b = y. [para(7(a,1),624(a,1,2,2,2,2)),rewrite([26(9),26(11),26(23)])]. given #608 (A,wt=33): 247 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 #609 (T,wt=29): 1882 x * b0 * x * b0 * x * b0 != y | a * a0 * x != y | b0 * x * b0 * x = b. [para(18(a,1),624(b,1))]. given #610 (T,wt=29): 1883 x * b0 * x * b0 * x * b0 != y | c * a0 * x != y | b0 * x * b0 * x = d. [para(22(a,1),624(b,1))]. given #611 (T,wt=29): 1884 x * d0 * x * d0 * x * d0 != y | a * c0 * x != y | d0 * x * d0 * x = b. [para(26(a,1),624(b,1))]. given #612 (T,wt=29): 1886 a * a0 * a * a0 * a * a0 != x | y * b0 * a != x | a0 * a * a0 * b = y. [para(4(a,1),625(a,1))]. given #613 (A,wt=33): 249 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 #614 (T,wt=29): 1899 c0 * b0 * d0 * b0 * d0 * b0 != x | a * a0 * d0 != x | a0 * d0 * b0 * d0 = b. [para(359(a,1),626(a,1))]. given #615 (T,wt=29): 1907 c * a0 * c * a0 * c * a0 != x | y * b0 * c != x | a0 * c * a0 * d = y. [para(4(a,1),627(a,1))]. given #616 (T,wt=29): 1909 a0 * c * a0 * c * a0 * c != x | y * b0 * d != x | b0 * c * a0 * d = y. [para(45(a,1),627(a,1))]. given #617 (T,wt=29): 1919 c0 * b0 * d0 * b0 * d0 * b0 != x | c * a0 * d0 != x | a0 * d0 * b0 * d0 = d. [para(359(a,1),628(a,1))]. given #618 (A,wt=33): 252 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 #619 (T,wt=29): 1927 a * c0 * a * c0 * a * c0 != x | y * d0 * a != x | c0 * a * c0 * b = y. [para(4(a,1),629(a,1))]. given #620 (T,wt=29): 1945 a0 * a * a0 * a * a0 * a != x | y * a0 * b != x | b0 * a * a0 * a = y. [para(4(a,1),633(a,1))]. given #621 (T,wt=29): 1946 c0 * a * c0 * a * c0 * a != x | y * c0 * b != x | d0 * a * c0 * a = y. [para(4(a,1),635(a,1))]. given #622 (T,wt=29): 1947 c * a0 * c * a0 * c * a0 != x | y * a0 * d != x | b0 * c * a0 * c = y. [para(4(a,1),639(a,1))]. given #623 (A,wt=33): 254 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 #624 (T,wt=29): 1963 b * x * b * x * a * a0 != y | x * b * x * b * x * b != y | b0 = x. [para(4(a,1),723(b,1))]. given #625 (T,wt=29): 1975 x * b * x * a * a0 != y | x * b * x * b * x * b != y | x * b = b0. [para(4(a,1),725(b,1))]. given #626 (T,wt=29): 1976 b0 * a * a0 * a * a0 != x | a * a0 * a * a0 * a * a0 != x | b0 * b = b0. [para(5(a,1),725(b,1,2,2,2,2)),rewrite([18(8),18(19),18(21)])]. given #627 (T,wt=29): 1977 d0 * a * c0 * a * a0 != x | a * c0 * a * c0 * a * c0 != x | d0 * b = b0. [para(7(a,1),725(b,1,2,2,2,2)),rewrite([26(8),26(19),26(21)])]. given #628 (A,wt=33): 257 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 #629 (T,wt=29): 1979 a0 * a * a0 * a * a0 != x | a * a0 * a * a0 * a * a0 != x | b0 * a = b0. [para(4(a,1),726(b,1))]. given #630 (T,wt=29): 1986 c0 * a * c0 * a * a0 != x | a * c0 * a * c0 * a * c0 != x | d0 * a = b0. [para(4(a,1),727(b,1))]. given #631 (T,wt=29): 1996 d * x * d * x * c * a0 != y | x * d * x * d * x * d != y | b0 = x. [para(4(a,1),739(b,1))]. given #632 (T,wt=29): 2006 x * d * x * c * a0 != y | x * d * x * d * x * d != y | x * d = b0. [para(4(a,1),741(b,1))]. given #633 (A,wt=33): 259 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 #634 (T,wt=29): 2007 b0 * c * a0 * c * a0 != x | c * a0 * c * a0 * c * a0 != x | b0 * d = b0. [para(6(a,1),741(b,1,2,2,2,2)),rewrite([22(8),22(19),22(21)])]. given #635 (T,wt=29): 2009 a0 * c * a0 * c * a0 != x | c * a0 * c * a0 * c * a0 != x | b0 * c = b0. [para(4(a,1),742(b,1))]. given #636 (T,wt=29): 2011 b0 * c * a0 * c * a0 != x | a0 * c * a0 * c * a0 * c != x | b0 * d = b0. [para(45(a,1),742(b,1))]. given #637 (T,wt=29): 2018 b * x * b * x * a * c0 != y | x * b * x * b * x * b != y | d0 = x. [para(4(a,1),751(b,1))]. given #638 (A,wt=33): 260 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 #639 (T,wt=29): 2030 x * b * x * a * c0 != y | x * b * x * b * x * b != y | x * b = d0. [para(4(a,1),753(b,1))]. given #640 (T,wt=29): 2031 b0 * a * a0 * a * c0 != x | a * a0 * a * a0 * a * a0 != x | b0 * b = d0. [para(5(a,1),753(b,1,2,2,2,2)),rewrite([18(8),18(19),18(21)])]. given #641 (T,wt=29): 2032 d0 * a * c0 * a * c0 != x | a * c0 * a * c0 * a * c0 != x | d0 * b = d0. [para(7(a,1),753(b,1,2,2,2,2)),rewrite([26(8),26(19),26(21)])]. given #642 (T,wt=29): 2034 a0 * a * a0 * a * c0 != x | a * a0 * a * a0 * a * a0 != x | b0 * a = d0. [para(4(a,1),754(b,1))]. given #643 (A,wt=33): 262 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 #644 (T,wt=29): 2042 c0 * a * c0 * a * c0 != x | a * c0 * a * c0 * a * c0 != x | d0 * a = d0. [para(4(a,1),755(b,1))]. given #645 (T,wt=29): 2051 a0 * a * a0 * a * a0 * a != x | y * b0 != x | a * a0 * a * a0 * b = y. [para(4(a,1),769(a,1))]. given #646 (T,wt=29): 2054 x * y * a * a0 != z | u * a * a0 * b0 != z | u * a * a0 = x * y * b. [para(18(a,1),771(b,1,2)),rewrite([5(19)]),flip(c)]. given #647 (T,wt=29): 2055 x * y * a * a0 != z | a * a0 * u * b0 != z | a * a0 * u = x * y * b. [para(18(a,1),771(b,1)),rewrite([18(20)]),flip(c)]. given #648 (A,wt=33): 264 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 #649 (T,wt=29): 2056 x * y * a * a0 != z | u * c * a0 * b0 != z | u * c * a0 = x * y * b. [para(22(a,1),771(b,1,2)),rewrite([6(19)]),flip(c)]. given #650 (T,wt=29): 2057 x * y * a * a0 != z | c * a0 * u * b0 != z | c * a0 * u = x * y * b. [para(22(a,1),771(b,1)),rewrite([22(20)]),flip(c)]. given #651 (T,wt=29): 2058 x * y * a * a0 != z | u * a * c0 * b0 != z | u * a * c0 = x * y * b. [para(26(a,1),771(b,1,2)),rewrite([7(19)]),flip(c)]. given #652 (T,wt=29): 2059 x * y * a * a0 != z | a * c0 * u * b0 != z | a * c0 * u = x * y * b. [para(26(a,1),771(b,1)),rewrite([26(20)]),flip(c)]. given #653 (A,wt=33): 266 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 #654 (T,wt=29): 2062 b0 * x * b0 * x * b0 * x != y | a * a0 != y | x * b0 * x * b0 * x = b. [para(4(a,1),773(a,1))]. given #655 (T,wt=29): 2065 a0 * c * a0 * c * a0 * c != x | y * b0 != x | c * a0 * c * a0 * d = y. [para(4(a,1),776(a,1))]. given #656 (T,wt=29): 2068 x * y * c * a0 != z | u * a * a0 * b0 != z | u * a * a0 = x * y * d. [para(18(a,1),778(b,1,2)),rewrite([5(19)]),flip(c)]. given #657 (T,wt=29): 2069 x * y * c * a0 != z | a * a0 * u * b0 != z | a * a0 * u = x * y * d. [para(18(a,1),778(b,1)),rewrite([18(20)]),flip(c)]. given #658 (A,wt=33): 267 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 #659 (T,wt=29): 2070 x * y * c * a0 != z | u * c * a0 * b0 != z | u * c * a0 = x * y * d. [para(22(a,1),778(b,1,2)),rewrite([6(19)]),flip(c)]. given #660 (T,wt=29): 2071 x * y * c * a0 != z | c * a0 * u * b0 != z | c * a0 * u = x * y * d. [para(22(a,1),778(b,1)),rewrite([22(20)]),flip(c)]. given #661 (T,wt=29): 2072 x * y * c * a0 != z | u * a * c0 * b0 != z | u * a * c0 = x * y * d. [para(26(a,1),778(b,1,2)),rewrite([7(19)]),flip(c)]. given #662 (T,wt=29): 2073 x * y * c * a0 != z | a * c0 * u * b0 != z | a * c0 * u = x * y * d. [para(26(a,1),778(b,1)),rewrite([26(20)]),flip(c)]. given #663 (A,wt=33): 269 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 #664 (T,wt=29): 2076 b0 * x * b0 * x * b0 * x != y | c * a0 != y | x * b0 * x * b0 * x = d. [para(4(a,1),780(a,1))]. given #665 (T,wt=29): 2110 c0 * a * c0 * a * c0 * a != x | y * d0 != x | a * c0 * a * c0 * b = y. [para(4(a,1),781(a,1))]. given #666 (T,wt=29): 2115 x * y * a * c0 != z | u * a * a0 * d0 != z | u * a * a0 = x * y * b. [para(18(a,1),783(b,1,2)),rewrite([5(19)]),flip(c)]. given #667 (T,wt=29): 2116 x * y * a * c0 != z | a * a0 * u * d0 != z | a * a0 * u = x * y * b. [para(18(a,1),783(b,1)),rewrite([18(20)]),flip(c)]. given #668 (A,wt=33): 271 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 #669 (T,wt=29): 2117 x * y * a * c0 != z | u * c * a0 * d0 != z | u * c * a0 = x * y * b. [para(22(a,1),783(b,1,2)),rewrite([6(19)]),flip(c)]. given #670 (T,wt=29): 2118 x * y * a * c0 != z | c * a0 * u * d0 != z | c * a0 * u = x * y * b. [para(22(a,1),783(b,1)),rewrite([22(20)]),flip(c)]. given #671 (T,wt=29): 2119 x * y * a * c0 != z | u * a * c0 * d0 != z | u * a * c0 = x * y * b. [para(26(a,1),783(b,1,2)),rewrite([7(19)]),flip(c)]. given #672 (T,wt=29): 2120 x * y * a * c0 != z | a * c0 * u * d0 != z | a * c0 * u = x * y * b. [para(26(a,1),783(b,1)),rewrite([26(20)]),flip(c)]. given #673 (A,wt=33): 275 x * y * z * y * z * y * z != u | w * z * y * z * y != u | x * z * y = w. [para(4(a,1),56(a,1,2))]. given #674 (T,wt=29): 2123 d0 * x * d0 * x * d0 * x != y | a * c0 != y | x * d0 * x * d0 * x = b. [para(4(a,1),785(a,1))]. given #675 (T,wt=29): 2124 c0 * b0 * d0 * b0 * d0 * b0 != x | a * c0 != x | a0 * d0 * b0 * d0 * b0 = b. [para(359(a,1),785(a,1))]. given #676 (T,wt=29): 2126 a * c0 * a * c0 * a * a0 != x | c0 * a * c0 * a * c0 * a != x | d0 = b0. [para(4(a,1),787(b,1))]. given #677 (T,wt=29): 2128 a0 * a * a0 * a * a0 * a != x | a * a0 != x | a * a0 * a * a0 * b = b. [para(4(a,1),788(a,1))]. given #678 (A,wt=33): 283 x * y * x * y * x * y * z != u | w * x * y * x * z != u | y * x * y = w. [para(12(a,1),56(a,1))]. given #679 (T,wt=29): 2130 a0 * a * a0 * a * a0 * a != x | c * a0 != x | a * a0 * a * a0 * b = d. [para(4(a,1),789(a,1))]. given #680 (T,wt=29): 2132 a0 * c * a0 * c * a0 * c != x | a * a0 != x | c * a0 * c * a0 * d = b. [para(4(a,1),790(a,1))]. given #681 (T,wt=29): 2134 a0 * c * a0 * c * a0 * c != x | c * a0 != x | c * a0 * c * a0 * d = d. [para(4(a,1),791(a,1))]. given #682 (T,wt=29): 2137 c0 * a * c0 * a * c0 * a != x | a * c0 != x | a * c0 * a * c0 * b = b. [para(4(a,1),792(a,1))]. given #683 (A,wt=33): 284 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 #684 (T,wt=29): 2140 a * a0 * a * a0 * a * a0 != x | a * a0 * a != x | a0 * a * a0 * b = b. [para(4(a,1),793(a,1))]. given #685 (T,wt=29): 2142 a * a0 * a * a0 * a * a0 != x | a * a0 * b != x | b0 * a * a0 * b = b. [para(21(a,1),793(a,1))]. given #686 (T,wt=29): 2150 a * a0 * a * a0 * a * a0 != x | c * a0 * a != x | a0 * a * a0 * b = d. [para(4(a,1),798(a,1))]. given #687 (T,wt=29): 2152 a * a0 * a * a0 * a * a0 != x | c * a0 * b != x | b0 * a * a0 * b = d. [para(21(a,1),798(a,1))]. given #688 (A,wt=33): 286 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 #689 (T,wt=29): 2161 c * a0 * c * a0 * c * a0 != x | a * a0 * c != x | a0 * c * a0 * d = b. [para(4(a,1),804(a,1))]. given #690 (T,wt=29): 2163 a0 * c * a0 * c * a0 * c != x | a * a0 * d != x | b0 * c * a0 * d = b. [para(45(a,1),804(a,1))]. given #691 (T,wt=29): 2171 c * a0 * c * a0 * c * a0 != x | c * a0 * c != x | a0 * c * a0 * d = d. [para(4(a,1),809(a,1))]. given #692 (T,wt=29): 2173 a0 * c * a0 * c * a0 * c != x | c * a0 * d != x | b0 * c * a0 * d = d. [para(45(a,1),809(a,1))]. given #693 (A,wt=33): 288 x * y * x * y * x * y != z | u * w * y * x * y * x != z | y * x = u * w. [para(4(a,1),57(a,1))]. given #694 (T,wt=29): 2182 a * c0 * a * c0 * a * c0 != x | a * c0 * a != x | c0 * a * c0 * b = b. [para(4(a,1),814(a,1))]. given #695 (T,wt=29): 2184 a * c0 * a * c0 * a * c0 != x | a * c0 * b != x | d0 * a * c0 * b = b. [para(29(a,1),814(a,1))]. given #696 (T,wt=29): 2193 a * a0 * a * a0 != x | y * z * c * a0 != x | a * a0 * b = y * z * d. [para(18(a,1),823(a,1)),rewrite([18(22)]),flip(c)]. given #697 (T,wt=29): 2194 c * a0 * a * a0 != x | y * z * c * a0 != x | c * a0 * b = y * z * d. [para(22(a,1),823(a,1)),rewrite([22(22)]),flip(c)]. given #698 (A,wt=33): 289 x * y * z * u * z * u != w | u * z * u * z * u * z != w | x * y = z * u. [para(4(a,1),57(b,1))]. given #699 (T,wt=29): 2195 a * c0 * a * a0 != x | y * z * c * a0 != x | a * c0 * b = y * z * d. [para(26(a,1),823(a,1)),rewrite([26(22)]),flip(c)]. given #700 (T,wt=29): 2255 c * a0 * c * a0 * c * a0 != x | b0 * c * a0 * c * a0 * y != x | d = y. [para(6(a,1),1711(a,1,2,2,2,2)),rewrite([22(9),22(11),22(19),22(21)])]. given #701 (T,wt=29): 2257 a0 * c * a0 * c * a0 * c != x | c * a0 * c * a0 * d * y != x | b0 = y. [para(22(a,1),1711(a,1,2,2,2)),rewrite([22(10),45(11),22(20),22(22)])]. given #702 (T,wt=29): 2299 c * a0 * c * a0 * c * a0 != x | y * d != x | b0 * c * a0 * c * a0 = y. [para(6(a,1),1811(a,1,2,2,2,2)),rewrite([22(9),22(11),6(21),22(23)])]. given #703 (A,wt=33): 293 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 #704 (T,wt=29): 2301 a0 * a * a0 * a * a0 * a != x | y * b != x | b0 * a * a0 * a * a0 = y. [para(4(a,1),1820(a,1))]. given #705 (T,wt=29): 2303 c0 * a * c0 * a * c0 * a != x | y * b != x | d0 * a * c0 * a * c0 = y. [para(4(a,1),1822(a,1))]. given #706 (T,wt=29): 2309 c * a0 * c * a0 * c * a0 != x | a * a0 * d != x | b0 * c * a0 * d = b. [para(18(a,1),1880(b,1))]. given #707 (T,wt=29): 2310 c * a0 * c * a0 * c * a0 != x | c * a0 * d != x | b0 * c * a0 * d = d. [para(22(a,1),1880(b,1))]. given #708 (A,wt=33): 294 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 #709 (T,wt=29): 2350 a0 * a * a0 * a * a0 * a != x | a * a0 * b != x | b0 * a * a0 * b = b. [para(4(a,1),2142(a,1))]. given #710 (T,wt=29): 2357 c0 * a * c0 * a * c0 * a != x | a * c0 * b != x | d0 * a * c0 * b = b. [para(4(a,1),2184(a,1))]. given #711 (T,wt=31): 447 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 #712 (T,wt=31): 666 d0 * a0 * a0 * c0 * a0 * a0 * c0 * a0 = b0 * c0 * a0 * a0 * c0 * a0 * a0 * c0. [hyper(148,a,xx,b,80,a)]. given #713 (A,wt=33): 295 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 #714 (T,wt=31): 667 d0 * a0 * c0 * c0 * a0 * c0 * c0 * a0 = b0 * c0 * c0 * a0 * c0 * c0 * a0 * c0. [hyper(148,a,80,a,b,xx)]. given #715 (T,wt=31): 668 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 #716 (T,wt=31): 669 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 #717 (T,wt=31): 786 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 #718 (A,wt=33): 296 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 #719 (T,wt=31): 803 a0 * d0 * b0 * b0 * d0 * b0 * b0 * d0 = c0 * b0 * b0 * d0 * b0 * b0 * d0 * b0. [hyper(2,a,26,a(flip),b,89,a(flip)),flip(a)]. given #720 (T,wt=31): 821 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 #721 (T,wt=31): 873 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 #722 (T,wt=31): 881 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 #723 (A,wt=33): 297 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 #724 (T,wt=31): 884 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 #725 (T,wt=27): 2389 a0 * a0 * x * a0 * x * a0 * x = x * a0 * x * a0 * x * a0 * a0. [hyper(2,a,xx,b,884,a),flip(a)]. given #726 (T,wt=31): 885 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 #727 (T,wt=31): 887 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 #728 (A,wt=33): 298 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 #729 (T,wt=31): 888 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 #730 (T,wt=31): 891 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 #731 (T,wt=31): 892 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 #732 (T,wt=27): 2407 c0 * c0 * x * c0 * x * c0 * x = x * c0 * x * c0 * x * c0 * c0. [hyper(2,a,xx,b,892,a),flip(a)]. given #733 (A,wt=33): 299 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 #734 (T,wt=31): 903 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 #735 (T,wt=31): 1005 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 #736 (T,wt=31): 1017 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 #737 (T,wt=31): 1018 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 #738 (A,wt=33): 300 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 #739 (T,wt=27): 2435 c0 * b * c0 * b * c0 * a * a0 = b * c0 * b * c0 * b * c0 * b0. [hyper(2,a,xx,b,1018,a),flip(a)]. given #740 (T,wt=31): 1029 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 #741 (T,wt=31): 1031 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 #742 (T,wt=31): 1057 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 #743 (A,wt=33): 301 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 #744 (T,wt=27): 2440 d0 * d * d0 * d * d0 * c * a0 = d * d0 * d * d0 * d * d0 * b0. [hyper(47,a,26,a(flip),b,1057,a)]. given #745 (T,wt=31): 1065 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 #746 (T,wt=31): 1074 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 #747 (T,wt=31): 1076 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 #748 (A,wt=33): 303 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 #749 (T,wt=31): 1102 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 #750 (T,wt=31): 1105 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 #751 (T,wt=31): 1117 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 #752 (T,wt=27): 2453 c0 * b * c0 * b * c0 * a * c0 = b * c0 * b * c0 * b * c0 * d0. [hyper(2,a,xx,b,1117,a),flip(a)]. given #753 (A,wt=33): 306 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 #754 (T,wt=31): 1128 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 #755 (T,wt=31): 1130 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 #756 (T,wt=31): 1159 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 #757 (T,wt=31): 1160 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 #758 (A,wt=33): 308 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 #759 (T,wt=31): 1161 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 #760 (T,wt=31): 1162 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 #761 (T,wt=31): 1179 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 #762 (T,wt=31): 1180 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 #763 (A,wt=33): 311 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 #764 (T,wt=31): 1181 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 #765 (T,wt=31): 1194 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 #766 (T,wt=27): 2483 c * c * a0 * c * a0 * c * a0 = a0 * c * a0 * c * a0 * c * c. [hyper(106,a,12,a,b,1194,a),flip(a)]. given #767 (T,wt=31): 1199 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),1116(15),890(29)])]. given #768 (A,wt=33): 312 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 #769 (T,wt=31): 1201 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 #770 (T,wt=31): 1202 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 #771 (T,wt=31): 1203 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 #772 (T,wt=31): 1254 a * c0 * a * c0 * a * c0 * c0 * b = c0 * b * a * c0 * a * c0 * a * c0. [para(256(a,1),12(a,1,2)),flip(a)]. given #773 (A,wt=33): 314 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 #774 (T,wt=31): 1296 d * a0 * c * a0 * c * a0 * c * x = c * a0 * c * a0 * c * a0 * d * x. [para(421(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 #775 (T,wt=31): 1312 d0 * a0 * a0 * c0 * a0 * c0 * a0 * c0 = b0 * c0 * a0 * c0 * a0 * c0 * c0 * a0. [para(4(a,1),516(a,1,2,2))]. given #776 (T,wt=31): 1318 d0 * c0 * a0 * c0 * a0 * c0 * a0 * x = b0 * c0 * a0 * c0 * a0 * c0 * c0 * x. [para(12(a,1),516(a,1,2))]. given #777 (T,wt=31): 1328 d0 * c0 * c0 * a0 * c0 * a0 * c0 * a0 = b0 * c0 * a0 * c0 * a0 * c0 * c0 * c0. [para(111(a,1),516(a,1,2))]. given #778 (A,wt=33): 316 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 #779 (T,wt=31): 1333 a0 * d0 * d0 * b0 * d0 * b0 * d0 * b0 = c0 * b0 * d0 * b0 * d0 * b0 * b0 * d0. [para(4(a,1),534(a,1,2,2))]. given #780 (T,wt=31): 1339 a0 * b0 * d0 * b0 * d0 * b0 * d0 * x = c0 * b0 * d0 * b0 * d0 * b0 * b0 * x. [para(12(a,1),534(a,1,2))]. given #781 (T,wt=31): 1353 c0 * b0 * d0 * b0 * d0 * b0 * b0 * b0 = a0 * b0 * b0 * d0 * b0 * d0 * b0 * d0. [para(111(a,1),534(a,1,2)),flip(a)]. given #782 (T,wt=31): 1384 a0 * a0 * a * a0 * a * a0 * a * x = a * a0 * a * a0 * a * a0 * a0 * x. [para(883(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 #783 (A,wt=33): 317 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 #784 (T,wt=31): 1390 c * a0 * c * a0 * c * a0 * a0 * b0 = a0 * b0 * a0 * c * a0 * c * a0 * c. [para(886(a,1),12(a,1,2)),flip(a)]. given #785 (T,wt=31): 1423 c0 * c0 * a * c0 * a * c0 * a * x = a * c0 * a * c0 * a * c0 * c0 * x. [para(890(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 #786 (T,wt=31): 1424 d * b * d * b * d * a * a0 * x = b * d * b * d * b * c * a0 * x. [para(1011(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 #787 (T,wt=31): 1430 d * b * d * b * d * b * a * a0 = b * b * d * b * d * b * c * a0. [para(1011(a,1),12(a,1,2)),flip(a)]. given #788 (A,wt=33): 319 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 #789 (T,wt=31): 1473 b * a0 * a * a0 * a * a0 * a * x = a * a0 * a * a0 * a * a0 * b * x. [para(1217(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 #790 (T,wt=31): 1490 d * a0 * a * a0 * a * a0 * a * x = c * a0 * a * a0 * a * a0 * b * x. [para(1234(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 #791 (T,wt=31): 1506 c0 * a * c0 * a * c0 * a * b * x = b * a * c0 * a * c0 * a * c0 * x. [para(1255(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 #792 (T,wt=31): 1510 c0 * a * c0 * a * c0 * a * a * b = a * b * a * c0 * a * c0 * a * c0. [para(1255(a,1),12(a,1,2)),flip(a)]. given #793 (A,wt=33): 320 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 #794 (T,wt=31): 1540 b0 * a0 * a * a0 * a * a0 * a * x = a * a0 * a * a0 * a * a0 * b0 * x. [para(1370(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 #795 (T,wt=31): 1554 a0 * c * a0 * c * a0 * c * b0 * x = b0 * a0 * c * a0 * c * a0 * c * x. [para(1391(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 #796 (T,wt=31): 1558 a0 * c * a0 * c * a0 * c * c * b0 = c * b0 * a0 * c * a0 * c * a0 * c. [para(1391(a,1),12(a,1,2)),flip(a)]. given #797 (T,wt=31): 1568 d0 * c0 * a * c0 * a * c0 * a * x = a * c0 * a * c0 * a * c0 * d0 * x. [para(1407(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 #798 (A,wt=33): 322 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 #799 (T,wt=31): 1581 d0 * a * a * c0 * a * c0 * a * c0 = a * c0 * a * c0 * a * c0 * d0 * a. [hyper(173,a,12,a,b,109,a(flip)),rewrite([1203(15)]),flip(a)]. given #800 (T,wt=31): 1582 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([1160(15)]),flip(a)]. given #801 (T,wt=31): 1593 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 #802 (T,wt=31): 1597 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 #803 (A,wt=33): 324 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 #804 (T,wt=31): 1599 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 #805 (T,wt=31): 1605 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 #806 (T,wt=31): 1636 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 #807 (T,wt=31): 1664 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 #808 (A,wt=33): 326 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 #809 (T,wt=31): 1677 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 #810 (T,wt=31): 1680 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 #811 (T,wt=31): 1683 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 #812 (T,wt=31): 2080 d0 * d0 * x * d0 * x * d0 * x * y = x * d0 * x * d0 * x * d0 * d0 * y. [para(2077(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 #813 (A,wt=33): 328 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 #814 (T,wt=31): 2081 x * d0 * d0 * y * d0 * y * d0 * y = x * y * d0 * y * d0 * y * d0 * d0. [para(2077(a,1),1(a,2,2)),rewrite([1(11)])]. given #815 (T,wt=31): 2082 d * d0 * d0 * b0 * d0 * b0 * d0 * b0 = c * c0 * b0 * d0 * b0 * d0 * b0 * d0. [para(2077(a,2),22(a,1,2)),rewrite([534(29)])]. ============================== PROOF ================================= % Proof 1 at 29.18 (+ 0.07) seconds. % Length of proof is 25. % Level of proof is 7. % Maximum clause weight is 31.000. % Given clauses 815. 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 | w * z != u | x * y = w. [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 | w * v5 * z != u | x * y = w * v5. [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)]. 179 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)])]. 359 a0 * d0 * b0 * d0 * b0 * d0 = c0 * b0 * d0 * b0 * d0 * b0. [hyper(2,a,26,a(flip),b,39,a(flip)),flip(a)]. 534 a0 * d0 * b0 * d0 * b0 * d0 * x = c0 * b0 * d0 * b0 * d0 * b0 * x. [para(359(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)]. 2077 d0 * d0 * x * d0 * x * d0 * x = x * d0 * x * d0 * x * d0 * d0. [hyper(47,a,179,a,b,122,a(flip))]. 2082 d * d0 * d0 * b0 * d0 * b0 * d0 * b0 = c * c0 * b0 * d0 * b0 * d0 * b0 * d0. [para(2077(a,2),22(a,1,2)),rewrite([534(29)])]. 2507 d * d0 = c * c0. [hyper(57,a,179,a,b,2082,a),flip(a)]. 2508 $F. [resolve(2507,a,8,a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=815. Generated=188800. Kept=2507. proofs=1. Usable=808. Sos=1609. Demods=234. Limbo=1, Disabled=96. Hints=0. Kept_by_rule=0, Deleted_by_rule=132037. Forward_subsumed=54256. Back_subsumed=43. Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. New_demodulators=284 (0 lex), Back_demodulated=45. Back_unit_deleted=0. Demod_attempts=9741268. Demod_rewrites=787599. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=160404. Nonunit_bsub_feature_tests=9686. Megabytes=3.82. User_CPU=29.18, System_CPU=0.07, Wall_clock=30. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED Exiting with 1 proof. Process 5118 exit (max_proofs) Tue Nov 3 09:42:56 2009