% Proof 1 at 11.61 (+ 0.06) seconds.

% Length of proof is 180.

% Level of proof is 33.

% Maximum clause weight is 23.000.

% Given clauses 732.

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

2 0 * x = x. [assumption].

3 x * 0 = x. [assumption].

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

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

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

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

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

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

10 (x * y) * (C * x) = x * ((y * C) * x). [copy(9),flip(a)].

11 C * x = x * C. [assumption].

12 (C * C) * (c1 * c2) != (C * c1) * (C * c2). [deny(1)].

13 (C * c1) * (C * c2) != (C * C) * (c1 * c2). [copy(12),flip(a)].

15 x \ x = 0. [para(3(a,1),5(a,1,2))].

16 x / x = 0. [para(2(a,1),6(a,1,1))].

19 (x / y) \ x = y. [para(7(a,1),5(a,1,2))].

20 (x * x) * y = x * (x * y). [para(2(a,1),8(a,1,1,2)),rewrite([2(5)])].

22 (x \ y) * (x * ((x \ y) * z)) = ((x \ y) * y) * z. [para(4(a,1),8(a,1,1,2)),flip(a)].

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

25 x * ((y / x) * (x * z)) = (x * y) * z. [para(7(a,1),8(a,1,1,2)),flip(a)].

28 (C * c1) * (C * c2) != C * (C * (c1 * c2)). [back_rewrite(13),rewrite([20(14)])].

29 x * ((C * (x \ y)) * x) = y * (C * x). [para(4(a,1),10(a,1,1)),rewrite([11(6,R)]),flip(a)].

30 (C \ x) * ((y * C) * (C \ x)) = ((C \ x) * y) * x. [para(4(a,1),10(a,1,2)),flip(a)].

31 (x * y) \ (x * ((y * C) * x)) = C * x. [para(10(a,1),5(a,1,2))].

33 (x / y) * ((y * C) * (x / y)) = x * (C * (x / y)). [para(7(a,1),10(a,1,1)),flip(a)].

41 C \ (x * C) = x. [para(11(a,1),5(a,1,2))].

44 (C * x) / C = x. [para(11(a,2),6(a,1,1))].

45 C * (x / C) = x. [para(11(a,2),7(a,1))].

46 (x * (x * C)) * y = x * (C * (x * y)). [para(11(a,1),8(a,1,1,2))].

50 C * (x * (y * x)) = x * (y * (C * x)). [para(11(a,2),8(a,2,2,2)),rewrite([11(4,R)])].

53 (C * x) * (C * x) = x * (C * (C * x)). [para(11(a,2),10(a,1,1)),rewrite([20(9)])].

56 C \ x = x / C. [para(7(a,1),41(a,1,2))].

57 (x / C) * ((y * C) * (x / C)) = ((x / C) * y) * x. [back_rewrite(30),rewrite([56(2),56(6),56(10)])].

60 x * (x * ((x * x) \ y)) = y. [para(20(a,1),4(a,1))].

62 (x * (x * y)) / y = x * x. [para(20(a,1),6(a,1,1))].

68 C * (x * x) = x * (x * C). [para(20(a,1),11(a,2))].

69 C * (C * x) = C * (x * C). [para(11(a,1),20(a,2,2)),rewrite([20(4)])].

70 C * (x * x) = x * (C * x). [para(11(a,2),20(a,2,2)),rewrite([11(3,R)])].

73 C * (x * C) = x * (C * C). [para(45(a,1),10(a,1,1)),rewrite([11(9,R),45(9)]),flip(a)].

74 x * ((x * x) \ y) = x \ y. [para(60(a,1),5(a,1,2)),flip(a)].

90 (x * y) / (x \ y) = x * x. [para(4(a,1),62(a,1,1,2))].

91 ((x / y) * x) / y = (x / y) * (x / y). [para(7(a,1),62(a,1,1,2))].

93 ((x * y) * (x * ((y * C) * x))) / (C * x) = (x * y) * (x * y). [para(10(a,1),62(a,1,1,2))].

101 C * ((x / C) * (x / C)) = (x / C) * x. [para(7(a,1),68(a,2,2))].

131 (((x \ y) * y) * z) / (x * ((x \ y) * z)) = x \ y. [para(22(a,1),6(a,1,1))].

140 (x / C) * (C * x) = C * ((x / C) * x). [para(69(a,2),22(a,1,2)),rewrite([56(2),56(6),45(7),56(7),11(10,R)])].

148 (C * (x * x)) * y = x * (C * (x * y)). [para(70(a,2),8(a,1,1))].

164 (x * (C * C)) / C = x * C. [para(73(a,1),5(a,1,2)),rewrite([56(6)])].

165 x \ (C * (x * C)) = C * C. [para(73(a,2),5(a,1,2))].

167 (C * (x * C)) / (C * C) = x. [para(73(a,2),6(a,1,1))].

185 (x * x) \ y = x \ (x \ y). [para(74(a,1),5(a,1,2)),flip(a)].

217 x / (x \ 0) = x * x. [para(3(a,1),90(a,1,1))].

229 (x * (C * C)) / x = C * C. [para(73(a,1),90(a,1,1)),rewrite([56(8),6(8)])].

233 (0 / x) * (0 / x) = (0 / x) / x. [para(19(a,1),217(a,1,2)),flip(a)].

238 x * ((y / (x * z)) * x) = (x * y) / z. [para(7(a,1),24(a,1,1,2)),flip(a)].

242 (C * (x * ((y * C) * x))) / x = C * (C * (x * y)). [para(10(a,1),24(a,1,1,2)),rewrite([11(11,R)])].

276 (x * y) * (x \ z) = x * ((y / x) * z). [para(4(a,1),25(a,1,2,2)),flip(a)].

277 x \ ((x * y) * z) = (y / x) * (x * z). [para(25(a,1),5(a,1,2))].

286 (C * x) * y = (x * C) * y. [para(11(a,1),25(a,2,1)),rewrite([25(7)])].

291 (C * x) * (y / C) = C * ((x / C) * y). [para(45(a,1),25(a,1,2,2)),flip(a)].

434 C * (x / (C * C)) = x / C. [para(7(a,1),164(a,1,1)),rewrite([11(8,R)]),flip(a)].

439 x \ (y * (C * x)) = (C * (x \ y)) * x. [para(29(a,1),5(a,1,2))].

445 x * (C * y) = x * (y * C). [para(11(a,1),29(a,2,2)),rewrite([29(5)])].

464 (x / C) \ (C * x) = C * C. [para(7(a,1),165(a,1,2,2))].

466 (C * (x \ C)) * x = C * C. [para(11(a,2),165(a,1,2,2)),rewrite([439(5)])].

472 (C * x) / (C * C) = x / C. [para(7(a,1),167(a,1,1,2))].

579 C * ((x / C) * x) = x * x. [para(11(a,1),33(a,1,2,1)),rewrite([20(8),45(7),140(5),45(9)])].

597 (x / C) * (C * x) = x * x. [back_rewrite(140),rewrite([579(10)])].

604 (x * C) * ((C * x) \ y) = y. [para(286(a,1),4(a,1))].

711 (x / C) / C = x / (C * C). [para(434(a,1),5(a,1,2)),rewrite([56(4)])].

720 (C * x) * (y / (C * C)) = C * ((x / C) * (y / C)). [para(434(a,1),25(a,1,2,2)),flip(a)].

731 (x * (C * y)) / (y * C) = x. [para(445(a,2),6(a,1,1))].

732 (x / (C * y)) * (y * C) = x. [para(445(a,1),7(a,1))].

761 (x / C) \ (x * C) = C * C. [para(11(a,1),464(a,1,2))].

768 (x / C) * (C * (C * x)) = (C * x) * x. [para(464(a,1),29(a,1,2,1,2)),rewrite([46(10),45(8),45(13)])].

816 (C * (x \ C)) \ (C * C) = x. [para(466(a,1),5(a,1,2))].

817 (C * C) / x = C * (x \ C). [para(466(a,1),6(a,1,1))].

822 (x \ C) * (C * (C * (x \ C))) = C * (((C * (x \ C)) \ x) \ C). [para(466(a,1),90(a,1,1)),rewrite([817(9),53(18)]),flip(a)].

932 (x * x) / C = (x / C) * x. [para(579(a,1),5(a,1,2)),rewrite([56(3)])].

972 (C * x) * x = C * (x * x). [para(597(a,1),8(a,2,2)),rewrite([11(5,R),45(5)])].

991 (x / C) * (C * (C * x)) = C * (x * x). [back_rewrite(768),rewrite([972(10)])].

1000 (C * x) \ y = (x * C) \ y. [para(604(a,1),5(a,1,2)),flip(a)].

1407 x * ((y / (C * x)) * x) = (x * y) / C. [para(732(a,1),24(a,1,1,2)),flip(a)].

1488 (x * C) * x = C * (x * x). [para(761(a,1),29(a,1,2,1,2)),rewrite([46(10),45(8),991(7),45(9)]),flip(a)].

1492 (C * x) \ (C * C) = C / x. [para(19(a,1),816(a,1,1,2))].

1790 (x / C) * x = x * (x / C). [para(4(a,1),972(a,1,1)),rewrite([56(2),56(6),56(8),101(10)]),flip(a)].

1870 (x * x) / C = x * (x / C). [back_rewrite(932),rewrite([1790(6)])].

2009 (C * (x \ 0)) * (x * x) = C * x. [para(1488(a,1),31(a,1,2,2)),rewrite([439(6),185(3),15(2)])].

2013 x \ (C * C) = C / (x / C). [para(4(a,1),1492(a,1,1)),rewrite([56(7)])].

3324 (C * (x \ 0)) \ (C * x) = x * x. [para(2009(a,1),5(a,1,2))].

3693 (C * ((x / C) \ 0)) \ x = (x / C) * (x / C). [para(4(a,1),3324(a,1,2)),rewrite([56(3),56(9),56(11)])].

5587 x \ ((x * y) / z) = (y / (x * z)) * x. [para(238(a,1),5(a,1,2))].

5597 ((C * x) / y) / C = C * (x / (C * y)). [para(238(a,1),44(a,1,1)),rewrite([11(10,R)])].

5598 (C * x) / (y / C) = C * (C * (x / y)). [para(45(a,1),238(a,1,2,1,2)),rewrite([11(4,R)]),flip(a)].

5621 (x \ C) * (C * x) = C * C. [para(229(a,1),238(a,2)),rewrite([817(5),185(4),29(7)])].

5724 ((x / C) \ C) * x = C * C. [para(4(a,1),5621(a,1,2)),rewrite([56(2)])].

5725 C / ((x \ C) / C) = C * x. [para(5621(a,1),5(a,1,2)),rewrite([2013(6)])].

5752 C * ((x * C) \ C) = x \ C. [para(5621(a,1),731(a,1,1)),rewrite([817(6)])].

5773 (x / C) \ C = C * (x \ C). [para(5724(a,1),6(a,1,1)),rewrite([817(4)]),flip(a)].

5868 C * ((x / C) * (x \ C)) = C. [para(5725(a,1),7(a,1,1)),rewrite([291(7)])].

5869 (C * x) \ C = (x \ C) / C. [para(5725(a,1),19(a,1,1))].

5959 (x * C) \ C = (x \ C) / C. [para(5752(a,1),5(a,1,2)),rewrite([56(4)]),flip(a)].

5960 C * ((x * (y * (x * C))) \ C) = (x * (y * x)) \ C. [para(8(a,1),5752(a,1,2,1))].

5964 (x * (C * x)) \ C = (x * (x * C)) \ C. [para(46(a,1),5752(a,1,2,1)),rewrite([5960(9)])].

5968 (((C * (x \ C)) \ x) \ C) / C = (x \ C) * (x \ C). [para(5752(a,1),93(a,1,1,1)),rewrite([5959(7),11(9,R),45(9),11(7,R),822(9),472(13),5

959(14),45(15),5959(16),45(17)])].

5970 (x * (C * x)) \ C = (x \ (x \ C)) / C. [para(148(a,1),5752(a,1,2,1)),rewrite([5960(9),5869(10),185(8)])].

5976 (x * (x * C)) \ C = (x \ (x \ C)) / C. [back_rewrite(5964),rewrite([5970(5)]),flip(a)].

6051 (x * (x / C)) \ C = C * (x \ (x \ C)). [para(185(a,1),5773(a,2,2)),rewrite([1870(3)])].

6057 (x / C) \ (C * (x \ C)) = C * (C * (x \ (x \ C))). [para(91(a,1),5773(a,1,1)),rewrite([185(7),5773(6),1790(11),6051(13)])].

6093 (x / C) * (x \ C) = 0. [para(5868(a,1),5(a,1,2)),rewrite([15(3)]),flip(a)].

6095 x * (C * ((x / C) / x)) = x. [para(5868(a,1),8(a,2,2)),rewrite([45(6),1790(3),276(6),11(5,R),11(10,R),45(10)])].

6104 (x / C) \ 0 = x \ C. [para(6093(a,1),5(a,1,2))].

