Deduction propagation order for scaffold minimisation

[MatvV04]

Based on this answers.ewi post it would be nice to explore the following techniques to reduce number of proof stages in a trimmed proof:

• Set the DeductionPropagator priority of a marked deduction to High to make sure previously marked deductions get propagated first if possible, preventing unnecessary marking of unmarked deductions.
• Prevent duplicate inferences from being added to proof stages by maintaining a visited set in the explain_predicates function (could be a different issue)
• Implement an UnmarkedDeductionPropagator that, as opposed to the current DeductionPropagator, contains all unmarked deductions. This propagator would then be able to select unmarked deductions, which would directly result in a conflict. See the following example:
  State:
  x >= 1
  y >= 3, y <= 6

Unmarked deductions:
x >= 1 /\ y == 3 -> false
x >= 1 /\ y >= 1 -> false

In this case both unmarked deductions could unit propagate / detect conflict, but it would be unnecessary to use and mark the first deduction as the second deduction directly conflicts.