[Toss-devel-svn] SF.net SVN: toss:[1555] trunk/Toss

[<luk...@us...>]

Revision: 1555
          http://toss.svn.sourceforge.net/toss/?rev=1555&view=rev
Author:   lukstafi
Date:     2011-09-02 13:37:14 +0000 (Fri, 02 Sep 2011)
Log Message:
-----------
FormulaMap: adapting to let-in expressions. GDL translation fixing: bugs (generating stable paths; finding paths for defined relation arguments). GameSimpl minor bug. Bugs in move translation for concurrent games. Fixing TranslateGame regression tests.

Modified Paths:
--------------
    trunk/Toss/Formula/FormulaMap.ml
    trunk/Toss/Formula/FormulaMap.mli
    trunk/Toss/GGP/GDL.ml
    trunk/Toss/GGP/GDL.mli
    trunk/Toss/GGP/GameSimpl.ml
    trunk/Toss/GGP/TranslateFormula.ml
    trunk/Toss/GGP/TranslateGame.ml
    trunk/Toss/GGP/TranslateGameTest.ml
    trunk/Toss/GGP/tests/2player_normal_form_2010-raw.toss
    trunk/Toss/GGP/tests/2player_normal_form_2010-simpl.toss
    trunk/Toss/GGP/tests/connect5-raw.toss
    trunk/Toss/GGP/tests/connect5-simpl.toss
    trunk/Toss/GGP/tests/tictactoe-raw.toss
    trunk/Toss/GGP/tests/tictactoe-simpl.toss

Modified: trunk/Toss/Formula/FormulaMap.ml
===================================================================
--- trunk/Toss/Formula/FormulaMap.ml	2011-08-31 23:11:10 UTC (rev 1554)
+++ trunk/Toss/Formula/FormulaMap.ml	2011-09-02 13:37:14 UTC (rev 1555)
@@ -16,6 +16,8 @@
   | All (vs, phi) -> All (vs, map_to_literals f g phi)
   | Lfp (v, vs, phi) -> Lfp (v, vs, map_to_literals f g phi)
   | Gfp (v, vs, phi) -> Gfp (v, vs, map_to_literals f g phi)
+  | Let (rel, args, body, scope) ->
+    Let (rel, args, map_to_literals f g body, map_to_literals f g scope)
 
 and map_to_literals_expr f g = function
   | RVar _ | Const _ | Fun _ as x -> g x
@@ -26,6 +28,8 @@
   | Char (phi) -> Char (map_to_literals f g phi)
   | Sum (vs, phi, r) ->
     Sum (vs, map_to_literals f g phi, map_to_literals_expr f g r)
+  | RLet (func, body, scope) ->
+    RLet (func, map_to_literals_expr f g body, map_to_literals_expr f g scope)
 
 (* Map [f] to all atoms in the given formula. *)
 let map_to_atoms_full f g phi =
@@ -63,6 +67,7 @@
   map_All : var list -> formula -> formula;
   map_Lfp : [ mso_var | so_var ] -> fo_var array -> formula -> formula;
   map_Gfp : [ mso_var | so_var ] -> fo_var array -> formula -> formula;
+  map_Let : string -> string list -> formula -> formula -> formula;
 
   map_RVar : string -> real_expr;
   map_Const : float -> real_expr;
@@ -70,7 +75,8 @@
   map_Plus : real_expr -> real_expr -> real_expr;
   map_Fun : string -> fo_var -> real_expr;
   map_Char : formula -> real_expr;
-  map_Sum : fo_var list -> formula -> real_expr -> real_expr
+  map_Sum : fo_var list -> formula -> real_expr -> real_expr;
+  map_RLet : string -> real_expr -> real_expr -> real_expr
 }
 
 let identity_map = {
@@ -86,6 +92,7 @@
   map_All = (fun vs phi -> All (vs, phi));
   map_Lfp = (fun v vs phi -> Lfp (v, vs, phi));
   map_Gfp = (fun v vs phi -> Gfp (v, vs, phi));
+  map_Let = (fun rel args body scope -> Let (rel, args, body, scope));
 
   map_RVar = (fun v -> RVar v);
   map_Const = (fun c -> Const c);
@@ -93,7 +100,8 @@
   map_Plus = (fun expr1 expr2 -> Plus (expr1, expr2));
   map_Fun = (fun f v -> Fun (f, v));
   map_Char = (fun phi -> Char phi);
-  map_Sum = (fun vs guard expr -> Sum (vs, guard, expr))
+  map_Sum = (fun vs guard expr -> Sum (vs, guard, expr));
+  map_RLet = (fun f body scope -> RLet (f, body, scope));
 }
 
 let rec map_formula gmap = function
@@ -110,6 +118,8 @@
   | All (vs, phi) -> gmap.map_All vs (map_formula gmap phi)
   | Lfp (v, vs, phi) -> gmap.map_Lfp v vs (map_formula gmap phi)
   | Gfp (v, vs, phi) -> gmap.map_Gfp v vs (map_formula gmap phi)
+  | Let (rel, args, body, scope) ->
+    gmap.map_Let rel args (map_formula gmap body) (map_formula gmap scope)
 
 and map_real_expr gmap = function
   | RVar v -> gmap.map_RVar v
@@ -122,6 +132,8 @@
   | Char phi -> gmap.map_Char (map_formula gmap phi)
   | Sum (vs, guard, expr) ->
     gmap.map_Sum vs (map_formula gmap guard) (map_real_expr gmap expr)
+  | RLet (f, body, scope) ->
+    gmap.map_RLet f (map_real_expr gmap body) (map_real_expr gmap scope)
 
 
 (* Generalized fold over formula and real expression types. *)
@@ -138,6 +150,7 @@
   fold_All : var list -> 'a -> 'a;
   fold_Lfp : [ mso_var | so_var ] -> fo_var array -> 'a -> 'a;
   fold_Gfp : [ mso_var | so_var ] -> fo_var array -> 'a -> 'a;
+  fold_Let : string -> string list -> 'a -> 'a -> 'a;
 
   fold_RVar : string -> 'a;
   fold_Const : float -> 'a;
@@ -145,7 +158,8 @@
   fold_Plus : 'a -> 'a -> 'a;
   fold_Fun : string -> fo_var -> 'a;
   fold_Char : 'a -> 'a;
-  fold_Sum : fo_var list -> 'a -> 'a -> 'a
+  fold_Sum : fo_var list -> 'a -> 'a -> 'a;
+  fold_RLet : string -> 'a -> 'a -> 'a
 }
 
 let make_fold union empty = {
@@ -161,6 +175,7 @@
   fold_All = (fun _ phi -> phi);
   fold_Lfp = (fun _ _ phi -> phi);
   fold_Gfp = (fun _ _ phi -> phi);
+  fold_Let = (fun _ _ -> union);
 
   fold_RVar = (fun _ -> empty);
   fold_Const = (fun _ -> empty);
@@ -168,7 +183,8 @@
   fold_Plus = union;
   fold_Fun = (fun _ _ -> empty);
   fold_Char = (fun phi -> phi);
-  fold_Sum = (fun _ guard expr -> union guard expr)
+  fold_Sum = (fun _ guard expr -> union guard expr);
+  fold_RLet = (fun _ -> union)
 }
 
 open Aux.BasicOperators
@@ -197,6 +213,8 @@
   | All (vs, phi) -> gfold.fold_All vs (fold_formula gfold phi)
   | Lfp (v, vs, phi) -> gfold.fold_Lfp v vs (fold_formula gfold phi)
   | Gfp (v, vs, phi) -> gfold.fold_Gfp v vs (fold_formula gfold phi)
+  | Let (rel, args, body, scope) ->
+    gfold.fold_Let rel args (fold_formula gfold body) (fold_formula gfold scope)
 
 and fold_real_expr gfold = function
   | RVar v -> gfold.fold_RVar v
@@ -209,6 +227,8 @@
   | Char phi -> gfold.fold_Char (fold_formula gfold phi)
   | Sum (vs, guard, expr) ->
     gfold.fold_Sum vs (fold_formula gfold guard) (fold_real_expr gfold expr)
+  | RLet (f, body, scope) ->
+    gfold.fold_RLet f (fold_real_expr gfold body) (fold_real_expr gfold scope)
 
 (* Map [f] to top-level formulas in the real expression ([Char]s and
    [Sum] guards). *)
@@ -221,6 +241,8 @@
   | Char (phi) -> Char (f phi)
   | Sum (vs, phi, r) ->
     Sum (vs, f phi, map_to_formulas_expr f r)
+  | RLet (func, body, scope) ->
+    RLet (func, map_to_formulas_expr f body, map_to_formulas_expr f scope)
 
 let rec fold_over_formulas_expr f r acc =
   match r with
@@ -231,6 +253,8 @@
     | Char (phi) -> f phi acc
     | Sum (vs, phi, r) ->
       fold_over_formulas_expr f r (f phi acc)
+    | RLet (func, r1, r2) ->
+      fold_over_formulas_expr f r1 (fold_over_formulas_expr f r2 acc)
 
 let rec fold_over_literals f phi acc =
   match phi with
@@ -242,6 +266,8 @@
     | And flist -> List.fold_right (fold_over_literals f) flist acc
     | Ex (_, phi) | All (_, phi) -> fold_over_literals f phi acc
     | Lfp (_, _, phi) | Gfp (_, _, phi) -> fold_over_literals f phi acc
+    | Let (_, _, body, scope) ->
+      fold_over_literals f body (fold_over_literals f scope acc)
 
 and fold_over_literals_expr f =
   fold_over_formulas_expr (fold_over_literals f)
@@ -252,6 +278,25 @@
 
 (* Map [f] to all variables occurring in the formula. Preserves order
    of subformulas. *)
+let map_to_all_vars (f : var -> var) phi =
+  let foaf va = Array.map (fun x -> to_fo (f (x :> var))) va in
+  let safs va = List.map (fun x -> var_str (f (var_of_string x))) va in
+  map_formula
+    {identity_map with
+      map_Rel = (fun rn vl -> Rel (rn, foaf vl));
+      map_Eq = (fun x y -> Eq (to_fo (f (x :> var)), to_fo (f (y :> var))));
+      map_In = (fun x y -> In (to_fo (f (x :> var)), to_mso (f (y :> var))));
+      map_SO = (fun v vs -> SO (to_so (f (v :> var)), foaf vs));
+      map_Ex = (fun vs phi -> Ex (List.map f vs, phi));
+      map_All = (fun vs phi -> All (List.map f vs, phi));
+      map_Lfp = (fun v vs phi -> 
+        Lfp (to_mso_or_so (f (v :> var)), foaf vs, phi));
+      map_Gfp = (fun v vs phi -> 
+        Gfp (to_mso_or_so (f (v :> var)), foaf vs, phi));
+      map_Let = (fun rel args body scope ->
+        Let (rel, safs args, body, scope))
+    } phi      
+(* alternative direct definition
 let rec map_to_all_vars (f : var -> var) phi =
   let foaf va = Array.map (fun x -> to_fo (f (x :> var))) va in
   match phi with
@@ -269,5 +314,7 @@
       Lfp (to_mso_or_so (f (v :> var)), foaf vs, map_to_all_vars f phi)
     | Gfp (v, vs, phi) -> 
       Gfp (to_mso_or_so (f (v :> var)), foaf vs, map_to_all_vars f phi)
+    | Let (rel, args, body, scope) ->
+      Let (rel, args, map_to_all_vars f body, map_to_all_vars f scope)
+*)
 
