Length of proof is 1.  Level of proof is 1.

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

2 [] f(x,y,x)=x.
7 [] f(f(x,w,y),w,z)=f(x,w,f(y,w,z)).
11 [] f(f(X,Y,Z),Y,Z)!=f(X,Y,Z)|$ANS("Step 1").
41 [para_into,7.1.2.3,2.1.1] f(f(x,y,z),y,z)=f(x,y,z).
43 [binary,41.1,11.1] $ANS("Step 1").

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