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__fst#(s(X), cons(Y, Z)) -> mark#(Y)
  a__from#(X) -> mark#(X)
  a__add#(0, X) -> mark#(X)
  mark#(fst(X1, X2)) -> a__fst#(mark(X1), mark(X2))
  mark#(fst(X1, X2)) -> mark#(X1)
  mark#(fst(X1, X2)) -> mark#(X2)
  mark#(from(X)) -> a__from#(mark(X))
  mark#(from(X)) -> mark#(X)
  mark#(add(X1, X2)) -> a__add#(mark(X1), mark(X2))
  mark#(add(X1, X2)) -> mark#(X1)
  mark#(add(X1, X2)) -> mark#(X2)
  mark#(len(X)) -> mark#(X)
  mark#(cons(X1, X2)) -> mark#(X1)
  rules:
  
  a__add(0, X) -> mark(X)
  a__add(s(X), Y) -> s(add(X, Y))
  a__add(X1, X2) -> add(X1, X2)
  a__from(X) -> cons(mark(X), from(s(X)))
  a__from(X) -> from(X)
  a__fst(0, Z) -> nil
  a__fst(s(X), cons(Y, Z)) -> cons(mark(Y), fst(X, Z))
  a__fst(X1, X2) -> fst(X1, X2)
  a__len(nil) -> 0
  a__len(cons(X, Z)) -> s(len(Z))
  a__len(X) -> len(X)
  mark(fst(X1, X2)) -> a__fst(mark(X1), mark(X2))
  mark(from(X)) -> a__from(mark(X))
  mark(add(X1, X2)) -> a__add(mark(X1), mark(X2))
  mark(len(X)) -> a__len(mark(X))
  mark(0) -> 0
  mark(s(X)) -> s(X)
  mark(nil) -> nil
  mark(cons(X1, X2)) -> cons(mark(X1), X2)
  
   the pairs 
  mark#(fst(X1, X2)) -> a__fst#(mark(X1), mark(X2))
  mark#(fst(X1, X2)) -> mark#(X1)
  mark#(fst(X1, X2)) -> mark#(X2)
  mark#(from(X)) -> mark#(X)
  mark#(add(X1, X2)) -> a__add#(mark(X1), mark(X2))
  mark#(add(X1, X2)) -> mark#(X1)
  mark#(add(X1, X2)) -> mark#(X2)
  
  could not apply the generic reduction pair processor with the following
  Argument Filter: 
  pi(mark#/1) = 1
  pi(fst/2) = [1,2]
  pi(a__fst#/2) = 2
  pi(mark/1) = [1]
  pi(s/1) = []
  pi(cons/2) = 1
  pi(from/1) = [1]
  pi(a__from#/1) = 1
  pi(add/2) = [1,2]
  pi(a__add#/2) = 2
  pi(0/0) = []
  pi(len/1) = 1
  pi(a__fst/2) = [1,2]
  pi(a__from/1) = [1]
  pi(a__add/2) = [1,2]
  pi(a__len/1) = 1
  pi(nil/0) = []
  
  RPO with the following precedence
  precedence(fst[2]) = 1
  precedence(mark[1]) = 1
  precedence(s[1]) = 0
  precedence(from[1]) = 1
  precedence(add[2]) = 1
  precedence(0[0]) = 2
  precedence(a__fst[2]) = 1
  precedence(a__from[1]) = 1
  precedence(a__add[2]) = 1
  precedence(nil[0]) = 2
  
  precedence(_) = 0
  and the following status
  status(fst[2]) = mul
  status(mark[1]) = mul
  status(s[1]) = mul
  status(from[1]) = mul
  status(add[2]) = mul
  status(0[0]) = mul
  status(a__fst[2]) = mul
  status(a__from[1]) = mul
  status(a__add[2]) = mul
  status(nil[0]) = mul
  
  status(_) = lex
  
  problem when orienting (usable) rules
  could not orient mark(from(X)) >= a__from(mark(X))
  pi( mark(from(X)) ) = mark(from(X))
  pi( a__from(mark(X)) ) = a__from(mark(X))
  could not orient mark(from(X)) >=RPO a__from(mark(X))