(0) Obligation:

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

g(x, x, x) → g(c, d, e)
g(x, y, x) → g(c, d, e)
s(f(x, y)) → f(y, f(s(s(x)), a))
h(h(x, a), y) → h(h(a, y), h(a, x))
f(x, f(y, f(x, y))) → f(a, f(x, f(y, b)))
f(h(a, y), g(x, b, a)) → h(f(x, s(y)), s(b))
h(f(x, s(y)), b) → f(a, g(y, a, f(s(x), a)))
f(x, g(x, a, f(s(x), y))) → f(h(x, b), g(a, b, y))
s(y) → b

Q is empty.