Maude> rew 'config{0}.
rewrite in CTXT : 'config{0} .
rewrites: 14 in 0ms cpu (1ms real) (14014 rewrites/second)
result Trm: $union('@TERMINATED-1{0} '@A{0}, '@TERMINATED-2{0} '@B{0}, '@TERMINATED-3{0} '@S{0}, 'F{0} ('suc{0} ('suc{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} '@princ{0}
    '@S{0}, 'EL{0} ('@ltK{0} '@A{0} '@S{0}) '@kAS{0}, 'EL{0} ('@ltK{0} '@B{0} '@S{0}) '@kBS{0})
Maude> set trace on .
Maude> rew 'config{0}.
rewrite in CTXT : 'config{0} .
rewrites: 14 in 1ms cpu (1ms real) (14000 rewrites/second)
result Trm: $union('@TERMINATED-1{0} '@A{0}, '@TERMINATED-2{0} '@B{0}, '@TERMINATED-3{0} '@S{0}, 'F{0} ('suc{0} ('suc{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} '@princ{0}
    '@S{0}, 'EL{0} ('@ltK{0} '@A{0} '@S{0}) '@kAS{0}, 'EL{0} ('@ltK{0} '@B{0} '@S{0}) '@kBS{0})
Maude> set trace select off .
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} ('union{0} ('EL{0} '@princ{0} '@S{0}) (
    'EL{0} '@princ{0} '@A{0})) ('EL{0} '@princ{0} '@B{0})) ('EL{0} ('@ltK{0} '@A{0} '@S{0}) '@kAS{0})) ('EL{0} ('@ltK{0}
    '@B{0} '@S{0}) '@kBS{0})) ('union{0} ('@START-1{0} '@A{0} '@B{0}) ('union{0} ('@START-2{0} '@B{0}) ('@START-3{0} '@S{
    0})))) .
empty substitution
Old: 'config{0}
'config{0}
--->
'union{0} ('F{0} '0{0}) ('union{0} ('union{0} ('union{0} ('union{0} ('union{0} ('EL{0} '@princ{0} '@S{0}) ('EL{0} '@princ{
    0} '@A{0})) ('EL{0} '@princ{0} '@B{0})) ('EL{0} ('@ltK{0} '@A{0} '@S{0}) '@kAS{0})) ('EL{0} ('@ltK{0} '@B{0} '@S{0})
    '@kBS{0})) ('union{0} ('@START-1{0} '@A{0} '@B{0}) ('union{0} ('@START-2{0} '@B{0}) ('@START-3{0} '@S{0}))))
New: 'union{0} ('F{0} '0{0}) ('union{0} ('union{0} ('union{0} ('union{0} ('union{0} ('EL{0} '@princ{0} '@S{0}) ('EL{0}
    '@princ{0} '@A{0})) ('EL{0} '@princ{0} '@B{0})) ('EL{0} ('@ltK{0} '@A{0} '@S{0}) '@kAS{0})) ('EL{0} ('@ltK{0} '@B{0}
    '@S{0}) '@kBS{0})) ('union{0} ('@START-1{0} '@A{0} '@B{0}) ('union{0} ('@START-2{0} '@B{0}) ('@START-3{0} '@S{0}))))
*********** equation
eq 'union{0} @1:Trm @2:Trm = $union(@1:Trm, @2:Trm) .
@1:Trm --> 'EL{0} '@princ{0} '@S{0}
@2:Trm --> 'EL{0} '@princ{0} '@A{0}
Old: 'union{0} ('F{0} '0{0}) ('union{0} ('union{0} ('union{0} ('union{0} ('union{0} ('EL{0} '@princ{0} '@S{0}) ('EL{0}
    '@princ{0} '@A{0})) ('EL{0} '@princ{0} '@B{0})) ('EL{0} ('@ltK{0} '@A{0} '@S{0}) '@kAS{0})) ('EL{0} ('@ltK{0} '@B{0}
    '@S{0}) '@kBS{0})) ('union{0} ('@START-1{0} '@A{0} '@B{0}) ('union{0} ('@START-2{0} '@B{0}) ('@START-3{0} '@S{0}))))
'union{0} ('EL{0} '@princ{0} '@S{0}) ('EL{0} '@princ{0} '@A{0})
--->
$union('EL{0} '@princ{0} '@S{0}, 'EL{0} '@princ{0} '@A{0})
New: 'union{0} ('F{0} '0{0}) ('union{0} ('union{0} ('union{0} ('union{0} $union('EL{0} '@princ{0} '@S{0}, 'EL{0} '@princ{0}
    '@A{0}) ('EL{0} '@princ{0} '@B{0})) ('EL{0} ('@ltK{0} '@A{0} '@S{0}) '@kAS{0})) ('EL{0} ('@ltK{0} '@B{0} '@S{0}) '@kBS{
    0})) ('union{0} ('@START-1{0} '@A{0} '@B{0}) ('union{0} ('@START-2{0} '@B{0}) ('@START-3{0} '@S{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} '@S{0})
@2:Trm --> 'EL{0} '@princ{0} '@B{0}
Old: 'union{0} ('F{0} '0{0}) ('union{0} ('union{0} ('union{0} ('union{0} $union('EL{0} '@princ{0} '@A{0}, 'EL{0} '@princ{0}
    '@S{0}) ('EL{0} '@princ{0} '@B{0})) ('EL{0} ('@ltK{0} '@A{0} '@S{0}) '@kAS{0})) ('EL{0} ('@ltK{0} '@B{0} '@S{0}) '@kBS{
    0})) ('union{0} ('@START-1{0} '@A{0} '@B{0}) ('union{0} ('@START-2{0} '@B{0}) ('@START-3{0} '@S{0}))))
'union{0} $union('EL{0} '@princ{0} '@A{0}, 'EL{0} '@princ{0} '@S{0}) ('EL{0} '@princ{0} '@B{0})
--->
$union($union('EL{0} '@princ{0} '@A{0}, 'EL{0} '@princ{0} '@S{0}), 'EL{0} '@princ{0} '@B{0})
New: 'union{0} ('F{0} '0{0}) ('union{0} ('union{0} ('union{0} $union($union('EL{0} '@princ{0} '@A{0}, 'EL{0} '@princ{0}
    '@S{0}), 'EL{0} '@princ{0} '@B{0}) ('EL{0} ('@ltK{0} '@A{0} '@S{0}) '@kAS{0})) ('EL{0} ('@ltK{0} '@B{0} '@S{0}) '@kBS{
    0})) ('union{0} ('@START-1{0} '@A{0} '@B{0}) ('union{0} ('@START-2{0} '@B{0}) ('@START-3{0} '@S{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} '@princ{0} '@S{0})
@2:Trm --> 'EL{0} ('@ltK{0} '@A{0} '@S{0}) '@kAS{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} '@princ{0} '@S{0}) ('EL{0} ('@ltK{0} '@A{0} '@S{0}) '@kAS{0})) ('EL{0} ('@ltK{0} '@B{0} '@S{0}) '@kBS{0})) (
    'union{0} ('@START-1{0} '@A{0} '@B{0}) ('union{0} ('@START-2{0} '@B{0}) ('@START-3{0} '@S{0}))))
'union{0} $union('EL{0} '@princ{0} '@A{0}, 'EL{0} '@princ{0} '@B{0}, 'EL{0} '@princ{0} '@S{0}) ('EL{0} ('@ltK{0} '@A{0}
    '@S{0}) '@kAS{0})
--->
$union($union('EL{0} '@princ{0} '@A{0}, 'EL{0} '@princ{0} '@B{0}, 'EL{0} '@princ{0} '@S{0}), 'EL{0} ('@ltK{0} '@A{0} '@S{
    0}) '@kAS{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}
    '@princ{0} '@S{0}), 'EL{0} ('@ltK{0} '@A{0} '@S{0}) '@kAS{0}) ('EL{0} ('@ltK{0} '@B{0} '@S{0}) '@kBS{0})) ('union{0} (
    '@START-1{0} '@A{0} '@B{0}) ('union{0} ('@START-2{0} '@B{0}) ('@START-3{0} '@S{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} '@princ{0} '@S{0}, 'EL{0} ('@ltK{0} '@A{0}
    '@S{0}) '@kAS{0})
@2:Trm --> 'EL{0} ('@ltK{0} '@B{0} '@S{0}) '@kBS{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}
    '@princ{0} '@S{0}, 'EL{0} ('@ltK{0} '@A{0} '@S{0}) '@kAS{0}) ('EL{0} ('@ltK{0} '@B{0} '@S{0}) '@kBS{0})) ('union{0} (
    '@START-1{0} '@A{0} '@B{0}) ('union{0} ('@START-2{0} '@B{0}) ('@START-3{0} '@S{0}))))
'union{0} $union('EL{0} '@princ{0} '@A{0}, 'EL{0} '@princ{0} '@B{0}, 'EL{0} '@princ{0} '@S{0}, 'EL{0} ('@ltK{0} '@A{0} '@S{
    0}) '@kAS{0}) ('EL{0} ('@ltK{0} '@B{0} '@S{0}) '@kBS{0})
--->
$union($union('EL{0} '@princ{0} '@A{0}, 'EL{0} '@princ{0} '@B{0}, 'EL{0} '@princ{0} '@S{0}, 'EL{0} ('@ltK{0} '@A{0} '@S{0})
    '@kAS{0}), 'EL{0} ('@ltK{0} '@B{0} '@S{0}) '@kBS{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} '@princ{0}
    '@S{0}, 'EL{0} ('@ltK{0} '@A{0} '@S{0}) '@kAS{0}), 'EL{0} ('@ltK{0} '@B{0} '@S{0}) '@kBS{0}) ('union{0} ('@START-1{0}
    '@A{0} '@B{0}) ('union{0} ('@START-2{0} '@B{0}) ('@START-3{0} '@S{0}))))
*********** equation
eq 'union{0} @1:Trm @2:Trm = $union(@1:Trm, @2:Trm) .
@1:Trm --> '@START-2{0} '@B{0}
@2:Trm --> '@START-3{0} '@S{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} '@princ{0} '@S{
    0}, 'EL{0} ('@ltK{0} '@A{0} '@S{0}) '@kAS{0}, 'EL{0} ('@ltK{0} '@B{0} '@S{0}) '@kBS{0}) ('union{0} ('@START-1{0} '@A{0}
    '@B{0}) ('union{0} ('@START-2{0} '@B{0}) ('@START-3{0} '@S{0}))))
'union{0} ('@START-2{0} '@B{0}) ('@START-3{0} '@S{0})
--->
$union('@START-2{0} '@B{0}, '@START-3{0} '@S{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} '@princ{0} '@S{
    0}, 'EL{0} ('@ltK{0} '@A{0} '@S{0}) '@kAS{0}, 'EL{0} ('@ltK{0} '@B{0} '@S{0}) '@kBS{0}) ('union{0} ('@START-1{0} '@A{0}
    '@B{0}) $union('@START-2{0} '@B{0}, '@START-3{0} '@S{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 --> $union('@START-2{0} '@B{0}, '@START-3{0} '@S{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} '@princ{0} '@S{
    0}, 'EL{0} ('@ltK{0} '@A{0} '@S{0}) '@kAS{0}, 'EL{0} ('@ltK{0} '@B{0} '@S{0}) '@kBS{0}) ('union{0} ('@START-1{0} '@A{0}
    '@B{0}) $union('@START-2{0} '@B{0}, '@START-3{0} '@S{0})))
'union{0} ('@START-1{0} '@A{0} '@B{0}) $union('@START-2{0} '@B{0}, '@START-3{0} '@S{0})
--->
$union('@START-1{0} '@A{0} '@B{0}, $union('@START-2{0} '@B{0}, '@START-3{0} '@S{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} '@princ{0} '@S{
    0}, 'EL{0} ('@ltK{0} '@A{0} '@S{0}) '@kAS{0}, 'EL{0} ('@ltK{0} '@B{0} '@S{0}) '@kBS{0}) $union('@START-1{0} '@A{0} '@B{
    0}, $union('@START-2{0} '@B{0}, '@START-3{0} '@S{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} '@princ{0} '@S{0}, 'EL{0} ('@ltK{0} '@A{0}
    '@S{0}) '@kAS{0}, 'EL{0} ('@ltK{0} '@B{0} '@S{0}) '@kBS{0})
