Prover9 input file, Cheban loops paper

% Proof 1 at 127.23 (+ 0.66) seconds.

% Length of proof is 421.

% Level of proof is 40.

% Maximum clause weight is 31.000.

% Given clauses 4507.

1 a(C * (C * C),A,x) = 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 A * ((x * y) * A) = (A * x) * (y * A). [assumption].

15 (A * x) * (y * A) = A * ((x * y) * A). [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)].

19 a(C * (C * C),A,c1) != 0. [deny(1)].

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

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

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

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

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

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

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

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

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

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

39 (A * x) * A = A * (x * A). [para(7(a,1),15(a,1,2)),rewrite([8(7)])].

40 A * (((A \ x) * y) * A) = x * (y * A). [para(9(a,1),15(a,1,1)),flip(a)].

41 (A * x) \ (A * ((x * y) * A)) = y * A. [para(15(a,1),10(a,1,2))].

42 (A * ((x * y) * A)) / (y * A) = A * x. [para(15(a,1),11(a,1,1))].

43 A * ((x * (y / A)) * A) = (A * x) * y. [para(12(a,1),15(a,1,2)),flip(a)].

44 ((x * A) * (A * ((y * x) * A))) * z = (x * A) * ((A * y) * ((x * A) * z)). [para(15(a,1),13(a,1,1,2))].

45 A * (((x * A) * y) * A) = A * (x * (A * (y * A))). [para(15(a,1),13(a,1))].

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

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

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

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

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

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

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

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

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

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

57 (A * x) * (A * C) = A * ((x * C) * A). [para(16(a,1),15(a,1,2))].

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

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

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

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

69 (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))].

70 (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)])].

72 A * ((x * y) * (A * a(A * x,y,A))) = ((A * x) * y) * A. [para(15(a,1),18(a,1,1)),rewrite([13(10)])].

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

75 (x * (C * y)) * a(x,y,C) = C * (x * y). [para(16(a,2),18(a,1,1,2)),rewrite([16(9,R)])].

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

78 x / (x / C) = C. [para(12(a,1),49(a,1,1))].

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

82 (x * (x * y)) / y = x * x. [para(31(a,1),11(a,1,1))].

87 C * (x * x) = x * (x * C). [para(31(a,1),16(a,2))].

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

94 (x / C) * (C * ((x / C) * y)) = ((x / C) * x) * y. [para(51(a,1),13(a,1,1,2)),flip(a)].

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

96 A * ((A \ x) * A) = x * A. [para(9(a,1),39(a,1,1)),flip(a)].

97 (A * x) \ (A * (x * A)) = A. [para(39(a,1),10(a,1,2))].

98 (A * (x * A)) / A = A * x. [para(39(a,1),11(a,1,1))].

101 (A * x) * (A * (y * A)) = A * ((x * (A * y)) * A). [para(39(a,1),15(a,1,2))].

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

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

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

131 ((x * C) * (C * x)) * y = (C * x) * ((C * x) * y). [para(74(a,1),31(a,1,1))].

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

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

154 ((x / y) * x) / y = (x / y) * (x / y). [para(12(a,1),82(a,1,1,2))].

157 (A * (x * (A * (x * A)))) / A = (A * x) * (A * x). [para(15(a,1),82(a,1,1)),rewrite([13(6)])].

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

165 ((x * C) * ((C * x) * y)) / y = (C * x) * (C * x). [para(74(a,1),82(a,1,1))].

172 ((A * x) \ y) * (A * ((x * ((A * x) \ y)) * A)) = (((A * x) \ y) * y) * A. [para(15(a,1),33(a,1,2))].

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

177 ((C * x) \ y) * ((x * C) * (((C * x) \ y) * z)) = (((C * x) \ y) * y) * z. [para(74(a,1),33(a,1,2))].

189 x * (y * (C * (x * x))) = x * (y * (x * (x * C))). [para(87(a,2),13(a,2,2,2)),rewrite([13(5)]),flip(a)].

201 (x * C) * (C * (C * x)) = C * ((C * x) * (C * x)). [para(87(a,2),74(a,1)),rewrite([16(13,R)]),flip(a)].

207 ((x / C) * x) * (x / C) = (x / C) * ((x / C) * x). [para(87(a,1),33(a,1,2)),rewrite([77(2),77(4),77(6),16(8,R),51(8),77(8),77(11)]),flip

(a)].

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

272 A \ (x * A) = (A \ x) * A. [para(96(a,1),10(a,1,2))].

275 A * ((A \ x) * (A * y)) = (x * A) * y. [para(96(a,1),13(a,1,1)),flip(a)].

276 ((A \ x) * x) * A = (A \ x) * (x * A). [para(96(a,1),13(a,2,2)),rewrite([9(6)])].

280 (A * (x / A)) \ (A * x) = A. [para(12(a,1),97(a,1,2,2))].

288 (A * x) / A = A * (x / A). [para(12(a,1),98(a,1,1,2))].

290 (A * x) * (A * x) = A * (x * (A * x)). [back_rewrite(157),rewrite([288(9),35(8)]),flip(a)].

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

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

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

304 (x * (A * ((y * x) * A))) / A = x * ((A * y) * x). [para(15(a,1),35(a,1,1,2))].

305 (C * (x * (y * C))) / y = C * (x * C). [para(16(a,1),35(a,1,1,2,2))].

308 C * (x * C) = x * (C * C). [para(35(a,1),50(a,1))].

311 ((A * x) * (y * (A * (x * A)))) / A = (A * x) * (y * (A * x)). [para(39(a,1),35(a,1,1,2,2))].

318 (C * (x * (y * (y * C)))) / (y * y) = C * (x * C). [para(87(a,1),35(a,1,1,2,2))].

331 ((A \ x) * (x * A)) / A = (A \ x) * x. [para(96(a,1),35(a,1,1,2)),rewrite([9(13)])].

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

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

342 (C * (C * x)) \ (C * (x * C)) = 0. [para(74(a,1),337(a,1,2)),rewrite([16(8,R)])].

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

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

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

363 ((C * x) * y) / C = (x / C) * (C * y). [para(36(a,1),50(a,1,1))].

365 (C * x) * (y / C) = C * ((x / C) * y). [para(51(a,1),36(a,1,2,2)),flip(a)].

366 A * (((x / A) * (A * y)) * A) = ((A * x) * y) * A. [para(36(a,1),39(a,1,1)),flip(a)].

368 (x * C) * ((y / (C * x)) * ((C * x) * z)) = ((C * x) * y) * z. [para(36(a,1),74(a,1)),flip(a)].

