#include <stdint.h>
typedef int                                                             int32_t;

/*
STDC(199901)
*/