Reading in file: "test12.maude"
==========================================

Reading in file: "test.maude"
==========================================
mod TEST
Advisory: redefining module TEST.
Done reading in file: "test.maude"
==========================================
mod TEST12
==========================================
search in TEST12 : start =>! s:State .

Solution 1 (state 130568)
states: 130583  rewrites: 9108810 in 298150ms cpu (308190ms real) (30551 rewrites/second)
s:State --> multicast-ack(proc("a"))
network(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")))
freshconf(5)
operational(proc("a"))
operational(proc("b"))
operational(proc("c"))
freshseq(1)
CONTROLLER(eController)
localconf(proc("a"), regconf(sProcSet(proc("a")), 2))
localconf(proc("b"), regconf(sProcSet(proc("b")) sProcSet(proc("c")), 4))
localconf(proc("c"), regconf(sProcSet(proc("b")) sProcSet(proc("c")), 4))
delivered(proc("a"), sMessageList(datamsg(proc("a"), agreed, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), 0, eNatSet, data(
    "test"))) sMessageList(transmsg(transconf(sProcSet(proc("a")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0))))
    sMessageList(confmsg(regconf(sProcSet(proc("a")), 2), sProcSet(proc("a")))))
delivered(proc("b"), sMessageList(datamsg(proc("a"), agreed, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), 0, eNatSet, data(
    "test"))) sMessageList(transmsg(transconf(sProcSet(proc("b")) sProcSet(proc("c")), 3, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc(
    "c")), 0)))) sMessageList(confmsg(regconf(sProcSet(proc("b")) sProcSet(proc("c")), 4), sProcSet(proc("b")) sProcSet(proc("c")))))
delivered(proc("c"), sMessageList(datamsg(proc("a"), agreed, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), 0, eNatSet, data(
    "test"))) sMessageList(transmsg(transconf(sProcSet(proc("b")) sProcSet(proc("c")), 3, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc(
    "c")), 0)))) sMessageList(confmsg(regconf(sProcSet(proc("b")) sProcSet(proc("c")), 4), sProcSet(proc("b")) sProcSet(proc("c")))))
alldelivered(proc("a"), sMessageList(datamsg(proc("a"), agreed, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), 0, eNatSet,
    data("test"))) sMessageList(transmsg(transconf(sProcSet(proc("a")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0))))
    sMessageList(confmsg(regconf(sProcSet(proc("a")), 2), sProcSet(proc("a")))))
alldelivered(proc("b"), sMessageList(datamsg(proc("a"), agreed, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), 0, eNatSet,
    data("test"))) sMessageList(transmsg(transconf(sProcSet(proc("b")) sProcSet(proc("c")), 3, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(
    proc("c")), 0)))) sMessageList(confmsg(regconf(sProcSet(proc("b")) sProcSet(proc("c")), 4), sProcSet(proc("b")) sProcSet(proc("c")))))
alldelivered(proc("c"), sMessageList(datamsg(proc("a"), agreed, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), 0, eNatSet,
    data("test"))) sMessageList(transmsg(transconf(sProcSet(proc("b")) sProcSet(proc("c")), 3, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(
    proc("c")), 0)))) sMessageList(confmsg(regconf(sProcSet(proc("b")) sProcSet(proc("c")), 4), sProcSet(proc("b")) sProcSet(proc("c")))))
reachable(proc("a"), sProcSet(proc("a")))
reachable(proc("b"), sProcSet(proc("b")) sProcSet(proc("c")))
reachable(proc("c"), sProcSet(proc("b")) sProcSet(proc("c")))
sent(proc("a"), eBroadcastSet)
sent(proc("b"), eBroadcastSet)
sent(proc("c"), eBroadcastSet)
received(proc("a"), eMessageSet)
received(proc("b"), eMessageSet)
received(proc("c"), eMessageSet)
acked(proc("a"), eMessageSet)
acked(proc("b"), eMessageSet)
acked(proc("c"), eMessageSet)
causalorder(regconf(sProcSet(proc("a")), 2), eConstraintSet)
causalorder(regconf(sProcSet(proc("b")) sProcSet(proc("c")), 4), eConstraintSet)
causalorder(regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), eConstraintSet)
causalorder(transconf(sProcSet(proc("a")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), eConstraintSet)
causalorder(transconf(sProcSet(proc("b")) sProcSet(proc("c")), 3, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)),
    eConstraintSet)
totalorder(regconf(sProcSet(proc("a")), 2), eEventList)
totalorder(regconf(sProcSet(proc("b")) sProcSet(proc("c")), 4), eEventList)
totalorder(regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), sEventList(event(proc("a"), 0)) sEventList(event(proc("a"), 0))
    sEventList(event(proc("a"), 0)))
totalorder(transconf(sProcSet(proc("a")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), sEventList(event(proc("a"), 0))
    sEventList(event(proc("a"), 0)))
totalorder(transconf(sProcSet(proc("b")) sProcSet(proc("c")), 3, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), sEventList(
    event(proc("a"), 0)) sEventList(event(proc("a"), 0)) sEventList(event(proc("a"), 0)))
localmsgs(proc("a"), regconf(sProcSet(proc("a")), 2), eNatSet)
localmsgs(proc("a"), regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), sNatSet(0))
localmsgs(proc("a"), transconf(sProcSet(proc("a")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), eNatSet)
localmsgs(proc("b"), regconf(sProcSet(proc("b")) sProcSet(proc("c")), 4), eNatSet)
localmsgs(proc("b"), regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), eNatSet)
localmsgs(proc("b"), transconf(sProcSet(proc("b")) sProcSet(proc("c")), 3, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)),
    eNatSet)
localmsgs(proc("c"), regconf(sProcSet(proc("b")) sProcSet(proc("c")), 4), eNatSet)
localmsgs(proc("c"), regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), eNatSet)
localmsgs(proc("c"), transconf(sProcSet(proc("b")) sProcSet(proc("c")), 3, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)),
    eNatSet)
knownmsgs(proc("a"), regconf(sProcSet(proc("a")), 2), eNatSet)
knownmsgs(proc("a"), regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), sNatSet(0))
knownmsgs(proc("a"), transconf(sProcSet(proc("a")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), eNatSet)
knownmsgs(proc("b"), regconf(sProcSet(proc("b")) sProcSet(proc("c")), 4), eNatSet)
knownmsgs(proc("b"), regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), sNatSet(0))
knownmsgs(proc("b"), transconf(sProcSet(proc("b")) sProcSet(proc("c")), 3, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)),
    eNatSet)
knownmsgs(proc("c"), regconf(sProcSet(proc("b")) sProcSet(proc("c")), 4), eNatSet)
knownmsgs(proc("c"), regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), sNatSet(0))
knownmsgs(proc("c"), transconf(sProcSet(proc("b")) sProcSet(proc("c")), 3, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)),
    eNatSet)

Solution 2 (state 130569)
states: 130583  rewrites: 9108812 in 298160ms cpu (308310ms real) (30550 rewrites/second)
s:State --> multicast-ack(proc("a"))
network(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")))
freshconf(5)
operational(proc("a"))
operational(proc("b"))
operational(proc("c"))
freshseq(1)
CONTROLLER(eController)
localconf(proc("a"), regconf(sProcSet(proc("a")), 3))
localconf(proc("b"), regconf(sProcSet(proc("b")) sProcSet(proc("c")), 4))
localconf(proc("c"), regconf(sProcSet(proc("b")) sProcSet(proc("c")), 4))
delivered(proc("a"), sMessageList(datamsg(proc("a"), agreed, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), 0, eNatSet, data(
    "test"))) sMessageList(transmsg(transconf(sProcSet(proc("a")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0))))
    sMessageList(confmsg(regconf(sProcSet(proc("a")), 3), sProcSet(proc("a")))))
delivered(proc("b"), sMessageList(datamsg(proc("a"), agreed, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), 0, eNatSet, data(
    "test"))) sMessageList(transmsg(transconf(sProcSet(proc("b")) sProcSet(proc("c")), 2, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc(
    "c")), 0)))) sMessageList(confmsg(regconf(sProcSet(proc("b")) sProcSet(proc("c")), 4), sProcSet(proc("b")) sProcSet(proc("c")))))
delivered(proc("c"), sMessageList(datamsg(proc("a"), agreed, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), 0, eNatSet, data(
    "test"))) sMessageList(transmsg(transconf(sProcSet(proc("b")) sProcSet(proc("c")), 2, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc(
    "c")), 0)))) sMessageList(confmsg(regconf(sProcSet(proc("b")) sProcSet(proc("c")), 4), sProcSet(proc("b")) sProcSet(proc("c")))))
alldelivered(proc("a"), sMessageList(datamsg(proc("a"), agreed, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), 0, eNatSet,
    data("test"))) sMessageList(transmsg(transconf(sProcSet(proc("a")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0))))
    sMessageList(confmsg(regconf(sProcSet(proc("a")), 3), sProcSet(proc("a")))))
alldelivered(proc("b"), sMessageList(datamsg(proc("a"), agreed, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), 0, eNatSet,
    data("test"))) sMessageList(transmsg(transconf(sProcSet(proc("b")) sProcSet(proc("c")), 2, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(
    proc("c")), 0)))) sMessageList(confmsg(regconf(sProcSet(proc("b")) sProcSet(proc("c")), 4), sProcSet(proc("b")) sProcSet(proc("c")))))
alldelivered(proc("c"), sMessageList(datamsg(proc("a"), agreed, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), 0, eNatSet,
    data("test"))) sMessageList(transmsg(transconf(sProcSet(proc("b")) sProcSet(proc("c")), 2, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(
    proc("c")), 0)))) sMessageList(confmsg(regconf(sProcSet(proc("b")) sProcSet(proc("c")), 4), sProcSet(proc("b")) sProcSet(proc("c")))))
reachable(proc("a"), sProcSet(proc("a")))
reachable(proc("b"), sProcSet(proc("b")) sProcSet(proc("c")))
reachable(proc("c"), sProcSet(proc("b")) sProcSet(proc("c")))
sent(proc("a"), eBroadcastSet)
sent(proc("b"), eBroadcastSet)
sent(proc("c"), eBroadcastSet)
received(proc("a"), eMessageSet)
received(proc("b"), eMessageSet)
received(proc("c"), eMessageSet)
acked(proc("a"), eMessageSet)
acked(proc("b"), eMessageSet)
acked(proc("c"), eMessageSet)
causalorder(regconf(sProcSet(proc("a")), 3), eConstraintSet)
causalorder(regconf(sProcSet(proc("b")) sProcSet(proc("c")), 4), eConstraintSet)
causalorder(regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), eConstraintSet)
causalorder(transconf(sProcSet(proc("a")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), eConstraintSet)
causalorder(transconf(sProcSet(proc("b")) sProcSet(proc("c")), 2, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)),
    eConstraintSet)
totalorder(regconf(sProcSet(proc("a")), 3), eEventList)
totalorder(regconf(sProcSet(proc("b")) sProcSet(proc("c")), 4), eEventList)
totalorder(regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), sEventList(event(proc("a"), 0)) sEventList(event(proc("a"), 0))
    sEventList(event(proc("a"), 0)))
totalorder(transconf(sProcSet(proc("a")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), sEventList(event(proc("a"), 0))
    sEventList(event(proc("a"), 0)))
totalorder(transconf(sProcSet(proc("b")) sProcSet(proc("c")), 2, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), sEventList(
    event(proc("a"), 0)) sEventList(event(proc("a"), 0)) sEventList(event(proc("a"), 0)))
localmsgs(proc("a"), regconf(sProcSet(proc("a")), 3), eNatSet)
localmsgs(proc("a"), regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), sNatSet(0))
localmsgs(proc("a"), transconf(sProcSet(proc("a")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), eNatSet)
localmsgs(proc("b"), regconf(sProcSet(proc("b")) sProcSet(proc("c")), 4), eNatSet)
localmsgs(proc("b"), regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), eNatSet)
localmsgs(proc("b"), transconf(sProcSet(proc("b")) sProcSet(proc("c")), 2, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)),
    eNatSet)
localmsgs(proc("c"), regconf(sProcSet(proc("b")) sProcSet(proc("c")), 4), eNatSet)
localmsgs(proc("c"), regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), eNatSet)
localmsgs(proc("c"), transconf(sProcSet(proc("b")) sProcSet(proc("c")), 2, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)),
    eNatSet)
