% Proof 1 at 0.01 (+ 0.00) seconds.

% Length of proof is 11.

% Level of proof is 4.

% Maximum clause weight is 15.000.

% Given clauses 41.

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

6 0 * x = x. [assumption].

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

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

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

14 (x * y) * (A * x) = x * ((y * A) * x). [copy(13),flip(a)].

20 ((c9 * A) * c9) * c10 != c9 * (A * (c9 * c10)). [deny(5)].

27 (x * x) * y = x * (x * y). [para(6(a,1),12(a,1,1,2)),rewrite([6(5)])].

50 x * ((x * A) * x) = x * (x * (A * x)). [para(27(a,1),14(a,1)),flip(a)].

216 (x * A) * x = x * (A * x). [para(50(a,1),9(a,1,2)),rewrite([9(5)]),flip(a)].

226 $F. [back_rewrite(20),rewrite([216(5),12(7)]),xx(a)].

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

% Proof 2 at 0.19 (+ 0.00) seconds.

% Length of proof is 44.

% Level of proof is 11.

% Maximum clause weight is 19.000.

% Given clauses 150.

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

6 0 * x = x. [assumption].

7 x * 0 = x. [assumption].

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

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

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

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

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

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

14 (x * y) * (A * x) = x * ((y * A) * x). [copy(13),flip(a)].

19 ((A * c7) * A) * c8 != A * (c7 * (A * c8)). [deny(4)].

25 x / (y \ x) = y. [para(8(a,1),10(a,1,1))].

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

27 (x * x) * y = x * (x * y). [para(6(a,1),12(a,1,1,2)),rewrite([6(5)])].

31 (x * (y * (x * z))) / z = x * (y * x). [para(12(a,1),10(a,1,1))].

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

35 x * (((x \ y) * A) * x) = y * (A * x). [para(8(a,1),14(a,1,1)),flip(a)].

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

50 x * ((x * A) * x) = x * (x * (A * x)). [para(27(a,1),14(a,1)),flip(a)].

120 x * ((y / (x * z)) * x) = (x * y) / z. [para(11(a,1),31(a,1,1,2)),flip(a)].

130 (x * y) * (x \ z) = x * ((y / x) * z). [para(8(a,1),32(a,1,2,2)),flip(a)].

216 (x * A) * x = x * (A * x). [para(50(a,1),9(a,1,2)),rewrite([9(5)]),flip(a)].

227 (x * A) \ (x * (A * x)) = x. [para(216(a,1),9(a,1,2))].

386 x * ((0 / x) * y) = y. [para(7(a,1),130(a,1,1)),rewrite([8(2)]),flip(a)].

447 x * (0 / x) = 0. [para(7(a,1),386(a,1,2))].

448 (0 / x) \ y = x * y. [para(8(a,1),386(a,1,2)),flip(a)].

449 (0 / x) * y = x \ y. [para(386(a,1),9(a,1,2)),flip(a)].

452 (x \ y) / y = 0 / x. [para(386(a,1),31(a,1,1,2)),rewrite([449(3),447(7),7(6)])].

491 (x * y) / (0 / x) = x * (y * x). [para(447(a,1),31(a,1,1,2,2)),rewrite([7(2)])].

492 (x * y) * (0 / x) = x * (y / x). [para(447(a,1),32(a,1,2,2)),rewrite([7(3)]),flip(a)].

531 x / (y * x) = 0 / y. [para(448(a,1),25(a,1,2))].

546 A * (0 / x) = A / x. [para(449(a,1),39(a,1)),rewrite([492(5),9(4),6(8)]),flip(a)].

547 x * ((x * y) \ x) = x / y. [para(449(a,1),120(a,1,2)),rewrite([7(5)])].

555 0 / (x / y) = y / x. [para(26(a,1),452(a,1,1)),flip(a)].

557 x / (x * (A * x)) = 0 / (x * A). [para(227(a,1),452(a,1,1))].

639 (x / y) \ z = (y / x) * z. [para(555(a,1),448(a,1,1))].

