Consider the TRS R consisting of the rewrite rules

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

There are 10 dependency pairs:

10: NOT(x) -> XOR(x,true)
11: OR(x,y) -> XOR(and(x,y),xor(x,y))
12: OR(x,y) -> AND(x,y)
13: OR(x,y) -> XOR(x,y)
14: IMPLIES(x,y) -> XOR(and(x,y),xor(x,true))
15: IMPLIES(x,y) -> AND(x,y)
16: IMPLIES(x,y) -> XOR(x,true)
17: AND(xor(x,y),z) -> XOR(and(x,z),and(y,z))
18: AND(xor(x,y),z) -> AND(x,z)
19: AND(xor(x,y),z) -> AND(y,z)

The approximated dependency graph contains one SCC:
{18,19}.

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

Hence the TRS is terminating.