Consider the TRS R consisting of the rewrite rules

1: f(g(x),g(y)) -> f(p(f(g(x),s(y))),g(s(p(x))))
2: p(0) -> g(0)
3: g(s(p(x))) -> p(x)

There are 6 dependency pairs:

4: F(g(x),g(y)) -> F(p(f(g(x),s(y))),g(s(p(x))))
5: F(g(x),g(y)) -> P(f(g(x),s(y)))
6: F(g(x),g(y)) -> F(g(x),s(y))
7: F(g(x),g(y)) -> G(s(p(x)))
8: F(g(x),g(y)) -> P(x)
9: P(0) -> G(0)

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

- Consider the SCC {4}.
By taking the polynomial interpretation
[f](x,y) = 0,
[0] = 2,
[F](x,y) = [p](x) = [s](x) = 2x + 1
and [g](x) = x + 2,
rule 1
is weakly decreasing and
the rules in {2-4}
are strictly decreasing.

Hence the TRS is terminating.