% ============================== PROOF =================================
% 
% % -------- Comments from original proof --------
% % Proof 1 at 123.04 (+ 0.51) seconds.
% % Length of proof is 762.
% % Level of proof is 59.
% % Maximum clause weight is 1019.
% % Given clauses 978.
% 
% 1 1 * x = x # label(1).  [assumption].
% 2 x * 1 = x # label(2).  [assumption].
% 3 x * (x \ y) = y # label(1777) # label(2).  [assumption].
% 4 x \ (x * y) = y # label(2589) # label(4).  [assumption].
% 5 (x * y) / y = x # label(359) # label(4).  [assumption].
% 6 (x / y) * y = x # label(6).  [assumption].
% 7 ((x * y) / x) * (x * z) = x * (y * z) # label(LCC) # label(2542) # label(6).  [assumption].
% 8 (x * y) * (y \ (z * y)) = (x * z) * y # label(RCC) # label(8).  [assumption].
% 9 A * (B * ((D * C) \ (C * D))) != (A * B) * ((D * C) \ (C * D)) # label("orig").  [assumption].
% 10 (A * B) * ((D * C) \ (C * D)) != A * (B * ((D * C) \ (C * D))) # label("orig") # label(10).  [copy(9),flip(a)].
% 11 1 \ x = x # label(13).  [para(3(a,1),1(a,1)),flip(a)].
% 12 x \ x = 1 # label(13).  [para(2(a,1),4(a,1,2))].
% 13 x / x = 1 # label(14).  [para(1(a,1),5(a,1,1))].
% 14 x / 1 = x # label(19).  [para(2(a,1),5(a,1,1))].
% 15 x / (y \ x) = y # label(813) # label(20).  [para(3(a,1),5(a,1,1))].
% 16 (x / y) \ x = y # label(2028) # label(25).  [para(6(a,1),4(a,1,2))].
% 17 (x / y) * (y * z) = y * ((y \ x) * z) # label(17).  [para(3(a,1),7(a,1,1,1))].
% 18 ((x * y) / x) * z = x * (y * (x \ z)) # label(561) # label(19).  [para(3(a,1),7(a,1,2))].
% 20 (x * (y * z)) / (x * z) = (x * y) / x # label(19).  [para(7(a,1),5(a,1,1))].
% 25 (x * (y \ z)) * ((y \ z) \ z) = (x * y) * (y \ z) # label(21).  [para(3(a,1),8(a,1,2,2))].
% 26 (x * y) \ ((x * z) * y) = y \ (z * y) # label(22).  [para(8(a,1),4(a,1,2))].
% 27 ((x * y) * z) / (z \ (y * z)) = x * z # label(23).  [para(8(a,1),5(a,1,1))].
% 28 ((x / y) * z) * y = x * (y \ (z * y)) # label(24).  [para(6(a,1),8(a,1,1)),flip(a)].
% 29 (x * (y / z)) * z = (x * z) * (z \ y) # label(25).  [para(6(a,1),8(a,1,2,2)),flip(a)].
% 32 x * ((x \ y) * (x \ z)) = (y / x) * z # label(28).  [para(3(a,1),17(a,1,2)),flip(a)].
% 33 (x / y) \ (y * ((y \ x) * z)) = y * z # label(30).  [para(17(a,1),4(a,1,2))].
% 34 x * ((x \ (y * x)) * z) = y * (x * z) # label(31).  [para(5(a,1),17(a,1,1)),flip(a)].
% 39 (x \ y) * (((x \ y) \ y) * z) = x * ((x \ y) * z) # label(37).  [para(15(a,1),17(a,1,1)),flip(a)].
% 41 x * (y * (x \ 1)) = (x * y) / x # label(39).  [para(18(a,1),2(a,1))].
% 43 (x * (y * (x \ z))) / z = (x * y) / x # label(40).  [para(18(a,1),5(a,1,1))].
% 44 x * ((x \ y) * ((y / x) \ z)) = (y / (y / x)) * z # label(52).  [para(6(a,1),18(a,1,1,1)),rewrite(17(8)),flip(a)].
% 51 x \ ((x * y) / x) = y * (x \ 1) # label(2355) # label(42).  [para(41(a,1),4(a,1,2))].
% 53 (x * (y / (x \ 1))) / x = x * y # label(46).  [para(6(a,1),41(a,1,2)),flip(a)].
% 56 ((1 / x) * y) / (1 / x) = (1 / x) * (y * x) # label(66).  [para(16(a,1),41(a,1,2,2)),flip(a)].
% 61 (x \ y) * (x \ 1) = x \ (y / x) # label(53).  [para(3(a,1),51(a,1,2,1)),flip(a)].
% 66 x \ (((x * y) / x) / x) = (y * (x \ 1)) * (x \ 1) # label(55).  [para(41(a,1),51(a,1,2,1))].
% 74 x * (y / (x \ 1)) = (x * y) * x # label(56).  [para(53(a,1),6(a,1,1)),flip(a)].
% 77 (x \ y) \ (x \ (y / x)) = x \ 1 # label(58).  [para(61(a,1),4(a,1,2))].
% 78 (x \ (y / x)) / (x \ 1) = x \ y # label(59).  [para(61(a,1),5(a,1,1))].
% 86 x \ ((x * y) * x) = y / (x \ 1) # label(62).  [para(74(a,1),4(a,1,2))].
% 97 (x \ y) / (x \ 1) = x \ (y * x) # label(71).  [para(5(a,1),78(a,1,1,2))].
% 101 (x * y) * (z / (y \ 1)) = (x * (y * z)) * y # label(80).  [para(86(a,1),8(a,1,2))].
% 103 (x \ (y * x)) \ (((x \ (y * x)) * y) * x) = x / ((x \ (y * x)) \ 1) # label(77).  [para(8(a,1),86(a,1,2))].
% 113 (x * y) / (x * (z \ y)) = (x * z) / x # label(63).  [para(3(a,1),20(a,1,1,2))].
% 114 (x * (y / z)) / x = (x * y) / (x * z) # label(132).  [para(6(a,1),20(a,1,1,2)),flip(a)].
% 134 (x \ y) \ (z * (x \ y)) = y \ ((x * z) * (x \ y)) # label(75).  [para(3(a,1),26(a,1,1)),flip(a)].
% 135 (x * y) \ (z * y) = y \ ((x \ z) * y) # label(81).  [para(3(a,1),26(a,1,2,1))].
% 153 (x * y) / (y \ (z * y)) = (x / z) * y # label(82) # label(129) # label(168).  [para(6(a,1),27(a,1,1,1))].
% 170 ((x / y) * z) \ (x * (y \ (z * y))) = y # label(105).  [para(28(a,1),4(a,1,2))].
% 171 (x * (y \ (z * y))) / y = (x / y) * z # label(83).  [para(28(a,1),5(a,1,1))].
% 176 (x * ((x \ y) * z)) * x = y * (z / (x \ 1)) # label(85).  [para(17(a,1),28(a,1,1)),rewrite(86(7))].
% 178 (x * (y * (x \ z))) * x = (x * y) * (x \ (z * x)) # label(311).  [para(18(a,1),28(a,1,1))].
% 188 ((x \ (y * x)) * z) * (x \ 1) = (x \ y) * ((x * z) * (x \ 1)) # label(88).  [para(97(a,1),28(a,1,1,1)),rewrite(134(13),11(13))].
% 195 ((x / (y / z)) * z) * (z \ y) = x * z # label(89).  [para(6(a,1),29(a,1,1)),flip(a)].
% 205 ((x * y) * x) * (x \ 1) = (x \ 1) \ y # label(99).  [para(74(a,1),29(a,1,1)),rewrite(3(8),1(10))].
% 207 x \ ((x * x) * (x \ y)) = (y / x) / (x \ 1) # label(118).  [para(29(a,1),86(a,1,2))].
% 215 x \ ((y / x) * z) = (x \ y) * (x \ z) # label(91).  [para(32(a,1),4(a,1,2))].
% 227 (x / y) \ (y * z) = y * ((y \ x) \ z) # label(92).  [para(3(a,1),33(a,1,2,2))].
% 231 x \ (y * (x * z)) = (x \ (y * x)) * z # label(93).  [para(34(a,1),4(a,1,2))].
% 241 (x \ y) * ((x * z) * (x \ 1)) = x \ ((y * (x * z)) / x) # label(95).  [para(34(a,1),51(a,1,2,1)),rewrite(188(10)),flip(a)].
% 255 ((x \ (y * x)) * z) * (x \ 1) = x \ ((y * (x * z)) / x).  [back_rewrite(188),rewrite(241(12))].
% 263 x / (x * (y \ 1)) = (x * y) / x # label(97).  [para(2(a,1),113(a,1,1))].
% 264 x / (y * (z \ (y \ x))) = (y * z) / y # label(98).  [para(3(a,1),113(a,1,1))].
% 265 ((x / y) * z) / (x / y) = x / ((x / y) * (z \ y)) # label(130).  [para(6(a,1),113(a,1,1)),flip(a)].
% 287 1 / ((1 / x) * (y \ x)) = (1 / x) * (y * x) # label(136).  [back_rewrite(56),rewrite(265(6))].
% 288 ((x * y) / x) \ x = x * (y \ 1) # label(107).  [para(263(a,1),16(a,1,1))].
% 296 x * ((x \ y) \ 1) = (y / x) \ x # label(108).  [para(3(a,1),288(a,1,1,1)),flip(a)].
% 315 x \ ((y / x) \ x) = (x \ y) \ 1 # label(110).  [para(296(a,1),4(a,1,2))].
% 336 (x \ (y * x)) \ 1 = x \ (y \ x) # label(115).  [para(5(a,1),315(a,1,2,1)),flip(a)].
% 337 (x \ y) \ (x \ (x \ y)) = ((x \ y) \ y) \ 1 # label(340).  [para(15(a,1),315(a,1,2,1))].
% 340 (x / (y \ 1)) \ 1 = y \ ((y * x) \ y) # label(118).  [para(86(a,1),315(a,2,1)),rewrite(5(3)),flip(a)].
% 349 (x \ (y * x)) \ (((x \ (y * x)) * y) * x) = x / (x \ (y \ x)).  [back_rewrite(103),rewrite(336(11))].
% 363 1 / (x \ (y \ x)) = x \ (y * x) # label(120).  [para(336(a,1),15(a,1,2))].
% 364 ((x \ (y * x)) * z) / (x \ (y * x)) = (x \ (y * x)) * (z * (x \ (y \ x))).  [para(336(a,1),18(a,2,2,2)),rewrite(2(8))].
% 372 (x * y) \ ((y * z) * (y \ (x * y))) = ((y \ (x * y)) \ z) / (y \ (x \ y)) # label(346).  [para(336(a,1),97(a,1,2)),rewrite(134(12)),flip(a)].
% 379 (x * (y \ (z * y))) / x = x / (x * (y \ (z \ y))) # label(143).  [para(336(a,1),113(a,1,2,2)),rewrite(2(2)),flip(a)].
% 388 x \ ((x / y) * x) = 1 / (x \ y) # label(121).  [para(16(a,1),363(a,1,2,2)),flip(a)].
% 400 x * (1 / (x \ y)) = (x / y) * x # label(123).  [para(388(a,1),3(a,1,2))].
% 401 (x * y) * (1 / (y \ z)) = (x * (y / z)) * y # label(367).  [para(388(a,1),8(a,1,2))].
% 404 (x * y) \ (x * (y * y)) = 1 / ((x * y) \ x) # label(369).  [para(17(a,1),388(a,1,2)),rewrite(4(3))].
% 405 (1 / (x \ y)) * (x \ 1) = x \ (x / y) # label(4463) # label(268).  [para(388(a,1),61(a,1,1)),rewrite(5(9))].
% 406 (1 / (x \ y)) \ (x \ (x / y)) = x \ 1 # label(127).  [para(388(a,1),77(a,1,1)),rewrite(5(6))].
% 419 ((x / y) / x) * (x / y) = (x / y) * (1 / y) # label(128).  [para(16(a,1),400(a,1,2,2)),flip(a)].
% 439 ((x * y) / (x * z)) * u = x * ((y / z) * (x \ u)) # label(248) # label(157).  [para(114(a,1),18(a,1,1))].
% 453 x \ ((y \ 1) * x) = (y * x) \ x # label(173).  [para(1(a,1),135(a,1,2)),flip(a)].
% 454 x \ ((y * (z \ y)) * (y \ x)) = (z * (y \ x)) \ x # label(104).  [para(3(a,1),135(a,1,2)),rewrite(134(8)),flip(a)].
% 455 x \ (((y / x) \ z) * x) = y \ (z * x) # label(175).  [para(6(a,1),135(a,1,1)),flip(a)].
% 456 x \ ((y \ (z / x)) * x) = (y * x) \ z # label(177).  [para(6(a,1),135(a,1,2)),flip(a)].
% 468 (x \ 1) \ (x \ (y / x)) = y * (x \ 1) # label(79).  [para(61(a,1),135(a,2,2)),rewrite(3(3),11(5)),flip(a)].
% 474 (x * y) \ (z * (y \ (u * y))) = y \ ((x \ ((z / y) * u)) * y) # label(182).  [para(28(a,1),135(a,1,2))].
% 501 x \ ((y \ (x * (z * (x \ y)))) * x) = ((x \ (y * x)) \ z) / (x \ (y \ x)) # label(348).  [back_rewrite(372),rewrite(474(6),18(3))].
% 505 x * ((y * x) \ x) = (y \ 1) * x # label(188).  [para(453(a,1),3(a,1,2))].
% 507 (x * y) * ((z * y) \ y) = (x * (z \ 1)) * y # label(168).  [para(453(a,1),8(a,1,2))].
% 509 ((1 / x) * y) \ y = y \ (x * y) # label(189).  [para(16(a,1),453(a,1,2,1)),flip(a)].
% 523 ((x * y) \ y) \ 1 = y \ ((x \ 1) \ y) # label(353).  [para(453(a,1),315(a,2,1)),rewrite(5(4)),flip(a)].
% 527 (x \ y) * (y \ (x \ y)) = (x \ 1) * (x \ y) # label(200).  [para(3(a,1),505(a,1,2,1))].
% 528 ((x / y) \ 1) * y = y * (x \ y) # label(201).  [para(6(a,1),505(a,1,2,1)),flip(a)].
% 539 (((x * y) \ y) \ y) / (y \ ((x \ 1) \ y)) = ((x * y) \ y) \ ((x \ 1) * y).  [para(505(a,1),97(a,2,2)),rewrite(523(7))].
% 559 x / (x \ (y * x)) = (1 / y) * x # label(203).  [para(509(a,1),15(a,1,2))].
% 566 (((1 / x) * y) * (z * (y \ (x * y)))) / y = (((1 / x) * y) * z) / ((1 / x) * y) # label(185).  [para(509(a,1),43(a,1,1,2,2))].
% 575 (x * (y \ x)) / x = (y / x) \ 1 # label(204).  [para(528(a,1),5(a,1,1))].
% 579 x * ((x \ y) * (y \ x)) = (1 / (y / x)) * y # label(189).  [para(528(a,1),17(a,2,2)),rewrite(6(5),17(8)),flip(a)].
% 615 (1 / (x / y)) * y = y / (y \ x) # label(206).  [para(6(a,1),559(a,1,2,2)),flip(a)].
% 623 (x \ 1) / (y * (x \ 1)) = x \ (x / y) # label(211).  [para(61(a,1),559(a,1,2,2)),rewrite(468(7),405(12))].
% 627 x / (y / (x \ 1)) = (1 / (x * y)) * x # label(201).  [para(86(a,1),559(a,1,2))].
% 637 x / (1 / (x \ y)) = (1 / (x / y)) * x # label(375).  [para(388(a,1),559(a,1,2))].
% 642 ((x * y) * y) / (x * y) = (x / (x * y)) \ 1 # label(203).  [para(4(a,1),575(a,1,1,2))].
% 644 ((x / y) / x) \ 1 = (x * y) / x # label(212).  [para(16(a,1),575(a,1,1,2)),flip(a)].
% 645 x * ((y \ x) * (x \ z)) = ((y / x) \ 1) * z # label(208).  [para(575(a,1),18(a,1,1)),flip(a)].
% 647 x \ ((y / x) \ 1) = (y \ x) * (x \ 1) # label(127).  [para(575(a,1),51(a,1,2))].
% 651 ((x / y) \ 1) \ y = y * ((x \ y) \ 1) # label(214).  [para(575(a,1),288(a,1,1))].
% 658 (1 / (x / y)) \ (y / (y \ x)) = y # label(220).  [para(615(a,1),4(a,1,2))].
% 659 (x / (x \ y)) / x = 1 / (y / x) # label(215).  [para(615(a,1),5(a,1,1))].
% 687 (x \ (x / (x \ y))) \ 1 = x \ ((1 / (y / x)) \ x) # label(360).  [para(615(a,1),336(a,1,1,2))].
% 698 1 / ((x * y) / x) = (x / y) / x # label(942) # label(121).  [para(644(a,1),15(a,1,2))].
% 738 ((x / y) / y) / (x / y) = 1 / (x / (x / y)) # label(221).  [para(16(a,1),659(a,1,1,2))].
% 746 1 / ((x * y) / (x * z)) = (x / (y / z)) / x # label(943) # label(123).  [para(114(a,1),659(a,2,2)),rewrite(4(3)),flip(a)].
% 774 x / (y \ (z * y)) = ((x / y) / z) * y # label(228).  [para(6(a,1),153(a,1,1))].
% 775 (x * y) / (y \ z) = (x / (z / y)) * y # label(229).  [para(6(a,1),153(a,1,2,2))].
% 780 ((x \ (y * x)) / y) * x = (x \ (y * x)) * (y \ x) # label(241).  [para(153(a,1),41(a,2)),rewrite(336(6),3(5)),flip(a)].
% 781 ((x \ (y * x)) \ (z * x)) * (x \ (y \ x)) = (x \ (y * x)) \ ((z / y) * x) # label(234).  [para(153(a,1),61(a,2,2)),rewrite(336(8))].
% 783 (x * (y \ 1)) / (z * (y \ 1)) = (x / (y \ z)) * (y \ 1) # label(232).  [para(61(a,1),153(a,1,2,2)),rewrite(468(8))].
% 785 (x * y) / (z / (y \ 1)) = (x / (y * z)) * y # label(244).  [para(86(a,1),153(a,1,2))].
% 789 (x \ (y * x)) / (x \ y) = (x \ (y * x)) * (y \ x).  [para(153(a,1),263(a,2)),rewrite(61(7),5(4),780(8))].
% 795 (x * y) / (1 / (y \ z)) = (x / (y / z)) * y # label(379).  [para(388(a,1),153(a,1,2))].
% 805 (x / ((y / z) \ 1)) * z = (x * z) / (y \ z) # label(234).  [para(528(a,1),153(a,1,2,2)),rewrite(4(4)),flip(a)].
% 816 ((((x \ (y * x)) * z) / x) / y) * x = (x \ (y * x)) * (z * (x \ (y \ x))).  [back_rewrite(364),rewrite(774(6))].
% 824 ((1 / x) * y) \ (x \ (y * x)) = x # label(170).  [para(1(a,1),170(a,1,2))].
% 862 (x \ (y * x)) / x = (1 / x) * y # label(168).  [para(824(a,1),15(a,1,2))].
% 863 (x * ((x \ 1) * y)) \ (y / (x \ 1)) = x # label(172).  [para(17(a,1),824(a,1,1)),rewrite(86(7))].
% 884 ((x \ (y * x)) \ ((1 / x) * y)) / (x \ (y \ x)) = 1 / ((x \ (y * x)) \ x) # label(251).  [para(824(a,1),363(a,1,2,2)),rewrite(134(14),474(14),18(11),501(14)),flip(a)].
% 890 ((1 / x) * (y \ 1)) \ ((y * x) \ x) = x # label(266).  [para(453(a,1),824(a,1,2))].
% 902 (1 / x) * (y / x) = (x \ y) / x # label(163).  [para(6(a,1),862(a,1,1,2)),flip(a)].
% 906 (x / (y \ 1)) / y = y * ((y \ 1) * x) # label(258).  [para(17(a,1),862(a,2)),rewrite(86(3))].
% 921 (1 / (x \ y)) / x = (1 / x) * (x / y) # label(165).  [para(388(a,1),862(a,1,1))].
% 923 ((x * y) \ y) / y = (1 / y) * (x \ 1) # label(196).  [para(453(a,1),862(a,1,1))].
% 927 (1 / x) * ((y / x) \ 1) = (y \ x) / x # label(262).  [para(528(a,1),862(a,1,1,2)),rewrite(4(3)),flip(a)].
% 939 ((x \ y) / x) / (y / x) = 1 / x # label(167).  [para(902(a,1),5(a,1,1))].
% 944 (1 / x) * ((y / x) * ((1 / x) \ z)) = (((x \ y) / x) / (1 / x)) * z # label(265).  [para(902(a,1),18(a,1,1,1)),flip(a)].
% 945 ((x \ y) / x) / (1 / x) = (1 / x) * y # label(1016).  [para(902(a,1),41(a,2,1)),rewrite(16(7),6(4)),flip(a)].
% 953 (1 / x) / ((y \ x) / x) = (1 / x) * y # label(2397).  [para(902(a,1),263(a,2,1)),rewrite(927(8),945(10))].
% 963 ((x \ y) / x) \ (y / x) = x * ((x \ y) \ (y / x)) # label(276).  [para(902(a,1),453(a,2,1)),rewrite(16(5),227(4)),flip(a)].
% 971 (1 / x) * ((y / x) * ((1 / x) \ z)) = ((1 / x) * y) * z.  [back_rewrite(944),rewrite(945(13))].
% 973 (x / y) / ((y * x) / y) = 1 / y # label(162).  [para(4(a,1),939(a,1,1,1))].
% 985 (((x * y) \ y) / y) / (x \ 1) = 1 / y # label(199).  [para(453(a,1),939(a,1,1,1)),rewrite(5(7))].
% 1000 (1 / x) \ (y / x) = (x * y) / x # label(158).  [para(973(a,1),16(a,1,1))].
% 1032 (x * (y * x)) / x = (1 / x) \ y # label(157).  [para(5(a,1),1000(a,1,2)),flip(a)].
% 1033 ((x \ 1) * y) / (x \ 1) = x \ (y / (x \ 1)) # label(435).  [para(15(a,1),1000(a,1,1)),flip(a)].
% 1036 ((x / y) / x) \ (z / ((x * y) / x)) = (x * (y * (x \ z))) / ((x * y) / x) # label(595).  [para(18(a,1),1000(a,2,1)),rewrite(698(4))].
% 1065 ((1 / x) \ y) * x = x * (y * x) # label(155).  [para(1032(a,1),6(a,1,1))].
% 1070 x * ((y * x) * (x \ z)) = ((1 / x) \ y) * z # label(301).  [para(1032(a,1),18(a,1,1)),flip(a)].
% 1072 x \ ((1 / x) \ y) = (y * x) * (x \ 1) # label(160).  [para(1032(a,1),51(a,1,2))].
% 1076 (x * (y * (x \ (z * x)))) / x = (1 / x) \ ((y / x) * z) # label(304).  [para(28(a,1),1032(a,1,1,2))].
% 1078 (1 / x) \ (y * (z / x)) = (((1 / x) \ y) * z) / x # label(306).  [para(29(a,1),1032(a,1,1,2)),rewrite(1070(4)),flip(a)].
% 1082 ((1 / x) \ y) \ x = x * ((y * x) \ 1) # label(613).  [para(1032(a,1),288(a,1,1))].
% 1092 (x / (y * x)) / x = 1 / ((1 / x) \ y) # label(616).  [para(1032(a,1),659(a,2,2)),rewrite(4(3))].
% 1106 (x \ 1) * (y * (x \ 1)) = x \ (y / x) # label(140).  [para(15(a,1),1065(a,1,1,1)),rewrite(61(4)),flip(a)].
% 1128 ((x \ (y * x)) \ z) * (x \ (y \ x)) = (x \ (y \ x)) * (z * (x \ (y \ x))) # label(127).  [para(363(a,1),1065(a,1,1,1))].
% 1143 (x \ (y \ x)) * ((z * x) * (x \ (y \ x))) = (x \ (y * x)) \ ((z / y) * x) # label(315).  [back_rewrite(781),rewrite(1128(7))].
% 1147 (x * (y \ z)) / y = (x / y) * (z / y) # label(247).  [para(6(a,1),171(a,1,1,2,2))].
% 1149 (x * (y / (z \ 1))) / z = z * ((z \ x) * y) # label(135).  [para(17(a,1),171(a,2)),rewrite(86(3))].
% 1152 (x * (y * (z \ 1))) / (z \ 1) = (x / (z \ 1)) * (z \ y) # label(239).  [para(61(a,1),171(a,1,1,2,2)),rewrite(468(5))].
% 1161 (x / y) * ((z / y) \ 1) = (x * (z \ y)) / y # label(1045).  [para(528(a,1),171(a,1,1,2,2)),rewrite(4(3)),flip(a)].
% 1164 (x / y) * ((1 / y) \ z) = (x * (z * y)) / y # label(325).  [para(1065(a,1),171(a,1,1,2,2)),rewrite(4(3)),flip(a)].
% 1170 (x \ (y * (z * x))) / x = ((1 / x) * y) * z # label(328).  [back_rewrite(971),rewrite(1164(7),902(6))].
% 1220 ((x / (y / (y / z))) * z) * (z \ y) = x * (y / z) # label(243).  [para(16(a,1),195(a,1,2)),rewrite(29(6))].
% 1233 (1 / x) \ (y / (z / x)) = (x * (y * x)) / z # label(245).  [para(195(a,1),43(a,1,1,2)),rewrite(1032(8)),flip(a)].
% 1265 (x \ 1) \ (x \ y) = (y * x) * (x \ 1) # label(141).  [para(3(a,1),205(a,1,1,1)),flip(a)].
% 1346 (x \ y) * (x \ ((y / x) \ z)) = x \ z # label(142).  [para(3(a,1),215(a,1,2)),flip(a)].
% 1347 (x \ (y * x)) * (x \ z) = x \ (y * z) # label(241).  [para(5(a,1),215(a,1,2,1)),flip(a)].
% 1353 (x / (y \ 1)) * (y \ z) = y \ ((y * x) * z) # label(248).  [para(86(a,1),215(a,2,1)),rewrite(5(3)),flip(a)].
% 1367 (1 / (x \ y)) * (x \ z) = x \ ((x / y) * z) # label(254).  [para(388(a,1),215(a,2,1)),rewrite(5(3)),flip(a)].
% 1389 (x * (y * (z \ 1))) / (z \ 1) = z \ ((z * x) * y) # label(256).  [back_rewrite(1152),rewrite(1353(12))].
% 1400 x * ((x \ (y * x)) \ z) = y \ (x * z) # label(136).  [para(5(a,1),227(a,1,1)),flip(a)].
% 1408 x * ((x \ y) \ (z * (x \ 1))) = (y / x) \ ((x * z) / x) # label(138).  [para(41(a,1),227(a,1,2)),flip(a)].
% 1414 x * ((y / (x \ 1)) \ z) = (x * y) \ (x * z) # label(258).  [para(86(a,1),227(a,2,2,1)),rewrite(5(3)),flip(a)].
% 1436 x * ((1 / (x \ y)) \ z) = (x / y) \ (x * z) # label(385).  [para(388(a,1),227(a,2,2,1)),rewrite(5(3)),flip(a)].
% 1476 (x \ (y * x)) * (y \ 1) = x \ ((y * x) / y) # label(149).  [para(41(a,1),231(a,1,2)),flip(a)].
% 1485 (x \ y) \ ((y / x) * z) = ((x \ y) \ y) * (x \ z) # label(3223).  [para(32(a,1),231(a,1,2)),rewrite(3(7))].
% 1514 ((x * y) / x) \ z = x * (y \ (x \ z)) # label(2111).  [para(264(a,1),16(a,1,1))].
% 1516 x / (y * (z * (y \ (u \ (y * (z \ (y \ x))))))) = (y * (z * (y \ u))) / ((y * z) / y).  [para(18(a,1),264(a,1,2)),rewrite(1514(3),18(11))].
% 1533 (x * (y * (z \ (y \ x)))) / x = (((y * z) / y) / x) \ 1 # label(270).  [para(264(a,1),644(a,1,1,1)),flip(a)].
% 1727 ((x / y) \ z) * y = y * (x \ (z * y)) # label(314).  [para(455(a,1),3(a,1,2)),flip(a)].
% 1731 (x \ y) \ (z * (x \ 1)) = (y \ (x * z)) * (x \ 1) # label(157).  [para(97(a,1),455(a,1,2,1,1)),rewrite(134(9),1400(5),11(7)),flip(a)].
% 1733 ((x / y) \ z) * (y * u) = y * ((x \ (z * y)) * u) # label(2435).  [para(455(a,1),34(a,1,2,1)),flip(a)].
% 1740 (1 / x) * ((y / x) \ z) = (y \ (z * x)) / x # label(1050).  [para(455(a,1),862(a,1,1)),flip(a)].
% 1743 ((x \ y) \ z) / (x \ 1) = y \ ((x * z) * x) # label(280).  [para(227(a,1),455(a,1,2,1)),rewrite(86(5))].
% 1747 (x \ (x / y)) * (x \ y) = y \ (x \ y) # label(324).  [para(406(a,1),455(a,1,2,1)),rewrite(453(6),3(2),11(8)),flip(a)].
% 1755 (x / y) \ ((y * z) / y) = (y * (x \ (y * z))) / y # label(171).  [back_rewrite(1408),rewrite(1731(5),41(6)),flip(a)].
% 1768 (x \ (y / z)) * z = z * ((x * z) \ y) # label(328).  [para(456(a,1),3(a,1,2)),flip(a)].
% 1769 (x * (y \ (z / u))) * u = (x * u) * ((y * u) \ z) # label(204).  [para(456(a,1),8(a,1,2)),flip(a)].
% 1771 (((x / y) / z) * y) \ x = y \ (z * y) # label(253).  [para(16(a,1),456(a,1,2,1)),flip(a)].
% 1815 (((x * y) \ y) \ z) / (y \ ((x \ 1) \ y)) = y \ (((x * y) * z) * ((x * y) \ y)).  [para(523(a,1),97(a,1,2)),rewrite(134(14))].
% 1847 ((x * y) \ y) \ ((x \ 1) * y) = y \ (((x * y) * (x \ 1)) * y).  [back_rewrite(539),rewrite(1815(8),507(5)),flip(a)].
% 1882 (x \ (y * x)) \ ((1 / x) * y) = (x \ (y \ x)) / (y \ x) # label(442).  [para(862(a,1),623(a,2,2)),rewrite(336(4),336(6),3(5)),flip(a)].
% 1897 ((x \ (y \ x)) / (y \ x)) / (x \ (y \ x)) = 1 / ((x \ (y * x)) \ x) # label(444).  [back_rewrite(884),rewrite(1882(6))].
% 1922 (1 / (x / (y \ 1))) \ ((1 / (y * x)) * y) = ((x / (y \ 1)) / (y * x)) * y.  [para(627(a,1),1000(a,1,2)),rewrite(785(18))].
% 1931 (1 / ((x / y) / x)) * (x / y) = (x / y) / (1 / y).  [para(16(a,1),637(a,1,2,2)),flip(a)].
% 1950 (1 / (1 / (x / y))) * (y / (y \ x)) = (y / (y \ x)) / (1 / (y \ x)).  [para(659(a,1),637(a,2,1,2)),rewrite(16(6)),flip(a)].
% 2020 (x \ y) * ((y \ (x \ y)) \ 1) = (y * x) * (x \ 1).  [para(15(a,1),651(a,1,1,1)),rewrite(1265(4)),flip(a)].
% 2036 ((x / y) \ y) * (((y \ x) \ 1) \ 1) = (y * (x / y)) * ((x / y) \ 1) # label(449).  [para(315(a,1),651(a,2,2,1)),rewrite(15(3),1265(6)),flip(a)].
% 2065 ((x / y) / (z / y)) * y = x / (y \ z) # label(349).  [para(6(a,1),774(a,1,2,2)),flip(a)].
% 2070 ((x \ (y * x)) * (z * (x \ (y \ x)))) * u = (x \ (y * x)) * (z * ((x \ (y * x)) \ u)).  [para(774(a,1),18(a,1,1)),rewrite(816(6))].
% 2073 ((x / (y \ 1)) / (y \ z)) * (y \ 1) = x / (z * (y \ 1)) # label(455).  [para(61(a,1),774(a,1,2,2)),rewrite(1265(5),6(2)),flip(a)].
% 2076 ((x / y) / (y * z)) * y = x / (z / (y \ 1)) # label(457).  [para(86(a,1),774(a,1,2)),flip(a)].
% 2089 ((x / y) / (y / z)) * y = x / (1 / (y \ z)) # label(459).  [para(388(a,1),774(a,1,2)),flip(a)].
% 2099 ((((x / y) / z) * y) / x) \ 1 = x / (x * (y \ (z \ y))).  [para(774(a,1),644(a,1,1,1)),rewrite(379(10))].
% 2102 (1 / (x / y)) * (y \ x) = y / ((y \ x) \ x) # label(462).  [para(659(a,1),774(a,2,1)),rewrite(3(3)),flip(a)].
% 2149 (x / ((y * z) / y)) * y = (x * y) / z # label(351).  [para(4(a,1),775(a,1,2)),flip(a)].
% 2196 (x / ((1 / y) \ z)) * y = (x * y) / (z * y) # label(481).  [para(1032(a,1),775(a,2,1,2)),rewrite(4(4)),flip(a)].
% 2244 (1 / (x * y)) \ (x * ((x \ 1) / y)) = x # label(313).  [para(400(a,1),863(a,1,1,2)),rewrite(41(7),114(5),3(3),921(11),15(7))].
% 2246 ((x * ((x \ 1) * y)) / (y / (x \ 1))) \ 1 = ((y / (x \ 1)) / (x * y)) * x # label(490).  [para(863(a,1),575(a,1,1,2)),rewrite(785(8)),flip(a)].
% 2261 (x / (y \ 1)) \ (((x / (y \ 1)) / (y * x)) * y) = (y * x) \ y # label(495).  [para(863(a,1),647(a,2,1)),rewrite(2246(13),1414(16),2(13))].
% 2265 (x \ (x / y)) \ (y \ (x \ y)) = x \ y # label(483).  [para(3(a,1),890(a,1,2,1)),rewrite(1367(6),2(3))].
% 2308 (x / y) / (1 / y) = y * ((y \ 1) * x) # label(1857).  [para(16(a,1),906(a,1,1,2)),rewrite(16(10),17(8))].
% 2348 (1 / (1 / (x / y))) * (y / (y \ x)) = (y \ x) * (((y \ x) \ 1) * y).  [back_rewrite(1950),rewrite(2308(14))].
% 2350 (1 / ((x / y) / x)) * (x / y) = y * ((y \ 1) * x).  [back_rewrite(1931),rewrite(2308(10))].
% 2479 (1 / (x / y)) * ((x / y) / x) = (1 / y) / (x / y) # label(503).  [para(16(a,1),921(a,1,1,2)),flip(a)].
% 2490 ((1 / (x \ y)) \ ((1 / x) * (x / y))) / (x \ y) = 1 / ((1 / (x \ y)) \ x) # label(507).  [para(921(a,1),388(a,1,2,1)),rewrite(1078(12),2(10))].
% 2523 (1 / (x \ y)) \ ((1 / x) * (x / y)) = (x \ y) / y # label(511).  [para(921(a,1),623(a,2,2)),rewrite(16(5),16(6),3(3)),flip(a)].
% 2537 ((x \ y) / y) / (x \ y) = 1 / ((1 / (x \ y)) \ x) # label(2519).  [back_rewrite(2490),rewrite(2523(8))].
% 2542 (x \ (y \ x)) / (y \ x) = y \ (y / x) # label(334).  [para(3(a,1),923(a,1,1,1)),rewrite(1367(10),2(7))].
% 2551 x * (((x * y) \ y) / y) = x / (x * y) # label(338).  [para(923(a,2),18(a,2,2)),rewrite(114(4),2(2),2(4)),flip(a)].
% 2554 x \ (x / (x * y)) = ((x * y) \ y) / y # label(430) # label(277).  [para(923(a,2),51(a,2)),rewrite(114(4),2(2))].
% 2608 (x \ 1) / (((x * y) \ y) / y) = x \ (x / (1 / y)) # label(340).  [para(923(a,2),623(a,1,2))].
% 2622 (x \ (x / y)) / (y \ (x \ y)) = 1 / ((y \ (x * y)) \ y) # label(529).  [back_rewrite(1897),rewrite(2542(4))].
% 2639 (1 / x) / (y / x) = (1 / x) * (x / y) # label(1885).  [para(16(a,1),953(a,1,2,1))].
% 2671 (1 / (x / y)) * ((x / y) / x) = (1 / y) * (y / x) # label(531).  [back_rewrite(2479),rewrite(2639(10))].
% 2774 (x * (y / x)) * ((y / x) \ 1) = y * ((x \ y) \ 1) # label(536).  [para(296(a,1),1072(a,2,1)),rewrite(15(8),1265(6),3(2),2036(12)),flip(a)].
% 2783 (x / (x \ y)) * (x \ 1) = x \ ((x * x) / y) # label(541).  [para(615(a,1),1072(a,2,1)),rewrite(1233(6),1(2)),flip(a)].
% 3023 x \ (y / (1 / x)) = (x \ 1) * (y * x) # label(2954).  [para(195(a,1),1106(a,1,2)),rewrite(5(9)),flip(a)].
% 3037 x \ ((x * x) / y) = 1 / (y * (x \ 1)) # label(372).  [para(1106(a,1),985(a,1,1,1,1)),rewrite(1731(6),227(3),783(10),1147(5),15(4),775(11),15(7),5(4),2783(5))].
% 3046 (x / y) * ((y * z) / y) = (x * z) / y # label(306).  [para(4(a,1),1147(a,1,1,2)),flip(a)].
% 3092 ((x \ 1) \ y) / x = (x * y) * (1 / x) # label(2497).  [para(205(a,1),1147(a,1,1)),rewrite(5(7))].
% 3154 (x * (y \ x)) * (x \ 1) = (y * (x \ 1)) \ 1 # label(212).  [para(647(a,1),1265(a,1,2)),rewrite(134(7),454(7),1727(9),1(7)),flip(a)].
% 3163 (x \ y) \ (x \ z) = x \ ((y / x) \ z) # label(4601) # label(190) # label(2469).  [para(1346(a,1),4(a,1,2))].
% 3276 x \ ((y / x) \ (x \ y)) = ((x \ y) \ y) \ 1 # label(1567).  [back_rewrite(337),rewrite(3163(4))].
% 3279 (x \ (y * z)) / (x \ z) = x \ (y * x) # label(159).  [para(1347(a,1),5(a,1,1))].
% 3366 (x \ (y * x)) \ z = x \ (y \ (x * z)) # label(611).  [para(1400(a,1),4(a,1,2)),flip(a)].
% 3371 (x \ 1) * ((y * (x \ 1)) \ z) = (x \ y) \ ((x \ 1) * z) # label(216).  [para(61(a,1),1400(a,1,2,1,2)),rewrite(3163(7),1000(6),51(5))].
% 3386 ((1 / x) * y) \ 1 = (y \ (x * x)) / x # label(264).  [para(1400(a,1),575(a,1,1)),rewrite(862(6)),flip(a)].
% 3398 x \ (y \ (x * ((1 / x) * y))) = y \ (y / x) # label(3540).  [para(1400(a,1),623(a,1,2)),rewrite(3366(4),2(2),2(4),2542(4),862(7),3366(8)),flip(a)].
% 3428 (x \ (x / y)) / (y \ (x \ y)) = 1 / (y \ (x \ (y * y))) # label(610).  [back_rewrite(2622),rewrite(3366(9))].
% 3446 ((x \ (y * x)) * (z * (x \ (y \ x)))) * u = (x \ (y * x)) * (z * (x \ (y \ (x * u)))).  [back_rewrite(2070),rewrite(3366(12))].
% 3460 (x \ (y \ x)) * ((z * x) * (x \ (y \ x))) = x \ (y \ (x * ((z / y) * x))).  [back_rewrite(1143),rewrite(3366(12))].
% 3489 x \ (y \ (x * (((x \ (y * x)) * y) * x))) = x / (x \ (y \ x)) # label(613).  [back_rewrite(349),rewrite(3366(7))].
% 3528 (x / y) * ((y \ x) \ 1) = (x / (x / y)) \ y # label(370).  [para(315(a,1),1514(a,2,2)),rewrite(6(2)),flip(a)].
% 3579 ((x \ (y * x)) * (y \ x)) \ z = x \ (y * (x \ (y \ (x * z)))) # label(625).  [para(1347(a,1),1514(a,2)),rewrite(774(6),5(4),780(4),3366(8))].
% 3592 (x * (y \ (z * x))) / x = (y / x) \ z # label(440).  [para(1727(a,1),5(a,1,1))].
% 3594 (x \ y) * (y \ (z * (x \ y))) = (x \ z) * (x \ y) # label(441).  [para(15(a,1),1727(a,1,1,1)),flip(a)].
% 3631 (((1 / x) * y) \ z) * x = y \ (x * (z * x)) # label(447).  [para(862(a,1),1727(a,1,1,1)),rewrite(3366(9),3(10))].
% 3673 x \ (((y / x) \ z) * u) = (y \ (z * x)) * (x \ u) # label(3242).  [para(1727(a,1),1347(a,1,1,2)),rewrite(4(4)),flip(a)].
% 3676 (x * (y \ (x \ z))) * x = x * ((x * y) \ (z * x)) # label(380).  [para(1514(a,1),1727(a,1,1))].
% 3688 (x \ y) \ (y \ (x \ y)) = (y \ x) * (y \ (x \ y)) # label(262).  [para(15(a,1),1747(a,1,1,2)),flip(a)].
% 3690 ((x / y) / x) * y = x * (y \ (x \ y)) # label(382).  [para(1747(a,1),17(a,2,2)),rewrite(3(4))].
% 3704 (x / y) * ((x \ y) / y) = (x / y) / x.  [para(1747(a,1),43(a,1,1,2)),rewrite(1147(4),3(7))].
% 3735 x / (x * (y \ (x \ y))) = (x / y) * ((x * y) / x) # label(640).  [para(1000(a,1),1747(a,1,2)),rewrite(2639(6),4(7),1000(9),1755(8),379(8)),flip(a)].
% 3806 (x * ((y * x) \ z)) / x = y \ (z / x) # label(185).  [para(1768(a,1),5(a,1,1))].
% 3886 x \ ((y \ (z / x)) * u) = ((y * x) \ z) * (x \ u) # label(648).  [para(1768(a,1),1347(a,1,1,2)),rewrite(4(4)),flip(a)].
% 3966 (x / (y \ z)) / y = (x / y) / (z / y) # label(396) # label(2360).  [para(2065(a,1),5(a,1,1))].
% 4032 (x / (y \ z)) * (y \ 1) = y \ ((y * x) / z) # label(708).  [para(2065(a,1),1072(a,2,1)),rewrite(1233(6),6(2)),flip(a)].
% 4033 x * ((y / (x \ z)) \ 1) = ((x * y) / z) \ x # label(499).  [para(2065(a,1),1082(a,2,2,1)),rewrite(1233(6),6(2)),flip(a)].
% 4057 x \ (((x * y) * x) / z) = y / (z * (x \ 1)) # label(871).  [back_rewrite(2073),rewrite(4032(8),74(4))].
% 4062 (x * (y \ 1)) / (z * (y \ 1)) = y \ ((y * x) / z) # label(3251).  [back_rewrite(783),rewrite(4032(12))].
% 4066 (x / ((y * z) / y)) \ ((x * y) / z) = y # label(2426).  [para(2149(a,1),4(a,1,2))].
% 4067 ((x * y) / z) / y = x / ((y * z) / y) # label(2938).  [para(2149(a,1),5(a,1,1))].
% 4069 (x * (y / ((z * u) / z))) * z = (x * z) * (z \ ((y * z) / u)) # label(1356) # label(1475).  [para(2149(a,1),8(a,1,2,2)),flip(a)].
% 4088 (x / ((y * z) / y)) * (y * u) = y * ((y \ ((x * y) / z)) * u) # label(1660).  [para(2149(a,1),34(a,1,2,1,2)),flip(a)].
% 4140 x \ ((y / ((x * z) / x)) * u) = (x \ ((y * x) / z)) * (x \ u) # label(729).  [para(2149(a,1),1347(a,1,1,2)),flip(a)].
% 4174 (1 / (x * y)) * x = x * ((x \ 1) / y) # label(733).  [para(2244(a,1),3(a,1,2))].
% 4270 (1 / (x / (y \ 1))) \ (y * ((y \ 1) / x)) = ((x / (y \ 1)) / (y * x)) * y.  [back_rewrite(1922),rewrite(4174(9))].
% 4287 x / (y / (x \ 1)) = x * ((x \ 1) / y) # label(956).  [back_rewrite(627),rewrite(4174(8))].
% 4382 ((x / y) \ 1) / ((x \ y) / y) = y * ((y \ x) \ ((y \ 1) * x)).  [para(2308(a,1),623(a,2,2)),rewrite(1161(9),1(6),227(12))].
% 4407 (x / y) \ ((x / y) / x) = (x \ y) / y # label(485).  [para(16(a,1),2542(a,1,1,2)),rewrite(16(3)),flip(a)].
% 4431 ((x / (y \ 1)) \ 1) / ((y * x) \ y) = (y * x) \ ((y * x) / y) # label(740).  [para(340(a,2),2542(a,1,1))].
% 4442 (x \ (y \ (x * (z \ (x \ (y * x)))))) / (z \ (x \ (y * x))) = z \ (((z / x) / y) * x) # label(392).  [para(774(a,1),2542(a,2,2)),rewrite(3366(6))].
% 4532 (1 / (x / (x * y))) \ (x / (1 / y)) = x # label(395).  [para(2551(a,1),2244(a,1,1,2)),rewrite(2608(10),3(9))].
% 4633 (1 / (x \ y)) * ((x \ y) / y) = (1 / x) * (x / y) # label(755).  [para(15(a,1),2639(a,1,2)),rewrite(3966(4),2639(4)),flip(a)].
% 4657 (1 / (x / y)) \ ((1 / y) * (y / x)) = (x / y) / x # label(760).  [para(2639(a,1),1000(a,1,2)),rewrite(114(14),2(11),6(11))].
% 4807 ((x * x) / y) / (1 / (y * (x \ 1))) = x # label(2340).  [para(3037(a,1),15(a,1,2))].
% 4926 ((x * y) * z) / y = x * ((y * z) / y) # label(143).  [para(5(a,1),3046(a,1,1)),flip(a)].
% 4935 x * (y * (z * (x \ 1))) = ((x * y) * z) / x # label(765).  [para(3046(a,1),18(a,1)),rewrite(51(6)),flip(a)].
% 4955 (x * ((x \ y) * z)) / y = ((y * z) / x) / (y / x) # label(769).  [para(3046(a,1),114(a,1,1)),rewrite(17(7),6(9)),flip(a)].
% 4959 (x / y) * ((x * y) / x) = x * (y \ ((x * y) / x)) # label(795).  [para(3046(a,1),509(a,1,1)),rewrite(1(2),1755(4),379(4),3735(4),227(10),4(6))].
% 4976 (x \ y) * (z * (x \ 1)) = x \ ((y * z) / x) # label(304).  [para(3046(a,1),215(a,1,2)),rewrite(51(7)),flip(a)].
% 5030 (((1 / x) * y) * z) / ((1 / x) * y) = (1 / x) * ((1 / y) \ ((z / y) * x)) # label(786).  [back_rewrite(566),rewrite(4926(8),1076(7)),flip(a)].
% 5044 x / (x * (y \ (x \ y))) = x * (y \ ((x * y) / x)) # label(788).  [back_rewrite(3735),rewrite(4959(8))].
% 5097 ((x * y) * (1 / x)) \ (x * z) = x * ((x \ ((x \ 1) \ y)) \ z).  [para(3092(a,1),227(a,1,1))].
% 5131 x \ ((((x * y) / x) / x) \ z) = (y * (x \ 1)) \ (x \ z) # label(794).  [para(51(a,1),3163(a,1,1)),flip(a)].
% 5140 (1 / (x \ y)) \ (x \ z) = x \ ((x / y) \ z) # label(1018).  [para(388(a,1),3163(a,1,1)),rewrite(5(8))].
% 5150 x \ (((y / x) \ 1) \ z) = (y \ x) \ (x \ z) # label(3400).  [para(575(a,1),3163(a,2,2,1)),rewrite(4(3)),flip(a)].
% 5167 ((x \ (y * x)) * z) \ (x \ u) = x \ (((y * (x * z)) / x) \ u) # label(801).  [para(231(a,1),3163(a,1,1))].
% 5168 (x \ y) \ ((x \ (z * x)) * u) = x \ ((y / x) \ (z * (x * u))).  [para(231(a,1),3163(a,1,2))].
% 5256 x \ ((y / z) * x) = (x \ y) / (x \ z) # label(404) # label(1358).  [para(6(a,1),3279(a,1,1,2)),flip(a)].
% 5260 (x / y) \ (z * (x / y)) = ((x / y) \ (z * x)) / y # label(298).  [para(16(a,1),3279(a,1,2)),flip(a)].
% 5314 (x * (y \ (x \ (z * u)))) / (x * (y \ (x \ u))) = x / (x * (y \ (x \ (z \ (x * y))))).  [para(1514(a,1),3279(a,1,1)),rewrite(1514(7),5260(14),1514(13),231(11),379(14),3366(11))].
% 5315 x / (x * (y \ (x \ (z \ (x * y))))) = x * (y \ (x \ (z * ((x * y) / x)))).  [para(1514(a,1),3279(a,2)),rewrite(1514(4),1514(7),5314(8))].
% 5388 x / (y \ (z \ (y * x))) = y \ (z * y) # label(208).  [para(3366(a,1),15(a,1,2))].
% 5392 (x * (y \ (x \ (z * ((x * y) / x))))) \ u = x * (y \ (x \ (z \ (x * (y * (x \ u)))))).  [para(18(a,1),3366(a,2,2,2)),rewrite(5260(6),1514(5),231(3),379(6),3366(3),5315(6),1514(14))].
% 5395 (x \ 1) \ ((x \ y) \ ((x \ 1) * z)) = (y * (x \ 1)) \ z # label(815).  [para(61(a,1),3366(a,1,1,2)),rewrite(3163(5),1000(4),51(3)),flip(a)].
% 5423 (x * ((x \ y) \ (y / x))) \ z = (y / x) \ ((x \ y) * (x \ z)).  [para(215(a,1),3366(a,2,2)),rewrite(227(4))].
% 5464 1 / ((x \ (y * y)) / y) = (1 / y) * x # label(820).  [para(3386(a,1),15(a,1,2))].
% 5675 (x / y) \ (z / y) = (y * (x \ z)) / y # label(2986) # label(443).  [para(6(a,1),3592(a,1,1,2,2)),flip(a)].
% 5681 (x \ (y * z)) * (z \ 1) = z \ ((x / z) \ y) # label(1068).  [para(3592(a,1),51(a,1,2)),flip(a)].
% 5715 (x * y) / (z \ (u * y)) = (x / ((z / y) \ u)) * y # label(312).  [para(3592(a,1),775(a,2,1,2)),rewrite(4(5))].
% 5720 (x * (y \ (z * u))) / u = (x / u) * ((y / u) \ z) # label(314).  [para(3592(a,1),1147(a,2,2)),rewrite(4(4))].
% 5732 (x / y) \ ((z / y) / (u / y)) = (y * (x \ (z / (y \ u)))) / y # label(833).  [para(2065(a,1),3592(a,1,1,2,2)),flip(a)].
% 5735 (x / y) \ (z / ((y * u) / y)) = (y * (x \ ((z * y) / u))) / y # label(835).  [para(2149(a,1),3592(a,1,1,2,2)),flip(a)].
% 5800 (x * ((x \ y) \ y)) / x = x * ((x \ y) \ (y / x)).  [back_rewrite(963),rewrite(5675(4))].
% 5820 (x * (y * (x \ z))) / ((x * y) / x) = (x * y) / (x * (y * (x \ (z \ x)))) # label(197).  [back_rewrite(1036),rewrite(5735(6),5675(4),379(4),114(6)),flip(a)].
% 5830 x / (y * (z * (y \ (u \ (y * (z \ (y \ x))))))) = (y * z) / (y * (z * (y \ (u \ y)))).  [back_rewrite(1516),rewrite(5820(14))].
% 5889 (x / ((y / z) / y)) * (y * (z \ (y \ z))) = ((y / z) / y) * ((((y / z) / y) \ x) * z) # label(842).  [para(3690(a,1),17(a,1,2))].
% 5898 (x \ y) * ((y * (x \ 1)) \ 1) = x \ ((y * x) / y) # label(437).  [para(97(a,1),3690(a,1,1,1)),rewrite(789(4),255(7),43(4),3163(10),647(10),134(11),3154(10),11(11)),flip(a)].
% 5903 (x / y) * (x \ (y * x)) = x * ((x * y) \ (y * x)).  [para(3690(a,1),28(a,1,1)),rewrite(3676(4)),flip(a)].
% 5915 (1 / (x / (x / y))) * y = (x / (x / y)) \ y # label(417).  [para(315(a,1),3690(a,2,2)),rewrite(738(4),3528(10))].
% 5918 (x * (y \ (x \ y))) \ (z * y) = y \ ((((x / y) / x) \ z) * y).  [para(3690(a,1),135(a,1,1))].
% 5932 (x / ((y * x) / y)) \ 1 = (1 / y) \ ((x / y) / x) # label(420).  [para(3690(a,1),1032(a,1,1,2)),rewrite(1533(5),4067(3))].
% 5940 ((x / y) / x) \ ((x * (y \ (x \ y))) \ ((x / y) / x)) = (1 / x) \ ((y / x) / y) # label(851).  [para(3690(a,1),340(a,2,2,1)),rewrite(644(4),5932(5)),flip(a)].
% 5949 (x / (x / y)) \ y = (x / y) / (y \ x) # label(436).  [para(3690(a,1),775(a,2)),rewrite(6(3),315(7),3528(8)),flip(a)].
% 5961 1 / ((1 / x) \ ((y / x) / y)) = y / ((x * y) / x).  [para(3690(a,1),1092(a,1,1,2)),rewrite(264(4),4067(3)),flip(a)].
% 5969 (x * (y \ (x \ y))) \ x = y \ (x * y) # label(440).  [para(3690(a,1),1771(a,1,1))].
% 5971 x * (y * (x \ (y \ 1))) = x / ((y * x) / y) # label(447).  [para(3690(a,1),2149(a,1)),rewrite(1514(5),12(3),4(6),18(5),6(9),4067(8))].
% 5980 x * ((x \ 1) * (y \ ((x * y) / x))) = (1 / ((1 / x) * y)) * (y / x) # label(874).  [para(2639(a,1),3690(a,1,1,1)),rewrite(114(7),6(3),5675(14),11(12),5675(13),379(13),5044(13),17(14)),flip(a)].
% 5987 x * (((x \ y) \ y) \ 1) = x / ((x \ y) \ y) # label(880).  [para(3163(a,1),3690(a,2,2)),rewrite(3966(3),13(1),2102(5),3276(7)),flip(a)].
% 5998 (1 / (x / (x / y))) * y = (x / y) / (y \ x) # label(561).  [back_rewrite(5915),rewrite(5949(8))].
% 6121 (1 / x) \ ((x \ (y * x)) / y) = (y * x) / y.  [para(824(a,1),3806(a,1,1,2)),flip(a)].
% 6138 (x * y) / ((z * y) \ u) = (x / (z \ (u / y))) * y # label(222).  [para(3806(a,1),775(a,2,1,2)),rewrite(4(5))].
% 6169 ((x * y) \ z) \ (y \ u) = y \ ((x \ (z / y)) \ u) # label(3290).  [para(3806(a,1),3163(a,2,2,1)),rewrite(4(4))].
% 6350 (x / y) / ((y * z) / y) = (x / z) / y # label(2392).  [para(4(a,1),3966(a,1,1,2)),flip(a)].
% 6578 ((x * (y \ (z * y))) / u) / y = ((x / y) * z) / ((y * u) / y).  [para(28(a,1),4067(a,1,1,1))].
% 6583 x / ((y * (x * (z \ y))) / y) = ((x * z) / x) / y # label(2947).  [para(113(a,1),4067(a,1,1)),flip(a)].
% 6604 (x / ((y * z) / y)) \ (y * u) = y * ((y \ ((x * y) / z)) \ u).  [para(4067(a,1),227(a,1,1))].
% 6609 x / ((y \ (z * y)) * (u * (y \ (z \ y)))) = ((x / y) / ((z * (y * u)) / (z * y))) * y.  [para(4067(a,1),774(a,1)),rewrite(774(6),816(6),6578(12),4067(13),114(12))].
% 6627 (x * (y / z)) / (z \ y) = (x / (y / (y / z))) * z # label(1485).  [para(4067(a,1),2065(a,1,1)),rewrite(6(2)),flip(a)].
% 6868 (x / (x \ y)) \ (1 / (y / x)) = (x \ (x \ y)) / (x \ y) # label(499).  [para(3966(a,1),4407(a,1,2)),rewrite(13(3))].
% 6876 (x / (1 / y)) / x = 1 / (x / (x * y)) # label(450).  [para(4532(a,1),15(a,1,2))].
% 6997 (x * y) \ (x * x) = (y \ 1) / (x \ 1) # label(310).  [para(4807(a,1),1771(a,1,1,1)),rewrite(4174(9),4(10))].
% 7029 (x * (y \ (z * y))) / z = (x / y) * ((z * y) / z) # label(991).  [para(28(a,1),4926(a,1,1))].
% 7092 (x * ((y * z) / y)) / z = (x * y) / ((z * y) / z) # label(2116).  [para(4926(a,1),4067(a,1,1))].
% 7113 x * ((x \ y) / (x \ z)) = (y / z) * x # label(582).  [para(5256(a,1),3(a,1,2))].
% 7121 (x \ y) / (z * (x \ 1)) = x \ ((y * x) / z) # label(929).  [para(51(a,1),5256(a,2,2)),rewrite(2149(4)),flip(a)].
% 7146 ((x \ y) / x) / (z / x) = (1 / x) * (y / z) # label(2412).  [para(5256(a,1),862(a,1,1)),rewrite(3966(4))].
% 7151 ((x \ y) / (x \ z)) * (x \ u) = x \ ((y / z) * u) # label(1021).  [para(5256(a,1),215(a,2,1)),rewrite(5(3)),flip(a)].
% 7163 x / ((y \ z) / (y \ u)) = ((x / y) / (z / u)) * y.  [para(5256(a,1),774(a,1,2))].
% 7252 ((x / y) \ (z * x)) / y = y / ((x / y) \ (z \ x)) # label(1025).  [para(6(a,1),5388(a,1,2,2,2)),rewrite(5260(8)),flip(a)].
% 7351 (x / y) \ (z * (x / y)) = y / ((x / y) \ (z \ x)) # label(814).  [back_rewrite(5260),rewrite(7252(8))].
% 7429 ((1 / x) * y) \ (z / x) = (y \ (x * z)) / x # label(679).  [para(862(a,1),5675(a,1,1)),rewrite(3366(8),3(9))].
% 7430 (x * (y \ (x \ (z * x)))) / x = (y / x) \ ((1 / x) * z) # label(1035).  [para(862(a,1),5675(a,1,2)),flip(a)].
% 7461 (x / (y / z)) \ ((1 / z) * (z / y)) = y / ((y / z) * ((x \ (1 / z)) \ z)) # label(1039).  [para(2639(a,1),5675(a,1,2)),rewrite(265(14))].
% 7474 (x / (y / (z \ 1))) \ (z * ((z \ 1) / y)) = y / ((y / (z \ 1)) * ((x \ z) \ (z \ 1))).  [para(4287(a,1),5675(a,1,2)),rewrite(265(18))].
% 7489 x / ((x * (y * y)) / y) = (x / y) / x # label(474).  [back_rewrite(4657),rewrite(7461(8),11(5),1164(5))].
% 7490 x / (y \ ((y * x) * (y \ 1))) = ((x / (y \ 1)) / (y * x)) * y.  [back_rewrite(4270),rewrite(7474(10),11(5),1353(7))].
% 7495 (x / y) \ (y \ x) = y / ((y \ x) \ x) # label(1044).  [para(15(a,1),5949(a,1,1,2)),rewrite(15(5))].
% 8259 1 / (x \ (y \ (x * y))) = (x * y) \ (y * x) # label(467).  [para(5969(a,1),363(a,1,2,2)),rewrite(3676(9),4(10))].
% 8264 x \ (((y * x) * (y \ 1)) * x) = (y * ((y * x) \ x)) \ x.  [para(505(a,1),5969(a,2,2)),rewrite(3688(6),1347(6),3(5),1847(10)),flip(a)].
% 8265 x * ((y \ (x \ y)) \ (x \ 1)) = x * (y \ ((x * y) / x)) # label(1063).  [para(5969(a,1),575(a,1,1,2)),rewrite(379(4),5044(4),1514(10)),flip(a)].
% 8284 ((x \ (y \ x)) / (y \ 1)) \ 1 = y \ (x \ (y * x)) # label(468).  [para(5969(a,1),340(a,2,2))].
% 8323 (x * (y \ (x \ y))) \ (z * (x * (y \ (x \ y)))) = ((((x * (y \ (x \ y))) \ (z * x)) / y) / x) * y.  [para(5969(a,1),3279(a,1,2)),rewrite(774(8)),flip(a)].
% 8330 (x / (y * (z \ (y \ z)))) / (y * (z \ ((y * z) / y))) = (((x / z) / y) * z) / (y * (z \ (y \ z))).  [para(5969(a,1),3966(a,1,1,2)),rewrite(774(3),5044(15)),flip(a)].
% 8361 ((x * y) \ y) \ ((x \ 1) * y) = (x * ((x * y) \ y)) \ y.  [back_rewrite(1847),rewrite(8264(12))].
% 8385 (x * (y * x)) / (x * y) = (x * y) / ((x * y) / x) # label(343).  [para(6350(a,1),644(a,1,1)),rewrite(4067(3),644(6),114(4),6(7))].
% 8664 x \ ((y \ 1) / (x \ 1)) = (y / (x \ 1)) \ x # label(2334).  [para(6997(a,1),3366(a,2,2)),rewrite(86(3)),flip(a)].
% 8691 ((x * y) / z) * x = x * (y / (x \ z)) # label(476).  [para(4(a,1),7113(a,1,2,1)),flip(a)].
% 8692 (x / (y * z)) * y = y * ((y \ x) / z) # label(1116).  [para(4(a,1),7113(a,1,2,2)),flip(a)].
% 8697 (x / y) * (((x / y) \ z) / y) = (z / x) * (x / y) # label(1632).  [para(16(a,1),7113(a,1,2,2))].
% 8828 x / (y \ ((y * x) * (y \ 1))) = y * ((y \ (x / (y \ 1))) / x).  [back_rewrite(7490),rewrite(8692(12))].
% 8844 (x / (y \ 1)) \ (y * ((y \ (x / (y \ 1))) / x)) = (y * x) \ y # label(1120).  [back_rewrite(2261),rewrite(8692(9))].
% 8845 x * ((x \ (y / x)) / z) = y / (z / (x \ 1)) # label(964).  [back_rewrite(2076),rewrite(8692(4))].
% 8857 ((x / y) / x) \ x = (x * (y * y)) / y # label(535).  [para(7489(a,1),16(a,1,1))].
% 8862 x / ((x * (y \ (1 / y))) / (y \ 1)) = (x / (y \ 1)) / x.  [para(61(a,1),7489(a,1,2,1,2))].
% 8897 (x / y) / (y \ x) = x / ((y \ x) * y) # label(1128).  [para(7489(a,1),2065(a,1,1)),rewrite(738(4),5998(5),17(6),4(7))].
% 9012 (x \ 1) \ ((x * y) \ y) = x * ((x * y) \ y) # label(1841).  [para(453(a,1),7495(a,1,2)),rewrite(5(4),453(9),8361(11),15(10))].
% 9711 (x * ((y * z) / u)) * y = (x * y) * (z / (y \ u)) # label(863).  [para(8691(a,1),8(a,1,2,2)),rewrite(4(5)),flip(a)].
% 9750 (1 / x) * ((x * y) / z) = (y / x) / (z / x) # label(1142).  [para(8691(a,1),862(a,1,1,2)),rewrite(4(4),3966(3)),flip(a)].
% 9785 x \ (((x * y) / z) * u) = (y / (x \ z)) * (x \ u) # label(886).  [para(8691(a,1),1347(a,1,1,2)),rewrite(4(4)),flip(a)].
% 9848 (x / (y * (z * (y \ u)))) * ((y * z) / y) = y * (z * (y \ ((y * (z \ (y \ x))) / u))).  [para(18(a,1),8692(a,1,1,2)),rewrite(1514(12),18(14))].
% 9860 (x / (y * z)) * (y * u) = y * (((y \ x) / z) * u) # label(410).  [para(8692(a,1),34(a,1,2,1,2)),rewrite(4(4)),flip(a)].
% 9925 x \ ((y / (x * z)) \ (x * u)) = ((x \ y) / z) \ u # label(953).  [para(8692(a,1),3366(a,1,1,2)),rewrite(4(4)),flip(a)].
% 9985 x / ((1 / x) \ (y \ 1)) = ((1 / x) \ y) / x.  [para(8857(a,1),97(a,1,2)),rewrite(14(4),1(6),5(5),14(8),14(10),7351(10)),flip(a)].
% 10188 (x * y) / (y * x) = x / ((y * x) / y) # label(515).  [para(4(a,1),8897(a,1,2)),rewrite(4067(3),4(6)),flip(a)].
% 10189 (x \ y) * (((x \ y) \ y) / x) = y / x # label(427).  [para(8897(a,1),6(a,1,1)),rewrite(8692(5))].
% 10700 x * (y * ((x * y) \ (y * x))) = y * x # label(32).  [para(10188(a,1),6(a,1,1)),rewrite(4088(5),1768(4))].
% 10717 (x * (y / ((z * y) / z))) * (z * y) = (x * (z * y)) * ((z * y) \ (y * z)).  [para(10188(a,1),29(a,1,1,2))].
% 10805 (x / ((y * x) / y)) * x = x * (y * (x \ (y \ x))) # label(1349).  [para(10188(a,1),8691(a,1,1)),rewrite(774(7),3690(7))].
% 10808 x * ((x \ (y * x)) / y) = (y * x) / y # label(1071).  [para(10188(a,1),8692(a,1,1)),rewrite(2149(4)),flip(a)].
% 10830 (x \ y) \ (y / x) = ((x \ y) \ y) / x # label(825).  [para(10189(a,1),4(a,1,2))].
% 10968 (x * ((x \ y) \ y)) / x = x * (((x \ y) \ y) / x).  [back_rewrite(5800),rewrite(10830(7))].
% 10971 (x * (((x \ y) \ y) / x)) \ z = (y / x) \ ((x \ y) * (x \ z)).  [back_rewrite(5423),rewrite(10830(3))].
% 11233 x * ((y * x) \ (x * y)) = y \ (x * y) # label(512).  [para(10700(a,1),4(a,1,2)),flip(a)].
% 11263 (1 / x) \ ((y / x) / z) = (x * y) / (z * x) # label(630).  [para(10700(a,1),114(a,2,2)),rewrite(11233(4),774(3),1032(5))].
% 11341 1 / (x / ((y * x) / y)) = y / ((x * y) / x) # label(557).  [back_rewrite(5961),rewrite(11263(6),10188(4))].
% 11342 ((x / y) / x) \ ((x * (y \ (x \ y))) \ ((x / y) / x)) = x / ((y * x) / y).  [back_rewrite(5940),rewrite(11263(14),10188(12))].
% 11343 (x / ((y * x) / y)) \ 1 = y / ((x * y) / x) # label(1308).  [back_rewrite(5932),rewrite(11263(10),10188(8))].
% 11444 x \ ((y * x) / y) = (x \ (y * x)) / y # label(293).  [para(10808(a,1),4(a,1,2))].
% 11530 (x / ((y \ (z * y)) / z)) / y = (x / y) / (z / ((y * z) / y)).  [para(10808(a,1),6350(a,1,2,1)),rewrite(4067(4)),flip(a)].
% 11551 (x / (y * (z \ (y \ z)))) / (y * ((z \ (y * z)) / y)) = (((x / z) / y) * z) / (y * (z \ (y \ z))).  [back_rewrite(8330),rewrite(11444(7))].
% 11558 x * ((y \ (x \ y)) \ (x \ 1)) = x * ((y \ (x * y)) / x) # label(1065).  [back_rewrite(8265),rewrite(11444(9))].
% 11565 x * ((x \ 1) * ((y \ (x * y)) / x)) = (1 / ((1 / x) * y)) * (y / x) # label(898).  [back_rewrite(5980),rewrite(11444(5))].
% 11568 (x \ y) * ((y * (x \ 1)) \ 1) = (x \ (y * x)) / y.  [back_rewrite(5898),rewrite(11444(10))].
% 11572 x / (x * (y \ (x \ y))) = x * ((y \ (x * y)) / x) # label(899).  [back_rewrite(5044),rewrite(11444(7))].
% 11593 (x \ (y * x)) * (y \ 1) = (x \ (y * x)) / y # label(292).  [back_rewrite(1476),rewrite(11444(8))].
% 11701 x * (((x \ y) * x) \ y) = (x \ y) \ y # label(746).  [para(10830(a,1),1768(a,1,1)),rewrite(6(4)),flip(a)].
% 11790 (x * y) \ (y * x) = y \ (x \ (y * x)) # label(519).  [para(11233(a,1),4(a,1,2)),flip(a)].
% 11839 (x \ (y \ x)) / (y \ 1) = x \ (y \ (x * y)) # label(530).  [para(11233(a,1),985(a,1,1,1,1)),rewrite(11790(5),3366(6),11790(9),4442(10),3690(3),4(4),11790(9),8259(10),11790(8))].
% 11878 1 / (x * (y \ (x \ y))) = (y \ (x * y)) / x # label(252).  [para(11233(a,1),6876(a,2,2,2)),rewrite(11790(4),8259(5),11790(3),5388(4),774(7),3690(7)),flip(a)].
% 11913 (x * (y / ((z * y) / z))) * (z * y) = (x * (z * y)) * (y \ (z \ (y * z))).  [back_rewrite(10717),rewrite(11790(11))].
% 11916 1 / (x \ (y \ (x * y))) = y \ (x \ (y * x)) # label(532).  [back_rewrite(8259),rewrite(11790(8))].
% 11917 (x / y) * (x \ (y * x)) = x * (y \ (x \ (y * x))).  [back_rewrite(5903),rewrite(11790(7))].
% 11918 (A * B) * (C \ (D \ (C * D))) != A * (B * (C \ (D \ (C * D)))) # label(435).  [back_rewrite(10),rewrite(11790(10),11790(20))].
% 11946 (x \ (y \ (x * y))) \ 1 = y \ (x \ (y * x)) # label(533).  [back_rewrite(8284),rewrite(11839(5))].
% 12004 ((x \ (y * x)) / y) \ (x \ z) = x \ ((y / ((x * y) / x)) \ z).  [para(11444(a,1),3163(a,1,1)),rewrite(4067(8))].
% 12271 x \ ((y \ (x * y)) * x) = (x \ (y \ (x * y))) * x # label(335).  [para(135(a,1),11701(a,1,2)),rewrite(3366(3),3(6),3366(8),231(7)),flip(a)].
% 12336 (x * (y / x)) \ y = x / ((x \ y) \ y) # label(1048).  [para(6(a,1),11790(a,1,2)),rewrite(6(6),7495(6))].
% 12919 x / ((x \ (y \ (x * y))) * x) = y \ (x \ (y * x)).  [para(5(a,1),12336(a,1,1,2)),rewrite(11790(3),3366(7),231(6),12271(7)),flip(a)].
% 13621 (x / (x / y)) / ((x / y) \ 1) = (x / y) \ (x * (y \ x)) # label(3096).  [para(16(a,1),207(a,1,2,2)),rewrite(29(5),6(3)),flip(a)].
% 14063 (x * (y * y)) / (1 / ((x * y) \ x)) = x * y # label(3170).  [para(404(a,1),15(a,1,2))].
% 14258 (x * (y \ (x \ y))) \ ((x / y) / x) = 1 / y # label(567).  [para(419(a,1),5969(a,2,2)),rewrite(16(7),16(4),3690(3),4(12))].
% 14300 ((x / y) / x) \ (1 / y) = x / ((y * x) / y) # label(1425).  [back_rewrite(11342),rewrite(14258(8))].
% 14463 (x * (y \ z)) * (z \ (y \ z)) = (x * (y \ 1)) * (y \ z).  [para(3(a,1),507(a,1,2,1))].
% 14811 (x * (y \ z)) / (z \ (y \ z)) = y \ ((y * x) * z) # label(572).  [para(527(a,1),2149(a,1,1,2,1)),rewrite(5(6),1353(5)),flip(a)].
% 14821 (x * (y \ (z \ y))) / (z \ y) = z \ ((z * x) / y) # label(2424).  [para(527(a,1),3046(a,1,2,1)),rewrite(5(8),4032(5)),flip(a)].
% 14834 ((x * (y \ (x \ y))) \ 1) * (y \ (x * y)) = (y \ (x * y)) * (x \ (y \ (x * y))).  [para(5969(a,1),527(a,1,1)),rewrite(5969(6),5969(15)),flip(a)].
% 14882 x \ ((1 / (y / x)) * y) = (x \ y) * (y \ x).  [para(579(a,1),4(a,1,2))].
% 14888 x * (y * ((x * y) \ x)) = y * ((y \ 1) * x).  [para(16(a,1),579(a,1,2,2)),rewrite(1768(3),2350(10))].
% 15158 (x * y) * (y * ((x * y) \ z)) = ((x / (x * y)) \ 1) * z.  [para(642(a,1),18(a,1,1)),flip(a)].
% 15161 x \ (x / ((y * x) / y)) = y * (x \ (y \ 1)).  [para(263(a,1),642(a,2,1)),rewrite(4062(10),41(4),4067(3),1514(8))].
% 15418 (x / (x * (y \ (z \ y)))) * u = x * ((y \ (z * y)) * (x \ u)).  [para(1771(a,1),645(a,1,2,1)),rewrite(2099(11)),flip(a)].
% 15651 (x / ((x \ y) / z)) / x = 1 / (y / (x * z)) # label(944).  [para(3(a,1),746(a,1,2,1)),flip(a)].
% 15849 (1 / (x \ y)) \ ((z / (x / y)) * x) = (x \ y) * ((z * x) * (x \ y)) # label(1213).  [para(795(a,1),61(a,2,2)),rewrite(16(10),1727(7),11(6)),flip(a)].
% 16278 (x \ 1) / ((y * (x \ 1)) / y) = (x \ (y / (x \ 1))) / y.  [para(1033(a,1),4067(a,1,1)),flip(a)].
% 17140 (x / y) \ ((1 / y) * x) = y * (x \ (y \ x)) # label(1243).  [para(1747(a,1),1149(a,2,2)),rewrite(97(5),11917(4),7430(5))].
% 17293 (x / (y \ (z \ y))) * (y \ (z \ (y * y))) = z \ ((z * x) * y) # label(1247).  [para(2265(a,1),1161(a,2,1,2)),rewrite(3428(8),16(10),14811(12))].
% 17348 x * ((x \ y) * ((z \ (x * z)) / x)) = (y / z) * ((x * z) / x) # label(1252).  [para(5969(a,1),1161(a,2,1,2)),rewrite(1514(7),11558(7),17(6),7029(10))].
% 17383 (x * ((y \ (z * y)) / z)) / ((z * y) / z) = (x / ((z * y) / z)) * (z / ((y * z) / y)).  [para(11444(a,1),1161(a,2,1,2)),rewrite(11343(8)),flip(a)].
% 17463 (1 / ((1 / x) * y)) * (y / x) = (1 / y) * ((x * y) / x) # label(1253).  [back_rewrite(11565),rewrite(17348(7)),flip(a)].
% 17488 (x * (y \ (z / y))) / (y \ 1) = y \ ((y * x) * (y \ z)).  [para(61(a,1),1164(a,2,1,2)),rewrite(15(7),1353(6)),flip(a)].
% 17551 (x * (y / (z \ u))) / z = (x / z) * ((z * y) / u) # label(880).  [para(2065(a,1),1164(a,2,1,2)),rewrite(5732(7),11(5),114(5),3(4)),flip(a)].
% 17658 x * ((x \ (y / (x \ 1))) / y) = (y / (x \ 1)) / y # label(3103).  [back_rewrite(8862),rewrite(17488(7),8828(6))].
% 17684 (x \ (y \ 1)) / (y \ 1) = (y * x) \ y # label(1270).  [back_rewrite(8844),rewrite(17658(9),4407(8))].
% 17714 (x \ (x \ y)) / (x \ y) = (x \ (y / x)) / (y / x) # label(1504).  [para(615(a,1),17684(a,2,1)),rewrite(16(5),16(7),6868(10)),flip(a)].
% 17767 (x * (y \ (x \ 1))) / (y \ 1) = x * (y \ (x \ y)) # label(1398).  [para(10808(a,1),17684(a,2,1)),rewrite(12004(6),11343(5),15161(4),1514(10))].
% 18132 (x * (y * x)) / (z * x) = (1 / x) \ (y / z) # label(1007).  [para(5(a,1),1233(a,1,2,2)),flip(a)].
% 18157 (1 / x) \ (y / ((1 / x) * z)) = (((1 / x) \ y) / z) * x.  [para(862(a,1),1233(a,1,2,2)),rewrite(774(12),1032(10))].
% 18339 (1 / x) \ (((1 / x) * y) * z) = (y * (z * x)) / x # label(1258).  [para(16(a,1),1353(a,1,1,2)),rewrite(1164(5)),flip(a)].
% 18349 x \ (((x * y) * z) / x) = y * (z * (x \ 1)) # label(568).  [para(1353(a,1),28(a,1,1)),rewrite(61(6),61(10),3163(9),5675(8),11(6),51(7))].
% 18418 x \ (y \ (x * (((x \ (y * x)) * z) * u))) = (z / (x \ (y \ x))) * (x \ (y \ (x * u))) # label(1268).  [para(3366(a,1),1353(a,1,1,2)),rewrite(2(2),3366(6),3366(14)),flip(a)].
% 18474 (x / (y \ 1)) * ((y \ (z * y)) / z) = y \ ((y * x) * ((z * y) / z)).  [para(11444(a,1),1353(a,1,2))].
% 18511 x \ ((x * x) * y) = y / (y \ (x \ y)) # label(893).  [back_rewrite(3489),rewrite(18418(7),17293(7))].
% 18538 (x / y) \ (x * (y \ x)) = y / ((y \ x) \ 1) # label(2733).  [para(28(a,1),18511(a,1,2)),rewrite(6(3),315(7))].
% 18573 (x \ ((x * x) * y)) / y = 1 / ((x \ y) / y) # label(2667).  [para(18511(a,2),698(a,2,1)),rewrite(3(4)),flip(a)].
% 18801 (x / (x / y)) / ((x / y) \ 1) = y / ((y \ x) \ 1) # label(3097).  [back_rewrite(13621),rewrite(18538(10))].
% 18838 (x \ (y * (z \ x))) / (z \ x) = z \ ((z / x) * y) # label(1283).  [para(1367(a,1),862(a,2)),rewrite(134(5),3(2))].
% 19240 ((1 / x) * y) \ ((1 / x) * z) = (y \ (z * x)) / x # label(3139).  [para(16(a,1),1414(a,1,2,1,2)),rewrite(1740(5)),flip(a)].
% 19248 (x * y) \ ((x * z) * x) = (y \ z) / (x \ 1) # label(459).  [para(74(a,1),1414(a,2,2)),rewrite(5675(7),1033(7),3(6)),flip(a)].
% 19297 (x / (x * y)) \ (x * z) = x * ((1 / y) \ z) # label(1542).  [para(985(a,1),1414(a,1,2,1)),rewrite(2551(8)),flip(a)].
% 19448 x \ ((x / y) \ (x * z)) = (1 / (x \ y)) \ z # label(284).  [para(1436(a,1),4(a,1,2))].
% 19452 ((x / y) / x) \ ((x / y) * z) = (x * (z * y)) / y # label(3340).  [para(16(a,1),1436(a,1,2,1,2)),rewrite(1164(5)),flip(a)].
% 19499 ((x \ (y * x)) / z) \ ((x \ (y * x)) * u) = x \ (y * ((x / (y \ (x * z))) \ (x * u))) # label(1297).  [para(1436(a,1),231(a,2)),rewrite(3366(4),1436(7)),flip(a)].
% 19839 (x \ (y * (z \ 1))) / (z \ 1) = (z * x) \ (z * y) # label(968).  [para(15(a,1),1740(a,1,1)),rewrite(1414(5)),flip(a)].
% 19842 (x / y) * ((x \ (z * y)) / y) = ((x / y) / x) * z # label(1302).  [para(1740(a,1),18(a,2,2)),rewrite(114(6),2(3),6(3)),flip(a)].
% 19872 (x \ 1) * (x \ ((y / x) \ z)) = x \ ((y \ (z * x)) / x) # label(1304).  [para(1740(a,1),215(a,1,2)),flip(a)].
% 19916 (1 / x) * ((y * x) / y) = (x \ (y * x)) / y # label(1315).  [para(1740(a,1),3690(a,2)),rewrite(2639(4),114(7),6(3),17463(7),5675(9),11(7),6(8))].
% 20681 ((x / (y * z)) / (y / ((z * y) / z))) * (y * z) = x / (y \ (z \ (y * z))).  [para(10188(a,1),2089(a,1,1,2)),rewrite(11790(12),11916(13))].
% 20783 (((1 / x) / y) * x) \ (x \ (y \ (x * y))) = y.  [para(2102(a,1),170(a,1,2)),rewrite(5(3),3366(8),231(7),12271(8),12919(9))].
% 21062 (x * y) / ((z * ((1 / y) * u)) * y) = (x / ((((1 / y) \ z) / y) * u)) * y.  [para(231(a,1),2196(a,1,1,2)),rewrite(7351(6),9985(6)),flip(a)].
% 21088 (x * y) / (z / (y \ u)) = (x / ((y * z) / u)) * y # label(1440).  [para(2065(a,1),2196(a,2,2)),rewrite(5732(6),11(4),114(4),3(3)),flip(a)].
% 21105 (x * y) / (z * (y \ (z \ y))) = (x / (y / ((z * y) / z))) * y.  [para(3690(a,1),2196(a,2,2)),rewrite(11263(5),10188(3)),flip(a)].
% 21229 (x / (y * (z \ (y \ z)))) / (y * ((z \ (y * z)) / y)) = (((x / z) / y) / (z / ((y * z) / y))) * z.  [back_rewrite(11551),rewrite(21105(16))].
% 21605 (x * (y * (z \ (y \ x)))) * (x \ 1) = (y * (z * (y \ (x \ 1)))) \ 1.  [para(18(a,1),3154(a,2,1)),rewrite(1514(3))].
% 21925 x \ (y * ((1 / y) * x)) = y * (x \ (x / y)) # label(3605).  [para(3398(a,1),3(a,1,2)),flip(a)].
% 21931 x \ ((y / x) \ (y * x)) = (y * (x \ 1)) \ y # label(1322).  [para(97(a,1),3398(a,2,2)),rewrite(15(9),3(7),5395(8),3163(8)),flip(a)].
% 21950 (x * ((1 / x) * y)) / (y / x) = (y * x) / y # label(3825).  [para(3398(a,1),264(a,1,2,2)),rewrite(3(7))].
% 22356 (1 / x) \ (((1 / x) * y) / z) = (y * x) / (z * x) # label(2425).  [para(16(a,1),4032(a,1,2)),rewrite(2196(5)),flip(a)].
% 22366 (x \ ((x * y) / z)) * (x \ z) = y * (z \ (x \ z)).  [para(4032(a,1),28(a,1,1)),rewrite(453(11),3(7))].
% 22963 (x / y) / ((y * z) / ((y * u) / y)) = (x / (z / (u * (y \ 1)))) / y.  [para(4057(a,1),3966(a,1,1,2)),rewrite(4067(11)),flip(a)].
% 22991 x \ ((y / (x \ 1)) / y) = (x \ (y / (x \ 1))) / y # label(3267).  [para(10188(a,1),4057(a,2)),rewrite(176(5),1(5),16278(12))].
% 23404 (x * (y * (z \ 1))) / (u * (z \ 1)) = z \ (((z * x) * y) / u).  [para(4935(a,1),4057(a,1,2,1,1)),rewrite(6(4)),flip(a)].
% 23422 (x * (y \ 1)) * (z * (y \ 1)) = (x * (y \ z)) * (y \ 1).  [para(51(a,1),4976(a,1,1)),rewrite(18(10),51(12))].
% 23473 (x \ y) * (((x * z) \ z) / z) = x \ ((y * (1 / z)) / x).  [para(923(a,2),4976(a,1,2))].
% 23483 (x * (y \ 1)) * (y * (x \ (y \ z))) = (y \ x) * (x \ z).  [para(4976(a,1),1768(a,1)),rewrite(8692(5),17551(6),14(5),17(4),4(5),41(10),1514(9)),flip(a)].
% 23588 (x \ y) * ((z * x) * (x \ y)) = ((1 / (x \ y)) \ z) * y # label(1380).  [para(1436(a,1),4976(a,1,2)),rewrite(2(7),16(6),21088(13),2(10),15849(12)),flip(a)].
% 23615 x \ (y \ (x * ((z / y) * x))) = (x \ (y \ (x * z))) * (y \ x) # label(1384).  [back_rewrite(3460),rewrite(23588(7),363(4),3366(3)),flip(a)].
% 23672 (((1 / x) / y) * x) \ (x \ z) = x \ ((x / (y * x)) \ z).  [para(774(a,1),5140(a,1,1))].
% 23858 x \ ((x / (y * x)) \ (y \ (x * y))) = y # label(2375).  [back_rewrite(20783),rewrite(23672(8))].
% 23886 (x / (y * x)) \ (y \ (x * y)) = x * y # label(2936).  [para(23858(a,1),3(a,1,2)),flip(a)].
% 24053 (x / ((x \ y) * x)) \ ((x \ y) \ y) = y # label(3014).  [para(3(a,1),23886(a,1,2,2)),rewrite(3(8))].
% 24058 (x \ (y * x)) / (y * x) = y / (x * y) # label(3015).  [para(23886(a,1),15(a,1,2))].
% 24525 ((x \ y) \ y) / y = x / ((x \ y) * x) # label(3033).  [para(24053(a,1),15(a,1,2))].
% 24655 (x / y) / (y * (x / y)) = (y \ x) / x # label(3027).  [para(6(a,1),24058(a,1,1,2)),rewrite(6(3)),flip(a)].
% 24821 x \ ((x * (x * y)) / y) = y / ((x \ 1) * y) # label(3257).  [para(24058(a,1),4057(a,2)),rewrite(134(6),11(6),41(5),6(4))].
% 25017 (x \ (y \ (x * y))) / y = ((1 / x) / y) * x # label(2221).  [para(5969(a,1),24525(a,1,1,1)),rewrite(3366(3),5969(11),6609(14),1147(8),3704(8),8385(10),22963(11),263(9),6350(8),13(5))].
% 25030 (x \ y) * (((x \ y) \ x) / x) = (((x \ y) \ y) / y) * (x \ y) # label(3080).  [para(24525(a,2),8692(a,1,1)),flip(a)].
% 25188 x / ((x / y) / (y \ 1)) = ((y \ x) / x) * y # label(3076).  [para(24655(a,1),774(a,2,1)),rewrite(29(3),207(4))].
% 26873 (x * (y \ (x \ (z * u)))) * (u \ 1) = u \ ((((x * y) / x) / u) \ z) # label(1390).  [para(1514(a,1),5681(a,1,1))].
% 27543 (x / ((y * x) / y)) / (y \ 1) = (x * y) / x # label(575).  [para(5971(a,1),20(a,1,1)),rewrite(3(7))].
% 27568 (x / y) / ((1 / y) * x) = x * (y \ (x \ y)) # label(1406).  [para(902(a,1),5971(a,2,2,1)),rewrite(16(8),1740(6),19842(5),3690(3),2308(9),32(9)),flip(a)].
% 27573 (x \ 1) \ (y * (x \ (y \ 1))) = x / ((y * x) / y).  [para(5971(a,1),205(a,1,1,1)),rewrite(10805(4),21605(7),5971(5),11343(5)),flip(a)].
% 27581 (x * (y \ (x \ y))) \ 1 = (y \ (x * y)) / x # label(1411).  [para(5971(a,1),340(a,2,2,1)),rewrite(17767(7),16(9),11444(8))].
% 27637 x * ((x \ y) / (z * (x \ (z \ 1)))) = (y / (x / ((z * x) / z))) * x.  [para(5971(a,1),8692(a,1,1,2)),flip(a)].
% 27660 (x * y) * ((y * x) \ y) = (x * y) / x # label(3082).  [para(5971(a,1),101(a,2,1)),rewrite(17684(7),2149(8))].
% 27669 (x * y) / (x * (y * (x \ (y \ x)))) = x * (y * (x \ (y / ((x * y) / x)))) # label(1187).  [para(5971(a,1),287(a,2,2)),rewrite(264(7),18(9),5830(10),264(12),18(12))].
% 27700 (1 / x) / ((y / x) / y) = (x \ (y * x)) / y # label(1460).  [para(1164(a,1),5971(a,1,2)),rewrite(1727(6),1(4),43(6),19916(5),114(11),2(8),6(8)),flip(a)].
% 27706 x \ ((x / ((y * x) / y)) * z) = (y * (x \ (y \ x))) * (x \ z) # label(1416).  [para(5971(a,1),1353(a,2,2,1)),rewrite(17767(7)),flip(a)].
% 27776 ((x \ (y * x)) / y) * (x \ (y * x)) = (x \ (y * x)) * (y \ (x \ (y * x))).  [back_rewrite(14834),rewrite(27581(5))].
% 27850 (x * y) \ ((x * y) / x) = (y * x) \ y # label(3036).  [para(27660(a,1),4(a,1,2))].
% 28105 ((x / (y \ 1)) \ 1) / ((y * x) \ y) = (x * y) \ x # label(1420).  [back_rewrite(4431),rewrite(27850(12))].
% 28114 ((x \ y) * x) \ (x \ y) = y \ (y / x) # label(3025).  [para(3(a,1),27850(a,1,1)),rewrite(3(2)),flip(a)].
% 28116 (x * (y / x)) \ x = y \ (y / (y / x)) # label(3044).  [para(6(a,1),27850(a,1,1)),rewrite(6(2)),flip(a)].
% 28270 ((x * (1 / y)) \ x) * y = x \ ((x * y) * y) # label(3215).  [para(27850(a,1),3631(a,1,1)),rewrite(265(11),287(11),28(10),1(10),3(9))].
% 28320 ((x \ y) * x) * (y \ (y / x)) = x \ y # label(3020).  [para(28114(a,1),3(a,1,2))].
% 28321 (x \ y) / (y \ (y / x)) = (x \ y) * x # label(2986).  [para(28114(a,1),15(a,1,2))].
% 28361 ((1 / x) \ (x \ y)) \ y = x * (y \ (y / x)) # label(3053).  [para(28114(a,1),1514(a,2,2)),rewrite(1032(4))].
% 29212 x / (x / ((x \ y) \ y)) = x * (((x \ y) \ y) / x).  [para(5987(a,1),113(a,1,2)),rewrite(2(2),10968(8))].
% 29940 x \ ((x * (y * (x \ (z \ (x * y))))) / y) = (x \ ((z * x) / y)) \ 1.  [para(7121(a,1),575(a,2,1)),rewrite(1731(8),23422(9),4062(11))].
% 30140 ((1 / x) * y) / (z / x) = (1 / x) * ((y * x) / z) # label(1500).  [para(862(a,1),7146(a,1,1))].
% 30285 (((1 / x) * y) * z) / (u / x) = (1 / x) * ((y * (z * x)) / u).  [para(1170(a,1),7146(a,1,1))].
% 30487 (x * ((x \ 1) / y)) \ (z / (x * y)) = (x \ ((x * y) * z)) / (x * y).  [para(8692(a,1),7429(a,1,1))].
% 30758 ((x / (y \ 1)) \ y) / ((x \ 1) / (y \ 1)) = x \ (x / y) # label(3406).  [para(8664(a,1),4407(a,2,1)),rewrite(4287(6),4287(12),114(13),3(9),30487(12),2(5),4(4),7121(6),1(2)),flip(a)].
% 30841 (x \ y) * (((x \ y) \ x) / z) = y / (z / ((x \ y) \ 1)) # label(3269).  [para(15(a,1),8845(a,1,2,1,2))].
% 31022 (((x \ y) \ y) / y) * (x \ y) = y / (x / ((x \ y) \ 1)) # label(3279).  [back_rewrite(25030),rewrite(30841(5)),flip(a)].
% 31037 (x \ 1) \ (y \ (x \ y)) = x * (y \ (x \ y)) # label(283).  [para(3(a,1),9012(a,1,2,1)),rewrite(3(7))].
% 33070 (1 / x) \ (y / ((z * x) / z)) = (x * (y * z)) / (z * x).  [para(4067(a,1),11263(a,1,2))].
% 33295 1 / ((x \ (y * x)) / y) = y * (x \ (y \ x)) # label(1453).  [para(902(a,1),11341(a,2,2,1)),rewrite(114(9),2(6),6(6),27700(6),2308(11),32(11),27568(10))].
% 33337 (x / (y / ((z * y) / z))) / (z / ((y * z) / y)) = (y / ((z * y) / z)) * ((z / ((y * z) / y)) * x) # label(1658).  [para(11341(a,1),2308(a,1,2)),rewrite(11343(16))].
% 33705 ((x \ (y * x)) / y) \ 1 = y * (x \ (y \ x)) # label(832).  [para(902(a,1),11343(a,2,2,1)),rewrite(114(8),2(5),6(5),27700(5),2308(11),32(11),27568(10))].
% 33784 (x / ((y * x) / y)) * ((z * (x / ((y * x) / y))) * (y / ((x * y) / x))) = (y / ((x * y) / x)) \ z # label(1669).  [para(11343(a,1),1070(a,1,2,2)),rewrite(11341(17),2(18))].
% 33956 (x \ 1) / (y \ (x \ y)) = x \ (y \ (x * y)) # label(416).  [para(11593(a,1),86(a,1,2,1)),rewrite(27776(8),4(9),3366(9),2(7)),flip(a)].
% 34099 (x * (y \ 1)) / ((z \ (y * z)) / y) = x * (z \ (y \ z)).  [para(11593(a,1),2196(a,2,2)),rewrite(15(4),4032(7),774(4),215(5),22366(5)),flip(a)].
% 34103 (x * (y \ 1)) \ (y \ x) = y * (x \ (y \ x)) # label(466).  [para(11593(a,1),3154(a,2,1)),rewrite(3366(3),26873(7),5131(5),33705(10))].
% 34150 (x \ y) / ((z \ (x * z)) / x) = (x \ ((y * x) / z)) * (x \ z).  [para(11593(a,1),7121(a,1,2)),rewrite(774(9),4067(8),4140(10))].
% 34486 (x * (y \ 1)) / (y \ x) = x * (y \ (x \ y)) # label(508).  [para(61(a,1),11878(a,2,1,2)),rewrite(3163(8),647(8),134(9),3154(8),11(9),11568(8),33295(5),3163(8),5675(7),11(5),51(6)),flip(a)].
% 34489 ((((x * (y \ (x \ y))) \ (z * x)) / y) / x) * y = (((y \ (x * y)) / x) * z) * (x * (y \ (x \ y))).  [para(11878(a,1),28(a,1,1,1)),rewrite(8323(17),1(18)),flip(a)].
% 34497 (x * (y \ (z * y))) / (x * z) = x / (x * (z * (y \ (z \ y)))) # label(2341).  [para(11878(a,1),114(a,1,1,2)),rewrite(114(5),2(7))].
% 34518 (x * (y \ (x \ y))) * ((y \ (x * y)) / x) = 1 # label(1684).  [para(11878(a,1),647(a,1,2,1)),rewrite(33705(8),12(7),11(6),27581(9)),flip(a)].
% 34762 (x * (y \ (x \ y))) \ (z * (x * (y \ (x \ y)))) = (((y \ (x * y)) / x) * z) * (x * (y \ (x \ y))).  [back_rewrite(8323),rewrite(34489(16))].
% 34852 (x * (y \ (z \ (y * z)))) / x = x / (x * (z \ (y \ (z * y)))) # label(1540).  [para(11916(a,1),114(a,1,1,2)),rewrite(2(7))].
% 34897 (x \ (y \ (x * y))) \ (z / (y \ (x \ (y * x)))) = (y \ (x \ (y * x))) * (z * (x \ (y \ (x * y)))) # label(485).  [para(11916(a,1),3023(a,1,2,2)),rewrite(11946(13))].
% 34912 ((x \ (y \ (x * y))) * z) / (x \ (y \ (x * y))) = (x \ (y \ (x * y))) * (z * (y \ (x \ (y * x)))) # label(524).  [para(11916(a,1),5675(a,1,1)),rewrite(34897(8),11(13)),flip(a)].
% 35238 (x \ (y \ (x * y))) * ((z * (x \ (y \ (x * y)))) * (y \ (x \ (y * x)))) = (y \ (x \ (y * x))) \ z # label(543).  [para(11946(a,1),1070(a,1,2,2)),rewrite(11916(17),2(18))].
% 36070 (x / ((y * x) / y)) / ((x * y) / x) = ((x * y) / x) / (((x / y) / x) \ y).  [para(14300(a,1),97(a,1,1)),rewrite(644(7),5256(14),644(10))].
% 36122 ((x / ((y / z) / y)) / ((z \ (y * z)) / y)) * ((y / z) / y) = x / (y / ((z * y) / z)) # label(1666).  [para(14300(a,1),2065(a,2,2)),rewrite(27700(8))].
% 36231 ((x * y) / x) / (((x / y) / x) \ y) = (x / ((y * x) / y)) * ((x / y) / x).  [para(14300(a,1),28321(a,1,1)),rewrite(27700(10),6121(9),36070(6),14300(11))].
% 36282 (x / ((y * x) / y)) / ((x * y) / x) = (x / ((y * x) / y)) * ((x / y) / x).  [back_rewrite(36070),rewrite(36231(12))].
% 36511 (x * ((y \ z) / u)) / y = (x / y) * (z / (y * u)).  [para(15651(a,1),1161(a,1,2,1)),rewrite(16(7),16(8)),flip(a)].
% 36548 ((x \ y) / z) \ (x \ u) = x \ ((y / (x * z)) \ u) # label(781).  [para(15651(a,1),5150(a,1,2,1,1)),rewrite(16(6),16(8)),flip(a)].
% 37393 x * ((x \ y) * ((y \ (z * x)) * (y \ (x \ y)))) = (z / (y / x)) * ((1 / x) * y).  [para(17140(a,1),32(a,1,2,2)),rewrite(1733(7),17(8))].
% 37446 ((x / (y / z)) / ((z \ (y * z)) / y)) * (y / z) = x / (z * (y \ (z \ y))) # label(1622).  [para(17140(a,1),2065(a,2,2)),rewrite(30140(7),19916(7))].
% 37523 (x * (y * (z \ (y \ z)))) * (y / z) = (x * (y / z)) * ((y \ (z * y)) / z) # label(1625).  [para(17140(a,1),401(a,1,2,2)),rewrite(11878(7),27568(11)),flip(a)].
% 37934 (x * x) / ((y \ (z \ (y * z))) * x) = (1 / x) \ (z \ (y \ (z * y))).  [para(11916(a,1),18132(a,2,2)),rewrite(1(2))].
% 37987 (x \ y) \ (z * (u * (x \ 1))) = (y \ ((x * z) * u)) * (x \ 1).  [para(18349(a,1),3163(a,1,2)),rewrite(5675(11),51(12))].
% 38669 (x * y) \ (x * (y * x)) = 1 / ((y * x) \ y) # label(3038).  [para(340(a,2),18573(a,2,2,1)),rewrite(18838(8),17(5),4(3),28105(13))].
% 38841 (x \ (y \ z)) / (y \ 1) = (y * x) \ (z * y) # label(580).  [para(3(a,1),19248(a,1,2,1)),flip(a)].
% 39277 ((x * y) / z) \ (x * u) = x * ((y / (x \ z)) \ u) # label(890).  [para(4033(a,1),19297(a,1,1,2)),rewrite(15(4),15(10))].
% 39312 (x / y) \ ((y \ x) * z) = y * (((y \ x) \ x) \ z) # label(1582).  [para(5987(a,1),19297(a,1,1,2)),rewrite(29212(4),10971(6),4(4),15(10))].
% 39707 ((x * (y * z)) / (z * x)) * ((z * x) / z) = z * (x * (z \ (((x \ (z * x)) / z) \ y))).  [para(19916(a,1),1768(a,2,2,1)),rewrite(33070(6),18(14))].
% 39910 (x \ 1) * (y \ (y / (x \ 1))) = y \ ((x \ 1) * (x * y)) # label(4014).  [para(15(a,1),21925(a,1,2,2,1)),flip(a)].
% 40116 x \ (((y / x) \ (y * x)) / x) = ((y * (x \ 1)) \ y) * (x \ 1).  [para(21931(a,1),61(a,1,1)),flip(a)].
% 40672 ((x * y) / x) / (x / ((y * x) / y)) = x * (y * (x \ (y / ((x * y) / x)))).  [para(19916(a,1),21950(a,1,1,2)),rewrite(10808(4),4067(5),18(9),5820(12),27669(12))].
% 41472 x \ (((x * (x * y)) / y) / x) = (x \ 1) * (((x \ 1) \ y) / y).  [para(24821(a,1),61(a,1,1)),rewrite(8692(7)),flip(a)].
% 41816 ((x \ (y \ (x * y))) * (z * y)) / y = (((1 / x) / y) * x) * ((1 / y) \ z).  [para(25017(a,1),1164(a,1,1)),flip(a)].
% 41916 x / (y / ((y \ x) \ 1)) = (y / x) * (x / y) # label(3620).  [para(16(a,1),25188(a,2,1,1)),rewrite(18801(6))].
% 42128 (((x \ y) \ y) / y) * (x \ y) = (x / y) * (y / x) # label(3627).  [back_rewrite(31022),rewrite(41916(10))].
% 42639 (x * x) * ((x \ (y * x)) / y) = x * ((y * x) / y).  [para(27543(a,1),74(a,1,2)),rewrite(4069(8),11444(7)),flip(a)].
% 42853 (((x \ 1) \ (y / ((x * y) / x))) * (x \ 1)) * x = (x \ 1) \ (y / ((x * y) / x)).  [para(27543(a,1),28320(a,1,2,2)),rewrite(4066(15))].
% 42856 ((x \ 1) \ (y / ((x * y) / x))) * (x \ 1) = (x * (y / ((x * y) / x))) * (1 / x).  [para(27543(a,1),28321(a,1,2,2)),rewrite(4066(12),3092(7)),flip(a)].
% 42860 ((x * y) * x) / ((z * x) / z) = x * (y / (z / ((x * z) / x))).  [para(27543(a,1),7146(a,1,2)),rewrite(1743(6),11(4),15(9))].
% 42906 (x \ 1) \ (y / ((x * y) / x)) = (x * ((y * x) / y)) * (x \ 1).  [back_rewrite(42853),rewrite(42856(9),29(8),4069(5),11444(4),42639(5)),flip(a)].
% 42985 ((x / ((1 / y) * z)) / (z * (y \ (z \ y)))) * ((1 / y) * z) = x / ((z \ (y * z)) / y).  [para(27568(a,1),2065(a,1,1,2)),rewrite(7429(17))].
% 43117 (x / ((1 / y) * z)) / (z * (y \ (z \ y))) = x / (z / y).  [para(27568(a,1),9750(a,2,2)),rewrite(30285(11),9860(12),16(6),3046(7),9750(6),5(2)),flip(a)].
% 43176 (x / (y / z)) * ((1 / z) * y) = x / ((y \ (z * y)) / z).  [back_rewrite(42985),rewrite(43117(8))].
% 43199 x * ((x \ y) * ((y \ (z * x)) * (y \ (x \ y)))) = z / ((y \ (x * y)) / x).  [back_rewrite(37393),rewrite(43176(14))].
% 43240 ((((x \ (y * x)) / y) * z) * (y * (x \ (y \ x)))) * ((x \ (y * x)) / y) = (y * (x \ (y \ x))) \ z.  [para(27581(a,1),1347(a,1,2)),rewrite(34762(8),2(17))].
% 43855 (((1 / x) \ y) / y) * x = (x * (x * y)) / y # label(3218).  [para(7429(a,1),28270(a,1,1)),rewrite(2(4),18339(12))].
% 43923 (x \ ((x \ 1) \ y)) \ y = y \ ((x \ 1) * (x * y)) # label(4015).  [para(15(a,1),28361(a,1,1,1)),rewrite(39910(12))].
% 43928 (x \ y) \ ((x \ 1) * y) = x \ ((y * (1 / x)) \ y) # label(1752).  [para(97(a,1),28361(a,2,2,2)),rewrite(15(4),3163(4),1072(4),3163(7),1147(5),5(2),3163(11),21931(11),3371(12)),flip(a)].
% 44096 (x / y) * ((y * (x / y)) \ y) = ((1 / (x / y)) \ y) \ x.  [para(28116(a,2),28361(a,2,2)),rewrite(16(5)),flip(a)].
% 44164 ((x / y) \ 1) / ((x \ y) / y) = (x * (1 / y)) \ x.  [back_rewrite(4382),rewrite(43928(11),3(12))].
% 44936 ((x * y) * (x \ 1)) * (x * (z \ (x \ z))) = (x \ 1) \ (y * (z \ (x \ z))).  [para(31037(a,1),1347(a,1,2)),rewrite(134(6),11(6))].
% 46400 (x * y) / (z \ (y \ (z * y))) = y * ((y \ x) / (z \ (y \ z))).  [para(33705(a,1),805(a,1,1,2)),rewrite(8692(5),3366(9)),flip(a)].
% 47229 ((x \ (y * x)) / y) * ((y * (x \ 1)) * z) = (y * (x \ 1)) * ((x * (y \ (x \ y))) * z).  [para(34103(a,1),17(a,2,2,1)),rewrite(7121(5),11444(3))].
% 47239 (x * (y \ 1)) * ((y * (x \ (y \ x))) * ((x * (y \ 1)) \ z)) = ((y \ (x * y)) / x) * z # label(1820).  [para(34103(a,1),32(a,1,2,1)),rewrite(7121(17),11444(15))].
% 47377 (x * (y \ (x \ y))) \ ((x * (y \ 1)) * z) = (x * (y \ 1)) * (((x \ (y * x)) / y) \ z).  [para(34103(a,1),1436(a,1,2,1,2)),rewrite(11878(8),34486(13)),flip(a)].
% 48854 ((x \ y) * x) \ ((x \ y) * y) = 1 / (y \ x) # label(3599).  [para(3(a,1),38669(a,1,2,2)),rewrite(3(8))].
% 49315 x \ ((x * (y \ (x \ z))) * u) = ((x * y) \ (z * x)) * (x \ u).  [para(38841(a,1),1164(a,1,1)),rewrite(15(7),1389(14)),flip(a)].
% 49321 (x * (y \ (x \ z))) \ (x * u) = x * (((x * y) \ (z * x)) \ u).  [para(38841(a,1),1414(a,1,2,1)),flip(a)].
% 51708 (x \ 1) * (((x \ 1) \ y) / y) = ((y * x) * (x \ 1)) / y # label(1911).  [para(263(a,1),41916(a,2,1)),rewrite(4(7),21088(9),14(5),8692(7),3046(14))].
% 51894 x \ (((x * (x * y)) / y) / x) = ((y * x) * (x \ 1)) / y.  [back_rewrite(41472),rewrite(51708(12))].
% 52106 ((x * (x * y)) / y) / x = ((1 / x) \ y) / y # label(3245).  [para(43855(a,1),5(a,1,1))].
% 52298 x \ (((1 / x) \ y) / y) = ((y * x) * (x \ 1)) / y # label(1916).  [back_rewrite(51894),rewrite(52106(4))].
% 53852 (x \ y) * (((x \ y) \ 1) * x) = (1 / (y / x)) * y # label(2342).  [para(658(a,1),44(a,1,2,2)),rewrite(1727(5),1(3),17(4),579(4),2348(12)),flip(a)].
% 54201 x \ ((x * y) * ((z * x) / z)) = y / (z * (x \ (z \ 1))).  [para(66(a,2),4067(a,2,2,1)),rewrite(1389(7),7121(7),4926(4),7121(13),6(9),4067(8),15161(9))].
% 54431 (x / (y \ 1)) * ((y \ (z * y)) / z) = x / (z * (y \ (z \ 1))).  [back_rewrite(18474),rewrite(54201(12))].
% 55984 (x * (y \ z)) / (x * (y \ u)) = x / (x * (y \ ((z / u) \ y))).  [para(5256(a,1),379(a,1,1,2)),rewrite(114(5))].
% 56216 x * ((y / ((x \ (z * x)) / z)) * (x \ u)) = ((x * y) / ((z * x) / z)) * u.  [para(10808(a,1),439(a,1,1,2)),flip(a)].
% 56298 (x / (x * (y \ (z \ (y * z))))) * u = x * ((z \ (y \ (z * y))) * (x \ u)).  [para(11916(a,1),439(a,2,2,1)),rewrite(2(2))].
% 58373 ((x \ y) * (z / ((x * z) / x))) / (x \ 1) = x \ (y * ((z * x) / z)).  [para(27543(a,1),1078(a,1,2,2)),rewrite(15(4),15(8)),flip(a)].
% 58385 ((x \ y) * (z \ (x \ u))) / (x \ 1) = x \ (y * ((x * z) \ (u * x))).  [para(38841(a,1),1078(a,1,2,2)),rewrite(15(4),15(9)),flip(a)].
% 58705 ((x / (y * (z * (y \ (z / ((y * z) / y)))))) * z) * ((z \ (y * z)) / y) = x * (y / ((z * y) / z)).  [para(11444(a,1),1220(a,1,2)),rewrite(4067(5),40672(6),4067(15))].
% 58749 ((x / ((y / ((z * y) / z)) * ((y / z) / y))) * ((y * z) / y)) * (z \ 1) = x * ((y * z) / y).  [para(27543(a,1),1220(a,1,1,1,2,2)),rewrite(36282(6),42906(16),23422(17),4(11),27543(19))].
% 58871 ((x \ (y \ (x * y))) * x) * (x \ z) = x \ ((y \ (x * y)) * z) # label(220).  [para(5(a,1),1485(a,1,2,1)),rewrite(3366(4),231(3),3366(8),231(7),12271(8)),flip(a)].
% 60421 ((x / (y \ 1)) * z) * ((y * z) \ u) = (y \ ((y * x) * (u / z))) * z.  [para(1353(a,1),1769(a,1,1)),flip(a)].
% 60927 ((x \ y) / y) \ (1 / ((1 / (x \ y)) \ x)) = ((x \ y) \ y) / y # label(2159).  [para(2537(a,1),2542(a,2,2)),rewrite(16(5),16(6)),flip(a)].
% 61519 (x * (y \ x)) * ((y \ x) \ 1) = y * ((x \ y) \ 1).  [para(575(a,1),2774(a,1,1,2)),rewrite(575(7),25(10),2774(6),4(9)),flip(a)].
% 62404 (x \ y) * ((y \ z) * (y \ (x \ y))) = (x \ (z / y)) * (x \ y).  [para(215(a,1),3594(a,1,2))].
% 62523 x / ((y \ (z * y)) / z) = (x / ((z * y) / z)) * y.  [back_rewrite(43199),rewrite(62404(7),32(6),4067(3)),flip(a)].
% 62541 ((x * (y * z)) / (z * x)) * u = ((x * y) / ((z * x) / z)) * u.  [back_rewrite(56216),rewrite(62523(4),1070(7),33070(6))].
% 62593 (((x / (y / z)) / ((y * z) / y)) * z) * (y / z) = x / (z * (y \ (z \ y))).  [back_rewrite(37446),rewrite(62523(6))].
% 62600 (((x / ((y / z) / y)) / ((y * z) / y)) * z) * ((y / z) / y) = x / (y / ((z * y) / z)).  [back_rewrite(36122),rewrite(62523(7))].
% 62607 ((x \ y) / ((x * z) / x)) * z = (x \ ((y * x) / z)) * (x \ z).  [back_rewrite(34150),rewrite(62523(5))].
% 62610 ((x * (y \ 1)) / ((y * z) / y)) * z = x * (z \ (y \ z)).  [back_rewrite(34099),rewrite(62523(7))].
% 62621 (x / y) / (z / ((y * z) / y)) = x / ((z * y) / z) # label(2855).  [back_rewrite(11530),rewrite(62523(4),5(5)),flip(a)].
% 62622 x * (y * (x \ (((y \ (x * y)) / x) \ z))) = y * z.  [back_rewrite(39707),rewrite(62541(7),6(7)),flip(a)].
% 62644 (x / (y * (z \ (y \ z)))) / (y * ((z \ (y * z)) / y)) = x / y.  [back_rewrite(21229),rewrite(62621(15),6350(13),6(12))].
% 63830 x * (((y \ (z * y)) / z) \ u) = x * (z * (y \ (z \ (y * u)))).  [para(34518(a,1),3886(a,2,1,1)),rewrite(62523(10),5918(11),5735(9),5675(7),379(7),114(9),439(10),15418(9),231(11),3446(12),19499(13),774(3),3690(3),49321(11),11790(3),5168(10),62622(12),4(7),11(7)),flip(a)].
% 63865 (x * (y \ (x \ y))) \ ((x * (y \ 1)) * z) = (y \ x) * z.  [back_rewrite(47377),rewrite(63830(16),23483(16),4(11))].
% 65123 x * (y \ ((y * (x \ z)) / (x \ u))) = (z / (y \ u)) * (y \ x).  [para(263(a,1),5715(a,2,1,2,1)),rewrite(231(9),23404(10),774(5),5(3),9785(4),1514(7),9860(12),4032(11)),flip(a)].
% 65233 ((x / (((1 / y) / z) \ u)) * z) * y = ((x * z) * y) / ((u * z) * y).  [para(5715(a,1),2196(a,1,1))].
% 65338 (x * (y * (x \ (z \ (u * v))))) / v = (((x * y) / x) / v) * ((z / v) \ u).  [para(18(a,1),5720(a,1,1))].
% 65402 (x * (y \ (z \ (y * (u * v))))) / v = (x / v) * (((y \ (z * y)) / v) \ u).  [para(3366(a,1),5720(a,1,1,2))].
% 65569 (x * (y \ (x \ y))) * (y \ ((z / x) \ y)) = (y \ ((z * y) / x)) \ 1.  [back_rewrite(29940),rewrite(65338(6),4067(3),27706(7))].
% 66528 (x \ y) \ ((y \ x) \ 1) = y \ (x * ((y \ x) \ 1)) # label(2169).  [para(687(a,1),6169(a,2,2)),rewrite(3(2),3163(12),1072(11),2774(11))].
% 67047 ((x \ (y * x)) * (y \ x)) / z = (x \ (y * x)) / ((x / z) \ y) # label(2176).  [para(1347(a,1),6583(a,1,2,1,2)),rewrite(5720(6),13(3),1(6),774(11),5(9),780(9)),flip(a)].
% 67289 ((x / ((y * z) / y)) * z) * ((z \ (y * z)) / y) = x.  [para(11878(a,1),6627(a,1,1,2)),rewrite(27581(9),62523(8),17383(7),4069(8),11444(7),11878(14),62523(13),698(12),3690(11),6(16))].
% 67735 ((x * y) * z) / ((x * z) / x) = x * (y * (z / ((x * z) / x))).  [para(7092(a,1),4935(a,2)),rewrite(18(5),5971(5)),flip(a)].
% 67741 (x * (y \ (x \ z))) / (y / ((x * y) / x)) = x * (y \ (x \ ((z * x) / ((y * x) / y)))).  [para(7092(a,1),7121(a,2,2)),rewrite(1514(3),1514(7),5971(8),1514(14))].
% 69216 ((1 / x) \ (y \ (z \ (y * z)))) / x = x / ((1 / x) \ (z \ (y \ (z * y)))).  [para(11946(a,1),7252(a,2,2,2)),rewrite(2(7))].
% 69918 (x * ((y \ x) \ z)) / y = ((y * z) / x) * (x / y).  [para(227(a,1),8697(a,1,2,1)),rewrite(3046(6))].
% 71619 ((x * y) / x) / (y / x) = y / ((1 / x) * y) # label(3496).  [para(43855(a,1),9860(a,2,2)),rewrite(6(7),2(6),9750(10)),flip(a)].
% 71714 (x \ y) / ((1 / y) * (x \ y)) = (x * (1 / y)) \ x.  [para(575(a,1),71619(a,1,1)),rewrite(44164(6)),flip(a)].
% 71739 (((x * y) \ y) / y) / (x / (x * y)) = (x \ (1 / y)) / (1 / y).  [para(985(a,1),71619(a,1,2)),rewrite(23473(6),1(4),97(7),6(4),15(13),2551(13)),flip(a)].
% 71890 (x * (y \ 1)) / ((y * x) / y) = (y \ x) / x # label(2982).  [para(1389(a,1),71619(a,1,1)),rewrite(3(3),1(2),5(7),15(9),41(9)),flip(a)].
% 72214 (x \ y) * (y \ (x * y)) = (y * (x \ 1)) * x # label(3966).  [para(71890(a,1),195(a,1,1,1)),rewrite(4(5),28(4))].
% 72223 ((x * (y \ 1)) * y) / x = ((y \ x) / x) * y # label(3594).  [para(71890(a,1),775(a,2,1)),rewrite(4(6))].
% 72479 ((x * (y \ 1)) * y) \ (y \ x) = (x \ 1) / (x \ y) # label(2208).  [para(72214(a,1),27850(a,2,1)),rewrite(774(11),67047(9),13(7),11(8),3579(10),23615(8),10808(4),51(3),4(4),32(5),5256(4)),flip(a)].
% 72531 (x * ((y * (x \ 1)) * x)) / y = y / ((1 / x) * y).  [para(72214(a,1),4955(a,1,1,2)),rewrite(3(9),71619(10))].
% 73715 ((x \ (y * x)) / y) \ z = y * (x \ (y \ (x * z))) # label(2375).  [para(10188(a,1),9925(a,1,2,1)),rewrite(6604(5),11444(3),63830(5),4(6)),flip(a)].
% 74358 (x / ((y * z) / y)) * z = x * (y * (z \ (y \ z))) # label(592).  [para(11572(a,1),195(a,1,1,1,2)),rewrite(9860(9),62523(5),62607(5),14463(8),61(6),4067(3),32(7),5969(9),8(8),6(5))].
% 74367 x * ((x \ y) * (z \ (x \ z))) = ((y / z) / x) * z # label(2152).  [para(11572(a,1),2065(a,1,1,2)),rewrite(62644(9),17(5),5969(9),774(8))].
% 74441 (x * (y * (z \ (y \ z)))) * ((z \ (y * z)) / y) = x # label(2511).  [back_rewrite(67289),rewrite(74358(4))].
% 74450 (x * (y \ 1)) * (y * (z \ (y \ z))) = x * (z \ (y \ z)).  [back_rewrite(62610),rewrite(74358(7))].
% 74459 x / (y / ((z * y) / z)) = x * (z / ((y * z) / y)) # label(1769).  [back_rewrite(62600),rewrite(74358(7),5889(7),176(10),644(4)),flip(a)].
% 74462 x / (y * (z \ (y \ z))) = x * ((z \ (y * z)) / y) # label(1968).  [back_rewrite(62593),rewrite(74358(6),37523(8),6(4)),flip(a)].
% 74483 x / ((y \ (z * y)) / z) = x * (z * (y \ (z \ y))) # label(1761).  [back_rewrite(62523),rewrite(74358(8))].
% 74510 (x * (y \ (x \ y))) \ z = ((y \ (x * y)) / x) * z # label(1776).  [back_rewrite(43240),rewrite(74441(12)),flip(a)].
% 74518 (x \ 1) \ (y * (z \ (x \ z))) = (x * y) * (z \ (x \ z)).  [back_rewrite(44936),rewrite(74450(8)),flip(a)].
% 74540 (x * (y \ (x \ z))) * (x / ((y * x) / y)) = x * (y \ (x \ ((z * x) / ((y * x) / y)))).  [back_rewrite(67741),rewrite(74459(7))].
% 74556 ((x * y) * x) / ((z * x) / z) = x * (y * (x / ((z * x) / z))).  [back_rewrite(42860),rewrite(74459(9))].
% 74566 (x * (y / ((z * y) / z))) * (z / ((y * z) / y)) = (z / ((y * z) / y)) * ((y / ((z * y) / z)) * x) # label(1782).  [back_rewrite(33337),rewrite(74459(4),74459(8))].
% 74571 x * ((x \ y) / (z * (x \ (z \ 1)))) = (y * x) * ((x \ (z * x)) / z).  [back_rewrite(27637),rewrite(74459(11),4069(12),11444(11))].
% 74574 x / (y \ (z \ (y * z))) = x * (z \ (y \ (z * y))) # label(559).  [back_rewrite(20681),rewrite(74459(6),11913(8),6(4)),flip(a)].
% 74651 (x * (y \ 1)) * ((y * (x \ (y \ x))) * z) = (y \ x) * z # label(1939).  [back_rewrite(63865),rewrite(74510(8),47229(8))].
% 74711 (x / ((y * x) / y)) * ((y / ((x * y) / x)) * ((x / ((y * x) / y)) * z)) = (y / ((x * y) / x)) \ z # label(1796).  [back_rewrite(33784),rewrite(74566(11))].
% 74724 (x * y) * (y \ (z \ (y * z))) = y * ((y \ x) / (z \ (y \ z))).  [back_rewrite(46400),rewrite(74574(5))].
% 74731 ((x \ (y \ (x * y))) * z) * (y \ (x \ (y * x))) = (x \ (y \ (x * y))) * (z * (y \ (x \ (y * x)))) # label(569).  [back_rewrite(34912),rewrite(74574(8))].
% 74758 (x \ y) * ((y * (x \ 1)) \ z) = ((x \ (y * x)) / y) * z # label(1941).  [back_rewrite(47239),rewrite(74651(12))].
% 74934 ((x \ (y \ (x * y))) * x) \ z = x \ (y \ ((x \ (y * x)) * z)).  [para(12271(a,1),3366(a,1,1)),rewrite(3366(9),231(8))].
% 75215 (x / ((y * x) / y)) * ((y / ((x * y) / x)) * z) = z # label(1802).  [para(11343(a,1),14811(a,1,1,2)),rewrite(11343(10),11(9),74459(8),74566(8),2(17),4(16))].
% 75216 (x * (y \ (z \ (y * z)))) * (z \ (y \ (z * y))) = x # label(614).  [para(11946(a,1),14811(a,1,1,2)),rewrite(11946(10),11(9),74574(8),2(17),4(16))].
% 75253 (x / ((y * x) / y)) \ z = (y / ((x * y) / x)) * z # label(1804).  [back_rewrite(74711),rewrite(75215(11)),flip(a)].
% 75254 (x * (y / ((z * y) / z))) * (z / ((y * z) / y)) = x.  [back_rewrite(74566),rewrite(75215(16))].
% 75255 (x \ (y \ (x * y))) \ z = (y \ (x \ (y * x))) * z # label(564).  [back_rewrite(35238),rewrite(75216(11)),flip(a)].
% 75407 ((x * y) * (y \ 1)) / x = y * ((y \ x) / x) # label(2108).  [para(14821(a,1),72223(a,1)),rewrite(2020(6),41(5),1032(3),52298(5),42128(14),15(7))].
% 75426 x \ (((1 / x) \ y) / y) = x * ((x \ y) / y) # label(2112).  [back_rewrite(52298),rewrite(75407(10))].
% 75431 (x \ 1) * (((x \ 1) \ y) / y) = x * ((x \ y) / y).  [back_rewrite(51708),rewrite(75407(12))].
% 75439 (x * (y \ 1)) / (x / y) = ((y \ x) / x) * y # label(3694).  [para(6(a,1),75407(a,1,1,1)),rewrite(8845(10),25188(10))].
% 75446 (x * (((x \ 1) * y) * (y \ 1))) * x = y * ((y \ 1) * x).  [para(75407(a,1),74(a,1,2)),rewrite(38841(6),1(3),14888(4)),flip(a)].
% 75448 x \ (y * ((y \ 1) * x)) = y * ((x * y) \ x) # label(2273).  [para(75407(a,1),86(a,2)),rewrite(75446(8),38841(11),1(8))].
% 75558 (x \ y) * (x / ((x \ y) * x)) = (y / x) * (x / y).  [para(24525(a,1),75407(a,2,2)),rewrite(61519(6),69918(5),2(2)),flip(a)].
% 75566 x \ (y / ((1 / x) * y)) = ((x \ y) / y) * x # label(4037).  [para(7121(a,1),75407(a,2,2)),rewrite(4062(11),72531(6),72223(10),5256(9),17714(9),8845(10),25188(10))].
% 75570 ((x * (y \ 1)) \ x) * (y \ 1) = y * (x \ (x / y)) # label(3745).  [para(8664(a,1),75407(a,2,2,1)),rewrite(28(9),3(7),75439(13),38841(8),1(5),30758(17))].
% 75672 x \ (((y / x) \ (y * x)) / x) = x * (y \ (y / x)) # label(2250).  [back_rewrite(40116),rewrite(75570(12))].
% 75723 (x \ 1) \ ((x \ y) / y) = x * ((x \ y) / y) # label(1894).  [para(15(a,1),75426(a,1,2,1,1)),rewrite(75431(12))].
% 75807 (x \ y) * (((x \ y) \ y) / y) = (y / x) * (x / y) # label(3964).  [para(24525(a,1),75426(a,2,2)),rewrite(75426(7),75558(10))].
% 76240 (x \ y) \ ((1 / x) * y) = x * (y \ (y / x)) # label(3667).  [para(61(a,1),75448(a,2,2,1)),rewrite(39(10),32(6),3163(11),19872(12),75672(10))].
% 76250 (1 / (x \ y)) * (((x / y) * x) \ x) = (x \ y) * (y \ x).  [para(400(a,1),75448(a,2,2,1)),rewrite(16(8),17(6),53852(6),14882(5)),flip(a)].
% 76263 ((1 / (x / y)) \ y) \ x = (y \ x) * (x \ y) # label(3601).  [para(75448(a,1),215(a,1)),rewrite(44096(5),1727(10),1(8),4(9))].
% 76312 (x / y) * ((x * (x / y)) \ x) = (x \ y) * (y \ x) # label(3995).  [para(75448(a,1),1367(a,2)),rewrite(453(8),76250(7)),flip(a)].
% 76472 x \ ((y \ 1) * (y * x)) = ((x * y) \ x) * y # label(4024).  [para(340(a,2),75566(a,2,1,1)),rewrite(71714(8),5097(6),43923(5),4(7),28105(13))].
% 76598 (x \ ((x \ 1) \ y)) \ y = ((y * x) \ y) * x # label(4023).  [back_rewrite(43923),rewrite(76472(10))].
% 76843 ((x \ y) \ 1) \ (y \ x) = (x \ y) * (y \ x) # label(4091).  [para(1743(a,1),75723(a,1,2)),rewrite(3(6),1(5),3163(10),647(10),5(13))].
% 77400 ((1 / x) * y) / (x * (y \ (y / x))) = x \ y # label(3671).  [para(76240(a,1),15(a,1,2))].
% 78520 ((1 / x) * (x / y)) / ((y / x) * (x / y)) = (y \ x) / x # label(2300).  [para(4407(a,1),77400(a,2)),rewrite(2671(6),4407(12),16(7))].
% 78571 (x \ y) \ ((x \ y) / y) = (y \ x) / x # label(3933).  [para(2537(a,1),77400(a,1,2,2,2)),rewrite(4633(6),60927(14),75807(9),78520(8)),flip(a)].
% 78805 (x \ (1 / y)) / (1 / y) = (y * x) \ y # label(3909).  [para(2554(a,1),78571(a,2,1)),rewrite(16(3),16(4),27850(4),71739(8)),flip(a)].
% 78984 ((x \ y) * (y \ x)) \ (x \ y) = 1 / (y \ x) # label(4152).  [para(76843(a,1),78571(a,1,1)),rewrite(76843(8),5(8),66528(10),19839(14),48854(10))].
% 81357 x * (((y * x) \ y) * x) = y \ (y / (1 / x)) # label(3959).  [para(78805(a,1),24655(a,1,1)),rewrite(78805(10),71714(8),5097(6),76598(5),2542(14))].
% 83685 (x \ 1) * (x * (y \ (y / x))) = y \ (y / x) # label(4074).  [para(15(a,1),81357(a,2,2,2)),rewrite(75570(9))].
% 92280 x * (((x \ (y * x)) / y) * (z * x)) = (((y / x) / y) \ z) * x.  [para(17658(a,1),3631(a,1,1,1)),rewrite(16(4),16(10),5675(8),11(6),4067(7),75253(10),4088(10),11444(7)),flip(a)].
% 92547 (x * (y / ((z * y) / z))) / (z \ 1) = x / (y * (z \ (y \ 1))).  [para(17767(a,1),3966(a,2,2)),rewrite(27573(7),74459(4),74462(14),54431(14))].
% 92609 (x \ y) / (z * (x \ (z \ 1))) = x \ (y * ((z * x) / z)).  [back_rewrite(58373),rewrite(92547(8))].
% 92634 (x * y) * ((y \ (z * y)) / z) = x * ((z * y) / z).  [back_rewrite(74571),rewrite(92609(6),3(5)),flip(a)].
% 92649 (x * y) / ((z * y) / z) = x * (y / ((z * y) / z)) # label(1025).  [back_rewrite(58705),rewrite(92634(12),9848(10),74459(7),74540(7),4(8),3(7),3(6))].
% 92663 (x * y) * (x / ((z * x) / z)) = x * (y * (x / ((z * x) / z))).  [back_rewrite(74556),rewrite(92649(5))].
% 92669 (x * y) * (z / ((x * z) / x)) = x * (y * (z / ((x * z) / x))).  [back_rewrite(67735),rewrite(92649(5))].
% 92900 x * (y * ((y \ (x \ (y * x))) * (x \ z))) = y * z.  [para(27543(a,1),18838(a,2,2,1)),rewrite(75253(8),37987(10),92663(6),11(7),75253(14),4062(15),74459(10),92669(10),92669(9),75254(8),4(3),18(7),75253(8),4088(8),11444(4),17(7)),flip(a)].
% 93159 (x * (y \ (x \ y))) * (y \ z) = x * (y \ (x \ z)) # label(1966).  [para(17767(a,1),19452(a,1,1,1)),rewrite(55984(8),97(4),3366(3),5315(6),17767(13),5392(11),49315(5),11790(3),92900(7),4(2),1389(14),5971(8),27706(8)),flip(a)].
% 93175 x * (y \ (x \ ((z / x) \ y))) = (y \ ((z * y) / x)) \ 1.  [back_rewrite(65569),rewrite(93159(7))].
% 93407 ((x \ (y \ (x * y))) * x) * z = (x \ (y \ (x * y))) * (x * z) # label(205).  [para(33956(a,1),19842(a,1,1)),rewrite(74518(9),5(10),33956(10),97(11),12271(9)),flip(a)].
% 93454 x \ ((y \ (x * y)) * z) = (x \ (y \ (x * y))) * z # label(222).  [back_rewrite(58871),rewrite(93407(6),3(5)),flip(a)].
% 93464 ((x \ (y \ (x * y))) * x) \ z = x \ ((y \ (x \ (y * x))) * z).  [back_rewrite(74934),rewrite(93454(9))].
% 93781 (x / ((y * x) / y)) * z = x * (y * (x \ (y \ z))) # label(2213).  [para(22991(a,1),1070(a,2,1)),rewrite(16(4),3690(3),93159(5),16(10),5675(8),11(6),4067(7)),flip(a)].
% 93854 (x / ((y * x) / y)) \ z = y * (x * (y \ (x \ z))) # label(2215).  [back_rewrite(75253),rewrite(93781(8))].
% 93866 ((x / ((y / z) / y)) * z) * (z \ 1) = x * ((y * z) / y).  [back_rewrite(58749),rewrite(93781(6),9848(10),65123(9),7151(7),3(6))].
% 95229 (((x \ (y * x)) * z) / u) \ (x \ v) = x \ (((y * (x * z)) / (x * u)) \ v).  [para(231(a,1),36548(a,1,1,1))].
% 95698 x * (((x \ (y * x)) / y) * z) = y * (x * (y \ z)) # label(1931).  [para(10188(a,1),39277(a,1,1)),rewrite(93854(5),4(2),774(6),3690(6),74510(7)),flip(a)].
% 95811 (((x / y) / x) \ z) * y = x * (y * (x \ (z * y))) # label(2579).  [back_rewrite(92280),rewrite(95698(6)),flip(a)].
% 95853 (x \ (y \ (x * y))) * (y \ z) = x \ (y \ (x * z)) # label(1074).  [para(1347(a,1),39312(a,1,2)),rewrite(5(2),3366(7),231(6),93454(7),93464(9),3(10)),flip(a)].
% 98170 (x * (y \ (x \ (y * z)))) / z = x * (y \ (x \ y)) # label(2386).  [para(73715(a,1),4407(a,2,1)),rewrite(74483(12),4(13)),flip(a)].
% 98174 1 / ((x / y) * (((z \ (x * z)) / y) \ y)) = (1 / y) * ((z \ (x * z)) / x).  [para(73715(a,1),5464(a,1,2,1)),rewrite(65402(7))].
% 98184 (x * (y \ (x \ y))) * z = x * (y \ (x \ (y * z))) # label(610).  [para(73715(a,1),645(a,2,1)),rewrite(3366(3),95853(5),2(6)),flip(a)].
% 99108 (x * (y * (z \ (y \ z)))) * (z \ (u * z)) = ((x / ((y * z) / y)) * u) * z.  [para(74358(a,1),8(a,1,1))].
% 99111 (x / y) * ((z * y) / z) = x * ((y \ (z * y)) / z) # label(928).  [para(61(a,1),74358(a,1,1,2,1)),rewrite(7163(5),93866(8),3163(11),647(11),134(12),3154(11),11(12),74758(11),2(9))].
% 99270 (x * (y \ (z * y))) / z = x * ((y \ (z * y)) / z) # label(2136).  [back_rewrite(7029),rewrite(99111(8))].
% 99370 (((x * y) / z) / x) * z = x * (y * (z \ (x \ z))) # label(2459).  [para(4(a,1),74367(a,1,2,1)),flip(a)].
% 99381 (x / y) * (z \ (y * z)) = x * (y \ (z \ (y * z))) # label(356).  [para(74367(a,1),74(a,2,1)),rewrite(58385(7),11790(3),3(6),28(8)),flip(a)].
% 99588 x * ((x \ y) / (z \ (x \ z))) = y * (z \ (x * z)).  [para(74441(a,1),401(a,2,1)),rewrite(99108(7),2149(4),6(3),3366(5),74574(6),1(6),74724(5))].
% 99622 (x * y) * (y \ (z \ (y * z))) = x * (z \ (y * z)) # label(348).  [back_rewrite(74724),rewrite(99588(10))].
% 99859 x \ ((x * x) * ((y \ (z * y)) / z)) = 1 / (z * (y \ (z \ (y * (x \ 1))))).  [para(74462(a,1),3037(a,1,2)),rewrite(98184(13))].
% 100202 ((x * (y \ (x \ y))) / z) \ 1 = (1 / z) \ ((y \ (x * y)) / x).  [para(74510(a,1),575(a,1,1,2)),rewrite(1032(6)),flip(a)].
% 100216 (((x \ (y * x)) / y) * z) * (z \ u) = z * ((y * (x \ (y \ (x * z)))) \ u).  [para(74510(a,1),1768(a,1,1)),rewrite(29(6),98184(10))].
% 100573 (x / (x * (y \ (z \ (y * z))))) \ 1 = x / (x * (z \ (y \ (z * y)))).  [para(74574(a,1),644(a,1,1,1)),rewrite(34852(5),34852(12))].
% 100621 x / ((y \ (z \ (y * z))) * x) = z \ (y \ (z * y)) # label(1816).  [para(74574(a,1),71619(a,1,1)),rewrite(74731(8),74574(12),5(13),74574(8),1(8)),flip(a)].
% 100627 (x * ((y \ (z \ (y * z))) * u)) / u = (x * u) / ((z \ (y \ (z * y))) * u).  [para(74574(a,1),22356(a,1,2)),rewrite(18339(10))].
% 100650 x / (y * ((z \ (u \ (z * u))) * (y \ x))) = y / (y * (z \ (u \ (z * u)))).  [para(75216(a,1),264(a,2,1)),rewrite(75255(13),15158(14),100573(7),56298(6))].
% 100700 ((x \ (y \ (x * y))) * z) * (z \ u) = z * (((y \ (x \ (y * x))) * z) \ u).  [para(75255(a,1),1768(a,1,1)),rewrite(29(6))].
% 101561 x * (y * (z \ (y \ (((z * x) / ((y * z) / y)) \ z)))) = 1.  [para(74510(a,1),76312(a,2,1)),rewrite(98184(12),49321(16),9711(11),6169(15),36511(11),18(11),231(12),5167(14),93175(16),178(12),8692(10),4(11),17551(11),5(6),4(10),100202(10),1164(11),98184(8),95698(5),4(4),4(3),3(2),13(1),100216(10),49321(9),6169(8),3163(7),4067(5)),flip(a)].
% 103818 ((x \ (y \ (x * y))) * z) \ (x \ u) = x \ ((((y \ (x * y)) * z) / x) \ u).  [para(93454(a,1),3163(a,1,1))].
% 103854 (x * y) / ((z \ (u \ (z * u))) * y) = (x / ((z / y) \ (u \ (z * u)))) * y # label(1118).  [para(93454(a,1),5715(a,1,2))].
% 103855 (x / ((y / z) \ (u \ (y * u)))) * z = (x / z) * ((u / z) \ (y \ (u * y))).  [para(93454(a,1),5720(a,1,1,2)),rewrite(100627(6),103854(6))].
% 103867 (x * y) \ (x * (z \ (y * z))) = y \ (z \ (y * z)) # label(124).  [para(93454(a,1),19839(a,1,1)),rewrite(5(9)),flip(a)].
% 103971 (1 / x) \ (y \ (z \ (y * z))) = (y / x) \ (z \ (y * z)) # label(1466).  [back_rewrite(37934),rewrite(103854(6),103855(6),13(1),1(6)),flip(a)].
% 103972 (x * y) / ((z \ (u \ (z * u))) * y) = (x / y) * ((u / y) \ (z \ (u * z))).  [back_rewrite(103854),rewrite(103855(12))].
% 103994 ((x / y) \ (z \ (x * z))) / y = y / ((z / y) \ (x \ (z * x))).  [back_rewrite(69216),rewrite(103971(6),103971(11))].
% 104220 ((x \ (y * x)) / y) * z = (x \ (y * x)) * (y \ z) # label(2397).  [para(93854(a,1),19448(a,1,2)),rewrite(4(2),231(4),11444(8),74483(9),1(9),74510(8)),flip(a)].
% 104313 (x * (y \ (x \ y))) \ z = (y \ (x * y)) * (x \ z) # label(1821).  [back_rewrite(74510),rewrite(104220(8))].
% 104717 ((1 / x) \ y) * (z \ (x * z)) = x * (y * (z \ (x * z))) # label(1603).  [para(34(a,1),95811(a,2)),rewrite(774(3),13(1),5(4),3(11))].
% 105301 x * (y \ (x \ (((y * z) / ((x * y) / x)) \ y))) = z \ 1.  [para(98170(a,1),83685(a,1,2,2,2)),rewrite(49321(10),6169(9),3163(8),4067(6),101561(11),2(4),98170(11),49321(10),6169(9),3163(8),4067(6)),flip(a)].
% 105373 (x / y) * (((z \ (x * z)) / y) \ y) = x * (z \ (x \ (z * y))).  [para(98184(a,1),14063(a,1,1)),rewrite(98184(10),49321(14),6169(13),3163(12),4067(10),105301(14),15(9),65402(6),98184(10))].
% 105419 1 / (x * (y \ (x \ (y * z)))) = (1 / z) * ((y \ (x * y)) / x).  [back_rewrite(98174),rewrite(105373(7))].
% 105439 x \ ((x * x) * ((y \ (z * y)) / z)) = x * ((y \ (z * y)) / z).  [back_rewrite(99859),rewrite(105419(14),15(10))].
% 105923 x \ ((x * y) * ((z \ (u * z)) / u)) = (y / (x \ z)) * (x \ ((u * z) / u)).  [para(99111(a,1),9785(a,1,2))].
% 105992 (x / (x \ y)) * (x \ ((z * y) / z)) = x * ((y \ (z * y)) / z).  [back_rewrite(105439),rewrite(105923(6))].
% 106334 ((x \ (y \ (x * y))) * z) / y = (x \ (y \ (x * y))) * (z / y).  [para(99381(a,1),7429(a,1,1)),rewrite(1(5),75255(5),3366(9),231(8),93454(9)),flip(a)].
% 106349 x \ ((x * y) * (z \ (u \ (z * u)))) = (y / (x \ z)) * (x \ (u \ (z * u))) # label(591).  [para(99381(a,1),9785(a,1,2))].
% 106375 (((1 / x) / y) * x) * ((1 / y) \ z) = (x \ (y \ (x * y))) * z # label(2426).  [back_rewrite(41816),rewrite(106334(6),5(5)),flip(a)].
% 106552 1 / ((x / y) \ (z \ (x * z))) = (z \ (x \ (z * x))) / y.  [para(100621(a,1),698(a,2,1)),rewrite(1032(7),103971(7))].
% 106591 (x / ((y / ((z / y) \ (u \ (z * u)))) * x)) * y = (z / y) \ (u \ (z * u)).  [para(100621(a,1),22356(a,1,2)),rewrite(103971(6),21062(14),103971(10),103994(9)),flip(a)].
% 106744 (x / (x * (y * (z \ (y \ z))))) / ((x * y) \ 1) = x * (z \ (y * z)) # label(2140).  [para(103867(a,1),207(a,1,2,2)),rewrite(106349(9),6138(4),13(1),60421(9),105923(6),105992(6),29(5),99622(5),34497(8)),flip(a)].
% 106762 x * ((x \ (y \ (z \ (y * z)))) * (z \ (y \ (z * y)))) = 1 # label(2150).  [para(103867(a,1),25188(a,2,1,1)),rewrite(34497(8),106744(12),13(7),9860(10),774(8),28(9),99381(9)),flip(a)].
% 110823 x * (y \ (z \ (y * ((z * (x * (y \ (z \ y)))) \ z)))) = 1.  [para(103971(a,1),75426(a,1,2,1)),rewrite(74574(8),3673(9),93454(4),100700(9),103818(8),95229(7),39277(6),774(4),99370(4),74574(17),106762(18))].
% 110826 ((x / (y * (z \ (x \ (z * x))))) \ (z \ (x * z))) \ y = 1.  [para(103971(a,1),76263(a,1,1)),rewrite(74574(4),75255(13),100700(18),103818(17),95229(16),39277(15),774(13),99370(13),110823(18))].
% 110827 ((x \ (y \ (x * y))) * (1 / z)) * ((y / z) \ (x \ (y * x))) = 1.  [para(103971(a,1),76263(a,2,2)),rewrite(74574(7),103971(12),110826(13),75255(7)),flip(a)].
% 110831 (x \ (y \ (x * y))) * (1 / z) = (x \ (y \ (x * y))) / z.  [para(103971(a,1),78984(a,1,1,2)),rewrite(75255(6),110827(11),75255(7),11(8),103971(13),106552(12))].
% 110841 x / ((y / x) \ (z \ (y * z))) = x / (x * (y \ (z \ (y * z)))) # label(3242).  [para(103971(a,1),72479(a,2,2)),rewrite(75255(7),2(7),75216(10),75255(8),110831(8),5675(7),11(5),34852(5),16(9)),flip(a)].
% 110865 (x / y) \ (z \ (x * z)) = y * (x \ (z \ (x * z))) # label(3072).  [back_rewrite(106591),rewrite(110841(5),56298(6),100650(7),56298(6),12(4),2(5)),flip(a)].
% 110892 (x * y) / ((z \ (u \ (z * u))) * y) = y * ((y \ x) * (u \ (z \ (u * z)))).  [back_rewrite(103972),rewrite(110865(11),17(12))].
% 114450 (x * ((y \ (z * y)) / z)) / (u * ((y \ (z * y)) / z)) = x / u.  [para(5030(a,1),2065(a,1,1,2)),rewrite(9860(17),18157(9),5715(13),65233(14),28(8),104717(8),28(9),9750(11),99270(4),99270(8),4(17))].
% 114884 x / ((y \ (z * y)) * (z \ u)) = (x / u) * (z * (y \ (z \ y))) # label(2537).  [para(104313(a,1),2065(a,2,2)),rewrite(74462(4),74462(8),114450(9)),flip(a)].
% 114952 x / ((y \ (z \ (y * z))) * u) = (x / u) * (z \ (y \ (z * y))) # label(1705).  [para(19240(a,1),114884(a,1,2,1)),rewrite(28(4),1(4),25017(4),106375(8),4(17),509(12),99381(11),1(11))].
% 115015 x * ((x \ y) * (z \ (u \ (z * u)))) = y * (z \ (u \ (z * u))) # label(1707).  [back_rewrite(110892),rewrite(114952(6),5(2)),flip(a)].
% 115347 (x * y) * (z \ (u \ (z * u))) = x * (y * (z \ (u \ (z * u)))) # label(1709).  [para(4(a,1),115015(a,1,2,1)),flip(a)].
% 115348 $F.  [resolve(115347,a,11918,a)].
% 
% ============================== end of proof ==========================