What is the syntactic type of (mid-, three-way) distributivity?

The source page states the original problem together with its recorded qualifications and progress updates as follows.

What is the syntactic type (maximum number of top-level steps needed in an equational proof [Claude Kirchner, 1993]) of the distributivity axiom? What is the syntactic type of ``three-way'' commutativity:

$$\begin{array}{l} f(x, y, z) = f(x, z, y) = f(y, x, z) = f(y, z, x) = f(z, x, y) = f(z, y, x)\\ f(f(x, y, z), u, x) = f(x, y, f(z, u, x)) \end{array}$$

What are the unification type, decidability, and syntactic type of ``mid-commutativity'': $(x+y)+(u+v) = (x+u)+(y+v)$?