(0) Obligation:

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

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

Q is empty.