Consider the TRS R consisting of the rewrite rules

1: not(true) -> false
2: not(false) -> true
3: evenodd(x,0) -> not(evenodd(x,s(0)))
4: evenodd(0,s(0)) -> false
5: evenodd(s(x),s(0)) -> evenodd(x,0)

There are 3 dependency pairs:

6: EVENODD(x,0) -> NOT(evenodd(x,s(0)))
7: EVENODD(x,0) -> EVENODD(x,s(0))
8: EVENODD(s(x),s(0)) -> EVENODD(x,0)

The approximated dependency graph contains one SCC:
{7,8}.

- Consider the SCC {7,8}.
There are no usable rules.
By taking the polynomial interpretation
[0] = 1
and [EVENODD](x,y) = [s](x) = x + 1,
rule 7
is weakly decreasing and
rule 8
is strictly decreasing.

Hence the TRS is terminating.