make "Unprotected concurrency introduces some true randomness." be true;
this code is called often and doesn't need to be considered critical. I added CRITICAL by mistake.
fix parsing of higher-order formulas;
this code was never exercised before because the current ATPs perform clausification, but someday ATPs might support FOF natively