day1-part2.smt

(set-logic QF_ALIA)

(declare-const len Int)
(assert (= len 247))

(declare-const a (Array Int Int))
(define-fun x () (Array Int Int)
  (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store a
  0 (+ 9057 8878 2753 7027 3880 7154 8022 6710 5721))
  1 (+ 4863 3690 3333 1831 5293 6258 1212 4255 2331 3785 1505 3355 3353 4416))
  2 (+ 5918 3076 2145 2712 6087 4310 1084 5807 1342 2770 5095 4696 5842 4555 5388))
  3 (+ 20770))
  4 (+ 3968 15647 3933 15427 16179))
  5 (+ 40721))
  6 (+ 5837 4419 2159 5173 5215 1991 4842 5642 5435 2853 1055 1667 4361 2316 1974))
  7 (+ 24315 6376 6153))
  8 (+ 3142 4989 8864 3819 9260 1273 2773))
  9 (+ 9320 4936 3707 2103 8804 10586 2018 3779))
  10 (+ 4129 1019 5054 9429 10526 6314))
  11 (+ 13364 14437 14046 7931 11712))
  12 (+ 2615 9583 7471 3552 7532 5797 1528 6479 2595))
  13 (+ 8758 1774 3734 5159 7046 2195 9245))
  14 (+ 12116 3801 10950 1935 11450 1091 5891))
  15 (+ 7792 4901 9062 8640 6065 6405 3606 2487 6606))
  16 (+ 5460 3272 1310 1439 3753 3947 4472 4155 2056 2435 2235 3662 2933 1110 1024))
  17 (+ 1590 6814 12646 1548 13624 5239))
  18 (+ 3955 2469 3104 1548 4551 2307 4450 4491 2233 4706 5950 3395 6592))
  19 (+ 17731 18903))
  20 (+ 6164 7718 7297 3277 3592 3462 7405 6164 2559 5171 3337))
  21 (+ 4797 9455 13275 5801 12597 2687))
  22 (+ 3091 1153 1733 5022 4441 3163 2375 6388 6061 1444 3255 5828 4414 6171))
  23 (+ 2841 17670 14820))
  24 (+ 2600 2598 14037 10164))
  25 (+ 10425 4618 7656 6910 8761 11429 11611))
  26 (+ 2787 4826 1527 5024 4252 1393 6744 5665 4601 4129))
  27 (+ 6876 8156 7854 6190 5234 8616 1414 1076 5161))
  28 (+ 6343 7372 7806 2309 7352 7249 4239 5572 7220 3920 6979))
  29 (+ 11380 9322 10505 1250 1122 1996 5199))
  30 (+ 7569 12600 14729 2514 6841))
  31 (+ 9414 9386 10521 4974 11016 11238 1334))
  32 (+ 21696 27477))
  33 (+ 11623 11309 7708 6139 2284 2789 4566))
  34 (+ 16850 5171 7647 5516))
  35 (+ 24499))
  36 (+ 4040 7221 3197 7251 8117 2221 1881 5914 8381))
  37 (+ 3786 2055 5301 4144 2543 1406 5609 5064 2447 4892 2306 1654 1650 3528))
  38 (+ 4187 2576 11910 8331 11613 9093 2752))
  39 (+ 4166 6057 4585 1942 5747 3102 2501 4831 5681 6596 4455 1125 4887))
  40 (+ 2083 10447 16506))
  41 (+ 4971 3313 1821 1493 5920 3617 4857 3995 5608 3679 1463 3539 2600 3574 2636))
  42 (+ 2804 17188 6966 15585))
  43 (+ 13184 15490 9948 14350 12788))
  44 (+ 31669))
  45 (+ 3318 2544 7560 2170 9138 2905 7010))
  46 (+ 3933 4835 4704 2140 1896 4951 3870 4241 2819 1065 3605 5667 2361 2642 1926))
  47 (+ 6614 3288 3982 7283 7086 2308 3237 7365 6767 6931 5417 5180))
  48 (+ 40453))
  49 (+ 4946 4257 2590 5342 3880 6297 1472 2441 4054 3490 5054))
  50 (+ 26102 29920))
  51 (+ 3726))
  52 (+ 18600 1537 7197 3487))
  53 (+ 8193 8147 5901 1975 3872 8834 1623 6604))
  54 (+ 4501 3385 5321 6771 2517 3943 2744 1330 2277 2344 6399 2090 3571))
  55 (+ 8236 6575 6362 3878 7021 8613 3520 3424 2606 5607))
  56 (+ 10326 9793 3341 7238 3008 8188 11807))
  57 (+ 3755 16826 7885 11677))
  58 (+ 5980 6793 2393 5757 2525 6496 6420 6902 6755 1023 4226 1451 5006))
  59 (+ 6122 3263 4273 2775 2251 1076 2995 5662 4189 2687 5552 6586 2418))
  60 (+ 9994 10470 7802 9572 9292 8390 8803 4013))
  61 (+ 28290))
  62 (+ 3210 9126 1346 7538 11536 10544 7409))
  63 (+ 20799 16110))
  64 (+ 3374 3818 1924 1637 3258 5224 4741 2689 1455 5948 4813 3549 2772 2562 4358))
  65 (+ 6843 10575 7103 9314 9901 3356 9120 4552))
  66 (+ 7709 3977 6868 4640 4665 7109 2662 5682 5388 4256 7249))
  67 (+ 69796))
  68 (+ 8596 1275 2723 2202 5544 3687 4055 3062 4137 4407))
  69 (+ 4870 2559 2177 5239 1059 4440 2536 1728 1520 2572 2977 6815 4679))
  70 (+ 9042 8883 2705 16255 7889))
  71 (+ 2318 4232 1042 3075 6202 7568 2519 5918 1812 3750 3845))
  72 (+ 13323 33324))
  73 (+ 13742 1087 17146 14863))
  74 (+ 2686 4132 5052 4751 4695 4528 4801 5741 6027 1754 5633 2427 4679 5777 3143))
  75 (+ 1533 4361 2196 10184 3981 6223 9273))
  76 (+ 1296 11261 5647 8657 7235 1788))
  77 (+ 3467 5537 10807 4793 3452 12209))
  78 (+ 5745 5137 4002 4824 2655 7597 5748 5931 5264 4469 8009))
  79 (+ 4436 4866 3784 5181 6240 6027 3343 5780 2258 6389 3827 6496 6378 4831))
  80 (+ 5894 7587 6913 10950 6733 5617 8084))
  81 (+ 2446 5375 4555 5327 1233 2773 2701 5454 3377 1217 5889 6168 1056))
  82 (+ 3468 2402 7848 5652 1448 1954 1021 7860 4305))
  83 (+ 2234 17391 5472))
  84 (+ 2028 5812 3091 5508 5531 3554 3706 2667 5670 4845 2749 5569 4811 3090 1063))
  85 (+ 2144 5088))
  86 (+ 20000 9957 9049 3092))
  87 (+ 12235 6601 3496 16002 1378))
  88 (+ 8800 1236 5552 5693 8482 3003 1126 4612 5833 8430))
  89 (+ 6223 4640 1392 2667 1602 2308 4433 4148 6467 1817 2926 3884 6015))
  90 (+ 2273 3007 4509 2902 4170 2731 4409 4873 4237 2667 4243 5788 3673 4582 4696))
  91 (+ 27388 26736))
  92 (+ 44158))
  93 (+ 4877 2172 5968 1222 6456 6920 3593 3631 7213 3968 2398 7264))
  94 (+ 7126 30978))
  95 (+ 4024 2766 2721 2774 2807 1584 2429 3517 5260 4234 2381 5066 4204 4737 4031))
  96 (+ 1528 2205 4533 5873 1587 2708 4198 5560 3413 4058 1799 1088 4285 6233))
  97 (+ 44226))
  98 (+ 12933 6090 14830))
  99 (+ 5766 2184 2552 4757 1895 2328 1265 5829 2645 6110 6499 5920 6421 2505))
  100 (+ 5039 6271 5081 10068 3856 7103))
  101 (+ 5441 2606 1249 2526 1241 1914 3734 4464 3855 4761 5528 1419 2772 1825))
  102 (+ 3554))
  103 (+ 8766 2123 7372 7752 6260 5632 3802 9546 7769))
  104 (+ 9108 4838))
  105 (+ 1374 3720 7558 4646 6793 4704 3361 8038 6147 2160 1983))
  106 (+ 3133 3621 6073 2533 1644 5277 4276 1921 6251 5273 1571 3769 2155))
  107 (+ 2721 3793 4935 2950 2399 1083 4213 4958 1139 1140 2454 3291 3865 1667 4798))
  108 (+ 5676 5904 1356 1439 3241 2933 4164 3887 4712 2759 4390 1274 6220 2557))
  109 (+ 2049 4787 1819 3172 5511 1006 1373 6094 3054 4914 6057 4883 2867 5363 3916))
  110 (+ 11348 3724 6793 7336 4032 11297))
  111 (+ 4231 4277 2982 2408 5673 6805 4710 7659 6866))
  112 (+ 2950 4018 6167 8316 7308 4955 8341 1512 3167 8493))
  113 (+ 15665 14654 1249 15313 4636))
  114 (+ 1494 3325 5902 1393 6813 3900 2827 5936 6589 6847 4658))
  115 (+ 11492 14548 5203 15187 5937))
  116 (+ 1358 2801 1086 5190 4022 5013 3511 4398 1774 2194 1887 5704 2012 1259))
  117 (+ 4763 2250 6915 4281 1246 7242 6049 5113 1187 2486 6688 3275))
  118 (+ 22345 1336 11325))
  119 (+ 6000 3641 1082 2924 5477 3336 4126 3981 5359 1053 4299 5952 4655))
  120 (+ 46233))
  121 (+ 17242 6366 7866))
  122 (+ 12504 4031 12664 9756 12750))
  123 (+ 3373))
  124 (+ 3091 11142 15034 1144 11747))
  125 (+ 3129 2007 8482 7205 7734 8770 2213 5582 5437 3223))
  126 (+ 4471 2591 3286 4446 5388 3600 3357 2644 5028 5569 5055 3284 5597 4116 1076))
  127 (+ 3792 2354 8030 3269 2483 1302 7427 6148 3836 7834 1663))
  128 (+ 2930 5964 1707 2899 4160 2193 2705 5799 4612 2741 2333 4969 3117 5276 1747))
  129 (+ 62287))
  130 (+ 4321 22825 5690))
  131 (+ 7287 1774 4464 2273 2903 8920 4092 8072 8763))
  132 (+ 8885 7470 3145 3523 5647 1067 3048))
  133 (+ 6923 6463 4032 5923 1982 4331 6323 1192 5583 5470 6476 5889 2991))
  134 (+ 6697 1560 5520 4516 4845 3035 6047 4906 4596 1934 7245 4476))
  135 (+ 4001 7227 5720 3195 8505 6612 4012 4050 8659 3804))
  136 (+ 8332 3362 4926 4307 4779 1856 7350 4068 8592 2415))
  137 (+ 60630))
  138 (+ 4263 1716 8004 5253 2004 5381 5614 3020 5985 5587 3563))
  139 (+ 18645 10906 3077 2255))
  140 (+ 59591))
  141 (+ 3203 7739 2234 1421 3353 5031 6395 5614))
  142 (+ 6259 8748 4341 7788 1074 8497 3996 1294 5197 5779))
  143 (+ 10765 5009 3541 2298 10698 13317))
  144 (+ 6181 1305 6527 2125 9085 2889 8794 3265 4166))
  145 (+ 3607 1912 1927 6455 1043 6949 2542 1552 3064 2009 6587))
  146 (+ 5574 4632 5869 4312 1703 6124 6479 4556 5917 5890 4949 5614 5576))
  147 (+ 2267 7221 5412 5721 2931 3149 6934 3520 6237 4317 1295 6450))
  148 (+ 12143 7105 2050 9391 3017 10750))
  149 (+ 4649 2052 1856 3055 2132 6630 5964 5505 3395 2080))
  150 (+ 4388 6963 2613 1055 6588 1348 3752 5538 4524 7994 3977))
  151 (+ 5444 6078 8572 10427 5423 3812 1984))
  152 (+ 9248 17691 12948 17445))
  153 (+ 5807 3737 5304 1495 5162 1178 6053 5597 5645 2267 4333 3455 4086 2024 4127))
  154 (+ 5502 3665 3494 1502 4702 4563 5216 6486 1931 6493 4618 3960 1149 5109))
  155 (+ 2198 1411 4511 1913 4173 4446 6176 2305 4748 4560 4048 5361 4481))
  156 (+ 30924))
  157 (+ 15726 4014 20018 2880))
  158 (+ 3345 2576 4787 2186 2156 2989 4400 5147 5393 2830 5869 4839 2860 2134))
  159 (+ 2400 2009 2634 4431 7342 5534 2072 5520 5518 2998 3686 4906))
  160 (+ 10948 12532 11104 7815))
  161 (+ 5883 6111 4117 3590 3295 3984 2950 6814 1123 4642 1770 2029 4406))
  162 (+ 19302 1549 10378 13976))
  163 (+ 4852 7261 4206 12867 8400 11611))
  164 (+ 2587 3559 1415 5308 3732 6752 3804 1720 2570 5106 6658 5105 6156))
  165 (+ 7380 10456 8378 10778 9788 1299 10299))
  166 (+ 3596 5969 8288 3025 8196 6410 5966 3060 3015 1270))
  167 (+ 14103 5510 13362 19169))
  168 (+ 3056 3546 7784 2262 3791 3159 5386 6489 3421 7995 4498))
  169 (+ 27239))
  170 (+ 9345 8921 5252 1154 3189 1175 3216 3282 9392))
  171 (+ 2821 7731 8002 1351 5951 4544 3688 4855 8082 1428 5613))
  172 (+ 6506 2529 6614 3938 4404 5581 1984 6242 7589))
  173 (+ 8393 6631 5200 9914 10229 2405 3933 9333))
  174 (+ 6766 3486 11457 3098))
  175 (+ 5091 4105 1368 4682 3094 4077 5876 1958 1641 3925 2969 3780 5489))
  176 (+ 10434 2285 2830 6976 3561 6756))
  177 (+ 3944 2998 1874 4642 4634 2155 2221 2270 2446 1514 5382 4333 5441 2412 1789))
  178 (+ 2433 4036 6005 1551 7281 8466 2141 4190))
  179 (+ 5103 6956 5839 2237 7177 6397 11533))
  180 (+ 7100 3476 4592 6502 3322 10524 2973 10712))
  181 (+ 3440 1323 1316 1979 1168 6432 3512 5739 2131 4504 5233 3726 6371 6125))
  182 (+ 1917 3442 4104 6123 1657 3139 1690 3323 1269 1407 5603 4819 1787 2340))
  183 (+ 11143 9483 9438 12565 7187 13478))
  184 (+ 6406 2289 8029 1790 5009 6300 2521))
  185 (+ 8040 6772 3244 5246 6455 6715 4024 3855 6458 4945 4207))
  186 (+ 4628 4872 3344 5675 3761 4467 5113 5746 4140))
  187 (+ 9532 1992 5741 8559 4606 6310 5183))
  188 (+ 7530 13402 8481 8327))
  189 (+ 17909 7813 12567 9674))
  190 (+ 3329 6032 5539 5513 2555 4767 1085 3329 5138 4448 4082 5569 2732 3326))
  191 (+ 2019 3327 3701 3145 1943 1467 1913 5141 7475 7026 4964 2353))
  192 (+ 3375 1186 2890 1248 5696 5993 3804 1133 2035 5068 4280 2123 1890))
  193 (+ 8675 10684 22636))
  194 (+ 2704 1093 9357 7940 4843 1118 5533 8943 6492))
  195 (+ 67791))
  196 (+ 7101 3406 8840 3652 9258 5329 4562 5314 9146))
  197 (+ 3673 13526 2792 5659 13396 8400))
  198 (+ 2492 5265 5244 2173 5032 1182 1486 4561 4673 2480 5148 1375 1093))
  199 (+ 1368 5899 6527 7584 2148 2960 7701 5381 6149 2589 7496))
  200 (+ 12206 11842 11444 12447))
  201 (+ 3417 5044 7116 5491 9020 8610 1047 5725 2712))
  202 (+ 9153 1836 3337 1686 6044 8786 7476 1688))
  203 (+ 17559 10138 16446))
  204 (+ 15625 16403 16979 7402))
  205 (+ 3561 2910 12805 8128 13171 5786))
  206 (+ 1332))
  207 (+ 1135 5954 9216 5471 3494 9353 6330 4152))
  208 (+ 2031 2180 1544 2509 3894 2882 1460 6647 4655 3164 6691 2156 5754))
  209 (+ 2309 5397 6055 5585 9712 9731 9274))
  210 (+ 9865 7291 4863 10688 4135 4572 7321 5603))
  211 (+ 1428 5533 4032 1648 1676 5556 1186 4594 5915 2477 4923 5393 2101 2509 1250))
  212 (+ 2388 2255 3768 5340 4357 5600 4198 6423 5974 5673 3717 3275 5871 3250))
  213 (+ 11192 1266 3583 10707 11653 3264 6641))
  214 (+ 2009 12343 2394 2147 1560 4352))
  215 (+ 5152 6000 6725 3479 1229 1599 3971 6829 8654))
  216 (+ 7486 15798 2011 9551 15283))
  217 (+ 8934 27039))
  218 (+ 2048 7506 3661 7298 8557 6387 6496 4471 8596 5325))
  219 (+ 1760 2615 1038 9295 6394 7329 5015 4727 9584))
  220 (+ 40347))
  221 (+ 5992 9771 14112))
  222 (+ 13049 14348 13202 10630 9351))
  223 (+ 8778 9152 10173 8648 4552 4300 5921 9924))
  224 (+ 26578 34718))
  225 (+ 2974 3130 4319 4116 3484 5362 5583 2885 4526 2756 5977 2629 2429 1755 1278))
  226 (+ 2848 4821 2207 6922 6699 1999 2354 1922 2133 4496 2510 6509 6929))
  227 (+ 5345 3244 2145 1243 1245 2210 5939 3311 6482 5700 3395 2508 3893 6405))
  228 (+ 3618 2718 4854 1334 3478 3043 3466 1028 2627 3873 4878 5160 6017 4880 1342))
  229 (+ 9909 7167 7465 7787 10618 6259 3751 1488))
  230 (+ 24782 13684 1905))
  231 (+ 5325 9319 7321 6398 8841 3773 2807 9032 2572))
  232 (+ 5346 7500 8693 9429 1728 1303 2467 3959 8196))
  233 (+ 6220 6193 4246 3802 6433 4710 3059 2880 6077 1924 5892))
  234 (+ 3421 1973 9474 3990 15878))
  235 (+ 6757 9558 9440 8896 5221 3819 6669 1578 7307))
  236 (+ 2015 5934 2351 4738 6504 1748 5112 4067 1623 1944 6297 3300 1089))
  237 (+ 1757 4617 8124 6837 4685 9532 11427))
  238 (+ 9094 6552 3882 5341 10752 5572 5882))
  239 (+ 5806 3599 1885 4608 6756 4656 1160 4783 2759 3006 3044 5491 6877))
  240 (+ 6295 18921 23198))
  241 (+ 2201 2488 1050 1414 2799 3883 7092 4746 3719 3211 1548))
  242 (+ 2656 3600 5148 2300 5547 8226 6952 2611 2268 6490))
  243 (+ 5499 8937 12091 1429 9253 2187 2660))
  244 (+ 12898))
  245 (+ 3536 3120 6811 2427 2710 2100 2030 7003 3932 3514 6390 6017))
  246 (+ 7645 3909 2219 2290 1401 1812 3180 7733 2547 2653))  )

(declare-const i1 Int)
(declare-const v1 Int)

(declare-const i2 Int)
(declare-const v2 Int)

(declare-const i3 Int)
(declare-const v3 Int)

(assert (and (>= i1 0) (< i1 len)))
(assert (and (>= i2 0) (< i2 len)))
(assert (and (>= i3 0) (< i3 len)))
(assert (= v1 (select x i1)))
(assert (= v2 (select x i2)))
(assert (= v3 (select x i3)))

(assert (forall ((i Int))
  (>= (select x i1) (select x i))))

(assert (not (= i1 i2)))
(assert (not (= i2 i3)))
(assert (< v2 v1))
(assert (< v3 v2))

(assert (forall ((i Int))
  (ite (= i i1)
       true
       (>= (select x i2) (select x i)))))

(assert (forall ((i Int))
  (ite (or (= i i1) (= i i2))
       true
       (>= (select x i3) (select x i)))))

(declare-const total Int)
(assert (= total (+ v1 v2 v3)))

(check-sat)

(get-value (total))