============================== Prover9 ===============================
Prover9 (32) version August-2006A, August 2006.
Process 11348 was started by mccune on cleo.thornwood,
Sat Aug 12 20:59:46 2006
The command was "/home/mccune/bin/prover9 -f gt.in AE.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 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:
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 = 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 (F,wt=5): 11 e @ x = e.  [para(2(a,1),5(a,1,2,2)),rewrite(3(4),3(4)),flip(a)].

given #8 (F,wt=5): 19 x @ e = e.  [back_rewrite(17),rewrite(18(2)),flip(a)].

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

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

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

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

given #13 (F,wt=5): 29 x * e = x.  [back_rewrite(22),rewrite(26(4))].

given #14 (T,wt=4): 31 e' = e.  [para(29(a,1),3(a,1))].

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

given #16 (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 #17 (F,wt=9): 26 x'' * y = x * y.  [para(8(a,1),8(a,1,2))].

given #18 (F,wt=5): 55 x'' = x.  [para(26(a,1),29(a,1)),rewrite(29(2)),flip(a)].

given #19 (T,wt=6): 50 x * x' = e.  [para(26(a,1),3(a,1))].

given #20 (T,wt=6): 58 x @ x' = e.  [para(55(a,1),12(a,1,1))].

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

given #22 (F,wt=7): 74 x * x @ x = e.  [para(10(a,1),10(a,1,2)),rewrite(3(2),31(2),2(4),3(4),11(5))].

given #23 (F,wt=8): 54 x * x' * y = y.  [para(26(a,1),8(a,1))].

given #24 (T,wt=10): 59 x * y * (x * y)' = e.  [para(50(a,1),1(a,1)),flip(a)].

given #25 (T,wt=9): 83 x * (y * x)' = y'.  [para(59(a,1),8(a,1,2)),rewrite(29(3)),flip(a)].

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

given #27 (F,wt=8): 94 (x @ y)' = y @ x.  [para(9(a,2),83(a,1,2,1)),rewrite(93(7),93(5),93(3),93(2),1(5),55(7),1(6),1(5),55(8),1(7),1(6),1(5),5(6),54(4)),flip(a)].

given #28 (F,wt=9): 100 (x @ y) * (y @ x) = e.  [back_rewrite(85),rewrite(93(8),93(6),93(4),93(3),1(6),55(8),1(7),1(6),55(9),1(8),1(7),1(6),5(7),54(5))].

given #29 (T,wt=9): 104 x * y @ x = y @ x.  [back_rewrite(68),rewrite(93(2),1(5),5(5)),flip(a)].

given #30 (T,wt=9): 139 x @ y * x = x @ y.  [back_rewrite(123),rewrite(132(4)),flip(a)].

given #31 (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 #32 (F,wt=8): 157 x' @ y = y @ x.  [back_rewrite(153),rewrite(156(3))].

given #33 (F,wt=8): 158 x @ y' = y @ x.  [back_rewrite(150),rewrite(156(2)),flip(a)].

given #34 (T,wt=9): 148 x @ x * y = x @ y.  [para(104(a,1),94(a,1,1)),rewrite(94(2)),flip(a)].

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

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

given #37 (F,wt=9): 178 x' @ y' = x @ y.  [para(157(a,2),157(a,1))].

given #38 (F,wt=9): 190 x' @ y = x @ y'.  [para(158(a,1),157(a,1)),flip(a)].

given #39 (T,wt=10): 93 (x * y)' = y' * x'.  [para(83(a,1),8(a,1,2)),flip(a)].

given #40 (T,wt=10): 122 x * y @ y' = y @ x.  [back_rewrite(73),rewrite(104(5))].

given #41 (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(26(6))].

given #42 (F,wt=10): 126 x' @ y * x = y @ x.  [para(27(a,1),5(a,1,2,2)),rewrite(55(2),93(2),1(6),8(5),54(4)),flip(a)].

given #43 (F,wt=10): 145 x' * y @ x = y @ x.  [para(54(a,1),104(a,1,1)),flip(a)].

given #44 (T,wt=10): 147 x' * y * x @ y = e.  [para(27(a,2),104(a,1,1)),rewrite(18(6))].

given #45 (T,wt=10): 172 (x @ y) * (x @ y') = e.  [para(157(a,1),100(a,1,1))].

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

given #47 (F,wt=10): 173 (x @ y') * (x @ y) = e.  [para(157(a,1),100(a,1,2))].

given #48 (F,wt=10): 174 (x' @ y) * (x @ y) = e.  [para(157(a,2),100(a,1,1))].

given #49 (T,wt=10): 175 (x @ y) * (x' @ y) = e.  [para(157(a,2),100(a,1,2))].

given #50 (T,wt=10): 195 x @ y' * x * y = e.  [para(27(a,2),148(a,1,2)),rewrite(16(6))].

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

given #52 (F,wt=10): 285 x * y * x' @ y = e.  [para(55(a,1),147(a,1,1,1))].

given #53 (F,wt=10): 324 x @ y * x * y' = e.  [para(55(a,1),195(a,1,2,1))].

given #54 (T,wt=11): 111 x' @ x * y = x' @ y.  [back_rewrite(28),rewrite(93(2),1(4),53(5)),flip(a)].

given #55 (T,wt=11): 121 x * y' @ y = y' @ x.  [back_rewrite(75),rewrite(104(6))].

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

given #57 (F,wt=11): 129 (x @ y) * z * (y @ x) = z.  [para(16(a,1),27(a,2,2)),rewrite(94(2),29(6))].

given #58 (F,wt=11): 130 x * y * (y @ x) = y * x.  [para(27(a,1),8(a,1,2)),rewrite(55(2))].

given #59 (T,wt=11): 140 (x @ y) * (y @ x) * z = z.  [para(94(a,1),8(a,1,1))].

given #60 (T,wt=11): 142 x' * y * x @ y' = e.  [para(5(a,1),104(a,1,1)),rewrite(18(3)),flip(a)].

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

given #62 (F,wt=11): 143 x * y @ x' = y @ x'.  [para(8(a,1),104(a,1,1)),flip(a)].

