% Proof 1 at 0.90 (+ 0.01) seconds.

% Length of proof is 51.

% Level of proof is 10.

% Maximum clause weight is 20.000.

% Given clauses 209.

1 (z * (A * y)) * z = (z * A) * (y * z) # 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 * (x \ y) = y. [assumption].

7 x \ (x * y) = y. [assumption].

8 (x * y) / y = x. [assumption].

9 (x / y) * y = x. [assumption].

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

11 x' * (x * y) = y. [assumption].

13 x * ((y * A) * x) = (x * y) * (A * x). [assumption].

14 (x * y) * (A * x) = x * ((y * A) * x). [copy(13),flip(a)].

15 (c1 * (A * c2)) * c1 != (c1 * A) * (c2 * c1). [deny(1)].

19 x \ 0 = x'. [para(4(a,1),7(a,1,2))].

20 x'' = x. [para(5(a,1),7(a,1,2)),rewrite([19(3)])].

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

31 (x * (y * (x * z))) / z = x * (y * x). [para(10(a,1),8(a,1,1))].

32 x * ((y / x) * (x * z)) = (x * y) * z. [para(9(a,1),10(a,1,1,2)),flip(a)].

35 x \ y = x' * y. [para(6(a,1),11(a,1,2)),flip(a)].

36 x / (y * x) = y'. [para(11(a,1),8(a,1,1))].

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

42 x * (x' * y) = y. [back_rewrite(6),rewrite([35(1)])].

50 x' * ((x * A) * x') = A * x'. [para(5(a,1),14(a,1,1)),rewrite([2(5)]),flip(a)].

52 (x / y) * ((y * A) * (x / y)) = x * (A * (x / y)). [para(9(a,1),14(a,1,1)),flip(a)].

56 (x * y)' * (x * ((y * A) * x)) = A * x. [para(14(a,1),11(a,1,2))].

68 (x / y)' = y / x. [para(9(a,1),36(a,1,2)),flip(a)].

77 (x * y) / x' = x * (y * x). [para(4(a,1),31(a,1,1,2,2)),rewrite([3(2)])].

