% Length of proof is 231.

% Level of proof is 32.

% Maximum clause weight is 31.

% Given clauses 178.

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

2 1 * x = x. [assumption].

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

9 (x * y) * (y * z) = y * ((y * x) * z). [copy(8),flip(a)].

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

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

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

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

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

15 x * A = A * x. [assumption].

16 A * x = x * A. [copy(15),flip(a)].

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

18 (A * c1) * c2 != c1 * (A * c2). [copy(17),rewrite([16(3,R)])].

19 A * (x * y) = x * (y * A). [back_rewrite(14),rewrite([16(3,R)])].

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

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

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

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

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

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

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

36 (x * (x * y)) / x = y * x. [para(10(a,1),6(a,1,1))].

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

42 (x / y) * (y * z) = y * ((y \ x) * z). [para(4(a,1),12(a,1,1,1))].

43 ((x * y) / x) * z = x * (y * (x \ z)). [para(4(a,1),12(a,1,2))].

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

55 (x * A) / x = A. [para(16(a,1),6(a,1,1))].

57 A * (x / A) = x. [para(16(a,2),7(a,1))].

64 (x * A) * x = x * (x * A). [para(16(a,1),10(a,1,1))].

66 x * (A * (x \ y)) = A * y. [para(4(a,1),19(a,1,2)),rewrite([16(5,R)]),flip(a)].

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

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

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

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

82 (x * A) * ((x * A) * y) = A * ((A * (y * x)) * x). [para(19(a,2),10(a,1,1)),rewrite([19(6,R)]),flip(a)].

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

85 A * (A * x) = x * (A * A). [para(16(a,2),19(a,1,2))].

86 A * (x * y) = x * (A * y). [para(16(a,2),19(a,2,2))].

89 (A * c1) * c2 != A * (c1 * c2). [back_rewrite(18),rewrite([86(10,R)])].

90 A \ x = x / A. [para(7(a,1),53(a,1,2))].

94 (A * x) * y = (x * A) * y. [para(57(a,1),9(a,1,2)),rewrite([72(10)]),flip(a)].

95 (x / A) * x = x * (x / A). [para(57(a,1),10(a,1,1)),rewrite([16(9,R),57(9)]),flip(a)].

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

101 (x \ A) * x = A. [back_rewrite(55),rewrite([96(3)])].

111 ((x \ y) * x) * z = x * (y * (x \ z)). [back_rewrite(43),rewrite([96(2)])].

113 (x \ A) \ A = x. [para(101(a,1),5(a,1,2))].

114 x \ A = A / x. [para(101(a,1),6(a,1,1)),flip(a)].

115 x * (A / x) = A. [para(25(a,1),101(a,1,1))].

116 A / (A / x) = x. [back_rewrite(113),rewrite([114(2),114(4)])].

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

120 (x * y) / (y * (x / y)) = y. [para(37(a,1),6(a,1,1))].

124 x * (A * (x * (y / x))) = A * (y * x). [para(37(a,1),19(a,1,2)),rewrite([16(7,R)]),flip(a)].

132 x \ (A * y) = A * (x \ y). [para(66(a,1),5(a,1,2))].

138 x * (A * (A * (x \ y))) = A * (A * y). [para(66(a,1),19(a,1,2)),rewrite([16(9,R)]),flip(a)].

148 (A * x) / (y * A) = x / y. [para(7(a,1),70(a,1,1,2))].

156 (x / (y * A)) * y = x / A. [para(71(a,1),5(a,1,2)),rewrite([90(2)]),flip(a)].

163 (x * y) / A = x * (y / A). [para(72(a,1),5(a,1,2)),rewrite([90(3)])].

164 (x / (y / A)) * y = A * x. [para(7(a,1),72(a,1,2)),flip(a)].

196 A * (x * (y * z)) = x * (y * (z * A)) # label(flip_matches_hint). [para(19(a,1),86(a,2,2))].

203 (A * x) * ((x * A) \ y) = y. [para(94(a,2),4(a,1))].

222 (A * (A * x)) * y = (x * (A * A)) * y. [para(85(a,1),94(a,1,1)),rewrite([16(9,R)]),flip(a)].

