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 when applying the reduction pair processor to remove from the DP problem
  pairs:
  
  U11#(tt, V1, V2) -> U12#(isNatKind(activate(V1)), activate(V1), activate(V2))
  U11#(tt, V1, V2) -> isNatKind#(activate(V1))
  U11#(tt, V1, V2) -> activate#(V1)
  U11#(tt, V1, V2) -> activate#(V2)
  U12#(tt, V1, V2) -> U13#(isNatKind(activate(V2)), activate(V1), activate(V2))
  U12#(tt, V1, V2) -> isNatKind#(activate(V2))
  U12#(tt, V1, V2) -> activate#(V2)
  U12#(tt, V1, V2) -> activate#(V1)
  U13#(tt, V1, V2) -> U14#(isNatKind(activate(V2)), activate(V1), activate(V2))
  U13#(tt, V1, V2) -> isNatKind#(activate(V2))
  U13#(tt, V1, V2) -> activate#(V2)
  U13#(tt, V1, V2) -> activate#(V1)
  U14#(tt, V1, V2) -> U15#(isNat(activate(V1)), activate(V2))
  U14#(tt, V1, V2) -> isNat#(activate(V1))
  U14#(tt, V1, V2) -> activate#(V1)
  U14#(tt, V1, V2) -> activate#(V2)
  U15#(tt, V2) -> isNat#(activate(V2))
  U15#(tt, V2) -> activate#(V2)
  U21#(tt, V1) -> U22#(isNatKind(activate(V1)), activate(V1))
  U21#(tt, V1) -> isNatKind#(activate(V1))
  U21#(tt, V1) -> activate#(V1)
  U22#(tt, V1) -> isNat#(activate(V1))
  U22#(tt, V1) -> activate#(V1)
  U31#(tt, V2) -> isNatKind#(activate(V2))
  U31#(tt, V2) -> activate#(V2)
  U51#(tt, N) -> U52#(isNatKind(activate(N)), activate(N))
  U51#(tt, N) -> isNatKind#(activate(N))
  U51#(tt, N) -> activate#(N)
  U52#(tt, N) -> activate#(N)
  U61#(tt, M, N) -> U62#(isNatKind(activate(M)), activate(M), activate(N))
  U61#(tt, M, N) -> isNatKind#(activate(M))
  U61#(tt, M, N) -> activate#(M)
  U61#(tt, M, N) -> activate#(N)
  U62#(tt, M, N) -> U63#(isNat(activate(N)), activate(M), activate(N))
  U62#(tt, M, N) -> isNat#(activate(N))
  U62#(tt, M, N) -> activate#(N)
  U62#(tt, M, N) -> activate#(M)
  U63#(tt, M, N) -> U64#(isNatKind(activate(N)), activate(M), activate(N))
  U63#(tt, M, N) -> isNatKind#(activate(N))
  U63#(tt, M, N) -> activate#(N)
  U63#(tt, M, N) -> activate#(M)
  U64#(tt, M, N) -> plus#(activate(N), activate(M))
  U64#(tt, M, N) -> activate#(N)
  U64#(tt, M, N) -> activate#(M)
  isNat#(n__plus(V1, V2)) -> U11#(isNatKind(activate(V1)), activate(V1), activate(V2))
  isNat#(n__plus(V1, V2)) -> isNatKind#(activate(V1))
  isNat#(n__plus(V1, V2)) -> activate#(V1)
  isNat#(n__plus(V1, V2)) -> activate#(V2)
  isNat#(n__s(V1)) -> U21#(isNatKind(activate(V1)), activate(V1))
  isNat#(n__s(V1)) -> isNatKind#(activate(V1))
  isNat#(n__s(V1)) -> activate#(V1)
  isNatKind#(n__plus(V1, V2)) -> U31#(isNatKind(activate(V1)), activate(V2))
  isNatKind#(n__plus(V1, V2)) -> isNatKind#(activate(V1))
  isNatKind#(n__plus(V1, V2)) -> activate#(V1)
  isNatKind#(n__plus(V1, V2)) -> activate#(V2)
  isNatKind#(n__s(V1)) -> isNatKind#(activate(V1))
  isNatKind#(n__s(V1)) -> activate#(V1)
  plus#(N, 0) -> U51#(isNat(N), N)
  plus#(N, 0) -> isNat#(N)
  plus#(N, s(M)) -> U61#(isNat(M), M, N)
  plus#(N, s(M)) -> isNat#(M)
  activate#(n__plus(X1, X2)) -> plus#(activate(X1), activate(X2))
  activate#(n__plus(X1, X2)) -> activate#(X1)
  activate#(n__plus(X1, X2)) -> activate#(X2)
  activate#(n__s(X)) -> activate#(X)
  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 
  U11#(tt, V1, V2) -> activate#(V2)
  U31#(tt, V2) -> isNatKind#(activate(V2))
  U31#(tt, V2) -> activate#(V2)
  isNat#(n__plus(V1, V2)) -> U11#(isNatKind(activate(V1)), activate(V1), activate(V2))
  isNat#(n__plus(V1, V2)) -> isNatKind#(activate(V1))
  isNat#(n__plus(V1, V2)) -> activate#(V1)
  isNat#(n__plus(V1, V2)) -> activate#(V2)
  isNatKind#(n__plus(V1, V2)) -> U31#(isNatKind(activate(V1)), activate(V2))
  isNatKind#(n__plus(V1, V2)) -> isNatKind#(activate(V1))
  isNatKind#(n__plus(V1, V2)) -> activate#(V1)
  isNatKind#(n__plus(V1, V2)) -> activate#(V2)
  activate#(n__plus(X1, X2)) -> plus#(activate(X1), activate(X2))
  activate#(n__plus(X1, X2)) -> activate#(X1)
  activate#(n__plus(X1, X2)) -> activate#(X2)
  
  could not apply the generic root reduction pair processor with the following
  SCNP-version with mu = MAX and the level mapping defined by 
  pi(U12#) = [(epsilon,0),(3,0)]
  pi(U13#) = [(2,0),(3,0)]
  pi(U14#) = [(2,0),(3,0)]
  pi(U15#) = [(2,0)]
  pi(isNat#) = [(1,0)]
  pi(U11#) = [(1,4),(2,0),(3,5)]
  pi(isNatKind#) = [(1,0)]
  pi(U31#) = [(2,9)]
  pi(activate#) = [(epsilon,0)]
  pi(plus#) = [(epsilon,0),(1,0)]
  pi(U51#) = [(epsilon,0)]
  pi(U52#) = [(2,0)]
  pi(U21#) = [(2,0)]
  pi(U22#) = [(2,0)]
  pi(U61#) = [(2,0),(3,0)]
  pi(U62#) = [(2,0),(3,0)]
  pi(U63#) = [(epsilon,0),(2,0)]
  pi(U64#) = [(2,0),(3,0)]
  Argument Filter: 
  pi(U12#/3) = 2
  pi(tt/0) = []
  pi(U13#/3) = [1]
  pi(isNatKind/1) = []
  pi(activate/1) = 1
  pi(U14#/3) = [3,2,1]
  pi(U15#/2) = [1,2]
  pi(isNat/1) = [1]
  pi(isNat#/1) = []
  pi(n__plus/2) = [1,2]
  pi(U11#/3) = [1]
  pi(isNatKind#/1) = [1]
  pi(U31#/2) = [1,2]
  pi(activate#/1) = 1
  pi(plus#/2) = 2
  pi(0/0) = []
  pi(U51#/2) = 2
  pi(U52#/2) = [1]
  pi(n__s/1) = 1
  pi(U21#/2) = []
  pi(U22#/2) = []
  pi(s/1) = 1
  pi(U61#/3) = [3]
  pi(U62#/3) = [1]
  pi(U63#/3) = 3
  pi(U64#/3) = []
  pi(n__0/0) = []
  pi(U52/2) = [1,2]
  pi(plus/2) = [1,2]
  pi(U51/2) = [2]
  pi(U31/2) = 1
  pi(U41/1) = []
  pi(U11/3) = [1,2,3]
  pi(U21/2) = [1]
  pi(U61/3) = [2,3]
  pi(U12/3) = [1,2,3]
  pi(U32/1) = 1
  pi(U22/2) = [1]
  pi(U62/3) = [2,3]
  pi(U13/3) = [1,2,3]
  pi(U23/1) = []
  pi(U63/3) = [2,3]
  pi(U14/3) = [1,2,3]
  pi(U64/3) = [2,3]
  pi(U15/2) = 1
  pi(U16/1) = []
  
  RPO with the following precedence
  precedence(tt[0]) = 5
  precedence(U13#[3]) = 6
  precedence(isNatKind[1]) = 5
  precedence(U14#[3]) = 5
  precedence(U15#[2]) = 1
  precedence(isNat[1]) = 7
  precedence(isNat#[1]) = 8
  precedence(n__plus[2]) = 11
  precedence(U11#[3]) = 12
  precedence(isNatKind#[1]) = 11
  precedence(U31#[2]) = 11
  precedence(0[0]) = 13
  precedence(U52#[2]) = 14
  precedence(U21#[2]) = 15
  precedence(U22#[2]) = 2
  precedence(U61#[3]) = 0
  precedence(U62#[3]) = 8
  precedence(U64#[3]) = 16
  precedence(n__0[0]) = 13
  precedence(U52[2]) = 3
  precedence(plus[2]) = 11
  precedence(U51[2]) = 9
  precedence(U41[1]) = 5
  precedence(U11[3]) = 10
  precedence(U21[2]) = 4
  precedence(U61[3]) = 11
  precedence(U12[3]) = 10
  precedence(U22[2]) = 4
  precedence(U62[3]) = 11
  precedence(U13[3]) = 10
  precedence(U23[1]) = 5
  precedence(U63[3]) = 11
  precedence(U14[3]) = 10
  precedence(U64[3]) = 11
  precedence(U16[1]) = 5
  
  precedence(_) = 0
  and the following status
  status(tt[0]) = mul
  status(U13#[3]) = mul
  status(isNatKind[1]) = mul
  status(U14#[3]) = lex
  status(U15#[2]) = mul
  status(isNat[1]) = lex
  status(isNat#[1]) = mul
  status(n__plus[2]) = mul
  status(U11#[3]) = mul
  status(isNatKind#[1]) = mul
  status(U31#[2]) = mul
  status(0[0]) = mul
  status(U52#[2]) = lex
  status(U21#[2]) = mul
  status(U22#[2]) = lex
  status(U61#[3]) = lex
  status(U62#[3]) = mul
  status(U64#[3]) = lex
  status(n__0[0]) = mul
  status(U52[2]) = lex
  status(plus[2]) = mul
  status(U51[2]) = lex
  status(U41[1]) = mul
  status(U11[3]) = lex
  status(U21[2]) = mul
  status(U61[3]) = mul
  status(U12[3]) = lex
  status(U22[2]) = mul
  status(U62[3]) = mul
  status(U13[3]) = lex
  status(U23[1]) = mul
  status(U63[3]) = mul
  status(U14[3]) = lex
  status(U64[3]) = mul
  status(U16[1]) = mul
  
  status(_) = lex
  
  problem when orienting (usable) rules
  could not orient U21(tt, V1) >= U22(isNatKind(activate(V1)), activate(V1))
  pi( U21(tt, V1) ) = U21(tt)
  pi( U22(isNatKind(activate(V1)), activate(V1)) ) = U22(isNatKind)
  could not orient U21(tt) >=RPO U22(isNatKind)