print localtime(int($t/1000)) . ' (' . sprintf("%03d", ($t % 1000)) .  "ms)\n";