% Proof 1 at 0.00 (+ 0.00) seconds.

% Length of proof is 8.

% Level of proof is 2.

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

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

27 (x * A) * x = x * (A * x). [para(3(a,1),10(a,1,1,2)),rewrite([4(5)])].

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

% Proof 2 at 0.41 (+ 0.01) seconds.

% Length of proof is 101.

% Level of proof is 24.

% Maximum clause weight is 25.000.

% Given clauses 216.

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

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

15 x / x = 0. [para(3(a,1),7(a,1,1))].

16 x / 0 = x. [para(4(a,1),7(a,1,1))].

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

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

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

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

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

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

27 (x * A) * x = x * (A * x). [para(3(a,1),10(a,1,1,2)),rewrite([4(5)])].

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

29 ((x * y) * (A * x)) / x = x * (y * A). [para(10(a,1),7(a,1,1))].

30 (x * (y / A)) * (A * x) = (x * y) * x. [para(8(a,1),10(a,1,1,2)),flip(a)].

33 (A * x) * (A * A) = A * (x * (A * A)). [para(10(a,1),9(a,1))].

40 (x * (x * y)) / y = x * x. [para(19(a,1),7(a,1,1))].

43 (x * (y * (y * A))) * x = (x * (y * y)) * (A * x). [para(19(a,1),10(a,1,1,2))].

46 (x * A) \ (x * (A * x)) = x. [para(27(a,1),6(a,1,2))].

48 (x / A) * (A * (x / A)) = x * (x / A). [para(8(a,1),27(a,1,1)),flip(a)].

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

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

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

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

111 (0 / x) \ ((0 / x) / x) = 0 / x. [para(96(a,1),6(a,1,2))].

114 (0 / x) * ((0 / x) * y) = ((0 / x) / x) * y. [para(96(a,1),19(a,1,1)),flip(a)].

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

127 ((x * A) * (y * (x * (A * x)))) / x = (x * A) * (y * (x * A)). [para(27(a,1),23(a,1,1,2,2))].

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

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

169 (x * (A * y)) / y = y * ((y \ x) * A). [para(5(a,1),29(a,1,1,1))].

170 (((A \ x) * y) * x) / (A \ x) = (A \ x) * (y * A). [para(5(a,1),29(a,1,1,2))].

288 ((A \ 0) * A) \ (A \ 0) = A \ 0. [para(4(a,1),71(a,1,2))].

307 (A \ 0) * A = 0. [para(288(a,1),17(a,1,2)),rewrite([15(7)]),flip(a)].

309 A \ 0 = 0 / A. [para(307(a,1),7(a,1,1)),flip(a)].

312 ((0 / A) * (A * A)) \ (A * (0 / A)) = 0 / A. [para(307(a,1),28(a,1,2,1)),rewrite([309(3),309(12),3(14),309(16)])].

313 A * (0 / A) = 0. [para(309(a,1),5(a,1,2))].

314 0 / (0 / A) = A. [para(309(a,1),17(a,1,2))].

317 ((0 / A) * (A * A)) \ 0 = 0 / A. [back_rewrite(312),rewrite([313(12)])].

318 (A * x) / (0 / A) = A * (x * A). [para(313(a,1),23(a,1,1,2,2)),rewrite([4(3)])].

319 (A * x) * (0 / A) = A * (x / A). [para(313(a,1),24(a,1,2,2)),rewrite([4(5)]),flip(a)].

320 ((0 / A) * (x * A)) \ ((0 / A) * x) = 0 / A. [para(313(a,1),28(a,1,2,2)),rewrite([4(12)])].

321 ((0 / A) * x) * (0 / A) = (0 / A) * (x / A). [para(313(a,1),30(a,1,2)),rewrite([4(8)]),flip(a)].

362 (0 / A) * (A * A) = A. [para(317(a,1),17(a,1,2)),rewrite([314(5)]),flip(a)].

400 (0 / A) / A = 0 / (A * A). [para(362(a,1),40(a,1,1,2)),rewrite([8(5),96(12)]),flip(a)].

413 (0 / A) \ (0 / (A * A)) = 0 / A. [para(400(a,1),111(a,1,2))].

415 A * ((0 / (A * A)) * (A * x)) = x. [para(400(a,1),24(a,1,2,1)),rewrite([313(15),3(12)])].

417 (0 / (A * A)) * (A * (0 / (A * A))) = (0 / A) * (0 / (A * A)). [para(400(a,1),48(a,1,1)),rewrite([400(11),400(21)])].

470 A * ((A \ x) * A) = x / (0 / A). [para(5(a,1),318(a,1,1)),flip(a)].

471 (A * (x * A)) \ (A * x) = 0 / A. [para(318(a,1),18(a,1,1))].

483 A * (0 / (A * A)) = 0 / A. [para(313(a,1),319(a,1,1)),rewrite([3(5),400(9)]),flip(a)].

486 (0 / (A * A)) * (0 / A) = (0 / A) * (0 / (A * A)). [back_rewrite(417),rewrite([483(12)])].

