Consider the TRS R consisting of the rewrite rules

1: not(x) -> xor(x,true)
2: implies(x,y) -> xor(and(x,y),xor(x,true))
3: or(x,y) -> xor(and(x,y),xor(x,y))
4: x = y -> xor(x,xor(y,true))

There are no dependency pairs.
Hence the TRS is trivially terminating.