YES(?,O(n^1))

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:
 RT 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
   interpretation:
    [s](x0) = x0 + 12,
    
    [evenodd](x0, x1) = x0 + x1 + 8,
    
    [0] = 20,
    
    [false] = 28,
    
    [not](x0) = x0 + 20,
    
    [true] = 8
   orientation:
    not(true()) = 28 >= 28 = false()
    
    not(false()) = 48 >= 8 = true()
    
    evenodd(x,0()) = x + 28 >= x + 60 = not(evenodd(x,s(0())))
    
    evenodd(0(),s(0())) = 60 >= 28 = false()
    
    evenodd(s(x),s(0())) = x + 52 >= x + 28 = evenodd(x,0())
   problem:
    strict:
     not(true()) -> false()
     evenodd(x,0()) -> not(evenodd(x,s(0())))
    weak:
     not(false()) -> true()
     evenodd(0(),s(0())) -> false()
     evenodd(s(x),s(0())) -> evenodd(x,0())
   Matrix Interpretation Processor:
    dimension: 1
    interpretation:
     [s](x0) = x0 + 4,
     
     [evenodd](x0, x1) = x0 + x1 + 4,
     
     [0] = 5,
     
     [false] = 18,
     
     [not](x0) = x0 + 10,
     
     [true] = 28
    orientation:
     not(true()) = 38 >= 18 = false()
     
     evenodd(x,0()) = x + 9 >= x + 23 = not(evenodd(x,s(0())))
     
     not(false()) = 28 >= 28 = true()
     
     evenodd(0(),s(0())) = 18 >= 18 = false()
     
     evenodd(s(x),s(0())) = x + 17 >= x + 9 = evenodd(x,0())
    problem:
     strict:
      evenodd(x,0()) -> not(evenodd(x,s(0())))
     weak:
      not(true()) -> false()
      not(false()) -> true()
      evenodd(0(),s(0())) -> false()
      evenodd(s(x),s(0())) -> evenodd(x,0())
    Bounds Processor:
     bound: 2
     enrichment: match-rt
     automaton:
      final states: {7}
      transitions:
       not1(13) -> 7*
       evenodd1(7,12) -> 13*
       evenodd1(7,11) -> 16,13
       s1(11) -> 12*
       01() -> 11*
       false1() -> 7,16,13
       not2(16) -> 16,13
       evenodd2(7,15) -> 16*
       evenodd0(7,7) -> 7*
       s2(14) -> 15*
       00() -> 7*
       02() -> 14*
       not0(7) -> 7*
       true1() -> 7*
       s0(7) -> 7*
       true2() -> 7,13,16
       true0() -> 7*
       false2() -> 13,7,16
       false0() -> 7*
     problem:
      strict:
       
      weak:
       evenodd(x,0()) -> not(evenodd(x,s(0())))
       not(true()) -> false()
       not(false()) -> true()
       evenodd(0(),s(0())) -> false()
       evenodd(s(x),s(0())) -> evenodd(x,0())
     Qed