% Proof 1 at 0.01 (+ 0.00) seconds.

% Length of proof is 13.

% Level of proof is 5.

% Maximum clause weight is 15.000.

% Given clauses 34.

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

3 0 * x = x. [assumption].

4 x * 0 = x. [assumption].

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

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

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

13 C * c3 != c3 * C. [deny(2)].

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

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

30 (C * x) * (C * y) = C * (C * (x * y)). [back_rewrite(10),rewrite([21(5)]),flip(a)].

114 (C * x) * C = C * (C * x). [para(4(a,1),30(a,1,2)),rewrite([4(8)])].

134 C * x = x * C. [para(5(a,1),114(a,1,1)),rewrite([5(7)]),flip(a)].

135 $F. [resolve(134,a,14,a(flip))].

% Proof 2 at 0.40 (+ 0.00) seconds.

% Length of proof is 41.

% Level of proof is 14.

% Maximum clause weight is 23.000.

% Given clauses 167.

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

3 0 * x = x. [assumption].

4 x * 0 = x. [assumption].

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

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

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

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

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

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

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

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

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

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

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

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

29 (c1 * C) * (c1 * c2) != c1 * (c1 * (C * c2)). [back_rewrite(12),rewrite([21(7)]),flip(a)].

30 (C * x) * (C * y) = C * (C * (x * y)). [back_rewrite(10),rewrite([21(5)]),flip(a)].

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

42 (x * y) / (x \ y) = x * x. [para(5(a,1),33(a,1,1,2))].

55 x / (x \ 0) = x * x. [para(4(a,1),42(a,1,1))].

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

114 (C * x) * C = C * (C * x). [para(4(a,1),30(a,1,2)),rewrite([4(8)])].

115 C * (C * ((C \ x) * y)) = x * (C * y). [para(5(a,1),30(a,1,1)),flip(a)].

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

134 C * x = x * C. [para(5(a,1),114(a,1,1)),rewrite([5(7)]),flip(a)].

144 (C * c1) * (c1 * c2) != c1 * (c1 * (C * c2)). [back_rewrite(29),rewrite([134(3,R)])].

178 C \ (x * C) = x. [para(134(a,1),6(a,1,2))].

182 C * (x / C) = x. [para(134(a,2),8(a,1))].

213 C \ x = x / C. [para(8(a,1),178(a,1,2))].

215 C * (C * (x * (y / C))) = (C * x) * y. [back_rewrite(116),rewrite([213(4)])].

216 C * (C * ((x / C) * y)) = x * (C * y). [back_rewrite(115),rewrite([213(4)])].

262 C / (0 / C) = C * C. [para(213(a,1),55(a,1,2))].

269 (0 / C) * (C * x) = x. [para(262(a,1),26(a,1,2,1)),rewrite([21(11),216(11),3(7),134(11,R),182(11),3(8)])].

271 (0 / C) * x = x / C. [para(5(a,1),269(a,1,2)),rewrite([213(6)])].

273 x / (C * x) = 0 / C. [para(269(a,1),7(a,1,1))].

281 (x * (x / C)) * y = x * ((x * y) / C). [para(269(a,1),27(a,1,1,2)),rewrite([271(4),271(13),182(12),271(9)])].

321 x / (x * C) = 0 / C. [para(134(a,1),273(a,1,2))].

2232 (x * x) / C = x * (x / C). [para(321(a,1),90(a,1,2,1)),rewrite([271(4)]),flip(a)].

2331 C * (x * (x / C)) = x * x. [para(2232(a,1),8(a,1,1)),rewrite([134(5,R)])].

2502 (C * x) * (x * y) = x * (x * (C * y)). [para(2331(a,1),30(a,1,1)),rewrite([21(4),281(10),215(12)]),flip(a)].

2503 $F. [resolve(2502,a,144,a)].

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

% Proof 1 at 0.78 (+ 0.01) seconds.

% Length of proof is 109.

% Level of proof is 24.

% Maximum clause weight is 23.000.

% Given clauses 188.

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

2 0 * x = x. [assumption].

3 x * 0 = x. [assumption].

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

27 (C * c1) * (C * c2) != C * (C * (c1 * c2)). [back_rewrite(12),rewrite([19(14)])].

28 (x * C) * (x * y) = x * (x * (C * y)). [back_rewrite(10),rewrite([19(8)])].

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

31 (x * (x * y)) / y = x * x. [para(19(a,1),6(a,1,1))].

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

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

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

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

