MAYBE Time: 0.000633 TRS: {u21(ackout X, Y) -> u22 ackin(Y, X), ackin(s X, s Y) -> u21(ackin(s X, Y), X)} DP: DP: {u21#(ackout X, Y) -> ackin#(Y, X), ackin#(s X, s Y) -> u21#(ackin(s X, Y), X), ackin#(s X, s Y) -> ackin#(s X, Y)} TRS: {u21(ackout X, Y) -> u22 ackin(Y, X), ackin(s X, s Y) -> u21(ackin(s X, Y), X)} UR: {u21(ackout X, Y) -> u22 ackin(Y, X), ackin(s X, s Y) -> u21(ackin(s X, Y), X), a(x, y) -> x, a(x, y) -> y} EDG: {(ackin#(s X, s Y) -> u21#(ackin(s X, Y), X), u21#(ackout X, Y) -> ackin#(Y, X)) (u21#(ackout X, Y) -> ackin#(Y, X), ackin#(s X, s Y) -> u21#(ackin(s X, Y), X)) (u21#(ackout X, Y) -> ackin#(Y, X), ackin#(s X, s Y) -> ackin#(s X, Y)) (ackin#(s X, s Y) -> ackin#(s X, Y), ackin#(s X, s Y) -> u21#(ackin(s X, Y), X)) (ackin#(s X, s Y) -> ackin#(s X, Y), ackin#(s X, s Y) -> ackin#(s X, Y))} STATUS: arrows: 0.444444 SCCS (1): Scc: {u21#(ackout X, Y) -> ackin#(Y, X), ackin#(s X, s Y) -> u21#(ackin(s X, Y), X), ackin#(s X, s Y) -> ackin#(s X, Y)} SCC (3): Strict: {u21#(ackout X, Y) -> ackin#(Y, X), ackin#(s X, s Y) -> u21#(ackin(s X, Y), X), ackin#(s X, s Y) -> ackin#(s X, Y)} Weak: {u21(ackout X, Y) -> u22 ackin(Y, X), ackin(s X, s Y) -> u21(ackin(s X, Y), X)} Open