\||||||||||||||||||/
		   --- Welcome to Maude ---
		     /||||||||||||||||||\
	Maude alpha 77 built: Jan  6 2003 19:36:42
	     Copyright 1997-2003 SRI International
		   Tue Mar 25 14:37:32 2003
Maude> in basic-test-1.maude 
==========================================

Reading in file: "sectrace.maude"
==========================================
mod SECTRACE
Done reading in file: "sectrace.maude"
==========================================
search in SECTRACE : shost(node("C"))
shost(node("SG1"))
shost(node("SG2"))
shost(node("S"))
sgw(node("SG1"))
sgw(node("SG2"))
sectraced(node("C"))
sectraced(node("SG1"))
sectraced(node("SG2"))
sectraced(node("S"))
subnet(sAddrSet(addr("Ca")) sAddrSet(addr("SG1a")))
subnet(sAddrSet(addr("SG1b")) sAddrSet(addr("SG2a")))
subnet(sAddrSet(addr("SG2b")) sAddrSet(addr("Sa")))
interfaces(node("C"), sAddrSet(addr("Ca")))
interfaces(node("S"), sAddrSet(addr("Sa")))
interfaces(node("SG1"), sAddrSet(addr("SG1a")) sAddrSet(addr("SG1b")))
interfaces(node("SG2"), sAddrSet(addr("SG2a")) sAddrSet(addr("SG2b")))
routetab(node("C"), sRouteList(route(addr("Ca"), addr("Ca"), addr("Ca")))
    sRouteList(route(addr("SG1a"), addr("Ca"), addr("SG1a"))) sRouteList(route(
    addr("SG1b"), addr("Ca"), addr("SG1a"))) sRouteList(route(addr("SG2a"),
    addr("Ca"), addr("SG1a"))) sRouteList(route(addr("SG2b"), addr("Ca"), addr(
    "SG1a"))) sRouteList(route(addr("Sa"), addr("Ca"), addr("SG1a"))))
routetab(node("SG1"), 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(
    "Ca"), addr("SG1a"), addr("Ca"))) sRouteList(route(addr("Sa"), addr(
    "SG1b"), addr("SG2a"))))
routetab(node("SG2"), sRouteList(route(addr("SG2a"), addr("SG2a"), addr(
    "SG2a"))) sRouteList(route(addr("SG2b"), addr("SG2b"), addr("SG2b")))
    sRouteList(route(addr("SG1a"), addr("SG2a"), addr("SG1b"))) sRouteList(
    route(addr("SG1b"), addr("SG2a"), addr("SG1b"))) sRouteList(route(addr(
    "Ca"), addr("SG2a"), addr("SG1b"))) sRouteList(route(addr("Sa"), addr(
    "SG2b"), addr("Sa"))))
routetab(node("S"), sRouteList(route(addr("Sa"), addr("Sa"), addr("Sa")))
    sRouteList(route(addr("Ca"), addr("Sa"), addr("SG2b"))) sRouteList(route(
    addr("SG1b"), addr("Sa"), addr("SG2b"))) sRouteList(route(addr("SG1a"),
    addr("Sa"), addr("SG2b"))) sRouteList(route(addr("SG2a"), addr("Sa"), addr(
    "SG2b"))) sRouteList(route(addr("SG2b"), addr("Sa"), addr("SG2b"))))
((((sadb(node("C"), eSASet)
sadb(node("SG1"), eSASet)
sadb(node("SG2"), eSASet)
sadb(node("S"), eSASet)
(((spdb(node("S"), eSPList, sSPList(sp(isinitiation, eSAList)) sSPList(sp(
    isresponse, eSAList)))
sectrace-start(node("C"), addr("Ca"), addr("Sa")))
spdb(node("SG2"), eSPList, sSPList(sp(isinitiation, eSAList)) sSPList(sp(
    isresponse, eSAList))))
spdb(node("SG1"), eSPList, sSPList(sp(isinitiation, eSAList)) sSPList(sp(
    isresponse, eSAList))))
spdb(node("C"), eSPList, sSPList(sp(isinitiation, eSAList)) sSPList(sp(
    isresponse, eSAList))))
rootinfo(node("S"), addr("CA1"), sAddrSet(addr("CA1"))))
rootinfo(node("SG2"), addr("CA1"), sAddrSet(addr("CA1"))))
rootinfo(node("SG1"), addr("CA1"), sAddrSet(addr("CA1"))))
rootinfo(node("C"), addr("CA1"), sAddrSet(addr("CA1"))) =>! state:State .

