\||||||||||||||||||/
		   --- Welcome to Maude ---
		     /||||||||||||||||||\
	Maude alpha 79 built: Mar 28 2003 16:27:07
	     Copyright 1997-2003 SRI International
		   Tue Nov  4 12:32:51 2003
Maude> in cliques.maude
==========================================
mod CLIQUES
Maude> in examples.maude 
==========================================

Reading in file: "cliques.maude"
==========================================
mod CLIQUES
Advisory: redefining module CLIQUES.
Done reading in file: "cliques.maude"
Advisory: "cliques.maude", line 203 (mod CLIQUES): collapse at top of x:PartialKey * inv(x:PartialKey) may cause it to match more than you expect.
Advisory: "cliques.maude", line 220 (mod CLIQUES): collapse at top of x:KeyShare * inv(x:KeyShare) may cause it to match more than you expect.
==========================================
rewrite in CLIQUES : fresh(0)
((join(agent("c"), sAgentList(agent("a")) sAgentList(agent("b")) sAgentList(agent("c")), group("G"))
join(agent("d"), sAgentList(agent("a")) sAgentList(agent("b")) sAgentList(agent("c")) sAgentList(agent("d")), group("G")))
join(agent("b"), sAgentList(agent("a")) sAgentList(agent("b")), group("G")))
start(agent("a"), group("G")) .
rewrites: 2499 in 10ms cpu (10ms real) (249900 rewrites/second)
result State: fresh(6)
ready(agent("a"), group("G"), context(random(0), alpha ^ random(0) * random(2) * random(4) * random(5), sGroupMemberList(groupmember(agent("a"), alpha ^
    random(2) * random(4) * random(5))) sGroupMemberList(groupmember(agent("b"), alpha ^ random(0) * random(4) * random(5))) sGroupMemberList(
    groupmember(agent("c"), alpha ^ random(0) * random(2) * random(5))) sGroupMemberList(groupmember(agent("d"), alpha ^ random(0) * random(2) * random(
    4)))), sAgentList(agent("a")) sAgentList(agent("b")) sAgentList(agent("c")) sAgentList(agent("d")))
ready(agent("b"), group("G"), context(random(2), alpha ^ random(0) * random(2) * random(4) * random(5), sGroupMemberList(groupmember(agent("a"), alpha ^
    random(2) * random(4) * random(5))) sGroupMemberList(groupmember(agent("b"), alpha ^ random(0) * random(4) * random(5))) sGroupMemberList(
    groupmember(agent("c"), alpha ^ random(0) * random(2) * random(5))) sGroupMemberList(groupmember(agent("d"), alpha ^ random(0) * random(2) * random(
    4)))), sAgentList(agent("a")) sAgentList(agent("b")) sAgentList(agent("c")) sAgentList(agent("d")))
ready(agent("c"), group("G"), context(random(4), alpha ^ random(0) * random(2) * random(4) * random(5), sGroupMemberList(groupmember(agent("a"), alpha ^
    random(2) * random(4) * random(5))) sGroupMemberList(groupmember(agent("b"), alpha ^ random(0) * random(4) * random(5))) sGroupMemberList(
    groupmember(agent("c"), alpha ^ random(0) * random(2) * random(5))) sGroupMemberList(groupmember(agent("d"), alpha ^ random(0) * random(2) * random(
    4)))), sAgentList(agent("a")) sAgentList(agent("b")) sAgentList(agent("c")) sAgentList(agent("d")))
ready(agent("d"), group("G"), context(random(5), alpha ^ random(0) * random(2) * random(4) * random(5), sGroupMemberList(groupmember(agent("a"), alpha ^
    random(2) * random(4) * random(5))) sGroupMemberList(groupmember(agent("b"), alpha ^ random(0) * random(4) * random(5))) sGroupMemberList(
    groupmember(agent("c"), alpha ^ random(0) * random(2) * random(5))) sGroupMemberList(groupmember(agent("d"), alpha ^ random(0) * random(2) * random(
    4)))), sAgentList(agent("a")) sAgentList(agent("b")) sAgentList(agent("c")) sAgentList(agent("d")))
==========================================
rewrite in CLIQUES : fresh(0)
(((join(agent("d"), sAgentList(agent("a")) sAgentList(agent("b")) sAgentList(agent("c")) sAgentList(agent("d")), group("G"))
leave(sAgentList(agent("d")), sAgentList(agent("a")) sAgentList(agent("b")) sAgentList(agent("c")) sAgentList(agent("d")), group("G")))
join(agent("c"), sAgentList(agent("a")) sAgentList(agent("b")) sAgentList(agent("c")), group("G")))
join(agent("b"), sAgentList(agent("a")) sAgentList(agent("b")), group("G")))
start(agent("a"), group("G")) .
rewrites: 3508 in 10ms cpu (10ms real) (350800 rewrites/second)
result State: fresh(7)
ready(agent("a"), group("G"), context(random(0), alpha ^ random(0) * random(2) * random(5) * random(6), sGroupMemberList(groupmember(agent("a"), alpha ^
    random(2) * random(5) * random(6))) sGroupMemberList(groupmember(agent("b"), alpha ^ random(0) * random(5) * random(6))) sGroupMemberList(
    groupmember(agent("c"), alpha ^ random(0) * random(2) * random(5)))), sAgentList(agent("a")) sAgentList(agent("b")) sAgentList(agent("c")))
