Input TRS: 1: active(f(X,g(X),Y)) -> mark(f(Y,Y,Y)) 2: active(g(b())) -> mark(c()) 3: active(b()) -> mark(c()) 4: mark(f(X1,X2,X3)) -> active(f(X1,X2,X3)) 5: mark(g(X)) -> active(g(mark(X))) 6: mark(b()) -> active(b()) 7: mark(c()) -> active(c()) 8: f(mark(X1),X2,X3) -> f(X1,X2,X3) 9: f(X1,mark(X2),X3) -> f(X1,X2,X3) 10: f(X1,X2,mark(X3)) -> f(X1,X2,X3) 11: f(active(X1),X2,X3) -> f(X1,X2,X3) 12: f(X1,active(X2),X3) -> f(X1,X2,X3) 13: f(X1,X2,active(X3)) -> f(X1,X2,X3) 14: g(mark(X)) -> g(X) 15: g(active(X)) -> g(X) Number of strict rules: 15 Direct Order(PosReal,>,Poly) ... failed. Freezing ... failed. Dependency Pairs: #1: #active(g(b())) -> #mark(c()) #2: #mark(b()) -> #active(b()) #3: #f(X1,X2,active(X3)) -> #f(X1,X2,X3) #4: #f(X1,mark(X2),X3) -> #f(X1,X2,X3) #5: #f(active(X1),X2,X3) -> #f(X1,X2,X3) #6: #f(X1,active(X2),X3) -> #f(X1,X2,X3) #7: #g(mark(X)) -> #g(X) #8: #mark(c()) -> #active(c()) #9: #f(X1,X2,mark(X3)) -> #f(X1,X2,X3) #10: #mark(g(X)) -> #active(g(mark(X))) #11: #mark(g(X)) -> #g(mark(X)) #12: #mark(g(X)) -> #mark(X) #13: #active(b()) -> #mark(c()) #14: #active(f(X,g(X),Y)) -> #mark(f(Y,Y,Y)) #15: #active(f(X,g(X),Y)) -> #f(Y,Y,Y) #16: #f(mark(X1),X2,X3) -> #f(X1,X2,X3) #17: #g(active(X)) -> #g(X) #18: #mark(f(X1,X2,X3)) -> #active(f(X1,X2,X3)) Number of SCCs: 4, DPs: 11, edges: 43 SCC { #12 } Removing DPs: Order(PosReal,>,Sum)... succeeded. b() weight: 0 c() weight: 0 f(x1,x2,x3) weight: 0 #mark(x1) weight: x1 mark(x1) weight: 0 #f(x1,x2,x3) weight: 0 #g(x1) weight: 0 active(x1) weight: 0 #active(x1) weight: 0 g(x1) weight: (/ 1 2) + x1 Usable rules: { } Removed DPs: #12 Number of SCCs: 3, DPs: 10, edges: 42 SCC { #7 #17 } Removing DPs: Order(PosReal,>,Sum)... succeeded. b() weight: 0 c() weight: 0 f(x1,x2,x3) weight: 0 #mark(x1) weight: 0 mark(x1) weight: (/ 1 2) + x1 #f(x1,x2,x3) weight: 0 #g(x1) weight: x1 active(x1) weight: (/ 1 2) + x1 #active(x1) weight: 0 g(x1) weight: (/ 1 2) Usable rules: { } Removed DPs: #7 #17 Number of SCCs: 2, DPs: 8, edges: 38 SCC { #14 #18 } 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...