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

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