(VAR x y)
(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
)