6105 0 / (x \ C) = x / C. [para(6093(a,1),6(a,1,1))].

6123 (C * (x \ C)) \ x = (x / C) * (x / C). [back_rewrite(3693),rewrite([6104(5)])].

6130 (x \ C) * (x \ C) = C * (x \ (x \ C)). [back_rewrite(5968),rewrite([6123(5),185(7),5773(6),6057(7),44(9)]),flip(a)].

6138 (x \ C) / C = x \ 0. [para(6(a,1),6104(a,1,1)),rewrite([5959(6)]),flip(a)].

6139 (x \ (x \ C)) / C = x \ (x \ 0). [para(62(a,1),6104(a,1,1)),rewrite([185(3),5976(8)]),flip(a)].

6153 (x * C) \ C = x \ 0. [back_rewrite(5959),rewrite([6138(8)])].

6228 (C / x) / C = 0 / x. [para(19(a,1),6105(a,1,2)),flip(a)].

6231 C * (x \ 0) = x \ C. [para(6138(a,1),7(a,1,1)),rewrite([11(4,R)])].

6235 C * ((x \ 0) * (C * y)) = (C * (x \ C)) * y. [para(6138(a,1),25(a,1,2,1))].

6242 (C * x) \ 0 = (x \ 0) / C. [para(1000(a,1),6138(a,1,1)),rewrite([6153(4)]),flip(a)].

6243 (x \ 0) * (x \ C) = (x \ C) * (x \ 0). [para(6138(a,1),1790(a,1,1)),rewrite([6138(11)])].

6246 (x \ C) * (x \ 0) = x \ (x \ C). [para(6138(a,1),1870(a,2,2)),rewrite([6130(5),44(7)]),flip(a)].

6250 (x \ 0) * (x \ 0) = x \ (x \ 0). [para(6138(a,1),91(a,1,1,1)),rewrite([6243(5),6246(5),6139(5),6138(7),6138(9)]),flip(a)].

6254 (x \ 0) \ 0 = (x \ C) \ C. [para(6138(a,1),6104(a,1,1))].

6358 x * (C / x) = C. [para(6153(a,1),4(a,1,2)),rewrite([276(5),3(4)])].

6387 x \ C = C / x. [para(6358(a,1),5(a,1,2))].

6388 C / (C / x) = x. [para(6358(a,1),6(a,1,1))].

6470 (x \ 0) \ 0 = x. [back_rewrite(6254),rewrite([6387(6),6387(8),6388(8)])].

6482 C * ((x \ 0) * (C * y)) = (C * (C / x)) * y. [back_rewrite(6235),rewrite([6387(10)])].

6485 C * (x \ 0) = C / x. [back_rewrite(6231),rewrite([6387(6)])].

6514 (x \ (C / x)) / C = x \ (x \ 0). [back_rewrite(6139),rewrite([6387(2)])].

6515 x \ 0 = 0 / x. [back_rewrite(6138),rewrite([6387(2),6228(4)]),flip(a)].

6639 (C * C) / x = C * (C / x). [back_rewrite(817),rewrite([6387(7)])].

6672 (x \ (C / x)) / C = x \ (0 / x). [back_rewrite(6514),rewrite([6515(7)])].

6682 C * (0 / x) = C / x. [back_rewrite(6485),rewrite([6515(3)])].

6685 C * ((0 / x) * (C * y)) = (C * (C / x)) * y. [back_rewrite(6482),rewrite([6515(3)])].

6696 0 / (0 / x) = x. [back_rewrite(6470),rewrite([6515(2),6515(4)])].

6770 x \ (0 / x) = (0 / x) / x. [back_rewrite(6250),rewrite([6515(2),6515(4),233(5),6515(5)]),flip(a)].

6771 (0 / x) / C = 0 / (C * x). [back_rewrite(6242),rewrite([6515(4),6515(6)]),flip(a)].

6800 x / (0 / x) = x * x. [back_rewrite(217),rewrite([6515(2)])].

6872 (x \ (C / x)) / C = (0 / x) / x. [back_rewrite(6672),rewrite([6770(8)])].

6991 x \ (C / x) = C / (x * x). [para(6387(a,1),185(a,1)),rewrite([6387(5)]),flip(a)].

6999 (0 / x) / x = 0 / (x * x). [back_rewrite(6872),rewrite([6991(3),6228(5)]),flip(a)].

7117 (0 / x) * (0 / x) = 0 / (x * x). [back_rewrite(233),rewrite([6999(8)])].

7122 x * (0 / x) = 0. [para(6515(a,1),4(a,1,2))].

7289 (x * y) / (0 / x) = x * (y * x). [para(7122(a,1),24(a,1,1,2,2)),rewrite([3(2)])].

7563 C * (C * (x / (C / y))) = (C * x) / (0 / y). [para(6682(a,1),238(a,1,2,1,2)),rewrite([11(6,R)])].

7843 C * ((x / C) / x) = 0. [para(6095(a,1),5(a,1,2)),rewrite([15(1)]),flip(a)].

7866 (x / C) / x = 0 / C. [para(7843(a,1),5(a,1,2)),rewrite([6515(3)]),flip(a)].

7871 (0 / C) * x = x / C. [para(7843(a,1),33(a,2,2)),rewrite([7866(3),7866(8),57(10),3(6),3(8)])].

7873 x * (0 / C) = x / C. [para(7843(a,1),50(a,2,2,2)),rewrite([7866(4),7866(7),7871(9),45(8),7866(7),3(9),7871(8)])].

8176 (x * (y / C)) / C = (x / (C * C)) * y. [para(7871(a,1),8(a,1,1)),rewrite([7873(4),711(4),7871(12),7871(12)]),flip(a)].

9177 (0 / (x * x)) \ (0 / x) = x. [para(6999(a,1),19(a,1,1))].

10898 x / ((0 / (y * y)) * (y * x)) = y. [para(9177(a,1),131(a,1,1,1,1)),rewrite([7122(3),2(2),9177(9),9177(12)])].

11964 (C * (x * (y * x))) / x = C * (C * (x * (y / C))). [para(7(a,1),242(a,1,1,2,2,1))].

11967 (C * (x * ((C * y) * x))) / x = C * (C * (x * y)). [para(11(a,2),242(a,1,1,2,2,1))].

13639 x * ((x \ y) * x) = y / (0 / x). [para(4(a,1),7289(a,1,1)),flip(a)].

15780 (0 / (x * x)) * (x * y) = x \ y. [para(10898(a,1),19(a,1,1)),flip(a)].

15855 x / (y * (y * ((0 / y) * x))) = 0 / y. [para(7117(a,1),10898(a,1,2,1,2)),rewrite([6696(5),20(5)])].

16122 (0 / x) * (x * y) = y. [para(6696(a,1),276(a,2,2,1)),rewrite([3(4),4(6)]),flip(a)].

16133 (0 / x) \ y = x * y. [para(6800(a,1),276(a,2,2,1)),rewrite([7(3),2(5),20(7),16122(8)])].

16202 (0 / x) * y = x \ y. [para(7117(a,1),276(a,1,1)),rewrite([16133(6),15780(5),16(8),2(5)]),flip(a)].

16244 x / (y * x) = 0 / y. [back_rewrite(15855),rewrite([16202(3),4(2)])].

16836 (C * (C / x)) * y = C * (x \ (C * y)). [back_rewrite(6685),rewrite([16202(6)]),flip(a)].

17380 0 / (x / y) = y / x. [para(7(a,1),16244(a,1,2)),flip(a)].

17552 (x / (y * C)) * y = (x / y) * (y / C). [para(7873(a,1),277(a,1,2)),rewrite([5587(4),7873(9)])].

17990 (x / y) \ z = (y / x) * z. [para(17380(a,1),16133(a,1,1))].

26994 (x / (C * y)) * y = (x / y) * (y / C). [para(1407(a,1),5(a,1,2)),rewrite([5587(4),17552(4)]),flip(a)].

27042 x * ((x \ y) * (x / C)) = (y / (0 / x)) / C. [para(13639(a,1),1407(a,2,1)),rewrite([26994(6),6(3)])].

30199 (C * x) / (0 / (C * y)) = C * (C * (x / (0 / y))). [para(6771(a,1),5598(a,1,2))].

31639 x / (C / y) = x * (y / C). [para(29(a,1),8176(a,2)),rewrite([17990(6),6639(5),16836(6),720(12),44(8),44(10),27042(7),5597(7),6682(5),4

4(7),434(9)])].

31727 C * (C * (x * (y / C))) = (C * x) / (0 / y). [back_rewrite(7563),rewrite([31639(5)])].

31750 (C * (x * (y * x))) / x = (C * x) / (0 / y). [back_rewrite(11964),rewrite([31727(12)])].

31759 C * (C * (x / (0 / y))) = C * (C * (x * y)). [back_rewrite(11967),rewrite([31750(7),30199(7)])].

31769 (C * x) / (0 / (C * y)) = C * (C * (x * y)). [back_rewrite(30199),rewrite([31759(14)])].

31794 x / (0 / y) = x * y. [para(6(a,1),31639(a,2,2)),rewrite([16244(4)])].

31843 (C * x) * (C * y) = C * (C * (x * y)). [back_rewrite(31769),rewrite([31794(7)])].

31844 $F. [resolve(31843,a,28,a)].

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

% Proof 1 at 0.16 (+ 0.00) seconds.

% Length of proof is 47.

% Level of proof is 12.

% Maximum clause weight is 23.000.

% Given clauses 110.

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

2 0 * x = x. [assumption].

3 x * 0 = x. [assumption].

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

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

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

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

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

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

10 (x * y) * (C * x) = x * ((y * C) * x). [copy(9),flip(a)].

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

12 (c1 * C) * (c1 * c2) != (c1 * c1) * (C * c2). [deny(1)].

13 (c1 * c1) * (C * c2) != (c1 * C) * (c1 * c2). [copy(12),flip(a)].

20 (x * x) * y = x * (x * y). [para(2(a,1),8(a,1,1,2)),rewrite([2(5)])].

22 (x \ y) * (x * ((x \ y) * z)) = ((x \ y) * y) * z. [para(4(a,1),8(a,1,1,2)),flip(a)].

25 x * ((y / x) * (x * z)) = (x * y) * z. [para(7(a,1),8(a,1,1,2)),flip(a)].

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

28 (c1 * C) * (c1 * c2) != c1 * (c1 * (C * c2)). [back_rewrite(13),rewrite([20(7)]),flip(a)].

29 (C * x) * (C * y) = C * (C * (x * y)). [back_rewrite(11),rewrite([20(5)]),flip(a)].

34 (x / y) * ((y * C) * (x / y)) = x * (C * (x / y)). [para(7(a,1),10(a,1,1)),flip(a)].

41 (x * (x * y)) / y = x * x. [para(20(a,1),6(a,1,1))].

54 (x * y) / (x \ y) = x * x. [para(4(a,1),41(a,1,1,2))].

71 x / (x \ 0) = x * x. [para(3(a,1),54(a,1,1))].

144 (C * x) * C = C * (C * x). [para(3(a,1),29(a,1,2)),rewrite([3(8)])].

145 C * (C * ((C \ x) * y)) = x * (C * y). [para(4(a,1),29(a,1,1)),flip(a)].

146 C * (C * (x * (C \ y))) = (C * x) * y. [para(4(a,1),29(a,1,2)),flip(a)].

168 C * x = x * C. [para(4(a,1),144(a,1,1)),rewrite([4(7)]),flip(a)].

184 (C * c1) * (c1 * c2) != c1 * (c1 * (C * c2)). [back_rewrite(28),rewrite([168(3,R)])].

223 C \ (x * C) = x. [para(168(a,1),5(a,1,2))].

227 C * (x / C) = x. [para(168(a,2),7(a,1))].

237 C * (C * x) = C * (x * C). [para(168(a,1),20(a,2,2)),rewrite([20(4)])].

238 C * (x * x) = x * (x * C). [para(168(a,2),20(a,1))].

263 C \ x = x / C. [para(7(a,1),223(a,1,2))].

265 C * (C * (x * (y / C))) = (C * x) * y. [back_rewrite(146),rewrite([263(4)])].

266 C * (C * ((x / C) * y)) = x * (C * y). [back_rewrite(145),rewrite([263(4)])].

300 C / (0 / C) = C * C. [para(263(a,1),71(a,1,2))].

313 (0 / C) * (C * x) = x. [para(300(a,1),25(a,1,2,1)),rewrite([20(11),266(11),2(7),168(11,R),227(11),2(8)])].

314 (0 / C) * x = x / C. [para(4(a,1),313(a,1,2)),rewrite([263(6)])].

324 (x * (x / C)) * y = x * ((x * y) / C). [para(313(a,1),26(a,1,1,2)),rewrite([314(4),314(13),227(12),314(9)])].

346 (x / C) * (C * x) = x * x. [para(20(a,1),34(a,1,2)),rewrite([227(7),227(9)])].

375 C * ((x / C) * x) = x * x. [para(237(a,2),22(a,1,2)),rewrite([263(2),263(6),227(7),346(5),263(3),168(6,R)]),flip(a)].

