Input TRS: 1: sel(s(X),cons(Y,Z)) -> sel(X,activate(Z)) 2: sel(0(),cons(X,Z)) -> X 3: first(0(),Z) -> nil() 4: first(s(X),cons(Y,Z)) -> cons(Y,n__first(X,activate(Z))) 5: from(X) -> cons(X,n__from(n__s(X))) 6: sel1(s(X),cons(Y,Z)) -> sel1(X,activate(Z)) 7: sel1(0(),cons(X,Z)) -> quote(X) 8: first1(0(),Z) -> nil1() 9: first1(s(X),cons(Y,Z)) -> cons1(quote(Y),first1(X,activate(Z))) 10: quote(n__0()) -> 01() 11: quote1(n__cons(X,Z)) -> cons1(quote(activate(X)),quote1(activate(Z))) 12: quote1(n__nil()) -> nil1() 13: quote(n__s(X)) -> s1(quote(activate(X))) 14: quote(n__sel(X,Z)) -> sel1(activate(X),activate(Z)) 15: quote1(n__first(X,Z)) -> first1(activate(X),activate(Z)) 16: unquote(01()) -> 0() 17: unquote(s1(X)) -> s(unquote(X)) 18: unquote1(nil1()) -> nil() 19: unquote1(cons1(X,Z)) -> fcons(unquote(X),unquote1(Z)) 20: fcons(X,Z) -> cons(X,Z) 21: first(X1,X2) -> n__first(X1,X2) 22: from(X) -> n__from(X) 23: s(X) -> n__s(X) 24: 0() -> n__0() 25: cons(X1,X2) -> n__cons(X1,X2) 26: nil() -> n__nil() 27: sel(X1,X2) -> n__sel(X1,X2) 28: activate(n__first(X1,X2)) -> first(activate(X1),activate(X2)) 29: activate(n__from(X)) -> from(activate(X)) 30: activate(n__s(X)) -> s(activate(X)) 31: activate(n__0()) -> 0() 32: activate(n__cons(X1,X2)) -> cons(activate(X1),X2) 33: activate(n__nil()) -> nil() 34: activate(n__sel(X1,X2)) -> sel(activate(X1),activate(X2)) 35: activate(X) -> X Number of strict rules: 35 Direct Order(PosReal,>,Poly) ... failed. Freezing ... failed. Dependency Pairs: #1: #activate(n__from(X)) -> #from(activate(X)) #2: #activate(n__from(X)) -> #activate(X) #3: #sel1(s(X),cons(Y,Z)) -> #sel1(X,activate(Z)) #4: #sel1(s(X),cons(Y,Z)) -> #activate(Z) #5: #quote(n__s(X)) -> #quote(activate(X)) #6: #quote(n__s(X)) -> #activate(X) #7: #first1(s(X),cons(Y,Z)) -> #quote(Y) #8: #first1(s(X),cons(Y,Z)) -> #first1(X,activate(Z)) #9: #first1(s(X),cons(Y,Z)) -> #activate(Z) #10: #quote1(n__cons(X,Z)) -> #quote(activate(X)) #11: #quote1(n__cons(X,Z)) -> #activate(X) #12: #quote1(n__cons(X,Z)) -> #quote1(activate(Z)) #13: #quote1(n__cons(X,Z)) -> #activate(Z) #14: #activate(n__0()) -> #0() #15: #quote(n__sel(X,Z)) -> #sel1(activate(X),activate(Z)) #16: #quote(n__sel(X,Z)) -> #activate(X) #17: #quote(n__sel(X,Z)) -> #activate(Z) #18: #activate(n__s(X)) -> #s(activate(X)) #19: #activate(n__s(X)) -> #activate(X) #20: #fcons(X,Z) -> #cons(X,Z) #21: #sel1(0(),cons(X,Z)) -> #quote(X) #22: #activate(n__nil()) -> #nil() #23: #from(X) -> #cons(X,n__from(n__s(X))) #24: #activate(n__first(X1,X2)) -> #first(activate(X1),activate(X2)) #25: #activate(n__first(X1,X2)) -> #activate(X1) #26: #activate(n__first(X1,X2)) -> #activate(X2) #27: #activate(n__sel(X1,X2)) -> #sel(activate(X1),activate(X2)) #28: #activate(n__sel(X1,X2)) -> #activate(X1) #29: #activate(n__sel(X1,X2)) -> #activate(X2) #30: #unquote(s1(X)) -> #s(unquote(X)) #31: #unquote(s1(X)) -> #unquote(X) #32: #activate(n__cons(X1,X2)) -> #cons(activate(X1),X2) #33: #activate(n__cons(X1,X2)) -> #activate(X1) #34: #unquote1(cons1(X,Z)) -> #fcons(unquote(X),unquote1(Z)) #35: #unquote1(cons1(X,Z)) -> #unquote(X) #36: #unquote1(cons1(X,Z)) -> #unquote1(Z) #37: #unquote(01()) -> #0() #38: #first(0(),Z) -> #nil() #39: #sel(s(X),cons(Y,Z)) -> #sel(X,activate(Z)) #40: #sel(s(X),cons(Y,Z)) -> #activate(Z) #41: #quote1(n__first(X,Z)) -> #first1(activate(X),activate(Z)) #42: #quote1(n__first(X,Z)) -> #activate(X) #43: #quote1(n__first(X,Z)) -> #activate(Z) #44: #first(s(X),cons(Y,Z)) -> #cons(Y,n__first(X,activate(Z))) #45: #first(s(X),cons(Y,Z)) -> #activate(Z) #46: #unquote1(nil1()) -> #nil() Number of SCCs: 6, DPs: 20, edges: 98 SCC { #31 } Removing DPs: Order(PosReal,>,Sum)... succeeded. #0() weight: 0 01() weight: 0 #cons(x1,x2) weight: 0 s(x1) weight: 0 unquote1(x1) weight: 0 #quote1(x1) weight: 0 n__first(x1,x2) weight: 0 activate(x1) weight: 0 #unquote1(x1) weight: 0 n__from(x1) weight: 0 #activate(x1) weight: 0 #fcons(x1,x2) weight: 0 #first1(x1,x2) weight: 0 n__nil() weight: 0 n__s(x1) weight: 0 cons1(x1,x2) weight: 0 0() weight: 0 #sel(x1,x2) weight: 0 sel(x1,x2) weight: 0 from(x1) weight: 0 #s(x1) weight: 0 n__cons(x1,x2) weight: 0 #first(x1,x2) weight: 0 nil() weight: 0 #sel1(x1,x2) weight: 0 quote1(x1) weight: 0 n__sel(x1,x2) weight: 0 #nil() weight: 0 nil1() weight: 0 first(x1,x2) weight: 0 n__0() weight: 0 first1(x1,x2) weight: 0 #unquote(x1) weight: x1 #from(x1) weight: 0 quote(x1) weight: 0 cons(x1,x2) weight: 0 #quote(x1) weight: 0 sel1(x1,x2) weight: 0 s1(x1) weight: (/ 1 2) + x1 unquote(x1) weight: 0 fcons(x1,x2) weight: 0 Usable rules: { } Removed DPs: #31 Number of SCCs: 5, DPs: 19, edges: 97 SCC { #36 } Removing DPs: Order(PosReal,>,Sum)... succeeded. #0() weight: 0 01() weight: 0 #cons(x1,x2) weight: 0 s(x1) weight: 0 unquote1(x1) weight: 0 #quote1(x1) weight: 0 n__first(x1,x2) weight: 0 activate(x1) weight: 0 #unquote1(x1) weight: x1 n__from(x1) weight: 0 #activate(x1) weight: 0 #fcons(x1,x2) weight: 0 #first1(x1,x2) weight: 0 n__nil() weight: 0 n__s(x1) weight: 0 cons1(x1,x2) weight: (/ 1 2) + x2 0() weight: 0 #sel(x1,x2) weight: 0 sel(x1,x2) weight: 0 from(x1) weight: 0 #s(x1) weight: 0 n__cons(x1,x2) weight: 0 #first(x1,x2) weight: 0 nil() weight: 0 #sel1(x1,x2) weight: 0 quote1(x1) weight: 0 n__sel(x1,x2) weight: 0 #nil() weight: 0 nil1() weight: 0 first(x1,x2) weight: 0 n__0() weight: 0 first1(x1,x2) weight: 0 #unquote(x1) weight: 0 #from(x1) weight: 0 quote(x1) weight: 0 cons(x1,x2) weight: 0 #quote(x1) weight: 0 sel1(x1,x2) weight: 0 s1(x1) weight: (/ 1 2) unquote(x1) weight: 0 fcons(x1,x2) weight: 0 Usable rules: { } Removed DPs: #36 Number of SCCs: 4, DPs: 18, edges: 96 SCC { #12 } 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. #quote1(n__cons(X,n__from(X_{i10}))) -#12-> #quote1(activate(n__from(X_{i10}))) --->* #quote1(n__cons(activate(X_{i10}),n__from(n__s(activate(X_{i10}))))) Looping with: [ X := activate(X_{i10}); X_{i10} := n__s(activate(X_{i10})); ] NO