% Length of proof is 58. Level of proof is 32. % % ---------------- PROOF ---------------- % % 9 [] f(x,y,x)=x. % 10 [] f(y,x,x)=x. % 11 [] f(x,y,z)=f(x,z,y). % 12 [] f(x,y,z)=f(y,x,z). % 13 [] f(x,y,z)=f(z,x,y). % 14 [] f(x,y,z)=f(z,y,x). % 15 [] f(x,y,z)=f(y,z,x). % 16 [] f(f(x,w,y),w,z)=f(x,w,f(y,w,z)) # label("associativity"). % 17 [] f(X,f(Y,U,V),f(Z,U,V))!=f(f(X,Y,Z),U,V)|$ANS("Distributivity (short)"). % 637 [para_into,11.1.1.1,10.1.2] f(f(x,y,y),z,u)=f(y,u,z). % 644 [para_into,11.1.1.2,9.1.1,flip.1] f(x,y,f(z,u,z))=f(x,z,y). % 716 [para_from,13.1.1,12.1.2.3,flip.1] f(x,y,f(z,u,w))=f(y,x,f(u,w,z)). % 717 [para_from,13.1.1,12.1.1.3,flip.1] f(x,y,f(z,u,w))=f(y,x,f(w,z,u)). % 822 [para_into,16.1.1.1,9.1.1,flip.1] f(x,y,f(x,y,z))=f(x,y,z). % 1003 [para_into,637.1.1,11.1.2] f(f(x,y,y),z,u)=f(y,z,u). % 1342 [para_into,822.1.1,15.1.2] f(f(x,y,z),x,y)=f(x,y,z). % 1458 [para_from,822.1.2,10.1.1.3] f(x,f(y,z,u),f(y,z,f(y,z,u)))=f(y,z,u). % 2209 [para_from,1342.1.1,12.1.1.2,flip.1] f(f(f(x,y,z),x,y),u,w)=f(u,f(x,y,z),w). % 2300 [para_into,716.1.1.2,15.1.2,flip.1] f(f(x,y,z),u,f(w,w5,w6))=f(u,f(z,x,y),f(w6,w,w5)). % 2825 [para_into,1458.1.1.3,11.1.2] f(x,f(y,z,u),f(y,f(y,z,u),z))=f(y,z,u). % 3257 [para_into,2209.1.1,16.1.1] f(f(x,y,z),x,f(y,x,u))=f(x,f(x,y,z),u). % 4061 [para_into,3257.1.1.3.3,14.1.2] f(f(x,y,z),x,f(y,x,f(u,w,w5)))=f(x,f(x,y,z),f(w5,w,u)). % 5020 [para_into,4061.1.1.3,12.1.2] f(f(x,y,z),x,f(x,y,f(u,w,w5)))=f(x,f(x,y,z),f(w5,w,u)). % 5361 [para_into,5020.1.1.3,16.1.2] f(f(x,y,z),x,f(f(x,y,u),y,w))=f(x,f(x,y,z),f(w,y,u)). % 5676 [para_into,5361.1.1,717.1.1] f(x,f(x,y,z),f(u,f(x,y,w),y))=f(x,f(x,y,z),f(u,y,w)). % 6268 [para_into,5676.1.1,16.1.2] f(f(x,f(x,y,z),u),f(x,y,z),y)=f(x,f(x,y,z),f(u,y,z)). % 6472 [para_into,6268.1.1.1,14.1.2] f(f(x,f(y,z,u),y),f(y,z,u),z)=f(y,f(y,z,u),f(x,z,u)). % 6774 [para_into,6472.1.1,16.1.1] f(x,f(y,z,u),f(y,f(y,z,u),z))=f(y,f(y,z,u),f(x,z,u)). % 7035 [para_into,6774.1.1,2825.1.1,flip.1] f(x,f(x,y,z),f(u,y,z))=f(x,y,z). % 7333 [para_into,7035.1.1.2,15.1.2] f(x,f(y,x,z),f(u,z,y))=f(x,z,y). % 7443 [para_into,7035.1.1,2300.1.2] f(f(x,y,z),z,f(x,y,u))=f(z,x,y). % 7586 [para_into,7035.1.2,9.1.2,flip.1] f(f(x,y,z),u,f(x,y,z))=f(x,f(x,y,z),f(w,y,z)). % 8117 [para_into,7333.1.1,15.1.2] f(f(x,y,z),u,f(z,u,y))=f(u,y,z). % 10261 [para_into,7586.1.2,15.1.1,flip.1] f(f(x,y,z),f(u,y,z),x)=f(f(x,y,z),w,f(x,y,z)). % 10264 [para_into,7586.1.2,11.1.2] f(f(x,y,z),u,f(x,y,z))=f(x,f(w,y,z),f(x,y,z)). % 10328 [para_from,7586.1.1,1003.1.1.1] f(f(x,f(x,y,z),f(u,y,z)),w,w5)=f(f(x,y,z),w,w5). % 11178 [para_from,10264.1.1,644.1.1.3] f(x,y,f(z,f(u,w,w5),f(z,w,w5)))=f(x,f(z,w,w5),y). % 11352 [para_into,10328.1.1.1.2,7035.1.2] f(f(x,f(x,f(x,y,z),f(u,y,z)),f(w,y,z)),w5,w6)=f(f(x,y,z),w5,w6). % 12006 [para_into,11178.1.1,16.1.2] f(f(x,f(y,z,u),w),f(y,z,u),f(w,z,u))=f(x,f(w,z,u),f(y,z,u)). % 13204 [para_into,11352.1.1.1,12.1.2] f(f(f(x,f(x,y,z),f(u,y,z)),x,f(w,y,z)),w5,w6)=f(f(x,y,z),w5,w6). % 13390 [para_into,12006.1.1.1,11.1.2] f(f(x,y,f(z,u,w)),f(z,u,w),f(y,u,w))=f(x,f(y,u,w),f(z,u,w)). % 13677 [para_into,13204.1.1.1.1,7586.1.2] f(f(f(f(x,y,z),u,f(x,y,z)),x,f(w,y,z)),w5,w6)=f(f(x,y,z),w5,w6). % 14091 [para_into,13390.1.2,15.1.2] f(f(x,y,f(z,u,w)),f(z,u,w),f(y,u,w))=f(f(z,u,w),x,f(y,u,w)). % 14246 [para_into,13677.1.1.1,11.1.2] f(f(f(f(x,y,z),u,f(x,y,z)),f(w,y,z),x),w5,w6)=f(f(x,y,z),w5,w6). % 14699 [para_into,14091.1.1.1,15.1.2] f(f(f(x,y,z),u,w),f(x,y,z),f(w,y,z))=f(f(x,y,z),u,f(w,y,z)). % 15059 [para_into,14246.1.1,16.1.1] f(f(f(x,y,z),u,f(x,y,z)),f(w,y,z),f(x,f(w,y,z),w5))=f(f(x,y,z),f(w,y,z),w5). % 15470 [para_into,14699.1.1.1,7443.1.2] f(f(f(x,y,f(z,u,w)),f(z,u,w),f(x,y,w5)),f(z,u,w),f(y,u,w))=f(f(z,u,w),x,f(y,u,w)). % 15716 [para_into,15059.1.1.1,10261.1.2] f(f(f(x,y,z),f(u,y,z),x),f(w,y,z),f(x,f(w,y,z),w5))=f(f(x,y,z),f(w,y,z),w5). % 15832 [para_into,15716.1.1,8117.1.1,flip.1] f(f(x,y,z),f(u,y,z),f(w,y,z))=f(f(u,y,z),f(w,y,z),x). % 16153 [para_into,15832.1.2,15.1.1] f(f(x,y,z),f(u,y,z),f(w,y,z))=f(f(w,y,z),x,f(u,y,z)). % 16747 [para_into,16153.1.1,15.1.2] f(f(x,y,z),f(u,y,z),f(w,y,z))=f(f(x,y,z),u,f(w,y,z)). % 17228 [para_into,15470.1.1,16.1.1] f(f(x,y,f(z,u,w)),f(z,u,w),f(f(x,y,w5),f(z,u,w),f(y,u,w)))=f(f(z,u,w),x,f(y,u,w)). % 17262 [para_into,17228.1.1.3,7035.1.1] f(f(x,y,f(f(x,y,z),u,w)),f(f(x,y,z),u,w),f(f(x,y,z),u,w))=f(f(f(x,y,z),u,w),x,f(y,u,w)). % 17277 [para_into,17262.1.1,10.1.1,flip.1] f(f(f(x,y,z),u,w),x,f(y,u,w))=f(f(x,y,z),u,w). % 17607 [para_into,17277.1.1,14.1.2] f(f(x,y,z),u,f(f(u,x,w),y,z))=f(f(u,x,w),y,z). % 17672 [para_into,17277.1.2.1,15.1.2] f(f(f(x,y,z),u,w),x,f(y,u,w))=f(f(z,x,y),u,w). % 17676 [para_into,17277.1.2.1,11.1.2] f(f(f(x,y,z),u,w),x,f(y,u,w))=f(f(x,z,y),u,w). % 18551 [para_into,17672.1.1.1.1,15.1.2] f(f(f(x,y,z),u,w),y,f(z,u,w))=f(f(x,y,z),u,w). % 19150 [para_into,17676.1.1.1.1,11.1.2] f(f(f(x,y,z),u,w),x,f(z,u,w))=f(f(x,y,z),u,w). % 19931 [para_into,18551.1.1,16747.1.2] f(f(f(x,y,z),u,w),f(y,u,w),f(z,u,w))=f(f(x,y,z),u,w). % 20764 [para_from,19150.1.2,17607.1.1.3] f(f(x,y,z),u,f(f(f(u,x,w),y,z),u,f(w,y,z)))=f(f(u,x,w),y,z). % 21804 [para_into,20764.1.1.3,14.1.2] f(f(x,y,z),u,f(f(w,y,z),u,f(f(u,x,w),y,z)))=f(f(u,x,w),y,z). % 22092 [para_into,21804.1.1,16.1.2] f(f(f(x,y,z),u,f(w,y,z)),u,f(f(u,x,w),y,z))=f(f(u,x,w),y,z). % 22302 [para_into,22092.1.1.1,12.1.2] f(f(x,f(y,z,u),f(w,z,u)),x,f(f(x,y,w),z,u))=f(f(x,y,w),z,u). % 22661 [para_into,22302.1.1,12.1.2] f(x,f(x,f(y,z,u),f(w,z,u)),f(f(x,y,w),z,u))=f(f(x,y,w),z,u). % 22917 [para_into,22661.1.1.3,19931.1.2] f(x,f(x,f(y,z,u),f(w,z,u)),f(f(f(x,y,w),z,u),f(y,z,u),f(w,z,u)))=f(f(x,y,w),z,u). % 23263 [para_into,22917.1.1,7035.1.1] f(x,f(y,z,u),f(w,z,u))=f(f(x,y,w),z,u). % 23264 [binary,23263.1,17.1] $ANS("Distributivity (short)"). % % ------------ end of proof -------------