MAYBE
Time: 0.010354
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))}
   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))}
    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