Input TRS: 1: a__zeros() -> cons(0(),zeros()) 2: a__U11(tt(),L) -> a__U12(tt(),L) 3: a__U12(tt(),L) -> s(a__length(mark(L))) 4: a__U21(tt(),IL,M,N) -> a__U22(tt(),IL,M,N) 5: a__U22(tt(),IL,M,N) -> a__U23(tt(),IL,M,N) 6: a__U23(tt(),IL,M,N) -> cons(mark(N),take(M,IL)) 7: a__length(nil()) -> 0() 8: a__length(cons(N,L)) -> a__U11(tt(),L) 9: a__take(0(),IL) -> nil() 10: a__take(s(M),cons(N,IL)) -> a__U21(tt(),IL,M,N) 11: mark(zeros()) -> a__zeros() 12: mark(U11(X1,X2)) -> a__U11(mark(X1),X2) 13: mark(U12(X1,X2)) -> a__U12(mark(X1),X2) 14: mark(length(X)) -> a__length(mark(X)) 15: mark(U21(X1,X2,X3,X4)) -> a__U21(mark(X1),X2,X3,X4) 16: mark(U22(X1,X2,X3,X4)) -> a__U22(mark(X1),X2,X3,X4) 17: mark(U23(X1,X2,X3,X4)) -> a__U23(mark(X1),X2,X3,X4) 18: mark(take(X1,X2)) -> a__take(mark(X1),mark(X2)) 19: mark(cons(X1,X2)) -> cons(mark(X1),X2) 20: mark(0()) -> 0() 21: mark(tt()) -> tt() 22: mark(s(X)) -> s(mark(X)) 23: mark(nil()) -> nil() 24: a__zeros() -> zeros() 25: a__U11(X1,X2) -> U11(X1,X2) 26: a__U12(X1,X2) -> U12(X1,X2) 27: a__length(X) -> length(X) 28: a__U21(X1,X2,X3,X4) -> U21(X1,X2,X3,X4) 29: a__U22(X1,X2,X3,X4) -> U22(X1,X2,X3,X4) 30: a__U23(X1,X2,X3,X4) -> U23(X1,X2,X3,X4) 31: a__take(X1,X2) -> take(X1,X2) Number of strict rules: 31 Direct Order(PosReal,>,Poly) ... removes: 7 9 U21(x1,x2,x3,x4) weight: 14137 + x1 + x2 + x3 + x4 U11(x1,x2) weight: (/ 26931 2) + x1 + x2 s(x1) weight: x1 take(x1,x2) weight: 14137 + x1 + x2 U23(x1,x2,x3,x4) weight: 14137 + 2 * x1 + x2 + x3 + x4 a__U22(x1,x2,x3,x4) weight: 14137 + x1 + x2 + x3 + x4 zeros() weight: 0 U12(x1,x2) weight: (/ 26931 2) + x1 + x2 0() weight: 0 a__U21(x1,x2,x3,x4) weight: 14137 + x1 + x2 + x3 + x4 nil() weight: 0 mark(x1) weight: x1 a__U11(x1,x2) weight: (/ 26931 2) + x1 + x2 a__U12(x1,x2) weight: (/ 26931 2) + x1 + x2 cons(x1,x2) weight: x1 + x2 a__take(x1,x2) weight: 14137 + x1 + x2 tt() weight: 0 a__U23(x1,x2,x3,x4) weight: 14137 + 2 * x1 + x2 + x3 + x4 U22(x1,x2,x3,x4) weight: 14137 + x1 + x2 + x3 + x4 length(x1) weight: (/ 26931 2) + x1 a__zeros() weight: 0 a__length(x1) weight: (/ 26931 2) + x1 Number of strict rules: 29 Direct Order(PosReal,>,Poly) ... failed. Freezing ... failed. Dependency Pairs: #1: #a__U11(tt(),L) -> #a__U12(tt(),L) #2: #a__U23(tt(),IL,M,N) -> #mark(N) #3: #mark(U12(X1,X2)) -> #a__U12(mark(X1),X2) #4: #mark(U12(X1,X2)) -> #mark(X1) #5: #mark(zeros()) -> #a__zeros() #6: #mark(U11(X1,X2)) -> #a__U11(mark(X1),X2) #7: #mark(U11(X1,X2)) -> #mark(X1) #8: #mark(length(X)) -> #a__length(mark(X)) #9: #mark(length(X)) -> #mark(X) #10: #a__take(s(M),cons(N,IL)) -> #a__U21(tt(),IL,M,N) #11: #a__U22(tt(),IL,M,N) -> #a__U23(tt(),IL,M,N) #12: #mark(s(X)) -> #mark(X) #13: #mark(U23(X1,X2,X3,X4)) -> #a__U23(mark(X1),X2,X3,X4) #14: #mark(U23(X1,X2,X3,X4)) -> #mark(X1) #15: #mark(cons(X1,X2)) -> #mark(X1) #16: #mark(U22(X1,X2,X3,X4)) -> #a__U22(mark(X1),X2,X3,X4) #17: #mark(U22(X1,X2,X3,X4)) -> #mark(X1) #18: #a__U12(tt(),L) -> #a__length(mark(L)) #19: #a__U12(tt(),L) -> #mark(L) #20: #a__length(cons(N,L)) -> #a__U11(tt(),L) #21: #mark(U21(X1,X2,X3,X4)) -> #a__U21(mark(X1),X2,X3,X4) #22: #mark(U21(X1,X2,X3,X4)) -> #mark(X1) #23: #a__U21(tt(),IL,M,N) -> #a__U22(tt(),IL,M,N) #24: #mark(take(X1,X2)) -> #a__take(mark(X1),mark(X2)) #25: #mark(take(X1,X2)) -> #mark(X1) #26: #mark(take(X1,X2)) -> #mark(X2) Number of SCCs: 1, DPs: 25, edges: 219 SCC { #1..4 #6..26 } Removing DPs: Order(PosReal,>,Sum)... succeeded. U21(x1,x2,x3,x4) weight: (/ 5 8) + x1 + x2 + x3 + x4 U11(x1,x2) weight: (/ 1 4) + x1 + x2 s(x1) weight: x1 #a__U23(x1,x2,x3,x4) weight: (/ 1 8) + x4 take(x1,x2) weight: (/ 5 8) + x1 + x2 U23(x1,x2,x3,x4) weight: (/ 5 8) + x1 + x2 + x3 + x4 a__U22(x1,x2,x3,x4) weight: (/ 5 8) + x1 + x2 + x3 + x4 #a__U11(x1,x2) weight: (/ 1 8) + x2 zeros() weight: 0 #a__take(x1,x2) weight: (/ 1 2) + x2 U12(x1,x2) weight: (/ 1 4) + x1 + x2 #a__U12(x1,x2) weight: (/ 1 8) + x2 #a__U21(x1,x2,x3,x4) weight: (/ 3 8) + x4 #mark(x1) weight: x1 0() weight: 0 #a__zeros() weight: 0 a__U21(x1,x2,x3,x4) weight: (/ 5 8) + x1 + x2 + x3 + x4 nil() weight: 0 mark(x1) weight: x1 a__U11(x1,x2) weight: (/ 1 4) + x1 + x2 #a__length(x1) weight: (/ 1 8) + x1 a__U12(x1,x2) weight: (/ 1 4) + x1 + x2 #a__U22(x1,x2,x3,x4) weight: (/ 1 4) + x4 cons(x1,x2) weight: x1 + x2 a__take(x1,x2) weight: (/ 5 8) + x1 + x2 tt() weight: 0 a__U23(x1,x2,x3,x4) weight: (/ 5 8) + x1 + x2 + x3 + x4 U22(x1,x2,x3,x4) weight: (/ 5 8) + x1 + x2 + x3 + x4 length(x1) weight: (/ 1 4) + x1 a__zeros() weight: 0 a__length(x1) weight: (/ 1 4) + x1 Usable rules: { 1..6 8 10..31 } Removed DPs: #2..4 #6..11 #13 #14 #16 #17 #19 #21..26 Number of SCCs: 2, DPs: 5, edges: 7 SCC { #12 #15 } Removing DPs: Order(PosReal,>,Sum)... succeeded. U21(x1,x2,x3,x4) weight: (/ 3 8) + x1 + x2 + x4 U11(x1,x2) weight: (/ 3 8) + x1 + x2 s(x1) weight: (/ 3 8) + x1 #a__U23(x1,x2,x3,x4) weight: (/ 1 8) take(x1,x2) weight: (/ 5 8) + x1 U23(x1,x2,x3,x4) weight: (/ 7 8) + x1 + x2 + x3 a__U22(x1,x2,x3,x4) weight: (/ 5 8) #a__U11(x1,x2) weight: (/ 1 8) zeros() weight: 0 #a__take(x1,x2) weight: (/ 1 2) U12(x1,x2) weight: (/ 3 4) + x1 #a__U12(x1,x2) weight: (/ 1 8) #a__U21(x1,x2,x3,x4) weight: (/ 3 8) #mark(x1) weight: x1 0() weight: 0 #a__zeros() weight: 0 a__U21(x1,x2,x3,x4) weight: (/ 1 2) + x1 + x4 nil() weight: 0 mark(x1) weight: (/ 1 8) + x1 a__U11(x1,x2) weight: (/ 1 2) + x1 #a__length(x1) weight: (/ 1 8) a__U12(x1,x2) weight: (/ 5 8) + x1 + x2 #a__U22(x1,x2,x3,x4) weight: (/ 1 4) cons(x1,x2) weight: (/ 3 4) + x1 a__take(x1,x2) weight: x1 tt() weight: 0 a__U23(x1,x2,x3,x4) weight: (/ 3 4) U22(x1,x2,x3,x4) weight: (/ 3 8) + x1 + x2 + x3 + x4 length(x1) weight: (/ 1 8) a__zeros() weight: 0 a__length(x1) weight: (/ 3 8) Usable rules: { } Removed DPs: #12 #15 Number of SCCs: 1, DPs: 3, edges: 3 SCC { #1 #18 #20 } 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... found. #a__length(cons(N,zeros())) -#20-> #a__U11(tt(),zeros()) --->* #a__U11(tt(),zeros()) -#1-> #a__U12(tt(),zeros()) --->* #a__U12(tt(),zeros()) -#18-> #a__length(mark(zeros())) --->* #a__length(cons(0(),zeros())) Looping with: [ N := 0(); ] NO