Maude> rew 'config{0}.
rewrite in CTXT : 'config{0} .
*********** equation
eq 'config{0} = 'union{0} ('F{0} '0{0}) ('union{0} ('union{0} ('union{0} ('union{0} ('EL{0} '@princ{0} '@A{0}) ('EL{0}
    '@princ{0} '@B{0})) ('EL{0} ('@pubK{0} '@A{0}) '@pkA{0})) ('EL{0} ('@pubK{0} '@B{0}) '@pkB{0})) ('union{0} ('@START-1{
    0} '@A{0} '@B{0}) ('@START-2{0} '@B{0}))) .
empty substitution
Old: 'config{0}
'config{0}
--->
'union{0} ('F{0} '0{0}) ('union{0} ('union{0} ('union{0} ('union{0} ('EL{0} '@princ{0} '@A{0}) ('EL{0} '@princ{0} '@B{0}))
    ('EL{0} ('@pubK{0} '@A{0}) '@pkA{0})) ('EL{0} ('@pubK{0} '@B{0}) '@pkB{0})) ('union{0} ('@START-1{0} '@A{0} '@B{0}) (
    '@START-2{0} '@B{0})))
New: 'union{0} ('F{0} '0{0}) ('union{0} ('union{0} ('union{0} ('union{0} ('EL{0} '@princ{0} '@A{0}) ('EL{0} '@princ{0} '@B{
    0})) ('EL{0} ('@pubK{0} '@A{0}) '@pkA{0})) ('EL{0} ('@pubK{0} '@B{0}) '@pkB{0})) ('union{0} ('@START-1{0} '@A{0} '@B{
    0}) ('@START-2{0} '@B{0})))
*********** equation
eq 'union{0} @1:Trm @2:Trm = $union(@1:Trm, @2:Trm) .
@1:Trm --> 'EL{0} '@princ{0} '@A{0}
@2:Trm --> 'EL{0} '@princ{0} '@B{0}
Old: 'union{0} ('F{0} '0{0}) ('union{0} ('union{0} ('union{0} ('union{0} ('EL{0} '@princ{0} '@A{0}) ('EL{0} '@princ{0} '@B{
    0})) ('EL{0} ('@pubK{0} '@A{0}) '@pkA{0})) ('EL{0} ('@pubK{0} '@B{0}) '@pkB{0})) ('union{0} ('@START-1{0} '@A{0} '@B{
    0}) ('@START-2{0} '@B{0})))
'union{0} ('EL{0} '@princ{0} '@A{0}) ('EL{0} '@princ{0} '@B{0})
--->
$union('EL{0} '@princ{0} '@A{0}, 'EL{0} '@princ{0} '@B{0})
New: 'union{0} ('F{0} '0{0}) ('union{0} ('union{0} ('union{0} $union('EL{0} '@princ{0} '@A{0}, 'EL{0} '@princ{0} '@B{0}) (
    'EL{0} ('@pubK{0} '@A{0}) '@pkA{0})) ('EL{0} ('@pubK{0} '@B{0}) '@pkB{0})) ('union{0} ('@START-1{0} '@A{0} '@B{0}) (
    '@START-2{0} '@B{0})))
*********** equation
eq 'union{0} @1:Trm @2:Trm = $union(@1:Trm, @2:Trm) .
@1:Trm --> $union('EL{0} '@princ{0} '@A{0}, 'EL{0} '@princ{0} '@B{0})
@2:Trm --> 'EL{0} ('@pubK{0} '@A{0}) '@pkA{0}
Old: 'union{0} ('F{0} '0{0}) ('union{0} ('union{0} ('union{0} $union('EL{0} '@princ{0} '@A{0}, 'EL{0} '@princ{0} '@B{0}) (
    'EL{0} ('@pubK{0} '@A{0}) '@pkA{0})) ('EL{0} ('@pubK{0} '@B{0}) '@pkB{0})) ('union{0} ('@START-1{0} '@A{0} '@B{0}) (
    '@START-2{0} '@B{0})))
'union{0} $union('EL{0} '@princ{0} '@A{0}, 'EL{0} '@princ{0} '@B{0}) ('EL{0} ('@pubK{0} '@A{0}) '@pkA{0})
--->
$union($union('EL{0} '@princ{0} '@A{0}, 'EL{0} '@princ{0} '@B{0}), 'EL{0} ('@pubK{0} '@A{0}) '@pkA{0})
New: 'union{0} ('F{0} '0{0}) ('union{0} ('union{0} $union($union('EL{0} '@princ{0} '@A{0}, 'EL{0} '@princ{0} '@B{0}), 'EL{
    0} ('@pubK{0} '@A{0}) '@pkA{0}) ('EL{0} ('@pubK{0} '@B{0}) '@pkB{0})) ('union{0} ('@START-1{0} '@A{0} '@B{0}) (
    '@START-2{0} '@B{0})))
*********** equation
eq 'union{0} @1:Trm @2:Trm = $union(@1:Trm, @2:Trm) .
@1:Trm --> $union('EL{0} '@princ{0} '@A{0}, 'EL{0} '@princ{0} '@B{0}, 'EL{0} ('@pubK{0} '@A{0}) '@pkA{0})
@2:Trm --> 'EL{0} ('@pubK{0} '@B{0}) '@pkB{0}
Old: 'union{0} ('F{0} '0{0}) ('union{0} ('union{0} $union('EL{0} '@princ{0} '@A{0}, 'EL{0} '@princ{0} '@B{0}, 'EL{0} (
    '@pubK{0} '@A{0}) '@pkA{0}) ('EL{0} ('@pubK{0} '@B{0}) '@pkB{0})) ('union{0} ('@START-1{0} '@A{0} '@B{0}) ('@START-2{0}
    '@B{0})))
'union{0} $union('EL{0} '@princ{0} '@A{0}, 'EL{0} '@princ{0} '@B{0}, 'EL{0} ('@pubK{0} '@A{0}) '@pkA{0}) ('EL{0} ('@pubK{0}
    '@B{0}) '@pkB{0})
--->
$union($union('EL{0} '@princ{0} '@A{0}, 'EL{0} '@princ{0} '@B{0}, 'EL{0} ('@pubK{0} '@A{0}) '@pkA{0}), 'EL{0} ('@pubK{0}
    '@B{0}) '@pkB{0})
New: 'union{0} ('F{0} '0{0}) ('union{0} $union($union('EL{0} '@princ{0} '@A{0}, 'EL{0} '@princ{0} '@B{0}, 'EL{0} ('@pubK{0}
    '@A{0}) '@pkA{0}), 'EL{0} ('@pubK{0} '@B{0}) '@pkB{0}) ('union{0} ('@START-1{0} '@A{0} '@B{0}) ('@START-2{0} '@B{0})))