given #63 (F,wt=11): 186 x @ x' * y = y @ x'.  [para(158(a,1),104(a,1))].

given #64 (T,wt=11): 192 x' @ y' * x * y = e.  [para(5(a,1),148(a,1,2)),rewrite(16(3)),flip(a)].

given #65 (T,wt=11): 203 x @ y * x' = y @ x'.  [para(156(a,1),158(a,1)),flip(a)].

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

given #67 (F,wt=11): 224 (x @ y') * (y @ x') = e.  [para(190(a,1),100(a,1,1))].

given #68 (F,wt=11): 225 (x' @ y) * (y' @ x) = e.  [para(190(a,2),100(a,1,1))].

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

given #70 (T,wt=11): 277 x * (x @ y) @ y = x @ y.  [para(27(a,1),145(a,1,1)),rewrite(156(5))].

given #71 (A,wt=14): 53 x * y' * x' * y = x' @ y.  [para(26(a,1),5(a,1))].

given #72 (F,wt=11): 278 x' * y' * x @ y = e.  [para(27(a,2),145(a,1,1)),rewrite(18(8))].

given #73 (F,wt=11): 288 x @ y' * x' * y = e.  [para(147(a,1),158(a,1)),flip(a)].

given #74 (T,wt=11): 355 (x @ y) * z = z * (x @ y).  [para(100(a,1),42(a,1,2,2)),rewrite(94(2),29(3),16(4),2(5))].

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

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

given #77 (F,wt=11): 415 x * y * x' @ y' = e.  [para(285(a,1),172(a,1,1)),rewrite(2(7))].

given #78 (F,wt=11): 416 x * y' * x' @ y = e.  [para(285(a,1),172(a,1,2)),rewrite(29(7))].

given #79 (T,wt=11): 426 x @ y * (y @ x) = x @ y.  [para(27(a,1),111(a,1,2)),rewrite(55(2),55(5),139(5))].

given #80 (T,wt=11): 438 (x @ y) * y * x = x * y.  [para(3(a,1),44(a,1,2,2)),rewrite(55(2),29(2),178(4)),flip(a)].

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

given #82 (F,wt=9): 781 x * y @ y * x = e.  [para(438(a,1),139(a,1,2)),rewrite(16(6))].

given #83 (F,wt=11): 530 x @ (y @ x) * z = x @ z.  [para(47(a,2),5(a,1,2,2)),rewrite(93(4),94(4),1(9),317(8),5(5)),flip(a)].

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

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

given #86 (A,wt=14): 60 x' * y' * x = (x @ y) * y'.  [para(50(a,1),9(a,1,2,2,2)),rewrite(29(4))].

given #87 (F,wt=11): 621 x' * y' @ y * x = e.  [para(229(a,1),94(a,1,1)),rewrite(31(2)),flip(a)].

given #88 (F,wt=11): 747 x' * y' @ x * y = e.  [back_rewrite(106),rewrite(742(12))].

given #89 (T,wt=11): 786 x * y @ x' * y' = e.  [para(438(a,1),122(a,1,1)),rewrite(93(3),16(8))].

given #90 (T,wt=11): 887 x @ (x @ y) * z = x @ z.  [para(54(a,1),530(a,1,2)),rewrite(94(3)),flip(a)].

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

given #92 (F,wt=11): 888 (x @ y) * z @ y = z @ y.  [para(530(a,1),94(a,1,1)),rewrite(94(2)),flip(a)].

given #93 (F,wt=11): 906 x @ y * (x @ z) = x @ y.  [para(129(a,1),530(a,1,2)),flip(a)].

given #94 (T,wt=11): 907 x @ y * (z @ x) = x @ y.  [para(130(a,1),530(a,1,2)),rewrite(16(5),29(5))].

given #95 (T,wt=11): 1007 x * y' @ x' * y = e.  [para(55(a,1),747(a,1,1,1))].

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

given #97 (F,wt=11): 1008 x' * y @ x * y' = e.  [para(55(a,1),747(a,1,1,2))].

given #98 (F,wt=11): 1241 (x @ y) * z @ u = z @ u.  [para(71(a,1),5(a,2)),rewrite(93(7),93(5),93(3),93(2),1(5),55(7),1(6),1(5),55(8),1(7),1(6),1(5),5(6),1(11),1(10),1(9),1(8),1(13),346(12),5(5)),flip(a)].

given #99 (T,wt=11): 1253 x @ (y @ z) * u = x @ u.  [para(71(a,2),94(a,1,1)),rewrite(1246(7),8(3),94(2)),flip(a)].

given #100 (T,wt=11): 1255 x @ y * (z @ u) = x @ y.  [para(71(a,2),139(a,1)),rewrite(1246(10),8(3),149(4),1241(6))].

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

given #102 (F,wt=11): 1271 x * (y @ z) @ u = x @ u.  [para(129(a,1),71(a,1,1,2,2,2)),rewrite(94(3),340(5),1241(3),16(3),2(5)),flip(a)].

given #103 (F,wt=11): 1360 x * y @ z = y * x @ z.  [para(438(a,1),1241(a,1,1))].

given #104 (T,wt=11): 1367 x @ y * z = x @ z * y.  [para(438(a,1),1253(a,1,2))].

given #105 (T,wt=12): 132 x' * (y @ z) * x = y @ z.  [para(18(a,1),27(a,2,2)),rewrite(29(7))].

given #106 (A,wt=24): 96 x' * y' * z * x * y * z' = y * x @ x' * z'.  [para(83(a,1),10(a,1,2,2,2)),rewrite(93(2),93(5),93(7),55(5),55(5),1(7),1(8),93(11))].

given #107 (F,wt=12): 138 (x @ y) * x' * y * x = y.  [para(27(a,2),27(a,1,2)),rewrite(94(2),16(7),29(7))].

given #108 (F,wt=12): 184 x * (y @ x) = y * x * y'.  [para(158(a,1),27(a,2,2)),rewrite(55(2)),flip(a)].

given #109 (T,wt=12): 208 x * (y @ x) = x * (x @ y').  [para(35(a,1),9(a,1,2,2)),rewrite(55(2),132(5),40(6)),flip(a)].

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

