============================== Prover9 ===============================
Prover9 (32) version August-2006A, August 2006.
Process 11354 was started by mccune on cleo.thornwood,
Sat Aug 12 20:59:51 2006
The command was "/home/mccune/bin/prover9 -f gt.in DE.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 DE.in


formulas(sos).
(x @ z) * (y @ z) = x * y @ z.
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 @ y) = x * z @ 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 @ y) = x * z @ 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 @ y) = x * z @ y.  [assumption].
end_of_list.

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

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

% Starting search at 0.00 seconds.

given #1 (I,wt=11): 1 (x * y) * z = x * y * z.  [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=13): 6 (x @ y) * (z @ y) = x * z @ y.  [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=6): 12 x' @ x = e.  [para(3(a,1),5(a,1,2,2)),rewrite(8(6)),flip(a)].

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

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

given #11 (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 #12 (F,wt=5): 29 x * e = x.  [back_rewrite(21),rewrite(26(4))].

given #13 (F,wt=4): 52 e' = e.  [para(29(a,1),3(a,1))].

given #14 (T,wt=5): 53 x @ e = e.  [para(29(a,1),5(a,1,2,2)),rewrite(52(3),2(3),3(2)),flip(a)].

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

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

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

given #18 (F,wt=6): 54 x * x' = e.  [para(26(a,1),3(a,1))].

given #19 (T,wt=6): 73 x @ x' = e.  [para(62(a,1),12(a,1,1))].

given #20 (T,wt=8): 58 x * x' * y = y.  [para(26(a,1),8(a,1))].

given #21 (A,wt=17): 14 (x * y @ z) * u = (x @ z) * (y @ z) * u.  [para(6(a,1),1(a,1,1))].

given #22 (F,wt=8): 72 x' @ y = y @ x.  [back_rewrite(64),rewrite(69(6))].

given #23 (F,wt=8): 80 x @ y' = y @ x.  [para(73(a,1),6(a,1,2)),rewrite(29(4),78(5))].

given #24 (T,wt=9): 32 x * y @ x = y @ x.  [para(23(a,1),6(a,1,1)),rewrite(2(3)),flip(a)].

given #25 (T,wt=9): 33 x * y @ y = x @ y.  [para(23(a,1),6(a,1,2)),rewrite(29(3)),flip(a)].

given #26 (A,wt=23): 15 (x @ y)' * (z @ y)' * (x * z @ y) = (x @ y) @ (z @ y).  [para(6(a,1),5(a,1,2,2))].

given #27 (F,wt=9): 105 x' @ y' = x @ y.  [para(72(a,2),72(a,1))].

given #28 (F,wt=9): 120 x' @ y = x @ y'.  [para(80(a,1),72(a,1)),flip(a)].

given #29 (T,wt=9): 139 x @ y * x = x @ y.  [para(8(a,1),33(a,1,1)),rewrite(132(5))].

given #30 (T,wt=10): 17 x' * y @ x = y @ x.  [para(12(a,1),6(a,1,1)),rewrite(2(3)),flip(a)].

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

given #32 (F,wt=7): 198 (x @ y) @ x = e.  [para(5(a,1),17(a,1,1)),rewrite(125(6),3(4),11(4))].

given #33 (F,wt=7): 232 (x @ y) @ y = e.  [para(80(a,1),198(a,1,1))].

given #34 (T,wt=8): 228 x' @ (x @ y) = e.  [para(198(a,1),72(a,2))].

given #35 (T,wt=7): 252 x @ (y @ x) = e.  [para(72(a,1),228(a,1,2)),rewrite(62(2))].

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

given #37 (F,wt=7): 255 x @ (x @ y) = e.  [para(105(a,1),228(a,1,2)),rewrite(62(2))].

given #38 (F,wt=8): 229 (x @ y) @ y' = e.  [para(72(a,1),198(a,1,1))].

given #39 (T,wt=8): 231 x @ (x' @ y) = e.  [para(198(a,1),80(a,1)),flip(a)].

given #40 (T,wt=8): 233 (x @ y') @ y = e.  [para(80(a,2),198(a,1,1))].

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

given #42 (F,wt=8): 237 (x @ y) @ x' = e.  [para(105(a,1),198(a,1,1))].

given #43 (F,wt=8): 238 (x' @ y) @ x = e.  [para(120(a,2),198(a,1,1))].

given #44 (T,wt=8): 247 x' @ (y @ x) = e.  [para(232(a,1),72(a,2))].

given #45 (T,wt=8): 248 x @ (y @ x') = e.  [para(232(a,1),80(a,1)),flip(a)].

given #46 (A,wt=10): 31 x * y' @ y = x @ y.  [back_rewrite(18),rewrite(29(5))].

given #47 (F,wt=9): 222 (x * y)' * x = y'.  [para(54(a,1),19(a,1,2,2)),rewrite(29(4))].

given #48 (F,wt=9): 234 (x @ y) @ y * x = e.  [para(32(a,1),198(a,1,1))].

given #49 (T,wt=9): 235 (x @ y) @ x * y = e.  [para(33(a,1),198(a,1,1))].

given #50 (T,wt=9): 272 (x @ y)' = x' @ y.  [para(54(a,1),25(a,1,2,1)),rewrite(11(4),29(4))].

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

given #52 (F,wt=9): 273 (x @ y) * (y @ x) = e.  [para(73(a,1),25(a,2)),rewrite(272(3),105(3),78(4))].

given #53 (F,wt=9): 302 (x @ y) @ (y @ x) = e.  [back_rewrite(152),rewrite(272(2),272(4),97(5),3(2),11(2)),flip(a)].

given #54 (T,wt=9): 403 x @ x * y = x @ y.  [para(222(a,1),17(a,1,1)),rewrite(142(3)),flip(a)].

given #55 (T,wt=9): 439 x * y @ y * x = e.  [para(234(a,1),32(a,2)),rewrite(1(3),335(3))].

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

given #57 (F,wt=10): 78 x * y @ y' = y @ x.  [para(54(a,1),10(a,1,2,2,2)),rewrite(62(4),29(4),69(4)),flip(a)].

given #58 (F,wt=10): 132 x' @ x * y = y @ x.  [para(32(a,1),72(a,2))].

given #59 (T,wt=10): 142 x' @ y * x = y @ x.  [para(33(a,1),72(a,2))].

given #60 (T,wt=10): 239 (x @ y) @ y' * x = e.  [para(17(a,1),198(a,1,1))].

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

given #62 (F,wt=10): 288 (x @ y) @ (x' @ y) = e.  [back_rewrite(150),rewrite(272(2),272(5),62(4),6(4),3(2),11(2)),flip(a)].

given #63 (F,wt=10): 289 (x' @ y) @ (x @ y) = e.  [back_rewrite(147),rewrite(272(3),62(2),272(3),6(4),54(2),11(2)),flip(a)].

given #64 (T,wt=10): 320 (x' @ y) @ y * x = e.  [para(139(a,1),229(a,1,1)),rewrite(120(4,R),272(2))].

given #65 (T,wt=10): 325 (x @ y) @ (y' @ x) = e.  [para(231(a,1),32(a,2)),rewrite(43(3),321(5))].

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

given #67 (F,wt=10): 363 (x @ y) * (x @ y') = e.  [back_rewrite(327),rewrite(360(6))].

given #68 (F,wt=10): 369 (x' @ y) @ x * y = e.  [para(33(a,1),237(a,1,1)),rewrite(120(4,R),272(2))].

given #69 (T,wt=10): 388 (x @ y) @ (x @ y') = e.  [para(248(a,1),17(a,2)),rewrite(272(3),105(3),384(5))].

