(31,59) d=28 cells=1392 SAT in 1s, check: ok, R=377 (I/3=377)
(33,60) d=27 cells=1569 SAT in 4s, check: ok, R=349 (I/3=349)
(32,58) d=26 cells=1473 SAT in 3s, check: ok, R=323 (I/3=323)
(31,56) d=25 cells=1380 SAT in 1s, check: ok, R=298 (I/3=298)
(27,51) d=24 cells=1050 SAT in 0s, check: ok, R=275 (I/3=275)
(33,57) d=24 cells=1548 SAT in 1s, check: ok, R=273 (I/3=273)
(26,49) d=23 cells=972 SAT in 1s, check: ok, R=252 (I/3=252)
(32,55) d=23 cells=1452 SAT in 1s, check: ok, R=250 (I/3=250)
(25,47) d=22 cells=897 SAT in 1s, check: ok, R=230 (I/3=230)
(31,53) d=22 cells=1359 SAT in 1s, check: ok, R=228 (I/3=228)
(37,59) d=22 cells=1893 SAT in 5s, check: ok, R=226 (I/3=226)
(30,51) d=21 cells=1269 SAT in 1s, check: ok, R=207 (I/3=207)
(36,57) d=21 cells=1785 SAT in 2s, check: ok, R=205 (I/3=205)
(29,49) d=20 cells=1182 SAT in 1s, check: ok, R=187 (I/3=187)
(35,55) d=20 cells=1680 SAT in 3s, check: ok, R=185 (I/3=185)
(31,50) d=19 cells=1329 SAT in 1s, check: ok, R=167 (I/3=167)
(37,56) d=19 cells=1845 SAT in 3s, check: ok, R=165 (I/3=165)
(30,48) d=18 cells=1239 SAT in 1s, check: ok, R=149 (I/3=149)
(36,54) d=18 cells=1737 SAT in 1s, check: ok, R=147 (I/3=147)
(42,60) d=18 cells=2307 SAT in 21s, check: ok, R=145 (I/3=145)
(35,52) d=17 cells=1632 SAT in 1s, check: ok, R=130 (I/3=130)
(41,58) d=17 cells=2184 SAT in 4s, check: ok, R=128 (I/3=128)
(34,50) d=16 cells=1530 SAT in 1s, check: ok, R=114 (I/3=114)
(40,56) d=16 cells=2064 SAT in 4s, check: ok, R=112 (I/3=112)
(33,48) d=15 cells=1431 SAT in 2s, check: ok, R=99 (I/3=99)
(39,54) d=15 cells=1947 SAT in 5s, check: ok, R=97 (I/3=97)
(45,60) d=15 cells=2535 SAT in 6s, check: ok, R=95 (I/3=95)
(38,52) d=14 cells=1833 SAT in 4s, check: ok, R=83 (I/3=83)
(44,58) d=14 cells=2403 SAT in 21s, check: ok, R=81 (I/3=81)
(37,50) d=13 cells=1722 SAT in 16s, check: ok, R=70 (I/3=70)
(43,56) d=13 cells=2274 SAT in 19s, check: ok, R=68 (I/3=68)
(36,48) d=12 cells=1614 SAT in 3s, check: ok, R=58 (I/3=58)
(42,54) d=12 cells=2148 SAT in 18s, check: ok, R=56 (I/3=56)
Exception in thread Thread-34:
(48,60) d=12 cells=2754 SAT in 126s, check: ok, R=54 (I/3=54)
Exception in thread Thread-35:
(41,52) d=11 cells=2025 SAT in 32s, check: ok, R=45 (I/3=45)
Traceback (most recent call last):
Traceback (most recent call last):
  File "/Library/Frameworks/Python.framework/Versions/3.13/lib/python3.13/threading.py", line 1043, in _bootstrap_inner
    self.run()
    ~~~~~~~~^^
  File "/Library/Frameworks/Python.framework/Versions/3.13/lib/python3.13/threading.py", line 1043, in _bootstrap_inner
    self.run()
    ~~~~~~~~^^
  File "/Library/Frameworks/Python.framework/Versions/3.13/lib/python3.13/threading.py", line 1344, in run
    self.function(*self.args, **self.kwargs)
    ~~~~~~~~~~~~~^^^^^^^^^^^^^^^^^^^^^^^^^^^
  File "/Library/Frameworks/Python.framework/Versions/3.13/lib/python3.13/threading.py", line 1344, in run
    self.function(*self.args, **self.kwargs)
    ~~~~~~~~~~~~~^^^^^^^^^^^^^^^^^^^^^^^^^^^
  File "/Library/Frameworks/Python.framework/Versions/3.13/lib/python3.13/site-packages/pysat/solvers.py", line 1074, in interrupt
    self.solver.interrupt()
    ~~~~~~~~~~~~~~~~~~~~~^^
  File "/Library/Frameworks/Python.framework/Versions/3.13/lib/python3.13/site-packages/pysat/solvers.py", line 1074, in interrupt
    self.solver.interrupt()
    ~~~~~~~~~~~~~~~~~~~~~^^
  File "/Library/Frameworks/Python.framework/Versions/3.13/lib/python3.13/site-packages/pysat/solvers.py", line 2169, in interrupt
    raise NotImplementedError('Limited solve is currently unsupported by CaDiCaL.')
  File "/Library/Frameworks/Python.framework/Versions/3.13/lib/python3.13/site-packages/pysat/solvers.py", line 2169, in interrupt
    raise NotImplementedError('Limited solve is currently unsupported by CaDiCaL.')
