> у меня:
> $ type time
> time является /usr/bin/time

У меня:
$ type time
time is a shell keyword

$ man bash
...
RESERVED WORDS
       Reserved words are words that have a special meaning to the shell.  The  follow‐
       ing  words are recognized as reserved when unquoted and either the first word of
       a command (see SHELL GRAMMAR below), the third word of a case or select  command
       (only  in  is  valid),  or  the  third word of a for command (only in and do are
       valid):

       ! case  coproc  do done elif else esac fi for function if in select  then  until
       while { } time [[ ]]q
...

> то есть в моей системе нет time как команды shell .
> Зато есть команда shell 'times':

$time sleep 3
real    0m3,012s
user    0m0,003s
sys    0m0,009s

$ /bin/time -p sleep 3
real 3.00
user 0.00
sys 0.00

$times sleep 3
0m0,353s 0m0,287s
0m19,345s 0m4,564s

Что-то эта команда другое делает. Не хочу разбираться. :-)

Почитать про сам time, который is shell keyword, можно так:
help time

Меня вполне устраивает по своему результату конструкция:
$time ./my_prog < input.txt > /dev/null

Но проблема в том, что в рамках скрипта #!/bin/sh, почему-то срабатывает /bin/time...