381 A * ((x * (A \ y)) * A) = A * ((x / A) * (y * A)). [para(96(a,1),36(a,1,2,2)),rewrite([15(14)]),flip(a)].

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

405 x / (y \ (y \ x)) = y * y. [para(136(a,1),82(a,1,1,2)),rewrite([9(2),399(2)])].

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

435 (C * (x * (y * (z * (y * x))))) * u = (x * (y * (z * (y * (x * C))))) * u. [para(37(a,1),74(a,2,1))].

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

520 (0 / x) * (0 / x) = (0 / x) / x. [para(30(a,1),498(a,1,2)),flip(a)].

527 A \ (x * (y * A)) = ((A \ x) * y) * A. [para(40(a,1),10(a,1,2))].

530 A * (((A \ x) * y) * (A * z)) = (x * (y * A)) * z. [para(40(a,1),13(a,1,1)),flip(a)].

532 A * ((C / A) * (x * A)) = x * (A * C). [para(16(a,1),40(a,2,2)),rewrite([16(5,R),381(8)])].

574 (A * x) \ (A * (y * A)) = (x \ y) * A. [para(9(a,1),41(a,1,2,2,1))].

599 (A * (x * A)) / (y * A) = A * (x / y). [para(12(a,1),42(a,1,1,2,1))].

630 (A \ 0) * A = 0. [para(7(a,1),272(a,1,2)),rewrite([26(3)]),flip(a)].

631 (A \ (x / A)) * A = A \ x. [para(12(a,1),272(a,1,2)),flip(a)].

633 (A \ C) * A = C. [para(16(a,1),272(a,1,2)),rewrite([10(5)]),flip(a)].

634 (A \ (x * x)) * A = (A \ x) * (x * A). [para(31(a,1),272(a,1,2)),rewrite([527(5),276(5)]),flip(a)].

638 A \ 0 = 0 / A. [para(630(a,1),11(a,1,1)),flip(a)].

639 x * a(x,0 / A,A) = (x * (0 / A)) * A. [para(630(a,1),18(a,1,1,2)),rewrite([8(2),638(3),638(9)])].

640 A * (0 / A) = 0. [para(630(a,1),96(a,2)),rewrite([638(5),631(8),638(4)])].

641 (0 / A) * (x * (0 / A)) = ((0 / A) * x) / A. [para(630(a,1),35(a,1,1,2,2)),rewrite([638(3),8(5),638(9),638(12)]),flip(a)].

644 A \ C = C / A. [para(633(a,1),11(a,1,1)),flip(a)].

647 A * (C / A) = C. [para(633(a,1),96(a,2)),rewrite([644(5),631(8),644(4)])].

649 (x * (y / A)) * A = (x / A) * (A * y). [para(43(a,1),10(a,1,2)),rewrite([350(5)]),flip(a)].

661 x * a(x,0 / A,A) = x. [back_rewrite(639),rewrite([649(12),8(11),12(10)])].

665 A * (((0 / A) * x) * A) = x * A. [para(638(a,1),40(a,1,2,1,1)),rewrite([7(12)])].

667 (A * x) / (0 / A) = A * (x * A). [para(640(a,1),35(a,1,1,2,2)),rewrite([8(3)])].

673 (A * C) / (C / A) = A * A. [para(644(a,1),153(a,1,2))].

674 A * (((C / A) * x) * A) = C * (x * A). [para(644(a,1),40(a,1,2,1,1))].

740 a(x,0 / A,A) = 0. [para(661(a,1),10(a,1,2)),rewrite([26(1)]),flip(a)].

742 ((x * A) * y) * A = x * (A * (y * A)). [para(45(a,1),10(a,1,2)),rewrite([10(9)]),flip(a)].

833 A * ((A \ x) / A) = x / A. [para(9(a,1),288(a,1,1)),flip(a)].

837 (x * (y * A)) / A = A * ((A \ x) * y). [para(40(a,1),288(a,1,1)),rewrite([11(13)])].

839 A * ((C / A) / A) = C / A. [para(647(a,1),288(a,1,1)),flip(a)].

841 A * ((A \ (A \ x)) * x) = (A \ x) * x. [back_rewrite(331),rewrite([837(7)])].

886 (x * (C * C)) / C = x * C. [para(308(a,1),10(a,1,2)),rewrite([77(6)])].

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

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

898 C * (C * x) = x * (C * C). [para(16(a,2),308(a,1,2))].

902 (x * C) \ (x * (C * C)) = C. [para(308(a,1),48(a,1,2))].

931 (x * (C * C)) / x = C * C. [para(308(a,1),153(a,1,1)),rewrite([77(8),11(8)])].

945 A * ((C * C) / A) = C * C. [para(308(a,2),288(a,1,1)),rewrite([308(5),931(7)]),flip(a)].

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

1110 A \ (x / A) = (A \ x) / A. [para(631(a,1),11(a,1,1)),flip(a)].

1111 (x / A) * (A * A) = x * A. [para(631(a,1),15(a,2,2,1)),rewrite([1110(5),833(6),96(12)])].

1113 (C / A) * (A * C) = C * C. [para(159(a,1),631(a,1,1,2)),rewrite([634(7),644(3),16(6),308(13),10(14)])].

1114 A * (((A \ x) / A) * y) = x * (A \ y). [para(631(a,1),40(a,2,2)),rewrite([1110(7),649(10),9(9)])].

1124 (C * (x * (C * C))) * y = C * ((C * x) * (C * y)). [para(54(a,1),74(a,2,1)),rewrite([54(7)]),flip(a)].

1164 (C / A) * (A * (A * ((C / A) * x))) = C * (C * x). [para(673(a,1),36(a,1,2,1)),rewrite([31(11),1113(19),31(16)])].

1169 (x * (A \ y)) * a(A,(A \ x) / A,y) = (x / A) * y. [para(833(a,1),18(a,2,1)),rewrite([1114(7)])].

1171 A * ((A \ x) * x) = x * x. [para(82(a,1),833(a,2)),rewrite([527(6),276(6),837(8),841(8)])].

1283 (C * (A * (x * A))) / A = A * ((x * (A * C)) / A). [para(55(a,2),288(a,1,1))].

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

1315 (x * (y * (x * (C * C)))) / C = C * (x * (y * x)). [para(13(a,1),886(a,1,1)),rewrite([16(12,R)])].

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

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

1420 (C * (x * (C * C))) / x = C * (C * C). [para(898(a,1),35(a,1,1,2))].

1472 (x / A) * (A * C) = A * ((C / A) * x). [para(833(a,1),57(a,1,1)),rewrite([16(13,R),649(15),9(14)])].

