A negated atom, in the sense of negation as failure, not logical negation.
That is, it is true if atom is not known/defined.
Constructs a formula that is true iff this formula and f are both true.
The underlying (positive) atom.
Constructs a clause that proves atoms when this formula is true.
Negates this literal.