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

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

% Reading from file quot-xy3a.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 = x * x * x * y * y * y # label("(xy)^3 = x^3y^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 = x * x * x * y * y * y # label("(xy)^3 = x^3y^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 = x * x * x * y * y * y # label("(xy)^3 = x^3y^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 = x * x * x * y * y * y # label("(xy)^3 = x^3y^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): 22 b * b0 * x = a * a0 * x.  [para(5(a,1),1(a,1,1)),rewrite(1(4)),flip(a)].

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

given #10 (T,wt=11): 30 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): 23 a * a0 != x | b * y != x | b0 = y.  [para(5(a,1),2(a,1))].

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

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

given #15 (T,wt=13): 28 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): 31 a * c0 != x | b * y != x | d0 = y.  [para(7(a,1),2(a,1))].

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

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

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

given #21 (A,wt=19): 11 x * y * x * y * x = y * y * x * x * x.  [hyper(2,a,xx,b,4,a),flip(a)].

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

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

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

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

given #26 (A,wt=27): 12 x * y * x * y * x * y * z = x * x * x * y * y * y * 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)),flip(a)].

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

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

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

given #30 (T,wt=17): 59 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 = x * y * x * y * x * y * z * z * z.  [para(4(a,1),1(a,1)),rewrite(1(6),1(7),1(8),1(11),1(13)),flip(a)].

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

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

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

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

given #36 (A,wt=27): 14 x * y * z * y * z * y * z = x * y * y * y * z * z * z.  [para(4(a,1),1(a,2,2)),rewrite(1(6))].

given #37 (F,wt=17): 73 c * a0 != x | c * a0 * y != x | b0 * y = b0.  [para(26(a,1),27(b,1)),flip(c)].

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

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

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

given #41 (A,wt=35): 15 x * y * z * x * y * z * x * y * z = x * x * x * y * z * y * z * y * z.  [para(1(a,1),4(a,1,2,2,2)),rewrite(1(7),1(12),1(13))].

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

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

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

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

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

given #47 (F,wt=17): 153 a * a0 * x != y | c * a0 * x != y | d = b.  [para(26(a,1),35(b,1)),flip(c)].

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

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

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

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

given #52 (F,wt=17): 348 c * a0 != x | y * a * a0 != x | y * b = d.  [para(5(a,1),74(b,1,2))].

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

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

given #55 (T,wt=19): 109 b0 * a * a0 * a * a0 = b * a * a0 * b0 * b0.  [para(5(a,1),11(a,1,2,2,2)),rewrite(22(8),22(17))].

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

given #57 (F,wt=19): 110 d * c * a0 * b0 * b0 = b0 * c * a0 * c * a0.  [para(6(a,1),11(a,1,2,2,2)),rewrite(26(8),26(17)),flip(a)].

given #58 (F,wt=19): 111 d0 * a * c0 * a * c0 = b * a * c0 * d0 * d0.  [para(7(a,1),11(a,1,2,2,2)),rewrite(30(8),30(17))].

given #59 (T,wt=19): 113 b0 * b0 * b * b * b = a * a0 * a * a0 * b.  [para(11(a,1),22(a,1)),rewrite(22(16))].

given #60 (T,wt=19): 115 a0 * a0 * a * a * a = a * a0 * a * a0 * a.  [para(11(a,1),22(a,2)),rewrite(22(9)),flip(a)].

given #61 (A,wt=29): 19 x * y * x * y * x * y != z | u * x * x * y * y * y != z | x = u.  [para(4(a,2),3(a,1))].

given #62 (F,wt=19): 119 b0 * b0 * d * d * d = c * a0 * c * a0 * d.  [para(11(a,1),26(a,1)),rewrite(26(16))].

given #63 (F,wt=19): 124 d0 * d0 * b * b * b = a * c0 * a * c0 * b.  [para(11(a,1),30(a,1)),rewrite(30(16))].

given #64 (T,wt=19): 126 c0 * c0 * a * a * a = a * c0 * a * c0 * a.  [para(11(a,1),30(a,2)),rewrite(30(9)),flip(a)].

