Maude> set trace on .
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} '@KAS{0} '@AS{0}) (
    'EL{0} '@server{0} '@S{0})) ('EL{0} ('@dbK{0} ('@client-tcs{0} '@C{0})) '@kC{0})) ('EL{0} ('@dbK{0} ('@ts-tcs{0} (
    '@TGS-ts{0} '@TS{0}))) '@kTS{0})) ('EL{0} ('@dbK{0} ('@ts-tcs{0} ('@server-ts{0} '@S{0}))) '@kS{0})) ('union{0} (
    '@START-ASE{0} '@C{0} '@TS{0}) ('union{0} ('@START-TGE{0} '@C{0}) ('@START-CSE{0} '@C{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} '@KAS{0} '@AS{0}) ('EL{0} '@server{
    0} '@S{0})) ('EL{0} ('@dbK{0} ('@client-tcs{0} '@C{0})) '@kC{0})) ('EL{0} ('@dbK{0} ('@ts-tcs{0} ('@TGS-ts{0} '@TS{
    0}))) '@kTS{0})) ('EL{0} ('@dbK{0} ('@ts-tcs{0} ('@server-ts{0} '@S{0}))) '@kS{0})) ('union{0} ('@START-ASE{0} '@C{0}
    '@TS{0}) ('union{0} ('@START-TGE{0} '@C{0}) ('@START-CSE{0} '@C{0}))))
