(declare-const assert-0-b-proj-1~5143 Int)
(declare-const assert-0-b-proj-7~5149 Int)
(declare-const assert-0-b-proj-8~5150 Int)
(declare-const assert-0-result Bool)
(declare-const assert-0-x-proj-0~5121 Bool)
(declare-const assert-0-x-proj-10~5131 Bool)
(declare-const assert-0-x-proj-17~5138 Bool)
(declare-const assert-1-result Bool)
(declare-const assert-1-x-proj-0~5121 Bool)
(declare-const assert-1-x-proj-10~5131 Bool)
(declare-const assert-1-x-proj-12~5133 Bool)
(declare-const assert-1-x-proj-17~5138 Bool)
(declare-const assert-1-x-proj-18~5139 Int)
(declare-const assert-1-x-proj-19~5140 Bool)
(declare-const assert-10-b-proj-1~5143 Int)
(declare-const assert-10-b-proj-7~5149 Int)
(declare-const assert-10-b-proj-8~5150 Int)
(declare-const assert-10-result Bool)
(declare-const assert-10-x-proj-0~5121 Bool)
(declare-const assert-10-x-proj-10~5131 Bool)
(declare-const assert-10-x-proj-17~5138 Bool)
(declare-const assert-11-result Bool)
(declare-const assert-11-x-proj-0~5121 Bool)
(declare-const assert-11-x-proj-10~5131 Bool)
(declare-const assert-11-x-proj-12~5133 Bool)
(declare-const assert-11-x-proj-17~5138 Bool)
(declare-const assert-11-x-proj-18~5139 Int)
(declare-const assert-11-x-proj-19~5140 Bool)
(declare-const assert-12-result Bool)
(declare-const assert-12-x-proj-0~5121 Bool)
(declare-const assert-12-x-proj-10~5131 Bool)
(declare-const assert-12-x-proj-12~5133 Bool)
(declare-const assert-12-x-proj-17~5138 Bool)
(declare-const assert-12-x-proj-18~5139 Int)
(declare-const assert-12-x-proj-19~5140 Bool)
(declare-const assert-13-b-proj-1~5143 Int)
(declare-const assert-13-b-proj-7~5149 Int)
(declare-const assert-13-b-proj-8~5150 Int)
(declare-const assert-13-result Bool)
(declare-const assert-13-x-proj-0~5121 Bool)
(declare-const assert-13-x-proj-10~5131 Bool)
(declare-const assert-13-x-proj-17~5138 Bool)
(declare-const assert-14-b-proj-1~5143 Int)
(declare-const assert-14-b-proj-7~5149 Int)
(declare-const assert-14-b-proj-8~5150 Int)
(declare-const assert-14-result Bool)
(declare-const assert-14-x-proj-0~5121 Bool)
(declare-const assert-14-x-proj-10~5131 Bool)
(declare-const assert-14-x-proj-17~5138 Bool)
(declare-const assert-15-result Bool)
(declare-const assert-15-x-proj-0~5121 Bool)
(declare-const assert-15-x-proj-10~5131 Bool)
(declare-const assert-15-x-proj-12~5133 Bool)
(declare-const assert-15-x-proj-17~5138 Bool)
(declare-const assert-15-x-proj-18~5139 Int)
(declare-const assert-15-x-proj-19~5140 Bool)
(declare-const assert-16-b-proj-1~5143 Int)
(declare-const assert-16-b-proj-7~5149 Int)
(declare-const assert-16-b-proj-8~5150 Int)
(declare-const assert-16-result Bool)
(declare-const assert-16-x-proj-0~5121 Bool)
(declare-const assert-16-x-proj-10~5131 Bool)
(declare-const assert-16-x-proj-17~5138 Bool)
(declare-const assert-2-result Bool)
(declare-const assert-2-x-proj-0~5121 Bool)
(declare-const assert-2-x-proj-10~5131 Bool)
(declare-const assert-2-x-proj-12~5133 Bool)
(declare-const assert-2-x-proj-17~5138 Bool)
(declare-const assert-2-x-proj-18~5139 Int)
(declare-const assert-2-x-proj-19~5140 Bool)
(declare-const assert-3-result Bool)
(declare-const assert-3-x-proj-0~5121 Bool)
(declare-const assert-3-x-proj-10~5131 Bool)
(declare-const assert-3-x-proj-12~5133 Bool)
(declare-const assert-3-x-proj-17~5138 Bool)
(declare-const assert-3-x-proj-18~5139 Int)
(declare-const assert-3-x-proj-19~5140 Bool)
(declare-const assert-4-result Bool)
(declare-const assert-4-x-proj-0~5121 Bool)
(declare-const assert-4-x-proj-10~5131 Bool)
(declare-const assert-4-x-proj-12~5133 Bool)
(declare-const assert-4-x-proj-17~5138 Bool)
(declare-const assert-4-x-proj-19~5140 Bool)
(declare-const assert-5-b-proj-1~5143 Int)
(declare-const assert-5-b-proj-7~5149 Int)
(declare-const assert-5-b-proj-8~5150 Int)
(declare-const assert-5-result Bool)
(declare-const assert-5-x-proj-0~5121 Bool)
(declare-const assert-5-x-proj-10~5131 Bool)
(declare-const assert-5-x-proj-17~5138 Bool)
(declare-const assert-6-b-proj-1~5143 Int)
(declare-const assert-6-b-proj-7~5149 Int)
(declare-const assert-6-b-proj-8~5150 Int)
(declare-const assert-6-result Bool)
(declare-const assert-6-x-proj-0~5121 Bool)
(declare-const assert-6-x-proj-10~5131 Bool)
(declare-const assert-6-x-proj-17~5138 Bool)
(declare-const assert-7-b-proj-1~5143 Int)
(declare-const assert-7-b-proj-7~5149 Int)
(declare-const assert-7-b-proj-8~5150 Int)
(declare-const assert-7-result Bool)
(declare-const assert-7-x-proj-0~5121 Bool)
(declare-const assert-7-x-proj-10~5131 Bool)
(declare-const assert-7-x-proj-17~5138 Bool)
(declare-const assert-8-result Bool)
(declare-const assert-8-x-proj-0~5121 Bool)
(declare-const assert-8-x-proj-10~5131 Bool)
(declare-const assert-8-x-proj-12~5133 Bool)
(declare-const assert-8-x-proj-17~5138 Bool)
(declare-const assert-8-x-proj-19~5140 Bool)
(declare-const assert-9-result Bool)
(declare-const assert-9-x-proj-0~5121 Bool)
(declare-const assert-9-x-proj-10~5131 Bool)
(declare-const assert-9-x-proj-12~5133 Bool)
(declare-const assert-9-x-proj-17~5138 Bool)
(declare-const assert-9-x-proj-18~5139 Int)
(declare-const assert-9-x-proj-19~5140 Bool)
(declare-const init-1-result-proj-0 Bool)
(declare-const init-1-result-proj-11 Bool)
(declare-const init-1-result-proj-5 Bool)
(declare-const init-11-result-proj-0 Bool)
(declare-const init-11-result-proj-11 Bool)
(declare-const init-11-result-proj-5 Bool)
(declare-const init-12-result-proj-0 Bool)
(declare-const init-12-result-proj-11 Bool)
(declare-const init-12-result-proj-5 Bool)
(declare-const init-15-result-proj-0 Bool)
(declare-const init-15-result-proj-11 Bool)
(declare-const init-15-result-proj-5 Bool)
(declare-const init-2-result-proj-0 Bool)
(declare-const init-2-result-proj-11 Bool)
(declare-const init-2-result-proj-5 Bool)
(declare-const init-3-result-proj-0 Bool)
(declare-const init-3-result-proj-11 Bool)
(declare-const init-3-result-proj-5 Bool)
(declare-const init-4-result-proj-0 Bool)
(declare-const init-4-result-proj-11 Bool)
(declare-const init-4-result-proj-5 Bool)
(declare-const init-8-result-proj-0 Bool)
(declare-const init-8-result-proj-11 Bool)
(declare-const init-8-result-proj-5 Bool)
(declare-const init-9-result-proj-0 Bool)
(declare-const init-9-result-proj-11 Bool)
(declare-const init-9-result-proj-5 Bool)
(declare-const merge-1-1-TupleFlattenVar~5262 Int)
(declare-const merge-1-1-TupleFlattenVar~5263 Int)
(declare-const merge-1-1-TupleFlattenVar~5264 Bool)
(declare-const merge-1-1-TupleFlattenVar~5265 Bool)
(declare-const merge-1-1-TupleFlattenVar~5266 Bool)
(declare-const merge-1-1-TupleFlattenVar~5267 Bool)
(declare-const merge-1-1-TupleFlattenVar~5268 Bool)
(declare-const merge-1-1-TupleFlattenVar~5269 Int)
(declare-const merge-1-1-TupleFlattenVar~5270 Int)
(declare-const merge-1-1-TupleFlattenVar~5299 Int)
(declare-const merge-1-1-TupleFlattenVar~5300 Int)
(declare-const merge-1-1-TupleFlattenVar~5301 Int)
(declare-const merge-1-1-TupleFlattenVar~5302 Int)
(declare-const merge-1-1-a-proj-0~5244 Int)
(declare-const merge-1-1-a-proj-1~5245 Int)
(declare-const merge-1-1-a-proj-7~5251 Int)
(declare-const merge-1-1-a-proj-8~5252 Int)
(declare-const merge-1-1-a~5225 Int)
(declare-const merge-1-1-a~5227 Int)
(declare-const merge-1-1-a~5229 Int)
(declare-const merge-1-1-b-proj-0~5217 Bool)
(declare-const merge-1-1-b-proj-0~5231 Int)
(declare-const merge-1-1-b-proj-1~5232 Int)
(declare-const merge-1-1-b-proj-1~5254 Int)
(declare-const merge-1-1-b-proj-2~5233 Bool)
(declare-const merge-1-1-b-proj-3~5234 Bool)
(declare-const merge-1-1-b-proj-4~5235 Bool)
(declare-const merge-1-1-b-proj-5~5236 Bool)
(declare-const merge-1-1-b-proj-6~5237 Bool)
(declare-const merge-1-1-b-proj-7~5238 Int)
(declare-const merge-1-1-b-proj-7~5260 Int)
(declare-const merge-1-1-b-proj-8~5239 Int)
(declare-const merge-1-1-b-proj-8~5261 Int)
(declare-const merge-1-1-b~5226 Int)
(declare-const merge-1-1-b~5228 Int)
(declare-const merge-1-1-b~5230 Int)
(declare-const merge-1-1-o-proj-0~5215 Bool)
(declare-const merge-1-1-o-proj-0~5240 Int)
(declare-const merge-1-1-o-proj-1~5241 Int)
(declare-const merge-1-1-o-proj-2~5242 Int)
(declare-const merge-1-1-o-proj-3~5243 Int)
(declare-const merge-1-1-p1~5221 Int)
(declare-const merge-1-1-p2~5224 Int)
(declare-const merge-1-1-x-proj-0~5219 Bool)
(declare-const merge-1-1-y-proj-0~5222 Bool)
(declare-const merge-11-1-TupleFlattenVar~5262 Int)
(declare-const merge-11-1-TupleFlattenVar~5263 Int)
(declare-const merge-11-1-TupleFlattenVar~5264 Bool)
(declare-const merge-11-1-TupleFlattenVar~5265 Bool)
(declare-const merge-11-1-TupleFlattenVar~5266 Bool)
(declare-const merge-11-1-TupleFlattenVar~5267 Bool)
(declare-const merge-11-1-TupleFlattenVar~5268 Bool)
(declare-const merge-11-1-TupleFlattenVar~5269 Int)
(declare-const merge-11-1-TupleFlattenVar~5270 Int)
(declare-const merge-11-1-TupleFlattenVar~5299 Int)
(declare-const merge-11-1-TupleFlattenVar~5300 Int)
(declare-const merge-11-1-TupleFlattenVar~5301 Int)
(declare-const merge-11-1-TupleFlattenVar~5302 Int)
(declare-const merge-11-1-a-proj-0~5244 Int)
(declare-const merge-11-1-a-proj-1~5245 Int)
(declare-const merge-11-1-a-proj-7~5251 Int)
(declare-const merge-11-1-a-proj-8~5252 Int)
(declare-const merge-11-1-a~5225 Int)
(declare-const merge-11-1-a~5227 Int)
(declare-const merge-11-1-a~5229 Int)
(declare-const merge-11-1-b-proj-0~5217 Bool)
(declare-const merge-11-1-b-proj-0~5231 Int)
(declare-const merge-11-1-b-proj-1~5232 Int)
(declare-const merge-11-1-b-proj-1~5254 Int)
(declare-const merge-11-1-b-proj-2~5233 Bool)
(declare-const merge-11-1-b-proj-3~5234 Bool)
(declare-const merge-11-1-b-proj-4~5235 Bool)
(declare-const merge-11-1-b-proj-5~5236 Bool)
(declare-const merge-11-1-b-proj-6~5237 Bool)
(declare-const merge-11-1-b-proj-7~5238 Int)
(declare-const merge-11-1-b-proj-7~5260 Int)
(declare-const merge-11-1-b-proj-8~5239 Int)
(declare-const merge-11-1-b-proj-8~5261 Int)
(declare-const merge-11-1-b~5226 Int)
(declare-const merge-11-1-b~5228 Int)
(declare-const merge-11-1-b~5230 Int)
(declare-const merge-11-1-o-proj-0~5215 Bool)
(declare-const merge-11-1-o-proj-0~5240 Int)
(declare-const merge-11-1-o-proj-1~5241 Int)
(declare-const merge-11-1-o-proj-2~5242 Int)
(declare-const merge-11-1-o-proj-3~5243 Int)
(declare-const merge-11-1-p1~5221 Int)
(declare-const merge-11-1-p2~5224 Int)
(declare-const merge-11-1-x-proj-0~5219 Bool)
(declare-const merge-11-1-y-proj-0~5222 Bool)
(declare-const merge-12-1-TupleFlattenVar~5262 Int)
(declare-const merge-12-1-TupleFlattenVar~5263 Int)
(declare-const merge-12-1-TupleFlattenVar~5264 Bool)
(declare-const merge-12-1-TupleFlattenVar~5265 Bool)
(declare-const merge-12-1-TupleFlattenVar~5266 Bool)
(declare-const merge-12-1-TupleFlattenVar~5267 Bool)
(declare-const merge-12-1-TupleFlattenVar~5268 Bool)
(declare-const merge-12-1-TupleFlattenVar~5269 Int)
(declare-const merge-12-1-TupleFlattenVar~5270 Int)
(declare-const merge-12-1-TupleFlattenVar~5299 Int)
(declare-const merge-12-1-TupleFlattenVar~5300 Int)
(declare-const merge-12-1-TupleFlattenVar~5301 Int)
(declare-const merge-12-1-TupleFlattenVar~5302 Int)
(declare-const merge-12-1-a-proj-0~5244 Int)
(declare-const merge-12-1-a-proj-1~5245 Int)
(declare-const merge-12-1-a-proj-7~5251 Int)
(declare-const merge-12-1-a-proj-8~5252 Int)
(declare-const merge-12-1-a~5225 Int)
(declare-const merge-12-1-a~5227 Int)
(declare-const merge-12-1-a~5229 Int)
(declare-const merge-12-1-b-proj-0~5217 Bool)
(declare-const merge-12-1-b-proj-0~5231 Int)
(declare-const merge-12-1-b-proj-1~5232 Int)
(declare-const merge-12-1-b-proj-1~5254 Int)
(declare-const merge-12-1-b-proj-2~5233 Bool)
(declare-const merge-12-1-b-proj-3~5234 Bool)
(declare-const merge-12-1-b-proj-4~5235 Bool)
(declare-const merge-12-1-b-proj-5~5236 Bool)
(declare-const merge-12-1-b-proj-6~5237 Bool)
(declare-const merge-12-1-b-proj-7~5238 Int)
(declare-const merge-12-1-b-proj-7~5260 Int)
(declare-const merge-12-1-b-proj-8~5239 Int)
(declare-const merge-12-1-b-proj-8~5261 Int)
(declare-const merge-12-1-b~5226 Int)
(declare-const merge-12-1-b~5228 Int)
(declare-const merge-12-1-b~5230 Int)
(declare-const merge-12-1-o-proj-0~5215 Bool)
(declare-const merge-12-1-o-proj-0~5240 Int)
(declare-const merge-12-1-o-proj-1~5241 Int)
(declare-const merge-12-1-o-proj-2~5242 Int)
(declare-const merge-12-1-o-proj-3~5243 Int)
(declare-const merge-12-1-p1~5221 Int)
(declare-const merge-12-1-p2~5224 Int)
(declare-const merge-12-1-x-proj-0~5219 Bool)
(declare-const merge-12-1-y-proj-0~5222 Bool)
(declare-const merge-15-1-TupleFlattenVar~5262 Int)
(declare-const merge-15-1-TupleFlattenVar~5263 Int)
(declare-const merge-15-1-TupleFlattenVar~5264 Bool)
(declare-const merge-15-1-TupleFlattenVar~5265 Bool)
(declare-const merge-15-1-TupleFlattenVar~5266 Bool)
(declare-const merge-15-1-TupleFlattenVar~5267 Bool)
(declare-const merge-15-1-TupleFlattenVar~5268 Bool)
(declare-const merge-15-1-TupleFlattenVar~5269 Int)
(declare-const merge-15-1-TupleFlattenVar~5270 Int)
(declare-const merge-15-1-TupleFlattenVar~5299 Int)
(declare-const merge-15-1-TupleFlattenVar~5300 Int)
(declare-const merge-15-1-TupleFlattenVar~5301 Int)
(declare-const merge-15-1-TupleFlattenVar~5302 Int)
(declare-const merge-15-1-a-proj-0~5244 Int)
(declare-const merge-15-1-a-proj-1~5245 Int)
(declare-const merge-15-1-a-proj-7~5251 Int)
(declare-const merge-15-1-a-proj-8~5252 Int)
(declare-const merge-15-1-a~5225 Int)
(declare-const merge-15-1-a~5227 Int)
(declare-const merge-15-1-a~5229 Int)
(declare-const merge-15-1-b-proj-0~5217 Bool)
(declare-const merge-15-1-b-proj-0~5231 Int)
(declare-const merge-15-1-b-proj-1~5232 Int)
(declare-const merge-15-1-b-proj-1~5254 Int)
(declare-const merge-15-1-b-proj-2~5233 Bool)
(declare-const merge-15-1-b-proj-3~5234 Bool)
(declare-const merge-15-1-b-proj-4~5235 Bool)
(declare-const merge-15-1-b-proj-5~5236 Bool)
(declare-const merge-15-1-b-proj-6~5237 Bool)
(declare-const merge-15-1-b-proj-7~5238 Int)
(declare-const merge-15-1-b-proj-7~5260 Int)
(declare-const merge-15-1-b-proj-8~5239 Int)
(declare-const merge-15-1-b-proj-8~5261 Int)
(declare-const merge-15-1-b~5226 Int)
(declare-const merge-15-1-b~5228 Int)
(declare-const merge-15-1-b~5230 Int)
(declare-const merge-15-1-o-proj-0~5215 Bool)
(declare-const merge-15-1-o-proj-0~5240 Int)
(declare-const merge-15-1-o-proj-1~5241 Int)
(declare-const merge-15-1-o-proj-2~5242 Int)
(declare-const merge-15-1-o-proj-3~5243 Int)
(declare-const merge-15-1-p1~5221 Int)
(declare-const merge-15-1-p2~5224 Int)
(declare-const merge-15-1-x-proj-0~5219 Bool)
(declare-const merge-15-1-y-proj-0~5222 Bool)
(declare-const merge-2-1-TupleFlattenVar~5262 Int)
(declare-const merge-2-1-TupleFlattenVar~5263 Int)
(declare-const merge-2-1-TupleFlattenVar~5264 Bool)
(declare-const merge-2-1-TupleFlattenVar~5265 Bool)
(declare-const merge-2-1-TupleFlattenVar~5266 Bool)
(declare-const merge-2-1-TupleFlattenVar~5267 Bool)
(declare-const merge-2-1-TupleFlattenVar~5268 Bool)
(declare-const merge-2-1-TupleFlattenVar~5269 Int)
(declare-const merge-2-1-TupleFlattenVar~5270 Int)
(declare-const merge-2-1-TupleFlattenVar~5299 Int)
(declare-const merge-2-1-TupleFlattenVar~5300 Int)
(declare-const merge-2-1-TupleFlattenVar~5301 Int)
(declare-const merge-2-1-TupleFlattenVar~5302 Int)
(declare-const merge-2-1-a-proj-0~5244 Int)
(declare-const merge-2-1-a-proj-1~5245 Int)
(declare-const merge-2-1-a-proj-7~5251 Int)
(declare-const merge-2-1-a-proj-8~5252 Int)
(declare-const merge-2-1-a~5225 Int)
(declare-const merge-2-1-a~5227 Int)
(declare-const merge-2-1-a~5229 Int)
(declare-const merge-2-1-b-proj-0~5217 Bool)
(declare-const merge-2-1-b-proj-0~5231 Int)
(declare-const merge-2-1-b-proj-1~5232 Int)
(declare-const merge-2-1-b-proj-1~5254 Int)
(declare-const merge-2-1-b-proj-2~5233 Bool)
(declare-const merge-2-1-b-proj-3~5234 Bool)
(declare-const merge-2-1-b-proj-4~5235 Bool)
(declare-const merge-2-1-b-proj-5~5236 Bool)
(declare-const merge-2-1-b-proj-6~5237 Bool)
(declare-const merge-2-1-b-proj-7~5238 Int)
(declare-const merge-2-1-b-proj-7~5260 Int)
(declare-const merge-2-1-b-proj-8~5239 Int)
(declare-const merge-2-1-b-proj-8~5261 Int)
(declare-const merge-2-1-b~5226 Int)
(declare-const merge-2-1-b~5228 Int)
(declare-const merge-2-1-b~5230 Int)
(declare-const merge-2-1-o-proj-0~5215 Bool)
(declare-const merge-2-1-o-proj-0~5240 Int)
(declare-const merge-2-1-o-proj-1~5241 Int)
(declare-const merge-2-1-o-proj-2~5242 Int)
(declare-const merge-2-1-o-proj-3~5243 Int)
(declare-const merge-2-1-p1~5221 Int)
(declare-const merge-2-1-p2~5224 Int)
(declare-const merge-2-1-x-proj-0~5219 Bool)
(declare-const merge-2-1-y-proj-0~5222 Bool)
(declare-const merge-3-1-TupleFlattenVar~5262 Int)
(declare-const merge-3-1-TupleFlattenVar~5263 Int)
(declare-const merge-3-1-TupleFlattenVar~5264 Bool)
(declare-const merge-3-1-TupleFlattenVar~5265 Bool)
(declare-const merge-3-1-TupleFlattenVar~5266 Bool)
(declare-const merge-3-1-TupleFlattenVar~5267 Bool)
(declare-const merge-3-1-TupleFlattenVar~5268 Bool)
(declare-const merge-3-1-TupleFlattenVar~5269 Int)
(declare-const merge-3-1-TupleFlattenVar~5270 Int)
(declare-const merge-3-1-TupleFlattenVar~5299 Int)
(declare-const merge-3-1-TupleFlattenVar~5300 Int)
(declare-const merge-3-1-TupleFlattenVar~5301 Int)
(declare-const merge-3-1-TupleFlattenVar~5302 Int)
(declare-const merge-3-1-a-proj-0~5244 Int)
(declare-const merge-3-1-a-proj-1~5245 Int)
(declare-const merge-3-1-a-proj-7~5251 Int)
(declare-const merge-3-1-a-proj-8~5252 Int)
(declare-const merge-3-1-a~5225 Int)
(declare-const merge-3-1-a~5227 Int)
(declare-const merge-3-1-a~5229 Int)
(declare-const merge-3-1-b-proj-0~5217 Bool)
(declare-const merge-3-1-b-proj-0~5231 Int)
(declare-const merge-3-1-b-proj-1~5232 Int)
(declare-const merge-3-1-b-proj-1~5254 Int)
(declare-const merge-3-1-b-proj-2~5233 Bool)
(declare-const merge-3-1-b-proj-3~5234 Bool)
(declare-const merge-3-1-b-proj-4~5235 Bool)
(declare-const merge-3-1-b-proj-5~5236 Bool)
(declare-const merge-3-1-b-proj-6~5237 Bool)
(declare-const merge-3-1-b-proj-7~5238 Int)
(declare-const merge-3-1-b-proj-7~5260 Int)
(declare-const merge-3-1-b-proj-8~5239 Int)
(declare-const merge-3-1-b-proj-8~5261 Int)
(declare-const merge-3-1-b~5226 Int)
(declare-const merge-3-1-b~5228 Int)
(declare-const merge-3-1-b~5230 Int)
(declare-const merge-3-1-o-proj-0~5215 Bool)
(declare-const merge-3-1-o-proj-0~5240 Int)
(declare-const merge-3-1-o-proj-1~5241 Int)
(declare-const merge-3-1-o-proj-2~5242 Int)
(declare-const merge-3-1-o-proj-3~5243 Int)
(declare-const merge-3-1-p1~5221 Int)
(declare-const merge-3-1-p2~5224 Int)
(declare-const merge-3-1-x-proj-0~5219 Bool)
(declare-const merge-3-1-y-proj-0~5222 Bool)
(declare-const merge-4-1-TupleFlattenVar~5262 Int)
(declare-const merge-4-1-TupleFlattenVar~5263 Int)
(declare-const merge-4-1-TupleFlattenVar~5264 Bool)
(declare-const merge-4-1-TupleFlattenVar~5265 Bool)
(declare-const merge-4-1-TupleFlattenVar~5266 Bool)
(declare-const merge-4-1-TupleFlattenVar~5267 Bool)
(declare-const merge-4-1-TupleFlattenVar~5268 Bool)
(declare-const merge-4-1-TupleFlattenVar~5269 Int)
(declare-const merge-4-1-TupleFlattenVar~5270 Int)
(declare-const merge-4-1-TupleFlattenVar~5299 Int)
(declare-const merge-4-1-TupleFlattenVar~5300 Int)
(declare-const merge-4-1-TupleFlattenVar~5301 Int)
(declare-const merge-4-1-TupleFlattenVar~5302 Int)
(declare-const merge-4-1-a-proj-0~5244 Int)
(declare-const merge-4-1-a-proj-1~5245 Int)
(declare-const merge-4-1-a-proj-7~5251 Int)
(declare-const merge-4-1-a-proj-8~5252 Int)
(declare-const merge-4-1-a~5225 Int)
(declare-const merge-4-1-a~5227 Int)
(declare-const merge-4-1-a~5229 Int)
(declare-const merge-4-1-b-proj-0~5217 Bool)
(declare-const merge-4-1-b-proj-0~5231 Int)
(declare-const merge-4-1-b-proj-1~5232 Int)
(declare-const merge-4-1-b-proj-1~5254 Int)
(declare-const merge-4-1-b-proj-2~5233 Bool)
(declare-const merge-4-1-b-proj-3~5234 Bool)
(declare-const merge-4-1-b-proj-4~5235 Bool)
(declare-const merge-4-1-b-proj-5~5236 Bool)
(declare-const merge-4-1-b-proj-6~5237 Bool)
(declare-const merge-4-1-b-proj-7~5238 Int)
(declare-const merge-4-1-b-proj-7~5260 Int)
(declare-const merge-4-1-b-proj-8~5239 Int)
(declare-const merge-4-1-b-proj-8~5261 Int)
(declare-const merge-4-1-b~5226 Int)
(declare-const merge-4-1-b~5228 Int)
(declare-const merge-4-1-b~5230 Int)
(declare-const merge-4-1-o-proj-0~5215 Bool)
(declare-const merge-4-1-o-proj-0~5240 Int)
(declare-const merge-4-1-o-proj-1~5241 Int)
(declare-const merge-4-1-o-proj-2~5242 Int)
(declare-const merge-4-1-o-proj-3~5243 Int)
(declare-const merge-4-1-p1~5221 Int)
(declare-const merge-4-1-p2~5224 Int)
(declare-const merge-4-1-result-proj-0 Bool)
(declare-const merge-4-1-result-proj-11 Bool)
(declare-const merge-4-1-result-proj-12 Int)
(declare-const merge-4-1-result-proj-13 Bool)
(declare-const merge-4-1-result-proj-5 Bool)
(declare-const merge-4-1-result-proj-7 Bool)
(declare-const merge-4-1-x-proj-0~5219 Bool)
(declare-const merge-4-1-y-proj-0~5222 Bool)
(declare-const merge-4-2-TupleFlattenVar~5262 Int)
(declare-const merge-4-2-TupleFlattenVar~5263 Int)
(declare-const merge-4-2-TupleFlattenVar~5264 Bool)
(declare-const merge-4-2-TupleFlattenVar~5265 Bool)
(declare-const merge-4-2-TupleFlattenVar~5266 Bool)
(declare-const merge-4-2-TupleFlattenVar~5267 Bool)
(declare-const merge-4-2-TupleFlattenVar~5268 Bool)
(declare-const merge-4-2-TupleFlattenVar~5269 Int)
(declare-const merge-4-2-TupleFlattenVar~5270 Int)
(declare-const merge-4-2-TupleFlattenVar~5299 Int)
(declare-const merge-4-2-TupleFlattenVar~5300 Int)
(declare-const merge-4-2-TupleFlattenVar~5301 Int)
(declare-const merge-4-2-TupleFlattenVar~5302 Int)
(declare-const merge-4-2-a-proj-0~5244 Int)
(declare-const merge-4-2-a-proj-1~5245 Int)
(declare-const merge-4-2-a-proj-7~5251 Int)
(declare-const merge-4-2-a-proj-8~5252 Int)
(declare-const merge-4-2-a~5225 Int)
(declare-const merge-4-2-a~5227 Int)
(declare-const merge-4-2-a~5229 Int)
(declare-const merge-4-2-b-proj-0~5217 Bool)
(declare-const merge-4-2-b-proj-0~5231 Int)
(declare-const merge-4-2-b-proj-1~5232 Int)
(declare-const merge-4-2-b-proj-2~5233 Bool)
(declare-const merge-4-2-b-proj-3~5234 Bool)
(declare-const merge-4-2-b-proj-4~5235 Bool)
(declare-const merge-4-2-b-proj-5~5236 Bool)
(declare-const merge-4-2-b-proj-6~5237 Bool)
(declare-const merge-4-2-b-proj-7~5238 Int)
(declare-const merge-4-2-b-proj-8~5239 Int)
(declare-const merge-4-2-b~5226 Int)
(declare-const merge-4-2-b~5228 Int)
(declare-const merge-4-2-b~5230 Int)
(declare-const merge-4-2-o-proj-0~5215 Bool)
(declare-const merge-4-2-o-proj-0~5240 Int)
(declare-const merge-4-2-p1~5221 Int)
(declare-const merge-4-2-p2~5224 Int)
(declare-const merge-4-2-x-proj-0~5219 Bool)
(declare-const merge-4-2-y-proj-0~5222 Bool)
(declare-const merge-8-1-TupleFlattenVar~5262 Int)
(declare-const merge-8-1-TupleFlattenVar~5263 Int)
(declare-const merge-8-1-TupleFlattenVar~5264 Bool)
(declare-const merge-8-1-TupleFlattenVar~5265 Bool)
(declare-const merge-8-1-TupleFlattenVar~5266 Bool)
(declare-const merge-8-1-TupleFlattenVar~5267 Bool)
(declare-const merge-8-1-TupleFlattenVar~5268 Bool)
(declare-const merge-8-1-TupleFlattenVar~5269 Int)
(declare-const merge-8-1-TupleFlattenVar~5270 Int)
(declare-const merge-8-1-TupleFlattenVar~5299 Int)
(declare-const merge-8-1-TupleFlattenVar~5300 Int)
(declare-const merge-8-1-TupleFlattenVar~5301 Int)
(declare-const merge-8-1-TupleFlattenVar~5302 Int)
(declare-const merge-8-1-a-proj-0~5244 Int)
(declare-const merge-8-1-a-proj-1~5245 Int)
(declare-const merge-8-1-a-proj-7~5251 Int)
(declare-const merge-8-1-a-proj-8~5252 Int)
(declare-const merge-8-1-a~5225 Int)
(declare-const merge-8-1-a~5227 Int)
(declare-const merge-8-1-a~5229 Int)
(declare-const merge-8-1-b-proj-0~5217 Bool)
(declare-const merge-8-1-b-proj-0~5231 Int)
(declare-const merge-8-1-b-proj-1~5232 Int)
(declare-const merge-8-1-b-proj-1~5254 Int)
(declare-const merge-8-1-b-proj-2~5233 Bool)
(declare-const merge-8-1-b-proj-3~5234 Bool)
(declare-const merge-8-1-b-proj-4~5235 Bool)
(declare-const merge-8-1-b-proj-5~5236 Bool)
(declare-const merge-8-1-b-proj-6~5237 Bool)
(declare-const merge-8-1-b-proj-7~5238 Int)
(declare-const merge-8-1-b-proj-7~5260 Int)
(declare-const merge-8-1-b-proj-8~5239 Int)
(declare-const merge-8-1-b-proj-8~5261 Int)
(declare-const merge-8-1-b~5226 Int)
(declare-const merge-8-1-b~5228 Int)
(declare-const merge-8-1-b~5230 Int)
(declare-const merge-8-1-o-proj-0~5215 Bool)
(declare-const merge-8-1-o-proj-0~5240 Int)
(declare-const merge-8-1-p1~5221 Int)
(declare-const merge-8-1-p2~5224 Int)
(declare-const merge-8-1-x-proj-0~5219 Bool)
(declare-const merge-8-1-y-proj-0~5222 Bool)
(declare-const merge-9-1-TupleFlattenVar~5262 Int)
(declare-const merge-9-1-TupleFlattenVar~5263 Int)
(declare-const merge-9-1-TupleFlattenVar~5264 Bool)
(declare-const merge-9-1-TupleFlattenVar~5265 Bool)
(declare-const merge-9-1-TupleFlattenVar~5266 Bool)
(declare-const merge-9-1-TupleFlattenVar~5267 Bool)
(declare-const merge-9-1-TupleFlattenVar~5268 Bool)
(declare-const merge-9-1-TupleFlattenVar~5269 Int)
(declare-const merge-9-1-TupleFlattenVar~5270 Int)
(declare-const merge-9-1-TupleFlattenVar~5299 Int)
(declare-const merge-9-1-TupleFlattenVar~5300 Int)
(declare-const merge-9-1-TupleFlattenVar~5301 Int)
(declare-const merge-9-1-TupleFlattenVar~5302 Int)
(declare-const merge-9-1-a-proj-0~5244 Int)
(declare-const merge-9-1-a-proj-1~5245 Int)
(declare-const merge-9-1-a-proj-7~5251 Int)
(declare-const merge-9-1-a-proj-8~5252 Int)
(declare-const merge-9-1-a~5225 Int)
(declare-const merge-9-1-a~5227 Int)
(declare-const merge-9-1-a~5229 Int)
(declare-const merge-9-1-b-proj-0~5217 Bool)
(declare-const merge-9-1-b-proj-0~5231 Int)
(declare-const merge-9-1-b-proj-1~5232 Int)
(declare-const merge-9-1-b-proj-1~5254 Int)
(declare-const merge-9-1-b-proj-2~5233 Bool)
(declare-const merge-9-1-b-proj-3~5234 Bool)
(declare-const merge-9-1-b-proj-4~5235 Bool)
(declare-const merge-9-1-b-proj-5~5236 Bool)
(declare-const merge-9-1-b-proj-6~5237 Bool)
(declare-const merge-9-1-b-proj-7~5238 Int)
(declare-const merge-9-1-b-proj-7~5260 Int)
(declare-const merge-9-1-b-proj-8~5239 Int)
(declare-const merge-9-1-b-proj-8~5261 Int)
(declare-const merge-9-1-b~5226 Int)
(declare-const merge-9-1-b~5228 Int)
(declare-const merge-9-1-b~5230 Int)
(declare-const merge-9-1-o-proj-0~5215 Bool)
(declare-const merge-9-1-o-proj-0~5240 Int)
(declare-const merge-9-1-o-proj-1~5241 Int)
(declare-const merge-9-1-o-proj-2~5242 Int)
(declare-const merge-9-1-o-proj-3~5243 Int)
(declare-const merge-9-1-p1~5221 Int)
(declare-const merge-9-1-p2~5224 Int)
(declare-const merge-9-1-x-proj-0~5219 Bool)
(declare-const merge-9-1-y-proj-0~5222 Bool)
(declare-const symbolic-d-proj-0~5119 Int)
(declare-const symbolic-d-proj-1~5118 Int)
(declare-const trans-0-1-b-proj-0~5365 Bool)
(declare-const trans-0-1-b-proj-0~5375 Int)
(declare-const trans-0-1-b-proj-0~5412 Bool)
(declare-const trans-0-1-b-proj-0~5422 Int)
(declare-const trans-0-1-b-proj-1~5376 Int)
(declare-const trans-0-1-b-proj-1~5423 Int)
(declare-const trans-0-1-b-proj-2~5377 Bool)
(declare-const trans-0-1-b-proj-3~5356 Bool)
(declare-const trans-0-1-b-proj-3~5378 Bool)
(declare-const trans-0-1-b-proj-4~5357 Bool)
(declare-const trans-0-1-b-proj-4~5379 Bool)
(declare-const trans-0-1-b-proj-5~5358 Bool)
(declare-const trans-0-1-b-proj-5~5380 Bool)
(declare-const trans-0-1-b-proj-6~5359 Bool)
(declare-const trans-0-1-b-proj-6~5381 Bool)
(declare-const trans-0-1-b-proj-7~5360 Bool)
(declare-const trans-0-1-b-proj-7~5382 Int)
(declare-const trans-0-1-b-proj-7~5429 Int)
(declare-const trans-0-1-b-proj-8~5383 Int)
(declare-const trans-0-1-b-proj-8~5430 Int)
(declare-const trans-0-1-result-proj-0 Bool)
(declare-const trans-10-4-b-proj-0~6099 Bool)
(declare-const trans-10-4-b-proj-0~6109 Int)
(declare-const trans-10-4-b-proj-0~6132 Bool)
(declare-const trans-10-4-b-proj-0~6142 Int)
(declare-const trans-10-4-b-proj-1~6110 Int)
(declare-const trans-10-4-b-proj-1~6143 Int)
(declare-const trans-10-4-b-proj-2~6111 Bool)
(declare-const trans-10-4-b-proj-3~5356 Bool)
(declare-const trans-10-4-b-proj-3~6112 Bool)
(declare-const trans-10-4-b-proj-4~5357 Bool)
(declare-const trans-10-4-b-proj-4~6113 Bool)
(declare-const trans-10-4-b-proj-5~5358 Bool)
(declare-const trans-10-4-b-proj-5~6114 Bool)
(declare-const trans-10-4-b-proj-6~5359 Bool)
(declare-const trans-10-4-b-proj-6~6115 Bool)
(declare-const trans-10-4-b-proj-7~5360 Bool)
(declare-const trans-10-4-b-proj-7~6116 Int)
(declare-const trans-10-4-b-proj-7~6149 Int)
(declare-const trans-10-4-b-proj-8~6117 Int)
(declare-const trans-10-4-b-proj-8~6150 Int)
(declare-const trans-10-4-result-proj-0 Bool)
(declare-const trans-13-3-b-proj-0~6192 Bool)
(declare-const trans-13-3-b-proj-0~6202 Int)
(declare-const trans-13-3-b-proj-1~6203 Int)
(declare-const trans-13-3-b-proj-3~5356 Bool)
(declare-const trans-13-3-b-proj-4~5357 Bool)
(declare-const trans-13-3-b-proj-5~5358 Bool)
(declare-const trans-13-3-b-proj-6~5359 Bool)
(declare-const trans-13-3-b-proj-7~5360 Bool)
(declare-const trans-13-3-b-proj-7~6209 Int)
(declare-const trans-13-3-b-proj-8~6210 Int)
(declare-const trans-13-3-result-proj-0 Bool)
(declare-const trans-14-15-b-proj-0~5919 Bool)
(declare-const trans-14-15-b-proj-0~5929 Int)
(declare-const trans-14-15-b-proj-0~5966 Bool)
(declare-const trans-14-15-b-proj-0~5976 Int)
(declare-const trans-14-15-b-proj-1~5930 Int)
(declare-const trans-14-15-b-proj-1~5977 Int)
(declare-const trans-14-15-b-proj-2~5931 Bool)
(declare-const trans-14-15-b-proj-3~5356 Bool)
(declare-const trans-14-15-b-proj-3~5932 Bool)
(declare-const trans-14-15-b-proj-4~5357 Bool)
(declare-const trans-14-15-b-proj-4~5933 Bool)
(declare-const trans-14-15-b-proj-5~5358 Bool)
(declare-const trans-14-15-b-proj-5~5934 Bool)
(declare-const trans-14-15-b-proj-6~5359 Bool)
(declare-const trans-14-15-b-proj-6~5935 Bool)
(declare-const trans-14-15-b-proj-7~5360 Bool)
(declare-const trans-14-15-b-proj-7~5936 Int)
(declare-const trans-14-15-b-proj-7~5983 Int)
(declare-const trans-14-15-b-proj-8~5937 Int)
(declare-const trans-14-15-b-proj-8~5984 Int)
(declare-const trans-14-15-result-proj-0 Bool)
(declare-const trans-16-12-b-proj-0~5836 Bool)
(declare-const trans-16-12-b-proj-0~5846 Int)
(declare-const trans-16-12-b-proj-0~5869 Bool)
(declare-const trans-16-12-b-proj-0~5879 Int)
(declare-const trans-16-12-b-proj-1~5847 Int)
(declare-const trans-16-12-b-proj-1~5880 Int)
(declare-const trans-16-12-b-proj-2~5848 Bool)
(declare-const trans-16-12-b-proj-3~5356 Bool)
(declare-const trans-16-12-b-proj-3~5849 Bool)
(declare-const trans-16-12-b-proj-4~5357 Bool)
(declare-const trans-16-12-b-proj-4~5850 Bool)
(declare-const trans-16-12-b-proj-5~5358 Bool)
(declare-const trans-16-12-b-proj-5~5851 Bool)
(declare-const trans-16-12-b-proj-6~5359 Bool)
(declare-const trans-16-12-b-proj-6~5852 Bool)
(declare-const trans-16-12-b-proj-7~5360 Bool)
(declare-const trans-16-12-b-proj-7~5853 Int)
(declare-const trans-16-12-b-proj-7~5886 Int)
(declare-const trans-16-12-b-proj-8~5854 Int)
(declare-const trans-16-12-b-proj-8~5887 Int)
(declare-const trans-16-12-result-proj-0 Bool)
(declare-const trans-4-8-b-proj-0~5573 Bool)
(declare-const trans-4-8-b-proj-0~5583 Int)
(declare-const trans-4-8-b-proj-0~5606 Bool)
(declare-const trans-4-8-b-proj-0~5616 Int)
(declare-const trans-4-8-b-proj-1~5584 Int)
(declare-const trans-4-8-b-proj-1~5617 Int)
(declare-const trans-4-8-b-proj-2~5585 Bool)
(declare-const trans-4-8-b-proj-3~5356 Bool)
(declare-const trans-4-8-b-proj-3~5586 Bool)
(declare-const trans-4-8-b-proj-4~5357 Bool)
(declare-const trans-4-8-b-proj-4~5587 Bool)
(declare-const trans-4-8-b-proj-5~5358 Bool)
(declare-const trans-4-8-b-proj-5~5588 Bool)
(declare-const trans-4-8-b-proj-6~5359 Bool)
(declare-const trans-4-8-b-proj-6~5589 Bool)
(declare-const trans-4-8-b-proj-7~5360 Bool)
(declare-const trans-4-8-b-proj-7~5590 Int)
(declare-const trans-4-8-b-proj-7~5623 Int)
(declare-const trans-4-8-b-proj-8~5591 Int)
(declare-const trans-4-8-b-proj-8~5624 Int)
(declare-const trans-4-8-o-proj-1~6241 Int)
(declare-const trans-4-8-o-proj-2~6242 Int)
(declare-const trans-4-8-o-proj-3~6243 Int)
(declare-const trans-4-8-result-proj-0 Bool)
(declare-const trans-4-8-y~5639 Int)
(declare-const trans-5-11-b-proj-0~5656 Bool)
(declare-const trans-5-11-b-proj-0~5666 Int)
(declare-const trans-5-11-b-proj-0~5689 Bool)
(declare-const trans-5-11-b-proj-0~5699 Int)
(declare-const trans-5-11-b-proj-1~5667 Int)
(declare-const trans-5-11-b-proj-1~5700 Int)
(declare-const trans-5-11-b-proj-2~5668 Bool)
(declare-const trans-5-11-b-proj-3~5356 Bool)
(declare-const trans-5-11-b-proj-3~5669 Bool)
(declare-const trans-5-11-b-proj-4~5357 Bool)
(declare-const trans-5-11-b-proj-4~5670 Bool)
(declare-const trans-5-11-b-proj-5~5358 Bool)
(declare-const trans-5-11-b-proj-5~5671 Bool)
(declare-const trans-5-11-b-proj-6~5359 Bool)
(declare-const trans-5-11-b-proj-6~5672 Bool)
(declare-const trans-5-11-b-proj-7~5360 Bool)
(declare-const trans-5-11-b-proj-7~5673 Int)
(declare-const trans-5-11-b-proj-7~5706 Int)
(declare-const trans-5-11-b-proj-8~5674 Int)
(declare-const trans-5-11-b-proj-8~5707 Int)
(declare-const trans-5-11-result-proj-0 Bool)
(declare-const trans-6-2-b-proj-0~5462 Bool)
(declare-const trans-6-2-b-proj-0~5472 Int)
(declare-const trans-6-2-b-proj-0~5523 Bool)
(declare-const trans-6-2-b-proj-0~5533 Int)
(declare-const trans-6-2-b-proj-1~5473 Int)
(declare-const trans-6-2-b-proj-1~5534 Int)
(declare-const trans-6-2-b-proj-2~5474 Bool)
(declare-const trans-6-2-b-proj-3~5356 Bool)
(declare-const trans-6-2-b-proj-3~5475 Bool)
(declare-const trans-6-2-b-proj-4~5357 Bool)
(declare-const trans-6-2-b-proj-4~5476 Bool)
(declare-const trans-6-2-b-proj-5~5358 Bool)
(declare-const trans-6-2-b-proj-5~5477 Bool)
(declare-const trans-6-2-b-proj-6~5359 Bool)
(declare-const trans-6-2-b-proj-6~5478 Bool)
(declare-const trans-6-2-b-proj-7~5360 Bool)
(declare-const trans-6-2-b-proj-7~5479 Int)
(declare-const trans-6-2-b-proj-7~5540 Int)
(declare-const trans-6-2-b-proj-8~5480 Int)
(declare-const trans-6-2-b-proj-8~5541 Int)
(declare-const trans-6-2-result-proj-0 Bool)
(declare-const trans-7-9-b-proj-0~6016 Bool)
(declare-const trans-7-9-b-proj-0~6026 Int)
(declare-const trans-7-9-b-proj-0~6049 Bool)
(declare-const trans-7-9-b-proj-0~6059 Int)
(declare-const trans-7-9-b-proj-1~6027 Int)
(declare-const trans-7-9-b-proj-1~6060 Int)
(declare-const trans-7-9-b-proj-2~6028 Bool)
(declare-const trans-7-9-b-proj-3~5356 Bool)
(declare-const trans-7-9-b-proj-3~6029 Bool)
(declare-const trans-7-9-b-proj-4~5357 Bool)
(declare-const trans-7-9-b-proj-4~6030 Bool)
(declare-const trans-7-9-b-proj-5~5358 Bool)
(declare-const trans-7-9-b-proj-5~6031 Bool)
(declare-const trans-7-9-b-proj-6~5359 Bool)
(declare-const trans-7-9-b-proj-6~6032 Bool)
(declare-const trans-7-9-b-proj-7~5360 Bool)
(declare-const trans-7-9-b-proj-7~6033 Int)
(declare-const trans-7-9-b-proj-7~6066 Int)
(declare-const trans-7-9-b-proj-8~6034 Int)
(declare-const trans-7-9-b-proj-8~6067 Int)
(declare-const trans-7-9-result-proj-0 Bool)
(declare-const trans-8-4-b-proj-0~5739 Bool)
(declare-const trans-8-4-b-proj-0~5749 Int)
(declare-const trans-8-4-b-proj-0~5786 Bool)
(declare-const trans-8-4-b-proj-0~5796 Int)
(declare-const trans-8-4-b-proj-1~5750 Int)
(declare-const trans-8-4-b-proj-1~5797 Int)
(declare-const trans-8-4-b-proj-2~5751 Bool)
(declare-const trans-8-4-b-proj-3~5356 Bool)
(declare-const trans-8-4-b-proj-3~5752 Bool)
(declare-const trans-8-4-b-proj-4~5357 Bool)
(declare-const trans-8-4-b-proj-4~5753 Bool)
(declare-const trans-8-4-b-proj-5~5358 Bool)
(declare-const trans-8-4-b-proj-5~5754 Bool)
(declare-const trans-8-4-b-proj-6~5359 Bool)
(declare-const trans-8-4-b-proj-6~5755 Bool)
(declare-const trans-8-4-b-proj-7~5360 Bool)
(declare-const trans-8-4-b-proj-7~5756 Int)
(declare-const trans-8-4-b-proj-7~5803 Int)
(declare-const trans-8-4-b-proj-8~5757 Int)
(declare-const trans-8-4-b-proj-8~5804 Int)
(declare-const trans-8-4-o-proj-1~6241 Int)
(declare-const trans-8-4-o-proj-2~6242 Int)
(declare-const trans-8-4-o-proj-3~6243 Int)
(declare-const trans-8-4-result-proj-0 Bool)
(declare-const trans-8-4-y~5819 Int)
 (assert (= assert-0-x-proj-0~5121 (ite (or (= symbolic-d-proj-0~5119 167772246) (= symbolic-d-proj-0~5119 167772162)) false (and (= symbolic-d-proj-1~5118 24) (= symbolic-d-proj-0~5119 3355585280)))))
