============================== Prover9 ===============================
Prover9 (32) version November-2006, November 2006.
Process 3901 was started by mccune on cleo.thornwood,
Wed Nov 22 11:24:36 2006
The command was "/home/mccune/bin/prover9 -f quot-xy3b.in".
============================== end of head ===========================

============================== INPUT =================================

% Reading from file quot-xy3b.in

op(400,infix_right,*).
set(restrict_denials).
assign(max_weight,35).

formulas(sos).
(x * y) * z = x * y * z # label(associativity).
x * y != u | x * z != u | y = z # label(left_cancellation_extended).
y * x != u | z * x != u | y = z # label(right_cancellation_extended).
x * y * x * y * x * y = y * x * y * x * y * x # label("(xy)^3 = (yx)^3").
b * b0 = a * a0.
d * b0 = c * a0.
b * d0 = a * c0.
d * d0 != c * c0.
end_of_list.

============================== end of input ==========================

============================== PROCESS NON-CLAUSAL FORMULAS ==========

% Formulas that are not ordinary clauses:

============================== end of process non-clausal formulas ===

============================== PROCESS INITIAL CLAUSES ===============

% Clauses before input processing:

formulas(usable).
end_of_list.

formulas(sos).
(x * y) * z = x * y * z # label(associativity).  [assumption].
x * y != z | x * u != z | y = u # label(left_cancellation_extended).  [assumption].
x * y != z | u * y != z | x = u # label(right_cancellation_extended).  [assumption].
x * y * x * y * x * y = y * x * y * x * y * x # label("(xy)^3 = (yx)^3").  [assumption].
b * b0 = a * a0.  [assumption].
d * b0 = c * a0.  [assumption].
b * d0 = a * c0.  [assumption].
d * d0 != c * c0.  [assumption].
end_of_list.

formulas(demodulators).
end_of_list.

============================== PREDICATE ELIMINATION =================

No predicates eliminated.

============================== end predicate elimination =============

Auto_denials:  (no changes).

Term ordering decisions:
Relation symbol precedence:  lex([ = ]).
Function symbol precedence:  lex([ a, a0, b, b0, c, c0, d, d0, * ]).
After inverse_order:  (no changes).
Unfolding symbols: (none).

Auto_inference settings:
  % set(paramodulation).  % (positive equality literals)
    % set(paramodulation) -> set(back_demod).
  % set(hyper_resolution).  % (nonunit Horn with equality)
  % set(neg_ur_resolution).  % (nonunit Horn with equality)
  % assign(para_lit_limit, 3).  % (nonunit Horn with equality)

Auto_process settings:  (no changes).

restricted denial: (wt=7): 8 d * d0 != c * c0.  [assumption].

============================== end of process initial clauses ========

============================== CLAUSES FOR SEARCH ====================

% Clauses after input processing:

formulas(usable).
8 d * d0 != c * c0.  [assumption].
end_of_list.

formulas(sos).
1 (x * y) * z = x * y * z # label(associativity).  [assumption].
2 x * y != z | x * u != z | y = u # label(left_cancellation_extended).  [assumption].
3 x * y != z | u * y != z | x = u # label(right_cancellation_extended).  [assumption].
4 x * y * x * y * x * y = y * x * y * x * y * x # label("(xy)^3 = (yx)^3").  [assumption].
5 b * b0 = a * a0.  [assumption].
6 d * b0 = c * a0.  [assumption].
7 b * d0 = a * c0.  [assumption].
end_of_list.

formulas(demodulators).
1 (x * y) * z = x * y * z # label(associativity).  [assumption].
5 b * b0 = a * a0.  [assumption].
6 d * b0 = c * a0.  [assumption].
7 b * d0 = a * c0.  [assumption].
end_of_list.

============================== end of clauses for search =============

============================== SEARCH ================================

% Starting search at 0.00 seconds.

given #1 (I,wt=11): 1 (x * y) * z = x * y * z # label(associativity).  [assumption].

given #2 (I,wt=13): 2 x * y != z | x * u != z | y = u # label(left_cancellation_extended).  [assumption].

given #3 (I,wt=13): 3 x * y != z | u * y != z | x = u # label(right_cancellation_extended).  [assumption].

given #4 (I,wt=23): 4 x * y * x * y * x * y = y * x * y * x * y * x # label("(xy)^3 = (yx)^3").  [assumption].

given #5 (I,wt=7): 5 b * b0 = a * a0.  [assumption].

given #6 (I,wt=7): 6 d * b0 = c * a0.  [assumption].

given #7 (I,wt=7): 7 b * d0 = a * c0.  [assumption].

given #8 (F,wt=11): 18 b * b0 * x = a * a0 * x.  [para(5(a,1),1(a,1,1)),rewrite(1(4)),flip(a)].

given #9 (T,wt=11): 22 d * b0 * x = c * a0 * x.  [para(6(a,1),1(a,1,1)),rewrite(1(4)),flip(a)].

given #10 (T,wt=11): 26 b * d0 * x = a * c0 * x.  [para(7(a,1),1(a,1,1)),rewrite(1(4)),flip(a)].

given #11 (A,wt=17): 9 x * y * z != u | x * y * v != u | z = v.  [para(1(a,1),2(a,1)),rewrite(1(5))].

given #12 (F,wt=13): 19 a * a0 != x | b * y != x | b0 = y.  [para(5(a,1),2(a,1))].

given #13 (F,wt=13): 20 a * a0 != x | y * b0 != x | b = y.  [para(5(a,1),3(a,1))].

given #14 (T,wt=13): 23 c * a0 != x | d * y != x | b0 = y.  [para(6(a,1),2(a,1))].

given #15 (T,wt=13): 24 c * a0 != x | y * b0 != x | d = y.  [para(6(a,1),3(a,1))].

given #16 (A,wt=17): 10 x * y * z != u | v * z != u | x * y = v.  [para(1(a,1),3(a,1))].

given #17 (F,wt=13): 27 a * c0 != x | b * y != x | d0 = y.  [para(7(a,1),2(a,1))].

given #18 (F,wt=13): 28 a * c0 != x | y * d0 != x | b = y.  [para(7(a,1),3(a,1))].

given #19 (T,wt=13): 53 a * a0 != x | a * c0 != x | d0 = b0.  [para(7(a,1),19(b,1)),flip(c)].

given #20 (T,wt=13): 57 a * a0 != x | c * a0 != x | d = b.  [para(6(a,1),20(b,1)),flip(c)].

given #21 (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 #22 (F,wt=17): 30 a * a0 * x != y | b * z != y | b0 * x = z.  [para(18(a,1),2(a,1))].

given #23 (F,wt=17): 31 a * a0 * x != y | z * b0 * x != y | b = z.  [para(18(a,1),3(a,1))].

given #24 (T,wt=17): 34 c * a0 * x != y | d * z != y | b0 * x = z.  [para(22(a,1),2(a,1))].

given #25 (T,wt=17): 35 c * a0 * x != y | z * b0 * x != y | d = z.  [para(22(a,1),3(a,1))].

given #26 (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 #27 (F,wt=17): 39 a * c0 * x != y | b * z != y | d0 * x = z.  [para(26(a,1),2(a,1))].

given #28 (F,wt=17): 40 a * c0 * x != y | z * d0 * x != y | b = z.  [para(26(a,1),3(a,1))].

given #29 (T,wt=17): 46 x * a * a0 != y | x * b * z != y | b0 = z.  [para(5(a,1),9(a,1,2))].

given #30 (T,wt=17): 47 x * c * a0 != y | x * d * z != y | b0 = z.  [para(6(a,1),9(a,1,2))].

given #31 (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 #32 (F,wt=17): 48 x * a * c0 != y | x * b * z != y | d0 = z.  [para(7(a,1),9(a,1,2))].

given #33 (F,wt=17): 54 a * a0 != x | a * a0 * y != x | b0 * y = b0.  [para(18(a,1),19(b,1)),flip(c)].

given #34 (T,wt=17): 55 a * a0 != x | a * c0 * y != x | d0 * y = b0.  [para(26(a,1),19(b,1)),flip(c)].

given #35 (T,wt=17): 56 a * a0 != x | y * z * b0 != x | y * z = b.  [para(1(a,1),20(b,1)),flip(c)].

given #36 (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 #37 (F,wt=17): 59 c * a0 != x | c * a0 * y != x | b0 * y = b0.  [para(22(a,1),23(b,1)),flip(c)].

given #38 (F,wt=17): 60 c * a0 != x | y * z * b0 != x | y * z = d.  [para(1(a,1),24(b,1)),flip(c)].

given #39 (T,wt=17): 66 x * a * a0 != y | z * b0 != y | x * b = z.  [para(5(a,1),10(a,1,2))].

given #40 (T,wt=17): 67 x * c * a0 != y | z * b0 != y | x * d = z.  [para(6(a,1),10(a,1,2))].

given #41 (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 #42 (F,wt=17): 68 x * a * c0 != y | z * d0 != y | x * b = z.  [para(7(a,1),10(a,1,2))].

given #43 (F,wt=17): 69 x * y * d0 != z | a * c0 != z | x * y = b.  [para(7(a,1),10(b,1))].

given #44 (T,wt=17): 77 a * c0 != x | a * a0 * y != x | b0 * y = d0.  [para(18(a,1),27(b,1)),flip(c)].

given #45 (T,wt=17): 78 a * c0 != x | a * c0 * y != x | d0 * y = d0.  [para(26(a,1),27(b,1)),flip(c)].

given #46 (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 #47 (F,wt=17): 108 a * a0 * x != y | c * a0 * x != y | d = b.  [para(22(a,1),31(b,1)),flip(c)].

given #48 (F,wt=17): 166 x * a * a0 != y | x * a * c0 != y | d0 = b0.  [para(7(a,1),46(b,1,2)),flip(c)].

given #49 (T,wt=17): 191 a * a0 != x | y * a * a0 != x | y * b = b.  [para(5(a,1),56(b,1,2))].

given #50 (T,wt=17): 192 a * a0 != x | y * c * a0 != x | y * d = b.  [para(6(a,1),56(b,1,2))].

given #51 (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 #52 (F,wt=17): 204 c * a0 != x | y * a * a0 != x | y * b = d.  [para(5(a,1),60(b,1,2))].

given #53 (F,wt=17): 205 c * a0 != x | y * c * a0 != x | y * d = d.  [para(6(a,1),60(b,1,2))].

given #54 (T,wt=17): 215 x * a * c0 != y | a * c0 != y | x * b = b.  [para(7(a,1),68(b,1))].

given #55 (T,wt=21): 43 x * y * z * u != v | x * y * z * w != v | u = w.  [para(1(a,1),9(a,1,2)),rewrite(1(6))].

given #56 (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 #57 (F,wt=21): 49 x * a * a0 * y != z | x * b * u != z | b0 * y = u.  [para(18(a,1),9(a,1,2))].

given #58 (F,wt=21): 50 x * c * a0 * y != z | x * d * u != z | b0 * y = u.  [para(22(a,1),9(a,1,2))].

given #59 (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 #60 (T,wt=21): 61 x * y * z * u != v | w * u != v | x * y * z = w.  [para(1(a,1),10(a,1,2))].

given #61 (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 #62 (F,wt=21): 62 x * y * z != u | v * w * z != u | x * y = v * w.  [para(1(a,1),10(b,1))].

given #63 (F,wt=21): 70 x * a * a0 * y != z | u * b0 * y != z | x * b = u.  [para(18(a,1),10(a,1,2))].

given #64 (T,wt=21): 71 x * y * b0 * z != u | a * a0 * z != u | x * y = b.  [para(18(a,1),10(b,1))].

given #65 (T,wt=21): 72 x * c * a0 * y != z | u * b0 * y != z | x * d = u.  [para(22(a,1),10(a,1,2))].

given #66 (A,wt=35): 32 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 #67 (F,wt=21): 73 x * y * b0 * z != u | c * a0 * z != u | x * y = d.  [para(22(a,1),10(b,1))].

given #68 (F,wt=21): 74 x * a * c0 * y != z | u * d0 * y != z | x * b = u.  [para(26(a,1),10(a,1,2))].

given #69 (T,wt=21): 75 x * y * d0 * z != u | a * c0 * z != u | x * y = b.  [para(26(a,1),10(b,1))].

given #70 (T,wt=21): 102 a * a0 * x != y | a * a0 * z != y | b0 * x = b0 * z.  [para(18(a,1),30(b,1))].

given #71 (A,wt=27): 33 b * x * b0 * x * b0 * x * b0 = a * a0 * x * b0 * x * b0 * x.  [para(4(a,1),18(a,1,2))].

given #72 (F,wt=21): 103 a * a0 * x != y | a * c0 * z != y | d0 * z = b0 * x.  [para(26(a,1),30(b,1)),flip(c)].

given #73 (F,wt=21): 112 c * a0 * x != y | c * a0 * z != y | b0 * x = b0 * z.  [para(22(a,1),34(b,1))].

given #74 (T,wt=21): 155 a * c0 * x != y | a * c0 * z != y | d0 * x = d0 * z.  [para(26(a,1),39(b,1))].

given #75 (T,wt=21): 163 x * y * a * a0 != z | x * y * b * u != z | b0 = u.  [para(1(a,1),46(a,1)),rewrite(1(10))].

given #76 (A,wt=35): 36 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 #77 (F,wt=21): 167 x * a * a0 != y | x * a * a0 * z != y | b0 * z = b0.  [para(18(a,1),46(b,1,2)),flip(c)].

given #78 (F,wt=21): 168 x * a * a0 != y | x * a * c0 * z != y | d0 * z = b0.  [para(26(a,1),46(b,1,2)),flip(c)].

given #79 (T,wt=21): 170 x * y * c * a0 != z | x * y * d * u != z | b0 = u.  [para(1(a,1),47(a,1)),rewrite(1(10))].

given #80 (T,wt=21): 173 x * c * a0 != y | x * c * a0 * z != y | b0 * z = b0.  [para(22(a,1),47(b,1,2)),flip(c)].

given #81 (A,wt=27): 37 d * x * b0 * x * b0 * x * b0 = c * a0 * x * b0 * x * b0 * x.  [para(4(a,1),22(a,1,2))].

given #82 (F,wt=21): 178 x * y * a * c0 != z | x * y * b * u != z | d0 = u.  [para(1(a,1),48(a,1)),rewrite(1(10))].

given #83 (F,wt=21): 181 x * a * c0 != y | x * a * a0 * z != y | b0 * z = d0.  [para(18(a,1),48(b,1,2)),flip(c)].

given #84 (T,wt=21): 182 x * a * c0 != y | x * a * c0 * z != y | d0 * z = d0.  [para(26(a,1),48(b,1,2)),flip(c)].

given #85 (T,wt=21): 190 a * a0 != x | y * z * u * b0 != x | y * z * u = b.  [para(1(a,1),56(b,1,2))].

given #86 (A,wt=23): 38 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 #87 (F,wt=21): 203 c * a0 != x | y * z * u * b0 != x | y * z * u = d.  [para(1(a,1),60(b,1,2))].

given #88 (F,wt=21): 206 x * y * a * a0 != z | u * b0 != z | x * y * b = u.  [para(1(a,1),66(a,1)),rewrite(1(12))].

given #89 (T,wt=21): 207 x * a * a0 != y | z * u * b0 != y | x * b = z * u.  [para(1(a,1),66(b,1))].

given #90 (T,wt=21): 208 x * y * c * a0 != z | u * b0 != z | x * y * d = u.  [para(1(a,1),67(a,1)),rewrite(1(12))].

given #91 (A,wt=35): 41 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 #92 (F,wt=21): 209 x * c * a0 != y | z * u * b0 != y | x * d = z * u.  [para(1(a,1),67(b,1))].

given #93 (F,wt=21): 213 x * y * a * c0 != z | u * d0 != z | x * y * b = u.  [para(1(a,1),68(a,1)),rewrite(1(12))].

given #94 (T,wt=21): 214 x * a * c0 != y | z * u * d0 != y | x * b = z * u.  [para(1(a,1),68(b,1))].

given #95 (T,wt=21): 216 x * y * z * d0 != u | a * c0 != u | x * y * z = b.  [para(1(a,1),69(a,1,2))].

given #96 (A,wt=27): 42 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 #97 (F,wt=21): 232 x * y * a * a0 != z | x * y * a * c0 != z | d0 = b0.  [para(1(a,1),166(a,1)),rewrite(1(11))].

given #98 (F,wt=21): 233 a * a0 != x | y * z * a * a0 != x | y * z * b = b.  [para(1(a,1),191(b,1)),rewrite(1(13))].

given #99 (T,wt=21): 234 a * a0 != x | y * z * c * a0 != x | y * z * d = b.  [para(1(a,1),192(b,1)),rewrite(1(13))].

given #100 (T,wt=21): 235 c * a0 != x | y * z * a * a0 != x | y * z * b = d.  [para(1(a,1),204(b,1)),rewrite(1(13))].

given #101 (A,wt=33): 44 x * y * z * y * z * y * z != u | x * z * v != u | y * z * y * z * y = v.  [para(4(a,1),9(a,1,2))].

given #102 (F,wt=21): 236 c * a0 != x | y * z * c * a0 != x | y * z * d = d.  [para(1(a,1),205(b,1)),rewrite(1(13))].

given #103 (F,wt=21): 237 x * y * a * c0 != z | a * c0 != z | x * y * b = b.  [para(1(a,1),215(a,1)),rewrite(1(13))].

given #104 (T,wt=21): 307 x * a * a0 * y != z | a * a0 * y != z | x * b = b.  [para(18(a,1),70(b,1))].

given #105 (T,wt=21): 308 x * a * a0 * y != z | c * a0 * y != z | x * b = d.  [para(22(a,1),70(b,1))].

given #106 (A,wt=29): 45 x * y * x * y * x * y != z | y * x * u != z | y * x * y * x = u.  [para(4(a,1),9(a,1))].

given #107 (F,wt=21): 314 x * c * a0 * y != z | a * a0 * y != z | x * d = b.  [para(22(a,1),71(a,1,2))].

given #108 (F,wt=21): 319 x * c * a0 * y != z | c * a0 * y != z | x * d = d.  [para(22(a,1),72(b,1))].

given #109 (T,wt=21): 328 x * a * c0 * y != z | a * c0 * y != z | x * b = b.  [para(26(a,1),74(b,1))].

given #110 (T,wt=21): 428 x * a * a0 != y | z * a * a0 != y | x * b = z * b.  [para(5(a,1),207(b,1,2))].

given #111 (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 #112 (F,wt=21): 429 x * a * a0 != y | z * c * a0 != y | z * d = x * b.  [para(6(a,1),207(b,1,2)),flip(c)].

given #113 (F,wt=21): 430 x * a * a0 != y | a * a0 * b0 != y | a * a0 = x * b.  [para(18(a,1),207(b,1)),rewrite(5(16)),flip(c)].

given #114 (T,wt=21): 431 x * a * a0 != y | c * a0 * b0 != y | c * a0 = x * b.  [para(22(a,1),207(b,1)),rewrite(6(16)),flip(c)].

given #115 (T,wt=21): 432 x * a * a0 != y | a * c0 * b0 != y | a * c0 = x * b.  [para(26(a,1),207(b,1)),rewrite(7(16)),flip(c)].

given #116 (A,wt=29): 58 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 #117 (F,wt=21): 436 x * c * a0 != y | z * c * a0 != y | x * d = z * d.  [para(6(a,1),209(b,1,2))].

given #118 (F,wt=21): 437 x * c * a0 != y | a * a0 * b0 != y | a * a0 = x * d.  [para(18(a,1),209(b,1)),rewrite(5(16)),flip(c)].

given #119 (T,wt=21): 438 x * c * a0 != y | c * a0 * b0 != y | c * a0 = x * d.  [para(22(a,1),209(b,1)),rewrite(6(16)),flip(c)].