1479 A * (C * (C / A)) = C * C. [back_rewrite(1113),rewrite([1472(7),16(6,R)])].

1491 A * ((((C * C) / A) * x) * A) = C * (C * (x * A)). [para(945(a,1),15(a,1,1)),rewrite([31(6)]),flip(a)].

1546 A \ (x * x) = (A \ x) * x. [para(82(a,1),1110(a,1,2)),rewrite([527(8),276(8),837(10),841(10)])].

1547 (C * C) / A = C * (C / A). [para(159(a,1),1110(a,1,2)),rewrite([1546(5),644(3),16(5,R),308(11),10(12)]),flip(a)].

1556 A * (((C * (C / A)) * x) * A) = C * (C * (x * A)). [back_rewrite(1491),rewrite([1547(6)])].

1560 (x * A) / (A * A) = x / A. [para(1111(a,1),11(a,1,1))].

1561 (x * A) * A = x * (A * A). [para(11(a,1),1111(a,1,1)),flip(a)].

1622 (x / A) * (x / A) = x * ((A \ x) / A). [para(1110(a,1),1171(a,1,2,1)),rewrite([1114(9),1110(4)]),flip(a)].

1644 (x * C) * (y / C) = C * ((x / C) * y). [para(16(a,2),62(a,2,1)),rewrite([77(4),95(6),77(9),365(10)])].

1648 (x * (x * y)) * a(x * x,z,z \ y) = (x * (x * z)) * (z \ y). [para(31(a,1),62(a,1,1)),rewrite([31(8)])].

1714 (x / C) / C = x / (C * C). [para(1314(a,1),10(a,1,2)),rewrite([77(4)])].

1718 (x / (C * C)) \ (x / C) = C. [para(1314(a,1),48(a,1,2))].

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

1815 (A / x) * (x * (0 / A)) = a(x,A,0 / A). [para(640(a,1),63(a,1,1,2)),rewrite([8(2),350(7)])].

1829 a(x,C * C,y) = a(x,C * y,C). [para(308(a,2),63(a,1,2,1)),rewrite([31(4),13(10),1767(11)]),flip(a)].

1844 (x * (A \ y)) \ ((x / A) * y) = a(A,(A \ x) / A,y). [para(833(a,1),63(a,1,2,1)),rewrite([1114(7)])].

1876 a(A,A \ x,x) = 0. [para(1171(a,1),63(a,1,1)),rewrite([9(5),26(3)]),flip(a)].

1956 a(A,(A \ x) / A,x / A) = 0. [para(1110(a,1),1876(a,1,2))].

2184 (x / (C * C)) / C = (x / C) / (C * C). [para(1314(a,1),1411(a,1,1)),flip(a)].

2309 C * (A * (C * C)) = A * (C * (C * C)). [para(1479(a,1),57(a,1,1)),rewrite([31(7),308(6),16(15,R),54(17),16(15),1472(16),16(15,R),1479(1

6)])].

2645 (x * (y * (x * (C * z)))) * a(x * (y * x),z,C) = C * (x * (y * (x * z))). [para(16(a,2),70(a,1,1,2,2,2)),rewrite([16(15,R)])].

2856 (x / A) / A = x / (A * A). [para(12(a,1),1560(a,1,1)),flip(a)].

2898 A * (C / (A * A)) = C / A. [back_rewrite(839),rewrite([2856(6)])].

3049 (x * y) * (A * a(A * x,y,A)) = ((x / A) * (A * y)) * A. [para(72(a,1),10(a,1,2)),rewrite([272(7),350(5)]),flip(a)].

3060 (C * (A * x)) * A = A * (C * (x * A)). [para(16(a,2),72(a,2,1)),rewrite([3049(11),1472(7),39(9),674(9)]),flip(a)].

3249 (x / (A * A)) * A = x / A. [para(2856(a,1),12(a,1,1))].

3253 (A * x) / (A * A) = A * (x / (A * A)). [para(288(a,1),2856(a,1,1)),rewrite([288(6),2856(5)]),flip(a)].

3516 ((x / (A * A)) * (A * y)) \ ((x / A) * y) = a(x / (A * A),A,y). [para(3249(a,1),63(a,1,2,1))].

4125 (C * (C * (x * y))) \ (C * (x * (C * y))) = a(C * C,x,y). [para(91(a,1),115(a,1,2)),rewrite([16(5,R),54(10)])].

4139 (x * (x * (0 / A))) * A = x * x. [para(740(a,1),91(a,1,2)),rewrite([12(5),8(2),8(3)]),flip(a)].

4259 a(C * C,x,x * C) = 0. [para(52(a,1),342(a,1,2,2)),rewrite([4125(15)])].

4395 a(C * C,x / C,x) = 0. [para(12(a,1),4259(a,1,3))].

4408 C * (C * ((x / C) * x)) = (C * x) * x. [para(4395(a,1),18(a,1,2)),rewrite([31(7),8(9),31(13),51(12)])].

4438 (x / C) * (C * (C * x)) = (C * x) * x. [para(308(a,2),94(a,1,2,2)),rewrite([16(8,R),51(8),308(14,R),16(13,R),4408(14)])].

4467 (0 / x) \ ((0 / x) / x) = 0 / x. [para(520(a,1),10(a,1,2))].

4516 A * ((0 / A) * x) = x. [para(13(a,1),665(a,1,2)),rewrite([12(9),8(6),649(12),8(11),12(10)])].

4522 A * (C * (0 / A)) = C. [para(52(a,1),665(a,1,2)),rewrite([12(10),8(7),16(6,R),16(12,R),649(14),8(13),12(12)])].

4539 (0 / A) * x = A \ x. [para(4516(a,1),10(a,1,2)),flip(a)].

4542 (x / (0 / A)) * (A \ y) = A * ((A \ x) * y). [para(36(a,1),4516(a,1,2)),rewrite([4539(5),4539(13)]),flip(a)].

4549 (x * (A \ y)) * a(A,A \ (x * (0 / A)),y) = (x * (0 / A)) * y. [para(4516(a,1),69(a,1,1)),rewrite([4539(4),4539(12),4539(21),9(20)])].

4565 A \ (x * (0 / A)) = (A \ x) / A. [back_rewrite(641),rewrite([4539(8),4539(10)])].

4567 (x * (0 / A)) * y = (x / A) * y. [back_rewrite(4549),rewrite([4565(10),1169(10)]),flip(a)].

4669 C * (0 / A) = C / A. [para(4522(a,1),10(a,1,2)),rewrite([644(3)]),flip(a)].

