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.2: error when applying the reduction pair processor to remove from the DP problem
    pairs:
    
    isNatKind#(n__s(V1)) -> isNatKind#(activate(V1))
    rules:
    
    0 -> n__0
    U11(tt, V1, V2) -> U12(isNatKind(activate(V1)), activate(V1), activate(V2))
    U12(tt, V1, V2) -> U13(isNatKind(activate(V2)), activate(V1), activate(V2))
    U13(tt, V1, V2) -> U14(isNatKind(activate(V2)), activate(V1), activate(V2))
    U14(tt, V1, V2) -> U15(isNat(activate(V1)), activate(V2))
    U15(tt, V2) -> U16(isNat(activate(V2)))
    U16(tt) -> tt
    U21(tt, V1) -> U22(isNatKind(activate(V1)), activate(V1))
    U22(tt, V1) -> U23(isNat(activate(V1)))
    U23(tt) -> tt
    U31(tt, V2) -> U32(isNatKind(activate(V2)))
    U32(tt) -> tt
    U41(tt) -> tt
    U51(tt, N) -> U52(isNatKind(activate(N)), activate(N))
    U52(tt, N) -> activate(N)
    U61(tt, M, N) -> U62(isNatKind(activate(M)), activate(M), activate(N))
    U62(tt, M, N) -> U63(isNat(activate(N)), activate(M), activate(N))
    U63(tt, M, N) -> U64(isNatKind(activate(N)), activate(M), activate(N))
    U64(tt, M, N) -> s(plus(activate(N), activate(M)))
    activate(n__0) -> 0
    activate(n__plus(X1, X2)) -> plus(activate(X1), activate(X2))
    activate(n__s(X)) -> s(activate(X))
    activate(X) -> X
    isNat(n__0) -> tt
    isNat(n__plus(V1, V2)) -> U11(isNatKind(activate(V1)), activate(V1), activate(V2))
    isNat(n__s(V1)) -> U21(isNatKind(activate(V1)), activate(V1))
    isNatKind(n__0) -> tt
    isNatKind(n__plus(V1, V2)) -> U31(isNatKind(activate(V1)), activate(V2))
    isNatKind(n__s(V1)) -> U41(isNatKind(activate(V1)))
    plus(N, 0) -> U51(isNat(N), N)
    plus(N, s(M)) -> U61(isNat(M), M, N)
    plus(X1, X2) -> n__plus(X1, X2)
    s(X) -> n__s(X)
    
     the pairs 
    isNatKind#(n__s(V1)) -> isNatKind#(activate(V1))
    
    could not apply the generic reduction pair processor with the following
    Argument Filter: 
    pi(isNatKind#/1) = 1
    pi(n__s/1) = [1]
    pi(activate/1) = 1
    pi(n__0/0) = []
    pi(0/0) = []
    pi(U52/2) = [1,2]
    pi(tt/0) = []
    pi(n__plus/2) = [2,1]
    pi(plus/2) = [2,1]
    pi(U51/2) = [1,2]
    pi(isNat/1) = []
    pi(isNatKind/1) = []
    pi(s/1) = [1]
    pi(U61/3) = [2,3,1]
    pi(U11/3) = 1
    pi(U21/2) = 1
    pi(U31/2) = 1
    pi(U41/1) = 1
    pi(U62/3) = [2,3,1]
    pi(U12/3) = 1
    pi(U22/2) = 1
    pi(U32/1) = 1
    pi(U63/3) = [2,3,1]
    pi(U13/3) = []
    pi(U23/1) = 1
    pi(U64/3) = [2,3,1]
    pi(U14/3) = 1
    pi(U15/2) = 1
    pi(U16/1) = 1
    
    RPO with the following precedence
    precedence(n__s[1]) = 0
    precedence(n__0[0]) = 2
    precedence(0[0]) = 2
    precedence(U52[2]) = 0
    precedence(tt[0]) = 1
    precedence(n__plus[2]) = 1
    precedence(plus[2]) = 1
    precedence(U51[2]) = 0
    precedence(isNat[1]) = 1
    precedence(isNatKind[1]) = 1
    precedence(s[1]) = 0
    precedence(U61[3]) = 1
    precedence(U62[3]) = 1
    precedence(U63[3]) = 1
    precedence(U13[3]) = 1
    precedence(U64[3]) = 1
    
    precedence(_) = 0
    and the following status
    status(n__s[1]) = mul
    status(n__0[0]) = mul
    status(0[0]) = mul
    status(U52[2]) = mul
    status(tt[0]) = mul
    status(n__plus[2]) = lex
    status(plus[2]) = lex
    status(U51[2]) = mul
    status(isNat[1]) = lex
    status(isNatKind[1]) = lex
    status(s[1]) = mul
    status(U61[3]) = lex
    status(U62[3]) = lex
    status(U63[3]) = lex
    status(U13[3]) = lex
    status(U64[3]) = lex
    
    status(_) = lex
    
    problem when orienting (usable) rules
    could not orient U51(tt, N) >= U52(isNatKind(activate(N)), activate(N))
    pi( U51(tt, N) ) = U51(tt, N)
    pi( U52(isNatKind(activate(N)), activate(N)) ) = U52(isNatKind, N)
    could not orient U51(tt, N) >=RPO U52(isNatKind, N)