print("$line_num $rest\n");
printf("%03d %s\n", $line_num, $rest);
                           12345678901