(0) Obligation:

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

f(c(a, z, x)) → b(a, z)
b(x, b(z, y)) → f(b(f(f(z)), c(x, z, y)))
b(y, z) → z

Q is empty.