awk '$0=$1<3?$1:5*($1-3)+3'