YES(?,O(n^2))

Problem:
 not(true()) -> false()
 not(false()) -> true()
 odd(0()) -> false()
 odd(s(x)) -> not(odd(x))
 +(x,0()) -> x
 +(x,s(y)) -> s(+(x,y))
 +(s(x),y) -> s(+(x,y))

Proof:
 RT Transformation Processor:
  strict:
   not(true()) -> false()
   not(false()) -> true()
   odd(0()) -> false()
   odd(s(x)) -> not(odd(x))
   +(x,0()) -> x
   +(x,s(y)) -> s(+(x,y))
   +(s(x),y) -> s(+(x,y))
  weak:
   
  Matrix Interpretation Processor:
   dimension: 1
   interpretation:
    [+](x0, x1) = x0 + x1 + 16,
    
    [s](x0) = x0 + 8,
    
    [odd](x0) = x0 + 28,
    
    [0] = 0,
    
    [false] = 12,
    
    [not](x0) = x0 + 22,
    
    [true] = 8
   orientation:
    not(true()) = 30 >= 12 = false()
    
    not(false()) = 34 >= 8 = true()
    
    odd(0()) = 28 >= 12 = false()
    
    odd(s(x)) = x + 36 >= x + 50 = not(odd(x))
    
    +(x,0()) = x + 16 >= x = x
    
    +(x,s(y)) = x + y + 24 >= x + y + 24 = s(+(x,y))
    
    +(s(x),y) = x + y + 24 >= x + y + 24 = s(+(x,y))
   problem:
    strict:
     odd(s(x)) -> not(odd(x))
     +(x,s(y)) -> s(+(x,y))
     +(s(x),y) -> s(+(x,y))
    weak:
     not(true()) -> false()
     not(false()) -> true()
     odd(0()) -> false()
     +(x,0()) -> x
   Matrix Interpretation Processor:
    dimension: 1
    interpretation:
     [+](x0, x1) = x0 + x1 + 8,
     
     [s](x0) = x0 + 1,
     
     [odd](x0) = x0 + 4,
     
     [0] = 24,
     
     [false] = 0,
     
     [not](x0) = x0,
     
     [true] = 0
    orientation:
     odd(s(x)) = x + 5 >= x + 4 = not(odd(x))
     
     +(x,s(y)) = x + y + 9 >= x + y + 9 = s(+(x,y))
     
     +(s(x),y) = x + y + 9 >= x + y + 9 = s(+(x,y))
     
     not(true()) = 0 >= 0 = false()
     
     not(false()) = 0 >= 0 = true()
     
     odd(0()) = 28 >= 0 = false()
     
     +(x,0()) = x + 32 >= x = x
    problem:
     strict:
      +(x,s(y)) -> s(+(x,y))
      +(s(x),y) -> s(+(x,y))
     weak:
      odd(s(x)) -> not(odd(x))
      not(true()) -> false()
      not(false()) -> true()
      odd(0()) -> false()
      +(x,0()) -> x
    Matrix Interpretation Processor:
     dimension: 2
     interpretation:
                    [1 1]          [8]
      [+](x0, x1) = [0 1]x0 + x1 + [4],
      
                     [0]
      [s](x0) = x0 + [8],
      
                    
      [odd](x0) = x0,
      
            [12]
      [0] = [0 ],
      
                [2]
      [false] = [0],
      
                  [1 0]     [0]
      [not](x0) = [0 0]x0 + [8],
      
               [2]
      [true] = [8]
     orientation:
                  [1 1]        [8 ]    [1 1]        [8 ]            
      +(x,s(y)) = [0 1]x + y + [12] >= [0 1]x + y + [12] = s(+(x,y))
      
                  [1 1]        [16]    [1 1]        [8 ]            
      +(s(x),y) = [0 1]x + y + [12] >= [0 1]x + y + [12] = s(+(x,y))
      
                      [0]    [1 0]    [0]              
      odd(s(x)) = x + [8] >= [0 0]x + [8] = not(odd(x))
      
                    [2]    [2]          
      not(true()) = [8] >= [0] = false()
      
                     [2]    [2]         
      not(false()) = [8] >= [8] = true()
      
                 [12]    [2]          
      odd(0()) = [0 ] >= [0] = false()
      
                 [1 1]    [20]         
      +(x,0()) = [0 1]x + [4 ] >= x = x
     problem:
      strict:
       +(x,s(y)) -> s(+(x,y))
      weak:
       +(s(x),y) -> s(+(x,y))
       odd(s(x)) -> not(odd(x))
       not(true()) -> false()
       not(false()) -> true()
       odd(0()) -> false()
       +(x,0()) -> x
     Matrix Interpretation Processor:
      dimension: 2
      interpretation:
                          [1 2]     [3]
       [+](x0, x1) = x0 + [0 1]x1 + [0],
       
                      [1]
       [s](x0) = x0 + [5],
       
                   [1 3]     [5]
       [odd](x0) = [0 0]x0 + [1],
       
             [1]
       [0] = [3],
       
                 [1]
       [false] = [0],
       
                   [1 3]     [12]
       [not](x0) = [0 0]x0 + [1 ],
       
                [8]
       [true] = [0]
      orientation:
                       [1 2]    [14]        [1 2]    [4]            
       +(x,s(y)) = x + [0 1]y + [5 ] >= x + [0 1]y + [5] = s(+(x,y))
       
                       [1 2]    [4]        [1 2]    [4]            
       +(s(x),y) = x + [0 1]y + [5] >= x + [0 1]y + [5] = s(+(x,y))
       
                   [1 3]    [21]    [1 3]    [20]              
       odd(s(x)) = [0 0]x + [1 ] >= [0 0]x + [1 ] = not(odd(x))
       
                     [20]    [1]          
       not(true()) = [1 ] >= [0] = false()
       
                      [13]    [8]         
       not(false()) = [1 ] >= [0] = true()
       
                  [15]    [1]          
       odd(0()) = [1 ] >= [0] = false()
       
                      [10]         
       +(x,0()) = x + [3 ] >= x = x
      problem:
       strict:
        
       weak:
        +(x,s(y)) -> s(+(x,y))
        +(s(x),y) -> s(+(x,y))
        odd(s(x)) -> not(odd(x))
        not(true()) -> false()
        not(false()) -> true()
        odd(0()) -> false()
        +(x,0()) -> x
      Qed