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