============================== Prover9 ===============================
Prover9 (32) version March-2007, March 2007.
Process 21023 was started by mccune on cleo,
Mon Mar 19 17:02:11 2007
The command was "/home/mccune/bin/prover9 -f gt.in NE.in".
============================== end of head ===========================

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

% Reading from file gt.in

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 NE.in


formulas(sos).
(x @ y) * z = z * (x @ y).
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 = z * (x @ y).  [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:
Relation symbol precedence:  lex([ = ]).
Function symbol precedence:  lex([ e, A, B, C, *, @, ' ]).
After inverse_order: Function symbol precedence:  lex([ e, A, B, C, *, ', @ ]).
Folding symbols: @/2.
After fold_eq: Function symbol precedence:  lex([ 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 = z * (x @ y).  [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)].
6 (x @ y) * z = z * (x @ y).  [assumption].
        % (lex-dep)
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 = z * (x @ y).  [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): 33 e' = e.  [para(11(a,1),5(a,2)),rewrite(2(5),3(4),31(4))].

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

given #11 (T,wt=5): 31 x * e = x.  [back_rewrite(22),rewrite(28(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): 34 x @ e = e.  [para(33(a,1),5(a,1,2,1)),rewrite(31(4),2(3),3(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): 18 (x @ y) @ z = e.  [para(6(a,1),5(a,1,2,2)),rewrite(8(6),6(4,R),17(4)),flip(a)].

given #16 (T,wt=7): 19 x @ (y @ z) = e.  [para(6(a,2),5(a,1,2,2)),rewrite(8(6),3(2)),flip(a)].

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): 72 x @ x * x = e.  [para(10(a,1),10(a,1,2)),rewrite(3(2),33(2),70(3),2(4),3(4),11(5))].

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

given #20 (T,wt=5): 82 x'' = x.  [para(28(a,1),31(a,1)),rewrite(31(2)),flip(a)].

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

given #22 (A,wt=15): 14 (x @ y) * z * u = z * (x @ y) * u.  [para(6(a,1),1(a,1,1)),rewrite(1(3)),flip(a)].

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

given #24 (T,wt=8): 81 x * x' * y = y.  [para(28(a,1),8(a,1))].

given #25 (T,wt=10): 87 x * y * (x * y)' = e.  [para(76(a,1),1(a,1)),flip(a)].

given #26 (T,wt=9): 122 x * (y * x)' = y'.  [para(87(a,1),8(a,1,2)),rewrite(31(3)),flip(a)].

given #27 (A,wt=15): 15 (x @ y) * z * u = z * u * (x @ y).  [para(6(a,2),1(a,1))].

given #28 (T,wt=8): 138 (x @ y)' = y @ x.  [para(9(a,2),122(a,1,2,1)),rewrite(137(7),137(5),137(3),137(2),1(5),82(7),1(6),1(5),82(8),1(7),1(6),1(5),5(6),81(4)),flip(a)].

given #29 (T,wt=9): 144 (x @ y) * (y @ x) = e.  [back_rewrite(127),rewrite(137(5),137(4),138(4),1(6),81(7),109(5))].

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

given #31 (T,wt=9): 174 x * y @ x = y @ x.  [back_rewrite(70),rewrite(153(4))].

given #32 (A,wt=15): 16 x * (y @ z) * u = x * u * (y @ z).  [para(6(a,1),1(a,2,2)),rewrite(1(3))].

given #33 (T,wt=8): 218 x @ y' = y @ x.  [para(8(a,1),174(a,1,1)),rewrite(216(5))].

given #34 (T,wt=8): 220 x' @ y = y @ x.  [para(81(a,1),174(a,1,1)),rewrite(215(4)),flip(a)].

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

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

given #37 (A,wt=12): 27 x' * (y @ z) * x = y @ z.  [para(6(a,2),8(a,1,2))].

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

given #39 (T,wt=9): 261 x' @ y = x @ y'.  [para(220(a,1),218(a,1))].

given #40 (T,wt=10): 137 (x * y)' = y' * x'.  [para(122(a,1),8(a,1,2)),flip(a)].

given #41 (T,wt=10): 172 x * y @ y' = y @ x.  [back_rewrite(90),rewrite(153(5))].

given #42 (A,wt=12): 29 x' * y * x = y * (y @ x).  [back_rewrite(25),rewrite(28(4)),flip(a)].

given #43 (T,wt=10): 216 x * y @ x' = x @ y.  [back_rewrite(207),rewrite(214(5))].

given #44 (T,wt=10): 243 (x @ y) * (x' @ y) = e.  [para(218(a,1),144(a,1,1))].

given #45 (T,wt=10): 244 (x @ y) * (x @ y') = e.  [para(218(a,2),144(a,1,1)),rewrite(6(4,R))].

given #46 (T,wt=10): 268 x' @ y * x = y @ x.  [para(214(a,1),220(a,2))].

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

given #48 (T,wt=10): 322 x' * y * x @ y = e.  [para(29(a,2),174(a,1,1)),rewrite(18(6))].

given #49 (T,wt=10): 328 x @ y' * x * y = e.  [para(29(a,2),221(a,1,2)),rewrite(19(6))].

given #50 (T,wt=10): 393 x * y * x' @ y = e.  [para(82(a,1),322(a,1,1,1))].

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

given #52 (A,wt=13): 38 x' * y * x = y * (x @ y').  [para(3(a,1),9(a,1,2,2,2)),rewrite(31(5),28(4),6(6))].

given #53 (T,wt=11): 129 x' * y' @ x * y = e.  [back_rewrite(59),rewrite(123(8),3(8)),flip(a)].

given #54 (T,wt=9): 467 x * y @ y * x = e.  [para(129(a,1),218(a,2)),rewrite(137(5),82(3),82(3))].

given #55 (T,wt=11): 163 x' @ x * y = x' @ y.  [back_rewrite(30),rewrite(137(2),1(4),79(5)),flip(a)].

given #56 (T,wt=11): 168 (x @ y) * z * (y @ x) = z.  [back_rewrite(110),rewrite(138(3))].

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

given #58 (T,wt=11): 173 x * y' @ y = y' @ x.  [back_rewrite(73),rewrite(153(7))].

given #59 (T,wt=11): 177 x @ y * (z @ u) = x @ y.  [para(15(a,2),5(a,1,2,2)),rewrite(137(4),138(3),1(8),166(8),5(5)),flip(a)].

given #60 (T,wt=11): 194 (x @ y) * (y @ x) * z = z.  [para(138(a,1),8(a,1,1))].

given #61 (T,wt=11): 195 x @ (y @ z) * u = x @ u.  [back_rewrite(151),rewrite(194(7),5(5)),flip(a)].

given #62 (A,wt=17): 44 x' * y' * x * y * z = z * (x @ y).  [para(9(a,2),6(a,1))].

given #63 (T,wt=11): 196 (x @ y) * z @ u = z @ u.  [back_rewrite(150),rewrite(194(8),5(5)),flip(a)].

given #64 (T,wt=11): 201 x * (y @ z) @ u = x @ u.  [back_rewrite(65),rewrite(196(3)),flip(a)].

given #65 (T,wt=11): 215 x' * y @ x = x' @ y.  [back_rewrite(212),rewrite(214(3)),flip(a)].

given #66 (T,wt=11): 245 x @ x' * y = y @ x'.  [para(218(a,1),174(a,1))].

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

given #68 (T,wt=11): 267 x @ y * x' = y @ x'.  [para(214(a,1),218(a,1)),flip(a)].

given #69 (T,wt=11): 286 (x @ y') * (y @ x') = e.  [para(261(a,1),144(a,1,1))].

given #70 (T,wt=11): 287 (x' @ y) * (y' @ x) = e.  [para(261(a,2),144(a,1,1))].

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

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

given #73 (T,wt=11): 311 x * y * (y @ x) = y * x.  [para(29(a,1),8(a,1,2)),rewrite(82(2))].

given #74 (T,wt=11): 323 (x @ y) * y * x = x * y.  [para(174(a,1),29(a,2,2)),rewrite(1(3),8(4),6(4,R)),flip(a)].

given #75 (T,wt=11): 420 x @ y * x' * y' = e.  [para(393(a,1),218(a,1)),flip(a)].

given #76 (T,wt=11): 427 x * y' * x' @ y = e.  [para(393(a,1),243(a,1,1)),rewrite(137(5),137(4),82(3),1(5),2(7))].

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

given #78 (T,wt=11): 461 x * y' @ x' * y = e.  [para(82(a,1),129(a,1,1,1))].

given #79 (T,wt=11): 462 x' * y @ x * y' = e.  [para(82(a,1),129(a,1,1,2))].

given #80 (T,wt=11): 464 x * y @ x' * y' = e.  [para(129(a,1),138(a,1,1)),rewrite(33(2)),flip(a)].

given #81 (T,wt=11): 552 x' * y' @ y * x = e.  [back_rewrite(351),rewrite(548(7))].

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

given #83 (T,wt=11): 652 x * y' @ y * x' = e.  [para(82(a,1),293(a,1,2,1))].

given #84 (T,wt=11): 653 x' * y @ y' * x = e.  [para(82(a,1),293(a,1,2,2))].

given #85 (T,wt=11): 794 x @ y * z = x @ z * y.  [para(323(a,1),195(a,1,2))].

given #86 (T,wt=11): 797 x * y @ z = y * x @ z.  [para(323(a,1),196(a,1,1))].

given #87 (A,wt=14): 78 x' * y * x * y' = x @ y'.  [para(28(a,1),5(a,1,2))].

given #88 (T,wt=12): 109 x * (y @ z) * x' = y @ z.  [para(76(a,1),14(a,1,2)),rewrite(31(3)),flip(a)].

given #89 (T,wt=12): 235 (x @ y) * z = z * (y @ x').  [para(218(a,1),6(a,1,1))].

given #90 (T,wt=12): 236 (x @ y') * z = z * (y @ x).  [para(218(a,2),6(a,1,1))].

given #91 (T,wt=12): 250 x * (y @ x) = y * x * y'.  [back_rewrite(159),rewrite(249(3))].

given #92 (A,wt=14): 79 x * y' * x' * y = x' @ y.  [para(28(a,1),5(a,1))].

given #93 (T,wt=12): 251 (x @ y) * z = z * (y' @ x).  [para(220(a,1),6(a,1,1))].

given #94 (T,wt=12): 252 (x' @ y) * z = z * (y @ x).  [para(220(a,2),6(a,1,1))].

given #95 (T,wt=12): 333 (x @ y) * x' * y * x = y.  [para(29(a,2),29(a,1,2)),rewrite(138(2),19(7),31(7))].

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

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

given #98 (T,wt=12): 339 (x @ y) * z * (x' @ y) = z.  [para(243(a,1),14(a,2,2)),rewrite(31(7))].

given #99 (T,wt=12): 340 (x' @ y) * z * (x @ y) = z.  [para(243(a,1),15(a,2,2)),rewrite(31(7))].

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

given #101 (T,wt=12): 345 (x @ y) * z * (x @ y') = z.  [para(244(a,1),14(a,2,2)),rewrite(31(7))].

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

given #103 (T,wt=12): 346 (x @ y') * z * (x @ y) = z.  [para(244(a,1),15(a,2,2)),rewrite(31(7))].

given #104 (T,wt=12): 386 x * (y' @ z) = x * (z @ y).  [para(243(a,1),35(a,1,2,2,2,2)),rewrite(138(3),31(4),27(4),19(4),2(6)),flip(a)].

given #105 (T,wt=12): 387 x * (y @ z') = x * (z @ y).  [para(244(a,1),35(a,1,2,2,2,2)),rewrite(138(3),31(4),27(4),19(4),2(6)),flip(a)].

given #106 (T,wt=12): 422 x * y * x' * y @ y = e.  [para(393(a,1),214(a,2)),rewrite(1(4),1(3))].

given #107 (A,wt=14): 88 x' * y' * x = (x @ y) * y'.  [para(76(a,1),9(a,1,2,2,2)),rewrite(31(4))].

given #108 (T,wt=12): 441 x * y * (x @ y') = y * x.  [para(38(a,1),8(a,1,2)),rewrite(82(2))].

given #109 (T,wt=12): 523 x' * y * x @ z = y @ z.  [para(41(a,1),216(a,1,1)),rewrite(82(8),196(7),354(9))].

given #110 (T,wt=12): 533 x @ y' * z * y = x @ z.  [para(41(a,1),163(a,1,2)),rewrite(82(2),195(7),82(6),232(8))].

given #111 (T,wt=12): 544 (x' @ y) * (x @ y) * z = z.  [para(218(a,1),194(a,1,2,1))].

given #112 (A,wt=19): 91 (x @ y) * z * u * v = z * u * (x @ y) * v.  [para(14(a,2),1(a,1)),rewrite(1(3))].

given #113 (T,wt=12): 545 (x @ y') * (x @ y) * z = z.  [para(218(a,2),194(a,1,1))].

given #114 (T,wt=12): 664 (x' @ y) * z = (y @ x) * z.  [para(47(a,1),9(a,1)),rewrite(99(6))].

given #115 (T,wt=12): 759 x * y * (x' @ y) = y * x.  [para(220(a,2),311(a,1,2,2))].

given #116 (T,wt=12): 784 (x @ y') * x * y = y * x.  [para(218(a,2),323(a,1,1))].

given #117 (A,wt=19): 92 x * (y @ z) * u * v = x * u * (y @ z) * v.  [para(14(a,1),1(a,2,2)),rewrite(1(4))].

given #118 (T,wt=12): 786 (x' @ y) * x * y = y * x.  [para(220(a,2),323(a,1,1))].

given #119 (T,wt=12): 822 (x @ y') * z = (y @ x) * z.  [para(49(a,1),9(a,1,2)),rewrite(99(6))].

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

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

given #122 (A,wt=21): 96 x' * (y @ z) * u' * x * u = (y @ z) * (x @ u).  [para(5(a,1),14(a,1,2)),flip(a)].

given #123 (T,wt=12): 972 x' @ y * z = z * y @ x.  [para(794(a,1),220(a,1))].

given #124 (T,wt=12): 1003 x * y * x' @ z = y @ z.  [para(8(a,1),797(a,1,1)),rewrite(1(4)),flip(a)].

given #125 (T,wt=12): 1127 x * (y @ x) = x * (x @ y').  [para(250(a,2),311(a,2)),rewrite(267(5),1(6),8(5)),flip(a)].

given #126 (T,wt=13): 204 x @ y * z * x = x @ y * z.  [para(1(a,1),153(a,1,2))].

given #127 (A,wt=19): 97 (x @ y) * (z @ u) * v = v * (x @ y) * (z @ u).  [para(6(a,2),14(a,1,2))].

given #128 (T,wt=13): 262 x * y * z @ z = x * y @ z.  [para(1(a,1),214(a,1,1))].

given #129 (T,wt=13): 276 x * y * x' * y' = x @ y.  [para(249(a,1),5(a,2)),rewrite(82(2),82(2))].

given #130 (T,wt=13): 278 (x @ y') * z = z * (x' @ y).  [para(261(a,1),6(a,1,1))].

given #131 (T,wt=13): 279 (x' @ y) * z = z * (x @ y').  [para(261(a,2),6(a,1,1))].

given #132 (A,wt=16): 99 x' * (y @ z) * x * u = (y @ z) * u.  [para(14(a,2),8(a,1,2))].

given #133 (T,wt=13): 291 x' * (y @ z) = (y @ z) * x'.  [para(6(a,1),137(a,1,1)),rewrite(137(3),138(2),138(6)),flip(a)].

given #134 (T,wt=13): 296 x * y @ z = z @ y' * x'.  [para(137(a,1),218(a,1,2)),flip(a)].

given #135 (T,wt=13): 297 x' * y' @ z = z @ y * x.  [para(137(a,1),220(a,1,1))].

given #136 (T,wt=13): 316 x * (x @ y') = y * x * y'.  [para(82(a,1),29(a,1,1)),flip(a)].

given #137 (A,wt=25): 101 x' * y' * x * (z @ u) * y * v = (x @ y) * (z @ u) * v.  [para(14(a,2),9(a,1,2,2,2))].

given #138 (T,wt=13): 326 x' * y * x = y * (x' @ y).  [para(220(a,2),29(a,2,2))].

given #139 (T,wt=13): 331 x * (x' @ y) = y * x * y'.  [para(261(a,2),29(a,2,2)),rewrite(82(2)),flip(a)].

given #140 (T,wt=13): 453 (x' @ y) * y' * x * y = x.  [para(38(a,2),29(a,1,2)),rewrite(138(3),19(9),31(8))].

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

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

given #143 (T,wt=13): 472 x * y * z @ y * z * x = e.  [para(1(a,1),467(a,1,2))].

given #144 (T,wt=13): 489 (x @ y') * z * (y @ x') = z.  [para(261(a,1),168(a,1,1))].

given #145 (T,wt=13): 490 (x' @ y) * z * (y' @ x) = z.  [para(261(a,2),168(a,1,1))].

given #146 (T,wt=13): 546 (x @ y') * (y @ x') * z = z.  [para(261(a,1),194(a,1,1))].

given #147 (A,wt=25): 103 x' * (y @ z) * u' * x * u * v = (y @ z) * (x @ u) * v.  [para(9(a,1),14(a,1,2)),flip(a)].

given #148 (T,wt=13): 547 (x' @ y) * (y' @ x) * z = z.  [para(261(a,2),194(a,1,1))].

given #149 (T,wt=13): 645 x * (y' @ z) = x * (y @ z').  [para(286(a,1),35(a,1,2,2,2,2)),rewrite(138(4),31(5),27(5),19(6),2(7))].

given #150 (T,wt=13): 671 x' * y = y * (y @ x) * x'.  [para(76(a,1),47(a,1,2,2)),rewrite(31(3))].

given #151 (T,wt=13): 724 x @ y * x * z = x @ y * z.  [para(47(a,1),163(a,1,2)),rewrite(82(2),548(4),82(4)),flip(a)].

given #152 (A,wt=25): 104 (x @ y) * z' * u' * z * u * v = (z @ u) * (x @ y) * v.  [para(9(a,2),14(a,1,2))].

given #153 (T,wt=13): 736 x @ y * z = (x @ z) * (x @ y).  [para(47(a,2),46(a,1,2,2)),rewrite(290(8))].

given #154 (T,wt=13): 757 x' * y * (x @ y) = y * x'.  [para(218(a,1),311(a,1,2,2))].

given #155 (T,wt=13): 758 x * y' * (x @ y) = y' * x.  [para(220(a,1),311(a,1,2,2))].

given #156 (T,wt=13): 783 (x @ y) * x' * y = y * x'.  [para(218(a,1),323(a,1,1))].

given #157 (A,wt=21): 105 (x @ y) * z * u = z * x' * y' * x * y * u.  [para(9(a,2),14(a,2,2))].

given #158 (T,wt=13): 785 x' * y = (y @ x) * y * x'.  [para(220(a,1),323(a,1,1)),flip(a)].

given #159 (T,wt=12): 3075 x * (y @ x) * y * x' = y.  [para(785(a,1),8(a,1,2)),rewrite(82(2))].

given #160 (T,wt=13): 861 (x' @ y) * z = (x @ y') * z.  [para(49(a,1),47(a,1,2)),rewrite(99(6),99(9)),flip(a)].

given #161 (T,wt=13): 968 (x * y @ z) * (z @ y * x) = e.  [para(794(a,1),144(a,1,2))].

given #162 (A,wt=23): 111 (x @ y) * (z @ u) * v * w = v * (x @ y) * (z @ u) * w.  [para(14(a,2),14(a,1,2))].

given #163 (T,wt=13): 973 x' * y' @ z = z @ x * y.  [para(794(a,1),220(a,2)),rewrite(137(2))].

given #164 (T,wt=13): 1009 x * y @ z = z @ x' * y'.  [para(797(a,1),218(a,2)),rewrite(137(2)),flip(a)].

given #165 (T,wt=13): 1420 x * x * y * y @ x * y = e.  [para(8(a,1),422(a,1,1,2,2)),rewrite(1(2))].

given #166 (T,wt=13): 1862 (x @ y) * (z @ y) = x * z @ y.  [para(49(a,2),96(a,1,2)),rewrite(164(8),82(4)),flip(a)].

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

given #168 (T,wt=13): 2037 x * y * z @ y = x * z @ y.  [para(311(a,1),262(a,1,1,2)),rewrite(177(5),177(7))].

given #169 (T,wt=13): 2218 x * y' @ z = z @ y * x'.  [para(82(a,1),296(a,2,2,1))].

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

given #171 (T,wt=13): 2436 x * y * z @ y * x * z = e.  [para(311(a,1),471(a,1,1,2)),rewrite(1(6),548(7))].

given #172 (A,wt=16): 116 x * (y @ z) * x' * u = (y @ z) * u.  [para(81(a,1),14(a,1,2)),flip(a)].

given #173 (T,wt=13): 2437 x * y * z @ z * y * x = e.  [para(323(a,1),471(a,1,1,2)),rewrite(1(6),1575(7))].

given #174 (T,wt=13): 2664 x * y' @ z = z @ x' * y.  [para(671(a,1),296(a,1,1)),rewrite(199(5),82(6))].

given #175 (T,wt=13): 2665 x' * y @ z = z @ x * y'.  [para(671(a,2),296(a,1,1)),rewrite(137(7),82(5),138(5),1(7),548(8))].

given #176 (T,wt=13): 2724 (x @ y) * (x @ z) = x @ y * z.  [para(736(a,2),6(a,1)),flip(a)].

given #177 (A,wt=24): 140 x' * y' * z * x * y * z' = y * x @ x' * z'.  [para(122(a,1),10(a,1,2,2,2)),rewrite(137(2),137(5),137(7),82(5),82(5),1(7),1(8),137(11))].

given #178 (T,wt=11): 4121 x * x @ y = x @ y * y.  [para(2724(a,1),1862(a,1)),flip(a)].

given #179 (T,wt=12): 4204 x * x @ y' = y * y @ x.  [para(4121(a,2),218(a,2))].

given #180 (T,wt=12): 4206 x' @ y * y = y @ x * x.  [para(4121(a,1),220(a,2))].

given #181 (T,wt=13): 2726 (x @ y) * (y @ z * x) = y @ z.  [para(736(a,2),8(a,1,2)),rewrite(138(2))].

given #182 (A,wt=15): 148 x' * y' = (x @ y) * y' * x'.  [back_rewrite(123),rewrite(137(3)),flip(a)].

given #183 (T,wt=13): 2747 (x @ y) * (y @ x * z) = y @ z.  [para(736(a,2),27(a,1,2)),rewrite(138(2))].

given #184 (T,wt=13): 3331 (x @ y) * (y * z @ x) = z @ x.  [para(1862(a,1),8(a,1,2)),rewrite(138(2))].

given #185 (T,wt=13): 3339 (x @ y) * (z * y @ x) = z @ x.  [para(1862(a,1),27(a,1,2)),rewrite(138(2))].

given #186 (T,wt=13): 3859 x * y * z @ x * z * y = e.  [para(323(a,1),2436(a,1,1,2)),rewrite(195(7))].

given #187 (A,wt=23): 149 x' * y' * z' * x * y * z = y * x @ x' * z.  [back_rewrite(115),rewrite(137(2),137(6),82(6),1(7),1(8))].

given #188 (T,wt=13): 4203 x @ y' * y' = y @ x * x.  [para(4121(a,1),218(a,1))].

given #189 (T,wt=13): 4205 x' * x' @ y = y * y @ x.  [para(4121(a,2),220(a,1))].

given #190 (T,wt=13): 4235 x * x @ y * x = x @ y * y.  [para(4121(a,2),204(a,1)),rewrite(1(5),724(6))].

given #191 (T,wt=13): 4236 x * y @ y * y = x * x @ y.  [para(4121(a,1),262(a,1)),rewrite(1(5),2037(6))].

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

given #193 (T,wt=13): 4273 x' @ y * y = x * x @ y'.  [para(4204(a,2),220(a,2))].

given #194 (T,wt=13): 4619 x * x @ y * x = x * x @ y.  [para(4235(a,2),5(a,2)),rewrite(137(3),1(7),149(8),4202(4)),flip(a)].

given #195 (T,wt=13): 4623 x * y @ x * x = y @ x * x.  [para(4235(a,2),214(a,1)),rewrite(1(5),1(4),262(9),1010(5))].

given #196 (T,wt=13): 4662 x * x @ x * y = x * x @ y.  [para(4236(a,2),153(a,1)),rewrite(1(8),1(7),204(9),969(5))].

given #197 (A,wt=23): 154 x * y' * z' * x' * y * z = y * x' @ x * z.  [back_rewrite(67),rewrite(137(3),82(2),137(4),1(7),1(8))].

given #198 (T,wt=13): 4668 x * y @ y * y = x @ y * y.  [para(4236(a,1),27(a,1,2,1)),rewrite(3330(4),275(6),2724(3)),flip(a)].

given #199 (T,wt=14): 300 x' * y' @ z = y * x @ z'.  [para(137(a,1),261(a,1,1))].

given #200 (T,wt=14): 301 x' @ y * z = x @ z' * y'.  [para(137(a,1),261(a,2,2))].

given #201 (T,wt=14): 302 x * y * z @ z' = z @ x * y.  [para(1(a,1),172(a,1,1))].

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

given #203 (T,wt=14): 310 (x @ y) * y' * x' * y = x'.  [para(5(a,1),29(a,1,2)),rewrite(137(4),137(2),82(5),1(4),6(6,R),263(12),31(9))].

given #204 (T,wt=14): 325 x' * (y @ x) = y' * x' * y.  [para(220(a,1),29(a,2,2)),flip(a)].

given #205 (T,wt=14): 329 x' * (x @ y) = y * x' * y'.  [para(249(a,1),29(a,2,2)),rewrite(82(2)),flip(a)].

given #206 (T,wt=14): 348 x' @ y * z * x = y * z @ x.  [para(1(a,1),268(a,1,2))].

given #207 (A,wt=15): 166 (x @ y) * z * (y @ x) * u = z * u.  [back_rewrite(117),rewrite(138(3))].

given #208 (T,wt=14): 452 x' * (y @ x) = x' * (x @ y').  [para(38(a,1),29(a,1,2)),rewrite(137(2),1(7),8(6),268(8)),flip(a)].

given #209 (T,wt=14): 658 x' * y' * x * (y @ x) = y'.  [para(3(a,1),47(a,1,2)),rewrite(31(3),137(3),137(6),173(8),249(7),6(6),1(7)),flip(a)].

given #210 (T,wt=14): 762 x * y' * (y @ x') = y' * x.  [para(261(a,1),311(a,1,2,2))].

given #211 (T,wt=14): 763 x' * y * (y' @ x) = y * x'.  [para(261(a,2),311(a,1,2,2))].

given #212 (A,wt=19): 175 (x @ y) * z * u * v = z * u * v * (x @ y).  [para(15(a,2),1(a,1)),rewrite(1(3))].

given #213 (T,wt=14): 787 x' * y = (x @ y') * y * x'.  [para(261(a,1),323(a,1,1)),flip(a)].

given #214 (T,wt=14): 788 (x' @ y) * y' * x = x * y'.  [para(261(a,2),323(a,1,1))].

given #215 (T,wt=14): 975 x' @ y' * z' = x @ y * z.  [para(794(a,1),249(a,2)),rewrite(137(3))].

given #216 (T,wt=14): 976 x' @ y * z = x @ y' * z'.  [para(794(a,1),261(a,1)),rewrite(137(5))].

given #217 (A,wt=19): 176 x * (y @ z) * u * v = x * u * v * (y @ z).  [para(15(a,1),1(a,2,2)),rewrite(1(4))].

given #218 (T,wt=14): 1011 x' * y' @ z' = x * y @ z.  [para(797(a,1),249(a,2)),rewrite(137(2))].

given #219 (T,wt=14): 1012 x' * y' @ z = x * y @ z'.  [para(797(a,1),261(a,2)),rewrite(137(2))].

given #220 (T,wt=14): 1060 x' * (y @ z) = (z' @ y) * x'.  [para(235(a,1),137(a,1,1)),rewrite(137(4),138(3),138(7)),flip(a)].

given #221 (T,wt=14): 1089 x' * (y' @ z) = (z @ y) * x'.  [para(236(a,1),137(a,1,1)),rewrite(137(3),138(2),138(7)),flip(a)].

given #222 (A,wt=19): 179 (x @ y) * z * (u @ v) = (u @ v) * z * (x @ y).  [para(6(a,1),15(a,1,2))].

given #223 (T,wt=14): 1115 (x @ y) * x' = y * x' * y'.  [para(250(a,1),137(a,1,1)),rewrite(137(4),137(3),82(2),1(4),138(6)),flip(a)].

given #224 (T,wt=14): 1160 x' * (y @ z) = (z @ y') * x'.  [para(251(a,1),137(a,1,1)),rewrite(137(4),138(3),138(7)),flip(a)].

given #225 (T,wt=14): 1193 x' * (y @ z') = (z @ y) * x'.  [para(252(a,1),137(a,1,1)),rewrite(137(3),138(2),138(7)),flip(a)].

given #226 (T,wt=14): 1211 (x @ y) * x * y' * x' = y'.  [para(249(a,1),333(a,1,1)),rewrite(82(3))].

given #227 (A,wt=19): 180 (x @ y) * (z @ u) * v = v * (z @ u) * (x @ y).  [para(6(a,2),15(a,1,2))].

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

given #229 (T,wt=14): 1870 (x @ y) * (y @ z') = x * z @ y.  [back_rewrite(1044),rewrite(1868(8)),flip(a)].

given #230 (T,wt=14): 2379 x * y' @ z = (z @ y) * (x @ z).  [back_rewrite(583),rewrite(2350(8))].

given #231 (T,wt=14): 2381 x * y' @ z = (x @ z) * (z @ y).  [back_rewrite(314),rewrite(2350(8))].

given #232 (A,wt=15): 181 (x @ y) * z * u * (y @ x) = z * u.  [para(15(a,1),8(a,1,2)),rewrite(138(2))].

given #233 (T,wt=14): 2383 (x @ y) * (y' @ z) = x * z @ y.  [para(331(a,1),9(a,1,2,2,2)),rewrite(1868(8)),flip(a)].

given #234 (T,wt=14): 2618 x * (x @ y) * y' * x' = y'.  [para(221(a,1),671(a,2,2,1)),rewrite(137(2),1(4),3(3),31(3),137(4)),flip(a)].

given #235 (T,wt=14): 2674 x @ y * x' * z = x @ y * z.  [para(81(a,1),724(a,1,2,2)),flip(a)].

given #236 (T,wt=14): 2738 x @ y * z' = (z @ x) * (x @ y).  [para(218(a,1),736(a,2,1))].

given #237 (A,wt=25): 182 x' * y' * x * (z @ u) * y * v = (x @ y) * v * (z @ u).  [para(15(a,2),9(a,1,2,2,2))].

given #238 (T,wt=14): 2739 x @ y' * z = (x @ z) * (y @ x).  [para(218(a,1),736(a,2,2))].

given #239 (T,wt=14): 2787 (x @ y) * (z @ x') = x @ y * z.  [para(736(a,2),235(a,1)),flip(a)].

given #240 (T,wt=14): 2788 x @ y' * z = (y @ x) * (x @ z).  [para(736(a,2),235(a,2)),flip(a)].

given #241 (T,wt=14): 2789 x @ y * z' = (x @ y) * (z @ x).  [para(736(a,2),236(a,1))].

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

given #243 (T,wt=14): 2791 (x @ y) * (z' @ x) = x @ y * z.  [para(736(a,2),251(a,1)),flip(a)].

given #244 (T,wt=14): 2794 (x' @ y) * (y @ z) = y @ x * z.  [para(736(a,2),252(a,2))].

given #245 (T,wt=14): 2801 (x' @ y) * (x @ y * z) = x @ z.  [para(736(a,2),340(a,1,2))].

given #246 (T,wt=14): 2806 (x' @ y) * (x @ z * y) = x @ z.  [para(736(a,2),544(a,1,2))].

given #247 (A,wt=25): 185 x' * y' * x * y * z * (u @ v) = (u @ v) * (x @ y) * z.  [para(15(a,2),9(a,2))].

given #248 (T,wt=14): 3336 (x @ y') * (z @ x) = y * z @ x.  [para(218(a,2),1862(a,1,1))].

given #249 (T,wt=14): 3337 x' * y @ z = (z @ x) * (y @ z).  [para(220(a,1),1862(a,1,1)),flip(a)].

given #250 (T,wt=14): 3366 x' * y @ z = (y @ z) * (z @ x).  [para(1862(a,1),252(a,1))].

given #251 (T,wt=14): 3370 (x @ y') * (z * x @ y) = z @ y.  [para(1862(a,1),346(a,1,2))].

given #252 (A,wt=25): 186 (x @ y) * z' * u' * z * u * v = (z @ u) * v * (x @ y).  [para(9(a,2),15(a,1,2))].

given #253 (T,wt=14): 3374 (x @ y') * (x * z @ y) = z @ y.  [para(1862(a,1),545(a,1,2))].

given #254 (T,wt=14): 3581 x * y' * x' * (x @ y) = y'.  [para(113(a,2),340(a,1)),rewrite(82(2))].

given #255 (T,wt=14): 3692 x' @ y * z' = x @ z * y'.  [para(2218(a,1),218(a,1))].

given #256 (T,wt=14): 3693 x * y' @ z' = y * x' @ z.  [para(2218(a,2),218(a,2))].

given #257 (A,wt=25): 187 (x @ y) * z * (u @ v) = z * u' * v' * u * v * (x @ y).  [para(9(a,2),15(a,2,2))].

given #258 (T,wt=14): 3724 x' @ y * z' = x @ y' * z.  [para(2218(a,1),971(a,1))].

given #259 (T,wt=14): 3725 x' * y @ z' = x * y' @ z.  [para(2218(a,2),971(a,2))].

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

given #261 (T,wt=14): 3727 x' @ y' * z = x @ y * z'.  [para(2218(a,1),972(a,2))].

given #262 (A,wt=23): 188 (x @ y) * (z @ u) * v * w = v * (x @ y) * w * (z @ u).  [para(15(a,2),14(a,1,2))].

given #263 (T,wt=14): 3769 x' @ y' * z = x @ z' * y.  [para(2219(a,1),218(a,1))].

given #264 (T,wt=14): 3770 x' * y @ z' = y' * x @ z.  [para(2219(a,2),218(a,2))].

given #265 (T,wt=14): 4202 x * y @ y' * x = y * y @ x.  [para(4121(a,2),5(a,2)),rewrite(137(3),1(7),149(8))].

given #266 (T,wt=14): 4211 x' @ y * y = x' * x' @ y.  [para(4121(a,2),163(a,2)),rewrite(163(4))].

given #267 (A,wt=23): 189 (x @ y) * z * u * (v @ w) = z * (v @ w) * (x @ y) * u.  [para(15(a,2),14(a,2,2))].

given #268 (T,wt=14): 4306 x * y' @ y * x = x @ y * y.  [para(4206(a,1),5(a,2)),rewrite(82(2),137(2),1(7),154(8))].

given #269 (T,wt=14): 4543 x * y' @ y * y = x @ y * y.  [para(29(a,1),149(a,1,2,2,2)),rewrite(82(2),4539(7),82(6)),flip(a)].

given #270 (T,wt=14): 4546 x * x @ x' * y = x * x @ y.  [para(47(a,1),149(a,1,2)),rewrite(843(6),149(8),4202(4)),flip(a)].

given #271 (T,wt=14): 4759 x' * y @ x * x = y @ x * x.  [para(81(a,1),4623(a,1,1)),flip(a)].

given #272 (A,wt=23): 190 (x @ y) * z * (u @ v) * w = (u @ v) * z * w * (x @ y).  [para(14(a,1),15(a,1,2)),rewrite(1(9))].

given #273 (T,wt=14): 4788 x * x @ y * x' = x * x @ y.  [para(250(a,2),4662(a,1,2)),rewrite(177(4)),flip(a)].

given #274 (T,wt=14): 7531 x' * y @ y * x = y @ x * x.  [para(4202(a,1),138(a,1,1)),rewrite(138(3)),flip(a)].

given #275 (T,wt=14): 7536 x * y @ x' * y = x * x @ y.  [para(311(a,1),4202(a,1,1)),rewrite(137(4),138(3),1(5),195(6),1(9),1577(10),6(6),594(8))].

given #276 (T,wt=14): 7537 x * y @ y * x' = x * x @ y.  [para(311(a,1),4202(a,1,2)),rewrite(1(4),6(3),441(4),177(9))].

given #277 (A,wt=23): 191 (x @ y) * (z @ u) * v * w = v * (z @ u) * w * (x @ y).  [para(14(a,2),15(a,1,2)),rewrite(1(9))].

given #278 (T,wt=14): 7539 x * y @ x * y' = y * y @ x.  [para(4202(a,1),794(a,1)),flip(a)].

given #279 (T,wt=14): 7617 x * y' @ x * y = x @ y * y.  [para(311(a,1),4306(a,1,2)),rewrite(1(4),199(6),201(8))].

given #280 (T,wt=14): 7619 x' * y @ x * y = y @ x * x.  [para(4306(a,1),797(a,1)),flip(a)].

given #281 (T,wt=15): 199 x * (y @ z) * u @ v = x * u @ v.  [back_rewrite(107),rewrite(196(4)),flip(a)].

given #282 (A,wt=23): 192 (x @ y) * z * u * (v @ w) = (v @ w) * z * u * (x @ y).  [para(15(a,1),15(a,1,2)),rewrite(1(9))].

given #283 (T,wt=15): 217 x * y * z @ x * y = z @ x * y.  [para(1(a,1),174(a,1,1))].

given #284 (T,wt=15): 270 x * y @ x * y * z = x * y @ z.  [para(1(a,1),221(a,1,2))].

given #285 (T,wt=15): 312 x' * (x' @ y) = y' * x' * y.  [para(8(a,1),29(a,1,2)),rewrite(137(2),1(4),163(8)),flip(a)].

given #286 (T,wt=15): 330 x' * (x @ y') = y' * x' * y.  [para(261(a,1),29(a,2,2)),flip(a)].

given #287 (A,wt=23): 193 (x @ y) * (z @ u) * v * w = v * w * (z @ u) * (x @ y).  [para(15(a,2),15(a,1,2)),rewrite(1(9))].

given #288 (T,wt=15): 535 x * y * z' @ z = z' @ x * y.  [para(1(a,1),173(a,1,1))].

given #289 (T,wt=15): 539 x @ y * z * (u @ v) = x @ y * z.  [para(1(a,1),177(a,1,2))].

given #290 (T,wt=15): 548 x @ y * (z @ u) * v = x @ y * v.  [para(14(a,1),195(a,1,2))].

given #291 (T,wt=15): 594 x * y * (z @ u) @ v = x * y @ v.  [para(15(a,1),196(a,1,1))].

given #292 (A,wt=19): 223 x * y * (z @ u) * v = x * y * v * (z @ u).  [para(16(a,1),1(a,1)),rewrite(1(4)),flip(a)].

given #293 (T,wt=15): 637 x @ y * z * x' = y * z @ x'.  [para(1(a,1),267(a,1,2))].

given #294 (T,wt=15): 650 x' * y' * x = (y @ x') * y'.  [para(287(a,1),41(a,1,2,2)),rewrite(138(3),31(5),82(8),18(7),2(10)),flip(a)].

given #295 (T,wt=15): 661 x * y * (y @ x) * z = y * x * z.  [para(47(a,1),8(a,1,2)),rewrite(82(2))].

given #296 (T,wt=15): 688 x * y * z @ y' = x * z @ y'.  [para(47(a,1),174(a,1,1)),rewrite(199(5)),flip(a)].

given #297 (A,wt=25): 224 x' * y' * x * y * z * (u @ v) = (x @ y) * (u @ v) * z.  [para(16(a,1),9(a,1,2,2,2))].

given #298 (T,wt=15): 697 x' @ y * x * z = x' @ y * z.  [para(47(a,1),221(a,1,2)),rewrite(548(5)),flip(a)].

given #299 (T,wt=15): 740 x' * y' * x * (x' @ y) = y'.  [para(287(a,1),47(a,2,2)),rewrite(31(10))].

given #300 (T,wt=15): 761 x' * y' = y' * x' * (x @ y).  [para(249(a,1),311(a,1,2,2)),flip(a)].

given #301 (T,wt=15): 766 x * y * y * x = y * x * x * y.  [para(467(a,1),311(a,1,2,2)),rewrite(31(4),1(3),1(6))].

given #302 (A,wt=25): 225 x' * y' * x * y * (z @ u) * v = (x @ y) * v * (z @ u).  [para(16(a,2),9(a,1,2,2,2))].

given #303 (T,wt=15): 773 (x @ y) * y * x * z = x * y * z.  [para(323(a,1),1(a,1,1)),rewrite(1(2),1(5)),flip(a)].

given #304 (T,wt=15): 779 (x @ y) * z * y * x = z * x * y.  [para(323(a,1),14(a,2,2))].

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

% Proof 1 at 4.37 (+ 0.04) seconds: E.
% Length of proof is 31.
% Level of proof is 11.
% Maximum clause weight is 19.
% Given clauses 304.

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 = z * (x @ y).  [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))].
14 (x @ y) * z * u = z * (x @ y) * u.  [para(6(a,1),1(a,1,1)),rewrite(1(3)),flip(a)].
22 x'' * e = x.  [para(3(a,1),8(a,1,2))].
25 x'' * (x @ y) = y' * x * y.  [para(5(a,1),8(a,1,2))].
28 x'' * y = x * y.  [para(8(a,1),8(a,1,2))].
29 x' * y * x = y * (y @ x).  [back_rewrite(25),rewrite(28(4)),flip(a)].
31 x * e = x.  [back_rewrite(22),rewrite(28(4))].
47 x' * y * x * z = y * (y @ x) * z.  [para(9(a,1),8(a,1,2)),rewrite(28(5)),flip(a)].
68 (x * y)' * y * x = x * y @ x.  [para(8(a,1),10(a,1,2))].
70 x * y @ x = y @ x * y.  [para(9(a,1),10(a,1,2)),rewrite(8(3),6(4),8(5),8(5))].
74 (x * y)' * y * x = y @ x * y.  [back_rewrite(68),rewrite(70(6))].
76 x * x' = e.  [para(28(a,1),3(a,1))].
82 x'' = x.  [para(28(a,1),31(a,1)),rewrite(31(2)),flip(a)].
87 x * y * (x * y)' = e.  [para(76(a,1),1(a,1)),flip(a)].
122 x * (y * x)' = y'.  [para(87(a,1),8(a,1,2)),rewrite(31(3)),flip(a)].
137 (x * y)' = y' * x'.  [para(122(a,1),8(a,1,2)),flip(a)].
153 x @ y * x = x @ y.  [back_rewrite(74),rewrite(137(2),1(5),5(5)),flip(a)].
174 x * y @ x = y @ x.  [back_rewrite(70),rewrite(153(4))].
323 (x @ y) * y * x = x * y.  [para(174(a,1),29(a,2,2)),rewrite(1(3),8(4),6(4,R)),flip(a)].
661 x * y * (y @ x) * z = y * x * z.  [para(47(a,1),8(a,1,2)),rewrite(82(2))].
779 (x @ y) * z * y * x = z * x * y.  [para(323(a,1),14(a,2,2))].
8540 $F # answer(E).  [para(779(a,2),7(a,1,2,2)),rewrite(661(13)),xx(a)].

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

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

Given=304. Generated=160465. Kept=8538. proofs=1.
Usable=277. Sos=6155. Demods=1753. Limbo=3, Disabled=2109. Hints=0.
Weight_deleted=23076. Literals_deleted=0.
Forward_subsumed=128850. Back_subsumed=266.
Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0.
New_demodulators=2920 (5 lex), Back_demodulated=1837. Back_unit_deleted=0.
Demod_attempts=2863784. Demod_rewrites=565330.
Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0.
Nonunit_fsub_feature_tests=0. Nonunit_bsub_feature_tests=0.
Megabytes=6.86.
User_CPU=4.37, System_CPU=0.04, Wall_clock=4.

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

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

THEOREM PROVED

Exiting with 1 proof.

Process 21023 exit (max_proofs) Mon Mar 19 17:02:15 2007