Prover9 input file, Cheban loops paper

% Proof 1 at 103.51 (+ 0.34) seconds.

% Length of proof is 583.

% Level of proof is 68.

% Maximum clause weight is 43.000.

% Given clauses 2734.

4 a(x * (x * x),y,C) = 0 # label(non_clause) # label(goal). [goal].

7 0 * x = x. [assumption].

8 x * 0 = x. [assumption].

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

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

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

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

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

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

15 (C * x) * (y * C) = C * ((x * y) * C). [copy(14),flip(a)].

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

17 (x * y) * z = (x * (y * z)) * a(x,y,z). [assumption].

18 (x * (y * z)) * a(x,y,z) = (x * y) * z. [copy(17),flip(a)].

22 a(c7 * (c7 * c7),c8,C) != 0. [deny(4)].

25 (C * x) * (y * C) = C * (C * (x * y)). [back_rewrite(15),rewrite([16(9,R)])].

27 x \ x = 0. [para(8(a,1),10(a,1,2))].

28 x / x = 0. [para(7(a,1),11(a,1,1))].

30 x / (y \ x) = y. [para(9(a,1),11(a,1,1))].

31 (x / y) \ x = y. [para(12(a,1),10(a,1,2))].

32 (x * x) * y = x * (x * y). [para(7(a,1),13(a,1,1,2)),rewrite([7(5)])].

33 x * (y * (x * ((x * (y * x)) \ z))) = z. [para(13(a,1),9(a,1))].

34 (x \ y) * (x * ((x \ y) * z)) = ((x \ y) * y) * z. [para(9(a,1),13(a,1,1,2)),flip(a)].

35 (x * (y * x)) \ (x * (y * (x * z))) = z. [para(13(a,1),10(a,1,2))].

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

37 x * ((y / x) * (x * z)) = (x * y) * z. [para(12(a,1),13(a,1,1,2)),flip(a)].

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

40 C \ (x * C) = x. [para(16(a,1),10(a,1,2))].

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

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

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

45 (x * (x * C)) * y = x * (C * (x * y)). [para(16(a,1),13(a,1,1,2))].

46 C * (x * (C * y)) = C * (x * (y * C)). [para(16(a,1),13(a,2,2,2)),rewrite([13(5)])].

47 (C * (C * x)) * y = C * (x * (C * y)). [para(16(a,2),13(a,1,1,2))].

48 C * (x * (y * x)) = x * (y * (x * C)). [para(16(a,2),13(a,1))].

49 C * (x * (y * x)) = x * (y * (C * x)). [para(16(a,2),13(a,2,2,2)),rewrite([16(4,R)])].

53 (x * y) * a(x,z,z \ y) = (x * z) * (z \ y). [para(9(a,1),18(a,1,1,2))].

54 (x * (y * z)) \ ((x * y) * z) = a(x,y,z). [para(18(a,1),10(a,1,2))].

56 (x * y) * a(x,y / z,z) = (x * (y / z)) * z. [para(12(a,1),18(a,1,1,2))].

57 x * a(x / (y * z),y,z) = ((x / (y * z)) * y) * z. [para(12(a,1),18(a,1,1))].

60 (x * (y * (z * (y * u)))) * a(x,y * (z * y),u) = (x * (y * (z * y))) * u. [para(13(a,1),18(a,1,1,2))].

61 (x * (y * (x * (z * u)))) * a(x * (y * x),z,u) = (x * (y * (x * z))) * u. [para(13(a,1),18(a,1,1)),rewrite([13(11)])].

63 (C * x) * y = (x * C) * y. [para(16(a,1),18(a,2,1)),rewrite([18(6)])].

66 C * (C * x) = C * (x * C). [para(7(a,1),25(a,2,2,2)),rewrite([8(3)]),flip(a)].

67 C * (C * ((C \ x) * y)) = x * (y * C). [para(9(a,1),25(a,1,1)),flip(a)].

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

70 (C * (C * (x * y))) / (y * C) = C * x. [para(25(a,1),11(a,1,1))].

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

73 C * (C * ((x * C) * y)) = C * (x * (C * (y * C))). [para(25(a,1),13(a,1))].

74 C * (x * ((C * y) * x)) = x * (C * (C * (y * x))). [para(25(a,1),13(a,2,2)),rewrite([16(6,R)])].

76 (x * C) * (y * C) = C * (C * (x * y)). [para(16(a,1),25(a,1,1))].

77 (C * x) * (C * y) = C * (C * (x * y)). [para(16(a,2),25(a,1,2))].

78 (x * (C * (C * (y * z)))) * a(x,C * y,z * C) = (x * (C * y)) * (z * C). [para(25(a,1),18(a,1,1,2))].

79 C * ((x * y) * (C * a(C * x,y,C))) = C * ((C * x) * y). [para(25(a,1),18(a,1,1)),rewrite([47(10),16(15,R)])].

80 C \ x = x / C. [para(12(a,1),40(a,1,2))].

81 C * (C * ((x / C) * y)) = x * (y * C). [back_rewrite(67),rewrite([80(4)])].

84 x * (x * ((x * x) \ y)) = y. [para(32(a,1),9(a,1))].

86 (x * (x * y)) / y = x * x. [para(32(a,1),11(a,1,1))].

87 (x * (y * (y * x))) * z = x * (y * (y * (x * z))). [para(32(a,1),13(a,1,1,2)),rewrite([32(7)])].

89 C * (x * x) = x * (x * C). [para(32(a,1),16(a,2))].

90 C * (x * x) = x * (C * x). [para(16(a,2),32(a,2,2)),rewrite([16(3,R)])].

92 (x * (x * (y * z))) * a(x * x,y,z) = (x * (x * y)) * z. [para(32(a,1),18(a,1,1)),rewrite([32(8)])].

94 (C * x) * (y * (y * C)) = C * (C * (x * (y * y))). [para(32(a,1),25(a,1,2))].

99 (x * y) * a(x,C,y / C) = (x * C) * (y / C). [para(44(a,1),18(a,1,1,2))].

100 (x * C) * ((C * x) \ y) = y. [para(63(a,1),9(a,1))].

101 (C * x) * ((x * C) \ y) = y. [para(63(a,2),9(a,1))].

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

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

105 ((x * C) * (y * (C * x))) * z = (C * x) * (y * ((C * x) * z)). [para(63(a,1),13(a,1,1))].

106 (C * x) * (y * ((C * x) * z)) = (C * x) * (y * ((x * C) * z)). [para(63(a,1),13(a,2,2,2)),rewrite([13(7)])].

108 (x * C) * (y * ((C * x) * z)) = (x * C) * (y * ((x * C) * z)). [para(63(a,2),13(a,2,2,2)),rewrite([13(7)]),flip(a)].

110 (x * ((y * C) * z)) * a(x,C * y,z) = (x * (C * y)) * z. [para(63(a,1),18(a,1,1,2))].

111 ((x * C) * (y * z)) * a(C * x,y,z) = ((C * x) * y) * z. [para(63(a,1),18(a,1,1))].

113 (x * ((C * y) * z)) * a(x,y * C,z) = (x * (y * C)) * z. [para(63(a,2),18(a,1,1,2))].

120 ((x * C) * (C * x)) * y = (C * x) * ((C * x) * y). [para(63(a,1),32(a,1,1))].

121 (C * x) * ((x * C) * y) = C * (x * (x * (C * y))). [para(63(a,1),32(a,2,2)),rewrite([77(5),47(6),32(5)]),flip(a)].

122 (x * C) * ((C * x) * y) = C * (x * (x * (C * y))). [para(63(a,1),32(a,2)),rewrite([77(5),47(6),32(5)]),flip(a)].

124 (C * (x * x)) * y = x * (C * (x * y)). [para(32(a,1),63(a,2,1)),rewrite([45(8)])].

125 x * (y * ((y * (x * y)) \ z)) = y \ z. [para(33(a,1),10(a,1,2)),flip(a)].

139 C * (C * (x * ((C * x) * y))) = C * (x * (C * (x * (C * y)))). [para(66(a,1),13(a,1,1,2)),rewrite([77(7),47(8),45(7),77(16)]),flip(a)].

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

149 x * ((x * x) \ y) = x \ y. [para(84(a,1),10(a,1,2)),flip(a)].

162 (x * y) / (x \ y) = x * x. [para(9(a,1),86(a,1,1,2))].

174 (x * C) * (C * x) = C * (C * (x * x)). [para(63(a,1),86(a,2)),rewrite([86(7),77(5)]),flip(a)].

178 (C * x) * ((C * x) * y) = C * (x * (x * (C * y))). [back_rewrite(120),rewrite([174(5),47(6),32(5)]),flip(a)].

181 (((x \ y) * y) * z) / (x * ((x \ y) * z)) = x \ y. [para(34(a,1),11(a,1,1))].

187 ((C * x) \ y) * (C * (C * (x * ((C * x) \ y)))) = C * (((C * x) \ y) * y). [para(25(a,1),34(a,1,2)),rewrite([16(18,R)])].

191 (x / C) * (C * x) = C * ((x / C) * x). [para(66(a,2),34(a,1,2)),rewrite([80(2),80(6),44(7),80(7),16(10,R)])].

196 C * ((x / C) * (x / C)) = (x / C) * x. [para(12(a,1),89(a,2,2))].

207 (x * (C * (y * y))) * a(x,y,y * C) = (x * y) * (y * C). [para(89(a,2),18(a,1,1,2))].

214 (x * (C * (x * x))) / (x * C) = x * x. [para(89(a,2),86(a,1,1,2))].

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

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

244 (x * (y * x)) \ (x * (y * z)) = x \ z. [para(9(a,1),35(a,1,2,2,2))].

271 (C * (x * C)) \ (C * (C * (x * x))) = x. [para(90(a,2),35(a,1,2,2))].

285 (x * C) \ (C * x) = 0. [para(8(a,1),103(a,1,2))].

287 (x * C) \ (C * (C * (x * y))) = y * C. [para(25(a,1),103(a,1,2))].

291 x * ((y / (x * z)) * x) = (x * y) / z. [para(12(a,1),36(a,1,1,2)),flip(a)].

293 (x * (y * (z * (y * (x * u))))) / u = x * (y * (z * (y * x))). [para(13(a,1),36(a,1,1,2)),rewrite([13(9)])].

297 ((C * x) * (y * (C * (C * (x * z))))) / (z * C) = (C * x) * (y * (C * x)). [para(25(a,1),36(a,1,1,2,2))].

298 (x * (C * (C * (y * x)))) / C = x * ((C * y) * x). [para(25(a,1),36(a,1,1,2))].

299 C * (x * C) = x * (C * C). [para(36(a,1),43(a,1))].

304 ((x * C) * (y * ((C * x) * z))) / z = (C * x) * (y * (C * x)). [para(63(a,1),36(a,1,1))].

305 (C * x) * (y * (C * x)) = (x * C) * (y * (x * C)). [para(63(a,2),36(a,1,1,2,2)),rewrite([304(8)])].

