Input TRS: 1: f(f(X)) -> c(n__f(n__g(n__f(X)))) 2: c(X) -> d(activate(X)) 3: h(X) -> c(n__d(X)) 4: f(X) -> n__f(X) 5: g(X) -> n__g(X) 6: d(X) -> n__d(X) 7: activate(n__f(X)) -> f(activate(X)) 8: activate(n__g(X)) -> g(X) 9: activate(n__d(X)) -> d(X) 10: activate(X) -> X Number of strict rules: 10 Direct Order(PosReal,>,Poly) ... removes: 3 h(x1) weight: (/ 1 8) + 2 * x1 d(x1) weight: x1 activate(x1) weight: x1 c(x1) weight: x1 f(x1) weight: (/ 1 8) + x1 n__f(x1) weight: (/ 1 8) + x1 n__g(x1) weight: x1 n__d(x1) weight: x1 g(x1) weight: x1 Number of strict rules: 9 Direct Order(PosReal,>,Poly) ... failed. Freezing ... failed. Dependency Pairs: #1: #c(X) -> #d(activate(X)) #2: #c(X) -> #activate(X) #3: #activate(n__d(X)) -> #d(X) #4: #activate(n__f(X)) -> #f(activate(X)) #5: #activate(n__f(X)) -> #activate(X) #6: #f(f(X)) -> #c(n__f(n__g(n__f(X)))) #7: #activate(n__g(X)) -> #g(X) Number of SCCs: 1, DPs: 4, edges: 6 SCC { #2 #4..6 } Removing DPs: Order(PosReal,>,Sum)... succeeded. h(x1) weight: 0 d(x1) weight: (/ 1 4) activate(x1) weight: x1 #activate(x1) weight: x1 c(x1) weight: (/ 1 4) f(x1) weight: (/ 1 4) + x1 n__f(x1) weight: (/ 1 4) + x1 #d(x1) weight: 0 #f(x1) weight: (/ 1 4) + x1 #g(x1) weight: 0 n__g(x1) weight: x1 #c(x1) weight: x1 n__d(x1) weight: (/ 1 4) g(x1) weight: x1 Usable rules: { 1 2 4..10 } Removed DPs: #5 Number of SCCs: 1, DPs: 3, edges: 3 SCC { #2 #4 #6 } Removing DPs: Order(PosReal,>,Sum)... succeeded. h(x1) weight: 0 d(x1) weight: (/ 1 2) activate(x1) weight: x1 #activate(x1) weight: x1 c(x1) weight: (/ 1 2) f(x1) weight: 2 + x1 n__f(x1) weight: 2 + x1 #d(x1) weight: 0 #f(x1) weight: (/ 3 2) + x1 #g(x1) weight: 0 n__g(x1) weight: (/ 1 2) #c(x1) weight: (/ 1 2) + x1 n__d(x1) weight: (/ 1 2) g(x1) weight: (/ 1 2) Usable rules: { 1 2 4..10 } Removed DPs: #2 #4 #6 Number of SCCs: 0, DPs: 0, edges: 0 YES