given #70 (T,wt=10): 393 (x @ y) @ x * y' = e.  [para(31(a,1),198(a,1,1))].

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

given #72 (F,wt=10): 397 (x * y)' = y' * x'.  [para(8(a,1),222(a,1,1,1)),flip(a)].

given #73 (F,wt=10): 437 (x @ y) @ x' * y = e.  [para(80(a,1),234(a,1,1))].

given #74 (T,wt=10): 438 (x @ y') @ x * y = e.  [para(80(a,2),234(a,1,1))].

given #75 (T,wt=10): 457 (x @ y) @ y * x' = e.  [para(80(a,1),235(a,1,1))].

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

given #77 (F,wt=10): 458 (x @ y') @ y * x = e.  [para(80(a,2),235(a,1,1))].

given #78 (F,wt=10): 510 (x @ y') * (x @ y) = e.  [para(72(a,1),273(a,1,2))].

given #79 (T,wt=10): 515 (x' @ y) @ (y @ x) = e.  [para(302(a,1),72(a,2)),rewrite(272(2))].

given #80 (T,wt=10): 516 (x @ y') @ (x @ y) = e.  [para(72(a,1),302(a,1,2))].

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

given #82 (F,wt=10): 529 x @ y' * x * y = e.  [para(27(a,2),403(a,1,2)),rewrite(255(6))].

given #83 (F,wt=10): 537 (x @ y) @ (y @ x') = e.  [para(5(a,1),439(a,1,1)),rewrite(1(6),1(5),56(6))].

given #84 (T,wt=10): 538 (x @ y') @ (y @ x) = e.  [para(5(a,1),439(a,1,2)),rewrite(1(5),1(4),56(5))].

given #85 (T,wt=10): 542 x @ y * x * y' = e.  [para(8(a,1),439(a,1,1)),rewrite(1(3))].

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

given #87 (F,wt=11): 79 x * y @ x' = y @ x'.  [para(73(a,1),6(a,1,1)),rewrite(2(4)),flip(a)].

given #88 (F,wt=11): 133 x @ x' * y = y @ x'.  [para(32(a,1),80(a,1)),flip(a)].

given #89 (T,wt=11): 143 x @ y * x' = y @ x'.  [para(33(a,1),80(a,1)),flip(a)].

given #90 (T,wt=11): 146 (x @ y) * (y @ x) * z = z.  [back_rewrite(134),rewrite(142(4))].

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

given #92 (F,wt=11): 201 (x @ y) * z @ x = z @ x.  [para(9(a,1),17(a,1,1)),rewrite(125(8),8(6))].

given #93 (F,wt=9): 1413 x @ (y @ (x @ z)) = e.  [para(27(a,2),201(a,1,1)),rewrite(1402(5),3(2),11(2),1286(4)),flip(a)].

given #94 (T,wt=9): 1451 x @ ((x @ y) @ z) = e.  [para(72(a,1),1413(a,1,2))].

given #95 (T,wt=9): 1454 x @ (y @ (z @ x)) = e.  [para(80(a,1),1413(a,1,2,2))].

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

given #97 (F,wt=9): 1473 x @ ((y @ x) @ z) = e.  [para(80(a,1),1451(a,1,2,1))].

given #98 (F,wt=10): 1448 x @ ((x' @ y) @ z) = e.  [para(1413(a,1),72(a,1)),rewrite(1286(5)),flip(a)].

given #99 (T,wt=10): 1450 x' @ (y @ (z @ x)) = e.  [para(72(a,1),1413(a,1,2,2))].

given #100 (T,wt=10): 1453 (x @ (y @ z)) @ y' = e.  [para(1413(a,1),80(a,2))].

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

given #102 (F,wt=10): 1455 x @ (y @ (z @ x')) = e.  [para(80(a,2),1413(a,1,2,2))].

given #103 (F,wt=10): 1457 x' @ (y @ (x @ z)) = e.  [para(105(a,1),1413(a,1,2,2))].

given #104 (T,wt=10): 1458 x @ (y @ (x' @ z)) = e.  [para(120(a,1),1413(a,1,2)),rewrite(272(2))].

given #105 (T,wt=10): 1470 x' @ ((y @ x) @ z) = e.  [para(72(a,1),1451(a,1,2,1))].

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

given #107 (F,wt=10): 1472 ((x @ y) @ z) @ x' = e.  [para(1451(a,1),80(a,2))].

given #108 (F,wt=10): 1474 x @ ((y @ x') @ z) = e.  [para(80(a,2),1451(a,1,2,1))].

given #109 (T,wt=10): 1476 x' @ ((x @ y) @ z) = e.  [para(105(a,1),1451(a,1,2,1))].

given #110 (T,wt=10): 1492 (x @ (y @ z)) @ z' = e.  [para(1454(a,1),80(a,2))].

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

given #112 (F,wt=10): 1517 ((x @ y) @ z) @ y' = e.  [para(1473(a,1),80(a,2))].

given #113 (F,wt=11): 227 x * (y @ z) @ y = x @ y.  [para(198(a,1),6(a,1,2)),rewrite(29(3)),flip(a)].

given #114 (T,wt=11): 244 (x @ y) * z @ y = z @ y.  [para(232(a,1),6(a,1,1)),rewrite(2(3)),flip(a)].

given #115 (T,wt=11): 245 x * (y @ z) @ z = x @ z.  [para(232(a,1),6(a,1,2)),rewrite(29(3)),flip(a)].

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

given #117 (F,wt=7): 1986 (x @ y) @ z = e.  [back_rewrite(300),rewrite(1980(3)),flip(a)].

given #118 (F,wt=7): 2014 x @ (y @ z) = e.  [back_rewrite(1788),rewrite(1986(8)),flip(a)].

given #119 (T,wt=11): 335 x * y * (y @ x) = y * x.  [para(27(a,1),8(a,1,2)),rewrite(62(2))].

given #120 (T,wt=11): 448 x' * y' @ y * x = e.  [para(234(a,1),31(a,2)),rewrite(397(3),430(7))].

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

given #122 (F,wt=11): 550 x' * y' @ x * y = e.  [para(439(a,1),72(a,2)),rewrite(397(2))].

given #123 (F,wt=11): 551 x * y @ x' * y' = e.  [para(439(a,1),80(a,2)),rewrite(397(3))].

given #124 (T,wt=11): 651 x' * y @ y' * x = e.  [para(239(a,1),31(a,2)),rewrite(397(4),62(4),644(7))].

given #125 (T,wt=11): 780 x * y' @ y * x' = e.  [para(393(a,1),31(a,2)),rewrite(397(4),62(3),775(7))].

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

given #127 (F,wt=11): 784 x * y' @ x' * y = e.  [para(393(a,1),132(a,2)),rewrite(397(3),62(2),1(6),394(6))].

given #128 (F,wt=11): 826 x * y @ y' * x' = e.  [para(397(a,1),73(a,1,2))].

given #129 (T,wt=11): 896 x' * y @ x * y' = e.  [para(457(a,1),17(a,2)),rewrite(397(3),62(2),1(4),394(4))].

given #130 (T,wt=11): 1129 x @ y' * x' * y = e.  [para(529(a,1),363(a,1,1)),rewrite(397(5),397(3),62(6),1(5),2(7))].

given #131 (A,wt=12): 85 (x' @ y) * (x @ y) * z = z.  [para(3(a,1),14(a,1,1,1)),rewrite(11(2),2(2)),flip(a)].

given #132 (F,wt=11): 1175 x @ y * x' * y' = e.  [para(542(a,1),363(a,1,1)),rewrite(397(5),397(4),62(3),1(5),2(7))].

