(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.