229 (x \ 1) * x = 1. [para(3(a,1),96(a,1,1)),rewrite([22(1)]),flip(a)].

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

231 ((x / y) \ y) * (x / y) = x / (x / y). [para(7(a,1),96(a,1,1)),flip(a)].

234 (A * (x * y)) / x = (x \ (y * A)) * x. [para(19(a,2),96(a,1,1))].

236 (x \ (A / x)) * x = A / x. [para(115(a,1),96(a,1,1)),flip(a)].

241 (x \ (y * A)) * x = (A * (x \ y)) * x. [para(86(a,2),96(a,1,1)),rewrite([234(4),132(7)])].

244 (A * (x * y)) / x = (A * (x \ y)) * x. [back_rewrite(234),rewrite([241(8)])].

245 (x \ 1) \ 1 = x. [para(229(a,1),5(a,1,2))].

246 x \ 1 = 1 / x. [para(229(a,1),6(a,1,1)),flip(a)].

247 x * (1 / x) = 1. [para(25(a,1),229(a,1,1))].

248 x / (x * (1 / A)) = A. [para(229(a,1),69(a,1,1,2)),rewrite([3(2),246(3)])].

249 1 / (1 / x) = x. [back_rewrite(245),rewrite([246(2),246(4)])].

250 x * (A * (1 / x)) = A. [para(246(a,1),66(a,1,2,2)),rewrite([3(8)])].

254 (x \ (1 / x)) * x = 1 / x. [para(247(a,1),96(a,1,1)),flip(a)].

257 x * (1 / A) = x / A. [para(248(a,1),25(a,1,1)),rewrite([90(2)]),flip(a)].

260 A * (1 / x) = A / x. [para(250(a,1),5(a,1,2)),rewrite([114(2)]),flip(a)].

265 (x * y) * (y / A) = y * (y * (x / A)). [para(257(a,1),9(a,1,2)),rewrite([257(9),163(7)])].

270 (A / x) / A = 1 / x. [para(260(a,1),5(a,1,2)),rewrite([90(4)])].

275 A / (1 / x) = A * x. [para(24(a,1),260(a,1,2)),rewrite([246(5)]),flip(a)].

276 A * (x * (1 / y)) = x * (A / y). [para(260(a,1),86(a,2,2))].

277 1 / (A / x) = x / A. [para(24(a,1),270(a,1,1)),rewrite([114(5)]),flip(a)].

280 A / (A * x) = 1 / x. [para(275(a,1),25(a,1,1)),rewrite([114(4)])].

283 1 / (x / A) = A / x. [para(277(a,1),25(a,1,1)),rewrite([246(4)])].

286 A / (x / A) = A * (A / x). [para(277(a,1),275(a,1,2))].

287 (1 / x) / A = 1 / (A * x). [para(275(a,1),277(a,1,2)),flip(a)].

291 1 / (x * (y / A)) = A / (x * y). [para(72(a,1),280(a,1,2)),flip(a)].

292 A / (x * (A * y)) = 1 / (x * y). [para(86(a,1),280(a,1,2))].

294 x * ((y / x) / x) = x \ y. [para(7(a,1),119(a,1,2)),flip(a)].

298 (A / x) * (x / (A / x)) = x. [para(115(a,1),119(a,1,2)),rewrite([114(4),116(4)]),flip(a)].

310 (1 / x) * (x / (1 / x)) = x. [para(247(a,1),119(a,1,2)),rewrite([246(4),249(4)]),flip(a)].

325 A * (x \ (y / A)) = x \ y. [para(4(a,1),132(a,1,2)),rewrite([90(4)]),flip(a)].

326 x \ (y * A) = A * (x \ y). [para(16(a,1),132(a,1,2))].

330 x \ (y * (A * z)) = A * (x \ (y * z)). [para(86(a,1),132(a,1,2))].

331 A * (x \ (1 / y)) = x \ (A / y). [para(260(a,1),132(a,1,2)),flip(a)].

332 (x / A) / y = x / (y * A). [para(4(a,1),148(a,1,1)),rewrite([90(5)]),flip(a)].

