*** 
*** Exhaustive Search (~2:39min on Linux, 450Mhz, PII)
***

Maude> (red irreducibleforms ( RBP , { 'test1 } 'Configuration , alldynamicrules ) .) 

Reduce in METATEST : irreducibleforms ( RBP , { 'test1 } 'Configuration ,
    alldynamicrules ) . 
Result TermSet : 
set ( '__ [ 
'<_:_|_> [ 
  { 'a } 'Oid , { 'Node } 'Node , [ 
  'nbs`:_ [ 'nbs [ { 'b } 'Oid , { 'c } 'Oid ] ] , 
  'nbsStates`:_ [ 'nbsStates [ 
     'nbState [ { 'a } 'Oid , { 'b } 'Oid , { 'passive } 'Status ] , 
     'nbState [ { 'a } 'Oid , { 'c } 'Oid , { 'passive } 'Status ] ,
     'nbState [ { 'b } 'Oid , { 'b } 'Oid , { 'passive } 'Status ] , 
     'nbState [ { 'b } 'Oid , { 'c } 'Oid , { 'passive } 'Status ] ,
     'nbState [ { 'c } 'Oid , { 'b } 'Oid , { 'passive } 'Status ] , 
     'nbState [ { 'c } 'Oid , { 'c } 'Oid , { 'passive } 'Status ] ] ] , 
  'seqNos`:_ [ 'seqNos [ 
     'seqNo [ { 'a } 'Oid , { '1 } 'NzMachineInt ] , 
     'seqNo [ { 'b } 'Oid , { '0 } 'MachineInt ] , 
     'seqNo [ { 'c } 'Oid , { '0 } 'MachineInt ] ] ] , 
  'parents`:_ [ 'parent [ { 'a } 'Oid , { 'a } 'Oid ] ] , 
  'states`:_ [ 'states [ 
     'state [ { 'a } 'Oid , { 'passive } 'Status ] , 
     'state [ { 'b } 'Oid , { 'passive } 'Status ] , 
     'state [ { 'c } 'Oid , { 'passive } 'Status ] ] ] ] ] , 

'<_:_|_> [ 
  { 'b } 'Oid , { 'Node } 'Node , '_`,_ [  
  'nbs`:_ [ 'nbs [ { 'a } 'Oid , { 'c } 'Oid ] ] , 
  'nbsStates`:_ [ 'nbsStates [  
     'nbState [ { 'a } 'Oid , { 'a } 'Oid , { 'passive } 'Status ] ,  
     'nbState [ { 'a } 'Oid , { 'c } 'Oid , { 'passive } 'Status ] ,
     'nbState [ { 'b } 'Oid , { 'a } 'Oid , { 'passive } 'Status ] ,
     'nbState [ { 'b } 'Oid , { 'c } 'Oid , { 'passive } 'Status ] , 
     'nbState [ { 'c } 'Oid , { 'a } 'Oid , { 'passive } 'Status ] , 
     'nbState [ { 'c } 'Oid , { 'c } 'Oid , { 'passive } 'Status ] ] ] , 
  'seqNos`:_ [ 
     'seqNos [ 
     'seqNo [ { 'a } 'Oid , { '1 } 'NzMachineInt ] , 
     'seqNo [ { 'b } 'Oid , { '0 } 'MachineInt ] , 
     'seqNo [ { 'c } 'Oid , { '0 } 'MachineInt ] ] ] ,  
  'parents`:_ [ 'parent [ { 'a } 'Oid , { 'a } 'Oid ] ] ,  
  'states`:_ [ 'states [  
     'state [ { 'a } 'Oid , { 'passive } 'Status ] ,  
     'state [ { 'b } 'Oid , { 'passive } 'Status ] ,  
     'state [ { 'c } 'Oid , { 'passive } 'Status ] ] ] ] ] ,  

