Consider the TRS R consisting of the rewrite rules

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

There are 9 dependency pairs:

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

The approximated dependency graph contains 2 SCCs:
{11-14}
and {7-10}.

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

- Consider the SCC {7-10}.
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-10}
are strictly decreasing.

Hence the TRS is terminating.