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 when applying the reduction pair processor with usable rules to remove from the DP problem
   pairs:
   
   div#(x, y) -> quot#(x, y, y)
   quot#(s(x), s(y), z) -> quot#(x, y, z)
   quot#(x, 0, s(z)) -> div#(x, s(z))
   rules:
   
   div(0, y) -> 0
   div(x, y) -> quot(x, y, y)
   div(div(x, y), z) -> div(x, times(y, z))
   divides(y, x) -> eq(x, times(div(x, y), y))
   eq(0, 0) -> true
   eq(s(x), 0) -> false
   eq(0, s(y)) -> false
   eq(s(x), s(y)) -> eq(x, y)
   if(true, x, y) -> false
   if(false, x, y) -> pr(x, y)
   plus(x, 0) -> x
   plus(0, y) -> y
   plus(s(x), y) -> s(plus(x, y))
   pr(x, s(0)) -> true
   pr(x, s(s(y))) -> if(divides(s(s(y)), x), x, s(y))
   prime(s(s(x))) -> pr(s(s(x)), s(x))
   quot(0, s(y), z) -> 0
   quot(s(x), s(y), z) -> quot(x, y, z)
   quot(x, 0, s(z)) -> s(div(x, s(z)))
   times(0, y) -> 0
   times(s(0), y) -> y
   times(s(x), y) -> plus(y, times(x, y))
   
    the pairs 
   quot#(s(x), s(y), z) -> quot#(x, y, z)
   
   could not apply the generic root reduction pair processor with the following
   SCNP-version with mu = MS and the level mapping defined by 
   pi(div#) = [(epsilon,0),(2,3)]
   pi(quot#) = [(epsilon,0),(3,3)]
   polynomial interpretration over naturals with negative constants
   Pol(div#(x_1, x_2)) = x_1
   Pol(quot#(x_1, x_2, x_3)) = x_1
   Pol(s(x_1)) = 1 + x_1
   Pol(0) = 0
   problem when orienting DPs
   cannot orient pair div#(x, y) -> quot#(x, y, y) weakly:
   [(div#(x, y),0),(y,3)] >=mu [(quot#(x, y, y),0),(y,3)] could not be ensured