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#(isNat(activate(V1)), activate(V2))
  U11#(tt, V1, V2) -> isNat#(activate(V1))
  U11#(tt, V1, V2) -> activate#(V1)
  U11#(tt, V1, V2) -> activate#(V2)
  U12#(tt, V2) -> isNat#(activate(V2))
  U12#(tt, V2) -> activate#(V2)
  U21#(tt, V1) -> isNat#(activate(V1))
  U21#(tt, V1) -> activate#(V1)
  U31#(tt, V1, V2) -> U32#(isNat(activate(V1)), activate(V2))
  U31#(tt, V1, V2) -> isNat#(activate(V1))
  U31#(tt, V1, V2) -> activate#(V1)
  U31#(tt, V1, V2) -> activate#(V2)
  U32#(tt, V2) -> isNat#(activate(V2))
  U32#(tt, V2) -> activate#(V2)
  U41#(tt, N) -> activate#(N)
  U51#(tt, M, N) -> plus#(activate(N), activate(M))
  U51#(tt, M, N) -> activate#(N)
  U51#(tt, M, N) -> activate#(M)
  U71#(tt, M, N) -> plus#(x(activate(N), activate(M)), activate(N))
  U71#(tt, M, N) -> x#(activate(N), activate(M))
  U71#(tt, M, N) -> activate#(N)
  U71#(tt, M, N) -> activate#(M)
  and#(tt, X) -> activate#(X)
  isNat#(n__plus(V1, V2)) -> U11#(and(isNatKind(activate(V1)), n__isNatKind(activate(V2))), activate(V1), activate(V2))
  isNat#(n__plus(V1, V2)) -> and#(isNatKind(activate(V1)), n__isNatKind(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)
  isNat#(n__x(V1, V2)) -> U31#(and(isNatKind(activate(V1)), n__isNatKind(activate(V2))), activate(V1), activate(V2))
  isNat#(n__x(V1, V2)) -> and#(isNatKind(activate(V1)), n__isNatKind(activate(V2)))
  isNat#(n__x(V1, V2)) -> isNatKind#(activate(V1))
  isNat#(n__x(V1, V2)) -> activate#(V1)
  isNat#(n__x(V1, V2)) -> activate#(V2)
  isNatKind#(n__plus(V1, V2)) -> and#(isNatKind(activate(V1)), n__isNatKind(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)
  isNatKind#(n__x(V1, V2)) -> and#(isNatKind(activate(V1)), n__isNatKind(activate(V2)))
  isNatKind#(n__x(V1, V2)) -> isNatKind#(activate(V1))
  isNatKind#(n__x(V1, V2)) -> activate#(V1)
  isNatKind#(n__x(V1, V2)) -> activate#(V2)
  plus#(N, 0) -> U41#(and(isNat(N), n__isNatKind(N)), N)
  plus#(N, 0) -> and#(isNat(N), n__isNatKind(N))
  plus#(N, 0) -> isNat#(N)
  plus#(N, s(M)) -> U51#(and(and(isNat(M), n__isNatKind(M)), n__and(isNat(N), n__isNatKind(N))), M, N)
  plus#(N, s(M)) -> and#(and(isNat(M), n__isNatKind(M)), n__and(isNat(N), n__isNatKind(N)))
  plus#(N, s(M)) -> and#(isNat(M), n__isNatKind(M))
  plus#(N, s(M)) -> isNat#(M)
  plus#(N, s(M)) -> isNat#(N)
  x#(N, 0) -> and#(isNat(N), n__isNatKind(N))
  x#(N, 0) -> isNat#(N)
  x#(N, s(M)) -> U71#(and(and(isNat(M), n__isNatKind(M)), n__and(isNat(N), n__isNatKind(N))), M, N)
  x#(N, s(M)) -> and#(and(isNat(M), n__isNatKind(M)), n__and(isNat(N), n__isNatKind(N)))
  x#(N, s(M)) -> and#(isNat(M), n__isNatKind(M))
  x#(N, s(M)) -> isNat#(M)
  x#(N, s(M)) -> isNat#(N)
  activate#(n__plus(X1, X2)) -> plus#(X1, X2)
  activate#(n__isNatKind(X)) -> isNatKind#(X)
  activate#(n__x(X1, X2)) -> x#(X1, X2)
  activate#(n__and(X1, X2)) -> and#(X1, X2)
  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, V1, V2) -> U32(isNat(activate(V1)), activate(V2))
  U32(tt, V2) -> U33(isNat(activate(V2)))
  U33(tt) -> tt
  U41(tt, N) -> activate(N)
  U51(tt, M, N) -> s(plus(activate(N), activate(M)))
  U61(tt) -> 0
  U71(tt, M, N) -> plus(x(activate(N), activate(M)), activate(N))
  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__x(X1, X2)) -> x(X1, X2)
  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))
  isNat(n__x(V1, V2)) -> U31(and(isNatKind(activate(V1)), n__isNatKind(activate(V2))), activate(V1), activate(V2))
  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(n__x(V1, V2)) -> and(isNatKind(activate(V1)), n__isNatKind(activate(V2)))
  isNatKind(X) -> n__isNatKind(X)
  plus(N, 0) -> U41(and(isNat(N), n__isNatKind(N)), N)
  plus(N, s(M)) -> U51(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)
  x(N, 0) -> U61(and(isNat(N), n__isNatKind(N)))
  x(N, s(M)) -> U71(and(and(isNat(M), n__isNatKind(M)), n__and(isNat(N), n__isNatKind(N))), M, N)
  x(X1, X2) -> n__x(X1, X2)
  
   the pairs 
  U11#(tt, V1, V2) -> U12#(isNat(activate(V1)), activate(V2))
  U11#(tt, V1, V2) -> isNat#(activate(V1))
  U11#(tt, V1, V2) -> activate#(V1)
  U11#(tt, V1, V2) -> activate#(V2)
  U12#(tt, V2) -> isNat#(activate(V2))
  U12#(tt, V2) -> activate#(V2)
  U31#(tt, V1, V2) -> U32#(isNat(activate(V1)), activate(V2))
  U31#(tt, V1, V2) -> isNat#(activate(V1))
  U31#(tt, V1, V2) -> activate#(V1)
  U31#(tt, V1, V2) -> activate#(V2)
  U32#(tt, V2) -> isNat#(activate(V2))
  U32#(tt, V2) -> activate#(V2)
  U51#(tt, M, N) -> plus#(activate(N), activate(M))
  U51#(tt, M, N) -> activate#(N)
  U51#(tt, M, N) -> activate#(M)
  U71#(tt, M, N) -> plus#(x(activate(N), activate(M)), activate(N))
  U71#(tt, M, N) -> x#(activate(N), activate(M))
  U71#(tt, M, N) -> activate#(N)
  U71#(tt, M, N) -> activate#(M)
  isNat#(n__plus(V1, V2)) -> U11#(and(isNatKind(activate(V1)), n__isNatKind(activate(V2))), activate(V1), activate(V2))
  isNat#(n__plus(V1, V2)) -> and#(isNatKind(activate(V1)), n__isNatKind(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)) -> activate#(V1)
  isNat#(n__x(V1, V2)) -> U31#(and(isNatKind(activate(V1)), n__isNatKind(activate(V2))), activate(V1), activate(V2))
  isNat#(n__x(V1, V2)) -> and#(isNatKind(activate(V1)), n__isNatKind(activate(V2)))
  isNat#(n__x(V1, V2)) -> isNatKind#(activate(V1))
  isNat#(n__x(V1, V2)) -> activate#(V1)
  isNat#(n__x(V1, V2)) -> activate#(V2)
  isNatKind#(n__plus(V1, V2)) -> and#(isNatKind(activate(V1)), n__isNatKind(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)
  isNatKind#(n__x(V1, V2)) -> and#(isNatKind(activate(V1)), n__isNatKind(activate(V2)))
  isNatKind#(n__x(V1, V2)) -> isNatKind#(activate(V1))
  isNatKind#(n__x(V1, V2)) -> activate#(V1)
  isNatKind#(n__x(V1, V2)) -> activate#(V2)
  plus#(N, 0) -> U41#(and(isNat(N), n__isNatKind(N)), N)
  plus#(N, 0) -> and#(isNat(N), n__isNatKind(N))
  plus#(N, 0) -> isNat#(N)
  plus#(N, s(M)) -> U51#(and(and(isNat(M), n__isNatKind(M)), n__and(isNat(N), n__isNatKind(N))), M, N)
  plus#(N, s(M)) -> and#(and(isNat(M), n__isNatKind(M)), n__and(isNat(N), n__isNatKind(N)))
  plus#(N, s(M)) -> and#(isNat(M), n__isNatKind(M))
  plus#(N, s(M)) -> isNat#(M)
  plus#(N, s(M)) -> isNat#(N)
  x#(N, 0) -> and#(isNat(N), n__isNatKind(N))
  x#(N, 0) -> isNat#(N)
  x#(N, s(M)) -> U71#(and(and(isNat(M), n__isNatKind(M)), n__and(isNat(N), n__isNatKind(N))), M, N)
  x#(N, s(M)) -> and#(and(isNat(M), n__isNatKind(M)), n__and(isNat(N), n__isNatKind(N)))
  x#(N, s(M)) -> and#(isNat(M), n__isNatKind(M))
  x#(N, s(M)) -> isNat#(M)
  x#(N, s(M)) -> isNat#(N)
  activate#(n__isNatKind(X)) -> isNatKind#(X)
  
  could not apply the generic reduction pair processor with the following
  Argument Filter: 
  pi(U12#/2) = [1,2]
  pi(tt/0) = []
  pi(isNat#/1) = 1
  pi(activate/1) = 1
  pi(n__plus/2) = [1,2]
  pi(U11#/3) = [1,2,3]
  pi(and/2) = 2
  pi(isNatKind/1) = [1]
  pi(n__isNatKind/1) = [1]
  pi(isNat/1) = []
  pi(activate#/1) = 1
  pi(plus#/2) = [1,2]
  pi(0/0) = []
  pi(U41#/2) = 2
  pi(isNatKind#/1) = [1]
  pi(and#/2) = 2
  pi(n__x/2) = [1,2]
  pi(x#/2) = [1,2]
  pi(n__and/2) = 2
  pi(n__s/1) = [1]
  pi(U21#/2) = 2
  pi(U31#/3) = [1,2,3]
  pi(U32#/2) = [1,2]
  pi(s/1) = [1]
  pi(U71#/3) = [3,2,1]
  pi(x/2) = [1,2]
  pi(U51#/3) = [3,2,1]
  pi(n__0/0) = []
  pi(plus/2) = [1,2]
  pi(U41/2) = [2,1]
  pi(U71/3) = [3,2,1]
  pi(U11/3) = []
  pi(U21/2) = []
  pi(U31/3) = []
  pi(U61/1) = []
  pi(U51/3) = [3,2,1]
  pi(U12/2) = 1
  pi(U22/1) = 1
  pi(U32/2) = 1
  pi(U13/1) = 1
  pi(U33/1) = 1
  
  RPO with the following precedence
  precedence(U12#[2]) = 2
  precedence(tt[0]) = 1
  precedence(n__plus[2]) = 5
  precedence(U11#[3]) = 2
  precedence(isNatKind[1]) = 3
  precedence(n__isNatKind[1]) = 3
  precedence(isNat[1]) = 1
  precedence(plus#[2]) = 5
  precedence(0[0]) = 1
  precedence(isNatKind#[1]) = 0
  precedence(n__x[2]) = 7
  precedence(x#[2]) = 7
  precedence(n__s[1]) = 0
  precedence(U31#[3]) = 6
  precedence(U32#[2]) = 6
  precedence(s[1]) = 0
  precedence(U71#[3]) = 7
  precedence(x[2]) = 7
  precedence(U51#[3]) = 5
  precedence(n__0[0]) = 1
  precedence(plus[2]) = 5
  precedence(U41[2]) = 4
  precedence(U71[3]) = 7
  precedence(U11[3]) = 1
  precedence(U21[2]) = 1
  precedence(U31[3]) = 1
  precedence(U61[1]) = 1
  precedence(U51[3]) = 5
  
  precedence(_) = 0
  and the following status
  status(U12#[2]) = mul
  status(tt[0]) = mul
  status(n__plus[2]) = lex
  status(U11#[3]) = mul
  status(isNatKind[1]) = mul
  status(n__isNatKind[1]) = mul
  status(isNat[1]) = lex
  status(plus#[2]) = lex
  status(0[0]) = mul
  status(isNatKind#[1]) = mul
  status(n__x[2]) = lex
  status(x#[2]) = lex
  status(n__s[1]) = mul
  status(U31#[3]) = mul
  status(U32#[2]) = mul
  status(s[1]) = mul
  status(U71#[3]) = lex
  status(x[2]) = lex
  status(U51#[3]) = lex
  status(n__0[0]) = mul
  status(plus[2]) = lex
  status(U41[2]) = lex
  status(U71[3]) = lex
  status(U11[3]) = lex
  status(U21[2]) = lex
  status(U31[3]) = lex
  status(U61[1]) = mul
  status(U51[3]) = lex
  
  status(_) = lex
  
  problem when orienting DPs
  could not orient U11#(tt, V1, V2) > U12#(isNat(activate(V1)), activate(V2))
  pi( U11#(tt, V1, V2) ) = U11#(tt, V1, V2)
  pi( U12#(isNat(activate(V1)), activate(V2)) ) = U12#(isNat, V2)
  could not orient U11#(tt, V1, V2) >RPO U12#(isNat, V2)