given #120 (T,wt=21): 439 x * c * a0 != y | a * c0 * b0 != y | a * c0 = x * d.  [para(26(a,1),209(b,1)),rewrite(7(16)),flip(c)].

given #121 (A,wt=33): 63 x * y * z * y * z * y * z != u | v * y * z * y * z * y != u | x * z = v.  [para(4(a,1),10(a,1,2))].

given #122 (F,wt=21): 443 x * a * c0 != y | z * a * c0 != y | x * b = z * b.  [para(7(a,1),214(b,1,2))].

given #123 (F,wt=21): 444 x * a * c0 != y | a * a0 * d0 != y | a * a0 = x * b.  [para(18(a,1),214(b,1)),rewrite(5(16)),flip(c)].

given #124 (T,wt=21): 445 x * a * c0 != y | c * a0 * d0 != y | c * a0 = x * b.  [para(22(a,1),214(b,1)),rewrite(6(16)),flip(c)].

given #125 (T,wt=21): 446 x * a * c0 != y | a * c0 * d0 != y | a * c0 = x * b.  [para(26(a,1),214(b,1)),rewrite(7(16)),flip(c)].

given #126 (A,wt=29): 64 x * y * x * y * x * y != z | u * y * x * y * x != z | y * x = u.  [para(4(a,1),10(a,1))].

given #127 (F,wt=23): 193 d0 * a0 * c0 * a0 * c0 * a0 = b0 * c0 * a0 * c0 * a0 * c0.  [hyper(39,a,14,a,b,18,a)].

given #128 (F,wt=23): 336 a0 * d0 * b0 * d0 * b0 * d0 = c0 * b0 * d0 * b0 * d0 * b0.  [hyper(2,a,26,a(flip),b,33,a(flip)),flip(a)].

given #129 (T,wt=25): 238 x * y * z * u * v != w | x * y * z * u * v6 != w | v = v6.  [para(1(a,1),43(a,1,2,2)),rewrite(1(7))].

given #130 (T,wt=25): 241 x * y * a * a0 * z != u | x * y * b * v != u | b0 * z = v.  [para(18(a,1),43(a,1,2,2))].

given #131 (A,wt=33): 65 x * y * z * u * z * u * z != v | z * u * z * u * z * u != v | x * y = u.  [para(4(a,1),10(b,1))].

given #132 (F,wt=25): 242 x * y * c * a0 * z != u | x * y * d * v != u | b0 * z = v.  [para(22(a,1),43(a,1,2,2))].

given #133 (F,wt=25): 243 x * y * a * c0 * z != u | x * y * b * v != u | d0 * z = v.  [para(26(a,1),43(a,1,2,2))].

given #134 (T,wt=25): 259 x * a * a0 * y != z | x * a * a0 * u != z | b0 * y = b0 * u.  [para(18(a,1),49(b,1,2))].

given #135 (T,wt=25): 260 x * a * a0 * y != z | x * a * c0 * u != z | d0 * u = b0 * y.  [para(26(a,1),49(b,1,2)),flip(c)].

given #136 (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 #137 (F,wt=25): 266 x * c * a0 * y != z | x * c * a0 * u != z | b0 * y = b0 * u.  [para(22(a,1),50(b,1,2))].

given #138 (F,wt=25): 271 x * a * c0 * y != z | x * a * c0 * u != z | d0 * y = d0 * u.  [para(26(a,1),51(b,1,2))].

given #139 (T,wt=25): 273 x * y * z * u * v != w | v6 * v != w | x * y * z * u = v6.  [para(1(a,1),61(a,1,2,2))].

given #140 (T,wt=25): 274 x * y * z * u != v | w * v6 * u != v | x * y * z = w * v6.  [para(1(a,1),61(b,1))].

given #141 (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 #142 (F,wt=25): 277 x * y * a * a0 * z != u | v * b0 * z != u | x * y * b = v.  [para(18(a,1),61(a,1,2,2))].

given #143 (F,wt=25): 278 x * y * z * b0 * u != v | a * a0 * u != v | x * y * z = b.  [para(18(a,1),61(b,1))].

given #144 (T,wt=25): 279 x * y * c * a0 * z != u | v * b0 * z != u | x * y * d = v.  [para(22(a,1),61(a,1,2,2))].

given #145 (T,wt=25): 280 x * y * z * b0 * u != v | c * a0 * u != v | x * y * z = d.  [para(22(a,1),61(b,1))].

given #146 (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 #147 (F,wt=25): 281 x * y * a * c0 * z != u | v * d0 * z != u | x * y * b = v.  [para(26(a,1),61(a,1,2,2))].

given #148 (F,wt=25): 282 x * y * z * d0 * u != v | a * c0 * u != v | x * y * z = b.  [para(26(a,1),61(b,1))].

given #149 (T,wt=25): 299 x * a * a0 * y != z | u * v * b0 * y != z | x * b = u * v.  [para(18(a,1),62(a,1,2))].

given #150 (T,wt=25): 300 x * c * a0 * y != z | u * v * b0 * y != z | x * d = u * v.  [para(22(a,1),62(a,1,2))].

given #151 (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 #152 (F,wt=25): 301 x * a * c0 * y != z | u * v * d0 * y != z | x * b = u * v.  [para(26(a,1),62(a,1,2))].

given #153 (F,wt=25): 354 x * y * z * a * a0 != u | x * y * z * b * v != u | b0 = v.  [para(1(a,1),163(a,1,2)),rewrite(1(11))].

given #154 (T,wt=25): 357 x * y * a * a0 != z | x * y * a * a0 * u != z | b0 * u = b0.  [para(18(a,1),163(b,1,2,2)),flip(c)].

given #155 (T,wt=25): 358 x * y * a * a0 != z | x * y * a * c0 * u != z | d0 * u = b0.  [para(26(a,1),163(b,1,2,2)),flip(c)].

given #156 (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 #157 (F,wt=25): 370 x * y * z * c * a0 != u | x * y * z * d * v != u | b0 = v.  [para(1(a,1),170(a,1,2)),rewrite(1(11))].

given #158 (F,wt=25): 373 x * y * c * a0 != z | x * y * c * a0 * u != z | b0 * u = b0.  [para(22(a,1),170(b,1,2,2)),flip(c)].

given #159 (T,wt=25): 391 x * y * z * a * c0 != u | x * y * z * b * v != u | d0 = v.  [para(1(a,1),178(a,1,2)),rewrite(1(11))].

given #160 (T,wt=25): 394 x * y * a * c0 != z | x * y * a * a0 * u != z | b0 * u = d0.  [para(18(a,1),178(b,1,2,2)),flip(c)].

given #161 (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 #162 (F,wt=25): 395 x * y * a * c0 != z | x * y * a * c0 * u != z | d0 * u = d0.  [para(26(a,1),178(b,1,2,2)),flip(c)].

given #163 (F,wt=25): 405 a * a0 != x | y * z * u * v * b0 != x | y * z * u * v = b.  [para(1(a,1),190(b,1,2,2))].

given #164 (T,wt=25): 424 c * a0 != x | y * z * u * v * b0 != x | y * z * u * v = d.  [para(1(a,1),203(b,1,2,2))].

given #165 (T,wt=25): 425 x * y * z * a * a0 != u | v * b0 != u | x * y * z * b = v.  [para(1(a,1),206(a,1,2)),rewrite(1(13))].

given #166 (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 #167 (F,wt=25): 426 x * y * a * a0 != z | u * v * b0 != z | x * y * b = u * v.  [para(1(a,1),206(b,1))].

given #168 (F,wt=25): 427 x * a * a0 != y | z * u * v * b0 != y | z * u * v = x * b.  [para(1(a,1),207(b,1,2)),flip(c)].

given #169 (T,wt=25): 433 x * y * z * c * a0 != u | v * b0 != u | x * y * z * d = v.  [para(1(a,1),208(a,1,2)),rewrite(1(13))].

given #170 (T,wt=25): 434 x * y * c * a0 != z | u * v * b0 != z | x * y * d = u * v.  [para(1(a,1),208(b,1))].

given #171 (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 #172 (F,wt=25): 435 x * c * a0 != y | z * u * v * b0 != y | z * u * v = x * d.  [para(1(a,1),209(b,1,2)),flip(c)].

given #173 (F,wt=25): 440 x * y * z * a * c0 != u | v * d0 != u | x * y * z * b = v.  [para(1(a,1),213(a,1,2)),rewrite(1(13))].

given #174 (T,wt=25): 441 x * y * a * c0 != z | u * v * d0 != z | x * y * b = u * v.  [para(1(a,1),213(b,1))].

given #175 (T,wt=25): 442 x * a * c0 != y | z * u * v * d0 != y | z * u * v = x * b.  [para(1(a,1),214(b,1,2)),flip(c)].

given #176 (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 #177 (F,wt=25): 447 x * y * z * u * d0 != v | a * c0 != v | x * y * z * u = b.  [para(1(a,1),216(a,1,2,2))].

given #178 (F,wt=25): 467 x * y * z * a * a0 != u | x * y * z * a * c0 != u | d0 = b0.  [para(1(a,1),232(a,1,2)),rewrite(1(12))].

given #179 (T,wt=25): 468 a * a0 != x | y * z * u * a * a0 != x | y * z * u * b = b.  [para(1(a,1),233(b,1,2)),rewrite(1(14))].

given #180 (T,wt=25): 469 a * a0 != x | y * z * u * c * a0 != x | y * z * u * d = b.  [para(1(a,1),234(b,1,2)),rewrite(1(14))].

given #181 (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 #182 (F,wt=25): 470 c * a0 != x | y * z * u * a * a0 != x | y * z * u * b = d.  [para(1(a,1),235(b,1,2)),rewrite(1(14))].

given #183 (F,wt=25): 473 c * a0 != x | y * z * u * c * a0 != x | y * z * u * d = d.  [para(1(a,1),236(b,1,2)),rewrite(1(14))].

given #184 (T,wt=25): 474 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 #185 (T,wt=25): 475 x * y * a * a0 * z != u | a * a0 * z != u | x * y * b = b.  [para(1(a,1),307(a,1)),rewrite(1(15))].

given #186 (A,wt=35): 88 b * x * b0 * b0 * x * b0 * b0 * x * b0 = a * a0 * x * b0 * b0 * x * b0 * b0 * x.  [para(11(a,2),18(a,1,2))].

given #187 (F,wt=25): 481 x * y * a * a0 * z != u | c * a0 * z != u | x * y * b = d.  [para(1(a,1),308(a,1)),rewrite(1(15))].

given #188 (F,wt=25): 488 x * y * c * a0 * z != u | a * a0 * z != u | x * y * d = b.  [para(1(a,1),314(a,1)),rewrite(1(15))].

given #189 (T,wt=25): 494 x * y * c * a0 * z != u | c * a0 * z != u | x * y * d = d.  [para(1(a,1),319(a,1)),rewrite(1(15))].

given #190 (T,wt=25): 500 x * y * a * c0 * z != u | a * c0 * z != u | x * y * b = b.  [para(1(a,1),328(a,1)),rewrite(1(15))].

given #191 (A,wt=31): 89 a0 * a * a0 * a0 * a * a0 * a0 * a = a * a0 * a0 * a * a0 * a0 * a * a0.  [para(11(a,1),18(a,2)),rewrite(18(15)),flip(a)].

given #192 (F,wt=25): 506 x * y * a * a0 != z | u * a * a0 != z | x * y * b = u * b.  [para(1(a,1),428(a,1)),rewrite(1(14))].

given #193 (F,wt=25): 508 x * y * a * a0 != z | u * c * a0 != z | x * y * b = u * d.  [para(1(a,1),429(a,1)),rewrite(1(16)),flip(c)].

given #194 (T,wt=25): 509 x * a * a0 != y | z * u * c * a0 != y | z * u * d = x * b.  [para(1(a,1),429(b,1)),rewrite(1(14))].

given #195 (T,wt=25): 510 x * y * a * a0 != z | a * a0 * b0 != z | a * a0 = x * y * b.  [para(1(a,1),430(a,1)),rewrite(1(18))].

given #196 (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 #197 (F,wt=25): 511 x * y * a * a0 != z | c * a0 * b0 != z | c * a0 = x * y * b.  [para(1(a,1),431(a,1)),rewrite(1(18))].

given #198 (F,wt=25): 512 x * y * a * a0 != z | a * c0 * b0 != z | a * c0 = x * y * b.  [para(1(a,1),432(a,1)),rewrite(1(18))].

given #199 (T,wt=25): 514 x * y * c * a0 != z | u * c * a0 != z | x * y * d = u * d.  [para(1(a,1),436(a,1)),rewrite(1(14))].

given #200 (T,wt=25): 515 x * y * c * a0 != z | a * a0 * b0 != z | a * a0 = x * y * d.  [para(1(a,1),437(a,1)),rewrite(1(18))].

given #201 (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 #202 (F,wt=25): 516 x * y * c * a0 != z | c * a0 * b0 != z | c * a0 = x * y * d.  [para(1(a,1),438(a,1)),rewrite(1(18))].

given #203 (F,wt=25): 517 x * y * c * a0 != z | a * c0 * b0 != z | a * c0 = x * y * d.  [para(1(a,1),439(a,1)),rewrite(1(18))].

given #204 (T,wt=25): 521 x * y * a * c0 != z | u * a * c0 != z | x * y * b = u * b.  [para(1(a,1),443(a,1)),rewrite(1(14))].

given #205 (T,wt=25): 522 x * y * a * c0 != z | a * a0 * d0 != z | a * a0 = x * y * b.  [para(1(a,1),444(a,1)),rewrite(1(18))].

given #206 (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 #207 (F,wt=25): 523 x * y * a * c0 != z | c * a0 * d0 != z | c * a0 = x * y * b.  [para(1(a,1),445(a,1)),rewrite(1(18))].

given #208 (F,wt=25): 524 x * y * a * c0 != z | a * c0 * d0 != z | a * c0 = x * y * b.  [para(1(a,1),446(a,1)),rewrite(1(18))].

given #209 (T,wt=25): 652 x * y * z * u != v | a * a0 * u != v | a * a0 = x * y * z.  [para(18(a,1),274(b,1)),rewrite(5(14)),flip(c)].

given #210 (T,wt=25): 655 x * y * z * u != v | c * a0 * u != v | c * a0 = x * y * z.  [para(22(a,1),274(b,1)),rewrite(6(14)),flip(c)].

given #211 (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 #212 (F,wt=25): 658 x * y * z * u != v | a * c0 * u != v | a * c0 = x * y * z.  [para(26(a,1),274(b,1)),rewrite(7(14)),flip(c)].

given #213 (F,wt=25): 710 x * a * a0 * y != z | u * a * a0 * y != z | x * b = u * b.  [para(18(a,1),299(b,1,2))].

given #214 (T,wt=25): 711 x * a * a0 * y != z | a * a0 * b0 * y != z | a * a0 = x * b.  [para(18(a,1),299(b,1)),rewrite(5(18)),flip(c)].

given #215 (T,wt=25): 712 x * a * a0 * y != z | u * c * a0 * y != z | u * d = x * b.  [para(22(a,1),299(b,1,2)),flip(c)].

given #216 (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 #217 (F,wt=25): 713 x * a * a0 * y != z | c * a0 * b0 * y != z | c * a0 = x * b.  [para(22(a,1),299(b,1)),rewrite(6(18)),flip(c)].

given #218 (F,wt=25): 714 x * a * a0 * y != z | a * c0 * b0 * y != z | a * c0 = x * b.  [para(26(a,1),299(b,1)),rewrite(7(18)),flip(c)].

given #219 (T,wt=25): 719 x * c * a0 * y != z | a * a0 * b0 * y != z | a * a0 = x * d.  [para(18(a,1),300(b,1)),rewrite(5(18)),flip(c)].

given #220 (T,wt=25): 720 x * c * a0 * y != z | u * c * a0 * y != z | x * d = u * d.  [para(22(a,1),300(b,1,2))].

given #221 (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 #222 (F,wt=25): 721 x * c * a0 * y != z | c * a0 * b0 * y != z | c * a0 = x * d.  [para(22(a,1),300(b,1)),rewrite(6(18)),flip(c)].

given #223 (F,wt=25): 722 x * c * a0 * y != z | a * c0 * b0 * y != z | a * c0 = x * d.  [para(26(a,1),300(b,1)),rewrite(7(18)),flip(c)].

given #224 (T,wt=25): 730 x * a * c0 * y != z | a * a0 * d0 * y != z | a * a0 = x * b.  [para(18(a,1),301(b,1)),rewrite(5(18)),flip(c)].

given #225 (T,wt=25): 731 x * a * c0 * y != z | c * a0 * d0 * y != z | c * a0 = x * b.  [para(22(a,1),301(b,1)),rewrite(6(18)),flip(c)].

given #226 (A,wt=35): 96 a * c0 * x * d0 * d0 * x * d0 * d0 * x = b * x * d0 * d0 * x * d0 * d0 * x * d0.  [para(11(a,2),26(a,1,2)),flip(a)].

given #227 (F,wt=25): 732 x * a * c0 * y != z | u * a * c0 * y != z | x * b = u * b.  [para(26(a,1),301(b,1,2))].

given #228 (F,wt=25): 733 x * a * c0 * y != z | a * c0 * d0 * y != z | a * c0 = x * b.  [para(26(a,1),301(b,1)),rewrite(7(18)),flip(c)].

given #229 (T,wt=27): 125 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 #230 (T,wt=27): 126 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 #231 (A,wt=31): 97 c0 * a * c0 * c0 * a * c0 * c0 * a = a * c0 * c0 * a * c0 * c0 * a * c0.  [para(11(a,1),26(a,2)),rewrite(26(15)),flip(a)].

given #232 (F,wt=27): 127 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 (F,wt=27): 128 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 #234 (T,wt=27): 130 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 #235 (T,wt=27): 133 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 #236 (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 #237 (F,wt=27): 136 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 (F,wt=27): 245 b * a * a0 * a * a0 * a * a0 = a * a0 * a * a0 * a * a0 * b.  [para(21(a,1),18(a,1,2))].

given #239 (T,wt=27): 246 d * a * a0 * a * a0 * a * a0 = c * a0 * a * a0 * a * a0 * b.  [para(21(a,1),22(a,1,2))].

given #240 (T,wt=27): 286 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 #241 (A,wt=33): 99 a * x * a0 * x * a0 * x * a0 != y | b * z != y | b0 * x * a0 * x * a0 * x = z.  [para(4(a,1),30(a,1,2))].

given #242 (F,wt=27): 379 d * c * a0 * c * a0 * c * a0 = c * a0 * c * a0 * c * a0 * d.  [para(6(a,1),37(a,1,2,2,2,2,2)),rewrite(22(10),22(12),22(22),22(24))].

given #243 (F,wt=27): 408 a * a0 * c * a0 * c * a0 * d = b * a0 * c * a0 * c * a0 * c.  [para(38(a,1),18(a,1,2)),flip(a)].

given #244 (T,wt=27): 409 d * a0 * c * a0 * c * a0 * c = c * a0 * c * a0 * c * a0 * d.  [para(38(a,1),22(a,1,2))].

given #245 (T,wt=27): 526 d0 * a0 * c0 * a0 * c0 * a0 * x = b0 * c0 * a0 * c0 * a0 * c0 * x.  [para(193(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 #246 (A,wt=29): 100 a0 * a * a0 * a * a0 * a != x | b * y != x | b0 * a * a0 * a * a0 = y.  [para(4(a,1),30(a,1))].

