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:
    
    isNat#(n__s(V1)) -> isNat#(activate(V1))
    rules:
    
    0 -> n__0
    U11(tt, V2) -> U12(isNat(activate(V2)))
    U12(tt) -> tt
    U21(tt) -> tt
    U31(tt, V2) -> U32(isNat(activate(V2)))
    U32(tt) -> tt
    U41(tt, N) -> activate(N)
    U51(tt, M, N) -> U52(isNat(activate(N)), activate(M), activate(N))
    U52(tt, M, N) -> s(plus(activate(N), activate(M)))
    U61(tt) -> 0
    U71(tt, M, N) -> U72(isNat(activate(N)), activate(M), activate(N))
    U72(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__s(X)) -> s(X)
    activate(n__x(X1, X2)) -> x(X1, X2)
    activate(X) -> X
    isNat(n__0) -> tt
    isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2))
    isNat(n__s(V1)) -> U21(isNat(activate(V1)))
    isNat(n__x(V1, V2)) -> U31(isNat(activate(V1)), activate(V2))
    plus(N, 0) -> U41(isNat(N), N)
    plus(N, s(M)) -> U51(isNat(M), M, N)
    plus(X1, X2) -> n__plus(X1, X2)
    s(X) -> n__s(X)
    x(N, 0) -> U61(isNat(N))
    x(N, s(M)) -> U71(isNat(M), M, N)
    x(X1, X2) -> n__x(X1, X2)
    
     the pairs 
    isNat#(n__s(V1)) -> isNat#(activate(V1))
    
    could not apply the generic root reduction pair processor with the following
    SCNP-version with mu = MAX and the level mapping defined by 
    pi(isNat#) = [(1,0)]
    Argument Filter: 
    pi(isNat#/1) = 1
    pi(n__s/1) = [1]
    pi(activate/1) = 1
    pi(n__0/0) = []
    pi(0/0) = []
    pi(n__plus/2) = [1,2]
    pi(plus/2) = [1,2]
    pi(U41/2) = 2
    pi(isNat/1) = []
    pi(tt/0) = []
    pi(n__x/2) = [1,2]
    pi(x/2) = [1,2]
    pi(s/1) = [1]
    pi(U71/3) = [1,2,3]
    pi(U72/3) = [1,2,3]
    pi(U51/3) = [1,2,3]
    pi(U11/2) = []
    pi(U21/1) = 1
    pi(U31/2) = 1
    pi(U61/1) = []
    pi(U52/3) = [1,2,3]
    pi(U12/1) = []
    pi(U32/1) = []
    
    RPO with the following precedence
    precedence(n__s[1]) = 0
    precedence(n__0[0]) = 1
    precedence(0[0]) = 1
    precedence(n__plus[2]) = 2
    precedence(plus[2]) = 2
    precedence(isNat[1]) = 0
    precedence(tt[0]) = 0
    precedence(n__x[2]) = 3
    precedence(x[2]) = 3
    precedence(s[1]) = 0
    precedence(U71[3]) = 3
    precedence(U72[3]) = 3
    precedence(U51[3]) = 2
    precedence(U11[2]) = 0
    precedence(U61[1]) = 1
    precedence(U52[3]) = 2
    precedence(U12[1]) = 0
    precedence(U32[1]) = 0
    
    precedence(_) = 0
    and the following status
    status(n__s[1]) = mul
    status(n__0[0]) = mul
    status(0[0]) = mul
    status(n__plus[2]) = mul
    status(plus[2]) = mul
    status(isNat[1]) = mul
    status(tt[0]) = mul
    status(n__x[2]) = mul
    status(x[2]) = mul
    status(s[1]) = mul
    status(U71[3]) = mul
    status(U72[3]) = mul
    status(U51[3]) = mul
    status(U11[2]) = mul
    status(U61[1]) = mul
    status(U52[3]) = mul
    status(U12[1]) = mul
    status(U32[1]) = mul
    
    status(_) = lex
    
    problem when orienting (usable) rules
    could not orient U51(tt, M, N) >= U52(isNat(activate(N)), activate(M), activate(N))
    pi( U51(tt, M, N) ) = U51(tt, M, N)
    pi( U52(isNat(activate(N)), activate(M), activate(N)) ) = U52(isNat, M, N)
    could not orient U51(tt, M, N) >=RPO U52(isNat, M, N)