4689 (0 / (A * A)) * x = A \ (A \ x). [para(4539(a,1),31(a,1,1)),rewrite([1110(5),638(3),2856(5),4539(13),4539(12)])].

4691 C * (0 / (A * A)) = C / (A * A). [para(4539(a,1),87(a,1,2)),rewrite([1110(6),638(4),2856(6),16(15,R),4669(15),4539(14),1110(12),644(10)

,2856(12)])].

4701 (C * (C / A)) * x = C * (A \ (C * x)). [para(4539(a,1),54(a,2,2)),rewrite([4669(6)])].

4707 a(A,(A \ x) / A,y) = a(x,0 / A,y). [para(4539(a,1),63(a,1,1,2)),rewrite([4567(8),1844(7)])].

4759 (C * x) * (A * C) = C * (C * (x * A)). [back_rewrite(1556),rewrite([4701(7),381(10),532(10)])].

4764 a(x,0 / A,x / A) = 0. [back_rewrite(1956),rewrite([4707(8)])].

4787 ((A * C) * x) * A = C * (A * (x * A)). [para(647(a,1),101(a,1,1)),rewrite([366(16)]),flip(a)].

4832 A * (A * ((C / A) * x)) = C * (A * x). [para(2898(a,1),101(a,2,2,1,2)),rewrite([3249(10),647(7),16(4,R),649(11),1472(11)]),flip(a)].

4855 (C / A) * (C * (A * x)) = C * (C * x). [back_rewrite(1164),rewrite([4832(11)])].

4949 a(x * A,0 / A,x) = 0. [para(11(a,1),4764(a,1,3))].

5065 (x * A) * (A \ x) = x * x. [para(4949(a,1),18(a,1,2)),rewrite([4539(6),8(7),4567(12),11(9)])].

5240 (x * A) \ (x * x) = A \ x. [para(5065(a,1),10(a,1,2))].

6387 x / (0 / A) = x * A. [para(9(a,1),667(a,1,1)),rewrite([96(10)])].

6390 (x * A) * (A \ y) = A * ((A \ x) * y). [back_rewrite(4542),rewrite([6387(4)])].

6523 (x * A) * (0 / A) = x. [para(6387(a,1),12(a,1,1))].

6524 (x * A) \ x = 0 / A. [para(6387(a,1),30(a,1,1))].

6529 x * (0 / A) = x / A. [para(12(a,1),6523(a,1,1))].

6533 (x * A) * (x * A) = x * (A * (x * A)). [para(6523(a,1),82(a,1,1,2)),rewrite([6387(7),742(5)]),flip(a)].

6536 (A * C) \ C = 0 / A. [para(6523(a,1),115(a,1,2))].

6546 (x * y) \ (A * ((A \ x) * y)) = a(x,y * A,0 / A). [para(6523(a,1),63(a,1,1,2)),rewrite([6529(8),837(6)])].

6548 a(x,A,0 / A) = 0. [para(6523(a,1),63(a,1,2)),rewrite([6529(5),27(3),8(2),26(1)]),flip(a)].

6561 (x * (x * y)) * a(x * x,y * A,0 / A) = (x * (x * (y * A))) / A. [para(6523(a,1),91(a,1,1,2,2)),rewrite([6529(18)])].

6586 (x / A) * (A * x) = x * x. [back_rewrite(4139),rewrite([6529(4),649(5)])].

6595 (A / x) * (x / A) = 0. [back_rewrite(1815),rewrite([6529(6),6548(10)])].

6628 x \ (x / A) = 0 / A. [para(12(a,1),6524(a,1,1))].

6732 (x * x) / A = x * (x / A). [para(6529(a,1),31(a,1)),rewrite([6529(7)])].

6737 (x * (y * (z * (y * x)))) / A = x * (y * (z * (y * (x / A)))). [para(6529(a,1),37(a,1)),rewrite([6529(10)])].

6740 (x * (x * C)) / A = x * (C * (x / A)). [para(6529(a,1),52(a,1)),rewrite([6529(10)])].

6741 (C * (C * x)) / A = C * (x * (C / A)). [para(6529(a,1),54(a,1)),rewrite([6529(12)])].

6798 (A / x) \ 0 = x / A. [para(6595(a,1),10(a,1,2))].

6799 0 / (x / A) = A / x. [para(6595(a,1),11(a,1,1))].

6802 (A * (A / x)) * x = A * A. [para(6595(a,1),15(a,2,2,1)),rewrite([12(8),7(9)])].

6962 (A / C) / A = 0 / C. [para(78(a,1),6798(a,1,1)),rewrite([77(3)]),flip(a)].

6965 A / (x * A) = 0 / x. [para(11(a,1),6799(a,1,2)),flip(a)].

6967 A / (x * (x * A)) = 0 / (x * x). [para(82(a,1),6799(a,1,2)),flip(a)].

6987 (A \ (A / C)) / A = A \ (0 / C). [para(6962(a,1),1110(a,1,2)),flip(a)].

6991 (A / C) / (A * A) = (0 / C) / A. [para(6962(a,1),2856(a,1,1)),flip(a)].

6993 (A / C) \ (0 / C) = 0 / A. [para(6962(a,1),6628(a,1,2))].

7813 (C * (C / (A * A))) * x = (C / A) * ((C / A) * x). [para(4539(a,1),131(a,1,1,1)),rewrite([644(3),6529(8),1622(7),644(4),2856(6),6529(13

),6529(16)])].

7845 (A * x) * x = A * (x * x). [para(6586(a,1),13(a,2,2)),rewrite([12(5)])].

7874 ((x * C) / A) * (A * (C * x)) = (x * C) * (x * C). [para(1037(a,2),6586(a,1,2))].

8246 (x * A) * x = x * (A * x). [para(11(a,1),6732(a,2,2)),rewrite([6533(5),35(7)]),flip(a)].

8262 (x * (x / A)) / A = (x * x) / (A * A). [para(6732(a,1),2856(a,1,1))].

8268 (0 / x) * ((0 / x) / A) = ((0 / x) / x) / A. [para(520(a,1),6732(a,1,1)),flip(a)].

8289 (A * (A / x)) \ (A * A) = x. [para(6802(a,1),10(a,1,2))].

8290 (A * A) / x = A * (A / x). [para(6802(a,1),11(a,1,1))].

8295 C * ((A / C) * A) = A * A. [para(78(a,1),6802(a,1,1,2)),rewrite([1644(7)])].

8424 ((0 / A) / x) * ((0 / A) / x) = (((0 / A) / x) / A) / x. [para(6529(a,1),154(a,1,1)),flip(a)].

