MAYBE
TRS:
 {                 even(0()) -> true(),
                even(s(0())) -> false(),
               even(s(s(x))) -> even(x),
                   half(0()) -> 0(),
               half(s(s(x))) -> s(half(x)),
                plus(0(), y) -> y,
               plus(s(x), y) -> s(plus(x, y)),
               times(0(), y) -> 0(),
              times(s(x), y) -> if_times(even(s(x)), s(x), y),
   if_times(true(), s(x), y) -> plus(times(half(s(x)), y), times(half(s(x)), y)),
  if_times(false(), s(x), y) -> plus(y, times(x, y))}
 DP:
  Strict:
   {             even#(s(s(x))) -> even#(x),
                 half#(s(s(x))) -> half#(x),
                 plus#(s(x), y) -> plus#(x, y),
                times#(s(x), y) -> even#(s(x)),
                times#(s(x), y) -> if_times#(even(s(x)), s(x), y),
     if_times#(true(), s(x), y) -> half#(s(x)),
     if_times#(true(), s(x), y) -> plus#(times(half(s(x)), y), times(half(s(x)), y)),
     if_times#(true(), s(x), y) -> times#(half(s(x)), y),
    if_times#(false(), s(x), y) -> plus#(y, times(x, y)),
    if_times#(false(), s(x), y) -> times#(x, y)}
  Weak:
  {                 even(0()) -> true(),
                 even(s(0())) -> false(),
                even(s(s(x))) -> even(x),
                    half(0()) -> 0(),
                half(s(s(x))) -> s(half(x)),
                 plus(0(), y) -> y,
                plus(s(x), y) -> s(plus(x, y)),
                times(0(), y) -> 0(),
               times(s(x), y) -> if_times(even(s(x)), s(x), y),
    if_times(true(), s(x), y) -> plus(times(half(s(x)), y), times(half(s(x)), y)),
   if_times(false(), s(x), y) -> plus(y, times(x, y))}
  EDG:
   {(half#(s(s(x))) -> half#(x), half#(s(s(x))) -> half#(x))
    (if_times#(false(), s(x), y) -> plus#(y, times(x, y)), plus#(s(x), y) -> plus#(x, y))
    (if_times#(true(), s(x), y) -> half#(s(x)), half#(s(s(x))) -> half#(x))
    (if_times#(false(), s(x), y) -> times#(x, y), times#(s(x), y) -> if_times#(even(s(x)), s(x), y))
    (if_times#(false(), s(x), y) -> times#(x, y), times#(s(x), y) -> even#(s(x)))
    (if_times#(true(), s(x), y) -> times#(half(s(x)), y), times#(s(x), y) -> if_times#(even(s(x)), s(x), y))
    (if_times#(true(), s(x), y) -> times#(half(s(x)), y), times#(s(x), y) -> even#(s(x)))
    (times#(s(x), y) -> if_times#(even(s(x)), s(x), y), if_times#(true(), s(x), y) -> half#(s(x)))
    (times#(s(x), y) -> if_times#(even(s(x)), s(x), y), if_times#(true(), s(x), y) -> plus#(times(half(s(x)), y), times(half(s(x)), y)))
    (times#(s(x), y) -> if_times#(even(s(x)), s(x), y), if_times#(true(), s(x), y) -> times#(half(s(x)), y))
    (times#(s(x), y) -> if_times#(even(s(x)), s(x), y), if_times#(false(), s(x), y) -> plus#(y, times(x, y)))
    (times#(s(x), y) -> if_times#(even(s(x)), s(x), y), if_times#(false(), s(x), y) -> times#(x, y))
    (plus#(s(x), y) -> plus#(x, y), plus#(s(x), y) -> plus#(x, y))
    (times#(s(x), y) -> even#(s(x)), even#(s(s(x))) -> even#(x))
    (if_times#(true(), s(x), y) -> plus#(times(half(s(x)), y), times(half(s(x)), y)), plus#(s(x), y) -> plus#(x, y))
    (even#(s(s(x))) -> even#(x), even#(s(s(x))) -> even#(x))}
   SCCS:
    Scc:
     {            times#(s(x), y) -> if_times#(even(s(x)), s(x), y),
       if_times#(true(), s(x), y) -> times#(half(s(x)), y),
      if_times#(false(), s(x), y) -> times#(x, y)}
    Scc:
     {plus#(s(x), y) -> plus#(x, y)}
    Scc:
     {half#(s(s(x))) -> half#(x)}
    Scc:
     {even#(s(s(x))) -> even#(x)}
    SCC:
     Strict:
      {            times#(s(x), y) -> if_times#(even(s(x)), s(x), y),
        if_times#(true(), s(x), y) -> times#(half(s(x)), y),
       if_times#(false(), s(x), y) -> times#(x, y)}
     Weak:
     {                 even(0()) -> true(),
                    even(s(0())) -> false(),
                   even(s(s(x))) -> even(x),
                       half(0()) -> 0(),
                   half(s(s(x))) -> s(half(x)),
                    plus(0(), y) -> y,
                   plus(s(x), y) -> s(plus(x, y)),
                   times(0(), y) -> 0(),
                  times(s(x), y) -> if_times(even(s(x)), s(x), y),
       if_times(true(), s(x), y) -> plus(times(half(s(x)), y), times(half(s(x)), y)),
      if_times(false(), s(x), y) -> plus(y, times(x, y))}
     POLY:
      Argument Filtering:
       pi(if_times#) = 1, pi(if_times) = [], pi(times#) = 0, pi(times) = [], pi(plus) = [], pi(half) = 0, pi(s) = [0], pi(false) = [], pi(0) = [], pi(even) = [], pi(true) = []
      Usable Rules:
       {}
      Interpretation:
       [s](x0) = x0 + 1
      Strict:
       {           times#(s(x), y) -> if_times#(even(s(x)), s(x), y),
        if_times#(true(), s(x), y) -> times#(half(s(x)), y)}
      Weak:
       {                 even(0()) -> true(),
                      even(s(0())) -> false(),
                     even(s(s(x))) -> even(x),
                         half(0()) -> 0(),
                     half(s(s(x))) -> s(half(x)),
                      plus(0(), y) -> y,
                     plus(s(x), y) -> s(plus(x, y)),
                     times(0(), y) -> 0(),
                    times(s(x), y) -> if_times(even(s(x)), s(x), y),
         if_times(true(), s(x), y) -> plus(times(half(s(x)), y), times(half(s(x)), y)),
        if_times(false(), s(x), y) -> plus(y, times(x, y))}
      EDG:
       {(if_times#(true(), s(x), y) -> times#(half(s(x)), y), times#(s(x), y) -> if_times#(even(s(x)), s(x), y))
        (times#(s(x), y) -> if_times#(even(s(x)), s(x), y), if_times#(true(), s(x), y) -> times#(half(s(x)), y))}
       SCCS:
        Scc:
         {           times#(s(x), y) -> if_times#(even(s(x)), s(x), y),
          if_times#(true(), s(x), y) -> times#(half(s(x)), y)}
        SCC:
         Strict:
          {           times#(s(x), y) -> if_times#(even(s(x)), s(x), y),
           if_times#(true(), s(x), y) -> times#(half(s(x)), y)}
         Weak:
         {                 even(0()) -> true(),
                        even(s(0())) -> false(),
                       even(s(s(x))) -> even(x),
                           half(0()) -> 0(),
                       half(s(s(x))) -> s(half(x)),
                        plus(0(), y) -> y,
                       plus(s(x), y) -> s(plus(x, y)),
                       times(0(), y) -> 0(),
                      times(s(x), y) -> if_times(even(s(x)), s(x), y),
           if_times(true(), s(x), y) -> plus(times(half(s(x)), y), times(half(s(x)), y)),
          if_times(false(), s(x), y) -> plus(y, times(x, y))}
         Fail
    SCC:
     Strict:
      {plus#(s(x), y) -> plus#(x, y)}
     Weak:
     {                 even(0()) -> true(),
                    even(s(0())) -> false(),
                   even(s(s(x))) -> even(x),
                       half(0()) -> 0(),
                   half(s(s(x))) -> s(half(x)),
                    plus(0(), y) -> y,
                   plus(s(x), y) -> s(plus(x, y)),
                   times(0(), y) -> 0(),
                  times(s(x), y) -> if_times(even(s(x)), s(x), y),
       if_times(true(), s(x), y) -> plus(times(half(s(x)), y), times(half(s(x)), y)),
      if_times(false(), s(x), y) -> plus(y, times(x, y))}
     SPSC:
      Simple Projection:
       pi(plus#) = 0
      Strict:
       {}
      Qed
    SCC:
     Strict:
      {half#(s(s(x))) -> half#(x)}
     Weak:
     {                 even(0()) -> true(),
                    even(s(0())) -> false(),
                   even(s(s(x))) -> even(x),
                       half(0()) -> 0(),
                   half(s(s(x))) -> s(half(x)),
                    plus(0(), y) -> y,
                   plus(s(x), y) -> s(plus(x, y)),
                   times(0(), y) -> 0(),
                  times(s(x), y) -> if_times(even(s(x)), s(x), y),
       if_times(true(), s(x), y) -> plus(times(half(s(x)), y), times(half(s(x)), y)),
      if_times(false(), s(x), y) -> plus(y, times(x, y))}
     SPSC:
      Simple Projection:
       pi(half#) = 0
      Strict:
       {}
      Qed
    SCC:
     Strict:
      {even#(s(s(x))) -> even#(x)}
     Weak:
     {                 even(0()) -> true(),
                    even(s(0())) -> false(),
                   even(s(s(x))) -> even(x),
                       half(0()) -> 0(),
                   half(s(s(x))) -> s(half(x)),
                    plus(0(), y) -> y,
                   plus(s(x), y) -> s(plus(x, y)),
                   times(0(), y) -> 0(),
                  times(s(x), y) -> if_times(even(s(x)), s(x), y),
       if_times(true(), s(x), y) -> plus(times(half(s(x)), y), times(half(s(x)), y)),
      if_times(false(), s(x), y) -> plus(y, times(x, y))}
     SPSC:
      Simple Projection:
       pi(even#) = 0
      Strict:
       {}
      Qed