given #133 (F,wt=11): 1319 x @ (y @ x) * z = x @ z.  [para(51(a,2),5(a,1,2,2)),rewrite(397(4),272(4),1(10),514(9),5(5)),flip(a)].

given #134 (T,wt=11): 1998 (x @ y) * z = z * (x @ y).  [back_rewrite(1236),rewrite(1986(4),2(4)),flip(a)].

given #135 (T,wt=11): 2076 (x @ y) * z @ u = z @ u.  [back_rewrite(810),rewrite(2057(8),85(6)),flip(a)].

given #136 (A,wt=12): 90 (x @ y) * (x' @ y) * z = z.  [para(54(a,1),14(a,1,1,1)),rewrite(11(2),2(2)),flip(a)].

given #137 (F,wt=11): 2192 x * (y @ z) @ u = x @ u.  [para(1986(a,1),6(a,1,2)),rewrite(29(3)),flip(a)].

given #138 (F,wt=11): 2197 x * y @ z = y * x @ z.  [para(335(a,1),6(a,2,1)),rewrite(2192(4),6(3))].

given #139 (T,wt=11): 2219 (x @ y) * z * (y @ x) = z.  [para(335(a,1),146(a,1,2)),rewrite(2014(6),29(6))].

given #140 (T,wt=11): 2467 x @ y * (z @ u) = x @ y.  [para(2076(a,1),139(a,1)),rewrite(188(4),2076(6))].

given #141 (A,wt=12): 92 (x @ y') * z = (y @ x) * z.  [para(73(a,1),14(a,2,2,1)),rewrite(78(3),2(6)),flip(a)].

given #142 (F,wt=11): 2470 x @ (y @ z) * u = x @ u.  [para(78(a,1),2076(a,2)),rewrite(596(5))].

given #143 (F,wt=12): 345 x * (y @ x) = y * x * y'.  [para(80(a,1),27(a,2,2)),rewrite(62(2)),flip(a)].

given #144 (T,wt=11): 2599 (x @ y) * y * x = x * y.  [para(139(a,1),345(a,1,2)),rewrite(1998(3,R),1(6),54(5),29(5))].

given #145 (T,wt=11): 2669 x @ y * z = x @ z * y.  [para(2599(a,1),2470(a,1,2))].

given #146 (A,wt=14): 94 x' * y @ z = (z @ x) * (y @ z).  [para(72(a,1),6(a,1,1)),flip(a)].

given #147 (F,wt=12): 391 (x' @ y) * z = (y @ x) * z.  [para(31(a,1),9(a,2,1)),rewrite(1(8),8(7),127(7))].

given #148 (F,wt=12): 564 (x @ y) * x' * y * x = y.  [para(38(a,2),8(a,1,2)),rewrite(272(3),105(3))].

given #149 (T,wt=12): 566 x * (y @ x) = x * (x @ y').  [para(38(a,1),9(a,1,2,2)),rewrite(62(2),360(5),43(6)),flip(a)].

given #150 (T,wt=12): 577 x * (y @ x') = x * (x @ y).  [para(38(a,1),27(a,1)),rewrite(573(3))].

given #151 (A,wt=14): 95 x * y' @ z = (x @ z) * (z @ y).  [para(72(a,1),6(a,1,2)),flip(a)].

given #152 (F,wt=12): 593 x * y * (x @ y') = y * x.  [back_rewrite(563),rewrite(573(3))].

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

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

given #155 (T,wt=12): 1223 x * y * (x' @ y) = y * x.  [para(49(a,2),43(a,1)),rewrite(397(2),397(4),62(2),62(2),397(3),1(5),57(6),1(4),132(8),1(7),335(7))].

given #156 (A,wt=14): 96 (x' @ y) * (z @ x) = y * z @ x.  [para(72(a,2),6(a,1,1))].

given #157 (F,wt=11): 2988 x * x @ y = x @ y * y.  [back_rewrite(820),rewrite(2978(7),8(5)),flip(a)].

given #158 (F,wt=12): 1916 x' * y * x @ z = y @ z.  [para(245(a,1),5(a,2)),rewrite(397(3),272(2),1(8),736(7),1(10),44(9),6(5))].

given #159 (T,wt=12): 2039 (x' @ y) * z = z * (y @ x).  [back_rewrite(1208),rewrite(1986(6),2(7))].

given #160 (T,wt=12): 2045 (x' @ y) * z * (x @ y) = z.  [back_rewrite(582),rewrite(1986(8),29(7))].

given #161 (A,wt=14): 97 (x @ y) * (y' @ z) = x * z @ y.  [para(72(a,2),6(a,1,2))].

given #162 (F,wt=12): 2048 x' * (y @ z) * x = y @ z.  [back_rewrite(339),rewrite(1986(4),29(4),5(5)),flip(a)].

given #163 (F,wt=12): 2058 x * (y @ z) * x' = y @ z.  [back_rewrite(1780),rewrite(2014(4),2(3)),flip(a)].

given #164 (T,wt=12): 2073 x * (y' @ z) = x * (z @ y).  [back_rewrite(511),rewrite(2048(5),2014(5),2(6))].

given #165 (T,wt=12): 2077 x * y * x' @ z = y @ z.  [back_rewrite(905),rewrite(2075(3)),flip(a)].

given #166 (A,wt=17): 98 (x @ y) * z = y * x' * y' * x * z.  [para(72(a,1),9(a,2,1)),rewrite(62(2)),flip(a)].

given #167 (F,wt=12): 2404 (x @ y) * z * (x' @ y) = z.  [para(85(a,1),335(a,2)),rewrite(1986(9),29(6),1(5))].

given #168 (F,wt=12): 2447 (x @ y) * z = z * (y' @ x).  [para(72(a,1),1998(a,1,1))].

given #169 (T,wt=12): 2448 (x @ y) * z = z * (y @ x').  [para(80(a,1),1998(a,1,1))].

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

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

given #172 (F,wt=12): 2525 x' @ y * z = z * y @ x.  [para(2197(a,1),72(a,2))].

given #173 (F,wt=12): 2526 x * y @ z' = z @ y * x.  [para(2197(a,1),80(a,1))].

given #174 (T,wt=12): 2554 (x @ y) * z * (x @ y') = z.  [para(72(a,1),2219(a,1,1))].

given #175 (T,wt=12): 2555 (x @ y') * z * (x @ y) = z.  [para(72(a,1),2219(a,1,2,2))].

given #176 (A,wt=18): 100 (x' @ y * z) * u = (y @ x) * (z @ x) * u.  [para(72(a,2),14(a,1,1))].

given #177 (F,wt=12): 2571 x @ y' * z * y = x @ z.  [para(27(a,2),2467(a,1,2))].

given #178 (F,wt=12): 2634 x @ y * z * y' = x @ z.  [para(345(a,1),2467(a,1,2))].

given #179 (T,wt=12): 2639 (x' @ y) * x * y = y * x.  [para(2599(a,1),8(a,1,2)),rewrite(272(2))].

given #180 (T,wt=12): 2645 (x @ y') * x * y = y * x.  [para(80(a,2),2599(a,1,1))].

given #181 (A,wt=25): 106 (x @ y) * (z @ y) * x * z * y = x * z * y * (x * z @ y).  [back_rewrite(70),rewrite(105(4),14(5))].

given #182 (F,wt=12): 3020 x' @ y * y = y @ x * x.  [para(2988(a,1),72(a,2))].

given #183 (F,wt=12): 3022 x * x @ y' = y * y @ x.  [para(2988(a,2),80(a,2))].

