Consider the TRS R consisting of the rewrite rules

1: g(f(x,y),z) -> f(x,g(y,z))
2: g(h(x,y),z) -> g(x,f(y,z))
3: g(x,h(y,z)) -> h(g(x,y),z)

There are 3 dependency pairs:

4: G(f(x,y),z) -> G(y,z)
5: G(h(x,y),z) -> G(x,f(y,z))
6: G(x,h(y,z)) -> G(x,y)

The approximated dependency graph contains one SCC:
{4-6}.

- Consider the SCC {4-6}.
There are no usable rules.
By taking the polynomial interpretation
[f](x,y) = [G](x,y) = [h](x,y) = x + y + 1,
rule 5
is weakly decreasing and
the rules in {4,6}
are strictly decreasing.
There is one new SCC.

- Consider the SCC {5}.
By taking the polynomial interpretation
[f](x,y) = x + y
and [G](x,y) = [h](x,y) = x + y + 1,
rule 5
is strictly decreasing.


Hence the TRS is terminating.