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