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)
  rules:
  
  +(p1, p1) -> p2
  +(p1, +(p2, p2)) -> p5
  +(p5, p5) -> p10
  +(+(x, y), z) -> +(x, +(y, z))
  +(p1, +(p1, x)) -> +(p2, x)
  +(p1, +(p2, +(p2, x))) -> +(p5, x)
  +(p2, p1) -> +(p1, p2)
  +(p2, +(p1, x)) -> +(p1, +(p2, x))
  +(p2, +(p2, p2)) -> +(p1, p5)
  +(p2, +(p2, +(p2, x))) -> +(p1, +(p5, x))
  +(p5, p1) -> +(p1, p5)
  +(p5, +(p1, x)) -> +(p1, +(p5, x))
  +(p5, p2) -> +(p2, p5)
  +(p5, +(p2, x)) -> +(p2, +(p5, x))
  +(p5, +(p5, x)) -> +(p10, x)
  +(p10, p1) -> +(p1, p10)
  +(p10, +(p1, x)) -> +(p1, +(p10, x))
  +(p10, p2) -> +(p2, p10)
  +(p10, +(p2, x)) -> +(p2, +(p10, x))
  +(p10, p5) -> +(p5, p10)
  +(p10, +(p5, x)) -> +(p5, +(p10, x))
  
   the pairs 
  +#(+(x, y), z) -> +#(x, +(y, 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,0)]
  Argument Filter: 
  pi(+#/2) = []
  pi(+/2) = [2,1]
  pi(p1/0) = []
  pi(p2/0) = []
  pi(p5/0) = []
  pi(p10/0) = []
  
  RPO with the following precedence
  precedence(+#[2]) = 1
  precedence(+[2]) = 0
  precedence(p1[0]) = 2
  precedence(p2[0]) = 2
  precedence(p5[0]) = 3
  precedence(p10[0]) = 3
  
  precedence(_) = 0
  and the following status
  status(+#[2]) = lex
  status(+[2]) = lex
  status(p1[0]) = lex
  status(p2[0]) = lex
  status(p5[0]) = lex
  status(p10[0]) = lex
  
  status(_) = lex
  
  problem when orienting DPs
  cannot orient pair +#(+(x, y), z) -> +#(x, +(y, z)) strictly:
  [(+#(+(x, y), z),0),(+(x, y),0)] >mu [(+#(x, +(y, z)),0),(x,0)] could not be ensured