YES
(VAR x y z)
(RULES 
xor(x,F) -> x
xor(x,neg(x)) -> F
and(x,T) -> x
and(x,F) -> F
and(x,x) -> x
and(xor(x,y),z) -> xor(and(x,z),and(y,z))
xor(x,x) -> F
impl(x,y) -> xor(and(x,y),xor(x,T))
or(x,y) -> xor(and(x,y),xor(x,y))
equiv(x,y) -> xor(x,xor(y,T))
neg(x) -> xor(x,T)
)

Proving termination of rewriting for boolean_rings:

-> Dependency pairs:
nF_and(xor(x,y),z) -> nF_xor(and(x,z),and(y,z))
nF_and(xor(x,y),z) -> nF_and(x,z)
nF_and(xor(x,y),z) -> nF_and(y,z)
nF_impl(x,y) -> nF_xor(and(x,y),xor(x,T))
nF_impl(x,y) -> nF_and(x,y)
nF_impl(x,y) -> nF_xor(x,T)
nF_or(x,y) -> nF_xor(and(x,y),xor(x,y))
nF_or(x,y) -> nF_and(x,y)
nF_or(x,y) -> nF_xor(x,y)
nF_equiv(x,y) -> nF_xor(x,xor(y,T))
nF_equiv(x,y) -> nF_xor(y,T)
nF_neg(x) -> nF_xor(x,T)

-> Proof of termination for boolean_rings_1:
-> -> Dependency pairs in cycle:
nF_and(xor(x,y),z) -> nF_and(x,z)
nF_and(xor(x,y),z) -> nF_and(y,z)

Termination proved: Cycles verify subterm criterion.

SETTINGS:
Base ordering: Polynomial ordering
Proof mode: SCCs in DG + base ordering
Upper bound for coeffs: 1
Rationals below 1 for all non-replacing args: No
Polynomial interpretation: Linear
Coeffs in polynomials: No rationals
Delta: automatic



Termination was proved succesfully.