YES
Time: 0.000430
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()))}
 DP:
  DP:
   {}
  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