ready(agent("b"), group("G"), context(random(2), alpha ^ random(0) * random(2) * random(5) * random(6), sGroupMemberList(groupmember(agent("a"), alpha ^
    random(2) * random(5) * random(6))) sGroupMemberList(groupmember(agent("b"), alpha ^ random(0) * random(5) * random(6))) sGroupMemberList(
    groupmember(agent("c"), alpha ^ random(0) * random(2) * random(5)))), sAgentList(agent("a")) sAgentList(agent("b")) sAgentList(agent("c")))
ready(agent("c"), group("G"), context(random(6), alpha ^ random(0) * random(2) * random(5) * random(6), sGroupMemberList(groupmember(agent("a"), alpha ^
    random(2) * random(5) * random(6))) sGroupMemberList(groupmember(agent("b"), alpha ^ random(0) * random(5) * random(6))) sGroupMemberList(
    groupmember(agent("c"), alpha ^ random(0) * random(2) * random(5)))), sAgentList(agent("a")) sAgentList(agent("b")) sAgentList(agent("c")))
==========================================
rewrite in CLIQUES : fresh(0)
(((join(agent("d"), sAgentList(agent("a")) sAgentList(agent("b")) sAgentList(agent("c")) sAgentList(agent("d")), group("G"))
leave(eAgentList, sAgentList(agent("a")) sAgentList(agent("b")) sAgentList(agent("c")) sAgentList(agent("d")), group("G")))
join(agent("c"), sAgentList(agent("a")) sAgentList(agent("b")) sAgentList(agent("c")), group("G")))
join(agent("b"), sAgentList(agent("a")) sAgentList(agent("b")), group("G")))
start(agent("a"), group("G")) .
rewrites: 4124 in 10ms cpu (10ms real) (412400 rewrites/second)
result State: fresh(7)
ready(agent("a"), group("G"), context(random(0), alpha ^ random(0) * random(2) * random(4) * random(6), sGroupMemberList(groupmember(agent("a"), alpha ^
    random(2) * random(4) * random(6))) sGroupMemberList(groupmember(agent("b"), alpha ^ random(0) * random(4) * random(6))) sGroupMemberList(
    groupmember(agent("c"), alpha ^ random(0) * random(2) * random(6))) sGroupMemberList(groupmember(agent("d"), alpha ^ random(0) * random(2) * random(
    4)))), sAgentList(agent("a")) sAgentList(agent("b")) sAgentList(agent("c")) sAgentList(agent("d")))
ready(agent("b"), group("G"), context(random(2), alpha ^ random(0) * random(2) * random(4) * random(6), sGroupMemberList(groupmember(agent("a"), alpha ^
    random(2) * random(4) * random(6))) sGroupMemberList(groupmember(agent("b"), alpha ^ random(0) * random(4) * random(6))) sGroupMemberList(
    groupmember(agent("c"), alpha ^ random(0) * random(2) * random(6))) sGroupMemberList(groupmember(agent("d"), alpha ^ random(0) * random(2) * random(
    4)))), sAgentList(agent("a")) sAgentList(agent("b")) sAgentList(agent("c")) sAgentList(agent("d")))
ready(agent("c"), group("G"), context(random(4), alpha ^ random(0) * random(2) * random(4) * random(6), sGroupMemberList(groupmember(agent("a"), alpha ^
    random(2) * random(4) * random(6))) sGroupMemberList(groupmember(agent("b"), alpha ^ random(0) * random(4) * random(6))) sGroupMemberList(
    groupmember(agent("c"), alpha ^ random(0) * random(2) * random(6))) sGroupMemberList(groupmember(agent("d"), alpha ^ random(0) * random(2) * random(
    4)))), sAgentList(agent("a")) sAgentList(agent("b")) sAgentList(agent("c")) sAgentList(agent("d")))
ready(agent("d"), group("G"), context(random(6), alpha ^ random(0) * random(2) * random(4) * random(6), sGroupMemberList(groupmember(agent("a"), alpha ^
    random(2) * random(4) * random(6))) sGroupMemberList(groupmember(agent("b"), alpha ^ random(0) * random(4) * random(6))) sGroupMemberList(
    groupmember(agent("c"), alpha ^ random(0) * random(2) * random(6))) sGroupMemberList(groupmember(agent("d"), alpha ^ random(0) * random(2) * random(
    4)))), sAgentList(agent("a")) sAgentList(agent("b")) sAgentList(agent("c")) sAgentList(agent("d")))
