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 dependency graph processor
    1.1.1.1.1.1: error when applying the reduction pair processor with usable rules to remove from the DP problem
     pairs:
     
     reach#(x, y, edge(u, v, i), h) -> if_reach_1#(eq(x, u), x, y, edge(u, v, i), h)
     if_reach_1#(false, x, y, edge(u, v, i), h) -> reach#(x, y, i, edge(u, v, h))
     rules:
     
     eq(0, 0) -> true
     eq(0, s(x)) -> false
     eq(s(x), 0) -> false
     eq(s(x), s(y)) -> eq(x, y)
     if_reach_1(true, x, y, edge(u, v, i), h) -> if_reach_2(eq(y, v), x, y, edge(u, v, i), h)
     if_reach_1(false, x, y, edge(u, v, i), h) -> reach(x, y, i, edge(u, v, h))
     if_reach_2(true, x, y, edge(u, v, i), h) -> true
     if_reach_2(false, x, y, edge(u, v, i), h) -> or(reach(x, y, i, h), reach(v, y, union(i, h), empty))
     or(true, y) -> true
     or(false, y) -> y
     reach(x, y, empty, h) -> false
     reach(x, y, edge(u, v, i), h) -> if_reach_1(eq(x, u), x, y, edge(u, v, i), h)
     union(empty, h) -> h
     union(edge(x, y, i), h) -> edge(x, y, union(i, h))
     
      the pairs 
     reach#(x, y, edge(u, v, i), h) -> if_reach_1#(eq(x, u), x, y, edge(u, v, i), h)
     if_reach_1#(false, x, y, edge(u, v, i), h) -> reach#(x, y, i, edge(u, v, h))
     
     could not apply the generic root reduction pair processor with the following
     SCNP-version with mu = MS and the level mapping defined by 
     pi(if_reach_1#) = [(epsilon,0),(1,8),(2,0),(3,0),(4,0)]
     pi(reach#) = [(epsilon,0),(2,0),(3,10)]
     polynomial interpretration over naturals with negative constants
     Pol(if_reach_1#(x_1, x_2, x_3, x_4, x_5)) = x_1
     Pol(false) = 0
     Pol(edge(x_1, x_2, x_3)) = 1 + x_3 + x_2 + x_1
     Pol(reach#(x_1, x_2, x_3, x_4)) = x_1
     Pol(eq(x_1, x_2)) = 1 + x_2
     Pol(0) = 0
     Pol(true) = 1
     Pol(s(x_1)) = x_1
     problem when orienting DPs
     cannot orient pair reach#(x, y, edge(u, v, i), h) -> if_reach_1#(eq(x, u), x, y, edge(u, v, i), h) strictly:
     [(reach#(x, y, edge(u, v, i), h),0),(y,0),(edge(u, v, i),10)] >mu [(if_reach_1#(eq(x, u), x, y, edge(u, v, i), h),0),(eq(x, u),8),(x,0),(y,0),(edge(u, v, i),0)] could not be ensured