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()))}
 POP*:
  Quasi-Precedence:
  or > xor, 
  or > and, 
  not > true, 
  not > xor, 
  implies > and, 
  implies > true, 
  implies > xor, 
  = > true, 
  = > xor
  empty
  
Normal:
   pi(=) = [1,2], pi(or) = [1,2], pi(implies) = [1,2], pi(not) = [1]
  
Safe:
   pi(and) = [1,2], pi(xor) = [1,2]
  
Predicative System:
   {      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