==========================================
rewrite in CLIQUES : fresh(0)
((join(agent("c"), sAgentList(agent("a")) sAgentList(agent("b")) sAgentList(agent("c")), group("G"))
merge(sAgentList(agent("d")) sAgentList(agent("e")), sAgentList(agent("a")) sAgentList(agent("b")) sAgentList(agent("c")) sAgentList(agent("d"))
    sAgentList(agent("e")), group("G")))
join(agent("b"), sAgentList(agent("a")) sAgentList(agent("b")), group("G")))
start(agent("a"), group("G")) .
rewrites: 4687 in 20ms cpu (20ms real) (234350 rewrites/second)
result State: fresh(11)
ready(agent("a"), group("G"), context(random(0), alpha ^ random(0) * random(2) * random(4) * random(5) * random(7), sGroupMemberList(groupmember(agent(
    "a"), alpha ^ random(2) * random(4) * random(5) * random(7))) sGroupMemberList(groupmember(agent("b"), alpha ^ random(0) * random(4) * random(5) *
    random(7))) sGroupMemberList(groupmember(agent("c"), alpha ^ random(0) * random(2) * random(5) * random(7))) sGroupMemberList(groupmember(agent("d"),
    alpha ^ random(0) * random(2) * random(4) * random(7))) sGroupMemberList(groupmember(agent("e"), alpha ^ random(0) * random(2) * random(4) * random(
    5)))), sAgentList(agent("a")) sAgentList(agent("b")) sAgentList(agent("c")) sAgentList(agent("d")) sAgentList(agent("e")))
ready(agent("b"), group("G"), context(random(2), alpha ^ random(0) * random(2) * random(4) * random(5) * random(7), sGroupMemberList(groupmember(agent(
    "a"), alpha ^ random(2) * random(4) * random(5) * random(7))) sGroupMemberList(groupmember(agent("b"), alpha ^ random(0) * random(4) * random(5) *
    random(7))) sGroupMemberList(groupmember(agent("c"), alpha ^ random(0) * random(2) * random(5) * random(7))) sGroupMemberList(groupmember(agent("d"),
    alpha ^ random(0) * random(2) * random(4) * random(7))) sGroupMemberList(groupmember(agent("e"), alpha ^ random(0) * random(2) * random(4) * random(
    5)))), sAgentList(agent("a")) sAgentList(agent("b")) sAgentList(agent("c")) sAgentList(agent("d")) sAgentList(agent("e")))
ready(agent("c"), group("G"), context(random(4), alpha ^ random(0) * random(2) * random(4) * random(5) * random(7), sGroupMemberList(groupmember(agent(
    "a"), alpha ^ random(2) * random(4) * random(5) * random(7))) sGroupMemberList(groupmember(agent("b"), alpha ^ random(0) * random(4) * random(5) *
    random(7))) sGroupMemberList(groupmember(agent("c"), alpha ^ random(0) * random(2) * random(5) * random(7))) sGroupMemberList(groupmember(agent("d"),
    alpha ^ random(0) * random(2) * random(4) * random(7))) sGroupMemberList(groupmember(agent("e"), alpha ^ random(0) * random(2) * random(4) * random(
    5)))), sAgentList(agent("a")) sAgentList(agent("b")) sAgentList(agent("c")) sAgentList(agent("d")) sAgentList(agent("e")))
ready(agent("d"), group("G"), context(random(5), alpha ^ random(0) * random(2) * random(4) * random(5) * random(7), sGroupMemberList(groupmember(agent(
    "a"), alpha ^ random(2) * random(4) * random(5) * random(7))) sGroupMemberList(groupmember(agent("b"), alpha ^ random(0) * random(4) * random(5) *
    random(7))) sGroupMemberList(groupmember(agent("c"), alpha ^ random(0) * random(2) * random(5) * random(7))) sGroupMemberList(groupmember(agent("d"),
    alpha ^ random(0) * random(2) * random(4) * random(7))) sGroupMemberList(groupmember(agent("e"), alpha ^ random(0) * random(2) * random(4) * random(
    5)))), sAgentList(agent("a")) sAgentList(agent("b")) sAgentList(agent("c")) sAgentList(agent("d")) sAgentList(agent("e")))
ready(agent("e"), group("G"), context(random(7), alpha ^ random(0) * random(2) * random(4) * random(5) * random(7), sGroupMemberList(groupmember(agent(
    "a"), alpha ^ random(2) * random(4) * random(5) * random(7))) sGroupMemberList(groupmember(agent("b"), alpha ^ random(0) * random(4) * random(5) *
    random(7))) sGroupMemberList(groupmember(agent("c"), alpha ^ random(0) * random(2) * random(5) * random(7))) sGroupMemberList(groupmember(agent("d"),
    alpha ^ random(0) * random(2) * random(4) * random(7))) sGroupMemberList(groupmember(agent("e"), alpha ^ random(0) * random(2) * random(4) * random(
    5)))), sAgentList(agent("a")) sAgentList(agent("b")) sAgentList(agent("c")) sAgentList(agent("d")) sAgentList(agent("e")))