knownmsgs(proc("a"), regconf(sProcSet(proc("a")), 3), eNatSet)
knownmsgs(proc("a"), regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), sNatSet(0))
knownmsgs(proc("a"), transconf(sProcSet(proc("a")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), eNatSet)
knownmsgs(proc("b"), regconf(sProcSet(proc("b")) sProcSet(proc("c")), 4), eNatSet)
knownmsgs(proc("b"), regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), sNatSet(0))
knownmsgs(proc("b"), transconf(sProcSet(proc("b")) sProcSet(proc("c")), 2, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)),
    eNatSet)
knownmsgs(proc("c"), regconf(sProcSet(proc("b")) sProcSet(proc("c")), 4), eNatSet)
knownmsgs(proc("c"), regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), sNatSet(0))
knownmsgs(proc("c"), transconf(sProcSet(proc("b")) sProcSet(proc("c")), 2, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)),
    eNatSet)

Solution 3 (state 130570)
states: 130583  rewrites: 9108814 in 298160ms cpu (308420ms real) (30550 rewrites/second)
s:State --> multicast-ack(proc("a"))
network(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")))
freshconf(5)
operational(proc("a"))
operational(proc("b"))
operational(proc("c"))
freshseq(1)
CONTROLLER(eController)
localconf(proc("a"), regconf(sProcSet(proc("a")), 4))
localconf(proc("b"), regconf(sProcSet(proc("b")) sProcSet(proc("c")), 3))
localconf(proc("c"), regconf(sProcSet(proc("b")) sProcSet(proc("c")), 3))
delivered(proc("a"), sMessageList(datamsg(proc("a"), agreed, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), 0, eNatSet, data(
    "test"))) sMessageList(transmsg(transconf(sProcSet(proc("a")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0))))
    sMessageList(confmsg(regconf(sProcSet(proc("a")), 4), sProcSet(proc("a")))))
delivered(proc("b"), sMessageList(datamsg(proc("a"), agreed, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), 0, eNatSet, data(
    "test"))) sMessageList(transmsg(transconf(sProcSet(proc("b")) sProcSet(proc("c")), 2, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc(
    "c")), 0)))) sMessageList(confmsg(regconf(sProcSet(proc("b")) sProcSet(proc("c")), 3), sProcSet(proc("b")) sProcSet(proc("c")))))
delivered(proc("c"), sMessageList(datamsg(proc("a"), agreed, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), 0, eNatSet, data(
    "test"))) sMessageList(transmsg(transconf(sProcSet(proc("b")) sProcSet(proc("c")), 2, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc(
    "c")), 0)))) sMessageList(confmsg(regconf(sProcSet(proc("b")) sProcSet(proc("c")), 3), sProcSet(proc("b")) sProcSet(proc("c")))))
alldelivered(proc("a"), sMessageList(datamsg(proc("a"), agreed, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), 0, eNatSet,
    data("test"))) sMessageList(transmsg(transconf(sProcSet(proc("a")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0))))
    sMessageList(confmsg(regconf(sProcSet(proc("a")), 4), sProcSet(proc("a")))))
alldelivered(proc("b"), sMessageList(datamsg(proc("a"), agreed, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), 0, eNatSet,
    data("test"))) sMessageList(transmsg(transconf(sProcSet(proc("b")) sProcSet(proc("c")), 2, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(
    proc("c")), 0)))) sMessageList(confmsg(regconf(sProcSet(proc("b")) sProcSet(proc("c")), 3), sProcSet(proc("b")) sProcSet(proc("c")))))
alldelivered(proc("c"), sMessageList(datamsg(proc("a"), agreed, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), 0, eNatSet,
    data("test"))) sMessageList(transmsg(transconf(sProcSet(proc("b")) sProcSet(proc("c")), 2, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(
    proc("c")), 0)))) sMessageList(confmsg(regconf(sProcSet(proc("b")) sProcSet(proc("c")), 3), sProcSet(proc("b")) sProcSet(proc("c")))))
reachable(proc("a"), sProcSet(proc("a")))
reachable(proc("b"), sProcSet(proc("b")) sProcSet(proc("c")))
reachable(proc("c"), sProcSet(proc("b")) sProcSet(proc("c")))
sent(proc("a"), eBroadcastSet)
sent(proc("b"), eBroadcastSet)
sent(proc("c"), eBroadcastSet)
received(proc("a"), eMessageSet)
received(proc("b"), eMessageSet)
received(proc("c"), eMessageSet)
acked(proc("a"), eMessageSet)
acked(proc("b"), eMessageSet)
acked(proc("c"), eMessageSet)
causalorder(regconf(sProcSet(proc("a")), 4), eConstraintSet)
causalorder(regconf(sProcSet(proc("b")) sProcSet(proc("c")), 3), eConstraintSet)
causalorder(regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), eConstraintSet)
causalorder(transconf(sProcSet(proc("a")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), eConstraintSet)
causalorder(transconf(sProcSet(proc("b")) sProcSet(proc("c")), 2, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)),
    eConstraintSet)
totalorder(regconf(sProcSet(proc("a")), 4), eEventList)
totalorder(regconf(sProcSet(proc("b")) sProcSet(proc("c")), 3), eEventList)
totalorder(regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), sEventList(event(proc("a"), 0)) sEventList(event(proc("a"), 0))
    sEventList(event(proc("a"), 0)))
totalorder(transconf(sProcSet(proc("a")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), sEventList(event(proc("a"), 0))
    sEventList(event(proc("a"), 0)))
totalorder(transconf(sProcSet(proc("b")) sProcSet(proc("c")), 2, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), sEventList(
    event(proc("a"), 0)) sEventList(event(proc("a"), 0)) sEventList(event(proc("a"), 0)))
localmsgs(proc("a"), regconf(sProcSet(proc("a")), 4), eNatSet)
localmsgs(proc("a"), regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), sNatSet(0))
localmsgs(proc("a"), transconf(sProcSet(proc("a")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), eNatSet)
localmsgs(proc("b"), regconf(sProcSet(proc("b")) sProcSet(proc("c")), 3), eNatSet)
localmsgs(proc("b"), regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), eNatSet)
localmsgs(proc("b"), transconf(sProcSet(proc("b")) sProcSet(proc("c")), 2, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)),
    eNatSet)
localmsgs(proc("c"), regconf(sProcSet(proc("b")) sProcSet(proc("c")), 3), eNatSet)
localmsgs(proc("c"), regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), eNatSet)
localmsgs(proc("c"), transconf(sProcSet(proc("b")) sProcSet(proc("c")), 2, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)),
    eNatSet)
knownmsgs(proc("a"), regconf(sProcSet(proc("a")), 4), eNatSet)
knownmsgs(proc("a"), regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), sNatSet(0))
knownmsgs(proc("a"), transconf(sProcSet(proc("a")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), eNatSet)
knownmsgs(proc("b"), regconf(sProcSet(proc("b")) sProcSet(proc("c")), 3), eNatSet)
knownmsgs(proc("b"), regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), sNatSet(0))
knownmsgs(proc("b"), transconf(sProcSet(proc("b")) sProcSet(proc("c")), 2, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)),
    eNatSet)
knownmsgs(proc("c"), regconf(sProcSet(proc("b")) sProcSet(proc("c")), 3), eNatSet)
knownmsgs(proc("c"), regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), sNatSet(0))
knownmsgs(proc("c"), transconf(sProcSet(proc("b")) sProcSet(proc("c")), 2, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)),
    eNatSet)

Solution 4 (state 130571)
states: 130583  rewrites: 9108816 in 298170ms cpu (308680ms real) (30549 rewrites/second)
s:State --> multicast-ack(proc("a"))
network(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")))
freshconf(5)
operational(proc("a"))
operational(proc("b"))
operational(proc("c"))
freshseq(1)
CONTROLLER(eController)
localconf(proc("a"), regconf(sProcSet(proc("a")), 3))
localconf(proc("b"), regconf(sProcSet(proc("b")) sProcSet(proc("c")), 4))
localconf(proc("c"), regconf(sProcSet(proc("b")) sProcSet(proc("c")), 4))
delivered(proc("a"), sMessageList(datamsg(proc("a"), agreed, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), 0, eNatSet, data(
    "test"))) sMessageList(transmsg(transconf(sProcSet(proc("a")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0))))
    sMessageList(confmsg(regconf(sProcSet(proc("a")), 3), sProcSet(proc("a")))))
delivered(proc("b"), sMessageList(datamsg(proc("a"), agreed, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), 0, eNatSet, data(
    "test"))) sMessageList(transmsg(transconf(sProcSet(proc("b")) sProcSet(proc("c")), 2, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc(
    "c")), 0)))) sMessageList(confmsg(regconf(sProcSet(proc("b")) sProcSet(proc("c")), 4), sProcSet(proc("b")) sProcSet(proc("c")))))
delivered(proc("c"), sMessageList(datamsg(proc("a"), agreed, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), 0, eNatSet, data(
    "test"))) sMessageList(transmsg(transconf(sProcSet(proc("b")) sProcSet(proc("c")), 2, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc(
    "c")), 0)))) sMessageList(confmsg(regconf(sProcSet(proc("b")) sProcSet(proc("c")), 4), sProcSet(proc("b")) sProcSet(proc("c")))))
alldelivered(proc("a"), sMessageList(datamsg(proc("a"), agreed, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), 0, eNatSet,
    data("test"))) sMessageList(transmsg(transconf(sProcSet(proc("a")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0))))
    sMessageList(confmsg(regconf(sProcSet(proc("a")), 3), sProcSet(proc("a")))))
alldelivered(proc("b"), sMessageList(datamsg(proc("a"), agreed, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), 0, eNatSet,
    data("test"))) sMessageList(transmsg(transconf(sProcSet(proc("b")) sProcSet(proc("c")), 2, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(
    proc("c")), 0)))) sMessageList(confmsg(regconf(sProcSet(proc("b")) sProcSet(proc("c")), 4), sProcSet(proc("b")) sProcSet(proc("c")))))
alldelivered(proc("c"), sMessageList(datamsg(proc("a"), agreed, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), 0, eNatSet,
    data("test"))) sMessageList(transmsg(transconf(sProcSet(proc("b")) sProcSet(proc("c")), 2, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(
    proc("c")), 0)))) sMessageList(confmsg(regconf(sProcSet(proc("b")) sProcSet(proc("c")), 4), sProcSet(proc("b")) sProcSet(proc("c")))))
reachable(proc("a"), sProcSet(proc("a")))
reachable(proc("b"), sProcSet(proc("b")) sProcSet(proc("c")))
reachable(proc("c"), sProcSet(proc("b")) sProcSet(proc("c")))
sent(proc("a"), eBroadcastSet)
sent(proc("b"), eBroadcastSet)
sent(proc("c"), eBroadcastSet)
received(proc("a"), eMessageSet)
received(proc("b"), eMessageSet)
received(proc("c"), eMessageSet)
acked(proc("a"), eMessageSet)
acked(proc("b"), eMessageSet)
acked(proc("c"), eMessageSet)
causalorder(regconf(sProcSet(proc("a")), 3), eConstraintSet)
causalorder(regconf(sProcSet(proc("b")) sProcSet(proc("c")), 4), eConstraintSet)
causalorder(regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), eConstraintSet)
causalorder(transconf(sProcSet(proc("a")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), eConstraintSet)
causalorder(transconf(sProcSet(proc("b")) sProcSet(proc("c")), 2, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)),
    eConstraintSet)
totalorder(regconf(sProcSet(proc("a")), 3), eEventList)
totalorder(regconf(sProcSet(proc("b")) sProcSet(proc("c")), 4), eEventList)
totalorder(regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), sEventList(event(proc("a"), 0)) sEventList(event(proc("a"), 0))
    sEventList(event(proc("a"), 0)))
