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 when applying the reduction pair processor with usable rules to remove from the DP problem
   pairs:
   
   b#(y, z) -> c#(y, z, z)
   c#(f(z), f(c(a, x, a)), y) -> b#(x, z)
   c#(f(z), f(c(a, x, a)), y) -> c#(z, y, a)
   rules:
   
   b(y, z) -> f(c(c(y, z, z), a, a))
   b(b(z, y), a) -> z
   c(f(z), f(c(a, x, a)), y) -> c(f(b(x, z)), c(z, y, a), a)
   
    the pairs 
   b#(y, z) -> c#(y, z, z)
   c#(f(z), f(c(a, x, a)), y) -> b#(x, z)
   c#(f(z), f(c(a, x, a)), y) -> c#(z, y, a)
   
   could not apply the generic root reduction pair processor with the following
   SCNP-version with mu = MS and the level mapping defined by 
   pi(b#) = [(1,4),(2,4)]
   pi(c#) = [(epsilon,0),(1,4),(3,3)]
   Argument Filter: 
   pi(b#/2) = 2
   pi(c#/3) = 2
   pi(f/1) = 1
   pi(c/3) = [1,3,2]
   pi(a/0) = []
   
   RPO with the following precedence
   precedence(c[3]) = 0
   precedence(a[0]) = 0
   
   precedence(_) = 0
   and the following status
   status(c[3]) = lex
   status(a[0]) = lex
   
   status(_) = lex
   
   problem when orienting DPs
   cannot orient pair c#(f(z), f(c(a, x, a)), y) -> b#(x, z) strictly:
   [(c#(f(z), f(c(a, x, a)), y),0),(f(z),4),(y,3)] >mu [(x,4),(z,4)] could not be ensured