% Proof 1 at 0.05 (+ 0.00) seconds.

% Length of proof is 31.

% Level of proof is 14.

% Maximum clause weight is 19.000.

% Given clauses 83.

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

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

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

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

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

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

32 A * (((x * A) * y) * A) = A * (x * (A * (y * A))). [para(10(a,1),8(a,1))].

41 A * ((A \ x) * A) = x * A. [para(4(a,1),26(a,1,1)),flip(a)].

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

112 (A \ 0) * A = 0. [para(2(a,1),70(a,1,2)),rewrite([13(3)]),flip(a)].

113 (A \ (x / A)) * A = A \ x. [para(7(a,1),70(a,1,2)),flip(a)].

127 A \ 0 = 0 / A. [para(112(a,1),6(a,1,1)),flip(a)].

128 A * (0 / A) = 0. [para(112(a,1),41(a,2)),rewrite([127(5),113(8),127(4)])].

140 (x * (A * ((y * x) * A))) / A = x * ((A * y) * x). [para(10(a,1),22(a,1,1,2))].

147 (A * x) / (0 / A) = A * (x * A). [para(128(a,1),22(a,1,1,2,2)),rewrite([3(3)])].

498 ((x * A) * y) * A = x * (A * (y * A)). [para(32(a,1),5(a,1,2)),rewrite([5(9)]),flip(a)].

582 x / (0 / A) = x * A. [para(4(a,1),147(a,1,1)),rewrite([41(10)])].

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

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

596 ((x * A) * (y * (x * A))) / A = (x * A) * (y * x). [para(585(a,1),8(a,2,2,2)),rewrite([595(10)])].

601 (x * A) * (y * (x * A)) = x * (A * ((y * x) * A)). [para(585(a,1),22(a,1,1,2,2)),rewrite([582(8),498(6)]),flip(a)].

619 (x * A) * (y * x) = x * ((A * y) * x). [back_rewrite(596),rewrite([601(6),140(8)]),flip(a)].

620 $F. [resolve(619,a,11,a)].

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

% Proof 1 at 0.00 (+ 0.00) seconds.

% Length of proof is 9.

% Level of proof is 3.

% Maximum clause weight is 15.000.

% Given clauses 8.

2 z * (A * (z * y)) = ((z * A) * z) * y # label(non_clause) # label(goal). [goal].

3 0 * x = x. [assumption].

4 x * 0 = x. [assumption].

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

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

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

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

28 (x * A) * x = x * (A * x). [para(3(a,1),11(a,1,2)),rewrite([4(6)])].

39 $F. [back_rewrite(13),rewrite([28(5),9(7)]),xx(a)].

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

% Proof 2 at 0.02 (+ 0.00) seconds.

% Length of proof is 11.

% Level of proof is 4.

% Maximum clause weight is 15.000.

% Given clauses 39.

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

3 0 * x = x. [assumption].

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

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

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

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

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

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

47 A * ((A * x) * A) = A * (A * (x * A)). [para(20(a,1),11(a,1)),flip(a)].

195 (A * x) * A = A * (x * A). [para(47(a,1),6(a,1,2)),rewrite([6(8)]),flip(a)].

202 $F. [back_rewrite(12),rewrite([195(5),9(7)]),xx(a)].

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