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

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

Revision: 1579
          http://toss.svn.sourceforge.net/toss/?rev=1579&view=rev
Author:   lukstafi
Date:     2011-09-29 22:18:32 +0000 (Thu, 29 Sep 2011)
Log Message:
-----------
GDL translation: bug fix in eliminating redundant existenital quantification; switched introducing relation complements off; fixes in translating incoming moves for concurrent games; regenerated tests.

Modified Paths:
--------------
    trunk/Toss/Formula/FormulaOpsTest.ml
    trunk/Toss/GGP/GameSimpl.ml
    trunk/Toss/GGP/TranslateGame.ml
    trunk/Toss/GGP/TranslateGameTest.ml
    trunk/Toss/GGP/tests/2player_normal_form_2010-simpl.toss
    trunk/Toss/GGP/tests/breakthrough-raw.toss
    trunk/Toss/GGP/tests/breakthrough-simpl.toss
    trunk/Toss/GGP/tests/connect4-raw.toss
    trunk/Toss/GGP/tests/connect4-simpl.toss
    trunk/Toss/GGP/tests/connect5-raw.toss
    trunk/Toss/GGP/tests/connect5-simpl.toss
    trunk/Toss/GGP/tests/tictactoe-simpl.toss

Modified: trunk/Toss/Formula/FormulaOpsTest.ml
===================================================================
--- trunk/Toss/Formula/FormulaOpsTest.ml	2011-09-29 16:34:12 UTC (rev 1578)
+++ trunk/Toss/Formula/FormulaOpsTest.ml	2011-09-29 22:18:32 UTC (rev 1579)
@@ -295,6 +295,7 @@
        let rr_eq phi1 phi2 =
          formula_eq id phi2 (FormulaOps.remove_redundant ~implies) phi1 in
        rr_eq "P(x) and Q(x)" "P(x)";
+       rr_eq "R(x, y) and (Q(x) and P(x))" "R(x, y) and P(x)";
        rr_eq "P(x) and (not Q(x) or R(x,y))" "P(x) and R(x,y)";
        rr_eq "Q(x) and (not P(x) or R(x,y))"
          "Q(x) and (R(x, y) or not P(x))";

Modified: trunk/Toss/GGP/GameSimpl.ml
===================================================================
--- trunk/Toss/GGP/GameSimpl.ml	2011-09-29 16:34:12 UTC (rev 1578)
+++ trunk/Toss/GGP/GameSimpl.ml	2011-09-29 22:18:32 UTC (rev 1579)
@@ -141,7 +141,7 @@
 
 let debug_level = ref 0
 
-let introduce_complement = ref true
+let introduce_complement = ref false
 let final_simplify =
   ref (FormulaOps.remove_redundant ?implies:None)
 
@@ -176,11 +176,19 @@
             | Eq (v1, v2) when List.mem (v2 :> var) vs ->
               Aux.Left (Formula.var_str v2, Formula.var_str v1)
             | phi -> Aux.Right phi) conj in
+        let more_conj = List.filter
+          (fun (elim, equated) -> List.tl equated <> [])
+          (Aux.collect sb) in
+        let more_conj = Aux.concat_map
+          (fun (_, equated) ->
+            let lhs = List.hd equated in
+            List.map (fun rhs -> Eq (`FO lhs, `FO rhs)) (List.tl equated))
+          more_conj in
         if sb = [] then Ex (vs, And conj)
         else
           let vs =
             List.filter (fun v -> not (List.mem_assoc (var_str v) sb)) vs in
-          let phi = FormulaSubst.subst_vars sb (And conj) in
+          let phi = FormulaSubst.subst_vars sb (And (more_conj @ conj)) in
           if vs = [] then phi else Ex (vs, phi)
       | phi -> phi} in
   FormulaMap.map_formula f_map phi

Modified: trunk/Toss/GGP/TranslateGame.ml
===================================================================
--- trunk/Toss/GGP/TranslateGame.ml	2011-09-29 16:34:12 UTC (rev 1578)
+++ trunk/Toss/GGP/TranslateGame.ml	2011-09-29 22:18:32 UTC (rev 1579)
@@ -650,7 +650,7 @@
    terms. Remove "true" atoms that are "subsumed" by more specific
    atoms (that have subterms instead of blanks). *)
 let call_transform term_arities ground_at_c_paths
-    rel partition ((h_rel,h_args as h),body as cl) =
+    rel partition ((h_rel,h_args as h),body) =
   let r_atoms = if h_rel = rel then [h_args] else [] in
   let r_atoms = r_atoms @ Aux.map_some
     (function Rel (r, args) when r = rel -> Some args
@@ -2833,7 +2833,7 @@
   (* }}} *)
   let game, state = result in
   let inl_game = Arena.map_to_formulas GameSimpl.remove_exist
-    (inline_defined_rels defined_rels game) in
+    (inline_defined_rels game.Arena.defined_rels game) in
   gdl_translation, game, (inl_game, state)
   
 
@@ -2869,8 +2869,11 @@
   (* {{{ log entry *)
   if !debug_level > 2 then (
     Printf.printf
-      "GDL.translate_incoming_move: rule=%s; trying precond=\n%s\n...%!"
-      rname (Formula.sprint precond)
+      "GDL.translate_incoming_move: rule=%s; move=%s; coords=%s; precond=\n%s\n...%!"
+      rname (term_str move)
+      (*String.concat ", " (List.map term_str (Array.to_list rdata.legal_tuple))*)
+      (String.concat ", " (List.map Formula.sprint coords))
+      (Formula.sprint precond)
   );
 
   (* }}} *)
