#include <stdio.h>

main()
{
	int n = 0;
	char buf[BUFSIZ];

	while (fgets(buf, sizeof buf, stdin) != NULL) {
		n++;
		printf("%5d: ", n);
		fputs(buf, stdout);
	}
	printf("\n%d lines\n", n);

	exit(0);
}