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