% Length of proof is 327.

% Level of proof is 54.

% Maximum clause weight is 54.

% Given clauses 7320.

1 ((A * B) * A) * C = A * (B * (A * C)) # label(non_clause) # label(goal).[goal].

2 0 * x = x. [assumption].

3 x * 0 = x. [assumption].

4 x' * x = 0. [assumption].

5 x * x' = 0. [assumption].

6 (x * y) * (z * x) = x * ((y * z) * x). [assumption].

9 s(A) * s(A) = A. [assumption].

11 s(C) * s(C) = C. [assumption].

13 ((A * B) * A) * C != A * (B * (A * C)). [deny(1)].

15 (x * y) * x = x * (y * x). [para(2(a,1),6(a,1,2)),rewrite([3(4)])].

16 x' * ((x * y) * x') = y * x'. [para(4(a,1),6(a,1,1)),rewrite([2(4)]),flip(a)].

17 x * ((y * x') * x) = x * y. [para(4(a,1),6(a,1,2)),rewrite([3(3)]),flip(a)].

18 x * ((x' * y) * x) = y * x. [para(5(a,1),6(a,1,1)),rewrite([2(3)]),flip(a)].

19 x' * ((y * x) * x') = x' * y. [para(5(a,1),6(a,1,2)),rewrite([3(4)]),flip(a)].

21 ((x * y) * z) * (y * ((u * x) * y)) = (x * y) * ((z * (y * u)) * (x *y)). [para(6(a,1),6(a,1,2))].

22 (A * (B * A)) * C != A * (B * (A * C)). [back_rewrite(13),rewrite([15(5)])].

27 (x * (y * x)) * (z * (x * y)) = (x * y) * ((x * z) * (x * y)). [para(15(a,1),6(a,1,1))].

28 (x * y) * (x * (z * x)) = x * ((y * (x * z)) * x). [para(15(a,1),6(a,1,2))].

30 s(A) * A = A * s(A). [para(9(a,1),15(a,1,1)),rewrite([9(11)]),flip(a)].

31 s(C) * C = C * s(C). [para(11(a,1),15(a,1,1)),rewrite([11(11)]),flip(a)].

32 (x * (y * x)) * (x * y) = (x * y) * (x * (x * y)). [para(15(a,1),15(a,1,1))].

36 x * x'' = x * x. [para(4(a,1),17(a,1,2,1)),rewrite([2(2)]),flip(a)].

37 x * ((((y * x') * x) * z) * x) = x * ((y * z) * x). [para(17(a,1),6(a,1,1)),rewrite([6(3)]),flip(a)].

41 (x * y') * y = y * (y' * x). [para(15(a,1),17(a,1,2,1)),rewrite([18(6)])].

46 x * (((x * (x' * y)) * z) * x) = x * ((y * z) * x). [back_rewrite(37),rewrite([41(3)])].

47 x * (x * (x' * y)) = x * y. [back_rewrite(17),rewrite([41(3)])].

51 x'' * x = x * x. [para(5(a,1),18(a,1,2,1)),rewrite([2(2)]),flip(a)].

52 x * ((((x' * y) * x) * z) * x) = (y * x) * (z * x). [para(18(a,1),6(a,1,1)),flip(a)].

55 x''' * x = 0. [para(36(a,1),18(a,1,2,1)),rewrite([41(4),47(5),5(2)]),flip(a)].

56 x'' * x'' = x * x. [para(36(a,1),18(a,2)),rewrite([55(6),2(6)])].

67 (x * (x' * y)) * (x * y) = (y * x) * (x * (x' * y)). [para(47(a,1),15(a,2,2)),rewrite([15(4),18(4)]),flip(a)].

68 x * x''' = 0. [para(36(a,1),47(a,1,2,2)),rewrite([47(5),5(2)]),flip(a)].

69 (x' * (x'' * y)) * x = y * x. [para(47(a,1),18(a,1,2,1)),rewrite([18(4)]),flip(a)].

74 x * x'''' = x * x. [para(68(a,1),47(a,1,2,2)),rewrite([3(2)]),flip(a)].

78 x''''' * x = 0. [para(74(a,1),18(a,1,2,1)),rewrite([41(4),47(5),5(2)]),flip(a)].

79 x * x''''' = 0. [para(74(a,1),47(a,1,2,2)),rewrite([47(5),5(2)]),flip(a)].

81 x * ((y * x''''') * x) = x * y. [para(78(a,1),6(a,1,2)),rewrite([3(3)]),flip(a)].

82 x * ((x''''' * y) * x) = y * x. [para(79(a,1),6(a,1,1)),rewrite([2(3)]),flip(a)].

87 (x * y) * (x * (x' * z)) = x * ((y * (z * x')) * x). [para(41(a,1),6(a,1,2))].

88 (x * y) * ((x * y)' * y) = y * (((x * y)' * x) * y). [para(41(a,1),6(a,1))].

90 (x' * (y * x')) * x = x * (x' * (x' * y)). [para(15(a,1),41(a,1,1))].

91 (x * x) * x' = x' * (x * x). [para(36(a,1),41(a,1,1)),rewrite([51(7)])].

93 x * (x' * (y * x'')) = y * x. [para(41(a,1),41(a,1,1)),rewrite([69(6)]),flip(a)].

108 x * (x' * (x * y)) = x * y. [para(16(a,1),18(a,1,2,1)),rewrite([41(3),47(4),41(5)]),flip(a)].

109 ((x' * y) * x) * x' = x' * y. [para(18(a,1),16(a,1,2,1)),rewrite([19(5)]),flip(a)].

110 x * ((x * y) * x') = x * (x * (y * x')). [para(16(a,1),47(a,1,2,2)),flip(a)].

111 (x * (x' * y)) * x' = y * x'. [para(47(a,1),16(a,1,2,1)),rewrite([16(5)]),flip(a)].

113 (x * x)' * x' = x' * (x * x)'. [para(91(a,1),16(a,1,2,1)),rewrite([19(9)])].

114 ((x * y) * x') * x'' = x'' * y. [para(16(a,1),16(a,1,2,1)),rewrite([19(8)]),flip(a)].

116 x * (((x' * (x * y)) * z) * x) = x * ((y * z) * x). [para(108(a,1),6(a,1,1)),rewrite([6(3)]),flip(a)].

121 (x * y) * ((x * y)' * (x * (y * x))) = x * (y * x). [para(15(a,1),108(a,1,2,2)),rewrite([15(9)])].

124 x * (x' * (y * x)) = y * x. [para(18(a,1),108(a,1,2,2)),rewrite([18(8)])].

143 (x * y) * y' = y' * (y * x). [para(15(a,1),19(a,1,2,1)),rewrite([16(6)])].

145 (x' * (x * y)) * x = y * x. [para(19(a,1),18(a,1,2,1)),rewrite([18(4),143(4)]),flip(a)].

146 x' * (x' * (x * y)) = x' * y. [para(19(a,1),18(a,2)),rewrite([143(3),143(6),143(12),18(14)])].

149 (x' * (x * y)) * x'' = y * x''. [para(19(a,1),16(a,1,2,1)),rewrite([16(8),143(6)]),flip(a)].

157 x'' * (x' * (x * y)) = x'' * y. [back_rewrite(114),rewrite([143(6)])].

158 x' * (x * (x' * y)) = x' * y. [back_rewrite(109),rewrite([143(5)])].

166 ((x' * y) * x) * x = (x' * (y * x)) * x. [para(18(a,1),145(a,1,1,2)),flip(a)].

176 (x' * y) * (x' * (x * z)) = x' * ((y * (z * x)) * x'). [para(143(a,1),6(a,1,2))].

179 (x * (y * x)) * x' = x' * (x * (x * y)). [para(15(a,1),143(a,1,1))].

184 x' * (x * (y * x')) = y * x'. [para(41(a,1),143(a,1,1)),rewrite([111(5)]),flip(a)].

189 x' * (x'' * y) = x' * (x * y). [para(143(a,1),124(a,1,2,2)),rewrite([157(7),143(8)])].

192 x'' * (x' * (y * x)) = y * x''. [para(143(a,1),143(a,1,1)),rewrite([149(6)]),flip(a)].

198 (x'' * y) * x = x * (y * x''). [para(15(a,1),93(a,1,2,2)),rewrite([189(8),108(7)]),flip(a)].

200 x * (y * x'') = x * (y * x). [para(93(a,1),47(a,1,2)),flip(a)].

202 (x * y''') * y = y * (y' * x). [para(41(a,1),93(a,1,2,2)),rewrite([189(8),108(7)]),flip(a)].

208 (x'' * y) * x = x * (y * x). [back_rewrite(198),rewrite([200(8)])].

234 x' * ((x' * y) * x) = x' * (x' * (y * x)). [para(18(a,1),146(a,1,2,2)),flip(a)].

238 x'' * (x'' * (y * x')) = x'' * ((x * y) * x'). [para(16(a,1),146(a,1,2,2))].

243 x' * (y * x'') = x' * (y * x). [para(200(a,1),146(a,1,2,2)),rewrite([146(6)]),flip(a)].

255 x'' * ((x * y) * x') = x'' * (x * (y * x')). [para(184(a,1),146(a,1,2,2)),rewrite([238(8)])].

256 x'' * (x'' * (y * x')) = x'' * (x * (y * x')). [back_rewrite(238),rewrite([255(14)])].

262 (x' * (x * x)') * (x * x)' = (x * x)' * (x' * (x * x)'). [para(113(a,1),15(a,1,1))].

273 x * (x'' * y) = x * (x * y). [para(189(a,1),47(a,1,2,2)),rewrite([108(4)]),flip(a)].

280 (x'' * y) * x' = (x * y) * x'. [para(189(a,1),111(a,1,1,2)),rewrite([108(4)]),flip(a)].

288 (x''' * y) * x = (x' * y) * x. [para(273(a,1),18(a,1,2,1)),rewrite([18(6)]),flip(a)].

311 (x * y'') * y'' = (x * y) * y''. [para(243(a,1),16(a,1,2,1)),rewrite([16(9)]),flip(a)].

334 x * (x' * (x' * (y * x))) = (x' * y) * x. [para(288(a,1),124(a,1,2,2)),rewrite([234(5),288(11)])].

386 (x * x)' * x = x * (x * x)'. [para(113(a,1),81(a,1,2,1)),rewrite([56(14),56(10),82(10),56(12),56(8)])].

399 (x * (x * x)') * (y * (x * x)') = (x * x)' * ((x * y) * (x * x)'). [para(386(a,1),6(a,1,1))].

400 (x * y) * (x * (x * x)') = x * ((y * (x * x)') * x). [para(386(a,1),6(a,1,2))].

403 (x * (x * x)') * (x * x)' = (x * x)' * (x * (x * x)'). [para(386(a,1),15(a,1,1))].

407 (x * x)'' * (x * (x * (x * (x * x)'))) = x * (x * x)''. [para(386(a,1),16(a,1,2,1)),rewrite([143(10),386(9),256(11),400(8),15(7),386(6)])].

409 (x * (x * x)') * x' = x' * (x * (x * x)'). [para(386(a,1),143(a,1,1))].

410 (x * x)'' * x = x * (x * x)''. [para(386(a,1),146(a,1,2,2)),rewrite([256(11),400(8),15(7),386(6),407(9)]),flip(a)].

448 x'' * (y * x'') = (x * y) * x''. [para(149(a,1),6(a,2,2)),rewrite([4(4),2(6)]),flip(a)].

501 x'' * (y * x) = (x * y) * x''. [para(200(a,1),157(a,1,2,2)),rewrite([157(7),448(10)])].

504 x'' * (x'' * y) = x'' * (x * y). [para(157(a,1),146(a,1,2))].

584 (x * y)'' * ((x * y)' * (y * ((z * x) * y))) = (y * z) * (x * y)''. [para(6(a,1),192(a,1,2,2))].

786 x * ((y * (x * (x' * z))) * x) = x * ((y * z) * x). [para(18(a,1),28(a,1,2)),rewrite([6(3)]),flip(a)].

791 x * ((y * (x * (z * x'))) * x) = (x * y) * (x * z). [para(41(a,1),28(a,1,2,2)),rewrite([47(5)]),flip(a)].

793 x' * ((y * (x' * (x * z))) * x') = x' * ((y * z) * x'). [para(16(a,1),28(a,1,2)),rewrite([6(5)]),flip(a)].

813 (x * (x * x)') * ((x * x)' * (y * (x * x)')) = (x * x)' * ((x * ((x *x)' *y)) * (x * x)'). [para(386(a,1),28(a,1,1))].

814 (x * y) * (x * (x * (x * x)')) = x * ((y * (x * (x * x)')) * x). [para(386(a,1),28(a,1,2,2))].

898 (x' * (x' * (y * x'))) * x = x * (x' * (x' * (x' * y))). [para(15(a,1),90(a,1,1,2))].

960 (x' * (x * (x * x)')) * (y * (x * (x * x)')) = (x * (x * x)') * ((x' *y) *(x * (x * x)')). [para(409(a,1),6(a,1,1))].

965 (x * (x * x)')' * ((x * (x * x)')' * (x' * (x * (x * x)'))) = x' * (x* (x * x)')'. [para(409(a,1),16(a,1,2,1)),rewrite([143(14),409(13)])].

967 (x * (x * x)')' * x' = x' * (x * (x * x)')'. [para(409(a,1),146(a,1,2,2)),rewrite([965(15)]),flip(a)].

971 (x * (x * x)') * ((x * (x * x)') * (x' * (x * (x * x)')')) = x' * (x *(x *x)'). [para(409(a,1),110(a,1,2,1)),rewrite([143(13),409(12),124(14)]),flip(a)].

1030 (x * x)' * ((((x * x)' * (x * (x * x))) * y) * (x * x)') = (x * x)' *((x * y) * (x * x)'). [para(410(a,1),46(a,1,2,1,1,2)),rewrite([243(9)])].

1154 x * ((y * (z * x')) * x) = x * (x' * ((x * y) * z)). [para(6(a,1),116(a,1,2,1)),rewrite([90(7),47(8)]),flip(a)].

1224 (x * y) * (x * (x' * z)) = x * (x' * ((x * y) * z)). [back_rewrite(87),rewrite([1154(10)])].

1333 x' * ((y * (z * x)) * x') = x' * (x * ((x' * y) * z)). [para(448(a,1),786(a,1,2,1,2,2)),rewrite([243(7),15(4),793(9),1154(14),189(14)])].

1354 (x' * y) * (x' * (x * z)) = x' * (x * ((x' * y) * z)). [back_rewrite(176),rewrite([1333(12)])].

1360 s(A) * (s(A) * (s(A) * x)) = A * (s(A) * x). [para(9(a,1),791(a,2,1)),rewrite([15(15),15(14),41(13),47(14)])].

1361 s(C) * (s(C) * (s(C) * x)) = C * (s(C) * x). [para(11(a,1),791(a,2,1)),rewrite([15(15),15(14),41(13),47(14)])].

1364 (x * x) * (x * y) = x * (x * (x * y)). [para(15(a,1),791(a,1,2)),rewrite([15(4),41(3),47(4)]),flip(a)].

1450 (x * x)' * ((x * (x * (x * y))) * (x * x)') = (x * y) * (x * x)'. [para(1364(a,1),16(a,1,2,1))].

1495 x * (((x * x) * y) * x) = x * (x * (x * (y * x))). [para(1364(a,1),786(a,1,2,1)),rewrite([47(4),15(3),15(2)]),flip(a)].

1496 (x * (x * x)) * (x * y) = x * (x * (x * (x * y))). [para(1364(a,1),791(a,1,2,1)),rewrite([15(6),15(5),15(4),41(3),47(4)]),flip(a)].

1541 x * (x' * ((x' * x') * y)) = x * (x' * (x' * (x' * y))). [para(1495(a,1),18(a,1,2,1)),rewrite([18(10),898(7),41(14)]),flip(a)].

1544 x * (((x' * x') * y) * x') = x * (x' * (x' * (y * x'))). [para(1495(a,1),47(a,1,2,2)),rewrite([47(10)]),flip(a)].

1577 (x' * (x' * (x' * (y * x')))) * x = x * (x' * (x' * (x' * (x' *y)))). [para(1495(a,1),334(a,2,1)),rewrite([41(9),1541(9),158(10)]),flip(a)].

1585 x * (x' * (x' * ((x' * x') * y))) = x * (x' * (x' * (x' * (x' *y)))). [para(1495(a,1),90(a,1,1)),rewrite([1577(9)]),flip(a)].

1718 x * (((x * x)' * (x' * (x * x)')) * x) = x * (x' * ((x * x)' * (x *(x * x)'))). [para(386(a,1),67(a,2,1)),rewrite([400(9),262(7),1224(18),403(16)])].

1787 x * (((x * (x * x)')' * (x * x)') * x) = x * (((x * x)' * (x * (x *x)')')* x). [para(386(a,1),88(a,1,1)),rewrite([386(6),6(9),386(12)]),flip(a)].

1874 ((x * (x * x)') * y) * (x * ((z * (x * x)') * x)) = (x * (x * x)') *((y *(x * z)) * (x * (x * x)')). [para(400(a,1),6(a,1,2))].

1916 x * (((x * x)' * (x * x)') * x) = (x * x)'. [para(400(a,1),52(a,2)),rewrite([410(6),41(9),410(8),243(9),1030(12),5(6),3(4)]),flip(a)].

1925 x * (((x * x)' * (x * ((x * x)' * (x * ((x * x)' * (x * (y * (x *x)'))))))) * x) = (x * x)' * ((x * ((x * x)' * (x * (y * x)))) * (x * x)'). [para(400(a,1),1495(a,2,2,2,2)),rewrite([400(10),1916(10),6(11),15(7),813(12),28(27),28(28),

28(29)]),flip(a)].

1944 x' * (x * ((x * x)' * (x * x)')) = x' * (x' * (x * x)'). [para(1916(a,1),16(a,1,2,1)),rewrite([113(5),143(14)]),flip(a)].

1945 x * (x' * (x * x)') = (x * x)'. [para(1916(a,1),108(a,1,2,2)),rewrite([1916(12)])].

1951 x' * (((x * x)' * (x * x)') * x) = x' * (x' * (x * x)'). [para(1916(a,1),146(a,1,2,2)),flip(a)].

1975 x * ((y * (x' * (x * x)')) * x) = (x * y) * (x * x)'. [para(1916(a,1),791(a,2,2)),rewrite([143(8),1944(8),786(10)])].

1976 x * (x * (x * x)') = 0. [para(1916(a,1),1364(a,1,2)),rewrite([5(4),1916(8)]),flip(a)].

1979 (x * x)' * (x * (x * x)) = x. [para(1916(a,1),1496(a,1,2)),rewrite([143(5),15(4),1916(12),1976(9),3(7)])].

1984 (((x * x)' * (x * x)') * x) * (x * (((x * x)'' * ((x * x)' * (x *x)')) * x)) = (x * x)' * (x * (x * x)'). [para(1916(a,1),88(a,1,1)),rewrite([1916(9),189(13),6(10),15(9),1916(9),1916(19),410(16),6(23)]),flip(a)].

1986 (x * x)'' = x * x. [para(400(a,1),1916(a,1,2,1,1,1)),rewrite([1916(10),400(13),1916(13),56(10),1364(6),400(10),143(8),15(7),1979(8),28(6),4(4),2(2),400(8),1916(8)]),flip(a)].

1994 x * (x' * ((x * x)' * (x * (x * x)'))) = (x * x)' * (x * (x * x)'). [back_rewrite(1718),rewrite([1975(9),403(6)]),flip(a)].

1999 x * ((y * (x * (x * x)')) * x) = x * y. [back_rewrite(814),rewrite([1976(5),3(3)]),flip(a)].

2000 ((x * x)' * (x * x)') * x = (x * x)' * (x * (x * x)'). [back_rewrite(1984),rewrite([1986(9),1495(15),1916(13),1976(10),3(8)])].

2015 x' * ((x * x)' * (x * (x * x)')) = x' * (x' * (x * x)'). [back_rewrite(1951),rewrite([2000(7)])].

2022 x * ((x * x)' * (x * (x * x)')) = (x * x)'. [back_rewrite(1916),rewrite([2000(6)])].

2023 x * (x' * (x' * (x * x)')) = (x * x)' * (x * (x * x)'). [back_rewrite(1994),rewrite([2015(8)])].

2026 (x * (x * (x * x)))'' = x * (x * (x * x)). [para(6(a,1),1986(a,1,1,1)),rewrite([15(2),1364(8)])].

2027 A'' = A. [para(9(a,1),1986(a,1,1,1)),rewrite([9(8)])].

2032 x * (((x * (x * x)') * y) * x) = y * x. [para(1976(a,1),6(a,1,1)),rewrite([2(3)]),flip(a)].

2033 (x * (x * x)') * ((y * x) * (x * (x * x)')) = (x * (x * x)') * y. [para(1976(a,1),6(a,1,2)),rewrite([3(6)]),flip(a)].

2037 x'' * (x * (x * x)') = 0. [para(56(a,1),1976(a,1,2,2,1)),rewrite([504(8)])].

2038 x' * (x * (x * x)') = x' * x'. [para(1976(a,1),16(a,1,2,1)),rewrite([2(4),409(8)]),flip(a)].

2058 (x * (x * x)') * ((x * (x * x)') * (x' * (x * (x * x)')')) = x' * x'. [back_rewrite(971),rewrite([2038(19)])].

2063 (x * (x * x)') * ((x' * y) * (x * (x * x)')) = (x' * x') * (y * (x *(x * x)')). [back_rewrite(960),rewrite([2038(5)]),flip(a)].

2080 x * (x' * x') = x * (x * x)'. [para(1979(a,1),121(a,1,1)),rewrite([1979(5),143(8),15(7),1979(8),386(4),2038(5),143(11),15(10),1979(11),386(7)])].

2081 (x * x)' * ((y * ((x * x)' * (x * (x * (x * (x * x)))))) * (x * x)')= ((x* x)' * y) * x. [para(1979(a,1),791(a,2,2)),rewrite([1986(9),6(8),15(6),15(7),15(6)])].

2098 ((x * (x * x)')' * x'') * (x * (x * x)') = x. [para(2037(a,1),334(a,1,2,2,2)),rewrite([3(13),2080(13),400(10),2000(9),2022(10),1986(6),6(5),386(3),15(4),386(3),1976(4),3(2)]),flip(a)].

2100 (x * (x * x)')' * (x * (x * x)')' = (x * (x * x)')' * x. [para(2037(a,1),234(a,2,2,2)),rewrite([2098(15),3(15)]),flip(a)].

2101 x' * (((x * (x * x)') * y) * x') = x' * (x' * (y * x')). [para(2037(a,1),46(a,1,2,1,1,2)),rewrite([3(4),15(5)]),flip(a)].

2141 ((x' * x') * (x * (x * x)')) * (x * (x * x)') = x' * (x' * (x' *x')). [para(2080(a,1),32(a,1,1,2)),rewrite([41(11),2080(11),41(15),2080(15),41(21),2080(21),2063(22),2038(19),1364(18)])].

2147 x * ((y * (x * x)') * x) = x * (y * x'). [para(2080(a,1),791(a,2,2)),rewrite([15(5),786(9),1154(6),16(5),400(8)]),flip(a)].

2152 x * (((x * x)' * (x * (x * x)')') * x) = x. [para(400(a,1),2080(a,2,2,1)),rewrite([2100(12),6(9),2000(18),2022(19),1986(15),6(14),386(12),15(13),386(12),1976(13),3(11)])].

2174 (x * (x * x)') * ((y * (x * z)) * (x * (x * x)')) = ((x * (x * x)') *y) *(x * (z * x')). [back_rewrite(1874),rewrite([2147(9)]),flip(a)].

2175 x * (x' * (x * (x * x)')') = x. [back_rewrite(1787),rewrite([2147(9),967(6),2152(16)])].

2177 (x * y) * (x * (x * x)') = x * (y * x'). [back_rewrite(400),rewrite([2147(10)])].

2194 x' * (x * (x * x)')' = 0. [para(2175(a,1),111(a,1,1)),rewrite([5(2),967(7)]),flip(a)].

2208 x' * x' = (x * x)'. [back_rewrite(2058),rewrite([2194(12),3(8),2177(7),113(4),1945(5)]),flip(a)].

2215 x' * (x' * (x * x)') = (x * (x * (x * x)))'. [back_rewrite(2141),rewrite([2208(3),6(10),15(6),386(5),1976(6),2(6),2208(5),1364(3),2208(9)]),flip(a)].

2228 (x * x)' * (x * (x * x)') = (x * (x * (x * x)))' * x. [back_rewrite(2000),rewrite([2208(5),1364(3)]),flip(a)].

2248 x * (x' * (x' * (x' * (x' * y)))) = x * (x' * (x' * ((x * x)' * y))). [back_rewrite(1585),rewrite([2208(5)]),flip(a)].

2249 x * (x' * (x' * (y * x'))) = x * (((x * x)' * y) * x'). [back_rewrite(1544),rewrite([2208(3)]),flip(a)].

2250 x * (x' * (x' * (x' * y))) = x * (x' * ((x * x)' * y)). [back_rewrite(1541),rewrite([2208(4)]),flip(a)].

2256 (x * (x * (x * x)))' * x = x * (x * (x * (x * x)))'. [back_rewrite(2023),rewrite([2215(6),2228(11)]),flip(a)].

2265 x * (x * (x * (x * (x * x)))') = (x * x)'. [back_rewrite(2022),rewrite([2228(6),2256(5)])].

2278 (x' * (x' * (x' * (y * x')))) * x = x * (x' * ((x * x)' * (x' * y))). [back_rewrite(1577),rewrite([2250(18)])].

2280 x * (x' * ((x * x)' * (x' * y))) = x * (x' * (x' * ((x * x)' * y))). [back_rewrite(2248),rewrite([2250(9)])].

2282 (x' * (x' * (y * x'))) * x = x * (x' * ((x * x)' * y)). [back_rewrite(898),rewrite([2250(14)])].

2286 (x * x)' * (x * (x * x)') = x * (x * (x * (x * x)))'. [back_rewrite(2228),rewrite([2256(11)])].

2291 (x' * (x' * (x' * (y * x')))) * x = x * (x' * (x' * ((x * x)' * y))). [back_rewrite(2278),rewrite([2280(17)])].

2292 x' * (x' * (y * x')) = (x * x)' * (y * x'). [para(2208(a,1),6(a,1,1)),rewrite([15(10)]),flip(a)].

2294 (x * x)' * (x' * (y * x')) = x' * ((x * x)' * (y * x')). [para(2208(a,1),28(a,1,1)),rewrite([15(14),15(13),2292(14)])].

2295 x' * (x' * (x' * y)) = (x * x)' * (x' * y). [para(2208(a,1),791(a,2,1)),rewrite([243(7),15(8),15(7),143(6),146(7)])].

2298 (x * x)' * (x' * (x * x)') = x' * (x * (x * (x * x)))'. [para(2208(a,1),1496(a,1,2)),rewrite([2208(4),262(7),2208(13),2215(14)])].

2300 (x * x) * (x' * (x * x)') = x'. [para(2208(a,1),1979(a,1,1,1)),rewrite([1986(3),2208(5)])].

2301 (x' * ((x * x)' * (y * x'))) * x = x * (x' * (x' * ((x * x)' * y))). [back_rewrite(2291),rewrite([2292(7)])].

2302 ((x * x)' * (y * x')) * x = x * (x' * ((x * x)' * y)). [back_rewrite(2282),rewrite([2292(6)])].

2304 x * (((x * x)' * y) * x') = x * ((x * x)' * (y * x')). [back_rewrite(2249),rewrite([2292(6)]),flip(a)].

2307 x' * (((x * (x * x)') * y) * x') = (x * x)' * (y * x'). [back_rewrite(2101),rewrite([2292(14)])].

2312 (x' * (x * x)') * (x * x)' = x' * (x * (x * (x * x)))'. [back_rewrite(262),rewrite([2298(14)])].

2356 (x * x) * ((y * ((x * x) * (x' * (x * (x * (x * x)))'))) * (x * x)) =((x * x) * y) * x'. [para(2300(a,1),791(a,2,2)),rewrite([2312(9)])].

2373 (x * (y * (y * y)')) * y = y * ((y * (y * y)') * x). [para(15(a,1),1999(a,1,2,1)),rewrite([2032(10)])].

2478 x * ((x * (x * x)') * (((x * (x * x)') * ((x * (x * x)')' * y)) * z))= x * ((x * (x * x)') * (y * z)). [para(46(a,1),2032(a,1,2,1)),rewrite([2032(11),2373(6),2373(21)]),flip(a)].

2511 x * (((x * x)' * (y * (x * x)')) * x) = x * ((x * x)' * (y * x')). [para(15(a,1),2147(a,1,2,1)),rewrite([2304(14)])].

2512 x * (x' * (y * (x * x))) = (y * x) * x. [para(2147(a,1),18(a,1,2,1)),rewrite([243(5),18(5),2208(5),1986(5),41(7)]),flip(a)].

2517 ((x * (y * y)') * y) * y = y * (y' * x). [para(2147(a,1),145(a,1,1,2)),rewrite([184(5),41(3)]),flip(a)].

2522 x' * ((y * (x * x)') * x) = x' * (y * x'). [para(2147(a,1),146(a,1,2,2)),rewrite([184(6)]),flip(a)].

2544 (x * y) * (y * (y * y)') = y * (y' * x). [para(2147(a,1),52(a,1)),rewrite([143(5),158(5),386(7)]),flip(a)].

2570 x * (x' * ((x * (x * x)') * y)) = (x * (x * x)') * y. [back_rewrite(2033),rewrite([2544(8),1224(7)])].

2580 x * ((y * x) * x) = x * (y * (x * x)). [para(2512(a,1),47(a,1,2))].

2590 (x * (y * y)) * y' = y' * (y * (x * y)). [para(2512(a,1),111(a,1,1)),rewrite([143(4)]),flip(a)].

2736 x * (x' * (y * x')) = (y * (x * x)') * x. [para(2580(a,1),18(a,1,2,1)),rewrite([2208(4),18(7),41(9)]),flip(a)].

2751 x' * ((y * x) * (x * x)') = x' * (y * x'). [para(143(a,1),2580(a,1,2,1)),rewrite([15(6),16(6),2208(9)]),flip(a)].

2774 x * ((x' * y) * (x * x)) = (y * x) * x. [para(166(a,1),2580(a,1,2)),rewrite([18(5)]),flip(a)].

2784 (x' * (y * (x * x)')) * x = x * ((x * x)' * (y * x')). [para(2580(a,1),334(a,2,1)),rewrite([41(7),2736(7),2522(7),2292(6),2208(10)]),flip(a)].

2827 x * ((x * (x * x)') * (y * (x * (x * x)'))) = x * ((x * x)' * ((x *y) * x')). [para(2580(a,1),2032(a,1,2,1)),rewrite([2177(10),113(7),1945(8),399(7),2511(9),2373(16)]),flip(a)].

2869 x * ((x * x)' * ((x * y) * x')) = (y * (x * x)') * x. [para(2774(a,1),288(a,1,1)),rewrite([311(8),202(7),2736(5),2208(17),2208(15),2208(13),1986(13),2784(15),288(13),280(11)]),flip(a)].

2911 x * ((x * (x * x)') * (y * (x * (x * x)'))) = (y * (x * x)') * x. [back_rewrite(2827),rewrite([2869(16)])].

2931 x * ((y * ((z * (x * x)') * x)) * x) = x * (x' * ((x * y) * z)). [para(2517(a,1),6(a,1,2)),rewrite([1224(5)]),flip(a)].

2949 (x * y) * (y * (y' * z)) = y * (y' * ((x * y) * z)). [para(2517(a,1),52(a,2,2)),rewrite([2931(10),18(5)]),flip(a)].

2953 x * ((((y * (x * (x' * ((x * (x' * z)) * z)))') * (x * (x' * z))) *z) * x) = x * ((z * ((x * (x' * z))' * y)) * x). [para(2517(a,1),786(a,1,2,1)),rewrite([46(11),1224(15)]),flip(a)].

2963 x * (x * ((x * x)' * y)) = x * (x' * y). [para(2517(a,1),2032(a,2)),rewrite([6(8),2511(8),15(7),2302(6),47(7)])].

3026 (x * (x * x)') * y = x * ((x * x)' * y). [para(2544(a,1),15(a,2,2)),rewrite([6(5),2177(9),143(6),108(7),1224(11),2570(11)]),flip(a)].

3079 x * (x' * (y * (x * (x * x)'))) = y * (x * (x * x)'). [para(2544(a,1),52(a,1,2)),rewrite([1224(16),18(14),1976(15),3(13)])].

3102 (x * (y * y)') * ((y * y)' * (y * (y * (y * y)))) = (y * y)' * ((y *y) * x). [para(1986(a,1),2544(a,2,2,1)),rewrite([2208(10),1364(8),2026(10)])].

3107 x * ((x * x)' * (x * y)) = x * (x' * y). [para(2544(a,1),2032(a,2)),rewrite([2177(13),113(10),1945(11),1986(9),6(8),386(6),15(7),386(6),1976(7),3(5),2177(9),143(6),108(7),3026(5)])].

3114 x * ((x * x)' * ((y * x) * (x * x)')) = x * ((x * x)' * (y * x')). [para(2544(a,1),2580(a,1,2,1)),rewrite([2177(10),15(7),2736(8),6(8),2511(8),2177(17),113(14),1945(15),3026(14)]),flip(a)].

3123 (x * (y * y)') * y = x * (y * (y * y)'). [back_rewrite(2911),rewrite([3026(8),2963(9),3079(7)]),flip(a)].

3136 x * (x' * ((x * ((x * x)' * ((x * (x * x)')' * y))) * z)) = x * (x' *(y *z)). [back_rewrite(2478),rewrite([3026(12),3026(14),2963(15),3026(18),2963(19)])].

3162 (x * (y * (y * y)')) * y = y * (y' * x). [back_rewrite(2373),rewrite([3026(9),2963(10)])].

3165 ((x * x)' * y) * x' = (x * x)' * (y * x'). [back_rewrite(2307),rewrite([3026(5),16(8)])].

3171 x * ((x * x)' * ((y * (x * z)) * (x * (x * x)'))) = (x * ((x * x)' *y)) *(x * (z * x')). [back_rewrite(2174),rewrite([3026(10),3026(14)])].

3180 x * (x * (((x * x)' * y) * x)) = y * x. [back_rewrite(2032),rewrite([3026(4),15(5)])].

3188 (x * x)' * ((x * y) * (x * x)') = x * ((x * x)' * (y * (x * x)')). [back_rewrite(399),rewrite([3026(7)]),flip(a)].

3193 x * (((x * x)' * (x' * (y * (x * x)'))) * x) = (x * x)' * ((y * x) *(x * x)'). [back_rewrite(1925),rewrite([3107(12),3107(12),786(13),3107(18),124(16)])].

3227 x * (x' * (y * x')) = y * (x * (x * x)'). [back_rewrite(2736),rewrite([3123(9)])].

3251 (x * y) * (x * x)' = x * (y * (x * x)'). [back_rewrite(1450),rewrite([3188(9),3188(8),3188(7),2963(8),47(7)]),flip(a)].

3257 (x * x)' * (x * (y * (x * x)')) = x * ((x * x)' * (y * (x * x)')). [back_rewrite(3188),rewrite([3251(6)])].

3270 ((x * x)' * ((x * x) * y)) * x = y * x. [para(47(a,1),3180(a,1,2,2,1)),rewrite([3180(6),1986(6)]),flip(a)].

3280 ((x * x) * y) * x = x * (x * (y * x)). [para(189(a,1),3180(a,1,2,2,1)),rewrite([3270(6),1986(6)]),flip(a)].

3286 x * (x' * (x' * y)) = x * ((x * x)' * y). [para(90(a,1),3180(a,2)),rewrite([2294(7),2301(8),47(9),47(7)]),flip(a)].

3410 x * ((x * x)' * (y * x)) = (x' * y) * x. [back_rewrite(334),rewrite([3286(6)])].

3411 (x' * (y * x')) * x = x * ((x * x)' * y). [back_rewrite(90),rewrite([3286(10)])].

3425 (x * x)' * ((x * y) * x') = x' * (y * x'). [para(16(a,1),3280(a,2,2)),rewrite([2208(3),3165(6)])].

3442 ((x * x) * y) * x'' = x'' * (x * (y * x)). [para(3280(a,1),192(a,1,2,2)),rewrite([157(8)]),flip(a)].

3470 x * (x' * ((x * x) * y)) = x * (x * y). [para(3280(a,1),2544(a,1,1)),rewrite([2177(7),179(4),108(5)]),flip(a)].

3579 x * (((x * x)' * y) * x) = (x' * y) * x. [para(3470(a,1),18(a,1,2,1)),rewrite([18(6),2208(8),208(10)]),flip(a)].

3580 x * ((x * x) * y) = x * (x * (x * y)). [para(3470(a,1),47(a,1,2)),flip(a)].

3587 ((x * x) * y) * x' = (x * (x * y)) * x'. [para(3470(a,1),111(a,1,1)),flip(a)].

3590 x' * ((x * x) * y) = x' * (x * (x * y)). [para(3470(a,1),158(a,1,2)),flip(a)].

3632 (x' * (x' * (y * (x * x)'))) * x = (x * x)' * ((y * x) * (x * x)'). [back_rewrite(3193),rewrite([3579(10)])].

3656 (x * x) * ((y * ((x * x) * (x' * (x * (x * (x * x)))'))) * (x * x)) =(x *(x * y)) * x'. [back_rewrite(2356),rewrite([3587(17)])].

3663 s(A) * (A * x) = A * (s(A) * x). [para(9(a,1),3580(a,1,2,1)),rewrite([1360(14)])].

3664 s(C) * (C * x) = C * (s(C) * x). [para(11(a,1),3580(a,1,2,1)),rewrite([1361(14)])].

3665 (x' * (x' * y)) * x = ((x * x)' * y) * x. [para(3580(a,1),18(a,1,2,1)),rewrite([2295(6),3579(7),2208(8)])].

3671 (x * x)' * (x' * y) = x' * ((x * x)' * y). [para(3580(a,1),158(a,2)),rewrite([2208(5),158(8),2295(11)]),flip(a)].

3704 ((x * x)' * (y * (x * x)')) * x = (x * x)' * ((y * x) * (x * x)'). [back_rewrite(3632),rewrite([3665(8)])].

3834 (x * x)' * (x * (x * (x * (x * x)))) = x * (x * x). [para(28(a,1),2590(a,2,2)),rewrite([1364(3),3251(7),3251(6),143(5),15(4),1979(5),15(7),15(6)]),flip(a)].

3862 ((x * x)' * y) * x = (x * x)' * (y * x). [back_rewrite(2081),rewrite([3834(9),1333(9),6(8),15(7),3579(7),18(6)]),flip(a)].

3876 (x * x)' * ((y * x) * (x * x)') = (x * x)' * (y * (x * (x * x)')). [back_rewrite(3704),rewrite([3862(7),3123(6)]),flip(a)].

3902 (x * x)' * (x * (x * (y * x))) = y * x. [back_rewrite(3270),rewrite([3862(6),3280(5)])].

3904 (x * x)' * (x * (x' * y)) = x * (x' * ((x * x)' * y)). [back_rewrite(2302),rewrite([3862(6),41(5)])].

3909 x * ((x * x)' * (y * (x * (x * x)'))) = x * ((x * x)' * (y * x')). [back_rewrite(3114),rewrite([3876(7)])].

3911 (x * x)' * ((x * x) * y) = (x * x) * ((x * x)' * y). [back_rewrite(3102),rewrite([3902(9),41(5)]),flip(a)].

3913 (x * ((x * x)' * y)) * (x * (z * x')) = x * ((x * x)' * ((y * (x *z)) * x')). [back_rewrite(3171),rewrite([3909(10)]),flip(a)].

3944 A' * (A * A) = A. [para(9(a,1),3902(a,1,2,2,2)),rewrite([9(5),30(8),3663(9),9(8),9(11)])].

3952 (x * x)' * (x * (x * y)) = x * (x' * y). [para(41(a,1),3902(a,1,2,2,2)),rewrite([47(6),41(8)])].

3966 (x * y) * (y * y)' = x * (y * (y * y)'). [para(3902(a,1),501(a,2,1)),rewrite([1986(3),3251(8),3251(7),3952(9),2751(6),3227(5),1986(8)]),flip(a)].

3972 (x * x) * (x' * y) = x' * (x * (x * y)). [para(179(a,1),3902(a,1,2,2,2)),rewrite([2208(3),1986(3),146(8),146(6),179(8)])].

3981 ((x * (x' * y)) * z) * x = (y * z) * x. [para(46(a,1),3902(a,1,2,2)),rewrite([3952(7),124(5)]),flip(a)].

3988 (x * (y * (y' * z))) * y = (x * z) * y. [para(786(a,1),3902(a,1,2,2)),rewrite([3952(7),124(5)]),flip(a)].

3996 (x * x) * (x * (x * (x * x)))' = (x * x)'. [para(2208(a,1),3902(a,1,2,2,2)),rewrite([2208(3),1986(3),2215(7),2208(9)])].

4011 (x * (x * y)) * x' = (x * x) * (y * x'). [back_rewrite(3656),rewrite([3972(9),2265(8),1154(9),3587(7),3425(8),16(6)]),flip(a)].

4056 A' * (A * x) = A * (A' * x). [para(3944(a,1),791(a,2,1)),rewrite([2027(10),3972(11),15(14),4011(13),143(12),3972(13),146(14),146(10)])].

4067 A * ((A * A)' * x) = A' * x. [para(4056(a,1),158(a,1)),rewrite([3286(8)])].

4136 (x * (y' * (y * z))) * y' = (x * z) * y'. [para(3988(a,1),16(a,2)),rewrite([189(6),16(9)])].

4142 (x * (y * (z * (z * z)'))) * z = (x * (y * z''')) * z. [para(200(a,1),3988(a,1,1,2,2)),rewrite([3227(5)])].

4147 ((x * (y * (y' * z))''') * z) * y = (z * ((y * (y' * z))' * x)) * y. [para(202(a,1),3988(a,1,1)),rewrite([3981(10)]),flip(a)].

4162 (x * (y * z'')) * z' = (x * (y * z)) * z'. [para(448(a,1),3988(a,1,1,2,2)),rewrite([243(6),15(3),4136(7)]),flip(a)].

4184 (x * ((y * z') * z')) * z = (x * (y * (z * z)')) * z. [para(2580(a,1),3988(a,1,1,2,2)),rewrite([2208(4),3988(8)]),flip(a)].

4186 x * (x' * (y * (x * (x' * z)))) = x * (x' * (y * z)). [para(3988(a,1),2544(a,1,1)),rewrite([2544(6)]),flip(a)].

4237 (x * (x' * y)) * (x * z) = x * (x' * (y * (x * z))). [para(2963(a,1),791(a,2,1)),rewrite([3913(8),15(9),3862(8),41(7),3904(8),47(9),2963(7)]),flip(a)].

4271 (x * x) * ((x * (x * (x * x)))' * y) = (x * x)' * y. [para(6(a,1),3026(a,1,1,2,1)),rewrite([15(3),3996(6),1364(7)]),flip(a)].

4331 x * ((x * x)' * ((x * (x * x)')' * y)) = x * (x' * y). [para(3026(a,1),2544(a,1,2,2,1)),rewrite([2286(13),2265(13),1986(10),6(9),386(7),15(8),386(7),1976(8),3(6),3162(5),3026(12)]),flip(a)].

4352 x * (x' * ((x * (x' * y)) * z)) = x * (x' * (y * z)). [back_rewrite(3136),rewrite([4331(10)])].

4387 x * ((((y * (x * (x' * (z * z)))') * (x * (x' * z))) * z) * x) = x *((z *((x * (x' * z))' * y)) * x). [back_rewrite(2953),rewrite([4352(7)])].

4558 (x * x)' * (x * y) = x * ((x * x)' * y). [para(3251(a,1),179(a,1,1,2)),rewrite([3257(7),1986(10),6(9),3862(7),3123(6),4142(8),3862(8),202(7),3904(6),47(7),1986(7),3286(13),1364(8),4271(12)]),flip(a)].

4702 x' * ((y * (x * (z * x))) * x') = x' * (x * ((x' * y) * (x * z))). [para(3590(a,1),791(a,2,2)),rewrite([3442(7),189(8),4136(9),1354(14)])].

4928 C * (C * C)' = C'. [para(11(a,1),3996(a,1,1)),rewrite([11(10),31(7),3664(8),11(7),11(11)])].

5802 x * ((y * (z * x')) * (x * x)) = ((x * y) * z) * x. [para(1154(a,1),15(a,1,1)),rewrite([15(6),18(6),2580(9)]),flip(a)].

5805 x * (((x' * y) * z) * x) = x * (x' * (y * (z * x))). [para(1154(a,1),18(a,1,2,1)),rewrite([189(8),145(7),4162(11),41(10)])].

5808 x * ((y * (z * x)) * x') = x * (x * ((x' * y) * z)). [para(1154(a,1),47(a,1,2,2)),rewrite([189(8),108(7),4162(11)]),flip(a)].

5855 x' * (((x' * y) * z) * x) = x' * (x' * (y * (z * x))). [para(1154(a,1),234(a,1,2,1)),rewrite([189(9),145(8),4162(14),41(13),158(14)])].

5894 x * ((x * x)' * (y * (z * x))) = ((x' * y) * z) * x. [para(1154(a,1),3410(a,2,1)),rewrite([4162(8),41(7),4558(8),3671(7),47(9),189(14),145(13)])].

6111 (x' * (x * y)) * y = (x * (x' * y)) * y. [para(2544(a,1),5802(a,2,1)),rewrite([3026(5),2963(6),5802(7),143(3)])].

6811 (x * (y * (y' * (z * z)))') * (y * (y' * z)) = x * ((y * (y' * z)) *(y * (y' * (z * z)))'). [para(4237(a,1),3123(a,1,1,2,1)),rewrite([4186(7),1224(20),4352(20)])].

6837 x * (x' * ((x' * y) * (x * z))) = (x * ((x * x)' * y)) * (x * z). [para(3286(a,1),4237(a,1,1)),flip(a)].

6886 x * (((y * ((x * (x' * z)) * (x * (x' * (z * z)))')) * z) * x) = x *((z *((x * (x' * z))' * y)) * x). [back_rewrite(4387),rewrite([6811(10)])].

6990 x' * (x * (x * ((x' * y) * z))) = (y * (z * x)) * x'. [para(5805(a,1),179(a,1,1)),rewrite([111(7)]),flip(a)].

7025 ((A' * x) * y) * A = A' * (x * (y * A)). [para(5805(a,1),4056(a,1,2)),rewrite([158(11),5855(16),3286(17),5894(16)]),flip(a)].

7183 (x * (y * A')) * A = A' * ((A * x) * y). [para(1154(a,1),7025(a,2,2)),rewrite([4(4),2(6),158(17)])].

7578 x * ((x * x)' * (y * (x * (x' * z)))) = x * ((x * x)' * (y * z)). [para(6(a,1),5894(a,2,1)),rewrite([41(5),3411(14)])].

7686 (((x * (x * x)')' * y) * (z * x)) * (x * (x * x)') = x * (y * z). [para(2544(a,1),5894(a,1,2,2,2)),rewrite([2177(10),113(7),1945(8),1986(6),3026(10),3911(9),3580(10),7578(8),2963(6),47(5)]),flip(a)].

7702 (((x * (x * x)')' * y) * z) * (x * (x * x)') = x * (y * (z * (x * (x* x)'))). [para(5894(a,1),3026(a,1)),rewrite([2177(19),113(16),1945(17),1986(15),3911(20),3580(21),2963(20),47(19)])].

7790 x * (y * (x * (x' * z))) = x * (y * z). [back_rewrite(7686),rewrite([7702(11),2544(5)])].

7808 x * (((y * (x * (x' * z))) * u) * x) = x * (((y * z) * u) * x). [para(7790(a,1),6(a,1,1)),rewrite([6(4)]),flip(a)].

7829 x' * (y * (x * (x' * z))) = x' * (y * z). [para(7790(a,1),146(a,1,2,2)),rewrite([146(6)]),flip(a)].

7891 x * ((x * (x' * y)) * z) = x * (y * z). [para(4237(a,1),7790(a,1,2)),rewrite([7829(6),47(5)]),flip(a)].

8025 x' * ((x * (x' * y)) * z) = x' * (y * z). [para(7891(a,1),146(a,1,2,2)),rewrite([146(6)]),flip(a)].

8811 (x * (y * z''')) * z = (x * (y * z')) * z. [para(143(a,1),4184(a,1,1,2,1)),rewrite([15(5),16(5),3966(8),4142(10)]),flip(a)].

8910 (x * (y * (z * (z * z)'))) * z = (x * (y * z')) * z. [back_rewrite(4142),rewrite([8811(12)])].

9149 x' * (x * (y * y)) = y * y. [para(108(a,1),27(a,1,2)),rewrite([16(5),6(4),4(2),2(2),4(6),2(9),1354(8),6111(6),7891(7)]),flip(a)].

9165 x * (x' * (y * y)) = y * y. [para(158(a,1),27(a,1,2)),rewrite([18(4),6(4),5(2),2(2),5(6),2(9),1224(8),8025(7)]),flip(a)].

9566 x * (((y * ((x * (x' * z)) * (z * z)')) * z) * x) = x * ((z * ((x *(x' * z))' * y)) * x). [back_rewrite(6886),rewrite([9165(7)])].

9811 x' * (x * A) = A. [para(9(a,1),9149(a,1,2,2)),rewrite([9(9)])].

9812 x' * (x * C) = C. [para(11(a,1),9149(a,1,2,2)),rewrite([11(9)])].

9878 x''' * (x * A) = A. [para(9811(a,1),157(a,1,2,2)),rewrite([9811(8)]),flip(a)].

9880 x' * (x * A)'' = A. [para(9811(a,1),192(a,1,2,2)),rewrite([9811(10)]),flip(a)].

9928 (A * (A' * x))''' * (x * A) = A. [para(145(a,1),9878(a,1,2)),rewrite([4056(5)])].

9973 x * (x' * A) = A. [para(9(a,1),9165(a,1,2,2)),rewrite([9(9)])].

9974 x * (x' * C) = C. [para(11(a,1),9165(a,1,2,2)),rewrite([11(9)])].

9990 x * (x' * (y * y)') = (y * y)'. [para(2208(a,1),9165(a,1,2,2)),rewrite([2208(8)])].

10042 x * (x' * A)'' = A. [para(9973(a,1),192(a,1,2,2)),rewrite([9811(12)]),flip(a)].

10059 (x * (x' * y)) * A = x * (x' * (y * A)). [para(9973(a,1),4237(a,1,2)),rewrite([9973(10)])].

10061 (x * (A * x)') * A = 0. [para(9973(a,1),7183(a,2,2)),rewrite([143(8),4056(8),3988(11),4(10)])].

10077 C * ((x * (C * x)') * C) = C. [para(9974(a,1),6(a,1)),flip(a)].

10086 x * (x' * ((x * y) * C)) = (x * y) * C. [para(9974(a,1),791(a,2,2)),rewrite([15(5),3227(6),8910(7),1154(6)])].

10100 x * (x' * ((y * x) * C)) = (y * x) * C. [para(9974(a,1),2949(a,1,2)),flip(a)].

10260 x * (x' * A') = A'. [para(9(a,1),9990(a,1,2,2,1)),rewrite([9(10)])].

10289 (x * (x' * y)) * (z * z)' = x * (x' * (y * (z * z)')). [para(9990(a,1),4237(a,1,2)),rewrite([9990(12)])].

10317 x * ((y * ((x * (x' * y))' * z)) * x) = x * ((y * (y' * z)) * x). [back_rewrite(9566),rewrite([10289(6),7808(10),3162(5)]),flip(a)].

10769 (x * (y * A)) * A' = A * ((A' * x) * y). [para(1333(a,1),4056(a,2,2)),rewrite([5808(10),6990(11),4056(16),47(17)])].

12200 x * (x' * ((y * x) * (z * (y * x)))) = x * (x' * (y * (x * ((z * y)* x)))). [para(2544(a,1),21(a,1,1)),rewrite([28(7),5805(7),15(4),3026(13),4558(12),2963(13),6(13),5805(13),2949(14)]),flip(a)].

13540 x' * ((y * x) * (z * (y * x))) = x' * (y * (x * ((z * y) * x))). [para(12200(a,1),158(a,1,2)),rewrite([158(9)]),flip(a)].

14970 x' * (x * C)'' = C. [para(9812(a,1),192(a,1,2,2)),rewrite([9812(10)]),flip(a)].

15755 x * (((x' * A)'' * y) * x) = A * (y * x). [para(10042(a,1),6(a,1,1)),flip(a)].

15813 x' * (x * (A * y)) = A * (x' * (x * y)). [para(10042(a,1),1333(a,2,2,2,1)),rewrite([15755(12),143(4)]),flip(a)].

15848 (x * (A * x)')' = A. [para(10061(a,1),189(a,2,2)),rewrite([9973(14),3(8)]),flip(a)].

16190 x * (A * x)' = A'. [para(15848(a,1),10260(a,1,2,1)),rewrite([5(8),3(6)])].

16843 (x * C)'' * x = x * (C * x). [para(14970(a,1),18(a,1,2,1)),flip(a)].

21065 (x * (C * x)') * C = 0. [para(10077(a,1),5894(a,1,2,2)),rewrite([386(7),4928(7),5(4),4(5),2(7)]),flip(a)].

21192 (x * (C * x)')' = C. [para(21065(a,1),189(a,2,2)),rewrite([9974(14),3(8)]),flip(a)].

21295 ((A * C)' * A)' = C. [para(16190(a,1),21192(a,1,1,2,1)),rewrite([2027(7)])].

21377 (A * C)'' * C' = A. [para(21295(a,1),9880(a,1,2,1))].

21648 (A * C)'' = A * C. [para(21377(a,1),10086(a,1,2,2,1)),rewrite([55(15),3(7),21377(13)])].

65396 A * (A' * (x * (A * (y * A)))) = ((x * A) * y) * A. [para(9928(a,1),584(a,1,1,1,1)),rewrite([2027(3),9928(12),13540(19),4147(16),10317(15),10059(9),7790(11),9928(24),2027(16)])].

65407 (A' * x) * (A * y) = A' * ((x * A) * y). [para(65396(a,1),16(a,1,2,1)),rewrite([143(10),4056(10),158(11),15(17),4702(17),4056(17),6837(17),4067(13)]),flip(a)].

113321 (x * (A * (C * A))) * A' = (x * A) * C. [para(16843(a,1),10769(a,1,1,2)),rewrite([21648(18),65407(17),10100(18)])].

114419 (A * (x * A)) * C = A * (x * (A * C)). [para(15(a,1),113321(a,2,1)),rewrite([28(8),179(11),15813(11),4056(10),47(11)]),flip(a)].

114420 $F. [resolve(114419,a,22,a)].

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

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

Given=7320. Generated=28814228. Kept=114417. proofs=1.

Usable=6135. Sos=19933. Demods=25982. Limbo=0, Disabled=88359. Hints=2189.

Kept_by_rule=0, Deleted_by_rule=95690.

Forward_subsumed=16210723. Back_subsumed=786.

Sos_limit_deleted=12393398. Sos_displaced=57136. Sos_removed=0.

New_demodulators=113569 (0 lex), Back_demodulated=30426. Back_unit_deleted=0.

Demod_attempts=1395662518. Demod_rewrites=151131629.

Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0.

Nonunit_fsub_feature_tests=0. Nonunit_bsub_feature_tests=0.

Megabytes=93.38.

User_CPU=1195.32, System_CPU=34.30, Wall_clock=1233.

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

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

THEOREM PROVED

Exiting with 1 proof.

Process 14654 exit (max_proofs) Mon Jul 18 16:47:25 2011