433 C * ((x / C) * (x / C)) = (x / C) * x. [para(7(a,1),238(a,2,2))].

917 (C * x) * x = C * (x * x). [para(346(a,1),8(a,2,2)),rewrite([168(5,R),227(5)])].

1006 C * (C * (((x / C) * x) * y)) = x * (x * (C * y)). [para(375(a,1),29(a,1,1)),rewrite([20(4)]),flip(a)].

1534 (x / C) * x = x * (x / C). [para(4(a,1),917(a,1,1)),rewrite([263(2),263(6),263(8),433(10)]),flip(a)].

1587 (C * x) * (x * y) = x * (x * (C * y)). [back_rewrite(1006),rewrite([1534(5),324(6),265(8)])].

1588 $F. [resolve(1587,a,184,a)].

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

% Proof 1 at 0.01 (+ 0.00) seconds.

% Length of proof is 21.

% Level of proof is 6.

% Maximum clause weight is 15.000.

% Given clauses 42.

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

2 0 * x = x. [assumption].

3 x * 0 = x. [assumption].

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

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

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

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

10 (x * y) * (C * x) = x * ((y * C) * x). [copy(9),flip(a)].

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

12 (x * C) * (x * y) = (x * x) * (C * y). [copy(11),flip(a)].

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

14 c1 * C != C * c1. [copy(13),flip(a)].

21 (x * x) * y = x * (x * y). [para(2(a,1),8(a,1,1,2)),rewrite([2(5)])].

29 (x * C) * (x * y) = x * (x * (C * y)). [back_rewrite(12),rewrite([21(8)])].

32 (x * y) \ (x * ((y * C) * x)) = C * x. [para(10(a,1),5(a,1,2))].

39 x * (x * ((x * x) \ y)) = y. [para(21(a,1),4(a,1))].

46 x * ((x * x) \ y) = x \ y. [para(39(a,1),5(a,1,2)),flip(a)].

67 (x * x) \ y = x \ (x \ y). [para(46(a,1),5(a,1,2)),flip(a)].

146 (x * C) * x = x * (x * C). [para(3(a,1),29(a,1,2)),rewrite([3(6)])].

274 C * x = x * C. [para(32(a,1),67(a,1)),rewrite([146(5),5(7),5(6)])].

275 $F. [resolve(274,a,14,a(flip))].

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

% Proof 1 at 0.00 (+ 0.00) seconds.

% Length of proof is 10.

% Level of proof is 3.

% Maximum clause weight is 15.000.

% Given clauses 7.

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

2 0 * x = x. [assumption].

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

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

10 (x * y) * (A * x) = x * ((y * A) * x). [copy(9),flip(a)].

11 C * x = x * C. [assumption].

12 (C * C) * (c1 * A) != (C * c1) * (C * A). [deny(1)].

13 (C * C) * (c1 * A) != C * (C * (c1 * A)). [copy(12),rewrite([11(13),10(14),11(13,R)])].

20 (x * x) * y = x * (x * y). [para(2(a,1),8(a,1,1,2)),rewrite([2(5)])].

21 $F. [resolve(20,a,13,a)].

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

% Proof 1 at 4.56 (+ 0.03) seconds.

% Length of proof is 115.

% Level of proof is 23.

% Maximum clause weight is 23.000.

% Given clauses 440.

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

2 0 * x = x. [assumption].

3 x * 0 = x. [assumption].

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

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

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

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

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

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

10 (x * y) * (A * x) = x * ((y * A) * x). [copy(9),flip(a)].

11 (C * C) * (x * A) = (C * x) * (C * A). [assumption].

12 (c1 * C) * (c1 * A) != (c1 * c1) * (C * A). [deny(1)].

13 (c1 * c1) * (C * A) != (c1 * C) * (c1 * A). [copy(12),flip(a)].

17 x / 0 = x. [para(3(a,1),6(a,1,1))].

18 x / (y \ x) = y. [para(4(a,1),6(a,1,1))].

19 (x / y) \ x = y. [para(7(a,1),5(a,1,2))].

20 (x * x) * y = x * (x * y). [para(2(a,1),8(a,1,1,2)),rewrite([2(5)])].

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

25 x * ((y / x) * (x * z)) = (x * y) * z. [para(7(a,1),8(a,1,1,2)),flip(a)].

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

28 (c1 * C) * (c1 * A) != c1 * (c1 * (C * A)). [back_rewrite(13),rewrite([20(7)]),flip(a)].

29 (C * x) * (C * A) = C * (C * (x * A)). [back_rewrite(11),rewrite([20(6)]),flip(a)].

30 x * (((x \ y) * A) * x) = y * (A * x). [para(4(a,1),10(a,1,1)),flip(a)].

34 (x / y) * ((y * A) * (x / y)) = x * (A * (x / y)). [para(7(a,1),10(a,1,1)),flip(a)].

39 x * (x * ((x * x) \ y)) = y. [para(20(a,1),4(a,1))].

41 (x * (x * y)) / y = x * x. [para(20(a,1),6(a,1,1))].

45 x * ((x * A) * x) = x * (x * (A * x)). [para(20(a,1),10(a,1)),flip(a)].

46 x * ((x * x) \ y) = x \ y. [para(39(a,1),5(a,1,2)),flip(a)].

66 (x * x) \ y = x \ (x \ y). [para(46(a,1),5(a,1,2)),flip(a)].

70 x / (y \ (y \ x)) = y * y. [para(46(a,1),41(a,1,1,2)),rewrite([4(2),66(2)])].

115 x * ((y / (x * z)) * x) = (x * y) / z. [para(7(a,1),24(a,1,1,2)),flip(a)].

125 (x * y) * (x \ z) = x * ((y / x) * z). [para(4(a,1),25(a,1,2,2)),flip(a)].

144 C * (C * ((C \ x) * A)) = x * (C * A). [para(4(a,1),29(a,1,1)),flip(a)].

161 x * (((x \ y) * A) * (x * z)) = (y * (A * x)) * z. [para(30(a,1),8(a,1,1)),flip(a)].

232 (x * A) * x = x * (A * x). [para(45(a,1),5(a,1,2)),rewrite([5(5)]),flip(a)].

245 (x * A) \ (x * (A * x)) = x. [para(232(a,1),5(a,1,2))].

445 x * ((0 / x) * y) = y. [para(3(a,1),125(a,1,1)),rewrite([4(2)]),flip(a)].

473 x * (0 / x) = 0. [para(3(a,1),445(a,1,2))].

474 (0 / x) \ y = x * y. [para(4(a,1),445(a,1,2)),flip(a)].

475 (0 / x) * y = x \ y. [para(445(a,1),5(a,1,2)),flip(a)].

478 (x \ y) / y = 0 / x. [para(445(a,1),24(a,1,1,2)),rewrite([475(3),473(7),3(6)])].

481 (x * (y \ x)) * z = x * (y \ (x * z)). [para(445(a,1),26(a,1,1,2,2)),rewrite([475(3),475(9),4(8),475(7)])].

508 x \ 0 = 0 / x. [para(473(a,1),5(a,1,2))].

511 x * ((x \ A) * x) = A * x. [para(473(a,1),10(a,1,1)),rewrite([2(4),475(6)]),flip(a)].

515 x / (0 / x) = x * x. [para(473(a,1),41(a,1,1,2)),rewrite([3(2)])].

517 (x * y) / (0 / x) = x * (y * x). [para(473(a,1),24(a,1,1,2,2)),rewrite([3(2)])].

518 (x * y) * (0 / x) = x * (y / x). [para(473(a,1),25(a,1,2,2)),rewrite([3(3)]),flip(a)].

559 x / (y * x) = 0 / y. [para(474(a,1),18(a,1,2))].

562 (x \ (y * (0 / x))) * z = x \ (y * (x \ z)). [para(475(a,1),8(a,1,1)),rewrite([475(10),475(10)])].

574 A * (0 / x) = A / x. [para(475(a,1),34(a,1)),rewrite([518(5),5(4),2(8)]),flip(a)].

575 x * ((x * y) \ x) = x / y. [para(475(a,1),115(a,1,2)),rewrite([3(5)])].

583 0 / (x / y) = y / x. [para(19(a,1),478(a,1,1)),flip(a)].

585 x / (x * (A * x)) = 0 / (x * A). [para(245(a,1),478(a,1,1))].

643 A \ (A / x) = 0 / x. [para(574(a,1),5(a,1,2))].

669 (x / y) \ z = (y / x) * z. [para(583(a,1),474(a,1,1))].

730 0 / (x \ A) = A \ x. [para(18(a,1),643(a,1,2)),flip(a)].

740 (A \ x) * (x \ A) = 0. [para(730(a,1),7(a,1,1))].

743 (x \ A) * ((A \ x) * y) = y. [para(730(a,1),125(a,2,2,1)),rewrite([3(4),4(6)]),flip(a)].

745 (x \ A) \ y = (A \ x) * y. [para(730(a,1),475(a,1,1)),flip(a)].

746 (x \ A) / (A \ x) = (x \ A) * (x \ A). [para(730(a,1),515(a,1,2))].

747 0 / (A \ x) = x \ A. [para(730(a,1),583(a,1,2)),rewrite([17(8)])].

785 (A \ x) * ((x \ A) * y) = y. [para(740(a,1),25(a,2,1)),rewrite([746(7),20(11),743(10),2(8)])].

786 (A \ x) \ y = (x \ A) * y. [para(740(a,1),125(a,1,1)),rewrite([2(5),746(10),20(11),785(12)])].

798 (A * x) \ A = 0 / x. [para(5(a,1),747(a,1,2)),flip(a)].

807 (0 / x) / A = 0 / (A * x). [para(798(a,1),478(a,1,1))].

869 (A * x) / ((x \ A) * x) = x. [para(511(a,1),6(a,1,1))].

965 x / (x \ y) = x * (y \ x). [para(4(a,1),575(a,1,2,1)),flip(a)].

966 (x * y) \ x = x \ (x / y). [para(575(a,1),5(a,1,2)),flip(a)].

1290 (x \ y) \ (0 / x) = x * ((0 / x) / y). [para(475(a,1),966(a,1,1)),rewrite([669(10),17(6)])].

1401 x * ((x \ y) * x) = y / (0 / x). [para(4(a,1),517(a,1,1)),flip(a)].

1405 x \ (y * (0 / x)) = (x \ y) / x. [para(18(a,1),517(a,1,2)),rewrite([508(2),475(3),508(4),508(6),475(8)]),flip(a)].

1443 x \ (y * (x \ z)) = ((x \ y) / x) * z. [back_rewrite(562),rewrite([1405(4)]),flip(a)].

2141 x * ((x \ y) / x) = y * (0 / x). [para(4(a,1),518(a,1,1)),flip(a)].

2156 (x * (A * y)) * (0 / y) = y * ((y \ x) * A). [para(30(a,1),518(a,1,1)),rewrite([6(11)])].

2318 (x \ (x / A)) * A = 0. [para(585(a,1),34(a,1,1)),rewrite([8(9),585(13),2156(14),966(9),475(13),5(11),585(10),574(11),559(9),473(8)])].

2326 x \ (x / A) = 0 / A. [para(2318(a,1),6(a,1,1)),flip(a)].

2352 x * (0 / A) = x / A. [para(2326(a,1),4(a,1,2))].

2359 x * (0 / (A * x)) = 0 / A. [para(478(a,1),2326(a,1,2)),rewrite([1290(5),807(4)])].

2362 (A \ x) * (0 / x) = 0 / A. [para(2326(a,1),745(a,1)),rewrite([478(9)]),flip(a)].

2366 x / (0 / A) = x * A. [para(2326(a,1),965(a,1,2)),rewrite([669(7),7(7)])].

2459 (A * x) / A = A * (x / A). [para(2352(a,1),518(a,1))].

2512 A \ (x * A) = (A \ x) * A. [para(2366(a,1),518(a,1,2)),rewrite([475(4),2(5),2366(11),475(10)]),flip(a)].

2629 (A \ C) * A = C. [para(2359(a,1),29(a,1,1)),rewrite([475(7),2512(5),475(14),966(12),643(12),473(11),3(8)])].

2653 (C \ A) * C = A. [para(2629(a,1),5(a,1,2)),rewrite([786(5)])].

2718 A * (C / A) = C. [para(2653(a,1),869(a,1,2)),rewrite([2459(5)])].

2758 C * A = A * C. [para(2718(a,1),517(a,1,1)),rewrite([2366(5),7(9)])].

2830 C * (C * ((C \ x) * A)) = x * (A * C). [back_rewrite(144),rewrite([2758(11)])].

2832 (c1 * C) * (c1 * A) != c1 * (c1 * (A * C)). [back_rewrite(28),rewrite([2758(12)])].

5652 (x * y) * (0 / y) = x. [para(2362(a,1),161(a,1,2,2)),rewrite([786(5),2352(11),6(9),785(6),4(4)]),flip(a)].

5722 x \ (x / y) = 0 / y. [para(5652(a,1),5(a,1,2)),rewrite([966(2)])].