'<_:_|_> [ 
  { 'c } 'Oid , { 'Node } 'Node , '_`,_ [  
  'nbs`:_ [ 'nbs [ { 'a } 'Oid , { 'b } 'Oid ] ] , 
  'nbsStates`:_ [ 'nbsStates [  
     'nbState [ { 'a } 'Oid , { 'a } 'Oid , { 'passive } 'Status ] ,  
     'nbState [ { 'a } 'Oid , { 'b } 'Oid , { 'passive } 'Status ] ,
     'nbState [ { 'b } 'Oid , { 'a } 'Oid , { 'passive } 'Status ] ,
     'nbState [ { 'b } 'Oid , { 'b } 'Oid , { 'passive } 'Status ] , 
     'nbState [ { 'c } 'Oid , { 'a } 'Oid , { 'passive } 'Status ] , 
     'nbState [ { 'c } 'Oid , { 'a } 'Oid , { 'passive } 'Status ] ] ] , 
  'seqNos`:_ [ 
     'seqNos [ 
     'seqNo [ { 'a } 'Oid , { '1 } 'NzMachineInt ] , 
     'seqNo [ { 'b } 'Oid , { '0 } 'MachineInt ] , 
     'seqNo [ { 'c } 'Oid , { '0 } 'MachineInt ] ] ] ,  
  'parents`:_ [ 'parent [ { 'a } 'Oid , { 'a } 'Oid ] ] ,  
  'states`:_ [ 'states [  
     'state [ { 'a } 'Oid , { 'passive } 'Status ] ,  
     'state [ { 'b } 'Oid , { 'passive } 'Status ] ,  
     'state [ { 'c } 'Oid , { 'passive } 'Status ] ] ] ] ] ] , 
     
'__ [  
'<_:_|_> [ 
  { 'a } 'Oid , { 'Node } 'Node , '_`,_ [  
  'nbs`:_ [ 'nbs [ { 'b } 'Oid , { 'c } 'Oid ] ] , 
  'nbsStates`:_ [ 'nbsStates [  
     'nbState [ { 'a } 'Oid , { 'b } 'Oid , { 'passive } 'Status ] ,  
     'nbState [ { 'a } 'Oid , { 'c } 'Oid , { 'passive } 'Status ] ,
     'nbState [ { 'b } 'Oid , { 'b } 'Oid , { 'passive } 'Status ] , 
     'nbState [ { 'b } 'Oid , { 'c } 'Oid , { 'passive } 'Status ] ,
     'nbState [ { 'c } 'Oid , { 'b } 'Oid , { 'passive } 'Status ] , 
     'nbState [ { 'c } 'Oid , { 'c } 'Oid , { 'passive } 'Status ] ] ] ,  
  'seqNos`:_ [ 
     'seqNos [ 
     'seqNo [ { 'a } 'Oid , { '1 } 'NzMachineInt ] , 
     'seqNo [ { 'b } 'Oid , { '0 } 'MachineInt ] , 
     'seqNo [ { 'c } 'Oid , { '0 } 'MachineInt ] ] ] ,  
  'parents`:_ [ 'parent [ { 'a } 'Oid , { 'a } 'Oid ] ] ,  
  'states`:_ [ 'states [  
     'state [ { 'a } 'Oid , { 'passive } 'Status ] ,  
     'state [ { 'b } 'Oid , { 'passive } 'Status ] ,  
     'state [ { 'c } 'Oid , { 'passive } 'Status ] ] ] ] ] ,  

'<_:_|_> [ 
  { 'b } 'Oid , { 'Node } 'Node , '_`,_ [  
  'nbs`:_ [ 'nbs [ { 'a } 'Oid , { 'c } 'Oid ] ] , 
  'nbsStates`:_ [ 'nbsStates [  
     'nbState [ { 'a } 'Oid , { 'a } 'Oid , { 'passive } 'Status ] ,  
     'nbState [ { 'a } 'Oid , { 'c } 'Oid , { 'passive } 'Status ] ,
     'nbState [ { 'b } 'Oid , { 'a } 'Oid , { 'passive } 'Status ] ,
     'nbState [ { 'b } 'Oid , { 'c } 'Oid , { 'passive } 'Status ] , 
     'nbState [ { 'c } 'Oid , { 'a } 'Oid , { 'passive } 'Status ] , 
     'nbState [ { 'c } 'Oid , { 'c } 'Oid , { 'passive } 'Status ] ] ] ,  
  'seqNos`:_ [ 
     'seqNos [ 
     'seqNo [ { 'a } 'Oid , { '1 } 'NzMachineInt ] , 
     'seqNo [ { 'b } 'Oid , { '0 } 'MachineInt ] , 
     'seqNo [ { 'c } 'Oid , { '0 } 'MachineInt ] ] ] ,  
  'parents`:_ [ 'parent [ { 'a } 'Oid , { 'a } 'Oid ] ] ,  
  'states`:_ [ 'states [  
     'state [ { 'a } 'Oid , { 'passive } 'Status ] ,  
     'state [ { 'b } 'Oid , { 'passive } 'Status ] ,  
     'state [ { 'c } 'Oid , { 'passive } 'Status ] ] ] ] ] ,  

