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 with usable rules to remove from the DP problem
  pairs:
  
  :#(:(x, y), z) -> :#(x, :(y, z))
  :#(:(x, y), z) -> :#(y, z)
  :#(+(x, y), z) -> :#(x, z)
  :#(+(x, y), z) -> :#(y, z)
  rules:
  
  :(:(x, y), z) -> :(x, :(y, z))
  :(+(x, y), z) -> +(:(x, z), :(y, z))
  :(z, +(x, f(y))) -> :(g(z, y), +(x, a))
  
   the pairs 
  :#(:(x, y), z) -> :#(x, :(y, z))
  :#(:(x, y), z) -> :#(y, z)
  :#(+(x, y), z) -> :#(x, z)
  :#(+(x, y), z) -> :#(y, z)
  
  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(:/2) = [1,2]
  pi(+/2) = [2,1]
  pi(f/1) = []
  pi(g/2) = 2
  pi(a/0) = []
  
  RPO with the following precedence
  precedence(:#[2]) = 1
  precedence(:[2]) = 0
  precedence(+[2]) = 2
  precedence(f[1]) = 0
  precedence(a[0]) = 3
  
  precedence(_) = 0
  and the following status
  status(:#[2]) = lex
  status(:[2]) = lex
  status(+[2]) = lex
  status(f[1]) = lex
  status(a[0]) = lex
  
  status(_) = lex
  
  problem when orienting DPs
  cannot orient pair :#(:(x, y), z) -> :#(x, :(y, z)) strictly:
  [(:#(:(x, y), z),0),(:(x, y),1)] >mu [(:#(x, :(y, z)),0),(x,1)] could not be ensured