333 (A * x) / y = x / (y / A). [para(7(a,1),148(a,1,2))].

336 (x * A) / y = x / (y / A). [para(19(a,2),148(a,1,1)),rewrite([333(7),6(6),333(3)]),flip(a)].

339 x / (A * y) = x / (y * A). [para(94(a,1),148(a,1,2)),rewrite([16(6,R),333(7),96(6),119(4),57(4)]),flip(a)].

346 (x * y) / (x / A) = (A * (x \ y)) * x. [back_rewrite(244),rewrite([333(4)])].

361 (x / (A * y)) * y = x / A. [para(16(a,2),156(a,1,1,2))].

362 A * (x * (y / (A * A))) = x * (y / A). [para(156(a,1),19(a,2,2))].

370 x * ((x \ y) / A) = y / A. [para(4(a,1),163(a,1,1)),flip(a)].

371 x * (x * ((y / x) / A)) = y * (x / A). [para(37(a,1),163(a,1,1)),rewrite([163(3),163(7)]),flip(a)].

372 (x * A) * (x / A) = x * x. [para(64(a,1),163(a,1,1)),rewrite([163(5),6(4)]),flip(a)].

373 (x / A) * (x / A) = x * (x / (A * A)). [para(95(a,1),163(a,1,1)),rewrite([163(5),332(4)]),flip(a)].

384 (A * (A / x)) * x = A * A. [para(16(a,2),164(a,2)),rewrite([286(4)])].

392 (A * x) \ y = (x * A) \ y. [para(203(a,1),5(a,1,2))].

405 x \ (x \ y) = (y / x) / x. [para(230(a,1),6(a,1,1)),flip(a)].

414 x \ (A / x) = (A / x) / x. [para(236(a,1),6(a,1,1)),flip(a)].

420 x \ (1 / x) = (1 / x) / x. [para(254(a,1),6(a,1,1)),flip(a)].

427 A / (x * (y / A)) = A * (A / (x * y)). [para(163(a,1),286(a,1,2))].

446 (A / x) \ x = x / (A / x). [para(298(a,1),5(a,1,2))].

456 x / (x / (1 / x)) = 1 / x. [para(310(a,1),6(a,1,1))].

464 x \ (y / A) = (x \ y) / A. [para(325(a,1),5(a,1,2)),rewrite([90(3)]),flip(a)].

474 (x / (A * A)) / y = x / (A * (y * A)). [para(332(a,1),332(a,1,1)),rewrite([332(10),16(9,R)])].

478 (x * (A * y)) / z = (x * y) / (z / A). [para(86(a,1),333(a,1,1))].

483 x / (A * (y * z)) = x / (y * (z * A)). [para(19(a,1),339(a,1,2)),rewrite([16(7,R)]),flip(a)].

492 x * (x * (y / (A * x))) = (y / A) * x. [para(361(a,1),10(a,1,1)),flip(a)].

520 (x * x) / (A * x) = x / A. [para(372(a,1),120(a,1,1)),rewrite([346(8),114(6),384(8),19(7,R),16(6,R),57(6)])].

538 (A * (A * x)) \ y = (x * (A * A)) \ y. [para(85(a,1),392(a,1,1)),rewrite([16(9,R)]),flip(a)].

558 A * ((1 / x) / x) = (A / x) / x. [para(420(a,1),132(a,2,2)),rewrite([260(4),414(3)]),flip(a)].

568 (x \ (x / (1 / x))) * x = x / (1 / x). [para(456(a,1),120(a,1,2,2)),rewrite([7(10),96(5)])].

575 x \ (1 / (A * y)) = (x \ (1 / y)) / A. [para(287(a,1),464(a,1,2))].

576 x \ (y / (A * A)) = (x \ y) / (A * A). [para(332(a,1),464(a,1,2)),rewrite([464(8),332(10)])].

644 A * ((1 / x) / (A * x)) = (A * x) \ (A / x). [para(446(a,1),331(a,1,2)),rewrite([275(7),275(11)])].

