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 below the reduction pair processor
  1.1.1.1: error when applying the reduction pair processor with usable rules to remove from the DP problem
   pairs:
   
   top#(ok(X)) -> top#(active(X))
   rules:
   
   active(fst(0, Z)) -> mark(nil)
   active(fst(s(X), cons(Y, Z))) -> mark(cons(Y, fst(X, Z)))
   active(from(X)) -> mark(cons(X, from(s(X))))
   active(add(0, X)) -> mark(X)
   active(add(s(X), Y)) -> mark(s(add(X, Y)))
   active(len(nil)) -> mark(0)
   active(len(cons(X, Z))) -> mark(s(len(Z)))
   active(cons(X1, X2)) -> cons(active(X1), X2)
   active(fst(X1, X2)) -> fst(active(X1), X2)
   active(fst(X1, X2)) -> fst(X1, active(X2))
   active(from(X)) -> from(active(X))
   active(add(X1, X2)) -> add(active(X1), X2)
   active(add(X1, X2)) -> add(X1, active(X2))
   active(len(X)) -> len(active(X))
   add(mark(X1), X2) -> mark(add(X1, X2))
   add(X1, mark(X2)) -> mark(add(X1, X2))
   add(ok(X1), ok(X2)) -> ok(add(X1, X2))
   cons(mark(X1), X2) -> mark(cons(X1, X2))
   cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))
   from(mark(X)) -> mark(from(X))
   from(ok(X)) -> ok(from(X))
   fst(mark(X1), X2) -> mark(fst(X1, X2))
   fst(X1, mark(X2)) -> mark(fst(X1, X2))
   fst(ok(X1), ok(X2)) -> ok(fst(X1, X2))
   len(mark(X)) -> mark(len(X))
   len(ok(X)) -> ok(len(X))
   proper(0) -> ok(0)
   proper(s(X)) -> s(proper(X))
   proper(nil) -> ok(nil)
   proper(cons(X1, X2)) -> cons(proper(X1), proper(X2))
   proper(fst(X1, X2)) -> fst(proper(X1), proper(X2))
   proper(from(X)) -> from(proper(X))
   proper(add(X1, X2)) -> add(proper(X1), proper(X2))
   proper(len(X)) -> len(proper(X))
   s(ok(X)) -> ok(s(X))
   top(mark(X)) -> top(proper(X))
   top(ok(X)) -> top(active(X))
   
    the pairs 
   top#(ok(X)) -> top#(active(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(top#) = [(epsilon,0)]
   Argument Filter: 
   pi(top#/1) = [1]
   pi(ok/1) = [1]
   pi(active/1) = 1
   pi(fst/2) = [1,2]
   pi(0/0) = []
   pi(mark/1) = []
   pi(nil/0) = []
   pi(s/1) = []
   pi(cons/2) = [1]
   pi(from/1) = [1]
   pi(add/2) = [2,1]
   pi(len/1) = [1]
   
   RPO with the following precedence
   precedence(top#[1]) = 4
   precedence(ok[1]) = 4
   precedence(fst[2]) = 5
   precedence(0[0]) = 2
   precedence(mark[1]) = 0
   precedence(nil[0]) = 1
   precedence(s[1]) = 3
   precedence(cons[2]) = 5
   precedence(from[1]) = 4
   precedence(add[2]) = 6
   precedence(len[1]) = 4
   
   precedence(_) = 0
   and the following status
   status(top#[1]) = lex
   status(ok[1]) = mul
   status(fst[2]) = mul
   status(0[0]) = mul
   status(mark[1]) = mul
   status(nil[0]) = mul
   status(s[1]) = mul
   status(cons[2]) = mul
   status(from[1]) = mul
   status(add[2]) = lex
   status(len[1]) = mul
   
   status(_) = lex
   
   problem when orienting (usable) rules
   could not orient from(ok(X)) >= ok(from(X))
   pi( from(ok(X)) ) = from(ok(X))
   pi( ok(from(X)) ) = ok(from(X))
   could not orient from(ok(X)) >=RPO ok(from(X))