MAYBE Time: 35.352597 TRS: { a(a(a(div2(), x), y), 0()) -> a(a(divides(), x), y), a(a(a(div2(), a(s(), x)), y), a(s(), z)) -> a(a(a(div2(), x), y), z), a(a(a(div2(), 0()), y), a(s(), z)) -> false(), a(a(a(if(), true()), x), xs) -> a(a(cons(), x), xs), a(a(a(if(), false()), x), xs) -> xs, a(a(divides(), a(s(), x)), a(s(), y)) -> a(a(a(div2(), x), a(s(), y)), y), a(a(divides(), 0()), a(s(), y)) -> true(), a(a(filter(), f), a(a(cons(), x), xs)) -> a(a(a(if(), a(f, x)), x), a(a(filter(), f), xs)), a(a(filter(), f), nil()) -> nil(), a(a(not(), f), x) -> a(not2(), a(f, x)), a(not2(), true()) -> false(), a(not2(), false()) -> true(), a(sieve(), a(a(cons(), x), xs)) -> a(a(cons(), x), a(sieve(), a(a(filter(), a(not(), a(divides(), x))), xs))), a(sieve(), nil()) -> nil()} DP: DP: { a#(a(a(div2(), x), y), 0()) -> a#(a(divides(), x), y), a#(a(a(div2(), x), y), 0()) -> a#(divides(), x), a#(a(a(div2(), a(s(), x)), y), a(s(), z)) -> a#(a(a(div2(), x), y), z), a#(a(a(div2(), a(s(), x)), y), a(s(), z)) -> a#(a(div2(), x), y), a#(a(a(div2(), a(s(), x)), y), a(s(), z)) -> a#(div2(), x), a#(a(a(if(), true()), x), xs) -> a#(a(cons(), x), xs), a#(a(a(if(), true()), x), xs) -> a#(cons(), x), a#(a(divides(), a(s(), x)), a(s(), y)) -> a#(a(a(div2(), x), a(s(), y)), y), a#(a(divides(), a(s(), x)), a(s(), y)) -> a#(a(div2(), x), a(s(), y)), a#(a(divides(), a(s(), x)), a(s(), y)) -> a#(div2(), x), a#(a(filter(), f), a(a(cons(), x), xs)) -> a#(f, x), a#(a(filter(), f), a(a(cons(), x), xs)) -> a#(a(a(if(), a(f, x)), x), a(a(filter(), f), xs)), a#(a(filter(), f), a(a(cons(), x), xs)) -> a#(a(filter(), f), xs), a#(a(filter(), f), a(a(cons(), x), xs)) -> a#(a(if(), a(f, x)), x), a#(a(filter(), f), a(a(cons(), x), xs)) -> a#(if(), a(f, x)), a#(a(not(), f), x) -> a#(f, x), a#(a(not(), f), x) -> a#(not2(), a(f, x)), a#(sieve(), a(a(cons(), x), xs)) -> a#(a(filter(), a(not(), a(divides(), x))), xs), a#(sieve(), a(a(cons(), x), xs)) -> a#(a(cons(), x), a(sieve(), a(a(filter(), a(not(), a(divides(), x))), xs))), a#(sieve(), a(a(cons(), x), xs)) -> a#(divides(), x), a#(sieve(), a(a(cons(), x), xs)) -> a#(filter(), a(not(), a(divides(), x))), a#(sieve(), a(a(cons(), x), xs)) -> a#(not(), a(divides(), x)), a#(sieve(), a(a(cons(), x), xs)) -> a#(sieve(), a(a(filter(), a(not(), a(divides(), x))), xs))} TRS: { a(a(a(div2(), x), y), 0()) -> a(a(divides(), x), y), a(a(a(div2(), a(s(), x)), y), a(s(), z)) -> a(a(a(div2(), x), y), z), a(a(a(div2(), 0()), y), a(s(), z)) -> false(), a(a(a(if(), true()), x), xs) -> a(a(cons(), x), xs), a(a(a(if(), false()), x), xs) -> xs, a(a(divides(), a(s(), x)), a(s(), y)) -> a(a(a(div2(), x), a(s(), y)), y), a(a(divides(), 0()), a(s(), y)) -> true(), a(a(filter(), f), a(a(cons(), x), xs)) -> a(a(a(if(), a(f, x)), x), a(a(filter(), f), xs)), a(a(filter(), f), nil()) -> nil(), a(a(not(), f), x) -> a(not2(), a(f, x)), a(not2(), true()) -> false(), a(not2(), false()) -> true(), a(sieve(), a(a(cons(), x), xs)) -> a(a(cons(), x), a(sieve(), a(a(filter(), a(not(), a(divides(), x))), xs))), a(sieve(), nil()) -> nil()} UR: { a(a(a(div2(), x), y), 0()) -> a(a(divides(), x), y), a(a(a(div2(), a(s(), x)), y), a(s(), z)) -> a(a(a(div2(), x), y), z), a(a(a(div2(), 0()), y), a(s(), z)) -> false(), a(a(a(if(), true()), x), xs) -> a(a(cons(), x), xs), a(a(a(if(), false()), x), xs) -> xs, a(a(divides(), a(s(), x)), a(s(), y)) -> a(a(a(div2(), x), a(s(), y)), y), a(a(divides(), 0()), a(s(), y)) -> true(), a(a(filter(), f), a(a(cons(), x), xs)) -> a(a(a(if(), a(f, x)), x), a(a(filter(), f), xs)), a(a(filter(), f), nil()) -> nil(), a(a(not(), f), x) -> a(not2(), a(f, x)), a(not2(), true()) -> false(), a(not2(), false()) -> true(), a(sieve(), a(a(cons(), x), xs)) -> a(a(cons(), x), a(sieve(), a(a(filter(), a(not(), a(divides(), x))), xs))), a(sieve(), nil()) -> nil(), b(w, v) -> w, b(w, v) -> v} EDG: {(a#(sieve(), a(a(cons(), x), xs)) -> a#(sieve(), a(a(filter(), a(not(), a(divides(), x))), xs)), a#(sieve(), a(a(cons(), x), xs)) -> a#(sieve(), a(a(filter(), a(not(), a(divides(), x))), xs))) (a#(sieve(), a(a(cons(), x), xs)) -> a#(sieve(), a(a(filter(), a(not(), a(divides(), x))), xs)), a#(sieve(), a(a(cons(), x), xs)) -> a#(not(), a(divides(), x))) (a#(sieve(), a(a(cons(), x), xs)) -> a#(sieve(), a(a(filter(), a(not(), a(divides(), x))), xs)), a#(sieve(), a(a(cons(), x), xs)) -> a#(filter(), a(not(), a(divides(), x)))) (a#(sieve(), a(a(cons(), x), xs)) -> a#(sieve(), a(a(filter(), a(not(), a(divides(), x))), xs)), a#(sieve(), a(a(cons(), x), xs)) -> a#(divides(), x)) (a#(sieve(), a(a(cons(), x), xs)) -> a#(sieve(), a(a(filter(), a(not(), a(divides(), x))), xs)), a#(sieve(), a(a(cons(), x), xs)) -> a#(a(cons(), x), a(sieve(), a(a(filter(), a(not(), a(divides(), x))), xs)))) (a#(sieve(), a(a(cons(), x), xs)) -> a#(sieve(), a(a(filter(), a(not(), a(divides(), x))), xs)), a#(sieve(), a(a(cons(), x), xs)) -> a#(a(filter(), a(not(), a(divides(), x))), xs)) (a#(a(not(), f), x) -> a#(f, x), a#(sieve(), a(a(cons(), x), xs)) -> a#(sieve(), a(a(filter(), a(not(), a(divides(), x))), xs))) (a#(a(not(), f), x) -> a#(f, x), a#(sieve(), a(a(cons(), x), xs)) -> a#(not(), a(divides(), x))) (a#(a(not(), f), x) -> a#(f, x), a#(sieve(), a(a(cons(), x), xs)) -> a#(filter(), a(not(), a(divides(), x)))) (a#(a(not(), f), x) -> a#(f, x), a#(sieve(), a(a(cons(), x), xs)) -> a#(divides(), x)) (a#(a(not(), f), x) -> a#(f, x), a#(sieve(), a(a(cons(), x), xs)) -> a#(a(cons(), x), a(sieve(), a(a(filter(), a(not(), a(divides(), x))), xs)))) (a#(a(not(), f), x) -> a#(f, x), a#(sieve(), a(a(cons(), x), xs)) -> a#(a(filter(), a(not(), a(divides(), x))), xs)) (a#(a(not(), f), x) -> a#(f, x), a#(a(not(), f), x) -> a#(not2(), a(f, x))) (a#(a(not(), f), x) -> a#(f, x), a#(a(not(), f), x) -> a#(f, x)) (a#(a(not(), f), x) -> a#(f, x), a#(a(filter(), f), a(a(cons(), x), xs)) -> a#(if(), a(f, x))) (a#(a(not(), f), x) -> a#(f, x), a#(a(filter(), f), a(a(cons(), x), xs)) -> a#(a(if(), a(f, x)), x)) (a#(a(not(), f), x) -> a#(f, x), a#(a(filter(), f), a(a(cons(), x), xs)) -> a#(a(filter(), f), xs)) (a#(a(not(), f), x) -> a#(f, x), a#(a(filter(), f), a(a(cons(), x), xs)) -> a#(a(a(if(), a(f, x)), x), a(a(filter(), f), xs))) (a#(a(not(), f), x) -> a#(f, x), a#(a(filter(), f), a(a(cons(), x), xs)) -> a#(f, x)) (a#(a(not(), f), x) -> a#(f, x), a#(a(divides(), a(s(), x)), a(s(), y)) -> a#(div2(), x)) (a#(a(not(), f), x) -> a#(f, x), a#(a(divides(), a(s(), x)), a(s(), y)) -> a#(a(div2(), x), a(s(), y))) (a#(a(not(), f), x) -> a#(f, x), a#(a(divides(), a(s(), x)), a(s(), y)) -> a#(a(a(div2(), x), a(s(), y)), y)) (a#(a(not(), f), x) -> a#(f, x), a#(a(a(if(), true()), x), xs) -> a#(cons(), x)) (a#(a(not(), f), x) -> a#(f, x), a#(a(a(if(), true()), x), xs) -> a#(a(cons(), x), xs)) (a#(a(not(), f), x) -> a#(f, x), a#(a(a(div2(), a(s(), x)), y), a(s(), z)) -> a#(div2(), x)) (a#(a(not(), f), x) -> a#(f, x), a#(a(a(div2(), a(s(), x)), y), a(s(), z)) -> a#(a(div2(), x), y)) (a#(a(not(), f), x) -> a#(f, x), a#(a(a(div2(), a(s(), x)), y), a(s(), z)) -> a#(a(a(div2(), x), y), z)) (a#(a(not(), f), x) -> a#(f, x), a#(a(a(div2(), x), y), 0()) -> a#(divides(), x)) (a#(a(not(), f), x) -> a#(f, x), a#(a(a(div2(), x), y), 0()) -> a#(a(divides(), x), y)) (a#(a(filter(), f), a(a(cons(), x), xs)) -> a#(a(filter(), f), xs), a#(a(filter(), f), a(a(cons(), x), xs)) -> a#(if(), a(f, x))) (a#(a(filter(), f), a(a(cons(), x), xs)) -> a#(a(filter(), f), xs), a#(a(filter(), f), a(a(cons(), x), xs)) -> a#(a(if(), a(f, x)), x)) (a#(a(filter(), f), a(a(cons(), x), xs)) -> a#(a(filter(), f), xs), a#(a(filter(), f), a(a(cons(), x), xs)) -> a#(a(filter(), f), xs)) (a#(a(filter(), f), a(a(cons(), x), xs)) -> a#(a(filter(), f), xs), a#(a(filter(), f), a(a(cons(), x), xs)) -> a#(a(a(if(), a(f, x)), x), a(a(filter(), f), xs))) (a#(a(filter(), f), a(a(cons(), x), xs)) -> a#(a(filter(), f), xs), a#(a(filter(), f), a(a(cons(), x), xs)) -> a#(f, x)) (a#(sieve(), a(a(cons(), x), xs)) -> a#(a(filter(), a(not(), a(divides(), x))), xs), a#(a(filter(), f), a(a(cons(), x), xs)) -> a#(f, x)) (a#(sieve(), a(a(cons(), x), xs)) -> a#(a(filter(), a(not(), a(divides(), x))), xs), a#(a(filter(), f), a(a(cons(), x), xs)) -> a#(a(a(if(), a(f, x)), x), a(a(filter(), f), xs))) (a#(sieve(), a(a(cons(), x), xs)) -> a#(a(filter(), a(not(), a(divides(), x))), xs), a#(a(filter(), f), a(a(cons(), x), xs)) -> a#(a(filter(), f), xs)) (a#(sieve(), a(a(cons(), x), xs)) -> a#(a(filter(), a(not(), a(divides(), x))), xs), a#(a(filter(), f), a(a(cons(), x), xs)) -> a#(a(if(), a(f, x)), x)) (a#(sieve(), a(a(cons(), x), xs)) -> a#(a(filter(), a(not(), a(divides(), x))), xs), a#(a(filter(), f), a(a(cons(), x), xs)) -> a#(if(), a(f, x))) (a#(a(filter(), f), a(a(cons(), x), xs)) -> a#(f, x), a#(a(a(div2(), x), y), 0()) -> a#(a(divides(), x), y)) (a#(a(filter(), f), a(a(cons(), x), xs)) -> a#(f, x), a#(a(a(div2(), x), y), 0()) -> a#(divides(), x)) (a#(a(filter(), f), a(a(cons(), x), xs)) -> a#(f, x), a#(a(a(div2(), a(s(), x)), y), a(s(), z)) -> a#(a(a(div2(), x), y), z)) (a#(a(filter(), f), a(a(cons(), x), xs)) -> a#(f, x), a#(a(a(div2(), a(s(), x)), y), a(s(), z)) -> a#(a(div2(), x), y)) (a#(a(filter(), f), a(a(cons(), x), xs)) -> a#(f, x), a#(a(a(div2(), a(s(), x)), y), a(s(), z)) -> a#(div2(), x)) (a#(a(filter(), f), a(a(cons(), x), xs)) -> a#(f, x), a#(a(a(if(), true()), x), xs) -> a#(a(cons(), x), xs)) (a#(a(filter(), f), a(a(cons(), x), xs)) -> a#(f, x), a#(a(a(if(), true()), x), xs) -> a#(cons(), x)) (a#(a(filter(), f), a(a(cons(), x), xs)) -> a#(f, x), a#(a(divides(), a(s(), x)), a(s(), y)) -> a#(a(a(div2(), x), a(s(), y)), y)) (a#(a(filter(), f), a(a(cons(), x), xs)) -> a#(f, x), a#(a(divides(), a(s(), x)), a(s(), y)) -> a#(a(div2(), x), a(s(), y))) (a#(a(filter(), f), a(a(cons(), x), xs)) -> a#(f, x), a#(a(divides(), a(s(), x)), a(s(), y)) -> a#(div2(), x)) (a#(a(filter(), f), a(a(cons(), x), xs)) -> a#(f, x), a#(a(filter(), f), a(a(cons(), x), xs)) -> a#(f, x)) (a#(a(filter(), f), a(a(cons(), x), xs)) -> a#(f, x), a#(a(filter(), f), a(a(cons(), x), xs)) -> a#(a(a(if(), a(f, x)), x), a(a(filter(), f), xs))) (a#(a(filter(), f), a(a(cons(), x), xs)) -> a#(f, x), a#(a(filter(), f), a(a(cons(), x), xs)) -> a#(a(filter(), f), xs)) (a#(a(filter(), f), a(a(cons(), x), xs)) -> a#(f, x), a#(a(filter(), f), a(a(cons(), x), xs)) -> a#(a(if(), a(f, x)), x)) (a#(a(filter(), f), a(a(cons(), x), xs)) -> a#(f, x), a#(a(filter(), f), a(a(cons(), x), xs)) -> a#(if(), a(f, x))) (a#(a(filter(), f), a(a(cons(), x), xs)) -> a#(f, x), a#(a(not(), f), x) -> a#(f, x)) (a#(a(filter(), f), a(a(cons(), x), xs)) -> a#(f, x), a#(a(not(), f), x) -> a#(not2(), a(f, x))) (a#(a(filter(), f), a(a(cons(), x), xs)) -> a#(f, x), a#(sieve(), a(a(cons(), x), xs)) -> a#(a(filter(), a(not(), a(divides(), x))), xs)) (a#(a(filter(), f), a(a(cons(), x), xs)) -> a#(f, x), a#(sieve(), a(a(cons(), x), xs)) -> a#(a(cons(), x), a(sieve(), a(a(filter(), a(not(), a(divides(), x))), xs)))) (a#(a(filter(), f), a(a(cons(), x), xs)) -> a#(f, x), a#(sieve(), a(a(cons(), x), xs)) -> a#(divides(), x)) (a#(a(filter(), f), a(a(cons(), x), xs)) -> a#(f, x), a#(sieve(), a(a(cons(), x), xs)) -> a#(filter(), a(not(), a(divides(), x)))) (a#(a(filter(), f), a(a(cons(), x), xs)) -> a#(f, x), a#(sieve(), a(a(cons(), x), xs)) -> a#(not(), a(divides(), x))) (a#(a(filter(), f), a(a(cons(), x), xs)) -> a#(f, x), a#(sieve(), a(a(cons(), x), xs)) -> a#(sieve(), a(a(filter(), a(not(), a(divides(), x))), xs))) (a#(a(a(div2(), a(s(), x)), y), a(s(), z)) -> a#(a(a(div2(), x), y), z), a#(a(a(div2(), x), y), 0()) -> a#(a(divides(), x), y)) (a#(a(a(div2(), a(s(), x)), y), a(s(), z)) -> a#(a(a(div2(), x), y), z), a#(a(a(div2(), x), y), 0()) -> a#(divides(), x)) (a#(a(a(div2(), a(s(), x)), y), a(s(), z)) -> a#(a(a(div2(), x), y), z), a#(a(a(div2(), a(s(), x)), y), a(s(), z)) -> a#(a(a(div2(), x), y), z)) (a#(a(a(div2(), a(s(), x)), y), a(s(), z)) -> a#(a(a(div2(), x), y), z), a#(a(a(div2(), a(s(), x)), y), a(s(), z)) -> a#(a(div2(), x), y)) (a#(a(a(div2(), a(s(), x)), y), a(s(), z)) -> a#(a(a(div2(), x), y), z), a#(a(a(div2(), a(s(), x)), y), a(s(), z)) -> a#(div2(), x)) (a#(a(filter(), f), a(a(cons(), x), xs)) -> a#(a(a(if(), a(f, x)), x), a(a(filter(), f), xs)), a#(a(a(if(), true()), x), xs) -> a#(a(cons(), x), xs)) (a#(a(filter(), f), a(a(cons(), x), xs)) -> a#(a(a(if(), a(f, x)), x), a(a(filter(), f), xs)), a#(a(a(if(), true()), x), xs) -> a#(cons(), x)) (a#(a(divides(), a(s(), x)), a(s(), y)) -> a#(a(a(div2(), x), a(s(), y)), y), a#(a(a(div2(), x), y), 0()) -> a#(a(divides(), x), y)) (a#(a(divides(), a(s(), x)), a(s(), y)) -> a#(a(a(div2(), x), a(s(), y)), y), a#(a(a(div2(), x), y), 0()) -> a#(divides(), x)) (a#(a(divides(), a(s(), x)), a(s(), y)) -> a#(a(a(div2(), x), a(s(), y)), y), a#(a(a(div2(), a(s(), x)), y), a(s(), z)) -> a#(a(a(div2(), x), y), z)) (a#(a(divides(), a(s(), x)), a(s(), y)) -> a#(a(a(div2(), x), a(s(), y)), y), a#(a(a(div2(), a(s(), x)), y), a(s(), z)) -> a#(a(div2(), x), y)) (a#(a(divides(), a(s(), x)), a(s(), y)) -> a#(a(a(div2(), x), a(s(), y)), y), a#(a(a(div2(), a(s(), x)), y), a(s(), z)) -> a#(div2(), x)) (a#(a(a(div2(), x), y), 0()) -> a#(a(divides(), x), y), a#(a(divides(), a(s(), x)), a(s(), y)) -> a#(a(a(div2(), x), a(s(), y)), y)) (a#(a(a(div2(), x), y), 0()) -> a#(a(divides(), x), y), a#(a(divides(), a(s(), x)), a(s(), y)) -> a#(a(div2(), x), a(s(), y))) (a#(a(a(div2(), x), y), 0()) -> a#(a(divides(), x), y), a#(a(divides(), a(s(), x)), a(s(), y)) -> a#(div2(), x))} STATUS: arrows: 0.854442 SCCS (2): Scc: {a#(a(filter(), f), a(a(cons(), x), xs)) -> a#(f, x), a#(a(filter(), f), a(a(cons(), x), xs)) -> a#(a(filter(), f), xs), a#(a(not(), f), x) -> a#(f, x), a#(sieve(), a(a(cons(), x), xs)) -> a#(a(filter(), a(not(), a(divides(), x))), xs), a#(sieve(), a(a(cons(), x), xs)) -> a#(sieve(), a(a(filter(), a(not(), a(divides(), x))), xs))} Scc: { a#(a(a(div2(), x), y), 0()) -> a#(a(divides(), x), y), a#(a(a(div2(), a(s(), x)), y), a(s(), z)) -> a#(a(a(div2(), x), y), z), a#(a(divides(), a(s(), x)), a(s(), y)) -> a#(a(a(div2(), x), a(s(), y)), y)} SCC (5): Strict: {a#(a(filter(), f), a(a(cons(), x), xs)) -> a#(f, x), a#(a(filter(), f), a(a(cons(), x), xs)) -> a#(a(filter(), f), xs), a#(a(not(), f), x) -> a#(f, x), a#(sieve(), a(a(cons(), x), xs)) -> a#(a(filter(), a(not(), a(divides(), x))), xs), a#(sieve(), a(a(cons(), x), xs)) -> a#(sieve(), a(a(filter(), a(not(), a(divides(), x))), xs))} Weak: { a(a(a(div2(), x), y), 0()) -> a(a(divides(), x), y), a(a(a(div2(), a(s(), x)), y), a(s(), z)) -> a(a(a(div2(), x), y), z), a(a(a(div2(), 0()), y), a(s(), z)) -> false(), a(a(a(if(), true()), x), xs) -> a(a(cons(), x), xs), a(a(a(if(), false()), x), xs) -> xs, a(a(divides(), a(s(), x)), a(s(), y)) -> a(a(a(div2(), x), a(s(), y)), y), a(a(divides(), 0()), a(s(), y)) -> true(), a(a(filter(), f), a(a(cons(), x), xs)) -> a(a(a(if(), a(f, x)), x), a(a(filter(), f), xs)), a(a(filter(), f), nil()) -> nil(), a(a(not(), f), x) -> a(not2(), a(f, x)), a(not2(), true()) -> false(), a(not2(), false()) -> true(), a(sieve(), a(a(cons(), x), xs)) -> a(a(cons(), x), a(sieve(), a(a(filter(), a(not(), a(divides(), x))), xs))), a(sieve(), nil()) -> nil()} Open SCC (3): Strict: { a#(a(a(div2(), x), y), 0()) -> a#(a(divides(), x), y), a#(a(a(div2(), a(s(), x)), y), a(s(), z)) -> a#(a(a(div2(), x), y), z), a#(a(divides(), a(s(), x)), a(s(), y)) -> a#(a(a(div2(), x), a(s(), y)), y)} Weak: { a(a(a(div2(), x), y), 0()) -> a(a(divides(), x), y), a(a(a(div2(), a(s(), x)), y), a(s(), z)) -> a(a(a(div2(), x), y), z), a(a(a(div2(), 0()), y), a(s(), z)) -> false(), a(a(a(if(), true()), x), xs) -> a(a(cons(), x), xs), a(a(a(if(), false()), x), xs) -> xs, a(a(divides(), a(s(), x)), a(s(), y)) -> a(a(a(div2(), x), a(s(), y)), y), a(a(divides(), 0()), a(s(), y)) -> true(), a(a(filter(), f), a(a(cons(), x), xs)) -> a(a(a(if(), a(f, x)), x), a(a(filter(), f), xs)), a(a(filter(), f), nil()) -> nil(), a(a(not(), f), x) -> a(not2(), a(f, x)), a(not2(), true()) -> false(), a(not2(), false()) -> true(), a(sieve(), a(a(cons(), x), xs)) -> a(a(cons(), x), a(sieve(), a(a(filter(), a(not(), a(divides(), x))), xs))), a(sieve(), nil()) -> nil()} Open