MAYBE

Problem:
 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))

Proof:
 DP Processor:
  DPs:
   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) -> times#(half(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) -> times#(x,y)
   if_times#(false(),s(x),y) -> plus#(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))
  ADG Processor:
   DPs:
    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) -> times#(half(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) -> times#(x,y)
    if_times#(false(),s(x),y) -> plus#(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))
   graph:
    if_times#(false(),s(x),y) -> times#(x,y) ->
    times#(s(x),y) -> even#(s(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) -> plus#(y,times(x,y)) ->
    plus#(s(x),y) -> plus#(x,y)
    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)
    if_times#(true(),s(x),y) -> plus#(times(half(s(x)),y),times(half(s(x)),y)) ->
    plus#(s(x),y) -> plus#(x,y)
    if_times#(true(),s(x),y) -> half#(s(x)) ->
    half#(s(s(x))) -> half#(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) -> 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#(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) -> even#(s(x)) -> even#(s(s(x))) -> even#(x)
    plus#(s(x),y) -> plus#(x,y) -> plus#(s(x),y) -> plus#(x,y)
    half#(s(s(x))) -> half#(x) -> half#(s(s(x))) -> half#(x)
    even#(s(s(x))) -> even#(x) -> even#(s(s(x))) -> even#(x)
   SCC Processor:
    #sccs: 4
    #rules: 6
    #arcs: 16/100
    DPs:
     if_times#(false(),s(x),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)
    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))
    Open
    
    DPs:
     half#(s(s(x))) -> half#(x)
    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))
    Open
    
    DPs:
     even#(s(s(x))) -> even#(x)
    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))
    Open
    
    DPs:
     plus#(s(x),y) -> plus#(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))
    Open