Consider the TRS R consisting of the rewrite rules

1: and(x,false) -> false
2: and(x,not(false)) -> x
3: not(not(x)) -> x
4: implies(false,y) -> not(false)
5: implies(x,false) -> not(x)
6: implies(not(x),not(y)) -> implies(y,and(x,y))

There are 4 dependency pairs:

7: IMPLIES(false,y) -> NOT(false)
8: IMPLIES(x,false) -> NOT(x)
9: IMPLIES(not(x),not(y)) -> IMPLIES(y,and(x,y))
10: IMPLIES(not(x),not(y)) -> AND(x,y)

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

- Consider the SCC {9}.
The usable rules are {1,2}.
By taking the polynomial interpretation
[false] = 1,
[and](x,y) = [not](x) = x + 1
and [IMPLIES](x,y) = x + y + 1,
rule 1
is weakly decreasing and
the rules in {2,9}
are strictly decreasing.

Hence the TRS is terminating.