The idea is to change the pairing so that it is better when only axioms
change. In the extreme case, the goal is unchanged.
The first idea is to add a separator when printing the shape so that goal
and hypothesis are separated.
When pairing shape, the first sorting is done only on goals. Then, we try
to add to the PQ all the elements that have the same goal shape. I say
that some goals that are very close would not be directly next to each
other with the current algorithm: we give them a chance to evaluate their
measure (lcp) before elements are withdrawn.
Then, we also tried to change lcp in case the goal is slightly changed but
an hypothesis is changed too. If the goal change slightly in the same way
for a lot of tasks, currently the (lcp Old New) value is always the same.
The idea is to transform the lcp into a lcp_list which compare the goal
like lcp and then compare each hypothesis like lcp. So, we hope that when
the goal differs the same for two New goals compared to one Old, the right
one will be taken because it differs the same way on the hypothesis.