YES
Time: 0.043802
TRS:
 {        not false() -> true(),
           not true() -> false(),
      evenodd(x, 0()) -> not evenodd(x, s 0()),
  evenodd(s x, s 0()) -> evenodd(x, 0()),
  evenodd(0(), s 0()) -> false()}
 DP:
  DP:
   {    evenodd#(x, 0()) -> not# evenodd(x, s 0()),
        evenodd#(x, 0()) -> evenodd#(x, s 0()),
    evenodd#(s x, s 0()) -> evenodd#(x, 0())}
  TRS:
  {        not false() -> true(),
            not true() -> false(),
       evenodd(x, 0()) -> not evenodd(x, s 0()),
   evenodd(s x, s 0()) -> evenodd(x, 0()),
   evenodd(0(), s 0()) -> false()}
  UR:
   {        not false() -> true(),
             not true() -> false(),
        evenodd(x, 0()) -> not evenodd(x, s 0()),
    evenodd(s x, s 0()) -> evenodd(x, 0()),
    evenodd(0(), s 0()) -> false()}
   EDG:
    {(evenodd#(s x, s 0()) -> evenodd#(x, 0()), evenodd#(x, 0()) -> evenodd#(x, s 0()))
     (evenodd#(s x, s 0()) -> evenodd#(x, 0()), evenodd#(x, 0()) -> not# evenodd(x, s 0()))
     (evenodd#(x, 0()) -> evenodd#(x, s 0()), evenodd#(s x, s 0()) -> evenodd#(x, 0()))}
    STATUS:
     arrows: 0.666667
     SCCS (1):
      Scc:
       {    evenodd#(x, 0()) -> evenodd#(x, s 0()),
        evenodd#(s x, s 0()) -> evenodd#(x, 0())}
      
      SCC (2):
       Strict:
        {    evenodd#(x, 0()) -> evenodd#(x, s 0()),
         evenodd#(s x, s 0()) -> evenodd#(x, 0())}
       Weak:
       {        not false() -> true(),
                 not true() -> false(),
            evenodd(x, 0()) -> not evenodd(x, s 0()),
        evenodd(s x, s 0()) -> evenodd(x, 0()),
        evenodd(0(), s 0()) -> false()}
       POLY:
        Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
        Interpretation:
         [evenodd](x0, x1) = x0 + 1,
         
         [not](x0) = x0,
         
         [s](x0) = x0 + 1,
         
         [false] = 0,
         
         [true] = 0,
         
         [0] = 0,
         
         [evenodd#](x0, x1) = x0 + 1
        Strict:
         evenodd#(s x, s 0()) -> evenodd#(x, 0())
         2 + 1x >= 1 + 1x
         evenodd#(x, 0()) -> evenodd#(x, s 0())
         1 + 1x >= 1 + 1x
        Weak:
         evenodd(0(), s 0()) -> false()
         2 >= 0
         evenodd(s x, s 0()) -> evenodd(x, 0())
         2 + 0x >= 1 + 0x
         evenodd(x, 0()) -> not evenodd(x, s 0())
         1 + 0x >= 2 + 0x
         not true() -> false()
         0 >= 0
         not false() -> true()
         0 >= 0
       SCCS (0):