YES

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

Proof:
 sorted: (order-sorted)
 0:and(x,T()) -> x
   and(x,F()) -> F()
   and(x,y) -> and(y,x)
   and(and(x,y),z) -> and(x,and(y,z))
 1:or(x,y) -> or(y,x)
   or(x,T()) -> T()
   or(x,F()) -> x
   or(or(x,y),z) -> or(x,or(y,z))
 -----
 sorts
   [0>2, 0>3, 1>2, 1>3]
 sort attachment (non-strict)
   or : 1 x 1 -> 1
   T : 3
   F : 2
   and : 0 x 0 -> 0
 -----
 0:and(x,T()) -> x
   and(x,F()) -> F()
   and(x,y) -> and(y,x)
   and(and(x,y),z) -> and(x,and(y,z))
   AT confluence processor
    Complete TRS T' of input TRS:
    and(x,T()) -> x
    and(x,F()) -> F()
    and(T(),y) -> y
    and(F(),y) -> F()
    and(x,y) -> and(y,x)
    and(and(x,y),z) -> and(x,and(y,z))
    
     T' = (P union S) with
    
     TRS P:and(x,y) -> and(y,x)
           and(and(x,y),z) -> and(x,and(y,z))
    
     TRS S:and(x,T()) -> x
           and(x,F()) -> F()
           and(T(),y) -> y
           and(F(),y) -> F()
    
    S is left-linear and P is reversible.
    
     CP(S,S) = 
    T() = T(), F() = F()
    
     CP(S,P union P^-1) = 
    x = and(T(),x), and(x,y) = and(x,and(y,T())), and(x,z) = and(x,and(T(),z)), 
    y = and(T(),y), and(x,y) = and(and(x,y),T()), F() = and(F(),x), F() = 
    and(x,and(y,F())), and(F(),z) = and(x,and(F(),z)), F() = and(F(),y), 
    and(x,F()) = and(and(x,y),F()), y = and(y,T()), and(y,z) = and(T(),and(y,z)), 
    x = and(x,T()), and(y,z) = and(and(T(),y),z), and(x,z) = and(and(x,T()),z), 
    F() = and(y,F()), and(F(),z) = and(F(),and(y,z)), F() = and(x,F()), 
    F() = and(and(F(),y),z), and(x,F()) = and(and(x,F()),z)
    
    
     PCP_in(P union P^-1,S) = 
    
    
    We have to check termination of S:
    
    Matrix Interpretation Processor: dim=1
     
     interpretation:
      [T] = 1,
      
      [and](x0, x1) = 5x0 + 5x1,
      
      [F] = 0
     orientation:
      and(x,T()) = 5x + 5 >= x = x
      
      and(x,F()) = 5x >= 0 = F()
      
      and(T(),y) = 5y + 5 >= y = y
      
      and(F(),y) = 5y >= 0 = F()
     problem:
      and(x,F()) -> F()
      and(F(),y) -> F()
     Matrix Interpretation Processor: dim=1
      
      interpretation:
       [and](x0, x1) = 2x0 + 4x1 + 6,
       
       [F] = 5
      orientation:
       and(x,F()) = 2x + 26 >= 5 = F()
       
       and(F(),y) = 4y + 16 >= 5 = F()
      problem:
       
      Qed
  
  
  1:or(x,y) -> or(y,x)
    or(x,T()) -> T()
    or(x,F()) -> x
    or(or(x,y),z) -> or(x,or(y,z))
    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(x,y) -> or(y,x)
     or(or(x,y),z) -> or(x,or(y,z))
     
      T' = (P union S) with
     
      TRS P:or(x,y) -> or(y,x)
            or(or(x,y),z) -> or(x,or(y,z))
     
      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(T(),x), T() = or(x,or(y,T())), or(T(),z) = or(x,or(T(),z)), 
     T() = or(T(),y), or(x,T()) = or(or(x,y),T()), x = or(F(),x), or(x,y) = 
     or(x,or(y,F())), or(x,z) = or(x,or(F(),z)), y = or(F(),y), or(x,y) = 
     or(or(x,y),F()), T() = or(y,T()), or(T(),z) = or(T(),or(y,z)), T() = 
     or(x,T()), T() = or(or(T(),y),z), or(x,T()) = or(or(x,T()),z), y = 
     or(y,F()), or(y,z) = or(F(),or(y,z)), x = or(x,F()), or(y,z) = or(or(F(),y),z), 
     or(x,z) = or(or(x,F()),z)
     
     
      PCP_in(P union P^-1,S) = 
     
     
     We have to check termination of S:
     
     Matrix Interpretation Processor: dim=1
      
      interpretation:
       [T] = 0,
       
       [or](x0, x1) = 2x0 + 4x1 + 5,
       
       [F] = 0
      orientation:
       or(x,T()) = 2x + 5 >= 0 = T()
       
       or(x,F()) = 2x + 5 >= x = x
       
       or(T(),y) = 4y + 5 >= 0 = T()
       
       or(F(),y) = 4y + 5 >= y = y
      problem:
       
      Qed