// bin2ahex : binary to altera hex of 32 bits width

#include <stdio.h>

int main(void)
{
  int i=0;
  int c;
  printf(":020000020000fc\n");
  while ((c=getchar())!=EOF)
    {
      int j;
      unsigned d;
      char s;
      d=c;
      s=4;
      s+=i;
      s+=i>>8;
      s+=c;
      for (j=1;j<4;j++)
	{
	  if ((c=getchar())!=EOF)
	    {
	      d|=c<<(j*8); 
	      s+=c;
	    }
	  else
	    break;
	}
      printf(":04%04x00%08x%02x\n",i,d,((-s) & 0xff));
      i++;
      if (c==EOF) break;
    }
  printf(":00000001FF\n");
  return 0;
}