MAYBE
Time: 0.040245
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))}
   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()}
     Fail
    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()}
     SPSC:
      Simple Projection:
       pi(inc#) = 0
      Strict:
       {}
      Qed
    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()}
     SPSC:
      Simple Projection:
       pi(le#) = 1
      Strict:
       {}
      Qed
    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()}
     POLY:
      Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
      Interpretation:
       [if](x0, x1, x2, x3) = x0 + x1 + 1,
       
       [minus](x0, x1) = x0,
       
       [quot](x0, x1) = x0 + 1,
       
       [le](x0, x1) = x0 + 1,
       
       [logIter](x0, x1) = x0 + 1,
       
       [s](x0) = x0 + 1,
       
       [inc](x0) = x0 + 1,
       
       [log](x0) = 0,
       
       [0] = 1,
       
       [true] = 0,
       
       [false] = 0,
       
       [logZeroError] = 0,
       
       [quot#](x0, x1) = x0 + 1
      Strict:
       quot#(s x, s y) -> quot#(minus(x, y), s y)
       2 + 1x + 0y >= 1 + 1x + 0y
      Weak:
       
     Qed
   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()}
    SPSC:
     Simple Projection:
      pi(minus#) = 1
     Strict:
      {}
     Qed