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 below the reduction pair processor
    1.1.1.1.2.1: error below the dependency graph processor
     1.1.1.1.2.1.1: 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, N) -> activate(N)
      U21(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__isNat(X)) -> isNat(X)
      activate(n__s(X)) -> s(activate(X))
      activate(X) -> X
      and(tt, X) -> activate(X)
      isNat(n__0) -> tt
      isNat(n__plus(V1, V2)) -> and(isNat(activate(V1)), n__isNat(activate(V2)))
      isNat(n__s(V1)) -> isNat(activate(V1))
      isNat(X) -> n__isNat(X)
      plus(N, 0) -> U11(isNat(N), N)
      plus(N, s(M)) -> U21(and(isNat(M), n__isNat(N)), M, N)
      plus(X1, X2) -> n__plus(X1, X2)
      s(X) -> n__s(X)
      
       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#) = [(epsilon,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(U11/2) = [1,2]
      pi(isNat/1) = []
      pi(tt/0) = []
      pi(n__isNat/1) = []
      pi(and/2) = 2
      pi(s/1) = [1]
      pi(U21/3) = [1,2,3]
      
      RPO with the following precedence
      precedence(n__s[1]) = 1
      precedence(n__0[0]) = 1
      precedence(0[0]) = 1
      precedence(n__plus[2]) = 2
      precedence(plus[2]) = 2
      precedence(U11[2]) = 2
      precedence(isNat[1]) = 1
      precedence(tt[0]) = 0
      precedence(n__isNat[1]) = 1
      precedence(s[1]) = 1
      precedence(U21[3]) = 2
      
      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(U11[2]) = mul
      status(isNat[1]) = mul
      status(tt[0]) = mul
      status(n__isNat[1]) = mul
      status(s[1]) = mul
      status(U21[3]) = mul
      
      status(_) = lex
      
      problem when orienting (usable) rules
      could not orient plus(N, 0) >= U11(isNat(N), N)
      pi( plus(N, 0) ) = plus(N, 0)
      pi( U11(isNat(N), N) ) = U11(isNat, N)
      could not orient plus(N, 0) >=RPO U11(isNat, N)