MAYBE
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:
  Strict:
   {       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)}
  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()}
  EDG:
   {(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))
    (le#(s(x), s(y)) -> le#(x, y), le#(s(x), s(y)) -> le#(x, y))
    (logIter#(x, y) -> quot#(x, s(s(0()))), quot#(s(x), s(y)) -> quot#(minus(x, y), s(y)))
    (logIter#(x, y) -> quot#(x, s(s(0()))), quot#(s(x), s(y)) -> minus#(x, y))
    (logIter#(x, y) -> le#(s(0()), x), le#(s(x), s(y)) -> le#(x, y))
    (logIter#(x, y) -> inc#(y), inc#(s(x)) -> inc#(x))
    (logIter#(x, y) -> le#(s(s(0())), x), le#(s(x), s(y)) -> le#(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)))
    (if#(true(), true(), x, y) -> logIter#(x, y), logIter#(x, y) -> quot#(x, s(s(0()))))
    (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) -> le#(s(s(0())), x))
    (if#(true(), true(), x, y) -> logIter#(x, y), logIter#(x, y) -> inc#(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)))
    (quot#(s(x), s(y)) -> minus#(x, y), minus#(s(x), s(y)) -> minus#(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))
    (inc#(s(x)) -> inc#(x), inc#(s(x)) -> inc#(x))}
   SCCS:
    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:
     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:
     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:
     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#) = 0
      Strict:
       {}
      Qed
    SCC:
     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:
      Argument Filtering:
       pi(logZeroError) = [], pi(if) = [], pi(log) = [], pi(logIter) = [], pi(inc) = [], pi(false) = [], pi(le) = [], pi(true) = [], pi(quot#) = 0, pi(quot) = [], pi(s) = [0], pi(0) = [], pi(minus) = 0
      Usable Rules:
       {}
      Interpretation:
       [s](x0) = x0 + 1
      Strict:
       {}
      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()}
      Qed
    SCC:
     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#) = 0
      Strict:
       {}
      Qed