[Toss-devel-svn] SF.net SVN: toss:[1545] trunk/Toss/GGP
Status: Beta
Brought to you by:
lukaszkaiser
Menu
▾
▴
[Toss-devel-svn] SF.net SVN: toss:[1545] trunk/Toss/GGP
|
From: <luk...@us...> - 2011-08-27 09:44:54
|
Revision: 1545
http://toss.svn.sourceforge.net/toss/?rev=1545&view=rev
Author: lukstafi
Date: 2011-08-27 09:44:45 +0000 (Sat, 27 Aug 2011)
Log Message:
-----------
GDL translation fixing: also simplify precondition stored in data for move translation. GameSimpl: remove undefined relations (replace with Or []), process additional formulas (assuming they do not introduce additional simplification data). Connect4: preconditions have redundant parts but too difficult to simplify.
Modified Paths:
--------------
trunk/Toss/GGP/GameSimpl.ml
trunk/Toss/GGP/GameSimpl.mli
trunk/Toss/GGP/GameSimplTest.ml
trunk/Toss/GGP/TranslateGame.ml
trunk/Toss/GGP/TranslateGameTest.ml
Added Paths:
-----------
trunk/Toss/GGP/tests/connect4-raw.toss
trunk/Toss/GGP/tests/connect4-simpl.toss
Modified: trunk/Toss/GGP/GameSimpl.ml
===================================================================
--- trunk/Toss/GGP/GameSimpl.ml 2011-08-26 14:33:35 UTC (rev 1544)
+++ trunk/Toss/GGP/GameSimpl.ml 2011-08-27 09:44:45 UTC (rev 1545)
@@ -14,6 +14,11 @@
instead of [DiscreteRule.special_rel_of rel <> None]? (To protect
against GDL using identifiers starting with underscore.)
+ (0) Cleanup.
+
+ (0a) Replace relations missing from the structure and defined
+ relations list, with "false", i.e. [Or []].
+
(1) Reduce equivalent or complement relations.
(1a) If [introduce_complement] is on, for each (unary) predicate
@@ -145,7 +150,11 @@
module Tups = Structure.Tuples
-let simplify ?(keep_nonempty_predicates=true) (game, state) =
+let map_all_formulas f more_formulas game =
+ Aux.StrMap.map f more_formulas,
+ Arena.map_to_formulas f game
+
+let simplify ?(keep_nonempty_predicates=true) ~more_formulas (game, state) =
(* {{{ log entry *)
if !debug_level > 0 then (
Printf.printf "GameSimpl: defined_rels = %s\n%!"
@@ -165,13 +174,24 @@
(String.concat ", " (Aux.Strings.elements fluents))
);
(* }}} *)
+ (* 0 *)
+ let present_rel rel =
+ List.mem_assoc rel signat ||
+ List.mem_assoc rel game.Arena.defined_rels in
+ let remove_absent = FormulaOps.map_formula
+ {FormulaOps.identity_map with FormulaOps.map_Rel =
+ fun rel args ->
+ if present_rel rel then Formula.Rel (rel, args)
+ else Formula.Or []} in
+ let more_formulas, game =
+ map_all_formulas remove_absent more_formulas game in
(* 1 *)
let add_rel rel acc =
match rel with
| Rel (rel,_) -> Aux.Strings.add rel acc
| _ -> acc in
let used_rels =
- Arena.fold_over_formulas ~include_defined_rels:false
+ Arena.fold_over_formulas ~include_defined_rels:false (* FIXME: why? *)
(FormulaOps.fold_over_atoms add_rel)
game Aux.Strings.empty in
let complemented = ref [] in
@@ -314,8 +334,9 @@
if neg then Not (Rel (orig, args)) else Rel (orig, args)
else phi
| phi -> phi in
- let game =
- Arena.map_to_formulas (FormulaOps.map_to_atoms repl_equiv) game in
+ let more_formulas, game =
+ map_all_formulas (FormulaOps.map_to_atoms repl_equiv)
+ more_formulas game in
let state =
{state with Arena.struc = Structure.clear_rels struc removable} in
(* Also have to apply to LHS structures... Don't use
@@ -448,8 +469,9 @@
List.mem_assoc rel2 game.Arena.defined_rels) &&
included_in rel1 rel2
| _ -> false in
- let game =
- Arena.map_to_formulas (FormulaOps.remove_redundant ~implies) game in
+ let more_formulas, game =
+ map_all_formulas (FormulaOps.remove_redundant ~implies)
+ more_formulas game in
(* 3 *)
let intersect_rels struc grel rels =
@@ -647,8 +669,8 @@
let res = glue_phi (Formula.flatten_sort phi) in
if old_used_rels == !used_rels then res
else glue_fixpoint res in
- let game =
- Arena.map_to_formulas glue_fixpoint game in
+ let more_formulas, game =
+ map_all_formulas glue_fixpoint more_formulas game in
(* 3e *)
let more_data =
Aux.map_some (fun (crel, orig_rel) ->
@@ -885,4 +907,4 @@
Structure.add_rel_name rel arity struc) struc signat in
Structure.clear_rels struc clear_rel)
(game, state) in
- game, state
+ more_formulas, (game, state)
Modified: trunk/Toss/GGP/GameSimpl.mli
===================================================================
--- trunk/Toss/GGP/GameSimpl.mli 2011-08-26 14:33:35 UTC (rev 1544)
+++ trunk/Toss/GGP/GameSimpl.mli 2011-08-27 09:44:45 UTC (rev 1545)
@@ -12,4 +12,6 @@
val simplify :
?keep_nonempty_predicates:bool ->
- Arena.game * Arena.game_state -> Arena.game * Arena.game_state
+ more_formulas:Formula.formula Aux.StrMap.t ->
+ Arena.game * Arena.game_state ->
+ Formula.formula Aux.StrMap.t * (Arena.game * Arena.game_state)
Modified: trunk/Toss/GGP/GameSimplTest.ml
===================================================================
--- trunk/Toss/GGP/GameSimplTest.ml 2011-08-26 14:33:35 UTC (rev 1544)
+++ trunk/Toss/GGP/GameSimplTest.ml 2011-08-27 09:44:45 UTC (rev 1545)
@@ -13,7 +13,8 @@
"connect5" >::
(fun () ->
let connect5 = state_of_file "./GGP/tests/connect5-raw.toss" in
- let res = GameSimpl.simplify connect5 in
+ let _, res =
+ GameSimpl.simplify ~more_formulas:Aux.StrMap.empty connect5 in
let goal = state_of_file "./GGP/tests/connect5-simpl.toss" in
let resf = open_out "./GGP/tests/connect5-temp.toss" in
let res_str = Arena.state_str res in
@@ -30,7 +31,8 @@
"breakthrough" >::
(fun () ->
let breakthrough = state_of_file "./GGP/tests/breakthrough-raw.toss" in
- let res = GameSimpl.simplify breakthrough in
+ let _, res =
+ GameSimpl.simplify ~more_formulas:Aux.StrMap.empty breakthrough in
let goal = state_of_file "./GGP/tests/breakthrough-simpl.toss" in
let resf = open_out "./GGP/tests/breakthrough-temp.toss" in
let res_str = Arena.state_str res in
@@ -67,7 +69,8 @@
let game = state_of_file ("./GGP/tests/"^game_name^"-raw.toss") in
Printf.printf "\nINPUT:\n%s\n%!" (Arena.state_str game);
(* GameSimpl.debug_level := 5; *)
- let res = GameSimpl.simplify game in
+ let _, res =
+ GameSimpl.simplify ~more_formulas:Aux.StrMap.empty game in
let resf = open_out ("./GGP/tests/"^game_name^"-simpl.toss") in
let res_str = Arena.state_str res in
output_string resf res_str;
@@ -78,7 +81,8 @@
let a () =
GameSimpl.debug_level := 5;
let connect5 = state_of_file "./GGP/tests/connect5-raw.toss" in
- let res = GameSimpl.simplify connect5 in
+ let _, res =
+ GameSimpl.simplify ~more_formulas:Aux.StrMap.empty connect5 in
let goal = state_of_file "./GGP/tests/connect5-simpl.toss" in
let resf = open_out "./GGP/tests/connect5-temp.toss" in
let res_str = Arena.state_str res in
Modified: trunk/Toss/GGP/TranslateGame.ml
===================================================================
--- trunk/Toss/GGP/TranslateGame.ml 2011-08-26 14:33:35 UTC (rev 1544)
+++ trunk/Toss/GGP/TranslateGame.ml 2011-08-27 09:44:45 UTC (rev 1545)
@@ -1655,8 +1655,22 @@
);
(* }}} *)
let tossrule_data = Aux.strmap_of_assoc tossrule_data in
+ let tossrule_preconds =
+ Aux.StrMap.map (fun rdata->rdata.precond) tossrule_data in
let playing_as =
Aux.array_argfind (fun x -> x = playing_as) players in
+ (match !generate_test_case with
+ | None -> ()
+ | Some game_name ->
+ let file = open_out ("./GGP/tests/"^game_name^"-raw.toss") in
+ output_string file (Arena.state_str result);
+ flush file; close_out file);
+ let tossrule_preconds, result =
+ GameSimpl.simplify ~more_formulas:tossrule_preconds result in
+ let tossrule_data = Aux.StrMap.mapi
+ (fun rname rdata->
+ {rdata with precond = Aux.StrMap.find rname tossrule_preconds})
+ tossrule_data in
let gdl_translation = {
(* map between structure elements and their term representations;
the reverse direction is by using element names *)
@@ -1674,13 +1688,6 @@
(match !generate_test_case with
| None -> ()
| Some game_name ->
- let file = open_out ("./GGP/tests/"^game_name^"-raw.toss") in
- output_string file (Arena.state_str result);
- flush file; close_out file);
- let result = GameSimpl.simplify result in
- (match !generate_test_case with
- | None -> ()
- | Some game_name ->
let file = open_out ("./GGP/tests/"^game_name^"-simpl.toss") in
output_string file (Arena.state_str result);
flush file; close_out file);
Modified: trunk/Toss/GGP/TranslateGameTest.ml
===================================================================
--- trunk/Toss/GGP/TranslateGameTest.ml 2011-08-26 14:33:35 UTC (rev 1544)
+++ trunk/Toss/GGP/TranslateGameTest.ml 2011-08-27 09:44:45 UTC (rev 1545)
@@ -193,23 +193,18 @@
"connect4" >::
(fun () ->
- (* Although the translation works, its quality is not good
- enough to warrant testing. *)
- todo "implement handling defined relations first";
- (* TODO: finish adapting the test after game is
- cleanly translated. *)
game_test_case ~game_name:"connect4" ~player:"white"
~own_plnum:0 ~opponent_plnum:1
- ~loc0_rule_name:"drop_???_0"
+ ~loc0_rule_name:"drop_c11_noop"
~loc0_emb:[
- "cell_x_y__blank_", "cell_2_1_MV1";
- "control__blank_", "control_MV1"]
+ "cell_c11_h4__BLANK_", "cell_2_1__BLANK_";
+ "control__BLANK_", "control__BLANK_"]
~loc0_move:"(drop 2)" ~loc0_noop:"noop"
- ~loc1:1 ~loc1_rule_name:"drop_???_1"
+ ~loc1:1 ~loc1_rule_name:"noop_drop_c12"
~loc1_emb:[
- "cell_x_y__blank_", "cell_f_g_MV1";
- "control__blank_", "control_MV1"]
- ~loc1_noop:"noop" ~loc1_move:"(mark f g)"
+ "cell_c12_h6__BLANK_", "cell_2_1__BLANK_";
+ "control__BLANK_", "control__BLANK_"]
+ ~loc1_noop:"noop" ~loc1_move:"(drop 2)"
);
]
@@ -224,20 +219,18 @@
let a () =
- game_test_case ~game_name:"breakthrough" ~player:"white"
+ game_test_case ~game_name:"connect4" ~player:"white"
~own_plnum:0 ~opponent_plnum:1
- ~loc0_rule_name:"move_x2_y3_x3_y4_noop"
+ ~loc0_rule_name:"drop_c11_noop"
~loc0_emb:[
- "cellholds_x2_y3__BLANK_", "cellholds_2_2__BLANK_";
- "cellholds_x3_y4__BLANK_", "cellholds_1_3__BLANK_";
+ "cell_c11_h4__BLANK_", "cell_2_1__BLANK_";
"control__BLANK_", "control__BLANK_"]
- ~loc0_move:"(move 2 2 1 3)" ~loc0_noop:"noop" ~loc1:1
- ~loc1_rule_name:"noop_move_x7_y9_x8_y10"
+ ~loc0_move:"(drop 2)" ~loc0_noop:"noop"
+ ~loc1:1 ~loc1_rule_name:"noop_drop_c12"
~loc1_emb:[
- "cellholds_x7_y9__blank_", "cellholds_7_7__BLANK_";
- "cellholds_x8_y10__blank_", "cellholds_6_6__BLANK_";
+ "cell_c12_h6__BLANK_", "cell_2_1__BLANK_";
"control__BLANK_", "control__BLANK_"]
- ~loc1_noop:"noop" ~loc1_move:"(move 7 7 6 6)"
+ ~loc1_noop:"noop" ~loc1_move:"(drop 2)"
let a () =
@@ -275,9 +268,9 @@
let a () =
(* regenerate ~debug:false ~game_name:"tictactoe" ~player:"xplayer"; *)
(* regenerate ~debug:false ~game_name:"connect5" ~player:"x"; *)
- regenerate ~debug:false ~game_name:"breakthrough" ~player:"white";
+ (* regenerate ~debug:false ~game_name:"breakthrough" ~player:"white"; *)
(* regenerate ~debug:true ~game_name:"pawn_whopping" ~player:"x"; *)
- (* regen_with_debug ~game_name:"connect4" ~player:"white"; *)
+ regenerate ~debug:false ~game_name:"connect4" ~player:"white";
(* failwith "generated"; *)
()
Added: trunk/Toss/GGP/tests/connect4-raw.toss
===================================================================
--- trunk/Toss/GGP/tests/connect4-raw.toss (rev 0)
+++ trunk/Toss/GGP/tests/connect4-raw.toss 2011-08-27 09:44:45 UTC (rev 1545)
@@ -0,0 +1,3116 @@
+REL row__w() =
+ ex cell_x0_y4__BLANK_, cell_x1_y4__BLANK_, cell_x2_y4__BLANK_,
+ cell_x3_y4__BLANK_
+ (succ__cell_0__cell_0(cell_x0_y4__BLANK_, cell_x1_y4__BLANK_) and
+ succ__cell_0__cell_0(cell_x1_y4__BLANK_, cell_x2_y4__BLANK_) and
+ succ__cell_0__cell_0(cell_x2_y4__BLANK_, cell_x3_y4__BLANK_) and
+ EQ___cell_1__cell_1(cell_x0_y4__BLANK_, cell_x1_y4__BLANK_) and
+ EQ___cell_1__cell_1(cell_x0_y4__BLANK_, cell_x2_y4__BLANK_) and
+ EQ___cell_1__cell_1(cell_x0_y4__BLANK_, cell_x3_y4__BLANK_) and
+ EQ___cell_1__cell_1(cell_x1_y4__BLANK_, cell_x0_y4__BLANK_) and
+ EQ___cell_1__cell_1(cell_x1_y4__BLANK_, cell_x2_y4__BLANK_) and
+ EQ___cell_1__cell_1(cell_x1_y4__BLANK_, cell_x3_y4__BLANK_) and
+ EQ___cell_1__cell_1(cell_x2_y4__BLANK_, cell_x0_y4__BLANK_) and
+ EQ___cell_1__cell_1(cell_x2_y4__BLANK_, cell_x1_y4__BLANK_) and
+ EQ___cell_1__cell_1(cell_x2_y4__BLANK_, cell_x3_y4__BLANK_) and
+ EQ___cell_1__cell_1(cell_x3_y4__BLANK_, cell_x0_y4__BLANK_) and
+ EQ___cell_1__cell_1(cell_x3_y4__BLANK_, cell_x1_y4__BLANK_) and
+ EQ___cell_1__cell_1(cell_x3_y4__BLANK_, cell_x2_y4__BLANK_) and
+ cell_2w(cell_x0_y4__BLANK_) and
+ cell__BLANK___BLANK___BLANK_(cell_x0_y4__BLANK_) and
+ cell_2w(cell_x1_y4__BLANK_) and
+ cell__BLANK___BLANK___BLANK_(cell_x1_y4__BLANK_) and
+ cell_2w(cell_x2_y4__BLANK_) and
+ cell__BLANK___BLANK___BLANK_(cell_x2_y4__BLANK_) and
+ cell_2w(cell_x3_y4__BLANK_) and
+ cell__BLANK___BLANK___BLANK_(cell_x3_y4__BLANK_))
+REL row__r() =
+ ex cell_x0_y4__BLANK_, cell_x1_y4__BLANK_, cell_x2_y4__BLANK_,
+ cell_x3_y4__BLANK_
+ (succ__cell_0__cell_0(cell_x0_y4__BLANK_, cell_x1_y4__BLANK_) and
+ succ__cell_0__cell_0(cell_x1_y4__BLANK_, cell_x2_y4__BLANK_) and
+ succ__cell_0__cell_0(cell_x2_y4__BLANK_, cell_x3_y4__BLANK_) and
+ EQ___cell_1__cell_1(cell_x0_y4__BLANK_, cell_x1_y4__BLANK_) and
+ EQ___cell_1__cell_1(cell_x0_y4__BLANK_, cell_x2_y4__BLANK_) and
+ EQ___cell_1__cell_1(cell_x0_y4__BLANK_, cell_x3_y4__BLANK_) and
+ EQ___cell_1__cell_1(cell_x1_y4__BLANK_, cell_x0_y4__BLANK_) and
+ EQ___cell_1__cell_1(cell_x1_y4__BLANK_, cell_x2_y4__BLANK_) and
+ EQ___cell_1__cell_1(cell_x1_y4__BLANK_, cell_x3_y4__BLANK_) and
+ EQ___cell_1__cell_1(cell_x2_y4__BLANK_, cell_x0_y4__BLANK_) and
+ EQ___cell_1__cell_1(cell_x2_y4__BLANK_, cell_x1_y4__BLANK_) and
+ EQ___cell_1__cell_1(cell_x2_y4__BLANK_, cell_x3_y4__BLANK_) and
+ EQ___cell_1__cell_1(cell_x3_y4__BLANK_, cell_x0_y4__BLANK_) and
+ EQ___cell_1__cell_1(cell_x3_y4__BLANK_, cell_x1_y4__BLANK_) and
+ EQ___cell_1__cell_1(cell_x3_y4__BLANK_, cell_x2_y4__BLANK_) and
+ cell_2r(cell_x0_y4__BLANK_) and
+ cell__BLANK___BLANK___BLANK_(cell_x0_y4__BLANK_) and
+ cell_2r(cell_x1_y4__BLANK_) and
+ cell__BLANK___BLANK___BLANK_(cell_x1_y4__BLANK_) and
+ cell_2r(cell_x2_y4__BLANK_) and
+ cell__BLANK___BLANK___BLANK_(cell_x2_y4__BLANK_) and
+ cell_2r(cell_x3_y4__BLANK_) and
+ cell__BLANK___BLANK___BLANK_(cell_x3_y4__BLANK_))
+REL row__dirt() =
+ ex cell_x0_y4__BLANK_, cell_x1_y4__BLANK_, cell_x2_y4__BLANK_,
+ cell_x3_y4__BLANK_
+ (succ__cell_0__cell_0(cell_x0_y4__BLANK_, cell_x1_y4__BLANK_) and
+ succ__cell_0__cell_0(cell_x1_y4__BLANK_, cell_x2_y4__BLANK_) and
+ succ__cell_0__cell_0(cell_x2_y4__BLANK_, cell_x3_y4__BLANK_) and
+ EQ___cell_1__cell_1(cell_x0_y4__BLANK_, cell_x1_y4__BLANK_) and
+ EQ___cell_1__cell_1(cell_x0_y4__BLANK_, cell_x2_y4__BLANK_) and
+ EQ___cell_1__cell_1(cell_x0_y4__BLANK_, cell_x3_y4__BLANK_) and
+ EQ___cell_1__cell_1(cell_x1_y4__BLANK_, cell_x0_y4__BLANK_) and
+ EQ___cell_1__cell_1(cell_x1_y4__BLANK_, cell_x2_y4__BLANK_) and
+ EQ___cell_1__cell_1(cell_x1_y4__BLANK_, cell_x3_y4__BLANK_) and
+ EQ___cell_1__cell_1(cell_x2_y4__BLANK_, cell_x0_y4__BLANK_) and
+ EQ___cell_1__cell_1(cell_x2_y4__BLANK_, cell_x1_y4__BLANK_) and
+ EQ___cell_1__cell_1(cell_x2_y4__BLANK_, cell_x3_y4__BLANK_) and
+ EQ___cell_1__cell_1(cell_x3_y4__BLANK_, cell_x0_y4__BLANK_) and
+ EQ___cell_1__cell_1(cell_x3_y4__BLANK_, cell_x1_y4__BLANK_) and
+ EQ___cell_1__cell_1(cell_x3_y4__BLANK_, cell_x2_y4__BLANK_) and
+ cell_2dirt(cell_x0_y4__BLANK_) and
+ cell__BLANK___BLANK___BLANK_(cell_x0_y4__BLANK_) and
+ cell_2dirt(cell_x1_y4__BLANK_) and
+ cell__BLANK___BLANK___BLANK_(cell_x1_y4__BLANK_) and
+ cell_2dirt(cell_x2_y4__BLANK_) and
+ cell__BLANK___BLANK___BLANK_(cell_x2_y4__BLANK_) and
+ cell_2dirt(cell_x3_y4__BLANK_) and
+ cell__BLANK___BLANK___BLANK_(cell_x3_y4__BLANK_))
+REL row__b() =
+ ex cell_x0_y4__BLANK_, cell_x1_y4__BLANK_, cell_x2_y4__BLANK_,
+ cell_x3_y4__BLANK_
+ (succ__cell_0__cell_0(cell_x0_y4__BLANK_, cell_x1_y4__BLANK_) and
+ succ__cell_0__cell_0(cell_x1_y4__BLANK_, cell_x2_y4__BLANK_) and
+ succ__cell_0__cell_0(cell_x2_y4__BLANK_, cell_x3_y4__BLANK_) and
+ EQ___cell_1__cell_1(cell_x0_y4__BLANK_, cell_x1_y4__BLANK_) and
+ EQ___cell_1__cell_1(cell_x0_y4__BLANK_, cell_x2_y4__BLANK_) and
+ EQ___cell_1__cell_1(cell_x0_y4__BLANK_, cell_x3_y4__BLANK_) and
+ EQ___cell_1__cell_1(cell_x1_y4__BLANK_, cell_x0_y4__BLANK_) and
+ EQ___cell_1__cell_1(cell_x1_y4__BLANK_, cell_x2_y4__BLANK_) and
+ EQ___cell_1__cell_1(cell_x1_y4__BLANK_, cell_x3_y4__BLANK_) and
+ EQ___cell_1__cell_1(cell_x2_y4__BLANK_, cell_x0_y4__BLANK_) and
+ EQ___cell_1__cell_1(cell_x2_y4__BLANK_, cell_x1_y4__BLANK_) and
+ EQ___cell_1__cell_1(cell_x2_y4__BLANK_, cell_x3_y4__BLANK_) and
+ EQ___cell_1__cell_1(cell_x3_y4__BLANK_, cell_x0_y4__BLANK_) and
+ EQ___cell_1__cell_1(cell_x3_y4__BLANK_, cell_x1_y4__BLANK_) and
+ EQ___cell_1__cell_1(cell_x3_y4__BLANK_, cell_x2_y4__BLANK_) and
+ cell_2b(cell_x0_y4__BLANK_) and
+ cell__BLANK___BLANK___BLANK_(cell_x0_y4__BLANK_) and
+ cell_2b(cell_x1_y4__BLANK_) and
+ cell__BLANK___BLANK___BLANK_(cell_x1_y4__BLANK_) and
+ cell_2b(cell_x2_y4__BLANK_) and
+ cell__BLANK___BLANK___BLANK_(cell_x2_y4__BLANK_) and
+ cell_2b(cell_x3_y4__BLANK_) and
+ cell__BLANK___BLANK___BLANK_(cell_x3_y4__BLANK_))
+REL filled(v0) =
+ ex cell_c0_h0__BLANK_
+ (v0 = cell_c0_h0__BLANK_ and
+ true and
+ cell_2dirt(cell_c0_h0__BLANK_) and
+ cell__BLANK___BLANK___BLANK_(cell_c0_h0__BLANK_)) or
+ ex cell_c1_h1__BLANK_
+ (v0 = cell_c1_h1__BLANK_ and
+ true and
+ cell_2w(cell_c1_h1__BLANK_) and
+ cell__BLANK___BLANK___BLANK_(cell_c1_h1__BLANK_)) or
+ ex cell_c2_h2__BLANK_
+ (v0 = cell_c2_h2__BLANK_ and
+ true and
+ cell_2r(cell_c2_h2__BLANK_) and
+ cell__BLANK___BLANK___BLANK_(cell_c2_h2__BLANK_))
+REL empty(v0) =
+ ex cell_c_h__BLANK_
+ (v0 = cell_c_h__BLANK_ and
+ true and
+ cell_2b(cell_c_h__BLANK_) and
+ cell__BLANK___BLANK___BLANK_(cell_c_h__BLANK_))
+REL diag__w() =
+ ex cell_x5_y9__BLANK_, cell_x6_y10__BLANK_, cell_x7_y11__BLANK_,
+ cell_x8_y12__BLANK_
+ (succ__cell_0__cell_0(cell_x5_y9__BLANK_, cell_x6_y10__BLANK_) and
+ succ__cell_1__cell_1(cell_x5_y9__BLANK_, cell_x6_y10__BLANK_) and
+ succ__cell_0__cell_0(cell_x6_y10__BLANK_, cell_x7_y11__BLANK_) and
+ succ__cell_1__cell_1(cell_x6_y10__BLANK_, cell_x7_y11__BLANK_) and
+ succ__cell_0__cell_0(cell_x7_y11__BLANK_, cell_x8_y12__BLANK_) and
+ succ__cell_1__cell_1(cell_x7_y11__BLANK_, cell_x8_y12__BLANK_) and
+ cell_2w(cell_x5_y9__BLANK_) and
+ cell__BLANK___BLANK___BLANK_(cell_x5_y9__BLANK_) and
+ cell_2w(cell_x6_y10__BLANK_) and
+ cell__BLANK___BLANK___BLANK_(cell_x6_y10__BLANK_) and
+ cell_2w(cell_x7_y11__BLANK_) and
+ cell__BLANK___BLANK___BLANK_(cell_x7_y11__BLANK_) and
+ cell_2w(cell_x8_y12__BLANK_) and
+ cell__BLANK___BLANK___BLANK_(cell_x8_y12__BLANK_)) or
+ ex cell_x9_y13__BLANK_, cell_x10_y14__BLANK_, cell_x11_y15__BLANK_,
+ cell_x12_y16__BLANK_
+ (succ__cell_0__cell_0(cell_x9_y13__BLANK_, cell_x10_y14__BLANK_) and
+ succ__cell_1__cell_1(cell_x10_y14__BLANK_, cell_x9_y13__BLANK_) and
+ succ__cell_0__cell_0(cell_x10_y14__BLANK_, cell_x11_y15__BLANK_) and
+ succ__cell_1__cell_1(cell_x11_y15__BLANK_, cell_x10_y14__BLANK_) and
+ succ__cell_0__cell_0(cell_x11_y15__BLANK_, cell_x12_y16__BLANK_) and
+ succ__cell_1__cell_1(cell_x12_y16__BLANK_, cell_x11_y15__BLANK_) and
+ cell_2w(cell_x9_y13__BLANK_) and
+ cell__BLANK___BLANK___BLANK_(cell_x9_y13__BLANK_) and
+ cell_2w(cell_x10_y14__BLANK_) and
+ cell__BLANK___BLANK___BLANK_(cell_x10_y14__BLANK_) and
+ cell_2w(cell_x11_y15__BLANK_) and
+ cell__BLANK___BLANK___BLANK_(cell_x11_y15__BLANK_) and
+ cell_2w(cell_x12_y16__BLANK_) and
+ cell__BLANK___BLANK___BLANK_(cell_x12_y16__BLANK_))
+REL diag__r() =
+ ex cell_x5_y9__BLANK_, cell_x6_y10__BLANK_, cell_x7_y11__BLANK_,
+ cell_x8_y12__BLANK_
+ (succ__cell_0__cell_0(cell_x5_y9__BLANK_, cell_x6_y10__BLANK_) and
+ succ__cell_1__cell_1(cell_x5_y9__BLANK_, cell_x6_y10__BLANK_) and
+ succ__cell_0__cell_0(cell_x6_y10__BLANK_, cell_x7_y11__BLANK_) and
+ succ__cell_1__cell_1(cell_x6_y10__BLANK_, cell_x7_y11__BLANK_) and
+ succ__cell_0__cell_0(cell_x7_y11__BLANK_, cell_x8_y12__BLANK_) and
+ succ__cell_1__cell_1(cell_x7_y11__BLANK_, cell_x8_y12__BLANK_) and
+ cell_2r(cell_x5_y9__BLANK_) and
+ cell__BLANK___BLANK___BLANK_(cell_x5_y9__BLANK_) and
+ cell_2r(cell_x6_y10__BLANK_) and
+ cell__BLANK___BLANK___BLANK_(cell_x6_y10__BLANK_) and
+ cell_2r(cell_x7_y11__BLANK_) and
+ cell__BLANK___BLANK___BLANK_(cell_x7_y11__BLANK_) and
+ cell_2r(cell_x8_y12__BLANK_) and
+ cell__BLANK___BLANK___BLANK_(cell_x8_y12__BLANK_)) or
+ ex cell_x9_y13__BLANK_, cell_x10_y14__BLANK_, cell_x11_y15__BLANK_,
+ cell_x12_y16__BLANK_
+ (succ__cell_0__cell_0(cell_x9_y13__BLANK_, cell_x10_y14__BLANK_) and
+ succ__cell_1__cell_1(cell_x10_y14__BLANK_, cell_x9_y13__BLANK_) and
+ succ__cell_0__cell_0(cell_x10_y14__BLANK_, cell_x11_y15__BLANK_) and
+ succ__cell_1__cell_1(cell_x11_y15__BLANK_, cell_x10_y14__BLANK_) and
+ succ__cell_0__cell_0(cell_x11_y15__BLANK_, cell_x12_y16__BLANK_) and
+ succ__cell_1__cell_1(cell_x12_y16__BLANK_, cell_x11_y15__BLANK_) and
+ cell_2r(cell_x9_y13__BLANK_) and
+ cell__BLANK___BLANK___BLANK_(cell_x9_y13__BLANK_) and
+ cell_2r(cell_x10_y14__BLANK_) and
+ cell__BLANK___BLANK___BLANK_(cell_x10_y14__BLANK_) and
+ cell_2r(cell_x11_y15__BLANK_) and
+ cell__BLANK___BLANK___BLANK_(cell_x11_y15__BLANK_) and
+ cell_2r(cell_x12_y16__BLANK_) and
+ cell__BLANK___BLANK___BLANK_(cell_x12_y16__BLANK_))
+REL diag__dirt() =
+ ex cell_x5_y9__BLANK_, cell_x6_y10__BLANK_, cell_x7_y11__BLANK_,
+ cell_x8_y12__BLANK_
+ (succ__cell_0__cell_0(cell_x5_y9__BLANK_, cell_x6_y10__BLANK_) and
+ succ__cell_1__cell_1(cell_x5_y9__BLANK_, cell_x6_y10__BLANK_) and
+ succ__cell_0__cell_0(cell_x6_y10__BLANK_, cell_x7_y11__BLANK_) and
+ succ__cell_1__cell_1(cell_x6_y10__BLANK_, cell_x7_y11__BLANK_) and
+ succ__cell_0__cell_0(cell_x7_y11__BLANK_, cell_x8_y12__BLANK_) and
+ succ__cell_1__cell_1(cell_x7_y11__BLANK_, cell_x8_y12__BLANK_) and
+ cell_2dirt(cell_x5_y9__BLANK_) and
+ cell__BLANK___BLANK___BLANK_(cell_x5_y9__BLANK_) and
+ cell_2dirt(cell_x6_y10__BLANK_) and
+ cell__BLANK___BLANK___BLANK_(cell_x6_y10__BLANK_) and
+ cell_2dirt(cell_x7_y11__BLANK_) and
+ cell__BLANK___BLANK___BLANK_(cell_x7_y11__BLANK_) and
+ cell_2dirt(cell_x8_y12__BLANK_) and
+ cell__BLANK___BLANK___BLANK_(cell_x8_y12__BLANK_)) or
+ ex cell_x9_y13__BLANK_, cell_x10_y14__BLANK_, cell_x11_y15__BLANK_,
+ cell_x12_y16__BLANK_
+ (succ__cell_0__cell_0(cell_x9_y13__BLANK_, cell_x10_y14__BLANK_) and
+ succ__cell_1__cell_1(cell_x10_y14__BLANK_, cell_x9_y13__BLANK_) and
+ succ__cell_0__cell_0(cell_x10_y14__BLANK_, cell_x11_y15__BLANK_) and
+ succ__cell_1__cell_1(cell_x11_y15__BLANK_, cell_x10_y14__BLANK_) and
+ succ__cell_0__cell_0(cell_x11_y15__BLANK_, cell_x12_y16__BLANK_) and
+ succ__cell_1__cell_1(cell_x12_y16__BLANK_, cell_x11_y15__BLANK_) and
+ cell_2dirt(cell_x9_y13__BLANK_) and
+ cell__BLANK___BLANK___BLANK_(cell_x9_y13__BLANK_) and
+ cell_2dirt(cell_x10_y14__BLANK_) and
+ cell__BLANK___BLANK___BLANK_(cell_x10_y14__BLANK_) and
+ cell_2dirt(cell_x11_y15__BLANK_) and
+ cell__BLANK___BLANK___BLANK_(cell_x11_y15__BLANK_) and
+ cell_2dirt(cell_x12_y16__BLANK_) and
+ cell__BLANK___BLANK___BLANK_(cell_x12_y16__BLANK_))
+REL diag__b() =
+ ex cell_x5_y9__BLANK_, cell_x6_y10__BLANK_, cell_x7_y11__BLANK_,
+ cell_x8_y12__BLANK_
+ (succ__cell_0__cell_0(cell_x5_y9__BLANK_, cell_x6_y10__BLANK_) and
+ succ__cell_1__cell_1(cell_x5_y9__BLANK_, cell_x6_y10__BLANK_) and
+ succ__cell_0__cell_0(cell_x6_y10__BLANK_, cell_x7_y11__BLANK_) and
+ succ__cell_1__cell_1(cell_x6_y10__BLANK_, cell_x7_y11__BLANK_) and
+ succ__cell_0__cell_0(cell_x7_y11__BLANK_, cell_x8_y12__BLANK_) and
+ succ__cell_1__cell_1(cell_x7_y11__BLANK_, cell_x8_y12__BLANK_) and
+ cell_2b(cell_x5_y9__BLANK_) and
+ cell__BLANK___BLANK___BLANK_(cell_x5_y9__BLANK_) and
+ cell_2b(cell_x6_y10__BLANK_) and
+ cell__BLANK___BLANK___BLANK_(cell_x6_y10__BLANK_) and
+ cell_2b(cell_x7_y11__BLANK_) and
+ cell__BLANK___BLANK___BLANK_(cell_x7_y11__BLANK_) and
+ cell_2b(cell_x8_y12__BLANK_) and
+ cell__BLANK___BLANK___BLANK_(cell_x8_y12__BLANK_)) or
+ ex cell_x9_y13__BLANK_, cell_x10_y14__BLANK_, cell_x11_y15__BLANK_,
+ cell_x12_y16__BLANK_
+ (succ__cell_0__cell_0(cell_x9_y13__BLANK_, cell_x10_y14__BLANK_) and
+ succ__cell_1__cell_1(cell_x10_y14__BLANK_, cell_x9_y13__BLANK_) and
+ succ__cell_0__cell_0(cell_x10_y14__BLANK_, cell_x11_y15__BLANK_) and
+ succ__cell_1__cell_1(cell_x11_y15__BLANK_, cell_x10_y14__BLANK_) and
+ succ__cell_0__cell_0(cell_x11_y15__BLANK_, cell_x12_y16__BLANK_) and
+ succ__cell_1__cell_1(cell_x12_y16__BLANK_, cell_x11_y15__BLANK_) and
+ cell_2b(cell_x9_y13__BLANK_) and
+ cell__BLANK___BLANK___BLANK_(cell_x9_y13__BLANK_) and
+ cell_2b(cell_x10_y14__BLANK_) and
+ cell__BLANK___BLANK___BLANK_(cell_x10_y14__BLANK_) and
+ cell_2b(cell_x11_y15__BLANK_) and
+ cell__BLANK___BLANK___BLANK_(cell_x11_y15__BLANK_) and
+ cell_2b(cell_x12_y16__BLANK_) and
+ cell__BLANK___BLANK___BLANK_(cell_x12_y16__BLANK_))
+REL column__w() =
+ ex cell_x4_y5__BLANK_, cell_x4_y6__BLANK_, cell_x4_y7__BLANK_,
+ cell_x4_y8__BLANK_
+ (succ__cell_1__cell_1(cell_x4_y5__BLANK_, cell_x4_y6__BLANK_) and
+ succ__cell_1__cell_1(cell_x4_y6__BLANK_, cell_x4_y7__BLANK_) and
+ succ__cell_1__cell_1(cell_x4_y7__BLANK_, cell_x4_y8__BLANK_) and
+ EQ___cell_0__cell_0(cell_x4_y5__BLANK_, cell_x4_y6__BLANK_) and
+ EQ___cell_0__cell_0(cell_x4_y5__BLANK_, cell_x4_y7__BLANK_) and
+ EQ___cell_0__cell_0(cell_x4_y5__BLANK_, cell_x4_y8__BLANK_) and
+ EQ___cell_0__cell_0(cell_x4_y6__BLANK_, cell_x4_y5__BLANK_) and
+ EQ___cell_0__cell_0(cell_x4_y6__BLANK_, cell_x4_y7__BLANK_) and
+ EQ___cell_0__cell_0(cell_x4_y6__BLANK_, cell_x4_y8__BLANK_) and
+ EQ___cell_0__cell_0(cell_x4_y7__BLANK_, cell_x4_y5__BLANK_) and
+ EQ___cell_0__cell_0(cell_x4_y7__BLANK_, cell_x4_y6__BLANK_) and
+ EQ___cell_0__cell_0(cell_x4_y7__BLANK_, cell_x4_y8__BLANK_) and
+ EQ___cell_0__cell_0(cell_x4_y8__BLANK_, cell_x4_y5__BLANK_) and
+ EQ___cell_0__cell_0(cell_x4_y8__BLANK_, cell_x4_y6__BLANK_) and
+ EQ___cell_0__cell_0(cell_x4_y8__BLANK_, cell_x4_y7__BLANK_) and
+ cell_2w(cell_x4_y5__BLANK_) and
+ cell__BLANK___BLANK___BLANK_(cell_x4_y5__BLANK_) and
+ cell_2w(cell_x4_y6__BLANK_) and
+ cell__BLANK___BLANK___BLANK_(cell_x4_y6__BLANK_) and
+ cell_2w(cell_x4_y7__BLANK_) and
+ cell__BLANK___BLANK___BLANK_(cell_x4_y7__BLANK_) and
+ cell_2w(cell_x4_y8__BLANK_) and
+ cell__BLANK___BLANK___BLANK_(cell_x4_y8__BLANK_))
+REL column__r() =
+ ex cell_x4_y5__BLANK_, cell_x4_y6__BLANK_, cell_x4_y7__BLANK_,
+ cell_x4_y8__BLANK_
+ (succ__cell_1__cell_1(cell_x4_y5__BLANK_, cell_x4_y6__BLANK_) and
+ succ__cell_1__cell_1(cell_x4_y6__BLANK_, cell_x4_y7__BLANK_) and
+ succ__cell_1__cell_1(cell_x4_y7__BLANK_, cell_x4_y8__BLANK_) and
+ EQ___cell_0__cell_0(cell_x4_y5__BLANK_, cell_x4_y6__BLANK_) and
+ EQ___cell_0__cell_0(cell_x4_y5__BLANK_, cell_x4_y7__BLANK_) and
+ EQ___cell_0__cell_0(cell_x4_y5__BLANK_, cell_x4_y8__BLANK_) and
+ EQ___cell_0__cell_0(cell_x4_y6__BLANK_, cell_x4_y5__BLANK_) and
+ EQ___cell_0__cell_0(cell_x4_y6__BLANK_, cell_x4_y7__BLANK_) and
+ EQ___cell_0__cell_0(cell_x4_y6__BLANK_, cell_x4_y8__BLANK_) and
+ EQ___cell_0__cell_0(cell_x4_y7__BLANK_, cell_x4_y5__BLANK_) and
+ EQ___cell_0__cell_0(cell_x4_y7__BLANK_, cell_x4_y6__BLANK_) and
+ EQ___cell_0__cell_0(cell_x4_y7__BLANK_, cell_x4_y8__BLANK_) and
+ EQ___cell_0__cell_0(cell_x4_y8__BLANK_, cell_x4_y5__BLANK_) and
+ EQ___cell_0__cell_0(cell_x4_y8__BLANK_, cell_x4_y6__BLANK_) and
+ EQ___cell_0__cell_0(cell_x4_y8__BLANK_, cell_x4_y7__BLANK_) and
+ cell_2r(cell_x4_y5__BLANK_) and
+ cell__BLANK___BLANK___BLANK_(cell_x4_y5__BLANK_) and
+ cell_2r(cell_x4_y6__BLANK_) and
+ cell__BLANK___BLANK___BLANK_(cell_x4_y6__BLANK_) and
+ cell_2r(cell_x4_y7__BLANK_) and
+ cell__BLANK___BLANK___BLANK_(cell_x4_y7__BLANK_) and
+ cell_2r(cell_x4_y8__BLANK_) and
+ cell__BLANK___BLANK___BLANK_(cell_x4_y8__BLANK_))
+REL column__dirt() =
+ ex cell_x4_y5__BLANK_, cell_x4_y6__BLANK_, cell_x4_y7__BLANK_,
+ cell_x4_y8__BLANK_
+ (succ__cell_1__cell_1(cell_x4_y5__BLANK_, cell_x4_y6__BLANK_) and
+ succ__cell_1__cell_1(cell_x4_y6__BLANK_, cell_x4_y7__BLANK_) and
+ succ__cell_1__cell_1(cell_x4_y7__BLANK_, cell_x4_y8__BLANK_) and
+ EQ___cell_0__cell_0(cell_x4_y5__BLANK_, cell_x4_y6__BLANK_) and
+ EQ___cell_0__cell_0(cell_x4_y5__BLANK_, cell_x4_y7__BLANK_) and
+ EQ___cell_0__cell_0(cell_x4_y5__BLANK_, cell_x4_y8__BLANK_) and
+ EQ___cell_0__cell_0(cell_x4_y6__BLANK_, cell_x4_y5__BLANK_) and
+ EQ___cell_0__cell_0(cell_x4_y6__BLANK_, cell_x4_y7__BLANK_) and
+ EQ___cell_0__cell_0(cell_x4_y6__BLANK_, cell_x4_y8__BLANK_) and
+ EQ___cell_0__cell_0(cell_x4_y7__BLANK_, cell_x4_y5__BLANK_) and
+ EQ___cell_0__cell_0(cell_x4_y7__BLANK_, cell_x4_y6__BLANK_) and
+ EQ___cell_0__cell_0(cell_x4_y7__BLANK_, cell_x4_y8__BLANK_) and
+ EQ___cell_0__cell_0(cell_x4_y8__BLANK_, cell_x4_y5__BLANK_) and
+ EQ___cell_0__cell_0(cell_x4_y8__BLANK_, cell_x4_y6__BLANK_) and
+ EQ___cell_0__cell_0(cell_x4_y8__BLANK_, cell_x4_y7__BLANK_) and
+ cell_2dirt(cell_x4_y5__BLANK_) and
+ cell__BLANK___BLANK___BLANK_(cell_x4_y5__BLANK_) and
+ cell_2dirt(cell_x4_y6__BLANK_) and
+ cell__BLANK___BLANK___BLANK_(cell_x4_y6__BLANK_) and
+ cell_2dirt(cell_x4_y7__BLANK_) and
+ cell__BLANK___BLANK___BLANK_(cell_x4_y7__BLANK_) and
+ cell_2dirt(cell_x4_y8__BLANK_) and
+ cell__BLANK___BLANK___BLANK_(cell_x4_y8__BLANK_))
+REL column__b() =
+ ex cell_x4_y5__BLANK_, cell_x4_y6__BLANK_, cell_x4_y7__BLANK_,
+ cell_x4_y8__BLANK_
+ (succ__cell_1__cell_1(cell_x4_y5__BLANK_, cell_x4_y6__BLANK_) and
+ succ__cell_1__cell_1(cell_x4_y6__BLANK_, cell_x4_y7__BLANK_) and
+ succ__cell_1__cell_1(cell_x4_y7__BLANK_, cell_x4_y8__BLANK_) and
+ EQ___cell_0__cell_0(cell_x4_y5__BLANK_, cell_x4_y6__BLANK_) and
+ EQ___cell_0__cell_0(cell_x4_y5__BLANK_, cell_x4_y7__BLANK_) and
+ EQ___cell_0__cell_0(cell_x4_y5__BLANK_, cell_x4_y8__BLANK_) and
+ EQ___cell_0__cell_0(cell_x4_y6__BLANK_, cell_x4_y5__BLANK_) and
+ EQ___cell_0__cell_0(cell_x4_y6__BLANK_, cell_x4_y7__BLANK_) and
+ EQ___cell_0__cell_0(cell_x4_y6__BLANK_, cell_x4_y8__BLANK_) and
+ EQ___cell_0__cell_0(cell_x4_y7__BLANK_, cell_x4_y5__BLANK_) and
+ EQ___cell_0__cell_0(cell_x4_y7__BLANK_, cell_x4_y6__BLANK_) and
+ EQ___cell_0__cell_0(cell_x4_y7__BLANK_, cell_x4_y8__BLANK_) and
+ EQ___cell_0__cell_0(cell_x4_y8__BLANK_, cell_x4_y5__BLANK_) and
+ EQ___cell_0__cell_0(cell_x4_y8__BLANK_, cell_x4_y6__BLANK_) and
+ EQ___cell_0__cell_0(cell_x4_y8__BLANK_, cell_x4_y7__BLANK_) and
+ cell_2b(cell_x4_y5__BLANK_) and
+ cell__BLANK___BLANK___BLANK_(cell_x4_y5__BLANK_) and
+ cell_2b(cell_x4_y6__BLANK_) and
+ cell__BLANK___BLANK___BLANK_(cell_x4_y6__BLANK_) and
+ cell_2b(cell_x4_y7__BLANK_) and
+ cell__BLANK___BLANK___BLANK_(cell_x4_y7__BLANK_) and
+ cell_2b(cell_x4_y8__BLANK_) and
+ cell__BLANK___BLANK___BLANK_(cell_x4_y8__BLANK_))
+REL open() =
+ ex cell_c10_h7__BLANK_
+ (empty(cell_c10_h7__BLANK_) and
+ cell__BLANK___BLANK___BLANK_(cell_c10_h7__BLANK_))
+REL line__w() =
+ (row__w() and true) or (column__w() and true) or (diag__w() and true)
+REL line__r() =
+ (row__r() and true) or (column__r() and true) or (diag__r() and true)
+REL line__dirt() =
+ (row__dirt() and true) or (column__dirt() and true) or
+ (diag__dirt() and true)
+REL line__b() =
+ (row__b() and true) or (column__b() and true) or (diag__b() and true)
+REL terminal() =
+ (line__r() and true) or (line__w() and true) or (not open() and true)
+REL lte(v0, v1) =
+ ex cell_0__BLANK___BLANK_, cell_x16__BLANK___BLANK_
+ (v0 = cell_0__BLANK___BLANK_ and v1 = cell_x16__BLANK___BLANK_ and
+ number__cell_0(cell_x16__BLANK___BLANK_) and
+ cell__BLANK___BLANK___BLANK_(cell_x16__BLANK___BLANK_) and
+ cell_00(cell_0__BLANK___BLANK_) and
+ cell__BLANK___BLANK___BLANK_(cell_0__BLANK___BLANK_)) or
+ ex cell_x17__BLANK___BLANK_, cell_x17__BLANK___BLANK_
+ (v0 = cell_x17__BLANK___BLANK_ and v1 = cell_x17__BLANK___BLANK_ and
+ number__cell_0(cell_x17__BLANK___BLANK_) and
+ number__cell_0(cell_x17__BLANK___BLANK_) and
+ cell__BLANK___BLANK___BLANK_(cell_x17__BLANK___BLANK_) and
+ cell__BLANK___BLANK___BLANK_(cell_x17__BLANK___BLANK_)) or
+ ex cell_x18__BLANK___BLANK_, cell_z4__BLANK___BLANK_
+ (v0 = cell_x18__BLANK___BLANK_ and v1 = cell_z4__BLANK___BLANK_ and
+ ex cell_y21__BLANK___BLANK_
+ (succ__cell_0__cell_0(cell_y21__BLANK___BLANK_,
+ cell_z4__BLANK___BLANK_) and lte(cell_x18__BLANK___BLANK_,
+ cell_y21__BLANK___BLANK_) and
+ cell__BLANK___BLANK___BLANK_(cell_y21__BLANK___BLANK_) and
+ cell__BLANK___BLANK___BLANK_(cell_x18__BLANK___BLANK_) and
+ cell__BLANK___BLANK___BLANK_(cell_z4__BLANK___BLANK_) and
+ cell__BLANK___BLANK___BLANK_(cell_x18__BLANK___BLANK_))) or
+ ex cell_x19__BLANK___BLANK_, cell_y22__BLANK___BLANK_
+ (v0 = cell_x19__BLANK___BLANK_ and v1 = cell_y22__BLANK___BLANK_ and
+ succ__cell_0__cell_0(cell_x19__BLANK___BLANK_,
+ cell_y22__BLANK___BLANK_) and
+ cell__BLANK___BLANK___BLANK_(cell_y22__BLANK___BLANK_) and
+ cell__BLANK___BLANK___BLANK_(cell_x19__BLANK___BLANK_))
+PLAYERS white, red
+RULE drop_c11_noop:
+ [cell_c11_h4__BLANK_, control__BLANK_ |
+ _opt_cell_2b (control__BLANK_);
+ _opt_cell_2dirt {cell_c11_h4__BLANK_; control__BLANK_};
+ _opt_cell_2r {cell_c11_h4__BLANK_; control__BLANK_};
+ _opt_cell_2w {cell_c11_h4__BLANK_; control__BLANK_};
+ _opt_control_0red {cell_c11_h4__BLANK_; control__BLANK_};
+ _opt_control_0white (cell_c11_h4__BLANK_); cell_2b (cell_c11_h4__BLANK_);
+ cell__BLANK___BLANK___BLANK_ (cell_c11_h4__BLANK_);
+ control_0white (control__BLANK_); control__BLANK_ (control__BLANK_)
+ |
+ ] ->
+ [cell_c11_h4__BLANK_, control__BLANK_ |
+ cell_2w (cell_c11_h4__BLANK_); control_0red (control__BLANK_) |
+ ] emb cell_2b, cell_2dirt, cell_2r, cell_2w, control_0red, control_0white
+ pre
+ (not terminal() and
+ ex cell_c11_y17__BLANK_, cell_c11_h3__BLANK_, cell_c11_y18__BLANK_
+ (cell__BLANK___BLANK___BLANK_(cell_c11_h3__BLANK_) and
+ filled(cell_c11_h3__BLANK_) and
+ cell__BLANK___BLANK___BLANK_(cell_c11_y17__BLANK_) and
+ filled(cell_c11_y17__BLANK_) and cell_2b(cell_c11_y18__BLANK_) and
+ cell__BLANK___BLANK___BLANK_(cell_c11_y18__BLANK_) and
+ EQ___cell_0__cell_0(cell_c11_h3__BLANK_, cell_c11_h4__BLANK_) and
+ succ__cell_1__cell_1(cell_c11_h3__BLANK_, cell_c11_h4__BLANK_) and
+ EQ___cell_0__cell_0(cell_c11_h3__BLANK_, cell_c11_y17__BLANK_) and
+ EQ___cell_0__cell_0(cell_c11_h3__BLANK_, cell_c11_y18__BLANK_) and
+ EQ___cell_0__cell_0(cell_c11_h4__BLANK_, cell_c11_h3__BLANK_) and
+ EQ___cell_0__cell_0(cell_c11_h4__BLANK_, cell_c11_y17__BLANK_) and
+ EQ___cell_0__cell_0(cell_c11_h4__BLANK_, cell_c11_y18__BLANK_) and
+ EQ___cell_0__cell_0(cell_c11_y17__BLANK_, cell_c11_h3__BLANK_) and
+ EQ___cell_0__cell_0(cell_c11_y17__BLANK_, cell_c11_h4__BLANK_) and
+ EQ___cell_0__cell_0(cell_c11_y17__BLANK_, cell_c11_y18__BLANK_) and
+ succ__cell_1__cell_1(cell_c11_y17__BLANK_, cell_c11_y18__BLANK_) and
+ EQ___cell_0__cell_0(cell_c11_y18__BLANK_, cell_c11_h3__BLANK_) and
+ EQ___cell_0__cell_0(cell_c11_y18__BLANK_, cell_c11_h4__BLANK_) and
+ EQ___cell_0__cell_0(cell_c11_y18__BLANK_, cell_c11_y17__BLANK_)))
+RULE noop_drop_c12:
+ [cell_c12_h6__BLANK_, control__BLANK_ |
+ _opt_cell_2b (control__BLANK_);
+ _opt_cell_2dirt {cell_c12_h6__BLANK_; control__BLANK_};
+ _opt_cell_2r {cell_c12_h6__BLANK_; control__BLANK_};
+ _opt_cell_2w {cell_c12_h6__BLANK_; control__BLANK_};
+ _opt_control_0red (cell_c12_h6__BLANK_);
+ _opt_control_0white {cell_c12_h6__BLANK_; control__BLANK_};
+ cell_2b (cell_c12_h6__BLANK_);
+ cell__BLANK___BLANK___BLANK_ (cell_c12_h6__BLANK_);
+ control_0red (control__BLANK_); control__BLANK_ (control__BLANK_)
+ |
+ ] ->
+ [cell_c12_h6__BLANK_, control__BLANK_ |
+ cell_2r (cell_c12_h6__BLANK_); control_0white (control__BLANK_) |
+ ]
+ emb cell_2b, cell_2dirt, cell_2r, cell_2w, control_0red, control_0white
+ pre
+ (not terminal() and
+ ex cell_c12_y19__BLANK_, cell_c12_h5__BLANK_, cell_c12_y20__BLANK_
+ (cell__BLANK___BLANK___BLANK_(cell_c12_h5__BLANK_) and
+ filled(cell_c12_h5__BLANK_) and
+ cell__BLANK___BLANK___BLANK_(cell_c12_y19__BLANK_) and
+ filled(cell_c12_y19__BLANK_) and cell_2b(cell_c12_y20__BLANK_) and
+ cell__BLANK___BLANK___BLANK_(cell_c12_y20__BLANK_) and
+ EQ___cell_0__cell_0(cell_c12_h5__BLANK_, cell_c12_h6__BLANK_) and
+ succ__cell_1__cell_1(cell_c12_h5__BLANK_, cell_c12_h6__BLANK_) and
+ EQ___cell_0__cell_0(cell_c12_h5__BLANK_, cell_c12_y19__BLANK_) and
+ EQ___cell_0__cell_0(cell_c12_h5__BLANK_, cell_c12_y20__BLANK_) and
+ EQ___cell_0__cell_0(cell_c12_h6__BLANK_, cell_c12_h5__BLANK_) and
+ EQ___cell_0__cell_0(cell_c12_h6__BLANK_, cell_c12_y19__BLANK_) and
+ EQ___cell_0__cell_0(cell_c12_h6__BLANK_, cell_c12_y20__BLANK_) and
+ EQ___cell_0__cell_0(cell_c12_y19__BLANK_, cell_c12_h5__BLANK_) and
+ EQ___cell_0__cell_0(cell_c12_y19__BLANK_, cell_c12_h6__BLANK_) and
+ EQ___cell_0__cell_0(cell_c12_y19__BLANK_, cell_c12_y20__BLANK_) and
+ succ__cell_1__cell_1(cell_c12_y19__BLANK_, cell_c12_y20__BLANK_) and
+ EQ___cell_0__cell_0(cell_c12_y20__BLANK_, cell_c12_h5__BLANK_) and
+ EQ___cell_0__cell_0(cell_c12_y20__BLANK_, cell_c12_h6__BLANK_) and
+ EQ___cell_0__cell_0(cell_c12_y20__BLANK_, cell_c12_y19__BLANK_)))
+LOC 0 {
+
+ PLAYER white {
+ PAYOFF
+ 100. * :((line__w() and true)) +
+ 50. * :((not line__r() and not line__w() and not open() and true)) +
+ 70. * :((not line__r() and not line__w() and open() and true))
+ MOVES [drop_c11_noop -> 1] }
+ PLAYER red {
+ PAYOFF
+ 100. * :((line__r() and true)) +
+ 50. * :((not line__r() and not line__w() and not open() and true)) +
+ 70. * :((not line__r() and not line__w() and open() and true))
+ }
+}
+LOC 1 {
+
+ PLAYER white {
+ PAYOFF
+ 100. * :((line__w() and true)) +
+ 50. * :((not line__r() and not line__w() and not open() and true)) +
+ 70. * :((not line__r() and not line__w() and open() and true))
+ }
+ PLAYER red {
+ PAYOFF
+ 100. * :((line__r() and true)) +
+ 50. * :((not line__r() and not line__w() and not open() and true)) +
+ 70. * :((not line__r() and not line__w() and open() and true))
+ MOVES [noop_drop_c12 -> 0] }
+}
+MODEL
+ [cell_1_0__BLANK_, cell_1_1__BLANK_, cell_1_2__BLANK_, cell_1_3__BLANK_,
+ cell_1_4__BLANK_, cell_1_5__BLANK_, cell_1_6__BLANK_, cell_2_0__BLANK_,
+ cell_2_1__BLANK_, cell_2_2__BLANK_, cell_2_3__BLANK_, cell_2_4__BLANK_,
+ cell_2_5__BLANK_, cell_2_6__BLANK_, cell_3_0__BLANK_, cell_3_1__BLANK_,
+ cell_3_2__BLANK_, cell_3_3__BLANK_, cell_3_4__BLANK_, cell_3_5__BLANK_,
+ cell_3_6__BLANK_, cell_4_0__BLANK_, cell_4_1__BLANK_, cell_4_2__BLANK_,
+ cell_4_3__BLANK_, cell_4_4__BLANK_, cell_4_5__BLANK_, cell_4_6__BLANK_,
+ cell_5_0__BLANK_, cell_5_1__BLANK_, cell_5_2__BLANK_, cell_5_3__BLANK_,
+ cell_5_4__BLANK_, cell_5_5__BLANK_, cell_5_6__BLANK_, cell_6_0__BLANK_,
+ cell_6_1__BLANK_, cell_6_2__BLANK_, cell_6_3__BLANK_, cell_6_4__BLANK_,
+ cell_6_5__BLANK_, cell_6_6__BLANK_, cell_7_0__BLANK_, cell_7_1__BLANK_,
+ cell_7_2__BLANK_, cell_7_3__BLANK_, cell_7_4__BLANK_, cell_7_5__BLANK_,
+ cell_7_6__BLANK_, control__BLANK_ |
+ EQ___cell_0__cell_0 {
+ (cell_1_0__BLANK_, cell_1_0__BLANK_);
+ (cell_1_0__BLANK_, cell_1_1__BLANK_);
+ (cell_1_0__BLANK_, cell_1_2__BLANK_);
+ (cell_1_0__BLANK_, cell_1_3__BLANK_);
+ (cell_1_0__BLANK_, cell_1_4__BLANK_);
+ (cell_1_0__BLANK_, cell_1_5__BLANK_);
+ (cell_1_0__BLANK_, cell_1_6__BLANK_);
+ (cell_1_1__BLANK_, cell_1_0__BLANK_);
+ (cell_1_1__BLANK_, cell_1_1__BLANK_);
+ (cell_1_1__BLANK_, cell_1_2__BLANK_);
+ (cell_1_1__BLANK_, cell_1_3__BLANK_);
+ (cell_1_1__BLANK_, cell_1_4__BLANK_);
+ (cell_1_1__BLANK_, cell_1_5__BLANK_);
+ (cell_1_1__BLANK_, cell_1_6__BLANK_);
+ (cell_1_2__BLANK_, cell_1_0__BLANK_);
+ (cell_1_2__BLANK_, cell_1_1__BLANK_);
+ (cell_1_2__BLANK_, cell_1_2__BLANK_);
+ (cell_1_2__BLANK_, cell_1_3__BLANK_);
+ (cell_1_2__BLANK_, cell_1_4__BLANK_);
+ (cell_1_2__BLANK_, cell_1_5__BLANK_);
+ (cell_1_2__BLANK_, cell_1_6__BLANK_);
+ (cell_1_3__BLANK_, cell_1_0__BLANK_);
+ (cell_1_3__BLANK_, cell_1_1__BLANK_);
+ (cell_1_3__BLANK_, cell_1_2__BLANK_);
+ (cell_1_3__BLANK_, cell_1_3__BLANK_);
+ (cell_1_3__BLANK_, cell_1_4__BLANK_);
+ (cell_1_3__BLANK_, cell_1_5__BLANK_);
+ (cell_1_3__BLANK_, cell_1_6__BLANK_);
+ (cell_1_4__BLANK_, cell_1_0__BLANK_);
+ (cell_1_4__BLANK_, cell_1_1__BLANK_);
+ (cell_1_4__BLANK_, cell_1_2__BLANK_);
+ (cell_1_4__BLANK_, cell_1_3__BLANK_);
+ (cell_1_4__BLANK_, cell_1_4__BLANK_);
+ (cell_1_4__BLANK_, cell_1_5__BLANK_);
+ (cell_1_4__BLANK_, cell_1_6__BLANK_);
+ (cell_1_5__BLANK_, cell_1_0__BLANK_);
+ (cell_1_5__BLANK_, cell_1_1__BLANK_);
+ (cell_1_5__BLANK_, cell_1_2__BLANK_);
+ (cell_1_5__BLANK_, cell_1_3__BLANK_);
+ (cell_1_5__BLANK_, cell_1_4__BLANK_);
+ (cell_1_5__BLANK_, cell_1_5__BLANK_);
+ (cell_1_5__BLANK_, cell_1_6__BLANK_);
+ (cell_1_6__BLANK_, cell_1_0__BLANK_);
+ (cell_1_6__BLANK_, cell_1_1__BLANK_);
+ (cell_1_6__BLANK_, cell_1_2__BLANK_);
+ (cell_1_6__BLANK_, cell_1_3__BLANK_);
+ (cell_1_6__BLANK_, cell_1_4__BLANK_);
+ (cell_1_6__BLANK_, cell_1_5__BLANK_);
+ (cell_1_6__BLANK_, cell_1_6__BLANK_);
+ (cell_2_0__BLANK_, cell_2_0__BLANK_);
+ (cell_2_0__BLANK_, cell_2_1__BLANK_);
+ (cell_2_0__BLANK_, cell_2_2__BLANK_);
+ (cell_2_0__BLANK_, cell_2_3__BLANK_);
+ (cell_2_0__BLANK_, cell_2_4__BLANK_);
+ (cell_2_0__BLANK_, cell_2_5__BLANK_);
+ (cell_2_0__BLANK_, cell_2_6__BLANK_);
+ (cell_2_1__BLANK_, cell_2_0__BLANK_);
+ (cell_2_1__BLANK_, cell_2_1__BLANK_);
+ (cell_2_1__BLANK_, cell_2_2__BLANK_);
+ (cell_2_1__BLANK_, cell_2_3__BLANK_);
+ (cell_2_1__BLANK_, cell_2_4__BLANK_);
+ (cell_2_1__BLANK_, cell_2_5__BLANK_);
+ (cell_2_1__BLANK_, cell_2_6__BLANK_);
+ (cell_2_2__BLANK_, cell_2_0__BLANK_);
+ (cell_2_2__BLANK_, cell_2_1__BLANK_);
+ (cell_2_2__BLANK_, cell_2_2__BLANK_);
+ (cell_2_2__BLANK_, cell_2_3__BLANK_);
+ (cell_2_2__BLANK_, cell_2_4__BLANK_);
+ (cell_2_2__BLANK_, cell_2_5__BLANK_);
+ (cell_2_2__BLANK_, cell_2_6__BLANK_);
+ (cell_2_3__BLANK_, cell_2_0__BLANK_);
+ (cell_2_3__BLANK_, cell_2_1__BLANK_);
+ (cell_2_3__BLANK_, cell_2_2__BLANK_);
+ (cell_2_3__BLANK_, cell_2_3__BLANK_);
+ (cell_2_3__BLANK_, cell_2_4__BLANK_);
+ (cell_2_3__BLANK_, cell_2_5__BLANK_);
+ (cell_2_3__BLANK_, cell_2_6__BLANK_);
+ (cell_2_4__BLANK_, cell_2_0__BLANK_);
+ (cell_2_4__BLANK_, cell_2_1__BLANK_);
+ (cell_2_4__BLANK_, cell_2_2__BLANK_);
+ (cell_2_4__BLANK_, cell_2_3__BLANK_);
+ (cell_2_4__BLANK_, cell_2_4__BLANK_);
+ (cell_2_4__BLANK_, cell_2_5__BLANK_);
+ (cell_2_4__BLANK_, cell_2_6__BLANK_);
+ (cell_2_5__BLANK_, cell_2_0__BLANK_);
+ (cell_2_5__BLANK_, cell_2_1__BLANK_);
+ (cell_2_5__BLANK_, cell_2_2__BLANK_);
+ (cell_2_5__BLANK_, cell_2_3__BLANK_);
+ (cell_2_5__BLANK_, cell_2_4__BLANK_);
+ (cell_2_5__BLANK_, cell_2_5__BLANK_);
+ (cell_2_5__BLANK_, cell_2_6__BLANK_);
+ (cell_2_6__BLANK_, cell_2_0__BLANK_);
+ (cell_2_6__BLANK_, cell_2_1__BLANK_);
+ (cell_2_6__BLANK_, cell_2_2__BLANK_);
+ (cell_2_6__BLANK_, cell_2_3__BLANK_);
+ (cell_2_6__BLANK_, cell_2_4__BLANK_);
+ (cell_2_6__BLANK_, cell_2_5__BLANK_);
+ (cell_2_6__BLANK_, cell_2_6__BLANK_);
+ (cell_3_0__BLANK_, cell_3_0__BLANK_);
+ (cell_3_0__BLANK_, cell_3_1__BLANK_);
+ (cell_3_0__BLANK_, cell_3_2__BLANK_);
+ (cell_3_0__BLANK_, cell_3_3__BLANK_);
+ (cell_3_0__BLANK_, cell_3_4__BLANK_);
+ (cell_3_0__BLANK_, cell_3_5__BLANK_);
+ (cell_3_0__BLANK_, cell_3_6__BLANK_);
+ (cell_3_1__BLANK_, cell_3_0__BLANK_);
+ (cell_3_1__BLANK_, cell_3_1__BLANK_);
+ (cell_3_1__BLANK_, cell_3_2__BLANK_);
+ (cell_3_1__BLANK_, cell_3_3__BLANK_);
+ (cell_3_1__BLANK_, cell_3_4__BLANK_);
+ (cell_3_1__BLANK_, cell_3_5__BLANK_);
+ (cell_3_1__BLANK_, cell_3_6__BLANK_);
+ (cell_3_2__BLANK_, cell_3_0__BLANK_);
+ (cell_3_2__BLANK_, cell_3_1__BLANK_);
+ (cell_3_2__BLANK_, cell_3_2__BLANK_);
+ (cell_3_2__BLANK_, cell_3_3__BLANK_);
+ (cell_3_2__BLANK_, cell_3_4__BLANK_);
+ (cell_3_2__BLANK_, cell_3_5__BLANK_);
+ (cell_3_2__BLANK_, cell_3_6__BLANK_);
+ (cell_3_3__BLANK_, cell_3_0__BLANK_);
+ (cell_3_3__BLANK_, cell_3_1__BLANK_);
+ (cell_3_3__BLANK_, cell_3_2__BLANK_);
+ (cell_3_3__BLANK_, cell_3_3__BLANK_);
+ (cell_3_3__BLANK_, cell_3_4__BLANK_);
+ (cell_3_3__BLANK_, cell_3_5__BLANK_);
+ (cell_3_3__BLANK_, cell_3_6__BLANK_);
+ (cell_3_4__BLANK_, cell_3_0__BLANK_);
+ (cell_3_4__BLANK_, cell_3_1__BLANK_);
+ (cell_3_4__BLANK_, cell_3_2__BLANK_);
+ (cell_3_4__BLANK_, cell_3_3__BLANK_);
+ (cell_3_4__BLANK_, cell_3_4__BLANK_);
+ (cell_3_4__BLANK_, cell_3_5__BLANK_);
+ (cell_3_4__BLANK_, cell_3_6__BLANK_);
+ (cell_3_5__BLANK_, cell_3_0__BLANK_);
+ (cell_3_5__BLANK_, cell_3_1__BLANK_);
+ (cell_3_5__BLANK_, cell_3_2__BLANK_);
+ (cell_3_5__BLANK_, cell_3_3__BLANK_);
+ (cell_3_5__BLANK_, cell_3_4__BLANK_);
+ (cell_3_5__BLANK_, cell_3_5__BLANK_);
+ (cell_3_5__BLANK_, cell_3_6__BLANK_);
+ (cell_3_6__BLANK_, cell_3_0__BLANK_);
+ (cell_3_6__BLANK_, cell_3_1__BLANK_);
+ (cell_3_6__BLANK_, cell_3_2__BLANK_);
+ (cell_3_6__BLANK_, cell_3_3__BLANK_);
+ (cell_3_6__BLANK_, cell_3_4__BLANK_);
+ (cell_3_6__BLANK_, cell_3_5__BLANK_);
+ (cell_3_6__BLANK_, cell_3_6__BLANK_);
+ (cell_4_0__BLANK_, cell_4_0__BLANK_);
+ (cell_4_0__BLANK_, cell_4_1__BLANK_);
+ (cell_4_0__BLANK_, cell_4_2__BLANK_);
+ (cell_4_0__BLANK_, cell_4_3__BLANK_);
+ (cell_4_0__BLANK_, cell_4_4__BLANK_);
+ (cell_4_0__BLANK_, cell_4_5__BLANK_);
+ (cell_4_0__BLANK_, cell_4_6__BLANK_);
+ (cell_4_1__BLANK_, cell_4_0__BLANK_);
+ (cell_4_1__BLANK_, cell_4_1__BLANK_);
+ (cell_4_1__BLANK_, cell_4_2__BLANK_);
+ (cell_4_1__BLANK_, cell_4_3__BLANK_);
+ (cell_4_1__BLANK_, cell_4_4__BLANK_);
+ (cell_4_1__BLANK_, cell_4_5__BLANK_);
+ (cell_4_1__BLANK_, cell_4_6__BLANK_);
+ (cell_4_2__BLANK_, cell_4_0__BLANK_);
+ (cell_4_2__BLANK_, cell_4_1__BLANK_);
+ (cell_4_2__BLANK_, cell_4_2__BLANK_);
+ (cell_4_2__BLANK_, cell_4_3__BLANK_);
+ (cell_4_2__BLANK_, cell_4_4__BLANK_);
+ (cell_4_2__BLANK_, cell_4_5__BLANK_);
+ (cell_4_2__BLANK_, cell_4_6__BLANK_);
+ (cell_4_3__BLANK_, cell_4_0__BLANK_);
+ (cell_4_3__BLANK_, cell_4_1__BLANK_);
+ (cell_4_3__BLANK_, cell_4_2__BLANK_);
+ (cell_4_3__BLANK_, cell_4_3__BLANK_);
+ (cell_4_3__BLANK_, cell_4_4__BLANK_);
+ (cell_4_3__BLANK_, cell_4_5__BLANK_);
+ (cell_4_3__BLANK_, cell_4_6__BLANK_);
+ (cell_4_4__BLANK_, cell_4_0__BLANK_);
+ (cell_4_4__BLANK_, cell_4_1__BLANK_);
+ (cell_4_4__BLANK_, cell_4_2__BLANK_);
+ (cell_4_4__BLANK_, cell_4_3__BLANK_);
+ (cell_4_4__BLANK_, cell_4_4__BLANK_);
+ (cell_4_4__BLANK_, cell_4_5__BLANK_);
+ (cell_4_4__BLANK_, cell_4_6__BLANK_);
+ (cell_4_5__BLANK_, cell_4_0__BLANK_);
+ (cell_4_5__BLANK_, cell_4_1__BLANK_);
+ (cell_4_5__BLANK_, cell_4_2__BLANK_);
+ (cell_4_5__BLANK_, cell_4_3__BLANK_);
+ (cell_4_5__BLANK_, cell_4_4__BLANK_);
+ (cell_4_5__BLANK_, cell_4_5__BLANK_);
+ (cell_4_5__BLANK_, cell_4_6__BLANK_);
+ (cell_4_6__BLANK_, cell_4_0__BLANK_);
+ (cell_4_6__BLANK_, cell_4_1__BLANK_);
+ (cell_4_6__BLANK_, cell_4_2__BLANK_);
+ (cell_4_6__BLANK_, cell_4_3__BLANK_);
+ (cell_4_6__BLANK_, cell_4_4__BLANK_);
+ (cell_4_6__BLANK_, cell_4_5__BLANK_);
+ (cell_4_6__BLANK_, cell_4_6__BLANK_);
+ (cell_5_0__BLANK_, cell_5_0__BLANK_);
+ (cell_5_0__BLANK_, cell_5_1__BLANK_);
+ (cell_5_0__BLANK_, cell_5_2__BLANK_);
+ (cell_5_0__BLANK_, cell_5_3__BLANK_);
+ (cell_5_0__BLANK_, cell_5_4__BLANK_);
+ (cell_5_0__BLANK_, cell_5_5__BLANK_);
+ (cell_5_0__BLANK_, cell_5_6__BLANK_);
+ (cell_5_1__BLANK_, cell_5_0__BLANK_);
+ (cell_5_1__BLANK_, cell_5_1__BLANK_);
+ (cell_5_1__BLANK_, cell_5_2__BLANK_);
+ (cell_5_1__BLANK_, cell_5_3__BLANK_);
+ (cell_5_1__BLANK_, cell_5_4__BLANK_);
+ (cell_5_1__BLANK_, cell_5_5__BLANK_);
+ (cell_5_1__BLANK_, cell_5_6__BLANK_);
+ (cell_5_2__BLANK_, cell_5_0__BLANK_);
+ (cell_5_2__BLANK_, cell_5_1__BLANK_);
+ (cell_5_2__BLANK_, cell_5_2__BLANK_);
+ (cell_5_2__BLANK_, cell_5_3__BLANK_);
+ (cell_5_2__BLANK_, cell_5_4__BLANK_);
+ (cell_5_2__BLANK_, cell_5_5__BLANK_);
+ (cell_5_2__BLANK_, cell_5_6__BLANK_);
+ (cell_5_3__BLANK_, cell_5_0__BLANK_);
+ (cell_5_3__BLANK_, cell_5_1__BLANK_);
+ (cell_5_3__BLANK_, cell_5_2__BLANK_);
+ (cell_5_3__BLANK_, cell_5_3__BLANK_);
+ (cell_5_3__BLANK_, cell_5_4__BLANK_);
+ (cell_5_3__BLANK_, cell_5_5__BLANK_);
+ (cell_5_3__BLANK_, cell_5_6__BLANK_);
+ (cell_5_4__BLANK_, cell_5_0__BLANK_);
+ (cell_5_4__BLANK_, cell_5_1__BLANK_);
+ (cell_5_4__BLANK_, cell_5_2__BLANK_);
+ (cell_5_4__BLANK_, cell_5_3__BLANK_);
+ (cell_5_4__BLANK_, cell_5_4__BLANK_);
+ (cell_5_4__BLANK_, cell_5_5__BLANK_);
+ (cell_5_4__BLANK_, cell_5_6__BLANK_);
+ (cell_5_5__BLANK_, cell_5_0__BLANK_);
+ (cell_5_5__BLANK_, cell_5_1__BLANK_);
+ (cell_5_5__BLANK_, cell_5_2__BLANK_);
+ (cell_5_5__BLANK_, cell_5_3__BLANK_);
+ (cell_5_5__BLANK_, cell_5_4__BLANK_);
+ (cell_5_5__BLANK_, cell_5_5__BLANK_);
+ (cell_5_5__BLANK_, cell_5_6__BLANK_);
+ (cell_5_6__BLANK_, cell_5_0__BLANK_);
+ (cell_5_6__BLANK_, cell_5_1__BLANK_);
+ (cell_5_6__BLANK_, cell_5_2__BLANK_);
+ (cell_5_6__BLANK_, cell_5_3__BLANK_);
+ (cell_5_6__BLANK_, cell_5_4__BLANK_);
+ (cell_5_6__BLANK_, cell_5_5__BLANK_);
+ (cell_5_6__BLANK_, cell_5_6__BLANK_);
+ (cell_6_0__BLANK_, cell_6_0__BLANK_);
+ (cell_6_0__BLANK_, cell_6_1__BLANK_);
+ (cell_6_0__BLANK_, cell_6_2__BLANK_);
+ (cell_6_0__BLANK_, cell_6_3__BLANK_);
+ (cell_6_0__BLANK_, cell_6_4__BLANK_);
+ (cell_6_0__BLANK_, cell_6_5__BLANK_);
+ (cell_6_0__BLANK_, cell_6_6__BLANK_);
+ (cell_6_1__BLANK_, cell_6_0__BLANK_);
+ (cell_6_1__BLANK_, cell_6_1__BLANK_);
+ (cell_6_1__BLANK_, cell_6_2__BLANK_);
+ (cell_6_1__BLANK_, cell_6_3__BLANK_);
+ (cell_6_1__BLANK_, cell_6_4__BLANK_);
+ (cell_6_1__BLANK_, cell_6_5__BLANK_);
+ (cell_6_1__BLANK_, cell_6_6__BLANK_);
+ (cell_6_2__BLANK_, cell_6_0__BLANK_);
+ (cell_6_2__BLANK_, cell_6_1__BLANK_);
+ (cell_6_2__BLANK_, cell_6_2__BLANK_);
+ (cell_6_2__BLANK_, cell_6_3__BLANK_);
+ (cell_6_2__BLANK_, cell_6_4__BLANK_);
+ (cell_6_2__BLANK_, cell_6_5__BLANK_);
+ (cell_6_2__BLANK_, cell_6_6__BLANK_);
+ (cell_6_3__BLANK_, cell_6_0__BLANK_);
+ (cell_6_3__BLANK_, cell_6_1__BLANK_);
+ (cell_6_3__BLANK_, cell_6_2__BLANK_);
+ (cell_6_3__BLANK_, cell_6_3__BLANK_);
+ (cell_6_3__BLANK_, cell_6_4__BLANK_);
+ (cell_6_3__BLANK_, cell_6_5__BLANK_);
+ (cell_6_3__BLANK_, cell_6_6__BLANK_);
+ (cell_6_4__BLANK_, cell_6_0__BLANK_);
+ (cell_6_4__BLANK_, cell_6_1__BLANK_);
+ (cell_6_4__BLANK_, cell_6_2__BLANK_);
+ (cell_6_4__BLANK_, cell_6_3__BLANK_);
+ (cell_6_4__BLANK_, cell_6_4__BLANK_);
+ (cell_6_4__BLANK_, cell_6_5__BLANK_);
+ (cell_6_4__BLANK_, cell_6_6__BLANK_);
+ (cell_6_5__BLANK_, cell_6_0__BLANK_);
+ (cell_6_5__BLANK_, cell_6_1__BLANK_);
+ (cell_6_5__BLANK_, cell_6_2__BLANK_);
+ (cell_6_5__BLANK_, cell_6_3__BLANK_);
+ (cell_6_5__BLANK_, cell_6_4__BLANK_);
+ (cell_6_5__BLANK_, cell_6_5__BLANK_);
+ (cell_6_5__BLANK_, cell_6_6__BLANK_);
+ (cell_6_6__BLANK_, cell_6_0__BLANK_);
+ (cell_6_6__BLANK_, cell_6_1__BLANK_);
+ (cell_6_6__BLANK_, cell_6_2__BLANK_);
+ (cell_6_6__BLANK_, cell_6_3__BLANK_);
+ (cell_6_6__BLANK_, cell_6_4__BLANK_);
+ (cell_6_6__BLANK_, cell_6_5__BLANK_);
+ (cell_6_6__BLANK_, cell_6_6__BLANK_);
+ (cell_7_0__BLANK_, cell_7_0__BLANK_);
+ (cell_7_0__BLANK_, cell_7_1__BLANK_);
+ (cell_7_0__BLANK_, cell_7_2__BLANK_);
+ (cell_7_0__BLANK_, cell_7_3__BLANK_);
+ (cell_7_0__BLANK_, cell_7_4__BLANK_);
+ (cell_7_0__BLANK_, cell_7_5__BLANK_);
+ (cell_7_0__BLANK_, cell_7_6__BLANK_);
+ (cell_7_1__BLANK_, cell_7_0__BLANK_);
+ (cell_7_1__BLANK_, cell_7_1__BLANK_);
+ (cell_7_1__BLANK_, cell_7_2__BLANK_);
+ (cell_7_1__BLANK_, cell_7_3__BLANK_);
+ (cell_7_1__BLANK_, cell_7_4__BLANK_);
+ (cell_7_1__BLANK_, cell_7_5__BLANK_);
+ (cell_7_1__BLANK_, cell_7_6__BLANK_);
+ (cell_7_2__BLANK_, cell_7_0__BLANK_);
+ (cell_7_2__BLANK_, cell_7_1__BLANK_);
+ (cell_7_2__BLANK_, cell_7_2__BLANK_);
+ (cell_7_2__BLANK_, cell_7_3__BLANK_);
+ (cell_7_2__BLANK_, cell_7_4__BLANK_);
+ (cell_7_2__BLANK_, cell_7_5__BLANK_);
+ (cell_7_2__BLANK_, cell_7_6__BLANK_);
+ (cell_7_3__BLANK_, cell_7_0__BLANK_);
+ (cell_7_3__BLANK_, cell_7_1__BLANK_);
+ (cell_7_3__BLANK_, cell_7_2__BLANK_);
+ (cell_7_3__BLANK_, cell_7_3__BLANK_);
+ (cell_7_3__BLANK_, cell_7_4__BLANK_);
+ (cell_7_3__BLANK_, cell_7_5__BLANK_);
+ (cell_7_3__BLANK_, cell_7_6__BLANK_);
+ (cell_7_4__BLANK_, cell_7_0__BLANK_);
+ (cell_7_4__BLANK_, cell_7_1__BLANK_);
+ (cell_7_4__BLANK_, cell_7_2__BLANK_);
+ (cell_7_4__BLANK_, cell_7_3__BLANK_);
+ (cell_7_4__BLANK_, cell_7_4__BLANK_);
+ (cell_7_4__BLANK_, cell_7_5__BLANK_);
+ (cell_7_4__BLANK_, cell_7_6__BLANK_);
+ (cell_7_5__BLANK_, cell_7_0__BLANK_);
+ (cell_7_5__BLANK_, cell_7_1__BLANK_);
+ (cell_7_5__BLANK_, cell_7_2__BLANK_);
+ (cell_7_5__BLANK_, cell_7_3__BLANK_);
+ (cell_7_5__BLANK_, cell_7_4__BLANK_);
+ (cell_7_5__BLANK_, cell_7_5__BLANK_);
+ (cell_7_5__BLANK_, cell_7_6__BLANK_);
+ (cell_7_6__BLANK_, cell_7_0__BLANK_);
+ (cell_7_6__BLANK_, cell_7_1__BLANK_);
+ (cell_7_6__BLANK_, cell_7_2__BLANK_);
+ (cell_7_6__BLANK_, cell_7_3__BLANK_);
+ (cell_7_6__BLANK_, cell_7_4__BLANK_);
+ (cell_7_6__BLANK_, cell_7_5__BLANK_);
+ (cell_7_6__BLANK_, cell_7_6__BLANK_)
+ };
+ EQ___cell_0__cell_1 {
+ (cell_1_0__BLANK_, cell_1_1__BLANK_);
+ (cell_1_0__BLANK_, cell_2_1__BLANK_);
+ (cell_1_0__BLANK_, cell_3_1__BLANK_);
+ (cell_1_0__BLANK_, cell_4_1__BLANK_);
+ (cell_1_0__BLANK_, cell_5_1__BLANK_);
+ (cell_1_0__BLANK_, cell_6_1__BLANK_);
+ (cell_1_0__BLANK_, cell_7_1__BLANK_);
+ (cell_1_1__BLANK_, cell_1_1__BLANK_);
+ (cell_1_1__BLANK_, cell_2_1__BLANK_);
+ (cell_1_1__BLANK_, cell_3_1__BLANK_);
+ (cell_1_1__BLANK_, cell_4_1__BLANK_);
+ (cell_1_1__BLANK_, cell_5_1__BLANK_);
+ (cell_1_1__BLANK_, cell_6_1__BLANK_);
+ (cell_1_1__BLANK_, cell_7_1__BLANK_);
+ (cell_1_2__BLANK_, cell_1_1__BLANK_);
+ (cell_1_2__BLANK_, cell_2_1__BLANK_);
+ (cell_1_2__BLANK_, cell_3_1__BLANK_);
+ (cell_1_2__BLANK_, cell_4_1__BLANK_);
+ (cell_1_2__BLANK_, cell_5_1__BLANK_);
+ (cell_1_2__BLANK_, cell_6_1__BLANK_);
+ (cell_1_2__BLANK_, cell_7_1__BLANK_);
+ (cell_1_3__BLANK_, cell_1_1__BLANK_);
+ (cell_1_3__BLANK_, cell_2_1__BLANK_);
+ (cell_1_3__BLANK_, cell_3_1__BLANK_);
+ (cell_1_3__BLANK_, cell_4_1__BLANK_);
+ (cell_1_3__BLANK_, cell_5_1__BLANK_);
+ (cell_1_3__BLANK_, cell_6_1__BLANK_);
+ (cell_1_3__BLANK_, cell_7_1__BLANK_);
+ (cell_1_4__BLANK_, cell_1_1__BLANK_);
+ (cell_1_4__BLANK_, cell_2_1__BLANK_);
+ (cell_1_4__BLANK_, cell_3_1__BLANK_);
+ (cell_1_4__BLANK_, cell_4_1__BLANK_);
+ (cell_1_4__BLANK_, cell_5_1__BLANK_);
+ (cell_1_4__BLANK_, cell_6_1__BLANK_);
+ (cell_1_4__BLANK_, cell_7_1__BLANK_);
+ (cell_1_5__BLANK_, cell_1_1__BLANK_);
+ (cell_1_5__BLANK_, cell_2_1__BLANK_);
+ (cell_1_5__BLANK_, cell_3_1__BLANK_);
+ (cell_1_5__BLANK_, cell_4_1__BLANK_);
+ (cell_1_5__BLANK_, cell_5_1__BLANK_);
+ (cell_1_5__BLANK_, cell_6_1__BLANK_);
+ (cell_1_5__BLANK_, cell_7_1__BLANK_);
+ (cell_1_6__BLANK_, cell_1_1__BLANK_);
+ (cell_1_6__BLANK_, cell_2_1__BLANK_);
+ (cell_1_6__BLANK_, cell_3_1__BLANK_);
+ (cell_1_6__BLANK_, cell_4_1__BLANK_);
+ (cell_1_6__BLANK_, cell_5_1__BLANK_);
+ (cell_1_6__BLANK_, cell_6_1__BLANK_);
+ (cell_1_6__BLANK_, cell_7_1__BLANK_);
+ (cell_2_0__BLANK_, cell_1_2__BLANK_);
+ (cell_2_0__BLANK_, cell_2_2__BLANK_);
+ (cell_2_0__BLANK_, cell_3_2__BLANK_);
+ (cell_2_0__BLANK_, cell_4_2__BLANK_);
+ (cell_2_0__BLANK_, cell_5_2__BLANK_);
+ (cell_2_0__BLANK_, cell_6_2__BLANK_);
+ (cell_2_0__BLANK_, cell_7_2__BLANK_);
+ (cell_2_1__BLANK_, cell_1_2__BLANK_);
+ (cell_2_1__BLANK_, cell_2_2__BLANK_);
+ (cell_2_1__BLANK_, cell_3_2__BLANK_);
+ (cell_2_1__BLANK_, cell_4_2__BLANK_);
+ (cell_2_1__BLANK_, cell_5_2__BLANK_);
+ (cell_2_1__BLANK_, cell_6_2__BLANK_);
+ (cell_2_1__BLANK_, cell_7_2__BLANK_);
+ (cell_2_2__BLANK_, cell_1_2__BLANK_);
+ (cell_2_2__BLANK_, cell_2_2__BLANK_);
+ (cell_2_2__BLANK_, cell_3_2__BLANK_);
+ (cell_2_2__BLANK_, cell_4_2__BLANK_);
+ (cell_2_2__BLANK_, cell_5_2__BLANK_);
+ (cell_2_2__BLANK_, cell_6_2__BLANK_);
+ (cell_2_2__BLANK_, cell_7_2__BLANK_);
+ (cell_2_3__BLANK_, cell_1_2__BLANK_);
+ (cell_2_3__BLANK_, cell_2_2__BLANK_);
+ (cell_2_3__BLANK_, cell_3_2__BLANK_);
+ (cell_2_3__BLANK_, cell_4_2__BLANK_);
+ (cell_2_3__BLANK_, cell_5_2__BLANK_);
+ (cell_2_3__BLANK_, cell_6_2__BLANK_);
+ (cell_2_3__BLANK_, cell_7_2__BLANK_);
+ (cell_2_4__BLANK_, cell_1_2__BLANK_);
+ (cell_2_4__BLANK_, cell_2_2__BLANK_);
+ (cell_2_4__BLANK_, cell_3_2__BLANK_);
+ (cell_2_4__BLANK_, cell_4_2__BLANK_);
+ (cell_2_4__BLANK_, cell_5_2__BLANK_);
+ (cell_2_4__BLANK_, cell_6_2__BLANK_);
+ (cell_2_4__BLANK_, cell_7_2__BLANK_);
+ (cell_2_5__BLANK_, cell_1_2__BLANK_);
+ (cell_2_5__BLANK_, cell_2_2__BLANK_);
+ (cell_2_5__BLANK_, cell_3_2__BLANK_);
+ (cell_2_5__BLANK_, cell_4_2__BLANK_);
+ (cell_2_5__BLANK_, cell_5_2__BLANK_);
+ (cell_2_5__BLANK_, cell_6_2__BLANK_);
+ (cell_2_5__BLANK_, cell_7_2__BLANK_);
+ (cell_2_6__BLANK_, cell_1_2__BLANK_);
+ (cell_2_6__BLANK_, cell_2_2__BLANK_);
+ (cell_2_6__BLANK_, cell_3_2__BLANK_);
+ (cell_2_6__BLANK_, cell_4_2__BLANK_);
+ (cell_2_6__BLANK_...
[truncated message content] |
