YES

Problem:
 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())

Proof:
 DP Processor:
  DPs:
   and#(xor(x,y),z) -> and#(y,z)
   and#(xor(x,y),z) -> and#(x,z)
   and#(xor(x,y),z) -> xor#(and(x,z),and(y,z))
   impl#(x,y) -> xor#(x,T())
   impl#(x,y) -> and#(x,y)
   impl#(x,y) -> xor#(and(x,y),xor(x,T()))
   or#(x,y) -> xor#(x,y)
   or#(x,y) -> and#(x,y)
   or#(x,y) -> xor#(and(x,y),xor(x,y))
   equiv#(x,y) -> xor#(y,T())
   equiv#(x,y) -> xor#(x,xor(y,T()))
   neg#(x) -> xor#(x,T())
  TRS:
   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())
  Usable Rule Processor:
   DPs:
    and#(xor(x,y),z) -> and#(y,z)
    and#(xor(x,y),z) -> and#(x,z)
    and#(xor(x,y),z) -> xor#(and(x,z),and(y,z))
    impl#(x,y) -> xor#(x,T())
    impl#(x,y) -> and#(x,y)
    impl#(x,y) -> xor#(and(x,y),xor(x,T()))
    or#(x,y) -> xor#(x,y)
    or#(x,y) -> and#(x,y)
    or#(x,y) -> xor#(and(x,y),xor(x,y))
    equiv#(x,y) -> xor#(y,T())
    equiv#(x,y) -> xor#(x,xor(y,T()))
    neg#(x) -> xor#(x,T())
   TRS:
    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,F()) -> x
    xor(x,neg(x)) -> F()
    xor(x,x) -> F()
   KBO Processor:
    argument filtering:
     pi(F) = []
     pi(xor) = [0,1]
     pi(neg) = 0
     pi(T) = []
     pi(and) = 0
     pi(xor#) = []
     pi(and#) = [0,1]
     pi(impl#) = [0,1]
     pi(or#) = [0,1]
     pi(equiv#) = []
     pi(neg#) = []
    usable rules:
     
    weight function:
     w0 = 1
     w(neg#) = w(equiv#) = w(impl#) = w(xor#) = w(and) = w(T) = w(neg) = w(
     F) = 1
     w(or#) = w(and#) = w(xor) = 0
    precedence:
     neg# ~ equiv# ~ or# ~ impl# ~ and ~ T ~ xor ~ F > and# ~ xor# ~ neg
    problem:
     DPs:
      
     TRS:
      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,F()) -> x
      xor(x,neg(x)) -> F()
      xor(x,x) -> F()
    Qed