New: 'union{0} ('F{0} '0{0}) ('union{0} ('union{0} ('union{0} ('union{0} ('union{0} ('EL{0} '@KAS{0} '@AS{0}) ('EL{0}
    '@server{0} '@S{0})) ('EL{0} ('@dbK{0} ('@client-tcs{0} '@C{0})) '@kC{0})) ('EL{0} ('@dbK{0} ('@ts-tcs{0} ('@TGS-ts{0}
    '@TS{0}))) '@kTS{0})) ('EL{0} ('@dbK{0} ('@ts-tcs{0} ('@server-ts{0} '@S{0}))) '@kS{0})) ('union{0} ('@START-ASE{0}
    '@C{0} '@TS{0}) ('union{0} ('@START-TGE{0} '@C{0}) ('@START-CSE{0} '@C{0}))))
*********** equation
eq 'union{0} @1:Trm @2:Trm = $union(@2:Trm, @1:Trm) .
@1:Trm --> 'EL{0} '@KAS{0} '@AS{0}
@2:Trm --> 'EL{0} '@server{0} '@S{0}
Old: 'union{0} ('F{0} '0{0}) ('union{0} ('union{0} ('union{0} ('union{0} ('union{0} ('EL{0} '@KAS{0} '@AS{0}) ('EL{0}
    '@server{0} '@S{0})) ('EL{0} ('@dbK{0} ('@client-tcs{0} '@C{0})) '@kC{0})) ('EL{0} ('@dbK{0} ('@ts-tcs{0} ('@TGS-ts{0}
    '@TS{0}))) '@kTS{0})) ('EL{0} ('@dbK{0} ('@ts-tcs{0} ('@server-ts{0} '@S{0}))) '@kS{0})) ('union{0} ('@START-ASE{0}
    '@C{0} '@TS{0}) ('union{0} ('@START-TGE{0} '@C{0}) ('@START-CSE{0} '@C{0}))))
'union{0} ('EL{0} '@KAS{0} '@AS{0}) ('EL{0} '@server{0} '@S{0})
--->
$union('EL{0} '@server{0} '@S{0}, 'EL{0} '@KAS{0} '@AS{0})
New: 'union{0} ('F{0} '0{0}) ('union{0} ('union{0} ('union{0} ('union{0} $union('EL{0} '@server{0} '@S{0}, 'EL{0} '@KAS{0}
    '@AS{0}) ('EL{0} ('@dbK{0} ('@client-tcs{0} '@C{0})) '@kC{0})) ('EL{0} ('@dbK{0} ('@ts-tcs{0} ('@TGS-ts{0} '@TS{0})))
    '@kTS{0})) ('EL{0} ('@dbK{0} ('@ts-tcs{0} ('@server-ts{0} '@S{0}))) '@kS{0})) ('union{0} ('@START-ASE{0} '@C{0} '@TS{
    0}) ('union{0} ('@START-TGE{0} '@C{0}) ('@START-CSE{0} '@C{0}))))
*********** equation
eq 'union{0} @1:Trm @2:Trm = $union(@2:Trm, @1:Trm) .
@1:Trm --> $union('EL{0} '@KAS{0} '@AS{0}, 'EL{0} '@server{0} '@S{0})
@2:Trm --> 'EL{0} ('@dbK{0} ('@client-tcs{0} '@C{0})) '@kC{0}
Old: 'union{0} ('F{0} '0{0}) ('union{0} ('union{0} ('union{0} ('union{0} $union('EL{0} '@KAS{0} '@AS{0}, 'EL{0} '@server{0}
    '@S{0}) ('EL{0} ('@dbK{0} ('@client-tcs{0} '@C{0})) '@kC{0})) ('EL{0} ('@dbK{0} ('@ts-tcs{0} ('@TGS-ts{0} '@TS{0})))
    '@kTS{0})) ('EL{0} ('@dbK{0} ('@ts-tcs{0} ('@server-ts{0} '@S{0}))) '@kS{0})) ('union{0} ('@START-ASE{0} '@C{0} '@TS{
    0}) ('union{0} ('@START-TGE{0} '@C{0}) ('@START-CSE{0} '@C{0}))))
'union{0} $union('EL{0} '@KAS{0} '@AS{0}, 'EL{0} '@server{0} '@S{0}) ('EL{0} ('@dbK{0} ('@client-tcs{0} '@C{0})) '@kC{0})
--->
$union('EL{0} ('@dbK{0} ('@client-tcs{0} '@C{0})) '@kC{0}, $union('EL{0} '@KAS{0} '@AS{0}, 'EL{0} '@server{0} '@S{0}))
New: 'union{0} ('F{0} '0{0}) ('union{0} ('union{0} ('union{0} $union('EL{0} ('@dbK{0} ('@client-tcs{0} '@C{0})) '@kC{0},
    $union('EL{0} '@KAS{0} '@AS{0}, 'EL{0} '@server{0} '@S{0})) ('EL{0} ('@dbK{0} ('@ts-tcs{0} ('@TGS-ts{0} '@TS{0})))
    '@kTS{0})) ('EL{0} ('@dbK{0} ('@ts-tcs{0} ('@server-ts{0} '@S{0}))) '@kS{0})) ('union{0} ('@START-ASE{0} '@C{0} '@TS{
    0}) ('union{0} ('@START-TGE{0} '@C{0}) ('@START-CSE{0} '@C{0}))))
*********** equation
eq 'union{0} @1:Trm @2:Trm = $union(@2:Trm, @1:Trm) .
@1:Trm --> $union('EL{0} '@KAS{0} '@AS{0}, 'EL{0} '@server{0} '@S{0}, 'EL{0} ('@dbK{0} ('@client-tcs{0} '@C{0})) '@kC{0})
@2:Trm --> 'EL{0} ('@dbK{0} ('@ts-tcs{0} ('@TGS-ts{0} '@TS{0}))) '@kTS{0}
Old: 'union{0} ('F{0} '0{0}) ('union{0} ('union{0} ('union{0} $union('EL{0} '@KAS{0} '@AS{0}, 'EL{0} '@server{0} '@S{0},
    'EL{0} ('@dbK{0} ('@client-tcs{0} '@C{0})) '@kC{0}) ('EL{0} ('@dbK{0} ('@ts-tcs{0} ('@TGS-ts{0} '@TS{0}))) '@kTS{0})) (
    'EL{0} ('@dbK{0} ('@ts-tcs{0} ('@server-ts{0} '@S{0}))) '@kS{0})) ('union{0} ('@START-ASE{0} '@C{0} '@TS{0}) ('union{0}
    ('@START-TGE{0} '@C{0}) ('@START-CSE{0} '@C{0}))))
'union{0} $union('EL{0} '@KAS{0} '@AS{0}, 'EL{0} '@server{0} '@S{0}, 'EL{0} ('@dbK{0} ('@client-tcs{0} '@C{0})) '@kC{0}) (
    'EL{0} ('@dbK{0} ('@ts-tcs{0} ('@TGS-ts{0} '@TS{0}))) '@kTS{0})
--->
$union('EL{0} ('@dbK{0} ('@ts-tcs{0} ('@TGS-ts{0} '@TS{0}))) '@kTS{0}, $union('EL{0} '@KAS{0} '@AS{0}, 'EL{0} '@server{0}
    '@S{0}, 'EL{0} ('@dbK{0} ('@client-tcs{0} '@C{0})) '@kC{0}))
New: 'union{0} ('F{0} '0{0}) ('union{0} ('union{0} $union('EL{0} ('@dbK{0} ('@ts-tcs{0} ('@TGS-ts{0} '@TS{0}))) '@kTS{0},
    $union('EL{0} '@KAS{0} '@AS{0}, 'EL{0} '@server{0} '@S{0}, 'EL{0} ('@dbK{0} ('@client-tcs{0} '@C{0})) '@kC{0})) ('EL{0}
    ('@dbK{0} ('@ts-tcs{0} ('@server-ts{0} '@S{0}))) '@kS{0})) ('union{0} ('@START-ASE{0} '@C{0} '@TS{0}) ('union{0} (
    '@START-TGE{0} '@C{0}) ('@START-CSE{0} '@C{0}))))
*********** equation
eq 'union{0} @1:Trm @2:Trm = $union(@2:Trm, @1:Trm) .
@1:Trm --> $union('EL{0} '@KAS{0} '@AS{0}, 'EL{0} '@server{0} '@S{0}, 'EL{0} ('@dbK{0} ('@client-tcs{0} '@C{0})) '@kC{0},
    'EL{0} ('@dbK{0} ('@ts-tcs{0} ('@TGS-ts{0} '@TS{0}))) '@kTS{0})
@2:Trm --> 'EL{0} ('@dbK{0} ('@ts-tcs{0} ('@server-ts{0} '@S{0}))) '@kS{0}
Old: 'union{0} ('F{0} '0{0}) ('union{0} ('union{0} $union('EL{0} '@KAS{0} '@AS{0}, 'EL{0} '@server{0} '@S{0}, 'EL{0} (
    '@dbK{0} ('@client-tcs{0} '@C{0})) '@kC{0}, 'EL{0} ('@dbK{0} ('@ts-tcs{0} ('@TGS-ts{0} '@TS{0}))) '@kTS{0}) ('EL{0} (
    '@dbK{0} ('@ts-tcs{0} ('@server-ts{0} '@S{0}))) '@kS{0})) ('union{0} ('@START-ASE{0} '@C{0} '@TS{0}) ('union{0} (
    '@START-TGE{0} '@C{0}) ('@START-CSE{0} '@C{0}))))
'union{0} $union('EL{0} '@KAS{0} '@AS{0}, 'EL{0} '@server{0} '@S{0}, 'EL{0} ('@dbK{0} ('@client-tcs{0} '@C{0})) '@kC{0},
    'EL{0} ('@dbK{0} ('@ts-tcs{0} ('@TGS-ts{0} '@TS{0}))) '@kTS{0}) ('EL{0} ('@dbK{0} ('@ts-tcs{0} ('@server-ts{0} '@S{
    0}))) '@kS{0})
--->
$union('EL{0} ('@dbK{0} ('@ts-tcs{0} ('@server-ts{0} '@S{0}))) '@kS{0}, $union('EL{0} '@KAS{0} '@AS{0}, 'EL{0} '@server{0}
    '@S{0}, 'EL{0} ('@dbK{0} ('@client-tcs{0} '@C{0})) '@kC{0}, 'EL{0} ('@dbK{0} ('@ts-tcs{0} ('@TGS-ts{0} '@TS{0})))
    '@kTS{0}))
New: 'union{0} ('F{0} '0{0}) ('union{0} $union('EL{0} ('@dbK{0} ('@ts-tcs{0} ('@server-ts{0} '@S{0}))) '@kS{0}, $union('EL{
    0} '@KAS{0} '@AS{0}, 'EL{0} '@server{0} '@S{0}, 'EL{0} ('@dbK{0} ('@client-tcs{0} '@C{0})) '@kC{0}, 'EL{0} ('@dbK{0} (
    '@ts-tcs{0} ('@TGS-ts{0} '@TS{0}))) '@kTS{0})) ('union{0} ('@START-ASE{0} '@C{0} '@TS{0}) ('union{0} ('@START-TGE{0}
    '@C{0}) ('@START-CSE{0} '@C{0}))))
*********** equation
eq 'union{0} @1:Trm @2:Trm = $union(@2:Trm, @1:Trm) .
@1:Trm --> '@START-TGE{0} '@C{0}
@2:Trm --> '@START-CSE{0} '@C{0}
Old: 'union{0} ('F{0} '0{0}) ('union{0} $union('EL{0} '@KAS{0} '@AS{0}, 'EL{0} '@server{0} '@S{0}, 'EL{0} ('@dbK{0} (
    '@client-tcs{0} '@C{0})) '@kC{0}, 'EL{0} ('@dbK{0} ('@ts-tcs{0} ('@TGS-ts{0} '@TS{0}))) '@kTS{0}, 'EL{0} ('@dbK{0} (
    '@ts-tcs{0} ('@server-ts{0} '@S{0}))) '@kS{0}) ('union{0} ('@START-ASE{0} '@C{0} '@TS{0}) ('union{0} ('@START-TGE{0}
    '@C{0}) ('@START-CSE{0} '@C{0}))))
'union{0} ('@START-TGE{0} '@C{0}) ('@START-CSE{0} '@C{0})
--->
$union('@START-CSE{0} '@C{0}, '@START-TGE{0} '@C{0})
New: 'union{0} ('F{0} '0{0}) ('union{0} $union('EL{0} '@KAS{0} '@AS{0}, 'EL{0} '@server{0} '@S{0}, 'EL{0} ('@dbK{0} (
    '@client-tcs{0} '@C{0})) '@kC{0}, 'EL{0} ('@dbK{0} ('@ts-tcs{0} ('@TGS-ts{0} '@TS{0}))) '@kTS{0}, 'EL{0} ('@dbK{0} (
    '@ts-tcs{0} ('@server-ts{0} '@S{0}))) '@kS{0}) ('union{0} ('@START-ASE{0} '@C{0} '@TS{0}) $union('@START-CSE{0} '@C{0},
    '@START-TGE{0} '@C{0})))
*********** equation
eq 'union{0} @1:Trm @2:Trm = $union(@2:Trm, @1:Trm) .
@1:Trm --> '@START-ASE{0} '@C{0} '@TS{0}
@2:Trm --> $union('@START-CSE{0} '@C{0}, '@START-TGE{0} '@C{0})
Old: 'union{0} ('F{0} '0{0}) ('union{0} $union('EL{0} '@KAS{0} '@AS{0}, 'EL{0} '@server{0} '@S{0}, 'EL{0} ('@dbK{0} (
    '@client-tcs{0} '@C{0})) '@kC{0}, 'EL{0} ('@dbK{0} ('@ts-tcs{0} ('@TGS-ts{0} '@TS{0}))) '@kTS{0}, 'EL{0} ('@dbK{0} (
    '@ts-tcs{0} ('@server-ts{0} '@S{0}))) '@kS{0}) ('union{0} ('@START-ASE{0} '@C{0} '@TS{0}) $union('@START-CSE{0} '@C{0},
    '@START-TGE{0} '@C{0})))
'union{0} ('@START-ASE{0} '@C{0} '@TS{0}) $union('@START-CSE{0} '@C{0}, '@START-TGE{0} '@C{0})
--->
$union($union('@START-CSE{0} '@C{0}, '@START-TGE{0} '@C{0}), '@START-ASE{0} '@C{0} '@TS{0})
New: 'union{0} ('F{0} '0{0}) ('union{0} $union('EL{0} '@KAS{0} '@AS{0}, 'EL{0} '@server{0} '@S{0}, 'EL{0} ('@dbK{0} (
    '@client-tcs{0} '@C{0})) '@kC{0}, 'EL{0} ('@dbK{0} ('@ts-tcs{0} ('@TGS-ts{0} '@TS{0}))) '@kTS{0}, 'EL{0} ('@dbK{0} (
    '@ts-tcs{0} ('@server-ts{0} '@S{0}))) '@kS{0}) $union($union('@START-CSE{0} '@C{0}, '@START-TGE{0} '@C{0}),
    '@START-ASE{0} '@C{0} '@TS{0}))
*********** equation
eq 'union{0} @1:Trm @2:Trm = $union(@2:Trm, @1:Trm) .
@1:Trm --> $union('EL{0} '@KAS{0} '@AS{0}, 'EL{0} '@server{0} '@S{0}, 'EL{0} ('@dbK{0} ('@client-tcs{0} '@C{0})) '@kC{0},
    'EL{0} ('@dbK{0} ('@ts-tcs{0} ('@TGS-ts{0} '@TS{0}))) '@kTS{0}, 'EL{0} ('@dbK{0} ('@ts-tcs{0} ('@server-ts{0} '@S{0})))
    '@kS{0})
@2:Trm --> $union('@START-CSE{0} '@C{0}, '@START-TGE{0} '@C{0}, '@START-ASE{0} '@C{0} '@TS{0})
Old: 'union{0} ('F{0} '0{0}) ('union{0} $union('EL{0} '@KAS{0} '@AS{0}, 'EL{0} '@server{0} '@S{0}, 'EL{0} ('@dbK{0} (
    '@client-tcs{0} '@C{0})) '@kC{0}, 'EL{0} ('@dbK{0} ('@ts-tcs{0} ('@TGS-ts{0} '@TS{0}))) '@kTS{0}, 'EL{0} ('@dbK{0} (
    '@ts-tcs{0} ('@server-ts{0} '@S{0}))) '@kS{0}) $union('@START-CSE{0} '@C{0}, '@START-TGE{0} '@C{0}, '@START-ASE{0} '@C{
    0} '@TS{0}))
'union{0} $union('EL{0} '@KAS{0} '@AS{0}, 'EL{0} '@server{0} '@S{0}, 'EL{0} ('@dbK{0} ('@client-tcs{0} '@C{0})) '@kC{0},
    'EL{0} ('@dbK{0} ('@ts-tcs{0} ('@TGS-ts{0} '@TS{0}))) '@kTS{0}, 'EL{0} ('@dbK{0} ('@ts-tcs{0} ('@server-ts{0} '@S{0})))
    '@kS{0}) $union('@START-CSE{0} '@C{0}, '@START-TGE{0} '@C{0}, '@START-ASE{0} '@C{0} '@TS{0})
--->
$union($union('@START-CSE{0} '@C{0}, '@START-TGE{0} '@C{0}, '@START-ASE{0} '@C{0} '@TS{0}), $union('EL{0} '@KAS{0} '@AS{0},
    'EL{0} '@server{0} '@S{0}, 'EL{0} ('@dbK{0} ('@client-tcs{0} '@C{0})) '@kC{0}, 'EL{0} ('@dbK{0} ('@ts-tcs{0} ('@TGS-ts{
    0} '@TS{0}))) '@kTS{0}, 'EL{0} ('@dbK{0} ('@ts-tcs{0} ('@server-ts{0} '@S{0}))) '@kS{0}))
New: 'union{0} ('F{0} '0{0}) $union($union('@START-CSE{0} '@C{0}, '@START-TGE{0} '@C{0}, '@START-ASE{0} '@C{0} '@TS{0}),
    $union('EL{0} '@KAS{0} '@AS{0}, 'EL{0} '@server{0} '@S{0}, 'EL{0} ('@dbK{0} ('@client-tcs{0} '@C{0})) '@kC{0}, 'EL{0} (
    '@dbK{0} ('@ts-tcs{0} ('@TGS-ts{0} '@TS{0}))) '@kTS{0}, 'EL{0} ('@dbK{0} ('@ts-tcs{0} ('@server-ts{0} '@S{0}))) '@kS{
    0}))
*********** equation
eq 'union{0} @1:Trm @2:Trm = $union(@2:Trm, @1:Trm) .
@1:Trm --> 'F{0} '0{0}
@2:Trm --> $union('@START-CSE{0} '@C{0}, '@START-TGE{0} '@C{0}, '@START-ASE{0} '@C{0} '@TS{0}, 'EL{0} '@KAS{0} '@AS{0},
    'EL{0} '@server{0} '@S{0}, 'EL{0} ('@dbK{0} ('@client-tcs{0} '@C{0})) '@kC{0}, 'EL{0} ('@dbK{0} ('@ts-tcs{0} ('@TGS-ts{
    0} '@TS{0}))) '@kTS{0}, 'EL{0} ('@dbK{0} ('@ts-tcs{0} ('@server-ts{0} '@S{0}))) '@kS{0})
Old: 'union{0} ('F{0} '0{0}) $union('@START-CSE{0} '@C{0}, '@START-TGE{0} '@C{0}, '@START-ASE{0} '@C{0} '@TS{0}, 'EL{0}
    '@KAS{0} '@AS{0}, 'EL{0} '@server{0} '@S{0}, 'EL{0} ('@dbK{0} ('@client-tcs{0} '@C{0})) '@kC{0}, 'EL{0} ('@dbK{0} (
    '@ts-tcs{0} ('@TGS-ts{0} '@TS{0}))) '@kTS{0}, 'EL{0} ('@dbK{0} ('@ts-tcs{0} ('@server-ts{0} '@S{0}))) '@kS{0})
'union{0} ('F{0} '0{0}) $union('@START-CSE{0} '@C{0}, '@START-TGE{0} '@C{0}, '@START-ASE{0} '@C{0} '@TS{0}, 'EL{0} '@KAS{0}
    '@AS{0}, 'EL{0} '@server{0} '@S{0}, 'EL{0} ('@dbK{0} ('@client-tcs{0} '@C{0})) '@kC{0}, 'EL{0} ('@dbK{0} ('@ts-tcs{0} (
    '@TGS-ts{0} '@TS{0}))) '@kTS{0}, 'EL{0} ('@dbK{0} ('@ts-tcs{0} ('@server-ts{0} '@S{0}))) '@kS{0})
--->
$union($union('@START-CSE{0} '@C{0}, '@START-TGE{0} '@C{0}, '@START-ASE{0} '@C{0} '@TS{0}, 'EL{0} '@KAS{0} '@AS{0}, 'EL{0}
    '@server{0} '@S{0}, 'EL{0} ('@dbK{0} ('@client-tcs{0} '@C{0})) '@kC{0}, 'EL{0} ('@dbK{0} ('@ts-tcs{0} ('@TGS-ts{0}
    '@TS{0}))) '@kTS{0}, 'EL{0} ('@dbK{0} ('@ts-tcs{0} ('@server-ts{0} '@S{0}))) '@kS{0}), 'F{0} '0{0})
New: $union($union('@START-CSE{0} '@C{0}, '@START-TGE{0} '@C{0}, '@START-ASE{0} '@C{0} '@TS{0}, 'EL{0} '@KAS{0} '@AS{0},
    'EL{0} '@server{0} '@S{0}, 'EL{0} ('@dbK{0} ('@client-tcs{0} '@C{0})) '@kC{0}, 'EL{0} ('@dbK{0} ('@ts-tcs{0} ('@TGS-ts{
    0} '@TS{0}))) '@kTS{0}, 'EL{0} ('@dbK{0} ('@ts-tcs{0} ('@server-ts{0} '@S{0}))) '@kS{0}), 'F{0} '0{0})
*********** trial #1
crl $union('F{0} @fresh:Trm, '@START-ASE{0} @@C:Trm @@T:Trm) => $union(@@L:Trm @@C:Trm @@T:Trm @@n1:Trm, $union(
    'T_clientASE_resp{0} @@C:Trm @@L:Trm, $union('@N{0} $@&($@&('@princ-msg{0} ('@tcs-princ{0} ('@client-tcs{0} @@C:Trm)),
    '@princ-msg{0} ('@tcs-princ{0} ('@ts-tcs{0} ('@TGS-ts{0} @@T:Trm)))), '@nonce-msg{0} @@n1:Trm), 'F{0} @fresh':Trm))) if
    @@L:Trm := 'FRESH{0} ({'_ : '@client{0}} {'_ : '@TGS{0}} {'_ : '@nonce{0}} '@state{0}) @fresh:Trm /\ @@n1:Trm :=
    'FRESH{0} '@nonce{0} ('suc{0} @fresh:Trm) /\ @fresh':Trm := 'suc{0} ('suc{0} @fresh:Trm) .
@fresh:Trm --> '0{0}
@@C:Trm --> '@C{0}
@@T:Trm --> '@TS{0}
@@L:Trm --> (unbound)
@@n1:Trm --> (unbound)
@fresh':Trm --> (unbound)
*********** solving condition fragment
@@L:Trm := 'FRESH{0} ({'_ : '@client{0}} {'_ : '@TGS{0}} {'_ : '@nonce{0}} '@state{0}) @fresh:Trm
*********** success for condition fragment
@@L:Trm := 'FRESH{0} ({'_ : '@client{0}} {'_ : '@TGS{0}} {'_ : '@nonce{0}} '@state{0}) @fresh:Trm
@fresh:Trm --> '0{0}
@@C:Trm --> '@C{0}
@@T:Trm --> '@TS{0}
@@L:Trm --> 'FRESH{0} ({'_ : '@client{0}} {'_ : '@TGS{0}} {'_ : '@nonce{0}} '@state{0}) '0{0}
@@n1:Trm --> (unbound)
@fresh':Trm --> (unbound)
*********** solving condition fragment
@@n1:Trm := 'FRESH{0} '@nonce{0} ('suc{0} @fresh:Trm)
*********** success for condition fragment
@@n1:Trm := 'FRESH{0} '@nonce{0} ('suc{0} @fresh:Trm)
@fresh:Trm --> '0{0}
@@C:Trm --> '@C{0}
@@T:Trm --> '@TS{0}
@@L:Trm --> 'FRESH{0} ({'_ : '@client{0}} {'_ : '@TGS{0}} {'_ : '@nonce{0}} '@state{0}) '0{0}
@@n1: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}
@@C:Trm --> '@C{0}
@@T:Trm --> '@TS{0}
@@L:Trm --> 'FRESH{0} ({'_ : '@client{0}} {'_ : '@TGS{0}} {'_ : '@nonce{0}} '@state{0}) '0{0}
@@n1: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-ASE{0} @@C:Trm @@T:Trm) => $union(@@L:Trm @@C:Trm @@T:Trm @@n1:Trm, $union(
    'T_clientASE_resp{0} @@C:Trm @@L:Trm, $union('@N{0} $@&($@&('@princ-msg{0} ('@tcs-princ{0} ('@client-tcs{0} @@C:Trm)),
    '@princ-msg{0} ('@tcs-princ{0} ('@ts-tcs{0} ('@TGS-ts{0} @@T:Trm)))), '@nonce-msg{0} @@n1:Trm), 'F{0} @fresh':Trm))) if
    @@L:Trm := 'FRESH{0} ({'_ : '@client{0}} {'_ : '@TGS{0}} {'_ : '@nonce{0}} '@state{0}) @fresh:Trm /\ @@n1:Trm :=
    'FRESH{0} '@nonce{0} ('suc{0} @fresh:Trm) /\ @fresh':Trm := 'suc{0} ('suc{0} @fresh:Trm) .
@fresh:Trm --> '0{0}
@@C:Trm --> '@C{0}
@@T:Trm --> '@TS{0}
@@L:Trm --> 'FRESH{0} ({'_ : '@client{0}} {'_ : '@TGS{0}} {'_ : '@nonce{0}} '@state{0}) '0{0}
@@n1:Trm --> 'FRESH{0} '@nonce{0} ('suc{0} '0{0})
@fresh':Trm --> 'suc{0} ('suc{0} '0{0})
Old: $union('@START-CSE{0} '@C{0}, '@START-TGE{0} '@C{0}, 'F{0} '0{0}, '@START-ASE{0} '@C{0} '@TS{0}, 'EL{0} '@KAS{0} '@AS{
    0}, 'EL{0} '@server{0} '@S{0}, 'EL{0} ('@dbK{0} ('@client-tcs{0} '@C{0})) '@kC{0}, 'EL{0} ('@dbK{0} ('@ts-tcs{0} (
    '@TGS-ts{0} '@TS{0}))) '@kTS{0}, 'EL{0} ('@dbK{0} ('@ts-tcs{0} ('@server-ts{0} '@S{0}))) '@kS{0})
$union('@START-CSE{0} '@C{0}, '@START-TGE{0} '@C{0}, 'F{0} '0{0}, '@START-ASE{0} '@C{0} '@TS{0}, 'EL{0} '@KAS{0} '@AS{0},
    'EL{0} '@server{0} '@S{0}, 'EL{0} ('@dbK{0} ('@client-tcs{0} '@C{0})) '@kC{0}, 'EL{0} ('@dbK{0} ('@ts-tcs{0} ('@TGS-ts{
    0} '@TS{0}))) '@kTS{0}, 'EL{0} ('@dbK{0} ('@ts-tcs{0} ('@server-ts{0} '@S{0}))) '@kS{0})
--->
$union($union('@START-CSE{0} '@C{0}, '@START-TGE{0} '@C{0}, 'EL{0} '@KAS{0} '@AS{0}, 'EL{0} '@server{0} '@S{0}, 'EL{0} (
    '@dbK{0} ('@client-tcs{0} '@C{0})) '@kC{0}, 'EL{0} ('@dbK{0} ('@ts-tcs{0} ('@TGS-ts{0} '@TS{0}))) '@kTS{0}, 'EL{0} (
    '@dbK{0} ('@ts-tcs{0} ('@server-ts{0} '@S{0}))) '@kS{0}), $union('FRESH{0} ({'_ : '@client{0}} {'_ : '@TGS{0}} {'_ :
    '@nonce{0}} '@state{0}) '0{0} '@C{0} '@TS{0} ('FRESH{0} '@nonce{0} ('suc{0} '0{0})), $union('T_clientASE_resp{0} '@C{0}
    ('FRESH{0} ({'_ : '@client{0}} {'_ : '@TGS{0}} {'_ : '@nonce{0}} '@state{0}) '0{0}), $union('@N{0} $@&($@&('@princ-msg{
    0} ('@tcs-princ{0} ('@client-tcs{0} '@C{0})), '@princ-msg{0} ('@tcs-princ{0} ('@ts-tcs{0} ('@TGS-ts{0} '@TS{0})))),
    '@nonce-msg{0} ('FRESH{0} '@nonce{0} ('suc{0} '0{0}))), 'F{0} ('suc{0} ('suc{0} '0{0}))))))
New: $union($union('@START-CSE{0} '@C{0}, '@START-TGE{0} '@C{0}, 'EL{0} '@KAS{0} '@AS{0}, 'EL{0} '@server{0} '@S{0}, 'EL{0}
    ('@dbK{0} ('@client-tcs{0} '@C{0})) '@kC{0}, 'EL{0} ('@dbK{0} ('@ts-tcs{0} ('@TGS-ts{0} '@TS{0}))) '@kTS{0}, 'EL{0} (
    '@dbK{0} ('@ts-tcs{0} ('@server-ts{0} '@S{0}))) '@kS{0}), $union('FRESH{0} ({'_ : '@client{0}} {'_ : '@TGS{0}} {'_ :
    '@nonce{0}} '@state{0}) '0{0} '@C{0} '@TS{0} ('FRESH{0} '@nonce{0} ('suc{0} '0{0})), $union('T_clientASE_resp{0} '@C{0}
    ('FRESH{0} ({'_ : '@client{0}} {'_ : '@TGS{0}} {'_ : '@nonce{0}} '@state{0}) '0{0}), $union('@N{0} $@&($@&('@princ-msg{
    0} ('@tcs-princ{0} ('@client-tcs{0} '@C{0})), '@princ-msg{0} ('@tcs-princ{0} ('@ts-tcs{0} ('@TGS-ts{0} '@TS{0})))),
    '@nonce-msg{0} ('FRESH{0} '@nonce{0} ('suc{0} '0{0}))), 'F{0} ('suc{0} ('suc{0} '0{0}))))))
*********** trial #2
crl $union('@N{0} $@&('@princ-msg{0} ('@tcs-princ{0} ('@client-tcs{0} @@C:Trm)), '@princ-msg{0} ('@tcs-princ{0} ('@ts-tcs{
    0} ('@TGS-ts{0} @@T:Trm))), '@nonce-msg{0} @@n1:Trm), 'F{0} @fresh:Trm, 'EL{0} ('@dbK{0} ('@client-tcs{0} @@C:Trm))
    @@kC:Trm, 'EL{0} ('@dbK{0} ('@ts-tcs{0} ('@TGS-ts{0} @@T:Trm))) @@kT:Trm) => $union('EL{0} ('@dbK{0} ('@ts-tcs{0} (
    '@TGS-ts{0} @@T:Trm))) @@kT:Trm, $union('EL{0} ('@dbK{0} ('@client-tcs{0} @@C:Trm)) @@kC:Trm, $union('@N{0} $@&($@&(
    '@princ-msg{0} ('@tcs-princ{0} ('@client-tcs{0} @@C:Trm)), '@encrypt{0} ('@dbK-key{0} @@kT:Trm) $@&('@shK-msg{0}
    @@AKey:Trm, '@princ-msg{0} ('@tcs-princ{0} ('@client-tcs{0} @@C:Trm)))), '@encrypt{0} ('@dbK-key{0} @@kC:Trm) $@&($@&(
    '@shK-msg{0} @@AKey:Trm, '@nonce-msg{0} @@n1:Trm), '@princ-msg{0} ('@tcs-princ{0} ('@ts-tcs{0} ('@TGS-ts{0}
    @@T:Trm))))), 'F{0} @fresh':Trm))) if @@AKey:Trm := 'FRESH{0} ('@shK{0} @@C:Trm ('@TGS-ts{0} @@T:Trm)) @fresh:Trm /\
    @fresh':Trm := 'suc{0} @fresh:Trm .
@@C:Trm --> '@C{0}
@@T:Trm --> '@TS{0}
@@n1:Trm --> 'FRESH{0} '@nonce{0} ('suc{0} '0{0})
@fresh:Trm --> 'suc{0} ('suc{0} '0{0})
@@kC:Trm --> '@kC{0}
@@kT:Trm --> '@kTS{0}
@@AKey:Trm --> (unbound)
@fresh':Trm --> (unbound)
*********** solving condition fragment
@@AKey:Trm := 'FRESH{0} ('@shK{0} @@C:Trm ('@TGS-ts{0} @@T:Trm)) @fresh:Trm
*********** success for condition fragment
@@AKey:Trm := 'FRESH{0} ('@shK{0} @@C:Trm ('@TGS-ts{0} @@T:Trm)) @fresh:Trm
@@C:Trm --> '@C{0}
@@T:Trm --> '@TS{0}
@@n1:Trm --> 'FRESH{0} '@nonce{0} ('suc{0} '0{0})
@fresh:Trm --> 'suc{0} ('suc{0} '0{0})
@@kC:Trm --> '@kC{0}
@@kT:Trm --> '@kTS{0}
@@AKey:Trm --> 'FRESH{0} ('@shK{0} '@C{0} ('@TGS-ts{0} '@TS{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
@@C:Trm --> '@C{0}
@@T:Trm --> '@TS{0}
@@n1:Trm --> 'FRESH{0} '@nonce{0} ('suc{0} '0{0})
@fresh:Trm --> 'suc{0} ('suc{0} '0{0})
@@kC:Trm --> '@kC{0}
@@kT:Trm --> '@kTS{0}
@@AKey:Trm --> 'FRESH{0} ('@shK{0} '@C{0} ('@TGS-ts{0} '@TS{0})) ('suc{0} ('suc{0} '0{0}))
@fresh':Trm --> 'suc{0} ('suc{0} ('suc{0} '0{0}))
*********** success #2
*********** rule
crl $union('@N{0} $@&('@princ-msg{0} ('@tcs-princ{0} ('@client-tcs{0} @@C:Trm)), '@princ-msg{0} ('@tcs-princ{0} ('@ts-tcs{
    0} ('@TGS-ts{0} @@T:Trm))), '@nonce-msg{0} @@n1:Trm), 'F{0} @fresh:Trm, 'EL{0} ('@dbK{0} ('@client-tcs{0} @@C:Trm))
    @@kC:Trm, 'EL{0} ('@dbK{0} ('@ts-tcs{0} ('@TGS-ts{0} @@T:Trm))) @@kT:Trm) => $union('EL{0} ('@dbK{0} ('@ts-tcs{0} (
    '@TGS-ts{0} @@T:Trm))) @@kT:Trm, $union('EL{0} ('@dbK{0} ('@client-tcs{0} @@C:Trm)) @@kC:Trm, $union('@N{0} $@&($@&(
    '@princ-msg{0} ('@tcs-princ{0} ('@client-tcs{0} @@C:Trm)), '@encrypt{0} ('@dbK-key{0} @@kT:Trm) $@&('@shK-msg{0}
    @@AKey:Trm, '@princ-msg{0} ('@tcs-princ{0} ('@client-tcs{0} @@C:Trm)))), '@encrypt{0} ('@dbK-key{0} @@kC:Trm) $@&($@&(
    '@shK-msg{0} @@AKey:Trm, '@nonce-msg{0} @@n1:Trm), '@princ-msg{0} ('@tcs-princ{0} ('@ts-tcs{0} ('@TGS-ts{0}
    @@T:Trm))))), 'F{0} @fresh':Trm))) if @@AKey:Trm := 'FRESH{0} ('@shK{0} @@C:Trm ('@TGS-ts{0} @@T:Trm)) @fresh:Trm /\
    @fresh':Trm := 'suc{0} @fresh:Trm .
@@C:Trm --> '@C{0}
@@T:Trm --> '@TS{0}
@@n1:Trm --> 'FRESH{0} '@nonce{0} ('suc{0} '0{0})
@fresh:Trm --> 'suc{0} ('suc{0} '0{0})
@@kC:Trm --> '@kC{0}
@@kT:Trm --> '@kTS{0}
@@AKey:Trm --> 'FRESH{0} ('@shK{0} '@C{0} ('@TGS-ts{0} '@TS{0})) ('suc{0} ('suc{0} '0{0}))
@fresh':Trm --> 'suc{0} ('suc{0} ('suc{0} '0{0}))
Old: $union('@N{0} $@&('@princ-msg{0} ('@tcs-princ{0} ('@client-tcs{0} '@C{0})), '@princ-msg{0} ('@tcs-princ{0} ('@ts-tcs{
    0} ('@TGS-ts{0} '@TS{0}))), '@nonce-msg{0} ('FRESH{0} '@nonce{0} ('suc{0} '0{0}))), '@START-CSE{0} '@C{0}, '@START-TGE{
    0} '@C{0}, 'F{0} ('suc{0} ('suc{0} '0{0})), 'EL{0} '@KAS{0} '@AS{0}, 'EL{0} '@server{0} '@S{0}, 'EL{0} ('@dbK{0} (
    '@client-tcs{0} '@C{0})) '@kC{0}, 'EL{0} ('@dbK{0} ('@ts-tcs{0} ('@TGS-ts{0} '@TS{0}))) '@kTS{0}, 'EL{0} ('@dbK{0} (
    '@ts-tcs{0} ('@server-ts{0} '@S{0}))) '@kS{0}, 'T_clientASE_resp{0} '@C{0} ('FRESH{0} ({'_ : '@client{0}} {'_ : '@TGS{
    0}} {'_ : '@nonce{0}} '@state{0}) '0{0}), 'FRESH{0} ({'_ : '@client{0}} {'_ : '@TGS{0}} {'_ : '@nonce{0}} '@state{0})
    '0{0} '@C{0} '@TS{0} ('FRESH{0} '@nonce{0} ('suc{0} '0{0})))
$union('@N{0} $@&('@princ-msg{0} ('@tcs-princ{0} ('@client-tcs{0} '@C{0})), '@princ-msg{0} ('@tcs-princ{0} ('@ts-tcs{0} (
    '@TGS-ts{0} '@TS{0}))), '@nonce-msg{0} ('FRESH{0} '@nonce{0} ('suc{0} '0{0}))), '@START-CSE{0} '@C{0}, '@START-TGE{0}
    '@C{0}, 'F{0} ('suc{0} ('suc{0} '0{0})), 'EL{0} '@KAS{0} '@AS{0}, 'EL{0} '@server{0} '@S{0}, 'EL{0} ('@dbK{0} (
    '@client-tcs{0} '@C{0})) '@kC{0}, 'EL{0} ('@dbK{0} ('@ts-tcs{0} ('@TGS-ts{0} '@TS{0}))) '@kTS{0}, 'EL{0} ('@dbK{0} (
    '@ts-tcs{0} ('@server-ts{0} '@S{0}))) '@kS{0}, 'T_clientASE_resp{0} '@C{0} ('FRESH{0} ({'_ : '@client{0}} {'_ : '@TGS{
    0}} {'_ : '@nonce{0}} '@state{0}) '0{0}), 'FRESH{0} ({'_ : '@client{0}} {'_ : '@TGS{0}} {'_ : '@nonce{0}} '@state{0})
    '0{0} '@C{0} '@TS{0} ('FRESH{0} '@nonce{0} ('suc{0} '0{0})))
--->
$union($union('@START-CSE{0} '@C{0}, '@START-TGE{0} '@C{0}, 'EL{0} '@KAS{0} '@AS{0}, 'EL{0} '@server{0} '@S{0}, 'EL{0} (
    '@dbK{0} ('@ts-tcs{0} ('@server-ts{0} '@S{0}))) '@kS{0}, 'T_clientASE_resp{0} '@C{0} ('FRESH{0} ({'_ : '@client{0}} {'_
    : '@TGS{0}} {'_ : '@nonce{0}} '@state{0}) '0{0}), 'FRESH{0} ({'_ : '@client{0}} {'_ : '@TGS{0}} {'_ : '@nonce{0}}
    '@state{0}) '0{0} '@C{0} '@TS{0} ('FRESH{0} '@nonce{0} ('suc{0} '0{0}))), $union('EL{0} ('@dbK{0} ('@ts-tcs{0} (
    '@TGS-ts{0} '@TS{0}))) '@kTS{0}, $union('EL{0} ('@dbK{0} ('@client-tcs{0} '@C{0})) '@kC{0}, $union('@N{0} $@&($@&(
    '@princ-msg{0} ('@tcs-princ{0} ('@client-tcs{0} '@C{0})), '@encrypt{0} ('@dbK-key{0} '@kTS{0}) $@&('@shK-msg{0} (
    'FRESH{0} ('@shK{0} '@C{0} ('@TGS-ts{0} '@TS{0})) ('suc{0} ('suc{0} '0{0}))), '@princ-msg{0} ('@tcs-princ{0} (
    '@client-tcs{0} '@C{0})))), '@encrypt{0} ('@dbK-key{0} '@kC{0}) $@&($@&('@shK-msg{0} ('FRESH{0} ('@shK{0} '@C{0} (
    '@TGS-ts{0} '@TS{0})) ('suc{0} ('suc{0} '0{0}))), '@nonce-msg{0} ('FRESH{0} '@nonce{0} ('suc{0} '0{0}))), '@princ-msg{
    0} ('@tcs-princ{0} ('@ts-tcs{0} ('@TGS-ts{0} '@TS{0}))))), 'F{0} ('suc{0} ('suc{0} ('suc{0} '0{0})))))))
New: $union($union('@START-CSE{0} '@C{0}, '@START-TGE{0} '@C{0}, 'EL{0} '@KAS{0} '@AS{0}, 'EL{0} '@server{0} '@S{0}, 'EL{0}
    ('@dbK{0} ('@ts-tcs{0} ('@server-ts{0} '@S{0}))) '@kS{0}, 'T_clientASE_resp{0} '@C{0} ('FRESH{0} ({'_ : '@client{0}} {
    '_ : '@TGS{0}} {'_ : '@nonce{0}} '@state{0}) '0{0}), 'FRESH{0} ({'_ : '@client{0}} {'_ : '@TGS{0}} {'_ : '@nonce{0}}
    '@state{0}) '0{0} '@C{0} '@TS{0} ('FRESH{0} '@nonce{0} ('suc{0} '0{0}))), $union('EL{0} ('@dbK{0} ('@ts-tcs{0} (
    '@TGS-ts{0} '@TS{0}))) '@kTS{0}, $union('EL{0} ('@dbK{0} ('@client-tcs{0} '@C{0})) '@kC{0}, $union('@N{0} $@&($@&(
    '@princ-msg{0} ('@tcs-princ{0} ('@client-tcs{0} '@C{0})), '@encrypt{0} ('@dbK-key{0} '@kTS{0}) $@&('@shK-msg{0} (
    'FRESH{0} ('@shK{0} '@C{0} ('@TGS-ts{0} '@TS{0})) ('suc{0} ('suc{0} '0{0}))), '@princ-msg{0} ('@tcs-princ{0} (
    '@client-tcs{0} '@C{0})))), '@encrypt{0} ('@dbK-key{0} '@kC{0}) $@&($@&('@shK-msg{0} ('FRESH{0} ('@shK{0} '@C{0} (
    '@TGS-ts{0} '@TS{0})) ('suc{0} ('suc{0} '0{0}))), '@nonce-msg{0} ('FRESH{0} '@nonce{0} ('suc{0} '0{0}))), '@princ-msg{
    0} ('@tcs-princ{0} ('@ts-tcs{0} ('@TGS-ts{0} '@TS{0}))))), 'F{0} ('suc{0} ('suc{0} ('suc{0} '0{0})))))))
*********** trial #3
crl $union('@N{0} $@&('@princ-msg{0} ('@tcs-princ{0} ('@client-tcs{0} @@C:Trm)), @@X:Trm, '@encrypt{0} ('@dbK-key{0}
    @@kC:Trm) $@&('@shK-msg{0} @@AKey:Trm, '@nonce-msg{0} @@n1:Trm, '@princ-msg{0} ('@tcs-princ{0} ('@ts-tcs{0} ('@TGS-ts{
    0} @@T:Trm))))), 'F{0} @fresh:Trm, @@L:Trm @@C:Trm @@T:Trm @@n1:Trm) => $union('@Auth{0} @@C:Trm @@X:Trm @@T:Trm
    @@AKey:Trm, $union('F{0} @fresh':Trm, 'T_clientASE_req{0} @@C:Trm @@L:Trm)) if @@L:Trm := 'FRESH{0} ({'_ : '@client{0}}
    {'_ : '@TGS{0}} {'_ : '@nonce{0}} '@state{0}) @fresh:Trm /\ @fresh':Trm := 'suc{0} @fresh:Trm .
@@C:Trm --> '@C{0}
@@X:Trm --> '@encrypt{0} ('@dbK-key{0} '@kTS{0}) $@&('@shK-msg{0} ('FRESH{0} ('@shK{0} '@C{0} ('@TGS-ts{0} '@TS{0})) ('suc{
    0} ('suc{0} '0{0}))), '@princ-msg{0} ('@tcs-princ{0} ('@client-tcs{0} '@C{0})))