340 (x * y) * (x \ z) = x * ((y / x) * z). [para(9(a,1),37(a,1,2,2)),flip(a)].

341 x \ ((x * y) * z) = (y / x) * (x * z). [para(37(a,1),10(a,1,2))].

352 C * ((C * x) * y) = x * (C * (C * y)). [para(37(a,1),25(a,2,2)),rewrite([44(4),16(4,R)]),flip(a)].

355 ((C * x) * y) / C = (x / C) * (C * y). [para(37(a,1),43(a,1,1))].

357 (C * x) * (y / C) = C * ((x / C) * y). [para(44(a,1),37(a,1,2,2)),flip(a)].

371 ((C * x) * y) * ((x * C) \ z) = (C * x) * ((y / (C * x)) * z). [para(101(a,1),37(a,1,2,2)),flip(a)].

372 (C * x) \ (((x * C) * y) * z) = (y / (x * C)) * ((x * C) * z). [para(37(a,1),102(a,1,2))].

373 (x * C) \ (((C * x) * y) * z) = (y / (C * x)) * ((C * x) * z). [para(37(a,1),103(a,1,2))].

380 (x * x) \ y = x \ (x \ y). [para(149(a,1),10(a,1,2)),flip(a)].

386 x / (y \ (y \ x)) = y * y. [para(149(a,1),86(a,1,1,2)),rewrite([9(2),380(2)])].

387 (C * (C * (x * x))) \ y = (C * x) \ ((x * C) \ y). [para(149(a,1),102(a,1,2)),rewrite([76(11)]),flip(a)].

392 x / (x \ 0) = x * x. [para(8(a,1),162(a,1,1))].

396 (C * x) / (x \ C) = x * x. [para(16(a,2),162(a,1,1))].

409 C / (0 / C) = C * C. [para(16(a,1),392(a,2)),rewrite([80(4)])].

411 (0 / x) * (0 / x) = (0 / x) / x. [para(31(a,1),392(a,1,2)),flip(a)].

420 C * (x * (y * (z * (y * x)))) = x * (y * (z * (y * (x * C)))). [para(38(a,1),16(a,2))].

503 (0 / C) * (x * C) = x. [para(409(a,1),37(a,1,2,1)),rewrite([32(11),81(11),7(7),16(11,R),44(11),7(8)])].

504 (0 / C) \ x = x * C. [para(503(a,1),10(a,1,2))].

506 (0 / C) * x = x / C. [para(12(a,1),503(a,1,2))].

509 C * (x * (x / C)) = x * x. [para(503(a,1),13(a,2,2)),rewrite([506(4),16(5,R)])].

517 (x * x) / C = x * (x / C). [para(503(a,1),36(a,1,1,2)),rewrite([506(7)])].

518 ((x / (0 / C)) * y) / C = (x / C) * (y * C). [para(503(a,1),37(a,1,2,2)),rewrite([506(9),506(11)])].

562 (x * (C * (x * C))) \ (C * (x * (x * C))) = 0. [para(45(a,1),285(a,1,1))].

575 (x * (x / C)) * y = x * ((x * y) / C). [para(506(a,1),13(a,1,1,2)),rewrite([506(9)])].

576 ((x * (0 / C)) / C) * y = (x * (y / C)) / C. [para(506(a,1),13(a,1,1)),rewrite([506(14),506(14)])].

579 ((0 / C) / C) * x = (x / C) / C. [para(506(a,1),32(a,1,1)),rewrite([506(13),506(12)])].

590 x * (C * y) = x * (y * C). [para(46(a,1),10(a,1,2)),rewrite([10(7)]),flip(a)].

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

662 (C * (x * (C * C))) * y = C * (C * (C * (x * y))). [para(47(a,1),63(a,2,1)),rewrite([47(7),77(6)]),flip(a)].

670 C * (C * (C * (C * x))) = C * (x * (C * (C * C))). [para(89(a,2),47(a,2,2,2)),rewrite([299(8,R),16(7,R)])].

725 C * ((x / C) * (y * (x / C))) = (x / C) * (y * x). [para(12(a,1),48(a,2,2,2))].

734 (x * (C * (y * (z * y)))) * a(x,y,z * (y * C)) = (x * y) * (z * (y * C)). [para(48(a,2),18(a,1,1,2))].

736 (x * y) * (z * (C * (x * y))) = C * ((x * y) * (z * (x * y))). [para(48(a,2),18(a,2)),rewrite([16(3,R),16(9,R),18(12)])].

744 (C * x) * (y * (C * (x * C))) = C * ((x * C) * (y * (x * C))). [para(48(a,2),63(a,2)),rewrite([16(6,R)])].

747 C * ((C * x) * (y * (C * x))) = C * ((x * C) * (y * (x * C))). [para(63(a,1),48(a,2,2,2)),rewrite([16(14,R),744(16)])].

795 x * (0 / C) = x / C. [para(48(a,2),506(a,1)),rewrite([506(9),44(8),16(9,R),44(9),8(6)])].

