MAYBE We are left with following problem, upon which TcT provides the certificate MAYBE. Strict Trs: { intlist(nil()) -> nil() , intlist(cons(x, y)) -> cons(s(x), intlist(y)) , int(s(x), s(y)) -> intlist(int(x, y)) , int(s(x), 0()) -> nil() , int(0(), s(y)) -> cons(0(), int(s(0()), s(y))) , int(0(), 0()) -> cons(0(), nil()) } Obligation: innermost runtime complexity Answer: MAYBE The input cannot be shown compatible Arrrr..