\||||||||||||||||||/
		   --- Welcome to Maude ---
		     /||||||||||||||||||\
	Maude alpha 77 built: Jan  6 2003 19:36:42
	     Copyright 1997-2003 SRI International
		   Tue Mar 25 14:39:13 2003
Maude> in ext-test-seq-c1-c2.maude
==========================================

Reading in file: "sectrace.maude"
==========================================
mod SECTRACE
Done reading in file: "sectrace.maude"
==========================================
mod EXT-TEST-SEQ-C1-C2
==========================================
search in EXT-TEST-SEQ-C1-C2 : network
start =>! state:State .

Solution 1 (state 304)
states: 305  rewrites: 434933 in 370ms cpu (370ms real) (1175494
    rewrites/second)
state:State --> terminated
subnet(sAddrSet(addr("C2a")) sAddrSet(addr("SG1a")))
subnet(sAddrSet(addr("SG1b")) sAddrSet(addr("SG2a")))
subnet(sAddrSet(addr("C1a")) sAddrSet(addr("SG2b")))
subnet(sAddrSet(addr("SG2c")) sAddrSet(addr("SG3a")))
subnet(sAddrSet(addr("SG3b")) sAddrSet(addr("SG4a")))
subnet(sAddrSet(addr("SG4b")) sAddrSet(addr("Sa")))
shost(node("C1"))
shost(node("C2"))
shost(node("S"))
shost(node("SG1"))
shost(node("SG2"))
shost(node("SG3"))
shost(node("SG4"))
sgw(node("SG1"))
sgw(node("SG2"))
sgw(node("SG3"))
sgw(node("SG4"))
sectraced(node("C1"))
sectraced(node("C2"))
sectraced(node("S"))
sectraced(node("SG1"))
sectraced(node("SG2"))
sectraced(node("SG3"))
sectraced(node("SG4"))
interfaces(node("C1"), sAddrSet(addr("C1a")))
interfaces(node("C2"), sAddrSet(addr("C2a")))
interfaces(node("S"), sAddrSet(addr("Sa")))
interfaces(node("SG1"), sAddrSet(addr("SG1a")) sAddrSet(addr("SG1b")))
interfaces(node("SG2"), sAddrSet(addr("SG2a")) sAddrSet(addr("SG2b")) sAddrSet(
    addr("SG2c")))
interfaces(node("SG3"), sAddrSet(addr("SG3a")) sAddrSet(addr("SG3b")))
interfaces(node("SG4"), sAddrSet(addr("SG4a")) sAddrSet(addr("SG4b")))
routetab(node("C1"), sRouteList(route(addr("C1a"), addr("C1a"), addr("C1a")))
    sRouteList(route(addr("C2a"), addr("C1a"), addr("SG2b"))) sRouteList(route(
    addr("SG1a"), addr("C1a"), addr("SG2b"))) sRouteList(route(addr("SG1b"),
    addr("C1a"), addr("SG2b"))) sRouteList(route(addr("SG2a"), addr("C1a"),
    addr("SG2b"))) sRouteList(route(addr("SG2b"), addr("C1a"), addr("SG2b")))
    sRouteList(route(addr("SG2c"), addr("C1a"), addr("SG2b"))) sRouteList(
    route(addr("SG3a"), addr("C1a"), addr("SG2b"))) sRouteList(route(addr(
    "SG3b"), addr("C1a"), addr("SG2b"))) sRouteList(route(addr("SG4a"), addr(
    "C1a"), addr("SG2b"))) sRouteList(route(addr("SG4b"), addr("C1a"), addr(
    "SG2b"))) sRouteList(route(addr("Sa"), addr("C1a"), addr("SG2b"))))
