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