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* + Boolean Semantic Labelling:
  Normal positions:
  pi(=_sl=1) = [1,2], pi(=_sl=0) = [1,2], pi(or_sl=1) = [1,2], pi(or_sl=0) = [1,2], pi(implies_sl=1) = [1,2], pi(implies_sl=0) = [1,2], pi(not_sl=1) = [1], pi(not_sl=0) = [1]
  
Safe positions:
   pi(and_sl=1) = [1,2], pi(and_sl=0) = [1,2], pi(xor_sl=1) = [1,2], pi(xor_sl=0) = [1,2]
  
Precedence:
   or_sl=0 > xor_sl=0, 
   or_sl=0 > and_sl=0, 
   not_sl=0 > true_sl=0, 
   not_sl=0 > xor_sl=0, 
   implies_sl=0 > and_sl=0, 
   implies_sl=0 > true_sl=0, 
   implies_sl=0 > xor_sl=0, 
   =_sl=0 > true_sl=0, 
   =_sl=0 > xor_sl=0
   empty
  
Interpretation:
   xor^(2):
   00 | 0
   01 | 0
   10 | 0
   11 | 0
   true^(0):
    | 0
   not^(1):
   0 | 0
   1 | 0
   and^(2):
   00 | 0
   01 | 0
   10 | 0
   11 | 1
   implies^(2):
   00 | 0
   01 | 0
   10 | 0
   11 | 0
   or^(2):
   00 | 0
   01 | 0
   10 | 0
   11 | 0
   =^(2):
   00 | 0
   01 | 0
   10 | 0
   11 | 0
   
  
Labelling:
   xor^(2):
   00 | 0
   01 | 0
   10 | 0
   11 | 0
   true^(0):
    | 0
   not^(1):
   0 | 0
   1 | 0
   and^(2):
   00 | 0
   01 | 0
   10 | 0
   11 | 0
   implies^(2):
   00 | 0
   01 | 0
   10 | 0
   11 | 0
   or^(2):
   00 | 0
   01 | 0
   10 | 0
   11 | 0
   =^(2):
   00 | 0
   01 | 0
   10 | 0
   11 | 0
   
  
Labelled predicative System:
   {      not_sl=0(x;) -> xor_sl=0(;x,true_sl=0()),
          not_sl=0(x;) -> xor_sl=0(;x,true_sl=0()),
    implies_sl=0(x,y;) -> xor_sl=0(;and_sl=0(;x,y),xor_sl=0(;x,true_sl=0())),
    implies_sl=0(x,y;) -> xor_sl=0(;and_sl=0(;x,y),xor_sl=0(;x,true_sl=0())),
    implies_sl=0(x,y;) -> xor_sl=0(;and_sl=0(;x,y),xor_sl=0(;x,true_sl=0())),
    implies_sl=0(x,y;) -> xor_sl=0(;and_sl=0(;x,y),xor_sl=0(;x,true_sl=0())),
         or_sl=0(x,y;) -> xor_sl=0(;and_sl=0(;x,y),xor_sl=0(;x,y)),
         or_sl=0(x,y;) -> xor_sl=0(;and_sl=0(;x,y),xor_sl=0(;x,y)),
         or_sl=0(x,y;) -> xor_sl=0(;and_sl=0(;x,y),xor_sl=0(;x,y)),
         or_sl=0(x,y;) -> xor_sl=0(;and_sl=0(;x,y),xor_sl=0(;x,y)),
          =_sl=0(x,y;) -> xor_sl=0(;x,xor_sl=0(;y,true_sl=0())),
          =_sl=0(x,y;) -> xor_sl=0(;x,xor_sl=0(;y,true_sl=0())),
          =_sl=0(x,y;) -> xor_sl=0(;x,xor_sl=0(;y,true_sl=0())),
          =_sl=0(x,y;) -> xor_sl=0(;x,xor_sl=0(;y,true_sl=0()))}
  

  Qed