totalorder(transconf(sProcSet(proc("a")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), sEventList(event(proc("a"), 0))
    sEventList(event(proc("a"), 0)) sEventList(event(proc("a"), 0)))
totalorder(transconf(sProcSet(proc("b")) sProcSet(proc("c")), 2, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), sEventList(
    event(proc("a"), 0)) sEventList(event(proc("a"), 0)) sEventList(event(proc("a"), 0)))
localmsgs(proc("a"), regconf(sProcSet(proc("a")), 3), eNatSet)
localmsgs(proc("a"), regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), sNatSet(0))
localmsgs(proc("a"), transconf(sProcSet(proc("a")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), eNatSet)
localmsgs(proc("b"), regconf(sProcSet(proc("b")) sProcSet(proc("c")), 4), eNatSet)
localmsgs(proc("b"), regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), eNatSet)
localmsgs(proc("b"), transconf(sProcSet(proc("b")) sProcSet(proc("c")), 2, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)),
    eNatSet)
localmsgs(proc("c"), regconf(sProcSet(proc("b")) sProcSet(proc("c")), 4), eNatSet)
localmsgs(proc("c"), regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), eNatSet)
localmsgs(proc("c"), transconf(sProcSet(proc("b")) sProcSet(proc("c")), 2, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)),
    eNatSet)
knownmsgs(proc("a"), regconf(sProcSet(proc("a")), 3), eNatSet)
knownmsgs(proc("a"), regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), sNatSet(0))
knownmsgs(proc("a"), transconf(sProcSet(proc("a")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), eNatSet)
knownmsgs(proc("b"), regconf(sProcSet(proc("b")) sProcSet(proc("c")), 4), eNatSet)
knownmsgs(proc("b"), regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), sNatSet(0))
knownmsgs(proc("b"), transconf(sProcSet(proc("b")) sProcSet(proc("c")), 2, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)),
    eNatSet)
knownmsgs(proc("c"), regconf(sProcSet(proc("b")) sProcSet(proc("c")), 4), eNatSet)
knownmsgs(proc("c"), regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), sNatSet(0))
knownmsgs(proc("c"), transconf(sProcSet(proc("b")) sProcSet(proc("c")), 2, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)),
    eNatSet)

Solution 5 (state 130572)
states: 130583  rewrites: 9108818 in 298190ms cpu (308840ms real) (30547 rewrites/second)
s:State --> multicast-ack(proc("a"))
network(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")))
freshconf(5)
operational(proc("a"))
operational(proc("b"))
operational(proc("c"))
freshseq(1)
CONTROLLER(eController)
localconf(proc("a"), regconf(sProcSet(proc("a")), 4))
localconf(proc("b"), regconf(sProcSet(proc("b")) sProcSet(proc("c")), 3))
localconf(proc("c"), regconf(sProcSet(proc("b")) sProcSet(proc("c")), 3))
delivered(proc("a"), sMessageList(datamsg(proc("a"), agreed, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), 0, eNatSet, data(
    "test"))) sMessageList(transmsg(transconf(sProcSet(proc("a")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0))))
    sMessageList(confmsg(regconf(sProcSet(proc("a")), 4), sProcSet(proc("a")))))
delivered(proc("b"), sMessageList(datamsg(proc("a"), agreed, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), 0, eNatSet, data(
    "test"))) sMessageList(transmsg(transconf(sProcSet(proc("b")) sProcSet(proc("c")), 2, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc(
    "c")), 0)))) sMessageList(confmsg(regconf(sProcSet(proc("b")) sProcSet(proc("c")), 3), sProcSet(proc("b")) sProcSet(proc("c")))))
delivered(proc("c"), sMessageList(datamsg(proc("a"), agreed, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), 0, eNatSet, data(
    "test"))) sMessageList(transmsg(transconf(sProcSet(proc("b")) sProcSet(proc("c")), 2, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc(
    "c")), 0)))) sMessageList(confmsg(regconf(sProcSet(proc("b")) sProcSet(proc("c")), 3), sProcSet(proc("b")) sProcSet(proc("c")))))
alldelivered(proc("a"), sMessageList(datamsg(proc("a"), agreed, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), 0, eNatSet,
    data("test"))) sMessageList(transmsg(transconf(sProcSet(proc("a")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0))))
    sMessageList(confmsg(regconf(sProcSet(proc("a")), 4), sProcSet(proc("a")))))
alldelivered(proc("b"), sMessageList(datamsg(proc("a"), agreed, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), 0, eNatSet,
    data("test"))) sMessageList(transmsg(transconf(sProcSet(proc("b")) sProcSet(proc("c")), 2, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(
    proc("c")), 0)))) sMessageList(confmsg(regconf(sProcSet(proc("b")) sProcSet(proc("c")), 3), sProcSet(proc("b")) sProcSet(proc("c")))))
alldelivered(proc("c"), sMessageList(datamsg(proc("a"), agreed, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), 0, eNatSet,
    data("test"))) sMessageList(transmsg(transconf(sProcSet(proc("b")) sProcSet(proc("c")), 2, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(
    proc("c")), 0)))) sMessageList(confmsg(regconf(sProcSet(proc("b")) sProcSet(proc("c")), 3), sProcSet(proc("b")) sProcSet(proc("c")))))
reachable(proc("a"), sProcSet(proc("a")))
reachable(proc("b"), sProcSet(proc("b")) sProcSet(proc("c")))
reachable(proc("c"), sProcSet(proc("b")) sProcSet(proc("c")))
sent(proc("a"), eBroadcastSet)
sent(proc("b"), eBroadcastSet)
sent(proc("c"), eBroadcastSet)
received(proc("a"), eMessageSet)
received(proc("b"), eMessageSet)
received(proc("c"), eMessageSet)
acked(proc("a"), eMessageSet)
acked(proc("b"), eMessageSet)
acked(proc("c"), eMessageSet)
causalorder(regconf(sProcSet(proc("a")), 4), eConstraintSet)
causalorder(regconf(sProcSet(proc("b")) sProcSet(proc("c")), 3), eConstraintSet)
causalorder(regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), eConstraintSet)
causalorder(transconf(sProcSet(proc("a")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), eConstraintSet)
causalorder(transconf(sProcSet(proc("b")) sProcSet(proc("c")), 2, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)),
    eConstraintSet)
totalorder(regconf(sProcSet(proc("a")), 4), eEventList)
totalorder(regconf(sProcSet(proc("b")) sProcSet(proc("c")), 3), eEventList)
totalorder(regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), sEventList(event(proc("a"), 0)) sEventList(event(proc("a"), 0))
    sEventList(event(proc("a"), 0)))
totalorder(transconf(sProcSet(proc("a")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), sEventList(event(proc("a"), 0))
    sEventList(event(proc("a"), 0)) sEventList(event(proc("a"), 0)))
totalorder(transconf(sProcSet(proc("b")) sProcSet(proc("c")), 2, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), sEventList(
    event(proc("a"), 0)) sEventList(event(proc("a"), 0)) sEventList(event(proc("a"), 0)))
localmsgs(proc("a"), regconf(sProcSet(proc("a")), 4), eNatSet)
localmsgs(proc("a"), regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), sNatSet(0))
localmsgs(proc("a"), transconf(sProcSet(proc("a")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), eNatSet)
localmsgs(proc("b"), regconf(sProcSet(proc("b")) sProcSet(proc("c")), 3), eNatSet)
localmsgs(proc("b"), regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), eNatSet)
localmsgs(proc("b"), transconf(sProcSet(proc("b")) sProcSet(proc("c")), 2, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)),
    eNatSet)
localmsgs(proc("c"), regconf(sProcSet(proc("b")) sProcSet(proc("c")), 3), eNatSet)
localmsgs(proc("c"), regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), eNatSet)
localmsgs(proc("c"), transconf(sProcSet(proc("b")) sProcSet(proc("c")), 2, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)),
    eNatSet)
knownmsgs(proc("a"), regconf(sProcSet(proc("a")), 4), eNatSet)
knownmsgs(proc("a"), regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), sNatSet(0))
knownmsgs(proc("a"), transconf(sProcSet(proc("a")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), eNatSet)
knownmsgs(proc("b"), regconf(sProcSet(proc("b")) sProcSet(proc("c")), 3), eNatSet)
knownmsgs(proc("b"), regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), sNatSet(0))
knownmsgs(proc("b"), transconf(sProcSet(proc("b")) sProcSet(proc("c")), 2, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)),
    eNatSet)
knownmsgs(proc("c"), regconf(sProcSet(proc("b")) sProcSet(proc("c")), 3), eNatSet)
knownmsgs(proc("c"), regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), sNatSet(0))
knownmsgs(proc("c"), transconf(sProcSet(proc("b")) sProcSet(proc("c")), 2, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)),
    eNatSet)

Solution 6 (state 130573)
states: 130583  rewrites: 9108820 in 298190ms cpu (308980ms real) (30547 rewrites/second)
s:State --> multicast-ack(proc("a"))
network(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")))
freshconf(5)
operational(proc("a"))
operational(proc("b"))
operational(proc("c"))
freshseq(1)
CONTROLLER(eController)
localconf(proc("a"), regconf(sProcSet(proc("a")), 2))
localconf(proc("b"), regconf(sProcSet(proc("b")) sProcSet(proc("c")), 4))
localconf(proc("c"), regconf(sProcSet(proc("b")) sProcSet(proc("c")), 4))
delivered(proc("a"), sMessageList(datamsg(proc("a"), agreed, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), 0, eNatSet, data(
    "test"))) sMessageList(transmsg(transconf(sProcSet(proc("a")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0))))
    sMessageList(confmsg(regconf(sProcSet(proc("a")), 2), sProcSet(proc("a")))))
delivered(proc("b"), sMessageList(datamsg(proc("a"), agreed, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), 0, eNatSet, data(
    "test"))) sMessageList(transmsg(transconf(sProcSet(proc("b")) sProcSet(proc("c")), 3, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc(
    "c")), 0)))) sMessageList(confmsg(regconf(sProcSet(proc("b")) sProcSet(proc("c")), 4), sProcSet(proc("b")) sProcSet(proc("c")))))
delivered(proc("c"), sMessageList(datamsg(proc("a"), agreed, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), 0, eNatSet, data(
    "test"))) sMessageList(transmsg(transconf(sProcSet(proc("b")) sProcSet(proc("c")), 3, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc(
    "c")), 0)))) sMessageList(confmsg(regconf(sProcSet(proc("b")) sProcSet(proc("c")), 4), sProcSet(proc("b")) sProcSet(proc("c")))))
alldelivered(proc("a"), sMessageList(datamsg(proc("a"), agreed, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), 0, eNatSet,
    data("test"))) sMessageList(transmsg(transconf(sProcSet(proc("a")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0))))
    sMessageList(confmsg(regconf(sProcSet(proc("a")), 2), sProcSet(proc("a")))))
alldelivered(proc("b"), sMessageList(datamsg(proc("a"), agreed, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), 0, eNatSet,
    data("test"))) sMessageList(transmsg(transconf(sProcSet(proc("b")) sProcSet(proc("c")), 3, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(
    proc("c")), 0)))) sMessageList(confmsg(regconf(sProcSet(proc("b")) sProcSet(proc("c")), 4), sProcSet(proc("b")) sProcSet(proc("c")))))
alldelivered(proc("c"), sMessageList(datamsg(proc("a"), agreed, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), 0, eNatSet,
    data("test"))) sMessageList(transmsg(transconf(sProcSet(proc("b")) sProcSet(proc("c")), 3, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(
    proc("c")), 0)))) sMessageList(confmsg(regconf(sProcSet(proc("b")) sProcSet(proc("c")), 4), sProcSet(proc("b")) sProcSet(proc("c")))))
reachable(proc("a"), sProcSet(proc("a")))
reachable(proc("b"), sProcSet(proc("b")) sProcSet(proc("c")))
reachable(proc("c"), sProcSet(proc("b")) sProcSet(proc("c")))
sent(proc("a"), eBroadcastSet)
sent(proc("b"), eBroadcastSet)
sent(proc("c"), eBroadcastSet)
received(proc("a"), eMessageSet)
received(proc("b"), eMessageSet)
received(proc("c"), eMessageSet)
acked(proc("a"), eMessageSet)
acked(proc("b"), eMessageSet)
acked(proc("c"), eMessageSet)
causalorder(regconf(sProcSet(proc("a")), 2), eConstraintSet)
causalorder(regconf(sProcSet(proc("b")) sProcSet(proc("c")), 4), eConstraintSet)
causalorder(regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), eConstraintSet)
causalorder(transconf(sProcSet(proc("a")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), eConstraintSet)
causalorder(transconf(sProcSet(proc("b")) sProcSet(proc("c")), 3, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)),
    eConstraintSet)