given #247 (F,wt=27): 541 a0 * d0 * b0 * d0 * b0 * d0 * x = c0 * b0 * d0 * b0 * d0 * b0 * x.  [para(336(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 (F,wt=27): 895 b0 * a * a0 * a * a0 * a * a0 = a * a0 * a * a0 * a * a0 * b0.  [para(125(a,1),18(a,1)),rewrite(18(9),18(11),21(12),18(22),18(24))].

given #249 (T,wt=27): 896 a0 * a0 * a * a0 * a * a0 * a = a * a0 * a * a0 * a * a0 * a0.  [para(125(a,1),18(a,2)),rewrite(18(13)),flip(a)].

given #250 (T,wt=27): 899 c * a0 * c * a0 * c * a0 * b0 = b0 * a0 * c * a0 * c * a0 * c.  [para(125(a,1),22(a,1)),rewrite(22(9),22(11),38(12),22(22),22(24)),flip(a)].

given #251 (A,wt=33): 101 a * a0 * x != y | z * b * z * b * z * b != y | b0 * x = z * b * z * b * z.  [para(4(a,1),30(b,1))].

given #252 (F,wt=27): 902 d0 * a * c0 * a * c0 * a * c0 = a * c0 * a * c0 * a * c0 * d0.  [para(125(a,1),26(a,1)),rewrite(26(9),26(11),29(12),26(22),26(24))].

given #253 (F,wt=27): 904 c0 * c0 * a * c0 * a * c0 * a = a * c0 * a * c0 * a * c0 * c0.  [para(125(a,1),26(a,2)),rewrite(26(13)),flip(a)].

given #254 (T,wt=27): 1025 d * b * d * b * d * a * a0 = b * d * b * d * b * c * a0.  [para(6(a,1),126(a,1,2,2,2,2,2)),flip(a)].

given #255 (T,wt=27): 1028 d0 * a * c0 * a * c0 * a * a0 = a * c0 * a * c0 * a * c0 * b0.  [para(126(a,1),26(a,1)),rewrite(26(10),26(12),26(22),26(24))].

given #256 (A,wt=33): 104 a * x * a0 * x * a0 * x * a0 != y | z * b0 * x * a0 * x * a0 * x != y | b = z.  [para(4(a,1),31(a,1,2))].

given #257 (F,wt=27): 1124 b0 * a * a0 * a * a0 * a * c0 = a * a0 * a * a0 * a * a0 * d0.  [para(128(a,1),18(a,1)),rewrite(18(10),18(12),18(22),18(24))].

given #258 (F,wt=27): 1230 b * a0 * a * a0 * a * a0 * a = a * a0 * a * a0 * a * a0 * b.  [para(4(a,1),245(a,1,2))].

given #259 (T,wt=27): 1247 d * a0 * a * a0 * a * a0 * a = c * a0 * a * a0 * a * a0 * b.  [para(4(a,1),246(a,1,2))].

given #260 (T,wt=27): 1268 c0 * a * c0 * a * c0 * a * b = b * a * c0 * a * c0 * a * c0.  [para(286(a,1),12(a,1)),flip(a)].

given #261 (A,wt=29): 105 a0 * a * a0 * a * a0 * a != x | y * b0 * a * a0 * a * a0 != x | b = y.  [para(4(a,1),31(a,1))].

given #262 (F,wt=27): 1325 d0 * c0 * a0 * c0 * a0 * c0 * a0 = b0 * c0 * a0 * c0 * a0 * c0 * c0.  [para(4(a,1),526(a,1,2))].

given #263 (F,wt=27): 1346 a0 * b0 * d0 * b0 * d0 * b0 * d0 = c0 * b0 * d0 * b0 * d0 * b0 * b0.  [para(4(a,1),541(a,1,2))].

given #264 (T,wt=27): 1371 b0 * a0 * a * a0 * a * a0 * a = a * a0 * a * a0 * a * a0 * b0.  [para(4(a,1),895(a,1,2))].

given #265 (T,wt=27): 1394 a0 * c * a0 * c * a0 * c * b0 = b0 * a0 * c * a0 * c * a0 * c.  [para(899(a,1),12(a,1)),flip(a)].

given #266 (A,wt=33): 106 a * a0 * x * b0 * x * b0 * x != y | z * x * b0 * x * b0 * x * b0 != y | b = z.  [para(4(a,1),31(b,1,2))].

given #267 (F,wt=27): 1408 d0 * c0 * a * c0 * a * c0 * a = a * c0 * a * c0 * a * c0 * d0.  [para(4(a,1),902(a,1,2))].

given #268 (F,wt=29): 107 a * a0 * x * b0 * x * b0 != y | b0 * x * b0 * x * b0 * x != y | b = x.  [para(4(a,1),31(b,1))].

given #269 (T,wt=29): 110 a0 * c * a0 * c * a0 * c != x | d * y != x | b0 * c * a0 * c * a0 = y.  [para(4(a,1),34(a,1))].

given #270 (T,wt=29): 114 a0 * c * a0 * c * a0 * c != x | y * b0 * c * a0 * c * a0 != x | d = y.  [para(4(a,1),35(a,1))].

given #271 (A,wt=33): 109 c * x * a0 * x * a0 * x * a0 != y | d * z != y | b0 * x * a0 * x * a0 * x = z.  [para(4(a,1),34(a,1,2))].

given #272 (F,wt=29): 116 c * a0 * x * b0 * x * b0 != y | b0 * x * b0 * x * b0 * x != y | d = x.  [para(4(a,1),35(b,1))].

given #273 (F,wt=29): 153 c0 * a * c0 * a * c0 * a != x | b * y != x | d0 * a * c0 * a * c0 = y.  [para(4(a,1),39(a,1))].

given #274 (T,wt=29): 158 c0 * a * c0 * a * c0 * a != x | y * d0 * a * c0 * a * c0 != x | b = y.  [para(4(a,1),40(a,1))].

given #275 (T,wt=29): 160 a * c0 * x * d0 * x * d0 != y | d0 * x * d0 * x * d0 * x != y | b = x.  [para(4(a,1),40(b,1))].

given #276 (A,wt=33): 111 c * a0 * x != y | z * d * z * d * z * d != y | b0 * x = z * d * z * d * z.  [para(4(a,1),34(b,1))].

given #277 (F,wt=29): 165 x * a * a0 != y | b * x * b * x * b * x != y | x * b * x * b = b0.  [para(4(a,1),46(b,1)),flip(c)].

given #278 (F,wt=29): 172 x * c * a0 != y | d * x * d * x * d * x != y | x * d * x * d = b0.  [para(4(a,1),47(b,1)),flip(c)].

given #279 (T,wt=29): 180 x * a * c0 != y | b * x * b * x * b * x != y | x * b * x * b = d0.  [para(4(a,1),48(b,1)),flip(c)].

given #280 (T,wt=29): 185 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 (A,wt=33): 113 c * x * a0 * x * a0 * x * a0 != y | z * b0 * x * a0 * x * a0 * x != y | d = z.  [para(4(a,1),35(a,1,2))].

given #282 (F,wt=29): 188 a * a0 != x | c0 * a * c0 * a * c0 * a != x | d0 * a * c0 * a * c0 = b0.  [para(4(a,1),55(b,1))].

given #283 (F,wt=29): 201 c * a0 != x | a0 * c * a0 * c * a0 * c != x | b0 * c * a0 * c * a0 = b0.  [para(4(a,1),59(b,1))].

given #284 (T,wt=29): 210 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 #285 (T,wt=29): 211 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 #286 (A,wt=33): 115 c * a0 * x * b0 * x * b0 * x != y | z * x * b0 * x * b0 * x * b0 != y | d = z.  [para(4(a,1),35(b,1,2))].

given #287 (F,wt=29): 212 a * c0 * a * c0 * a * c0 != x | d0 * y != x | a * c0 * a * c0 * b = y.  [para(7(a,1),15(a,1,2,2,2,2)),rewrite(26(9),26(11),26(22),26(24))].

given #288 (F,wt=29): 218 a * c0 != x | a0 * a * a0 * a * a0 * a != x | b0 * a * a0 * a * a0 = d0.  [para(4(a,1),77(b,1))].

given #289 (T,wt=29): 221 a * c0 != x | c0 * a * c0 * a * c0 * a != x | d0 * a * c0 * a * c0 = d0.  [para(4(a,1),78(b,1))].

given #290 (T,wt=29): 223 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 #291 (A,wt=35): 117 b0 * d * c * a0 * d * c * a0 * d * x = c * a0 * d * c * a0 * d * c * a0 * x.  [hyper(34,a,1,a(flip),b,12,a),rewrite(1(12),1(14),1(28),1(30),1(32))].

given #292 (F,wt=29): 224 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 #293 (F,wt=29): 225 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 #294 (T,wt=29): 227 a0 * a * a0 * a * a0 * a != x | c * a0 * a * a0 * a * a0 != x | d = b.  [para(4(a,1),108(a,1))].

given #295 (T,wt=29): 229 a * a0 * c * a0 * c * a0 != x | a0 * c * a0 * c * a0 * c != x | d = b.  [para(4(a,1),108(b,1))].

given #296 (A,wt=35): 118 b0 * b * a * a0 * b * a * a0 * b * x = a * a0 * b * a * a0 * b * a * a0 * x.  [hyper(30,a,1,a(flip),b,12,a),rewrite(1(12),1(14),1(28),1(30),1(32))].

given #297 (F,wt=29): 240 x * y * x * y * x * y != z | y * x * y * u != z | x * y * x = u.  [para(4(a,1),43(a,1))].

given #298 (F,wt=29): 248 a * a0 * a * a0 * a * a0 != x | b0 * a * y != x | a0 * a * a0 * b = y.  [para(21(a,1),9(a,1))].

given #299 (T,wt=29): 250 a * a0 * a * a0 * a * a0 != x | y * a0 * a * a0 * b != x | b0 * a = y.  [para(21(a,1),10(a,1))].

given #300 (T,wt=29): 255 a * a0 * a * a0 * a * a0 != x | b0 * a * a0 * y != x | a * a0 * b = y.  [para(21(a,1),43(a,1))].

given #301 (A,wt=31): 119 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 #302 (F,wt=29): 257 a * a0 * a * a0 * a * a0 != x | a0 * b * y != x | b0 * a * a0 * a = y.  [para(4(a,1),49(a,1))].

given #303 (F,wt=29): 262 a * a0 * a * a0 * a * a0 != x | b0 * b * y != x | b0 * a * a0 * b = y.  [para(21(a,1),49(a,1))].

given #304 (T,wt=29): 264 c * a0 * c * a0 * c * a0 != x | a0 * d * y != x | b0 * c * a0 * c = y.  [para(4(a,1),50(a,1))].

given #305 (T,wt=29): 269 a * c0 * a * c0 * a * c0 != x | c0 * b * y != x | d0 * a * c0 * a = y.  [para(4(a,1),51(a,1))].

given #306 (A,wt=33): 120 x * y * x * y * x * y * z != u | y * v != u | x * y * x * y * x * z = v.  [para(12(a,1),2(a,1))].

given #307 (F,wt=29): 276 x * y * x * y * x * y != z | u * x * y * x != z | y * x * y = u.  [para(4(a,1),61(a,1))].

given #308 (F,wt=29): 285 a * a0 * a * a0 * a * a0 != x | y * a * a0 * b != x | b0 * a * a0 = y.  [para(21(a,1),61(a,1))].

given #309 (T,wt=29): 288 a * c0 * a * c0 * a * c0 != x | d0 * a * y != x | c0 * a * c0 * b = y.  [para(29(a,1),9(a,1))].

given #310 (T,wt=29): 290 a * c0 * a * c0 * a * c0 != x | y * c0 * a * c0 * b != x | d0 * a = y.  [para(29(a,1),10(a,1))].

given #311 (A,wt=33): 121 x * y * x * y * x * y * z != u | v * x * y * x * y * x * z != u | y = v.  [para(12(a,1),3(a,1))].

given #312 (F,wt=29): 293 a * c0 * a * c0 * a * c0 != x | d0 * a * c0 * y != x | a * c0 * b = y.  [para(29(a,1),43(a,1))].

given #313 (F,wt=29): 294 a * c0 * a * c0 * a * c0 != x | d0 * b * y != x | d0 * a * c0 * b = y.  [para(29(a,1),51(a,1))].

given #314 (T,wt=29): 296 a * c0 * a * c0 * a * c0 != x | y * a * c0 * b != x | d0 * a * c0 = y.  [para(29(a,1),61(a,1))].

given #315 (T,wt=29): 305 a * a0 * a * a0 * a * a0 != x | y * b0 * a * a0 * a != x | a0 * b = y.  [para(4(a,1),70(a,1))].

given #316 (A,wt=33): 122 x * y * z * y * z * y * u != v | y * z * y * z * y * z * u != v | x = z.  [para(12(a,1),3(b,1))].

given #317 (F,wt=29): 310 a * a0 * a * a0 * a * a0 != x | y * b0 * a * a0 * b != x | b0 * b = y.  [para(21(a,1),70(a,1))].

given #318 (F,wt=29): 312 x * b0 * x * b0 * x * b0 != y | a * a0 * x * b0 * x != y | b0 * x = b.  [para(4(a,1),71(a,1))].

given #319 (T,wt=29): 317 c * a0 * c * a0 * c * a0 != x | y * b0 * c * a0 * c != x | a0 * d = y.  [para(4(a,1),72(a,1))].

given #320 (T,wt=29): 322 x * b0 * x * b0 * x * b0 != y | c * a0 * x * b0 * x != y | b0 * x = d.  [para(4(a,1),73(a,1))].

given #321 (A,wt=35): 123 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 #322 (F,wt=29): 326 a * c0 * a * c0 * a * c0 != x | y * d0 * a * c0 * a != x | c0 * b = y.  [para(4(a,1),74(a,1))].

given #323 (F,wt=29): 330 a * c0 * a * c0 * a * c0 != x | y * d0 * a * c0 * b != x | d0 * b = y.  [para(29(a,1),74(a,1))].

given #324 (T,wt=29): 332 x * d0 * x * d0 * x * d0 != y | a * c0 * x * d0 * x != y | d0 * x = b.  [para(4(a,1),75(a,1))].

given #325 (T,wt=29): 356 b * x * a * a0 != y | x * b * x * b * x * b != y | x * b * x = b0.  [para(4(a,1),163(b,1)),flip(c)].

given #326 (A,wt=31): 124 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 #327 (F,wt=29): 363 a0 * a * a0 != x | a * a0 * a * a0 * a * a0 != x | b0 * a * a0 * a = b0.  [para(4(a,1),167(b,1))].

given #328 (F,wt=29): 365 b0 * a * a0 != x | a * a0 * a * a0 * a * a0 != x | b0 * a * a0 * b = b0.  [para(21(a,1),167(b,1))].

given #329 (T,wt=29): 367 c0 * a * a0 != x | a * c0 * a * c0 * a * c0 != x | d0 * a * c0 * a = b0.  [para(4(a,1),168(b,1))].

given #330 (T,wt=29): 369 d0 * a * a0 != x | a * c0 * a * c0 * a * c0 != x | d0 * a * c0 * b = b0.  [para(29(a,1),168(b,1))].

given #331 (A,wt=31): 129 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 #332 (F,wt=29): 372 d * x * c * a0 != y | x * d * x * d * x * d != y | x * d * x = b0.  [para(4(a,1),170(b,1)),flip(c)].

given #333 (F,wt=29): 376 a0 * c * a0 != x | c * a0 * c * a0 * c * a0 != x | b0 * c * a0 * c = b0.  [para(4(a,1),173(b,1))].

given #334 (T,wt=29): 393 b * x * a * c0 != y | x * b * x * b * x * b != y | x * b * x = d0.  [para(4(a,1),178(b,1)),flip(c)].

given #335 (T,wt=29): 398 a0 * a * c0 != x | a * a0 * a * a0 * a * a0 != x | b0 * a * a0 * a = d0.  [para(4(a,1),181(b,1))].

given #336 (A,wt=31): 131 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 #337 (F,wt=29): 400 b0 * a * c0 != x | a * a0 * a * a0 * a * a0 != x | b0 * a * a0 * b = d0.  [para(21(a,1),181(b,1))].

given #338 (F,wt=29): 402 c0 * a * c0 != x | a * c0 * a * c0 * a * c0 != x | d0 * a * c0 * a = d0.  [para(4(a,1),182(b,1))].

given #339 (T,wt=29): 404 d0 * a * c0 != x | a * c0 * a * c0 * a * c0 != x | d0 * a * c0 * b = d0.  [para(29(a,1),182(b,1))].

given #340 (T,wt=29): 406 a0 * c * a0 * c * a0 * c != x | b0 * y != x | c * a0 * c * a0 * d = y.  [para(38(a,1),2(a,1))].

given #341 (A,wt=31): 132 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 #342 (F,wt=29): 407 a0 * c * a0 * c * a0 * c != x | y * c * a0 * c * a0 * d != x | b0 = y.  [para(38(a,1),3(a,1))].

given #343 (F,wt=29): 411 a0 * c * a0 * c * a0 * c != x | b0 * c * y != x | a0 * c * a0 * d = y.  [para(38(a,1),9(a,1))].

given #344 (T,wt=29): 413 a0 * c * a0 * c * a0 * c != x | y * a0 * c * a0 * d != x | b0 * c = y.  [para(38(a,1),10(a,1))].

given #345 (T,wt=29): 417 a0 * c * a0 * c * a0 * c != x | b0 * c * a0 * y != x | c * a0 * d = y.  [para(38(a,1),43(a,1))].

given #346 (A,wt=31): 134 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 #347 (F,wt=29): 418 a0 * c * a0 * c * a0 * c != x | b0 * d * y != x | b0 * c * a0 * d = y.  [para(38(a,1),50(a,1))].

given #348 (F,wt=29): 420 a0 * c * a0 * c * a0 * c != x | y * c * a0 * d != x | b0 * c * a0 = y.  [para(38(a,1),61(a,1))].

given #349 (T,wt=29): 422 a0 * c * a0 * c * a0 * c != x | y * b0 * c * a0 * d != x | b0 * d = y.  [para(38(a,1),72(a,1))].

given #350 (T,wt=29): 423 b0 * c * a0 != x | a0 * c * a0 * c * a0 * c != x | b0 * c * a0 * d = b0.  [para(38(a,1),173(b,1))].

given #351 (A,wt=31): 135 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 #352 (F,wt=29): 477 a * a0 * a * a0 * a * a0 != x | a * a0 * a * a0 * a != x | a0 * b = b.  [para(4(a,1),307(a,1))].

given #353 (F,wt=29): 480 a * a0 * a * a0 * a * a0 != x | a * a0 * a * a0 * b != x | b0 * b = b.  [para(21(a,1),307(a,1))].

given #354 (T,wt=29): 483 a * a0 * a * a0 * a * a0 != x | c * a0 * a * a0 * a != x | a0 * b = d.  [para(4(a,1),308(a,1))].

given #355 (T,wt=29): 486 a * a0 * a * a0 * a * a0 != x | c * a0 * a * a0 * b != x | b0 * b = d.  [para(21(a,1),308(a,1))].

given #356 (A,wt=31): 137 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 #357 (F,wt=29): 487 c * a0 * c * a0 * c * a0 != x | b0 * d * y != x | b0 * c * a0 * d = y.  [para(6(a,1),45(a,1,2,2,2,2)),rewrite(22(9),22(11),22(23))].

given #358 (F,wt=29): 490 c * a0 * c * a0 * c * a0 != x | a * a0 * c * a0 * c != x | a0 * d = b.  [para(4(a,1),314(a,1))].

given #359 (T,wt=29): 493 a0 * c * a0 * c * a0 * c != x | a * a0 * c * a0 * d != x | b0 * d = b.  [para(38(a,1),314(a,1))].

given #360 (T,wt=29): 496 c * a0 * c * a0 * c * a0 != x | c * a0 * c * a0 * c != x | a0 * d = d.  [para(4(a,1),319(a,1))].

