MAYBE
Time: 0.004119
TRS:
 {              minus(x, 0()) -> x,
              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),
                   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), quot(x, s s 0()), inc y),
                        log 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()}
 DP:
  DP:
   {         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),
                le#(s x, s y) -> le#(x, y),
                     inc# s x -> inc# x,
               logIter#(x, y) -> quot#(x, s s 0()),
               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), quot(x, s s 0()), inc y),
                       log# x -> logIter#(x, 0()),
    if#(true(), true(), x, y) -> logIter#(x, y)}
  TRS:
  {              minus(x, 0()) -> x,
               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),
                    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), quot(x, s s 0()), inc y),
                         log 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()}
  EDG:
   {(logIter#(x, y) -> if#(le(s 0(), x), le(s s 0(), x), quot(x, s s 0()), inc y), if#(true(), true(), x, y) -> logIter#(x, y))
    (logIter#(x, y) -> inc# y, inc# s x -> inc# x)
    (quot#(s x, s y) -> minus#(x, y), minus#(s x, s y) -> minus#(x, y))
    (if#(true(), true(), x, y) -> logIter#(x, y), logIter#(x, y) -> if#(le(s 0(), x), le(s s 0(), x), quot(x, s s 0()), 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) -> quot#(x, s s 0()))
    (inc# s x -> inc# x, inc# s x -> inc# x)
    (logIter#(x, y) -> le#(s s 0(), x), le#(s x, s y) -> le#(x, y))
    (logIter#(x, y) -> le#(s 0(), x), le#(s x, s y) -> le#(x, y))
    (logIter#(x, y) -> quot#(x, s s 0()), quot#(s x, s y) -> minus#(x, y))
    (logIter#(x, y) -> quot#(x, s s 0()), quot#(s x, s y) -> quot#(minus(x, y), s y))
    (le#(s x, s y) -> le#(x, y), le#(s x, s y) -> le#(x, y))
    (minus#(s x, s y) -> minus#(x, y), minus#(s x, s y) -> minus#(x, y))
    (log# x -> logIter#(x, 0()), logIter#(x, y) -> quot#(x, s s 0()))
    (log# x -> logIter#(x, 0()), logIter#(x, y) -> le#(s 0(), x))
    (log# x -> logIter#(x, 0()), logIter#(x, y) -> le#(s s 0(), x))
    (log# x -> logIter#(x, 0()), logIter#(x, y) -> inc# y)
    (log# x -> logIter#(x, 0()), logIter#(x, y) -> if#(le(s 0(), x), le(s s 0(), x), quot(x, s s 0()), inc y))
    (quot#(s x, s y) -> quot#(minus(x, y), s y), quot#(s x, s y) -> minus#(x, y))
    (quot#(s x, s y) -> quot#(minus(x, y), s y), quot#(s x, s y) -> quot#(minus(x, y), s y))}
   STATUS:
    arrows: 0.847222
    SCCS (5):
     Scc:
      {           logIter#(x, y) -> if#(le(s 0(), x), le(s s 0(), x), quot(x, s s 0()), inc y),
       if#(true(), true(), x, y) -> logIter#(x, y)}
     Scc:
      {inc# s x -> inc# x}
     Scc:
      {le#(s x, s y) -> le#(x, y)}
     Scc:
      {quot#(s x, s y) -> quot#(minus(x, y), s y)}
     Scc:
      {minus#(s x, s y) -> minus#(x, y)}
     
     
     SCC (2):
      Strict:
       {           logIter#(x, y) -> if#(le(s 0(), x), le(s s 0(), x), quot(x, s s 0()), inc y),
        if#(true(), true(), x, y) -> logIter#(x, y)}
      Weak:
      {              minus(x, 0()) -> x,
                   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),
                        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), quot(x, s s 0()), inc y),
                             log 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()}
      Open
     
     SCC (1):
      Strict:
       {inc# s x -> inc# x}
      Weak:
      {              minus(x, 0()) -> x,
                   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),
                        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), quot(x, s s 0()), inc y),
                             log 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()}
      Open
     
     
     SCC (1):
      Strict:
       {le#(s x, s y) -> le#(x, y)}
      Weak:
      {              minus(x, 0()) -> x,
                   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),
                        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), quot(x, s s 0()), inc y),
                             log 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()}
      Open
     
     SCC (1):
      Strict:
       {quot#(s x, s y) -> quot#(minus(x, y), s y)}
      Weak:
      {              minus(x, 0()) -> x,
                   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),
                        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), quot(x, s s 0()), inc y),
                             log 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()}
      Open
     
     SCC (1):
      Strict:
       {minus#(s x, s y) -> minus#(x, y)}
      Weak:
      {              minus(x, 0()) -> x,
                   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),
                        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), quot(x, s s 0()), inc y),
                             log 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()}
      Open