Fix test_predtest's idea of what weak refutation means.

I'd initially supposed that predicate_refuted_by(..., true) ought to
say that "A refutes B" means "non-falsity of A implies non-truth of B".
But it seems better to define it as "truth of A implies non-truth of B".
This is more useful in the current system, slightly easier to prove,
and in closer correspondence to the existing code behavior.

With this change, test_predtest no longer claims that any existing
test cases show false proof reports, though there still are cases
where we could prove something and fail to.

Discussion: https://postgr.es/m/[email protected]

0 files changed, 0 insertions, 0 deletions