[proof-new] Adding MACRO_RESOLUTION rule and updating proof checker (#5612)

[proof-new] Adding MACRO_RESOLUTION rule and updating proof checker (#5612)

Previously CHAIN_RESOLUTION's definition and checker were not properly capturing its intended behavior as merely an n-ary RESOLUTION rule (i.e., no factoring nor reordering). A new rule, MACRO_RESOLUTION, now captures this behavior: it combines CHAIN_RESOLUTION, FACTORING, and REORDERING.

This commit also adds a proof checker for the new rule and updates the proof checker of CHAIN_RESOLUTION.