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(X)
  activate(X) -> X
  from(X) -> cons(X, n__from(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))
  square(X) -> times(X, X)
  times(0, Y) -> 0
  times(s(X), Y) -> plus(Y, times(X, Y))
  
   the pairs 
  2ndspos#(s(N), cons2(X, cons(Y, Z))) -> 2ndsneg#(N, activate(Z))
  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 = MS and the level mapping defined by 
  pi(2ndspos#) = [(epsilon,0),(1,5)]
  pi(2ndsneg#) = [(epsilon,0),(1,2)]
  Argument Filter: 
  pi(2ndspos#/2) = []
  pi(s/1) = [1]
  pi(cons2/2) = [1]
  pi(cons/2) = 2
  pi(2ndsneg#/2) = []
  pi(activate/1) = []
  pi(n__from/1) = [1]
  pi(from/1) = [1]
  
  RPO with the following precedence
  precedence(2ndspos#[2]) = 3
  precedence(s[1]) = 3
  precedence(cons2[2]) = 0
  precedence(2ndsneg#[2]) = 3
  precedence(activate[1]) = 3
  precedence(n__from[1]) = 1
  precedence(from[1]) = 2
  
  precedence(_) = 0
  and the following status
  status(2ndspos#[2]) = lex
  status(s[1]) = lex
  status(cons2[2]) = lex
  status(2ndsneg#[2]) = lex
  status(activate[1]) = lex
  status(n__from[1]) = lex
  status(from[1]) = lex
  
  status(_) = lex
  
  problem when orienting DPs
  cannot orient pair 2ndspos#(s(N), cons(X, Z)) -> 2ndspos#(s(N), cons2(X, activate(Z))) weakly:
  [(2ndspos#(s(N), cons(X, Z)),0),(s(N),5)] >=mu [(2ndspos#(s(N), cons2(X, activate(Z))),0),(s(N),5)] could not be ensured