MAYBE
TRS:
 {            check(0()) -> zero(),
           check(s(0())) -> odd(),
        check(s(s(0()))) -> even(),
       check(s(s(s(x)))) -> check(s(x)),
               half(0()) -> 0(),
            half(s(0())) -> 0(),
           half(s(s(x))) -> s(half(x)),
            plus(0(), y) -> y,
           plus(s(x), y) -> s(plus(x, y)),
      timesIter(x, y, z) -> if(check(x), x, y, z, plus(z, y)),
             times(x, y) -> timesIter(x, y, 0()),
  if(zero(), x, y, z, u) -> z,
   if(odd(), x, y, z, u) -> timesIter(p(x), y, u),
  if(even(), x, y, z, u) -> plus(timesIter(half(x), y, half(z)), timesIter(half(x), y, half(s(z)))),
                  p(0()) -> 0(),
                 p(s(x)) -> x}
 DP:
  Strict:
   {     check#(s(s(s(x)))) -> check#(s(x)),
             half#(s(s(x))) -> half#(x),
             plus#(s(x), y) -> plus#(x, y),
        timesIter#(x, y, z) -> check#(x),
        timesIter#(x, y, z) -> plus#(z, y),
        timesIter#(x, y, z) -> if#(check(x), x, y, z, plus(z, y)),
               times#(x, y) -> timesIter#(x, y, 0()),
     if#(odd(), x, y, z, u) -> timesIter#(p(x), y, u),
     if#(odd(), x, y, z, u) -> p#(x),
    if#(even(), x, y, z, u) -> half#(x),
    if#(even(), x, y, z, u) -> half#(z),
    if#(even(), x, y, z, u) -> half#(s(z)),
    if#(even(), x, y, z, u) -> plus#(timesIter(half(x), y, half(z)), timesIter(half(x), y, half(s(z)))),
    if#(even(), x, y, z, u) -> timesIter#(half(x), y, half(z)),
    if#(even(), x, y, z, u) -> timesIter#(half(x), y, half(s(z)))}
  Weak:
  {            check(0()) -> zero(),
            check(s(0())) -> odd(),
         check(s(s(0()))) -> even(),
        check(s(s(s(x)))) -> check(s(x)),
                half(0()) -> 0(),
             half(s(0())) -> 0(),
            half(s(s(x))) -> s(half(x)),
             plus(0(), y) -> y,
            plus(s(x), y) -> s(plus(x, y)),
       timesIter(x, y, z) -> if(check(x), x, y, z, plus(z, y)),
              times(x, y) -> timesIter(x, y, 0()),
   if(zero(), x, y, z, u) -> z,
    if(odd(), x, y, z, u) -> timesIter(p(x), y, u),
   if(even(), x, y, z, u) -> plus(timesIter(half(x), y, half(z)), timesIter(half(x), y, half(s(z)))),
                   p(0()) -> 0(),
                  p(s(x)) -> x}
  EDG:
   {(if#(even(), x, y, z, u) -> half#(z), half#(s(s(x))) -> half#(x))
    (half#(s(s(x))) -> half#(x), half#(s(s(x))) -> half#(x))
    (times#(x, y) -> timesIter#(x, y, 0()), timesIter#(x, y, z) -> if#(check(x), x, y, z, plus(z, y)))
    (times#(x, y) -> timesIter#(x, y, 0()), timesIter#(x, y, z) -> plus#(z, y))
    (times#(x, y) -> timesIter#(x, y, 0()), timesIter#(x, y, z) -> check#(x))
    (check#(s(s(s(x)))) -> check#(s(x)), check#(s(s(s(x)))) -> check#(s(x)))
    (plus#(s(x), y) -> plus#(x, y), plus#(s(x), y) -> plus#(x, y))
    (if#(even(), x, y, z, u) -> timesIter#(half(x), y, half(z)), timesIter#(x, y, z) -> if#(check(x), x, y, z, plus(z, y)))
    (if#(even(), x, y, z, u) -> timesIter#(half(x), y, half(z)), timesIter#(x, y, z) -> plus#(z, y))
    (if#(even(), x, y, z, u) -> timesIter#(half(x), y, half(z)), timesIter#(x, y, z) -> check#(x))
    (if#(odd(), x, y, z, u) -> timesIter#(p(x), y, u), timesIter#(x, y, z) -> check#(x))
    (if#(odd(), x, y, z, u) -> timesIter#(p(x), y, u), timesIter#(x, y, z) -> plus#(z, y))
    (if#(odd(), x, y, z, u) -> timesIter#(p(x), y, u), timesIter#(x, y, z) -> if#(check(x), x, y, z, plus(z, y)))
    (timesIter#(x, y, z) -> plus#(z, y), plus#(s(x), y) -> plus#(x, y))
    (timesIter#(x, y, z) -> if#(check(x), x, y, z, plus(z, y)), if#(odd(), x, y, z, u) -> timesIter#(p(x), y, u))
    (timesIter#(x, y, z) -> if#(check(x), x, y, z, plus(z, y)), if#(odd(), x, y, z, u) -> p#(x))
    (timesIter#(x, y, z) -> if#(check(x), x, y, z, plus(z, y)), if#(even(), x, y, z, u) -> half#(x))
    (timesIter#(x, y, z) -> if#(check(x), x, y, z, plus(z, y)), if#(even(), x, y, z, u) -> half#(z))
    (timesIter#(x, y, z) -> if#(check(x), x, y, z, plus(z, y)), if#(even(), x, y, z, u) -> half#(s(z)))
    (timesIter#(x, y, z) -> if#(check(x), x, y, z, plus(z, y)), if#(even(), x, y, z, u) -> plus#(timesIter(half(x), y, half(z)), timesIter(half(x), y, half(s(z)))))
    (timesIter#(x, y, z) -> if#(check(x), x, y, z, plus(z, y)), if#(even(), x, y, z, u) -> timesIter#(half(x), y, half(z)))
    (timesIter#(x, y, z) -> if#(check(x), x, y, z, plus(z, y)), if#(even(), x, y, z, u) -> timesIter#(half(x), y, half(s(z))))
    (if#(even(), x, y, z, u) -> half#(s(z)), half#(s(s(x))) -> half#(x))
    (if#(even(), x, y, z, u) -> half#(x), half#(s(s(x))) -> half#(x))
    (timesIter#(x, y, z) -> check#(x), check#(s(s(s(x)))) -> check#(s(x)))
    (if#(even(), x, y, z, u) -> timesIter#(half(x), y, half(s(z))), timesIter#(x, y, z) -> check#(x))
    (if#(even(), x, y, z, u) -> timesIter#(half(x), y, half(s(z))), timesIter#(x, y, z) -> plus#(z, y))
    (if#(even(), x, y, z, u) -> timesIter#(half(x), y, half(s(z))), timesIter#(x, y, z) -> if#(check(x), x, y, z, plus(z, y)))
    (if#(even(), x, y, z, u) -> plus#(timesIter(half(x), y, half(z)), timesIter(half(x), y, half(s(z)))), plus#(s(x), y) -> plus#(x, y))}
   SCCS:
    Scc:
     {    timesIter#(x, y, z) -> if#(check(x), x, y, z, plus(z, y)),
       if#(odd(), x, y, z, u) -> timesIter#(p(x), y, u),
      if#(even(), x, y, z, u) -> timesIter#(half(x), y, half(z)),
      if#(even(), x, y, z, u) -> timesIter#(half(x), y, half(s(z)))}
    Scc:
     {plus#(s(x), y) -> plus#(x, y)}
    Scc:
     {half#(s(s(x))) -> half#(x)}
    Scc:
     {check#(s(s(s(x)))) -> check#(s(x))}
    SCC:
     Strict:
      {    timesIter#(x, y, z) -> if#(check(x), x, y, z, plus(z, y)),
        if#(odd(), x, y, z, u) -> timesIter#(p(x), y, u),
       if#(even(), x, y, z, u) -> timesIter#(half(x), y, half(z)),
       if#(even(), x, y, z, u) -> timesIter#(half(x), y, half(s(z)))}
     Weak:
     {            check(0()) -> zero(),
               check(s(0())) -> odd(),
            check(s(s(0()))) -> even(),
           check(s(s(s(x)))) -> check(s(x)),
                   half(0()) -> 0(),
                half(s(0())) -> 0(),
               half(s(s(x))) -> s(half(x)),
                plus(0(), y) -> y,
               plus(s(x), y) -> s(plus(x, y)),
          timesIter(x, y, z) -> if(check(x), x, y, z, plus(z, y)),
                 times(x, y) -> timesIter(x, y, 0()),
      if(zero(), x, y, z, u) -> z,
       if(odd(), x, y, z, u) -> timesIter(p(x), y, u),
      if(even(), x, y, z, u) -> plus(timesIter(half(x), y, half(z)), timesIter(half(x), y, half(s(z)))),
                      p(0()) -> 0(),
                     p(s(x)) -> x}
     Fail
    SCC:
     Strict:
      {plus#(s(x), y) -> plus#(x, y)}
     Weak:
     {            check(0()) -> zero(),
               check(s(0())) -> odd(),
            check(s(s(0()))) -> even(),
           check(s(s(s(x)))) -> check(s(x)),
                   half(0()) -> 0(),
                half(s(0())) -> 0(),
               half(s(s(x))) -> s(half(x)),
                plus(0(), y) -> y,
               plus(s(x), y) -> s(plus(x, y)),
          timesIter(x, y, z) -> if(check(x), x, y, z, plus(z, y)),
                 times(x, y) -> timesIter(x, y, 0()),
      if(zero(), x, y, z, u) -> z,
       if(odd(), x, y, z, u) -> timesIter(p(x), y, u),
      if(even(), x, y, z, u) -> plus(timesIter(half(x), y, half(z)), timesIter(half(x), y, half(s(z)))),
                      p(0()) -> 0(),
                     p(s(x)) -> x}
     SPSC:
      Simple Projection:
       pi(plus#) = 0
      Strict:
       {}
      Qed
    SCC:
     Strict:
      {half#(s(s(x))) -> half#(x)}
     Weak:
     {            check(0()) -> zero(),
               check(s(0())) -> odd(),
            check(s(s(0()))) -> even(),
           check(s(s(s(x)))) -> check(s(x)),
                   half(0()) -> 0(),
                half(s(0())) -> 0(),
               half(s(s(x))) -> s(half(x)),
                plus(0(), y) -> y,
               plus(s(x), y) -> s(plus(x, y)),
          timesIter(x, y, z) -> if(check(x), x, y, z, plus(z, y)),
                 times(x, y) -> timesIter(x, y, 0()),
      if(zero(), x, y, z, u) -> z,
       if(odd(), x, y, z, u) -> timesIter(p(x), y, u),
      if(even(), x, y, z, u) -> plus(timesIter(half(x), y, half(z)), timesIter(half(x), y, half(s(z)))),
                      p(0()) -> 0(),
                     p(s(x)) -> x}
     SPSC:
      Simple Projection:
       pi(half#) = 0
      Strict:
       {}
      Qed
    SCC:
     Strict:
      {check#(s(s(s(x)))) -> check#(s(x))}
     Weak:
     {            check(0()) -> zero(),
               check(s(0())) -> odd(),
            check(s(s(0()))) -> even(),
           check(s(s(s(x)))) -> check(s(x)),
                   half(0()) -> 0(),
                half(s(0())) -> 0(),
               half(s(s(x))) -> s(half(x)),
                plus(0(), y) -> y,
               plus(s(x), y) -> s(plus(x, y)),
          timesIter(x, y, z) -> if(check(x), x, y, z, plus(z, y)),
                 times(x, y) -> timesIter(x, y, 0()),
      if(zero(), x, y, z, u) -> z,
       if(odd(), x, y, z, u) -> timesIter(p(x), y, u),
      if(even(), x, y, z, u) -> plus(timesIter(half(x), y, half(z)), timesIter(half(x), y, half(s(z)))),
                      p(0()) -> 0(),
                     p(s(x)) -> x}
     SPSC:
      Simple Projection:
       pi(check#) = 0
      Strict:
       {}
      Qed