awk -M '$0=$1<3?$1:5*$1-12'