Logic Life Search

[LaundryPizza03]

I can't submit custom inputs using STDIN for some reason; I can use them only as files. Where does the EOF character go?

Are you getting stdin by redirecting from a file or by pasting to the console? If the former then the EOL char comes from the file. If the latter then the EOL char can be provided by typing Ctrl-D after pasting.

If that doesn't help resolve the issue then please provide more details about how you are invoking LLS and what steps you are carrying out.

I'm pasting it into the console. Maybe I keep missing a required newline.

[LaundryPizza03]

I can't submit custom inputs using STDIN for some reason; I can use them only as files. Where does the EOF character go?

Are you getting stdin by redirecting from a file or by pasting to the console? If the former then the EOL char comes from the file. If the latter then the EOL char can be provided by typing Ctrl-D after pasting.

If that doesn't help resolve the issue then please provide more details about how you are invoking LLS and what steps you are carrying out.

It happens for any input that's larger than 1*1. Try pasting this or typing it manually into STDIN. No matter how I enter it, it throws an assertion error "Search pattern is not cuboidal". I suspect that this is a genuine bug.

Code: Select all

a a
a a

a a
a a

[wildmyron]

I can't submit custom inputs using STDIN for some reason; I can use them only as files. Where does the EOF character go?

Are you getting stdin by redirecting from a file or by pasting to the console? If the former then the EOL char comes from the file. If the latter then the EOL char can be provided by typing Ctrl-D after pasting.

If that doesn't help resolve the issue then please provide more details about how you are invoking LLS and what steps you are carrying out.

It happens for any input that's larger than 1*1. Try pasting this or typing it manually into STDIN. No matter how I enter it, it throws an assertion error "Search pattern is not cuboidal". I suspect that this is a genuine bug.

Code: Select all

a a
a a

a a
a a

OK, I can reproduce this now, but only on MacOS. Reproduced with develop branch, using command "python lls". Using Linux under WSL on Win10 I can't reproduce after trying lots of different ways of entering the pattern to STDIN. As a check I modified the assertion to output the search pattern (In the variable "input_string"). For the above pattern it outputs:

Code: Select all

a a
a
a a
a

I guess this means that some code to deal with funny newline behaviour on Windows (under Cygwin) is chomping parts of the input pattern which it shouldn't be.

[LaundryPizza03]

Are you getting stdin by redirecting from a file or by pasting to the console? If the former then the EOL char comes from the file. If the latter then the EOL char can be provided by typing Ctrl-D after pasting.

If that doesn't help resolve the issue then please provide more details about how you are invoking LLS and what steps you are carrying out.

It happens for any input that's larger than 1*1. Try pasting this or typing it manually into STDIN. No matter how I enter it, it throws an assertion error "Search pattern is not cuboidal". I suspect that this is a genuine bug.

Code: Select all

a a
a a

a a
a a

OK, I can reproduce this now, but only on MacOS. Reproduced with develop branch, using command "python lls". Using Linux under WSL on Win10 I can't reproduce after trying lots of different ways of entering the pattern to STDIN. As a check I modified the assertion to output the search pattern (In the variable "input_string"). For the above pattern it outputs:

Code: Select all

a a
a
a a
a

I guess this means that some code to deal with funny newline behaviour on Windows (under Cygwin) is chomping parts of the input pattern which it shouldn't be.

I'm using macOS.

[LaundryPizza03]

I encountered bugged behavior in rules with B0 and S8. One result I got from a generic OT p2 search was:

Code: Select all

x = 12, y = 12, rule = B012345678/S08
bbbbbbbbbbbb$
booobboobbob$
bbbbboboobob$
boobbobbobob$
bobooooobbob$
bbobbooobobb$
bbbooobbooob$
boboboobbobb$
booobbbbooob$
booobbboooob$
booooobobbob$
bbbbbbbbbbbb!

This rule is equivalent to B1234567/S, so it can't be correct. (Note that this is how rules with B0 and S8 are handled by Golly and LifeViewer.)

[LaundryPizza03]

This script should allow you to run most natively supported commands from outside the command line:

Code: Select all

import math, shlex, subprocess

LLS_DIRECTORY = "/Users/gb/logic-life-search" #Replace with the fully qualified directory for Logic Life Search