5723 x / (0 / y) = x * y. [para(5652(a,1),6(a,1,1))].

5724 x * (0 / y) = x / y. [para(7(a,1),5652(a,1,1))].

5879 x * ((x \ y) * x) = y * x. [back_rewrite(1401),rewrite([5723(6)])].

5970 x * ((x \ y) / x) = y / x. [back_rewrite(2141),rewrite([5724(6)])].

6481 0 / (x \ y) = y \ x. [para(18(a,1),5722(a,1,2)),flip(a)].

6483 (x \ y) \ x = y \ (x * x). [para(70(a,1),5722(a,1,2)),rewrite([6481(6)]),flip(a)].

6487 x \ (0 / y) = 0 / (y * x). [para(559(a,1),5722(a,1,2))].

6576 x * ((y / (x / z)) * x) = (x * y) * z. [para(5723(a,1),115(a,2)),rewrite([5724(3)])].

6578 x / (y / z) = x * (z / y). [para(583(a,1),5723(a,1,2))].

6591 x * ((y * (z / x)) * x) = (x * y) * z. [back_rewrite(6576),rewrite([6578(2)])].

7587 (x \ y) \ z = (y \ x) * z. [para(6481(a,1),475(a,1,1)),flip(a)].

7614 x \ (y * y) = (x \ y) * y. [back_rewrite(6483),rewrite([7587(2)]),flip(a)].

8294 (x / y) * x = x * (y \ x). [para(5722(a,1),5879(a,1,2,1)),rewrite([475(3)]),flip(a)].

14340 x \ (y / (z * x)) = ((x \ y) / x) / z. [para(5724(a,1),1443(a,2)),rewrite([6487(3),5724(4)])].

14839 C * (x / C) = x. [para(7(a,1),2830(a,2)),rewrite([14340(8),7(10),5970(7)])].

14842 C * (C * (((C \ x) * x) * A)) = x * (x * (A * C)). [para(20(a,1),2830(a,2)),rewrite([7614(5)])].

14924 C \ x = x / C. [para(14839(a,1),5(a,1,2))].

14926 C * x = x * C. [para(6(a,1),14839(a,1,2))].

15017 C * (C * ((x * (x / C)) * A)) = x * (x * (A * C)). [back_rewrite(14842),rewrite([14924(4),8294(5),14924(4)])].

15155 (C * c1) * (c1 * A) != c1 * (c1 * (A * C)). [back_rewrite(2832),rewrite([14926(3,R)])].

15259 (x * (x / C)) * y = x * ((x * y) / C). [para(14924(a,1),481(a,1,1,2)),rewrite([14924(7)])].

15274 C * (C * (x * ((x * A) / C))) = x * (x * (A * C)). [back_rewrite(15017),rewrite([15259(7)])].

25932 C * (C * (x * (y / C))) = (C * x) * y. [para(6591(a,1),14926(a,1)),rewrite([14926(8,R),14926(10,R)]),flip(a)].

26316 (C * x) * (x * A) = x * (x * (A * C)). [back_rewrite(15274),rewrite([25932(9)])].

26317 $F. [resolve(26316,a,15155,a)].

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

% Proof 1 at 31.58 (+ 0.16) seconds.

% Length of proof is 418.

% Level of proof is 37.

% Maximum clause weight is 39.000.

% Given clauses 1018.

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

2 0 * x = x. [assumption].

3 x * 0 = x. [assumption].

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

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

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

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

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

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

10 (x * y) * (A * x) = x * ((y * A) * x). [copy(9),flip(a)].

11 (x * x) * (C * A) = (x * C) * (x * A). [assumption].

12 (x * C) * (x * A) = (x * x) * (C * A). [copy(11),flip(a)].

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

14 c1 * C != C * c1. [copy(13),flip(a)].

16 x \ x = 0. [para(3(a,1),5(a,1,2))].

17 x / x = 0. [para(2(a,1),6(a,1,1))].

18 x / 0 = x. [para(3(a,1),6(a,1,1))].

19 x / (y \ x) = y. [para(4(a,1),6(a,1,1))].

20 (x / y) \ x = y. [para(7(a,1),5(a,1,2))].

21 (x * x) * y = x * (x * y). [para(2(a,1),8(a,1,1,2)),rewrite([2(5)])].

22 x * (y * (x * ((x * (y * x)) \ z))) = z. [para(8(a,1),4(a,1))].

23 (x \ y) * (x * ((x \ y) * z)) = ((x \ y) * y) * z. [para(4(a,1),8(a,1,1,2)),flip(a)].

24 (x * (y * x)) \ (x * (y * (x * z))) = z. [para(8(a,1),5(a,1,2))].

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

26 x * ((y / x) * (x * z)) = (x * y) * z. [para(7(a,1),8(a,1,1,2)),flip(a)].

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

29 (x * C) * (x * A) = x * (x * (C * A)). [back_rewrite(12),rewrite([21(10)])].

30 x * (((x \ y) * A) * x) = y * (A * x). [para(4(a,1),10(a,1,1)),flip(a)].

31 (A \ x) * ((y * A) * (A \ x)) = ((A \ x) * y) * x. [para(4(a,1),10(a,1,2)),flip(a)].

34 (x / y) * ((y * A) * (x / y)) = x * (A * (x / y)). [para(7(a,1),10(a,1,1)),flip(a)].

39 x * (x * ((x * x) \ y)) = y. [para(21(a,1),4(a,1))].

41 (x * (x * y)) / y = x * x. [para(21(a,1),6(a,1,1))].

45 x * ((x * A) * x) = x * (x * (A * x)). [para(21(a,1),10(a,1)),flip(a)].

46 x * ((x * x) \ y) = x \ y. [para(39(a,1),5(a,1,2)),flip(a)].

54 (x * y) / (x \ y) = x * x. [para(4(a,1),41(a,1,1,2))].

55 ((x / y) * x) / y = (x / y) * (x / y). [para(7(a,1),41(a,1,1,2))].

60 x * (y * ((y * (x * y)) \ z)) = y \ z. [para(22(a,1),5(a,1,2)),flip(a)].

66 (x * x) \ y = x \ (x \ y). [para(46(a,1),5(a,1,2)),flip(a)].

70 x / (y \ (y \ x)) = y * y. [para(46(a,1),41(a,1,1,2)),rewrite([4(2),66(2)])].

71 x / (x \ 0) = x * x. [para(3(a,1),54(a,1,1))].

72 x / ((x / y) \ y) = (x / y) * (x / y). [para(7(a,1),54(a,1,1))].

78 (0 / x) * (0 / x) = (0 / x) / x. [para(20(a,1),71(a,1,2)),flip(a)].

86 (x * ((x \ y) * z)) * ((x \ y) * ((x * ((x \ y) * z)) * u)) = ((x * ((x \ y) * z)) * (((x \ y) * y) * z)) * u. [para(23(a,1),8(a,1,1,2)),

flip(a)].

87 ((x * (y * x)) \ z) * (x * (y * (x * (((x * (y * x)) \ z) * u)))) = (((x * (y * x)) \ z) * z) * u. [para(8(a,1),23(a,1,2))].

104 (x * (y * x)) \ (x * (y * z)) = x \ z. [para(4(a,1),24(a,1,2,2,2))].

113 (x * (y * z)) / (x \ z) = x * (y * x). [para(4(a,1),25(a,1,1,2,2))].

114 ((x / y) * (z * x)) / y = (x / y) * (z * (x / y)). [para(7(a,1),25(a,1,1,2,2))].

115 x * ((y / (x * z)) * x) = (x * y) / z. [para(7(a,1),25(a,1,1,2)),flip(a)].

117 (x * (y * (z * (y * (x * u))))) / u = x * (y * (z * (y * x))). [para(8(a,1),25(a,1,1,2)),rewrite([8(9)])].

118 ((x * y) * (z * (x * ((y * A) * x)))) / (A * x) = (x * y) * (z * (x * y)). [para(10(a,1),25(a,1,1,2,2))].

125 (x * y) * (x \ z) = x * ((y / x) * z). [para(4(a,1),26(a,1,2,2)),flip(a)].

126 x \ ((x * y) * z) = (y / x) * (x * z). [para(26(a,1),5(a,1,2))].

128 (x / y) * ((z / (x / y)) * x) = ((x / y) * z) * y. [para(7(a,1),26(a,1,2,2))].

133 (x * y) * ((z / (x * y)) * (x * ((y * A) * x))) = ((x * y) * z) * (A * x). [para(10(a,1),26(a,1,2,2))].

143 (x * y) * ((z / x) * (x * u)) = x * ((y / x) * ((x * z) * u)). [para(26(a,1),26(a,1,2,2)),flip(a)].

145 (x * (x * (C * A))) / (x * A) = x * C. [para(29(a,1),6(a,1,1))].

161 x * (((x \ y) * A) * (x * z)) = (y * (A * x)) * z. [para(30(a,1),8(a,1,1)),flip(a)].

229 (x * A) * x = x * (A * x). [para(45(a,1),5(a,1,2)),rewrite([5(5)]),flip(a)].

239 (x * A) \ (x * (A * x)) = x. [para(229(a,1),5(a,1,2))].

241 (x / A) * (A * (x / A)) = x * (x / A). [para(7(a,1),229(a,1,1)),flip(a)].

293 (x / y) * (y * ((y * x) \ z)) = y \ z. [para(7(a,1),60(a,1,2,2,1,2))].

339 (x * (y * x)) \ (x * z) = x \ (y \ z). [para(4(a,1),104(a,1,2,2))].

343 (x * (y * (x * (z * (x * (y * x)))))) \ (x * (y * (x * (z * u)))) = (x * (y * x)) \ u. [para(8(a,1),104(a,1,1)),rewrite([8(10)])].

369 (x * y) / (x \ z) = x * ((y / z) * x). [para(7(a,1),113(a,1,1,2))].

377 x \ ((x * y) / z) = (y / (x * z)) * x. [para(115(a,1),5(a,1,2))].

379 (x / y) * ((z / x) * (x / y)) = ((x / y) * z) / y. [para(7(a,1),115(a,1,2,1,2))].

381 x * ((y / (x * z)) * (x * u)) = ((x * y) / z) * u. [para(115(a,1),8(a,1,1)),flip(a)].

439 x * ((0 / x) * y) = y. [para(3(a,1),125(a,1,1)),rewrite([4(2)]),flip(a)].

440 x * (((x \ y) / x) * z) = y * (x \ z). [para(4(a,1),125(a,1,1)),flip(a)].

467 x * (0 / x) = 0. [para(3(a,1),439(a,1,2))].

468 (0 / x) \ y = x * y. [para(4(a,1),439(a,1,2)),flip(a)].

469 (0 / x) * y = x \ y. [para(439(a,1),5(a,1,2)),flip(a)].

472 (x \ y) / y = 0 / x. [para(439(a,1),25(a,1,1,2)),rewrite([469(3),467(7),3(6)])].

473 (x / (0 / y)) * (y \ z) = y * ((y \ x) * z). [para(26(a,1),439(a,1,2)),rewrite([469(3),469(9)]),flip(a)].

475 (x * (y \ x)) * z = x * (y \ (x * z)). [para(439(a,1),27(a,1,1,2,2)),rewrite([469(3),469(9),4(8),469(7)])].

494 x \ (0 / x) = (0 / x) / x. [back_rewrite(78),rewrite([469(5)])].

502 x \ 0 = 0 / x. [para(467(a,1),5(a,1,2))].

505 x * ((x \ A) * x) = A * x. [para(467(a,1),10(a,1,1)),rewrite([2(4),469(6)]),flip(a)].

509 x / (0 / x) = x * x. [para(467(a,1),41(a,1,1,2)),rewrite([3(2)])].

511 (x * y) / (0 / x) = x * (y * x). [para(467(a,1),25(a,1,1,2,2)),rewrite([3(2)])].

512 (x * y) * (0 / x) = x * (y / x). [para(467(a,1),26(a,1,2,2)),rewrite([3(3)]),flip(a)].

519 (0 / x) / x = 0 / (x * x). [para(502(a,1),66(a,1)),rewrite([502(5),494(6)]),flip(a)].

527 x \ (0 / x) = 0 / (x * x). [back_rewrite(494),rewrite([519(6)])].

552 x / (y * x) = 0 / y. [para(468(a,1),19(a,1,2))].

553 x / (y * (y * x)) = 0 / (y * y). [para(468(a,1),70(a,1,2,2)),rewrite([468(4),469(8),527(6)])].

555 (x \ (y * (0 / x))) * z = x \ (y * (x \ z)). [para(469(a,1),8(a,1,1)),rewrite([469(10),469(10)])].

559 (x * (y \ (x * z))) / z = x * (y \ x). [para(469(a,1),25(a,1,1,2)),rewrite([469(7)])].

563 (x \ (y * (z * (y * (0 / x))))) * u = x \ (y * (z * (y * (x \ u)))). [para(469(a,1),27(a,1,1)),rewrite([469(12),469(14)])].