given #184 (T,wt=12): 3156 x * (y @ z') = x * (z @ y).  [para(62(a,1),2073(a,1,2,1)),flip(a)].

given #185 (T,wt=13): 125 x * y * z @ y = x * z @ y.  [para(32(a,1),6(a,1,2)),rewrite(6(3)),flip(a)].

given #186 (A,wt=15): 109 (x @ y) * (z @ x') = y * z @ x'.  [para(80(a,1),6(a,1,1))].

given #187 (F,wt=13): 136 x * y * z @ z = x * y @ z.  [para(1(a,1),33(a,1,1))].

given #188 (F,wt=13): 169 x * y * x' * y' = x @ y.  [para(105(a,1),5(a,2)),rewrite(62(2),62(2))].

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

given #190 (T,wt=13): 275 (x @ y) * (y * z @ x) = z @ x.  [para(72(a,2),25(a,1,1,1)),rewrite(272(3),62(2))].

given #191 (A,wt=15): 110 (x @ y') * (y @ z) = x * z @ y'.  [para(80(a,1),6(a,1,2))].

given #192 (F,wt=13): 342 x * (x @ y') = y * x * y'.  [para(62(a,1),27(a,1,1)),flip(a)].

given #193 (F,wt=13): 344 x' * y * x = y * (x' @ y).  [para(72(a,2),27(a,2,2))].

given #194 (T,wt=13): 346 x' * y * x = y * (x @ y').  [para(80(a,2),27(a,2,2))].

given #195 (T,wt=13): 351 x * (x' @ y) = y * x * y'.  [para(120(a,2),27(a,2,2)),rewrite(62(2)),flip(a)].

given #196 (A,wt=14): 111 (x @ y') * (z @ x) = y * z @ x.  [para(80(a,2),6(a,1,1))].

given #197 (F,wt=13): 394 x * y' * (x @ y) = y' * x.  [para(31(a,1),27(a,2,2)),rewrite(1(4),3(3),29(3),1(6)),flip(a)].

given #198 (F,wt=13): 421 x * y @ z = z @ y' * x'.  [back_rewrite(113),rewrite(397(4))].

given #199 (T,wt=13): 514 (x' @ y) * (y' @ x) * z = z.  [para(302(a,1),9(a,2,1)),rewrite(272(2),272(4),146(8),2(8))].

given #200 (T,wt=13): 534 x * y * z @ z * x * y = e.  [para(1(a,1),439(a,1,1))].

given #201 (A,wt=14): 112 (x @ y) * (y @ z') = x * z @ y.  [para(80(a,2),6(a,1,2))].

given #202 (F,wt=13): 535 x * y * z @ y * z * x = e.  [para(1(a,1),439(a,1,2))].

given #203 (F,wt=13): 827 x' * y' @ z = z @ y * x.  [para(397(a,1),72(a,1,1))].

given #204 (T,wt=13): 1030 x' * y = y * (y @ x) * x'.  [para(54(a,1),47(a,1,2,2)),rewrite(29(3))].

given #205 (T,wt=13): 1102 (x' @ y) * z = (x @ y') * z.  [para(516(a,1),47(a,2,2,1)),rewrite(272(2),995(7),2(7))].

given #206 (A,wt=17): 114 x' * y * x * y' * z = (y @ x) * z.  [para(80(a,1),9(a,2,1)),rewrite(62(3))].

given #207 (F,wt=13): 1285 (x @ y') * (y @ x') * z = z.  [para(120(a,1),146(a,1,1))].

given #208 (F,wt=13): 2038 (x' @ y) * z = z * (x @ y').  [back_rewrite(1226),rewrite(1986(6),2(8))].

given #209 (T,wt=13): 2071 x * (y' @ z) = x * (y @ z').  [back_rewrite(754),rewrite(2048(5),2014(5),2(7))].

given #210 (T,wt=13): 2202 x' * y * (x @ y) = y * x'.  [para(80(a,1),335(a,1,2,2))].

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

given #212 (F,wt=13): 2450 (x @ y') * z = z * (x' @ y).  [para(120(a,1),1998(a,1,1))].

given #213 (F,wt=13): 2527 x * y @ z = z @ x' * y'.  [para(2197(a,1),80(a,2)),rewrite(397(2)),flip(a)].

given #214 (T,wt=13): 2550 (x @ y) * (z * y @ x) = z @ x.  [para(6(a,1),2219(a,1,2))].

given #215 (T,wt=13): 2556 (x @ y') * z * (y @ x') = z.  [para(120(a,1),2219(a,1,1))].

given #216 (A,wt=20): 119 (x @ y) * (z @ y) * u = (x @ y) * (y @ z') * u.  [para(80(a,2),14(a,2,2,1)),rewrite(14(3))].

given #217 (F,wt=13): 2557 (x' @ y) * z * (y' @ x) = z.  [para(120(a,2),2219(a,1,1))].

given #218 (F,wt=13): 2643 x' * y = (y @ x) * y * x'.  [para(72(a,1),2599(a,1,1)),flip(a)].

given #219 (T,wt=12): 4909 x * (y @ x) * y * x' = y.  [para(2643(a,1),8(a,1,2)),rewrite(62(2))].

given #220 (T,wt=13): 2644 (x @ y) * x' * y = y * x'.  [para(80(a,1),2599(a,1,1))].

given #221 (A,wt=15): 123 x * y * z @ x * y = z @ x * y.  [para(1(a,1),32(a,1,1))].

given #222 (F,wt=13): 2675 x' * y' @ z = z @ x * y.  [para(2669(a,1),72(a,2)),rewrite(397(2))].

given #223 (F,wt=13): 2954 (x @ y) * (x @ z) = x @ y * z.  [para(78(a,1),96(a,1,2)),rewrite(62(2),596(7))].

given #224 (T,wt=13): 2966 x' * y @ z = z @ y' * x.  [para(651(a,1),96(a,1,2)),rewrite(397(3),62(3),29(5),2289(9))].

given #225 (T,wt=13): 2967 x * y' @ z = z @ y * x'.  [para(780(a,1),96(a,1,2)),rewrite(397(3),62(2),29(5),2304(9))].

given #226 (A,wt=16): 170 x' * y @ z' = (x @ z) * (y @ z').  [para(105(a,1),6(a,1,1)),flip(a)].

given #227 (F,wt=13): 2970 x' * x' @ y = y * y @ x.  [para(96(a,1),95(a,2))].

given #228 (F,wt=13): 2975 x * y' @ z = z @ x' * y.  [back_rewrite(2840),rewrite(2954(7))].

given #229 (T,wt=13): 2976 x' * y @ z = z @ x * y'.  [back_rewrite(2710),rewrite(2954(7))].

given #230 (T,wt=13): 3021 x @ y' * y' = y @ x * x.  [para(2988(a,1),80(a,1))].

given #231 (A,wt=16): 171 x * y' @ z' = (x @ z') * (y @ z).  [para(105(a,1),6(a,1,2)),flip(a)].

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

given #233 (F,wt=13): 3813 x' @ y * y = x * x @ y'.  [para(3020(a,2),80(a,2)),flip(a)].

given #234 (T,wt=13): 3912 x * y @ x * x = y * y @ x.  [para(125(a,1),2988(a,1)),rewrite(1(2),32(3)),flip(a)].

given #235 (T,wt=13): 4015 x @ y * x * z = x @ y * z.  [para(335(a,1),188(a,1,2,2)),rewrite(2192(5),2192(7))].

given #236 (A,wt=17): 172 (x @ y) * z = x * y * x' * y' * z.  [para(105(a,1),9(a,2,1)),rewrite(62(2),62(2)),flip(a)].

