Input TRS: 1: f(g(x)) -> g(g(f(x))) 2: g(s(x)) -> s(s(g(x))) 3: s(x) -> h(0(),x) 4: s(x) -> h(x,0()) 5: f(0()) -> 0() 6: s(s(s(0()))) -> f(s(0())) 7: f(s(0())) -> s(0()) 8: h(f(x),g(x)) -> f(s(x)) 9: g(x) -> h(h(h(h(x,x),x),x),x) 10: f(s(s(x))) -> h(f(x),g(h(x,x))) 11: s(0()) -> r(0()) 12: s(s(s(0()))) -> r(s(0())) 13: r(s(0())) -> s(0()) 14: g(x) -> r(x) 15: s(0()) -> p(0()) 16: s(s(0())) -> p(s(0())) 17: p(s(0())) -> 0() 18: s(s(s(s(s(0()))))) -> p(s(s(0()))) 19: p(s(s(0()))) -> s(s(s(0()))) 20: h(p(x),g(x)) -> p(s(x)) 21: s(0()) -> k(0()) 22: s(s(p(p(a())))) -> s(k(p(a()))) 23: s(k(p(a()))) -> p(p(a())) 24: g(x) -> k(x) 25: a() -> 0() 26: s(h(r(k(p(x))),r(x))) -> h(r(r(p(x))),k(x)) Number of strict rules: 26 Direct Order(PosReal,>,Poly) ... failed. Freezing ... failed. Dependency Pairs: #1: #g(s(x)) -> #s(s(g(x))) #2: #g(s(x)) -> #s(g(x)) #3: #g(s(x)) -> #g(x) #4: #s(s(s(0()))) -> #f(s(0())) #5: #g(x) -> #h(h(h(h(x,x),x),x),x) #6: #g(x) -> #h(h(h(x,x),x),x) #7: #g(x) -> #h(h(x,x),x) #8: #g(x) -> #h(x,x) #9: #s(0()) -> #r(0()) #10: #s(k(p(a()))) -> #p(p(a())) #11: #s(s(s(0()))) -> #r(s(0())) #12: #g(x) -> #r(x) #13: #h(p(x),g(x)) -> #p(s(x)) #14: #h(p(x),g(x)) -> #s(x) #15: #f(s(s(x))) -> #h(f(x),g(h(x,x))) #16: #f(s(s(x))) -> #f(x) #17: #f(s(s(x))) -> #g(h(x,x)) #18: #f(s(s(x))) -> #h(x,x) #19: #s(s(p(p(a())))) -> #s(k(p(a()))) #20: #p(s(s(0()))) -> #s(s(s(0()))) #21: #s(h(r(k(p(x))),r(x))) -> #h(r(r(p(x))),k(x)) #22: #s(h(r(k(p(x))),r(x))) -> #r(r(p(x))) #23: #s(h(r(k(p(x))),r(x))) -> #r(p(x)) #24: #s(s(0())) -> #p(s(0())) #25: #s(x) -> #h(0(),x) #26: #f(g(x)) -> #g(g(f(x))) #27: #f(g(x)) -> #g(f(x)) #28: #f(g(x)) -> #f(x) #29: #h(f(x),g(x)) -> #f(s(x)) #30: #h(f(x),g(x)) -> #s(x) #31: #s(0()) -> #p(0()) #32: #s(x) -> #h(x,0()) #33: #s(s(s(s(s(0()))))) -> #p(s(s(0()))) Number of SCCs: 1, DPs: 13, edges: 44 SCC { #3 #5..8 #15..18 #26..29 } Removing DPs: Order(PosReal,>,Sum)... Order(PosReal,>,Max)... QLPOpS... Order(PosReal,>,MaxSum)... QWPOpS(PosReal,>,MaxSum)... Order(PosReal,>,Sum-Sum; PosReal,≥,Sum-Sum)... succeeded. h(x1,x2) weight: x1_1; x1_2 a() weight: (/ 1 4); (/ 1 4) s(x1) weight: x1_1; x1_2 r(x1) weight: 0; 0 k(x1) weight: 0; 0 #p(x1) weight: 0; 0 f(x1) weight: x1_1 + x1_2; x1_1 + x1_2 p(x1) weight: 0; 0 0() weight: 0; 0 #h(x1,x2) weight: x1_2; x1_1 #s(x1) weight: 0; 0 #f(x1) weight: x1_1 + x1_2; x1_1 + x1_2 #g(x1) weight: x1_2; x1_1 #r(x1) weight: 0; 0 #a() weight: 0; 0 g(x1) weight: (/ 1 4) + x1_1; (/ 1 4) + x1_2 Usable rules: { 1..24 26 } Removed DPs: #26..28 Number of SCCs: 1, DPs: 10, edges: 24 SCC { #3 #5..8 #15..18 #29 } Removing DPs: Order(PosReal,>,Sum)... Order(PosReal,>,Max)... QLPOpS... Order(PosReal,>,MaxSum)... QWPOpS(PosReal,>,MaxSum)... Order(PosReal,>,Sum-Sum; PosReal,≥,Sum-Sum)... succeeded. h(x1,x2) weight: x1_1; x1_2 a() weight: (/ 1 4); (/ 1 4) s(x1) weight: x1_1; x1_2 r(x1) weight: 0; 0 k(x1) weight: 0; 0 #p(x1) weight: 0; 0 f(x1) weight: x1_1 + x1_2; x1_1 + x1_2 p(x1) weight: 0; 0 0() weight: 0; 0 #h(x1,x2) weight: x2_2; 0 #s(x1) weight: 0; 0 #f(x1) weight: (/ 1 2) + x1_2; 0 #g(x1) weight: (/ 1 4) + x1_2; 0 #r(x1) weight: 0; 0 #a() weight: 0; 0 g(x1) weight: (/ 1 2) + x1_1; (/ 1 2) + x1_2 Usable rules: { 1..24 26 } Removed DPs: #5..8 #17 #18 Number of SCCs: 2, DPs: 4, edges: 6 SCC { #3 } Removing DPs: Order(PosReal,>,Sum)... Order(PosReal,>,Max)... QLPOpS... Order(PosReal,>,MaxSum)... QWPOpS(PosReal,>,MaxSum)... Order(PosReal,>,Sum-Sum; PosReal,≥,Sum-Sum)... Order(PosReal,>,Sum-Sum; NegReal,≥,Sum)... succeeded. h(x1,x2) weight: 0; 0 a() weight: 0; 0 s(x1) weight: max{0, (/ 1 4) + x1_1}; (- (/ 1 4)) r(x1) weight: 0; 0 k(x1) weight: 0; 0 #p(x1) weight: 0; 0 f(x1) weight: 0; 0 p(x1) weight: 0; 0 0() weight: 0; 0 #h(x1,x2) weight: 0; 0 #s(x1) weight: 0; 0 #f(x1) weight: 0; 0 #g(x1) weight: max{0, (/ 1 4) + x1_1}; 0 #r(x1) weight: 0; 0 #a() weight: 0; 0 g(x1) weight: 0; 0 Usable rules: { } Removed DPs: #3 Number of SCCs: 1, DPs: 3, edges: 5 SCC { #15 #16 #29 } Removing DPs: Order(PosReal,>,Sum)... Order(PosReal,>,Max)... QLPOpS... Order(PosReal,>,MaxSum)... QWPOpS(PosReal,>,MaxSum)... Order(PosReal,>,Sum-Sum; PosReal,≥,Sum-Sum)... Order(PosReal,>,Sum-Sum; NegReal,≥,Sum)... Order(PosReal,>,MaxSum-Sum; NegReal,≥,Sum)... failed. Removing edges: failed. Finding a loop... failed. MAYBE