totalorder(regconf(sProcSet(proc("a")), 2), eEventList)
totalorder(regconf(sProcSet(proc("b")) sProcSet(proc("c")), 4), eEventList)
totalorder(regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), sEventList(event(proc("a"), 0)) sEventList(event(proc("a"), 0))
    sEventList(event(proc("a"), 0)))
totalorder(transconf(sProcSet(proc("a")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), sEventList(event(proc("a"), 0))
    sEventList(event(proc("a"), 0)) sEventList(event(proc("a"), 0)))
totalorder(transconf(sProcSet(proc("b")) sProcSet(proc("c")), 3, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), sEventList(
    event(proc("a"), 0)) sEventList(event(proc("a"), 0)) sEventList(event(proc("a"), 0)))
localmsgs(proc("a"), regconf(sProcSet(proc("a")), 2), eNatSet)
localmsgs(proc("a"), regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), sNatSet(0))
localmsgs(proc("a"), transconf(sProcSet(proc("a")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), eNatSet)
localmsgs(proc("b"), regconf(sProcSet(proc("b")) sProcSet(proc("c")), 4), eNatSet)
localmsgs(proc("b"), regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), eNatSet)
localmsgs(proc("b"), transconf(sProcSet(proc("b")) sProcSet(proc("c")), 3, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)),
    eNatSet)
localmsgs(proc("c"), regconf(sProcSet(proc("b")) sProcSet(proc("c")), 4), eNatSet)
localmsgs(proc("c"), regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), eNatSet)
localmsgs(proc("c"), transconf(sProcSet(proc("b")) sProcSet(proc("c")), 3, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)),
    eNatSet)
knownmsgs(proc("a"), regconf(sProcSet(proc("a")), 2), eNatSet)
knownmsgs(proc("a"), regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), sNatSet(0))
knownmsgs(proc("a"), transconf(sProcSet(proc("a")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), eNatSet)
knownmsgs(proc("b"), regconf(sProcSet(proc("b")) sProcSet(proc("c")), 4), eNatSet)
knownmsgs(proc("b"), regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), sNatSet(0))
knownmsgs(proc("b"), transconf(sProcSet(proc("b")) sProcSet(proc("c")), 3, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)),
    eNatSet)
knownmsgs(proc("c"), regconf(sProcSet(proc("b")) sProcSet(proc("c")), 4), eNatSet)
knownmsgs(proc("c"), regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), sNatSet(0))
knownmsgs(proc("c"), transconf(sProcSet(proc("b")) sProcSet(proc("c")), 3, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)),
    eNatSet)

Solution 7 (state 130574)
states: 130583  rewrites: 9108822 in 298200ms cpu (309080ms real) (30546 rewrites/second)
s:State --> multicast-ack(proc("a"))
network(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")))
freshconf(5)
operational(proc("a"))
operational(proc("b"))
operational(proc("c"))
freshseq(1)
CONTROLLER(eController)
localconf(proc("a"), regconf(sProcSet(proc("a")), 3))
localconf(proc("b"), regconf(sProcSet(proc("b")) sProcSet(proc("c")), 4))
localconf(proc("c"), regconf(sProcSet(proc("b")) sProcSet(proc("c")), 4))
delivered(proc("a"), sMessageList(datamsg(proc("a"), agreed, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), 0, eNatSet, data(
    "test"))) sMessageList(transmsg(transconf(sProcSet(proc("a")), 2, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0))))
    sMessageList(confmsg(regconf(sProcSet(proc("a")), 3), sProcSet(proc("a")))))
delivered(proc("b"), sMessageList(datamsg(proc("a"), agreed, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), 0, eNatSet, data(
    "test"))) sMessageList(transmsg(transconf(sProcSet(proc("b")) sProcSet(proc("c")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc(
    "c")), 0)))) sMessageList(confmsg(regconf(sProcSet(proc("b")) sProcSet(proc("c")), 4), sProcSet(proc("b")) sProcSet(proc("c")))))
delivered(proc("c"), sMessageList(datamsg(proc("a"), agreed, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), 0, eNatSet, data(
    "test"))) sMessageList(transmsg(transconf(sProcSet(proc("b")) sProcSet(proc("c")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc(
    "c")), 0)))) sMessageList(confmsg(regconf(sProcSet(proc("b")) sProcSet(proc("c")), 4), sProcSet(proc("b")) sProcSet(proc("c")))))
alldelivered(proc("a"), sMessageList(datamsg(proc("a"), agreed, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), 0, eNatSet,
    data("test"))) sMessageList(transmsg(transconf(sProcSet(proc("a")), 2, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0))))
    sMessageList(confmsg(regconf(sProcSet(proc("a")), 3), sProcSet(proc("a")))))
alldelivered(proc("b"), sMessageList(datamsg(proc("a"), agreed, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), 0, eNatSet,
    data("test"))) sMessageList(transmsg(transconf(sProcSet(proc("b")) sProcSet(proc("c")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(
    proc("c")), 0)))) sMessageList(confmsg(regconf(sProcSet(proc("b")) sProcSet(proc("c")), 4), sProcSet(proc("b")) sProcSet(proc("c")))))
alldelivered(proc("c"), sMessageList(datamsg(proc("a"), agreed, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), 0, eNatSet,
    data("test"))) sMessageList(transmsg(transconf(sProcSet(proc("b")) sProcSet(proc("c")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(
    proc("c")), 0)))) sMessageList(confmsg(regconf(sProcSet(proc("b")) sProcSet(proc("c")), 4), sProcSet(proc("b")) sProcSet(proc("c")))))
reachable(proc("a"), sProcSet(proc("a")))
reachable(proc("b"), sProcSet(proc("b")) sProcSet(proc("c")))
reachable(proc("c"), sProcSet(proc("b")) sProcSet(proc("c")))
sent(proc("a"), eBroadcastSet)
sent(proc("b"), eBroadcastSet)
sent(proc("c"), eBroadcastSet)
received(proc("a"), eMessageSet)
received(proc("b"), eMessageSet)
received(proc("c"), eMessageSet)
acked(proc("a"), eMessageSet)
acked(proc("b"), eMessageSet)
acked(proc("c"), eMessageSet)
causalorder(regconf(sProcSet(proc("a")), 3), eConstraintSet)
causalorder(regconf(sProcSet(proc("b")) sProcSet(proc("c")), 4), eConstraintSet)
causalorder(regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), eConstraintSet)
causalorder(transconf(sProcSet(proc("a")), 2, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), eConstraintSet)
causalorder(transconf(sProcSet(proc("b")) sProcSet(proc("c")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)),
    eConstraintSet)
totalorder(regconf(sProcSet(proc("a")), 3), eEventList)
totalorder(regconf(sProcSet(proc("b")) sProcSet(proc("c")), 4), eEventList)
totalorder(regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), sEventList(event(proc("a"), 0)) sEventList(event(proc("a"), 0))
    sEventList(event(proc("a"), 0)))
totalorder(transconf(sProcSet(proc("a")), 2, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), sEventList(event(proc("a"), 0))
    sEventList(event(proc("a"), 0)) sEventList(event(proc("a"), 0)))
totalorder(transconf(sProcSet(proc("b")) sProcSet(proc("c")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), sEventList(
    event(proc("a"), 0)) sEventList(event(proc("a"), 0)) sEventList(event(proc("a"), 0)))
localmsgs(proc("a"), regconf(sProcSet(proc("a")), 3), eNatSet)
localmsgs(proc("a"), regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), sNatSet(0))
localmsgs(proc("a"), transconf(sProcSet(proc("a")), 2, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), eNatSet)
localmsgs(proc("b"), regconf(sProcSet(proc("b")) sProcSet(proc("c")), 4), eNatSet)
localmsgs(proc("b"), regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), eNatSet)
localmsgs(proc("b"), transconf(sProcSet(proc("b")) sProcSet(proc("c")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)),
    eNatSet)
localmsgs(proc("c"), regconf(sProcSet(proc("b")) sProcSet(proc("c")), 4), eNatSet)
localmsgs(proc("c"), regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), eNatSet)
localmsgs(proc("c"), transconf(sProcSet(proc("b")) sProcSet(proc("c")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)),
    eNatSet)
knownmsgs(proc("a"), regconf(sProcSet(proc("a")), 3), eNatSet)
knownmsgs(proc("a"), regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), sNatSet(0))
knownmsgs(proc("a"), transconf(sProcSet(proc("a")), 2, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), eNatSet)
knownmsgs(proc("b"), regconf(sProcSet(proc("b")) sProcSet(proc("c")), 4), eNatSet)
knownmsgs(proc("b"), regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), sNatSet(0))
knownmsgs(proc("b"), transconf(sProcSet(proc("b")) sProcSet(proc("c")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)),
    eNatSet)
knownmsgs(proc("c"), regconf(sProcSet(proc("b")) sProcSet(proc("c")), 4), eNatSet)
knownmsgs(proc("c"), regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), sNatSet(0))
knownmsgs(proc("c"), transconf(sProcSet(proc("b")) sProcSet(proc("c")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)),
    eNatSet)

Solution 8 (state 130575)
states: 130583  rewrites: 9108824 in 298200ms cpu (309100ms real) (30546 rewrites/second)
s:State --> multicast-ack(proc("a"))
network(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")))
freshconf(5)
operational(proc("a"))
operational(proc("b"))
operational(proc("c"))
freshseq(1)
CONTROLLER(eController)
localconf(proc("a"), regconf(sProcSet(proc("a")), 4))
localconf(proc("b"), regconf(sProcSet(proc("b")) sProcSet(proc("c")), 3))
localconf(proc("c"), regconf(sProcSet(proc("b")) sProcSet(proc("c")), 3))
delivered(proc("a"), sMessageList(datamsg(proc("a"), agreed, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), 0, eNatSet, data(
    "test"))) sMessageList(transmsg(transconf(sProcSet(proc("a")), 2, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0))))
    sMessageList(confmsg(regconf(sProcSet(proc("a")), 4), sProcSet(proc("a")))))
delivered(proc("b"), sMessageList(datamsg(proc("a"), agreed, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), 0, eNatSet, data(
    "test"))) sMessageList(transmsg(transconf(sProcSet(proc("b")) sProcSet(proc("c")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc(
    "c")), 0)))) sMessageList(confmsg(regconf(sProcSet(proc("b")) sProcSet(proc("c")), 3), sProcSet(proc("b")) sProcSet(proc("c")))))
delivered(proc("c"), sMessageList(datamsg(proc("a"), agreed, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), 0, eNatSet, data(
    "test"))) sMessageList(transmsg(transconf(sProcSet(proc("b")) sProcSet(proc("c")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc(
    "c")), 0)))) sMessageList(confmsg(regconf(sProcSet(proc("b")) sProcSet(proc("c")), 3), sProcSet(proc("b")) sProcSet(proc("c")))))
alldelivered(proc("a"), sMessageList(datamsg(proc("a"), agreed, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), 0, eNatSet,
    data("test"))) sMessageList(transmsg(transconf(sProcSet(proc("a")), 2, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0))))
    sMessageList(confmsg(regconf(sProcSet(proc("a")), 4), sProcSet(proc("a")))))
alldelivered(proc("b"), sMessageList(datamsg(proc("a"), agreed, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), 0, eNatSet,
    data("test"))) sMessageList(transmsg(transconf(sProcSet(proc("b")) sProcSet(proc("c")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(
    proc("c")), 0)))) sMessageList(confmsg(regconf(sProcSet(proc("b")) sProcSet(proc("c")), 3), sProcSet(proc("b")) sProcSet(proc("c")))))
alldelivered(proc("c"), sMessageList(datamsg(proc("a"), agreed, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), 0, eNatSet,
    data("test"))) sMessageList(transmsg(transconf(sProcSet(proc("b")) sProcSet(proc("c")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(
    proc("c")), 0)))) sMessageList(confmsg(regconf(sProcSet(proc("b")) sProcSet(proc("c")), 3), sProcSet(proc("b")) sProcSet(proc("c")))))
