MAYBE
Time: 0.009348
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:
  DP:
   {         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)}
  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}
  EDG:
   {(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) -> 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) -> check# x)
    (if#(even(), x, y, z, u) -> half# z, half# s s x -> half# x)
    (if#(even(), x, y, z, u) -> half# s z, half# s s x -> half# x)
    (half# s s x -> half# x, half# s s x -> half# x)
    (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))
    (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) -> 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) -> half# s z)
    (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# x)
    (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#(odd(), x, y, z, u) -> timesIter#(p x, y, u))
    (if#(even(), x, y, z, u) -> half# x, half# s s x -> half# x)
    (timesIter#(x, y, z) -> plus#(z, y), plus#(s x, y) -> plus#(x, y))
    (if#(even(), x, y, z, u) -> timesIter#(half x, y, half z), timesIter#(x, y, z) -> check# x)
    (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) -> if#(check x, x, y, z, plus(z, y)))
    (plus#(s x, y) -> plus#(x, y), plus#(s x, y) -> plus#(x, y))
    (timesIter#(x, y, z) -> check# x, check# s s s x -> check# s x)
    (check# s s s x -> check# s x, check# s s s x -> check# s x)
    (times#(x, y) -> timesIter#(x, y, 0()), timesIter#(x, y, z) -> check# x)
    (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) -> if#(check x, x, y, z, plus(z, y)))
    (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)))
    (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))}
   STATUS:
    arrows: 0.871111
    SCCS (4):
     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:
      {half# s s x -> half# x}
     Scc:
      {check# s s s x -> check# s x}
     Scc:
      {plus#(s x, y) -> plus#(x, y)}
     
     
     SCC (4):
      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}
      Open
     
     
     
     SCC (1):
      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}
      Open
     
     
     
     SCC (1):
      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}
      Open
     
     SCC (1):
      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}
      Open