'<_:_|_> [ 
  { 'c } 'Oid , { 'Node } 'Node , '_`,_ [  
  'nbs`:_ [ 'nbs [ { 'a } 'Oid , { 'b } 'Oid ] ] , 
  'nbsStates`:_ [ 'nbsStates [  
     'nbState [ { 'a } 'Oid , { 'a } 'Oid , { 'passive } 'Status ] ,  
     'nbState [ { 'a } 'Oid , { 'b } 'Oid , { 'passive } 'Status ] ,
     'nbState [ { 'b } 'Oid , { 'a } 'Oid , { 'passive } 'Status ] ,
     'nbState [ { 'b } 'Oid , { 'b } 'Oid , { 'passive } 'Status ] , 
     'nbState [ { 'c } 'Oid , { 'a } 'Oid , { 'passive } 'Status ] , 
     'nbState [ { 'c } 'Oid , { 'a } 'Oid , { 'passive } 'Status ] ] ] ,  
  'seqNos`:_ [ 
     'seqNos [ 
     'seqNo [ { 'a } 'Oid , { '1 } 'NzMachineInt ] , 
     'seqNo [ { 'b } 'Oid , { '0 } 'MachineInt ] , 
     'seqNo [ { 'c } 'Oid , { '0 } 'MachineInt ] ] ] ,  
  'parents`:_ [ 'parent [ { 'a } 'Oid , { 'b } 'Oid ] ] ,  
  'states`:_ [ 'states [  
     'state [ { 'a } 'Oid , { 'passive } 'Status ] ,  
     'state [ { 'b } 'Oid , { 'passive } 'Status ] ,  
     'state [ { 'c } 'Oid , { 'passive } 'Status ] ] ] ] ] ] , 
  
  
'__ [  
'<_:_|_> [ 
  { 'a } 'Oid , { 'Node } 'Node , '_`,_ [  
  'nbs`:_ [ 'nbs [ { 'b } 'Oid , { 'c } 'Oid ] ] , 
  'nbsStates`:_ [ 'nbsStates [  
     'nbState [ { 'a } 'Oid , { 'b } 'Oid , { 'passive } 'Status ] ,  
     'nbState [ { 'a } 'Oid , { 'c } 'Oid , { 'passive } 'Status ] ,
     'nbState [ { 'b } 'Oid , { 'b } 'Oid , { 'passive } 'Status ] , 
     'nbState [ { 'b } 'Oid , { 'c } 'Oid , { 'passive } 'Status ] ,
     'nbState [ { 'c } 'Oid , { 'b } 'Oid , { 'passive } 'Status ] , 
     'nbState [ { 'c } 'Oid , { 'c } 'Oid , { 'passive } 'Status ] ] ] , 
  'seqNos`:_ [ 
     'seqNos [ 
     'seqNo [ { 'a } 'Oid , { '1 } 'NzMachineInt ] , 
     'seqNo [ { 'b } 'Oid , { '0 } 'MachineInt ] , 
     'seqNo [ { 'c } 'Oid , { '0 } 'MachineInt ] ] ] ,  
  'parents`:_ [ 'parent [ { 'a } 'Oid , { 'a } 'Oid ] ] ,  
  'states`:_ [ 'states [  
     'state [ { 'a } 'Oid , { 'passive } 'Status ] ,  
     'state [ { 'b } 'Oid , { 'passive } 'Status ] ,  
     'state [ { 'c } 'Oid , { 'passive } 'Status ] ] ] ] ] ,  

'<_:_|_> [ 
  { 'b } 'Oid , { 'Node } 'Node , '_`,_ [  
  'nbs`:_ [ 'nbs [ { 'a } 'Oid , { 'c } 'Oid ] ] , 
  'nbsStates`:_ [ 'nbsStates [  
     'nbState [ { 'a } 'Oid , { 'a } 'Oid , { 'passive } 'Status ] ,  
     'nbState [ { 'a } 'Oid , { 'c } 'Oid , { 'passive } 'Status ] ,
     'nbState [ { 'b } 'Oid , { 'a } 'Oid , { 'passive } 'Status ] ,
     'nbState [ { 'b } 'Oid , { 'c } 'Oid , { 'passive } 'Status ] , 
     'nbState [ { 'c } 'Oid , { 'a } 'Oid , { 'passive } 'Status ] , 
     'nbState [ { 'c } 'Oid , { 'c } 'Oid , { 'passive } 'Status ] ] ] ,  
  'seqNos`:_ [ 
     'seqNos [ 
     'seqNo [ { 'a } 'Oid , { '1 } 'NzMachineInt ] , 
     'seqNo [ { 'b } 'Oid , { '0 } 'MachineInt ] , 
     'seqNo [ { 'c } 'Oid , { '0 } 'MachineInt ] ] ] ,  
  'parents`:_ [ 'parent [ { 'a } 'Oid , { 'c } 'Oid ] ] ,  
  'states`:_ [ 'states [  
     'state [ { 'a } 'Oid , { 'passive } 'Status ] ,  
     'state [ { 'b } 'Oid , { 'passive } 'Status ] ,  
     'state [ { 'c } 'Oid , { 'passive } 'Status ] ] ] ] ] ,  

