(0) Obligation:

Q restricted rewrite system:
The TRS R consists of the following rules:

f(x, y, f(z, u, v)) → f(f(x, y, z), u, f(x, y, v))

Q is empty.