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__U11#(tt, M, N) -> a__U12#(tt, M, N)
   a__U12#(tt, M, N) -> a__plus#(mark(N), mark(M))
   a__plus#(N, s(M)) -> a__U11#(tt, M, N)
   rules:
   
   a__U11(tt, M, N) -> a__U12(tt, M, N)
   a__U11(X1, X2, X3) -> U11(X1, X2, X3)
   a__U12(tt, M, N) -> s(a__plus(mark(N), mark(M)))
   a__U12(X1, X2, X3) -> U12(X1, X2, X3)
   a__plus(N, 0) -> mark(N)
   a__plus(N, s(M)) -> a__U11(tt, M, N)
   a__plus(X1, X2) -> plus(X1, X2)
   mark(U11(X1, X2, X3)) -> a__U11(mark(X1), X2, X3)
   mark(U12(X1, X2, X3)) -> a__U12(mark(X1), X2, X3)
   mark(plus(X1, X2)) -> a__plus(mark(X1), mark(X2))
   mark(tt) -> tt
   mark(s(X)) -> s(mark(X))
   mark(0) -> 0
   
    the pairs 
   a__U11#(tt, M, N) -> a__U12#(tt, M, N)
   a__plus#(N, s(M)) -> a__U11#(tt, 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__U12#) = [(epsilon,0),(2,1)]
   pi(a__plus#) = [(epsilon,0),(2,1)]
   pi(a__U11#) = [(2,14),(3,0)]
   Argument Filter: 
   pi(a__U12#/3) = 3
   pi(tt/0) = []
   pi(a__plus#/2) = 1
   pi(mark/1) = 1
   pi(s/1) = [1]
   pi(a__U11#/3) = 2
   pi(U11/3) = [3,2,1]
   pi(a__U11/3) = [3,2,1]
   pi(U12/3) = [3,2,1]
   pi(a__U12/3) = [3,2,1]
   pi(a__plus/2) = [1,2]
   pi(0/0) = []
   pi(plus/2) = [1,2]
   
   RPO with the following precedence
   precedence(tt[0]) = 1
   precedence(s[1]) = 0
   precedence(U11[3]) = 2
   precedence(a__U11[3]) = 2
   precedence(U12[3]) = 2
   precedence(a__U12[3]) = 2
   precedence(a__plus[2]) = 2
   precedence(0[0]) = 3
   precedence(plus[2]) = 2
   
   precedence(_) = 0
   and the following status
   status(tt[0]) = lex
   status(s[1]) = lex
   status(U11[3]) = lex
   status(a__U11[3]) = lex
   status(U12[3]) = lex
   status(a__U12[3]) = lex
   status(a__plus[2]) = lex
   status(0[0]) = lex
   status(plus[2]) = lex
   
   status(_) = lex
   
   problem when orienting DPs
   cannot orient pair a__U12#(tt, M, N) -> a__plus#(mark(N), mark(M)) weakly:
   [(a__U12#(tt, M, N),0),(M,1)] >=mu [(a__plus#(mark(N), mark(M)),0),(mark(M),1)] could not be ensured