9048 (C * x) * (C * x) = C * ((C * x) * x). [para(165(a,1),1314(a,2)),rewrite([16(7,R),201(8),1411(12),363(8),4438(8)]),flip(a)].

9074 (x * C) * (x * C) = C * ((C * x) * x). [para(165(a,1),6387(a,1)),rewrite([9048(5),6529(13),649(14),7874(14)]),flip(a)].

9472 (x * A) \ (x * (A * x)) = x. [para(8246(a,1),10(a,1,2))].

9741 (A * x) \ (A * A) = x \ A. [para(29(a,1),8289(a,1,1,2))].

9744 A * (A / (x \ (A * A))) = x. [para(8290(a,1),29(a,1))].

9991 (A / C) * A = A * (A / C). [para(8295(a,1),10(a,1,2)),rewrite([77(5),8290(5)]),flip(a)].

10339 A / (x \ (A * A)) = A \ x. [para(9744(a,1),10(a,1,2)),flip(a)].

10341 a(x,y * A,0 / A) = a(x,A,A \ y). [para(9744(a,1),63(a,1,1,2)),rewrite([10339(9),6390(6),6546(7),10339(13)])].

10346 (x * (x * (y * A))) / A = (x * (x * A)) * (A \ y). [back_rewrite(6561),rewrite([10341(9),1648(8)]),flip(a)].

10438 A * (0 / C) = A / C. [para(9991(a,1),11(a,1,1)),rewrite([288(7),6962(6)])].

10463 A * ((0 / C) / A) = 0 / C. [para(9991(a,1),1560(a,1,1)),rewrite([3253(9),6991(8),6962(12)])].

10514 A \ (A / C) = 0 / C. [para(10438(a,1),10(a,1,2))].

10557 A \ (0 / C) = (0 / C) / A. [back_rewrite(6987),rewrite([10514(5)]),flip(a)].

10586 C * (A * (A * x)) = A * ((A * C) * x). [para(280(a,1),173(a,1,1)),rewrite([280(13),16(8),57(9),16(6,R),649(8),36(9),280(14)]),flip(a)]

10647 C * ((0 / C) / A) = 0 / A. [para(6993(a,1),173(a,1,1)),rewrite([6993(14),6529(11),6595(10),8(5),6993(11),4539(11),10557(9)]),flip(a)].

11123 (A * (C * (C * C))) * x = C * ((A * C) * (C * x)). [para(9472(a,1),177(a,1,1)),rewrite([16(7),308(12),902(13),16(11),308(16),902(17),3

08(14),2309(15)]),flip(a)].

11129 (A * x) * ((0 / C) / A) = A * ((x / A) * (0 / C)). [para(10463(a,1),36(a,1,2,2)),flip(a)].

11166 ((0 / C) / A) * (0 / C) = (0 / (C * C)) / A. [para(10463(a,1),8246(a,2,2)),rewrite([12(7),8268(9),1714(5)]),flip(a)].

11169 ((0 / C) / A) \ A = (0 / C) \ (A * A). [para(10463(a,1),9741(a,1,1)),flip(a)].

11289 (0 / C) / A = (0 / A) / C. [para(10647(a,1),10(a,1,2)),rewrite([77(5)]),flip(a)].

11322 ((0 / A) / C) \ A = (0 / C) \ (A * A). [back_rewrite(11169),rewrite([11289(5)])].

11324 ((0 / A) / C) * (0 / C) = (0 / (C * C)) / A. [back_rewrite(11166),rewrite([11289(5)])].

11350 (A * x) * ((0 / A) / C) = A * ((x / A) * (0 / C)). [back_rewrite(11129),rewrite([11289(7)])].

11363 A \ (0 / C) = (0 / A) / C. [back_rewrite(10557),rewrite([11289(10)])].

11367 A * ((0 / A) / C) = 0 / C. [back_rewrite(10463),rewrite([11289(6)])].

11513 ((0 / A) / C) * A = 0 / C. [para(11289(a,1),12(a,1,1))].

11517 A \ ((0 / A) / C) = ((0 / A) / C) / A. [para(11289(a,1),1110(a,1,2)),rewrite([11363(12)])].

11521 ((0 / A) / C) / A = (0 / C) / (A * A). [para(11289(a,1),2856(a,1,1))].

11529 (0 / C) * ((0 / A) / C) = (0 / (C * C)) / A. [para(11289(a,1),6732(a,2,2)),rewrite([520(7),1714(5)]),flip(a)].

11530 ((0 / C) / (A * A)) / C = (0 / (C * C)) / (A * A). [para(11289(a,1),154(a,1,1,1)),rewrite([11324(9),2856(9),11289(14),11289(19),8424(2

0),11521(16)]),flip(a)].

11532 A \ ((0 / A) / C) = (0 / C) / (A * A). [back_rewrite(11517),rewrite([11521(14)])].

11584 A * ((0 / (C * C)) / (A * A)) = (0 / (C * C)) / A. [para(11367(a,1),7845(a,1,1)),rewrite([11529(9),8424(19),11521(15),11530(17)]),flip

(a)].

11590 (0 / C) / ((0 / C) \ (A * A)) = (0 / (C * C)) / (A * A). [para(11513(a,1),153(a,1,1)),rewrite([11322(10),8424(22),11521(18),11530(20)]

)].

13266 C * (C * (x * C)) = x * (C * (C * C)). [para(189(a,1),50(a,1,1)),rewrite([1315(10)])].

14704 ((0 / C) / (A * A)) * ((0 / A) / C) = ((0 / A) / C) * ((0 / C) / (A * A)). [para(6529(a,1),207(a,1,1)),rewrite([11521(7),6529(27),1152

1(25)])].

14792 (x * (y * (x * (C * C)))) * z = C * (x * (y * (x * (C * z)))). [para(1829(a,1),70(a,1,2)),rewrite([31(4),2645(14)]),flip(a)].

16257 (C / A) * ((C / A) * x) = C * (A \ (A \ (C * x))). [para(4689(a,1),54(a,2,2)),rewrite([4691(8),7813(8)])].

16343 (C * (C / (A * A))) * x = C * (A \ (A \ (C * x))). [back_rewrite(7813),rewrite([16257(16)])].

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

16704 (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)])].

16706 ((A * x) * (y * (A * x))) \ (A * ((x * y) * A)) = (A * x) \ A. [para(15(a,1),244(a,1,2))].

16822 (x / A) \ y = (A / x) * y. [para(6595(a,1),244(a,1,1,2)),rewrite([8(4),10(9)]),flip(a)].

