% Proof 1 at 0.00 (+ 0.00) seconds.

% Length of proof is 13.

% Level of proof is 4.

% Maximum clause weight is 15.000.

% Given clauses 9.

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

2 0 * x = x. [assumption].

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

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

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

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

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

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

14 (C * x) * (y * C) = C * (C * (x * y)). [back_rewrite(10),rewrite([11(9,R)])].

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

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

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

52 $F. [resolve(51,a,29,a)].

% Proof 1 at 0.23 (+ 0.00) seconds.

% Length of proof is 55.

% Level of proof is 18.

% Maximum clause weight is 23.000.

% Given clauses 128.

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

2 0 * x = x. [assumption].

3 x * 0 = x. [assumption].

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

30 (C * x) * C = C * (x * C). [para(2(a,1),10(a,1,2)),rewrite([3(7)])].

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

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

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

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

48 (C * (x * C)) / C = C * x. [para(30(a,1),6(a,1,1))].

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

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

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

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

117 (C \ 0) * C = 0. [para(2(a,1),77(a,1,2)),rewrite([15(3)]),flip(a)].

118 (C \ (x / C)) * C = C \ x. [para(7(a,1),77(a,1,2)),flip(a)].

132 C \ 0 = 0 / C. [para(117(a,1),6(a,1,1)),flip(a)].

133 C * (0 / C) = 0. [para(117(a,1),46(a,2)),rewrite([132(5),118(8),132(4)])].

136 C / (0 / C) = C * C. [para(132(a,1),69(a,1,2)),rewrite([3(3)])].

137 C * (((0 / C) * x) * C) = x * C. [para(133(a,1),10(a,1,1)),rewrite([2(4)]),flip(a)].

160 C * ((C \ x) / C) = x / C. [para(4(a,1),87(a,1,1)),flip(a)].

184 (0 / C) * (C * (C * ((0 / C) * x))) = x. [para(136(a,1),25(a,1,2,1)),rewrite([20(11),7(17),2(14)])].

272 C * (C * x) = C * (x * C). [para(3(a,1),29(a,1,2)),rewrite([30(4),3(8)]),flip(a)].

290 C * (C * ((0 / C) * x)) = C * x. [para(133(a,1),29(a,1,1)),rewrite([2(4)]),flip(a)].

318 C * x = x * C. [back_rewrite(137),rewrite([272(8,R),290(8)])].

329 C * (C * (x * (y / C))) = (C * x) * y. [back_rewrite(34),rewrite([318(6,R)])].

336 (0 / C) * (C * x) = x. [back_rewrite(184),rewrite([290(11)])].

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

375 C * (x / C) = x. [para(318(a,2),6(a,1,1)),rewrite([87(4)])].

388 C \ x = x / C. [para(318(a,1),160(a,1)),rewrite([318(6,R),375(6)])].

458 (0 / C) * x = x / C. [para(4(a,1),336(a,1,2)),rewrite([388(6)])].

468 (x * (x / C)) * y = x * ((x * y) / C). [para(336(a,1),26(a,1,1,2)),rewrite([458(4),458(13),375(12),458(9)])].

869 (x * (0 / C)) \ x = C. [para(458(a,1),84(a,1,1,2)),rewrite([375(8),318(13,R),375(13),3(10),458(9),375(8)])].

881 x \ (x / (0 / C)) = C. [para(7(a,1),869(a,1,1))].

883 x * (0 / C) = x / C. [para(869(a,1),18(a,1,2)),flip(a)].

895 x / (0 / C) = x * C. [para(881(a,1),4(a,1,2)),flip(a)].

902 C * (x * (x / C)) = x * x. [para(883(a,1),40(a,1,1,2)),rewrite([895(7),318(5,R)])].

1735 (C * x) * (x * y) = x * (x * (C * y)). [para(902(a,1),29(a,1,1)),rewrite([20(4),468(10),329(12)]),flip(a)].

1736 $F. [resolve(1735,a,361,a)].

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

% Proof 1 at 0.03 (+ 0.00) seconds.

% Length of proof is 21.

% Level of proof is 6.

% Maximum clause weight is 15.000.

% Given clauses 68.

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

2 0 * x = x. [assumption].

3 x * 0 = x. [assumption].

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

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

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

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

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

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

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

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

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

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

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

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

30 (C * x) * C = C * (x * C). [para(2(a,1),10(a,1,2)),rewrite([3(7)])].

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

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

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

456 C * x = x * C. [para(10(a,1),370(a,1,2)),rewrite([30(4),8(10),120(12),5(6)]),flip(a)].

457 $F. [resolve(456,a,14,a(flip))].

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