MAYBE We are left with following problem, upon which TcT provides the certificate MAYBE. Strict Trs: { rev(ls) -> r1(ls, empty()) , r1(empty(), a) -> a , r1(cons(x, k), a) -> r1(k, cons(x, a)) } Obligation: innermost runtime complexity Answer: MAYBE The input cannot be shown compatible Arrrr..