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:
    
    U41#(tt, M, N) -> U42#(isNat(activate(N)), activate(M), activate(N))
    U42#(tt, M, N) -> plus#(activate(N), activate(M))
    plus#(N, s(M)) -> U41#(isNat(M), M, N)
    rules:
    
    0 -> n__0
    U11(tt, V2) -> U12(isNat(activate(V2)))
    U12(tt) -> tt
    U21(tt) -> tt
    U31(tt, N) -> activate(N)
    U41(tt, M, N) -> U42(isNat(activate(N)), activate(M), activate(N))
    U42(tt, M, N) -> s(plus(activate(N), activate(M)))
    activate(n__0) -> 0
    activate(n__plus(X1, X2)) -> plus(X1, X2)
    activate(n__s(X)) -> s(X)
    activate(X) -> X
    isNat(n__0) -> tt
    isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2))
    isNat(n__s(V1)) -> U21(isNat(activate(V1)))
    plus(N, 0) -> U31(isNat(N), N)
    plus(N, s(M)) -> U41(isNat(M), M, N)
    plus(X1, X2) -> n__plus(X1, X2)
    s(X) -> n__s(X)
    
     the pairs 
    U41#(tt, M, N) -> U42#(isNat(activate(N)), activate(M), activate(N))
    U42#(tt, M, N) -> plus#(activate(N), activate(M))
    plus#(N, s(M)) -> U41#(isNat(M), 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,1)]
    pi(U41#) = [(epsilon,0),(1,15),(2,2),(3,0)]
    pi(U42#) = [(epsilon,0),(1,15),(2,1),(3,0)]
    Argument Filter: 
    pi(plus#/2) = 1
    pi(s/1) = [1]
    pi(U41#/3) = []
    pi(isNat/1) = []
    pi(tt/0) = []
    pi(U42#/3) = 2
    pi(activate/1) = 1
    pi(n__0/0) = []
    pi(n__plus/2) = [2,1]
    pi(U11/2) = 1
    pi(n__s/1) = [1]
    pi(U21/1) = []
    pi(0/0) = []
    pi(plus/2) = [2,1]
    pi(U31/2) = 2
    pi(U41/3) = [2,3,1]
    pi(U12/1) = 1
    pi(U42/3) = [2,3,1]
    
    RPO with the following precedence
    precedence(s[1]) = 2
    precedence(U41#[3]) = 0
    precedence(isNat[1]) = 1
    precedence(tt[0]) = 1
    precedence(n__0[0]) = 1
    precedence(n__plus[2]) = 3
    precedence(n__s[1]) = 2
    precedence(U21[1]) = 1
    precedence(0[0]) = 1
    precedence(plus[2]) = 3
    precedence(U41[3]) = 3
    precedence(U42[3]) = 3
    
    precedence(_) = 0
    and the following status
    status(s[1]) = lex
    status(U41#[3]) = lex
    status(isNat[1]) = lex
    status(tt[0]) = lex
    status(n__0[0]) = lex
    status(n__plus[2]) = lex
    status(n__s[1]) = lex
    status(U21[1]) = lex
    status(0[0]) = lex
    status(plus[2]) = lex
    status(U41[3]) = lex
    status(U42[3]) = lex
    
    status(_) = lex
    
    problem when orienting DPs
    cannot orient pair U41#(tt, M, N) -> U42#(isNat(activate(N)), activate(M), activate(N)) strictly:
    [(U41#(tt, M, N),0),(tt,15),(M,2),(N,0)] >mu [(U42#(isNat(activate(N)), activate(M), activate(N)),0),(isNat(activate(N)),15),(activate(M),1),(activate(N),0)] could not be ensured