given #65 (T,wt=19): 395 c * c * a0 * a0 * a0 = a0 * c * a0 * c * a0.  [hyper(17,a,26,a(flip),b,26,a(flip))].

given #66 (A,wt=29): 20 x * y * z * y * z * y != u | z * z * z * y * y * y != u | x = z.  [para(4(a,1),3(b,1))].

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

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

given #69 (T,wt=21): 62 x * c * a0 * y != z | x * d * u != z | b0 * y = u.  [para(26(a,1),9(a,1,2))].

given #70 (T,wt=21): 63 x * a * c0 * y != z | x * b * u != z | d0 * y = u.  [para(30(a,1),9(a,1,2))].

given #71 (A,wt=29): 21 x * y * y * z * z * z != u | y * z * y * z * y * z != u | x = y.  [para(4(a,2),3(b,1))].

given #72 (F,wt=21): 75 x * y * z * u != v | w * u != v | x * y * z = w.  [para(1(a,1),10(a,1,2))].

given #73 (F,wt=21): 76 x * y * z != u | v * w * z != u | x * y = v * w.  [para(1(a,1),10(b,1))].

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

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

given #76 (A,wt=23): 25 b * b * a * a0 * b0 * b0 = a * a0 * a * a0 * a * a0.  [para(5(a,1),4(a,1,2,2,2,2)),rewrite(22(9),22(11),22(20)),flip(a)].

given #77 (F,wt=21): 89 x * c * a0 * y != z | u * b0 * y != z | x * d = u.  [para(26(a,1),10(a,1,2))].

given #78 (F,wt=21): 90 x * y * b0 * z != u | c * a0 * z != u | x * y = d.  [para(26(a,1),10(b,1))].

given #79 (T,wt=21): 91 x * a * c0 * y != z | u * d0 * y != z | x * b = u.  [para(30(a,1),10(a,1,2))].

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

given #81 (A,wt=23): 33 b * b * a * c0 * d0 * d0 = a * c0 * a * c0 * a * c0.  [para(7(a,1),4(a,1,2,2,2,2)),rewrite(30(9),30(11),30(20)),flip(a)].

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

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

given #84 (T,wt=21): 162 c * a0 * x != y | c * a0 * z != y | b0 * x = b0 * z.  [para(26(a,1),40(b,1))].

given #85 (T,wt=21): 227 a * c0 * x != y | a * c0 * z != y | d0 * x = d0 * z.  [para(30(a,1),47(b,1))].

given #86 (A,wt=35): 36 b * b * a * a0 * x * b0 * x * b0 * x = a * a0 * x * a * a0 * x * a * a0 * x.  [para(22(a,1),4(a,1,2,2,2,2)),rewrite(1(11),22(12),1(13),22(14),1(24),1(25),22(26)),flip(a)].

given #87 (F,wt=21): 242 x * y * a * a0 != z | x * y * b * u != z | b0 = u.  [para(1(a,1),58(a,1)),rewrite(1(10))].

given #88 (F,wt=21): 244 x * a * a0 != y | x * a * a0 * z != y | b0 * z = b0.  [para(22(a,1),58(b,1,2)),flip(c)].

given #89 (T,wt=21): 245 x * a * a0 != y | x * a * c0 * z != y | d0 * z = b0.  [para(30(a,1),58(b,1,2)),flip(c)].

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

given #91 (A,wt=27): 38 a * a0 * b0 * b0 * x * x * x = a * a0 * x * b0 * x * b0 * x.  [para(4(a,1),22(a,1,2)),rewrite(22(10))].

given #92 (F,wt=19): 789 b0 * b0 * x * x * x = x * b0 * x * b0 * x.  [hyper(9,a,xx,b,38,a),flip(a)].

given #93 (F,wt=21): 253 x * c * a0 != y | x * c * a0 * z != y | b0 * z = b0.  [para(26(a,1),59(b,1,2)),flip(c)].

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

given #95 (T,wt=21): 281 x * a * c0 != y | x * a * a0 * z != y | b0 * z = d0.  [para(22(a,1),60(b,1,2)),flip(c)].

given #96 (A,wt=27): 39 a * a0 * a0 * a0 * x * x * x = a * a0 * x * a0 * x * a0 * x.  [para(4(a,1),22(a,2,2)),rewrite(22(10)),flip(a)].

