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 reduction pair processor
     1.1.1.1.2.1.1: error when applying the reduction pair processor with usable rules to remove from the DP problem
      pairs:
      
      mark#(U12(X)) -> mark#(X)
      mark#(U21(X)) -> mark#(X)
      mark#(U32(X)) -> mark#(X)
      rules:
      
      a__U11(tt, V2) -> a__U12(a__isNat(V2))
      a__U11(X1, X2) -> U11(X1, X2)
      a__U12(tt) -> tt
      a__U12(X) -> U12(X)
      a__U21(tt) -> tt
      a__U21(X) -> U21(X)
      a__U31(tt, V2) -> a__U32(a__isNat(V2))
      a__U31(X1, X2) -> U31(X1, X2)
      a__U32(tt) -> tt
      a__U32(X) -> U32(X)
      a__U41(tt, N) -> mark(N)
      a__U41(X1, X2) -> U41(X1, X2)
      a__U51(tt, M, N) -> a__U52(a__isNat(N), M, N)
      a__U51(X1, X2, X3) -> U51(X1, X2, X3)
      a__U52(tt, M, N) -> s(a__plus(mark(N), mark(M)))
      a__U52(X1, X2, X3) -> U52(X1, X2, X3)
      a__U61(tt) -> 0
      a__U61(X) -> U61(X)
      a__U71(tt, M, N) -> a__U72(a__isNat(N), M, N)
      a__U71(X1, X2, X3) -> U71(X1, X2, X3)
      a__U72(tt, M, N) -> a__plus(a__x(mark(N), mark(M)), mark(N))
      a__U72(X1, X2, X3) -> U72(X1, X2, X3)
      a__isNat(0) -> tt
      a__isNat(plus(V1, V2)) -> a__U11(a__isNat(V1), V2)
      a__isNat(s(V1)) -> a__U21(a__isNat(V1))
      a__isNat(x(V1, V2)) -> a__U31(a__isNat(V1), V2)
      a__isNat(X) -> isNat(X)
      a__plus(N, 0) -> a__U41(a__isNat(N), N)
      a__plus(N, s(M)) -> a__U51(a__isNat(M), M, N)
      a__plus(X1, X2) -> plus(X1, X2)
      a__x(N, 0) -> a__U61(a__isNat(N))
      a__x(N, s(M)) -> a__U71(a__isNat(M), M, N)
      a__x(X1, X2) -> x(X1, X2)
      mark(U11(X1, X2)) -> a__U11(mark(X1), X2)
      mark(U12(X)) -> a__U12(mark(X))
      mark(isNat(X)) -> a__isNat(X)
      mark(U21(X)) -> a__U21(mark(X))
      mark(U31(X1, X2)) -> a__U31(mark(X1), X2)
      mark(U32(X)) -> a__U32(mark(X))
      mark(U41(X1, X2)) -> a__U41(mark(X1), X2)
      mark(U51(X1, X2, X3)) -> a__U51(mark(X1), X2, X3)
      mark(U52(X1, X2, X3)) -> a__U52(mark(X1), X2, X3)
      mark(plus(X1, X2)) -> a__plus(mark(X1), mark(X2))
      mark(U61(X)) -> a__U61(mark(X))
      mark(U71(X1, X2, X3)) -> a__U71(mark(X1), X2, X3)
      mark(U72(X1, X2, X3)) -> a__U72(mark(X1), X2, X3)
      mark(x(X1, X2)) -> a__x(mark(X1), mark(X2))
      mark(tt) -> tt
      mark(s(X)) -> s(mark(X))
      mark(0) -> 0
      
       the pairs 
      mark#(U21(X)) -> mark#(X)
      
      could not apply the generic root reduction pair processor with the following
      SCNP-version with mu = MS and the level mapping defined by 
      pi(mark#) = [(epsilon,0),(1,0)]
      Argument Filter: 
      pi(mark#/1) = []
      pi(U12/1) = 1
      pi(U21/1) = [1]
      pi(U32/1) = 1
      
      RPO with the following precedence
      precedence(mark#[1]) = 0
      precedence(U21[1]) = 1
      
      precedence(_) = 0
      and the following status
      status(mark#[1]) = lex
      status(U21[1]) = lex
      
      status(_) = lex
      
      problem when orienting DPs
      cannot orient pair mark#(U12(X)) -> mark#(X) weakly:
      [(mark#(U12(X)),0),(U12(X),0)] >=mu [(mark#(X),0),(X,0)] could not be ensured