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:

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

Q is empty.