568 A * (0 / x) = A / x. [para(469(a,1),34(a,1)),rewrite([512(5),5(4),2(8)]),flip(a)].

569 x * ((x * y) \ x) = x / y. [para(469(a,1),115(a,1,2)),rewrite([3(5)])].

577 0 / (x / y) = y / x. [para(20(a,1),472(a,1,1)),flip(a)].

579 x / (x * (A * x)) = 0 / (x * A). [para(239(a,1),472(a,1,1))].

626 x / (y * (z * (y * x))) = 0 / (y * (z * y)). [para(8(a,1),552(a,1,2))].

631 x / (y * (z * (u * (z * (y * x))))) = 0 / (y * (z * (u * (z * y)))). [para(27(a,1),552(a,1,2))].

637 A \ (A / x) = 0 / x. [para(568(a,1),5(a,1,2))].

658 0 / ((x / y) * (x / y)) = y / ((x / y) * x). [para(55(a,1),577(a,1,2))].

661 ((x / y) \ y) / x = y / ((x / y) * x). [para(72(a,1),577(a,1,2)),rewrite([658(5)]),flip(a)].

662 (x / y) * ((y / x) * z) = z. [para(577(a,1),125(a,2,2,1)),rewrite([3(3),4(4)]),flip(a)].

663 (x / y) \ z = (y / x) * z. [para(577(a,1),468(a,1,1))].

664 A / (x / y) = A * (y / x). [para(577(a,1),568(a,1,2)),flip(a)].

665 x / ((y / x) * y) = (x / y) * (x / y). [back_rewrite(661),rewrite([663(2),55(3)]),flip(a)].

724 0 / (x \ A) = A \ x. [para(19(a,1),637(a,1,2)),flip(a)].

734 (A \ x) * (x \ A) = 0. [para(724(a,1),7(a,1,1))].

737 (x \ A) * ((A \ x) * y) = y. [para(724(a,1),125(a,2,2,1)),rewrite([3(4),4(6)]),flip(a)].

739 (x \ A) \ y = (A \ x) * y. [para(724(a,1),469(a,1,1)),flip(a)].

740 (x \ A) / (A \ x) = (x \ A) * (x \ A). [para(724(a,1),509(a,1,2))].

778 (A \ x) * ((x \ A) * y) = y. [para(734(a,1),26(a,2,1)),rewrite([740(7),21(11),737(10),2(8)])].

779 (A \ x) \ y = (x \ A) * y. [para(734(a,1),125(a,1,1)),rewrite([2(5),740(10),21(11),778(12)])].

861 x \ (A * x) = (x \ A) * x. [para(505(a,1),5(a,1,2))].

955 x / (x \ y) = x * (y \ x). [para(4(a,1),569(a,1,2,1)),flip(a)].

956 (x * y) \ x = x \ (x / y). [para(569(a,1),5(a,1,2)),flip(a)].

966 (x * A) / x = x * (A / x). [para(229(a,1),569(a,1,2,1)),rewrite([339(8),16(5),502(4),512(5)]),flip(a)].

1036 0 / (A * (x / y)) = (y / x) / A. [para(664(a,1),577(a,1,2))].

1277 (x * ((y / x) * z)) \ (x * y) = (x * y) \ (x * ((y / z) * x)). [para(125(a,1),956(a,1,1)),rewrite([369(9)])].

1303 0 / (x * (A / x)) = x / (x * A). [para(966(a,1),577(a,1,2))].

1385 x * ((x \ y) * x) = y / (0 / x). [para(4(a,1),511(a,1,1)),flip(a)].

1386 (x / y) * (y * (x / y)) = x / (y / x). [para(7(a,1),511(a,1,1)),rewrite([577(3)]),flip(a)].

1389 x \ (y * (0 / x)) = (x \ y) / x. [para(19(a,1),511(a,1,2)),rewrite([502(2),469(3),502(4),502(6),469(8)]),flip(a)].

1404 (A / x) / (0 / A) = A * (x \ A). [para(568(a,1),511(a,1,1)),rewrite([469(11)])].

1421 x / (A / x) = x * (x / A). [back_rewrite(241),rewrite([1386(7)])].

1427 x \ (y * (x \ z)) = ((x \ y) / x) * z. [back_rewrite(555),rewrite([1389(4)]),flip(a)].

1509 (x * (x / A)) * (A / x) = x. [para(1421(a,1),7(a,1,1))].

1555 x \ (x / (x / A)) = A / x. [para(1509(a,1),5(a,1,2)),rewrite([956(4)])].

1602 x / (x / A) = x * (A / x). [para(1555(a,1),4(a,1,2)),flip(a)].

1624 (x / A) / x = x / (x * A). [para(1602(a,1),577(a,1,2)),rewrite([1303(5)]),flip(a)].

1650 (x / (x * A)) * x = x / A. [para(1624(a,1),7(a,1,1))].

1709 (x * x) / A = x * (x / A). [para(1650(a,1),115(a,1,2)),flip(a)].

1733 (x * (x / A)) * A = x * x. [para(1709(a,1),7(a,1,1))].

1780 ((A \ x) * (y * (y / A))) * x = (A \ x) * (y * (y * (A \ x))). [para(1733(a,1),31(a,1,2,1)),rewrite([21(6)]),flip(a)].

1929 (x \ (y * z)) / (x * z) = (x \ y) / x. [para(552(a,1),114(a,1,1,1)),rewrite([469(4),552(6),552(8),469(10),1389(8)])].

1931 0 / ((x / y) * (z * (x / y))) = y / ((x / y) * (z * x)). [para(114(a,1),577(a,1,2))].

2132 x * ((x \ y) / x) = y * (0 / x). [para(4(a,1),512(a,1,1)),flip(a)].

2134 (x / y) * (y / (x / y)) = x * (y / x). [para(7(a,1),512(a,1,1)),rewrite([577(3)]),flip(a)].

2138 x \ (y / (0 / x)) = (x \ y) * x. [para(19(a,1),512(a,1,2)),rewrite([502(2),469(3),502(4),502(6),469(8)]),flip(a)].

2147 (x * (A * y)) * (0 / y) = y * ((y \ x) * A). [para(30(a,1),512(a,1,1)),rewrite([6(11)])].

2154 ((x * y) / z) * (0 / x) = x * (y / (x * z)). [para(115(a,1),512(a,1,1)),rewrite([6(9)])].

2170 x * ((x \ y) * (x * z)) = (y / (0 / x)) * z. [para(512(a,1),86(a,2,1,2)),rewrite([467(5),3(2),467(6),3(3),467(9),3(6),19(7),1385(7)])].

2308 (x \ (x / A)) * A = 0. [para(579(a,1),34(a,1,1)),rewrite([8(9),579(13),2147(14),956(9),469(13),5(11),579(10),568(11),552(9),467(8)])].

2316 x \ (x / A) = 0 / A. [para(2308(a,1),6(a,1,1)),flip(a)].

2342 x * (0 / A) = x / A. [para(2316(a,1),4(a,1,2))].

2352 (A \ x) * (0 / x) = 0 / A. [para(2316(a,1),739(a,1)),rewrite([472(9)]),flip(a)].

2356 x / (0 / A) = x * A. [para(2316(a,1),955(a,1,2)),rewrite([663(7),7(7)])].

2367 (A / x) * A = A * (x \ A). [back_rewrite(1404),rewrite([2356(6)])].

2417 (x * (y * x)) / A = x * (y * (x / A)). [para(2342(a,1),8(a,1)),rewrite([2342(8)])].

2449 (A * x) / A = A * (x / A). [para(2342(a,1),512(a,1))].

2502 (A * x) * A = A * (x * A). [para(2356(a,1),511(a,1))].

2650 ((A \ x) * y) / (0 / x) = ((A \ x) * y) * x. [para(2352(a,1),115(a,1,2,1,2)),rewrite([2356(6),31(8)]),flip(a)].

2661 ((A \ x) * (y * (z * (y / A)))) * x = (A \ x) * (y * (z * (y * (A \ x)))). [para(2352(a,1),117(a,1,1,2,2,2,2)),rewrite([2342(6),2650(10

)])].

2757 (A * A) / x = A * (A / x). [para(2367(a,1),115(a,1,2)),rewrite([956(6),637(6),568(5)]),flip(a)].

2858 (x * (A * A)) / A = x * A. [para(30(a,1),2449(a,1,1)),rewrite([6(15),1385(12),2356(10)])].

3001 ((x \ y) / x) * (x * z) = x \ (y * z). [para(4(a,1),126(a,1,2,1)),flip(a)].

3010 (C / x) * (x * (x * A)) = x * (C * A). [para(29(a,1),126(a,1,2)),rewrite([5(6)]),flip(a)].

3137 (x / A) / A = x / (A * A). [para(2757(a,1),577(a,1,2)),rewrite([1036(6)])].

3269 A * (C * A) = A * (A * C). [para(29(a,1),2858(a,1,1)),rewrite([2449(9),2417(8),17(6),3(5),2502(10)]),flip(a)].

3391 (x / y) * ((y / x) / ((z / (y / x)) * y)) = (((y / x) * z) * x) \ (y / x). [para(128(a,1),956(a,1,1)),rewrite([663(12)]),flip(a)].

3656 C * A = A * C. [para(3269(a,1),5(a,1,2)),rewrite([5(7)]),flip(a)].

3686 (C / x) * (x * (x * A)) = x * (A * C). [back_rewrite(3010),rewrite([3656(9)])].

3742 (x * (x * (A * C))) / (x * A) = x * C. [back_rewrite(145),rewrite([3656(3)])].

3744 (x * C) * (x * A) = x * (x * (A * C)). [back_rewrite(29),rewrite([3656(8)])].

3750 (C \ A) * C = A. [para(3656(a,1),5(a,1,2)),rewrite([861(5)])].

3751 A * (C / A) = C. [para(3656(a,1),6(a,1,1)),rewrite([2449(5)])].

3909 C \ A = A / C. [para(3750(a,1),6(a,1,1)),flip(a)].

3925 A \ C = C / A. [para(3751(a,1),5(a,1,2))].

3931 (A * x) * (C / A) = A * ((x / A) * C). [para(3751(a,1),26(a,1,2,2)),flip(a)].

3935 A * ((C / (A * A)) * x) = C * (A \ x). [para(3751(a,1),125(a,1,1)),rewrite([3137(10)]),flip(a)].

3946 (C / (A * A)) * (A * x) = A \ (C * x). [para(3751(a,1),126(a,1,2,1)),rewrite([3137(9)]),flip(a)].

4157 ((x * y) * y) * (A * x) = (x * y) * ((y * A) * x). [para(552(a,1),133(a,1,2,1)),rewrite([469(8),5(6)]),flip(a)].

5503 (x * y) * (0 / y) = x. [para(2352(a,1),161(a,1,2,2)),rewrite([779(5),2342(11),6(9),778(6),4(4)]),flip(a)].

5578 x \ (x / y) = 0 / y. [para(5503(a,1),5(a,1,2)),rewrite([956(2)])].

5579 x / (0 / y) = x * y. [para(5503(a,1),6(a,1,1))].

5580 x * (0 / y) = x / y. [para(7(a,1),5503(a,1,1))].

5585 ((x * y) * x) * y = (x * y) * (x * y). [para(5503(a,1),41(a,1,1,2)),rewrite([5579(5)])].

5586 ((x * y) * (z * x)) * y = (x * y) * (z * (x * y)). [para(5503(a,1),25(a,1,1,2,2)),rewrite([5579(6)])].

5594 (0 / x) / y = 0 / (y * x). [para(5503(a,1),552(a,1,2))].

5595 (x * (y / z)) * (z / y) = x. [para(577(a,1),5503(a,1,2))].

5658 (x * y) \ x = 0 / y. [back_rewrite(956),rewrite([5578(4)])].

5701 x * ((x \ y) * (x * z)) = (y * x) * z. [back_rewrite(2170),rewrite([5579(7)])].

5704 x \ (y * x) = (x \ y) * x. [back_rewrite(2138),rewrite([5579(3)])].

5735 x * ((x \ y) * x) = y * x. [back_rewrite(1385),rewrite([5579(6)])].

5741 (x * y) * x = x * (y * x). [back_rewrite(511),rewrite([5579(4)])].

5742 (x * y) * (y \ z) = y * ((y \ x) * z). [back_rewrite(473),rewrite([5579(3)])].

5817 ((x * y) / z) / x = x * (y / (x * z)). [back_rewrite(2154),rewrite([5580(5)])].

5825 x * ((x \ y) / x) = y / x. [back_rewrite(2132),rewrite([5580(6)])].

5836 x \ (y / x) = (x \ y) / x. [back_rewrite(1389),rewrite([5580(3)])].

5857 x \ (y * (z * (y * (x \ u)))) = (x \ (y * (z * (y / x)))) * u. [back_rewrite(563),rewrite([5580(3)]),flip(a)].

5860 (x * y) / x = x * (y / x). [back_rewrite(512),rewrite([5580(4)])].

5991 (x * y) * (x * y) = x * (y * (x * y)). [back_rewrite(5585),rewrite([5741(2),8(3)]),flip(a)].