given #111 (A,wt=15): 101 x' * y' = (x @ y) * y' * x'.  [back_rewrite(84),rewrite(93(3)),flip(a)].

given #112 (F,wt=12): 296 x * (y @ z') = x * (z @ y).  [para(172(a,1),32(a,1,2,2,2,2)),rewrite(94(3),29(4),132(4),16(4),2(6)),flip(a)].

given #113 (F,wt=12): 304 (x' @ y) * x * y = y * x.  [para(139(a,1),40(a,2,2)),rewrite(93(2),145(4),1(7),130(7))].

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

given #115 (T,wt=12): 313 x * (y' @ z) = x * (z @ y).  [para(173(a,1),32(a,1,2,2,2,2)),rewrite(94(4),29(5),132(5),16(6),2(6))].

given #116 (A,wt=23): 102 x' * y' * z' * x * y * z = y * x @ x' * z.  [back_rewrite(80),rewrite(93(2),93(6),55(6),1(7),1(8))].

given #117 (F,wt=12): 315 (x' @ y) * (x @ y) * z = z.  [para(174(a,1),1(a,1,1)),rewrite(2(2)),flip(a)].

given #118 (F,wt=12): 317 (x @ y) * (x' @ y) * z = z.  [para(175(a,1),1(a,1,1)),rewrite(2(2)),flip(a)].

given #119 (T,wt=12): 342 (x' @ y) * z = (y @ x) * z.  [para(42(a,1),9(a,1)),rewrite(340(6))].

given #120 (T,wt=12): 386 (x @ y) * z = z * (y @ x').  [para(172(a,1),42(a,1,2,2)),rewrite(94(2),29(3),16(4),2(6))].

given #121 (A,wt=21): 103 x' * y' * z * y * x * z' = y * x @ z'.  [back_rewrite(72),rewrite(93(2),1(8))].

given #122 (F,wt=12): 390 (x' @ y) * z = z * (y @ x).  [para(173(a,1),42(a,1,2,2)),rewrite(94(3),29(4),16(6),2(6))].

given #123 (F,wt=12): 392 (x @ y') * z = z * (y @ x).  [para(174(a,1),42(a,1,2,2)),rewrite(94(3),29(4),16(6),2(6))].

given #124 (T,wt=12): 393 (x @ y) * z = z * (y' @ x).  [para(175(a,1),42(a,1,2,2)),rewrite(94(2),29(3),16(4),2(6))].

given #125 (T,wt=12): 445 (x @ y') * z = (y @ x) * z.  [para(44(a,1),9(a,1,2)),rewrite(340(6))].

given #126 (A,wt=23): 105 x * y' * z' * x' * y * z = y * x' @ x * z.  [back_rewrite(67),rewrite(93(3),55(2),93(4),1(7),1(8))].

given #127 (F,wt=12): 486 (x @ y) * z * (x @ y') = z.  [para(157(a,1),129(a,1,1))].

given #128 (F,wt=12): 487 (x @ y') * z * (x @ y) = z.  [para(157(a,1),129(a,1,2,2))].

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

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

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

given #132 (F,wt=12): 501 x * y * (x' @ y) = y * x.  [para(157(a,2),130(a,1,2,2))].

given #133 (F,wt=12): 503 x * y * (x @ y') = y * x.  [para(158(a,2),130(a,1,2,2))].

given #134 (T,wt=12): 692 x * (y @ z) * x' = y @ z.  [para(355(a,2),54(a,1,2))].

given #135 (T,wt=12): 784 (x @ y') * x * y = y * x.  [para(158(a,2),438(a,1,1))].

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

given #137 (F,wt=12): 1273 x' * y * x @ z = y @ z.  [para(130(a,1),71(a,1,1,2,2,2)),rewrite(1246(7),1241(9),1271(7))].

given #138 (F,wt=12): 1275 x * y * x' @ z = y @ z.  [para(52(a,1),71(a,1,1,2,2,2)),rewrite(55(3),1246(7),1271(4),1241(8)),flip(a)].

given #139 (T,wt=12): 1336 x @ y' * z * y = x @ z.  [back_rewrite(1072),rewrite(1255(7))].

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

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

given #142 (F,wt=11): 2439 x * x @ y = x @ y * y.  [back_rewrite(1787),rewrite(2412(4))].

given #143 (F,wt=12): 1461 x * y @ z' = z @ y * x.  [para(1360(a,1),158(a,1))].

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

given #145 (T,wt=12): 2461 x' @ y * y = y @ x * x.  [para(2439(a,1),157(a,2))].

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

given #147 (F,wt=12): 2463 x * x @ y' = y * y @ x.  [para(2439(a,2),158(a,2))].

given #148 (F,wt=13): 136 x * (x @ y') = y * x * y'.  [para(55(a,1),27(a,1,1)),flip(a)].

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

given #150 (T,wt=13): 171 x' * y * x = y * (x' @ y).  [para(157(a,2),27(a,2,2))].

given #151 (A,wt=15): 131 x' * (x' @ y) = y' * x' * y.  [para(8(a,1),27(a,1,2)),rewrite(93(2),1(4),111(8)),flip(a)].

given #152 (F,wt=13): 185 x' * y * x = y * (x @ y').  [para(158(a,2),27(a,2,2))].

given #153 (F,wt=13): 198 x * y * z @ z = x * y @ z.  [para(1(a,1),156(a,1,1))].

given #154 (T,wt=13): 216 x * y * x' * y' = x @ y.  [para(178(a,1),5(a,2)),rewrite(55(2),55(2))].

given #155 (T,wt=13): 223 x * (x' @ y) = y * x * y'.  [para(190(a,2),27(a,2,2)),rewrite(55(2)),flip(a)].

given #156 (A,wt=21): 133 x' * y * x * z * (z @ y) = (x @ y') * z * y.  [para(27(a,1),9(a,1,2,2,2)),rewrite(55(3))].

given #157 (F,wt=13): 231 x' * y' @ z = z @ y * x.  [para(93(a,1),157(a,1,1))].

