#include <stdint.h>

uint64_t values[12] = {
	UINT64_C(1486918591), UINT64_C(28100), ~UINT64_C(4),
	UINT64_C(0x2700f184), UINT64_C(0x69b88dcc4d7e98eb),
	UINT64_C(0x0ab8e2a231b49732),
	UINT64_C(0x8226beae36e7317e), UINT64_C(0x5739289992c21658),
	UINT64_C(0x3acce043), ~UINT64_C(8), UINT64_C(4022),
	UINT64_C(63365009),
};