given #97 (F,wt=19): 843 a0 * a0 * x * x * x = x * a0 * x * a0 * x.  [hyper(9,a,xx,b,39,a),flip(a)].

given #98 (F,wt=21): 282 x * a * c0 != y | x * a * c0 * z != y | d0 * z = d0.  [para(30(a,1),60(b,1,2)),flip(c)].

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

given #100 (T,wt=21): 347 c * a0 != x | y * z * u * b0 != x | y * z * u = d.  [para(1(a,1),74(b,1,2))].

given #101 (A,wt=35): 42 c * a0 * x * c * a0 * x * c * a0 * x = d * d * c * a0 * x * b0 * x * b0 * x.  [para(26(a,1),4(a,1,2,2,2,2)),rewrite(1(11),26(12),1(13),26(14),1(24),1(25),26(26))].

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

given #103 (F,wt=21): 351 x * a * a0 != y | z * u * b0 != y | x * b = z * u.  [para(1(a,1),83(b,1))].

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

given #105 (T,wt=21): 353 x * c * a0 != y | z * u * b0 != y | x * d = z * u.  [para(1(a,1),84(b,1))].

given #106 (A,wt=27): 44 c * a0 * b0 * b0 * x * x * x = c * a0 * x * b0 * x * b0 * x.  [para(4(a,1),26(a,1,2)),rewrite(26(10))].

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

given #108 (F,wt=21): 366 x * a * c0 != y | z * u * d0 != y | x * b = z * u.  [para(1(a,1),85(b,1))].

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

given #110 (T,wt=21): 392 x * y * a * a0 != z | x * y * a * c0 != z | d0 = b0.  [para(1(a,1),243(a,1)),rewrite(1(11))].

given #111 (A,wt=27): 45 c * a0 * a0 * a0 * x * x * x = c * a0 * x * a0 * x * a0 * x.  [para(4(a,1),26(a,2,2)),rewrite(26(10)),flip(a)].

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

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

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

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

given #116 (A,wt=35): 49 b * b * a * c0 * x * d0 * x * d0 * x = a * c0 * x * a * c0 * x * a * c0 * x.  [para(30(a,1),4(a,1,2,2,2,2)),rewrite(1(11),30(12),1(13),30(14),1(24),1(25),30(26)),flip(a)].

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

given #118 (F,wt=21): 615 x * a * a0 * y != z | a * a0 * y != z | x * b = b.  [para(22(a,1),87(b,1))].

given #119 (T,wt=21): 616 x * a * a0 * y != z | c * a0 * y != z | x * b = d.  [para(26(a,1),87(b,1))].

given #120 (T,wt=21): 630 x * c * a0 * y != z | a * a0 * y != z | x * d = b.  [para(26(a,1),88(a,1,2))].

given #121 (A,wt=27): 51 a * c0 * d0 * d0 * x * x * x = a * c0 * x * d0 * x * d0 * x.  [para(4(a,1),30(a,1,2)),rewrite(30(10))].

given #122 (F,wt=19): 959 d0 * d0 * x * x * x = x * d0 * x * d0 * x.  [hyper(9,a,xx,b,51,a),flip(a)].

given #123 (F,wt=21): 662 x * c * a0 * y != z | c * a0 * y != z | x * d = d.  [para(26(a,1),89(b,1))].

given #124 (T,wt=21): 692 x * a * c0 * y != z | a * c0 * y != z | x * b = b.  [para(30(a,1),91(b,1))].

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

given #126 (A,wt=27): 52 a * c0 * c0 * c0 * x * x * x = a * c0 * x * c0 * x * c0 * x.  [para(4(a,1),30(a,2,2)),rewrite(30(10)),flip(a)].

given #127 (F,wt=19): 1007 c0 * c0 * x * x * x = x * c0 * x * c0 * x.  [hyper(9,a,xx,b,52,a),flip(a)].

given #128 (F,wt=21): 885 x * a * a0 != y | z * c * a0 != y | z * d = x * b.  [para(6(a,1),351(b,1,2)),flip(c)].