6313 0 / (x \ y) = y \ x. [para(19(a,1),5578(a,1,2)),flip(a)].

6314 (x / y) / (x \ (0 / y)) = x * x. [para(5578(a,1),70(a,1,2,2))].

6315 (x \ y) \ x = y \ (x * x). [para(70(a,1),5578(a,1,2)),rewrite([6313(6)]),flip(a)].

6318 x * ((y / x) * (x / z)) = (x * y) / z. [para(5578(a,1),125(a,1,2)),rewrite([5580(4)]),flip(a)].

6319 x \ (0 / y) = 0 / (y * x). [para(552(a,1),5578(a,1,2))].

6323 (x / y) * ((y / x) / z) = 0 / z. [para(5578(a,1),663(a,1)),flip(a)].

6328 (x \ (y * (z * (y / x)))) * u = ((x \ (y * (z * y))) / x) * u. [para(5578(a,1),87(a,1,1)),rewrite([5578(8),469(5),469(7),5857(5),5578(1

1),469(11),5836(9)])].

6360 (x / y) * (y * x) = x * x. [back_rewrite(6314),rewrite([6319(4),5579(5)])].

6402 (((x / y) * z) * y) \ (x / y) = 0 / ((z / (x / y)) * x). [back_rewrite(3391),rewrite([6323(7)]),flip(a)].

6403 x \ (y * (z * (y * (x \ u)))) = ((x \ (y * (z * y))) / x) * u. [back_rewrite(5857),rewrite([6328(10)])].

6416 (x * (x / y)) * y = x * x. [para(5579(a,1),41(a,1)),rewrite([5580(3)])].

6417 (x * (y * (x / z))) * z = x * (y * x). [para(5579(a,1),25(a,1)),rewrite([5580(3)])].

6418 x * ((y / (x / z)) * x) = (x * y) * z. [para(5579(a,1),115(a,2)),rewrite([5580(3)])].

6420 x / (y / z) = x * (z / y). [para(577(a,1),5579(a,1,2))].

6433 x * ((y * (z / x)) * x) = (x * y) * z. [back_rewrite(6418),rewrite([6420(2)])].

6434 (((x / y) * z) * y) \ (x / y) = 0 / ((z * (y / x)) * x). [back_rewrite(6402),rewrite([6420(8)])].

6603 (x / y) * (y * (y / x)) = x * (y / x). [back_rewrite(2134),rewrite([6420(3)])].

6632 (x / y) * (y * (x / y)) = x * (x / y). [back_rewrite(1386),rewrite([6420(6)])].

6731 (x * (y * x)) / z = x * (y * (x / z)). [para(5580(a,1),8(a,1)),rewrite([5580(6)])].

6732 (x * x) / y = x * (x / y). [para(5580(a,1),21(a,1)),rewrite([5580(5)])].

6737 x * (((x * y) * z) \ x) = (x / z) / y. [para(5580(a,1),115(a,2,1)),rewrite([5594(4),469(5)])].

6739 (x / y) * (x \ z) = x * ((x * y) \ z). [para(5580(a,1),125(a,1,1)),rewrite([5594(6),469(7)])].

6740 (x * y) / (z * x) = x * ((y / x) / z). [para(5580(a,1),125(a,2,2)),rewrite([6319(4),5580(5)])].

6745 0 / (x * (y / z)) = (z / y) / x. [para(5580(a,1),663(a,2)),rewrite([6319(4)])].

6761 x \ (y * (z * (y / x))) = (x \ (y * (z * y))) / x. [para(5580(a,1),117(a,2,2,2,2)),rewrite([469(5),469(7),6403(5),6(6),469(10)]),flip(a

)].

6765 (x * y) \ (x * z) = x \ ((x / y) * z). [para(5580(a,1),126(a,1,2,1)),rewrite([5594(6),469(8)]),flip(a)].

6766 (x / (y * z)) * y = (x / y) * (y / z). [para(5580(a,1),126(a,1,2)),rewrite([377(3),5580(7)])].

6904 x \ ((x / ((y / x) * z)) * y) = x \ ((x / y) * ((y / z) * x)). [back_rewrite(1277),rewrite([6765(5),6765(10)])].

6913 (x * (y * x)) \ z = x \ (y \ (x \ z)). [back_rewrite(343),rewrite([6765(11),631(6),469(10),6765(8),626(4),469(7),6765(5),552(2),469(4),

5(2)]),flip(a)].

6976 x \ ((x * y) / z) = (y / x) * (x / z). [back_rewrite(377),rewrite([6766(6)])].

7313 x \ ((x / y) * ((y / z) * x)) = z \ x. [para(125(a,1),5658(a,1,1)),rewrite([6765(5),6904(5),6313(8)])].

7314 0 / ((x / y) * z) = z \ (y / x). [para(662(a,1),5658(a,1,1)),flip(a)].

7318 ((x * y) * z) \ x = (x * z) \ (x / y). [para(143(a,1),5658(a,1,1)),rewrite([6765(7),6904(7),7313(7),7314(8)])].

7328 (x * (y / z)) \ (z / y) = z / ((y / z) * (x * y)). [back_rewrite(1931),rewrite([7314(6)])].

7343 x * ((x * y) \ (x / z)) = (x / y) / z. [back_rewrite(6737),rewrite([7318(3)])].

7345 0 / ((x * (y / z)) * z) = z \ ((z / y) / x). [back_rewrite(6434),rewrite([7318(5),7(2)]),flip(a)].

7392 (x \ y) * ((y \ x) * z) = z. [para(6313(a,1),125(a,2,2,1)),rewrite([3(3),4(4)]),flip(a)].

7393 (x \ y) \ z = (y \ x) * z. [para(6313(a,1),469(a,1,1)),flip(a)].

7401 x / (y \ z) = x * (z \ y). [para(6313(a,1),5580(a,1,2)),flip(a)].

7420 x \ (y * y) = (x \ y) * y. [back_rewrite(6315),rewrite([7393(2)]),flip(a)].

7744 (x * y) * (z \ x) = x * ((y / z) * x). [back_rewrite(369),rewrite([7401(3)])].

7844 0 / (x * ((y / x) * z)) = (z \ x) / (x * y). [para(125(a,1),5594(a,2,2)),rewrite([7401(3),2(3)]),flip(a)].

7845 (x \ (y / z)) * (z / y) = 0 / x. [para(662(a,1),5594(a,2,2)),rewrite([7314(4),6420(4)])].

7993 x \ (y * (y * x)) = ((x \ y) * y) * x. [para(21(a,1),5704(a,1,2)),rewrite([7420(5)])].

8002 (x * y) \ y = y \ (x \ y). [para(469(a,1),5704(a,1,2)),rewrite([6319(5),469(6)]),flip(a)].

8016 (x / y) * (y * y) = x * y. [para(5704(a,1),126(a,1)),rewrite([5(2)]),flip(a)].

8043 ((x \ y) * y) * x = (x \ y) * (y * x). [para(5735(a,1),8(a,2,2)),rewrite([4(3)])].

8044 x * (((x \ y) * x) * x) = y * (x * x). [para(5735(a,1),21(a,1)),rewrite([66(4),5701(7)]),flip(a)].

8045 x * ((x \ y) * (y * x)) = y * (y * x). [para(21(a,1),5735(a,2)),rewrite([7420(2),8043(3)])].

8047 ((x \ y) * (y * x)) / x = (x \ y) * y. [para(5735(a,1),25(a,1,1,2)),rewrite([4(7)])].

8084 (x / y) * x = x * (y \ x). [para(5578(a,1),5735(a,1,2,1)),rewrite([469(3)]),flip(a)].

8086 0 / ((x \ y) * x) = x \ (y \ x). [para(5735(a,1),5658(a,1,1)),rewrite([8002(2)]),flip(a)].

8087 (x \ (y \ x)) / x = 0 / (y * x). [para(5735(a,1),5594(a,2,2)),rewrite([8086(4)])].

8090 (x * y) * y = x * (y * y). [para(5704(a,1),5735(a,1,2,1)),rewrite([8044(4)]),flip(a)].

8091 x \ (y * (y * x)) = (x \ y) * (y * x). [back_rewrite(7993),rewrite([8043(6)])].

8157 x / (y * (x \ y)) = (x / y) * (x / y). [back_rewrite(665),rewrite([8084(2)])].

8227 (x * y) * ((y * A) * x) = x * ((y * (y * A)) * x). [back_rewrite(4157),rewrite([8090(2),10(5),21(3)]),flip(a)].

8419 (x * y) * ((x \ z) / x) = x * ((y / x) * (z / x)). [para(5825(a,1),26(a,1,2,2)),flip(a)].

8420 ((x / A) * (A * y)) / A = x * (y / A). [para(5825(a,1),30(a,2,2)),rewrite([663(9),7401(8),475(9),5741(11),8419(16),6(12),3001(13),6761(

9),5735(6),126(5)])].

8455 (x / y) / x = x / (x * y). [para(5578(a,1),5825(a,1,2,1)),rewrite([5594(3),5580(4)]),flip(a)].

8511 (x * (y / x)) * ((x / (x * y)) * z) = z. [para(5860(a,1),662(a,1,1))].

8619 ((x \ y) / x) * y = (x \ y) * (x \ y). [para(4(a,1),6360(a,1,2))].

8629 (x * (y * y)) / y = x * y. [para(6360(a,1),25(a,1,1,2)),rewrite([7(5)])].

8661 ((x * y) * ((y * (y * A)) * x)) / (A * x) = (x * y) * (y * y). [para(6360(a,1),118(a,2,2)),rewrite([143(8),8227(6),26(8)])].

8723 (x / y) / y = x / (y * y). [para(6416(a,1),552(a,1,2)),rewrite([6745(6)]),flip(a)].

8793 (x * (y / z)) \ u = ((z / y) / x) * u. [para(6420(a,1),663(a,1,1))].

8802 x / (y * (z / u)) = x * ((u / z) / y). [para(6420(a,1),6420(a,1,2))].

8812 x / ((y / x) * (z * y)) = (x / y) * (z \ (x / y)). [back_rewrite(7328),rewrite([8793(4),8084(4)]),flip(a)].

8992 (x / (y * y)) * ((y * (y / x)) * z) = z. [para(6732(a,1),662(a,1,2,1))].

9034 (x \ y) * (((y \ x) * x) * z) = y * ((y \ x) * z). [para(23(a,1),7392(a,1,2))].

9038 ((x / y) * z) * ((z \ (y / x)) * u) = u. [para(663(a,1),7392(a,1,1))].

9053 (x \ y) * ((y \ x) / z) = 0 / z. [para(5580(a,1),7392(a,1,2))].

9071 ((x / y) * z) \ u = (z \ (y / x)) * u. [para(663(a,1),7393(a,1,1))].

9083 ((x \ y) * z) * ((z \ (y \ x)) * u) = u. [para(7393(a,1),7392(a,1,1))].

9085 ((x \ y) * z) \ u = (z \ (y \ x)) * u. [para(7393(a,1),7393(a,1,1))].

9230 (x * (y \ z)) \ u = ((z \ y) / x) * u. [para(7401(a,1),663(a,1,1))].

9231 x / ((y / z) * u) = x * (u \ (z / y)). [para(663(a,1),7401(a,1,2))].

9241 x / (y * (z \ y)) = x * ((y \ z) / y). [para(5836(a,1),7401(a,2,2)),rewrite([663(2),8084(2)])].

9242 x / (y * (z \ u)) = x * ((u \ z) / y). [para(7401(a,1),6420(a,1,2))].

9243 x / ((y \ z) * u) = x * (u \ (z \ y)). [para(7393(a,1),7401(a,1,2))].

9289 (x / y) * (z \ (x / y)) = x * ((z * y) \ (x / y)). [back_rewrite(8812),rewrite([9231(4)]),flip(a)].

9431 (x / y) * (x / y) = x * ((y \ x) / y). [back_rewrite(8157),rewrite([9241(3)]),flip(a)].

10611 (x / (y * y)) * (y / x) = x / (x * y). [para(7(a,1),8455(a,2,2)),rewrite([8723(2),6420(4),8455(6)])].

10617 ((x / y) / z) / x = x / ((x * z) * y). [para(26(a,1),8455(a,2,2)),rewrite([9231(4),7343(4)])].

11550 (x \ y) * (y \ z) = y * ((x * y) \ z). [para(8087(a,1),125(a,2,2,1)),rewrite([4(3),469(7)])].

12871 (x \ (y * z)) / y = (x \ y) * (z / y). [para(293(a,1),5658(a,1,1)),rewrite([7393(3),9242(8),2(8)]),flip(a)].

13156 x * (((x \ y) / x) / z) = y / (z * x). [para(5580(a,1),440(a,1,2)),rewrite([6319(7),5580(8)])].

13159 x \ (y * (z \ y)) = ((x \ y) / z) * y. [para(440(a,1),5658(a,1,1)),rewrite([9230(3),9231(8),7401(6),2(8)]),flip(a)].