798 C * (C * (x * (C * (y * (C * (C * x)))))) = C * (x * (C * (y * (C * (C * (C * x)))))). [para(48(a,2),47(a,1)),rewrite([47(11),16(20,R)])

807 (x * (y / C)) / C = ((x / C) / C) * y. [back_rewrite(576),rewrite([795(4)]),flip(a)].

812 x \ (x / C) = 0 / C. [para(795(a,1),10(a,1,2))].

813 (x / C) / (0 / C) = x. [para(795(a,1),11(a,1,1))].

815 (x * (y * x)) / C = x * (y * (x / C)). [para(795(a,1),13(a,1)),rewrite([795(8)])].

820 (x * C) \ x = 0 / C. [para(795(a,1),103(a,1,2)),rewrite([43(6)])].

821 (x * (y * (x / C))) / (0 / C) = x * (y * x). [para(795(a,1),36(a,1,1,2,2))].

823 (x / C) / (x \ (0 / C)) = x * x. [para(795(a,1),162(a,1,1))].

828 x / (0 / C) = x * C. [para(11(a,1),813(a,1,1))].

829 C * (x * (y * (x / C))) = x * (y * x). [back_rewrite(821),rewrite([828(8),16(6,R)])].

830 ((x * C) * y) / C = (x / C) * (y * C). [back_rewrite(518),rewrite([828(4)])].

911 (C * (x * (C * C))) \ (C * (C * x)) = 0 / C. [para(47(a,1),820(a,1,1))].

912 (C * (x * (y * x))) \ z = (x * (y * (x * C))) \ z. [para(13(a,1),237(a,2,1))].

914 (C * (C * x)) \ y = (C * (x * C)) \ y. [para(63(a,1),237(a,2,1)),rewrite([16(9,R)])].

928 (x * (C * C)) / C = x * C. [para(299(a,1),10(a,1,2)),rewrite([80(6)])].

929 x \ (C * (x * C)) = C * C. [para(299(a,2),10(a,1,2))].

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

934 (x * (C * C)) * y = C * (x * (C * y)). [para(299(a,1),13(a,1,1))].

935 C * (x * (C * (y * C))) = C * (x * (y * (C * C))). [para(299(a,1),13(a,2,2,2)),rewrite([13(7)])].

939 C * (C * x) = x * (C * C). [para(16(a,2),299(a,1,2))].

955 (C * (x * C)) \ (x * (C * C)) = 0. [para(299(a,1),285(a,1,2)),rewrite([16(4,R)])].

959 x * ((y / x) * (C * (x * C))) = C * (C * (x * y)). [para(299(a,2),37(a,1,2,2)),rewrite([299(12,R),16(11,R)])].

960 (x * (C * C)) / x = C * C. [para(299(a,1),162(a,1,1)),rewrite([80(8),11(8)])].

978 (C * (x * C)) \ y = (x * (C * C)) \ y. [para(299(a,1),237(a,1,1)),rewrite([16(9,R)]),flip(a)].

1011 (0 / C) / C = 0 / (C * C). [para(504(a,1),396(a,1,2)),rewrite([795(5),28(3),795(12)]),flip(a)].

1019 (0 / (C * C)) * x = (x / C) / C. [back_rewrite(579),rewrite([1011(5)])].

1031 (C * x) * (x * y) = x * (x * (y * C)). [para(509(a,1),25(a,1,1)),rewrite([32(4),575(10),71(12)]),flip(a)].

1032 (C * x) * x = C * (x * x). [para(509(a,1),25(a,2,2)),rewrite([16(6,R),44(6)])].

1062 (x * C) * x = C * (x * x). [para(11(a,1),517(a,2,2)),rewrite([76(5),43(7)]),flip(a)].

1070 (x * (y * C)) / (C * y) = x. [para(590(a,1),11(a,1,1))].

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

1072 (x / (C * y)) * (y * C) = x. [para(590(a,1),12(a,1))].

1073 (x / (y * C)) * (C * y) = x. [para(590(a,2),12(a,1))].

1083 (x * C) * (C * y) = C * (C * (x * y)). [para(590(a,1),63(a,1)),rewrite([25(5)]),flip(a)].

1100 x * (C * (C * (C * y))) = x * (C * (y * (C * C))). [para(47(a,1),590(a,2,2))].

1104 C * ((x * C) * (y * (C * x))) = C * ((x * C) * (y * (x * C))). [para(590(a,2),48(a,1,2,2)),rewrite([16(14,R),736(16)])].

1106 x * (C * (y * C)) = x * (y * (C * C)). [para(299(a,1),590(a,1,2)),rewrite([16(9,R)]),flip(a)].

1117 C * (x / (C * C)) = x / C. [para(12(a,1),928(a,1,1)),rewrite([16(8,R)]),flip(a)].

1122 (x * y) \ ((x * z) * (z \ y)) = a(x,z,z \ y). [para(53(a,1),10(a,1,2))].

1128 (C * x) * (x \ y) = x * ((C / x) * y). [para(16(a,1),53(a,2,1)),rewrite([53(6),340(8)])].

1130 (x * C) * (y / C) = C * ((x / C) * y). [para(16(a,2),53(a,2,1)),rewrite([80(4),99(6),80(9),357(10)])].

1188 (x / C) \ (C * x) = C * C. [para(12(a,1),929(a,1,2,2))].

1190 x \ (C * (C * x)) = C * C. [para(16(a,2),929(a,1,2,2))].

1201 (C * x) / (C * C) = x / C. [para(12(a,1),931(a,1,1,2))].

1204 C * (C * (x * (y * x))) = x * (y * (C * (C * x))). [para(939(a,2),13(a,2,2,2)),rewrite([299(6,R),16(5,R)])].

1234 (x * ((x \ y) * z)) \ (y * z) = a(x,x \ y,z). [para(9(a,1),54(a,1,2,1))].

1236 (x * y) \ ((x * (y / z)) * z) = a(x,y / z,z). [para(12(a,1),54(a,1,1,2))].

1239 (x * (y * (z * (y * u)))) \ ((x * (y * (z * y))) * u) = a(x,y * (z * y),u). [para(13(a,1),54(a,1,1,2))].

1244 (x * (C * y)) \ (C * (x * y)) = a(x,y,C). [para(16(a,2),54(a,1,1,2)),rewrite([16(6,R)])].

1253 (C * (x * (y * C))) \ (C * (C * (x * y))) = a(C,x,y * C). [para(25(a,1),54(a,1,2))].

1256 a(x,x,y) = 0. [para(32(a,1),54(a,1,2)),rewrite([27(5)]),flip(a)].

1262 (x * ((C * y) * z)) \ ((x * (y * C)) * z) = a(x,y * C,z). [para(63(a,2),54(a,1,1,2))].

1275 a(x,C,x) = 0. [para(90(a,2),54(a,1,1)),rewrite([1062(6),27(7)]),flip(a)].

1320 a(x,C * C,y) = a(x,C * y,C). [para(299(a,2),54(a,1,2,1)),rewrite([32(4),13(10),1244(11)]),flip(a)].

1324 x \ (x \ (C * ((x / C) * x))) = a(C,x,x / C). [para(509(a,1),54(a,1,1)),rewrite([357(6),380(7)])].

1327 a(x,C * y,z) = a(x,y * C,z). [para(590(a,1),54(a,1,2,1)),rewrite([1262(9)]),flip(a)].

1328 (x * (y * (C * z))) \ ((x * y) * (z * C)) = a(x,y,C * z). [para(590(a,1),54(a,1,2))].

1329 a(x,y,C * z) = a(x,y,z * C). [para(590(a,2),54(a,1,1,2)),rewrite([1328(9)])].

1334 a(x,x * C,C) = 0. [back_rewrite(562),rewrite([1244(11)])].

1335 (x / C) * x = x * (x / C). [para(1275(a,1),53(a,1,2)),rewrite([80(2),8(5),80(5),16(7,R),44(7),80(5)])].

1336 a(C,x,x / C) = 0. [back_rewrite(1324),rewrite([1335(4),509(5),10(2),27(1)]),flip(a)].

1346 C * ((x / C) * (x / C)) = x * (x / C). [back_rewrite(196),rewrite([1335(10)])].

1347 (x / C) * (C * x) = x * x. [back_rewrite(191),rewrite([1335(9),509(10)])].

1408 a(x / C,x,C) = 0. [para(12(a,1),1334(a,1,2))].

1418 a(C,C * x,x) = 0. [para(43(a,1),1336(a,1,3))].

1464 C * (x * (C * a(C,(C * x) / y,y))) = (C * ((C * x) / y)) * y. [para(56(a,1),47(a,1)),flip(a)].

1487 ((x / C) / C) * x = (x / C) * (x / C). [para(1408(a,1),56(a,1,2)),rewrite([8(7),1335(12),16(14,R),509(14)])].

1519 C * ((x / (C * y)) * y) = C * ((x / (y * C)) * y). [para(16(a,2),57(a,2,1,1,2)),rewrite([57(6),16(6,R),16(12,R)]),flip(a)].

1705 x / (x / (C * C)) = C * C. [para(12(a,1),960(a,1,1))].

1723 (C * x) \ (C * (x * x)) = x. [para(1032(a,1),10(a,1,2))].

1724 (C * (x * x)) / x = C * x. [para(1032(a,1),11(a,1,1))].

1725 (x * (C * (x * x))) * y = x * (x * (x * (y * C))). [para(1032(a,1),13(a,1,1,2)),rewrite([1031(9)])].

1818 x / (C * y) = x / (y * C). [para(12(a,1),1070(a,1,1))].

2033 x \ (C * ((x / (C * y)) * y)) = a(x / (C * y),y,C). [para(1072(a,1),54(a,1,1)),rewrite([16(6,R)])].

2046 C * (C * (x / (y * C))) = (C * x) / y. [para(1073(a,1),36(a,1,1,2)),rewrite([16(9,R)]),flip(a)].

2225 (x / C) / C = x / (C * C). [para(1117(a,1),10(a,1,2)),rewrite([80(4)])].

2229 C * (C * ((x / (C * C)) * y)) = (x / C) * (y * C). [para(1117(a,1),25(a,1,1)),flip(a)].

2231 C * ((x / (C * C)) * (x / (C * C))) = (x / (C * C)) * (x / C). [para(1117(a,1),90(a,2,2))].

2233 (C * x) * (y / (C * C)) = C * ((x / C) * (y / C)). [para(1117(a,1),37(a,1,2,2)),flip(a)].

2239 C * ((x / (C * C)) * (x / C)) = (x / (C * C)) * x. [para(1117(a,1),48(a,1,2,2)),rewrite([16(20,R),1117(20),44(17)])].

2249 a(C,x / C,x / (C * C)) = 0. [para(1117(a,1),1418(a,1,2))].

2252 (x / (C * C)) * (x / C) = (x / C) * (x / (C * C)). [para(1117(a,1),1032(a,1,1)),rewrite([2231(18)]),flip(a)].

2256 (x / (C * C)) * x = (x / C) * (x / C). [back_rewrite(1487),rewrite([2225(4)])].

2260 (0 / (C * C)) * x = x / (C * C). [back_rewrite(1019),rewrite([2225(10)])].

2265 (x * (y / C)) / C = (x / (C * C)) * y. [back_rewrite(807),rewrite([2225(9)])].

2267 C * ((x / C) * (x / (C * C))) = (x / C) * (x / C). [back_rewrite(2239),rewrite([2252(8),2256(14)])].

2275 (x * x) / (C * C) = (x / C) * (x / C). [para(1188(a,1),162(a,1,2)),rewrite([1347(5)])].

2290 (x * C) / (C * C) = x / C. [para(16(a,1),1201(a,1,1))].

2363 (x * x) / (C * x) = x / C. [para(1347(a,1),11(a,1,1))].

2393 (x * x) / (x * C) = x / C. [para(1347(a,1),1071(a,1,1))].

2662 (x / (C * C)) * ((x / C) * (y * C)) = (x / C) * ((x / C) * y). [para(1705(a,1),37(a,1,2,1)),rewrite([32(13),2229(13),2256(15),32(16)])]

2663 (C * (x * (y * x))) \ (C * (x * (y * (x * (x * (y * x)))))) = x * (y * x). [para(13(a,1),1723(a,1,2,2))].

2694 (C * x) \ (C * (C * y)) = C * (x \ y). [para(9(a,1),69(a,1,2,2,2)),rewrite([16(10,R)])].

2716 C * ((x * (y * C)) \ (x * y)) = a(C,x,y * C). [back_rewrite(1253),rewrite([2694(11)])].

2717 C * ((x * (C * C)) \ x) = 0 / C. [back_rewrite(911),rewrite([2694(11)])].

2723 C * ((x * C) \ (x * x)) = x. [back_rewrite(271),rewrite([2694(10)])].

2746 (C * (C * x)) / (y * C) = C * (x / y). [para(12(a,1),70(a,1,1,2,2))].

2773 (C * (C * x)) / (C * (C * y)) = C * (x / (y * C)). [para(1073(a,1),70(a,1,1,2,2)),rewrite([16(8,R)])].

2793 (x / C) * (C * y) = C * (x * (y / C)). [para(71(a,1),10(a,1,2)),rewrite([341(5)])].

2826 (C * x) * (y * (C * C)) = C * (C * (x * (y * C))). [para(928(a,1),71(a,1,2,2,2)),flip(a)].

2853 C * (C * (x * (y / (C * C)))) = C * ((x / C) * y). [para(2225(a,1),71(a,1,2,2,2)),rewrite([357(14)])].

2859 ((C * x) * y) / C = C * (x * (y / C)). [back_rewrite(355),rewrite([2793(10)])].

2873 (x * (y * (x * (x * (y * x))))) / (C * (x * (y * x))) = x * (y * (x / C)). [para(13(a,1),2363(a,1,1)),rewrite([815(14)])].

2945 (C * x) * (y * (C * (z * C))) = C * (C * (x * ((y * C) * z))). [para(73(a,1),37(a,1,2,2)),rewrite([2793(11),71(12),77(16)])].

3064 C * ((x * C) * (y * (x * C))) = C * (C * (x * ((y * C) * x))). [back_rewrite(744),rewrite([2945(8)]),flip(a)].

3071 C * ((x * C) * (y * (C * x))) = C * (C * (x * ((y * C) * x))). [back_rewrite(1104),rewrite([3064(16)])].

3073 C * ((C * x) * (y * (C * x))) = C * (C * (x * ((y * C) * x))). [back_rewrite(747),rewrite([3064(16)])].

3314 (x / C) * ((C * y) * x) = (C * x) * ((y / C) * x). [para(71(a,1),74(a,2,2)),rewrite([357(8),2793(9),71(10)]),flip(a)].

3339 (x * C) \ (x * x) = x / C. [para(2723(a,1),10(a,1,2)),rewrite([80(2)]),flip(a)].

3477 (C * x) \ (x * x) = x / C. [para(16(a,2),3339(a,1,1))].

3658 (x * (C * (C * (C * (y * z))))) * a(x,C * (C * (C * y)),z) = (x * (C * (C * (C * y)))) * z. [para(77(a,1),60(a,1,1,2,2)),rewrite([16(13

,R),16(21,R)])].

3665 C * (C * (C * ((x * (y * z)) * a(C * (C * (C * x)),y,z)))) = C * (C * (C * ((x * y) * z))). [para(77(a,1),61(a,1,1,2)),rewrite([16(13,R

),47(16),77(15),77(22),47(24),77(23)])].

3668 (x / C) * (y * C) = C * (x * (y / C)). [para(1117(a,1),77(a,1,1)),rewrite([2793(5),2229(14)]),flip(a)].

3688 (x / (C * C)) * (C * (x * (y / C))) = (x / C) * ((x / C) * y). [back_rewrite(2662),rewrite([3668(9)])].

3689 C * (C * ((x / (C * C)) * y)) = C * (x * (y / C)). [back_rewrite(2229),rewrite([3668(14)])].

3690 ((x * C) * y) / C = C * (x * (y / C)). [back_rewrite(830),rewrite([3668(10)])].

3767 C * ((C * (C * (x * y))) \ ((C * x) * y)) = a(C,C * x,y * C). [para(78(a,1),103(a,1,2)),rewrite([16(7,R),25(14),2694(15)])].

3956 C * (x * (C * a(C * (x / (y * C)),C * y,C))) = C * (C * (C * ((x / (y * C)) * y))). [para(1073(a,1),79(a,1,2,1)),rewrite([77(23)])].

3987 (x / C) * (x / C) = x * (x / (C * C)). [para(2249(a,1),18(a,1,2)),rewrite([2267(9),8(7),44(9)])].

4006 (x * x) / (C * C) = x * (x / (C * C)). [back_rewrite(2275),rewrite([3987(10)])].

4009 (x / (C * C)) * x = x * (x / (C * C)). [back_rewrite(2256),rewrite([3987(10)])].

4012 C * (x * (x / (C * C))) = x * (x / C). [back_rewrite(1346),rewrite([3987(6)])].

4033 (x * (y * C)) / C = C * ((x / C) * y). [para(81(a,1),10(a,1,2)),rewrite([80(5)])].

4051 (x * (C * (C * C))) * y = C * (C * (C * (x * y))). [para(81(a,1),38(a,1,1)),rewrite([16(5,R),2793(16),43(14)])].

4290 (x * (x / (C * C))) * y = x * ((x * y) / (C * C)). [para(506(a,1),87(a,1,1,2,2)),rewrite([506(6),2225(4),506(14),506(13),2225(11)])].

4384 (x / C) * ((x / C) * y) = x * ((x * y) / (C * C)). [para(1117(a,1),87(a,1,1,2,2)),rewrite([44(8),4009(5),4290(6),3689(19),3688(16)]),fl

ip(a)].

4540 (0 / x) * ((0 / x) * y) = ((0 / x) / x) * y. [para(411(a,1),18(a,2,1)),rewrite([1256(11),8(8)])].

4549 (0 / x) * (C * ((0 / x) / x)) = C * ((0 / x) * ((0 / x) / x)). [para(411(a,1),48(a,1,2,2)),rewrite([16(16,R),90(17,R),411(16)]),flip(a)

4551 (0 / x) * ((0 / x) / C) = ((0 / x) / x) / C. [para(411(a,1),517(a,1,1)),flip(a)].

4565 (C * ((0 / x) / x)) / (0 / x) = C * (0 / x). [para(411(a,1),1724(a,1,1,2))].

4574 (C * (0 / x)) \ ((0 / x) / x) = (0 / x) / C. [para(411(a,1),3339(a,1,2)),rewrite([16(4,R)])].

4891 ((0 / C) / x) * ((0 / C) / x) = (((0 / C) / x) / C) / x. [para(31(a,1),823(a,1,2)),flip(a)].

5295 C * (x * ((y * (C * x)) / C)) = (C * x) * (y * x). [para(105(a,1),795(a,1)),rewrite([795(8),43(6),3690(12)]),flip(a)].

5304 (C * x) * (y * (C * (x * (x * (C * (y * (C * x))))))) = C * ((C * x) * (y * (C * (x * (x * (C * (y * x))))))). [para(105(a,1),509(a,1,2

)),rewrite([3690(13),5295(13),178(10),105(26),121(24)]),flip(a)].

5323 C * (C * ((C * x) * (y * (C * (x * (x * (C * (y * x)))))))) = C * (C * (C * (x * ((y * C) * (x * (x * ((y * C) * x))))))). [para(105(a,

1),1032(a,2,2)),rewrite([3071(8),47(15),3071(13),736(14),90(13,R),13(12),121(27),5304(29)]),flip(a)].

5343 (x * C) * (y * (C * x)) = C * (x * ((y * C) * x)). [para(105(a,1),1723(a,1,2,2)),rewrite([3071(8),121(20),5304(22),5323(23),2694(24),26

63(19)]),flip(a)].

5350 C * (x * (C * ((y / C) * x))) = x * ((y * C) * x). [para(105(a,1),2393(a,1,2)),rewrite([5343(6),5343(12),77(13),13(11),16(19,R),736(21)

,3073(21),2773(22),16(16,R),2873(17),1130(6),5343(14),43(16)])].

5369 (C * x) * (y * (C * (C * (x * z)))) = C * (C * (x * ((y * C) * (x * z)))). [para(77(a,1),105(a,2,2,2)),rewrite([5343(6),77(9),13(7)]),f

lip(a)].

5481 (C * x) * (y * (C * x)) = C * (x * ((y * C) * x)). [back_rewrite(297),rewrite([5369(9),2746(12),36(7)]),flip(a)].

5521 (x * C) * (y * (x * C)) = C * (x * ((y * C) * x)). [back_rewrite(305),rewrite([5481(6)]),flip(a)].

5565 (C * x) * (y * (x * C)) = C * (x * ((y * C) * x)). [para(8(a,1),106(a,1,2,2)),rewrite([5481(6),8(12)]),flip(a)].

5714 C * ((x * (x * (x * (C * y)))) * (C * a(C * (C * (x * x)),x * C,y))) = (x * (x * (C * (x * (C * C))))) * y. [para(106(a,2),92(a,1,1)),r

ewrite([178(8),77(9),77(14),47(18),1031(25),1031(26),16(24,R)])].

5915 (x * (x * (C * (x * (C * C))))) * y = C * (x * (x * (x * (C * (C * y))))). [para(108(a,2),92(a,1,1)),rewrite([122(8),1083(9),76(14),47(

18),5714(18),76(16),1083(17),47(18),1725(17),16(14,R)])].

5929 (C * x) \ ((x * C) \ (x * (x * (C * C)))) = 0. [para(32(a,1),955(a,1,2)),rewrite([16(4,R),387(11)])].

6568 a(x,y * (z * (y * C)),C) = a(x,C * C,y * (z * y)). [para(48(a,1),1320(a,2,2)),flip(a)].

6574 a(x,C * (C * y),C) = a(x,C * C,y * C). [para(590(a,2),1320(a,2,2)),flip(a)].

6584 a(x,C * C,y / (C * C)) = a(x,y / C,C). [para(1117(a,1),1320(a,2,2))].

7068 (x * (C * (C * (C * y)))) * z = (x * (C * (y * (C * C)))) * z. [para(47(a,1),113(a,2,1,2)),rewrite([47(7),77(6),16(14,R),3658(16)])].

7779 a(x,C * (C * (C * y)),z) = a(x,C * (y * (C * C)),z). [para(47(a,1),1327(a,2,2))].

8094 (0 / x) * (C * ((0 / x) * y)) = (C * ((0 / x) / x)) * y. [para(411(a,1),124(a,1,1,2)),flip(a)].

8139 (x * (C * (x * ((y * C) * z)))) * a(C * (x * x),C * y,z) = C * ((x * (x * y)) * (C * z)). [para(124(a,1),110(a,1,1)),rewrite([77(20),32

(18),47(21)])].

8140 (x * (C * (x * (C * y)))) * z = C * ((x * (x * y)) * (C * z)). [para(124(a,1),110(a,2,1)),rewrite([124(7),8139(14)]),flip(a)].

8222 x * ((x * (y * x)) \ z) = y \ (x \ z). [para(125(a,1),10(a,1,2)),flip(a)].

8246 x * (C * (C * ((x * C) \ 0))) = C. [para(147(a,1),125(a,2)),rewrite([5521(8),2694(13),1083(10),8222(8),27(5)])].

8376 ((x * y) / (C * C)) \ ((x / (C * C)) * y) = a(0 / (C * C),x,y). [para(2260(a,1),54(a,1,1)),rewrite([2260(11)])].

8780 (x * (C * C)) \ x = 0 / (C * C). [para(2717(a,1),10(a,1,2)),rewrite([80(5),2225(5)]),flip(a)].

9448 ((x \ 0) * y) / (x * ((x \ 0) * y)) = x \ 0. [para(8(a,1),181(a,1,1,1))].

10120 C * (C * ((x * C) \ 0)) = x \ C. [para(8246(a,1),10(a,1,2)),flip(a)].

10128 C * (x \ (0 / C)) = (C * x) \ C. [para(8246(a,1),102(a,1,2)),rewrite([16(10,R),8222(13),80(8)]),flip(a)].

10163 x \ (x / (C * C)) = 0 / (C * C). [para(12(a,1),8780(a,1,1))].

10637 C * ((x * C) \ 0) = (x \ C) / C. [para(10120(a,1),10(a,1,2)),rewrite([80(4)]),flip(a)].

10638 C * (C * (x \ 0)) = (x / C) \ C. [para(12(a,1),10120(a,1,2,2,1))].

10644 C * (((x * C) \ 0) * ((x \ C) / C)) = ((x * C) \ 0) * (x \ C). [para(10120(a,1),49(a,2,2)),rewrite([10637(11)])].

10647 ((x * C) \ 0) \ (x \ C) = C * C. [para(10120(a,1),1190(a,1,2))].

10669 ((C * x) \ C) / C = x \ (0 / C). [para(10128(a,1),10(a,1,2)),rewrite([80(6)])].

10674 (C * ((0 / C) / x)) \ C = C * x. [para(31(a,1),10128(a,1,2)),flip(a)].

10677 C * (x \ (x \ (0 / C))) = (x * (x * C)) \ C. [para(89(a,1),10128(a,2,1)),rewrite([380(6)])].

10679 (x * (C * x)) \ C = (x * (x * C)) \ C. [para(90(a,1),10128(a,2,1)),rewrite([380(6),10677(7)]),flip(a)].

10743 x * (0 / (C * C)) = x / (C * C). [para(10163(a,1),9(a,1,2))].

10915 (x \ C) / (C * C) = (x * C) \ 0. [para(10637(a,1),10(a,1,2)),rewrite([80(6),2225(6)])].

10917 ((x / C) \ C) / C = C * (x \ 0). [para(12(a,1),10637(a,1,2,1)),flip(a)].

10918 ((x * C) \ 0) * (C * (((x * C) \ 0) * y)) = (((x * C) \ 0) * ((x \ C) / C)) * y. [para(10637(a,1),13(a,1,1,2)),flip(a)].

10920 C * ((C * x) \ 0) = (x \ C) / C. [para(16(a,2),10637(a,1,2,1))].

10926 C * (((x * C) \ 0) * ((x * C) \ 0)) = ((x * C) \ 0) * ((x \ C) / C). [para(10637(a,1),90(a,2,2))].

10947 ((x * C) \ 0) * ((x \ C) / C) = ((x \ C) / C) * ((x * C) \ 0). [para(10637(a,1),1032(a,1,1)),rewrite([10926(20)]),flip(a)].

10995 C * (((x * C) \ 0) * ((x * C) \ 0)) = ((x \ C) / C) * ((x * C) \ 0). [back_rewrite(10926),rewrite([10947(20)])].

10996 ((x * C) \ 0) * (C * (((x * C) \ 0) * y)) = (((x \ C) / C) * ((x * C) \ 0)) * y. [back_rewrite(10918),rewrite([10947(21)])].

10997 C * (((x \ C) / C) * ((x * C) \ 0)) = ((x * C) \ 0) * (x \ C). [back_rewrite(10644),rewrite([10947(10)])].

11009 ((0 / x) / C) \ C = C * (C * x). [para(31(a,1),10638(a,1,2,2)),flip(a)].

11017 C * ((x \ 0) * (C * y)) = ((x / C) \ C) * y. [para(10638(a,1),37(a,2,1)),rewrite([43(7)])].

11028 C * (C * ((x \ 0) * (x \ 0))) = (x \ 0) * ((x / C) \ C). [para(10638(a,1),49(a,2,2)),rewrite([90(8,R)])].

11030 ((x / C) \ C) / ((C * (x \ 0)) \ C) = (x \ 0) * ((x / C) \ C). [para(10638(a,1),396(a,1,1)),rewrite([77(20),11028(20)])].

11046 (x \ 0) \ ((x / C) \ C) = C * C. [para(10638(a,1),1188(a,1,2)),rewrite([43(6)])].

11689 (((x * C) \ 0) * (x \ C)) / (C * C) = ((x * C) \ 0) * ((x * C) \ 0). [para(10647(a,1),162(a,1,2))].

12028 (x / C) \ (0 / C) = (x \ C) / C. [para(9(a,1),10669(a,1,1,1)),rewrite([80(6)]),flip(a)].

12029 ((x * (C * x)) \ C) / C = x \ (x \ (0 / C)). [para(90(a,1),10669(a,1,1,1)),rewrite([380(12)])].

12084 C * ((0 / C) / x) = C / (C * x). [para(10674(a,1),30(a,1,2)),flip(a)].

12781 (C * (C / x)) \ 0 = x / (C * C). [para(31(a,1),10915(a,1,1)),rewrite([16(8,R)]),flip(a)].

13068 C * ((x * (C * x)) \ 0) = (x \ (x \ C)) / C. [para(90(a,1),10920(a,1,2,1)),rewrite([380(10)])].

13729 a(C,x,x * C) = 0. [para(207(a,1),103(a,1,2)),rewrite([16(5,R),1031(10),387(11),5929(11)]),flip(a)].

13806 (((x * C) \ 0) * (x \ C)) * a(C,(x * C) \ 0,(x \ C) / C) = (x \ C) * ((x * C) \ 0). [para(10637(a,1),207(a,2,1)),rewrite([10995(12),10

997(11),16(18,R),10637(18),16(28,R),10637(28),3987(27),10915(26)])].

13816 a(C,x,C * x) = 0. [para(16(a,2),13729(a,1,3))].

13854 a(C,(x * C) \ 0,(x \ C) / C) = 0. [para(10637(a,1),13816(a,1,3))].

13862 ((x * C) \ 0) * (x \ C) = (x \ C) * ((x * C) \ 0). [back_rewrite(13806),rewrite([13854(17),8(9)])].

13865 ((x \ C) * ((x * C) \ 0)) / (C * C) = ((x * C) \ 0) * ((x * C) \ 0). [back_rewrite(11689),rewrite([13862(7)])].

14746 (C * ((0 / x) * ((0 / x) / x))) / (C * (0 / x)) = (0 / x) / x. [para(411(a,1),214(a,1,1,2,2)),rewrite([4549(8),16(12,R),411(18)])].

14790 C / (C * (C * x)) = (0 / x) / C. [para(11009(a,1),30(a,1,2))].

14868 ((x \ 0) * ((x / C) \ C)) / (C * C) = (x \ 0) * (x \ 0). [para(11046(a,1),162(a,1,2))].

15144 (x / C) * ((x \ C) / C) = 0 / C. [para(12028(a,1),9(a,1,2))].

15145 (0 / C) / ((x \ C) / C) = x / C. [para(12028(a,1),30(a,1,2))].

15173 (C / (C * x)) / C = (0 / C) / x. [para(12084(a,1),10(a,1,2)),rewrite([80(6)])].

15174 (C / (C * x)) / ((0 / C) / x) = C. [para(12084(a,1),11(a,1,1))].

15175 ((0 / C) / x) * (C * (((0 / C) / x) * y)) = (((0 / C) / x) * (C / (C * x))) * y. [para(12084(a,1),13(a,1,1,2)),flip(a)].

15178 ((0 / C) / x) \ (C / (C * x)) = C. [para(12084(a,1),41(a,1,2))].

15180 ((0 / C) / x) * (C / (C * x)) = C * ((((0 / C) / x) / C) / x). [para(12084(a,1),90(a,2,2)),rewrite([4891(10)]),flip(a)].

15193 C / (C * (x * C)) = (0 / x) / C. [para(590(a,1),12084(a,2,2)),rewrite([12084(8),14790(6)]),flip(a)].

15195 C / (x * (C * C)) = (0 / x) / C. [para(939(a,1),12084(a,2,2)),rewrite([12084(8),14790(6)]),flip(a)].

15255 ((0 / C) / x) * (C * (((0 / C) / x) * y)) = (C * ((((0 / C) / x) / C) / x)) * y. [back_rewrite(15175),rewrite([15180(21)])].

15556 0 / (x / (C * C)) = C * (C / x). [para(12781(a,1),30(a,1,2))].

15871 (0 / (x / C)) / C = C / (C * x). [para(9(a,1),14790(a,1,2,2)),rewrite([80(7)]),flip(a)].

15906 ((x / C) * (y / C)) / ((x \ C) / C) = (x / C) * (y * (x / C)). [para(15144(a,1),36(a,1,1,2,2)),rewrite([795(6)])].

15932 (0 / C) / (x / C) = (C / x) / C. [para(31(a,1),15145(a,1,2,1))].

15935 (C / (x * C)) / C = (0 / C) / x. [para(16(a,1),15173(a,1,1,2))].

15947 (0 / C) / (x / (C * C)) = (C / (x / C)) / C. [para(1117(a,1),15173(a,1,1,2)),flip(a)].

16029 (C / (x * C)) / ((0 / C) / x) = C. [para(16(a,1),15174(a,1,1,2))].

16056 ((0 / C) / x) \ (C / (x * C)) = C. [para(16(a,1),15178(a,1,2,2))].

16098 ((0 / x) / C) * (x * (C * C)) = C. [para(15195(a,1),12(a,1,1))].

16126 C * (C / (C * x)) = 0 / (x / C). [para(1201(a,1),15556(a,1,2)),flip(a)].

16128 C * (C / (x * C)) = 0 / (x / C). [para(1818(a,1),15556(a,2,2)),rewrite([1201(7)]),flip(a)].

16184 (0 / (x / C)) * (C / (C * x)) = (C / (C * x)) * (0 / (x / C)). [para(15871(a,1),1335(a,1,1)),rewrite([15871(19)]),flip(a)].

16275 ((0 / C) / x) * (C / (x * C)) = (C / (x * C)) * ((0 / C) / x). [para(15935(a,1),1335(a,1,1)),rewrite([15935(19)])].

16313 ((C / (x * C)) * ((0 / C) / x)) * y = (C * ((((0 / C) / x) / C) / x)) * y. [para(16029(a,1),37(a,1,2,1)),rewrite([15255(12),16275(19)]

),flip(a)].

16330 (C / (x * C)) / (((0 / C) / x) \ C) = (((0 / C) / x) / C) / x. [para(16056(a,1),386(a,1,2,2)),rewrite([4891(20)])].

16345 x * (((0 / x) / C) * x) = x / C. [para(16098(a,1),36(a,1,1,2)),rewrite([2290(6)]),flip(a)].

16370 C * ((x / C) * (0 / x)) = x * (0 / x). [para(16098(a,1),87(a,2,2,2)),rewrite([4384(10),12(5),10743(8),299(11,R),16(10,R),2853(11),16(1

3,R),44(13)])].

16463 (C / (C * x)) * (C / (C * x)) = (0 / (x / C)) / (C * x). [para(16126(a,1),396(a,1,1)),rewrite([31(10)]),flip(a)].

16472 (C / (C * x)) * (0 / (x / C)) = C * ((0 / (x / C)) / (C * x)). [para(16126(a,1),1032(a,1,1)),rewrite([16184(9),16463(19)])].

16515 ((C / (C * x)) * (C * ((0 / (x / C)) / (C * x)))) / (0 / (x / C)) = (0 / (x / C)) / (C * x). [para(16126(a,1),227(a,1,2)),rewrite([164

63(14),16463(28)])].

16541 (0 / (x / C)) * (C / (C * x)) = C * ((0 / (x / C)) / (C * x)). [back_rewrite(16184),rewrite([16472(18)])].

16548 C * ((C / (x * C)) * (C / (x * C))) = (C / (x * C)) * (0 / (x / C)). [para(16128(a,1),90(a,2,2))].

16558 (C / (x * C)) * (C / (x * C)) = (0 / (x / C)) / (x * C). [para(16128(a,1),396(a,1,1)),rewrite([31(10)]),flip(a)].

16574 (C * ((0 / (x / C)) / (x * C))) / (C / (x * C)) = 0 / (x / C). [para(16128(a,1),1724(a,2)),rewrite([16558(10)])].

16580 (0 / (x / C)) \ ((0 / (x / C)) / (x * C)) = (0 / C) / x. [para(16128(a,1),3477(a,1,1)),rewrite([16558(13),15935(18)])].

16626 ((C / (x * C)) * (C * ((0 / (x / C)) / (x * C)))) / (0 / (x / C)) = (0 / (x / C)) / (x * C). [para(16128(a,1),227(a,1,2)),rewrite([165

58(14),16558(28)])].

16628 (C / (x * C)) * (0 / (x / C)) = C * ((0 / (x / C)) / (x * C)). [back_rewrite(16548),rewrite([16558(10)]),flip(a)].

16710 ((0 / x) / C) * x = 0 / C. [para(16345(a,1),10(a,1,2)),rewrite([812(3)]),flip(a)].

16745 ((0 / x) \ C) / C = x. [para(16710(a,1),10(a,1,2)),rewrite([12028(8)])].

16746 (0 / C) / x = (0 / x) / C. [para(16710(a,1),11(a,1,1))].

16748 (0 / x) * (x * C) = C. [para(16710(a,1),25(a,2,2,2)),rewrite([44(6),795(11),28(9),8(8)])].

16749 (x / C) * (x \ 0) = 0 / C. [para(30(a,1),16710(a,1,1,1))].

16771 (0 / x) * (C * x) = C. [para(16710(a,1),77(a,2,2,2)),rewrite([44(6),795(11),28(9),8(8)])].

16864 (C / x) / C = C / (C * x). [back_rewrite(15871),rewrite([16746(6,R),15932(6)])].

16911 (0 / C) / (x / (C * C)) = C / x. [back_rewrite(15947),rewrite([16864(14),44(13)])].

16978 (0 / x) \ C = x * C. [para(16745(a,1),12(a,1,1)),flip(a)].

16979 (x \ C) / C = x \ 0. [para(30(a,1),16745(a,1,1,1))].

16980 (x \ (x \ C)) / C = x \ (x \ 0). [para(386(a,1),16745(a,1,1,1)),rewrite([380(3)])].

16981 C * (x \ 0) = x \ C. [para(16745(a,1),10638(a,2,1)),rewrite([16978(6),10637(7),16979(5)])].

16983 (x * C) \ C = x \ 0. [para(16745(a,1),10917(a,1,1,1)),rewrite([16979(4),16978(7),16981(8)]),flip(a)].

16988 x \ (0 / C) = (x \ 0) / C. [para(16745(a,1),12028(a,1,1)),rewrite([16978(8),16983(8)])].

17016 ((x / C) * (y / C)) / (x \ 0) = (x / C) * (y * (x / C)). [back_rewrite(15906),rewrite([16979(9)])].

17149 (x * (C * x)) \ 0 = x \ ((x \ 0) / C). [back_rewrite(12029),rewrite([16979(7),16988(9)])].

17155 ((x * C) \ 0) * (C * (((x * C) \ 0) * y)) = ((x \ 0) * ((x * C) \ 0)) * y. [back_rewrite(10996),rewrite([16979(16)])].

17156 C * (((x * C) \ 0) * ((x * C) \ 0)) = (x \ 0) * ((x * C) \ 0). [back_rewrite(10995),rewrite([16979(15)])].

17203 (C * x) \ C = x \ 0. [back_rewrite(10920),rewrite([16981(6),16979(8)])].

17221 C * (x \ ((x \ 0) / C)) = x \ (x \ 0). [back_rewrite(13068),rewrite([17149(6),16980(12)])].

17289 ((x / C) \ C) / ((x \ C) \ C) = (x \ 0) * ((x / C) \ C). [back_rewrite(11030),rewrite([16981(8)])].

17301 (x / C) \ C = C * (x \ C). [back_rewrite(10638),rewrite([16981(5)]),flip(a)].

17452 (x * (x * C)) \ C = x \ (x \ 0). [back_rewrite(10677),rewrite([16988(5),17221(7)]),flip(a)].

17547 (x \ 0) * (C * (x \ C)) = (x \ C) * (x \ C). [back_rewrite(17289),rewrite([17301(4),396(9),17301(11)]),flip(a)].

17563 (x \ C) * ((x * C) \ 0) = (x \ 0) * (x \ 0). [back_rewrite(14868),rewrite([17301(6),17547(7),4006(9),10915(8)])].

17581 C * ((x \ 0) * (C * y)) = (C * (x \ C)) * y. [back_rewrite(11017),rewrite([17301(11)])].

17587 (x * (C * x)) \ C = x \ (x \ 0). [back_rewrite(10679),rewrite([17452(10)])].

17615 ((x * C) \ 0) * ((x * C) \ 0) = (x \ 0) * ((x \ 0) / (C * C)). [back_rewrite(13865),rewrite([17563(7),4006(9)]),flip(a)].

17628 (x \ 0) * ((x * C) \ 0) = (x \ 0) * ((x \ 0) / C). [back_rewrite(17156),rewrite([17615(10),4012(11)]),flip(a)].

17634 ((x * C) \ 0) * (C * (((x * C) \ 0) * y)) = (x \ 0) * (((x \ 0) * y) / C). [back_rewrite(17155),rewrite([17628(19),575(20)])].

17649 C / (x * C) = 0 / x. [para(16748(a,1),11(a,1,1))].

17658 (C * (0 / x)) / (x * C) = (0 / x) / x. [para(16748(a,1),86(a,1,1,2)),rewrite([16(4,R),411(12)])].

17670 a(0 / x,x,C) = 0. [para(16748(a,1),54(a,1,1)),rewrite([12(4),16(4,R),8(4),27(3)]),flip(a)].

17675 C / (C * x) = 0 / x. [para(16748(a,1),1070(a,1,1))].

17722 C * ((0 / (x / C)) / (x * C)) = (0 / x) * (0 / (x / C)). [back_rewrite(16628),rewrite([17649(4)]),flip(a)].

17723 (0 / (x / C)) / (x * C) = (0 / x) / x. [back_rewrite(16626),rewrite([17649(4),17722(11),4540(10),11(13)]),flip(a)].

17741 0 / (x / C) = C * (0 / x). [back_rewrite(16574),rewrite([17723(8),17649(9),4565(8)]),flip(a)].

17743 (0 / x) / (((0 / C) / x) \ C) = (((0 / C) / x) / C) / x. [back_rewrite(16330),rewrite([17649(4)])].

17746 (C * ((((0 / C) / x) / C) / x)) * y = ((0 / x) * ((0 / C) / x)) * y. [back_rewrite(16313),rewrite([17649(4)]),flip(a)].

17797 (C / x) / C = 0 / x. [back_rewrite(16864),rewrite([17675(8)])].

17821 C * ((C * (0 / x)) / (C * x)) = C * ((0 / x) / x). [back_rewrite(16541),rewrite([17741(4),17675(8),1032(7),411(6),17741(10)]),flip(a)]

17822 (C * (0 / x)) / (C * x) = (0 / x) / x. [back_rewrite(16515),rewrite([17675(4),17741(7),17821(11),4549(8),17741(12),14746(13),17741(7)]

),flip(a)].

17874 (0 / x) / C = 0 / (x * C). [back_rewrite(15193),rewrite([17675(6)]),flip(a)].

17896 (0 / C) / x = 0 / (x * C). [back_rewrite(16580),rewrite([17741(4),17741(8),17658(11),4574(8),17874(4)]),flip(a)].

17936 (C * ((0 / (C * (x * C))) / x)) * y = (C * ((0 / (x * C)) / (x * C))) * y. [back_rewrite(15255),rewrite([17896(4),17896(9),8094(12),17

896(15),16746(17,R),17896(17),16(16,R)]),flip(a)].

17938 (C * ((0 / (x * C)) / (x * C))) * y = ((0 / x) * (0 / (x * C))) * y. [back_rewrite(17746),rewrite([17896(5),16746(7,R),17896(7),16(6,R

),17936(10),17896(16)])].

17940 (0 / (C * (x * C))) / x = (0 / x) / (C * (x * C)). [back_rewrite(17743),rewrite([17896(6),16978(8),16(6,R),17896(11),16746(13,R),17896

(13),16(12,R)]),flip(a)].

17943 (0 / (x * C)) / (x * C) = (0 / x) / (C * (x * C)). [back_rewrite(4891),rewrite([17896(4),17896(8),411(9),17896(11),16746(13,R),17896(1

3),16(12,R),17940(14)])].

18096 (0 / x) * (0 / (x * C)) = ((0 / x) / x) / C. [back_rewrite(4551),rewrite([17874(6)])].

18154 C * (0 / x) = C / x. [back_rewrite(16911),rewrite([17896(8),16(7,R),1117(7),17741(4)])].

18203 (C * ((0 / x) / (C * (x * C)))) * y = (((0 / x) / x) / C) * y. [back_rewrite(17938),rewrite([17943(8),18096(17)])].

18261 (C / x) / (C * x) = (0 / x) / x. [back_rewrite(17822),rewrite([18154(4)])].

18351 a(x,x \ 0,C) = 0. [para(30(a,1),17670(a,1,1))].

18361 x * (C / x) = C. [para(18351(a,1),111(a,1,2)),rewrite([16(8,R),16981(8),17203(6),340(5),8(4),8(5),9(10),16(6,R),8(6)])].

18489 x \ C = C / x. [para(18361(a,1),10(a,1,2))].

18570 C / (x * (C * x)) = x \ (x \ 0). [back_rewrite(17587),rewrite([18489(5)])].

18573 C * ((x \ 0) * (C * y)) = (C * (C / x)) * y. [back_rewrite(17581),rewrite([18489(10)])].

18704 x \ 0 = 0 / x. [back_rewrite(17203),rewrite([18489(4),17675(4)]),flip(a)].

18715 (x \ (C / x)) / C = x \ (0 / x). [back_rewrite(16980),rewrite([18489(2),18704(7)])].

18932 C * ((0 / x) * (C * y)) = (C * (C / x)) * y. [back_rewrite(18573),rewrite([18704(3)])].

18935 C / (x * (C * x)) = x \ (0 / x). [back_rewrite(18570),rewrite([18704(7)])].

18958 (0 / x) * (((0 / x) * y) / C) = (((0 / x) / x) / C) * y. [back_rewrite(17634),rewrite([18704(4),18704(9),8094(12),17943(8),18203(10),1

8704(8),18704(10)]),flip(a)].

19099 ((x / C) * (y / C)) / (0 / x) = (x / C) * (y * (x / C)). [back_rewrite(17016),rewrite([18704(7)])].

19117 (x / C) * (0 / x) = 0 / C. [back_rewrite(16749),rewrite([18704(4)])].

19122 ((0 / x) * y) / (x * ((0 / x) * y)) = 0 / x. [back_rewrite(9448),rewrite([18704(2),18704(5),18704(10)])].

19172 x * (0 / x) = 0. [back_rewrite(16370),rewrite([19117(6),795(5),28(3)]),flip(a)].

19181 x \ (C / x) = C / (x * x). [para(18489(a,1),380(a,1)),rewrite([18489(5)]),flip(a)].

19196 x \ (0 / x) = 0 / (x * x). [back_rewrite(18715),rewrite([19181(3),17797(5)]),flip(a)].

19209 C / (x * (C * x)) = 0 / (x * x). [back_rewrite(18935),rewrite([19196(8)])].

19269 (C * x) * (C / x) = C * C. [para(19172(a,1),25(a,2,2,2)),rewrite([16(6,R),18154(6),8(9)])].

19541 (C * C) / x = C * (C / x). [para(16771(a,1),36(a,1,1,2)),rewrite([16(9,R),18154(9)])].

19542 C / ((0 / x) \ (C * x)) = (0 / x) / x. [para(16771(a,1),162(a,1,1)),rewrite([411(12)])].

19776 (x * (y * x)) \ (x * z) = x \ (y \ z). [para(9(a,1),244(a,1,2,2))].

19780 (x * (y * (x * (z * (x * (y * x)))))) \ (x * (y * (x * (z * u)))) = (x * (y * x)) \ u. [para(13(a,1),244(a,1,1)),rewrite([13(10)])].

19785 x \ (C * y) = x \ (y * C). [para(25(a,1),244(a,1,2,2)),rewrite([19776(11),2694(8),10(3)])].

19873 (C * x) \ (y * C) = C * (x \ (y / C)). [para(94(a,1),244(a,1,2)),rewrite([5481(6),2694(13),19776(8),3339(5)]),flip(a)].

19910 (C * x) * (y * x) = x * ((y * C) * x). [para(244(a,1),187(a,1,1)),rewrite([80(2),19776(14),10(9),80(8),1130(9),81(10),2793(8),4033(6),

5350(8),19776(13),10(8),80(7),2793(11),71(12)]),flip(a)].

19939 (0 / x) \ y = x * y. [para(19172(a,1),244(a,1,1,2)),rewrite([8(4),10(7)]),flip(a)].

19974 (x / C) * ((C * y) * x) = x * (y * x). [back_rewrite(3314),rewrite([19910(12),16(10,R),44(10)])].

19988 (0 / x) / x = 0 / (x * x). [back_rewrite(19542),rewrite([19939(6),19209(5)]),flip(a)].

20067 (0 / x) * (((0 / x) * y) / C) = (0 / (C * (x * x))) * y. [back_rewrite(18958),rewrite([19988(11),17874(13),16(12,R)])].

20102 (C / x) / (C * x) = 0 / (x * x). [back_rewrite(18261),rewrite([19988(8)])].

20430 x / (y * x) = 0 / y. [para(19939(a,1),30(a,1,2))].

20431 (0 / x) * y = x \ y. [para(30(a,1),19939(a,1,1)),rewrite([18704(3)]),flip(a)].

20459 (x \ y) / y = 0 / x. [back_rewrite(19122),rewrite([20431(3),20431(4),9(3)])].

20521 (C * (x * x)) \ y = x \ ((x \ y) / C). [back_rewrite(20067),rewrite([20431(5),20431(6),20431(10)]),flip(a)].

20601 (C * (C / x)) * y = C * (x \ (C * y)). [back_rewrite(18932),rewrite([20431(6)]),flip(a)].

20903 0 / (x / y) = y / x. [para(12(a,1),20430(a,1,2)),flip(a)].

20904 x / (y * (z * (y * x))) = 0 / (y * (z * y)). [para(13(a,1),20430(a,1,2))].

20911 x / (y * (z * (u * (z * (y * x))))) = 0 / (y * (z * (u * (z * y)))). [para(38(a,1),20430(a,1,2))].

20998 C * (C * ((x * C) \ y)) = x \ (y * C). [para(20431(a,1),81(a,2)),rewrite([17874(6),20431(7)])].

21155 (x / y) \ z = (y / x) * z. [para(20903(a,1),19939(a,1,1))].

21162 C * ((x * y) \ (C * ((x / (C * C)) * y))) = a(0 / (C * C),x,y). [back_rewrite(8376),rewrite([21155(11),19541(5),20601(11)])].

21527 (x \ (C * y)) / C = C * ((C * x) \ y). [para(100(a,1),287(a,1,2,2,2)),rewrite([16(4,R),19776(9),80(5),16(10,R)])].

21531 (x * C) \ (y * C) = C * (x \ (y / C)). [para(287(a,1),380(a,2,2)),rewrite([76(5),2694(11),20521(6),10(3)]),flip(a)].

21937 x * ((x * y) \ x) = x / y. [para(8(a,1),291(a,2,1)),rewrite([20431(4)])].

21938 x \ ((x * y) / z) = (y / (x * z)) * x. [para(291(a,1),10(a,1,2))].

22259 (x * (y * (z * (y * (C * x))))) / C = x * (y * (z * (y * x))). [para(16(a,2),293(a,1,1,2,2,2,2))].

22629 C * (x * (((y / C) * x) / C)) = ((x / C) * y) / (0 / x). [para(19117(a,1),291(a,1,2,1,2)),rewrite([828(6),1130(7),2793(8)])].

22630 ((x / C) * (y * (z * (y / C)))) / (0 / x) = (x / C) * (y * (z * (y * (x / C)))). [para(19117(a,1),293(a,1,1,2,2,2,2)),rewrite([795(6)]

)].

22935 ((x / C) * y) / (0 / x) = x * (y * (x / C)). [para(71(a,1),298(a,1,1,2)),rewrite([19974(6),815(4),357(11),2793(12),22629(12)]),flip(a)

22973 (x / C) * (y * (z * (y * (x / C)))) = x * ((y * (z * (y / C))) * (x / C)). [back_rewrite(22630),rewrite([22935(10)]),flip(a)].

22975 (x / C) * (y * (x / C)) = x * ((y / C) * (x / C)). [back_rewrite(19099),rewrite([22935(8)]),flip(a)].

23019 (x / C) * (y * x) = x * ((y / C) * x). [back_rewrite(725),rewrite([22975(7),829(8)]),flip(a)].

23336 (x * C) \ (C * y) = C * (x \ (y / C)). [para(19785(a,1),237(a,1)),rewrite([19873(5)]),flip(a)].

23337 (C * x) \ (C * y) = C * (x \ (y / C)). [para(19785(a,1),237(a,2)),rewrite([21531(10)])].

24528 (x * y) \ x = x \ (x / y). [para(21937(a,1),10(a,1,2)),flip(a)].

24573 C / (x * (C * (x * (C * y)))) = 0 / (x * ((C * x) * y)). [para(139(a,1),21937(a,1,2,1)),rewrite([18489(11),17675(11),18154(10),17675(1

6)])].

24894 (x \ (x / y)) / x = 0 / (x * y). [para(24528(a,1),20459(a,1,1))].

25175 C * ((x / (C * C)) * y) = x * (y / C). [para(44(a,1),340(a,1,1)),rewrite([80(2),2225(8)]),flip(a)].

25292 C * (C * ((C * x) \ y)) = x * ((C / x) * (x \ y)). [para(19269(a,1),340(a,1,1)),rewrite([32(7),20102(14),20431(13),380(11),1128(12)])]

25311 C * ((x * y) \ (x * (y / C))) = a(0 / (C * C),x,y). [back_rewrite(21162),rewrite([25175(9)])].

25453 x \ ((C * x) * y) = (C / x) * (x * y). [para(16(a,2),341(a,1,2,1))].

25480 (x / (y * C)) * y = (x / y) * (y / C). [para(795(a,1),341(a,1,2)),rewrite([21938(4),795(9)])].

25486 x \ (C * (C * (x * y))) = (y / x) * (x * (C * C)). [para(299(a,2),341(a,1,2)),rewrite([16(4,R)])].

25571 C * (((C * x) / y) * (y / C)) = (C / y) * (y * x). [para(17675(a,1),341(a,2,1)),rewrite([16(6,R),47(7),23337(8),21938(7),25480(7),2043

1(14),25453(12)])].

25572 ((C / x) * y) / C = C * (x \ (y / C)). [para(18154(a,1),341(a,1,2,1)),rewrite([80(5),17874(9),20431(12),23336(10)])].

25644 C * (x * (C * a(C * (x / (y * C)),C * y,C))) = C * ((C * (x / y)) * y). [back_rewrite(3956),rewrite([25480(21),71(23)])].

25646 C * ((x / (C * y)) * y) = C * ((x / y) * (y / C)). [back_rewrite(1519),rewrite([25480(11)])].

25695 x \ (C * ((x / y) * (y / C))) = a(x / (C * y),y,C). [back_rewrite(2033),rewrite([25646(6)])].

26852 a(C,C * x,y) = a(x,C * y,C). [para(352(a,1),54(a,1,1)),rewrite([47(10),1244(11)]),flip(a)].

26883 (x * (C * (C * (C * y)))) * z = C * (C * (C * ((x * y) * z))). [para(352(a,1),61(a,2,1)),rewrite([77(7),16(13,R),47(16),77(15),3665(16

)]),flip(a)].

26956 a(x,y * (C * (C * z)),C) = a(x,C * C,(C * y) * z). [para(352(a,1),1320(a,2,2)),flip(a)].

27067 C / (x * (C * (C * y))) = 0 / ((C * x) * y). [para(352(a,1),17675(a,1,2))].

27068 x \ (C * (C * y)) = C * ((C / x) * y). [para(18154(a,1),352(a,1,2,1)),rewrite([20431(12)]),flip(a)].

27198 (x * (C * (y * (C * C)))) * z = C * (C * (C * ((x * y) * z))). [back_rewrite(7068),rewrite([26883(8)]),flip(a)].

27215 (x / y) * (y * (C * C)) = C * ((C / y) * (y * x)). [back_rewrite(25486),rewrite([27068(6)]),flip(a)].

27356 ((C * x) / y) * (z / C) = C * ((x / (C * y)) * z). [para(291(a,1),357(a,1,1)),rewrite([16(12,R),43(14)])].

27367 (C * (x / y)) * y = (C / y) * (y * x). [back_rewrite(25571),rewrite([27356(7),25646(7),71(8)])].

27372 C * (x * (C * a(C * (x / (y * C)),C * y,C))) = C * ((C / y) * (y * x)). [back_rewrite(25644),rewrite([27367(19)])].

27390 C * (x * (C * a(C,(C * x) / y,y))) = (C / y) * (y * (C * x)). [back_rewrite(1464),rewrite([27367(16)])].

28078 x * ((C / x) * (x \ y)) = x \ (y * C). [para(19269(a,1),371(a,1,1)),rewrite([32(7),20998(7),20102(10),20431(9),380(7),1128(8)]),flip(a

)].

28097 C * (C * ((C * x) \ y)) = x \ (y * C). [back_rewrite(25292),rewrite([28078(12)])].

28147 C * (x \ ((x / (C * C)) * y)) = (y / x) * (x / C). [para(795(a,1),372(a,1,2)),rewrite([3690(7),23337(8),2265(6),795(17),11(15),25480(1

2)])].

28275 (x / (C * y)) * y = (x / y) * (y / C). [para(795(a,1),373(a,1,2)),rewrite([2859(7),23336(8),2265(6),28147(8),795(13),43(11)]),flip(a)]

30817 (x * y) \ (x * z) = x \ ((x / y) * z). [para(24894(a,1),341(a,2,1)),rewrite([9(3),20431(8)]),flip(a)].

30851 C * (x \ ((x / y) * (y / C))) = a(0 / (C * C),x,y). [back_rewrite(25311),rewrite([30817(6)])].

30875 (x * (y * x)) \ z = x \ (y \ (x \ z)). [back_rewrite(19780),rewrite([30817(11),20911(6),20431(10),30817(8),20904(4),20431(7),30817(5),

20430(2),20431(4),10(2)]),flip(a)].

30907 a(0 / (C * C),x,y) = a(C,x,y * C). [back_rewrite(2716),rewrite([30817(6),25480(5),30851(7)])].

30949 (x * (C * C)) \ y = (x \ (y / C)) / C. [back_rewrite(978),rewrite([30875(5),80(3),80(5)]),flip(a)].

30950 (C * (C * x)) \ y = (x \ (y / C)) / C. [back_rewrite(914),rewrite([30875(10),80(8),80(10)])].

30951 C * (x \ ((x / y) * (y / C))) = a(C,x,y * C). [back_rewrite(30851),rewrite([30907(13)])].

31021 (x * y) \ (C * (x * (y / C))) = a(C,C * x,y * C). [back_rewrite(3767),rewrite([30950(10),2859(7),21527(10),28097(11),16(6,R)])].

31103 (x / C) * (y * (z * (y * x))) = x * ((y * (z * (y / C))) * x). [para(12(a,1),420(a,2,2,2,2,2)),rewrite([22973(9),829(10)]),flip(a)].

31586 a(x / C,C * y,C) = a(C,x,y). [para(9(a,1),26852(a,1,2)),rewrite([80(4)]),flip(a)].

31587 a(C,C * x,y / C) = a(x,y,C). [para(9(a,1),26852(a,2,2)),rewrite([80(5)])].

31588 a(C,x * C,y) = a(x,C * y,C). [para(16(a,1),26852(a,1,2))].

31589 a(C,C * x,y) = a(x,y * C,C). [para(16(a,1),26852(a,2,2))].

31606 a(C * x,C * y,C) = a(C,C * (x * C),y). [para(590(a,1),26852(a,1,2)),flip(a)].

31626 a(C,C * x,y) = a(x,C * C,y). [para(26852(a,2),1320(a,2)),flip(a)].

31650 a((C * x) * y,C * z,C) = a(C,x * (C * (C * y)),z). [para(352(a,1),26852(a,1,2)),flip(a)].

31663 (C / x) * (x * (C * y)) = C * ((C / x) * (x * y)). [back_rewrite(27372),rewrite([31606(11),16(9,R),2046(10),27390(10)])].

32802 a(x / C,C * C,y) = a(C,x,y). [para(31586(a,1),1320(a,2))].

32839 a(x / (C * C),y,C) = a(C,x / C,y / C). [para(1117(a,1),31587(a,1,2)),flip(a)].

32855 a(C * (x / (C * y)),z,C) = a(C,(C * x) / y,z / C). [para(291(a,1),31587(a,1,2)),rewrite([16(12,R)]),flip(a)].

32938 a(C,x * C,y) = a(x,y * C,C). [para(16(a,1),31588(a,2,2))].

32943 a(C,x * C,y * (C * C)) = a(x,C * C,C * (y * C)). [para(48(a,2),31588(a,2,2)),rewrite([6574(16),16(15,R)])].

32956 a(C,x * C,y) = a(x,C * C,y). [para(31588(a,2),1320(a,2)),flip(a)].

32972 a(C,C * x,C * (C * y)) = a(x,C * C,C * (y * C)). [para(47(a,1),31589(a,2,2)),rewrite([6568(16)])].

32998 a(C,C * x,y * C) = a(x,C * C,C * y). [para(31626(a,1),1329(a,1)),flip(a)].

33110 a(C,x * C,C * (C * y)) = a(x,C * C,C * (y * C)). [para(47(a,1),32938(a,2,2)),rewrite([6568(16)])].

40764 a(x,C * (y * (C * C)),z) = a(x,y,z). [para(662(a,1),54(a,1,1,2)),rewrite([27198(16),27068(17),27067(11),77(8),20431(14),30817(12),1767

5(8),20431(9),54(7),80(4),44(5)]),flip(a)].

40874 a(x,C * (C * (C * y)),z) = a(x,y,z). [back_rewrite(7779),rewrite([40764(14)])].

41334 a(C,x * (C * (C * C)),y) = a(C,x,y). [para(670(a,2),54(a,1,2,1)),rewrite([4051(8),8140(18),77(17),27068(19),24573(12),32(8),20431(16),

30817(14),17675(9),20431(11),54(9),80(5),44(6)]),flip(a)].

42694 (x \ ((C / y) * (y * x))) / C = a(C,x,y * (x * C)). [para(734(a,1),103(a,1,2)),rewrite([16(6,R),5565(12),30817(13),17675(7),20431(10),

30817(8),20430(3),20431(7),341(5),80(7)])].

49615 a(C,x,y * (C * C)) = a(C,x,y * C). [para(935(a,2),54(a,1,1)),rewrite([2826(14),27068(15),17675(10),20431(12),30817(10),28275(9),11(8),

25480(5),30951(7)]),flip(a)].

49681 a(x,C * C,C * (y * C)) = a(C,x * C,y * C). [back_rewrite(32943),rewrite([49615(8)]),flip(a)].

49683 a(C,x * C,C * (C * y)) = a(C,x * C,y * C). [back_rewrite(33110),rewrite([49681(16)])].

49684 a(C,C * x,C * (C * y)) = a(C,x * C,y * C). [back_rewrite(32972),rewrite([49681(16)])].

50293 a(x,C * C,C * (C * y)) = a(C,x * C,y * C). [para(959(a,1),26852(a,2,2)),rewrite([27215(11),28(7),7(8),49684(8),26956(14),32(13)]),flip

(a)].

50295 a(C * (C * x),y,C) = a(C,x,y / C). [para(959(a,1),31587(a,1,2)),rewrite([40874(10),27215(12),28(8),7(9)]),flip(a)].

52819 a(x,C * C,C * (y * (C * C))) = a(C,x * C,y * C). [para(1100(a,2),1320(a,2,2)),rewrite([26956(20),32(19),50293(20),16(17,R),49683(18)])

52998 a(C * (x * C),y,C) = a(C,x,y / C). [para(1106(a,1),31587(a,1,2)),rewrite([40764(10)]),flip(a)].

53225 a(C,C * x,y * C) = a(x,y / C,C). [para(299(a,2),1122(a,1,2,1)),rewrite([380(9),80(8),80(9),2225(9),13(10),1117(8),31021(7),380(13),80(

12),80(13),2225(13),6584(14)])].

53263 a(C,x,y / (C * C)) = a(C,x,y * C). [para(32802(a,1),1122(a,2)),rewrite([299(9,R),16(8,R),44(8),380(9),80(8),80(9),2225(9),2233(10),310

21(11),44(5),380(9),80(8),80(9),2225(9)]),flip(a)].

53265 a(C,x * C,y * C) = a(x,y / C,C). [para(32956(a,2),1122(a,2)),rewrite([380(9),80(8),80(9),2225(9),934(10),1117(8),31021(7),53225(6),380

(11),80(10),80(11),2225(11),53263(12)]),flip(a)].

53321 a(x,C * C,C * y) = a(x,y / C,C). [back_rewrite(32998),rewrite([53225(6)]),flip(a)].

53335 a(x,y / C,C) = a(x,C * y,C). [back_rewrite(52819),rewrite([53321(10),4033(6),16(5,R),44(5),53265(10)]),flip(a)].

53336 a(x,C * y,C) = a(x,y,C). [back_rewrite(50293),rewrite([53321(8),43(4),53265(8),53335(6)]),flip(a)].

53465 a(C,x * (C * (C * y)),z) = a((C * x) * y,z,C). [back_rewrite(31650),rewrite([53336(7)]),flip(a)].

53474 a(C,C * x,y) = a(x,y,C). [back_rewrite(26852),rewrite([53336(8)])].

53601 a(C,x,y / C) = a(C,x,y). [back_rewrite(41334),rewrite([53465(8),16(4,R),50295(6)])].

53762 a(C * (x * C),y,C) = a(C,x,y). [back_rewrite(52998),rewrite([53601(10)])].

53776 a(C * (x / (C * y)),z,C) = a(C,(C * x) / y,z). [back_rewrite(32855),rewrite([53601(14)])].

53777 a(x / (C * C),y,C) = a(C,x / C,y). [back_rewrite(32839),rewrite([53601(12)])].

54102 x \ (C * ((x / C) * y)) = (C / x) * (x * (y / C)). [para(1130(a,1),341(a,1,2))].

54105 (C / x) * (x * (y / C)) = C * ((y / x) * (x / C)). [para(1130(a,1),372(a,1,2)),rewrite([11(7),30817(6),80(6),25572(6),21938(5),25480(5

),20430(10),1130(13),20431(14),54102(12)]),flip(a)].

54129 a(C,x,y * C) = a(C,x,y). [para(11(a,1),53601(a,1,3)),flip(a)].

54131 a(C,x,C * y) = a(C,x,y). [para(43(a,1),53601(a,1,3)),flip(a)].

54193 C * (x \ ((x / y) * (y / C))) = a(C,x,y). [back_rewrite(30951),rewrite([54129(11)])].

54194 a(0 / (C * C),x,y) = a(C,x,y). [back_rewrite(30907),rewrite([54129(10)])].

54502 a(C,x,(C * y) * z) = a(C,x,y * (z / C)). [para(37(a,1),54131(a,1,3)),rewrite([2793(11),54131(12)])].

54511 a(C,x,y * (C * (C * z))) = a(C,x,y * (z / C)). [para(352(a,1),54131(a,1,3)),rewrite([54502(12)])].

54902 a(C * x,y,C) = a(C,x / C,y). [para(12(a,1),53762(a,1,1,2))].

54926 a(C,(x / (C * y)) / C,z) = a(C,(C * x) / y,z). [back_rewrite(53776),rewrite([54902(7)])].

56822 a(x * (y * (C * (C * x))),z,C) = a(C,x * (y * x),z). [para(1204(a,1),54902(a,1,1)),rewrite([43(15)])].

57653 a(C,x / C,y * (x / C)) = a(C,x,y * (x * C)). [para(798(a,2),1234(a,1,1)),rewrite([80(4),80(9),44(10),31103(10),28(6),8(5),80(14),44(15

),30950(17),22259(14),30817(11),20430(4),20431(10),30817(8),31663(7),10(8),42694(7),80(8),80(14),44(15),54131(16),54511(14)]),flip(a)].

57658 a(x / (C * y),y,C) = a(C,x,y * (x * C)). [para(1234(a,1),912(a,1)),rewrite([80(3),80(5),57653(7),80(7),80(9),16(11,R),44(11),23019(9),

80(11),30817(14),20430(9),20903(9),54105(11),25695(12)]),flip(a)].

57952 a(x / (C * y),y,C) = a(C,(x / C) / y,y). [para(44(a,1),1236(a,1,1)),rewrite([27367(6),54105(6),25695(7)])].

57956 a(C,(C * x) / y,y) = a(C,x,y * (x * C)). [para(939(a,1),1236(a,1,1)),rewrite([27367(10),31663(10),30949(11),43(8),42694(7)]),flip(a)].

58005 a(C,x / y,y) = a(C,x,y). [para(54194(a,1),1236(a,2)),rewrite([20431(6),380(4),80(3),80(4),2225(4),20431(11),380(9),80(8),80(9),2225(9)

,21155(11),19541(4),20601(11),25175(9),54193(7)]),flip(a)].

58020 a(C,x,y * (x * C)) = a(C,x / C,y). [back_rewrite(57658),rewrite([57952(5),58005(5)]),flip(a)].

58046 a(C,x / C,y) = a(x,y,C). [back_rewrite(57956),rewrite([58005(5),53474(4),58020(7)]),flip(a)].

58135 a(x / (C * y),z,C) = a(C,(C * x) / y,z). [back_rewrite(54926),rewrite([58046(7)])].

58143 a(C,x,y) = a(x,y,C). [back_rewrite(53777),rewrite([58135(6),43(5),58046(6)])].

58292 a(C,x * (y * (C * (C * x))),z) = a(C,x * (y * x),z). [back_rewrite(56822),rewrite([58143(8,R)])].

58428 a(C,c7 * (c7 * c7),c8) != 0. [back_rewrite(22),rewrite([58143(8,R)])].

59233 a(C,x * (x * x),y) = 0. [para(608(a,1),1239(a,1,2,1)),rewrite([178(9),77(10),1031(19),1031(20),16(18,R),30950(23),2859(20),5915(19),44

(14),41(17),28(3),19910(9),32(8),736(10),1031(9),16(7,R),53474(11),58143(9,R),58292(9)]),flip(a)].

59234 $F. [resolve(59233,a,58428,a)].

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

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

% Proof 2 at 103.52 (+ 0.34) seconds.

% Length of proof is 582.