'<_:_|_> [ 
  { 'c } 'Oid , { 'Node } 'Node , '_`,_ [  
  'nbs`:_ [ 'nbs [ { 'a } 'Oid , { 'b } 'Oid ] ] , 
  'nbsStates`:_ [ 'nbsStates [  
     'nbState [ { 'a } 'Oid , { 'a } 'Oid , { 'passive } 'Status ] ,  
     'nbState [ { 'a } 'Oid , { 'b } 'Oid , { 'passive } 'Status ] ,
     'nbState [ { 'b } 'Oid , { 'a } 'Oid , { 'passive } 'Status ] ,
     'nbState [ { 'b } 'Oid , { 'b } 'Oid , { 'passive } 'Status ] , 
     'nbState [ { 'c } 'Oid , { 'a } 'Oid , { 'passive } 'Status ] , 
     'nbState [ { 'c } 'Oid , { 'a } 'Oid , { 'passive } 'Status ] ] ] ,  
  'seqNos`:_ [ 
     'seqNos [ 
     'seqNo [ { 'a } 'Oid , { '1 } 'NzMachineInt ] , 
     'seqNo [ { 'b } 'Oid , { '0 } 'MachineInt ] , 
     'seqNo [ { 'c } 'Oid , { '0 } 'MachineInt ] ] ] ,  
  'parents`:_ [ 'parent [ { 'a } 'Oid , { 'a } 'Oid ] ] ,  
  'states`:_ [ 'states [  
     'state [ { 'a } 'Oid , { 'passive } 'Status ] ,  
     'state [ { 'b } 'Oid , { 'passive } 'Status ] ,  
     'state [ { 'c } 'Oid , { 'passive } 'Status  ] ] ] ] ] ] )
 
    
	

*** 
*** Exhaustive Search / TEST: New Link  (~0:38min on Linux, 450Mhz, PII)
***

Maude> (red irreducibleforms ( RBP , { 'test2 } 'Configuration , alldynamicrules ) .) 

Reduce in METATEST : irreducibleforms ( RBP , { 'test2 } 'Configuration ,
    alldynamicrules ) . 
Result Term : 
'__ [ 
'<_:_|_> [ 
  { 'b } 'Oid , { 'Node } 'Node , '_`,_ [ 
  'nbs`:_ [ 'nbs [ { 'a } 'Oid , { 'c } 'Oid ] ] , 
  'nbsStates`:_ [ 'nbsStates [
      'nbState [ { 'a } 'Oid , { 'a } 'Oid , { 'passive } 'Status ] , 
      'nbState [ { 'a } 'Oid , { 'c } 'Oid , { 'passive } 'Status ] , 
      'nbState [ { 'b } 'Oid , { 'a } 'Oid , { 'passive } 'Status ] , 
      'nbState [ { 'b } 'Oid , { 'c } 'Oid , { 'passive } 'Status ] , 
      'nbState [ { 'c } 'Oid , { 'a } 'Oid , { 'passive } 'Status ] , 
      'nbState [ { 'c } 'Oid , { 'c } 'Oid , { 'passive } 'Status ] ] ]  
  'seqNos`:_ [ 'seqNos [ 
      'seqNo [ { 'a } 'Oid , { '0 } 'MachineInt ] , 
      'seqNo [ { 'b } 'Oid , { '0 } 'MachineInt ] , 
      'seqNo [ { 'c } 'Oid , { '0 } 'MachineInt ] ] ] , 
  'parents`:_ [ { 'mtparents } 'IdIdPFun ] , 
  'states`:_ [ 'states [ 
      'state [ { 'a } 'Oid , { 'passive } 'Status ] ,
      'state [ { 'b } 'Oid , { 'passive } 'Status ] , 
      'state [ { 'c } 'Oid , { 'passive } 'Status ] ] ] ] ] , 

