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:
  
  a__U51#(tt, N) -> a__U52#(a__isNatKind(N), N)
  a__U52#(tt, N) -> mark#(N)
  a__U61#(tt, M, N) -> a__U62#(a__isNatKind(M), M, N)
  a__U62#(tt, M, N) -> a__U63#(a__isNat(N), M, N)
  a__U63#(tt, M, N) -> a__U64#(a__isNatKind(N), M, N)
  a__U64#(tt, M, N) -> a__plus#(mark(N), mark(M))
  a__U64#(tt, M, N) -> mark#(N)
  a__U64#(tt, M, N) -> mark#(M)
  a__plus#(N, 0) -> a__U51#(a__isNat(N), N)
  a__plus#(N, s(M)) -> a__U61#(a__isNat(M), M, N)
  mark#(U11(X1, X2, X3)) -> mark#(X1)
  mark#(U12(X1, X2, X3)) -> mark#(X1)
  mark#(U13(X1, X2, X3)) -> mark#(X1)
  mark#(U14(X1, X2, X3)) -> mark#(X1)
  mark#(U15(X1, X2)) -> mark#(X1)
  mark#(U16(X)) -> mark#(X)
  mark#(U21(X1, X2)) -> mark#(X1)
  mark#(U22(X1, X2)) -> mark#(X1)
  mark#(U23(X)) -> mark#(X)
  mark#(U31(X1, X2)) -> mark#(X1)
  mark#(U32(X)) -> mark#(X)
  mark#(U41(X)) -> mark#(X)
  mark#(U51(X1, X2)) -> a__U51#(mark(X1), X2)
  mark#(U51(X1, X2)) -> mark#(X1)
  mark#(U52(X1, X2)) -> a__U52#(mark(X1), X2)
  mark#(U52(X1, X2)) -> mark#(X1)
  mark#(U61(X1, X2, X3)) -> a__U61#(mark(X1), X2, X3)
  mark#(U61(X1, X2, X3)) -> mark#(X1)
  mark#(U62(X1, X2, X3)) -> a__U62#(mark(X1), X2, X3)
  mark#(U62(X1, X2, X3)) -> mark#(X1)
  mark#(U63(X1, X2, X3)) -> a__U63#(mark(X1), X2, X3)
  mark#(U63(X1, X2, X3)) -> mark#(X1)
  mark#(U64(X1, X2, X3)) -> a__U64#(mark(X1), X2, X3)
  mark#(U64(X1, X2, X3)) -> mark#(X1)
  mark#(plus(X1, X2)) -> a__plus#(mark(X1), mark(X2))
  mark#(plus(X1, X2)) -> mark#(X1)
  mark#(plus(X1, X2)) -> mark#(X2)
  mark#(s(X)) -> mark#(X)
  rules:
  
  a__U11(tt, V1, V2) -> a__U12(a__isNatKind(V1), V1, V2)
  a__U11(X1, X2, X3) -> U11(X1, X2, X3)
  a__U12(tt, V1, V2) -> a__U13(a__isNatKind(V2), V1, V2)
  a__U12(X1, X2, X3) -> U12(X1, X2, X3)
  a__U13(tt, V1, V2) -> a__U14(a__isNatKind(V2), V1, V2)
  a__U13(X1, X2, X3) -> U13(X1, X2, X3)
  a__U14(tt, V1, V2) -> a__U15(a__isNat(V1), V2)
  a__U14(X1, X2, X3) -> U14(X1, X2, X3)
  a__U15(tt, V2) -> a__U16(a__isNat(V2))
  a__U15(X1, X2) -> U15(X1, X2)
  a__U16(tt) -> tt
  a__U16(X) -> U16(X)
  a__U21(tt, V1) -> a__U22(a__isNatKind(V1), V1)
  a__U21(X1, X2) -> U21(X1, X2)
  a__U22(tt, V1) -> a__U23(a__isNat(V1))
  a__U22(X1, X2) -> U22(X1, X2)
  a__U23(tt) -> tt
  a__U23(X) -> U23(X)
  a__U31(tt, V2) -> a__U32(a__isNatKind(V2))
  a__U31(X1, X2) -> U31(X1, X2)
  a__U32(tt) -> tt
  a__U32(X) -> U32(X)
  a__U41(tt) -> tt
  a__U41(X) -> U41(X)
  a__U51(tt, N) -> a__U52(a__isNatKind(N), N)
  a__U51(X1, X2) -> U51(X1, X2)
  a__U52(tt, N) -> mark(N)
  a__U52(X1, X2) -> U52(X1, X2)
  a__U61(tt, M, N) -> a__U62(a__isNatKind(M), M, N)
  a__U61(X1, X2, X3) -> U61(X1, X2, X3)
  a__U62(tt, M, N) -> a__U63(a__isNat(N), M, N)
  a__U62(X1, X2, X3) -> U62(X1, X2, X3)
  a__U63(tt, M, N) -> a__U64(a__isNatKind(N), M, N)
  a__U63(X1, X2, X3) -> U63(X1, X2, X3)
  a__U64(tt, M, N) -> s(a__plus(mark(N), mark(M)))
  a__U64(X1, X2, X3) -> U64(X1, X2, X3)
  a__isNat(0) -> tt
  a__isNat(plus(V1, V2)) -> a__U11(a__isNatKind(V1), V1, V2)
  a__isNat(s(V1)) -> a__U21(a__isNatKind(V1), V1)
  a__isNat(X) -> isNat(X)
  a__isNatKind(0) -> tt
  a__isNatKind(plus(V1, V2)) -> a__U31(a__isNatKind(V1), V2)
  a__isNatKind(s(V1)) -> a__U41(a__isNatKind(V1))
  a__isNatKind(X) -> isNatKind(X)
  a__plus(N, 0) -> a__U51(a__isNat(N), N)
  a__plus(N, s(M)) -> a__U61(a__isNat(M), M, N)
  a__plus(X1, X2) -> plus(X1, X2)
  mark(U11(X1, X2, X3)) -> a__U11(mark(X1), X2, X3)
  mark(U12(X1, X2, X3)) -> a__U12(mark(X1), X2, X3)
  mark(isNatKind(X)) -> a__isNatKind(X)
  mark(U13(X1, X2, X3)) -> a__U13(mark(X1), X2, X3)
  mark(U14(X1, X2, X3)) -> a__U14(mark(X1), X2, X3)
  mark(U15(X1, X2)) -> a__U15(mark(X1), X2)
  mark(isNat(X)) -> a__isNat(X)
  mark(U16(X)) -> a__U16(mark(X))
  mark(U21(X1, X2)) -> a__U21(mark(X1), X2)
  mark(U22(X1, X2)) -> a__U22(mark(X1), X2)
  mark(U23(X)) -> a__U23(mark(X))
  mark(U31(X1, X2)) -> a__U31(mark(X1), X2)
  mark(U32(X)) -> a__U32(mark(X))
  mark(U41(X)) -> a__U41(mark(X))
  mark(U51(X1, X2)) -> a__U51(mark(X1), X2)
  mark(U52(X1, X2)) -> a__U52(mark(X1), X2)
  mark(U61(X1, X2, X3)) -> a__U61(mark(X1), X2, X3)
  mark(U62(X1, X2, X3)) -> a__U62(mark(X1), X2, X3)
  mark(U63(X1, X2, X3)) -> a__U63(mark(X1), X2, X3)
  mark(U64(X1, X2, X3)) -> a__U64(mark(X1), X2, X3)
  mark(plus(X1, X2)) -> a__plus(mark(X1), mark(X2))
  mark(tt) -> tt
  mark(s(X)) -> s(mark(X))
  mark(0) -> 0
  
   the pairs 
  a__U64#(tt, M, N) -> a__plus#(mark(N), mark(M))
  a__U64#(tt, M, N) -> mark#(N)
  a__U64#(tt, M, N) -> mark#(M)
  a__plus#(N, 0) -> a__U51#(a__isNat(N), N)
  a__plus#(N, s(M)) -> a__U61#(a__isNat(M), M, N)
  mark#(U51(X1, X2)) -> a__U51#(mark(X1), X2)
  mark#(U51(X1, X2)) -> mark#(X1)
  mark#(U52(X1, X2)) -> a__U52#(mark(X1), X2)
  mark#(U52(X1, X2)) -> mark#(X1)
  mark#(U61(X1, X2, X3)) -> a__U61#(mark(X1), X2, X3)
  mark#(U61(X1, X2, X3)) -> mark#(X1)
  mark#(U62(X1, X2, X3)) -> a__U62#(mark(X1), X2, X3)
  mark#(U62(X1, X2, X3)) -> mark#(X1)
  mark#(U63(X1, X2, X3)) -> a__U63#(mark(X1), X2, X3)
  mark#(U63(X1, X2, X3)) -> mark#(X1)
  mark#(U64(X1, X2, X3)) -> a__U64#(mark(X1), X2, X3)
  mark#(U64(X1, X2, X3)) -> mark#(X1)
  mark#(plus(X1, X2)) -> a__plus#(mark(X1), mark(X2))
  mark#(plus(X1, X2)) -> mark#(X1)
  mark#(plus(X1, X2)) -> mark#(X2)
  mark#(s(X)) -> mark#(X)
  
  could not apply the generic root reduction pair processor with the following
  SCNP-version with mu = MS and the level mapping defined by 
  pi(mark#) = [(epsilon,0),(1,8)]
  pi(a__U51#) = [(epsilon,0),(2,8)]
  pi(a__U52#) = [(epsilon,0),(2,8)]
  pi(a__U61#) = [(epsilon,0),(2,20),(3,16)]
  pi(a__U62#) = [(epsilon,0),(2,20),(3,16)]
  pi(a__U63#) = [(epsilon,0),(2,20),(3,16)]
  pi(a__U64#) = [(epsilon,0),(2,20),(3,16)]
  pi(a__plus#) = [(epsilon,0),(1,16),(2,18)]
  Argument Filter: 
  pi(mark#/1) = []
  pi(U11/3) = 1
  pi(U12/3) = 1
  pi(U13/3) = 1
  pi(U14/3) = 1
  pi(U15/2) = 1
  pi(U16/1) = 1
  pi(U21/2) = 1
  pi(U22/2) = 1
  pi(U23/1) = 1
  pi(U31/2) = 1
  pi(U32/1) = 1
  pi(U41/1) = 1
  pi(U51/2) = [2,1]
  pi(a__U51#/2) = []
  pi(mark/1) = 1
  pi(tt/0) = []
  pi(a__U52#/2) = []
  pi(a__isNatKind/1) = []
  pi(U52/2) = [2,1]
  pi(U61/3) = [2,3,1]
  pi(a__U61#/3) = []
  pi(a__U62#/3) = []
  pi(a__U63#/3) = []
  pi(a__isNat/1) = []
  pi(a__U64#/3) = []
  pi(a__plus#/2) = []
  pi(0/0) = []
  pi(s/1) = [1]
  pi(U62/3) = [2,3,1]
  pi(U63/3) = [2,3,1]
  pi(U64/3) = [2,3,1]
  pi(plus/2) = [2,1]
  pi(a__U11/3) = 1
  pi(a__U12/3) = 1
  pi(isNatKind/1) = []
  pi(a__U13/3) = 1
  pi(a__U14/3) = 1
  pi(a__U15/2) = 1
  pi(isNat/1) = []
  pi(a__U16/1) = 1
  pi(a__U21/2) = 1
  pi(a__U22/2) = 1
  pi(a__U23/1) = 1
  pi(a__U31/2) = 1
  pi(a__U32/1) = 1
  pi(a__U41/1) = 1
  pi(a__U51/2) = [2,1]
  pi(a__U52/2) = [2,1]
  pi(a__plus/2) = [2,1]
  pi(a__U61/3) = [2,3,1]
  pi(a__U62/3) = [2,3,1]
  pi(a__U63/3) = [2,3,1]
  pi(a__U64/3) = [2,3,1]
  
  RPO with the following precedence
  precedence(mark#[1]) = 1
  precedence(U51[2]) = 0
  precedence(a__U51#[2]) = 1
  precedence(tt[0]) = 1
  precedence(a__U52#[2]) = 1
  precedence(a__isNatKind[1]) = 1
  precedence(U52[2]) = 0
  precedence(U61[3]) = 1
  precedence(a__U61#[3]) = 1
  precedence(a__U62#[3]) = 1
  precedence(a__U63#[3]) = 1
  precedence(a__isNat[1]) = 1
  precedence(a__U64#[3]) = 1
  precedence(a__plus#[2]) = 1
  precedence(0[0]) = 0
  precedence(s[1]) = 0
  precedence(U62[3]) = 1
  precedence(U63[3]) = 1
  precedence(U64[3]) = 1
  precedence(plus[2]) = 1
  precedence(isNatKind[1]) = 1
  precedence(isNat[1]) = 1
  precedence(a__U51[2]) = 0
  precedence(a__U52[2]) = 0
  precedence(a__plus[2]) = 1
  precedence(a__U61[3]) = 1
  precedence(a__U62[3]) = 1
  precedence(a__U63[3]) = 1
  precedence(a__U64[3]) = 1
  
  precedence(_) = 0
  and the following status
  status(mark#[1]) = lex
  status(U51[2]) = lex
  status(a__U51#[2]) = lex
  status(tt[0]) = lex
  status(a__U52#[2]) = lex
  status(a__isNatKind[1]) = lex
  status(U52[2]) = lex
  status(U61[3]) = lex
  status(a__U61#[3]) = lex
  status(a__U62#[3]) = lex
  status(a__U63#[3]) = lex
  status(a__isNat[1]) = lex
  status(a__U64#[3]) = lex
  status(a__plus#[2]) = lex
  status(0[0]) = lex
  status(s[1]) = lex
  status(U62[3]) = lex
  status(U63[3]) = lex
  status(U64[3]) = lex
  status(plus[2]) = lex
  status(isNatKind[1]) = lex
  status(isNat[1]) = lex
  status(a__U51[2]) = lex
  status(a__U52[2]) = lex
  status(a__plus[2]) = lex
  status(a__U61[3]) = lex
  status(a__U62[3]) = lex
  status(a__U63[3]) = lex
  status(a__U64[3]) = lex
  
  status(_) = lex
  
  problem when orienting DPs
  cannot orient pair a__U51#(tt, N) -> a__U52#(a__isNatKind(N), N) weakly:
  [(a__U51#(tt, N),0),(N,8)] >=mu [(a__U52#(a__isNatKind(N), N),0),(N,8)] could not be ensured