Solution 1 (state 104)
states: 105  rewrites: 36955 in 50ms cpu (50ms real) (739100 rewrites/second)
state:State --> subnet(sAddrSet(addr("Ca")) sAddrSet(addr("SG1a")))
subnet(sAddrSet(addr("SG1b")) sAddrSet(addr("SG2a")))
subnet(sAddrSet(addr("SG2b")) sAddrSet(addr("Sa")))
shost(node("C"))
shost(node("S"))
shost(node("SG1"))
shost(node("SG2"))
sgw(node("SG1"))
sgw(node("SG2"))
sectraced(node("C"))
sectraced(node("S"))
sectraced(node("SG1"))
sectraced(node("SG2"))
interfaces(node("C"), sAddrSet(addr("Ca")))
interfaces(node("S"), sAddrSet(addr("Sa")))
interfaces(node("SG1"), sAddrSet(addr("SG1a")) sAddrSet(addr("SG1b")))
interfaces(node("SG2"), sAddrSet(addr("SG2a")) sAddrSet(addr("SG2b")))
routetab(node("C"), sRouteList(route(addr("Ca"), addr("Ca"), addr("Ca")))
    sRouteList(route(addr("SG1a"), addr("Ca"), addr("SG1a"))) sRouteList(route(
    addr("SG1b"), addr("Ca"), addr("SG1a"))) sRouteList(route(addr("SG2a"),
    addr("Ca"), addr("SG1a"))) sRouteList(route(addr("SG2b"), addr("Ca"), addr(
    "SG1a"))) sRouteList(route(addr("Sa"), addr("Ca"), addr("SG1a"))))
routetab(node("S"), sRouteList(route(addr("Sa"), addr("Sa"), addr("Sa")))
    sRouteList(route(addr("Ca"), addr("Sa"), addr("SG2b"))) sRouteList(route(
    addr("SG1b"), addr("Sa"), addr("SG2b"))) sRouteList(route(addr("SG1a"),
    addr("Sa"), addr("SG2b"))) sRouteList(route(addr("SG2a"), addr("Sa"), addr(
    "SG2b"))) sRouteList(route(addr("SG2b"), addr("Sa"), addr("SG2b"))))
routetab(node("SG1"), 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(
    "Ca"), addr("SG1a"), addr("Ca"))) sRouteList(route(addr("Sa"), addr(
    "SG1b"), addr("SG2a"))))
routetab(node("SG2"), sRouteList(route(addr("SG2a"), addr("SG2a"), addr(
    "SG2a"))) sRouteList(route(addr("SG2b"), addr("SG2b"), addr("SG2b")))
    sRouteList(route(addr("SG1a"), addr("SG2a"), addr("SG1b"))) sRouteList(
    route(addr("SG1b"), addr("SG2a"), addr("SG1b"))) sRouteList(route(addr(
    "Ca"), addr("SG2a"), addr("SG1b"))) sRouteList(route(addr("Sa"), addr(
    "SG2b"), addr("Sa"))))
sadb(node("C"), sSASet(sa(addr("Ca"), addr("SG1a"), 0)))
sadb(node("S"), sSASet(sa(addr("SG2a"), addr("Sa"), 0)))
sadb(node("SG1"), sSASet(sa(addr("Ca"), addr("SG1a"), 0)) sSASet(sa(addr(
    "SG1a"), addr("SG2a"), 0)))
sadb(node("SG2"), sSASet(sa(addr("SG1a"), addr("SG2a"), 0)) sSASet(sa(addr(
    "SG2a"), addr("Sa"), 0)))
rootinfo(node("C"), addr("CA1"), sAddrSet(addr("CA1")))
rootinfo(node("S"), addr("CA1"), sAddrSet(addr("CA1")))
rootinfo(node("SG1"), addr("CA1"), sAddrSet(addr("CA1")))
rootinfo(node("SG2"), addr("CA1"), sAddrSet(addr("CA1")))
spdb(node("C"), eSPList, sSPList(sp(towards(addr("Sa")), sSAList(sa(addr("Ca"),
    addr("SG1a"), 0)))) sSPList(sp(isinitiation, eSAList)) sSPList(sp(
    isresponse, eSAList)))
spdb(node("S"), sSPList(sp(towards(addr("Sa")), sSAList(sa(addr("SG2a"), addr(
    "Sa"), 0)))), sSPList(sp(isinitiation, eSAList)) sSPList(sp(isresponse,
    eSAList)))
spdb(node("SG1"), sSPList(sp(towards(addr("Sa")), sSAList(sa(addr("Ca"), 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("SG1a"),
    addr("SG2a"), 0)))), sSPList(sp(towards(addr("Sa")), sSAList(sa(addr(
    "SG2a"), addr("Sa"), 0)))) sSPList(sp(isinitiation, eSAList)) sSPList(sp(
    isresponse, eSAList)))
sectrace-terminated(node("C"), addr("Ca"), addr("Sa"))

No more solutions.
states: 105  rewrites: 36955 in 60ms cpu (80ms real) (615916 rewrites/second)
Maude>