MAYBE Time: 0.189709 TRS: { :(x, x) -> e(), :(x, e()) -> x, :(x, :(y, :(i x, z))) -> :(i z, y), :(x, :(y, i x)) -> i y, :(e(), x) -> i x, :(:(x, y), z) -> :(x, :(z, i y)), :(i x, :(y, x)) -> i y, :(i x, :(y, :(x, z))) -> :(i z, y), i e() -> e(), i :(x, y) -> :(y, x), i i x -> x} DP: DP: {:#(x, :(y, :(i x, z))) -> :#(i z, y), :#(x, :(y, :(i x, z))) -> i# z, :#(x, :(y, i x)) -> i# y, :#(e(), x) -> i# x, :#(:(x, y), z) -> :#(x, :(z, i y)), :#(:(x, y), z) -> :#(z, i y), :#(:(x, y), z) -> i# y, :#(i x, :(y, x)) -> i# y, :#(i x, :(y, :(x, z))) -> :#(i z, y), :#(i x, :(y, :(x, z))) -> i# z, i# :(x, y) -> :#(y, x)} TRS: { :(x, x) -> e(), :(x, e()) -> x, :(x, :(y, :(i x, z))) -> :(i z, y), :(x, :(y, i x)) -> i y, :(e(), x) -> i x, :(:(x, y), z) -> :(x, :(z, i y)), :(i x, :(y, x)) -> i y, :(i x, :(y, :(x, z))) -> :(i z, y), i e() -> e(), i :(x, y) -> :(y, x), i i x -> x} UR: { :(x, x) -> e(), :(x, e()) -> x, :(x, :(y, :(i x, z))) -> :(i z, y), :(x, :(y, i x)) -> i y, :(e(), x) -> i x, :(:(x, y), z) -> :(x, :(z, i y)), :(i x, :(y, x)) -> i y, :(i x, :(y, :(x, z))) -> :(i z, y), i e() -> e(), i :(x, y) -> :(y, x), i i x -> x} EDG: {(:#(:(x, y), z) -> :#(z, i y), :#(i x, :(y, :(x, z))) -> i# z) (:#(:(x, y), z) -> :#(z, i y), :#(i x, :(y, :(x, z))) -> :#(i z, y)) (:#(:(x, y), z) -> :#(z, i y), :#(i x, :(y, x)) -> i# y) (:#(:(x, y), z) -> :#(z, i y), :#(:(x, y), z) -> i# y) (:#(:(x, y), z) -> :#(z, i y), :#(:(x, y), z) -> :#(z, i y)) (:#(:(x, y), z) -> :#(z, i y), :#(:(x, y), z) -> :#(x, :(z, i y))) (:#(:(x, y), z) -> :#(z, i y), :#(e(), x) -> i# x) (:#(:(x, y), z) -> :#(z, i y), :#(x, :(y, i x)) -> i# y) (:#(:(x, y), z) -> :#(z, i y), :#(x, :(y, :(i x, z))) -> i# z) (:#(:(x, y), z) -> :#(z, i y), :#(x, :(y, :(i x, z))) -> :#(i z, y)) (:#(:(x, y), z) -> i# y, i# :(x, y) -> :#(y, x)) (:#(x, :(y, :(i x, z))) -> i# z, i# :(x, y) -> :#(y, x)) (:#(x, :(y, :(i x, z))) -> :#(i z, y), :#(i x, :(y, :(x, z))) -> i# z) (:#(x, :(y, :(i x, z))) -> :#(i z, y), :#(i x, :(y, :(x, z))) -> :#(i z, y)) (:#(x, :(y, :(i x, z))) -> :#(i z, y), :#(i x, :(y, x)) -> i# y) (:#(x, :(y, :(i x, z))) -> :#(i z, y), :#(:(x, y), z) -> i# y) (:#(x, :(y, :(i x, z))) -> :#(i z, y), :#(:(x, y), z) -> :#(z, i y)) (:#(x, :(y, :(i x, z))) -> :#(i z, y), :#(:(x, y), z) -> :#(x, :(z, i y))) (:#(x, :(y, :(i x, z))) -> :#(i z, y), :#(e(), x) -> i# x) (:#(x, :(y, :(i x, z))) -> :#(i z, y), :#(x, :(y, i x)) -> i# y) (:#(x, :(y, :(i x, z))) -> :#(i z, y), :#(x, :(y, :(i x, z))) -> i# z) (:#(x, :(y, :(i x, z))) -> :#(i z, y), :#(x, :(y, :(i x, z))) -> :#(i z, y)) (:#(:(x, y), z) -> :#(x, :(z, i y)), :#(i x, :(y, :(x, z))) -> i# z) (:#(:(x, y), z) -> :#(x, :(z, i y)), :#(i x, :(y, :(x, z))) -> :#(i z, y)) (:#(:(x, y), z) -> :#(x, :(z, i y)), :#(i x, :(y, x)) -> i# y) (:#(:(x, y), z) -> :#(x, :(z, i y)), :#(:(x, y), z) -> i# y) (:#(:(x, y), z) -> :#(x, :(z, i y)), :#(:(x, y), z) -> :#(z, i y)) (:#(:(x, y), z) -> :#(x, :(z, i y)), :#(:(x, y), z) -> :#(x, :(z, i y))) (:#(:(x, y), z) -> :#(x, :(z, i y)), :#(e(), x) -> i# x) (:#(:(x, y), z) -> :#(x, :(z, i y)), :#(x, :(y, i x)) -> i# y) (:#(:(x, y), z) -> :#(x, :(z, i y)), :#(x, :(y, :(i x, z))) -> i# z) (:#(:(x, y), z) -> :#(x, :(z, i y)), :#(x, :(y, :(i x, z))) -> :#(i z, y)) (i# :(x, y) -> :#(y, x), :#(x, :(y, :(i x, z))) -> :#(i z, y)) (i# :(x, y) -> :#(y, x), :#(x, :(y, :(i x, z))) -> i# z) (i# :(x, y) -> :#(y, x), :#(x, :(y, i x)) -> i# y) (i# :(x, y) -> :#(y, x), :#(e(), x) -> i# x) (i# :(x, y) -> :#(y, x), :#(:(x, y), z) -> :#(x, :(z, i y))) (i# :(x, y) -> :#(y, x), :#(:(x, y), z) -> :#(z, i y)) (i# :(x, y) -> :#(y, x), :#(:(x, y), z) -> i# y) (i# :(x, y) -> :#(y, x), :#(i x, :(y, x)) -> i# y) (i# :(x, y) -> :#(y, x), :#(i x, :(y, :(x, z))) -> :#(i z, y)) (i# :(x, y) -> :#(y, x), :#(i x, :(y, :(x, z))) -> i# z) (:#(i x, :(y, :(x, z))) -> :#(i z, y), :#(x, :(y, :(i x, z))) -> :#(i z, y)) (:#(i x, :(y, :(x, z))) -> :#(i z, y), :#(x, :(y, :(i x, z))) -> i# z) (:#(i x, :(y, :(x, z))) -> :#(i z, y), :#(x, :(y, i x)) -> i# y) (:#(i x, :(y, :(x, z))) -> :#(i z, y), :#(e(), x) -> i# x) (:#(i x, :(y, :(x, z))) -> :#(i z, y), :#(:(x, y), z) -> :#(x, :(z, i y))) (:#(i x, :(y, :(x, z))) -> :#(i z, y), :#(:(x, y), z) -> :#(z, i y)) (:#(i x, :(y, :(x, z))) -> :#(i z, y), :#(:(x, y), z) -> i# y) (:#(i x, :(y, :(x, z))) -> :#(i z, y), :#(i x, :(y, x)) -> i# y) (:#(i x, :(y, :(x, z))) -> :#(i z, y), :#(i x, :(y, :(x, z))) -> :#(i z, y)) (:#(i x, :(y, :(x, z))) -> :#(i z, y), :#(i x, :(y, :(x, z))) -> i# z) (:#(i x, :(y, :(x, z))) -> i# z, i# :(x, y) -> :#(y, x)) (:#(i x, :(y, x)) -> i# y, i# :(x, y) -> :#(y, x)) (:#(x, :(y, i x)) -> i# y, i# :(x, y) -> :#(y, x)) (:#(e(), x) -> i# x, i# :(x, y) -> :#(y, x))} STATUS: arrows: 0.537190 SCCS (1): Scc: {:#(x, :(y, :(i x, z))) -> :#(i z, y), :#(x, :(y, :(i x, z))) -> i# z, :#(x, :(y, i x)) -> i# y, :#(e(), x) -> i# x, :#(:(x, y), z) -> :#(x, :(z, i y)), :#(:(x, y), z) -> :#(z, i y), :#(:(x, y), z) -> i# y, :#(i x, :(y, x)) -> i# y, :#(i x, :(y, :(x, z))) -> :#(i z, y), :#(i x, :(y, :(x, z))) -> i# z, i# :(x, y) -> :#(y, x)} SCC (11): Strict: {:#(x, :(y, :(i x, z))) -> :#(i z, y), :#(x, :(y, :(i x, z))) -> i# z, :#(x, :(y, i x)) -> i# y, :#(e(), x) -> i# x, :#(:(x, y), z) -> :#(x, :(z, i y)), :#(:(x, y), z) -> :#(z, i y), :#(:(x, y), z) -> i# y, :#(i x, :(y, x)) -> i# y, :#(i x, :(y, :(x, z))) -> :#(i z, y), :#(i x, :(y, :(x, z))) -> i# z, i# :(x, y) -> :#(y, x)} Weak: { :(x, x) -> e(), :(x, e()) -> x, :(x, :(y, :(i x, z))) -> :(i z, y), :(x, :(y, i x)) -> i y, :(e(), x) -> i x, :(:(x, y), z) -> :(x, :(z, i y)), :(i x, :(y, x)) -> i y, :(i x, :(y, :(x, z))) -> :(i z, y), i e() -> e(), i :(x, y) -> :(y, x), i i x -> x} Open