CfP: CI-BD-SOQE 2026: Workshop on Craig Interpolation, Beth Definability, and Second-Order Quantifier Elimination

Christoph Wernhard via clean-list <[email protected]> Wed, 25 Feb 2026 07:47:42 +0100
Newsgroups gmane.comp.lang.clean
Message-ID <[email protected]>
W0Fwb2xvZ2llcyBpZiB5b3UgcmVjZWl2ZSBtdWx0aXBsZSBjb3BpZXMuIFBsZWFzZSBmb3J3YXJk
CiAgdGhpcyBjYWxsIHRvIGludGVyZXN0ZWQgcGFydGllcy5dCgogICAgICAgICAgICAgICAgICAg
ICAgIENBTEwgRk9SIFBBUEVSUwoKICAgICAgICAgICAgICAgICAgICAgICBDSS1CRC1TT1FFIDIw
MjYKICAgICBXT1JLU0hPUCBPTiBDUkFJRyBJTlRFUlBPTEFUSU9OLCBCRVRIIERFRklOQUJJTElU
WSwKICAgICAgICAgICBBTkQgU0VDT05ELU9SREVSIFFVQU5USUZJRVIgRUxJTUlOQVRJT04KCiAg
ICAgICAgICAgICAgICAgRkxvQyAyMDI2LCBMaXNib24sIFBvcnR1Z2FsCiAgICAgICAgICAgICAg
ICAgICAgICAgMjQtMjUgSnVseSAyMDI2CgogICAgICAgICAgICAgICAgICAgICBEZWFkbGluZTog
NCBNYXkgMjAyNgoKICAgICAgICAgICAgICAgICBodHRwczovL2V1cjAxLnNhZmVsaW5rcy5wcm90
ZWN0aW9uLm91dGxvb2suY29tLz91cmw9aHR0cCUzQSUyRiUyRjIwMjYuY2ktYmQuc29xZS5vcmcl
MkYmZGF0YT0wNSU3QzAyJTdDY2xlYW4tbGlzdCU0MHNjaWVuY2UucnUubmwlN0M5ODI0OWE4N2Ni
NzA0YmM4YTVlOTA4ZGU3NDM5YzgyOCU3QzA4NDU3OGQ5NDAwZDRhNWFhN2M3ZTc2Y2E0N2FmNDAw
JTdDMSU3QzAlN0M2MzkwNzU5ODg2NzcwODAyNzAlN0NVbmtub3duJTdDVFdGcGJHWnNiM2Q4ZXlK
RmJYQjBlVTFoY0draU9uUnlkV1VzSWxZaU9pSXdMakF1TURBd01DSXNJbEFpT2lKWGFXNHpNaUlz
SWtGT0lqb2lUV0ZwYkNJc0lsZFVJam95ZlElM0QlM0QlN0MwJTdDJTdDJTdDJnNkYXRhPUV0cGJW
OFZQN3piaCUyRkE1MzF1SjI1NTB3c0JxVzhOUVVweUc1amdPOVU2dyUzRCZyZXNlcnZlZD0wCgpH
RU5FUkFMIElORk9STUFUSU9OCgogICAgQ0ktQkQtU09RRSAyMDI2IGlzIGEgRkxvQyAyMDI2IHdv
cmtzaG9wIGFuZCB3aWxsIHRha2UKICAgIHBsYWNlIGluIExpc2JvbiwgUG9ydHVnYWwsIDI0LTI1
IEp1bHkgMjAyNi4gSXQgY29udGludWVzCiAgICBhIHNlcmllcyBvZiBwcmV2aW91cyB3b3Jrc2hv
cHMgb24gQ3JhaWcgSW50ZXJwb2xhdGlvbgogICAgKENJKSwgQmV0aCBEZWZpbmFiaWxpdHkgKEJE
KSwgYW5kIFNlY29uZC1PcmRlciBRdWFudGlmaWVyCiAgICBFbGltaW5hdGlvbiAoU09RRSk6Cgog
ICAgKiBXb3Jrc2hvcCBvbiBDcmFpZyBJbnRlcnBvbGF0aW9uIGFuZCBCZXRoIERlZmluYWJpbGl0
eQogICAgICAoQ0lCRCAyMDI0LCBodHRwczovL2V1cjAxLnNhZmVsaW5rcy5wcm90ZWN0aW9uLm91
dGxvb2suY29tLz91cmw9aHR0cHMlM0ElMkYlMkZjaWJkLmJpdGJ1Y2tldC5pbyUyRmNpYmQyMDI0
JTJGJmRhdGE9MDUlN0MwMiU3Q2NsZWFuLWxpc3QlNDBzY2llbmNlLnJ1Lm5sJTdDOTgyNDlhODdj
YjcwNGJjOGE1ZTkwOGRlNzQzOWM4MjglN0MwODQ1NzhkOTQwMGQ0YTVhYTdjN2U3NmNhNDdhZjQw
MCU3QzElN0MwJTdDNjM5MDc1OTg4NjkxOTU2MzIxJTdDVW5rbm93biU3Q1RXRnBiR1pzYjNkOGV5
SkZiWEIwZVUxaGNHa2lPblJ5ZFdVc0lsWWlPaUl3TGpBdU1EQXdNQ0lzSWxBaU9pSlhhVzR6TWlJ
c0lrRk9Jam9pVFdGcGJDSXNJbGRVSWpveWZRJTNEJTNEJTdDMCU3QyU3QyU3QyZzZGF0YT1DMUsz
ckZOS3FteHlTZzN3JTJGR3BTJTJCaDkxVWw0SkhSblNRRklTZU5sT1Z2VSUzRCZyZXNlcnZlZD0w
KQogICAgKiA0dGggV29ya3Nob3Agb24gSW50ZXJwb2xhdGlvbjogRnJvbSBQcm9vZnMgdG8KICAg
ICAgQXBwbGljYXRpb25zIChpUFJBIDIwMjIsIGh0dHBzOi8vZXVyMDEuc2FmZWxpbmtzLnByb3Rl
Y3Rpb24ub3V0bG9vay5jb20vP3VybD1odHRwcyUzQSUyRiUyRmlwcmEtMjAyMi5iaXRidWNrZXQu
aW8lMkYmZGF0YT0wNSU3QzAyJTdDY2xlYW4tbGlzdCU0MHNjaWVuY2UucnUubmwlN0M5ODI0OWE4
N2NiNzA0YmM4YTVlOTA4ZGU3NDM5YzgyOCU3QzA4NDU3OGQ5NDAwZDRhNWFhN2M3ZTc2Y2E0N2Fm
NDAwJTdDMSU3QzAlN0M2MzkwNzU5ODg2OTE5NzE2MjIlN0NVbmtub3duJTdDVFdGcGJHWnNiM2Q4
ZXlKRmJYQjBlVTFoY0draU9uUnlkV1VzSWxZaU9pSXdMakF1TURBd01DSXNJbEFpT2lKWGFXNHpN
aUlzSWtGT0lqb2lUV0ZwYkNJc0lsZFVJam95ZlElM0QlM0QlN0MwJTdDJTdDJTdDJnNkYXRhPW9G
TSUyRkdyaHJwYTV3Zm1lTWllVWVtZGRWJTJGcXYlMkJqRDVSVENHdWxvaHBVMDAlM0QmcmVzZXJ2
ZWQ9MCkKICAgICogU2Vjb25kIFdvcmtzaG9wIG9uIFNlY29uZC1PcmRlciBRdWFudGlmaWVyIEVs
aW1pbmF0aW9uCiAgICAgIGFuZCBSZWxhdGVkIFRvcGljcyAoU09RRSAyMDIxLCBodHRwczovL2V1
cjAxLnNhZmVsaW5rcy5wcm90ZWN0aW9uLm91dGxvb2suY29tLz91cmw9aHR0cCUzQSUyRiUyRjIw
MjEuc29xZS5vcmclMkYmZGF0YT0wNSU3QzAyJTdDY2xlYW4tbGlzdCU0MHNjaWVuY2UucnUubmwl
N0M5ODI0OWE4N2NiNzA0YmM4YTVlOTA4ZGU3NDM5YzgyOCU3QzA4NDU3OGQ5NDAwZDRhNWFhN2M3
ZTc2Y2E0N2FmNDAwJTdDMSU3QzAlN0M2MzkwNzU5ODg2OTE5ODUyMDUlN0NVbmtub3duJTdDVFdG
cGJHWnNiM2Q4ZXlKRmJYQjBlVTFoY0draU9uUnlkV1VzSWxZaU9pSXdMakF1TURBd01DSXNJbEFp
T2lKWGFXNHpNaUlzSWtGT0lqb2lUV0ZwYkNJc0lsZFVJam95ZlElM0QlM0QlN0MwJTdDJTdDJTdD
JnNkYXRhPWVWSWpSYSUyQmF0JTJCJTJCeHJCR2VtYTVpTkNDTjEwRSUyQmhpMU1Pb0F3M2ZUakVq
USUzRCZyZXNlcnZlZD0wKTsKICAgICogRmlyc3QgV29ya3Nob3Agb24gU2Vjb25kLU9yZGVyIFF1
YW50aWZpZXIgRWxpbWluYXRpb24gYW5kCiAgICAgIFJlbGF0ZWQgVG9waWNzIChTT1FFIDIwMTcs
IGh0dHBzOi8vZXVyMDEuc2FmZWxpbmtzLnByb3RlY3Rpb24ub3V0bG9vay5jb20vP3VybD1odHRw
JTNBJTJGJTJGMjAxNy5zb3FlLm9yZyUyRiZkYXRhPTA1JTdDMDIlN0NjbGVhbi1saXN0JTQwc2Np
ZW5jZS5ydS5ubCU3Qzk4MjQ5YTg3Y2I3MDRiYzhhNWU5MDhkZTc0MzljODI4JTdDMDg0NTc4ZDk0
MDBkNGE1YWE3YzdlNzZjYTQ3YWY0MDAlN0MxJTdDMCU3QzYzOTA3NTk4ODY5MTk5ODU3MyU3Q1Vu
a25vd24lN0NUV0ZwYkdac2IzZDhleUpGYlhCMGVVMWhjR2tpT25SeWRXVXNJbFlpT2lJd0xqQXVN
REF3TUNJc0lsQWlPaUpYYVc0ek1pSXNJa0ZPSWpvaVRXRnBiQ0lzSWxkVUlqb3lmUSUzRCUzRCU3
QzAlN0MlN0MlN0Mmc2RhdGE9YnR2elpidlVaTG8wJTJCRHlqZEROR1VtUFclMkJrOEtmS0ZrVkxS
dk15UnZEODQlM0QmcmVzZXJ2ZWQ9MCkuCgpUT1BJQ1MgQU5EIEFJTQoKICAgIEJyb2FkbHkgdmll
d2VkLCBDcmFpZyBJbnRlcnBvbGF0aW9uIChDSSksIEJldGgKICAgIERlZmluYWJpbGl0eSAoQkQp
LCBhbmQgU2Vjb25kLU9yZGVyIFF1YW50aWZpZXIKICAgIEVsaW1pbmF0aW9uIChTT1FFKSBjb25j
ZXJuIHRoZSBleGlzdGVuY2UgYW5kIGNvbXB1dGF0aW9uCiAgICBvZiBmb3JtdWxhcyB0aGF0IGNh
cHR1cmUgY29uc2VxdWVuY2VzIG9yIGxvZ2ljYWwKICAgIGNvbnN0cmFpbnRzIHVuZGVyIHNvbWUg
c3ludGFjdGljIHJlc3RyaWN0aW9ucy4gU2luY2Ugc3VjaAogICAgZXhpc3RlbmNlL2NvbXB1dGF0
aW9uIHF1ZXN0aW9ucyBhcmlzZSBpbiBtYW55IGFyZWFzIG9mCiAgICBjb21wdXRlciBzY2llbmNl
LCBDSSwgQkQsIGFuZCBTT1FFIGhhdmUgYmVlbiB0aG9yb3VnaGx5CiAgICBpbnZlc3RpZ2F0ZWQg
YnkgZGlmZmVyZW50IGNvbW11bml0aWVzLCB3aGljaCBoYXMgbGVkIHRvIGEKICAgIGxhcmdlIG51
bWJlciBvZiByZXN1bHRzLCBmcm9tIGZvdW5kYXRpb25hbCBpc3N1ZXMgdG8KICAgIHByYWN0aWNh
bCBhcHBsaWNhdGlvbnMuIFJlbGV2YW50IGZpZWxkcyBpbmNsdWRlIHByb29mCiAgICB0aGVvcnks
IG1vZGVsIHRoZW9yeSwgcHJvb2YgY29tcGxleGl0eSwgYXV0b21hdGVkCiAgICByZWFzb25pbmcs
IGF1dG9tYXRhIHRoZW9yeSwga25vd2xlZGdlIHJlcHJlc2VudGF0aW9uLAogICAgcHJvZ3JhbSB2
ZXJpZmljYXRpb24gYW5kIGRhdGFiYXNlcyBhcyB3ZWxsIGFzIHBoaWxvc29waHkKICAgIGFuZCBs
aW5ndWlzdGljcy4KCiAgICBUb3BpY3Mgb2YgaW50ZXJlc3QgZm9yIHRoZSB3b3Jrc2hvcCBpbmNs
dWRlLCBidXQgYXJlIG5vdAogICAgbGltaXRlZCB0bzoKCiAgICAqIEFiZHVjdGl2ZSByZWFzb25p
bmcKICAgICogQWxnb3JpdGhtcyBmb3IgQ0ksIEJELCBTT1FFIGFuZCByZWxhdGVkIHRhc2tzCiAg
ICAqIEFwcGxpY2F0aW9ucyBvZiBDSSwgQkQsIFNPUUUgYW5kIHJlbGF0ZWQgdGVjaG5pcXVlcwog
ICAgKiBBdXRvbWF0aW5nIGNpcmN1bXNjcmlwdGlvbgogICAgKiBBdXRvbWF0aW5nIG1vZGFsIGNv
cnJlc3BvbmRlbmNlIHRoZW9yeQogICAgKiBDSSBhbmQgQkQgZm9yIHNwZWNpZmljIGxvZ2ljcwog
ICAgKiBDSSBhbmQgQkQgaW4gbW9kZWwgdGhlb3J5CiAgICAqIENJIGluIHByb2dyYW0gdmVyaWZp
Y2F0aW9uCiAgICAqIEZvcmdldHRpbmcgaW4gYW5zd2VyIHNldCBwcm9ncmFtbWluZwogICAgKiBG
b3JnZXR0aW5nIGluIGtub3dsZWRnZSByZXByZXNlbnRhdGlvbgogICAgKiBHZW5lcmFsaXphdGlv
bnMgb2YgQ0kKICAgICogR2VuZXJhdGluZyBleHBsYW5hdGlvbnMgdmlhIENJCiAgICAqIEltcGxl
bWVudGF0aW9uIG9mIENJLCBCRCwgU09RRSBhbmQgcmVsYXRlZCB0YXNrcwogICAgKiBPbnRvbG9n
eSBtb2R1bGFyaXphdGlvbiBhbmQgY29udGVudCBleHRyYWN0aW9uCiAgICAqIFByb29mIGNvbXBs
ZXhpdHkgYW5kIGZlYXNpYmxlIGludGVycG9sYXRpb24KICAgICogUHJvb2Ygc3lzdGVtcyBmb3Ig
Q0kgYW5kIEJECiAgICAqIFF1ZXJ5IHJld3JpdGluZyBvbiB0aGUgYmFzaXMgb2YgQ0kgYW5kIEJE
CiAgICAqIFNlcGFyYWJpbGl0eQogICAgKiBTb2x2aW5nIGNvbnN0cmFpbmVkIEhvcm4gY2xhdXNl
cwogICAgKiBTb2x2aW5nIGZvcm11bGEgZXF1YXRpb25zCiAgICAqIFVuaWZvcm0gaW50ZXJwb2xh
dGlvbgoKICAgIFRoZSBhaW0gb2YgdGhlIHdvcmtzaG9wIGlzIHRvIGJyaW5nIHRvZ2V0aGVyIHJl
c2VhcmNoZXJzCiAgICBmcm9tIHRoZSBtYW55IHJlbGV2YW50IGZpZWxkcyB0byBleGNoYW5nZSBl
eHBlcmllbmNlcyBhbmQKICAgIGZpbmRpbmdzIGFib3V0IGFwcHJvYWNoZXMsIHRlY2huaXF1ZXMs
IG9uZ29pbmcgcmVzZWFyY2gKICAgIGFuZCBpbXBvcnRhbnQgb3BlbiBwcm9ibGVtcy4gV2Ugc3Ry
b25nbHkgYmVsaWV2ZSB0aGF0IENJLAogICAgQkQsIGFuZCBTT1FFIC0gYmV5b25kIHNoYXJpbmcg
YSBzaW1pbGFyIGhpc3RvcmljYWwKICAgIGJhY2tncm91bmQgLSBvZmZlciBhIGNvbW1vbiBiYXNp
cyBmb3IgZnJ1aXRmdWwKICAgIGNyb3NzLWRpc2NpcGxpbmFyeSBleGNoYW5nZS4KClNVQk1JU1NJ
T04KCiAgICBXZSBpbnZpdGUgc3VibWlzc2lvbnMgb2Y6CgogICAgKiBXb3JrcyB3aXRoIG9yaWdp
bmFsIHJlc2VhcmNoLCBlaXRoZXIgYXMKICAgICAgLSBGdWxsIHBhcGVyOiAxMC0xNSBwYWdlcyAr
IHJlZmVyZW5jZXMsIG9yCiAgICAgIC0gRXh0ZW5kZWQgYWJzdHJhY3Q6IDUtOSBwYWdlcyArIHJl
ZmVyZW5jZXMKCiAgICAqIEFic3RyYWN0cyBvZiByZXNlYXJjaCBwdWJsaXNoZWQgZWxzZXdoZXJl
LCBhcwogICAgICAtIEFic3RyYWN0OiAxLTQgcGFnZXMgKyByZWZlcmVuY2VzCgogICAgUHJlc2Vu
dGF0aW9ucyBvZiBhcHBsaWNhdGlvbnMsIG5ldyBzeXN0ZW1zIG9yIHJlbGV2YW50CiAgICBiZW5j
aG1hcmtzIGFyZSB3ZWxjb21lLgoKICAgIEl0IGlzIGV4cGVjdGVkIHRoYXQgYWNjZXB0ZWQgc3Vi
bWlzc2lvbnMgYXJlIHByZXNlbnRlZCBhdAogICAgdGhlIHdvcmtzaG9wIGJ5IGF0IGxlYXN0IG9u
ZSBvZiB0aGUgYXV0aG9ycy4KCiAgICBTdWJtaXNzaW9ucyBzaG91bGQgYmUgd3JpdHRlbiBpbiBF
bmdsaXNoLCBmb3JtYXR0ZWQgd2l0aAogICAgdGhlIENFVVJBUlQgc3R5bGUKICAgIChodHRwczov
L2V1cjAxLnNhZmVsaW5rcy5wcm90ZWN0aW9uLm91dGxvb2suY29tLz91cmw9aHR0cHMlM0ElMkYl
MkZjZXVyLXdzLm9yZyUyRkhPV1RPU1VCTUlULmh0bWwlMjNDRVVSQVJUJmRhdGE9MDUlN0MwMiU3
Q2NsZWFuLWxpc3QlNDBzY2llbmNlLnJ1Lm5sJTdDOTgyNDlhODdjYjcwNGJjOGE1ZTkwOGRlNzQz
OWM4MjglN0MwODQ1NzhkOTQwMGQ0YTVhYTdjN2U3NmNhNDdhZjQwMCU3QzElN0MwJTdDNjM5MDc1
OTg4NjkyMDExNDIwJTdDVW5rbm93biU3Q1RXRnBiR1pzYjNkOGV5SkZiWEIwZVUxaGNHa2lPblJ5
ZFdVc0lsWWlPaUl3TGpBdU1EQXdNQ0lzSWxBaU9pSlhhVzR6TWlJc0lrRk9Jam9pVFdGcGJDSXNJ
bGRVSWpveWZRJTNEJTNEJTdDMCU3QyU3QyU3QyZzZGF0YT1tJTJGMk9NeCUyQklqd3JuSU51aHZ1
VE1SSlUlMkYzOTgyc2hHdW1pSGE1WTREb0s4JTNEJnJlc2VydmVkPTApLgoKICAgIFN1Ym1pc3Np
b25zIG11c3QgYmUgdXBsb2FkZWQgdmlhIHRoZSBzdWJtaXNzaW9uIHBhZ2UKICAgIGh0dHBzOi8v
ZXVyMDEuc2FmZWxpbmtzLnByb3RlY3Rpb24ub3V0bG9vay5jb20vP3VybD1odHRwcyUzQSUyRiUy
RnN1Ym1pc3Npb25zLmZsb2MyNi5vcmclMkZjaS1iZC1zb3FlJTJGJmRhdGE9MDUlN0MwMiU3Q2Ns
ZWFuLWxpc3QlNDBzY2llbmNlLnJ1Lm5sJTdDOTgyNDlhODdjYjcwNGJjOGE1ZTkwOGRlNzQzOWM4
MjglN0MwODQ1NzhkOTQwMGQ0YTVhYTdjN2U3NmNhNDdhZjQwMCU3QzElN0MwJTdDNjM5MDc1OTg4
NjkyMDI0MDc1JTdDVW5rbm93biU3Q1RXRnBiR1pzYjNkOGV5SkZiWEIwZVUxaGNHa2lPblJ5ZFdV
c0lsWWlPaUl3TGpBdU1EQXdNQ0lzSWxBaU9pSlhhVzR6TWlJc0lrRk9Jam9pVFdGcGJDSXNJbGRV
SWpveWZRJTNEJTNEJTdDMCU3QyU3QyU3QyZzZGF0YT02T0olMkJLam5kcHBOVTNXZlJlaHdwWDR0
dDl1Uk1BYkxqV1NLUzJ4TXUlMkJhYyUzRCZyZXNlcnZlZD0wCgogICAgU3VibWlzc2lvbnMgd2ls
bCBiZSByZXZpZXdlZCBieSB0aGUgcHJvZ3JhbSBjb21taXR0ZWUsCiAgICB3aGljaCB3aWxsIHNl
bGVjdCBhIGJhbGFuY2VkIHByb2dyYW0gb2YgaGlnaC1xdWFsaXR5CiAgICBjb250cmlidXRpb25z
LgoKUFJPQ0VFRElOR1MKCiAgICBQcm9jZWVkaW5ncyBvZiB0aGUgd29ya3Nob3Agd2lsbCBiZSBw
dWJsaXNoZWQgYXMgQ0VVUgogICAgV29ya3Nob3AgUHJvY2VlZGluZ3MuCgpSRUdJU1RSQVRJT04K
CiAgICBSZWdpc3RyYXRpb24gaXMgdmlhIEZMb0MgMjAyNjoKICAgIGh0dHBzOi8vZXVyMDEuc2Fm
ZWxpbmtzLnByb3RlY3Rpb24ub3V0bG9vay5jb20vP3VybD1odHRwcyUzQSUyRiUyRnd3dy5mbG9j
MjYub3JnJTJGcmVnaXN0cmF0aW9uJmRhdGE9MDUlN0MwMiU3Q2NsZWFuLWxpc3QlNDBzY2llbmNl
LnJ1Lm5sJTdDOTgyNDlhODdjYjcwNGJjOGE1ZTkwOGRlNzQzOWM4MjglN0MwODQ1NzhkOTQwMGQ0
YTVhYTdjN2U3NmNhNDdhZjQwMCU3QzElN0MwJTdDNjM5MDc1OTg4NjkyMDM3MjEyJTdDVW5rbm93
biU3Q1RXRnBiR1pzYjNkOGV5SkZiWEIwZVUxaGNHa2lPblJ5ZFdVc0lsWWlPaUl3TGpBdU1EQXdN
Q0lzSWxBaU9pSlhhVzR6TWlJc0lrRk9Jam9pVFdGcGJDSXNJbGRVSWpveWZRJTNEJTNEJTdDMCU3
QyU3QyU3QyZzZGF0YT1jaGtBRGpGU3BsSlpjZ2hmWGxrRXVUOVBoaE50TW9ndFFlJTJCcGhzQTRY
clUlM0QmcmVzZXJ2ZWQ9MAoKSU1QT1JUQU5UIERBVEVTCgogICAgICAgIDQgTWF5IDIwMjY6IFN1
Ym1pc3Npb24gZGVhZGxpbmUKICAgICAgIDI1IE1heSAyMDI2OiBBdXRob3Igbm90aWZpY2F0aW9u
CiAgICAgICAgMSBKdW5lIDIwMjY6IEVhcmx5IHJlZ2lzdHJhdGlvbiBmb3IgRkxvQyB3b3Jrc2hv
cHMKICAgIDI0LTI1IEp1bHkgMjAyNjogQ0ktQkQtU09RRSBXb3Jrc2hvcCBAIEZMb0MgMjAyNgoK
T1JHQU5JWkFUSU9OCgogICAgU3RlZmFuIEhldHpsIChUVSBXaWVuKQogICAgSmVhbiBDaHJpc3Rv
cGggSnVuZyAoVFUgRG9ydG11bmQgVW5pdmVyc2l0eSkKICAgIFJlbmF0ZSBBLiBTY2htaWR0IChU
aGUgVW5pdmVyc2l0eSBvZiBNYW5jaGVzdGVyKQogICAgQ2hyaXN0b3BoIFdlcm5oYXJkIChVbml2
ZXJzaXR5IG9mIFBvdHNkYW0pCl9fX19fX19fX19fX19fX19fX19fX19fX19fX19fX19fX19fX19f
X19fX19fX19fCmNsZWFuLWxpc3QgbWFpbGluZyBsaXN0CmNsZWFuLWxpc3RAc2NpZW5jZS5ydS5u
bApodHRwczovL21haWxtYW4uc2NpZW5jZS5ydS5ubC9tYWlsbWFuL2xpc3RpbmZvL2NsZWFuLWxp
c3QK