Problem:
 not(T()) -> F()
 not(F()) -> T()
 not(not(x)) -> x
 exor(x,T()) -> not(x)
 exor(x,F()) -> x
 exor(not(x),y) -> not(exor(x,y))
 exor(exor(x,y),z) -> exor(x,exor(y,z))
 exor(x,y) -> exor(y,x)

Proof:
 AT confluence processor
  Complete TRS T' of input TRS:
  not(T()) -> F()
  not(F()) -> T()
  not(not(x)) -> x
  exor(x,T()) -> not(x)
  exor(x,F()) -> x
  exor(not(x),y) -> not(exor(x,y))
  exor(T(),y) -> not(y)
  exor(F(),y) -> y
  exor(x,not(x111)) -> not(exor(x,x111))
  exor(exor(x,y),z) -> exor(x,exor(y,z))
  exor(x,y) -> exor(y,x)
  
   T' = (P union S) with
  
   TRS P:exor(exor(x,y),z) -> exor(x,exor(y,z))
         exor(x,y) -> exor(y,x)
  
   TRS S:not(T()) -> F()
         not(F()) -> T()
         not(not(x)) -> x
         exor(x,T()) -> not(x)
         exor(x,F()) -> x
         exor(not(x),y) -> not(exor(x,y))
         exor(T(),y) -> not(y)
         exor(F(),y) -> y
         exor(x,not(x111)) -> not(exor(x,x111))
  
  S is left-linear and P is reversible.
  
   CP(S,S) = 
  not(F()) = T(), exor(F(),y) = not(exor(T(),y)), exor(x,F()) = not(exor(x,T())), 
  not(T()) = F(), exor(T(),y) = not(exor(F(),y)), exor(x,T()) = not(exor(x,F())), 
  not(x648) = not(x648), exor(x649,y) = not(exor(not(x649),y)), exor(x,x650) = 
  not(exor(x,not(x650))), not(not(x)) = not(exor(x,T())), not(T()) = 
  not(T()), not(x) = not(exor(x,F())), T() = not(F()), F() = F(), not(exor(x657,T())) = 
  not(not(x657)), not(exor(x659,F())) = not(x659), not(exor(x661,not(x111))) = 
  not(exor(not(x661),x111)), not(not(x111)) = not(exor(T(),x111)), not(x111) = 
  not(exor(F(),x111)), not(exor(not(x),x670)) = not(exor(x,not(x670))), 
  not(exor(T(),x672)) = not(not(x672)), not(exor(F(),x674)) = not(x674)
  
   CP(S,P union P^-1) = 
  not(exor(x,y)) = exor(x,exor(y,T())), exor(not(x),z) = exor(x,exor(T(),z)), 
  not(x) = exor(T(),x), exor(x,not(y)) = exor(exor(x,y),T()), not(y) = 
  exor(T(),y), exor(x,y) = exor(x,exor(y,F())), exor(x,z) = exor(x,exor(F(),z)), 
  x = exor(F(),x), exor(x,y) = exor(exor(x,y),F()), y = exor(F(),y), 
  exor(not(exor(x739,y)),z) = exor(not(x739),exor(y,z)), not(exor(x741,y)) = 
  exor(y,not(x741)), not(exor(x743,exor(y,z))) = exor(exor(not(x743),y),z), 
  exor(x,not(exor(x745,z))) = exor(exor(x,not(x745)),z), not(exor(x747,x)) = 
  exor(x,not(x747)), exor(not(y),z) = exor(T(),exor(y,z)), not(y) = exor(y,T()), 
  not(exor(y,z)) = exor(exor(T(),y),z), exor(x,not(z)) = exor(exor(x,T()),z), 
  not(x) = exor(x,T()), exor(y,z) = exor(F(),exor(y,z)), y = exor(y,F()), 
  exor(y,z) = exor(exor(F(),y),z), exor(x,z) = exor(exor(x,F()),z), x = 
  exor(x,F()), not(exor(exor(x,y),x760)) = exor(x,exor(y,not(x760))), 
  exor(not(exor(x,x762)),z) = exor(x,exor(not(x762),z)), not(exor(x,x764)) = 
  exor(not(x764),x), exor(x,not(exor(y,x766))) = exor(exor(x,y),not(x766)), 
  not(exor(y,x768)) = exor(not(x768),y)
  
  
   PCP_in(P union P^-1,S) = 
  
  
  We have to check termination of S:
  
  Matrix Interpretation Processor: dim=1
   
   interpretation:
    [exor](x0, x1) = x0 + 5x1 + 1,
    
    [F] = 4,
    
    [not](x0) = x0 + 4,
    
    [T] = 5
   orientation:
    not(T()) = 9 >= 4 = F()
    
    not(F()) = 8 >= 5 = T()
    
    not(not(x)) = x + 8 >= x = x
    
    exor(x,T()) = x + 26 >= x + 4 = not(x)
    
    exor(x,F()) = x + 21 >= x = x
    
    exor(not(x),y) = x + 5y + 5 >= x + 5y + 5 = not(exor(x,y))
    
    exor(T(),y) = 5y + 6 >= y + 4 = not(y)
    
    exor(F(),y) = 5y + 5 >= y = y
    
    exor(x,not(x111)) = x + 5x111 + 21 >= x + 5x111 + 5 = not(exor(x,x111))
   problem:
    exor(not(x),y) -> not(exor(x,y))
   Matrix Interpretation Processor: dim=1
    
    interpretation:
     [exor](x0, x1) = 2x0 + 4x1 + 5,
     
     [not](x0) = x0 + 1
    orientation:
     exor(not(x),y) = 2x + 4y + 7 >= 2x + 4y + 6 = not(exor(x,y))
    problem:
     
    Qed