13250 (x * ((y * z) \ (x / z))) * z = (x / z) * (y \ x). [para(7(a,1),475(a,2,2,2)),rewrite([9289(4)])].

13288 (x * (y \ x)) / z = x * (y \ (x / z)). [para(475(a,1),5580(a,1)),rewrite([5580(3)]),flip(a)].

13291 x \ ((y \ z) / y) = ((y * x) \ z) / y. [para(475(a,1),5594(a,2,2)),rewrite([9242(5),469(5),9242(8),2(8)])].

13298 (x * (y \ (x * z))) * (x * (y \ x)) = x * (((y \ (x * (z * x))) / y) * x). [para(475(a,1),5741(a,1,1)),rewrite([475(12),6403(11)])].

13686 (x * (y \ (x / z))) * z = x * (y \ x). [para(5580(a,1),559(a,1,1,2,2)),rewrite([6420(6),18(5)])].

13691 ((x * y) * (z \ (x * (y * x)))) / x = (x * y) * (z \ (x * y)). [para(5741(a,1),559(a,1,1,2,2))].

13732 (x / y) * (z \ x) = x * ((z * y) \ x). [back_rewrite(13250),rewrite([13686(5)]),flip(a)].

14140 ((x \ y) / x) * (x / z) = x \ (y / z). [para(5578(a,1),1427(a,1,2,2)),rewrite([5580(3)]),flip(a)].

14141 x \ (y / (z * x)) = ((x \ y) / x) / z. [para(5580(a,1),1427(a,2)),rewrite([6319(3),5580(4)])].

14148 ((x * y) / z) * y = x * (y * (z \ y)). [para(5825(a,1),1427(a,2)),rewrite([663(3),7401(2),475(3),6420(6),7401(5),13298(6),5(7),440(6),

7744(4),5(5),6420(6),7401(5)])].

14248 (x \ (y / z)) / x = (x \ y) / (x * z). [para(7(a,1),1929(a,1,1,2)),flip(a)].

14270 (x \ y) / (x * ((z / u) * y)) = (x \ u) / (x * z). [para(662(a,1),1929(a,1,1,2)),rewrite([14248(8)])].

14310 (x \ (y * (z / u))) / x = (x \ y) * ((z / u) / x). [para(5595(a,1),1929(a,1,1,2)),rewrite([8802(4)]),flip(a)].

14314 (x \ (y * (z * y))) / (x * y) = (x \ (y * z)) / x. [para(5741(a,1),1929(a,1,1,2))].

15190 (x / C) * (x * (A * C)) = x * (x * A). [para(3686(a,1),5(a,1,2)),rewrite([663(7)])].

15191 (x * (A * C)) / (x * (x * A)) = C / x. [para(3686(a,1),6(a,1,1))].

15207 x * ((x \ C) * (x \ A)) = x \ (A * C). [para(469(a,1),3686(a,1,2,2)),rewrite([6420(4),18(3),469(7),5742(6),469(12)])].

15772 (x * A) * (C / A) = A * ((A \ x) * C). [para(5735(a,1),3931(a,1,1)),rewrite([6(13)])].

15787 (x \ A) * (C / A) = A * ((x * A) \ C). [para(8087(a,1),3931(a,2,2,1)),rewrite([4(6),469(13)])].

17634 (x * y) * ((y \ z) * y) = y * ((y \ x) * (z * y)). [para(5735(a,1),5701(a,1,2,2)),flip(a)].

18427 x * ((x \ y) / (x * z)) = (y / z) / x. [para(4(a,1),5817(a,1,1,1)),flip(a)].

18445 x \ (y * (z \ x)) = ((x \ y) / z) * x. [para(469(a,1),5817(a,1,1,1)),rewrite([6420(5),18(4),469(8),7401(7),469(8)]),flip(a)].

18475 ((x * y) * z) / x = x * (y * (z / x)). [para(5580(a,1),5817(a,2,2,2)),rewrite([6420(4),18(3),6420(5)])].

18604 (x * y) * (z \ (x * y)) = x * (y * ((z \ x) * y)). [back_rewrite(13691),rewrite([18475(6),12871(4),6(3)]),flip(a)].

19300 (x * (y * (x * y))) / z = (x * y) * ((x * y) / z). [para(5991(a,1),6732(a,1,1))].

19868 (x * y) / (z * (z * x)) = x * ((y / x) / (z * z)). [para(553(a,1),6318(a,1,2,2)),rewrite([5580(5)]),flip(a)].

20699 x * ((y \ (z / x)) * x) = (x / y) * z. [para(7845(a,1),6417(a,1,1,2)),rewrite([5580(3)]),flip(a)].

20952 (x * (y / z)) * z = (x / z) * (z * y). [para(6433(a,1),5(a,1,2)),rewrite([126(3)]),flip(a)].

20953 (x * y) * (z * x) = x * ((y * z) * x). [para(6(a,1),6433(a,1,2,1,2)),flip(a)].

20970 (x * (y * (z / u))) * (u / z) = (z / u) * (((u / z) * x) * y). [para(6433(a,1),662(a,1,2)),rewrite([6420(7)]),flip(a)].

21119 (x * y) \ (x / z) = x \ ((x / y) / z). [back_rewrite(7345),rewrite([20952(4),9231(5),2(5)])].

21409 (x * y) * (y * y) = x * (y * (y * y)). [back_rewrite(8661),rewrite([20953(6),6740(9),6(6),25(6)]),flip(a)].

21454 (x * y) * (z * (x * y)) = x * (y * ((z * x) * y)). [back_rewrite(5586),rewrite([20953(3),8(4),20953(3)]),flip(a)].

24692 x * ((y * (z / u)) / z) = x * ((y * z) / (z * u)). [para(6740(a,1),6420(a,1,2)),rewrite([8802(4),6420(2)])].

24726 (x \ y) / (z * y) = y / (z * (x * y)). [para(8087(a,1),6740(a,2,2,1)),rewrite([4(3),5594(7),5580(8)])].

24826 (x * (x / y)) * ((z * (y / (x * x))) * (x / y)) = ((x * (x / y)) * z) * (y / (y * x)). [para(6603(a,1),6740(a,1,2)),rewrite([8802(6),8

455(5),8802(11),8723(10),6420(13)]),flip(a)].

24965 ((x * y) * z) \ (x * u) = x \ (((x / z) / y) * u). [para(26(a,1),6765(a,1,1)),rewrite([9231(8),21119(7),4(8)])].

25213 (x / y) * (y * (z \ y)) = (x / z) * y. [para(4(a,1),6766(a,1,1,2)),rewrite([7401(5)]),flip(a)].

25286 (x / (y * z)) * z = (x / z) * (y \ z). [para(5735(a,1),6766(a,1,1,2)),rewrite([552(7),7401(7),2(7)])].

25406 (x * (y / (z * u))) * z = (x / z) * ((z * y) / u). [para(6318(a,1),6766(a,1,1,2)),rewrite([6420(3),8802(9),6420(8),6318(9)])].

25416 (x * (y / (z * z))) * (z / y) = (x * (y / z)) / y. [para(6632(a,1),6766(a,1,1,2)),rewrite([8802(3),8723(2),6420(7),552(11),5580(10)])]

.

25495 ((x * (x / y)) * z) * (y / (y * x)) = (x * (x / y)) * ((z * y) / (y * x)). [back_rewrite(24826),rewrite([25416(7),24692(6)]),flip(a)].

26178 (x * ((A * C) / x)) * (x / (x * A)) = C. [para(3742(a,1),6976(a,1,2)),rewrite([5(3),5860(6)]),flip(a)].

26208 (x / y) * ((z / x) * (x / u)) = x * ((x * y) \ ((x * z) / u)). [para(6976(a,1),6739(a,1,2))].

26249 x * ((x * y) \ ((x * z) / y)) = ((x / y) * z) / y. [back_rewrite(379),rewrite([26208(5)])].

26250 (x / y) * ((y / z) * x) = x * (z \ x). [para(7313(a,1),4(a,1,2)),flip(a)].

26306 A * (((C / A) / x) * A) = C * (x \ A). [para(7313(a,1),3935(a,2,2)),rewrite([26250(12),3946(11),18445(7),3925(4)])].

26328 (x * (y * z)) \ z = z \ (y \ (x \ z)). [para(7313(a,1),6913(a,2,2,2)),rewrite([26250(6),13159(5),5658(3),5594(4),469(5)])].

26624 ((x * y) * z) * y = x * (y * (z * y)). [para(5(a,1),7744(a,1,2)),rewrite([21454(8),7(5)])].

28100 (x / y) * ((x \ z) * (z * x)) = x * ((x * y) \ (z * (z * x))). [para(8091(a,1),6739(a,1,2))].

28449 (x * (A * y)) / A = (x * A) * (y / A). [para(6(a,1),8420(a,1,1,1))].

28769 (x \ (y * z)) / (x * y) = (x \ y) * ((z / y) / x). [para(8511(a,1),1929(a,1,1,2)),rewrite([14270(6),14310(8)])].

28833 (x \ (y * z)) / x = (x \ y) * (z / x). [back_rewrite(14314),rewrite([28769(5),6(3)]),flip(a)].

29500 (x \ y) * (y * ((x * y) \ z)) = y * (((y \ (x \ y)) / x) * z). [para(8619(a,1),5742(a,1,1)),rewrite([21(5),11550(4),13291(8),8002(7)])

].

31178 (x * y) \ ((x * z) / u) = (y \ (z / (x * u))) * x. [para(381(a,1),5658(a,1,1)),rewrite([9071(4),9231(10),2(10)]),flip(a)].

31195 (x * (y \ (z \ u))) * ((u \ z) * w) = (z \ u) * ((((u \ z) * x) / y) * w). [para(381(a,1),7392(a,1,2)),rewrite([9243(9)]),flip(a)].

31393 ((x / y) * z) / y = x * ((y \ z) / y). [back_rewrite(26249),rewrite([31178(4),14141(3),7(4)]),flip(a)].

31396 (x / y) * ((z / x) * (x / u)) = x * ((y \ (z / (x * u))) * x). [back_rewrite(26208),rewrite([31178(9)])].

32155 x / (y * ((z / u) * w)) = x * ((w \ (u / z)) / y). [para(9038(a,1),6740(a,1,1)),rewrite([9231(12),5741(12),6731(13),9038(14)])].

32232 (x \ (y / z)) / y = (x \ y) / (y * z). [back_rewrite(7844),rewrite([32155(5),2(5)])].

32816 (x \ (y \ z)) * ((z \ y) * u) = (y \ z) * (((z \ y) / x) * u). [para(9085(a,1),6765(a,1)),rewrite([7393(10)])].

35472 (x * (y / z)) / y = (x * y) / (y * z). [para(10611(a,1),5701(a,1,2,2)),rewrite([663(5),6732(4),25495(8),8992(9),25416(8)]),flip(a)].

35532 ((x / y) * z) / x = x * (y \ (z / x)). [para(5580(a,1),10617(a,2,2,1)),rewrite([6420(4),18(3),9231(6)])].

36744 ((x \ y) * (z * u)) / z = ((x \ y) * z) * (u / z). [para(7393(a,1),12871(a,1,1)),rewrite([7393(6)])].

37034 x * (((x \ y) * z) * x) = y * (z * x). [para(8629(a,1),13156(a,2)),rewrite([5991(3),28833(6),19300(5),6(4),5741(3),36744(5),6(4)])].

37127 (x / y) * (z * x) = x * ((y \ z) * x). [para(5(a,1),13159(a,2,1,1)),rewrite([18604(4),5(5)]),flip(a)].

37933 x \ ((x / y) * z) = (y \ (z / x)) * x. [para(13732(a,1),11550(a,2)),rewrite([663(4),7(4),20952(6),26328(7),663(5),4(8)]),flip(a)].

38003 (x * y) \ (x * z) = (y \ (z / x)) * x. [back_rewrite(6765),rewrite([37933(6)])].

38368 x * (((y * x) \ z) * x) = y \ (z * x). [para(8629(a,1),14140(a,2,2)),rewrite([28833(4),6732(3),20970(6),6739(4),37127(6),5(4)])].

38460 x \ (y * (z * x)) = ((x \ y) * z) * x. [para(8629(a,1),14141(a,1,2)),rewrite([5991(6),28833(9),19300(8),6(7),5741(6),36744(8),6(7)])].

38473 (((A \ x) * x) * C) / x = A \ (x * C). [para(3742(a,1),14141(a,1,2)),rewrite([28833(13),28449(12),15772(12),23(13)]),flip(a)].

38581 ((A * C) / x) * A = C * (A * (x \ A)). [para(3656(a,1),14148(a,1,1,1))].

39396 (x \ (A * C)) * ((A \ x) * x) = C * x. [para(469(a,1),15191(a,1,1)),rewrite([469(10),469(9),7401(8),7393(7),6420(12),18(11)])].

39412 (x * A) * ((C / A) / (x * x)) = C / x. [para(15191(a,1),13156(a,2)),rewrite([38003(9),6976(8),20952(9),6(12),8723(7)])].

