open CONFIG, "$hol_file" || die "Cannot open log for writing. $!";