#include <stdio.h>
#include <string.h>

char buffer[3276800];

int main(void) {
	char* pos;
	int count;
	while(1) {
		fgets(buffer,sizeof(buffer),stdin);
		pos=strchr(buffer,'\n');
		if(pos==NULL)pos=&buffer[strlen(buffer)];
		pos[0]=' ';
		pos[1]=0;
		if(strcmp(buffer,"END OF INPUT ")==0)break;
		for(pos=buffer,count=0;*pos!=0;pos++) {
			if(*pos==' ') {
				printf("%d",count);
				count=0;
			} else {
				count++;
			}
		}
		putchar('\n');
	}
	return 0;
}