YES
Time: 0.001419
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:
   DP:
    {  odd# s x -> not# odd x,
       odd# s x -> odd# x,
     +#(x, s y) -> +#(x, y),
     +#(s x, y) -> +#(x, y)}
   TRS:
   {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 (2):
     Scc:
      {+#(x, s y) -> +#(x, y),
       +#(s x, y) -> +#(x, y)}
     Scc:
      {odd# s x -> odd# x}
     SCC (2):
      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(+#) = 1
       Strict:
        {+#(s x, y) -> +#(x, y)}
       EDG:
        {(+#(s x, y) -> +#(x, y), +#(s x, y) -> +#(x, y))}
        SCCS (1):
         Scc:
          {+#(s x, y) -> +#(x, y)}
         SCC (1):
          Strict:
           {+#(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:
            {}
           Qed
     SCC (1):
      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