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 below the reduction pair processor
  1.1.1.1: error below the reduction pair processor
   1.1.1.1.1: error when applying the reduction pair processor with usable rules to remove from the DP problem
    pairs:
    
    inter#(cons(x, l1), l2) -> ifinter#(mem(x, l2), x, l1, l2)
    ifinter#(true, x, l1, l2) -> inter#(l1, l2)
    ifinter#(false, x, l1, l2) -> inter#(l1, l2)
    rules:
    
    app(nil, l) -> l
    app(cons(x, l1), l2) -> cons(x, app(l1, l2))
    app(app(l1, l2), l3) -> app(l1, app(l2, l3))
    eq(0, 0) -> true
    eq(0, s(x)) -> false
    eq(s(x), 0) -> false
    eq(s(x), s(y)) -> eq(x, y)
    if(true, x, y) -> x
    if(false, x, y) -> y
    ifinter(true, x, l1, l2) -> cons(x, inter(l1, l2))
    ifinter(false, x, l1, l2) -> inter(l1, l2)
    ifmem(true, x, l) -> true
    ifmem(false, x, l) -> mem(x, l)
    inter(x, nil) -> nil
    inter(nil, x) -> nil
    inter(app(l1, l2), l3) -> app(inter(l1, l3), inter(l2, l3))
    inter(l1, app(l2, l3)) -> app(inter(l1, l2), inter(l1, l3))
    inter(cons(x, l1), l2) -> ifinter(mem(x, l2), x, l1, l2)
    inter(l1, cons(x, l2)) -> ifinter(mem(x, l1), x, l2, l1)
    mem(x, nil) -> false
    mem(x, cons(y, l)) -> ifmem(eq(x, y), x, l)
    
     the pairs 
    inter#(cons(x, l1), l2) -> ifinter#(mem(x, l2), x, l1, l2)
    ifinter#(true, x, l1, l2) -> inter#(l1, l2)
    ifinter#(false, x, l1, l2) -> inter#(l1, 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(inter#) = [(epsilon,0),(1,0)]
    pi(ifinter#) = [(2,5),(3,0),(4,0)]
    Argument Filter: 
    pi(inter#/2) = 2
    pi(cons/2) = [1,2]
    pi(ifinter#/4) = [2,3,4]
    pi(mem/2) = 1
    pi(true/0) = []
    pi(false/0) = []
    pi(nil/0) = []
    pi(ifmem/3) = [3]
    pi(eq/2) = 1
    pi(0/0) = []
    pi(s/1) = []
    
    RPO with the following precedence
    precedence(cons[2]) = 0
    precedence(ifinter#[4]) = 1
    precedence(true[0]) = 2
    precedence(ifmem[3]) = 3
    precedence(false[0]) = 4
    precedence(s[1]) = 5
    precedence(0[0]) = 6
    precedence(nil[0]) = 7
    
    precedence(_) = 0
    and the following status
    status(cons[2]) = lex
    status(ifinter#[4]) = lex
    status(true[0]) = lex
    status(ifmem[3]) = lex
    status(false[0]) = lex
    status(s[1]) = lex
    status(0[0]) = lex
    status(nil[0]) = lex
    
    status(_) = lex
    
    problem when orienting DPs
    cannot orient pair inter#(cons(x, l1), l2) -> ifinter#(mem(x, l2), x, l1, l2) strictly:
    [(inter#(cons(x, l1), l2),0),(cons(x, l1),0)] >mu [(x,5),(l1,0),(l2,0)] could not be ensured