MAYBE Time: 0.002481 TRS: { ack_in(s m, s n) -> u21(ack_in(s m, n), m), ack_in(s m, 0()) -> u11 ack_in(m, s 0()), ack_in(0(), n) -> ack_out s n, u11 ack_out n -> ack_out n, u21(ack_out n, m) -> u22 ack_in(m, n), u22 ack_out n -> ack_out n} DP: DP: { ack_in#(s m, s n) -> ack_in#(s m, n), ack_in#(s m, s n) -> u21#(ack_in(s m, n), m), ack_in#(s m, 0()) -> ack_in#(m, s 0()), ack_in#(s m, 0()) -> u11# ack_in(m, s 0()), u21#(ack_out n, m) -> ack_in#(m, n), u21#(ack_out n, m) -> u22# ack_in(m, n)} TRS: { ack_in(s m, s n) -> u21(ack_in(s m, n), m), ack_in(s m, 0()) -> u11 ack_in(m, s 0()), ack_in(0(), n) -> ack_out s n, u11 ack_out n -> ack_out n, u21(ack_out n, m) -> u22 ack_in(m, n), u22 ack_out n -> ack_out n} UR: { ack_in(s m, s n) -> u21(ack_in(s m, n), m), ack_in(s m, 0()) -> u11 ack_in(m, s 0()), ack_in(0(), n) -> ack_out s n, u11 ack_out n -> ack_out n, u21(ack_out n, m) -> u22 ack_in(m, n), u22 ack_out n -> ack_out n, a(x, y) -> x, a(x, y) -> y} EDG: {(ack_in#(s m, 0()) -> ack_in#(m, s 0()), ack_in#(s m, s n) -> u21#(ack_in(s m, n), m)) (ack_in#(s m, 0()) -> ack_in#(m, s 0()), ack_in#(s m, s n) -> ack_in#(s m, n)) (ack_in#(s m, s n) -> u21#(ack_in(s m, n), m), u21#(ack_out n, m) -> u22# ack_in(m, n)) (ack_in#(s m, s n) -> u21#(ack_in(s m, n), m), u21#(ack_out n, m) -> ack_in#(m, n)) (ack_in#(s m, s n) -> ack_in#(s m, n), ack_in#(s m, 0()) -> u11# ack_in(m, s 0())) (ack_in#(s m, s n) -> ack_in#(s m, n), ack_in#(s m, 0()) -> ack_in#(m, s 0())) (ack_in#(s m, s n) -> ack_in#(s m, n), ack_in#(s m, s n) -> u21#(ack_in(s m, n), m)) (ack_in#(s m, s n) -> ack_in#(s m, n), ack_in#(s m, s n) -> ack_in#(s m, n)) (u21#(ack_out n, m) -> ack_in#(m, n), ack_in#(s m, s n) -> ack_in#(s m, n)) (u21#(ack_out n, m) -> ack_in#(m, n), ack_in#(s m, s n) -> u21#(ack_in(s m, n), m)) (u21#(ack_out n, m) -> ack_in#(m, n), ack_in#(s m, 0()) -> ack_in#(m, s 0())) (u21#(ack_out n, m) -> ack_in#(m, n), ack_in#(s m, 0()) -> u11# ack_in(m, s 0()))} STATUS: arrows: 0.666667 SCCS (1): Scc: { ack_in#(s m, s n) -> ack_in#(s m, n), ack_in#(s m, s n) -> u21#(ack_in(s m, n), m), ack_in#(s m, 0()) -> ack_in#(m, s 0()), u21#(ack_out n, m) -> ack_in#(m, n)} SCC (4): Strict: { ack_in#(s m, s n) -> ack_in#(s m, n), ack_in#(s m, s n) -> u21#(ack_in(s m, n), m), ack_in#(s m, 0()) -> ack_in#(m, s 0()), u21#(ack_out n, m) -> ack_in#(m, n)} Weak: { ack_in(s m, s n) -> u21(ack_in(s m, n), m), ack_in(s m, 0()) -> u11 ack_in(m, s 0()), ack_in(0(), n) -> ack_out s n, u11 ack_out n -> ack_out n, u21(ack_out n, m) -> u22 ack_in(m, n), u22 ack_out n -> ack_out n} Open