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