651 A * (x / (A * (A / x))) = x / (A / x). [para(24(a,1),558(a,2,1)),rewrite([114(4),277(5),114(5),332(6),16(5,R),114(9)])].

688 x * (1 / (x * y)) = (y * x) \ x. [para(247(a,1),28(a,1,2,2)),rewrite([3(3)]),flip(a)].

697 ((x \ y) * x) \ x = x * (1 / y). [para(4(a,1),688(a,1,2,2)),flip(a)].

733 x * (1 / (x \ y)) = (y / x) \ x. [para(294(a,1),688(a,1,2,2)),rewrite([7(7)])].

737 (1 / x) * (1 / x) = (1 / x) / x. [para(310(a,1),688(a,1,2,2)),rewrite([7(11),420(8)])].

738 x \ (x / (1 / x)) = x. [para(310(a,1),688(a,2,1)),rewrite([7(10),7(6)]),flip(a)].

762 x / (1 / x) = x * x. [back_rewrite(568),rewrite([738(4)]),flip(a)].

775 (x * x) \ x = 1 / x. [para(762(a,1),25(a,1,1))].

777 x / (A * (A / x)) = x * (x / (A * A)). [para(283(a,1),762(a,1,2)),rewrite([332(5),16(4,R),373(10)])].

791 x / (A / x) = x * (x / A). [back_rewrite(651),rewrite([777(6),362(7)]),flip(a)].

811 (1 / x) * (1 / (A * x)) = (1 / x) / (A * x). [para(275(a,1),791(a,1,2)),rewrite([287(11)]),flip(a)].

818 x / (x * (1 / y)) = (x \ y) * x. [para(697(a,1),24(a,1,2))].

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

831 ((x / y) \ y) / (1 / (y \ x)) = y. [para(733(a,1),6(a,1,1))].

839 (x \ (1 / (x \ y))) * x = ((y / x) \ x) / x. [para(733(a,1),96(a,1,1)),flip(a)].

841 x * (1 / (A * (x \ y))) = (y / (x / A)) \ x. [para(132(a,1),733(a,1,2,2)),rewrite([333(9)])].

842 (x / (y / A)) \ y = ((x / y) \ y) / A. [para(733(a,1),163(a,1,1)),rewrite([287(9),841(10)]),flip(a)].

843 (x / (y * A)) \ y = y * (A / (y \ x)). [para(332(a,1),733(a,2,1)),rewrite([464(4),283(5)]),flip(a)].

863 (A * x) \ (A / x) = (1 / x) / x. [para(737(a,1),72(a,2)),rewrite([287(7),811(8),644(7)])].

875 (x \ (1 / y)) * x = x / (x * y). [para(24(a,1),818(a,1,2,2)),rewrite([246(4)]),flip(a)].

888 ((x / y) \ y) / y = y / x. [back_rewrite(839),rewrite([875(5),4(2)]),flip(a)].

890 (x \ y) / y = y / (x * y). [para(6(a,1),888(a,1,1,1))].

891 (x / y) \ y = (y / x) * y. [para(888(a,1),7(a,1,1)),flip(a)].

898 (x / (y / A)) * x = A * ((x / y) * x). [para(888(a,1),156(a,1,1)),rewrite([336(3),326(10),843(9),96(12),90(10),163(10),270(9),733(8),891(6),16(8,R)])].

901 ((x / y) * x) / (x / A) = x / (y / A). [para(888(a,1),332(a,2)),rewrite([326(6),843(5),96(8),90(6),163(6),270(5),733(4),891(2),16(4,R),333(5),336(8)])].

908 x / ((x / y) * x) = y / x. [para(888(a,1),888(a,1,1,1)),rewrite([25(2),891(3)]),flip(a)].

917 (x / (y / A)) \ y = (y / x) * (y / A). [back_rewrite(842),rewrite([891(6),163(8)])].

924 ((x / y) * x) / (1 / (x \ y)) = x. [back_rewrite(831),rewrite([891(2)])].

925 x * ((x / y) / x) = 1 / (x \ y). [back_rewrite(830),rewrite([891(2),119(3)])].

