Length of proof is 192.  Level of proof is 28.

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

1 [] f(f(x,w,y),w,z)=f(x,w,f(y,w,z)).
2 [] f(x,y,z)=f(y,x,z).
5 [] f(x,x,y)=x.
6 [] f(x,y,x)=x.
7 [] f(y,x,x)=x.
8 [] f(x,y,z)=f(y,x,z).
9 [] f(x,y,z)=f(x,z,y).
10 [] f(x,y,z)=f(z,y,x).
41 [] f(x,x,y)=x.
42 [] f(x,y,z)=f(y,x,z).
43 [] f(x,y,z)=f(x,z,y).
44 [] f(x,y,z)=f(z,y,x).
45 [] f(f(x,w,y),w,z)=f(x,w,f(y,w,z)).
48 [] f(f(A,D,E),f(B,D,E),f(C,D,E))!=f(D,E,f(A,B,C)).
1081 [para_into,2.1.1,2.1.2] f(x,y,z)=f(x,y,z).
1082 (heat=1) [para_into,1081.1.1,1.1.2,demod,10,8,8] f(x,y,f(z,x,u))=f(z,x,f(x,u,y)).
1084 [para_into,45.1.1.1,45.1.2,demod,10,8,10,8,8,10,8] f(x,y,f(x,z,f(u,x,w)))=f(u,x,f(x,y,f(x,w,z))).
1085 [para_into,45.1.1.1,45.1.1,demod,8,10,8,8,8,flip.1] f(x,f(y,x,z),f(x,u,w))=f(x,w,f(y,x,f(x,z,u))).
1086 [para_into,45.1.1.1,44.1.2,demod,10,8,8] f(x,y,f(z,x,u))=f(x,u,f(z,x,y)).
1087 [para_into,45.1.1.1,43.1.2,demod,10,8] f(x,y,f(z,u,x))=f(z,x,f(u,x,y)).
1088 [para_into,45.1.1.1,42.1.2,demod,10,8,8,8] f(x,y,f(x,z,u))=f(x,z,f(x,u,y)).
1089 [para_into,45.1.1,45.1.2,demod,10,8,10,8,8,8] f(x,y,f(x,z,f(u,x,w)))=f(u,x,f(x,w,f(x,z,y))).
1090 [para_into,45.1.1,44.1.2,demod,8,10,8,flip.1] f(x,y,f(z,x,u))=f(z,x,f(x,y,u)).
1091 [para_into,45.1.2.3,45.1.2,demod,8,8,8,10,8] f(x,f(y,x,z),f(x,u,w))=f(y,x,f(x,w,f(x,z,u))).
1103 (heat=1) [para_from,1084.1.1,1.1.2.3,demod,8,8,9,8,8] f(x,f(y,x,z),f(z,u,f(z,w,w5)))=f(y,x,f(z,w,f(x,z,f(z,u,w5)))).
1110 (heat=1) [para_into,1085.1.1.3,1.1.2,demod,8,10,8,8,8,9,flip.1] f(x,f(x,y,f(x,z,u)),f(u,w,w5))=f(x,f(x,y,z),f(u,w5,f(x,u,w))).
1111 (heat=1) [para_into,1085.1.1.3,1.1.1,demod,9,8,9,10,8] f(f(x,y,z),f(x,y,f(y,z,u)),f(w,w5,f(x,y,z)))=f(u,f(x,y,z),f(w,f(x,y,z),f(y,w5,f(x,y,z)))).
1123 (heat=1) [para_into,1086.1.1,1.1.1,demod,9,8,10,9,8,flip.1] f(x,f(y,z,u),f(z,w,f(y,z,u)))=f(y,z,f(z,u,f(w,x,f(y,z,u)))).
1128 (heat=1) [para_from,1086.1.1,1.1.1.1,demod,8,10,8,10,8,10,8] f(x,y,f(z,u,f(z,w,x)))=f(z,x,f(x,y,f(z,u,w))).
1132,1131 (heat=1) [para_into,1087.1.1,1.1.2,demod,10,6,10,8] f(x,y,f(x,y,z))=f(x,y,z).
1192 [para_into,1131.1.2,45.1.1,demod,10,8,8,8] f(x,f(y,x,z),f(x,u,f(y,x,z)))=f(y,x,f(x,z,u)).
1240 (heat=1) [para_into,1192.1.2,1.1.1,demod,8,10,8,8,10,8,8,8] f(x,f(x,y,f(x,z,u)),f(x,w,f(x,y,f(x,z,u))))=f(x,z,f(x,u,f(x,y,w))).
1249,1248 [para_from,1131.1.2,44.1.2,demod,10,8,flip.1] f(x,y,f(z,x,y))=f(z,x,y).
1251,1250 [para_from,1131.1.2,43.1.2,demod,9,flip.1] f(x,y,f(x,z,y))=f(x,z,y).
1278 (heat=1) [para_from,1248.1.1,1.1.1.1,demod,10,8,10,8,flip.1] f(x,y,f(y,z,f(u,x,y)))=f(y,z,f(u,x,y)).
1281 [back_demod,1240,demod,1251] f(x,y,f(x,z,f(x,u,w)))=f(x,u,f(x,w,f(x,z,y))).
1309 (heat=1) [para_into,1281.1.1.3,1.1.2,demod,6,9,flip.1] f(x,y,f(x,z,f(x,u,y)))=f(x,u,f(x,y,z)).
1324 [para_into,1082.1.1.3,1082.1.1,demod,10,9,9,8,flip.1] f(x,y,f(x,z,f(u,y,w)))=f(x,z,f(u,y,f(x,y,w))).
1328 [para_into,1082.1.2.3,1082.1.2,demod,10,8,9,8] f(x,f(x,y,z),f(y,u,w))=f(x,z,f(y,w,f(x,y,u))).
1344 (heat=1) [para_into,1324.1.1,1.1.2,demod,6,8,8,flip.1] f(x,y,f(y,z,f(x,y,u)))=f(x,y,f(y,z,u)).
1349 (heat=1) [para_into,1324.1.2,1.1.2,demod,8,1132,8,flip.1] f(x,f(y,x,z),f(y,x,u))=f(y,x,f(x,z,u)).
1392,1391 (heat=1) [para_into,1328.1.1,1.1.2,demod,9,1132,5,1132,flip.1] f(x,y,f(z,u,f(x,z,y)))=f(x,z,y).
1401 (heat=1) [para_from,1328.1.2,1.1.2,demod,8,9,10,9] f(x,f(y,x,z),f(y,z,u))=f(y,f(y,x,z),f(x,z,u)).
1484 [para_from,1086.1.1,1082.1.1.3,demod,10,10,8,9,8,flip.1] f(x,y,f(x,z,f(y,u,w)))=f(x,z,f(y,u,f(x,y,w))).
1489 (heat=1) [para_into,1484.1.2,1.1.2,demod,9,8,flip.1] f(x,f(y,z,x),f(y,z,u))=f(y,z,f(y,x,f(z,x,u))).
1498,1497 [para_into,1087.1.1.3,1131.1.1,demod,6,9,flip.1] f(x,f(x,y,z),f(y,u,f(x,y,z)))=f(x,y,z).
1502 [para_into,1087.1.1,1248.1.2,demod,8,9,10,9] f(x,f(x,y,f(z,u,y)),f(z,u,y))=f(z,y,f(x,u,y)).
1595 (heat=1) [para_into,1502.1.2.3,1.1.1,demod,10,8,8,10,8,9,1249,8,8] f(x,f(y,z,u),f(z,x,w))=f(x,w,f(y,z,f(z,u,x))).
1618,1617 [para_into,1391.1.1.3.3,1250.1.2,demod,9,1132,9] f(x,y,f(z,u,f(x,y,z)))=f(x,y,z).
1625,1624 [para_into,1391.1.1.3,1248.1.2,demod,9,9,8,1251,9] f(x,y,f(z,u,f(x,y,u)))=f(x,y,u).
1627,1626 [para_into,1391.1.1.3,1086.1.2,demod,8,9] f(x,y,f(y,z,f(x,z,u)))=f(x,y,z).
1629,1628 [para_into,1391.1.1.3,1082.1.1,demod,8,9] f(x,y,f(x,z,f(y,z,u)))=f(x,y,z).
1632 [para_into,1391.1.1,44.1.2,demod,8,10,8] f(x,y,f(z,u,f(z,x,y)))=f(z,x,y).
1744 [back_demod,1489,demod,10,9,8,8,flip.1] f(x,y,f(z,x,f(z,y,u)))=f(z,f(z,x,y),f(x,y,u)).
1936 [para_into,1084.1.1,1087.1.2,demod,5,9,10,9,8,1132,flip.1] f(x,y,f(z,y,u))=f(z,y,f(x,y,u)).
2455 [para_into,1624.1.1,1391.1.2,demod,9,9,1392,9] f(x,y,f(z,u,f(x,u,y)))=f(x,u,y).
2459 [para_into,1624.1.1,44.1.2,demod,10,9,10,10,9] f(x,y,f(z,u,f(u,x,y)))=f(u,x,y).
2477,2476 (heat=1) [para_into,2455.1.1.3,1.1.2,demod,10,9,10,9] f(x,y,f(y,z,f(x,u,z)))=f(x,y,z).
2530,2529 [para_into,1626.1.1,1082.1.2,demod,8,9,8] f(x,f(x,y,z),f(y,z,u))=f(x,y,z).
2628,2627 [back_demod,1744,demod,8,8,1629,10,8,flip.1] f(x,f(y,z,x),f(y,z,u))=f(y,z,x).
2629 [back_demod,1401,demod,8,2530,8,flip.1] f(x,f(y,x,z),f(y,z,u))=f(y,x,z).
2632 (heat=1) [para_into,2529.1.1.2,1.1.1,demod,8,10,8] f(f(x,y,z),f(x,y,f(y,z,u)),f(y,u,w))=f(y,u,f(x,y,z)).
2639,2638 (heat=1) [para_from,2529.1.1,1.1.2.3,demod,9,7] f(f(x,y,f(y,z,u)),f(y,z,u),f(z,u,w))=f(y,z,u).
2714 (heat=1) [para_from,2627.1.1,1.1.2.3,demod,9,7] f(f(x,y,f(z,u,y)),f(z,u,y),f(z,u,w))=f(z,u,y).
2717 (heat=1) [para_from,2627.1.2,1.1.1.1,demod,10,9,2530,10,8] f(x,y,f(z,u,x))=f(u,x,f(z,x,y)).
2725 (heat=1) [para_from,2629.1.1,1.1.2.3,demod,9,7] f(f(x,y,f(z,y,u)),f(z,y,u),f(z,u,w))=f(z,y,u).
2825,2824 [para_from,1626.1.2,1391.1.2,demod,9,1618,8,flip.1] f(x,y,f(z,y,f(x,z,u)))=f(x,z,y).
2992,2991 [para_into,2638.1.1.1,1248.1.2,demod,8,1251,8] f(f(x,y,z),f(x,u,f(x,y,z)),f(y,z,w))=f(x,y,z).
2995 [para_into,2638.1.1.1,1082.1.2,demod,8,9,8,8,9] f(f(x,y,z),f(x,y,f(x,u,z)),f(y,z,w))=f(x,y,z).
2999 [para_into,2638.1.1.1,42.1.2] f(f(x,y,f(x,z,u)),f(x,z,u),f(z,u,w))=f(x,z,u).
3026 [para_into,2638.1.1,44.1.2,demod,10,8,10,8,8,10,8] f(f(x,y,z),f(x,y,u),f(u,w,f(x,y,u)))=f(x,y,u).
3494 (heat=1) [para_into,3026.1.1.1,1.1.2,demod,10,8,8] f(f(x,y,z),f(y,u,f(x,y,w)),f(z,w5,f(x,y,z)))=f(x,y,z).
4282 [para_into,1085.1.2.3,1626.1.1,demod,8,9,8] f(x,f(x,y,z),f(x,u,f(y,z,w)))=f(x,u,f(x,y,z)).
5864,5863 [para_into,2995.1.1.1,2991.1.2,demod,2992,9] f(f(x,y,z),f(x,y,f(x,z,u)),f(y,z,w))=f(x,y,z).
5865 [para_into,2995.1.1.1,2725.1.2,demod,8,8,2639,9,8,8] f(f(x,y,z),f(x,y,f(y,z,u)),f(x,z,w))=f(x,y,z).
5944 [para_into,2995.1.1,44.1.2,demod,10,9,8,10,8,9,10,8] f(f(x,y,z),f(x,y,u),f(x,u,f(y,u,w)))=f(x,y,u).
6912 [para_from,1088.1.1,1248.1.1.3,demod,10,9,8] f(x,f(y,z,u),f(y,z,f(x,y,u)))=f(x,y,f(y,z,u)).
6950 [para_into,3026.1.1.1,2714.1.2,demod,10,9,10,9,2639] f(f(x,y,z),f(y,z,u),f(u,w,f(y,z,u)))=f(y,z,u).
6952 [para_into,3026.1.1.1,1391.1.2,demod,9,1618] f(f(x,y,z),f(x,z,u),f(u,w,f(x,z,u)))=f(x,z,u).
6982,6981 [para_into,3026.1.1.3.3,1624.1.1,demod,1625,10,8,1625] f(f(x,y,z),f(x,y,u),f(w,f(x,y,u),f(w5,u,f(x,y,u))))=f(x,y,u).
7001,7000 [para_into,3026.1.1.3,41.1.1,demod,10,9] f(x,f(y,z,u),f(y,z,x))=f(y,z,x).
7293 (heat=1) [para_into,7000.1.1,1.1.1,demod,9,9] f(x,f(y,z,u),f(w,f(y,z,u),f(y,z,f(x,w,f(y,z,u)))))=f(y,z,f(x,w,f(y,z,u))).
7369 [para_from,3026.1.1,1084.1.1.3,demod,8,7,8,flip.1] f(x,f(y,z,u),f(w,f(y,z,u),f(y,z,x)))=f(w,f(y,z,u),f(y,z,x)).
7407 (heat=1) [para_into,7369.1.1,1.1.2,demod,9,10,9,10,9,10,9,9] f(f(x,y,z),f(x,u,f(y,z,w)),f(y,z,w))=f(u,f(x,y,z),f(y,z,w)).
11962,11961 [para_into,5944.1.1.1,2714.1.2,demod,10,9,10,9,2639] f(f(x,y,z),f(y,z,u),f(y,u,f(z,u,w)))=f(y,z,u).
11963 [para_into,5944.1.1.1,1391.1.2,demod,9,1618] f(f(x,y,z),f(x,z,u),f(x,u,f(z,u,w)))=f(x,z,u).
11984 [para_into,5944.1.1.1,44.1.2,demod,8,8] f(f(x,y,z),f(y,z,u),f(z,u,f(y,u,w)))=f(y,z,u).
12169,12168 (heat=1) [para_into,11984.1.1.3.3,1.1.2,demod,10,8] f(f(x,y,z),f(y,z,u),f(z,u,f(u,w,f(y,u,w5))))=f(y,z,u).
12504,12503 [para_into,6950.1.1.3,41.1.1,demod,10,9] f(x,f(y,z,u),f(z,u,x))=f(z,u,x).
12518,12517 [para_into,6950.1.1,1248.1.1,demod,10,9,9,10,9] f(x,f(x,y,z),f(u,y,z))=f(x,y,z).
12996 [para_from,6950.1.1,1089.1.1.3,demod,8,10,9,1249,flip.1] f(x,f(y,z,u),f(w,f(y,z,u),f(z,u,x)))=f(w,f(y,z,u),f(z,u,x)).
13075 (heat=1) [para_into,12996.1.1,1.1.2,demod,9,10,9,10,9,10,9,9] f(f(x,y,z),f(x,u,f(w,y,z)),f(w,y,z))=f(u,f(x,y,z),f(w,y,z)).
13254 [para_into,6952.1.1.3,41.1.1,demod,10,9] f(x,f(y,z,u),f(y,u,x))=f(y,u,x).
13269,13268 [para_into,6952.1.1,1248.1.1,demod,10,9,9,10,9] f(x,f(x,y,z),f(y,u,z))=f(x,y,z).
14832 [para_from,1091.1.1,2999.1.1.1,demod,9,8,9] f(f(x,y,f(y,z,f(y,u,w))),f(y,z,w),f(z,w,w5))=f(y,z,w).
16025 [para_into,11961.1.1.1,1391.1.1,demod,9,10,8,9] f(f(x,y,z),f(z,u,f(y,w,f(x,y,z))),f(z,u,f(u,w5,f(y,w,f(x,y,z)))))=f(z,u,f(y,w,f(x,y,z))).
16165,16164 (heat=1) [para_into,16025.1.1.2,1.1.2,demod,10,9,10,8,12504,12169,flip.1] f(x,y,f(z,y,f(u,z,x)))=f(z,x,y).
18345 [para_from,2529.1.2,48.1.1.3,demod,10,9,9] f(f(A,D,E),f(B,D,E),f(C,f(x,D,E),f(C,D,E)))!=f(D,E,f(A,B,C)).
18349 (heat=1) [para_into,18345.1.1,1.1.2,demod,10,9,10,8] f(f(B,D,E),f(C,D,E),f(C,f(A,D,E),f(B,D,E)))!=f(D,E,f(A,B,C)).
18357 [para_from,2629.1.1,11963.1.1.1,demod,9,10,8,9] f(f(x,y,z),f(y,u,f(x,z,w)),f(y,u,f(u,w5,f(x,z,w))))=f(y,u,f(x,z,w)).
18359 (heat=1) [para_into,18357.1.1.3,1.1.2,demod,7,5,10,9] f(x,f(y,z,u),f(z,x,f(y,u,w)))=f(z,x,f(y,u,w)).
18374,18373 [para_into,7000.1.1.2,1090.1.1,demod,10,9,9,10,9] f(x,f(x,y,z),f(u,y,f(y,z,w)))=f(x,y,z).
18376,18375 [para_into,7000.1.1.2,1088.1.1,demod,10,9,9,10,9] f(x,f(x,y,z),f(y,u,f(y,w,z)))=f(x,y,z).
18377 [para_into,7000.1.1.3,2725.1.1,demod,9,9,10,9,9,6982,9,9,10,flip.1] f(f(x,y,z),f(x,y,u),f(w,u,f(x,y,u)))=f(x,y,u).
18402 [para_from,12503.1.1,2629.1.1.3,demod,8,10,9,8] f(x,f(x,y,f(z,u,w)),f(y,u,w))=f(x,y,f(z,u,w)).
18469 [para_into,1628.1.1.3,13254.1.2,demod,9,10,8] f(x,y,f(f(x,z,u),f(x,z,f(y,z,w)),f(y,z,w)))=f(x,y,z).
18496 (heat=1) [para_into,18469.1.1.3.2,1.1.2,demod,9,10,8,9] f(x,y,f(f(x,z,u),f(y,z,w),f(z,w,f(x,y,z))))=f(x,y,z).
18526 [para_into,1632.1.2,1087.1.1,demod,8,1392,10,9,flip.1] f(x,y,f(z,u,y))=f(z,y,f(x,u,y)).
18680 [para_into,16164.1.1.3.3,1088.1.2,demod,9,8,8,10,9] f(x,f(y,z,u),f(x,w,f(y,u,f(y,z,w))))=f(x,w,f(y,z,u)).
18689,18688 [para_into,16164.1.1,16164.1.2,demod,8,8,8,8,10,2825,10,9] f(x,y,f(x,z,f(z,u,y)))=f(x,z,y).
18696,18695 (heat=1) [para_into,18680.1.1.3.3,1.1.2,demod,7,6,7,9] f(x,y,f(x,z,f(u,y,z)))=f(x,y,z).
18730 [para_into,18688.1.1.3.3,2629.1.1,demod,9,9] f(x,f(x,y,f(z,u,y)),f(z,u,w))=f(x,y,f(z,u,w)).
18793 [para_into,2632.1.1.1,13254.1.2,demod,10,9,9,13269,8,10,9] f(f(x,y,z),f(y,z,f(x,z,u)),f(z,u,w))=f(z,u,f(x,y,z)).
18801 [para_from,2632.1.2,2459.1.2,demod,8,8,1392,10,9,8,10,9,flip.1] f(f(x,y,z),f(u,y,w),f(u,y,f(x,y,w)))=f(x,y,f(u,y,w)).
18810 (heat=1) [para_into,18801.1.2,1.1.2,demod,8,8,10,8] f(f(x,y,z),f(y,u,w),f(y,u,f(x,y,w)))=f(y,w,f(x,y,u)).
18864 [para_into,3494.1.1,1087.1.2,demod,8,8,8,8,10,8,1249,8] f(x,f(y,z,f(y,u,w)),f(y,u,x))=f(y,u,x).
18904 [para_into,14832.1.1.1.3,18688.1.2,demod,18689,9,8,9] f(f(x,y,f(y,z,f(y,u,w))),f(y,w,z),f(w,z,w5))=f(y,w,z).
18915,18914 [para_into,14832.1.1,12503.1.1,demod,10,9,8,10,8] f(x,y,f(z,u,f(x,u,f(y,u,w))))=f(x,y,u).
18921,18920 [para_into,14832.1.1,1617.1.1,demod,10,9] f(x,f(y,z,f(z,x,f(z,u,w))),f(z,x,w))=f(z,x,w).
18938,18937 [para_from,14832.1.1,12503.1.1,demod,9,8,flip.1] f(x,y,f(z,u,f(z,x,f(z,y,w))))=f(z,x,y).
18981 [para_from,18496.1.2,13254.1.2,demod,10,9,9,13269,8,8,10,9,flip.1] f(x,y,f(f(z,x,u),f(z,y,w),f(z,w,f(z,x,y))))=f(z,x,y).
19029,19028 [para_from,1103.1.2,2632.1.2,demod,8,8,9,1627,8,5864,10,9,flip.1] f(x,f(y,z,x),f(y,u,f(y,z,w)))=f(y,z,x).
19064 [para_into,18810.1.1.1,16164.1.2,demod,10,8,1627,8,8] f(f(x,y,z),f(x,u,w),f(x,u,f(x,z,w)))=f(x,w,f(x,z,u)).
19067 [para_into,18810.1.1.1,44.1.2,demod,8,8] f(f(x,y,z),f(y,u,w),f(y,u,f(y,z,w)))=f(y,w,f(y,z,u)).
19587,19586 [para_into,18375.1.1,18810.1.2,demod,8,9,8,1132,9,7,8] f(x,f(y,x,z),f(y,u,z))=f(y,x,z).
19602 [para_from,1110.1.1,6950.1.1.3,demod,10,8,1251,9] f(f(x,y,z),f(y,z,u),f(u,f(y,z,u),f(u,w,w5)))=f(y,z,u).
19625,19624 [para_into,19602.1.1,1936.1.2,demod,10,9,10,8,10,9,10,8,10,9] f(x,f(x,y,z),f(f(x,y,z),f(x,u,w),f(y,z,w5)))=f(x,y,z).
19659,19658 [para_from,1111.1.1,13254.1.1,demod,10,9,1498,7,10,9,flip.1] f(x,f(y,z,u),f(x,z,u))=f(x,z,u).
19785,19784 [para_into,1309.1.1.3,18695.1.1,demod,9,12518,9,flip.1] f(x,y,f(x,z,f(u,z,y)))=f(x,z,y).
20041,20040 [para_into,18914.1.1,2459.1.2,demod,8,8,8,8,1392,10,8] f(x,y,f(z,u,f(u,y,f(x,u,w))))=f(x,u,y).
20340 [para_into,7407.1.1.2,1087.1.2,demod,9,12504,flip.1] f(x,f(y,z,x),f(z,x,u))=f(x,u,f(y,z,x)).
20343,20342 [para_into,7407.1.2,18793.1.2,demod,16165,9,5] f(f(x,y,z),f(x,u,f(y,z,u)),f(y,z,u))=f(y,z,u).
20346 [para_from,7407.1.2,1278.1.2,demod,10,9,10,8,9,19587,1132,10,9,10,8,8,10,8,10,9,flip.1] f(f(x,y,z),f(x,u,z),f(y,u,f(x,y,z)))=f(x,y,z).
20354 [para_into,20342.1.1,19586.1.2,demod,10,9,10,9,10,9,8,10,9,8,9,19659,10,9] f(f(x,y,f(y,z,u)),f(x,z,u),f(y,z,u))=f(y,z,u).
20386,20385 [para_from,20346.1.1,1278.1.1.3,demod,7,8,8,10,8,flip.1] f(f(x,y,z),f(x,u,f(y,u,z)),f(y,u,z))=f(y,u,z).
20399 [para_into,20354.1.1.1,1344.1.2] f(f(x,y,f(y,z,f(x,y,u))),f(x,z,u),f(y,z,u))=f(y,z,u).
20410 [para_into,20399.1.1.1.3,20040.1.2,demod,20041,9,9,9] f(f(x,y,f(y,z,f(x,y,u))),f(x,u,z),f(y,u,z))=f(y,u,z).
20438 [para_into,20410.1.1.2,1250.1.1,demod,9,19587,1132] f(f(x,y,z),f(x,u,z),f(y,z,f(x,u,z)))=f(y,z,f(x,u,z)).
20453,20452 [para_into,20438.1.2,18377.1.1,demod,10,9,8,19659] f(f(x,y,f(z,u,y)),f(z,u,w),f(z,u,y))=f(z,u,y).
20485 [para_into,20340.1.2,18904.1.1,demod,8,9,18921,9,12504,9] f(x,y,f(z,u,f(u,x,f(u,w,y))))=f(u,x,y).
20520 [para_into,20485.1.1,20385.1.2,demod,8,8,8,20386,8] f(x,y,f(z,u,f(x,u,f(u,w,y))))=f(x,u,y).
20700 [para_into,1123.1.2.3.3,1086.1.2,demod,5,9,10,9,1132,flip.1] f(x,y,f(y,z,f(u,x,y)))=f(u,y,f(x,y,z)).
20754,20753 [para_into,20700.1.1.3,20346.1.1,demod,7,8,9,13269,9,flip.1] f(x,f(y,z,u),f(z,x,u))=f(z,x,u).
20991 [para_into,4282.1.2,19658.1.1,demod,10,8] f(x,f(x,y,z),f(x,f(y,z,u),f(y,z,w)))=f(x,y,z).
21054 [para_from,20991.1.1,18981.1.1.3.3,demod,9,10,8,7001,10,8,7] f(f(x,y,z),f(x,y,u),f(x,y,w))=f(w,f(x,y,z),f(x,y,u)).
21059 [para_into,21054.1.1.1,20520.1.2,demod,10,9,18915,9] f(f(x,y,z),f(x,z,u),f(x,z,w))=f(w,f(x,y,z),f(x,z,u)).
21060 [para_into,21054.1.1.1,20485.1.1,demod,9,8,18938] f(f(x,y,z),f(y,z,u),f(y,z,w))=f(w,f(x,y,z),f(y,z,u)).
21062 [para_into,21054.1.1,19064.1.1,demod,9,9,9,9,flip.1] f(f(x,y,z),f(x,y,u),f(x,z,u))=f(x,y,f(x,z,u)).
21070 [para_into,21062.1.1.1,20485.1.2,demod,10,9,8,18915,8,8,8,8] f(f(x,y,z),f(x,z,u),f(y,z,u))=f(x,z,f(y,z,u)).
21080 [para_into,21062.1.1,13254.1.2,demod,9,9,8,9,9,10,9,19659] f(f(x,y,z),f(x,y,u),f(x,z,u))=f(x,u,f(x,y,z)).
21109,21108 [para_from,21062.1.2,18864.1.1.2,demod,10,9,9,10,9] f(x,f(x,y,z),f(f(y,u,z),f(y,u,w),f(y,z,w)))=f(x,y,z).
21147 [para_into,21070.1.2,20700.1.2] f(f(x,y,z),f(x,z,u),f(y,z,u))=f(y,z,f(z,u,f(x,y,z))).
21156 [para_from,21070.1.2,1131.1.1.3,demod,9,8,8] f(x,y,f(f(x,y,z),f(x,y,u),f(y,z,u)))=f(x,y,f(y,z,u)).
21180 [para_into,21059.1.1,20385.1.2,demod,9,9,20343] f(f(x,y,z),f(x,z,u),f(x,z,w))=f(u,f(x,y,z),f(x,z,w)).
21183 [para_into,21059.1.2,18810.1.2,demod,7,10,9,1251,7] f(x,f(y,z,x),f(y,x,u))=f(x,u,f(y,z,x)).
21225 [para_into,1128.1.2.3,18801.1.2,demod,10,9,8,1627,8,8,8,flip.1] f(x,y,f(f(x,z,u),f(z,y,w),f(z,y,f(x,z,w))))=f(x,z,y).
21337 [para_from,21147.1.2,1123.1.2.3,demod,1249,7,10,9,10,9,10,8,flip.1] f(x,y,f(f(z,x,u),f(z,y,u),f(x,y,u)))=f(x,y,u).
21364 [para_from,21337.1.1,13075.1.1.2,demod,9,12518,8,9,5,9,12518,8,9,flip.1] f(x,f(y,x,z),f(f(y,u,z),f(y,x,z),f(u,x,z)))=f(y,x,z).
21379 [para_from,21156.1.2,2459.1.1.3,demod,10,9,10,9,10,8,10,9,10,8] f(x,y,f(z,u,f(f(x,y,u),f(x,z,u),f(y,z,u))))=f(x,y,u).
21383 [para_from,21225.1.2,21364.1.2,demod,8,9,8,10,8,10,8,19625,8,8,flip.1] f(x,y,f(f(z,x,u),f(z,y,w),f(z,y,f(z,x,w))))=f(z,x,y).
21402 [para_into,21379.1.1,20452.1.2,demod,10,9,10,8,10,8,10,8,10,9,10,8,10,8,10,8,10,9,10,8,10,8,10,8,20453,10,9] f(x,y,f(z,u,f(f(z,u,x),f(z,u,y),f(u,x,y))))=f(u,x,y).
21432 [para_from,21183.1.2,21180.1.2,demod,7,flip.1] f(x,f(y,z,x),f(y,x,f(y,u,z)))=f(y,z,x).
21515 [para_from,6912.1.1,2824.1.1.3.3,demod,10,8,9] f(x,y,f(y,f(x,z,f(z,u,w)),f(z,u,w)))=f(x,y,f(z,u,w)).
21527 [para_from,6912.1.2,1349.1.2,demod,8,8,8,flip.1] f(x,f(y,z,u),f(y,z,f(y,x,u)))=f(y,f(y,x,z),f(y,x,u)).
21536 (heat=1) [para_into,21515.1.2,1.1.1,demod,8,9,8,18696,8] f(x,f(y,x,z),f(u,w,w5))=f(y,x,f(x,z,f(u,w,w5))).
21650 [para_into,18359.1.1.3,21402.1.1,demod,10,9,12518,9,10,9,10,10,8,8,flip.1] f(x,y,f(z,u,f(f(x,z,u),f(x,y,u),f(z,y,u))))=f(x,y,u).
21665 [para_into,18359.1.1,1595.1.1,demod,10,8] f(x,f(y,z,u),f(y,w,f(x,z,w)))=f(x,w,f(y,z,u)).
21685 [para_from,18359.1.1,21383.1.1.3.3.3,demod,9,8,8,7,8,10,9] f(x,f(y,z,u),f(x,w,f(z,w,f(y,u,w5))))=f(x,w,f(y,z,u)).
21829 [para_from,18402.1.2,21432.1.2,demod,9,19029,10,8,9,flip.1] f(x,f(y,z,u),f(x,u,f(w,y,z)))=f(x,u,f(w,y,z)).
22045 [para_into,18730.1.1.2,18526.1.2,demod,9] f(x,f(y,z,f(x,z,u)),f(y,u,w))=f(x,z,f(y,u,w)).
22557,22556 [para_into,21536.1.1.2,13268.1.1,demod,5,9,flip.1] f(x,f(x,y,z),f(f(x,y,z),f(y,z,u),f(w,w5,w6)))=f(x,y,z).
22560 [para_into,21536.1.1.2,2627.1.1,demod,5,flip.1] f(x,f(y,z,x),f(f(y,z,x),f(y,z,u),f(w,w5,w6)))=f(y,z,x).
22626 [para_from,21536.1.2,5865.1.1.2,demod,9] f(f(x,y,z),f(x,z,u),f(y,f(x,y,z),f(w,w5,w6)))=f(x,y,z).
22685 [para_into,22626.1.1,20753.1.2,demod,9,9,9,9,8,19659,9] f(f(x,y,z),f(x,y,u),f(u,f(x,y,u),f(w,w5,w6)))=f(x,y,u).
22701 [para_into,22685.1.1.1,22560.1.2,demod,10,9,10,9,22557] f(f(x,y,z),f(y,z,u),f(u,f(y,z,u),f(w,w5,w6)))=f(y,z,u).
23010 [para_into,21829.1.1.3,21665.1.1,demod,9,8,8,9,13269,8,9,8,9,flip.1] f(x,f(y,z,f(x,y,u)),f(u,z,w))=f(x,y,f(u,z,w)).
23012,23011 [para_into,21829.1.1.3,21650.1.1,demod,9,9,10,9,9,9,9,2530,9,9,10,9,8,flip.1] f(x,y,f(z,u,f(f(x,z,u),f(x,z,y),f(z,u,y))))=f(x,z,y).
23140 [para_into,22045.1.1,21402.1.1,demod,10,9,1625,10,8,10,9,8,2477,10,9,1625,9,8,flip.1] f(x,y,f(z,u,f(f(z,x,u),f(z,x,y),f(z,u,y))))=f(z,x,y).
23211 [para_into,23010.1.1,44.1.2,demod,10,8,10,9,8] f(x,f(y,z,u),f(z,w,f(y,w,x)))=f(w,x,f(y,z,u)).
23506 [para_from,21527.1.2,19067.1.2,demod,1132,7,9,flip.1] f(x,f(y,z,u),f(y,u,f(y,x,z)))=f(y,z,f(y,x,u)).
23905 [para_into,21685.1.1.3.3,21080.1.2,demod,5,9,8,5,9] f(x,y,f(x,z,f(f(y,u,z),f(y,u,w),f(y,z,w))))=f(x,y,z).
23974 [para_from,23905.1.1,1309.1.1.3,demod,9,21109,9,flip.1] f(x,y,f(x,z,f(f(z,u,y),f(z,u,w),f(z,y,w))))=f(x,z,y).
23984 [para_from,23974.1.1,23506.1.1.3,demod,9,8,9,2530,8,9,flip.1] f(x,f(y,x,z),f(f(y,u,z),f(y,u,w),f(y,z,w)))=f(y,x,z).
24293 [para_from,7293.1.2,7407.1.1.2,demod,9,11962,flip.1] f(x,f(y,z,u),f(z,u,f(y,x,w)))=f(z,u,f(y,x,w)).
24299 [para_into,24293.1.1.3.3,20753.1.1,demod,9,9,12504] f(f(x,y,z),f(u,w,w5),f(w,w5,f(y,z,u)))=f(w,w5,f(y,z,u)).
24317 [para_into,24293.1.1.3,22560.1.1,demod,6,7,8,flip.1] f(x,f(y,z,x),f(f(y,z,u),f(y,z,x),f(w,w5,w6)))=f(y,z,x).
24356 [para_into,24293.1.1.3,11984.1.1,demod,10,9,10,9,10,9,18376,10,9,10,8,8,10,8,flip.1] f(f(x,y,z),f(x,y,f(x,z,u)),f(y,w,z))=f(x,y,z).
24369 [para_into,24293.1.1,23211.1.2,demod,16165,9] f(f(x,y,z),f(y,z,u),f(y,z,f(x,u,w)))=f(y,z,f(x,u,w)).
24453 [para_from,24356.1.1,24293.1.1.3,demod,8,8,18374,8,7,8,8,8,10,9,flip.1] f(f(x,y,z),f(y,u,z),f(y,u,f(u,z,w)))=f(y,u,z).
24472 [para_into,24299.1.1,13254.1.2,demod,10,8,10,8,10,8,10,8,10,8,10,8,20754] f(f(x,y,z),f(x,y,f(u,w,z)),f(u,w,w5))=f(x,y,f(u,w,z)).
24480 [para_from,24299.1.2,23140.1.2,demod,8,8,23012,10,8,10,9,8,10,8,flip.1] f(f(x,y,z),f(x,z,f(u,w,y)),f(u,w,w5))=f(x,z,f(u,w,y)).
24495 (heat=1) [para_into,24480.1.2,1.1.2,demod,10,8,10] f(f(x,y,z),f(x,z,f(y,z,u)),f(z,u,w))=f(y,z,f(x,z,u)).
24526 [para_into,24369.1.1,21060.1.1,demod,10,9] f(f(x,y,z),f(x,u,w),f(y,u,w))=f(u,w,f(x,y,z)).
24552 [para_into,24526.1.1.1,24453.1.2,demod,9,8,11962,9] f(f(x,y,z),f(x,u,w),f(z,u,w))=f(u,w,f(x,y,z)).
24555 [para_into,24526.1.1.1,19658.1.1,demod,10,8,10,8,10,8,9,2530] f(f(x,y,z),f(x,u,w),f(u,w,f(y,z,w5)))=f(u,w,f(x,y,z)).
24597,24596 [para_from,24526.1.2,7000.1.1.2,demod,10,9,9,10,9] f(x,f(x,y,z),f(f(u,w,w5),f(u,y,z),f(w,y,z)))=f(x,y,z).
24604 [para_into,24552.1.1,23984.1.2,demod,10,8,8,10,8,8,10,8,10,8,10,9,8,24597] f(f(x,y,z),f(x,u,w),f(y,z,w))=f(y,z,f(x,u,w)).
24648 [para_into,24604.1.1.1,24317.1.2,demod,10,9,10,9,8,22557,8,9,8] f(f(x,y,z),f(x,z,u),f(y,w,u))=f(x,z,f(y,w,u)).
24809 [para_from,24472.1.1,1617.1.1.3] f(x,y,f(z,u,f(x,y,w)))=f(x,y,f(z,u,w)).
24825 [para_into,24495.1.1.2,22701.1.1,demod,8,12504,10,9,5,flip.1] f(x,f(y,z,x),f(f(u,y,z),f(y,z,x),f(w,w5,w6)))=f(y,z,x).
25061 [para_from,24809.1.2,24526.1.2,demod,10,9] f(f(x,y,z),f(x,u,w),f(y,u,w))=f(u,w,f(x,y,f(z,u,w))).
25109 [para_into,25061.1.1.1,24825.1.2,demod,10,9,10,8,10,9,8,22557] f(f(x,y,z),f(y,u,w),f(z,u,w))=f(u,w,f(y,z,f(x,u,w))).
25223 [para_into,25109.1.2.3,24648.1.1,demod,8,2530,8,10,10,2628,9,8,flip.1] f(x,y,f(z,u,f(w,x,y)))=f(x,y,f(w,z,u)).
26096 [para_from,2717.1.1,24555.1.1.3] f(f(x,y,z),f(x,u,w),f(z,u,f(y,u,w)))=f(u,w,f(x,y,z)).
26126 [para_from,26096.1.2,18349.1.1.3,demod,8,8,19785,8,1249] f(f(B,C,f(A,D,E)),f(B,D,E),f(C,D,E))!=f(D,E,f(A,B,C)).
26127 [para_into,26126.1.1,25061.1.1,demod,10,8,1249] f(D,E,f(B,C,f(A,D,E)))!=f(D,E,f(A,B,C)).
26128 [binary,26127.1,25223.1] $F.

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