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

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

11 [] f(x,y,z)=f(y,x,z).
13 [] f(x,y,z)=f(z,y,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").
17 [] f(W,X,Y)=W.
18 [] f(W,X,Z)=W.
19 [] f(W,Y,Z)=W.
20 [] f(X,Y,Z)!=W|$ANS("Step 3").
226 [para_into,17.1.1,13.1.2] f(Y,X,W)=W.
505 [para_into,226.1.1.3,18.1.2] f(Y,X,f(W,X,Z))=W.
722 [para_into,505.1.1.3,13.1.2] f(Y,X,f(Z,X,W))=W.
850 [para_into,722.1.1,14.1.2] f(f(Y,X,Z),X,W)=W.
958 [para_into,850.1.1.1,11.1.2] f(f(X,Y,Z),X,W)=W.
1106 [para_into,958.1.1,11.1.2] f(X,f(X,Y,Z),W)=W.
1226 [para_into,1106.1.1.3,19.1.2] f(X,f(X,Y,Z),f(W,Y,Z))=W.
1525 [para_into,1226.1.1,16.1.1] f(X,Y,Z)=W.
1526 [binary,1525.1,20.1] $ANS("Step 3").

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