given #361 (A,wt=33): 138 x * y * x * y * x * y * z != u | y * x * v != u | y * x * y * x * z = v.  [para(12(a,1),9(a,1))].

given #362 (F,wt=29): 499 a0 * c * a0 * c * a0 * c != x | c * a0 * c * a0 * d != x | b0 * d = d.  [para(38(a,1),319(a,1))].

given #363 (F,wt=29): 502 a * c0 * a * c0 * a * c0 != x | a * c0 * a * c0 * a != x | c0 * b = b.  [para(4(a,1),328(a,1))].

given #364 (T,wt=29): 505 a * c0 * a * c0 * a * c0 != x | a * c0 * a * c0 * b != x | d0 * b = b.  [para(29(a,1),328(a,1))].

given #365 (T,wt=29): 507 a * a0 != x | b * y * b * y * b * y != x | y * b * y * b * y = b0.  [para(4(a,1),52(b,1))].

given #366 (A,wt=33): 139 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 #367 (F,wt=29): 513 c * a0 != x | d * y * d * y * d * y != x | y * d * y * d * y = b0.  [para(4(a,1),58(b,1))].

given #368 (F,wt=29): 525 c * a0 * c * a0 * c * a0 != x | y * b0 * c * a0 * d != x | b0 * d = y.  [para(6(a,1),64(a,1,2,2,2,2)),rewrite(22(9),22(11),22(18))].

given #369 (T,wt=29): 527 b0 * c0 * a0 * c0 * a0 * c0 != x | d0 * y != x | a0 * c0 * a0 * c0 * a0 = y.  [para(193(a,1),2(a,1))].

given #370 (T,wt=29): 528 b0 * c0 * a0 * c0 * a0 * c0 != x | y * a0 * c0 * a0 * c0 * a0 != x | d0 = y.  [para(193(a,1),3(a,1))].

given #371 (A,wt=33): 140 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 #372 (F,wt=29): 530 b0 * c0 * a0 * c0 * a0 * c0 != x | d0 * a0 * y != x | c0 * a0 * c0 * a0 = y.  [para(193(a,1),9(a,1))].

given #373 (F,wt=29): 532 b0 * c0 * a0 * c0 * a0 * c0 != x | y * c0 * a0 * c0 * a0 != x | d0 * a0 = y.  [para(193(a,1),10(a,1))].

given #374 (T,wt=29): 534 a0 * c0 * a0 * c0 * a0 * c0 != x | b0 * c0 * a0 * c0 * a0 * c0 != x | d0 = c0.  [para(193(a,1),16(b,1)),flip(c)].

given #375 (T,wt=29): 536 b0 * c0 * a0 * c0 * a0 * c0 != x | d0 * a0 * c0 * y != x | a0 * c0 * a0 = y.  [para(193(a,1),43(a,1))].

given #376 (A,wt=33): 141 x * y * x * y * x * y * z != u | v * y * x * y * x * z != u | y * x = v.  [para(12(a,1),10(a,1))].

given #377 (F,wt=29): 538 b0 * c0 * a0 * c0 * a0 * c0 != x | y * a0 * c0 * a0 != x | d0 * a0 * c0 = y.  [para(193(a,1),61(a,1))].

given #378 (F,wt=29): 542 c0 * b0 * d0 * b0 * d0 * b0 != x | a0 * y != x | d0 * b0 * d0 * b0 * d0 = y.  [para(336(a,1),2(a,1))].

given #379 (T,wt=29): 543 c0 * b0 * d0 * b0 * d0 * b0 != x | y * d0 * b0 * d0 * b0 * d0 != x | a0 = y.  [para(336(a,1),3(a,1))].

given #380 (T,wt=29): 545 c0 * b0 * d0 * b0 * d0 * b0 != x | a0 * d0 * y != x | b0 * d0 * b0 * d0 = y.  [para(336(a,1),9(a,1))].

given #381 (A,wt=33): 142 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 #382 (F,wt=29): 547 c0 * b0 * d0 * b0 * d0 * b0 != x | y * b0 * d0 * b0 * d0 != x | a0 * d0 = y.  [para(336(a,1),10(a,1))].

given #383 (F,wt=29): 551 a * c0 * b0 * d0 * b0 * d0 != x | c0 * b0 * d0 * b0 * d0 * b0 != x | b = a0.  [para(336(a,1),40(b,1))].

given #384 (T,wt=29): 553 d0 * b0 * d0 * b0 * d0 * b0 != x | c0 * b0 * d0 * b0 * d0 * b0 != x | b0 = a0.  [para(336(a,1),16(b,1))].

given #385 (T,wt=29): 555 c0 * b0 * d0 * b0 * d0 * b0 != x | a0 * d0 * b0 * y != x | d0 * b0 * d0 = y.  [para(336(a,1),43(a,1))].

given #386 (A,wt=33): 143 a0 * a * a0 * a * a0 * a * x != y | b * z != y | b0 * a * a0 * a * a0 * x = z.  [para(12(a,1),30(a,1))].

given #387 (F,wt=29): 557 c0 * b0 * d0 * b0 * d0 * b0 != x | y * d0 * b0 * d0 != x | a0 * d0 * b0 = y.  [para(336(a,1),61(a,1))].

given #388 (F,wt=29): 559 c0 * b0 * d0 * b0 * d0 * b0 != x | a * a0 * d0 * b0 * d0 != x | a0 * d0 = b.  [para(336(a,1),71(a,1))].

given #389 (T,wt=29): 560 c0 * b0 * d0 * b0 * d0 * b0 != x | c * a0 * d0 * b0 * d0 != x | a0 * d0 = d.  [para(336(a,1),73(a,1))].

given #390 (T,wt=29): 564 x * y * z * u * v * w != v6 | x * y * z * u * v * v7 != v6 | w = v7.  [para(1(a,1),238(a,1,2,2,2)),rewrite(1(8))].

given #391 (A,wt=33): 144 a0 * a * a0 * a * a0 * a * x != y | z * b0 * a * a0 * a * a0 * x != y | b = z.  [para(12(a,1),31(a,1))].

given #392 (F,wt=29): 566 x * y * x * y * x * y != z | y * x * y * x * u != z | y * x = u.  [para(4(a,1),238(a,1))].

given #393 (F,wt=29): 567 x * y * z * a * a0 * u != v | x * y * z * b * w != v | b0 * u = w.  [para(18(a,1),238(a,1,2,2,2))].

given #394 (T,wt=29): 568 x * y * z * c * a0 * u != v | x * y * z * d * w != v | b0 * u = w.  [para(22(a,1),238(a,1,2,2,2))].

given #395 (T,wt=29): 569 x * y * z * a * c0 * u != v | x * y * z * b * w != v | d0 * u = w.  [para(26(a,1),238(a,1,2,2,2))].

given #396 (A,wt=33): 145 a * a0 * x * b0 * x * b0 * y != z | b0 * x * b0 * x * b0 * x * y != z | b = x.  [para(12(a,1),31(b,1))].

given #397 (F,wt=29): 572 a * a0 * a * a0 * a * a0 != x | b0 * a * a0 * a * y != x | a0 * b = y.  [para(21(a,1),238(a,1))].

given #398 (F,wt=29): 574 a * c0 * a * c0 * a * c0 != x | d0 * a * c0 * a * y != x | c0 * b = y.  [para(29(a,1),238(a,1))].

given #399 (T,wt=29): 578 a0 * c * a0 * c * a0 * c != x | b0 * c * a0 * c * y != x | a0 * d = y.  [para(38(a,1),238(a,1))].

given #400 (T,wt=29): 582 b0 * c0 * a0 * c0 * a0 * c0 != x | d0 * a0 * c0 * a0 * y != x | c0 * a0 = y.  [para(193(a,1),238(a,1))].

given #401 (A,wt=33): 146 a0 * c * a0 * c * a0 * c * x != y | d * z != y | b0 * c * a0 * c * a0 * x = z.  [para(12(a,1),34(a,1))].

given #402 (F,wt=29): 584 c0 * b0 * d0 * b0 * d0 * b0 != x | a0 * d0 * b0 * d0 * y != x | b0 * d0 = y.  [para(336(a,1),238(a,1))].

given #403 (F,wt=29): 586 a0 * a * a0 * a * a0 * a != x | a * a0 * b * y != x | b0 * a * a0 = y.  [para(4(a,1),241(a,1))].

given #404 (T,wt=29): 588 x * y * a * a0 * z != u | x * y * a * a0 * v != u | b0 * z = b0 * v.  [para(18(a,1),241(b,1,2,2))].

given #405 (T,wt=29): 589 x * y * a * a0 * z != u | x * y * a * c0 * v != u | d0 * v = b0 * z.  [para(26(a,1),241(b,1,2,2)),flip(c)].

given #406 (A,wt=33): 147 a0 * c * a0 * c * a0 * c * x != y | z * b0 * c * a0 * c * a0 * x != y | d = z.  [para(12(a,1),35(a,1))].

given #407 (F,wt=29): 601 a0 * c * a0 * c * a0 * c != x | c * a0 * d * y != x | b0 * c * a0 = y.  [para(4(a,1),242(a,1))].

given #408 (F,wt=29): 603 x * y * c * a0 * z != u | x * y * c * a0 * v != u | b0 * z = b0 * v.  [para(22(a,1),242(b,1,2,2))].

given #409 (T,wt=29): 607 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): 609 x * y * a * c0 * z != u | x * y * a * c0 * v != u | d0 * z = d0 * v.  [para(26(a,1),243(b,1,2,2))].

given #411 (A,wt=33): 148 c * a0 * x * b0 * x * b0 * y != z | b0 * x * b0 * x * b0 * x * y != z | d = x.  [para(12(a,1),35(b,1))].

given #412 (F,wt=29): 618 a * c0 != x | b * y * b * y * b * y != x | y * b * y * b * y = d0.  [para(4(a,1),76(b,1))].

given #413 (F,wt=29): 623 x * y * z * u * v * w != v6 | v7 * w != v6 | x * y * z * u * v = v7.  [para(1(a,1),273(a,1,2,2,2))].

given #414 (T,wt=29): 624 x * y * z * u * v != w | v6 * v7 * v != w | x * y * z * u = v6 * v7.  [para(1(a,1),273(b,1))].

given #415 (T,wt=29): 626 x * y * x * y * x * y != z | u * y * x != z | y * x * y * x = u.  [para(4(a,1),273(a,1))].

given #416 (A,wt=35): 149 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 #417 (F,wt=29): 627 x * y * z * a * a0 * u != v | w * b0 * u != v | x * y * z * b = w.  [para(18(a,1),273(a,1,2,2,2))].

given #418 (F,wt=29): 628 x * y * z * u * b0 * v != w | a * a0 * v != w | x * y * z * u = b.  [para(18(a,1),273(b,1))].

given #419 (T,wt=29): 629 x * y * z * c * a0 * u != v | w * b0 * u != v | x * y * z * d = w.  [para(22(a,1),273(a,1,2,2,2))].

given #420 (T,wt=29): 630 x * y * z * u * b0 * v != w | c * a0 * v != w | x * y * z * u = d.  [para(22(a,1),273(b,1))].

given #421 (A,wt=31): 150 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 #422 (F,wt=29): 631 x * y * z * a * c0 * u != v | w * d0 * u != v | x * y * z * b = w.  [para(26(a,1),273(a,1,2,2,2))].

given #423 (F,wt=29): 632 x * y * z * u * d0 * v != w | a * c0 * v != w | x * y * z * u = b.  [para(26(a,1),273(b,1))].

given #424 (T,wt=29): 635 a * a0 * a * a0 * a * a0 != x | y * a0 * b != x | b0 * a * a0 * a = y.  [para(21(a,1),273(a,1))].

given #425 (T,wt=29): 637 a * c0 * a * c0 * a * c0 != x | y * c0 * b != x | d0 * a * c0 * a = y.  [para(29(a,1),273(a,1))].

given #426 (A,wt=35): 151 d0 * b * a * c0 * b * a * c0 * b * x = a * c0 * b * a * c0 * b * a * c0 * x.  [hyper(39,a,1,a(flip),b,12,a),rewrite(1(12),1(14),1(28),1(30),1(32))].

given #427 (F,wt=29): 641 a0 * c * a0 * c * a0 * c != x | y * a0 * d != x | b0 * c * a0 * c = y.  [para(38(a,1),273(a,1))].

given #428 (F,wt=29): 645 b0 * c0 * a0 * c0 * a0 * c0 != x | y * c0 * a0 != x | d0 * a0 * c0 * a0 = y.  [para(193(a,1),273(a,1))].

given #429 (T,wt=29): 647 c0 * b0 * d0 * b0 * d0 * b0 != x | y * b0 * d0 != x | a0 * d0 * b0 * d0 = y.  [para(336(a,1),273(a,1))].

given #430 (T,wt=29): 648 x * y * z * u != v | w * v6 * v7 * u != v | x * y * z = w * v6 * v7.  [para(1(a,1),274(b,1,2))].

given #431 (A,wt=33): 152 a * x * c0 * x * c0 * x * c0 != y | b * z != y | d0 * x * c0 * x * c0 * x = z.  [para(4(a,1),39(a,1,2))].

given #432 (F,wt=29): 650 x * y * a * a0 * z != u | v * w * b0 * z != u | x * y * b = v * w.  [para(18(a,1),274(a,1,2,2))].

given #433 (F,wt=29): 651 x * y * z * b0 * u != v | w * a * a0 * u != v | x * y * z = w * b.  [para(18(a,1),274(b,1,2))].

given #434 (T,wt=29): 653 x * y * c * a0 * z != u | v * w * b0 * z != u | x * y * d = v * w.  [para(22(a,1),274(a,1,2,2))].

given #435 (T,wt=29): 654 x * y * z * b0 * u != v | w * c * a0 * u != v | x * y * z = w * d.  [para(22(a,1),274(b,1,2))].

given #436 (A,wt=33): 154 a * c0 * x != y | z * b * z * b * z * b != y | d0 * x = z * b * z * b * z.  [para(4(a,1),39(b,1))].

given #437 (F,wt=29): 656 x * y * a * c0 * z != u | v * w * d0 * z != u | x * y * b = v * w.  [para(26(a,1),274(a,1,2,2))].

given #438 (F,wt=29): 657 x * y * z * d0 * u != v | w * a * c0 * u != v | x * y * z = w * b.  [para(26(a,1),274(b,1,2))].

given #439 (T,wt=29): 677 a0 * a * a0 * a * a0 * a != x | y * b0 * a * a0 != x | a * a0 * b = y.  [para(4(a,1),277(a,1))].

given #440 (T,wt=29): 681 b0 * x * b0 * x * b0 * x != y | a * a0 * x * b0 != y | x * b0 * x = b.  [para(4(a,1),278(a,1))].

given #441 (A,wt=33): 156 c0 * a * c0 * a * c0 * a * x != y | b * z != y | d0 * a * c0 * a * c0 * x = z.  [para(12(a,1),39(a,1))].

given #442 (F,wt=29): 686 a0 * c * a0 * c * a0 * c != x | y * b0 * c * a0 != x | c * a0 * d = y.  [para(4(a,1),279(a,1))].

given #443 (F,wt=29): 690 b0 * x * b0 * x * b0 * x != y | c * a0 * x * b0 != y | x * b0 * x = d.  [para(4(a,1),280(a,1))].

given #444 (T,wt=29): 699 c0 * a * c0 * a * c0 * a != x | y * d0 * a * c0 != x | a * c0 * b = y.  [para(4(a,1),281(a,1))].

given #445 (T,wt=29): 703 d0 * x * d0 * x * d0 * x != y | a * c0 * x * d0 != y | x * d0 * x = b.  [para(4(a,1),282(a,1))].

given #446 (A,wt=33): 157 a * x * c0 * x * c0 * x * c0 != y | z * d0 * x * c0 * x * c0 * x != y | b = z.  [para(4(a,1),40(a,1,2))].

given #447 (F,wt=29): 707 c0 * b0 * d0 * b0 * d0 * b0 != x | a * c0 * b0 * d0 != x | a0 * d0 * b0 = b.  [para(336(a,1),282(a,1))].

given #448 (F,wt=29): 735 x * y * z * u * a * a0 != v | x * y * z * u * b * w != v | b0 = w.  [para(1(a,1),354(a,1,2,2)),rewrite(1(12))].

given #449 (T,wt=29): 737 x * b * x * a * a0 != y | b * x * b * x * b * x != y | x * b = b0.  [para(4(a,1),354(b,1)),flip(c)].

given #450 (T,wt=29): 738 x * y * z * a * a0 != u | x * y * z * a * a0 * v != u | b0 * v = b0.  [para(18(a,1),354(b,1,2,2,2)),flip(c)].

given #451 (A,wt=33): 159 a * c0 * x * d0 * x * d0 * x != y | z * x * d0 * x * d0 * x * d0 != y | b = z.  [para(4(a,1),40(b,1,2))].

given #452 (F,wt=29): 739 x * y * z * a * a0 != u | x * y * z * a * c0 * v != u | d0 * v = b0.  [para(26(a,1),354(b,1,2,2,2)),flip(c)].

given #453 (F,wt=29): 744 a * a0 * a * a0 != x | a0 * a * a0 * a * a0 * a != x | b0 * a * a0 = b0.  [para(4(a,1),357(b,1))].

given #454 (T,wt=29): 748 a * c0 * a * a0 != x | c0 * a * c0 * a * c0 * a != x | d0 * a * c0 = b0.  [para(4(a,1),358(b,1))].

given #455 (T,wt=29): 753 x * y * z * u * c * a0 != v | x * y * z * u * d * w != v | b0 = w.  [para(1(a,1),370(a,1,2,2)),rewrite(1(12))].

given #456 (A,wt=33): 161 c0 * a * c0 * a * c0 * a * x != y | z * d0 * a * c0 * a * c0 * x != y | b = z.  [para(12(a,1),40(a,1))].

given #457 (F,wt=29): 755 x * d * x * c * a0 != y | d * x * d * x * d * x != y | x * d = b0.  [para(4(a,1),370(b,1)),flip(c)].

given #458 (F,wt=29): 756 x * y * z * c * a0 != u | x * y * z * c * a0 * v != u | b0 * v = b0.  [para(22(a,1),370(b,1,2,2,2)),flip(c)].

given #459 (T,wt=29): 762 c * a0 * c * a0 != x | a0 * c * a0 * c * a0 * c != x | b0 * c * a0 = b0.  [para(4(a,1),373(b,1))].

given #460 (T,wt=29): 765 x * y * z * u * a * c0 != v | x * y * z * u * b * w != v | d0 = w.  [para(1(a,1),391(a,1,2,2)),rewrite(1(12))].

given #461 (A,wt=33): 162 a * c0 * x * d0 * x * d0 * y != z | d0 * x * d0 * x * d0 * x * y != z | b = x.  [para(12(a,1),40(b,1))].

given #462 (F,wt=29): 767 x * b * x * a * c0 != y | b * x * b * x * b * x != y | x * b = d0.  [para(4(a,1),391(b,1)),flip(c)].

given #463 (F,wt=29): 768 x * y * z * a * c0 != u | x * y * z * a * a0 * v != u | b0 * v = d0.  [para(18(a,1),391(b,1,2,2,2)),flip(c)].

given #464 (T,wt=29): 769 x * y * z * a * c0 != u | x * y * z * a * c0 * v != u | d0 * v = d0.  [para(26(a,1),391(b,1,2,2,2)),flip(c)].

given #465 (T,wt=29): 774 a * a0 * a * c0 != x | a0 * a * a0 * a * a0 * a != x | b0 * a * a0 = d0.  [para(4(a,1),394(b,1))].

