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