-

Modified: trunk/Toss/Formula/FormulaMap.mli
===================================================================
--- trunk/Toss/Formula/FormulaMap.mli	2011-08-31 23:11:10 UTC (rev 1554)
+++ trunk/Toss/Formula/FormulaMap.mli	2011-09-02 13:37:14 UTC (rev 1555)
@@ -35,6 +35,7 @@
   map_All : var list -> formula -> formula;
   map_Lfp : [ mso_var | so_var ] -> fo_var array -> formula -> formula;
   map_Gfp : [ mso_var | so_var ] -> fo_var array -> formula -> formula;
+  map_Let : string -> string list -> formula -> formula -> formula;
 
   map_RVar : string -> real_expr;
   map_Const : float -> real_expr;
@@ -42,7 +43,8 @@
   map_Plus : real_expr -> real_expr -> real_expr;
   map_Fun : string -> fo_var -> real_expr;
   map_Char : formula -> real_expr;
-  map_Sum : fo_var list -> formula -> real_expr -> real_expr
+  map_Sum : fo_var list -> formula -> real_expr -> real_expr;
+  map_RLet : string -> real_expr -> real_expr -> real_expr
 }
 
 (** Identity map to be refined using the [with] syntax. *)
@@ -66,6 +68,7 @@
   fold_All : var list -> 'a -> 'a;
   fold_Lfp : [ mso_var | so_var ] -> fo_var array -> 'a -> 'a;
   fold_Gfp : [ mso_var | so_var ] -> fo_var array -> 'a -> 'a;
+  fold_Let : string -> string list -> 'a -> 'a -> 'a;
 
   fold_RVar : string -> 'a;
   fold_Const : float -> 'a;
@@ -73,7 +76,8 @@
   fold_Plus : 'a -> 'a -> 'a;
   fold_Fun : string -> fo_var -> 'a;
   fold_Char : 'a -> 'a;
-  fold_Sum : fo_var list -> 'a -> 'a -> 'a
+  fold_Sum : fo_var list -> 'a -> 'a -> 'a;
+  fold_RLet : string -> 'a -> 'a -> 'a
 }
 
 val make_fold : ('a -> 'a -> 'a) -> 'a -> 'a formula_and_expr_fold

Modified: trunk/Toss/GGP/GDL.ml
===================================================================
--- trunk/Toss/GGP/GDL.ml	2011-08-31 23:11:10 UTC (rev 1554)
+++ trunk/Toss/GGP/GDL.ml	2011-09-02 13:37:14 UTC (rev 1555)
@@ -1745,17 +1745,17 @@
 
 (* Split paths in the set until, if possible, none of subterms at the
    paths meets the predicate. Also remove paths not present in terms. *)
-let refine_paths_avoiding paths avoid terms =
+let refine_paths_avoiding paths avoid_later avoid_now terms =
   let rec aux terms = function
     | Empty -> Empty
     | Here ->
       if terms=[] then Empty
-      else if not (List.exists avoid terms)
+      else if not (List.exists avoid_later terms)
       then Here
       else
         let subterms =
           Aux.map_some (function
-            | Func (rel,args) as t when not (avoid t) -> Some (rel,args)
+            | Func (rel,args) as t when not (avoid_now t) -> Some (rel,args)
             | _ -> None) terms in
         if subterms = [] then Empty
         else
@@ -1764,7 +1764,7 @@
             let arity =
               Array.length (List.hd args_set) in
             (* {{{ log entry *)
-            if !debug_level > 3 then (
+            if !debug_level > 1 then (
               Printf.printf "refine_paths_avoiding: aux rel=%s, no terms=%d\n%!"
                 rel (List.length args_set)
             );
@@ -1772,12 +1772,12 @@
             rel, aux2 (Array.make arity Here) args_set) subterms)
     | (Here_and_below subpaths | Below subpaths) as path ->
       if terms=[] then Empty
-      else if not (List.exists avoid terms)
+      else if not (List.exists avoid_later terms)
       then path
       else
         let subterms =
           Aux.map_some (function
-            | Func (rel,args) as t when not (avoid t) -> Some (rel,args)
+            | Func (rel,args) as t when not (avoid_now t) -> Some (rel,args)
             | _ -> None) terms in
         if subterms = [] then Empty
         else

Modified: trunk/Toss/GGP/GDL.mli
===================================================================
--- trunk/Toss/GGP/GDL.mli	2011-08-31 23:11:10 UTC (rev 1554)
+++ trunk/Toss/GGP/GDL.mli	2011-09-02 13:37:14 UTC (rev 1555)
@@ -264,8 +264,10 @@
     paths that together cover all leafs the original path covered. *)
 val refine_leaf_paths : path_set -> term list -> path_set
 
-(** Split paths in the set until, if possible, none of subterms at the
-    paths meets the predicate. Also remove paths not present in
-    terms. *)
+(** [refine_paths_avoiding paths avoid_later avoid_now terms] splits
+    paths in the set until, if possible, none of subterms at the paths
+    meets the predicate [avoid_later]; it does not descend subterms
+    for which [avoid_now] holds. Also removes paths not present
+    in terms. *)
 val refine_paths_avoiding :
-  path_set -> (term -> bool) -> term list -> path_set
+  path_set -> (term -> bool) -> (term -> bool) -> term list -> path_set

Modified: trunk/Toss/GGP/GameSimpl.ml
===================================================================
--- trunk/Toss/GGP/GameSimpl.ml	2011-08-31 23:11:10 UTC (rev 1554)
+++ trunk/Toss/GGP/GameSimpl.ml	2011-09-02 13:37:14 UTC (rev 1555)
@@ -313,7 +313,7 @@
         | None -> rel
         | Some spec -> DiscreteRule.orig_rel_of rel in
     (* {{{ log entry *)
-    if !debug_level > 3 then (
+    if !debug_level > 4 then (
       Printf.printf "removable: %s...%!" rel
     );
     (* }}} *)
@@ -326,7 +326,7 @@
                List.mem_assoc (fst (List.assoc rel equivalent))
                game.Arena.defined_rels) in
     (* {{{ log entry *)
-    if !debug_level > 3 then (
+    if !debug_level > 4 then (
       Printf.printf "%B\n%!" res;
     );
     (* }}} *)
@@ -926,6 +926,7 @@
       ) &&
         not (Aux.Strings.mem rel fluents) &&
         (not (Aux.Strings.mem rel used_rels) ||
+           not (List.mem_assoc rel defined_rels) &&
            Structure.rel_size !struc rel = 0) in
     (* {{{ log entry *)
     if !debug_level > 2 && res then (

Modified: trunk/Toss/GGP/TranslateFormula.ml
===================================================================
--- trunk/Toss/GGP/TranslateFormula.ml	2011-08-31 23:11:10 UTC (rev 1554)
+++ trunk/Toss/GGP/TranslateFormula.ml	2011-09-02 13:37:14 UTC (rev 1555)
@@ -310,16 +310,32 @@
           | _ -> None)
         (atoms_of_body body) in
       r_atoms, state_terms body
-      (* we take all state terms to have more compact partition *)
-      (*Aux.map_some
-        (function Pos (True s) -> Some s | _ -> None) body*))
+          (* we take all state terms to have more compact partition *)
+          (*Aux.map_some
+            (function Pos (True s) -> Some s | _ -> None) body*))
     clauses in
   let check_path args p s_p =
     let inds = Aux.array_argfind_all (fun r -> r=s_p) args in
     List.map (fun i->p,i) inds in
   let sterm_path_sets args s =
-    let ptups = Aux.product
-      (map_paths (check_path args) data.m_paths s) in
+    (* {{{ log entry *)
+    if !debug_level > 4 then (
+      Printf.printf "sterm_path_sets: rel=%s args={%s} sterm=%s\n%!"
+        drel
+        (String.concat ", " (Array.to_list (Array.map term_str args)))
+        (term_str s)
+    );
+    (* }}} *)
+    let psets = map_paths (check_path args) data.m_paths s in
+    (* {{{ log entry *)
+    if !debug_level > 4 then (
+      Printf.printf "sterm_path_sets: psets=%s\n%!"
+        (String.concat "; "(List.map (fun pset->"["^
+          String.concat ", " (List.map (fun (p,i)->
+            path_str p^":"^string_of_int i) pset)^"]") psets))
+    );
+    (* }}} *)
+    let ptups = Aux.product (Aux.list_remove [] psets) in
     (* distinct [p] in a tuple is already ensured *)
     List.filter (fun tup ->
       not (Aux.not_unique (List.map snd tup))) ptups in

Modified: trunk/Toss/GGP/TranslateGame.ml
===================================================================
--- trunk/Toss/GGP/TranslateGame.ml	2011-08-31 23:11:10 UTC (rev 1554)
+++ trunk/Toss/GGP/TranslateGame.ml	2011-09-02 13:37:14 UTC (rev 1555)
@@ -424,7 +424,8 @@
   );
   (* }}} *)
   let m_paths =
