Santiago:prototype-20111114 santiago$ examples/nsl-command 
Mon Nov 14 00:12:59 CET 2011
		     \||||||||||||||||||/
		   --- Welcome to Maude ---
		     /||||||||||||||||||\
	    Maude 2.6 built: Dec 10 2010 11:12:39
	    Copyright 1997-2010 SRI International
		   Mon Nov 14 00:12:59 2011
Maude> 
	    Maude-NPA Version: 11/14/2011
	    Copyright (c) 2011, University of Illinois
	    All rights reserved.

==========================================
reduce in MAUDE-NPA : genGrammars .
rewrites: 7974742 in 25966ms cpu (27044ms real) (307113 rewrites/second)
result GrammarList: (
grl #0:Msg inL => pk(#1:Name, #0:Msg) inL . ; 
grl #0:Msg inL => sk(#1:Key, #0:Msg) inL . ; 
grl #0:Msg inL => (#0:Msg ; #1:Msg) inL . ; 
grl #0:Msg inL => (#1:Msg ; #0:Msg) inL . ; 
grl #0:Msg notInI, #0:Msg notLeq n(#1:Name, #2:Fresh) => (#0:Msg ; #3:Msg) inL . ; 
grl #0:Msg notInI, #0:Msg notLeq n(#1:Name, #2:Fresh) => (#3:Name ; #0:Msg) inL .)
| (
grl #0:Msg inL => pk(#1:Name, #0:Msg) inL . ; 
grl #0:Msg inL => sk(#1:Key, #0:Msg) inL . ; 
grl #0:Msg inL => (#0:Msg ; #1:Msg) inL . ; 
grl #0:Msg inL => (#1:Msg ; #0:Msg) inL . ; 
grl #0:Msg notInI, (#0:Msg notLeq n(#1:Name, #2:Fresh)), #0:Msg notLeq n(#3:Name, #4:Fresh) ; #3:Name => (#5:Msg ; #0:Msg) inL .)
| (errorNoHeuristicApplied {
grl empty => (#1:Msg ; #2:Msg) inL .,none,
grl empty => (#1:Msg,#2:Msg) inL .,none,
grl empty => (#1:Msg,#2:Msg) inL .} usingGrammar 
grl empty => (#1:Msg ; #2:Msg) inL .)
| (errorInconsistentExceptionsInGrammarRule 
grl n(#0:Name, #1:Fresh) notLeq #1:Nonce => n(#0:Name, #1:Fresh) inL . inGrammar 
grl #0:Msg inL => sk(#1:Key, #0:Msg) inL . ; 
grl #0:Msg inL => (#0:Msg ; #1:Msg) inL . ; 
grl #0:Msg inL => (#1:Msg ; #0:Msg) inL . ; 
grl #5:Msg inL => pk(#3:Name, #5:Msg) inL . ; 
grl n(#0:Name, #1:Fresh) notLeq #1:Nonce => n(#0:Name, #1:Fresh) inL .)
| (errorNoHeuristicApplied {
grl #50:Key notInI => pk(#50:Key, #60:Msg) inL .,none,
grl #50:Key notInI => #60:Msg inL .,none,
grl #50:Key notInI => #60:Msg inL .} usingGrammar 
grl #50:Key notInI => pk(#50:Key, #60:Msg) inL .)
| (
grl #0:Msg inL => pk(#1:Name, #0:Msg) inL . ; 
grl #0:Msg inL => sk(#1:Key, #0:Msg) inL . ; 
grl #0:Msg inL => (#0:Msg ; #1:Msg) inL . ; 
grl #0:Msg inL => (#1:Msg ; #0:Msg) inL . ; 
grl #0:Msg notInI, (#0:Msg notLeq #1:Nonce), (#0:Msg notLeq #2:Name ; n(#2:Name, #3:Fresh)), #0:Msg notLeq #4:Nonce ; n(#5:Name, #6:Fresh) ; #5:Name => pk(#7:Key, #0:Msg) inL .)
| (errorNoHeuristicApplied {
grl empty => pk(#1:Key, #2:Msg) inL .,none,
grl empty => #2:Msg inL .,none,
grl empty => #2:Msg inL .} usingGrammar 
grl empty => pk(#1:Key, #2:Msg) inL .)
| (
grl #0:Msg inL => pk(#1:Name, #0:Msg) inL . ; 
grl #0:Msg inL => sk(#1:Key, #0:Msg) inL . ; 
grl #0:Msg inL => (#0:Msg ; #1:Msg) inL . ; 
grl #0:Msg inL => (#1:Msg ; #0:Msg) inL . ; 
grl #0:Key notInI => sk(#0:Key, #1:Msg) inL .)
| (
grl #0:Msg inL => pk(#1:Name, #0:Msg) inL . ; 
grl #0:Msg inL => sk(#1:Key, #0:Msg) inL . ; 
grl #0:Msg inL => (#0:Msg ; #1:Msg) inL . ; 
grl #0:Msg inL => (#1:Msg ; #0:Msg) inL . ; 
grl #0:Msg notInI => sk(#1:Key, #0:Msg) inL .)
| 
grl #0:Msg inL => pk(#1:Name, #0:Msg) inL . ; 
grl #0:Msg inL => sk(#1:Key, #0:Msg) inL . ; 
grl #0:Msg inL => (#0:Msg ; #1:Msg) inL . ; 
grl #0:Msg inL => (#1:Msg ; #0:Msg) inL . ; 
grl sk(#0:Key, #1:Msg) notLeq sk(i, #2:Msg) => sk(#0:Key, #1:Msg) inL .
==========================================
reduce in MAUDE-NPA : run(0) .
rewrites: 2501 in 52ms cpu (55ms real) (48039 rewrites/second)
result IdSystem: < 1 > 
:: r:Fresh ::
[ nil, 
   -(pk(b, a ; N:Nonce)), 
   +(pk(a, N:Nonce ; n(b, r:Fresh) ; b)), 
   -(pk(b, n(b, r:Fresh))) | nil] 
|| 
n(b, r:Fresh) inI
|| 
nil
|| 
nil
|| 
nil
==========================================
reduce in MAUDE-NPA : summary(1) .
rewrites: 868779 in 2305ms cpu (2389ms real) (376863 rewrites/second)
result Summary: States>> 4 Solutions>> 0
==========================================
reduce in MAUDE-NPA : summary(2) .
rewrites: 1780642 in 4593ms cpu (4811ms real) (387659 rewrites/second)
result Summary: States>> 7 Solutions>> 0
==========================================
reduce in MAUDE-NPA : summary(3) .
rewrites: 3269313 in 8778ms cpu (9132ms real) (372441 rewrites/second)
result Summary: States>> 6 Solutions>> 0
==========================================
reduce in MAUDE-NPA : summary(4) .
rewrites: 2636183 in 7251ms cpu (7544ms real) (363558 rewrites/second)
result Summary: States>> 2 Solutions>> 0
==========================================
reduce in MAUDE-NPA : summary(5) .
rewrites: 642339 in 1901ms cpu (1981ms real) (337834 rewrites/second)
result Summary: States>> 0 Solutions>> 0
==========================================
reduce in MAUDE-NPA : run(1) .
rewrites: 18 in 0ms cpu (0ms real) (18000000 rewrites/second)
result IdSystemSet: (< 1 . 2 > (
:: nil ::
[ nil | 
   -(pk(i, n(b, #0:Fresh))), 
   +(n(b, #0:Fresh)), nil]  & 
:: #0:Fresh ::
[ nil, 
   -(pk(b, a ; #1:Nonce)), 
   +(pk(a, #1:Nonce ; n(b, #0:Fresh) ; b)) | 
   -(pk(b, n(b, #0:Fresh))), nil] )
|| 
n(b, #0:Fresh) !inI,
pk(b, n(b, #0:Fresh)) inI,
pk(i, n(b, #0:Fresh)) inI
|| 
-(pk(i, n(b, #0:Fresh))), 
+(n(b, #0:Fresh)), 
-(pk(b, n(b, #0:Fresh)))
|| 
nil
|| 
nil)
(< 1 . 5 > (
:: nil ::
[ nil | 
   -(n(b, #0:Fresh)), 
   +(pk(b, n(b, #0:Fresh))), nil]  & 
:: #0:Fresh ::
[ nil, 
   -(pk(b, a ; #1:Nonce)), 
   +(pk(a, #1:Nonce ; n(b, #0:Fresh) ; b)) | 
   -(pk(b, n(b, #0:Fresh))), nil] )
|| 
pk(b, n(b, #0:Fresh)) !inI,
n(b, #0:Fresh) inI
|| 
-(n(b, #0:Fresh)), 
+(pk(b, n(b, #0:Fresh))), 
-(pk(b, n(b, #0:Fresh)))
|| 
nil
|| 
nil)
(< 1 . 7 > (
:: nil ::
[ nil | 
   -(#0:Msg ; n(b, #1:Fresh)), 
   +(n(b, #1:Fresh)), nil]  & 
:: #1:Fresh ::
[ nil, 
   -(pk(b, a ; #2:Nonce)), 
   +(pk(a, #2:Nonce ; n(b, #1:Fresh) ; b)) | 
   -(pk(b, n(b, #1:Fresh))), nil] )
|| 
n(b, #1:Fresh) !inI,
pk(b, n(b, #1:Fresh)) inI,
(#0:Msg ; n(b, #1:Fresh)) inI
|| 
-(#0:Msg ; n(b, #1:Fresh)), 
+(n(b, #1:Fresh)), 
-(pk(b, n(b, #1:Fresh)))
|| 
nil
|| 
nil)
< 1 . 9 > (
:: nil ::
[ nil | 
   -(n(b, #0:Fresh) ; #1:Msg), 
   +(n(b, #0:Fresh)), nil]  & 
:: #0:Fresh ::
[ nil, 
   -(pk(b, a ; #2:Nonce)), 
   +(pk(a, #2:Nonce ; n(b, #0:Fresh) ; b)) | 
   -(pk(b, n(b, #0:Fresh))), nil] )
|| 
n(b, #0:Fresh) !inI,
pk(b, n(b, #0:Fresh)) inI,
(n(b, #0:Fresh) ; #1:Msg) inI
|| 
-(n(b, #0:Fresh) ; #1:Msg), 
+(n(b, #0:Fresh)), 
-(pk(b, n(b, #0:Fresh)))
|| 
nil
|| 
nil
==========================================
reduce in MAUDE-NPA : run(2) .
rewrites: 18 in 0ms cpu (0ms real) (18000000 rewrites/second)
result IdSystemSet: (< 1 . 2 . 9 > (
:: nil ::
[ nil | 
   -(pk(i, n(b, #0:Fresh))), 
   +(n(b, #0:Fresh)), nil]  & 
:: #0:Fresh ::
[ nil, 
   -(pk(b, a ; #1:Nonce)), 
   +(pk(a, #1:Nonce ; n(b, #0:Fresh) ; b)) | 
   -(pk(b, n(b, #0:Fresh))), nil]  & 
:: #2:Fresh ::
[ nil, 
   +(pk(i, #3:Name ; n(#3:Name, #2:Fresh))) | 
   -(pk(#3:Name, n(#3:Name, #2:Fresh) ; n(b, #0:Fresh) ; i)), 
   +(pk(i, n(b, #0:Fresh))), nil] )
|| 
pk(i, n(b, #0:Fresh)) !inI,
n(b, #0:Fresh) !inI,
pk(b, n(b, #0:Fresh)) inI,
pk(#3:Name, n(#3:Name, #2:Fresh) ; n(b, #0:Fresh) ; i) inI
|| 
-(pk(#3:Name, n(#3:Name, #2:Fresh) ; n(b, #0:Fresh) ; i)), 
+(pk(i, n(b, #0:Fresh))), 
-(pk(i, n(b, #0:Fresh))), 
+(n(b, #0:Fresh)), 
-(pk(b, n(b, #0:Fresh)))
|| 
nil
|| 
nil)
(< 1 . 5 . 2 > (
:: nil ::
[ nil | 
   -(pk(i, n(b, #0:Fresh))), 
   +(n(b, #0:Fresh)), nil]  & 
:: nil ::
[ nil | 
   -(n(b, #0:Fresh)), 
   +(pk(b, n(b, #0:Fresh))), nil]  & 
:: #0:Fresh ::
[ nil, 
   -(pk(b, a ; #1:Nonce)), 
   +(pk(a, #1:Nonce ; n(b, #0:Fresh) ; b)) | 
   -(pk(b, n(b, #0:Fresh))), nil] )
|| 
pk(b, n(b, #0:Fresh)) !inI,
n(b, #0:Fresh) !inI,
pk(i, n(b, #0:Fresh)) inI
|| 
-(pk(i, n(b, #0:Fresh))), 
+(n(b, #0:Fresh)), 
-(n(b, #0:Fresh)), 
+(pk(b, n(b, #0:Fresh))), 
-(pk(b, n(b, #0:Fresh)))
|| 
nil
|| 
nil)
(< 1 . 5 . 4 > (
:: nil ::
[ nil | 
   -(n(b, #0:Fresh)), 
   +(pk(b, n(b, #0:Fresh))), nil]  & 
:: nil ::
[ nil | 
   -(n(b, #0:Fresh) ; #1:Msg), 
   +(n(b, #0:Fresh)), nil]  & 
:: #0:Fresh ::
[ nil, 
   -(pk(b, a ; #2:Nonce)), 
   +(pk(a, #2:Nonce ; n(b, #0:Fresh) ; b)) | 
   -(pk(b, n(b, #0:Fresh))), nil] )
|| 
pk(b, n(b, #0:Fresh)) !inI,
n(b, #0:Fresh) !inI,
(n(b, #0:Fresh) ; #1:Msg) inI
|| 
-(n(b, #0:Fresh) ; #1:Msg), 
+(n(b, #0:Fresh)), 
-(n(b, #0:Fresh)), 
+(pk(b, n(b, #0:Fresh))), 
-(pk(b, n(b, #0:Fresh)))
|| 
nil
|| 
nil)
(< 1 . 5 . 5 > (
:: nil ::
[ nil | 
   -(n(b, #1:Fresh)), 
   +(pk(b, n(b, #1:Fresh))), nil]  & 
:: nil ::
[ nil | 
   -(#0:Msg ; n(b, #1:Fresh)), 
   +(n(b, #1:Fresh)), nil]  & 
:: #1:Fresh ::
[ nil, 
   -(pk(b, a ; #2:Nonce)), 
   +(pk(a, #2:Nonce ; n(b, #1:Fresh) ; b)) | 
   -(pk(b, n(b, #1:Fresh))), nil] )
|| 
pk(b, n(b, #1:Fresh)) !inI,
n(b, #1:Fresh) !inI,
(#0:Msg ; n(b, #1:Fresh)) inI
|| 
-(#0:Msg ; n(b, #1:Fresh)), 
+(n(b, #1:Fresh)), 
-(n(b, #1:Fresh)), 
+(pk(b, n(b, #1:Fresh))), 
-(pk(b, n(b, #1:Fresh)))
|| 
nil
|| 
nil)
(< 1 . 7 . 4 > (
:: nil ::
[ nil | 
   -(pk(i, #0:Msg ; n(b, #1:Fresh))), 
   +(#0:Msg ; n(b, #1:Fresh)), nil]  & 
:: nil ::
[ nil | 
   -(#0:Msg ; n(b, #1:Fresh)), 
   +(n(b, #1:Fresh)), nil]  & 
:: #1:Fresh ::
[ nil, 
   -(pk(b, a ; #2:Nonce)), 
   +(pk(a, #2:Nonce ; n(b, #1:Fresh) ; b)) | 
   -(pk(b, n(b, #1:Fresh))), nil] )
|| 
n(b, #1:Fresh) !inI,
(#0:Msg ; n(b, #1:Fresh)) !inI,
pk(b, n(b, #1:Fresh)) inI,
pk(i, #0:Msg ; n(b, #1:Fresh)) inI
|| 
-(pk(i, #0:Msg ; n(b, #1:Fresh))), 
+(#0:Msg ; n(b, #1:Fresh)), 
-(#0:Msg ; n(b, #1:Fresh)), 
+(n(b, #1:Fresh)), 
-(pk(b, n(b, #1:Fresh)))
|| 
nil
|| 
nil)
(< 1 . 9 . 3 > (
:: nil ::
[ nil | 
   -(pk(i, n(b, #0:Fresh) ; #1:Msg)), 
   +(n(b, #0:Fresh) ; #1:Msg), nil]  & 
:: nil ::
[ nil | 
   -(n(b, #0:Fresh) ; #1:Msg), 
   +(n(b, #0:Fresh)), nil]  & 
:: #0:Fresh ::
[ nil, 
   -(pk(b, a ; #2:Nonce)), 
   +(pk(a, #2:Nonce ; n(b, #0:Fresh) ; b)) | 
   -(pk(b, n(b, #0:Fresh))), nil] )
|| 
n(b, #0:Fresh) !inI,
(n(b, #0:Fresh) ; #1:Msg) !inI,
pk(b, n(b, #0:Fresh)) inI,
pk(i, n(b, #0:Fresh) ; #1:Msg) inI
|| 
-(pk(i, n(b, #0:Fresh) ; #1:Msg)), 
+(n(b, #0:Fresh) ; #1:Msg), 
-(n(b, #0:Fresh) ; #1:Msg), 
+(n(b, #0:Fresh)), 
-(pk(b, n(b, #0:Fresh)))
|| 
nil
|| 
nil)
< 1 . 9 . 9 > (
:: nil ::
[ nil | 
   -(#0:Msg ; n(b, #1:Fresh) ; #2:Msg), 
   +(n(b, #1:Fresh) ; #2:Msg), nil]  & 
:: nil ::
[ nil | 
   -(n(b, #1:Fresh) ; #2:Msg), 
   +(n(b, #1:Fresh)), nil]  & 
:: #1:Fresh ::
[ nil, 
   -(pk(b, a ; #3:Nonce)), 
   +(pk(a, #3:Nonce ; n(b, #1:Fresh) ; b)) | 
   -(pk(b, n(b, #1:Fresh))), nil] )
|| 
n(b, #1:Fresh) !inI,
(n(b, #1:Fresh) ; #2:Msg) !inI,
pk(b, n(b, #1:Fresh)) inI,
(#0:Msg ; n(b, #1:Fresh) ; #2:Msg) inI
|| 
-(#0:Msg ; n(b, #1:Fresh) ; #2:Msg), 
+(n(b, #1:Fresh) ; #2:Msg), 
-(n(b, #1:Fresh) ; #2:Msg), 
+(n(b, #1:Fresh)), 
-(pk(b, n(b, #1:Fresh)))
|| 
nil
|| 
nil
==========================================
reduce in MAUDE-NPA : run(3) .
rewrites: 18 in 0ms cpu (0ms real) (18000000 rewrites/second)
result IdSystemSet: (< 1 . 5 . 2 . 5 > (
:: nil ::
[ nil | 
   -(pk(i, n(b, #0:Fresh))), 
   +(n(b, #0:Fresh)), nil]  & 
:: nil ::
[ nil | 
   -(n(b, #0:Fresh)), 
   +(pk(b, n(b, #0:Fresh))), nil]  & 
:: #0:Fresh ::
[ nil, 
   -(pk(b, a ; #1:Nonce)), 
   +(pk(a, #1:Nonce ; n(b, #0:Fresh) ; b)) | 
   -(pk(b, n(b, #0:Fresh))), nil]  & 
:: #2:Fresh ::
[ nil, 
   +(pk(i, #3:Name ; n(#3:Name, #2:Fresh))) | 
   -(pk(#3:Name, n(#3:Name, #2:Fresh) ; n(b, #0:Fresh) ; i)), 
   +(pk(i, n(b, #0:Fresh))), nil] )
|| 
pk(b, n(b, #0:Fresh)) !inI,
pk(i, n(b, #0:Fresh)) !inI,
n(b, #0:Fresh) !inI,
pk(#3:Name, n(#3:Name, #2:Fresh) ; n(b, #0:Fresh) ; i) inI
|| 
-(pk(#3:Name, n(#3:Name, #2:Fresh) ; n(b, #0:Fresh) ; i)), 
+(pk(i, n(b, #0:Fresh))), 
-(pk(i, n(b, #0:Fresh))), 
+(n(b, #0:Fresh)), 
-(n(b, #0:Fresh)), 
+(pk(b, n(b, #0:Fresh))), 
-(pk(b, n(b, #0:Fresh)))
|| 
nil
|| 
nil)
(< 1 . 5 . 4 . 2 > (
:: nil ::
[ nil | 
   -(pk(i, n(b, #0:Fresh) ; #1:Msg)), 
   +(n(b, #0:Fresh) ; #1:Msg), nil]  & 
:: nil ::
[ nil | 
   -(n(b, #0:Fresh)), 
   +(pk(b, n(b, #0:Fresh))), nil]  & 
:: nil ::
[ nil | 
   -(n(b, #0:Fresh) ; #1:Msg), 
   +(n(b, #0:Fresh)), nil]  & 
:: #0:Fresh ::
[ nil, 
   -(pk(b, a ; #2:Nonce)), 
   +(pk(a, #2:Nonce ; n(b, #0:Fresh) ; b)) | 
   -(pk(b, n(b, #0:Fresh))), nil] )
|| 
pk(b, n(b, #0:Fresh)) !inI,
n(b, #0:Fresh) !inI,
(n(b, #0:Fresh) ; #1:Msg) !inI,
pk(i, n(b, #0:Fresh) ; #1:Msg) inI
|| 
-(pk(i, n(b, #0:Fresh) ; #1:Msg)), 
+(n(b, #0:Fresh) ; #1:Msg), 
-(n(b, #0:Fresh) ; #1:Msg), 
+(n(b, #0:Fresh)), 
-(n(b, #0:Fresh)), 
+(pk(b, n(b, #0:Fresh))), 
-(pk(b, n(b, #0:Fresh)))
|| 
nil
|| 
nil)
(< 1 . 5 . 4 . 6 > (
:: nil ::
[ nil | 
   -(n(b, #1:Fresh)), 
   +(pk(b, n(b, #1:Fresh))), nil]  & 
:: nil ::
[ nil | 
   -(#0:Msg ; n(b, #1:Fresh) ; #2:Msg), 
   +(n(b, #1:Fresh) ; #2:Msg), nil]  & 
:: nil ::
[ nil | 
   -(n(b, #1:Fresh) ; #2:Msg), 
   +(n(b, #1:Fresh)), nil]  & 
:: #1:Fresh ::
[ nil, 
   -(pk(b, a ; #3:Nonce)), 
   +(pk(a, #3:Nonce ; n(b, #1:Fresh) ; b)) | 
   -(pk(b, n(b, #1:Fresh))), nil] )
|| 
pk(b, n(b, #1:Fresh)) !inI,
n(b, #1:Fresh) !inI,
(n(b, #1:Fresh) ; #2:Msg) !inI,
(#0:Msg ; n(b, #1:Fresh) ; #2:Msg) inI
|| 
-(#0:Msg ; n(b, #1:Fresh) ; #2:Msg), 
+(n(b, #1:Fresh) ; #2:Msg), 
-(n(b, #1:Fresh) ; #2:Msg), 
+(n(b, #1:Fresh)), 
-(n(b, #1:Fresh)), 
+(pk(b, n(b, #1:Fresh))), 
-(pk(b, n(b, #1:Fresh)))
|| 
nil
|| 
nil)
(< 1 . 5 . 5 . 3 > (
:: nil ::
[ nil | 
   -(pk(i, #0:Msg ; n(b, #1:Fresh))), 
   +(#0:Msg ; n(b, #1:Fresh)), nil]  & 
:: nil ::
[ nil | 
   -(n(b, #1:Fresh)), 
   +(pk(b, n(b, #1:Fresh))), nil]  & 
:: nil ::
[ nil | 
   -(#0:Msg ; n(b, #1:Fresh)), 
   +(n(b, #1:Fresh)), nil]  & 
:: #1:Fresh ::
[ nil, 
   -(pk(b, a ; #2:Nonce)), 
   +(pk(a, #2:Nonce ; n(b, #1:Fresh) ; b)) | 
   -(pk(b, n(b, #1:Fresh))), nil] )
|| 
pk(b, n(b, #1:Fresh)) !inI,
n(b, #1:Fresh) !inI,
(#0:Msg ; n(b, #1:Fresh)) !inI,
pk(i, #0:Msg ; n(b, #1:Fresh)) inI
|| 
-(pk(i, #0:Msg ; n(b, #1:Fresh))), 
+(#0:Msg ; n(b, #1:Fresh)), 
-(#0:Msg ; n(b, #1:Fresh)), 
+(n(b, #1:Fresh)), 
-(n(b, #1:Fresh)), 
+(pk(b, n(b, #1:Fresh))), 
-(pk(b, n(b, #1:Fresh)))
|| 
nil
|| 
nil)
(< 1 . 9 . 3 . 9 > (
:: nil ::
[ nil | 
   -(pk(i, n(b, #0:Fresh) ; n(#3:Name, #2:Fresh) ; #3:Name)), 
   +(n(b, #0:Fresh) ; n(#3:Name, #2:Fresh) ; #3:Name), nil]  & 
:: nil ::
[ nil | 
   -(n(b, #0:Fresh) ; n(#3:Name, #2:Fresh) ; #3:Name), 
   +(n(b, #0:Fresh)), nil]  & 
:: #0:Fresh ::
[ nil, 
   -(pk(b, a ; #1:Nonce)), 
   +(pk(a, #1:Nonce ; n(b, #0:Fresh) ; b)) | 
   -(pk(b, n(b, #0:Fresh))), nil]  & 
:: #2:Fresh ::
[ nil | 
   -(pk(#3:Name, i ; n(b, #0:Fresh))), 
   +(pk(i, n(b, #0:Fresh) ; n(#3:Name, #2:Fresh) ; #3:Name)), nil] )
|| 
pk(i, n(b, #0:Fresh) ; n(#3:Name, #2:Fresh) ; #3:Name) !inI,
n(b, #0:Fresh) !inI,
(n(b, #0:Fresh) ; n(#3:Name, #2:Fresh) ; #3:Name) !inI,
pk(b, n(b, #0:Fresh)) inI,
pk(#3:Name, i ; n(b, #0:Fresh)) inI
|| 
-(pk(#3:Name, i ; n(b, #0:Fresh))), 
+(pk(i, n(b, #0:Fresh) ; n(#3:Name, #2:Fresh) ; #3:Name)), 
-(pk(i, n(b, #0:Fresh) ; n(#3:Name, #2:Fresh) ; #3:Name)), 
+(n(b, #0:Fresh) ; n(#3:Name, #2:Fresh) ; #3:Name), 
-(n(b, #0:Fresh) ; n(#3:Name, #2:Fresh) ; #3:Name), 
+(n(b, #0:Fresh)), 
-(pk(b, n(b, #0:Fresh)))
|| 
nil
|| 
nil)
< 1 . 9 . 9 . 4 > (
:: nil ::
[ nil | 
   -(pk(i, #0:Msg ; n(b, #1:Fresh) ; #2:Msg)), 
   +(#0:Msg ; n(b, #1:Fresh) ; #2:Msg), nil]  & 
:: nil ::
[ nil | 
   -(#0:Msg ; n(b, #1:Fresh) ; #2:Msg), 
   +(n(b, #1:Fresh) ; #2:Msg), nil]  & 
:: nil ::
[ nil | 
   -(n(b, #1:Fresh) ; #2:Msg), 
   +(n(b, #1:Fresh)), nil]  & 
:: #1:Fresh ::
[ nil, 
   -(pk(b, a ; #3:Nonce)), 
   +(pk(a, #3:Nonce ; n(b, #1:Fresh) ; b)) | 
   -(pk(b, n(b, #1:Fresh))), nil] )
|| 
n(b, #1:Fresh) !inI,
(#0:Msg ; n(b, #1:Fresh) ; #2:Msg) !inI,
(n(b, #1:Fresh) ; #2:Msg) !inI,
pk(b, n(b, #1:Fresh)) inI,
pk(i, #0:Msg ; n(b, #1:Fresh) ; #2:Msg) inI
|| 
-(pk(i, #0:Msg ; n(b, #1:Fresh) ; #2:Msg)), 
+(#0:Msg ; n(b, #1:Fresh) ; #2:Msg), 
-(#0:Msg ; n(b, #1:Fresh) ; #2:Msg), 
+(n(b, #1:Fresh) ; #2:Msg), 
-(n(b, #1:Fresh) ; #2:Msg), 
+(n(b, #1:Fresh)), 
-(pk(b, n(b, #1:Fresh)))
|| 
nil
|| 
nil
==========================================
reduce in MAUDE-NPA : run(4) .
rewrites: 18 in 0ms cpu (0ms real) (18000000 rewrites/second)
result IdSystemSet: (< 1 . 5 . 4 . 2 . 5 > (
:: nil ::
[ nil | 
   -(pk(i, n(b, #0:Fresh) ; n(#3:Name, #2:Fresh) ; #3:Name)), 
   +(n(b, #0:Fresh) ; n(#3:Name, #2:Fresh) ; #3:Name), nil]  & 
:: nil ::
[ nil | 
   -(n(b, #0:Fresh)), 
   +(pk(b, n(b, #0:Fresh))), nil]  & 
:: nil ::
[ nil | 
   -(n(b, #0:Fresh) ; n(#3:Name, #2:Fresh) ; #3:Name), 
   +(n(b, #0:Fresh)), nil]  & 
:: #0:Fresh ::
[ nil, 
   -(pk(b, a ; #1:Nonce)), 
   +(pk(a, #1:Nonce ; n(b, #0:Fresh) ; b)) | 
   -(pk(b, n(b, #0:Fresh))), nil]  & 
:: #2:Fresh ::
[ nil | 
   -(pk(#3:Name, i ; n(b, #0:Fresh))), 
   +(pk(i, n(b, #0:Fresh) ; n(#3:Name, #2:Fresh) ; #3:Name)), nil] )
|| 
pk(b, n(b, #0:Fresh)) !inI,
pk(i, n(b, #0:Fresh) ; n(#3:Name, #2:Fresh) ; #3:Name) !inI,
n(b, #0:Fresh) !inI,
(n(b, #0:Fresh) ; n(#3:Name, #2:Fresh) ; #3:Name) !inI,
pk(#3:Name, i ; n(b, #0:Fresh)) inI
|| 
-(pk(#3:Name, i ; n(b, #0:Fresh))), 
+(pk(i, n(b, #0:Fresh) ; n(#3:Name, #2:Fresh) ; #3:Name)), 
-(pk(i, n(b, #0:Fresh) ; n(#3:Name, #2:Fresh) ; #3:Name)), 
+(n(b, #0:Fresh) ; n(#3:Name, #2:Fresh) ; #3:Name), 
-(n(b, #0:Fresh) ; n(#3:Name, #2:Fresh) ; #3:Name), 
+(n(b, #0:Fresh)), 
-(n(b, #0:Fresh)), 
+(pk(b, n(b, #0:Fresh))), 
-(pk(b, n(b, #0:Fresh)))
|| 
nil
|| 
nil)
< 1 . 5 . 4 . 6 . 3 > (
:: nil ::
[ nil | 
   -(pk(i, #0:Msg ; n(b, #1:Fresh) ; #2:Msg)), 
   +(#0:Msg ; n(b, #1:Fresh) ; #2:Msg), nil]  & 
:: nil ::
[ nil | 
   -(n(b, #1:Fresh)), 
   +(pk(b, n(b, #1:Fresh))), nil]  & 
:: nil ::
[ nil | 
   -(#0:Msg ; n(b, #1:Fresh) ; #2:Msg), 
   +(n(b, #1:Fresh) ; #2:Msg), nil]  & 
:: nil ::
[ nil | 
   -(n(b, #1:Fresh) ; #2:Msg), 
   +(n(b, #1:Fresh)), nil]  & 
:: #1:Fresh ::
[ nil, 
   -(pk(b, a ; #3:Nonce)), 
   +(pk(a, #3:Nonce ; n(b, #1:Fresh) ; b)) | 
   -(pk(b, n(b, #1:Fresh))), nil] )
|| 
pk(b, n(b, #1:Fresh)) !inI,
n(b, #1:Fresh) !inI,
(#0:Msg ; n(b, #1:Fresh) ; #2:Msg) !inI,
(n(b, #1:Fresh) ; #2:Msg) !inI,
pk(i, #0:Msg ; n(b, #1:Fresh) ; #2:Msg) inI
|| 
-(pk(i, #0:Msg ; n(b, #1:Fresh) ; #2:Msg)), 
+(#0:Msg ; n(b, #1:Fresh) ; #2:Msg), 
-(#0:Msg ; n(b, #1:Fresh) ; #2:Msg), 
+(n(b, #1:Fresh) ; #2:Msg), 
-(n(b, #1:Fresh) ; #2:Msg), 
+(n(b, #1:Fresh)), 
-(n(b, #1:Fresh)), 
+(pk(b, n(b, #1:Fresh))), 
-(pk(b, n(b, #1:Fresh)))
|| 
nil
|| 
nil
==========================================
reduce in MAUDE-NPA : run(5) .
rewrites: 18 in 0ms cpu (0ms real) (18000000 rewrites/second)
result IdSystemSet: (empty).IdSystemSet
Maude> Bye.
Mon Nov 14 00:13:54 CET 2011
Santiago:prototype-20111114 santiago$