refutes(proof1, raining).
method(proof1, contrapositive).
reason(proof1, "if rain implies wet ground and the ground is not wet, then it is not raining").