ceta_equiv: termination proof not accepted
1: error below switch to dependency pairs
1.1: error below the dependency graph processor
 1.1.4: 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(#) -> #
  and(x, true) -> x
  and(x, false) -> false
  bs(l(x)) -> true
  bs(n(x, y, z)) -> and(and(ge(x, max(y)), ge(min(z), x)), and(bs(y), bs(z)))
  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(#, 1(x)) -> false
  ge(#, 0(x)) -> ge(#, x)
  if(true, x, y) -> x
  if(false, x, y) -> y
  max(l(x)) -> x
  max(n(x, y, z)) -> max(z)
  min(l(x)) -> x
  min(n(x, y, z)) -> min(y)
  not(false) -> true
  not(true) -> false
  size(l(x)) -> 1(#)
  size(n(x, y, z)) -> +(+(size(x), size(y)), 1(#))
  val(l(x)) -> x
  val(n(x, y, z)) -> x
  wb(l(x)) -> true
  wb(n(x, y, z)) -> and(if(ge(size(y), size(z)), ge(1(#), -(size(y), size(z))), ge(1(#), -(size(z), size(y)))), and(wb(y), wb(z)))
  
   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