============================== Prover9 ===============================
Prover9 (32) version 22-May-2007, May 2007.
Process 27431 was started by mccune on cleo,
Tue May 22 14:45:40 2007
The command was "/home/mccune/bin/prover9 -f gt.in AE.in".
============================== end of head ===========================

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

% Reading from file gt.in

assign(max_seconds,30).
op(450,infix,@).
op(400,infix_right,*).
assign(eq_defs,fold).
assign(max_weight,25).

formulas(sos).
(x * y) * z = x * y * z.
e * x = x.
x' * x = e.
x @ y = x' * y' * x * y.
end_of_list.

% Reading from file AE.in


formulas(sos).
(x @ y) @ z = u @ (v @ w).
end_of_list.

formulas(sos).
A * B * C * B * A != B * A * C * A * B # answer(E).
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.  [assumption].
e * x = x.  [assumption].
x' * x = e.  [assumption].
x @ y = x' * y' * x * y.  [assumption].
(x @ y) @ z = u @ (v @ w).  [assumption].
A * B * C * B * A != B * A * C * A * B # answer(E).  [assumption].
end_of_list.

formulas(demodulators).
end_of_list.

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

No predicates eliminated.

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

Auto_denials:  (no changes).

Term ordering decisions:
Predicate symbol precedence:  predicate_order([ = ]).
Function symbol precedence:  function_order([ e, A, B, C, *, @, ' ]).
After inverse_order: Function symbol precedence:  function_order([ e, A, B, C, *, ', @ ]).
Folding symbols: @/2.
After fold_eq: Function symbol precedence:  function_order([ e, A, B, C, @, *, ' ]).

Auto_inference settings:
  % set(paramodulation).  % (positive equality literals)
    % set(paramodulation) -> set(back_demod).

Auto_process settings:  (no changes).

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

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

% Clauses after input processing:

formulas(usable).
end_of_list.

formulas(sos).
1 (x * y) * z = x * y * z.  [assumption].
2 e * x = x.  [assumption].
3 x' * x = e.  [assumption].
5 x' * y' * x * y = x @ y.  [copy(4),flip(a)].
6 (x @ y) @ z = u @ (v @ w).  [assumption].
7 A * B * C * B * A != B * A * C * A * B # answer(E).  [assumption].
end_of_list.

formulas(demodulators).
1 (x * y) * z = x * y * z.  [assumption].
2 e * x = x.  [assumption].
3 x' * x = e.  [assumption].
5 x' * y' * x * y = x @ y.  [copy(4),flip(a)].
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.  [assumption].

given #2 (I,wt=5): 2 e * x = x.  [assumption].

given #3 (I,wt=6): 3 x' * x = e.  [assumption].

given #4 (I,wt=13): 5 x' * y' * x * y = x @ y.  [copy(4),flip(a)].

given #5 (I,wt=11): 6 (x @ y) @ z = u @ (v @ w).  [assumption].

given #6 (I,wt=19): 7 A * B * C * B * A != B * A * C * A * B # answer(E).  [assumption].

given #7 (A,wt=8): 8 x' * x * y = y.  [para(3(a,1),1(a,1,1)),rewrite([2(2)]),flip(a)].

given #8 (T,wt=5): 11 e @ x = e.  [para(2(a,1),5(a,1,2,2)),rewrite([3(4),3(4)]),flip(a)].

given #9 (T,wt=4): 27 e' = e.  [para(11(a,1),5(a,2)),rewrite([2(5),3(4),25(4)])].

given #10 (T,wt=5): 20 x @ x = e.  [para(8(a,1),5(a,1,2)),rewrite([3(2)]),flip(a)].

given #11 (T,wt=5): 25 x * e = x.  [back_rewrite(18),rewrite([22(4)])].

given #12 (A,wt=17): 9 x' * y' * x * y * z = (x @ y) * z.  [para(5(a,1),1(a,1,1)),rewrite([1(7),1(6)]),flip(a)].

given #13 (T,wt=5): 31 x @ e = e.  [back_rewrite(29),rewrite([30(2)]),flip(a)].

given #14 (T,wt=6): 12 x' @ x = e.  [para(3(a,1),5(a,1,2,2)),rewrite([8(6)]),flip(a)].

given #15 (T,wt=7): 28 x @ (y @ z) = e.  [para(11(a,1),6(a,1,1)),rewrite([11(2)]),flip(a)].

given #16 (T,wt=7): 30 (x @ y) @ z = e.  [para(11(a,1),6(a,2))].

given #17 (A,wt=19): 10 (x * y)' * z' * x * y * z = x * y @ z.  [para(1(a,1),5(a,1,2,2))].

given #18 (T,wt=7): 60 x * x @ x = e.  [para(10(a,1),10(a,1,2)),rewrite([3(2),27(2),2(4),3(4),11(5)])].

given #19 (T,wt=9): 22 x'' * y = x * y.  [para(8(a,1),8(a,1,2))].

given #20 (T,wt=5): 68 x'' = x.  [para(22(a,1),25(a,1)),rewrite([25(2)]),flip(a)].

given #21 (T,wt=6): 63 x * x' = e.  [para(22(a,1),3(a,1))].

given #22 (A,wt=12): 16 (x * y)' * x * y * z = z.  [para(1(a,1),8(a,1,2))].

given #23 (T,wt=6): 72 x @ x' = e.  [para(68(a,1),12(a,1,1))].

given #24 (T,wt=7): 81 x @ x * x = e.  [para(16(a,1),5(a,1,2)),rewrite([3(2)]),flip(a)].

given #25 (T,wt=8): 67 x * x' * y = y.  [para(22(a,1),8(a,1))].

given #26 (T,wt=9): 92 x' * x' @ x = e.  [para(16(a,1),10(a,1)),rewrite([3(2)]),flip(a)].

given #27 (A,wt=12): 23 x' * y * x = y * (y @ x).  [back_rewrite(21),rewrite([22(4)]),flip(a)].

given #28 (T,wt=9): 94 (x * y)' * x = y'.  [para(63(a,1),16(a,1,2,2)),rewrite([25(4)])].

given #29 (T,wt=8): 134 (x @ y)' = y @ x.  [para(23(a,2),94(a,1,1,1)),rewrite([124(4),124(2),68(5),1(4),1(5),1(4),5(5)]),flip(a)].

given #30 (T,wt=9): 138 x @ y * x = x @ y.  [back_rewrite(121),rewrite([124(2),1(5),5(5)]),flip(a)].

given #31 (T,wt=8): 180 x' @ y = y @ x.  [back_rewrite(176),rewrite([179(3)])].

given #32 (A,wt=21): 32 x * y' * z' * y * z * u = x * (y @ z) * u.  [para(9(a,1),1(a,2,2)),rewrite([1(7)])].

given #33 (T,wt=8): 184 x @ y' = y @ x.  [para(68(a,1),180(a,1,1)),flip(a)].

given #34 (T,wt=9): 168 x * y @ x = y @ x.  [back_rewrite(118),rewrite([138(4)])].

given #35 (T,wt=9): 169 (x @ y) * (y @ x) = e.  [para(134(a,1),3(a,1,1))].

given #36 (T,wt=9): 179 x * y @ y = x @ y.  [para(138(a,1),134(a,1,1)),rewrite([134(2)]),flip(a)].

given #37 (A,wt=13): 35 x' * y * x = (x @ y') * y.  [para(3(a,1),9(a,1,2,2,2)),rewrite([25(5),22(4)])].

given #38 (T,wt=9): 187 x' @ y' = x @ y.  [para(180(a,1),180(a,2))].

given #39 (T,wt=9): 209 x' @ y = x @ y'.  [para(184(a,1),180(a,1)),flip(a)].

given #40 (T,wt=9): 216 x @ x * y = x @ y.  [para(168(a,1),134(a,1,1)),rewrite([134(2)]),flip(a)].

given #41 (T,wt=10): 103 x' @ y * x = y @ x.  [para(23(a,1),5(a,1,2,2)),rewrite([68(2),100(5),67(4)]),flip(a)].

given #42 (A,wt=22): 38 x' * y * x * (y @ z) = (x @ y') * z' * y * z.  [para(5(a,1),9(a,1,2,2,2)),rewrite([22(6)])].

given #43 (T,wt=10): 113 x' * y @ x = y @ x.  [para(23(a,1),10(a,1,2,2)),rewrite([100(8),8(4)]),flip(a)].

given #44 (T,wt=10): 124 (x * y)' = y' * x'.  [para(8(a,1),94(a,1,1,1)),flip(a)].

given #45 (T,wt=10): 167 x * y @ y' = y @ x.  [back_rewrite(119),rewrite([138(5)])].

given #46 (T,wt=10): 181 x * y @ x' = x @ y.  [back_rewrite(173),rewrite([179(5)])].

given #47 (A,wt=12): 40 (x' @ y) * x = x * (y @ x).  [para(5(a,1),9(a,1,2)),rewrite([22(4)]),flip(a)].

given #48 (T,wt=10): 215 x' * y * x @ y = e.  [para(23(a,2),168(a,1,1)),rewrite([30(6)])].

given #49 (T,wt=10): 217 x' @ x * y = y @ x.  [para(168(a,1),180(a,2))].

given #50 (T,wt=10): 220 (x @ y) * (x @ y') = e.  [para(180(a,1),169(a,1,1))].

given #51 (T,wt=10): 221 (x @ y') * (x @ y) = e.  [para(180(a,1),169(a,1,2))].

given #52 (A,wt=16): 41 x' * y * x * z = y * (y @ x) * z.  [para(9(a,1),8(a,1,2)),rewrite([22(5)]),flip(a)].

given #53 (T,wt=10): 223 (x @ y) * (x' @ y) = e.  [para(180(a,2),169(a,1,2))].

given #54 (T,wt=10): 242 x @ y' * x * y = e.  [para(35(a,2),138(a,1,2)),rewrite([28(7)])].

given #55 (T,wt=10): 338 x * y * x' @ y = e.  [para(68(a,1),215(a,1,1,1))].

given #56 (T,wt=10): 440 x @ y * x * y' = e.  [para(68(a,1),242(a,1,2,1))].

given #57 (A,wt=17): 43 x' * y * x * z = (x @ y') * y * z.  [para(8(a,1),9(a,1,2,2,2)),rewrite([22(5)])].

given #58 (T,wt=11): 106 x * y * (y @ x) = y * x.  [para(23(a,1),8(a,1,2)),rewrite([68(2)])].

given #59 (T,wt=11): 157 (x @ y) * z * (y @ x) = z.  [back_rewrite(112),rewrite([134(2)])].

given #60 (T,wt=11): 166 x * y' @ y = y' @ x.  [back_rewrite(120),rewrite([138(7)])].

given #61 (T,wt=11): 170 (x @ y) * (y @ x) * z = z.  [para(134(a,1),8(a,1,1))].

given #62 (A,wt=16): 45 (x' @ y) * x * z = x * (y @ x) * z.  [para(9(a,1),9(a,1,2)),rewrite([22(5)]),flip(a)].

given #63 (T,wt=11): 172 x' * y * x @ y' = e.  [para(5(a,1),138(a,1,2)),rewrite([28(5)]),flip(a)].

given #64 (T,wt=11): 218 x @ x' * y = y @ x'.  [para(168(a,1),184(a,1)),flip(a)].

given #65 (T,wt=11): 225 x' @ y' * x * y = e.  [para(5(a,1),179(a,1,1)),rewrite([30(5)]),flip(a)].

given #66 (T,wt=11): 230 x @ y * x' = y @ x'.  [para(179(a,1),184(a,1)),flip(a)].

given #67 (A,wt=18): 54 x' * y * z * x = y * z * (y * z @ x).  [para(10(a,1),8(a,1,2)),rewrite([22(6),1(4)]),flip(a)].

given #68 (T,wt=11): 254 (x @ y') * (y @ x') = e.  [para(209(a,1),169(a,1,1))].

given #69 (T,wt=11): 255 (x' @ y) * (y' @ x) = e.  [para(209(a,2),169(a,1,1))].

given #70 (T,wt=11): 294 x * (x @ y) @ y = x @ y.  [para(23(a,1),113(a,1,1)),rewrite([179(5)])].

given #71 (T,wt=11): 295 x' * y' * x @ y = e.  [para(23(a,2),113(a,1,1)),rewrite([30(8)])].

given #72 (A,wt=21): 59 x' * y' * x * y * z @ u = (x @ y) * z @ u.  [para(9(a,2),10(a,2,1)),rewrite([10(9)]),flip(a)].

given #73 (T,wt=11): 300 x * y @ y' * x' = e.  [para(124(a,1),72(a,1,2))].

given #74 (T,wt=11): 341 x @ y' * x' * y = e.  [para(215(a,1),184(a,1)),flip(a)].

given #75 (T,wt=11): 352 (x @ y) * y * x = x * y.  [para(217(a,1),40(a,2,2)),rewrite([124(2),179(5),187(3),1(6),106(6)])].

given #76 (T,wt=9): 827 x * y @ y * x = e.  [para(352(a,1),138(a,1,2)),rewrite([28(6)])].

given #77 (A,wt=14): 65 x' * y * x * y' = x @ y'.  [para(22(a,1),5(a,1,2))].

given #78 (T,wt=11): 392 (x @ y) * z = z * (x @ y).  [para(169(a,1),41(a,1,2,2)),rewrite([134(2),25(3),28(4),2(5)])].

given #79 (T,wt=11): 457 x @ y * x' * y' = e.  [para(338(a,1),184(a,1)),flip(a)].

given #80 (T,wt=11): 733 (x @ y) * z @ u = z @ u.  [para(59(a,1),5(a,2)),rewrite([124(7),124(5),124(3),124(2),1(5),68(7),1(6),1(5),68(8),1(7),1(6),1(5),5(6),1(11),1(10),1(9),1(8),1(13),372(12),5(5)]),flip(a)].

given #81 (T,wt=11): 745 x @ (y @ z) * u = x @ u.  [para(59(a,2),134(a,1,1)),rewrite([738(7),8(3),134(2)]),flip(a)].

given #82 (A,wt=14): 66 x * y' * x' * y = x' @ y.  [para(22(a,1),5(a,1))].

given #83 (T,wt=11): 747 x @ y * (z @ u) = x @ y.  [para(59(a,2),138(a,1)),rewrite([738(10),8(3),171(4),733(6)])].

given #84 (T,wt=11): 764 x * (y @ z) @ u = x @ u.  [para(106(a,1),59(a,2,1)),rewrite([28(4),25(4),738(7),8(3)]),flip(a)].

given #85 (T,wt=11): 810 x * y' @ y * x' = e.  [para(68(a,1),300(a,1,2,1))].

given #86 (T,wt=11): 811 x' * y @ y' * x = e.  [para(68(a,1),300(a,1,2,2))].

given #87 (A,wt=18): 69 x' * y * x * y' * z = (x @ y') * z.  [para(22(a,1),9(a,1,2))].

given #88 (T,wt=11): 812 x' * y' @ y * x = e.  [para(300(a,1),134(a,1,1)),rewrite([27(2)]),flip(a)].

given #89 (T,wt=11): 817 x * y @ x' * y' = e.  [para(106(a,1),300(a,1,1)),rewrite([124(4),134(3),1(6),745(7)])].

given #90 (T,wt=11): 837 x' * y' @ x * y = e.  [para(352(a,1),103(a,1,2)),rewrite([124(2),30(8)])].

given #91 (T,wt=11): 904 x * y @ z = y * x @ z.  [para(352(a,1),733(a,1,1))].

given #92 (A,wt=18): 70 (x' @ y) * z = x * y' * x' * y * z.  [para(22(a,1),9(a,1)),flip(a)].

given #93 (T,wt=11): 913 x @ y * z = x @ z * y.  [para(352(a,1),745(a,1,2))].

given #94 (T,wt=11): 999 x' * y @ x * y' = e.  [para(68(a,1),817(a,1,2,1))].

given #95 (T,wt=11): 1000 x * y' @ x' * y = e.  [para(68(a,1),817(a,1,2,2))].

given #96 (T,wt=12): 110 x' * (y @ z) * x = y @ z.  [para(23(a,2),9(a,2)),rewrite([30(4),25(4),5(5)]),flip(a)].

given #97 (A,wt=14): 74 x' * y' * x = (x @ y) * y'.  [para(63(a,1),9(a,1,2,2,2)),rewrite([25(4)])].

given #98 (T,wt=12): 156 (x @ y) * x' * y * x = y.  [back_rewrite(117),rewrite([134(2)])].

given #99 (T,wt=12): 207 x * (y @ x) = y * x * y'.  [para(184(a,1),23(a,2,2)),rewrite([68(2)]),flip(a)].

given #100 (T,wt=12): 236 x * (y @ x) = x * (x @ y').  [para(35(a,1),9(a,1,2,2)),rewrite([68(2),110(5),40(6)]),flip(a)].

given #101 (T,wt=12): 327 (x' @ y) * x * y = y * x.  [para(138(a,1),40(a,2,2)),rewrite([124(2),113(4),1(7),106(7)])].

given #102 (A,wt=18): 97 x' * y' * x * z = (x @ y) * y' * z.  [para(67(a,1),9(a,1,2,2,2))].

given #103 (T,wt=12): 353 (x @ y) * (x @ y') * z = z.  [para(220(a,1),1(a,1,1)),rewrite([2(2)]),flip(a)].

given #104 (T,wt=12): 355 x * (y @ z') = x * (z @ y).  [para(220(a,1),32(a,1,2,2,2,2)),rewrite([134(3),25(4),110(4),28(4),2(6)]),flip(a)].

given #105 (T,wt=12): 357 (x @ y') * (x @ y) * z = z.  [para(221(a,1),1(a,1,1)),rewrite([2(2)]),flip(a)].

given #106 (T,wt=12): 359 x * (y' @ z) = x * (z @ y).  [para(221(a,1),32(a,1,2,2,2,2)),rewrite([134(4),25(5),110(5),28(6),2(6)])].

given #107 (A,wt=16): 102 x * y' * z * y = x * z * (z @ y).  [para(23(a,1),1(a,2,2)),rewrite([1(4)])].

given #108 (T,wt=12): 418 (x @ y) * z = z * (y @ x').  [para(220(a,1),41(a,1,2,2)),rewrite([134(2),25(3),28(4),2(6)])].

given #109 (T,wt=12): 420 (x' @ y) * z = z * (y @ x).  [para(221(a,1),41(a,1,2,2)),rewrite([134(3),25(4),28(6),2(6)])].

given #110 (T,wt=12): 423 (x' @ y) * z = (y @ x) * z.  [para(41(a,1),41(a,1,2)),rewrite([8(5),375(8)]),flip(a)].

given #111 (T,wt=12): 430 (x @ y) * (x' @ y) * z = z.  [para(223(a,1),1(a,1,1)),rewrite([2(2)]),flip(a)].

given #112 (A,wt=21): 108 x' * y * x * z * (z @ y) = (x @ y') * z * y.  [para(23(a,1),9(a,1,2,2,2)),rewrite([68(3)])].

given #113 (T,wt=12): 433 (x @ y) * z = z * (y' @ x).  [para(223(a,1),41(a,1,2,2)),rewrite([134(2),25(3),28(4),2(6)])].

given #114 (T,wt=12): 469 x @ y * x * y' * x = e.  [para(440(a,1),138(a,2)),rewrite([1(4),1(3)])].

given #115 (T,wt=12): 481 (x @ y') * z = (y @ x) * z.  [para(43(a,1),9(a,1,2)),rewrite([375(6)])].

given #116 (T,wt=12): 522 x * y * (x' @ y) = y * x.  [para(180(a,2),106(a,1,2,2))].

given #117 (A,wt=22): 109 x' * y' * x * z' * y * z = (x @ y) * (y @ z).  [para(23(a,2),9(a,1,2,2,2))].

given #118 (T,wt=12): 526 x * y * (x @ y') = y * x.  [para(184(a,2),106(a,1,2,2))].

given #119 (T,wt=12): 545 (x @ y) * z * (x @ y') = z.  [para(180(a,1),157(a,1,1))].

given #120 (T,wt=12): 546 (x @ y') * z * (x @ y) = z.  [para(180(a,1),157(a,1,2,2))].

given #121 (T,wt=12): 547 (x' @ y) * z * (x @ y) = z.  [para(180(a,2),157(a,1,1))].

given #122 (A,wt=18): 111 x' * y' * z' * y * z * x = y @ z.  [para(9(a,2),23(a,1,2)),rewrite([30(11),25(11)])].

given #123 (T,wt=12): 548 (x @ y) * z * (x' @ y) = z.  [para(180(a,2),157(a,1,2,2))].

given #124 (T,wt=12): 562 (x' @ y) * (x @ y) * z = z.  [para(180(a,2),170(a,1,1))].

given #125 (T,wt=12): 674 (x @ y') * z = z * (y @ x).  [para(223(a,1),54(a,1,2,2)),rewrite([134(3),25(4),28(9),25(6)])].

given #126 (T,wt=12): 767 x' * y * x @ z = y @ z.  [para(54(a,1),59(a,1,1)),rewrite([8(5),138(4),392(4,R),352(4),168(6),392(6),764(7)])].

given #127 (A,wt=13): 116 x * (x @ y') = y * x * y'.  [para(68(a,1),23(a,1,1)),flip(a)].

given #128 (T,wt=12): 792 x * y * x' @ z = y @ z.  [back_rewrite(732),rewrite([764(3)]),flip(a)].

given #129 (T,wt=12): 834 (x @ y') * x * y = y * x.  [para(184(a,2),352(a,1,1))].

given #130 (T,wt=12): 888 x * (y @ z) * x' = y @ z.  [para(392(a,2),67(a,1,2))].

given #131 (T,wt=12): 914 x @ y' * z * y = x @ z.  [back_rewrite(906),rewrite([907(6),747(3)]),flip(a)].

given #132 (A,wt=23): 141 x' * y' * z' * x * y * z = y * x @ x' * z.  [back_rewrite(99),rewrite([124(2),124(6),68(6),1(7),1(8)])].

given #133 (T,wt=12): 1023 x' @ y * z = z * y @ x.  [para(904(a,1),180(a,2))].

given #134 (T,wt=12): 1026 x * y @ z' = z @ y * x.  [para(904(a,1),184(a,1))].

given #135 (T,wt=12): 1091 x @ y * z * y' = x @ z.  [para(8(a,1),913(a,1,2)),rewrite([1(4)]),flip(a)].

given #136 (T,wt=13): 171 x @ y * z * x = x @ y * z.  [para(1(a,1),138(a,1,2))].

given #137 (A,wt=24): 142 (x @ y * z) * z' * y' * x' * y * z * x * u = u.  [back_rewrite(93),rewrite([134(3),124(4),1(11)])].

given #138 (T,wt=13): 186 x' * y * x = y * (x' @ y).  [para(180(a,2),23(a,2,2))].

given #139 (T,wt=13): 188 x * y * x' * y' = x @ y.  [back_rewrite(165),rewrite([187(8)])].

given #140 (T,wt=13): 208 x' * y * x = y * (x @ y').  [para(184(a,2),23(a,2,2))].

given #141 (T,wt=13): 224 x * y * z @ z = x * y @ z.  [para(1(a,1),179(a,1,1))].

given #142 (A,wt=15): 144 x * y * (y @ x) * z = y * x * z.  [back_rewrite(88),rewrite([124(4),68(2),68(2),1(4)])].

given #143 (T,wt=12): 2394 x' @ y * y = y @ x * x.  [back_rewrite(2211),rewrite([2385(7),67(6)])].

given #144 (T,wt=11): 2451 x * x @ y = x @ y * y.  [para(2394(a,1),180(a,1)),flip(a)].

given #145 (T,wt=12): 2450 x * x @ y' = y * y @ x.  [para(2394(a,1),134(a,1,1)),rewrite([134(3)]),flip(a)].

given #146 (T,wt=13): 251 x * (x' @ y) = y * x * y'.  [para(209(a,2),23(a,2,2)),rewrite([68(2)]),flip(a)].

given #147 (A,wt=24): 146 x' * y * z * x * u = (x @ z' * y') * y * z * u.  [back_rewrite(85),rewrite([124(7)])].

given #148 (T,wt=13): 302 x' * y' @ z = z @ y * x.  [para(124(a,1),180(a,1,1))].

given #149 (T,wt=13): 303 x * y @ z = z @ y' * x'.  [para(124(a,1),184(a,1,2)),flip(a)].

given #150 (T,wt=13): 377 x' * y = y * (y @ x) * x'.  [para(63(a,1),41(a,1,2,2)),rewrite([25(3)])].

given #151 (T,wt=13): 509 (x' @ y) * z = (x @ y') * z.  [para(43(a,1),41(a,1,2)),rewrite([375(6),375(9)]),flip(a)].

given #152 (A,wt=21): 147 x' * y' * z * y * x * z' = y * x @ z'.  [back_rewrite(71),rewrite([124(2),1(8)])].

given #153 (T,wt=13): 521 x * y' * (x @ y) = y' * x.  [para(180(a,1),106(a,1,2,2))].

given #154 (T,wt=13): 525 x' * y * (x @ y) = y * x'.  [para(184(a,1),106(a,1,2,2))].

given #155 (T,wt=13): 550 (x @ y') * z * (y @ x') = z.  [para(209(a,1),157(a,1,1))].

given #156 (T,wt=13): 551 (x' @ y) * z * (y' @ x) = z.  [para(209(a,2),157(a,1,1))].

given #157 (A,wt=23): 148 x * y' * z' * x' * y * z = y * x' @ x * z.  [back_rewrite(55),rewrite([124(3),68(2),124(4),1(7),1(8)])].

given #158 (T,wt=13): 563 (x @ y') * (y @ x') * z = z.  [para(209(a,1),170(a,1,1))].

given #159 (T,wt=13): 564 (x' @ y) * (y' @ x) * z = z.  [para(209(a,2),170(a,1,1))].

given #160 (T,wt=13): 687 x * (y' @ z) = x * (y @ z').  [para(254(a,1),32(a,1,2,2,2,2)),rewrite([134(4),25(5),110(5),28(6),2(7)])].

given #161 (T,wt=13): 690 (x' @ y) * z = z * (x @ y').  [para(254(a,1),41(a,1,2,2)),rewrite([134(3),25(4),28(6),2(7)])].

given #162 (A,wt=24): 150 x' * y' * z' * y * x * z * u = (y * x @ z) * u.  [back_rewrite(34),rewrite([124(2),1(9)])].

given #163 (T,wt=13): 695 (x @ y') * z = z * (x' @ y).  [para(255(a,1),41(a,1,2,2)),rewrite([134(3),25(4),28(6),2(7)])].

given #164 (T,wt=13): 773 x * y * z @ y = x * z @ y.  [back_rewrite(502),rewrite([733(5)]),flip(a)].

given #165 (T,wt=13): 828 x' * y = (y @ x) * y * x'.  [para(180(a,1),352(a,1,1)),flip(a)].

given #166 (T,wt=13): 833 (x @ y) * x' * y = y * x'.  [para(184(a,1),352(a,1,1))].

given #167 (A,wt=24): 151 x' * y' * z' * x * z * y * u = (x @ z * y) * u.  [back_rewrite(33),rewrite([124(3),1(8)])].

given #168 (T,wt=13): 853 x * y * z @ z * x * y = e.  [para(1(a,1),827(a,1,1))].

given #169 (T,wt=13): 854 x * y * z @ y * z * x = e.  [para(1(a,1),827(a,1,2))].

given #170 (T,wt=13): 893 x' * (y @ z) = (y @ z) * x'.  [para(392(a,1),124(a,1,1)),rewrite([124(3),134(2),134(6)]),flip(a)].

given #171 (T,wt=13): 1027 x * y @ z = z @ x' * y'.  [para(904(a,1),184(a,2)),rewrite([124(2)]),flip(a)].

given #172 (A,wt=20): 152 x' * y' * z' * y * x * z = y * x @ z.  [back_rewrite(10),rewrite([124(2),1(8)])].

given #173 (T,wt=13): 1028 (x * y @ z) * (z @ y * x) = e.  [para(904(a,1),169(a,1,1))].

given #174 (T,wt=13): 1029 (x @ y * z) * (z * y @ x) = e.  [para(904(a,1),169(a,1,2))].

given #175 (T,wt=13): 1094 x' * y' @ z = z @ x * y.  [para(913(a,1),180(a,2)),rewrite([124(2)])].

given #176 (T,wt=13): 1675 (x @ y) * (y * z @ x) = z @ x.  [para(43(a,2),109(a,1,2,2)),rewrite([68(2),134(2),152(9),68(6),30(6),2(7)])].

given #177 (A,wt=15): 153 x' * y' = (x @ y) * y' * x'.  [back_rewrite(133),rewrite([134(2)]),flip(a)].

given #178 (T,wt=13): 1751 (x @ y) * (z * y @ x) = z @ x.  [para(106(a,1),111(a,1,2,2,2,2)),rewrite([124(3),134(2),1(10),152(9)])].

given #179 (T,wt=13): 2119 x @ y * x * z = x @ y * z.  [para(106(a,1),171(a,1,2,2)),rewrite([764(5),764(7)])].

given #180 (T,wt=13): 2170 (x @ y * z) * (y @ x) = x @ z.  [para(106(a,1),142(a,1,2,2,2,2,2)),rewrite([111(10)])].

given #181 (T,wt=13): 2332 x * y * z @ x * z * y = e.  [para(144(a,1),827(a,1,1)),rewrite([1(6),1(5),1120(7)])].

given #182 (A,wt=22): 154 x' * y' * z' * x = (x @ z * y) * y' * z'.  [back_rewrite(131),rewrite([134(3)]),flip(a)].

given #183 (T,wt=13): 2413 (x @ y) * (x @ z) = x @ y * z.  [back_rewrite(271),rewrite([2404(7),8(5)]),flip(a)].

given #184 (T,wt=13): 2416 x @ y' * y' = y @ x * x.  [back_rewrite(1938),rewrite([2412(7),8(5)]),flip(a)].

given #185 (T,wt=13): 2453 x' @ y * y = x * x @ y'.  [para(2394(a,2),184(a,2)),flip(a)].

given #186 (T,wt=13): 2511 x' * x' @ y = y * y @ x.  [para(2451(a,2),180(a,1))].

given #187 (A,wt=17): 182 (x @ y) * z = y * x' * y' * x * z.  [para(180(a,1),9(a,2,1)),rewrite([68(2)]),flip(a)].

given #188 (T,wt=13): 2569 x * x @ y * x = x @ y * y.  [para(2451(a,2),171(a,1)),rewrite([1(5),2119(6)])].

given #189 (T,wt=13): 2572 x * y @ y * y = x * x @ y.  [para(2451(a,1),224(a,1)),rewrite([1(5),773(6)])].

given #190 (T,wt=13): 2768 x * y' @ z = z @ y * x'.  [para(68(a,1),302(a,1,1,1))].

given #191 (T,wt=13): 2769 x' * y @ z = z @ y' * x.  [para(68(a,1),302(a,1,1,2))].

given #192 (A,wt=18): 183 x' * y' * x * y * z = (y' @ x) * z.  [para(180(a,2),9(a,2,1))].

given #193 (T,wt=13): 2907 x' * y @ z = z @ x * y'.  [para(377(a,1),302(a,2,2)),rewrite([68(3),2336(8)])].

given #194 (T,wt=13): 2908 x * y' @ z = z @ x' * y.  [para(377(a,2),302(a,2,2)),rewrite([124(4),68(2),134(2),1(4),2334(5)])].

given #195 (T,wt=13): 3169 (x * y @ z) * (z @ y) = x @ z.  [para(106(a,1),150(a,1,2,2,2,2)),rewrite([111(8)]),flip(a)].

given #196 (T,wt=13): 3420 x * y * z @ y * x * z = e.  [para(106(a,1),853(a,1,1,2)),rewrite([1(6),2336(7)])].

given #197 (A,wt=14): 185 x' * (y @ x) = y' * x' * y.  [para(180(a,1),23(a,2,2)),flip(a)].

given #198 (T,wt=13): 3448 x * y * z @ z * y * x = e.  [para(144(a,1),853(a,1,1)),rewrite([1(6),745(7)])].

given #199 (T,wt=13): 3587 (x @ y) * (y @ x * z) = y @ z.  [para(23(a,2),152(a,2,1)),rewrite([134(2),2307(7),8(6),767(8)])].

given #200 (T,wt=13): 3623 (x @ y) * (z @ y) = x * z @ y.  [back_rewrite(1193),rewrite([3590(8)]),flip(a)].

given #201 (T,wt=13): 4090 (x @ y) * (y @ z * x) = y @ z.  [para(2413(a,1),23(a,1,2)),rewrite([134(2),28(8),25(7)])].

given #202 (A,wt=16): 189 (x @ y) * y * z = x * y * x' * z.  [back_rewrite(164),rewrite([187(3)])].

given #203 (T,wt=13): 4486 x * x @ y * x = x * x @ y.  [para(2569(a,2),5(a,2)),rewrite([124(3),1(7),141(8),2507(4)]),flip(a)].

given #204 (T,wt=13): 4490 x * y @ x * x = y @ x * x.  [para(2569(a,2),168(a,1)),rewrite([1(2),1(4),1(5),1(4),1(7),2381(9),171(5)])].

given #205 (T,wt=13): 4517 x * x @ x * y = x * x @ y.  [para(2572(a,2),138(a,1)),rewrite([1(8),1(7),171(9),1097(5)])].

given #206 (T,wt=13): 4529 x * y @ y * y = x @ y * y.  [para(2572(a,1),110(a,1,2,1)),rewrite([4271(4),4104(6)]),flip(a)].

given #207 (A,wt=25): 193 x * y * z' * u' * z * u * v = x * y * (z @ u) * v.  [para(32(a,1),1(a,1)),rewrite([1(4)]),flip(a)].

given #208 (T,wt=14): 231 x' * y' * x * (y @ x) = y'.  [back_rewrite(137),rewrite([225(6),25(3)]),flip(a)].

given #209 (T,wt=14): 239 x' * (y @ x) = x' * (x @ y').  [para(35(a,1),23(a,1,2)),rewrite([124(2),1(7),110(6),103(8)]),flip(a)].

given #210 (T,wt=14): 246 x' * (x @ y) = y * x' * y'.  [para(187(a,1),23(a,2,2)),rewrite([68(2)]),flip(a)].

given #211 (T,wt=14): 260 x' @ y * z * x = y * z @ x.  [para(1(a,1),103(a,1,2))].

given #212 (A,wt=21): 196 x * y' * z * y * u = x * (y @ z') * z * u.  [para(8(a,1),32(a,1,2,2,2,2)),rewrite([68(3)])].

given #213 (T,wt=14): 306 x' * y' @ z = y * x @ z'.  [para(124(a,1),209(a,1,1))].

given #214 (T,wt=14): 307 x' @ y * z = x @ z' * y'.  [para(124(a,1),209(a,2,2))].

given #215 (T,wt=14): 310 x * y * z @ z' = z @ x * y.  [para(1(a,1),167(a,1,1))].

given #216 (T,wt=14): 475 (x @ y) * y' * x' * y = x'.  [para(3(a,1),43(a,1,2)),rewrite([25(3),124(3),124(5),68(3),68(3),216(3),124(4),1(6)]),flip(a)].

given #217 (A,wt=22): 198 x * (y' @ z) * u = x * y * z' * y' * z * u.  [para(68(a,1),32(a,1,2,1)),flip(a)].

given #218 (T,wt=14): 484 x' * y = (x @ y') * y * x'.  [para(63(a,1),43(a,1,2,2)),rewrite([25(3)])].

given #219 (T,wt=14): 529 x * y' * (y @ x') = y' * x.  [para(209(a,1),106(a,1,2,2))].

given #220 (T,wt=14): 530 x' * y * (y' @ x) = y * x'.  [para(209(a,2),106(a,1,2,2))].

given #221 (T,wt=14): 836 (x' @ y) * y' * x = x * y'.  [para(209(a,2),352(a,1,1))].

given #222 (A,wt=22): 199 x * y' * z * y * z' * u = x * (y @ z') * u.  [para(68(a,1),32(a,1,2,2,1))].

given #223 (T,wt=14): 1030 x' * y' @ z' = x * y @ z.  [para(904(a,1),187(a,2)),rewrite([124(2)])].

given #224 (T,wt=14): 1031 x' * y' @ z = x * y @ z'.  [para(904(a,1),209(a,2)),rewrite([124(2)])].

given #225 (T,wt=14): 1099 x' @ y' * z' = x @ y * z.  [para(913(a,1),187(a,2)),rewrite([124(3)])].

given #226 (T,wt=14): 1100 x' @ y * z = x @ y' * z'.  [para(913(a,1),209(a,1)),rewrite([124(5)])].

given #227 (A,wt=18): 200 x * y' * z' * y = x * (y @ z) * z'.  [para(63(a,1),32(a,1,2,2,2,2)),rewrite([25(4)])].

given #228 (T,wt=14): 1148 (x @ y) * x' = y * x' * y'.  [para(180(a,1),74(a,2,1)),rewrite([68(2)]),flip(a)].

given #229 (T,wt=14): 1175 (x @ y) * x * y' * x' = y'.  [para(187(a,1),156(a,1,1)),rewrite([68(3)])].

given #230 (T,wt=14): 1281 x' * (y @ z') = (z @ y) * x'.  [para(220(a,1),97(a,1,2,2)),rewrite([134(2),25(4),30(5),2(9)]),flip(a)].

given #231 (T,wt=14): 1284 x' * (y' @ z) = (z @ y) * x'.  [para(223(a,1),97(a,1,2,2)),rewrite([134(2),25(4),30(5),2(9)]),flip(a)].

given #232 (A,wt=22): 201 x * y' * z' * y * u = x * (y @ z) * z' * u.  [para(67(a,1),32(a,1,2,2,2,2))].

given #233 (T,wt=14): 1447 x' * (y @ z) = (z' @ y) * x'.  [para(418(a,1),124(a,1,1)),rewrite([124(4),134(3),134(7)]),flip(a)].

given #234 (T,wt=14): 1578 x' * (y @ z) = (z @ y') * x'.  [para(433(a,1),124(a,1,1)),rewrite([124(4),134(3),134(7)]),flip(a)].

given #235 (T,wt=14): 1654 x' * y = y * (x @ y') * x'.  [para(418(a,2),522(a,1,2)),flip(a)].

given #236 (T,wt=14): 1676 x @ y * z' = (z @ x) * (x @ y).  [para(109(a,1),106(a,2)),rewrite([783(15),5(13),28(10),25(9),1(8),1(7),1(6),1(5),1557(8)])].

given #237 (A,wt=25): 202 x * y' * z * y * u * (u @ z) = x * (y @ z') * u * z.  [para(23(a,1),32(a,1,2,2,2,2)),rewrite([68(3)])].

given #238 (T,wt=14): 1743 x * y' * x' * (x @ y) = y'.  [para(547(a,1),97(a,2)),rewrite([68(2)])].

given #239 (T,wt=14): 1761 (x @ y') * (z * x @ y) = z @ y.  [para(522(a,1),111(a,1,2,2,2,2)),rewrite([124(4),134(3),1(11),152(10)])].

given #240 (T,wt=14): 1918 x * y' @ y * y = x @ y * y.  [para(23(a,1),141(a,1,2,2,2)),rewrite([68(2),1912(7),68(6)]),flip(a)].

given #241 (T,wt=14): 1927 (x @ y') * (x * z @ y) = z @ y.  [para(41(a,2),141(a,1,2,2)),rewrite([134(3),152(10),134(11),392(11),747(12),764(9)])].

given #242 (A,wt=21): 203 x * (y @ z) * u = x * z * y' * z' * y * u.  [para(180(a,1),32(a,2,2,1)),rewrite([68(2)]),flip(a)].

given #243 (T,wt=14): 1931 (x' @ y) * (x @ y * z) = x @ z.  [para(43(a,2),141(a,1,2,2,2)),rewrite([134(3),299(10),134(11),745(12),764(9)])].

given #244 (T,wt=14): 2223 x' * y @ z = (y @ z) * (z @ x).  [para(188(a,1),108(a,2,2)),rewrite([1091(10),72(7),25(7),1(7),1(6),1680(8),124(8),124(7),68(5),68(5),1(6),1091(7)])].

given #245 (T,wt=14): 2410 (x' @ y) * (y @ z) = y @ x * z.  [back_rewrite(405),rewrite([2404(7),8(5)]),flip(a)].

given #246 (T,wt=14): 2414 x @ y * x' * z = x @ y * z.  [back_rewrite(1997),rewrite([2410(8)])].

given #247 (A,wt=22): 204 x * y' * z' * y * z * u = x * (z' @ y) * u.  [para(180(a,2),32(a,2,2,1))].

given #248 (T,wt=14): 2426 x' @ y' * z = x @ y * z'.  [back_rewrite(2000),rewrite([2414(9)])].

given #249 (T,wt=14): 2427 (x @ y') * (y @ z) = y @ x * z.  [back_rewrite(1995),rewrite([2414(8)])].

given #250 (T,wt=14): 2428 x @ y' * z = (y @ x) * (x @ z).  [back_rewrite(1984),rewrite([2414(5)])].

given #251 (T,wt=14): 2433 x @ y' * z = (x @ z) * (y @ x).  [back_rewrite(1978),rewrite([2414(5)])].

given #252 (A,wt=17): 205 x' * y * x * y' * z = (y @ x) * z.  [para(184(a,1),9(a,2,1)),rewrite([68(3)])].

given #253 (T,wt=14): 2444 x * y' @ y * x = x @ y * y.  [para(2394(a,1),5(a,2)),rewrite([68(2),124(2),1(7),148(8)])].

given #254 (T,wt=14): 2452 x' @ y * y = x' * x' @ y.  [para(2394(a,2),180(a,2)),rewrite([124(2)]),flip(a)].

given #255 (T,wt=14): 2507 x * y @ y' * x = y * y @ x.  [para(2451(a,2),5(a,2)),rewrite([124(3),1(7),141(8)])].

given #256 (T,wt=14): 2578 x * x @ x' * y = x * x @ y.  [back_rewrite(1925),rewrite([2507(4)]),flip(a)].

given #257 (A,wt=18): 206 x' * y' * x * y * z = (y @ x') * z.  [para(184(a,2),9(a,2,1))].

given #258 (T,wt=14): 2854 x * (x @ y) * y' * x' = y'.  [para(216(a,1),377(a,2,2,1)),rewrite([124(2),1(4),3(3),25(3),124(4)]),flip(a)].

given #259 (T,wt=12): 7676 x * (y @ x) * y * x' = y.  [para(184(a,1),2854(a,1,2,1)),rewrite([68(3),68(7)])].

given #260 (T,wt=14): 3232 x * y' * z @ y = x * z @ y.  [para(67(a,1),773(a,1,1,2)),flip(a)].

given #261 (T,wt=14): 3588 (x' @ y) * (z @ x) = y * z @ x.  [para(41(a,1),152(a,1,2)),rewrite([3078(8)])].

given #262 (A,wt=21): 210 x * y' * z * y * z' * u = x * (z @ y) * u.  [para(184(a,1),32(a,2,2,1)),rewrite([68(3)])].

given #263 (T,wt=14): 3622 (x @ y) * (y' @ z) = x * z @ y.  [back_rewrite(1673),rewrite([3590(8)]),flip(a)].

given #264 (T,wt=14): 3624 (x @ y) * (y @ z') = x * z @ y.  [back_rewrite(883),rewrite([3590(8)]),flip(a)].

given #265 (T,wt=14): 3699 (x @ y') * (z @ x) = y * z @ x.  [para(8(a,1),1675(a,1,2,1))].

given #266 (T,wt=14): 3701 x' * y @ z = (z @ x) * (y @ z).  [para(67(a,1),1675(a,1,2,1)),flip(a)].

given #267 (A,wt=22): 211 x * y' * z' * y * z * u = x * (z @ y') * u.  [para(184(a,2),32(a,2,2,1))].

given #268 (T,wt=14): 3725 x * y' @ z = (z @ y) * (x @ z).  [para(207(a,2),1675(a,1,2,1)),rewrite([764(4)]),flip(a)].

given #269 (T,wt=14): 3734 (x @ y) * (x' @ z * y) = z @ x.  [para(1023(a,2),1675(a,1,2))].

given #270 (T,wt=14): 3912 (x @ y) * (z' @ x) = x @ y * z.  [para(23(a,1),2170(a,1,1,2)),rewrite([747(3)])].

given #271 (T,wt=14): 3926 x @ y * z' = (x @ y) * (z @ x).  [para(207(a,2),2170(a,1,1,2)),rewrite([747(3)]),flip(a)].

given #272 (A,wt=15): 212 x * y * z @ x * y = z @ x * y.  [para(1(a,1),168(a,1,1))].

given #273 (T,wt=14): 4491 x' * y @ x * y = y @ x * x.  [para(2569(a,1),113(a,2)),rewrite([124(2),1(5),738(7)])].

given #274 (T,wt=14): 4550 x' @ y * z' = x @ z * y'.  [para(2768(a,1),180(a,2))].

given #275 (T,wt=14): 4551 x * y' @ z' = y * x' @ z.  [para(2768(a,2),180(a,1))].

given #276 (T,wt=14): 4590 x' * y @ z = x * y' @ z'.  [para(2768(a,2),1023(a,1)),flip(a)].

given #277 (A,wt=17): 245 (x @ y) * z = x * y * x' * y' * z.  [para(187(a,1),9(a,2,1)),rewrite([68(2),68(2)]),flip(a)].

given #278 (T,wt=14): 4591 x' @ y * z' = x @ y' * z.  [para(2768(a,1),1026(a,1))].

given #279 (T,wt=14): 4592 x' * y @ z' = x * y' @ z.  [para(2768(a,2),1026(a,2))].

given #280 (T,wt=14): 4637 x' @ y' * z = x @ z' * y.  [para(2769(a,1),180(a,2))].

given #281 (T,wt=14): 4638 x' * y @ z' = y' * x @ z.  [para(2769(a,2),180(a,1))].

given #282 (A,wt=21): 247 x * (y @ z) * u = x * y * z * y' * z' * u.  [para(187(a,1),32(a,2,2,1)),rewrite([68(2),68(2)]),flip(a)].

given #283 (T,wt=14): 5154 x * y' @ z = (x @ z) * (z @ y).  [para(180(a,1),3623(a,1,2)),flip(a)].

given #284 (T,wt=14): 5546 x' * y @ x * x = y @ x * x.  [para(67(a,1),4490(a,1,1)),flip(a)].

given #285 (T,wt=14): 5574 x * x @ y * x' = x * x @ y.  [para(207(a,2),4517(a,1,2)),rewrite([747(4)]),flip(a)].

given #286 (T,wt=14): 6872 x * y' @ x * y = x @ y * y.  [para(1918(a,1),216(a,2)),rewrite([1(6),8(5)])].

given #287 (A,wt=18): 248 (x @ y') * z = x * y' * x' * y * z.  [para(209(a,1),9(a,2,1)),rewrite([68(2)]),flip(a)].

given #288 (T,wt=14): 7525 x * y @ y * x' = x * x @ y.  [para(2444(a,1),134(a,1,1)),rewrite([134(3)]),flip(a)].

given #289 (T,wt=14): 7533 x' * y @ y * x = y @ x * x.  [para(522(a,1),2444(a,1,2)),rewrite([1(5),392(4),106(5),764(9)])].

given #290 (T,wt=14): 7575 x * y @ x' * y = x * x @ y.  [para(106(a,1),2507(a,1,1)),rewrite([124(4),134(3),1(5),745(6),1(9),2334(10),941(8)])].

given #291 (T,wt=14): 7577 x * y @ x * y' = y * y @ x.  [para(2507(a,1),913(a,1)),flip(a)].

given #292 (A,wt=18): 249 x' * y * x * y' * z = (x' @ y) * z.  [para(209(a,2),9(a,2,1)),rewrite([68(3)])].

given #293 (T,wt=15): 250 x' * (x @ y') = y' * x' * y.  [para(209(a,1),23(a,2,2)),flip(a)].

given #294 (T,wt=15): 256 x * y @ x * y * z = x * y @ z.  [para(1(a,1),216(a,1,2))].

given #295 (T,wt=15): 269 x' * (x' @ y) = y' * x' * y.  [para(8(a,1),38(a,1,2)),rewrite([68(6),20(5),2(10)])].

given #296 (T,wt=15): 374 (x @ y) * z * (y @ x) * u = z * u.  [para(28(a,1),41(a,2,2,1)),rewrite([134(2),2(7)])].

given #297 (A,wt=22): 252 x * (y @ z') * u = x * y * z' * y' * z * u.  [para(209(a,1),32(a,2,2,1)),rewrite([68(2)]),flip(a)].

given #298 (T,wt=15): 479 (x @ y) * y * x * z = x * y * z.  [para(8(a,1),43(a,1,2,2)),rewrite([68(2),187(5)]),flip(a)].

given #299 (T,wt=15): 528 x' * y' = y' * x' * (x @ y).  [para(187(a,1),106(a,1,2,2)),flip(a)].

given #300 (T,wt=15): 542 (x @ y) * z * u * (y @ x) = z * u.  [para(1(a,1),157(a,1,2))].

given #301 (T,wt=15): 549 x * (y @ z) * u = x * u * (y @ z).  [para(157(a,1),32(a,1,2,2,2,2)),rewrite([134(3),375(5),28(5),2(7)])].

given #302 (A,wt=22): 253 x * y' * z * y * z' * u = x * (y' @ z) * u.  [para(209(a,2),32(a,2,2,1)),rewrite([68(3)])].

given #303 (T,wt=15): 552 (x @ y) * z * u = z * u * (x @ y).  [para(157(a,1),41(a,1,2,2)),rewrite([134(2),28(5),2(7)])].

given #304 (T,wt=15): 554 x * y * z' @ z = z' @ x * y.  [para(1(a,1),166(a,1,1))].

given #305 (T,wt=15): 565 (x @ y) * z * u = z * (x @ y) * u.  [para(170(a,1),41(a,1,2,2)),rewrite([134(2),28(5),2(7)])].

given #306 (T,wt=15): 628 x @ y * z * x' = y * z @ x'.  [para(1(a,1),230(a,1,2))].

given #307 (A,wt=22): 280 (x' @ y) * z' * x * z = y * x * y' * (x @ z).  [para(180(a,1),38(a,2,1)),rewrite([68(2)]),flip(a)].

given #308 (T,wt=15): 692 x' * y' * x = (y @ x') * y'.  [para(255(a,1),38(a,1,2,2)),rewrite([134(3),25(5),68(8),30(7),2(10)]),flip(a)].

given #309 (T,wt=15): 775 x * y * z @ y' = x * z @ y'.  [back_rewrite(495),rewrite([733(6)]),flip(a)].

given #310 (T,wt=15): 783 x' @ y * x * z = x' @ y * z.  [back_rewrite(500),rewrite([745(6)]),flip(a)].

given #311 (T,wt=15): 839 (x @ y) * z * y * x = z * x * y.  [para(352(a,1),41(a,1,2,2)),rewrite([134(2),28(6),2(7)])].

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

% Proof 1 at 3.87 (+ 0.03) seconds: E.
% Length of proof is 47.
% Level of proof is 13.
% Maximum clause weight is 19.
% Given clauses 311.

1 (x * y) * z = x * y * z.  [assumption].
2 e * x = x.  [assumption].
3 x' * x = e.  [assumption].
4 x @ y = x' * y' * x * y.  [assumption].
5 x' * y' * x * y = x @ y.  [copy(4),flip(a)].
6 (x @ y) @ z = u @ (v @ w).  [assumption].
7 A * B * C * B * A != B * A * C * A * B # answer(E).  [assumption].
8 x' * x * y = y.  [para(3(a,1),1(a,1,1)),rewrite([2(2)]),flip(a)].
9 x' * y' * x * y * z = (x @ y) * z.  [para(5(a,1),1(a,1,1)),rewrite([1(7),1(6)]),flip(a)].
10 (x * y)' * z' * x * y * z = x * y @ z.  [para(1(a,1),5(a,1,2,2))].
11 e @ x = e.  [para(2(a,1),5(a,1,2,2)),rewrite([3(4),3(4)]),flip(a)].
16 (x * y)' * x * y * z = z.  [para(1(a,1),8(a,1,2))].
18 x'' * e = x.  [para(3(a,1),8(a,1,2))].
21 x'' * (x @ y) = y' * x * y.  [para(5(a,1),8(a,1,2))].
22 x'' * y = x * y.  [para(8(a,1),8(a,1,2))].
23 x' * y * x = y * (y @ x).  [back_rewrite(21),rewrite([22(4)]),flip(a)].
25 x * e = x.  [back_rewrite(18),rewrite([22(4)])].
28 x @ (y @ z) = e.  [para(11(a,1),6(a,1,1)),rewrite([11(2)]),flip(a)].
30 (x @ y) @ z = e.  [para(11(a,1),6(a,2))].
40 (x' @ y) * x = x * (y @ x).  [para(5(a,1),9(a,1,2)),rewrite([22(4)]),flip(a)].
41 x' * y * x * z = y * (y @ x) * z.  [para(9(a,1),8(a,1,2)),rewrite([22(5)]),flip(a)].
56 (x * y)' * y * x = x * y @ x.  [para(8(a,1),10(a,1,2))].
58 x' * (y * x @ y) * x = x @ y * x.  [para(9(a,1),10(a,1,2)),rewrite([8(3),8(8)])].
63 x * x' = e.  [para(22(a,1),3(a,1))].
67 x * x' * y = y.  [para(22(a,1),8(a,1))].
68 x'' = x.  [para(22(a,1),25(a,1)),rewrite([25(2)]),flip(a)].
88 (x' * y')' * (x @ y) * z = x * y * z.  [para(9(a,1),16(a,1,2))].
94 (x * y)' * x = y'.  [para(63(a,1),16(a,1,2,2)),rewrite([25(4)])].
100 (x * y)' * x * z = y' * z.  [para(67(a,1),16(a,1,2,2))].
106 x * y * (y @ x) = y * x.  [para(23(a,1),8(a,1,2)),rewrite([68(2)])].
110 x' * (y @ z) * x = y @ z.  [para(23(a,2),9(a,2)),rewrite([30(4),25(4),5(5)]),flip(a)].
113 x' * y @ x = y @ x.  [para(23(a,1),10(a,1,2,2)),rewrite([100(8),8(4)]),flip(a)].
118 x * y @ x = y @ x * y.  [back_rewrite(58),rewrite([110(5)])].
121 (x * y)' * y * x = y @ x * y.  [back_rewrite(56),rewrite([118(6)])].
124 (x * y)' = y' * x'.  [para(8(a,1),94(a,1,1,1)),flip(a)].
134 (x @ y)' = y @ x.  [para(23(a,2),94(a,1,1,1)),rewrite([124(4),124(2),68(5),1(4),1(5),1(4),5(5)]),flip(a)].
138 x @ y * x = x @ y.  [back_rewrite(121),rewrite([124(2),1(5),5(5)]),flip(a)].
144 x * y * (y @ x) * z = y * x * z.  [back_rewrite(88),rewrite([124(4),68(2),68(2),1(4)])].
168 x * y @ x = y @ x.  [back_rewrite(118),rewrite([138(4)])].
176 x' * y @ y = y @ x.  [para(67(a,1),138(a,1,2)),rewrite([113(6)])].
179 x * y @ y = x @ y.  [para(138(a,1),134(a,1,1)),rewrite([134(2)]),flip(a)].
180 x' @ y = y @ x.  [back_rewrite(176),rewrite([179(3)])].
187 x' @ y' = x @ y.  [para(180(a,1),180(a,2))].
217 x' @ x * y = y @ x.  [para(168(a,1),180(a,2))].
352 (x @ y) * y * x = x * y.  [para(217(a,1),40(a,2,2)),rewrite([124(2),179(5),187(3),1(6),106(6)])].
839 (x @ y) * z * y * x = z * x * y.  [para(352(a,1),41(a,1,2,2)),rewrite([134(2),28(6),2(7)])].
9816 $F # answer(E).  [para(839(a,2),7(a,1,2,2)),rewrite([144(13)]),xx(a)].

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

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

Given=311. Generated=134548. Kept=9814. proofs=1.
Usable=265. Sos=6390. Demods=1891. Limbo=3, Disabled=3162. Hints=0.
Weight_deleted=13739. Literals_deleted=0.
Forward_subsumed=110994. Back_subsumed=441.
Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0.
New_demodulators=3711 (5 lex), Back_demodulated=2715. Back_unit_deleted=0.
Demod_attempts=2480416. Demod_rewrites=523491.
Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0.
Nonunit_fsub_feature_tests=0. Nonunit_bsub_feature_tests=0.
Megabytes=7.64.
User_CPU=3.87, System_CPU=0.03, Wall_clock=4.

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

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

THEOREM PROVED

Exiting with 1 proof.

Process 27431 exit (max_proofs) Tue May 22 14:45:44 2007