given #237 (F,wt=13): 4028 x * x @ y * x = x @ y * y.  [para(188(a,1),2988(a,2)),rewrite(1(5),4015(6))].

given #238 (F,wt=13): 4322 x * y * z @ y * x * z = e.  [para(335(a,1),534(a,1,1,2)),rewrite(1(6),2697(7))].

given #239 (T,wt=13): 5017 x * y @ y * y = x @ y * y.  [para(123(a,1),2988(a,1)),rewrite(1(2),4015(3),1(5),1(7),1(8),1(7),520(9),4020(7)),flip(a)].

given #240 (T,wt=13): 5082 (x @ y) * (y @ x * z) = y @ z.  [para(2954(a,1),146(a,1,2))].

given #241 (A,wt=15): 173 x' * y @ z = (x @ z') * (y @ z).  [para(120(a,1),6(a,1,1)),flip(a)].

given #242 (F,wt=13): 5093 (x @ y) * (y @ z * x) = y @ z.  [para(2954(a,1),2219(a,1,2))].

given #243 (F,wt=13): 5736 x * y @ x * x = y @ x * x.  [para(3912(a,2),5(a,2)),rewrite(397(2),1(6),1(8),3773(7),8(5)),flip(a)].

given #244 (T,wt=13): 5797 x * x @ x * y = x @ y * y.  [para(4015(a,1),2988(a,2)),rewrite(1(5),403(6))].

given #245 (T,wt=13): 5902 x * x @ y * x = x * x @ y.  [para(4028(a,2),5(a,2)),rewrite(397(3),1(7),422(8),2168(4)),flip(a)].

given #246 (A,wt=15): 174 x * y' @ z = (x @ z) * (y @ z').  [para(120(a,1),6(a,1,2)),flip(a)].

given #247 (F,wt=13): 5988 x * y * z @ x * z * y = e.  [para(4322(a,1),2197(a,1)),rewrite(1(3)),flip(a)].

given #248 (F,wt=13): 6176 x * x @ x * y = x * x @ y.  [para(5797(a,2),5(a,2)),rewrite(397(3),1(7),422(8),2168(4)),flip(a)].

given #249 (T,wt=13): 6327 x * y * z @ z * y * x = e.  [para(5988(a,1),2197(a,1)),rewrite(1(3)),flip(a)].

given #250 (T,wt=14): 199 x * y' * z @ y = x * z @ y.  [para(17(a,1),6(a,1,2)),rewrite(6(3)),flip(a)].

given #251 (A,wt=16): 175 (x' @ y) * (z @ y') = x * z @ y'.  [para(120(a,2),6(a,1,1))].

given #252 (F,wt=14): 277 (x @ y) * (x * z @ y') = y @ z.  [para(80(a,1),25(a,2)),rewrite(272(3),105(3))].

given #253 (F,wt=14): 343 x' * (y @ x) = y' * x' * y.  [para(72(a,1),27(a,2,2)),flip(a)].

given #254 (T,wt=14): 349 x' * (x @ y) = y * x' * y'.  [para(105(a,1),27(a,2,2)),rewrite(62(2)),flip(a)].

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

given #256 (A,wt=16): 176 (x @ y') * (z' @ y) = x * z @ y'.  [para(120(a,2),6(a,1,2))].

given #257 (F,wt=14): 405 x' * y' * x * (y @ x) = y'.  [back_rewrite(364),rewrite(397(4),397(2),62(5),1(4),1(6),1(5))].

given #258 (F,wt=14): 576 x' * (y @ x) = x' * (x @ y').  [para(38(a,1),27(a,1,2)),rewrite(397(2),573(6),1(7),8(6),142(8)),flip(a)].

given #259 (T,wt=14): 596 x * y * z @ z' = z @ x * y.  [para(1(a,1),78(a,1,1))].

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

given #261 (A,wt=18): 177 (x @ y') * z = x * y' * x' * y * z.  [para(120(a,1),9(a,2,1)),rewrite(62(2)),flip(a)].

given #262 (F,wt=14): 801 x' * y' @ z = y * x @ z'.  [para(120(a,2),44(a,2)),rewrite(62(3),792(8),397(5)),flip(a)].

given #263 (F,wt=14): 830 x' @ y * z = x @ z' * y'.  [para(397(a,1),120(a,2,2))].

given #264 (T,wt=14): 1179 (x @ y) * y' * x' * y = x'.  [para(3(a,1),49(a,1,2)),rewrite(29(3),397(3),397(5),62(3),62(3),403(3),397(4),1(6)),flip(a)].

given #265 (T,wt=14): 1188 x' * y = (x @ y') * y * x'.  [para(54(a,1),49(a,1,2,2)),rewrite(29(3))].

given #266 (A,wt=18): 178 x' * y * x * y' * z = (x' @ y) * z.  [para(120(a,2),9(a,2,1)),rewrite(62(3))].

given #267 (F,wt=14): 1210 x' @ y * x * z = y * z @ x.  [para(49(a,1),403(a,1,2)),rewrite(1108(6)),flip(a)].

given #268 (F,wt=14): 1261 (x' @ y) * y' * x = x * y'.  [para(133(a,1),43(a,2,2)),rewrite(397(3),62(3),33(3),1(10),335(10))].

given #269 (T,wt=14): 2168 x * y @ y' * x = y * y @ x.  [para(67(a,2),44(a,1,2,2)),rewrite(422(8),136(7))].

given #270 (T,wt=14): 2186 x * y' * (y @ x') = y' * x.  [para(56(a,1),67(a,1,2)),rewrite(397(3),62(2),1(5),896(11),29(8))].

given #271 (A,wt=17): 190 (x @ y) * (z @ y * x) = x * z @ y * x.  [para(139(a,1),6(a,1,1))].

given #272 (F,wt=14): 2188 x' * y * (y' @ x) = y * x'.  [para(57(a,1),67(a,1,2)),rewrite(397(3),62(3),1(5),784(11),29(8))].

given #273 (F,wt=14): 2236 (x @ y) * x' = y * x' * y'.  [para(72(a,1),76(a,2,1)),rewrite(62(2)),flip(a)].

given #274 (T,wt=14): 2318 x' * (y @ z) = (z' @ y) * x'.  [para(273(a,1),82(a,1,2,2)),rewrite(272(2),29(5),1986(6),2(9)),flip(a)].

given #275 (T,wt=14): 2498 (x @ y) * x * y' * x' = y'.  [para(76(a,2),90(a,1,2)),rewrite(62(3))].

given #276 (A,wt=18): 284 (x' @ y) * (x * z @ y * x) = z @ y * x.  [para(139(a,1),25(a,1,1,1)),rewrite(272(2))].

given #277 (F,wt=14): 2528 x' * y' @ z' = x * y @ z.  [para(2197(a,1),105(a,2)),rewrite(397(2))].

given #278 (F,wt=14): 2529 x' * y' @ z = x * y @ z'.  [para(2197(a,1),120(a,2)),rewrite(397(2))].

given #279 (T,wt=14): 2676 x' @ y' * z' = x @ y * z.  [para(2669(a,1),105(a,2)),rewrite(397(3))].

given #280 (T,wt=14): 2677 x' @ y * z = x @ y' * z'.  [para(2669(a,1),120(a,1)),rewrite(397(5))].

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

given #282 (F,wt=14): 2708 x @ y' * z = (x @ z) * (y @ x).  [para(94(a,1),80(a,2)),rewrite(397(3),62(3))].

given #283 (F,wt=14): 2713 x' * y @ z' = x * y' @ z.  [para(120(a,2),94(a,2,2)),rewrite(96(9))].

