MAYBE
Time: 0.492589
TRS:
 {                   half 0() -> 0(),
                   half s 0() -> 0(),
                   half s s x -> s half x,
                   le(0(), y) -> true(),
                 le(s x, 0()) -> false(),
                 le(s x, s y) -> le(x, y),
                      inc 0() -> s 0(),
                      inc s x -> s inc x,
                logIter(x, y) -> if(le(s 0(), x), le(s s 0(), x), half x, inc y),
                  logarithm x -> logIter(x, 0()),
     if(true(), true(), x, y) -> logIter(x, y),
  if(true(), false(), x, s y) -> y,
         if(false(), b, x, y) -> logZeroError(),
                          f() -> g(),
                          f() -> h()}
 DP:
  DP:
   {              half# s s x -> half# x,
                le#(s x, s y) -> le#(x, y),
                     inc# s x -> inc# x,
               logIter#(x, y) -> half# x,
               logIter#(x, y) -> le#(s 0(), x),
               logIter#(x, y) -> le#(s s 0(), x),
               logIter#(x, y) -> inc# y,
               logIter#(x, y) -> if#(le(s 0(), x), le(s s 0(), x), half x, inc y),
                 logarithm# x -> logIter#(x, 0()),
    if#(true(), true(), x, y) -> logIter#(x, y)}
  TRS:
  {                   half 0() -> 0(),
                    half s 0() -> 0(),
                    half s s x -> s half x,
                    le(0(), y) -> true(),
                  le(s x, 0()) -> false(),
                  le(s x, s y) -> le(x, y),
                       inc 0() -> s 0(),
                       inc s x -> s inc x,
                 logIter(x, y) -> if(le(s 0(), x), le(s s 0(), x), half x, inc y),
                   logarithm x -> logIter(x, 0()),
      if(true(), true(), x, y) -> logIter(x, y),
   if(true(), false(), x, s y) -> y,
          if(false(), b, x, y) -> logZeroError(),
                           f() -> g(),
                           f() -> h()}
  UR:
   {    half 0() -> 0(),
      half s 0() -> 0(),
      half s s x -> s half x,
      le(0(), y) -> true(),
    le(s x, 0()) -> false(),
    le(s x, s y) -> le(x, y),
         inc 0() -> s 0(),
         inc s x -> s inc x,
         a(z, w) -> z,
         a(z, w) -> w}
   EDG:
    {(logIter#(x, y) -> if#(le(s 0(), x), le(s s 0(), x), half x, inc y), if#(true(), true(), x, y) -> logIter#(x, y))
     (if#(true(), true(), x, y) -> logIter#(x, y), logIter#(x, y) -> if#(le(s 0(), x), le(s s 0(), x), half x, inc y))
     (if#(true(), true(), x, y) -> logIter#(x, y), logIter#(x, y) -> inc# y)
     (if#(true(), true(), x, y) -> logIter#(x, y), logIter#(x, y) -> le#(s s 0(), x))
     (if#(true(), true(), x, y) -> logIter#(x, y), logIter#(x, y) -> le#(s 0(), x))
     (if#(true(), true(), x, y) -> logIter#(x, y), logIter#(x, y) -> half# x)
     (logIter#(x, y) -> le#(s s 0(), x), le#(s x, s y) -> le#(x, y))
     (half# s s x -> half# x, half# s s x -> half# x)
     (logIter#(x, y) -> half# x, half# s s x -> half# x)
     (inc# s x -> inc# x, inc# s x -> inc# x)
     (logarithm# x -> logIter#(x, 0()), logIter#(x, y) -> half# x)
     (logarithm# x -> logIter#(x, 0()), logIter#(x, y) -> le#(s 0(), x))
     (logarithm# x -> logIter#(x, 0()), logIter#(x, y) -> le#(s s 0(), x))
     (logarithm# x -> logIter#(x, 0()), logIter#(x, y) -> inc# y)
     (logarithm# x -> logIter#(x, 0()), logIter#(x, y) -> if#(le(s 0(), x), le(s s 0(), x), half x, inc y))
     (logIter#(x, y) -> le#(s 0(), x), le#(s x, s y) -> le#(x, y))
     (le#(s x, s y) -> le#(x, y), le#(s x, s y) -> le#(x, y))
     (logIter#(x, y) -> inc# y, inc# s x -> inc# x)}
    STATUS:
     arrows: 0.820000
     SCCS (4):
      Scc:
       {           logIter#(x, y) -> if#(le(s 0(), x), le(s s 0(), x), half x, inc y),
        if#(true(), true(), x, y) -> logIter#(x, y)}
      Scc:
       {le#(s x, s y) -> le#(x, y)}
      Scc:
       {half# s s x -> half# x}
      Scc:
       {inc# s x -> inc# x}
      
      
      SCC (2):
       Strict:
        {           logIter#(x, y) -> if#(le(s 0(), x), le(s s 0(), x), half x, inc y),
         if#(true(), true(), x, y) -> logIter#(x, y)}
       Weak:
       {                   half 0() -> 0(),
                         half s 0() -> 0(),
                         half s s x -> s half x,
                         le(0(), y) -> true(),
                       le(s x, 0()) -> false(),
                       le(s x, s y) -> le(x, y),
                            inc 0() -> s 0(),
                            inc s x -> s inc x,
                      logIter(x, y) -> if(le(s 0(), x), le(s s 0(), x), half x, inc y),
                        logarithm x -> logIter(x, 0()),
           if(true(), true(), x, y) -> logIter(x, y),
        if(true(), false(), x, s y) -> y,
               if(false(), b, x, y) -> logZeroError(),
                                f() -> g(),
                                f() -> h()}
       Open
      
      
      SCC (1):
       Strict:
        {le#(s x, s y) -> le#(x, y)}
       Weak:
       {                   half 0() -> 0(),
                         half s 0() -> 0(),
                         half s s x -> s half x,
                         le(0(), y) -> true(),
                       le(s x, 0()) -> false(),
                       le(s x, s y) -> le(x, y),
                            inc 0() -> s 0(),
                            inc s x -> s inc x,
                      logIter(x, y) -> if(le(s 0(), x), le(s s 0(), x), half x, inc y),
                        logarithm x -> logIter(x, 0()),
           if(true(), true(), x, y) -> logIter(x, y),
        if(true(), false(), x, s y) -> y,
               if(false(), b, x, y) -> logZeroError(),
                                f() -> g(),
                                f() -> h()}
       Open
      
      SCC (1):
       Strict:
        {half# s s x -> half# x}
       Weak:
       {                   half 0() -> 0(),
                         half s 0() -> 0(),
                         half s s x -> s half x,
                         le(0(), y) -> true(),
                       le(s x, 0()) -> false(),
                       le(s x, s y) -> le(x, y),
                            inc 0() -> s 0(),
                            inc s x -> s inc x,
                      logIter(x, y) -> if(le(s 0(), x), le(s s 0(), x), half x, inc y),
                        logarithm x -> logIter(x, 0()),
           if(true(), true(), x, y) -> logIter(x, y),
        if(true(), false(), x, s y) -> y,
               if(false(), b, x, y) -> logZeroError(),
                                f() -> g(),
                                f() -> h()}
       Open
      
      SCC (1):
       Strict:
        {inc# s x -> inc# x}
       Weak:
       {                   half 0() -> 0(),
                         half s 0() -> 0(),
                         half s s x -> s half x,
                         le(0(), y) -> true(),
                       le(s x, 0()) -> false(),
                       le(s x, s y) -> le(x, y),
                            inc 0() -> s 0(),
                            inc s x -> s inc x,
                      logIter(x, y) -> if(le(s 0(), x), le(s s 0(), x), half x, inc y),
                        logarithm x -> logIter(x, 0()),
           if(true(), true(), x, y) -> logIter(x, y),
        if(true(), false(), x, s y) -> y,
               if(false(), b, x, y) -> logZeroError(),
                                f() -> g(),
                                f() -> h()}
       Open