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 when applying the reduction pair processor with usable rules to remove from the DP problem
   pairs:
   
   app#(app(filter, f), app(app(cons, y), ys)) -> app#(app(app(filtersub, app(f, y)), f), app(app(cons, y), ys))
   app#(app(app(filtersub, true), f), app(app(cons, y), ys)) -> app#(app(filter, f), ys)
   app#(app(app(filtersub, false), f), app(app(cons, y), ys)) -> app#(app(filter, f), ys)
   rules:
   
   app(app(neq, 0), 0) -> false
   app(app(neq, 0), app(s, y)) -> true
   app(app(neq, app(s, x)), 0) -> true
   app(app(neq, app(s, x)), app(s, y)) -> app(app(neq, x), y)
   app(app(filter, f), nil) -> nil
   app(app(filter, f), app(app(cons, y), ys)) -> app(app(app(filtersub, app(f, y)), f), app(app(cons, y), ys))
   app(app(app(filtersub, true), f), app(app(cons, y), ys)) -> app(app(cons, y), app(app(filter, f), ys))
   app(app(app(filtersub, false), f), app(app(cons, y), ys)) -> app(app(filter, f), ys)
   nonzero -> app(filter, app(neq, 0))
   
    the pairs 
   app#(app(app(filtersub, true), f), app(app(cons, y), ys)) -> app#(app(filter, f), ys)
   app#(app(app(filtersub, false), f), app(app(cons, y), ys)) -> app#(app(filter, f), ys)
   
   could not apply the generic root reduction pair processor with the following
   SCNP-version with mu = MS and the level mapping defined by 
   pi(app#) = [(epsilon,0),(1,0)]
   Argument Filter: 
   pi(app#/2) = [2]
   pi(app/2) = [2]
   pi(filter/0) = []
   pi(cons/0) = []
   pi(filtersub/0) = []
   pi(true/0) = []
   pi(false/0) = []
   pi(neq/0) = []
   pi(0/0) = []
   pi(s/0) = []
   pi(nil/0) = []
   
   RPO with the following precedence
   precedence(app#[2]) = 3
   precedence(app[2]) = 3
   precedence(filter[0]) = 2
   precedence(cons[0]) = 4
   precedence(filtersub[0]) = 0
   precedence(true[0]) = 2
   precedence(false[0]) = 1
   precedence(neq[0]) = 2
   precedence(0[0]) = 5
   precedence(s[0]) = 3
   precedence(nil[0]) = 6
   
   precedence(_) = 0
   and the following status
   status(app#[2]) = lex
   status(app[2]) = lex
   status(filter[0]) = lex
   status(cons[0]) = lex
   status(filtersub[0]) = lex
   status(true[0]) = lex
   status(false[0]) = lex
   status(neq[0]) = lex
   status(0[0]) = lex
   status(s[0]) = lex
   status(nil[0]) = lex
   
   status(_) = lex
   
   problem when orienting DPs
   cannot orient pair app#(app(filter, f), app(app(cons, y), ys)) -> app#(app(app(filtersub, app(f, y)), f), app(app(cons, y), ys)) weakly:
   [(app#(app(filter, f), app(app(cons, y), ys)),0),(app(filter, f),0)] >=mu [(app#(app(app(filtersub, app(f, y)), f), app(app(cons, y), ys)),0),(app(app(filtersub, app(f, y)), f),0)] could not be ensured