int
main (void)
{
  printf ("Hello World!\n");  /* no header */
  return 0;
}
