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()))}
 MPO:
  Prec:
   or > xor, 
   or > and, 
   not > true, 
   not > xor, 
   implies > and, 
   implies > true, 
   implies > xor, 
   = > true, 
   = > xor
   empty
  Strict:
   {}
   Weak:
    {}
  Qed