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