*********** equation
eq 'union{0} @1:Trm @2:Trm = $union(@1:Trm, @2:Trm) .
@1:Trm --> '@START-1{0} '@A{0} '@B{0}
@2:Trm --> '@START-2{0} '@B{0}
Old: 'union{0} ('F{0} '0{0}) ('union{0} $union('EL{0} '@princ{0} '@A{0}, 'EL{0} '@princ{0} '@B{0}, 'EL{0} ('@pubK{0} '@A{
    0}) '@pkA{0}, 'EL{0} ('@pubK{0} '@B{0}) '@pkB{0}) ('union{0} ('@START-1{0} '@A{0} '@B{0}) ('@START-2{0} '@B{0})))
'union{0} ('@START-1{0} '@A{0} '@B{0}) ('@START-2{0} '@B{0})
--->
$union('@START-1{0} '@A{0} '@B{0}, '@START-2{0} '@B{0})
New: 'union{0} ('F{0} '0{0}) ('union{0} $union('EL{0} '@princ{0} '@A{0}, 'EL{0} '@princ{0} '@B{0}, 'EL{0} ('@pubK{0} '@A{
    0}) '@pkA{0}, 'EL{0} ('@pubK{0} '@B{0}) '@pkB{0}) $union('@START-1{0} '@A{0} '@B{0}, '@START-2{0} '@B{0}))
*********** equation
eq 'union{0} @1:Trm @2:Trm = $union(@1:Trm, @2:Trm) .
@1:Trm --> $union('EL{0} '@princ{0} '@A{0}, 'EL{0} '@princ{0} '@B{0}, 'EL{0} ('@pubK{0} '@A{0}) '@pkA{0}, 'EL{0} ('@pubK{0}
    '@B{0}) '@pkB{0})
@2:Trm --> $union('@START-2{0} '@B{0}, '@START-1{0} '@A{0} '@B{0})
Old: 'union{0} ('F{0} '0{0}) ('union{0} $union('EL{0} '@princ{0} '@A{0}, 'EL{0} '@princ{0} '@B{0}, 'EL{0} ('@pubK{0} '@A{
    0}) '@pkA{0}, 'EL{0} ('@pubK{0} '@B{0}) '@pkB{0}) $union('@START-2{0} '@B{0}, '@START-1{0} '@A{0} '@B{0}))
