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:
  
  wb#(n(x, y, z)) -> wb#(y)
  wb#(n(x, y, z)) -> wb#(z)
  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 
  wb#(n(x, y, z)) -> wb#(y)
  wb#(n(x, y, z)) -> wb#(z)
  
  could not apply the generic root reduction pair processor with the following
  SCNP-version with mu = MS and the level mapping defined by 
  pi(wb#) = [(epsilon,0),(1,0)]
  polynomial interpretration over naturals with negative constants
  Pol(wb#(x_1)) = 1
  Pol(n(x_1, x_2, x_3)) = 1 + x_3 + x_2
  problem when orienting DPs
  cannot orient pair wb#(n(x, y, z)) -> wb#(y) strictly:
  [(wb#(n(x, y, z)),0),(n(x, y, z),0)] >mu [(wb#(y),0),(y,0)] could not be ensured