'<_:_|_> [ 
  { 'c } 'Oid , { 'Node } 'Node , '_`,_ [ 
  'nbs`:_ [ 'nbs [ { 'a } 'Oid , { 'b } 'Oid ] ] , 
  'nbsStates`:_ [ 'nbsStates [ 
      'nbState [ { 'a } 'Oid , { 'a } 'Oid , { 'passive } 'Status ] ,
      'nbState [ { 'a } 'Oid , { 'b } 'Oid , { 'passive } 'Status ] , 
      'nbState [ { 'b } 'Oid , { 'a } 'Oid , { 'passive } 'Status ] , 
      'nbState [ { 'b } 'Oid , { 'b } 'Oid , { 'passive } 'Status ] , 
      'nbState [ { 'c } 'Oid , { 'a } 'Oid , { 'passive } 'Status ] , 
      'nbState [ { 'c } 'Oid , { 'b } 'Oid , { 'passive } 'Status ] ] ] , 
  'seqNos`:_ [ 'seqNos [ 
      'seqNo [ { 'a } 'Oid , { '0 } 'MachineInt ] , 
      'seqNo [ { 'b } 'Oid , { '0 } 'MachineInt ] , 
      'seqNo [ { 'c } 'Oid , { '0 } 'MachineInt ] ] ] ,
  'parents`:_ [ { 'mtparents } 'IdIdPFun ] , 
  'states`:_ [ 'states [ 
      'state [ { 'a } 'Oid , { 'passive } 'Status ] , 
      'state [ { 'b } 'Oid , { 'passive } 'Status ] , 
      'state [ { 'c } 'Oid , { 'passive } 'Status ] ] ] ] ] ]

      
*** Since only one term is the result, this term can be pretty-printed
Maude> (down RBP : red irreducibleforms ( RBP , { 'test2 } 'Configuration , alldynamicrules ) .) 

Result Configuration : 
< b : Node | nbs : nbs ( a , c ) ,
             nbsStates : nbsStates ( nbState ( a , a , passive ) , 
	                             nbState ( a , c , passive ) ,
				     nbState ( b , a , passive ) ,
				     nbState ( b , c , passive ) ,
				     nbState ( c , a , passive ) , 
				     nbState ( c , c , passive ) ) , 
	     seqNos : seqNos ( seqNo ( a , 0 ) , 
	                       seqNo ( b , 0 ) , 
			       seqNo ( c , 0 ) ) , 
             parents : mtparents ,
	     states : states ( state ( a , passive ) , 
	                       state ( b , passive ) , 
			       state ( c , passive ) ) > 
< c : Node | nbs : nbs ( a , b ) , 
             nbsStates : nbsStates ( nbState ( a , a , passive ) , 
	                             nbState ( a , b , passive ) , 
				     nbState ( b , a , passive ) , 
				     nbState ( b , b , passive ) ,
				     nbState ( c , a , passive ) , 
				     nbState ( c , b , passive ) ) , 
             seqNos : seqNos ( seqNo ( a , 0 ) , 
	                       seqNo ( b , 0 ) , 
			       seqNo ( c , 0 ) ) , 
             parents : mtparents , 
	     states : states ( state ( a , passive ) , 
	                       state ( b , passive ) ,
			       state ( c , passive ) ) >

    
   
*** 
*** Exhaustive Search / TEST: Failure of Link (~56:27min Linux, 450Mhz, PII) 
***
Maude>  (red irreducibleforms ( RBP , { 'test3 } 'Configuration , alldynamicrules ) .) 
  
  
Reduce in METATEST : irreducibleforms ( RBP , { 'test3 } 'Configuration ,
    alldynamicrules ) . 
Result TermSet : 
set ( '__ [ 
'<_:_|_> [ 
  { 'a } 'Oid , { 'Node } 'Node , '_`,_ [ 
  'nbs`:_ [ { 'mtnbs } 'OidSet ] , 
  'nbsStates`:_ [ { 'mtnbsStates } 'IdIdStatusPFun ] , 
  'seqNos`:_ [ 'seqNos [ 
     'seqNo [ { 'a } 'Oid , { '0 } 'MachineInt ] ,  
     'seqNo [ { 'b } 'Oid , { '0 } 'MachineInt ] ] ] , 
  'parents`:_ [ { 'mtparents } 'IdIdPFun ] ,
  'states`:_ [ 'states [ 
     'state [ { 'a } 'Oid , { 'passive } 'Status ] ,  
     'state [ { 'b } 'Oid , { 'passive } 'Status ] ] ] ] ] , 

