ceta_eq: termination proof not accepted
1: error below switch to dependency pairs
1.1: error below the dependency graph processor
 1.1.1: error below the reduction pair processor
  1.1.1.1: error below the reduction pair processor
   1.1.1.1.1: error below the dependency graph processor
    1.1.1.1.1.1: error when applying the reduction pair processor with usable rules to remove from the DP problem
     pairs:
     
     activate#(n__first(X1, X2)) -> activate#(X1)
     activate#(n__first(X1, X2)) -> activate#(X2)
     rules:
     
     activate(n__terms(X)) -> terms(activate(X))
     activate(n__s(X)) -> s(activate(X))
     activate(n__first(X1, X2)) -> first(activate(X1), activate(X2))
     activate(X) -> X
     add(0, X) -> X
     add(s(X), Y) -> s(add(X, Y))
     dbl(0) -> 0
     dbl(s(X)) -> s(s(dbl(X)))
     first(0, X) -> nil
     first(s(X), cons(Y, Z)) -> cons(Y, n__first(X, activate(Z)))
     first(X1, X2) -> n__first(X1, X2)
     s(X) -> n__s(X)
     sqr(0) -> 0
     sqr(s(X)) -> s(add(sqr(X), dbl(X)))
     terms(N) -> cons(recip(sqr(N)), n__terms(n__s(N)))
     terms(X) -> n__terms(X)
     
      the pairs 
     activate#(n__first(X1, X2)) -> activate#(X1)
     activate#(n__first(X1, X2)) -> activate#(X2)
     
     could not apply the generic root reduction pair processor with the following
     SCNP-version with mu = MS and the level mapping defined by 
     pi(activate#) = [(epsilon,0),(1,0)]
     polynomial interpretration over naturals with negative constants
     Pol(activate#(x_1)) = 1
     Pol(n__first(x_1, x_2)) = 1 + x_2 + x_1
     problem when orienting DPs
     cannot orient pair activate#(n__first(X1, X2)) -> activate#(X1) strictly:
     [(activate#(n__first(X1, X2)),0),(n__first(X1, X2),0)] >mu [(activate#(X1),0),(X1,0)] could not be ensured