ceta_eq: termination proof not accepted
1: error below switch to dependency pairs
1.1: error below the dependency graph processor
 1.1.2: error below the reduction pair processor
  1.1.2.1: error below the reduction pair processor
   1.1.2.1.1: error below the reduction pair processor
    1.1.2.1.1.1: error below the reduction pair processor
     1.1.2.1.1.1.1: error when applying the reduction pair processor with usable rules to remove from the DP problem
      pairs:
      
      active#(cons1(X1, X2)) -> active#(X1)
      active#(cons1(X1, X2)) -> active#(X2)
      rules:
      
      2nd(mark(X)) -> mark(2nd(X))
      2nd(ok(X)) -> ok(2nd(X))
      active(2nd(cons1(X, cons(Y, Z)))) -> mark(Y)
      active(2nd(cons(X, X1))) -> mark(2nd(cons1(X, X1)))
      active(from(X)) -> mark(cons(X, from(s(X))))
      active(2nd(X)) -> 2nd(active(X))
      active(cons(X1, X2)) -> cons(active(X1), X2)
      active(from(X)) -> from(active(X))
      active(s(X)) -> s(active(X))
      active(cons1(X1, X2)) -> cons1(active(X1), X2)
      active(cons1(X1, X2)) -> cons1(X1, active(X2))
      cons(mark(X1), X2) -> mark(cons(X1, X2))
      cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))
      cons1(mark(X1), X2) -> mark(cons1(X1, X2))
      cons1(X1, mark(X2)) -> mark(cons1(X1, X2))
      cons1(ok(X1), ok(X2)) -> ok(cons1(X1, X2))
      from(mark(X)) -> mark(from(X))
      from(ok(X)) -> ok(from(X))
      proper(2nd(X)) -> 2nd(proper(X))
      proper(cons(X1, X2)) -> cons(proper(X1), proper(X2))
      proper(from(X)) -> from(proper(X))
      proper(s(X)) -> s(proper(X))
      proper(cons1(X1, X2)) -> cons1(proper(X1), proper(X2))
      s(mark(X)) -> mark(s(X))
      s(ok(X)) -> ok(s(X))
      top(mark(X)) -> top(proper(X))
      top(ok(X)) -> top(active(X))
      
       the pairs 
      active#(cons1(X1, X2)) -> active#(X1)
      active#(cons1(X1, X2)) -> active#(X2)
      
      could not apply the generic root reduction pair processor with the following
      SCNP-version with mu = MS and the level mapping defined by 
      pi(active#) = [(epsilon,0),(1,0)]
      polynomial interpretration over naturals with negative constants
      Pol(active#(x_1)) = 1
      Pol(cons1(x_1, x_2)) = 1 + x_2 + x_1
      problem when orienting DPs
      cannot orient pair active#(cons1(X1, X2)) -> active#(X1) strictly:
      [(active#(cons1(X1, X2)),0),(cons1(X1, X2),0)] >mu [(active#(X1),0),(X1,0)] could not be ensured