============================== Prover9 ===============================
Prover9 (32) version June-2006C, June 2006.
Process 13119 was started by mccune on cleo.thornwood,
Mon Jun 19 16:41:29 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).

clauses(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


clauses(sos).
(x @ y) * (z @ y) = x * z @ y.
end_of_list.

clauses(sos).
A * B * C * B * A != B * A * C * A * B # answer(E).
end_of_list.

============================== end of input ==========================

============================== PROCESS INITIAL CLAUSES ===============

% Clauses before input processing:

clauses(usable).
end_of_list.

clauses(sos).
1 (x * y) * z = x * y * z.  [input].
2 e * x = x.  [input].
3 x ' * x = e.  [input].
4 x @ y = x ' * y ' * x * y.  [input].
5 (x @ y) * (z @ y) = x * z @ y.  [input].
6 A * B * C * B * A != B * A * C * A * B # answer(E).  [input].
end_of_list.

clauses(demodulators).
end_of_list.

Predicate elimination: (none).

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:

clauses(usable).
end_of_list.

clauses(sos).
7 (x * y) * z = x * y * z.  [input].
8 e * x = x.  [input].
9 x ' * x = e.  [input].
10 x ' * y ' * x * y = x @ y.  [copy(4),flip(a)].
11 (x @ y) * (z @ y) = x * z @ y.  [input].
12 A * B * C * B * A != B * A * C * A * B # answer(E).  [input].
end_of_list.

clauses(demodulators).
7 (x * y) * z = x * y * z.  [input].
8 e * x = x.  [input].
9 x ' * x = e.  [input].
10 x ' * y ' * x * y = x @ y.  [copy(4),flip(a)].
11 (x @ y) * (z @ y) = x * z @ y.  [input].
end_of_list.

clauses(denials).
end_of_list.

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

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

% Starting search at 0.00 seconds.

given #1 (I,wt=11): 7 (x * y) * z = x * y * z.  [input].

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

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

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

given #5 (I,wt=13): 11 (x @ y) * (z @ y) = x * z @ y.  [input].

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

given #7 (F,wt=5): 16 e @ x = e.  [para(8(a,1),10(a,1,2,2)),demod(9(4),9(4)),flip(a)].

given #8 (F,wt=6): 17 x ' @ x = e.  [para(9(a,1),10(a,1,2,2)),demod(13(6)),flip(a)].

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

given #10 (T,wt=5): 28 x @ x = e.  [para(13(a,1),10(a,1,2)),demod(9(2)),flip(a)].

given #11 (A,wt=17): 14 x ' * y ' * x * y * z = (x @ y) * z.  [para(10(a,1),7(a,1,1)),demod(7(7),7(6)),flip(a)].

given #12 (F,wt=5): 34 x * e = x.  [back_demod(26),demod(31(4))].

given #13 (F,wt=4): 57 e ' = e.  [para(34(a,1),9(a,1))].

given #14 (T,wt=5): 58 x @ e = e.  [para(34(a,1),10(a,1,2,2)),demod(57(3),8(3),9(2)),flip(a)].

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

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

given #17 (F,wt=5): 67 x ' ' = x.  [para(31(a,1),34(a,1)),demod(34(2)),flip(a)].

given #18 (F,wt=6): 59 x * x ' = e.  [para(31(a,1),9(a,1))].

given #19 (T,wt=6): 78 x @ x ' = e.  [para(67(a,1),17(a,1,1))].

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

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

given #22 (F,wt=8): 77 x ' @ y = y @ x.  [back_demod(69),demod(74(6))].

given #23 (F,wt=8): 85 x @ y ' = y @ x.  [para(78(a,1),11(a,1,2)),demod(34(4),83(5))].

given #24 (T,wt=9): 37 x * y @ x = y @ x.  [para(28(a,1),11(a,1,1)),demod(8(3)),flip(a)].

given #25 (T,wt=9): 38 x * y @ y = x @ y.  [para(28(a,1),11(a,1,2)),demod(34(3)),flip(a)].

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

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

given #28 (F,wt=9): 125 x ' @ y = x @ y '.  [para(85(a,1),77(a,1)),flip(a)].

given #29 (T,wt=9): 144 x @ y * x = x @ y.  [para(13(a,1),38(a,1,1)),demod(137(5))].

given #30 (T,wt=10): 22 x ' * y @ x = y @ x.  [para(17(a,1),11(a,1,1)),demod(8(3)),flip(a)].

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

given #32 (F,wt=7): 203 (x @ y) @ x = e.  [para(10(a,1),22(a,1,1)),demod(130(6),9(4),16(4))].

given #33 (F,wt=7): 237 (x @ y) @ y = e.  [para(85(a,1),203(a,1,1))].

given #34 (T,wt=8): 233 x ' @ (x @ y) = e.  [para(203(a,1),77(a,2))].

given #35 (T,wt=7): 257 x @ (y @ x) = e.  [para(77(a,1),233(a,1,2)),demod(67(2))].

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

given #37 (F,wt=7): 260 x @ (x @ y) = e.  [para(110(a,1),233(a,1,2)),demod(67(2))].

given #38 (F,wt=8): 234 (x @ y) @ y ' = e.  [para(77(a,1),203(a,1,1))].

given #39 (T,wt=8): 236 x @ (x ' @ y) = e.  [para(203(a,1),85(a,1)),flip(a)].

given #40 (T,wt=8): 238 (x @ y ') @ y = e.  [para(85(a,2),203(a,1,1))].

given #41 (A,wt=12): 32 x ' * y * x = y * (y @ x).  [back_demod(29),demod(31(4)),flip(a)].

given #42 (F,wt=8): 242 (x @ y) @ x ' = e.  [para(110(a,1),203(a,1,1))].

given #43 (F,wt=8): 243 (x ' @ y) @ x = e.  [para(125(a,2),203(a,1,1))].

given #44 (T,wt=8): 252 x ' @ (y @ x) = e.  [para(237(a,1),77(a,2))].

given #45 (T,wt=8): 253 x @ (y @ x ') = e.  [para(237(a,1),85(a,1)),flip(a)].

given #46 (A,wt=10): 36 x * y ' @ y = x @ y.  [back_demod(23),demod(34(5))].

given #47 (F,wt=9): 227 (x * y) ' * x = y '.  [para(59(a,1),24(a,1,2,2)),demod(34(4))].

given #48 (F,wt=9): 239 (x @ y) @ y * x = e.  [para(37(a,1),203(a,1,1))].

given #49 (T,wt=9): 240 (x @ y) @ x * y = e.  [para(38(a,1),203(a,1,1))].

given #50 (T,wt=9): 277 (x @ y) ' = x ' @ y.  [para(59(a,1),30(a,1,2,1)),demod(16(4),34(4))].

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

given #52 (F,wt=9): 278 (x @ y) * (y @ x) = e.  [para(78(a,1),30(a,2)),demod(277(3),110(3),83(4))].

given #53 (F,wt=9): 307 (x @ y) @ (y @ x) = e.  [back_demod(157),demod(277(2),277(4),102(5),9(2),16(2)),flip(a)].

given #54 (T,wt=9): 408 x @ x * y = x @ y.  [para(227(a,1),22(a,1,1)),demod(147(3)),flip(a)].

given #55 (T,wt=9): 444 x * y @ y * x = e.  [para(239(a,1),37(a,2)),demod(7(3),340(3))].

given #56 (A,wt=13): 43 x ' * y * x = (x @ y ') * y.  [para(9(a,1),14(a,1,2,2,2)),demod(34(5),31(4))].

given #57 (F,wt=10): 83 x * y @ y ' = y @ x.  [para(59(a,1),15(a,1,2,2,2)),demod(67(4),34(4),74(4)),flip(a)].

given #58 (F,wt=10): 137 x ' @ x * y = y @ x.  [para(37(a,1),77(a,2))].

given #59 (T,wt=10): 147 x ' @ y * x = y @ x.  [para(38(a,1),77(a,2))].

given #60 (T,wt=10): 244 (x @ y) @ y ' * x = e.  [para(22(a,1),203(a,1,1))].

given #61 (A,wt=22): 46 x ' * y * x * (y @ z) = (x @ y ') * z ' * y * z.  [para(10(a,1),14(a,1,2,2,2)),demod(31(6))].

given #62 (F,wt=10): 293 (x @ y) @ (x ' @ y) = e.  [back_demod(155),demod(277(2),277(5),67(4),11(4),9(2),16(2)),flip(a)].

given #63 (F,wt=10): 294 (x ' @ y) @ (x @ y) = e.  [back_demod(152),demod(277(3),67(2),277(3),11(4),59(2),16(2)),flip(a)].

given #64 (T,wt=10): 325 (x ' @ y) @ y * x = e.  [para(144(a,1),234(a,1,1)),demod(125(4,R),277(2))].

given #65 (T,wt=10): 330 (x @ y) @ (y ' @ x) = e.  [para(236(a,1),37(a,2)),demod(48(3),326(5))].

given #66 (A,wt=12): 48 (x ' @ y) * x = x * (y @ x).  [para(10(a,1),14(a,1,2)),demod(31(4)),flip(a)].

given #67 (F,wt=10): 368 (x @ y) * (x @ y ') = e.  [back_demod(332),demod(365(6))].

given #68 (F,wt=10): 374 (x ' @ y) @ x * y = e.  [para(38(a,1),242(a,1,1)),demod(125(4,R),277(2))].

given #69 (T,wt=10): 393 (x @ y) @ (x @ y ') = e.  [para(253(a,1),22(a,2)),demod(277(3),110(3),389(5))].

given #70 (T,wt=10): 398 (x @ y) @ x * y ' = e.  [para(36(a,1),203(a,1,1))].

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

given #72 (F,wt=10): 402 (x * y) ' = y ' * x '.  [para(13(a,1),227(a,1,1,1)),flip(a)].

given #73 (F,wt=10): 442 (x @ y) @ x ' * y = e.  [para(85(a,1),239(a,1,1))].

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

given #75 (T,wt=10): 462 (x @ y) @ y * x ' = e.  [para(85(a,1),240(a,1,1))].

given #76 (A,wt=21): 50 x ' * y ' * x * y * z @ u = (x @ y) * z @ u.  [para(14(a,1),11(a,2,1)),demod(11(8))].

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

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

given #79 (T,wt=10): 520 (x ' @ y) @ (y @ x) = e.  [para(307(a,1),77(a,2)),demod(277(2))].

given #80 (T,wt=10): 521 (x @ y ') @ (x @ y) = e.  [para(77(a,1),307(a,1,2))].

given #81 (A,wt=16): 52 x ' * y * x * z = y * (y @ x) * z.  [para(14(a,1),13(a,1,2)),demod(31(5)),flip(a)].

given #82 (F,wt=10): 534 x @ y ' * x * y = e.  [para(32(a,2),408(a,1,2)),demod(260(6))].

given #83 (F,wt=10): 542 (x @ y) @ (y @ x ') = e.  [para(10(a,1),444(a,1,1)),demod(7(6),7(5),61(6))].

given #84 (T,wt=10): 543 (x @ y ') @ (y @ x) = e.  [para(10(a,1),444(a,1,2)),demod(7(5),7(4),61(5))].

given #85 (T,wt=10): 547 x @ y * x * y ' = e.  [para(13(a,1),444(a,1,1)),demod(7(3))].

given #86 (A,wt=17): 54 x ' * y * x * z = (x @ y ') * y * z.  [para(13(a,1),14(a,1,2,2,2)),demod(31(5))].

given #87 (F,wt=11): 84 x * y @ x ' = y @ x '.  [para(78(a,1),11(a,1,1)),demod(8(4)),flip(a)].

given #88 (F,wt=11): 138 x @ x ' * y = y @ x '.  [para(37(a,1),85(a,1)),flip(a)].

given #89 (T,wt=11): 148 x @ y * x ' = y @ x '.  [para(38(a,1),85(a,1)),flip(a)].

given #90 (T,wt=11): 151 (x @ y) * (y @ x) * z = z.  [back_demod(139),demod(147(4))].

given #91 (A,wt=16): 56 (x ' @ y) * x * z = x * (y @ x) * z.  [para(14(a,1),14(a,1,2)),demod(31(5)),flip(a)].

given #92 (F,wt=11): 206 (x @ y) * z @ x = z @ x.  [para(14(a,1),22(a,1,1)),demod(130(8),13(6))].

given #93 (F,wt=9): 1418 x @ (y @ (x @ z)) = e.  [para(32(a,2),206(a,1,1)),demod(1407(5),9(2),16(2),1291(4)),flip(a)].

given #94 (T,wt=9): 1456 x @ ((x @ y) @ z) = e.  [para(77(a,1),1418(a,1,2))].

given #95 (T,wt=9): 1459 x @ (y @ (z @ x)) = e.  [para(85(a,1),1418(a,1,2,2))].

given #96 (A,wt=14): 61 x ' * y * x * y ' = x @ y '.  [para(31(a,1),10(a,1,2))].

given #97 (F,wt=9): 1478 x @ ((y @ x) @ z) = e.  [para(85(a,1),1456(a,1,2,1))].

given #98 (F,wt=10): 1453 x @ ((x ' @ y) @ z) = e.  [para(1418(a,1),77(a,1)),demod(1291(5)),flip(a)].

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

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

given #101 (A,wt=14): 62 x * y ' * x ' * y = x ' @ y.  [para(31(a,1),10(a,1))].

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

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

given #104 (T,wt=10): 1463 x @ (y @ (x ' @ z)) = e.  [para(125(a,1),1418(a,1,2)),demod(277(2))].

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

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

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

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

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

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

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

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

given #113 (F,wt=11): 232 x * (y @ z) @ y = x @ y.  [para(203(a,1),11(a,1,2)),demod(34(3)),flip(a)].

given #114 (T,wt=11): 249 (x @ y) * z @ y = z @ y.  [para(237(a,1),11(a,1,1)),demod(8(3)),flip(a)].

given #115 (T,wt=11): 250 x * (y @ z) @ z = x @ z.  [para(237(a,1),11(a,1,2)),demod(34(3)),flip(a)].

given #116 (A,wt=18): 72 x ' * y * z * x = y * z * (y * z @ x).  [para(15(a,1),13(a,1,2)),demod(67(3),7(4)),flip(a)].

given #117 (F,wt=7): 1991 (x @ y) @ z = e.  [back_demod(305),demod(1985(3)),flip(a)].

given #118 (F,wt=7): 2019 x @ (y @ z) = e.  [back_demod(1793),demod(1991(8)),flip(a)].

given #119 (T,wt=11): 340 x * y * (y @ x) = y * x.  [para(32(a,1),13(a,1,2)),demod(67(2))].

given #120 (T,wt=11): 453 x ' * y ' @ y * x = e.  [para(239(a,1),36(a,2)),demod(402(3),435(7))].

given #121 (A,wt=14): 81 x ' * y ' * x = (x @ y) * y '.  [para(59(a,1),14(a,1,2,2,2)),demod(34(4))].

given #122 (F,wt=11): 555 x ' * y ' @ x * y = e.  [para(444(a,1),77(a,2)),demod(402(2))].

given #123 (F,wt=11): 556 x * y @ x ' * y ' = e.  [para(444(a,1),85(a,2)),demod(402(3))].

given #124 (T,wt=11): 656 x ' * y @ y ' * x = e.  [para(244(a,1),36(a,2)),demod(402(4),67(4),649(7))].

given #125 (T,wt=11): 785 x * y ' @ y * x ' = e.  [para(398(a,1),36(a,2)),demod(402(4),67(3),780(7))].

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

given #127 (F,wt=11): 789 x * y ' @ x ' * y = e.  [para(398(a,1),137(a,2)),demod(402(3),67(2),7(6),399(6))].

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

given #129 (T,wt=11): 901 x ' * y @ x * y ' = e.  [para(462(a,1),22(a,2)),demod(402(3),67(2),7(4),399(4))].

given #130 (T,wt=11): 1134 x @ y ' * x ' * y = e.  [para(534(a,1),368(a,1,1)),demod(402(5),402(3),67(6),7(5),8(7))].

given #131 (A,wt=12): 90 (x ' @ y) * (x @ y) * z = z.  [para(9(a,1),19(a,1,1,1)),demod(16(2),8(2)),flip(a)].

given #132 (F,wt=11): 1180 x @ y * x ' * y ' = e.  [para(547(a,1),368(a,1,1)),demod(402(5),402(4),67(3),7(5),8(7))].

given #133 (F,wt=11): 1324 x @ (y @ x) * z = x @ z.  [para(56(a,2),10(a,1,2,2)),demod(402(4),277(4),7(10),519(9),10(5)),flip(a)].

given #134 (T,wt=11): 2003 (x @ y) * z = z * (x @ y).  [back_demod(1241),demod(1991(4),8(4)),flip(a)].

given #135 (T,wt=11): 2081 (x @ y) * z @ u = z @ u.  [back_demod(815),demod(2062(8),90(6)),flip(a)].

given #136 (A,wt=12): 95 (x @ y) * (x ' @ y) * z = z.  [para(59(a,1),19(a,1,1,1)),demod(16(2),8(2)),flip(a)].

given #137 (F,wt=11): 2197 x * (y @ z) @ u = x @ u.  [para(1991(a,1),11(a,1,2)),demod(34(3)),flip(a)].

given #138 (F,wt=11): 2202 x * y @ z = y * x @ z.  [para(340(a,1),11(a,2,1)),demod(2197(4),11(3))].

given #139 (T,wt=11): 2224 (x @ y) * z * (y @ x) = z.  [para(340(a,1),151(a,1,2)),demod(2019(6),34(6))].

given #140 (T,wt=11): 2472 x @ y * (z @ u) = x @ y.  [para(2081(a,1),144(a,1)),demod(193(4),2081(6))].

given #141 (A,wt=12): 97 (x @ y ') * z = (y @ x) * z.  [para(78(a,1),19(a,2,2,1)),demod(83(3),8(6)),flip(a)].

given #142 (F,wt=11): 2475 x @ (y @ z) * u = x @ u.  [para(83(a,1),2081(a,2)),demod(601(5))].

given #143 (F,wt=12): 350 x * (y @ x) = y * x * y '.  [para(85(a,1),32(a,2,2)),demod(67(2)),flip(a)].

given #144 (T,wt=11): 2604 (x @ y) * y * x = x * y.  [para(144(a,1),350(a,1,2)),demod(2003(3,R),7(6),59(5),34(5))].

given #145 (T,wt=11): 2674 x @ y * z = x @ z * y.  [para(2604(a,1),2475(a,1,2))].

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

given #147 (F,wt=12): 396 (x ' @ y) * z = (y @ x) * z.  [para(36(a,1),14(a,2,1)),demod(7(8),13(7),132(7))].

given #148 (F,wt=12): 569 (x @ y) * x ' * y * x = y.  [para(43(a,2),13(a,1,2)),demod(277(3),110(3))].

given #149 (T,wt=12): 571 x * (y @ x) = x * (x @ y ').  [para(43(a,1),14(a,1,2,2)),demod(67(2),365(5),48(6)),flip(a)].

given #150 (T,wt=12): 582 x * (y @ x ') = x * (x @ y).  [para(43(a,1),32(a,1)),demod(578(3))].

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

given #152 (F,wt=12): 598 x * y * (x @ y ') = y * x.  [back_demod(568),demod(578(3))].

given #153 (F,wt=12): 754 (x @ y) * (x @ y ') * z = z.  [para(368(a,1),7(a,1,1)),demod(8(2)),flip(a)].

given #154 (T,wt=12): 1000 (x @ y ') * (x @ y) * z = z.  [para(515(a,1),7(a,1,1)),demod(8(2)),flip(a)].

given #155 (T,wt=12): 1228 x * y * (x ' @ y) = y * x.  [para(54(a,2),48(a,1)),demod(402(2),402(4),67(2),67(2),402(3),7(5),62(6),7(4),137(8),7(7),340(7))].

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

given #157 (F,wt=11): 2993 x * x @ y = x @ y * y.  [back_demod(825),demod(2983(7),13(5)),flip(a)].

given #158 (F,wt=12): 1921 x ' * y * x @ z = y @ z.  [para(250(a,1),10(a,2)),demod(402(3),277(2),7(8),741(7),7(10),49(9),11(5))].

given #159 (T,wt=12): 2044 (x ' @ y) * z = z * (y @ x).  [back_demod(1213),demod(1991(6),8(7))].

given #160 (T,wt=12): 2050 (x ' @ y) * z * (x @ y) = z.  [back_demod(587),demod(1991(8),34(7))].

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

given #162 (F,wt=12): 2053 x ' * (y @ z) * x = y @ z.  [back_demod(344),demod(1991(4),34(4),10(5)),flip(a)].

given #163 (F,wt=12): 2063 x * (y @ z) * x ' = y @ z.  [back_demod(1785),demod(2019(4),8(3)),flip(a)].

given #164 (T,wt=12): 2078 x * (y ' @ z) = x * (z @ y).  [back_demod(516),demod(2053(5),2019(5),8(6))].

given #165 (T,wt=12): 2082 x * y * x ' @ z = y @ z.  [back_demod(910),demod(2080(3)),flip(a)].

given #166 (A,wt=17): 103 (x @ y) * z = y * x ' * y ' * x * z.  [para(77(a,1),14(a,2,1)),demod(67(2)),flip(a)].

given #167 (F,wt=12): 2409 (x @ y) * z * (x ' @ y) = z.  [para(90(a,1),340(a,2)),demod(1991(9),34(6),7(5))].

given #168 (F,wt=12): 2452 (x @ y) * z = z * (y ' @ x).  [para(77(a,1),2003(a,1,1))].

given #169 (T,wt=12): 2453 (x @ y) * z = z * (y @ x ').  [para(85(a,1),2003(a,1,1))].

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

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

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

given #173 (F,wt=12): 2531 x * y @ z ' = z @ y * x.  [para(2202(a,1),85(a,1))].

given #174 (T,wt=12): 2559 (x @ y) * z * (x @ y ') = z.  [para(77(a,1),2224(a,1,1))].

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

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

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

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

given #179 (T,wt=12): 2644 (x ' @ y) * x * y = y * x.  [para(2604(a,1),13(a,1,2)),demod(277(2))].

given #180 (T,wt=12): 2650 (x @ y ') * x * y = y * x.  [para(85(a,2),2604(a,1,1))].

given #181 (A,wt=25): 111 (x @ y) * (z @ y) * x * z * y = x * z * y * (x * z @ y).  [back_demod(75),demod(110(4),19(5))].

given #182 (F,wt=12): 3025 x ' @ y * y = y @ x * x.  [para(2993(a,1),77(a,2))].

given #183 (F,wt=12): 3027 x * x @ y ' = y * y @ x.  [para(2993(a,2),85(a,2))].

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

given #185 (T,wt=13): 130 x * y * z @ y = x * z @ y.  [para(37(a,1),11(a,1,2)),demod(11(3)),flip(a)].

given #186 (A,wt=15): 114 (x @ y) * (z @ x ') = y * z @ x '.  [para(85(a,1),11(a,1,1))].

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

given #188 (F,wt=13): 174 x * y * x ' * y ' = x @ y.  [para(110(a,1),10(a,2)),demod(67(2),67(2))].

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

given #190 (T,wt=13): 280 (x @ y) * (y * z @ x) = z @ x.  [para(77(a,2),30(a,1,1,1)),demod(277(3),67(2))].

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

given #192 (F,wt=13): 347 x * (x @ y ') = y * x * y '.  [para(67(a,1),32(a,1,1)),flip(a)].

given #193 (F,wt=13): 349 x ' * y * x = y * (x ' @ y).  [para(77(a,2),32(a,2,2))].

given #194 (T,wt=13): 351 x ' * y * x = y * (x @ y ').  [para(85(a,2),32(a,2,2))].

given #195 (T,wt=13): 356 x * (x ' @ y) = y * x * y '.  [para(125(a,2),32(a,2,2)),demod(67(2)),flip(a)].

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

given #197 (F,wt=13): 399 x * y ' * (x @ y) = y ' * x.  [para(36(a,1),32(a,2,2)),demod(7(4),9(3),34(3),7(6)),flip(a)].

given #198 (F,wt=13): 426 x * y @ z = z @ y ' * x '.  [back_demod(118),demod(402(4))].

given #199 (T,wt=13): 519 (x ' @ y) * (y ' @ x) * z = z.  [para(307(a,1),14(a,2,1)),demod(277(2),277(4),151(8),8(8))].

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

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

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

given #203 (F,wt=13): 832 x ' * y ' @ z = z @ y * x.  [para(402(a,1),77(a,1,1))].

given #204 (T,wt=13): 1035 x ' * y = y * (y @ x) * x '.  [para(59(a,1),52(a,1,2,2)),demod(34(3))].

given #205 (T,wt=13): 1107 (x ' @ y) * z = (x @ y ') * z.  [para(521(a,1),52(a,2,2,1)),demod(277(2),1000(7),8(7))].

given #206 (A,wt=17): 119 x ' * y * x * y ' * z = (y @ x) * z.  [para(85(a,1),14(a,2,1)),demod(67(3))].

given #207 (F,wt=13): 1290 (x @ y ') * (y @ x ') * z = z.  [para(125(a,1),151(a,1,1))].

given #208 (F,wt=13): 2043 (x ' @ y) * z = z * (x @ y ').  [back_demod(1231),demod(1991(6),8(8))].

given #209 (T,wt=13): 2076 x * (y ' @ z) = x * (y @ z ').  [back_demod(759),demod(2053(5),2019(5),8(7))].

given #210 (T,wt=13): 2207 x ' * y * (x @ y) = y * x '.  [para(85(a,1),340(a,1,2,2))].

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

given #212 (F,wt=13): 2455 (x @ y ') * z = z * (x ' @ y).  [para(125(a,1),2003(a,1,1))].

given #213 (F,wt=13): 2532 x * y @ z = z @ x ' * y '.  [para(2202(a,1),85(a,2)),demod(402(2)),flip(a)].

given #214 (T,wt=13): 2555 (x @ y) * (z * y @ x) = z @ x.  [para(11(a,1),2224(a,1,2))].

given #215 (T,wt=13): 2561 (x @ y ') * z * (y @ x ') = z.  [para(125(a,1),2224(a,1,1))].

given #216 (A,wt=20): 124 (x @ y) * (z @ y) * u = (x @ y) * (y @ z ') * u.  [para(85(a,2),19(a,2,2,1)),demod(19(3))].

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

given #218 (F,wt=13): 2648 x ' * y = (y @ x) * y * x '.  [para(77(a,1),2604(a,1,1)),flip(a)].

given #219 (T,wt=12): 4914 x * (y @ x) * y * x ' = y.  [para(2648(a,1),13(a,1,2)),demod(67(2))].

given #220 (T,wt=13): 2649 (x @ y) * x ' * y = y * x '.  [para(85(a,1),2604(a,1,1))].

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

given #222 (F,wt=13): 2680 x ' * y ' @ z = z @ x * y.  [para(2674(a,1),77(a,2)),demod(402(2))].

given #223 (F,wt=13): 2959 (x @ y) * (x @ z) = x @ y * z.  [para(83(a,1),101(a,1,2)),demod(67(2),601(7))].

given #224 (T,wt=13): 2971 x ' * y @ z = z @ y ' * x.  [para(656(a,1),101(a,1,2)),demod(402(3),67(3),34(5),2294(9))].

given #225 (T,wt=13): 2972 x * y ' @ z = z @ y * x '.  [para(785(a,1),101(a,1,2)),demod(402(3),67(2),34(5),2309(9))].

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

given #227 (F,wt=13): 2975 x ' * x ' @ y = y * y @ x.  [para(101(a,1),100(a,2))].

given #228 (F,wt=13): 2980 x * y ' @ z = z @ x ' * y.  [back_demod(2845),demod(2959(7))].

given #229 (T,wt=13): 2981 x ' * y @ z = z @ x * y '.  [back_demod(2715),demod(2959(7))].

given #230 (T,wt=13): 3026 x @ y ' * y ' = y @ x * x.  [para(2993(a,1),85(a,1))].

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

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

given #233 (F,wt=13): 3818 x ' @ y * y = x * x @ y '.  [para(3025(a,2),85(a,2)),flip(a)].

given #234 (T,wt=13): 3917 x * y @ x * x = y * y @ x.  [para(130(a,1),2993(a,1)),demod(7(2),37(3)),flip(a)].

given #235 (T,wt=13): 4020 x @ y * x * z = x @ y * z.  [para(340(a,1),193(a,1,2,2)),demod(2197(5),2197(7))].

given #236 (A,wt=17): 177 (x @ y) * z = x * y * x ' * y ' * z.  [para(110(a,1),14(a,2,1)),demod(67(2),67(2)),flip(a)].

given #237 (F,wt=13): 4033 x * x @ y * x = x @ y * y.  [para(193(a,1),2993(a,2)),demod(7(5),4020(6))].

given #238 (F,wt=13): 4327 x * y * z @ y * x * z = e.  [para(340(a,1),539(a,1,1,2)),demod(7(6),2702(7))].

given #239 (T,wt=13): 5022 x * y @ y * y = x @ y * y.  [para(128(a,1),2993(a,1)),demod(7(2),4020(3),7(5),7(7),7(8),7(7),525(9),4025(7)),flip(a)].

given #240 (T,wt=13): 5087 (x @ y) * (y @ x * z) = y @ z.  [para(2959(a,1),151(a,1,2))].

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

given #242 (F,wt=13): 5098 (x @ y) * (y @ z * x) = y @ z.  [para(2959(a,1),2224(a,1,2))].

given #243 (F,wt=13): 5741 x * y @ x * x = y @ x * x.  [para(3917(a,2),10(a,2)),demod(402(2),7(6),7(8),3778(7),13(5)),flip(a)].

given #244 (T,wt=13): 5802 x * x @ x * y = x @ y * y.  [para(4020(a,1),2993(a,2)),demod(7(5),408(6))].

given #245 (T,wt=13): 5907 x * x @ y * x = x * x @ y.  [para(4033(a,2),10(a,2)),demod(402(3),7(7),427(8),2173(4)),flip(a)].

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

given #247 (F,wt=13): 5993 x * y * z @ x * z * y = e.  [para(4327(a,1),2202(a,1)),demod(7(3)),flip(a)].

given #248 (F,wt=13): 6181 x * x @ x * y = x * x @ y.  [para(5802(a,2),10(a,2)),demod(402(3),7(7),427(8),2173(4)),flip(a)].

given #249 (T,wt=13): 6332 x * y * z @ z * y * x = e.  [para(5993(a,1),2202(a,1)),demod(7(3)),flip(a)].

given #250 (T,wt=14): 204 x * y ' * z @ y = x * z @ y.  [para(22(a,1),11(a,1,2)),demod(11(3)),flip(a)].

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

given #252 (F,wt=14): 282 (x @ y) * (x * z @ y ') = y @ z.  [para(85(a,1),30(a,2)),demod(277(3),110(3))].

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

given #254 (T,wt=14): 354 x ' * (x @ y) = y * x ' * y '.  [para(110(a,1),32(a,2,2)),demod(67(2)),flip(a)].

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

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

given #257 (F,wt=14): 410 x ' * y ' * x * (y @ x) = y '.  [back_demod(369),demod(402(4),402(2),67(5),7(4),7(6),7(5))].

given #258 (F,wt=14): 581 x ' * (y @ x) = x ' * (x @ y ').  [para(43(a,1),32(a,1,2)),demod(402(2),578(6),7(7),13(6),147(8)),flip(a)].

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

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

given #261 (A,wt=18): 182 (x @ y ') * z = x * y ' * x ' * y * z.  [para(125(a,1),14(a,2,1)),demod(67(2)),flip(a)].

given #262 (F,wt=14): 806 x ' * y ' @ z = y * x @ z '.  [para(125(a,2),49(a,2)),demod(67(3),797(8),402(5)),flip(a)].

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

given #264 (T,wt=14): 1184 (x @ y) * y ' * x ' * y = x '.  [para(9(a,1),54(a,1,2)),demod(34(3),402(3),402(5),67(3),67(3),408(3),402(4),7(6)),flip(a)].

given #265 (T,wt=14): 1193 x ' * y = (x @ y ') * y * x '.  [para(59(a,1),54(a,1,2,2)),demod(34(3))].

given #266 (A,wt=18): 183 x ' * y * x * y ' * z = (x ' @ y) * z.  [para(125(a,2),14(a,2,1)),demod(67(3))].

given #267 (F,wt=14): 1215 x ' @ y * x * z = y * z @ x.  [para(54(a,1),408(a,1,2)),demod(1113(6)),flip(a)].

given #268 (F,wt=14): 1266 (x ' @ y) * y ' * x = x * y '.  [para(138(a,1),48(a,2,2)),demod(402(3),67(3),38(3),7(10),340(10))].

given #269 (T,wt=14): 2173 x * y @ y ' * x = y * y @ x.  [para(72(a,2),49(a,1,2,2)),demod(427(8),141(7))].

given #270 (T,wt=14): 2191 x * y ' * (y @ x ') = y ' * x.  [para(61(a,1),72(a,1,2)),demod(402(3),67(2),7(5),901(11),34(8))].

given #271 (A,wt=17): 195 (x @ y) * (z @ y * x) = x * z @ y * x.  [para(144(a,1),11(a,1,1))].

given #272 (F,wt=14): 2193 x ' * y * (y ' @ x) = y * x '.  [para(62(a,1),72(a,1,2)),demod(402(3),67(3),7(5),789(11),34(8))].

given #273 (F,wt=14): 2241 (x @ y) * x ' = y * x ' * y '.  [para(77(a,1),81(a,2,1)),demod(67(2)),flip(a)].

given #274 (T,wt=14): 2323 x ' * (y @ z) = (z ' @ y) * x '.  [para(278(a,1),87(a,1,2,2)),demod(277(2),34(5),1991(6),8(9)),flip(a)].

given #275 (T,wt=14): 2503 (x @ y) * x * y ' * x ' = y '.  [para(81(a,2),95(a,1,2)),demod(67(3))].

given #276 (A,wt=18): 289 (x ' @ y) * (x * z @ y * x) = z @ y * x.  [para(144(a,1),30(a,1,1,1)),demod(277(2))].

given #277 (F,wt=14): 2533 x ' * y ' @ z ' = x * y @ z.  [para(2202(a,1),110(a,2)),demod(402(2))].

given #278 (F,wt=14): 2534 x ' * y ' @ z = x * y @ z '.  [para(2202(a,1),125(a,2)),demod(402(2))].

given #279 (T,wt=14): 2681 x ' @ y ' * z ' = x @ y * z.  [para(2674(a,1),110(a,2)),demod(402(3))].

given #280 (T,wt=14): 2682 x ' @ y * z = x @ y ' * z '.  [para(2674(a,1),125(a,1)),demod(402(5))].

given #281 (A,wt=16): 336 x * y ' * z * y = x * z * (z @ y).  [para(32(a,1),7(a,2,2)),demod(7(4))].

given #282 (F,wt=14): 2713 x @ y ' * z = (x @ z) * (y @ x).  [para(99(a,1),85(a,2)),demod(402(3),67(3))].

given #283 (F,wt=14): 2718 x ' * y @ z ' = x * y ' @ z.  [para(125(a,2),99(a,2,2)),demod(101(9))].

given #284 (T,wt=14): 2750 x ' * y @ z = (y @ z) * (z @ x).  [para(99(a,2),340(a,2)),demod(2019(5),34(4)),flip(a)].

given #285 (T,wt=14): 2751 x * y ' @ z = (z @ y) * (x @ z).  [para(340(a,1),99(a,1,1)),demod(2197(8))].

given #286 (A,wt=21): 342 x ' * y * x * z * (z @ y) = (x @ y ') * z * y.  [para(32(a,1),14(a,1,2,2,2)),demod(67(3))].

given #287 (F,wt=14): 2836 x ' * y @ z = x * y ' @ z '.  [back_demod(2803),demod(2824(8)),flip(a)].

given #288 (F,wt=14): 2843 x @ y * z ' = (z @ x) * (x @ y).  [para(100(a,1),85(a,2)),demod(402(3),67(2))].

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

given #290 (T,wt=14): 2992 (x ' @ y) * (y @ z) = y @ x * z.  [back_demod(1094),demod(2983(7),13(5)),flip(a)].

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

given #292 (F,wt=14): 2997 (x @ y) * (z ' @ x) = x @ y * z.  [back_demod(2889),demod(2992(4)),flip(a)].

given #293 (F,wt=14): 3034 x ' @ y * y = x ' * x ' @ y.  [para(2993(a,1),277(a,1,1)),demod(277(3),402(5))].

given #294 (T,wt=14): 3124 x * y ' * x ' * (x @ y) = y '.  [para(2050(a,1),87(a,2)),demod(67(2))].

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

given #296 (A,wt=22): 404 (x ' @ y) * z * (y @ z) = y * z * x * y ' * x '.  [para(227(a,1),14(a,1,2,2)),demod(7(2),402(3),402(2),7(5),402(6),402(4),67(2),67(2),67(3),7(2),7(6),7(5),7(8),402(9),402(8),7(11),395(12),19(11),48(11)),flip(a)].

given #297 (F,wt=14): 3270 x ' * (y ' @ z) = (z @ y) * x '.  [para(2452(a,1),402(a,1,1)),demod(402(4),277(3),67(2),277(6)),flip(a)].

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

given #299 (T,wt=14): 3564 (x @ y) * (x ' @ z * y) = z @ x.  [para(278(a,1),105(a,2,2)),demod(2003(5,R),34(8))].

given #300 (T,wt=14): 3588 (x @ y) * (x ' @ y * z) = z @ x.  [para(105(a,2),2224(a,1)),demod(2003(5,R))].

given #301 (A,wt=21): 406 x * y * z ' * x ' * z * y ' = z * y ' @ x.  [para(227(a,1),15(a,1,2,2,2)),demod(402(2),402(5),402(4),67(2),67(2),7(3),7(8),7(7),402(10),395(13))].

given #302 (F,wt=14): 3817 x * y ' @ y * x = x @ y * y.  [para(3025(a,1),10(a,2)),demod(67(2),402(2),7(7),429(8))].

given #303 (F,wt=14): 4179 x @ y ' * z = (y @ x) * (x @ z).  [para(100(a,1),116(a,2)),demod(2997(5))].

given #304 (T,wt=14): 4199 x * (x @ y) * y ' * x ' = y '.  [para(408(a,1),399(a,1,2,2)),demod(402(2),2003(5,R),402(8),7(10),9(9),34(9))].

given #305 (T,wt=14): 4215 x ' * (y @ z ') = (z @ y) * x '.  [para(399(a,1),97(a,1)),demod(1991(9),34(8))].

given #306 (A,wt=24): 407 x ' * y ' * (x ' * y ' @ z) = z ' * x ' * y ' * z.  [para(15(a,1),227(a,1,1,1)),demod(277(3),402(2),402(6),359(8),7(8),402(13),402(11),402(10),7(13),67(15),7(14),7(13))].

given #307 (F,wt=14): 4216 x ' * (y @ z) = (z @ y ') * x '.  [para(399(a,1),97(a,2)),demod(1991(5),34(5)),flip(a)].

given #308 (F,wt=14): 4600 x ' * y @ z ' = y ' * x @ z.  [para(2043(a,2),99(a,2)),demod(102(9))].

given #309 (T,wt=14): 4756 x * y ' @ z ' = y * x ' @ z.  [para(2455(a,1),100(a,2)),demod(101(9))].

given #310 (T,wt=14): 4788 x @ y * z ' = (x @ y) * (z @ x).  [para(2532(a,1),99(a,1)),demod(67(2))].

given #311 (A,wt=15): 411 x ' * (x ' @ y) = y ' * x ' * y.  [back_demod(401),demod(402(4),402(2),67(5),7(4)),flip(a)].

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

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

given #314 (T,wt=14): 5206 x ' @ y ' * z = x @ y * z '.  [para(2971(a,1),2531(a,1))].

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

given #316 (A,wt=20): 418 x * y * z ' * y ' * x ' * z = z @ x * y.  [back_demod(231),demod(402(3),402(2),7(5),7(6),7(5))].

given #317 (F,wt=14): 5913 x ' * y @ x * y = y @ x * x.  [para(4033(a,1),22(a,2)),demod(402(2),7(5),2118(7))].

given #318 (F,wt=14): 6025 x ' * y @ x * x = y @ x * x.  [para(5022(a,1),22(a,2)),demod(402(2),7(5),3073(7))].

given #319 (T,wt=14): 6027 x * y ' @ y * y = x @ y * y.  [para(5022(a,1),36(a,2)),demod(402(3),7(5),63(4))].

given #320 (T,wt=14): 6185 x ' * y @ y * x = y @ x * x.  [para(5802(a,1),22(a,2)),demod(402(2),7(5),13(4))].

given #321 (A,wt=17): 419 x ' * y ' @ y * x * z = z @ y * x.  [back_demod(230),demod(402(2))].

given #322 (F,wt=14): 6186 x * y ' @ x * y = x @ y * y.  [para(5802(a,1),36(a,2)),demod(402(3),7(5),3183(7))].

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

given #324 (T,wt=14): 6370 x * x @ y * x ' = x * x @ y.  [para(350(a,2),6181(a,1,2)),demod(2472(4)),flip(a)].

given #325 (T,wt=14): 6888 x * y @ x ' * y = x * x @ y.  [para(340(a,1),2173(a,1,1)),demod(402(4),277(3),2003(5),7(6),2003(5),2573(7),7(9),2989(8),2505(9))].

given #326 (A,wt=19): 420 x * y * z @ y ' * x ' = z @ y ' * x '.  [back_demod(229),demod(402(4),402(8))].

given #327 (F,wt=14): 6889 x * y @ y * x ' = x * x @ y.  [para(340(a,1),2173(a,1,2)),demod(7(4),2003(3),598(4),2472(9))].

given #328 (F,wt=14): 6890 x * y @ x * y ' = y * y @ x.  [para(2173(a,1),2674(a,1)),flip(a)].

given #329 (T,wt=15): 421 x * y * (y @ x) * z = y * x * z.  [back_demod(222),demod(402(4),67(2),67(2),7(4))].

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

given #331 (A,wt=23): 423 (x ' @ y) * (z ' @ y) * u = (z @ y ') * (x @ y ') * u.  [back_demod(184),demod(402(2),19(5))].

given #332 (F,wt=15): 544 x * y * z @ y * x = z @ y * x.  [para(444(a,1),11(a,1,1)),demod(8(4),7(4)),flip(a)].

given #333 (F,wt=15): 545 x * y * z @ z * y = x @ z * y.  [para(444(a,1),11(a,1,2)),demod(34(4)),flip(a)].

given #334 (T,wt=15): 603 x * y * z @ y ' = x * z @ y '.  [para(83(a,1),11(a,1,1)),demod(114(4),7(5)),flip(a)].

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

given #336 (A,wt=23): 427 x ' * y ' * z ' * x * y * z = y * x @ x ' * z.  [back_demod(89),demod(402(2),402(6),67(6),7(7),7(8))].

given #337 (F,wt=15): 1507 x * y ' * x ' * (y @ x ') = y '.  [para(61(a,1),32(a,1,2)),demod(402(4),402(3),67(2),7(4),7(7),7(6),1215(13),59(10),16(10),34(10))].

given #338 (F,wt=15): 1747 (x ' @ y) * y ' = x * y ' * x '.  [para(59(a,1),66(a,2,2,2,2)),demod(34(8))].

given #339 (T,wt=15): 1961 (x @ y) * (z * x @ y ') = z @ y '.  [para(250(a,1),61(a,2)),demod(402(4),277(3),110(3),7(8),741(7),7(10),797(9))].

given #340 (T,wt=15): 2096 x * y @ x * z * y = x * y @ z.  [back_demod(1251),demod(2081(7))].

given #341 (A,wt=21): 428 x ' * y ' * z * y * x * z ' = y * x @ z '.  [back_demod(79),demod(402(2),7(8))].

given #342 (F,wt=15): 2137 x ' * y ' = (x @ y) * y ' * x '.  [para(10(a,1),72(a,1,2)),demod(402(2),2003(5,R),555(12),34(9)),flip(a)].

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

given #344 (T,wt=15): 2213 x * y * y * x = y * x * x * y.  [para(444(a,1),340(a,1,2,2)),demod(34(4),7(3),7(6))].

given #345 (T,wt=15): 2242 x ' * y ' * x = (y @ x ') * y '.  [para(85(a,2),81(a,2,1))].

given #346 (A,wt=23): 429 x * y ' * z ' * x ' * y * z = y * x ' @ x * z.  [back_demod(73),demod(402(3),67(2),402(4),7(7),7(8))].

given #347 (F,wt=15): 2257 x ' * (y ' @ x) = y * x ' * y '.  [para(547(a,1),81(a,2,1)),demod(402(5),402(4),67(3),7(5),7(6),7(5),62(6),402(9),402(8),67(7),7(9),8(10))].

given #348 (F,wt=15): 2261 (x @ y ') * y * x ' * y ' = x '.  [para(61(a,1),81(a,1,2)),demod(402(4),402(3),67(2),7(4),2003(7,R),130(11),59(9),16(9),8(10))].

given #349 (T,wt=15): 2329 x ' * (y @ z ') = (y ' @ z) * x '.  [para(368(a,1),87(a,1,2,2)),demod(277(2),34(5),1991(6),8(10)),flip(a)].

given #350 (T,wt=15): 2405 (x @ y) * z * u = z * (x @ y) * u.  [para(90(a,1),52(a,1,2,2)),demod(277(3),67(2),2019(6),8(7))].

given #351 (A,wt=20): 432 x ' * y ' * z ' * y * x * z = y * x @ z.  [back_demod(15),demod(402(2),7(8))].

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

given #353 (F,wt=15): 2449 x * (y @ z) * u = x * u * (y @ z).  [para(2003(a,1),7(a,2,2)),demod(7(3))].

given #354 (T,wt=15): 2471 x * (y @ z) * u @ v = x * u @ v.  [para(2081(a,1),11(a,1,2)),demod(11(3)),flip(a)].

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

given #356 (A,wt=25): 490 x * y * z ' * u ' * z * u * v = x * y * (z @ u) * v.  [para(39(a,1),7(a,1)),demod(7(4)),flip(a)].

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

given #358 (F,wt=15): 2528 x * y * z @ u = y * x * z @ u.  [para(2202(a,1),11(a,1,1)),demod(11(4),7(2),7(5))].

given #359 (T,wt=15): 2529 x * y * z @ u = x * z * y @ u.  [para(2202(a,1),11(a,1,2)),demod(11(4))].

given #360 (T,wt=15): 2535 x * y @ z * y * x = y * x @ z.  [para(2202(a,1),144(a,1))].

given #361 (A,wt=16): 492 x * y * (z @ y) = x * z * y * z '.  [para(9(a,1),39(a,1,2,2,2)),demod(402(2),402(4),67(2),67(2),34(4),7(3),402(6),36(8),48(7)),flip(a)].

given #362 (F,wt=15): 2539 x * y @ y * x * z = y * x @ z.  [para(2202(a,1),408(a,1)),demod(7(3))].

given #363 (F,wt=15): 2553 (x @ y) * z * (y @ x) * u = z * u.  [para(2224(a,1),7(a,1,1)),demod(7(5)),flip(a)].

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

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

given #366 (A,wt=21): 494 x * y ' * z * y * u = x * (y @ z ') * z * u.  [para(13(a,1),39(a,1,2,2,2,2)),demod(67(3))].

given #367 (F,wt=15): 2642 (x @ y) * y * x * z = x * y * z.  [para(2604(a,1),7(a,1,1)),demod(7(2),7(5)),flip(a)].

given #368 (F,wt=15): 2672 (x @ y) * z * y * x = z * x * y.  [para(2202(a,1),2604(a,1,1)),demod(19(5),2642(5),7(6))].

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

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

4 x @ y = x ' * y ' * x * y.  [input].
7 (x * y) * z = x * y * z.  [input].
8 e * x = x.  [input].
9 x ' * x = e.  [input].
10 x ' * y ' * x * y = x @ y.  [copy(4),flip(a)].
11 (x @ y) * (z @ y) = x * z @ y.  [input].
12 A * B * C * B * A != B * A * C * A * B # answer(E).  [input].
13 x ' * x * y = y.  [para(9(a,1),7(a,1,1)),demod(8(2)),flip(a)].
14 x ' * y ' * x * y * z = (x @ y) * z.  [para(10(a,1),7(a,1,1)),demod(7(7),7(6)),flip(a)].
15 (x * y) ' * z ' * x * y * z = x * y @ z.  [para(7(a,1),10(a,1,2,2))].
16 e @ x = e.  [para(8(a,1),10(a,1,2,2)),demod(9(4),9(4)),flip(a)].
17 x ' @ x = e.  [para(9(a,1),10(a,1,2,2)),demod(13(6)),flip(a)].
19 (x * y @ z) * u = (x @ z) * (y @ z) * u.  [para(11(a,1),7(a,1,1))].
20 (x @ y) ' * (z @ y) ' * (x * z @ y) = (x @ y) @ (z @ y).  [para(11(a,1),10(a,1,2,2))].
21 (x @ y) * e = x * e @ y.  [para(16(a,1),11(a,1,2))].
22 x ' * y @ x = y @ x.  [para(17(a,1),11(a,1,1)),demod(8(3)),flip(a)].
23 x * y ' @ y = x * e @ y.  [para(17(a,1),11(a,1,2)),demod(21(3)),flip(a)].
24 (x * y) ' * x * y * z = z.  [para(7(a,1),13(a,1,2))].
26 x ' ' * e = x.  [para(9(a,1),13(a,1,2))].
28 x @ x = e.  [para(13(a,1),10(a,1,2)),demod(9(2)),flip(a)].
29 x ' ' * (x @ y) = y ' * x * y.  [para(10(a,1),13(a,1,2))].
30 (x @ y) ' * (x * z @ y) = z @ y.  [para(11(a,1),13(a,1,2))].
31 x ' ' * y = x * y.  [para(13(a,1),13(a,1,2))].
32 x ' * y * x = y * (y @ x).  [back_demod(29),demod(31(4)),flip(a)].
34 x * e = x.  [back_demod(26),demod(31(4))].
36 x * y ' @ y = x @ y.  [back_demod(23),demod(34(5))].
37 x * y @ x = y @ x.  [para(28(a,1),11(a,1,1)),demod(8(3)),flip(a)].
38 x * y @ y = x @ y.  [para(28(a,1),11(a,1,2)),demod(34(3)),flip(a)].
48 (x ' @ y) * x = x * (y @ x).  [para(10(a,1),14(a,1,2)),demod(31(4)),flip(a)].
49 x ' * y ' * x * y * (z @ y) = x * z @ y.  [para(14(a,2),11(a,1))].
54 x ' * y * x * z = (x @ y ') * y * z.  [para(13(a,1),14(a,1,2,2,2)),demod(31(5))].
59 x * x ' = e.  [para(31(a,1),9(a,1))].
67 x ' ' = x.  [para(31(a,1),34(a,1)),demod(34(2)),flip(a)].
69 (x * y ') ' * y ' * x = x @ y.  [para(9(a,1),15(a,1,2,2,2)),demod(34(6),36(9))].
74 (x * y) ' * y * x = y @ x.  [para(13(a,1),15(a,1,2)),demod(37(6))].
77 x ' @ y = y @ x.  [back_demod(69),demod(74(6))].
78 x @ x ' = e.  [para(67(a,1),17(a,1,1))].
83 x * y @ y ' = y @ x.  [para(59(a,1),15(a,1,2,2,2)),demod(67(4),34(4),74(4)),flip(a)].
85 x @ y ' = y @ x.  [para(78(a,1),11(a,1,2)),demod(34(4),83(5))].
110 x ' @ y ' = x @ y.  [para(77(a,2),77(a,1))].
117 (x @ y) * (y @ z ') = x * z @ y.  [para(85(a,2),11(a,1,2))].
130 x * y * z @ y = x * z @ y.  [para(37(a,1),11(a,1,2)),demod(11(3)),flip(a)].
137 x ' @ x * y = y @ x.  [para(37(a,1),77(a,2))].
144 x @ y * x = x @ y.  [para(13(a,1),38(a,1,1)),demod(137(5))].
160 (x ' @ y) ' * (z @ x) ' * (y * z @ x) = (y @ x) @ (z @ x).  [para(77(a,2),20(a,1,1,1))].
169 (x @ y) ' * (z @ y) ' * (y @ (x * z) ') = (x @ y) @ (z @ y).  [para(85(a,2),20(a,1,2,2))].
203 (x @ y) @ x = e.  [para(10(a,1),22(a,1,1)),demod(130(6),9(4),16(4))].
222 (x ' * y ') ' * (x @ y) * z = x * y * z.  [para(14(a,1),24(a,1,2))].
227 (x * y) ' * x = y '.  [para(59(a,1),24(a,1,2,2)),demod(34(4))].
237 (x @ y) @ y = e.  [para(85(a,1),203(a,1,1))].
250 x * (y @ z) @ z = x @ z.  [para(237(a,1),11(a,1,2)),demod(34(3)),flip(a)].
277 (x @ y) ' = x ' @ y.  [para(59(a,1),30(a,1,2,1)),demod(16(4),34(4))].
278 (x @ y) * (y @ x) = e.  [para(78(a,1),30(a,2)),demod(277(3),110(3),83(4))].
292 (x @ y) * (z ' * y * z @ x) = (y @ x) @ (z @ x).  [back_demod(160),demod(277(3),67(2),277(3),11(6))].
305 (x @ y) @ (z @ y) = (x @ z) @ y.  [back_demod(169),demod(277(2),277(4),117(8),11(7),10(5)),flip(a)].
340 x * y * (y @ x) = y * x.  [para(32(a,1),13(a,1,2)),demod(67(2))].
350 x * (y @ x) = y * x * y '.  [para(85(a,1),32(a,2,2)),demod(67(2)),flip(a)].
402 (x * y) ' = y ' * x '.  [para(13(a,1),227(a,1,1,1)),flip(a)].
421 x * y * (y @ x) * z = y * x * z.  [back_demod(222),demod(402(4),67(2),67(2),7(4))].
515 (x @ y ') * (x @ y) = e.  [para(77(a,1),278(a,1,2))].
741 (x @ y) * y = y * (x @ y).  [para(77(a,1),48(a,1,1))].
1241 ((x @ y ') @ z ') * z * (x @ y) = (x @ y) * z.  [para(515(a,1),54(a,1,2,2)),demod(277(3),110(3),34(3)),flip(a)].
1921 x ' * y * x @ z = y @ z.  [para(250(a,1),10(a,2)),demod(402(3),277(2),7(8),741(7),7(10),49(9),11(5))].
1985 (x @ y) @ (z @ y) = e.  [back_demod(292),demod(1921(5),278(3)),flip(a)].
1991 (x @ y) @ z = e.  [back_demod(305),demod(1985(3)),flip(a)].
2003 (x @ y) * z = z * (x @ y).  [back_demod(1241),demod(1991(4),8(4)),flip(a)].
2197 x * (y @ z) @ u = x @ u.  [para(1991(a,1),11(a,1,2)),demod(34(3)),flip(a)].
2202 x * y @ z = y * x @ z.  [para(340(a,1),11(a,2,1)),demod(2197(4),11(3))].
2604 (x @ y) * y * x = x * y.  [para(144(a,1),350(a,1,2)),demod(2003(3,R),7(6),59(5),34(5))].
2642 (x @ y) * y * x * z = x * y * z.  [para(2604(a,1),7(a,1,1)),demod(7(2),7(5)),flip(a)].
2672 (x @ y) * z * y * x = z * x * y.  [para(2202(a,1),2604(a,1,1)),demod(19(5),2642(5),7(6))].
10653 $F # answer(E).  [para(2672(a,2),12(a,1,2,2)),demod(421(13)),xx(a)].

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

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

Given=368. Generated=169112. Kept=10646. proofs=1.
Usable=289. Sos=6435. Demods=1903. Denials=0. 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=2978376. 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.79.
User_CPU=4.76, System_CPU=0.08, Wall_clock=5.

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

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

THEOREM PROVED

Exiting with 1 proof.

Process 13119 exit (max_proofs) Mon Jun 19 16:41:34 2006