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