In checkRuleEntailment(), the unfinished horn clause system, put in a monadic design for variable name freshness.