52 x / (y \ (y \ x)) = y * y. [para(34(a,1),31(a,1,1,2)),rewrite([4(2),49(2)])].

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

57 (0 / x) * (0 / x) = (0 / x) / x. [para(18(a,1),53(a,1,2)),flip(a)].

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

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

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

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

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

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

137 (x / C) * x = x * (x / C). [para(7(a,1),112(a,1,1)),rewrite([7(9)]),flip(a)].

186 (x / C) \ (x * (x / C)) = x. [para(137(a,1),5(a,1,2))].

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

358 x * ((0 / x) / x) = 0 / x. [para(57(a,1),96(a,2,2)),rewrite([3(2),4(4)]),flip(a)].

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

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

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

394 (x \ y) / y = 0 / x. [para(349(a,1),23(a,1,1,2)),rewrite([391(3),389(7),3(6)])].

396 (x * (y \ x)) * z = x * (y \ (x * z)). [para(349(a,1),25(a,1,1,2,2)),rewrite([391(3),391(9),4(8),391(7)])].

420 x \ (0 / x) = (0 / x) / x. [back_rewrite(57),rewrite([391(5)])].

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

440 (x * y) * (0 / x) = x * (y / x). [para(389(a,1),24(a,1,2,2)),rewrite([3(3)]),flip(a)].

441 x * (x * (C * (0 / x))) = x * C. [para(389(a,1),28(a,1,2)),rewrite([3(4)]),flip(a)].

447 (0 / x) / x = 0 / (x * x). [para(433(a,1),49(a,1)),rewrite([433(5),420(6)]),flip(a)].

465 x * (0 / (x * x)) = 0 / x. [back_rewrite(358),rewrite([447(3)])].

473 x / (y * x) = 0 / y. [para(390(a,1),17(a,1,2))].

496 0 / (x / y) = y / x. [para(18(a,1),394(a,1,1)),flip(a)].

528 (x / y) * ((y / x) * z) = z. [para(496(a,1),96(a,2,2,1)),rewrite([3(3),4(4)]),flip(a)].

529 (x / y) \ z = (y / x) * z. [para(496(a,1),390(a,1,1))].

545 (C / x) * (x * (x / C)) = x. [back_rewrite(186),rewrite([529(6)])].

586 x * (x * (C * (0 / (x * x)))) = x * (C / x). [para(465(a,1),28(a,1,2)),rewrite([440(5)]),flip(a)].

662 (x * C) * (x / C) = x * x. [para(545(a,1),8(a,2,2)),rewrite([7(3)])].

781 ((x \ C) * C) * (0 / x) = (x \ C) * (x \ C). [para(394(a,1),662(a,1,2))].

900 x * (C * (0 / x)) = C. [para(441(a,1),5(a,1,2)),rewrite([5(3)]),flip(a)].

922 C * (0 / x) = x \ C. [para(900(a,1),5(a,1,2)),flip(a)].

923 x \ (C * x) = C. [para(17(a,1),900(a,1,2,2)),rewrite([433(2),391(5)])].

925 (C * x) * (C / x) = C * C. [para(900(a,1),24(a,1,2)),rewrite([496(9)]),flip(a)].

930 x * (C / x) = C. [back_rewrite(586),rewrite([922(5),49(3),4(4),4(3)]),flip(a)].

937 C * x = x * C. [para(923(a,1),4(a,1,2)),flip(a)].

938 (C \ x) \ x = C. [para(4(a,1),923(a,1,2))].

939 (C * x) / C = x. [para(923(a,1),17(a,1,2))].

942 (C * x) / (x \ C) = x * x. [para(923(a,1),52(a,1,2,2))].

957 (x \ C) * (x \ C) = C * (x \ (x \ C)). [back_rewrite(781),rewrite([937(4,R),396(7),922(5)]),flip(a)].

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

987 C / (C / x) = x. [para(930(a,1),6(a,1,1))].

1008 (C / x) / C = 0 / x. [para(930(a,1),473(a,1,2))].

1010 C / (x / y) = C * (y / x). [para(930(a,1),528(a,1,2)),rewrite([937(3,R)]),flip(a)].

1025 (C / x) * (C / x) = C * (x \ (C / x)). [back_rewrite(957),rewrite([986(2),986(4),986(8)])].

1028 (C * x) / (C / x) = x * x. [back_rewrite(942),rewrite([986(4)])].

1029 C * (0 / x) = C / x. [back_rewrite(922),rewrite([986(6)])].

1046 C * (x / C) = x. [back_rewrite(987),rewrite([1010(4)])].

