P
rop
R
es
P
I
Propositional_Resolution
Prime_Implicates