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, n__cons(Y, Z))) -> 2ndsneg#(N, activate(Z))
  2ndsneg#(s(N), cons(X, n__cons(Y, Z))) -> 2ndspos#(N, activate(Z))
  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(X)
  activate(n__cons(X1, X2)) -> cons(X1, X2)
  activate(X) -> X
  cons(X1, X2) -> n__cons(X1, X2)
  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), cons(X, n__cons(Y, Z))) -> 2ndsneg#(N, activate(Z))
  2ndsneg#(s(N), cons(X, n__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#) = [(1,4),(2,1)]
  pi(2ndsneg#) = [(1,4),(2,6)]
  Argument Filter: 
  pi(2ndspos#/2) = [2]
  pi(s/1) = 1
  pi(cons/2) = [2]
  pi(n__cons/2) = [2]
  pi(2ndsneg#/2) = [1]
  pi(activate/1) = [1]
  pi(n__from/1) = 1
  pi(from/1) = [1]
  
  RPO with the following precedence
  precedence(2ndspos#[2]) = 0
  precedence(cons[2]) = 1
  precedence(n__cons[2]) = 1
  precedence(2ndsneg#[2]) = 0
  precedence(activate[1]) = 1
  precedence(from[1]) = 1
  
  precedence(_) = 0
  and the following status
  status(2ndspos#[2]) = lex
  status(cons[2]) = lex
  status(n__cons[2]) = lex
  status(2ndsneg#[2]) = lex
  status(activate[1]) = lex
  status(from[1]) = lex
  
  status(_) = lex
  
  problem when orienting DPs
  cannot orient pair 2ndspos#(s(N), cons(X, n__cons(Y, Z))) -> 2ndsneg#(N, activate(Z)) strictly:
  [(s(N),4),(cons(X, n__cons(Y, Z)),1)] >mu [(N,4),(activate(Z),6)] could not be ensured