ceta_eq: termination proof not accepted
1: error below switch to dependency pairs
1.1: error below the dependency graph processor
 1.1.3: error below the reduction pair processor
  1.1.3.1: error below the reduction pair processor
   1.1.3.1.1: error when applying the reduction pair processor with usable rules to remove from the DP problem
    pairs:
    
    proper#(f(X)) -> proper#(X)
    proper#(d(X)) -> proper#(X)
    proper#(h(X)) -> proper#(X)
    rules:
    
    active(f(f(X))) -> mark(c(f(g(f(X)))))
    active(c(X)) -> mark(d(X))
    active(h(X)) -> mark(c(d(X)))
    active(f(X)) -> f(active(X))
    active(h(X)) -> h(active(X))
    c(ok(X)) -> ok(c(X))
    d(ok(X)) -> ok(d(X))
    f(mark(X)) -> mark(f(X))
    f(ok(X)) -> ok(f(X))
    g(ok(X)) -> ok(g(X))
    h(mark(X)) -> mark(h(X))
    h(ok(X)) -> ok(h(X))
    proper(f(X)) -> f(proper(X))
    proper(c(X)) -> c(proper(X))
    proper(g(X)) -> g(proper(X))
    proper(d(X)) -> d(proper(X))
    proper(h(X)) -> h(proper(X))
    top(mark(X)) -> top(proper(X))
    top(ok(X)) -> top(active(X))
    
     the pairs 
    proper#(d(X)) -> proper#(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(proper#) = [(epsilon,0),(1,0)]
    Argument Filter: 
    pi(proper#/1) = []
    pi(f/1) = 1
    pi(d/1) = [1]
    pi(h/1) = 1
    
    RPO with the following precedence
    precedence(proper#[1]) = 0
    precedence(d[1]) = 1
    
    precedence(_) = 0
    and the following status
    status(proper#[1]) = lex
    status(d[1]) = lex
    
    status(_) = lex
    
    problem when orienting DPs
    cannot orient pair proper#(f(X)) -> proper#(X) weakly:
    [(proper#(f(X)),0),(f(X),0)] >=mu [(proper#(X),0),(X,0)] could not be ensured