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 when applying the reduction pair processor with usable rules to remove from the DP problem
  pairs:
  
  2ndspos#(s(N), cons(X, Z)) -> 2ndspos#(s(N), cons2(X, activate(Z)))
  2ndspos#(s(N), cons2(X, cons(Y, Z))) -> 2ndsneg#(N, activate(Z))
  2ndsneg#(s(N), cons(X, Z)) -> 2ndsneg#(s(N), cons2(X, activate(Z)))
  2ndsneg#(s(N), cons2(X, cons(Y, Z))) -> 2ndspos#(N, activate(Z))
  rules:
  
  2ndsneg(0, Z) -> rnil
  2ndsneg(s(N), cons(X, Z)) -> 2ndsneg(s(N), cons2(X, activate(Z)))
  2ndsneg(s(N), cons2(X, cons(Y, Z))) -> rcons(negrecip(Y), 2ndspos(N, activate(Z)))
  2ndspos(0, Z) -> rnil
  2ndspos(s(N), cons(X, Z)) -> 2ndspos(s(N), cons2(X, activate(Z)))
  2ndspos(s(N), cons2(X, cons(Y, Z))) -> rcons(posrecip(Y), 2ndsneg(N, activate(Z)))
  activate(n__from(X)) -> from(activate(X))
  activate(n__s(X)) -> s(activate(X))
  activate(X) -> X
  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 
  2ndsneg#(s(N), cons2(X, cons(Y, Z))) -> 2ndspos#(N, activate(Z))
  
  could not apply the generic root reduction pair processor with the following
  SCNP-version with mu = MAX and the level mapping defined by 
  pi(2ndspos#) = [(1,0)]
  pi(2ndsneg#) = [(epsilon,0)]
  Argument Filter: 
  pi(2ndspos#/2) = [1,2]
  pi(s/1) = [1]
  pi(cons2/2) = [2]
  pi(cons/2) = []
  pi(2ndsneg#/2) = [1]
  pi(activate/1) = [1]
  pi(n__from/1) = [1]
  pi(from/1) = [1]
  pi(n__s/1) = [1]
  
  RPO with the following precedence
  precedence(2ndspos#[2]) = 1
  precedence(s[1]) = 1
  precedence(cons2[2]) = 2
  precedence(cons[2]) = 1
  precedence(2ndsneg#[2]) = 1
  precedence(activate[1]) = 2
  precedence(n__from[1]) = 2
  precedence(from[1]) = 2
  precedence(n__s[1]) = 0
  
  precedence(_) = 0
  and the following status
  status(2ndspos#[2]) = mul
  status(s[1]) = mul
  status(cons2[2]) = mul
  status(cons[2]) = mul
  status(2ndsneg#[2]) = mul
  status(activate[1]) = mul
  status(n__from[1]) = mul
  status(from[1]) = mul
  status(n__s[1]) = mul
  
  status(_) = lex
  
  problem when orienting (usable) rules
  could not orient activate(n__from(X)) >= from(activate(X))
  pi( activate(n__from(X)) ) = activate(n__from(X))
  pi( from(activate(X)) ) = from(activate(X))
  could not orient activate(n__from(X)) >=RPO from(activate(X))