Consider the TRS R consisting of the rewrite rules

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

There are 3 dependency pairs:

4: F(x,y) -> G(x,y)
5: G(h(x),y) -> F(x,y)
6: G(h(x),y) -> 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
[h](x) = x + 1
and [F](x,y) = [G](x,y) = x + y + 1,
rule 4
is weakly decreasing and
the rules in {5,6}
are strictly decreasing.

Hence the TRS is terminating.