YES(?,O(n^3))

Problem:
 not(true()) -> false()
 not(false()) -> true()
 evenodd(x,0()) -> not(evenodd(x,s(0())))
 evenodd(0(),s(0())) -> false()
 evenodd(s(x),s(0())) -> evenodd(x,0())

Proof:
 Complexity Transformation Processor:
  strict:
   not(true()) -> false()
   not(false()) -> true()
   evenodd(x,0()) -> not(evenodd(x,s(0())))
   evenodd(0(),s(0())) -> false()
   evenodd(s(x),s(0())) -> evenodd(x,0())
  weak:
   
  Matrix Interpretation Processor:
   dimension: 1
   max_matrix:
    1
    interpretation:
     [s](x0) = x0 + 1,
     
     [evenodd](x0, x1) = x0 + x1,
     
     [0] = 0,
     
     [false] = 0,
     
     [not](x0) = x0 + 1,
     
     [true] = 1
    orientation:
     not(true()) = 2 >= 0 = false()
     
     not(false()) = 1 >= 1 = true()
     
     evenodd(x,0()) = x >= x + 2 = not(evenodd(x,s(0())))
     
     evenodd(0(),s(0())) = 1 >= 0 = false()
     
     evenodd(s(x),s(0())) = x + 2 >= x = evenodd(x,0())
    problem:
     strict:
      not(false()) -> true()
      evenodd(x,0()) -> not(evenodd(x,s(0())))
     weak:
      not(true()) -> false()
      evenodd(0(),s(0())) -> false()
      evenodd(s(x),s(0())) -> evenodd(x,0())
    Matrix Interpretation Processor:
     dimension: 1
     max_matrix:
      1
      interpretation:
       [s](x0) = x0 + 1,
       
       [evenodd](x0, x1) = x0 + x1,
       
       [0] = 0,
       
       [false] = 1,
       
       [not](x0) = x0 + 1,
       
       [true] = 0
      orientation:
       not(false()) = 2 >= 0 = true()
       
       evenodd(x,0()) = x >= x + 2 = not(evenodd(x,s(0())))
       
       not(true()) = 1 >= 1 = false()
       
       evenodd(0(),s(0())) = 1 >= 1 = false()
       
       evenodd(s(x),s(0())) = x + 2 >= x = evenodd(x,0())
      problem:
       strict:
        evenodd(x,0()) -> not(evenodd(x,s(0())))
       weak:
        not(false()) -> true()
        not(true()) -> false()
        evenodd(0(),s(0())) -> false()
        evenodd(s(x),s(0())) -> evenodd(x,0())
      Matrix Interpretation Processor:
       dimension: 3
       max_matrix:
        [1 1 1]
        [0 0 0]
        [0 0 0]
        interpretation:
                   [1 0 1]     [0]
         [s](x0) = [0 0 0]x0 + [0]
                   [0 0 0]     [1],
         
                             [1 0 1]     [1 1 0]  
         [evenodd](x0, x1) = [0 0 0]x0 + [0 0 0]x1
                             [0 0 0]     [0 0 0]  ,
         
               [1]
         [0] = [1]
               [0],
         
                   [1]
         [false] = [0]
                   [0],
         
                     [1 0 0]  
         [not](x0) = [0 0 0]x0
                     [0 0 0]  ,
         
                  [1]
         [true] = [0]
                  [0]
        orientation:
                          [1 0 1]    [2]    [1 0 1]    [1]                         
         evenodd(x,0()) = [0 0 0]x + [0] >= [0 0 0]x + [0] = not(evenodd(x,s(0())))
                          [0 0 0]    [0]    [0 0 0]    [0]                         
         
                        [1]    [1]         
         not(false()) = [0] >= [0] = true()
                        [0]    [0]         
         
                       [1]    [1]          
         not(true()) = [0] >= [0] = false()
                       [0]    [0]          
         
                               [2]    [1]          
         evenodd(0(),s(0())) = [0] >= [0] = false()
                               [0]    [0]          
         
                                [1 0 1]    [2]    [1 0 1]    [2]                 
         evenodd(s(x),s(0())) = [0 0 0]x + [0] >= [0 0 0]x + [0] = evenodd(x,0())
                                [0 0 0]    [0]    [0 0 0]    [0]                 
        problem:
         strict:
          
         weak:
          evenodd(x,0()) -> not(evenodd(x,s(0())))
          not(false()) -> true()
          not(true()) -> false()
          evenodd(0(),s(0())) -> false()
          evenodd(s(x),s(0())) -> evenodd(x,0())
        Qed