given #129 (T,wt=21): 886 x * a * a0 != y | a * a0 * b0 != y | a * a0 = x * b.  [para(22(a,1),351(b,1)),rewrite(5(16)),flip(c)].

given #130 (T,wt=21): 887 x * a * a0 != y | c * a0 * b0 != y | c * a0 = x * b.  [para(26(a,1),351(b,1)),rewrite(6(16)),flip(c)].

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

given #132 (F,wt=21): 888 x * a * a0 != y | a * c0 * b0 != y | a * c0 = x * b.  [para(30(a,1),351(b,1)),rewrite(7(16)),flip(c)].

given #133 (F,wt=21): 892 x * c * a0 != y | z * c * a0 != y | x * d = z * d.  [para(6(a,1),353(b,1,2))].

given #134 (T,wt=21): 893 x * c * a0 != y | a * a0 * b0 != y | a * a0 = x * d.  [para(22(a,1),353(b,1)),rewrite(5(16)),flip(c)].

given #135 (T,wt=21): 894 x * c * a0 != y | c * a0 * b0 != y | c * a0 = x * d.  [para(26(a,1),353(b,1)),rewrite(6(16)),flip(c)].

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

given #137 (F,wt=21): 895 x * c * a0 != y | a * c0 * b0 != y | a * c0 = x * d.  [para(30(a,1),353(b,1)),rewrite(7(16)),flip(c)].

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

given #139 (T,wt=21): 913 x * a * c0 != y | a * a0 * d0 != y | a * a0 = x * b.  [para(22(a,1),366(b,1)),rewrite(5(16)),flip(c)].

given #140 (T,wt=21): 914 x * a * c0 != y | c * a0 * d0 != y | c * a0 = x * b.  [para(26(a,1),366(b,1)),rewrite(6(16)),flip(c)].

given #141 (A,wt=29): 64 a * a0 != x | b * b * b * y * y * y != x | y * b * y * b * y = b0.  [para(4(a,1),23(b,1)),flip(c)].

given #142 (F,wt=21): 915 x * a * c0 != y | a * c0 * d0 != y | a * c0 = x * b.  [para(30(a,1),366(b,1)),rewrite(7(16)),flip(c)].

given #143 (F,wt=23): 97 x * y * x * y * y * y = y * x * y * y * x * y.  [hyper(2,a,1,a(flip),b,11,a),rewrite(1(4),1(8),1(10))].

given #144 (T,wt=23): 99 x * y * x * y * x * z = y * y * x * x * x * z.  [para(11(a,1),1(a,1,1)),rewrite(1(5),1(4),1(3),1(2),1(9),1(8),1(7)),flip(a)].

given #145 (T,wt=23): 102 x * y * z * y * z * y = x * z * z * y * y * y.  [para(11(a,1),1(a,2,2)),rewrite(1(5))].

given #146 (A,wt=27): 98 x * y * y * x * y * y * x = y * y * x * y * x * y * x.  [hyper(2,a,1,a(flip),b,11,a(flip)),rewrite(1(4),1(10),1(11))].

given #147 (F,wt=19): 1559 d0 * a0 * c0 * a0 * c0 = b0 * a0 * c0 * c0 * c0.  [hyper(148,a,xx,b,102,a)].

given #148 (F,wt=19): 1560 d0 * c0 * a0 * a0 * a0 = b0 * c0 * a0 * c0 * a0.  [hyper(148,a,102,a,b,xx)].

given #149 (T,wt=23): 112 a * a0 * x * b0 * x * b0 = b * x * x * b0 * b0 * b0.  [para(11(a,1),22(a,1,2)),flip(a)].

given #150 (T,wt=19): 1753 a0 * d0 * b0 * d0 * b0 = c0 * d0 * b0 * b0 * b0.  [hyper(2,a,30,a(flip),b,112,a),flip(a)].

given #151 (A,wt=31): 100 x * y * z * x * y * z * x * y = z * z * x * y * x * y * x * y.  [para(11(a,1),1(a,1)),rewrite(1(4),1(5),1(11)),flip(a)].

