It appears that we need to set very_verbose to get the prover to output
clauses generated by factorisation, etc. Without this, we get only 5 clauses
from LCL403 instead of the nearly 30,000 expected.
Playing with the dumps from SET012, it becomes apparent that using clustered subgraphs may be useful. When a large inter-rank gap is used with clustered subgraphs for iterations, the resultant plot is almost understandable. Further experiments to try include:
creating edges between a given clause and its cluster of children (rather than a given clause and every child);
collapsing nodes introduced by ‘factor’ into their parents; and
correctly ordering the iteration clusters with respect to each other.
Creating “given” edges to clusters (instead of to all children) appears to be of some value. Perhaps it might be interesting to represent this differently in an animation: e.g. highlighting the current “given clause” during those frames that comprise an iteration.