ceta_eq: termination proof not accepted
1: error below switch to dependency pairs
1.1: error below the dependency graph processor
 1.1.2: error below the reduction pair processor
  1.1.2.1: error below the dependency graph processor
   1.1.2.1.1: error when applying the reduction pair processor with usable rules to remove from the DP problem
    pairs:
    
    +#(O(x), O(y)) -> +#(x, y)
    +#(I(x), O(y)) -> +#(x, y)
    rules:
    
    *(0, x) -> 0
    *(x, 0) -> 0
    *(O(x), y) -> O(*(x, y))
    *(I(x), y) -> +(O(*(x, y)), y)
    +(0, x) -> x
    +(x, 0) -> x
    +(O(x), O(y)) -> O(+(x, y))
    +(O(x), I(y)) -> I(+(x, y))
    +(I(x), O(y)) -> I(+(x, y))
    +(I(x), I(y)) -> O(+(+(x, y), I(0)))
    O(0) -> 0
    
     the pairs 
    +#(I(x), O(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(I(x_1)) = 1 + x_1
    Pol(O(x_1)) = x_1
    problem when orienting DPs
    cannot orient pair +#(O(x), O(y)) -> +#(x, y) weakly:
    [(+#(O(x), O(y)),0),(O(x),2)] >=mu [(+#(x, y),0),(x,2)] could not be ensured