the current solver when encountering ambiguity during proving should consider reproving if progress has been made