TRS: { log(x, s(s(y))) -> cond(le(x, s(s(y))), x, y), cond(true(), x, y) -> s(0()), cond(false(), x, y) -> double(log(x, square(s(s(y))))), le(0(), v) -> true(), le(s(u), 0()) -> false(), le(s(u), s(v)) -> le(u, v), double(0()) -> 0(), double(s(x)) -> s(s(double(x))), square(0()) -> 0(), square(s(x)) -> s(plus(square(x), double(x))), plus(n, 0()) -> n, plus(n, s(m)) -> s(plus(n, m))} Fail