reachable(proc("a"), sProcSet(proc("a")))
reachable(proc("b"), sProcSet(proc("b")) sProcSet(proc("c")))
reachable(proc("c"), sProcSet(proc("b")) sProcSet(proc("c")))
sent(proc("a"), eBroadcastSet)
sent(proc("b"), eBroadcastSet)
sent(proc("c"), eBroadcastSet)
received(proc("a"), eMessageSet)
received(proc("b"), eMessageSet)
received(proc("c"), eMessageSet)
acked(proc("a"), eMessageSet)
acked(proc("b"), eMessageSet)
acked(proc("c"), eMessageSet)
causalorder(regconf(sProcSet(proc("a")), 4), eConstraintSet)
causalorder(regconf(sProcSet(proc("b")) sProcSet(proc("c")), 3), eConstraintSet)
causalorder(regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), eConstraintSet)
causalorder(transconf(sProcSet(proc("a")), 2, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), eConstraintSet)
causalorder(transconf(sProcSet(proc("b")) sProcSet(proc("c")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)),
    eConstraintSet)
totalorder(regconf(sProcSet(proc("a")), 4), eEventList)
totalorder(regconf(sProcSet(proc("b")) sProcSet(proc("c")), 3), eEventList)
totalorder(regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), sEventList(event(proc("a"), 0)) sEventList(event(proc("a"), 0))
    sEventList(event(proc("a"), 0)))
totalorder(transconf(sProcSet(proc("a")), 2, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), sEventList(event(proc("a"), 0))
    sEventList(event(proc("a"), 0)) sEventList(event(proc("a"), 0)))
totalorder(transconf(sProcSet(proc("b")) sProcSet(proc("c")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), sEventList(
    event(proc("a"), 0)) sEventList(event(proc("a"), 0)) sEventList(event(proc("a"), 0)))
localmsgs(proc("a"), regconf(sProcSet(proc("a")), 4), eNatSet)
localmsgs(proc("a"), regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), sNatSet(0))
localmsgs(proc("a"), transconf(sProcSet(proc("a")), 2, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), eNatSet)
localmsgs(proc("b"), regconf(sProcSet(proc("b")) sProcSet(proc("c")), 3), eNatSet)
localmsgs(proc("b"), regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), eNatSet)
localmsgs(proc("b"), transconf(sProcSet(proc("b")) sProcSet(proc("c")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)),
    eNatSet)
localmsgs(proc("c"), regconf(sProcSet(proc("b")) sProcSet(proc("c")), 3), eNatSet)
localmsgs(proc("c"), regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), eNatSet)
localmsgs(proc("c"), transconf(sProcSet(proc("b")) sProcSet(proc("c")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)),
    eNatSet)
knownmsgs(proc("a"), regconf(sProcSet(proc("a")), 4), eNatSet)
knownmsgs(proc("a"), regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), sNatSet(0))
knownmsgs(proc("a"), transconf(sProcSet(proc("a")), 2, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), eNatSet)
knownmsgs(proc("b"), regconf(sProcSet(proc("b")) sProcSet(proc("c")), 3), eNatSet)
knownmsgs(proc("b"), regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), sNatSet(0))
knownmsgs(proc("b"), transconf(sProcSet(proc("b")) sProcSet(proc("c")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)),
    eNatSet)
knownmsgs(proc("c"), regconf(sProcSet(proc("b")) sProcSet(proc("c")), 3), eNatSet)
knownmsgs(proc("c"), regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), sNatSet(0))
knownmsgs(proc("c"), transconf(sProcSet(proc("b")) sProcSet(proc("c")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)),
    eNatSet)

Solution 9 (state 130576)
states: 130583  rewrites: 9108826 in 298210ms cpu (309310ms real) (30545 rewrites/second)
s:State --> multicast-ack(proc("a"))
network(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")))
freshconf(5)
operational(proc("a"))
operational(proc("b"))
operational(proc("c"))
freshseq(1)
CONTROLLER(eController)
localconf(proc("a"), regconf(sProcSet(proc("a")), 4))
localconf(proc("b"), regconf(sProcSet(proc("b")) sProcSet(proc("c")), 2))
localconf(proc("c"), regconf(sProcSet(proc("b")) sProcSet(proc("c")), 2))
delivered(proc("a"), sMessageList(datamsg(proc("a"), agreed, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), 0, eNatSet, data(
    "test"))) sMessageList(transmsg(transconf(sProcSet(proc("a")), 3, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0))))
    sMessageList(confmsg(regconf(sProcSet(proc("a")), 4), sProcSet(proc("a")))))
delivered(proc("b"), sMessageList(datamsg(proc("a"), agreed, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), 0, eNatSet, data(
    "test"))) sMessageList(transmsg(transconf(sProcSet(proc("b")) sProcSet(proc("c")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc(
    "c")), 0)))) sMessageList(confmsg(regconf(sProcSet(proc("b")) sProcSet(proc("c")), 2), sProcSet(proc("b")) sProcSet(proc("c")))))
delivered(proc("c"), sMessageList(datamsg(proc("a"), agreed, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), 0, eNatSet, data(
    "test"))) sMessageList(transmsg(transconf(sProcSet(proc("b")) sProcSet(proc("c")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc(
    "c")), 0)))) sMessageList(confmsg(regconf(sProcSet(proc("b")) sProcSet(proc("c")), 2), sProcSet(proc("b")) sProcSet(proc("c")))))
alldelivered(proc("a"), sMessageList(datamsg(proc("a"), agreed, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), 0, eNatSet,
    data("test"))) sMessageList(transmsg(transconf(sProcSet(proc("a")), 3, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0))))
    sMessageList(confmsg(regconf(sProcSet(proc("a")), 4), sProcSet(proc("a")))))
alldelivered(proc("b"), sMessageList(datamsg(proc("a"), agreed, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), 0, eNatSet,
    data("test"))) sMessageList(transmsg(transconf(sProcSet(proc("b")) sProcSet(proc("c")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(
    proc("c")), 0)))) sMessageList(confmsg(regconf(sProcSet(proc("b")) sProcSet(proc("c")), 2), sProcSet(proc("b")) sProcSet(proc("c")))))
alldelivered(proc("c"), sMessageList(datamsg(proc("a"), agreed, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), 0, eNatSet,
    data("test"))) sMessageList(transmsg(transconf(sProcSet(proc("b")) sProcSet(proc("c")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(
    proc("c")), 0)))) sMessageList(confmsg(regconf(sProcSet(proc("b")) sProcSet(proc("c")), 2), sProcSet(proc("b")) sProcSet(proc("c")))))
reachable(proc("a"), sProcSet(proc("a")))
reachable(proc("b"), sProcSet(proc("b")) sProcSet(proc("c")))
reachable(proc("c"), sProcSet(proc("b")) sProcSet(proc("c")))
sent(proc("a"), eBroadcastSet)
sent(proc("b"), eBroadcastSet)
sent(proc("c"), eBroadcastSet)
received(proc("a"), eMessageSet)
received(proc("b"), eMessageSet)
received(proc("c"), eMessageSet)
acked(proc("a"), eMessageSet)
acked(proc("b"), eMessageSet)
acked(proc("c"), eMessageSet)
causalorder(regconf(sProcSet(proc("a")), 4), eConstraintSet)
causalorder(regconf(sProcSet(proc("b")) sProcSet(proc("c")), 2), eConstraintSet)
causalorder(regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), eConstraintSet)
causalorder(transconf(sProcSet(proc("a")), 3, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), eConstraintSet)
causalorder(transconf(sProcSet(proc("b")) sProcSet(proc("c")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)),
    eConstraintSet)
totalorder(regconf(sProcSet(proc("a")), 4), eEventList)
totalorder(regconf(sProcSet(proc("b")) sProcSet(proc("c")), 2), eEventList)
totalorder(regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), sEventList(event(proc("a"), 0)) sEventList(event(proc("a"), 0))
    sEventList(event(proc("a"), 0)))
totalorder(transconf(sProcSet(proc("a")), 3, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), sEventList(event(proc("a"), 0))
    sEventList(event(proc("a"), 0)) sEventList(event(proc("a"), 0)))
totalorder(transconf(sProcSet(proc("b")) sProcSet(proc("c")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), sEventList(
    event(proc("a"), 0)) sEventList(event(proc("a"), 0)) sEventList(event(proc("a"), 0)))
localmsgs(proc("a"), regconf(sProcSet(proc("a")), 4), eNatSet)
localmsgs(proc("a"), regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), sNatSet(0))
localmsgs(proc("a"), transconf(sProcSet(proc("a")), 3, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), eNatSet)
localmsgs(proc("b"), regconf(sProcSet(proc("b")) sProcSet(proc("c")), 2), eNatSet)
localmsgs(proc("b"), regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), eNatSet)
localmsgs(proc("b"), transconf(sProcSet(proc("b")) sProcSet(proc("c")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)),
    eNatSet)
localmsgs(proc("c"), regconf(sProcSet(proc("b")) sProcSet(proc("c")), 2), eNatSet)
localmsgs(proc("c"), regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), eNatSet)
localmsgs(proc("c"), transconf(sProcSet(proc("b")) sProcSet(proc("c")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)),
    eNatSet)
knownmsgs(proc("a"), regconf(sProcSet(proc("a")), 4), eNatSet)
knownmsgs(proc("a"), regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), sNatSet(0))
knownmsgs(proc("a"), transconf(sProcSet(proc("a")), 3, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), eNatSet)
knownmsgs(proc("b"), regconf(sProcSet(proc("b")) sProcSet(proc("c")), 2), eNatSet)
knownmsgs(proc("b"), regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), sNatSet(0))
knownmsgs(proc("b"), transconf(sProcSet(proc("b")) sProcSet(proc("c")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)),
    eNatSet)
knownmsgs(proc("c"), regconf(sProcSet(proc("b")) sProcSet(proc("c")), 2), eNatSet)
knownmsgs(proc("c"), regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), sNatSet(0))
knownmsgs(proc("c"), transconf(sProcSet(proc("b")) sProcSet(proc("c")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)),
    eNatSet)

Solution 10 (state 130577)
states: 130583  rewrites: 9108828 in 298210ms cpu (309370ms real) (30545 rewrites/second)
s:State --> multicast-ack(proc("a"))
network(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")))
freshconf(5)
operational(proc("a"))
operational(proc("b"))
operational(proc("c"))
freshseq(1)
CONTROLLER(eController)
localconf(proc("a"), regconf(sProcSet(proc("a")), 2))
localconf(proc("b"), regconf(sProcSet(proc("b")) sProcSet(proc("c")), 4))
localconf(proc("c"), regconf(sProcSet(proc("b")) sProcSet(proc("c")), 4))
delivered(proc("a"), sMessageList(datamsg(proc("a"), agreed, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), 0, eNatSet, data(
    "test"))) sMessageList(transmsg(transconf(sProcSet(proc("a")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0))))
    sMessageList(confmsg(regconf(sProcSet(proc("a")), 2), sProcSet(proc("a")))))
delivered(proc("b"), sMessageList(datamsg(proc("a"), agreed, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), 0, eNatSet, data(
    "test"))) sMessageList(transmsg(transconf(sProcSet(proc("b")) sProcSet(proc("c")), 3, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc(
    "c")), 0)))) sMessageList(confmsg(regconf(sProcSet(proc("b")) sProcSet(proc("c")), 4), sProcSet(proc("b")) sProcSet(proc("c")))))
delivered(proc("c"), sMessageList(datamsg(proc("a"), agreed, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), 0, eNatSet, data(
    "test"))) sMessageList(transmsg(transconf(sProcSet(proc("b")) sProcSet(proc("c")), 3, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc(
    "c")), 0)))) sMessageList(confmsg(regconf(sProcSet(proc("b")) sProcSet(proc("c")), 4), sProcSet(proc("b")) sProcSet(proc("c")))))
alldelivered(proc("a"), sMessageList(datamsg(proc("a"), agreed, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), 0, eNatSet,
    data("test"))) sMessageList(transmsg(transconf(sProcSet(proc("a")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0))))
    sMessageList(confmsg(regconf(sProcSet(proc("a")), 2), sProcSet(proc("a")))))