'union{0} $union('EL{0} '@princ{0} '@A{0}, 'EL{0} '@princ{0} '@B{0}, 'EL{0} ('@pubK{0} '@A{0}) '@pkA{0}, 'EL{0} ('@pubK{0}
    '@B{0}) '@pkB{0}) $union('@START-2{0} '@B{0}, '@START-1{0} '@A{0} '@B{0})
--->
$union($union('EL{0} '@princ{0} '@A{0}, 'EL{0} '@princ{0} '@B{0}, 'EL{0} ('@pubK{0} '@A{0}) '@pkA{0}, 'EL{0} ('@pubK{0}
    '@B{0}) '@pkB{0}), $union('@START-2{0} '@B{0}, '@START-1{0} '@A{0} '@B{0}))
New: 'union{0} ('F{0} '0{0}) $union($union('EL{0} '@princ{0} '@A{0}, 'EL{0} '@princ{0} '@B{0}, 'EL{0} ('@pubK{0} '@A{0})
    '@pkA{0}, 'EL{0} ('@pubK{0} '@B{0}) '@pkB{0}), $union('@START-2{0} '@B{0}, '@START-1{0} '@A{0} '@B{0}))
*********** equation
eq 'union{0} @1:Trm @2:Trm = $union(@1:Trm, @2:Trm) .
@1:Trm --> 'F{0} '0{0}
@2:Trm --> $union('@START-2{0} '@B{0}, '@START-1{0} '@A{0} '@B{0}, 'EL{0} '@princ{0} '@A{0}, 'EL{0} '@princ{0} '@B{0}, 'EL{
    0} ('@pubK{0} '@A{0}) '@pkA{0}, 'EL{0} ('@pubK{0} '@B{0}) '@pkB{0})
Old: 'union{0} ('F{0} '0{0}) $union('@START-2{0} '@B{0}, '@START-1{0} '@A{0} '@B{0}, 'EL{0} '@princ{0} '@A{0}, 'EL{0}
    '@princ{0} '@B{0}, 'EL{0} ('@pubK{0} '@A{0}) '@pkA{0}, 'EL{0} ('@pubK{0} '@B{0}) '@pkB{0})
'union{0} ('F{0} '0{0}) $union('@START-2{0} '@B{0}, '@START-1{0} '@A{0} '@B{0}, 'EL{0} '@princ{0} '@A{0}, 'EL{0} '@princ{0}
    '@B{0}, 'EL{0} ('@pubK{0} '@A{0}) '@pkA{0}, 'EL{0} ('@pubK{0} '@B{0}) '@pkB{0})
--->
$union('F{0} '0{0}, $union('@START-2{0} '@B{0}, '@START-1{0} '@A{0} '@B{0}, 'EL{0} '@princ{0} '@A{0}, 'EL{0} '@princ{0}
    '@B{0}, 'EL{0} ('@pubK{0} '@A{0}) '@pkA{0}, 'EL{0} ('@pubK{0} '@B{0}) '@pkB{0}))
New: $union('F{0} '0{0}, $union('@START-2{0} '@B{0}, '@START-1{0} '@A{0} '@B{0}, 'EL{0} '@princ{0} '@A{0}, 'EL{0} '@princ{
    0} '@B{0}, 'EL{0} ('@pubK{0} '@A{0}) '@pkA{0}, 'EL{0} ('@pubK{0} '@B{0}) '@pkB{0}))
*********** trial #1
crl $union('F{0} @fresh:Trm, '@START-1{0} @@A:Trm @@B:Trm, 'EL{0} ('@pubK{0} @@B:Trm) @@PKB:Trm) => $union(
    'T_initiator_Init2{0} @@A:Trm @@L:Trm, $union('EL{0} ('@pubK{0} @@B:Trm) @@PKB:Trm, $union(@@L:Trm @@B:Trm @@nA:Trm,
    $union('@N{0} $@&($@&('@princ-msg{0} @@A:Trm, '@princ-msg{0} @@B:Trm), '@encrypt{0} @@PKB:Trm $@&('@nonce-msg{0}
    @@nA:Trm, '@princ-msg{0} @@A:Trm)), 'F{0} @fresh':Trm)))) if @@L:Trm := 'FRESH{0} ({'_ : '@princ{0}} {'_ : '@nonce{0}}
    '@state{0}) @fresh:Trm /\ @@nA:Trm := 'FRESH{0} '@nonce{0} ('suc{0} @fresh:Trm) /\ @fresh':Trm := 'suc{0} ('suc{0}
    @fresh:Trm) .
@fresh:Trm --> '0{0}
@@A:Trm --> '@A{0}
@@B:Trm --> '@B{0}
@@PKB:Trm --> '@pkB{0}
@@L:Trm --> (unbound)
@@nA:Trm --> (unbound)
@fresh':Trm --> (unbound)
*********** solving condition fragment
@@L:Trm := 'FRESH{0} ({'_ : '@princ{0}} {'_ : '@nonce{0}} '@state{0}) @fresh:Trm
*********** success for condition fragment
@@L:Trm := 'FRESH{0} ({'_ : '@princ{0}} {'_ : '@nonce{0}} '@state{0}) @fresh:Trm
@fresh:Trm --> '0{0}
@@A:Trm --> '@A{0}
@@B:Trm --> '@B{0}
@@PKB:Trm --> '@pkB{0}
@@L:Trm --> 'FRESH{0} ({'_ : '@princ{0}} {'_ : '@nonce{0}} '@state{0}) '0{0}
@@nA:Trm --> (unbound)
@fresh':Trm --> (unbound)
*********** solving condition fragment
@@nA:Trm := 'FRESH{0} '@nonce{0} ('suc{0} @fresh:Trm)
*********** success for condition fragment
@@nA:Trm := 'FRESH{0} '@nonce{0} ('suc{0} @fresh:Trm)
@fresh:Trm --> '0{0}
@@A:Trm --> '@A{0}
@@B:Trm --> '@B{0}
@@PKB:Trm --> '@pkB{0}
@@L:Trm --> 'FRESH{0} ({'_ : '@princ{0}} {'_ : '@nonce{0}} '@state{0}) '0{0}
@@nA:Trm --> 'FRESH{0} '@nonce{0} ('suc{0} '0{0})
@fresh':Trm --> (unbound)
*********** solving condition fragment
@fresh':Trm := 'suc{0} ('suc{0} @fresh:Trm)
*********** success for condition fragment
@fresh':Trm := 'suc{0} ('suc{0} @fresh:Trm)
@fresh:Trm --> '0{0}
@@A:Trm --> '@A{0}
@@B:Trm --> '@B{0}
@@PKB:Trm --> '@pkB{0}
@@L:Trm --> 'FRESH{0} ({'_ : '@princ{0}} {'_ : '@nonce{0}} '@state{0}) '0{0}
@@nA:Trm --> 'FRESH{0} '@nonce{0} ('suc{0} '0{0})
@fresh':Trm --> 'suc{0} ('suc{0} '0{0})
*********** success #1
*********** rule
crl $union('F{0} @fresh:Trm, '@START-1{0} @@A:Trm @@B:Trm, 'EL{0} ('@pubK{0} @@B:Trm) @@PKB:Trm) => $union(
    'T_initiator_Init2{0} @@A:Trm @@L:Trm, $union('EL{0} ('@pubK{0} @@B:Trm) @@PKB:Trm, $union(@@L:Trm @@B:Trm @@nA:Trm,
    $union('@N{0} $@&($@&('@princ-msg{0} @@A:Trm, '@princ-msg{0} @@B:Trm), '@encrypt{0} @@PKB:Trm $@&('@nonce-msg{0}
    @@nA:Trm, '@princ-msg{0} @@A:Trm)), 'F{0} @fresh':Trm)))) if @@L:Trm := 'FRESH{0} ({'_ : '@princ{0}} {'_ : '@nonce{0}}
    '@state{0}) @fresh:Trm /\ @@nA:Trm := 'FRESH{0} '@nonce{0} ('suc{0} @fresh:Trm) /\ @fresh':Trm := 'suc{0} ('suc{0}
    @fresh:Trm) .
@fresh:Trm --> '0{0}
@@A:Trm --> '@A{0}
@@B:Trm --> '@B{0}
@@PKB:Trm --> '@pkB{0}
@@L:Trm --> 'FRESH{0} ({'_ : '@princ{0}} {'_ : '@nonce{0}} '@state{0}) '0{0}
@@nA:Trm --> 'FRESH{0} '@nonce{0} ('suc{0} '0{0})
@fresh':Trm --> 'suc{0} ('suc{0} '0{0})
Old: $union('@START-2{0} '@B{0}, 'F{0} '0{0}, '@START-1{0} '@A{0} '@B{0}, 'EL{0} '@princ{0} '@A{0}, 'EL{0} '@princ{0} '@B{
    0}, 'EL{0} ('@pubK{0} '@A{0}) '@pkA{0}, 'EL{0} ('@pubK{0} '@B{0}) '@pkB{0})
$union('@START-2{0} '@B{0}, 'F{0} '0{0}, '@START-1{0} '@A{0} '@B{0}, 'EL{0} '@princ{0} '@A{0}, 'EL{0} '@princ{0} '@B{0},
    'EL{0} ('@pubK{0} '@A{0}) '@pkA{0}, 'EL{0} ('@pubK{0} '@B{0}) '@pkB{0})
--->
$union($union('@START-2{0} '@B{0}, 'EL{0} '@princ{0} '@A{0}, 'EL{0} '@princ{0} '@B{0}, 'EL{0} ('@pubK{0} '@A{0}) '@pkA{0}),
    $union('T_initiator_Init2{0} '@A{0} ('FRESH{0} ({'_ : '@princ{0}} {'_ : '@nonce{0}} '@state{0}) '0{0}), $union('EL{0} (
    '@pubK{0} '@B{0}) '@pkB{0}, $union('FRESH{0} ({'_ : '@princ{0}} {'_ : '@nonce{0}} '@state{0}) '0{0} '@B{0} ('FRESH{0}
    '@nonce{0} ('suc{0} '0{0})), $union('@N{0} $@&($@&('@princ-msg{0} '@A{0}, '@princ-msg{0} '@B{0}), '@encrypt{0} '@pkB{0}
    $@&('@nonce-msg{0} ('FRESH{0} '@nonce{0} ('suc{0} '0{0})), '@princ-msg{0} '@A{0})), 'F{0} ('suc{0} ('suc{0} '0{
    0})))))))
New: $union($union('@START-2{0} '@B{0}, 'EL{0} '@princ{0} '@A{0}, 'EL{0} '@princ{0} '@B{0}, 'EL{0} ('@pubK{0} '@A{0})
    '@pkA{0}), $union('T_initiator_Init2{0} '@A{0} ('FRESH{0} ({'_ : '@princ{0}} {'_ : '@nonce{0}} '@state{0}) '0{0}),
    $union('EL{0} ('@pubK{0} '@B{0}) '@pkB{0}, $union('FRESH{0} ({'_ : '@princ{0}} {'_ : '@nonce{0}} '@state{0}) '0{0} '@B{
    0} ('FRESH{0} '@nonce{0} ('suc{0} '0{0})), $union('@N{0} $@&($@&('@princ-msg{0} '@A{0}, '@princ-msg{0} '@B{0}),
    '@encrypt{0} '@pkB{0} $@&('@nonce-msg{0} ('FRESH{0} '@nonce{0} ('suc{0} '0{0})), '@princ-msg{0} '@A{0})), 'F{0} ('suc{
    0} ('suc{0} '0{0})))))))
*********** trial #2
crl $union('@N{0} $@&('@princ-msg{0} @@A:Trm, '@princ-msg{0} @@B:Trm, '@encrypt{0} @@PKB:Trm $@&('@nonce-msg{0} @@nA:Trm,
    '@princ-msg{0} @@A:Trm)), '@START-2{0} @@B:Trm, 'F{0} @fresh:Trm, 'EL{0} ('@pubK{0} @@A:Trm) @@PKA:Trm) => $union(
    'T_responder_Resp2{0} @@B:Trm @@L:Trm, $union('EL{0} ('@pubK{0} @@A:Trm) @@PKA:Trm, $union(@@L:Trm @@A:Trm @@nB:Trm,
    $union('@N{0} $@&($@&('@princ-msg{0} @@B:Trm, '@princ-msg{0} @@A:Trm), '@encrypt{0} @@PKA:Trm $@&('@nonce-msg{0}
    @@nA:Trm, '@nonce-msg{0} @@nB:Trm)), 'F{0} @fresh':Trm)))) if @@L:Trm := 'FRESH{0} ({'_ : '@princ{0}} {'_ : '@nonce{0}}
    '@state{0}) @fresh:Trm /\ @@nB:Trm := 'FRESH{0} '@nonce{0} ('suc{0} @fresh:Trm) /\ @fresh':Trm := 'suc{0} ('suc{0}
    @fresh:Trm) .
@@A:Trm --> '@A{0}
@@B:Trm --> '@B{0}
@@PKB:Trm --> '@pkB{0}
@@nA:Trm --> 'FRESH{0} '@nonce{0} ('suc{0} '0{0})
@fresh:Trm --> 'suc{0} ('suc{0} '0{0})
@@PKA:Trm --> '@pkA{0}
@@L:Trm --> (unbound)
@@nB:Trm --> (unbound)
@fresh':Trm --> (unbound)
*********** solving condition fragment
@@L:Trm := 'FRESH{0} ({'_ : '@princ{0}} {'_ : '@nonce{0}} '@state{0}) @fresh:Trm
*********** success for condition fragment
@@L:Trm := 'FRESH{0} ({'_ : '@princ{0}} {'_ : '@nonce{0}} '@state{0}) @fresh:Trm
@@A:Trm --> '@A{0}
@@B:Trm --> '@B{0}
@@PKB:Trm --> '@pkB{0}
@@nA:Trm --> 'FRESH{0} '@nonce{0} ('suc{0} '0{0})
@fresh:Trm --> 'suc{0} ('suc{0} '0{0})
@@PKA:Trm --> '@pkA{0}
@@L:Trm --> 'FRESH{0} ({'_ : '@princ{0}} {'_ : '@nonce{0}} '@state{0}) ('suc{0} ('suc{0} '0{0}))
@@nB:Trm --> (unbound)
@fresh':Trm --> (unbound)
*********** solving condition fragment
@@nB:Trm := 'FRESH{0} '@nonce{0} ('suc{0} @fresh:Trm)
*********** success for condition fragment
@@nB:Trm := 'FRESH{0} '@nonce{0} ('suc{0} @fresh:Trm)
@@A:Trm --> '@A{0}
@@B:Trm --> '@B{0}
@@PKB:Trm --> '@pkB{0}
@@nA:Trm --> 'FRESH{0} '@nonce{0} ('suc{0} '0{0})
@fresh:Trm --> 'suc{0} ('suc{0} '0{0})
@@PKA:Trm --> '@pkA{0}
@@L:Trm --> 'FRESH{0} ({'_ : '@princ{0}} {'_ : '@nonce{0}} '@state{0}) ('suc{0} ('suc{0} '0{0}))
@@nB:Trm --> 'FRESH{0} '@nonce{0} ('suc{0} ('suc{0} ('suc{0} '0{0})))
@fresh':Trm --> (unbound)
*********** solving condition fragment
@fresh':Trm := 'suc{0} ('suc{0} @fresh:Trm)
*********** success for condition fragment
@fresh':Trm := 'suc{0} ('suc{0} @fresh:Trm)
@@A:Trm --> '@A{0}
@@B:Trm --> '@B{0}
@@PKB:Trm --> '@pkB{0}
@@nA:Trm --> 'FRESH{0} '@nonce{0} ('suc{0} '0{0})
@fresh:Trm --> 'suc{0} ('suc{0} '0{0})
@@PKA:Trm --> '@pkA{0}
@@L:Trm --> 'FRESH{0} ({'_ : '@princ{0}} {'_ : '@nonce{0}} '@state{0}) ('suc{0} ('suc{0} '0{0}))
@@nB:Trm --> 'FRESH{0} '@nonce{0} ('suc{0} ('suc{0} ('suc{0} '0{0})))
@fresh':Trm --> 'suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0})))
*********** success #2
*********** rule
crl $union('@N{0} $@&('@princ-msg{0} @@A:Trm, '@princ-msg{0} @@B:Trm, '@encrypt{0} @@PKB:Trm $@&('@nonce-msg{0} @@nA:Trm,
    '@princ-msg{0} @@A:Trm)), '@START-2{0} @@B:Trm, 'F{0} @fresh:Trm, 'EL{0} ('@pubK{0} @@A:Trm) @@PKA:Trm) => $union(
    'T_responder_Resp2{0} @@B:Trm @@L:Trm, $union('EL{0} ('@pubK{0} @@A:Trm) @@PKA:Trm, $union(@@L:Trm @@A:Trm @@nB:Trm,
    $union('@N{0} $@&($@&('@princ-msg{0} @@B:Trm, '@princ-msg{0} @@A:Trm), '@encrypt{0} @@PKA:Trm $@&('@nonce-msg{0}
    @@nA:Trm, '@nonce-msg{0} @@nB:Trm)), 'F{0} @fresh':Trm)))) if @@L:Trm := 'FRESH{0} ({'_ : '@princ{0}} {'_ : '@nonce{0}}
    '@state{0}) @fresh:Trm /\ @@nB:Trm := 'FRESH{0} '@nonce{0} ('suc{0} @fresh:Trm) /\ @fresh':Trm := 'suc{0} ('suc{0}
    @fresh:Trm) .
@@A:Trm --> '@A{0}
@@B:Trm --> '@B{0}
@@PKB:Trm --> '@pkB{0}
@@nA:Trm --> 'FRESH{0} '@nonce{0} ('suc{0} '0{0})
@fresh:Trm --> 'suc{0} ('suc{0} '0{0})
@@PKA:Trm --> '@pkA{0}
@@L:Trm --> 'FRESH{0} ({'_ : '@princ{0}} {'_ : '@nonce{0}} '@state{0}) ('suc{0} ('suc{0} '0{0}))
@@nB:Trm --> 'FRESH{0} '@nonce{0} ('suc{0} ('suc{0} ('suc{0} '0{0})))
@fresh':Trm --> 'suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0})))
Old: $union('@N{0} $@&('@princ-msg{0} '@A{0}, '@princ-msg{0} '@B{0}, '@encrypt{0} '@pkB{0} $@&('@nonce-msg{0} ('FRESH{0}
    '@nonce{0} ('suc{0} '0{0})), '@princ-msg{0} '@A{0})), '@START-2{0} '@B{0}, 'F{0} ('suc{0} ('suc{0} '0{0})), 'EL{0}
    '@princ{0} '@A{0}, 'EL{0} '@princ{0} '@B{0}, 'EL{0} ('@pubK{0} '@A{0}) '@pkA{0}, 'EL{0} ('@pubK{0} '@B{0}) '@pkB{0},
    'T_initiator_Init2{0} '@A{0} ('FRESH{0} ({'_ : '@princ{0}} {'_ : '@nonce{0}} '@state{0}) '0{0}), 'FRESH{0} ({'_ :
    '@princ{0}} {'_ : '@nonce{0}} '@state{0}) '0{0} '@B{0} ('FRESH{0} '@nonce{0} ('suc{0} '0{0})))
$union('@N{0} $@&('@princ-msg{0} '@A{0}, '@princ-msg{0} '@B{0}, '@encrypt{0} '@pkB{0} $@&('@nonce-msg{0} ('FRESH{0}
    '@nonce{0} ('suc{0} '0{0})), '@princ-msg{0} '@A{0})), '@START-2{0} '@B{0}, 'F{0} ('suc{0} ('suc{0} '0{0})), 'EL{0}
    '@princ{0} '@A{0}, 'EL{0} '@princ{0} '@B{0}, 'EL{0} ('@pubK{0} '@A{0}) '@pkA{0}, 'EL{0} ('@pubK{0} '@B{0}) '@pkB{0},
    'T_initiator_Init2{0} '@A{0} ('FRESH{0} ({'_ : '@princ{0}} {'_ : '@nonce{0}} '@state{0}) '0{0}), 'FRESH{0} ({'_ :
    '@princ{0}} {'_ : '@nonce{0}} '@state{0}) '0{0} '@B{0} ('FRESH{0} '@nonce{0} ('suc{0} '0{0})))
--->
$union($union('EL{0} '@princ{0} '@A{0}, 'EL{0} '@princ{0} '@B{0}, 'EL{0} ('@pubK{0} '@B{0}) '@pkB{0}, 'T_initiator_Init2{0}
    '@A{0} ('FRESH{0} ({'_ : '@princ{0}} {'_ : '@nonce{0}} '@state{0}) '0{0}), 'FRESH{0} ({'_ : '@princ{0}} {'_ : '@nonce{
    0}} '@state{0}) '0{0} '@B{0} ('FRESH{0} '@nonce{0} ('suc{0} '0{0}))), $union('T_responder_Resp2{0} '@B{0} ('FRESH{0} ({
    '_ : '@princ{0}} {'_ : '@nonce{0}} '@state{0}) ('suc{0} ('suc{0} '0{0}))), $union('EL{0} ('@pubK{0} '@A{0}) '@pkA{0},
    $union('FRESH{0} ({'_ : '@princ{0}} {'_ : '@nonce{0}} '@state{0}) ('suc{0} ('suc{0} '0{0})) '@A{0} ('FRESH{0} '@nonce{
    0} ('suc{0} ('suc{0} ('suc{0} '0{0})))), $union('@N{0} $@&($@&('@princ-msg{0} '@B{0}, '@princ-msg{0} '@A{0}),
    '@encrypt{0} '@pkA{0} $@&('@nonce-msg{0} ('FRESH{0} '@nonce{0} ('suc{0} '0{0})), '@nonce-msg{0} ('FRESH{0} '@nonce{0} (
    'suc{0} ('suc{0} ('suc{0} '0{0})))))), 'F{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0})))))))))
New: $union($union('EL{0} '@princ{0} '@A{0}, 'EL{0} '@princ{0} '@B{0}, 'EL{0} ('@pubK{0} '@B{0}) '@pkB{0},
    'T_initiator_Init2{0} '@A{0} ('FRESH{0} ({'_ : '@princ{0}} {'_ : '@nonce{0}} '@state{0}) '0{0}), 'FRESH{0} ({'_ :
    '@princ{0}} {'_ : '@nonce{0}} '@state{0}) '0{0} '@B{0} ('FRESH{0} '@nonce{0} ('suc{0} '0{0}))), $union(
    'T_responder_Resp2{0} '@B{0} ('FRESH{0} ({'_ : '@princ{0}} {'_ : '@nonce{0}} '@state{0}) ('suc{0} ('suc{0} '0{0}))),
    $union('EL{0} ('@pubK{0} '@A{0}) '@pkA{0}, $union('FRESH{0} ({'_ : '@princ{0}} {'_ : '@nonce{0}} '@state{0}) ('suc{0} (
    'suc{0} '0{0})) '@A{0} ('FRESH{0} '@nonce{0} ('suc{0} ('suc{0} ('suc{0} '0{0})))), $union('@N{0} $@&($@&('@princ-msg{0}
    '@B{0}, '@princ-msg{0} '@A{0}), '@encrypt{0} '@pkA{0} $@&('@nonce-msg{0} ('FRESH{0} '@nonce{0} ('suc{0} '0{0})),
    '@nonce-msg{0} ('FRESH{0} '@nonce{0} ('suc{0} ('suc{0} ('suc{0} '0{0})))))), 'F{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0}
    '0{0})))))))))
*********** trial #3
crl $union('@N{0} $@&('@princ-msg{0} @@B:Trm, '@princ-msg{0} @@A:Trm, '@encrypt{0} @@PKA:Trm $@&('@nonce-msg{0} @@nA:Trm,
    '@nonce-msg{0} @@nB:Trm)), 'F{0} @fresh:Trm, @@L:Trm @@B:Trm @@nA:Trm, 'EL{0} ('@pubK{0} @@B:Trm) @@PKB:Trm) => $union(
    'T_initiator_Init1{0} @@A:Trm @@L:Trm, $union('EL{0} ('@pubK{0} @@B:Trm) @@PKB:Trm, $union('F{0} @fresh':Trm, $union(
    '@N{0} $@&($@&('@princ-msg{0} @@A:Trm, '@princ-msg{0} @@B:Trm), '@encrypt{0} @@PKB:Trm ('@nonce-msg{0} @@nB:Trm)),
    '@TERMINATED-1{0} @@A:Trm)))) if @@L:Trm := 'FRESH{0} ({'_ : '@princ{0}} {'_ : '@nonce{0}} '@state{0}) @fresh:Trm /\
    @fresh':Trm := 'suc{0} @fresh:Trm .
@@B:Trm --> '@B{0}
@@A:Trm --> '@A{0}
@@PKA:Trm --> '@pkA{0}
@@nA:Trm --> 'FRESH{0} '@nonce{0} ('suc{0} '0{0})
@@nB:Trm --> 'FRESH{0} '@nonce{0} ('suc{0} ('suc{0} ('suc{0} '0{0})))
@fresh:Trm --> 'suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0})))
@@L:Trm --> 'FRESH{0} ({'_ : '@princ{0}} {'_ : '@nonce{0}} '@state{0}) '0{0}
@@PKB:Trm --> '@pkB{0}
@fresh':Trm --> (unbound)
*********** solving condition fragment
@@L:Trm := 'FRESH{0} ({'_ : '@princ{0}} {'_ : '@nonce{0}} '@state{0}) @fresh:Trm
*********** failure for condition fragment
@@L:Trm := 'FRESH{0} ({'_ : '@princ{0}} {'_ : '@nonce{0}} '@state{0}) @fresh:Trm
*********** failure #3
*********** trial #4
crl $union('@N{0} $@&('@princ-msg{0} @@B:Trm, '@princ-msg{0} @@A:Trm, '@encrypt{0} @@PKA:Trm $@&('@nonce-msg{0} @@nA:Trm,
    '@nonce-msg{0} @@nB:Trm)), 'F{0} @fresh:Trm, @@L:Trm @@B:Trm @@nA:Trm, 'EL{0} ('@pubK{0} @@B:Trm) @@PKB:Trm,
    'T_initiator_Init2{0} @@A:Trm @@L:Trm) => $union('EL{0} ('@pubK{0} @@B:Trm) @@PKB:Trm, $union('F{0} @fresh':Trm,
    $union('@N{0} $@&($@&('@princ-msg{0} @@A:Trm, '@princ-msg{0} @@B:Trm), '@encrypt{0} @@PKB:Trm ('@nonce-msg{0}
    @@nB:Trm)), '@TERMINATED-1{0} @@A:Trm))) if @fresh':Trm := @fresh:Trm .
@@B:Trm --> '@B{0}
@@A:Trm --> '@A{0}
@@PKA:Trm --> '@pkA{0}
@@nA:Trm --> 'FRESH{0} '@nonce{0} ('suc{0} '0{0})
@@nB:Trm --> 'FRESH{0} '@nonce{0} ('suc{0} ('suc{0} ('suc{0} '0{0})))
@fresh:Trm --> 'suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0})))
@@L:Trm --> 'FRESH{0} ({'_ : '@princ{0}} {'_ : '@nonce{0}} '@state{0}) '0{0}
@@PKB:Trm --> '@pkB{0}
@fresh':Trm --> (unbound)
*********** solving condition fragment
@fresh':Trm := @fresh:Trm
*********** success for condition fragment
@fresh':Trm := @fresh:Trm
@@B:Trm --> '@B{0}
@@A:Trm --> '@A{0}
@@PKA:Trm --> '@pkA{0}
@@nA:Trm --> 'FRESH{0} '@nonce{0} ('suc{0} '0{0})
@@nB:Trm --> 'FRESH{0} '@nonce{0} ('suc{0} ('suc{0} ('suc{0} '0{0})))
@fresh:Trm --> 'suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0})))
@@L:Trm --> 'FRESH{0} ({'_ : '@princ{0}} {'_ : '@nonce{0}} '@state{0}) '0{0}
@@PKB:Trm --> '@pkB{0}
@fresh':Trm --> 'suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0})))
*********** success #4
*********** rule
crl $union('@N{0} $@&('@princ-msg{0} @@B:Trm, '@princ-msg{0} @@A:Trm, '@encrypt{0} @@PKA:Trm $@&('@nonce-msg{0} @@nA:Trm,
    '@nonce-msg{0} @@nB:Trm)), 'F{0} @fresh:Trm, @@L:Trm @@B:Trm @@nA:Trm, 'EL{0} ('@pubK{0} @@B:Trm) @@PKB:Trm,
    'T_initiator_Init2{0} @@A:Trm @@L:Trm) => $union('EL{0} ('@pubK{0} @@B:Trm) @@PKB:Trm, $union('F{0} @fresh':Trm,
    $union('@N{0} $@&($@&('@princ-msg{0} @@A:Trm, '@princ-msg{0} @@B:Trm), '@encrypt{0} @@PKB:Trm ('@nonce-msg{0}
    @@nB:Trm)), '@TERMINATED-1{0} @@A:Trm))) if @fresh':Trm := @fresh:Trm .
@@B:Trm --> '@B{0}
@@A:Trm --> '@A{0}
@@PKA:Trm --> '@pkA{0}
@@nA:Trm --> 'FRESH{0} '@nonce{0} ('suc{0} '0{0})
@@nB:Trm --> 'FRESH{0} '@nonce{0} ('suc{0} ('suc{0} ('suc{0} '0{0})))
@fresh:Trm --> 'suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0})))
@@L:Trm --> 'FRESH{0} ({'_ : '@princ{0}} {'_ : '@nonce{0}} '@state{0}) '0{0}
@@PKB:Trm --> '@pkB{0}
@fresh':Trm --> 'suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0})))
Old: $union('@N{0} $@&('@princ-msg{0} '@B{0}, '@princ-msg{0} '@A{0}, '@encrypt{0} '@pkA{0} $@&('@nonce-msg{0} ('FRESH{0}
    '@nonce{0} ('suc{0} '0{0})), '@nonce-msg{0} ('FRESH{0} '@nonce{0} ('suc{0} ('suc{0} ('suc{0} '0{0})))))), 'F{0} ('suc{
    0} ('suc{0} ('suc{0} ('suc{0} '0{0})))), 'EL{0} '@princ{0} '@A{0}, 'EL{0} '@princ{0} '@B{0}, 'EL{0} ('@pubK{0} '@A{0})
    '@pkA{0}, 'EL{0} ('@pubK{0} '@B{0}) '@pkB{0}, 'T_initiator_Init2{0} '@A{0} ('FRESH{0} ({'_ : '@princ{0}} {'_ : '@nonce{
    0}} '@state{0}) '0{0}), 'T_responder_Resp2{0} '@B{0} ('FRESH{0} ({'_ : '@princ{0}} {'_ : '@nonce{0}} '@state{0}) ('suc{
    0} ('suc{0} '0{0}))), 'FRESH{0} ({'_ : '@princ{0}} {'_ : '@nonce{0}} '@state{0}) '0{0} '@B{0} ('FRESH{0} '@nonce{0} (
    'suc{0} '0{0})), 'FRESH{0} ({'_ : '@princ{0}} {'_ : '@nonce{0}} '@state{0}) ('suc{0} ('suc{0} '0{0})) '@A{0} ('FRESH{0}
    '@nonce{0} ('suc{0} ('suc{0} ('suc{0} '0{0})))))
$union('@N{0} $@&('@princ-msg{0} '@B{0}, '@princ-msg{0} '@A{0}, '@encrypt{0} '@pkA{0} $@&('@nonce-msg{0} ('FRESH{0}
    '@nonce{0} ('suc{0} '0{0})), '@nonce-msg{0} ('FRESH{0} '@nonce{0} ('suc{0} ('suc{0} ('suc{0} '0{0})))))), 'F{0} ('suc{
    0} ('suc{0} ('suc{0} ('suc{0} '0{0})))), 'EL{0} '@princ{0} '@A{0}, 'EL{0} '@princ{0} '@B{0}, 'EL{0} ('@pubK{0} '@A{0})
    '@pkA{0}, 'EL{0} ('@pubK{0} '@B{0}) '@pkB{0}, 'T_initiator_Init2{0} '@A{0} ('FRESH{0} ({'_ : '@princ{0}} {'_ : '@nonce{
    0}} '@state{0}) '0{0}), 'T_responder_Resp2{0} '@B{0} ('FRESH{0} ({'_ : '@princ{0}} {'_ : '@nonce{0}} '@state{0}) ('suc{
    0} ('suc{0} '0{0}))), 'FRESH{0} ({'_ : '@princ{0}} {'_ : '@nonce{0}} '@state{0}) '0{0} '@B{0} ('FRESH{0} '@nonce{0} (
    'suc{0} '0{0})), 'FRESH{0} ({'_ : '@princ{0}} {'_ : '@nonce{0}} '@state{0}) ('suc{0} ('suc{0} '0{0})) '@A{0} ('FRESH{0}
    '@nonce{0} ('suc{0} ('suc{0} ('suc{0} '0{0})))))
--->
$union($union('EL{0} '@princ{0} '@A{0}, 'EL{0} '@princ{0} '@B{0}, 'EL{0} ('@pubK{0} '@A{0}) '@pkA{0}, 'T_responder_Resp2{0}
    '@B{0} ('FRESH{0} ({'_ : '@princ{0}} {'_ : '@nonce{0}} '@state{0}) ('suc{0} ('suc{0} '0{0}))), 'FRESH{0} ({'_ :
    '@princ{0}} {'_ : '@nonce{0}} '@state{0}) ('suc{0} ('suc{0} '0{0})) '@A{0} ('FRESH{0} '@nonce{0} ('suc{0} ('suc{0} (
    'suc{0} '0{0}))))), $union('EL{0} ('@pubK{0} '@B{0}) '@pkB{0}, $union('F{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{
    0})))), $union('@N{0} $@&($@&('@princ-msg{0} '@A{0}, '@princ-msg{0} '@B{0}), '@encrypt{0} '@pkB{0} ('@nonce-msg{0} (
    'FRESH{0} '@nonce{0} ('suc{0} ('suc{0} ('suc{0} '0{0})))))), '@TERMINATED-1{0} '@A{0}))))
