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