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:
   
   selsort#(cons(N, L)) -> ifselsort#(eq(N, min(cons(N, L))), cons(N, L))
   ifselsort#(false, cons(N, L)) -> selsort#(replace(min(cons(N, L)), N, L))
   rules:
   
   eq(0, 0) -> true
   eq(0, s(Y)) -> false
   eq(s(X), 0) -> false
   eq(s(X), s(Y)) -> eq(X, Y)
   ifmin(true, cons(N, cons(M, L))) -> min(cons(N, L))
   ifmin(false, cons(N, cons(M, L))) -> min(cons(M, L))
   ifrepl(true, N, M, cons(K, L)) -> cons(M, L)
   ifrepl(false, N, M, cons(K, L)) -> cons(K, replace(N, M, L))
   ifselsort(true, cons(N, L)) -> cons(N, selsort(L))
   ifselsort(false, cons(N, L)) -> cons(min(cons(N, L)), selsort(replace(min(cons(N, L)), N, L)))
   le(0, Y) -> true
   le(s(X), 0) -> false
   le(s(X), s(Y)) -> le(X, Y)
   min(cons(0, nil)) -> 0
   min(cons(s(N), nil)) -> s(N)
   min(cons(N, cons(M, L))) -> ifmin(le(N, M), cons(N, cons(M, L)))
   replace(N, M, nil) -> nil
   replace(N, M, cons(K, L)) -> ifrepl(eq(N, K), N, M, cons(K, L))
   selsort(nil) -> nil
   selsort(cons(N, L)) -> ifselsort(eq(N, min(cons(N, L))), cons(N, L))
   
    the pairs 
   selsort#(cons(N, L)) -> ifselsort#(eq(N, min(cons(N, L))), cons(N, L))
   ifselsort#(false, cons(N, L)) -> selsort#(replace(min(cons(N, L)), N, L))
   
   could not apply the generic root reduction pair processor with the following
   SCNP-version with mu = MS and the level mapping defined by 
   pi(selsort#) = [(epsilon,0),(1,2)]
   pi(ifselsort#) = [(1,0),(2,0)]
   Argument Filter: 
   pi(selsort#/1) = []
   pi(cons/2) = [2]
   pi(ifselsort#/2) = 1
   pi(eq/2) = []
   pi(min/1) = []
   pi(false/0) = []
   pi(replace/3) = 3
   pi(0/0) = []
   pi(nil/0) = []
   pi(s/1) = 1
   pi(ifmin/2) = [2]
   pi(le/2) = 2
   pi(true/0) = []
   pi(ifrepl/4) = 4
   
   RPO with the following precedence
   precedence(selsort#[1]) = 3
   precedence(cons[2]) = 2
   precedence(eq[2]) = 3
   precedence(min[1]) = 5
   precedence(false[0]) = 3
   precedence(0[0]) = 1
   precedence(nil[0]) = 0
   precedence(ifmin[2]) = 4
   precedence(true[0]) = 2
   
   precedence(_) = 0
   and the following status
   status(selsort#[1]) = lex
   status(cons[2]) = lex
   status(eq[2]) = lex
   status(min[1]) = lex
   status(false[0]) = lex
   status(0[0]) = lex
   status(nil[0]) = lex
   status(ifmin[2]) = lex
   status(true[0]) = lex
   
   status(_) = lex
   
   problem when orienting DPs
   cannot orient pair selsort#(cons(N, L)) -> ifselsort#(eq(N, min(cons(N, L))), cons(N, L)) strictly:
   [(selsort#(cons(N, L)),0),(cons(N, L),2)] >mu [(eq(N, min(cons(N, L))),0),(cons(N, L),0)] could not be ensured