#!/usr/bin/python3
from MK85 import *

s=MK85()

out = s.BitVec('out', 64)

tmp=[]
for i in range(64):
    tmp.append((out>>i)&0x3F)

# all overlapping 6-bit chunks must be distinct:
s.add(s.Distinct(tmp))
# MSB must be zero:
s.add((out&0x8000000000000000)==0)

print (s.check())

result=s.model()["out"]
print ("0x%x" % result)

# print overlapping 6-bit chunks:
for i in range(64):
    t=(result>>i)&0x3F
    print (" "*(63-i) + format(t, 'b').zfill(6))