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(0(), y) -> 0(),
         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))),
                log(x) -> log2(x, 0()),
            log2(x, y) -> if(le(x, 0()), le(x, s(0())), x, inc(y)),
   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