Abduction: graph_gg_parent_not_finished_updated

[yutakang]

Somehow we have to apply graph_gg_parent_not_finished_updated quite often every time we prove an or-node. https://github.com/data61/PSL/blob/f210799199d4603afb4f74b7d43084990141f0be/Abduction/Update_Abduction_Graph.ML#L168

And it is not enough to call graph_gg_parent_not_finished_updated once for each loop.

But why?

[yutakang]

Now we check completely_proved_wo_assuming_conjectures and still_need_proof by transforming graphs into trees.

So, this issue is not longer relevant to us.