#include <stdint.h>
#define UINT64_MAX                                     (18446744073709551616ULL)

/*
STDC(199901)
*/