Input TRS: 1: s(s(|0|())) -> f(s(|0|())) 2: g(x) -> h(x,x) 3: s(x) -> h(x,|0|()) 4: s(x) -> h(|0|(),x) 5: f(g(x)) -> g(g(f(x))) 6: g(s(x)) -> s(s(g(x))) 7: h(f(x),g(x)) -> f(s(x)) 8: s(|0|()) -> k(|0|()) 9: s(k(|0|())) -> |0|() 10: s(s(|0|())) -> k(s(|0|())) 11: k(s(|0|())) -> |0|() 12: s(s(s(s(s(s(s(|0|()))))))) -> k(s(s(|0|()))) 13: k(s(s(|0|()))) -> s(s(s(s(s(|0|()))))) 14: h(k(x),g(x)) -> k(s(x)) Number of strict rules: 14 Direct Order(PosReal,>,Poly) ... failed. Freezing ... failed. Dependency Pairs: #1: #g(x) -> #h(x,x) #2: #g(s(x)) -> #s(s(g(x))) #3: #g(s(x)) -> #s(g(x)) #4: #g(s(x)) -> #g(x) #5: #k(s(s(|0|()))) -> #s(s(s(s(s(|0|()))))) #6: #k(s(s(|0|()))) -> #s(s(s(s(|0|())))) #7: #k(s(s(|0|()))) -> #s(s(s(|0|()))) #8: #s(s(s(s(s(s(s(|0|()))))))) -> #k(s(s(|0|()))) #9: #h(k(x),g(x)) -> #k(s(x)) #10: #h(k(x),g(x)) -> #s(x) #11: #h(f(x),g(x)) -> #f(s(x)) #12: #h(f(x),g(x)) -> #s(x) #13: #s(s(|0|())) -> #k(s(|0|())) #14: #f(g(x)) -> #g(g(f(x))) #15: #f(g(x)) -> #g(f(x)) #16: #f(g(x)) -> #f(x) #17: #s(x) -> #h(x,|0|()) #18: #s(s(|0|())) -> #f(s(|0|())) #19: #s(|0|()) -> #k(|0|()) #20: #s(x) -> #h(|0|(),x) Number of SCCs: 2, DPs: 2, edges: 2 SCC { #4 } Removing DPs: Order(PosReal,>,Sum)... succeeded. |0|() weight: 0 h(x1,x2) weight: 0 s(x1) weight: (/ 1 2) + x1 k(x1) weight: 0 f(x1) weight: 0 #h(x1,x2) weight: 0 #k(x1) weight: 0 #s(x1) weight: 0 #f(x1) weight: 0 #g(x1) weight: x1 g(x1) weight: 0 Usable rules: { } Removed DPs: #4 Number of SCCs: 1, DPs: 1, edges: 1 SCC { #16 } Removing DPs: Order(PosReal,>,Sum)... succeeded. |0|() weight: 0 h(x1,x2) weight: 0 s(x1) weight: (/ 1 2) k(x1) weight: 0 f(x1) weight: 0 #h(x1,x2) weight: 0 #k(x1) weight: 0 #s(x1) weight: 0 #f(x1) weight: x1 #g(x1) weight: 0 g(x1) weight: (/ 1 2) + x1 Usable rules: { } Removed DPs: #16 Number of SCCs: 0, DPs: 0, edges: 0 YES