@@ -2883,7 +2886,6 @@
       (Structure.str struc)
   );
   (* }}} *)
-  DiscreteRule.debug_level := 6;
   let asgns =
     DiscreteRule.find_matchings struc r_obj in
   (* {{{ log entry *)
@@ -2959,28 +2961,32 @@
 
 (* We translate as a suite of moves, one for each player; after these
    rules have been applied, the server should apply the environment rule. *)
-let translate_incoming_move_concurrent gdl state actions =
+let translate_incoming_move_concurrent gdl (game,state as gstate) actions =
   (* there is only location 0; Environment is not among [actions] *)
+  let loc = game.Arena.graph.(0) in
   let actions = Array.of_list actions in
-  (* let location = (fst state).Arena.graph.(0) in *)
-  let struc = (snd state).Arena.struc in
+  (* let location = state.Arena.graph.(0) in *)
+  let struc = state.Arena.struc in
   (* the players actually start at 1, index 0 is the environment *)
   let candidates = Array.mapi
     (fun player_not_env move ->
       let player = player_not_env + 1 in
+      let prules = loc.(player).Arena.moves in
+      let prules = List.map (fun (lb,_)->lb.Arena.lb_rule) prules in
       let tossrules =
-        Aux.strmap_filter (fun  _ rdata ->
-          rdata.legal_tuple <> [||] &&  (* not Environment rule *)
+        Aux.strmap_filter (fun  rname rdata ->
+          List.mem rname prules &&
+            rdata.legal_tuple <> [||] &&  (* not Environment rule *)
             let legal_term =
               if Array.length rdata.legal_tuple > 1
-              then rdata.legal_tuple.(player)
+              then rdata.legal_tuple.(player_not_env)
               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
-          rdata state player move rname    
+          rdata gstate player move rname    
       ) tossrules in
       match candidates with
         | [] ->

Modified: trunk/Toss/GGP/TranslateGameTest.ml
===================================================================
--- trunk/Toss/GGP/TranslateGameTest.ml	2011-09-29 16:34:12 UTC (rev 1578)
+++ trunk/Toss/GGP/TranslateGameTest.ml	2011-09-29 22:18:32 UTC (rev 1579)
@@ -95,14 +95,31 @@
 (* COPIED FROM ReqHandler. *)
 exception Found of int
 (* The player applying the rewrite seems not to be used. *)
-(* Problem: are players indexed from 0 or from 1 in graph? *)
-let apply_rewrite state (player, (r_name, mtch)) =
+(* players are indexed from 1 in graph (0 is Environment) *)
+let apply_rewrite (game,state as gstate) (player, (r_name, mtch)) =
   if r_name <> "" then (
-    let {Arena.rules=rules; graph=graph} = fst state in
-    let mv_loc = graph.((snd state).Arena.cur_loc).(player) in
+    let {Arena.rules=rules; graph=graph} = game in
+    let struc = state.Arena.struc in
+    let mv_loc = graph.(state.Arena.cur_loc).(player) in
     let moves =
-      Move.gen_moves Move.cGRID_SIZE rules
-        (snd state).Arena.struc mv_loc in
+      Move.gen_moves Move.cGRID_SIZE rules struc mv_loc in
+    (* {{{ log entry *)
+    if !debug_level > 0 then (
+      let prules =
+        List.map (fun (lb,_)->lb.Arena.lb_rule) mv_loc.Arena.moves in
+      Printf.printf
+        "apply_rewrite: r_name=%s; mtch=%s; player=%d; prules=%s; moves= %s\n%!"
+        r_name
+        (ContinuousRule.embedding_str (List.assoc r_name rules) struc mtch)
+        player (String.concat ", " prules)
+        (String.concat "; "
+           (List.map (fun m->
+             let rul = List.assoc m.Arena.rule rules in
+             m.Arena.rule^":"^
+               ContinuousRule.embedding_str rul struc
+               m.Arena.embedding) (Array.to_list moves)))
+    );
+    (* }}} *)
     let pos = (
       try
         for i = 0 to Array.length moves - 1 do
@@ -118,11 +135,11 @@
       with Found pos ->
         pos) in
     let req = Arena.ApplyRuleInt (r_name, mtch, 0.1, []) in
-    let (new_state_noloc, resp) = Arena.handle_request state req in
+    let (new_state_noloc, resp) = Arena.handle_request gstate req in
     let new_loc = moves.(pos).Arena.next_loc in
     (fst new_state_noloc,
      {snd new_state_noloc with Arena.cur_loc = new_loc})
-  ) else state
+  ) else gstate
 
 let simult_test_case ~game_name ~player ~own_plnum ~opp_plnum
     ~own_rule_name ~own_emb ~own_move ~opp_rule_name ~opp_emb
@@ -289,7 +306,7 @@
         ~loc0_move:"(drop 2)" ~loc0_noop:"noop"
         ~loc1:1 ~loc1_rule_name:"noop_drop_c12"
         ~loc1_emb:[
-          "cell_c12_h6__BLANK_", "cell_2_1__BLANK_";
+          "cell_c12_h6__BLANK_", "cell_2_2__BLANK_";
           "control__BLANK_", "control__BLANK_"]
         ~loc1_noop:"noop" ~loc1_move:"(drop 2)"
     );
@@ -307,18 +324,18 @@
 
 let a () =
   set_debug_level 4;
-      game_test_case ~game_name:"tictactoe" ~player:"xplayer"
+      game_test_case ~game_name:"connect4" ~player:"white"
         ~own_plnum:0 ~opponent_plnum:1
-        ~loc0_rule_name:"mark_x6_y_noop"
+        ~loc0_rule_name:"drop_c11_noop"
         ~loc0_emb:[
-          "cell_x6_y__BLANK_", "cell_2_2__BLANK_";
+          "cell_c11_h4__BLANK_", "cell_2_1__BLANK_";
           "control__BLANK_", "control__BLANK_"]
-        ~loc0_move:"(mark 2 2)" ~loc0_noop:"noop"
-        ~loc1:1 ~loc1_rule_name:"noop_mark_x7_y0"
+        ~loc0_move:"(drop 2)" ~loc0_noop:"noop"
+        ~loc1:1 ~loc1_rule_name:"noop_drop_c12"
         ~loc1_emb:[
-          "cell_x7_y0__BLANK_", "cell_1_1__BLANK_";
+          "cell_c12_h6__BLANK_", "cell_2_2__BLANK_";
           "control__BLANK_", "control__BLANK_"]
-        ~loc1_noop:"noop" ~loc1_move:"(mark 1 1)";
+        ~loc1_noop:"noop" ~loc1_move:"(drop 2)";
   (* failwith "tested"; *)
   ()
 
@@ -356,14 +373,14 @@
   TranslateGame.generate_test_case := None
 
 let a () =
-  regenerate ~debug:false ~game_name:"tictactoe" ~player:"xplayer";
+  (* 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: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"; *)
-  (* regenerate ~debug:true ~game_name:"pacman3p" ~player:"pacman"; *)
-  failwith "generated";
+  regenerate ~debug:true ~game_name:"pacman3p" ~player:"pacman";
+  (* failwith "generated"; *)
   ()
 
 let translate_file fname timeout =

Modified: trunk/Toss/GGP/tests/2player_normal_form_2010-simpl.toss
===================================================================
--- trunk/Toss/GGP/tests/2player_normal_form_2010-simpl.toss	2011-09-29 16:34:12 UTC (rev 1578)
+++ trunk/Toss/GGP/tests/2player_normal_form_2010-simpl.toss	2011-09-29 22:18:32 UTC (rev 1579)
@@ -4,7 +4,6 @@
   ex did__BLANK__m11
    (did__BLANK___BLANK_(did__BLANK__m11) and did_0row(did__BLANK__m11))
 PLAYERS Environment, row, column
-DATA C: C__val___BLANK_
 RULE m:
  [did__BLANK__m, synch_control_ |
     _opt_column__SYNC {did__BLANK__m; synch_control_};
@@ -22,8 +21,9 @@
   pre
    (not terminal() and
     ex val__r0, val__r, did__BLANK__m0
-     (did__BLANK___BLANK_(did__BLANK__m0) and reward(did__BLANK__m,
-      did__BLANK__m0, val__r, val__r0) and not C(val__r) and not C(val__r0)))
+     (did__BLANK___BLANK_(did__BLANK__m0) and val___BLANK_(val__r) and
+      val___BLANK_(val__r0) and reward(did__BLANK__m, did__BLANK__m0, val__r,
+      val__r0)))
 RULE m2:
  [did__BLANK__m2, synch_control_ |
     _opt_column__SYNC (did__BLANK__m2);
@@ -41,9 +41,9 @@
   pre
    (not terminal() and
     ex val__r2, val__r1, did__BLANK__m1
-     (did__BLANK___BLANK_(did__BLANK__m1) and reward(did__BLANK__m1,
-      did__BLANK__m2, val__r1, val__r2) and not C(val__r1) and
-      not C(val__r2)))
+     (did__BLANK___BLANK_(did__BLANK__m1) and val___BLANK_(val__r1) and
+      val___BLANK_(val__r2) and reward(did__BLANK__m1, did__BLANK__m2,
+      val__r1, val__r2)))
 RULE Environment:
  [synch_control_ |
     _opt_did_0column (synch_control_); _opt_did_0row (synch_control_);
@@ -61,9 +61,9 @@
      ex val__r6, val__10, did__BLANK__m7, did__BLANK__m8
       (did__BLANK___BLANK_(did__BLANK__m7) and
        did__BLANK___BLANK_(did__BLANK__m8) and val__010(val__10) and
-       reward(did__BLANK__m7, did__BLANK__m8, val__10, val__r6) and
-       did_0row(did__BLANK__m7) and did_0column(did__BLANK__m8) and
-       not C(val__10) and not C(val__r6))
+       val___BLANK_(val__r6) and reward(did__BLANK__m7, did__BLANK__m8,
+       val__10, val__r6) and did_0row(did__BLANK__m7) and
+       did_0column(did__BLANK__m8))
      )
     +
     100. *
@@ -71,9 +71,9 @@
       ex val__r6, val__100, did__BLANK__m7, did__BLANK__m8
        (did__BLANK___BLANK_(did__BLANK__m7) and
         did__BLANK___BLANK_(did__BLANK__m8) and val__0100(val__100) and
-        reward(did__BLANK__m7, did__BLANK__m8, val__100, val__r6) and
-        did_0row(did__BLANK__m7) and did_0column(did__BLANK__m8) and
-        not C(val__100) and not C(val__r6))
+        val___BLANK_(val__r6) and reward(did__BLANK__m7, did__BLANK__m8,
+        val__100, val__r6) and did_0row(did__BLANK__m7) and
+        did_0column(did__BLANK__m8))
       )
     +
     20. *
@@ -81,9 +81,9 @@
       ex val__r6, val__20, did__BLANK__m7, did__BLANK__m8
        (did__BLANK___BLANK_(did__BLANK__m7) and
         did__BLANK___BLANK_(did__BLANK__m8) and val__020(val__20) and
-        reward(did__BLANK__m7, did__BLANK__m8, val__20, val__r6) and
-        did_0row(did__BLANK__m7) and did_0column(did__BLANK__m8) and
-        not C(val__20) and not C(val__r6))
+        val___BLANK_(val__r6) and reward(did__BLANK__m7, did__BLANK__m8,
+        val__20, val__r6) and did_0row(did__BLANK__m7) and
+        did_0column(did__BLANK__m8))
       )
     +
     30. *
