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