Length of proof is 16.  Level of proof is 13.

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

10 [] f(x,y,x)=x.
11 [] f(y,x,x)=x.
12 [] f(x,y,z)=f(y,x,z).
13 [] f(x,y,z)=f(x,z,y).
14 [] f(x,y,z)=f(z,y,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)|$ANS("Step 2").
713 [para_into,13.1.2,12.1.2,flip.1] f(x,y,z)=f(y,z,x).
768 [para_into,15.1.1.1,10.1.1,flip.1] f(x,y,f(x,y,z))=f(x,y,z).
1224 [para_into,768.1.1,713.1.2] f(f(x,y,z),x,y)=f(x,y,z).
1278 [para_from,768.1.2,11.1.1.3] f(x,f(y,z,u),f(y,z,f(y,z,u)))=f(y,z,u).
1631 [para_from,1224.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).
1897 [para_into,1278.1.1.3,13.1.2] f(x,f(y,z,u),f(y,f(y,z,u),z))=f(y,z,u).
1926 [para_into,1631.1.1,15.1.1] f(f(x,y,z),x,f(y,x,u))=f(x,f(x,y,z),u).
1977 [para_into,1926.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)).
2102 [para_into,1977.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)).
2105 [para_into,2102.1.1.3,15.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)).
2107 [para_into,2105.1.1.3,713.1.2] f(f(x,y,z),x,f(u,f(x,y,w),y))=f(x,f(x,y,z),f(u,y,w)).
2113 [para_into,2107.1.1,12.1.2] f(x,f(x,y,z),f(u,f(x,y,w),y))=f(x,f(x,y,z),f(u,y,w)).
2114 [para_into,2113.1.1,15.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)).
2115 [para_into,2114.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)).
2117 [para_into,2115.1.1,15.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)).
2119 [para_into,2117.1.1,1897.1.1,flip.1] f(x,f(x,y,z),f(u,y,z))=f(x,y,z).
2120 [binary,2119.1,17.1] $ANS("Step 2").

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