YES

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:
 DP Processor:
  DPs:
   odd#(s(x)) -> odd#(x)
   odd#(s(x)) -> not#(odd(x))
   +#(x,s(y)) -> +#(x,y)
   +#(s(x),y) -> +#(x,y)
  TRS:
   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))
  Usable Rule Processor:
   DPs:
    odd#(s(x)) -> odd#(x)
    odd#(s(x)) -> not#(odd(x))
    +#(x,s(y)) -> +#(x,y)
    +#(s(x),y) -> +#(x,y)
   TRS:
    odd(0()) -> false()
    odd(s(x)) -> not(odd(x))
    not(true()) -> false()
    not(false()) -> true()
   EDG Processor:
    DPs:
     odd#(s(x)) -> odd#(x)
     odd#(s(x)) -> not#(odd(x))
     +#(x,s(y)) -> +#(x,y)
     +#(s(x),y) -> +#(x,y)
    TRS:
     odd(0()) -> false()
     odd(s(x)) -> not(odd(x))
     not(true()) -> false()
     not(false()) -> true()
    graph:
     +#(s(x),y) -> +#(x,y) -> +#(x,s(y)) -> +#(x,y)
     +#(s(x),y) -> +#(x,y) -> +#(s(x),y) -> +#(x,y)
     +#(x,s(y)) -> +#(x,y) -> +#(x,s(y)) -> +#(x,y)
     +#(x,s(y)) -> +#(x,y) -> +#(s(x),y) -> +#(x,y)
     odd#(s(x)) -> odd#(x) -> odd#(s(x)) -> odd#(x)
     odd#(s(x)) -> odd#(x) -> odd#(s(x)) -> not#(odd(x))
    Restore Modifier:
     DPs:
      odd#(s(x)) -> odd#(x)
      odd#(s(x)) -> not#(odd(x))
      +#(x,s(y)) -> +#(x,y)
      +#(s(x),y) -> +#(x,y)
     TRS:
      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))
     SCC Processor:
      #sccs: 2
      #rules: 3
      #arcs: 6/16
      DPs:
       odd#(s(x)) -> odd#(x)
      TRS:
       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))
      Matrix Interpretation Processor:
       dimension: 1
       interpretation:
        [odd#](x0) = x0 + 1,
        
        [+](x0, x1) = x0 + x1,
        
        [s](x0) = x0 + 1,
        
        [odd](x0) = x0,
        
        [0] = 0,
        
        [false] = 0,
        
        [not](x0) = 1,
        
        [true] = 1
       orientation:
        odd#(s(x)) = x + 2 >= x + 1 = odd#(x)
        
        not(true()) = 1 >= 0 = false()
        
        not(false()) = 1 >= 1 = true()
        
        odd(0()) = 0 >= 0 = false()
        
        odd(s(x)) = x + 1 >= 1 = not(odd(x))
        
        +(x,0()) = x >= x = 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))
       problem:
        DPs:
         
        TRS:
         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))
       Qed
      
      DPs:
       +#(s(x),y) -> +#(x,y)
       +#(x,s(y)) -> +#(x,y)
      TRS:
       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))
      Matrix Interpretation Processor:
       dimension: 1
       interpretation:
        [+#](x0, x1) = x1,
        
        [+](x0, x1) = x0 + x1 + 1,
        
        [s](x0) = x0 + 1,
        
        [odd](x0) = 0,
        
        [0] = 0,
        
        [false] = 0,
        
        [not](x0) = 0,
        
        [true] = 0
       orientation:
        +#(s(x),y) = y >= y = +#(x,y)
        
        +#(x,s(y)) = y + 1 >= y = +#(x,y)
        
        not(true()) = 0 >= 0 = false()
        
        not(false()) = 0 >= 0 = true()
        
        odd(0()) = 0 >= 0 = false()
        
        odd(s(x)) = 0 >= 0 = not(odd(x))
        
        +(x,0()) = x + 1 >= x = x
        
        +(x,s(y)) = x + y + 2 >= x + y + 2 = s(+(x,y))
        
        +(s(x),y) = x + y + 2 >= x + y + 2 = s(+(x,y))
       problem:
        DPs:
         +#(s(x),y) -> +#(x,y)
        TRS:
         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))
       Matrix Interpretation Processor:
        dimension: 1
        interpretation:
         [+#](x0, x1) = x0,
         
         [+](x0, x1) = x0 + x1 + 1,
         
         [s](x0) = x0 + 1,
         
         [odd](x0) = 0,
         
         [0] = 0,
         
         [false] = 0,
         
         [not](x0) = 0,
         
         [true] = 0
        orientation:
         +#(s(x),y) = x + 1 >= x = +#(x,y)
         
         not(true()) = 0 >= 0 = false()
         
         not(false()) = 0 >= 0 = true()
         
         odd(0()) = 0 >= 0 = false()
         
         odd(s(x)) = 0 >= 0 = not(odd(x))
         
         +(x,0()) = x + 1 >= x = x
         
         +(x,s(y)) = x + y + 2 >= x + y + 2 = s(+(x,y))
         
         +(s(x),y) = x + y + 2 >= x + y + 2 = s(+(x,y))
        problem:
         DPs:
          
         TRS:
          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))
        Qed