Add subsumption rule in the preliminary steps

Now resolution_rule takes almost 1/3 of the time less