PLAYERS 1, 2
REL Win1() = ex x0, x1 (
 (tc !4 x0, x1 ((Q(x0) and Q(x1) and C(x0, x1)))) or
 (tc !4 x0, x1 ((Q(x0) and Q(x1) and Da(x0, x1)))) or
 (tc !4 x0, x1 ((Q(x0) and Q(x1) and Db(x0, x1)))) or
 (tc !4 x0, x1 ((Q(x0) and Q(x1) and R(x0, x1)))) )
REL Win2() = ex x0, x1 (
 (tc !4 x0, x1 ((P(x0) and P(x1) and C(x0, x1)))) or
 (tc !4 x0, x1 ((P(x0) and P(x1) and Da(x0, x1)))) or
 (tc !4 x0, x1 ((P(x0) and P(x1) and Db(x0, x1)))) or
 (tc !4 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 (true) 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 (true) 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, h1, a2, b2, c2, d2, e2, f2, g2, h2, a3, b3, c3, d3, e3, f3, g3, h3, a4, b4, c4, d4, e4, f4, g4, h4, a5, b5, c5, d5, e5, f5, g5, h5, a6, b6, c6, d6, e6, f6, g6, h6, a7, b7, c7, d7, e7, f7, g7, h7, a8, b8, c8, d8, e8, f8, g8, h8 | Da {(a1, b2); (b1, c2); (c1, d2); (d1, e2); (e1, f2); (f1, g2); (g1, h2); (a2, b3); (b2, c3); (c2, d3); (d2, e3); (e2, f3); (f2, g3); (g2, h3); (a3, b4); (b3, c4); (c3, d4); (d3, e4); (e3, f4); (f3, g4); (g3, h4); (a4, b5); (b4, c5); (c4, d5); (d4, e5); (e4, f5); (f4, g5); (g4, h5); (a5, b6); (b5, c6); (c5, d6); (d5, e6); (e5, f6); (f5, g6); (g5, h6); (a6, b7); (b6, c7); (c6, d7); (d6, e7); (e6, f7); (f6, g7); (g6, h7); (a7, b8); (b7, c8); (c7, d8); (d7, e8); (e7, f8); (f7, g8); (g7, h8)}; Db {(b1, a2); (c1, b2); (d1, c2); (e1, d2); (f1, e2); (g1, f2); (h1, g2); (b2, a3); (c2, b3); (d2, c3); (e2, d3); (f2, e3); (g2, f3); (h2, g3); (b3, a4); (c3, b4); (d3, c4); (e3, d4); (f3, e4); (g3, f4); (h3, g4); (b4, a5); (c4, b5); (d4, c5); (e4, d5); (f4, e5); (g4, f5); (h4, g5); (b5, a6); (c5, b6); (d5, c6); (e5, d6); (f5, e6); (g5, f6); (h5, g6); (b6, a7); (c6, b7); (d6, c7); (e6, d7); (f6, e7); (g6, f7); (h6, g7); (b7, a8); (c7, b8); (d7, c8); (e7, d8); (f7, e8); (g7, f8); (h7, g8)}; P:1 {}; Q:1 {} | ] "
	   ...   ...   ...   ...
	   ...   ...   ...   ...
	...   ...   ...   ...   
	...   ...   ...   ...   
	   ...   ...   ...   ...
	   ...   ...   ...   ...
	...   ...   ...   ...   
	...   ...   ...   ...   
	   ...   ...   ...   ...
	   ...   ...   ...   ...
	...   ...   ...   ...   
	...   ...   ...   ...   
	   ...   ...   ...   ...
	   ...   ...   ...   ...
	...   ...   ...   ...   
	...   ...   ...   ...   
"