@2:Trm --> $union('@START-2{0} '@B{0}, '@START-3{0} '@S{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} '@princ{0} '@S{
    0}, 'EL{0} ('@ltK{0} '@A{0} '@S{0}) '@kAS{0}, 'EL{0} ('@ltK{0} '@B{0} '@S{0}) '@kBS{0}) $union('@START-2{0} '@B{0},
    '@START-3{0} '@S{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} '@princ{0} '@S{0}, 'EL{0} ('@ltK{0} '@A{0} '@S{
    0}) '@kAS{0}, 'EL{0} ('@ltK{0} '@B{0} '@S{0}) '@kBS{0}) $union('@START-2{0} '@B{0}, '@START-3{0} '@S{0}, '@START-1{0}
    '@A{0} '@B{0})
--->
$union($union('EL{0} '@princ{0} '@A{0}, 'EL{0} '@princ{0} '@B{0}, 'EL{0} '@princ{0} '@S{0}, 'EL{0} ('@ltK{0} '@A{0} '@S{0})
    '@kAS{0}, 'EL{0} ('@ltK{0} '@B{0} '@S{0}) '@kBS{0}), $union('@START-2{0} '@B{0}, '@START-3{0} '@S{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} '@princ{0} '@S{0},
    'EL{0} ('@ltK{0} '@A{0} '@S{0}) '@kAS{0}, 'EL{0} ('@ltK{0} '@B{0} '@S{0}) '@kBS{0}), $union('@START-2{0} '@B{0},
    '@START-3{0} '@S{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-3{0} '@S{0}, '@START-1{0} '@A{0} '@B{0}, 'EL{0} '@princ{0} '@A{0}, 'EL{0}
    '@princ{0} '@B{0}, 'EL{0} '@princ{0} '@S{0}, 'EL{0} ('@ltK{0} '@A{0} '@S{0}) '@kAS{0}, 'EL{0} ('@ltK{0} '@B{0} '@S{0})
    '@kBS{0})
Old: 'union{0} ('F{0} '0{0}) $union('@START-2{0} '@B{0}, '@START-3{0} '@S{0}, '@START-1{0} '@A{0} '@B{0}, 'EL{0} '@princ{0}
    '@A{0}, 'EL{0} '@princ{0} '@B{0}, 'EL{0} '@princ{0} '@S{0}, 'EL{0} ('@ltK{0} '@A{0} '@S{0}) '@kAS{0}, 'EL{0} ('@ltK{0}
    '@B{0} '@S{0}) '@kBS{0})
'union{0} ('F{0} '0{0}) $union('@START-2{0} '@B{0}, '@START-3{0} '@S{0}, '@START-1{0} '@A{0} '@B{0}, 'EL{0} '@princ{0} '@A{
    0}, 'EL{0} '@princ{0} '@B{0}, 'EL{0} '@princ{0} '@S{0}, 'EL{0} ('@ltK{0} '@A{0} '@S{0}) '@kAS{0}, 'EL{0} ('@ltK{0} '@B{
    0} '@S{0}) '@kBS{0})
--->
$union('F{0} '0{0}, $union('@START-2{0} '@B{0}, '@START-3{0} '@S{0}, '@START-1{0} '@A{0} '@B{0}, 'EL{0} '@princ{0} '@A{0},
    'EL{0} '@princ{0} '@B{0}, 'EL{0} '@princ{0} '@S{0}, 'EL{0} ('@ltK{0} '@A{0} '@S{0}) '@kAS{0}, 'EL{0} ('@ltK{0} '@B{0}
    '@S{0}) '@kBS{0}))
New: $union('F{0} '0{0}, $union('@START-2{0} '@B{0}, '@START-3{0} '@S{0}, '@START-1{0} '@A{0} '@B{0}, 'EL{0} '@princ{0}
    '@A{0}, 'EL{0} '@princ{0} '@B{0}, 'EL{0} '@princ{0} '@S{0}, 'EL{0} ('@ltK{0} '@A{0} '@S{0}) '@kAS{0}, 'EL{0} ('@ltK{0}
    '@B{0} '@S{0}) '@kBS{0}))
*********** trial #1
crl $union('F{0} @fresh:Trm, '@START-1{0} @@A:Trm @@B:Trm, 'EL{0} ('@ltK{0} @@A:Trm '@S{0}) @@kAS:Trm) => $union(@@L:Trm
    @@A:Trm @@B:Trm @@n:Trm @@nA:Trm, $union('T_initiator_Init2{0} @@A:Trm @@L:Trm, $union('EL{0} ('@ltK{0} @@A:Trm '@S{0})
    @@kAS:Trm, $union('@N{0} $@&($@&($@&('@nonce-msg{0} @@n:Trm, '@princ-msg{0} @@A:Trm), '@princ-msg{0} @@B:Trm),
    '@encrypt{0} ('@ltK-shK{0} @@kAS:Trm) $@&($@&($@&('@nonce-msg{0} @@nA:Trm, '@nonce-msg{0} @@n:Trm), '@princ-msg{0}
    @@A:Trm), '@princ-msg{0} @@B:Trm)), 'F{0} @fresh':Trm)))) if @@L:Trm := 'FRESH{0} ({'_ : '@princ{0}} {'_ : '@princ{0}}
    {'_ : '@nonce{0}} {'_ : '@nonce{0}} '@state{0}) @fresh:Trm /\ @@n:Trm := 'FRESH{0} '@nonce{0} ('suc{0} @fresh:Trm) /\
    @@nA:Trm := 'FRESH{0} '@nonce{0} ('suc{0} ('suc{0} @fresh:Trm)) /\ @fresh':Trm := 'suc{0} ('suc{0} ('suc{0}
    @fresh:Trm)) .
@fresh:Trm --> '0{0}
@@A:Trm --> '@A{0}
@@B:Trm --> '@B{0}
@@kAS:Trm --> '@kAS{0}
@@L:Trm --> (unbound)
@@n:Trm --> (unbound)
@@nA:Trm --> (unbound)
@fresh':Trm --> (unbound)
*********** solving condition fragment
@@L:Trm := 'FRESH{0} ({'_ : '@princ{0}} {'_ : '@princ{0}} {'_ : '@nonce{0}} {'_ : '@nonce{0}} '@state{0}) @fresh:Trm
*********** success for condition fragment
@@L:Trm := 'FRESH{0} ({'_ : '@princ{0}} {'_ : '@princ{0}} {'_ : '@nonce{0}} {'_ : '@nonce{0}} '@state{0}) @fresh:Trm
@fresh:Trm --> '0{0}
@@A:Trm --> '@A{0}
@@B:Trm --> '@B{0}
@@kAS:Trm --> '@kAS{0}
@@L:Trm --> 'FRESH{0} ({'_ : '@princ{0}} {'_ : '@princ{0}} {'_ : '@nonce{0}} {'_ : '@nonce{0}} '@state{0}) '0{0}
@@n:Trm --> (unbound)
@@nA:Trm --> (unbound)
@fresh':Trm --> (unbound)
*********** solving condition fragment
@@n:Trm := 'FRESH{0} '@nonce{0} ('suc{0} @fresh:Trm)
*********** success for condition fragment
@@n:Trm := 'FRESH{0} '@nonce{0} ('suc{0} @fresh:Trm)
@fresh:Trm --> '0{0}
@@A:Trm --> '@A{0}
@@B:Trm --> '@B{0}
@@kAS:Trm --> '@kAS{0}
@@L:Trm --> 'FRESH{0} ({'_ : '@princ{0}} {'_ : '@princ{0}} {'_ : '@nonce{0}} {'_ : '@nonce{0}} '@state{0}) '0{0}
@@n:Trm --> 'FRESH{0} '@nonce{0} ('suc{0} '0{0})
@@nA:Trm --> (unbound)
@fresh':Trm --> (unbound)
*********** solving condition fragment
@@nA:Trm := 'FRESH{0} '@nonce{0} ('suc{0} ('suc{0} @fresh:Trm))
*********** success for condition fragment
@@nA:Trm := 'FRESH{0} '@nonce{0} ('suc{0} ('suc{0} @fresh:Trm))
@fresh:Trm --> '0{0}
@@A:Trm --> '@A{0}
@@B:Trm --> '@B{0}
@@kAS:Trm --> '@kAS{0}
@@L:Trm --> 'FRESH{0} ({'_ : '@princ{0}} {'_ : '@princ{0}} {'_ : '@nonce{0}} {'_ : '@nonce{0}} '@state{0}) '0{0}
@@n:Trm --> 'FRESH{0} '@nonce{0} ('suc{0} '0{0})
@@nA:Trm --> 'FRESH{0} '@nonce{0} ('suc{0} ('suc{0} '0{0}))
@fresh':Trm --> (unbound)
*********** solving condition fragment
@fresh':Trm := 'suc{0} ('suc{0} ('suc{0} @fresh:Trm))
*********** success for condition fragment
@fresh':Trm := 'suc{0} ('suc{0} ('suc{0} @fresh:Trm))
@fresh:Trm --> '0{0}
@@A:Trm --> '@A{0}
@@B:Trm --> '@B{0}
@@kAS:Trm --> '@kAS{0}
@@L:Trm --> 'FRESH{0} ({'_ : '@princ{0}} {'_ : '@princ{0}} {'_ : '@nonce{0}} {'_ : '@nonce{0}} '@state{0}) '0{0}
@@n:Trm --> 'FRESH{0} '@nonce{0} ('suc{0} '0{0})
@@nA:Trm --> 'FRESH{0} '@nonce{0} ('suc{0} ('suc{0} '0{0}))
@fresh':Trm --> 'suc{0} ('suc{0} ('suc{0} '0{0}))
*********** success #1
*********** rule
crl $union('F{0} @fresh:Trm, '@START-1{0} @@A:Trm @@B:Trm, 'EL{0} ('@ltK{0} @@A:Trm '@S{0}) @@kAS:Trm) => $union(@@L:Trm
    @@A:Trm @@B:Trm @@n:Trm @@nA:Trm, $union('T_initiator_Init2{0} @@A:Trm @@L:Trm, $union('EL{0} ('@ltK{0} @@A:Trm '@S{0})
    @@kAS:Trm, $union('@N{0} $@&($@&($@&('@nonce-msg{0} @@n:Trm, '@princ-msg{0} @@A:Trm), '@princ-msg{0} @@B:Trm),
    '@encrypt{0} ('@ltK-shK{0} @@kAS:Trm) $@&($@&($@&('@nonce-msg{0} @@nA:Trm, '@nonce-msg{0} @@n:Trm), '@princ-msg{0}
    @@A:Trm), '@princ-msg{0} @@B:Trm)), 'F{0} @fresh':Trm)))) if @@L:Trm := 'FRESH{0} ({'_ : '@princ{0}} {'_ : '@princ{0}}
    {'_ : '@nonce{0}} {'_ : '@nonce{0}} '@state{0}) @fresh:Trm /\ @@n:Trm := 'FRESH{0} '@nonce{0} ('suc{0} @fresh:Trm) /\
    @@nA:Trm := 'FRESH{0} '@nonce{0} ('suc{0} ('suc{0} @fresh:Trm)) /\ @fresh':Trm := 'suc{0} ('suc{0} ('suc{0}
    @fresh:Trm)) .
@fresh:Trm --> '0{0}
@@A:Trm --> '@A{0}
@@B:Trm --> '@B{0}
@@kAS:Trm --> '@kAS{0}
@@L:Trm --> 'FRESH{0} ({'_ : '@princ{0}} {'_ : '@princ{0}} {'_ : '@nonce{0}} {'_ : '@nonce{0}} '@state{0}) '0{0}
@@n:Trm --> 'FRESH{0} '@nonce{0} ('suc{0} '0{0})
@@nA:Trm --> 'FRESH{0} '@nonce{0} ('suc{0} ('suc{0} '0{0}))
@fresh':Trm --> 'suc{0} ('suc{0} ('suc{0} '0{0}))
Old: $union('@START-2{0} '@B{0}, '@START-3{0} '@S{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} '@princ{0} '@S{0}, 'EL{0} ('@ltK{0} '@A{0} '@S{0}) '@kAS{0}, 'EL{0} ('@ltK{0} '@B{0}
    '@S{0}) '@kBS{0})
$union('@START-2{0} '@B{0}, '@START-3{0} '@S{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} '@princ{0} '@S{0}, 'EL{0} ('@ltK{0} '@A{0} '@S{0}) '@kAS{0}, 'EL{0} ('@ltK{0} '@B{0} '@S{0})
    '@kBS{0})
--->
$union($union('@START-2{0} '@B{0}, '@START-3{0} '@S{0}, 'EL{0} '@princ{0} '@A{0}, 'EL{0} '@princ{0} '@B{0}, 'EL{0} '@princ{
    0} '@S{0}, 'EL{0} ('@ltK{0} '@B{0} '@S{0}) '@kBS{0}), $union('FRESH{0} ({'_ : '@princ{0}} {'_ : '@princ{0}} {'_ :
    '@nonce{0}} {'_ : '@nonce{0}} '@state{0}) '0{0} '@A{0} '@B{0} ('FRESH{0} '@nonce{0} ('suc{0} '0{0})) ('FRESH{0}
    '@nonce{0} ('suc{0} ('suc{0} '0{0}))), $union('T_initiator_Init2{0} '@A{0} ('FRESH{0} ({'_ : '@princ{0}} {'_ : '@princ{
    0}} {'_ : '@nonce{0}} {'_ : '@nonce{0}} '@state{0}) '0{0}), $union('EL{0} ('@ltK{0} '@A{0} '@S{0}) '@kAS{0}, $union(
    '@N{0} $@&($@&($@&('@nonce-msg{0} ('FRESH{0} '@nonce{0} ('suc{0} '0{0})), '@princ-msg{0} '@A{0}), '@princ-msg{0} '@B{
    0}), '@encrypt{0} ('@ltK-shK{0} '@kAS{0}) $@&($@&($@&('@nonce-msg{0} ('FRESH{0} '@nonce{0} ('suc{0} ('suc{0} '0{0}))),
    '@nonce-msg{0} ('FRESH{0} '@nonce{0} ('suc{0} '0{0}))), '@princ-msg{0} '@A{0}), '@princ-msg{0} '@B{0})), 'F{0} ('suc{0}
    ('suc{0} ('suc{0} '0{0}))))))))
New: $union($union('@START-2{0} '@B{0}, '@START-3{0} '@S{0}, 'EL{0} '@princ{0} '@A{0}, 'EL{0} '@princ{0} '@B{0}, 'EL{0}
    '@princ{0} '@S{0}, 'EL{0} ('@ltK{0} '@B{0} '@S{0}) '@kBS{0}), $union('FRESH{0} ({'_ : '@princ{0}} {'_ : '@princ{0}} {'_
    : '@nonce{0}} {'_ : '@nonce{0}} '@state{0}) '0{0} '@A{0} '@B{0} ('FRESH{0} '@nonce{0} ('suc{0} '0{0})) ('FRESH{0}
    '@nonce{0} ('suc{0} ('suc{0} '0{0}))), $union('T_initiator_Init2{0} '@A{0} ('FRESH{0} ({'_ : '@princ{0}} {'_ : '@princ{
    0}} {'_ : '@nonce{0}} {'_ : '@nonce{0}} '@state{0}) '0{0}), $union('EL{0} ('@ltK{0} '@A{0} '@S{0}) '@kAS{0}, $union(
    '@N{0} $@&($@&($@&('@nonce-msg{0} ('FRESH{0} '@nonce{0} ('suc{0} '0{0})), '@princ-msg{0} '@A{0}), '@princ-msg{0} '@B{
    0}), '@encrypt{0} ('@ltK-shK{0} '@kAS{0}) $@&($@&($@&('@nonce-msg{0} ('FRESH{0} '@nonce{0} ('suc{0} ('suc{0} '0{0}))),
    '@nonce-msg{0} ('FRESH{0} '@nonce{0} ('suc{0} '0{0}))), '@princ-msg{0} '@A{0}), '@princ-msg{0} '@B{0})), 'F{0} ('suc{0}
    ('suc{0} ('suc{0} '0{0}))))))))
*********** trial #2
crl $union('@N{0} $@&('@nonce-msg{0} @@n:Trm, '@princ-msg{0} @@A:Trm, '@princ-msg{0} @@B:Trm, @@X:Trm), '@START-2{0}
    @@B:Trm, 'F{0} @fresh:Trm, 'EL{0} ('@ltK{0} @@B:Trm '@S{0}) @@kBS:Trm) => $union(@@L:Trm @@B:Trm @@A:Trm @@n:Trm
    @@nB:Trm @@kBS:Trm, $union('T_responder_Resp2{0} @@B:Trm @@L:Trm, $union('EL{0} ('@ltK{0} @@B:Trm '@S{0}) @@kBS:Trm,
    $union('@N{0} $@&($@&($@&($@&('@nonce-msg{0} @@n:Trm, '@princ-msg{0} @@A:Trm), '@princ-msg{0} @@B:Trm), @@X:Trm),
    '@encrypt{0} ('@ltK-shK{0} @@kBS:Trm) $@&($@&($@&('@nonce-msg{0} @@nB:Trm, '@nonce-msg{0} @@n:Trm), '@princ-msg{0}
    @@A:Trm), '@princ-msg{0} @@B:Trm)), 'F{0} @fresh':Trm)))) if @@L:Trm := 'FRESH{0} ({'@B : '@princ{0}} {'_ : '@princ{0}}
    {'_ : '@nonce{0}} {'_ : '@nonce{0}} {'_ : '@ltK{0} @@B:Trm '@S{0}} '@state{0}) @fresh:Trm /\ @@nB:Trm := 'FRESH{0}
    '@nonce{0} ('suc{0} @fresh:Trm) /\ @fresh':Trm := 'suc{0} ('suc{0} @fresh:Trm) .
@@n:Trm --> 'FRESH{0} '@nonce{0} ('suc{0} '0{0})
@@A:Trm --> '@A{0}
@@B:Trm --> '@B{0}
@@X:Trm --> '@encrypt{0} ('@ltK-shK{0} '@kAS{0}) $@&('@nonce-msg{0} ('FRESH{0} '@nonce{0} ('suc{0} ('suc{0} '0{0}))),
    '@nonce-msg{0} ('FRESH{0} '@nonce{0} ('suc{0} '0{0})), '@princ-msg{0} '@A{0}, '@princ-msg{0} '@B{0})
@fresh:Trm --> 'suc{0} ('suc{0} ('suc{0} '0{0}))
@@kBS:Trm --> '@kBS{0}
@@L:Trm --> (unbound)
@@nB:Trm --> (unbound)
@fresh':Trm --> (unbound)
*********** solving condition fragment
@@L:Trm := 'FRESH{0} ({'@B : '@princ{0}} {'_ : '@princ{0}} {'_ : '@nonce{0}} {'_ : '@nonce{0}} {'_ : '@ltK{0} @@B:Trm '@S{
    0}} '@state{0}) @fresh:Trm
*********** success for condition fragment
@@L:Trm := 'FRESH{0} ({'@B : '@princ{0}} {'_ : '@princ{0}} {'_ : '@nonce{0}} {'_ : '@nonce{0}} {'_ : '@ltK{0} @@B:Trm '@S{
    0}} '@state{0}) @fresh:Trm
@@n:Trm --> 'FRESH{0} '@nonce{0} ('suc{0} '0{0})
@@A:Trm --> '@A{0}
@@B:Trm --> '@B{0}
@@X:Trm --> '@encrypt{0} ('@ltK-shK{0} '@kAS{0}) $@&('@nonce-msg{0} ('FRESH{0} '@nonce{0} ('suc{0} ('suc{0} '0{0}))),
    '@nonce-msg{0} ('FRESH{0} '@nonce{0} ('suc{0} '0{0})), '@princ-msg{0} '@A{0}, '@princ-msg{0} '@B{0})
@fresh:Trm --> 'suc{0} ('suc{0} ('suc{0} '0{0}))
@@kBS:Trm --> '@kBS{0}
@@L:Trm --> 'FRESH{0} ({'@B : '@princ{0}} {'_ : '@princ{0}} {'_ : '@nonce{0}} {'_ : '@nonce{0}} {'_ : '@ltK{0} '@B{0} '@S{
    0}} '@state{0}) ('suc{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)
@@n:Trm --> 'FRESH{0} '@nonce{0} ('suc{0} '0{0})
@@A:Trm --> '@A{0}
@@B:Trm --> '@B{0}
@@X:Trm --> '@encrypt{0} ('@ltK-shK{0} '@kAS{0}) $@&('@nonce-msg{0} ('FRESH{0} '@nonce{0} ('suc{0} ('suc{0} '0{0}))),
    '@nonce-msg{0} ('FRESH{0} '@nonce{0} ('suc{0} '0{0})), '@princ-msg{0} '@A{0}, '@princ-msg{0} '@B{0})
@fresh:Trm --> 'suc{0} ('suc{0} ('suc{0} '0{0}))
@@kBS:Trm --> '@kBS{0}
@@L:Trm --> 'FRESH{0} ({'@B : '@princ{0}} {'_ : '@princ{0}} {'_ : '@nonce{0}} {'_ : '@nonce{0}} {'_ : '@ltK{0} '@B{0} '@S{
    0}} '@state{0}) ('suc{0} ('suc{0} ('suc{0} '0{0})))
@@nB:Trm --> 'FRESH{0} '@nonce{0} ('suc{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)
@@n:Trm --> 'FRESH{0} '@nonce{0} ('suc{0} '0{0})
@@A:Trm --> '@A{0}
@@B:Trm --> '@B{0}
@@X:Trm --> '@encrypt{0} ('@ltK-shK{0} '@kAS{0}) $@&('@nonce-msg{0} ('FRESH{0} '@nonce{0} ('suc{0} ('suc{0} '0{0}))),
    '@nonce-msg{0} ('FRESH{0} '@nonce{0} ('suc{0} '0{0})), '@princ-msg{0} '@A{0}, '@princ-msg{0} '@B{0})
@fresh:Trm --> 'suc{0} ('suc{0} ('suc{0} '0{0}))
@@kBS:Trm --> '@kBS{0}
@@L:Trm --> 'FRESH{0} ({'@B : '@princ{0}} {'_ : '@princ{0}} {'_ : '@nonce{0}} {'_ : '@nonce{0}} {'_ : '@ltK{0} '@B{0} '@S{
    0}} '@state{0}) ('suc{0} ('suc{0} ('suc{0} '0{0})))
@@nB:Trm --> 'FRESH{0} '@nonce{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0}))))
@fresh':Trm --> 'suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0}))))
*********** success #2
*********** rule
crl $union('@N{0} $@&('@nonce-msg{0} @@n:Trm, '@princ-msg{0} @@A:Trm, '@princ-msg{0} @@B:Trm, @@X:Trm), '@START-2{0}
    @@B:Trm, 'F{0} @fresh:Trm, 'EL{0} ('@ltK{0} @@B:Trm '@S{0}) @@kBS:Trm) => $union(@@L:Trm @@B:Trm @@A:Trm @@n:Trm
    @@nB:Trm @@kBS:Trm, $union('T_responder_Resp2{0} @@B:Trm @@L:Trm, $union('EL{0} ('@ltK{0} @@B:Trm '@S{0}) @@kBS:Trm,
    $union('@N{0} $@&($@&($@&($@&('@nonce-msg{0} @@n:Trm, '@princ-msg{0} @@A:Trm), '@princ-msg{0} @@B:Trm), @@X:Trm),
    '@encrypt{0} ('@ltK-shK{0} @@kBS:Trm) $@&($@&($@&('@nonce-msg{0} @@nB:Trm, '@nonce-msg{0} @@n:Trm), '@princ-msg{0}
    @@A:Trm), '@princ-msg{0} @@B:Trm)), 'F{0} @fresh':Trm)))) if @@L:Trm := 'FRESH{0} ({'@B : '@princ{0}} {'_ : '@princ{0}}
    {'_ : '@nonce{0}} {'_ : '@nonce{0}} {'_ : '@ltK{0} @@B:Trm '@S{0}} '@state{0}) @fresh:Trm /\ @@nB:Trm := 'FRESH{0}
    '@nonce{0} ('suc{0} @fresh:Trm) /\ @fresh':Trm := 'suc{0} ('suc{0} @fresh:Trm) .
@@n:Trm --> 'FRESH{0} '@nonce{0} ('suc{0} '0{0})
@@A:Trm --> '@A{0}
@@B:Trm --> '@B{0}
@@X:Trm --> '@encrypt{0} ('@ltK-shK{0} '@kAS{0}) $@&('@nonce-msg{0} ('FRESH{0} '@nonce{0} ('suc{0} ('suc{0} '0{0}))),
    '@nonce-msg{0} ('FRESH{0} '@nonce{0} ('suc{0} '0{0})), '@princ-msg{0} '@A{0}, '@princ-msg{0} '@B{0})
@fresh:Trm --> 'suc{0} ('suc{0} ('suc{0} '0{0}))
@@kBS:Trm --> '@kBS{0}
@@L:Trm --> 'FRESH{0} ({'@B : '@princ{0}} {'_ : '@princ{0}} {'_ : '@nonce{0}} {'_ : '@nonce{0}} {'_ : '@ltK{0} '@B{0} '@S{
    0}} '@state{0}) ('suc{0} ('suc{0} ('suc{0} '0{0})))
@@nB:Trm --> 'FRESH{0} '@nonce{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0}))))
@fresh':Trm --> 'suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0}))))
Old: $union('@N{0} $@&('@nonce-msg{0} ('FRESH{0} '@nonce{0} ('suc{0} '0{0})), '@princ-msg{0} '@A{0}, '@princ-msg{0} '@B{0},
    '@encrypt{0} ('@ltK-shK{0} '@kAS{0}) $@&('@nonce-msg{0} ('FRESH{0} '@nonce{0} ('suc{0} ('suc{0} '0{0}))), '@nonce-msg{
    0} ('FRESH{0} '@nonce{0} ('suc{0} '0{0})), '@princ-msg{0} '@A{0}, '@princ-msg{0} '@B{0})), '@START-2{0} '@B{0},
    '@START-3{0} '@S{0}, 'F{0} ('suc{0} ('suc{0} ('suc{0} '0{0}))), 'EL{0} '@princ{0} '@A{0}, 'EL{0} '@princ{0} '@B{0},
    'EL{0} '@princ{0} '@S{0}, 'EL{0} ('@ltK{0} '@A{0} '@S{0}) '@kAS{0}, 'EL{0} ('@ltK{0} '@B{0} '@S{0}) '@kBS{0},
    'T_initiator_Init2{0} '@A{0} ('FRESH{0} ({'_ : '@princ{0}} {'_ : '@princ{0}} {'_ : '@nonce{0}} {'_ : '@nonce{0}}
    '@state{0}) '0{0}), 'FRESH{0} ({'_ : '@princ{0}} {'_ : '@princ{0}} {'_ : '@nonce{0}} {'_ : '@nonce{0}} '@state{0}) '0{
    0} '@A{0} '@B{0} ('FRESH{0} '@nonce{0} ('suc{0} '0{0})) ('FRESH{0} '@nonce{0} ('suc{0} ('suc{0} '0{0}))))
$union('@N{0} $@&('@nonce-msg{0} ('FRESH{0} '@nonce{0} ('suc{0} '0{0})), '@princ-msg{0} '@A{0}, '@princ-msg{0} '@B{0},
    '@encrypt{0} ('@ltK-shK{0} '@kAS{0}) $@&('@nonce-msg{0} ('FRESH{0} '@nonce{0} ('suc{0} ('suc{0} '0{0}))), '@nonce-msg{
    0} ('FRESH{0} '@nonce{0} ('suc{0} '0{0})), '@princ-msg{0} '@A{0}, '@princ-msg{0} '@B{0})), '@START-2{0} '@B{0},
    '@START-3{0} '@S{0}, 'F{0} ('suc{0} ('suc{0} ('suc{0} '0{0}))), 'EL{0} '@princ{0} '@A{0}, 'EL{0} '@princ{0} '@B{0},
    'EL{0} '@princ{0} '@S{0}, 'EL{0} ('@ltK{0} '@A{0} '@S{0}) '@kAS{0}, 'EL{0} ('@ltK{0} '@B{0} '@S{0}) '@kBS{0},
    'T_initiator_Init2{0} '@A{0} ('FRESH{0} ({'_ : '@princ{0}} {'_ : '@princ{0}} {'_ : '@nonce{0}} {'_ : '@nonce{0}}
    '@state{0}) '0{0}), 'FRESH{0} ({'_ : '@princ{0}} {'_ : '@princ{0}} {'_ : '@nonce{0}} {'_ : '@nonce{0}} '@state{0}) '0{
    0} '@A{0} '@B{0} ('FRESH{0} '@nonce{0} ('suc{0} '0{0})) ('FRESH{0} '@nonce{0} ('suc{0} ('suc{0} '0{0}))))
--->
$union($union('@START-3{0} '@S{0}, 'EL{0} '@princ{0} '@A{0}, 'EL{0} '@princ{0} '@B{0}, 'EL{0} '@princ{0} '@S{0}, 'EL{0} (
    '@ltK{0} '@A{0} '@S{0}) '@kAS{0}, 'T_initiator_Init2{0} '@A{0} ('FRESH{0} ({'_ : '@princ{0}} {'_ : '@princ{0}} {'_ :
    '@nonce{0}} {'_ : '@nonce{0}} '@state{0}) '0{0}), 'FRESH{0} ({'_ : '@princ{0}} {'_ : '@princ{0}} {'_ : '@nonce{0}} {'_
    : '@nonce{0}} '@state{0}) '0{0} '@A{0} '@B{0} ('FRESH{0} '@nonce{0} ('suc{0} '0{0})) ('FRESH{0} '@nonce{0} ('suc{0} (
    'suc{0} '0{0})))), $union('FRESH{0} ({'@B : '@princ{0}} {'_ : '@princ{0}} {'_ : '@nonce{0}} {'_ : '@nonce{0}} {'_ :
    '@ltK{0} '@B{0} '@S{0}} '@state{0}) ('suc{0} ('suc{0} ('suc{0} '0{0}))) '@B{0} '@A{0} ('FRESH{0} '@nonce{0} ('suc{0}
    '0{0})) ('FRESH{0} '@nonce{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0}))))) '@kBS{0}, $union('T_responder_Resp2{0}
    '@B{0} ('FRESH{0} ({'@B : '@princ{0}} {'_ : '@princ{0}} {'_ : '@nonce{0}} {'_ : '@nonce{0}} {'_ : '@ltK{0} '@B{0} '@S{
    0}} '@state{0}) ('suc{0} ('suc{0} ('suc{0} '0{0})))), $union('EL{0} ('@ltK{0} '@B{0} '@S{0}) '@kBS{0}, $union('@N{0}
    $@&($@&($@&($@&('@nonce-msg{0} ('FRESH{0} '@nonce{0} ('suc{0} '0{0})), '@princ-msg{0} '@A{0}), '@princ-msg{0} '@B{0}),
    '@encrypt{0} ('@ltK-shK{0} '@kAS{0}) $@&('@nonce-msg{0} ('FRESH{0} '@nonce{0} ('suc{0} ('suc{0} '0{0}))), '@nonce-msg{
    0} ('FRESH{0} '@nonce{0} ('suc{0} '0{0})), '@princ-msg{0} '@A{0}, '@princ-msg{0} '@B{0})), '@encrypt{0} ('@ltK-shK{0}
    '@kBS{0}) $@&($@&($@&('@nonce-msg{0} ('FRESH{0} '@nonce{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0}))))), '@nonce-msg{
    0} ('FRESH{0} '@nonce{0} ('suc{0} '0{0}))), '@princ-msg{0} '@A{0}), '@princ-msg{0} '@B{0})), 'F{0} ('suc{0} ('suc{0} (
    'suc{0} ('suc{0} ('suc{0} '0{0}))))))))))
