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 reduction pair processor
   1.1.2.1.1: error when applying the reduction pair processor with usable rules to remove from the DP problem
    pairs:
    
    zWquot#(cons(X, XS), cons(Y, YS)) -> activate#(XS)
    zWquot#(cons(X, XS), cons(Y, YS)) -> activate#(YS)
    activate#(n__zWquot(X1, X2)) -> zWquot#(activate(X1), activate(X2))
    activate#(n__zWquot(X1, X2)) -> activate#(X1)
    activate#(n__zWquot(X1, X2)) -> activate#(X2)
    rules:
    
    activate(n__from(X)) -> from(activate(X))
    activate(n__s(X)) -> s(activate(X))
    activate(n__zWquot(X1, X2)) -> zWquot(activate(X1), activate(X2))
    activate(X) -> X
    from(X) -> cons(X, n__from(n__s(X)))
    from(X) -> n__from(X)
    minus(X, 0) -> 0
    minus(s(X), s(Y)) -> minus(X, Y)
    quot(0, s(Y)) -> 0
    quot(s(X), s(Y)) -> s(quot(minus(X, Y), s(Y)))
    s(X) -> n__s(X)
    sel(0, cons(X, XS)) -> X
    sel(s(N), cons(X, XS)) -> sel(N, activate(XS))
    zWquot(XS, nil) -> nil
    zWquot(nil, XS) -> nil
    zWquot(cons(X, XS), cons(Y, YS)) -> cons(quot(X, Y), n__zWquot(activate(XS), activate(YS)))
    zWquot(X1, X2) -> n__zWquot(X1, X2)
    
     the pairs 
    zWquot#(cons(X, XS), cons(Y, YS)) -> activate#(XS)
    zWquot#(cons(X, XS), cons(Y, YS)) -> activate#(YS)
    activate#(n__zWquot(X1, X2)) -> zWquot#(activate(X1), activate(X2))
    activate#(n__zWquot(X1, X2)) -> activate#(X1)
    activate#(n__zWquot(X1, X2)) -> activate#(X2)
    
    could not apply the generic root reduction pair processor with the following
    SCNP-version with mu = MS and the level mapping defined by 
    pi(zWquot#) = [(epsilon,0),(1,0),(2,0)]
    pi(activate#) = [(epsilon,0),(1,0)]
    polynomial interpretration over naturals with negative constants
    Pol(zWquot#(x_1, x_2)) = 1
    Pol(cons(x_1, x_2)) = x_2
    Pol(activate#(x_1)) = 1
    Pol(n__zWquot(x_1, x_2)) = 1 + x_2 + x_1
    Pol(activate(x_1)) = x_1
    Pol(n__from(x_1)) = 0
    Pol(from(x_1)) = 0
    Pol(n__s(x_1)) = x_1
    Pol(s(x_1)) = x_1
    Pol(zWquot(x_1, x_2)) = 1 + x_2 + x_1
    Pol(quot(x_1, x_2)) = x_1
    Pol(nil) = 0
    Pol(0) = 0
    Pol(minus(x_1, x_2)) = 1
    problem when orienting DPs
    cannot orient pair zWquot#(cons(X, XS), cons(Y, YS)) -> activate#(XS) strictly:
    [(zWquot#(cons(X, XS), cons(Y, YS)),0),(cons(X, XS),0),(cons(Y, YS),0)] >mu [(activate#(XS),0),(XS,0)] could not be ensured