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 when applying the reduction pair processor with usable rules to remove from the DP problem
  pairs:
  
  activate#(n__from(X)) -> activate#(X)
  activate#(n__s(X)) -> activate#(X)
  activate#(n__cons(X1, X2)) -> activate#(X1)
  rules:
  
  2ndsneg(0, Z) -> rnil
  2ndsneg(s(N), cons(X, n__cons(Y, Z))) -> rcons(negrecip(activate(Y)), 2ndspos(N, activate(Z)))
  2ndspos(0, Z) -> rnil
  2ndspos(s(N), cons(X, n__cons(Y, Z))) -> rcons(posrecip(activate(Y)), 2ndsneg(N, activate(Z)))
  activate(n__from(X)) -> from(activate(X))
  activate(n__s(X)) -> s(activate(X))
  activate(n__cons(X1, X2)) -> cons(activate(X1), X2)
  activate(X) -> X
  cons(X1, X2) -> n__cons(X1, X2)
  from(X) -> cons(X, n__from(n__s(X)))
  from(X) -> n__from(X)
  pi(X) -> 2ndspos(X, from(0))
  plus(0, Y) -> Y
  plus(s(X), Y) -> s(plus(X, Y))
  s(X) -> n__s(X)
  square(X) -> times(X, X)
  times(0, Y) -> 0
  times(s(X), Y) -> plus(Y, times(X, Y))
  
   the pairs 
  activate#(n__cons(X1, X2)) -> activate#(X1)
  
  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)]
  Argument Filter: 
  pi(activate#/1) = []
  pi(n__s/1) = 1
  pi(n__from/1) = 1
  pi(n__cons/2) = [1]
  
  RPO with the following precedence
  precedence(activate#[1]) = 0
  precedence(n__cons[2]) = 1
  
  precedence(_) = 0
  and the following status
  status(activate#[1]) = lex
  status(n__cons[2]) = lex
  
  status(_) = lex
  
  problem when orienting DPs
  cannot orient pair activate#(n__from(X)) -> activate#(X) weakly:
  [(activate#(n__from(X)),0),(n__from(X),0)] >=mu [(activate#(X),0),(X,0)] could not be ensured