Problem:
 or(x,T()) -> T()
 or(x,F()) -> x
 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(),x) -> T()
  or(F(),x) -> x
  or(x,y) -> or(y,x)
  
   T' = (P union S) with
  
   TRS P:or(x,y) -> or(y,x)
  
   TRS S:or(x,T()) -> T()
         or(x,F()) -> x
         or(T(),x) -> T()
         or(F(),x) -> x
  
  S is linear and P is reversible.
  
   CP(S,S) = 
  T() = T(), F() = F()
  
   CP(S,P union P^-1) = 
  T() = or(T(),x), T() = or(T(),y), x = or(F(),x), y = or(F(),y), T() = 
  or(y,T()), T() = or(x,T()), y = or(y,F()), x = or(x,F())
  
   CP(P union P^-1,S) = 
  or(T(),x) = T(), or(F(),x) = x, or(x,T()) = T(), or(x,F()) = x
  
  
  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(),x) = 2x + 5 >= 2 = T()
    
    or(F(),x) = 2x + 11 >= x = x
   problem:
    
   Qed