17037 (0 / x) * y = x \ y. [para(11(a,1),16822(a,1,1)),rewrite([6965(5)]),flip(a)].

17041 (0 / C) \ x = C * x. [para(78(a,1),16822(a,2,1)),rewrite([6962(5)])].

17110 (0 / (C * C)) / A = (0 / A) / (C * C). [back_rewrite(11529),rewrite([17037(9),77(7),1714(7)]),flip(a)].

17149 x \ ((0 / x) / A) = ((0 / x) / x) / A. [back_rewrite(8268),rewrite([17037(7)])].

17217 x \ (0 / x) = (0 / x) / x. [back_rewrite(520),rewrite([17037(5)])].

17223 (0 / (C * C)) / (A * A) = (0 / C) / (A * (A * C)). [back_rewrite(11590),rewrite([17041(10),87(8)]),flip(a)].

17279 A * ((0 / C) / (A * (A * C))) = (0 / A) / (C * C). [back_rewrite(11584),rewrite([17223(10),17110(18)])].

17361 ((0 / C) / (A * A)) / C = (0 / C) / (A * (A * C)). [back_rewrite(11530),rewrite([17223(18)])].

17370 x \ 0 = 0 / x. [para(17037(a,1),8(a,1))].

17373 (x \ y) / y = 0 / x. [para(17037(a,1),11(a,1,1))].

17374 (x * (y \ x)) * z = x * (y \ (x * z)). [para(17037(a,1),13(a,1,1,2)),rewrite([17037(7)])].

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

17380 (0 / x) \ y = x * y. [para(29(a,1),17037(a,1,1)),rewrite([17370(3)]),flip(a)].

17400 x / (y * (y * x)) = (0 / y) / y. [para(17037(a,1),405(a,2)),rewrite([17380(5),17380(4),17217(6)])].

17426 x \ (A * A) = (x \ A) * A. [para(17037(a,1),1561(a,1,1)),rewrite([17037(10)]),flip(a)].

17458 x \ (0 / A) = (0 / x) / A. [para(17037(a,1),6529(a,1))].

17461 0 / (0 / x) = x. [para(17037(a,1),6965(a,1,2)),rewrite([29(4)]),flip(a)].

17500 x * ((0 / x) / x) = 0 / x. [para(4467(a,1),17037(a,2)),rewrite([17461(4)])].

17646 (0 / x) / x = 0 / (x * x). [back_rewrite(6967),rewrite([17400(5)])].

17690 0 / (x \ A) = A \ x. [back_rewrite(10339),rewrite([17426(5),6965(6)])].

17730 x * (0 / (x * x)) = 0 / x. [back_rewrite(17500),rewrite([17646(3)])].

17764 x \ ((0 / x) / A) = (0 / (x * x)) / A. [back_rewrite(17149),rewrite([17646(8)])].

17882 x * (0 / x) = 0. [para(17370(a,1),9(a,1,2))].

17884 (C * x) * (0 / (x * C)) = 0. [para(17370(a,1),113(a,1,2))].

17936 (A * x) * (y * (A * (z * A))) = A * ((x * ((y * A) * z)) * A). [para(275(a,1),101(a,2,2,1,2)),rewrite([40(11),39(6)])].

18051 (A * x) * (y * (A * x)) = A * (x * ((y * A) * x)). [back_rewrite(311),rewrite([17936(8),13(7),6737(10),27(6),8(5)]),flip(a)].

18076 (A * x) \ A = 0 / x. [back_rewrite(16706),rewrite([18051(6),574(12),16700(6),6524(3),17458(4),12(6)]),flip(a)].

18099 (x * y) * (0 / x) = x * (y / x). [para(17882(a,1),36(a,1,2,2)),rewrite([8(3)]),flip(a)].

18104 x * (0 / C) = x / C. [para(17882(a,1),56(a,2,2,2)),rewrite([17037(9),77(7),51(8),8(9),17037(8),77(6)])].

18107 a(x,0 / x,y) = 0. [para(17882(a,1),63(a,1,2,1)),rewrite([17037(3),9(2),7(2),26(1)]),flip(a)].

18175 (A * x) * ((0 / A) / C) = A * ((x / A) / C). [back_rewrite(11350),rewrite([18104(15)])].

18270 (((0 / A) / C) * ((0 / C) / (A * A))) * A = (0 / C) / (A * (A * C)). [para(11513(a,1),276(a,2,2)),rewrite([11532(7),14704(13),11532(22

),18104(26),17361(24)])].

18308 x / (y * x) = 0 / y. [para(10(a,1),17373(a,1,1))].

18309 0 / (x / y) = y / x. [para(30(a,1),17373(a,1,1)),flip(a)].

18310 C / (C * x) = 0 / x. [para(48(a,1),17373(a,1,1))].

18311 (x / C) / x = 0 / C. [para(77(a,1),17373(a,1,1))].

18318 (C * C) / x = C / (x / C). [para(1718(a,1),17373(a,1,1)),rewrite([18309(10)]),flip(a)].

18320 (0 / A) / x = 0 / (x * A). [para(6524(a,1),17373(a,1,1))].

18332 ((A * C) \ ((0 / C) / (A * A))) * A = (0 / C) / (A * (A * C)). [back_rewrite(18270),rewrite([18320(5),16(4),17037(13)])].

18337 (A * x) * (0 / (A * C)) = A * ((x / A) / C). [back_rewrite(18175),rewrite([18320(7),16(6)])].

18367 A * ((0 / C) / (A * (A * C))) = 0 / (A * (C * C)). [back_rewrite(17279),rewrite([18320(18),31(17),16(16),308(17)])].

18411 A \ (0 / (A * C)) = (0 / C) / (A * A). [back_rewrite(11532),rewrite([18320(6),16(5)])].

18590 (C * (x \ y)) \ ((x \ C) * y) = a(C,0 / x,y). [para(17377(a,1),63(a,1,2,1)),rewrite([17037(4)])].

18591 ((x \ C) * y) / a(C,0 / x,y) = C * (x \ y). [para(17377(a,1),64(a,1,1,1)),rewrite([17037(12)])].

18684 A \ (0 / x) = 0 / (x * A). [para(17380(a,1),17690(a,1,2)),flip(a)].

18686 (0 / C) / (A * A) = 0 / (A * (A * C)). [back_rewrite(18411),rewrite([18684(7),39(6),16(5)]),flip(a)].

18709 ((A * C) \ (0 / (A * (A * C)))) * A = (0 / C) / (A * (A * C)). [back_rewrite(18332),rewrite([18686(10)])].

