MAYBE Time: 0.001933 TRS: {ack(s x, s y) -> ack(x, ack(s x, y)), ack(s x, 0()) -> ack(x, s 0()), ack(0(), y) -> s y} DP: DP: {ack#(s x, s y) -> ack#(x, ack(s x, y)), ack#(s x, s y) -> ack#(s x, y), ack#(s x, 0()) -> ack#(x, s 0())} TRS: {ack(s x, s y) -> ack(x, ack(s x, y)), ack(s x, 0()) -> ack(x, s 0()), ack(0(), y) -> s y} EDG: {(ack#(s x, s y) -> ack#(s x, y), ack#(s x, 0()) -> ack#(x, s 0())) (ack#(s x, s y) -> ack#(s x, y), ack#(s x, s y) -> ack#(s x, y)) (ack#(s x, s y) -> ack#(s x, y), ack#(s x, s y) -> ack#(x, ack(s x, y))) (ack#(s x, 0()) -> ack#(x, s 0()), ack#(s x, s y) -> ack#(x, ack(s x, y))) (ack#(s x, 0()) -> ack#(x, s 0()), ack#(s x, s y) -> ack#(s x, y)) (ack#(s x, 0()) -> ack#(x, s 0()), ack#(s x, 0()) -> ack#(x, s 0())) (ack#(s x, s y) -> ack#(x, ack(s x, y)), ack#(s x, s y) -> ack#(x, ack(s x, y))) (ack#(s x, s y) -> ack#(x, ack(s x, y)), ack#(s x, s y) -> ack#(s x, y)) (ack#(s x, s y) -> ack#(x, ack(s x, y)), ack#(s x, 0()) -> ack#(x, s 0()))} EDG: {(ack#(s x, s y) -> ack#(s x, y), ack#(s x, 0()) -> ack#(x, s 0())) (ack#(s x, s y) -> ack#(s x, y), ack#(s x, s y) -> ack#(s x, y)) (ack#(s x, s y) -> ack#(s x, y), ack#(s x, s y) -> ack#(x, ack(s x, y))) (ack#(s x, 0()) -> ack#(x, s 0()), ack#(s x, s y) -> ack#(x, ack(s x, y))) (ack#(s x, 0()) -> ack#(x, s 0()), ack#(s x, s y) -> ack#(s x, y)) (ack#(s x, s y) -> ack#(x, ack(s x, y)), ack#(s x, s y) -> ack#(x, ack(s x, y))) (ack#(s x, s y) -> ack#(x, ack(s x, y)), ack#(s x, s y) -> ack#(s x, y))} EDG: {(ack#(s x, s y) -> ack#(s x, y), ack#(s x, 0()) -> ack#(x, s 0())) (ack#(s x, s y) -> ack#(s x, y), ack#(s x, s y) -> ack#(s x, y)) (ack#(s x, s y) -> ack#(s x, y), ack#(s x, s y) -> ack#(x, ack(s x, y))) (ack#(s x, 0()) -> ack#(x, s 0()), ack#(s x, s y) -> ack#(x, ack(s x, y))) (ack#(s x, 0()) -> ack#(x, s 0()), ack#(s x, s y) -> ack#(s x, y)) (ack#(s x, s y) -> ack#(x, ack(s x, y)), ack#(s x, s y) -> ack#(x, ack(s x, y))) (ack#(s x, s y) -> ack#(x, ack(s x, y)), ack#(s x, s y) -> ack#(s x, y))} EDG: {(ack#(s x, s y) -> ack#(s x, y), ack#(s x, 0()) -> ack#(x, s 0())) (ack#(s x, s y) -> ack#(s x, y), ack#(s x, s y) -> ack#(s x, y)) (ack#(s x, s y) -> ack#(s x, y), ack#(s x, s y) -> ack#(x, ack(s x, y))) (ack#(s x, 0()) -> ack#(x, s 0()), ack#(s x, s y) -> ack#(x, ack(s x, y))) (ack#(s x, 0()) -> ack#(x, s 0()), ack#(s x, s y) -> ack#(s x, y)) (ack#(s x, s y) -> ack#(x, ack(s x, y)), ack#(s x, s y) -> ack#(x, ack(s x, y))) (ack#(s x, s y) -> ack#(x, ack(s x, y)), ack#(s x, s y) -> ack#(s x, y))} STATUS: arrows: 0.222222 SCCS (1): Scc: {ack#(s x, s y) -> ack#(x, ack(s x, y)), ack#(s x, s y) -> ack#(s x, y), ack#(s x, 0()) -> ack#(x, s 0())} SCC (3): Strict: {ack#(s x, s y) -> ack#(x, ack(s x, y)), ack#(s x, s y) -> ack#(s x, y), ack#(s x, 0()) -> ack#(x, s 0())} Weak: {ack(s x, s y) -> ack(x, ack(s x, y)), ack(s x, 0()) -> ack(x, s 0()), ack(0(), y) -> s y} Open