==========================================
rewrite in CLIQUES : fresh(0)
((join(agent("c"), sAgentList(agent("a")) sAgentList(agent("b")) sAgentList(agent("c")), group("G"))
merge(sAgentList(agent("d")) sAgentList(agent("e")) sAgentList(agent("f")), sAgentList(agent("a")) sAgentList(agent("b")) sAgentList(agent("c"))
    sAgentList(agent("d")) sAgentList(agent("e")) sAgentList(agent("f")), group("G")))
join(agent("b"), sAgentList(agent("a")) sAgentList(agent("b")), group("G")))
start(agent("a"), group("G")) .
rewrites: 6668 in 20ms cpu (20ms real) (333400 rewrites/second)
result State: fresh(13)
ready(agent("a"), group("G"), context(random(0), alpha ^ random(0) * random(2) * random(4) * random(5) * random(6) * random(8), sGroupMemberList(
    groupmember(agent("a"), alpha ^ random(2) * random(4) * random(5) * random(6) * random(8))) sGroupMemberList(groupmember(agent("b"), alpha ^ random(
    0) * random(4) * random(5) * random(6) * random(8))) sGroupMemberList(groupmember(agent("c"), alpha ^ random(0) * random(2) * random(5) * random(6) *
    random(8))) sGroupMemberList(groupmember(agent("d"), alpha ^ random(0) * random(2) * random(4) * random(6) * random(8))) sGroupMemberList(
    groupmember(agent("e"), alpha ^ random(0) * random(2) * random(4) * random(5) * random(8))) sGroupMemberList(groupmember(agent("f"), alpha ^ random(
    0) * random(2) * random(4) * random(5) * random(6)))), sAgentList(agent("a")) sAgentList(agent("b")) sAgentList(agent("c")) sAgentList(agent("d"))
    sAgentList(agent("e")) sAgentList(agent("f")))
ready(agent("b"), group("G"), context(random(2), alpha ^ random(0) * random(2) * random(4) * random(5) * random(6) * random(8), sGroupMemberList(
    groupmember(agent("a"), alpha ^ random(2) * random(4) * random(5) * random(6) * random(8))) sGroupMemberList(groupmember(agent("b"), alpha ^ random(
    0) * random(4) * random(5) * random(6) * random(8))) sGroupMemberList(groupmember(agent("c"), alpha ^ random(0) * random(2) * random(5) * random(6) *
    random(8))) sGroupMemberList(groupmember(agent("d"), alpha ^ random(0) * random(2) * random(4) * random(6) * random(8))) sGroupMemberList(
    groupmember(agent("e"), alpha ^ random(0) * random(2) * random(4) * random(5) * random(8))) sGroupMemberList(groupmember(agent("f"), alpha ^ random(
    0) * random(2) * random(4) * random(5) * random(6)))), sAgentList(agent("a")) sAgentList(agent("b")) sAgentList(agent("c")) sAgentList(agent("d"))
    sAgentList(agent("e")) sAgentList(agent("f")))
ready(agent("c"), group("G"), context(random(4), alpha ^ random(0) * random(2) * random(4) * random(5) * random(6) * random(8), sGroupMemberList(
    groupmember(agent("a"), alpha ^ random(2) * random(4) * random(5) * random(6) * random(8))) sGroupMemberList(groupmember(agent("b"), alpha ^ random(
    0) * random(4) * random(5) * random(6) * random(8))) sGroupMemberList(groupmember(agent("c"), alpha ^ random(0) * random(2) * random(5) * random(6) *
    random(8))) sGroupMemberList(groupmember(agent("d"), alpha ^ random(0) * random(2) * random(4) * random(6) * random(8))) sGroupMemberList(
    groupmember(agent("e"), alpha ^ random(0) * random(2) * random(4) * random(5) * random(8))) sGroupMemberList(groupmember(agent("f"), alpha ^ random(
    0) * random(2) * random(4) * random(5) * random(6)))), sAgentList(agent("a")) sAgentList(agent("b")) sAgentList(agent("c")) sAgentList(agent("d"))
    sAgentList(agent("e")) sAgentList(agent("f")))
ready(agent("d"), group("G"), context(random(5), alpha ^ random(0) * random(2) * random(4) * random(5) * random(6) * random(8), sGroupMemberList(
    groupmember(agent("a"), alpha ^ random(2) * random(4) * random(5) * random(6) * random(8))) sGroupMemberList(groupmember(agent("b"), alpha ^ random(
    0) * random(4) * random(5) * random(6) * random(8))) sGroupMemberList(groupmember(agent("c"), alpha ^ random(0) * random(2) * random(5) * random(6) *
    random(8))) sGroupMemberList(groupmember(agent("d"), alpha ^ random(0) * random(2) * random(4) * random(6) * random(8))) sGroupMemberList(
    groupmember(agent("e"), alpha ^ random(0) * random(2) * random(4) * random(5) * random(8))) sGroupMemberList(groupmember(agent("f"), alpha ^ random(
    0) * random(2) * random(4) * random(5) * random(6)))), sAgentList(agent("a")) sAgentList(agent("b")) sAgentList(agent("c")) sAgentList(agent("d"))
    sAgentList(agent("e")) sAgentList(agent("f")))
