Input TRS: 1: a__c() -> a__f(g(c())) 2: a__f(g(X)) -> g(X) 3: mark(c()) -> a__c() 4: mark(f(X)) -> a__f(X) 5: mark(g(X)) -> g(X) 6: a__c() -> c() 7: a__f(X) -> f(X) Number of strict rules: 7 Direct Order(PosReal,>,Poly) ... removes: 4 3 5 a__f(x1) weight: x1 c() weight: 0 f(x1) weight: x1 mark(x1) weight: (/ 1 2) + x1 g(x1) weight: x1 a__c() weight: 0 Number of strict rules: 4 Direct Order(PosReal,>,Poly) ... failed. Freezing ... failed. Dependency Pairs: #1: #a__c() -> #a__f(g(c())) Number of SCCs: 0, DPs: 0, edges: 0 YES