Predicate elimination 2

[quickbeam123]

Implements (behind an option) an extension suggested by Andrei:

 "Also eliminate a predicate P occurring more than once in a clause, provided P never occurs"
" both positively and negatively in a single clause and the multi-occurrence clauses all sit"
" on one polarity side. Instead of pairwise resolvents, the replacement clauses are then all"
" the hyper-resolvents, each occurrence of a multi-occurrence clause being resolved against"
" its own (variable-disjoint) copy of a single-occurrence clause of the opposite polarity."

In addition, performance has been tuned and improved (also for the non-pelmo case).
(Sneakily, cl->maxVar no longer uses the expensive getUniquePersistentIterator which positively impacts other places too.)

[quickbeam123]

Discount (awr 10) runs limited at -i 10000 over TPTP CNF/FOF/TF0

Sort by SAT
1025 ['problemsSTD_predelOld_dis10_i10K.pkl']
1074 ['problemsSTD_predelOld_dis10_pel-on_i10K.pkl']
1074 ['problemsSTD_predelNew_dis10_pel-on_pelmo-off_i10K.pkl']
1122 ['problemsSTD_predelNew_dis10_pel-on_pelmo-on_i10K.pkl']
Sort by UNS
8406 ['problemsSTD_predelOld_dis10_i10K.pkl']
8567 ['problemsSTD_predelNew_dis10_pel-on_pelmo-on_i10K.pkl']
SEU235+2 1.0 ('uns', 0.191, 838, 2171)
SEU349+2 1.0 ('uns', 0.222, 853, 908)
SEU347+2 1.0 ('uns', 0.208, 800, 836)
8596 ['problemsSTD_predelOld_dis10_pel-on_i10K.pkl']
8596 ['problemsSTD_predelNew_dis10_pel-on_pelmo-off_i10K.pkl']
Total 1156 / 8865
Num only-by (UNS):
problemsSTD_predelOld_dis10_i10K.pkl 221
problemsSTD_predelNew_dis10_pel-on_pelmo-on_i10K.pkl 40
problemsSTD_predelOld_dis10_pel-on_i10K.pkl 0
problemsSTD_predelNew_dis10_pel-on_pelmo-off_i10K.pkl 0
Greedy cover (UNS):
# problemsSTD_predelOld_dis10_pel-on_i10K.pkl contributes 8596 total 8596
# problemsSTD_predelOld_dis10_i10K.pkl contributes 229 total 8406
# problemsSTD_predelNew_dis10_pel-on_pelmo-on_i10K.pkl contributes 40 total 8567
Total 8865