MAYBE
Time: 0.006235
TRS:
 {          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,
         minus(x, 0()) -> x,
         minus(0(), y) -> 0(),
       minus(s x, s y) -> minus(x, y),
        quot(0(), s y) -> 0(),
        quot(s x, s y) -> s quot(minus(x, y), s y),
            log2(x, y) -> if(le(x, 0()), le(x, s 0()), x, inc y),
                 log x -> log2(x, 0()),
   if(true(), b, x, y) -> log_undefined(),
  if(false(), b, x, y) -> if2(b, x, y),
   if2(true(), x, s y) -> y,
    if2(false(), x, y) -> log2(quot(x, s s 0()), y)}
 DP:
  DP:
   {        le#(s x, s y) -> le#(x, y),
                 inc# s x -> inc# x,
         minus#(s x, s y) -> minus#(x, y),
          quot#(s x, s y) -> minus#(x, y),
          quot#(s x, s y) -> quot#(minus(x, y), s y),
              log2#(x, y) -> le#(x, 0()),
              log2#(x, y) -> le#(x, s 0()),
              log2#(x, y) -> inc# y,
              log2#(x, y) -> if#(le(x, 0()), le(x, s 0()), x, inc y),
                   log# x -> log2#(x, 0()),
    if#(false(), b, x, y) -> if2#(b, x, y),
      if2#(false(), x, y) -> quot#(x, s s 0()),
      if2#(false(), x, y) -> log2#(quot(x, s s 0()), y)}
  TRS:
  {          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,
          minus(x, 0()) -> x,
          minus(0(), y) -> 0(),
        minus(s x, s y) -> minus(x, y),
         quot(0(), s y) -> 0(),
         quot(s x, s y) -> s quot(minus(x, y), s y),
             log2(x, y) -> if(le(x, 0()), le(x, s 0()), x, inc y),
                  log x -> log2(x, 0()),
    if(true(), b, x, y) -> log_undefined(),
   if(false(), b, x, y) -> if2(b, x, y),
    if2(true(), x, s y) -> y,
     if2(false(), x, y) -> log2(quot(x, s s 0()), y)}
  EDG:
   {(if2#(false(), x, y) -> quot#(x, s s 0()), quot#(s x, s y) -> quot#(minus(x, y), s y))
    (if2#(false(), x, y) -> quot#(x, s s 0()), quot#(s x, s y) -> minus#(x, y))
    (if2#(false(), x, y) -> log2#(quot(x, s s 0()), y), log2#(x, y) -> if#(le(x, 0()), le(x, s 0()), x, inc y))
    (if2#(false(), x, y) -> log2#(quot(x, s s 0()), y), log2#(x, y) -> inc# y)
    (if2#(false(), x, y) -> log2#(quot(x, s s 0()), y), log2#(x, y) -> le#(x, s 0()))
    (if2#(false(), x, y) -> log2#(quot(x, s s 0()), y), log2#(x, y) -> le#(x, 0()))
    (log2#(x, y) -> inc# y, inc# s x -> inc# x)
    (inc# s x -> inc# x, inc# s x -> inc# x)
    (quot#(s x, s y) -> quot#(minus(x, y), s y), quot#(s x, s y) -> quot#(minus(x, y), s y))
    (quot#(s x, s y) -> quot#(minus(x, y), s y), quot#(s x, s y) -> minus#(x, y))
    (minus#(s x, s y) -> minus#(x, y), minus#(s x, s y) -> minus#(x, y))
    (quot#(s x, s y) -> minus#(x, y), minus#(s x, s y) -> minus#(x, y))
    (le#(s x, s y) -> le#(x, y), le#(s x, s y) -> le#(x, y))
    (log2#(x, y) -> if#(le(x, 0()), le(x, s 0()), x, inc y), if#(false(), b, x, y) -> if2#(b, x, y))
    (log# x -> log2#(x, 0()), log2#(x, y) -> le#(x, 0()))
    (log# x -> log2#(x, 0()), log2#(x, y) -> le#(x, s 0()))
    (log# x -> log2#(x, 0()), log2#(x, y) -> inc# y)
    (log# x -> log2#(x, 0()), log2#(x, y) -> if#(le(x, 0()), le(x, s 0()), x, inc y))
    (if#(false(), b, x, y) -> if2#(b, x, y), if2#(false(), x, y) -> quot#(x, s s 0()))
    (if#(false(), b, x, y) -> if2#(b, x, y), if2#(false(), x, y) -> log2#(quot(x, s s 0()), y))
    (log2#(x, y) -> le#(x, s 0()), le#(s x, s y) -> le#(x, y))}
   STATUS:
    arrows: 0.875740
    SCCS (5):
     Scc:
      {          log2#(x, y) -> if#(le(x, 0()), le(x, s 0()), x, inc y),
       if#(false(), b, x, y) -> if2#(b, x, y),
         if2#(false(), x, y) -> log2#(quot(x, s s 0()), y)}
     Scc:
      {inc# s x -> inc# x}
     Scc:
      {quot#(s x, s y) -> quot#(minus(x, y), s y)}
     Scc:
      {minus#(s x, s y) -> minus#(x, y)}
     Scc:
      {le#(s x, s y) -> le#(x, y)}
     
     
     SCC (3):
      Strict:
       {          log2#(x, y) -> if#(le(x, 0()), le(x, s 0()), x, inc y),
        if#(false(), b, x, y) -> if2#(b, x, y),
          if2#(false(), x, y) -> log2#(quot(x, s s 0()), y)}
      Weak:
      {          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,
              minus(x, 0()) -> x,
              minus(0(), y) -> 0(),
            minus(s x, s y) -> minus(x, y),
             quot(0(), s y) -> 0(),
             quot(s x, s y) -> s quot(minus(x, y), s y),
                 log2(x, y) -> if(le(x, 0()), le(x, s 0()), x, inc y),
                      log x -> log2(x, 0()),
        if(true(), b, x, y) -> log_undefined(),
       if(false(), b, x, y) -> if2(b, x, y),
        if2(true(), x, s y) -> y,
         if2(false(), x, y) -> log2(quot(x, s s 0()), y)}
      Open
     
     SCC (1):
      Strict:
       {inc# s x -> inc# x}
      Weak:
      {          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,
              minus(x, 0()) -> x,
              minus(0(), y) -> 0(),
            minus(s x, s y) -> minus(x, y),
             quot(0(), s y) -> 0(),
             quot(s x, s y) -> s quot(minus(x, y), s y),
                 log2(x, y) -> if(le(x, 0()), le(x, s 0()), x, inc y),
                      log x -> log2(x, 0()),
        if(true(), b, x, y) -> log_undefined(),
       if(false(), b, x, y) -> if2(b, x, y),
        if2(true(), x, s y) -> y,
         if2(false(), x, y) -> log2(quot(x, s s 0()), y)}
      Open
     
     
     SCC (1):
      Strict:
       {quot#(s x, s y) -> quot#(minus(x, y), s y)}
      Weak:
      {          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,
              minus(x, 0()) -> x,
              minus(0(), y) -> 0(),
            minus(s x, s y) -> minus(x, y),
             quot(0(), s y) -> 0(),
             quot(s x, s y) -> s quot(minus(x, y), s y),
                 log2(x, y) -> if(le(x, 0()), le(x, s 0()), x, inc y),
                      log x -> log2(x, 0()),
        if(true(), b, x, y) -> log_undefined(),
       if(false(), b, x, y) -> if2(b, x, y),
        if2(true(), x, s y) -> y,
         if2(false(), x, y) -> log2(quot(x, s s 0()), y)}
      Open
     
     SCC (1):
      Strict:
       {minus#(s x, s y) -> minus#(x, y)}
      Weak:
      {          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,
              minus(x, 0()) -> x,
              minus(0(), y) -> 0(),
            minus(s x, s y) -> minus(x, y),
             quot(0(), s y) -> 0(),
             quot(s x, s y) -> s quot(minus(x, y), s y),
                 log2(x, y) -> if(le(x, 0()), le(x, s 0()), x, inc y),
                      log x -> log2(x, 0()),
        if(true(), b, x, y) -> log_undefined(),
       if(false(), b, x, y) -> if2(b, x, y),
        if2(true(), x, s y) -> y,
         if2(false(), x, y) -> log2(quot(x, s s 0()), y)}
      Open
     
     SCC (1):
      Strict:
       {le#(s x, s y) -> le#(x, y)}
      Weak:
      {          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,
              minus(x, 0()) -> x,
              minus(0(), y) -> 0(),
            minus(s x, s y) -> minus(x, y),
             quot(0(), s y) -> 0(),
             quot(s x, s y) -> s quot(minus(x, y), s y),
                 log2(x, y) -> if(le(x, 0()), le(x, s 0()), x, inc y),
                      log x -> log2(x, 0()),
        if(true(), b, x, y) -> log_undefined(),
       if(false(), b, x, y) -> if2(b, x, y),
        if2(true(), x, s y) -> y,
         if2(false(), x, y) -> log2(quot(x, s s 0()), y)}
      Open