ready(agent("e"), group("G"), context(random(6), alpha ^ random(0) * random(2) * random(4) * random(5) * random(6) * random(8), sGroupMemberList(
    groupmember(agent("a"), alpha ^ random(2) * random(4) * random(5) * random(6) * random(8))) sGroupMemberList(groupmember(agent("b"), alpha ^ random(
    0) * random(4) * random(5) * random(6) * random(8))) sGroupMemberList(groupmember(agent("c"), alpha ^ random(0) * random(2) * random(5) * random(6) *
    random(8))) sGroupMemberList(groupmember(agent("d"), alpha ^ random(0) * random(2) * random(4) * random(6) * random(8))) sGroupMemberList(
    groupmember(agent("e"), alpha ^ random(0) * random(2) * random(4) * random(5) * random(8))) sGroupMemberList(groupmember(agent("f"), alpha ^ random(
    0) * random(2) * random(4) * random(5) * random(6)))), sAgentList(agent("a")) sAgentList(agent("b")) sAgentList(agent("c")) sAgentList(agent("d"))
    sAgentList(agent("e")) sAgentList(agent("f")))
ready(agent("f"), group("G"), context(random(8), alpha ^ random(0) * random(2) * random(4) * random(5) * random(6) * random(8), sGroupMemberList(
    groupmember(agent("a"), alpha ^ random(2) * random(4) * random(5) * random(6) * random(8))) sGroupMemberList(groupmember(agent("b"), alpha ^ random(
    0) * random(4) * random(5) * random(6) * random(8))) sGroupMemberList(groupmember(agent("c"), alpha ^ random(0) * random(2) * random(5) * random(6) *
    random(8))) sGroupMemberList(groupmember(agent("d"), alpha ^ random(0) * random(2) * random(4) * random(6) * random(8))) sGroupMemberList(
    groupmember(agent("e"), alpha ^ random(0) * random(2) * random(4) * random(5) * random(8))) sGroupMemberList(groupmember(agent("f"), alpha ^ random(
    0) * random(2) * random(4) * random(5) * random(6)))), sAgentList(agent("a")) sAgentList(agent("b")) sAgentList(agent("c")) sAgentList(agent("d"))
    sAgentList(agent("e")) sAgentList(agent("f")))
==========================================
search in CLIQUES : fresh(0)
start(agent("a"), group("G")) =>! state:State .

Solution 1 (state 3)
states: 4  rewrites: 3 in 0ms cpu (0ms real) (~ rewrites/second)
state:State --> fresh(0)
ready(agent("a"), group("G"), context(idKeyShare, idPartialKey, sGroupMemberList(groupmember(agent("a"), alpha))), sAgentList(agent("a")))

No more solutions.
states: 4  rewrites: 3 in 0ms cpu (0ms real) (~ rewrites/second)
==========================================
search in CLIQUES : fresh(0)
start(agent("a"), group("G"))
join(agent("b"), sAgentList(agent("a")) sAgentList(agent("b")), group("G")) =>! state:State .

Solution 1 (state 179)
states: 180  rewrites: 5966 in 20ms cpu (20ms real) (298300 rewrites/second)
state:State --> fresh(2)
ready(agent("a"), group("G"), context(random(0), alpha ^ random(0) * random(1), sGroupMemberList(groupmember(agent("a"), alpha ^ random(1)))
    sGroupMemberList(groupmember(agent("b"), alpha ^ random(0)))), sAgentList(agent("a")) sAgentList(agent("b")))
ready(agent("b"), group("G"), context(random(1), alpha ^ random(0) * random(1), sGroupMemberList(groupmember(agent("a"), alpha ^ random(1)))
    sGroupMemberList(groupmember(agent("b"), alpha ^ random(0)))), sAgentList(agent("a")) sAgentList(agent("b")))

No more solutions.
states: 180  rewrites: 5966 in 20ms cpu (20ms real) (298300 rewrites/second)
==========================================
search in CLIQUES : fresh(0)
(join(agent("b"), sAgentList(agent("a")) sAgentList(agent("b")), group("G"))
join(agent("c"), sAgentList(agent("a")) sAgentList(agent("b")) sAgentList(agent("c")), group("G")))
start(agent("a"), group("G")) =>! state:State .

Solution 1 (state 270256)
states: 270257  rewrites: 28927765 in 122380ms cpu (124040ms real) (236376 rewrites/second)
state:State --> fresh(4)
ready(agent("a"), group("G"), context(random(0), alpha ^ random(0) * random(2) * random(3), sGroupMemberList(groupmember(agent("a"), alpha ^ random(2) *
    random(3))) sGroupMemberList(groupmember(agent("b"), alpha ^ random(0) * random(3))) sGroupMemberList(groupmember(agent("c"), alpha ^ random(0) *
    random(2)))), sAgentList(agent("a")) sAgentList(agent("b")) sAgentList(agent("c")))
ready(agent("b"), group("G"), context(random(2), alpha ^ random(0) * random(2) * random(3), sGroupMemberList(groupmember(agent("a"), alpha ^ random(2) *
    random(3))) sGroupMemberList(groupmember(agent("b"), alpha ^ random(0) * random(3))) sGroupMemberList(groupmember(agent("c"), alpha ^ random(0) *
    random(2)))), sAgentList(agent("a")) sAgentList(agent("b")) sAgentList(agent("c")))
