//----------------------------------------------------------------------
// Simple Hex to Intel Hex file converter
// W. J. Dally - 11/26/01
//----------------------------------------------------------------------
#include <Stdio.h>
#include <stdlib.h>
//----------------------------------------------------------------------
#define BYTES_PER_LINE 8
//----------------------------------------------------------------------
int data[BYTES_PER_LINE] ;
//----------------------------------------------------------------------
// read a line in a hex format
// aaaa dd dd dd dd dd dd dd dd
//
// print a line in hex format
// :llaaaattdd...ddcc
//----------------------------------------------------------------------
void main(){
  int i, cs, address, j ;
  while(!feof(stdin)) {
    j = scanf("%x",&address) ;
    if((j==EOF)||(j==0)) break ;
    if(address == 0xffff) break ;
    for(i=0;i<BYTES_PER_LINE;i++){  
      if(scanf("%x",&(data[i]))==EOF) goto label ;
    }
    printf(":08%04X00",address) ;
    cs = 8 + (address & 0xff) + ((address>>8) & 0xff) ;
    for(i=0;i<BYTES_PER_LINE;i++) {
      printf("%02X",data[i]) ;
      cs = cs+data[i] ;
    }
    cs = (0x100 - cs) & 0xff ;
    printf("%02x\n",cs) ;
  }
label:
  printf(":00000001FF\n") ;
}
//----------------------------------------------------------------------