924 x / (x \ y) = x * (y \ x). [para(8(a,1),547(a,1,2,1)),flip(a)].

925 (x * y) \ x = x \ (x / y). [para(547(a,1),9(a,1,2)),flip(a)].

1876 (x * (A * y)) * (0 / y) = y * ((y \ x) * A). [para(35(a,1),492(a,1,1)),rewrite([10(11)])].

2250 (x \ (x / A)) * A = 0. [para(557(a,1),39(a,1,1)),rewrite([12(9),557(13),1876(14),925(9),449(13),9(11),557(10),546(11),531(9),447(8)])].

2258 x \ (x / A) = 0 / A. [para(2250(a,1),10(a,1,1)),flip(a)].

2298 x / (0 / A) = x * A. [para(2258(a,1),924(a,1,2)),rewrite([639(7),11(7)])].

2441 (A * x) * A = A * (x * A). [para(2298(a,1),491(a,1))].

2548 $F. [back_rewrite(19),rewrite([2441(5),12(7)]),xx(a)].

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

% Proof 3 at 0.52 (+ 0.00) seconds.

% Length of proof is 64.

% Level of proof is 16.

% Maximum clause weight is 23.000.

% Given clauses 233.

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

6 0 * x = x. [assumption].

7 x * 0 = x. [assumption].

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

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

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

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

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

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

14 (x * y) * (A * x) = x * ((y * A) * x). [copy(13),flip(a)].

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

25 x / (y \ x) = y. [para(8(a,1),10(a,1,1))].

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

27 (x * x) * y = x * (x * y). [para(6(a,1),12(a,1,1,2)),rewrite([6(5)])].

31 (x * (y * (x * z))) / z = x * (y * x). [para(12(a,1),10(a,1,1))].

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

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

35 x * (((x \ y) * A) * x) = y * (A * x). [para(8(a,1),14(a,1,1)),flip(a)].

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

50 x * ((x * A) * x) = x * (x * (A * x)). [para(27(a,1),14(a,1)),flip(a)].

120 x * ((y / (x * z)) * x) = (x * y) / z. [para(11(a,1),31(a,1,1,2)),flip(a)].

122 (x * (y * (z * (y * (x * u))))) / u = x * (y * (z * (y * x))). [para(12(a,1),31(a,1,1,2)),rewrite([12(9)])].

124 (A * (x * ((y * A) * x))) / x = A * ((x * y) * A). [para(14(a,1),31(a,1,1,2))].

130 (x * y) * (x \ z) = x * ((y / x) * z). [para(8(a,1),32(a,1,2,2)),flip(a)].

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

216 (x * A) * x = x * (A * x). [para(50(a,1),9(a,1,2)),rewrite([9(5)]),flip(a)].

227 (x * A) \ (x * (A * x)) = x. [para(216(a,1),9(a,1,2))].

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

386 x * ((0 / x) * y) = y. [para(7(a,1),130(a,1,1)),rewrite([8(2)]),flip(a)].

447 x * (0 / x) = 0. [para(7(a,1),386(a,1,2))].

448 (0 / x) \ y = x * y. [para(8(a,1),386(a,1,2)),flip(a)].

449 (0 / x) * y = x \ y. [para(386(a,1),9(a,1,2)),flip(a)].

452 (x \ y) / y = 0 / x. [para(386(a,1),31(a,1,1,2)),rewrite([449(3),447(7),7(6)])].

455 (x * (y \ x)) * z = x * (y \ (x * z)). [para(386(a,1),33(a,1,1,2,2)),rewrite([449(3),449(9),8(8),449(7)])].

491 (x * y) / (0 / x) = x * (y * x). [para(447(a,1),31(a,1,1,2,2)),rewrite([7(2)])].

492 (x * y) * (0 / x) = x * (y / x). [para(447(a,1),32(a,1,2,2)),rewrite([7(3)]),flip(a)].

531 x / (y * x) = 0 / y. [para(448(a,1),25(a,1,2))].

