Better strategy for applications of A2

[ceilican]

Is RedRec using a good greedy strategy?

An idea for a possibly better strategy: prioritize downward permutation of cuts whose pivots occur very often in the proof. This would increase the chance that A1' could be applied later.

[Jogo27]

A very simple strategy which could lead to consider more permutations is to apply A2 randomly. The probability could depend on the ratio m/h, where m is the number of previous execution for which no other rule than A2 have been applied and h is the height of the resulting proof.