alldelivered(proc("b"), sMessageList(datamsg(proc("a"), agreed, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), 0, eNatSet,
    data("test"))) sMessageList(transmsg(transconf(sProcSet(proc("b")) sProcSet(proc("c")), 3, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(
    proc("c")), 0)))) sMessageList(confmsg(regconf(sProcSet(proc("b")) sProcSet(proc("c")), 4), sProcSet(proc("b")) sProcSet(proc("c")))))
alldelivered(proc("c"), sMessageList(datamsg(proc("a"), agreed, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), 0, eNatSet,
    data("test"))) sMessageList(transmsg(transconf(sProcSet(proc("b")) sProcSet(proc("c")), 3, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(
    proc("c")), 0)))) sMessageList(confmsg(regconf(sProcSet(proc("b")) sProcSet(proc("c")), 4), sProcSet(proc("b")) sProcSet(proc("c")))))
reachable(proc("a"), sProcSet(proc("a")))
reachable(proc("b"), sProcSet(proc("b")) sProcSet(proc("c")))
reachable(proc("c"), sProcSet(proc("b")) sProcSet(proc("c")))
sent(proc("a"), eBroadcastSet)
sent(proc("b"), eBroadcastSet)
sent(proc("c"), eBroadcastSet)
received(proc("a"), eMessageSet)
received(proc("b"), eMessageSet)
received(proc("c"), eMessageSet)
acked(proc("a"), eMessageSet)
acked(proc("b"), eMessageSet)
acked(proc("c"), eMessageSet)
causalorder(regconf(sProcSet(proc("a")), 2), eConstraintSet)
causalorder(regconf(sProcSet(proc("b")) sProcSet(proc("c")), 4), eConstraintSet)
causalorder(regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), eConstraintSet)
causalorder(transconf(sProcSet(proc("a")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), eConstraintSet)
causalorder(transconf(sProcSet(proc("b")) sProcSet(proc("c")), 3, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)),
    eConstraintSet)
totalorder(regconf(sProcSet(proc("a")), 2), eEventList)
totalorder(regconf(sProcSet(proc("b")) sProcSet(proc("c")), 4), eEventList)
totalorder(regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), sEventList(event(proc("a"), 0)) sEventList(event(proc("a"), 0))
    sEventList(event(proc("a"), 0)))
totalorder(transconf(sProcSet(proc("a")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), sEventList(event(proc("a"), 0)))
totalorder(transconf(sProcSet(proc("b")) sProcSet(proc("c")), 3, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), sEventList(
    event(proc("a"), 0)) sEventList(event(proc("a"), 0)) sEventList(event(proc("a"), 0)))
localmsgs(proc("a"), regconf(sProcSet(proc("a")), 2), eNatSet)
localmsgs(proc("a"), regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), sNatSet(0))
localmsgs(proc("a"), transconf(sProcSet(proc("a")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), eNatSet)
localmsgs(proc("b"), regconf(sProcSet(proc("b")) sProcSet(proc("c")), 4), eNatSet)
localmsgs(proc("b"), regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), eNatSet)
localmsgs(proc("b"), transconf(sProcSet(proc("b")) sProcSet(proc("c")), 3, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)),
    eNatSet)
localmsgs(proc("c"), regconf(sProcSet(proc("b")) sProcSet(proc("c")), 4), eNatSet)
localmsgs(proc("c"), regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), eNatSet)
localmsgs(proc("c"), transconf(sProcSet(proc("b")) sProcSet(proc("c")), 3, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)),
    eNatSet)
knownmsgs(proc("a"), regconf(sProcSet(proc("a")), 2), eNatSet)
knownmsgs(proc("a"), regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), sNatSet(0))
knownmsgs(proc("a"), transconf(sProcSet(proc("a")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), eNatSet)
knownmsgs(proc("b"), regconf(sProcSet(proc("b")) sProcSet(proc("c")), 4), eNatSet)
knownmsgs(proc("b"), regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), sNatSet(0))
knownmsgs(proc("b"), transconf(sProcSet(proc("b")) sProcSet(proc("c")), 3, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)),
    eNatSet)
knownmsgs(proc("c"), regconf(sProcSet(proc("b")) sProcSet(proc("c")), 4), eNatSet)
knownmsgs(proc("c"), regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), sNatSet(0))
knownmsgs(proc("c"), transconf(sProcSet(proc("b")) sProcSet(proc("c")), 3, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)),
    eNatSet)

Solution 11 (state 130578)
states: 130583  rewrites: 9108830 in 298220ms cpu (309430ms real) (30543 rewrites/second)
s:State --> multicast-ack(proc("a"))
network(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")))
freshconf(5)
operational(proc("a"))
operational(proc("b"))
operational(proc("c"))
freshseq(1)
CONTROLLER(eController)
localconf(proc("a"), regconf(sProcSet(proc("a")), 3))
localconf(proc("b"), regconf(sProcSet(proc("b")) sProcSet(proc("c")), 4))
localconf(proc("c"), regconf(sProcSet(proc("b")) sProcSet(proc("c")), 4))
delivered(proc("a"), sMessageList(datamsg(proc("a"), agreed, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), 0, eNatSet, data(
    "test"))) sMessageList(transmsg(transconf(sProcSet(proc("a")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0))))
    sMessageList(confmsg(regconf(sProcSet(proc("a")), 3), sProcSet(proc("a")))))
delivered(proc("b"), sMessageList(datamsg(proc("a"), agreed, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), 0, eNatSet, data(
    "test"))) sMessageList(transmsg(transconf(sProcSet(proc("b")) sProcSet(proc("c")), 2, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc(
    "c")), 0)))) sMessageList(confmsg(regconf(sProcSet(proc("b")) sProcSet(proc("c")), 4), sProcSet(proc("b")) sProcSet(proc("c")))))
delivered(proc("c"), sMessageList(datamsg(proc("a"), agreed, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), 0, eNatSet, data(
    "test"))) sMessageList(transmsg(transconf(sProcSet(proc("b")) sProcSet(proc("c")), 2, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc(
    "c")), 0)))) sMessageList(confmsg(regconf(sProcSet(proc("b")) sProcSet(proc("c")), 4), sProcSet(proc("b")) sProcSet(proc("c")))))
alldelivered(proc("a"), sMessageList(datamsg(proc("a"), agreed, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), 0, eNatSet,
    data("test"))) sMessageList(transmsg(transconf(sProcSet(proc("a")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0))))
    sMessageList(confmsg(regconf(sProcSet(proc("a")), 3), sProcSet(proc("a")))))
alldelivered(proc("b"), sMessageList(datamsg(proc("a"), agreed, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), 0, eNatSet,
    data("test"))) sMessageList(transmsg(transconf(sProcSet(proc("b")) sProcSet(proc("c")), 2, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(
    proc("c")), 0)))) sMessageList(confmsg(regconf(sProcSet(proc("b")) sProcSet(proc("c")), 4), sProcSet(proc("b")) sProcSet(proc("c")))))
alldelivered(proc("c"), sMessageList(datamsg(proc("a"), agreed, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), 0, eNatSet,
    data("test"))) sMessageList(transmsg(transconf(sProcSet(proc("b")) sProcSet(proc("c")), 2, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(
    proc("c")), 0)))) sMessageList(confmsg(regconf(sProcSet(proc("b")) sProcSet(proc("c")), 4), sProcSet(proc("b")) sProcSet(proc("c")))))
reachable(proc("a"), sProcSet(proc("a")))
reachable(proc("b"), sProcSet(proc("b")) sProcSet(proc("c")))
reachable(proc("c"), sProcSet(proc("b")) sProcSet(proc("c")))
sent(proc("a"), eBroadcastSet)
sent(proc("b"), eBroadcastSet)
sent(proc("c"), eBroadcastSet)
received(proc("a"), eMessageSet)
received(proc("b"), eMessageSet)
received(proc("c"), eMessageSet)
acked(proc("a"), eMessageSet)
acked(proc("b"), eMessageSet)
acked(proc("c"), eMessageSet)
causalorder(regconf(sProcSet(proc("a")), 3), eConstraintSet)
causalorder(regconf(sProcSet(proc("b")) sProcSet(proc("c")), 4), eConstraintSet)
causalorder(regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), eConstraintSet)
causalorder(transconf(sProcSet(proc("a")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), eConstraintSet)
causalorder(transconf(sProcSet(proc("b")) sProcSet(proc("c")), 2, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)),
    eConstraintSet)
totalorder(regconf(sProcSet(proc("a")), 3), eEventList)
totalorder(regconf(sProcSet(proc("b")) sProcSet(proc("c")), 4), eEventList)
totalorder(regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), sEventList(event(proc("a"), 0)) sEventList(event(proc("a"), 0))
    sEventList(event(proc("a"), 0)))
totalorder(transconf(sProcSet(proc("a")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), sEventList(event(proc("a"), 0)))
totalorder(transconf(sProcSet(proc("b")) sProcSet(proc("c")), 2, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), sEventList(
    event(proc("a"), 0)) sEventList(event(proc("a"), 0)) sEventList(event(proc("a"), 0)))
localmsgs(proc("a"), regconf(sProcSet(proc("a")), 3), eNatSet)
localmsgs(proc("a"), regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), sNatSet(0))
localmsgs(proc("a"), transconf(sProcSet(proc("a")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), eNatSet)
localmsgs(proc("b"), regconf(sProcSet(proc("b")) sProcSet(proc("c")), 4), eNatSet)
localmsgs(proc("b"), regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), eNatSet)
localmsgs(proc("b"), transconf(sProcSet(proc("b")) sProcSet(proc("c")), 2, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)),
    eNatSet)
localmsgs(proc("c"), regconf(sProcSet(proc("b")) sProcSet(proc("c")), 4), eNatSet)
localmsgs(proc("c"), regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), eNatSet)
localmsgs(proc("c"), transconf(sProcSet(proc("b")) sProcSet(proc("c")), 2, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)),
    eNatSet)
knownmsgs(proc("a"), regconf(sProcSet(proc("a")), 3), eNatSet)
knownmsgs(proc("a"), regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), sNatSet(0))
knownmsgs(proc("a"), transconf(sProcSet(proc("a")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), eNatSet)
knownmsgs(proc("b"), regconf(sProcSet(proc("b")) sProcSet(proc("c")), 4), eNatSet)
knownmsgs(proc("b"), regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), sNatSet(0))
knownmsgs(proc("b"), transconf(sProcSet(proc("b")) sProcSet(proc("c")), 2, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)),
    eNatSet)
knownmsgs(proc("c"), regconf(sProcSet(proc("b")) sProcSet(proc("c")), 4), eNatSet)
knownmsgs(proc("c"), regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), sNatSet(0))
knownmsgs(proc("c"), transconf(sProcSet(proc("b")) sProcSet(proc("c")), 2, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)),
    eNatSet)

Solution 12 (state 130579)
states: 130583  rewrites: 9108832 in 298220ms cpu (309530ms real) (30544 rewrites/second)
s:State --> multicast-ack(proc("a"))
network(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")))
freshconf(5)
operational(proc("a"))
operational(proc("b"))
operational(proc("c"))
freshseq(1)
CONTROLLER(eController)
localconf(proc("a"), regconf(sProcSet(proc("a")), 4))
localconf(proc("b"), regconf(sProcSet(proc("b")) sProcSet(proc("c")), 3))
localconf(proc("c"), regconf(sProcSet(proc("b")) sProcSet(proc("c")), 3))
delivered(proc("a"), sMessageList(datamsg(proc("a"), agreed, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), 0, eNatSet, data(
    "test"))) sMessageList(transmsg(transconf(sProcSet(proc("a")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0))))
    sMessageList(confmsg(regconf(sProcSet(proc("a")), 4), sProcSet(proc("a")))))
delivered(proc("b"), sMessageList(datamsg(proc("a"), agreed, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), 0, eNatSet, data(
    "test"))) sMessageList(transmsg(transconf(sProcSet(proc("b")) sProcSet(proc("c")), 2, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc(
    "c")), 0)))) sMessageList(confmsg(regconf(sProcSet(proc("b")) sProcSet(proc("c")), 3), sProcSet(proc("b")) sProcSet(proc("c")))))