@@ -91,9 +91,9 @@
       ex val__r6, val__30, did__BLANK__m7, did__BLANK__m8
        (did__BLANK___BLANK_(did__BLANK__m7) and
         did__BLANK___BLANK_(did__BLANK__m8) and val__030(val__30) and
-        reward(did__BLANK__m7, did__BLANK__m8, val__30, val__r6) and
-        did_0row(did__BLANK__m7) and did_0column(did__BLANK__m8) and
-        not C(val__30) and not C(val__r6))
+        val___BLANK_(val__r6) and reward(did__BLANK__m7, did__BLANK__m8,
+        val__30, val__r6) and did_0row(did__BLANK__m7) and
+        did_0column(did__BLANK__m8))
       )
     +
     40. *
@@ -101,9 +101,9 @@
       ex val__r6, val__40, did__BLANK__m7, did__BLANK__m8
        (did__BLANK___BLANK_(did__BLANK__m7) and
         did__BLANK___BLANK_(did__BLANK__m8) and val__040(val__40) and
-        reward(did__BLANK__m7, did__BLANK__m8, val__40, val__r6) and
-        did_0row(did__BLANK__m7) and did_0column(did__BLANK__m8) and
-        not C(val__40) and not C(val__r6))
+        val___BLANK_(val__r6) and reward(did__BLANK__m7, did__BLANK__m8,
+        val__40, val__r6) and did_0row(did__BLANK__m7) and
+        did_0column(did__BLANK__m8))
       )
     +
     50. *