@@kC:Trm --> '@kC{0}
@@AKey:Trm --> 'FRESH{0} ('@shK{0} '@C{0} ('@TGS-ts{0} '@TS{0})) ('suc{0} ('suc{0} '0{0}))
@@n1:Trm --> 'FRESH{0} '@nonce{0} ('suc{0} '0{0})
@@T:Trm --> '@TS{0}
@fresh:Trm --> 'suc{0} ('suc{0} ('suc{0} '0{0}))
@@L:Trm --> 'FRESH{0} ({'_ : '@client{0}} {'_ : '@TGS{0}} {'_ : '@nonce{0}} '@state{0}) '0{0}
@fresh':Trm --> (unbound)
*********** solving condition fragment
@@L:Trm := 'FRESH{0} ({'_ : '@client{0}} {'_ : '@TGS{0}} {'_ : '@nonce{0}} '@state{0}) @fresh:Trm
*********** failure for condition fragment
@@L:Trm := 'FRESH{0} ({'_ : '@client{0}} {'_ : '@TGS{0}} {'_ : '@nonce{0}} '@state{0}) @fresh:Trm
*********** failure #3
*********** trial #4
crl $union('@N{0} $@&('@princ-msg{0} ('@tcs-princ{0} ('@client-tcs{0} @@C:Trm)), @@X:Trm, '@encrypt{0} ('@dbK-key{0}
    @@kC:Trm) $@&('@shK-msg{0} @@AKey:Trm, '@nonce-msg{0} @@n1:Trm, '@princ-msg{0} ('@tcs-princ{0} ('@ts-tcs{0} ('@TGS-ts{
    0} @@T:Trm))))), 'F{0} @fresh:Trm, 'T_clientASE_resp{0} @@C:Trm @@L:Trm, @@L:Trm @@C:Trm @@T:Trm @@n1:Trm) => $union(
    'F{0} @fresh':Trm, '@Auth{0} @@C:Trm @@X:Trm @@T:Trm @@AKey:Trm) if @fresh':Trm := @fresh:Trm .
@@C:Trm --> '@C{0}
@@X:Trm --> '@encrypt{0} ('@dbK-key{0} '@kTS{0}) $@&('@shK-msg{0} ('FRESH{0} ('@shK{0} '@C{0} ('@TGS-ts{0} '@TS{0})) ('suc{
    0} ('suc{0} '0{0}))), '@princ-msg{0} ('@tcs-princ{0} ('@client-tcs{0} '@C{0})))
@@kC:Trm --> '@kC{0}
@@AKey:Trm --> 'FRESH{0} ('@shK{0} '@C{0} ('@TGS-ts{0} '@TS{0})) ('suc{0} ('suc{0} '0{0}))
@@n1:Trm --> 'FRESH{0} '@nonce{0} ('suc{0} '0{0})
@@T:Trm --> '@TS{0}
@fresh:Trm --> 'suc{0} ('suc{0} ('suc{0} '0{0}))
@@L:Trm --> 'FRESH{0} ({'_ : '@client{0}} {'_ : '@TGS{0}} {'_ : '@nonce{0}} '@state{0}) '0{0}
@fresh':Trm --> (unbound)
*********** solving condition fragment
@fresh':Trm := @fresh:Trm
*********** success for condition fragment
@fresh':Trm := @fresh:Trm
@@C:Trm --> '@C{0}
@@X:Trm --> '@encrypt{0} ('@dbK-key{0} '@kTS{0}) $@&('@shK-msg{0} ('FRESH{0} ('@shK{0} '@C{0} ('@TGS-ts{0} '@TS{0})) ('suc{
    0} ('suc{0} '0{0}))), '@princ-msg{0} ('@tcs-princ{0} ('@client-tcs{0} '@C{0})))
@@kC:Trm --> '@kC{0}
@@AKey:Trm --> 'FRESH{0} ('@shK{0} '@C{0} ('@TGS-ts{0} '@TS{0})) ('suc{0} ('suc{0} '0{0}))
@@n1:Trm --> 'FRESH{0} '@nonce{0} ('suc{0} '0{0})
@@T:Trm --> '@TS{0}
@fresh:Trm --> 'suc{0} ('suc{0} ('suc{0} '0{0}))
@@L:Trm --> 'FRESH{0} ({'_ : '@client{0}} {'_ : '@TGS{0}} {'_ : '@nonce{0}} '@state{0}) '0{0}
@fresh':Trm --> 'suc{0} ('suc{0} ('suc{0} '0{0}))
*********** success #4
*********** rule
crl $union('@N{0} $@&('@princ-msg{0} ('@tcs-princ{0} ('@client-tcs{0} @@C:Trm)), @@X:Trm, '@encrypt{0} ('@dbK-key{0}
    @@kC:Trm) $@&('@shK-msg{0} @@AKey:Trm, '@nonce-msg{0} @@n1:Trm, '@princ-msg{0} ('@tcs-princ{0} ('@ts-tcs{0} ('@TGS-ts{
    0} @@T:Trm))))), 'F{0} @fresh:Trm, 'T_clientASE_resp{0} @@C:Trm @@L:Trm, @@L:Trm @@C:Trm @@T:Trm @@n1:Trm) => $union(
    'F{0} @fresh':Trm, '@Auth{0} @@C:Trm @@X:Trm @@T:Trm @@AKey:Trm) if @fresh':Trm := @fresh:Trm .
@@C:Trm --> '@C{0}
@@X:Trm --> '@encrypt{0} ('@dbK-key{0} '@kTS{0}) $@&('@shK-msg{0} ('FRESH{0} ('@shK{0} '@C{0} ('@TGS-ts{0} '@TS{0})) ('suc{
    0} ('suc{0} '0{0}))), '@princ-msg{0} ('@tcs-princ{0} ('@client-tcs{0} '@C{0})))
@@kC:Trm --> '@kC{0}
@@AKey:Trm --> 'FRESH{0} ('@shK{0} '@C{0} ('@TGS-ts{0} '@TS{0})) ('suc{0} ('suc{0} '0{0}))
@@n1:Trm --> 'FRESH{0} '@nonce{0} ('suc{0} '0{0})
@@T:Trm --> '@TS{0}
@fresh:Trm --> 'suc{0} ('suc{0} ('suc{0} '0{0}))
@@L:Trm --> 'FRESH{0} ({'_ : '@client{0}} {'_ : '@TGS{0}} {'_ : '@nonce{0}} '@state{0}) '0{0}
@fresh':Trm --> 'suc{0} ('suc{0} ('suc{0} '0{0}))
Old: $union('@N{0} $@&('@princ-msg{0} ('@tcs-princ{0} ('@client-tcs{0} '@C{0})), '@encrypt{0} ('@dbK-key{0} '@kTS{0}) $@&(
    '@shK-msg{0} ('FRESH{0} ('@shK{0} '@C{0} ('@TGS-ts{0} '@TS{0})) ('suc{0} ('suc{0} '0{0}))), '@princ-msg{0} (
    '@tcs-princ{0} ('@client-tcs{0} '@C{0}))), '@encrypt{0} ('@dbK-key{0} '@kC{0}) $@&('@shK-msg{0} ('FRESH{0} ('@shK{0}
    '@C{0} ('@TGS-ts{0} '@TS{0})) ('suc{0} ('suc{0} '0{0}))), '@nonce-msg{0} ('FRESH{0} '@nonce{0} ('suc{0} '0{0})),
    '@princ-msg{0} ('@tcs-princ{0} ('@ts-tcs{0} ('@TGS-ts{0} '@TS{0}))))), '@START-CSE{0} '@C{0}, '@START-TGE{0} '@C{0},
    'F{0} ('suc{0} ('suc{0} ('suc{0} '0{0}))), 'EL{0} '@KAS{0} '@AS{0}, 'EL{0} '@server{0} '@S{0}, 'EL{0} ('@dbK{0} (
    '@client-tcs{0} '@C{0})) '@kC{0}, 'EL{0} ('@dbK{0} ('@ts-tcs{0} ('@TGS-ts{0} '@TS{0}))) '@kTS{0}, 'EL{0} ('@dbK{0} (
    '@ts-tcs{0} ('@server-ts{0} '@S{0}))) '@kS{0}, 'T_clientASE_resp{0} '@C{0} ('FRESH{0} ({'_ : '@client{0}} {'_ : '@TGS{
    0}} {'_ : '@nonce{0}} '@state{0}) '0{0}), 'FRESH{0} ({'_ : '@client{0}} {'_ : '@TGS{0}} {'_ : '@nonce{0}} '@state{0})
    '0{0} '@C{0} '@TS{0} ('FRESH{0} '@nonce{0} ('suc{0} '0{0})))
$union('@N{0} $@&('@princ-msg{0} ('@tcs-princ{0} ('@client-tcs{0} '@C{0})), '@encrypt{0} ('@dbK-key{0} '@kTS{0}) $@&(
    '@shK-msg{0} ('FRESH{0} ('@shK{0} '@C{0} ('@TGS-ts{0} '@TS{0})) ('suc{0} ('suc{0} '0{0}))), '@princ-msg{0} (
    '@tcs-princ{0} ('@client-tcs{0} '@C{0}))), '@encrypt{0} ('@dbK-key{0} '@kC{0}) $@&('@shK-msg{0} ('FRESH{0} ('@shK{0}
    '@C{0} ('@TGS-ts{0} '@TS{0})) ('suc{0} ('suc{0} '0{0}))), '@nonce-msg{0} ('FRESH{0} '@nonce{0} ('suc{0} '0{0})),
    '@princ-msg{0} ('@tcs-princ{0} ('@ts-tcs{0} ('@TGS-ts{0} '@TS{0}))))), '@START-CSE{0} '@C{0}, '@START-TGE{0} '@C{0},
    'F{0} ('suc{0} ('suc{0} ('suc{0} '0{0}))), 'EL{0} '@KAS{0} '@AS{0}, 'EL{0} '@server{0} '@S{0}, 'EL{0} ('@dbK{0} (
    '@client-tcs{0} '@C{0})) '@kC{0}, 'EL{0} ('@dbK{0} ('@ts-tcs{0} ('@TGS-ts{0} '@TS{0}))) '@kTS{0}, 'EL{0} ('@dbK{0} (
    '@ts-tcs{0} ('@server-ts{0} '@S{0}))) '@kS{0}, 'T_clientASE_resp{0} '@C{0} ('FRESH{0} ({'_ : '@client{0}} {'_ : '@TGS{
    0}} {'_ : '@nonce{0}} '@state{0}) '0{0}), 'FRESH{0} ({'_ : '@client{0}} {'_ : '@TGS{0}} {'_ : '@nonce{0}} '@state{0})
    '0{0} '@C{0} '@TS{0} ('FRESH{0} '@nonce{0} ('suc{0} '0{0})))
--->
$union($union('@START-CSE{0} '@C{0}, '@START-TGE{0} '@C{0}, 'EL{0} '@KAS{0} '@AS{0}, 'EL{0} '@server{0} '@S{0}, 'EL{0} (
    '@dbK{0} ('@client-tcs{0} '@C{0})) '@kC{0}, 'EL{0} ('@dbK{0} ('@ts-tcs{0} ('@TGS-ts{0} '@TS{0}))) '@kTS{0}, 'EL{0} (
    '@dbK{0} ('@ts-tcs{0} ('@server-ts{0} '@S{0}))) '@kS{0}), $union('F{0} ('suc{0} ('suc{0} ('suc{0} '0{0}))), '@Auth{0}
    '@C{0} ('@encrypt{0} ('@dbK-key{0} '@kTS{0}) $@&('@shK-msg{0} ('FRESH{0} ('@shK{0} '@C{0} ('@TGS-ts{0} '@TS{0})) ('suc{
    0} ('suc{0} '0{0}))), '@princ-msg{0} ('@tcs-princ{0} ('@client-tcs{0} '@C{0})))) '@TS{0} ('FRESH{0} ('@shK{0} '@C{0} (
    '@TGS-ts{0} '@TS{0})) ('suc{0} ('suc{0} '0{0})))))
New: $union($union('@START-CSE{0} '@C{0}, '@START-TGE{0} '@C{0}, 'EL{0} '@KAS{0} '@AS{0}, 'EL{0} '@server{0} '@S{0}, 'EL{0}
    ('@dbK{0} ('@client-tcs{0} '@C{0})) '@kC{0}, 'EL{0} ('@dbK{0} ('@ts-tcs{0} ('@TGS-ts{0} '@TS{0}))) '@kTS{0}, 'EL{0} (
    '@dbK{0} ('@ts-tcs{0} ('@server-ts{0} '@S{0}))) '@kS{0}), $union('F{0} ('suc{0} ('suc{0} ('suc{0} '0{0}))), '@Auth{0}
    '@C{0} ('@encrypt{0} ('@dbK-key{0} '@kTS{0}) $@&('@shK-msg{0} ('FRESH{0} ('@shK{0} '@C{0} ('@TGS-ts{0} '@TS{0})) ('suc{
    0} ('suc{0} '0{0}))), '@princ-msg{0} ('@tcs-princ{0} ('@client-tcs{0} '@C{0})))) '@TS{0} ('FRESH{0} ('@shK{0} '@C{0} (
    '@TGS-ts{0} '@TS{0})) ('suc{0} ('suc{0} '0{0})))))
*********** trial #5
crl $union('@START-TGE{0} @@C:Trm, 'F{0} @fresh:Trm, 'EL{0} '@server{0} @@S:Trm, '@Auth{0} @@C:Trm @@X:Trm @@T:Trm
    @@AKey:Trm) => $union(@@L:Trm @@C:Trm @@S:Trm @@T:Trm @@n2:Trm, $union('@Auth{0} @@C:Trm @@X:Trm @@T:Trm @@AKey:Trm,
    $union('T_clientTGE_resp{0} @@C:Trm @@L:Trm, $union('EL{0} '@server{0} @@S:Trm, $union('@N{0} $@&($@&($@&($@&(@@X:Trm,
    '@encrypt{0} ('@shK-key{0} @@AKey:Trm) ('@princ-msg{0} ('@tcs-princ{0} ('@client-tcs{0} @@C:Trm)))), '@princ-msg{0} (
    '@tcs-princ{0} ('@client-tcs{0} @@C:Trm))), '@princ-msg{0} ('@tcs-princ{0} ('@ts-tcs{0} ('@server-ts{0} @@S:Trm)))),
    '@nonce-msg{0} @@n2:Trm), 'F{0} @fresh':Trm))))) if @@L:Trm := 'FRESH{0} ({'_ : '@client{0}} {'_ : '@server{0}} {'_ :
    '@TGS{0}} {'_ : '@nonce{0}} '@state{0}) @fresh:Trm /\ @@n2:Trm := 'FRESH{0} '@nonce{0} ('suc{0} @fresh:Trm) /\
    @fresh':Trm := 'suc{0} ('suc{0} @fresh:Trm) .
@@C:Trm --> '@C{0}
@fresh:Trm --> 'suc{0} ('suc{0} ('suc{0} '0{0}))
@@S:Trm --> '@S{0}
@@X:Trm --> '@encrypt{0} ('@dbK-key{0} '@kTS{0}) $@&('@shK-msg{0} ('FRESH{0} ('@shK{0} '@C{0} ('@TGS-ts{0} '@TS{0})) ('suc{
    0} ('suc{0} '0{0}))), '@princ-msg{0} ('@tcs-princ{0} ('@client-tcs{0} '@C{0})))
@@T:Trm --> '@TS{0}
@@AKey:Trm --> 'FRESH{0} ('@shK{0} '@C{0} ('@TGS-ts{0} '@TS{0})) ('suc{0} ('suc{0} '0{0}))
@@L:Trm --> (unbound)
@@n2:Trm --> (unbound)
@fresh':Trm --> (unbound)
*********** solving condition fragment
@@L:Trm := 'FRESH{0} ({'_ : '@client{0}} {'_ : '@server{0}} {'_ : '@TGS{0}} {'_ : '@nonce{0}} '@state{0}) @fresh:Trm
*********** success for condition fragment
@@L:Trm := 'FRESH{0} ({'_ : '@client{0}} {'_ : '@server{0}} {'_ : '@TGS{0}} {'_ : '@nonce{0}} '@state{0}) @fresh:Trm
@@C:Trm --> '@C{0}
@fresh:Trm --> 'suc{0} ('suc{0} ('suc{0} '0{0}))
@@S:Trm --> '@S{0}
@@X:Trm --> '@encrypt{0} ('@dbK-key{0} '@kTS{0}) $@&('@shK-msg{0} ('FRESH{0} ('@shK{0} '@C{0} ('@TGS-ts{0} '@TS{0})) ('suc{
    0} ('suc{0} '0{0}))), '@princ-msg{0} ('@tcs-princ{0} ('@client-tcs{0} '@C{0})))
@@T:Trm --> '@TS{0}
@@AKey:Trm --> 'FRESH{0} ('@shK{0} '@C{0} ('@TGS-ts{0} '@TS{0})) ('suc{0} ('suc{0} '0{0}))
@@L:Trm --> 'FRESH{0} ({'_ : '@client{0}} {'_ : '@server{0}} {'_ : '@TGS{0}} {'_ : '@nonce{0}} '@state{0}) ('suc{0} ('suc{
    0} ('suc{0} '0{0})))