given #466 (A,wt=33): 164 x * a * a0 != y | x * z * b * z * b * z * b != y | z * b * z * b * z = b0.  [para(4(a,1),46(b,1,2)),flip(c)].

given #467 (F,wt=29): 778 a * c0 * a * c0 != x | c0 * a * c0 * a * c0 * a != x | d0 * a * c0 = d0.  [para(4(a,1),395(b,1))].

given #468 (F,wt=29): 781 a * a0 != x | y * z * u * v * w * b0 != x | y * z * u * v * w = b.  [para(1(a,1),405(b,1,2,2,2))].

given #469 (T,wt=29): 782 c * a0 != x | y * z * u * v * w * b0 != x | y * z * u * v * w = d.  [para(1(a,1),424(b,1,2,2,2))].

given #470 (T,wt=29): 783 x * y * z * u * a * a0 != v | w * b0 != v | x * y * z * u * b = w.  [para(1(a,1),425(a,1,2,2)),rewrite(1(14))].

given #471 (A,wt=33): 169 x * a * a0 != y | b * x * b * x * b * x * z != y | x * b * x * b * z = b0.  [para(12(a,1),46(b,1)),flip(c)].

given #472 (F,wt=29): 784 x * y * z * a * a0 != u | v * w * b0 != u | x * y * z * b = v * w.  [para(1(a,1),425(b,1))].

given #473 (F,wt=29): 787 x * y * a * a0 != z | u * v * w * b0 != z | x * y * b = u * v * w.  [para(1(a,1),426(b,1,2))].

given #474 (T,wt=29): 788 x * a * a0 != y | z * u * v * w * b0 != y | z * u * v * w = x * b.  [para(1(a,1),427(b,1,2,2))].

given #475 (T,wt=29): 789 x * y * z * u * c * a0 != v | w * b0 != v | x * y * z * u * d = w.  [para(1(a,1),433(a,1,2,2)),rewrite(1(14))].

given #476 (A,wt=33): 171 x * c * a0 != y | x * z * d * z * d * z * d != y | z * d * z * d * z = b0.  [para(4(a,1),47(b,1,2)),flip(c)].

given #477 (F,wt=29): 790 x * y * z * c * a0 != u | v * w * b0 != u | x * y * z * d = v * w.  [para(1(a,1),433(b,1))].

given #478 (F,wt=29): 791 x * y * c * a0 != z | u * v * w * b0 != z | x * y * d = u * v * w.  [para(1(a,1),434(b,1,2))].

given #479 (T,wt=29): 794 x * c * a0 != y | z * u * v * w * b0 != y | z * u * v * w = x * d.  [para(1(a,1),435(b,1,2,2))].

given #480 (T,wt=29): 795 x * y * z * u * a * c0 != v | w * d0 != v | x * y * z * u * b = w.  [para(1(a,1),440(a,1,2,2)),rewrite(1(14))].

given #481 (A,wt=33): 174 x * c * a0 != y | d * x * d * x * d * x * z != y | x * d * x * d * z = b0.  [para(12(a,1),47(b,1)),flip(c)].

given #482 (F,wt=29): 796 x * y * z * a * c0 != u | v * w * d0 != u | x * y * z * b = v * w.  [para(1(a,1),440(b,1))].

given #483 (F,wt=29): 797 x * y * a * c0 != z | u * v * w * d0 != z | x * y * b = u * v * w.  [para(1(a,1),441(b,1,2))].

given #484 (T,wt=29): 798 x * a * c0 != y | z * u * v * w * d0 != y | z * u * v * w = x * b.  [para(1(a,1),442(b,1,2,2))].

given #485 (T,wt=29): 799 x * y * z * u * v * d0 != w | a * c0 != w | x * y * z * u * v = b.  [para(1(a,1),447(a,1,2,2,2))].

given #486 (A,wt=35): 176 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 #487 (F,wt=29): 800 x * y * z * u * a * a0 != v | x * y * z * u * a * c0 != v | d0 = b0.  [para(1(a,1),467(a,1,2,2)),rewrite(1(13))].

given #488 (F,wt=29): 801 a * a0 != x | y * z * u * v * a * a0 != x | y * z * u * v * b = b.  [para(1(a,1),468(b,1,2,2)),rewrite(1(15))].

given #489 (T,wt=29): 802 a * a0 != x | y * z * u * v * c * a0 != x | y * z * u * v * d = b.  [para(1(a,1),469(b,1,2,2)),rewrite(1(15))].

given #490 (T,wt=29): 804 c * a0 != x | y * z * u * v * a * a0 != x | y * z * u * v * b = d.  [para(1(a,1),470(b,1,2,2)),rewrite(1(15))].

given #491 (A,wt=35): 177 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 #492 (F,wt=29): 805 c * a0 != x | y * z * u * v * c * a0 != x | y * z * u * v * d = d.  [para(1(a,1),473(b,1,2,2)),rewrite(1(15))].

given #493 (F,wt=29): 806 x * y * z * u * a * c0 != v | a * c0 != v | x * y * z * u * b = b.  [para(1(a,1),474(a,1,2,2)),rewrite(1(15))].

given #494 (T,wt=29): 807 x * y * z * a * a0 * u != v | a * a0 * u != v | x * y * z * b = b.  [para(1(a,1),475(a,1,2)),rewrite(1(16))].

given #495 (T,wt=29): 809 a0 * a * a0 * a * a0 * a != x | a * a0 * a * a0 != x | a * a0 * b = b.  [para(4(a,1),475(a,1))].

given #496 (A,wt=33): 179 x * a * c0 != y | x * z * b * z * b * z * b != y | z * b * z * b * z = d0.  [para(4(a,1),48(b,1,2)),flip(c)].

given #497 (F,wt=29): 813 x * y * z * a * a0 * u != v | c * a0 * u != v | x * y * z * b = d.  [para(1(a,1),481(a,1,2)),rewrite(1(16))].

given #498 (F,wt=29): 815 a0 * a * a0 * a * a0 * a != x | c * a0 * a * a0 != x | a * a0 * b = d.  [para(4(a,1),481(a,1))].

given #499 (T,wt=29): 818 x * y * z * c * a0 * u != v | a * a0 * u != v | x * y * z * d = b.  [para(1(a,1),488(a,1,2)),rewrite(1(16))].

NOTE: Back_subsumption disabled, ratio of kept to back_subsumed is 86 (0.00 of 8.10 sec).

given #500 (T,wt=29): 820 a0 * c * a0 * c * a0 * c != x | a * a0 * c * a0 != x | c * a0 * d = b.  [para(4(a,1),488(a,1))].

given #501 (A,wt=33): 183 x * a * c0 != y | b * x * b * x * b * x * z != y | x * b * x * b * z = d0.  [para(12(a,1),48(b,1)),flip(c)].

given #502 (F,wt=29): 823 x * y * z * c * a0 * u != v | c * a0 * u != v | x * y * z * d = d.  [para(1(a,1),494(a,1,2)),rewrite(1(16))].

given #503 (F,wt=29): 825 a0 * c * a0 * c * a0 * c != x | c * a0 * c * a0 != x | c * a0 * d = d.  [para(4(a,1),494(a,1))].

given #504 (T,wt=29): 828 x * y * z * a * c0 * u != v | a * c0 * u != v | x * y * z * b = b.  [para(1(a,1),500(a,1,2)),rewrite(1(16))].

given #505 (T,wt=29): 830 c0 * a * c0 * a * c0 * a != x | a * c0 * a * c0 != x | a * c0 * b = b.  [para(4(a,1),500(a,1))].

given #506 (A,wt=33): 184 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 #507 (F,wt=29): 833 x * y * z * a * a0 != u | v * a * a0 != u | x * y * z * b = v * b.  [para(1(a,1),506(a,1,2)),rewrite(1(15))].

given #508 (F,wt=29): 834 x * y * a * a0 != z | u * v * a * a0 != z | x * y * b = u * v * b.  [para(1(a,1),506(b,1)),rewrite(1(18))].

given #509 (T,wt=29): 835 x * y * z * a * a0 != u | v * c * a0 != u | x * y * z * b = v * d.  [para(1(a,1),508(a,1,2)),rewrite(1(15))].

given #510 (T,wt=29): 836 x * y * a * a0 != z | u * v * c * a0 != z | u * v * d = x * y * b.  [para(1(a,1),508(b,1)),rewrite(1(18)),flip(c)].

given #511 (A,wt=33): 186 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 #512 (F,wt=29): 837 x * a * a0 != y | z * u * v * c * a0 != y | z * u * v * d = x * b.  [para(1(a,1),509(b,1,2)),rewrite(1(15))].

given #513 (F,wt=29): 838 x * y * z * a * a0 != u | a * a0 * b0 != u | a * a0 = x * y * z * b.  [para(1(a,1),510(a,1,2)),rewrite(1(19))].

given #514 (T,wt=29): 840 x * y * z * a * a0 != u | c * a0 * b0 != u | c * a0 = x * y * z * b.  [para(1(a,1),511(a,1,2)),rewrite(1(19))].

given #515 (T,wt=29): 841 x * y * z * a * a0 != u | a * c0 * b0 != u | a * c0 = x * y * z * b.  [para(1(a,1),512(a,1,2)),rewrite(1(19))].

given #516 (A,wt=33): 187 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 #517 (F,wt=29): 842 x * y * z * c * a0 != u | v * c * a0 != u | x * y * z * d = v * d.  [para(1(a,1),514(a,1,2)),rewrite(1(15))].

given #518 (F,wt=29): 843 x * y * c * a0 != z | u * v * c * a0 != z | x * y * d = u * v * d.  [para(1(a,1),514(b,1)),rewrite(1(18))].

given #519 (T,wt=29): 844 x * y * z * c * a0 != u | a * a0 * b0 != u | a * a0 = x * y * z * d.  [para(1(a,1),515(a,1,2)),rewrite(1(19))].

given #520 (T,wt=29): 845 x * y * z * c * a0 != u | c * a0 * b0 != u | c * a0 = x * y * z * d.  [para(1(a,1),516(a,1,2)),rewrite(1(19))].

given #521 (A,wt=33): 189 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 #522 (F,wt=29): 846 x * y * z * c * a0 != u | a * c0 * b0 != u | a * c0 = x * y * z * d.  [para(1(a,1),517(a,1,2)),rewrite(1(19))].

given #523 (F,wt=29): 847 x * y * z * a * c0 != u | v * a * c0 != u | x * y * z * b = v * b.  [para(1(a,1),521(a,1,2)),rewrite(1(15))].

given #524 (T,wt=29): 848 x * y * a * c0 != z | u * v * a * c0 != z | x * y * b = u * v * b.  [para(1(a,1),521(b,1)),rewrite(1(18))].

given #525 (T,wt=29): 849 x * y * z * a * c0 != u | a * a0 * d0 != u | a * a0 = x * y * z * b.  [para(1(a,1),522(a,1,2)),rewrite(1(19))].

given #526 (A,wt=31): 194 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 #527 (F,wt=27): 2208 d0 * d0 * x * d0 * x * d0 * x = x * d0 * x * d0 * x * d0 * d0.  [hyper(39,a,194,a,b,135,a(flip))].

given #528 (F,wt=27): 2209 b0 * b0 * x * b0 * x * b0 * x = x * b0 * x * b0 * x * b0 * b0.  [hyper(34,a,194,a,b,132,a)].

given #529 (T,wt=29): 850 x * y * z * a * c0 != u | c * a0 * d0 != u | c * a0 = x * y * z * b.  [para(1(a,1),523(a,1,2)),rewrite(1(19))].

given #530 (T,wt=29): 851 x * y * z * a * c0 != u | a * c0 * d0 != u | a * c0 = x * y * z * b.  [para(1(a,1),524(a,1,2)),rewrite(1(19))].

given #531 (A,wt=33): 195 x * y * z * y * z * y * z != u | x * v != u | z * y * z * y * z * y = v.  [para(14(a,1),2(a,1))].

given #532 (F,wt=29): 852 x * y * z * u * v != w | a * a0 * v != w | a * a0 = x * y * z * u.  [para(1(a,1),652(a,1,2,2))].

given #533 (F,wt=29): 854 x * y * a * a0 * z != u | a * a0 * b0 * z != u | a * a0 = x * y * b.  [para(18(a,1),652(a,1,2,2))].

given #534 (T,wt=29): 855 x * y * c * a0 * z != u | a * a0 * b0 * z != u | a * a0 = x * y * d.  [para(22(a,1),652(a,1,2,2))].

given #535 (T,wt=29): 856 x * y * a * c0 * z != u | a * a0 * d0 * z != u | a * a0 = x * y * b.  [para(26(a,1),652(a,1,2,2))].

given #536 (A,wt=33): 196 x * y * z * y * z * y * z != u | v * z * y * z * y * z * y != u | x = v.  [para(14(a,1),3(a,1))].

given #537 (F,wt=29): 857 x * y * z * u * v != w | c * a0 * v != w | c * a0 = x * y * z * u.  [para(1(a,1),655(a,1,2,2))].

given #538 (F,wt=29): 859 x * y * a * a0 * z != u | c * a0 * b0 * z != u | c * a0 = x * y * b.  [para(18(a,1),655(a,1,2,2))].

given #539 (T,wt=29): 860 x * y * c * a0 * z != u | c * a0 * b0 * z != u | c * a0 = x * y * d.  [para(22(a,1),655(a,1,2,2))].

given #540 (T,wt=29): 861 x * y * a * c0 * z != u | c * a0 * d0 * z != u | c * a0 = x * y * b.  [para(26(a,1),655(a,1,2,2))].

given #541 (A,wt=33): 197 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 #542 (F,wt=29): 863 x * y * z * u * v != w | a * c0 * v != w | a * c0 = x * y * z * u.  [para(1(a,1),658(a,1,2,2))].

given #543 (F,wt=29): 865 x * y * a * a0 * z != u | a * c0 * b0 * z != u | a * c0 = x * y * b.  [para(18(a,1),658(a,1,2,2))].

given #544 (T,wt=29): 866 x * y * c * a0 * z != u | a * c0 * b0 * z != u | a * c0 = x * y * d.  [para(22(a,1),658(a,1,2,2))].

given #545 (T,wt=29): 867 x * y * a * c0 * z != u | a * c0 * d0 * z != u | a * c0 = x * y * b.  [para(26(a,1),658(a,1,2,2))].

given #546 (A,wt=33): 198 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 #547 (F,wt=29): 868 x * y * a * a0 * z != u | v * a * a0 * z != u | x * y * b = v * b.  [para(1(a,1),710(a,1)),rewrite(1(16))].

given #548 (F,wt=29): 871 x * y * a * a0 * z != u | v * c * a0 * z != u | x * y * b = v * d.  [para(1(a,1),712(a,1)),rewrite(1(18)),flip(c)].

given #549 (T,wt=29): 872 x * a * a0 * y != z | u * v * c * a0 * y != z | u * v * d = x * b.  [para(1(a,1),712(b,1)),rewrite(1(16))].

given #550 (T,wt=29): 879 x * y * c * a0 * z != u | v * c * a0 * z != u | x * y * d = v * d.  [para(1(a,1),720(a,1)),rewrite(1(16))].

given #551 (A,wt=33): 199 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 #552 (F,wt=29): 884 x * y * a * c0 * z != u | v * a * c0 * z != u | x * y * b = v * b.  [para(1(a,1),732(a,1)),rewrite(1(16))].

given #553 (F,wt=29): 1564 x * a * a0 != y | x * b * x * b * x * b != y | x * b * x * b = b0.  [para(4(a,1),165(b,1))].

given #554 (T,wt=29): 1565 x * c * a0 != y | x * d * x * d * x * d != y | x * d * x * d = b0.  [para(4(a,1),172(b,1))].

given #555 (T,wt=29): 1566 b0 * c * a0 != x | c * a0 * c * a0 * c * a0 != x | b0 * c * a0 * d = b0.  [para(6(a,1),172(b,1,2,2,2,2)),rewrite(22(15),22(17),22(24))].

given #556 (A,wt=33): 200 c * a0 != x | c * y * a0 * y * a0 * y * a0 != x | b0 * y * a0 * y * a0 * y = b0.  [para(4(a,1),59(b,1,2))].

given #557 (F,wt=29): 1567 x * a * c0 != y | x * b * x * b * x * b != y | x * b * x * b = d0.  [para(4(a,1),180(b,1))].

given #558 (F,wt=29): 1568 a0 * a * a0 * a * a0 * a != x | b0 * y != x | a * a0 * a * a0 * b = y.  [para(4(a,1),210(a,1))].

given #559 (T,wt=29): 1570 c0 * a * c0 * a * c0 * a != x | d0 * y != x | a * c0 * a * c0 * b = y.  [para(4(a,1),212(a,1))].

given #560 (T,wt=29): 1571 a0 * a * a0 * a * a0 * a != x | y * a * a0 * a * a0 * b != x | b0 = y.  [para(4(a,1),223(a,1))].

given #561 (A,wt=33): 202 c * a0 != x | a0 * c * a0 * c * a0 * c * y != x | b0 * c * a0 * c * a0 * y = b0.  [para(12(a,1),59(b,1))].

given #562 (F,wt=29): 1572 c0 * a * c0 * a * c0 * a != x | y * a * c0 * a * c0 * b != x | d0 = y.  [para(4(a,1),225(a,1))].

given #563 (F,wt=29): 1573 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 #564 (T,wt=29): 1574 a0 * a * a0 * a * a0 * a != x | b0 * a * y != x | a0 * a * a0 * b = y.  [para(4(a,1),248(a,1))].

given #565 (T,wt=29): 1575 a0 * a * a0 * a * a0 * a != x | y * a0 * a * a0 * b != x | b0 * a = y.  [para(4(a,1),250(a,1))].

given #566 (A,wt=33): 217 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 #567 (F,wt=29): 1576 a0 * a * a0 * a * a0 * a != x | b0 * a * a0 * y != x | a * a0 * b = y.  [para(4(a,1),255(a,1))].

given #568 (F,wt=29): 1588 a0 * a * a0 * a * a0 * a != x | b0 * b * y != x | b0 * a * a0 * b = y.  [para(4(a,1),262(a,1))].

given #569 (T,wt=29): 1589 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 #570 (T,wt=29): 1590 a0 * a * a0 * a * a0 * a != x | y * a * a0 * b != x | b0 * a * a0 = y.  [para(4(a,1),285(a,1))].

given #571 (A,wt=33): 219 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 #572 (F,wt=29): 1591 c0 * a * c0 * a * c0 * a != x | d0 * a * y != x | c0 * a * c0 * b = y.  [para(4(a,1),288(a,1))].

given #573 (F,wt=29): 1592 c0 * a * c0 * a * c0 * a != x | y * c0 * a * c0 * b != x | d0 * a = y.  [para(4(a,1),290(a,1))].

given #574 (T,wt=29): 1611 c0 * a * c0 * a * c0 * a != x | d0 * a * c0 * y != x | a * c0 * b = y.  [para(4(a,1),293(a,1))].

given #575 (T,wt=29): 1612 c0 * a * c0 * a * c0 * a != x | d0 * b * y != x | d0 * a * c0 * b = y.  [para(4(a,1),294(a,1))].

given #576 (A,wt=33): 220 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 #577 (F,wt=29): 1613 c0 * a * c0 * a * c0 * a != x | y * a * c0 * b != x | d0 * a * c0 = y.  [para(4(a,1),296(a,1))].

given #578 (F,wt=29): 1614 a0 * a * a0 * a * a0 * a != x | y * b0 * a * a0 * b != x | b0 * b = y.  [para(4(a,1),310(a,1))].

given #579 (T,wt=29): 1615 c * a0 * c * a0 * c * a0 != x | a * a0 * c * a0 * d != x | b0 * d = b.  [para(6(a,1),312(a,1,2,2,2,2)),rewrite(22(9),22(11),22(19))].