@@ -111,9 +111,9 @@
       ex val__r6, val__50, did__BLANK__m7, did__BLANK__m8
        (did__BLANK___BLANK_(did__BLANK__m7) and
         did__BLANK___BLANK_(did__BLANK__m8) and val__050(val__50) and
-        reward(did__BLANK__m7, did__BLANK__m8, val__50, val__r6) and
-        did_0row(did__BLANK__m7) and did_0column(did__BLANK__m8) and
-        not C(val__50) and not C(val__r6))
+        val___BLANK_(val__r6) and reward(did__BLANK__m7, did__BLANK__m8,
+        val__50, val__r6) and did_0row(did__BLANK__m7) and
+        did_0column(did__BLANK__m8))
       )
     +
     80. *
@@ -121,9 +121,9 @@
       ex val__r6, val__80, did__BLANK__m7, did__BLANK__m8
        (did__BLANK___BLANK_(did__BLANK__m7) and
         did__BLANK___BLANK_(did__BLANK__m8) and val__080(val__80) and
-        reward(did__BLANK__m7, did__BLANK__m8, val__80, val__r6) and
-        did_0row(did__BLANK__m7) and did_0column(did__BLANK__m8) and
-        not C(val__80) and not C(val__r6))
+        val___BLANK_(val__r6) and reward(did__BLANK__m7, did__BLANK__m8,
+        val__80, val__r6) and did_0row(did__BLANK__m7) and
+        did_0column(did__BLANK__m8))
       )
     +
     90. *
@@ -131,9 +131,9 @@
       ex val__r6, val__90, did__BLANK__m7, did__BLANK__m8
        (did__BLANK___BLANK_(did__BLANK__m7) and
         did__BLANK___BLANK_(did__BLANK__m8) and val__090(val__90) and
-        reward(did__BLANK__m7, did__BLANK__m8, val__90, val__r6) and
-        did_0row(did__BLANK__m7) and did_0column(did__BLANK__m8) and
-        not C(val__90) and not C(val__r6))
+        val___BLANK_(val__r6) and reward(did__BLANK__m7, did__BLANK__m8,
+        val__90, val__r6) and did_0row(did__BLANK__m7) and
+        did_0column(did__BLANK__m8))
       )
   MOVES [m -> 0] }
   PLAYER column {
@@ -143,9 +143,9 @@
      ex val__10, val__r7, did__BLANK__m9, did__BLANK__m10
       (did__BLANK___BLANK_(did__BLANK__m10) and
        did__BLANK___BLANK_(did__BLANK__m9) and val__010(val__10) and
-       reward(did__BLANK__m9, did__BLANK__m10, val__r7, val__10) and
-       did_0column(did__BLANK__m10) and did_0row(did__BLANK__m9) and
-       not C(val__10) and not C(val__r7))
+       val___BLANK_(val__r7) and reward(did__BLANK__m9, did__BLANK__m10,
+       val__r7, val__10) and did_0column(did__BLANK__m10) and
+       did_0row(did__BLANK__m9))
      )
     +
     100. *
@@ -153,9 +153,9 @@
       ex val__100, val__r7, did__BLANK__m9, did__BLANK__m10
        (did__BLANK___BLANK_(did__BLANK__m10) and
         did__BLANK___BLANK_(did__BLANK__m9) and val__0100(val__100) and
-        reward(did__BLANK__m9, did__BLANK__m10, val__r7, val__100) and
-        did_0column(did__BLANK__m10) and did_0row(did__BLANK__m9) and
-        not C(val__100) and not C(val__r7))
+        val___BLANK_(val__r7) and reward(did__BLANK__m9, did__BLANK__m10,
+        val__r7, val__100) and did_0column(did__BLANK__m10) and
+        did_0row(did__BLANK__m9))
       )
     +
     20. *
