Problem:
 not(T()) -> F()
 not(F()) -> T()
 or(x,T()) -> T()
 or(x,F()) -> x
 or(x,y) -> or(y,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))
 imply(x,y) -> or(not(x),y)

Proof:
 sorted: (order)
 0:not(T()) -> F()
   not(F()) -> T()
   or(x,T()) -> T()
   or(x,F()) -> x
   or(x,y) -> or(y,x)
   or(or(x,y),z) -> or(x,or(y,z))
   imply(x,y) -> or(not(x),y)
 1:and(x,T()) -> x
   and(x,F()) -> F()
   and(x,y) -> and(y,x)
   and(and(x,y),z) -> and(x,and(y,z))
 -----
 sorts
   [0>2, 1>7, 1>8, 2>3, 2>4, 4>5, 5>6, 5>7, 5>8]
 sort attachment (non-strict)
   not : 5 -> 4
   T : 8
   F : 7
   or : 2 x 2 -> 2
   and : 1 x 1 -> 1
   imply : 6 x 3 -> 0
 -----
 0:not(T()) -> F()
   not(F()) -> T()
   or(x,T()) -> T()
   or(x,F()) -> x
   or(x,y) -> or(y,x)
   or(or(x,y),z) -> or(x,or(y,z))
   imply(x,y) -> or(not(x),y)
   AT confluence processor
    Complete TRS T' of input TRS:
    not(T()) -> F()
    not(F()) -> T()
    or(x,T()) -> T()
    or(x,F()) -> x
    imply(x,y) -> or(not(x),y)
    or(T(),x) -> T()
    or(F(),x) -> x
    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:not(T()) -> F()
           not(F()) -> T()
           or(x,T()) -> T()
           or(x,F()) -> x
           imply(x,y) -> or(not(x),y)
           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(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)
    
     CP(P union P^-1,S) = 
    or(T(),x) = T(), or(F(),x) = x, or(x,T()) = T(), or(x,F()) = x, or(x933,or(x934,T())) = 
    T(), or(x936,or(x937,F())) = or(x936,x937), or(or(T(),x948),x949) = 
    T(), or(or(F(),x951),x952) = or(x951,x952)
    
    
    We have to check termination of S:
    
    Matrix Interpretation Processor: dim=1
     
     interpretation:
      [imply](x0, x1) = 5x0 + 2x1 + 2,
      
      [or](x0, x1) = 2x0 + x1,
      
      [F] = 1,
      
      [not](x0) = 2x0 + 1,
      
      [T] = 3
     orientation:
      not(T()) = 7 >= 1 = F()
      
      not(F()) = 3 >= 3 = T()
      
      or(x,T()) = 2x + 3 >= 3 = T()
      
      or(x,F()) = 2x + 1 >= x = x
      
      imply(x,y) = 5x + 2y + 2 >= 4x + y + 2 = or(not(x),y)
      
      or(T(),x) = x + 6 >= 3 = T()
      
      or(F(),x) = x + 2 >= x = x
     problem:
      not(F()) -> T()
      or(x,T()) -> T()
      imply(x,y) -> or(not(x),y)
     Matrix Interpretation Processor: dim=1
      
      interpretation:
       [imply](x0, x1) = 4x0 + x1 + 1,
       
       [or](x0, x1) = 2x0 + x1 + 1,
       
       [F] = 4,
       
       [not](x0) = 2x0,
       
       [T] = 0
      orientation:
       not(F()) = 8 >= 0 = T()
       
       or(x,T()) = 2x + 1 >= 0 = T()
       
       imply(x,y) = 4x + y + 1 >= 4x + y + 1 = or(not(x),y)
      problem:
       imply(x,y) -> or(not(x),y)
      Matrix Interpretation Processor: dim=1
       
       interpretation:
        [imply](x0, x1) = x0 + x1 + 1,
        
        [or](x0, x1) = x0 + x1,
        
        [not](x0) = x0
       orientation:
        imply(x,y) = x + y + 1 >= x + y = or(not(x),y)
       problem:
        
       Qed
 
 
 1: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(),x) -> x
    and(F(),x) -> 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(),x) -> x
           and(F(),x) -> F()
    
    S is 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)
    
     CP(P union P^-1,S) = 
    and(T(),x) = x, and(F(),x) = F(), and(x,T()) = x, and(x,F()) = F(), 
    and(x1125,and(x1126,T())) = and(x1125,x1126), and(x1128,and(x1129,F())) = 
    F(), and(and(T(),x1140),x1141) = and(x1140,x1141), and(and(F(),x1143),x1144) = 
    F()
    
    
    We have to check termination of S:
    
    Matrix Interpretation Processor: dim=1
     
     interpretation:
      [and](x0, x1) = 4x0 + x1,
      
      [F] = 0,
      
      [T] = 1
     orientation:
      and(x,T()) = 4x + 1 >= x = x
      
      and(x,F()) = 4x >= 0 = F()
      
      and(T(),x) = x + 4 >= x = x
      
      and(F(),x) = x >= 0 = F()
     problem:
      and(x,F()) -> F()
      and(F(),x) -> F()
     Matrix Interpretation Processor: dim=1
      
      interpretation:
       [and](x0, x1) = 4x0 + 4x1,
       
       [F] = 2
      orientation:
       and(x,F()) = 4x + 8 >= 2 = F()
       
       and(F(),x) = 4x + 8 >= 2 = F()
      problem:
       
      Qed