PLAYERS 1, 2
REL Win1() = ex x0, x1 (
 (tc !2 x0, x1 ((Q(x0) and Q(x1) and C(x0, x1)))) or
 (tc !2 x0, x1 ((Q(x0) and Q(x1) and Da(x0, x1)))) or
 (tc !2 x0, x1 ((Q(x0) and Q(x1) and Db(x0, x1)))) or
 (tc !2 x0, x1 ((Q(x0) and Q(x1) and R(x0, x1)))) )
REL Win2() = ex x0, x1 (
 (tc !2 x0, x1 ((P(x0) and P(x1) and C(x0, x1)))) or
 (tc !2 x0, x1 ((P(x0) and P(x1) and Da(x0, x1)))) or
 (tc !2 x0, x1 ((P(x0) and P(x1) and Db(x0, x1)))) or
 (tc !2 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, a2, b2, c2, a3, b3, c3 | Da {(a1, b2); (b1, c2); (a2, b3); (b2, c3)}; Db {(b1, a2); (c1, b2); (b2, a3); (c2, b3)}; P:1 {}; Q:1 {} | ] "
	         
	.  .  .  
	         
	.  .  .  
	         
	.  .  .  
"