MAYBE Time: 0.006817 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(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(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#(app(filter(), f), ys)) (app#(app(app(filtersub(), false()), f), app(app(cons(), y), ys)) -> 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(), 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(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(filter(), f), app(app(cons(), y), ys)) -> app#(filtersub(), 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#(app(filtersub(), app(f, y)), f)) (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#(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#(f, y)) (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#(filter(), f)) (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(filtersub(), app(f, y)), f), 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(filtersub(), app(f, y)), f), 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(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#(app(app(filtersub(), app(f, y)), f), app(app(cons(), y), ys)), app#(app(filter(), f), app(app(cons(), y), ys)) -> app#(filtersub(), 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#(app(app(filtersub(), app(f, y)), f), app(app(cons(), y), 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(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(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(app(filtersub(), true()), f), app(app(cons(), y), ys)) -> app#(filter(), f), 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#(filter(), f), 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#(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#(filter(), f), 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(app(filtersub(), false()), f), app(app(cons(), y), ys)) -> app#(filter(), f)) (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(), true()), f), app(app(cons(), y), ys)) -> app#(filter(), f), app#(app(app(filtersub(), true()), f), app(app(cons(), y), ys)) -> app#(filter(), f)) (app#(app(app(filtersub(), true()), f), app(app(cons(), y), ys)) -> app#(filter(), f), 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(), true()), 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(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#(filter(), f), 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#(filter(), f), 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#(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(app(filtersub(), false()), f), app(app(cons(), y), ys)) -> app#(filter(), f)) (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(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#(filter(), f), 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#(filter(), f), app#(app(filter(), f), app(app(cons(), y), ys)) -> app#(filtersub(), 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#(filtersub(), 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#(filtersub(), 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#(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#(filtersub(), 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#(filtersub(), 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#(filtersub(), 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#(filtersub(), 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#(filtersub(), 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(cons(), y), app(app(filter(), f), ys)), 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#(app(cons(), y), 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(), 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(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#(filter(), f)) (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#(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(cons(), y), 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(cons(), y), app(app(filter(), f), ys)), app#(app(filter(), f), app(app(cons(), y), ys)) -> app#(filtersub(), app(f, y))) (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(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(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#(app(filter(), f), ys), app#(app(app(filtersub(), true()), f), app(app(cons(), y), ys)) -> app#(filter(), f)) (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(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#(filter(), 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#(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.000000 SCCS (1): Scc: { 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))} SCC (9): Strict: { 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))} 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