TIMEOUT We are left with following problem, upon which TcT provides the certificate TIMEOUT. Strict 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(s(u), s(v)) -> le(u, v) , le(s(u), 0()) -> false() , le(0(), v) -> true() , double(s(x)) -> s(s(double(x))) , double(0()) -> 0() , square(s(x)) -> s(plus(square(x), double(x))) , square(0()) -> 0() , plus(n, s(m)) -> s(plus(n, m)) , plus(n, 0()) -> n } Obligation: innermost runtime complexity Answer: TIMEOUT Computation stopped due to timeout after 60.0 seconds. Arrrr..