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 reduction pair processor
   1.1.1.1.1: error below the dependency graph processor
    1.1.1.1.1.1: error when applying the reduction pair processor to remove from the DP problem
     pairs:
     
     U41#(tt, M, N) -> U42#(isNat(activate(N)), activate(M), activate(N))
     U42#(tt, M, N) -> plus#(activate(N), activate(M))
     plus#(N, s(M)) -> U41#(isNat(M), M, N)
     rules:
     
     0 -> n__0
     U11(tt, V2) -> U12(isNat(activate(V2)))
     U12(tt) -> tt
     U21(tt) -> tt
     U31(tt, N) -> activate(N)
     U41(tt, M, N) -> U42(isNat(activate(N)), activate(M), activate(N))
     U42(tt, M, N) -> s(plus(activate(N), activate(M)))
     activate(n__0) -> 0
     activate(n__plus(X1, X2)) -> plus(X1, X2)
     activate(n__s(X)) -> s(X)
     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)))
     plus(N, 0) -> U31(isNat(N), N)
     plus(N, s(M)) -> U41(isNat(M), M, N)
     plus(X1, X2) -> n__plus(X1, X2)
     s(X) -> n__s(X)
     
      the pairs 
     plus#(N, s(M)) -> U41#(isNat(M), M, N)
     
     could not apply the generic root reduction pair processor with the following
     SCNP-version with mu = MAX and the level mapping defined by 
     pi(plus#) = [(2,0)]
     pi(U41#) = [(1,15),(2,0)]
     pi(U42#) = [(1,0),(2,0)]
     Argument Filter: 
     pi(plus#/2) = [1,2]
     pi(s/1) = [1]
     pi(U41#/3) = [1,2,3]
     pi(isNat/1) = []
     pi(tt/0) = []
     pi(U42#/3) = [3]
     pi(activate/1) = 1
     pi(n__0/0) = []
     pi(n__plus/2) = [1,2]
     pi(U11/2) = 1
     pi(n__s/1) = [1]
     pi(U21/1) = 1
     pi(0/0) = []
     pi(plus/2) = [1,2]
     pi(U31/2) = [1,2]
     pi(U41/3) = [1,2,3]
     pi(U12/1) = []
     pi(U42/3) = [1,2,3]
     
     RPO with the following precedence
     precedence(plus#[2]) = 1
     precedence(s[1]) = 0
     precedence(U41#[3]) = 1
     precedence(isNat[1]) = 0
     precedence(tt[0]) = 0
     precedence(U42#[3]) = 1
     precedence(n__0[0]) = 2
     precedence(n__plus[2]) = 3
     precedence(n__s[1]) = 0
     precedence(0[0]) = 2
     precedence(plus[2]) = 3
     precedence(U31[2]) = 0
     precedence(U41[3]) = 3
     precedence(U12[1]) = 0
     precedence(U42[3]) = 3
     
     precedence(_) = 0
     and the following status
     status(plus#[2]) = mul
     status(s[1]) = mul
     status(U41#[3]) = mul
     status(isNat[1]) = lex
     status(tt[0]) = mul
     status(U42#[3]) = mul
     status(n__0[0]) = mul
     status(n__plus[2]) = mul
     status(n__s[1]) = mul
     status(0[0]) = mul
     status(plus[2]) = mul
     status(U31[2]) = lex
     status(U41[3]) = mul
     status(U12[1]) = lex
     status(U42[3]) = mul
     
     status(_) = lex
     
     problem when orienting (usable) rules
     could not orient U41(tt, M, N) >= U42(isNat(activate(N)), activate(M), activate(N))
     pi( U41(tt, M, N) ) = U41(tt, M, N)
     pi( U42(isNat(activate(N)), activate(M), activate(N)) ) = U42(isNat, M, N)
     could not orient U41(tt, M, N) >=RPO U42(isNat, M, N)