Big difference with Mace4

Stream: Equational

[Jose Brox]

Just to report that I'm experimenting a bit with the Mace4 selection options, and they produce big differences in performance. As a benchmark, I'm using the candidates to right division in groups that @Bruno Le Floch has generated, trying to prove that they don't imply
$(xz)(yz) = xy$.
His 7th candidate was solved by Vampire-SAT in less than a second, but Mace4 run for more than 5500s without finding a countermodel. This is with the selection options that come as default in the Windows GUI, which are selection_order 2 and selection_measure 4. Looking at the Mace4 manual, it makes more sense to me to choose selection_measure 3: "Select the candidate that would cause the greatest number of contradictions; for each cell being considered, all assignments and subsequent propagations are done (and undone), and the number of assignments that lead directly to contradictions are counted; this is an expensive lookahead operation with the motivation of cutting off paths as soon as possible."

With this option, Mace4 finds a contradiction in 1s and exhausts all models of size 7 in 3s. Similarly, huge time improvements are found with the other slow candidates too (another one that needed 1485s for one model, is now solved in 2s and exhausted in 109s).