given #580 (T,wt=29): 1616 c * a0 * c * a0 * c * a0 != x | c * a0 * c * a0 * d != x | b0 * d = d.  [para(6(a,1),322(a,1,2,2,2,2)),rewrite(22(9),22(11),22(19))].

given #581 (A,wt=33): 222 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 #582 (F,wt=29): 1626 c0 * a * c0 * a * c0 * a != x | y * d0 * a * c0 * b != x | d0 * b = y.  [para(4(a,1),330(a,1))].

given #583 (F,wt=29): 1627 b * x * a * a0 != y | b * x * b * x * b * x != y | x * b * x = b0.  [para(4(a,1),356(b,1))].

given #584 (T,wt=29): 1646 b0 * a * a0 != x | a0 * a * a0 * a * a0 * a != x | b0 * a * a0 * b = b0.  [para(4(a,1),365(b,1))].

given #585 (T,wt=29): 1647 d0 * a * a0 != x | c0 * a * c0 * a * c0 * a != x | d0 * a * c0 * b = b0.  [para(4(a,1),369(b,1))].

given #586 (A,wt=33): 226 a * x * a0 * x * a0 * x * a0 != y | c * a0 * x * a0 * x * a0 * x != y | d = b.  [para(4(a,1),108(a,1,2))].

given #587 (F,wt=29): 1653 d * x * c * a0 != y | d * x * d * x * d * x != y | x * d * x = b0.  [para(4(a,1),372(b,1))].

given #588 (F,wt=29): 1654 b * x * a * c0 != y | b * x * b * x * b * x != y | x * b * x = d0.  [para(4(a,1),393(b,1))].

given #589 (T,wt=29): 1656 b0 * a * c0 != x | a0 * a * a0 * a * a0 * a != x | b0 * a * a0 * b = d0.  [para(4(a,1),400(b,1))].

given #590 (T,wt=29): 1657 d0 * a * c0 != x | c0 * a * c0 * a * c0 * a != x | d0 * a * c0 * b = d0.  [para(4(a,1),404(b,1))].

given #591 (A,wt=33): 228 a * a0 * x * a0 * x * a0 * x != y | c * x * a0 * x * a0 * x * a0 != y | d = b.  [para(4(a,1),108(b,1,2))].

given #592 (F,wt=29): 1663 c * a0 * c * a0 * c * a0 != x | b0 * c * y != x | a0 * c * a0 * d = y.  [para(4(a,1),411(a,1))].

given #593 (F,wt=29): 1664 c * a0 * c * a0 * c * a0 != x | y * a0 * c * a0 * d != x | b0 * c = y.  [para(4(a,1),413(a,1))].

given #594 (T,wt=29): 1679 a0 * a * a0 * a * a0 * a != x | a * a0 * a * a0 * b != x | b0 * b = b.  [para(4(a,1),480(a,1))].

given #595 (T,wt=29): 1680 a0 * a * a0 * a * a0 * a != x | c * a0 * a * a0 * b != x | b0 * b = d.  [para(4(a,1),486(a,1))].

given #596 (A,wt=33): 230 a0 * a * a0 * a * a0 * a * x != y | c * a0 * a * a0 * a * a0 * x != y | d = b.  [para(12(a,1),108(a,1))].

given #597 (F,wt=29): 1683 c0 * a * c0 * a * c0 * a != x | a * c0 * a * c0 * b != x | d0 * b = b.  [para(4(a,1),505(a,1))].

given #598 (F,wt=29): 1694 b0 * d0 * b0 * d0 * b0 * d0 != x | c0 * b0 * d0 * b0 * d0 * b0 != x | b0 = a0.  [para(4(a,1),553(a,1))].

given #599 (T,wt=29): 1697 x * y * x * y * x * y != z | y * x * y * x * y * u != z | x = u.  [para(4(a,1),564(a,1))].

given #600 (T,wt=29): 1698 x * y * x * y * x * z != u | y * x * y * x * y * x != u | z = y.  [para(4(a,1),564(b,1))].

given #601 (A,wt=33): 231 a * a0 * c * a0 * c * a0 * x != y | a0 * c * a0 * c * a0 * c * x != y | d = b.  [para(12(a,1),108(b,1))].

given #602 (F,wt=29): 1704 a * a0 * a * a0 * a * a0 != x | b0 * a * a0 * a * a0 * y != x | b = y.  [para(21(a,1),564(a,1))].

given #603 (F,wt=29): 1706 a * c0 * a * c0 * a * c0 != x | d0 * a * c0 * a * c0 * y != x | b = y.  [para(29(a,1),564(a,1))].

given #604 (T,wt=29): 1710 a0 * c * a0 * c * a0 * c != x | b0 * c * a0 * c * a0 * y != x | d = y.  [para(38(a,1),564(a,1))].

given #605 (T,wt=29): 1714 b0 * c0 * a0 * c0 * a0 * c0 != x | d0 * a0 * c0 * a0 * c0 * y != x | a0 = y.  [para(193(a,1),564(a,1))].

given #606 (A,wt=33): 239 x * y * z * y * z * y * z != u | x * z * y * v != u | z * y * z * y = v.  [para(4(a,1),43(a,1,2))].

given #607 (F,wt=29): 1716 c0 * b0 * d0 * b0 * d0 * b0 != x | a0 * d0 * b0 * d0 * b0 * y != x | d0 = y.  [para(336(a,1),564(a,1))].

given #608 (F,wt=29): 1751 a * a0 * a * a0 * a * a0 != x | b0 * a * a0 * b * y != x | b0 * b = y.  [para(5(a,1),566(a,1,2,2,2,2)),rewrite(18(9),18(11),18(19))].

given #609 (T,wt=29): 1752 c * a0 * c * a0 * c * a0 != x | b0 * c * a0 * d * y != x | b0 * d = y.  [para(6(a,1),566(a,1,2,2,2,2)),rewrite(22(9),22(11),22(19))].

given #610 (T,wt=29): 1753 a * c0 * a * c0 * a * c0 != x | d0 * a * c0 * b * y != x | d0 * b = y.  [para(7(a,1),566(a,1,2,2,2,2)),rewrite(26(9),26(11),26(19))].

given #611 (A,wt=33): 244 x * y * x * y * x * y * z != u | y * x * y * v != u | x * y * x * z = v.  [para(12(a,1),43(a,1))].

given #612 (F,wt=29): 1758 a * a0 * a * a0 * a * a0 != x | a0 * a * a0 * b * y != x | b0 * a = y.  [para(4(a,1),567(a,1))].

given #613 (F,wt=29): 1770 c * a0 * c * a0 * c * a0 != x | a0 * c * a0 * d * y != x | b0 * c = y.  [para(4(a,1),568(a,1))].

given #614 (T,wt=29): 1773 a0 * c * a0 * c * a0 * c != x | b0 * c * a0 * d * y != x | b0 * d = y.  [para(38(a,1),568(a,1))].

given #615 (T,wt=29): 1780 a * c0 * a * c0 * a * c0 != x | c0 * a * c0 * b * y != x | d0 * a = y.  [para(4(a,1),569(a,1))].

given #616 (A,wt=33): 247 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 #617 (F,wt=29): 1789 a0 * a * a0 * a * a0 * a != x | b0 * a * a0 * a * y != x | a0 * b = y.  [para(4(a,1),572(a,1))].

given #618 (F,wt=29): 1790 c0 * a * c0 * a * c0 * a != x | d0 * a * c0 * a * y != x | c0 * b = y.  [para(4(a,1),574(a,1))].

given #619 (T,wt=29): 1791 c * a0 * c * a0 * c * a0 != x | b0 * c * a0 * c * y != x | a0 * d = y.  [para(4(a,1),578(a,1))].

given #620 (T,wt=29): 1802 x * y * x * y * x * y != z | u * x != z | y * x * y * x * y = u.  [para(4(a,1),623(a,1))].

given #621 (A,wt=33): 249 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 #622 (F,wt=29): 1811 a * a0 * a * a0 * a * a0 != x | y * b != x | b0 * a * a0 * a * a0 = y.  [para(21(a,1),623(a,1))].

given #623 (F,wt=29): 1813 a * c0 * a * c0 * a * c0 != x | y * b != x | d0 * a * c0 * a * c0 = y.  [para(29(a,1),623(a,1))].

given #624 (T,wt=29): 1817 a0 * c * a0 * c * a0 * c != x | y * d != x | b0 * c * a0 * c * a0 = y.  [para(38(a,1),623(a,1))].

given #625 (T,wt=29): 1821 b0 * c0 * a0 * c0 * a0 * c0 != x | y * a0 != x | d0 * a0 * c0 * a0 * c0 = y.  [para(193(a,1),623(a,1))].

given #626 (A,wt=33): 251 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 #627 (F,wt=29): 1823 c0 * b0 * d0 * b0 * d0 * b0 != x | y * d0 != x | a0 * d0 * b0 * d0 * b0 = y.  [para(336(a,1),623(a,1))].

given #628 (F,wt=29): 1870 a * a0 * a * a0 * a * a0 != x | y * b0 * b != x | b0 * a * a0 * b = y.  [para(5(a,1),626(a,1,2,2,2,2)),rewrite(18(9),18(11),18(23))].

given #629 (T,wt=29): 1871 c * a0 * c * a0 * c * a0 != x | y * b0 * d != x | b0 * c * a0 * d = y.  [para(6(a,1),626(a,1,2,2,2,2)),rewrite(22(9),22(11),22(23))].

given #630 (T,wt=29): 1872 a * c0 * a * c0 * a * c0 != x | y * d0 * b != x | d0 * a * c0 * b = y.  [para(7(a,1),626(a,1,2,2,2,2)),rewrite(26(9),26(11),26(23))].

given #631 (A,wt=33): 252 a * a0 * a * a0 * a * a0 * b != x | y * a * a0 * a * a0 * a * a0 != x | b = y.  [para(21(a,1),31(b,1,2))].

given #632 (F,wt=29): 1873 x * b0 * x * b0 * x * b0 != y | a * a0 * x != y | b0 * x * b0 * x = b.  [para(18(a,1),626(b,1))].

given #633 (F,wt=29): 1874 x * b0 * x * b0 * x * b0 != y | c * a0 * x != y | b0 * x * b0 * x = d.  [para(22(a,1),626(b,1))].

given #634 (T,wt=29): 1875 x * d0 * x * d0 * x * d0 != y | a * c0 * x != y | d0 * x * d0 * x = b.  [para(26(a,1),626(b,1))].

given #635 (T,wt=29): 1884 a * a0 * a * a0 * a * a0 != x | y * b0 * a != x | a0 * a * a0 * b = y.  [para(4(a,1),627(a,1))].

given #636 (A,wt=33): 253 c * a0 * a * a0 * a * a0 * b != x | y * a * a0 * a * a0 * a * a0 != x | d = y.  [para(21(a,1),35(b,1,2))].

given #637 (F,wt=29): 1897 c0 * b0 * d0 * b0 * d0 * b0 != x | a * a0 * d0 != x | a0 * d0 * b0 * d0 = b.  [para(336(a,1),628(a,1))].

given #638 (F,wt=29): 1905 c * a0 * c * a0 * c * a0 != x | y * b0 * c != x | a0 * c * a0 * d = y.  [para(4(a,1),629(a,1))].

given #639 (T,wt=29): 1907 a0 * c * a0 * c * a0 * c != x | y * b0 * d != x | b0 * c * a0 * d = y.  [para(38(a,1),629(a,1))].

given #640 (T,wt=29): 1917 c0 * b0 * d0 * b0 * d0 * b0 != x | c * a0 * d0 != x | a0 * d0 * b0 * d0 = d.  [para(336(a,1),630(a,1))].

given #641 (A,wt=33): 254 x * a * a0 * a * a0 * a * a0 != y | x * b0 * a * z != y | a0 * a * a0 * b = z.  [para(21(a,1),43(a,1,2))].

given #642 (F,wt=29): 1951 a * c0 * a * c0 * a * c0 != x | y * d0 * a != x | c0 * a * c0 * b = y.  [para(4(a,1),631(a,1))].

given #643 (F,wt=29): 1969 a0 * a * a0 * a * a0 * a != x | y * a0 * b != x | b0 * a * a0 * a = y.  [para(4(a,1),635(a,1))].

given #644 (T,wt=29): 1970 c0 * a * c0 * a * c0 * a != x | y * c0 * b != x | d0 * a * c0 * a = y.  [para(4(a,1),637(a,1))].

given #645 (T,wt=29): 1971 c * a0 * c * a0 * c * a0 != x | y * a0 * d != x | b0 * c * a0 * c = y.  [para(4(a,1),641(a,1))].

given #646 (A,wt=33): 256 x * a0 * a * a0 * a * a0 * a != y | x * b * z != y | b0 * a * a0 * a * a0 = z.  [para(4(a,1),49(a,1,2))].

given #647 (F,wt=29): 1983 a0 * a * a0 * a * a0 * a != x | a * a0 * a * a0 * b * y != x | b0 = y.  [para(4(a,1),735(a,1))].

given #648 (F,wt=29): 1985 b * x * b * x * a * a0 != y | x * b * x * b * x * b != y | b0 = x.  [para(4(a,1),735(b,1))].

given #649 (T,wt=29): 1997 x * b * x * a * a0 != y | x * b * x * b * x * b != y | x * b = b0.  [para(4(a,1),737(b,1))].

given #650 (T,wt=29): 1998 b0 * a * a0 * a * a0 != x | a * a0 * a * a0 * a * a0 != x | b0 * b = b0.  [para(5(a,1),737(b,1,2,2,2,2)),rewrite(18(8),18(19),18(21))].

given #651 (A,wt=33): 258 x * a * a0 * y != z | b * x * b * x * b * x != z | b0 * y = x * b * x * b.  [para(4(a,1),49(b,1))].

given #652 (F,wt=29): 1999 d0 * a * c0 * a * a0 != x | a * c0 * a * c0 * a * c0 != x | d0 * b = b0.  [para(7(a,1),737(b,1,2,2,2,2)),rewrite(26(8),26(19),26(21))].

given #653 (F,wt=29): 2001 a0 * a * a0 * a * a0 != x | a * a0 * a * a0 * a * a0 != x | b0 * a = b0.  [para(4(a,1),738(b,1))].

given #654 (T,wt=29): 2008 c0 * a * c0 * a * a0 != x | a * c0 * a * c0 * a * c0 != x | d0 * a = b0.  [para(4(a,1),739(b,1))].

given #655 (T,wt=29): 2017 a0 * c * a0 * c * a0 * c != x | c * a0 * c * a0 * d * y != x | b0 = y.  [para(4(a,1),753(a,1))].

given #656 (A,wt=33): 261 a * a0 * a * a0 * a * a0 * x != y | a0 * b * z != y | b0 * a * a0 * a * x = z.  [para(12(a,1),49(a,1))].

given #657 (F,wt=29): 2019 d * x * d * x * c * a0 != y | x * d * x * d * x * d != y | b0 = x.  [para(4(a,1),753(b,1))].

given #658 (F,wt=29): 2029 x * d * x * c * a0 != y | x * d * x * d * x * d != y | x * d = b0.  [para(4(a,1),755(b,1))].

given #659 (T,wt=29): 2030 b0 * c * a0 * c * a0 != x | c * a0 * c * a0 * c * a0 != x | b0 * d = b0.  [para(6(a,1),755(b,1,2,2,2,2)),rewrite(22(8),22(19),22(21))].

given #660 (T,wt=29): 2032 a0 * c * a0 * c * a0 != x | c * a0 * c * a0 * c * a0 != x | b0 * c = b0.  [para(4(a,1),756(b,1))].

given #661 (A,wt=33): 263 x * a0 * c * a0 * c * a0 * c != y | x * d * z != y | b0 * c * a0 * c * a0 = z.  [para(4(a,1),50(a,1,2))].

given #662 (F,wt=29): 2034 b0 * c * a0 * c * a0 != x | a0 * c * a0 * c * a0 * c != x | b0 * d = b0.  [para(38(a,1),756(b,1))].

given #663 (F,wt=29): 2040 c0 * a * c0 * a * c0 * a != x | a * c0 * a * c0 * b * y != x | d0 = y.  [para(4(a,1),765(a,1))].

given #664 (T,wt=29): 2042 b * x * b * x * a * c0 != y | x * b * x * b * x * b != y | d0 = x.  [para(4(a,1),765(b,1))].

given #665 (T,wt=29): 2054 x * b * x * a * c0 != y | x * b * x * b * x * b != y | x * b = d0.  [para(4(a,1),767(b,1))].

given #666 (A,wt=33): 265 x * c * a0 * y != z | d * x * d * x * d * x != z | b0 * y = x * d * x * d.  [para(4(a,1),50(b,1))].

given #667 (F,wt=29): 2055 b0 * a * a0 * a * c0 != x | a * a0 * a * a0 * a * a0 != x | b0 * b = d0.  [para(5(a,1),767(b,1,2,2,2,2)),rewrite(18(8),18(19),18(21))].

given #668 (F,wt=29): 2056 d0 * a * c0 * a * c0 != x | a * c0 * a * c0 * a * c0 != x | d0 * b = d0.  [para(7(a,1),767(b,1,2,2,2,2)),rewrite(26(8),26(19),26(21))].

given #669 (T,wt=29): 2058 a0 * a * a0 * a * c0 != x | a * a0 * a * a0 * a * a0 != x | b0 * a = d0.  [para(4(a,1),768(b,1))].

given #670 (T,wt=29): 2066 c0 * a * c0 * a * c0 != x | a * c0 * a * c0 * a * c0 != x | d0 * a = d0.  [para(4(a,1),769(b,1))].

given #671 (A,wt=33): 267 c * a0 * c * a0 * c * a0 * x != y | a0 * d * z != y | b0 * c * a0 * c * x = z.  [para(12(a,1),50(a,1))].

given #672 (F,wt=29): 2075 a * a0 != x | b0 * y * b0 * y * b0 * y != x | y * b0 * y * b0 * y = b.  [para(4(a,1),781(b,1))].

given #673 (F,wt=29): 2077 c * a0 != x | b0 * y * b0 * y * b0 * y != x | y * b0 * y * b0 * y = d.  [para(4(a,1),782(b,1))].

given #674 (T,wt=29): 2080 a0 * a * a0 * a * a0 * a != x | y * b0 != x | a * a0 * a * a0 * b = y.  [para(4(a,1),783(a,1))].

given #675 (T,wt=29): 2086 x * y * a * a0 != z | u * a * a0 * b0 != z | u * a * a0 = x * y * b.  [para(18(a,1),787(b,1,2)),rewrite(5(19)),flip(c)].

given #676 (A,wt=33): 268 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 #677 (F,wt=29): 2087 x * y * a * a0 != z | a * a0 * u * b0 != z | a * a0 * u = x * y * b.  [para(18(a,1),787(b,1)),rewrite(18(20)),flip(c)].

given #678 (F,wt=29): 2088 x * y * a * a0 != z | u * c * a0 * b0 != z | u * c * a0 = x * y * b.  [para(22(a,1),787(b,1,2)),rewrite(6(19)),flip(c)].

given #679 (T,wt=29): 2089 x * y * a * a0 != z | c * a0 * u * b0 != z | c * a0 * u = x * y * b.  [para(22(a,1),787(b,1)),rewrite(22(20)),flip(c)].

given #680 (T,wt=29): 2090 x * y * a * a0 != z | u * a * c0 * b0 != z | u * a * c0 = x * y * b.  [para(26(a,1),787(b,1,2)),rewrite(7(19)),flip(c)].

given #681 (A,wt=33): 270 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 #682 (F,wt=29): 2091 x * y * a * a0 != z | a * c0 * u * b0 != z | a * c0 * u = x * y * b.  [para(26(a,1),787(b,1)),rewrite(26(20)),flip(c)].