given #158 (F,wt=13): 232 x * y @ z = z @ y' * x'.  [para(93(a,1),158(a,1,2)),flip(a)].

given #159 (T,wt=13): 349 x' * y = y * (y @ x) * x'.  [para(50(a,1),42(a,1,2,2)),rewrite(29(3))].

given #160 (T,wt=13): 474 (x' @ y) * z = (x @ y') * z.  [para(44(a,1),42(a,1,2)),rewrite(340(6),340(9)),flip(a)].

given #161 (A,wt=18): 135 x' * y' * z' * y * z * x = y @ z.  [para(9(a,2),27(a,1,2)),rewrite(18(11),29(11))].

given #162 (F,wt=13): 490 (x @ y') * z * (y @ x') = z.  [para(190(a,1),129(a,1,1))].

given #163 (F,wt=13): 491 (x' @ y) * z * (y' @ x) = z.  [para(190(a,2),129(a,1,1))].

given #164 (T,wt=13): 500 x * y' * (x @ y) = y' * x.  [para(157(a,1),130(a,1,2,2))].

given #165 (T,wt=13): 502 x' * y * (x @ y) = y * x'.  [para(158(a,1),130(a,1,2,2))].

given #166 (A,wt=15): 141 x * y * z @ x * y = z @ x * y.  [para(1(a,1),104(a,1,1))].

given #167 (F,wt=13): 519 (x @ y') * (y @ x') * z = z.  [para(190(a,1),140(a,1,1))].

given #168 (F,wt=13): 520 (x' @ y) * (y' @ x) * z = z.  [para(190(a,2),140(a,1,1))].

given #169 (T,wt=13): 604 x * (y' @ z) = x * (y @ z').  [para(224(a,1),32(a,1,2,2,2,2)),rewrite(94(4),29(5),132(5),16(6),2(7))].

given #170 (T,wt=13): 607 (x' @ y) * z = z * (x @ y').  [para(224(a,1),42(a,1,2,2)),rewrite(94(3),29(4),16(6),2(7))].

given #171 (A,wt=25): 159 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 #172 (F,wt=13): 612 (x @ y') * z = z * (x' @ y).  [para(225(a,1),42(a,1,2,2)),rewrite(94(3),29(4),16(6),2(7))].

given #173 (F,wt=13): 696 x' * (y @ z) = (y @ z) * x'.  [para(355(a,1),93(a,1,1)),rewrite(93(3),94(2),94(6)),flip(a)].

given #174 (T,wt=13): 782 x' * y = (y @ x) * y * x'.  [para(157(a,1),438(a,1,1)),flip(a)].

given #175 (T,wt=13): 783 (x @ y) * x' * y = y * x'.  [para(158(a,1),438(a,1,1))].

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

given #177 (F,wt=13): 846 x * y * z @ z * x * y = e.  [para(1(a,1),781(a,1,1))].

given #178 (F,wt=13): 847 x * y * z @ y * z * x = e.  [para(1(a,1),781(a,1,2))].

given #179 (T,wt=13): 1310 x * y @ y * (z @ u) * x = e.  [back_rewrite(856),rewrite(1246(11),8(4))].

given #180 (T,wt=13): 1318 x * y * z @ y = x * z @ y.  [back_rewrite(381),rewrite(1247(4)),flip(a)].

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

given #182 (F,wt=13): 1455 (x * y @ z) * (z @ y * x) = e.  [para(1360(a,1),100(a,1,1))].

given #183 (F,wt=13): 1456 (x @ y * z) * (z * y @ x) = e.  [para(1360(a,1),100(a,1,2))].

given #184 (T,wt=13): 1462 x * y @ z = z @ x' * y'.  [para(1360(a,1),158(a,2)),rewrite(93(2)),flip(a)].

given #185 (T,wt=13): 1497 x' * y' @ z = z @ x * y.  [para(1367(a,1),157(a,2)),rewrite(93(2))].

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

given #187 (F,wt=13): 1522 x @ y * x * z = x @ y * z.  [back_rewrite(428),rewrite(1520(4)),flip(a)].

given #188 (F,wt=13): 2135 (x * y @ z) * (z @ y) = x @ z.  [para(130(a,1),108(a,1,2,2,2,2)),rewrite(135(8)),flip(a)].

given #189 (T,wt=13): 2413 (x @ y) * (y @ x * z) = y @ z.  [para(42(a,2),112(a,1,2,2,2)),rewrite(94(2),228(9),1271(7))].

given #190 (T,wt=13): 2424 (x @ y) * (y * z @ x) = z @ x.  [para(138(a,1),112(a,1,2,2,2,2)),rewrite(94(2),93(6),93(4),55(7),1(6),1(8),1(7),112(9),1336(10),1271(7))].

given #191 (A,wt=18): 165 x * y' * z' * y = x * (y @ z) * z'.  [para(50(a,1),32(a,1,2,2,2,2)),rewrite(29(4))].

given #192 (F,wt=13): 2441 (x @ y) * (z @ y) = x * z @ y.  [back_rewrite(1595),rewrite(2415(6)),flip(a)].

given #193 (F,wt=13): 2460 x' * x' @ y = y * y @ x.  [para(2439(a,2),157(a,1))].

given #194 (T,wt=13): 2462 x @ y' * y' = y @ x * x.  [para(2439(a,1),158(a,1))].

given #195 (T,wt=13): 2600 x' @ y * y = x * x @ y'.  [para(2461(a,2),158(a,2)),flip(a)].

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

given #197 (F,wt=13): 2809 x * x @ y * x = x @ y * y.  [para(149(a,1),2439(a,2)),rewrite(1(5),1522(6))].

given #198 (F,wt=13): 3026 x * y' @ z = z @ y * x'.  [para(55(a,1),231(a,1,1,1))].

given #199 (T,wt=13): 3027 x' * y @ z = z @ y' * x.  [para(55(a,1),231(a,1,1,2))].

given #200 (T,wt=13): 3169 x' * y @ z = z @ x * y'.  [para(349(a,1),231(a,2,2)),rewrite(55(3),1520(8))].

