PLAYERS 1, 2
REL Win1() = ex x0, x1 (
 (tc !3 x0, x1 ((Q(x0) and Q(x1) and C(x0, x1)))) or
 (tc !3 x0, x1 ((Q(x0) and Q(x1) and Da(x0, x1)))) or
 (tc !3 x0, x1 ((Q(x0) and Q(x1) and Db(x0, x1)))) or
 (tc !3 x0, x1 ((Q(x0) and Q(x1) and R(x0, x1)))) )
REL Win2() = ex x0, x1 (
 (tc !3 x0, x1 ((P(x0) and P(x1) and C(x0, x1)))) or
 (tc !3 x0, x1 ((P(x0) and P(x1) and Da(x0, x1)))) or
 (tc !3 x0, x1 ((P(x0) and P(x1) and Db(x0, x1)))) or
 (tc !3 x0, x1 ((P(x0) and P(x1) and R(x0, x1)))) )

RULE Mv1r0: 
[e1 | C:2 {}; Da:2 {}; Db:2 {}; P:1 {}; Q:1 {}; R:2 {} | ] -> [e1 | C:2 {}; Da:2 {}; Db:2 {}; P:1 {}; Q (e1); R:2 {} | ]
emb R,Q,P,Db,Da,C
pre (ex x1 (x1 = e1 and all x0 not C(x0, x1)) or
 ex x1 (P(x1) and ex x0 (C(x1, x0) and x0 = e1)) or
 ex x1 (Q(x1) and ex x0 (C(x1, x0) and x0 = e1))) and not Win2()


RULE Mv2r0: 
[e1 | C:2 {}; Da:2 {}; Db:2 {}; P:1 {}; Q:1 {}; R:2 {} | ] -> [e1 | C:2 {}; Da:2 {}; Db:2 {}; P (e1); Q:1 {}; R:2 {} | ]
emb R,Q,P,Db,Da,C
pre (ex x1 (x1 = e1 and all x0 not C(x0, x1)) or
 ex x1 (P(x1) and ex x0 (C(x1, x0) and x0 = e1)) or
 ex x1 (Q(x1) and ex x0 (C(x1, x0) and x0 = e1))) and not Win1()

LOC 0 { 
  PLAYER 1 { PAYOFF : (Win1()) - :(Win2())
             MOVES [Mv1r0 -> 1]}
  PLAYER 2 { PAYOFF : (Win2()) - :(Win1()) }
}
LOC 1 {
  PLAYER 1 { PAYOFF :(Win1()) - :(Win2()) }
  PLAYER 2 { PAYOFF :(Win2()) - :(Win1())
             MOVES [Mv2r0 -> 0]}
}
MODEL [a1, b1, c1, d1, e1, f1, g1, a2, b2, c2, d2, e2, f2, g2, a3, b3, c3, d3, e3, f3, g3, a4, b4, c4, d4, e4, f4, g4, a5, b5, c5, d5, e5, f5, g5, a6, b6, c6, d6, e6, f6, g6 | Da {(a1, b2); (b1, c2); (c1, d2); (d1, e2); (e1, f2); (f1, g2); (a2, b3); (b2, c3); (c2, d3); (d2, e3); (e2, f3); (f2, g3); (a3, b4); (b3, c4); (c3, d4); (d3, e4); (e3, f4); (f3, g4); (a4, b5); (b4, c5); (c4, d5); (d4, e5); (e4, f5); (f4, g5); (a5, b6); (b5, c6); (c5, d6); (d5, e6); (e5, f6); (f5, g6)}; Db {(b1, a2); (c1, b2); (d1, c2); (e1, d2); (f1, e2); (g1, f2); (b2, a3); (c2, b3); (d2, c3); (e2, d3); (f2, e3); (g2, f3); (b3, a4); (c3, b4); (d3, c4); (e3, d4); (f3, e4); (g3, f4); (b4, a5); (c4, b5); (d4, c5); (e4, d5); (f4, e5); (g4, f5); (b5, a6); (c5, b6); (d5, c6); (e5, d6); (f5, e6); (g5, f6)}; P:1 {}; Q:1 {} | ] "
	                     
	.  .  .  .  .  .  .  
	                     
	.  .  .  .  .  .  .  
	                     
	.  .  .  .  .  .  .  
	                     
	.  .  .  .  .  .  .  
	                     
	.  .  .  .  .  .  .  
	                     
	.  .  .  .  .  .  .  
"