MAYBE
Time: 1.542069
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))}
      POLY:
       Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
       Interpretation:
        [if_times](x0, x1, x2) = x0 + 1,
        
        [plus](x0, x1) = 0,
        
        [times](x0, x1) = 0,
        
        [even](x0) = 1,
        
        [s](x0) = x0 + 1,
        
        [half](x0) = x0,
        
        [true] = 1,
        
        [0] = 0,
        
        [false] = 1,
        
        [if_times#](x0, x1, x2) = x0 + x1,
        
        [times#](x0, x1) = x0 + 1
       Strict:
        if_times#(false(), s x, y) -> times#(x, y)
        2 + 1x + 0y >= 1 + 1x + 0y
        if_times#(true(), s x, y) -> times#(half s x, y)
        2 + 1x + 0y >= 2 + 1x + 0y
        times#(s x, y) -> if_times#(even s x, s x, y)
        2 + 1x + 0y >= 2 + 1x + 0y
       Weak:
        if_times(false(), s x, y) -> plus(y, times(x, y))
        2 + 0x + 0y >= 0 + 0x + 0y
        if_times(true(), s x, y) -> plus(times(half s x, y), times(half s x, y))
        2 + 0x + 0y >= 0 + 0x + 0y
        times(s x, y) -> if_times(even s x, s x, y)
        0 + 0x + 0y >= 2 + 0x + 0y
        times(0(), y) -> 0()
        0 + 0y >= 0
        plus(s x, y) -> s plus(x, y)
        0 + 0x + 0y >= 1 + 0x + 0y
        plus(0(), y) -> y
        0 + 0y >= 1y
        half s s x -> s half x
        2 + 1x >= 1 + 1x
        half 0() -> 0()
        0 >= 0
        even s s x -> even x
        1 + 0x >= 1 + 0x
        even s 0() -> false()
        1 >= 1
        even 0() -> true()
        1 >= 1
      SCCS (1):
       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 (2):
        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 (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))}
     POLY:
      Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
      Interpretation:
       [if_times](x0, x1, x2) = x0,
       
       [plus](x0, x1) = x0 + x1 + 1,
       
       [times](x0, x1) = x0 + 1,
       
       [even](x0) = x0 + 1,
       
       [s](x0) = x0 + 1,
       
       [half](x0) = x0 + 1,
       
       [true] = 0,
       
       [0] = 1,
       
       [false] = 0,
       
       [half#](x0) = x0
      Strict:
       half# s s x -> half# x
       2 + 1x >= 0 + 1x
      Weak:
       if_times(false(), s x, y) -> plus(y, times(x, y))
       0 + 0x + 0y >= 2 + 1x + 1y
       if_times(true(), s x, y) -> plus(times(half s x, y), times(half s x, y))
       0 + 0x + 0y >= 7 + 2x + 0y
       times(s x, y) -> if_times(even s x, s x, y)
       2 + 1x + 0y >= 2 + 1x + 0y
       times(0(), y) -> 0()
       2 + 0y >= 1
       plus(s x, y) -> s plus(x, y)
       2 + 1x + 1y >= 2 + 1x + 1y
       plus(0(), y) -> y
       2 + 1y >= 1y
       half s s x -> s half x
       3 + 1x >= 2 + 1x
       half 0() -> 0()
       2 >= 1
       even s s x -> even x
       3 + 1x >= 1 + 1x
       even s 0() -> false()
       3 >= 0
       even 0() -> true()
       2 >= 0
     Qed
    
    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))}
     POLY:
      Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
      Interpretation:
       [if_times](x0, x1, x2) = x0,
       
       [plus](x0, x1) = x0 + x1 + 1,
       
       [times](x0, x1) = x0 + 1,
       
       [even](x0) = x0 + 1,
       
       [s](x0) = x0 + 1,
       
       [half](x0) = x0 + 1,
       
       [true] = 0,
       
       [0] = 1,
       
       [false] = 0,
       
       [even#](x0) = x0
      Strict:
       even# s s x -> even# x
       2 + 1x >= 0 + 1x
      Weak:
       if_times(false(), s x, y) -> plus(y, times(x, y))
       0 + 0x + 0y >= 2 + 1x + 1y
       if_times(true(), s x, y) -> plus(times(half s x, y), times(half s x, y))
       0 + 0x + 0y >= 7 + 2x + 0y
       times(s x, y) -> if_times(even s x, s x, y)
       2 + 1x + 0y >= 2 + 1x + 0y
       times(0(), y) -> 0()
       2 + 0y >= 1
       plus(s x, y) -> s plus(x, y)
       2 + 1x + 1y >= 2 + 1x + 1y
       plus(0(), y) -> y
       2 + 1y >= 1y
       half s s x -> s half x
       3 + 1x >= 2 + 1x
       half 0() -> 0()
       2 >= 1
       even s s x -> even x
       3 + 1x >= 1 + 1x
       even s 0() -> false()
       3 >= 0
       even 0() -> true()
       2 >= 0
     Qed
   
   
   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))}
    POLY:
     Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
     Interpretation:
      [if_times](x0, x1, x2) = x0,
      
      [plus](x0, x1) = x0 + 1,
      
      [times](x0, x1) = x0 + 1,
      
      [even](x0) = x0 + 1,
      
      [s](x0) = x0 + 1,
      
      [half](x0) = 0,
      
      [true] = 0,
      
      [0] = 1,
      
      [false] = 0,
      
      [plus#](x0, x1) = x0
     Strict:
      plus#(s x, y) -> plus#(x, y)
      1 + 1x + 0y >= 0 + 1x + 0y
     Weak:
      if_times(false(), s x, y) -> plus(y, times(x, y))
      0 + 0x + 0y >= 1 + 0x + 1y
      if_times(true(), s x, y) -> plus(times(half s x, y), times(half s x, y))
      0 + 0x + 0y >= 2 + 0x + 0y
      times(s x, y) -> if_times(even s x, s x, y)
      2 + 1x + 0y >= 2 + 1x + 0y
      times(0(), y) -> 0()
      2 + 0y >= 1
      plus(s x, y) -> s plus(x, y)
      2 + 1x + 0y >= 2 + 1x + 0y
      plus(0(), y) -> y
      2 + 0y >= 1y
      half s s x -> s half x
      0 + 0x >= 1 + 0x
      half 0() -> 0()
      0 >= 1
      even s s x -> even x
      3 + 1x >= 1 + 1x
      even s 0() -> false()
      3 >= 0
      even 0() -> true()
      2 >= 0
    Qed