New: $union($union('EL{0} '@princ{0} '@A{0}, 'EL{0} '@princ{0} '@B{0}, 'EL{0} ('@pubK{0} '@A{0}) '@pkA{0},
    'T_responder_Resp2{0} '@B{0} ('FRESH{0} ({'_ : '@princ{0}} {'_ : '@nonce{0}} '@state{0}) ('suc{0} ('suc{0} '0{0}))),
    'FRESH{0} ({'_ : '@princ{0}} {'_ : '@nonce{0}} '@state{0}) ('suc{0} ('suc{0} '0{0})) '@A{0} ('FRESH{0} '@nonce{0} (
    'suc{0} ('suc{0} ('suc{0} '0{0}))))), $union('EL{0} ('@pubK{0} '@B{0}) '@pkB{0}, $union('F{0} ('suc{0} ('suc{0} ('suc{
    0} ('suc{0} '0{0})))), $union('@N{0} $@&($@&('@princ-msg{0} '@A{0}, '@princ-msg{0} '@B{0}), '@encrypt{0} '@pkB{0} (
    '@nonce-msg{0} ('FRESH{0} '@nonce{0} ('suc{0} ('suc{0} ('suc{0} '0{0})))))), '@TERMINATED-1{0} '@A{0}))))
*********** trial #5
crl $union('@N{0} $@&('@princ-msg{0} @@A:Trm, '@princ-msg{0} @@B:Trm, '@encrypt{0} @@PKB:Trm ('@nonce-msg{0} @@nB:Trm)),
    'F{0} @fresh:Trm, @@L:Trm @@A:Trm @@nB:Trm, 'T_responder_Resp2{0} @@B:Trm @@L:Trm) => $union('@TERMINATED-2{0} @@B:Trm,
    'F{0} @fresh':Trm) if @fresh':Trm := @fresh:Trm .
@@A:Trm --> '@A{0}
@@B:Trm --> '@B{0}
@@PKB:Trm --> '@pkB{0}
@@nB:Trm --> 'FRESH{0} '@nonce{0} ('suc{0} ('suc{0} ('suc{0} '0{0})))
@fresh:Trm --> 'suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0})))
@@L:Trm --> 'FRESH{0} ({'_ : '@princ{0}} {'_ : '@nonce{0}} '@state{0}) ('suc{0} ('suc{0} '0{0}))
@fresh':Trm --> (unbound)
*********** solving condition fragment
@fresh':Trm := @fresh:Trm
*********** success for condition fragment
@fresh':Trm := @fresh:Trm
@@A:Trm --> '@A{0}
@@B:Trm --> '@B{0}
@@PKB:Trm --> '@pkB{0}
@@nB:Trm --> 'FRESH{0} '@nonce{0} ('suc{0} ('suc{0} ('suc{0} '0{0})))
@fresh:Trm --> 'suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0})))
@@L:Trm --> 'FRESH{0} ({'_ : '@princ{0}} {'_ : '@nonce{0}} '@state{0}) ('suc{0} ('suc{0} '0{0}))
@fresh':Trm --> 'suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0})))
*********** success #5
*********** rule
crl $union('@N{0} $@&('@princ-msg{0} @@A:Trm, '@princ-msg{0} @@B:Trm, '@encrypt{0} @@PKB:Trm ('@nonce-msg{0} @@nB:Trm)),
    'F{0} @fresh:Trm, @@L:Trm @@A:Trm @@nB:Trm, 'T_responder_Resp2{0} @@B:Trm @@L:Trm) => $union('@TERMINATED-2{0} @@B:Trm,
    'F{0} @fresh':Trm) if @fresh':Trm := @fresh:Trm .
@@A:Trm --> '@A{0}
@@B:Trm --> '@B{0}
@@PKB:Trm --> '@pkB{0}
@@nB:Trm --> 'FRESH{0} '@nonce{0} ('suc{0} ('suc{0} ('suc{0} '0{0})))
@fresh:Trm --> 'suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0})))
@@L:Trm --> 'FRESH{0} ({'_ : '@princ{0}} {'_ : '@nonce{0}} '@state{0}) ('suc{0} ('suc{0} '0{0}))
@fresh':Trm --> 'suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0})))
Old: $union('@N{0} $@&('@princ-msg{0} '@A{0}, '@princ-msg{0} '@B{0}, '@encrypt{0} '@pkB{0} ('@nonce-msg{0} ('FRESH{0}
    '@nonce{0} ('suc{0} ('suc{0} ('suc{0} '0{0})))))), '@TERMINATED-1{0} '@A{0}, 'F{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0}
    '0{0})))), 'EL{0} '@princ{0} '@A{0}, 'EL{0} '@princ{0} '@B{0}, 'EL{0} ('@pubK{0} '@A{0}) '@pkA{0}, 'EL{0} ('@pubK{0}
    '@B{0}) '@pkB{0}, 'T_responder_Resp2{0} '@B{0} ('FRESH{0} ({'_ : '@princ{0}} {'_ : '@nonce{0}} '@state{0}) ('suc{0} (
    'suc{0} '0{0}))), 'FRESH{0} ({'_ : '@princ{0}} {'_ : '@nonce{0}} '@state{0}) ('suc{0} ('suc{0} '0{0})) '@A{0} ('FRESH{
    0} '@nonce{0} ('suc{0} ('suc{0} ('suc{0} '0{0})))))
$union('@N{0} $@&('@princ-msg{0} '@A{0}, '@princ-msg{0} '@B{0}, '@encrypt{0} '@pkB{0} ('@nonce-msg{0} ('FRESH{0} '@nonce{0}
    ('suc{0} ('suc{0} ('suc{0} '0{0})))))), '@TERMINATED-1{0} '@A{0}, 'F{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0})))),
    'EL{0} '@princ{0} '@A{0}, 'EL{0} '@princ{0} '@B{0}, 'EL{0} ('@pubK{0} '@A{0}) '@pkA{0}, 'EL{0} ('@pubK{0} '@B{0})
    '@pkB{0}, 'T_responder_Resp2{0} '@B{0} ('FRESH{0} ({'_ : '@princ{0}} {'_ : '@nonce{0}} '@state{0}) ('suc{0} ('suc{0}
    '0{0}))), 'FRESH{0} ({'_ : '@princ{0}} {'_ : '@nonce{0}} '@state{0}) ('suc{0} ('suc{0} '0{0})) '@A{0} ('FRESH{0}
    '@nonce{0} ('suc{0} ('suc{0} ('suc{0} '0{0})))))
--->
$union($union('@TERMINATED-1{0} '@A{0}, 'EL{0} '@princ{0} '@A{0}, 'EL{0} '@princ{0} '@B{0}, 'EL{0} ('@pubK{0} '@A{0})
    '@pkA{0}, 'EL{0} ('@pubK{0} '@B{0}) '@pkB{0}), $union('@TERMINATED-2{0} '@B{0}, 'F{0} ('suc{0} ('suc{0} ('suc{0} ('suc{
    0} '0{0}))))))
New: $union($union('@TERMINATED-1{0} '@A{0}, 'EL{0} '@princ{0} '@A{0}, 'EL{0} '@princ{0} '@B{0}, 'EL{0} ('@pubK{0} '@A{0})
    '@pkA{0}, 'EL{0} ('@pubK{0} '@B{0}) '@pkB{0}), $union('@TERMINATED-2{0} '@B{0}, 'F{0} ('suc{0} ('suc{0} ('suc{0} ('suc{
    0} '0{0}))))))
rewrites: 11 in 21ms cpu (122ms real) (500 rewrites/second)
result Trm: $union('@TERMINATED-1{0} '@A{0}, '@TERMINATED-2{0} '@B{0}, 'F{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0})))),
    'EL{0} '@princ{0} '@A{0}, 'EL{0} '@princ{0} '@B{0}, 'EL{0} ('@pubK{0} '@A{0}) '@pkA{0}, 'EL{0} ('@pubK{0} '@B{0})
    '@pkB{0})
Maude>