929 ((x / y) * x) * (y / x) = y / (y / x). [back_rewrite(231),rewrite([891(2)])].

931 (x / (y * x)) * x = y \ x. [para(890(a,1),7(a,1,1))].

942 1 / (x * (y / x)) = x \ (y \ x). [para(890(a,1),294(a,1,2,1)),rewrite([925(4),119(3)])].

948 (x / y) * ((y / x) * y) = y. [para(891(a,1),4(a,1,2))].

954 (x / (y * A)) * (x / A) = (x / y) * (x / (A * A)). [para(332(a,1),891(a,2,1)),rewrite([464(6),917(4),163(6),332(5)]),flip(a)].

955 (x / (A * y)) * x = (x / y) * (x / A). [para(333(a,1),891(a,1,1)),rewrite([917(4)]),flip(a)].

1043 (x / (x * y)) / x = x \ (1 / y). [para(875(a,1),6(a,1,1))].

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

1144 (1 / x) / x = 1 / (x * x). [para(520(a,1),942(a,1,2,2)),rewrite([265(6),22(4),3(3),132(9),775(8),260(9),863(8)]),flip(a)].

1153 ((x / y) * x) \ (1 / (x \ y)) = 1 / (y / (y / x)). [para(908(a,1),942(a,1,2,2)),rewrite([929(5),119(9),925(9)]),flip(a)].

1187 (1 / x) * (1 / x) = 1 / (x * x). [back_rewrite(737),rewrite([1144(8)])].

1274 x \ (A / (x \ y)) = (x / (y / A)) / x. [para(370(a,1),1043(a,1,1,2)),rewrite([283(9)]),flip(a)].

1289 (x / (y / A)) / x = A * ((x / y) / x). [para(1095(a,1),132(a,2,2)),rewrite([260(5),1274(4)])].

1296 ((x / y) * x) \ (y / (y / x)) = y / x. [para(924(a,1),1095(a,2,1)),rewrite([1153(9),249(8),908(8)])].

1299 x \ (A / (x \ y)) = A * ((x / y) / x). [back_rewrite(1274),rewrite([1289(8)])].

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

1460 x * (y * (1 / x)) = (x \ y) * x. [para(111(a,1),3(a,1)),rewrite([246(2)])].

1521 (A * (A * (((A * (A * x)) \ y) * x))) * z = (A * (A * x)) * (y * ((A * (A * x)) \ z)). [para(84(a,2),111(a,1,1)),rewrite([19(9,R)])].

1528 x * ((x \ y) / x) = y * (1 / x). [para(1460(a,1),5(a,1,2)),rewrite([119(3)])].

1530 (x \ (y / (1 / x))) * x = x * y. [para(7(a,1),1460(a,1,2)),flip(a)].

1575 (x * y) * (1 / x) = x * (y / x). [para(5(a,1),1528(a,1,2,1)),flip(a)].

1619 x \ (y / (1 / x)) = (x \ y) * x. [para(1530(a,1),6(a,1,1)),rewrite([96(2)]),flip(a)].

1634 A * (A * ((A * (A * x)) * (y * ((A * (A * x)) \ x)))) = (A * (A * x)) * y. [para(1530(a,1),84(a,2)),rewrite([1619(13),86(11,R),86(10,R),19(14,R),1521(13)])].

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

1737 (x * y) / (1 / y) = x * (y * y). [para(119(a,1),1690(a,1,2,1)),rewrite([30(4)]),flip(a)].

1762 (x * (y * y)) * (1 / y) = x * y. [para(1737(a,1),7(a,1,1))].

1765 (x * (1 / y)) / y = x * (1 / (y * y)). [para(24(a,1),1737(a,1,2)),rewrite([246(2),246(6),246(8),1187(9)])].

1808 (x * y) * (1 / (x * x)) = (x \ (y / x)) * x. [para(1575(a,1),1737(a,1,1)),rewrite([249(6),96(3),1187(9)]),flip(a)].

1813 (x / (y * y)) * y = x * (1 / y). [para(7(a,1),1762(a,1,1)),flip(a)].

1850 x * (1 / (y * y)) = x / (y * y). [para(1813(a,1),6(a,1,1)),rewrite([1765(4)])].

