MAYBE
Time: 1.457022
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:
  DP:
   {               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)}
  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))}
  EDG:
   {(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)
    (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) -> 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#(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) -> 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) -> half# s x)
    (half# s s x -> half# x, half# s s x -> half# x)
    (even# s s x -> even# x, even# s s x -> even# x)
    (if_times#(true(), s x, y) -> times#(half s 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))
    (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))}
   STATUS:
    arrows: 0.840000
    SCCS (4):
     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:
      {half# s s x -> half# x}
     Scc:
      {even# s s x -> even# x}
     Scc:
      {plus#(s x, y) -> plus#(x, y)}
     
     SCC (3):
      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))}
      Open
     
     SCC (1):
      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))}
      Open
     
     SCC (1):
      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))}
      Open
     
     
     SCC (1):
      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))}
      Open