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