if no counter-example is found by the disprover, return a reasoner failure...

if no counter-example is found by the disprover, return a reasoner failure instead of modifying the proof tree (to act more like pp does)