remember interesting facts proved by SMT

I believe this heuristic gets rid of abduce_instance_rule and the like.
removed Prover.guess_instances
minor debug message adjustment