Experiment 1

These are results of the experiments for WSkS Antiprenexing:

Directory antiprenex-ai/1
File
Timeout 300 s
Benchmarks 62

MONA Sanity check

Scatter Plots

Experiment 2

Directory antiprenex-ai/2
Timeout 300 s
Benchmarks 105
MONA Timeouts 16
MONA Mean 49.7201942
MONA Mean (w/o TO) 0.9331034
MONA Median 0.08

Removed:

removed from processing

method pred why
u1 TRUE subsumed by u2(TRUE) and u4(TRUE)
u3 TRUE subsumed by u2(TRUE) and u4(TRUE)
u4 FALSE subsumed by u2(FALSE)
u3 FALSE subsumed by u1(FALSE)
u4 FALSE subsumed by u4(TRUE)
u2 TRUE same as by u4(TRUE)

Summary

Data

Experiment 3

Directory antiprenex-ai/2
Timeout 300 s
Benchmarks 103
MONA Timeouts 16
MONA Mean 49.7201942
MONA Mean (w/o TO) 0.9331034
MONA Median 0.08

LS0tCnRpdGxlOiAiV1NrUyBBbnRpcHJlbmV4aW5nIEFuYWx5c2lzIgpwYXJhbXM6CiAgZGlyLmFpOiBhbnRpcHJlbmV4LWFpLzEKICAjZGlyLnB1cmU6IGFudGlwcmVuZXgtcHVyZQogIGZpbGUxOiByZXN1bHRzMS5jc3YKICBmaWxlMjogcmVzdWx0czIuY3N2CiAgI3N1ZmZpeDogcHlleC1oYXJkLXByb2QKICAjd2ViOiBodHRwczovL2dpdGh1Yi5jb20vVmVyaUZJVC9yZXRyby90cmVlL21hc3Rlci9lcXVhdGlvbnMvcHlleC1oYXJkLXozLWVudW0vc210LwogICNkaXI6IHN0cjJfMQogICNzdWZmaXg6IHN0cjIKb3V0cHV0OgogIGh0bWxfbm90ZWJvb2s6CiAgICBjb2RlX2ZvbGRpbmc6IGhpZGUKICBwZGZfZG9jdW1lbnQ6IGRlZmF1bHQKICBodG1sX2RvY3VtZW50OgogICAgZGZfcHJpbnQ6IHBhZ2VkCiAgICB0b2M6IHRydWUKICAgIHRvY19mbG9hdDogdHJ1ZQotLS0KCmBgYHtyIGVjaG89RkFMU0V9CiM9PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT0KIyBQUkVBTUJMRQojPT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09CgojIGxvYWQgdGhlIHBsb3R0aW5nIGxpYnJhcnkKc3VwcHJlc3NNZXNzYWdlcyhsaWJyYXJ5KGdncGxvdDIpKQpsaWJyYXJ5KGdyaWRFeHRyYSkKbGlicmFyeSh0aWt6RGV2aWNlKQoKdGhlbWVfc2V0KHRoZW1lX2J3KCkpCgpvcHRpb25zKHNjaXBlbj05OTkpICAjIHR1cm4tb2ZmIHNjaWVudGlmaWMgbm90YXRpb24gbGlrZSAxZSs0OAoKIyBzaXplIG9mIHBvaW50IGZvciBzY2F0dGVycGxvdHMKUE9JTlRfU0laRSA9IDAuNQojUE9JTlRfU0laRSA9IDEKCiMgdGltZW91dApUSU1FT1VUID0gMzAwICMgc2Vjb25kcwpUSU1FT1VUX1ZBTCA9IDEuMDUgKiBUSU1FT1VUCgojIEZVTkNUSU9OUwpyZWFkX2ZpbGUgPC0gZnVuY3Rpb24oZGlyLCBmaWxlKSB7CiAgZmlsZW5hbWUgPSBwYXN0ZTAoIi4vIiwgZGlyLCAiLyIsIGZpbGUpCiAgZGYgPC0gcmVhZC5jc3YyKGZpbGVuYW1lLAogICAgICAgICAgICAgICAgICBoZWFkZXI9VFJVRSwKICAgICAgICAgICAgICAgICAgc2VwPSI7IiwKICAgICAgICAgICAgICAgICAgY29tbWVudC5jaGFyPSIjIiwKICAgICAgICAgICAgICAgICAgc3RyaXAud2hpdGU9VFJVRSwKICAgICAgICAgICAgICAgICAgc3RyaW5nc0FzRmFjdG9ycz1GQUxTRSkKICAKICAjIGNoYW5nZSB0aGUgdHlwZSBvZiBjb2x1bW5zIG90aGVyIHRoYW4gdGhlIG5hbWUKICBmb3IgKGkgaW4gMjo2KSB7CiAgICBzdXBwcmVzc1dhcm5pbmdzKGRmWyxpXSA8LSBhcy5udW1lcmljKGRmWyxpXSkpCiAgfQogIAogICMgZ2V0IHJpZCBvZiBleHRyZW1hbCB2YWx1ZXMKICBkZltpcy5uYShkZildIDwtIFRJTUVPVVRfVkFMCiAgZGZbZGYgPT0gMC4wMF0gPC0gMC4wMQogIAogIHJldHVybihkZikKfQoKcGxvdF9zY2F0dGVyX2xvZyA8LSBmdW5jdGlvbihkZiwgeGxhYiwgeWxhYikgewogIHBzY2F0IDwtIGdncGxvdChkZiwgYWVzX3N0cmluZyh4PXhsYWIsIHk9eWxhYikpICsKICAgIGdlb21fcG9pbnQoc2l6ZT1QT0lOVF9TSVpFKSArCiAgICBnZW9tX2FibGluZShzaXplPTAuMSkgKwogICAgZ2VvbV92bGluZShzaXplPTAuMSwgeGludGVyY2VwdD1USU1FT1VUX1ZBTCwgbGluZXR5cGU9ImRhc2hlZCIpICsKICAgIGdlb21faGxpbmUoc2l6ZT0wLjEsIHlpbnRlcmNlcHQ9VElNRU9VVF9WQUwsIGxpbmV0eXBlPSJkYXNoZWQiKSArCiAgICBzY2FsZV94X2xvZzEwKCkgKwogICAgc2NhbGVfeV9sb2cxMCgpICsKICAgIHRoZW1lKGF4aXMudGV4dC55ID0gZWxlbWVudF90ZXh0KGFuZ2xlID0gOTAsIGhqdXN0ID0gMC41KSkgKwogICAjIGNvb3JkX2ZpeGVkKHhsaW0gPSBjKDAuOSwgVElNRU9VVF9WQUwpLCB5bGltID0gYygwLjksIFRJTUVPVVRfVkFMKSkgKwogICAgY29vcmRfZml4ZWQoeGxpbSA9IGMoMC4wMDksIFRJTUVPVVRfVkFMKSwgeWxpbSA9IGMoMC4wMDksIFRJTUVPVVRfVkFMKSkgKwogICAgbGFicygKICAgICAgI3RpdGxlPSJUaXRsZSIsCiAgICAgICNzdWJ0aXRsZT0iU3VidGl0bGUiLAogICAgICB4PXhsYWIsCiAgICAgIHk9eWxhYikKICByZXR1cm4ocHNjYXQpCn0KCm1ha2VfdGlreiA8LSBmdW5jdGlvbihmaWxlLCBwaWN0dXJlLCB3aWR0aD0yLjUsIGhlaWdodD0yLjUpIHsKICBmb250X3NpemUgPC0gMQogIHRpa3ooZmlsZT1maWxlLCBvbmVmaWxlPVQsIHdpZHRoPXdpZHRoLCBoZWlnaHQ9aGVpZ2h0KQogIHBsb3QocGljdHVyZSkKICBnYXJiYWdlIDwtIGRldi5vZmYoKQp9CmBgYAoKYGBge3IgZWNobz1GQUxTRX0KZGYuYWkxIDwtIHJlYWRfZmlsZShwYXJhbXMkZGlyLmFpLCBwYXJhbXMkZmlsZTEpCmRmLmFpMiA8LSByZWFkX2ZpbGUocGFyYW1zJGRpci5haSwgcGFyYW1zJGZpbGUyKQpkZi5haTEgPC0gZGYuYWkxWywgYygiZm9ybXVsYSIsICJtb25hIiwgIm1vbmEuYW50aXByZW5leCIsICJtb25hLmFudGlwcmVuZXgucHJlZCIpXQpuYW1lcyhkZi5haTEpIDwtIGMoImZvcm11bGEiLCAibW9uYS50MSIsICJhbnRpcHJlbmV4LnQxIiwgImFudGlwcmVuZXgucHJlZC50MSIpCmRmLmFpMiA8LSBkZi5haTJbLCBjKCJmb3JtdWxhIiwgIm1vbmEiLCAibW9uYS5hbnRpcHJlbmV4IiwgIm1vbmEuYW50aXByZW5leC5wcmVkIildCm5hbWVzKGRmLmFpMikgPC0gYygiZm9ybXVsYSIsICJtb25hLnQyIiwgImFudGlwcmVuZXgudDIiLCAiYW50aXByZW5leC5wcmVkLnQyIikKCmRmMSA8LSBtZXJnZShkZi5haTEsIGRmLmFpMikKYGBgCgojIEV4cGVyaW1lbnQgMQoKVGhlc2UgYXJlIHJlc3VsdHMgb2YgdGhlIGV4cGVyaW1lbnRzIGZvciBXU2tTIEFudGlwcmVuZXhpbmc6Cgp8ICAgICAgICAgICAgICAgICAgICAgfCAgICAgICAgICAgICAgICAgICAgIHwKfC0tLS0tLS0tLS0tLS0tLS0tLS0tLXwtLS0tLS0tLS0tLS0tLS0tLS0tLTp8CnwgKipEaXJlY3RvcnkqKiAgICAgICB8IGByIHBhcmFtcyRkaXJgICAgICAgfAp8ICoqRmlsZSoqICAgICAgICAgICAgfCBgciBwYXJhbXMkZmlsZWAgICAgIHwKfCAqKlRpbWVvdXQqKiAgICAgICAgIHwgYHIgVElNRU9VVGAgcyAgICAgICB8CnwgKipCZW5jaG1hcmtzKiogICAgICB8IGByIG5yb3coZGYxKWAgICAgICAgIHwKCmBgYHtyIGVjaG89RkFMU0V9CmRmMQpgYGAKCiMgTU9OQSBTYW5pdHkgY2hlY2sKCmBgYHtyIGVjaG89RkFMU0V9CnBsb3QxIDwtIHBsb3Rfc2NhdHRlcl9sb2coZGYxLCAibW9uYS50MSIsICJtb25hLnQyIikKcGxvdChwbG90MSkKYGBgCgpgYGB7ciBlY2hvPUZBTFNFfQpuYW1lcyhkZjEpW25hbWVzKGRmMSkgPT0gJ21vbmEudDEnXSA8LSAnbW9uYScKd2l0aGluKGRmMSwgcm0oIm1vbmEudDIiKSkKYGBgCgojIFNjYXR0ZXIgUGxvdHMKCmBgYHtyIGVjaG89RkFMU0V9CgpwbG90LmFuZC50aWt6IDwtIGZ1bmN0aW9uKGRmLCB4bGFiLCB5bGFiKSB7CiAgcGljIDwtIHBsb3Rfc2NhdHRlcl9sb2coZGYsIHhsYWIsIHlsYWIpCiAgbWFrZV90aWt6KHBhc3RlMCgiZmlncy8iLCB4bGFiLCAiLXZzLSIsIHlsYWIsICIudGlreiIpLCBwaWMpCiAgcGljCn0KCnBsb3QxIDwtIHBsb3QuYW5kLnRpa3ooZGYxLCAibW9uYSIsICJhbnRpcHJlbmV4LnQxIikKcGxvdDIgPC0gcGxvdC5hbmQudGlreihkZjEsICJtb25hIiwgImFudGlwcmVuZXgucHJlZC50MSIpCnBsb3QzIDwtIHBsb3QuYW5kLnRpa3ooZGYxLCAibW9uYSIsICJhbnRpcHJlbmV4LnQyIikKcGxvdDQgPC0gcGxvdC5hbmQudGlreihkZjEsICJtb25hIiwgImFudGlwcmVuZXgucHJlZC50MiIpCnBsb3Q1IDwtIHBsb3QuYW5kLnRpa3ooZGYxLCAiYW50aXByZW5leC50MSIsICJhbnRpcHJlbmV4LnByZWQudDEiKQpwbG90NiA8LSBwbG90LmFuZC50aWt6KGRmMSwgImFudGlwcmVuZXgudDEiLCAiYW50aXByZW5leC50MiIpCnBsb3Q3IDwtIHBsb3QuYW5kLnRpa3ooZGYxLCAiYW50aXByZW5leC50MSIsICJhbnRpcHJlbmV4LnByZWQudDIiKQpwbG90OCA8LSBwbG90LmFuZC50aWt6KGRmMSwgImFudGlwcmVuZXgucHJlZC50MSIsICJhbnRpcHJlbmV4LnQyIikKcGxvdDkgPC0gcGxvdC5hbmQudGlreihkZjEsICJhbnRpcHJlbmV4LnByZWQudDEiLCAiYW50aXByZW5leC5wcmVkLnQyIikKcGxvdDEwIDwtIHBsb3QuYW5kLnRpa3ooZGYxLCAiYW50aXByZW5leC50MiIsICJhbnRpcHJlbmV4LnByZWQudDIiKQoKZ3JpZC5hcnJhbmdlKHBsb3QxLCBwbG90MiwgbmNvbCA9IDIpCmdyaWQuYXJyYW5nZShwbG90MywgcGxvdDQsIG5jb2wgPSAyKQpncmlkLmFycmFuZ2UocGxvdDUsIHBsb3Q2LCBuY29sID0gMikKZ3JpZC5hcnJhbmdlKHBsb3Q3LCBwbG90OCwgbmNvbCA9IDIpCmdyaWQuYXJyYW5nZShwbG90OSwgcGxvdDEwLCBuY29sID0gMikKYGBgCgojIEV4cGVyaW1lbnQgMgoKCmBgYHtyIGVjaG89RkFMU0V9CgpleHAyZGlyID0gImFudGlwcmVuZXgtYWkvMiIKZGYuYWkxIDwtIHJlYWRfZmlsZShleHAyZGlyLCAicmVzdWx0czEuY3N2IikKZGYuYWkyIDwtIHJlYWRfZmlsZShleHAyZGlyLCAicmVzdWx0czIuY3N2IikKZGYuYWkzIDwtIHJlYWRfZmlsZShleHAyZGlyLCAicmVzdWx0czMuY3N2IikKZGYuYWk0IDwtIHJlYWRfZmlsZShleHAyZGlyLCAicmVzdWx0czQuY3N2IikKCmNvbHMgPSBjKCJmb3JtdWxhIiwgIm1vbmEiLCAibW9uYS5hbnRpcHJlbmV4IiwgIm1vbmEuYW50aXByZW5leC5wcmVkIikgICMgY29sdW1ucyB0byBwaWNrCmRmLmFpMSA8LSBkZi5haTFbLCBjb2xzXQpuYW1lcyhkZi5haTEpIDwtIGMoImZvcm11bGEiLCAibW9uYS51MSIsICJhbnRpcHJlbmV4LnUxIiwgImFudGlwcmVuZXgucHJlZC51MSIpCmRmLmFpMiA8LSBkZi5haTJbLCBjb2xzXQpuYW1lcyhkZi5haTIpIDwtIGMoImZvcm11bGEiLCAibW9uYS51MiIsICJhbnRpcHJlbmV4LnUyIiwgImFudGlwcmVuZXgucHJlZC51MiIpCmRmLmFpMyA8LSBkZi5haTNbLCBjb2xzXQpuYW1lcyhkZi5haTMpIDwtIGMoImZvcm11bGEiLCAibW9uYS51MyIsICJhbnRpcHJlbmV4LnUzIiwgImFudGlwcmVuZXgucHJlZC51MyIpCmRmLmFpNCA8LSBkZi5haTRbLCBjb2xzXQpuYW1lcyhkZi5haTQpIDwtIGMoImZvcm11bGEiLCAibW9uYS51NCIsICJhbnRpcHJlbmV4LnU0IiwgImFudGlwcmVuZXgucHJlZC51NCIpCgpkZjIgPC0gbWVyZ2UoZGYuYWkxLCBkZi5haTIpCmRmMiA8LSBtZXJnZShkZjIsIGRmLmFpMykKZGYyIDwtIG1lcmdlKGRmMiwgZGYuYWk0KQoKbmFtZXMoZGYyKVtuYW1lcyhkZjIpID09ICdtb25hLnUxJ10gPC0gJ21vbmEnCmRmMiA8LSB3aXRoaW4oZGYyLCBybSgibW9uYS51MiIpKQpkZjIgPC0gd2l0aGluKGRmMiwgcm0oIm1vbmEudTMiKSkKZGYyIDwtIHdpdGhpbihkZjIsIHJtKCJtb25hLnU0IikpCmBgYAoKYGBge3IgZWNobz1GQUxTRX0KbWV0aG9kID0gYygidTEiLCAidTIiLCAidTMiLCAidTQiKQpyZXN1bHRzIDwtIGRhdGEuZnJhbWUobWV0aG9kLCBtZXRob2QsIHJvdy5uYW1lcz0ibWV0aG9kIikKbmFtZXMocmVzdWx0cykgPC0gYygibWV0aG9kIikKcmVzdWx0c1sidTEiLCAiZGlzdHIudGhyZXMiXSA8LSAxMDAwMDAwMDAwCnJlc3VsdHNbInUyIiwgImRpc3RyLnRocmVzIl0gPC0gMTAwMDAwMDAwMApyZXN1bHRzWyJ1MyIsICJkaXN0ci50aHJlcyJdIDwtIDEwMDAwCnJlc3VsdHNbInU0IiwgImRpc3RyLnRocmVzIl0gPC0gMTAwMDAKCnJlc3VsdHNbInUxIiwgImFudGlwLnRocmVzIl0gPC0gMjAwMApyZXN1bHRzWyJ1MiIsICJhbnRpcC50aHJlcyJdIDwtIDEwMDAwCnJlc3VsdHNbInUzIiwgImFudGlwLnRocmVzIl0gPC0gMjAwMApyZXN1bHRzWyJ1NCIsICJhbnRpcC50aHJlcyJdIDwtIDEwMDAwCgp0bXBfY29sIDwtIGMoVFJVRSwgRkFMU0UpCnRtcCA8LSBkYXRhLmZyYW1lKHRtcF9jb2wpCm5hbWVzKHRtcCkgPC0gYygicHJlZCIpCnJlc3VsdHMgPC0gbWVyZ2UocmVzdWx0cywgdG1wKQoKY29tcHV0ZV90aW1lb3V0cyA8LSBmdW5jdGlvbihkZiwgY29sKSB7CiAgdG1wIDwtIGRmW2RmWywgY29sXSA9PSBUSU1FT1VUX1ZBTCxdCiAgdG1wCn0KCm1vbmEudGltZW91dHMgPC0gbnJvdyhjb21wdXRlX3RpbWVvdXRzKGRmMiwgIm1vbmEiKSkKbW9uYS5uby50byA8LSBkZjJbZGYyWywgIm1vbmEiXSAhPSBUSU1FT1VUX1ZBTCxdCm1vbmEubWVhbiA8LSBtZWFuKGRmMlssICJtb25hIl0pCm1vbmEubWVhbi5uby50byA8LSBtZWFuKG1vbmEubm8udG9bLCAibW9uYSJdKQptb25hLm1lZGlhbiA8LSBtZWRpYW4oZGYyWywgIm1vbmEiXSkKCnBhcmFtcy5mb3IubWV0aG9kIDwtIGZ1bmN0aW9uKHJlc19kZiwgZGF0YV9kZiwgcHJlZCwgbWV0aG9kKSB7CiAgaW5maXggPC0gaWYgKHByZWQpICJwcmVkLiIgZWxzZSAiIgogIHNyY19jb2wgPC0gcGFzdGUwKCJhbnRpcHJlbmV4LiIsIGluZml4LCBtZXRob2QpCiAgCiAgcmVzX2RmW3Jlc19kZiRtZXRob2QgPT0gbWV0aG9kICYgcmVzX2RmJHByZWQgPT0gcHJlZCwgInRpbWVvdXRzIl0gPC0gbnJvdyhjb21wdXRlX3RpbWVvdXRzKGRhdGFfZGYsIHNyY19jb2wpKQogIHJlc19kZltyZXNfZGYkbWV0aG9kID09IG1ldGhvZCAmIHJlc19kZiRwcmVkID09IHByZWQsICJtZWFuIl0gPC0gbWVhbihkYXRhX2RmWywgc3JjX2NvbF0pCiAgZGF0YV9ub190byA8LSBkYXRhX2RmW2RhdGFfZGZbLCBzcmNfY29sXSAhPSBUSU1FT1VUX1ZBTCxdCiAgcmVzX2RmW3Jlc19kZiRtZXRob2QgPT0gbWV0aG9kICYgcmVzX2RmJHByZWQgPT0gcHJlZCwgIm1lYW4tbm8tdG8iXSA8LSBtZWFuKGRhdGFfbm9fdG9bLCBzcmNfY29sXSkKICAKICByZXNfZGZbcmVzX2RmJG1ldGhvZCA9PSBtZXRob2QgJiByZXNfZGYkcHJlZCA9PSBwcmVkLCAibWVkaWFuIl0gPC0gbWVkaWFuKGRhdGFfZGZbLCBzcmNfY29sXSkKCiAgcmVzX2RmCn0KCnBhcmFtcy5mb3IuYWxsLm1ldGhvZHMgPC0gZnVuY3Rpb24ocmVzX2RmLCBkYXRhX2RmLCBtZXRob2QpIHsKICByZXNfZGYgPC0gcGFyYW1zLmZvci5tZXRob2QocmVzX2RmLCBkYXRhX2RmLCBGQUxTRSwgbWV0aG9kKQogIHJlc19kZiA8LSBwYXJhbXMuZm9yLm1ldGhvZChyZXNfZGYsIGRhdGFfZGYsIFRSVUUsIG1ldGhvZCkKICByZXNfZGYKfQoKcmVzdWx0cyA8LSBwYXJhbXMuZm9yLmFsbC5tZXRob2RzKHJlc3VsdHMsIGRmMiwgInUxIikKcmVzdWx0cyA8LSBwYXJhbXMuZm9yLmFsbC5tZXRob2RzKHJlc3VsdHMsIGRmMiwgInUyIikKcmVzdWx0cyA8LSBwYXJhbXMuZm9yLmFsbC5tZXRob2RzKHJlc3VsdHMsIGRmMiwgInUzIikKcmVzdWx0cyA8LSBwYXJhbXMuZm9yLmFsbC5tZXRob2RzKHJlc3VsdHMsIGRmMiwgInU0IikKCgojcmVzdWx0c1tyZXN1bHRzJG1ldGhvZCA9PSAidTEiICYgcmVzdWx0cyRwcmVkID09IEZBTFNFLCAidGltZW91dHMiXSA8LSBucm93KGNvbXB1dGVfdGltZW91dHMoZGYyLCAiYW50aXByZW5leC51MSIpKQojcmVzdWx0c1tyZXN1bHRzJG1ldGhvZCA9PSAidTEiICYgcmVzdWx0cyRwcmVkID09IFRSVUUsICJ0aW1lb3V0cyJdIDwtIG5yb3coY29tcHV0ZV90aW1lb3V0cyhkZjIsICJhbnRpcHJlbmV4LnByZWQudTEiKSkKCiNyZXN1bHRzIDwtIGRhdGEuZnJhbWUocmVzdWx0cywgdG1wKQpgYGAKCnwgICAgICAgICAgICAgICAgICAgICB8ICAgICAgICAgICAgICAgICAgICAgfAp8LS0tLS0tLS0tLS0tLS0tLS0tLS0tfC0tLS0tLS0tLS0tLS0tLS0tLS0tOnwKfCAqKkRpcmVjdG9yeSoqICAgICAgIHwgYW50aXByZW5leC1haS8yICAgICB8CnwgKipUaW1lb3V0KiogICAgICAgICB8IGByIFRJTUVPVVRgIHMgICAgICAgfAp8ICoqQmVuY2htYXJrcyoqICAgICAgfCBgciBucm93KGRmMilgICAgICAgIHwKfCAqKk1PTkEgVGltZW91dHMqKiAgIHwgYHIgbW9uYS50aW1lb3V0c2AgICB8CnwgKipNT05BIE1lYW4qKiAgICAgICB8IGByIG1vbmEubWVhbmAgICAgICAgfAp8ICoqTU9OQSBNZWFuICh3L28gVE8pKiogICB8IGByIG1vbmEubWVhbi5uby50b2AgICAgICAgfAp8ICoqTU9OQSBNZWRpYW4qKiAgICAgfCBgciBtb25hLm1lZGlhbmAgICB8CgojIyBSZW1vdmVkOgoKcmVtb3ZlZCBmcm9tIHByb2Nlc3NpbmcKCnwgbWV0aG9kIHwgcHJlZCB8IHdoeSAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICB8CnwtLS0tLS0tLXwtLS0tLS18LS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS18CnwgdTEgICAgIHwgVFJVRSB8IHN1YnN1bWVkIGJ5IHUyKFRSVUUpIGFuZCB1NChUUlVFKSB8CnwgdTMgICAgIHwgVFJVRSB8IHN1YnN1bWVkIGJ5IHUyKFRSVUUpIGFuZCB1NChUUlVFKSB8CnwgdTQgICAgIHwgRkFMU0UgfCBzdWJzdW1lZCBieSB1MihGQUxTRSkgICAgICAgICAgICB8CnwgdTMgICAgIHwgRkFMU0UgfCBzdWJzdW1lZCBieSB1MShGQUxTRSkgICAgICAgICAgICB8CnwgdTQgICAgIHwgRkFMU0UgfCBzdWJzdW1lZCBieSB1NChUUlVFKSAgICAgICAgICAgICB8CnwgdTIgICAgIHwgVFJVRSB8IHNhbWUgYXMgYnkgdTQoVFJVRSkgICAgICAgICAgICAgICB8CgojIyBTdW1tYXJ5CgpgYGB7ciBlY2hvPUZBTFNFfQpyZXN1bHRzCmBgYAoKIyMgRGF0YQoKYGBge3IgZWNobz1GQUxTRX0KZGYyCmBgYAoKYGBge3IgZWNobz1GQUxTRX0KCiMgYW50aXByZW5leC5wcmVkLnUzIGlzIHN1YnN1bWVkIGJ5IGFudGlwcmVuZXgucHJlZC51NCBhbmQgYW50aXByZW5leC5wcmVkLnUyCiMgYW50aXByZW5leC5wcmVkLnUxIGlzIHN1YnN1bWVkIGJ5IGFudGlwcmVuZXgucHJlZC51NCBhbmQgYW50aXByZW5leC5wcmVkLnUyCiMgYW50aXByZW5leC51NCBpcyBzdWJzdW1lZCBieSBhbnRpcHJlbmV4LnUyCiMgYW50aXByZW5leC51MyBpcyBzdWJzdW1lZCBieSBhbnRpcHJlbmV4LnUxCiMgYW50aXByZW5leC51NCBpcyBzdWJzdW1lZCBieSBhbnRpcHJlbmV4LnByZWQudTQKIyBhbnRpcHJlbmV4LnByZWQudTQgaXMgdGhlIHNhbWUgYXMgYW50aXByZW5leC5wcmVkLnUyLCBrZWVwaW5nIG9ubHkgYW50aXByZW5leC5wcmVkLnU0IAoKCgpwbG90MSA8LSBwbG90LmFuZC50aWt6KGRmMiwgIm1vbmEiLCAiYW50aXByZW5leC51MSIpCnBsb3QyIDwtIHBsb3QuYW5kLnRpa3ooZGYyLCAibW9uYSIsICJhbnRpcHJlbmV4LnUyIikKI3Bsb3QzIDwtIHBsb3QuYW5kLnRpa3ooZGYyLCAibW9uYSIsICJhbnRpcHJlbmV4LnUzIikKI3Bsb3Q0IDwtIHBsb3QuYW5kLnRpa3ooZGYyLCAibW9uYSIsICJhbnRpcHJlbmV4LnU0IikKI3Bsb3Q1IDwtIHBsb3QuYW5kLnRpa3ooZGYyLCAibW9uYSIsICJhbnRpcHJlbmV4LnByZWQudTEiKQojcGxvdDYgPC0gcGxvdC5hbmQudGlreihkZjIsICJtb25hIiwgImFudGlwcmVuZXgucHJlZC51MiIpCiNwbG90NyA8LSBwbG90LmFuZC50aWt6KGRmMiwgIm1vbmEiLCAiYW50aXByZW5leC5wcmVkLnUzIikKcGxvdDggPC0gcGxvdC5hbmQudGlreihkZjIsICJtb25hIiwgImFudGlwcmVuZXgucHJlZC51NCIpCgpwbG90OSA8LSBwbG90LmFuZC50aWt6KGRmMiwgImFudGlwcmVuZXgudTEiLCAiYW50aXByZW5leC5wcmVkLnU0IikKcGxvdDEwIDwtIHBsb3QuYW5kLnRpa3ooZGYyLCAiYW50aXByZW5leC51MiIsICJhbnRpcHJlbmV4LnByZWQudTQiKQojcGxvdDExIDwtIHBsb3QuYW5kLnRpa3ooZGYyLCAiYW50aXByZW5leC51MyIsICJhbnRpcHJlbmV4LnByZWQudTMiKQojcGxvdDEyIDwtIHBsb3QuYW5kLnRpa3ooZGYyLCAiYW50aXByZW5leC51NCIsICJhbnRpcHJlbmV4LnByZWQudTQiKQoKcGxvdDEzIDwtIHBsb3QuYW5kLnRpa3ooZGYyLCAiYW50aXByZW5leC51MSIsICJhbnRpcHJlbmV4LnUyIikKI3Bsb3QxNCA8LSBwbG90LmFuZC50aWt6KGRmMiwgImFudGlwcmVuZXgudTEiLCAiYW50aXByZW5leC51MyIpCiNwbG90MTUgPC0gcGxvdC5hbmQudGlreihkZjIsICJhbnRpcHJlbmV4LnUxIiwgImFudGlwcmVuZXgudTQiKQojcGxvdDE2IDwtIHBsb3QuYW5kLnRpa3ooZGYyLCAiYW50aXByZW5leC51MiIsICJhbnRpcHJlbmV4LnUzIikKI3Bsb3QxNyA8LSBwbG90LmFuZC50aWt6KGRmMiwgImFudGlwcmVuZXgudTIiLCAiYW50aXByZW5leC51NCIpCiNwbG90MTggPC0gcGxvdC5hbmQudGlreihkZjIsICJhbnRpcHJlbmV4LnUzIiwgImFudGlwcmVuZXgudTQiKQoKI3Bsb3QxOSA8LSBwbG90LmFuZC50aWt6KGRmMiwgImFudGlwcmVuZXgucHJlZC51MSIsICJhbnRpcHJlbmV4LnByZWQudTIiKQojcGxvdDIwIDwtIHBsb3QuYW5kLnRpa3ooZGYyLCAiYW50aXByZW5leC5wcmVkLnUxIiwgImFudGlwcmVuZXgucHJlZC51MyIpCiNwbG90MjEgPC0gcGxvdC5hbmQudGlreihkZjIsICJhbnRpcHJlbmV4LnByZWQudTEiLCAiYW50aXByZW5leC5wcmVkLnU0IikKI3Bsb3QyMiA8LSBwbG90LmFuZC50aWt6KGRmMiwgImFudGlwcmVuZXgucHJlZC51MiIsICJhbnRpcHJlbmV4LnByZWQudTMiKQojcGxvdDIzIDwtIHBsb3QuYW5kLnRpa3ooZGYyLCAiYW50aXByZW5leC5wcmVkLnUyIiwgImFudGlwcmVuZXgucHJlZC51NCIpCiNwbG90MjQgPC0gcGxvdC5hbmQudGlreihkZjIsICJhbnRpcHJlbmV4LnByZWQudTMiLCAiYW50aXByZW5leC5wcmVkLnU0IikKCmdyaWQuYXJyYW5nZShwbG90MSwgcGxvdDIsIG5jb2wgPSAyKQojZ3JpZC5hcnJhbmdlKHBsb3QzLCBwbG90NCwgbmNvbCA9IDIpCmdyaWQuYXJyYW5nZShwbG90OCwgcGxvdDksIG5jb2wgPSAyKQpncmlkLmFycmFuZ2UocGxvdDEwLCBwbG90MTMsIG5jb2wgPSAyKQpgYGAKCmBgYHtyIGVjaG89RkFMU0V9CmFkZF9yb3cgPC0gZnVuY3Rpb24od2hlcmUsIGZyb20sIG1ldGhvZCkgewogIHdoZXJlW25yb3cod2hlcmUpICsgMSxdIDwtIGZyb21bZnJvbSRmb3JtdWxhID09IG1ldGhvZCxdCiAgcmV0dXJuKHdoZXJlKQp9CgppbnRlcmVzdGluZyA8LSBkYXRhLmZyYW1lKGRmMltkZjIkZm9ybXVsYSA9PSAiZm91ci13ZWlnaHRzLm1vbmEiLF0pCmludGVyZXN0aW5nIDwtIGFkZF9yb3coaW50ZXJlc3RpbmcsIGRmMiwgInNtb290aGluZy5tb25hIikKaW50ZXJlc3RpbmcgPC0gYWRkX3JvdyhpbnRlcmVzdGluZywgZGYyLCAidHJlZS13ZWlnaHRzLW1pbmltaXNhdGlvbi5tb25hIikKaW50ZXJlc3RpbmcgPC0gYWRkX3JvdyhpbnRlcmVzdGluZywgZGYyLCAid3Mxcy12b24tbmV1bWFubi1hZGRlci5tb25hIikKaW50ZXJlc3RpbmcgPC0gYWRkX3JvdyhpbnRlcmVzdGluZywgZGYyLCAic2wubW9uYSIpCmludGVyZXN0aW5nIDwtIGFkZF9yb3coaW50ZXJlc3RpbmcsIGRmMiwgImxpZnRfOC5sdGwwLm1vbmEiKQppbnRlcmVzdGluZyA8LSBhZGRfcm93KGludGVyZXN0aW5nLCBkZjIsICJsaWZ0X2JfNy5sdGwwLm1vbmEiKQppbnRlcmVzdGluZyA8LSBhZGRfcm93KGludGVyZXN0aW5nLCBkZjIsICJob3JuX3N1YjE3Lm1vbmEiKQppbnRlcmVzdGluZyA8LSBhZGRfcm93KGludGVyZXN0aW5nLCBkZjIsICJob3JuX3N1YjE4Lm1vbmEiKQppbnRlcmVzdGluZyA8LSBhZGRfcm93KGludGVyZXN0aW5nLCBkZjIsICJob3JuX3N1YjE5Lm1vbmEiKQoKaW50ZXJlc3RpbmcgPC0gaW50ZXJlc3RpbmdbLCBjKCJmb3JtdWxhIiwgIm1vbmEiLCAiYW50aXByZW5leC51MiIsICJhbnRpcHJlbmV4LnByZWQudTQiKV0KCmludGVyZXN0aW5nCmBgYAoKCiMgRXhwZXJpbWVudCAzCgoKYGBge3IgZWNobz1GQUxTRX0KCmV4cDJkaXIgPSAiYW50aXByZW5leC1haS8zIgpkZi5haS56NSA8LSByZWFkX2ZpbGUoZXhwMmRpciwgInJlc3VsdHM1LmNzdiIpCmRmLmFpLno2IDwtIHJlYWRfZmlsZShleHAyZGlyLCAicmVzdWx0czYuY3N2IikKZGYuYWkuejcgPC0gcmVhZF9maWxlKGV4cDJkaXIsICJyZXN1bHRzNy5jc3YiKQoKY29scyA9IGMoImZvcm11bGEiLCAibW9uYSIsICJtb25hLmFudGlwcmVuZXgiLCAibW9uYS5hbnRpcHJlbmV4LnByZWQiKSAgIyBjb2x1bW5zIHRvIHBpY2sKZGYuYWkuejUgPC0gZGYuYWkuejVbLCBjb2xzXQpuYW1lcyhkZi5haS56NSkgPC0gYygiZm9ybXVsYSIsICJtb25hLno1IiwgImFudGlwcmVuZXguejUiLCAiYW50aXByZW5leC5wcmVkLno1IikKZGYuYWkuejYgPC0gZGYuYWkuejZbLCBjb2xzXQpuYW1lcyhkZi5haS56NikgPC0gYygiZm9ybXVsYSIsICJtb25hLno2IiwgImFudGlwcmVuZXguejYiLCAiYW50aXByZW5leC5wcmVkLno2IikKZGYuYWkuejcgPC0gZGYuYWkuejdbLCBjb2xzXQpuYW1lcyhkZi5haS56NykgPC0gYygiZm9ybXVsYSIsICJtb25hLno3IiwgImFudGlwcmVuZXguejciLCAiYW50aXByZW5leC5wcmVkLno3IikKCmRmMyA8LSBkZi5haS56NQpkZjMgPC0gbWVyZ2UoZGYzLCBkZi5haS56NikKZGYzIDwtIG1lcmdlKGRmMywgZGYuYWkuejcpCgpuYW1lcyhkZjMpW25hbWVzKGRmMykgPT0gJ21vbmEuejUnXSA8LSAnbW9uYScKZGYzIDwtIHdpdGhpbihkZjMsIHJtKCJtb25hLno2IikpCmRmMyA8LSB3aXRoaW4oZGYzLCBybSgibW9uYS56NyIpKQojZGYyIDwtIHdpdGhpbihkZjIsIHJtKCJtb25hLnUzIikpCiNkZjIgPC0gd2l0aGluKGRmMiwgcm0oIm1vbmEudTQiKSkKCiMgcmVtb3ZlIHRob3NlIHdoZXJlIGV2ZXJ5b25lIGRpZXMKZGYzIDwtIGRmM1tkZjMkZm9ybXVsYSAhPSAibGlmdF9iXzgubHRsMC5tb25hIiwgXQpkZjMgPC0gZGYzW2RmMyRmb3JtdWxhICE9ICJsaWZ0X2JfOS5sdGwwLm1vbmEiLCBdCgptb25hLnRpbWVvdXRzIDwtIG5yb3coY29tcHV0ZV90aW1lb3V0cyhkZjMsICJtb25hIikpCm1vbmEubm8udG8gPC0gZGYzW2RmM1ssICJtb25hIl0gIT0gVElNRU9VVF9WQUwsXQptb25hLm1lYW4gPC0gbWVhbihkZjNbLCAibW9uYSJdKQptb25hLm1lYW4ubm8udG8gPC0gbWVhbihtb25hLm5vLnRvWywgIm1vbmEiXSkKbW9uYS5tZWRpYW4gPC0gbWVkaWFuKGRmM1ssICJtb25hIl0pCgpgYGAKCnwgICAgICAgICAgICAgICAgICAgICB8ICAgICAgICAgICAgICAgICAgICAgfAp8LS0tLS0tLS0tLS0tLS0tLS0tLS0tfC0tLS0tLS0tLS0tLS0tLS0tLS0tOnwKfCAqKkRpcmVjdG9yeSoqICAgICAgIHwgYW50aXByZW5leC1haS8yICAgICB8CnwgKipUaW1lb3V0KiogICAgICAgICB8IGByIFRJTUVPVVRgIHMgICAgICAgfAp8ICoqQmVuY2htYXJrcyoqICAgICAgfCBgciBucm93KGRmMylgICAgICAgIHwKfCAqKk1PTkEgVGltZW91dHMqKiAgIHwgYHIgbW9uYS50aW1lb3V0c2AgICB8CnwgKipNT05BIE1lYW4qKiAgICAgICB8IGByIG1vbmEubWVhbmAgICAgICAgfAp8ICoqTU9OQSBNZWFuICh3L28gVE8pKiogICB8IGByIG1vbmEubWVhbi5uby50b2AgICAgICAgfAp8ICoqTU9OQSBNZWRpYW4qKiAgICAgfCBgciBtb25hLm1lZGlhbmAgICB8CgpgYGB7ciBlY2hvPUZBTFNFfQpkZjMKYGBgCgpgYGB7ciBlY2hvPUZBTFNFfQpwbG90MSA8LSBwbG90LmFuZC50aWt6KGRmMywgIm1vbmEiLCAiYW50aXByZW5leC56NSIpCnBsb3QyIDwtIHBsb3QuYW5kLnRpa3ooZGYzLCAibW9uYSIsICJhbnRpcHJlbmV4Lno2IikKcGxvdDMgPC0gcGxvdC5hbmQudGlreihkZjMsICJtb25hIiwgImFudGlwcmVuZXguejciKQojcGxvdDQgPC0gcGxvdC5hbmQudGlreihkZjMsICJtb25hIiwgImFudGlwcmVuZXgucHJlZC56NSIpCnBsb3Q1IDwtIHBsb3QuYW5kLnRpa3ooZGYzLCAibW9uYSIsICJhbnRpcHJlbmV4LnByZWQuejYiKQojcGxvdDYgPC0gcGxvdC5hbmQudGlreihkZjMsICJtb25hIiwgImFudGlwcmVuZXgucHJlZC56NyIpCgpwbG90NyA8LSBwbG90LmFuZC50aWt6KGRmMywgImFudGlwcmVuZXguejUiLCAiYW50aXByZW5leC5wcmVkLno2IikKcGxvdDggPC0gcGxvdC5hbmQudGlreihkZjMsICJhbnRpcHJlbmV4Lno2IiwgImFudGlwcmVuZXgucHJlZC56NiIpCnBsb3Q5IDwtIHBsb3QuYW5kLnRpa3ooZGYzLCAiYW50aXByZW5leC56NyIsICJhbnRpcHJlbmV4LnByZWQuejYiKQoKcGxvdDEwIDwtIHBsb3QuYW5kLnRpa3ooZGYzLCAiYW50aXByZW5leC56NSIsICJhbnRpcHJlbmV4Lno2IikKcGxvdDExIDwtIHBsb3QuYW5kLnRpa3ooZGYzLCAiYW50aXByZW5leC56NSIsICJhbnRpcHJlbmV4Lno3IikKcGxvdDEyIDwtIHBsb3QuYW5kLnRpa3ooZGYzLCAiYW50aXByZW5leC56NiIsICJhbnRpcHJlbmV4Lno3IikKCiNwbG90MTMgPC0gcGxvdC5hbmQudGlreihkZjMsICJhbnRpcHJlbmV4LnByZWQuejUiLCAiYW50aXByZW5leC5wcmVkLno2IikKI3Bsb3QxNCA8LSBwbG90LmFuZC50aWt6KGRmMywgImFudGlwcmVuZXgucHJlZC56NSIsICJhbnRpcHJlbmV4LnByZWQuejciKQojcGxvdDE1IDwtIHBsb3QuYW5kLnRpa3ooZGYzLCAiYW50aXByZW5leC5wcmVkLno2IiwgImFudGlwcmVuZXgucHJlZC56NyIpCiNwbG90MjIgPC0gcGxvdC5hbmQudGlreihkZjIsICJhbnRpcHJlbmV4LnByZWQudTIiLCAiYW50aXByZW5leC5wcmVkLnUzIikKI3Bsb3QyMyA8LSBwbG90LmFuZC50aWt6KGRmMiwgImFudGlwcmVuZXgucHJlZC51MiIsICJhbnRpcHJlbmV4LnByZWQudTQiKQojcGxvdDI0IDwtIHBsb3QuYW5kLnRpa3ooZGYyLCAiYW50aXByZW5leC5wcmVkLnUzIiwgImFudGlwcmVuZXgucHJlZC51NCIpCgpncmlkLmFycmFuZ2UocGxvdDEsIHBsb3QyLCBuY29sID0gMikKZ3JpZC5hcnJhbmdlKHBsb3QzLCBwbG90NSwgbmNvbCA9IDIpCiNncmlkLmFycmFuZ2UocGxvdDUsIHBsb3Q2LCBuY29sID0gMikKZ3JpZC5hcnJhbmdlKHBsb3Q3LCBwbG90OCwgbmNvbCA9IDIpCmdyaWQuYXJyYW5nZShwbG90OSwgcGxvdDEwLCBuY29sID0gMikKZ3JpZC5hcnJhbmdlKHBsb3QxMSwgcGxvdDEyLCBuY29sID0gMikKI2dyaWQuYXJyYW5nZShwbG90MTMsIHBsb3QxNCwgbmNvbCA9IDIpCiNncmlkLmFycmFuZ2UocGxvdDE1LCBwbG90MTUsIG5jb2wgPSAyKQpgYGAKCmBgYHtyIGVjaG89RkFMU0V9CgppbnRlcmVzdGluZyA8LSBkYXRhLmZyYW1lKGRmM1tkZjMkZm9ybXVsYSA9PSAiZm91ci13ZWlnaHRzLm1vbmEiLF0pCmludGVyZXN0aW5nIDwtIGFkZF9yb3coaW50ZXJlc3RpbmcsIGRmMywgInNtb290aGluZy5tb25hIikKaW50ZXJlc3RpbmcgPC0gYWRkX3JvdyhpbnRlcmVzdGluZywgZGYzLCAidHJlZS13ZWlnaHRzLW1pbmltaXNhdGlvbi5tb25hIikKaW50ZXJlc3RpbmcgPC0gYWRkX3JvdyhpbnRlcmVzdGluZywgZGYzLCAid3Mxcy12b24tbmV1bWFubi1hZGRlci5tb25hIikKaW50ZXJlc3RpbmcgPC0gYWRkX3JvdyhpbnRlcmVzdGluZywgZGYzLCAic2wubW9uYSIpCmludGVyZXN0aW5nIDwtIGFkZF9yb3coaW50ZXJlc3RpbmcsIGRmMywgImxpZnRfOC5sdGwwLm1vbmEiKQppbnRlcmVzdGluZyA8LSBhZGRfcm93KGludGVyZXN0aW5nLCBkZjMsICJsaWZ0X2JfNy5sdGwwLm1vbmEiKQppbnRlcmVzdGluZyA8LSBhZGRfcm93KGludGVyZXN0aW5nLCBkZjMsICJob3JuX3N1YjE3Lm1vbmEiKQppbnRlcmVzdGluZyA8LSBhZGRfcm93KGludGVyZXN0aW5nLCBkZjMsICJob3JuX3N1YjE4Lm1vbmEiKQppbnRlcmVzdGluZyA8LSBhZGRfcm93KGludGVyZXN0aW5nLCBkZjMsICJob3JuX3N1YjE5Lm1vbmEiKQoKCgoKI2ludGVyZXN0aW5nIDwtIGRmM1tkZjMkZm9ybXVsYSA9PSAiZm91ci13ZWlnaHRzLm1vbmEiLF0KI2ludGVyZXN0aW5nW25yb3coaW50ZXJlc3RpbmcpICsgMSxdIDwtIGRmM1tkZjMkZm9ybXVsYSA9PSAic21vb3RoaW5nLm1vbmEiLF0KI2ludGVyZXN0aW5nW25yb3coaW50ZXJlc3RpbmcpICsgMSxdIDwtIGRmM1tkZjMkZm9ybXVsYSA9PSAidHJlZS13ZWlnaHRzLW1pbmltaXNhdGlvbi5tb25hIixdCiNpbnRlcmVzdGluZ1tucm93KGludGVyZXN0aW5nKSArIDEsXSA8LSBkZjNbZGYzJGZvcm11bGEgPT0gIndzMXMtdm9uLW5ldW1hbm4tYWRkZXIubW9uYSIsXQojaW50ZXJlc3RpbmdbbnJvdyhpbnRlcmVzdGluZykgKyAxLF0gPC0gZGYzW2RmMyRmb3JtdWxhID09ICJzbC5tb25hIixdCiNpbnRlcmVzdGluZ1tucm93KGludGVyZXN0aW5nKSArIDEsXSA8LSBkZjNbZGYzJGZvcm11bGEgPT0gInNsLm1vbmEiLF0KCgoKIyByZW1vdmUgdW51c2VkIGNvbHVtbnMKaW50ZXJlc3RpbmcgPC0gaW50ZXJlc3RpbmdbLCBjKCJmb3JtdWxhIiwgIm1vbmEiLCAiYW50aXByZW5leC56NiIsICJhbnRpcHJlbmV4LnByZWQuejYiLCAiYW50aXByZW5leC5wcmVkLno3IildCgppbnRlcmVzdGluZwpgYGA=