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 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 below the reduction pair processor
       1.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#(b(x, y)) -> D#(x)
        D#(b(x, y)) -> D#(y)
        rules:
        
        D(t) -> s(h)
        D(constant) -> h
        D(b(x, y)) -> b(D(x), D(y))
        D(c(x, y)) -> b(c(y, D(x)), c(x, D(y)))
        D(m(x, y)) -> m(D(x), D(y))
        D(opp(x)) -> opp(D(x))
        D(div(x, y)) -> m(div(D(x), y), div(c(x, D(y)), pow(y, 2)))
        D(ln(x)) -> div(D(x), x)
        D(pow(x, y)) -> b(c(c(y, pow(x, m(y, 1))), D(x)), c(c(pow(x, y), ln(x)), D(y)))
        b(h, x) -> x
        b(x, h) -> x
        b(s(x), s(y)) -> s(s(b(x, y)))
        b(b(x, y), z) -> b(x, b(y, z))
        
         the pairs 
        D#(b(x, y)) -> D#(x)
        D#(b(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(b(x_1, x_2)) = 1 + x_2 + x_1
        problem when orienting DPs
        cannot orient pair D#(b(x, y)) -> D#(x) strictly:
        [(D#(b(x, y)),0),(b(x, y),0)] >mu [(D#(x),0),(x,0)] could not be ensured