MAYBE
Time: 0.006287
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() -> 0(),
             inc s x -> s inc x,
          log2(x, y) -> if(le(x, s 0()), x, inc y),
               log x -> log2(x, 0()),
  if(true(), x, s y) -> y,
   if(false(), x, y) -> log2(half x, y)}
 DP:
  DP:
   {       half# s s x -> half# x,
         le#(s x, s y) -> le#(x, y),
              inc# s x -> inc# x,
           log2#(x, y) -> le#(x, s 0()),
           log2#(x, y) -> inc# y,
           log2#(x, y) -> if#(le(x, s 0()), x, inc y),
                log# x -> log2#(x, 0()),
    if#(false(), x, y) -> half# x,
    if#(false(), x, y) -> log2#(half 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() -> 0(),
              inc s x -> s inc x,
           log2(x, y) -> if(le(x, s 0()), x, inc y),
                log x -> log2(x, 0()),
   if(true(), x, s y) -> y,
    if(false(), x, y) -> log2(half x, y)}
  EDG:
   {(inc# s x -> inc# x, inc# s x -> inc# x)
    (log# x -> log2#(x, 0()), log2#(x, y) -> if#(le(x, s 0()), x, inc y))
    (log# x -> log2#(x, 0()), log2#(x, y) -> inc# y)
    (log# x -> log2#(x, 0()), log2#(x, y) -> le#(x, s 0()))
    (le#(s x, s y) -> le#(x, y), le#(s x, s y) -> le#(x, y))
    (log2#(x, y) -> inc# y, inc# s x -> inc# x)
    (log2#(x, y) -> if#(le(x, s 0()), x, inc y), if#(false(), x, y) -> half# x)
    (log2#(x, y) -> if#(le(x, s 0()), x, inc y), if#(false(), x, y) -> log2#(half x, y))
    (log2#(x, y) -> le#(x, s 0()), le#(s x, s y) -> le#(x, y))
    (if#(false(), x, y) -> log2#(half x, y), log2#(x, y) -> le#(x, s 0()))
    (if#(false(), x, y) -> log2#(half x, y), log2#(x, y) -> inc# y)
    (if#(false(), x, y) -> log2#(half x, y), log2#(x, y) -> if#(le(x, s 0()), x, inc y))
    (if#(false(), x, y) -> half# x, half# s s x -> half# x)
    (half# s s x -> half# x, half# s s x -> half# x)}
   EDG:
    {(inc# s x -> inc# x, inc# s x -> inc# x)
     (log# x -> log2#(x, 0()), log2#(x, y) -> if#(le(x, s 0()), x, inc y))
     (log# x -> log2#(x, 0()), log2#(x, y) -> inc# y)
     (log# x -> log2#(x, 0()), log2#(x, y) -> le#(x, s 0()))
     (le#(s x, s y) -> le#(x, y), le#(s x, s y) -> le#(x, y))
     (log2#(x, y) -> inc# y, inc# s x -> inc# x)
     (log2#(x, y) -> if#(le(x, s 0()), x, inc y), if#(false(), x, y) -> half# x)
     (log2#(x, y) -> if#(le(x, s 0()), x, inc y), if#(false(), x, y) -> log2#(half x, y))
     (log2#(x, y) -> le#(x, s 0()), le#(s x, s y) -> le#(x, y))
     (if#(false(), x, y) -> log2#(half x, y), log2#(x, y) -> le#(x, s 0()))
     (if#(false(), x, y) -> log2#(half x, y), log2#(x, y) -> inc# y)
     (if#(false(), x, y) -> log2#(half x, y), log2#(x, y) -> if#(le(x, s 0()), x, inc y))
     (if#(false(), x, y) -> half# x, half# s s x -> half# x)
     (half# s s x -> half# x, half# s s x -> half# x)}
    EDG:
     {(inc# s x -> inc# x, inc# s x -> inc# x)
      (log# x -> log2#(x, 0()), log2#(x, y) -> if#(le(x, s 0()), x, inc y))
      (log# x -> log2#(x, 0()), log2#(x, y) -> inc# y)
      (log# x -> log2#(x, 0()), log2#(x, y) -> le#(x, s 0()))
      (le#(s x, s y) -> le#(x, y), le#(s x, s y) -> le#(x, y))
      (log2#(x, y) -> inc# y, inc# s x -> inc# x)
      (log2#(x, y) -> if#(le(x, s 0()), x, inc y), if#(false(), x, y) -> half# x)
      (log2#(x, y) -> if#(le(x, s 0()), x, inc y), if#(false(), x, y) -> log2#(half x, y))
      (log2#(x, y) -> le#(x, s 0()), le#(s x, s y) -> le#(x, y))
      (if#(false(), x, y) -> log2#(half x, y), log2#(x, y) -> le#(x, s 0()))
      (if#(false(), x, y) -> log2#(half x, y), log2#(x, y) -> inc# y)
      (if#(false(), x, y) -> log2#(half x, y), log2#(x, y) -> if#(le(x, s 0()), x, inc y))
      (if#(false(), x, y) -> half# x, half# s s x -> half# x)
      (half# s s x -> half# x, half# s s x -> half# x)}
     STATUS:
      arrows: 0.827160
      SCCS (4):
       Scc:
        {       log2#(x, y) -> if#(le(x, s 0()), x, inc y),
         if#(false(), x, y) -> log2#(half x, y)}
       Scc:
        {le#(s x, s y) -> le#(x, y)}
       Scc:
        {inc# s x -> inc# x}
       Scc:
        {half# s s x -> half# x}
       
       
       SCC (2):
        Strict:
         {       log2#(x, y) -> if#(le(x, s 0()), x, inc y),
          if#(false(), x, y) -> log2#(half 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() -> 0(),
                    inc s x -> s inc x,
                 log2(x, y) -> if(le(x, s 0()), x, inc y),
                      log x -> log2(x, 0()),
         if(true(), x, s y) -> y,
          if(false(), x, y) -> log2(half x, y)}
        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() -> 0(),
                    inc s x -> s inc x,
                 log2(x, y) -> if(le(x, s 0()), x, inc y),
                      log x -> log2(x, 0()),
         if(true(), x, s y) -> y,
          if(false(), x, y) -> log2(half x, y)}
        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() -> 0(),
                    inc s x -> s inc x,
                 log2(x, y) -> if(le(x, s 0()), x, inc y),
                      log x -> log2(x, 0()),
         if(true(), x, s y) -> y,
          if(false(), x, y) -> log2(half x, y)}
        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() -> 0(),
                    inc s x -> s inc x,
                 log2(x, y) -> if(le(x, s 0()), x, inc y),
                      log x -> log2(x, 0()),
         if(true(), x, s y) -> y,
          if(false(), x, y) -> log2(half x, y)}
        Open