546 A * (0 / x) = A / x. [para(449(a,1),39(a,1)),rewrite([492(5),9(4),6(8)]),flip(a)].

547 x * ((x * y) \ x) = x / y. [para(449(a,1),120(a,1,2)),rewrite([7(5)])].

555 0 / (x / y) = y / x. [para(26(a,1),452(a,1,1)),flip(a)].

557 x / (x * (A * x)) = 0 / (x * A). [para(227(a,1),452(a,1,1))].

625 A * ((x / (A / y)) * A) = (A * x) / (0 / y). [para(546(a,1),120(a,1,2,1,2))].

639 (x / y) \ z = (y / x) * z. [para(555(a,1),448(a,1,1))].

924 x / (x \ y) = x * (y \ x). [para(8(a,1),547(a,1,2,1)),flip(a)].

925 (x * y) \ x = x \ (x / y). [para(547(a,1),9(a,1,2)),flip(a)].

1347 x * ((x \ y) * x) = y / (0 / x). [para(8(a,1),491(a,1,1)),flip(a)].

1862 x * ((x \ y) / x) = y * (0 / x). [para(8(a,1),492(a,1,1)),flip(a)].

1876 (x * (A * y)) * (0 / y) = y * ((y \ x) * A). [para(35(a,1),492(a,1,1)),rewrite([10(11)])].

2250 (x \ (x / A)) * A = 0. [para(557(a,1),39(a,1,1)),rewrite([12(9),557(13),1876(14),925(9),449(13),9(11),557(10),546(11),531(9),447(8)])].

2258 x \ (x / A) = 0 / A. [para(2250(a,1),10(a,1,1)),flip(a)].

2267 A \ (x * (y * (x * (0 / A)))) = (A \ (x * (y * x))) / A. [para(2250(a,1),122(a,1,1,2,2,2,2)),rewrite([2258(3),7(5),449(6),2258(9),2258(

12),449(16)]),flip(a)].

2284 x * (0 / A) = x / A. [para(2258(a,1),8(a,1,2))].

2298 x / (0 / A) = x * A. [para(2258(a,1),924(a,1,2)),rewrite([639(7),11(7)])].

2306 A \ (x * (y * (x / A))) = (A \ (x * (y * x))) / A. [back_rewrite(2267),rewrite([2284(5)])].

2393 (A * (x * (y * x))) / x = A * ((x * (y / A)) * A). [para(11(a,1),124(a,1,1,2,2,1))].

2441 (A * x) * A = A * (x * A). [para(2298(a,1),491(a,1))].

2957 ((x \ y) / x) * (x * z) = x \ (y * z). [para(8(a,1),131(a,1,2,1)),flip(a)].

5607 x / (A / y) = x * (y / A). [para(1862(a,1),35(a,2,2)),rewrite([639(9),924(8),455(9),2441(11),12(16),1862(14),2284(12),2957(13),2306(9),

1347(6),359(7),546(4),10(7),2284(7)])].

5740 A * ((x * (y / A)) * A) = (A * x) / (0 / y). [back_rewrite(625),rewrite([5607(4)])].

5765 (A * (x * (y * x))) / x = (A * x) / (0 / y). [back_rewrite(2393),rewrite([5740(12)])].

5772 (A * x) / (0 / (y * A)) = A * ((x * y) * A). [back_rewrite(124),rewrite([5765(7)])].

5778 x / (0 / y) = x * y. [para(10(a,1),5607(a,2,2)),rewrite([531(4)])].

5827 (A * x) * (y * A) = A * ((x * y) * A). [back_rewrite(5772),rewrite([5778(7)])].

5828 $F. [resolve(5827,a,16,a)].

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

% Proof 4 at 0.54 (+ 0.00) seconds.

% Length of proof is 59.

% Level of proof is 14.

% Maximum clause weight is 23.000.

% Given clauses 233.

3 (z * (x * A)) * z = (z * x) * (A * z) # label(non_clause) # label(goal). [goal].

6 0 * x = x. [assumption].

7 x * 0 = x. [assumption].

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

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

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

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

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

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