given #284 (T,wt=14): 2745 x' * y @ z = (y @ z) * (z @ x).  [para(94(a,2),335(a,2)),rewrite(2014(5),29(4)),flip(a)].

given #285 (T,wt=14): 2746 x * y' @ z = (z @ y) * (x @ z).  [para(335(a,1),94(a,1,1)),rewrite(2192(8))].

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

given #287 (F,wt=14): 2831 x' * y @ z = x * y' @ z'.  [back_rewrite(2798),rewrite(2819(8)),flip(a)].

given #288 (F,wt=14): 2838 x @ y * z' = (z @ x) * (x @ y).  [para(95(a,1),80(a,2)),rewrite(397(3),62(2))].

given #289 (T,wt=14): 2922 (x @ y') * (x * z @ y) = z @ y.  [para(6(a,1),995(a,1,2))].

given #290 (T,wt=14): 2987 (x' @ y) * (y @ z) = y @ x * z.  [back_rewrite(1089),rewrite(2978(7),8(5)),flip(a)].

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

given #292 (F,wt=14): 2992 (x @ y) * (z' @ x) = x @ y * z.  [back_rewrite(2884),rewrite(2987(4)),flip(a)].

given #293 (F,wt=14): 3029 x' @ y * y = x' * x' @ y.  [para(2988(a,1),272(a,1,1)),rewrite(272(3),397(5))].

given #294 (T,wt=14): 3119 x * y' * x' * (x @ y) = y'.  [para(2045(a,1),82(a,2)),rewrite(62(2))].

given #295 (T,wt=14): 3137 (x @ y') * (z * x @ y) = z @ y.  [para(97(a,1),2219(a,1,2))].

given #296 (A,wt=22): 399 (x' @ y) * z * (y @ z) = y * z * x * y' * x'.  [para(222(a,1),9(a,1,2,2)),rewrite(1(2),397(3),397(2),1(5),397(6),397(4),62(2),62(2),62(3),1(2),1(6),1(5),1(8),397(9),397(8),1(11),390(12),14(11),43(11)),flip(a)].

given #297 (F,wt=14): 3265 x' * (y' @ z) = (z @ y) * x'.  [para(2447(a,1),397(a,1,1)),rewrite(397(4),272(3),62(2),272(6)),flip(a)].

given #298 (F,wt=14): 3326 x' * y = y * (x @ y') * x'.  [para(2448(a,2),1223(a,1,2)),flip(a)].

given #299 (T,wt=14): 3559 (x @ y) * (x' @ z * y) = z @ x.  [para(273(a,1),100(a,2,2)),rewrite(1998(5,R),29(8))].

given #300 (T,wt=14): 3583 (x @ y) * (x' @ y * z) = z @ x.  [para(100(a,2),2219(a,1)),rewrite(1998(5,R))].

given #301 (A,wt=21): 401 x * y * z' * x' * z * y' = z * y' @ x.  [para(222(a,1),10(a,1,2,2,2)),rewrite(397(2),397(5),397(4),62(2),62(2),1(3),1(8),1(7),397(10),390(13))].

given #302 (F,wt=14): 3812 x * y' @ y * x = x @ y * y.  [para(3020(a,1),5(a,2)),rewrite(62(2),397(2),1(7),424(8))].

given #303 (F,wt=14): 4174 x @ y' * z = (y @ x) * (x @ z).  [para(95(a,1),111(a,2)),rewrite(2992(5))].

given #304 (T,wt=14): 4194 x * (x @ y) * y' * x' = y'.  [para(403(a,1),394(a,1,2,2)),rewrite(397(2),1998(5,R),397(8),1(10),3(9),29(9))].

given #305 (T,wt=14): 4210 x' * (y @ z') = (z @ y) * x'.  [para(394(a,1),92(a,1)),rewrite(1986(9),29(8))].

given #306 (A,wt=24): 402 x' * y' * (x' * y' @ z) = z' * x' * y' * z.  [para(10(a,1),222(a,1,1,1)),rewrite(272(3),397(2),397(6),354(8),1(8),397(13),397(11),397(10),1(13),62(15),1(14),1(13))].

given #307 (F,wt=14): 4211 x' * (y @ z) = (z @ y') * x'.  [para(394(a,1),92(a,2)),rewrite(1986(5),29(5)),flip(a)].

given #308 (F,wt=14): 4595 x' * y @ z' = y' * x @ z.  [para(2038(a,2),94(a,2)),rewrite(97(9))].

given #309 (T,wt=14): 4751 x * y' @ z' = y * x' @ z.  [para(2450(a,1),95(a,2)),rewrite(96(9))].

given #310 (T,wt=14): 4783 x @ y * z' = (x @ y) * (z @ x).  [para(2527(a,1),94(a,1)),rewrite(62(2))].

given #311 (A,wt=15): 406 x' * (x' @ y) = y' * x' * y.  [back_rewrite(396),rewrite(397(4),397(2),62(5),1(4)),flip(a)].

given #312 (F,wt=14): 5153 x' @ y' * z = x @ z' * y.  [para(2966(a,1),72(a,2))].

given #313 (F,wt=14): 5200 x' @ y * z' = x @ y' * z.  [para(2966(a,1),2525(a,2))].

given #314 (T,wt=14): 5201 x' @ y' * z = x @ y * z'.  [para(2966(a,1),2526(a,1))].

given #315 (T,wt=14): 5247 x' @ y * z' = x @ z * y'.  [para(2967(a,1),72(a,2))].

given #316 (A,wt=20): 413 x * y * z' * y' * x' * z = z @ x * y.  [back_rewrite(226),rewrite(397(3),397(2),1(5),1(6),1(5))].

given #317 (F,wt=14): 5908 x' * y @ x * y = y @ x * x.  [para(4028(a,1),17(a,2)),rewrite(397(2),1(5),2113(7))].

given #318 (F,wt=14): 6020 x' * y @ x * x = y @ x * x.  [para(5017(a,1),17(a,2)),rewrite(397(2),1(5),3068(7))].

given #319 (T,wt=14): 6022 x * y' @ y * y = x @ y * y.  [para(5017(a,1),31(a,2)),rewrite(397(3),1(5),58(4))].

given #320 (T,wt=14): 6180 x' * y @ y * x = y @ x * x.  [para(5797(a,1),17(a,2)),rewrite(397(2),1(5),8(4))].

given #321 (A,wt=17): 414 x' * y' @ y * x * z = z @ y * x.  [back_rewrite(225),rewrite(397(2))].

given #322 (F,wt=14): 6181 x * y' @ x * y = x @ y * y.  [para(5797(a,1),31(a,2)),rewrite(397(3),1(5),3178(7))].

given #323 (F,wt=14): 6361 x * x @ x' * y = x * x @ y.  [para(58(a,1),6176(a,1,2)),flip(a)].

given #324 (T,wt=14): 6365 x * x @ y * x' = x * x @ y.  [para(345(a,2),6176(a,1,2)),rewrite(2467(4)),flip(a)].

given #325 (T,wt=14): 6883 x * y @ x' * y = x * x @ y.  [para(335(a,1),2168(a,1,1)),rewrite(397(4),272(3),1998(5),1(6),1998(5),2568(7),1(9),2984(8),2500(9))].

given #326 (A,wt=19): 415 x * y * z @ y' * x' = z @ y' * x'.  [back_rewrite(224),rewrite(397(4),397(8))].

given #327 (F,wt=14): 6884 x * y @ y * x' = x * x @ y.  [para(335(a,1),2168(a,1,2)),rewrite(1(4),1998(3),593(4),2467(9))].

given #328 (F,wt=14): 6885 x * y @ x * y' = y * y @ x.  [para(2168(a,1),2669(a,1)),flip(a)].