1059 C * (C * x) = C * (x * C). [para(937(a,1),19(a,2,2)),rewrite([19(4)])].

1069 (C * x) * y = (x * C) * y. [para(937(a,1),24(a,2,1)),rewrite([24(7)])].

1087 (C * (C / x)) / x = C * (x \ (C / x)). [para(937(a,2),41(a,1,1)),rewrite([1025(10)])].

1095 C * (C * (x / (C * y))) = (C * x) / y. [para(937(a,1),88(a,1)),rewrite([937(5,R),937(7,R)])].

1096 (C * x) / y = (x * C) / y. [para(937(a,1),88(a,2,1)),rewrite([937(6,R),1095(7)])].

1190 C \ x = x / C. [para(938(a,1),17(a,1,2)),flip(a)].

1203 C * (x * C) = x * (C * C). [para(939(a,1),23(a,1)),flip(a)].

1209 x \ (C / x) = C / (x * x). [para(986(a,1),49(a,1)),rewrite([986(5)]),flip(a)].

1219 (C * (C / x)) / x = C * (C / (x * x)). [back_rewrite(1087),rewrite([1209(9)])].

1356 (C * (C / x)) * y = C * (x \ (C * y)). [para(1008(a,1),24(a,1,2,1)),rewrite([391(6)]),flip(a)].

1597 x \ (C * (x * y)) = (y / x) * (x * C). [para(937(a,2),97(a,1,2))].

1664 x * (C * (C / x)) = C * C. [para(4(a,1),925(a,1,1)),rewrite([1190(3),1010(4)])].

1684 (C / x) * (C * x) = C * C. [para(1029(a,1),925(a,1,1)),rewrite([1010(6),16(5)])].

1751 (x / C) * (C * (C * y)) = x * (x * ((C / x) * y)). [para(1028(a,1),97(a,2,1)),rewrite([1684(7),19(6),529(7),19(12)])].

1805 (x / C) * (C * (C * y)) = (x / C) * (C * (y * C)). [para(1059(a,1),97(a,2,2)),rewrite([97(7)])].

2443 (x * C) / (C * x) = 0. [para(1096(a,1),15(a,1))].

2591 x * (C * y) = x * (y * C). [para(2443(a,1),99(a,1,1)),rewrite([2443(6),16(3),2(5),2443(8),2(5)]),flip(a)].

2685 C * ((x / C) * (y * (C * C))) = (C * x) * (y * C). [para(1203(a,1),24(a,1,2,2))].

2771 (x / C) * (C * (y * C)) = (x / C) * (y * (C * C)). [para(1203(a,1),97(a,2,2)),rewrite([97(7)])].

3341 x \ ((y / x) * (x * C)) = (C / x) * y. [para(113(a,1),391(a,1)),rewrite([937(4,R),1029(4),529(9),16(8),391(9),1597(7)]),flip(a)].

3677 x \ (C * (C * y)) = C * ((C / x) * y). [para(1664(a,1),97(a,1,2,1)),rewrite([19(4),1219(10),1356(12),49(11),1597(10),3341(11)])].

3837 x * (x * ((C / x) * y)) = C * (x * y). [para(1684(a,1),97(a,1,2,1)),rewrite([19(6),3677(7),1010(5),1046(5),1028(8),19(8)]),flip(a)].

3851 (x / C) * (C * (C * y)) = C * (x * y). [back_rewrite(1751),rewrite([3837(12)])].

3861 (x / C) * (C * (y * C)) = C * (x * y). [back_rewrite(1805),rewrite([3851(7)]),flip(a)].

3868 (x / C) * (y * (C * C)) = C * (x * y). [back_rewrite(2771),rewrite([3861(7)]),flip(a)].

3875 (C * x) * (y * C) = C * (C * (x * y)). [back_rewrite(2685),rewrite([3868(8)]),flip(a)].

4868 (x * C) * (C * y) = C * (C * (x * y)). [para(2591(a,1),1069(a,1)),rewrite([3875(5)]),flip(a)].

4869 (C * x) * (C * y) = (x * C) * (y * C). [para(2591(a,1),1069(a,2))].

4888 (x * C) * (y * C) = C * (C * (x * y)). [para(2591(a,1),113(a,2)),rewrite([113(7),4868(5)]),flip(a)].

4960 (C * x) * (C * y) = C * (C * (x * y)). [back_rewrite(4869),rewrite([4888(10)])].

4961 $F. [resolve(4960,a,27,a)].

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