MAYBE We are left with following problem, upon which TcT provides the certificate MAYBE. Strict Trs: { eq(X, Y) -> false() , eq(0(), 0()) -> true() , eq(s(X), s(Y)) -> eq(X, Y) , inf(X) -> cons(X, inf(s(X))) , take(0(), X) -> nil() , take(s(X), cons(Y, L)) -> cons(Y, take(X, L)) , length(cons(X, L)) -> s(length(L)) , length(nil()) -> 0() } Obligation: innermost runtime complexity Answer: MAYBE The input cannot be shown compatible Arrrr..