f600 = 1; f601 = 1; f602 = 0; f603 = 0; f604 = 0; f605 = 0; f606 = 1; f607 = 1; f608 = 1; f609 = 1; f1028 = 4; f1029 = 4; f1026 = 4; f1027 = 4; f1024 = 4; f1025 = 4; f1022 = 4; f1023 = 4; f1020 = 3; f1021 = 3; f932 = 1; f933 = 1; f930 = -inf; f931 = 0; f936 = 1; f937 = 2; f934 = 1; f935 = 2; f938 = 1; f939 = 1; f118 = 5; f119 = 5; f114 = 4; f115 = 4; f116 = 4; f117 = 4; f110 = 4; f111 = 4; f112 = 4; f113 = 4; f590 = 5; f591 = 5; f592 = 5; f593 = 5; f594 = 0; f595 = 0; f596 = 0; f597 = 0; f1242 = 0; f599 = 1; f1240 = 4; f1241 = 4; f1246 = 0; f1247 = 1; f1244 = 0; f1245 = 0; f334 = 3; f335 = 3; f336 = 3; f337 = 3; f330 = 2; f331 = 2; f332 = 2; f333 = 2; f338 = 2; f339 = 2; f41 = 2; f40 = 2; f43 = 1; f42 = 1; f45 = 1; f44 = 1; f47 = 2; f46 = 2; f49 = 2; f48 = 2; f1305 = 2; f1304 = 2; f1303 = 2; f1302 = 2; f1301 = 1; f1300 = 1; f613 = 0; f612 = 0; f611 = 0; f610 = 0; f617 = 1; f616 = 1; f615 = 1; f614 = 1; f619 = 0; f618 = 0; f855 = 1; f854 = 1; f857 = 1; f856 = 1; f851 = 0; f850 = 0; f853 = 0; f852 = 0; f1013 = 3; f1012 = 3; f1011 = 2; f1010 = 2; f859 = 0; f858 = 0; f1015 = 4; f1014 = 3; f929 = 5; f928 = 5; f925 = 4; f924 = 4; f927 = 5; f926 = 5; f921 = 4; f920 = 4; f923 = 4; f922 = 4; f109 = 3; f108 = 3; f107 = 3; f106 = 3; f105 = 4; f104 = 3; f103 = 4; f102 = 3; f101 = 3; f100 = 3; f1277 = 0; f1276 = 0; f1275 = 0; f1274 = 0; f1273 = 1; f1272 = 1; f1271 = 1; f1270 = 1; f1248 = 1; f1279 = 1; f1278 = 1; f583 = 4; f582 = 4; f581 = 3; f580 = 3; f587 = 4; f586 = 4; f585 = 4; f584 = 4; f589 = 4; f588 = 4; f598 = 0; f1243 = 0; f327 = 3; f326 = 3; f325 = 2; f324 = 2; f323 = 2; f322 = 2; f321 = 3; f320 = 2; f329 = 3; f328 = 3; f437 = 2; f436 = 2; f435 = 2; f434 = 2; f433 = 3; f432 = 2; f431 = 3; f430 = 2; f864 = 1; f865 = 2; f866 = 1; f867 = 1; f860 = 1; f861 = 1; f862 = 1; f863 = 2; f1318 = 3; f57 = 2; f54 = 2; f55 = 2; f52 = 1; f53 = 1; f50 = 1; f51 = 1; f1310 = 2; f1311 = 3; f1312 = 2; f1313 = 3; f1314 = 2; f1315 = 2; f1316 = 2; f59 = 1; f1093 = 1; f629 = 0; f626 = 0; f627 = 0; f624 = 1; f625 = 1; f622 = 1; f623 = 1; f620 = 0; f621 = 0; f1004 = 2; f1005 = 2; f1006 = 3; f1007 = 3; f1092 = 1; f1001 = 3; f1002 = 2; f1003 = 2; f1008 = 3; f1009 = 3; f820 = 0; f821 = 0; f822 = 0; f823 = 1; f824 = 1; f825 = 1; f826 = 0; f827 = 0; f828 = 0; f829 = 0; f958 = 2; f959 = 2; f488 = 5; f489 = 5; f482 = 4; f483 = 4; f952 = 2; f953 = 2; f486 = 5; f487 = 5; f484 = 4; f485 = 4; f138 = 0; f139 = 0; f132 = 0; f133 = 0; f130 = 0; f131 = 0; f136 = 1; f137 = 1; f134 = 1; f135 = 1; f1260 = 0; f1261 = 0; f1262 = 1; f1263 = 1; f1264 = 1; f1265 = 1; f1266 = 0; f1267 = 0; f1268 = 0; f1269 = 0; f554 = 2; f555 = 2; f556 = 2; f557 = 2; f550 = 2; f551 = 3; f552 = 2; f553 = 3; f558 = 3; f559 = 3; f312 = 2; f313 = 2; f310 = 2; f311 = 2; f316 = 2; f317 = 2; f314 = 1; f315 = 1; f318 = 2; f319 = 3; f1099 = 1; f1098 = 1; f914 = 3; f915 = 3; f916 = 3; f917 = 3; f910 = 3; f911 = 4; f440 = 3; f441 = 3; f639 = 2; f638 = 1; f631 = 1; f630 = 1; f633 = 1; f632 = 1; f635 = 0; f634 = 0; f637 = 1; f636 = 1; f1071 = 1; f1070 = 1; f1073 = 1; f1072 = 1; f1075 = 0; f1074 = 0; f1077 = 1; f1076 = 1; f1079 = 2; f1078 = 1; f833 = 1; f832 = 1; f831 = 1; f830 = 1; f837 = 0; f836 = 0; f835 = 0; f834 = 0; f839 = 1; f838 = 1; f125 = 0; f124 = 0; f949 = 1; f948 = 1; f121 = 5; f120 = 5; f123 = 0; f122 = 0; f943 = 2; f942 = 2; f941 = 1; f940 = 1; f947 = 1; f946 = 1; f945 = 2; f944 = 2; f1299 = 1; f1298 = 1; f1295 = 2; f1294 = 2; f1297 = 2; f1296 = 2; f1291 = 1; f1290 = 1; f1293 = 1; f1292 = 1; f1109 = 2; f1108 = 2; f1105 = 3; f1104 = 2; f1107 = 2; f1106 = 2; f1101 = 2; f1100 = 2; f1103 = 3; f1102 = 2; f547 = 1; f546 = 1; f545 = 2; f544 = 2; f543 = 2; f542 = 2; f541 = 1; f540 = 1; f549 = 2; f548 = 2; f495 = 2; f494 = 1; f497 = 2; f496 = 1; f491 = 0; f490 = -inf; f493 = 1; f492 = 1; f499 = 1; f498 = 1; f309 = 1; f308 = 1; f305 = 2; f304 = 2; f307 = 1; f306 = 1; f301 = 1; f300 = 1; f303 = 2; f302 = 2; f730 = 1; f887 = 3; f732 = 1; f733 = 1; f734 = 2; f735 = 2; f736 = 2; f737 = 2; f1062 = 1; f1063 = 1; f1060 = 0; f1061 = 0; f1066 = 0; f1067 = 0; f1064 = 1; f1065 = 1; f1068 = 0; f1069 = 0; f808 = 4; f809 = 4; f806 = 4; f807 = 4; f804 = 3; f805 = 3; f802 = 3; f803 = 3; f800 = 3; f801 = 4; f150 = 1; f151 = 1; f152 = 1; f153 = 1; f154 = 0; f155 = 0; f156 = 0; f157 = 0; f158 = 1; f159 = 1; f796 = 3; f797 = 3; f794 = 2; f795 = 2; f792 = 3; f793 = 3; f790 = 3; f791 = 3; f798 = 3; f799 = 4; f1288 = 1; f1289 = 2; f1286 = 1; f1287 = 2; f1284 = 1; f1285 = 1; f1282 = 0; f1283 = 0; f1280 = 1; f1281 = 1; f1118 = 3; f1119 = 3; f1116 = 2; f1117 = 2; f1114 = 2; f1115 = 2; f1112 = 3; f1113 = 3; f1110 = 3; f1111 = 3; f572 = 3; f573 = 3; f570 = 2; f571 = 2; f576 = 3; f577 = 4; f574 = 3; f575 = 4; f578 = 3; f579 = 3; f976 = 2; f977 = 2; f974 = 2; f975 = 2; f972 = 1; f973 = 1; f970 = 1; f971 = 1; f978 = 1; f979 = 1; f1376 = 4; f1377 = 4; f378 = 0; f379 = 0; f370 = 0; f371 = 0; f372 = 0; f373 = 0; f374 = 1; f375 = 1; f376 = 1; f377 = 1; f127 = 1; f126 = 0; f204 = 2; f205 = 2; f206 = 3; f207 = 3; f200 = 3; f201 = 3; f202 = 2; f203 = 2; f208 = 3; f209 = 3; f129 = 1; f128 = 1; f89 = 3; f88 = 3; f85 = 2; f84 = 2; f87 = 3; f86 = 3; f81 = 3; f80 = 2; f83 = 2; f82 = 2; f1059 = 0; f1058 = 0; f1057 = 1; f1056 = 1; f1055 = 1; f1054 = 1; f1053 = 0; f1052 = 0; f1051 = 0; f1050 = 0; f819 = 0; f818 = 0; f811 = 4; f810 = 4; f813 = 4; f812 = 4; f815 = 5; f814 = 5; f817 = 5; f816 = 5; f143 = 1; f142 = 1; f141 = 0; f140 = 0; f147 = 0; f146 = 0; f145 = 1; f144 = 1; f149 = 0; f148 = 0; f781 = 2; f780 = 2; f783 = 3; f782 = 3; f785 = 3; f784 = 3; f787 = 2; f786 = 2; f789 = 2; f788 = 2; f1129 = 4; f1128 = 3; f1123 = 2; f1122 = 2; f1121 = 3; f1120 = 3; f1127 = 4; f1126 = 3; f1125 = 3; f1124 = 3; f569 = 3; f568 = 3; f565 = 2; f564 = 2; f567 = 3; f566 = 3; f561 = 3; f560 = 3; f563 = 2; f562 = 2; f961 = 2; f960 = 2; f963 = 1; f962 = 1; f965 = 1; f964 = 1; f967 = 2; f966 = 2; f969 = 2; f968 = 2; f392 = 1; f393 = 1; f390 = 1; f369 = 1; f368 = 1; f363 = 0; f362 = 0; f361 = 5; f360 = 5; f367 = 1; f366 = 0; f365 = 0; f364 = 0; f394 = 0; f395 = 0; f217 = 4; f216 = 3; f215 = 4; f214 = 3; f213 = 3; f212 = 3; f211 = 2; f210 = 2; f219 = 3; f218 = 3; f1249 = 1; f1309 = 2; f1308 = 2; f1307 = 1; f1306 = 1; f92 = 2; f93 = 2; f90 = 2; f91 = 2; f96 = 3; f97 = 3; f94 = 3; f95 = 3; f98 = 2; f99 = 2; f1048 = 1; f1049 = 1; f1040 = 1; f1041 = 1; f1042 = 0; f1043 = 0; f1044 = 0; f1045 = 0; f1046 = 1; f1047 = 1; f178 = 1; f179 = 1; f176 = 2; f177 = 2; f174 = 2; f175 = 2; f172 = 1; f173 = 1; f170 = 1; f171 = 1; f778 = 2; f779 = 2; f774 = 2; f775 = 3; f776 = 2; f777 = 3; f770 = 1; f771 = 1; f772 = 2; f773 = 2; f1134 = 4; f1135 = 4; f1136 = 4; f1137 = 4; f1130 = 3; f1131 = 3; f1132 = 3; f1133 = 3; f1138 = -inf; f1139 = 0; f518 = 2; f519 = 2; f510 = 2; f511 = 2; f512 = 2; f513 = 2; f514 = 1; f515 = 1; f516 = 1; f517 = 1; f688 = 3; f689 = 4; f680 = 3; f681 = 3; f682 = 2; f683 = 2; f684 = 3; f685 = 3; f686 = 3; f687 = 4; f998 = 3; f999 = 3; f994 = 2; f995 = 2; f996 = 2; f997 = 2; f990 = 2; f991 = 3; f992 = 2; f993 = 3; f424 = 2; f425 = 2; f426 = 1; f427 = 1; f420 = 1; f421 = 1; f422 = 2; f423 = 2; f428 = 2; f429 = 2; f358 = 5; f359 = 5; f194 = 2; f195 = 2; f196 = 2; f197 = 2; f190 = 2; f191 = 3; f192 = 2; f193 = 3; f198 = 3; f199 = 3; f222 = 4; f223 = 4; f220 = 3; f221 = 3; f226 = 3; f227 = 3; f224 = 4; f225 = 4; f228 = 3; f229 = 3; f1019 = 3; f1018 = 3; f1017 = 4; f1016 = 3; f169 = 2; f168 = 1; f1091 = 1; f1090 = 1; f1097 = 2; f1096 = 2; f1095 = 2; f1094 = 2; f161 = 1; f160 = 1; f163 = 0; f162 = 0; f165 = 1; f164 = 1; f167 = 2; f166 = 1; f769 = 2; f768 = 2; f767 = 2; f766 = 2; f765 = 1; f764 = 1; f763 = 1; f762 = 1; f761 = 2; f760 = 2; f1141 = 1; f1140 = 1; f1143 = 2; f1142 = 1; f1145 = 2; f1144 = 1; f1147 = 1; f1146 = 1; f1149 = 1; f1148 = 1; f509 = 1; f508 = 1; f503 = 2; f502 = 2; f501 = 1; f500 = 1; f507 = 1; f506 = 1; f505 = 2; f504 = 2; f699 = 3; f698 = 3; f693 = 3; f692 = 3; f691 = 3; f690 = 3; f697 = 4; f696 = 4; f695 = 4; f694 = 4; f989 = 2; f988 = 2; f987 = 1; f986 = 1; f985 = 2; f984 = 2; f983 = 2; f982 = 2; f981 = 1; f980 = 1; f341 = 3; f340 = 3; f343 = 4; f342 = 3; f345 = 4; f344 = 3; f347 = 3; f346 = 3; f349 = 3; f348 = 3; f439 = 3; f438 = 3; f187 = 1; f186 = 1; f185 = 2; f184 = 2; f183 = 2; f182 = 2; f181 = 1; f180 = 1; f189 = 2; f188 = 2; f239 = 4; f238 = 4; f235 = 3; f234 = 3; f237 = 3; f236 = 3; f231 = 4; f230 = 4; f233 = 4; f232 = 4; f701 = 3; f876 = 1; f875 = 1; f702 = 4; f873 = 2; f704 = 4; f707 = 4; f706 = 4; f0 = 1; f1 = 0; f2 = 1; f3 = 0; f4 = 0; f5 = -inf; f6 = -inf; f7 = 0; f8 = 0; f9 = 0; f1088 = 2; f1089 = 2; f1084 = 1; f1085 = 1; f1086 = 2; f1087 = 2; f1080 = 1; f1081 = 2; f1082 = 1; f1083 = 1; f758 = 2; f759 = 2; f752 = 2; f753 = 2; f750 = 2; f751 = 2; f756 = 1; f757 = 1; f754 = 1; f755 = 1; f1152 = 2; f1153 = 2; f1150 = 2; f1151 = 2; f1156 = 1; f1157 = 1; f1154 = 1; f1155 = 1; f1158 = 2; f1159 = 2; f536 = 2; f537 = 2; f534 = 2; f535 = 2; f532 = 1; f533 = 1; f530 = 1; f531 = 1; f538 = 1; f539 = 1; f402 = 0; f403 = 0; f400 = 1; f401 = 1; f406 = 1; f407 = 2; f404 = 1; f405 = 1; f408 = 1; f409 = 2; f248 = 4; f249 = 4; f240 = 4; f241 = 4; f242 = 3; f243 = 3; f244 = 3; f245 = 3; f246 = 4; f247 = 4; f451 = 2; f450 = 2; f453 = 3; f452 = 3; f903 = 3; f454 = 3; f457 = 4; f456 = 3; f745 = 2; f744 = 2; f747 = 1; f746 = 1; f741 = 1; f740 = 1; f743 = 2; f742 = 2; f749 = 1; f748 = 1; f1169 = 2; f1168 = 2; f1167 = 2; f1166 = 2; f1165 = 1; f1164 = 1; f1163 = 1; f1162 = 1; f1161 = 2; f1160 = 2; f23 = 2; f22 = 1; f21 = 1; f20 = 1; f27 = 1; f26 = 1; f25 = 2; f24 = 1; f1365 = 3; f1364 = 3; f29 = 1; f28 = 1; f1361 = 4; f1360 = 4; f1363 = 3; f1362 = 3; f1185 = 2; f520 = 2; f523 = 1; f1186 = 1; f1181 = 1; f1180 = 1; f1183 = 2; f1182 = 2; f529 = 2; f528 = 2; f1189 = 1; f1188 = 1; f419 = 1; f418 = 1; f415 = 2; f414 = 2; f417 = 2; f416 = 2; f411 = 1; f410 = 1; f413 = 1; f412 = 1; f1215 = 3; f1214 = 3; f1217 = 3; f1216 = 3; f1211 = 2; f1210 = 2; f1213 = 2; f1212 = 2; f1219 = 2; f1218 = 2; f259 = 0; f258 = -inf; f253 = 4; f252 = 4; f251 = 4; f250 = 4; f257 = 5; f256 = 5; f255 = 5; f254 = 5; f356 = 4; f357 = 4; f354 = 4; f355 = 4; f352 = 4; f353 = 4; f723 = 1; f350 = 4; f890 = 2; f351 = 4; f893 = 2; f892 = 2; f895 = 3; f726 = 2; f897 = 3; f896 = 3; f886 = 2; f731 = 1; f884 = 2; f885 = 2; f882 = 1; f883 = 1; f880 = 2; f881 = 2; f738 = 1; f739 = 1; f888 = 2; f889 = 3; f1178 = 1; f1179 = 1; f1170 = 1; f1171 = 1; f1172 = 1; f1173 = 1; f1174 = 2; f1175 = 2; f1176 = 2; f1177 = 2; f30 = 2; f31 = 2; f32 = 2; f33 = 2; f34 = 1; f35 = 1; f36 = 1; f37 = 1; f38 = 2; f39 = 2; f1374 = 4; f1375 = 4; f1372 = 3; f1373 = 3; f1370 = 3; f1371 = 3; f1196 = 2; f1197 = 2; f1194 = 1; f1195 = 1; f1192 = 2; f1193 = 2; f1190 = 2; f1191 = 2; f1198 = 2; f1199 = 3; f648 = 2; f649 = 2; f644 = 1; f645 = 1; f646 = 2; f647 = 2; f640 = 1; f641 = 2; f642 = 1; f643 = 1; f468 = 3; f469 = 3; f398 = 1; f399 = 1; f460 = 3; f461 = 3; f462 = 4; f463 = 4; f464 = 4; f465 = 4; f466 = 3; f467 = 3; f1206 = 3; f1207 = 3; f1204 = 2; f1205 = 2; f1202 = 2; f1203 = 2; f1200 = 2; f1201 = 3; f1208 = 3; f1209 = 3; f266 = 1; f267 = 1; f264 = 1; f265 = 2; f262 = 1; f263 = 2; f260 = 1; f261 = 1; f268 = 1; f269 = 1; f891 = 2; f722 = 1; f721 = 2; f720 = 1; f727 = 2; f894 = 3; f725 = 1; f724 = 1; f899 = 2; f898 = 2; f729 = 2; f728 = 2; f1349 = 3; f1348 = 3; f1343 = 4; f1342 = 4; f1341 = 3; f1340 = 3; f1347 = 3; f1346 = 3; f1345 = 4; f1344 = 4; f659 = 1; f658 = 1; f657 = 2; f656 = 2; f655 = 2; f654 = 2; f653 = 1; f652 = 1; f651 = 1; f650 = 1; f385 = 1; f384 = 1; f387 = 0; f386 = 0; f381 = 0; f380 = 0; f383 = 1; f382 = 1; f389 = 0; f388 = 0; f479 = 4; f478 = 4; f473 = 4; f472 = 4; f471 = 4; f470 = 4; f477 = 3; f476 = 3; f475 = 3; f474 = 3; f1233 = 4; f1232 = 4; f1231 = 4; f1230 = 4; f1237 = 3; f1236 = 3; f1235 = 3; f1234 = 3; f1239 = 4; f1238 = 4; f271 = 2; f270 = 2; f273 = 2; f272 = 2; f275 = 1; f274 = 1; f277 = 1; f276 = 1; f279 = 2; f278 = 2; f56 = 2; f1319 = 3; f58 = 1; f1317 = 2; f628 = 0; f868 = 1; f869 = 1; f718 = 1; f719 = 2; f716 = 1; f717 = 1; f714 = -inf; f715 = 0; f712 = 5; f713 = 5; f710 = 5; f711 = 5; f1354 = 3; f1355 = 3; f1356 = 3; f1357 = 3; f1350 = 4; f1351 = 4; f1352 = 4; f1353 = 4; f1358 = 4; f1359 = 4; f18 = -inf; f19 = 0; f12 = 0; f13 = -inf; f10 = 1; f11 = 0; f16 = -inf; f17 = -inf; f14 = 1; f15 = 1; f668 = 2; f669 = 2; f662 = 2; f663 = 3; f660 = 2; f661 = 2; f666 = 2; f667 = 2; f664 = 2; f665 = 3; f446 = 3; f447 = 3; f444 = 2; f445 = 2; f442 = 2; f443 = 2; f912 = 3; f913 = 4; f918 = 4; f919 = 4; f448 = 3; f449 = 3; f1000 = 3; f1228 = 3; f1229 = 3; f1224 = 3; f1225 = 4; f1226 = 3; f1227 = 3; f1220 = 3; f1221 = 3; f1222 = 3; f1223 = 4; f288 = 2; f289 = 2; f284 = 1; f285 = 1; f286 = 2; f287 = 2; f280 = 2; f281 = 2; f282 = 1; f283 = 1; f1369 = 4; f1368 = 4; f1367 = 4; f1366 = 4; f521 = 2; f1184 = 2; f1187 = 1; f522 = 1; f525 = 1; f524 = 1; f527 = 2; f526 = 2; f950 = 2; f951 = 2; f480 = 4; f481 = 4; f954 = 1; f955 = 1; f956 = 1; f957 = 1; f709 = 4; f708 = 4; f879 = 2; f878 = 2; f877 = 1; f700 = 3; f703 = 4; f874 = 1; f705 = 4; f872 = 2; f871 = 2; f870 = 2; f1321 = 3; f1320 = 3; f1323 = 2; f1322 = 2; f1325 = 2; f1324 = 2; f1327 = 3; f1326 = 3; f1329 = 3; f1328 = 3; f69 = 1; f68 = 1; f67 = 1; f66 = 1; f65 = 2; f64 = 2; f63 = 2; f62 = 2; f61 = 1; f60 = 1; f675 = 2; f674 = 2; f677 = 2; f676 = 2; f671 = 3; f670 = 3; f673 = 3; f672 = 3; f679 = 3; f678 = 3; f1039 = 1; f1038 = 0; f1035 = 0; f1034 = 0; f1037 = 0; f1036 = 0; f1031 = 5; f1030 = 5; f1033 = 5; f1032 = 5; f907 = 2; f906 = 2; f905 = 3; f904 = 3; f455 = 4; f902 = 3; f901 = 2; f900 = 2; f459 = 3; f458 = 3; f909 = 3; f908 = 3; f1259 = 0; f1258 = 0; f1251 = 0; f1250 = 0; f1253 = 0; f1252 = 0; f1255 = 1; f1254 = 1; f1257 = 1; f1256 = 1; f299 = 1; f298 = 1; f297 = 2; f296 = 2; f295 = 2; f294 = 2; f293 = 1; f292 = 1; f291 = 1; f290 = 1; f391 = 1; f396 = 0; f397 = 0; f848 = 1; f849 = 1; f842 = 0; f843 = 0; f840 = 1; f841 = 1; f846 = 1; f847 = 1; f844 = 0; f845 = 0; f1332 = 3; f1333 = 3; f1330 = 2; f1331 = 2; f1336 = 3; f1337 = 4; f1334 = 3; f1335 = 4; f1338 = 3; f1339 = 3; f78 = 2; f79 = 3; f74 = 1; f75 = 1; f76 = 2; f77 = 2; f70 = 2; f71 = 2; f72 = 2; f73 = 2; ---------- ./Problems/SMT/arctic/slice-5/arctic-39bf7cecf04a4493e26e9c8c09e78b72.smt2 ; Sat ; 4.11686086655 ; 0.632225990295 ; None