Add PL-Resolution.
Add CNF.