ceta_eq: termination proof not accepted
1: error below switch to dependency pairs
1.1: error below the reduction pair processor
 1.1.1: error below the dependency graph processor
  1.1.1.1: error when applying the reduction pair processor with usable rules to remove from the DP problem
   pairs:
   
   *#(+(x, y), z) -> *#(x, z)
   *#(+(x, y), z) -> *#(y, z)
   rules:
   
   *(x, *(y, z)) -> *(otimes(x, y), z)
   *(1, y) -> y
   *(+(x, y), z) -> oplus(*(x, z), *(y, z))
   *(x, oplus(y, z)) -> oplus(*(x, y), *(x, z))
   
    the pairs 
   *#(+(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,3)]
   Argument Filter: 
   pi(*#/2) = [2]
   pi(+/2) = [2,1]
   
   RPO with the following precedence
   precedence(*#[2]) = 0
   precedence(+[2]) = 0
   
   precedence(_) = 0
   and the following status
   status(*#[2]) = lex
   status(+[2]) = lex
   
   status(_) = lex
   
   problem when orienting DPs
   cannot orient pair *#(+(x, y), z) -> *#(x, z) strictly:
   [(*#(+(x, y), z),0),(+(x, y),3)] >mu [(*#(x, z),0),(x,3)] could not be ensured