New: $union($union('@START-3{0} '@S{0}, 'EL{0} '@princ{0} '@A{0}, 'EL{0} '@princ{0} '@B{0}, 'EL{0} '@princ{0} '@S{0}, 'EL{
    0} ('@ltK{0} '@A{0} '@S{0}) '@kAS{0}, 'T_initiator_Init2{0} '@A{0} ('FRESH{0} ({'_ : '@princ{0}} {'_ : '@princ{0}} {'_
    : '@nonce{0}} {'_ : '@nonce{0}} '@state{0}) '0{0}), 'FRESH{0} ({'_ : '@princ{0}} {'_ : '@princ{0}} {'_ : '@nonce{0}} {
    '_ : '@nonce{0}} '@state{0}) '0{0} '@A{0} '@B{0} ('FRESH{0} '@nonce{0} ('suc{0} '0{0})) ('FRESH{0} '@nonce{0} ('suc{0}
    ('suc{0} '0{0})))), $union('FRESH{0} ({'@B : '@princ{0}} {'_ : '@princ{0}} {'_ : '@nonce{0}} {'_ : '@nonce{0}} {'_ :
    '@ltK{0} '@B{0} '@S{0}} '@state{0}) ('suc{0} ('suc{0} ('suc{0} '0{0}))) '@B{0} '@A{0} ('FRESH{0} '@nonce{0} ('suc{0}
    '0{0})) ('FRESH{0} '@nonce{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0}))))) '@kBS{0}, $union('T_responder_Resp2{0}
    '@B{0} ('FRESH{0} ({'@B : '@princ{0}} {'_ : '@princ{0}} {'_ : '@nonce{0}} {'_ : '@nonce{0}} {'_ : '@ltK{0} '@B{0} '@S{
    0}} '@state{0}) ('suc{0} ('suc{0} ('suc{0} '0{0})))), $union('EL{0} ('@ltK{0} '@B{0} '@S{0}) '@kBS{0}, $union('@N{0}
    $@&($@&($@&($@&('@nonce-msg{0} ('FRESH{0} '@nonce{0} ('suc{0} '0{0})), '@princ-msg{0} '@A{0}), '@princ-msg{0} '@B{0}),
    '@encrypt{0} ('@ltK-shK{0} '@kAS{0}) $@&('@nonce-msg{0} ('FRESH{0} '@nonce{0} ('suc{0} ('suc{0} '0{0}))), '@nonce-msg{
    0} ('FRESH{0} '@nonce{0} ('suc{0} '0{0})), '@princ-msg{0} '@A{0}, '@princ-msg{0} '@B{0})), '@encrypt{0} ('@ltK-shK{0}
    '@kBS{0}) $@&($@&($@&('@nonce-msg{0} ('FRESH{0} '@nonce{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0}))))), '@nonce-msg{
    0} ('FRESH{0} '@nonce{0} ('suc{0} '0{0}))), '@princ-msg{0} '@A{0}), '@princ-msg{0} '@B{0})), 'F{0} ('suc{0} ('suc{0} (
    'suc{0} ('suc{0} ('suc{0} '0{0}))))))))))
