Since the dimacs functor has an internal state (relating to the output
in iCNF format), it is desirable to have a generative functor, inc as
esomeone wants to output select parts of a problem to two distinct iCNF
files).
When adding clauses that conatins duplicates, the checking
of some proof would fail because there would sometime be multiple
littrals to resolve over. This fixes that problem.