YES

Problem:
 or(x,T()) -> T()
 or(x,F()) -> x
 or(T(),x) -> T()
 or(F(),x) -> 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(),x) -> T()
  or(F(),x) -> x
  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(),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(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())
  
   CP(P union P^-1,S) = 
  or(x359,or(x360,T())) = T(), or(x362,or(x363,F())) = or(x362,x363), 
  or(T(),x) = T(), or(F(),x) = x, or(x,T()) = T(), or(x,F()) = x, or(or(T(),x374),x375) = 
  T(), or(or(F(),x377),x378) = or(x377,x378)
  
  
  We have to check termination of S:
  
  Matrix Interpretation Processor: dim=1
   
   interpretation:
    [or](x0, x1) = 2x0 + 4x1 + 1,
    
    [T] = 1,
    
    [F] = 3
   orientation:
    or(x,T()) = 2x + 5 >= 1 = T()
    
    or(x,F()) = 2x + 13 >= x = x
    
    or(T(),x) = 4x + 3 >= 1 = T()
    
    or(F(),x) = 4x + 7 >= x = x
   problem:
    
   Qed