*********** trial #3
crl $union('@N{0} $@&('@nonce-msg{0} @@n:Trm, '@princ-msg{0} @@A:Trm, '@princ-msg{0} @@B:Trm, '@encrypt{0} ('@ltK-shK{0}
    @@kAS:Trm) $@&('@nonce-msg{0} @@nA:Trm, '@nonce-msg{0} @@n:Trm, '@princ-msg{0} @@A:Trm, '@princ-msg{0} @@B:Trm),
    '@encrypt{0} ('@ltK-shK{0} @@kBS:Trm) $@&('@nonce-msg{0} @@nB:Trm, '@nonce-msg{0} @@n:Trm, '@princ-msg{0} @@A:Trm,
    '@princ-msg{0} @@B:Trm)), '@START-3{0} '@S{0}, 'F{0} @fresh:Trm) => $union('F{0} @fresh':Trm, $union('@N{0} $@&($@&(
    '@nonce-msg{0} @@n:Trm, '@encrypt{0} ('@ltK-shK{0} @@kAS:Trm) $@&('@nonce-msg{0} @@nA:Trm, '@stK-msg{0} @@kAB:Trm)),
    '@encrypt{0} ('@ltK-shK{0} @@kBS:Trm) $@&('@nonce-msg{0} @@nB:Trm, '@stK-msg{0} @@kAB:Trm)), '@TERMINATED-3{0} '@S{0}))
    if @@kAB:Trm := 'FRESH{0} ('@stK{0} @@A:Trm @@B:Trm) @fresh:Trm /\ @fresh':Trm := 'suc{0} @fresh:Trm .
