Length of proof is 9.  Level of proof is 5.

---------------- PROOF ----------------

7 [] f(x,x,y)=x.
8 [] f(x,y,x)=x.
10 [] f(x,y,z)=f(x,z,y).
14 [] f(x,y,z)=f(y,z,x).
18 [] f(w,x,y)!=w|f(w,x,z)!=w|f(y,w,z)!=w|f(x,y,z)=w   # label("step 3").
19 [] f(f(x,u,v),f(y,u,v),f(z,u,v))=f(x,f(y,u,v),f(z,u,v))   # label("step 4").
21 [] f(f(f(x,y,z),u,v),x,f(y,u,v))=f(f(x,y,z),u,v)   # label("step 6").
22 [] f(X,f(Y,U,V),f(Z,U,V))!=f(f(X,Y,Z),U,V)|$ANS("Step 7").
1869 [para_into,19.1.2,14.1.2] f(f(x,y,z),f(u,y,z),f(w,y,z))=f(f(w,y,z),x,f(u,y,z)).
2828 [para_into,21.1.2.1,14.1.2] f(f(f(x,y,z),u,w),x,f(y,u,w))=f(f(z,x,y),u,w).
2832 [para_into,21.1.2.1,10.1.2] f(f(f(x,y,z),u,w),x,f(y,u,w))=f(f(x,z,y),u,w).
3330 [para_into,2828.1.1.1.1,14.1.2] f(f(f(x,y,z),u,w),y,f(z,u,w))=f(f(x,y,z),u,w).
4041 [para_into,2832.1.1.1.1,10.1.2] f(f(f(x,y,z),u,w),x,f(z,u,w))=f(f(x,y,z),u,w).
6367 [para_into,1869.1.1,14.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)).
7009 [para_into,6367.1.2,3330.1.1] f(f(f(x,y,z),u,w),f(y,u,w),f(z,u,w))=f(f(x,y,z),u,w).
7352 [hyper,18,8.1,7009.1,7.1] f(f(x,y,z),f(f(u,x,w),y,z),f(w,y,z))=f(f(u,x,w),y,z).
8054 [hyper,18,21.1,4041.1,7352.1] f(x,f(y,z,u),f(w,z,u))=f(f(x,y,w),z,u).
8055 [binary,8054.1,22.1] $ANS("Step 7").

------------ end of proof -------------