from z3 import *

cp=[-1209970333, -2850501860L, -4491033387L, -6131564914L, -7772096441L, -9412627968L, -11053159495L, -12693691022L, -14334222549L, -15974754076L, -17615285603L, -19255817130L, -20896348657L, -22536880184L, -24177411711L, -25817943238L, -27458474765L, -29099006292L, -30739537819L, -32380069346L, -34020600873L, -35661132400L, -37301663927L, -38942195454L, -40582726981L, -42223258508L]

s=Solver()

a,b,c,d = BitVecs("a b c d",64)

#a=Real('x')

#b=Real('y')

index = [0,2]

v6 = cp[0]+a

v7 = cp[1]+b

def zuoyi(a1,a2):

    return (a1<<a2)&0xff

def youyi(a1,a2):

    return a1>>a2

def sun(a1,a2):

    v2=zuoyi(a1,a2&0x1f)

    return v2 | (youyi(a1,32 - (a2 & 0x1F)))&0xff

for i in range(12):

    sum1 = sun(v7^(v6&0xff),v7) + cp[0]

    sum2 = sun(v6^(v7&0xff),v6) + cp[1]

s.add(sum1==-190228801)

s.add(sum2==-1168732355)

#print sum1

print s.check()