routetab(node("C2"), sRouteList(route(addr("C1a"), addr("C2a"), addr("SG1a")))
    sRouteList(route(addr("C2a"), addr("C2a"), addr("C2a"))) sRouteList(route(
    addr("SG1a"), addr("C2a"), addr("SG1a"))) sRouteList(route(addr("SG1b"),
    addr("C2a"), addr("SG1a"))) sRouteList(route(addr("SG2a"), addr("C2a"),
    addr("SG1a"))) sRouteList(route(addr("SG2b"), addr("C2a"), addr("SG1a")))
    sRouteList(route(addr("SG2c"), addr("C2a"), addr("SG1a"))) sRouteList(
    route(addr("SG3a"), addr("C2a"), addr("SG1a"))) sRouteList(route(addr(
    "SG3b"), addr("C2a"), addr("SG1a"))) sRouteList(route(addr("SG4a"), addr(
    "C2a"), addr("SG1a"))) sRouteList(route(addr("SG4b"), addr("C2a"), addr(
    "SG1a"))) sRouteList(route(addr("Sa"), addr("C2a"), addr("SG1a"))))
routetab(node("S"), sRouteList(route(addr("C1a"), addr("Sa"), addr("SG4b")))
    sRouteList(route(addr("C2a"), addr("Sa"), addr("SG4b"))) sRouteList(route(
    addr("SG1a"), addr("Sa"), addr("SG4b"))) sRouteList(route(addr("SG1b"),
    addr("Sa"), addr("SG4b"))) sRouteList(route(addr("SG2a"), addr("Sa"), addr(
    "SG4b"))) sRouteList(route(addr("SG2b"), addr("Sa"), addr("SG4b")))
    sRouteList(route(addr("SG2c"), addr("Sa"), addr("SG4b"))) sRouteList(route(
    addr("SG3a"), addr("Sa"), addr("SG4b"))) sRouteList(route(addr("SG3b"),
    addr("Sa"), addr("SG4b"))) sRouteList(route(addr("SG4a"), addr("Sa"), addr(
    "SG4b"))) sRouteList(route(addr("SG4b"), addr("Sa"), addr("SG4b")))
    sRouteList(route(addr("Sa"), addr("Sa"), addr("Sa"))))
routetab(node("SG1"), sRouteList(route(addr("C1a"), addr("SG1b"), addr(
    "SG2a"))) sRouteList(route(addr("C2a"), addr("SG1a"), addr("C2a")))
    sRouteList(route(addr("SG1a"), addr("SG1a"), addr("SG1a"))) sRouteList(
    route(addr("SG1b"), addr("SG1b"), addr("SG1b"))) sRouteList(route(addr(
    "SG2a"), addr("SG1b"), addr("SG2a"))) sRouteList(route(addr("SG2b"), addr(
    "SG1b"), addr("SG2a"))) sRouteList(route(addr("SG2c"), addr("SG1b"), addr(
    "SG2a"))) sRouteList(route(addr("SG3a"), addr("SG1b"), addr("SG2a")))
    sRouteList(route(addr("SG3b"), addr("SG1b"), addr("SG2a"))) sRouteList(
    route(addr("SG4a"), addr("SG1b"), addr("SG2a"))) sRouteList(route(addr(
    "SG4b"), addr("SG1b"), addr("SG2a"))) sRouteList(route(addr("Sa"), addr(
    "SG1b"), addr("SG2a"))))
routetab(node("SG2"), sRouteList(route(addr("C1a"), addr("SG2b"), addr("C1a")))
    sRouteList(route(addr("C2a"), addr("SG2a"), addr("SG1b"))) sRouteList(
    route(addr("SG1a"), addr("SG2a"), addr("SG1b"))) sRouteList(route(addr(
    "SG1b"), addr("SG2a"), addr("SG1b"))) sRouteList(route(addr("SG2a"), addr(
    "SG2a"), addr("SG2a"))) sRouteList(route(addr("SG2b"), addr("SG2b"), addr(
    "SG2b"))) sRouteList(route(addr("SG2c"), addr("SG2c"), addr("SG2c")))
    sRouteList(route(addr("SG3a"), addr("SG2c"), addr("SG3a"))) sRouteList(
    route(addr("SG3b"), addr("SG2c"), addr("SG3a"))) sRouteList(route(addr(
    "SG4a"), addr("SG2c"), addr("SG3a"))) sRouteList(route(addr("SG4b"), addr(
    "SG2c"), addr("SG3a"))) sRouteList(route(addr("Sa"), addr("SG2c"), addr(
    "SG3a"))))
