(30,57) d=27 cells=1302 SAT in 1s, check: ok, R=350 (I/3=350)
(29,55) d=26 cells=1215 SAT in 1s, check: ok, R=324 (I/3=324)
(28,53) d=25 cells=1131 SAT in 0s, check: ok, R=299 (I/3=299)
(34,59) d=25 cells=1647 SAT in 1s, check: ok, R=297 (I/3=297)
(30,54) d=24 cells=1290 SAT in 1s, check: ok, R=274 (I/3=274)
(36,60) d=24 cells=1824 SAT in 3s, check: ok, R=272 (I/3=272)
(29,52) d=23 cells=1203 SAT in 1s, check: ok, R=251 (I/3=251)
(35,58) d=23 cells=1719 SAT in 3s, check: ok, R=249 (I/3=249)
(28,50) d=22 cells=1119 SAT in 0s, check: ok, R=229 (I/3=229)
(34,56) d=22 cells=1617 SAT in 1s, check: ok, R=227 (I/3=227)
(27,48) d=21 cells=1038 SAT in 1s, check: ok, R=208 (I/3=208)
(33,54) d=21 cells=1518 SAT in 1s, check: ok, R=206 (I/3=206)
(39,60) d=21 cells=2070 SAT in 4s, check: ok, R=204 (I/3=204)
(32,52) d=20 cells=1422 SAT in 1s, check: ok, R=186 (I/3=186)
(38,58) d=20 cells=1956 SAT in 4s, check: ok, R=184 (I/3=184)
(34,53) d=19 cells=1578 SAT in 3s, check: ok, R=166 (I/3=166)
(40,59) d=19 cells=2130 SAT in 3s, check: ok, R=164 (I/3=164)
(33,51) d=18 cells=1479 SAT in 1s, check: ok, R=148 (I/3=148)
(39,57) d=18 cells=2013 SAT in 1s, check: ok, R=146 (I/3=146)
(32,49) d=17 cells=1383 SAT in 1s, check: ok, R=131 (I/3=131)
(38,55) d=17 cells=1899 SAT in 3s, check: ok, R=129 (I/3=129)
(31,47) d=16 cells=1290 SAT in 1s, check: ok, R=115 (I/3=115)
(37,53) d=16 cells=1788 SAT in 4s, check: ok, R=113 (I/3=113)
(43,59) d=16 cells=2358 SAT in 21s, check: ok, R=111 (I/3=111)
(36,51) d=15 cells=1680 SAT in 1s, check: ok, R=98 (I/3=98)
(42,57) d=15 cells=2232 SAT in 22s, check: ok, R=96 (I/3=96)
(35,49) d=14 cells=1575 SAT in 4s, check: ok, R=84 (I/3=84)
(41,55) d=14 cells=2109 SAT in 19s, check: ok, R=82 (I/3=82)
(34,47) d=13 cells=1473 SAT in 1s, check: ok, R=71 (I/3=71)
(40,53) d=13 cells=1989 SAT in 5s, check: ok, R=69 (I/3=69)
(46,59) d=13 cells=2577 SAT in 24s, check: ok, R=67 (I/3=67)
(39,51) d=12 cells=1872 SAT in 21s, check: ok, R=57 (I/3=57)
Exception in thread Thread-33:
(45,57) d=12 cells=2442 SAT in 97s, check: ok, R=55 (I/3=55)
(38,49) d=11 cells=1758 SAT in 3s, check: ok, R=46 (I/3=46)
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.
(44,55) d=11 cells=2310 SAT in 24s, check: ok, R=44 (I/3=44)
(37,47) d=10 cells=1647 SAT in 4s, check: ok, R=36 (I/3=36)
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.
(43,53) d=10 cells=2181 SAT in 130s, check: ok, R=34 (I/3=34)
Exception in thread Thread-38:
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.
(49,59) d=10 cells=2787 SAT in 632s, check: ok, R=32 (I/3=32)
(42,51) d=9 cells=2055 SAT in 26s, check: ok, R=25 (I/3=25)
Exception in thread Thread-40:
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.
(48,57) d=9 cells=2643 SAT in 153s, check: ok, R=23 (I/3=23)
