Fix test_predtest's idea of what weak refutation means.

 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/5983.1520487191@sss.pgh.pa.us