14 (x * y) * (A * x) = x * ((y * A) * x). [copy(13),flip(a)].

17 (c5 * (c6 * A)) * c5 != (c5 * c6) * (A * c5). [deny(3)].

18 (c5 * (c6 * A)) * c5 != c5 * ((c6 * A) * c5). [copy(17),rewrite([14(14)])].

25 x / (y \ x) = y. [para(8(a,1),10(a,1,1))].

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

27 (x * x) * y = x * (x * y). [para(6(a,1),12(a,1,1,2)),rewrite([6(5)])].

31 (x * (y * (x * z))) / z = x * (y * x). [para(12(a,1),10(a,1,1))].

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

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

35 x * (((x \ y) * A) * x) = y * (A * x). [para(8(a,1),14(a,1,1)),flip(a)].

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

50 x * ((x * A) * x) = x * (x * (A * x)). [para(27(a,1),14(a,1)),flip(a)].

120 x * ((y / (x * z)) * x) = (x * y) / z. [para(11(a,1),31(a,1,1,2)),flip(a)].

122 (x * (y * (z * (y * (x * u))))) / u = x * (y * (z * (y * x))). [para(12(a,1),31(a,1,1,2)),rewrite([12(9)])].

130 (x * y) * (x \ z) = x * ((y / x) * z). [para(8(a,1),32(a,1,2,2)),flip(a)].

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

216 (x * A) * x = x * (A * x). [para(50(a,1),9(a,1,2)),rewrite([9(5)]),flip(a)].

227 (x * A) \ (x * (A * x)) = x. [para(216(a,1),9(a,1,2))].

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

386 x * ((0 / x) * y) = y. [para(7(a,1),130(a,1,1)),rewrite([8(2)]),flip(a)].

447 x * (0 / x) = 0. [para(7(a,1),386(a,1,2))].

448 (0 / x) \ y = x * y. [para(8(a,1),386(a,1,2)),flip(a)].

449 (0 / x) * y = x \ y. [para(386(a,1),9(a,1,2)),flip(a)].

452 (x \ y) / y = 0 / x. [para(386(a,1),31(a,1,1,2)),rewrite([449(3),447(7),7(6)])].

455 (x * (y \ x)) * z = x * (y \ (x * z)). [para(386(a,1),33(a,1,1,2,2)),rewrite([449(3),449(9),8(8),449(7)])].

491 (x * y) / (0 / x) = x * (y * x). [para(447(a,1),31(a,1,1,2,2)),rewrite([7(2)])].

492 (x * y) * (0 / x) = x * (y / x). [para(447(a,1),32(a,1,2,2)),rewrite([7(3)]),flip(a)].

531 x / (y * x) = 0 / y. [para(448(a,1),25(a,1,2))].

546 A * (0 / x) = A / x. [para(449(a,1),39(a,1)),rewrite([492(5),9(4),6(8)]),flip(a)].

547 x * ((x * y) \ x) = x / y. [para(449(a,1),120(a,1,2)),rewrite([7(5)])].

555 0 / (x / y) = y / x. [para(26(a,1),452(a,1,1)),flip(a)].

557 x / (x * (A * x)) = 0 / (x * A). [para(227(a,1),452(a,1,1))].

639 (x / y) \ z = (y / x) * z. [para(555(a,1),448(a,1,1))].

924 x / (x \ y) = x * (y \ x). [para(8(a,1),547(a,1,2,1)),flip(a)].

925 (x * y) \ x = x \ (x / y). [para(547(a,1),9(a,1,2)),flip(a)].

1347 x * ((x \ y) * x) = y / (0 / x). [para(8(a,1),491(a,1,1)),flip(a)].

1862 x * ((x \ y) / x) = y * (0 / x). [para(8(a,1),492(a,1,1)),flip(a)].

1876 (x * (A * y)) * (0 / y) = y * ((y \ x) * A). [para(35(a,1),492(a,1,1)),rewrite([10(11)])].

