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