1857 (x / (y * (y / (A * A)))) * y = A * (x * (A / y)). [para(1813(a,1),72(a,1,2)),rewrite([283(5),373(10)]),flip(a)].

1883 (x * y) / (x * x) = (x \ (y / x)) * x. [back_rewrite(1808),rewrite([1850(5)])].

1908 x / (y * (y / (A * A))) = x * (A * (A / (y * y))). [para(291(a,1),1850(a,1,2)),rewrite([95(4),427(5),373(11)]),flip(a)].

1931 (x * (A * (A / (y * y)))) * y = A * (x * (A / y)). [back_rewrite(1857),rewrite([1908(6)])].

1942 (x * y) / (y / A) = (A * (x / y)) * y. [para(124(a,1),96(a,1,1)),rewrite([333(4),1301(9),115(7)])].1958 (A * ((x / y) / x)) * x = x / (y / A). [back_rewrite(901),rewrite([1942(5)])].

1962 (A * (A * ((x / y) / y))) * y = x / (y / (A * A)). [para(138(a,1),96(a,1,1)),rewrite([478(5),333(5),332(4),330(11),132(10),405(9)]),flip(a)].

2190 x / ((x * (A * A)) * (1 / (A * (A * y)))) = A * (A * (((A * (A * x)) \ y) * x)). [para(222(a,1),818(a,1,2)),rewrite([478(12),163(11),287(10),333(12),163(11),287(10),86(22,R),86(21,R)])].

2223 (x * (A * A)) * (1 / y) = A * (x * (A / y)). [para(222(a,1),1813(a,2)),rewrite([478(6),163(5),333(6),163(5),332(4),1908(6),1931(7)]),flip(a)].

2236 A * (A * (((A * (A * x)) \ y) * x)) = (x \ y) * x. [back_rewrite(2190),rewrite([2223(11),292(7),276(7),280(4),818(4)]),flip(a)].

2243 (A * (A * x)) * (y * ((A * (A * x)) \ z)) = x * (y * (x \ z)). [back_rewrite(1521),rewrite([2236(10),111(3)]),flip(a)].

2248 (A * (A * x)) * y = A * (A * (x * y)). [back_rewrite(1634),rewrite([2243(13),21(3),3(4)]),flip(a)].

2290 x / (y / (A * A)) = A * (A * (x / y)). [back_rewrite(1962),rewrite([2248(7),7(5)]),flip(a)].

2329 A * ((A * ((x / A) * y)) * y) = (x * (y * A)) * y. [para(6(a,1),265(a,1,2)),rewrite([82(12)]),flip(a)].

2347 x * (x * ((y / (x / A)) / A)) = (A * y) * (x / A). [para(164(a,1),265(a,1,1)),flip(a)].

2548 A * (A * (x / (A * (y * A)))) = x / y. [para(156(a,1),474(a,2,2,2)),rewrite([2290(9),474(7),57(13)])].

2566 (x / (y * x)) * (x / (A * A)) = (y \ x) / (A * A). [para(474(a,1),931(a,1,1)),rewrite([16(8,R),362(8),72(5),576(12)])].

2607 (x / (y * (A * z))) * x = (x / (y * z)) * (x / A). [para(478(a,1),891(a,1,1)),rewrite([917(5)]),flip(a)].

2694 x * (x * (A * (y / (A * x)))) = A * ((y / A) * x). [para(492(a,1),196(a,1,2)),rewrite([16(10,R)]),flip(a)].

2744 (x / (A * (y * x))) * (x / A) = (y * (A * A)) \ x. [para(538(a,1),931(a,2)),rewrite([2248(5),2607(7)])].

2779 (x / (1 / (A * y))) / x = A * ((x / (1 / y)) / x). [para(575(a,1),1095(a,1,2,2)),rewrite([283(7),1299(6)]),flip(a)].

3018 (x / (A * y)) * (x / A) = (x / y) * (x / (A * A)). [para(19(a,2),955(a,1,1,2)),rewrite([2607(6),954(12)])].

