Some playing with analysing what happens during antiprenexing.

Parameter Value
Name of benchmark set inf-distr.csv
Size of benchmark set 81
Timeout 30

LS0tCnRpdGxlOiAiV1NrUyBBbnRpcHJlbmV4aW5nIEFuYWx5c2lzIgpwYXJhbXM6CiAgZGlyOiAiLiIKICBmaWxlOiBpbmYtZGlzdHIuY3N2Cm91dHB1dDoKICBodG1sX25vdGVib29rOgogICAgY29kZV9mb2xkaW5nOiBoaWRlCiAgcGRmX2RvY3VtZW50OiBkZWZhdWx0CiAgaHRtbF9kb2N1bWVudDoKICAgIGRmX3ByaW50OiBwYWdlZAogICAgdG9jOiB0cnVlCiAgICB0b2NfZmxvYXQ6IHRydWUgCi0tLQoKU29tZSBwbGF5aW5nIHdpdGggYW5hbHlzaW5nIHdoYXQgaGFwcGVucyBkdXJpbmcgYW50aXByZW5leGluZy4KCmBgYHtyIGVjaG89RkFMU0V9CiMgU0VUVElOR1MKCiMgbG9hZCB0aGUgcGxvdHRpbmcgbGlicmFyeQpzdXBwcmVzc01lc3NhZ2VzKGxpYnJhcnkoZ2dwbG90MikpCmxpYnJhcnkoZ3JpZCkKbGlicmFyeShncmlkRXh0cmEpCmxpYnJhcnkodGlrekRldmljZSkKCnRoZW1lX3NldCh0aGVtZV9idygpKQoKb3B0aW9ucyhzY2lwZW49OTk5KSAgIyB0dXJuLW9mZiBzY2llbnRpZmljIG5vdGF0aW9uIGxpa2UgMWUrNDgKCiMgc2l6ZSBvZiBwb2ludCBmb3Igc2NhdHRlcnBsb3RzClBPSU5UX1NJWkU9MC41CgojIHRoZSB0aW1lb3V0ClRJTUVPVVQ9MzAKCiNGSUxFUz1jKCdnb2FsJywgJ2RpcicsICdkZWwnLCAnY29tYicsICdkaXItcXVvdCcsICdkZWwtcXVvdCcsICdjb21iLXF1b3QnLCAnZ29hbC1xdW90JykKCiMgQVVYSUxJQVJZIEZVTkNUSU9OUwpyZWFkX2ZpbGUgPSBmdW5jdGlvbihmKSB7CiAgI3ByaW50KHBhc3RlMCgncHJvY2Vzc2luZyAnLCBmLCAnIC4uLicpKQogIHBhdGggPSBwYXN0ZTAocGFyYW1zJGRpciwgJy8nLCBmKSMsICcuY3N2JykKICByZWFkLmNzdihwYXRoLCBoZWFkZXI9VFJVRSwgc2VwPSI7IiwgY29tbWVudC5jaGFyPScjJywgbmEuc3RyaW5ncz0nVE8nLCBzdHJpbmdzQXNGYWN0b3JzPUZBTFNFKQp9CgojIE1ha2VzIGEgc2NhdHRlcnBsb3QKc2NhdCA9IGZ1bmN0aW9uKGRmLCB4X2F4aXMsIHlfYXhpcykgewpnZ3Bsb3QoZGYsIGFlc19zdHJpbmcoeD14X2F4aXMsIHk9eV9heGlzKSkgKwogIGdlb21fcG9pbnQoc2l6ZT1QT0lOVF9TSVpFKSArCiAgZ2VvbV9hYmxpbmUoc2l6ZT0wLjEpICsKIyAgc2NhbGVfeF9sb2cxMCgpICsKIyAgc2NhbGVfeV9sb2cxMCgpICsKICB0aGVtZShheGlzLnRleHQueSA9IGVsZW1lbnRfdGV4dChhbmdsZSA9IDkwLCBoanVzdCA9IDAuNSkpICsKICBjb29yZF9maXhlZCh4bGltID0gYygwLCAxLjA1ICogVElNRU9VVCksIHlsaW0gPSBjKDAsIDEuMDUqVElNRU9VVCkpICsKICBsYWJzKAojICAgIHRpdGxlPSJUaW1lIiwKIyAgICBzdWJ0aXRsZT0iT3VyIHZzIFVuZm9sZGluZyAodG8gREZBKSIsCiAgICB4PXhfYXhpcywKICAgIHk9eV9heGlzKQp9CgojIE1ha2VzIGEgaGlzdG9ncmFtCmhpc3RvMiA9IGZ1bmN0aW9uKGRmLCBuYW1lMSwgbmFtZTIpIHsKICB0bXAxID0gZGF0YS5mcmFtZShkZltuYW1lMV0pCiAgdG1wMSR0eXBlID0gbmFtZTEKICBuYW1lcyh0bXAxKVsxXSA9ICdibGFoJwogIAogIHRtcDIgPSBkYXRhLmZyYW1lKGRmW25hbWUyXSkKICB0bXAyJHR5cGUgPSBuYW1lMgogIG5hbWVzKHRtcDIpWzFdID0gJ2JsYWgnCiAgCiAgdG1wID0gcmJpbmQoCiAgICB0bXAxLAogICAgdG1wMgogICkKCiAgZ2dwbG90KHRtcCwgYWVzX3N0cmluZygnYmxhaCcpKSArCiAgICBnZW9tX2RlbnNpdHkoYWVzKGZpbGw9ZmFjdG9yKHR5cGUpKSwgYWxwaGE9MC43KSArCiAgICAjZ2VvbV9oaXN0b2dyYW0oYWVzKGZpbGw9ZmFjdG9yKHR5cGUpKSwgYWxwaGE9MC44KSArCiAgICBzY2FsZV94X2xvZzEwKCkgKwogICAgbGFicygKICAgICAgI3RpdGxlPSJTdGF0ZXMiLAogICAgICAjc3VidGl0bGU9IklucHV0IiwKICAgICAgeD0iYmxhaCIsCiAgICAgIHk9IkRlbnNpdHkiKSAgCn0KYGBgCgoKCmBgYHtyIGVjaG89RkFMU0V9CiMgTG9hZGluZyBpbnB1dCBkYXRhCmRmID0gcmVhZF9maWxlKHBhcmFtcyRmaWxlKQoKZGYKCiMgcHJvY2VzcyBUSU1FT1VUUwpkZltpcy5uYShkZildIDwtIFRJTUVPVVQgKiAxLjAzCmBgYAoKfCBQYXJhbWV0ZXIgICAgICAgICAgICAgICAgICAgIHwgIFZhbHVlICAgICAgICAgIHwKfC0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLXwtLS0tLS0tLS0tLS0tLS0tLXwKfCAqKk5hbWUgb2YgYmVuY2htYXJrIHNldCoqICAgIHwgYHIgcGFyYW1zJGZpbGVgIHwKfCAqKlNpemUgb2YgYmVuY2htYXJrIHNldCoqICAgIHwgYHIgbnJvdyhkZilgICAgIHwKfCAqKlRpbWVvdXQqKiAgICAgICAgICAgICAgICAgIHwgYHIgVElNRU9VVGAgICAgIHwKCgoKYGBge3IgZWNobz1GQUxTRX0KcDEgPSBzY2F0KGRmLCAnTU9OQScsICdNT05BLmFudGlwcmVuZXhpbmcud2l0aC5mbGF0dGVuaW5nJykKcDIgPSBzY2F0KGRmLCAnTU9OQScsICdNT05BLmFudGlwcmVuZXhpbmcub24udGhlLmxldmVsLm9mLnByZWRpY2F0ZXMnKQpwMyA9IHNjYXQoZGYsICdNT05BLmFudGlwcmVuZXhpbmcud2l0aC5mbGF0dGVuaW5nJywgJ01PTkEuYW50aXByZW5leGluZy5vbi50aGUubGV2ZWwub2YucHJlZGljYXRlcycpCiNwMiA9IHNjYXQoY29uanVuY3Rpb24sICdtaW5yZXN1bHQnLCAnd29yc3RfY2FzZScpCgpncmlkLmFycmFuZ2UocDEsIHAyLCBwMywgbmNvbCA9IDMpCiNwbG90KHAxKQpgYGA=