'<_:_|_> [ 
  { 'b } 'Oid , { 'Node } 'Node , '_`,_ [  
  'nbs`:_ [ { 'c } 'Oid ] ,  
  'nbsStates`:_ [ 'nbsStates [ 
     'nbState [ { 'b } 'Oid , { 'c } 'Oid , { 'passive } 'Status ] ,  
     'nbState [ { 'a } 'Oid , { 'c } 'Oid , { 'passive } 'Status ] ,  
     'nbState [ { 'c } 'Oid , { 'c } 'Oid , { 'passive } 'Status ] ] ] , 
  'seqNos`:_ [ 'seqNos [  
     'seqNo [ { 'a } 'Oid , { '0 } 'MachineInt ] ,  
     'seqNo [ { 'b } 'Oid , { '0 } 'MachineInt ] ,  
     'seqNo [ { 'c } 'Oid , { '0 } 'MachineInt ] ] ] , 
  'parents`:_ [ { 'mtparents } 'IdIdPFun ] , 
  'states`:_ [ 'states [  
     'state [ { 'a } 'Oid , { 'passive } 'Status ] ,  
     'state [ { 'b } 'Oid , { 'passive } 'Status ] ,  
     'state [ { 'c } 'Oid , { 'passive } 'Status ] ] ] ] ] , 

'<_:_|_> [ 
  { 'c } 'Oid , { 'Node } 'Node , '_`,_ [  
  'nbs`:_ [ { 'b } 'Oid ] ,  
  'nbsStates`:_ [ 'nbsStates [  
     'nbState [ { 'b } 'Oid , { 'b } 'Oid , { 'passive } 'Status ] ,  
     'nbState [ { 'c } 'Oid , { 'b } 'Oid , { 'passive } 'Status ] ] ] , 
  'seqNos`:_ [ 'seqNos [  
     'seqNo [ { 'b } 'Oid , { '0 } 'MachineInt ] ,  
     'seqNo [ { 'c } 'Oid , { '0 } 'MachineInt ] ] ] ,
  'parents`:_ [ { 'mtparents } 'IdIdPFun ] , 
  'states`:_ [ 'states [  
     'state [ { 'b } 'Oid , { 'passive } 'Status ] ,  
     'state [ { 'c } 'Oid , { 'passive } 'Status ] ] ] ] ] ] , 

'__ [ 
'<_:_|_> [  
  { 'a } 'Oid , { 'Node } 'Node , '_`,_ [  
  'nbs`:_ [ { 'mtnbs } 'OidSet ] ,  
  'nbsStates`:_ [ { 'mtnbsStates } 'IdIdStatusPFun ] , 
  'seqNos`:_ [ 'seqNos [  
     'seqNo [ { 'a } 'Oid , { '1 } 'NzMachineInt ] ,  
     'seqNo [ { 'b } 'Oid , { '0 } 'MachineInt ] ] ] , 
  'parents`:_ [ 'parent [ { 'a } 'Oid , { 'a } 'Oid ] ] , 
  'states`:_ [ 'states [  
     'state [ { 'a } 'Oid , { 'passive } 'Status ] ,  
     'state [ { 'b } 'Oid , { 'passive } 'Status ] ] ] ] ] , 

'<_:_|_> [  
  { 'b } 'Oid , { 'Node } 'Node , '_`,_ [  
  'nbs`:_ [ { 'c } 'Oid ] ,  
  'nbsStates`:_ [ 'nbsStates [  
     'nbState [ { 'a } 'Oid , { 'c } 'Oid , { 'passive } 'Status ] ,  
     'nbState [ { 'b } 'Oid , { 'c } 'Oid , { 'passive } 'Status ] ,  
     'nbState [ { 'c } 'Oid , { 'c } 'Oid , { 'passive } 'Status ] ] ] , 
  'seqNos`:_ [ 'seqNos [  
     'seqNo [ { 'a } 'Oid , { '1 } 'NzMachineInt ] ,  
     'seqNo [ { 'b } 'Oid , { '0 } 'MachineInt ] ,  
     'seqNo [ { 'c } 'Oid , { '0 } 'MachineInt ] ] ] , 
  'parents`:_ [ { 'mtparents } 'IdIdPFun ] , 
  'states`:_ [ 'states [  
     'state [ { 'a } 'Oid , { 'passive } 'Status ] ,  
     'state [ { 'b } 'Oid , { 'passive } 'Status ] ,  
     'state [ { 'c } 'Oid , { 'passive } 'Status ] ] ] ] ] , 

