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