given #329 (T,wt=15): 416 x * y * (y @ x) * z = y * x * z.  [back_rewrite(217),rewrite(397(4),62(2),62(2),1(4))].

given #330 (T,wt=15): 520 x * y @ x * y * z = x * y @ z.  [para(1(a,1),403(a,1,2))].

given #331 (A,wt=23): 418 (x' @ y) * (z' @ y) * u = (z @ y') * (x @ y') * u.  [back_rewrite(179),rewrite(397(2),14(5))].

given #332 (F,wt=15): 539 x * y * z @ y * x = z @ y * x.  [para(439(a,1),6(a,1,1)),rewrite(2(4),1(4)),flip(a)].

given #333 (F,wt=15): 540 x * y * z @ z * y = x @ z * y.  [para(439(a,1),6(a,1,2)),rewrite(29(4)),flip(a)].

given #334 (T,wt=15): 598 x * y * z @ y' = x * z @ y'.  [para(78(a,1),6(a,1,1)),rewrite(109(4),1(5)),flip(a)].

given #335 (T,wt=15): 1267 x @ y * z * x' = y * z @ x'.  [para(1(a,1),143(a,1,2))].

given #336 (A,wt=23): 422 x' * y' * z' * x * y * z = y * x @ x' * z.  [back_rewrite(84),rewrite(397(2),397(6),62(6),1(7),1(8))].

given #337 (F,wt=15): 1502 x * y' * x' * (y @ x') = y'.  [para(56(a,1),27(a,1,2)),rewrite(397(4),397(3),62(2),1(4),1(7),1(6),1210(13),54(10),11(10),29(10))].

given #338 (F,wt=15): 1742 (x' @ y) * y' = x * y' * x'.  [para(54(a,1),61(a,2,2,2,2)),rewrite(29(8))].

given #339 (T,wt=15): 1956 (x @ y) * (z * x @ y') = z @ y'.  [para(245(a,1),56(a,2)),rewrite(397(4),272(3),105(3),1(8),736(7),1(10),792(9))].

given #340 (T,wt=15): 2091 x * y @ x * z * y = x * y @ z.  [back_rewrite(1246),rewrite(2076(7))].

given #341 (A,wt=21): 423 x' * y' * z * y * x * z' = y * x @ z'.  [back_rewrite(74),rewrite(397(2),1(8))].

given #342 (F,wt=15): 2132 x' * y' = (x @ y) * y' * x'.  [para(5(a,1),67(a,1,2)),rewrite(397(2),1998(5,R),550(12),29(9)),flip(a)].

given #343 (F,wt=15): 2204 x' * y' = y' * x' * (x @ y).  [para(105(a,1),335(a,1,2,2)),flip(a)].

given #344 (T,wt=15): 2208 x * y * y * x = y * x * x * y.  [para(439(a,1),335(a,1,2,2)),rewrite(29(4),1(3),1(6))].

given #345 (T,wt=15): 2237 x' * y' * x = (y @ x') * y'.  [para(80(a,2),76(a,2,1))].

given #346 (A,wt=23): 424 x * y' * z' * x' * y * z = y * x' @ x * z.  [back_rewrite(68),rewrite(397(3),62(2),397(4),1(7),1(8))].

given #347 (F,wt=15): 2252 x' * (y' @ x) = y * x' * y'.  [para(542(a,1),76(a,2,1)),rewrite(397(5),397(4),62(3),1(5),1(6),1(5),57(6),397(9),397(8),62(7),1(9),2(10))].

given #348 (F,wt=15): 2256 (x @ y') * y * x' * y' = x'.  [para(56(a,1),76(a,1,2)),rewrite(397(4),397(3),62(2),1(4),1998(7,R),125(11),54(9),11(9),2(10))].

given #349 (T,wt=15): 2324 x' * (y @ z') = (y' @ z) * x'.  [para(363(a,1),82(a,1,2,2)),rewrite(272(2),29(5),1986(6),2(10)),flip(a)].

given #350 (T,wt=15): 2400 (x @ y) * z * u = z * (x @ y) * u.  [para(85(a,1),47(a,1,2,2)),rewrite(272(3),62(2),2014(6),2(7))].

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

given #352 (F,wt=15): 2443 (x @ y) * z * u = z * u * (x @ y).  [para(1998(a,2),1(a,1))].

given #353 (F,wt=15): 2444 x * (y @ z) * u = x * u * (y @ z).  [para(1998(a,1),1(a,2,2)),rewrite(1(3))].

given #354 (T,wt=15): 2466 x * (y @ z) * u @ v = x * u @ v.  [para(2076(a,1),6(a,1,2)),rewrite(6(3)),flip(a)].

given #355 (T,wt=15): 2500 x * y * (z @ u) @ v = x * y @ v.  [para(1(a,1),2192(a,1,1))].

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

given #357 (F,wt=15): 2522 x * y * z @ u = z * x * y @ u.  [para(1(a,1),2197(a,1,1))].

given #358 (F,wt=15): 2523 x * y * z @ u = y * x * z @ u.  [para(2197(a,1),6(a,1,1)),rewrite(6(4),1(2),1(5))].

given #359 (T,wt=15): 2524 x * y * z @ u = x * z * y @ u.  [para(2197(a,1),6(a,1,2)),rewrite(6(4))].

given #360 (T,wt=15): 2530 x * y @ z * y * x = y * x @ z.  [para(2197(a,1),139(a,1))].

given #361 (A,wt=16): 487 x * y * (z @ y) = x * z * y * z'.  [para(3(a,1),34(a,1,2,2,2)),rewrite(397(2),397(4),62(2),62(2),29(4),1(3),397(6),31(8),43(7)),flip(a)].

given #362 (F,wt=15): 2534 x * y @ y * x * z = y * x @ z.  [para(2197(a,1),403(a,1)),rewrite(1(3))].

given #363 (F,wt=15): 2548 (x @ y) * z * (y @ x) * u = z * u.  [para(2219(a,1),1(a,1,1)),rewrite(1(5)),flip(a)].

given #364 (T,wt=15): 2549 (x @ y) * z * u * (y @ x) = z * u.  [para(1(a,1),2219(a,1,2))].

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

given #366 (A,wt=21): 489 x * y' * z * y * u = x * (y @ z') * z * u.  [para(8(a,1),34(a,1,2,2,2,2)),rewrite(62(3))].

given #367 (F,wt=15): 2637 (x @ y) * y * x * z = x * y * z.  [para(2599(a,1),1(a,1,1)),rewrite(1(2),1(5)),flip(a)].

given #368 (F,wt=15): 2667 (x @ y) * z * y * x = z * x * y.  [para(2197(a,1),2599(a,1,1)),rewrite(14(5),2637(5),1(6))].

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