ready(agent("c"), group("G"), context(random(3), alpha ^ random(0) * random(2) * random(3), sGroupMemberList(groupmember(agent("a"), alpha ^ random(2) *
    random(3))) sGroupMemberList(groupmember(agent("b"), alpha ^ random(0) * random(3))) sGroupMemberList(groupmember(agent("c"), alpha ^ random(0) *
    random(2)))), sAgentList(agent("a")) sAgentList(agent("b")) sAgentList(agent("c")))

No more solutions.
states: 270257  rewrites: 28927765 in 122380ms cpu (124040ms real) (236376 rewrites/second)
==========================================
search in CLIQUES : fresh(0)
start(agent("a"), group("G"))
merge(sAgentList(agent("b")) sAgentList(agent("c")), sAgentList(agent("a")) sAgentList(agent("b")) sAgentList(agent("c")), group("G")) =>! state:State .

Solution 1 (state 258500)
states: 258501  rewrites: 27753458 in 352340ms cpu (354090ms real) (78768 rewrites/second)
state:State --> fresh(5)
ready(agent("a"), group("G"), context(random(0), alpha ^ random(0) * random(1) * random(3), sGroupMemberList(groupmember(agent("a"), alpha ^ random(1) *
    random(3))) sGroupMemberList(groupmember(agent("b"), alpha ^ random(0) * random(3))) sGroupMemberList(groupmember(agent("c"), alpha ^ random(0) *
    random(1)))), sAgentList(agent("a")) sAgentList(agent("b")) sAgentList(agent("c")))
ready(agent("b"), group("G"), context(random(1), alpha ^ random(0) * random(1) * random(3), sGroupMemberList(groupmember(agent("a"), alpha ^ random(1) *
    random(3))) sGroupMemberList(groupmember(agent("b"), alpha ^ random(0) * random(3))) sGroupMemberList(groupmember(agent("c"), alpha ^ random(0) *
    random(1)))), sAgentList(agent("a")) sAgentList(agent("b")) sAgentList(agent("c")))
ready(agent("c"), group("G"), context(random(3), alpha ^ random(0) * random(1) * random(3), sGroupMemberList(groupmember(agent("a"), alpha ^ random(1) *
    random(3))) sGroupMemberList(groupmember(agent("b"), alpha ^ random(0) * random(3))) sGroupMemberList(groupmember(agent("c"), alpha ^ random(0) *
    random(1)))), sAgentList(agent("a")) sAgentList(agent("b")) sAgentList(agent("c")))

No more solutions.
states: 258501  rewrites: 27753458 in 352350ms cpu (354100ms real) (78766 rewrites/second)
==========================================
search in CLIQUES : fresh(0)
(join(agent("b"), sAgentList(agent("a")) sAgentList(agent("b")), group("G"))
merge(sAgentList(agent("c")), sAgentList(agent("a")) sAgentList(agent("b")) sAgentList(agent("c")), group("G")))
start(agent("a"), group("G")) =>! state:State .

Solution 1 (state 260645)
states: 260646  rewrites: 27859114 in 348350ms cpu (359300ms real) (79974 rewrites/second)
state:State --> fresh(6)
ready(agent("a"), group("G"), context(random(0), alpha ^ random(0) * random(2) * random(4), sGroupMemberList(groupmember(agent("a"), alpha ^ random(2) *
    random(4))) sGroupMemberList(groupmember(agent("b"), alpha ^ random(0) * random(4))) sGroupMemberList(groupmember(agent("c"), alpha ^ random(0) *
    random(2)))), sAgentList(agent("a")) sAgentList(agent("b")) sAgentList(agent("c")))
ready(agent("b"), group("G"), context(random(2), alpha ^ random(0) * random(2) * random(4), sGroupMemberList(groupmember(agent("a"), alpha ^ random(2) *
    random(4))) sGroupMemberList(groupmember(agent("b"), alpha ^ random(0) * random(4))) sGroupMemberList(groupmember(agent("c"), alpha ^ random(0) *
    random(2)))), sAgentList(agent("a")) sAgentList(agent("b")) sAgentList(agent("c")))
ready(agent("c"), group("G"), context(random(4), alpha ^ random(0) * random(2) * random(4), sGroupMemberList(groupmember(agent("a"), alpha ^ random(2) *
    random(4))) sGroupMemberList(groupmember(agent("b"), alpha ^ random(0) * random(4))) sGroupMemberList(groupmember(agent("c"), alpha ^ random(0) *
    random(2)))), sAgentList(agent("a")) sAgentList(agent("b")) sAgentList(agent("c")))

No more solutions.
states: 260646  rewrites: 27859114 in 348350ms cpu (359300ms real) (79974 rewrites/second)
==========================================
search in CLIQUES : fresh(0)
((join(agent("b"), sAgentList(agent("a")) sAgentList(agent("b")), group("G1"))
join(agent("c"), sAgentList(agent("a")) sAgentList(agent("c")), group("G2")))
start(agent("a"), group("G2")))
start(agent("a"), group("G1")) =>! state:State .

