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 below the reduction pair processor
  1.1.1.1: error below the dependency graph processor
   1.1.1.1.1: error when applying the reduction pair processor to remove from the DP problem
    pairs:
    
    U21#(tt, M, N) -> plus#(activate(N), activate(M))
    plus#(N, s(M)) -> U21#(and(isNat(M), n__isNat(N)), M, N)
    rules:
    
    0 -> n__0
    U11(tt, N) -> activate(N)
    U21(tt, M, N) -> s(plus(activate(N), activate(M)))
    U31(tt) -> 0
    U41(tt, M, N) -> plus(x(activate(N), activate(M)), activate(N))
    activate(n__0) -> 0
    activate(n__plus(X1, X2)) -> plus(X1, X2)
    activate(n__isNat(X)) -> isNat(X)
    activate(n__s(X)) -> s(X)
    activate(n__x(X1, X2)) -> x(X1, X2)
    activate(X) -> X
    and(tt, X) -> activate(X)
    isNat(n__0) -> tt
    isNat(n__plus(V1, V2)) -> and(isNat(activate(V1)), n__isNat(activate(V2)))
    isNat(n__s(V1)) -> isNat(activate(V1))
    isNat(n__x(V1, V2)) -> and(isNat(activate(V1)), n__isNat(activate(V2)))
    isNat(X) -> n__isNat(X)
    plus(N, 0) -> U11(isNat(N), N)
    plus(N, s(M)) -> U21(and(isNat(M), n__isNat(N)), M, N)
    plus(X1, X2) -> n__plus(X1, X2)
    s(X) -> n__s(X)
    x(N, 0) -> U31(isNat(N))
    x(N, s(M)) -> U41(and(isNat(M), n__isNat(N)), M, N)
    x(X1, X2) -> n__x(X1, X2)
    
     the pairs 
    U21#(tt, M, N) -> plus#(activate(N), activate(M))
    plus#(N, s(M)) -> U21#(and(isNat(M), n__isNat(N)), M, N)
    
    could not apply the generic root reduction pair processor with the following
    SCNP-version with mu = MS and the level mapping defined by 
    pi(plus#) = [(epsilon,0),(2,2)]
    pi(U21#) = [(epsilon,0),(2,3),(3,0)]
    Argument Filter: 
    pi(plus#/2) = 1
    pi(s/1) = [1]
    pi(U21#/3) = [1]
    pi(and/2) = 2
    pi(isNat/1) = []
    pi(n__isNat/1) = []
    pi(tt/0) = []
    pi(activate/1) = 1
    pi(n__0/0) = []
    pi(n__plus/2) = [1,2]
    pi(plus/2) = [1,2]
    pi(0/0) = []
    pi(U11/2) = [2]
    pi(n__x/2) = [1,2]
    pi(x/2) = [1,2]
    pi(U41/3) = [3,2,1]
    pi(n__s/1) = [1]
    pi(U21/3) = [3,2,1]
    pi(U31/1) = [1]
    
    RPO with the following precedence
    precedence(s[1]) = 0
    precedence(U21#[3]) = 0
    precedence(isNat[1]) = 0
    precedence(n__isNat[1]) = 0
    precedence(tt[0]) = 0
    precedence(n__0[0]) = 2
    precedence(n__plus[2]) = 1
    precedence(plus[2]) = 1
    precedence(0[0]) = 2
    precedence(U11[2]) = 1
    precedence(n__x[2]) = 3
    precedence(x[2]) = 3
    precedence(U41[3]) = 3
    precedence(n__s[1]) = 0
    precedence(U21[3]) = 1
    precedence(U31[1]) = 3
    
    precedence(_) = 0
    and the following status
    status(s[1]) = lex
    status(U21#[3]) = lex
    status(isNat[1]) = lex
    status(n__isNat[1]) = lex
    status(tt[0]) = lex
    status(n__0[0]) = lex
    status(n__plus[2]) = lex
    status(plus[2]) = lex
    status(0[0]) = lex
    status(U11[2]) = lex
    status(n__x[2]) = lex
    status(x[2]) = lex
    status(U41[3]) = lex
    status(n__s[1]) = lex
    status(U21[3]) = lex
    status(U31[1]) = lex
    
    status(_) = lex
    
    problem when orienting DPs
    cannot orient pair U21#(tt, M, N) -> plus#(activate(N), activate(M)) strictly:
    [(U21#(tt, M, N),0),(M,3),(N,0)] >mu [(plus#(activate(N), activate(M)),0),(activate(M),2)] could not be ensured