39415 (x * A) \ (C / x) = (C / A) / (x * x). [para(15191(a,1),14141(a,1,2)),rewrite([38003(12),6976(11),20952(12),6(15),8723(10)])].

39439 (x \ (A * C)) * ((A \ x) * (C \ x)) = x. [para(15207(a,1),6(a,1,1)),rewrite([9242(10),7401(9)])].

39788 A * ((x * C) \ (A * (A * ((x * A) \ C)))) = A * ((((x * C) \ A) / x) * C). [para(15787(a,1),8043(a,2,2)),rewrite([663(6),13732(6),7744

(9),8(13),3751(11),663(15),13732(15),475(22)]),flip(a)].

39789 (C / A) * (A * ((((x * C) \ A) / x) * C)) = A * (((A \ (x \ A)) / x) * C). [para(15787(a,1),8045(a,1,2,2)),rewrite([663(9),13732(9),47

5(16),39788(16),15787(21),29500(22)])].

41373 x * ((x \ y) * (z / x)) = (y * z) / x. [para(5580(a,1),18427(a,1,2,2)),rewrite([6420(3),6420(7),18(6)])].

41760 (x * (y * z)) / (x * y) = (x * y) * ((z / y) / x). [para(18427(a,1),18475(a,2,2)),rewrite([5741(2),125(4),6(2)])].

42293 x * ((y \ (z / x)) * (x * u)) = ((x / y) * z) * u. [para(20699(a,1),8(a,1,1)),flip(a)].

42301 ((x / y) * z) * (x \ u) = x * ((y \ (z / x)) * u). [para(20699(a,1),125(a,1,1)),rewrite([6(8)])].

42348 x * ((x * y) \ (z * (z * x))) = x * ((y \ ((x \ z) * z)) * x). [para(8047(a,1),20699(a,1,2,1,2)),rewrite([28100(10)]),flip(a)].

42389 (x / y) * ((x \ z) * (z * x)) = x * ((y \ ((x \ z) * z)) * x). [back_rewrite(28100),rewrite([42348(10)])].

42428 (x / y) * (y * (z * y)) = (x * z) * y. [para(6(a,1),20952(a,1,1,2)),flip(a)].

42585 (x * y) * (x * (z * x)) = x * ((y * (x * z)) * x). [para(5741(a,1),20953(a,1,2))].

43691 (C / x) * (x * A) = x * (C * (x \ A)). [para(15191(a,1),25286(a,1,1)),rewrite([41760(12),5(15),26624(14),26306(13)])].

43806 (x / (x * A)) * C = x * ((C / A) / x). [para(26178(a,1),20953(a,2,2)),rewrite([8084(4),5658(3),5580(4),31396(11),19868(8),5(9),6766(6)

,17(5),3(6)]),flip(a)].

43931 (x * (x * (A * C))) \ A = A \ (x \ ((x * C) \ A)). [para(3744(a,1),26328(a,1,1))].

44708 (x * ((y \ z) / y)) / y = ((x / y) * z) / (y * y). [para(31393(a,1),8723(a,1,1))].

44745 (x * (x * A)) / C = x * ((C \ x) * A). [para(15190(a,1),31393(a,1,1)),rewrite([38460(11),6(13)])].

44785 (x \ ((y \ z) / u)) * (z \ y) = (x \ (y \ z)) * (u \ (z \ y)). [para(32232(a,1),7401(a,1)),rewrite([9243(5)]),flip(a)].

44952 (x * ((y / z) / u)) / y = (x * y) / ((y * u) * z). [para(26(a,1),35472(a,2,2)),rewrite([9231(4),21119(3),4(4)])].

45078 (x \ (y * z)) * (y \ x) = (x \ y) * ((z / y) * x). [para(3001(a,1),35532(a,1,1)),rewrite([7401(4),7401(8),7744(8),5(9)])].

46121 (x \ (y * (y / z))) * z = (x \ (y / z)) * (z * y). [para(21409(a,1),38003(a,1,2)),rewrite([24965(6),42428(5),8090(3),37933(4),6732(2),

6732(7),552(6),5580(7)])].

46127 (x * y) \ (z * (u * x)) = (y \ ((x \ z) * u)) * x. [para(37034(a,1),38003(a,1,2)),rewrite([6(8)])].

46203 x \ ((y \ (z * x)) * u) = ((y * x) \ z) * (x * u). [para(38368(a,1),126(a,1,2,1)),rewrite([6(8)])].

46348 (A \ (x * C)) * x = ((A \ x) * x) * C. [para(38473(a,1),7(a,1,1))].

46409 C * (x \ ((x * C) \ A)) = x \ (x \ A). [para(553(a,1),38581(a,1,1)),rewrite([469(5),66(3),43931(12),4(13)]),flip(a)].

46473 ((A * C) \ x) * (C * x) = (A \ x) * x. [para(39396(a,1),5(a,1,2)),rewrite([7393(7)])].

46484 (x \ A) * ((C / A) * (x * x)) = C * x. [para(39396(a,1),8016(a,2)),rewrite([9243(8),5991(15),31195(16),11550(9),38003(8),5860(10),4258

5(15),25213(13),6(10),8090(8),5701(9),8090(7)])].

46521 x * (C * (x \ (x \ A))) = (C / x) * A. [para(39412(a,1),26624(a,1,1)),rewrite([26306(13),66(8)]),flip(a)].

46524 (C / A) * (A * ((x \ A) / x)) = x \ (C * (A / x)). [para(7(a,1),39415(a,1,1)),rewrite([6420(4),9431(13),8802(14),7401(12),13288(13),58

36(12)]),flip(a)].

46555 x \ ((C / x) * A) = C * (x \ (x \ A)). [para(39415(a,1),38368(a,1,2,1)),rewrite([26306(9),66(4)]),flip(a)].

46559 C * ((A \ (x / C)) * x) = (A \ x) * x. [para(39439(a,1),8(a,2,2)),rewrite([45078(9),7392(10),42301(7)])].

47914 (x * (C * (x \ A))) / (x * A) = C / x. [para(43691(a,1),6(a,1,1))].

47918 (C / (x * x)) * (x * (x * A)) = x * ((C / x) * A). [para(21(a,1),43691(a,1,2)),rewrite([66(12),21(14),46521(13)])].

47950 x * ((C * (x \ A)) / x) = C * (A / x). [para(43691(a,1),31393(a,1,1)),rewrite([5860(6),5(10)])].

47951 (x * (x / A)) * (C * (A * (x \ (x \ A)))) = x * ((C / x) * A). [para(1780(a,1),43691(a,1,2)),rewrite([16(4),2(6),8802(5),8723(4),16(8)

,16(9),3(8),2(8),20952(7),21(6),47918(7),16(8),2(10),16(12),2(14),8793(14),8723(12),8084(14),66(13)]),flip(a)].

48012 (x * C) / ((C * x) * A) = x / (x * A). [para(43806(a,1),6(a,1,1)),rewrite([44952(7)])].

48343 x \ ((x * C) \ A) = (x \ (x \ A)) / C. [para(469(a,1),44745(a,1,1,2)),rewrite([469(5),6319(11),469(13),469(12)]),flip(a)].

48424 C * ((x \ (x \ A)) / C) = x \ (x \ A). [back_rewrite(46409),rewrite([48343(6)])].

48737 ((x \ (C / A)) * A) * (A / x) = ((x \ A) / x) * C. [para(5578(a,1),46348(a,2,1,1)),rewrite([37933(6),469(14),5836(12)])].

48741 (C \ ((A \ x) * x)) * C = (A \ x) * x. [para(46348(a,2),5704(a,1,2)),rewrite([46203(7),46473(7)]),flip(a)].

48743 (A \ (x * C)) * x = C * ((A \ x) * x). [para(46348(a,2),5735(a,2)),rewrite([48741(8)]),flip(a)].

48999 ((C \ (x \ C)) * A) * (C * ((A \ ((C \ x) * x)) * C)) = x * C. [para(5735(a,1),46484(a,2)),rewrite([9085(6),5991(18),5735(17),42389(15

)])].

49158 C \ ((A \ x) * x) = (A \ (x / C)) * x. [para(46559(a,1),5(a,1,2))].

49163 (C * x) * ((A \ (y / C)) * y) = C * ((x / C) * ((A \ y) * y)). [para(46559(a,1),26(a,1,2,2)),flip(a)].

49169 (x \ (x \ A)) * C = C * (x \ (x \ A)). [para(46559(a,1),5658(a,1,1)),rewrite([9085(5),9243(12),663(10),46555(11),2(12)])].

49171 ((A \ (x / C)) * x) * C = (A \ x) * x. [para(46559(a,1),5735(a,2)),rewrite([9085(12),663(9),46555(10),5741(12),49169(11),49163(18),586

0(13),48424(13),32816(13),472(11),469(12),11550(11),5658(10),5580(11),17(9),3(8)])].

49520 x * (((C / x) * A) / (x * x)) = C * (A / (x * x)). [para(1780(a,1),47914(a,1,2)),rewrite([16(3),2(5),16(7),2(9),8793(9),8723(7),8084(9

),66(8),47951(11),16(8),16(9),3(8),2(8),6740(7),31393(5),44708(6),16(11),2(13),8802(12),8723(11)])].

49644 x \ (C * (A / x)) = (C * (x \ A)) / x. [para(47950(a,1),5(a,1,2))].

49671 (C / A) * (A * ((x \ A) / x)) = (C * (x \ A)) / x. [back_rewrite(46524),rewrite([49644(14)])].

49799 (x \ C) * (A \ (x / C)) = x \ (A \ x). [para(469(a,1),48012(a,1,1)),rewrite([5580(6),9231(7),469(13),7401(12),469(12)])].

50470 ((x \ A) / x) * C = C * ((x \ A) / x). [para(5578(a,1),48743(a,2,2,1)),rewrite([37933(6),48737(9),469(11),5836(9)])].

50870 (A \ ((A / x) / C)) * (A / x) = ((x * C) \ A) / x. [para(5578(a,1),49158(a,1,2,1)),rewrite([469(6),5836(4),13291(5)]),flip(a)].

50934 (((x * C) \ A) / x) * C = (x \ A) / x. [para(5578(a,1),49171(a,2,1)),rewrite([50870(9),469(12),5836(10)])].

50966 A * (((A \ (x \ A)) / x) * C) = (C * (x \ A)) / x. [back_rewrite(39789),rewrite([50934(11),49671(9)]),flip(a)].

51690 (x \ (A \ x)) * ((C / x) * A) = x \ C. [para(49799(a,1),6(a,1,1)),rewrite([7401(8),663(7)])].

52301 ((C / x) * A) / (x * x) = (x \ A) * ((x \ C) / x). [para(50470(a,1),31393(a,1,1)),rewrite([44708(6)])].

52323 (A * (x \ C)) / x = C * (A / (x * x)). [back_rewrite(49520),rewrite([52301(6),41373(7)])].

52499 (A \ (x / C)) * ((x \ A) * x) = C \ x. [para(51690(a,1),5594(a,2,2)),rewrite([9231(6),2(6),7401(8),7393(7),7401(12),2(12)])].

52560 (C / x) * (x * (A / x)) = A * (x \ C). [para(52323(a,1),7(a,1,1)),rewrite([25406(6),5860(5)])].

52851 ((A \ x) * (C \ (x \ A))) * x = x * ((x \ A) * (C \ (A \ x))). [para(52499(a,1),2661(a,2,2,2)),rewrite([7393(6),7393(16),6(18),44785(1

5),9083(16),7393(14),9034(20)])].

53004 (x / C) * (A * (x \ C)) = x * (A / x). [para(52560(a,1),5(a,1,2)),rewrite([663(7)])].

53831 ((x \ (A / C)) * x) * C = (x \ A) * x. [para(469(a,1),53004(a,2)),rewrite([5594(4),663(9),18(7),469(9),46127(7),3909(3),5704(5),6420(1

1),18(10),5704(10)])].

55317 x * ((x \ (x \ (C / A))) * (A * x)) = C. [para(53831(a,1),5(a,1,2)),rewrite([9085(9),663(4),5704(5),17634(9)])].

56994 (A \ x) * (C * (x \ A)) = C. [para(4(a,1),55317(a,1,2,2)),rewrite([7393(10),15787(10),7393(11),29500(11),50966(11),7(8)])].

57025 C \ (A \ x) = (A \ x) / C. [para(56994(a,1),5658(a,1,1)),rewrite([9242(10),2(10)])].

57070 C \ (x \ A) = (x \ A) / C. [para(56994(a,1),24726(a,2,2)),rewrite([11550(9),5658(8),5580(7),17(5),18(6)])].

57171 C \ x = x / C. [back_rewrite(52851),rewrite([57070(6),9053(7),469(4),57025(8),9053(9),5580(6)])].

57297 C * x = x * C. [back_rewrite(48999),rewrite([57171(4),472(4),469(4),57171(6),8084(7),57171(6),46121(10),42293(11),8090(7),46484(8)])].

57298 $F. [resolve(57297,a,14,a(flip))].

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