given #201 (A,wt=25): 167 x * y' * z * y * u * (u @ z) = x * (y @ z') * u * z.  [para(27(a,1),32(a,1,2,2,2,2)),rewrite(55(3))].

given #202 (F,wt=13): 3170 x * y' @ z = z @ x' * y.  [para(349(a,2),231(a,2,2)),rewrite(93(4),55(2),94(2),1(4),1247(5))].

given #203 (F,wt=13): 3217 (x @ y) * (z * y @ x) = z @ x.  [para(130(a,1),135(a,1,2,2,2,2)),rewrite(93(3),94(2),1(10),112(9))].

given #204 (T,wt=13): 3372 x * y @ y * y = x @ y * y.  [para(141(a,1),2439(a,1)),rewrite(1(2),1522(3),1(5),1(7),1(8),1(7),191(9),2791(7)),flip(a)].

given #205 (T,wt=13): 3703 x * y * z @ y * x * z = e.  [para(130(a,1),846(a,1,1,2)),rewrite(1(6),1520(7))].

given #206 (A,wt=17): 168 (x @ y) * z = y * x' * y' * x * z.  [para(157(a,1),9(a,2,1)),rewrite(55(2)),flip(a)].

given #207 (F,wt=13): 3840 x * y * z @ z * y * x = e.  [para(438(a,1),1310(a,1,2,2)),rewrite(1(2))].

given #208 (F,wt=13): 4223 (x @ y * z) * (y @ x) = x @ z.  [para(2135(a,1),8(a,1,2)),rewrite(94(3))].

given #209 (T,wt=13): 4233 (x @ y) * (y @ z * x) = y @ z.  [para(2135(a,1),93(a,1,1)),rewrite(94(2),94(3),94(5)),flip(a)].

given #210 (T,wt=13): 4308 (x @ y) * (x @ z) = x @ y * z.  [para(2413(a,1),8(a,1,2)),rewrite(94(2))].

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

given #212 (F,wt=13): 4881 x * x @ y * x = x * x @ y.  [para(2809(a,2),5(a,2)),rewrite(93(3),1(7),102(8),2423(4)),flip(a)].

given #213 (F,wt=13): 4886 x * y @ x * x = y @ x * x.  [para(2809(a,2),156(a,1)),rewrite(1(5),1(4),198(9),1463(5))].

given #214 (T,wt=13): 5377 x * x @ x * y = x * x @ y.  [para(3372(a,1),2413(a,1,1)),rewrite(1(5),2413(7))].

given #215 (T,wt=13): 5400 x * y * z @ x * z * y = e.  [para(438(a,1),3703(a,1,1,2)),rewrite(1253(7))].

given #216 (A,wt=14): 170 x' * (y @ x) = y' * x' * y.  [para(157(a,1),27(a,2,2)),flip(a)].

given #217 (F,wt=14): 197 x' * y' * x * (y @ x) = y'.  [back_rewrite(128),rewrite(192(6),29(3)),flip(a)].

given #218 (F,wt=14): 211 x' * (y @ x) = x' * (x @ y').  [para(35(a,1),27(a,1,2)),rewrite(93(2),1(7),132(6),126(8)),flip(a)].

given #219 (T,wt=14): 218 x' * (x @ y) = y * x' * y'.  [para(178(a,1),27(a,2,2)),rewrite(55(2)),flip(a)].

given #220 (T,wt=14): 235 x' * y' @ z = y * x @ z'.  [para(93(a,1),190(a,1,1))].

given #221 (A,wt=21): 176 x * (y @ z) * u = x * z * y' * z' * y * u.  [para(157(a,1),32(a,2,2,1)),rewrite(55(2)),flip(a)].

given #222 (F,wt=14): 236 x' @ y * z = x @ z' * y'.  [para(93(a,1),190(a,2,2))].

given #223 (F,wt=14): 237 x * y * z @ z' = z @ x * y.  [para(1(a,1),122(a,1,1))].

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

given #225 (T,wt=14): 439 (x @ y) * y' * x' * y = x'.  [para(3(a,1),44(a,1,2)),rewrite(29(3),93(3),93(5),55(3),55(3),148(3),93(4),1(6)),flip(a)].

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

given #227 (F,wt=14): 449 x' * y = (x @ y') * y * x'.  [para(50(a,1),44(a,1,2,2)),rewrite(29(3))].

given #228 (F,wt=14): 506 x * y' * (y @ x') = y' * x.  [para(190(a,1),130(a,1,2,2))].

given #229 (T,wt=14): 507 x' * y * (y' @ x) = y * x'.  [para(190(a,2),130(a,1,2,2))].

given #230 (T,wt=14): 785 (x' @ y) * y' * x = x * y'.  [para(190(a,2),438(a,1,1))].

given #231 (A,wt=19): 180 (x @ y) * x * y * z = x * y * (x @ y) * z.  [back_rewrite(46),rewrite(178(3))].

given #232 (F,wt=14): 965 (x @ y) * x' = y * x' * y'.  [para(157(a,1),60(a,2,1)),rewrite(55(2)),flip(a)].

given #233 (F,wt=14): 1058 x * y * z @ y' = y @ x * z.  [para(44(a,2),887(a,1,2)),rewrite(186(5))].

given #234 (T,wt=14): 1405 x' * (y @ z') = (z @ y) * x'.  [para(172(a,1),78(a,1,2,2)),rewrite(94(2),29(4),18(5),2(9)),flip(a)].

given #235 (T,wt=14): 1406 x' * (y' @ z) = (z @ y) * x'.  [para(175(a,1),78(a,1,2,2)),rewrite(94(2),29(4),18(5),2(9)),flip(a)].

given #236 (A,wt=17): 182 x' * y * x * y' * z = (y @ x) * z.  [para(158(a,1),9(a,2,1)),rewrite(55(3))].

given #237 (F,wt=14): 1464 x' * y' @ z' = x * y @ z.  [para(1360(a,1),178(a,2)),rewrite(93(2))].

given #238 (F,wt=14): 1465 x' * y' @ z = x * y @ z'.  [para(1360(a,1),190(a,2)),rewrite(93(2))].

