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:
 
 append#(l1, l2) -> ifappend#(l1, l2, l1)
 ifappend#(l1, l2, cons(x, l)) -> append#(l, l2)
 rules:
 
 append(l1, l2) -> ifappend(l1, l2, l1)
 hd(cons(x, l)) -> x
 ifappend(l1, l2, nil) -> l2
 ifappend(l1, l2, cons(x, l)) -> cons(x, append(l, l2))
 is_empty(nil) -> true
 is_empty(cons(x, l)) -> false
 tl(cons(x, l)) -> l
 
  the pairs 
 append#(l1, l2) -> ifappend#(l1, l2, l1)
 ifappend#(l1, l2, cons(x, l)) -> append#(l, l2)
 
 could not apply the generic root reduction pair processor with the following
 SCNP-version with mu = MS and the level mapping defined by 
 pi(append#) = [(1,5),(2,0)]
 pi(ifappend#) = [(epsilon,0),(1,4),(3,1)]
 Argument Filter: 
 pi(append#/2) = [1]
 pi(ifappend#/3) = 2
 pi(cons/2) = [1,2]
 
 RPO with the following precedence
 precedence(cons[2]) = 0
 precedence(append#[2]) = 1
 
 precedence(_) = 0
 and the following status
 status(cons[2]) = lex
 status(append#[2]) = lex
 
 status(_) = lex
 
 problem when orienting DPs
 cannot orient pair append#(l1, l2) -> ifappend#(l1, l2, l1) strictly:
 [(l1,5),(l2,0)] >mu [(ifappend#(l1, l2, l1),0),(l1,4),(l1,1)] could not be ensured