Consider the TRS R consisting of the rewrite rules

1: xor(x,F) -> x
2: xor(x,neg(x)) -> F
3: and(x,T) -> x
4: and(x,F) -> F
5: and(x,x) -> x
6: and(xor(x,y),z) -> xor(and(x,z),and(y,z))
7: xor(x,x) -> F
8: impl(x,y) -> xor(and(x,y),xor(x,T))
9: or(x,y) -> xor(and(x,y),xor(x,y))
10: equiv(x,y) -> xor(x,xor(y,T))
11: neg(x) -> xor(x,T)

There are 12 dependency pairs:

12: AND(xor(x,y),z) -> XOR(and(x,z),and(y,z))
13: AND(xor(x,y),z) -> AND(x,z)
14: AND(xor(x,y),z) -> AND(y,z)
15: IMPL(x,y) -> XOR(and(x,y),xor(x,T))
16: IMPL(x,y) -> AND(x,y)
17: IMPL(x,y) -> XOR(x,T)
18: OR(x,y) -> XOR(and(x,y),xor(x,y))
19: OR(x,y) -> AND(x,y)
20: OR(x,y) -> XOR(x,y)
21: EQUIV(x,y) -> XOR(x,xor(y,T))
22: EQUIV(x,y) -> XOR(y,T)
23: NEG(x) -> XOR(x,T)

The approximated dependency graph contains one SCC:
{13,14}.

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

Hence the TRS is terminating.