ceta_eq: termination proof not accepted
1: error below switch to dependency pairs
1.1: error below the reduction pair processor
 1.1.1: error below the dependency graph processor
  1.1.1.1: error when applying the reduction pair processor to remove from the DP problem
   pairs:
   
   a__U21#(tt, M, N) -> a__plus#(mark(N), mark(M))
   a__plus#(N, s(M)) -> a__U21#(a__and(a__isNat(M), isNat(N)), M, N)
   rules:
   
   a__U11(tt, N) -> mark(N)
   a__U11(X1, X2) -> U11(X1, X2)
   a__U21(tt, M, N) -> s(a__plus(mark(N), mark(M)))
   a__U21(X1, X2, X3) -> U21(X1, X2, X3)
   a__and(tt, X) -> mark(X)
   a__and(X1, X2) -> and(X1, X2)
   a__isNat(0) -> tt
   a__isNat(plus(V1, V2)) -> a__and(a__isNat(V1), isNat(V2))
   a__isNat(s(V1)) -> a__isNat(V1)
   a__isNat(X) -> isNat(X)
   a__plus(N, 0) -> a__U11(a__isNat(N), N)
   a__plus(N, s(M)) -> a__U21(a__and(a__isNat(M), isNat(N)), M, N)
   a__plus(X1, X2) -> plus(X1, X2)
   mark(U11(X1, X2)) -> a__U11(mark(X1), X2)
   mark(U21(X1, X2, X3)) -> a__U21(mark(X1), X2, X3)
   mark(plus(X1, X2)) -> a__plus(mark(X1), mark(X2))
   mark(and(X1, X2)) -> a__and(mark(X1), X2)
   mark(isNat(X)) -> a__isNat(X)
   mark(tt) -> tt
   mark(s(X)) -> s(mark(X))
   mark(0) -> 0
   
    the pairs 
   a__U21#(tt, M, N) -> a__plus#(mark(N), mark(M))
   a__plus#(N, s(M)) -> a__U21#(a__and(a__isNat(M), isNat(N)), M, N)
   
   could not apply the generic root reduction pair processor with the following
   SCNP-version with mu = MS and the level mapping defined by 
   pi(a__plus#) = [(epsilon,0),(1,0),(2,0)]
   pi(a__U21#) = [(epsilon,0),(2,3),(3,0)]
   Argument Filter: 
   pi(a__plus#/2) = 2
   pi(s/1) = [1]
   pi(a__U21#/3) = []
   pi(a__and/2) = [2]
   pi(a__isNat/1) = [1]
   pi(isNat/1) = [1]
   pi(tt/0) = []
   pi(mark/1) = 1
   pi(0/0) = []
   pi(U11/2) = [1,2]
   pi(a__U11/2) = [1,2]
   pi(plus/2) = [1,2]
   pi(a__plus/2) = [1,2]
   pi(and/2) = [2]
   pi(U21/3) = [3,2,1]
   pi(a__U21/3) = [3,2,1]
   
   RPO with the following precedence
   precedence(s[1]) = 1
   precedence(a__U21#[3]) = 1
   precedence(a__and[2]) = 2
   precedence(a__isNat[1]) = 3
   precedence(isNat[1]) = 3
   precedence(tt[0]) = 4
   precedence(0[0]) = 4
   precedence(U11[2]) = 0
   precedence(a__U11[2]) = 0
   precedence(plus[2]) = 3
   precedence(a__plus[2]) = 3
   precedence(and[2]) = 2
   precedence(U21[3]) = 3
   precedence(a__U21[3]) = 3
   
   precedence(_) = 0
   and the following status
   status(s[1]) = mul
   status(a__U21#[3]) = mul
   status(a__and[2]) = lex
   status(a__isNat[1]) = lex
   status(isNat[1]) = lex
   status(tt[0]) = mul
   status(0[0]) = mul
   status(U11[2]) = mul
   status(a__U11[2]) = mul
   status(plus[2]) = lex
   status(a__plus[2]) = lex
   status(and[2]) = lex
   status(U21[3]) = lex
   status(a__U21[3]) = lex
   
   status(_) = lex
   
   problem when orienting DPs
   cannot orient pair a__U21#(tt, M, N) -> a__plus#(mark(N), mark(M)) strictly:
   [(a__U21#(tt, M, N),0),(M,3),(N,0)] >mu [(a__plus#(mark(N), mark(M)),0),(mark(N),0),(mark(M),0)] could not be ensured