delivered(proc("c"), sMessageList(datamsg(proc("a"), agreed, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), 0, eNatSet, data(
    "test"))) sMessageList(transmsg(transconf(sProcSet(proc("b")) sProcSet(proc("c")), 2, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc(
    "c")), 0)))) sMessageList(confmsg(regconf(sProcSet(proc("b")) sProcSet(proc("c")), 3), sProcSet(proc("b")) sProcSet(proc("c")))))
alldelivered(proc("a"), sMessageList(datamsg(proc("a"), agreed, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), 0, eNatSet,
    data("test"))) sMessageList(transmsg(transconf(sProcSet(proc("a")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0))))
    sMessageList(confmsg(regconf(sProcSet(proc("a")), 4), sProcSet(proc("a")))))
alldelivered(proc("b"), sMessageList(datamsg(proc("a"), agreed, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), 0, eNatSet,
    data("test"))) sMessageList(transmsg(transconf(sProcSet(proc("b")) sProcSet(proc("c")), 2, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(
    proc("c")), 0)))) sMessageList(confmsg(regconf(sProcSet(proc("b")) sProcSet(proc("c")), 3), sProcSet(proc("b")) sProcSet(proc("c")))))
alldelivered(proc("c"), sMessageList(datamsg(proc("a"), agreed, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), 0, eNatSet,
    data("test"))) sMessageList(transmsg(transconf(sProcSet(proc("b")) sProcSet(proc("c")), 2, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(
    proc("c")), 0)))) sMessageList(confmsg(regconf(sProcSet(proc("b")) sProcSet(proc("c")), 3), sProcSet(proc("b")) sProcSet(proc("c")))))
reachable(proc("a"), sProcSet(proc("a")))
reachable(proc("b"), sProcSet(proc("b")) sProcSet(proc("c")))
reachable(proc("c"), sProcSet(proc("b")) sProcSet(proc("c")))
sent(proc("a"), eBroadcastSet)
sent(proc("b"), eBroadcastSet)
sent(proc("c"), eBroadcastSet)
received(proc("a"), eMessageSet)
received(proc("b"), eMessageSet)
received(proc("c"), eMessageSet)
acked(proc("a"), eMessageSet)
acked(proc("b"), eMessageSet)
acked(proc("c"), eMessageSet)
causalorder(regconf(sProcSet(proc("a")), 4), eConstraintSet)
causalorder(regconf(sProcSet(proc("b")) sProcSet(proc("c")), 3), eConstraintSet)
causalorder(regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), eConstraintSet)
causalorder(transconf(sProcSet(proc("a")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), eConstraintSet)
causalorder(transconf(sProcSet(proc("b")) sProcSet(proc("c")), 2, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)),
    eConstraintSet)
totalorder(regconf(sProcSet(proc("a")), 4), eEventList)
totalorder(regconf(sProcSet(proc("b")) sProcSet(proc("c")), 3), eEventList)
totalorder(regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), sEventList(event(proc("a"), 0)) sEventList(event(proc("a"), 0))
    sEventList(event(proc("a"), 0)))
totalorder(transconf(sProcSet(proc("a")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), sEventList(event(proc("a"), 0)))
totalorder(transconf(sProcSet(proc("b")) sProcSet(proc("c")), 2, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), sEventList(
    event(proc("a"), 0)) sEventList(event(proc("a"), 0)) sEventList(event(proc("a"), 0)))
localmsgs(proc("a"), regconf(sProcSet(proc("a")), 4), eNatSet)
localmsgs(proc("a"), regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), sNatSet(0))
localmsgs(proc("a"), transconf(sProcSet(proc("a")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), eNatSet)
localmsgs(proc("b"), regconf(sProcSet(proc("b")) sProcSet(proc("c")), 3), eNatSet)
localmsgs(proc("b"), regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), eNatSet)
localmsgs(proc("b"), transconf(sProcSet(proc("b")) sProcSet(proc("c")), 2, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)),
    eNatSet)
localmsgs(proc("c"), regconf(sProcSet(proc("b")) sProcSet(proc("c")), 3), eNatSet)
localmsgs(proc("c"), regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), eNatSet)
localmsgs(proc("c"), transconf(sProcSet(proc("b")) sProcSet(proc("c")), 2, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)),
    eNatSet)
knownmsgs(proc("a"), regconf(sProcSet(proc("a")), 4), eNatSet)
knownmsgs(proc("a"), regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), sNatSet(0))
knownmsgs(proc("a"), transconf(sProcSet(proc("a")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), eNatSet)
knownmsgs(proc("b"), regconf(sProcSet(proc("b")) sProcSet(proc("c")), 3), eNatSet)
knownmsgs(proc("b"), regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), sNatSet(0))
knownmsgs(proc("b"), transconf(sProcSet(proc("b")) sProcSet(proc("c")), 2, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)),
    eNatSet)
knownmsgs(proc("c"), regconf(sProcSet(proc("b")) sProcSet(proc("c")), 3), eNatSet)
knownmsgs(proc("c"), regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), sNatSet(0))
knownmsgs(proc("c"), transconf(sProcSet(proc("b")) sProcSet(proc("c")), 2, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)),
    eNatSet)

Solution 13 (state 130580)
states: 130583  rewrites: 9108834 in 298230ms cpu (309700ms real) (30542 rewrites/second)
s:State --> multicast-ack(proc("a"))
network(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")))
freshconf(5)
operational(proc("a"))
operational(proc("b"))
operational(proc("c"))
freshseq(1)
CONTROLLER(eController)
localconf(proc("a"), regconf(sProcSet(proc("a")), 3))
localconf(proc("b"), regconf(sProcSet(proc("b")) sProcSet(proc("c")), 4))
localconf(proc("c"), regconf(sProcSet(proc("b")) sProcSet(proc("c")), 4))
delivered(proc("a"), sMessageList(datamsg(proc("a"), agreed, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), 0, eNatSet, data(
    "test"))) sMessageList(transmsg(transconf(sProcSet(proc("a")), 2, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0))))
    sMessageList(confmsg(regconf(sProcSet(proc("a")), 3), sProcSet(proc("a")))))
delivered(proc("b"), sMessageList(datamsg(proc("a"), agreed, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), 0, eNatSet, data(
    "test"))) sMessageList(transmsg(transconf(sProcSet(proc("b")) sProcSet(proc("c")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc(
    "c")), 0)))) sMessageList(confmsg(regconf(sProcSet(proc("b")) sProcSet(proc("c")), 4), sProcSet(proc("b")) sProcSet(proc("c")))))
delivered(proc("c"), sMessageList(datamsg(proc("a"), agreed, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), 0, eNatSet, data(
    "test"))) sMessageList(transmsg(transconf(sProcSet(proc("b")) sProcSet(proc("c")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc(
    "c")), 0)))) sMessageList(confmsg(regconf(sProcSet(proc("b")) sProcSet(proc("c")), 4), sProcSet(proc("b")) sProcSet(proc("c")))))
alldelivered(proc("a"), sMessageList(datamsg(proc("a"), agreed, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), 0, eNatSet,
    data("test"))) sMessageList(transmsg(transconf(sProcSet(proc("a")), 2, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0))))
    sMessageList(confmsg(regconf(sProcSet(proc("a")), 3), sProcSet(proc("a")))))
alldelivered(proc("b"), sMessageList(datamsg(proc("a"), agreed, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), 0, eNatSet,
    data("test"))) sMessageList(transmsg(transconf(sProcSet(proc("b")) sProcSet(proc("c")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(
    proc("c")), 0)))) sMessageList(confmsg(regconf(sProcSet(proc("b")) sProcSet(proc("c")), 4), sProcSet(proc("b")) sProcSet(proc("c")))))
alldelivered(proc("c"), sMessageList(datamsg(proc("a"), agreed, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), 0, eNatSet,
    data("test"))) sMessageList(transmsg(transconf(sProcSet(proc("b")) sProcSet(proc("c")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(
    proc("c")), 0)))) sMessageList(confmsg(regconf(sProcSet(proc("b")) sProcSet(proc("c")), 4), sProcSet(proc("b")) sProcSet(proc("c")))))
reachable(proc("a"), sProcSet(proc("a")))
reachable(proc("b"), sProcSet(proc("b")) sProcSet(proc("c")))
reachable(proc("c"), sProcSet(proc("b")) sProcSet(proc("c")))
sent(proc("a"), eBroadcastSet)
sent(proc("b"), eBroadcastSet)
sent(proc("c"), eBroadcastSet)
received(proc("a"), eMessageSet)
received(proc("b"), eMessageSet)
received(proc("c"), eMessageSet)
acked(proc("a"), eMessageSet)
acked(proc("b"), eMessageSet)
acked(proc("c"), eMessageSet)
causalorder(regconf(sProcSet(proc("a")), 3), eConstraintSet)
causalorder(regconf(sProcSet(proc("b")) sProcSet(proc("c")), 4), eConstraintSet)
causalorder(regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), eConstraintSet)
causalorder(transconf(sProcSet(proc("a")), 2, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), eConstraintSet)
causalorder(transconf(sProcSet(proc("b")) sProcSet(proc("c")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)),
    eConstraintSet)
totalorder(regconf(sProcSet(proc("a")), 3), eEventList)
totalorder(regconf(sProcSet(proc("b")) sProcSet(proc("c")), 4), eEventList)
totalorder(regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), sEventList(event(proc("a"), 0)) sEventList(event(proc("a"), 0))
    sEventList(event(proc("a"), 0)))
totalorder(transconf(sProcSet(proc("a")), 2, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), sEventList(event(proc("a"), 0))
    sEventList(event(proc("a"), 0)) sEventList(event(proc("a"), 0)))
totalorder(transconf(sProcSet(proc("b")) sProcSet(proc("c")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), sEventList(
    event(proc("a"), 0)) sEventList(event(proc("a"), 0)))
localmsgs(proc("a"), regconf(sProcSet(proc("a")), 3), eNatSet)
localmsgs(proc("a"), regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), sNatSet(0))
localmsgs(proc("a"), transconf(sProcSet(proc("a")), 2, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), eNatSet)
localmsgs(proc("b"), regconf(sProcSet(proc("b")) sProcSet(proc("c")), 4), eNatSet)
localmsgs(proc("b"), regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), eNatSet)
localmsgs(proc("b"), transconf(sProcSet(proc("b")) sProcSet(proc("c")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)),
    eNatSet)
localmsgs(proc("c"), regconf(sProcSet(proc("b")) sProcSet(proc("c")), 4), eNatSet)
localmsgs(proc("c"), regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), eNatSet)
localmsgs(proc("c"), transconf(sProcSet(proc("b")) sProcSet(proc("c")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)),
    eNatSet)
knownmsgs(proc("a"), regconf(sProcSet(proc("a")), 3), eNatSet)
knownmsgs(proc("a"), regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), sNatSet(0))
knownmsgs(proc("a"), transconf(sProcSet(proc("a")), 2, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), eNatSet)
knownmsgs(proc("b"), regconf(sProcSet(proc("b")) sProcSet(proc("c")), 4), eNatSet)
knownmsgs(proc("b"), regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), sNatSet(0))
knownmsgs(proc("b"), transconf(sProcSet(proc("b")) sProcSet(proc("c")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)),
    eNatSet)
knownmsgs(proc("c"), regconf(sProcSet(proc("b")) sProcSet(proc("c")), 4), eNatSet)
knownmsgs(proc("c"), regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), sNatSet(0))
knownmsgs(proc("c"), transconf(sProcSet(proc("b")) sProcSet(proc("c")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)),
    eNatSet)

Solution 14 (state 130581)
states: 130583  rewrites: 9108836 in 298230ms cpu (309840ms real) (30542 rewrites/second)
s:State --> multicast-ack(proc("a"))
network(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")))
freshconf(5)
operational(proc("a"))
operational(proc("b"))
operational(proc("c"))
freshseq(1)
CONTROLLER(eController)
localconf(proc("a"), regconf(sProcSet(proc("a")), 4))
localconf(proc("b"), regconf(sProcSet(proc("b")) sProcSet(proc("c")), 3))
localconf(proc("c"), regconf(sProcSet(proc("b")) sProcSet(proc("c")), 3))
delivered(proc("a"), sMessageList(datamsg(proc("a"), agreed, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), 0, eNatSet, data(
    "test"))) sMessageList(transmsg(transconf(sProcSet(proc("a")), 2, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0))))
    sMessageList(confmsg(regconf(sProcSet(proc("a")), 4), sProcSet(proc("a")))))
