MAYBE We are left with following problem, upon which TcT provides the certificate MAYBE. Strict Trs: { from(X) -> cons(X, from(s(X))) , head(cons(X, XS)) -> X , 2nd(cons(X, XS)) -> head(XS) , take(s(N), cons(X, XS)) -> cons(X, take(N, XS)) , take(0(), XS) -> nil() , sel(s(N), cons(X, XS)) -> sel(N, XS) , sel(0(), cons(X, XS)) -> X } Obligation: innermost runtime complexity Answer: MAYBE The input cannot be shown compatible Arrrr..