Input TRS: 1: fib(N) -> sel(N,fib1(s(0()),s(0()))) 2: fib1(X,Y) -> cons(X,n__fib1(Y,n__add(X,Y))) 3: add(0(),X) -> X 4: add(s(X),Y) -> s(add(X,Y)) 5: sel(0(),cons(X,XS)) -> X 6: sel(s(N),cons(X,XS)) -> sel(N,activate(XS)) 7: fib1(X1,X2) -> n__fib1(X1,X2) 8: add(X1,X2) -> n__add(X1,X2) 9: activate(n__fib1(X1,X2)) -> fib1(activate(X1),activate(X2)) 10: activate(n__add(X1,X2)) -> add(activate(X1),activate(X2)) 11: activate(X) -> X Number of strict rules: 11 Direct Order(PosReal,>,Poly) ... failed. Freezing ... failed. Dependency Pairs: #1: #sel(s(N),cons(X,XS)) -> #sel(N,activate(XS)) #2: #sel(s(N),cons(X,XS)) -> #activate(XS) #3: #activate(n__fib1(X1,X2)) -> #fib1(activate(X1),activate(X2)) #4: #activate(n__fib1(X1,X2)) -> #activate(X1) #5: #activate(n__fib1(X1,X2)) -> #activate(X2) #6: #activate(n__add(X1,X2)) -> #add(activate(X1),activate(X2)) #7: #activate(n__add(X1,X2)) -> #activate(X1) #8: #activate(n__add(X1,X2)) -> #activate(X2) #9: #fib(N) -> #sel(N,fib1(s(0()),s(0()))) #10: #fib(N) -> #fib1(s(0()),s(0())) #11: #add(s(X),Y) -> #add(X,Y) Number of SCCs: 3, DPs: 6, edges: 18 SCC { #11 } Removing DPs: Order(PosReal,>,Sum)... succeeded. s(x1) weight: (/ 1 2) + x1 activate(x1) weight: 0 #activate(x1) weight: 0 n__add(x1,x2) weight: 0 #fib1(x1,x2) weight: 0 n__fib1(x1,x2) weight: 0 fib1(x1,x2) weight: 0 fib(x1) weight: 0 0() weight: 0 #sel(x1,x2) weight: 0 sel(x1,x2) weight: 0 cons(x1,x2) weight: 0 #add(x1,x2) weight: x1 add(x1,x2) weight: 0 #fib(x1) weight: 0 Usable rules: { } Removed DPs: #11 Number of SCCs: 2, DPs: 5, edges: 17 SCC { #1 } Removing DPs: Order(PosReal,>,Sum)... succeeded. s(x1) weight: (/ 1 4) + x1 activate(x1) weight: (/ 1 4) #activate(x1) weight: 0 n__add(x1,x2) weight: (/ 3 4) #fib1(x1,x2) weight: 0 n__fib1(x1,x2) weight: (/ 3 4) fib1(x1,x2) weight: (/ 1 2) fib(x1) weight: 0 0() weight: 0 #sel(x1,x2) weight: x1 sel(x1,x2) weight: 0 cons(x1,x2) weight: (/ 3 4) #add(x1,x2) weight: 0 add(x1,x2) weight: (/ 1 2) #fib(x1) weight: 0 Usable rules: { } Removed DPs: #1 Number of SCCs: 1, DPs: 4, edges: 16 SCC { #4 #5 #7 #8 } Removing DPs: Order(PosReal,>,Sum)... succeeded. s(x1) weight: (/ 1 4) + x1 activate(x1) weight: (/ 1 4) #activate(x1) weight: x1 n__add(x1,x2) weight: (/ 1 2) + x1 + x2 #fib1(x1,x2) weight: 0 n__fib1(x1,x2) weight: (/ 3 4) + x1 + x2 fib1(x1,x2) weight: (/ 1 2) fib(x1) weight: 0 0() weight: 0 #sel(x1,x2) weight: 0 sel(x1,x2) weight: 0 cons(x1,x2) weight: x2 #add(x1,x2) weight: 0 add(x1,x2) weight: (/ 1 4) + x2 #fib(x1) weight: 0 Usable rules: { } Removed DPs: #4 #5 #7 #8 Number of SCCs: 0, DPs: 0, edges: 0 YES