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:
 Complexity 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
   max_matrix:
    1
    interpretation:
     [+](x0, x1) = x0 + x1,
     
     [s](x0) = x0,
     
     [odd](x0) = x0,
     
     [0] = 1,
     
     [false] = 0,
     
     [not](x0) = x0,
     
     [true] = 1
    orientation:
     not(true()) = 1 >= 0 = false()
     
     not(false()) = 0 >= 1 = true()
     
     odd(0()) = 1 >= 0 = false()
     
     odd(s(x)) = x >= x = not(odd(x))
     
     +(x,0()) = x + 1 >= x = x
     
     +(x,s(y)) = x + y >= x + y = s(+(x,y))
     
     +(s(x),y) = x + y >= x + y = s(+(x,y))
    problem:
     strict:
      not(false()) -> true()
      odd(s(x)) -> not(odd(x))
      +(x,s(y)) -> s(+(x,y))
      +(s(x),y) -> s(+(x,y))
     weak:
      not(true()) -> false()
      odd(0()) -> false()
      +(x,0()) -> x
    Matrix Interpretation Processor:
     dimension: 1
     max_matrix:
      1
      interpretation:
       [+](x0, x1) = x0 + x1,
       
       [s](x0) = x0 + 1,
       
       [odd](x0) = x0,
       
       [0] = 0,
       
       [false] = 0,
       
       [not](x0) = x0,
       
       [true] = 0
      orientation:
       not(false()) = 0 >= 0 = true()
       
       odd(s(x)) = x + 1 >= x = not(odd(x))
       
       +(x,s(y)) = x + y + 1 >= x + y + 1 = s(+(x,y))
       
       +(s(x),y) = x + y + 1 >= x + y + 1 = s(+(x,y))
       
       not(true()) = 0 >= 0 = false()
       
       odd(0()) = 0 >= 0 = false()
       
       +(x,0()) = x >= x = x
      problem:
       strict:
        not(false()) -> true()
        +(x,s(y)) -> s(+(x,y))
        +(s(x),y) -> s(+(x,y))
       weak:
        odd(s(x)) -> not(odd(x))
        not(true()) -> false()
        odd(0()) -> false()
        +(x,0()) -> x
      Matrix Interpretation Processor:
       dimension: 1
       max_matrix:
        1
        interpretation:
         [+](x0, x1) = x0 + x1,
         
         [s](x0) = x0 + 1,
         
         [odd](x0) = x0 + 1,
         
         [0] = 0,
         
         [false] = 0,
         
         [not](x0) = x0 + 1,
         
         [true] = 0
        orientation:
         not(false()) = 1 >= 0 = true()
         
         +(x,s(y)) = x + y + 1 >= x + y + 1 = s(+(x,y))
         
         +(s(x),y) = x + y + 1 >= x + y + 1 = s(+(x,y))
         
         odd(s(x)) = x + 2 >= x + 2 = not(odd(x))
         
         not(true()) = 1 >= 0 = false()
         
         odd(0()) = 1 >= 0 = false()
         
         +(x,0()) = x >= x = x
        problem:
         strict:
          +(x,s(y)) -> s(+(x,y))
          +(s(x),y) -> s(+(x,y))
         weak:
          not(false()) -> true()
          odd(s(x)) -> not(odd(x))
          not(true()) -> false()
          odd(0()) -> false()
          +(x,0()) -> x
        Matrix Interpretation Processor:
         dimension: 2
         max_matrix:
          [1 1]
          [0 1]
          interpretation:
                              [1 1]  
           [+](x0, x1) = x0 + [0 1]x1,
           
                          [0]
           [s](x0) = x0 + [1],
           
                       [1 1]     [0]
           [odd](x0) = [0 0]x0 + [1],
           
                 [1]
           [0] = [0],
           
                     [1]
           [false] = [0],
           
                       [1 0]     [1]
           [not](x0) = [0 0]x0 + [0],
           
                    [0]
           [true] = [0]
          orientation:
                           [1 1]    [1]        [1 1]    [0]            
           +(x,s(y)) = x + [0 1]y + [1] >= x + [0 1]y + [1] = s(+(x,y))
           
                           [1 1]    [0]        [1 1]    [0]            
           +(s(x),y) = x + [0 1]y + [1] >= x + [0 1]y + [1] = s(+(x,y))
           
                          [2]    [0]         
           not(false()) = [0] >= [0] = true()
           
                       [1 1]    [1]    [1 1]    [1]              
           odd(s(x)) = [0 0]x + [1] >= [0 0]x + [0] = not(odd(x))
           
                         [1]    [1]          
           not(true()) = [0] >= [0] = false()
           
                      [1]    [1]          
           odd(0()) = [1] >= [0] = false()
           
                          [1]         
           +(x,0()) = x + [0] >= x = x
          problem:
           strict:
            +(s(x),y) -> s(+(x,y))
           weak:
            +(x,s(y)) -> s(+(x,y))
            not(false()) -> true()
            odd(s(x)) -> not(odd(x))
            not(true()) -> false()
            odd(0()) -> false()
            +(x,0()) -> x
          Matrix Interpretation Processor:
           dimension: 2
           max_matrix:
            [1 1]
            [0 1]
            interpretation:
                           [1 1]       
             [+](x0, x1) = [0 1]x0 + x1,
             
                            [0]
             [s](x0) = x0 + [1],
             
                              [0]
             [odd](x0) = x0 + [1],
             
                   [1]
             [0] = [1],
             
                       [1]
             [false] = [0],
             
                           
             [not](x0) = x0,
             
                      [1]
             [true] = [0]
            orientation:
                         [1 1]        [1]    [1 1]        [0]            
             +(s(x),y) = [0 1]x + y + [1] >= [0 1]x + y + [1] = s(+(x,y))
             
                         [1 1]        [0]    [1 1]        [0]            
             +(x,s(y)) = [0 1]x + y + [1] >= [0 1]x + y + [1] = s(+(x,y))
             
                            [1]    [1]         
             not(false()) = [0] >= [0] = true()
             
                             [0]        [0]              
             odd(s(x)) = x + [2] >= x + [1] = not(odd(x))
             
                           [1]    [1]          
             not(true()) = [0] >= [0] = false()
             
                        [1]    [1]          
             odd(0()) = [2] >= [0] = false()
             
                        [1 1]    [1]         
             +(x,0()) = [0 1]x + [1] >= x = x
            problem:
             strict:
              
             weak:
              +(s(x),y) -> s(+(x,y))
              +(x,s(y)) -> s(+(x,y))
              not(false()) -> true()
              odd(s(x)) -> not(odd(x))
              not(true()) -> false()
              odd(0()) -> false()
              +(x,0()) -> x
            Qed