Solution 1 (state 168851)
states: 168857  rewrites: 11822450 in 302690ms cpu (302800ms real) (39057 rewrites/second)
state:State --> fresh(4)
ready(agent("a"), group("G1"), context(random(0), alpha ^ random(0) * random(1), sGroupMemberList(groupmember(agent("a"), alpha ^ random(1)))
    sGroupMemberList(groupmember(agent("b"), alpha ^ random(0)))), sAgentList(agent("a")) sAgentList(agent("b")))
ready(agent("a"), group("G2"), context(random(2), alpha ^ random(2) * random(3), sGroupMemberList(groupmember(agent("a"), alpha ^ random(3)))
    sGroupMemberList(groupmember(agent("c"), alpha ^ random(2)))), sAgentList(agent("a")) sAgentList(agent("c")))
ready(agent("b"), group("G1"), context(random(1), alpha ^ random(0) * random(1), sGroupMemberList(groupmember(agent("a"), alpha ^ random(1)))
    sGroupMemberList(groupmember(agent("b"), alpha ^ random(0)))), sAgentList(agent("a")) sAgentList(agent("b")))
ready(agent("c"), group("G2"), context(random(3), alpha ^ random(2) * random(3), sGroupMemberList(groupmember(agent("a"), alpha ^ random(3)))
    sGroupMemberList(groupmember(agent("c"), alpha ^ random(2)))), sAgentList(agent("a")) sAgentList(agent("c")))

Solution 2 (state 168852)
states: 168857  rewrites: 11822450 in 302690ms cpu (302820ms real) (39057 rewrites/second)
state:State --> fresh(4)
ready(agent("a"), group("G1"), context(random(0), alpha ^ random(0) * random(2), sGroupMemberList(groupmember(agent("a"), alpha ^ random(2)))
    sGroupMemberList(groupmember(agent("b"), alpha ^ random(0)))), sAgentList(agent("a")) sAgentList(agent("b")))
ready(agent("a"), group("G2"), context(random(1), alpha ^ random(1) * random(3), sGroupMemberList(groupmember(agent("a"), alpha ^ random(3)))
    sGroupMemberList(groupmember(agent("c"), alpha ^ random(1)))), sAgentList(agent("a")) sAgentList(agent("c")))
ready(agent("b"), group("G1"), context(random(2), alpha ^ random(0) * random(2), sGroupMemberList(groupmember(agent("a"), alpha ^ random(2)))
    sGroupMemberList(groupmember(agent("b"), alpha ^ random(0)))), sAgentList(agent("a")) sAgentList(agent("b")))
ready(agent("c"), group("G2"), context(random(3), alpha ^ random(1) * random(3), sGroupMemberList(groupmember(agent("a"), alpha ^ random(3)))
    sGroupMemberList(groupmember(agent("c"), alpha ^ random(1)))), sAgentList(agent("a")) sAgentList(agent("c")))

Solution 3 (state 168853)
states: 168857  rewrites: 11822450 in 302690ms cpu (302820ms real) (39057 rewrites/second)
state:State --> fresh(4)
ready(agent("a"), group("G1"), context(random(0), alpha ^ random(0) * random(3), sGroupMemberList(groupmember(agent("a"), alpha ^ random(3)))
    sGroupMemberList(groupmember(agent("b"), alpha ^ random(0)))), sAgentList(agent("a")) sAgentList(agent("b")))
ready(agent("a"), group("G2"), context(random(1), alpha ^ random(1) * random(2), sGroupMemberList(groupmember(agent("a"), alpha ^ random(2)))
    sGroupMemberList(groupmember(agent("c"), alpha ^ random(1)))), sAgentList(agent("a")) sAgentList(agent("c")))
ready(agent("b"), group("G1"), context(random(3), alpha ^ random(0) * random(3), sGroupMemberList(groupmember(agent("a"), alpha ^ random(3)))
    sGroupMemberList(groupmember(agent("b"), alpha ^ random(0)))), sAgentList(agent("a")) sAgentList(agent("b")))
ready(agent("c"), group("G2"), context(random(2), alpha ^ random(1) * random(2), sGroupMemberList(groupmember(agent("a"), alpha ^ random(2)))
    sGroupMemberList(groupmember(agent("c"), alpha ^ random(1)))), sAgentList(agent("a")) sAgentList(agent("c")))

Solution 4 (state 168854)
states: 168857  rewrites: 11822450 in 302690ms cpu (302820ms real) (39057 rewrites/second)
state:State --> fresh(4)
ready(agent("a"), group("G1"), context(random(1), alpha ^ random(1) * random(2), sGroupMemberList(groupmember(agent("a"), alpha ^ random(2)))
    sGroupMemberList(groupmember(agent("b"), alpha ^ random(1)))), sAgentList(agent("a")) sAgentList(agent("b")))
ready(agent("a"), group("G2"), context(random(0), alpha ^ random(0) * random(3), sGroupMemberList(groupmember(agent("a"), alpha ^ random(3)))
    sGroupMemberList(groupmember(agent("c"), alpha ^ random(0)))), sAgentList(agent("a")) sAgentList(agent("c")))
