[mezpusz]

Another small improvement I had lying around.

Adds one more demodulation redundancy check option that squeezes a bit more out of encompassment demodulation. Namely, we can also demodulate one ordered equation with another if their LHSs are renamings of each other but they are incomparable (when normalized to the same variables). In this case we just break tie by looking at the clause number. This of course does not help too much, as there are usually not so many such equation pairs, so I hid it behind a new option for strategizing.

Also tightened the demodulation redundancy check code a bit.

Results:

DIscount FOL TPTP

run 0 unsat: 9292 (18) sat: 1044 (1) cputime: 60321.32 s instructions: 221610392 Mi memory: 1787763.52 MB
run 1 unsat: 9302 (28) sat: 1044 (1) cputime: 60225.97 s instructions: 221463251 Mi memory: 1782538.74 MB

Otter FOL TPTP

run 0 unsat: 9399 (26) sat: 1027 (0) cputime: 65487.18 s instructions: 221404490 Mi memory: 2023222.52 MB
run 1 unsat: 9395 (22) sat: 1027 (0) cputime: 65517.28 s instructions: 221489242 Mi memory: 2028634.55 MB

No change for HOL TPTP

[mezpusz]

If this gets merged, let's squash the commits by GitHub's "squash and merge".

[MichaelRawson]

Cool! I'm OK with the option, but this one seems like it "always makes sense" especially if we're paying for encompassment demodulation anyway - how would you feel about this being part of the regular encompassment implementation?

[mezpusz]

I wouldn't be against it, but the results suggest it's not a clear improvement, so I don't mind it being a non-default option if you don't mind having one more option. 🙂