@@n:Trm --> 'FRESH{0} '@nonce{0} ('suc{0} '0{0})
@@A:Trm --> '@A{0}
@@B:Trm --> '@B{0}
@@kAS:Trm --> '@kAS{0}
@@nA:Trm --> 'FRESH{0} '@nonce{0} ('suc{0} ('suc{0} '0{0}))
@@kBS:Trm --> '@kBS{0}
@@nB:Trm --> 'FRESH{0} '@nonce{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0}))))
@fresh:Trm --> 'suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0}))))
@@kAB:Trm --> (unbound)
@fresh':Trm --> (unbound)
*********** solving condition fragment
@@kAB:Trm := 'FRESH{0} ('@stK{0} @@A:Trm @@B:Trm) @fresh:Trm
*********** success for condition fragment
@@kAB:Trm := 'FRESH{0} ('@stK{0} @@A:Trm @@B:Trm) @fresh:Trm
@@n:Trm --> 'FRESH{0} '@nonce{0} ('suc{0} '0{0})
@@A:Trm --> '@A{0}
@@B:Trm --> '@B{0}
@@kAS:Trm --> '@kAS{0}
@@nA:Trm --> 'FRESH{0} '@nonce{0} ('suc{0} ('suc{0} '0{0}))
@@kBS:Trm --> '@kBS{0}
@@nB:Trm --> 'FRESH{0} '@nonce{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0}))))
@fresh:Trm --> 'suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0}))))
@@kAB:Trm --> 'FRESH{0} ('@stK{0} '@A{0} '@B{0}) ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0})))))
@fresh':Trm --> (unbound)
*********** solving condition fragment
@fresh':Trm := 'suc{0} @fresh:Trm
*********** success for condition fragment
@fresh':Trm := 'suc{0} @fresh:Trm
@@n:Trm --> 'FRESH{0} '@nonce{0} ('suc{0} '0{0})
@@A:Trm --> '@A{0}
@@B:Trm --> '@B{0}
@@kAS:Trm --> '@kAS{0}
@@nA:Trm --> 'FRESH{0} '@nonce{0} ('suc{0} ('suc{0} '0{0}))
@@kBS:Trm --> '@kBS{0}
@@nB:Trm --> 'FRESH{0} '@nonce{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0}))))
@fresh:Trm --> 'suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0}))))
@@kAB:Trm --> 'FRESH{0} ('@stK{0} '@A{0} '@B{0}) ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0})))))
@fresh':Trm --> 'suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0})))))
*********** success #3
*********** rule
crl $union('@N{0} $@&('@nonce-msg{0} @@n:Trm, '@princ-msg{0} @@A:Trm, '@princ-msg{0} @@B:Trm, '@encrypt{0} ('@ltK-shK{0}
    @@kAS:Trm) $@&('@nonce-msg{0} @@nA:Trm, '@nonce-msg{0} @@n:Trm, '@princ-msg{0} @@A:Trm, '@princ-msg{0} @@B:Trm),
    '@encrypt{0} ('@ltK-shK{0} @@kBS:Trm) $@&('@nonce-msg{0} @@nB:Trm, '@nonce-msg{0} @@n:Trm, '@princ-msg{0} @@A:Trm,
    '@princ-msg{0} @@B:Trm)), '@START-3{0} '@S{0}, 'F{0} @fresh:Trm) => $union('F{0} @fresh':Trm, $union('@N{0} $@&($@&(
    '@nonce-msg{0} @@n:Trm, '@encrypt{0} ('@ltK-shK{0} @@kAS:Trm) $@&('@nonce-msg{0} @@nA:Trm, '@stK-msg{0} @@kAB:Trm)),
    '@encrypt{0} ('@ltK-shK{0} @@kBS:Trm) $@&('@nonce-msg{0} @@nB:Trm, '@stK-msg{0} @@kAB:Trm)), '@TERMINATED-3{0} '@S{0}))
    if @@kAB:Trm := 'FRESH{0} ('@stK{0} @@A:Trm @@B:Trm) @fresh:Trm /\ @fresh':Trm := 'suc{0} @fresh:Trm .
@@n:Trm --> 'FRESH{0} '@nonce{0} ('suc{0} '0{0})
@@A:Trm --> '@A{0}
@@B:Trm --> '@B{0}
@@kAS:Trm --> '@kAS{0}
@@nA:Trm --> 'FRESH{0} '@nonce{0} ('suc{0} ('suc{0} '0{0}))
@@kBS:Trm --> '@kBS{0}
@@nB:Trm --> 'FRESH{0} '@nonce{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0}))))
@fresh:Trm --> 'suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0}))))
@@kAB:Trm --> 'FRESH{0} ('@stK{0} '@A{0} '@B{0}) ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0})))))
@fresh':Trm --> 'suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0})))))
Old: $union('@N{0} $@&('@nonce-msg{0} ('FRESH{0} '@nonce{0} ('suc{0} '0{0})), '@princ-msg{0} '@A{0}, '@princ-msg{0} '@B{0},
    '@encrypt{0} ('@ltK-shK{0} '@kAS{0}) $@&('@nonce-msg{0} ('FRESH{0} '@nonce{0} ('suc{0} ('suc{0} '0{0}))), '@nonce-msg{
    0} ('FRESH{0} '@nonce{0} ('suc{0} '0{0})), '@princ-msg{0} '@A{0}, '@princ-msg{0} '@B{0}), '@encrypt{0} ('@ltK-shK{0}
    '@kBS{0}) $@&('@nonce-msg{0} ('FRESH{0} '@nonce{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0}))))), '@nonce-msg{0} (
    'FRESH{0} '@nonce{0} ('suc{0} '0{0})), '@princ-msg{0} '@A{0}, '@princ-msg{0} '@B{0})), '@START-3{0} '@S{0}, 'F{0} (
    'suc{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}
    '@princ{0} '@S{0}, 'EL{0} ('@ltK{0} '@A{0} '@S{0}) '@kAS{0}, 'EL{0} ('@ltK{0} '@B{0} '@S{0}) '@kBS{0},
    'T_initiator_Init2{0} '@A{0} ('FRESH{0} ({'_ : '@princ{0}} {'_ : '@princ{0}} {'_ : '@nonce{0}} {'_ : '@nonce{0}}
    '@state{0}) '0{0}), 'T_responder_Resp2{0} '@B{0} ('FRESH{0} ({'@B : '@princ{0}} {'_ : '@princ{0}} {'_ : '@nonce{0}} {'_
    : '@nonce{0}} {'_ : '@ltK{0} '@B{0} '@S{0}} '@state{0}) ('suc{0} ('suc{0} ('suc{0} '0{0})))), 'FRESH{0} ({'_ : '@princ{
    0}} {'_ : '@princ{0}} {'_ : '@nonce{0}} {'_ : '@nonce{0}} '@state{0}) '0{0} '@A{0} '@B{0} ('FRESH{0} '@nonce{0} ('suc{
    0} '0{0})) ('FRESH{0} '@nonce{0} ('suc{0} ('suc{0} '0{0}))), 'FRESH{0} ({'@B : '@princ{0}} {'_ : '@princ{0}} {'_ :
    '@nonce{0}} {'_ : '@nonce{0}} {'_ : '@ltK{0} '@B{0} '@S{0}} '@state{0}) ('suc{0} ('suc{0} ('suc{0} '0{0}))) '@B{0} '@A{
    0} ('FRESH{0} '@nonce{0} ('suc{0} '0{0})) ('FRESH{0} '@nonce{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0}))))) '@kBS{
    0})
