When the software can prove X, return True.
When the software can prove !X, return False.
When the software can't do either, return Sorry.
When the software can prove X, return True.
When the software can prove !X, return False.
When the software can't do either, return Sorry.