Revised some functions in order to allow an axiom to include equality literals.