given #239 (T,wt=14): 1499 x' @ y' * z' = x @ y * z.  [para(1367(a,1),178(a,2)),rewrite(93(3))].

given #240 (T,wt=14): 1500 x' @ y * z = x @ y' * z'.  [para(1367(a,1),190(a,1)),rewrite(93(5))].

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

given #242 (F,wt=14): 1573 (x @ y) * x * y' * x' = y'.  [para(178(a,1),138(a,1,1)),rewrite(55(3))].

given #243 (F,wt=14): 1675 x * (x @ y) * y' * x' = y'.  [para(101(a,1),8(a,1,2)),rewrite(55(2))].

given #244 (T,wt=12): 6859 x * (y @ x) * y * x' = y.  [para(158(a,1),1675(a,1,2,1)),rewrite(55(3),55(7))].

given #245 (T,wt=14): 1775 x * y' @ y * y = x @ y * y.  [para(27(a,1),102(a,1,2,2,2)),rewrite(55(2),1771(7),55(6)),flip(a)].

given #246 (A,wt=21): 188 x * y' * z * y * z' * u = x * (z @ y) * u.  [para(158(a,1),32(a,2,2,1)),rewrite(55(3))].

given #247 (F,wt=14): 1786 (x @ y') * (x * z @ y) = z @ y.  [para(42(a,2),102(a,1,2,2)),rewrite(94(3),112(10),94(11),355(11),1255(12),1271(9))].

given #248 (F,wt=14): 1789 (x' @ y) * (x @ y * z) = x @ z.  [para(44(a,2),102(a,1,2,2,2)),rewrite(94(3),228(10),94(11),1253(12),1271(9))].

given #249 (T,wt=14): 1877 x' * (y @ z) = (z' @ y) * x'.  [para(386(a,1),93(a,1,1)),rewrite(93(4),94(3),94(7)),flip(a)].

given #250 (T,wt=14): 2001 x' * (y @ z) = (z @ y') * x'.  [para(393(a,1),93(a,1,1)),rewrite(93(4),94(3),94(7)),flip(a)].

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

given #252 (F,wt=14): 2062 x * y' @ y * x = x @ y * y.  [para(184(a,2),105(a,1,2,2,2)),rewrite(55(3),2049(8),55(8),1775(8))].

given #253 (F,wt=14): 2102 x * y' * x' * (x @ y) = y'.  [para(488(a,1),78(a,2)),rewrite(55(2))].

given #254 (T,wt=14): 2181 x' * y = y * (x @ y') * x'.  [para(386(a,2),501(a,1,2)),flip(a)].

given #255 (T,wt=14): 2412 (x' @ y) * (z @ x) = y * z @ x.  [para(42(a,1),112(a,1,2)),rewrite(2055(8))].

given #256 (A,wt=15): 191 x * y @ x * y * z = x * y @ z.  [para(1(a,1),148(a,1,2))].

given #257 (F,wt=14): 2423 x * y @ y' * x = y * y @ x.  [para(66(a,1),112(a,1,2)),rewrite(156(8),126(6),355(5,R),1400(6),355(4),1544(7),1(6),1318(7))].

given #258 (F,wt=14): 2428 x * x @ x' * y = x * x @ y.  [para(112(a,1),102(a,1)),flip(a)].

given #259 (T,wt=14): 2471 x' @ y * y = x' * x' @ y.  [para(2439(a,2),111(a,2)),rewrite(111(4))].

given #260 (T,wt=14): 2748 (x @ y) * (y @ z') = x * z @ y.  [para(136(a,1),9(a,1,2,2,2)),rewrite(2442(8)),flip(a)].

given #261 (A,wt=17): 217 (x @ y) * z = x * y * x' * y' * z.  [para(178(a,1),9(a,2,1)),rewrite(55(2),55(2)),flip(a)].

given #262 (F,wt=14): 2752 (x @ y') * (y @ z) = y @ x * z.  [para(136(a,1),56(a,1,2,2,2)),rewrite(1563(8),178(7)),flip(a)].

given #263 (F,wt=14): 2955 (x @ y) * (y' @ z) = x * z @ y.  [para(216(a,1),78(a,2,2)),rewrite(55(4),2442(8)),flip(a)].

given #264 (T,wt=14): 3023 x' * y @ z = (y @ z) * (z @ x).  [para(216(a,1),133(a,2,2)),rewrite(1491(10),58(7),29(7),1(7),1(6),2410(8),93(8),93(7),55(5),55(5),1(6),1491(7))].

given #265 (T,wt=14): 3230 (x @ y') * (z * x @ y) = z @ y.  [para(501(a,1),135(a,1,2,2,2,2)),rewrite(93(4),94(3),1(11),112(10))].

given #266 (A,wt=21): 219 x * (y @ z) * u = x * y * z * y' * z' * u.  [para(178(a,1),32(a,2,2,1)),rewrite(55(2),55(2)),flip(a)].

given #267 (F,wt=14): 3859 x * y' * z @ y = x * z @ y.  [para(54(a,1),1318(a,1,1,2)),flip(a)].

given #268 (F,wt=14): 3914 x' * y @ z' = x * y' @ z.  [back_rewrite(2815),rewrite(3862(8)),flip(a)].

given #269 (T,wt=14): 3916 x' * y @ z = x * y' @ z'.  [back_rewrite(2446),rewrite(3862(8))].

given #270 (T,wt=14): 4228 (x @ y) * (x' @ z * y) = z @ x.  [para(157(a,2),2135(a,1,1)),rewrite(355(5,R))].

given #271 (A,wt=18): 220 (x @ y') * z = x * y' * x' * y * z.  [para(190(a,1),9(a,2,1)),rewrite(55(2)),flip(a)].

given #272 (F,wt=14): 4260 x * y' @ z = (z @ y) * (x @ z).  [para(2135(a,1),486(a,1,2)),flip(a)].

given #273 (F,wt=14): 4309 (x' @ y) * (y @ z) = y @ x * z.  [para(8(a,1),2413(a,1,2,2))].

