Footnote
The primitive
notKnown
cannot currently be used in consequents. If permitted, it could be used to check that something has not been deduced to be true, yielding an error if it has.