Consider the TRS R consisting of the rewrite rules

1: not(x) -> if(x,false,true)
2: and(x,y) -> if(x,y,false)
3: or(x,y) -> if(x,true,y)
4: implies(x,y) -> if(x,y,true)
5: x = x -> true
6: x = y -> if(x,y,not(y))
7: if(true,x,y) -> x
8: if(false,x,y) -> y
9: if(x,x,if(x,false,true)) -> true
10: x = y -> if(x,y,if(y,false,true))

There are 8 dependency pairs:

11: NOT(x) -> IF(x,false,true)
12: AND(x,y) -> IF(x,y,false)
13: OR(x,y) -> IF(x,true,y)
14: IMPLIES(x,y) -> IF(x,y,true)
15: x =# y -> IF(x,y,not(y))
16: x =# y -> NOT(y)
17: x =# y -> IF(x,y,if(y,false,true))
18: x =# y -> IF(y,false,true)

The approximated dependency graph contains no SCCs
and hence the TRS is trivially terminating.