% Length of proof is 824.  Level of proof is 111.
% 
% ---------------- PROOF ----------------
% 
% 2 [] 1*x=x.
% 3 [] x*1=x.
% 4 [] x* (x\y)=y.
% 5 [] x\ (x*y)=y.
% 6 [] (x*y)/y=x.
% 7 [] (x/y)*y=x.
% 8 [] ((x*y)/x)* (x*z)=x* (y*z)   # label(LCC).
% 9 [] (z*x)* (x\ (y*x))= (z*y)*x   # label(RCC).
% 11 [] (A*B)* ((D*C)\ (C*D))!=A* (B* ((D*C)\ (C*D)))   # label("orig flipped").
% 855 [para_into,4.1.1,2.1.1] 1\x=x.
% 856 [para_into,5.1.1.2,3.1.1] x\x=1.
% 857 [para_into,6.1.1.1,4.1.1] x/ (y\x)=y.
% 859 [para_into,6.1.1.1,2.1.1] x/x=1.
% 860 [para_from,7.1.1,5.1.1.2] (x/y)\x=y.
% 861 [para_into,8.1.1.1.1,4.1.1] (x/y)* (y*z)=y* ((y\x)*z).
% 862 [para_into,8.1.1.2,4.1.1] ((x*y)/x)*z=x* (y* (x\z)).
% 863 [para_from,8.1.1,6.1.1.1] (x* (y*z))/ (x*z)= (x*y)/x.
% 864 [para_into,9.1.1.1,7.1.1,flip.1] ((x/y)*z)*y=x* (y\ (z*y)).
% 865 [para_into,9.1.1.2.2,7.1.1,flip.1] (x* (y/z))*z= (x*z)* (z\y).
% 866 [para_into,9.1.1.2.2,4.1.1] (x* (y\z))* ((y\z)\z)= (x*y)* (y\z).
% 867 [para_from,9.1.1,6.1.1.1] ((x*y)*z)/ (z\ (y*z))=x*z.
% 868 [para_from,9.1.1,5.1.1.2] (x*y)\ ((x*z)*y)=y\ (z*y).
% 869 [para_into,861.1.1.1,6.1.1,flip.1] x* ((x\ (y*x))*z)=y* (x*z).
% 870 [para_into,861.1.1.2,4.1.1,flip.1] x* ((x\y)* (x\z))= (y/x)*z.
% 871 [para_from,861.1.1,5.1.1.2] (x/y)\ (y* ((y\x)*z))=y*z.
% 872 [para_into,862.1.1.1.1,7.1.1,flip.1] (x/y)* (y* ((x/y)\z))= (x/ (x/y))*z.
% 873 [para_into,862.1.1,3.1.1,flip.1] x* (y* (x\1))= (x*y)/x.
% 874 [para_from,862.1.1,6.1.1.1] (x* (y* (x\z)))/z= (x*y)/x.
% 875 [para_into,873.1.1.2.2,860.1.1,flip.1] ((1/x)*y)/ (1/x)= (1/x)* (y*x).
% 876 [para_into,873.1.1.2,7.1.1,flip.1] (x* (y/ (x\1)))/x=x*y.
% 877 [para_from,873.1.1,5.1.1.2] x\ ((x*y)/x)=y* (x\1).
% 878 [para_from,876.1.1,7.1.1.1,flip.1] x* (y/ (x\1))= (x*y)*x.
% 879 [para_into,877.1.1.2.1,4.1.1,flip.1] (x\y)* (x\1)=x\ (y/x).
% 880 [para_from,878.1.1,5.1.1.2] x\ ((x*y)*x)=y/ (x\1).
% 881 [para_into,880.1.1.2.1,4.1.1,flip.1] (x\y)/ (x\1)=x\ (y*x).
% 882 [para_from,880.1.1,9.1.1.2] (x*y)* (z/ (y\1))= (x* (y*z))*y.
% 883 [para_into,881.1.1.2,860.1.1,flip.1] (1/x)\ (y* (1/x))= ((1/x)\y)/x.
% 884 [para_into,863.1.1.1.2,7.1.1,flip.1] (x* (y/z))/x= (x*y)/ (x*z).
% 885 [para_into,863.1.1.1.2,4.1.1] (x*y)/ (x* (z\y))= (x*z)/x.
% 886 [para_into,864.1.1.1,862.1.1] (x* (y* (x\z)))*x= (x*y)* (x\ (z*x)).
% 887 [para_into,864.1.1.1,861.1.1] (x* ((x\y)*z))*x=y* (x\ ((x*z)*x)).
% 888 [para_from,864.1.1,6.1.1.1] (x* (y\ (z*y)))/y= (x/y)*z.
% 889 [para_from,864.1.1,5.1.1.2] ((x/y)*z)\ (x* (y\ (z*y)))=y.
% 890 [para_into,865.1.1.1,7.1.1,flip.1] ((x/ (y/z))*z)* (z\y)=x*z.
% 891 [para_from,865.1.1,880.1.1.2] x\ ((x*x)* (x\y))= (y/x)/ (x\1).
% 892 [para_into,867.1.1.1.1,7.1.1] (x*y)/ (y\ (z*y))= (x/z)*y.
% 893 [para_into,868.1.1.1,4.1.1,flip.1] (x\y)\ (z* (x\y))=y\ ((x*z)* (x\y)).
% 894 [para_into,868.1.1.2.1,4.1.1] (x*y)\ (z*y)=y\ ((x\z)*y).
% 895 [para_from,869.1.1,5.1.1.2] x\ (y* (x*z))= (x\ (y*x))*z.
% 896 [para_from,870.1.1,5.1.1.2] x\ ((y/x)*z)= (x\y)* (x\z).
% 897 [para_into,871.1.1.2.2,4.1.1] (x/y)\ (y*z)=y* ((y\x)\z).
% 898 [para_into,874.1.1.1.2,7.1.1,flip.1] (x* (y/ (x\z)))/x= (x*y)/z.
% 899 [para_from,884.1.1,862.1.1.1] ((x*y)/ (x*z))*u=x* ((y/z)* (x\u)).
% 900 [para_into,885.1.1.1,4.1.1] x/ (y* (z\ (y\x)))= (y*z)/y.
% 901 [para_into,885.1.1.1,3.1.1] x/ (x* (y\1))= (x*y)/x.
% 902 [para_from,901.1.1,860.1.1.1] ((x*y)/x)\x=x* (y\1).
% 903 [para_into,902.1.1.1.1,4.1.1,flip.1] x* ((x\y)\1)= (y/x)\x.
% 904 [para_from,903.1.1,5.1.1.2] x\ ((y/x)\x)= (x\y)\1.
% 905 [para_into,904.1.1.2.1,6.1.1,flip.1] (x\ (y*x))\1=x\ (y\x).
% 907 [para_from,905.1.1,901.1.1.2.2,flip.1] (x* (y\ (z*y)))/x=x/ (x* (y\ (z\y))).
% 914 [para_into,888.1.1.1.2.2,7.1.1] (x* (y\z))/y= (x/y)* (z/y).
% 915 [para_into,888.1.1.1,2.1.1] (x\ (y*x))/x= (1/x)*y.
% 916 [para_into,915.1.1.1.2,7.1.1,flip.1] (1/x)* (y/x)= (x\y)/x.
% 918 [para_from,916.1.1,6.1.1.1] ((x\y)/x)/ (y/x)=1/x.
% 919 [para_into,918.1.1.1.1,5.1.1] (x/y)/ ((y*x)/y)=1/y.
% 920 [para_from,919.1.1,860.1.1.1] (1/x)\ (y/x)= (x*y)/x.
% 921 [para_into,920.1.1.2,888.1.1,flip.1] (x* (y* (x\ (z*x))))/x= (1/x)\ ((y/x)*z).
% 927 [para_into,889.1.1.2,2.1.1] ((1/x)*y)\ (x\ (y*x))=x.
% 928 [para_from,890.1.1,874.1.1.1.2,flip.1] (x* ((y/ (z/x))*x))/x= (x* (y*x))/z.
% 929 [para_from,890.1.1,6.1.1.1] (x*y)/ (y\z)= (x/ (z/y))*y.
% 930 [para_into,892.1.1.1,7.1.1] x/ (y\ (z*y))= ((x/y)/z)*y.
% 931 [para_into,892.1.1.1,2.1.1] x/ (x\ (y*x))= (1/y)*x.
% 932 [para_into,892.1.1.2,880.1.1] (x*y)/ (z/ (y\1))= (x/ (y*z))*y.
% 933 [para_into,892.1.1,873.1.2] (x\ (y*x))* (x* ((x\ (y*x))\1))= ((x\ (y*x))/y)*x.
% 934 [para_from,892.1.1,879.1.2.2] ((x\ (y*x))\ (z*x))* ((x\ (y*x))\1)= (x\ (y*x))\ ((z/y)*x).
% 935 [para_into,931.1.1.2.2,7.1.1,flip.1] (1/ (x/y))*y=y/ (y\x).
% 937 [para_from,931.1.1,860.1.1.1] ((1/x)*y)\y=y\ (x*y).
% 938 [para_from,935.1.1,6.1.1.1] (x/ (x\y))/x=1/ (y/x).
% 939 [para_from,935.1.1,5.1.1.2] (1/ (x/y))\ (y/ (y\x))=y.
% 941 [para_into,937.1.1.1,916.1.1] ((x\y)/x)\ (y/x)= (y/x)\ (x* (y/x)).
% 942 [para_from,937.1.1,874.1.1.1.2.2] (((1/x)*y)* (z* (y\ (x*y))))/y= (((1/x)*y)*z)/ ((1/x)*y).
% 943 [para_into,938.1.1.1.2,5.1.1,flip.1] 1/ ((x*y)/x)= (x/y)/x.
% 948 [para_from,943.1.1,860.1.1.1] ((x/y)/x)\1= (x*y)/x.
% 955 [para_into,894.1.1.1,7.1.1,flip.1] x\ (((y/x)\z)*x)=y\ (z*x).
% 956 [para_into,894.1.1.2,7.1.1,flip.1] x\ ((y\ (z/x))*x)= (y*x)\z.
% 957 [para_into,894.1.1.2,2.1.1,flip.1] x\ ((y\1)*x)= (y*x)\x.
% 958 [para_from,957.1.1,927.1.1.2] ((1/x)* (y\1))\ ((y*x)\x)=x.
% 959 [para_from,957.1.1,9.1.1.2] (x*y)* ((z*y)\y)= (x* (z\1))*y.
% 960 [para_from,957.1.1,4.1.1.2] x* ((y*x)\x)= (y\1)*x.
% 961 [para_into,960.1.1.2.1,7.1.1,flip.1] ((x/y)\1)*y=y* (x\y).
% 962 [para_from,961.1.1,861.1.2.2] (1/ (x/y))* ((x/y)*y)= (x/y)* (y* (x\y)).
% 963 [para_from,961.1.1,6.1.1.1] (x* (y\x))/x= (y/x)\1.
% 964 [para_into,963.1.1.1.2,5.1.1] ((x*y)*y)/ (x*y)= (x/ (x*y))\1.
% 965 [para_from,963.1.1,902.1.1.1] ((x/y)\1)\y=y* ((x\y)\1).
% 966 [para_from,963.1.1,862.1.1.1,flip.1] x* ((y\x)* (x\z))= ((y/x)\1)*z.
% 967 [para_into,895.1.1.2.2,4.1.1,flip.1] (x\ (y*x))* (x\z)=x\ (y*z).
% 968 [para_into,895.1.1.2,873.1.1,flip.1] (x\ (y*x))* (y\1)=x\ ((y*x)/y).
% 969 [para_into,896.1.1.2,4.1.1,flip.1] (x\y)* (x\ ((y/x)\z))=x\z.
% 970 [para_into,897.1.1.1,6.1.1,flip.1] x* ((x\ (y*x))\z)=y\ (x*z).
% 971 [para_into,897.1.1.2,3.1.1,flip.1] x* ((x\y)\1)= (y/x)\x.
% 972 [para_from,971.1.1,5.1.1.2] x\ ((y/x)\x)= (x\y)\1.
% 973 [para_into,972.1.1.2.1,6.1.1,flip.1] (x\ (y*x))\1=x\ (y\x).
% 974 [para_into,973.1.1.1,880.1.1] (x/ (y\1))\1=y\ ((y*x)\y).
% 975 [para_from,973.1.1,873.1.1.2.2,flip.1] ((x\ (y*x))*z)/ (x\ (y*x))= (x\ (y*x))* (z* (x\ (y\x))).
% 976 [para_from,973.1.1,857.1.1.2] 1/ (x\ (y\x))=x\ (y*x).
% 983 [para_from,898.1.1,865.1.1.1.2,flip.1] (x*y)* (y\ (y* (z/ (y\u))))= (x* ((y*z)/u))*y.
% 984 [para_from,898.1.1,902.1.1.1,flip.1] x* ((y/ (x\z))\1)= ((x*y)/z)\x.
% 985 [para_from,898.1.1,877.1.1.2,flip.1] (x/ (y\z))* (y\1)=y\ ((y*x)/z).
% 986 [para_from,898.1.1,7.1.1.1] ((x*y)/z)*x=x* (y/ (x\z)).
% 987 [para_from,900.1.1,948.1.1.1.1,flip.1] (x* (y* (z\ (y\x))))/x= (((y*z)/y)/x)\1.
% 988 [para_from,900.1.1,860.1.1.1] ((x*y)/x)\z=x* (y\ (x\z)).
% 989 [para_into,914.1.1.1.2,5.1.1,flip.1] (x/y)* ((y*z)/y)= (x*z)/y.
% 990 [para_into,929.1.1.1,7.1.1,flip.1] ((x/y)/ (z/y))*y=x/ (y\z).
% 991 [para_into,929.1.1.2,5.1.1,flip.1] (x/ ((y*z)/y))*y= (x*y)/z.
% 993 [para_into,930.1.1.2,880.1.1,flip.1] ((x/y)/ (y*z))*y=x/ (z/ (y\1)).
% 994 [para_into,930.1.2.1,938.1.1] x/ ((x\y)\ (x* (x\y)))= (1/ (y/x))* (x\y).
% 995 [para_from,930.1.1,860.1.1.1] (((x/y)/z)*y)\x=y\ (z*y).
% 996 [para_into,955.1.1.2.1.1,881.1.1] (x\1)\ (((x\ (y*x))\z)* (x\1))= (x\y)\ (z* (x\1)).
% 997 [para_into,955.1.1.2.1,897.1.1] x\ ((x* ((x\y)\z))*x)=y\ ((x*z)*x).
% 998 [para_from,955.1.1,915.1.1.1,flip.1] (1/x)* ((y/x)\z)= (y\ (z*x))/x.
% 999 [para_from,955.1.1,869.1.1.2.1,flip.1] ((x/y)\z)* (y*u)=y* ((x\ (z*y))*u).
% 1000 [para_from,955.1.1,888.1.1.1.2] (x* (y\ (z*u)))/u= (x/u)* ((y/u)\z).
% 1001 [para_from,955.1.1,4.1.1.2,flip.1] ((x/y)\z)*y=y* (x\ (z*y)).
% 1002 [para_from,956.1.1,892.1.1.2] (x*y)/ ((z*y)\u)= (x/ (z\ (u/y)))*y.
% 1003 [para_from,956.1.1,9.1.1.2,flip.1] (x* (y\ (z/u)))*u= (x*u)* ((y*u)\z).
% 1004 [para_from,956.1.1,4.1.1.2,flip.1] (x\ (y/z))*z=z* ((x*z)\y).
% 1005 [para_into,958.1.1.2.1,4.1.1] ((1/ (x\y))* (x\1))\ (y\ (x\y))=x\y.
% 1006 [para_into,965.1.1.1.1,857.1.1,flip.1] (x\y)* ((y\ (x\y))\1)= (x\1)\ (x\y).
% 1007 [para_into,967.1.1.1,956.1.1,flip.1] x\ ((y\ (z/x))*u)= ((y*x)\z)* (x\u).
% 1008 [para_into,967.1.1.1,955.1.1,flip.1] x\ (((y/x)\z)*u)= (y\ (z*x))* (x\u).
% 1010 [para_into,967.1.1.1,880.1.1] (x/ (y\1))* (y\z)=y\ ((y*x)*z).
% 1011 [para_from,967.1.1,6.1.1.1] (x\ (y*z))/ (x\z)=x\ (y*x).
% 1012 [para_from,969.1.1,5.1.1.2] (x\y)\ (x\z)=x\ ((y/x)\z).
% 1014 [para_into,970.1.1.2.1,880.1.1] x* ((y/ (x\1))\z)= (x*y)\ (x*z).
% 1015 [para_from,970.1.1,963.1.1.1,flip.1] ((x\ (y*x))/x)\1= (y\ (x*x))/x.
% 1016 [para_from,970.1.1,5.1.1.2,flip.1] (x\ (y*x))\z=x\ (y\ (x*z)).
% 1019 [para_into,986.1.1.1.1,4.1.1,flip.1] x* ((x\y)/ (x\z))= (y/z)*x.
% 1020 [para_into,986.1.1.1.1,3.1.1,flip.1] x* (1/ (x\y))= (x/y)*x.
% 1021 [para_into,1020.1.1.2.2,860.1.1,flip.1] ((x/y)/x)* (x/y)= (x/y)* (1/y).
% 1022 [para_from,1020.1.1,5.1.1.2] x\ ((x/y)*x)=1/ (x\y).
% 1023 [para_into,1022.1.1.2,8.1.1] (x*y)\ (x* (y*y))=1/ ((x*y)\x).
% 1025 [para_from,1022.1.1,931.1.1.2] x/ (1/ (x\y))= (1/ (x/y))*x.
% 1026 [para_from,1022.1.1,970.1.1.2.1] x* ((1/ (x\y))\z)= (x/y)\ (x*z).
% 1027 [para_from,1022.1.1,930.1.1.2,flip.1] ((x/y)/ (y/z))*y=x/ (1/ (y\z)).
% 1028 [para_into,988.1.2.2,972.1.1] (((x/y)*y)/ (x/y))\y= (x/y)* ((y\x)\1).
% 1029 [para_into,988.1.2,967.1.1] (((x\ (y*x))*x)/ (x\ (y*x)))\z=x\ (y* ((x\ (y*x))\z)).
% 1030 [para_into,989.1.1.1,6.1.1,flip.1] ((x*y)*z)/y=x* ((y*z)/y).
% 1031 [para_into,989.1.1.2,898.1.1,flip.1] (x* (y/ (z\u)))/z= (x/z)* ((z*y)/u).
% 1034 [para_into,989.1.1.2,884.1.1] (x/y)* ((y*z)/ (y*u))= (x* (z/u))/y.
% 1035 [para_into,989.1.1,862.1.1] x* (y* (x\ ((x*z)/x)))= ((x*y)*z)/x.
% 1036 [para_from,990.1.1,6.1.1.1] (x/ (y\z))/y= (x/y)/ (z/y).
% 1037 [para_into,991.1.1.1.2,963.1.1] (x/ ((y/z)\1))*z= (x*z)/ (y\z).
% 1039 [para_from,991.1.1,869.1.1.2.1.2,flip.1] (x/ ((y*z)/y))* (y*u)=y* ((y\ ((x*y)/z))*u).
% 1040 [para_from,991.1.1,6.1.1.1] ((x*y)/z)/y=x/ ((y*z)/y).
% 1041 [para_into,1001.1.1.1.1,915.1.1,flip.1] x* ((x\ (y*x))\ (z*x))= (((1/x)*y)\z)*x.
% 1042 [para_into,1001.1.1.1.1,857.1.1,flip.1] (x\y)* (y\ (z* (x\y)))= (x\z)* (x\y).
% 1043 [para_into,1001.1.2.2,855.1.1] ((1/x)\y)*x=x* (y*x).
% 1044 [para_from,1001.1.1,6.1.1.1] (x* (y\ (z*x)))/x= (y/x)\z.
% 1045 [para_into,1043.1.1.1.1,976.1.1] ((x\ (y*x))\z)* (x\ (y\x))= (x\ (y\x))* (z* (x\ (y\x))).
% 1046 [para_from,1043.1.1,6.1.1.1] (x* (y*x))/x= (1/x)\y.
% 1047 [para_into,1046.1.1.1.2,865.1.1] (x* ((y*x)* (x\z)))/x= (1/x)\ (y* (z/x)).
% 1048 [para_from,1046.1.1,991.1.1.1.2] (x/ ((1/y)\z))*y= (x*y)/ (z*y).
% 1049 [para_from,1046.1.1,943.1.1.2,flip.1] (x/ (y*x))/x=1/ ((1/x)\y).
% 1050 [para_from,1046.1.1,862.1.1.1,flip.1] x* ((y*x)* (x\z))= ((1/x)\y)*z.
% 1051 [para_from,1004.1.1,6.1.1.1] (x* ((y*x)\z))/x=y\ (z/x).
% 1052 [para_into,1011.1.1.1.2,7.1.1,flip.1] x\ ((y/z)*x)= (x\y)/ (x\z).
% 1053 [para_into,1012.1.1.2,895.1.1] (x\y)\ ((x\ (z*x))*u)=x\ ((y/x)\ (z* (x*u))).
% 1054 [para_into,1016.1.1.1,1022.1.1,flip.1] x\ ((x/y)\ (x*z))= (1/ (x\y))\z.
% 1055 [para_from,1016.1.1,857.1.1.2] x/ (y\ (z\ (y*x)))=y\ (z*y).
% 1056 [para_into,1019.1.1.2.2,5.1.1,flip.1] (x/ (y*z))*y=y* ((y\x)/z).
% 1057 [para_into,1025.1.1.2.2,860.1.1,flip.1] (1/ ((x/y)/x))* (x/y)= (x/y)/ (1/y).
% 1058 [para_from,1025.1.2,6.1.1.1] (x/ (1/ (x\y)))/x=1/ (x/y).
% 1059 [para_into,1030.1.1.1,864.1.1] (x* (y\ (z*y)))/z= (x/y)* ((z*y)/z).
% 1060 [para_into,1040.1.1.1,885.1.1,flip.1] x/ ((y* (x* (z\y)))/y)= ((x*z)/x)/y.
% 1061 [para_into,1044.1.1.1.2.2,991.1.1,flip.1] (x/y)\ (z/ ((y*u)/y))= (y* (x\ ((z*y)/u)))/y.
% 1062 [para_into,1044.1.1.1.2.2,7.1.1,flip.1] (x/y)\ (z/y)= (y* (x\z))/y.
% 1063 [para_into,1051.1.1.1.2,927.1.1,flip.1] (1/x)\ ((x\ (y*x))/y)= (y*x)/y.
% 1064 [para_from,1051.1.1,1012.1.2.2.1] (x\ (x* ((y*x)\z)))\ (x\u)=x\ ((y\ (z/x))\u).
% 1065 [para_into,1052.1.2.2,877.1.1] x\ ((y/ ((x*z)/x))*x)= (x\y)/ (z* (x\1)).
% 1066 [para_from,1052.1.1,967.1.1.1] ((x\y)/ (x\z))* (x\u)=x\ ((y/z)*u).
% 1067 [para_from,1052.1.1,915.1.1.1] ((x\y)/ (x\z))/x= (1/x)* (y/z).
% 1068 [para_into,1055.1.1.2.2.2,7.1.1,flip.1] (x/y)\ (z* (x/y))=y/ ((x/y)\ (z\x)).
% 1069 [para_from,1056.1.1,1016.1.1.1.2] (x\ (x* ((x\y)/z)))\u=x\ ((y/ (x*z))\ (x*u)).
% 1070 [para_from,1056.1.1,869.1.1.2.1.2] x* ((x\ (x* ((x\y)/z)))*u)= (y/ (x*z))* (x*u).
% 1071 [para_into,1062.1.1.1,915.1.1,flip.1] (x* ((x\ (y*x))\z))/x= ((1/x)*y)\ (z/x).
% 1072 [para_into,1062.1.1.2,915.1.1,flip.1] (x* (y\ (x\ (z*x))))/x= (y/x)\ ((1/x)*z).
% 1073 [para_into,891.1.1.2.2,860.1.1] (x/y)\ (((x/y)* (x/y))*y)= (x/ (x/y))/ ((x/y)\1).
% 1074 [para_into,959.1.1.2.1,4.1.1] (x* (y\z))* (z\ (y\z))= (x* (y\1))* (y\z).
% 1075 [para_into,964.1.2.1,901.1.1] ((x* (y\1))* (y\1))/ (x* (y\1))= ((x*y)/x)\1.
% 1076 [para_from,964.1.1,862.1.1.1,flip.1] (x*y)* (y* ((x*y)\z))= ((x/ (x*y))\1)*z.
% 1077 [para_into,985.1.1.2,860.1.1,flip.1] (1/x)\ (((1/x)*y)/z)= (y/ ((1/x)\z))*x.
% 1078 [para_into,985.1.2.2.1,3.1.1] (1/ (x\y))* (x\1)=x\ (x/y).
% 1079 [para_into,1010.1.1.1.2,860.1.1,flip.1] (1/x)\ (((1/x)*y)*z)= (y/x)* ((1/x)\z).
% 1080 [para_into,1014.1.1.2.1.2,860.1.1,flip.1] ((1/x)*y)\ ((1/x)*z)= (1/x)* ((y/x)\z).
% 1081 [para_into,1015.1.1.1,915.1.1] ((1/x)*y)\1= (y\ (x*x))/x.
% 1082 [para_from,1081.1.1,857.1.1.2] 1/ ((x\ (y*y))/y)= (1/y)*x.
% 1083 [para_from,1023.1.1,857.1.1.2] (x* (y*y))/ (1/ ((x*y)\x))=x*y.
% 1084 [para_into,1026.1.1.2.1.2,860.1.1,flip.1] ((x/y)/x)\ ((x/y)*z)= (x/y)* ((1/y)\z).
% 1085 [para_into,1026.1.1.2.1.2,5.1.1,flip.1] (x/ (x*y))\ (x*z)=x* ((1/y)\z).
% 1086 [para_into,1026.1.1,895.1.2] x\ (y* (x* ((1/ ((x\ (y*x))\z))\u)))= ((x\ (y*x))/z)\ ((x\ (y*x))*u).
% 1088 [para_into,1037.1.1.1.2.1,857.1.1,flip.1] (x* (y\z))/ (z\ (y\z))= (x/ (y\1))* (y\z).
% 1089 [para_into,1048.1.1.1.2.1,857.1.1,flip.1] (x* (y\1))/ (z* (y\1))= (x/ (y\z))* (y\1).
% 1090 [para_into,1048.1.1.1.2,895.1.1] (x/ (((1/y)\ (z* (1/y)))*u))*y= (x*y)/ ((z* ((1/y)*u))*y).
% 1091 [para_into,1054.1.1.2.2,4.1.1,flip.1] (1/ (x\y))\ (x\z)=x\ ((x/y)\z).
% 1092 [para_from,1063.1.1,4.1.1.2] (1/x)* ((y*x)/y)= (x\ (y*x))/y.
% 1094 [para_into,1067.1.1,1036.1.1] ((x\y)/x)/ (z/x)= (1/x)* (y/z).
% 1095 [para_into,1085.1.1.1.2,984.1.1] (x/ (((x*y)/z)\x))\ (x*u)=x* ((1/ ((y/ (x\z))\1))\u).
% 1096 [para_into,1091.1.1.1,930.1.1] (((1/x)/y)*x)\ (x\z)=x\ ((x/ (y*x))\z).
% 1097 [para_from,1092.1.1,1004.1.2.2.1] ((1/x)\ (y/ ((z*x)/z)))* ((z*x)/z)= ((z*x)/z)* (((x\ (z*x))/z)\y).
% 1099 [para_from,866.1.1,1050.1.1.2] (x\y)* ((z*x)* (x\y))= ((1/ (x\y))\z)*y.
% 1100 [para_into,872.1.1,861.1.1] x* ((x\y)* ((y/x)\z))= (y/ (y/x))*z.
% 1101 [para_into,887.1.2.2,880.1.1] (x* ((x\y)*z))*x=y* (z/ (x\1)).
% 1102 [para_from,1101.1.1,6.1.1.1] (x* (y/ (z\1)))/z=z* ((z\x)*y).
% 1103 [para_into,1102.1.1.1,2.1.1] (x/ (y\1))/y=y* ((y\1)*x).
% 1104 [para_into,1103.1.1,1036.1.1] (x/y)/ (1/y)=y* ((y\1)*x).
% 1105 [para_into,1104.1.2,870.1.1] ((x\y)/x)/ (1/x)= (1/x)*y.
% 1106 [para_into,899.1.2.2,998.1.1] (((x/y)*1)/ ((x/y)*y))*z= (x/y)* ((x\ (z*y))/y).
% 1107 [para_from,907.1.1,862.1.1.1] (x/ (x* (y\ (z\y))))*u=x* ((y\ (z*y))* (x\u)).
% 1108 [para_into,928.1.1,1046.1.1] (1/x)\ (y/ (z/x))= (x* (y*x))/z.
% 1109 [para_into,1108.1.1.2.2,915.1.1] (1/x)\ (y/ ((1/x)*z))= (x* (y*x))/ (x\ (z*x)).
% 1110 [para_into,1108.1.1.2.2,6.1.1,flip.1] (x* (y*x))/ (z*x)= (1/x)\ (y/z).
% 1111 [para_into,1110.1.1.1.2,7.1.1,flip.1] (1/x)\ ((y/x)/z)= (x*y)/ (z*x).
% 1112 [para_into,1111.1.1.2,1040.1.1] (1/x)\ (y/ ((z*x)/z))= (x* (y*z))/ (z*x).
% 1113 [para_into,941.1.1.1.1,5.1.1,flip.1] ((x*y)/x)\ (x* ((x*y)/x))= (y/x)\ ((x*y)/x).
% 1114 [para_into,997.1.1,880.1.1] ((x\y)\z)/ (x\1)=y\ ((x*z)*x).
% 1115 [para_into,1114.1.1.1.1,5.1.1,flip.1] (x*y)\ ((x*z)*x)= (y\z)/ (x\1).
% 1116 [para_into,1115.1.1.2.1,4.1.1,flip.1] (x\ (y\z))/ (y\1)= (y*x)\ (z*y).
% 1117 [para_into,1115.1.1.2.1,3.1.1] (x*y)\ (x*x)= (y\1)/ (x\1).
% 1118 [para_into,1116.1.2.2,2.1.1] (x\ (y\1))/ (y\1)= (y*x)\y.
% 1119 [para_from,1116.1.1,1014.1.1.2.1,flip.1] (x* (y\ (x\z)))\ (x*u)=x* (((x*y)\ (z*x))\u).
% 1120 [para_into,1000.1.1.1.2.2,2.1.1,flip.1] (x/y)* ((z/y)\1)= (x* (z\y))/y.
% 1121 [para_into,1000.1.1.1.2,1016.1.1] (x* (y\ (z\ (y* (u*w)))))/w= (x/w)* (((y\ (z*y))/w)\u).
% 1122 [para_into,1000.1.1.1.2,855.1.1,flip.1] (x/y)* ((1/y)\z)= (x* (z*y))/y.
% 1123 [para_into,1000.1.1.1,862.1.1] (x* (y* (x\ (z\ (u*w)))))/w= (((x*y)/x)/w)* ((z/w)\u).
% 1124 [para_into,1120.1.1.2.1,857.1.1,flip.1] (x* (y\ (z\y)))/ (z\y)= (x/ (z\y))* (z\1).
% 1125 [para_into,1003.1.1.1,1010.1.1,flip.1] ((x/ (y\1))*z)* ((y*z)\u)= (y\ ((y*x)* (u/z)))*z.
% 1126 [para_into,1005.1.1.1,1078.1.1] (x\ (x/y))\ (y\ (x\y))=x\y.
% 1127 [para_from,1126.1.1,4.1.1.2] (x\ (x/y))* (x\y)=y\ (x\y).
% 1128 [para_into,1127.1.1.1.2,857.1.1,flip.1] (x\y)\ (y\ (x\y))= (y\x)* (y\ (x\y)).
% 1129 [para_from,1127.1.1,870.1.1.2,flip.1] ((x/y)/x)*y=x* (y\ (x\y)).
% 1130 [para_into,1129.1.1,990.1.1,flip.1] (x/y)* (y\ ((x/y)\y))= (x/y)/ (y\x).
% 1131 [para_from,1129.1.1,995.1.1.1] (x* (y\ (x\y)))\x=y\ (x*y).
% 1132 [para_from,1129.1.1,1046.1.1.1.2] (x* (y* (x\ (y\x))))/x= (1/x)\ ((y/x)/y).
% 1133 [para_from,1129.1.1,974.1.2.2.1,flip.1] ((x/y)/x)\ ((x* (y\ (x\y)))\ ((x/y)/x))= (y/ (((x/y)/x)\1))\1.
% 1134 [para_from,1129.1.1,894.1.1.1] (x* (y\ (x\y)))\ (z*y)=y\ ((((x/y)/x)\z)*y).
% 1135 [para_from,1129.1.1,861.1.1.2,flip.1] ((x/y)/x)* ((((x/y)/x)\z)*y)= (z/ ((x/y)/x))* (x* (y\ (x\y))).
% 1136 [para_into,1131.1.2.2,1021.1.1] (((x/y)/x)* ((x/y)\ (((x/y)/x)\ (x/y))))\ ((x/y)/x)= (x/y)\ ((x/y)* (1/y)).
% 1137 [para_into,1131.1.2.2,960.1.1] (x* (((y*x)\x)\ (x\ ((y*x)\x))))\x= ((y*x)\x)\ ((y\1)*x).
% 1138 [para_from,1131.1.1,974.1.2.2] ((x\ (y\x))/ (y\1))\1=y\ (x\ (y*x)).
% 1139 [para_into,1031.1.1.1,2.1.1,flip.1] (1/x)* ((x*y)/z)= (y/ (x\z))/x.
% 1140 [para_into,1139.1.2,1036.1.1] (1/x)* ((x*y)/z)= (y/x)/ (z/x).
% 1141 [para_into,1034.1.1.2.1,4.1.1,flip.1] (x* ((y\z)/u))/y= (x/y)* (z/ (y*u)).
% 1142 [para_into,1035.1.1.2.2,877.1.1] x* (y* (z* (x\1)))= ((x*y)*z)/x.
% 1143 [para_from,1142.1.1,5.1.1.2] x\ (((x*y)*z)/x)=y* (z* (x\1)).
% 1144 [para_into,1143.1.1.2.1.1,873.1.1] x\ ((((x*y)/x)*z)/x)= (y* (x\1))* (z* (x\1)).
% 1145 [para_into,1143.1.1.2.1.1,4.1.1,flip.1] (x\y)* (z* (x\1))=x\ ((y*z)/x).
% 1146 [para_into,1145.1.1,1004.1.1] (x* (y\1))* ((y* (x* (y\1)))\z)=y\ (((z/ (x* (y\1)))*x)/y).
% 1147 [para_into,1145.1.2.2.1,2.1.1] (x\1)* (y* (x\1))=x\ (y/x).
% 1148 [para_into,1147.1.1.2,890.1.1,flip.1] x\ (((y/ (1/x))*x)/x)= (x\1)* (y*x).
% 1149 [para_from,1147.1.1,5.1.1.2] (x\1)\ (x\ (y/x))=y* (x\1).
% 1150 [para_into,1149.1.1.2.2,6.1.1] (x\1)\ (x\y)= (y*x)* (x\1).
% 1151 [para_into,1150.1.1,1006.1.2] (x\y)* ((y\ (x\y))\1)= (y*x)* (x\1).
% 1152 [para_into,1042.1.1.2,896.1.1] (x\y)* ((y\z)* (y\ (x\y)))= (x\ (z/y))* (x\y).
% 1153 [para_into,1057.1.2,1104.1.1] (1/ ((x/y)/x))* (x/y)=y* ((y\1)*x).
% 1154 [para_into,1059.1.1.1,2.1.1,flip.1] (1/x)* ((y*x)/y)= (x\ (y*x))/y.
% 1155 [para_into,1059.1.1,907.1.1] x/ (x* (y\ (x\y)))= (x/y)* ((x*y)/x).
% 1156 [para_into,1059.1.1,1062.1.2] (x/y)\ ((y*x)/y)= (y/x)* ((y*x)/y).
% 1158 [para_into,1060.1.1.2.1.2,967.1.1] (x\ (y*x))/ ((z* (x\ (y*z)))/z)= (((x\ (y*x))*x)/ (x\ (y*x)))/z.
% 1159 [para_into,1066.1.1.1.1,856.1.1] (1/ (x\y))* (x\z)=x\ ((x/y)*z).
% 1160 [para_into,1066.1.1.1.1,5.1.1,flip.1] x\ (((x*y)/z)*u)= (y/ (x\z))* (x\u).
% 1161 [para_into,1068.1.1,883.1.1,flip.1] x/ ((1/x)\ (y\1))= ((1/x)\y)/x.
% 1162 [para_into,1100.1.1.2.2,939.1.1,flip.1] (1/ (1/ (x/y)))* (y/ (y\x))= (x/y)* (((x/y)\1)*y).
% 1163 [para_into,1130.1.1.2,972.1.1] (x/y)* ((y\x)\1)= (x/y)/ (y\x).
% 1164 [para_from,1138.1.1,857.1.1.2,flip.1] (x\ (y\x))/ (y\1)=1/ (y\ (x\ (y*x))).
% 1165 [para_into,1148.1.1.2,6.1.1] x\ (y/ (1/x))= (x\1)* (y*x).
% 1167 [para_into,1153.1.1.1.2,938.1.1] (1/ (1/ (x/y)))* (y/ (y\x))= (y\x)* (((y\x)\1)*y).
% 1168 [para_into,1164.1.1,1116.1.1,flip.1] 1/ (x\ (y\ (x*y)))= (x*y)\ (y*x).
% 1169 [para_from,1168.1.1,1058.1.1.1.2] (x/ ((x*y)\ (y*x)))/x=1/ (x/ (y\ (x*y))).
% 1170 [para_into,962.1.1.2,7.1.1,flip.1] (x/y)* (y* (x\y))= (1/ (x/y))*x.
% 1171 [para_into,1170.1.1,861.1.1] x* ((x\y)* (y\x))= (1/ (y/x))*y.
% 1173 [para_into,1171.1.1.2.2,860.1.1,flip.1] (1/ ((x/y)/x))* (x/y)=x* ((x\ (x/y))*y).
% 1174 [para_from,1171.1.1,5.1.1.2] x\ ((1/ (y/x))*y)= (x\y)* (y\x).
% 1175 [para_into,994.1.1.2.2,4.1.1,flip.1] (1/ (x/y))* (y\x)=y/ ((y\x)\x).
% 1177 [para_from,1175.1.1,889.1.1.2] (((1/ ((x*y)/y))/y)*x)\ (y/ ((y\ (x*y))\ (x*y)))=y.
% 1178 [para_into,1028.1.1.1.1,7.1.1,flip.1] (x/y)* ((y\x)\1)= (x/ (x/y))\y.
% 1179 [para_into,1178.1.1,1163.1.1,flip.1] (x/ (x/y))\y= (x/y)/ (y\x).
% 1181 [para_into,1179.1.1.1.2,857.1.1,flip.1] (x/ (y\x))/ ((y\x)\x)= (x/y)\ (y\x).
% 1182 [para_into,1181.1.1.1,857.1.1,flip.1] (x/y)\ (y\x)=y/ ((y\x)\x).
% 1183 [para_into,1182.1.1.1,6.1.1,flip.1] x/ ((x\ (y*x))\ (y*x))=y\ (x\ (y*x)).
% 1185 [para_into,1183.1.2.2,957.1.1] x/ ((x\ ((y\1)*x))\ ((y\1)*x))= (y\1)\ ((y*x)\x).
% 1186 [para_into,1041.1.1,970.1.1,flip.1] (((1/x)*y)\z)*x=y\ (x* (z*x)).
% 1187 [para_into,1047.1.1.1,1050.1.1,flip.1] (1/x)\ (y* (z/x))= (((1/x)\y)*z)/x.
% 1188 [para_into,1187.1.1.2.2,1116.1.1,flip.1] (((1/ (x\1))\y)* (z\ (x\u)))/ (x\1)= (1/ (x\1))\ (y* ((x*z)\ (u*x))).
% 1189 [para_into,1065.1.1.2,991.1.1,flip.1] (x\y)/ (z* (x\1))=x\ ((y*x)/z).
% 1190 [para_into,1189.1.1.1,856.1.1,flip.1] x\ ((x*x)/y)=1/ (y* (x\1)).
% 1191 [para_into,1189.1.1.1,5.1.1,flip.1] x\ (((x*y)*x)/z)=y/ (z* (x\1)).
% 1192 [para_from,1189.1.1,963.1.2.1] ((x* (y\1))* ((y\z)\ (x* (y\1))))/ (x* (y\1))= (y\ ((z*y)/x))\1.
% 1193 [para_into,1071.1.1.1,970.1.1,flip.1] ((1/x)*y)\ (z/x)= (y\ (x*z))/x.
% 1194 [para_into,1077.1.2,1048.1.1] (1/x)\ (((1/x)*y)/z)= (y*x)/ (z*x).
% 1195 [para_into,1079.1.2,1122.1.1] (1/x)\ (((1/x)*y)*z)= (y* (z*x))/x.
% 1196 [para_from,1195.1.1,4.1.1.2] (1/x)* ((y* (z*x))/x)= ((1/x)*y)*z.
% 1197 [para_into,1196.1.1,916.1.1] (x\ (y* (z*x)))/x= ((1/x)*y)*z.
% 1198 [para_from,1197.1.1,1094.1.1.1] (((1/x)*y)*z)/ (u/x)= (1/x)* ((y* (z*x))/u).
% 1199 [para_into,1080.1.2,998.1.1] ((1/x)*y)\ ((1/x)*z)= (y\ (z*x))/x.
% 1200 [para_into,1084.1.2,1122.1.1] ((x/y)/x)\ ((x/y)*z)= (x* (z*y))/y.
% 1201 [para_into,1200.1.1.2,7.1.1] ((x/y)/x)\x= (x* (y*y))/y.
% 1202 [para_from,1201.1.1,857.1.1.2] x/ ((x* (y*y))/y)= (x/y)/x.
% 1203 [para_from,1202.1.1,990.1.1.1,flip.1] x/ (y\ ((x/y)* (y*y)))= (((x/y)/y)/ (x/y))*y.
% 1204 [para_into,1088.1.2,1010.1.1] (x* (y\z))/ (z\ (y\z))=y\ ((y*x)*z).
% 1205 [para_into,1204.1.1.1,4.1.1,flip.1] x\ ((x*x)*y)=y/ (y\ (x\y)).
% 1206 [para_into,1205.1.1.2,864.1.1] (x/y)\ (x* (y\ ((x/y)*y)))=y/ (y\ ((x/y)\y)).
% 1207 [para_into,1089.1.2,985.1.1] (x* (y\1))/ (z* (y\1))=y\ ((y*x)/z).
% 1208 [para_into,1124.1.2,985.1.1] (x* (y\ (z\y)))/ (z\y)=z\ ((z*x)/y).
% 1209 [para_from,1208.1.1,7.1.1.1] (x\ ((x*y)/z))* (x\z)=y* (z\ (x\z)).
% 1210 [para_from,1209.1.1,870.1.1.2,flip.1] (((x*y)/z)/x)*z=x* (y* (z\ (x\z))).
% 1211 [para_into,1210.1.1.1.1.1,4.1.1,flip.1] x* ((x\y)* (z\ (x\z)))= ((y/z)/x)*z.
% 1212 [para_from,1211.1.1,878.1.2.1] x* (((x\y)* (z\ (x\z)))/ (x\1))= (((y/z)/x)*z)*x.
% 1213 [para_into,1132.1.1,987.1.1] (((x*y)/x)/y)\1= (1/y)\ ((x/y)/x).
% 1214 [para_into,1213.1.1.1,1040.1.1,flip.1] (1/x)\ ((y/x)/y)= (y/ ((x*y)/x))\1.
% 1215 [para_into,1214.1.1,1111.1.1,flip.1] (x/ ((y*x)/y))\1= (y*x)/ (x*y).
% 1216 [para_from,1215.1.1,857.1.1.2] 1/ ((x*y)/ (y*x))=y/ ((x*y)/x).
% 1217 [para_into,1173.1.2.2,1004.1.1] (1/ ((x/y)/x))* (x/y)=x* (y* ((x*y)\x)).
% 1218 [para_into,1217.1.1,1153.1.1,flip.1] x* (y* ((x*y)\x))=y* ((y\1)*x).
% 1219 [para_from,1218.1.1,5.1.1.2] x\ (y* ((y\1)*x))=y* ((x*y)\x).
% 1220 [para_into,1219.1.1,1159.1.2] (1/ (x\y))* (x\ (((x/y)\1)*x))= (x/y)* ((x* (x/y))\x).
% 1221 [para_into,1219.1.1,896.1.1] (x\y)* (x\ (((y/x)\1)*x))= (y/x)* ((x* (y/x))\x).
% 1222 [para_into,1219.1.2.2.1,1020.1.1] x\ ((1/ (x\y))* (((1/ (x\y))\1)*x))= (1/ (x\y))* (((x/y)*x)\x).
% 1223 [para_into,983.1.1.2,5.1.1,flip.1] (x* ((y*z)/u))*y= (x*y)* (z/ (y\u)).
% 1225 [para_into,1064.1.1.1,5.1.1] ((x*y)\z)\ (y\u)=y\ ((x\ (z/y))\u).
% 1227 [para_into,1069.1.1.1,5.1.1,flip.1] x\ ((y/ (x*z))\ (x*u))= ((x\y)/z)\u.
% 1228 [para_into,1227.1.1.2.2,4.1.1,flip.1] ((x\y)/z)\ (x\u)=x\ ((y/ (x*z))\u).
% 1230 [para_into,1228.1.1.1.1,895.1.1] (((x\ (y*x))*z)/u)\ (x\w)=x\ (((y* (x*z))/ (x*u))\w).
% 1231 [para_into,1070.1.1.2.1,5.1.1,flip.1] (x/ (y*z))* (y*u)=y* (((y\x)/z)*u).
% 1233 [para_into,1075.1.1,1207.1.1] x\ ((x* (y* (x\1)))/y)= ((y*x)/y)\1.
% 1234 [para_into,1233.1.1.2.1,873.1.1] x\ (((x*y)/x)/y)= ((y*x)/y)\1.
% 1235 [para_into,1234.1.1.2,1040.1.1] x\ (x/ ((y*x)/y))= ((y*x)/y)\1.
% 1236 [para_into,1235.1.2,988.1.1] x\ (x/ ((y*x)/y))=y* (x\ (y\1)).
% 1237 [para_from,1236.1.1,4.1.1.2] x* (y* (x\ (y\1)))=x/ ((y*x)/y).
% 1238 [para_into,1237.1.1.2,1122.1.1,flip.1] (1/x)/ (((y/x)* (1/x))/ (y/x))= (1/x)* ((y* (((y/x)\1)*x))/x).
% 1239 [para_into,1237.1.2.2.1,916.1.1] (x/y)* ((1/y)* ((x/y)\ ((1/y)\1)))= (x/y)/ (((y\x)/y)/ (1/y)).
% 1240 [para_from,1237.1.1,882.1.2.1] (x*y)* ((x\ (y\1))/ (y\1))= (x/ ((y*x)/y))*y.
% 1241 [para_from,1237.1.1,1010.1.2.2.1] ((x* (y\ (x\1)))/ (y\1))* (y\z)=y\ ((y/ ((x*y)/x))*z).
% 1242 [para_into,1109.1.2,930.1.1] (1/x)\ (y/ ((1/x)*z))= (((x* (y*x))/x)/z)*x.
% 1243 [para_into,1113.1.2,1156.1.1] ((x*y)/x)\ (x* ((x*y)/x))= (x/y)* ((x*y)/x).
% 1244 [para_into,1144.1.1.2.1,862.1.1] x\ ((x* (y* (x\z)))/x)= (y* (x\1))* (z* (x\1)).
% 1245 [para_into,1203.1.2,990.1.1] x/ (y\ ((x/y)* (y*y)))= (x/y)/ (y\x).
% 1246 [para_into,1245.1.1.2.2,861.1.1] x/ (y\ (y* ((y\x)*y)))= (x/y)/ (y\x).
% 1247 [para_into,1246.1.1.2,5.1.1,flip.1] (x/y)/ (y\x)=x/ ((y\x)*y).
% 1248 [para_into,1247.1.1.2,5.1.1,flip.1] (x*y)/ ((x\ (x*y))*x)= ((x*y)/x)/y.
% 1250 [para_into,1248.1.2,1040.1.1] (x*y)/ ((x\ (x*y))*x)=x/ ((y*x)/y).
% 1251 [para_into,1250.1.1.2.1,5.1.1] (x*y)/ (y*x)=x/ ((y*x)/y).
% 1253 [para_into,1251.1.1,1215.1.2] (x/ ((y*x)/y))\1=y/ ((x*y)/x).
% 1254 [para_from,1251.1.1,1228.1.2.2.1] ((x\ (y*x))/y)\ (x\z)=x\ ((y/ ((x*y)/x))\z).
% 1255 [para_from,1251.1.1,1216.1.1.2] 1/ (x/ ((y*x)/y))=y/ ((x*y)/x).
% 1256 [para_from,1251.1.1,1027.1.1.1.2] ((x/ (y*z))/ (y/ ((z*y)/z)))* (y*z)=x/ (1/ ((y*z)\ (z*y))).
% 1257 [para_from,1251.1.1,865.1.1.1.2] (x* (y/ ((z*y)/z)))* (z*y)= (x* (z*y))* ((z*y)\ (y*z)).
% 1258 [para_from,1251.1.1,7.1.1.1] (x/ ((y*x)/y))* (y*x)=x*y.
% 1259 [para_into,1258.1.1,1039.1.1] x* ((x\ ((y*x)/y))*y)=y*x.
% 1260 [para_into,1259.1.1.2,1004.1.1] x* (y* ((x*y)\ (y*x)))=y*x.
% 1261 [para_from,1260.1.1,5.1.1.2,flip.1] x* ((y*x)\ (x*y))=y\ (x*y).
% 1262 [para_from,1261.1.1,1051.1.1.1,flip.1] x\ ((y*x)/y)= (x\ (y*x))/y.
% 1263 [para_from,1261.1.1,5.1.1.2,flip.1] (x*y)\ (y*x)=y\ (x\ (y*x)).
% 1264 [para_into,1262.1.1,968.1.2] (x\ (y*x))* (y\1)= (x\ (y*x))/y.
% 1265 [para_from,1262.1.1,4.1.1.2] x* ((x\ (y*x))/y)= (y*x)/y.
% 1266 [para_into,1263.1.1,1168.1.2] 1/ (x\ (y\ (x*y)))=y\ (x\ (y*x)).
% 1267 [para_into,1263.1.1,1116.1.2] (x\ (y\x))/ (y\1)=x\ (y\ (x*y)).
% 1268 [para_from,1263.1.1,1169.1.1.1.2] (x/ (y\ (x\ (y*x))))/x=1/ (x/ (y\ (x*y))).
% 1269 [para_from,1265.1.1,899.1.1.1.2,flip.1] x* ((y/ ((x\ (z*x))/z))* (x\u))= ((x*y)/ ((z*x)/z))*u.
% 1270 [para_from,1265.1.1,1118.1.2.1] (((x\ (y*x))/y)\ (x\1))/ (x\1)= ((y*x)/y)\x.
% 1271 [para_from,1253.1.1,1050.1.1.2.2] (x/ ((y*x)/y))* ((z* (x/ ((y*x)/y)))* (y/ ((x*y)/x)))= ((1/ (x/ ((y*x)/y)))\z)*1.
% 1272 [para_from,1264.1.1,1207.1.1.2] (x* (y\1))/ ((z\ (y*z))/y)=y\ ((y*x)/ (z\ (y*z))).
% 1273 [para_from,1264.1.1,1189.1.1.2,flip.1] x\ ((y*x)/ (z\ (x*z)))= (x\y)/ ((z\ (x*z))/x).
% 1274 [para_from,1266.1.1,1165.1.1.2.2,flip.1] ((x\ (y\ (x*y)))\1)* (z* (x\ (y\ (x*y))))= (x\ (y\ (x*y)))\ (z/ (y\ (x\ (y*x)))).
% 1276 [para_from,1267.1.1,1138.1.1.1] (x\ (y\ (x*y)))\1=y\ (x\ (y*x)).
% 1277 [para_from,1267.1.1,876.1.1.1.2] (x* (y\ (x\ (y*x))))/x=x* (y\ (x\y)).
% 1278 [para_from,1276.1.1,1161.1.1.2.2,flip.1] ((1/x)\ (y\ (z\ (y*z))))/x=x/ ((1/x)\ (z\ (y\ (z*y)))).
% 1279 [para_from,1276.1.1,901.1.1.2.2,flip.1] (x* (y\ (z\ (y*z))))/x=x/ (x* (z\ (y\ (z*y)))).
% 1281 [para_into,1277.1.1,1072.1.1] (x/y)\ ((1/y)*x)=y* (x\ (y\x)).
% 1282 [para_from,1281.1.1,870.1.1.2.2] (x/y)* (((x/y)\z)* (y* (x\ (y\x))))= (z/ (x/y))* ((1/y)*x).
% 1283 [para_into,1268.1.1.1,1055.1.1,flip.1] 1/ (x/ (y\ (x*y)))= (y\ (x*y))/x.
% 1284 [para_into,1283.1.1.2,930.1.1] 1/ (((x/y)/x)*y)= (y\ (x*y))/x.
% 1286 [para_into,1284.1.1.2,1129.1.1] 1/ (x* (y\ (x\y)))= (y\ (x*y))/x.
% 1287 [para_from,1286.1.1,864.1.1.1.1,flip.1] 1* ((x* (y\ (x\y)))\ (z* (x* (y\ (x\y)))))= (((y\ (x*y))/x)*z)* (x* (y\ (x\y))).
% 1288 [para_into,1206.1.1.2.2.2,7.1.1] (x/y)\ (x* (y\x))=y/ (y\ ((x/y)\y)).
% 1290 [para_into,1288.1.2.2,972.1.1] (x/y)\ (x* (y\x))=y/ ((y\x)\1).
% 1291 [para_into,1240.1.1.2,1118.1.1,flip.1] (x/ ((y*x)/y))*y= (x*y)* ((y*x)\y).
% 1292 [para_into,1291.1.1,991.1.1,flip.1] (x*y)* ((y*x)\y)= (x*y)/x.
% 1293 [para_from,1292.1.1,5.1.1.2] (x*y)\ ((x*y)/x)= (y*x)\y.
% 1294 [para_into,1293.1.1.1,7.1.1] x\ (((x/y)*y)/ (x/y))= (y* (x/y))\y.
% 1295 [para_into,1293.1.1.1,4.1.1,flip.1] ((x\y)*x)\ (x\y)=y\ ((x* (x\y))/x).
% 1296 [para_from,1293.1.1,1186.1.1.1,flip.1] x\ (y* ((((1/y)*x)/ (1/y))*y))= ((x* (1/y))\x)*y.
% 1297 [para_into,1294.1.1.2.1,7.1.1,flip.1] (x* (y/x))\x=y\ (y/ (y/x)).
% 1299 [para_into,1295.1.2.2.1,4.1.1] ((x\y)*x)\ (x\y)=y\ (y/x).
% 1301 [para_from,1299.1.1,988.1.2.2] ((x* ((x\y)*x))/x)\y=x* (y\ (y/x)).
% 1302 [para_into,1301.1.1.1,1046.1.1] ((1/x)\ (x\y))\y=x* (y\ (y/x)).
% 1303 [para_into,1302.1.2.2,1297.1.2] ((1/ (x/y))\ ((x/y)\x))\x= (x/y)* ((y* (x/y))\y).
% 1304 [para_into,1242.1.2.1.1,1046.1.1] (1/x)\ (y/ ((1/x)*z))= (((1/x)\y)/z)*x.
% 1305 [para_into,1243.1.1,897.1.1] x* ((x\ (x*y))\ ((x*y)/x))= (x/y)* ((x*y)/x).
% 1306 [para_into,1244.1.1,877.1.1,flip.1] (x* (y\1))* (z* (y\1))= (x* (y\z))* (y\1).
% 1307 [para_into,1270.1.1.1,1254.1.1] (x\ ((y/ ((x*y)/x))\1))/ (x\1)= ((y*x)/y)\x.
% 1308 [para_into,1273.1.1.2,930.1.1] x\ ((((y*x)/z)/x)*z)= (x\y)/ ((z\ (x*z))/x).
% 1309 [para_from,1279.1.1,862.1.1.1] (x/ (x* (y\ (z\ (y*z)))))*u=x* ((z\ (y\ (z*y)))* (x\u)).
% 1310 [para_into,1305.1.1.2.1,5.1.1,flip.1] (x/y)* ((x*y)/x)=x* (y\ ((x*y)/x)).
% 1311 [para_into,1310.1.1,1155.1.2] x/ (x* (y\ (x\y)))=x* (y\ ((x*y)/x)).
% 1313 [para_into,1311.1.2.2,1262.1.1] x/ (x* (y\ (x\y)))=x* ((y\ (x*y))/x).
% 1314 [para_from,1313.1.1,890.1.1.1.1.2] ((x/ (y* ((z\ (y*z))/y)))* (y* (z\ (y\z))))* ((y* (z\ (y\z)))\y)=x* (y* (z\ (y\z))).
% 1315 [para_into,1307.1.1.1.2,1253.1.1] (x\ (x/ ((y*x)/y)))/ (x\1)= ((y*x)/y)\x.
% 1316 [para_into,1315.1.1.1,1236.1.1] (x* (y\ (x\1)))/ (y\1)= ((x*y)/x)\y.
% 1317 [para_into,1316.1.2,988.1.1] (x* (y\ (x\1)))/ (y\1)=x* (y\ (x\y)).
% 1318 [para_into,1308.1.1,896.1.1,flip.1] (x\y)/ ((z\ (x*z))/x)= (x\ ((y*x)/z))* (x\z).
% 1319 [para_into,933.1.1.2.2,973.1.1] (x\ (y*x))* (x* (x\ (y\x)))= ((x\ (y*x))/y)*x.
% 1320 [para_into,1319.1.1.2,4.1.1] (x\ (y*x))* (y\x)= ((x\ (y*x))/y)*x.
% 1322 [para_into,996.1.1,893.1.1] 1\ ((x* ((x\ (y*x))\z))* (x\1))= (x\y)\ (z* (x\1)).
% 1323 [para_into,1073.1.1.2,865.1.1] (x/y)\ (((x/y)*y)* (y\x))= (x/ (x/y))/ ((x/y)\1).
% 1324 [para_into,1106.1.1.1.1,3.1.1] ((x/y)/ ((x/y)*y))*z= (x/y)* ((x\ (z*y))/y).
% 1325 [para_into,1324.1.1.1.2,7.1.1,flip.1] (x/y)* ((x\ (z*y))/y)= ((x/y)/x)*z.
% 1328 [para_into,1162.1.2.2,961.1.1] (1/ (1/ (x/y)))* (y/ (y\x))= (x/y)* (y* (x\y)).
% 1329 [para_into,1328.1.2,1170.1.1] (1/ (1/ (x/y)))* (y/ (y\x))= (1/ (x/y))*x.
% 1330 [para_into,1167.1.1,1329.1.1,flip.1] (x\y)* (((x\y)\1)*x)= (1/ (y/x))*y.
% 1331 [para_into,1177.1.1.1.1.1.2,6.1.1] (((1/x)/y)*x)\ (y/ ((y\ (x*y))\ (x*y)))=y.
% 1333 [para_into,1331.1.1.2,1183.1.1] (((1/x)/y)*x)\ (x\ (y\ (x*y)))=y.
% 1334 [para_into,1333.1.1,1096.1.1] x\ ((x/ (y*x))\ (y\ (x*y)))=y.
% 1335 [para_from,1333.1.1,857.1.1.2] (x\ (y\ (x*y)))/y= ((1/x)/y)*x.
% 1336 [para_from,1334.1.1,4.1.1.2,flip.1] (x/ (y*x))\ (y\ (x*y))=x*y.
% 1337 [para_from,1336.1.1,857.1.1.2] (x\ (y*x))/ (y*x)=y/ (x*y).
% 1338 [para_into,1337.1.1.1.2,7.1.1] (x\y)/ ((y/x)*x)= (y/x)/ (x* (y/x)).
% 1339 [para_into,1337.1.1,1191.1.2] x\ (((x* ((x\1)\ (y* (x\1))))*x)/y)=y/ ((x\1)*y).
% 1340 [para_from,1335.1.1,1122.1.1.1,flip.1] ((x\ (y\ (x*y)))* (z*y))/y= (((1/x)/y)*x)* ((1/y)\z).
% 1341 [para_into,1338.1.1.2,7.1.1,flip.1] (x/y)/ (y* (x/y))= (y\x)/x.
% 1343 [para_from,1341.1.1,993.1.1.1,flip.1] x/ ((x/y)/ (y\1))= ((y\x)/x)*y.
% 1344 [para_into,1343.1.1.2.1,857.1.1,flip.1] (((x\y)\y)/y)* (x\y)=y/ (x/ ((x\y)\1)).
% 1345 [para_into,1343.1.2.1.1,860.1.1] x/ ((x/ (x/y))/ ((x/y)\1))= (y/x)* (x/y).
% 1346 [para_into,1185.1.1.2.1,957.1.1] x/ (((y*x)\x)\ ((y\1)*x))= (y\1)\ ((y*x)\x).
% 1347 [para_into,1272.1.2.2,930.1.1] (x* (y\1))/ ((z\ (y*z))/y)=y\ ((((y*x)/z)/y)*z).
% 1348 [para_into,1296.1.1.2.2.1,875.1.1] x\ (y* (((1/y)* (x*y))*y))= ((x* (1/y))\x)*y.
% 1349 [para_into,1348.1.1.2.2,864.1.1] x\ (y* (1* (y\ ((x*y)*y))))= ((x* (1/y))\x)*y.
% 1350 [para_into,1349.1.1.2.2,2.1.1] x\ (y* (y\ ((x*y)*y)))= ((x* (1/y))\x)*y.
% 1351 [para_into,1350.1.1.2,4.1.1,flip.1] ((x* (1/y))\x)*y=x\ ((x*y)*y).
% 1352 [para_into,1351.1.1.1,1193.1.1,flip.1] (1/x)\ (((1/x)*y)*y)= (((1/y)\ (x*1))/x)*y.
% 1355 [para_into,1352.1.2.1.1.2,3.1.1] (1/x)\ (((1/x)*y)*y)= (((1/y)\x)/x)*y.
% 1356 [para_into,1355.1.1,1195.1.1,flip.1] (((1/x)\y)/y)*x= (x* (x*y))/y.
% 1357 [para_from,1356.1.1,6.1.1.1] ((x* (x*y))/y)/x= ((1/x)\y)/y.
% 1358 [para_into,1303.1.1.1.2,860.1.1,flip.1] (x/y)* ((y* (x/y))\y)= ((1/ (x/y))\y)\x.
% 1359 [para_into,1358.1.1,1221.1.2] (x\y)* (x\ (((y/x)\1)*x))= ((1/ (y/x))\x)\y.
% 1361 [para_into,1359.1.1.2.2,961.1.1] (x\y)* (x\ (x* (y\x)))= ((1/ (y/x))\x)\y.
% 1362 [para_into,1361.1.1.2,5.1.1,flip.1] ((1/ (x/y))\y)\x= (y\x)* (x\y).
% 1364 [para_into,1322.1.1.2.1,970.1.1] 1\ ((x\ (y*z))* (y\1))= (y\x)\ (z* (y\1)).
% 1365 [para_into,1364.1.1,855.1.1,flip.1] (x\y)\ (z* (x\1))= (y\ (x*z))* (x\1).
% 1366 [para_into,1323.1.1.2.1,7.1.1,flip.1] (x/ (x/y))/ ((x/y)\1)= (x/y)\ (x* (y\x)).
% 1368 [para_into,1366.1.2,1290.1.1] (x/ (x/y))/ ((x/y)\1)=y/ ((y\x)\1).
% 1369 [para_from,1368.1.1,1345.1.1.2] x/ (y/ ((y\x)\1))= (y/x)* (x/y).
% 1370 [para_into,1369.1.1,1344.1.2] (((x\y)\y)/y)* (x\y)= (x/y)* (y/x).
% 1371 [para_into,1369.1.2.1,901.1.1] (x* (y\1))/ (x/ ((x\ (x* (y\1)))\1))= ((x*y)/x)* ((x* (y\1))/x).
% 1372 [para_into,1339.1.1.2.1.1.2,893.1.1] x\ (((x* (1\ ((x*y)* (x\1))))*x)/y)=y/ ((x\1)*y).
% 1373 [para_into,1347.1.2,896.1.1] (x* (y\1))/ ((z\ (y*z))/y)= (y\ ((y*x)/z))* (y\z).
% 1374 [para_into,1372.1.1.2.1.1.2,855.1.1] x\ (((x* ((x*y)* (x\1)))*x)/y)=y/ ((x\1)*y).
% 1375 [para_into,1374.1.1.2.1.1,873.1.1] x\ ((((x* (x*y))/x)*x)/y)=y/ ((x\1)*y).
% 1376 [para_into,1375.1.1.2.1,7.1.1] x\ ((x* (x*y))/y)=y/ ((x\1)*y).
% 1378 [para_from,1376.1.1,879.1.1.1,flip.1] x\ (((x* (x*y))/y)/x)= (y/ ((x\1)*y))* (x\1).
% 1379 [para_into,1378.1.2,1056.1.1] x\ (((x* (x*y))/y)/x)= (x\1)* (((x\1)\y)/y).
% 1381 [para_into,1373.1.2,1209.1.1] (x* (y\1))/ ((z\ (y*z))/y)=x* (z\ (y\z)).
% 1382 [para_into,1381.1.1.1,4.1.1] 1/ ((x\ (y*x))/y)=y* (x\ (y\x)).
% 1383 [para_from,1382.1.1,7.1.1.1] (x* (y\ (x\y)))* ((y\ (x*y))/x)=1.
% 1384 [para_from,1383.1.1,895.1.1.2.2,flip.1] ((x* (y\ (x\y)))\ (z* (x* (y\ (x\y)))))* ((y\ (x*y))/x)= (x* (y\ (x\y)))\ (z*1).
% 1385 [para_from,1383.1.1,1007.1.2.1.1] ((x\ (y*x))/y)\ (((y* (x\ (y\x)))\ (z/ ((x\ (y*x))/y)))*u)= (1\z)* (((x\ (y*x))/y)\u).
% 1386 [para_from,975.1.1,862.1.1.1,flip.1] (x\ (y*x))* (z* ((x\ (y*x))\u))= ((x\ (y*x))* (z* (x\ (y\x))))*u.
% 1387 [para_into,1029.1.1.1,892.1.1] (((x\ (y*x))/y)*x)\z=x\ (y* ((x\ (y*x))\z)).
% 1388 [para_into,1387.1.1.1,1320.1.2] ((x\ (y*x))* (y\x))\z=x\ (y* ((x\ (y*x))\z)).
% 1389 [para_into,1388.1.2.2.2,1016.1.1] ((x\ (y*x))* (y\x))\z=x\ (y* (x\ (y\ (x*z)))).
% 1390 [para_into,1095.1.1.1,857.1.1,flip.1] x* ((1/ ((y/ (x\z))\1))\u)= ((x*y)/z)\ (x*u).
% 1391 [para_into,1390.1.1.2.1,857.1.1,flip.1] ((x*y)/z)\ (x*u)=x* ((y/ (x\z))\u).
% 1395 [para_into,1220.1.1.2,957.1.1] (1/ (x\y))* (((x/y)*x)\x)= (x/y)* ((x* (x/y))\x).
% 1396 [para_into,1241.1.1.1,1317.1.1,flip.1] x\ ((x/ ((y*x)/y))*z)= (y* (x\ (y\x)))* (x\z).
% 1397 [para_into,1257.1.2.2,1263.1.1] (x* (y/ ((z*y)/z)))* (z*y)= (x* (z*y))* (y\ (z\ (y*z))).
% 1398 [para_into,934.1.1.2,973.1.1] ((x\ (y*x))\ (z*x))* (x\ (y\x))= (x\ (y*x))\ ((z/y)*x).
% 1399 [para_into,1398.1.1,1045.1.1] (x\ (y\x))* ((z*x)* (x\ (y\x)))= (x\ (y*x))\ ((z/y)*x).
% 1400 [para_into,1399.1.2,1016.1.1] (x\ (y\x))* ((z*x)* (x\ (y\x)))=x\ (y\ (x* ((z/y)*x))).
% 1401 [para_into,1400.1.1,1099.1.1] ((1/ (x\ (y\x)))\z)* (y\x)=x\ (y\ (x* ((z/y)*x))).
% 1402 [para_into,1401.1.1.1.1,976.1.1,flip.1] x\ (y\ (x* ((z/y)*x)))= ((x\ (y*x))\z)* (y\x).
% 1403 [para_into,1402.1.2.1,1016.1.1] x\ (y\ (x* ((z/y)*x)))= (x\ (y\ (x*z)))* (y\x).
% 1404 [para_into,942.1.1,1030.1.1] (1/x)* ((y* (z* (y\ (x*y))))/y)= (((1/x)*y)*z)/ ((1/x)*y).
% 1405 [para_into,1090.1.1.1.2.1,883.1.1,flip.1] (x*y)/ ((z* ((1/y)*u))*y)= (x/ ((((1/y)\z)/y)*u))*y.
% 1406 [para_into,1137.1.1.1.2,1128.1.1] (x* ((x\ (y*x))* (x\ ((y*x)\x))))\x= ((y*x)\x)\ ((y\1)*x).
% 1407 [para_into,1146.1.2.2.1,1056.1.1] (x* (y\1))* ((y* (x* (y\1)))\z)=y\ ((x* ((x\z)/ (y\1)))/y).
% 1408 [para_into,1256.1.2.2.2,1263.1.1] ((x/ (y*z))/ (y/ ((z*y)/z)))* (y*z)=x/ (1/ (z\ (y\ (z*y)))).
% 1409 [para_into,1282.1.1.2,999.1.1] (x/y)* (y* ((x\ (z*y))* (x\ (y\x))))= (z/ (x/y))* ((1/y)*x).
% 1410 [para_into,1404.1.1.2,921.1.1,flip.1] (((1/x)*y)*z)/ ((1/x)*y)= (1/x)* ((1/y)\ ((z/y)*x)).
% 1411 [para_from,1410.1.1,990.1.1.1.2] ((x/ ((1/y)*z))/ ((1/y)* ((1/z)\ ((u/z)*y))))* ((1/y)*z)=x/ (((1/y)*z)\ (((1/y)*z)*u)).
% 1412 [para_into,1406.1.1.1.2,967.1.1] (x* (x\ (y* ((y*x)\x))))\x= ((y*x)\x)\ ((y\1)*x).
% 1413 [para_into,1412.1.1.1,4.1.1,flip.1] ((x*y)\y)\ ((x\1)*y)= (x* ((x*y)\y))\y.
% 1415 [para_from,1413.1.1,1346.1.1.2] x/ ((y* ((y*x)\x))\x)= (y\1)\ ((y*x)\x).
% 1416 [para_into,1415.1.1,857.1.1,flip.1] (x\1)\ ((x*y)\y)=x* ((x*y)\y).
% 1417 [para_into,1416.1.1.2.1,4.1.1,flip.1] x* ((x* (x\y))\ (x\y))= (x\1)\ (y\ (x\y)).
% 1419 [para_into,1417.1.1.2.1,4.1.1,flip.1] (x\1)\ (y\ (x\y))=x* (y\ (x\y)).
% 1421 [para_from,1419.1.1,967.1.1.2] ((x\1)\ (y* (x\1)))* (x* (z\ (x\z)))= (x\1)\ (y* (z\ (x\z))).
% 1423 [para_into,1407.1.2.2,1102.1.1] (x* (y\1))* ((y* (x* (y\1)))\z)=y\ (y* ((y\x)* (x\z))).
% 1424 [para_into,1423.1.2,5.1.1] (x* (y\1))* ((y* (x* (y\1)))\z)= (y\x)* (x\z).
% 1425 [para_into,1424.1.1.2.1,873.1.1] (x* (y\1))* (((y*x)/y)\z)= (y\x)* (x\z).
% 1427 [para_into,1425.1.1.2,860.1.1,flip.1] (x\y)* (y\ (x*y))= (y* (x\1))*x.
% 1428 [para_from,1427.1.1,888.1.1.1] ((x* (y\1))*y)/x= ((y\x)/x)*y.
% 1429 [para_from,1427.1.1,1293.1.2.1] ((x\ (y*x))* (y\x))\ (((x\ (y*x))* (y\x))/ (x\ (y*x)))= ((x* (y\1))*y)\ (y\x).
% 1430 [para_into,1428.1.1,1208.1.1,flip.1] (((x\ (y\x))\ (y\x))/ (y\x))* (x\ (y\x))=y\ ((y* ((y\x)* ((x\ (y\x))\1)))/x).
% 1431 [para_into,1408.1.2.2,1266.1.1] ((x/ (y*z))/ (y/ ((z*y)/z)))* (y*z)=x/ (y\ (z\ (y*z))).
% 1432 [para_into,1409.1.1,861.1.1] x* ((x\y)* ((y\ (z*x))* (y\ (x\y))))= (z/ (y/x))* ((1/x)*y).
% 1433 [para_into,1421.1.1.1,893.1.1] (1\ ((x*y)* (x\1)))* (x* (z\ (x\z)))= (x\1)\ (y* (z\ (x\z))).
% 1434 [para_into,1433.1.1.1,855.1.1] ((x*y)* (x\1))* (x* (z\ (x\z)))= (x\1)\ (y* (z\ (x\z))).
% 1436 [para_into,1133.1.2.1.2,948.1.1] ((x/y)/x)\ ((x* (y\ (x\y)))\ ((x/y)/x))= (y/ ((x*y)/x))\1.
% 1437 [para_into,1436.1.2,1253.1.1] ((x/y)/x)\ ((x* (y\ (x\y)))\ ((x/y)/x))=x/ ((y*x)/y).
% 1439 [para_into,1158.1.1.2,1044.1.1,flip.1] (((x\ (y*x))*x)/ (x\ (y*x)))/z= (x\ (y*x))/ ((x/z)\y).
% 1440 [para_into,1439.1.1.1,892.1.1,flip.1] (x\ (y*x))/ ((x/z)\y)= (((x\ (y*x))/y)*x)/z.
% 1441 [para_into,1440.1.2.1,1320.1.2] (x\ (y*x))/ ((x/z)\y)= ((x\ (y*x))* (y\x))/z.
% 1442 [para_into,1192.1.1.1.2,1365.1.1] ((x* (y\1))* ((z\ (y*x))* (y\1)))/ (x* (y\1))= (y\ ((z*y)/x))\1.
% 1443 [para_into,1222.1.1.2.2.1,860.1.1] x\ ((1/ (x\y))* ((x\y)*x))= (1/ (x\y))* (((x/y)*x)\x).
% 1445 [para_into,1443.1.1.2,861.1.1] x\ ((x\y)* (((x\y)\1)*x))= (1/ (x\y))* (((x/y)*x)\x).
% 1446 [para_into,1445.1.1.2,1330.1.1,flip.1] (1/ (x\y))* (((x/y)*x)\x)=x\ ((1/ (y/x))*y).
% 1447 [para_into,1446.1.2,1174.1.1] (1/ (x\y))* (((x/y)*x)\x)= (x\y)* (y\x).
% 1448 [para_into,1447.1.1,1395.1.1] (x/y)* ((x* (x/y))\x)= (x\y)* (y\x).
% 1449 [para_into,1238.1.2.2.1.2,961.1.1] (1/x)/ (((y/x)* (1/x))/ (y/x))= (1/x)* ((y* (x* (y\x)))/x).
% 1450 [para_into,1449.1.2.2,874.1.1] (1/x)/ (((y/x)* (1/x))/ (y/x))= (1/x)* ((y*x)/y).
% 1452 [para_into,1450.1.2,1154.1.1] (1/x)/ (((y/x)* (1/x))/ (y/x))= (x\ (y*x))/y.
% 1453 [para_into,1452.1.1.2,884.1.1] (1/x)/ (((y/x)*1)/ ((y/x)*x))= (x\ (y*x))/y.
% 1454 [para_into,1453.1.1.2.1,3.1.1] (1/x)/ ((y/x)/ ((y/x)*x))= (x\ (y*x))/y.
% 1455 [para_into,1454.1.1.2.2,7.1.1] (1/x)/ ((y/x)/y)= (x\ (y*x))/y.
% 1458 [para_into,1239.1.1.2.2.2,860.1.1,flip.1] (x/y)/ (((y\x)/y)/ (1/y))= (x/y)* ((1/y)* ((x/y)\y)).
% 1460 [para_into,1458.1.2.2,998.1.1] (x/y)/ (((y\x)/y)/ (1/y))= (x/y)* ((x\ (y*y))/y).
% 1461 [para_into,1460.1.2,1325.1.1] (x/y)/ (((y\x)/y)/ (1/y))= ((x/y)/x)*y.
% 1462 [para_into,1461.1.2,1129.1.1] (x/y)/ (((y\x)/y)/ (1/y))=x* (y\ (x\y)).
% 1463 [para_into,1462.1.1.2,1105.1.1] (x/y)/ ((1/y)*x)=x* (y\ (x\y)).
% 1464 [para_from,1463.1.1,1140.1.2.2] (1/ ((1/x)*y))* ((((1/x)*y)*z)/ (y/x))= (z/ ((1/x)*y))/ (y* (x\ (y\x))).
% 1465 [para_from,1463.1.1,990.1.1.1.2] ((x/ ((1/y)*z))/ (z* (y\ (z\y))))* ((1/y)*z)=x/ (((1/y)*z)\ (z/y)).
% 1466 [para_into,1371.1.1.2.2.1,5.1.1] (x* (y\1))/ (x/ ((y\1)\1))= ((x*y)/x)* ((x* (y\1))/x).
% 1468 [para_into,1466.1.1,932.1.1,flip.1] ((x*y)/x)* ((x* (y\1))/x)= (x/ ((y\1)*x))* (y\1).
% 1470 [para_into,1468.1.2,1056.1.1] ((x*y)/x)* ((x* (y\1))/x)= (y\1)* (((y\1)\x)/x).
% 1471 [para_into,1470.1.1,989.1.1,flip.1] (x\1)* (((x\1)\y)/y)= ((y*x)* (x\1))/y.
% 1472 [para_into,1471.1.1,1379.1.2] x\ (((x* (x*y))/y)/x)= ((y*x)* (x\1))/y.
% 1473 [para_into,1472.1.1.2,1357.1.1] x\ (((1/x)\y)/y)= ((y*x)* (x\1))/y.
% 1474 [para_into,1386.1.1.2.2,1016.1.1] (x\ (y*x))* (z* (x\ (y\ (x*u))))= ((x\ (y*x))* (z* (x\ (y\x))))*u.
% 1476 [para_into,1442.1.1.1,1306.1.1] ((x* (y\ (z\ (y*x))))* (y\1))/ (x* (y\1))= (y\ ((z*y)/x))\1.
% 1477 [para_into,1476.1.1,1207.1.1] x\ ((x* (y* (x\ (z\ (x*y)))))/y)= (x\ ((z*x)/y))\1.
% 1478 [para_into,1477.1.1.2,1123.1.1] x\ ((((x*y)/x)/y)* ((z/y)\x))= (x\ ((z*x)/y))\1.
% 1479 [para_into,1478.1.1.2.1,1040.1.1] x\ ((x/ ((y*x)/y))* ((z/y)\x))= (x\ ((z*x)/y))\1.
% 1480 [para_into,1479.1.1,1396.1.1] (x* (y\ (x\y)))* (y\ ((z/x)\y))= (y\ ((z*y)/x))\1.
% 1481 [para_into,1086.1.1.2.2.2.1.2,1016.1.1] x\ (y* (x* ((1/ (x\ (y\ (x*z))))\u)))= ((x\ (y*x))/z)\ ((x\ (y*x))*u).
% 1482 [para_into,1097.1.1.1,1112.1.1,flip.1] ((x*y)/x)* (((y\ (x*y))/x)\z)= ((y* (z*x))/ (x*y))* ((x*y)/x).
% 1483 [para_into,1482.1.1,862.1.1,flip.1] ((x* (y*z))/ (z*x))* ((z*x)/z)=z* (x* (z\ (((x\ (z*x))/z)\y))).
% 1485 [para_into,1188.1.2.1,857.1.1] (((1/ (x\1))\y)* (z\ (x\u)))/ (x\1)=x\ (y* ((x*z)\ (u*x))).
% 1486 [para_into,1485.1.1.1.1.1,857.1.1] ((x\y)* (z\ (x\u)))/ (x\1)=x\ (y* ((x*z)\ (u*x))).
% 1489 [para_from,1486.1.1,1212.1.1.2] x* (x\ (y* ((x*z)\ (z*x))))= (((y/z)/x)*z)*x.
% 1490 [para_into,1489.1.1.2.2.2,1263.1.1] x* (x\ (y* (z\ (x\ (z*x)))))= (((y/z)/x)*z)*x.
% 1491 [para_into,1490.1.1,4.1.1,flip.1] (((x/y)/z)*y)*z=x* (y\ (z\ (y*z))).
% 1492 [para_into,1491.1.1,864.1.1] (x/y)* (z\ (y*z))=x* (y\ (z\ (y*z))).
% 1494 [para_into,1492.1.1.1,6.1.1,flip.1] (x*y)* (y\ (z\ (y*z)))=x* (z\ (y*z)).
% 1496 [para_from,1492.1.1,1160.1.1.2] x\ ((x*y)* (z\ (u\ (z*u))))= (y/ (x\z))* (x\ (u\ (z*u))).
% 1497 [para_from,1492.1.1,1193.1.1.1] (1* (x\ (y\ (x*y))))\ (z/x)= ((y\ (x*y))\ (x*z))/x.
% 1498 [para_from,1494.1.1,1050.1.1.2,flip.1] ((1/x)\y)* (z\ (x*z))=x* (y* (z\ (x*z))).
% 1499 [para_from,1494.1.1,5.1.1.2] (x*y)\ (x* (z\ (y*z)))=y\ (z\ (y*z)).
% 1500 [para_into,1499.1.1,1117.1.1] (x\1)/ ((y\ (x*y))\1)=x\ (y\ (x*y)).
% 1501 [para_from,1499.1.1,891.1.1.2.2] (x*y)\ (((x*y)* (x*y))* (y\ (z\ (y*z))))= ((x* (z\ (y*z)))/ (x*y))/ ((x*y)\1).
% 1502 [para_from,1499.1.1,1343.1.2.1.1] (x* (y\ (z*y)))/ (((x* (y\ (z*y)))/ (x*z))/ ((x*z)\1))= ((z\ (y\ (z*y)))/ (x* (y\ (z*y))))* (x*z).
% 1503 [para_into,1500.1.1.2,973.1.1] (x\1)/ (y\ (x\y))=x\ (y\ (x*y)).
% 1504 [para_from,1503.1.1,1325.1.1.1] (x\ (y\ (x*y)))* (((x\1)\ (z* (y\ (x\y))))/ (y\ (x\y)))= (((x\1)/ (y\ (x\y)))/ (x\1))*z.
% 1506 [para_into,1497.1.1.1,2.1.1] (x\ (y\ (x*y)))\ (z/x)= ((y\ (x*y))\ (x*z))/x.
% 1508 [para_into,1465.1.2.2,1193.1.1] ((x/ ((1/y)*z))/ (z* (y\ (z\y))))* ((1/y)*z)=x/ ((z\ (y*z))/y).
% 1509 [para_into,1481.1.1.2.2,1026.1.1,flip.1] ((x\ (y*x))/z)\ ((x\ (y*x))*u)=x\ (y* ((x/ (y\ (x*z)))\ (x*u))).
% 1510 [para_into,1464.1.1.2,1198.1.1] (1/ ((1/x)*y))* ((1/x)* ((y* (z*x))/y))= (z/ ((1/x)*y))/ (y* (x\ (y\x))).
% 1511 [para_into,1510.1.1,1231.1.1] (1/x)* ((((1/x)\1)/y)* ((y* (z*x))/y))= (z/ ((1/x)*y))/ (y* (x\ (y\x))).
% 1512 [para_into,1511.1.1.2.1.1,860.1.1,flip.1] (x/ ((1/y)*z))/ (z* (y\ (z\y)))= (1/y)* ((y/z)* ((z* (x*y))/z)).
% 1514 [para_into,1512.1.2.2,989.1.1] (x/ ((1/y)*z))/ (z* (y\ (z\y)))= (1/y)* ((y* (x*y))/z).
% 1515 [para_into,1514.1.2,1140.1.1] (x/ ((1/y)*z))/ (z* (y\ (z\y)))= ((x*y)/y)/ (z/y).
% 1516 [para_into,1515.1.2.1,6.1.1] (x/ ((1/y)*z))/ (z* (y\ (z\y)))=x/ (z/y).
% 1518 [para_from,1516.1.1,1508.1.1.1] (x/ (y/z))* ((1/z)*y)=x/ ((y\ (z*y))/z).
% 1519 [para_into,1518.1.1,1432.1.2] x* ((x\y)* ((y\ (z*x))* (y\ (x\y))))=z/ ((y\ (x*y))/x).
% 1520 [para_into,1519.1.1.2,1152.1.1] x* ((x\ ((y*x)/z))* (x\z))=y/ ((z\ (x*z))/x).
% 1521 [para_into,1520.1.1,870.1.1,flip.1] x/ ((y\ (z*y))/z)= (((x*z)/y)/z)*y.
% 1522 [para_into,1521.1.2.1,1040.1.1] x/ ((y\ (z*y))/z)= (x/ ((z*y)/z))*y.
% 1523 [para_into,1522.1.1,1381.1.1,flip.1] ((x* (y\1))/ ((y*z)/y))*z=x* (z\ (y\z)).
% 1524 [para_from,1522.1.1,1269.1.1.2.1] x* (((y/ ((z*x)/z))*x)* (x\u))= ((x*y)/ ((z*x)/z))*u.
% 1525 [para_from,1522.1.1,7.1.1.1] ((x/ ((y*z)/y))*z)* ((z\ (y*z))/y)=x.
% 1526 [para_into,1525.1.1.1.1,6.1.1] (x*y)* ((y\ (z*y))/z)=x* ((z*y)/z).
% 1527 [para_into,1526.1.1.1,7.1.1,flip.1] (x/y)* ((z*y)/z)=x* ((y\ (z*y))/z).
% 1528 [para_into,1527.1.1,1059.1.2] (x* (y\ (z*y)))/z=x* ((y\ (z*y))/z).
% 1532 [para_into,1524.1.1,1050.1.1] ((1/x)\ (y/ ((z*x)/z)))*u= ((x*y)/ ((z*x)/z))*u.
% 1533 [para_into,1532.1.1.1,1112.1.1] ((x* (y*z))/ (z*x))*u= ((x*y)/ ((z*x)/z))*u.
% 1534 [para_into,1533.1.1,1483.1.1,flip.1] ((x*y)/ ((z*x)/z))* ((z*x)/z)=z* (x* (z\ (((x\ (z*x))/z)\y))).
% 1535 [para_into,1534.1.1,7.1.1,flip.1] x* (y* (x\ (((y\ (x*y))/x)\z)))=y*z.
% 1536 [para_into,1136.1.1.1.2.2,860.1.1] (((x/y)/x)* ((x/y)\x))\ ((x/y)/x)= (x/y)\ ((x/y)* (1/y)).
% 1538 [para_into,1536.1.1.1.2,860.1.1] (((x/y)/x)*y)\ ((x/y)/x)= (x/y)\ ((x/y)* (1/y)).
% 1540 [para_into,1538.1.1.1,1129.1.1] (x* (y\ (x\y)))\ ((x/y)/x)= (x/y)\ ((x/y)* (1/y)).
% 1541 [para_into,1540.1.2,5.1.1] (x* (y\ (x\y)))\ ((x/y)/x)=1/y.
% 1543 [para_from,1541.1.1,1437.1.1.2] ((x/y)/x)\ (1/y)=x/ ((y*x)/y).
% 1545 [para_from,1543.1.1,990.1.2.2] ((x/ ((y/z)/y))/ ((1/z)/ ((y/z)/y)))* ((y/z)/y)=x/ (y/ ((z*y)/z)).
% 1552 [para_into,1545.1.1.1.2,1455.1.1] ((x/ ((y/z)/y))/ ((z\ (y*z))/y))* ((y/z)/y)=x/ (y/ ((z*y)/z)).
% 1553 [para_into,1552.1.1.1,1522.1.1] (((x/ ((y/z)/y))/ ((y*z)/y))*z)* ((y/z)/y)=x/ (y/ ((z*y)/z)).
% 1554 [para_into,1274.1.1.1,1276.1.1,flip.1] (x\ (y\ (x*y)))\ (z/ (y\ (x\ (y*x))))= (y\ (x\ (y*x)))* (z* (x\ (y\ (x*y)))).
% 1555 [para_into,1554.1.1.2,6.1.1,flip.1] (x\ (y\ (x*y)))* ((z* (x\ (y\ (x*y))))* (y\ (x\ (y*x))))= (y\ (x\ (y*x)))\z.
% 1556 [para_into,1287.1.1,2.1.1] (x* (y\ (x\y)))\ (z* (x* (y\ (x\y))))= (((y\ (x*y))/x)*z)* (x* (y\ (x\y))).
% 1557 [para_into,1384.1.1.1,1556.1.1] ((((x\ (y*x))/y)*z)* (y* (x\ (y\x))))* ((x\ (y*x))/y)= (y* (x\ (y\x)))\ (z*1).
% 1558 [para_into,1429.1.1.2,930.1.1] ((x\ (y*x))* (y\x))\ (((((x\ (y*x))* (y\x))/x)/y)*x)= ((x* (y\1))*y)\ (y\x).
% 1559 [para_into,1430.1.2.2.1.2,1151.1.1] (((x\ (y\x))\ (y\x))/ (y\x))* (x\ (y\x))=y\ ((y* ((x*y)* (y\1)))/x).
% 1560 [para_into,1559.1.2.2.1,873.1.1] (((x\ (y\x))\ (y\x))/ (y\x))* (x\ (y\x))=y\ (((y* (x*y))/y)/x).
% 1561 [para_into,1560.1.2.2.1,1046.1.1] (((x\ (y\x))\ (y\x))/ (y\x))* (x\ (y\x))=y\ (((1/y)\x)/x).
% 1562 [para_into,1561.1.2,1473.1.1] (((x\ (y\x))\ (y\x))/ (y\x))* (x\ (y\x))= ((x*y)* (y\1))/x.
% 1563 [para_into,1562.1.1,1370.1.1] (x/ (y\x))* ((y\x)/x)= ((x*y)* (y\1))/x.
% 1564 [para_into,1563.1.1.1,857.1.1,flip.1] ((x*y)* (y\1))/x=y* ((y\x)/x).
% 1565 [para_into,1564.1.1,1473.1.2] x\ (((1/x)\y)/y)=x* ((x\y)/y).
% 1567 [para_into,1501.1.1,1496.1.1] ((x*y)/ ((x*y)\y))* ((x*y)\ (z\ (y*z)))= ((x* (z\ (y*z)))/ (x*y))/ ((x*y)\1).
% 1568 [para_into,1557.1.2.2,3.1.1] ((((x\ (y*x))/y)*z)* (y* (x\ (y\x))))* ((x\ (y*x))/y)= (y* (x\ (y\x)))\z.
% 1569 [para_into,1558.1.1.2.1.1,1441.1.2] ((x\ (y*x))* (y\x))\ ((((x\ (y*x))/ ((x/x)\y))/y)*x)= ((x* (y\1))*y)\ (y\x).
% 1570 [para_into,1567.1.1.1,1002.1.1] ((x/ (x\ (y/y)))*y)* ((x*y)\ (z\ (y*z)))= ((x* (z\ (y*z)))/ (x*y))/ ((x*y)\1).
% 1571 [para_into,1569.1.1.2.1.1.2.1,859.1.1] ((x\ (y*x))* (y\x))\ ((((x\ (y*x))/ (1\y))/y)*x)= ((x* (y\1))*y)\ (y\x).
% 1573 [para_into,1571.1.1.2.1.1.2,855.1.1] ((x\ (y*x))* (y\x))\ ((((x\ (y*x))/y)/y)*x)= ((x* (y\1))*y)\ (y\x).
% 1574 [para_into,1573.1.1,1389.1.1] x\ (y* (x\ (y\ (x* ((((x\ (y*x))/y)/y)*x)))))= ((x* (y\1))*y)\ (y\x).
% 1575 [para_into,1574.1.1.2.2,1403.1.1] x\ (y* ((x\ (y\ (x* ((x\ (y*x))/y))))* (y\x)))= ((x* (y\1))*y)\ (y\x).
% 1576 [para_into,1575.1.1.2.2.1.2.2,1265.1.1] x\ (y* ((x\ (y\ ((y*x)/y)))* (y\x)))= ((x* (y\1))*y)\ (y\x).
% 1577 [para_into,1576.1.1.2.2.1.2,877.1.1] x\ (y* ((x\ (x* (y\1)))* (y\x)))= ((x* (y\1))*y)\ (y\x).
% 1578 [para_into,1577.1.1.2.2.1,5.1.1,flip.1] ((x* (y\1))*y)\ (y\x)=x\ (y* ((y\1)* (y\x))).
% 1580 [para_into,1578.1.2.2,870.1.1] ((x* (y\1))*y)\ (y\x)=x\ ((1/y)*x).
% 1581 [para_into,1580.1.2,1052.1.1] ((x* (y\1))*y)\ (y\x)= (x\1)/ (x\y).
% 1584 [para_into,1570.1.1.1.1.2.2,859.1.1,flip.1] ((x* (y\ (z*y)))/ (x*z))/ ((x*z)\1)= ((x/ (x\1))*z)* ((x*z)\ (y\ (z*y))).
% 1586 [para_into,1584.1.2,1125.1.1] ((x* (y\ (z*y)))/ (x*z))/ ((x*z)\1)= (x\ ((x*x)* ((y\ (z*y))/z)))*z.
% 1587 [para_into,1271.1.2.1.1,1255.1.1] (x/ ((y*x)/y))* ((z* (x/ ((y*x)/y)))* (y/ ((x*y)/x)))= ((y/ ((x*y)/x))\z)*1.
% 1588 [para_into,1587.1.2,3.1.1] (x/ ((y*x)/y))* ((z* (x/ ((y*x)/y)))* (y/ ((x*y)/x)))= (y/ ((x*y)/x))\z.
% 1589 [para_into,1314.1.1.1,1231.1.1] (x* (((x\y)/ ((z\ (x*z))/x))* (z\ (x\z))))* ((x* (z\ (x\z)))\x)=y* (x* (z\ (x\z))).
% 1590 [para_into,1589.1.1.1.2.1,1318.1.1] (x* (((x\ ((y*x)/z))* (x\z))* (z\ (x\z))))* ((x* (z\ (x\z)))\x)=y* (x* (z\ (x\z))).
% 1591 [para_into,1590.1.1.1.2,1074.1.1] (x* (((x\ ((y*x)/z))* (x\1))* (x\z)))* ((x* (z\ (x\z)))\x)=y* (x* (z\ (x\z))).
% 1592 [para_into,1591.1.1.1.2.1,879.1.1] (x* ((x\ (((y*x)/z)/x))* (x\z)))* ((x* (z\ (x\z)))\x)=y* (x* (z\ (x\z))).
% 1593 [para_into,1592.1.1.1.2.1.2,1040.1.1] (x* ((x\ (y/ ((x*z)/x)))* (x\z)))* ((x* (z\ (x\z)))\x)=y* (x* (z\ (x\z))).
% 1594 [para_into,1593.1.1.1,870.1.1] (((x/ ((y*z)/y))/y)*z)* ((y* (z\ (y\z)))\y)=x* (y* (z\ (y\z))).
% 1595 [para_into,1594.1.1.2,1131.1.1] (((x/ ((y*z)/y))/y)*z)* (z\ (y*z))=x* (y* (z\ (y\z))).
% 1596 [para_into,1595.1.1,9.1.1] (((x/ ((y*z)/y))/y)*y)*z=x* (y* (z\ (y\z))).
% 1597 [para_into,1596.1.1.1,7.1.1] (x/ ((y*z)/y))*z=x* (y* (z\ (y\z))).
% 1599 [para_into,1597.1.1,1523.1.1,flip.1] (x* (y\1))* (y* (z\ (y\z)))=x* (z\ (y\z)).
% 1600 [para_from,1597.1.1,1553.1.1.1] ((x/ ((y/z)/y))* (y* (z\ (y\z))))* ((y/z)/y)=x/ (y/ ((z*y)/z)).
% 1601 [para_from,1597.1.1,1525.1.1.1] (x* (y* (z\ (y\z))))* ((z\ (y*z))/y)=x.
% 1602 [para_into,1601.1.1.1,7.1.1,flip.1] x/ (y* (z\ (y\z)))=x* ((z\ (y*z))/y).
% 1603 [para_into,1601.1.1,1568.1.1] (x* (y\ (x\y)))\z= ((y\ (x*y))/x)*z.
% 1606 [para_from,1602.1.1,1190.1.1.2] x\ ((x*x)* ((y\ (z*y))/z))=1/ ((z* (y\ (z\y)))* (x\1)).
% 1609 [para_from,1603.1.1,1004.1.1.1] (((x\ (y*x))/y)* (z/u))*u=u* (((y* (x\ (y\x)))*u)\z).
% 1610 [para_from,1603.1.1,1448.1.2.1] ((x* (y\ (x\y)))/z)* (((x* (y\ (x\y)))* ((x* (y\ (x\y)))/z))\ (x* (y\ (x\y))))= (((y\ (x*y))/x)*z)* (z\ (x* (y\ (x\y)))).
% 1611 [para_into,1599.1.1,1434.1.1] (x\1)\ (y* (z\ (x\z)))= (x*y)* (z\ (x\z)).
% 1613 [para_into,1609.1.1,865.1.1] (((x\ (y*x))/y)*z)* (z\u)=z* (((y* (x\ (y\x)))*z)\u).
% 1615 [para_into,1600.1.1.1,1135.1.2] (((x/y)/x)* ((((x/y)/x)\z)*y))* ((x/y)/x)=z/ (x/ ((y*x)/y)).
% 1617 [para_into,1615.1.1,1101.1.1] x* (y/ (((z/y)/z)\1))=x/ (z/ ((y*z)/y)).
% 1618 [para_into,1617.1.1.2.2,948.1.1,flip.1] x/ (y/ ((z*y)/z))=x* (z/ ((y*z)/y)).
% 1619 [para_into,1618.1.1,6.1.1,flip.1] (x* (y/ ((z*y)/z)))* (z/ ((y*z)/y))=x.
% 1620 [para_from,1618.1.1,1431.1.1.1] ((x/ (y*z))* (z/ ((y*z)/y)))* (y*z)=x/ (y\ (z\ (y*z))).
% 1621 [para_from,1619.1.1,1588.1.1.2,flip.1] (x/ ((y*x)/y))\z= (y/ ((x*y)/x))*z.
% 1623 [para_into,1620.1.1,1397.1.1] ((x/ (y*z))* (y*z))* (z\ (y\ (z*y)))=x/ (y\ (z\ (y*z))).
% 1624 [para_into,1623.1.1.1,7.1.1,flip.1] x/ (y\ (z\ (y*z)))=x* (z\ (y\ (z*y))).
% 1626 [para_into,1624.1.1,6.1.1,flip.1] (x* (y\ (z\ (y*z))))* (z\ (y\ (z*y)))=x.
% 1627 [para_from,1624.1.1,1194.1.1.2] (1/x)\ (((1/x)*y)* (z\ (u\ (z*u))))= (y*x)/ ((u\ (z\ (u*z)))*x).
% 1628 [para_from,1624.1.1,948.1.1.1.1] ((x* (y\ (z\ (y*z))))/x)\1= (x* (z\ (y\ (z*y))))/x.
% 1629 [para_from,1626.1.1,1555.1.1.2,flip.1] (x\ (y\ (x*y)))\z= (y\ (x\ (y*x)))*z.
% 1630 [para_from,1626.1.1,900.1.2.1] x/ ((y* (z\ (u\ (z*u))))* ((u\ (z\ (u*z)))\ ((y* (z\ (u\ (z*u))))\x)))=y/ (y* (z\ (u\ (z*u)))).
% 1633 [para_into,1629.1.1,1506.1.1] ((x\ (y*x))\ (y*z))/y= (x\ (y\ (x*y)))* (z/y).
% 1634 [para_from,1629.1.1,1004.1.1.1] ((x\ (y\ (x*y)))* (z/u))*u=u* (((y\ (x\ (y*x)))*u)\z).
% 1635 [para_from,1629.1.1,857.1.1.2] x/ ((y\ (z\ (y*z)))*x)=z\ (y\ (z*y)).
% 1636 [para_from,1635.1.1,1194.1.1.2,flip.1] (x*y)/ (((z\ (u\ (z*u)))* ((1/y)*x))*y)= (1/y)\ (u\ (z\ (u*z))).
% 1637 [para_from,1635.1.1,1049.1.1.1,flip.1] 1/ ((1/x)\ (y\ (z\ (y*z))))= (z\ (y\ (z*y)))/x.
% 1638 [para_into,1633.1.1.1,1016.1.1] (x\ (y\ (x* (y*z))))/y= (x\ (y\ (x*y)))* (z/y).
% 1639 [para_into,1638.1.1.1.2,895.1.1] (x\ ((y\ (x*y))*z))/y= (x\ (y\ (x*y)))* (z/y).
% 1640 [para_into,1628.1.1.1,1279.1.1] (x/ (x* (y\ (z\ (y*z)))))\1= (x* (y\ (z\ (y*z))))/x.
% 1641 [para_into,1640.1.2,1279.1.1] (x/ (x* (y\ (z\ (y*z)))))\1=x/ (x* (z\ (y\ (z*y)))).
% 1642 [para_into,1634.1.1,865.1.1] ((x\ (y\ (x*y)))*z)* (z\u)=z* (((y\ (x\ (y*x)))*z)\u).
% 1643 [para_into,1627.1.1,1195.1.1] (x* ((y\ (z\ (y*z)))*u))/u= (x*u)/ ((z\ (y\ (z*y)))*u).
% 1649 [para_into,1385.1.1.2.1.2,1522.1.1] ((x\ (y*x))/y)\ (((y* (x\ (y\x)))\ ((z/ ((y*x)/y))*x))*u)= (1\z)* (((x\ (y*x))/y)\u).
% 1650 [para_into,1504.1.1.2.1,1611.1.1] (x\ (y\ (x*y)))* (((x*z)* (y\ (x\y)))/ (y\ (x\y)))= (((x\1)/ (y\ (x\y)))/ (x\1))*z.
% 1651 [para_into,1650.1.1.2,6.1.1,flip.1] (((x\1)/ (y\ (x\y)))/ (x\1))*z= (x\ (y\ (x*y)))* (x*z).
% 1652 [para_into,1651.1.1.1.1,1503.1.1] ((x\ (y\ (x*y)))/ (x\1))*z= (x\ (y\ (x*y)))* (x*z).
% 1654 [para_into,1652.1.1.1,881.1.1,flip.1] (x\ (y\ (x*y)))* (x*z)= (x\ ((y\ (x*y))*x))*z.
% 1655 [para_into,1654.1.2,967.1.1] (x\ (y\ (x*y)))* (x* (x\z))=x\ ((y\ (x*y))*z).
% 1656 [para_into,1655.1.1.2,4.1.1,flip.1] x\ ((y\ (x*y))*z)= (x\ (y\ (x*y)))*z.
% 1658 [para_into,1656.1.1.2,967.1.1,flip.1] (x\ (y\ (x*y)))* (y\z)=x\ (y\ (x*z)).
% 1659 [para_from,1656.1.1,1639.1.1.1] ((x\ (y\ (x*y)))*z)/y= (x\ (y\ (x*y)))* (z/y).
% 1660 [para_from,1656.1.1,1000.1.1.1.2] (x* ((y\ (z\ (y*z)))*u))/u= (x/u)* ((y/u)\ (z\ (y*z))).
% 1661 [para_from,1656.1.1,1012.1.1.1] ((x\ (y\ (x*y)))*z)\ (x\u)=x\ ((((y\ (x*y))*z)/x)\u).
% 1662 [para_into,1659.1.1,1340.1.1,flip.1] (x\ (y\ (x*y)))* ((z*y)/y)= (((1/x)/y)*x)* ((1/y)\z).
% 1663 [para_into,1660.1.1,1643.1.1] (x*y)/ ((z\ (u\ (z*u)))*y)= (x/y)* ((u/y)\ (z\ (u*z))).
% 1664 [para_into,1660.1.1,1046.1.1,flip.1] (x/x)* ((y/x)\ (z\ (y*z)))= (1/x)\ (y\ (z\ (y*z))).
% 1665 [para_into,1664.1.1.1,859.1.1,flip.1] (1/x)\ (y\ (z\ (y*z)))=1* ((y/x)\ (z\ (y*z))).
% 1667 [para_into,1665.1.2,2.1.1] (1/x)\ (y\ (z\ (y*z)))= (y/x)\ (z\ (y*z)).
% 1668 [para_into,1667.1.1,1636.1.2] (x*y)/ (((z\ (u\ (z*u)))* ((1/y)*x))*y)= (u/y)\ (z\ (u*z)).
% 1669 [para_from,1667.1.1,1637.1.1.2] 1/ ((x/y)\ (z\ (x*z)))= (z\ (x\ (z*x)))/y.
% 1670 [para_from,1667.1.1,1278.1.1.1,flip.1] x/ ((1/x)\ (y\ (z\ (y*z))))= ((z/x)\ (y\ (z*y)))/x.
% 1671 [para_from,1667.1.1,1362.1.1.1] ((x/ (y/ (x\ (z\ (x*z)))))\ (z\ (x*z)))\y= ((x\ (z\ (x*z)))\y)* (y\ (x\ (z\ (x*z)))).
% 1672 [para_from,1667.1.1,1565.1.1.2.1] x\ (((y/x)\ (z\ (y*z)))/ (y\ (z\ (y*z))))=x* ((x\ (y\ (z\ (y*z))))/ (y\ (z\ (y*z)))).
% 1673 [para_from,1667.1.1,1581.1.2.2] (((1/x)* ((y\ (z\ (y*z)))\1))* (y\ (z\ (y*z))))\ ((y\ (z\ (y*z)))\ (1/x))= ((1/x)\1)/ ((y/x)\ (z\ (y*z))).
% 1674 [para_into,1670.1.1.2,1667.1.1,flip.1] ((x/y)\ (z\ (x*z)))/y=y/ ((z/y)\ (x\ (z*x))).
% 1675 [para_into,1662.1.1.2,6.1.1,flip.1] (((1/x)/y)*x)* ((1/y)\z)= (x\ (y\ (x*y)))*z.
% 1677 [para_into,1668.1.1,1405.1.1] (x/ ((((1/y)\ (z\ (u\ (z*u))))/y)*x))*y= (u/y)\ (z\ (u*z)).
% 1678 [para_into,1677.1.1.1.2.1.1,1667.1.1] (x/ ((((y/z)\ (u\ (y*u)))/z)*x))*z= (u/z)\ (y\ (u*y)).
% 1679 [para_into,1678.1.1.1.2.1,1674.1.1] (x/ ((y/ ((z/y)\ (u\ (z*u))))*x))*y= (z/y)\ (u\ (z*u)).
% 1681 [para_into,1671.1.1.1.1.2,1624.1.1] ((x/ (y* (z\ (x\ (z*x)))))\ (z\ (x*z)))\y= ((x\ (z\ (x*z)))\y)* (y\ (x\ (z\ (x*z)))).
% 1682 [para_into,1672.1.1.2,1624.1.1] x\ (((y/x)\ (z\ (y*z)))* (z\ (y\ (z*y))))=x* ((x\ (y\ (z\ (y*z))))/ (y\ (z\ (y*z)))).
% 1683 [para_into,1681.1.2.1,1629.1.1] ((x/ (y* (z\ (x\ (z*x)))))\ (z\ (x*z)))\y= ((z\ (x\ (z*x)))*y)* (y\ (x\ (z\ (x*z)))).
% 1684 [para_into,1681.1.2.2,1667.1.1] ((x/ ((1/y)* (z\ (x\ (z*x)))))\ (z\ (x*z)))\ (1/y)= ((x\ (z\ (x*z)))\ (1/y))* ((x/y)\ (z\ (x*z))).
% 1685 [para_into,1682.1.1,1008.1.1] (x\ ((y\ (x*y))*z))* (z\ (y\ (x\ (y*x))))=z* ((z\ (x\ (y\ (x*y))))/ (x\ (y\ (x*y)))).
% 1686 [para_into,1683.1.2,1642.1.1] ((x/ (y* (z\ (x\ (z*x)))))\ (z\ (x*z)))\y=y* (((x\ (z\ (x*z)))*y)\ (x\ (z\ (x*z)))).
% 1687 [para_into,1685.1.1.1,1656.1.1] ((x\ (y\ (x*y)))*z)* (z\ (y\ (x\ (y*x))))=z* ((z\ (x\ (y\ (x*y))))/ (x\ (y\ (x*y)))).
% 1688 [para_into,1686.1.2.2,1661.1.1] ((x/ (y* (z\ (x\ (z*x)))))\ (z\ (x*z)))\y=y* (x\ ((((z\ (x*z))*y)/x)\ (z\ (x*z)))).
% 1689 [para_into,1687.1.1,1642.1.1] x* (((y\ (z\ (y*z)))*x)\ (y\ (z\ (y*z))))=x* ((x\ (z\ (y\ (z*y))))/ (z\ (y\ (z*y)))).
% 1690 [para_into,1688.1.2.2.2,1230.1.1] ((x/ (y* (z\ (x\ (z*x)))))\ (z\ (x*z)))\y=y* (x\ (z\ (((x* (z*y))/ (z*x))\ (x*z)))).
% 1691 [para_into,1689.1.1.2,1661.1.1] x* (y\ ((((z\ (y*z))*x)/y)\ (z\ (y*z))))=x* ((x\ (z\ (y\ (z*y))))/ (z\ (y\ (z*y)))).
% 1692 [para_into,1690.1.2.2.2.2,1391.1.1] ((x/ (y* (z\ (x\ (z*x)))))\ (z\ (x*z)))\y=y* (x\ (z\ (x* (((z*y)/ (x\ (z*x)))\z)))).
% 1693 [para_into,1691.1.1.2.2,1230.1.1] x* (y\ (z\ (((y* (z*x))/ (z*y))\ (y*z))))=x* ((x\ (z\ (y\ (z*y))))/ (z\ (y\ (z*y)))).
% 1694 [para_into,1692.1.2.2.2.2.2.1,930.1.1] ((x/ (y* (z\ (x\ (z*x)))))\ (z\ (x*z)))\y=y* (x\ (z\ (x* (((((z*y)/x)/z)*x)\z)))).
% 1695 [para_into,1693.1.1.2.2.2,1391.1.1] x* (y\ (z\ (y* (((z*x)/ (y\ (z*y)))\z))))=x* ((x\ (z\ (y\ (z*y))))/ (z\ (y\ (z*y)))).
% 1696 [para_into,1694.1.2.2.2.2.2.1,1210.1.1] ((x/ (y* (z\ (x\ (z*x)))))\ (z\ (x*z)))\y=y* (x\ (z\ (x* ((z* (y* (x\ (z\x))))\z)))).
% 1697 [para_into,1695.1.1.2.2.2.2.1,930.1.1] x* (y\ (z\ (y* (((((z*x)/y)/z)*y)\z))))=x* ((x\ (z\ (y\ (z*y))))/ (z\ (y\ (z*y)))).
% 1698 [para_into,1697.1.1.2.2.2.2.1,1210.1.1] x* (y\ (z\ (y* ((z* (x* (y\ (z\y))))\z))))=x* ((x\ (z\ (y\ (z*y))))/ (z\ (y\ (z*y)))).
% 1699 [para_into,1698.1.2.2,1624.1.1] x* (y\ (z\ (y* ((z* (x* (y\ (z\y))))\z))))=x* ((x\ (z\ (y\ (z*y))))* (y\ (z\ (y*z)))).
% 1700 [para_into,1649.1.1.2.1,1134.1.1] ((x\ (y*x))/y)\ ((x\ ((((y/x)/y)\ (z/ ((y*x)/y)))*x))*u)= (1\z)* (((x\ (y*x))/y)\u).
% 1701 [para_into,1700.1.1.2.1.2.1,1061.1.1] ((x\ (y*x))/y)\ ((x\ (((y* ((y/x)\ ((z*y)/x)))/y)*x))*u)= (1\z)* (((x\ (y*x))/y)\u).
% 1702 [para_into,1701.1.1.2.1.2.1.1.2,1062.1.1] ((x\ (y*x))/y)\ ((x\ (((y* ((x* (y\ (z*y)))/x))/y)*x))*u)= (1\z)* (((x\ (y*x))/y)\u).
% 1703 [para_into,1702.1.1.2.1.2.1.1.2,907.1.1] ((x\ (y*x))/y)\ ((x\ (((y* (x/ (x* (y\ (z\y)))))/y)*x))*u)= (1\z)* (((x\ (y*x))/y)\u).
% 1704 [para_into,1703.1.1.2.1.2,862.1.1] ((x\ (y*x))/y)\ ((x\ (y* ((x/ (x* (y\ (z\y))))* (y\x))))*u)= (1\z)* (((x\ (y*x))/y)\u).
% 1705 [para_into,1704.1.1.2.1.2.2,1107.1.1] ((x\ (y*x))/y)\ ((x\ (y* (x* ((y\ (z*y))* (x\ (y\x))))))*u)= (1\z)* (((x\ (y*x))/y)\u).
% 1706 [para_into,1705.1.1.2.1,895.1.1] ((x\ (y*x))/y)\ (((x\ (y*x))* ((y\ (z*y))* (x\ (y\x))))*u)= (1\z)* (((x\ (y*x))/y)\u).
% 1707 [para_into,1706.1.1.2,1474.1.2] ((x\ (y*x))/y)\ ((x\ (y*x))* ((y\ (z*y))* (x\ (y\ (x*u)))))= (1\z)* (((x\ (y*x))/y)\u).
% 1708 [para_into,1707.1.1,1509.1.1] x\ (y* ((x/ (y\ (x*y)))\ (x* ((y\ (z*y))* (x\ (y\ (x*u)))))))= (1\z)* (((x\ (y*x))/y)\u).
% 1709 [para_into,1708.1.1.2.2.1,930.1.1] x\ (y* ((((x/y)/x)*y)\ (x* ((y\ (z*y))* (x\ (y\ (x*u)))))))= (1\z)* (((x\ (y*x))/y)\u).
% 1710 [para_into,1709.1.1.2.2.1,1129.1.1] x\ (y* ((x* (y\ (x\y)))\ (x* ((y\ (z*y))* (x\ (y\ (x*u)))))))= (1\z)* (((x\ (y*x))/y)\u).
% 1711 [para_into,1710.1.1.2.2,1119.1.1] x\ (y* (x* (((x*y)\ (y*x))\ ((y\ (z*y))* (x\ (y\ (x*u)))))))= (1\z)* (((x\ (y*x))/y)\u).
% 1712 [para_into,1711.1.1.2.2.2.1,1263.1.1] x\ (y* (x* ((y\ (x\ (y*x)))\ ((y\ (z*y))* (x\ (y\ (x*u)))))))= (1\z)* (((x\ (y*x))/y)\u).
% 1713 [para_into,1712.1.1.2.2.2,1053.1.1] x\ (y* (x* (y\ (((x\ (y*x))/y)\ (z* (y* (x\ (y\ (x*u)))))))))= (1\z)* (((x\ (y*x))/y)\u).
% 1714 [para_into,1713.1.1.2,1535.1.1] x\ (x* (y* (z* (x\ (z\ (x*u))))))= (1\y)* (((x\ (z*x))/z)\u).
% 1716 [para_into,1714.1.1,5.1.1,flip.1] (1\x)* (((y\ (z*y))/z)\u)=x* (z* (y\ (z\ (y*u)))).
% 1717 [para_into,1716.1.1.1,855.1.1] x* (((y\ (z*y))/z)\u)=x* (z* (y\ (z\ (y*u)))).
% 1719 [para_from,1717.1.1,5.1.1.2] x\ (x* (y* (z\ (y\ (z*u)))))= ((z\ (y*z))/y)\u.
% 1720 [para_into,1719.1.1,5.1.1,flip.1] ((x\ (y*x))/y)\z=y* (x\ (y\ (x*z))).
% 1721 [para_from,1720.1.1,1082.1.1.2.1] 1/ ((x* (y\ (x\ (y* (z*z)))))/z)= (1/z)* ((y\ (x*y))/x).
% 1722 [para_from,1720.1.1,966.1.2.1] x* (((y\ (x*y))\x)* (x\z))= (x* (y\ (x\ (y*1))))*z.
% 1723 [para_into,1722.1.1.2.1,1016.1.1] x* ((y\ (x\ (y*x)))* (x\z))= (x* (y\ (x\ (y*1))))*z.
% 1724 [para_into,1723.1.1.2,1658.1.1,flip.1] (x* (y\ (x\ (y*1))))*z=x* (y\ (x\ (y*z))).
% 1725 [para_into,1724.1.1.1.2.2.2,3.1.1] (x* (y\ (x\y)))*z=x* (y\ (x\ (y*z))).
% 1726 [para_into,1725.1.2.2.2.2,4.1.1] (x* (y\ (x\y)))* (y\z)=x* (y\ (x\z)).
% 1727 [para_from,1725.1.1,1613.1.2.2.1] (((x\ (y*x))/y)*z)* (z\u)=z* ((y* (x\ (y\ (x*z))))\u).
% 1728 [para_from,1725.1.1,1606.1.2.2] x\ ((x*x)* ((y\ (z*y))/z))=1/ (z* (y\ (z\ (y* (x\1))))).
% 1729 [para_from,1725.1.1,1083.1.1.1] (x* (y\ (x\ (y* (z*z)))))/ (1/ (((x* (y\ (x\y)))*z)\ (x* (y\ (x\y)))))= (x* (y\ (x\y)))*z.
% 1731 [para_into,1726.1.1,1480.1.1,flip.1] x* (y\ (x\ ((z/x)\y)))= (y\ ((z*y)/x))\1.
% 1732 [para_into,1726.1.1,1396.1.2] x\ ((x/ ((y*x)/y))*z)=y* (x\ (y\z)).
% 1734 [para_from,1732.1.1,4.1.1.2,flip.1] (x/ ((y*x)/y))*z=x* (y* (x\ (y\z))).
% 1737 [para_into,1734.1.1,1621.1.2] (x/ ((y*x)/y))\z=y* (x* (y\ (x\z))).
% 1738 [para_from,1737.1.1,1054.1.1.2] x\ (y* (x* (y\ (x\ (x*z)))))= (1/ (x\ ((y*x)/y)))\z.
% 1739 [para_into,1738.1.1.2.2.2.2,5.1.1,flip.1] (1/ (x\ ((y*x)/y)))\z=x\ (y* (x* (y\z))).
% 1741 [para_into,1739.1.2,895.1.1] (1/ (x\ ((y*x)/y)))\z= (x\ (y*x))* (y\z).
% 1742 [para_into,1741.1.1.1.2,1262.1.1] (1/ ((x\ (y*x))/y))\z= (x\ (y*x))* (y\z).
% 1743 [para_into,1742.1.1.1,1382.1.1] (x* (y\ (x\y)))\z= (y\ (x*y))* (x\z).
% 1745 [para_from,1743.1.1,990.1.2.2] ((x/ (y* (z\ (y\z))))/ (u/ (y* (z\ (y\z)))))* (y* (z\ (y\z)))=x/ ((z\ (y*z))* (y\u)).
% 1748 [para_into,1721.1.1.2,1121.1.1] 1/ ((x/y)* (((z\ (x*z))/y)\y))= (1/y)* ((z\ (x*z))/x).
% 1750 [para_into,1745.1.1.1.1,1602.1.1] ((x* ((y\ (z*y))/z))/ (u/ (z* (y\ (z\y)))))* (z* (y\ (z\y)))=x/ ((y\ (z*y))* (z\u)).
% 1751 [para_into,1750.1.1.1.2,1602.1.1] ((x* ((y\ (z*y))/z))/ (u* ((y\ (z*y))/z)))* (z* (y\ (z\y)))=x/ ((y\ (z*y))* (z\u)).
% 1752 [para_into,1729.1.1.2.2.1,1725.1.1] (x* (y\ (x\ (y* (z*z)))))/ (1/ ((x* (y\ (x\ (y*z))))\ (x* (y\ (x\y)))))= (x* (y\ (x\y)))*z.
% 1759 [para_into,1411.1.1,1231.1.1] (1/x)* ((((1/x)\ (y/ ((1/x)*z)))/ ((1/z)\ ((u/z)*x)))*z)=y/ (((1/x)*z)\ (((1/x)*z)*u)).
% 1760 [para_into,1630.1.1.2.2,1629.1.1] x/ ((y* (z\ (u\ (z*u))))* ((z\ (u\ (z*u)))* ((y* (z\ (u\ (z*u))))\x)))=y/ (y* (z\ (u\ (z*u)))).
% 1761 [para_into,1759.1.1.2.1.1,1304.1.1] (1/x)* ((((((1/x)\y)/z)*x)/ ((1/z)\ ((u/z)*x)))*z)=y/ (((1/x)*z)\ (((1/x)*z)*u)).
% 1762 [para_into,1761.1.1.2,1048.1.1] (1/x)* ((((((1/x)\y)/z)*x)*z)/ (((u/z)*x)*z))=y/ (((1/x)*z)\ (((1/x)*z)*u)).
% 1763 [para_into,1762.1.1.2.1,864.1.1] (1/x)* ((((1/x)\y)* (z\ (x*z)))/ (((u/z)*x)*z))=y/ (((1/x)*z)\ (((1/x)*z)*u)).
% 1764 [para_into,1763.1.1.2.1,1498.1.1] (1/x)* ((x* (y* (z\ (x*z))))/ (((u/z)*x)*z))=y/ (((1/x)*z)\ (((1/x)*z)*u)).
% 1765 [para_into,1764.1.1.2.2,864.1.1] (1/x)* ((x* (y* (z\ (x*z))))/ (u* (z\ (x*z))))=y/ (((1/x)*z)\ (((1/x)*z)*u)).
% 1766 [para_into,1765.1.1,1140.1.1] ((x* (y\ (z*y)))/z)/ ((u* (y\ (z*y)))/z)=x/ (((1/z)*y)\ (((1/z)*y)*u)).
% 1767 [para_into,1766.1.1.1,1528.1.1] (x* ((y\ (z*y))/z))/ ((u* (y\ (z*y)))/z)=x/ (((1/z)*y)\ (((1/z)*y)*u)).
% 1768 [para_into,1767.1.1.2,1528.1.1] (x* ((y\ (z*y))/z))/ (u* ((y\ (z*y))/z))=x/ (((1/z)*y)\ (((1/z)*y)*u)).
% 1769 [para_into,1768.1.2.2,5.1.1] (x* ((y\ (z*y))/z))/ (u* ((y\ (z*y))/z))=x/u.
% 1771 [para_from,1769.1.1,1751.1.1.1,flip.1] x/ ((y\ (z*y))* (z\u))= (x/u)* (z* (y\ (z\y))).
% 1772 [para_into,1771.1.1.2.1,1199.1.1,flip.1] (x/y)* ((1/z)* (((1/z)*u)\ ((1/z)\ ((1/z)*u))))=x/ (((u\ (((1/z)*u)*z))/z)* ((1/z)\y)).
% 1785 [para_into,1760.1.1.2,1076.1.1] x/ (((y/ (y* (z\ (u\ (z*u)))))\1)*x)=y/ (y* (z\ (u\ (z*u)))).
% 1786 [para_into,1785.1.1.2.1,1641.1.1] x/ ((y/ (y* (z\ (u\ (z*u)))))*x)=y/ (y* (u\ (z\ (u*z)))).
% 1787 [para_into,1772.1.2.2.1.1.2,864.1.1] (x/y)* ((1/z)* (((1/z)*u)\ ((1/z)\ ((1/z)*u))))=x/ (((u\ (1* (z\ (u*z))))/z)* ((1/z)\y)).
% 1788 [para_into,1787.1.2.2.1.1.2,2.1.1] (x/y)* ((1/z)* (((1/z)*u)\ ((1/z)\ ((1/z)*u))))=x/ (((u\ (z\ (u*z)))/z)* ((1/z)\y)).
% 1789 [para_into,1788.1.2.2.1,1335.1.1] (x/y)* ((1/z)* (((1/z)*u)\ ((1/z)\ ((1/z)*u))))=x/ ((((1/u)/z)*u)* ((1/z)\y)).
% 1790 [para_into,1789.1.2.2,1675.1.1] (x/y)* ((1/z)* (((1/z)*u)\ ((1/z)\ ((1/z)*u))))=x/ ((u\ (z\ (u*z)))*y).
% 1791 [para_into,1790.1.1.2.2.2,5.1.1] (x/y)* ((1/z)* (((1/z)*u)\u))=x/ ((u\ (z\ (u*z)))*y).
% 1793 [para_into,1791.1.1.2.2,937.1.1] (x/y)* ((1/z)* (u\ (z*u)))=x/ ((u\ (z\ (u*z)))*y).
% 1794 [para_into,1793.1.1.2,1492.1.1] (x/y)* (1* (z\ (u\ (z*u))))=x/ ((u\ (z\ (u*z)))*y).
% 1795 [para_into,1794.1.1.2,2.1.1,flip.1] x/ ((y\ (z\ (y*z)))*u)= (x/u)* (z\ (y\ (z*y))).
% 1798 [para_into,1673.1.1.1.1.2,1276.1.1] (((1/x)* (y\ (z\ (y*z))))* (z\ (y\ (z*y))))\ ((z\ (y\ (z*y)))\ (1/x))= ((1/x)\1)/ ((z/x)\ (y\ (z*y))).
% 1799 [para_into,1798.1.1.1,1626.1.1] (1/x)\ ((y\ (z\ (y*z)))\ (1/x))= ((1/x)\1)/ ((y/x)\ (z\ (y*z))).
% 1801 [para_into,1799.1.1.2,1629.1.1] (1/x)\ ((y\ (z\ (y*z)))* (1/x))= ((1/x)\1)/ ((z/x)\ (y\ (z*y))).
% 1803 [para_into,1610.1.1.2.1,1725.1.1] ((x* (y\ (x\y)))/z)* ((x* (y\ (x\ (y* ((x* (y\ (x\y)))/z)))))\ (x* (y\ (x\y))))= (((y\ (x*y))/x)*z)* (z\ (x* (y\ (x\y)))).
% 1804 [para_into,1803.1.1.2,1119.1.1] ((x* (y\ (x\y)))/z)* (x* (((x*y)\ ((y* ((x* (y\ (x\y)))/z))*x))\ (y\ (x\y))))= (((y\ (x*y))/x)*z)* (z\ (x* (y\ (x\y)))).
% 1805 [para_into,1804.1.1.2.2.1.2,1223.1.1] ((x* (y\ (x\y)))/z)* (x* (((x*y)\ ((y*x)* ((y\ (x\y))/ (x\z))))\ (y\ (x\y))))= (((y\ (x*y))/x)*z)* (z\ (x* (y\ (x\y)))).
% 1806 [para_into,1805.1.1.2.2,1225.1.1] ((x* (y\ (x\y)))/z)* (x* (y\ ((x\ (((y*x)* ((y\ (x\y))/ (x\z)))/y))\ (x\y))))= (((y\ (x*y))/x)*z)* (z\ (x* (y\ (x\y)))).
% 1807 [para_into,1806.1.1.2.2.2.1.2,1141.1.1] ((x* (y\ (x\y)))/z)* (x* (y\ ((x\ (((y*x)/y)* ((x\y)/ (y* (x\z)))))\ (x\y))))= (((y\ (x*y))/x)*z)* (z\ (x* (y\ (x\y)))).
% 1808 [para_into,1807.1.1.2.2.2.1.2,862.1.1] ((x* (y\ (x\y)))/z)* (x* (y\ ((x\ (y* (x* (y\ ((x\y)/ (y* (x\z)))))))\ (x\y))))= (((y\ (x*y))/x)*z)* (z\ (x* (y\ (x\y)))).
% 1809 [para_into,1808.1.1.2.2.2,1012.1.1] ((x* (y\ (x\y)))/z)* (x* (y\ (x\ (((y* (x* (y\ ((x\y)/ (y* (x\z))))))/x)\y))))= (((y\ (x*y))/x)*z)* (z\ (x* (y\ (x\y)))).
% 1810 [para_into,1809.1.1.2,1731.1.1] ((x* (y\ (x\y)))/z)* ((y\ (((y* (x* (y\ ((x\y)/ (y* (x\z))))))*y)/x))\1)= (((y\ (x*y))/x)*z)* (z\ (x* (y\ (x\y)))).
% 1811 [para_into,1810.1.1.2.1.2.1,886.1.1] ((x* (y\ (x\y)))/z)* ((y\ (((y*x)* (y\ (((x\y)/ (y* (x\z)))*y)))/x))\1)= (((y\ (x*y))/x)*z)* (z\ (x* (y\ (x\y)))).
% 1812 [para_into,1811.1.1.2.1.2.1.2.2,1056.1.1] ((x* (y\ (x\y)))/z)* ((y\ (((y*x)* (y\ (y* ((y\ (x\y))/ (x\z)))))/x))\1)= (((y\ (x*y))/x)*z)* (z\ (x* (y\ (x\y)))).
% 1813 [para_into,1812.1.1.2.1.2.1.2,5.1.1] ((x* (y\ (x\y)))/z)* ((y\ (((y*x)* ((y\ (x\y))/ (x\z)))/x))\1)= (((y\ (x*y))/x)*z)* (z\ (x* (y\ (x\y)))).
% 1815 [para_into,1813.1.1.2.1.2,1031.1.1] ((x* (y\ (x\y)))/z)* ((y\ (((y*x)/x)* ((x* (y\ (x\y)))/z)))\1)= (((y\ (x*y))/x)*z)* (z\ (x* (y\ (x\y)))).
% 1816 [para_into,1815.1.1.2.1.2.1,6.1.1] ((x* (y\ (x\y)))/z)* ((y\ (y* ((x* (y\ (x\y)))/z)))\1)= (((y\ (x*y))/x)*z)* (z\ (x* (y\ (x\y)))).
% 1818 [para_into,1816.1.1.2.1,5.1.1] ((x* (y\ (x\y)))/z)* (((x* (y\ (x\y)))/z)\1)= (((y\ (x*y))/x)*z)* (z\ (x* (y\ (x\y)))).
% 1820 [para_into,1818.1.1,4.1.1,flip.1] (((x\ (y*x))/y)*z)* (z\ (y* (x\ (y\x))))=1.
% 1821 [para_into,1820.1.1,1727.1.1] x* ((y* (z\ (y\ (z*x))))\ (y* (z\ (y\z))))=1.
% 1822 [para_from,1821.1.1,5.1.1.2,flip.1] (x* (y\ (x\ (y*z))))\ (x* (y\ (x\y)))=z\1.
% 1823 [para_from,1822.1.1,1752.1.1.2.2] (x* (y\ (x\ (y* (z*z)))))/ (1/ (z\1))= (x* (y\ (x\y)))*z.
% 1826 [para_into,1823.1.1.2,857.1.1] (x* (y\ (x\ (y* (z*z)))))/z= (x* (y\ (x\y)))*z.
% 1828 [para_into,1826.1.1,1121.1.1] (x/y)* (((z\ (x*z))/y)\y)= (x* (z\ (x\z)))*y.
% 1829 [para_into,1828.1.2,1725.1.1] (x/y)* (((z\ (x*z))/y)\y)=x* (z\ (x\ (z*y))).
% 1830 [para_from,1829.1.1,1748.1.1.2] 1/ (x* (y\ (x\ (y*z))))= (1/z)* ((y\ (x*y))/x).
% 1831 [para_into,1830.1.1,1728.1.2] x\ ((x*x)* ((y\ (z*y))/z))= (1/ (x\1))* ((y\ (z*y))/z).
% 1832 [para_into,1831.1.2.1,857.1.1] x\ ((x*x)* ((y\ (z*y))/z))=x* ((y\ (z*y))/z).
% 1834 [para_from,1832.1.1,1586.1.2.1] ((x* (y\ (z*y)))/ (x*z))/ ((x*z)\1)= (x* ((y\ (z*y))/z))*z.
% 1835 [para_into,1834.1.2,865.1.1] ((x* (y\ (z*y)))/ (x*z))/ ((x*z)\1)= (x*z)* (z\ (y\ (z*y))).
% 1836 [para_into,1835.1.2,1494.1.1] ((x* (y\ (z*y)))/ (x*z))/ ((x*z)\1)=x* (y\ (z*y)).
% 1837 [para_from,1836.1.1,1502.1.1.2,flip.1] ((x\ (y\ (x*y)))/ (z* (y\ (x*y))))* (z*x)= (z* (y\ (x*y)))/ (z* (y\ (x*y))).
% 1838 [para_into,1837.1.2,859.1.1] ((x\ (y\ (x*y)))/ (z* (y\ (x*y))))* (z*x)=1.
% 1839 [para_into,1838.1.1,1231.1.1] x* (((x\ (y\ (z\ (y*z))))/ (z\ (y*z)))*y)=1.
% 1841 [para_into,1839.1.1.2.1,930.1.1] x* (((((x\ (y\ (z\ (y*z))))/z)/y)*z)*y)=1.
% 1842 [para_into,1841.1.1.2,1491.1.1] x* ((x\ (y\ (z\ (y*z))))* (z\ (y\ (z*y))))=1.
% 1843 [para_into,1842.1.1,1699.1.2] x* (y\ (z\ (y* ((z* (x* (y\ (z\y))))\z))))=1.
% 1844 [para_into,1843.1.1,1696.1.2] ((x/ (y* (z\ (x\ (z*x)))))\ (z\ (x*z)))\y=1.
% 1846 [para_into,1844.1.1,1684.1.1] ((x\ (y\ (x*y)))\ (1/z))* ((x/z)\ (y\ (x*y)))=1.
% 1849 [para_into,1846.1.1.1,1629.1.1] ((x\ (y\ (x*y)))* (1/z))* ((y/z)\ (x\ (y*x)))=1.
% 1850 [para_from,1849.1.1,6.1.1.1] 1/ ((x/y)\ (z\ (x*z)))= (z\ (x\ (z*x)))* (1/y).
% 1851 [para_into,1850.1.1,1669.1.1,flip.1] (x\ (y\ (x*y)))* (1/z)= (x\ (y\ (x*y)))/z.
% 1852 [para_from,1851.1.1,1801.1.1.2,flip.1] ((1/x)\1)/ ((y/x)\ (z\ (y*z)))= (1/x)\ ((z\ (y\ (z*y)))/x).
% 1853 [para_into,1852.1.2,920.1.1] ((1/x)\1)/ ((y/x)\ (z\ (y*z)))= (x* (z\ (y\ (z*y))))/x.
% 1854 [para_into,1853.1.2,1279.1.1] ((1/x)\1)/ ((y/x)\ (z\ (y*z)))=x/ (x* (y\ (z\ (y*z)))).
% 1855 [para_into,1854.1.1.1,860.1.1] x/ ((y/x)\ (z\ (y*z)))=x/ (x* (y\ (z\ (y*z)))).
% 1857 [para_from,1855.1.1,1679.1.1.1.2.1] (x/ ((y/ (y* (z\ (u\ (z*u)))))*x))*y= (z/y)\ (u\ (z*u)).
% 1859 [para_into,1857.1.1.1,1786.1.1] (x/ (x* (y\ (z\ (y*z)))))*x= (z/x)\ (y\ (z*y)).
% 1860 [para_into,1859.1.1,1309.1.1] x* ((y\ (z\ (y*z)))* (x\x))= (y/x)\ (z\ (y*z)).
% 1861 [para_into,1860.1.1.2.2,856.1.1] x* ((y\ (z\ (y*z)))*1)= (y/x)\ (z\ (y*z)).
% 1863 [para_into,1861.1.1.2,3.1.1,flip.1] (x/y)\ (z\ (x*z))=y* (x\ (z\ (x*z))).
% 1864 [para_from,1863.1.1,1663.1.2.2] (x*y)/ ((z\ (u\ (z*u)))*y)= (x/y)* (y* (u\ (z\ (u*z)))).
% 1866 [para_into,1864.1.2,861.1.1] (x*y)/ ((z\ (u\ (z*u)))*y)=y* ((y\x)* (u\ (z\ (u*z)))).
% 1867 [para_into,1866.1.1,1795.1.1] ((x*y)/y)* (z\ (u\ (z*u)))=y* ((y\x)* (z\ (u\ (z*u)))).
% 1868 [para_into,1867.1.1.1,6.1.1,flip.1] x* ((x\y)* (z\ (u\ (z*u))))=y* (z\ (u\ (z*u))).
% 1870 [para_into,1868.1.1.2.1,5.1.1,flip.1] (x*y)* (z\ (u\ (z*u)))=x* (y* (z\ (u\ (z*u)))).
% 1871 [para_into,1870.1.2.2.2,1263.1.2] (x*y)* (z\ (u\ (z*u)))=x* (y* ((u*z)\ (z*u))).
% 1872 [para_into,1871.1.1.2,1263.1.2] (x*y)* ((z*u)\ (u*z))=x* (y* ((z*u)\ (u*z))).
% 1873 [binary,1872.1,11.1] $F.
% 
% ------------ end of proof -------------