given #274 (T,wt=14): 4311 x @ y' * z = (y @ x) * (x @ z).  [para(54(a,1),2413(a,1,2,2)),flip(a)].

given #275 (T,wt=14): 4333 x @ y * z' = (z @ x) * (x @ y).  [para(184(a,2),2413(a,1,2,2)),rewrite(1255(4)),flip(a)].

given #276 (A,wt=18): 221 x' * y * x * y' * z = (x' @ y) * z.  [para(190(a,2),9(a,2,1)),rewrite(55(3))].

given #277 (F,wt=14): 4375 (x @ y') * (z @ x) = y * z @ x.  [para(8(a,1),2424(a,1,2,1))].

given #278 (F,wt=14): 4377 x' * y @ z = (z @ x) * (y @ z).  [para(54(a,1),2424(a,1,2,1)),flip(a)].

given #279 (T,wt=14): 4494 x * y' @ z = (x @ z) * (z @ y).  [para(157(a,1),2441(a,1,2)),flip(a)].

given #280 (T,wt=14): 4888 x' * y @ x * y = y @ x * x.  [para(2809(a,1),145(a,2)),rewrite(93(2),1(5),1246(7))].

given #281 (A,wt=15): 222 x' * (x @ y') = y' * x' * y.  [para(190(a,1),27(a,2,2)),flip(a)].

given #282 (F,wt=14): 4911 x * y' @ z' = y * x' @ z.  [para(3026(a,2),5(a,2)),rewrite(93(4),55(3),1(7),1533(8))].

given #283 (F,wt=14): 4915 x' @ y * z' = x @ z * y'.  [para(3026(a,1),157(a,2))].

given #284 (T,wt=14): 4955 x' @ y' * z = x @ y * z'.  [para(3026(a,1),1460(a,2))].

given #285 (T,wt=14): 4958 x' @ y * z' = x @ y' * z.  [para(3026(a,1),1461(a,1))].

given #286 (A,wt=22): 226 x * (y @ z') * u = x * y * z' * y' * z * u.  [para(190(a,1),32(a,2,2,1)),rewrite(55(2)),flip(a)].

given #287 (F,wt=14): 4997 x' * y @ z' = y' * x @ z.  [para(3027(a,2),5(a,2)),rewrite(93(4),55(4),1(7),1768(8))].

given #288 (F,wt=14): 5000 x' @ y' * z = x @ z' * y.  [para(3027(a,1),157(a,2))].

given #289 (T,wt=14): 5363 x' * y @ x * x = y @ x * x.  [para(3372(a,1),145(a,2)),rewrite(93(2),1(5),2942(7))].

given #290 (T,wt=14): 5464 x @ y * z' = (x @ y) * (z @ x).  [para(208(a,1),168(a,2,2,2,2)),rewrite(4210(11)),flip(a)].

given #291 (A,wt=22): 227 x * y' * z * y * z' * u = x * (y' @ z) * u.  [para(190(a,2),32(a,2,2,1)),rewrite(55(3))].

given #292 (F,wt=14): 5578 x @ y' * z = (x @ z) * (y @ x).  [para(54(a,1),4223(a,1,1,2)),flip(a)].

given #293 (F,wt=14): 5579 (x @ y) * (z' @ x) = x @ y * z.  [para(27(a,1),4223(a,1,1,2)),rewrite(1255(3))].

given #294 (T,wt=14): 6030 x * x @ y * x' = x * x @ y.  [para(184(a,2),5377(a,1,2)),rewrite(1255(4)),flip(a)].

given #295 (T,wt=14): 6916 x * y' @ x * y = x @ y * y.  [para(1775(a,1),148(a,2)),rewrite(1(6),8(5))].

given #296 (A,wt=20): 228 x' * y' * z' * x * z * y = x @ z * y.  [para(93(a,1),5(a,1,2,1)),rewrite(1(7))].

given #297 (F,wt=14): 6997 x * y @ y * x' = x * x @ y.  [para(2062(a,1),94(a,1,1)),rewrite(94(3)),flip(a)].

given #298 (F,wt=14): 7005 x' * y @ y * x = y @ x * x.  [para(501(a,1),2062(a,1,2)),rewrite(1(5),355(4),130(5),1271(9))].

given #299 (T,wt=14): 7162 x * y @ x' * y = x * x @ y.  [para(130(a,1),2423(a,1,1)),rewrite(93(4),94(3),1(5),1253(6),1(9),3876(10),1437(8))].

given #300 (T,wt=14): 7164 x * y @ x * y' = y * y @ x.  [para(2423(a,1),1367(a,1)),flip(a)].

given #301 (A,wt=19): 230 x' * y' * z * y * x = z * (z @ y * x).  [para(93(a,1),27(a,1,1)),rewrite(1(6))].

given #302 (F,wt=15): 337 (x @ y) * z * (y @ x) * u = z * u.  [para(16(a,1),42(a,2,2,1)),rewrite(94(2),2(7))].

given #303 (F,wt=15): 338 x * y * (y @ x) * z = y * x * z.  [para(42(a,1),8(a,1,2)),rewrite(55(2))].

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

given #305 (T,wt=15): 443 (x @ y) * y * x * z = x * y * z.  [para(8(a,1),44(a,1,2,2)),rewrite(55(2),178(5)),flip(a)].

given #306 (A,wt=17): 242 x * y * z @ z' * y' = y * z @ x.  [para(93(a,1),122(a,1,2))].

given #307 (F,wt=15): 482 (x @ y) * z * u * (y @ x) = z * u.  [para(1(a,1),129(a,1,2))].

given #308 (F,wt=15): 485 x * (y @ z) * u = x * u * (y @ z).  [para(129(a,1),32(a,1,2,2,2,2)),rewrite(94(3),340(5),16(5),2(7))].

given #309 (T,wt=15): 492 (x @ y) * z * u = z * u * (x @ y).  [para(129(a,1),42(a,1,2,2)),rewrite(94(2),16(5),2(7))].

given #310 (T,wt=15): 505 x' * y' = y' * x' * (x @ y).  [para(178(a,1),130(a,1,2,2)),flip(a)].

