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 when applying the reduction pair processor with usable rules to remove from the DP problem
  pairs:
  
  app#(app(and, x), app(app(or, y), z)) -> app#(app(and, x), y)
  app#(app(and, x), app(app(or, y), z)) -> app#(app(and, x), z)
  app#(app(and, app(app(or, y), z)), x) -> app#(app(and, x), y)
  app#(app(and, app(app(or, y), z)), x) -> app#(app(and, x), z)
  rules:
  
  app(not, app(not, x)) -> x
  app(not, app(app(or, x), y)) -> app(app(and, app(not, x)), app(not, y))
  app(not, app(app(and, x), y)) -> app(app(or, app(not, x)), app(not, y))
  app(app(and, x), app(app(or, y), z)) -> app(app(or, app(app(and, x), y)), app(app(and, x), z))
  app(app(and, app(app(or, y), z)), x) -> app(app(or, app(app(and, x), y)), app(app(and, x), z))
  app(app(map, f), nil) -> nil
  app(app(map, f), app(app(cons, x), xs)) -> app(app(cons, app(f, x)), app(app(map, f), xs))
  app(app(filter, f), nil) -> nil
  app(app(filter, f), app(app(cons, x), xs)) -> app(app(app(app(filter2, app(f, x)), f), x), xs)
  app(app(app(app(filter2, true), f), x), xs) -> app(app(cons, x), app(app(filter, f), xs))
  app(app(app(app(filter2, false), f), x), xs) -> app(app(filter, f), xs)
  
   the pairs 
  app#(app(and, x), app(app(or, y), z)) -> app#(app(and, x), y)
  app#(app(and, x), app(app(or, y), z)) -> app#(app(and, x), z)
  app#(app(and, app(app(or, y), z)), x) -> app#(app(and, x), y)
  app#(app(and, app(app(or, y), z)), x) -> app#(app(and, x), z)
  
  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#) = [(1,0),(2,0)]
  polynomial interpretration over naturals with negative constants
  Pol(app#(x_1, x_2)) = 1
  Pol(app(x_1, x_2)) = x_2 + x_1
  Pol(and) = 0
  Pol(or) = 1
  problem when orienting DPs
  cannot orient pair app#(app(and, app(app(or, y), z)), x) -> app#(app(and, x), y) strictly:
  [(app(and, app(app(or, y), z)),0),(x,0)] >mu [(app(and, x),0),(y,0)] could not be ensured