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:
       
       D#(+(x, y)) -> D#(x)
       D#(+(x, y)) -> D#(y)
       rules:
       
       D(t) -> 1
       D(constant) -> 0
       D(+(x, y)) -> +(D(x), D(y))
       D(*(x, y)) -> +(*(y, D(x)), *(x, D(y)))
       D(-(x, y)) -> -(D(x), D(y))
       D(minus(x)) -> minus(D(x))
       D(div(x, y)) -> -(div(D(x), y), div(*(x, D(y)), pow(y, 2)))
       D(ln(x)) -> div(D(x), x)
       D(pow(x, y)) -> +(*(*(y, pow(x, -(y, 1))), D(x)), *(*(pow(x, y), ln(x)), D(y)))
       
        the pairs 
       D#(+(x, y)) -> D#(x)
       D#(+(x, y)) -> D#(y)
       
       could not apply the generic root reduction pair processor with the following
       SCNP-version with mu = MS and the level mapping defined by 
       pi(D#) = [(epsilon,0),(1,0)]
       polynomial interpretration over naturals with negative constants
       Pol(D#(x_1)) = 1
       Pol(+(x_1, x_2)) = 1 + x_2 + x_1
       problem when orienting DPs
       cannot orient pair D#(+(x, y)) -> D#(x) strictly:
       [(D#(+(x, y)),0),(+(x, y),0)] >mu [(D#(x),0),(x,0)] could not be ensured