given #152 (F,wt=23): 114 a * a0 * b0 * x * x * x = b * x * b0 * x * b0 * x.  [para(11(a,2),22(a,1,2)),flip(a)].

given #153 (F,wt=19): 1870 a0 * b0 * d0 * d0 * d0 = c0 * b0 * d0 * b0 * d0.  [hyper(2,a,30,a(flip),b,114,a),flip(a)].

given #154 (T,wt=23): 118 c * a0 * x * b0 * x * b0 = d * x * x * b0 * b0 * b0.  [para(11(a,1),26(a,1,2)),flip(a)].

given #155 (T,wt=23): 120 d * x * b0 * x * b0 * x = c * a0 * b0 * x * x * x.  [para(11(a,2),26(a,1,2))].

given #156 (A,wt=27): 101 x * y * z * x * y * z * x = y * z * y * z * x * x * x.  [para(11(a,2),1(a,1)),rewrite(1(3),1(5),1(10))].

given #157 (F,wt=23): 123 a * c0 * x * d0 * x * d0 = b * x * x * d0 * d0 * d0.  [para(11(a,1),30(a,1,2)),flip(a)].

given #158 (F,wt=23): 125 a * c0 * d0 * x * x * x = b * x * d0 * x * d0 * x.  [para(11(a,2),30(a,1,2)),flip(a)].

given #159 (T,wt=23): 145 b0 * a * a0 * b * b * b = a * a0 * b * a * a0 * b.  [hyper(34,a,1,a(flip),b,11,a),rewrite(1(10),1(20),1(22))].

given #160 (T,wt=23): 160 b0 * c * a0 * d * d * d = c * a0 * d * c * a0 * d.  [hyper(40,a,1,a(flip),b,11,a),rewrite(1(10),1(20),1(22))].

given #161 (A,wt=25): 103 x * x * y * y * y != z | y * u != z | x * y * x * y = u.  [para(11(a,1),2(a,1))].

given #162 (F,wt=23): 175 d * c * a0 * b0 * b0 * x = b0 * c * a0 * c * a0 * x.  [hyper(40,a,26,a(flip),b,12,a(flip)),rewrite(26(7),26(9),26(19)),flip(a)].

given #163 (F,wt=23): 176 b * a * a0 * b0 * b0 * x = b0 * a * a0 * a * a0 * x.  [hyper(34,a,22,a(flip),b,12,a(flip)),rewrite(22(7),22(9),22(19)),flip(a)].

given #164 (T,wt=23): 224 b * a * c0 * d0 * d0 * x = d0 * a * c0 * a * c0 * x.  [hyper(47,a,30,a(flip),b,12,a(flip)),rewrite(30(7),30(9),30(19)),flip(a)].

given #165 (T,wt=23): 225 d0 * a * c0 * b * b * b = a * c0 * b * a * c0 * b.  [hyper(47,a,1,a(flip),b,11,a),rewrite(1(10),1(20),1(22))].

given #166 (A,wt=25): 104 x * y * x * y * x != z | y * u != z | y * x * x * x = u.  [para(11(a,2),2(a,1))].

given #167 (F,wt=23): 302 x * x * y * y * y * x = y * y * y * x * x * x.  [hyper(2,a,12,a(flip),b,14,a(flip))].

given #168 (F,wt=23): 404 d * b * a * a0 * b0 * b0 = c * a0 * a * a0 * a * a0.  [para(109(a,1),26(a,1,2))].

given #169 (T,wt=23): 433 b0 * b0 * b * b * b * x = a * a0 * a * a0 * b * x.  [para(113(a,1),1(a,1,1)),rewrite(1(10),1(9),1(8),1(7),1(19),1(18),1(17)),flip(a)].

given #170 (T,wt=23): 436 a * a0 * b0 * b * b * b = b * a * a0 * a * a0 * b.  [para(113(a,1),22(a,1,2)),flip(a)].

given #171 (A,wt=25): 105 x * x * y * y * y != z | u * x * y * x * y != z | y = u.  [para(11(a,1),3(a,1))].

given #172 (F,wt=23): 437 d * a * a0 * a * a0 * b = c * a0 * b0 * b * b * b.  [para(113(a,1),26(a,1,2))].