given #311 (A,wt=21): 250 (x @ y) * z' * y * z = x * y * x' * (y @ z).  [para(55(a,1),38(a,1,1)),rewrite(178(8)),flip(a)].

given #312 (F,wt=15): 521 (x @ y) * z * u = z * (x @ y) * u.  [para(140(a,1),42(a,1,2,2)),rewrite(94(2),16(5),2(7))].

given #313 (F,wt=15): 586 x @ y * z * x' = y * z @ x'.  [para(1(a,1),203(a,1,2))].

given #314 (T,wt=15): 596 (x @ y') * y * x' * y' = x'.  [para(52(a,1),27(a,1,2)),rewrite(93(4),93(3),55(2),1(4),355(7,R),409(13),29(10))].

given #315 (T,wt=15): 611 x' * y' * x = (y @ x') * y'.  [para(225(a,1),38(a,1,2,2)),rewrite(94(3),29(5),55(8),18(7),2(10)),flip(a)].

given #316 (A,wt=23): 264 x' * y' * x * (y @ z) = (x @ y) * z * y' * z'.  [para(178(a,1),38(a,1,2,2,2)),rewrite(55(8),55(9))].

given #317 (F,wt=15): 674 x' @ y * x * z = x' @ y * z.  [back_rewrite(461),rewrite(667(6)),flip(a)].

given #318 (F,wt=15): 753 x' * (y' @ x) = y * x' * y'.  [para(416(a,1),27(a,2,2)),rewrite(1(6),1(5),53(6),29(10))].

given #319 (T,wt=15): 787 (x @ y) * z * y * x = z * x * y.  [para(438(a,1),42(a,1,2,2)),rewrite(94(2),16(6),2(7))].

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

% Proof 1 at 4.44 (+ 0.03) seconds: E.
% Length of proof is 42.
% Level of proof is 15.
% Maximum clause weight is 19.
% Given clauses 319.

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 @ z) = e.  [para(11(a,1),6(a,1,1)),rewrite(11(2)),flip(a)].
18 (x @ y) @ z = e.  [para(11(a,1),6(a,2))].
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))].
26 x'' * y = x * y.  [para(8(a,1),8(a,1,2))].
27 x' * y * x = y * (y @ x).  [back_rewrite(25),rewrite(26(4)),flip(a)].
29 x * e = x.  [back_rewrite(22),rewrite(26(4))].
42 x' * y * x * z = y * (y @ x) * z.  [para(9(a,1),8(a,1,2)),rewrite(26(5)),flip(a)].
44 x' * y * x * z = (x @ y') * y * z.  [para(8(a,1),9(a,1,2,2,2)),rewrite(26(5))].
50 x * x' = e.  [para(26(a,1),3(a,1))].
54 x * x' * y = y.  [para(26(a,1),8(a,1))].
55 x'' = x.  [para(26(a,1),29(a,1)),rewrite(29(2)),flip(a)].
59 x * y * (x * y)' = e.  [para(50(a,1),1(a,1)),flip(a)].
68 (x * y)' * y * x = x * y @ x.  [para(8(a,1),10(a,1,2))].
70 x' * (y * x @ y) * x = x @ y * x.  [para(9(a,1),10(a,1,2)),rewrite(8(3),8(8))].
83 x * (y * x)' = y'.  [para(59(a,1),8(a,1,2)),rewrite(29(3)),flip(a)].
93 (x * y)' = y' * x'.  [para(83(a,1),8(a,1,2)),flip(a)].
94 (x @ y)' = y @ x.  [para(9(a,2),83(a,1,2,1)),rewrite(93(7),93(5),93(3),93(2),1(5),55(7),1(6),1(5),55(8),1(7),1(6),1(5),5(6),54(4)),flip(a)].
104 x * y @ x = y @ x.  [back_rewrite(68),rewrite(93(2),1(5),5(5)),flip(a)].
123 x' * (x @ y) * x = x @ y * x.  [back_rewrite(70),rewrite(104(3))].
132 x' * (y @ z) * x = y @ z.  [para(18(a,1),27(a,2,2)),rewrite(29(7))].
139 x @ y * x = x @ y.  [back_rewrite(123),rewrite(132(4)),flip(a)].
145 x' * y @ x = y @ x.  [para(54(a,1),104(a,1,1)),flip(a)].
153 x' * y @ y = y @ x.  [para(54(a,1),139(a,1,2)),rewrite(145(6))].
156 x * y @ y = x @ y.  [para(139(a,1),94(a,1,1)),rewrite(94(2)),flip(a)].
157 x' @ y = y @ x.  [back_rewrite(153),rewrite(156(3))].
178 x' @ y' = x @ y.  [para(157(a,2),157(a,1))].
338 x * y * (y @ x) * z = y * x * z.  [para(42(a,1),8(a,1,2)),rewrite(55(2))].
438 (x @ y) * y * x = x * y.  [para(3(a,1),44(a,1,2,2)),rewrite(55(2),29(2),178(4)),flip(a)].
787 (x @ y) * z * y * x = z * x * y.  [para(438(a,1),42(a,1,2,2)),rewrite(94(2),16(6),2(7))].
9892 $F # answer(E).  [para(787(a,2),7(a,1,2,2)),rewrite(338(13)),xx(a)].

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

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

Given=319. Generated=154662. Kept=9890. proofs=1.
Usable=270. Sos=6141. Demods=1953. Limbo=3, Disabled=3482. Hints=0.
Weight_deleted=16406. Literals_deleted=0.
Forward_subsumed=127215. Back_subsumed=564.
Sos_limit_deleted=1150. Sos_displaced=0. Sos_removed=0.
New_demodulators=4102 (5 lex), Back_demodulated=2912. Back_unit_deleted=0.
Demod_attempts=2834319. Demod_rewrites=595547.
Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0.
Nonunit_fsub_feature_tests=0. Nonunit_bsub_feature_tests=0.
Megabytes=6.43.
User_CPU=4.45, System_CPU=0.03, Wall_clock=5.

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

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

THEOREM PROVED

Exiting with 1 proof.

Process 11348 exit (max_proofs) Sat Aug 12 20:59:51 2006