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