Consider the TRS R consisting of the rewrite rules

1: f(s(x),y) -> f(x,s(x))
2: f(x,s(y)) -> f(y,x)

There are 2 dependency pairs:

3: F(s(x),y) -> F(x,s(x))
4: F(x,s(y)) -> F(y,x)

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

- Consider the SCC {3,4}.
There are no usable rules.
By taking the polynomial interpretation
[s](x) = 3x + 1
and [F](x,y) = 3x + 2y + 1,
the rules in {3,4}
are strictly decreasing.

Hence the TRS is terminating.