make that three conjectures

I'm beginning to wonder if it is the case that for every winning E-strategy s there is an expansion s' of s such that s' is a winning D-strategy. The example I'm doing is:

(not (not (implies (implies (implies a b) c) (implies (implies (implies b a) c) c))))

i.e.,

¬¬(((A → B) → C) → (((B → A) → C) → C))

And if I start off by following the E-strategy we found last week for this formula, I can extend the left-most branch and then close it, but once I get into the middle branch, I'm finding I'm getting into what appears to be a cycle; I'm running out of options which don't provide branching for O, so the width of the tree keeps getting bigger and bigger and bigger.

Of course, maybe I haven't figured out the right algorithm for closing the branches. But I spent a lot of yesterday afternoon, and a good portion of this morning, working on it, and I'm getting into the same rut every single time. This makes me worried.

ETA: I was wrong! (Thank goodness). After at one point exploring the tree down to depth 46 and width I-have-no-idea), I started from scratch for yet another time, and finally found a winning D-strat that extends the E-strat (but only at the leaves, so this may not in fact be a winning D-strat; that's to test next). Unfortunately, the strat is too wide to get a screen shot of and display here. However, I've saved the code and you can view it here.