581 ((0 / A) * (0 / (A * A))) * x = (0 / A) * ((0 / (A * A)) * x). [para(413(a,1),21(a,1,1)),rewrite([413(15),114(11),400(8),413(19)]),flip(a)].

585 (0 / (A * A)) * (A * x) = A \ x. [para(415(a,1),6(a,1,2)),flip(a)].

586 (0 / (A * A)) * x = (0 / A) * (A \ x). [para(415(a,1),9(a,2,2)),rewrite([483(12),486(9),581(12),585(11)]),flip(a)].

599 (A * (((0 / A) * x) * A)) \ (x * (A * A)) = A. [para(415(a,1),28(a,1,2,1)),rewrite([586(9),6(8)])].

625 (0 / A) * x = A \ x. [back_rewrite(585),rewrite([586(8),6(7)])].

636 (x / (0 / A)) \ (x * (A * A)) = A. [back_rewrite(599),rewrite([625(5),470(6)])].

653 (A \ x) * (0 / A) = A \ (x / A). [back_rewrite(321),rewrite([625(4),625(12)])].

654 (A \ (x * A)) \ (A \ x) = 0 / A. [back_rewrite(320),rewrite([625(6),625(8)])].

755 A * ((A \ x) * (A * y)) = (x / (0 / A)) * y. [para(470(a,1),9(a,1,1)),flip(a)].

757 (x / (0 / A)) * A = x * (A * A). [para(470(a,1),10(a,1,1)),rewrite([5(10)])].

791 (A * (((A \ x) * A) * A)) \ (x / (0 / A)) = 0 / A. [para(470(a,1),471(a,1,2))].

831 ((x / (A * A)) / (0 / A)) \ x = A. [para(8(a,1),636(a,1,2))].

866 A \ ((A * x) / A) = x * (0 / A). [para(6(a,1),653(a,1,1)),flip(a)].

885 ((x / A) * (A * A)) \ x = 0 / A. [para(6(a,1),654(a,1,2)),rewrite([134(6)])].

1096 (x / (A * A)) / (0 / A) = x / A. [para(831(a,1),17(a,1,2)),flip(a)].

1125 (x * (A * A)) * (0 / A) = x * A. [para(23(a,1),866(a,1,2)),rewrite([6(6)]),flip(a)].

1146 (x / A) * (A * A) = x / (0 / A). [para(885(a,1),17(a,1,2)),flip(a)].

1315 A * (x / (0 / A)) = (A * x) * A. [para(33(a,1),1125(a,1,1)),rewrite([319(10),169(7),470(7)])].

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

1520 (x / (0 / A)) / A = (x / A) / (0 / A). [para(1351(a,1),1096(a,1,1)),flip(a)].

1827 x * ((0 / x) * y) = y. [para(4(a,1),133(a,1,1)),rewrite([5(2)]),flip(a)].

1895 x * (0 / x) = 0. [para(4(a,1),1827(a,1,2))].

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

1897 (0 / x) * y = x \ y. [para(1827(a,1),6(a,1,2)),flip(a)].

1900 (x \ y) / y = 0 / x. [para(1827(a,1),23(a,1,1,2)),rewrite([1897(3),1895(7),4(6)])].

1907 x \ (A * x) = (x \ A) * x. [para(1827(a,1),43(a,1,1)),rewrite([1897(4),1897(8),5(7),1897(8)]),flip(a)].

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

2068 x * ((x * y) \ x) = x / y. [para(1897(a,1),121(a,1,2)),rewrite([4(5)])].

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

2176 (x / y) \ z = (y / x) * z. [para(2070(a,1),1896(a,1,1))].

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

2385 (x / (0 / A)) * ((x * (A * A)) \ (x / (0 / A))) = (x / A) / (0 / A). [para(757(a,1),2068(a,1,2,1)),rewrite([1520(20)])].

2463 A * (0 / x) = A / x. [para(2284(a,1),1897(a,1)),rewrite([2176(8),16(6),1962(9),6(8)])].

2584 A \ (A / x) = 0 / x. [para(2463(a,1),6(a,1,2))].

2620 0 / (x \ A) = A \ x. [para(17(a,1),2584(a,1,2)),flip(a)].

2650 (x \ A) * ((A \ x) * y) = y. [para(2620(a,1),133(a,2,2,1)),rewrite([4(4),5(6)]),flip(a)].

4292 ((A \ x) * A) * A = (A \ x) * (A * A). [para(2650(a,1),127(a,1,1,2)),rewrite([5(8),170(8),2650(17)]),flip(a)].

4313 (x * (A * A)) \ (x / (0 / A)) = 0 / A. [back_rewrite(791),rewrite([4292(7),755(8),757(6)])].

4318 (x / A) / (0 / A) = x. [back_rewrite(2385),rewrite([4313(13),8(8)]),flip(a)].

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

4511 (A * x) * A = A * (x * A). [back_rewrite(1315),rewrite([4340(5)]),flip(a)].

4943 $F. [back_rewrite(11),rewrite([4511(5),9(7)]),xx(a)].

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