'<_:_|_> [  
  { 'c } 'Oid , { 'Node } 'Node , '_`,_ [  
  'nbs`:_ [ { 'b } 'Oid ] ,  
  'nbsStates`:_ [ 'nbsStates [  
     'nbState [ { 'a } 'Oid , { 'b } 'Oid , { 'passive } 'Status ] ,  
     'nbState [ { 'b } 'Oid , { 'b } 'Oid , { 'passive } 'Status ] ,  
     'nbState [ { 'c } 'Oid , { 'b } 'Oid , { 'passive } 'Status ] ] ] , 
  'seqNos`:_ [ 'seqNos [  
     'seqNo [ { 'a } 'Oid , { '1 } 'NzMachineInt ] ,  
     'seqNo [ { 'b } 'Oid , { '0 } 'MachineInt ] ,  
     'seqNo [ { 'c } 'Oid , { '0 } 'MachineInt ] ] ] , 
  'parents`:_ [ 'parent [ { 'a } 'Oid , { 'b } 'Oid ] ] , 
  'states`:_ [ 'states [  
     'state [ { 'a } 'Oid , { 'passive } 'Status ] ,  
     'state [ { 'b } 'Oid , { 'passive } 'Status ] ,  
     'state [ { 'c } 'Oid , { 'passive } 'Status ] ] ] ] ] ] , 

'__ [ 
'<_:_|_> [  
  { 'a } 'Oid , { 'Node } 'Node , '_`,_ [  
  'nbs`:_ [ { 'mtnbs } 'OidSet ] ,  
  'nbsStates`:_ [ { 'mtnbsStates } 'IdIdStatusPFun ] , 
  'seqNos`:_ [ 'seqNos [  
     'seqNo [ { 'a } 'Oid , { '1 } 'NzMachineInt ] ,  
     'seqNo [ { 'b } 'Oid , { '0 } 'MachineInt ] ] ] , 
  'parents`:_ [ { 'mtparents } 'IdIdPFun ] , 
  'states`:_ [ 'states [  
     'state [ { 'a } 'Oid , { 'passive } 'Status ] ,  
     'state [ { 'b } 'Oid , { 'passive } 'Status ] ] ] ] ] , 

'<_:_|_> [  
  { 'b } 'Oid , { 'Node }    'Node , '_`,_ [  
  'nbs`:_ [ { 'c } 'Oid ] ,  
  'nbsStates`:_ [ 'nbsStates [  
     'nbState [ { 'a } 'Oid , { 'c } 'Oid , { 'passive } 'Status ] ,  
     'nbState [ { 'b } 'Oid , { 'c } 'Oid , { 'passive } 'Status ] ,  
     'nbState [ { 'c } 'Oid , { 'c } 'Oid , { 'passive } 'Status ] ] ] , 
  'seqNos`:_ [ 'seqNos [  
     'seqNo [ { 'a } 'Oid , { '0 } 'MachineInt ] ,  
     'seqNo [ { 'b } 'Oid , { '0 } 'MachineInt ] ,  
     'seqNo [ { 'c } 'Oid , { '0 } 'MachineInt ] ] ] , 
  'parents`:_ [ { 'mtparents } 'IdIdPFun ] , 
  'states`:_ [ 'states [  
     'state [ { 'a } 'Oid , { 'passive } 'Status ] ,  
     'state [ { 'b } 'Oid , { 'passive } 'Status ] ,  
     'state [ { 'c } 'Oid , { 'passive } 'Status ] ] ] ] ] , 

'<_:_|_> [  
  { 'c } 'Oid , { 'Node } 'Node , '_`,_ [  
  'nbs`:_ [ { 'b } 'Oid ] ,  
  'nbsStates`:_ [ 'nbsStates [  
     'nbState [ { 'b } 'Oid , { 'b } 'Oid , { 'passive } 'Status ] ,  
     'nbState [ { 'c } 'Oid , { 'b } 'Oid , { 'passive } 'Status ] ] ] , 
  'seqNos`:_ [ 'seqNos [  
     'seqNo [ { 'b } 'Oid , { '0 } 'MachineInt ] ,  
     'seqNo [ { 'c } 'Oid , { '0 } 'MachineInt ] ] ] , 
  'parents`:_ [ { 'mtparents } 'IdIdPFun ] , 
  'states`:_ [ 'states [  
     'state [ { 'b } 'Oid , { 'passive } 'Status ] ,  
     'state [ { 'c } 'Oid , { 'passive } 'Status ] ] ] ] ] ] , 

'__ [ 
'<_:_|_> [  
  { 'a } 'Oid , { 'Node } 'Node , '_`,_ [  
  'nbs`:_ [ { 'mtnbs } 'OidSet ] ,  
  'nbsStates`:_ [ { 'mtnbsStates } 'IdIdStatusPFun ] , 
  'seqNos`:_ [ 'seqNos [  
     'seqNo [ { 'a } 'Oid , { '1 } 'NzMachineInt ] ,  
     'seqNo [ { 'b } 'Oid , { '0 } 'MachineInt ] ] ] , 
  'parents`:_ [ { 'mtparents } 'IdIdPFun ] , 
  'states`:_ [ 'states [  
     'state [ { 'a } 'Oid , { 'passive } 'Status ] ,  
     'state [ { 'b } 'Oid , { 'passive } 'Status ] ] ] ] ] , 

