ceta_eq: termination proof not accepted
1: error below switch to dependency pairs
1.1: error below the dependency graph processor
 1.1.2: error below the reduction pair processor
  1.1.2.1: error when applying the reduction pair processor with usable rules to remove from the DP problem
   pairs:
   
   activate#(n__fib1(X1, X2)) -> activate#(X1)
   activate#(n__fib1(X1, X2)) -> activate#(X2)
   rules:
   
   activate(n__fib1(X1, X2)) -> fib1(activate(X1), activate(X2))
   activate(n__add(X1, X2)) -> add(activate(X1), activate(X2))
   activate(X) -> X
   add(0, X) -> X
   add(s(X), Y) -> s(add(X, Y))
   add(X1, X2) -> n__add(X1, X2)
   fib(N) -> sel(N, fib1(s(0), s(0)))
   fib1(X, Y) -> cons(X, n__fib1(Y, n__add(X, Y)))
   fib1(X1, X2) -> n__fib1(X1, X2)
   sel(0, cons(X, XS)) -> X
   sel(s(N), cons(X, XS)) -> sel(N, activate(XS))
   
    the pairs 
   activate#(n__fib1(X1, X2)) -> activate#(X1)
   activate#(n__fib1(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__fib1(x_1, x_2)) = 1 + x_2 + x_1
   problem when orienting DPs
   cannot orient pair activate#(n__fib1(X1, X2)) -> activate#(X1) strictly:
   [(activate#(n__fib1(X1, X2)),0),(n__fib1(X1, X2),0)] >mu [(activate#(X1),0),(X1,0)] could not be ensured