#include <stdint.h>
#define WINT_MAX                                                    (2147483647)

/*
STDC(199901)
*/