ceta_eq: termination proof not accepted
1: error below switch to dependency pairs
1.1: error below the reduction pair processor
 1.1.1: error below the dependency graph processor
  1.1.1.3: error when applying the reduction pair processor to remove from the DP problem
   pairs:
   
   a__add#(s(X), Y) -> a__add#(mark(X), mark(Y))
   rules:
   
   a__add(0, X) -> mark(X)
   a__add(s(X), Y) -> s(a__add(mark(X), mark(Y)))
   a__add(X1, X2) -> add(X1, X2)
   a__dbl(0) -> 0
   a__dbl(s(X)) -> s(s(a__dbl(mark(X))))
   a__dbl(X) -> dbl(X)
   a__first(0, X) -> nil
   a__first(s(X), cons(Y, Z)) -> cons(mark(Y), first(X, Z))
   a__first(X1, X2) -> first(X1, X2)
   a__half(0) -> 0
   a__half(s(0)) -> 0
   a__half(s(s(X))) -> s(a__half(mark(X)))
   a__half(dbl(X)) -> mark(X)
   a__half(X) -> half(X)
   a__sqr(0) -> 0
   a__sqr(s(X)) -> s(a__add(a__sqr(mark(X)), a__dbl(mark(X))))
   a__sqr(X) -> sqr(X)
   a__terms(N) -> cons(recip(a__sqr(mark(N))), terms(s(N)))
   a__terms(X) -> terms(X)
   mark(terms(X)) -> a__terms(mark(X))
   mark(sqr(X)) -> a__sqr(mark(X))
   mark(add(X1, X2)) -> a__add(mark(X1), mark(X2))
   mark(dbl(X)) -> a__dbl(mark(X))
   mark(first(X1, X2)) -> a__first(mark(X1), mark(X2))
   mark(half(X)) -> a__half(mark(X))
   mark(cons(X1, X2)) -> cons(mark(X1), X2)
   mark(recip(X)) -> recip(mark(X))
   mark(s(X)) -> s(mark(X))
   mark(0) -> 0
   mark(nil) -> nil
   
    the pairs 
   a__add#(s(X), Y) -> a__add#(mark(X), mark(Y))
   
   could not apply the generic root reduction pair processor with the following
   SCNP-version with mu = MS and the level mapping defined by 
   pi(a__add#) = [(epsilon,0),(1,3),(2,0)]
   Argument Filter: 
   pi(a__add#/2) = 2
   pi(s/1) = [1]
   pi(mark/1) = 1
   pi(terms/1) = []
   pi(a__terms/1) = []
   pi(sqr/1) = [1]
   pi(a__sqr/1) = [1]
   pi(add/2) = [2,1]
   pi(a__add/2) = [2,1]
   pi(0/0) = []
   pi(half/1) = 1
   pi(a__half/1) = 1
   pi(dbl/1) = [1]
   pi(a__dbl/1) = [1]
   pi(first/2) = [2,1]
   pi(a__first/2) = [2,1]
   pi(cons/2) = 2
   pi(recip/1) = 1
   pi(nil/0) = []
   
   RPO with the following precedence
   precedence(s[1]) = 0
   precedence(terms[1]) = 1
   precedence(a__terms[1]) = 1
   precedence(sqr[1]) = 5
   precedence(a__sqr[1]) = 5
   precedence(add[2]) = 2
   precedence(a__add[2]) = 2
   precedence(0[0]) = 3
   precedence(dbl[1]) = 4
   precedence(a__dbl[1]) = 4
   precedence(first[2]) = 7
   precedence(a__first[2]) = 7
   precedence(nil[0]) = 6
   
   precedence(_) = 0
   and the following status
   status(s[1]) = lex
   status(terms[1]) = lex
   status(a__terms[1]) = lex
   status(sqr[1]) = lex
   status(a__sqr[1]) = lex
   status(add[2]) = lex
   status(a__add[2]) = lex
   status(0[0]) = lex
   status(dbl[1]) = lex
   status(a__dbl[1]) = lex
   status(first[2]) = lex
   status(a__first[2]) = lex
   status(nil[0]) = lex
   
   status(_) = lex
   
   problem when orienting DPs
   cannot orient pair a__add#(s(X), Y) -> a__add#(mark(X), mark(Y)) strictly:
   [(a__add#(s(X), Y),0),(s(X),3),(Y,0)] >mu [(a__add#(mark(X), mark(Y)),0),(mark(X),3),(mark(Y),0)] could not be ensured