ceta_eq: termination proof not accepted
1: error below switch to dependency pairs
1.1: error below the dependency graph processor
 1.1.4: error below the reduction pair processor
  1.1.4.1: error below the dependency graph processor
   1.1.4.1.1: error when applying the reduction pair processor with usable rules to remove from the DP problem
    pairs:
    
    +#(0(x), 0(y)) -> +#(x, y)
    +#(1(x), 0(y)) -> +#(x, y)
    rules:
    
    *(#, x) -> #
    *(0(x), y) -> 0(*(x, y))
    *(1(x), y) -> +(0(*(x, y)), y)
    +(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(#)))
    0(#) -> #
    prod(nil) -> 1(#)
    prod(cons(x, l)) -> *(x, prod(l))
    sum(nil) -> 0(#)
    sum(cons(x, l)) -> +(x, sum(l))
    
     the pairs 
    +#(1(x), 0(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,2)]
    polynomial interpretration over naturals with negative constants
    Pol(+#(x_1, x_2)) = x_2
    Pol(1(x_1)) = 1 + x_1
    Pol(0(x_1)) = x_1
    problem when orienting DPs
    cannot orient pair +#(0(x), 0(y)) -> +#(x, y) weakly:
    [(+#(0(x), 0(y)),0),(0(x),2)] >=mu [(+#(x, y),0),(x,2)] could not be ensured