def format_time(time):
hours, remainder = divmod(time / <NUM_LIT:1000>, <NUM_LIT>)<EOL>minutes, seconds = divmod(remainder, <NUM_LIT>)<EOL>return '<STR_LIT>' % (hours, minutes, seconds)<EOL>
Formats the given time into HH:MM:SS.