YES
TRS:
 {not(false()) -> true(),
   not(true()) -> false(),
      odd(0()) -> false(),
     odd(s(x)) -> not(odd(x)),
     +(x, 0()) -> x,
    +(x, s(y)) -> s(+(x, y)),
    +(s(x), y) -> s(+(x, y))}
 RUF:
  Strict:
   {not(false()) -> true(),
     not(true()) -> false(),
       odd(s(x)) -> not(odd(x)),
      +(x, s(y)) -> s(+(x, y)),
      +(s(x), y) -> s(+(x, y))}
  Weak:
   {}
  DP:
   Strict:
    { odd#(s(x)) -> not#(odd(x)),
      odd#(s(x)) -> odd#(x),
     +#(x, s(y)) -> +#(x, y),
     +#(s(x), y) -> +#(x, y)}
   Weak:
   {not(false()) -> true(),
     not(true()) -> false(),
       odd(s(x)) -> not(odd(x)),
      +(x, s(y)) -> s(+(x, y)),
      +(s(x), y) -> s(+(x, y))}
   EDG:
    {(+#(s(x), 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))
     (+#(x, s(y)) -> +#(x, y), +#(s(x), y) -> +#(x, y))
     (odd#(s(x)) -> odd#(x), odd#(s(x)) -> not#(odd(x)))
     (odd#(s(x)) -> odd#(x), odd#(s(x)) -> odd#(x))}
    SCCS:
     Scc:
      {+#(x, s(y)) -> +#(x, y),
       +#(s(x), y) -> +#(x, y)}
     Scc:
      {odd#(s(x)) -> odd#(x)}
     SCC:
      Strict:
       {+#(x, s(y)) -> +#(x, y),
        +#(s(x), y) -> +#(x, y)}
      Weak:
      {not(false()) -> true(),
        not(true()) -> false(),
          odd(s(x)) -> not(odd(x)),
         +(x, s(y)) -> s(+(x, y)),
         +(s(x), y) -> s(+(x, y))}
      SPSC:
       Simple Projection:
        pi(+#) = 0
       Strict:
        {+#(x, s(y)) -> +#(x, y)}
       EDG:
        {(+#(x, s(y)) -> +#(x, y), +#(x, s(y)) -> +#(x, y))}
        SCCS:
         Scc:
          {+#(x, s(y)) -> +#(x, y)}
         SCC:
          Strict:
           {+#(x, s(y)) -> +#(x, y)}
          Weak:
          {not(false()) -> true(),
            not(true()) -> false(),
              odd(s(x)) -> not(odd(x)),
             +(x, s(y)) -> s(+(x, y)),
             +(s(x), y) -> s(+(x, y))}
          SPSC:
           Simple Projection:
            pi(+#) = 1
           Strict:
            {}
           Qed
     SCC:
      Strict:
       {odd#(s(x)) -> odd#(x)}
      Weak:
      {not(false()) -> true(),
        not(true()) -> false(),
          odd(s(x)) -> not(odd(x)),
         +(x, s(y)) -> s(+(x, y)),
         +(s(x), y) -> s(+(x, y))}
      SPSC:
       Simple Projection:
        pi(odd#) = 0
       Strict:
        {}
       Qed