given #683 (F,wt=29): 2095 a0 * c * a0 * c * a0 * c != x | y * b0 != x | c * a0 * c * a0 * d = y.  [para(4(a,1),789(a,1))].

given #684 (T,wt=29): 2099 x * y * c * a0 != z | u * a * a0 * b0 != z | u * a * a0 = x * y * d.  [para(18(a,1),791(b,1,2)),rewrite(5(19)),flip(c)].

given #685 (T,wt=29): 2100 x * y * c * a0 != z | a * a0 * u * b0 != z | a * a0 * u = x * y * d.  [para(18(a,1),791(b,1)),rewrite(18(20)),flip(c)].

given #686 (A,wt=33): 272 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 #687 (F,wt=29): 2101 x * y * c * a0 != z | u * c * a0 * b0 != z | u * c * a0 = x * y * d.  [para(22(a,1),791(b,1,2)),rewrite(6(19)),flip(c)].

given #688 (F,wt=29): 2102 x * y * c * a0 != z | c * a0 * u * b0 != z | c * a0 * u = x * y * d.  [para(22(a,1),791(b,1)),rewrite(22(20)),flip(c)].

given #689 (T,wt=29): 2103 x * y * c * a0 != z | u * a * c0 * b0 != z | u * a * c0 = x * y * d.  [para(26(a,1),791(b,1,2)),rewrite(7(19)),flip(c)].

given #690 (T,wt=29): 2104 x * y * c * a0 != z | a * c0 * u * b0 != z | a * c0 * u = x * y * d.  [para(26(a,1),791(b,1)),rewrite(26(20)),flip(c)].

given #691 (A,wt=33): 275 x * y * z * y * z * y * z != u | v * z * y * z * y != u | x * z * y = v.  [para(4(a,1),61(a,1,2))].

given #692 (F,wt=29): 2108 c0 * a * c0 * a * c0 * a != x | y * d0 != x | a * c0 * a * c0 * b = y.  [para(4(a,1),795(a,1))].

given #693 (F,wt=29): 2113 x * y * a * c0 != z | u * a * a0 * d0 != z | u * a * a0 = x * y * b.  [para(18(a,1),797(b,1,2)),rewrite(5(19)),flip(c)].

given #694 (T,wt=29): 2114 x * y * a * c0 != z | a * a0 * u * d0 != z | a * a0 * u = x * y * b.  [para(18(a,1),797(b,1)),rewrite(18(20)),flip(c)].

given #695 (T,wt=29): 2115 x * y * a * c0 != z | u * c * a0 * d0 != z | u * c * a0 = x * y * b.  [para(22(a,1),797(b,1,2)),rewrite(6(19)),flip(c)].

given #696 (A,wt=33): 283 x * y * x * y * x * y * z != u | v * x * y * x * z != u | y * x * y = v.  [para(12(a,1),61(a,1))].

given #697 (F,wt=29): 2116 x * y * a * c0 != z | c * a0 * u * d0 != z | c * a0 * u = x * y * b.  [para(22(a,1),797(b,1)),rewrite(22(20)),flip(c)].

given #698 (F,wt=29): 2117 x * y * a * c0 != z | u * a * c0 * d0 != z | u * a * c0 = x * y * b.  [para(26(a,1),797(b,1,2)),rewrite(7(19)),flip(c)].

given #699 (T,wt=29): 2118 x * y * a * c0 != z | a * c0 * u * d0 != z | a * c0 * u = x * y * b.  [para(26(a,1),797(b,1)),rewrite(26(20)),flip(c)].

given #700 (T,wt=29): 2121 d0 * x * d0 * x * d0 * x != y | a * c0 != y | x * d0 * x * d0 * x = b.  [para(4(a,1),799(a,1))].

given #701 (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),61(a,1,2))].

given #702 (F,wt=29): 2122 c0 * b0 * d0 * b0 * d0 * b0 != x | a * c0 != x | a0 * d0 * b0 * d0 * b0 = b.  [para(336(a,1),799(a,1))].

given #703 (F,wt=29): 2124 a0 * a * a0 * a * a0 * a != x | a * a0 * a * a0 * a * c0 != x | d0 = b0.  [para(4(a,1),800(a,1))].

given #704 (T,wt=29): 2125 a * c0 * a * c0 * a * a0 != x | c0 * a * c0 * a * c0 * a != x | d0 = b0.  [para(4(a,1),800(b,1))].

given #705 (T,wt=29): 2127 a * a0 != x | a0 * a * a0 * a * a0 * a != x | a * a0 * a * a0 * b = b.  [para(4(a,1),801(b,1))].

given #706 (A,wt=33): 287 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 #707 (F,wt=29): 2129 a * a0 != x | a0 * c * a0 * c * a0 * c != x | c * a0 * c * a0 * d = b.  [para(4(a,1),802(b,1))].

given #708 (F,wt=29): 2131 c * a0 != x | a0 * a * a0 * a * a0 * a != x | a * a0 * a * a0 * b = d.  [para(4(a,1),804(b,1))].

given #709 (T,wt=29): 2133 c * a0 != x | a0 * c * a0 * c * a0 * c != x | c * a0 * c * a0 * d = d.  [para(4(a,1),805(b,1))].

given #710 (T,wt=29): 2135 c0 * a * c0 * a * c0 * a != x | a * c0 != x | a * c0 * a * c0 * b = b.  [para(4(a,1),806(a,1))].

given #711 (A,wt=33): 289 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 #712 (F,wt=29): 2138 a * a0 * a * a0 * a * a0 != x | a * a0 * a != x | a0 * a * a0 * b = b.  [para(4(a,1),807(a,1))].

given #713 (F,wt=29): 2140 a * a0 * a * a0 * a * a0 != x | a * a0 * b != x | b0 * a * a0 * b = b.  [para(21(a,1),807(a,1))].

given #714 (T,wt=29): 2149 a * a0 * a * a0 * a * a0 != x | c * a0 * a != x | a0 * a * a0 * b = d.  [para(4(a,1),813(a,1))].

given #715 (T,wt=29): 2151 a * a0 * a * a0 * a * a0 != x | c * a0 * b != x | b0 * a * a0 * b = d.  [para(21(a,1),813(a,1))].

given #716 (A,wt=33): 291 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 #717 (F,wt=29): 2159 c * a0 * c * a0 * c * a0 != x | a * a0 * c != x | a0 * c * a0 * d = b.  [para(4(a,1),818(a,1))].

given #718 (F,wt=29): 2161 a0 * c * a0 * c * a0 * c != x | a * a0 * d != x | b0 * c * a0 * d = b.  [para(38(a,1),818(a,1))].

given #719 (T,wt=29): 2172 c * a0 * c * a0 * c * a0 != x | c * a0 * c != x | a0 * c * a0 * d = d.  [para(4(a,1),823(a,1))].

given #720 (T,wt=29): 2174 a0 * c * a0 * c * a0 * c != x | c * a0 * d != x | b0 * c * a0 * d = d.  [para(38(a,1),823(a,1))].

given #721 (A,wt=33): 292 x * a * c0 * a * c0 * a * c0 != y | x * d0 * a * z != y | c0 * a * c0 * b = z.  [para(29(a,1),43(a,1,2))].

given #722 (F,wt=29): 2182 a * c0 * a * c0 * a * c0 != x | a * c0 * a != x | c0 * a * c0 * b = b.  [para(4(a,1),828(a,1))].

given #723 (F,wt=29): 2184 a * c0 * a * c0 * a * c0 != x | a * c0 * b != x | d0 * a * c0 * b = b.  [para(29(a,1),828(a,1))].

given #724 (T,wt=29): 2193 a * a0 * a * a0 != x | y * z * c * a0 != x | a * a0 * b = y * z * d.  [para(18(a,1),836(a,1)),rewrite(18(22)),flip(c)].

given #725 (T,wt=29): 2194 c * a0 * a * a0 != x | y * z * c * a0 != x | c * a0 * b = y * z * d.  [para(22(a,1),836(a,1)),rewrite(22(22)),flip(c)].

given #726 (A,wt=33): 295 x * a * c0 * a * c0 * a * c0 != y | z * c0 * a * c0 * b != y | x * d0 * a = z.  [para(29(a,1),61(a,1,2))].

given #727 (F,wt=29): 2195 a * c0 * a * a0 != x | y * z * c * a0 != x | a * c0 * b = y * z * d.  [para(26(a,1),836(a,1)),rewrite(26(22)),flip(c)].

given #728 (F,wt=29): 2295 c * a0 * c * a0 * c * a0 != x | b0 * c * a0 * c * a0 * y != x | d = y.  [para(6(a,1),1697(a,1,2,2,2,2)),rewrite(22(9),22(11),22(19),22(21))].

given #729 (T,wt=29): 2311 a0 * a * a0 * a * a0 * a != x | b0 * a * a0 * a * a0 * y != x | b = y.  [para(4(a,1),1704(a,1))].

given #730 (T,wt=29): 2315 c0 * a * c0 * a * c0 * a != x | d0 * a * c0 * a * c0 * y != x | b = y.  [para(4(a,1),1706(a,1))].

given #731 (A,wt=33): 297 x * y * x * y * x * y != z | u * v * y * x * y * x != z | y * x = u * v.  [para(4(a,1),62(a,1))].

given #732 (F,wt=29): 2326 a0 * a * a0 * a * a0 * a != x | b0 * a * a0 * b * y != x | b0 * b = y.  [para(4(a,1),1751(a,1))].

given #733 (F,wt=29): 2330 c0 * a * c0 * a * c0 * a != x | d0 * a * c0 * b * y != x | d0 * b = y.  [para(4(a,1),1753(a,1))].

given #734 (T,wt=29): 2344 c * a0 * c * a0 * c * a0 != x | y * d != x | b0 * c * a0 * c * a0 = y.  [para(6(a,1),1802(a,1,2,2,2,2)),rewrite(22(9),22(11),6(21),22(23))].

given #735 (T,wt=29): 2351 a0 * a * a0 * a * a0 * a != x | y * b != x | b0 * a * a0 * a * a0 = y.  [para(4(a,1),1811(a,1))].

given #736 (A,wt=33): 298 x * y * z * u * z * u != v | u * z * u * z * u * z != v | x * y = z * u.  [para(4(a,1),62(b,1))].

given #737 (F,wt=29): 2353 c0 * a * c0 * a * c0 * a != x | y * b != x | d0 * a * c0 * a * c0 = y.  [para(4(a,1),1813(a,1))].

given #738 (F,wt=29): 2358 a0 * a * a0 * a * a0 * a != x | y * b0 * b != x | b0 * a * a0 * b = y.  [para(4(a,1),1870(a,1))].

given #739 (T,wt=29): 2360 c * a0 * c * a0 * c * a0 != x | a * a0 * d != x | b0 * c * a0 * d = b.  [para(18(a,1),1871(b,1))].

given #740 (T,wt=29): 2361 c * a0 * c * a0 * c * a0 != x | c * a0 * d != x | b0 * c * a0 * d = d.  [para(22(a,1),1871(b,1))].

given #741 (A,wt=33): 302 a * a0 * a * a0 * a * a0 != x | y * z * a0 * a * a0 * b != x | b0 * a = y * z.  [para(21(a,1),62(a,1))].

given #742 (F,wt=29): 2363 c0 * a * c0 * a * c0 * a != x | y * d0 * b != x | d0 * a * c0 * b = y.  [para(4(a,1),1872(a,1))].

given #743 (F,wt=29): 2378 b0 * a * a0 * a * a0 != x | a0 * a * a0 * a * a0 * a != x | b0 * b = b0.  [para(4(a,1),1998(b,1))].

given #744 (T,wt=29): 2379 d0 * a * c0 * a * a0 != x | c0 * a * c0 * a * c0 * a != x | d0 * b = b0.  [para(4(a,1),1999(b,1))].

given #745 (T,wt=29): 2383 b0 * a * a0 * a * c0 != x | a0 * a * a0 * a * a0 * a != x | b0 * b = d0.  [para(4(a,1),2055(b,1))].

given #746 (A,wt=33): 303 a * c0 * a * c0 * a * c0 != x | y * z * c0 * a * c0 * b != x | d0 * a = y * z.  [para(29(a,1),62(a,1))].

given #747 (F,wt=29): 2384 d0 * a * c0 * a * c0 != x | c0 * a * c0 * a * c0 * a != x | d0 * b = d0.  [para(4(a,1),2056(b,1))].

given #748 (F,wt=29): 2420 a0 * a * a0 * a * a0 * a != x | a * a0 * b != x | b0 * a * a0 * b = b.  [para(4(a,1),2140(a,1))].

given #749 (T,wt=29): 2421 a0 * a * a0 * a * a0 * a != x | c * a0 * b != x | b0 * a * a0 * b = d.  [para(4(a,1),2151(a,1))].

given #750 (T,wt=29): 2426 c0 * a * c0 * a * c0 * a != x | a * c0 * b != x | d0 * a * c0 * b = b.  [para(4(a,1),2184(a,1))].

given #751 (A,wt=33): 304 x * a0 * a * a0 * a * a0 * a != y | z * b0 * a * a0 * a * a0 != y | x * b = z.  [para(4(a,1),70(a,1,2))].

given #752 (F,wt=31): 448 x * a * c0 * y * d0 * y * d0 * y = x * b * y * d0 * y * d0 * y * d0.  [para(42(a,1),1(a,2,2)),rewrite(1(11))].

given #753 (F,wt=31): 694 d0 * a0 * a0 * c0 * a0 * a0 * c0 * a0 = b0 * c0 * a0 * a0 * c0 * a0 * a0 * c0.  [hyper(103,a,xx,b,80,a)].

given #754 (T,wt=31): 695 d0 * a0 * c0 * c0 * a0 * c0 * c0 * a0 = b0 * c0 * c0 * a0 * c0 * c0 * a0 * c0.  [hyper(103,a,80,a,b,xx)].

given #755 (T,wt=31): 696 d0 * x * d0 * d0 * x * d0 * d0 * x = x * d0 * d0 * x * d0 * d0 * x * d0.  [hyper(39,a,26,a(flip),b,80,a)].

given #756 (A,wt=33): 306 x * a * a0 * y * b0 * y * b0 != z | b0 * y * b0 * y * b0 * y != z | x * b = y.  [para(4(a,1),70(b,1))].

given #757 (F,wt=31): 697 b0 * x * b0 * b0 * x * b0 * b0 * x = x * b0 * b0 * x * b0 * b0 * x * b0.  [hyper(34,a,22,a(flip),b,80,a)].

given #758 (F,wt=31): 803 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 #759 (T,wt=31): 812 a0 * d0 * b0 * b0 * d0 * b0 * b0 * d0 = c0 * b0 * b0 * d0 * b0 * b0 * d0 * b0.  [hyper(2,a,26,a(flip),b,88,a(flip)),flip(a)].

given #760 (T,wt=31): 839 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 #761 (A,wt=33): 309 a * a0 * a * a0 * a * a0 * x != y | z * b0 * a * a0 * a * x != y | a0 * b = z.  [para(12(a,1),70(a,1))].

given #762 (F,wt=31): 887 x * y * z * y * z * y * z * z = x * z * z * y * z * y * z * y.  [para(125(a,1),1(a,2,2)),rewrite(1(7))].

given #763 (F,wt=31): 894 a * a0 * x * b0 * x * b0 * x * x = b * x * x * b0 * x * b0 * x * b0.  [para(125(a,1),18(a,1,2)),flip(a)].

given #764 (T,wt=31): 897 a * a0 * a0 * x * a0 * x * a0 * x = a * x * a0 * x * a0 * x * a0 * a0.  [para(125(a,2),18(a,2,2)),rewrite(18(12))].

given #765 (T,wt=27): 2471 a0 * a0 * x * a0 * x * a0 * x = x * a0 * x * a0 * x * a0 * a0.  [hyper(2,a,xx,b,897,a),flip(a)].

given #766 (A,wt=33): 311 x * b0 * y * b0 * y * b0 * y != z | a * a0 * y * b0 * y * b0 != z | x * y = b.  [para(4(a,1),71(a,1,2))].

given #767 (F,wt=31): 898 c * a0 * x * b0 * x * b0 * x * x = d * x * x * b0 * x * b0 * x * b0.  [para(125(a,1),22(a,1,2)),flip(a)].

given #768 (F,wt=31): 900 c * a0 * a0 * x * a0 * x * a0 * x = c * x * a0 * x * a0 * x * a0 * a0.  [para(125(a,2),22(a,2,2)),rewrite(22(12))].

given #769 (T,wt=31): 901 a * c0 * x * d0 * x * d0 * x * x = b * x * x * d0 * x * d0 * x * d0.  [para(125(a,1),26(a,1,2)),flip(a)].

given #770 (T,wt=31): 903 a * c0 * d0 * x * d0 * x * d0 * x = b * x * d0 * x * d0 * x * d0 * d0.  [para(125(a,2),26(a,1,2)),flip(a)].

given #771 (A,wt=33): 313 x * y * b0 * a * a0 * a * a0 != z | a0 * a * a0 * a * a0 * a != z | x * y = b.  [para(4(a,1),71(b,1))].

given #772 (F,wt=31): 905 a * c0 * c0 * x * c0 * x * c0 * x = a * x * c0 * x * c0 * x * c0 * c0.  [para(125(a,2),26(a,2,2)),rewrite(26(12))].

given #773 (F,wt=27): 2489 c0 * c0 * x * c0 * x * c0 * x = x * c0 * x * c0 * x * c0 * c0.  [hyper(2,a,xx,b,905,a),flip(a)].

given #774 (T,wt=31): 921 x * y * x * y * x * y * y * y = y * y * y * x * y * x * y * x.  [para(125(a,1),12(a,1,2)),flip(a)].

given #775 (T,wt=31): 1019 x * b * y * b * y * b * y * b0 = x * y * b * y * b * y * a * a0.  [para(126(a,1),1(a,2,2)),rewrite(1(11))].

given #776 (A,wt=33): 315 x * b0 * x * b0 * x * b0 * y != z | a * a0 * x * b0 * x * y != z | b0 * x = b.  [para(12(a,1),71(a,1))].

given #777 (F,wt=31): 1029 a * c0 * a * c0 * a * c0 * a * a0 = b * a * c0 * a * c0 * a * c0 * b0.  [para(126(a,2),26(a,1,2)),rewrite(26(10),26(12),26(14),26(26),26(28)),flip(a)].

given #778 (F,wt=31): 1030 a * c0 * b * c0 * b * c0 * a * a0 = a * b * c0 * b * c0 * b * c0 * b0.  [para(126(a,2),26(a,2,2)),rewrite(26(15))].

given #779 (T,wt=27): 2517 c0 * b * c0 * b * c0 * a * a0 = b * c0 * b * c0 * b * c0 * b0.  [hyper(2,a,xx,b,1030,a),flip(a)].

given #780 (T,wt=31): 1041 b * x * b * x * b * x * x * b0 = x * x * b * x * b * x * a * a0.  [para(126(a,1),12(a,1,2)),flip(a)].

given #781 (A,wt=33): 316 x * a0 * c * a0 * c * a0 * c != y | z * b0 * c * a0 * c * a0 != y | x * d = z.  [para(4(a,1),72(a,1,2))].

given #782 (F,wt=31): 1043 b * b * x * b * x * b * x * b0 = x * b * x * b * x * b * a * a0.  [para(126(a,2),12(a,1,2))].

given #783 (F,wt=31): 1071 x * d * y * d * y * d * y * b0 = x * y * d * y * d * y * c * a0.  [para(127(a,1),1(a,2,2)),rewrite(1(11))].

