MAYBE
Time: 26.212616
TRS:
 { 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),
                                     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))}
 DP:
  DP:
   { app#(app(app(filtersub(), true()), f), app(app(cons(), y), ys)) -> app#(app(filter(), f), 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(), true()), f), app(app(cons(), y), ys)) -> app#(filter(), f),
    app#(app(app(filtersub(), false()), f), app(app(cons(), y), ys)) -> app#(app(filter(), f), ys),
    app#(app(app(filtersub(), false()), f), app(app(cons(), y), ys)) -> app#(filter(), f),
                     app#(app(filter(), f), app(app(cons(), y), ys)) -> app#(f, y),
                     app#(app(filter(), f), app(app(cons(), y), ys)) -> app#(app(app(filtersub(), app(f, y)), f), app(app(cons(), y), ys)),
                     app#(app(filter(), f), app(app(cons(), y), ys)) -> app#(app(filtersub(), app(f, y)), f),
                     app#(app(filter(), f), app(app(cons(), y), ys)) -> app#(filtersub(), app(f, y))}
  TRS:
  { 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),
                                      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))}
  UR:
   { 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),
                                       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)),
                                                            a(x, z) -> x,
                                                            a(x, z) -> z}
   EDG:
    {(app#(app(app(filtersub(), false()), f), app(app(cons(), y), ys)) -> app#(app(filter(), f), ys), app#(app(filter(), f), app(app(cons(), y), ys)) -> app#(filtersub(), app(f, y)))
     (app#(app(app(filtersub(), false()), f), app(app(cons(), y), ys)) -> app#(app(filter(), f), ys), app#(app(filter(), f), app(app(cons(), y), ys)) -> app#(app(filtersub(), app(f, y)), f))
     (app#(app(app(filtersub(), false()), f), app(app(cons(), y), ys)) -> app#(app(filter(), f), ys), 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(), false()), f), app(app(cons(), y), ys)) -> app#(app(filter(), f), ys), app#(app(filter(), f), app(app(cons(), y), ys)) -> app#(f, y))
     (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(), false()), f), app(app(cons(), y), ys)) -> app#(filter(), f))
     (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(), false()), f), app(app(cons(), y), ys)) -> app#(app(filter(), f), ys))
     (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#(filter(), f))
     (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(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(filter(), f), app(app(cons(), y), ys)) -> app#(f, y), app#(app(app(filtersub(), true()), f), app(app(cons(), y), ys)) -> app#(app(filter(), f), ys))
     (app#(app(filter(), f), app(app(cons(), y), ys)) -> app#(f, y), app#(app(app(filtersub(), true()), f), app(app(cons(), y), ys)) -> app#(app(cons(), y), app(app(filter(), f), ys)))
     (app#(app(filter(), f), app(app(cons(), y), ys)) -> app#(f, y), app#(app(app(filtersub(), true()), f), app(app(cons(), y), ys)) -> app#(filter(), f))
     (app#(app(filter(), f), app(app(cons(), y), ys)) -> app#(f, y), app#(app(app(filtersub(), false()), f), app(app(cons(), y), ys)) -> app#(app(filter(), f), ys))
     (app#(app(filter(), f), app(app(cons(), y), ys)) -> app#(f, y), app#(app(app(filtersub(), false()), f), app(app(cons(), y), ys)) -> app#(filter(), f))
     (app#(app(filter(), f), app(app(cons(), y), ys)) -> app#(f, y), app#(app(filter(), f), app(app(cons(), y), ys)) -> app#(f, y))
     (app#(app(filter(), f), app(app(cons(), y), ys)) -> app#(f, y), app#(app(filter(), f), app(app(cons(), y), ys)) -> app#(app(app(filtersub(), app(f, y)), f), app(app(cons(), y), ys)))
     (app#(app(filter(), f), app(app(cons(), y), ys)) -> app#(f, y), app#(app(filter(), f), app(app(cons(), y), ys)) -> app#(app(filtersub(), app(f, y)), f))
     (app#(app(filter(), f), app(app(cons(), y), ys)) -> app#(f, y), app#(app(filter(), f), app(app(cons(), y), ys)) -> app#(filtersub(), app(f, y)))
     (app#(app(app(filtersub(), true()), f), app(app(cons(), y), ys)) -> app#(app(filter(), f), ys), app#(app(filter(), f), app(app(cons(), y), ys)) -> app#(f, y))
     (app#(app(app(filtersub(), true()), f), app(app(cons(), y), ys)) -> app#(app(filter(), f), ys), 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(filter(), f), app(app(cons(), y), ys)) -> app#(app(filtersub(), app(f, y)), f))
     (app#(app(app(filtersub(), true()), f), app(app(cons(), y), ys)) -> app#(app(filter(), f), ys), app#(app(filter(), f), app(app(cons(), y), ys)) -> app#(filtersub(), app(f, y)))}
    STATUS:
     arrows: 0.728395
     SCCS (1):
      Scc:
       { 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),
                         app#(app(filter(), f), app(app(cons(), y), ys)) -> app#(f, y),
                         app#(app(filter(), f), app(app(cons(), y), ys)) -> app#(app(app(filtersub(), app(f, y)), f), app(app(cons(), y), ys))}
      
      SCC (4):
       Strict:
        { 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),
                          app#(app(filter(), f), app(app(cons(), y), ys)) -> app#(f, y),
                          app#(app(filter(), f), app(app(cons(), y), ys)) -> app#(app(app(filtersub(), app(f, y)), f), app(app(cons(), y), ys))}
       Weak:
       { 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),
                                           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))}
       Open