ceta_equiv: termination proof not accepted
1: error below switch to dependency pairs
1.1: error below the dependency graph processor
 1.1.6: 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) -> #
  *(0(x), y) -> 0(*(x, y))
  *(1(x), y) -> +(0(*(x, y)), y)
  *(*(x, y), z) -> *(x, *(y, z))
  *(x, +(y, z)) -> +(*(x, y), *(x, z))
  +(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(#) -> #
  app(nil, l) -> l
  app(cons(x, l1), l2) -> cons(x, app(l1, l2))
  eq(#, #) -> true
  eq(#, 1(y)) -> false
  eq(1(x), #) -> false
  eq(#, 0(y)) -> eq(#, y)
  eq(0(x), #) -> eq(x, #)
  eq(1(x), 1(y)) -> eq(x, y)
  eq(0(x), 1(y)) -> false
  eq(1(x), 0(y)) -> false
  eq(0(x), 0(y)) -> eq(x, y)
  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
  ifinter(true, x, l1, l2) -> cons(x, inter(l1, l2))
  ifinter(false, x, l1, l2) -> inter(l1, l2)
  inter(x, nil) -> nil
  inter(nil, x) -> nil
  inter(app(l1, l2), l3) -> app(inter(l1, l3), inter(l2, l3))
  inter(l1, app(l2, l3)) -> app(inter(l1, l2), inter(l1, l3))
  inter(cons(x, l1), l2) -> ifinter(mem(x, l2), x, l1, l2)
  inter(l1, cons(x, l2)) -> ifinter(mem(x, l1), x, l2, l1)
  log(x) -> -(log'(x), 1(#))
  log'(#) -> #
  log'(1(x)) -> +(log'(x), 1(#))
  log'(0(x)) -> if(ge(x, 1(#)), +(log'(x), 1(#)), #)
  mem(x, nil) -> false
  mem(x, cons(y, l)) -> if(eq(x, y), true, mem(x, l))
  not(true) -> false
  not(false) -> true
  prod(nil) -> 1(#)
  prod(cons(x, l)) -> *(x, prod(l))
  prod(app(l1, l2)) -> *(prod(l1), prod(l2))
  sum(nil) -> 0(#)
  sum(cons(x, l)) -> +(x, sum(l))
  sum(app(l1, l2)) -> +(sum(l1), sum(l2))
  
   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