Proper.CNF
type
CNF
c
cnf
mergeCNFFormulas
naiveSAT