Termination w.r.t. Q of the given QTRS could not be shown:

(0) Obligation:

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

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

Q is empty.