ceta_eq: termination proof not accepted
1: error below switch to dependency pairs
1.1: error below the dependency graph processor
 1.1.2: error when applying the reduction pair processor with usable rules to remove from the DP problem
  pairs:
  
  __#(mark(X1), X2) -> __#(X1, X2)
  __#(X1, mark(X2)) -> __#(X1, X2)
  __#(active(X1), X2) -> __#(X1, X2)
  __#(X1, active(X2)) -> __#(X1, X2)
  rules:
  
  U11(mark(X)) -> U11(X)
  U11(active(X)) -> U11(X)
  U12(mark(X)) -> U12(X)
  U12(active(X)) -> U12(X)
  __(mark(X1), X2) -> __(X1, X2)
  __(X1, mark(X2)) -> __(X1, X2)
  __(active(X1), X2) -> __(X1, X2)
  __(X1, active(X2)) -> __(X1, X2)
  active(__(__(X, Y), Z)) -> mark(__(X, __(Y, Z)))
  active(__(X, nil)) -> mark(X)
  active(__(nil, X)) -> mark(X)
  active(U11(tt)) -> mark(U12(tt))
  active(U12(tt)) -> mark(tt)
  active(isNePal(__(I, __(P, I)))) -> mark(U11(tt))
  isNePal(mark(X)) -> isNePal(X)
  isNePal(active(X)) -> isNePal(X)
  mark(__(X1, X2)) -> active(__(mark(X1), mark(X2)))
  mark(nil) -> active(nil)
  mark(U11(X)) -> active(U11(mark(X)))
  mark(tt) -> active(tt)
  mark(U12(X)) -> active(U12(mark(X)))
  mark(isNePal(X)) -> active(isNePal(mark(X)))
  
   the pairs 
  __#(active(X1), X2) -> __#(X1, X2)
  
  could not apply the generic root reduction pair processor with the following
  SCNP-version with mu = MS and the level mapping defined by 
  pi(__#) = [(epsilon,0),(1,1)]
  Argument Filter: 
  pi(__#/2) = []
  pi(mark/1) = 1
  pi(active/1) = [1]
  
  RPO with the following precedence
  precedence(__#[2]) = 0
  precedence(active[1]) = 1
  
  precedence(_) = 0
  and the following status
  status(__#[2]) = lex
  status(active[1]) = lex
  
  status(_) = lex
  
  problem when orienting DPs
  cannot orient pair __#(mark(X1), X2) -> __#(X1, X2) weakly:
  [(__#(mark(X1), X2),0),(mark(X1),1)] >=mu [(__#(X1, X2),0),(X1,1)] could not be ensured