Consider the TRS R consisting of the rewrite rules

1: or(x,x) -> x
2: and(x,x) -> x
3: not(not(x)) -> x
4: not(and(x,y)) -> or(not(x),not(y))
5: not(or(x,y)) -> and(not(x),not(y))

There are 6 dependency pairs:

6: NOT(and(x,y)) -> OR(not(x),not(y))
7: NOT(and(x,y)) -> NOT(x)
8: NOT(and(x,y)) -> NOT(y)
9: NOT(or(x,y)) -> AND(not(x),not(y))
10: NOT(or(x,y)) -> NOT(x)
11: NOT(or(x,y)) -> NOT(y)

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

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

Hence the TRS is terminating.