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

Proof:
 AT confluence processor
  Complete TRS T' of input TRS:
  or(x,T()) -> T()
  or(x,F()) -> x
  or(T(),y) -> T()
  or(F(),y) -> y
  or(or(x,y),z) -> or(x,or(y,z))
  or(x,y) -> or(y,x)
  
   T' = (P union S) with
  
   TRS P:or(or(x,y),z) -> or(x,or(y,z))
         or(x,y) -> or(y,x)
  
   TRS S:or(x,T()) -> T()
         or(x,F()) -> x
         or(T(),y) -> T()
         or(F(),y) -> y
  
  S is left-linear and P is reversible.
  
   CP(S,S) = 
  T() = T(), F() = F()
  
   CP(S,P union P^-1) = 
  T() = or(x,or(y,T())), or(T(),z) = or(x,or(T(),z)), T() = or(T(),x), 
  or(x,T()) = or(or(x,y),T()), T() = or(T(),y), or(x,y) = or(x,or(y,F())), 
  or(x,z) = or(x,or(F(),z)), x = or(F(),x), or(x,y) = or(or(x,y),F()), 
  y = or(F(),y), or(T(),z) = or(T(),or(y,z)), T() = or(y,T()), T() = 
  or(or(T(),y),z), or(x,T()) = or(or(x,T()),z), T() = or(x,T()), or(y,z) = 
  or(F(),or(y,z)), y = or(y,F()), or(y,z) = or(or(F(),y),z), or(x,z) = 
  or(or(x,F()),z), x = or(x,F())
  
  
   PCP_in(P union P^-1,S) = 
  
  
  We have to check termination of S:
  
  Matrix Interpretation Processor: dim=1
   
   interpretation:
    [F] = 5,
    
    [or](x0, x1) = 2x0 + 2x1 + 1,
    
    [T] = 2
   orientation:
    or(x,T()) = 2x + 5 >= 2 = T()
    
    or(x,F()) = 2x + 11 >= x = x
    
    or(T(),y) = 2y + 5 >= 2 = T()
    
    or(F(),y) = 2y + 11 >= y = y
   problem:
    
   Qed