We are left with following problem, upon which TcT provides the certificate YES(?,O(n^1)). Strict Trs: { a__f(X) -> f(X) , a__f(f(X)) -> a__c(f(g(f(X)))) , a__c(X) -> d(X) , a__c(X) -> c(X) , a__h(X) -> a__c(d(X)) , a__h(X) -> h(X) , mark(f(X)) -> a__f(mark(X)) , mark(g(X)) -> g(X) , mark(d(X)) -> d(X) , mark(c(X)) -> a__c(X) , mark(h(X)) -> a__h(mark(X)) } Obligation: innermost runtime complexity Answer: YES(?,O(n^1)) The input was oriented with the instance of 'Small Polynomial Path Order (PS,1-bounded)' as induced by the safe mapping safe(a__f) = {1}, safe(f) = {1}, safe(a__c) = {1}, safe(g) = {1}, safe(d) = {1}, safe(a__h) = {1}, safe(mark) = {}, safe(c) = {1}, safe(h) = {1} and precedence a__f > a__c, a__h > a__c, mark > a__f, mark > a__c, mark > a__h . Following symbols are considered recursive: {mark} The recursion depth is 1. For your convenience, here are the satisfied ordering constraints: a__f(; X) > f(; X) a__f(; f(; X)) > a__c(; f(; g(; f(; X)))) a__c(; X) > d(; X) a__c(; X) > c(; X) a__h(; X) > a__c(; d(; X)) a__h(; X) > h(; X) mark(f(; X);) > a__f(; mark(X;)) mark(g(; X);) > g(; X) mark(d(; X);) > d(; X) mark(c(; X);) > a__c(; X) mark(h(; X);) > a__h(; mark(X;)) Hurray, we answered YES(?,O(n^1))