routetab(node("SG3"), sRouteList(route(addr("C1a"), addr("SG3a"), addr(
    "SG2c"))) sRouteList(route(addr("C2a"), addr("SG3a"), addr("SG2c")))
    sRouteList(route(addr("SG1a"), addr("SG3a"), addr("SG2c"))) sRouteList(
    route(addr("SG1b"), addr("SG3a"), addr("SG2c"))) sRouteList(route(addr(
    "SG2a"), addr("SG3a"), addr("SG2c"))) sRouteList(route(addr("SG2b"), addr(
    "SG3a"), addr("SG2c"))) sRouteList(route(addr("SG2c"), addr("SG3a"), addr(
    "SG2c"))) sRouteList(route(addr("SG3a"), addr("SG3a"), addr("SG3a")))
    sRouteList(route(addr("SG3b"), addr("SG3b"), addr("SG3b"))) sRouteList(
    route(addr("SG4a"), addr("SG3b"), addr("SG4a"))) sRouteList(route(addr(
    "SG4b"), addr("SG3b"), addr("SG4a"))) sRouteList(route(addr("Sa"), addr(
    "SG3b"), addr("SG4a"))))
routetab(node("SG4"), sRouteList(route(addr("C1a"), addr("SG4a"), addr(
    "SG3b"))) sRouteList(route(addr("C2a"), addr("SG4a"), addr("SG3b")))
    sRouteList(route(addr("SG1a"), addr("SG4a"), addr("SG3b"))) sRouteList(
    route(addr("SG1b"), addr("SG4a"), addr("SG3b"))) sRouteList(route(addr(
    "SG2a"), addr("SG4a"), addr("SG3b"))) sRouteList(route(addr("SG2b"), addr(
    "SG4a"), addr("SG3b"))) sRouteList(route(addr("SG2c"), addr("SG4a"), addr(
    "SG3b"))) sRouteList(route(addr("SG3a"), addr("SG4a"), addr("SG3b")))
    sRouteList(route(addr("SG3b"), addr("SG4a"), addr("SG3b"))) sRouteList(
    route(addr("SG4a"), addr("SG4a"), addr("SG4a"))) sRouteList(route(addr(
    "SG4b"), addr("SG4b"), addr("SG4b"))) sRouteList(route(addr("Sa"), addr(
    "SG4b"), addr("Sa"))))
sadb(node("C1"), sSASet(sa(addr("C1a"), addr("SG2b"), 0)) sSASet(sa(addr(
    "C1a"), addr("SG3a"), 0)))
sadb(node("C2"), sSASet(sa(addr("C2a"), addr("SG1a"), 0)) sSASet(sa(addr(
    "C2a"), addr("SG3a"), 0)))
sadb(node("S"), sSASet(sa(addr("SG4a"), addr("Sa"), 0)))
sadb(node("SG1"), sSASet(sa(addr("C2a"), addr("SG1a"), 0)) sSASet(sa(addr(
    "SG1a"), addr("SG2a"), 0)))
sadb(node("SG2"), sSASet(sa(addr("C1a"), addr("SG2b"), 0)) sSASet(sa(addr(
    "SG1a"), addr("SG2a"), 0)))
sadb(node("SG3"), sSASet(sa(addr("C1a"), addr("SG3a"), 0)) sSASet(sa(addr(
    "C2a"), addr("SG3a"), 0)) sSASet(sa(addr("SG3a"), addr("SG4a"), 0)))
sadb(node("SG4"), sSASet(sa(addr("SG3a"), addr("SG4a"), 0)) sSASet(sa(addr(
    "SG4a"), addr("Sa"), 0)))