@@n2:Trm --> (unbound)
@fresh':Trm --> (unbound)
*********** solving condition fragment
@@n2:Trm := 'FRESH{0} '@nonce{0} ('suc{0} @fresh:Trm)
*********** success for condition fragment
@@n2:Trm := 'FRESH{0} '@nonce{0} ('suc{0} @fresh:Trm)
@@C:Trm --> '@C{0}
@fresh:Trm --> 'suc{0} ('suc{0} ('suc{0} '0{0}))
@@S:Trm --> '@S{0}
@@X:Trm --> '@encrypt{0} ('@dbK-key{0} '@kTS{0}) $@&('@shK-msg{0} ('FRESH{0} ('@shK{0} '@C{0} ('@TGS-ts{0} '@TS{0})) ('suc{
    0} ('suc{0} '0{0}))), '@princ-msg{0} ('@tcs-princ{0} ('@client-tcs{0} '@C{0})))
@@T:Trm --> '@TS{0}
@@AKey:Trm --> 'FRESH{0} ('@shK{0} '@C{0} ('@TGS-ts{0} '@TS{0})) ('suc{0} ('suc{0} '0{0}))
@@L:Trm --> 'FRESH{0} ({'_ : '@client{0}} {'_ : '@server{0}} {'_ : '@TGS{0}} {'_ : '@nonce{0}} '@state{0}) ('suc{0} ('suc{
    0} ('suc{0} '0{0})))
@@n2: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)
@@C:Trm --> '@C{0}
@fresh:Trm --> 'suc{0} ('suc{0} ('suc{0} '0{0}))
@@S:Trm --> '@S{0}
@@X:Trm --> '@encrypt{0} ('@dbK-key{0} '@kTS{0}) $@&('@shK-msg{0} ('FRESH{0} ('@shK{0} '@C{0} ('@TGS-ts{0} '@TS{0})) ('suc{
    0} ('suc{0} '0{0}))), '@princ-msg{0} ('@tcs-princ{0} ('@client-tcs{0} '@C{0})))
@@T:Trm --> '@TS{0}
@@AKey:Trm --> 'FRESH{0} ('@shK{0} '@C{0} ('@TGS-ts{0} '@TS{0})) ('suc{0} ('suc{0} '0{0}))
@@L:Trm --> 'FRESH{0} ({'_ : '@client{0}} {'_ : '@server{0}} {'_ : '@TGS{0}} {'_ : '@nonce{0}} '@state{0}) ('suc{0} ('suc{
    0} ('suc{0} '0{0})))
@@n2: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 #5
*********** rule
crl $union('@START-TGE{0} @@C:Trm, 'F{0} @fresh:Trm, 'EL{0} '@server{0} @@S:Trm, '@Auth{0} @@C:Trm @@X:Trm @@T:Trm
    @@AKey:Trm) => $union(@@L:Trm @@C:Trm @@S:Trm @@T:Trm @@n2:Trm, $union('@Auth{0} @@C:Trm @@X:Trm @@T:Trm @@AKey:Trm,
    $union('T_clientTGE_resp{0} @@C:Trm @@L:Trm, $union('EL{0} '@server{0} @@S:Trm, $union('@N{0} $@&($@&($@&($@&(@@X:Trm,
    '@encrypt{0} ('@shK-key{0} @@AKey:Trm) ('@princ-msg{0} ('@tcs-princ{0} ('@client-tcs{0} @@C:Trm)))), '@princ-msg{0} (
    '@tcs-princ{0} ('@client-tcs{0} @@C:Trm))), '@princ-msg{0} ('@tcs-princ{0} ('@ts-tcs{0} ('@server-ts{0} @@S:Trm)))),
    '@nonce-msg{0} @@n2:Trm), 'F{0} @fresh':Trm))))) if @@L:Trm := 'FRESH{0} ({'_ : '@client{0}} {'_ : '@server{0}} {'_ :
    '@TGS{0}} {'_ : '@nonce{0}} '@state{0}) @fresh:Trm /\ @@n2:Trm := 'FRESH{0} '@nonce{0} ('suc{0} @fresh:Trm) /\
    @fresh':Trm := 'suc{0} ('suc{0} @fresh:Trm) .
@@C:Trm --> '@C{0}
@fresh:Trm --> 'suc{0} ('suc{0} ('suc{0} '0{0}))
@@S:Trm --> '@S{0}
@@X:Trm --> '@encrypt{0} ('@dbK-key{0} '@kTS{0}) $@&('@shK-msg{0} ('FRESH{0} ('@shK{0} '@C{0} ('@TGS-ts{0} '@TS{0})) ('suc{
    0} ('suc{0} '0{0}))), '@princ-msg{0} ('@tcs-princ{0} ('@client-tcs{0} '@C{0})))
@@T:Trm --> '@TS{0}
@@AKey:Trm --> 'FRESH{0} ('@shK{0} '@C{0} ('@TGS-ts{0} '@TS{0})) ('suc{0} ('suc{0} '0{0}))
@@L:Trm --> 'FRESH{0} ({'_ : '@client{0}} {'_ : '@server{0}} {'_ : '@TGS{0}} {'_ : '@nonce{0}} '@state{0}) ('suc{0} ('suc{
    0} ('suc{0} '0{0})))
@@n2: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('@START-CSE{0} '@C{0}, '@START-TGE{0} '@C{0}, 'F{0} ('suc{0} ('suc{0} ('suc{0} '0{0}))), 'EL{0} '@KAS{0} '@AS{
    0}, 'EL{0} '@server{0} '@S{0}, 'EL{0} ('@dbK{0} ('@client-tcs{0} '@C{0})) '@kC{0}, 'EL{0} ('@dbK{0} ('@ts-tcs{0} (
    '@TGS-ts{0} '@TS{0}))) '@kTS{0}, 'EL{0} ('@dbK{0} ('@ts-tcs{0} ('@server-ts{0} '@S{0}))) '@kS{0}, '@Auth{0} '@C{0} (
    '@encrypt{0} ('@dbK-key{0} '@kTS{0}) $@&('@shK-msg{0} ('FRESH{0} ('@shK{0} '@C{0} ('@TGS-ts{0} '@TS{0})) ('suc{0} (
    'suc{0} '0{0}))), '@princ-msg{0} ('@tcs-princ{0} ('@client-tcs{0} '@C{0})))) '@TS{0} ('FRESH{0} ('@shK{0} '@C{0} (
    '@TGS-ts{0} '@TS{0})) ('suc{0} ('suc{0} '0{0}))))
$union('@START-CSE{0} '@C{0}, '@START-TGE{0} '@C{0}, 'F{0} ('suc{0} ('suc{0} ('suc{0} '0{0}))), 'EL{0} '@KAS{0} '@AS{0},
    'EL{0} '@server{0} '@S{0}, 'EL{0} ('@dbK{0} ('@client-tcs{0} '@C{0})) '@kC{0}, 'EL{0} ('@dbK{0} ('@ts-tcs{0} ('@TGS-ts{
    0} '@TS{0}))) '@kTS{0}, 'EL{0} ('@dbK{0} ('@ts-tcs{0} ('@server-ts{0} '@S{0}))) '@kS{0}, '@Auth{0} '@C{0} ('@encrypt{0}
    ('@dbK-key{0} '@kTS{0}) $@&('@shK-msg{0} ('FRESH{0} ('@shK{0} '@C{0} ('@TGS-ts{0} '@TS{0})) ('suc{0} ('suc{0} '0{0}))),
    '@princ-msg{0} ('@tcs-princ{0} ('@client-tcs{0} '@C{0})))) '@TS{0} ('FRESH{0} ('@shK{0} '@C{0} ('@TGS-ts{0} '@TS{0})) (
    'suc{0} ('suc{0} '0{0}))))
--->
$union($union('@START-CSE{0} '@C{0}, 'EL{0} '@KAS{0} '@AS{0}, 'EL{0} ('@dbK{0} ('@client-tcs{0} '@C{0})) '@kC{0}, 'EL{0} (
    '@dbK{0} ('@ts-tcs{0} ('@TGS-ts{0} '@TS{0}))) '@kTS{0}, 'EL{0} ('@dbK{0} ('@ts-tcs{0} ('@server-ts{0} '@S{0}))) '@kS{
    0}), $union('FRESH{0} ({'_ : '@client{0}} {'_ : '@server{0}} {'_ : '@TGS{0}} {'_ : '@nonce{0}} '@state{0}) ('suc{0} (
    'suc{0} ('suc{0} '0{0}))) '@C{0} '@S{0} '@TS{0} ('FRESH{0} '@nonce{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0}))))),
    $union('@Auth{0} '@C{0} ('@encrypt{0} ('@dbK-key{0} '@kTS{0}) $@&('@shK-msg{0} ('FRESH{0} ('@shK{0} '@C{0} ('@TGS-ts{0}
    '@TS{0})) ('suc{0} ('suc{0} '0{0}))), '@princ-msg{0} ('@tcs-princ{0} ('@client-tcs{0} '@C{0})))) '@TS{0} ('FRESH{0} (
    '@shK{0} '@C{0} ('@TGS-ts{0} '@TS{0})) ('suc{0} ('suc{0} '0{0}))), $union('T_clientTGE_resp{0} '@C{0} ('FRESH{0} ({'_ :
    '@client{0}} {'_ : '@server{0}} {'_ : '@TGS{0}} {'_ : '@nonce{0}} '@state{0}) ('suc{0} ('suc{0} ('suc{0} '0{0})))),
    $union('EL{0} '@server{0} '@S{0}, $union('@N{0} $@&($@&($@&($@&('@encrypt{0} ('@dbK-key{0} '@kTS{0}) $@&('@shK-msg{0} (
    'FRESH{0} ('@shK{0} '@C{0} ('@TGS-ts{0} '@TS{0})) ('suc{0} ('suc{0} '0{0}))), '@princ-msg{0} ('@tcs-princ{0} (
    '@client-tcs{0} '@C{0}))), '@encrypt{0} ('@shK-key{0} ('FRESH{0} ('@shK{0} '@C{0} ('@TGS-ts{0} '@TS{0})) ('suc{0} (
    'suc{0} '0{0})))) ('@princ-msg{0} ('@tcs-princ{0} ('@client-tcs{0} '@C{0})))), '@princ-msg{0} ('@tcs-princ{0} (
    '@client-tcs{0} '@C{0}))), '@princ-msg{0} ('@tcs-princ{0} ('@ts-tcs{0} ('@server-ts{0} '@S{0})))), '@nonce-msg{0} (
    'FRESH{0} '@nonce{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0})))))), 'F{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{
    0} '0{0})))))))))))
New: $union($union('@START-CSE{0} '@C{0}, 'EL{0} '@KAS{0} '@AS{0}, 'EL{0} ('@dbK{0} ('@client-tcs{0} '@C{0})) '@kC{0}, 'EL{
    0} ('@dbK{0} ('@ts-tcs{0} ('@TGS-ts{0} '@TS{0}))) '@kTS{0}, 'EL{0} ('@dbK{0} ('@ts-tcs{0} ('@server-ts{0} '@S{0})))
    '@kS{0}), $union('FRESH{0} ({'_ : '@client{0}} {'_ : '@server{0}} {'_ : '@TGS{0}} {'_ : '@nonce{0}} '@state{0}) ('suc{
    0} ('suc{0} ('suc{0} '0{0}))) '@C{0} '@S{0} '@TS{0} ('FRESH{0} '@nonce{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{
    0}))))), $union('@Auth{0} '@C{0} ('@encrypt{0} ('@dbK-key{0} '@kTS{0}) $@&('@shK-msg{0} ('FRESH{0} ('@shK{0} '@C{0} (
    '@TGS-ts{0} '@TS{0})) ('suc{0} ('suc{0} '0{0}))), '@princ-msg{0} ('@tcs-princ{0} ('@client-tcs{0} '@C{0})))) '@TS{0} (
    'FRESH{0} ('@shK{0} '@C{0} ('@TGS-ts{0} '@TS{0})) ('suc{0} ('suc{0} '0{0}))), $union('T_clientTGE_resp{0} '@C{0} (
    'FRESH{0} ({'_ : '@client{0}} {'_ : '@server{0}} {'_ : '@TGS{0}} {'_ : '@nonce{0}} '@state{0}) ('suc{0} ('suc{0} ('suc{
    0} '0{0})))), $union('EL{0} '@server{0} '@S{0}, $union('@N{0} $@&($@&($@&($@&('@encrypt{0} ('@dbK-key{0} '@kTS{0}) $@&(
    '@shK-msg{0} ('FRESH{0} ('@shK{0} '@C{0} ('@TGS-ts{0} '@TS{0})) ('suc{0} ('suc{0} '0{0}))), '@princ-msg{0} (
    '@tcs-princ{0} ('@client-tcs{0} '@C{0}))), '@encrypt{0} ('@shK-key{0} ('FRESH{0} ('@shK{0} '@C{0} ('@TGS-ts{0} '@TS{
    0})) ('suc{0} ('suc{0} '0{0})))) ('@princ-msg{0} ('@tcs-princ{0} ('@client-tcs{0} '@C{0})))), '@princ-msg{0} (
    '@tcs-princ{0} ('@client-tcs{0} '@C{0}))), '@princ-msg{0} ('@tcs-princ{0} ('@ts-tcs{0} ('@server-ts{0} '@S{0})))),
    '@nonce-msg{0} ('FRESH{0} '@nonce{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0})))))), 'F{0} ('suc{0} ('suc{0} ('suc{0}
    ('suc{0} ('suc{0} '0{0})))))))))))
*********** trial #6
crl $union('@N{0} $@&('@encrypt{0} ('@dbK-key{0} @@kT:Trm) $@&('@shK-msg{0} @@AKey:Trm, '@princ-msg{0} ('@tcs-princ{0} (
    '@client-tcs{0} @@C:Trm))), '@encrypt{0} ('@shK-key{0} @@AKey:Trm) ('@princ-msg{0} ('@tcs-princ{0} ('@client-tcs{0}
    @@C:Trm))), '@princ-msg{0} ('@tcs-princ{0} ('@client-tcs{0} @@C:Trm)), '@princ-msg{0} ('@tcs-princ{0} ('@ts-tcs{0} (
    '@server-ts{0} @@S:Trm))), '@nonce-msg{0} @@n2:Trm), 'F{0} @fresh:Trm, 'EL{0} ('@dbK{0} ('@ts-tcs{0} ('@server-ts{0}
    @@S:Trm))) @@kS:Trm) => $union('EL{0} ('@dbK{0} ('@ts-tcs{0} ('@server-ts{0} @@S:Trm))) @@kS:Trm, $union('@N{0} $@&(
    $@&('@princ-msg{0} ('@tcs-princ{0} ('@client-tcs{0} @@C:Trm)), '@encrypt{0} ('@dbK-key{0} @@kS:Trm) $@&('@shK-msg{0}
    @@SKey:Trm, '@princ-msg{0} ('@tcs-princ{0} ('@client-tcs{0} @@C:Trm)))), '@encrypt{0} ('@shK-key{0} @@AKey:Trm) $@&(
    $@&('@shK-msg{0} @@SKey:Trm, '@nonce-msg{0} @@n2:Trm), '@princ-msg{0} ('@tcs-princ{0} ('@ts-tcs{0} ('@server-ts{0}
    @@S:Trm))))), 'F{0} @fresh':Trm)) if @@SKey:Trm := 'FRESH{0} ('@shK{0} @@C:Trm ('@server-ts{0} @@S:Trm)) @fresh:Trm /\
    @fresh':Trm := 'suc{0} @fresh:Trm .
@@kT:Trm --> '@kTS{0}
@@AKey:Trm --> 'FRESH{0} ('@shK{0} '@C{0} ('@TGS-ts{0} '@TS{0})) ('suc{0} ('suc{0} '0{0}))
@@C:Trm --> '@C{0}
@@S:Trm --> '@S{0}
@@n2: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}))))
@@kS:Trm --> '@kS{0}
@@SKey:Trm --> (unbound)
@fresh':Trm --> (unbound)
*********** solving condition fragment
@@SKey:Trm := 'FRESH{0} ('@shK{0} @@C:Trm ('@server-ts{0} @@S:Trm)) @fresh:Trm
*********** success for condition fragment
@@SKey:Trm := 'FRESH{0} ('@shK{0} @@C:Trm ('@server-ts{0} @@S:Trm)) @fresh:Trm
@@kT:Trm --> '@kTS{0}
@@AKey:Trm --> 'FRESH{0} ('@shK{0} '@C{0} ('@TGS-ts{0} '@TS{0})) ('suc{0} ('suc{0} '0{0}))
@@C:Trm --> '@C{0}
@@S:Trm --> '@S{0}
@@n2: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}))))
@@kS:Trm --> '@kS{0}
@@SKey:Trm --> 'FRESH{0} ('@shK{0} '@C{0} ('@server-ts{0} '@S{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
@@kT:Trm --> '@kTS{0}
@@AKey:Trm --> 'FRESH{0} ('@shK{0} '@C{0} ('@TGS-ts{0} '@TS{0})) ('suc{0} ('suc{0} '0{0}))
@@C:Trm --> '@C{0}
@@S:Trm --> '@S{0}
@@n2: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}))))
@@kS:Trm --> '@kS{0}
@@SKey:Trm --> 'FRESH{0} ('@shK{0} '@C{0} ('@server-ts{0} '@S{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 #6
*********** rule
crl $union('@N{0} $@&('@encrypt{0} ('@dbK-key{0} @@kT:Trm) $@&('@shK-msg{0} @@AKey:Trm, '@princ-msg{0} ('@tcs-princ{0} (
    '@client-tcs{0} @@C:Trm))), '@encrypt{0} ('@shK-key{0} @@AKey:Trm) ('@princ-msg{0} ('@tcs-princ{0} ('@client-tcs{0}
    @@C:Trm))), '@princ-msg{0} ('@tcs-princ{0} ('@client-tcs{0} @@C:Trm)), '@princ-msg{0} ('@tcs-princ{0} ('@ts-tcs{0} (
    '@server-ts{0} @@S:Trm))), '@nonce-msg{0} @@n2:Trm), 'F{0} @fresh:Trm, 'EL{0} ('@dbK{0} ('@ts-tcs{0} ('@server-ts{0}
    @@S:Trm))) @@kS:Trm) => $union('EL{0} ('@dbK{0} ('@ts-tcs{0} ('@server-ts{0} @@S:Trm))) @@kS:Trm, $union('@N{0} $@&(
    $@&('@princ-msg{0} ('@tcs-princ{0} ('@client-tcs{0} @@C:Trm)), '@encrypt{0} ('@dbK-key{0} @@kS:Trm) $@&('@shK-msg{0}
    @@SKey:Trm, '@princ-msg{0} ('@tcs-princ{0} ('@client-tcs{0} @@C:Trm)))), '@encrypt{0} ('@shK-key{0} @@AKey:Trm) $@&(
    $@&('@shK-msg{0} @@SKey:Trm, '@nonce-msg{0} @@n2:Trm), '@princ-msg{0} ('@tcs-princ{0} ('@ts-tcs{0} ('@server-ts{0}
    @@S:Trm))))), 'F{0} @fresh':Trm)) if @@SKey:Trm := 'FRESH{0} ('@shK{0} @@C:Trm ('@server-ts{0} @@S:Trm)) @fresh:Trm /\
    @fresh':Trm := 'suc{0} @fresh:Trm .
@@kT:Trm --> '@kTS{0}
@@AKey:Trm --> 'FRESH{0} ('@shK{0} '@C{0} ('@TGS-ts{0} '@TS{0})) ('suc{0} ('suc{0} '0{0}))
@@C:Trm --> '@C{0}
@@S:Trm --> '@S{0}
@@n2: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}))))
@@kS:Trm --> '@kS{0}
@@SKey:Trm --> 'FRESH{0} ('@shK{0} '@C{0} ('@server-ts{0} '@S{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} $@&('@encrypt{0} ('@dbK-key{0} '@kTS{0}) $@&('@shK-msg{0} ('FRESH{0} ('@shK{0} '@C{0} ('@TGS-ts{0} '@TS{
    0})) ('suc{0} ('suc{0} '0{0}))), '@princ-msg{0} ('@tcs-princ{0} ('@client-tcs{0} '@C{0}))), '@encrypt{0} ('@shK-key{0}
    ('FRESH{0} ('@shK{0} '@C{0} ('@TGS-ts{0} '@TS{0})) ('suc{0} ('suc{0} '0{0})))) ('@princ-msg{0} ('@tcs-princ{0} (
    '@client-tcs{0} '@C{0}))), '@princ-msg{0} ('@tcs-princ{0} ('@client-tcs{0} '@C{0})), '@princ-msg{0} ('@tcs-princ{0} (
    '@ts-tcs{0} ('@server-ts{0} '@S{0}))), '@nonce-msg{0} ('FRESH{0} '@nonce{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{
    0})))))), '@START-CSE{0} '@C{0}, 'F{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0}))))), 'EL{0} '@KAS{0} '@AS{
    0}, 'EL{0} '@server{0} '@S{0}, 'EL{0} ('@dbK{0} ('@client-tcs{0} '@C{0})) '@kC{0}, 'EL{0} ('@dbK{0} ('@ts-tcs{0} (
    '@TGS-ts{0} '@TS{0}))) '@kTS{0}, 'EL{0} ('@dbK{0} ('@ts-tcs{0} ('@server-ts{0} '@S{0}))) '@kS{0}, 'T_clientTGE_resp{0}
    '@C{0} ('FRESH{0} ({'_ : '@client{0}} {'_ : '@server{0}} {'_ : '@TGS{0}} {'_ : '@nonce{0}} '@state{0}) ('suc{0} ('suc{
    0} ('suc{0} '0{0})))), '@Auth{0} '@C{0} ('@encrypt{0} ('@dbK-key{0} '@kTS{0}) $@&('@shK-msg{0} ('FRESH{0} ('@shK{0}
    '@C{0} ('@TGS-ts{0} '@TS{0})) ('suc{0} ('suc{0} '0{0}))), '@princ-msg{0} ('@tcs-princ{0} ('@client-tcs{0} '@C{0}))))
    '@TS{0} ('FRESH{0} ('@shK{0} '@C{0} ('@TGS-ts{0} '@TS{0})) ('suc{0} ('suc{0} '0{0}))), 'FRESH{0} ({'_ : '@client{0}} {
    '_ : '@server{0}} {'_ : '@TGS{0}} {'_ : '@nonce{0}} '@state{0}) ('suc{0} ('suc{0} ('suc{0} '0{0}))) '@C{0} '@S{0} '@TS{
    0} ('FRESH{0} '@nonce{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0}))))))