2250 (x \ (x / A)) * A = 0. [para(557(a,1),39(a,1,1)),rewrite([12(9),557(13),1876(14),925(9),449(13),9(11),557(10),546(11),531(9),447(8)])].

2258 x \ (x / A) = 0 / A. [para(2250(a,1),10(a,1,1)),flip(a)].

2267 A \ (x * (y * (x * (0 / A)))) = (A \ (x * (y * x))) / A. [para(2250(a,1),122(a,1,1,2,2,2,2)),rewrite([2258(3),7(5),449(6),2258(9),2258(

12),449(16)]),flip(a)].

2284 x * (0 / A) = x / A. [para(2258(a,1),8(a,1,2))].

2298 x / (0 / A) = x * A. [para(2258(a,1),924(a,1,2)),rewrite([639(7),11(7)])].

2306 A \ (x * (y * (x / A))) = (A \ (x * (y * x))) / A. [back_rewrite(2267),rewrite([2284(5)])].

2441 (A * x) * A = A * (x * A). [para(2298(a,1),491(a,1))].

2957 ((x \ y) / x) * (x * z) = x \ (y * z). [para(8(a,1),131(a,1,2,1)),flip(a)].

5607 x / (A / y) = x * (y / A). [para(1862(a,1),35(a,2,2)),rewrite([639(9),924(8),455(9),2441(11),12(16),1862(14),2284(12),2957(13),2306(9),

1347(6),359(7),546(4),10(7),2284(7)])].

5778 x / (0 / y) = x * y. [para(10(a,1),5607(a,2,2)),rewrite([531(4)])].

6014 (x * y) * x = x * (y * x). [back_rewrite(491),rewrite([5778(4)])].

6015 $F. [resolve(6014,a,18,a)].

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

% Proof 5 at 3.26 (+ 0.02) seconds.

% Length of proof is 62.

% Level of proof is 16.

% Maximum clause weight is 23.000.

% Given clauses 357.

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

6 0 * x = x. [assumption].

7 x * 0 = x. [assumption].

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

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

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

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

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

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

14 (x * y) * (A * x) = x * ((y * A) * x). [copy(13),flip(a)].

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

25 x / (y \ x) = y. [para(8(a,1),10(a,1,1))].

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

27 (x * x) * y = x * (x * y). [para(6(a,1),12(a,1,1,2)),rewrite([6(5)])].

31 (x * (y * (x * z))) / z = x * (y * x). [para(12(a,1),10(a,1,1))].

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

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

35 x * (((x \ y) * A) * x) = y * (A * x). [para(8(a,1),14(a,1,1)),flip(a)].

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

50 x * ((x * A) * x) = x * (x * (A * x)). [para(27(a,1),14(a,1)),flip(a)].

120 x * ((y / (x * z)) * x) = (x * y) / z. [para(11(a,1),31(a,1,1,2)),flip(a)].

122 (x * (y * (z * (y * (x * u))))) / u = x * (y * (z * (y * x))). [para(12(a,1),31(a,1,1,2)),rewrite([12(9)])].

130 (x * y) * (x \ z) = x * ((y / x) * z). [para(8(a,1),32(a,1,2,2)),flip(a)].

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

216 (x * A) * x = x * (A * x). [para(50(a,1),9(a,1,2)),rewrite([9(5)]),flip(a)].

227 (x * A) \ (x * (A * x)) = x. [para(216(a,1),9(a,1,2))].

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

386 x * ((0 / x) * y) = y. [para(7(a,1),130(a,1,1)),rewrite([8(2)]),flip(a)].

447 x * (0 / x) = 0. [para(7(a,1),386(a,1,2))].

448 (0 / x) \ y = x * y. [para(8(a,1),386(a,1,2)),flip(a)].

449 (0 / x) * y = x \ y. [para(386(a,1),9(a,1,2)),flip(a)].

452 (x \ y) / y = 0 / x. [para(386(a,1),31(a,1,1,2)),rewrite([449(3),447(7),7(6)])].

