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