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: f#(a, y) -> f#(y, g(y)) rules: f(a, y) -> f(y, g(y)) g(a) -> b g(b) -> b the pairs f#(a, y) -> f#(y, g(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(f#) = [(epsilon,0),(1,0)] Argument Filter: pi(f#/2) = 2 pi(a/0) = [] pi(g/1) = [] pi(b/0) = [] RPO with the following precedence precedence(a[0]) = 1 precedence(g[1]) = 0 precedence(b[0]) = 0 precedence(_) = 0 and the following status status(a[0]) = lex status(g[1]) = lex status(b[0]) = lex status(_) = lex problem when orienting DPs cannot orient pair f#(a, y) -> f#(y, g(y)) strictly: [(f#(a, y),0),(a,0)] >mu [(f#(y, g(y)),0),(y,0)] could not be ensured