Consider the TRS R consisting of the rewrite rules

1: s(a) -> a
2: s(s(x)) -> x
3: s(f(x,y)) -> f(s(y),s(x))
4: s(g(x,y)) -> g(s(x),s(y))
5: f(x,a) -> x
6: f(a,y) -> y
7: f(g(x,y),g(u,v)) -> g(f(x,u),f(y,v))
8: g(a,a) -> a

There are 9 dependency pairs:

9: S(f(x,y)) -> F(s(y),s(x))
10: S(f(x,y)) -> S(y)
11: S(f(x,y)) -> S(x)
12: S(g(x,y)) -> G(s(x),s(y))
13: S(g(x,y)) -> S(x)
14: S(g(x,y)) -> S(y)
15: F(g(x,y),g(u,v)) -> G(f(x,u),f(y,v))
16: F(g(x,y),g(u,v)) -> F(x,u)
17: F(g(x,y),g(u,v)) -> F(y,v)

The approximated dependency graph contains 2 SCCs:
{16,17}
and {10,11,13,14}.

- Consider the SCC {16,17}.
There are no usable rules.
By taking the polynomial interpretation
[F](x,y) = [g](x,y) = x + y + 1,
the rules in {16,17}
are strictly decreasing.

- Consider the SCC {10,11,13,14}.
There are no usable rules.
By taking the polynomial interpretation
[S](x) = x + 1
and [f](x,y) = [g](x,y) = x + y + 1,
the rules in {10,11,13,14}
are strictly decreasing.

Hence the TRS is terminating.