@@ -163,9 +163,9 @@
       ex val__20, val__r7, did__BLANK__m9, did__BLANK__m10
        (did__BLANK___BLANK_(did__BLANK__m10) and
         did__BLANK___BLANK_(did__BLANK__m9) and val__020(val__20) and
-        reward(did__BLANK__m9, did__BLANK__m10, val__r7, val__20) and
-        did_0column(did__BLANK__m10) and did_0row(did__BLANK__m9) and
-        not C(val__20) and not C(val__r7))
+        val___BLANK_(val__r7) and reward(did__BLANK__m9, did__BLANK__m10,
+        val__r7, val__20) and did_0column(did__BLANK__m10) and
+        did_0row(did__BLANK__m9))
       )
     +
     30. *
@@ -173,9 +173,9 @@
       ex val__30, val__r7, did__BLANK__m9, did__BLANK__m10
        (did__BLANK___BLANK_(did__BLANK__m10) and
         did__BLANK___BLANK_(did__BLANK__m9) and val__030(val__30) and
-        reward(did__BLANK__m9, did__BLANK__m10, val__r7, val__30) and
-        did_0column(did__BLANK__m10) and did_0row(did__BLANK__m9) and
-        not C(val__30) and not C(val__r7))
+        val___BLANK_(val__r7) and reward(did__BLANK__m9, did__BLANK__m10,
+        val__r7, val__30) and did_0column(did__BLANK__m10) and
+        did_0row(did__BLANK__m9))
       )
     +
     40. *
@@ -183,9 +183,9 @@
       ex val__40, val__r7, did__BLANK__m9, did__BLANK__m10
        (did__BLANK___BLANK_(did__BLANK__m10) and
         did__BLANK___BLANK_(did__BLANK__m9) and val__040(val__40) and
-        reward(did__BLANK__m9, did__BLANK__m10, val__r7, val__40) and
-        did_0column(did__BLANK__m10) and did_0row(did__BLANK__m9) and
-        not C(val__40) and not C(val__r7))
+        val___BLANK_(val__r7) and reward(did__BLANK__m9, did__BLANK__m10,
+        val__r7, val__40) and did_0column(did__BLANK__m10) and
+        did_0row(did__BLANK__m9))
       )
     +
     50. *
@@ -193,9 +193,9 @@
       ex val__50, val__r7, did__BLANK__m9, did__BLANK__m10
        (did__BLANK___BLANK_(did__BLANK__m10) and
         did__BLANK___BLANK_(did__BLANK__m9) and val__050(val__50) and
-        reward(did__BLANK__m9, did__BLANK__m10, val__r7, val__50) and
-        did_0column(did__BLANK__m10) and did_0row(did__BLANK__m9) and
-        not C(val__50) and not C(val__r7))
+        val___BLANK_(val__r7) and reward(did__BLANK__m9, did__BLANK__m10,
+        val__r7, val__50) and did_0column(did__BLANK__m10) and
+        did_0row(did__BLANK__m9))
       )
     +
     80. *
@@ -203,9 +203,9 @@
       ex val__80, val__r7, did__BLANK__m9, did__BLANK__m10
        (did__BLANK___BLANK_(did__BLANK__m10) and
         did__BLANK___BLANK_(did__BLANK__m9) and val__080(val__80) and
-        reward(did__BLANK__m9, did__BLANK__m10, val__r7, val__80) and
-        did_0column(did__BLANK__m10) and did_0row(did__BLANK__m9) and
-        not C(val__80) and not C(val__r7))
+        val___BLANK_(val__r7) and reward(did__BLANK__m9, did__BLANK__m10,
+        val__r7, val__80) and did_0column(did__BLANK__m10) and
+        did_0row(did__BLANK__m9))
       )
     +
     90. *
@@ -213,9 +213,9 @@
       ex val__90, val__r7, did__BLANK__m9, did__BLANK__m10
        (did__BLANK___BLANK_(did__BLANK__m10) and
         did__BLANK___BLANK_(did__BLANK__m9) and val__090(val__90) and
-        reward(did__BLANK__m9, did__BLANK__m10, val__r7, val__90) and
-        did_0column(did__BLANK__m10) and did_0row(did__BLANK__m9) and
-        not C(val__90) and not C(val__r7))
+        val___BLANK_(val__r7) and reward(did__BLANK__m9, did__BLANK__m10,
+        val__r7, val__90) and did_0column(did__BLANK__m10) and
+        did_0row(did__BLANK__m9))
       )
   MOVES [m2 -> 0] }
 }
@@ -224,10 +224,6 @@
    did__BLANK__r2, did__BLANK__r3, val__0, val__10, val__100, val__20,
    val__30, val__40, val__50, val__80, val__90, val__column, val__row,
    synch_control_ |
-    C {
-     did__BLANK__c1; did__BLANK__c2; did__BLANK__c3; did__BLANK__r1;
-      did__BLANK__r2; did__BLANK__r3; synch_control_
-     };
     column__SYNC:1 {}; did_0column:1 {}; did_0row:1 {};
     did_1c1 (did__BLANK__c1); did_1c2 (did__BLANK__c2);
     did_1c3 (did__BLANK__c3); did_1r1 (did__BLANK__r1);
@@ -251,6 +247,10 @@
     synch_control_ (synch_control_); val__00 (val__0); val__010 (val__10);
     val__0100 (val__100); val__020 (val__20); val__030 (val__30);
     val__040 (val__40); val__050 (val__50); val__080 (val__80);