$union('@N{0} $@&('@encrypt{0} ('@dbK-key{0} '@kTS{0}) $@&('@shK-msg{0} ('FRESH{0} ('@shK{0} '@C{0} ('@TGS-ts{0} '@TS{0}))
    ('suc{0} ('suc{0} '0{0}))), '@princ-msg{0} ('@tcs-princ{0} ('@client-tcs{0} '@C{0}))), '@encrypt{0} ('@shK-key{0} (
    'FRESH{0} ('@shK{0} '@C{0} ('@TGS-ts{0} '@TS{0})) ('suc{0} ('suc{0} '0{0})))) ('@princ-msg{0} ('@tcs-princ{0} (
    '@client-tcs{0} '@C{0}))), '@princ-msg{0} ('@tcs-princ{0} ('@client-tcs{0} '@C{0})), '@princ-msg{0} ('@tcs-princ{0} (
    '@ts-tcs{0} ('@server-ts{0} '@S{0}))), '@nonce-msg{0} ('FRESH{0} '@nonce{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{
    0})))))), '@START-CSE{0} '@C{0}, 'F{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0}))))), 'EL{0} '@KAS{0} '@AS{
    0}, 'EL{0} '@server{0} '@S{0}, 'EL{0} ('@dbK{0} ('@client-tcs{0} '@C{0})) '@kC{0}, 'EL{0} ('@dbK{0} ('@ts-tcs{0} (
    '@TGS-ts{0} '@TS{0}))) '@kTS{0}, 'EL{0} ('@dbK{0} ('@ts-tcs{0} ('@server-ts{0} '@S{0}))) '@kS{0}, 'T_clientTGE_resp{0}
    '@C{0} ('FRESH{0} ({'_ : '@client{0}} {'_ : '@server{0}} {'_ : '@TGS{0}} {'_ : '@nonce{0}} '@state{0}) ('suc{0} ('suc{
    0} ('suc{0} '0{0})))), '@Auth{0} '@C{0} ('@encrypt{0} ('@dbK-key{0} '@kTS{0}) $@&('@shK-msg{0} ('FRESH{0} ('@shK{0}
    '@C{0} ('@TGS-ts{0} '@TS{0})) ('suc{0} ('suc{0} '0{0}))), '@princ-msg{0} ('@tcs-princ{0} ('@client-tcs{0} '@C{0}))))
    '@TS{0} ('FRESH{0} ('@shK{0} '@C{0} ('@TGS-ts{0} '@TS{0})) ('suc{0} ('suc{0} '0{0}))), 'FRESH{0} ({'_ : '@client{0}} {
    '_ : '@server{0}} {'_ : '@TGS{0}} {'_ : '@nonce{0}} '@state{0}) ('suc{0} ('suc{0} ('suc{0} '0{0}))) '@C{0} '@S{0} '@TS{
    0} ('FRESH{0} '@nonce{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0}))))))
--->
$union($union('@START-CSE{0} '@C{0}, 'EL{0} '@KAS{0} '@AS{0}, 'EL{0} '@server{0} '@S{0}, 'EL{0} ('@dbK{0} ('@client-tcs{0}
    '@C{0})) '@kC{0}, 'EL{0} ('@dbK{0} ('@ts-tcs{0} ('@TGS-ts{0} '@TS{0}))) '@kTS{0}, 'T_clientTGE_resp{0} '@C{0} ('FRESH{
    0} ({'_ : '@client{0}} {'_ : '@server{0}} {'_ : '@TGS{0}} {'_ : '@nonce{0}} '@state{0}) ('suc{0} ('suc{0} ('suc{0} '0{
    0})))), '@Auth{0} '@C{0} ('@encrypt{0} ('@dbK-key{0} '@kTS{0}) $@&('@shK-msg{0} ('FRESH{0} ('@shK{0} '@C{0} ('@TGS-ts{
    0} '@TS{0})) ('suc{0} ('suc{0} '0{0}))), '@princ-msg{0} ('@tcs-princ{0} ('@client-tcs{0} '@C{0})))) '@TS{0} ('FRESH{0}
    ('@shK{0} '@C{0} ('@TGS-ts{0} '@TS{0})) ('suc{0} ('suc{0} '0{0}))), 'FRESH{0} ({'_ : '@client{0}} {'_ : '@server{0}} {
    '_ : '@TGS{0}} {'_ : '@nonce{0}} '@state{0}) ('suc{0} ('suc{0} ('suc{0} '0{0}))) '@C{0} '@S{0} '@TS{0} ('FRESH{0}
    '@nonce{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0})))))), $union('EL{0} ('@dbK{0} ('@ts-tcs{0} ('@server-ts{0} '@S{
    0}))) '@kS{0}, $union('@N{0} $@&($@&('@princ-msg{0} ('@tcs-princ{0} ('@client-tcs{0} '@C{0})), '@encrypt{0} ('@dbK-key{
    0} '@kS{0}) $@&('@shK-msg{0} ('FRESH{0} ('@shK{0} '@C{0} ('@server-ts{0} '@S{0})) ('suc{0} ('suc{0} ('suc{0} ('suc{0} (
    'suc{0} '0{0})))))), '@princ-msg{0} ('@tcs-princ{0} ('@client-tcs{0} '@C{0})))), '@encrypt{0} ('@shK-key{0} ('FRESH{0}
    ('@shK{0} '@C{0} ('@TGS-ts{0} '@TS{0})) ('suc{0} ('suc{0} '0{0})))) $@&($@&('@shK-msg{0} ('FRESH{0} ('@shK{0} '@C{0} (
    '@server-ts{0} '@S{0})) ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0})))))), '@nonce-msg{0} ('FRESH{0} '@nonce{0}
    ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0})))))), '@princ-msg{0} ('@tcs-princ{0} ('@ts-tcs{0} ('@server-ts{0} '@S{
    0}))))), 'F{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0})))))))))
New: $union($union('@START-CSE{0} '@C{0}, 'EL{0} '@KAS{0} '@AS{0}, 'EL{0} '@server{0} '@S{0}, 'EL{0} ('@dbK{0} (
    '@client-tcs{0} '@C{0})) '@kC{0}, 'EL{0} ('@dbK{0} ('@ts-tcs{0} ('@TGS-ts{0} '@TS{0}))) '@kTS{0}, 'T_clientTGE_resp{0}
    '@C{0} ('FRESH{0} ({'_ : '@client{0}} {'_ : '@server{0}} {'_ : '@TGS{0}} {'_ : '@nonce{0}} '@state{0}) ('suc{0} ('suc{
    0} ('suc{0} '0{0})))), '@Auth{0} '@C{0} ('@encrypt{0} ('@dbK-key{0} '@kTS{0}) $@&('@shK-msg{0} ('FRESH{0} ('@shK{0}
    '@C{0} ('@TGS-ts{0} '@TS{0})) ('suc{0} ('suc{0} '0{0}))), '@princ-msg{0} ('@tcs-princ{0} ('@client-tcs{0} '@C{0}))))
    '@TS{0} ('FRESH{0} ('@shK{0} '@C{0} ('@TGS-ts{0} '@TS{0})) ('suc{0} ('suc{0} '0{0}))), 'FRESH{0} ({'_ : '@client{0}} {
    '_ : '@server{0}} {'_ : '@TGS{0}} {'_ : '@nonce{0}} '@state{0}) ('suc{0} ('suc{0} ('suc{0} '0{0}))) '@C{0} '@S{0} '@TS{
    0} ('FRESH{0} '@nonce{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0})))))), $union('EL{0} ('@dbK{0} ('@ts-tcs{0} (
    '@server-ts{0} '@S{0}))) '@kS{0}, $union('@N{0} $@&($@&('@princ-msg{0} ('@tcs-princ{0} ('@client-tcs{0} '@C{0})),
    '@encrypt{0} ('@dbK-key{0} '@kS{0}) $@&('@shK-msg{0} ('FRESH{0} ('@shK{0} '@C{0} ('@server-ts{0} '@S{0})) ('suc{0} (
    'suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0})))))), '@princ-msg{0} ('@tcs-princ{0} ('@client-tcs{0} '@C{0})))), '@encrypt{
    0} ('@shK-key{0} ('FRESH{0} ('@shK{0} '@C{0} ('@TGS-ts{0} '@TS{0})) ('suc{0} ('suc{0} '0{0})))) $@&($@&('@shK-msg{0} (
    'FRESH{0} ('@shK{0} '@C{0} ('@server-ts{0} '@S{0})) ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0})))))),
    '@nonce-msg{0} ('FRESH{0} '@nonce{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0})))))), '@princ-msg{0} ('@tcs-princ{0} (
    '@ts-tcs{0} ('@server-ts{0} '@S{0}))))), 'F{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0})))))))))
*********** trial #7
crl $union('@N{0} $@&('@princ-msg{0} ('@tcs-princ{0} ('@client-tcs{0} @@C:Trm)), @@Y:Trm, '@encrypt{0} ('@shK-key{0}
    @@AKey:Trm) $@&('@shK-msg{0} @@SKey:Trm, '@nonce-msg{0} @@n2:Trm, '@princ-msg{0} ('@tcs-princ{0} ('@ts-tcs{0} (
    '@server-ts{0} @@S:Trm))))), 'F{0} @fresh:Trm, @@L:Trm @@C:Trm @@S:Trm @@T:Trm @@n2:Trm) => $union('@Service{0} @@C:Trm
    @@Y:Trm @@S:Trm @@SKey:Trm, $union('F{0} @fresh':Trm, 'T_clientTGE_req{0} @@C:Trm @@L:Trm)) if @@L:Trm := 'FRESH{0} ({
    '_ : '@client{0}} {'_ : '@server{0}} {'_ : '@TGS{0}} {'_ : '@nonce{0}} '@state{0}) @fresh:Trm /\ @fresh':Trm := 'suc{0}
    @fresh:Trm .
@@C:Trm --> '@C{0}
@@Y:Trm --> '@encrypt{0} ('@dbK-key{0} '@kS{0}) $@&('@shK-msg{0} ('FRESH{0} ('@shK{0} '@C{0} ('@server-ts{0} '@S{0})) (
    'suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0})))))), '@princ-msg{0} ('@tcs-princ{0} ('@client-tcs{0} '@C{0})))
@@AKey:Trm --> 'FRESH{0} ('@shK{0} '@C{0} ('@TGS-ts{0} '@TS{0})) ('suc{0} ('suc{0} '0{0}))
@@SKey:Trm --> 'FRESH{0} ('@shK{0} '@C{0} ('@server-ts{0} '@S{0})) ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0})))))
@@n2:Trm --> 'FRESH{0} '@nonce{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0}))))
@@S:Trm --> '@S{0}
@fresh:Trm --> 'suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0})))))
@@L:Trm --> 'FRESH{0} ({'_ : '@client{0}} {'_ : '@server{0}} {'_ : '@TGS{0}} {'_ : '@nonce{0}} '@state{0}) ('suc{0} ('suc{
    0} ('suc{0} '0{0})))
@@T:Trm --> '@TS{0}
@fresh':Trm --> (unbound)
*********** solving condition fragment
@@L:Trm := 'FRESH{0} ({'_ : '@client{0}} {'_ : '@server{0}} {'_ : '@TGS{0}} {'_ : '@nonce{0}} '@state{0}) @fresh:Trm
*********** failure for condition fragment
@@L:Trm := 'FRESH{0} ({'_ : '@client{0}} {'_ : '@server{0}} {'_ : '@TGS{0}} {'_ : '@nonce{0}} '@state{0}) @fresh:Trm
*********** failure #7
*********** trial #8
crl $union('@N{0} $@&('@princ-msg{0} ('@tcs-princ{0} ('@client-tcs{0} @@C:Trm)), @@Y:Trm, '@encrypt{0} ('@shK-key{0}
    @@AKey:Trm) $@&('@shK-msg{0} @@SKey:Trm, '@nonce-msg{0} @@n2:Trm, '@princ-msg{0} ('@tcs-princ{0} ('@ts-tcs{0} (
    '@server-ts{0} @@S:Trm))))), 'F{0} @fresh:Trm, 'T_clientTGE_resp{0} @@C:Trm @@L:Trm, @@L:Trm @@C:Trm @@S:Trm @@T:Trm
    @@n2:Trm) => $union('F{0} @fresh':Trm, '@Service{0} @@C:Trm @@Y:Trm @@S:Trm @@SKey:Trm) if @fresh':Trm := @fresh:Trm .
@@C:Trm --> '@C{0}
@@Y:Trm --> '@encrypt{0} ('@dbK-key{0} '@kS{0}) $@&('@shK-msg{0} ('FRESH{0} ('@shK{0} '@C{0} ('@server-ts{0} '@S{0})) (
    'suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0})))))), '@princ-msg{0} ('@tcs-princ{0} ('@client-tcs{0} '@C{0})))
@@AKey:Trm --> 'FRESH{0} ('@shK{0} '@C{0} ('@TGS-ts{0} '@TS{0})) ('suc{0} ('suc{0} '0{0}))
@@SKey:Trm --> 'FRESH{0} ('@shK{0} '@C{0} ('@server-ts{0} '@S{0})) ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0})))))
@@n2:Trm --> 'FRESH{0} '@nonce{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0}))))
@@S:Trm --> '@S{0}
@fresh:Trm --> 'suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0})))))
@@L:Trm --> 'FRESH{0} ({'_ : '@client{0}} {'_ : '@server{0}} {'_ : '@TGS{0}} {'_ : '@nonce{0}} '@state{0}) ('suc{0} ('suc{
    0} ('suc{0} '0{0})))
@@T:Trm --> '@TS{0}
@fresh':Trm --> (unbound)
*********** solving condition fragment
@fresh':Trm := @fresh:Trm
*********** success for condition fragment
@fresh':Trm := @fresh:Trm
@@C:Trm --> '@C{0}
@@Y:Trm --> '@encrypt{0} ('@dbK-key{0} '@kS{0}) $@&('@shK-msg{0} ('FRESH{0} ('@shK{0} '@C{0} ('@server-ts{0} '@S{0})) (
    'suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0})))))), '@princ-msg{0} ('@tcs-princ{0} ('@client-tcs{0} '@C{0})))
@@AKey:Trm --> 'FRESH{0} ('@shK{0} '@C{0} ('@TGS-ts{0} '@TS{0})) ('suc{0} ('suc{0} '0{0}))
@@SKey:Trm --> 'FRESH{0} ('@shK{0} '@C{0} ('@server-ts{0} '@S{0})) ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0})))))
@@n2:Trm --> 'FRESH{0} '@nonce{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0}))))
@@S:Trm --> '@S{0}
@fresh:Trm --> 'suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0})))))
@@L:Trm --> 'FRESH{0} ({'_ : '@client{0}} {'_ : '@server{0}} {'_ : '@TGS{0}} {'_ : '@nonce{0}} '@state{0}) ('suc{0} ('suc{
    0} ('suc{0} '0{0})))
@@T:Trm --> '@TS{0}
@fresh':Trm --> 'suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0})))))
*********** success #8
*********** rule
crl $union('@N{0} $@&('@princ-msg{0} ('@tcs-princ{0} ('@client-tcs{0} @@C:Trm)), @@Y:Trm, '@encrypt{0} ('@shK-key{0}
    @@AKey:Trm) $@&('@shK-msg{0} @@SKey:Trm, '@nonce-msg{0} @@n2:Trm, '@princ-msg{0} ('@tcs-princ{0} ('@ts-tcs{0} (
    '@server-ts{0} @@S:Trm))))), 'F{0} @fresh:Trm, 'T_clientTGE_resp{0} @@C:Trm @@L:Trm, @@L:Trm @@C:Trm @@S:Trm @@T:Trm
    @@n2:Trm) => $union('F{0} @fresh':Trm, '@Service{0} @@C:Trm @@Y:Trm @@S:Trm @@SKey:Trm) if @fresh':Trm := @fresh:Trm .
@@C:Trm --> '@C{0}
@@Y:Trm --> '@encrypt{0} ('@dbK-key{0} '@kS{0}) $@&('@shK-msg{0} ('FRESH{0} ('@shK{0} '@C{0} ('@server-ts{0} '@S{0})) (
    'suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0})))))), '@princ-msg{0} ('@tcs-princ{0} ('@client-tcs{0} '@C{0})))
@@AKey:Trm --> 'FRESH{0} ('@shK{0} '@C{0} ('@TGS-ts{0} '@TS{0})) ('suc{0} ('suc{0} '0{0}))
@@SKey:Trm --> 'FRESH{0} ('@shK{0} '@C{0} ('@server-ts{0} '@S{0})) ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0})))))
@@n2:Trm --> 'FRESH{0} '@nonce{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0}))))
@@S:Trm --> '@S{0}
@fresh:Trm --> 'suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0})))))
@@L:Trm --> 'FRESH{0} ({'_ : '@client{0}} {'_ : '@server{0}} {'_ : '@TGS{0}} {'_ : '@nonce{0}} '@state{0}) ('suc{0} ('suc{
    0} ('suc{0} '0{0})))
@@T:Trm --> '@TS{0}
@fresh':Trm --> 'suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0})))))
Old: $union('@N{0} $@&('@princ-msg{0} ('@tcs-princ{0} ('@client-tcs{0} '@C{0})), '@encrypt{0} ('@dbK-key{0} '@kS{0}) $@&(
    '@shK-msg{0} ('FRESH{0} ('@shK{0} '@C{0} ('@server-ts{0} '@S{0})) ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{
    0})))))), '@princ-msg{0} ('@tcs-princ{0} ('@client-tcs{0} '@C{0}))), '@encrypt{0} ('@shK-key{0} ('FRESH{0} ('@shK{0}
    '@C{0} ('@TGS-ts{0} '@TS{0})) ('suc{0} ('suc{0} '0{0})))) $@&('@shK-msg{0} ('FRESH{0} ('@shK{0} '@C{0} ('@server-ts{0}
    '@S{0})) ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0})))))), '@nonce-msg{0} ('FRESH{0} '@nonce{0} ('suc{0} ('suc{
    0} ('suc{0} ('suc{0} '0{0}))))), '@princ-msg{0} ('@tcs-princ{0} ('@ts-tcs{0} ('@server-ts{0} '@S{0}))))), '@START-CSE{
    0} '@C{0}, 'F{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0})))))), 'EL{0} '@KAS{0} '@AS{0}, 'EL{0}
    '@server{0} '@S{0}, 'EL{0} ('@dbK{0} ('@client-tcs{0} '@C{0})) '@kC{0}, 'EL{0} ('@dbK{0} ('@ts-tcs{0} ('@TGS-ts{0}
    '@TS{0}))) '@kTS{0}, 'EL{0} ('@dbK{0} ('@ts-tcs{0} ('@server-ts{0} '@S{0}))) '@kS{0}, 'T_clientTGE_resp{0} '@C{0} (
    'FRESH{0} ({'_ : '@client{0}} {'_ : '@server{0}} {'_ : '@TGS{0}} {'_ : '@nonce{0}} '@state{0}) ('suc{0} ('suc{0} ('suc{
    0} '0{0})))), '@Auth{0} '@C{0} ('@encrypt{0} ('@dbK-key{0} '@kTS{0}) $@&('@shK-msg{0} ('FRESH{0} ('@shK{0} '@C{0} (
    '@TGS-ts{0} '@TS{0})) ('suc{0} ('suc{0} '0{0}))), '@princ-msg{0} ('@tcs-princ{0} ('@client-tcs{0} '@C{0})))) '@TS{0} (
    'FRESH{0} ('@shK{0} '@C{0} ('@TGS-ts{0} '@TS{0})) ('suc{0} ('suc{0} '0{0}))), 'FRESH{0} ({'_ : '@client{0}} {'_ :
    '@server{0}} {'_ : '@TGS{0}} {'_ : '@nonce{0}} '@state{0}) ('suc{0} ('suc{0} ('suc{0} '0{0}))) '@C{0} '@S{0} '@TS{0} (
    'FRESH{0} '@nonce{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0}))))))
