Consider the TRS R consisting of the rewrite rules

1: not(true) -> false
2: not(false) -> true
3: odd(0) -> false
4: odd(s(x)) -> not(odd(x))
5: x + 0 -> x
6: x + s(y) -> s(x + y)
7: s(x) + y -> s(x + y)

There are 4 dependency pairs:

8: ODD(s(x)) -> NOT(odd(x))
9: ODD(s(x)) -> ODD(x)
10: x +# s(y) -> x +# y
11: s(x) +# y -> x +# y

The approximated dependency graph contains 2 SCCs:
{10,11}
and {9}.

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

- Consider the SCC {9}.
There are no usable rules.
By taking the polynomial interpretation
[ODD](x) = [s](x) = x + 1,
rule 9
is strictly decreasing.

Hence the TRS is terminating.