Consider the TRS R consisting of the rewrite rules

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

There are 12 dependency pairs:

4: NOT(or(x,y)) -> NOT(not(not(x)))
5: NOT(or(x,y)) -> NOT(not(x))
6: NOT(or(x,y)) -> NOT(x)
7: NOT(or(x,y)) -> NOT(not(not(y)))
8: NOT(or(x,y)) -> NOT(not(y))
9: NOT(or(x,y)) -> NOT(y)
10: NOT(and(x,y)) -> NOT(not(not(x)))
11: NOT(and(x,y)) -> NOT(not(x))
12: NOT(and(x,y)) -> NOT(x)
13: NOT(and(x,y)) -> NOT(not(not(y)))
14: NOT(and(x,y)) -> NOT(not(y))
15: NOT(and(x,y)) -> NOT(y)

Consider the SCC {4-15}.
By taking the polynomial interpretation
[not](x) = x,
[NOT](x) = x + 1
and [and](x,y) = [or](x,y) = x + y + 1,
the rules in {1-3}
are weakly decreasing and
the rules in {4-15}
are strictly decreasing.
Hence the TRS is terminating.