YES(?,PRIMREC) We are left with following problem, upon which TcT provides the certificate YES(?,PRIMREC). Strict Trs: { a__g(X) -> a__h(X) , a__g(X) -> g(X) , a__h(X) -> h(X) , a__h(d()) -> a__g(c()) , a__c() -> d() , a__c() -> c() , mark(d()) -> d() , mark(c()) -> a__c() , mark(g(X)) -> a__g(X) , mark(h(X)) -> a__h(X) } Obligation: innermost runtime complexity Answer: YES(?,PRIMREC) The input was oriented with the instance of'multiset path order' as induced by the precedence a__g > a__h, a__g > c, a__g > g, a__g > h, a__h > h, a__c > a__g, a__c > a__h, a__c > d, a__c > c, a__c > g, a__c > h, d > a__g, d > a__h, d > c, d > g, d > h, mark > a__g, mark > a__h, mark > a__c, mark > d, mark > c, mark > g, mark > h, g > a__h, g > c, g > h, h > c . Hurray, we answered YES(?,PRIMREC)