18746 (0 / x) / A = 0 / (A * x). [para(18076(a,1),17373(a,1,1))].

18756 x \ (0 / (A * x)) = 0 / (A * (x * x)). [back_rewrite(17764),rewrite([18746(4),18746(10)])].

18770 (0 / C) / (A * (A * C)) = 0 / (A * (A * (C * C))). [back_rewrite(18709),rewrite([18756(11),9074(9),16(6),39(8),16(7),10586(9),16(8,R),

308(8),17037(13),18076(11)]),flip(a)].

18781 A * (0 / (A * (A * (C * C)))) = 0 / (A * (C * C)). [back_rewrite(18367),rewrite([18770(10)])].

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

18787 (x * (y / C)) / C = (x / (C * C)) * y. [para(18104(a,1),13(a,1,1,2)),rewrite([17037(6),77(4),1714(4),17037(12),77(10),17037(12),77(10)

]),flip(a)].

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

18792 (x * x) / C = x * (x / C). [para(18104(a,1),31(a,1)),rewrite([18104(7)])].

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

19038 x / (y * (z * (u * (z * (y * x))))) = 0 / (y * (z * (u * (z * y)))). [para(37(a,1),18308(a,1,2))].

19049 A * (0 / x) = A / x. [para(1111(a,1),18308(a,1,2)),rewrite([8290(6),18308(5),18309(8)])].

19099 A / (A * (A * (C * C))) = 0 / (A * (C * C)). [back_rewrite(18781),rewrite([19049(11)])].

19124 (x / y) * (y / x) = 0. [para(18309(a,1),12(a,1,1))].

19126 x / (C * (x * C)) = 0 / (C * C). [para(159(a,1),18309(a,1,2)),flip(a)].

19141 (x / y) \ z = (y / x) * z. [para(18309(a,1),17037(a,1,1)),flip(a)].

19175 (C / x) * (C * x) = C * C. [back_rewrite(1318),rewrite([19141(5)])].

19197 (x * (x / C)) * y = x * ((x * y) / C). [para(18311(a,1),36(a,1,2,1)),rewrite([17037(5),77(3)]),flip(a)].

19498 ((A * x) / (C * C)) * A = A * ((x / C) * (A / C)). [para(18784(a,1),172(a,1,1)),rewrite([18784(11),18104(8),17037(10),77(8),18788(8),1

8784(15),17037(16),77(14),1714(14)]),flip(a)].

19776 C * (A * ((x * C) * A)) = A * (C * (C * (x * A))). [para(6536(a,1),298(a,1,2)),rewrite([6387(10),4787(8),18051(16),16(14,R)])].

20158 x \ (x \ C) = (x \ C) / x. [para(17377(a,1),299(a,2,2)),rewrite([8(5),16(4,R),17377(4),17037(8)]),flip(a)].

20259 x * ((x * y) \ x) = x / y. [para(8(a,1),300(a,2,1)),rewrite([17037(4)])].

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

20464 C / (x / C) = C * (x \ C). [para(18310(a,1),300(a,1,2,1)),rewrite([16(5,R),17377(5),18318(8)]),flip(a)].

20507 (C * C) / x = C * (x \ C). [back_rewrite(18318),rewrite([20464(8)])].

20827 A * (A * (C * (A \ (C * x)))) = C * (C * (A * x)). [para(16(a,1),304(a,1,1)),rewrite([16(8,R),19776(8),288(10),10346(9),16(5),308(6),3

49(9),6732(7),4701(8),16(15,R)])].

21891 a(x,0 / (x * x),y) = 0. [para(17730(a,1),63(a,1,2,1)),rewrite([17037(4),399(2),9(3),17037(4),26(3)]),flip(a)].

21901 x * ((x \ C) / x) = x \ C. [para(17730(a,1),75(a,2,2)),rewrite([17377(5),399(3),20158(3),21891(9),8(6),17377(8)])].

22007 x / (0 / (C * C)) = C * (x * C). [para(18104(a,1),318(a,1,2)),rewrite([16(9,R),17882(9),8(6),18104(5),51(4),1714(5)])].

22108 (A * C) * (A * x) = A * (A * (x * C)). [para(17884(a,1),44(a,2,2,2)),rewrite([16(3),101(10),3060(9),18337(16),288(11),837(10),644(6),4

832(11),50(9),16(9),8(13)]),flip(a)].

22465 x * ((x * (C / (x * x))) / C) = 0. [para(18792(a,1),19124(a,1,1)),rewrite([19197(7)])].

23240 (A * (A * (A * (C * C)))) \ (A * (A * (A * (C * (C * x))))) = x. [para(290(a,1),338(a,1,2,1,2)),rewrite([39(7),16(6),10586(9),9074(8),

16(5),39(7),16(6),10586(8),16(7,R),308(7),308(16),14792(19),10586(19),22108(18),16(16,R)])].

23613 x * (((x \ y) / x) * z) = y * (x \ z). [para(9(a,1),349(a,1,1)),flip(a)].

23668 A * (C * (A \ (A \ (C * x)))) = C * (C * (A \ x)). [para(1479(a,1),349(a,1,1)),rewrite([31(6),8262(14),20507(14),399(13),644(12),1110(

13),644(11),2856(13),16343(15)]),flip(a)].

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

23974 (x * A) \ (x * y) = x \ ((x / A) * y). [para(6529(a,1),350(a,1,2,1)),rewrite([18320(8),17037(10)]),flip(a)].

23975 (x / (y * A)) * y = (x / y) * (y / A). [para(6529(a,1),350(a,1,2)),rewrite([20260(4),6529(9)])].

24013 (x / (y * C)) * y = (x / y) * (y / C). [para(18104(a,1),350(a,1,2)),rewrite([20260(4),18104(9)])].

24020 (A * x) \ (A * y) = A \ ((A / x) * y). [para(19049(a,1),350(a,1,2,1)),rewrite([18746(9),17037(12)]),flip(a)].

24115 x \ ((x / A) * x) = A \ x. [back_rewrite(5240),rewrite([23974(4)])].

24128 A \ (A \ ((A / (C * C)) * (A * (C * (C * x))))) = x. [back_rewrite(23240),rewrite([24020(20),19099(10),17037(17),24020(15)])].

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

24456 (x / C) * (C * (x \ (C * y))) = x * ((C / x) * y). [para(20464(a,1),349(a,2,2,1)),rewrite([16(4,R),51(4),19141(3),17374(11)]),flip(a)]

25064 a(x,(x \ C) / x,y) = a(C,0 / x,y). [para(21901(a,1),63(a,1,2,1)),rewrite([23613(5),18590(7)]),flip(a)].

