(0) Obligation:

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

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

Q is empty.