Input TRS: 1: zeros() -> cons(0(),n__zeros()) 2: tail(cons(X,XS)) -> activate(XS) 3: zeros() -> n__zeros() 4: activate(n__zeros()) -> zeros() 5: activate(X) -> X Number of strict rules: 5 Direct Order(PosReal,>,Poly) ... removes: 4 5 2 activate(x1) weight: (/ 1 4) + x1 n__zeros() weight: 0 zeros() weight: 0 tail(x1) weight: (/ 1 2) + x1 0() weight: 0 cons(x1,x2) weight: x1 + x2 Number of strict rules: 2 Direct Order(PosReal,>,Poly) ... failed. Freezing ... failed. Dependency Pairs: Number of SCCs: 0, DPs: 0, edges: 0 YES