% Proof 1 at 4.75 (+ 0.05) seconds: E.
% Length of proof is 72.
% Level of proof is 16.
% Maximum clause weight is 24.
% Given clauses 368.

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 @ y) = x * z @ 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))].
11 e @ x = e.  [para(2(a,1),5(a,1,2,2)),rewrite(3(4),3(4)),flip(a)].
12 x' @ x = e.  [para(3(a,1),5(a,1,2,2)),rewrite(8(6)),flip(a)].
14 (x * y @ z) * u = (x @ z) * (y @ z) * u.  [para(6(a,1),1(a,1,1))].
15 (x @ y)' * (z @ y)' * (x * z @ y) = (x @ y) @ (z @ y).  [para(6(a,1),5(a,1,2,2))].
16 (x @ y) * e = x * e @ y.  [para(11(a,1),6(a,1,2))].
17 x' * y @ x = y @ x.  [para(12(a,1),6(a,1,1)),rewrite(2(3)),flip(a)].
18 x * y' @ y = x * e @ y.  [para(12(a,1),6(a,1,2)),rewrite(16(3)),flip(a)].
19 (x * y)' * x * y * z = z.  [para(1(a,1),8(a,1,2))].
21 x'' * e = x.  [para(3(a,1),8(a,1,2))].
23 x @ x = e.  [para(8(a,1),5(a,1,2)),rewrite(3(2)),flip(a)].
24 x'' * (x @ y) = y' * x * y.  [para(5(a,1),8(a,1,2))].
25 (x @ y)' * (x * z @ y) = z @ y.  [para(6(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(24),rewrite(26(4)),flip(a)].
29 x * e = x.  [back_rewrite(21),rewrite(26(4))].
31 x * y' @ y = x @ y.  [back_rewrite(18),rewrite(29(5))].
32 x * y @ x = y @ x.  [para(23(a,1),6(a,1,1)),rewrite(2(3)),flip(a)].
33 x * y @ y = x @ y.  [para(23(a,1),6(a,1,2)),rewrite(29(3)),flip(a)].
43 (x' @ y) * x = x * (y @ x).  [para(5(a,1),9(a,1,2)),rewrite(26(4)),flip(a)].
44 x' * y' * x * y * (z @ y) = x * z @ y.  [para(9(a,2),6(a,1))].
49 x' * y * x * z = (x @ y') * y * z.  [para(8(a,1),9(a,1,2,2,2)),rewrite(26(5))].
54 x * x' = e.  [para(26(a,1),3(a,1))].
62 x'' = x.  [para(26(a,1),29(a,1)),rewrite(29(2)),flip(a)].
64 (x * y')' * y' * x = x @ y.  [para(3(a,1),10(a,1,2,2,2)),rewrite(29(6),31(9))].
69 (x * y)' * y * x = y @ x.  [para(8(a,1),10(a,1,2)),rewrite(32(6))].
72 x' @ y = y @ x.  [back_rewrite(64),rewrite(69(6))].
73 x @ x' = e.  [para(62(a,1),12(a,1,1))].
78 x * y @ y' = y @ x.  [para(54(a,1),10(a,1,2,2,2)),rewrite(62(4),29(4),69(4)),flip(a)].
80 x @ y' = y @ x.  [para(73(a,1),6(a,1,2)),rewrite(29(4),78(5))].
105 x' @ y' = x @ y.  [para(72(a,2),72(a,1))].
112 (x @ y) * (y @ z') = x * z @ y.  [para(80(a,2),6(a,1,2))].
125 x * y * z @ y = x * z @ y.  [para(32(a,1),6(a,1,2)),rewrite(6(3)),flip(a)].
132 x' @ x * y = y @ x.  [para(32(a,1),72(a,2))].
139 x @ y * x = x @ y.  [para(8(a,1),33(a,1,1)),rewrite(132(5))].
155 (x' @ y)' * (z @ x)' * (y * z @ x) = (y @ x) @ (z @ x).  [para(72(a,2),15(a,1,1,1))].
164 (x @ y)' * (z @ y)' * (y @ (x * z)') = (x @ y) @ (z @ y).  [para(80(a,2),15(a,1,2,2))].
198 (x @ y) @ x = e.  [para(5(a,1),17(a,1,1)),rewrite(125(6),3(4),11(4))].
217 (x' * y')' * (x @ y) * z = x * y * z.  [para(9(a,1),19(a,1,2))].
222 (x * y)' * x = y'.  [para(54(a,1),19(a,1,2,2)),rewrite(29(4))].
232 (x @ y) @ y = e.  [para(80(a,1),198(a,1,1))].
245 x * (y @ z) @ z = x @ z.  [para(232(a,1),6(a,1,2)),rewrite(29(3)),flip(a)].
272 (x @ y)' = x' @ y.  [para(54(a,1),25(a,1,2,1)),rewrite(11(4),29(4))].
273 (x @ y) * (y @ x) = e.  [para(73(a,1),25(a,2)),rewrite(272(3),105(3),78(4))].
287 (x @ y) * (z' * y * z @ x) = (y @ x) @ (z @ x).  [back_rewrite(155),rewrite(272(3),62(2),272(3),6(6))].
300 (x @ y) @ (z @ y) = (x @ z) @ y.  [back_rewrite(164),rewrite(272(2),272(4),112(8),6(7),5(5)),flip(a)].
335 x * y * (y @ x) = y * x.  [para(27(a,1),8(a,1,2)),rewrite(62(2))].
345 x * (y @ x) = y * x * y'.  [para(80(a,1),27(a,2,2)),rewrite(62(2)),flip(a)].
397 (x * y)' = y' * x'.  [para(8(a,1),222(a,1,1,1)),flip(a)].
416 x * y * (y @ x) * z = y * x * z.  [back_rewrite(217),rewrite(397(4),62(2),62(2),1(4))].
510 (x @ y') * (x @ y) = e.  [para(72(a,1),273(a,1,2))].
736 (x @ y) * y = y * (x @ y).  [para(72(a,1),43(a,1,1))].
1236 ((x @ y') @ z') * z * (x @ y) = (x @ y) * z.  [para(510(a,1),49(a,1,2,2)),rewrite(272(3),105(3),29(3)),flip(a)].
1916 x' * y * x @ z = y @ z.  [para(245(a,1),5(a,2)),rewrite(397(3),272(2),1(8),736(7),1(10),44(9),6(5))].
1980 (x @ y) @ (z @ y) = e.  [back_rewrite(287),rewrite(1916(5),273(3)),flip(a)].
1986 (x @ y) @ z = e.  [back_rewrite(300),rewrite(1980(3)),flip(a)].
1998 (x @ y) * z = z * (x @ y).  [back_rewrite(1236),rewrite(1986(4),2(4)),flip(a)].
2192 x * (y @ z) @ u = x @ u.  [para(1986(a,1),6(a,1,2)),rewrite(29(3)),flip(a)].
2197 x * y @ z = y * x @ z.  [para(335(a,1),6(a,2,1)),rewrite(2192(4),6(3))].
2599 (x @ y) * y * x = x * y.  [para(139(a,1),345(a,1,2)),rewrite(1998(3,R),1(6),54(5),29(5))].
2637 (x @ y) * y * x * z = x * y * z.  [para(2599(a,1),1(a,1,1)),rewrite(1(2),1(5)),flip(a)].
2667 (x @ y) * z * y * x = z * x * y.  [para(2197(a,1),2599(a,1,1)),rewrite(14(5),2637(5),1(6))].
10648 $F # answer(E).  [para(2667(a,2),7(a,1,2,2)),rewrite(416(13)),xx(a)].

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

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

Given=368. Generated=169112. Kept=10646. proofs=1.
Usable=289. Sos=6435. Demods=1903. Limbo=2, Disabled=3926. Hints=0.
Weight_deleted=12333. Literals_deleted=0.
Forward_subsumed=144029. Back_subsumed=1159.
Sos_limit_deleted=2103. Sos_displaced=0. Sos_removed=0.
New_demodulators=4548 (6 lex), Back_demodulated=2761. Back_unit_deleted=0.
Demod_attempts=2978415. Demod_rewrites=629090.
Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0.
Nonunit_fsub_feature_tests=0. Nonunit_bsub_feature_tests=0.
Megabytes=6.75.
User_CPU=4.75, System_CPU=0.05, Wall_clock=5.

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

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

THEOREM PROVED

Exiting with 1 proof.

Process 11354 exit (max_proofs) Sat Aug 12 20:59:56 2006