-    refine_paths_avoiding eps_path_set contains_blank element_reps in
+    refine_paths_avoiding eps_path_set
+      contains_blank (fun t->t=blank) element_reps in
   (* {{{ log entry *)
   if !debug_level > 2 then (
     Printf.printf
@@ -1336,7 +1337,10 @@
   (* a defined relation for checking game termination *)
   let nonterminal = Formula.Not (Formula.Rel ("terminal", [||])) in
   let precond =
-    Formula.And (nonterminal :: synch_precond @ [case_precond]) in
+    if legal_tuple = [] then            (* Environment rule *)
+      Formula.And (synch_precond @ [case_precond])
+    else
+      Formula.And (nonterminal :: synch_precond @ [case_precond]) in
   (* {{{ log entry *)
   if !debug_level > 2 then (
     Printf.printf "build_toss_rule: synch precond = %s; main precond = %s\n%!"
@@ -1591,7 +1595,7 @@
   payoffs
 
 
-let transl_arg_type_no_side defined_rels init_state program
+let transl_argpath_no_side defined_rels init_state program
     ground_at_m_paths =
   if ground_at_m_paths = [] then []
   else
@@ -1774,6 +1778,18 @@
       let args = List.assoc rel (List.map fst clauses) in
       rel, Array.length args)
     defined_rels in
+  let argpath_no_side =
+    transl_argpath_no_side defined_rel_arities init_state program
+      (ground_at m_paths) in
+  (* {{{ log entry *)
+  if !debug_level > 2 then (
+    Printf.printf "argpath_no_side:\n%!";
+    List.iter (fun (rel, argps) ->
+      Printf.printf "default paths for %s: %s\n%!" rel
+        (String.concat "; "(List.map (function None -> "None"
+          | Some p -> path_str p) (Array.to_list argps)))) argpath_no_side;
+  );
+  (* }}} *)
   let transl_data = {
     TranslateFormula.f_paths = f_paths;
     m_paths = m_paths;
@@ -1782,9 +1798,7 @@
     defined_rels = defined_rels;
     defrel_argpaths = [];           (* built in TranslateFormula *)
     term_arities = term_arities;
-    rel_default_path =
-      transl_arg_type_no_side defined_rel_arities init_state program
-        (ground_at m_paths);
+    rel_default_path = argpath_no_side;
   } in
   (* Building defined rels needs to happen between creating rule
      candidates and rule translation, so that transformed clauses don't
@@ -1793,6 +1807,13 @@
   (* Transform the rule conditions as well so they can be translated. *)
   let rule_cands, clauses =
     encode_rule_cands_in_clauses rule_cands clauses in
+  (* {{{ log entry *)
+  if !debug_level > 2 then (
+    Printf.printf
+      "traslate_game: all clauses prior to building defined rels\n%s\n\n%!"
+      (String.concat "\n"(List.map clause_str clauses));
+  );
+  (* }}} *)
   let clauses, defined_rels =
     TranslateFormula.build_defrels transl_data clauses in
   let rule_cands, clauses =
@@ -2031,9 +2052,13 @@
     (fun player move ->
       let tossrules =
         Aux.strmap_filter (fun  _ rdata ->
-          try ignore (unify [] [move]
-                        [rdata.legal_tuple.(player)]); true
-          with Not_found -> false
+          rdata.legal_tuple <> [||] &&  (* not Environment rule *)
+            let legal_term =
+              if Array.length rdata.legal_tuple > 1
+              then rdata.legal_tuple.(player)
+              else rdata.legal_tuple.(0) in
+            try ignore (unify [] [move] [legal_term]); true
+            with Not_found -> false
         ) gdl.tossrule_data in
       let candidates = Aux.map_some (fun (rname, rdata) ->
         translate_incoming_single_action gdl.fluents gdl.transl_data
@@ -2046,30 +2071,30 @@
                 " for player " ^ string_of_int player)
         | [rname, emb, lhs_struc] ->
       (* {{{ log entry *)
-      if !debug_level > 0 then (
-        Printf.printf "GDL.translate_incoming_move: rname=%s; emb=%s\n...%!"
-          rname
-          (String.concat ", " (List.map (fun (v,e) ->
-            Structure.elem_str lhs_struc v ^ ": " ^
-              Structure.elem_str struc e) emb))
-      );
-      (* }}} *)
-        player, (rname, emb)
+          if !debug_level > 0 then (
+            Printf.printf "GDL.translate_incoming_move: rname=%s; emb=%s\n...%!"
+              rname
+              (String.concat ", " (List.map (fun (v,e) ->
+                Structure.elem_str lhs_struc v ^ ": " ^
+                  Structure.elem_str struc e) emb))
+          );
+        (* }}} *)
+          player, (rname, emb)
         | _ ->
       (* {{{ log entry *)
-      if !debug_level > 0 then (
-        Printf.printf "GDL.translate_incoming_move: ambiguity\n%!";
-        List.iter (fun (rname, emb, lhs_struc) ->
-          Printf.printf "rname=%s; emb=%s\n%!"
-            rname
-            (String.concat ", " (List.map (fun (v,e) ->
-              Structure.elem_str lhs_struc v ^ ": " ^
-                Structure.elem_str struc e) emb))) candidates
-      );
-      (* }}} *)      
-        failwith
-        ("GDL.translate_incoming_move: ambiguity among rules "^
-            String.concat ", " (List.map Aux.fst3 candidates))
+          if !debug_level > 0 then (
+            Printf.printf "GDL.translate_incoming_move: ambiguity\n%!";
+            List.iter (fun (rname, emb, lhs_struc) ->
+              Printf.printf "rname=%s; emb=%s\n%!"
+                rname
+                (String.concat ", " (List.map (fun (v,e) ->
+                  Structure.elem_str lhs_struc v ^ ": " ^
+                    Structure.elem_str struc e) emb))) candidates
+          );
+        (* }}} *)      
+          failwith
+            ("GDL.translate_incoming_move: ambiguity among rules "^
+                String.concat ", " (List.map Aux.fst3 candidates))
     )
     actions in
   Array.to_list candidates
@@ -2116,12 +2141,26 @@
   );
   (* }}} *)
   (* 10d *)
