ceta_eq: termination proof not accepted
1: error below switch to dependency pairs
1.1: error when applying the reduction pair processor to remove from the DP problem
 pairs:
 
 a#(a(x)) -> b#(b(x))
 a#(a(x)) -> b#(x)
 b#(b(a(x))) -> a#(b(b(x)))
 b#(b(a(x))) -> b#(b(x))
 b#(b(a(x))) -> b#(x)
 rules:
 
 a(a(x)) -> b(b(x))
 b(b(a(x))) -> a(b(b(x)))
 
  the pairs 
 a#(a(x)) -> b#(x)
 b#(b(a(x))) -> b#(b(x))
 b#(b(a(x))) -> b#(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(a#) = [(epsilon,0),(1,2)]
 pi(b#) = [(epsilon,0),(1,2)]
 Argument Filter: 
 pi(a#/1) = []
 pi(a/1) = [1]
 pi(b#/1) = []
 pi(b/1) = [1]
 
 RPO with the following precedence
 precedence(a#[1]) = 0
 precedence(a[1]) = 0
 precedence(b#[1]) = 0
 precedence(b[1]) = 0
 
 precedence(_) = 0
 and the following status
 status(a#[1]) = lex
 status(a[1]) = lex
 status(b#[1]) = lex
 status(b[1]) = lex
 
 status(_) = lex
 
 problem when orienting DPs
 cannot orient pair a#(a(x)) -> b#(b(x)) weakly:
 [(a#(a(x)),0),(a(x),2)] >=mu [(b#(b(x)),0),(b(x),2)] could not be ensured