-    val__090 (val__90); val__0column (val__column); val__0row (val__row)
+    val__090 (val__90); val__0column (val__column); val__0row (val__row);
+    val___BLANK_ {
+     val__0; val__10; val__100; val__20; val__30; val__40; val__50; val__80;
+      val__90; val__column; val__row
+     }
    | 
  ]

Modified: trunk/Toss/GGP/tests/breakthrough-raw.toss
===================================================================
--- trunk/Toss/GGP/tests/breakthrough-raw.toss	2011-09-29 16:34:12 UTC (rev 1578)
+++ trunk/Toss/GGP/tests/breakthrough-raw.toss	2011-09-29 22:18:32 UTC (rev 1579)
@@ -19,7 +19,6 @@
       cellholds_x24_y26__BLANK_) and
      cellholds__BLANK___BLANK___BLANK_(cellholds_x24_y26__BLANK_) and
       cellholds__BLANK___BLANK___BLANK_(cellholds_x23_y25__BLANK_))
-REL terminal() = (whitewin() and true) or (blackwin() and true)
 REL blackcell() =
  ex cellholds_x28_y28__BLANK_
   (cell(cellholds_x28_y28__BLANK_) and
@@ -43,6 +42,7 @@
         cellholds__BLANK___BLANK___BLANK_(cellholds_x20_y22__BLANK_)) or
        (cellholds_2black(cellholds_x20_y22__BLANK_) and
         cellholds__BLANK___BLANK___BLANK_(cellholds_x20_y22__BLANK_)))))
+REL terminal() = (whitewin() and true) or (blackwin() and true)
 REL whitecell() =
  ex cellholds_x27_y27__BLANK_
   (cell(cellholds_x27_y27__BLANK_) and

Modified: trunk/Toss/GGP/tests/breakthrough-simpl.toss
===================================================================
--- trunk/Toss/GGP/tests/breakthrough-simpl.toss	2011-09-29 16:34:12 UTC (rev 1578)
+++ trunk/Toss/GGP/tests/breakthrough-simpl.toss	2011-09-29 22:18:32 UTC (rev 1579)
@@ -1,39 +1,30 @@
-REL cell(v0) =
- ex cellholds_x19_y21__BLANK_
-  (v0 = cellholds_x19_y21__BLANK_ and not C(cellholds_x19_y21__BLANK_))
-REL terminal() = blackwin() or whitewin()
+REL cell(v0) = index__cellholds_1(v0)
 REL blackcell() =
  ex cellholds_x28_y28__BLANK_
-  (cell(cellholds_x28_y28__BLANK_) and
-   cellholds_2black(cellholds_x28_y28__BLANK_) and
-   not C(cellholds_x28_y28__BLANK_))
+  (index__cellholds_1(cellholds_x28_y28__BLANK_) and
+   cell(cellholds_x28_y28__BLANK_) and
+   cellholds_2black(cellholds_x28_y28__BLANK_))
 REL blackwin() =
  not whitecell() or
   ex cellholds_x26_1__BLANK_
    (cellholds_11(cellholds_x26_1__BLANK_) and
-    cellholds_2black(cellholds_x26_1__BLANK_) and
-    not C(cellholds_x26_1__BLANK_))
+    cellholds_2black(cellholds_x26_1__BLANK_))
 REL cellempty(v0) =
- ex cellholds_x20_y22__BLANK_
-  (cell(cellholds_x20_y22__BLANK_) and v0 = cellholds_x20_y22__BLANK_ and
-   not C(cellholds_x20_y22__BLANK_) and
-   not
-    (cellholds_2black(cellholds_x20_y22__BLANK_) or
-     cellholds_2white(cellholds_x20_y22__BLANK_)))
+ (index__cellholds_1(v0) and cell(v0) and
+  not (cellholds_2black(v0) or cellholds_2white(v0)))
+REL terminal() = blackwin() or whitewin()
 REL whitecell() =
  ex cellholds_x27_y27__BLANK_
-  (cell(cellholds_x27_y27__BLANK_) and
-   cellholds_2white(cellholds_x27_y27__BLANK_) and
-   not C(cellholds_x27_y27__BLANK_))
+  (index__cellholds_1(cellholds_x27_y27__BLANK_) and
+   cell(cellholds_x27_y27__BLANK_) and
+   cellholds_2white(cellholds_x27_y27__BLANK_))
 REL whitewin() =
  not blackcell() or
   ex cellholds_x25_8__BLANK_
    (cellholds_18(cellholds_x25_8__BLANK_) and
-    cellholds_2white(cellholds_x25_8__BLANK_) and
-    not C(cellholds_x25_8__BLANK_))
+    cellholds_2white(cellholds_x25_8__BLANK_))
 PLAYERS white, black
-DATA C: C__index__cellholds_1,
- R0: succ__cellholds_0__cellholds_0__AND__succ__cellholds_1__cellholds_1,
+DATA R0: succ__cellholds_0__cellholds_0__AND__succ__cellholds_1__cellholds_1,
  R: EQ___cellholds_0__cellholds_0__AND__succ__cellholds_1__cellholds_1,
  R1: succ__cellholds_0__cellholds_0__AND_INV__succ__cellholds_1__cellholds_1
 RULE move_x_y_x_y0_noop:
@@ -47,7 +38,8 @@
     _opt_control_0white {cellholds_x_y0__BLANK_; cellholds_x_y__BLANK_};
     cellempty (cellholds_x_y0__BLANK_);
     cellholds_2white (cellholds_x_y__BLANK_);