-  let emb = List.map (fun (lhs_e, struc_e) ->
+  (* only the synchronization element should raise [Not_found] *)
+  let emb = Aux.map_try (fun (lhs_e, struc_e) ->
     let v = DiscreteRule.elemvar_of_elem
       rule.ContinuousRule.compiled.DiscreteRule.lhs_elem_inv_names
       lhs_e in
+    (* {{{ log entry *)
+    if !debug_level > 3 then (
+      Printf.printf
+        "translate_outgoing_move: emb lhs_e=%d, v=%s, struc_e=%d\n%!"
+        lhs_e v struc_e;
+      Printf.printf
+        "translate_outgoing_move: emb lhs term=%s\n%!"
+        (term_str (Aux.StrMap.find v tossrule.rulevar_terms));
+      Printf.printf
+        "translate_outgoing_move: emb struc term=%s\n%!"
+        (term_str (Aux.IntMap.find struc_e gdl.elem_term_map));
+    );
+    (* }}} *)
     Aux.StrMap.find v tossrule.rulevar_terms,
-    Aux.IntMap.find struc_e gdl.elem_term_map) emb in
+      Aux.IntMap.find struc_e gdl.elem_term_map) emb in
   (* {{{ log entry *)
   if !debug_level > 2 then (
     Printf.printf "outgoing-emb={%s}\n%!"

Modified: trunk/Toss/GGP/TranslateGameTest.ml
===================================================================
--- trunk/Toss/GGP/TranslateGameTest.ml	2011-08-31 23:11:10 UTC (rev 1554)
+++ trunk/Toss/GGP/TranslateGameTest.ml	2011-09-02 13:37:14 UTC (rev 1555)
@@ -93,17 +93,13 @@
     (norm_move (rname, emb)) (norm_move move)
 
 (* COPIED FROM ReqHandler. *)
-let select_moving a = (* temporary func - accept just one player w/ moves *)
-  let locs = Aux.array_find_all (fun l -> l.Arena.moves <> []) a in
-  if List.length locs <> 1 then failwith "too many moves" else
-    if locs = [] then a.(0) else List.hd locs
 exception Found of int
 (* The player applying the rewrite seems not to be used. *)
-(* FIXME: adapt to simultaneous moves. *)
+(* Problem: are players indexed from 0 or from 1 in graph? *)
 let apply_rewrite state (player, (r_name, mtch)) =
   if r_name <> "" then (
     let {Arena.rules=rules; graph=graph} = fst state in
-    let mv_loc = select_moving graph.((snd state).Arena.cur_loc) in
+    let mv_loc = graph.((snd state).Arena.cur_loc).(player) in
     let moves =
       Move.gen_moves Move.cGRID_SIZE rules
         (snd state).Arena.struc mv_loc in
@@ -184,11 +180,13 @@
     (fun () ->
       simult_test_case ~game_name:"2player_normal_form_2010" ~player:"row"
         ~own_plnum:0 ~opp_plnum:1
-        ~own_rule_name:"row"
-        ~own_emb:["_BLANK_", "_BLANK_"]
+        ~own_rule_name:"r1"
+        ~own_emb:["did__BLANK___BLANK_", "did__BLANK___BLANK_";
+                  "reward_r1_c1_90_90", "reward_r1_c1_90_90"]
         ~own_move:"r1"
-        ~opp_rule_name:"column"
-        ~opp_emb:["_BLANK_", "_BLANK_"]
+        ~opp_rule_name:"c1"
+        ~opp_emb:["did__BLANK___BLANK_", "did__BLANK___BLANK_";
+                  "reward_r1_c1_90_90", "reward_r1_c1_90_90"]
         ~opp_move:"c1"
     );
 
@@ -225,7 +223,7 @@
       (* adjacent_cell is a defined relation only because it has
          large arity: see {!TranslateGame.defined_arity_above}. *)
       assert_equal ~msg:"defined_rels" ~printer:(fun x->x)
-        "adjacent_cell, col, conn5, diag1, diag2, exists_empty_cell, exists_line_of_five, goal, legal, next, row, terminal"
+        "adjacent, adjacent_cell, col, conn5, diag1, diag2, exists_empty_cell, exists_line_of_five, goal, legal, next, row, terminal"
         (String.concat ", " (List.sort String.compare defined_rels));
 
       assert_equal ~msg:"fluents" ~printer:(fun x->x)
@@ -233,7 +231,7 @@
         (String.concat ", " fluents);
 
       assert_equal ~msg:"stable_rels" ~printer:(fun x->x)
-        "EQ___cell_0__cell_0, EQ___cell_0__cell_1, EQ___cell_1__cell_0, EQ___cell_1__cell_1, adjacent__cell_0__cell_0, adjacent__cell_0__cell_1, adjacent__cell_1__cell_0, adjacent__cell_1__cell_1, cell_0a, cell_0b, cell_0c, cell_0d, cell_0e, cell_0f, cell_0g, cell_0h, cell_1a, cell_1b, cell_1c, cell_1d, cell_1e, cell_1f, cell_1g, cell_1h, cell__BLANK___BLANK___BLANK_, control__BLANK_, coordinate__cell_0, coordinate__cell_1, nextcol__cell_0__cell_0, nextcol__cell_0__cell_1, nextcol__cell_1__cell_0, nextcol__cell_1__cell_1"
+        "EQ___cell_0__cell_0, EQ___cell_0__cell_1, EQ___cell_1__cell_0, EQ___cell_1__cell_1, cell_0a, cell_0b, cell_0c, cell_0d, cell_0e, cell_0f, cell_0g, cell_0h, cell_1a, cell_1b, cell_1c, cell_1d, cell_1e, cell_1f, cell_1g, cell_1h, cell__BLANK___BLANK___BLANK_, control__BLANK_, coordinate__cell_0, coordinate__cell_1, nextcol__cell_0__cell_0, nextcol__cell_0__cell_1, nextcol__cell_1__cell_0, nextcol__cell_1__cell_1"
         (String.concat ", " stable_rels);
 
       assert_equal ~msg:"structure elements" ~printer:(fun x->x)
@@ -246,15 +244,15 @@
     (fun () ->
       game_test_case ~game_name:"connect5" ~player:"x"
         ~own_plnum:0 ~opponent_plnum:1
-        ~loc0_rule_name:"mark_x161_y162_0"
+        ~loc0_rule_name:"mark_x5_y5_noop"
         ~loc0_emb:[
-          "cell_x161_y162__blank_", "cell_e_f_MV1";
-          "control__blank_", "control_MV1"]
+          "cell_x5_y5__BLANK_", "cell_e_f__BLANK_";
+          "control__BLANK_", "control__BLANK_"]
         ~loc0_move:"(mark e f)" ~loc0_noop:"noop"
-        ~loc1:1 ~loc1_rule_name:"mark_x175_y176_1"
+        ~loc1:1 ~loc1_rule_name:"noop_mark_x6_y6"
         ~loc1_emb:[
-          "cell_x175_y176__blank_", "cell_f_g_MV1";
-          "control__blank_", "control_MV1"]
+          "cell_x6_y6__BLANK_", "cell_f_g__BLANK_";
+          "control__BLANK_", "control__BLANK_"]
         ~loc1_noop:"noop" ~loc1_move:"(mark f g)"
     );
 
@@ -270,8 +268,8 @@
         ~loc0_move:"(move 2 2 1 3)" ~loc0_noop:"noop" ~loc1:1
         ~loc1_rule_name:"noop_move_x7_y9_x8_y10"
         ~loc1_emb:[
-          "cellholds_x7_y9__blank_", "cellholds_7_7__BLANK_";
-          "cellholds_x8_y10__blank_", "cellholds_6_6__BLANK_";
+          "cellholds_x7_y9__BLANK_", "cellholds_7_7__BLANK_";
+          "cellholds_x8_y10__BLANK_", "cellholds_6_6__BLANK_";
           "control__BLANK_", "control__BLANK_"]
         ~loc1_noop:"noop" ~loc1_move:"(move 7 7 6 6)"
     );
@@ -307,11 +305,13 @@
   set_debug_level 4;
       simult_test_case ~game_name:"2player_normal_form_2010" ~player:"row"
         ~own_plnum:0 ~opp_plnum:1
-        ~own_rule_name:"row"
-        ~own_emb:["_BLANK_", "_BLANK_"]
+        ~own_rule_name:"r1"
+        ~own_emb:["did__BLANK___BLANK_", "did__BLANK___BLANK_";
+                  "reward_r1_c1_90_90", "reward_r1_c1_90_90"]
         ~own_move:"r1"
-        ~opp_rule_name:"column"
-        ~opp_emb:["_BLANK_", "_BLANK_"]
+        ~opp_rule_name:"c1"
+        ~opp_emb:["did__BLANK___BLANK_", "did__BLANK___BLANK_";
+                  "reward_r1_c1_90_90", "reward_r1_c1_90_90"]
         ~opp_move:"c1"
 
 
@@ -354,7 +354,7 @@
   (* regenerate ~debug:true ~game_name:"pawn_whopping" ~player:"x"; *)
   (* regenerate ~debug:false ~game_name:"connect4" ~player:"white"; *)
   regenerate ~debug:false ~game_name:"2player_normal_form_2010" ~player:"row";
-  failwith "generated";
+  (* failwith "generated"; *)
   ()
 
 let exec () =

Modified: trunk/Toss/GGP/tests/2player_normal_form_2010-raw.toss
===================================================================
--- trunk/Toss/GGP/tests/2player_normal_form_2010-raw.toss	2011-08-31 23:11:10 UTC (rev 1554)
+++ trunk/Toss/GGP/tests/2player_normal_form_2010-raw.toss	2011-09-02 13:37:14 UTC (rev 1555)
@@ -228,7 +228,6 @@
   ] -> [reward_r1_c1_90_90 |  | ]
   emb row__SYNC, column__SYNC, did_0column, did_0row, did_1c1, did_1c2,
    did_1c3, did_1r1, did_1r2, did_1r3
-  pre not terminal()
 LOC 0 {
   PLAYER Environment { PAYOFF 0. MOVES [Environment -> 0] }
   PLAYER row {

Modified: trunk/Toss/GGP/tests/2player_normal_form_2010-simpl.toss
===================================================================
--- trunk/Toss/GGP/tests/2player_normal_form_2010-simpl.toss	2011-08-31 23:11:10 UTC (rev 1554)
+++ trunk/Toss/GGP/tests/2player_normal_form_2010-simpl.toss	2011-09-02 13:37:14 UTC (rev 1555)
@@ -108,9 +108,10 @@
   emb column__SYNC, did_0column, did_0row, did_1c1, did_1c2, did_1c3,
    did_1r1, did_1r2, did_1r3, row__SYNC
   pre
-   ex reward_r3_m0_r_r0
-    (reward_0r3(reward_r3_m0_r_r0) and
-     not did__BLANK___BLANK_(reward_r3_m0_r_r0))
+   (not terminal() and
+    ex reward_r3_m0_r_r0
+     (reward_0r3(reward_r3_m0_r_r0) and
+      not did__BLANK___BLANK_(reward_r3_m0_r_r0)))
 RULE r2:
  [did__BLANK___BLANK_, reward_r1_c1_90_90 |
     _opt_column__SYNC {did__BLANK___BLANK_; reward_r1_c1_90_90};
@@ -135,9 +136,10 @@
   emb column__SYNC, did_0column, did_0row, did_1c1, did_1c2, did_1c3,
    did_1r1, did_1r2, did_1r3, row__SYNC
   pre
-   ex reward_r2_m0_r_r0
-    (reward_0r2(reward_r2_m0_r_r0) and
-     not did__BLANK___BLANK_(reward_r2_m0_r_r0))
+   (not terminal() and
+    ex reward_r2_m0_r_r0
+     (reward_0r2(reward_r2_m0_r_r0) and
+      not did__BLANK___BLANK_(reward_r2_m0_r_r0)))
 RULE r1:
  [did__BLANK___BLANK_, reward_r1_c1_90_90 |
     _opt_column__SYNC {did__BLANK___BLANK_; reward_r1_c1_90_90};
@@ -162,9 +164,10 @@
   emb column__SYNC, did_0column, did_0row, did_1c1, did_1c2, did_1c3,
    did_1r1, did_1r2, did_1r3, row__SYNC
   pre
-   ex reward_r1_m0_r_r0
-    (reward_0r1(reward_r1_m0_r_r0) and
-     not did__BLANK___BLANK_(reward_r1_m0_r_r0))
+   (not terminal() and
+    ex reward_r1_m0_r_r0
+     (reward_0r1(reward_r1_m0_r_r0) and
+      not did__BLANK___BLANK_(reward_r1_m0_r_r0)))
 RULE c3:
  [did__BLANK___BLANK_, reward_r1_c1_90_90 |
     _opt_column__SYNC {did__BLANK___BLANK_; reward_r1_c1_90_90};
@@ -189,9 +192,10 @@
   emb column__SYNC, did_0column, did_0row, did_1c1, did_1c2, did_1c3,
    did_1r1, did_1r2, did_1r3, row__SYNC
   pre
-   ex reward_m1_c3_r1_r2
-    (reward_1c3(reward_m1_c3_r1_r2) and
-     not did__BLANK___BLANK_(reward_m1_c3_r1_r2))
+   (not terminal() and
+    ex reward_m1_c3_r1_r2
+     (reward_1c3(reward_m1_c3_r1_r2) and
+      not did__BLANK___BLANK_(reward_m1_c3_r1_r2)))
 RULE c2:
  [did__BLANK___BLANK_, reward_r1_c1_90_90 |
     _opt_column__SYNC {did__BLANK___BLANK_; reward_r1_c1_90_90};
@@ -216,9 +220,10 @@
   emb column__SYNC, did_0column, did_0row, did_1c1, did_1c2, did_1c3,
    did_1r1, did_1r2, did_1r3, row__SYNC
   pre
-   ex reward_m1_c2_r1_r2
-    (reward_1c2(reward_m1_c2_r1_r2) and
-     not did__BLANK___BLANK_(reward_m1_c2_r1_r2))
+   (not terminal() and
+    ex reward_m1_c2_r1_r2
+     (reward_1c2(reward_m1_c2_r1_r2) and
+      not did__BLANK___BLANK_(reward_m1_c2_r1_r2)))
 RULE c1:
  [did__BLANK___BLANK_, reward_r1_c1_90_90 |
     _opt_column__SYNC {did__BLANK___BLANK_; reward_r1_c1_90_90};
@@ -243,9 +248,10 @@
   emb column__SYNC, did_0column, did_0row, did_1c1, did_1c2, did_1c3,
    did_1r1, did_1r2, did_1r3, row__SYNC
   pre
-   ex reward_m1_c1_r1_r2
-    (reward_1c1(reward_m1_c1_r1_r2) and
-     not did__BLANK___BLANK_(reward_m1_c1_r1_r2))
+   (not terminal() and
+    ex reward_m1_c1_r1_r2
+     (reward_1c1(reward_m1_c1_r1_r2) and
+      not did__BLANK___BLANK_(reward_m1_c1_r1_r2)))
 RULE Environment:
  [reward_r1_c1_90_90 |
     _opt_did_0column (reward_r1_c1_90_90);

Modified: trunk/Toss/GGP/tests/connect5-raw.toss
===================================================================
--- trunk/Toss/GGP/tests/connect5-raw.toss	2011-08-31 23:11:10 UTC (rev 1554)
+++ trunk/Toss/GGP/tests/connect5-raw.toss	2011-09-02 13:37:14 UTC (rev 1555)
@@ -1,45 +1,249 @@
-REL adjacent_cell(v0, v1, v2, v3) =
- ex cell_x22__BLANK___BLANK_, cell_y22__BLANK___BLANK_,
-  cell_x23__BLANK___BLANK_, cell_y23__BLANK___BLANK_
-  (v0 = cell_x22__BLANK___BLANK_ and v1 = cell_y22__BLANK___BLANK_ and
-    v2 = cell_x23__BLANK___BLANK_ and v3 = cell_y23__BLANK___BLANK_ and
-   adjacent__cell_0__cell_0(cell_x22__BLANK___BLANK_,
-    cell_x23__BLANK___BLANK_) and
-    adjacent__cell_0__cell_0(cell_y22__BLANK___BLANK_,
-    cell_y23__BLANK___BLANK_) and
-   cell__BLANK___BLANK___BLANK_(cell_x22__BLANK___BLANK_) and
-    cell__BLANK___BLANK___BLANK_(cell_y22__BLANK___BLANK_) and
-    cell__BLANK___BLANK___BLANK_(cell_x23__BLANK___BLANK_) and
-    cell__BLANK___BLANK___BLANK_(cell_y23__BLANK___BLANK_)) or
-  ex cell_x20__BLANK___BLANK_, cell_y21__BLANK___BLANK_,
-   cell_x21__BLANK___BLANK_, cell_y21__BLANK___BLANK_
-   (v0 = cell_x20__BLANK___BLANK_ and v1 = cell_y21__BLANK___BLANK_ and
-     v2 = cell_x21__BLANK___BLANK_ and v3 = cell_y21__BLANK___BLANK_ and
-    adjacent__cell_0__cell_0(cell_x20__BLANK___BLANK_,
-     cell_x21__BLANK___BLANK_) and
-     coordinate__cell_0(cell_y21__BLANK___BLANK_) and
-     coordinate__cell_0(cell_y21__BLANK___BLANK_) and
-    cell__BLANK___BLANK___BLANK_(cell_x20__BLANK___BLANK_) and
-     cell__BLANK___BLANK___BLANK_(cell_y21__BLANK___BLANK_) and
-     cell__BLANK___BLANK___BLANK_(cell_x21__BLANK___BLANK_) and
-     cell__BLANK___BLANK___BLANK_(cell_y21__BLANK___BLANK_)) or
-  ex cell_x19__BLANK___BLANK_, cell_y19__BLANK___BLANK_,
-   cell_x19__BLANK___BLANK_, cell_y20__BLANK___BLANK_
-   (v0 = cell_x19__BLANK___BLANK_ and v1 = cell_y19__BLANK___BLANK_ and
-     v2 = cell_x19__BLANK___BLANK_ and v3 = cell_y20__BLANK___BLANK_ and
-    adjacent__cell_0__cell_0(cell_y19__BLANK___BLANK_,
-     cell_y20__BLANK___BLANK_) and
-     coordinate__cell_0(cell_x19__BLANK___BLANK_) and
-     coordinate__cell_0(cell_x19__BLANK___BLANK_) and
-    cell__BLANK___BLANK___BLANK_(cell_x19__BLANK___BLANK_) and
-     cell__BLANK___BLANK___BLANK_(cell_y19__BLANK___BLANK_) and
-     cell__BLANK___BLANK___BLANK_(cell_x19__BLANK___BLANK_) and
-     cell__BLANK___BLANK___BLANK_(cell_y20__BLANK___BLANK_))
-REL col__b() =
+REL row__x() =
+ ex cell_a_y8__BLANK_, cell_b_y8__BLANK_, cell_c1_y8__BLANK_,
+  cell_d_y8__BLANK_, cell_e_y8__BLANK_
+  (nextcol__cell_0__cell_0(cell_a_y8__BLANK_, cell_b_y8__BLANK_) and
+    nextcol__cell_0__cell_0(cell_b_y8__BLANK_, cell_c1_y8__BLANK_) and
+    nextcol__cell_0__cell_0(cell_c1_y8__BLANK_, cell_d_y8__BLANK_) and
+    nextcol__cell_0__cell_0(cell_d_y8__BLANK_, cell_e_y8__BLANK_) and
+    EQ___cell_1__cell_1(cell_a_y8__BLANK_, cell_b_y8__BLANK_) and
+    EQ___cell_1__cell_1(cell_a_y8__BLANK_, cell_c1_y8__BLANK_) and
+    EQ___cell_1__cell_1(cell_a_y8__BLANK_, cell_d_y8__BLANK_) and
+    EQ___cell_1__cell_1(cell_a_y8__BLANK_, cell_e_y8__BLANK_) and
+    EQ___cell_1__cell_1(cell_b_y8__BLANK_, cell_a_y8__BLANK_) and
+    EQ___cell_1__cell_1(cell_b_y8__BLANK_, cell_c1_y8__BLANK_) and
+    EQ___cell_1__cell_1(cell_b_y8__BLANK_, cell_d_y8__BLANK_) and
+    EQ___cell_1__cell_1(cell_b_y8__BLANK_, cell_e_y8__BLANK_) and
+    EQ___cell_1__cell_1(cell_c1_y8__BLANK_, cell_a_y8__BLANK_) and
+    EQ___cell_1__cell_1(cell_c1_y8__BLANK_, cell_b_y8__BLANK_) and
+    EQ___cell_1__cell_1(cell_c1_y8__BLANK_, cell_d_y8__BLANK_) and
+    EQ___cell_1__cell_1(cell_c1_y8__BLANK_, cell_e_y8__BLANK_) and
+    EQ___cell_1__cell_1(cell_d_y8__BLANK_, cell_a_y8__BLANK_) and
+    EQ___cell_1__cell_1(cell_d_y8__BLANK_, cell_b_y8__BLANK_) and
+    EQ___cell_1__cell_1(cell_d_y8__BLANK_, cell_c1_y8__BLANK_) and
+    EQ___cell_1__cell_1(cell_d_y8__BLANK_, cell_e_y8__BLANK_) and
+    EQ___cell_1__cell_1(cell_e_y8__BLANK_, cell_a_y8__BLANK_) and
+    EQ___cell_1__cell_1(cell_e_y8__BLANK_, cell_b_y8__BLANK_) and
+    EQ___cell_1__cell_1(cell_e_y8__BLANK_, cell_c1_y8__BLANK_) and
+    EQ___cell_1__cell_1(cell_e_y8__BLANK_, cell_d_y8__BLANK_) and
+   cell_2x(cell_a_y8__BLANK_) and
+    cell__BLANK___BLANK___BLANK_(cell_a_y8__BLANK_) and
+    cell_2x(cell_b_y8__BLANK_) and
+     cell__BLANK___BLANK___BLANK_(cell_b_y8__BLANK_) and
+    cell_2x(cell_c1_y8__BLANK_) and
+     cell__BLANK___BLANK___BLANK_(cell_c1_y8__BLANK_) and
+    cell_2x(cell_d_y8__BLANK_) and
+     cell__BLANK___BLANK___BLANK_(cell_d_y8__BLANK_) and
+    cell_2x(cell_e_y8__BLANK_) and
+     cell__BLANK___BLANK___BLANK_(cell_e_y8__BLANK_))
+REL row__o() =
+ ex cell_a_y8__BLANK_, cell_b_y8__BLANK_, cell_c1_y8__BLANK_,
+  cell_d_y8__BLANK_, cell_e_y8__BLANK_
+  (nextcol__cell_0__cell_0(cell_a_y8__BLANK_, cell_b_y8__BLANK_) and
+    nextcol__cell_0__cell_0(cell_b_y8__BLANK_, cell_c1_y8__BLANK_) and
+    nextcol__cell_0__cell_0(cell_c1_y8__BLANK_, cell_d_y8__BLANK_) and
+    nextcol__cell_0__cell_0(cell_d_y8__BLANK_, cell_e_y8__BLANK_) and
+    EQ___cell_1__cell_1(cell_a_y8__BLANK_, cell_b_y8__BLANK_) and
+    EQ___cell_1__cell_1(cell_a_y8__BLANK_, cell_c1_y8__BLANK_) and
+    EQ___cell_1__cell_1(cell_a_y8__BLANK_, cell_d_y8__BLANK_) and
+    EQ___cell_1__cell_1(cell_a_y8__BLANK_, cell_e_y8__BLANK_) and
+    EQ___cell_1__cell_1(cell_b_y8__BLANK_, cell_a_y8__BLANK_) and
+    EQ___cell_1__cell_1(cell_b_y8__BLANK_, cell_c1_y8__BLANK_) and
+    EQ___cell_1__cell_1(cell_b_y8__BLANK_, cell_d_y8__BLANK_) and
+    EQ___cell_1__cell_1(cell_b_y8__BLANK_, cell_e_y8__BLANK_) and
+    EQ___cell_1__cell_1(cell_c1_y8__BLANK_, cell_a_y8__BLANK_) and
+    EQ___cell_1__cell_1(cell_c1_y8__BLANK_, cell_b_y8__BLANK_) and
+    EQ___cell_1__cell_1(cell_c1_y8__BLANK_, cell_d_y8__BLANK_) and
+    EQ___cell_1__cell_1(cell_c1_y8__BLANK_, cell_e_y8__BLANK_) and
+    EQ___cell_1__cell_1(cell_d_y8__BLANK_, cell_a_y8__BLANK_) and
+    EQ___cell_1__cell_1(cell_d_y8__BLANK_, cell_b_y8__BLANK_) and
+    EQ___cell_1__cell_1(cell_d_y8__BLANK_, cell_c1_y8__BLANK_) and
+    EQ___cell_1__cell_1(cell_d_y8__BLANK_, cell_e_y8__BLANK_) and
+    EQ___cell_1__cell_1(cell_e_y8__BLANK_, cell_a_y8__BLANK_) and
+    EQ___cell_1__cell_1(cell_e_y8__BLANK_, cell_b_y8__BLANK_) and
+    EQ___cell_1__cell_1(cell_e_y8__BLANK_, cell_c1_y8__BLANK_) and
+    EQ___cell_1__cell_1(cell_e_y8__BLANK_, cell_d_y8__BLANK_) and
+   cell_2o(cell_a_y8__BLANK_) and
+    cell__BLANK___BLANK___BLANK_(cell_a_y8__BLANK_) and
+    cell_2o(cell_b_y8__BLANK_) and
+     cell__BLANK___BLANK___BLANK_(cell_b_y8__BLANK_) and
+    cell_2o(cell_c1_y8__BLANK_) and
+     cell__BLANK___BLANK___BLANK_(cell_c1_y8__BLANK_) and
+    cell_2o(cell_d_y8__BLANK_) and
+     cell__BLANK___BLANK___BLANK_(cell_d_y8__BLANK_) and
+    cell_2o(cell_e_y8__BLANK_) and
+     cell__BLANK___BLANK___BLANK_(cell_e_y8__BLANK_))
+REL row__b() =
+ ex cell_a_y8__BLANK_, cell_b_y8__BLANK_, cell_c1_y8__BLANK_,
+  cell_d_y8__BLANK_, cell_e_y8__BLANK_
+  (nextcol__cell_0__cell_0(cell_a_y8__BLANK_, cell_b_y8__BLANK_) and
+    nextcol__cell_0__cell_0(cell_b_y8__BLANK_, cell_c1_y8__BLANK_) and
+    nextcol__cell_0__cell_0(cell_c1_y8__BLANK_, cell_d_y8__BLANK_) and
+    nextcol__cell_0__cell_0(cell_d_y8__BLANK_, cell_e_y8__BLANK_) and
+    EQ___cell_1__cell_1(cell_a_y8__BLANK_, cell_b_y8__BLANK_) and
+    EQ___cell_1__cell_1(cell_a_y8__BLANK_, cell_c1_y8__BLANK_) and
+    EQ___cell_1__cell_1(cell_a_y8__BLANK_, cell_d_y8__BLANK_) and
+    EQ___cell_1__cell_1(cell_a_y8__BLANK_, cell_e_y8__BLANK_) and
+    EQ___cell_1__cell_1(cell_b_y8__BLANK_, cell_a_y8__BLANK_) and
+    EQ___cell_1__cell_1(cell_b_y8__BLANK_, cell_c1_y8__BLANK_) and
+    EQ___cell_1__cell_1(cell_b_y8__BLANK_, cell_d_y8__BLANK_) and
+    EQ___cell_1__cell_1(cell_b_y8__BLANK_, cell_e_y8__BLANK_) and
+    EQ___cell_1__cell_1(cell_c1_y8__BLANK_, cell_a_y8__BLANK_) and
+    EQ___cell_1__cell_1(cell_c1_y8__BLANK_, cell_b_y8__BLANK_) and
+    EQ___cell_1__cell_1(cell_c1_y8__BLANK_, cell_d_y8__BLANK_) and
+    EQ___cell_1__cell_1(cell_c1_y8__BLANK_, cell_e_y8__BLANK_) and
+    EQ___cell_1__cell_1(cell_d_y8__BLANK_, cell_a_y8__BLANK_) and
+    EQ___cell_1__cell_1(cell_d_y8__BLANK_, cell_b_y8__BLANK_) and
+    EQ___cell_1__cell_1(cell_d_y8__BLANK_, cell_c1_y8__BLANK_) and
+    EQ___cell_1__cell_1(cell_d_y8__BLANK_, cell_e_y8__BLANK_) and
+    EQ___cell_1__cell_1(cell_e_y8__BLANK_, cell_a_y8__BLANK_) and
+    EQ___cell_1__cell_1(cell_e_y8__BLANK_, cell_b_y8__BLANK_) and
+    EQ___cell_1__cell_1(cell_e_y8__BLANK_, cell_c1_y8__BLANK_) and
+    EQ___cell_1__cell_1(cell_e_y8__BLANK_, cell_d_y8__BLANK_) and
+   cell_2b(cell_a_y8__BLANK_) and
+    cell__BLANK___BLANK___BLANK_(cell_a_y8__BLANK_) and
+    cell_2b(cell_b_y8__BLANK_) and
+     cell__BLANK___BLANK___BLANK_(cell_b_y8__BLANK_) and
+    cell_2b(cell_c1_y8__BLANK_) and
+     cell__BLANK___BLANK___BLANK_(cell_c1_y8__BLANK_) and
+    cell_2b(cell_d_y8__BLANK_) and
+     cell__BLANK___BLANK___BLANK_(cell_d_y8__BLANK_) and
+    cell_2b(cell_e_y8__BLANK_) and
+     cell__BLANK___BLANK___BLANK_(cell_e_y8__BLANK_))
+REL exists_empty_cell() =
+ ex cell_x7_y7__BLANK_
+  (true and
+   cell_2b(cell_x7_y7__BLANK_) and
+    cell__BLANK___BLANK___BLANK_(cell_x7_y7__BLANK_))
+REL diag2__x() =
+ ex cell_x14_y18__BLANK_, cell_x15_y17__BLANK_, cell_x16_y16__BLANK_,
+  cell_x17_y15__BLANK_, cell_x18_y14__BLANK_
+  (nextcol__cell_0__cell_0(cell_x14_y18__BLANK_, cell_x15_y17__BLANK_) and
+    nextcol__cell_1__cell_1(cell_x15_y17__BLANK_, cell_x14_y18__BLANK_) and
+    nextcol__cell_0__cell_0(cell_x15_y17__BLANK_, cell_x16_y16__BLANK_) and
+    nextcol__cell_1__cell_1(cell_x16_y16__BLANK_, cell_x15_y17__BLANK_) and
+    nextcol__cell_0__cell_0(cell_x16_y16__BLANK_, cell_x17_y15__BLANK_) and
+    nextcol__cell_1__cell_1(cell_x17_y15__BLANK_, cell_x16_y16__BLANK_) and
+    nextcol__cell_0__cell_0(cell_x17_y15__BLANK_, cell_x18_y14__BLANK_) and
+    nextcol__cell_1__cell_1(cell_x18_y14__BLANK_, cell_x17_y15__BLANK_) and
+   cell_2x(cell_x14_y18__BLANK_) and
+    cell__BLANK___BLANK___BLANK_(cell_x14_y18__BLANK_) and
+    cell_2x(cell_x15_y17__BLANK_) and
+     cell__BLANK___BLANK___BLANK_(cell_x15_y17__BLANK_) and
+    cell_2x(cell_x16_y16__BLANK_) and
+     cell__BLANK___BLANK___BLANK_(cell_x16_y16__BLANK_) and
+    cell_2x(cell_x17_y15__BLANK_) and
+     cell__BLANK___BLANK___BLANK_(cell_x17_y15__BLANK_) and
+    cell_2x(cell_x18_y14__BLANK_) and
+     cell__BLANK___BLANK___BLANK_(cell_x18_y14__BLANK_))
+REL diag2__o() =
+ ex cell_x14_y18__BLANK_, cell_x15_y17__BLANK_, cell_x16_y16__BLANK_,
+  cell_x17_y15__BLANK_, cell_x18_y14__BLANK_
+  (nextcol__cell_0__cell_0(cell_x14_y18__BLANK_, cell_x15_y17__BLANK_) and
+    nextcol__cell_1__cell_1(cell_x15_y17__BLANK_, cell_x14_y18__BLANK_) and
+    nextcol__cell_0__cell_0(cell_x15_y17__BLANK_, cell_x16_y16__BLANK_) and
+    nextcol__cell_1__cell_1(cell_x16_y16__BLANK_, cell_x15_y17__BLANK_) and
+    nextcol__cell_0__cell_0(cell_x16_y16__BLANK_, cell_x17_y15__BLANK_) and
+    nextcol__cell_1__cell_1(cell_x17_y15__BLANK_, cell_x16_y16__BLANK_) and
+    nextcol__cell_0__cell_0(cell_x17_y15__BLANK_, cell_x18_y14__BLANK_) and
+    nextcol__cell_1__cell_1(cell_x18_y14__BLANK_, cell_x17_y15__BLANK_) and
+   cell_2o(cell_x14_y18__BLANK_) and
+    cell__BLANK___BLANK___BLANK_(cell_x14_y18__BLANK_) and
+    cell_2o(cell_x15_y17__BLANK_) and
+     cell__BLANK___BLANK___BLANK_(cell_x15_y17__BLANK_) and
+    cell_2o(cell_x16_y16__BLANK_) and
+     cell__BLANK___BLANK___BLANK_(cell_x16_y16__BLANK_) and
+    cell_2o(cell_x17_y15__BLANK_) and
+     cell__BLANK___BLANK___BLANK_(cell_x17_y15__BLANK_) and
+    cell_2o(cell_x18_y14__BLANK_) and
+     cell__BLANK___BLANK___BLANK_(cell_x18_y14__BLANK_))
+REL diag2__b() =
+ ex cell_x14_y18__BLANK_, cell_x15_y17__BLANK_, cell_x16_y16__BLANK_,
+  cell_x17_y15__BLANK_, cell_x18_y14__BLANK_
+  (nextcol__cell_0__cell_0(cell_x14_y18__BLANK_, cell_x15_y17__BLANK_) and
+    nextcol__cell_1__cell_1(cell_x15_y17__BLANK_, cell_x14_y18__BLANK_) and
+    nextcol__cell_0__cell_0(cell_x15_y17__BLANK_, cell_x16_y16__BLANK_) and
+    nextcol__cell_1__cell_1(cell_x16_y16__BLANK_, cell_x15_y17__BLANK_) and
+    nextcol__cell_0__cell_0(cell_x16_y16__BLANK_, cell_x17_y15__BLANK_) and
+    nextcol__cell_1__cell_1(cell_x17_y15__BLANK_, cell_x16_y16__BLANK_) and
+    nextcol__cell_0__cell_0(cell_x17_y15__BLANK_, cell_x18_y14__BLANK_) and
+    nextcol__cell_1__cell_1(cell_x18_y14__BLANK_, cell_x17_y15__BLANK_) and
+   cell_2b(cell_x14_y18__BLANK_) and
+    cell__BLANK___BLANK___BLANK_(cell_x14_y18__BLANK_) and
+    cell_2b(cell_x15_y17__BLANK_) and
+     cell__BLANK___BLANK___BLANK_(cell_x15_y17__BLANK_) and
+    cell_2b(cell_x16_y16__BLANK_) and
+     cell__BLANK___BLANK___BLANK_(cell_x16_y16__BLANK_) and
+    cell_2b(cell_x17_y15__BLANK_) and
+     cell__BLANK___BLANK___BLANK_(cell_x17_y15__BLANK_) and
+    cell_2b(cell_x18_y14__BLANK_) and
+     cell__BLANK___BLANK___BLANK_(cell_x18_y14__BLANK_))
+REL diag1__x() =
+ ex cell_x9_y9__BLANK_, cell_x10_y10__BLANK_, cell_x11_y11__BLANK_,
+  cell_x12_y12__BLANK_, cell_x13_y13__BLANK_
+  (nextcol__cell_0__cell_0(cell_x9_y9__BLANK_, cell_x10_y10__BLANK_) and
+    nextcol__cell_1__cell_1(cell_x9_y9__BLANK_, cell_x10_y10__BLANK_) and
+    nextcol__cell_0__cell_0(cell_x10_y10__BLANK_, cell_x11_y11__BLANK_) and
+    nextcol__cell_1__cell_1(cell_x10_y10__BLANK_, cell_x11_y11__BLANK_) and
+    nextcol__cell_0__cell_0(cell_x11_y11__BLANK_, cell_x12_y12__BLANK_) and
+    nextcol__cell_1__cell_1(cell_x11_y11__BLANK_, cell_x12_y12__BLANK_) and
+    nextcol__cell_0__cell_0(cell_x12_y12__BLANK_, cell_x13_y13__BLANK_) and
+    nextcol__cell_1__cell_1(cell_x12_y12__BLANK_, cell_x13_y13__BLANK_) and
+   cell_2x(cell_x9_y9__BLANK_) and
+    cell__BLANK___BLANK___BLANK_(cell_x9_y9__BLANK_) and
+    cell_2x(cell_x10_y10__BLANK_) and
+     cell__BLANK___BLANK___BLANK_(cell_x10_y10__BLANK_) and
+    cell_2x(cell_x11_y11__BLANK_) and
+     cell__BLANK___BLANK___BLANK_(cell_x11_y11__BLANK_) and
+    cell_2x(cell_x12_y12__BLANK_) and
+     cell__BLANK___BLANK___BLANK_(cell_x12_y12__BLANK_) and
+    cell_2x(cell_x13_y13__BLANK_) and
+     cell__BLANK___BLANK___BLANK_(cell_x13_y13__BLANK_))
+REL diag1__o() =
+ ex cell_x9_y9__BLANK_, cell_x10_y10__BLANK_, cell_x11_y11__BLANK_,
+  cell_x12_y12__BLANK_, cell_x13_y13__BLANK_
+  (nextcol__cell_0__cell_0(cell_x9_y9__BLANK_, cell_x10_y10__BLANK_) and
+    nextcol__cell_1__cell_1(cell_x9_y9__BLANK_, cell_x10_y10__BLANK_) and
+    nextcol__cell_0__cell_0(cell_x10_y10__BLANK_, cell_x11_y11__BLANK_) and
+    nextcol__cell_1__cell_1(cell_x10_y10__BLANK_, cell_x11_y11__BLANK_) and
+    nextcol__cell_0__cell_0(cell_x11_y11__BLANK_, cell_x12_y12__BLANK_) and
+    nextcol__cell_1__cell_1(cell_x11_y11__BLANK_, cell_x12_y12__BLANK_) and
+    nextcol__cell_0__cell_0(cell_x12_y12__BLANK_, cell_x13_y13__BLANK_) and
+    nextcol__cell_1__cell_1(cell_x12_y12__BLANK_, cell_x13_y13__BLANK_) and
+   cell_2o(cell_x9_y9__BLANK_) and
+    cell__BLANK___BLANK___BLANK_(cell_x9_y9__BLANK_) and
+    cell_2o(cell_x10_y10__BLANK_) and
+     cell__BLANK___BLANK___BLANK_(cell_x10_y10__BLANK_) and
+    cell_2o(cell_x11_y11__BLANK_) and
+     cell__BLANK___BLANK___BLANK_(cell_x11_y11__BLANK_) and
+    cell_2o(cell_x12_y12__BLANK_) and
+     cell__BLANK___BLANK___BLANK_(cell_x12_y12__BLANK_) and
+    cell_2o(cell_x13_y13__BLANK_) and
+     cell__BLANK___BLANK___BLANK_(cell_x13_y13__BLANK_))
+REL diag1__b() =
+ ex cell_x9_y9__BLANK_, cell_x10_y10__BLANK_, cell_x11_y11__BLANK_,
+  cell_x12_y12__BLANK_, cell_x13_y13__BLANK_
+  (nextcol__cell_0__cell_0(cell_x9_y9__BLANK_, cell_x10_y10__BLANK_) and
+    nextcol__cell_1__cell_1(cell_x9_y9__BLANK_, cell_x10_y10__BLANK_) and
+    nextcol__cell_0__cell_0(cell_x10_y10__BLANK_, cell_x11_y11__BLANK_) and
+    nextcol__cell_1__cell_1(cell_x10_y10__BLANK_, cell_x11_y11__BLANK_) and
+    nextcol__cell_0__cell_0(cell_x11_y11__BLANK_, cell_x12_y12__BLANK_) and
+    nextcol__cell_1__cell_1(cell_x11_y11__BLANK_, cell_x12_y12__BLANK_) and
+    nextcol__cell_0__cell_0(cell_x12_y12__BLANK_, cell_x13_y13__BLANK_) and
+    nextcol__cell_1__cell_1(cell_x12_y12__BLANK_, cell_x13_y13__BLANK_) and
+   cell_2b(cell_x9_y9__BLANK_) and
+    cell__BLANK___BLANK___BLANK_(cell_x9_y9__BLANK_) and
+    cell_2b(cell_x10_y10__BLANK_) and
+     cell__BLANK___BLANK___BLANK_(cell_x10_y10__BLANK_) and
+    cell_2b(cell_x11_y11__BLANK_) and
+     cell__BLANK___BLANK___BLANK_(cell_x11_y11__BLANK_) and
+    cell_2b(cell_x12_y12__BLANK_) and
+     cell__BLANK___BLANK___BLANK_(cell_x12_y12__BLANK_) and
+    cell_2b(cell_x13_y13__BLANK_) and
+     cell__BLANK___BLANK___BLANK_(cell_x13_y13__BLANK_))
+REL col__x() =
  ex cell_x8_a0__BLANK_, cell_x8_b0__BLANK_, cell_x8_c2__BLANK_,
   cell_x8_d0__BLANK_, cell_x8_e0__BLANK_
-  (true and
-   nextcol__cell_1__cell_1(cell_x8_a0__BLANK_, cell_x8_b0__BLANK_) and
+  (nextcol__cell_1__cell_1(cell_x8_a0__BLANK_, cell_x8_b0__BLANK_) and
     nextcol__cell_1__cell_1(cell_x8_b0__BLANK_, cell_x8_c2__BLANK_) and
     nextcol__cell_1__cell_1(cell_x8_c2__BLANK_, cell_x8_d0__BLANK_) and
     nextcol__cell_1__cell_1(cell_x8_d0__BLANK_, cell_x8_e0__BLANK_) and
@@ -63,21 +267,20 @@
     EQ___cell_0__cell_0(cell_x8_e0__BLANK_, cell_x8_b0__BLANK_) and
     EQ___cell_0__cell_0(cell_x8_e0__BLANK_, cell_x8_c2__BLANK_) and
     EQ___cell_0__cell_0(cell_x8_e0__BLANK_, cell_x8_d0__BLANK_) and
-   cell_2b(cell_x8_a0__BLANK_) and
+   cell_2x(cell_x8_a0__BLANK_) and
     cell__BLANK___BLANK___BLANK_(cell_x8_a0__BLANK_) and
-    cell_2b(cell_x8_b0__BLANK_) and
+    cell_2x(cell_x8_b0__BLANK_) and
      cell__BLANK___BLANK___BLANK_(cell_x8_b0__BLANK_) and
-    cell_2b(cell_x8_c2__BLANK_) and
+    cell_2x(cell_x8_c2__BLANK_) and
      cell__BLANK___BLANK___BLANK_(cell_x8_c2__BLANK_) and
-    cell_2b(cell_x8_d0__BLANK_) and
+    cell_2x(cell_x8_d0__BLANK_) and
      cell__BLANK___BLANK___BLANK_(cell_x8_d0__BLANK_) and
-    cell_2b(cell_x8_e0__BLANK_) and
+    cell_2x(cell_x8_e0__BLANK_) and
      cell__BLANK___BLANK___BLANK_(cell_x8_e0__BLANK_))
 REL col__o() =
  ex cell_x8_a0__BLANK_, cell_x8_b0__BLANK_, cell_x8_c2__BLANK_,
   cell_x8_d0__BLANK_, cell_x8_e0__BLANK_
-  (true and
-   nextcol__cell_1__cell_1(cell_x8_a0__BLANK_, cell_x8_b0__BLANK_) and
+  (nextcol__cell_1__cell_1(cell_x8_a0__BLANK_, cell_x8_b0__BLANK_) and
     nextcol__cell_1__cell_1(cell_x8_b0__BLANK_, cell_x8_c2__BLANK_) and
     nextcol__cell_1__cell_1(cell_x8_c2__BLANK_, cell_x8_d0__BLANK_) and
     nextcol__cell_1__cell_1(cell_x8_d0__BLANK_, cell_x8_e0__BLANK_) and
@@ -111,11 +314,10 @@
      cell__BLANK___BLANK___BLANK_(cell_x8_d0__BLANK_) and
     cell_2o(cell_x8_e0__BLANK_) and
      cell__BLANK___BLANK___BLANK_(cell_x8_e0__BLANK_))
-REL col__x() =
+REL col__b() =
  ex cell_x8_a0__BLANK_, cell_x8_b0__BLANK_, cell_x8_c2__BLANK_,
   cell_x8_d0__BLANK_, cell_x8_e0__BLANK_
-  (true and
-   nextcol__cell_1__cell_1(cell_x8_a0__BLANK_, cell_x8_b0__BLANK_) and
+  (nextcol__cell_1__cell_1(cell_x8_a0__BLANK_, cell_x8_b0__BLANK_) and
     nextcol__cell_1__cell_1(cell_x8_b0__BLANK_, cell_x8_c2__BLANK_) and
     nextcol__cell_1__cell_1(cell_x8_c2__BLANK_, cell_x8_d0__BLANK_) and
     nextcol__cell_1__cell_1(cell_x8_d0__BLANK_, cell_x8_e0__BLANK_) and
@@ -139,278 +341,71 @@
     EQ___cell_0__cell_0(cell_x8_e0__BLANK_, cell_x8_b0__BLANK_) and
     EQ___cell_0__cell_0(cell_x8_e0__BLANK_, cell_x8_c2__BLANK_) and
     EQ___cell_0__cell_0(cell_x8_e0__BLANK_, cell_x8_d0__BLANK_) and
-   cell_2x(cell_x8_a0__BLANK_) and
+   cell_2b(cell_x8_a0__BLANK_) and
     cell__BLANK___BLANK___BLANK_(cell_x8_a0__BLANK_) and
-    cell_2x(cell_x8_b0__BLANK_) and
+    cell_2b(cell_x8_b0__BLANK_) and
      cell__BLANK___BLANK___BLANK_(cell_x8_b0__BLANK_) and
-    cell_2x(cell_x8_c2__BLANK_) and
+    cell_2b(cell_x8_c2__BLANK_) and
      cell__BLANK___BLANK___BLANK_(cell_x8_c2__BLANK_) and
-    cell_2x(cell_x8_d0__BLANK_) and
+    cell_2b(cell_x8_d0__BLANK_) and
      cell__BLANK___BLANK___BLANK_(cell_x8_d0__BLANK_) and
-    cell_2x(cell_x8_e0__BLANK_) and
+    cell_2b(cell_x8_e0__BLANK_) and
      cell__BLANK___BLANK___BLANK_(cell_x8_e0__BLANK_))
-REL conn5__b() =
- (true and (col__b() or row__b() or diag1__b() or diag2__b()) and true)
-REL conn5__o() =
- (true and (col__o() or row__o() or diag1__o() or diag2__o()) and true)
+REL adjacent(v0, v1) =
+ ex cell_x24__BLANK___BLANK_, cell_y24__BLANK___BLANK_
+  (v0 = cell_x24__BLANK___BLANK_ and v1 = cell_y24__BLANK___BLANK_ and
+   nextcol__cell_0__cell_0(cell_x24__BLANK___BLANK_,
+    cell_y24__BLANK___BLANK_) and
+    cell__BLANK___BLANK___BLANK_(cell_y24__BLANK___BLANK_) and
+     cell__BLANK___BLANK___BLANK_(cell_x24__BLANK___BLANK_)) or
+  ex cell_x25__BLANK___BLANK_, cell_y25__BLANK___BLANK_
+   (v0 = cell_x25__BLANK___BLANK_ and v1 = cell_y25__BLANK___BLANK_ and
+    nextcol__cell_0__cell_0(cell_y25__BLANK___BLANK_,
+     cell_x25__BLANK___BLANK_) and
+     cell__BLANK___BLANK___BLANK_(cell_y25__BLANK___BLANK_) and
+      cell__BLANK___BLANK___BLANK_(cell_x25__BLANK___BLANK_))
 REL conn5__x() =
- (true and (col__x() or row__x() or diag1__x() or diag2__x()) and true)
-REL diag1__b() =
- ex cell_x9_y9__BLANK_, cell_x10_y10__BLANK_, cell_x11_y11__BLANK_,
-  cell_x12_y12__BLANK_, cell_x13_y13__BLANK_
-  (true and
-   nextcol__cell_0__cell_0(cell_x9_y9__BLANK_, cell_x10_y10__BLANK_) and
-    nextcol__cell_1__cell_1(cell_x9_y9__BLANK_, cell_x10_y10__BLANK_) and
-    nextcol__cell_0__cell_0(cell_x10_y10__BLANK_, cell_x11_y11__BLANK_) and
-    nextcol__cell_1__cell_1(cell_x10_y10__BLANK_, cell_x11_y11__BLANK_) and
-    nextcol__cell_0__cell_0(cell_x11_y11__BLANK_, cell_x12_y12__BLANK_) and
-    nextcol__cell_1__cell_1(cell_x11_y11__BLANK_, cell_x12_y12__BLANK_) and
-    nextcol__cell_0__cell_0(cell_x12_y12__BLANK_, cell_x13_y13__BLANK_) and
-    nextcol__cell_1__cell_1(cell_x12_y12__BLANK_, cell_x13_y13__BLANK_) and
-   cell_2b(cell_x9_y9__BLANK_) and
-    cell__BLANK___BLANK___BLANK_(cell_x9_y9__BLANK_) and
-    cell_2b(cell_x10_y10__BLANK_) and
-     cell__BLANK___BLANK___BLANK_(cell_x10_y10__BLANK_) and
-    cell_2b(cell_x11_y11__BLANK_) and
-     cell__BLANK___BLANK___BLANK_(cell_x11_y11__BLANK_) and
-    cell_2b(cell_x12_y12__BLANK_) and
-     cell__BLANK___BLANK___BLANK_(cell_x12_y12__BLANK_) and
-    cell_2b(cell_x13_y13__BLANK_) and
-     cell__BLANK___BLANK___BLANK_(cell_x13_y13__BLANK_))
-REL diag1__o() =
- ex cell_x9_y9__BLANK_, cell_x10_y10__BLANK_, cell_x11_y11__BLANK_,
-  cell_x12_y12__BLANK_, cell_x13_y13__BLANK_
-  (true and
-   nextcol__cell_0__cell_0(cell_x9_y9__BLANK_, cell_x10_y10__BLANK_) and
-    nextcol__cell_1__cell_1(cell_x9_y9__BLANK_, cell_x10_y10__BLANK_) and
-    nextcol__cell_0__cell_0(cell_x10_y10__BLANK_, cell_x11_y11__BLANK_) and
-    nextcol__cell_1__cell_1(cell_x10_y10__BLANK_, cell_x11_y11__BLANK_) and
-    nextcol__cell_0__cell_0(cell_x11_y11__BLANK_, cell_x12_y12__BLANK_) and
-    nextcol__cell_1__cell_1(cell_x11_y11__BLANK_, cell_x12_y12__BLANK_) and
-    nextcol__cell_0__cell_0(cell_x12_y12__BLANK_, cell_x13_y13__BLANK_) and
-    nextcol__cell_1__cell_1(cell_x12_y12__BLANK_, cell_x13_y13__BLANK_) and
-   cell_2o(cell_x9_y9__BLANK_) and
-    cell__BLANK___BLANK___BLANK_(cell_x9_y9__BLANK_) and
-    cell_2o(cell_x10_y10__BLANK_) and
-     cell__BLANK___BLANK___BLANK_(cell_x10_y10__BLANK_) and
-    cell_2o(cell_x11_y11__BLANK_) and
-     cell__BLANK___BLANK___BLANK_(cell_x11_y11__BLANK_) and
-    cell_2o(cell_x12_y12__BLANK_) and
-     cell__BLANK___BLANK___BLANK_(cell_x12_y12__BLANK_) and
-    cell_2o(cell_x13_y13__BLANK_) and
-     cell__BLANK___BLANK___BLANK_(cell_x13_y13__BLANK_))
-REL diag1__x() =
- ex cell_x9_y9__BLANK_, cell_x10_y10__BLANK_, cell_x11_y11__BLANK_,
-  cell_x12_y12__BLANK_, cell_x13_y13__BLANK_
-  (true and
-   nextcol__cell_0__cell_0(cell_x9_y9__BLANK_, cell_x10_y10__BLANK_) and
-    nextcol__cell_1__cell_1(cell_x9_y9__BLANK_, cell_x10_y10__BLANK_) and
-    nextcol__cell_0__cell_0(cell_x10_y10__BLANK_, cell_x11_y11__BLANK_) and
-    nextcol__cell_1__cell_1(cell_x10_y10__BLANK_, cell_x11_y11__BLANK_) and
-    nextcol__cell_0__cell_0(cell_x11_y11__BLANK_, cell_x12_y12__BLANK_) and
-    nextcol__cell_1__cell_1(cell_x11_y11__BLANK_, cell_x12_y12__BLANK_) and
-    nextcol__cell_0__cell_0(cell_x12_y12__BLANK_, cell_x13_y13__BLANK_) and
-    nextcol__cell_1__cell_1(cell_x12_y12__BLANK_, cell_x13_y13__BLANK_) and
-   cell_2x(cell_x9_y9__BLANK_) and
-    cell__BLANK___BLANK___BLANK_(cell_x9_y9__BLANK_) and
-    cell_2x(cell_x10_y10__BLANK_) and
-     cell__BLANK___BLANK___BLANK_(cell_x10_y10__BLANK_) and
-    cell_2x(cell_x11_y11__BLANK_) and
-     cell__BLANK___BLANK___BLANK_(cell_x11_y11__BLANK_) and
-    cell_2x(cell_x12_y12__BLANK_) and
-     cell__BLANK___BLANK___BLANK_(cell_x12_y12__BLANK_) and
-    cell_2x(cell_x13_y13__BLANK_) and
-     cell__BLANK___BLANK___BLANK_(cell_x13_y13__BLANK_))
-REL diag2__b() =
- ex cell_x14_y18__BLANK_, cell_x15_y17__BLANK_, cell_x16_y16__BLANK_,
-  cell_x17_y15__BLANK_, cell_x18_y14__BLANK_
-  (true and
-   nextcol__cell_0__cell_0(cell_x14_y18__BLANK_, cell_x15_y17__BLANK_) and
-    nextcol__cell_1__cell_1(cell_x15_y17__BLANK_, cell_x14_y18__BLANK_) and
-    nextcol__cell_0__cell_0(cell_x15_y17__BLANK_, cell_x16_y16__BLANK_) and
-    nextcol__cell_1__cell_1(cell_x16_y16__BLANK_, cell_x15_y17__BLANK_) and
-    nextcol__cell_0__cell_0(cell_x16_y16__BLANK_, cell_x17_y15__BLANK_) and
-    nextcol__cell_1__cell_1(cell_x17_y15__BLANK_, cell_x16_y16__BLANK_) and
-    nextcol__cell_0__cell_0(cell_x17_y15__BLANK_, cell_x18_y14__BLANK_) and
-    nextcol__cell_1__cell_1(cell_x18_y14__BLANK_, cell_x17_y15__BLANK_) and
-   cell_2b(cell_x14_y18__BLANK_) and
-    cell__BLANK___BLANK___BLANK_(cell_x14_y18__BLANK_) and
-    cell_2b(cell_x15_y17__BLANK_) and
-     cell__BLANK___BLANK___BLANK_(cell_x15_y17__BLANK_) and
-    cell_2b(cell_x16_y16__BLANK_) and
-     cell__BLANK___BLANK___BLANK_(cell_x16_y16__BLANK_) and
-    cell_2b(cell_x17_y15__BLANK_) and
-     cell__BLANK___BLANK___BLANK_(cell_x17_y15__BLANK_) and
-    cell_2b(cell_x18_y14__BLANK_) and
-     cell__BLANK___BLANK___BLANK_(cell_x18_y14__BLANK_))
-REL diag2__o() =
- ex cell_x14_y18__BLANK_, cell_x15_y17__BLANK_, cell_x16_y16__BLANK_,
-  cell_x17_y15__BLANK_, cell_x18_y14__BLANK_
-  (true and
-   nextcol__cell_0__cell_0(cell_x14_y18__BLANK_, cell_x15_y17__BLANK_) and
-    nextcol__cell_1__cell_1(cell_x15_y17__BLANK_, cell_x14_y18__BLANK_) and
-    nextcol__cell_0__cell_0(cell_x15_y17__BLANK_, cell_x16_y16__BLANK_) and
-    nextcol__cell_1__cell_1(cell_x16_y16__BLANK_, cell_x15_y17__BLANK_) and
-    nextcol__cell_0__cell_0(cell_x16_y16__BLANK_, cell_x17_y15__BLANK_) and
-    nextcol__cell_1__cell_1(cell_x17_y15__BLANK_, cell_x16_y16__BLANK_) and
-    nextcol__cell_0__cell_0(cell_x17_y15__BLANK_, cell_x18_y14__BLANK_) and
-    nextcol__cell_1__cell_1(cell_x18_y14__BLANK_, cell_x17_y15__BLANK_) and
-   cell_2o(cell_x14_y18__BLANK_) and
-    cell__BLANK___BLANK___BLANK_(cell_x14_y18__BLANK_) and
-    cell_2o(cell_x15_y17__BLANK_) and
-     cell__BLANK___BLANK___BLANK_(cell_x15_y17__BLANK_) and
-    cell_2o(cell_x16_y16__BLANK_) and
-     cell__BLANK___BLANK___BLANK_(cell_x16_y16__BLANK_) and
-    cell_2o(cell_x17_y15__BLANK_) and
-     cell__BLANK___BLANK___BLANK_(cell_x17_y15__BLANK_) and
-    cell_2o(cell_x18_y14__BLANK_) and
-     cell__BLANK___BLANK___BLANK_(cell_x18_y14__BLANK_))
-REL diag2__x() =
- ex cell_x14_y18__BLANK_, cell_x15_y17__BLANK_, cell_x16_y16__BLANK_,
-  cell_x17_y15__BLANK_, cell_x18_y14__BLANK_
-  (true and
-   nextcol__cell_0__cell_0(cell_x14_y18__BLANK_, cell_x15_y17__BLANK_) and
-  ...
 
[truncated message content]