3055 (x * (A * A)) \ y = (x \ y) / (A * A). [back_rewrite(2744),rewrite([3018(7),2566(7)]),flip(a)].

3080 (A * (A * x)) \ y = (x \ y) / (A * A). [back_rewrite(538),rewrite([3055(10)])].

3116 A * ((x / (A * y)) / x) = (x / y) / x. [para(96(a,1),1289(a,1,1,2)),rewrite([90(2),16(4,R),57(4)]),flip(a)].

3144 A * ((x / (y * (z * A))) / x) = (x / (y * z)) / x. [para(483(a,1),1289(a,2,2,1)),rewrite([96(5),90(3),163(3),16(5,R),72(5)]),flip(a)].

3154 (((x / y) * x) \ (y / (y / (A * x)))) / (A * A) = y / (A * x). [para(86(a,2),1296(a,1,1)),rewrite([333(4),898(5),3080(11)])].

3189 (x / y) / (A * A) = x / (A * (y * A)). [para(474(a,1),1296(a,1,2,2)),rewrite([2290(5),2248(6),474(16),16(14,R),2548(15),3080(9),1296(5),474(10)])].

3466 (A * ((A * (x / y)) * y)) * (y / A) = A * (A * ((x / A) * y)). [para(265(a,1),1942(a,1,1)),rewrite([332(8),2290(9),96(7),5(6),1942(12)]),flip(a)].

3492 (A * ((x / y) / x)) * (x / A) = (x / (y / A)) / A. [para(1958(a,1),163(a,1,1)),flip(a)].

3503 (x / (y / A)) / A = A * (x / (A * y)). [para(1958(a,1),362(a,1,2)),rewrite([474(8),16(6,R),57(6),474(11),2290(16),3144(15),3116(12),3492(12)]),flip(a)].

3529 (A * x) * (y / A) = A * ((x / A) * y). [back_rewrite(2347),rewrite([3503(5),2694(7)]),flip(a)].

3542 A * (A * ((x / A) * y)) = (A * x) * y. [back_rewrite(3466),rewrite([3529(9),163(7),3529(7),2329(9),19(4,R),7(3)]),flip(a)].

3784 A * (x / (A * (y * A))) = (x / y) / A. [para(3189(a,1),156(a,1,1)),rewrite([16(7,R)])].

4118 (x / (x / y)) * x = x / (1 / y). [para(948(a,1),31(a,1,2,1)),rewrite([42(3),1690(3),929(7)]),flip(a)].

4185 (x / (1 / y)) / x = x / (x / y). [para(4118(a,1),6(a,1,1))].

4232 x / (x / (A * y)) = A * (x / (x / y)). [back_rewrite(2779),rewrite([4185(6),4185(9)])].

4241 (x / y) / A = x / (A * y). [back_rewrite(3154),rewrite([4232(6),132(7),1296(6),1883(7),464(5),90(3),332(5),3189(5),16(7,R),3784(7)])].

4346 (x / A) * y = x * (y / A). [back_rewrite(371),rewrite([4241(3),492(5)])].

4540 (A * x) * y = A * (x * y). [back_rewrite(3542),rewrite([4346(5),72(6)]),flip(a)].

4541 $F. [resolve(4540,a,89,a)].

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

============================== STATISTICS ============================

Given=178. Generated=20394. Kept=4534. proofs=1.

Usable=133. Sos=2285. Demods=2309. Limbo=194, Disabled=1933. Hints=590.

Kept_by_rule=0, Deleted_by_rule=0.

Forward_subsumed=15860. Back_subsumed=143.

Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0.

New_demodulators=4021 (11 lex), Back_demodulated=1778. Back_unit_deleted=0.

Demod_attempts=475291. Demod_rewrites=73464.

Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0.

Nonunit_fsub_feature_tests=0. Nonunit_bsub_feature_tests=0.

Megabytes=5.06.

User_CPU=1.07, System_CPU=0.03, Wall_clock=1.

============================== end of statistics =====================

============================== end of search =========================

THEOREM PROVED

Exiting with 1 proof.

Process 79332 exit (max_proofs) Thu Oct 1 12:52:59 2009