ready(agent("b"), group("G1"), context(random(2), alpha ^ random(1) * random(2), sGroupMemberList(groupmember(agent("a"), alpha ^ random(2)))
    sGroupMemberList(groupmember(agent("b"), alpha ^ random(1)))), sAgentList(agent("a")) sAgentList(agent("b")))
ready(agent("c"), group("G2"), context(random(3), alpha ^ random(0) * random(3), sGroupMemberList(groupmember(agent("a"), alpha ^ random(3)))
    sGroupMemberList(groupmember(agent("c"), alpha ^ random(0)))), sAgentList(agent("a")) sAgentList(agent("c")))

Solution 5 (state 168855)
states: 168857  rewrites: 11822450 in 302690ms cpu (302820ms real) (39057 rewrites/second)
state:State --> fresh(4)
ready(agent("a"), group("G1"), context(random(1), alpha ^ random(1) * random(3), sGroupMemberList(groupmember(agent("a"), alpha ^ random(3)))
    sGroupMemberList(groupmember(agent("b"), alpha ^ random(1)))), sAgentList(agent("a")) sAgentList(agent("b")))
ready(agent("a"), group("G2"), context(random(0), alpha ^ random(0) * random(2), sGroupMemberList(groupmember(agent("a"), alpha ^ random(2)))
    sGroupMemberList(groupmember(agent("c"), alpha ^ random(0)))), sAgentList(agent("a")) sAgentList(agent("c")))
ready(agent("b"), group("G1"), context(random(3), alpha ^ random(1) * random(3), sGroupMemberList(groupmember(agent("a"), alpha ^ random(3)))
    sGroupMemberList(groupmember(agent("b"), alpha ^ random(1)))), sAgentList(agent("a")) sAgentList(agent("b")))
ready(agent("c"), group("G2"), context(random(2), alpha ^ random(0) * random(2), sGroupMemberList(groupmember(agent("a"), alpha ^ random(2)))
    sGroupMemberList(groupmember(agent("c"), alpha ^ random(0)))), sAgentList(agent("a")) sAgentList(agent("c")))

Solution 6 (state 168856)
states: 168857  rewrites: 11822450 in 302690ms cpu (302870ms real) (39057 rewrites/second)
state:State --> fresh(4)
ready(agent("a"), group("G1"), context(random(2), alpha ^ random(2) * random(3), sGroupMemberList(groupmember(agent("a"), alpha ^ random(3)))
    sGroupMemberList(groupmember(agent("b"), alpha ^ random(2)))), sAgentList(agent("a")) sAgentList(agent("b")))
ready(agent("a"), group("G2"), context(random(0), alpha ^ random(0) * random(1), sGroupMemberList(groupmember(agent("a"), alpha ^ random(1)))
    sGroupMemberList(groupmember(agent("c"), alpha ^ random(0)))), sAgentList(agent("a")) sAgentList(agent("c")))
ready(agent("b"), group("G1"), context(random(3), alpha ^ random(2) * random(3), sGroupMemberList(groupmember(agent("a"), alpha ^ random(3)))
    sGroupMemberList(groupmember(agent("b"), alpha ^ random(2)))), sAgentList(agent("a")) sAgentList(agent("b")))
ready(agent("c"), group("G2"), context(random(1), alpha ^ random(0) * random(1), sGroupMemberList(groupmember(agent("a"), alpha ^ random(1)))
    sGroupMemberList(groupmember(agent("c"), alpha ^ random(0)))), sAgentList(agent("a")) sAgentList(agent("c")))

No more solutions.
states: 168857  rewrites: 11822450 in 302690ms cpu (302870ms real) (39057 rewrites/second)
==========================================
 .
Reading in file: "model-checker.maude"
==========================================
fmod LTL
==========================================
fmod LTL-SIMPLIFIER
==========================================
fmod SAT-SOLVER
==========================================
fmod SATISFACTION
==========================================
fmod MODEL-CHECKER
Done reading in file: "model-checker.maude"
==========================================
mod CLIQUES-MODEL-CHECK-1
Warning: "examples.maude", line 93 (mod CLIQUES-MODEL-CHECK-1): sort State has been imported from both "model-checker.maude", line 193 (fmod
    SATISFACTION) and "cliques.maude", line 747 (mod CLIQUES).
Advisory: "cliques.maude", line 203 (mod CLIQUES): collapse at top of x:PartialKey * inv(x:PartialKey) may cause it to match more than you expect.
Advisory: "cliques.maude", line 220 (mod CLIQUES): collapse at top of x:KeyShare * inv(x:KeyShare) may cause it to match more than you expect.
==========================================
reduce in CLIQUES-MODEL-CHECK-1 : modelCheck(initial, <> done) .
rewrites: 27753469 in 257920ms cpu (258180ms real) (107604 rewrites/second)
result Bool: true
==========================================
mod CLIQUES-MODEL-CHECK-2
Warning: "examples.maude", line 125 (mod CLIQUES-MODEL-CHECK-2): sort State has been imported from both "model-checker.maude", line 193 (fmod
    SATISFACTION) and "cliques.maude", line 747 (mod CLIQUES).