given #784 (T,wt=27): 2520 d0 * d * d0 * d * d0 * c * a0 = d * d0 * d * d0 * d * d0 * b0.  [hyper(39,a,26,a(flip),b,1071,a)].

given #785 (T,wt=31): 1077 b * d * d0 * d * d0 * d * d0 * b0 = a * c0 * d * d0 * d * d0 * c * a0.  [para(127(a,2),26(a,1,2))].

given #786 (A,wt=33): 318 x * c * a0 * y * b0 * y * b0 != z | b0 * y * b0 * y * b0 * y != z | x * d = y.  [para(4(a,1),72(b,1))].

given #787 (F,wt=31): 1088 d * x * d * x * d * x * x * b0 = x * x * d * x * d * x * c * a0.  [para(127(a,1),12(a,1,2)),flip(a)].

given #788 (F,wt=31): 1090 d * d * x * d * x * d * x * b0 = x * d * x * d * x * d * c * a0.  [para(127(a,2),12(a,1,2))].

given #789 (T,wt=31): 1118 x * b * y * b * y * b * y * d0 = x * y * b * y * b * y * a * c0.  [para(128(a,1),1(a,2,2)),rewrite(1(11))].

given #790 (T,wt=31): 1128 a * c0 * b * c0 * b * c0 * a * c0 = a * b * c0 * b * c0 * b * c0 * d0.  [para(128(a,2),26(a,2,2)),rewrite(26(15))].

given #791 (A,wt=33): 320 c * a0 * c * a0 * c * a0 * x != y | z * b0 * c * a0 * c * x != y | a0 * d = z.  [para(12(a,1),72(a,1))].

given #792 (F,wt=27): 2528 c0 * b * c0 * b * c0 * a * c0 = b * c0 * b * c0 * b * c0 * d0.  [hyper(2,a,xx,b,1128,a),flip(a)].

given #793 (F,wt=31): 1139 b * x * b * x * b * x * x * d0 = x * x * b * x * b * x * a * c0.  [para(128(a,1),12(a,1,2)),flip(a)].

given #794 (T,wt=31): 1141 b * b * x * b * x * b * x * d0 = x * b * x * b * x * b * a * c0.  [para(128(a,2),12(a,1,2))].

given #795 (T,wt=31): 1171 b * a * a0 * a * a0 * a * a0 * x = a * a0 * a * a0 * a * a0 * b * x.  [para(130(a,1),18(a,1,2))].

given #796 (A,wt=33): 321 x * b0 * y * b0 * y * b0 * y != z | c * a0 * y * b0 * y * b0 != z | x * y = d.  [para(4(a,1),73(a,1,2))].

given #797 (F,wt=31): 1172 b0 * a * a0 * a * a0 * a * a0 * x = a * a0 * a * a0 * a * a0 * b0 * x.  [para(18(a,1),130(a,1,2,2,2,2,2))].

given #798 (F,wt=31): 1173 d * a * a0 * a * a0 * a * a0 * x = c * a0 * a * a0 * a * a0 * b * x.  [para(130(a,1),22(a,1,2))].

given #799 (T,wt=31): 1174 a * a0 * a * a0 * a * a0 * d0 * x = b0 * a * a0 * a * a0 * a * c0 * x.  [para(26(a,1),130(a,1,2,2,2,2,2)),flip(a)].

given #800 (T,wt=31): 1191 a * a0 * c * a0 * c * a0 * d * x = b * c * a0 * c * a0 * c * a0 * x.  [para(133(a,1),18(a,1,2)),flip(a)].

given #801 (A,wt=33): 323 x * y * b0 * c * a0 * c * a0 != z | a0 * c * a0 * c * a0 * c != z | x * y = d.  [para(4(a,1),73(b,1))].

given #802 (F,wt=31): 1192 d * c * a0 * c * a0 * c * a0 * x = c * a0 * c * a0 * c * a0 * d * x.  [para(133(a,1),22(a,1,2))].

given #803 (F,wt=31): 1193 c * a0 * c * a0 * c * a0 * b0 * x = b0 * c * a0 * c * a0 * c * a0 * x.  [para(22(a,1),133(a,1,2,2,2,2,2)),flip(a)].

given #804 (T,wt=31): 1207 c * c * c * a0 * c * a0 * c * a0 = c * a0 * c * a0 * c * a0 * c * c.  [para(125(a,1),133(a,2,2)),rewrite(133(15)),flip(a)].

given #805 (T,wt=27): 2558 c * c * a0 * c * a0 * c * a0 = a0 * c * a0 * c * a0 * c * c.  [hyper(120,a,12,a,b,1207,a),flip(a)].

given #806 (A,wt=33): 324 x * b0 * x * b0 * x * b0 * y != z | c * a0 * x * b0 * x * y != z | b0 * x = d.  [para(12(a,1),73(a,1))].

given #807 (F,wt=31): 1209 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 #808 (F,wt=31): 1213 b * a * c0 * a * c0 * a * c0 * d0 = a * a * c0 * a * c0 * a * c0 * c0.  [para(4(a,1),136(a,2,2,2)),rewrite(136(15),1127(15),904(29))].

given #809 (T,wt=31): 1214 d0 * a * c0 * a * c0 * a * a0 * x = a * c0 * a * c0 * a * c0 * b0 * x.  [para(18(a,1),136(a,1,2,2,2,2,2))].

given #810 (T,wt=31): 1215 a * c0 * a * c0 * a * c0 * b * x = b * a * c0 * a * c0 * a * c0 * x.  [para(136(a,1),26(a,1,2)),flip(a)].

given #811 (A,wt=33): 325 x * c0 * a * c0 * a * c0 * a != y | z * d0 * a * c0 * a * c0 != y | x * b = z.  [para(4(a,1),74(a,1,2))].

given #812 (F,wt=31): 1216 d0 * a * c0 * a * c0 * a * c0 * x = a * c0 * a * c0 * a * c0 * d0 * x.  [para(26(a,1),136(a,1,2,2,2,2,2))].

given #813 (F,wt=31): 1267 a * c0 * a * c0 * a * c0 * c0 * b = c0 * b * a * c0 * a * c0 * a * c0.  [para(286(a,1),12(a,1,2)),flip(a)].

given #814 (T,wt=31): 1308 d * a0 * c * a0 * c * a0 * c * x = c * a0 * c * a0 * c * a0 * d * x.  [para(409(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 #815 (T,wt=31): 1324 d0 * a0 * a0 * c0 * a0 * c0 * a0 * c0 = b0 * c0 * a0 * c0 * a0 * c0 * c0 * a0.  [para(4(a,1),526(a,1,2,2))].

given #816 (A,wt=33): 327 x * a * c0 * y * d0 * y * d0 != z | d0 * y * d0 * y * d0 * y != z | x * b = y.  [para(4(a,1),74(b,1))].

given #817 (F,wt=31): 1330 d0 * c0 * a0 * c0 * a0 * c0 * a0 * x = b0 * c0 * a0 * c0 * a0 * c0 * c0 * x.  [para(12(a,1),526(a,1,2))].

given #818 (F,wt=31): 1340 d0 * c0 * c0 * a0 * c0 * a0 * c0 * a0 = b0 * c0 * a0 * c0 * a0 * c0 * c0 * c0.  [para(125(a,1),526(a,1,2))].

given #819 (T,wt=31): 1345 a0 * d0 * d0 * b0 * d0 * b0 * d0 * b0 = c0 * b0 * d0 * b0 * d0 * b0 * b0 * d0.  [para(4(a,1),541(a,1,2,2))].

given #820 (T,wt=31): 1351 a0 * b0 * d0 * b0 * d0 * b0 * d0 * x = c0 * b0 * d0 * b0 * d0 * b0 * b0 * x.  [para(12(a,1),541(a,1,2))].

given #821 (A,wt=33): 329 a * c0 * a * c0 * a * c0 * x != y | z * d0 * a * c0 * a * x != y | c0 * b = z.  [para(12(a,1),74(a,1))].

given #822 (F,wt=31): 1365 c0 * b0 * d0 * b0 * d0 * b0 * b0 * b0 = a0 * b0 * b0 * d0 * b0 * d0 * b0 * d0.  [para(125(a,1),541(a,1,2)),flip(a)].

given #823 (F,wt=31): 1367 c0 * d0 * d0 * b0 * d0 * b0 * d0 * b0 = c0 * b0 * d0 * b0 * d0 * b0 * d0 * d0.  [para(125(a,1),541(a,2,2)),rewrite(541(15)),flip(a)].

given #824 (T,wt=31): 1385 a0 * a0 * a * a0 * a * a0 * a * x = a * a0 * a * a0 * a * a0 * a0 * x.  [para(896(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 #825 (T,wt=31): 1393 c * a0 * c * a0 * c * a0 * a0 * b0 = a0 * b0 * a0 * c * a0 * c * a0 * c.  [para(899(a,1),12(a,1,2)),flip(a)].

given #826 (A,wt=33): 331 x * d0 * y * d0 * y * d0 * y != z | a * c0 * y * d0 * y * d0 != z | x * y = b.  [para(4(a,1),75(a,1,2))].

given #827 (F,wt=31): 1422 c0 * c0 * a * c0 * a * c0 * a * x = a * c0 * a * c0 * a * c0 * c0 * x.  [para(904(a,1),1(a,1,1)),rewrite(1(14),1(13),1(12),1(11),1(10),1(9),1(27),1(26),1(25),1(24),1(23)),flip(a)].

given #828 (F,wt=31): 1423 d * b * d * b * d * a * a0 * x = b * d * b * d * b * c * a0 * x.  [para(1025(a,1),1(a,1,1)),rewrite(1(14),1(13),1(12),1(11),1(10),1(9),1(27),1(26),1(25),1(24),1(23)),flip(a)].

given #829 (T,wt=31): 1429 d * b * d * b * d * b * a * a0 = b * b * d * b * d * b * c * a0.  [para(1025(a,1),12(a,1,2)),flip(a)].

given #830 (T,wt=31): 1458 b * a0 * a * a0 * a * a0 * a * x = a * a0 * a * a0 * a * a0 * b * x.  [para(1230(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 #831 (A,wt=33): 333 x * y * d0 * a * c0 * a * c0 != z | c0 * a * c0 * a * c0 * a != z | x * y = b.  [para(4(a,1),75(b,1))].

given #832 (F,wt=31): 1474 d * a0 * a * a0 * a * a0 * a * x = c * a0 * a * a0 * a * a0 * b * x.  [para(1247(a,1),1(a,1,1)),rewrite(1(14),1(13),1(12),1(11),1(10),1(9),1(27),1(26),1(25),1(24),1(23)),flip(a)].

given #833 (F,wt=31): 1489 c0 * a * c0 * a * c0 * a * b * x = b * a * c0 * a * c0 * a * c0 * x.  [para(1268(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 #834 (T,wt=31): 1495 c0 * a * c0 * a * c0 * a * a * b = a * b * a * c0 * a * c0 * a * c0.  [para(1268(a,1),12(a,1,2)),flip(a)].

given #835 (T,wt=31): 1523 b0 * a0 * a * a0 * a * a0 * a * x = a * a0 * a * a0 * a * a0 * b0 * x.  [para(1371(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 #836 (A,wt=33): 334 x * d0 * x * d0 * x * d0 * y != z | a * c0 * x * d0 * x * y != z | d0 * x = b.  [para(12(a,1),75(a,1))].

given #837 (F,wt=31): 1536 a0 * c * a0 * c * a0 * c * b0 * x = b0 * a0 * c * a0 * c * a0 * c * x.  [para(1394(a,1),1(a,1,1)),rewrite(1(14),1(13),1(12),1(11),1(10),1(9),1(27),1(26),1(25),1(24),1(23)),flip(a)].

given #838 (F,wt=31): 1542 a0 * c * a0 * c * a0 * c * c * b0 = c * b0 * a0 * c * a0 * c * a0 * c.  [para(1394(a,1),12(a,1,2)),flip(a)].

given #839 (T,wt=31): 1552 d0 * c0 * a * c0 * a * c0 * a * x = a * c0 * a * c0 * a * c0 * d0 * x.  [para(1408(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 #840 (T,wt=31): 1617 d0 * a * a * c0 * a * c0 * a * c0 = a * c0 * a * c0 * a * c0 * d0 * a.  [hyper(155,a,12,a,b,123,a(flip)),rewrite(1216(15)),flip(a)].

given #841 (A,wt=33): 335 a0 * a * a0 * a * a0 * a != x | a * a0 * y != x | b0 * a * a0 * a * a0 = b0 * y.  [para(4(a,1),102(a,1))].

given #842 (F,wt=31): 1618 b0 * a * a * a0 * a * a0 * a * a0 = a * a0 * a * a0 * a * a0 * b0 * a.  [hyper(102,a,12,a,b,123,a(flip)),rewrite(1172(15)),flip(a)].

given #843 (F,wt=31): 1628 d0 * b * a * c0 * a * c0 * a * c0 = a * c0 * a * c0 * a * c0 * d0 * b.  [para(7(a,1),124(a,1,2,2,2,2,2,2)),rewrite(26(11),26(13),26(26),26(28),26(30))].

given #844 (T,wt=31): 1632 a * a0 * a * a0 * a * a0 * a0 * a = a0 * a * a * a0 * a * a0 * a * a0.  [para(124(a,2),18(a,2)),rewrite(18(15))].

given #845 (T,wt=31): 1635 a0 * c * a0 * c * a0 * c * c * a0 = c * a0 * a0 * c * a0 * c * a0 * c.  [para(124(a,1),22(a,2)),rewrite(22(15)),flip(a)].

given #846 (A,wt=33): 337 a * a0 * x * b0 * x * b0 * x != y | b * z != y | x * b0 * x * b0 * x * b0 = z.  [para(33(a,1),2(a,1))].

given #847 (F,wt=31): 1640 a * c0 * a * c0 * a * c0 * c0 * a = c0 * a * a * c0 * a * c0 * a * c0.  [para(124(a,2),26(a,2)),rewrite(26(15))].

given #848 (F,wt=31): 1674 a * d0 * c0 * d0 * c0 * d0 * c0 * c0 = b * c0 * d0 * c0 * d0 * c0 * d0 * d0.  [para(125(a,2),135(a,1,2))].

given #849 (T,wt=31): 1877 x * y * y * x * y * x * y * x = x * x * y * x * y * x * y * y.  [hyper(2,a,123,a(flip),b,149,a)].

given #850 (T,wt=31): 1929 b * b * a * b * a * b * a * b0 = a * a * b * a * b * a * b * a0.  [para(126(a,2),150(a,1,2))].

given #851 (A,wt=33): 339 a * a0 * x * b0 * x * b0 * x != y | b * x * z != y | b0 * x * b0 * x * b0 = z.  [para(33(a,1),9(a,1))].

given #852 (F,wt=31): 1932 d * d * c * d * c * d * c * b0 = c * c * d * c * d * c * d * a0.  [para(127(a,2),150(a,1,2))].

given #853 (F,wt=31): 1935 b * b * a * b * a * b * a * d0 = a * a * b * a * b * a * b * c0.  [para(128(a,2),150(a,1,2))].

given #854 (T,wt=31): 2211 d0 * d0 * x * d0 * x * d0 * x * y = x * d0 * x * d0 * x * d0 * d0 * y.  [para(2208(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 #855 (T,wt=31): 2212 x * d0 * d0 * y * d0 * y * d0 * y = x * y * d0 * y * d0 * y * d0 * d0.  [para(2208(a,1),1(a,2,2)),rewrite(1(11))].

given #856 (A,wt=33): 340 a * a0 != x | a * a0 * y * b0 * y * b0 * y != x | y * b0 * y * b0 * y * b0 = b0.  [para(33(a,1),19(b,1)),flip(c)].

given #857 (F,wt=31): 2213 d * d0 * d0 * b0 * d0 * b0 * d0 * b0 = c * c0 * b0 * d0 * b0 * d0 * b0 * d0.  [para(2208(a,2),22(a,1,2)),rewrite(541(29))].

============================== PROOF =================================

% Proof 1 at 28.75 (+ 0.03) seconds.
% Length of proof is 25.
% Level of proof is 7.
% Maximum clause weight is 31.
% Given clauses 857.

1 (x * y) * z = x * y * z # label(associativity).  [assumption].
2 x * y != z | x * u != z | y = u # label(left_cancellation_extended).  [assumption].
3 x * y != z | u * y != z | x = u # label(right_cancellation_extended).  [assumption].
4 x * y * x * y * x * y = y * x * y * x * y * x # label("(xy)^3 = (yx)^3").  [assumption].
5 b * b0 = a * a0.  [assumption].
6 d * b0 = c * a0.  [assumption].
7 b * d0 = a * c0.  [assumption].
8 d * d0 != c * c0.  [assumption].
10 x * y * z != u | v * z != u | x * y = v.  [para(1(a,1),3(a,1))].
12 x * y * x * y * x * y * z = y * x * y * x * y * x * z.  [para(4(a,1),1(a,1,1)),rewrite(1(6),1(5),1(4),1(3),1(2),1(11),1(10),1(9),1(8))].
14 x * y * z * y * z * y * z = x * z * y * z * y * z * y.  [para(4(a,1),1(a,2,2)),rewrite(1(6))].
18 b * b0 * x = a * a0 * x.  [para(5(a,1),1(a,1,1)),rewrite(1(4)),flip(a)].
22 d * b0 * x = c * a0 * x.  [para(6(a,1),1(a,1,1)),rewrite(1(4)),flip(a)].
26 b * d0 * x = a * c0 * x.  [para(7(a,1),1(a,1,1)),rewrite(1(4)),flip(a)].
33 b * x * b0 * x * b0 * x * b0 = a * a0 * x * b0 * x * b0 * x.  [para(4(a,1),18(a,1,2))].
39 a * c0 * x != y | b * z != y | d0 * x = z.  [para(26(a,1),2(a,1))].
62 x * y * z != u | v * w * z != u | x * y = v * w.  [para(1(a,1),10(b,1))].
135 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)].
194 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))].
336 a0 * d0 * b0 * d0 * b0 * d0 = c0 * b0 * d0 * b0 * d0 * b0.  [hyper(2,a,26,a(flip),b,33,a(flip)),flip(a)].
541 a0 * d0 * b0 * d0 * b0 * d0 * x = c0 * b0 * d0 * b0 * d0 * b0 * x.  [para(336(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)].
2208 d0 * d0 * x * d0 * x * d0 * x = x * d0 * x * d0 * x * d0 * d0.  [hyper(39,a,194,a,b,135,a(flip))].
2213 d * d0 * d0 * b0 * d0 * b0 * d0 * b0 = c * c0 * b0 * d0 * b0 * d0 * b0 * d0.  [para(2208(a,2),22(a,1,2)),rewrite(541(29))].
2586 d * d0 = c * c0.  [hyper(62,a,194,a,b,2213,a),flip(a)].
2587 $F.  [resolve(2586,a,8,a)].

============================== end of proof ==========================

============================== STATISTICS ============================

Given=857. Generated=198945. Kept=2586. proofs=1.
Usable=850. Sos=1662. Demods=242. Limbo=1, Disabled=80. Hints=0.
Weight_deleted=140356. Literals_deleted=0.
Forward_subsumed=56003. Back_subsumed=25.
Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0.
New_demodulators=284 (0 lex), Back_demodulated=47. Back_unit_deleted=0.
Demod_attempts=10282687. Demod_rewrites=815777.
Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0.
Nonunit_fsub_feature_tests=169732. Nonunit_bsub_feature_tests=9941.
Megabytes=3.86.
User_CPU=28.75, System_CPU=0.03, Wall_clock=29.

============================== end of statistics =====================

============================== end of search =========================

THEOREM PROVED

Exiting with 1 proof.

Process 3901 exit (max_proofs) Wed Nov 22 11:25:05 2006