Seems specific to the Open rule. When SuSLik succeeds on one branch (and adds the trace of this branch), the other branch (assuming the branch number is 2) is to be added to Worklist. However, it is possible that other expansion is successful, then makes the Open.0 a ghost node.