79 x * ((x * y)' * x) = x / y. [para(5(a,1),31(a,1,1,2)),rewrite([3(2)]),flip(a)].

80 ((x / y) * (z * x)) / y = (x / y) * (z * (x / y)). [para(9(a,1),31(a,1,1,2,2))].

107 (x * y) * x' = x * (y / x). [para(4(a,1),32(a,1,2,2)),rewrite([3(3)]),flip(a)].

121 A / x = A * x'. [back_rewrite(50),rewrite([107(5),11(5)])].

127 A * (x * A)' = x'. [para(121(a,1),36(a,1))].

148 (x * A)' = A' * x'. [para(127(a,1),11(a,1,2)),flip(a)].

250 (x * y) / (z * ((z * (x * z))' * y)) = x * (z * x). [para(41(a,1),31(a,1,1,2))].

568 (x * (y * x))' = x' / (x * y). [para(77(a,1),68(a,1,1))].

600 (x * y) / (z * ((z' / (z * x)) * y)) = x * (z * x). [back_rewrite(250),rewrite([568(4)])].

699 (x * y)' * x = x' * (x / y). [para(79(a,1),11(a,1,2)),flip(a)].

700 x' / (x * y) = x' * (y' * x'). [para(11(a,1),79(a,1,2,1,1)),flip(a)].

724 (x * y) / (x' * (z' * y)) = x * (z * x). [back_rewrite(600),rewrite([700(4),10(7),42(8)])].

741 x' * ((x / y) * x') = (x * y)'. [para(107(a,1),36(a,1,2)),rewrite([700(4),68(3)])].

823 (x / y) * ((y * A) * x) = x * (A * x). [para(56(a,1),10(a,2,2)),rewrite([699(3),42(4)])].

832 (x * (A * x)) / ((y * A) * x) = x / y. [para(56(a,1),31(a,1,1,2)),rewrite([699(10),42(11)])].

2125 (x * (A * x)) / y = x * (A * (x / y)). [para(52(a,1),80(a,2)),rewrite([823(5)])].

2176 x / y = x * y'. [back_rewrite(832),rewrite([2125(7),36(5),148(4),42(6)]),flip(a)].

2568 (x * y)' = y' * x'. [back_rewrite(741),rewrite([2176(2),107(5),2176(3),11(6)]),flip(a)].

2576 (x * y) * ((y' * z) * x) = x * (z * x). [back_rewrite(724),rewrite([2176(6),2568(6),2568(4),20(4),20(5)])].

2700 (x * y) * x = x * (y * x). [back_rewrite(77),rewrite([2176(3),20(3)])].

3150 (c1 * A) * (c2 * c1) != c1 * ((A * c2) * c1). [back_rewrite(15),rewrite([2700(7)]),flip(a)].

6793 (x * y) * (z * x) = x * ((y * z) * x). [para(11(a,1),2576(a,1,2,1))].

6794 $F. [resolve(6793,a,3150,a)].

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

% Proof 1 at 6.11 (+ 0.03) seconds.

% Length of proof is 99.

% Level of proof is 35.

% Maximum clause weight is 25.000.

% Given clauses 423.

1 z * (x * (z * A)) = ((z * x) * z) * A # 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 * (x \ y) = y. [assumption].

7 x \ (x * y) = y. [assumption].

8 (x * y) / y = x. [assumption].

9 (x / y) * y = x. [assumption].

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

11 x' * (x * y) = y. [assumption].

12 (x * x) * y = x * (x * y). [assumption].

13 (x * (A * y)) * x = (x * A) * (y * x). [assumption].

14 ((c1 * c2) * c1) * A != c1 * (c2 * (c1 * A)). [deny(1)].

18 x \ 0 = x'. [para(4(a,1),7(a,1,2))].

19 x'' = x. [para(5(a,1),7(a,1,2)),rewrite([18(3)])].

20 x / x = 0. [para(2(a,1),8(a,1,1))].

30 (x * (y * (x * z))) / z = x * (y * x). [para(10(a,1),8(a,1,1))].

31 x * ((y / x) * (x * z)) = (x * y) * z. [para(9(a,1),10(a,1,1,2)),flip(a)].

34 x \ y = x' * y. [para(6(a,1),11(a,1,2)),flip(a)].

35 x / (y * x) = y'. [para(11(a,1),8(a,1,1))].

41 x * (x' * y) = y. [back_rewrite(6),rewrite([34(1)])].

43 (x * (x * y)) / y = x * x. [para(12(a,1),8(a,1,1))].

47 (x * A) * (A' * x) = x * x. [para(4(a,1),13(a,1,1,2)),rewrite([3(2)]),flip(a)].

49 ((x * A) * (y * x)) / x = x * (A * y). [para(13(a,1),8(a,1,1))].

66 (x / y)' = y / x. [para(9(a,1),35(a,1,2)),flip(a)].

71 (x * A) * ((A' * y) * x) = (x * y) * x. [para(41(a,1),13(a,1,1,2)),flip(a)].

73 (x / y) * ((y / x) * z) = z. [para(66(a,1),11(a,1,1))].

74 (x * y) / x' = x * (y * x). [para(4(a,1),30(a,1,1,2,2)),rewrite([3(2)])].

76 x * ((x * y)' * x) = x / y. [para(5(a,1),30(a,1,1,2)),rewrite([3(2)]),flip(a)].

78 x * ((y / (x * z)) * x) = (x * y) / z. [para(9(a,1),30(a,1,1,2)),flip(a)].

102 (x * y) * x' = x * (y / x). [para(4(a,1),31(a,1,2,2)),rewrite([3(3)]),flip(a)].

103 (x' * y) * x = x' * (y / x'). [para(5(a,1),31(a,1,2,2)),rewrite([3(5)]),flip(a)].

108 (x / y) * (y * z) = y' * ((y * x) * z). [para(31(a,1),11(a,1,2)),flip(a)].

109 (x' * y) * (x * z) = x' * ((y / x') * z). [para(11(a,1),31(a,1,2,2)),flip(a)].

112 (x * y) * (x' * z) = x * ((y / x) * z). [para(41(a,1),31(a,1,2,2)),flip(a)].

125 (x * y) / (x' * y) = x * x. [para(41(a,1),43(a,1,1,2))].

157 (x * x) / (A' * x) = x * A. [para(47(a,1),8(a,1,1))].

161 (x * A)' * (x * x) = A' * x. [para(47(a,1),11(a,1,2))].

178 (x * (y * x))' = x' / (x * y). [para(74(a,1),66(a,1,1))].

196 (x * y)' * x = x' * (x / y). [para(76(a,1),11(a,1,2)),flip(a)].

197 x' / (x * y) = x' * (y' * x'). [para(11(a,1),76(a,1,2,1,1)),flip(a)].

210 (x * (y * x))' = x' * (y' * x'). [back_rewrite(178),rewrite([197(6)])].

262 ((A * x) * (A * x)) / x = (A * x) * A. [para(11(a,1),157(a,1,2))].

273 (x / A) * x = x * (A' * x). [para(161(a,1),10(a,2,2)),rewrite([196(4),41(5)])].

291 ((x * A) * y) / x = x * (A * (y / x)). [para(9(a,1),49(a,1,1,2))].

296 x * (A * (x * A)') = 0. [para(41(a,1),49(a,1,1)),rewrite([20(1)]),flip(a)].

309 A * (x * A)' = x'. [para(296(a,1),11(a,1,2)),rewrite([3(3)]),flip(a)].

317 A / x = A * x'. [para(9(a,1),309(a,1,2,1)),rewrite([66(6)]),flip(a)].

320 (x * A)' = A' * x'. [para(309(a,1),11(a,1,2)),flip(a)].

342 (A * x') * x = A. [para(317(a,1),9(a,1,1))].

349 (A * x) * x' = A. [para(19(a,1),342(a,1,1,2))].

387 (A * x)' = x' / A. [para(349(a,1),35(a,1,2)),flip(a)].

388 x * (A' * x)' = A. [para(41(a,1),349(a,1,1))].

396 (A * x) * (A * x) = A * (x * (A * x)). [para(349(a,1),125(a,1,1)),rewrite([387(4),273(6),317(8),210(8),19(3),19(4),19(4)]),flip(a)].

403 (A * x) * A = A * (x * A). [back_rewrite(262),rewrite([396(5),30(6)]),flip(a)].

429 (A' * x)' = x' * A. [para(388(a,1),11(a,1,2)),flip(a)].

436 (A' * x') * (x * A) = 0. [para(320(a,1),5(a,1,1))].

440 (x * A) * ((A' * x') * y) = y. [para(320(a,1),41(a,1,2,1))].

525 (x' * A) * ((A' * x) * y) = y. [para(429(a,1),11(a,1,1))].

575 x / A' = x * A. [para(41(a,1),403(a,1,1)),rewrite([103(8),41(10)]),flip(a)].

616 (x * A') * A = x. [para(575(a,1),8(a,1))].

617 (x * A) * A' = x. [para(575(a,1),9(a,1,1))].

622 x / A = x * A'. [para(616(a,1),8(a,1,1))].

676 (A' * x') * x = A'. [para(617(a,1),11(a,1,2)),rewrite([320(3)])].

798 (A' * x) * x' = A'. [para(19(a,1),676(a,1,1,2))].

820 ((A' * x) * (y * A')) / x' = (A' * x) * (y * (A' * x)). [para(798(a,1),30(a,1,1,2,2))].

857 ((A' * x') * y) / (x * A) = (A' * x') * (y * (A' * x')). [para(436(a,1),30(a,1,1,2,2)),rewrite([3(6)])].

1873 (x / (y * z)) * y = y' * ((y * x) / z). [para(78(a,1),11(a,1,2)),flip(a)].

1894 x * ((A * x') * ((x * y) * A)) = ((x * A) * y) * A. [para(617(a,1),78(a,1,2,1,2)),rewrite([108(6),112(8),317(2),575(14)])].

1901 (A' * x) * ((y * A) * (A' * x)) = ((A' * x) * y) / x'. [para(798(a,1),78(a,1,2,1,2)),rewrite([575(6)])].

3465 (x * A) * (A' * y) = A * ((A' * x) * y). [para(575(a,1),108(a,1,1)),rewrite([19(9)])].

3595 ((A' * x) * y) / x' = A' * ((x * y) * x). [back_rewrite(1901),rewrite([3465(9),109(10),575(5),71(9)]),flip(a)].

3685 (A' * x) * (y * (A' * x)) = A' * ((x * (y * A')) * x). [back_rewrite(820),rewrite([3595(9)]),flip(a)].

3740 ((A' * x') * y) / (x * A) = A' * ((x' * (y * A')) * x'). [back_rewrite(857),rewrite([3685(18)])].

5500 x' * ((x * y) * x) = y / x'. [para(525(a,1),291(a,1,1)),rewrite([3595(10),41(10)]),flip(a)].

5561 (x * y) * x = x * (y / x'). [para(5500(a,1),11(a,1,2)),rewrite([19(2)]),flip(a)].

5700 ((A' * x') * y) / (x * A) = A' * (x' * ((y * A') / x)). [back_rewrite(3740),rewrite([5561(17),19(16)])].

5755 ((A' * x) * y) / x' = A' * (x * (y / x')). [back_rewrite(3595),rewrite([5561(10)])].

5818 (c1 * (c2 / c1')) * A != c1 * (c2 * (c1 * A)). [back_rewrite(14),rewrite([5561(5)])].

5819 (x * A) * (y * x) = x * ((A * y) / x'). [back_rewrite(13),rewrite([5561(4)]),flip(a)].

14249 ((x * y) / z) * (x' * ((x * z) / y)) = x. [para(1873(a,1),11(a,1,2)),rewrite([66(3)])].

17090 (x * ((A * y) / x')) / (y * x) = x * A. [para(5819(a,1),8(a,1,1))].

21742 ((x * (y * x)) / ((A * y) / x')) * A = x. [para(17090(a,1),14249(a,1,2,2)),rewrite([11(11)])].

22695 ((x / y) / ((A * (y * x)) / y)) * A = y'. [para(102(a,1),21742(a,1,1,1,2)),rewrite([11(4),19(6)])].

23206 (((A * (x * y)) / x) / (y / x)) * x' = A. [para(22695(a,1),73(a,1,2))].

23566 ((A * (x * y)) / x) / (y / x) = A * x. [para(23206(a,1),8(a,1,1)),rewrite([317(3),19(3)]),flip(a)].

23711 (A * (x * y)) / x = (A * x) * (y / x). [para(23566(a,1),9(a,1,1)),flip(a)].

23852 ((A * x) * (y / x)) * x = A * (x * y). [para(23711(a,1),9(a,1,1))].

24093 (A * ((x * A') / y)) * (y * A) = A * x. [para(440(a,1),23852(a,2,2)),rewrite([5700(12),112(14),622(5),617(6),41(8)])].

24593 (A * (x / y)) * (y * A) = A * (x * A). [para(9(a,1),24093(a,1,1,2,1)),rewrite([575(10)])].

24639 (A * x) * (y * A) = A * ((x * y) * A). [para(8(a,1),24593(a,1,1,2))].

24646 (x * (A * (y * A))) * A' = x * ((A * (y / x)) * x). [para(24593(a,1),30(a,1,1,2)),rewrite([622(7)])].

24808 ((x * A) * y) * A = x * (A * (y * A)). [back_rewrite(1894),rewrite([24639(7),11(4)]),flip(a)].

25244 (x * (A * (y * A))) * A' = (x * A) * y. [para(24808(a,1),8(a,1,1)),rewrite([622(7)])].

25335 x * ((A * (y / x)) * x) = (x * A) * y. [back_rewrite(24646),rewrite([25244(8)]),flip(a)].

25748 (x / y') / y = x. [para(525(a,1),25335(a,2)),rewrite([5755(8),41(9),102(6),11(6)])].

25896 x / y = x * y'. [para(8(a,1),25748(a,1,1))].

34225 $F. [back_rewrite(5818),rewrite([25896(5),19(5),10(7)]),xx(a)].

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

% Proof 1 at 0.20 (+ 0.01) seconds.

% Length of proof is 36.

% Level of proof is 9.

% Maximum clause weight is 17.000.

% Given clauses 85.

1 ((A * z) * y) * z = A * (z * (y * z)) # label(non_clause) # label(goal). [goal].

3 x * 0 = x. [assumption].

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

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

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

7 x \ (x * y) = y. [assumption].

8 (x * y) / y = x. [assumption].

9 (x / y) * y = x. [assumption].

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

11 x' * (x * y) = y. [assumption].

13 x * (y * (x * A)) = ((x * y) * x) * A. [assumption].

14 ((x * y) * x) * A = x * (y * (x * A)). [copy(13),flip(a)].

15 ((A * c1) * c2) * c1 != A * (c1 * (c2 * c1)). [deny(1)].

19 x \ 0 = x'. [para(4(a,1),7(a,1,2))].

20 x'' = x. [para(5(a,1),7(a,1,2)),rewrite([19(3)])].

31 (x * (y * (x * z))) / z = x * (y * x). [para(10(a,1),8(a,1,1))].

32 x * ((y / x) * (x * z)) = (x * y) * z. [para(9(a,1),10(a,1,1,2)),flip(a)].

35 x \ y = x' * y. [para(6(a,1),11(a,1,2)),flip(a)].

36 x / (y * x) = y'. [para(11(a,1),8(a,1,1))].

42 x * (x' * y) = y. [back_rewrite(6),rewrite([35(1)])].

48 (x * y) * x = x * (y * x). [para(14(a,1),8(a,1,1)),rewrite([31(6)]),flip(a)].

75 (x * (y * z)) / (x' * z) = x * (y * x). [para(42(a,1),31(a,1,1,2,2))].

91 (x * y) * x' = x * (y / x). [para(4(a,1),32(a,1,2,2)),rewrite([3(3)]),flip(a)].

97 (x / y) * (y * z) = y' * ((y * x) * z). [para(32(a,1),11(a,1,2)),flip(a)].

100 (x * y) * (x' * z) = x * ((y / x) * z). [para(42(a,1),32(a,1,2,2)),flip(a)].

125 x / y = x * y'. [para(11(a,1),48(a,1,1)),rewrite([91(6),11(6)]),flip(a)].

147 (x * y) * (x' * z) = x * ((y * x') * z). [back_rewrite(100),rewrite([125(5)])].

150 (x * y') * (y * z) = y' * ((y * x) * z). [back_rewrite(97),rewrite([125(1)])].

157 (x * (y * z)) * (x' * z)' = x * (y * x). [back_rewrite(75),rewrite([125(5)])].

170 x * (y * x)' = y'. [back_rewrite(36),rewrite([125(2)])].

173 (x * y) * y' = x. [back_rewrite(8),rewrite([125(2)])].

208 (x * y)' = y' * x'. [para(170(a,1),11(a,1,2)),flip(a)].

221 (x * (y * z)) * (z' * x) = x * (y * x). [back_rewrite(157),rewrite([208(5),20(5)])].

1772 (x * y) * (z * x) = x * ((y * z) * x). [para(173(a,1),221(a,1,1,2)),rewrite([20(3)])].

2144 ((x * y) * z) * y = x * (y * (z * y)). [para(11(a,1),1772(a,1,2)),rewrite([150(8),147(9),1772(8),11(6)])].

2145 $F. [resolve(2144,a,15,a)].

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

% Proof 1 at 21.98 (+ 0.09) seconds.

% Length of proof is 105.

% Level of proof is 28.

% Maximum clause weight is 31.000.

% Given clauses 646.

1 ((x * z) * A) * z = x * (z * (A * z)) # label(non_clause) # label(goal). [goal].

3 x * 0 = x. [assumption].

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

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

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

7 x \ (x * y) = y. [assumption].

8 (x * y) / y = x. [assumption].

9 (x / y) * y = x. [assumption].

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

11 x' * (x * y) = y. [assumption].

13 ((A * x) * y) * x = A * (x * (y * x)). [assumption].

14 ((c1 * c2) * A) * c2 != c1 * (c2 * (A * c2)). [deny(1)].

18 x \ 0 = x'. [para(4(a,1),7(a,1,2))].

19 x'' = x. [para(5(a,1),7(a,1,2)),rewrite([18(3)])].

30 (x * (y * (x * z))) / z = x * (y * x). [para(10(a,1),8(a,1,1))].

31 x * ((y / x) * (x * z)) = (x * y) * z. [para(9(a,1),10(a,1,1,2)),flip(a)].

32 (x * (y * (z * (y * x)))) * u = x * (y * (z * (y * (x * u)))). [para(10(a,1),10(a,1,1,2)),rewrite([10(9)])].

34 x \ y = x' * y. [para(6(a,1),11(a,1,2)),flip(a)].

35 x / (y * x) = y'. [para(11(a,1),8(a,1,1))].

41 x * (x' * y) = y. [back_rewrite(6),rewrite([34(1)])].

49 (A * (x * (y * x))) / x = (A * x) * y. [para(13(a,1),8(a,1,1))].

53 ((A * x) * y)' * (A * (x * (y * x))) = x. [para(13(a,1),11(a,1,2))].

63 (x / y)' = y / x. [para(9(a,1),35(a,1,2)),flip(a)].

69 A * (x * (((A * x)' * y) * x)) = y * x. [para(41(a,1),13(a,1,1)),flip(a)].

70 (x / y) * (y / x) = 0. [para(63(a,1),4(a,1,2))].

71 (x / y) * ((y / x) * z) = z. [para(63(a,1),11(a,1,1))].

72 (x * y) / x' = x * (y * x). [para(4(a,1),30(a,1,1,2,2)),rewrite([3(2)])].

74 x * ((x * y)' * x) = x / y. [para(5(a,1),30(a,1,1,2)),rewrite([3(2)]),flip(a)].

76 x * ((y / (x * z)) * x) = (x * y) / z. [para(9(a,1),30(a,1,1,2)),flip(a)].

101 (x * y) * x' = x * (y / x). [para(4(a,1),31(a,1,2,2)),rewrite([3(3)]),flip(a)].

102 (x' * y) * x = x' * (y / x'). [para(5(a,1),31(a,1,2,2)),rewrite([3(5)]),flip(a)].

107 (x / y) * (y * z) = y' * ((y * x) * z). [para(31(a,1),11(a,1,2)),flip(a)].

108 (x' * y) * (x * z) = x' * ((y / x') * z). [para(11(a,1),31(a,1,2,2)),flip(a)].

111 (x * y) * (x' * z) = x * ((y / x) * z). [para(41(a,1),31(a,1,2,2)),flip(a)].

155 (x * (y * (z * (u * (z * (y * (x * w))))))) / w = x * (y * (z * (u * (z * (y * x))))). [para(32(a,1),30(a,1,1,2)),rewrite([32(13)])].

184 (x * (y * x))' = x' / (x * y). [para(72(a,1),63(a,1,1))].

229 x' / (x * y) = x' * (y' * x'). [para(11(a,1),74(a,1,2,1,1)),flip(a)].

244 (x * (y * x))' = x' * (y' * x'). [back_rewrite(184),rewrite([229(6)])].

286 (A * x') * x = A. [para(4(a,1),49(a,1,1,2,2)),rewrite([3(4),8(5)]),flip(a)].

287 (A * x) * x' = A. [para(5(a,1),49(a,1,1,2,2)),rewrite([3(3),8(3)]),flip(a)].

288 (A * (x * y)) / x = (A * x) * (y / x). [para(9(a,1),49(a,1,1,2,2))].

291 (A * x) * A = A * (x * A). [para(49(a,1),30(a,1))].

295 (A * (x / y)) / y' = (A * y') * (y * x). [para(101(a,1),49(a,1,1,2,2)),rewrite([11(5)])].

297 A / x = A * x'. [para(286(a,1),8(a,1,1))].

315 (A * x)' = x' / A. [para(287(a,1),35(a,1,2)),flip(a)].

316 x * (A' * x)' = A. [para(41(a,1),287(a,1,1))].

356 A * (x * (((x' / A) * y) * x)) = y * x. [back_rewrite(69),rewrite([315(4)])].

357 A * (x * A)' = x'. [para(297(a,1),35(a,1))].

358 (A * x') * (x / A) = 0. [para(297(a,1),70(a,1,1))].

370 (A * (x' / A)) * (A * x) = A. [para(315(a,1),286(a,1,1,2))].

402 (A' * x)' = x' * A. [para(316(a,1),11(a,1,2)),flip(a)].

412 (x * A)' = A' * x'. [para(357(a,1),11(a,1,2)),flip(a)].

418 x' / A = x' * A'. [para(315(a,1),357(a,2)),rewrite([291(5),244(6),41(9)]),flip(a)].

423 (A * (x' * A')) * (A * x) = A. [back_rewrite(370),rewrite([418(4)])].

432 A * (x * (((x' * A') * y) * x)) = y * x. [back_rewrite(356),rewrite([418(4)])].

451 (A * x)' = x' * A'. [back_rewrite(315),rewrite([418(6)])].

453 x / A = x * A'. [para(358(a,1),11(a,1,2)),rewrite([451(4),19(2),3(5)]),flip(a)].

485 (x * A) * A' = x. [para(453(a,1),8(a,1))].

486 (x * A') * A = x. [para(453(a,1),9(a,1,1))].

487 (x * (y * (x * A))) * A' = x * (y * x). [para(453(a,1),30(a,1))].

528 x / A' = x * A. [para(485(a,1),8(a,1,1))].

531 A' / x = A' * x'. [para(485(a,1),35(a,1,2)),rewrite([412(6)])].

544 (x * (y * (x * A'))) * A = x * (y * x). [para(10(a,1),486(a,1,1))].

559 (A' * x') * ((x * A) * y) = y. [para(528(a,1),71(a,1,2,1)),rewrite([531(3)])].

1314 (A * (A * x')) * x = A * A. [para(423(a,1),10(a,2,2)),rewrite([291(9),486(8)])].

1355 (A * x') * (x * A) = A * A. [para(412(a,1),1314(a,1,1,2,2)),rewrite([41(7)])].

1403 (x * A) * A = x * (A * A). [para(1355(a,1),10(a,2,2)),rewrite([286(4)])].

1594 x * ((y / (x * z)) * (x * u)) = ((x * y) / z) * u. [para(76(a,1),10(a,1,1)),flip(a)].

1598 (x * y) / (x' * z) = x * ((y / z) * x). [para(41(a,1),76(a,1,2,1,2)),flip(a)].

1610 x * ((A * x') * ((x * y) * A)) = ((x * A) * y) * A. [para(485(a,1),76(a,1,2,1,2)),rewrite([107(6),111(8),297(2),528(14)])].

3265 (A * x') * (x * y) = x' * ((x * A) * y). [para(297(a,1),107(a,1,1))].

3277 (x * A) * (A' * y) = A * ((A' * x) * y). [para(528(a,1),107(a,1,1)),rewrite([19(9)])].

3406 (A * (x / y)) / y' = y' * ((y * A) * x). [back_rewrite(295),rewrite([3265(10)])].

5174 x' * ((x * A) * (y * x)) = (A * y) / x'. [para(11(a,1),288(a,1,1,2)),rewrite([72(10),3265(10)]),flip(a)].

8206 x * (y * (A * (((A * y) * x)' * (A * (y * x))))) = (x * (y * (A * y))) / y. [para(53(a,1),155(a,1,1,2,2,2)),flip(a)].

20667 A * (((A' * x) * y) / x') = (x * y) * x. [para(108(a,1),432(a,1,2,2,1)),rewrite([531(6),19(6),102(8),41(10)])].

22822 (x * A) * ((A' * y) * (x * A)) = A * ((((A' * x) * y) / x') * A). [para(3277(a,1),72(a,1,1)),rewrite([412(9),1598(11)]),flip(a)].

22854 A' * ((x * A) * ((A' * y) * x)) = ((A' * x) * y) / x'. [para(3277(a,1),487(a,2,2)),rewrite([102(10),528(10),3277(11),108(12),528(5),22

822(11),11(13),485(11),108(16),528(11)]),flip(a)].

23156 (A * (x / y')) / y = y * ((y' * A) * x). [para(19(a,1),3406(a,1,2)),rewrite([19(7)])].

24464 (x * (A * A)) * (y * x) = (x * A) * ((A * y) / x'). [para(5174(a,1),10(a,2,2)),rewrite([11(6),1403(4)])].

24466 (x * A) * (y * x) = x * ((A * y) / x'). [para(5174(a,1),11(a,1,2)),rewrite([19(2)]),flip(a)].

24513 (A * (x * A)) / (y' * A) = A * (x / y'). [para(3277(a,1),5174(a,1,2,2)),rewrite([402(4),102(8),528(8),108(15),528(10),1403(9),24464(14

),41(12),3277(12),559(11),402(12)]),flip(a)].

24538 ((A' * x) * y) / x' = A' * (x * (y / x')). [back_rewrite(22854),rewrite([24466(9),41(7)]),flip(a)].

24610 (x * y) * x = x * (y / x'). [back_rewrite(20667),rewrite([24538(7),41(8)]),flip(a)].

24912 x / (x * (y / x')) = (x * y)'. [para(24610(a,1),35(a,1,2))].

34466 (A * (x * A)) / (y * A) = A * (x / y). [para(19(a,1),24513(a,1,2,1)),rewrite([19(10)])].

34525 (A * (x / y)) * (y * A) = A * (x * A). [para(34466(a,1),9(a,1,1))].

34661 (A * x) * (y * A) = A * ((x * y) * A). [para(8(a,1),34525(a,1,1,2))].

34807 ((x * A) * y) * A = x * (A * (y * A)). [back_rewrite(1610),rewrite([34661(7),11(4)]),flip(a)].

34964 (x * (A * ((y * x) * A))) * A' = x * ((A * y) * x). [para(34661(a,1),30(a,1,1,2)),rewrite([453(8)])].

35219 (x * (A * (y * A))) * A' = (x * A) * y. [para(34807(a,1),8(a,1,1)),rewrite([453(7)])].

35282 x * ((A * y) / x') = x * ((A * y) * x). [back_rewrite(34964),rewrite([35219(9),24466(4)])].

35466 (x * A) * (y * x) = x * ((A * y) * x). [back_rewrite(24466),rewrite([35282(9)])].

35707 (A * x) / y = (A * x) * y'. [para(35466(a,1),23156(a,2,2)),rewrite([8(5),41(10)])].

36799 x / y = x * y'. [para(41(a,1),35707(a,1,1)),rewrite([41(6)])].

41471 (x * y)' = y' * x'. [back_rewrite(24912),rewrite([36799(2),19(2),36799(3),244(3),41(6)]),flip(a)].

44627 x * (y * (A * ((x' * (y' * A')) * (A * (y * x))))) = (x * (y * (A * y))) * y'. [back_rewrite(8206),rewrite([41471(5),41471(5),36799(19

)])].

45548 x * ((y * (z' * x')) * (x * u)) = ((x * y) * z') * u. [back_rewrite(1594),rewrite([36799(2),41471(2),36799(9)])].

45608 (x * y') * (y * z) = y' * ((y * x) * z). [back_rewrite(107),rewrite([36799(1)])].

45621 (x * y') * y = x. [back_rewrite(9),rewrite([36799(1)])].

48646 (x * (y * (A * y))) * y' = x * ((y * (A * x')) * x). [back_rewrite(44627),rewrite([45548(12),45608(7),41(8)]),flip(a)].

49276 x * ((y * (A * x')) * x) = (x * y) * A. [para(45621(a,1),544(a,1,1,2)),rewrite([41471(7),19(6)]),flip(a)].

49323 (x * (y * (A * y))) * y' = (x * y) * A. [back_rewrite(48646),rewrite([49276(12)])].

52433 ((x * y) * A) * y = x * (y * (A * y)). [para(49323(a,1),45621(a,1,1))].

52434 $F. [resolve(52433,a,14,a)].

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

% Proof 1 at 0.28 (+ 0.00) seconds.

% Length of proof is 17.

% Level of proof is 5.

% Maximum clause weight is 16.000.

% Given clauses 174.

1 z * ((x * A) * z) = (z * x) * (A * z) # label(non_clause) # label(goal). [goal].

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

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

7 x \ (x * y) = y. [assumption].

9 (x / y) * y = x. [assumption].

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

11 x' * (x * y) = y. [assumption].

13 ((x * y) * A) * y = x * (y * (A * y)). [assumption].

14 (c1 * c2) * (A * c1) != c1 * ((c2 * A) * c1). [deny(1)].

18 x \ 0 = x'. [para(4(a,1),7(a,1,2))].

19 x'' = x. [para(5(a,1),7(a,1,2)),rewrite([18(3)])].

31 x * ((y / x) * (x * z)) = (x * y) * z. [para(9(a,1),10(a,1,1,2)),flip(a)].

49 (x / y) * (y * (A * y)) = (x * A) * y. [para(9(a,1),13(a,1,1,1)),flip(a)].

108 (x / y) * (y * z) = y' * ((y * x) * z). [para(31(a,1),11(a,1,2)),flip(a)].

117 x' * ((x * y) * (A * x)) = (y * A) * x. [back_rewrite(49),rewrite([108(5)])].

3947 (x * y) * (A * x) = x * ((y * A) * x). [para(117(a,1),11(a,1,2)),rewrite([19(2)]),flip(a)].

3948 $F. [resolve(3947,a,14,a)].

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

% Proof 1 at 0.00 (+ 0.00) seconds.

% Length of proof is 9.

% Level of proof is 3.

% Maximum clause weight is 15.000.

% Given clauses 12.

1 (A * (x * y)) * A = (A * x) * (y * A) # label(non_clause) # label(goal). [goal].

2 0 * x = x. [assumption].

3 x * 0 = x. [assumption].

13 A * ((x * y) * A) = (A * x) * (y * A). [assumption].

14 (A * x) * (y * A) = A * ((x * y) * A). [copy(13),flip(a)].

15 (A * (c1 * c2)) * A != (A * c1) * (c2 * A). [deny(1)].

16 (A * (c1 * c2)) * A != A * ((c1 * c2) * A). [copy(15),rewrite([14(14)])].

49 (A * x) * A = A * (x * A). [para(2(a,1),14(a,1,2)),rewrite([3(7)])].

50 $F. [resolve(49,a,16,a)].

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

% Proof 1 at 0.02 (+ 0.00) seconds.

% Length of proof is 11.

% Level of proof is 4.

% Maximum clause weight is 19.000.

% Given clauses 59.

1 ((x * A) * y) * A = x * (A * (y * A)) # label(non_clause) # label(goal). [goal].

2 0 * x = x. [assumption].

3 x * 0 = x. [assumption].

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

11 x' * (x * y) = y. [assumption].

13 (A * (x * y)) * A = (A * x) * (y * A). [assumption].

14 ((c1 * A) * c2) * A != c1 * (A * (c2 * A)). [deny(1)].

47 (A * x) * A = A * (x * A). [para(2(a,1),13(a,1,1,2)),rewrite([3(7)])].

59 A * (((x * A) * y) * A) = A * (x * (A * (y * A))). [para(10(a,1),13(a,2)),rewrite([47(7)])].

498 ((x * A) * y) * A = x * (A * (y * A)). [para(59(a,1),11(a,1,2)),rewrite([11(10)]),flip(a)].

499 $F. [resolve(498,a,14,a)].

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

% Proof 1 at 0.25 (+ 0.00) seconds.

% Length of proof is 17.

% Level of proof is 5.

% Maximum clause weight is 16.000.

% Given clauses 169.

1 A * ((x * y) * A) = (A * x) * (y * A) # label(non_clause) # label(goal). [goal].

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

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

7 x \ (x * y) = y. [assumption].

9 (x / y) * y = x. [assumption].

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

11 x' * (x * y) = y. [assumption].

13 ((x * A) * y) * A = x * (A * (y * A)). [assumption].

14 (A * c1) * (c2 * A) != A * ((c1 * c2) * A). [deny(1)].

18 x \ 0 = x'. [para(4(a,1),7(a,1,2))].

19 x'' = x. [para(5(a,1),7(a,1,2)),rewrite([18(3)])].

31 x * ((y / x) * (x * z)) = (x * y) * z. [para(9(a,1),10(a,1,1,2)),flip(a)].

51 (x / A) * (A * (y * A)) = (x * y) * A. [para(9(a,1),13(a,1,1,1)),flip(a)].

108 (x / y) * (y * z) = y' * ((y * x) * z). [para(31(a,1),11(a,1,2)),flip(a)].

117 A' * ((A * x) * (y * A)) = (x * y) * A. [back_rewrite(51),rewrite([108(7)])].

3583 (A * x) * (y * A) = A * ((x * y) * A). [para(117(a,1),11(a,1,2)),rewrite([19(3)]),flip(a)].

3584 $F. [resolve(3583,a,14,a)].

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