$union('@N{0} $@&('@princ-msg{0} ('@tcs-princ{0} ('@client-tcs{0} '@C{0})), '@encrypt{0} ('@dbK-key{0} '@kS{0}) $@&(
    '@shK-msg{0} ('FRESH{0} ('@shK{0} '@C{0} ('@server-ts{0} '@S{0})) ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{
    0})))))), '@princ-msg{0} ('@tcs-princ{0} ('@client-tcs{0} '@C{0}))), '@encrypt{0} ('@shK-key{0} ('FRESH{0} ('@shK{0}
    '@C{0} ('@TGS-ts{0} '@TS{0})) ('suc{0} ('suc{0} '0{0})))) $@&('@shK-msg{0} ('FRESH{0} ('@shK{0} '@C{0} ('@server-ts{0}
    '@S{0})) ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0})))))), '@nonce-msg{0} ('FRESH{0} '@nonce{0} ('suc{0} ('suc{
    0} ('suc{0} ('suc{0} '0{0}))))), '@princ-msg{0} ('@tcs-princ{0} ('@ts-tcs{0} ('@server-ts{0} '@S{0}))))), '@START-CSE{
    0} '@C{0}, 'F{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0})))))), 'EL{0} '@KAS{0} '@AS{0}, 'EL{0}
    '@server{0} '@S{0}, 'EL{0} ('@dbK{0} ('@client-tcs{0} '@C{0})) '@kC{0}, 'EL{0} ('@dbK{0} ('@ts-tcs{0} ('@TGS-ts{0}
    '@TS{0}))) '@kTS{0}, 'EL{0} ('@dbK{0} ('@ts-tcs{0} ('@server-ts{0} '@S{0}))) '@kS{0}, 'T_clientTGE_resp{0} '@C{0} (
    'FRESH{0} ({'_ : '@client{0}} {'_ : '@server{0}} {'_ : '@TGS{0}} {'_ : '@nonce{0}} '@state{0}) ('suc{0} ('suc{0} ('suc{
    0} '0{0})))), '@Auth{0} '@C{0} ('@encrypt{0} ('@dbK-key{0} '@kTS{0}) $@&('@shK-msg{0} ('FRESH{0} ('@shK{0} '@C{0} (
    '@TGS-ts{0} '@TS{0})) ('suc{0} ('suc{0} '0{0}))), '@princ-msg{0} ('@tcs-princ{0} ('@client-tcs{0} '@C{0})))) '@TS{0} (
    'FRESH{0} ('@shK{0} '@C{0} ('@TGS-ts{0} '@TS{0})) ('suc{0} ('suc{0} '0{0}))), 'FRESH{0} ({'_ : '@client{0}} {'_ :
    '@server{0}} {'_ : '@TGS{0}} {'_ : '@nonce{0}} '@state{0}) ('suc{0} ('suc{0} ('suc{0} '0{0}))) '@C{0} '@S{0} '@TS{0} (
    'FRESH{0} '@nonce{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0}))))))
--->
$union($union('@START-CSE{0} '@C{0}, 'EL{0} '@KAS{0} '@AS{0}, 'EL{0} '@server{0} '@S{0}, 'EL{0} ('@dbK{0} ('@client-tcs{0}
    '@C{0})) '@kC{0}, 'EL{0} ('@dbK{0} ('@ts-tcs{0} ('@TGS-ts{0} '@TS{0}))) '@kTS{0}, 'EL{0} ('@dbK{0} ('@ts-tcs{0} (
    '@server-ts{0} '@S{0}))) '@kS{0}, '@Auth{0} '@C{0} ('@encrypt{0} ('@dbK-key{0} '@kTS{0}) $@&('@shK-msg{0} ('FRESH{0} (
    '@shK{0} '@C{0} ('@TGS-ts{0} '@TS{0})) ('suc{0} ('suc{0} '0{0}))), '@princ-msg{0} ('@tcs-princ{0} ('@client-tcs{0} '@C{
    0})))) '@TS{0} ('FRESH{0} ('@shK{0} '@C{0} ('@TGS-ts{0} '@TS{0})) ('suc{0} ('suc{0} '0{0})))), $union('F{0} ('suc{0} (
    'suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0})))))), '@Service{0} '@C{0} ('@encrypt{0} ('@dbK-key{0} '@kS{0}) $@&(
    '@shK-msg{0} ('FRESH{0} ('@shK{0} '@C{0} ('@server-ts{0} '@S{0})) ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{
    0})))))), '@princ-msg{0} ('@tcs-princ{0} ('@client-tcs{0} '@C{0})))) '@S{0} ('FRESH{0} ('@shK{0} '@C{0} ('@server-ts{0}
    '@S{0})) ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0}))))))))
New: $union($union('@START-CSE{0} '@C{0}, 'EL{0} '@KAS{0} '@AS{0}, 'EL{0} '@server{0} '@S{0}, 'EL{0} ('@dbK{0} (
    '@client-tcs{0} '@C{0})) '@kC{0}, 'EL{0} ('@dbK{0} ('@ts-tcs{0} ('@TGS-ts{0} '@TS{0}))) '@kTS{0}, 'EL{0} ('@dbK{0} (
    '@ts-tcs{0} ('@server-ts{0} '@S{0}))) '@kS{0}, '@Auth{0} '@C{0} ('@encrypt{0} ('@dbK-key{0} '@kTS{0}) $@&('@shK-msg{0}
    ('FRESH{0} ('@shK{0} '@C{0} ('@TGS-ts{0} '@TS{0})) ('suc{0} ('suc{0} '0{0}))), '@princ-msg{0} ('@tcs-princ{0} (
    '@client-tcs{0} '@C{0})))) '@TS{0} ('FRESH{0} ('@shK{0} '@C{0} ('@TGS-ts{0} '@TS{0})) ('suc{0} ('suc{0} '0{0})))),
    $union('F{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0})))))), '@Service{0} '@C{0} ('@encrypt{0} (
    '@dbK-key{0} '@kS{0}) $@&('@shK-msg{0} ('FRESH{0} ('@shK{0} '@C{0} ('@server-ts{0} '@S{0})) ('suc{0} ('suc{0} ('suc{0}
    ('suc{0} ('suc{0} '0{0})))))), '@princ-msg{0} ('@tcs-princ{0} ('@client-tcs{0} '@C{0})))) '@S{0} ('FRESH{0} ('@shK{0}
    '@C{0} ('@server-ts{0} '@S{0})) ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0}))))))))
*********** trial #9
crl $union('@START-CSE{0} @@C:Trm, 'F{0} @fresh:Trm, '@Service{0} @@C:Trm @@Y:Trm @@S:Trm @@SKey:Trm) => $union(@@L:Trm
    @@C:Trm @@S:Trm @@SKey:Trm @@t:Trm @@Y:Trm, $union('@Service{0} @@C:Trm @@Y:Trm @@S:Trm @@SKey:Trm, $union(
    'T_clientCSE_resp{0} @@C:Trm @@L:Trm, $union('@N{0} $@&(@@Y:Trm, '@encrypt{0} ('@shK-key{0} @@SKey:Trm) $@&(
    '@princ-msg{0} ('@tcs-princ{0} ('@client-tcs{0} @@C:Trm)), '@time-msg{0} @@t:Trm)), 'F{0} @fresh':Trm)))) if @@L:Trm :=
    'FRESH{0} ({'@C : '@client{0}} {'@S : '@server{0}} {'_ : '@shK{0} @@C:Trm ('@server-ts{0} @@S:Trm)} {'_ : '@time{0}} {
    '_ : '@msg{0}} '@state{0}) @fresh:Trm /\ @@t:Trm := 'FRESH{0} '@time{0} ('suc{0} @fresh:Trm) /\ @fresh':Trm := 'suc{0}
    ('suc{0} @fresh:Trm) .
@@C:Trm --> '@C{0}
@fresh:Trm --> 'suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0})))))
@@Y:Trm --> '@encrypt{0} ('@dbK-key{0} '@kS{0}) $@&('@shK-msg{0} ('FRESH{0} ('@shK{0} '@C{0} ('@server-ts{0} '@S{0})) (
    'suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0})))))), '@princ-msg{0} ('@tcs-princ{0} ('@client-tcs{0} '@C{0})))
@@S:Trm --> '@S{0}
@@SKey:Trm --> 'FRESH{0} ('@shK{0} '@C{0} ('@server-ts{0} '@S{0})) ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0})))))
@@L:Trm --> (unbound)
@@t:Trm --> (unbound)
@fresh':Trm --> (unbound)
*********** solving condition fragment
@@L:Trm := 'FRESH{0} ({'@C : '@client{0}} {'@S : '@server{0}} {'_ : '@shK{0} @@C:Trm ('@server-ts{0} @@S:Trm)} {'_ :
    '@time{0}} {'_ : '@msg{0}} '@state{0}) @fresh:Trm
*********** success for condition fragment
@@L:Trm := 'FRESH{0} ({'@C : '@client{0}} {'@S : '@server{0}} {'_ : '@shK{0} @@C:Trm ('@server-ts{0} @@S:Trm)} {'_ :
    '@time{0}} {'_ : '@msg{0}} '@state{0}) @fresh:Trm
@@C:Trm --> '@C{0}
@fresh:Trm --> 'suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0})))))
@@Y:Trm --> '@encrypt{0} ('@dbK-key{0} '@kS{0}) $@&('@shK-msg{0} ('FRESH{0} ('@shK{0} '@C{0} ('@server-ts{0} '@S{0})) (
    'suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0})))))), '@princ-msg{0} ('@tcs-princ{0} ('@client-tcs{0} '@C{0})))
@@S:Trm --> '@S{0}
@@SKey:Trm --> 'FRESH{0} ('@shK{0} '@C{0} ('@server-ts{0} '@S{0})) ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0})))))
@@L:Trm --> 'FRESH{0} ({'@C : '@client{0}} {'@S : '@server{0}} {'_ : '@shK{0} '@C{0} ('@server-ts{0} '@S{0})} {'_ : '@time{
    0}} {'_ : '@msg{0}} '@state{0}) ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0}))))))
@@t:Trm --> (unbound)
@fresh':Trm --> (unbound)
*********** solving condition fragment
@@t:Trm := 'FRESH{0} '@time{0} ('suc{0} @fresh:Trm)
*********** success for condition fragment
@@t:Trm := 'FRESH{0} '@time{0} ('suc{0} @fresh:Trm)
@@C:Trm --> '@C{0}
@fresh:Trm --> 'suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0})))))
@@Y:Trm --> '@encrypt{0} ('@dbK-key{0} '@kS{0}) $@&('@shK-msg{0} ('FRESH{0} ('@shK{0} '@C{0} ('@server-ts{0} '@S{0})) (
    'suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0})))))), '@princ-msg{0} ('@tcs-princ{0} ('@client-tcs{0} '@C{0})))
@@S:Trm --> '@S{0}
@@SKey:Trm --> 'FRESH{0} ('@shK{0} '@C{0} ('@server-ts{0} '@S{0})) ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0})))))
@@L:Trm --> 'FRESH{0} ({'@C : '@client{0}} {'@S : '@server{0}} {'_ : '@shK{0} '@C{0} ('@server-ts{0} '@S{0})} {'_ : '@time{
    0}} {'_ : '@msg{0}} '@state{0}) ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0}))))))
@@t:Trm --> 'FRESH{0} '@time{0} ('suc{0} ('suc{0} ('suc{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)
@@C:Trm --> '@C{0}
@fresh:Trm --> 'suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0})))))
@@Y:Trm --> '@encrypt{0} ('@dbK-key{0} '@kS{0}) $@&('@shK-msg{0} ('FRESH{0} ('@shK{0} '@C{0} ('@server-ts{0} '@S{0})) (
    'suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0})))))), '@princ-msg{0} ('@tcs-princ{0} ('@client-tcs{0} '@C{0})))
@@S:Trm --> '@S{0}
@@SKey:Trm --> 'FRESH{0} ('@shK{0} '@C{0} ('@server-ts{0} '@S{0})) ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0})))))
@@L:Trm --> 'FRESH{0} ({'@C : '@client{0}} {'@S : '@server{0}} {'_ : '@shK{0} '@C{0} ('@server-ts{0} '@S{0})} {'_ : '@time{
    0}} {'_ : '@msg{0}} '@state{0}) ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0}))))))
@@t:Trm --> 'FRESH{0} '@time{0} ('suc{0} ('suc{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} ('suc{0} ('suc{0} '0{0})))))))
*********** success #9
*********** rule
crl $union('@START-CSE{0} @@C:Trm, 'F{0} @fresh:Trm, '@Service{0} @@C:Trm @@Y:Trm @@S:Trm @@SKey:Trm) => $union(@@L:Trm
    @@C:Trm @@S:Trm @@SKey:Trm @@t:Trm @@Y:Trm, $union('@Service{0} @@C:Trm @@Y:Trm @@S:Trm @@SKey:Trm, $union(
    'T_clientCSE_resp{0} @@C:Trm @@L:Trm, $union('@N{0} $@&(@@Y:Trm, '@encrypt{0} ('@shK-key{0} @@SKey:Trm) $@&(
    '@princ-msg{0} ('@tcs-princ{0} ('@client-tcs{0} @@C:Trm)), '@time-msg{0} @@t:Trm)), 'F{0} @fresh':Trm)))) if @@L:Trm :=
    'FRESH{0} ({'@C : '@client{0}} {'@S : '@server{0}} {'_ : '@shK{0} @@C:Trm ('@server-ts{0} @@S:Trm)} {'_ : '@time{0}} {
    '_ : '@msg{0}} '@state{0}) @fresh:Trm /\ @@t:Trm := 'FRESH{0} '@time{0} ('suc{0} @fresh:Trm) /\ @fresh':Trm := 'suc{0}
    ('suc{0} @fresh:Trm) .
@@C:Trm --> '@C{0}
@fresh:Trm --> 'suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0})))))
@@Y:Trm --> '@encrypt{0} ('@dbK-key{0} '@kS{0}) $@&('@shK-msg{0} ('FRESH{0} ('@shK{0} '@C{0} ('@server-ts{0} '@S{0})) (
    'suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0})))))), '@princ-msg{0} ('@tcs-princ{0} ('@client-tcs{0} '@C{0})))
@@S:Trm --> '@S{0}
@@SKey:Trm --> 'FRESH{0} ('@shK{0} '@C{0} ('@server-ts{0} '@S{0})) ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0})))))
@@L:Trm --> 'FRESH{0} ({'@C : '@client{0}} {'@S : '@server{0}} {'_ : '@shK{0} '@C{0} ('@server-ts{0} '@S{0})} {'_ : '@time{
    0}} {'_ : '@msg{0}} '@state{0}) ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0}))))))
@@t:Trm --> 'FRESH{0} '@time{0} ('suc{0} ('suc{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} ('suc{0} ('suc{0} '0{0})))))))
Old: $union('@START-CSE{0} '@C{0}, 'F{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0})))))), 'EL{0} '@KAS{0}
    '@AS{0}, 'EL{0} '@server{0} '@S{0}, 'EL{0} ('@dbK{0} ('@client-tcs{0} '@C{0})) '@kC{0}, 'EL{0} ('@dbK{0} ('@ts-tcs{0} (
    '@TGS-ts{0} '@TS{0}))) '@kTS{0}, 'EL{0} ('@dbK{0} ('@ts-tcs{0} ('@server-ts{0} '@S{0}))) '@kS{0}, '@Auth{0} '@C{0} (
    '@encrypt{0} ('@dbK-key{0} '@kTS{0}) $@&('@shK-msg{0} ('FRESH{0} ('@shK{0} '@C{0} ('@TGS-ts{0} '@TS{0})) ('suc{0} (
    'suc{0} '0{0}))), '@princ-msg{0} ('@tcs-princ{0} ('@client-tcs{0} '@C{0})))) '@TS{0} ('FRESH{0} ('@shK{0} '@C{0} (
    '@TGS-ts{0} '@TS{0})) ('suc{0} ('suc{0} '0{0}))), '@Service{0} '@C{0} ('@encrypt{0} ('@dbK-key{0} '@kS{0}) $@&(
    '@shK-msg{0} ('FRESH{0} ('@shK{0} '@C{0} ('@server-ts{0} '@S{0})) ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{
    0})))))), '@princ-msg{0} ('@tcs-princ{0} ('@client-tcs{0} '@C{0})))) '@S{0} ('FRESH{0} ('@shK{0} '@C{0} ('@server-ts{0}
    '@S{0})) ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0})))))))
$union('@START-CSE{0} '@C{0}, 'F{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0})))))), 'EL{0} '@KAS{0}
    '@AS{0}, 'EL{0} '@server{0} '@S{0}, 'EL{0} ('@dbK{0} ('@client-tcs{0} '@C{0})) '@kC{0}, 'EL{0} ('@dbK{0} ('@ts-tcs{0} (
    '@TGS-ts{0} '@TS{0}))) '@kTS{0}, 'EL{0} ('@dbK{0} ('@ts-tcs{0} ('@server-ts{0} '@S{0}))) '@kS{0}, '@Auth{0} '@C{0} (
    '@encrypt{0} ('@dbK-key{0} '@kTS{0}) $@&('@shK-msg{0} ('FRESH{0} ('@shK{0} '@C{0} ('@TGS-ts{0} '@TS{0})) ('suc{0} (
    'suc{0} '0{0}))), '@princ-msg{0} ('@tcs-princ{0} ('@client-tcs{0} '@C{0})))) '@TS{0} ('FRESH{0} ('@shK{0} '@C{0} (
    '@TGS-ts{0} '@TS{0})) ('suc{0} ('suc{0} '0{0}))), '@Service{0} '@C{0} ('@encrypt{0} ('@dbK-key{0} '@kS{0}) $@&(
    '@shK-msg{0} ('FRESH{0} ('@shK{0} '@C{0} ('@server-ts{0} '@S{0})) ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{
    0})))))), '@princ-msg{0} ('@tcs-princ{0} ('@client-tcs{0} '@C{0})))) '@S{0} ('FRESH{0} ('@shK{0} '@C{0} ('@server-ts{0}
    '@S{0})) ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0})))))))
--->
$union($union('EL{0} '@KAS{0} '@AS{0}, 'EL{0} '@server{0} '@S{0}, 'EL{0} ('@dbK{0} ('@client-tcs{0} '@C{0})) '@kC{0}, 'EL{
    0} ('@dbK{0} ('@ts-tcs{0} ('@TGS-ts{0} '@TS{0}))) '@kTS{0}, 'EL{0} ('@dbK{0} ('@ts-tcs{0} ('@server-ts{0} '@S{0})))
    '@kS{0}, '@Auth{0} '@C{0} ('@encrypt{0} ('@dbK-key{0} '@kTS{0}) $@&('@shK-msg{0} ('FRESH{0} ('@shK{0} '@C{0} ('@TGS-ts{
    0} '@TS{0})) ('suc{0} ('suc{0} '0{0}))), '@princ-msg{0} ('@tcs-princ{0} ('@client-tcs{0} '@C{0})))) '@TS{0} ('FRESH{0}
    ('@shK{0} '@C{0} ('@TGS-ts{0} '@TS{0})) ('suc{0} ('suc{0} '0{0})))), $union('FRESH{0} ({'@C : '@client{0}} {'@S :
    '@server{0}} {'_ : '@shK{0} '@C{0} ('@server-ts{0} '@S{0})} {'_ : '@time{0}} {'_ : '@msg{0}} '@state{0}) ('suc{0} (
    'suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0})))))) '@C{0} '@S{0} ('FRESH{0} ('@shK{0} '@C{0} ('@server-ts{0} '@S{
    0})) ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0})))))) ('FRESH{0} '@time{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0}
    ('suc{0} ('suc{0} ('suc{0} '0{0})))))))) ('@encrypt{0} ('@dbK-key{0} '@kS{0}) $@&('@shK-msg{0} ('FRESH{0} ('@shK{0}
    '@C{0} ('@server-ts{0} '@S{0})) ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0})))))), '@princ-msg{0} ('@tcs-princ{
    0} ('@client-tcs{0} '@C{0})))), $union('@Service{0} '@C{0} ('@encrypt{0} ('@dbK-key{0} '@kS{0}) $@&('@shK-msg{0} (
    'FRESH{0} ('@shK{0} '@C{0} ('@server-ts{0} '@S{0})) ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0})))))),
    '@princ-msg{0} ('@tcs-princ{0} ('@client-tcs{0} '@C{0})))) '@S{0} ('FRESH{0} ('@shK{0} '@C{0} ('@server-ts{0} '@S{0}))
    ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0})))))), $union('T_clientCSE_resp{0} '@C{0} ('FRESH{0} ({'@C :
    '@client{0}} {'@S : '@server{0}} {'_ : '@shK{0} '@C{0} ('@server-ts{0} '@S{0})} {'_ : '@time{0}} {'_ : '@msg{0}}
    '@state{0}) ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0}))))))), $union('@N{0} $@&('@encrypt{0} (
    '@dbK-key{0} '@kS{0}) $@&('@shK-msg{0} ('FRESH{0} ('@shK{0} '@C{0} ('@server-ts{0} '@S{0})) ('suc{0} ('suc{0} ('suc{0}
    ('suc{0} ('suc{0} '0{0})))))), '@princ-msg{0} ('@tcs-princ{0} ('@client-tcs{0} '@C{0}))), '@encrypt{0} ('@shK-key{0} (
    'FRESH{0} ('@shK{0} '@C{0} ('@server-ts{0} '@S{0})) ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0}))))))) $@&(
    '@princ-msg{0} ('@tcs-princ{0} ('@client-tcs{0} '@C{0})), '@time-msg{0} ('FRESH{0} '@time{0} ('suc{0} ('suc{0} ('suc{0}
    ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0})))))))))), 'F{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{
    0} ('suc{0} '0{0})))))))))))))
