ceta_eq: termination proof not accepted
1: error below switch to dependency pairs
1.1: error below the reduction pair processor
 1.1.1: error below the reduction pair processor
  1.1.1.1: error below the reduction pair processor
   1.1.1.1.1: error below the reduction pair processor
    1.1.1.1.1.1: error below the reduction pair processor
     1.1.1.1.1.1.1: error below the reduction pair processor
      1.1.1.1.1.1.1.1: error when applying the reduction pair processor with usable rules to remove from the DP problem
       pairs:
       
       dx#(plus(ALPHA, BETA)) -> dx#(ALPHA)
       dx#(plus(ALPHA, BETA)) -> dx#(BETA)
       rules:
       
       dx(X) -> one
       dx(a) -> zero
       dx(plus(ALPHA, BETA)) -> plus(dx(ALPHA), dx(BETA))
       dx(times(ALPHA, BETA)) -> plus(times(BETA, dx(ALPHA)), times(ALPHA, dx(BETA)))
       dx(minus(ALPHA, BETA)) -> minus(dx(ALPHA), dx(BETA))
       dx(neg(ALPHA)) -> neg(dx(ALPHA))
       dx(div(ALPHA, BETA)) -> minus(div(dx(ALPHA), BETA), times(ALPHA, div(dx(BETA), exp(BETA, two))))
       dx(ln(ALPHA)) -> div(dx(ALPHA), ALPHA)
       dx(exp(ALPHA, BETA)) -> plus(times(BETA, times(exp(ALPHA, minus(BETA, one)), dx(ALPHA))), times(exp(ALPHA, BETA), times(ln(ALPHA), dx(BETA))))
       
        the pairs 
       dx#(plus(ALPHA, BETA)) -> dx#(ALPHA)
       dx#(plus(ALPHA, BETA)) -> dx#(BETA)
       
       could not apply the generic root reduction pair processor with the following
       SCNP-version with mu = MS and the level mapping defined by 
       pi(dx#) = [(epsilon,0),(1,0)]
       polynomial interpretration over naturals with negative constants
       Pol(dx#(x_1)) = 1
       Pol(plus(x_1, x_2)) = 1 + x_2 + x_1
       problem when orienting DPs
       cannot orient pair dx#(plus(ALPHA, BETA)) -> dx#(ALPHA) strictly:
       [(dx#(plus(ALPHA, BETA)),0),(plus(ALPHA, BETA),0)] >mu [(dx#(ALPHA),0),(ALPHA,0)] could not be ensured