seq 8e3|factor|awk '$0*=/: [2357]*$/'