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