455 (x * (y \ x)) * z = x * (y \ (x * z)). [para(386(a,1),33(a,1,1,2,2)),rewrite([449(3),449(9),8(8),449(7)])].

491 (x * y) / (0 / x) = x * (y * x). [para(447(a,1),31(a,1,1,2,2)),rewrite([7(2)])].

492 (x * y) * (0 / x) = x * (y / x). [para(447(a,1),32(a,1,2,2)),rewrite([7(3)]),flip(a)].

531 x / (y * x) = 0 / y. [para(448(a,1),25(a,1,2))].

546 A * (0 / x) = A / x. [para(449(a,1),39(a,1)),rewrite([492(5),9(4),6(8)]),flip(a)].

547 x * ((x * y) \ x) = x / y. [para(449(a,1),120(a,1,2)),rewrite([7(5)])].

555 0 / (x / y) = y / x. [para(26(a,1),452(a,1,1)),flip(a)].

557 x / (x * (A * x)) = 0 / (x * A). [para(227(a,1),452(a,1,1))].

639 (x / y) \ z = (y / x) * z. [para(555(a,1),448(a,1,1))].

924 x / (x \ y) = x * (y \ x). [para(8(a,1),547(a,1,2,1)),flip(a)].

925 (x * y) \ x = x \ (x / y). [para(547(a,1),9(a,1,2)),flip(a)].

1347 x * ((x \ y) * x) = y / (0 / x). [para(8(a,1),491(a,1,1)),flip(a)].

1862 x * ((x \ y) / x) = y * (0 / x). [para(8(a,1),492(a,1,1)),flip(a)].

1876 (x * (A * y)) * (0 / y) = y * ((y \ x) * A). [para(35(a,1),492(a,1,1)),rewrite([10(11)])].

2250 (x \ (x / A)) * A = 0. [para(557(a,1),39(a,1,1)),rewrite([12(9),557(13),1876(14),925(9),449(13),9(11),557(10),546(11),531(9),447(8)])].

2258 x \ (x / A) = 0 / A. [para(2250(a,1),10(a,1,1)),flip(a)].

2267 A \ (x * (y * (x * (0 / A)))) = (A \ (x * (y * x))) / A. [para(2250(a,1),122(a,1,1,2,2,2,2)),rewrite([2258(3),7(5),449(6),2258(9),2258(

12),449(16)]),flip(a)].

2284 x * (0 / A) = x / A. [para(2258(a,1),8(a,1,2))].

2298 x / (0 / A) = x * A. [para(2258(a,1),924(a,1,2)),rewrite([639(7),11(7)])].

2306 A \ (x * (y * (x / A))) = (A \ (x * (y * x))) / A. [back_rewrite(2267),rewrite([2284(5)])].

2441 (A * x) * A = A * (x * A). [para(2298(a,1),491(a,1))].

2957 ((x \ y) / x) * (x * z) = x \ (y * z). [para(8(a,1),131(a,1,2,1)),flip(a)].

5607 x / (A / y) = x * (y / A). [para(1862(a,1),35(a,2,2)),rewrite([639(9),924(8),455(9),2441(11),12(16),1862(14),2284(12),2957(13),2306(9),

1347(6),359(7),546(4),10(7),2284(7)])].

5778 x / (0 / y) = x * y. [para(10(a,1),5607(a,2,2)),rewrite([531(4)])].

5780 x * (0 / y) = x / y. [para(25(a,1),5607(a,1,2)),rewrite([452(5)]),flip(a)].

6849 x * ((y / (x / z)) * x) = (x * y) * z. [para(5778(a,1),120(a,2)),rewrite([5780(3)])].

6852 x / (y / z) = x * (z / y). [para(555(a,1),5778(a,1,2))].

7052 x * ((y * (z / x)) * x) = (x * y) * z. [back_rewrite(6849),rewrite([6852(2)])].

19950 (x * y) * (z * x) = x * ((y * z) * x). [para(10(a,1),7052(a,1,2,1,2)),flip(a)].

19951 $F. [resolve(19950,a,15,a)].

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