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:

h(x, x) → h(a, b)
g(g(x, a), y) → g(g(a, y), g(a, x))
f(g(x, y)) → g(g(f(f(y)), h(a, a)), x)
h(h(f(f(x)), y), h(z, v)) → h(h(f(z), f(f(f(y)))), h(v, x))

Q is empty.