'<_:_|_> [  
  { 'b } 'Oid , { 'Node } 'Node , '_`,_ [  
  'nbs`:_ [ { 'c } 'Oid ] ,  
  'nbsStates`:_ [ 'nbsStates [  
     'nbState [ { 'a } 'Oid , { 'c } 'Oid , { 'passive } 'Status ] ,  
     'nbState [ { 'b } 'Oid , { 'c } 'Oid , { 'passive } 'Status ] ,  
     'nbState [ { 'c } 'Oid , { 'c } 'Oid , { 'passive } 'Status ] ] ] , 
  'seqNos`:_ [ 'seqNos [  
     'seqNo [ { 'a } 'Oid , { '1 } 'NzMachineInt ] ,  
     'seqNo [ { 'b } 'Oid , { '0 } 'MachineInt ] ,  
     'seqNo [ { 'c } 'Oid , { '0 } 'MachineInt ] ] ] , 
  'parents`:_ [ { 'mtparents } 'IdIdPFun ] , 
  'states`:_ [ 'states [  
     'state [ { 'a } 'Oid , { 'passive } 'Status ] ,  
     'state [ { 'b } 'Oid , { 'passive } 'Status ] ,  
     'state [ { 'c } 'Oid , { 'passive } 'Status ] ] ] ] ] , 

'<_:_|_> [  
  { 'c } 'Oid , { 'Node } 'Node , '_`,_ [  
  'nbs`:_ [ { 'b } 'Oid ] ,  
  'nbsStates`:_ [ 'nbsStates [  
     'nbState [ { 'a } 'Oid , { 'b } 'Oid , { 'passive } 'Status ] ,  
     'nbState [ { 'b } 'Oid , { 'b } 'Oid , { 'passive } 'Status ] , 
     'nbState [ { 'c } 'Oid , { 'b } 'Oid , { 'passive } 'Status ] ] ] , 
  'seqNos`:_ [ 'seqNos [  
     'seqNo [ { 'a } 'Oid , { '1 } 'NzMachineInt ] ,  
     'seqNo [ { 'b } 'Oid , { '0 } 'MachineInt ] ,  
     'seqNo [ { 'c } 'Oid , { '0 } 'MachineInt ] ] ] , 
  'parents`:_ [ 'parent [ { 'a } 'Oid , { 'b } 'Oid ] ] , 
  'states`:_ [ 'states [  
     'state [ { 'a } 'Oid , { 'passive } 'Status ] ,  
     'state [ { 'b } 'Oid , { 'passive } 'Status ] ,  
     'state [ { 'c } 'Oid , { 'passive } 'Status ] ] ] ] ] ] )

  
*** 
*** Execution of object-level term at meta-level
***		

Maude> (down RBP : red meta-reduce(RBP,{'test1}'Configuration) .)

*** This gives the same result as executing Maude> (rew test1 .)
*** after only introducing rbpDynamic.maude!

Result Configuration :
< a : Node | nbs : nbs ( b , c ) , 
             nbsstates : nbsStates ( nbState( a , b , passive ) , 
                                     nbState( a , c , passive ) ) ,  
             seqNos : seqNos( seqNo ( a , 1 ) , 
                              seqNo ( b , 0 ) ,  
                              seqNo ( c , 0 ) ) ,  
             parents : parent( a , a ) ,			    
             states : states( state( a , passive ) , 
                              state( b , passive ) ,  
                              state( c , passive ) ) >  


< b : Node | nbs : nbs ( a , c ) , 
             nbsstates : nbsStates ( nbstate ( a , a , passive ) ,  
                                     nbstate ( a , c , passive ) ) ,  
             seqNos : seqNos ( seqNo ( a , 1 ) ,  
                               seqNo ( b , 0 ) ,  
                               seqNo ( c , 0 ) ) , 
             parents : parent (a , a ) ,
             states : states ( state ( a , passive ) ,  
                               state ( b , passive ) ,  
                               state ( c , passive ) ) >

< c : Node | nbs : nbs ( a , b ) , 
             nbsstates : nbsStates ( nbstate ( a , a , passive ) ,  
                                     nbstate ( a , b , passive ) ) ,  
             seqNos : seqNos ( seqNo ( a , 1 ) ,  
                               seqNo ( b , 0 ) ,  
                               seqNo ( c , 0 ) ) , 
             parents : parent ( a , a ) , 
             states : states ( state ( a , passive ) ,  
                               state ( b , passive ) ,  
                               state ( c , passive ) ) >