New: $union($union('EL{0} '@KAS{0} '@AS{0}, 'EL{0} '@server{0} '@S{0}, 'EL{0} ('@dbK{0} ('@client-tcs{0} '@C{0})) '@kC{0},
    'EL{0} ('@dbK{0} ('@ts-tcs{0} ('@TGS-ts{0} '@TS{0}))) '@kTS{0}, 'EL{0} ('@dbK{0} ('@ts-tcs{0} ('@server-ts{0} '@S{0})))
    '@kS{0}, '@Auth{0} '@C{0} ('@encrypt{0} ('@dbK-key{0} '@kTS{0}) $@&('@shK-msg{0} ('FRESH{0} ('@shK{0} '@C{0} ('@TGS-ts{
    0} '@TS{0})) ('suc{0} ('suc{0} '0{0}))), '@princ-msg{0} ('@tcs-princ{0} ('@client-tcs{0} '@C{0})))) '@TS{0} ('FRESH{0}
    ('@shK{0} '@C{0} ('@TGS-ts{0} '@TS{0})) ('suc{0} ('suc{0} '0{0})))), $union('FRESH{0} ({'@C : '@client{0}} {'@S :
    '@server{0}} {'_ : '@shK{0} '@C{0} ('@server-ts{0} '@S{0})} {'_ : '@time{0}} {'_ : '@msg{0}} '@state{0}) ('suc{0} (
    'suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0})))))) '@C{0} '@S{0} ('FRESH{0} ('@shK{0} '@C{0} ('@server-ts{0} '@S{
    0})) ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0})))))) ('FRESH{0} '@time{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0}
    ('suc{0} ('suc{0} ('suc{0} '0{0})))))))) ('@encrypt{0} ('@dbK-key{0} '@kS{0}) $@&('@shK-msg{0} ('FRESH{0} ('@shK{0}
    '@C{0} ('@server-ts{0} '@S{0})) ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0})))))), '@princ-msg{0} ('@tcs-princ{
    0} ('@client-tcs{0} '@C{0})))), $union('@Service{0} '@C{0} ('@encrypt{0} ('@dbK-key{0} '@kS{0}) $@&('@shK-msg{0} (
    'FRESH{0} ('@shK{0} '@C{0} ('@server-ts{0} '@S{0})) ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0})))))),
    '@princ-msg{0} ('@tcs-princ{0} ('@client-tcs{0} '@C{0})))) '@S{0} ('FRESH{0} ('@shK{0} '@C{0} ('@server-ts{0} '@S{0}))
    ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0})))))), $union('T_clientCSE_resp{0} '@C{0} ('FRESH{0} ({'@C :
    '@client{0}} {'@S : '@server{0}} {'_ : '@shK{0} '@C{0} ('@server-ts{0} '@S{0})} {'_ : '@time{0}} {'_ : '@msg{0}}
    '@state{0}) ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0}))))))), $union('@N{0} $@&('@encrypt{0} (
    '@dbK-key{0} '@kS{0}) $@&('@shK-msg{0} ('FRESH{0} ('@shK{0} '@C{0} ('@server-ts{0} '@S{0})) ('suc{0} ('suc{0} ('suc{0}
    ('suc{0} ('suc{0} '0{0})))))), '@princ-msg{0} ('@tcs-princ{0} ('@client-tcs{0} '@C{0}))), '@encrypt{0} ('@shK-key{0} (
    'FRESH{0} ('@shK{0} '@C{0} ('@server-ts{0} '@S{0})) ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0}))))))) $@&(
    '@princ-msg{0} ('@tcs-princ{0} ('@client-tcs{0} '@C{0})), '@time-msg{0} ('FRESH{0} '@time{0} ('suc{0} ('suc{0} ('suc{0}
    ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0})))))))))), 'F{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{
    0} ('suc{0} '0{0})))))))))))))
*********** trial #10
crl $union('@N{0} $@&('@encrypt{0} ('@dbK-key{0} @@kS:Trm) @@X:Trm, '@encrypt{0} ('@shK-key{0} @@SKey:Trm) $@&('@princ-msg{
    0} ('@tcs-princ{0} ('@client-tcs{0} @@C:Trm)), '@time-msg{0} @@t:Trm)), 'F{0} @fresh:Trm, 'EL{0} '@server{0} @@S:Trm)
    => $union('@Mem{0} @@S:Trm @@C:Trm @@SKey:Trm @@t:Trm, $union('EL{0} '@server{0} @@S:Trm, $union('@N{0} ('@encrypt{0} (
    '@shK-key{0} @@SKey:Trm) ('@time-msg{0} @@t:Trm)), 'F{0} @fresh':Trm))) if @fresh':Trm := @fresh:Trm .
@@kS:Trm --> '@kS{0}
@@X:Trm --> $@&('@shK-msg{0} ('FRESH{0} ('@shK{0} '@C{0} ('@server-ts{0} '@S{0})) ('suc{0} ('suc{0} ('suc{0} ('suc{0} (
    'suc{0} '0{0})))))), '@princ-msg{0} ('@tcs-princ{0} ('@client-tcs{0} '@C{0})))
@@SKey:Trm --> 'FRESH{0} ('@shK{0} '@C{0} ('@server-ts{0} '@S{0})) ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0})))))
@@C:Trm --> '@C{0}
@@t:Trm --> 'FRESH{0} '@time{0} ('suc{0} ('suc{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} ('suc{0} ('suc{0} '0{0})))))))
@@S:Trm --> '@S{0}
@fresh':Trm --> (unbound)
*********** solving condition fragment
@fresh':Trm := @fresh:Trm
*********** success for condition fragment
@fresh':Trm := @fresh:Trm
@@kS:Trm --> '@kS{0}
@@X:Trm --> $@&('@shK-msg{0} ('FRESH{0} ('@shK{0} '@C{0} ('@server-ts{0} '@S{0})) ('suc{0} ('suc{0} ('suc{0} ('suc{0} (
    'suc{0} '0{0})))))), '@princ-msg{0} ('@tcs-princ{0} ('@client-tcs{0} '@C{0})))
@@SKey:Trm --> 'FRESH{0} ('@shK{0} '@C{0} ('@server-ts{0} '@S{0})) ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0})))))
@@C:Trm --> '@C{0}
@@t:Trm --> 'FRESH{0} '@time{0} ('suc{0} ('suc{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} ('suc{0} ('suc{0} '0{0})))))))
@@S:Trm --> '@S{0}
@fresh':Trm --> 'suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0})))))))
*********** success #10
*********** rule
crl $union('@N{0} $@&('@encrypt{0} ('@dbK-key{0} @@kS:Trm) @@X:Trm, '@encrypt{0} ('@shK-key{0} @@SKey:Trm) $@&('@princ-msg{
    0} ('@tcs-princ{0} ('@client-tcs{0} @@C:Trm)), '@time-msg{0} @@t:Trm)), 'F{0} @fresh:Trm, 'EL{0} '@server{0} @@S:Trm)
    => $union('@Mem{0} @@S:Trm @@C:Trm @@SKey:Trm @@t:Trm, $union('EL{0} '@server{0} @@S:Trm, $union('@N{0} ('@encrypt{0} (
    '@shK-key{0} @@SKey:Trm) ('@time-msg{0} @@t:Trm)), 'F{0} @fresh':Trm))) if @fresh':Trm := @fresh:Trm .
@@kS:Trm --> '@kS{0}
@@X:Trm --> $@&('@shK-msg{0} ('FRESH{0} ('@shK{0} '@C{0} ('@server-ts{0} '@S{0})) ('suc{0} ('suc{0} ('suc{0} ('suc{0} (
    'suc{0} '0{0})))))), '@princ-msg{0} ('@tcs-princ{0} ('@client-tcs{0} '@C{0})))
@@SKey:Trm --> 'FRESH{0} ('@shK{0} '@C{0} ('@server-ts{0} '@S{0})) ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0})))))
@@C:Trm --> '@C{0}
@@t:Trm --> 'FRESH{0} '@time{0} ('suc{0} ('suc{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} ('suc{0} ('suc{0} '0{0})))))))
@@S:Trm --> '@S{0}
@fresh':Trm --> 'suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0})))))))
Old: $union('@N{0} $@&('@encrypt{0} ('@dbK-key{0} '@kS{0}) $@&('@shK-msg{0} ('FRESH{0} ('@shK{0} '@C{0} ('@server-ts{0}
    '@S{0})) ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0})))))), '@princ-msg{0} ('@tcs-princ{0} ('@client-tcs{0} '@C{
    0}))), '@encrypt{0} ('@shK-key{0} ('FRESH{0} ('@shK{0} '@C{0} ('@server-ts{0} '@S{0})) ('suc{0} ('suc{0} ('suc{0} (
    'suc{0} ('suc{0} '0{0}))))))) $@&('@princ-msg{0} ('@tcs-princ{0} ('@client-tcs{0} '@C{0})), '@time-msg{0} ('FRESH{0}
    '@time{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0})))))))))), 'F{0} ('suc{0} ('suc{0} (
    'suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0})))))))), 'EL{0} '@KAS{0} '@AS{0}, 'EL{0} '@server{0} '@S{0},
    'EL{0} ('@dbK{0} ('@client-tcs{0} '@C{0})) '@kC{0}, 'EL{0} ('@dbK{0} ('@ts-tcs{0} ('@TGS-ts{0} '@TS{0}))) '@kTS{0},
    'EL{0} ('@dbK{0} ('@ts-tcs{0} ('@server-ts{0} '@S{0}))) '@kS{0}, 'T_clientCSE_resp{0} '@C{0} ('FRESH{0} ({'@C :
    '@client{0}} {'@S : '@server{0}} {'_ : '@shK{0} '@C{0} ('@server-ts{0} '@S{0})} {'_ : '@time{0}} {'_ : '@msg{0}}
    '@state{0}) ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0}))))))), '@Auth{0} '@C{0} ('@encrypt{0} (
    '@dbK-key{0} '@kTS{0}) $@&('@shK-msg{0} ('FRESH{0} ('@shK{0} '@C{0} ('@TGS-ts{0} '@TS{0})) ('suc{0} ('suc{0} '0{0}))),
    '@princ-msg{0} ('@tcs-princ{0} ('@client-tcs{0} '@C{0})))) '@TS{0} ('FRESH{0} ('@shK{0} '@C{0} ('@TGS-ts{0} '@TS{0})) (
    'suc{0} ('suc{0} '0{0}))), '@Service{0} '@C{0} ('@encrypt{0} ('@dbK-key{0} '@kS{0}) $@&('@shK-msg{0} ('FRESH{0} ('@shK{
    0} '@C{0} ('@server-ts{0} '@S{0})) ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0})))))), '@princ-msg{0} (
    '@tcs-princ{0} ('@client-tcs{0} '@C{0})))) '@S{0} ('FRESH{0} ('@shK{0} '@C{0} ('@server-ts{0} '@S{0})) ('suc{0} ('suc{
    0} ('suc{0} ('suc{0} ('suc{0} '0{0})))))), 'FRESH{0} ({'@C : '@client{0}} {'@S : '@server{0}} {'_ : '@shK{0} '@C{0} (
    '@server-ts{0} '@S{0})} {'_ : '@time{0}} {'_ : '@msg{0}} '@state{0}) ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} (
    'suc{0} '0{0})))))) '@C{0} '@S{0} ('FRESH{0} ('@shK{0} '@C{0} ('@server-ts{0} '@S{0})) ('suc{0} ('suc{0} ('suc{0} (
    'suc{0} ('suc{0} '0{0})))))) ('FRESH{0} '@time{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{
    0})))))))) ('@encrypt{0} ('@dbK-key{0} '@kS{0}) $@&('@shK-msg{0} ('FRESH{0} ('@shK{0} '@C{0} ('@server-ts{0} '@S{0})) (
    'suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0})))))), '@princ-msg{0} ('@tcs-princ{0} ('@client-tcs{0} '@C{0})))))
$union('@N{0} $@&('@encrypt{0} ('@dbK-key{0} '@kS{0}) $@&('@shK-msg{0} ('FRESH{0} ('@shK{0} '@C{0} ('@server-ts{0} '@S{0}))
    ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0})))))), '@princ-msg{0} ('@tcs-princ{0} ('@client-tcs{0} '@C{0}))),
    '@encrypt{0} ('@shK-key{0} ('FRESH{0} ('@shK{0} '@C{0} ('@server-ts{0} '@S{0})) ('suc{0} ('suc{0} ('suc{0} ('suc{0} (
    'suc{0} '0{0}))))))) $@&('@princ-msg{0} ('@tcs-princ{0} ('@client-tcs{0} '@C{0})), '@time-msg{0} ('FRESH{0} '@time{0} (
    'suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0})))))))))), 'F{0} ('suc{0} ('suc{0} ('suc{0} ('suc{
    0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0})))))))), 'EL{0} '@KAS{0} '@AS{0}, 'EL{0} '@server{0} '@S{0}, 'EL{0} (
    '@dbK{0} ('@client-tcs{0} '@C{0})) '@kC{0}, 'EL{0} ('@dbK{0} ('@ts-tcs{0} ('@TGS-ts{0} '@TS{0}))) '@kTS{0}, 'EL{0} (
    '@dbK{0} ('@ts-tcs{0} ('@server-ts{0} '@S{0}))) '@kS{0}, 'T_clientCSE_resp{0} '@C{0} ('FRESH{0} ({'@C : '@client{0}} {
    '@S : '@server{0}} {'_ : '@shK{0} '@C{0} ('@server-ts{0} '@S{0})} {'_ : '@time{0}} {'_ : '@msg{0}} '@state{0}) ('suc{0}
    ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0}))))))), '@Auth{0} '@C{0} ('@encrypt{0} ('@dbK-key{0} '@kTS{0}) $@&(
    '@shK-msg{0} ('FRESH{0} ('@shK{0} '@C{0} ('@TGS-ts{0} '@TS{0})) ('suc{0} ('suc{0} '0{0}))), '@princ-msg{0} (
    '@tcs-princ{0} ('@client-tcs{0} '@C{0})))) '@TS{0} ('FRESH{0} ('@shK{0} '@C{0} ('@TGS-ts{0} '@TS{0})) ('suc{0} ('suc{0}
    '0{0}))), '@Service{0} '@C{0} ('@encrypt{0} ('@dbK-key{0} '@kS{0}) $@&('@shK-msg{0} ('FRESH{0} ('@shK{0} '@C{0} (
    '@server-ts{0} '@S{0})) ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0})))))), '@princ-msg{0} ('@tcs-princ{0} (
    '@client-tcs{0} '@C{0})))) '@S{0} ('FRESH{0} ('@shK{0} '@C{0} ('@server-ts{0} '@S{0})) ('suc{0} ('suc{0} ('suc{0} (
    'suc{0} ('suc{0} '0{0})))))), 'FRESH{0} ({'@C : '@client{0}} {'@S : '@server{0}} {'_ : '@shK{0} '@C{0} ('@server-ts{0}
    '@S{0})} {'_ : '@time{0}} {'_ : '@msg{0}} '@state{0}) ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0}))))))
    '@C{0} '@S{0} ('FRESH{0} ('@shK{0} '@C{0} ('@server-ts{0} '@S{0})) ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{
    0})))))) ('FRESH{0} '@time{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0})))))))) ('@encrypt{
    0} ('@dbK-key{0} '@kS{0}) $@&('@shK-msg{0} ('FRESH{0} ('@shK{0} '@C{0} ('@server-ts{0} '@S{0})) ('suc{0} ('suc{0} (
    'suc{0} ('suc{0} ('suc{0} '0{0})))))), '@princ-msg{0} ('@tcs-princ{0} ('@client-tcs{0} '@C{0})))))
--->
$union($union('EL{0} '@KAS{0} '@AS{0}, 'EL{0} ('@dbK{0} ('@client-tcs{0} '@C{0})) '@kC{0}, 'EL{0} ('@dbK{0} ('@ts-tcs{0} (
    '@TGS-ts{0} '@TS{0}))) '@kTS{0}, 'EL{0} ('@dbK{0} ('@ts-tcs{0} ('@server-ts{0} '@S{0}))) '@kS{0}, 'T_clientCSE_resp{0}
    '@C{0} ('FRESH{0} ({'@C : '@client{0}} {'@S : '@server{0}} {'_ : '@shK{0} '@C{0} ('@server-ts{0} '@S{0})} {'_ : '@time{
    0}} {'_ : '@msg{0}} '@state{0}) ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0}))))))), '@Auth{0} '@C{0} (
    '@encrypt{0} ('@dbK-key{0} '@kTS{0}) $@&('@shK-msg{0} ('FRESH{0} ('@shK{0} '@C{0} ('@TGS-ts{0} '@TS{0})) ('suc{0} (
    'suc{0} '0{0}))), '@princ-msg{0} ('@tcs-princ{0} ('@client-tcs{0} '@C{0})))) '@TS{0} ('FRESH{0} ('@shK{0} '@C{0} (
    '@TGS-ts{0} '@TS{0})) ('suc{0} ('suc{0} '0{0}))), '@Service{0} '@C{0} ('@encrypt{0} ('@dbK-key{0} '@kS{0}) $@&(
    '@shK-msg{0} ('FRESH{0} ('@shK{0} '@C{0} ('@server-ts{0} '@S{0})) ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{
    0})))))), '@princ-msg{0} ('@tcs-princ{0} ('@client-tcs{0} '@C{0})))) '@S{0} ('FRESH{0} ('@shK{0} '@C{0} ('@server-ts{0}
    '@S{0})) ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0})))))), 'FRESH{0} ({'@C : '@client{0}} {'@S : '@server{0}} {
    '_ : '@shK{0} '@C{0} ('@server-ts{0} '@S{0})} {'_ : '@time{0}} {'_ : '@msg{0}} '@state{0}) ('suc{0} ('suc{0} ('suc{0} (
    'suc{0} ('suc{0} ('suc{0} '0{0})))))) '@C{0} '@S{0} ('FRESH{0} ('@shK{0} '@C{0} ('@server-ts{0} '@S{0})) ('suc{0} (
    'suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0})))))) ('FRESH{0} '@time{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{
    0} ('suc{0} '0{0})))))))) ('@encrypt{0} ('@dbK-key{0} '@kS{0}) $@&('@shK-msg{0} ('FRESH{0} ('@shK{0} '@C{0} (
    '@server-ts{0} '@S{0})) ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0})))))), '@princ-msg{0} ('@tcs-princ{0} (
    '@client-tcs{0} '@C{0}))))), $union('@Mem{0} '@S{0} '@C{0} ('FRESH{0} ('@shK{0} '@C{0} ('@server-ts{0} '@S{0})) ('suc{
    0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0})))))) ('FRESH{0} '@time{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} (
    'suc{0} ('suc{0} '0{0})))))))), $union('EL{0} '@server{0} '@S{0}, $union('@N{0} ('@encrypt{0} ('@shK-key{0} ('FRESH{0}
    ('@shK{0} '@C{0} ('@server-ts{0} '@S{0})) ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0}))))))) ('@time-msg{0} (
    'FRESH{0} '@time{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0})))))))))), 'F{0} ('suc{0} (
    'suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0}))))))))))))
New: $union($union('EL{0} '@KAS{0} '@AS{0}, 'EL{0} ('@dbK{0} ('@client-tcs{0} '@C{0})) '@kC{0}, 'EL{0} ('@dbK{0} ('@ts-tcs{
    0} ('@TGS-ts{0} '@TS{0}))) '@kTS{0}, 'EL{0} ('@dbK{0} ('@ts-tcs{0} ('@server-ts{0} '@S{0}))) '@kS{0},
    'T_clientCSE_resp{0} '@C{0} ('FRESH{0} ({'@C : '@client{0}} {'@S : '@server{0}} {'_ : '@shK{0} '@C{0} ('@server-ts{0}
    '@S{0})} {'_ : '@time{0}} {'_ : '@msg{0}} '@state{0}) ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{
    0}))))))), '@Auth{0} '@C{0} ('@encrypt{0} ('@dbK-key{0} '@kTS{0}) $@&('@shK-msg{0} ('FRESH{0} ('@shK{0} '@C{0} (
    '@TGS-ts{0} '@TS{0})) ('suc{0} ('suc{0} '0{0}))), '@princ-msg{0} ('@tcs-princ{0} ('@client-tcs{0} '@C{0})))) '@TS{0} (
    'FRESH{0} ('@shK{0} '@C{0} ('@TGS-ts{0} '@TS{0})) ('suc{0} ('suc{0} '0{0}))), '@Service{0} '@C{0} ('@encrypt{0} (
    '@dbK-key{0} '@kS{0}) $@&('@shK-msg{0} ('FRESH{0} ('@shK{0} '@C{0} ('@server-ts{0} '@S{0})) ('suc{0} ('suc{0} ('suc{0}
    ('suc{0} ('suc{0} '0{0})))))), '@princ-msg{0} ('@tcs-princ{0} ('@client-tcs{0} '@C{0})))) '@S{0} ('FRESH{0} ('@shK{0}
    '@C{0} ('@server-ts{0} '@S{0})) ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0})))))), 'FRESH{0} ({'@C : '@client{
    0}} {'@S : '@server{0}} {'_ : '@shK{0} '@C{0} ('@server-ts{0} '@S{0})} {'_ : '@time{0}} {'_ : '@msg{0}} '@state{0}) (
    'suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0})))))) '@C{0} '@S{0} ('FRESH{0} ('@shK{0} '@C{0} (
    '@server-ts{0} '@S{0})) ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0})))))) ('FRESH{0} '@time{0} ('suc{0} ('suc{0}
    ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0})))))))) ('@encrypt{0} ('@dbK-key{0} '@kS{0}) $@&('@shK-msg{0} (
    'FRESH{0} ('@shK{0} '@C{0} ('@server-ts{0} '@S{0})) ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0})))))),
    '@princ-msg{0} ('@tcs-princ{0} ('@client-tcs{0} '@C{0}))))), $union('@Mem{0} '@S{0} '@C{0} ('FRESH{0} ('@shK{0} '@C{0}
    ('@server-ts{0} '@S{0})) ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0})))))) ('FRESH{0} '@time{0} ('suc{0} ('suc{
    0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0})))))))), $union('EL{0} '@server{0} '@S{0}, $union('@N{0} (
    '@encrypt{0} ('@shK-key{0} ('FRESH{0} ('@shK{0} '@C{0} ('@server-ts{0} '@S{0})) ('suc{0} ('suc{0} ('suc{0} ('suc{0} (
    'suc{0} '0{0}))))))) ('@time-msg{0} ('FRESH{0} '@time{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0}
    '0{0})))))))))), 'F{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0}))))))))))))
