ceta_equiv: termination proof not accepted
1: error below switch to dependency pairs
1.1: error below the dependency graph processor
 1.1.2: error when applying the reduction pair processor with usable rules to remove from the DP problem
  pairs:
  
  f#(s(x), s(y)) -> f#(x, s(c(s(y))))
  rules:
  
  f(x, c(y)) -> f(x, s(f(y, y)))
  f(s(x), s(y)) -> f(x, s(c(s(y))))
  
   the pairs 
  f#(s(x), s(y)) -> f#(x, s(c(s(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(f#) = [(epsilon,0),(1,0),(2,0)]
  polynomial interpretration over naturals with negative constants
  Pol(f#(x_1, x_2)) = 1
  Pol(s(x_1)) = 1 + x_1
  Pol(c(x_1)) = 0
  problem when orienting DPs
  cannot orient pair f#(s(x), s(y)) -> f#(x, s(c(s(y)))) strictly:
  [(f#(s(x), s(y)),0),(s(x),0),(s(y),0)] >mu [(f#(x, s(c(s(y)))),0),(x,0),(s(c(s(y))),0)] could not be ensured