A simpler case

Some amount of thought on the previous post made it clear to me that my example was way more complicated than it needs to be. The following formula should be IL valid and allows Opp to assert a conditional so that Pro can attack it:

(implies (implies (and p p) q) (implies (and p p) q))

Or, in readable fashion:

(((P ∧ P) → Q) → ((P ∧ P) → Q))

I'm hoping that this example is small enough that the dialogues website can compute both the D and E strategies for me.

---

ETA: This is still too complicated a formula for the site, so I calculated the D and E strategies by hand; they do differ, but only by the final two moves in two of the three branches [ETA, 23Jun: This is wrong; I did not finish filling out one of the branches]. I came up with a more interesting example:

(implies (implies (and p p) (implies p q)) (implies (and p p) (implies p q)))

Or, readable:

(((P ∧ P) → (P → Q) → ((P ∧ P) → (P → Q))

Here, not only does the game not immediately end when Pro asserts an atom (he does so in the attack on an implication, which means that Opp still has the possibility to defend), but the D and E strategies differ by the final four moves in two of the branches. If I can think of a way to nicely represent the trees in HTML, I'll try to post all four strategies here.