Consider the TRS R consisting of the rewrite rules

1: and(x,or(y,z)) -> or(and(x,y),and(x,z))
2: and(x,and(y,y)) -> and(x,y)
3: or(or(x,y),and(y,z)) -> or(x,y)
4: or(x,and(x,y)) -> x
5: or(true,y) -> true
6: or(x,false) -> x
7: or(x,x) -> x
8: or(x,or(y,y)) -> or(x,y)
9: and(x,true) -> x
10: and(false,y) -> false
11: and(x,x) -> x

There are 5 dependency pairs:

12: AND(x,or(y,z)) -> OR(and(x,y),and(x,z))
13: AND(x,or(y,z)) -> AND(x,y)
14: AND(x,or(y,z)) -> AND(x,z)
15: AND(x,and(y,y)) -> AND(x,y)
16: OR(x,or(y,y)) -> OR(x,y)

The approximated dependency graph contains 2 SCCs:
{16}
and {13-15}.

- Consider the SCC {16}.
There are no usable rules.
By taking the polynomial interpretation
[or](x,y) = [OR](x,y) = x + y + 1,
rule 16
is strictly decreasing.

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

Hence the TRS is terminating.