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