given #173 (F,wt=23): 453 b0 * b0 * d * d * d * x = c * a0 * c * a0 * d * x.  [para(119(a,1),1(a,1,1)),rewrite(1(10),1(9),1(8),1(7),1(19),1(18),1(17)),flip(a)].

given #174 (T,wt=23): 456 a * a0 * b0 * d * d * d = b * c * a0 * c * a0 * d.  [para(119(a,1),22(a,1,2)),flip(a)].

given #175 (T,wt=23): 457 c * a0 * b0 * d * d * d = d * c * a0 * c * a0 * d.  [para(119(a,1),26(a,1,2)),flip(a)].

given #176 (A,wt=25): 106 x * y * x * y * x != z | u * y * x * x * x != z | y = u.  [para(11(a,2),3(a,1))].

given #177 (F,wt=23): 467 d0 * d0 * b * b * b * x = a * c0 * a * c0 * b * x.  [para(124(a,1),1(a,1,1)),rewrite(1(10),1(9),1(8),1(7),1(19),1(18),1(17)),flip(a)].

given #178 (F,wt=23): 470 a * c0 * d0 * b * b * b = b * a * c0 * a * c0 * b.  [para(124(a,1),30(a,1,2)),flip(a)].

given #179 (T,wt=23): 481 c * c * a0 * a0 * a0 * x = a0 * c * a0 * c * a0 * x.  [para(395(a,1),1(a,1,1)),rewrite(1(10),1(9),1(8),1(7),1(19),1(18),1(17)),flip(a)].

given #180 (T,wt=23): 809 b0 * b0 * x * x * x * y = x * b0 * x * b0 * x * y.  [para(789(a,1),1(a,1,1)),rewrite(1(7),1(6),1(5),1(4),1(13),1(12),1(11)),flip(a)].

given #181 (A,wt=25): 107 x * y * z * y * z != u | y * y * z * z * z != u | x = z.  [para(11(a,1),3(b,1))].

given #182 (F,wt=23): 811 x * b0 * b0 * y * y * y = x * y * b0 * y * b0 * y.  [para(789(a,1),1(a,2,2)),rewrite(1(7))].

given #183 (F,wt=23): 847 a0 * a0 * x * x * x * y = x * a0 * x * a0 * x * y.  [para(843(a,1),1(a,1,1)),rewrite(1(7),1(6),1(5),1(4),1(13),1(12),1(11)),flip(a)].

given #184 (T,wt=23): 849 x * a0 * a0 * y * y * y = x * y * a0 * y * a0 * y.  [para(843(a,1),1(a,2,2)),rewrite(1(7))].

given #185 (T,wt=23): 850 b * a0 * a0 * b0 * b0 * b0 = a * a0 * a0 * b0 * a0 * b0.  [para(843(a,2),22(a,1,2))].

given #186 (A,wt=25): 108 x * y * z * z * z != u | z * y * z * y * z != u | x = y.  [para(11(a,2),3(b,1))].

given #187 (F,wt=23): 851 d * a0 * a0 * b0 * b0 * b0 = c * a0 * a0 * b0 * a0 * b0.  [para(843(a,2),26(a,1,2))].

given #188 (F,wt=23): 852 b * a0 * a0 * d0 * d0 * d0 = a * c0 * a0 * d0 * a0 * d0.  [para(843(a,2),30(a,1,2))].

given #189 (T,wt=23): 977 d0 * d0 * x * x * x * y = x * d0 * x * d0 * x * y.  [para(959(a,1),1(a,1,1)),rewrite(1(7),1(6),1(5),1(4),1(13),1(12),1(11)),flip(a)].

given #190 (T,wt=23): 979 x * d0 * d0 * y * y * y = x * y * d0 * y * d0 * y.  [para(959(a,1),1(a,2,2)),rewrite(1(7))].

given #191 (A,wt=31): 117 b0 * x * a * a0 * x * a * a0 * x = b * a * a0 * x * b0 * x * b0 * x.  [para(22(a,1),11(a,1,2,2,2)),rewrite(1(10),22(11),1(12),1(21),1(22),22(23))].