-    control_0white (control__BLANK_); control__BLANK_ (control__BLANK_)
+    control_0white (control__BLANK_); control__BLANK_ (control__BLANK_);
+    index__cellholds_1 {cellholds_x_y0__BLANK_; cellholds_x_y__BLANK_}
    | 
   ] ->
   [cellholds_x_y0__BLANK_, cellholds_x_y__BLANK_, control__BLANK_ |
@@ -66,7 +58,8 @@
      cellholds_x0_y1__BLANK_; cellholds_x1_y2__BLANK_; control__BLANK_};
     _opt_control_0white {cellholds_x0_y1__BLANK_; cellholds_x1_y2__BLANK_};
     cellholds_2white (cellholds_x0_y1__BLANK_);
-    control_0white (control__BLANK_); control__BLANK_ (control__BLANK_)
+    control_0white (control__BLANK_); control__BLANK_ (control__BLANK_);
+    index__cellholds_1 {cellholds_x0_y1__BLANK_; cellholds_x1_y2__BLANK_}
    | 
   ] ->
   [cellholds_x0_y1__BLANK_, cellholds_x1_y2__BLANK_, control__BLANK_ |
@@ -85,7 +78,8 @@
      cellholds_x2_y3__BLANK_; cellholds_x3_y4__BLANK_; control__BLANK_};
     _opt_control_0white {cellholds_x2_y3__BLANK_; cellholds_x3_y4__BLANK_};
     cellholds_2white (cellholds_x2_y3__BLANK_);
-    control_0white (control__BLANK_); control__BLANK_ (control__BLANK_)
+    control_0white (control__BLANK_); control__BLANK_ (control__BLANK_);
+    index__cellholds_1 {cellholds_x2_y3__BLANK_; cellholds_x3_y4__BLANK_}
    | 
   ] ->
   [cellholds_x2_y3__BLANK_, cellholds_x3_y4__BLANK_, control__BLANK_ |
@@ -105,7 +99,8 @@
      cellholds_x4_y5__BLANK_; cellholds_x4_y6__BLANK_; control__BLANK_};
     cellempty (cellholds_x4_y6__BLANK_);
     cellholds_2black (cellholds_x4_y5__BLANK_);
-    control_0black (control__BLANK_); control__BLANK_ (control__BLANK_)
+    control_0black (control__BLANK_); control__BLANK_ (control__BLANK_);
+    index__cellholds_1 {cellholds_x4_y5__BLANK_; cellholds_x4_y6__BLANK_}
    | 
   ] ->
   [cellholds_x4_y5__BLANK_, cellholds_x4_y6__BLANK_, control__BLANK_ |
@@ -124,7 +119,8 @@
     _opt_control_0white {
      cellholds_x5_y7__BLANK_; cellholds_x6_y8__BLANK_; control__BLANK_};
     cellholds_2black (cellholds_x5_y7__BLANK_);
-    control_0black (control__BLANK_); control__BLANK_ (control__BLANK_)
+    control_0black (control__BLANK_); control__BLANK_ (control__BLANK_);
+    index__cellholds_1 {cellholds_x5_y7__BLANK_; cellholds_x6_y8__BLANK_}
    | 
   ] ->
   [cellholds_x5_y7__BLANK_, cellholds_x6_y8__BLANK_, control__BLANK_ |
@@ -143,7 +139,8 @@
     _opt_control_0white {
      cellholds_x7_y9__BLANK_; cellholds_x8_y10__BLANK_; control__BLANK_};
     cellholds_2black (cellholds_x7_y9__BLANK_);
-    control_0black (control__BLANK_); control__BLANK_ (control__BLANK_)
+    control_0black (control__BLANK_); control__BLANK_ (control__BLANK_);
+    index__cellholds_1 {cellholds_x7_y9__BLANK_; cellholds_x8_y10__BLANK_}
    | 
   ] ->
   [cellholds_x7_y9__BLANK_, cellholds_x8_y10__BLANK_, control__BLANK_ |
@@ -189,7 +186,6 @@
    cellholds_8_2__BLANK_, cellholds_8_3__BLANK_, cellholds_8_4__BLANK_,
    cellholds_8_5__BLANK_, cellholds_8_6__BLANK_, cellholds_8_7__BLANK_,
    cellholds_8_8__BLANK_, val__black, val__white, control__BLANK_ |
-    C {val__black; val__white; control__BLANK_};
     R {
      (cellholds_1_1__BLANK_, cellholds_1_2__BLANK_);
       (cellholds_1_2__BLANK_, cellholds_1_3__BLANK_);
@@ -447,7 +443,32 @@
       cellholds_8_2__BLANK_
      };
     control_0black:1 {}; control_0white (control__BLANK_);
-    control__BLANK_ (control__BLANK_); val__0black (val__black);
-    val__0white (val__white); val___BLANK_ {val__black; val__white}
+    control__BLANK_ (control__BLANK_);
+    index__cellholds_1 {
+     cellholds_1_1__BLANK_; cellholds_1_2__BLANK_; cellholds_1_3__BLANK_;
+      cellholds_1_4__BLANK_; cellholds_1_5__BLANK_; cellholds_1_6__BLANK_;
+      cellholds_1_7__BLANK_; cellholds_1_8__BLANK_; cellholds_2_1__BLANK_;
+      cellholds_2_2__BLANK_; cellholds_2_3__BLANK_; cellholds_2_4__BLANK_;
+      cellholds_2_5__BLANK_; cellholds_2_6__BLANK_; cellholds_2_7__BLANK_;
+      cellholds_2_8__BLANK_; cellholds_3_1__BLANK_; cellholds_3_2__BLANK_;
+      cellholds_3_3__BLANK_; cellholds_3_4__BLANK_; cellholds_3_5__BLANK_;
+      cellholds_3_6__BLANK_; cellholds_3_7__BLANK_; cellholds_3_8__BLANK_;
+      cellholds_4_1__BLANK_; cellholds_4_2__BLANK_; cellholds_4_3__BLANK_;
+      cellholds_4_4__BLANK_; cellholds_4_5__BLANK_; cellholds_4_6__BLANK_;
+      cellholds_4_7__BLANK_; cellholds_4_8__BLANK_; cellholds_5_1__BLANK_;
+      cellholds_5_2__BLANK_; cellholds_5_3__BLANK_; cellholds_5_4__BLANK_;
+      cellholds_5_5__BLANK_; cellholds_5_6__BLANK_; cellholds_5_7__BLANK_;
+      cellholds_5_8__BLANK_; cellholds_6_1__BLANK_; cellholds_6_2__BLANK_;
+      cellholds_6_3__BLANK_; cellholds_6_4__BLANK_; cellholds_6_5__BLANK_;
+      cellholds_6_6__BLANK_; cellholds_6_7__BLANK_; cellholds_6_8__BLANK_;
+      cellholds_7_1__BLANK_; cellholds_7_2__BLANK_; cellholds_7_3__BLANK_;
+      cellholds_7_4__BLANK_; cellholds_7_5__BLANK_; cellholds_7_6__BLANK_;
+      cellholds_7_7__BLANK_; cellholds_7_8__BLANK_; cellholds_8_1__BLANK_;
+      cellholds_8_2__BLANK_; cellholds_8_3__BLANK_; cellholds_8_4__BLANK_;
+      cellholds_8_5__BLANK_; cellholds_8_6__BLANK_; cellholds_8_7__BLANK_;
+      cellholds_8_8__BLANK_
+     };
+    val__0black (val__black); val__0white (val__white);
+    val___BLANK_ {val__black; val__white}
    | 
  ]