delivered(proc("b"), sMessageList(datamsg(proc("a"), agreed, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), 0, eNatSet, data(
    "test"))) sMessageList(transmsg(transconf(sProcSet(proc("b")) sProcSet(proc("c")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc(
    "c")), 0)))) sMessageList(confmsg(regconf(sProcSet(proc("b")) sProcSet(proc("c")), 3), sProcSet(proc("b")) sProcSet(proc("c")))))
delivered(proc("c"), sMessageList(datamsg(proc("a"), agreed, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), 0, eNatSet, data(
    "test"))) sMessageList(transmsg(transconf(sProcSet(proc("b")) sProcSet(proc("c")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc(
    "c")), 0)))) sMessageList(confmsg(regconf(sProcSet(proc("b")) sProcSet(proc("c")), 3), sProcSet(proc("b")) sProcSet(proc("c")))))
alldelivered(proc("a"), sMessageList(datamsg(proc("a"), agreed, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), 0, eNatSet,
    data("test"))) sMessageList(transmsg(transconf(sProcSet(proc("a")), 2, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0))))
    sMessageList(confmsg(regconf(sProcSet(proc("a")), 4), sProcSet(proc("a")))))
alldelivered(proc("b"), sMessageList(datamsg(proc("a"), agreed, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), 0, eNatSet,
    data("test"))) sMessageList(transmsg(transconf(sProcSet(proc("b")) sProcSet(proc("c")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(
    proc("c")), 0)))) sMessageList(confmsg(regconf(sProcSet(proc("b")) sProcSet(proc("c")), 3), sProcSet(proc("b")) sProcSet(proc("c")))))
alldelivered(proc("c"), sMessageList(datamsg(proc("a"), agreed, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), 0, eNatSet,
    data("test"))) sMessageList(transmsg(transconf(sProcSet(proc("b")) sProcSet(proc("c")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(
    proc("c")), 0)))) sMessageList(confmsg(regconf(sProcSet(proc("b")) sProcSet(proc("c")), 3), sProcSet(proc("b")) sProcSet(proc("c")))))
reachable(proc("a"), sProcSet(proc("a")))
reachable(proc("b"), sProcSet(proc("b")) sProcSet(proc("c")))
reachable(proc("c"), sProcSet(proc("b")) sProcSet(proc("c")))
sent(proc("a"), eBroadcastSet)
sent(proc("b"), eBroadcastSet)
sent(proc("c"), eBroadcastSet)
received(proc("a"), eMessageSet)
received(proc("b"), eMessageSet)
received(proc("c"), eMessageSet)
acked(proc("a"), eMessageSet)
acked(proc("b"), eMessageSet)
acked(proc("c"), eMessageSet)
causalorder(regconf(sProcSet(proc("a")), 4), eConstraintSet)
causalorder(regconf(sProcSet(proc("b")) sProcSet(proc("c")), 3), eConstraintSet)
causalorder(regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), eConstraintSet)
causalorder(transconf(sProcSet(proc("a")), 2, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), eConstraintSet)
causalorder(transconf(sProcSet(proc("b")) sProcSet(proc("c")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)),
    eConstraintSet)
totalorder(regconf(sProcSet(proc("a")), 4), eEventList)
totalorder(regconf(sProcSet(proc("b")) sProcSet(proc("c")), 3), eEventList)
totalorder(regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), sEventList(event(proc("a"), 0)) sEventList(event(proc("a"), 0))
    sEventList(event(proc("a"), 0)))
totalorder(transconf(sProcSet(proc("a")), 2, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), sEventList(event(proc("a"), 0))
    sEventList(event(proc("a"), 0)) sEventList(event(proc("a"), 0)))
totalorder(transconf(sProcSet(proc("b")) sProcSet(proc("c")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), sEventList(
    event(proc("a"), 0)) sEventList(event(proc("a"), 0)))
localmsgs(proc("a"), regconf(sProcSet(proc("a")), 4), eNatSet)
localmsgs(proc("a"), regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), sNatSet(0))
localmsgs(proc("a"), transconf(sProcSet(proc("a")), 2, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), eNatSet)
localmsgs(proc("b"), regconf(sProcSet(proc("b")) sProcSet(proc("c")), 3), eNatSet)
localmsgs(proc("b"), regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), eNatSet)
localmsgs(proc("b"), transconf(sProcSet(proc("b")) sProcSet(proc("c")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)),
    eNatSet)
localmsgs(proc("c"), regconf(sProcSet(proc("b")) sProcSet(proc("c")), 3), eNatSet)
localmsgs(proc("c"), regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), eNatSet)
localmsgs(proc("c"), transconf(sProcSet(proc("b")) sProcSet(proc("c")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)),
    eNatSet)
knownmsgs(proc("a"), regconf(sProcSet(proc("a")), 4), eNatSet)
knownmsgs(proc("a"), regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), sNatSet(0))
knownmsgs(proc("a"), transconf(sProcSet(proc("a")), 2, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), eNatSet)
knownmsgs(proc("b"), regconf(sProcSet(proc("b")) sProcSet(proc("c")), 3), eNatSet)
knownmsgs(proc("b"), regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), sNatSet(0))
knownmsgs(proc("b"), transconf(sProcSet(proc("b")) sProcSet(proc("c")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)),
    eNatSet)
knownmsgs(proc("c"), regconf(sProcSet(proc("b")) sProcSet(proc("c")), 3), eNatSet)
knownmsgs(proc("c"), regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), sNatSet(0))
knownmsgs(proc("c"), transconf(sProcSet(proc("b")) sProcSet(proc("c")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)),
    eNatSet)

Solution 15 (state 130582)
states: 130583  rewrites: 9108838 in 298230ms cpu (309940ms real) (30542 rewrites/second)
s:State --> multicast-ack(proc("a"))
network(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")))
freshconf(5)
operational(proc("a"))
operational(proc("b"))
operational(proc("c"))
freshseq(1)
CONTROLLER(eController)
localconf(proc("a"), regconf(sProcSet(proc("a")), 4))
localconf(proc("b"), regconf(sProcSet(proc("b")) sProcSet(proc("c")), 2))
localconf(proc("c"), regconf(sProcSet(proc("b")) sProcSet(proc("c")), 2))
delivered(proc("a"), sMessageList(datamsg(proc("a"), agreed, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), 0, eNatSet, data(
    "test"))) sMessageList(transmsg(transconf(sProcSet(proc("a")), 3, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0))))
    sMessageList(confmsg(regconf(sProcSet(proc("a")), 4), sProcSet(proc("a")))))
delivered(proc("b"), sMessageList(datamsg(proc("a"), agreed, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), 0, eNatSet, data(
    "test"))) sMessageList(transmsg(transconf(sProcSet(proc("b")) sProcSet(proc("c")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc(
    "c")), 0)))) sMessageList(confmsg(regconf(sProcSet(proc("b")) sProcSet(proc("c")), 2), sProcSet(proc("b")) sProcSet(proc("c")))))
delivered(proc("c"), sMessageList(datamsg(proc("a"), agreed, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), 0, eNatSet, data(
    "test"))) sMessageList(transmsg(transconf(sProcSet(proc("b")) sProcSet(proc("c")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc(
    "c")), 0)))) sMessageList(confmsg(regconf(sProcSet(proc("b")) sProcSet(proc("c")), 2), sProcSet(proc("b")) sProcSet(proc("c")))))
alldelivered(proc("a"), sMessageList(datamsg(proc("a"), agreed, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), 0, eNatSet,
    data("test"))) sMessageList(transmsg(transconf(sProcSet(proc("a")), 3, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0))))
    sMessageList(confmsg(regconf(sProcSet(proc("a")), 4), sProcSet(proc("a")))))
alldelivered(proc("b"), sMessageList(datamsg(proc("a"), agreed, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), 0, eNatSet,
    data("test"))) sMessageList(transmsg(transconf(sProcSet(proc("b")) sProcSet(proc("c")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(
    proc("c")), 0)))) sMessageList(confmsg(regconf(sProcSet(proc("b")) sProcSet(proc("c")), 2), sProcSet(proc("b")) sProcSet(proc("c")))))
alldelivered(proc("c"), sMessageList(datamsg(proc("a"), agreed, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), 0, eNatSet,
    data("test"))) sMessageList(transmsg(transconf(sProcSet(proc("b")) sProcSet(proc("c")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(
    proc("c")), 0)))) sMessageList(confmsg(regconf(sProcSet(proc("b")) sProcSet(proc("c")), 2), sProcSet(proc("b")) sProcSet(proc("c")))))
reachable(proc("a"), sProcSet(proc("a")))
reachable(proc("b"), sProcSet(proc("b")) sProcSet(proc("c")))
reachable(proc("c"), sProcSet(proc("b")) sProcSet(proc("c")))
sent(proc("a"), eBroadcastSet)
sent(proc("b"), eBroadcastSet)
sent(proc("c"), eBroadcastSet)
received(proc("a"), eMessageSet)
received(proc("b"), eMessageSet)
received(proc("c"), eMessageSet)
acked(proc("a"), eMessageSet)
acked(proc("b"), eMessageSet)
acked(proc("c"), eMessageSet)
causalorder(regconf(sProcSet(proc("a")), 4), eConstraintSet)
causalorder(regconf(sProcSet(proc("b")) sProcSet(proc("c")), 2), eConstraintSet)
causalorder(regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), eConstraintSet)
causalorder(transconf(sProcSet(proc("a")), 3, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), eConstraintSet)
causalorder(transconf(sProcSet(proc("b")) sProcSet(proc("c")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)),
    eConstraintSet)
totalorder(regconf(sProcSet(proc("a")), 4), eEventList)
totalorder(regconf(sProcSet(proc("b")) sProcSet(proc("c")), 2), eEventList)
totalorder(regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), sEventList(event(proc("a"), 0)) sEventList(event(proc("a"), 0))
    sEventList(event(proc("a"), 0)))
totalorder(transconf(sProcSet(proc("a")), 3, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), sEventList(event(proc("a"), 0))
    sEventList(event(proc("a"), 0)) sEventList(event(proc("a"), 0)))
totalorder(transconf(sProcSet(proc("b")) sProcSet(proc("c")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), sEventList(
    event(proc("a"), 0)) sEventList(event(proc("a"), 0)))
localmsgs(proc("a"), regconf(sProcSet(proc("a")), 4), eNatSet)
localmsgs(proc("a"), regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), sNatSet(0))
localmsgs(proc("a"), transconf(sProcSet(proc("a")), 3, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), eNatSet)
localmsgs(proc("b"), regconf(sProcSet(proc("b")) sProcSet(proc("c")), 2), eNatSet)
localmsgs(proc("b"), regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), eNatSet)
localmsgs(proc("b"), transconf(sProcSet(proc("b")) sProcSet(proc("c")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)),
    eNatSet)
localmsgs(proc("c"), regconf(sProcSet(proc("b")) sProcSet(proc("c")), 2), eNatSet)
localmsgs(proc("c"), regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), eNatSet)
localmsgs(proc("c"), transconf(sProcSet(proc("b")) sProcSet(proc("c")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)),
    eNatSet)
knownmsgs(proc("a"), regconf(sProcSet(proc("a")), 4), eNatSet)
knownmsgs(proc("a"), regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), sNatSet(0))
knownmsgs(proc("a"), transconf(sProcSet(proc("a")), 3, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), eNatSet)
knownmsgs(proc("b"), regconf(sProcSet(proc("b")) sProcSet(proc("c")), 2), eNatSet)
knownmsgs(proc("b"), regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), sNatSet(0))
knownmsgs(proc("b"), transconf(sProcSet(proc("b")) sProcSet(proc("c")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)),
    eNatSet)
knownmsgs(proc("c"), regconf(sProcSet(proc("b")) sProcSet(proc("c")), 2), eNatSet)
knownmsgs(proc("c"), regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), sNatSet(0))
knownmsgs(proc("c"), transconf(sProcSet(proc("b")) sProcSet(proc("c")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)),
    eNatSet)

No more solutions.
states: 130583  rewrites: 9108838 in 298230ms cpu (310060ms real) (30542 rewrites/second)
Done reading in file: "test12.maude"