Length of proof is 91.  Level of proof is 35.

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

2 [] f(x,y,x)=x.
3 [] f(y,x,x)=x.
4 [] f(x,y,z)=f(x,z,y).
5 [] f(x,y,z)=f(y,x,z).
6 [] f(x,y,z)=f(z,x,y).
7 [] f(x,y,z)=f(z,y,x).
8 [] f(x,y,z)=f(y,z,x).
9 [] f(f(x,w,y),w,z)=f(x,w,f(y,w,z)).
10 [] f(f(A,D,E),f(B,D,E),f(C,D,E))!=f(D,E,f(A,B,C))|$ANS("Distributivity (long)").
175 [para_into,4.1.1.1,3.1.2] f(f(x,y,y),z,u)=f(y,u,z).
254 [para_from,6.1.1,5.1.2.3,flip.1] f(x,y,f(z,u,w))=f(y,x,f(u,w,z)).
255 [para_from,6.1.1,5.1.1.3,flip.1] f(x,y,f(z,u,w))=f(y,x,f(w,z,u)).
360 [para_into,9.1.1.1,2.1.1,flip.1] f(x,y,f(x,y,z))=f(x,y,z).
388 [para_into,9.1.1,8.1.1,flip.1] f(x,y,f(z,y,u))=f(y,u,f(x,y,z)).
390 [para_into,9.1.1,5.1.2,flip.1] f(x,y,f(z,y,u))=f(y,f(x,y,z),u).
427 [para_into,9.1.2.3,2.1.1] f(f(x,y,z),y,z)=f(x,y,z).
438 [para_from,9.1.1,8.1.1,flip.1] f(x,y,f(z,x,u))=f(z,x,f(u,x,y)).
541 [para_into,175.1.1,4.1.2] f(f(x,y,y),z,u)=f(y,z,u).
708 [para_into,360.1.1,8.1.2] f(f(x,y,z),x,y)=f(x,y,z).
807 [para_from,360.1.2,3.1.1.3] f(x,f(y,z,u),f(y,z,f(y,z,u)))=f(y,z,u).
927 [para_into,427.1.1,8.1.1] f(x,y,f(z,x,y))=f(z,x,y).
1894 [para_into,254.1.1.2,8.1.2,flip.1] f(f(x,y,z),u,f(w,w5,w6))=f(u,f(z,x,y),f(w6,w,w5)).
2352 [para_into,388.1.1.3,8.1.1,flip.1] f(x,y,f(z,x,u))=f(z,x,f(x,y,u)).
2751 [para_into,390.1.1.3,5.1.2,flip.1] f(x,f(y,x,z),u)=f(y,x,f(x,z,u)).
2821 [para_into,390.1.2.2,708.1.1] f(f(x,y,z),x,f(y,x,u))=f(x,f(x,y,z),u).
3045 [para_into,438.1.1.3,8.1.2,flip.1] f(x,y,f(z,y,u))=f(y,u,f(z,x,y)).
4227 [para_into,2751.1.2.3,2352.1.2,flip.1] f(x,y,f(z,u,f(y,z,w)))=f(y,f(x,y,z),f(z,u,w)).
4861 [para_into,807.1.1.3,4.1.2] f(x,f(y,z,u),f(y,f(y,z,u),z))=f(y,z,u).
5302 [para_into,2821.1.1.3.3,7.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)).
7195 [para_into,4227.1.2.2,8.1.1,flip.1] f(x,f(x,y,z),f(y,u,w))=f(z,x,f(y,u,f(x,y,w))).
7868 [para_into,7195.1.2.3.3,8.1.1,flip.1] f(x,y,f(z,u,f(z,w,y)))=f(y,f(y,z,x),f(z,u,w)).
9058 [para_into,5302.1.1.3,5.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)).
9483 [para_into,9058.1.1.3,9.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)).
9860 [para_into,9483.1.1,255.1.1] f(x,f(x,y,z),f(u,f(x,y,w),y))=f(x,f(x,y,z),f(u,y,w)).
10228 [para_into,9860.1.1,9.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)).
10472 [para_into,10228.1.1.1,7.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)).
10780 [para_into,10472.1.1,9.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)).
11050 [para_into,10780.1.1,4861.1.1,flip.1] f(x,f(x,y,z),f(u,y,z))=f(x,y,z).
11412 [para_into,11050.1.1.2,8.1.2] f(x,f(y,x,z),f(u,z,y))=f(x,z,y).
11542 [para_into,11050.1.1.3,5.1.2] f(x,f(x,y,z),f(y,u,z))=f(x,y,z).
11554 [para_into,11050.1.1,1894.1.2] f(f(x,y,z),z,f(x,y,u))=f(z,x,y).
11574 [para_into,11050.1.1,4.1.2] f(x,f(y,z,u),f(x,z,u))=f(x,z,u).
11742 [para_into,11050.1.2,2.1.2,flip.1] f(f(x,y,z),u,f(x,y,z))=f(x,f(x,y,z),f(w,y,z)).
12453 [para_into,11412.1.1,8.1.2] f(f(x,y,z),u,f(z,u,y))=f(u,y,z).
13544 [para_into,11542.1.2,8.1.1] f(x,f(x,y,z),f(y,u,z))=f(y,z,x).
15051 [para_into,11574.1.1.2,9.1.1] f(x,f(y,z,f(u,z,w)),f(x,z,w))=f(x,z,w).
15442 [para_into,11574.1.2,8.1.1] f(x,f(y,z,u),f(x,z,u))=f(z,u,x).
15637 [para_from,11574.1.1,4.1.2.2] f(x,y,f(z,f(u,w,w5),f(z,w,w5)))=f(x,f(z,w,w5),y).
17258 [para_into,13544.1.1,7868.1.2] f(x,y,f(z,u,f(z,x,y)))=f(z,x,y).
18289 [para_into,15442.1.1.3,8.1.1] f(x,f(y,z,u),f(z,u,x))=f(z,u,x).
19145 [para_into,18289.1.1.2,708.1.1] f(x,f(y,z,u),f(y,z,x))=f(y,z,x).
20183 [para_into,19145.1.1.2,19145.1.1] f(x,f(y,z,u),f(u,f(y,z,w),x))=f(u,f(y,z,w),x).
20705 [para_from,19145.1.1,3045.1.1.3,flip.1] f(f(x,y,z),f(x,y,u),f(u,w,f(x,y,z)))=f(w,f(x,y,z),f(x,y,u)).
24011 [para_into,11742.1.2,8.1.1,flip.1] f(f(x,y,z),f(u,y,z),x)=f(f(x,y,z),w,f(x,y,z)).
24144 [para_from,11742.1.1,541.1.1.1] f(f(x,f(x,y,z),f(u,y,z)),w,w5)=f(f(x,y,z),w,w5).
25269 [para_into,15637.1.1,9.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)).
25709 [para_into,25269.1.1.1,4.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)).
26252 [para_into,25709.1.2,8.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)).
26381 [para_into,26252.1.1.1,8.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)).
26693 [para_into,26381.1.1.1,11554.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)).
27335 [para_into,20183.1.1,20705.1.1] f(f(x,y,z),f(x,y,u),f(x,y,w))=f(w,f(x,y,z),f(x,y,u)).
27964 [para_into,27335.1.1,8.1.2] f(f(x,y,z),f(x,y,u),f(x,y,w))=f(z,f(x,y,u),f(x,y,w)).
28384 [para_into,27964.1.1,27335.1.1,flip.1] f(x,f(y,z,u),f(y,z,w))=f(w,f(y,z,x),f(y,z,u)).
28661 [para_into,24144.1.1.1.2,11050.1.2] f(f(x,f(x,f(x,y,z),f(u,y,z)),f(w,y,z)),w5,w6)=f(f(x,y,z),w5,w6).
29319 [para_into,28661.1.1.1,5.1.2] f(f(f(x,f(x,y,z),f(u,y,z)),x,f(w,y,z)),w5,w6)=f(f(x,y,z),w5,w6).
29536 [para_into,29319.1.1.1.1,11742.1.2] f(f(f(f(x,y,z),u,f(x,y,z)),x,f(w,y,z)),w5,w6)=f(f(x,y,z),w5,w6).
29910 [para_into,29536.1.1.1,4.1.2] f(f(f(f(x,y,z),u,f(x,y,z)),f(w,y,z),x),w5,w6)=f(f(x,y,z),w5,w6).
30236 [para_into,29910.1.1,9.1.1] f(f(f(x,y,z),u,f(x,y,z)),f(w,y,z),f(x,f(w,y,z),w5))=f(f(x,y,z),f(w,y,z),w5).
30359 [para_into,30236.1.1.1,24011.1.2] f(f(f(x,y,z),f(u,y,z),x),f(w,y,z),f(x,f(w,y,z),w5))=f(f(x,y,z),f(w,y,z),w5).
30493 [para_into,30359.1.1,12453.1.1,flip.1] f(f(x,y,z),f(u,y,z),f(w,y,z))=f(f(u,y,z),f(w,y,z),x).
30860 [para_into,30493.1.2,8.1.1] f(f(x,y,z),f(u,y,z),f(w,y,z))=f(f(w,y,z),x,f(u,y,z)).
31149 [para_into,30860.1.1,8.1.2] f(f(x,y,z),f(u,y,z),f(w,y,z))=f(f(x,y,z),u,f(w,y,z)).
31722 [para_into,26693.1.1,9.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)).
31755 [para_into,31722.1.1.3,11050.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)).
31769 [para_into,31755.1.1,3.1.1,flip.1] f(f(f(x,y,z),u,w),x,f(y,u,w))=f(f(x,y,z),u,w).
32190 [para_into,31769.1.1,7.1.2] f(f(x,y,z),u,f(f(u,x,w),y,z))=f(f(u,x,w),y,z).
32282 [para_into,31769.1.2.1,8.1.2] f(f(f(x,y,z),u,w),x,f(y,u,w))=f(f(z,x,y),u,w).
32286 [para_into,31769.1.2.1,4.1.2] f(f(f(x,y,z),u,w),x,f(y,u,w))=f(f(x,z,y),u,w).
33457 [para_into,32282.1.1.1.1,8.1.2] f(f(f(x,y,z),u,w),y,f(z,u,w))=f(f(x,y,z),u,w).
34233 [para_into,32286.1.1.1.1,4.1.2] f(f(f(x,y,z),u,w),x,f(z,u,w))=f(f(x,y,z),u,w).
35221 [para_into,33457.1.1,31149.1.2] f(f(f(x,y,z),u,w),f(y,u,w),f(z,u,w))=f(f(x,y,z),u,w).
36804 [para_from,34233.1.2,32190.1.1.3] f(f(x,y,z),u,f(f(f(u,x,w),y,z),u,f(w,y,z)))=f(f(u,x,w),y,z).
37057 [para_into,36804.1.1.3,7.1.2] f(f(x,y,z),u,f(f(w,y,z),u,f(f(u,x,w),y,z)))=f(f(u,x,w),y,z).
37394 [para_into,37057.1.1,9.1.2] f(f(f(x,y,z),u,f(w,y,z)),u,f(f(u,x,w),y,z))=f(f(u,x,w),y,z).
37645 [para_into,37394.1.1.1,5.1.2] f(f(x,f(y,z,u),f(w,z,u)),x,f(f(x,y,w),z,u))=f(f(x,y,w),z,u).
38061 [para_into,37645.1.1,5.1.2] f(x,f(x,f(y,z,u),f(w,z,u)),f(f(x,y,w),z,u))=f(f(x,y,w),z,u).
38370 [para_into,38061.1.1.3,35221.1.2] f(x,f(x,f(y,z,u),f(w,z,u)),f(f(f(x,y,w),z,u),f(y,z,u),f(w,z,u)))=f(f(x,y,w),z,u).
38554 [para_into,38370.1.1,11050.1.1] f(x,f(y,z,u),f(w,z,u))=f(f(x,y,w),z,u).
39407 [para_into,38554.1.2,8.1.1] f(x,f(y,z,u),f(w,z,u))=f(z,u,f(x,y,w)).
40521 [para_into,39407.1.2.3,8.1.2] f(x,f(y,z,u),f(w,z,u))=f(z,u,f(w,x,y)).
41433 [para_into,40521.1.1.3,17258.1.2] f(x,f(y,z,u),f(z,u,f(w,w5,f(w,z,u))))=f(z,u,f(w,x,y)).
43327 [para_into,28384.1.2.2,927.1.1] f(f(x,y,z),f(y,z,u),f(y,z,w))=f(w,f(x,y,z),f(y,z,u)).
44010 [para_into,43327.1.1,4.1.2] f(f(x,y,z),f(y,z,u),f(y,z,w))=f(u,f(x,y,z),f(y,z,w)).
44351 [para_into,44010.1.1.2,8.1.2] f(f(x,y,z),f(u,y,z),f(y,z,w))=f(u,f(x,y,z),f(y,z,w)).
44917 [para_into,44351.1.1,5.1.2] f(f(x,y,z),f(u,y,z),f(y,z,w))=f(x,f(u,y,z),f(y,z,w)).
45264 [para_into,44917.1.1.2,8.1.1] f(f(x,y,z),f(y,z,u),f(y,z,w))=f(x,f(u,y,z),f(y,z,w)).
45778 [para_into,45264.1.1,43327.1.1,flip.1] f(x,f(y,z,u),f(z,u,w))=f(w,f(x,z,u),f(z,u,y)).
46626 [para_into,45778.1.2.3,8.1.2,flip.1] f(x,f(y,z,u),f(w,z,u))=f(y,f(w,z,u),f(z,u,x)).
47569 [para_into,46626.1.2,41433.1.1] f(f(x,y,f(x,z,u)),f(w,z,u),f(w5,z,u))=f(z,u,f(x,w,w5)).
48002 [para_into,47569.1.1.1,15051.1.1] f(f(x,y,z),f(u,y,z),f(w,y,z))=f(y,z,f(x,u,w)).
48003 [binary,48002.1,10.1] $ANS("Distributivity (long)").

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