Length of proof is 16.  Level of proof is 11.

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

7 [] f(x,y,x)=x.
8 [] f(y,x,x)=x.
9 [] f(x,y,z)=f(x,z,y).
10 [] f(x,y,z)=f(y,x,z).
13 [] f(x,y,z)=f(y,z,x).
14 [] f(f(x,w,y),w,z)=f(x,w,f(y,w,z))   # label("associativity").
16 [] f(x,f(x,u,v),f(z,u,v))=f(x,u,v)   # label("step 2").
18 [] f(f(X,U,V),f(Y,U,V),f(Z,U,V))!=f(X,f(Y,U,V),f(Z,U,V))|$ANS("Step 4").
399 [para_into,9.1.1.1,8.1.2] f(f(x,y,y),z,u)=f(y,u,z).
707 [para_into,16.1.1.2,13.1.2] f(x,f(y,x,z),f(u,z,y))=f(x,z,y).
748 [para_into,16.1.2,7.1.2,flip.1] f(f(x,y,z),u,f(x,y,z))=f(x,f(x,y,z),f(w,y,z)).
868 [para_into,399.1.1,9.1.2] f(f(x,y,y),z,u)=f(y,z,u).
1073 [para_into,707.1.1,13.1.2] f(f(x,y,z),u,f(z,u,y))=f(u,y,z).
1173 [para_into,748.1.2,13.1.1,flip.1] f(f(x,y,z),f(u,y,z),x)=f(f(x,y,z),w,f(x,y,z)).
1175 [para_into,748.1.2,9.1.2] f(f(x,y,z),u,f(x,y,z))=f(x,f(w,y,z),f(x,y,z)).
1176 [para_from,748.1.1,868.1.1.1] f(f(x,f(x,y,z),f(u,y,z)),w,w5)=f(f(x,y,z),w,w5).
1216 [para_into,1176.1.1.1.2,16.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).
1237 [para_into,1216.1.1.1,10.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).
1240 [para_into,1237.1.1.1.1,1175.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).
1243 [para_into,1240.1.1.1,9.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).
1246 [para_into,1243.1.1,14.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).
1250 [para_into,1246.1.1.1,1173.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).
1254 [para_into,1250.1.1,1073.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).
1256 [para_into,1254.1.2,13.1.2] f(f(x,y,z),f(u,y,z),f(w,y,z))=f(x,f(u,y,z),f(w,y,z)).
1257 [binary,1256.1,18.1] $ANS("Step 4").

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