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 when applying the reduction pair processor to remove from the DP problem
  pairs:
  
  active#(f(a, X, X)) -> mark#(f(X, b, b))
  mark#(f(X1, X2, X3)) -> active#(f(X1, mark(X2), X3))
  mark#(f(X1, X2, X3)) -> mark#(X2)
  rules:
  
  active(f(a, X, X)) -> mark(f(X, b, b))
  active(b) -> mark(a)
  f(mark(X1), X2, X3) -> f(X1, X2, X3)
  f(X1, mark(X2), X3) -> f(X1, X2, X3)
  f(X1, X2, mark(X3)) -> f(X1, X2, X3)
  f(active(X1), X2, X3) -> f(X1, X2, X3)
  f(X1, active(X2), X3) -> f(X1, X2, X3)
  f(X1, X2, active(X3)) -> f(X1, X2, X3)
  mark(f(X1, X2, X3)) -> active(f(X1, mark(X2), X3))
  mark(a) -> active(a)
  mark(b) -> active(b)
  
   the pairs 
  mark#(f(X1, X2, X3)) -> mark#(X2)
  
  could not apply the generic root reduction pair processor with the following
  SCNP-version with mu = MAX and the level mapping defined by 
  pi(mark#) = [(epsilon,0)]
  pi(active#) = [(epsilon,0)]
  Argument Filter: 
  pi(mark#/1) = 1
  pi(f/3) = [1,2,3]
  pi(active#/1) = 1
  pi(mark/1) = 1
  pi(a/0) = []
  pi(b/0) = []
  pi(active/1) = 1
  
  RPO with the following precedence
  precedence(f[3]) = 1
  precedence(a[0]) = 0
  precedence(b[0]) = 0
  
  precedence(_) = 0
  and the following status
  status(f[3]) = mul
  status(a[0]) = mul
  status(b[0]) = mul
  
  status(_) = lex
  
  problem when orienting (usable) rules
  could not orient active(f(a, X, X)) >= mark(f(X, b, b))
  pi( active(f(a, X, X)) ) = f(a, X, X)
  pi( mark(f(X, b, b)) ) = f(X, b, b)
  could not orient f(a, X, X) >=RPO f(X, b, b)