MAYBE

Problem:
 half(x) -> if(ge(x,s(s(0()))),x)
 if(false(),x) -> 0()
 if(true(),x) -> s(half(p(p(x))))
 p(0()) -> 0()
 p(s(x)) -> x
 ge(x,0()) -> true()
 ge(0(),s(x)) -> false()
 ge(s(x),s(y)) -> ge(x,y)
 log(0()) -> 0()
 log(s(x)) -> s(log(half(s(x))))

Proof:
 DP Processor:
  DPs:
   half#(x) -> ge#(x,s(s(0())))
   half#(x) -> if#(ge(x,s(s(0()))),x)
   if#(true(),x) -> p#(x)
   if#(true(),x) -> p#(p(x))
   if#(true(),x) -> half#(p(p(x)))
   ge#(s(x),s(y)) -> ge#(x,y)
   log#(s(x)) -> half#(s(x))
   log#(s(x)) -> log#(half(s(x)))
  TRS:
   half(x) -> if(ge(x,s(s(0()))),x)
   if(false(),x) -> 0()
   if(true(),x) -> s(half(p(p(x))))
   p(0()) -> 0()
   p(s(x)) -> x
   ge(x,0()) -> true()
   ge(0(),s(x)) -> false()
   ge(s(x),s(y)) -> ge(x,y)
   log(0()) -> 0()
   log(s(x)) -> s(log(half(s(x))))
  Usable Rule Processor:
   DPs:
    half#(x) -> ge#(x,s(s(0())))
    half#(x) -> if#(ge(x,s(s(0()))),x)
    if#(true(),x) -> p#(x)
    if#(true(),x) -> p#(p(x))
    if#(true(),x) -> half#(p(p(x)))
    ge#(s(x),s(y)) -> ge#(x,y)
    log#(s(x)) -> half#(s(x))
    log#(s(x)) -> log#(half(s(x)))
   TRS:
    f14(x,y) -> x
    f14(x,y) -> y
    ge(0(),s(x)) -> false()
    ge(s(x),s(y)) -> ge(x,y)
    ge(x,0()) -> true()
    p(0()) -> 0()
    p(s(x)) -> x
    half(x) -> if(ge(x,s(s(0()))),x)
    if(false(),x) -> 0()
    if(true(),x) -> s(half(p(p(x))))
   EDG Processor:
    DPs:
     half#(x) -> ge#(x,s(s(0())))
     half#(x) -> if#(ge(x,s(s(0()))),x)
     if#(true(),x) -> p#(x)
     if#(true(),x) -> p#(p(x))
     if#(true(),x) -> half#(p(p(x)))
     ge#(s(x),s(y)) -> ge#(x,y)
     log#(s(x)) -> half#(s(x))
     log#(s(x)) -> log#(half(s(x)))
    TRS:
     f14(x,y) -> x
     f14(x,y) -> y
     ge(0(),s(x)) -> false()
     ge(s(x),s(y)) -> ge(x,y)
     ge(x,0()) -> true()
     p(0()) -> 0()
     p(s(x)) -> x
     half(x) -> if(ge(x,s(s(0()))),x)
     if(false(),x) -> 0()
     if(true(),x) -> s(half(p(p(x))))
    graph:
     log#(s(x)) -> log#(half(s(x))) -> log#(s(x)) -> half#(s(x))
     log#(s(x)) -> log#(half(s(x))) -> log#(s(x)) -> log#(half(s(x)))
     log#(s(x)) -> half#(s(x)) -> half#(x) -> ge#(x,s(s(0())))
     log#(s(x)) -> half#(s(x)) -> half#(x) -> if#(ge(x,s(s(0()))),x)
     if#(true(),x) -> half#(p(p(x))) -> half#(x) -> ge#(x,s(s(0())))
     if#(true(),x) -> half#(p(p(x))) ->
     half#(x) -> if#(ge(x,s(s(0()))),x)
     ge#(s(x),s(y)) -> ge#(x,y) -> ge#(s(x),s(y)) -> ge#(x,y)
     half#(x) -> if#(ge(x,s(s(0()))),x) -> if#(true(),x) -> p#(x)
     half#(x) -> if#(ge(x,s(s(0()))),x) ->
     if#(true(),x) -> p#(p(x))
     half#(x) -> if#(ge(x,s(s(0()))),x) ->
     if#(true(),x) -> half#(p(p(x)))
     half#(x) -> ge#(x,s(s(0()))) -> ge#(s(x),s(y)) -> ge#(x,y)
    Restore Modifier:
     DPs:
      half#(x) -> ge#(x,s(s(0())))
      half#(x) -> if#(ge(x,s(s(0()))),x)
      if#(true(),x) -> p#(x)
      if#(true(),x) -> p#(p(x))
      if#(true(),x) -> half#(p(p(x)))
      ge#(s(x),s(y)) -> ge#(x,y)
      log#(s(x)) -> half#(s(x))
      log#(s(x)) -> log#(half(s(x)))
     TRS:
      half(x) -> if(ge(x,s(s(0()))),x)
      if(false(),x) -> 0()
      if(true(),x) -> s(half(p(p(x))))
      p(0()) -> 0()
      p(s(x)) -> x
      ge(x,0()) -> true()
      ge(0(),s(x)) -> false()
      ge(s(x),s(y)) -> ge(x,y)
      log(0()) -> 0()
      log(s(x)) -> s(log(half(s(x))))
     SCC Processor:
      #sccs: 3
      #rules: 4
      #arcs: 11/64
      DPs:
       log#(s(x)) -> log#(half(s(x)))
      TRS:
       half(x) -> if(ge(x,s(s(0()))),x)
       if(false(),x) -> 0()
       if(true(),x) -> s(half(p(p(x))))
       p(0()) -> 0()
       p(s(x)) -> x
       ge(x,0()) -> true()
       ge(0(),s(x)) -> false()
       ge(s(x),s(y)) -> ge(x,y)
       log(0()) -> 0()
       log(s(x)) -> s(log(half(s(x))))
      Open
      
      DPs:
       half#(x) -> if#(ge(x,s(s(0()))),x)
       if#(true(),x) -> half#(p(p(x)))
      TRS:
       half(x) -> if(ge(x,s(s(0()))),x)
       if(false(),x) -> 0()
       if(true(),x) -> s(half(p(p(x))))
       p(0()) -> 0()
       p(s(x)) -> x
       ge(x,0()) -> true()
       ge(0(),s(x)) -> false()
       ge(s(x),s(y)) -> ge(x,y)
       log(0()) -> 0()
       log(s(x)) -> s(log(half(s(x))))
      Open
      
      DPs:
       ge#(s(x),s(y)) -> ge#(x,y)
      TRS:
       half(x) -> if(ge(x,s(s(0()))),x)
       if(false(),x) -> 0()
       if(true(),x) -> s(half(p(p(x))))
       p(0()) -> 0()
       p(s(x)) -> x
       ge(x,0()) -> true()
       ge(0(),s(x)) -> false()
       ge(s(x),s(y)) -> ge(x,y)
       log(0()) -> 0()
       log(s(x)) -> s(log(half(s(x))))
      Open