Exception in thread Thread-36:
NotImplementedError: Limited solve is currently unsupported by CaDiCaL.
NotImplementedError: Limited solve is currently unsupported by CaDiCaL.
Traceback (most recent call last):
(47,58) d=11 cells=2613 SAT in 701s, check: ok, R=43 (I/3=43)
  File "/Library/Frameworks/Python.framework/Versions/3.13/lib/python3.13/threading.py", line 1043, in _bootstrap_inner
    self.run()
    ~~~~~~~~^^
  File "/Library/Frameworks/Python.framework/Versions/3.13/lib/python3.13/threading.py", line 1344, in run
    self.function(*self.args, **self.kwargs)
    ~~~~~~~~~~~~~^^^^^^^^^^^^^^^^^^^^^^^^^^^
  File "/Library/Frameworks/Python.framework/Versions/3.13/lib/python3.13/site-packages/pysat/solvers.py", line 1074, in interrupt
    self.solver.interrupt()
    ~~~~~~~~~~~~~~~~~~~~~^^
  File "/Library/Frameworks/Python.framework/Versions/3.13/lib/python3.13/site-packages/pysat/solvers.py", line 2169, in interrupt
    raise NotImplementedError('Limited solve is currently unsupported by CaDiCaL.')
NotImplementedError: Limited solve is currently unsupported by CaDiCaL.
Exception in thread Thread-37:
Traceback (most recent call last):
  File "/Library/Frameworks/Python.framework/Versions/3.13/lib/python3.13/threading.py", line 1043, in _bootstrap_inner
    self.run()
    ~~~~~~~~^^
  File "/Library/Frameworks/Python.framework/Versions/3.13/lib/python3.13/threading.py", line 1344, in run
    self.function(*self.args, **self.kwargs)
    ~~~~~~~~~~~~~^^^^^^^^^^^^^^^^^^^^^^^^^^^
  File "/Library/Frameworks/Python.framework/Versions/3.13/lib/python3.13/site-packages/pysat/solvers.py", line 1074, in interrupt
    self.solver.interrupt()
    ~~~~~~~~~~~~~~~~~~~~~^^
  File "/Library/Frameworks/Python.framework/Versions/3.13/lib/python3.13/site-packages/pysat/solvers.py", line 2169, in interrupt
    raise NotImplementedError('Limited solve is currently unsupported by CaDiCaL.')
NotImplementedError: Limited solve is currently unsupported by CaDiCaL.
(40,50) d=10 cells=1905 SAT in 101s, check: ok, R=35 (I/3=35)
