Length of proof is 11.  Level of proof is 8.

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

9 [] f(y,x,x)=x.
10 [] f(x,y,z)=f(x,z,y).
11 [] f(x,y,z)=f(y,x,z).
12 [] f(x,y,z)=f(z,x,y).
14 [] f(x,y,z)=f(y,z,x).
15 [] f(f(x,w,y),w,z)=f(x,w,f(y,w,z))   # label("associativity").
17 [] f(x,f(x,u,v),f(z,u,v))=f(x,u,v)   # label("step 2").
20 [] f(f(x,y,f(z,u,v)),f(y,u,v),f(z,u,v))=f(x,f(y,u,v),f(z,u,v))   # label("step 5").
21 [] f(f(f(X,Y,Z),U,V),X,f(Y,U,V))!=f(f(X,Y,Z),U,V)|$ANS("Step 6").
583 [para_from,12.1.1,11.1.2.3] f(x,y,f(z,u,w))=f(y,x,f(w,z,u)).
1092 [para_into,20.1.2,14.1.2] f(f(x,y,f(z,u,w)),f(y,u,w),f(z,u,w))=f(f(z,u,w),x,f(y,u,w)).
1093 [para_into,583.1.1.1,14.1.1] f(f(x,y,z),u,f(w,w5,w6))=f(u,f(z,x,y),f(w6,w,w5)).
1279 [para_into,1093.1.2,17.1.1] f(f(x,y,z),z,f(x,y,u))=f(z,x,y).
1402 [para_into,1092.1.1,10.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)).
1404 [para_into,1402.1.1.1,14.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)).
1405 [para_into,1404.1.1.1,1279.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)).
1408 [para_into,1405.1.1,15.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)).
1409 [para_into,1408.1.1.3,17.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)).
1410 [para_into,1409.1.1,9.1.1] f(f(x,y,z),u,w)=f(f(f(x,y,z),u,w),x,f(y,u,w)).
1411 [copy,1410,flip.1] f(f(f(x,y,z),u,w),x,f(y,u,w))=f(f(x,y,z),u,w).
1412 [binary,1411.1,21.1] $ANS("Step 6").

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