MAYBE
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:
  Strict:
   {      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)}
  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)}
  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))
    (log2#(x, y) -> inc#(y), inc#(s(x)) -> inc#(x))
    (log#(x) -> log2#(x, 0()), log2#(x, y) -> if#(le(x, 0()), le(x, s(0())), x, inc(y)))
    (log#(x) -> log2#(x, 0()), log2#(x, y) -> inc#(y))
    (log#(x) -> log2#(x, 0()), log2#(x, y) -> le#(x, s(0())))
    (log#(x) -> log2#(x, 0()), log2#(x, y) -> le#(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))
    (le#(s(x), s(y)) -> le#(x, y), le#(s(x), s(y)) -> le#(x, y))
    (quot#(s(x), s(y)) -> minus#(x, y), minus#(s(x), s(y)) -> minus#(x, 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))
    (minus#(s(x), s(y)) -> minus#(x, y), minus#(s(x), s(y)) -> minus#(x, 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)))
    (inc#(s(x)) -> inc#(x), inc#(s(x)) -> inc#(x))
    (if2#(false(), x, y) -> log2#(quot(x, s(s(0()))), y), log2#(x, y) -> le#(x, 0()))
    (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) -> inc#(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)))
    (log2#(x, y) -> le#(x, s(0())), le#(s(x), s(y)) -> le#(x, y))}
   SCCS:
    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:
     {quot#(s(x), s(y)) -> quot#(minus(x, y), s(y))}
    Scc:
     {minus#(s(x), s(y)) -> minus#(x, y)}
    Scc:
     {inc#(s(x)) -> inc#(x)}
    Scc:
     {le#(s(x), s(y)) -> le#(x, y)}
    SCC:
     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)}
     Fail
    SCC:
     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)}
     POLY:
      Argument Filtering:
       pi(if2) = [], pi(log_undefined) = [], pi(if) = [], pi(log) = [], pi(log2) = [], pi(quot#) = 0, pi(quot) = [], pi(minus) = 0, pi(inc) = [], pi(s) = [0], pi(false) = [], pi(0) = [], pi(le) = [], pi(true) = []
      Usable Rules:
       {}
      Interpretation:
       [s](x0) = x0 + 1
      Strict:
       {}
      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)}
      Qed
    SCC:
     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)}
     SPSC:
      Simple Projection:
       pi(minus#) = 0
      Strict:
       {}
      Qed
    SCC:
     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)}
     SPSC:
      Simple Projection:
       pi(inc#) = 0
      Strict:
       {}
      Qed
    SCC:
     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)}
     SPSC:
      Simple Projection:
       pi(le#) = 0
      Strict:
       {}
      Qed