rootinfo(node("C1"), addr("CAC1"), sAddrSet(addr("CAC1")))
rootinfo(node("C2"), addr("CAC2"), sAddrSet(addr("CAC2")))
rootinfo(node("S"), addr("CAS"), sAddrSet(addr("CAC1")) sAddrSet(addr("CAC2"))
    sAddrSet(addr("CAS")) sAddrSet(addr("CASG3")) sAddrSet(addr("CASG4")))
rootinfo(node("SG1"), addr("CASG1"), sAddrSet(addr("CAC2")) sAddrSet(addr(
    "CASG1")))
rootinfo(node("SG2"), addr("CASG2"), sAddrSet(addr("CAC1")) sAddrSet(addr(
    "CASG1")) sAddrSet(addr("CASG2")))
rootinfo(node("SG3"), addr("CASG3"), sAddrSet(addr("CAC1")) sAddrSet(addr(
    "CAC2")) sAddrSet(addr("CASG3")))
rootinfo(node("SG4"), addr("CASG4"), sAddrSet(addr("CASG3")) sAddrSet(addr(
    "CASG4")))
spdb(node("C1"), eSPList, sSPList(sp(towards(addr("Sa")), sSAList(sa(addr(
    "C1a"), addr("SG3a"), 0)) sSAList(sa(addr("C1a"), addr("SG2b"), 0))))
    sSPList(sp(isinitiation, eSAList)) sSPList(sp(isresponse, eSAList)))
spdb(node("C2"), eSPList, sSPList(sp(towards(addr("Sa")), sSAList(sa(addr(
    "C2a"), addr("SG3a"), 0)) sSAList(sa(addr("C2a"), addr("SG1a"), 0))))
    sSPList(sp(isinitiation, eSAList)) sSPList(sp(isresponse, eSAList)))
spdb(node("S"), sSPList(sp(towards(addr("Sa")), sSAList(sa(addr("SG4a"), addr(
    "Sa"), 0)))), sSPList(sp(isinitiation, eSAList)) sSPList(sp(isresponse,
    eSAList)))
spdb(node("SG1"), sSPList(sp(towards(addr("Sa")), sSAList(sa(addr("C2a"), addr(
    "SG1a"), 0)))), sSPList(sp(towards(addr("Sa")), sSAList(sa(addr("SG1a"),
    addr("SG2a"), 0)))) sSPList(sp(isinitiation, eSAList)) sSPList(sp(
    isresponse, eSAList)))
spdb(node("SG2"), sSPList(sp(towards(addr("Sa")), sSAList(sa(addr("C1a"), addr(
    "SG2b"), 0)))) sSPList(sp(towards(addr("Sa")), sSAList(sa(addr("SG1a"),
    addr("SG2a"), 0)))), sSPList(sp(isinitiation, eSAList)) sSPList(sp(
    isresponse, eSAList)))
spdb(node("SG3"), sSPList(sp(towards(addr("Sa")), sSAList(sa(addr("C1a"), addr(
    "SG3a"), 0)))) sSPList(sp(towards(addr("Sa")), sSAList(sa(addr("C2a"),
    addr("SG3a"), 0)))), sSPList(sp(towards(addr("Sa")), sSAList(sa(addr(
    "SG3a"), addr("SG4a"), 0)))) sSPList(sp(isinitiation, eSAList)) sSPList(sp(
    isresponse, eSAList)))
spdb(node("SG4"), sSPList(sp(towards(addr("Sa")), sSAList(sa(addr("SG3a"),
    addr("SG4a"), 0)))), sSPList(sp(towards(addr("Sa")), sSAList(sa(addr(
    "SG4a"), addr("Sa"), 0)))) sSPList(sp(isinitiation, eSAList)) sSPList(sp(
    isresponse, eSAList)))

No more solutions.
states: 305  rewrites: 434933 in 370ms cpu (1070ms real) (1175494
    rewrites/second)
Maude>