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:
  
  U11#(tt, N, X, XS) -> splitAt#(activate(N), activate(XS))
  splitAt#(s(N), cons(X, XS)) -> U11#(tt, N, X, activate(XS))
  rules:
  
  U11(tt, N, X, XS) -> U12(splitAt(activate(N), activate(XS)), activate(X))
  U12(pair(YS, ZS), X) -> pair(cons(activate(X), YS), ZS)
  activate(n__natsFrom(X)) -> natsFrom(X)
  activate(X) -> X
  afterNth(N, XS) -> snd(splitAt(N, XS))
  and(tt, X) -> activate(X)
  fst(pair(X, Y)) -> X
  head(cons(N, XS)) -> N
  natsFrom(N) -> cons(N, n__natsFrom(s(N)))
  natsFrom(X) -> n__natsFrom(X)
  sel(N, XS) -> head(afterNth(N, XS))
  snd(pair(X, Y)) -> Y
  splitAt(0, XS) -> pair(nil, XS)
  splitAt(s(N), cons(X, XS)) -> U11(tt, N, X, activate(XS))
  tail(cons(N, XS)) -> activate(XS)
  take(N, XS) -> fst(splitAt(N, XS))
  
   the pairs 
  U11#(tt, N, X, XS) -> splitAt#(activate(N), activate(XS))
  splitAt#(s(N), cons(X, XS)) -> U11#(tt, N, X, activate(XS))
  
  could not apply the generic root reduction pair processor with the following
  SCNP-version with mu = MS and the level mapping defined by 
  pi(U11#) = [(2,4),(4,0)]
  pi(splitAt#) = [(epsilon,0),(1,0),(2,0)]
  Argument Filter: 
  pi(U11#/4) = [1,2]
  pi(tt/0) = []
  pi(splitAt#/2) = []
  pi(activate/1) = 1
  pi(s/1) = [1]
  pi(cons/2) = 2
  pi(n__natsFrom/1) = []
  pi(natsFrom/1) = []
  
  RPO with the following precedence
  precedence(U11#[4]) = 1
  precedence(tt[0]) = 0
  precedence(splitAt#[2]) = 0
  precedence(s[1]) = 1
  precedence(n__natsFrom[1]) = 2
  precedence(natsFrom[1]) = 2
  
  precedence(_) = 0
  and the following status
  status(U11#[4]) = mul
  status(tt[0]) = mul
  status(splitAt#[2]) = mul
  status(s[1]) = mul
  status(n__natsFrom[1]) = mul
  status(natsFrom[1]) = mul
  
  status(_) = lex
  
  problem when orienting DPs
  cannot orient pair U11#(tt, N, X, XS) -> splitAt#(activate(N), activate(XS)) strictly:
  [(N,4),(XS,0)] >mu [(splitAt#(activate(N), activate(XS)),0),(activate(N),0),(activate(XS),0)] could not be ensured