def generateLLSCommand(solver, rule, bx, by, period, sym='', x=0, y=0, minpop=1, maxpop=-1, subperiod=False):
    bashCommand = ["./lls"]
    bashCommand += ["-S", solver]
    bashCommand += ["-r", rule]
    bashCommand += ["-b", str(bx), str(by)]
    
    def periodArgs(sa, x, y, period):
        args = [sa]
        args += ['p' + str(period)]
        if x != 0: args += ["x" + str(x)]
        if y != 0: args += ["y" + str(y)]
        return args
    
    bashCommand += periodArgs('-s', x, y, period)
    if sym != '': bashCommand += ["\"" + sym.replace('\\', '\\\\') + "\""]
    if not subperiod:
        dis, mul = simplify(x, y, period)
        mulpf = set(primeFactors(mul))
        for p in mulpf:
            bashCommand += periodArgs('-a', x//p, y//p, period//p)
        if 'RE' in sym: bashCommand += ['-a', sym.replace('RE', 'D2').replace('\\', '\\\\')]
        if period == 1 and sym != '':bashCommand += ['-a', 'p1']
    
    assert minpop <= maxpop or minpop == -1 or maxpop == -1, "minpop must be less than or equal to maxpop: %d > %d"%(minpop,maxpop)
    if minpop != -1: bashCommand += ['-p', '\">=%d\"'%minpop]
    if maxpop != -1: bashCommand += ['-p', '\"<=%d\"'%maxpop]
    
    bashCommand = ' '.join(bashCommand)
    return shlex.split(bashCommand)

def simplify(x, y, period):
    gcd = math.gcd(period, math.gcd(x, y))
    return ((x//gcd, y//gcd, period//gcd), gcd)

def primeFactors(n):
    if n in {0, 1}: return []
    elif n == -1: return [-1]
    else:
        i = 2
        while n % i != 0: i += 1
        return [i] + primeFactors(n//i)

def runLLSCommand(solver, rule, bx, by, period, sym='', x=0, y=0, minpop=0, maxpop=-1, subperiod=False):
    bashCommand = generateLLSCommand(solver, rule, bx, by, period, sym=sym, x=x, y=y, minpop=minpop, maxpop=maxpop, subperiod=subperiod)
    process = subprocess.Popen(bashCommand, stdout=subprocess.PIPE, cwd = LLS_DIRECTORY)
    return process.communicate()
    

[pcallahan]

I just installed Logic Life Search and I've been trying it out on examples and other things I can come up with in regular life.

Is there a way to search on hexagonal rules? I don't really understand the rule format at this point. If it is possible to enter a non-isotropic Moore neighborhood rule, I guess I could expand an isotropic hex rule into that format, just by enumerating all symmetries and ignoring two opposite diagonals. Is this a reasonable approach? (I also can't quite figure out if it supports non-isotropic rules.)

[Macbi]

I just installed Logic Life Search and I've been trying it out on examples and other things I can come up with in regular life.

Is there a way to search on hexagonal rules? I don't really understand the rule format at this point. If it is possible to enter a non-isotropic Moore neighborhood rule, I guess I could expand an isotropic hex rule into that format, just by enumerating all symmetries and ignoring two opposite diagonals. Is this a reasonable approach? (I also can't quite figure out if it supports non-isotropic rules.)

No, it only supports isotropic Moore neighborhood rules at the moment. There's a program here that supports hexagonal rules.

[pcallahan]

No, it only supports isotropic Moore neighborhood rules at the moment. There's a program here that supports hexagonal rules.

Thanks. I'll take a look. Maybe I should start working directly with SAT solvers. I will admit that I am only familiar with SAT as a problem you reduce to other problems to prove that they're hard. Actually using it to solve things sounds like fun.

What I've become interested it are still lifes in isotropic hex rules, ideally with periodic boundary conditions. I am curious if there are any rules that can be used to generate random but aesthetically pleasing tilings. With the number of possibilities to choose from, it seems like there should be some surprises.

[pcallahan]

This is really cool. I wish I had known about SAT solvers a few years back. Using just lingeling with my own python script (not lss) I can make periodic still life "wallpaper" very fast (I have some other applications apart from Life and they are static so this is a proof of concept). Here's my script stillsat.py (not well documented, except a few comments; it is a very direct translation of constraints and uses one variable for each life cell).

Code: Select all

import sys
m = int(sys.argv[1])
n = int(sys.argv[2])

def ix(i, j):
  return n * i + j + 1

def neighborhood(i, j):
  neighbors = [ix(i, j)]
  for di in [-1, 0, 1]:
    for dj in [-1, 0, 1]:  
      if di != 0 or dj != 0:
        neighbors.append(ix((i + di) % m, (j + dj) % n))
  return neighbors

def subsets_recur(vals, n, sofar, accum):
  if n <= len(vals):
    if n == 0:
      accum.append(list(sofar))
    else:
      sofar.append(vals[0])
      subsets_recur(vals[1:], n - 1, sofar, accum) 
      sofar.pop()
      subsets_recur(vals[1:], n, sofar, accum)

def subsets(vals, n):
  accum = []
  subsets_recur(vals, n, [], accum)
  return accum

def clauses(i, j):
  res = []
  ngh = neighborhood(i, j)
  # dead if all but one neighbor dead
  for subs in subsets(ngh[1:], 7):
    res.append([-ngh[0]] + subs)
  # dead if any four neighbors live
  for subs in subsets(ngh[1:], 4):
    res.append([-ngh[0]] + [-x for x in subs])
  # live if exactly three neighbors live
  for subs in subsets(ngh[1:], 3):
    inv = [x for x in ngh[1:] if x not in subs]
    res.append([ngh[0]] + [-x for x in subs] + inv) 
  # no dead 2x2 windows
  res.append([ix((i + di) % m, (j + dj) % n) for di in range(2) for dj in range(2)])
  return res

print "p cnf %d %d" % (m * n, len(clauses(0,0)) * m * n)

for i in range(m):
  for j in range(n):
    for clause in clauses(i, j):
      print " ".join([str(x) for x in clause]), 0

It generates a SAT problem for a periodic still life of the given dimensions with the additional constraint that every 2x2 window contains at least one live cell (so you get reasonable density and avoid the trivial empty assignment).

Generate a 20x20 still life SAT, solve it with lingeling, and convert it back to a picture pattern as follows:

Code: Select all

python stillsat.py 20 20 > sat.txt
./solvers/lingeling sat.txt > sol20_20.out
python decode.py 20 20 < sol20_20.out 

decode.py is a small utility to convert the output back to a pattern:

Code: Select all

import sys
m = int(sys.argv[1])
n = int(sys.argv[2])

def ix(i, j):
  return n * i + j + 1

cells = [[0] * n for i in range(m)]

for line in sys.stdin:
  toks = line.split()
  if toks[0] == 'v':
    for x in toks[1:]:
      ix = int(x)
      if ix > 0:
        cells[(ix - 1) / n][(ix - 1) % n] = 1 

for row in cells:
  print "".join(["*" if x else "." for x in row])

Copy-pasting this into Golly I can verify that it tiles with periodic boundaries. Here is a 60x60 composed of 9 copies. (added toroidal boundaries as suggested by dvgrn)

Code: Select all

x = 60, y = 60, rule = B3/S23:T60,60
bo3b2obo3bo2bobobobo3b2obo3bo2bobobobo3b2obo3bo2bobobo$ob2obo2bob2ob2o
bobobob2obo2bob2ob2obobobob2obo2bob2ob2obobo$2bo2bobobobo2bobo2bo2bo2b
obobobo2bobo2bo2bo2bobobobo2bobo2bo$bo2bobo2bo3bo3bobobo2bobo2bo3bo3bo
bobo2bobo2bo3bo3bobo$2ob2obobo2bobob2obob2ob2obobo2bobob2obob2ob2obobo
2bobob2obo$3bo3bob2obob2o2bo4bo3bob2obob2o2bo4bo3bob2obob2o2bo$b2o2b2o
2bo2bo4bobob2o2b2o2bo2bo4bobob2o2b2o2bo2bo4bobo$o2b2obobo2bob3obob2o2b
2obobo2bob3obob2o2b2obobo2bob3obobo$2bo3bob2obo2bo2bo4bo3bob2obo2bo2bo
4bo3bob2obo2bo2bo$3ob2o5b2o3bo2b4ob2o5b2o3bo2b4ob2o5b2o3bo2bo$3bo2b4o
2bobob4o3bo2b4o2bobob4o3bo2b4o2bobob4o$bobobo3bobo2b2o5bobobo3bobo2b2o
5bobobo3bobo2b2o$2obo2b2obob2o4b2ob2obo2b2obob2o4b2ob2obo2b2obob2o4b2o
$bo2b2o2b2o2bob2obo3bo2b2o2b2o2bob2obo3bo2b2o2b2o2bob2obo$2b2o2bo3bobo
2bo2b2o2b2o2bo3bobo2bo2b2o2b2o2bo3bobo2bo2b2o$2o2bobob2obobo2b2o2b2o2b
obob2obobo2b2o2b2o2bobob2obobo2b2o$2bob2obobobob3o2b2o2bob2obobobob3o
2b2o2bob2obobobob3o2b2o$bobo3bo3bo4bobo2bobo3bo3bo4bobo2bobo3bo3bo4bob
o$2o3b3obobob2obobob2o3b3obobob2obobob2o3b3obobob2obobo$2b3o3bob2o2bo
2bobo2b3o3bob2o2bo2bobo2b3o3bob2o2bo2bobo$bo3b2obo3bo2bobobobo3b2obo3b
o2bobobobo3b2obo3bo2bobobo$ob2obo2bob2ob2obobobob2obo2bob2ob2obobobob
2obo2bob2ob2obobo$2bo2bobobobo2bobo2bo2bo2bobobobo2bobo2bo2bo2bobobobo
2bobo2bo$bo2bobo2bo3bo3bobobo2bobo2bo3bo3bobobo2bobo2bo3bo3bobo$2ob2ob
obo2bobob2obob2ob2obobo2bobob2obob2ob2obobo2bobob2obo$3bo3bob2obob2o2b
o4bo3bob2obob2o2bo4bo3bob2obob2o2bo$b2o2b2o2bo2bo4bobob2o2b2o2bo2bo4bo
bob2o2b2o2bo2bo4bobo$o2b2obobo2bob3obob2o2b2obobo2bob3obob2o2b2obobo2b
ob3obobo$2bo3bob2obo2bo2bo4bo3bob2obo2bo2bo4bo3bob2obo2bo2bo$3ob2o5b2o
3bo2b4ob2o5b2o3bo2b4ob2o5b2o3bo2bo$3bo2b4o2bobob4o3bo2b4o2bobob4o3bo2b
4o2bobob4o$bobobo3bobo2b2o5bobobo3bobo2b2o5bobobo3bobo2b2o$2obo2b2obob
2o4b2ob2obo2b2obob2o4b2ob2obo2b2obob2o4b2o$bo2b2o2b2o2bob2obo3bo2b2o2b
2o2bob2obo3bo2b2o2b2o2bob2obo$2b2o2bo3bobo2bo2b2o2b2o2bo3bobo2bo2b2o2b
2o2bo3bobo2bo2b2o$2o2bobob2obobo2b2o2b2o2bobob2obobo2b2o2b2o2bobob2obo
bo2b2o$2bob2obobobob3o2b2o2bob2obobobob3o2b2o2bob2obobobob3o2b2o$bobo
3bo3bo4bobo2bobo3bo3bo4bobo2bobo3bo3bo4bobo$2o3b3obobob2obobob2o3b3obo
bob2obobob2o3b3obobob2obobo$2b3o3bob2o2bo2bobo2b3o3bob2o2bo2bobo2b3o3b
ob2o2bo2bobo$bo3b2obo3bo2bobobobo3b2obo3bo2bobobobo3b2obo3bo2bobobo$ob
2obo2bob2ob2obobobob2obo2bob2ob2obobobob2obo2bob2ob2obobo$2bo2bobobobo
2bobo2bo2bo2bobobobo2bobo2bo2bo2bobobobo2bobo2bo$bo2bobo2bo3bo3bobobo
2bobo2bo3bo3bobobo2bobo2bo3bo3bobo$2ob2obobo2bobob2obob2ob2obobo2bobob
2obob2ob2obobo2bobob2obo$3bo3bob2obob2o2bo4bo3bob2obob2o2bo4bo3bob2obo
b2o2bo$b2o2b2o2bo2bo4bobob2o2b2o2bo2bo4bobob2o2b2o2bo2bo4bobo$o2b2obob
o2bob3obob2o2b2obobo2bob3obob2o2b2obobo2bob3obobo$2bo3bob2obo2bo2bo4bo
3bob2obo2bo2bo4bo3bob2obo2bo2bo$3ob2o5b2o3bo2b4ob2o5b2o3bo2b4ob2o5b2o
3bo2bo$3bo2b4o2bobob4o3bo2b4o2bobob4o3bo2b4o2bobob4o$bobobo3bobo2b2o5b
obobo3bobo2b2o5bobobo3bobo2b2o$2obo2b2obob2o4b2ob2obo2b2obob2o4b2ob2ob
o2b2obob2o4b2o$bo2b2o2b2o2bob2obo3bo2b2o2b2o2bob2obo3bo2b2o2b2o2bob2ob
o$2b2o2bo3bobo2bo2b2o2b2o2bo3bobo2bo2b2o2b2o2bo3bobo2bo2b2o$2o2bobob2o
bobo2b2o2b2o2bobob2obobo2b2o2b2o2bobob2obobo2b2o$2bob2obobobob3o2b2o2b
ob2obobobob3o2b2o2bob2obobobob3o2b2o$bobo3bo3bo4bobo2bobo3bo3bo4bobo2b
obo3bo3bo4bobo$2o3b3obobob2obobob2o3b3obobob2obobob2o3b3obobob2obobo$
2b3o3bob2o2bo2bobo2b3o3bob2o2bo2bobo2b3o3bob2o2bo2bobo!

I realize that generating still lifes is not a hard problem (without constraints anyway) but I was still very impressed with the speed of this approach. It requires 1 boolean variable and 135 clauses per cell.

Added. So with a 128x128 pattern, it is not quite real time. I had to wait 18 seconds for lingeling to solve it. That's still amazing. This is periodic, but I'll just include one copy.(added toroidal boundaries as suggested by dvgrn)

Code: Select all

x = 128, y = 128, rule = B3/S23:T128,128
obo4bobobob2obo2b2o5bobo2bobo3bo3b2o4b2o3bob2obo3bob2o4bobo2b3o4bob2o
3bob2o2bo3bo5bob2o3bo4bob2obob2o$2bob2obobob2obob3o2b3obo2bobo2b4o2bob
ob2ob2o2b2obo3b4o4b2obo2b2obo3b3ob2ob2obo4bob4obob2obo3b2ob3obo2bobo2b
obo$3ob2obobo4bo4b2o3b2ob2ob2o5b3o4b2o3b2o2bob2o3bob2o2bob2o3bo2b2o2bo
5bob2ob2obo4bob2o2bob2obobo2b2obo2bobo2b2o$8bob4o2b3o3bo3bo4bob2obo3b
3o4b2o3b2obo2bobo2bobo4b2o2b2obobo2b3obo2bobo2bob2obo4bobobo4bo4bob2ob
2o$ob2ob2obobo3b2o4b2ob3o2b2obo2bobobo3b5obob2o3bob2ob2obo2b3obob2o5b
3o3bobo2bo2bobo2bob2ob2obo2b3obob2obobo4b2o$2obobo2bobob2o3b3obobo2b2o
2bobo2bobob2o5bo2bo2bob2obo2bo2b3o2bobo4b4o3b2obob2obob2o2bobo2bobo2b
3o3bobo2bo2bob3o2bo$6b3ob2o3b2obo2bo2bo3bobob2obobo3b4o2bobobo5bobo2bo
3b2o2b2ob2o4b2o3bo4bobo2b2o2bobo2bobo3b2obo2bobobobo3bo$ob4o3bo3b2o5bo
bob3obo2bo3bobob2o3bob2o2bob2ob3obob2obo3b2o2b2o2bobo2b2obob2o2bo2bo2b
2o2bobo2bobo2bo2bobobobo2b2ob2o$2o4bobo2b2o2b6obo4bobobob3obo2bobo2bo
2bobo2b2o3bobo2bob3o2bo4b2ob3o2bobob2obob2obo2b3obobo2b2obob2o2bobobob
obo2bo$3b3o3b2o2bo2bo6bobo2bobobo4b3o2b2obob2o2bo4bobo3bo2bo2bob4obo5b
obobo3bobo2bobo4b2obobo3b2o2b2o2bobo4bo$2obo2b3o2bob2o3bob2obob2obobo
2b3o4b2o2bobo2b2ob4obo2bobobo2bobo4bo2b2ob2ob2ob2obo3bo2b2obo3bobob3o
3bo2b3o2b4ob2o$bo3bo2bobobo2b5obobo3b2o2bobo2b3o4bo2bobo2bo5bob2obo2b
3obob2o2b2obobo5bobob4obo2b5o2bo4b2ob3o3b2o3bobo$o2bobobo2bo3bo7bob2o
3bobo2bo4b2ob2obo2b2o2b4obo2bob3o4bo2b2obo4bob2obo4bo3bobo6b2o2b2o3bo
3b2o3b2obobo$ob2obobobo2bob4ob2obo3b3ob2ob2ob2o2bobo2b2o3b2o4bobobo4b
3o2bo4bob4o2b2ob4o2bobo2b2obobo2b3ob2o3b2o2b3o2bobo$bo3bobo2b2obo4b2ob
ob3o2bo4bo2bob2o4bo2b2o2bob2obobo2b3obo2b3ob2ob2o4bo4bo3b2obob2o2b2obo
bo6b3o2b2o2bobo2bobo$2bobobobobo2bob2o4bobo3bo2b2o2bobo2bob3obo2bobo2b
obo2b3o2bobobo3bobo4b2ob3obo2bo2bobo3bo4bob2ob2obo3bo4bo2bobo2bo$b2obo
bobo2b2obobob3o3b2obob2ob2obob2o2bo3bobo2b2obo2b2o4bo2bobobo4bob2obo4b
2ob2obo3bobob3obo2bobo3b3ob2ob2ob2ob2obo$o3bob2obobo2bo3bo2b2obobobo4b
obo2bobo2b3o2b2o2bobobo2b2obobobob7obo2bob2o4bo2b2ob2obo4bobobobob2o4b
o4bo6bo$2b2obo3bo3bob3o2bo2bo2bobob2obo2bo3b3o3b2o3bo2bo2bobob2obobo
10bo2bobob2obobo6bob2o3bo2bobo2b3o2b4o2b4o$obo2bob2ob3o2bo2b2obo2b2o2b
o2bob4obo4bobo3b2ob2ob2obo4bo3b2obob4ob3o2bo2bobo2bob3o2bo2b3obobobobo
3b2o4b2o3bobo$obob2obo2bo2b2o2bo2bob2o2b3obo7b2ob2ob2ob2obo4bo2bob2o2b
3o2b2obo2bo4b3obo2bob2obo2b2o2bo4b2obobobobo2b3o2bobo2bo$o2bo4bobobo2b
2obobo3bo4bob2ob4o4bo4bo2bob2obob2obob2o3bo6bo2b3o4bob2obo2bobo2b2ob2o
bo3bobob2obo3bobo2b2obo$bobob3obo2bobo2bobobobob3obo2bobo3b3o2b3o2bobo
2bobobo2bobo2bob4obob2obo2b2obo2bo3bobob2o2bobo3b3obo5b3o3b2o4bo$bobo
2bo2bobobob2o2bobobo3bo2bo4bobo3b2o3b2o2bobo2bo2bobo3b2o5b2o2bo2bo2bob
2obob3o2bo2b2o4b2o2bobob2obo3b3o2b2obobo$o3bo3b2obobo2bobo3bob2o2b3obo
b2ob4o2b3o2b3ob2ob3o2b4o2b4o3bo2bob2obobo2b2o3bobobo2b4o2bo3b2obob2obo
3b2o2b2o$ob2ob3o3bo2bo2bob2obobob2o3b2obo5bobo4bo6bo3b2o4bo3bob2ob2obo
3bo3bo4bobobob3o4bo2b3o9bobo2bo3bo$b2o2bo3b2obob2obo3bobo5bo5b4obob2ob
2o2bob3o2b2o2b2obob2o4b2o2bob2o2b3ob5o2bo6bobob2o3b2obob2ob2obob2ob2ob
o$4bo2b2o3bo2bob2obo2bob2ob2ob4o2bobobo4bob2obo2b2o2bo2bobo3b3o4bo2bob
2o3bo5bobob3ob3obo2bobo2b3obobo2bo2bobo2bo$b3ob2obob3obo3bobobo2bo4bo
4bo5bob2o2bo5bo2bo2b2o3b2obo2b3ob3o4b2o3bobobobo2bo6bob2ob2o5bo2bob2ob
o2bobo$o3bo4bo4b3obobob2obob2obob3ob5obob2obob5obob2o2b2obobo2bo2bo4b
3o3b3ob2o2bobo3b3obobo5b4ob3obo3bob2o$2bobob2obob3o3b2obo2bobobo2bobo
3bo4bo4bo2bo4bobo2bo2bobo2b2obo2b3o3bob2o2bo3b2o2b4o2bobo2bob2o3bobo4b
ob3o3b2o$3obobobo2bo3bo4b2o3bobobo3bobo2b2obob2o2b2o2b2o3bobob2o3b2o2b
ob2o3b2obo2bobo2b2o2b2o5bo2b2ob2o2b2o3bobobobo4b2o$4bobobobo2b2ob4o2b
4obo2b2ob2ob2obobobob2o2b2o2b3obobo2b3o2bo2bo2b3o2bobo3b3o2b2o2b4obobo
2bo3bo2b3obob2o2b4o2b2o$b2obobobobob2o2bo2bobo6bobobo3bo2bobo2bo3bo2bo
bo2bo2bobo3bob2obobo3bo3bobo4bo3bobo3bob2obo2b2obobo3bo3b2o4b2o$2ob2o
2bobobo3bo2bo2b8obo2b2obob2o2b2o2b2ob3o2bobobo2bobo2bo3bob4ob3o2b4o2b
4obobobo4b2obo2bobob2ob2obo2b2o3bo$5bobo2bo2b2ob2ob2o10bobobobo2b2o2b
2obo4bobo2bob2obob2o2b2obo4bo2bobo4b2o4bob2o2b4o3bobo2b2obo2bo2bobob3o
$2ob2obobobob2o2bo2bo2bob4ob2obo2bo2bo3bobo2bob2o2bobobo2bobo3b2o3bob
2o3bo2bob3o3b2obo3bobo3b2o2bob2o4bobob2obo4b2o$bobo2bo2bobo3bo2bo2b2ob
o2bobo2bobob2ob2obobob2o2b2obo2bob2o3bobo2b2obobob3ob2obo4b2obob2ob2o
3bo2b2obo3bob2obobo4bob2o$bo2bo2bobo2b2ob2ob2obo4bo2bobo2bobo2bo2bobo
3bo4b2obo3b4ob2o3bo3bo4bo2bob3o3bobo5bob2o4b2ob2obo2bobob2obobo2bo$ob
2ob2obobobobo3bo2bob4obob2obo2bobo2bobob4ob2o2bobob2o4bo2b2o2b3o2bobo
2b2obo2b3o3b4ob2o2b4o4bo2bobobobo2bo2b2o$o2bo2bo3bo4b2o2bo2bo5bo3bob3o
b2obobobo4b2obo2b2o3b2o2bobob2o2bob2ob3o3bobo3b3o4bo3bo5b2o2b2obobo3bo
b2obo$2o2bobobo2b4o2b2ob2o2b4ob2obo4bo2bobo2bob2o4bobo3b2ob4o2bo2bobo
7bobo2bobo3bob2obob2ob5ob2obo2bo2b4o2bo2bo$2b2obob3obo3bo2bo2bob2o4bo
2b2obo2bo3bobobob4obo2bob2o6bobobobo2b4ob2obob2ob3obobo2b2obo9bo2bob2o
4b2o2b2o$o4bo4bo2bob2o2bo2bo3b2o2bo2bob2ob5obobo4b2obob2o3b3obobob2o2b
2o3bobo2bo2bo4bo4bo3bob4ob2obob2o2bob3o2b2o2bo$ob2ob4obob3o2b2ob2o2b2o
b2obobo4bo5bobobobo4b2o3b2o2bobobo3b2o2b2obobob2obo2b2o2b5ob2obo3bob2o
bo2bobo2bo2bo3bo$o2bo4b2obo4bo2bo2b2obo3bo2bob2o2bob2obobobob4o4b2o2bo
bobo2bobo2bo3bo2bo4b2obob2o6bo2bobobo4b2obob3o2bob2ob2o$3o2b2o4bob2ob
2o2bobo3b2obob2ob2ob2obo2b2obobo4b4obobobo2b2ob2ob2ob2obob2ob2o4bo3bob
3o3bob2obob3o2bobo3b3obo2bo$3b2o2b3obobobo2b3o2b2obobobo6bo2bobo3bobob
2o5bo2bobobo2bo3bo2bo2bo2bo2b2ob2ob2obobo2b4o3bobo3bobo2b3o5bobobo$obo
2b2o2bobobo2bo4bobo2bobo2bob3o2bobobob2o2b2obob3obobo2bo2bo2b3o2bo2bob
o2bo5bobo2bo2bobo3b2o3bobo2bobobo2b5obo2bo$3bo2bobo2bo2bobob2obo2bobob
2ob2obob2obobobo2b2o3bo2bobobob2obob2obo2b3ob2obob2ob2obo3bob3o2bobo2b
obo2bob2o2bo2b2o4bobobo$2ob2o3bob2ob2obobo2bob2obo2bo6bo2bobo2bo2bob2o
bo3bo3bo2bobo2bobo4bo2bobo2bob2ob2obo3b2o2b2obob2obo3b2obobo2b2obob2ob
o$2bo2b3obo3bo2bo2bobo2bobobo2b5o2bobobobobo2bo2b4ob3o2bo3bob2ob3o2bob
obobo5bo2bob2o2b2o2bo4bob2o3b2o3b2o2bo4bo$o2bo3bo2bobo2bo2b2obobo2bob
2obo4b2o2bo2bo2b2obobo5bo2b3ob2obo3bo2b2obob2o2b5o2b2obo2bo2bo2b3obobo
b2o3b3o3bo2b2o$b2ob2o2bobob2ob3o2bobob3o2bo3b2o3b2obobobo3bo2bob2obobo
3bobo2b2o2bo2bobo3bobo4b2o4bobobob2o2bobobobob2o4b2ob4ob2o$bo2bob2obob
o2bo3bo3bo4bo2b3o2b2obo2b2obobobobob2obobo2bobo3bobob2ob2o3bobobo2bobo
3b4o2bobo2bobo2bo2bo2b5o2bo$bobo2bo2bobobo2b2ob3ob4ob2o3bobobo2bo3bob
2obobo4bobobob2ob2obo3bo2b4obobob2obob2o4b2o2bob2o2bobobobo5bobo2b2ob
3o$2ob2obob2o2bob2obobo2bo3bobo2b2o2bo2b2obob2o4bobob2obobobo5bob2obo
2bo5bo2bo3bobo2bobo2b3o3bobobobob2ob2o2bob2obobo$2bo2bobo2bobobo2bo2bo
2b2obo2b2obobobobo2b2o3b2obobobobobobob5o2bo3b3ob2obob2o2b2o2bob2ob2o
4bob2ob2obo6b2obo2bobo2bo$o3bo2bob2obobobobob2obobobobo4bobo3bo3b2o2b
2obo2bo2bo2bo4bobo2b2o3bobobo3b2o2b3o3bo2b3ob2o6bob4o4b3o3bob2o$b3ob3o
2bobobobobo2bobo3bo2bobobobobob4o2bo4b2obobobobob2obo2b2obobobo3bob2o
2bo4bobo2bo3bo3b2ob2obobo2b3o4b2obo$bo2bo3bo2bo2bobobobo2bobobob2ob2ob
obobo4bob4o3b2obobo2bobob3o4bobo2bob2o3b2ob2obob3obobo2b2ob2o3bo3bo2bo
b2obob2ob2o$2bo2b2ob2obobo2bobobobobobobo6bo3bob3obo4b2o4bob2obo6b4o2b
ob2o4b2o2bobobo5bob3obo4b2ob3obobo2bobo3bobo$2ob2o2bo2b2obob2obob2obo
2bo2b4obo2bo2bo3bo2b2obob2obo4bo2bob2obo3b3o2bob2obo2bo2bo2b4obo5bob3o
bo4bo2b2obob3o$2bo2bo2bo5bo3bo4bobob2o3bobob3obobo2b2obobobob2ob2obob
2obo2bob2o3bo3bobo2b2obob2o3bo2b4o2bobo4b2o2b2o2bo5b4o$bo2b2ob2ob4o2b
2o2b2obobo2bob2o2b2o4bob3o2bo2bobo4bob2o2bo2bobo2bobob4o3b2o2bo2bo2bo
2bobo3b2o4b3ob3o2bobob3o4bo$b3o2bo2bobo2b2o2b2obobo2bo2bo2b2o3b4o4bo2b
2obob2obo4bo2b2obob2o2b2o3bob2o2bobobo2b3obo2b3o2b4o8bobobo3b2obo$o3bo
3bo4bo2bobo4b2ob2obobo2b2obo3bobob2obo2bo2bobob2o2b2o3bo3b2o3bobo2bob
2obob3o4b3o4bo5b2ob5o2bo2bo2bobo$bobob3ob5ob2o2bobo2bo4bob2obo2bob2ob
2o3bo2bobo4bob3o3b3ob2o3b4obobo2bobo4b2obo4b4obob2obobo4bobob2obo2bo$b
obobo3bo4bo2bobob2o2b4o2bo2bob2o2bo3b2obob2ob5o5b3o3bobob2o5bobobo3b3o
2bobob2obo3bob2o2bo3b2ob2obo3bobobo$ob2o3b2o2bobo2bobo4b2o4b2o2bobo2bo
2b2obobobo2bo5b3obo3b2obo3bo2b2ob2obo2b3o2b2o3bobo2bobobo4bob3o2bo3bob
3o2bo$o3b3obob2obob2o2b4o3b2o3b3o2bob2obobo2bo2bo2bob2o3bob3o2bobobobo
b2o5b3o3bo3b3obo2bo2b2obob2obo3bo3b2obo3b2o$b3o2bo2bo2bobo2bobo3bob2ob
3o3bob2o3bo2b2obob2obobob2obo4b2o2bob2obo3b4o4bob2obo2bo2b2ob2o3bobo2b
ob2ob3obo3bo2bobo$4bo2b2o2bo2bobo2bob2o5bo2b2o2bo3b2obobo2bo2bobo3bobo
b2obo2b2o5bob2obo2b4obo4bo2b2o2bo2b2obobobobobo2bo2bobob2o3bo$b3ob2o2b
3obo2bobobobob3o2bobob2o2b2o3bobobobobo2b3o2bobo3bo3b3obobo5bo3bobob2o
b3o2bo2bo2bobobo2bo3bo3b2ob2o2b4o$2o2bo3bo3b2obo2bobobo2bob3o2bo2b2o3b
2o2bo2bobob2o2bobo3b2obob2o3b2obob5obobo2bo2bo4bob2ob2o2bob2obob2ob3o
6bo$3bo2b2ob2o4bobo2bo2bo6bobobo2b3o2b2obobo2bo2bo2bob2obobobo2b2o4bo
2bo3bobobobobo2b2obo2bo2bobo4bobobo2bo2b2ob2obobo$b2ob2obo2b3obo2bobob
2ob5obobo2b2o4bo3bo2b2o2bob2o2bo2bobobobo2b3ob2o3bo3bobobob2obo2b2o3bo
2bob2obobo2bo3b2ob2o2bob2o$2bo2bo2bo4b2obob2obo2bo3bo2bob2o2b3ob4ob2o
2b3o2bobo2b2obobo2bo3b2o2b3ob3obob2obo2bobo2b4obobo2bobobob4o6bobo$o2b
o2b3ob2o3b2o5bo3bo2bobo3b2o2bo6bo2bo4bo2b3o2bobob2ob2o4bo2bo5bo6b2o2bo
bo4bo2bobobobo6b6obobo$b2ob2o3b2ob2o3bob2ob5ob2obob2o2bo3b4o2bobob2ob
3o4bo2bobo2bob2ob2obo2b3o2b6o3b2o3b2ob2obo2bobob2ob2obo7bo$o2bo2b2o4bo
b2obobobo5bo3bo2bobob3o4b2obo2bobo3bob3obobo2bo3bobo2b2obo2b2o6b2obo2b
ob2o4b2obobo2bobo2bob5obo$obo2bo2b3obobo2bobo3b3o2b2ob2o3bobo2bobo4bob
o4bob2o4bo2b2ob3o2bobo3bobo3b2obobo2bob2o4b2o2bobo2bobobobo2bo3bobo$ob
3ob2o3b2o2bobobobobo2b2o2bo2b3obo2bob2ob2obob2obob2o3b2o2bobo2bo2b2ob
2ob2obob2obob2o3bobo3b4ob2o3bobob2obob2o2bobobo$bo3bo3bo3bobo2bob2o2bo
bo2bo2bo2bobob2o3bobobo3b2o4b2obob2o2bo2bo2bo3bo3bo2bo5b4o2b3o7b2obobo
4bo3b3obobo$bobo3b2ob2obob2obo3b3o2b2ob2obobobo3b2o3bob3o4b2obo2bo3b2o
b3obo2b2o2b2obo2b4obo3b2o2bob2ob3o2bo2b6ob2o4bo2bo$b2ob3obobo2bo3bo2b
2o3b2o3bo2bo2bob2o2bobo2bo3b4obo2bo2bobo2bo4b3o2b2o3b2obo3bo2b2o2bo2bo
b2o3bo2b2o6bo3bobob2o$o3bo3bo2bob3o2b2o2b2o3bobo2bobobo2bobo2b3o2b2o2b
o3bobob2obobo2b2o4bo3b2o3bo2bo2b2o2bob2obo4bo2b2o2b4obo2b2ob2o2bo$ob2o
2b2o2b2o4b2o2b2o2b4ob2obobobobo2bobo3b2o2bo3b2o2bo2bobo2b2o2b4ob3o2b2o
2b2ob2o2bobo3bob3ob3o2bo4bob3obo4bo$bo2b2o2b2o2b3o3bo3b2o8bobo2bob2obo
b2o2bobob3o2b2ob2o2b3o2bo5bo2bobo2b2o3bo2bobo2b2o2bo2bo4bob3o2bo4bob2o
bobo$2bobo2bo2b2o3b3ob3o3bob6ob2obo4bo2b2o3b2o2bobo2bo2b2o4bob4obobo2b
2o3b2obob2o2b2obobo2bo2bob2obo2b2o2b3o2bobo2bo$obo2bob2o3b2o3bobo2bob
2obo8bo2b3obo3b3o3bo2b2o3bo2bob2obo4bo2b2o3b2obobobo2b2o3bobob2ob2obo
2bobo2b2o2bobo2bobo$ob4o3b2obob2obobobo6b2obob2o2b2o4b2obo3b3ob2o2b3ob
obobo2bob2obobo2b2o2bobobobobo2bobo2b2o3bo2bob2o2bobo2bo2bobobo$6bobo
2bo2bobobo2bob2ob2o2b3ob3o3b2o2bobobo3bo2bobo4bobo3b2obo2b2obo2bobo3bo
2b2obobobobo3b2o2bobo2bobo3b2obobo2bobo$4ob2ob2obobo2bo2b2obob2o2bo9b
2obobo2b2ob2o2bobo2b4obob3o3bobo3bobo2b3obobo3bobobobob2obob2obob2ob4o
3bobobobo$o2bobo4bo2b2ob3o3bo4bob4ob5o2bob2o4bob3o2b2o5bobo2b2obo2b2ob
ob3o3b2ob2obob2obobobo2bo3bobo6bob2obobo2bo$bo4b3obobo2bo3b2obob2ob2o
3bobo5bobo2b4o5b2o2b5obo2bo2bobobo2bo4b2o5bobo4bobobobobobo2bob2obo3bo
2bobobo$b4obo2bobobo2bobo2bo2bobo3bo3bobob2obo2bo4b4o2bobo6bob2obo2bo
3bobobo2bob2obo2b5o3bo2bobob3o2bob2obobob2ob2ob2o$o3bo2bobo3b2obob2o2b
2o3b4obo2bob2o2bob2ob2o4b2obob8obo2bobob3obob3obobob2obo5b2obob2obo4b
2o4b2obo2bo4bo$ob2o2b2obobo3bobo2b2o2b3o5b2obo4b2o3bobob2o4bo10bob2obo
3bobo4bobo5b5o2bobobo2bob2o3b3o4bobo2b2obo$2o2b2o4bob2obo2bo3bobo3bob
2o2bob4o2bobo2bob2ob2ob4ob4obobo2bob2o2bob2obo2bob2obo5b2o2bo2bob2ob2o
bo3b4o2b2obobo$3bo3b2obo2b2ob2ob2obo3b3obo2bo2bo2bob2obob2o4b2o4bobo3b
2o2bobo2b2obo3b2ob2o2b2ob2ob2o2b2ob3o8b3o3bobo2bo2bobo$b2ob2obo2b2o4bo
2bobob3o5bob2o2bobo5bo3b2o4b3o2bobo3b3ob2o3bob2o3bo2bo4bob2o2bo2bo3b5o
b2o2bobo2bobobob2obo$2bo2bobobo2b3o2bobo3bo3bob3o3b3ob2ob3o2b3ob3obo2b
2obob2o7b2obo2b2obo2bob3o6b2obo2bobo3b2obobo2b2obobobo2bobo$o2bobobo2b
obo2b2o2bobo2b5o3b2o6bobo2b2o6bo2bo4bobob2ob2obo2bobo5b2obo3b5obo2bob
2o2b2o6bobo2bobobo2bo2bo$b2obo2bob2o2bo2bobo2b2obo5bobob2ob2obo2bo2bob
ob2o2bob3obobo3bob2ob2o3bob3obo2bobo6bo2bobo2bobob7o2bobobobob2obo$4bo
b2o3bobobo2b2obo2bob2ob2obo2bobo2b4obo2b2ob2obo4b2o2b3o6bobo2bo2bobobo
2b3ob2o2b3obobo2bobo6b2obobo2bo4b2o$b4o3bobo2bob2o3bo2bobobobo3bobo2b
2o5b3o5bobobo3b2o2bob4obob2obobo2bobobo3b2ob2o4bobob2obob2obo2bobobob
2ob2o2bo$bo3b4ob2obo3b2obob2o2bo3bob2o2bobo2b2obo3b3obo2bob2obo2bo2bo
4bobo3bob2obobobobo4bo2b2obobobo3bobob2obobobo4bob2o$o2bo5bo2bob3o2b2o
3bobob2o5b2o2b2obob2obo2bobob2obo3bob2obob2obo2b4o3bo2bobob4obob2ob2ob
o2b2obobo2bobo2bob3obo2bo$b2ob4o2bobobo2bo3bobo2bo2bob4o2b2o2bo3bob2ob
obo2bo2bob2obo2bo2bo2bobo3b2o2b2o3bo4bobo6b3o2b2o2bobob2obo3b2obobo$o
2bo3bob2obobobob2obobobobo2bo3bobo2bobob2o5bobobo2b2obo3bob2o2b3obob2o
2b2o2b2obob2obo2b4obo3bo3bobobo4b3o4bo2bo$bo3bo2bo4bo2bo2bo2bob2ob2obo
b2o2bobobobo2b5obobob2o5b2obo2b2o5bo2b2o2b2o2bo2bo2b2obo2bob4ob2obobob
ob3o3b2obob2o$bobob2obob2obobobo2bobo6bobobobobo2bobobo3bo2bo2bo3b4obo
2b2o2bob2obobo2bo3bobobo2bo3bobo7bo2bobob2o3b2o3b2o3bo$ob2o2bobobobo2b
ob3obob2ob2obobobobo2b2obobob2o3bobobob2o6bobo2bob2obobob3ob2obobob2ob
obo2b4ob2o2bobob2o3bobob2o4b2o$o3bo3bobobob2o5bo2b2obo2bo2bob2obo2bobo
bob3obobobo2b2ob3o2bob2o6bo4bo3bobo3bob2obo3bobob2o2bo4b2obo2bob4obo$b
2ob4o2bobo4b2obobo5bobobo2bo2bob2obo7bobo2bo2b2o3b2obo2bob5ob2o2b3o3b
2obo4b3o3bo2bob2ob4o2bobo2bo5bo$bobo3bob2ob2ob2obobo2b2ob2o2bob3o2b2o
5b7o3bob2o4bobo2bobob2o4bob3o3b3o2b2ob2o4b3obobo3bo5bo2bobo2bob2o$o2bo
bobobo3bobo2bob2obo3bobobo3b2o3b3obo6b3obo2b2ob2o3bo2bo4b2obo5bo4bo3bo
2b4o3bobo2b2o2bob2ob2obob4obo$b2obobo3b3o2bob2o2bo2b2obo2bo2bo2bob2o2b
o3b2obo3bo2bobo3bobob3ob2ob2obobob2ob4ob2obo2bo4b2obo2b2obob2obo2bo2bo
7bo$bo2bobob2o3b2obo2bo2bobobobobob3obobo2bo2bobob3obo2b2o2bobo2b2o4bo
7bobobo3bo2bob2obob2obobob2o3bobo2bobo2bob2ob4o$o2bob2o2bobo4bobob2o2b
o3bo2bo3b2o2bobob2obo6b2o2b2ob2obo3b2o2bob6obo2b2obobo4bobobo3bo2bob2o
2bobo2b4o2bobo2bo$ob2o3b2o2b2ob2obobo2b2ob3ob2o2bo3b2obobo2bob6o2bo2bo
4bob2o2b2ob2o5bobobo2bobob3o2bo3bo2bo2bobobo2b2o6bo3bo$o3b2o3b2o4bobo
2bo4bo2bo2b2ob2obo2bo2bobo2bo5b2obo2b2ob2o2bo2bo4b3obo2bo2bo2bobo2b2o
2bob2ob3o2bobobo2b2ob2ob4ob3o$b2obob3o3b2obob2obob2o2bo2bo4bobo2bobobo
b2o3b4o3bob2obo3b2obo2b2obo2bobobob2obo3b2o2b3o2bo4b3obo2bo2bobobo3bo$
2bobo4b3o2b2o3bobob2obob2ob2obobob2obobo3b3obo2bobobo5b2o2bob2obo2bobo
2bobo2bob3o2b2o3b2o2b2o6bob2obobo2b2o2b4o$2o2b2ob2o3bo3b2o3bo3b2o2bob
2obobobo2bo2b2o3bo3b2obo3b4o2bobo5bobob2obo2bo3bo2b2o2bobo2b2o2b7o3b2o
b3o2b2o2bo$bobo4bob2ob3o2b3ob2o4bo5bobo3bob2o2b3o2bobo2b4o4bobo2b5ob2o
4b4obo2bo3bobob2o3bobo6b2o7b2o2bo$o2b4obo2bo4bobo3bob3obob2obobob4o3b
2o3b2obo2bo3bob2obob2obo3bo3b4o5b2obob2obobo2b4o3bob3o2b4obo3bo2b3o!

[dvgrn]

So with a 128x128 pattern, it is not quite real time. I had to wait 18 seconds for lingeling to solve it. That's still amazing. This is periodic, but I'll just include one copy.

In case you're not familiar with this, LifeViewer supports Golly's torus bounded-grid syntax:

Code: Select all

x = 128, y = 128, rule = B3/S23:T128,128
obo4bobobob2obo2b2o5bobo2bobo3bo3b2o4b2o3bob2obo3bob2o4bobo2b3o4bob2o
3bob2o2bo3bo5bob2o3bo4bob2obob2o$2bob2obobob2obob3o2b3obo2bobo2b4o2bob
ob2ob2o2b2obo3b4o4b2obo2b2obo3b3ob2ob2obo4bob4obob2obo3b2ob3obo2bobo2b
obo$3ob2obobo4bo4b2o3b2ob2ob2o5b3o4b2o3b2o2bob2o3bob2o2bob2o3bo2b2o2bo
5bob2ob2obo4bob2o2bob2obobo2b2obo2bobo2b2o$8bob4o2b3o3bo3bo4bob2obo3b
3o4b2o3b2obo2bobo2bobo4b2o2b2obobo2b3obo2bobo2bob2obo4bobobo4bo4bob2ob
2o$ob2ob2obobo3b2o4b2ob3o2b2obo2bobobo3b5obob2o3bob2ob2obo2b3obob2o5b
3o3bobo2bo2bobo2bob2ob2obo2b3obob2obobo4b2o$2obobo2bobob2o3b3obobo2b2o
2bobo2bobob2o5bo2bo2bob2obo2bo2b3o2bobo4b4o3b2obob2obob2o2bobo2bobo2b
3o3bobo2bo2bob3o2bo$6b3ob2o3b2obo2bo2bo3bobob2obobo3b4o2bobobo5bobo2bo
3b2o2b2ob2o4b2o3bo4bobo2b2o2bobo2bobo3b2obo2bobobobo3bo$ob4o3bo3b2o5bo
bob3obo2bo3bobob2o3bob2o2bob2ob3obob2obo3b2o2b2o2bobo2b2obob2o2bo2bo2b
2o2bobo2bobo2bo2bobobobo2b2ob2o$2o4bobo2b2o2b6obo4bobobob3obo2bobo2bo
2bobo2b2o3bobo2bob3o2bo4b2ob3o2bobob2obob2obo2b3obobo2b2obob2o2bobobob
obo2bo$3b3o3b2o2bo2bo6bobo2bobobo4b3o2b2obob2o2bo4bobo3bo2bo2bob4obo5b
obobo3bobo2bobo4b2obobo3b2o2b2o2bobo4bo$2obo2b3o2bob2o3bob2obob2obobo
2b3o4b2o2bobo2b2ob4obo2bobobo2bobo4bo2b2ob2ob2ob2obo3bo2b2obo3bobob3o
3bo2b3o2b4ob2o$bo3bo2bobobo2b5obobo3b2o2bobo2b3o4bo2bobo2bo5bob2obo2b
3obob2o2b2obobo5bobob4obo2b5o2bo4b2ob3o3b2o3bobo$o2bobobo2bo3bo7bob2o
3bobo2bo4b2ob2obo2b2o2b4obo2bob3o4bo2b2obo4bob2obo4bo3bobo6b2o2b2o3bo
3b2o3b2obobo$ob2obobobo2bob4ob2obo3b3ob2ob2ob2o2bobo2b2o3b2o4bobobo4b
3o2bo4bob4o2b2ob4o2bobo2b2obobo2b3ob2o3b2o2b3o2bobo$bo3bobo2b2obo4b2ob
ob3o2bo4bo2bob2o4bo2b2o2bob2obobo2b3obo2b3ob2ob2o4bo4bo3b2obob2o2b2obo
bo6b3o2b2o2bobo2bobo$2bobobobobo2bob2o4bobo3bo2b2o2bobo2bob3obo2bobo2b
obo2b3o2bobobo3bobo4b2ob3obo2bo2bobo3bo4bob2ob2obo3bo4bo2bobo2bo$b2obo
bobo2b2obobob3o3b2obob2ob2obob2o2bo3bobo2b2obo2b2o4bo2bobobo4bob2obo4b
2ob2obo3bobob3obo2bobo3b3ob2ob2ob2ob2obo$o3bob2obobo2bo3bo2b2obobobo4b
obo2bobo2b3o2b2o2bobobo2b2obobobob7obo2bob2o4bo2b2ob2obo4bobobobob2o4b
o4bo6bo$2b2obo3bo3bob3o2bo2bo2bobob2obo2bo3b3o3b2o3bo2bo2bobob2obobo
10bo2bobob2obobo6bob2o3bo2bobo2b3o2b4o2b4o$obo2bob2ob3o2bo2b2obo2b2o2b
o2bob4obo4bobo3b2ob2ob2obo4bo3b2obob4ob3o2bo2bobo2bob3o2bo2b3obobobobo
3b2o4b2o3bobo$obob2obo2bo2b2o2bo2bob2o2b3obo7b2ob2ob2ob2obo4bo2bob2o2b
3o2b2obo2bo4b3obo2bob2obo2b2o2bo4b2obobobobo2b3o2bobo2bo$o2bo4bobobo2b
2obobo3bo4bob2ob4o4bo4bo2bob2obob2obob2o3bo6bo2b3o4bob2obo2bobo2b2ob2o
bo3bobob2obo3bobo2b2obo$bobob3obo2bobo2bobobobob3obo2bobo3b3o2b3o2bobo
2bobobo2bobo2bob4obob2obo2b2obo2bo3bobob2o2bobo3b3obo5b3o3b2o4bo$bobo
2bo2bobobob2o2bobobo3bo2bo4bobo3b2o3b2o2bobo2bo2bobo3b2o5b2o2bo2bo2bob
2obob3o2bo2b2o4b2o2bobob2obo3b3o2b2obobo$o3bo3b2obobo2bobo3bob2o2b3obo
b2ob4o2b3o2b3ob2ob3o2b4o2b4o3bo2bob2obobo2b2o3bobobo2b4o2bo3b2obob2obo
3b2o2b2o$ob2ob3o3bo2bo2bob2obobob2o3b2obo5bobo4bo6bo3b2o4bo3bob2ob2obo
3bo3bo4bobobob3o4bo2b3o9bobo2bo3bo$b2o2bo3b2obob2obo3bobo5bo5b4obob2ob
2o2bob3o2b2o2b2obob2o4b2o2bob2o2b3ob5o2bo6bobob2o3b2obob2ob2obob2ob2ob
o$4bo2b2o3bo2bob2obo2bob2ob2ob4o2bobobo4bob2obo2b2o2bo2bobo3b3o4bo2bob
2o3bo5bobob3ob3obo2bobo2b3obobo2bo2bobo2bo$b3ob2obob3obo3bobobo2bo4bo
4bo5bob2o2bo5bo2bo2b2o3b2obo2b3ob3o4b2o3bobobobo2bo6bob2ob2o5bo2bob2ob
o2bobo$o3bo4bo4b3obobob2obob2obob3ob5obob2obob5obob2o2b2obobo2bo2bo4b
3o3b3ob2o2bobo3b3obobo5b4ob3obo3bob2o$2bobob2obob3o3b2obo2bobobo2bobo
3bo4bo4bo2bo4bobo2bo2bobo2b2obo2b3o3bob2o2bo3b2o2b4o2bobo2bob2o3bobo4b
ob3o3b2o$3obobobo2bo3bo4b2o3bobobo3bobo2b2obob2o2b2o2b2o3bobob2o3b2o2b
ob2o3b2obo2bobo2b2o2b2o5bo2b2ob2o2b2o3bobobobo4b2o$4bobobobo2b2ob4o2b
4obo2b2ob2ob2obobobob2o2b2o2b3obobo2b3o2bo2bo2b3o2bobo3b3o2b2o2b4obobo
2bo3bo2b3obob2o2b4o2b2o$b2obobobobob2o2bo2bobo6bobobo3bo2bobo2bo3bo2bo
bo2bo2bobo3bob2obobo3bo3bobo4bo3bobo3bob2obo2b2obobo3bo3b2o4b2o$2ob2o
2bobobo3bo2bo2b8obo2b2obob2o2b2o2b2ob3o2bobobo2bobo2bo3bob4ob3o2b4o2b
4obobobo4b2obo2bobob2ob2obo2b2o3bo$5bobo2bo2b2ob2ob2o10bobobobo2b2o2b
2obo4bobo2bob2obob2o2b2obo4bo2bobo4b2o4bob2o2b4o3bobo2b2obo2bo2bobob3o
$2ob2obobobob2o2bo2bo2bob4ob2obo2bo2bo3bobo2bob2o2bobobo2bobo3b2o3bob
2o3bo2bob3o3b2obo3bobo3b2o2bob2o4bobob2obo4b2o$bobo2bo2bobo3bo2bo2b2ob
o2bobo2bobob2ob2obobob2o2b2obo2bob2o3bobo2b2obobob3ob2obo4b2obob2ob2o
3bo2b2obo3bob2obobo4bob2o$bo2bo2bobo2b2ob2ob2obo4bo2bobo2bobo2bo2bobo
3bo4b2obo3b4ob2o3bo3bo4bo2bob3o3bobo5bob2o4b2ob2obo2bobob2obobo2bo$ob
2ob2obobobobo3bo2bob4obob2obo2bobo2bobob4ob2o2bobob2o4bo2b2o2b3o2bobo
2b2obo2b3o3b4ob2o2b4o4bo2bobobobo2bo2b2o$o2bo2bo3bo4b2o2bo2bo5bo3bob3o
b2obobobo4b2obo2b2o3b2o2bobob2o2bob2ob3o3bobo3b3o4bo3bo5b2o2b2obobo3bo
b2obo$2o2bobobo2b4o2b2ob2o2b4ob2obo4bo2bobo2bob2o4bobo3b2ob4o2bo2bobo
7bobo2bobo3bob2obob2ob5ob2obo2bo2b4o2bo2bo$2b2obob3obo3bo2bo2bob2o4bo
2b2obo2bo3bobobob4obo2bob2o6bobobobo2b4ob2obob2ob3obobo2b2obo9bo2bob2o
4b2o2b2o$o4bo4bo2bob2o2bo2bo3b2o2bo2bob2ob5obobo4b2obob2o3b3obobob2o2b
2o3bobo2bo2bo4bo4bo3bob4ob2obob2o2bob3o2b2o2bo$ob2ob4obob3o2b2ob2o2b2o
b2obobo4bo5bobobobo4b2o3b2o2bobobo3b2o2b2obobob2obo2b2o2b5ob2obo3bob2o
bo2bobo2bo2bo3bo$o2bo4b2obo4bo2bo2b2obo3bo2bob2o2bob2obobobob4o4b2o2bo
bobo2bobo2bo3bo2bo4b2obob2o6bo2bobobo4b2obob3o2bob2ob2o$3o2b2o4bob2ob
2o2bobo3b2obob2ob2ob2obo2b2obobo4b4obobobo2b2ob2ob2ob2obob2ob2o4bo3bob
3o3bob2obob3o2bobo3b3obo2bo$3b2o2b3obobobo2b3o2b2obobobo6bo2bobo3bobob
2o5bo2bobobo2bo3bo2bo2bo2bo2b2ob2ob2obobo2b4o3bobo3bobo2b3o5bobobo$obo
2b2o2bobobo2bo4bobo2bobo2bob3o2bobobob2o2b2obob3obobo2bo2bo2b3o2bo2bob
o2bo5bobo2bo2bobo3b2o3bobo2bobobo2b5obo2bo$3bo2bobo2bo2bobob2obo2bobob
2ob2obob2obobobo2b2o3bo2bobobob2obob2obo2b3ob2obob2ob2obo3bob3o2bobo2b
obo2bob2o2bo2b2o4bobobo$2ob2o3bob2ob2obobo2bob2obo2bo6bo2bobo2bo2bob2o
bo3bo3bo2bobo2bobo4bo2bobo2bob2ob2obo3b2o2b2obob2obo3b2obobo2b2obob2ob
o$2bo2b3obo3bo2bo2bobo2bobobo2b5o2bobobobobo2bo2b4ob3o2bo3bob2ob3o2bob
obobo5bo2bob2o2b2o2bo4bob2o3b2o3b2o2bo4bo$o2bo3bo2bobo2bo2b2obobo2bob
2obo4b2o2bo2bo2b2obobo5bo2b3ob2obo3bo2b2obob2o2b5o2b2obo2bo2bo2b3obobo
b2o3b3o3bo2b2o$b2ob2o2bobob2ob3o2bobob3o2bo3b2o3b2obobobo3bo2bob2obobo
3bobo2b2o2bo2bobo3bobo4b2o4bobobob2o2bobobobob2o4b2ob4ob2o$bo2bob2obob
o2bo3bo3bo4bo2b3o2b2obo2b2obobobobob2obobo2bobo3bobob2ob2o3bobobo2bobo
3b4o2bobo2bobo2bo2bo2b5o2bo$bobo2bo2bobobo2b2ob3ob4ob2o3bobobo2bo3bob
2obobo4bobobob2ob2obo3bo2b4obobob2obob2o4b2o2bob2o2bobobobo5bobo2b2ob
3o$2ob2obob2o2bob2obobo2bo3bobo2b2o2bo2b2obob2o4bobob2obobobo5bob2obo
2bo5bo2bo3bobo2bobo2b3o3bobobobob2ob2o2bob2obobo$2bo2bobo2bobobo2bo2bo
2b2obo2b2obobobobo2b2o3b2obobobobobobob5o2bo3b3ob2obob2o2b2o2bob2ob2o
4bob2ob2obo6b2obo2bobo2bo$o3bo2bob2obobobobob2obobobobo4bobo3bo3b2o2b
2obo2bo2bo2bo4bobo2b2o3bobobo3b2o2b3o3bo2b3ob2o6bob4o4b3o3bob2o$b3ob3o
2bobobobobo2bobo3bo2bobobobobob4o2bo4b2obobobobob2obo2b2obobobo3bob2o
2bo4bobo2bo3bo3b2ob2obobo2b3o4b2obo$bo2bo3bo2bo2bobobobo2bobobob2ob2ob
obobo4bob4o3b2obobo2bobob3o4bobo2bob2o3b2ob2obob3obobo2b2ob2o3bo3bo2bo
b2obob2ob2o$2bo2b2ob2obobo2bobobobobobobo6bo3bob3obo4b2o4bob2obo6b4o2b
ob2o4b2o2bobobo5bob3obo4b2ob3obobo2bobo3bobo$2ob2o2bo2b2obob2obob2obo
2bo2b4obo2bo2bo3bo2b2obob2obo4bo2bob2obo3b3o2bob2obo2bo2bo2b4obo5bob3o
bo4bo2b2obob3o$2bo2bo2bo5bo3bo4bobob2o3bobob3obobo2b2obobobob2ob2obob
2obo2bob2o3bo3bobo2b2obob2o3bo2b4o2bobo4b2o2b2o2bo5b4o$bo2b2ob2ob4o2b
2o2b2obobo2bob2o2b2o4bob3o2bo2bobo4bob2o2bo2bobo2bobob4o3b2o2bo2bo2bo
2bobo3b2o4b3ob3o2bobob3o4bo$b3o2bo2bobo2b2o2b2obobo2bo2bo2b2o3b4o4bo2b
2obob2obo4bo2b2obob2o2b2o3bob2o2bobobo2b3obo2b3o2b4o8bobobo3b2obo$o3bo
3bo4bo2bobo4b2ob2obobo2b2obo3bobob2obo2bo2bobob2o2b2o3bo3b2o3bobo2bob
2obob3o4b3o4bo5b2ob5o2bo2bo2bobo$bobob3ob5ob2o2bobo2bo4bob2obo2bob2ob
2o3bo2bobo4bob3o3b3ob2o3b4obobo2bobo4b2obo4b4obob2obobo4bobob2obo2bo$b
obobo3bo4bo2bobob2o2b4o2bo2bob2o2bo3b2obob2ob5o5b3o3bobob2o5bobobo3b3o
2bobob2obo3bob2o2bo3b2ob2obo3bobobo$ob2o3b2o2bobo2bobo4b2o4b2o2bobo2bo
2b2obobobo2bo5b3obo3b2obo3bo2b2ob2obo2b3o2b2o3bobo2bobobo4bob3o2bo3bob
3o2bo$o3b3obob2obob2o2b4o3b2o3b3o2bob2obobo2bo2bo2bob2o3bob3o2bobobobo
b2o5b3o3bo3b3obo2bo2b2obob2obo3bo3b2obo3b2o$b3o2bo2bo2bobo2bobo3bob2ob
3o3bob2o3bo2b2obob2obobob2obo4b2o2bob2obo3b4o4bob2obo2bo2b2ob2o3bobo2b
ob2ob3obo3bo2bobo$4bo2b2o2bo2bobo2bob2o5bo2b2o2bo3b2obobo2bo2bobo3bobo
b2obo2b2o5bob2obo2b4obo4bo2b2o2bo2b2obobobobobo2bo2bobob2o3bo$b3ob2o2b
3obo2bobobobob3o2bobob2o2b2o3bobobobobo2b3o2bobo3bo3b3obobo5bo3bobob2o
b3o2bo2bo2bobobo2bo3bo3b2ob2o2b4o$2o2bo3bo3b2obo2bobobo2bob3o2bo2b2o3b
2o2bo2bobob2o2bobo3b2obob2o3b2obob5obobo2bo2bo4bob2ob2o2bob2obob2ob3o
6bo$3bo2b2ob2o4bobo2bo2bo6bobobo2b3o2b2obobo2bo2bo2bob2obobobo2b2o4bo
2bo3bobobobobo2b2obo2bo2bobo4bobobo2bo2b2ob2obobo$b2ob2obo2b3obo2bobob
2ob5obobo2b2o4bo3bo2b2o2bob2o2bo2bobobobo2b3ob2o3bo3bobobob2obo2b2o3bo
2bob2obobo2bo3b2ob2o2bob2o$2bo2bo2bo4b2obob2obo2bo3bo2bob2o2b3ob4ob2o
2b3o2bobo2b2obobo2bo3b2o2b3ob3obob2obo2bobo2b4obobo2bobobob4o6bobo$o2b
o2b3ob2o3b2o5bo3bo2bobo3b2o2bo6bo2bo4bo2b3o2bobob2ob2o4bo2bo5bo6b2o2bo
bo4bo2bobobobo6b6obobo$b2ob2o3b2ob2o3bob2ob5ob2obob2o2bo3b4o2bobob2ob
3o4bo2bobo2bob2ob2obo2b3o2b6o3b2o3b2ob2obo2bobob2ob2obo7bo$o2bo2b2o4bo
b2obobobo5bo3bo2bobob3o4b2obo2bobo3bob3obobo2bo3bobo2b2obo2b2o6b2obo2b
ob2o4b2obobo2bobo2bob5obo$obo2bo2b3obobo2bobo3b3o2b2ob2o3bobo2bobo4bob
o4bob2o4bo2b2ob3o2bobo3bobo3b2obobo2bob2o4b2o2bobo2bobobobo2bo3bobo$ob
3ob2o3b2o2bobobobobo2b2o2bo2b3obo2bob2ob2obob2obob2o3b2o2bobo2bo2b2ob
2ob2obob2obob2o3bobo3b4ob2o3bobob2obob2o2bobobo$bo3bo3bo3bobo2bob2o2bo
bo2bo2bo2bobob2o3bobobo3b2o4b2obob2o2bo2bo2bo3bo3bo2bo5b4o2b3o7b2obobo
4bo3b3obobo$bobo3b2ob2obob2obo3b3o2b2ob2obobobo3b2o3bob3o4b2obo2bo3b2o
b3obo2b2o2b2obo2b4obo3b2o2bob2ob3o2bo2b6ob2o4bo2bo$b2ob3obobo2bo3bo2b
2o3b2o3bo2bo2bob2o2bobo2bo3b4obo2bo2bobo2bo4b3o2b2o3b2obo3bo2b2o2bo2bo
b2o3bo2b2o6bo3bobob2o$o3bo3bo2bob3o2b2o2b2o3bobo2bobobo2bobo2b3o2b2o2b
o3bobob2obobo2b2o4bo3b2o3bo2bo2b2o2bob2obo4bo2b2o2b4obo2b2ob2o2bo$ob2o
2b2o2b2o4b2o2b2o2b4ob2obobobobo2bobo3b2o2bo3b2o2bo2bobo2b2o2b4ob3o2b2o
2b2ob2o2bobo3bob3ob3o2bo4bob3obo4bo$bo2b2o2b2o2b3o3bo3b2o8bobo2bob2obo
b2o2bobob3o2b2ob2o2b3o2bo5bo2bobo2b2o3bo2bobo2b2o2bo2bo4bob3o2bo4bob2o
bobo$2bobo2bo2b2o3b3ob3o3bob6ob2obo4bo2b2o3b2o2bobo2bo2b2o4bob4obobo2b
2o3b2obob2o2b2obobo2bo2bob2obo2b2o2b3o2bobo2bo$obo2bob2o3b2o3bobo2bob
2obo8bo2b3obo3b3o3bo2b2o3bo2bob2obo4bo2b2o3b2obobobo2b2o3bobob2ob2obo
2bobo2b2o2bobo2bobo$ob4o3b2obob2obobobo6b2obob2o2b2o4b2obo3b3ob2o2b3ob
obobo2bob2obobo2b2o2bobobobobo2bobo2b2o3bo2bob2o2bobo2bo2bobobo$6bobo
2bo2bobobo2bob2ob2o2b3ob3o3b2o2bobobo3bo2bobo4bobo3b2obo2b2obo2bobo3bo
2b2obobobobo3b2o2bobo2bobo3b2obobo2bobo$4ob2ob2obobo2bo2b2obob2o2bo9b
2obobo2b2ob2o2bobo2b4obob3o3bobo3bobo2b3obobo3bobobobob2obob2obob2ob4o
3bobobobo$o2bobo4bo2b2ob3o3bo4bob4ob5o2bob2o4bob3o2b2o5bobo2b2obo2b2ob
ob3o3b2ob2obob2obobobo2bo3bobo6bob2obobo2bo$bo4b3obobo2bo3b2obob2ob2o
3bobo5bobo2b4o5b2o2b5obo2bo2bobobo2bo4b2o5bobo4bobobobobobo2bob2obo3bo
2bobobo$b4obo2bobobo2bobo2bo2bobo3bo3bobob2obo2bo4b4o2bobo6bob2obo2bo
3bobobo2bob2obo2b5o3bo2bobob3o2bob2obobob2ob2ob2o$o3bo2bobo3b2obob2o2b
2o3b4obo2bob2o2bob2ob2o4b2obob8obo2bobob3obob3obobob2obo5b2obob2obo4b
2o4b2obo2bo4bo$ob2o2b2obobo3bobo2b2o2b3o5b2obo4b2o3bobob2o4bo10bob2obo
3bobo4bobo5b5o2bobobo2bob2o3b3o4bobo2b2obo$2o2b2o4bob2obo2bo3bobo3bob
2o2bob4o2bobo2bob2ob2ob4ob4obobo2bob2o2bob2obo2bob2obo5b2o2bo2bob2ob2o
bo3b4o2b2obobo$3bo3b2obo2b2ob2ob2obo3b3obo2bo2bo2bob2obob2o4b2o4bobo3b
2o2bobo2b2obo3b2ob2o2b2ob2ob2o2b2ob3o8b3o3bobo2bo2bobo$b2ob2obo2b2o4bo
2bobob3o5bob2o2bobo5bo3b2o4b3o2bobo3b3ob2o3bob2o3bo2bo4bob2o2bo2bo3b5o
b2o2bobo2bobobob2obo$2bo2bobobo2b3o2bobo3bo3bob3o3b3ob2ob3o2b3ob3obo2b
2obob2o7b2obo2b2obo2bob3o6b2obo2bobo3b2obobo2b2obobobo2bobo$o2bobobo2b
obo2b2o2bobo2b5o3b2o6bobo2b2o6bo2bo4bobob2ob2obo2bobo5b2obo3b5obo2bob
2o2b2o6bobo2bobobo2bo2bo$b2obo2bob2o2bo2bobo2b2obo5bobob2ob2obo2bo2bob
ob2o2bob3obobo3bob2ob2o3bob3obo2bobo6bo2bobo2bobob7o2bobobobob2obo$4bo
b2o3bobobo2b2obo2bob2ob2obo2bobo2b4obo2b2ob2obo4b2o2b3o6bobo2bo2bobobo
2b3ob2o2b3obobo2bobo6b2obobo2bo4b2o$b4o3bobo2bob2o3bo2bobobobo3bobo2b
2o5b3o5bobobo3b2o2bob4obob2obobo2bobobo3b2ob2o4bobob2obob2obo2bobobob
2ob2o2bo$bo3b4ob2obo3b2obob2o2bo3bob2o2bobo2b2obo3b3obo2bob2obo2bo2bo
4bobo3bob2obobobobo4bo2b2obobobo3bobob2obobobo4bob2o$o2bo5bo2bob3o2b2o
3bobob2o5b2o2b2obob2obo2bobob2obo3bob2obob2obo2b4o3bo2bobob4obob2ob2ob
o2b2obobo2bobo2bob3obo2bo$b2ob4o2bobobo2bo3bobo2bo2bob4o2b2o2bo3bob2ob
obo2bo2bob2obo2bo2bo2bobo3b2o2b2o3bo4bobo6b3o2b2o2bobob2obo3b2obobo$o
2bo3bob2obobobob2obobobobo2bo3bobo2bobob2o5bobobo2b2obo3bob2o2b3obob2o
2b2o2b2obob2obo2b4obo3bo3bobobo4b3o4bo2bo$bo3bo2bo4bo2bo2bo2bob2ob2obo
b2o2bobobobo2b5obobob2o5b2obo2b2o5bo2b2o2b2o2bo2bo2b2obo2bob4ob2obobob
ob3o3b2obob2o$bobob2obob2obobobo2bobo6bobobobobo2bobobo3bo2bo2bo3b4obo
2b2o2bob2obobo2bo3bobobo2bo3bobo7bo2bobob2o3b2o3b2o3bo$ob2o2bobobobo2b
ob3obob2ob2obobobobo2b2obobob2o3bobobob2o6bobo2bob2obobob3ob2obobob2ob
obo2b4ob2o2bobob2o3bobob2o4b2o$o3bo3bobobob2o5bo2b2obo2bo2bob2obo2bobo
bob3obobobo2b2ob3o2bob2o6bo4bo3bobo3bob2obo3bobob2o2bo4b2obo2bob4obo$b
2ob4o2bobo4b2obobo5bobobo2bo2bob2obo7bobo2bo2b2o3b2obo2bob5ob2o2b3o3b
2obo4b3o3bo2bob2ob4o2bobo2bo5bo$bobo3bob2ob2ob2obobo2b2ob2o2bob3o2b2o
5b7o3bob2o4bobo2bobob2o4bob3o3b3o2b2ob2o4b3obobo3bo5bo2bobo2bob2o$o2bo
bobobo3bobo2bob2obo3bobobo3b2o3b3obo6b3obo2b2ob2o3bo2bo4b2obo5bo4bo3bo
2b4o3bobo2b2o2bob2ob2obob4obo$b2obobo3b3o2bob2o2bo2b2obo2bo2bo2bob2o2b
o3b2obo3bo2bobo3bobob3ob2ob2obobob2ob4ob2obo2bo4b2obo2b2obob2obo2bo2bo
7bo$bo2bobob2o3b2obo2bo2bobobobobob3obobo2bo2bobob3obo2b2o2bobo2b2o4bo
7bobobo3bo2bob2obob2obobob2o3bobo2bobo2bob2ob4o$o2bob2o2bobo4bobob2o2b
o3bo2bo3b2o2bobob2obo6b2o2b2ob2obo3b2o2bob6obo2b2obobo4bobobo3bo2bob2o
2bobo2b4o2bobo2bo$ob2o3b2o2b2ob2obobo2b2ob3ob2o2bo3b2obobo2bob6o2bo2bo
4bob2o2b2ob2o5bobobo2bobob3o2bo3bo2bo2bobobo2b2o6bo3bo$o3b2o3b2o4bobo
2bo4bo2bo2b2ob2obo2bo2bobo2bo5b2obo2b2ob2o2bo2bo4b3obo2bo2bo2bobo2b2o
2bob2ob3o2bobobo2b2ob2ob4ob3o$b2obob3o3b2obob2obob2o2bo2bo4bobo2bobobo
b2o3b4o3bob2obo3b2obo2b2obo2bobobob2obo3b2o2b3o2bo4b3obo2bo2bobobo3bo$
2bobo4b3o2b2o3bobob2obob2ob2obobob2obobo3b3obo2bobobo5b2o2bob2obo2bobo
2bobo2bob3o2b2o3b2o2b2o6bob2obobo2b2o2b4o$2o2b2ob2o3bo3b2o3bo3b2o2bob
2obobobo2bo2b2o3bo3b2obo3b4o2bobo5bobob2obo2bo3bo2b2o2bobo2b2o2b7o3b2o
b3o2b2o2bo$bobo4bob2ob3o2b3ob2o4bo5bobo3bob2o2b3o2bobo2b4o4bobo2b5ob2o
4b4obo2bo3bobob2o3bobo6b2o7b2o2bo$o2b4obo2bo4bobo3bob3obob2obobob4o3b
2o3b2obo2bo3bob2obob2obo3bo3b4o5b2obob2obobo2b4o3bob3o2b4obo3bo2b3o!

[/quote]

[pcallahan]

Another question, mostly for Macbi, and maybe this has been discussed before.

Has anyone implemented a SAT approach for a Bellman-like search? I don't know the Bellman algorithm, but I can see how SAT would be a great way to express a still-life region combined with a more variable region representing short perturbation events, like eating a glider and restoring the object.

I don't think I'm exaggerating when I say that SAT solvers are the most exciting thing I've seen in algorithmic tools since I last paid much attention (over 20 years ago). Oddly, I'm not even that interested in knowing how they work, but I am really curious what applications I can extend them to (not just Life, but many other search problems).

[dvgrn]

I don't think I'm exaggerating when I say that SAT solvers are the most exciting thing I've seen in algorithmic tools since I last paid much attention (over 20 years ago). Oddly, I'm not even that interested in knowing how they work, but I am really curious what applications I can extend them to (not just Life, but many other search problems).

Donald Knuth seems to have found them useful for Conway's Life problems. I'm not sure what the status is at the moment, but have you seen the preliminary fascicle he sent out from several years ago, applying SAT solvers to various Life problems?

EDIT: preliminary fascicle download link

Notes from Gosper about the fascicle (2015):

> At a puzzle party today Knuth expressed strong interest in
> (dis)proving his conjectural formula f(i,j)
> (http://www-cs-faculty.stanford.edu/~uno/fasc6a.ps.gz
> (seems to be deliberately crIPpled).
> page122 "116" example 88
> for the soonest cell i,j can turn on
> if initially, all cells with a non-negative coordinate are off.
> Also, although this fascicle is very preliminary, he offers his
> usual monetary bounty on detected bugs.
> Assuming nobody here prevails, please rebroadcast this on
> the appropriate wider forum.
> --Bill Gosper

[Macbi]

Another question, mostly for Macbi, and maybe this has been discussed before.

Has anyone implemented a SAT approach for a Bellman-like search? I don't know the Bellman algorithm, but I can see how SAT would be a great way to express a still-life region combined with a more variable region representing short perturbation events, like eating a glider and restoring the object.

I don't think I'm exaggerating when I say that SAT solvers are the most exciting thing I've seen in algorithmic tools since I last paid much attention (over 20 years ago). Oddly, I'm not even that interested in knowing how they work, but I am really curious what applications I can extend them to (not just Life, but many other search problems).

I tried implementing that in LLS, and it didn't seem to work very well. In particular I implemented a constraint that forced the number of cells that were different between two generations to be bounded above, in the hope of finding catalysts by narrowing down the search space to rule out ones that were exploding. But I couldn't find the snark even leaving it running overnight. On the other hand I never understood Bellman well enough to find the snark with it either, so it could be that LLS is actually competitive and I'm just overestimating how good Bellman is. How long is it supposed to take to find the snark?

[Hunting]

Question: Why does SAT solver behave so badly in normal searches? I mean, it takes 143s to rule out the existence of a 15x8 c/3 spaceship in LeapLife. This takes less than 1 seconds with the normal brute-force method.

[pcallahan]

Question: Why does SAT solver behave so badly in normal searches? I mean, it takes 143s to rule out the existence of a 15x8 c/3 spaceship in LeapLife.

Macbi may have some other thoughts, but it's unrealistic to expect a SAT solver to do a better job all the time. In fact, I'm amazed they work so well. The same search can be translated to very different SAT instances, and some are more tractable than others.

I would guess (but I don't know these well enough) that SAT solvers work best when the inference paths that lead to contradictions are as short as possible. The introduction of new variables may slow things down. I have been playing around with lingeling for simple planar constraint satisfaction problems, and it works much better than I expected, considering how little effort I put into setting up clauses. But I can already see qualitatively which problems are harder. The slowest to solve are those that are relatively easy to solve locally but introduce a global packing problem with periodic boundaries. The SAT solver still solves pretty large cases, and I can't imagine how I would write such an algorithm myself. It would require a lot more thought.

This takes less than 1 seconds with the normal brute-force method.

Can you explain what you mean by brute-force? Very few searches are truly "brute force". lifesrc and similar algorithms are backtracking searches that do some forward inference on constraints to limit the recursive calls. This is pretty effective for finding small oscillators and spaceships, though it can bog down for essentially the same reason: you have to make a lot of cell assignments before finding the inconsistency.

Pure brute force in my view would be enumerating all 15x8 starting patterns and seeing if they are spaceships, which is clearly not feasible.

I wonder if it would be possible to make the SAT solver work more like the lifesrc algorithm by introducing additional clauses derived from the base clauses to capture some of the forward inference. I'm not sure. lingeling must also be able to do this, but maybe you could narrow it down this way.

[wildmyron]

Following up on a bug report posted to Discord a little while ago:

Here is a reduced test case (not necessarily minimal) which exhibits the bug. The search pattern includes negated variables but in the output pattern one of those variables has both the variable itself and it's negation set to "On".

STR:

Create this search file: agar_test.txt

Code: Select all

 a1  -a1   a1  -a1
 a2    0   a2  -a2
 a3  -a3   a3  -a3
-a3   a3  -a3   a3

 a1' -a1'  a1' -a1'
 a2' -a2   a2  -a2'
 a3' -a3   a3  -a3'
-a3'  a3' -a3'  a3'

Run

Code: Select all

./lls --background forced_vacuum -v 1 -- agar_test.txt

(I used cadical but I don't think it matters)

Result:

Code: Select all

x = 6, y = 6, rule = B3/S23
bbbbbb$
bobobb$
bobobb$
boooob$
boooob$
bbbbbb!

Note that both 'a3' and '-a3' are output as 'o'. Expected output:

Code: Select all

x = 6, y = 6, rule = B3/S23
bbbbbb$
bobobb$
bobobb$
bobobb$
bbobob$
bbbbbb!

Here is console output from some troubleshooting steps:

Code: Select all

$ ./lls --background forced_vacuum --dry_run --save_dimacs agar_test.cnf --save_state agar_test.pkl -- agar_test.txt
Getting search pattern...
    Creating background from file "forced_vacuum" ...
        Reading file "backgrounds/forced_vacuum" ...
        Done
        
        Parsing input pattern...
        Done
        
        Pattern parsed as:
        0'
        
        
        
        
    Done
    
    Creating search pattern from file "agar_test.txt" ...
        Reading file "agar_test.txt" ...
        Done
        
        Parsing input pattern...
        Done
        
        Pattern parsed as:
         a1, -a1,  a1, -a1
         a2,   0,  a2, -a2
         a3, -a3,  a3, -a3
        -a3,  a3, -a3,  a3
        
         a1',-a1', a1',-a1'
         a2',-a2,  a2, -a2'
         a3',-a3,  a3, -a3'
        -a3', a3',-a3', a3'
        
        
    Done
    
Done

Preprocessing...
    Standardising variable names...
    Done
    
    Removing redundant transitions...
    Done
    
    Standardising variable names...
    Done
    
    Search grid:
    
        Rule = B3/S23
        0',  0',  0',  0',  0',  0'
        0', c0, -c0,  c0, -c0,   0'
        0', c1,   0,  c1, -c1,   0'
        0', c2, -c2,  c2, -c2,   0'
        0',-c2,  c2, -c2,  c2,   0'
        0',  0',  0',  0',  0',  0'
        
        0',  0',  0',  0',  0',  0'
        0', c0',-c0', c0',-c0',  0'
        0', c1',-c1,  c1, -c1',  0'
        0', c2',-c2,  c2, -c2',  0'
        0',-c2', c2',-c2', c2',  0'
        0',  0',  0',  0',  0',  0'
        
        Background:
        
        0'
        
    Enforcing evolution rule...
        Method: 1
        Number of clauses used: 5
    Done
    
Done

    Saving state...
        Writing file "agar_test.pkl" ...
        Done
        
    Done
    
Number of undetermined cells: 6
Number of variables: 3
Number of clauses: 5

Active width: 4
Active height: 4
Active duration: 2

Solving...
    Preparing SAT solver input...
        Writing file "agar_test.cnf" ...
        Done
        
    Done
    
Done

Dry run

$ cat agar_test.cnf
p cnf 3 5
-1 -3 2 0
-2 1 0
1 2 3 0
-2 1 3 0
-1 2 0

$ solvers/cadical agar_test.cnf | grep '^[sv]' > agar_test.soln

$ cat agar_test.soln
s SATISFIABLE
v 1 2 3 0

$ ./lls --substitute_solution agar_test.pkl agar_test.soln

x = 6, y = 6, rule = B3/S23
bbbbbb$
bobobb$
bobobb$
boooob$
boooob$
bbbbbb!

This points to the bug being somewhere in solution substitution.

Edit: Thanks for the bugfix. LLS gives me the expected output pattern now.

[Macbi]

Thanks for the detailed investigation. The problem was that in search patterns I use 0 and 1 for Dead and Alive, but in the DIMACS format the negation of 1 is -1. So I had a flag in the 'negate' function to tell if was dealing with a DIMACS file and should negate 1 to -1 rather than 0. But I forgot to actually set that flag when substituting the solution. (If I was writing it today I'd just make two separate functions.)

Now fixed on the develop branch.

[LaundryPizza03]

Which solvers are non-deterministic? I am searching for a 5s-worthy template for non-totalistic rules and need to find solutions from multiple rules in the same rulespace.

[toroidalet]

Lingeling is deterministic, but Glucose, plingeling and treengeling are not (however, they use more CPU). I am not sure about Cadical.
Nondeterminism is probably possible in lingeling by slightly altering the conditions, such as exploiting symmetry or forcing a single cell to be on.

[LaundryPizza03]

Lingeling is deterministic, but Glucose, plingeling and treengeling are not (however, they use more CPU). I am not sure about Cadical.
Nondeterminism is probably possible in lingeling by slightly altering the conditions, such as exploiting symmetry or forcing a single cell to be on.

In cadical's Github repository, I see a C++ file dedicated to pseudorandom generation. Look for a parameter that can enable randomness.

[wwei47]

Is there a way to constrain the population of each generation, rather than just the first one?

[Macbi]

Is there a way to constrain the population of each generation, rather than just the first one?

Yes. In the develop branch you do -p followed by the population constraint, followed by a list of generations to sum over. So for example

Code: Select all

-p =40 7

means generation 7 must have a generation of 40.

Code: Select all

-p <100 0 1 2 3

would mean that the average population of the first four generations had to be less than 25. Note that since > and < are also part of the syntax of the command line you might have to wrap them in quotation marks like

Code: Select all

-p "<100" 0 1 2 3

or suchlike.

[wwei47]

Is there a way to constrain the population of each generation, rather than just the first one?

Yes. In the develop branch you do -p followed by the population constraint, followed by a list of generations to sum over.=

Thanks!
EDIT: Is there a way to get a save/load feature into kissat?

[LaundryPizza03]

I got this error after updating the LLS from github and trying to run LLS again:

Code: Select all

Traceback (most recent call last):
  File "./lls", line 9, in <module>
    import src.LLS_main
  File "/Users/gb/logic-life-search/src/LLS_main.py", line 3, in <module>
    import src.LLS_formatting as LLS_formatting
  File "/Users/gb/logic-life-search/src/LLS_formatting.py", line 3, in <module>
    import src.LLS_rules.py as LLS_rules
  File "/Users/gb/logic-life-search/src/LLS_rules.py", line 3, in <module>
    import src.LLS_formatting as LLS_formatting
AttributeError: 'module' object has no attribute 'LLS_formatting'

I'm using macOS Big Sur 11.4 with Python 3.9.

EDIT: This is on the develop branch; the master branch works fine, but has the old flag system. It looks python2 is the branch I need.