(assert (= assert-0-b-proj-1~5143 (ite (or (= symbolic-d-proj-0~5119 167772246) (= symbolic-d-proj-0~5119 167772162)) 0 (ite (and (= symbolic-d-proj-1~5118 24) (= symbolic-d-proj-0~5119 3355585280)) 20 0))))
(assert (= assert-0-b-proj-7~5149 (ite (or (= symbolic-d-proj-0~5119 167772246) (= symbolic-d-proj-0~5119 167772162)) 0 (ite (and (= symbolic-d-proj-1~5118 24) (= symbolic-d-proj-0~5119 3355585280)) 100 0))))
(assert (= assert-0-b-proj-8~5150 (ite (or (= symbolic-d-proj-0~5119 167772246) (= symbolic-d-proj-0~5119 167772162)) 0 (ite (and (= symbolic-d-proj-1~5118 24) (= symbolic-d-proj-0~5119 3355585280)) 80 0))))
(assert (= assert-0-x-proj-10~5131 (ite (or (= symbolic-d-proj-0~5119 167772246) (= symbolic-d-proj-0~5119 167772162)) true (and (= symbolic-d-proj-1~5118 24) (= symbolic-d-proj-0~5119 3355585280)))))
(assert (= assert-0-x-proj-17~5138 (ite (or (= symbolic-d-proj-0~5119 167772246) (= symbolic-d-proj-0~5119 167772162)) true (and (= symbolic-d-proj-1~5118 24) (= symbolic-d-proj-0~5119 3355585280)))))
(assert (= init-1-result-proj-0 (ite (or (or (= symbolic-d-proj-0~5119 167772164) (= symbolic-d-proj-0~5119 167772162)) (= symbolic-d-proj-0~5119 167772160)) false (and (= symbolic-d-proj-1~5118 24) (= symbolic-d-proj-0~5119 3355595264)))))
(assert (= merge-1-1-b-proj-1~5254 (ite (or (or (= symbolic-d-proj-0~5119 167772164) (= symbolic-d-proj-0~5119 167772162)) (= symbolic-d-proj-0~5119 167772160)) 0 (ite (and (= symbolic-d-proj-1~5118 24) (= symbolic-d-proj-0~5119 3355595264)) 20 0))))
(assert (= merge-1-1-b-proj-7~5260 (ite (or (or (= symbolic-d-proj-0~5119 167772164) (= symbolic-d-proj-0~5119 167772162)) (= symbolic-d-proj-0~5119 167772160)) 0 (ite (and (= symbolic-d-proj-1~5118 24) (= symbolic-d-proj-0~5119 3355595264)) 100 0))))
(assert (= merge-1-1-b-proj-8~5261 (ite (or (or (= symbolic-d-proj-0~5119 167772164) (= symbolic-d-proj-0~5119 167772162)) (= symbolic-d-proj-0~5119 167772160)) 0 (ite (and (= symbolic-d-proj-1~5118 24) (= symbolic-d-proj-0~5119 3355595264)) 80 0))))
(assert (= init-1-result-proj-5 (ite (or (or (= symbolic-d-proj-0~5119 167772164) (= symbolic-d-proj-0~5119 167772162)) (= symbolic-d-proj-0~5119 167772160)) true (and (= symbolic-d-proj-1~5118 24) (= symbolic-d-proj-0~5119 3355595264)))))
(assert (= init-1-result-proj-11 (ite (or (or (= symbolic-d-proj-0~5119 167772164) (= symbolic-d-proj-0~5119 167772162)) (= symbolic-d-proj-0~5119 167772160)) true (and (= symbolic-d-proj-1~5118 24) (= symbolic-d-proj-0~5119 3355595264)))))
(assert (= init-2-result-proj-0 (ite (or (or (= symbolic-d-proj-0~5119 167772286) (= symbolic-d-proj-0~5119 167772328)) (= symbolic-d-proj-0~5119 167772326)) false (and (= symbolic-d-proj-1~5118 24) (= symbolic-d-proj-0~5119 3355600128)))))
(assert (= merge-2-1-b-proj-1~5254 (ite (or (or (= symbolic-d-proj-0~5119 167772286) (= symbolic-d-proj-0~5119 167772328)) (= symbolic-d-proj-0~5119 167772326)) 0 (ite (and (= symbolic-d-proj-1~5118 24) (= symbolic-d-proj-0~5119 3355600128)) 20 0))))
(assert (= merge-2-1-b-proj-7~5260 (ite (or (or (= symbolic-d-proj-0~5119 167772286) (= symbolic-d-proj-0~5119 167772328)) (= symbolic-d-proj-0~5119 167772326)) 0 (ite (and (= symbolic-d-proj-1~5118 24) (= symbolic-d-proj-0~5119 3355600128)) 100 0))))
(assert (= merge-2-1-b-proj-8~5261 (ite (or (or (= symbolic-d-proj-0~5119 167772286) (= symbolic-d-proj-0~5119 167772328)) (= symbolic-d-proj-0~5119 167772326)) 0 (ite (and (= symbolic-d-proj-1~5118 24) (= symbolic-d-proj-0~5119 3355600128)) 80 0))))
(assert (= init-2-result-proj-5 (ite (or (or (= symbolic-d-proj-0~5119 167772286) (= symbolic-d-proj-0~5119 167772328)) (= symbolic-d-proj-0~5119 167772326)) true (and (= symbolic-d-proj-1~5118 24) (= symbolic-d-proj-0~5119 3355600128)))))
(assert (= init-2-result-proj-11 (ite (or (or (= symbolic-d-proj-0~5119 167772286) (= symbolic-d-proj-0~5119 167772328)) (= symbolic-d-proj-0~5119 167772326)) true (and (= symbolic-d-proj-1~5118 24) (= symbolic-d-proj-0~5119 3355600128)))))
(assert (= init-3-result-proj-0 (ite (and (= symbolic-d-proj-1~5118 31) (= symbolic-d-proj-0~5119 167772248)) false (or (= symbolic-d-proj-0~5119 3355591424) (= symbolic-d-proj-0~5119 2147485440)))))
(assert (= merge-3-1-b-proj-1~5254 (ite (and (= symbolic-d-proj-1~5118 31) (= symbolic-d-proj-0~5119 167772248)) 0 (ite (or (= symbolic-d-proj-0~5119 3355591424) (= symbolic-d-proj-0~5119 2147485440)) 20 0))))
(assert (= merge-3-1-b-proj-7~5260 (ite (and (= symbolic-d-proj-1~5118 31) (= symbolic-d-proj-0~5119 167772248)) 0 (ite (or (= symbolic-d-proj-0~5119 3355591424) (= symbolic-d-proj-0~5119 2147485440)) 100 0))))
(assert (= merge-3-1-b-proj-8~5261 (ite (and (= symbolic-d-proj-1~5118 31) (= symbolic-d-proj-0~5119 167772248)) 0 (ite (or (= symbolic-d-proj-0~5119 3355591424) (= symbolic-d-proj-0~5119 2147485440)) 80 0))))
(assert (= init-3-result-proj-5 (ite (and (= symbolic-d-proj-1~5118 31) (= symbolic-d-proj-0~5119 167772248)) true (or (= symbolic-d-proj-0~5119 3355591424) (= symbolic-d-proj-0~5119 2147485440)))))
(assert (= init-3-result-proj-11 (ite (and (= symbolic-d-proj-1~5118 31) (= symbolic-d-proj-0~5119 167772248)) true (or (= symbolic-d-proj-0~5119 3355591424) (= symbolic-d-proj-0~5119 2147485440)))))
(assert (= init-4-result-proj-0 (ite (or (or (= symbolic-d-proj-0~5119 167772204) (= symbolic-d-proj-0~5119 167772202)) (= symbolic-d-proj-0~5119 167772200)) false (and (= symbolic-d-proj-1~5118 24) (= symbolic-d-proj-0~5119 3355596544)))))
(assert (= merge-4-1-b-proj-1~5254 (ite (or (or (= symbolic-d-proj-0~5119 167772204) (= symbolic-d-proj-0~5119 167772202)) (= symbolic-d-proj-0~5119 167772200)) 0 (ite (and (= symbolic-d-proj-1~5118 24) (= symbolic-d-proj-0~5119 3355596544)) 20 0))))
(assert (= merge-4-1-b-proj-7~5260 (ite (or (or (= symbolic-d-proj-0~5119 167772204) (= symbolic-d-proj-0~5119 167772202)) (= symbolic-d-proj-0~5119 167772200)) 0 (ite (and (= symbolic-d-proj-1~5118 24) (= symbolic-d-proj-0~5119 3355596544)) 100 0))))
(assert (= merge-4-1-b-proj-8~5261 (ite (or (or (= symbolic-d-proj-0~5119 167772204) (= symbolic-d-proj-0~5119 167772202)) (= symbolic-d-proj-0~5119 167772200)) 0 (ite (and (= symbolic-d-proj-1~5118 24) (= symbolic-d-proj-0~5119 3355596544)) 80 0))))
(assert (= init-4-result-proj-5 (ite (or (or (= symbolic-d-proj-0~5119 167772204) (= symbolic-d-proj-0~5119 167772202)) (= symbolic-d-proj-0~5119 167772200)) true (and (= symbolic-d-proj-1~5118 24) (= symbolic-d-proj-0~5119 3355596544)))))
(assert (= init-4-result-proj-11 (ite (or (or (= symbolic-d-proj-0~5119 167772204) (= symbolic-d-proj-0~5119 167772202)) (= symbolic-d-proj-0~5119 167772200)) true (and (= symbolic-d-proj-1~5118 24) (= symbolic-d-proj-0~5119 3355596544)))))
(assert (= assert-5-x-proj-0~5121 (ite (or (or (or (= symbolic-d-proj-0~5119 167772302) (= symbolic-d-proj-0~5119 167772300)) (= symbolic-d-proj-0~5119 167772298)) (= symbolic-d-proj-0~5119 167772304)) false (and (= symbolic-d-proj-1~5118 24) (= symbolic-d-proj-0~5119 3355590656)))))
(assert (= assert-5-b-proj-1~5143 (ite (or (or (or (= symbolic-d-proj-0~5119 167772302) (= symbolic-d-proj-0~5119 167772300)) (= symbolic-d-proj-0~5119 167772298)) (= symbolic-d-proj-0~5119 167772304)) 0 (ite (and (= symbolic-d-proj-1~5118 24) (= symbolic-d-proj-0~5119 3355590656)) 20 0))))
(assert (= assert-5-b-proj-7~5149 (ite (or (or (or (= symbolic-d-proj-0~5119 167772302) (= symbolic-d-proj-0~5119 167772300)) (= symbolic-d-proj-0~5119 167772298)) (= symbolic-d-proj-0~5119 167772304)) 0 (ite (and (= symbolic-d-proj-1~5118 24) (= symbolic-d-proj-0~5119 3355590656)) 100 0))))
(assert (= assert-5-b-proj-8~5150 (ite (or (or (or (= symbolic-d-proj-0~5119 167772302) (= symbolic-d-proj-0~5119 167772300)) (= symbolic-d-proj-0~5119 167772298)) (= symbolic-d-proj-0~5119 167772304)) 0 (ite (and (= symbolic-d-proj-1~5118 24) (= symbolic-d-proj-0~5119 3355590656)) 80 0))))
(assert (= assert-5-x-proj-10~5131 (ite (or (or (or (= symbolic-d-proj-0~5119 167772302) (= symbolic-d-proj-0~5119 167772300)) (= symbolic-d-proj-0~5119 167772298)) (= symbolic-d-proj-0~5119 167772304)) true (and (= symbolic-d-proj-1~5118 24) (= symbolic-d-proj-0~5119 3355590656)))))
(assert (= assert-5-x-proj-17~5138 (ite (or (or (or (= symbolic-d-proj-0~5119 167772302) (= symbolic-d-proj-0~5119 167772300)) (= symbolic-d-proj-0~5119 167772298)) (= symbolic-d-proj-0~5119 167772304)) true (and (= symbolic-d-proj-1~5118 24) (= symbolic-d-proj-0~5119 3355590656)))))
(assert (= assert-6-x-proj-0~5121 (ite (or (or (or (= symbolic-d-proj-0~5119 167772234) (= symbolic-d-proj-0~5119 167772328)) (= symbolic-d-proj-0~5119 167772324)) (= symbolic-d-proj-0~5119 167772354)) false (and (= symbolic-d-proj-1~5118 24) (= symbolic-d-proj-0~5119 3355590400)))))
(assert (= assert-6-b-proj-1~5143 (ite (or (or (or (= symbolic-d-proj-0~5119 167772234) (= symbolic-d-proj-0~5119 167772328)) (= symbolic-d-proj-0~5119 167772324)) (= symbolic-d-proj-0~5119 167772354)) 0 (ite (and (= symbolic-d-proj-1~5118 24) (= symbolic-d-proj-0~5119 3355590400)) 20 0))))
(assert (= assert-6-b-proj-7~5149 (ite (or (or (or (= symbolic-d-proj-0~5119 167772234) (= symbolic-d-proj-0~5119 167772328)) (= symbolic-d-proj-0~5119 167772324)) (= symbolic-d-proj-0~5119 167772354)) 0 (ite (and (= symbolic-d-proj-1~5118 24) (= symbolic-d-proj-0~5119 3355590400)) 100 0))))
(assert (= assert-6-b-proj-8~5150 (ite (or (or (or (= symbolic-d-proj-0~5119 167772234) (= symbolic-d-proj-0~5119 167772328)) (= symbolic-d-proj-0~5119 167772324)) (= symbolic-d-proj-0~5119 167772354)) 0 (ite (and (= symbolic-d-proj-1~5118 24) (= symbolic-d-proj-0~5119 3355590400)) 80 0))))
(assert (= assert-6-x-proj-10~5131 (ite (or (or (or (= symbolic-d-proj-0~5119 167772234) (= symbolic-d-proj-0~5119 167772328)) (= symbolic-d-proj-0~5119 167772324)) (= symbolic-d-proj-0~5119 167772354)) true (and (= symbolic-d-proj-1~5118 24) (= symbolic-d-proj-0~5119 3355590400)))))
(assert (= assert-6-x-proj-17~5138 (ite (or (or (or (= symbolic-d-proj-0~5119 167772234) (= symbolic-d-proj-0~5119 167772328)) (= symbolic-d-proj-0~5119 167772324)) (= symbolic-d-proj-0~5119 167772354)) true (and (= symbolic-d-proj-1~5118 24) (= symbolic-d-proj-0~5119 3355590400)))))
(assert (= assert-7-x-proj-0~5121 (ite (and (= symbolic-d-proj-1~5118 31) (= symbolic-d-proj-0~5119 167772258)) false (and (= symbolic-d-proj-1~5118 24) (= symbolic-d-proj-0~5119 3355595520)))))
(assert (= assert-7-b-proj-1~5143 (ite (and (= symbolic-d-proj-1~5118 31) (= symbolic-d-proj-0~5119 167772258)) 0 (ite (and (= symbolic-d-proj-1~5118 24) (= symbolic-d-proj-0~5119 3355595520)) 20 0))))
(assert (= assert-7-b-proj-7~5149 (ite (and (= symbolic-d-proj-1~5118 31) (= symbolic-d-proj-0~5119 167772258)) 0 (ite (and (= symbolic-d-proj-1~5118 24) (= symbolic-d-proj-0~5119 3355595520)) 100 0))))
(assert (= assert-7-b-proj-8~5150 (ite (and (= symbolic-d-proj-1~5118 31) (= symbolic-d-proj-0~5119 167772258)) 0 (ite (and (= symbolic-d-proj-1~5118 24) (= symbolic-d-proj-0~5119 3355595520)) 80 0))))
(assert (= assert-7-x-proj-10~5131 (ite (and (= symbolic-d-proj-1~5118 31) (= symbolic-d-proj-0~5119 167772258)) true (and (= symbolic-d-proj-1~5118 24) (= symbolic-d-proj-0~5119 3355595520)))))
(assert (= assert-7-x-proj-17~5138 (ite (and (= symbolic-d-proj-1~5118 31) (= symbolic-d-proj-0~5119 167772258)) true (and (= symbolic-d-proj-1~5118 24) (= symbolic-d-proj-0~5119 3355595520)))))
(assert (= init-8-result-proj-0 (ite (or (= symbolic-d-proj-0~5119 167772204) (= symbolic-d-proj-0~5119 167772304)) false (and (= symbolic-d-proj-1~5118 24) (= symbolic-d-proj-0~5119 3355594240)))))
(assert (= merge-8-1-b-proj-1~5254 (ite (or (= symbolic-d-proj-0~5119 167772204) (= symbolic-d-proj-0~5119 167772304)) 0 (ite (and (= symbolic-d-proj-1~5118 24) (= symbolic-d-proj-0~5119 3355594240)) 20 0))))
(assert (= merge-8-1-b-proj-7~5260 (ite (or (= symbolic-d-proj-0~5119 167772204) (= symbolic-d-proj-0~5119 167772304)) 0 (ite (and (= symbolic-d-proj-1~5118 24) (= symbolic-d-proj-0~5119 3355594240)) 100 0))))
(assert (= merge-8-1-b-proj-8~5261 (ite (or (= symbolic-d-proj-0~5119 167772204) (= symbolic-d-proj-0~5119 167772304)) 0 (ite (and (= symbolic-d-proj-1~5118 24) (= symbolic-d-proj-0~5119 3355594240)) 80 0))))
(assert (= init-8-result-proj-5 (ite (or (= symbolic-d-proj-0~5119 167772204) (= symbolic-d-proj-0~5119 167772304)) true (and (= symbolic-d-proj-1~5118 24) (= symbolic-d-proj-0~5119 3355594240)))))
(assert (= init-8-result-proj-11 (ite (or (= symbolic-d-proj-0~5119 167772204) (= symbolic-d-proj-0~5119 167772304)) true (and (= symbolic-d-proj-1~5118 24) (= symbolic-d-proj-0~5119 3355594240)))))
(assert (= init-9-result-proj-0 (ite (or (or (= symbolic-d-proj-0~5119 167772260) (= symbolic-d-proj-0~5119 167772210)) (= symbolic-d-proj-0~5119 167772258)) false (and (= symbolic-d-proj-1~5118 24) (= symbolic-d-proj-0~5119 3355592448)))))
(assert (= merge-9-1-b-proj-1~5254 (ite (or (or (= symbolic-d-proj-0~5119 167772260) (= symbolic-d-proj-0~5119 167772210)) (= symbolic-d-proj-0~5119 167772258)) 0 (ite (and (= symbolic-d-proj-1~5118 24) (= symbolic-d-proj-0~5119 3355592448)) 20 0))))
(assert (= merge-9-1-b-proj-7~5260 (ite (or (or (= symbolic-d-proj-0~5119 167772260) (= symbolic-d-proj-0~5119 167772210)) (= symbolic-d-proj-0~5119 167772258)) 0 (ite (and (= symbolic-d-proj-1~5118 24) (= symbolic-d-proj-0~5119 3355592448)) 100 0))))
(assert (= merge-9-1-b-proj-8~5261 (ite (or (or (= symbolic-d-proj-0~5119 167772260) (= symbolic-d-proj-0~5119 167772210)) (= symbolic-d-proj-0~5119 167772258)) 0 (ite (and (= symbolic-d-proj-1~5118 24) (= symbolic-d-proj-0~5119 3355592448)) 80 0))))
(assert (= init-9-result-proj-5 (ite (or (or (= symbolic-d-proj-0~5119 167772260) (= symbolic-d-proj-0~5119 167772210)) (= symbolic-d-proj-0~5119 167772258)) true (and (= symbolic-d-proj-1~5118 24) (= symbolic-d-proj-0~5119 3355592448)))))
(assert (= init-9-result-proj-11 (ite (or (or (= symbolic-d-proj-0~5119 167772260) (= symbolic-d-proj-0~5119 167772210)) (= symbolic-d-proj-0~5119 167772258)) true (and (= symbolic-d-proj-1~5118 24) (= symbolic-d-proj-0~5119 3355592448)))))
(assert (= assert-10-x-proj-0~5121 (ite (or (or (= symbolic-d-proj-0~5119 167772238) (= symbolic-d-proj-0~5119 167772202)) (= symbolic-d-proj-0~5119 167772226)) false (and (= symbolic-d-proj-1~5118 24) (= symbolic-d-proj-0~5119 3355589120)))))
(assert (= assert-10-b-proj-1~5143 (ite (or (or (= symbolic-d-proj-0~5119 167772238) (= symbolic-d-proj-0~5119 167772202)) (= symbolic-d-proj-0~5119 167772226)) 0 (ite (and (= symbolic-d-proj-1~5118 24) (= symbolic-d-proj-0~5119 3355589120)) 20 0))))
(assert (= assert-10-b-proj-7~5149 (ite (or (or (= symbolic-d-proj-0~5119 167772238) (= symbolic-d-proj-0~5119 167772202)) (= symbolic-d-proj-0~5119 167772226)) 0 (ite (and (= symbolic-d-proj-1~5118 24) (= symbolic-d-proj-0~5119 3355589120)) 100 0))))
(assert (= assert-10-b-proj-8~5150 (ite (or (or (= symbolic-d-proj-0~5119 167772238) (= symbolic-d-proj-0~5119 167772202)) (= symbolic-d-proj-0~5119 167772226)) 0 (ite (and (= symbolic-d-proj-1~5118 24) (= symbolic-d-proj-0~5119 3355589120)) 80 0))))
(assert (= assert-10-x-proj-10~5131 (ite (or (or (= symbolic-d-proj-0~5119 167772238) (= symbolic-d-proj-0~5119 167772202)) (= symbolic-d-proj-0~5119 167772226)) true (and (= symbolic-d-proj-1~5118 24) (= symbolic-d-proj-0~5119 3355589120)))))
(assert (= assert-10-x-proj-17~5138 (ite (or (or (= symbolic-d-proj-0~5119 167772238) (= symbolic-d-proj-0~5119 167772202)) (= symbolic-d-proj-0~5119 167772226)) true (and (= symbolic-d-proj-1~5118 24) (= symbolic-d-proj-0~5119 3355589120)))))
(assert (= init-11-result-proj-0 (ite (or (or (or (= symbolic-d-proj-0~5119 167772334) (= symbolic-d-proj-0~5119 167772284)) (= symbolic-d-proj-0~5119 167772298)) (= symbolic-d-proj-0~5119 167772326)) false (and (= symbolic-d-proj-1~5118 24) (= symbolic-d-proj-0~5119 3355595776)))))
(assert (= merge-11-1-b-proj-1~5254 (ite (or (or (or (= symbolic-d-proj-0~5119 167772334) (= symbolic-d-proj-0~5119 167772284)) (= symbolic-d-proj-0~5119 167772298)) (= symbolic-d-proj-0~5119 167772326)) 0 (ite (and (= symbolic-d-proj-1~5118 24) (= symbolic-d-proj-0~5119 3355595776)) 20 0))))
(assert (= merge-11-1-b-proj-7~5260 (ite (or (or (or (= symbolic-d-proj-0~5119 167772334) (= symbolic-d-proj-0~5119 167772284)) (= symbolic-d-proj-0~5119 167772298)) (= symbolic-d-proj-0~5119 167772326)) 0 (ite (and (= symbolic-d-proj-1~5118 24) (= symbolic-d-proj-0~5119 3355595776)) 100 0))))
(assert (= merge-11-1-b-proj-8~5261 (ite (or (or (or (= symbolic-d-proj-0~5119 167772334) (= symbolic-d-proj-0~5119 167772284)) (= symbolic-d-proj-0~5119 167772298)) (= symbolic-d-proj-0~5119 167772326)) 0 (ite (and (= symbolic-d-proj-1~5118 24) (= symbolic-d-proj-0~5119 3355595776)) 80 0))))
(assert (= init-11-result-proj-5 (ite (or (or (or (= symbolic-d-proj-0~5119 167772334) (= symbolic-d-proj-0~5119 167772284)) (= symbolic-d-proj-0~5119 167772298)) (= symbolic-d-proj-0~5119 167772326)) true (and (= symbolic-d-proj-1~5118 24) (= symbolic-d-proj-0~5119 3355595776)))))
(assert (= init-11-result-proj-11 (ite (or (or (or (= symbolic-d-proj-0~5119 167772334) (= symbolic-d-proj-0~5119 167772284)) (= symbolic-d-proj-0~5119 167772298)) (= symbolic-d-proj-0~5119 167772326)) true (and (= symbolic-d-proj-1~5118 24) (= symbolic-d-proj-0~5119 3355595776)))))
(assert (= init-12-result-proj-0 (ite (or (or (= symbolic-d-proj-0~5119 167772212) (= symbolic-d-proj-0~5119 167772242)) (= symbolic-d-proj-0~5119 167772240)) false (and (= symbolic-d-proj-1~5118 24) (= symbolic-d-proj-0~5119 3355600640)))))
(assert (= merge-12-1-b-proj-1~5254 (ite (or (or (= symbolic-d-proj-0~5119 167772212) (= symbolic-d-proj-0~5119 167772242)) (= symbolic-d-proj-0~5119 167772240)) 0 (ite (and (= symbolic-d-proj-1~5118 24) (= symbolic-d-proj-0~5119 3355600640)) 20 0))))
(assert (= merge-12-1-b-proj-7~5260 (ite (or (or (= symbolic-d-proj-0~5119 167772212) (= symbolic-d-proj-0~5119 167772242)) (= symbolic-d-proj-0~5119 167772240)) 0 (ite (and (= symbolic-d-proj-1~5118 24) (= symbolic-d-proj-0~5119 3355600640)) 100 0))))
(assert (= merge-12-1-b-proj-8~5261 (ite (or (or (= symbolic-d-proj-0~5119 167772212) (= symbolic-d-proj-0~5119 167772242)) (= symbolic-d-proj-0~5119 167772240)) 0 (ite (and (= symbolic-d-proj-1~5118 24) (= symbolic-d-proj-0~5119 3355600640)) 80 0))))
(assert (= init-12-result-proj-5 (ite (or (or (= symbolic-d-proj-0~5119 167772212) (= symbolic-d-proj-0~5119 167772242)) (= symbolic-d-proj-0~5119 167772240)) true (and (= symbolic-d-proj-1~5118 24) (= symbolic-d-proj-0~5119 3355600640)))))
(assert (= init-12-result-proj-11 (ite (or (or (= symbolic-d-proj-0~5119 167772212) (= symbolic-d-proj-0~5119 167772242)) (= symbolic-d-proj-0~5119 167772240)) true (and (= symbolic-d-proj-1~5118 24) (= symbolic-d-proj-0~5119 3355600640)))))
(assert (= assert-13-x-proj-0~5121 (ite (or (or (= symbolic-d-proj-0~5119 167772248) (= symbolic-d-proj-0~5119 167772230)) (= symbolic-d-proj-0~5119 167772198)) false (and (= symbolic-d-proj-1~5118 24) (= symbolic-d-proj-0~5119 3355587840)))))
(assert (= assert-13-b-proj-1~5143 (ite (or (or (= symbolic-d-proj-0~5119 167772248) (= symbolic-d-proj-0~5119 167772230)) (= symbolic-d-proj-0~5119 167772198)) 0 (ite (and (= symbolic-d-proj-1~5118 24) (= symbolic-d-proj-0~5119 3355587840)) 20 0))))
(assert (= assert-13-b-proj-7~5149 (ite (or (or (= symbolic-d-proj-0~5119 167772248) (= symbolic-d-proj-0~5119 167772230)) (= symbolic-d-proj-0~5119 167772198)) 0 (ite (and (= symbolic-d-proj-1~5118 24) (= symbolic-d-proj-0~5119 3355587840)) 100 0))))
(assert (= assert-13-b-proj-8~5150 (ite (or (or (= symbolic-d-proj-0~5119 167772248) (= symbolic-d-proj-0~5119 167772230)) (= symbolic-d-proj-0~5119 167772198)) 0 (ite (and (= symbolic-d-proj-1~5118 24) (= symbolic-d-proj-0~5119 3355587840)) 80 0))))
(assert (= assert-13-x-proj-10~5131 (ite (or (or (= symbolic-d-proj-0~5119 167772248) (= symbolic-d-proj-0~5119 167772230)) (= symbolic-d-proj-0~5119 167772198)) true (and (= symbolic-d-proj-1~5118 24) (= symbolic-d-proj-0~5119 3355587840)))))
(assert (= assert-13-x-proj-17~5138 (ite (or (or (= symbolic-d-proj-0~5119 167772248) (= symbolic-d-proj-0~5119 167772230)) (= symbolic-d-proj-0~5119 167772198)) true (and (= symbolic-d-proj-1~5118 24) (= symbolic-d-proj-0~5119 3355587840)))))
(assert (= assert-14-x-proj-0~5121 (ite (or (or (= symbolic-d-proj-0~5119 167772246) (= symbolic-d-proj-0~5119 167772166)) (= symbolic-d-proj-0~5119 167772244)) false (and (= symbolic-d-proj-1~5118 24) (= symbolic-d-proj-0~5119 3355588096)))))
(assert (= assert-14-b-proj-1~5143 (ite (or (or (= symbolic-d-proj-0~5119 167772246) (= symbolic-d-proj-0~5119 167772166)) (= symbolic-d-proj-0~5119 167772244)) 0 (ite (and (= symbolic-d-proj-1~5118 24) (= symbolic-d-proj-0~5119 3355588096)) 20 0))))
(assert (= assert-14-b-proj-7~5149 (ite (or (or (= symbolic-d-proj-0~5119 167772246) (= symbolic-d-proj-0~5119 167772166)) (= symbolic-d-proj-0~5119 167772244)) 0 (ite (and (= symbolic-d-proj-1~5118 24) (= symbolic-d-proj-0~5119 3355588096)) 100 0))))
(assert (= assert-14-b-proj-8~5150 (ite (or (or (= symbolic-d-proj-0~5119 167772246) (= symbolic-d-proj-0~5119 167772166)) (= symbolic-d-proj-0~5119 167772244)) 0 (ite (and (= symbolic-d-proj-1~5118 24) (= symbolic-d-proj-0~5119 3355588096)) 80 0))))
(assert (= assert-14-x-proj-10~5131 (ite (or (or (= symbolic-d-proj-0~5119 167772246) (= symbolic-d-proj-0~5119 167772166)) (= symbolic-d-proj-0~5119 167772244)) true (and (= symbolic-d-proj-1~5118 24) (= symbolic-d-proj-0~5119 3355588096)))))
(assert (= assert-14-x-proj-17~5138 (ite (or (or (= symbolic-d-proj-0~5119 167772246) (= symbolic-d-proj-0~5119 167772166)) (= symbolic-d-proj-0~5119 167772244)) true (and (= symbolic-d-proj-1~5118 24) (= symbolic-d-proj-0~5119 3355588096)))))
(assert (= init-15-result-proj-0 (ite (or (= symbolic-d-proj-0~5119 167772168) (= symbolic-d-proj-0~5119 167772166)) false (and (= symbolic-d-proj-1~5118 24) (= symbolic-d-proj-0~5119 3355594752)))))
(assert (= merge-15-1-b-proj-1~5254 (ite (or (= symbolic-d-proj-0~5119 167772168) (= symbolic-d-proj-0~5119 167772166)) 0 (ite (and (= symbolic-d-proj-1~5118 24) (= symbolic-d-proj-0~5119 3355594752)) 20 0))))
(assert (= merge-15-1-b-proj-7~5260 (ite (or (= symbolic-d-proj-0~5119 167772168) (= symbolic-d-proj-0~5119 167772166)) 0 (ite (and (= symbolic-d-proj-1~5118 24) (= symbolic-d-proj-0~5119 3355594752)) 100 0))))
(assert (= merge-15-1-b-proj-8~5261 (ite (or (= symbolic-d-proj-0~5119 167772168) (= symbolic-d-proj-0~5119 167772166)) 0 (ite (and (= symbolic-d-proj-1~5118 24) (= symbolic-d-proj-0~5119 3355594752)) 80 0))))
(assert (= init-15-result-proj-5 (ite (or (= symbolic-d-proj-0~5119 167772168) (= symbolic-d-proj-0~5119 167772166)) true (and (= symbolic-d-proj-1~5118 24) (= symbolic-d-proj-0~5119 3355594752)))))
(assert (= init-15-result-proj-11 (ite (or (= symbolic-d-proj-0~5119 167772168) (= symbolic-d-proj-0~5119 167772166)) true (and (= symbolic-d-proj-1~5118 24) (= symbolic-d-proj-0~5119 3355594752)))))
(assert (= assert-16-x-proj-0~5121 (ite (or (or (or (or (= symbolic-d-proj-0~5119 167772350) (= symbolic-d-proj-0~5119 167772344)) (= symbolic-d-proj-0~5119 167772354)) (= symbolic-d-proj-0~5119 167772352)) (= symbolic-d-proj-0~5119 167772240)) false (and (= symbolic-d-proj-1~5118 24) (= symbolic-d-proj-0~5119 3355583744)))))
(assert (= assert-16-b-proj-1~5143 (ite (or (or (or (or (= symbolic-d-proj-0~5119 167772350) (= symbolic-d-proj-0~5119 167772344)) (= symbolic-d-proj-0~5119 167772354)) (= symbolic-d-proj-0~5119 167772352)) (= symbolic-d-proj-0~5119 167772240)) 0 (ite (and (= symbolic-d-proj-1~5118 24) (= symbolic-d-proj-0~5119 3355583744)) 20 0))))
(assert (= assert-16-b-proj-7~5149 (ite (or (or (or (or (= symbolic-d-proj-0~5119 167772350) (= symbolic-d-proj-0~5119 167772344)) (= symbolic-d-proj-0~5119 167772354)) (= symbolic-d-proj-0~5119 167772352)) (= symbolic-d-proj-0~5119 167772240)) 0 (ite (and (= symbolic-d-proj-1~5118 24) (= symbolic-d-proj-0~5119 3355583744)) 100 0))))
(assert (= assert-16-b-proj-8~5150 (ite (or (or (or (or (= symbolic-d-proj-0~5119 167772350) (= symbolic-d-proj-0~5119 167772344)) (= symbolic-d-proj-0~5119 167772354)) (= symbolic-d-proj-0~5119 167772352)) (= symbolic-d-proj-0~5119 167772240)) 0 (ite (and (= symbolic-d-proj-1~5118 24) (= symbolic-d-proj-0~5119 3355583744)) 80 0))))
(assert (= assert-16-x-proj-10~5131 (ite (or (or (or (or (= symbolic-d-proj-0~5119 167772350) (= symbolic-d-proj-0~5119 167772344)) (= symbolic-d-proj-0~5119 167772354)) (= symbolic-d-proj-0~5119 167772352)) (= symbolic-d-proj-0~5119 167772240)) true (and (= symbolic-d-proj-1~5118 24) (= symbolic-d-proj-0~5119 3355583744)))))
(assert (= assert-16-x-proj-17~5138 (ite (or (or (or (or (= symbolic-d-proj-0~5119 167772350) (= symbolic-d-proj-0~5119 167772344)) (= symbolic-d-proj-0~5119 167772354)) (= symbolic-d-proj-0~5119 167772352)) (= symbolic-d-proj-0~5119 167772240)) true (and (= symbolic-d-proj-1~5118 24) (= symbolic-d-proj-0~5119 3355583744)))))
(assert (= trans-0-1-b-proj-0~5412 (ite (= assert-0-x-proj-17~5138 false) false (ite (= assert-0-x-proj-17~5138 true) true assert-0-x-proj-0~5121))))
(assert (= trans-0-1-b-proj-0~5422 0))
(assert (= trans-0-1-b-proj-1~5423 (ite (= assert-0-x-proj-17~5138 false) 0 (ite (= assert-0-x-proj-17~5138 true) 0 assert-0-b-proj-1~5143))))
(assert (= trans-0-1-b-proj-7~5429 (ite (= assert-0-x-proj-17~5138 false) 0 (ite (= assert-0-x-proj-17~5138 true) 100 assert-0-b-proj-7~5149))))
(assert (= trans-0-1-b-proj-8~5430 (ite (= assert-0-x-proj-17~5138 false) 0 (ite (= assert-0-x-proj-17~5138 true) 80 assert-0-b-proj-8~5150))))
(assert (= trans-0-1-b-proj-0~5365 (ite (= trans-0-1-b-proj-0~5412 false) false (and (= symbolic-d-proj-1~5118 24) (and (<= 3355585280 symbolic-d-proj-0~5119) (< symbolic-d-proj-0~5119 3355585536))))))
(assert (= trans-0-1-b-proj-0~5375 (ite (= trans-0-1-b-proj-0~5412 false) 0 (ite (and (= symbolic-d-proj-1~5118 24) (and (<= 3355585280 symbolic-d-proj-0~5119) (< symbolic-d-proj-0~5119 3355585536))) (+ trans-0-1-b-proj-0~5422 1) 0))))
(assert (= trans-0-1-b-proj-1~5376 (ite (= trans-0-1-b-proj-0~5412 false) 0 (ite (and (= symbolic-d-proj-1~5118 24) (and (<= 3355585280 symbolic-d-proj-0~5119) (< symbolic-d-proj-0~5119 3355585536))) trans-0-1-b-proj-1~5423 0))))
(assert (= trans-0-1-b-proj-2~5377 false))
(assert (= trans-0-1-b-proj-3~5378 false))
(assert (= trans-0-1-b-proj-4~5379 false))
(assert (= trans-0-1-b-proj-5~5380 false))
(assert (= trans-0-1-b-proj-6~5381 false))
(assert (= trans-0-1-b-proj-7~5382 (ite (= trans-0-1-b-proj-0~5412 false) 0 (ite (and (= symbolic-d-proj-1~5118 24) (and (<= 3355585280 symbolic-d-proj-0~5119) (< symbolic-d-proj-0~5119 3355585536))) trans-0-1-b-proj-7~5429 0))))
(assert (= trans-0-1-b-proj-8~5383 (ite (= trans-0-1-b-proj-0~5412 false) 0 (ite (and (= symbolic-d-proj-1~5118 24) (and (<= 3355585280 symbolic-d-proj-0~5119) (< symbolic-d-proj-0~5119 3355585536))) trans-0-1-b-proj-8~5430 0))))
(assert (= trans-0-1-result-proj-0 (ite (= trans-0-1-b-proj-0~5365 false) false (ite (and (= symbolic-d-proj-1~5118 24) (and (<= 2147486208 symbolic-d-proj-0~5119) (< symbolic-d-proj-0~5119 2147486464))) true (not (and (= symbolic-d-proj-1~5118 20) (and (<= 2147483648 symbolic-d-proj-0~5119) (< symbolic-d-proj-0~5119 2147487744))))))))
(assert (= merge-1-1-a-proj-0~5244 (ite (= trans-0-1-b-proj-0~5365 false) 0 (ite (and (= symbolic-d-proj-1~5118 24) (and (<= 2147486208 symbolic-d-proj-0~5119) (< symbolic-d-proj-0~5119 2147486464))) trans-0-1-b-proj-0~5375 (ite (and (= symbolic-d-proj-1~5118 20) (and (<= 2147483648 symbolic-d-proj-0~5119) (< symbolic-d-proj-0~5119 2147487744))) 0 trans-0-1-b-proj-0~5375)))))
(assert (= merge-1-1-a-proj-1~5245 (ite (= trans-0-1-b-proj-0~5365 false) 0 (ite (and (= symbolic-d-proj-1~5118 24) (and (<= 2147486208 symbolic-d-proj-0~5119) (< symbolic-d-proj-0~5119 2147486464))) trans-0-1-b-proj-1~5376 (ite (and (= symbolic-d-proj-1~5118 20) (and (<= 2147483648 symbolic-d-proj-0~5119) (< symbolic-d-proj-0~5119 2147487744))) 0 trans-0-1-b-proj-1~5376)))))
(assert (= trans-0-1-b-proj-3~5356 (ite (= trans-0-1-b-proj-0~5365 false) false (ite (and (= symbolic-d-proj-1~5118 24) (and (<= 2147486208 symbolic-d-proj-0~5119) (< symbolic-d-proj-0~5119 2147486464))) true (ite (and (= symbolic-d-proj-1~5118 20) (and (<= 2147483648 symbolic-d-proj-0~5119) (< symbolic-d-proj-0~5119 2147487744))) false trans-0-1-b-proj-2~5377)))))
(assert (= trans-0-1-b-proj-4~5357 (ite (= trans-0-1-b-proj-0~5365 false) false (ite (and (= symbolic-d-proj-1~5118 24) (and (<= 2147486208 symbolic-d-proj-0~5119) (< symbolic-d-proj-0~5119 2147486464))) trans-0-1-b-proj-3~5378 (ite (and (= symbolic-d-proj-1~5118 20) (and (<= 2147483648 symbolic-d-proj-0~5119) (< symbolic-d-proj-0~5119 2147487744))) false trans-0-1-b-proj-3~5378)))))
(assert (= trans-0-1-b-proj-5~5358 (ite (= trans-0-1-b-proj-0~5365 false) false (ite (and (= symbolic-d-proj-1~5118 24) (and (<= 2147486208 symbolic-d-proj-0~5119) (< symbolic-d-proj-0~5119 2147486464))) trans-0-1-b-proj-4~5379 (ite (and (= symbolic-d-proj-1~5118 20) (and (<= 2147483648 symbolic-d-proj-0~5119) (< symbolic-d-proj-0~5119 2147487744))) false trans-0-1-b-proj-4~5379)))))
(assert (= trans-0-1-b-proj-6~5359 (ite (= trans-0-1-b-proj-0~5365 false) false (ite (and (= symbolic-d-proj-1~5118 24) (and (<= 2147486208 symbolic-d-proj-0~5119) (< symbolic-d-proj-0~5119 2147486464))) trans-0-1-b-proj-5~5380 (ite (and (= symbolic-d-proj-1~5118 20) (and (<= 2147483648 symbolic-d-proj-0~5119) (< symbolic-d-proj-0~5119 2147487744))) false trans-0-1-b-proj-5~5380)))))
(assert (= trans-0-1-b-proj-7~5360 (ite (= trans-0-1-b-proj-0~5365 false) false (ite (and (= symbolic-d-proj-1~5118 24) (and (<= 2147486208 symbolic-d-proj-0~5119) (< symbolic-d-proj-0~5119 2147486464))) trans-0-1-b-proj-6~5381 (ite (and (= symbolic-d-proj-1~5118 20) (and (<= 2147483648 symbolic-d-proj-0~5119) (< symbolic-d-proj-0~5119 2147487744))) false trans-0-1-b-proj-6~5381)))))
(assert (= merge-1-1-a-proj-7~5251 (ite (= trans-0-1-b-proj-0~5365 false) 0 (ite (and (= symbolic-d-proj-1~5118 24) (and (<= 2147486208 symbolic-d-proj-0~5119) (< symbolic-d-proj-0~5119 2147486464))) 1 (ite (and (= symbolic-d-proj-1~5118 20) (and (<= 2147483648 symbolic-d-proj-0~5119) (< symbolic-d-proj-0~5119 2147487744))) 0 trans-0-1-b-proj-7~5382)))))
(assert (= merge-1-1-a-proj-8~5252 (ite (= trans-0-1-b-proj-0~5365 false) 0 (ite (and (= symbolic-d-proj-1~5118 24) (and (<= 2147486208 symbolic-d-proj-0~5119) (< symbolic-d-proj-0~5119 2147486464))) trans-0-1-b-proj-8~5383 (ite (and (= symbolic-d-proj-1~5118 20) (and (<= 2147483648 symbolic-d-proj-0~5119) (< symbolic-d-proj-0~5119 2147487744))) 0 trans-0-1-b-proj-8~5383)))))
(assert (= trans-4-8-b-proj-0~5606 (ite (= assert-4-x-proj-17~5138 false) false (ite (and (= trans-4-8-y~5639 0) (= assert-4-x-proj-17~5138 true)) true (ite (and (= trans-4-8-y~5639 1) (= assert-4-x-proj-17~5138 true)) true (ite (and (= trans-4-8-y~5639 2) (= assert-4-x-proj-17~5138 true)) true assert-4-x-proj-0~5121))))))
(assert (= trans-4-8-b-proj-0~5616 (ite (= assert-4-x-proj-17~5138 false) 0 (ite (and (= trans-4-8-y~5639 0) (= assert-4-x-proj-17~5138 true)) 0 (ite (and (= trans-4-8-y~5639 1) (= assert-4-x-proj-17~5138 true)) 0 (ite (and (= trans-4-8-y~5639 2) (= assert-4-x-proj-17~5138 true)) 0 merge-4-2-b-proj-0~5231))))))
(assert (= trans-4-8-b-proj-1~5617 (ite (= assert-4-x-proj-17~5138 false) 0 (ite (and (= trans-4-8-y~5639 0) (= assert-4-x-proj-17~5138 true)) 0 (ite (and (= trans-4-8-y~5639 1) (= assert-4-x-proj-17~5138 true)) 1 (ite (and (= trans-4-8-y~5639 2) (= assert-4-x-proj-17~5138 true)) 110 merge-4-2-b-proj-1~5232))))))
(assert (= trans-4-8-b-proj-7~5623 (ite (= assert-4-x-proj-17~5138 false) 0 (ite (and (= trans-4-8-y~5639 0) (= assert-4-x-proj-17~5138 true)) 100 (ite (and (= trans-4-8-y~5639 1) (= assert-4-x-proj-17~5138 true)) 100 (ite (and (= trans-4-8-y~5639 2) (= assert-4-x-proj-17~5138 true)) 100 merge-4-2-b-proj-7~5238))))))
(assert (= trans-4-8-b-proj-8~5624 (ite (= assert-4-x-proj-17~5138 false) 0 (ite (and (= trans-4-8-y~5639 0) (= assert-4-x-proj-17~5138 true)) 80 (ite (and (= trans-4-8-y~5639 1) (= assert-4-x-proj-17~5138 true)) 80 (ite (and (= trans-4-8-y~5639 2) (= assert-4-x-proj-17~5138 true)) 80 merge-4-2-b-proj-8~5239))))))
(assert (= trans-4-8-b-proj-0~5573 (ite (= trans-4-8-b-proj-0~5606 false) false (ite (and (= symbolic-d-proj-1~5118 24) (and (<= 3355596544 symbolic-d-proj-0~5119) (< symbolic-d-proj-0~5119 3355596800))) true (ite (= assert-4-x-proj-17~5138 false) false (= 3 trans-4-8-y~5639))))))
(assert (= trans-4-8-b-proj-0~5583 (ite (= trans-4-8-b-proj-0~5606 false) 0 (ite (and (= symbolic-d-proj-1~5118 24) (and (<= 3355596544 symbolic-d-proj-0~5119) (< symbolic-d-proj-0~5119 3355596800))) (+ trans-4-8-b-proj-0~5616 1) (ite (ite (= assert-4-x-proj-17~5138 false) false (= 3 trans-4-8-y~5639)) (+ trans-4-8-b-proj-0~5616 1) 0)))))
(assert (= trans-4-8-b-proj-1~5584 (ite (= trans-4-8-b-proj-0~5606 false) 0 (ite (and (= symbolic-d-proj-1~5118 24) (and (<= 3355596544 symbolic-d-proj-0~5119) (< symbolic-d-proj-0~5119 3355596800))) trans-4-8-b-proj-1~5617 (ite (ite (= assert-4-x-proj-17~5138 false) false (= 3 trans-4-8-y~5639)) trans-4-8-b-proj-1~5617 0)))))
(assert (= trans-4-8-b-proj-2~5585 false))
(assert (= trans-4-8-b-proj-3~5586 false))
(assert (= trans-4-8-b-proj-4~5587 false))
(assert (= trans-4-8-b-proj-5~5588 false))
(assert (= trans-4-8-b-proj-6~5589 false))
(assert (= trans-4-8-b-proj-7~5590 (ite (= trans-4-8-b-proj-0~5606 false) 0 (ite (and (= symbolic-d-proj-1~5118 24) (and (<= 3355596544 symbolic-d-proj-0~5119) (< symbolic-d-proj-0~5119 3355596800))) trans-4-8-b-proj-7~5623 (ite (ite (= assert-4-x-proj-17~5138 false) false (= 3 trans-4-8-y~5639)) trans-4-8-b-proj-7~5623 0)))))
(assert (= trans-4-8-b-proj-8~5591 (ite (= trans-4-8-b-proj-0~5606 false) 0 (ite (and (= symbolic-d-proj-1~5118 24) (and (<= 3355596544 symbolic-d-proj-0~5119) (< symbolic-d-proj-0~5119 3355596800))) trans-4-8-b-proj-8~5624 (ite (ite (= assert-4-x-proj-17~5138 false) false (= 3 trans-4-8-y~5639)) trans-4-8-b-proj-8~5624 0)))))
(assert (= trans-4-8-result-proj-0 (ite (= trans-4-8-b-proj-0~5573 false) false (not (and (= symbolic-d-proj-1~5118 20) (and (<= 2147483648 symbolic-d-proj-0~5119) (< symbolic-d-proj-0~5119 2147487744)))))))
(assert (= merge-8-1-a-proj-0~5244 (ite (= trans-4-8-b-proj-0~5573 false) 0 (ite (and (= symbolic-d-proj-1~5118 20) (and (<= 2147483648 symbolic-d-proj-0~5119) (< symbolic-d-proj-0~5119 2147487744))) 0 trans-4-8-b-proj-0~5583))))
(assert (= merge-8-1-a-proj-1~5245 (ite (= trans-4-8-b-proj-0~5573 false) 0 (ite (and (= symbolic-d-proj-1~5118 20) (and (<= 2147483648 symbolic-d-proj-0~5119) (< symbolic-d-proj-0~5119 2147487744))) 0 trans-4-8-b-proj-1~5584))))
(assert (= trans-4-8-b-proj-3~5356 (ite (= trans-4-8-b-proj-0~5573 false) false (ite (and (= symbolic-d-proj-1~5118 20) (and (<= 2147483648 symbolic-d-proj-0~5119) (< symbolic-d-proj-0~5119 2147487744))) false trans-4-8-b-proj-2~5585))))
(assert (= trans-4-8-b-proj-4~5357 (ite (= trans-4-8-b-proj-0~5573 false) false (ite (and (= symbolic-d-proj-1~5118 20) (and (<= 2147483648 symbolic-d-proj-0~5119) (< symbolic-d-proj-0~5119 2147487744))) false trans-4-8-b-proj-3~5586))))
(assert (= trans-4-8-b-proj-5~5358 (ite (= trans-4-8-b-proj-0~5573 false) false (ite (and (= symbolic-d-proj-1~5118 20) (and (<= 2147483648 symbolic-d-proj-0~5119) (< symbolic-d-proj-0~5119 2147487744))) false trans-4-8-b-proj-4~5587))))
(assert (= trans-4-8-b-proj-6~5359 (ite (= trans-4-8-b-proj-0~5573 false) false (ite (and (= symbolic-d-proj-1~5118 20) (and (<= 2147483648 symbolic-d-proj-0~5119) (< symbolic-d-proj-0~5119 2147487744))) false trans-4-8-b-proj-5~5588))))
(assert (= trans-4-8-b-proj-7~5360 (ite (= trans-4-8-b-proj-0~5573 false) false (ite (and (= symbolic-d-proj-1~5118 20) (and (<= 2147483648 symbolic-d-proj-0~5119) (< symbolic-d-proj-0~5119 2147487744))) false trans-4-8-b-proj-6~5589))))
(assert (= merge-8-1-a-proj-7~5251 (ite (= trans-4-8-b-proj-0~5573 false) 0 (ite (and (= symbolic-d-proj-1~5118 20) (and (<= 2147483648 symbolic-d-proj-0~5119) (< symbolic-d-proj-0~5119 2147487744))) 0 trans-4-8-b-proj-7~5590))))
(assert (= merge-8-1-a-proj-8~5252 (ite (= trans-4-8-b-proj-0~5573 false) 0 (ite (and (= symbolic-d-proj-1~5118 20) (and (<= 2147483648 symbolic-d-proj-0~5119) (< symbolic-d-proj-0~5119 2147487744))) 0 trans-4-8-b-proj-8~5591))))
(assert (= trans-5-11-b-proj-0~5689 (ite (= assert-5-x-proj-17~5138 false) false (ite (= assert-5-x-proj-17~5138 true) true assert-5-x-proj-0~5121))))
(assert (= trans-5-11-b-proj-0~5699 0))
(assert (= trans-5-11-b-proj-1~5700 (ite (= assert-5-x-proj-17~5138 false) 0 (ite (= assert-5-x-proj-17~5138 true) 0 assert-5-b-proj-1~5143))))
(assert (= trans-5-11-b-proj-7~5706 (ite (= assert-5-x-proj-17~5138 false) 0 (ite (= assert-5-x-proj-17~5138 true) 100 assert-5-b-proj-7~5149))))
(assert (= trans-5-11-b-proj-8~5707 (ite (= assert-5-x-proj-17~5138 false) 0 (ite (= assert-5-x-proj-17~5138 true) 80 assert-5-b-proj-8~5150))))
(assert (= trans-5-11-b-proj-0~5656 (ite (= trans-5-11-b-proj-0~5689 false) false (and (= symbolic-d-proj-1~5118 24) (and (<= 3355590656 symbolic-d-proj-0~5119) (< symbolic-d-proj-0~5119 3355590912))))))
(assert (= trans-5-11-b-proj-0~5666 (ite (= trans-5-11-b-proj-0~5689 false) 0 (ite (and (= symbolic-d-proj-1~5118 24) (and (<= 3355590656 symbolic-d-proj-0~5119) (< symbolic-d-proj-0~5119 3355590912))) (+ trans-5-11-b-proj-0~5699 1) 0))))
(assert (= trans-5-11-b-proj-1~5667 (ite (= trans-5-11-b-proj-0~5689 false) 0 (ite (and (= symbolic-d-proj-1~5118 24) (and (<= 3355590656 symbolic-d-proj-0~5119) (< symbolic-d-proj-0~5119 3355590912))) trans-5-11-b-proj-1~5700 0))))
(assert (= trans-5-11-b-proj-2~5668 false))
(assert (= trans-5-11-b-proj-3~5669 false))
(assert (= trans-5-11-b-proj-4~5670 false))
(assert (= trans-5-11-b-proj-5~5671 false))
(assert (= trans-5-11-b-proj-6~5672 false))
(assert (= trans-5-11-b-proj-7~5673 (ite (= trans-5-11-b-proj-0~5689 false) 0 (ite (and (= symbolic-d-proj-1~5118 24) (and (<= 3355590656 symbolic-d-proj-0~5119) (< symbolic-d-proj-0~5119 3355590912))) trans-5-11-b-proj-7~5706 0))))
(assert (= trans-5-11-b-proj-8~5674 (ite (= trans-5-11-b-proj-0~5689 false) 0 (ite (and (= symbolic-d-proj-1~5118 24) (and (<= 3355590656 symbolic-d-proj-0~5119) (< symbolic-d-proj-0~5119 3355590912))) trans-5-11-b-proj-8~5707 0))))
(assert (= trans-5-11-result-proj-0 (ite (= trans-5-11-b-proj-0~5656 false) false (not (and (= symbolic-d-proj-1~5118 20) (and (<= 2147483648 symbolic-d-proj-0~5119) (< symbolic-d-proj-0~5119 2147487744)))))))
(assert (= merge-11-1-a-proj-0~5244 (ite (= trans-5-11-b-proj-0~5656 false) 0 (ite (and (= symbolic-d-proj-1~5118 20) (and (<= 2147483648 symbolic-d-proj-0~5119) (< symbolic-d-proj-0~5119 2147487744))) 0 trans-5-11-b-proj-0~5666))))
(assert (= merge-11-1-a-proj-1~5245 (ite (= trans-5-11-b-proj-0~5656 false) 0 (ite (and (= symbolic-d-proj-1~5118 20) (and (<= 2147483648 symbolic-d-proj-0~5119) (< symbolic-d-proj-0~5119 2147487744))) 0 trans-5-11-b-proj-1~5667))))
(assert (= trans-5-11-b-proj-3~5356 (ite (= trans-5-11-b-proj-0~5656 false) false (ite (and (= symbolic-d-proj-1~5118 20) (and (<= 2147483648 symbolic-d-proj-0~5119) (< symbolic-d-proj-0~5119 2147487744))) false trans-5-11-b-proj-2~5668))))
(assert (= trans-5-11-b-proj-4~5357 (ite (= trans-5-11-b-proj-0~5656 false) false (ite (and (= symbolic-d-proj-1~5118 20) (and (<= 2147483648 symbolic-d-proj-0~5119) (< symbolic-d-proj-0~5119 2147487744))) false trans-5-11-b-proj-3~5669))))
(assert (= trans-5-11-b-proj-5~5358 (ite (= trans-5-11-b-proj-0~5656 false) false (ite (and (= symbolic-d-proj-1~5118 20) (and (<= 2147483648 symbolic-d-proj-0~5119) (< symbolic-d-proj-0~5119 2147487744))) false trans-5-11-b-proj-4~5670))))
(assert (= trans-5-11-b-proj-6~5359 (ite (= trans-5-11-b-proj-0~5656 false) false (ite (and (= symbolic-d-proj-1~5118 20) (and (<= 2147483648 symbolic-d-proj-0~5119) (< symbolic-d-proj-0~5119 2147487744))) false trans-5-11-b-proj-5~5671))))
(assert (= trans-5-11-b-proj-7~5360 (ite (= trans-5-11-b-proj-0~5656 false) false (ite (and (= symbolic-d-proj-1~5118 20) (and (<= 2147483648 symbolic-d-proj-0~5119) (< symbolic-d-proj-0~5119 2147487744))) false trans-5-11-b-proj-6~5672))))
(assert (= merge-11-1-a-proj-7~5251 (ite (= trans-5-11-b-proj-0~5656 false) 0 (ite (and (= symbolic-d-proj-1~5118 20) (and (<= 2147483648 symbolic-d-proj-0~5119) (< symbolic-d-proj-0~5119 2147487744))) 0 trans-5-11-b-proj-7~5673))))
(assert (= merge-11-1-a-proj-8~5252 (ite (= trans-5-11-b-proj-0~5656 false) 0 (ite (and (= symbolic-d-proj-1~5118 20) (and (<= 2147483648 symbolic-d-proj-0~5119) (< symbolic-d-proj-0~5119 2147487744))) 0 trans-5-11-b-proj-8~5674))))
(assert (= trans-6-2-b-proj-0~5523 (ite (= assert-6-x-proj-17~5138 false) false (ite (= assert-6-x-proj-17~5138 true) true assert-6-x-proj-0~5121))))
(assert (= trans-6-2-b-proj-0~5533 0))
(assert (= trans-6-2-b-proj-1~5534 (ite (= assert-6-x-proj-17~5138 false) 0 (ite (= assert-6-x-proj-17~5138 true) 0 assert-6-b-proj-1~5143))))
(assert (= trans-6-2-b-proj-7~5540 (ite (= assert-6-x-proj-17~5138 false) 0 (ite (= assert-6-x-proj-17~5138 true) 100 assert-6-b-proj-7~5149))))
(assert (= trans-6-2-b-proj-8~5541 (ite (= assert-6-x-proj-17~5138 false) 0 (ite (= assert-6-x-proj-17~5138 true) 80 assert-6-b-proj-8~5150))))
(assert (= trans-6-2-b-proj-0~5462 (ite (= trans-6-2-b-proj-0~5523 false) false (and (= symbolic-d-proj-1~5118 24) (and (<= 3355590400 symbolic-d-proj-0~5119) (< symbolic-d-proj-0~5119 3355590656))))))
(assert (= trans-6-2-b-proj-0~5472 (ite (= trans-6-2-b-proj-0~5523 false) 0 (ite (and (= symbolic-d-proj-1~5118 24) (and (<= 3355590400 symbolic-d-proj-0~5119) (< symbolic-d-proj-0~5119 3355590656))) (+ trans-6-2-b-proj-0~5533 1) 0))))
(assert (= trans-6-2-b-proj-1~5473 (ite (= trans-6-2-b-proj-0~5523 false) 0 (ite (and (= symbolic-d-proj-1~5118 24) (and (<= 3355590400 symbolic-d-proj-0~5119) (< symbolic-d-proj-0~5119 3355590656))) trans-6-2-b-proj-1~5534 0))))
(assert (= trans-6-2-b-proj-2~5474 false))
(assert (= trans-6-2-b-proj-3~5475 false))
(assert (= trans-6-2-b-proj-4~5476 false))
(assert (= trans-6-2-b-proj-5~5477 false))
(assert (= trans-6-2-b-proj-6~5478 false))
(assert (= trans-6-2-b-proj-7~5479 (ite (= trans-6-2-b-proj-0~5523 false) 0 (ite (and (= symbolic-d-proj-1~5118 24) (and (<= 3355590400 symbolic-d-proj-0~5119) (< symbolic-d-proj-0~5119 3355590656))) trans-6-2-b-proj-7~5540 0))))
(assert (= trans-6-2-b-proj-8~5480 (ite (= trans-6-2-b-proj-0~5523 false) 0 (ite (and (= symbolic-d-proj-1~5118 24) (and (<= 3355590400 symbolic-d-proj-0~5119) (< symbolic-d-proj-0~5119 3355590656))) trans-6-2-b-proj-8~5541 0))))
(assert (= trans-6-2-result-proj-0 (ite (= trans-6-2-b-proj-0~5462 false) false (ite (and (= symbolic-d-proj-1~5118 24) (and (<= 2147487232 symbolic-d-proj-0~5119) (< symbolic-d-proj-0~5119 2147487488))) true (ite (and (= symbolic-d-proj-1~5118 24) (and (<= 2147487488 symbolic-d-proj-0~5119) (< symbolic-d-proj-0~5119 2147487744))) true (not (and (= symbolic-d-proj-1~5118 20) (and (<= 2147483648 symbolic-d-proj-0~5119) (< symbolic-d-proj-0~5119 2147487744)))))))))
(assert (= merge-2-1-a-proj-0~5244 (ite (= trans-6-2-b-proj-0~5462 false) 0 (ite (and (= symbolic-d-proj-1~5118 24) (and (<= 2147487232 symbolic-d-proj-0~5119) (< symbolic-d-proj-0~5119 2147487488))) trans-6-2-b-proj-0~5472 (ite (and (= symbolic-d-proj-1~5118 24) (and (<= 2147487488 symbolic-d-proj-0~5119) (< symbolic-d-proj-0~5119 2147487744))) trans-6-2-b-proj-0~5472 (ite (and (= symbolic-d-proj-1~5118 20) (and (<= 2147483648 symbolic-d-proj-0~5119) (< symbolic-d-proj-0~5119 2147487744))) 0 trans-6-2-b-proj-0~5472))))))
(assert (= merge-2-1-a-proj-1~5245 (ite (= trans-6-2-b-proj-0~5462 false) 0 (ite (and (= symbolic-d-proj-1~5118 24) (and (<= 2147487232 symbolic-d-proj-0~5119) (< symbolic-d-proj-0~5119 2147487488))) trans-6-2-b-proj-1~5473 (ite (and (= symbolic-d-proj-1~5118 24) (and (<= 2147487488 symbolic-d-proj-0~5119) (< symbolic-d-proj-0~5119 2147487744))) trans-6-2-b-proj-1~5473 (ite (and (= symbolic-d-proj-1~5118 20) (and (<= 2147483648 symbolic-d-proj-0~5119) (< symbolic-d-proj-0~5119 2147487744))) 0 trans-6-2-b-proj-1~5473))))))
(assert (= trans-6-2-b-proj-3~5356 (ite (= trans-6-2-b-proj-0~5462 false) false (ite (and (= symbolic-d-proj-1~5118 24) (and (<= 2147487232 symbolic-d-proj-0~5119) (< symbolic-d-proj-0~5119 2147487488))) trans-6-2-b-proj-2~5474 (ite (and (= symbolic-d-proj-1~5118 24) (and (<= 2147487488 symbolic-d-proj-0~5119) (< symbolic-d-proj-0~5119 2147487744))) trans-6-2-b-proj-2~5474 (ite (and (= symbolic-d-proj-1~5118 20) (and (<= 2147483648 symbolic-d-proj-0~5119) (< symbolic-d-proj-0~5119 2147487744))) false trans-6-2-b-proj-2~5474))))))
(assert (= trans-6-2-b-proj-4~5357 (ite (= trans-6-2-b-proj-0~5462 false) false (ite (and (= symbolic-d-proj-1~5118 24) (and (<= 2147487232 symbolic-d-proj-0~5119) (< symbolic-d-proj-0~5119 2147487488))) trans-6-2-b-proj-3~5475 (ite (and (= symbolic-d-proj-1~5118 24) (and (<= 2147487488 symbolic-d-proj-0~5119) (< symbolic-d-proj-0~5119 2147487744))) true (ite (and (= symbolic-d-proj-1~5118 20) (and (<= 2147483648 symbolic-d-proj-0~5119) (< symbolic-d-proj-0~5119 2147487744))) false trans-6-2-b-proj-3~5475))))))
(assert (= trans-6-2-b-proj-5~5358 (ite (= trans-6-2-b-proj-0~5462 false) false (ite (and (= symbolic-d-proj-1~5118 24) (and (<= 2147487232 symbolic-d-proj-0~5119) (< symbolic-d-proj-0~5119 2147487488))) true (ite (and (= symbolic-d-proj-1~5118 24) (and (<= 2147487488 symbolic-d-proj-0~5119) (< symbolic-d-proj-0~5119 2147487744))) trans-6-2-b-proj-4~5476 (ite (and (= symbolic-d-proj-1~5118 20) (and (<= 2147483648 symbolic-d-proj-0~5119) (< symbolic-d-proj-0~5119 2147487744))) false trans-6-2-b-proj-4~5476))))))
(assert (= trans-6-2-b-proj-6~5359 (ite (= trans-6-2-b-proj-0~5462 false) false (ite (and (= symbolic-d-proj-1~5118 24) (and (<= 2147487232 symbolic-d-proj-0~5119) (< symbolic-d-proj-0~5119 2147487488))) trans-6-2-b-proj-5~5477 (ite (and (= symbolic-d-proj-1~5118 24) (and (<= 2147487488 symbolic-d-proj-0~5119) (< symbolic-d-proj-0~5119 2147487744))) trans-6-2-b-proj-5~5477 (ite (and (= symbolic-d-proj-1~5118 20) (and (<= 2147483648 symbolic-d-proj-0~5119) (< symbolic-d-proj-0~5119 2147487744))) false trans-6-2-b-proj-5~5477))))))
(assert (= trans-6-2-b-proj-7~5360 (ite (= trans-6-2-b-proj-0~5462 false) false (ite (and (= symbolic-d-proj-1~5118 24) (and (<= 2147487232 symbolic-d-proj-0~5119) (< symbolic-d-proj-0~5119 2147487488))) trans-6-2-b-proj-6~5478 (ite (and (= symbolic-d-proj-1~5118 24) (and (<= 2147487488 symbolic-d-proj-0~5119) (< symbolic-d-proj-0~5119 2147487744))) trans-6-2-b-proj-6~5478 (ite (and (= symbolic-d-proj-1~5118 20) (and (<= 2147483648 symbolic-d-proj-0~5119) (< symbolic-d-proj-0~5119 2147487744))) false trans-6-2-b-proj-6~5478))))))
(assert (= merge-2-1-a-proj-7~5251 (ite (= trans-6-2-b-proj-0~5462 false) 0 (ite (and (= symbolic-d-proj-1~5118 24) (and (<= 2147487232 symbolic-d-proj-0~5119) (< symbolic-d-proj-0~5119 2147487488))) 1 (ite (and (= symbolic-d-proj-1~5118 24) (and (<= 2147487488 symbolic-d-proj-0~5119) (< symbolic-d-proj-0~5119 2147487744))) 101 (ite (and (= symbolic-d-proj-1~5118 20) (and (<= 2147483648 symbolic-d-proj-0~5119) (< symbolic-d-proj-0~5119 2147487744))) 0 trans-6-2-b-proj-7~5479))))))
(assert (= merge-2-1-a-proj-8~5252 (ite (= trans-6-2-b-proj-0~5462 false) 0 (ite (and (= symbolic-d-proj-1~5118 24) (and (<= 2147487232 symbolic-d-proj-0~5119) (< symbolic-d-proj-0~5119 2147487488))) trans-6-2-b-proj-8~5480 (ite (and (= symbolic-d-proj-1~5118 24) (and (<= 2147487488 symbolic-d-proj-0~5119) (< symbolic-d-proj-0~5119 2147487744))) trans-6-2-b-proj-8~5480 (ite (and (= symbolic-d-proj-1~5118 20) (and (<= 2147483648 symbolic-d-proj-0~5119) (< symbolic-d-proj-0~5119 2147487744))) 0 trans-6-2-b-proj-8~5480))))))
(assert (= trans-7-9-b-proj-0~6049 (ite (= assert-7-x-proj-17~5138 false) false (ite (= assert-7-x-proj-17~5138 true) true assert-7-x-proj-0~5121))))
(assert (= trans-7-9-b-proj-0~6059 0))
(assert (= trans-7-9-b-proj-1~6060 (ite (= assert-7-x-proj-17~5138 false) 0 (ite (= assert-7-x-proj-17~5138 true) 0 assert-7-b-proj-1~5143))))
(assert (= trans-7-9-b-proj-7~6066 (ite (= assert-7-x-proj-17~5138 false) 0 (ite (= assert-7-x-proj-17~5138 true) 100 assert-7-b-proj-7~5149))))
(assert (= trans-7-9-b-proj-8~6067 (ite (= assert-7-x-proj-17~5138 false) 0 (ite (= assert-7-x-proj-17~5138 true) 80 assert-7-b-proj-8~5150))))
(assert (= trans-7-9-b-proj-0~6016 (ite (= trans-7-9-b-proj-0~6049 false) false (and (= symbolic-d-proj-1~5118 24) (and (<= 3355595520 symbolic-d-proj-0~5119) (< symbolic-d-proj-0~5119 3355595776))))))
(assert (= trans-7-9-b-proj-0~6026 (ite (= trans-7-9-b-proj-0~6049 false) 0 (ite (and (= symbolic-d-proj-1~5118 24) (and (<= 3355595520 symbolic-d-proj-0~5119) (< symbolic-d-proj-0~5119 3355595776))) (+ trans-7-9-b-proj-0~6059 1) 0))))
(assert (= trans-7-9-b-proj-1~6027 (ite (= trans-7-9-b-proj-0~6049 false) 0 (ite (and (= symbolic-d-proj-1~5118 24) (and (<= 3355595520 symbolic-d-proj-0~5119) (< symbolic-d-proj-0~5119 3355595776))) trans-7-9-b-proj-1~6060 0))))
(assert (= trans-7-9-b-proj-2~6028 false))
(assert (= trans-7-9-b-proj-3~6029 false))
(assert (= trans-7-9-b-proj-4~6030 false))
(assert (= trans-7-9-b-proj-5~6031 false))
(assert (= trans-7-9-b-proj-6~6032 false))
(assert (= trans-7-9-b-proj-7~6033 (ite (= trans-7-9-b-proj-0~6049 false) 0 (ite (and (= symbolic-d-proj-1~5118 24) (and (<= 3355595520 symbolic-d-proj-0~5119) (< symbolic-d-proj-0~5119 3355595776))) trans-7-9-b-proj-7~6066 0))))
(assert (= trans-7-9-b-proj-8~6034 (ite (= trans-7-9-b-proj-0~6049 false) 0 (ite (and (= symbolic-d-proj-1~5118 24) (and (<= 3355595520 symbolic-d-proj-0~5119) (< symbolic-d-proj-0~5119 3355595776))) trans-7-9-b-proj-8~6067 0))))
(assert (= trans-7-9-result-proj-0 (ite (= trans-7-9-b-proj-0~6016 false) false (not (and (= symbolic-d-proj-1~5118 20) (and (<= 2147483648 symbolic-d-proj-0~5119) (< symbolic-d-proj-0~5119 2147487744)))))))
(assert (= merge-9-1-a-proj-0~5244 (ite (= trans-7-9-b-proj-0~6016 false) 0 (ite (and (= symbolic-d-proj-1~5118 20) (and (<= 2147483648 symbolic-d-proj-0~5119) (< symbolic-d-proj-0~5119 2147487744))) 0 trans-7-9-b-proj-0~6026))))
(assert (= merge-9-1-a-proj-1~5245 (ite (= trans-7-9-b-proj-0~6016 false) 0 (ite (and (= symbolic-d-proj-1~5118 20) (and (<= 2147483648 symbolic-d-proj-0~5119) (< symbolic-d-proj-0~5119 2147487744))) 0 trans-7-9-b-proj-1~6027))))
(assert (= trans-7-9-b-proj-3~5356 (ite (= trans-7-9-b-proj-0~6016 false) false (ite (and (= symbolic-d-proj-1~5118 20) (and (<= 2147483648 symbolic-d-proj-0~5119) (< symbolic-d-proj-0~5119 2147487744))) false trans-7-9-b-proj-2~6028))))
(assert (= trans-7-9-b-proj-4~5357 (ite (= trans-7-9-b-proj-0~6016 false) false (ite (and (= symbolic-d-proj-1~5118 20) (and (<= 2147483648 symbolic-d-proj-0~5119) (< symbolic-d-proj-0~5119 2147487744))) false trans-7-9-b-proj-3~6029))))
(assert (= trans-7-9-b-proj-5~5358 (ite (= trans-7-9-b-proj-0~6016 false) false (ite (and (= symbolic-d-proj-1~5118 20) (and (<= 2147483648 symbolic-d-proj-0~5119) (< symbolic-d-proj-0~5119 2147487744))) false trans-7-9-b-proj-4~6030))))
(assert (= trans-7-9-b-proj-6~5359 (ite (= trans-7-9-b-proj-0~6016 false) false (ite (and (= symbolic-d-proj-1~5118 20) (and (<= 2147483648 symbolic-d-proj-0~5119) (< symbolic-d-proj-0~5119 2147487744))) false trans-7-9-b-proj-5~6031))))
(assert (= trans-7-9-b-proj-7~5360 (ite (= trans-7-9-b-proj-0~6016 false) false (ite (and (= symbolic-d-proj-1~5118 20) (and (<= 2147483648 symbolic-d-proj-0~5119) (< symbolic-d-proj-0~5119 2147487744))) false trans-7-9-b-proj-6~6032))))
(assert (= merge-9-1-a-proj-7~5251 (ite (= trans-7-9-b-proj-0~6016 false) 0 (ite (and (= symbolic-d-proj-1~5118 20) (and (<= 2147483648 symbolic-d-proj-0~5119) (< symbolic-d-proj-0~5119 2147487744))) 0 trans-7-9-b-proj-7~6033))))
(assert (= merge-9-1-a-proj-8~5252 (ite (= trans-7-9-b-proj-0~6016 false) 0 (ite (and (= symbolic-d-proj-1~5118 20) (and (<= 2147483648 symbolic-d-proj-0~5119) (< symbolic-d-proj-0~5119 2147487744))) 0 trans-7-9-b-proj-8~6034))))
(assert (= trans-8-4-b-proj-0~5786 (ite (= assert-8-x-proj-17~5138 false) false (ite (and (= trans-8-4-y~5819 0) (= assert-8-x-proj-17~5138 true)) true (ite (and (= trans-8-4-y~5819 1) (= assert-8-x-proj-17~5138 true)) true (ite (and (= trans-8-4-y~5819 2) (= assert-8-x-proj-17~5138 true)) true assert-8-x-proj-0~5121))))))
(assert (= trans-8-4-b-proj-0~5796 (ite (= assert-8-x-proj-17~5138 false) 0 (ite (and (= trans-8-4-y~5819 0) (= assert-8-x-proj-17~5138 true)) 0 (ite (and (= trans-8-4-y~5819 1) (= assert-8-x-proj-17~5138 true)) 0 (ite (and (= trans-8-4-y~5819 2) (= assert-8-x-proj-17~5138 true)) 0 merge-8-1-b-proj-0~5231))))))
(assert (= trans-8-4-b-proj-1~5797 (ite (= assert-8-x-proj-17~5138 false) 0 (ite (and (= trans-8-4-y~5819 0) (= assert-8-x-proj-17~5138 true)) 0 (ite (and (= trans-8-4-y~5819 1) (= assert-8-x-proj-17~5138 true)) 1 (ite (and (= trans-8-4-y~5819 2) (= assert-8-x-proj-17~5138 true)) 110 merge-8-1-b-proj-1~5232))))))
(assert (= trans-8-4-b-proj-7~5803 (ite (= assert-8-x-proj-17~5138 false) 0 (ite (and (= trans-8-4-y~5819 0) (= assert-8-x-proj-17~5138 true)) 100 (ite (and (= trans-8-4-y~5819 1) (= assert-8-x-proj-17~5138 true)) 100 (ite (and (= trans-8-4-y~5819 2) (= assert-8-x-proj-17~5138 true)) 100 merge-8-1-b-proj-7~5238))))))
(assert (= trans-8-4-b-proj-8~5804 (ite (= assert-8-x-proj-17~5138 false) 0 (ite (and (= trans-8-4-y~5819 0) (= assert-8-x-proj-17~5138 true)) 80 (ite (and (= trans-8-4-y~5819 1) (= assert-8-x-proj-17~5138 true)) 80 (ite (and (= trans-8-4-y~5819 2) (= assert-8-x-proj-17~5138 true)) 80 merge-8-1-b-proj-8~5239))))))
(assert (= trans-8-4-b-proj-0~5739 (ite (= trans-8-4-b-proj-0~5786 false) false (ite (and (= symbolic-d-proj-1~5118 24) (and (<= 3355594240 symbolic-d-proj-0~5119) (< symbolic-d-proj-0~5119 3355594496))) true (ite (= assert-8-x-proj-17~5138 false) false (= 3 trans-8-4-y~5819))))))
(assert (= trans-8-4-b-proj-0~5749 (ite (= trans-8-4-b-proj-0~5786 false) 0 (ite (and (= symbolic-d-proj-1~5118 24) (and (<= 3355594240 symbolic-d-proj-0~5119) (< symbolic-d-proj-0~5119 3355594496))) (+ trans-8-4-b-proj-0~5796 1) (ite (ite (= assert-8-x-proj-17~5138 false) false (= 3 trans-8-4-y~5819)) (+ trans-8-4-b-proj-0~5796 1) 0)))))
(assert (= trans-8-4-b-proj-1~5750 (ite (= trans-8-4-b-proj-0~5786 false) 0 (ite (and (= symbolic-d-proj-1~5118 24) (and (<= 3355594240 symbolic-d-proj-0~5119) (< symbolic-d-proj-0~5119 3355594496))) trans-8-4-b-proj-1~5797 (ite (ite (= assert-8-x-proj-17~5138 false) false (= 3 trans-8-4-y~5819)) trans-8-4-b-proj-1~5797 0)))))
(assert (= trans-8-4-b-proj-2~5751 false))
(assert (= trans-8-4-b-proj-3~5752 false))
(assert (= trans-8-4-b-proj-4~5753 false))
(assert (= trans-8-4-b-proj-5~5754 false))
(assert (= trans-8-4-b-proj-6~5755 false))
(assert (= trans-8-4-b-proj-7~5756 (ite (= trans-8-4-b-proj-0~5786 false) 0 (ite (and (= symbolic-d-proj-1~5118 24) (and (<= 3355594240 symbolic-d-proj-0~5119) (< symbolic-d-proj-0~5119 3355594496))) trans-8-4-b-proj-7~5803 (ite (ite (= assert-8-x-proj-17~5138 false) false (= 3 trans-8-4-y~5819)) trans-8-4-b-proj-7~5803 0)))))
(assert (= trans-8-4-b-proj-8~5757 (ite (= trans-8-4-b-proj-0~5786 false) 0 (ite (and (= symbolic-d-proj-1~5118 24) (and (<= 3355594240 symbolic-d-proj-0~5119) (< symbolic-d-proj-0~5119 3355594496))) trans-8-4-b-proj-8~5804 (ite (ite (= assert-8-x-proj-17~5138 false) false (= 3 trans-8-4-y~5819)) trans-8-4-b-proj-8~5804 0)))))
(assert (= trans-8-4-result-proj-0 (ite (= trans-8-4-b-proj-0~5739 false) false (ite (and (= symbolic-d-proj-1~5118 24) (and (<= 2147487232 symbolic-d-proj-0~5119) (< symbolic-d-proj-0~5119 2147487488))) true (not (and (= symbolic-d-proj-1~5118 20) (and (<= 2147483648 symbolic-d-proj-0~5119) (< symbolic-d-proj-0~5119 2147487744))))))))
(assert (= merge-4-2-a-proj-0~5244 (ite (= trans-8-4-b-proj-0~5739 false) 0 (ite (and (= symbolic-d-proj-1~5118 24) (and (<= 2147487232 symbolic-d-proj-0~5119) (< symbolic-d-proj-0~5119 2147487488))) trans-8-4-b-proj-0~5749 (ite (and (= symbolic-d-proj-1~5118 20) (and (<= 2147483648 symbolic-d-proj-0~5119) (< symbolic-d-proj-0~5119 2147487744))) 0 trans-8-4-b-proj-0~5749)))))
(assert (= merge-4-2-a-proj-1~5245 (ite (= trans-8-4-b-proj-0~5739 false) 0 (ite (and (= symbolic-d-proj-1~5118 24) (and (<= 2147487232 symbolic-d-proj-0~5119) (< symbolic-d-proj-0~5119 2147487488))) trans-8-4-b-proj-1~5750 (ite (and (= symbolic-d-proj-1~5118 20) (and (<= 2147483648 symbolic-d-proj-0~5119) (< symbolic-d-proj-0~5119 2147487744))) 0 trans-8-4-b-proj-1~5750)))))
(assert (= trans-8-4-b-proj-3~5356 (ite (= trans-8-4-b-proj-0~5739 false) false (ite (and (= symbolic-d-proj-1~5118 24) (and (<= 2147487232 symbolic-d-proj-0~5119) (< symbolic-d-proj-0~5119 2147487488))) trans-8-4-b-proj-2~5751 (ite (and (= symbolic-d-proj-1~5118 20) (and (<= 2147483648 symbolic-d-proj-0~5119) (< symbolic-d-proj-0~5119 2147487744))) false trans-8-4-b-proj-2~5751)))))
(assert (= trans-8-4-b-proj-4~5357 (ite (= trans-8-4-b-proj-0~5739 false) false (ite (and (= symbolic-d-proj-1~5118 24) (and (<= 2147487232 symbolic-d-proj-0~5119) (< symbolic-d-proj-0~5119 2147487488))) trans-8-4-b-proj-3~5752 (ite (and (= symbolic-d-proj-1~5118 20) (and (<= 2147483648 symbolic-d-proj-0~5119) (< symbolic-d-proj-0~5119 2147487744))) false trans-8-4-b-proj-3~5752)))))
(assert (= trans-8-4-b-proj-5~5358 (ite (= trans-8-4-b-proj-0~5739 false) false (ite (and (= symbolic-d-proj-1~5118 24) (and (<= 2147487232 symbolic-d-proj-0~5119) (< symbolic-d-proj-0~5119 2147487488))) trans-8-4-b-proj-4~5753 (ite (and (= symbolic-d-proj-1~5118 20) (and (<= 2147483648 symbolic-d-proj-0~5119) (< symbolic-d-proj-0~5119 2147487744))) false trans-8-4-b-proj-4~5753)))))
(assert (= trans-8-4-b-proj-6~5359 (ite (= trans-8-4-b-proj-0~5739 false) false (ite (and (= symbolic-d-proj-1~5118 24) (and (<= 2147487232 symbolic-d-proj-0~5119) (< symbolic-d-proj-0~5119 2147487488))) true (ite (and (= symbolic-d-proj-1~5118 20) (and (<= 2147483648 symbolic-d-proj-0~5119) (< symbolic-d-proj-0~5119 2147487744))) false trans-8-4-b-proj-5~5754)))))
(assert (= trans-8-4-b-proj-7~5360 (ite (= trans-8-4-b-proj-0~5739 false) false (ite (and (= symbolic-d-proj-1~5118 24) (and (<= 2147487232 symbolic-d-proj-0~5119) (< symbolic-d-proj-0~5119 2147487488))) trans-8-4-b-proj-6~5755 (ite (and (= symbolic-d-proj-1~5118 20) (and (<= 2147483648 symbolic-d-proj-0~5119) (< symbolic-d-proj-0~5119 2147487744))) false trans-8-4-b-proj-6~5755)))))
(assert (= merge-4-2-a-proj-7~5251 (ite (= trans-8-4-b-proj-0~5739 false) 0 (ite (and (= symbolic-d-proj-1~5118 24) (and (<= 2147487232 symbolic-d-proj-0~5119) (< symbolic-d-proj-0~5119 2147487488))) 1 (ite (and (= symbolic-d-proj-1~5118 20) (and (<= 2147483648 symbolic-d-proj-0~5119) (< symbolic-d-proj-0~5119 2147487744))) 0 trans-8-4-b-proj-7~5756)))))
(assert (= merge-4-2-a-proj-8~5252 (ite (= trans-8-4-b-proj-0~5739 false) 0 (ite (and (= symbolic-d-proj-1~5118 24) (and (<= 2147487232 symbolic-d-proj-0~5119) (< symbolic-d-proj-0~5119 2147487488))) trans-8-4-b-proj-8~5757 (ite (and (= symbolic-d-proj-1~5118 20) (and (<= 2147483648 symbolic-d-proj-0~5119) (< symbolic-d-proj-0~5119 2147487744))) 0 trans-8-4-b-proj-8~5757)))))
(assert (= trans-10-4-b-proj-0~6132 (ite (= assert-10-x-proj-17~5138 false) false (ite (= assert-10-x-proj-17~5138 true) true assert-10-x-proj-0~5121))))
(assert (= trans-10-4-b-proj-0~6142 0))
(assert (= trans-10-4-b-proj-1~6143 (ite (= assert-10-x-proj-17~5138 false) 0 (ite (= assert-10-x-proj-17~5138 true) 0 assert-10-b-proj-1~5143))))
(assert (= trans-10-4-b-proj-7~6149 (ite (= assert-10-x-proj-17~5138 false) 0 (ite (= assert-10-x-proj-17~5138 true) 100 assert-10-b-proj-7~5149))))
(assert (= trans-10-4-b-proj-8~6150 (ite (= assert-10-x-proj-17~5138 false) 0 (ite (= assert-10-x-proj-17~5138 true) 80 assert-10-b-proj-8~5150))))
(assert (= trans-10-4-b-proj-0~6099 (ite (= trans-10-4-b-proj-0~6132 false) false (and (= symbolic-d-proj-1~5118 24) (and (<= 3355589120 symbolic-d-proj-0~5119) (< symbolic-d-proj-0~5119 3355589376))))))
(assert (= trans-10-4-b-proj-0~6109 (ite (= trans-10-4-b-proj-0~6132 false) 0 (ite (and (= symbolic-d-proj-1~5118 24) (and (<= 3355589120 symbolic-d-proj-0~5119) (< symbolic-d-proj-0~5119 3355589376))) (+ trans-10-4-b-proj-0~6142 1) 0))))
(assert (= trans-10-4-b-proj-1~6110 (ite (= trans-10-4-b-proj-0~6132 false) 0 (ite (and (= symbolic-d-proj-1~5118 24) (and (<= 3355589120 symbolic-d-proj-0~5119) (< symbolic-d-proj-0~5119 3355589376))) trans-10-4-b-proj-1~6143 0))))
(assert (= trans-10-4-b-proj-2~6111 false))
(assert (= trans-10-4-b-proj-3~6112 false))
(assert (= trans-10-4-b-proj-4~6113 false))
(assert (= trans-10-4-b-proj-5~6114 false))
(assert (= trans-10-4-b-proj-6~6115 false))
(assert (= trans-10-4-b-proj-7~6116 (ite (= trans-10-4-b-proj-0~6132 false) 0 (ite (and (= symbolic-d-proj-1~5118 24) (and (<= 3355589120 symbolic-d-proj-0~5119) (< symbolic-d-proj-0~5119 3355589376))) trans-10-4-b-proj-7~6149 0))))
(assert (= trans-10-4-b-proj-8~6117 (ite (= trans-10-4-b-proj-0~6132 false) 0 (ite (and (= symbolic-d-proj-1~5118 24) (and (<= 3355589120 symbolic-d-proj-0~5119) (< symbolic-d-proj-0~5119 3355589376))) trans-10-4-b-proj-8~6150 0))))
(assert (= trans-10-4-result-proj-0 (ite (= trans-10-4-b-proj-0~6099 false) false (not (and (= symbolic-d-proj-1~5118 20) (and (<= 2147483648 symbolic-d-proj-0~5119) (< symbolic-d-proj-0~5119 2147487744)))))))
(assert (= merge-4-1-a-proj-0~5244 (ite (= trans-10-4-b-proj-0~6099 false) 0 (ite (and (= symbolic-d-proj-1~5118 20) (and (<= 2147483648 symbolic-d-proj-0~5119) (< symbolic-d-proj-0~5119 2147487744))) 0 trans-10-4-b-proj-0~6109))))
(assert (= merge-4-1-a-proj-1~5245 (ite (= trans-10-4-b-proj-0~6099 false) 0 (ite (and (= symbolic-d-proj-1~5118 20) (and (<= 2147483648 symbolic-d-proj-0~5119) (< symbolic-d-proj-0~5119 2147487744))) 0 trans-10-4-b-proj-1~6110))))
(assert (= trans-10-4-b-proj-3~5356 (ite (= trans-10-4-b-proj-0~6099 false) false (ite (and (= symbolic-d-proj-1~5118 20) (and (<= 2147483648 symbolic-d-proj-0~5119) (< symbolic-d-proj-0~5119 2147487744))) false trans-10-4-b-proj-2~6111))))
(assert (= trans-10-4-b-proj-4~5357 (ite (= trans-10-4-b-proj-0~6099 false) false (ite (and (= symbolic-d-proj-1~5118 20) (and (<= 2147483648 symbolic-d-proj-0~5119) (< symbolic-d-proj-0~5119 2147487744))) false trans-10-4-b-proj-3~6112))))
(assert (= trans-10-4-b-proj-5~5358 (ite (= trans-10-4-b-proj-0~6099 false) false (ite (and (= symbolic-d-proj-1~5118 20) (and (<= 2147483648 symbolic-d-proj-0~5119) (< symbolic-d-proj-0~5119 2147487744))) false trans-10-4-b-proj-4~6113))))
(assert (= trans-10-4-b-proj-6~5359 (ite (= trans-10-4-b-proj-0~6099 false) false (ite (and (= symbolic-d-proj-1~5118 20) (and (<= 2147483648 symbolic-d-proj-0~5119) (< symbolic-d-proj-0~5119 2147487744))) false trans-10-4-b-proj-5~6114))))
(assert (= trans-10-4-b-proj-7~5360 (ite (= trans-10-4-b-proj-0~6099 false) false (ite (and (= symbolic-d-proj-1~5118 20) (and (<= 2147483648 symbolic-d-proj-0~5119) (< symbolic-d-proj-0~5119 2147487744))) false trans-10-4-b-proj-6~6115))))
(assert (= merge-4-1-a-proj-7~5251 (ite (= trans-10-4-b-proj-0~6099 false) 0 (ite (and (= symbolic-d-proj-1~5118 20) (and (<= 2147483648 symbolic-d-proj-0~5119) (< symbolic-d-proj-0~5119 2147487744))) 0 trans-10-4-b-proj-7~6116))))
(assert (= merge-4-1-a-proj-8~5252 (ite (= trans-10-4-b-proj-0~6099 false) 0 (ite (and (= symbolic-d-proj-1~5118 20) (and (<= 2147483648 symbolic-d-proj-0~5119) (< symbolic-d-proj-0~5119 2147487744))) 0 trans-10-4-b-proj-8~6117))))
(assert (= trans-13-3-b-proj-0~6192 (ite (= assert-13-x-proj-17~5138 false) false (ite (= assert-13-x-proj-17~5138 true) true assert-13-x-proj-0~5121))))
(assert (= trans-13-3-b-proj-0~6202 0))
(assert (= trans-13-3-b-proj-1~6203 (ite (= assert-13-x-proj-17~5138 false) 0 (ite (= assert-13-x-proj-17~5138 true) 0 assert-13-b-proj-1~5143))))
(assert (= trans-13-3-b-proj-7~6209 (ite (= assert-13-x-proj-17~5138 false) 0 (ite (= assert-13-x-proj-17~5138 true) 100 assert-13-b-proj-7~5149))))
(assert (= trans-13-3-b-proj-8~6210 (ite (= assert-13-x-proj-17~5138 false) 0 (ite (= assert-13-x-proj-17~5138 true) 80 assert-13-b-proj-8~5150))))
(assert (= trans-13-3-result-proj-0 (ite (= trans-13-3-b-proj-0~6192 false) false (ite (and (= symbolic-d-proj-1~5118 24) (and (<= 3355587840 symbolic-d-proj-0~5119) (< symbolic-d-proj-0~5119 3355588096))) (not (and (= symbolic-d-proj-1~5118 20) (and (<= 2147483648 symbolic-d-proj-0~5119) (< symbolic-d-proj-0~5119 2147487744)))) false))))
(assert (= merge-3-1-a-proj-0~5244 (ite (= trans-13-3-b-proj-0~6192 false) 0 (ite (and (= symbolic-d-proj-1~5118 24) (and (<= 3355587840 symbolic-d-proj-0~5119) (< symbolic-d-proj-0~5119 3355588096))) (ite (and (= symbolic-d-proj-1~5118 20) (and (<= 2147483648 symbolic-d-proj-0~5119) (< symbolic-d-proj-0~5119 2147487744))) 0 (+ trans-13-3-b-proj-0~6202 1)) 0))))
(assert (= merge-3-1-a-proj-1~5245 (ite (= trans-13-3-b-proj-0~6192 false) 0 (ite (and (= symbolic-d-proj-1~5118 24) (and (<= 3355587840 symbolic-d-proj-0~5119) (< symbolic-d-proj-0~5119 3355588096))) (ite (and (= symbolic-d-proj-1~5118 20) (and (<= 2147483648 symbolic-d-proj-0~5119) (< symbolic-d-proj-0~5119 2147487744))) 0 trans-13-3-b-proj-1~6203) 0))))
(assert (= trans-13-3-b-proj-3~5356 false))
(assert (= trans-13-3-b-proj-4~5357 false))
(assert (= trans-13-3-b-proj-5~5358 false))
(assert (= trans-13-3-b-proj-6~5359 false))
(assert (= trans-13-3-b-proj-7~5360 false))
(assert (= merge-3-1-a-proj-7~5251 (ite (= trans-13-3-b-proj-0~6192 false) 0 (ite (and (= symbolic-d-proj-1~5118 24) (and (<= 3355587840 symbolic-d-proj-0~5119) (< symbolic-d-proj-0~5119 3355588096))) (ite (and (= symbolic-d-proj-1~5118 20) (and (<= 2147483648 symbolic-d-proj-0~5119) (< symbolic-d-proj-0~5119 2147487744))) 0 trans-13-3-b-proj-7~6209) 0))))
(assert (= merge-3-1-a-proj-8~5252 (ite (= trans-13-3-b-proj-0~6192 false) 0 (ite (and (= symbolic-d-proj-1~5118 24) (and (<= 3355587840 symbolic-d-proj-0~5119) (< symbolic-d-proj-0~5119 3355588096))) (ite (and (= symbolic-d-proj-1~5118 20) (and (<= 2147483648 symbolic-d-proj-0~5119) (< symbolic-d-proj-0~5119 2147487744))) 0 trans-13-3-b-proj-8~6210) 0))))
(assert (= trans-14-15-b-proj-0~5966 (ite (= assert-14-x-proj-17~5138 false) false (ite (= assert-14-x-proj-17~5138 true) true assert-14-x-proj-0~5121))))
(assert (= trans-14-15-b-proj-0~5976 0))
(assert (= trans-14-15-b-proj-1~5977 (ite (= assert-14-x-proj-17~5138 false) 0 (ite (= assert-14-x-proj-17~5138 true) 0 assert-14-b-proj-1~5143))))
(assert (= trans-14-15-b-proj-7~5983 (ite (= assert-14-x-proj-17~5138 false) 0 (ite (= assert-14-x-proj-17~5138 true) 100 assert-14-b-proj-7~5149))))
(assert (= trans-14-15-b-proj-8~5984 (ite (= assert-14-x-proj-17~5138 false) 0 (ite (= assert-14-x-proj-17~5138 true) 80 assert-14-b-proj-8~5150))))
(assert (= trans-14-15-b-proj-0~5919 (ite (= trans-14-15-b-proj-0~5966 false) false (and (= symbolic-d-proj-1~5118 24) (and (<= 3355588096 symbolic-d-proj-0~5119) (< symbolic-d-proj-0~5119 3355588352))))))
(assert (= trans-14-15-b-proj-0~5929 (ite (= trans-14-15-b-proj-0~5966 false) 0 (ite (and (= symbolic-d-proj-1~5118 24) (and (<= 3355588096 symbolic-d-proj-0~5119) (< symbolic-d-proj-0~5119 3355588352))) (+ trans-14-15-b-proj-0~5976 1) 0))))
(assert (= trans-14-15-b-proj-1~5930 (ite (= trans-14-15-b-proj-0~5966 false) 0 (ite (and (= symbolic-d-proj-1~5118 24) (and (<= 3355588096 symbolic-d-proj-0~5119) (< symbolic-d-proj-0~5119 3355588352))) trans-14-15-b-proj-1~5977 0))))
(assert (= trans-14-15-b-proj-2~5931 false))
(assert (= trans-14-15-b-proj-3~5932 false))
(assert (= trans-14-15-b-proj-4~5933 false))
(assert (= trans-14-15-b-proj-5~5934 false))
(assert (= trans-14-15-b-proj-6~5935 false))
(assert (= trans-14-15-b-proj-7~5936 (ite (= trans-14-15-b-proj-0~5966 false) 0 (ite (and (= symbolic-d-proj-1~5118 24) (and (<= 3355588096 symbolic-d-proj-0~5119) (< symbolic-d-proj-0~5119 3355588352))) trans-14-15-b-proj-7~5983 0))))
(assert (= trans-14-15-b-proj-8~5937 (ite (= trans-14-15-b-proj-0~5966 false) 0 (ite (and (= symbolic-d-proj-1~5118 24) (and (<= 3355588096 symbolic-d-proj-0~5119) (< symbolic-d-proj-0~5119 3355588352))) trans-14-15-b-proj-8~5984 0))))
(assert (= trans-14-15-result-proj-0 (ite (= trans-14-15-b-proj-0~5919 false) false (ite (and (= symbolic-d-proj-1~5118 24) (and (<= 2147483648 symbolic-d-proj-0~5119) (< symbolic-d-proj-0~5119 2147483904))) true (not (and (= symbolic-d-proj-1~5118 20) (and (<= 2147483648 symbolic-d-proj-0~5119) (< symbolic-d-proj-0~5119 2147487744))))))))
(assert (= merge-15-1-a-proj-0~5244 (ite (= trans-14-15-b-proj-0~5919 false) 0 (ite (and (= symbolic-d-proj-1~5118 24) (and (<= 2147483648 symbolic-d-proj-0~5119) (< symbolic-d-proj-0~5119 2147483904))) trans-14-15-b-proj-0~5929 (ite (and (= symbolic-d-proj-1~5118 20) (and (<= 2147483648 symbolic-d-proj-0~5119) (< symbolic-d-proj-0~5119 2147487744))) 0 trans-14-15-b-proj-0~5929)))))
(assert (= merge-15-1-a-proj-1~5245 (ite (= trans-14-15-b-proj-0~5919 false) 0 (ite (and (= symbolic-d-proj-1~5118 24) (and (<= 2147483648 symbolic-d-proj-0~5119) (< symbolic-d-proj-0~5119 2147483904))) trans-14-15-b-proj-1~5930 (ite (and (= symbolic-d-proj-1~5118 20) (and (<= 2147483648 symbolic-d-proj-0~5119) (< symbolic-d-proj-0~5119 2147487744))) 0 trans-14-15-b-proj-1~5930)))))
(assert (= trans-14-15-b-proj-3~5356 (ite (= trans-14-15-b-proj-0~5919 false) false (ite (and (= symbolic-d-proj-1~5118 24) (and (<= 2147483648 symbolic-d-proj-0~5119) (< symbolic-d-proj-0~5119 2147483904))) trans-14-15-b-proj-2~5931 (ite (and (= symbolic-d-proj-1~5118 20) (and (<= 2147483648 symbolic-d-proj-0~5119) (< symbolic-d-proj-0~5119 2147487744))) false trans-14-15-b-proj-2~5931)))))
(assert (= trans-14-15-b-proj-4~5357 (ite (= trans-14-15-b-proj-0~5919 false) false (ite (and (= symbolic-d-proj-1~5118 24) (and (<= 2147483648 symbolic-d-proj-0~5119) (< symbolic-d-proj-0~5119 2147483904))) trans-14-15-b-proj-3~5932 (ite (and (= symbolic-d-proj-1~5118 20) (and (<= 2147483648 symbolic-d-proj-0~5119) (< symbolic-d-proj-0~5119 2147487744))) false trans-14-15-b-proj-3~5932)))))
(assert (= trans-14-15-b-proj-5~5358 (ite (= trans-14-15-b-proj-0~5919 false) false (ite (and (= symbolic-d-proj-1~5118 24) (and (<= 2147483648 symbolic-d-proj-0~5119) (< symbolic-d-proj-0~5119 2147483904))) trans-14-15-b-proj-4~5933 (ite (and (= symbolic-d-proj-1~5118 20) (and (<= 2147483648 symbolic-d-proj-0~5119) (< symbolic-d-proj-0~5119 2147487744))) false trans-14-15-b-proj-4~5933)))))
(assert (= trans-14-15-b-proj-6~5359 (ite (= trans-14-15-b-proj-0~5919 false) false (ite (and (= symbolic-d-proj-1~5118 24) (and (<= 2147483648 symbolic-d-proj-0~5119) (< symbolic-d-proj-0~5119 2147483904))) trans-14-15-b-proj-5~5934 (ite (and (= symbolic-d-proj-1~5118 20) (and (<= 2147483648 symbolic-d-proj-0~5119) (< symbolic-d-proj-0~5119 2147487744))) false trans-14-15-b-proj-5~5934)))))
(assert (= trans-14-15-b-proj-7~5360 (ite (= trans-14-15-b-proj-0~5919 false) false (ite (and (= symbolic-d-proj-1~5118 24) (and (<= 2147483648 symbolic-d-proj-0~5119) (< symbolic-d-proj-0~5119 2147483904))) true (ite (and (= symbolic-d-proj-1~5118 20) (and (<= 2147483648 symbolic-d-proj-0~5119) (< symbolic-d-proj-0~5119 2147487744))) false trans-14-15-b-proj-6~5935)))))
(assert (= merge-15-1-a-proj-7~5251 (ite (= trans-14-15-b-proj-0~5919 false) 0 (ite (and (= symbolic-d-proj-1~5118 24) (and (<= 2147483648 symbolic-d-proj-0~5119) (< symbolic-d-proj-0~5119 2147483904))) 1 (ite (and (= symbolic-d-proj-1~5118 20) (and (<= 2147483648 symbolic-d-proj-0~5119) (< symbolic-d-proj-0~5119 2147487744))) 0 trans-14-15-b-proj-7~5936)))))
(assert (= merge-15-1-a-proj-8~5252 (ite (= trans-14-15-b-proj-0~5919 false) 0 (ite (and (= symbolic-d-proj-1~5118 24) (and (<= 2147483648 symbolic-d-proj-0~5119) (< symbolic-d-proj-0~5119 2147483904))) trans-14-15-b-proj-8~5937 (ite (and (= symbolic-d-proj-1~5118 20) (and (<= 2147483648 symbolic-d-proj-0~5119) (< symbolic-d-proj-0~5119 2147487744))) 0 trans-14-15-b-proj-8~5937)))))
(assert (= trans-16-12-b-proj-0~5869 (ite (= assert-16-x-proj-17~5138 false) false (ite (= assert-16-x-proj-17~5138 true) true assert-16-x-proj-0~5121))))
(assert (= trans-16-12-b-proj-0~5879 0))
(assert (= trans-16-12-b-proj-1~5880 (ite (= assert-16-x-proj-17~5138 false) 0 (ite (= assert-16-x-proj-17~5138 true) 0 assert-16-b-proj-1~5143))))
(assert (= trans-16-12-b-proj-7~5886 (ite (= assert-16-x-proj-17~5138 false) 0 (ite (= assert-16-x-proj-17~5138 true) 100 assert-16-b-proj-7~5149))))
(assert (= trans-16-12-b-proj-8~5887 (ite (= assert-16-x-proj-17~5138 false) 0 (ite (= assert-16-x-proj-17~5138 true) 80 assert-16-b-proj-8~5150))))
(assert (= trans-16-12-b-proj-0~5836 (ite (= trans-16-12-b-proj-0~5869 false) false (ite (and (= symbolic-d-proj-1~5118 24) (and (<= 3355583744 symbolic-d-proj-0~5119) (< symbolic-d-proj-0~5119 3355584000))) (not (and (= symbolic-d-proj-1~5118 20) (and (<= 2147483648 symbolic-d-proj-0~5119) (< symbolic-d-proj-0~5119 2147487744)))) false))))
(assert (= trans-16-12-b-proj-0~5846 (ite (= trans-16-12-b-proj-0~5869 false) 0 (ite (and (= symbolic-d-proj-1~5118 24) (and (<= 3355583744 symbolic-d-proj-0~5119) (< symbolic-d-proj-0~5119 3355584000))) (ite (and (= symbolic-d-proj-1~5118 20) (and (<= 2147483648 symbolic-d-proj-0~5119) (< symbolic-d-proj-0~5119 2147487744))) 0 (+ trans-16-12-b-proj-0~5879 1)) 0))))
(assert (= trans-16-12-b-proj-1~5847 (ite (= trans-16-12-b-proj-0~5869 false) 0 (ite (and (= symbolic-d-proj-1~5118 24) (and (<= 3355583744 symbolic-d-proj-0~5119) (< symbolic-d-proj-0~5119 3355584000))) (ite (and (= symbolic-d-proj-1~5118 20) (and (<= 2147483648 symbolic-d-proj-0~5119) (< symbolic-d-proj-0~5119 2147487744))) 0 trans-16-12-b-proj-1~5880) 0))))
(assert (= trans-16-12-b-proj-2~5848 false))
(assert (= trans-16-12-b-proj-3~5849 false))
(assert (= trans-16-12-b-proj-4~5850 false))
(assert (= trans-16-12-b-proj-5~5851 false))
(assert (= trans-16-12-b-proj-6~5852 false))
(assert (= trans-16-12-b-proj-7~5853 (ite (= trans-16-12-b-proj-0~5869 false) 0 (ite (and (= symbolic-d-proj-1~5118 24) (and (<= 3355583744 symbolic-d-proj-0~5119) (< symbolic-d-proj-0~5119 3355584000))) (ite (and (= symbolic-d-proj-1~5118 20) (and (<= 2147483648 symbolic-d-proj-0~5119) (< symbolic-d-proj-0~5119 2147487744))) 0 trans-16-12-b-proj-7~5886) 0))))
(assert (= trans-16-12-b-proj-8~5854 (ite (= trans-16-12-b-proj-0~5869 false) 0 (ite (and (= symbolic-d-proj-1~5118 24) (and (<= 3355583744 symbolic-d-proj-0~5119) (< symbolic-d-proj-0~5119 3355584000))) (ite (and (= symbolic-d-proj-1~5118 20) (and (<= 2147483648 symbolic-d-proj-0~5119) (< symbolic-d-proj-0~5119 2147487744))) 0 trans-16-12-b-proj-8~5887) 0))))
(assert (= trans-16-12-result-proj-0 (ite (= trans-16-12-b-proj-0~5836 false) false (not (and (= symbolic-d-proj-1~5118 20) (and (<= 2147483648 symbolic-d-proj-0~5119) (< symbolic-d-proj-0~5119 2147487744)))))))
(assert (= merge-12-1-a-proj-0~5244 (ite (= trans-16-12-b-proj-0~5836 false) 0 (ite (and (= symbolic-d-proj-1~5118 20) (and (<= 2147483648 symbolic-d-proj-0~5119) (< symbolic-d-proj-0~5119 2147487744))) 0 trans-16-12-b-proj-0~5846))))
(assert (= merge-12-1-a-proj-1~5245 (ite (= trans-16-12-b-proj-0~5836 false) 0 (ite (and (= symbolic-d-proj-1~5118 20) (and (<= 2147483648 symbolic-d-proj-0~5119) (< symbolic-d-proj-0~5119 2147487744))) 0 trans-16-12-b-proj-1~5847))))
(assert (= trans-16-12-b-proj-3~5356 (ite (= trans-16-12-b-proj-0~5836 false) false (ite (and (= symbolic-d-proj-1~5118 20) (and (<= 2147483648 symbolic-d-proj-0~5119) (< symbolic-d-proj-0~5119 2147487744))) false trans-16-12-b-proj-2~5848))))
(assert (= trans-16-12-b-proj-4~5357 (ite (= trans-16-12-b-proj-0~5836 false) false (ite (and (= symbolic-d-proj-1~5118 20) (and (<= 2147483648 symbolic-d-proj-0~5119) (< symbolic-d-proj-0~5119 2147487744))) false trans-16-12-b-proj-3~5849))))
(assert (= trans-16-12-b-proj-5~5358 (ite (= trans-16-12-b-proj-0~5836 false) false (ite (and (= symbolic-d-proj-1~5118 20) (and (<= 2147483648 symbolic-d-proj-0~5119) (< symbolic-d-proj-0~5119 2147487744))) false trans-16-12-b-proj-4~5850))))
(assert (= trans-16-12-b-proj-6~5359 (ite (= trans-16-12-b-proj-0~5836 false) false (ite (and (= symbolic-d-proj-1~5118 20) (and (<= 2147483648 symbolic-d-proj-0~5119) (< symbolic-d-proj-0~5119 2147487744))) false trans-16-12-b-proj-5~5851))))
(assert (= trans-16-12-b-proj-7~5360 (ite (= trans-16-12-b-proj-0~5836 false) false (ite (and (= symbolic-d-proj-1~5118 20) (and (<= 2147483648 symbolic-d-proj-0~5119) (< symbolic-d-proj-0~5119 2147487744))) false trans-16-12-b-proj-6~5852))))
(assert (= merge-12-1-a-proj-7~5251 (ite (= trans-16-12-b-proj-0~5836 false) 0 (ite (and (= symbolic-d-proj-1~5118 20) (and (<= 2147483648 symbolic-d-proj-0~5119) (< symbolic-d-proj-0~5119 2147487744))) 0 trans-16-12-b-proj-7~5853))))
(assert (= merge-12-1-a-proj-8~5252 (ite (= trans-16-12-b-proj-0~5836 false) 0 (ite (and (= symbolic-d-proj-1~5118 20) (and (<= 2147483648 symbolic-d-proj-0~5119) (< symbolic-d-proj-0~5119 2147487744))) 0 trans-16-12-b-proj-8~5854))))
(assert (= assert-1-x-proj-10~5131 init-1-result-proj-5))
(assert (= merge-1-1-a~5229 0))
(assert (= assert-1-x-proj-19~5140 false))
(assert (= merge-1-1-b~5230 0))
(assert (= merge-1-1-TupleFlattenVar~5299 0))
(assert (= merge-1-1-TupleFlattenVar~5300 0))
(assert (= merge-1-1-TupleFlattenVar~5301 0))
(assert (= merge-1-1-TupleFlattenVar~5302 0))
(assert (= assert-1-x-proj-12~5133 false))
(assert (= merge-1-1-o-proj-0~5240 0))
(assert (= merge-1-1-o-proj-1~5241 0))
(assert (= merge-1-1-o-proj-2~5242 0))
(assert (= merge-1-1-o-proj-3~5243 0))
(assert (= merge-1-1-TupleFlattenVar~5262 (ite (< merge-1-1-b-proj-7~5260 merge-1-1-a-proj-7~5251) merge-1-1-a-proj-0~5244 (ite (< merge-1-1-a-proj-7~5251 merge-1-1-b-proj-7~5260) 0 (ite (< merge-1-1-a-proj-0~5244 0) merge-1-1-a-proj-0~5244 (ite (< 0 merge-1-1-a-proj-0~5244) 0 (ite (<= merge-1-1-b-proj-8~5261 merge-1-1-a-proj-8~5252) merge-1-1-a-proj-0~5244 0)))))))
(assert (= merge-1-1-TupleFlattenVar~5263 (ite (< merge-1-1-b-proj-7~5260 merge-1-1-a-proj-7~5251) merge-1-1-a-proj-1~5245 (ite (< merge-1-1-a-proj-7~5251 merge-1-1-b-proj-7~5260) merge-1-1-b-proj-1~5254 (ite (< merge-1-1-a-proj-0~5244 0) merge-1-1-a-proj-1~5245 (ite (< 0 merge-1-1-a-proj-0~5244) merge-1-1-b-proj-1~5254 (ite (<= merge-1-1-b-proj-8~5261 merge-1-1-a-proj-8~5252) merge-1-1-a-proj-1~5245 merge-1-1-b-proj-1~5254)))))))
(assert (= merge-1-1-TupleFlattenVar~5264 false))
(assert (= merge-1-1-TupleFlattenVar~5265 false))
(assert (= merge-1-1-TupleFlattenVar~5266 false))
(assert (= merge-1-1-TupleFlattenVar~5267 false))
(assert (= merge-1-1-TupleFlattenVar~5268 false))
(assert (= merge-1-1-TupleFlattenVar~5269 (ite (< merge-1-1-b-proj-7~5260 merge-1-1-a-proj-7~5251) merge-1-1-a-proj-7~5251 (ite (< merge-1-1-a-proj-7~5251 merge-1-1-b-proj-7~5260) merge-1-1-b-proj-7~5260 (ite (< merge-1-1-a-proj-0~5244 0) merge-1-1-a-proj-7~5251 (ite (< 0 merge-1-1-a-proj-0~5244) merge-1-1-b-proj-7~5260 (ite (<= merge-1-1-b-proj-8~5261 merge-1-1-a-proj-8~5252) merge-1-1-a-proj-7~5251 merge-1-1-b-proj-7~5260)))))))
(assert (= merge-1-1-TupleFlattenVar~5270 (ite (< merge-1-1-b-proj-7~5260 merge-1-1-a-proj-7~5251) merge-1-1-a-proj-8~5252 (ite (< merge-1-1-a-proj-7~5251 merge-1-1-b-proj-7~5260) merge-1-1-b-proj-8~5261 (ite (< merge-1-1-a-proj-0~5244 0) merge-1-1-a-proj-8~5252 (ite (< 0 merge-1-1-a-proj-0~5244) merge-1-1-b-proj-8~5261 (ite (<= merge-1-1-b-proj-8~5261 merge-1-1-a-proj-8~5252) merge-1-1-a-proj-8~5252 merge-1-1-b-proj-8~5261)))))))
(assert (= assert-1-x-proj-0~5121 (ite (= trans-0-1-result-proj-0 false) init-1-result-proj-0 (ite (= init-1-result-proj-0 false) trans-0-1-result-proj-0 true))))
(assert (= merge-1-1-b-proj-0~5231 (ite (= trans-0-1-result-proj-0 false) 0 (ite (= init-1-result-proj-0 false) merge-1-1-a-proj-0~5244 merge-1-1-TupleFlattenVar~5262))))
(assert (= merge-1-1-b-proj-1~5232 (ite (= trans-0-1-result-proj-0 false) merge-1-1-b-proj-1~5254 (ite (= init-1-result-proj-0 false) merge-1-1-a-proj-1~5245 merge-1-1-TupleFlattenVar~5263))))
(assert (= merge-1-1-b-proj-2~5233 (ite (= trans-0-1-result-proj-0 false) false (ite (= init-1-result-proj-0 false) false merge-1-1-TupleFlattenVar~5264))))
(assert (= merge-1-1-b-proj-3~5234 (ite (= trans-0-1-result-proj-0 false) false (ite (= init-1-result-proj-0 false) false merge-1-1-TupleFlattenVar~5265))))
(assert (= merge-1-1-b-proj-4~5235 (ite (= trans-0-1-result-proj-0 false) false (ite (= init-1-result-proj-0 false) false merge-1-1-TupleFlattenVar~5266))))
(assert (= merge-1-1-b-proj-5~5236 (ite (= trans-0-1-result-proj-0 false) false (ite (= init-1-result-proj-0 false) false merge-1-1-TupleFlattenVar~5267))))
(assert (= merge-1-1-b-proj-6~5237 (ite (= trans-0-1-result-proj-0 false) false (ite (= init-1-result-proj-0 false) false merge-1-1-TupleFlattenVar~5268))))
(assert (= merge-1-1-b-proj-7~5238 (ite (= trans-0-1-result-proj-0 false) merge-1-1-b-proj-7~5260 (ite (= init-1-result-proj-0 false) merge-1-1-a-proj-7~5251 merge-1-1-TupleFlattenVar~5269))))
(assert (= merge-1-1-b-proj-8~5239 (ite (= trans-0-1-result-proj-0 false) merge-1-1-b-proj-8~5261 (ite (= init-1-result-proj-0 false) merge-1-1-a-proj-8~5252 merge-1-1-TupleFlattenVar~5270))))
(assert (= merge-1-1-o-proj-0~5215 (not (= assert-1-x-proj-12~5133 false))))
(assert (= merge-1-1-a~5227 (ite (= assert-1-x-proj-12~5133 false) 0 merge-1-1-o-proj-2~5242)))
(assert (= merge-1-1-b-proj-0~5217 (not (= assert-1-x-proj-0~5121 false))))
(assert (= merge-1-1-b~5228 (ite (= assert-1-x-proj-0~5121 false) 0 merge-1-1-b-proj-1~5232)))
(assert (= merge-1-1-x-proj-0~5219 (ite (ite (= assert-1-x-proj-19~5140 false) true (ite (= assert-1-x-proj-10~5131 false) false (<= merge-1-1-a~5229 merge-1-1-b~5230))) assert-1-x-proj-10~5131 assert-1-x-proj-19~5140)))
(assert (= merge-1-1-a~5225 (ite (ite (= assert-1-x-proj-19~5140 false) true (ite (= assert-1-x-proj-10~5131 false) false (<= merge-1-1-a~5229 merge-1-1-b~5230))) merge-1-1-a~5229 merge-1-1-b~5230)))
(assert (= merge-1-1-p1~5221 (ite (ite (= assert-1-x-proj-19~5140 false) true (ite (= assert-1-x-proj-10~5131 false) false (<= merge-1-1-a~5229 merge-1-1-b~5230))) 0 1)))
(assert (= merge-1-1-y-proj-0~5222 (ite (ite (= merge-1-1-b-proj-0~5217 false) true (ite (= merge-1-1-o-proj-0~5215 false) false (<= merge-1-1-a~5227 merge-1-1-b~5228))) merge-1-1-o-proj-0~5215 merge-1-1-b-proj-0~5217)))
(assert (= merge-1-1-b~5226 (ite (ite (= merge-1-1-b-proj-0~5217 false) true (ite (= merge-1-1-o-proj-0~5215 false) false (<= merge-1-1-a~5227 merge-1-1-b~5228))) merge-1-1-a~5227 merge-1-1-b~5228)))
(assert (= merge-1-1-p2~5224 (ite (ite (= merge-1-1-b-proj-0~5217 false) true (ite (= merge-1-1-o-proj-0~5215 false) false (<= merge-1-1-a~5227 merge-1-1-b~5228))) 2 3)))
(assert (= assert-1-x-proj-17~5138 (not (and (= assert-1-x-proj-0~5121 false) (and (= assert-1-x-proj-12~5133 false) (and (= assert-1-x-proj-19~5140 false) (= assert-1-x-proj-10~5131 false)))))))
(assert (= assert-1-x-proj-18~5139 (ite (and (= assert-1-x-proj-0~5121 false) (and (= assert-1-x-proj-12~5133 false) (and (= assert-1-x-proj-19~5140 false) (= assert-1-x-proj-10~5131 false)))) 0 (ite (ite (= merge-1-1-y-proj-0~5222 false) true (ite (= merge-1-1-x-proj-0~5219 false) false (<= merge-1-1-a~5225 merge-1-1-b~5226))) merge-1-1-p1~5221 merge-1-1-p2~5224))))
(assert (= assert-2-x-proj-10~5131 init-2-result-proj-5))
(assert (= merge-2-1-a~5229 0))
(assert (= assert-2-x-proj-19~5140 false))
(assert (= merge-2-1-b~5230 0))
(assert (= merge-2-1-TupleFlattenVar~5299 0))
(assert (= merge-2-1-TupleFlattenVar~5300 0))
(assert (= merge-2-1-TupleFlattenVar~5301 0))
(assert (= merge-2-1-TupleFlattenVar~5302 0))
(assert (= assert-2-x-proj-12~5133 false))
(assert (= merge-2-1-o-proj-0~5240 0))
(assert (= merge-2-1-o-proj-1~5241 0))
(assert (= merge-2-1-o-proj-2~5242 0))
(assert (= merge-2-1-o-proj-3~5243 0))
(assert (= merge-2-1-TupleFlattenVar~5262 (ite (< merge-2-1-b-proj-7~5260 merge-2-1-a-proj-7~5251) merge-2-1-a-proj-0~5244 (ite (< merge-2-1-a-proj-7~5251 merge-2-1-b-proj-7~5260) 0 (ite (< merge-2-1-a-proj-0~5244 0) merge-2-1-a-proj-0~5244 (ite (< 0 merge-2-1-a-proj-0~5244) 0 (ite (<= merge-2-1-b-proj-8~5261 merge-2-1-a-proj-8~5252) merge-2-1-a-proj-0~5244 0)))))))
(assert (= merge-2-1-TupleFlattenVar~5263 (ite (< merge-2-1-b-proj-7~5260 merge-2-1-a-proj-7~5251) merge-2-1-a-proj-1~5245 (ite (< merge-2-1-a-proj-7~5251 merge-2-1-b-proj-7~5260) merge-2-1-b-proj-1~5254 (ite (< merge-2-1-a-proj-0~5244 0) merge-2-1-a-proj-1~5245 (ite (< 0 merge-2-1-a-proj-0~5244) merge-2-1-b-proj-1~5254 (ite (<= merge-2-1-b-proj-8~5261 merge-2-1-a-proj-8~5252) merge-2-1-a-proj-1~5245 merge-2-1-b-proj-1~5254)))))))
(assert (= merge-2-1-TupleFlattenVar~5264 false))
(assert (= merge-2-1-TupleFlattenVar~5265 false))
(assert (= merge-2-1-TupleFlattenVar~5266 false))
(assert (= merge-2-1-TupleFlattenVar~5267 false))
(assert (= merge-2-1-TupleFlattenVar~5268 false))
(assert (= merge-2-1-TupleFlattenVar~5269 (ite (< merge-2-1-b-proj-7~5260 merge-2-1-a-proj-7~5251) merge-2-1-a-proj-7~5251 (ite (< merge-2-1-a-proj-7~5251 merge-2-1-b-proj-7~5260) merge-2-1-b-proj-7~5260 (ite (< merge-2-1-a-proj-0~5244 0) merge-2-1-a-proj-7~5251 (ite (< 0 merge-2-1-a-proj-0~5244) merge-2-1-b-proj-7~5260 (ite (<= merge-2-1-b-proj-8~5261 merge-2-1-a-proj-8~5252) merge-2-1-a-proj-7~5251 merge-2-1-b-proj-7~5260)))))))
(assert (= merge-2-1-TupleFlattenVar~5270 (ite (< merge-2-1-b-proj-7~5260 merge-2-1-a-proj-7~5251) merge-2-1-a-proj-8~5252 (ite (< merge-2-1-a-proj-7~5251 merge-2-1-b-proj-7~5260) merge-2-1-b-proj-8~5261 (ite (< merge-2-1-a-proj-0~5244 0) merge-2-1-a-proj-8~5252 (ite (< 0 merge-2-1-a-proj-0~5244) merge-2-1-b-proj-8~5261 (ite (<= merge-2-1-b-proj-8~5261 merge-2-1-a-proj-8~5252) merge-2-1-a-proj-8~5252 merge-2-1-b-proj-8~5261)))))))
(assert (= assert-2-x-proj-0~5121 (ite (= trans-6-2-result-proj-0 false) init-2-result-proj-0 (ite (= init-2-result-proj-0 false) trans-6-2-result-proj-0 true))))
(assert (= merge-2-1-b-proj-0~5231 (ite (= trans-6-2-result-proj-0 false) 0 (ite (= init-2-result-proj-0 false) merge-2-1-a-proj-0~5244 merge-2-1-TupleFlattenVar~5262))))
(assert (= merge-2-1-b-proj-1~5232 (ite (= trans-6-2-result-proj-0 false) merge-2-1-b-proj-1~5254 (ite (= init-2-result-proj-0 false) merge-2-1-a-proj-1~5245 merge-2-1-TupleFlattenVar~5263))))
(assert (= merge-2-1-b-proj-2~5233 (ite (= trans-6-2-result-proj-0 false) false (ite (= init-2-result-proj-0 false) false merge-2-1-TupleFlattenVar~5264))))
(assert (= merge-2-1-b-proj-3~5234 (ite (= trans-6-2-result-proj-0 false) false (ite (= init-2-result-proj-0 false) false merge-2-1-TupleFlattenVar~5265))))
(assert (= merge-2-1-b-proj-4~5235 (ite (= trans-6-2-result-proj-0 false) false (ite (= init-2-result-proj-0 false) false merge-2-1-TupleFlattenVar~5266))))
(assert (= merge-2-1-b-proj-5~5236 (ite (= trans-6-2-result-proj-0 false) false (ite (= init-2-result-proj-0 false) false merge-2-1-TupleFlattenVar~5267))))
(assert (= merge-2-1-b-proj-6~5237 (ite (= trans-6-2-result-proj-0 false) false (ite (= init-2-result-proj-0 false) false merge-2-1-TupleFlattenVar~5268))))
(assert (= merge-2-1-b-proj-7~5238 (ite (= trans-6-2-result-proj-0 false) merge-2-1-b-proj-7~5260 (ite (= init-2-result-proj-0 false) merge-2-1-a-proj-7~5251 merge-2-1-TupleFlattenVar~5269))))
(assert (= merge-2-1-b-proj-8~5239 (ite (= trans-6-2-result-proj-0 false) merge-2-1-b-proj-8~5261 (ite (= init-2-result-proj-0 false) merge-2-1-a-proj-8~5252 merge-2-1-TupleFlattenVar~5270))))
(assert (= merge-2-1-o-proj-0~5215 (not (= assert-2-x-proj-12~5133 false))))
(assert (= merge-2-1-a~5227 (ite (= assert-2-x-proj-12~5133 false) 0 merge-2-1-o-proj-2~5242)))
(assert (= merge-2-1-b-proj-0~5217 (not (= assert-2-x-proj-0~5121 false))))
(assert (= merge-2-1-b~5228 (ite (= assert-2-x-proj-0~5121 false) 0 merge-2-1-b-proj-1~5232)))
(assert (= merge-2-1-x-proj-0~5219 (ite (ite (= assert-2-x-proj-19~5140 false) true (ite (= assert-2-x-proj-10~5131 false) false (<= merge-2-1-a~5229 merge-2-1-b~5230))) assert-2-x-proj-10~5131 assert-2-x-proj-19~5140)))
(assert (= merge-2-1-a~5225 (ite (ite (= assert-2-x-proj-19~5140 false) true (ite (= assert-2-x-proj-10~5131 false) false (<= merge-2-1-a~5229 merge-2-1-b~5230))) merge-2-1-a~5229 merge-2-1-b~5230)))
(assert (= merge-2-1-p1~5221 (ite (ite (= assert-2-x-proj-19~5140 false) true (ite (= assert-2-x-proj-10~5131 false) false (<= merge-2-1-a~5229 merge-2-1-b~5230))) 0 1)))
(assert (= merge-2-1-y-proj-0~5222 (ite (ite (= merge-2-1-b-proj-0~5217 false) true (ite (= merge-2-1-o-proj-0~5215 false) false (<= merge-2-1-a~5227 merge-2-1-b~5228))) merge-2-1-o-proj-0~5215 merge-2-1-b-proj-0~5217)))
(assert (= merge-2-1-b~5226 (ite (ite (= merge-2-1-b-proj-0~5217 false) true (ite (= merge-2-1-o-proj-0~5215 false) false (<= merge-2-1-a~5227 merge-2-1-b~5228))) merge-2-1-a~5227 merge-2-1-b~5228)))
(assert (= merge-2-1-p2~5224 (ite (ite (= merge-2-1-b-proj-0~5217 false) true (ite (= merge-2-1-o-proj-0~5215 false) false (<= merge-2-1-a~5227 merge-2-1-b~5228))) 2 3)))
(assert (= assert-2-x-proj-17~5138 (not (and (= assert-2-x-proj-0~5121 false) (and (= assert-2-x-proj-12~5133 false) (and (= assert-2-x-proj-19~5140 false) (= assert-2-x-proj-10~5131 false)))))))
(assert (= assert-2-x-proj-18~5139 (ite (and (= assert-2-x-proj-0~5121 false) (and (= assert-2-x-proj-12~5133 false) (and (= assert-2-x-proj-19~5140 false) (= assert-2-x-proj-10~5131 false)))) 0 (ite (ite (= merge-2-1-y-proj-0~5222 false) true (ite (= merge-2-1-x-proj-0~5219 false) false (<= merge-2-1-a~5225 merge-2-1-b~5226))) merge-2-1-p1~5221 merge-2-1-p2~5224))))
(assert (= assert-3-x-proj-10~5131 init-3-result-proj-5))
(assert (= merge-3-1-a~5229 0))
(assert (= assert-3-x-proj-19~5140 false))
(assert (= merge-3-1-b~5230 0))
(assert (= merge-3-1-TupleFlattenVar~5299 0))
(assert (= merge-3-1-TupleFlattenVar~5300 0))
(assert (= merge-3-1-TupleFlattenVar~5301 0))
(assert (= merge-3-1-TupleFlattenVar~5302 0))
(assert (= assert-3-x-proj-12~5133 false))
(assert (= merge-3-1-o-proj-0~5240 0))
(assert (= merge-3-1-o-proj-1~5241 0))
(assert (= merge-3-1-o-proj-2~5242 0))
(assert (= merge-3-1-o-proj-3~5243 0))
(assert (= merge-3-1-TupleFlattenVar~5262 (ite (< merge-3-1-b-proj-7~5260 merge-3-1-a-proj-7~5251) merge-3-1-a-proj-0~5244 (ite (< merge-3-1-a-proj-7~5251 merge-3-1-b-proj-7~5260) 0 (ite (< merge-3-1-a-proj-0~5244 0) merge-3-1-a-proj-0~5244 (ite (< 0 merge-3-1-a-proj-0~5244) 0 (ite (<= merge-3-1-b-proj-8~5261 merge-3-1-a-proj-8~5252) merge-3-1-a-proj-0~5244 0)))))))
(assert (= merge-3-1-TupleFlattenVar~5263 (ite (< merge-3-1-b-proj-7~5260 merge-3-1-a-proj-7~5251) merge-3-1-a-proj-1~5245 (ite (< merge-3-1-a-proj-7~5251 merge-3-1-b-proj-7~5260) merge-3-1-b-proj-1~5254 (ite (< merge-3-1-a-proj-0~5244 0) merge-3-1-a-proj-1~5245 (ite (< 0 merge-3-1-a-proj-0~5244) merge-3-1-b-proj-1~5254 (ite (<= merge-3-1-b-proj-8~5261 merge-3-1-a-proj-8~5252) merge-3-1-a-proj-1~5245 merge-3-1-b-proj-1~5254)))))))
(assert (= merge-3-1-TupleFlattenVar~5264 false))
(assert (= merge-3-1-TupleFlattenVar~5265 false))
(assert (= merge-3-1-TupleFlattenVar~5266 false))
(assert (= merge-3-1-TupleFlattenVar~5267 false))
(assert (= merge-3-1-TupleFlattenVar~5268 false))
(assert (= merge-3-1-TupleFlattenVar~5269 (ite (< merge-3-1-b-proj-7~5260 merge-3-1-a-proj-7~5251) merge-3-1-a-proj-7~5251 (ite (< merge-3-1-a-proj-7~5251 merge-3-1-b-proj-7~5260) merge-3-1-b-proj-7~5260 (ite (< merge-3-1-a-proj-0~5244 0) merge-3-1-a-proj-7~5251 (ite (< 0 merge-3-1-a-proj-0~5244) merge-3-1-b-proj-7~5260 (ite (<= merge-3-1-b-proj-8~5261 merge-3-1-a-proj-8~5252) merge-3-1-a-proj-7~5251 merge-3-1-b-proj-7~5260)))))))
(assert (= merge-3-1-TupleFlattenVar~5270 (ite (< merge-3-1-b-proj-7~5260 merge-3-1-a-proj-7~5251) merge-3-1-a-proj-8~5252 (ite (< merge-3-1-a-proj-7~5251 merge-3-1-b-proj-7~5260) merge-3-1-b-proj-8~5261 (ite (< merge-3-1-a-proj-0~5244 0) merge-3-1-a-proj-8~5252 (ite (< 0 merge-3-1-a-proj-0~5244) merge-3-1-b-proj-8~5261 (ite (<= merge-3-1-b-proj-8~5261 merge-3-1-a-proj-8~5252) merge-3-1-a-proj-8~5252 merge-3-1-b-proj-8~5261)))))))
(assert (= assert-3-x-proj-0~5121 (ite (= trans-13-3-result-proj-0 false) init-3-result-proj-0 (ite (= init-3-result-proj-0 false) trans-13-3-result-proj-0 true))))
(assert (= merge-3-1-b-proj-0~5231 (ite (= trans-13-3-result-proj-0 false) 0 (ite (= init-3-result-proj-0 false) merge-3-1-a-proj-0~5244 merge-3-1-TupleFlattenVar~5262))))
(assert (= merge-3-1-b-proj-1~5232 (ite (= trans-13-3-result-proj-0 false) merge-3-1-b-proj-1~5254 (ite (= init-3-result-proj-0 false) merge-3-1-a-proj-1~5245 merge-3-1-TupleFlattenVar~5263))))
(assert (= merge-3-1-b-proj-2~5233 (ite (= trans-13-3-result-proj-0 false) false (ite (= init-3-result-proj-0 false) false merge-3-1-TupleFlattenVar~5264))))
(assert (= merge-3-1-b-proj-3~5234 (ite (= trans-13-3-result-proj-0 false) false (ite (= init-3-result-proj-0 false) false merge-3-1-TupleFlattenVar~5265))))
(assert (= merge-3-1-b-proj-4~5235 (ite (= trans-13-3-result-proj-0 false) false (ite (= init-3-result-proj-0 false) false merge-3-1-TupleFlattenVar~5266))))
(assert (= merge-3-1-b-proj-5~5236 (ite (= trans-13-3-result-proj-0 false) false (ite (= init-3-result-proj-0 false) false merge-3-1-TupleFlattenVar~5267))))
(assert (= merge-3-1-b-proj-6~5237 (ite (= trans-13-3-result-proj-0 false) false (ite (= init-3-result-proj-0 false) false merge-3-1-TupleFlattenVar~5268))))
(assert (= merge-3-1-b-proj-7~5238 (ite (= trans-13-3-result-proj-0 false) merge-3-1-b-proj-7~5260 (ite (= init-3-result-proj-0 false) merge-3-1-a-proj-7~5251 merge-3-1-TupleFlattenVar~5269))))
(assert (= merge-3-1-b-proj-8~5239 (ite (= trans-13-3-result-proj-0 false) merge-3-1-b-proj-8~5261 (ite (= init-3-result-proj-0 false) merge-3-1-a-proj-8~5252 merge-3-1-TupleFlattenVar~5270))))
(assert (= merge-3-1-o-proj-0~5215 (not (= assert-3-x-proj-12~5133 false))))
(assert (= merge-3-1-a~5227 (ite (= assert-3-x-proj-12~5133 false) 0 merge-3-1-o-proj-2~5242)))
(assert (= merge-3-1-b-proj-0~5217 (not (= assert-3-x-proj-0~5121 false))))
(assert (= merge-3-1-b~5228 (ite (= assert-3-x-proj-0~5121 false) 0 merge-3-1-b-proj-1~5232)))
(assert (= merge-3-1-x-proj-0~5219 (ite (ite (= assert-3-x-proj-19~5140 false) true (ite (= assert-3-x-proj-10~5131 false) false (<= merge-3-1-a~5229 merge-3-1-b~5230))) assert-3-x-proj-10~5131 assert-3-x-proj-19~5140)))
(assert (= merge-3-1-a~5225 (ite (ite (= assert-3-x-proj-19~5140 false) true (ite (= assert-3-x-proj-10~5131 false) false (<= merge-3-1-a~5229 merge-3-1-b~5230))) merge-3-1-a~5229 merge-3-1-b~5230)))
(assert (= merge-3-1-p1~5221 (ite (ite (= assert-3-x-proj-19~5140 false) true (ite (= assert-3-x-proj-10~5131 false) false (<= merge-3-1-a~5229 merge-3-1-b~5230))) 0 1)))
(assert (= merge-3-1-y-proj-0~5222 (ite (ite (= merge-3-1-b-proj-0~5217 false) true (ite (= merge-3-1-o-proj-0~5215 false) false (<= merge-3-1-a~5227 merge-3-1-b~5228))) merge-3-1-o-proj-0~5215 merge-3-1-b-proj-0~5217)))
(assert (= merge-3-1-b~5226 (ite (ite (= merge-3-1-b-proj-0~5217 false) true (ite (= merge-3-1-o-proj-0~5215 false) false (<= merge-3-1-a~5227 merge-3-1-b~5228))) merge-3-1-a~5227 merge-3-1-b~5228)))
(assert (= merge-3-1-p2~5224 (ite (ite (= merge-3-1-b-proj-0~5217 false) true (ite (= merge-3-1-o-proj-0~5215 false) false (<= merge-3-1-a~5227 merge-3-1-b~5228))) 2 3)))
(assert (= assert-3-x-proj-17~5138 (not (and (= assert-3-x-proj-0~5121 false) (and (= assert-3-x-proj-12~5133 false) (and (= assert-3-x-proj-19~5140 false) (= assert-3-x-proj-10~5131 false)))))))
(assert (= assert-3-x-proj-18~5139 (ite (and (= assert-3-x-proj-0~5121 false) (and (= assert-3-x-proj-12~5133 false) (and (= assert-3-x-proj-19~5140 false) (= assert-3-x-proj-10~5131 false)))) 0 (ite (ite (= merge-3-1-y-proj-0~5222 false) true (ite (= merge-3-1-x-proj-0~5219 false) false (<= merge-3-1-a~5225 merge-3-1-b~5226))) merge-3-1-p1~5221 merge-3-1-p2~5224))))
(assert (= merge-4-1-result-proj-5 init-4-result-proj-5))
(assert (= merge-4-1-a~5229 0))
(assert (= merge-4-1-result-proj-13 false))
(assert (= merge-4-1-b~5230 0))
(assert (= merge-4-1-TupleFlattenVar~5299 0))
(assert (= merge-4-1-TupleFlattenVar~5300 0))
(assert (= merge-4-1-TupleFlattenVar~5301 0))
(assert (= merge-4-1-TupleFlattenVar~5302 0))
(assert (= merge-4-1-result-proj-7 false))
(assert (= merge-4-1-o-proj-0~5240 0))
(assert (= merge-4-1-o-proj-1~5241 0))
(assert (= merge-4-1-o-proj-2~5242 0))
(assert (= merge-4-1-o-proj-3~5243 0))
(assert (= merge-4-1-TupleFlattenVar~5262 (ite (< merge-4-1-b-proj-7~5260 merge-4-1-a-proj-7~5251) merge-4-1-a-proj-0~5244 (ite (< merge-4-1-a-proj-7~5251 merge-4-1-b-proj-7~5260) 0 (ite (< merge-4-1-a-proj-0~5244 0) merge-4-1-a-proj-0~5244 (ite (< 0 merge-4-1-a-proj-0~5244) 0 (ite (<= merge-4-1-b-proj-8~5261 merge-4-1-a-proj-8~5252) merge-4-1-a-proj-0~5244 0)))))))
(assert (= merge-4-1-TupleFlattenVar~5263 (ite (< merge-4-1-b-proj-7~5260 merge-4-1-a-proj-7~5251) merge-4-1-a-proj-1~5245 (ite (< merge-4-1-a-proj-7~5251 merge-4-1-b-proj-7~5260) merge-4-1-b-proj-1~5254 (ite (< merge-4-1-a-proj-0~5244 0) merge-4-1-a-proj-1~5245 (ite (< 0 merge-4-1-a-proj-0~5244) merge-4-1-b-proj-1~5254 (ite (<= merge-4-1-b-proj-8~5261 merge-4-1-a-proj-8~5252) merge-4-1-a-proj-1~5245 merge-4-1-b-proj-1~5254)))))))
(assert (= merge-4-1-TupleFlattenVar~5264 false))
(assert (= merge-4-1-TupleFlattenVar~5265 false))
(assert (= merge-4-1-TupleFlattenVar~5266 false))
(assert (= merge-4-1-TupleFlattenVar~5267 false))
(assert (= merge-4-1-TupleFlattenVar~5268 false))
(assert (= merge-4-1-TupleFlattenVar~5269 (ite (< merge-4-1-b-proj-7~5260 merge-4-1-a-proj-7~5251) merge-4-1-a-proj-7~5251 (ite (< merge-4-1-a-proj-7~5251 merge-4-1-b-proj-7~5260) merge-4-1-b-proj-7~5260 (ite (< merge-4-1-a-proj-0~5244 0) merge-4-1-a-proj-7~5251 (ite (< 0 merge-4-1-a-proj-0~5244) merge-4-1-b-proj-7~5260 (ite (<= merge-4-1-b-proj-8~5261 merge-4-1-a-proj-8~5252) merge-4-1-a-proj-7~5251 merge-4-1-b-proj-7~5260)))))))
(assert (= merge-4-1-TupleFlattenVar~5270 (ite (< merge-4-1-b-proj-7~5260 merge-4-1-a-proj-7~5251) merge-4-1-a-proj-8~5252 (ite (< merge-4-1-a-proj-7~5251 merge-4-1-b-proj-7~5260) merge-4-1-b-proj-8~5261 (ite (< merge-4-1-a-proj-0~5244 0) merge-4-1-a-proj-8~5252 (ite (< 0 merge-4-1-a-proj-0~5244) merge-4-1-b-proj-8~5261 (ite (<= merge-4-1-b-proj-8~5261 merge-4-1-a-proj-8~5252) merge-4-1-a-proj-8~5252 merge-4-1-b-proj-8~5261)))))))
(assert (= merge-4-1-result-proj-0 (ite (= trans-10-4-result-proj-0 false) init-4-result-proj-0 (ite (= init-4-result-proj-0 false) trans-10-4-result-proj-0 true))))
(assert (= merge-4-1-b-proj-0~5231 (ite (= trans-10-4-result-proj-0 false) 0 (ite (= init-4-result-proj-0 false) merge-4-1-a-proj-0~5244 merge-4-1-TupleFlattenVar~5262))))
(assert (= merge-4-1-b-proj-1~5232 (ite (= trans-10-4-result-proj-0 false) merge-4-1-b-proj-1~5254 (ite (= init-4-result-proj-0 false) merge-4-1-a-proj-1~5245 merge-4-1-TupleFlattenVar~5263))))
(assert (= merge-4-1-b-proj-2~5233 (ite (= trans-10-4-result-proj-0 false) false (ite (= init-4-result-proj-0 false) false merge-4-1-TupleFlattenVar~5264))))
(assert (= merge-4-1-b-proj-3~5234 (ite (= trans-10-4-result-proj-0 false) false (ite (= init-4-result-proj-0 false) false merge-4-1-TupleFlattenVar~5265))))
(assert (= merge-4-1-b-proj-4~5235 (ite (= trans-10-4-result-proj-0 false) false (ite (= init-4-result-proj-0 false) false merge-4-1-TupleFlattenVar~5266))))
(assert (= merge-4-1-b-proj-5~5236 (ite (= trans-10-4-result-proj-0 false) false (ite (= init-4-result-proj-0 false) false merge-4-1-TupleFlattenVar~5267))))
(assert (= merge-4-1-b-proj-6~5237 (ite (= trans-10-4-result-proj-0 false) false (ite (= init-4-result-proj-0 false) false merge-4-1-TupleFlattenVar~5268))))
(assert (= merge-4-1-b-proj-7~5238 (ite (= trans-10-4-result-proj-0 false) merge-4-1-b-proj-7~5260 (ite (= init-4-result-proj-0 false) merge-4-1-a-proj-7~5251 merge-4-1-TupleFlattenVar~5269))))
(assert (= merge-4-1-b-proj-8~5239 (ite (= trans-10-4-result-proj-0 false) merge-4-1-b-proj-8~5261 (ite (= init-4-result-proj-0 false) merge-4-1-a-proj-8~5252 merge-4-1-TupleFlattenVar~5270))))
(assert (= merge-4-1-o-proj-0~5215 (not (= merge-4-1-result-proj-7 false))))
(assert (= merge-4-1-a~5227 (ite (= merge-4-1-result-proj-7 false) 0 merge-4-1-o-proj-2~5242)))
(assert (= merge-4-1-b-proj-0~5217 (not (= merge-4-1-result-proj-0 false))))
(assert (= merge-4-1-b~5228 (ite (= merge-4-1-result-proj-0 false) 0 merge-4-1-b-proj-1~5232)))
(assert (= merge-4-1-x-proj-0~5219 (ite (ite (= merge-4-1-result-proj-13 false) true (ite (= merge-4-1-result-proj-5 false) false (<= merge-4-1-a~5229 merge-4-1-b~5230))) merge-4-1-result-proj-5 merge-4-1-result-proj-13)))
(assert (= merge-4-1-a~5225 (ite (ite (= merge-4-1-result-proj-13 false) true (ite (= merge-4-1-result-proj-5 false) false (<= merge-4-1-a~5229 merge-4-1-b~5230))) merge-4-1-a~5229 merge-4-1-b~5230)))
(assert (= merge-4-1-p1~5221 (ite (ite (= merge-4-1-result-proj-13 false) true (ite (= merge-4-1-result-proj-5 false) false (<= merge-4-1-a~5229 merge-4-1-b~5230))) 0 1)))
(assert (= merge-4-1-y-proj-0~5222 (ite (ite (= merge-4-1-b-proj-0~5217 false) true (ite (= merge-4-1-o-proj-0~5215 false) false (<= merge-4-1-a~5227 merge-4-1-b~5228))) merge-4-1-o-proj-0~5215 merge-4-1-b-proj-0~5217)))
(assert (= merge-4-1-b~5226 (ite (ite (= merge-4-1-b-proj-0~5217 false) true (ite (= merge-4-1-o-proj-0~5215 false) false (<= merge-4-1-a~5227 merge-4-1-b~5228))) merge-4-1-a~5227 merge-4-1-b~5228)))
(assert (= merge-4-1-p2~5224 (ite (ite (= merge-4-1-b-proj-0~5217 false) true (ite (= merge-4-1-o-proj-0~5215 false) false (<= merge-4-1-a~5227 merge-4-1-b~5228))) 2 3)))
(assert (= merge-4-1-result-proj-11 (not (and (= merge-4-1-result-proj-0 false) (and (= merge-4-1-result-proj-7 false) (and (= merge-4-1-result-proj-13 false) (= merge-4-1-result-proj-5 false)))))))
(assert (= merge-4-1-result-proj-12 (ite (and (= merge-4-1-result-proj-0 false) (and (= merge-4-1-result-proj-7 false) (and (= merge-4-1-result-proj-13 false) (= merge-4-1-result-proj-5 false)))) 0 (ite (ite (= merge-4-1-y-proj-0~5222 false) true (ite (= merge-4-1-x-proj-0~5219 false) false (<= merge-4-1-a~5225 merge-4-1-b~5226))) merge-4-1-p1~5221 merge-4-1-p2~5224))))
(assert (= assert-4-x-proj-10~5131 merge-4-1-result-proj-5))
(assert (= merge-4-2-a~5229 merge-4-1-a~5229))
(assert (= assert-4-x-proj-19~5140 merge-4-1-result-proj-13))
(assert (= merge-4-2-b~5230 merge-4-1-b~5230))
(assert (= merge-4-2-TupleFlattenVar~5299 0))
(assert (= merge-4-2-TupleFlattenVar~5300 (ite (< merge-4-1-o-proj-1~5241 0) 0 (ite (< 0 merge-4-1-o-proj-1~5241) merge-4-1-o-proj-1~5241 (ite (<= 0 merge-4-1-o-proj-3~5243) 0 merge-4-1-o-proj-1~5241)))))
(assert (= merge-4-2-TupleFlattenVar~5301 (ite (< merge-4-1-o-proj-1~5241 0) 0 (ite (< 0 merge-4-1-o-proj-1~5241) merge-4-1-o-proj-2~5242 (ite (<= 0 merge-4-1-o-proj-3~5243) 0 merge-4-1-o-proj-2~5242)))))
(assert (= merge-4-2-TupleFlattenVar~5302 (ite (< merge-4-1-o-proj-1~5241 0) 0 (ite (< 0 merge-4-1-o-proj-1~5241) merge-4-1-o-proj-3~5243 (ite (<= 0 merge-4-1-o-proj-3~5243) 0 merge-4-1-o-proj-3~5243)))))
(assert (= assert-4-x-proj-12~5133 merge-4-1-result-proj-7))
(assert (= merge-4-2-o-proj-0~5240 0))
(assert (= trans-4-8-o-proj-1~6241 merge-4-1-o-proj-1~5241))
(assert (= trans-4-8-o-proj-2~6242 merge-4-1-o-proj-2~5242))
(assert (= trans-4-8-o-proj-3~6243 merge-4-1-o-proj-3~5243))
(assert (= merge-4-2-TupleFlattenVar~5262 (ite (< merge-4-1-b-proj-7~5238 merge-4-2-a-proj-7~5251) merge-4-2-a-proj-0~5244 (ite (< merge-4-2-a-proj-7~5251 merge-4-1-b-proj-7~5238) merge-4-1-b-proj-0~5231 (ite (< merge-4-2-a-proj-0~5244 merge-4-1-b-proj-0~5231) merge-4-2-a-proj-0~5244 (ite (< merge-4-1-b-proj-0~5231 merge-4-2-a-proj-0~5244) merge-4-1-b-proj-0~5231 (ite (<= merge-4-1-b-proj-8~5239 merge-4-2-a-proj-8~5252) merge-4-2-a-proj-0~5244 merge-4-1-b-proj-0~5231)))))))
(assert (= merge-4-2-TupleFlattenVar~5263 (ite (< merge-4-1-b-proj-7~5238 merge-4-2-a-proj-7~5251) merge-4-2-a-proj-1~5245 (ite (< merge-4-2-a-proj-7~5251 merge-4-1-b-proj-7~5238) merge-4-1-b-proj-1~5232 (ite (< merge-4-2-a-proj-0~5244 merge-4-1-b-proj-0~5231) merge-4-2-a-proj-1~5245 (ite (< merge-4-1-b-proj-0~5231 merge-4-2-a-proj-0~5244) merge-4-1-b-proj-1~5232 (ite (<= merge-4-1-b-proj-8~5239 merge-4-2-a-proj-8~5252) merge-4-2-a-proj-1~5245 merge-4-1-b-proj-1~5232)))))))
(assert (= merge-4-2-TupleFlattenVar~5264 false))
(assert (= merge-4-2-TupleFlattenVar~5265 false))
(assert (= merge-4-2-TupleFlattenVar~5266 false))
(assert (= merge-4-2-TupleFlattenVar~5267 false))
(assert (= merge-4-2-TupleFlattenVar~5268 false))
(assert (= merge-4-2-TupleFlattenVar~5269 (ite (< merge-4-1-b-proj-7~5238 merge-4-2-a-proj-7~5251) merge-4-2-a-proj-7~5251 (ite (< merge-4-2-a-proj-7~5251 merge-4-1-b-proj-7~5238) merge-4-1-b-proj-7~5238 (ite (< merge-4-2-a-proj-0~5244 merge-4-1-b-proj-0~5231) merge-4-2-a-proj-7~5251 (ite (< merge-4-1-b-proj-0~5231 merge-4-2-a-proj-0~5244) merge-4-1-b-proj-7~5238 (ite (<= merge-4-1-b-proj-8~5239 merge-4-2-a-proj-8~5252) merge-4-2-a-proj-7~5251 merge-4-1-b-proj-7~5238)))))))
(assert (= merge-4-2-TupleFlattenVar~5270 (ite (< merge-4-1-b-proj-7~5238 merge-4-2-a-proj-7~5251) merge-4-2-a-proj-8~5252 (ite (< merge-4-2-a-proj-7~5251 merge-4-1-b-proj-7~5238) merge-4-1-b-proj-8~5239 (ite (< merge-4-2-a-proj-0~5244 merge-4-1-b-proj-0~5231) merge-4-2-a-proj-8~5252 (ite (< merge-4-1-b-proj-0~5231 merge-4-2-a-proj-0~5244) merge-4-1-b-proj-8~5239 (ite (<= merge-4-1-b-proj-8~5239 merge-4-2-a-proj-8~5252) merge-4-2-a-proj-8~5252 merge-4-1-b-proj-8~5239)))))))
(assert (= assert-4-x-proj-0~5121 (ite (= trans-8-4-result-proj-0 false) merge-4-1-result-proj-0 (ite (= merge-4-1-result-proj-0 false) trans-8-4-result-proj-0 true))))
(assert (= merge-4-2-b-proj-0~5231 (ite (= trans-8-4-result-proj-0 false) merge-4-1-b-proj-0~5231 (ite (= merge-4-1-result-proj-0 false) merge-4-2-a-proj-0~5244 merge-4-2-TupleFlattenVar~5262))))
(assert (= merge-4-2-b-proj-1~5232 (ite (= trans-8-4-result-proj-0 false) merge-4-1-b-proj-1~5232 (ite (= merge-4-1-result-proj-0 false) merge-4-2-a-proj-1~5245 merge-4-2-TupleFlattenVar~5263))))
(assert (= merge-4-2-b-proj-2~5233 (ite (= trans-8-4-result-proj-0 false) false (ite (= merge-4-1-result-proj-0 false) false merge-4-2-TupleFlattenVar~5264))))
(assert (= merge-4-2-b-proj-3~5234 (ite (= trans-8-4-result-proj-0 false) false (ite (= merge-4-1-result-proj-0 false) false merge-4-2-TupleFlattenVar~5265))))
(assert (= merge-4-2-b-proj-4~5235 (ite (= trans-8-4-result-proj-0 false) false (ite (= merge-4-1-result-proj-0 false) false merge-4-2-TupleFlattenVar~5266))))
(assert (= merge-4-2-b-proj-5~5236 (ite (= trans-8-4-result-proj-0 false) false (ite (= merge-4-1-result-proj-0 false) false merge-4-2-TupleFlattenVar~5267))))
(assert (= merge-4-2-b-proj-6~5237 (ite (= trans-8-4-result-proj-0 false) false (ite (= merge-4-1-result-proj-0 false) false merge-4-2-TupleFlattenVar~5268))))
(assert (= merge-4-2-b-proj-7~5238 (ite (= trans-8-4-result-proj-0 false) merge-4-1-b-proj-7~5238 (ite (= merge-4-1-result-proj-0 false) merge-4-2-a-proj-7~5251 merge-4-2-TupleFlattenVar~5269))))
(assert (= merge-4-2-b-proj-8~5239 (ite (= trans-8-4-result-proj-0 false) merge-4-1-b-proj-8~5239 (ite (= merge-4-1-result-proj-0 false) merge-4-2-a-proj-8~5252 merge-4-2-TupleFlattenVar~5270))))
(assert (= merge-4-2-o-proj-0~5215 (not (= assert-4-x-proj-12~5133 false))))
(assert (= merge-4-2-a~5227 (ite (= assert-4-x-proj-12~5133 false) 0 trans-4-8-o-proj-2~6242)))
(assert (= merge-4-2-b-proj-0~5217 (not (= assert-4-x-proj-0~5121 false))))
(assert (= merge-4-2-b~5228 (ite (= assert-4-x-proj-0~5121 false) 0 merge-4-2-b-proj-1~5232)))
(assert (= merge-4-2-x-proj-0~5219 (ite (ite (= assert-4-x-proj-19~5140 false) true (ite (= assert-4-x-proj-10~5131 false) false (<= merge-4-2-a~5229 merge-4-2-b~5230))) assert-4-x-proj-10~5131 assert-4-x-proj-19~5140)))
(assert (= merge-4-2-a~5225 (ite (ite (= assert-4-x-proj-19~5140 false) true (ite (= assert-4-x-proj-10~5131 false) false (<= merge-4-2-a~5229 merge-4-2-b~5230))) merge-4-2-a~5229 merge-4-2-b~5230)))
(assert (= merge-4-2-p1~5221 (ite (ite (= assert-4-x-proj-19~5140 false) true (ite (= assert-4-x-proj-10~5131 false) false (<= merge-4-2-a~5229 merge-4-2-b~5230))) 0 1)))
(assert (= merge-4-2-y-proj-0~5222 (ite (ite (= merge-4-2-b-proj-0~5217 false) true (ite (= merge-4-2-o-proj-0~5215 false) false (<= merge-4-2-a~5227 merge-4-2-b~5228))) merge-4-2-o-proj-0~5215 merge-4-2-b-proj-0~5217)))
(assert (= merge-4-2-b~5226 (ite (ite (= merge-4-2-b-proj-0~5217 false) true (ite (= merge-4-2-o-proj-0~5215 false) false (<= merge-4-2-a~5227 merge-4-2-b~5228))) merge-4-2-a~5227 merge-4-2-b~5228)))
(assert (= merge-4-2-p2~5224 (ite (ite (= merge-4-2-b-proj-0~5217 false) true (ite (= merge-4-2-o-proj-0~5215 false) false (<= merge-4-2-a~5227 merge-4-2-b~5228))) 2 3)))
(assert (= assert-4-x-proj-17~5138 (not (and (= assert-4-x-proj-0~5121 false) (and (= assert-4-x-proj-12~5133 false) (and (= assert-4-x-proj-19~5140 false) (= assert-4-x-proj-10~5131 false)))))))
(assert (= trans-4-8-y~5639 (ite (and (= assert-4-x-proj-0~5121 false) (and (= assert-4-x-proj-12~5133 false) (and (= assert-4-x-proj-19~5140 false) (= assert-4-x-proj-10~5131 false)))) 0 (ite (ite (= merge-4-2-y-proj-0~5222 false) true (ite (= merge-4-2-x-proj-0~5219 false) false (<= merge-4-2-a~5225 merge-4-2-b~5226))) merge-4-2-p1~5221 merge-4-2-p2~5224))))
(assert (= assert-8-x-proj-10~5131 init-8-result-proj-5))
(assert (= merge-8-1-a~5229 0))
(assert (= assert-8-x-proj-19~5140 false))
(assert (= merge-8-1-b~5230 0))
(assert (= merge-8-1-TupleFlattenVar~5299 0))
(assert (= merge-8-1-TupleFlattenVar~5300 0))
(assert (= merge-8-1-TupleFlattenVar~5301 0))
(assert (= merge-8-1-TupleFlattenVar~5302 0))
(assert (= assert-8-x-proj-12~5133 false))
(assert (= merge-8-1-o-proj-0~5240 0))
(assert (= trans-8-4-o-proj-1~6241 0))
(assert (= trans-8-4-o-proj-2~6242 0))
(assert (= trans-8-4-o-proj-3~6243 0))
(assert (= merge-8-1-TupleFlattenVar~5262 (ite (< merge-8-1-b-proj-7~5260 merge-8-1-a-proj-7~5251) merge-8-1-a-proj-0~5244 (ite (< merge-8-1-a-proj-7~5251 merge-8-1-b-proj-7~5260) 0 (ite (< merge-8-1-a-proj-0~5244 0) merge-8-1-a-proj-0~5244 (ite (< 0 merge-8-1-a-proj-0~5244) 0 (ite (<= merge-8-1-b-proj-8~5261 merge-8-1-a-proj-8~5252) merge-8-1-a-proj-0~5244 0)))))))
(assert (= merge-8-1-TupleFlattenVar~5263 (ite (< merge-8-1-b-proj-7~5260 merge-8-1-a-proj-7~5251) merge-8-1-a-proj-1~5245 (ite (< merge-8-1-a-proj-7~5251 merge-8-1-b-proj-7~5260) merge-8-1-b-proj-1~5254 (ite (< merge-8-1-a-proj-0~5244 0) merge-8-1-a-proj-1~5245 (ite (< 0 merge-8-1-a-proj-0~5244) merge-8-1-b-proj-1~5254 (ite (<= merge-8-1-b-proj-8~5261 merge-8-1-a-proj-8~5252) merge-8-1-a-proj-1~5245 merge-8-1-b-proj-1~5254)))))))
(assert (= merge-8-1-TupleFlattenVar~5264 false))
(assert (= merge-8-1-TupleFlattenVar~5265 false))
(assert (= merge-8-1-TupleFlattenVar~5266 false))
(assert (= merge-8-1-TupleFlattenVar~5267 false))
(assert (= merge-8-1-TupleFlattenVar~5268 false))
(assert (= merge-8-1-TupleFlattenVar~5269 (ite (< merge-8-1-b-proj-7~5260 merge-8-1-a-proj-7~5251) merge-8-1-a-proj-7~5251 (ite (< merge-8-1-a-proj-7~5251 merge-8-1-b-proj-7~5260) merge-8-1-b-proj-7~5260 (ite (< merge-8-1-a-proj-0~5244 0) merge-8-1-a-proj-7~5251 (ite (< 0 merge-8-1-a-proj-0~5244) merge-8-1-b-proj-7~5260 (ite (<= merge-8-1-b-proj-8~5261 merge-8-1-a-proj-8~5252) merge-8-1-a-proj-7~5251 merge-8-1-b-proj-7~5260)))))))
(assert (= merge-8-1-TupleFlattenVar~5270 (ite (< merge-8-1-b-proj-7~5260 merge-8-1-a-proj-7~5251) merge-8-1-a-proj-8~5252 (ite (< merge-8-1-a-proj-7~5251 merge-8-1-b-proj-7~5260) merge-8-1-b-proj-8~5261 (ite (< merge-8-1-a-proj-0~5244 0) merge-8-1-a-proj-8~5252 (ite (< 0 merge-8-1-a-proj-0~5244) merge-8-1-b-proj-8~5261 (ite (<= merge-8-1-b-proj-8~5261 merge-8-1-a-proj-8~5252) merge-8-1-a-proj-8~5252 merge-8-1-b-proj-8~5261)))))))
(assert (= assert-8-x-proj-0~5121 (ite (= trans-4-8-result-proj-0 false) init-8-result-proj-0 (ite (= init-8-result-proj-0 false) trans-4-8-result-proj-0 true))))
(assert (= merge-8-1-b-proj-0~5231 (ite (= trans-4-8-result-proj-0 false) 0 (ite (= init-8-result-proj-0 false) merge-8-1-a-proj-0~5244 merge-8-1-TupleFlattenVar~5262))))
(assert (= merge-8-1-b-proj-1~5232 (ite (= trans-4-8-result-proj-0 false) merge-8-1-b-proj-1~5254 (ite (= init-8-result-proj-0 false) merge-8-1-a-proj-1~5245 merge-8-1-TupleFlattenVar~5263))))
(assert (= merge-8-1-b-proj-2~5233 (ite (= trans-4-8-result-proj-0 false) false (ite (= init-8-result-proj-0 false) false merge-8-1-TupleFlattenVar~5264))))
(assert (= merge-8-1-b-proj-3~5234 (ite (= trans-4-8-result-proj-0 false) false (ite (= init-8-result-proj-0 false) false merge-8-1-TupleFlattenVar~5265))))
(assert (= merge-8-1-b-proj-4~5235 (ite (= trans-4-8-result-proj-0 false) false (ite (= init-8-result-proj-0 false) false merge-8-1-TupleFlattenVar~5266))))
(assert (= merge-8-1-b-proj-5~5236 (ite (= trans-4-8-result-proj-0 false) false (ite (= init-8-result-proj-0 false) false merge-8-1-TupleFlattenVar~5267))))
(assert (= merge-8-1-b-proj-6~5237 (ite (= trans-4-8-result-proj-0 false) false (ite (= init-8-result-proj-0 false) false merge-8-1-TupleFlattenVar~5268))))
(assert (= merge-8-1-b-proj-7~5238 (ite (= trans-4-8-result-proj-0 false) merge-8-1-b-proj-7~5260 (ite (= init-8-result-proj-0 false) merge-8-1-a-proj-7~5251 merge-8-1-TupleFlattenVar~5269))))
(assert (= merge-8-1-b-proj-8~5239 (ite (= trans-4-8-result-proj-0 false) merge-8-1-b-proj-8~5261 (ite (= init-8-result-proj-0 false) merge-8-1-a-proj-8~5252 merge-8-1-TupleFlattenVar~5270))))
(assert (= merge-8-1-o-proj-0~5215 (not (= assert-8-x-proj-12~5133 false))))
(assert (= merge-8-1-a~5227 (ite (= assert-8-x-proj-12~5133 false) 0 trans-8-4-o-proj-2~6242)))
(assert (= merge-8-1-b-proj-0~5217 (not (= assert-8-x-proj-0~5121 false))))
(assert (= merge-8-1-b~5228 (ite (= assert-8-x-proj-0~5121 false) 0 merge-8-1-b-proj-1~5232)))
(assert (= merge-8-1-x-proj-0~5219 (ite (ite (= assert-8-x-proj-19~5140 false) true (ite (= assert-8-x-proj-10~5131 false) false (<= merge-8-1-a~5229 merge-8-1-b~5230))) assert-8-x-proj-10~5131 assert-8-x-proj-19~5140)))
(assert (= merge-8-1-a~5225 (ite (ite (= assert-8-x-proj-19~5140 false) true (ite (= assert-8-x-proj-10~5131 false) false (<= merge-8-1-a~5229 merge-8-1-b~5230))) merge-8-1-a~5229 merge-8-1-b~5230)))
(assert (= merge-8-1-p1~5221 (ite (ite (= assert-8-x-proj-19~5140 false) true (ite (= assert-8-x-proj-10~5131 false) false (<= merge-8-1-a~5229 merge-8-1-b~5230))) 0 1)))
(assert (= merge-8-1-y-proj-0~5222 (ite (ite (= merge-8-1-b-proj-0~5217 false) true (ite (= merge-8-1-o-proj-0~5215 false) false (<= merge-8-1-a~5227 merge-8-1-b~5228))) merge-8-1-o-proj-0~5215 merge-8-1-b-proj-0~5217)))
(assert (= merge-8-1-b~5226 (ite (ite (= merge-8-1-b-proj-0~5217 false) true (ite (= merge-8-1-o-proj-0~5215 false) false (<= merge-8-1-a~5227 merge-8-1-b~5228))) merge-8-1-a~5227 merge-8-1-b~5228)))
(assert (= merge-8-1-p2~5224 (ite (ite (= merge-8-1-b-proj-0~5217 false) true (ite (= merge-8-1-o-proj-0~5215 false) false (<= merge-8-1-a~5227 merge-8-1-b~5228))) 2 3)))
(assert (= assert-8-x-proj-17~5138 (not (and (= assert-8-x-proj-0~5121 false) (and (= assert-8-x-proj-12~5133 false) (and (= assert-8-x-proj-19~5140 false) (= assert-8-x-proj-10~5131 false)))))))
(assert (= trans-8-4-y~5819 (ite (and (= assert-8-x-proj-0~5121 false) (and (= assert-8-x-proj-12~5133 false) (and (= assert-8-x-proj-19~5140 false) (= assert-8-x-proj-10~5131 false)))) 0 (ite (ite (= merge-8-1-y-proj-0~5222 false) true (ite (= merge-8-1-x-proj-0~5219 false) false (<= merge-8-1-a~5225 merge-8-1-b~5226))) merge-8-1-p1~5221 merge-8-1-p2~5224))))
(assert (= assert-9-x-proj-10~5131 init-9-result-proj-5))
(assert (= merge-9-1-a~5229 0))
(assert (= assert-9-x-proj-19~5140 false))
(assert (= merge-9-1-b~5230 0))
(assert (= merge-9-1-TupleFlattenVar~5299 0))
(assert (= merge-9-1-TupleFlattenVar~5300 0))
(assert (= merge-9-1-TupleFlattenVar~5301 0))
(assert (= merge-9-1-TupleFlattenVar~5302 0))
(assert (= assert-9-x-proj-12~5133 false))
(assert (= merge-9-1-o-proj-0~5240 0))
(assert (= merge-9-1-o-proj-1~5241 0))
(assert (= merge-9-1-o-proj-2~5242 0))
(assert (= merge-9-1-o-proj-3~5243 0))
(assert (= merge-9-1-TupleFlattenVar~5262 (ite (< merge-9-1-b-proj-7~5260 merge-9-1-a-proj-7~5251) merge-9-1-a-proj-0~5244 (ite (< merge-9-1-a-proj-7~5251 merge-9-1-b-proj-7~5260) 0 (ite (< merge-9-1-a-proj-0~5244 0) merge-9-1-a-proj-0~5244 (ite (< 0 merge-9-1-a-proj-0~5244) 0 (ite (<= merge-9-1-b-proj-8~5261 merge-9-1-a-proj-8~5252) merge-9-1-a-proj-0~5244 0)))))))
(assert (= merge-9-1-TupleFlattenVar~5263 (ite (< merge-9-1-b-proj-7~5260 merge-9-1-a-proj-7~5251) merge-9-1-a-proj-1~5245 (ite (< merge-9-1-a-proj-7~5251 merge-9-1-b-proj-7~5260) merge-9-1-b-proj-1~5254 (ite (< merge-9-1-a-proj-0~5244 0) merge-9-1-a-proj-1~5245 (ite (< 0 merge-9-1-a-proj-0~5244) merge-9-1-b-proj-1~5254 (ite (<= merge-9-1-b-proj-8~5261 merge-9-1-a-proj-8~5252) merge-9-1-a-proj-1~5245 merge-9-1-b-proj-1~5254)))))))
(assert (= merge-9-1-TupleFlattenVar~5264 false))
(assert (= merge-9-1-TupleFlattenVar~5265 false))
(assert (= merge-9-1-TupleFlattenVar~5266 false))
(assert (= merge-9-1-TupleFlattenVar~5267 false))
(assert (= merge-9-1-TupleFlattenVar~5268 false))
(assert (= merge-9-1-TupleFlattenVar~5269 (ite (< merge-9-1-b-proj-7~5260 merge-9-1-a-proj-7~5251) merge-9-1-a-proj-7~5251 (ite (< merge-9-1-a-proj-7~5251 merge-9-1-b-proj-7~5260) merge-9-1-b-proj-7~5260 (ite (< merge-9-1-a-proj-0~5244 0) merge-9-1-a-proj-7~5251 (ite (< 0 merge-9-1-a-proj-0~5244) merge-9-1-b-proj-7~5260 (ite (<= merge-9-1-b-proj-8~5261 merge-9-1-a-proj-8~5252) merge-9-1-a-proj-7~5251 merge-9-1-b-proj-7~5260)))))))
(assert (= merge-9-1-TupleFlattenVar~5270 (ite (< merge-9-1-b-proj-7~5260 merge-9-1-a-proj-7~5251) merge-9-1-a-proj-8~5252 (ite (< merge-9-1-a-proj-7~5251 merge-9-1-b-proj-7~5260) merge-9-1-b-proj-8~5261 (ite (< merge-9-1-a-proj-0~5244 0) merge-9-1-a-proj-8~5252 (ite (< 0 merge-9-1-a-proj-0~5244) merge-9-1-b-proj-8~5261 (ite (<= merge-9-1-b-proj-8~5261 merge-9-1-a-proj-8~5252) merge-9-1-a-proj-8~5252 merge-9-1-b-proj-8~5261)))))))
(assert (= assert-9-x-proj-0~5121 (ite (= trans-7-9-result-proj-0 false) init-9-result-proj-0 (ite (= init-9-result-proj-0 false) trans-7-9-result-proj-0 true))))
(assert (= merge-9-1-b-proj-0~5231 (ite (= trans-7-9-result-proj-0 false) 0 (ite (= init-9-result-proj-0 false) merge-9-1-a-proj-0~5244 merge-9-1-TupleFlattenVar~5262))))
(assert (= merge-9-1-b-proj-1~5232 (ite (= trans-7-9-result-proj-0 false) merge-9-1-b-proj-1~5254 (ite (= init-9-result-proj-0 false) merge-9-1-a-proj-1~5245 merge-9-1-TupleFlattenVar~5263))))
(assert (= merge-9-1-b-proj-2~5233 (ite (= trans-7-9-result-proj-0 false) false (ite (= init-9-result-proj-0 false) false merge-9-1-TupleFlattenVar~5264))))
(assert (= merge-9-1-b-proj-3~5234 (ite (= trans-7-9-result-proj-0 false) false (ite (= init-9-result-proj-0 false) false merge-9-1-TupleFlattenVar~5265))))
(assert (= merge-9-1-b-proj-4~5235 (ite (= trans-7-9-result-proj-0 false) false (ite (= init-9-result-proj-0 false) false merge-9-1-TupleFlattenVar~5266))))
(assert (= merge-9-1-b-proj-5~5236 (ite (= trans-7-9-result-proj-0 false) false (ite (= init-9-result-proj-0 false) false merge-9-1-TupleFlattenVar~5267))))
(assert (= merge-9-1-b-proj-6~5237 (ite (= trans-7-9-result-proj-0 false) false (ite (= init-9-result-proj-0 false) false merge-9-1-TupleFlattenVar~5268))))
(assert (= merge-9-1-b-proj-7~5238 (ite (= trans-7-9-result-proj-0 false) merge-9-1-b-proj-7~5260 (ite (= init-9-result-proj-0 false) merge-9-1-a-proj-7~5251 merge-9-1-TupleFlattenVar~5269))))
(assert (= merge-9-1-b-proj-8~5239 (ite (= trans-7-9-result-proj-0 false) merge-9-1-b-proj-8~5261 (ite (= init-9-result-proj-0 false) merge-9-1-a-proj-8~5252 merge-9-1-TupleFlattenVar~5270))))
(assert (= merge-9-1-o-proj-0~5215 (not (= assert-9-x-proj-12~5133 false))))
(assert (= merge-9-1-a~5227 (ite (= assert-9-x-proj-12~5133 false) 0 merge-9-1-o-proj-2~5242)))
(assert (= merge-9-1-b-proj-0~5217 (not (= assert-9-x-proj-0~5121 false))))
(assert (= merge-9-1-b~5228 (ite (= assert-9-x-proj-0~5121 false) 0 merge-9-1-b-proj-1~5232)))
(assert (= merge-9-1-x-proj-0~5219 (ite (ite (= assert-9-x-proj-19~5140 false) true (ite (= assert-9-x-proj-10~5131 false) false (<= merge-9-1-a~5229 merge-9-1-b~5230))) assert-9-x-proj-10~5131 assert-9-x-proj-19~5140)))
(assert (= merge-9-1-a~5225 (ite (ite (= assert-9-x-proj-19~5140 false) true (ite (= assert-9-x-proj-10~5131 false) false (<= merge-9-1-a~5229 merge-9-1-b~5230))) merge-9-1-a~5229 merge-9-1-b~5230)))
(assert (= merge-9-1-p1~5221 (ite (ite (= assert-9-x-proj-19~5140 false) true (ite (= assert-9-x-proj-10~5131 false) false (<= merge-9-1-a~5229 merge-9-1-b~5230))) 0 1)))
(assert (= merge-9-1-y-proj-0~5222 (ite (ite (= merge-9-1-b-proj-0~5217 false) true (ite (= merge-9-1-o-proj-0~5215 false) false (<= merge-9-1-a~5227 merge-9-1-b~5228))) merge-9-1-o-proj-0~5215 merge-9-1-b-proj-0~5217)))
(assert (= merge-9-1-b~5226 (ite (ite (= merge-9-1-b-proj-0~5217 false) true (ite (= merge-9-1-o-proj-0~5215 false) false (<= merge-9-1-a~5227 merge-9-1-b~5228))) merge-9-1-a~5227 merge-9-1-b~5228)))
(assert (= merge-9-1-p2~5224 (ite (ite (= merge-9-1-b-proj-0~5217 false) true (ite (= merge-9-1-o-proj-0~5215 false) false (<= merge-9-1-a~5227 merge-9-1-b~5228))) 2 3)))
(assert (= assert-9-x-proj-17~5138 (not (and (= assert-9-x-proj-0~5121 false) (and (= assert-9-x-proj-12~5133 false) (and (= assert-9-x-proj-19~5140 false) (= assert-9-x-proj-10~5131 false)))))))
(assert (= assert-9-x-proj-18~5139 (ite (and (= assert-9-x-proj-0~5121 false) (and (= assert-9-x-proj-12~5133 false) (and (= assert-9-x-proj-19~5140 false) (= assert-9-x-proj-10~5131 false)))) 0 (ite (ite (= merge-9-1-y-proj-0~5222 false) true (ite (= merge-9-1-x-proj-0~5219 false) false (<= merge-9-1-a~5225 merge-9-1-b~5226))) merge-9-1-p1~5221 merge-9-1-p2~5224))))
(assert (= assert-11-x-proj-10~5131 init-11-result-proj-5))
(assert (= merge-11-1-a~5229 0))
(assert (= assert-11-x-proj-19~5140 false))
(assert (= merge-11-1-b~5230 0))
(assert (= merge-11-1-TupleFlattenVar~5299 0))
(assert (= merge-11-1-TupleFlattenVar~5300 0))
(assert (= merge-11-1-TupleFlattenVar~5301 0))
(assert (= merge-11-1-TupleFlattenVar~5302 0))
(assert (= assert-11-x-proj-12~5133 false))
(assert (= merge-11-1-o-proj-0~5240 0))
(assert (= merge-11-1-o-proj-1~5241 0))
(assert (= merge-11-1-o-proj-2~5242 0))
(assert (= merge-11-1-o-proj-3~5243 0))
(assert (= merge-11-1-TupleFlattenVar~5262 (ite (< merge-11-1-b-proj-7~5260 merge-11-1-a-proj-7~5251) merge-11-1-a-proj-0~5244 (ite (< merge-11-1-a-proj-7~5251 merge-11-1-b-proj-7~5260) 0 (ite (< merge-11-1-a-proj-0~5244 0) merge-11-1-a-proj-0~5244 (ite (< 0 merge-11-1-a-proj-0~5244) 0 (ite (<= merge-11-1-b-proj-8~5261 merge-11-1-a-proj-8~5252) merge-11-1-a-proj-0~5244 0)))))))
(assert (= merge-11-1-TupleFlattenVar~5263 (ite (< merge-11-1-b-proj-7~5260 merge-11-1-a-proj-7~5251) merge-11-1-a-proj-1~5245 (ite (< merge-11-1-a-proj-7~5251 merge-11-1-b-proj-7~5260) merge-11-1-b-proj-1~5254 (ite (< merge-11-1-a-proj-0~5244 0) merge-11-1-a-proj-1~5245 (ite (< 0 merge-11-1-a-proj-0~5244) merge-11-1-b-proj-1~5254 (ite (<= merge-11-1-b-proj-8~5261 merge-11-1-a-proj-8~5252) merge-11-1-a-proj-1~5245 merge-11-1-b-proj-1~5254)))))))
(assert (= merge-11-1-TupleFlattenVar~5264 false))
(assert (= merge-11-1-TupleFlattenVar~5265 false))
(assert (= merge-11-1-TupleFlattenVar~5266 false))
(assert (= merge-11-1-TupleFlattenVar~5267 false))
(assert (= merge-11-1-TupleFlattenVar~5268 false))
(assert (= merge-11-1-TupleFlattenVar~5269 (ite (< merge-11-1-b-proj-7~5260 merge-11-1-a-proj-7~5251) merge-11-1-a-proj-7~5251 (ite (< merge-11-1-a-proj-7~5251 merge-11-1-b-proj-7~5260) merge-11-1-b-proj-7~5260 (ite (< merge-11-1-a-proj-0~5244 0) merge-11-1-a-proj-7~5251 (ite (< 0 merge-11-1-a-proj-0~5244) merge-11-1-b-proj-7~5260 (ite (<= merge-11-1-b-proj-8~5261 merge-11-1-a-proj-8~5252) merge-11-1-a-proj-7~5251 merge-11-1-b-proj-7~5260)))))))
(assert (= merge-11-1-TupleFlattenVar~5270 (ite (< merge-11-1-b-proj-7~5260 merge-11-1-a-proj-7~5251) merge-11-1-a-proj-8~5252 (ite (< merge-11-1-a-proj-7~5251 merge-11-1-b-proj-7~5260) merge-11-1-b-proj-8~5261 (ite (< merge-11-1-a-proj-0~5244 0) merge-11-1-a-proj-8~5252 (ite (< 0 merge-11-1-a-proj-0~5244) merge-11-1-b-proj-8~5261 (ite (<= merge-11-1-b-proj-8~5261 merge-11-1-a-proj-8~5252) merge-11-1-a-proj-8~5252 merge-11-1-b-proj-8~5261)))))))
(assert (= assert-11-x-proj-0~5121 (ite (= trans-5-11-result-proj-0 false) init-11-result-proj-0 (ite (= init-11-result-proj-0 false) trans-5-11-result-proj-0 true))))
(assert (= merge-11-1-b-proj-0~5231 (ite (= trans-5-11-result-proj-0 false) 0 (ite (= init-11-result-proj-0 false) merge-11-1-a-proj-0~5244 merge-11-1-TupleFlattenVar~5262))))
(assert (= merge-11-1-b-proj-1~5232 (ite (= trans-5-11-result-proj-0 false) merge-11-1-b-proj-1~5254 (ite (= init-11-result-proj-0 false) merge-11-1-a-proj-1~5245 merge-11-1-TupleFlattenVar~5263))))
(assert (= merge-11-1-b-proj-2~5233 (ite (= trans-5-11-result-proj-0 false) false (ite (= init-11-result-proj-0 false) false merge-11-1-TupleFlattenVar~5264))))
(assert (= merge-11-1-b-proj-3~5234 (ite (= trans-5-11-result-proj-0 false) false (ite (= init-11-result-proj-0 false) false merge-11-1-TupleFlattenVar~5265))))
(assert (= merge-11-1-b-proj-4~5235 (ite (= trans-5-11-result-proj-0 false) false (ite (= init-11-result-proj-0 false) false merge-11-1-TupleFlattenVar~5266))))
(assert (= merge-11-1-b-proj-5~5236 (ite (= trans-5-11-result-proj-0 false) false (ite (= init-11-result-proj-0 false) false merge-11-1-TupleFlattenVar~5267))))
(assert (= merge-11-1-b-proj-6~5237 (ite (= trans-5-11-result-proj-0 false) false (ite (= init-11-result-proj-0 false) false merge-11-1-TupleFlattenVar~5268))))
(assert (= merge-11-1-b-proj-7~5238 (ite (= trans-5-11-result-proj-0 false) merge-11-1-b-proj-7~5260 (ite (= init-11-result-proj-0 false) merge-11-1-a-proj-7~5251 merge-11-1-TupleFlattenVar~5269))))
(assert (= merge-11-1-b-proj-8~5239 (ite (= trans-5-11-result-proj-0 false) merge-11-1-b-proj-8~5261 (ite (= init-11-result-proj-0 false) merge-11-1-a-proj-8~5252 merge-11-1-TupleFlattenVar~5270))))
(assert (= merge-11-1-o-proj-0~5215 (not (= assert-11-x-proj-12~5133 false))))
(assert (= merge-11-1-a~5227 (ite (= assert-11-x-proj-12~5133 false) 0 merge-11-1-o-proj-2~5242)))
(assert (= merge-11-1-b-proj-0~5217 (not (= assert-11-x-proj-0~5121 false))))
(assert (= merge-11-1-b~5228 (ite (= assert-11-x-proj-0~5121 false) 0 merge-11-1-b-proj-1~5232)))
(assert (= merge-11-1-x-proj-0~5219 (ite (ite (= assert-11-x-proj-19~5140 false) true (ite (= assert-11-x-proj-10~5131 false) false (<= merge-11-1-a~5229 merge-11-1-b~5230))) assert-11-x-proj-10~5131 assert-11-x-proj-19~5140)))
(assert (= merge-11-1-a~5225 (ite (ite (= assert-11-x-proj-19~5140 false) true (ite (= assert-11-x-proj-10~5131 false) false (<= merge-11-1-a~5229 merge-11-1-b~5230))) merge-11-1-a~5229 merge-11-1-b~5230)))
(assert (= merge-11-1-p1~5221 (ite (ite (= assert-11-x-proj-19~5140 false) true (ite (= assert-11-x-proj-10~5131 false) false (<= merge-11-1-a~5229 merge-11-1-b~5230))) 0 1)))
(assert (= merge-11-1-y-proj-0~5222 (ite (ite (= merge-11-1-b-proj-0~5217 false) true (ite (= merge-11-1-o-proj-0~5215 false) false (<= merge-11-1-a~5227 merge-11-1-b~5228))) merge-11-1-o-proj-0~5215 merge-11-1-b-proj-0~5217)))
(assert (= merge-11-1-b~5226 (ite (ite (= merge-11-1-b-proj-0~5217 false) true (ite (= merge-11-1-o-proj-0~5215 false) false (<= merge-11-1-a~5227 merge-11-1-b~5228))) merge-11-1-a~5227 merge-11-1-b~5228)))
(assert (= merge-11-1-p2~5224 (ite (ite (= merge-11-1-b-proj-0~5217 false) true (ite (= merge-11-1-o-proj-0~5215 false) false (<= merge-11-1-a~5227 merge-11-1-b~5228))) 2 3)))
(assert (= assert-11-x-proj-17~5138 (not (and (= assert-11-x-proj-0~5121 false) (and (= assert-11-x-proj-12~5133 false) (and (= assert-11-x-proj-19~5140 false) (= assert-11-x-proj-10~5131 false)))))))
(assert (= assert-11-x-proj-18~5139 (ite (and (= assert-11-x-proj-0~5121 false) (and (= assert-11-x-proj-12~5133 false) (and (= assert-11-x-proj-19~5140 false) (= assert-11-x-proj-10~5131 false)))) 0 (ite (ite (= merge-11-1-y-proj-0~5222 false) true (ite (= merge-11-1-x-proj-0~5219 false) false (<= merge-11-1-a~5225 merge-11-1-b~5226))) merge-11-1-p1~5221 merge-11-1-p2~5224))))
(assert (= assert-12-x-proj-10~5131 init-12-result-proj-5))
(assert (= merge-12-1-a~5229 0))
(assert (= assert-12-x-proj-19~5140 false))
(assert (= merge-12-1-b~5230 0))
(assert (= merge-12-1-TupleFlattenVar~5299 0))
(assert (= merge-12-1-TupleFlattenVar~5300 0))
(assert (= merge-12-1-TupleFlattenVar~5301 0))
(assert (= merge-12-1-TupleFlattenVar~5302 0))
(assert (= assert-12-x-proj-12~5133 false))
(assert (= merge-12-1-o-proj-0~5240 0))
(assert (= merge-12-1-o-proj-1~5241 0))
(assert (= merge-12-1-o-proj-2~5242 0))
(assert (= merge-12-1-o-proj-3~5243 0))
(assert (= merge-12-1-TupleFlattenVar~5262 (ite (< merge-12-1-b-proj-7~5260 merge-12-1-a-proj-7~5251) merge-12-1-a-proj-0~5244 (ite (< merge-12-1-a-proj-7~5251 merge-12-1-b-proj-7~5260) 0 (ite (< merge-12-1-a-proj-0~5244 0) merge-12-1-a-proj-0~5244 (ite (< 0 merge-12-1-a-proj-0~5244) 0 (ite (<= merge-12-1-b-proj-8~5261 merge-12-1-a-proj-8~5252) merge-12-1-a-proj-0~5244 0)))))))
(assert (= merge-12-1-TupleFlattenVar~5263 (ite (< merge-12-1-b-proj-7~5260 merge-12-1-a-proj-7~5251) merge-12-1-a-proj-1~5245 (ite (< merge-12-1-a-proj-7~5251 merge-12-1-b-proj-7~5260) merge-12-1-b-proj-1~5254 (ite (< merge-12-1-a-proj-0~5244 0) merge-12-1-a-proj-1~5245 (ite (< 0 merge-12-1-a-proj-0~5244) merge-12-1-b-proj-1~5254 (ite (<= merge-12-1-b-proj-8~5261 merge-12-1-a-proj-8~5252) merge-12-1-a-proj-1~5245 merge-12-1-b-proj-1~5254)))))))
(assert (= merge-12-1-TupleFlattenVar~5264 false))
(assert (= merge-12-1-TupleFlattenVar~5265 false))
(assert (= merge-12-1-TupleFlattenVar~5266 false))
(assert (= merge-12-1-TupleFlattenVar~5267 false))
(assert (= merge-12-1-TupleFlattenVar~5268 false))
(assert (= merge-12-1-TupleFlattenVar~5269 (ite (< merge-12-1-b-proj-7~5260 merge-12-1-a-proj-7~5251) merge-12-1-a-proj-7~5251 (ite (< merge-12-1-a-proj-7~5251 merge-12-1-b-proj-7~5260) merge-12-1-b-proj-7~5260 (ite (< merge-12-1-a-proj-0~5244 0) merge-12-1-a-proj-7~5251 (ite (< 0 merge-12-1-a-proj-0~5244) merge-12-1-b-proj-7~5260 (ite (<= merge-12-1-b-proj-8~5261 merge-12-1-a-proj-8~5252) merge-12-1-a-proj-7~5251 merge-12-1-b-proj-7~5260)))))))
(assert (= merge-12-1-TupleFlattenVar~5270 (ite (< merge-12-1-b-proj-7~5260 merge-12-1-a-proj-7~5251) merge-12-1-a-proj-8~5252 (ite (< merge-12-1-a-proj-7~5251 merge-12-1-b-proj-7~5260) merge-12-1-b-proj-8~5261 (ite (< merge-12-1-a-proj-0~5244 0) merge-12-1-a-proj-8~5252 (ite (< 0 merge-12-1-a-proj-0~5244) merge-12-1-b-proj-8~5261 (ite (<= merge-12-1-b-proj-8~5261 merge-12-1-a-proj-8~5252) merge-12-1-a-proj-8~5252 merge-12-1-b-proj-8~5261)))))))
(assert (= assert-12-x-proj-0~5121 (ite (= trans-16-12-result-proj-0 false) init-12-result-proj-0 (ite (= init-12-result-proj-0 false) trans-16-12-result-proj-0 true))))
(assert (= merge-12-1-b-proj-0~5231 (ite (= trans-16-12-result-proj-0 false) 0 (ite (= init-12-result-proj-0 false) merge-12-1-a-proj-0~5244 merge-12-1-TupleFlattenVar~5262))))
(assert (= merge-12-1-b-proj-1~5232 (ite (= trans-16-12-result-proj-0 false) merge-12-1-b-proj-1~5254 (ite (= init-12-result-proj-0 false) merge-12-1-a-proj-1~5245 merge-12-1-TupleFlattenVar~5263))))
(assert (= merge-12-1-b-proj-2~5233 (ite (= trans-16-12-result-proj-0 false) false (ite (= init-12-result-proj-0 false) false merge-12-1-TupleFlattenVar~5264))))
(assert (= merge-12-1-b-proj-3~5234 (ite (= trans-16-12-result-proj-0 false) false (ite (= init-12-result-proj-0 false) false merge-12-1-TupleFlattenVar~5265))))
(assert (= merge-12-1-b-proj-4~5235 (ite (= trans-16-12-result-proj-0 false) false (ite (= init-12-result-proj-0 false) false merge-12-1-TupleFlattenVar~5266))))
(assert (= merge-12-1-b-proj-5~5236 (ite (= trans-16-12-result-proj-0 false) false (ite (= init-12-result-proj-0 false) false merge-12-1-TupleFlattenVar~5267))))
(assert (= merge-12-1-b-proj-6~5237 (ite (= trans-16-12-result-proj-0 false) false (ite (= init-12-result-proj-0 false) false merge-12-1-TupleFlattenVar~5268))))
(assert (= merge-12-1-b-proj-7~5238 (ite (= trans-16-12-result-proj-0 false) merge-12-1-b-proj-7~5260 (ite (= init-12-result-proj-0 false) merge-12-1-a-proj-7~5251 merge-12-1-TupleFlattenVar~5269))))
(assert (= merge-12-1-b-proj-8~5239 (ite (= trans-16-12-result-proj-0 false) merge-12-1-b-proj-8~5261 (ite (= init-12-result-proj-0 false) merge-12-1-a-proj-8~5252 merge-12-1-TupleFlattenVar~5270))))
(assert (= merge-12-1-o-proj-0~5215 (not (= assert-12-x-proj-12~5133 false))))
(assert (= merge-12-1-a~5227 (ite (= assert-12-x-proj-12~5133 false) 0 merge-12-1-o-proj-2~5242)))
(assert (= merge-12-1-b-proj-0~5217 (not (= assert-12-x-proj-0~5121 false))))
(assert (= merge-12-1-b~5228 (ite (= assert-12-x-proj-0~5121 false) 0 merge-12-1-b-proj-1~5232)))
(assert (= merge-12-1-x-proj-0~5219 (ite (ite (= assert-12-x-proj-19~5140 false) true (ite (= assert-12-x-proj-10~5131 false) false (<= merge-12-1-a~5229 merge-12-1-b~5230))) assert-12-x-proj-10~5131 assert-12-x-proj-19~5140)))
(assert (= merge-12-1-a~5225 (ite (ite (= assert-12-x-proj-19~5140 false) true (ite (= assert-12-x-proj-10~5131 false) false (<= merge-12-1-a~5229 merge-12-1-b~5230))) merge-12-1-a~5229 merge-12-1-b~5230)))
(assert (= merge-12-1-p1~5221 (ite (ite (= assert-12-x-proj-19~5140 false) true (ite (= assert-12-x-proj-10~5131 false) false (<= merge-12-1-a~5229 merge-12-1-b~5230))) 0 1)))
(assert (= merge-12-1-y-proj-0~5222 (ite (ite (= merge-12-1-b-proj-0~5217 false) true (ite (= merge-12-1-o-proj-0~5215 false) false (<= merge-12-1-a~5227 merge-12-1-b~5228))) merge-12-1-o-proj-0~5215 merge-12-1-b-proj-0~5217)))
(assert (= merge-12-1-b~5226 (ite (ite (= merge-12-1-b-proj-0~5217 false) true (ite (= merge-12-1-o-proj-0~5215 false) false (<= merge-12-1-a~5227 merge-12-1-b~5228))) merge-12-1-a~5227 merge-12-1-b~5228)))
(assert (= merge-12-1-p2~5224 (ite (ite (= merge-12-1-b-proj-0~5217 false) true (ite (= merge-12-1-o-proj-0~5215 false) false (<= merge-12-1-a~5227 merge-12-1-b~5228))) 2 3)))
(assert (= assert-12-x-proj-17~5138 (not (and (= assert-12-x-proj-0~5121 false) (and (= assert-12-x-proj-12~5133 false) (and (= assert-12-x-proj-19~5140 false) (= assert-12-x-proj-10~5131 false)))))))
(assert (= assert-12-x-proj-18~5139 (ite (and (= assert-12-x-proj-0~5121 false) (and (= assert-12-x-proj-12~5133 false) (and (= assert-12-x-proj-19~5140 false) (= assert-12-x-proj-10~5131 false)))) 0 (ite (ite (= merge-12-1-y-proj-0~5222 false) true (ite (= merge-12-1-x-proj-0~5219 false) false (<= merge-12-1-a~5225 merge-12-1-b~5226))) merge-12-1-p1~5221 merge-12-1-p2~5224))))
(assert (= assert-15-x-proj-10~5131 init-15-result-proj-5))
(assert (= merge-15-1-a~5229 0))
(assert (= assert-15-x-proj-19~5140 false))
(assert (= merge-15-1-b~5230 0))
(assert (= merge-15-1-TupleFlattenVar~5299 0))
(assert (= merge-15-1-TupleFlattenVar~5300 0))
(assert (= merge-15-1-TupleFlattenVar~5301 0))
(assert (= merge-15-1-TupleFlattenVar~5302 0))
(assert (= assert-15-x-proj-12~5133 false))
(assert (= merge-15-1-o-proj-0~5240 0))
(assert (= merge-15-1-o-proj-1~5241 0))
(assert (= merge-15-1-o-proj-2~5242 0))
(assert (= merge-15-1-o-proj-3~5243 0))
(assert (= merge-15-1-TupleFlattenVar~5262 (ite (< merge-15-1-b-proj-7~5260 merge-15-1-a-proj-7~5251) merge-15-1-a-proj-0~5244 (ite (< merge-15-1-a-proj-7~5251 merge-15-1-b-proj-7~5260) 0 (ite (< merge-15-1-a-proj-0~5244 0) merge-15-1-a-proj-0~5244 (ite (< 0 merge-15-1-a-proj-0~5244) 0 (ite (<= merge-15-1-b-proj-8~5261 merge-15-1-a-proj-8~5252) merge-15-1-a-proj-0~5244 0)))))))
(assert (= merge-15-1-TupleFlattenVar~5263 (ite (< merge-15-1-b-proj-7~5260 merge-15-1-a-proj-7~5251) merge-15-1-a-proj-1~5245 (ite (< merge-15-1-a-proj-7~5251 merge-15-1-b-proj-7~5260) merge-15-1-b-proj-1~5254 (ite (< merge-15-1-a-proj-0~5244 0) merge-15-1-a-proj-1~5245 (ite (< 0 merge-15-1-a-proj-0~5244) merge-15-1-b-proj-1~5254 (ite (<= merge-15-1-b-proj-8~5261 merge-15-1-a-proj-8~5252) merge-15-1-a-proj-1~5245 merge-15-1-b-proj-1~5254)))))))
(assert (= merge-15-1-TupleFlattenVar~5264 false))
(assert (= merge-15-1-TupleFlattenVar~5265 false))
(assert (= merge-15-1-TupleFlattenVar~5266 false))
(assert (= merge-15-1-TupleFlattenVar~5267 false))
(assert (= merge-15-1-TupleFlattenVar~5268 false))
(assert (= merge-15-1-TupleFlattenVar~5269 (ite (< merge-15-1-b-proj-7~5260 merge-15-1-a-proj-7~5251) merge-15-1-a-proj-7~5251 (ite (< merge-15-1-a-proj-7~5251 merge-15-1-b-proj-7~5260) merge-15-1-b-proj-7~5260 (ite (< merge-15-1-a-proj-0~5244 0) merge-15-1-a-proj-7~5251 (ite (< 0 merge-15-1-a-proj-0~5244) merge-15-1-b-proj-7~5260 (ite (<= merge-15-1-b-proj-8~5261 merge-15-1-a-proj-8~5252) merge-15-1-a-proj-7~5251 merge-15-1-b-proj-7~5260)))))))
(assert (= merge-15-1-TupleFlattenVar~5270 (ite (< merge-15-1-b-proj-7~5260 merge-15-1-a-proj-7~5251) merge-15-1-a-proj-8~5252 (ite (< merge-15-1-a-proj-7~5251 merge-15-1-b-proj-7~5260) merge-15-1-b-proj-8~5261 (ite (< merge-15-1-a-proj-0~5244 0) merge-15-1-a-proj-8~5252 (ite (< 0 merge-15-1-a-proj-0~5244) merge-15-1-b-proj-8~5261 (ite (<= merge-15-1-b-proj-8~5261 merge-15-1-a-proj-8~5252) merge-15-1-a-proj-8~5252 merge-15-1-b-proj-8~5261)))))))
(assert (= assert-15-x-proj-0~5121 (ite (= trans-14-15-result-proj-0 false) init-15-result-proj-0 (ite (= init-15-result-proj-0 false) trans-14-15-result-proj-0 true))))
(assert (= merge-15-1-b-proj-0~5231 (ite (= trans-14-15-result-proj-0 false) 0 (ite (= init-15-result-proj-0 false) merge-15-1-a-proj-0~5244 merge-15-1-TupleFlattenVar~5262))))
(assert (= merge-15-1-b-proj-1~5232 (ite (= trans-14-15-result-proj-0 false) merge-15-1-b-proj-1~5254 (ite (= init-15-result-proj-0 false) merge-15-1-a-proj-1~5245 merge-15-1-TupleFlattenVar~5263))))
(assert (= merge-15-1-b-proj-2~5233 (ite (= trans-14-15-result-proj-0 false) false (ite (= init-15-result-proj-0 false) false merge-15-1-TupleFlattenVar~5264))))
(assert (= merge-15-1-b-proj-3~5234 (ite (= trans-14-15-result-proj-0 false) false (ite (= init-15-result-proj-0 false) false merge-15-1-TupleFlattenVar~5265))))
(assert (= merge-15-1-b-proj-4~5235 (ite (= trans-14-15-result-proj-0 false) false (ite (= init-15-result-proj-0 false) false merge-15-1-TupleFlattenVar~5266))))
(assert (= merge-15-1-b-proj-5~5236 (ite (= trans-14-15-result-proj-0 false) false (ite (= init-15-result-proj-0 false) false merge-15-1-TupleFlattenVar~5267))))
(assert (= merge-15-1-b-proj-6~5237 (ite (= trans-14-15-result-proj-0 false) false (ite (= init-15-result-proj-0 false) false merge-15-1-TupleFlattenVar~5268))))
(assert (= merge-15-1-b-proj-7~5238 (ite (= trans-14-15-result-proj-0 false) merge-15-1-b-proj-7~5260 (ite (= init-15-result-proj-0 false) merge-15-1-a-proj-7~5251 merge-15-1-TupleFlattenVar~5269))))
(assert (= merge-15-1-b-proj-8~5239 (ite (= trans-14-15-result-proj-0 false) merge-15-1-b-proj-8~5261 (ite (= init-15-result-proj-0 false) merge-15-1-a-proj-8~5252 merge-15-1-TupleFlattenVar~5270))))
(assert (= merge-15-1-o-proj-0~5215 (not (= assert-15-x-proj-12~5133 false))))
(assert (= merge-15-1-a~5227 (ite (= assert-15-x-proj-12~5133 false) 0 merge-15-1-o-proj-2~5242)))
(assert (= merge-15-1-b-proj-0~5217 (not (= assert-15-x-proj-0~5121 false))))
(assert (= merge-15-1-b~5228 (ite (= assert-15-x-proj-0~5121 false) 0 merge-15-1-b-proj-1~5232)))
(assert (= merge-15-1-x-proj-0~5219 (ite (ite (= assert-15-x-proj-19~5140 false) true (ite (= assert-15-x-proj-10~5131 false) false (<= merge-15-1-a~5229 merge-15-1-b~5230))) assert-15-x-proj-10~5131 assert-15-x-proj-19~5140)))
(assert (= merge-15-1-a~5225 (ite (ite (= assert-15-x-proj-19~5140 false) true (ite (= assert-15-x-proj-10~5131 false) false (<= merge-15-1-a~5229 merge-15-1-b~5230))) merge-15-1-a~5229 merge-15-1-b~5230)))
(assert (= merge-15-1-p1~5221 (ite (ite (= assert-15-x-proj-19~5140 false) true (ite (= assert-15-x-proj-10~5131 false) false (<= merge-15-1-a~5229 merge-15-1-b~5230))) 0 1)))
(assert (= merge-15-1-y-proj-0~5222 (ite (ite (= merge-15-1-b-proj-0~5217 false) true (ite (= merge-15-1-o-proj-0~5215 false) false (<= merge-15-1-a~5227 merge-15-1-b~5228))) merge-15-1-o-proj-0~5215 merge-15-1-b-proj-0~5217)))
(assert (= merge-15-1-b~5226 (ite (ite (= merge-15-1-b-proj-0~5217 false) true (ite (= merge-15-1-o-proj-0~5215 false) false (<= merge-15-1-a~5227 merge-15-1-b~5228))) merge-15-1-a~5227 merge-15-1-b~5228)))
(assert (= merge-15-1-p2~5224 (ite (ite (= merge-15-1-b-proj-0~5217 false) true (ite (= merge-15-1-o-proj-0~5215 false) false (<= merge-15-1-a~5227 merge-15-1-b~5228))) 2 3)))
(assert (= assert-15-x-proj-17~5138 (not (and (= assert-15-x-proj-0~5121 false) (and (= assert-15-x-proj-12~5133 false) (and (= assert-15-x-proj-19~5140 false) (= assert-15-x-proj-10~5131 false)))))))
(assert (= assert-15-x-proj-18~5139 (ite (and (= assert-15-x-proj-0~5121 false) (and (= assert-15-x-proj-12~5133 false) (and (= assert-15-x-proj-19~5140 false) (= assert-15-x-proj-10~5131 false)))) 0 (ite (ite (= merge-15-1-y-proj-0~5222 false) true (ite (= merge-15-1-x-proj-0~5219 false) false (<= merge-15-1-a~5225 merge-15-1-b~5226))) merge-15-1-p1~5221 merge-15-1-p2~5224))))
(assert (= assert-0-result true))
(assert (= assert-1-result (ite (and (= symbolic-d-proj-1~5118 24) (= symbolic-d-proj-0~5119 3355592960)) (ite (and (= assert-1-x-proj-18~5139 3) (= assert-1-x-proj-17~5138 true)) (ite (= assert-1-x-proj-0~5121 false) false (< merge-1-1-b-proj-0~5231 20)) true) true)))
(assert (= assert-2-result (ite (and (= symbolic-d-proj-1~5118 24) (= symbolic-d-proj-0~5119 3355592960)) (ite (and (= assert-2-x-proj-18~5139 3) (= assert-2-x-proj-17~5138 true)) (ite (= assert-2-x-proj-0~5121 false) false (< merge-2-1-b-proj-0~5231 20)) true) true)))
(assert (= assert-3-result (ite (and (= symbolic-d-proj-1~5118 24) (= symbolic-d-proj-0~5119 3355592960)) (ite (and (= assert-3-x-proj-18~5139 3) (= assert-3-x-proj-17~5138 true)) (ite (= assert-3-x-proj-0~5121 false) false (< merge-3-1-b-proj-0~5231 20)) true) true)))
(assert (= assert-4-result (ite (and (= symbolic-d-proj-1~5118 24) (= symbolic-d-proj-0~5119 3355592960)) (ite (and (= trans-4-8-y~5639 3) (= assert-4-x-proj-17~5138 true)) (ite (= assert-4-x-proj-0~5121 false) false (< merge-4-2-b-proj-0~5231 20)) true) true)))
(assert (= assert-5-result true))
(assert (= assert-6-result true))
(assert (= assert-7-result true))
(assert (= assert-8-result (ite (and (= symbolic-d-proj-1~5118 24) (= symbolic-d-proj-0~5119 3355592960)) (ite (and (= trans-8-4-y~5819 3) (= assert-8-x-proj-17~5138 true)) (ite (= assert-8-x-proj-0~5121 false) false (< merge-8-1-b-proj-0~5231 20)) true) true)))
(assert (= assert-9-result (ite (and (= symbolic-d-proj-1~5118 24) (= symbolic-d-proj-0~5119 3355592960)) (ite (and (= assert-9-x-proj-18~5139 3) (= assert-9-x-proj-17~5138 true)) (ite (= assert-9-x-proj-0~5121 false) false (< merge-9-1-b-proj-0~5231 20)) true) true)))
(assert (= assert-10-result true))
(assert (= assert-11-result (ite (and (= symbolic-d-proj-1~5118 24) (= symbolic-d-proj-0~5119 3355592960)) (ite (and (= assert-11-x-proj-18~5139 3) (= assert-11-x-proj-17~5138 true)) (ite (= assert-11-x-proj-0~5121 false) false (< merge-11-1-b-proj-0~5231 20)) true) true)))
(assert (= assert-12-result (ite (and (= symbolic-d-proj-1~5118 24) (= symbolic-d-proj-0~5119 3355592960)) (ite (and (= assert-12-x-proj-18~5139 3) (= assert-12-x-proj-17~5138 true)) (ite (= assert-12-x-proj-0~5121 false) false (< merge-12-1-b-proj-0~5231 20)) true) true)))
(assert (= assert-13-result true))
(assert (= assert-14-result true))
(assert (= assert-15-result (ite (and (= symbolic-d-proj-1~5118 24) (= symbolic-d-proj-0~5119 3355592960)) (ite (and (= assert-15-x-proj-18~5139 3) (= assert-15-x-proj-17~5138 true)) (ite (= assert-15-x-proj-0~5121 false) false (< merge-15-1-b-proj-0~5231 20)) true) true)))
(assert (= assert-16-result true))
(assert (not (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (= assert-0-result true) (= assert-1-result true)) (= assert-2-result true)) (= assert-3-result true)) (= assert-4-result true)) (= assert-5-result true)) (= assert-6-result true)) (= assert-7-result true)) (= assert-8-result true)) (= assert-9-result true)) (= assert-10-result true)) (= assert-11-result true)) (= assert-12-result true)) (= assert-13-result true)) (= assert-14-result true)) (= assert-15-result true)) (= assert-16-result true))))

(check-sat-using (then simplify propagate-values simplify solve-eqs smt))