MAYBE
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()
 }
 DUP: We consider a duplicating system.
  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()
   }
  Fail