$union('@N{0} $@&('@nonce-msg{0} ('FRESH{0} '@nonce{0} ('suc{0} '0{0})), '@princ-msg{0} '@A{0}, '@princ-msg{0} '@B{0},
    '@encrypt{0} ('@ltK-shK{0} '@kAS{0}) $@&('@nonce-msg{0} ('FRESH{0} '@nonce{0} ('suc{0} ('suc{0} '0{0}))), '@nonce-msg{
    0} ('FRESH{0} '@nonce{0} ('suc{0} '0{0})), '@princ-msg{0} '@A{0}, '@princ-msg{0} '@B{0}), '@encrypt{0} ('@ltK-shK{0}
    '@kBS{0}) $@&('@nonce-msg{0} ('FRESH{0} '@nonce{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0}))))), '@nonce-msg{0} (
    'FRESH{0} '@nonce{0} ('suc{0} '0{0})), '@princ-msg{0} '@A{0}, '@princ-msg{0} '@B{0})), '@START-3{0} '@S{0}, 'F{0} (
    'suc{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}
    '@princ{0} '@S{0}, 'EL{0} ('@ltK{0} '@A{0} '@S{0}) '@kAS{0}, 'EL{0} ('@ltK{0} '@B{0} '@S{0}) '@kBS{0},
    'T_initiator_Init2{0} '@A{0} ('FRESH{0} ({'_ : '@princ{0}} {'_ : '@princ{0}} {'_ : '@nonce{0}} {'_ : '@nonce{0}}
    '@state{0}) '0{0}), 'T_responder_Resp2{0} '@B{0} ('FRESH{0} ({'@B : '@princ{0}} {'_ : '@princ{0}} {'_ : '@nonce{0}} {'_
    : '@nonce{0}} {'_ : '@ltK{0} '@B{0} '@S{0}} '@state{0}) ('suc{0} ('suc{0} ('suc{0} '0{0})))), 'FRESH{0} ({'_ : '@princ{
    0}} {'_ : '@princ{0}} {'_ : '@nonce{0}} {'_ : '@nonce{0}} '@state{0}) '0{0} '@A{0} '@B{0} ('FRESH{0} '@nonce{0} ('suc{
    0} '0{0})) ('FRESH{0} '@nonce{0} ('suc{0} ('suc{0} '0{0}))), 'FRESH{0} ({'@B : '@princ{0}} {'_ : '@princ{0}} {'_ :
    '@nonce{0}} {'_ : '@nonce{0}} {'_ : '@ltK{0} '@B{0} '@S{0}} '@state{0}) ('suc{0} ('suc{0} ('suc{0} '0{0}))) '@B{0} '@A{
    0} ('FRESH{0} '@nonce{0} ('suc{0} '0{0})) ('FRESH{0} '@nonce{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0}))))) '@kBS{
    0})
--->
$union($union('EL{0} '@princ{0} '@A{0}, 'EL{0} '@princ{0} '@B{0}, 'EL{0} '@princ{0} '@S{0}, 'EL{0} ('@ltK{0} '@A{0} '@S{0})
    '@kAS{0}, 'EL{0} ('@ltK{0} '@B{0} '@S{0}) '@kBS{0}, 'T_initiator_Init2{0} '@A{0} ('FRESH{0} ({'_ : '@princ{0}} {'_ :
    '@princ{0}} {'_ : '@nonce{0}} {'_ : '@nonce{0}} '@state{0}) '0{0}), 'T_responder_Resp2{0} '@B{0} ('FRESH{0} ({'@B :
    '@princ{0}} {'_ : '@princ{0}} {'_ : '@nonce{0}} {'_ : '@nonce{0}} {'_ : '@ltK{0} '@B{0} '@S{0}} '@state{0}) ('suc{0} (
    'suc{0} ('suc{0} '0{0})))), 'FRESH{0} ({'_ : '@princ{0}} {'_ : '@princ{0}} {'_ : '@nonce{0}} {'_ : '@nonce{0}} '@state{
    0}) '0{0} '@A{0} '@B{0} ('FRESH{0} '@nonce{0} ('suc{0} '0{0})) ('FRESH{0} '@nonce{0} ('suc{0} ('suc{0} '0{0}))),
    'FRESH{0} ({'@B : '@princ{0}} {'_ : '@princ{0}} {'_ : '@nonce{0}} {'_ : '@nonce{0}} {'_ : '@ltK{0} '@B{0} '@S{0}}
    '@state{0}) ('suc{0} ('suc{0} ('suc{0} '0{0}))) '@B{0} '@A{0} ('FRESH{0} '@nonce{0} ('suc{0} '0{0})) ('FRESH{0}
    '@nonce{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0}))))) '@kBS{0}), $union('F{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} (
    'suc{0} ('suc{0} '0{0})))))), $union('@N{0} $@&($@&('@nonce-msg{0} ('FRESH{0} '@nonce{0} ('suc{0} '0{0})), '@encrypt{0}
    ('@ltK-shK{0} '@kAS{0}) $@&('@nonce-msg{0} ('FRESH{0} '@nonce{0} ('suc{0} ('suc{0} '0{0}))), '@stK-msg{0} ('FRESH{0} (
    '@stK{0} '@A{0} '@B{0}) ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0})))))))), '@encrypt{0} ('@ltK-shK{0} '@kBS{
    0}) $@&('@nonce-msg{0} ('FRESH{0} '@nonce{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0}))))), '@stK-msg{0} ('FRESH{0} (
    '@stK{0} '@A{0} '@B{0}) ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0})))))))), '@TERMINATED-3{0} '@S{0})))
New: $union($union('EL{0} '@princ{0} '@A{0}, 'EL{0} '@princ{0} '@B{0}, 'EL{0} '@princ{0} '@S{0}, 'EL{0} ('@ltK{0} '@A{0}
    '@S{0}) '@kAS{0}, 'EL{0} ('@ltK{0} '@B{0} '@S{0}) '@kBS{0}, 'T_initiator_Init2{0} '@A{0} ('FRESH{0} ({'_ : '@princ{0}}
    {'_ : '@princ{0}} {'_ : '@nonce{0}} {'_ : '@nonce{0}} '@state{0}) '0{0}), 'T_responder_Resp2{0} '@B{0} ('FRESH{0} ({'@B
    : '@princ{0}} {'_ : '@princ{0}} {'_ : '@nonce{0}} {'_ : '@nonce{0}} {'_ : '@ltK{0} '@B{0} '@S{0}} '@state{0}) ('suc{0}
    ('suc{0} ('suc{0} '0{0})))), 'FRESH{0} ({'_ : '@princ{0}} {'_ : '@princ{0}} {'_ : '@nonce{0}} {'_ : '@nonce{0}}
    '@state{0}) '0{0} '@A{0} '@B{0} ('FRESH{0} '@nonce{0} ('suc{0} '0{0})) ('FRESH{0} '@nonce{0} ('suc{0} ('suc{0} '0{
    0}))), 'FRESH{0} ({'@B : '@princ{0}} {'_ : '@princ{0}} {'_ : '@nonce{0}} {'_ : '@nonce{0}} {'_ : '@ltK{0} '@B{0} '@S{
    0}} '@state{0}) ('suc{0} ('suc{0} ('suc{0} '0{0}))) '@B{0} '@A{0} ('FRESH{0} '@nonce{0} ('suc{0} '0{0})) ('FRESH{0}
    '@nonce{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0}))))) '@kBS{0}), $union('F{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} (
    'suc{0} ('suc{0} '0{0})))))), $union('@N{0} $@&($@&('@nonce-msg{0} ('FRESH{0} '@nonce{0} ('suc{0} '0{0})), '@encrypt{0}
    ('@ltK-shK{0} '@kAS{0}) $@&('@nonce-msg{0} ('FRESH{0} '@nonce{0} ('suc{0} ('suc{0} '0{0}))), '@stK-msg{0} ('FRESH{0} (
    '@stK{0} '@A{0} '@B{0}) ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0})))))))), '@encrypt{0} ('@ltK-shK{0} '@kBS{
    0}) $@&('@nonce-msg{0} ('FRESH{0} '@nonce{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0}))))), '@stK-msg{0} ('FRESH{0} (
    '@stK{0} '@A{0} '@B{0}) ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0})))))))), '@TERMINATED-3{0} '@S{0})))
*********** trial #4
crl $union('@N{0} $@&('@nonce-msg{0} @@n:Trm, @@Y:Trm, '@encrypt{0} ('@ltK-shK{0} @@kBS:Trm) $@&('@nonce-msg{0} @@nB:Trm,
    '@stK-msg{0} @@kAB:Trm)), 'F{0} @fresh:Trm, @@L:Trm @@B:Trm @@A:Trm @@n:Trm @@nB:Trm @@kBS:Trm) => $union(
    'T_responder_Resp1{0} @@B:Trm @@L:Trm, $union('F{0} @fresh':Trm, $union('@N{0} $@&('@nonce-msg{0} @@n:Trm, @@Y:Trm),
    '@TERMINATED-2{0} @@B:Trm))) if @@L:Trm := 'FRESH{0} ({'@B : '@princ{0}} {'_ : '@princ{0}} {'_ : '@nonce{0}} {'_ :
    '@nonce{0}} {'_ : '@ltK{0} @@B:Trm '@S{0}} '@state{0}) @fresh:Trm /\ @fresh':Trm := 'suc{0} @fresh:Trm .
@@n:Trm --> 'FRESH{0} '@nonce{0} ('suc{0} '0{0})
@@Y:Trm --> '@encrypt{0} ('@ltK-shK{0} '@kAS{0}) $@&('@nonce-msg{0} ('FRESH{0} '@nonce{0} ('suc{0} ('suc{0} '0{0}))),
    '@stK-msg{0} ('FRESH{0} ('@stK{0} '@A{0} '@B{0}) ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0})))))))
@@kBS:Trm --> '@kBS{0}
@@nB:Trm --> 'FRESH{0} '@nonce{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0}))))
@@kAB:Trm --> 'FRESH{0} ('@stK{0} '@A{0} '@B{0}) ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0})))))
@fresh:Trm --> 'suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0})))))
@@L:Trm --> 'FRESH{0} ({'@B : '@princ{0}} {'_ : '@princ{0}} {'_ : '@nonce{0}} {'_ : '@nonce{0}} {'_ : '@ltK{0} '@B{0} '@S{
    0}} '@state{0}) ('suc{0} ('suc{0} ('suc{0} '0{0})))
@@B:Trm --> '@B{0}
@@A:Trm --> '@A{0}
@fresh':Trm --> (unbound)
*********** solving condition fragment
@@L:Trm := 'FRESH{0} ({'@B : '@princ{0}} {'_ : '@princ{0}} {'_ : '@nonce{0}} {'_ : '@nonce{0}} {'_ : '@ltK{0} @@B:Trm '@S{
    0}} '@state{0}) @fresh:Trm
*********** failure for condition fragment
@@L:Trm := 'FRESH{0} ({'@B : '@princ{0}} {'_ : '@princ{0}} {'_ : '@nonce{0}} {'_ : '@nonce{0}} {'_ : '@ltK{0} @@B:Trm '@S{
    0}} '@state{0}) @fresh:Trm
*********** failure #4
*********** trial #5
crl $union('@N{0} $@&('@nonce-msg{0} @@n:Trm, @@Y:Trm, '@encrypt{0} ('@ltK-shK{0} @@kBS:Trm) $@&('@nonce-msg{0} @@nB:Trm,
    '@stK-msg{0} @@kAB:Trm)), 'F{0} @fresh:Trm, 'T_responder_Resp2{0} @@B:Trm @@L:Trm, @@L:Trm @@B:Trm @@A:Trm @@n:Trm
    @@nB:Trm @@kBS:Trm) => $union('F{0} @fresh':Trm, $union('@N{0} $@&('@nonce-msg{0} @@n:Trm, @@Y:Trm), '@TERMINATED-2{0}
    @@B:Trm)) if @fresh':Trm := @fresh:Trm .
@@n:Trm --> 'FRESH{0} '@nonce{0} ('suc{0} '0{0})
@@Y:Trm --> '@encrypt{0} ('@ltK-shK{0} '@kAS{0}) $@&('@nonce-msg{0} ('FRESH{0} '@nonce{0} ('suc{0} ('suc{0} '0{0}))),
    '@stK-msg{0} ('FRESH{0} ('@stK{0} '@A{0} '@B{0}) ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0})))))))
@@kBS:Trm --> '@kBS{0}
@@nB:Trm --> 'FRESH{0} '@nonce{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0}))))
@@kAB:Trm --> 'FRESH{0} ('@stK{0} '@A{0} '@B{0}) ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0})))))
@fresh:Trm --> 'suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0})))))
@@B:Trm --> '@B{0}
@@L:Trm --> 'FRESH{0} ({'@B : '@princ{0}} {'_ : '@princ{0}} {'_ : '@nonce{0}} {'_ : '@nonce{0}} {'_ : '@ltK{0} '@B{0} '@S{
    0}} '@state{0}) ('suc{0} ('suc{0} ('suc{0} '0{0})))
@@A:Trm --> '@A{0}
@fresh':Trm --> (unbound)
*********** solving condition fragment
@fresh':Trm := @fresh:Trm
*********** success for condition fragment
@fresh':Trm := @fresh:Trm
@@n:Trm --> 'FRESH{0} '@nonce{0} ('suc{0} '0{0})
@@Y:Trm --> '@encrypt{0} ('@ltK-shK{0} '@kAS{0}) $@&('@nonce-msg{0} ('FRESH{0} '@nonce{0} ('suc{0} ('suc{0} '0{0}))),
    '@stK-msg{0} ('FRESH{0} ('@stK{0} '@A{0} '@B{0}) ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0})))))))
@@kBS:Trm --> '@kBS{0}
@@nB:Trm --> 'FRESH{0} '@nonce{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0}))))
@@kAB:Trm --> 'FRESH{0} ('@stK{0} '@A{0} '@B{0}) ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0})))))
@fresh:Trm --> 'suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0})))))
@@B:Trm --> '@B{0}
@@L:Trm --> 'FRESH{0} ({'@B : '@princ{0}} {'_ : '@princ{0}} {'_ : '@nonce{0}} {'_ : '@nonce{0}} {'_ : '@ltK{0} '@B{0} '@S{
    0}} '@state{0}) ('suc{0} ('suc{0} ('suc{0} '0{0})))
@@A:Trm --> '@A{0}
@fresh':Trm --> 'suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0})))))
*********** success #5
*********** rule
crl $union('@N{0} $@&('@nonce-msg{0} @@n:Trm, @@Y:Trm, '@encrypt{0} ('@ltK-shK{0} @@kBS:Trm) $@&('@nonce-msg{0} @@nB:Trm,
    '@stK-msg{0} @@kAB:Trm)), 'F{0} @fresh:Trm, 'T_responder_Resp2{0} @@B:Trm @@L:Trm, @@L:Trm @@B:Trm @@A:Trm @@n:Trm
    @@nB:Trm @@kBS:Trm) => $union('F{0} @fresh':Trm, $union('@N{0} $@&('@nonce-msg{0} @@n:Trm, @@Y:Trm), '@TERMINATED-2{0}
    @@B:Trm)) if @fresh':Trm := @fresh:Trm .