given #192 (F,wt=23): 1011 c0 * c0 * x * x * x * y = x * c0 * x * c0 * x * y.  [para(1007(a,1),1(a,1,1)),rewrite(1(7),1(6),1(5),1(4),1(13),1(12),1(11)),flip(a)].

given #193 (F,wt=23): 1013 x * c0 * c0 * y * y * y = x * y * c0 * y * c0 * y.  [para(1007(a,1),1(a,2,2)),rewrite(1(7))].

given #194 (T,wt=23): 1014 b * c0 * c0 * b0 * b0 * b0 = a * a0 * c0 * b0 * c0 * b0.  [para(1007(a,2),22(a,1,2))].

given #195 (T,wt=23): 1015 d * c0 * c0 * b0 * b0 * b0 = c * a0 * c0 * b0 * c0 * b0.  [para(1007(a,2),26(a,1,2))].

given #196 (A,wt=31): 128 d0 * x * a * c0 * x * a * c0 * x = b * a * c0 * x * d0 * x * d0 * x.  [para(30(a,1),11(a,1,2,2,2)),rewrite(1(10),30(11),1(12),1(21),1(22),30(23))].

given #197 (F,wt=23): 1016 b * c0 * c0 * d0 * d0 * d0 = a * c0 * c0 * d0 * c0 * d0.  [para(1007(a,2),30(a,1,2))].

given #198 (F,wt=23): 1069 b0 * a * a0 * b0 * a * a0 = a * a0 * a * a0 * b0 * b0.  [para(5(a,1),97(a,2,2,2,2,2)),rewrite(22(9),22(11),22(21)),flip(a)].

given #199 (T,wt=23): 1070 c * a0 * c * a0 * b0 * b0 = b0 * c * a0 * b0 * c * a0.  [para(6(a,1),97(a,2,2,2,2,2)),rewrite(26(9),26(11),26(21))].

given #200 (T,wt=23): 1071 d0 * a * c0 * d0 * a * c0 = a * c0 * a * c0 * d0 * d0.  [para(7(a,1),97(a,2,2,2,2,2)),rewrite(30(9),30(11),30(21)),flip(a)].

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

given #202 (F,wt=23): 1074 a0 * a * a0 * a0 * a * a0 = a * a0 * a * a0 * a0 * a0.  [para(97(a,1),22(a,2)),rewrite(22(11)),flip(a)].

given #203 (F,wt=23): 1079 c * a0 * c * c * a0 * c = a0 * c * a0 * c * c * c.  [para(97(a,2),26(a,2)),rewrite(26(11))].

given #204 (T,wt=23): 1082 c0 * a * c0 * c0 * a * c0 = a * c0 * a * c0 * c0 * c0.  [para(97(a,1),30(a,2)),rewrite(30(11)),flip(a)].

given #205 (T,wt=23): 1304 b * x * b * x * a * a0 = x * x * b * b * a * a0.  [para(5(a,1),99(a,1,2,2,2,2)),rewrite(5(14))].

given #206 (A,wt=25): 130 x * x * y * y * y != z | y * x * u != z | y * x * y = u.  [para(11(a,1),9(a,1))].

given #207 (F,wt=23): 1305 d * x * d * x * c * a0 = x * x * d * d * c * a0.  [para(6(a,1),99(a,1,2,2,2,2)),rewrite(6(14))].

given #208 (F,wt=23): 1306 b * x * b * x * a * c0 = x * x * b * b * a * c0.  [para(7(a,1),99(a,1,2,2,2,2)),rewrite(7(14))].

given #209 (T,wt=23): 1511 b0 * b0 * b0 * x * x * x = x * x * b0 * b0 * b0 * x.  [para(789(a,2),99(a,1,2))].

given #210 (T,wt=23): 1523 a0 * a0 * a0 * x * x * x = x * x * a0 * a0 * a0 * x.  [para(843(a,2),99(a,1,2))].

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

given #212 (F,wt=23): 1543 d0 * d0 * d0 * x * x * x = x * x * d0 * d0 * d0 * x.  [para(959(a,2),99(a,1,2))].

given #213 (F,wt=23): 1553 c0 * c0 * c0 * x * x * x = x * x * c0 * c0 * c0 * x.  [para(1007(a,2),99(a,1,2))].