25410 A * (C * (C * (C / A))) = C * (C * C). [para(1479(a,1),358(a,2,2)),rewrite([8262(8),20507(8),399(7),644(6),1110(7),644(5),2856(7),16(1

1),4759(12),23975(10),27(9),8(8)])].

25486 (x / A) * x = x * (A \ x). [para(24115(a,1),9(a,1,2)),flip(a)].

25671 (x \ (x / y)) / x = 0 / (x * y). [para(24304(a,1),17373(a,1,1))].

26075 x / (x * (A \ x)) = A / x. [para(25486(a,1),18308(a,1,2)),rewrite([18309(8)])].

26840 C * ((C / A) * (C * x)) = C * (C * (C * (A \ x))). [para(26075(a,1),368(a,1,2,1)),rewrite([644(3),16(5,R),644(12),4701(14),24456(15),4

701(12),23896(11),1472(11),16257(10),23668(11),644(12),16(15,R),54(16)]),flip(a)].

28822 C * ((A * C) * (C * x)) = A * (C * (C * (C * x))). [para(6586(a,1),421(a,1,1,2,2)),rewrite([11123(8),4855(18)])].

29710 (x * (C * (C * C))) * y = C * ((C * x) * (C * y)). [para(19175(a,1),435(a,2,1,2,2)),rewrite([18308(6),17037(7),48(5),1124(7)]),flip(a)

30494 x * ((x \ y) / x) = y * (0 / x). [para(9(a,1),18099(a,1,1)),flip(a)].

32547 (0 / (C * C)) / x = 0 / (C * (x * C)). [para(22007(a,1),18309(a,1,2)),flip(a)].

33608 (x * (C / (x * x))) / C = 0 / x. [para(22465(a,1),10(a,1,2)),rewrite([17370(2)]),flip(a)].

33616 x * (x * (C / (x * x))) = C. [para(22465(a,1),65(a,2,1)),rewrite([33608(11),18107(9),8(7),7(8)])].

33619 x * (C / (x * x)) = x \ C. [para(33616(a,1),10(a,1,2)),flip(a)].

33660 (x \ C) / x = C / (x * x). [para(33619(a,1),10(a,1,2)),rewrite([20158(3)])].

33675 ((x \ C) * y) / a(x,C / (x * x),y) = x * ((C / (x * x)) * y). [para(33619(a,1),64(a,1,1,1))].

33746 a(x,C / (x * x),y) = a(C,0 / x,y). [back_rewrite(25064),rewrite([33660(3)])].

33799 x * ((C / (x * x)) * y) = C * (x \ y). [back_rewrite(33675),rewrite([33746(7),18591(8)]),flip(a)].

34772 (x * y) \ (x * z) = x \ ((x / y) * z). [para(25671(a,1),350(a,2,1)),rewrite([9(3),17037(8)]),flip(a)].

34880 (x * (y * x)) \ z = x \ (y \ (x \ z)). [back_rewrite(16704),rewrite([34772(11),19038(6),17037(10),34772(8),19030(4),17037(7),34772(5),

18308(2),17037(4),10(2)]),flip(a)].

35353 (x * (y * A)) * (C / A) = A * (C * ((A \ x) * y)). [para(647(a,1),530(a,1,2,2)),rewrite([16(6,R)]),flip(a)].

35496 (x * (A * C)) / A = A * (C * (A \ x)). [para(532(a,1),288(a,1,1)),rewrite([837(15),1110(13),644(11),2856(13),33799(15)])].

35557 (C * (A * (x * A))) / A = A * (A * (C * (A \ x))). [back_rewrite(1283),rewrite([35496(15)])].

36227 x * (0 / (C * C)) = x / (C * C). [para(19126(a,1),30494(a,2,2)),rewrite([7(4),7(7),399(7),77(6),77(7),1714(7),7(11),31(12),1314(11),21

84(7),1314(8),1714(4)]),flip(a)].

37142 x \ ((x / (C * C)) * y) = ((y / x) / (C * C)) * x. [para(36227(a,1),350(a,1,2,1)),rewrite([32547(12),17037(14),34880(12),77(10),20260(

11),24013(11),77(12),18787(12)])].

37177 (x * (C / A)) * (A / C) = x. [back_rewrite(24128),rewrite([37142(15),288(9),6741(8),19498(15),50(10),10(12)])].

37183 x / (A / C) = x * (C / A). [para(37177(a,1),11(a,1,1))].

37210 (x * (A / C)) * (C / A) = x. [para(37183(a,1),11(a,1))].

38082 (A * x) / (y * A) = A * ((x / A) / y). [para(12(a,1),599(a,1,1,2))].

40385 (x * (A * (y * A))) / A = (x * A) * y. [para(742(a,1),11(a,1,1))].

40444 A * (A * (C * (A \ x))) = (A * C) * x. [back_rewrite(35557),rewrite([40385(8),16(3)]),flip(a)].

40469 (A * C) * (C * x) = C * (C * (A * x)). [back_rewrite(20827),rewrite([40444(10)])].

40476 C * (C * (C * (A * x))) = A * (C * (C * (C * x))). [back_rewrite(28822),rewrite([40469(7)])].

49265 A * (C * (C * (C * (A \ x)))) = C * (x * (C * C)). [para(1124(a,1),37210(a,1,1)),rewrite([51(8),35353(10),644(5),26840(9)])].

62097 (x * (C * (C * C))) / x = C * (C * C). [para(13266(a,1),305(a,1,1))].

62118 (x * (A * (C * (C * C)))) / A = C * (x * (C * C)). [para(13266(a,2),837(a,2,2)),rewrite([52(7),16(5),308(6),2309(7),16(17,R),49265(20)

])].

76684 a(C * (C * C),A,x) = 0. [para(1420(a,1),3516(a,1,1,1)),rewrite([52(8),40476(8),308(16,R),16(15,R),87(15),10586(16),16(15,R),308(15),10

586(17),308(16,R),16(15,R),308(15),2309(16),62118(19),2309(15),29710(16),16(12),40469(15),40476(16),26(17),308(9,R),16(8,R),87(8),10586(9),16

(8,R),308(8),10586(10),308(9,R),16(8,R),308(8),2309(9),38082(14),62097(11),6740(9),25410(10)]),flip(a)].

76685 $F. [resolve(76684,a,19,a)].

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

% Proof 2 at 403.34 (+ 2.22) seconds.

% Length of proof is 247.

% Level of proof is 34.

% Maximum clause weight is 28.000.

% Given clauses 10987.

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