YES

Problem:
 or(true(),true()) -> true()
 or(x,y) -> or(y,x)

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