given #214 (T,wt=23): 1714 d0 * a0 * c0 * a0 * c0 * x = b0 * a0 * c0 * c0 * c0 * x.  [para(1559(a,1),1(a,1,1)),rewrite(1(10),1(9),1(8),1(7),1(19),1(18),1(17)),flip(a)].

given #215 (T,wt=23): 1733 d0 * c0 * a0 * a0 * a0 * x = b0 * c0 * a0 * c0 * a0 * x.  [para(1560(a,1),1(a,1,1)),rewrite(1(10),1(9),1(8),1(7),1(19),1(18),1(17)),flip(a)].

given #216 (A,wt=25): 132 x * y * x * y * x != z | y * y * u != z | x * x * x = u.  [para(11(a,2),9(a,1))].

given #217 (F,wt=23): 1795 d * d0 * d0 * b0 * b0 * b0 = c * c0 * d0 * b0 * b0 * b0.  [back_rewrite(981),rewrite(1753(21))].

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

% Proof 1 at 2.52 (+ 0.02) seconds.
% Length of proof is 23.
% Level of proof is 7.
% Maximum clause weight is 27.
% Given clauses 217.

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 = x * x * x * y * y * y # label("(xy)^3 = x^3y^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].
9 x * y * z != u | x * y * v != u | z = v.  [para(1(a,1),2(a,1)),rewrite(1(5))].
10 x * y * z != u | v * z != u | x * y = v.  [para(1(a,1),3(a,1))].
11 x * y * x * y * x = y * y * x * x * x.  [hyper(2,a,xx,b,4,a),flip(a)].
22 b * b0 * x = a * a0 * x.  [para(5(a,1),1(a,1,1)),rewrite(1(4)),flip(a)].
26 d * b0 * x = c * a0 * x.  [para(6(a,1),1(a,1,1)),rewrite(1(4)),flip(a)].
30 b * d0 * x = a * c0 * x.  [para(7(a,1),1(a,1,1)),rewrite(1(4)),flip(a)].
51 a * c0 * d0 * d0 * x * x * x = a * c0 * x * d0 * x * d0 * x.  [para(4(a,1),30(a,1,2)),rewrite(30(10))].
76 x * y * z != u | v * w * z != u | x * y = v * w.  [para(1(a,1),10(b,1))].
112 a * a0 * x * b0 * x * b0 = b * x * x * b0 * b0 * b0.  [para(11(a,1),22(a,1,2)),flip(a)].
959 d0 * d0 * x * x * x = x * d0 * x * d0 * x.  [hyper(9,a,xx,b,51,a),flip(a)].
981 d * d0 * d0 * b0 * b0 * b0 = c * a0 * d0 * b0 * d0 * b0.  [para(959(a,2),26(a,1,2))].
1753 a0 * d0 * b0 * d0 * b0 = c0 * d0 * b0 * b0 * b0.  [hyper(2,a,30,a(flip),b,112,a),flip(a)].
1795 d * d0 * d0 * b0 * b0 * b0 = c * c0 * d0 * b0 * b0 * b0.  [back_rewrite(981),rewrite(1753(21))].
3552 d * d0 = c * c0.  [hyper(76,a,xx,b,1795,a),flip(a)].
3553 $F.  [resolve(3552,a,8,a)].

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

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

Given=217. Generated=41926. Kept=3552. proofs=1.
Usable=196. Sos=3084. Demods=418. Limbo=0, Disabled=279. Hints=0.
Weight_deleted=14744. Literals_deleted=0.
Forward_subsumed=23630. Back_subsumed=225.
Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0.
New_demodulators=474 (0 lex), Back_demodulated=46. Back_unit_deleted=0.
Demod_attempts=1419879. Demod_rewrites=125847.
Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0.
Nonunit_fsub_feature_tests=253616. Nonunit_bsub_feature_tests=31488.
Megabytes=4.90.
User_CPU=2.52, System_CPU=0.02, Wall_clock=2.

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

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

THEOREM PROVED

Exiting with 1 proof.

Process 3900 exit (max_proofs) Wed Nov 22 11:24:36 2006