--- reverse1.py	2025-12-26 21:57:07.468454794 +0200
+++ reverse2.py	2025-12-20 23:10:11.279336986 +0200
@@ -1,12 +1,37 @@
 #!/usr/bin/python3
 
-import os
-import GoL_SAT_utils, SAT_lib
+from typing import List
+import os, SAT_lib, GoL_SAT_utils, my_utils
 
+"""
 final_state=[
 " * ",
 "* *",
 " * "]
+"""
+
+"""
+final_state=[
+"      ",
+"      ",
+" **** ",
+"      ",
+"      "]
+"""
+
+#"""
+final_state=[
+"             ",
+"   *     *   ",
+"    *   *    ",
+"   *******   ",
+"  ** *** **  ",
+" *********** ",
+" * ******* * ",
+" * *     * * ",
+"    ** **    ",
+"             "]
+#"""
 
 H=len(final_state) # HEIGHT
 W=len(final_state[0]) # WIDTH
@@ -24,7 +49,7 @@
             v=GoL_SAT_utils.coords_to_var(grid, VAR_FALSE, r, c, H, W)
             n=GoL_SAT_utils.get_neighbours(grid, VAR_FALSE, r, c, H, W)
             if final_state[r][c]=="*":
-                s.add_clauses (GoL_SAT_utils.cell_is_true(v, n))
+                s.add_clauses (GoL_SAT_utils.cell_is_true(v,n))
             else:
                 s.add_clauses (GoL_SAT_utils.cell_is_false(v, n))
 
@@ -41,7 +66,8 @@
             n=GoL_SAT_utils.get_neighbours(grid, VAR_FALSE, r, c, H, W)
             s.add_clauses (GoL_SAT_utils.cell_is_false(v, n))
 
-    assert s.solve()
+    if s.solve()==False:
+        return None
 
     tmp=GoL_SAT_utils.SAT_solution_to_grid(grid, VAR_FALSE, s.solution, H, W)
 
@@ -51,8 +77,22 @@
     return tmp
 
 while True:
-    try_again()
-    if s.fetch_next_solution()==False:
+    solution=try_again()
+    if solution==None:
         break
-    print ("")
 
+    c=GoL_SAT_utils.grid_to_clause(solution, grid, VAR_FALSE, H, W)
+    s.add_clause(GoL_SAT_utils.negate_clause(c))
+    c=GoL_SAT_utils.grid_to_clause(my_utils.reflect_vertically(solution), grid, VAR_FALSE, H, W)
+    s.add_clause(GoL_SAT_utils.negate_clause(c))
+    c=GoL_SAT_utils.grid_to_clause(my_utils.reflect_horizontally(solution), grid, VAR_FALSE, H, W)
+    s.add_clause(GoL_SAT_utils.negate_clause(c))
+    # is this square?
+    if W==H:
+        c=GoL_SAT_utils.grid_to_clause(my_utils.rotate_rect_array(solution,1), grid, VAR_FALSE, H, W)
+        s.add_clause(GoL_SAT_utils.negate_clause(c))
+        c=GoL_SAT_utils.grid_to_clause(my_utils.rotate_rect_array(solution,2), grid, VAR_FALSE, H, W)
+        s.add_clause(GoL_SAT_utils.negate_clause(c))
+        c=GoL_SAT_utils.grid_to_clause(my_utils.rotate_rect_array(solution,3), grid, VAR_FALSE, H, W)
+        s.add_clause(GoL_SAT_utils.negate_clause(c))
+    print ("")