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 to remove from the DP problem
  pairs:
  
  a__hd#(cons(X, Y)) -> mark#(X)
  a__tl#(cons(X, Y)) -> mark#(Y)
  mark#(adx(X)) -> mark#(X)
  mark#(incr(X)) -> mark#(X)
  mark#(hd(X)) -> a__hd#(mark(X))
  mark#(hd(X)) -> mark#(X)
  mark#(tl(X)) -> a__tl#(mark(X))
  mark#(tl(X)) -> mark#(X)
  rules:
  
  a__adx(cons(X, Y)) -> a__incr(cons(X, adx(Y)))
  a__adx(X) -> adx(X)
  a__hd(cons(X, Y)) -> mark(X)
  a__hd(X) -> hd(X)
  a__incr(cons(X, Y)) -> cons(s(X), incr(Y))
  a__incr(X) -> incr(X)
  a__nats -> a__adx(a__zeros)
  a__nats -> nats
  a__tl(cons(X, Y)) -> mark(Y)
  a__tl(X) -> tl(X)
  a__zeros -> cons(0, zeros)
  a__zeros -> zeros
  mark(nats) -> a__nats
  mark(adx(X)) -> a__adx(mark(X))
  mark(zeros) -> a__zeros
  mark(incr(X)) -> a__incr(mark(X))
  mark(hd(X)) -> a__hd(mark(X))
  mark(tl(X)) -> a__tl(mark(X))
  mark(cons(X1, X2)) -> cons(X1, X2)
  mark(0) -> 0
  mark(s(X)) -> s(X)
  
   the pairs 
  a__hd#(cons(X, Y)) -> mark#(X)
  a__tl#(cons(X, Y)) -> mark#(Y)
  mark#(adx(X)) -> mark#(X)
  mark#(hd(X)) -> mark#(X)
  mark#(tl(X)) -> mark#(X)
  
  could not apply the generic root reduction pair processor with the following
  SCNP-version with mu = MAX and the level mapping defined by 
  pi(mark#) = [(epsilon,0),(1,0)]
  pi(a__hd#) = [(epsilon,0)]
  pi(a__tl#) = [(epsilon,0)]
  Argument Filter: 
  pi(mark#/1) = []
  pi(adx/1) = [1]
  pi(incr/1) = 1
  pi(hd/1) = [1]
  pi(a__hd#/1) = 1
  pi(mark/1) = [1]
  pi(cons/2) = [1,2]
  pi(tl/1) = [1]
  pi(a__tl#/1) = 1
  pi(nats/0) = []
  pi(a__nats/0) = []
  pi(a__adx/1) = [1]
  pi(zeros/0) = []
  pi(a__zeros/0) = []
  pi(a__incr/1) = 1
  pi(a__hd/1) = [1]
  pi(a__tl/1) = [1]
  pi(0/0) = []
  pi(s/1) = 1
  
  RPO with the following precedence
  precedence(mark#[1]) = 0
  precedence(adx[1]) = 0
  precedence(hd[1]) = 3
  precedence(mark[1]) = 3
  precedence(cons[2]) = 0
  precedence(tl[1]) = 3
  precedence(nats[0]) = 4
  precedence(a__nats[0]) = 4
  precedence(a__adx[1]) = 0
  precedence(zeros[0]) = 1
  precedence(a__zeros[0]) = 3
  precedence(a__hd[1]) = 3
  precedence(a__tl[1]) = 3
  precedence(0[0]) = 2
  
  precedence(_) = 0
  and the following status
  status(mark#[1]) = mul
  status(adx[1]) = mul
  status(hd[1]) = mul
  status(mark[1]) = mul
  status(cons[2]) = mul
  status(tl[1]) = mul
  status(nats[0]) = mul
  status(a__nats[0]) = mul
  status(a__adx[1]) = mul
  status(zeros[0]) = mul
  status(a__zeros[0]) = mul
  status(a__hd[1]) = mul
  status(a__tl[1]) = mul
  status(0[0]) = mul
  
  status(_) = lex
  
  problem when orienting (usable) rules
  could not orient mark(hd(X)) >= a__hd(mark(X))
  pi( mark(hd(X)) ) = mark(hd(X))
  pi( a__hd(mark(X)) ) = a__hd(mark(X))
  could not orient mark(hd(X)) >=RPO a__hd(mark(X))