#include <stdint.h>
typedef uint32_t PLINT;

int main(int, char*[]) {
  PLINT foo=1;
  return 0;
}