@@n:Trm --> 'FRESH{0} '@nonce{0} ('suc{0} '0{0})
@@Y:Trm --> '@encrypt{0} ('@ltK-shK{0} '@kAS{0}) $@&('@nonce-msg{0} ('FRESH{0} '@nonce{0} ('suc{0} ('suc{0} '0{0}))),
    '@stK-msg{0} ('FRESH{0} ('@stK{0} '@A{0} '@B{0}) ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0})))))))
@@kBS:Trm --> '@kBS{0}
@@nB:Trm --> 'FRESH{0} '@nonce{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0}))))
@@kAB:Trm --> 'FRESH{0} ('@stK{0} '@A{0} '@B{0}) ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0})))))
@fresh:Trm --> 'suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0})))))
@@B:Trm --> '@B{0}
@@L:Trm --> 'FRESH{0} ({'@B : '@princ{0}} {'_ : '@princ{0}} {'_ : '@nonce{0}} {'_ : '@nonce{0}} {'_ : '@ltK{0} '@B{0} '@S{
    0}} '@state{0}) ('suc{0} ('suc{0} ('suc{0} '0{0})))
@@A:Trm --> '@A{0}
@fresh':Trm --> 'suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0})))))
Old: $union('@N{0} $@&('@nonce-msg{0} ('FRESH{0} '@nonce{0} ('suc{0} '0{0})), '@encrypt{0} ('@ltK-shK{0} '@kAS{0}) $@&(
    '@nonce-msg{0} ('FRESH{0} '@nonce{0} ('suc{0} ('suc{0} '0{0}))), '@stK-msg{0} ('FRESH{0} ('@stK{0} '@A{0} '@B{0}) (
    'suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0}))))))), '@encrypt{0} ('@ltK-shK{0} '@kBS{0}) $@&('@nonce-msg{0} (
    'FRESH{0} '@nonce{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0}))))), '@stK-msg{0} ('FRESH{0} ('@stK{0} '@A{0} '@B{0}) (
    'suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0})))))))), '@TERMINATED-3{0} '@S{0}, 'F{0} ('suc{0} ('suc{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} '@princ{0} '@S{0},
    'EL{0} ('@ltK{0} '@A{0} '@S{0}) '@kAS{0}, 'EL{0} ('@ltK{0} '@B{0} '@S{0}) '@kBS{0}, 'T_initiator_Init2{0} '@A{0} (
    'FRESH{0} ({'_ : '@princ{0}} {'_ : '@princ{0}} {'_ : '@nonce{0}} {'_ : '@nonce{0}} '@state{0}) '0{0}),
    'T_responder_Resp2{0} '@B{0} ('FRESH{0} ({'@B : '@princ{0}} {'_ : '@princ{0}} {'_ : '@nonce{0}} {'_ : '@nonce{0}} {'_ :
    '@ltK{0} '@B{0} '@S{0}} '@state{0}) ('suc{0} ('suc{0} ('suc{0} '0{0})))), 'FRESH{0} ({'_ : '@princ{0}} {'_ : '@princ{
    0}} {'_ : '@nonce{0}} {'_ : '@nonce{0}} '@state{0}) '0{0} '@A{0} '@B{0} ('FRESH{0} '@nonce{0} ('suc{0} '0{0})) ('FRESH{
    0} '@nonce{0} ('suc{0} ('suc{0} '0{0}))), 'FRESH{0} ({'@B : '@princ{0}} {'_ : '@princ{0}} {'_ : '@nonce{0}} {'_ :
    '@nonce{0}} {'_ : '@ltK{0} '@B{0} '@S{0}} '@state{0}) ('suc{0} ('suc{0} ('suc{0} '0{0}))) '@B{0} '@A{0} ('FRESH{0}
    '@nonce{0} ('suc{0} '0{0})) ('FRESH{0} '@nonce{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0}))))) '@kBS{0})
$union('@N{0} $@&('@nonce-msg{0} ('FRESH{0} '@nonce{0} ('suc{0} '0{0})), '@encrypt{0} ('@ltK-shK{0} '@kAS{0}) $@&(
    '@nonce-msg{0} ('FRESH{0} '@nonce{0} ('suc{0} ('suc{0} '0{0}))), '@stK-msg{0} ('FRESH{0} ('@stK{0} '@A{0} '@B{0}) (
    'suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0}))))))), '@encrypt{0} ('@ltK-shK{0} '@kBS{0}) $@&('@nonce-msg{0} (
    'FRESH{0} '@nonce{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0}))))), '@stK-msg{0} ('FRESH{0} ('@stK{0} '@A{0} '@B{0}) (
    'suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0})))))))), '@TERMINATED-3{0} '@S{0}, 'F{0} ('suc{0} ('suc{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} '@princ{0} '@S{0},
    'EL{0} ('@ltK{0} '@A{0} '@S{0}) '@kAS{0}, 'EL{0} ('@ltK{0} '@B{0} '@S{0}) '@kBS{0}, 'T_initiator_Init2{0} '@A{0} (
    'FRESH{0} ({'_ : '@princ{0}} {'_ : '@princ{0}} {'_ : '@nonce{0}} {'_ : '@nonce{0}} '@state{0}) '0{0}),
    'T_responder_Resp2{0} '@B{0} ('FRESH{0} ({'@B : '@princ{0}} {'_ : '@princ{0}} {'_ : '@nonce{0}} {'_ : '@nonce{0}} {'_ :
    '@ltK{0} '@B{0} '@S{0}} '@state{0}) ('suc{0} ('suc{0} ('suc{0} '0{0})))), 'FRESH{0} ({'_ : '@princ{0}} {'_ : '@princ{
    0}} {'_ : '@nonce{0}} {'_ : '@nonce{0}} '@state{0}) '0{0} '@A{0} '@B{0} ('FRESH{0} '@nonce{0} ('suc{0} '0{0})) ('FRESH{
    0} '@nonce{0} ('suc{0} ('suc{0} '0{0}))), 'FRESH{0} ({'@B : '@princ{0}} {'_ : '@princ{0}} {'_ : '@nonce{0}} {'_ :
    '@nonce{0}} {'_ : '@ltK{0} '@B{0} '@S{0}} '@state{0}) ('suc{0} ('suc{0} ('suc{0} '0{0}))) '@B{0} '@A{0} ('FRESH{0}
    '@nonce{0} ('suc{0} '0{0})) ('FRESH{0} '@nonce{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0}))))) '@kBS{0})