Modified: trunk/Toss/GGP/tests/connect4-raw.toss
===================================================================
--- trunk/Toss/GGP/tests/connect4-raw.toss	2011-09-29 16:34:12 UTC (rev 1578)
+++ trunk/Toss/GGP/tests/connect4-raw.toss	2011-09-29 22:18:32 UTC (rev 1579)
@@ -1,215 +1,180 @@
-REL terminal() =
- ex val__r (line(val__r) and val__0r(val__r) and val___BLANK_(val__r)) or
-  ex val__w (line(val__w) and val__0w(val__w) and val___BLANK_(val__w)) or
-  (not open() and true)
-REL line(v0) =
- ex val__x13 (v0 = val__x13 and row(val__x13) and val___BLANK_(val__x13)) or
-  ex val__x14 (v0 = val__x14 and column(val__x14) and val___BLANK_(val__x14)) or
-  ex val__x15 (v0 = val__x15 and diag(val__x15) and val___BLANK_(val__x15))
-REL open() =
- ex cell_c10_h7__BLANK_
-  (empty(cell_c10_h7__BLANK_) and
-   cell__BLANK___BLANK___BLANK_(cell_c10_h7__BLANK_))
-REL column(v0) =
- ex val__dirt
-  (v0 = val__dirt and
-   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
-     val__0dirt(val__dirt) and val___BLANK_(val__dirt) 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_))) or
-  ex val__r
-   (v0 = val__r and
-    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
-      val__0r(val__r) and val___BLANK_(val__r) 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_))) or
-  ex val__w
-   (v0 = val__w and
-    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
-      val__0w(val__w) and val___BLANK_(val__w) 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 diag(v0) =
- ex val__dirt
-  (v0 = val__dirt and
-   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
-     val__0dirt(val__dirt) and val___BLANK_(val__dirt) 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 val__r
-   (v0 = val__r and
-    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
-      val__0r(val__r) and val___BLANK_(val__r) 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 val__w
-   (v0 = val__w and
-    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
-      val__0w(val__w) and val___BLANK_(val__w) 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 val__dirt
-   (v0 = val__dirt and
-    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
-      val__0dirt(val__dirt) and val___BLANK_(val__dirt) 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_))) or
-  ex val__r
-   (v0 = val__r and
-    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
-      val__0r(val__r) and val___BLANK_(val__r) 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_))) or
-  ex val__w
-   (v0 = val__w and
-    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
-      val__0w(val__w) and val___BLANK_(val__w) 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 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__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__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 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__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__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 empty(v0) =
  ex cell_c_h__BLANK_
   (v0 = cell_c_h__BLANK_ and
@@ -232,63 +197,69 @@
     true and
      cell_2r(cell_c2_h2__BLANK_) and
       cell__BLANK___BLANK___BLANK_(cell_c2_h2__BLANK_))
-REL row(v0) =
- ex val__r
-  (v0 = val__r and
-   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
-     val__0r(val__r) and val___BLANK_(val__r) 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_))) or
-  ex val__w
-   (v0 = val__w and
-    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
-      val__0w(val__w) and val___BLANK_(val__w) 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 line__dirt() = (column__dirt() and true) or (diag__dirt() and true)
+REL line__r() =
+ (row__r() and true) or (column__r() and true) or (diag__r() and true)
+REL line__w() =
+ (row__w() and true) or (column__w() and true) or (diag__w() and true)
+REL open() =
+ ex cell_c10_h7__BLANK_
+  (empty(cell_c10_h7__BLANK_) and
+   cell__BLANK___BLANK___BLANK_(cell_c10_h7__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__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_x...
 
[truncated message content]