Subsumption equality resolution

[mezpusz]

Adds the new inference subsumption equality resolution that is similar in spirit to subsumption resolution and is based on equality resolution rather than resolution. The inference is behind a (default false) flag so it shouldn't cause much trouble now.

Some figures over FOL benchmarks when it's enabled:

Discount:
run 0 unsat: 9208 (5) sat: 1042 (0) cputime: 56575.07 s instructions: 222740733 Mi memory: 1461763.85 MB
run 1 unsat: 9215 (12) sat: 1042 (0) cputime: 57393.50 s instructions: 222608978 Mi memory: 1459148.81 MB

Otter:
run 0 unsat: 9322 (7) sat: 1025 (0) cputime: 61514.09 s instructions: 222752334 Mi memory: 1694391.73 MB
run 1 unsat: 9327 (12) sat: 1025 (0) cputime: 62363.23 s instructions: 222637658 Mi memory: 1691635.40 MB

[MichaelRawson]

Good idea! Could we also look at any/every other generating inference in a similar light?

One thought: if we do enable this by default, I think it subsumes trivial literal removal.

[mezpusz]

Good idea! Could we also look at any/every other generating inference in a similar light?

I'm afraid the standard inferences are done ((subsumption) demodulation for superpositions, subsumption resolution and this for resolutions), but we could go crazy and implement URResolution or something from ALASCA maybe?

One thought: if we do enable this by default, I think it subsumes trivial literal removal.

Yes. But depending on the order of simplifications, we might get a slowdown (trivial literal removal is much faster and can be applied up front)?

[quickbeam123]

@mezpusz , could you please also create an entry for this in the sampler files?

[mezpusz]

@mezpusz , could you please also create an entry for this in the sampler files?

Sure, I set the ratio now to 9 off / 1 on. Do you think it's okay now?

[MichaelRawson]

the standard inferences are done

True, I was thinking about the less-standard. I don't want to duplicate every inference to have a subsuming version, so I had two things in mind:

1. When performing any generating inference and the conclusion subsumes (any of) the parents, delete the parent. But perhaps this is just backward subsumption with extra steps.
2. Do generating inferences as a final ultra-expensive simplification to see if any conclusion simplifies the parent. But I think this is (1) in disguise.

Not one of my better thoughts. Happy to go!

[mezpusz]

I think (1) would be reasonable, and there is already some logic with the generateSimplify that returns also a premiseRedundant bool. But AFAIK only some ALASCA inferences implement this fully, and not sure how it would look like with the general "perform inferences as usual but at the end try to subsume" logic.

It could be also strengthened by stopping all further inferences when we find redundancy and only adding the premises that actually make the clause redundant.