YES

Problem:
 not(x) -> xor(x,true())
 implies(x,y) -> xor(and(x,y),xor(x,true()))
 or(x,y) -> xor(and(x,y),xor(x,y))
 =(x,y) -> xor(x,xor(y,true()))

Proof:
 DP Processor:
  DPs:
   
  TRS:
   not(x) -> xor(x,true())
   implies(x,y) -> xor(and(x,y),xor(x,true()))
   or(x,y) -> xor(and(x,y),xor(x,y))
   =(x,y) -> xor(x,xor(y,true()))
  Qed