*********** trial #11
crl $union('@N{0} ('@encrypt{0} ('@shK-key{0} @@SKey:Trm) ('@time-msg{0} @@t:Trm)), 'F{0} @fresh:Trm, @@L:Trm @@C:Trm
    @@S:Trm @@SKey:Trm @@t:Trm @@Y:Trm) => $union('@DoneMut{0} @@C:Trm @@S:Trm @@SKey:Trm, $union('F{0} @fresh':Trm,
    'T_clientCSE_req{0} @@C:Trm @@L:Trm)) if @@L:Trm := 'FRESH{0} ({'@C : '@client{0}} {'@S : '@server{0}} {'_ : '@shK{0}
    @@C:Trm ('@server-ts{0} @@S:Trm)} {'_ : '@time{0}} {'_ : '@msg{0}} '@state{0}) @fresh:Trm /\ @fresh':Trm := 'suc{0}
    @fresh:Trm .
@@SKey:Trm --> 'FRESH{0} ('@shK{0} '@C{0} ('@server-ts{0} '@S{0})) ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0})))))
@@t:Trm --> 'FRESH{0} '@time{0} ('suc{0} ('suc{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} ('suc{0} ('suc{0} '0{0})))))))
@@L:Trm --> 'FRESH{0} ({'@C : '@client{0}} {'@S : '@server{0}} {'_ : '@shK{0} '@C{0} ('@server-ts{0} '@S{0})} {'_ : '@time{
    0}} {'_ : '@msg{0}} '@state{0}) ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0}))))))
@@C:Trm --> '@C{0}
@@S:Trm --> '@S{0}
@@Y:Trm --> '@encrypt{0} ('@dbK-key{0} '@kS{0}) $@&('@shK-msg{0} ('FRESH{0} ('@shK{0} '@C{0} ('@server-ts{0} '@S{0})) (
    'suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0})))))), '@princ-msg{0} ('@tcs-princ{0} ('@client-tcs{0} '@C{0})))
@fresh':Trm --> (unbound)
*********** solving condition fragment
@@L:Trm := 'FRESH{0} ({'@C : '@client{0}} {'@S : '@server{0}} {'_ : '@shK{0} @@C:Trm ('@server-ts{0} @@S:Trm)} {'_ :
    '@time{0}} {'_ : '@msg{0}} '@state{0}) @fresh:Trm
*********** failure for condition fragment
@@L:Trm := 'FRESH{0} ({'@C : '@client{0}} {'@S : '@server{0}} {'_ : '@shK{0} @@C:Trm ('@server-ts{0} @@S:Trm)} {'_ :
    '@time{0}} {'_ : '@msg{0}} '@state{0}) @fresh:Trm
*********** failure #11
*********** trial #12
crl $union('@N{0} ('@encrypt{0} ('@shK-key{0} @@SKey:Trm) ('@time-msg{0} @@t:Trm)), 'F{0} @fresh:Trm, 'T_clientCSE_resp{0}
    @@C:Trm @@L:Trm, @@L:Trm @@C:Trm @@S:Trm @@SKey:Trm @@t:Trm @@Y:Trm) => $union('F{0} @fresh':Trm, '@DoneMut{0} @@C:Trm
    @@S:Trm @@SKey:Trm) if @fresh':Trm := @fresh:Trm .
@@SKey:Trm --> 'FRESH{0} ('@shK{0} '@C{0} ('@server-ts{0} '@S{0})) ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0})))))
@@t:Trm --> 'FRESH{0} '@time{0} ('suc{0} ('suc{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} ('suc{0} ('suc{0} '0{0})))))))
@@C:Trm --> '@C{0}
@@L:Trm --> 'FRESH{0} ({'@C : '@client{0}} {'@S : '@server{0}} {'_ : '@shK{0} '@C{0} ('@server-ts{0} '@S{0})} {'_ : '@time{
    0}} {'_ : '@msg{0}} '@state{0}) ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0}))))))
@@S:Trm --> '@S{0}
@@Y:Trm --> '@encrypt{0} ('@dbK-key{0} '@kS{0}) $@&('@shK-msg{0} ('FRESH{0} ('@shK{0} '@C{0} ('@server-ts{0} '@S{0})) (
    'suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0})))))), '@princ-msg{0} ('@tcs-princ{0} ('@client-tcs{0} '@C{0})))
@fresh':Trm --> (unbound)
*********** solving condition fragment
@fresh':Trm := @fresh:Trm
*********** success for condition fragment
@fresh':Trm := @fresh:Trm
@@SKey:Trm --> 'FRESH{0} ('@shK{0} '@C{0} ('@server-ts{0} '@S{0})) ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0})))))
@@t:Trm --> 'FRESH{0} '@time{0} ('suc{0} ('suc{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} ('suc{0} ('suc{0} '0{0})))))))
@@C:Trm --> '@C{0}
@@L:Trm --> 'FRESH{0} ({'@C : '@client{0}} {'@S : '@server{0}} {'_ : '@shK{0} '@C{0} ('@server-ts{0} '@S{0})} {'_ : '@time{
    0}} {'_ : '@msg{0}} '@state{0}) ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0}))))))
@@S:Trm --> '@S{0}
@@Y:Trm --> '@encrypt{0} ('@dbK-key{0} '@kS{0}) $@&('@shK-msg{0} ('FRESH{0} ('@shK{0} '@C{0} ('@server-ts{0} '@S{0})) (
    'suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0})))))), '@princ-msg{0} ('@tcs-princ{0} ('@client-tcs{0} '@C{0})))
@fresh':Trm --> 'suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0})))))))
*********** success #12
*********** rule
crl $union('@N{0} ('@encrypt{0} ('@shK-key{0} @@SKey:Trm) ('@time-msg{0} @@t:Trm)), 'F{0} @fresh:Trm, 'T_clientCSE_resp{0}
    @@C:Trm @@L:Trm, @@L:Trm @@C:Trm @@S:Trm @@SKey:Trm @@t:Trm @@Y:Trm) => $union('F{0} @fresh':Trm, '@DoneMut{0} @@C:Trm
    @@S:Trm @@SKey:Trm) if @fresh':Trm := @fresh:Trm .
@@SKey:Trm --> 'FRESH{0} ('@shK{0} '@C{0} ('@server-ts{0} '@S{0})) ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0})))))
@@t:Trm --> 'FRESH{0} '@time{0} ('suc{0} ('suc{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} ('suc{0} ('suc{0} '0{0})))))))
@@C:Trm --> '@C{0}
@@L:Trm --> 'FRESH{0} ({'@C : '@client{0}} {'@S : '@server{0}} {'_ : '@shK{0} '@C{0} ('@server-ts{0} '@S{0})} {'_ : '@time{
    0}} {'_ : '@msg{0}} '@state{0}) ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0}))))))
@@S:Trm --> '@S{0}
@@Y:Trm --> '@encrypt{0} ('@dbK-key{0} '@kS{0}) $@&('@shK-msg{0} ('FRESH{0} ('@shK{0} '@C{0} ('@server-ts{0} '@S{0})) (
    'suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0})))))), '@princ-msg{0} ('@tcs-princ{0} ('@client-tcs{0} '@C{0})))
@fresh':Trm --> 'suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0})))))))
Old: $union('@N{0} ('@encrypt{0} ('@shK-key{0} ('FRESH{0} ('@shK{0} '@C{0} ('@server-ts{0} '@S{0})) ('suc{0} ('suc{0} (
    'suc{0} ('suc{0} ('suc{0} '0{0}))))))) ('@time-msg{0} ('FRESH{0} '@time{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0}
    ('suc{0} ('suc{0} '0{0})))))))))), 'F{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{
    0})))))))), 'EL{0} '@KAS{0} '@AS{0}, 'EL{0} '@server{0} '@S{0}, 'EL{0} ('@dbK{0} ('@client-tcs{0} '@C{0})) '@kC{0},
    'EL{0} ('@dbK{0} ('@ts-tcs{0} ('@TGS-ts{0} '@TS{0}))) '@kTS{0}, 'EL{0} ('@dbK{0} ('@ts-tcs{0} ('@server-ts{0} '@S{0})))
    '@kS{0}, 'T_clientCSE_resp{0} '@C{0} ('FRESH{0} ({'@C : '@client{0}} {'@S : '@server{0}} {'_ : '@shK{0} '@C{0} (
    '@server-ts{0} '@S{0})} {'_ : '@time{0}} {'_ : '@msg{0}} '@state{0}) ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} (
    'suc{0} '0{0}))))))), '@Auth{0} '@C{0} ('@encrypt{0} ('@dbK-key{0} '@kTS{0}) $@&('@shK-msg{0} ('FRESH{0} ('@shK{0} '@C{
    0} ('@TGS-ts{0} '@TS{0})) ('suc{0} ('suc{0} '0{0}))), '@princ-msg{0} ('@tcs-princ{0} ('@client-tcs{0} '@C{0})))) '@TS{
    0} ('FRESH{0} ('@shK{0} '@C{0} ('@TGS-ts{0} '@TS{0})) ('suc{0} ('suc{0} '0{0}))), '@Mem{0} '@S{0} '@C{0} ('FRESH{0} (
    '@shK{0} '@C{0} ('@server-ts{0} '@S{0})) ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0})))))) ('FRESH{0} '@time{0}
    ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0})))))))), '@Service{0} '@C{0} ('@encrypt{0} (
    '@dbK-key{0} '@kS{0}) $@&('@shK-msg{0} ('FRESH{0} ('@shK{0} '@C{0} ('@server-ts{0} '@S{0})) ('suc{0} ('suc{0} ('suc{0}
    ('suc{0} ('suc{0} '0{0})))))), '@princ-msg{0} ('@tcs-princ{0} ('@client-tcs{0} '@C{0})))) '@S{0} ('FRESH{0} ('@shK{0}
    '@C{0} ('@server-ts{0} '@S{0})) ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0})))))), 'FRESH{0} ({'@C : '@client{
    0}} {'@S : '@server{0}} {'_ : '@shK{0} '@C{0} ('@server-ts{0} '@S{0})} {'_ : '@time{0}} {'_ : '@msg{0}} '@state{0}) (
    'suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0})))))) '@C{0} '@S{0} ('FRESH{0} ('@shK{0} '@C{0} (
    '@server-ts{0} '@S{0})) ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0})))))) ('FRESH{0} '@time{0} ('suc{0} ('suc{0}
    ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0})))))))) ('@encrypt{0} ('@dbK-key{0} '@kS{0}) $@&('@shK-msg{0} (
    'FRESH{0} ('@shK{0} '@C{0} ('@server-ts{0} '@S{0})) ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0})))))),
    '@princ-msg{0} ('@tcs-princ{0} ('@client-tcs{0} '@C{0})))))
$union('@N{0} ('@encrypt{0} ('@shK-key{0} ('FRESH{0} ('@shK{0} '@C{0} ('@server-ts{0} '@S{0})) ('suc{0} ('suc{0} ('suc{0} (
    'suc{0} ('suc{0} '0{0}))))))) ('@time-msg{0} ('FRESH{0} '@time{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0}
    ('suc{0} '0{0})))))))))), 'F{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0})))))))),
    'EL{0} '@KAS{0} '@AS{0}, 'EL{0} '@server{0} '@S{0}, 'EL{0} ('@dbK{0} ('@client-tcs{0} '@C{0})) '@kC{0}, 'EL{0} ('@dbK{
    0} ('@ts-tcs{0} ('@TGS-ts{0} '@TS{0}))) '@kTS{0}, 'EL{0} ('@dbK{0} ('@ts-tcs{0} ('@server-ts{0} '@S{0}))) '@kS{0},
    'T_clientCSE_resp{0} '@C{0} ('FRESH{0} ({'@C : '@client{0}} {'@S : '@server{0}} {'_ : '@shK{0} '@C{0} ('@server-ts{0}
    '@S{0})} {'_ : '@time{0}} {'_ : '@msg{0}} '@state{0}) ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{
    0}))))))), '@Auth{0} '@C{0} ('@encrypt{0} ('@dbK-key{0} '@kTS{0}) $@&('@shK-msg{0} ('FRESH{0} ('@shK{0} '@C{0} (
    '@TGS-ts{0} '@TS{0})) ('suc{0} ('suc{0} '0{0}))), '@princ-msg{0} ('@tcs-princ{0} ('@client-tcs{0} '@C{0})))) '@TS{0} (
    'FRESH{0} ('@shK{0} '@C{0} ('@TGS-ts{0} '@TS{0})) ('suc{0} ('suc{0} '0{0}))), '@Mem{0} '@S{0} '@C{0} ('FRESH{0} ('@shK{
    0} '@C{0} ('@server-ts{0} '@S{0})) ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0})))))) ('FRESH{0} '@time{0} ('suc{
    0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0})))))))), '@Service{0} '@C{0} ('@encrypt{0} ('@dbK-key{0}
    '@kS{0}) $@&('@shK-msg{0} ('FRESH{0} ('@shK{0} '@C{0} ('@server-ts{0} '@S{0})) ('suc{0} ('suc{0} ('suc{0} ('suc{0} (
    'suc{0} '0{0})))))), '@princ-msg{0} ('@tcs-princ{0} ('@client-tcs{0} '@C{0})))) '@S{0} ('FRESH{0} ('@shK{0} '@C{0} (
    '@server-ts{0} '@S{0})) ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0})))))), 'FRESH{0} ({'@C : '@client{0}} {'@S :
    '@server{0}} {'_ : '@shK{0} '@C{0} ('@server-ts{0} '@S{0})} {'_ : '@time{0}} {'_ : '@msg{0}} '@state{0}) ('suc{0} (
    'suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0})))))) '@C{0} '@S{0} ('FRESH{0} ('@shK{0} '@C{0} ('@server-ts{0} '@S{
    0})) ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0})))))) ('FRESH{0} '@time{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0}
    ('suc{0} ('suc{0} ('suc{0} '0{0})))))))) ('@encrypt{0} ('@dbK-key{0} '@kS{0}) $@&('@shK-msg{0} ('FRESH{0} ('@shK{0}
    '@C{0} ('@server-ts{0} '@S{0})) ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0})))))), '@princ-msg{0} ('@tcs-princ{
    0} ('@client-tcs{0} '@C{0})))))
--->
$union($union('EL{0} '@KAS{0} '@AS{0}, 'EL{0} '@server{0} '@S{0}, 'EL{0} ('@dbK{0} ('@client-tcs{0} '@C{0})) '@kC{0}, 'EL{
    0} ('@dbK{0} ('@ts-tcs{0} ('@TGS-ts{0} '@TS{0}))) '@kTS{0}, 'EL{0} ('@dbK{0} ('@ts-tcs{0} ('@server-ts{0} '@S{0})))
    '@kS{0}, '@Auth{0} '@C{0} ('@encrypt{0} ('@dbK-key{0} '@kTS{0}) $@&('@shK-msg{0} ('FRESH{0} ('@shK{0} '@C{0} ('@TGS-ts{
    0} '@TS{0})) ('suc{0} ('suc{0} '0{0}))), '@princ-msg{0} ('@tcs-princ{0} ('@client-tcs{0} '@C{0})))) '@TS{0} ('FRESH{0}
    ('@shK{0} '@C{0} ('@TGS-ts{0} '@TS{0})) ('suc{0} ('suc{0} '0{0}))), '@Mem{0} '@S{0} '@C{0} ('FRESH{0} ('@shK{0} '@C{0}
    ('@server-ts{0} '@S{0})) ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0})))))) ('FRESH{0} '@time{0} ('suc{0} ('suc{
    0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0})))))))), '@Service{0} '@C{0} ('@encrypt{0} ('@dbK-key{0} '@kS{0})
    $@&('@shK-msg{0} ('FRESH{0} ('@shK{0} '@C{0} ('@server-ts{0} '@S{0})) ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{
    0})))))), '@princ-msg{0} ('@tcs-princ{0} ('@client-tcs{0} '@C{0})))) '@S{0} ('FRESH{0} ('@shK{0} '@C{0} ('@server-ts{0}
    '@S{0})) ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0}))))))), $union('F{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} (
    'suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0})))))))), '@DoneMut{0} '@C{0} '@S{0} ('FRESH{0} ('@shK{0} '@C{0} ('@server-ts{
    0} '@S{0})) ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0}))))))))
New: $union($union('EL{0} '@KAS{0} '@AS{0}, 'EL{0} '@server{0} '@S{0}, 'EL{0} ('@dbK{0} ('@client-tcs{0} '@C{0})) '@kC{0},
    'EL{0} ('@dbK{0} ('@ts-tcs{0} ('@TGS-ts{0} '@TS{0}))) '@kTS{0}, 'EL{0} ('@dbK{0} ('@ts-tcs{0} ('@server-ts{0} '@S{0})))
    '@kS{0}, '@Auth{0} '@C{0} ('@encrypt{0} ('@dbK-key{0} '@kTS{0}) $@&('@shK-msg{0} ('FRESH{0} ('@shK{0} '@C{0} ('@TGS-ts{
    0} '@TS{0})) ('suc{0} ('suc{0} '0{0}))), '@princ-msg{0} ('@tcs-princ{0} ('@client-tcs{0} '@C{0})))) '@TS{0} ('FRESH{0}
    ('@shK{0} '@C{0} ('@TGS-ts{0} '@TS{0})) ('suc{0} ('suc{0} '0{0}))), '@Mem{0} '@S{0} '@C{0} ('FRESH{0} ('@shK{0} '@C{0}
    ('@server-ts{0} '@S{0})) ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0})))))) ('FRESH{0} '@time{0} ('suc{0} ('suc{
    0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0})))))))), '@Service{0} '@C{0} ('@encrypt{0} ('@dbK-key{0} '@kS{0})
    $@&('@shK-msg{0} ('FRESH{0} ('@shK{0} '@C{0} ('@server-ts{0} '@S{0})) ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{
    0})))))), '@princ-msg{0} ('@tcs-princ{0} ('@client-tcs{0} '@C{0})))) '@S{0} ('FRESH{0} ('@shK{0} '@C{0} ('@server-ts{0}
    '@S{0})) ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0}))))))), $union('F{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} (
    'suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0})))))))), '@DoneMut{0} '@C{0} '@S{0} ('FRESH{0} ('@shK{0} '@C{0} ('@server-ts{
    0} '@S{0})) ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0}))))))))
rewrites: 18 in 90ms cpu (512ms real) (197 rewrites/second)
result Trm: $union('F{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0})))))))), 'EL{0}
    '@KAS{0} '@AS{0}, 'EL{0} '@server{0} '@S{0}, 'EL{0} ('@dbK{0} ('@client-tcs{0} '@C{0})) '@kC{0}, 'EL{0} ('@dbK{0} (
    '@ts-tcs{0} ('@TGS-ts{0} '@TS{0}))) '@kTS{0}, 'EL{0} ('@dbK{0} ('@ts-tcs{0} ('@server-ts{0} '@S{0}))) '@kS{0},
    '@DoneMut{0} '@C{0} '@S{0} ('FRESH{0} ('@shK{0} '@C{0} ('@server-ts{0} '@S{0})) ('suc{0} ('suc{0} ('suc{0} ('suc{0} (
    'suc{0} '0{0})))))), '@Auth{0} '@C{0} ('@encrypt{0} ('@dbK-key{0} '@kTS{0}) $@&('@shK-msg{0} ('FRESH{0} ('@shK{0} '@C{
    0} ('@TGS-ts{0} '@TS{0})) ('suc{0} ('suc{0} '0{0}))), '@princ-msg{0} ('@tcs-princ{0} ('@client-tcs{0} '@C{0})))) '@TS{
    0} ('FRESH{0} ('@shK{0} '@C{0} ('@TGS-ts{0} '@TS{0})) ('suc{0} ('suc{0} '0{0}))), '@Mem{0} '@S{0} '@C{0} ('FRESH{0} (
    '@shK{0} '@C{0} ('@server-ts{0} '@S{0})) ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0})))))) ('FRESH{0} '@time{0}
    ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0})))))))), '@Service{0} '@C{0} ('@encrypt{0} (
    '@dbK-key{0} '@kS{0}) $@&('@shK-msg{0} ('FRESH{0} ('@shK{0} '@C{0} ('@server-ts{0} '@S{0})) ('suc{0} ('suc{0} ('suc{0}
    ('suc{0} ('suc{0} '0{0})))))), '@princ-msg{0} ('@tcs-princ{0} ('@client-tcs{0} '@C{0})))) '@S{0} ('FRESH{0} ('@shK{0}
    '@C{0} ('@server-ts{0} '@S{0})) ('suc{0} ('suc{0} ('suc{0} ('suc{0} ('suc{0} '0{0})))))))
Maude>