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:
 
 g#(f(x, y), z) -> g#(y, z)
 g#(h(x, y), z) -> g#(x, f(y, z))
 g#(x, h(y, z)) -> g#(x, y)
 rules:
 
 g(f(x, y), z) -> f(x, g(y, z))
 g(h(x, y), z) -> g(x, f(y, z))
 g(x, h(y, z)) -> h(g(x, y), z)
 
  the pairs 
 g#(h(x, y), z) -> g#(x, f(y, z))
 g#(x, h(y, z)) -> g#(x, y)
 
 could not apply the generic root reduction pair processor with the following
 SCNP-version with mu = MS and the level mapping defined by 
 pi(g#) = [(epsilon,0),(1,2),(2,0)]
 Argument Filter: 
 pi(g#/2) = 2
 pi(f/2) = 2
 pi(h/2) = [1,2]
 
 RPO with the following precedence
 precedence(h[2]) = 0
 
 precedence(_) = 0
 and the following status
 status(h[2]) = lex
 
 status(_) = lex
 
 problem when orienting DPs
 cannot orient pair g#(f(x, y), z) -> g#(y, z) weakly:
 [(g#(f(x, y), z),0),(f(x, y),2),(z,0)] >=mu [(g#(y, z),0),(y,2),(z,0)] could not be ensured