better pp
union-find-"split" algorithm fixed

a good implementation of the split operation is still to be
found, this one is just more likely to be correct.
the reduction machine updates the subst only

because of an error (or optimization) a chunk of the stack
could have been just moved to the subst. Hence updating the subst
would update the stack too.

This is OK, but makes the interaction with UF and hashcons more complex
and less predictable.
convert_stacks updates the stack with the reducts (and tells UF)
trickier convert_stacks that always updates the comparands
compare_stacks goes rigth to left (for now)
ctx < subst -> we compare ctx first
better pp
avoid adding twice the same update
avoid proliferation of updates on the stack (still possible via append)
more compact report
[reduction.ml] avoid adding stupid constraint: u = u
better pp
fix logging
some facility to benchmark
better convplot