from z3 import *



def ror8(a,b):
    return RotateRight(a,b)

def rol8(a,b):
    return RotateLeft(a,b)

input = BitVec("buf" , 64)

v533 = rol8(input, 48);
v534 = ror8(v533, 28);
v535 = rol8(v534, 48);
v536 = ror8((v535 ^ 0x7C8A34C5E84FF9C2) + 365916104, 58);
v537 = rol8(v536 - 1314176731, 28);
v538 = ror8(v537, 57);
v539 = ror8(v538, 17);
v540 = rol8(v539, 46);
v541 = rol8(v540, 0);
v542 = rol8(v541 + 2499302335, 34);
v543 = rol8(v542, 4);
v544 = rol8(v543 ^ 0x29EABB4C5AA04268, 63);
v545 = ror8(v544, 64);
v546 = ror8(v545, 64);
v547 = ror8(v546 + 543427281, 43);
v548 = ror8(v547, 42);
v549 = ror8(v548, 26);
v550 = rol8(v549, 43);
v551 = rol8(v550, 22);
v552 = rol8(v551 - 125062904, 42);
v553 = rol8(v552 - 953577019 + 1865970985, 7);
v554 = ror8(v553, 28);
v555 = rol8(v554 ^ 0x141B8691D7B6B8BB, 64);
v556 = ror8((v555 + 1623747214) ^ 0x908812017F8AE0C3, 25);
v557 = rol8(v556, 40);
v558 = rol8((v557 + 731816048) ^ 0xB4EC588D66219B7C, 50);
v559 = ror8(v558, 6);
v560 = ror8(v559 ^ 0xDADA4F98F3E2C282, 7);
v561 = ror8(v560 ^ 0x41249D6920AF3840, 58);
v562 = rol8(v561, 24);
v563 = ror8(v562, 36);
v564 = rol8(v563, 5);
v565 = ror8((v564 ^ 0x508B64BDD3CDE0F8) - 4618774765, 26);
v566 = ror8(v565, 26);
v567 = ror8(v566, 25);
v568 = ror8(v567 + 2089431261, 64);
v569 = rol8(v568 ^ 0xDF2890BE42CEDF58, 16);
v570 = rol8(v569 ^ 0xCCA4209900BAB11C, 18);
v571 = rol8((v570 ^ 0x770EEA1CF61DF9AB) + 749855658, 56);
v572 = ror8(v571 ^ 0xCBA0FA860852750E, 2);
v573 = ror8(v572, 49);
v574 = ror8(v573, 30);
v575 = ror8(v574, 35);
v576 = rol8(v575, 37);
v577 = rol8((v576 - 797200417) ^ 0x9796432C1F6880AA, 9);
v578 = ror8(v577, 51);
v579 = rol8(v578, 43);
v580 = rol8(v579, 51);
v581 = rol8(v580, 3);
v582 = rol8((v581 + 1556301638) ^ 0xBFEA9C009548E06C, 10);
v583 = rol8(((v582 ^ 0x5176B884724A94B5) - 1551316485) ^ 0xC196D720D092A491, 56);
v584 = rol8(v583 - 584591141, 28);
v585 = rol8(v584, 19);
v586 = ror8(v585, 52);
v587 = ror8(v586 ^ 0x839F53118B284FCE, 60);
v588 = rol8(v587, 22);
v589 = rol8(v588 + 26316176, 16);
v590 = ror8((v589 ^ 0xE1820828D8312BF0) + (3588543110 & 0xffffffffffffffff), 13);
v591 = ror8(v590 ^ 0x219FF219DAC612E1, 64);
v592 = rol8(v591, 42);
v593 = ror8(v592 - 1955517967, 28);
v594 = ror8(v593, 15);
v595 = rol8(v594 - 781818201, 52);
v596 = ror8((v595 ^ 0x9BE76350B1251F3A) + 262334776, 32);
v597 = rol8(v596 - 2296363855, 37);
v598 = ror8(v597 ^ 0xB326E771471AEC87, 19);
v599 = rol8(v598, 54);
v600 = ror8(v599, 48);
v601 = rol8(v600, 44);
v602 = ror8((v601 ^ 0xF6713E4F814C2CC8) - 1978112454, 2);
v603 = ror8(v602, 56);
v604 = rol8(v603 - 2211796515, 61);
v605 = rol8(v604, 58);
v606 = rol8(v605, 16);
v607 = ror8(v606 ^ 0xD0571A355B7E1FF4, 4);
v608 = ror8(v607, 18);
v609 = ror8(v608, 23);
v610 = ror8(v609, 47);
v611 = ror8(v610, 26);
v612 = ror8(v611, 42);
v613 = ror8(v612, 2);
v614 = rol8((v613 ^ 0x91873E78D47C89F2) - 1218173186, 6);
v615 = ror8(v614, 4);
v616 = rol8(v615, 7);
v617 = rol8(v616 + 1392556645, 21);
v618 = ror8(v617, 58);
v619 = ror8(((v618 - 763488126) ^ 0x32789A752ED060A6) - 993913077, 9);
v620 = ror8(v619, 9);
v621 = rol8(v620, 53);
v622 = ror8(v621, 48);
v623 = ror8(v622, 24);
v624 = rol8(v623, 38);
v625 = rol8((v624 ^ 0x50908E0A61C67139) - 1040006147, 10);
v626 = ror8(v625 + 1201763364, 28);
v627 = ror8(v626, 35);
v628 = rol8(v627, 1);
v629 = rol8(v628, 44);
v630 = rol8(v629, 35);
v631 = ror8(v630 ^ 0x9ED862BFCF4FC1E9, 60);
v632 = rol8(v631, 45);
v633 = ror8(v632, 31);
v634 = rol8(v633, 2);
v635 = rol8(v634 ^ 0xC6965820803E6C22, 53);
v636 = rol8(v635 ^ 0xCCE7F1B135E80B81, 47);
v637 = rol8((v636 - 2469287539) ^ 0x774EE66BD84B7D7E, 1);
v638 = rol8(v637, 38);
v639 = rol8(v638 + 1171877673, 50);
v640 = ror8(v639 ^ 0x5553F131E60F2B65, 5);
v641 = rol8(v640, 36);
v642 = ror8(v641 ^ 0x1A1830E5FBBC72E, 7);
v643 = ror8(v642, 3);
v644 = ror8(v643 ^ 0x8F0A2731511587C7, 16);
v645 = ror8(v644, 61);
v646 = rol8((v645 + 2135774281) ^ 0x582089E0D818852F, 36);
v647 = ror8(v646, 55);
v648 = ror8(v647, 47);
v649 = rol8(v648, 18);
v650 = rol8(v649, 8);
v651 = ror8(v650 ^ 0x6B259DBEC0B8C23E, 19);
v652 = rol8(v651 ^ 0xCB689FAB003E802A, 27);
v653 = ror8((v652 ^ 0x7CE2DA24E00763B8) + 2134012006, 40);
v654 = ror8(v653, 11);
v655 = rol8(v654 + 956771026, 16);
v656 = rol8(v655, 39);
v657 = ror8(v656 ^ 0xE1424FDE31A85BE1, 26);
v658 = rol8(v657 + 1685335456, 43);
v659 = rol8(v658, 8);
v660 = rol8(v659, 41);
v661 = ror8(v660, 12);
v662 = ror8(v661 ^ 0xAE5E353FA9369E9C, 57);
v663 = ror8(v662 ^ 0x2D6500EADED5A729, 33);
v664 = rol8(v663, 11);
v665 = ror8(v664, 41);
v666 = rol8(v665, 21);
v667 = rol8(v666 - 1425542105, 40);
v668 = ror8((v667 - 2133293282) ^ 0x92642B584D828B0A, 43);
v669 = ror8(v668, 20);
v670 = rol8(v669, 61);
v671 = ror8(v670, 49);
v672 = ror8(v671 - 571321309, 5);
v673 = ror8(v672 ^ 0xA71E0FE57F8CBFE9, 63);
v674 = rol8(v673, 40);
v675 = ror8(v674, 13);
v676 = rol8(v675 + 1112323808, 24);
v677 = rol8(v676, 19);
v678 = rol8(v677, 35);
v679 = ror8(v678, 2);
v680 = rol8(v679, 45);
v681 = ror8(v680, 37);
v682 = rol8(v681, 37);
v683 = ror8(v682, 25);
v684 = rol8(v683, 23);
v685 = rol8(v684, 44);
v686 = rol8(v685, 1);
v687 = ror8(v686, 63);
v688 = ror8(v687 ^ 0x31EDDAC9A946CD8E, 40);
v689 = rol8(v688 ^ 0x8DC48B6C51FB67DE, 58);
v690 = ror8(v689, 15);
v691 = ror8((v690 ^ 0x34A3BC81FDA9319E) + 396032210, 28);
v692 = ror8(v691, 16);
v693 = ror8(v692, 0);
v694 = ror8(v693 - 1254740817, 4);
v695 = ror8(v694, 60);
v696 = rol8(v695, 11);
v697 = rol8(v696 - 1340370624, 10);
v698 = ror8(v697, 9);
v699 = rol8(v698 + 634911122, 21);
v700 = ror8(v699, 0);
v701 = rol8((((v700 ^ 0xA3027FFD8E6634B6) + 1321574253) ^ 0x57AC66AEA0276EE6) - 1463827211, 31);
v702 = ror8(v701, 33);
v703 = rol8(v702, 45);
v704 = ror8(v703, 61);
v705 = rol8(v704, 8);
v706 = ror8((((v705 + 2188175405) ^ 0xD3C92459879C1820) + 1783889000) ^ 0xB3EF85726F53BC81, 35);
v707 = ror8(v706, 10);
v708 = ror8(v707, 63);
v709 = ror8(((v708 ^ 0x625A7F300F87688B) + 2020157351) ^ 0x123C291CA9DC51FA, 33);
v710 = ror8(v709 - 557754125, 27);
v711 = ror8(v710 ^ 0xD6133F96F70F1832, 3);
v712 = rol8(v711, 40);
v713 = ror8((v712 ^ 0xEA5F3D19663FDEBB) + (2673007032 & 0xffffffffffffffff), 22);
v714 = rol8(v713, 44);
v715 = ror8(v714, 42);
v716 = ror8(v715, 24);
v717 = ror8(v716 - 2502717952, 35);
v718 = rol8(v717, 28);
v719 = rol8(v718 - 974252697, 24);
v720 = ror8(v719 - 2346856762 + 2470485935, 40);
v721 = rol8(v720, 41);
v722 = ror8(v721 - 1117991261, 41);
v723 = ror8(v722 - 2584055713, 17);
v724 = ror8(v723, 41);
v725 = ror8(v724, 39);
v726 = rol8(v725, 20);
v727 = rol8(v726 - 945428400, 26);
v728 = ror8(v727, 35);
v729 = ror8(v728, 10);
v730 = ror8(v729 + 1323390616, 43);
v731 = rol8(v730, 26);
v732 = rol8(v731 + 1751003863, 42);
v733 = rol8(v732 - 1355585359, 0);
v734 = rol8(v733 + 1258573883, 23);
v735 = ror8(v734 + 1152560063, 25);
v736 = ror8(v735, 24);
v737 = ror8(v736, 1);
v738 = rol8(v737, 39);
v739 = rol8(v738, 9);
v740 = ror8(v739, 61);
v741 = rol8(v740 - 1984100912, 58);
v742 = ror8((v741 + 986815966) ^ 0x474DC84C20DDE987, 32);
v743 = rol8(v742, 20);
v744 = rol8((((v743 + 523119852) ^ 0xD3910648BBA12A42) + 1350638991) ^ 0x2D337097371538CC, 38);
v745 = ror8(v744, 25);
v746 = ror8(v745 + 883675169, 8);
v747 = ror8(v746, 35);
v748 = rol8(v747 ^ 0x776B8CABC0FD885B, 61);
v749 = ror8(v748 - 1523035201, 43);
v750 = ror8(v749, 7);
v751 = ror8(v750, 23);
v752 = ror8(v751, 61);
v753 = ror8(v752 ^ 0xA6EEB1B8DF3F7A35, 17);
v754 = ror8((((v753 ^ 0x8F4FF3A784F6AD45) - (3959562642 & 0xffffffffffffffff)) ^ 0xA46F35E8FC454BCE) + 813737596, 57);
v755 = rol8(v754, 15);
v756 = rol8((v755 ^ 0xB9A16C3A7A836F8F) - 1247957728, 26);
v757 = rol8((v756 ^ 0x3A422D7ADD27C86C) - 2326298844 + 411078670, 45);
v758 = ror8(v757, 38);
v759 = ror8(v758, 40);
v760 = ror8(v759 + 2492062388, 1);
v761 = ror8(v760, 45);
v762 = rol8(v761, 29);
v763 = ror8(v762 + 4577651661, 58);
v764 = rol8(v763 ^ 0xDF3DB3A43BBC4C7C, 43);
v765 = ror8(v764, 47);
v766 = rol8(v765 + 1950185900, 17);
v767 = rol8(v766 - 1936576703, 64);
v768 = ror8(v767, 26);
v769 = ror8(v768, 14);
v770 = ror8(v769 ^ 0xA1E055C9AEF9C7B2, 42);
v771 = ror8(v770 ^ 0xE22BA874A28FAA9C, 35);
v772 = ror8(v771 ^ 0xB309073F801359BD, 63);
v773 = rol8(v772, 22);
v774 = ror8(v773, 22);
v775 = ror8(v774 + 2310374846, 6);
v776 = ror8(v775 + 692052532, 21);
v777 = rol8(v776, 29);
v778 = ror8(v777, 33);
v779 = rol8(v778 + 2450945669, 40);
v780 = rol8(v779 ^ 0x25B54FED9F72BFFD, 57);
v781 = rol8(v780 + 1128434817, 12);
v782 = rol8(v781, 37);
v783 = rol8(v782 ^ 0xBD4128438551F4DF, 8);
v784 = rol8(v783, 25);
v785 = rol8(v784, 6);
v786 = ror8(v785, 53);
v787 = ror8(v786, 28);
v788 = ror8(v787, 60);
v789 = ror8(v788 - 773597232, 2);
v790 = rol8((v789 ^ 0x4FE2EA2173C0AC6E) + 2397559178, 7);
v791 = rol8(v790, 61);
v792 = ror8(v791, 44);
v793 = rol8(v792, 14);
v794 = ror8(v793, 22);
v795 = ror8(v794, 3);
v796 = ror8(v795 + 1979997106, 3);
v797 = ror8(v796 - 1119807131, 47);
v798 = ror8(v797 ^ 0x67B4A786A12DEBC8, 47);
v799 = rol8(v798, 24);
v800 = ror8(v799, 41);
v801 = rol8(v800, 47);
v802 = ror8(v801, 25);
v803 = rol8(v802, 10);
v804 = rol8(v803, 53);
v805 = ror8(v804 + 166559990, 5);
v806 = ror8(v805, 24);
v807 = rol8(v806 + 1939684457, 12);
v808 = rol8(v807 - 847055132, 63);
v809 = ror8(v808, 54);
v810 = ror8(v809, 3);
v811 = rol8(v810, 46);
v812 = rol8(v811, 49);
v813 = ror8(v812, 29);
v814 = rol8((v813 ^ 0xD8BF44A2BD660025) + (2385916922 & 0xffffffffffffffff), 26);
v815 = rol8(v814 ^ 0x3DA0E24A5762B0A2, 28);
v816 = ror8(v815, 39);
v817 = rol8(v816, 57);
v818 = rol8((v817 ^ 0xFB7182E7AFB095DB) - 592778886, 64);
v819 = ror8(v818, 24);
v820 = ror8(v819 ^ 0x9E535379E667C318, 27);
v821 = ror8(v820 + 1197900025, 57);
v822 = rol8(v821, 53);
v823 = rol8(v822, 17);
v824 = rol8(v823, 58);
v825 = rol8(v824, 46);
v826 = ror8(v825, 28);
v827 = rol8(v826 ^ 0x1635F8D922CC7E, 40);
v828 = ror8(v827 + 3518693969, 7);
v829 = ror8(v828, 43);
v830 = rol8(v829, 16);
v831 = rol8(v830, 38);
v832 = rol8(v831, 61);
v833 = ror8(v832 + 2172702168, 14);
v834 = ror8(v833 ^ 0xF8806D812BEE0ED7, 52);
v835 = rol8(v834 ^ 0x28F2EFDF47A67A32, 8);
v836 = ror8(v835 + 1519583631, 57);
v837 = rol8(v836, 59);
v838 = ror8(v837, 37);
v839 = rol8((v838 ^ 0xE6301B59C7208120) - 545750604, 30);
v840 = rol8(v839, 8);
v841 = ror8(v840 + 1872945756, 55);
v842 = ror8(v841, 0);
v843 = ror8(v842, 31);
v844 = ror8(v843, 46);
v845 = rol8(v844, 5);
v846 = ror8(v845 + 1402534426, 26);
v847 = ror8(v846 ^ 0xF1BE0EFB45A3E0E9, 1);
v848 = rol8(v847, 47);
v849 = rol8(v848, 21);
v850 = rol8(v849, 21);
v851 = ror8(v850, 42);
v852 = rol8(v851 + 1088410395, 49);
v853 = rol8(v852 ^ 0x299657B16C64F4DC, 32);
v854 = rol8(v853, 3);
v855 = rol8(v854 + 3566130234, 19);
v856 = rol8(v855, 19);
v857 = ror8(v856 + 4460399, 51);
v858 = ror8(v857, 4);
v859 = rol8(v858, 1);
v860 = rol8(v859, 19);
v861 = ror8(v860, 34);
v862 = ror8(v861, 63);
v863 = rol8((v862 ^ 0x285C6D49F398C9EC) + 2373161673, 53);
v864 = ror8((((v863 ^ 0x27BB274530B8A15E) - 1237997577) ^ 0x8AD5C89E5C91FAE2) + 1419997013, 15);
v865 = rol8(v864, 0);
v866 = rol8(v865, 38);
v867 = rol8(v866, 24);
v868 = rol8(v867, 8);
v869 = rol8((v868 ^ 0xC7AC28C1728AAA7B) - 387938428, 53);
v870 = ror8(v869, 33);
v871 = rol8(v870 ^ 0x1434AC1C2F3B8657, 40);
v872 = rol8(v871 ^ 0x42237D4097E2C089, 5);
v873 = rol8(v872, 56);
v874 = rol8(v873, 18);
v875 = ror8(v874, 45);
v876 = rol8(v875, 41);
v877 = ror8(v876, 39);
v878 = rol8(v877 - 831669556, 56);
v879 = ror8(v878 ^ 0x1B43623A7A30D5E2, 41);
v880 = rol8(v879, 1);
v881 = rol8(v880 ^ 0xA1CC262DBDF142C4, 17);
v882 = rol8(v881 + 3829990965, 51);
v883 = rol8(v882, 62);
v884 = rol8(v883, 38);
v885 = ror8(v884 ^ 0x325514F5330F1A22, 40);
v886 = rol8(v885 ^ 0xF8C259DA4FDECFA5, 14);
v887 = rol8(v886, 8);
v888 = ror8(v887 ^ 0x5D4B5766B7F4E35C, 37);
v889 = ror8(v888, 2);
v890 = ror8(v889, 7);
v891 = rol8((v890 + 2562904134) ^ 0x614CDA9159AFF761, 12);
v892 = ror8(v891 - 1399420156, 57);
v893 = ror8(v892, 9);
v894 = rol8(v893 ^ 0xD793570F4852AD32, 14);
v895 = ror8(v894, 36);
v896 = rol8(v895 ^ 0xEAA5F070663A7889, 4);
v897 = ror8(v896, 59);
v898 = rol8(v897, 55);
v899 = rol8(v898 - 3294510276, 31);
v900 = rol8((v899 ^ 0xE05303B088C43109) - (2473708600 & 0xffffffffffffffff), 7);
v901 = ror8(v900, 8);
v902 = ror8(v901 ^ 0x3C7F427C8796284C, 23);
v903 = ror8(v902, 33);
v904 = rol8((v903 ^ 0xF16A7A0B54187275) - 1677570727, 33);
v905 = ror8(v904 ^ 0xEA7427E0D00602A5, 21);
v906 = ror8(v905, 0);
v907 = rol8(v906, 9);
v908 = rol8(v907, 1);
v909 = ror8(v908, 33);
v910 = ror8(v909 + 144620561, 44);
v911 = rol8(v910 - 2309661763, 62);
v912 = rol8(v911 ^ 0x3D825C1E9B4BCD33, 14);
v913 = rol8(v912, 34);
v914 = rol8(v913, 36);
v915 = ror8(v914 ^ 0x2D370175C40CAAFF, 4);
v916 = rol8((v915 + 1316873188) ^ 0xC78F2939526C202C, 36);
v917 = rol8((v916 + 2501555959) ^ 0xE9EE32814E52A802, 6);
v918 = rol8(v917, 4);
v919 = ror8(v918 ^ 0x3ADAD82E4F1FA242, 15);
v920 = ror8(v919, 23);
v921 = ror8(v920 - 2492924372, 0);
v922 = ror8(v921, 10);
v923 = ror8(v922, 14);
v924 = ror8((v923 ^ 0x5AAFE4672E910C04) - 1966926629, 54);
v925 = ror8(v924, 57);
v926 = rol8(v925, 40);
v927 = ror8(v926 + 608460574, 31);
v928 = ror8(v927, 53);
v929 = rol8(v928, 10);
v930 = ror8(v929, 57);
v931 = rol8(v930 ^ 0xF580B100D338ADB5, 50);
v932 = rol8(v931, 24);
v933 = rol8(v932, 14);
v934 = rol8(v933 + 2101439829, 35);
v935 = rol8(((v934 - 659893494 + 2204452641) ^ 0x9F57D52150C2F8EA) + (2168448924 & 0xffffffffffffffff), 27);
v936 = ror8(v935 ^ 0x78D2BED6BBC3EA3, 6);
v937 = ror8(v936 - 2413847973, 44);
v938 = ror8(v937, 5);
v939 = ror8((v938 - 3154530539) ^ 0xB0549D3869A01D2F, 54);
v940 = rol8(v939, 25);
v941 = rol8(v940, 55);
v942 = ror8(v941 ^ 0x78A1839ABCD56F08, 12);
v943 = ror8(v942, 41);
v944 = ror8(v943, 11);
v945 = rol8(v944, 34);
v946 = rol8(((v945 ^ 0xD2A641EC7A3DA2FF) + 1448720418) ^ 0x3A484D7A3C9BE1E4, 27);
v947 = rol8(v946, 26);
v948 = rol8(v947 - 2145715231, 7);
v949 = ror8(v948, 16);
v950 = rol8(v949 + 1991561095, 52);
v951 = ror8(v950, 50);
v952 = rol8(v951, 61);
v953 = ror8(v952, 51);
v954 = rol8(v953 - 1577991232, 14);
v955 = ror8(v954, 39);
v956 = ror8(v955, 18);
v957 = rol8(v956 ^ 0x7015C0F166E904D4, 1);
v958 = rol8(v957 + 1743998716, 5);
v959 = rol8(v958, 12);
v960 = ror8(v959, 47);
v961 = rol8(v960 ^ 0xB4C524E317EA3A43, 28);
v962 = rol8(v961, 16);
v963 = ror8(v962, 37);
v964 = ror8(v963 ^ 0x89119F0C81023738, 40);
v965 = ror8(v964, 28);
v966 = rol8((v965 ^ 0x442F9EC8423F5449) + 2134464929, 9);
v967 = ror8(v966, 25);
v968 = ror8((v967 ^ 0x610F8A76BA5200B2) - 1188483979, 39);
v969 = rol8(v968, 21);
v970 = rol8(v969, 18);
v971 = rol8(v970 + 1155915905, 39);
v972 = ror8(v971, 6);
v973 = rol8((v972 ^ 0xDE5184C1C5AAAE90) + 1605063939, 9);
v974 = ror8((((v973 + 1717103935) ^ 0x8999675FAA08F92C) + (2318583546 & 0xffffffffffffffff)) ^ 0xE8F9752268E7DC9F, 61);
v975 = ror8(v974, 23);
v976 = rol8(v975, 57);
v977 = ror8(v976, 11);
v978 = ror8(v977, 61);
v979 = rol8(v978, 28);
v980 = rol8(v979, 45);
v981 = rol8(v980, 1);
v982 = rol8(v981, 55);
v983 = rol8(v982 ^ 0xD584ECDCE92AFD72, 9);
v984 = ror8(v983, 30);
v985 = ror8(v984 - 2226684184, 0);
v986 = ror8(v985, 21);
v987 = rol8(v986, 2);
v988 = ror8(v987 ^ 0x6E195E40F0E843AD, 46);
v989 = ror8(v988, 62);
v990 = ror8((v989 ^ 0x2B7D0B7FCDE52CAE) + 372399185, 55);
v991 = ror8(v990 - 979493889, 33);
v992 = rol8(v991, 17);
v993 = rol8(v992, 36);
v994 = ror8(v993 ^ 0xCCEA1EF26B078066, 23);
v995 = ror8(v994 + 2084028622, 7);
v996 = rol8(v995, 35);
v997 = ror8(v996, 23);
v998 = rol8(v997, 60);
v999 = ror8((v998 ^ 0xEC85204E427CEB73) - 2140847765, 12);
v1000 = rol8(v999 - 1771941597, 58);
v1001 = ror8(v1000, 45);
v1002 = ror8(v1001, 16);
v1003 = rol8(v1002, 41);
v1004 = rol8(v1003, 35);
v1005 = rol8(v1004, 6);
v1006 = ror8(v1005 ^ 0xB12B1C0887DBEA3B, 0);
v1007 = ror8(v1006, 22);
v1008 = rol8(v1007, 54);
v1009 = ror8(v1008, 25);
v1010 = ror8(v1009 - 1843290958, 34);
v1011 = rol8(v1010, 27);
v1012 = rol8(v1011, 32);
v1013 = ror8(v1012 - 2171752296, 54);
v1014 = ror8(v1013 ^ 0x8D88E2BC49FC3564, 55);
v1015 = rol8((v1014 + 1337935076) ^ 0xB6DEADFC1001F64B, 25);
v1016 = rol8(v1015, 17);
v1017 = ror8(v1016 - 1773520261, 20);
v1018 = rol8(v1017, 27);
v1019 = ror8(v1018, 19);
v1020 = rol8(v1019 - 795094491, 53);
v1021 = ror8((v1020 + 2451846194) ^ 0x66BDF7A975EF077D, 32);
v1022 = rol8(v1021, 59);
v1023 = ror8(v1022 ^ 0xA510E931ED9FB616, 28);
v1024 = rol8(v1023 - 1309318850, 14);
v1025 = ror8(v1024, 51);
v1026 = rol8(v1025, 48);
v1027 = ror8(v1026, 52);
v1028 = ror8(v1027, 11);
v1029 = rol8(v1028, 39);
v1030 = rol8(v1029, 40);
v1031 = rol8(v1030, 51);
v1032 = ror8(v1031, 59);
v1033 = rol8(v1032, 49);
v1034 = ror8(v1033 - 1878205927, 2);
v1035 = ror8(v1034, 26);
v1036 = ror8(v1035, 45);
v1037 = ror8(v1036, 35);
v1038 = rol8(v1037, 38);
v1039 = ror8(((v1038 ^ 0x5928D9D754C0A13E) - 640609561) ^ 0xB2BB322D9D6CD1B0, 6);
v1040 = ror8(v1039, 58);
v1041 = ror8(v1040, 49);
v1042 = ror8(v1041 ^ 0xCF7C0026B6B10930, 27);
v1043 = ror8(v1042, 7);
v1044 = ror8(v1043, 45);
v1045 = ror8(v1044, 14);
v1046 = rol8(v1045, 59);
v1047 = rol8(v1046, 56);
v1048 = rol8(v1047, 61);
v1049 = rol8(v1048 - 358330380, 38);
v1050 = ror8(((v1049 + 1418789870) ^ 0x47BA6455BAC3C9F) - 2321561993, 34);
v1051 = rol8(v1050, 21);
v1052 = rol8(v1051, 28);
v1053 = ror8(v1052, 4);
v1054 = ror8(v1053 + 1693398710, 44);
v1055 = ror8(v1054 ^ 0x644D82B1DFA4483C, 32);
v1056 = ror8(v1055, 27);
v1057 = rol8(v1056, 21);
v1058 = rol8(v1057 ^ 0x7AFFFD2BBCB10E40, 12);
v1059 = rol8(v1058 - 422097114, 8);
v1060 = ror8(v1059 ^ 0x74F69AD69C652296, 56);
v1061 = ror8(v1060 + 825496093, 53);
v1062 = rol8(v1061 ^ 0xAD7E0FE96E2AB98A, 34);
v1063 = ror8(v1062, 54);
v1064 = ror8(((v1063 + 587372517) ^ 0x8ED60A3E784B689C) - 1977221759, 37);
v1065 = rol8(v1064 - 1180122135, 2);
v1066 = ror8(v1065, 13);
v1067 = ror8(v1066, 61);
v1068 = ror8(v1067, 10);
v1069 = rol8(v1068, 48);
v1070 = rol8(v1069 ^ 0x310279364A066080, 47);
v1071 = rol8(v1070, 58);
v1072 = rol8(v1071, 31);
v1073 = ror8(v1072, 6);
v1074 = ror8(v1073, 17);
v1075 = rol8(v1074 - 1772600999, 59);
v1076 = ror8(v1075, 22);
v1077 = rol8(v1076, 50);
v1078 = ror8(v1077, 31);
v1079 = ror8(v1078, 59);
v1080 = rol8(v1079, 26);
v1081 = rol8(v1080, 1);
v1082 = rol8(v1081, 3);
v1083 = ror8(v1082 ^ 0x917ADB05A8967A65, 32);
v1084 = ror8(v1083, 12);
v1085 = ror8(v1084 ^ 0x82B8FA0BEC02D6AB, 29);
v1086 = ror8(v1085, 37);
v1087 = rol8(v1086 ^ 0x7A3382324E265073, 42);
v1088 = rol8(v1087, 58);
v1089 = rol8((v1088 - 2208445724) ^ 0xEFFF18A64D8D15B0, 7);
v1090 = ror8(v1089 + 1661501117, 34);
v1091 = ror8(v1090, 4);
v1092 = rol8(v1091 - 1708467213 + 1752515344, 18);
v1093 = ror8(((v1092 ^ 0xB781649DE00B25C3) - 979889615) ^ 0x22C441D025A23742, 44);
v1094 = rol8(v1093, 31) ^ 0x2B6A0E54C8A4D626;

final  = rol8(v1094, 2)
s = Solver()

s.add( final == 1983272704493466908 )

print s.check()
m = s.model()
print m