--->
$union($union('@TERMINATED-3{0} '@S{0}, 'EL{0} '@princ{0} '@A{0}, 'EL{0} '@princ{0} '@B{0}, 'EL{0} '@princ{0} '@S{0}, 'EL{
    0} ('@ltK{0} '@A{0} '@S{0}) '@kAS{0}, 'EL{0} ('@ltK{0} '@B{0} '@S{0}) '@kBS{0}, 'T_initiator_Init2{0} '@A{0} ('FRESH{0}
    ({'_ : '@princ{0}} {'_ : '@princ{0}} {'_ : '@nonce{0}} {'_ : '@nonce{0}} '@state{0}) '0{0}), 'FRESH{0} ({'_ : '@princ{
    0}} {'_ : '@princ{0}} {'_ : '@nonce{0}} {'_ : '@nonce{0}} '@state{0}) '0{0} '@A{0} '@B{0} ('FRESH{0} '@nonce{0} ('suc{
    0} '0{0})) ('FRESH{0} '@nonce{0} ('suc{0} ('suc{0} '0{0})))), $union('F{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0}
    ('suc{0} '0{0})))))), $union('@N{0} $@&('@nonce-msg{0} ('FRESH{0} '@nonce{0} ('suc{0} '0{0})), '@encrypt{0} ('@ltK-shK{
    0} '@kAS{0}) $@&('@nonce-msg{0} ('FRESH{0} '@nonce{0} ('suc{0} ('suc{0} '0{0}))), '@stK-msg{0} ('FRESH{0} ('@stK{0}
    '@A{0} '@B{0}) ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0})))))))), '@TERMINATED-2{0} '@B{0})))
New: $union($union('@TERMINATED-3{0} '@S{0}, 'EL{0} '@princ{0} '@A{0}, 'EL{0} '@princ{0} '@B{0}, 'EL{0} '@princ{0} '@S{0},
    'EL{0} ('@ltK{0} '@A{0} '@S{0}) '@kAS{0}, 'EL{0} ('@ltK{0} '@B{0} '@S{0}) '@kBS{0}, 'T_initiator_Init2{0} '@A{0} (
    'FRESH{0} ({'_ : '@princ{0}} {'_ : '@princ{0}} {'_ : '@nonce{0}} {'_ : '@nonce{0}} '@state{0}) '0{0}), 'FRESH{0} ({'_ :
    '@princ{0}} {'_ : '@princ{0}} {'_ : '@nonce{0}} {'_ : '@nonce{0}} '@state{0}) '0{0} '@A{0} '@B{0} ('FRESH{0} '@nonce{0}
    ('suc{0} '0{0})) ('FRESH{0} '@nonce{0} ('suc{0} ('suc{0} '0{0})))), $union('F{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} (
    'suc{0} ('suc{0} '0{0})))))), $union('@N{0} $@&('@nonce-msg{0} ('FRESH{0} '@nonce{0} ('suc{0} '0{0})), '@encrypt{0} (
    '@ltK-shK{0} '@kAS{0}) $@&('@nonce-msg{0} ('FRESH{0} '@nonce{0} ('suc{0} ('suc{0} '0{0}))), '@stK-msg{0} ('FRESH{0} (
    '@stK{0} '@A{0} '@B{0}) ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0})))))))), '@TERMINATED-2{0} '@B{0})))
*********** trial #6
crl $union('@N{0} $@&('@nonce-msg{0} @@n:Trm, '@encrypt{0} ('@ltK-shK{0} @@kAS:Trm) $@&('@nonce-msg{0} @@nA:Trm, '@stK-msg{
    0} @@kAB:Trm)), 'F{0} @fresh:Trm, 'T_initiator_Init2{0} @@A:Trm @@L:Trm, @@L:Trm @@A:Trm @@B:Trm @@n:Trm @@nA:Trm) =>
    $union('@TERMINATED-1{0} @@A:Trm, 'F{0} @fresh':Trm) if @fresh':Trm := @fresh:Trm .
@@n:Trm --> 'FRESH{0} '@nonce{0} ('suc{0} '0{0})
@@kAS:Trm --> '@kAS{0}
@@nA:Trm --> 'FRESH{0} '@nonce{0} ('suc{0} ('suc{0} '0{0}))
@@kAB:Trm --> 'FRESH{0} ('@stK{0} '@A{0} '@B{0}) ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0})))))
@fresh:Trm --> 'suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0})))))
@@A:Trm --> '@A{0}
@@L:Trm --> 'FRESH{0} ({'_ : '@princ{0}} {'_ : '@princ{0}} {'_ : '@nonce{0}} {'_ : '@nonce{0}} '@state{0}) '0{0}
@@B:Trm --> '@B{0}
@fresh':Trm --> (unbound)
*********** solving condition fragment
@fresh':Trm := @fresh:Trm
*********** success for condition fragment
@fresh':Trm := @fresh:Trm
@@n:Trm --> 'FRESH{0} '@nonce{0} ('suc{0} '0{0})
@@kAS:Trm --> '@kAS{0}
@@nA:Trm --> 'FRESH{0} '@nonce{0} ('suc{0} ('suc{0} '0{0}))
@@kAB:Trm --> 'FRESH{0} ('@stK{0} '@A{0} '@B{0}) ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0})))))
@fresh:Trm --> 'suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0})))))
@@A:Trm --> '@A{0}
@@L:Trm --> 'FRESH{0} ({'_ : '@princ{0}} {'_ : '@princ{0}} {'_ : '@nonce{0}} {'_ : '@nonce{0}} '@state{0}) '0{0}
@@B:Trm --> '@B{0}
@fresh':Trm --> 'suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0})))))
*********** success #6
*********** rule
crl $union('@N{0} $@&('@nonce-msg{0} @@n:Trm, '@encrypt{0} ('@ltK-shK{0} @@kAS:Trm) $@&('@nonce-msg{0} @@nA:Trm, '@stK-msg{
    0} @@kAB:Trm)), 'F{0} @fresh:Trm, 'T_initiator_Init2{0} @@A:Trm @@L:Trm, @@L:Trm @@A:Trm @@B:Trm @@n:Trm @@nA:Trm) =>
    $union('@TERMINATED-1{0} @@A:Trm, 'F{0} @fresh':Trm) if @fresh':Trm := @fresh:Trm .
@@n:Trm --> 'FRESH{0} '@nonce{0} ('suc{0} '0{0})
@@kAS:Trm --> '@kAS{0}
@@nA:Trm --> 'FRESH{0} '@nonce{0} ('suc{0} ('suc{0} '0{0}))
@@kAB:Trm --> 'FRESH{0} ('@stK{0} '@A{0} '@B{0}) ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0})))))
@fresh:Trm --> 'suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0})))))
@@A:Trm --> '@A{0}
@@L:Trm --> 'FRESH{0} ({'_ : '@princ{0}} {'_ : '@princ{0}} {'_ : '@nonce{0}} {'_ : '@nonce{0}} '@state{0}) '0{0}
@@B:Trm --> '@B{0}
@fresh':Trm --> 'suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0})))))
Old: $union('@N{0} $@&('@nonce-msg{0} ('FRESH{0} '@nonce{0} ('suc{0} '0{0})), '@encrypt{0} ('@ltK-shK{0} '@kAS{0}) $@&(
    '@nonce-msg{0} ('FRESH{0} '@nonce{0} ('suc{0} ('suc{0} '0{0}))), '@stK-msg{0} ('FRESH{0} ('@stK{0} '@A{0} '@B{0}) (
    'suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0})))))))), '@TERMINATED-2{0} '@B{0}, '@TERMINATED-3{0} '@S{0}, 'F{0} (
    'suc{0} ('suc{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} '@princ{0} '@S{0}, 'EL{0} ('@ltK{0} '@A{0} '@S{0}) '@kAS{0}, 'EL{0} ('@ltK{0} '@B{0} '@S{0}) '@kBS{0},
    'T_initiator_Init2{0} '@A{0} ('FRESH{0} ({'_ : '@princ{0}} {'_ : '@princ{0}} {'_ : '@nonce{0}} {'_ : '@nonce{0}}
    '@state{0}) '0{0}), 'FRESH{0} ({'_ : '@princ{0}} {'_ : '@princ{0}} {'_ : '@nonce{0}} {'_ : '@nonce{0}} '@state{0}) '0{
    0} '@A{0} '@B{0} ('FRESH{0} '@nonce{0} ('suc{0} '0{0})) ('FRESH{0} '@nonce{0} ('suc{0} ('suc{0} '0{0}))))
$union('@N{0} $@&('@nonce-msg{0} ('FRESH{0} '@nonce{0} ('suc{0} '0{0})), '@encrypt{0} ('@ltK-shK{0} '@kAS{0}) $@&(
    '@nonce-msg{0} ('FRESH{0} '@nonce{0} ('suc{0} ('suc{0} '0{0}))), '@stK-msg{0} ('FRESH{0} ('@stK{0} '@A{0} '@B{0}) (
    'suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0})))))))), '@TERMINATED-2{0} '@B{0}, '@TERMINATED-3{0} '@S{0}, 'F{0} (
    'suc{0} ('suc{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} '@princ{0} '@S{0}, 'EL{0} ('@ltK{0} '@A{0} '@S{0}) '@kAS{0}, 'EL{0} ('@ltK{0} '@B{0} '@S{0}) '@kBS{0},
    'T_initiator_Init2{0} '@A{0} ('FRESH{0} ({'_ : '@princ{0}} {'_ : '@princ{0}} {'_ : '@nonce{0}} {'_ : '@nonce{0}}
    '@state{0}) '0{0}), 'FRESH{0} ({'_ : '@princ{0}} {'_ : '@princ{0}} {'_ : '@nonce{0}} {'_ : '@nonce{0}} '@state{0}) '0{
    0} '@A{0} '@B{0} ('FRESH{0} '@nonce{0} ('suc{0} '0{0})) ('FRESH{0} '@nonce{0} ('suc{0} ('suc{0} '0{0}))))
--->
$union($union('@TERMINATED-2{0} '@B{0}, '@TERMINATED-3{0} '@S{0}, 'EL{0} '@princ{0} '@A{0}, 'EL{0} '@princ{0} '@B{0}, 'EL{
    0} '@princ{0} '@S{0}, 'EL{0} ('@ltK{0} '@A{0} '@S{0}) '@kAS{0}, 'EL{0} ('@ltK{0} '@B{0} '@S{0}) '@kBS{0}), $union(
    '@TERMINATED-1{0} '@A{0}, 'F{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0}))))))))
New: $union($union('@TERMINATED-2{0} '@B{0}, '@TERMINATED-3{0} '@S{0}, 'EL{0} '@princ{0} '@A{0}, 'EL{0} '@princ{0} '@B{0},
    'EL{0} '@princ{0} '@S{0}, 'EL{0} ('@ltK{0} '@A{0} '@S{0}) '@kAS{0}, 'EL{0} ('@ltK{0} '@B{0} '@S{0}) '@kBS{0}), $union(
    '@TERMINATED-1{0} '@A{0}, 'F{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0}))))))))
rewrites: 14 in 47ms cpu (273ms real) (291 rewrites/second)
result Trm: $union('@TERMINATED-1{0} '@A{0}, '@TERMINATED-2{0} '@B{0}, '@TERMINATED-3{0} '@S{0}, 'F{0} ('suc{0} ('suc{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} '@princ{0}
    '@S{0}, 'EL{0} ('@ltK{0} '@A{0} '@S{0}) '@kAS{0}, 'EL{0} ('@ltK{0} '@B{0} '@S{0}) '@kBS{0})