PLAYERS 1, 2 REL Win1() = ex x1 (W(x1) and all x0 not C(x1, x0)) REL Win2() = ex x1 (B(x1) and all x0 not C(x0, x1)) RULE Mv1r0: [e1, e2 | B:1 {}; C:2 {}; Da:2 {}; Db (e1, e2); R:2 {}; W (e1) | ] -> [e1, e2 | B:1 {}; C:2 {}; Da:2 {}; Db (e1, e2); R:2 {}; W (e2) | ] emb W,R,Db,Da,C,B pre (true) and not Win2() RULE Mv1r1: [e1, e2 | B:1 {}; C:2 {}; Da (e1, e2); Db:2 {}; R:2 {}; W (e1) | ] -> [e1, e2 | B:1 {}; C:2 {}; Da (e1, e2); Db:2 {}; R:2 {}; W (e2) | ] emb W,R,Db,Da,C,B pre (true) and not Win2() RULE Mv1r2: [e1, e2 | B:1 {}; C (e1, e2); Da:2 {}; Db:2 {}; R:2 {}; W (e1) | ] -> [e1, e2 | B:1 {}; C (e1, e2); Da:2 {}; Db:2 {}; R:2 {}; W (e2) | ] emb W,R,Db,Da,C,B pre (true) and not Win2() RULE Mv1r3: [e1, e2 | B (e2); C:2 {}; Da:2 {}; Db (e1, e2); R:2 {}; W (e1) | ] -> [e1, e2 | B:1 {}; C:2 {}; Da:2 {}; Db (e1, e2); R:2 {}; W (e2) | ] emb W,R,Db,Da,C,B pre (true) and not Win2() RULE Mv1r4: [e1, e2 | B (e2); C:2 {}; Da (e1, e2); Db:2 {}; R:2 {}; W (e1) | ] -> [e1, e2 | B:1 {}; C:2 {}; Da (e1, e2); Db:2 {}; R:2 {}; W (e2) | ] emb W,R,Db,Da,C,B pre (true) and not Win2() RULE Mv2r0: [e1, e2 | B (e2); C:2 {}; Da:2 {}; Db (e1, e2); R:2 {}; W:1 {} | ] -> [e1, e2 | B (e1); C:2 {}; Da:2 {}; Db (e1, e2); R:2 {}; W:1 {} | ] emb W,R,Db,Da,C,B pre (true) and not Win1() RULE Mv2r1: [e1, e2 | B (e2); C:2 {}; Da:2 {}; Db (e1, e2); R:2 {}; W (e1) | ] -> [e1, e2 | B (e1); C:2 {}; Da:2 {}; Db (e1, e2); R:2 {}; W:1 {} | ] emb W,R,Db,Da,C,B pre (true) and not Win1() RULE Mv2r2: [e1, e2 | B (e2); C:2 {}; Da (e1, e2); Db:2 {}; R:2 {}; W:1 {} | ] -> [e1, e2 | B (e1); C:2 {}; Da (e1, e2); Db:2 {}; R:2 {}; W:1 {} | ] emb W,R,Db,Da,C,B pre (true) and not Win1() RULE Mv2r3: [e1, e2 | B (e2); C:2 {}; Da (e1, e2); Db:2 {}; R:2 {}; W (e1) | ] -> [e1, e2 | B (e1); C:2 {}; Da (e1, e2); Db:2 {}; R:2 {}; W:1 {} | ] emb W,R,Db,Da,C,B pre (true) and not Win1() RULE Mv2r4: [e1, e2 | B (e2); C (e1, e2); Da:2 {}; Db:2 {}; R:2 {}; W:1 {} | ] -> [e1, e2 | B (e1); C (e1, e2); Da:2 {}; Db:2 {}; R:2 {}; W:1 {} | ] emb W,R,Db,Da,C,B pre (true) and not Win1() LOC 0 { PLAYER 1 { PAYOFF : (Win1()) - :(Win2()) MOVES [Mv1r0 -> 1]; [Mv1r1 -> 1]; [Mv1r2 -> 1]; [Mv1r3 -> 1]; [Mv1r4 -> 1]} PLAYER 2 { PAYOFF : (Win2()) - :(Win1()) } } LOC 1 { PLAYER 1 { PAYOFF :(Win1()) - :(Win2()) } PLAYER 2 { PAYOFF :(Win2()) - :(Win1()) MOVES [Mv2r0 -> 0]; [Mv2r1 -> 0]; [Mv2r2 -> 0]; [Mv2r3 -> 0]; [Mv2r4 -> 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)} | ] " ... ... ... ... B B..B B..B B..B B.. ... ... ... ... B..B B..B B..B B..B ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... W W..W W..W W..W W.. ... ... ... ... W..W W..W W..W W..W "