Length of proof is 5. Level of proof is 5. ---------------- PROOF ---------------- 8 [] f(x,y,x)=x. 10 [] f(x,y,z)=f(x,z,y). 15 [] f(f(x,w,y),w,z)=f(x,w,f(y,w,z)) # label("associativity"). 19 [] f(f(x,u,v),f(y,u,v),f(z,u,v))=f(x,f(y,u,v),f(z,u,v)) # label("step 4"). 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))|$ANS("Step 5"). 223 [para_into,10.1.1.2,8.1.1,flip.1] f(x,y,f(z,u,z))=f(x,z,y). 1343 [para_into,223.1.1.3,19.1.1] f(x,y,f(z,f(u,w,w5),f(z,w,w5)))=f(x,f(z,w,w5),y). 1699 [para_into,1343.1.1,15.1.2] f(f(x,f(y,z,u),w),f(y,z,u),f(w,z,u))=f(x,f(w,z,u),f(y,z,u)). 2698 [para_into,1699.1.1.1,10.1.2] f(f(x,y,f(z,u,w)),f(z,u,w),f(y,u,w))=f(x,f(y,u,w),f(z,u,w)). 3500 [para_into,2698.1.1,10.1.2] f(f(x,y,f(z,u,w)),f(y,u,w),f(z,u,w))=f(x,f(y,u,w),f(z,u,w)). 3501 [binary,3500.1,20.1] $ANS("Step 5"). ------------ end of proof -------------