PB'05 competition: run trace

Some explanations

A solver is run under the control of another program named runsolver. runsolver is in charge of imposing the CPU time limit and the memory limit to the solver. It also monitors some information about the process. The trace of the execution of a solver is divided in four parts:
LAUNCHER DATA
These informations are related to the script which will launch the solver. The most important informations are the command line given to the solver, the md5sum of the different files and the dump of the /proc/cpuinfo and /proc/meminfo which provide some useful information on the computer.
SOLVER DATA
This is the output of the solver (stdout and stderr).
WATCHER DATA
This is the informations gathered by the runsolver program. It first prints the different limits. There's a first limit on CPU time set to 1200 seconds. After this time has ellapsed, runsolver sends a SIGTERM and 2 seconds later a SIGKILL to the solver. For safety, there's also another limit set to 1230 seconds which will send a SIGXPU to the solver. The last limit is on the virtual memory used by the process (900Mb).
Every ten seconds, the runsolver process fetches the content of /proc/loadavg, /proc/pid/stat and /proc/pid/statm (see man proc) and prints it as raw data. This is only recorded in case we need to investigate the behaviour of a solver. The memory used by the solver (vsize) is also given every ten seconds.
When the solver exits, runsolver prints some informations such as status and time. CPU usage is the ratio CPU Time/Real Time.
VERIFIER DATA
The output of the solver is piped to a verifier program which will search a value line "v " and, if found, will check that the given interpretation satisfies all constraints.
General information on the benchmark

Name	normalized-opb/mps-v2-20-10/MIPLIB/miplib2003/normalized-mps-v2-20-10-protfold.opb
MD5SUM	c5ca7819a7dcae16ff6045242cdd1f87
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	-23
Optimality of the best value was proved	NO
Number of terms in the objective function	120
Biggest coefficient in the objective function	1
Number of bits for the biggest coefficient in the objective function	1
Sum of the numbers in the objective function	120
Number of bits of the sum of numbers in the objective function	7
Biggest number in a constraint	18
Number of bits of the biggest number in a constraint	5
Biggest sum of numbers in a constraint	900
Number of bits of the biggest sum of numbers	10
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1175.06
Number of variables	1835
Total number of constraints	3947
Number of constraints which are clauses	1906
Number of constraints which are cardinality constraints (but not clauses)	1921
Number of constraints which are nor clauses,nor cardinality constraints	120
Minimum length of a constraint	1
Maximum length of a constraint	882
Trace number 21612

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc10 THE 2005-04-22 00:30:33 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=12947 boxname=wulflinc10 idbench=996 idsolver=12 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  c5ca7819a7dcae16ff6045242cdd1f87  /oldhome/oroussel/tmp/wulflinc10/normalized-mps-v2-20-10-protfold.opb
REAL COMMAND:  minisat+ -cb -gs /oldhome/oroussel/tmp/wulflinc10/normalized-mps-v2-20-10-protfold.opb /oldhome/oroussel/tmp/wulflinc10/normalized-mps-v2-20-10-protfold.opb
IDLAUNCH: 12947
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 450.999
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 890.88

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 450.999
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 899.07

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        687352 kB
Buffers:         24416 kB
Cached:         301168 kB
SwapCached:          0 kB
Active:          49236 kB
Inactive:       278868 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        687100 kB
SwapTotal:     2097136 kB
SwapFree:      2096784 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6412 kB
Slab:            13356 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-22 00:50:36 (client local time) WITH STATUS 10 IN 1200.46 SECONDS
stats: 12947 7 1200.46 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 2149 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: #####################################
c   -- Clauses(.)/Splits(s): ..................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ---[1908]---> BDD-cost:   98
c ---[1907]---> BDD-cost:   98
c ---[1906]---> BDD-cost:   98
c ---[1905]---> BDD-cost:   98
c ---[1904]---> BDD-cost:   98
c ---[1903]---> BDD-cost:   98
c ---[1902]---> BDD-cost:   98
c ---[1901]---> BDD-cost:   98
c ---[1900]---> BDD-cost:   98
c ---[1899]---> BDD-cost:   98
c ---[1898]---> BDD-cost:   98
c ---[1897]---> BDD-cost:   98
c ---[1896]---> BDD-cost:   98
c ---[1895]---> BDD-cost:   98
c ---[1894]---> BDD-cost:   98
c ---[1893]---> BDD-cost:   98
c ---[1892]---> BDD-cost:   98
c ---[1891]---> BDD-cost:   98
c ---[1890]---> BDD-cost:   98
c ---[1889]---> BDD-cost:   98
c ---[1888]---> BDD-cost:   98
c ---[1887]---> BDD-cost:   98
c ---[1886]---> BDD-cost:   98
c ---[1885]---> BDD-cost:   98
c ---[1884]---> BDD-cost:   98
c ---[1883]---> BDD-cost:   98
c ---[1882]---> BDD-cost:   98
c ---[1881]---> BDD-cost:   98
c ---[1880]---> BDD-cost:   98
c ---[1879]---> BDD-cost:   98
c ---[1878]---> BDD-cost:   98
c ---[1877]---> BDD-cost:   98
c ---[1876]---> BDD-cost:   98
c ---[1875]---> BDD-cost:   98
c ---[1874]---> BDD-cost:   98
c ---[1873]---> BDD-cost:   98
c ---[1872]---> BDD-cost:   98
c ---[1871]---> BDD-cost:   98
c ---[1870]---> BDD-cost:   98
c ---[1869]---> BDD-cost:   98
c ---[1868]---> BDD-cost:   98
c ---[1867]---> BDD-cost:   98
c ---[1866]---> BDD-cost:   98
c ---[1865]---> BDD-cost:   98
c ---[1864]---> BDD-cost:   98
c ---[1863]---> BDD-cost:   98
c ---[1862]---> BDD-cost:   98
c ---[1861]---> BDD-cost:   98
c ---[1860]---> BDD-cost:   98
c ---[1859]---> BDD-cost:   98
c ---[1858]---> BDD-cost:   98
c ---[1857]---> BDD-cost:   98
c ---[1856]---> BDD-cost:   98
c ---[1855]---> BDD-cost:   98
c ---[1854]---> BDD-cost:   98
c ---[1853]---> BDD-cost:   98
c ---[1852]---> BDD-cost:   98
c ---[1851]---> BDD-cost:   98
c ---[1850]---> BDD-cost:   98
c ---[1849]---> BDD-cost:   98
c ---[1848]---> BDD-cost:   98
c ---[1847]---> BDD-cost:   98
c ---[1846]---> BDD-cost:   98
c ---[1845]---> BDD-cost:   98
c ---[1844]---> BDD-cost:   98
c ---[1843]---> BDD-cost:   98
c ---[1842]---> BDD-cost:   98
c ---[1841]---> BDD-cost:   98
c ---[1840]---> BDD-cost:   98
c ---[1839]---> BDD-cost:   98
c ---[1838]---> BDD-cost:   98
c ---[1837]---> BDD-cost:   98
c ---[1836]---> BDD-cost:   98
c ---[1835]---> BDD-cost:   98
c ---[1834]---> BDD-cost:   98
c ---[1833]---> BDD-cost:   98
c ---[1832]---> BDD-cost:   98
c ---[1831]---> BDD-cost:   98
c ---[1830]---> BDD-cost:   98
c ---[1829]---> BDD-cost:   98
c ---[1828]---> BDD-cost:   98
c ---[1827]---> BDD-cost:   98
c ---[1826]---> BDD-cost:   98
c ---[1825]---> BDD-cost:   98
c ---[1824]---> BDD-cost:   98
c ---[1823]---> BDD-cost:   98
c ---[1822]---> BDD-cost:   98
c ---[1821]---> BDD-cost:   98
c ---[1820]---> BDD-cost:   98
c ---[1819]---> BDD-cost:   98
c ---[1818]---> BDD-cost:   98
c ---[1817]---> BDD-cost:   98
c ---[1816]---> BDD-cost:   98
c ---[1815]---> BDD-cost:   98
c ---[1814]---> BDD-cost:   98
c ---[1813]---> BDD-cost:   98
c ---[1812]---> BDD-cost:   98
c ---[1811]---> BDD-cost:   98
c ---[1810]---> BDD-cost:   98
c ---[1809]---> BDD-cost:   98
c ---[1808]---> BDD-cost:   98
c ---[1807]---> BDD-cost:   98
c ---[1806]---> BDD-cost:   98
c ---[1805]---> BDD-cost:   98
c ---[1804]---> BDD-cost:   98
c ---[1803]---> BDD-cost:   98
c ---[1802]---> BDD-cost:   98
c ---[1801]---> BDD-cost:   98
c ---[1800]---> BDD-cost:   98
c ---[1799]---> BDD-cost:   98
c ---[1798]---> BDD-cost:   98
c ---[1797]---> BDD-cost:   98
c ---[1796]---> BDD-cost:   98
c ---[1795]---> BDD-cost:   98
c ---[1794]---> BDD-cost:   98
c ---[1793]---> BDD-cost:   98
c ---[1792]---> BDD-cost:   98
c ---[1791]---> BDD-cost:   98
c ---[1790]---> BDD-cost:   98
c ---[1789]---> BDD-cost:   98
c ---[1787]---> BDD-cost:14703
c ---[1785]---> BDD-cost:16432
c ---[1783]---> BDD-cost:   95
c ---[1781]---> BDD-cost:   95
c ---[1779]---> BDD-cost:   95
c ---[1777]---> BDD-cost:   95
c ---[1775]---> BDD-cost:   95
c ---[1773]---> BDD-cost:   95
c ---[1771]---> BDD-cost:   95
c ---[1769]---> BDD-cost:   95
c ---[1767]---> BDD-cost:   95
c ---[1765]---> BDD-cost:   95
c ---[1763]---> BDD-cost:   95
c ---[1761]---> BDD-cost:   95
c ---[1759]---> BDD-cost:   95
c ---[1757]---> BDD-cost:   95
c ---[1755]---> BDD-cost:   95
c ---[1753]---> BDD-cost:   95
c ---[1751]---> BDD-cost:   95
c ---[1749]---> BDD-cost:   95
c ---[1747]---> BDD-cost:   95
c ---[1745]---> BDD-cost:   95
c ---[1743]---> BDD-cost:   95
c ---[1741]---> BDD-cost:   95
c ---[1739]---> BDD-cost:   95
c ---[1737]---> BDD-cost:   95
c ---[1735]---> BDD-cost:   95
c ---[1733]---> BDD-cost:   95
c ---[1731]---> BDD-cost:   95
c ---[1729]---> BDD-cost:   95
c ---[1727]---> BDD-cost:   95
c ---[1725]---> BDD-cost:   95
c ---[1723]---> BDD-cost:   95
c ---[1721]---> BDD-cost:   95
c ---[1719]---> BDD-cost:   95
c ---[1717]---> BDD-cost:   95
c ---[1715]---> BDD-cost:   95
c ---[1714]---> BDD-cost:   67
c ---[1713]---> BDD-cost:   67
c ---[1712]---> BDD-cost:   67
c ---[1711]---> BDD-cost:   67
c ---[1710]---> BDD-cost:   67
c ---[1709]---> BDD-cost:   67
c ---[1708]---> BDD-cost:   67
c ---[1707]---> BDD-cost:   67
c ---[1706]---> BDD-cost:   67
c ---[1705]---> BDD-cost:   67
c ---[1704]---> BDD-cost:   67
c ---[1703]---> BDD-cost:   67
c ---[1702]---> BDD-cost:   67
c ---[1701]---> BDD-cost:   67
c ---[1700]---> BDD-cost:   67
c ---[1699]---> BDD-cost:   67
c ---[1698]---> BDD-cost:   67
c ---[1697]---> BDD-cost:   67
c ---[1696]---> BDD-cost:   67
c ---[1695]---> BDD-cost:   67
c ---[1694]---> BDD-cost:   67
c ---[1693]---> BDD-cost:   67
c ---[1692]---> BDD-cost:   67
c ---[1691]---> BDD-cost:   67
c ---[1690]---> BDD-cost:   67
c ---[1689]---> BDD-cost:   67
c ---[1688]---> BDD-cost:   67
c ---[1687]---> BDD-cost:   67
c ---[1686]---> BDD-cost:   67
c ---[1685]---> BDD-cost:   67
c ---[1684]---> BDD-cost:   67
c ---[1683]---> BDD-cost:   67
c ---[1682]---> BDD-cost:   67
c ---[1681]---> BDD-cost:   67
c ---[1680]---> BDD-cost:   67
c ---[1679]---> BDD-cost:   67
c ---[1678]---> BDD-cost:   67
c ---[1677]---> BDD-cost:   67
c ---[1676]---> BDD-cost:   67
c ---[1675]---> BDD-cost:   67
c ---[1674]---> BDD-cost:   67
c ---[1673]---> BDD-cost:   67
c ---[1672]---> BDD-cost:   67
c ---[1671]---> BDD-cost:   50
c ---[1670]---> BDD-cost:   67
c ---[1669]---> BDD-cost:   67
c ---[1668]---> BDD-cost:   67
c ---[1667]---> BDD-cost:   67
c ---[1666]---> BDD-cost:   67
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  140955   413699 |   46985       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: -12[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost: 2744     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |        84 |  143562   419869 |   47854      84    10363   123.4 |  0.000 % |
c |       184 |  143562   419869 |   52639     184    17655    96.0 |  0.398 % |
c |       334 |  143562   419869 |   57903     334    41025   122.8 |  0.398 % |
c |       559 |  143562   419869 |   63693     559    65518   117.2 |  0.398 % |
c ==============================================================================
c [1mFound solution: -15[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       799 |  143663   420174 |   47887     799    84829   106.2 |  0.398 % |
c |       901 |  143663   420174 |   52675     901    89360    99.2 |  0.399 % |
c |      1051 |  143663   420174 |   57943    1051   127806   121.6 |  0.399 % |
c |      1277 |  143663   420174 |   63737    1277   218616   171.2 |  0.399 % |
c |      1615 |  143663   420174 |   70111    1615   286713   177.5 |  0.399 % |
c |      2122 |  143663   420174 |   77122    2122   365160   172.1 |  0.399 % |
c |      2881 |  143663   420174 |   84834    2881   429311   149.0 |  0.399 % |
c ==============================================================================
c [1mFound solution: -16[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      3460 |  143657   420154 |   47885    3460   504408   145.8 |  0.399 % |
c |      3563 |  143657   420154 |   52673    3563   513069   144.0 |  0.414 % |
c |      3715 |  143657   420154 |   57940    3715   530099   142.7 |  0.414 % |
c |      3942 |  143657   420154 |   63734    3942   548206   139.1 |  0.414 % |
c |      4279 |  143657   420154 |   70108    4279   571220   133.5 |  0.414 % |
c ==============================================================================
c [1mFound solution: -17[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      4397 |  143686   420259 |   47895    4397   576276   131.1 |  0.414 % |
c |      4498 |  143686   420259 |   52684    4498   584056   129.8 |  0.416 % |
c ==============================================================================
c [1mFound solution: -18[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      4588 |  143678   420188 |   47892    4574   589681   128.9 |  0.416 % |
c |      4689 |  143678   420188 |   52681    4675   601982   128.8 |  0.433 % |
c |      4842 |  143678   420188 |   57949    4828   610824   126.5 |  0.433 % |
c |      5069 |  143678   420188 |   63744    5055   646048   127.8 |  0.433 % |
c |      5406 |  143678   420188 |   70118    5392   682148   126.5 |  0.433 % |
c |      5912 |  143678   420188 |   77130    5898   760566   129.0 |  0.433 % |
c |      6674 |  143678   420188 |   84843    6660   867994   130.3 |  0.433 % |
c |      7813 |  143678   420188 |   93327    7799  1017276   130.4 |  0.433 % |
c |      9521 |  143678   420188 |  102660    9507  1229022   129.3 |  0.433 % |
c ==============================================================================
c [1mFound solution: -19[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     10351 |  143738   420381 |   47912   10337  1352708   130.9 |  0.433 % |
c |     10453 |  143738   420381 |   52703   10439  1359968   130.3 |  0.434 % |
c |     10603 |  143738   420381 |   57973   10589  1375588   129.9 |  0.434 % |
c |     10829 |  143738   420381 |   63770   10815  1398764   129.3 |  0.434 % |
c |     11170 |  143738   420381 |   70147   11156  1442735   129.3 |  0.434 % |
c |     11679 |  143738   420381 |   77162   11665  1502211   128.8 |  0.434 % |
c |     12440 |  143738   420381 |   84879   12426  1685077   135.6 |  0.434 % |
c |     13579 |  143738   420381 |   93366   13565  1826215   134.6 |  0.434 % |
c |     15288 |  143738   420381 |  102703   15274  2264955   148.3 |  0.434 % |
c |     17852 |  143738   420381 |  112973   17838  2664976   149.4 |  0.434 % |
c |     21696 |  143738   420381 |  124271   21682  3903728   180.0 |  0.434 % |
c |     27465 |  143738   420381 |  136698   27451  4595734   167.4 |  0.434 % |
c |     36115 |  143738   420381 |  150368   36101  5625339   155.8 |  0.434 % |
c |     49089 |  143738   420381 |  165405   49075  6833769   139.3 |  0.434 % |
c ==============================================================================
c [1mFound solution: -20[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     62911 |  143730   420350 |   47910   62897  8380786   133.2 |  0.434 % |
c |     63011 |  143730   420350 |   52701   16744  1524785    91.1 |  0.451 % |
c |     63161 |  143730   420350 |   57971   16894  1533305    90.8 |  0.451 % |
c |     63386 |  143730   420350 |   63768   17119  1547767    90.4 |  0.451 % |
c |     63723 |  143730   420350 |   70145   17456  1567306    89.8 |  0.451 % |
c |     64229 |  143730   420350 |   77159   17962  1599942    89.1 |  0.451 % |
c |     64991 |  143730   420350 |   84875   18724  1672445    89.3 |  0.451 % |
c |     66131 |  143730   420350 |   93363   19864  1768790    89.0 |  0.451 % |
c |     67839 |  143730   420350 |  102699   21572  1974411    91.5 |  0.451 % |
c |     70406 |  143730   420350 |  112969   24139  2528499   104.7 |  0.451 % |
c |     74250 |  143730   420350 |  124266   27983  3385458   121.0 |  0.451 % |
c |     80017 |  143730   420350 |  136692   33750  5582665   165.4 |  0.451 % |
c ==============================================================================
c [1mFound solution: -21[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     82569 |  143759   420449 |   47919   36302  6257614   172.4 |  0.451 % |
c |     82669 |  143759   420449 |   52710   36402  6265727   172.1 |  0.453 % |
c |     82819 |  143759   420449 |   57981   36552  6270973   171.6 |  0.453 % |
c |     83046 |  143759   420449 |   63780   36779  6293940   171.1 |  0.453 % |
c |     83384 |  143759   420449 |   70158   37117  6341868   170.9 |  0.453 % |
c |     83890 |  143759   420449 |   77174   37623  6424624   170.8 |  0.453 % |
c |     84649 |  143759   420449 |   84891   38382  6519979   169.9 |  0.453 % |
c |     85788 |  143759   420449 |   93380   39521  6678049   169.0 |  0.453 % |
c |     87496 |  143759   420449 |  102718   41229  7084022   171.8 |  0.453 % |
c |     90058 |  143759   420449 |  112990   43791  7489074   171.0 |  0.453 % |
c |     93902 |  143759   420449 |  124289   47635  8160519   171.3 |  0.453 % |
c |     99669 |  143759   420449 |  136718   53402  8719717   163.3 |  0.453 % |
c |    108323 |  143759   420449 |  150390   62056  9544494   153.8 |  0.453 % |
c |    121299 |  143759   420449 |  165429   75032 12205512   162.7 |  0.453 % |
c |    140761 |  143759   420449 |  181972   94494 18875239   199.8 |  0.453 % |
c |    169953 |  143759   420449 |  200169  123686 30254985   244.6 |  0.453 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v -N_0x23_1_0x23_2_bit0 N_0x23_2_0x23_3_bit0 -N_0x23_3_0x23_4_bit0 -N_0x23_4_0x23_5_bit0 -N_0x23_5_0x23_6_bit0 -N_0x23_6_0x23_7_bit0 -N_0x23_8_0x23_9_bit0 -N_0x23_9_0x23_10_bit0 -N_0x23_10_0x23_11_bit0 -N_0x23_11_0x23_12_bit0 -N_0x23_12_0x23_13_bit0 -N_0x23_13_0x23_14_bit0 -N_0x23_15_0x23_16_bit0 -N_0x23_16_0x23_17_bit0 -N_0x23_17_0x23_18_bit0 -N_0x23_18_0x23_19_bit0 N_0x23_19_0x23_20_bit0 -N_0x23_20_0x23_21_bit0 -N_0x23_22_0x23_23_bit0 -N_0x23_23_0x23_24_bit0 N_0x23_24_0x23_25_bit0 -N_0x23_25_0x23_26_bit0 -N_0x23_26_0x23_27_bit0 N_0x23_27_0x23_28_bit0 N_0x23_29_0x23_30_bit0 -N_0x23_30_0x23_31_bit0 -N_0x23_31_0x23_32_bit0 N_0x23_32_0x23_33_bit0 N_0x23_33_0x23_34_bit0 -N_0x23_34_0x23_35_bit0 -N_0x23_36_0x23_37_bit0 N_0x23_37_0x23_38_bit0 -N_0x23_38_0x23_39_bit0 -N_0x23_39_0x23_40_bit0 -N_0x23_40_0x23_41_bit0 -N_0x23_41_0x23_42_bit0 -N_0x23_43_0x23_44_bit0 -N_0x23_44_0x23_45_bit0 -N_0x23_45_0x23_46_bit0 -N_0x23_46_0x23_47_bit0 -N_0x23_47_0x23_48_bit0 -N_0x23_48_0x23_49_bit0 -N_0x23_1_0x23_8_bit0 -N_0x23_2_0x23_9_bit0 -N_0x23_3_0x23_10_bit0 -N_0x23_4_0x23_11_bit0 -N_0x23_5_0x23_12_bit0 -N_0x23_6_0x23_13_bit0 -N_0x23_7_0x23_14_bit0 -N_0x23_8_0x23_15_bit0 -N_0x23_9_0x23_16_bit0 -N_0x23_10_0x23_17_bit0 -N_0x23_11_0x23_18_bit0 -N_0x23_12_0x23_19_bit0 -N_0x23_13_0x23_20_bit0 -N_0x23_14_0x23_21_bit0 -N_0x23_15_0x23_22_bit0 -N_0x23_16_0x23_23_bit0 -N_0x23_17_0x23_24_bit0 -N_0x23_18_0x23_25_bit0 -N_0x23_19_0x23_26_bit0 N_0x23_20_0x23_27_bit0 -N_0x23_21_0x23_28_bit0 -N_0x23_22_0x23_29_bit0 -N_0x23_23_0x23_30_bit0 -N_0x23_24_0x23_31_bit0 N_0x23_25_0x23_32_bit0 -N_0x23_26_0x23_33_bit0 N_0x23_27_0x23_34_bit0 -N_0x23_28_0x23_35_bit0 -N_0x23_29_0x23_36_bit0 N_0x23_30_0x23_37_bit0 -N_0x23_31_0x23_38_bit0 -N_0x23_32_0x23_39_bit0 N_0x23_33_0x23_40_bit0 -N_0x23_34_0x23_41_bit0 -N_0x23_35_0x23_42_bit0 -N_0x23_36_0x23_43_bit0 -N_0x23_37_0x23_44_bit0 -N_0x23_38_0x23_45_bit0 -N_0x23_39_0x23_46_bit0 -N_0x23_40_0x23_47_bit0 -N_0x23_41_0x23_48_bit0 -N_0x23_42_0x23_49_bit0 -N_0x23_1_0x23_9_bit0 -N_0x23_2_0x23_10_bit0 -N_0x23_3_0x23_11_bit0 -N_0x23_4_0x23_12_bit0 -N_0x23_5_0x23_13_bit0 -N_0x23_6_0x23_14_bit0 -N_0x23_8_0x23_16_bit0 -N_0x23_9_0x23_17_bit0 -N_0x23_10_0x23_18_bit0 -N_0x23_11_0x23_19_bit0 -N_0x23_12_0x23_20_bit0 -N_0x23_13_0x23_21_bit0 -N_0x23_15_0x23_23_bit0 N_0x23_16_0x23_24_bit0 -N_0x23_17_0x23_25_bit0 -N_0x23_18_0x23_26_bit0 N_0x23_19_0x23_27_bit0 N_0x23_20_0x23_28_bit0 -N_0x23_22_0x23_30_bit0 -N_0x23_23_0x23_31_bit0 N_0x23_24_0x23_32_bit0 N_0x23_25_0x23_33_bit0 -N_0x23_26_0x23_34_bit0 -N_0x23_27_0x23_35_bit0 N_0x23_29_0x23_37_bit0 N_0x23_30_0x23_38_bit0 -N_0x23_31_0x23_39_bit0 N_0x23_32_0x23_40_bit0 -N_0x23_33_0x23_41_bit0 -N_0x23_34_0x23_42_bit0 -N_0x23_36_0x23_44_bit0 -N_0x23_37_0x23_45_bit0 -N_0x23_38_0x23_46_bit0 -N_0x23_39_0x23_47_bit0 -N_0x23_40_0x23_48_bit0 -N_0x23_41_0x23_49_bit0 -x_0x23_49_0x23_34_bit0 -x_0x23_49_0x23_32_bit0 -x_0x23_49_0x23_30_bit0 -x_0x23_49_0x23_29_bit0 -x_0x23_49_0x23_27_bit0 -x_0x23_49_0x23_26_bit0 -x_0x23_49_0x23_23_bit0 -x_0x23_49_0x23_20_bit0 -x_0x23_49_0x23_18_bit0 -x_0x23_49_0x23_16_bit0 -x_0x23_49_0x23_13_bit0 -x_0x23_49_0x23_11_bit0 -x_0x23_49_0x23_9_bit0 -x_0x23_49_0x23_8_bit0 -x_0x23_49_0x23_6_bit0 -x_0x23_49_0x23_3_bit0 -x_0x23_49_0x23_1_bit0 -x_0x23_48_0x23_34_bit0 -x_0x23_48_0x23_32_bit0 -x_0x23_48_0x23_30_bit0 -x_0x23_48_0x23_29_bit0 -x_0x23_48_0x23_27_bit0 -x_0x23_48_0x23_26_bit0 -x_0x23_48_0x23_23_bit0 -x_0x23_48_0x23_20_bit0 -x_0x23_48_0x23_18_bit0 -x_0x23_48_0x23_16_bit0 -x_0x23_48_0x23_13_bit0 -x_0x23_48_0x23_11_bit0 -x_0x23_48_0x23_9_bit0 -x_0x23_48_0x23_8_bit0 -x_0x23_48_0x23_6_bit0 -x_0x23_48_0x23_3_bit0 -x_0x23_48_0x23_1_bit0 -x_0x23_47_0x23_34_bit0 -x_0x23_47_0x23_32_bit0 -x_0x23_47_0x23_30_bit0 -x_0x23_47_0x23_29_bit0 -x_0x23_47_0x23_27_bit0 -x_0x23_47_0x23_26_bit0 -x_0x23_47_0x23_23_bit0 -x_0x23_47_0x23_20_bit0 -x_0x23_47_0x23_18_bit0 -x_0x23_47_0x23_16_bit0 -x_0x23_47_0x23_13_bit0 -x_0x23_47_0x23_11_bit0 -x_0x23_47_0x23_9_bit0 -x_0x23_47_0x23_8_bit0 -x_0x23_47_0x23_6_bit0 -x_0x23_47_0x23_3_bit0 -x_0x23_47_0x23_1_bit0 -x_0x23_46_0x23_34_bit0 -x_0x23_46_0x23_32_bit0 -x_0x23_46_0x23_30_bit0 -x_0x23_46_0x23_29_bit0 -x_0x23_46_0x23_27_bit0 -x_0x23_46_0x23_26_bit0 -x_0x23_46_0x23_23_bit0 -x_0x23_46_0x23_20_bit0 -x_0x23_46_0x23_18_bit0 -x_0x23_46_0x23_16_bit0 -x_0x23_46_0x23_13_bit0 -x_0x23_46_0x23_11_bit0 -x_0x23_46_0x23_9_bit0 -x_0x23_46_0x23_8_bit0 -x_0x23_46_0x23_6_bit0 -x_0x23_46_0x23_3_bit0 -x_0x23_46_0x23_1_bit0 -x_0x23_45_0x23_34_bit0 -x_0x23_45_0x23_32_bit0 -x_0x23_45_0x23_30_bit0 -x_0x23_45_0x23_29_bit0 -x_0x23_45_0x23_27_bit0 -x_0x23_45_0x23_26_bit0 -x_0x23_45_0x23_23_bit0 -x_0x23_45_0x23_20_bit0 -x_0x23_45_0x23_18_bit0 -x_0x23_45_0x23_16_bit0 -x_0x23_45_0x23_13_bit0 -x_0x23_45_0x23_11_bit0 -x_0x23_45_0x23_9_bit0 -x_0x23_45_0x23_8_bit0 -x_0x23_45_0x23_6_bit0 -x_0x23_45_0x23_3_bit0 -x_0x23_45_0x23_1_bit0 -x_0x23_44_0x23_34_bit0 -x_0x23_44_0x23_32_bit0 -x_0x23_44_0x23_30_bit0 -x_0x23_44_0x23_29_bit0 -x_0x23_44_0x23_27_bit0 -x_0x23_44_0x23_26_bit0 -x_0x23_44_0x23_23_bit0 -x_0x23_44_0x23_20_bit0 -x_0x23_44_0x23_18_bit0 -x_0x23_44_0x23_16_bit0 -x_0x23_44_0x23_13_bit0 -x_0x23_44_0x23_11_bit0 -x_0x23_44_0x23_9_bit0 -x_0x23_44_0x23_8_bit0 -x_0x23_44_0x23_6_bit0 -x_0x23_44_0x23_3_bit0 -x_0x23_44_0x23_1_bit0 -x_0x23_43_0x23_34_bit0 -x_0x23_43_0x23_32_bit0 -x_0x23_43_0x23_30_bit0 -x_0x23_43_0x23_29_bit0 -x_0x23_43_0x23_27_bit0 -x_0x23_43_0x23_26_bit0 -x_0x23_43_0x23_23_bit0 -x_0x23_43_0x23_20_bit0 -x_0x23_43_0x23_18_bit0 -x_0x23_43_0x23_16_bit0 -x_0x23_43_0x23_13_bit0 -x_0x23_43_0x23_11_bit0 -x_0x23_43_0x23_9_bit0 -x_0x23_43_0x23_8_bit0 -x_0x23_43_0x23_6_bit0 -x_0x23_43_0x23_3_bit0 -x_0x23_43_0x23_1_bit0 -x_0x23_42_0x23_34_bit0 -x_0x23_42_0x23_32_bit0 -x_0x23_42_0x23_30_bit0 -x_0x23_42_0x23_29_bit0 -x_0x23_42_0x23_27_bit0 -x_0x23_42_0x23_26_bit0 -x_0x23_42_0x23_23_bit0 -x_0x23_42_0x23_20_bit0 -x_0x23_42_0x23_18_bit0 -x_0x23_42_0x23_16_bit0 -x_0x23_42_0x23_13_bit0 -x_0x23_42_0x23_11_bit0 -x_0x23_42_0x23_9_bit0 -x_0x23_42_0x23_8_bit0 -x_0x23_42_0x23_6_bit0 -x_0x23_42_0x23_3_bit0 -x_0x23_42_0x23_1_bit0 -x_0x23_41_0x23_34_bit0 -x_0x23_41_0x23_32_bit0 -x_0x23_41_0x23_30_bit0 -x_0x23_41_0x23_29_bit0 -x_0x23_41_0x23_27_bit0 -x_0x23_41_0x23_26_bit0 -x_0x23_41_0x23_23_bit0 -x_0x23_41_0x23_20_bit0 -x_0x23_41_0x23_18_bit0 -x_0x23_41_0x23_16_bit0 -x_0x23_41_0x23_13_bit0 -x_0x23_41_0x23_11_bit0 -x_0x23_41_0x23_9_bit0 -x_0x23_41_0x23_8_bit0 -x_0x23_41_0x23_6_bit0 -x_0x23_41_0x23_3_bit0 -x_0x23_41_0x23_1_bit0 -x_0x23_40_0x23_34_bit0 -x_0x23_40_0x23_32_bit0 -x_0x23_40_0x23_30_bit0 -x_0x23_40_0x23_29_bit0 -x_0x23_40_0x23_27_bit0 -x_0x23_40_0x23_26_bit0 -x_0x23_40_0x23_23_bit0 -x_0x23_40_0x23_20_bit0 -x_0x23_40_0x23_18_bit0 -x_0x23_40_0x23_16_bit0 x_0x23_40_0x23_13_bit0 -x_0x23_40_0x23_11_bit0 -x_0x23_40_0x23_9_bit0 -x_0x23_40_0x23_8_bit0 -x_0x23_40_0x23_6_bit0 -x_0x23_40_0x23_3_bit0 -x_0x23_40_0x23_1_bit0 -x_0x23_39_0x23_34_bit0 -x_0x23_39_0x23_32_bit0 -x_0x23_39_0x23_30_bit0 -x_0x23_39_0x23_29_bit0 -x_0x23_39_0x23_27_bit0 -x_0x23_39_0x23_26_bit0 -x_0x23_39_0x23_23_bit0 -x_0x23_39_0x23_20_bit0 -x_0x23_39_0x23_18_bit0 -x_0x23_39_0x23_16_bit0 -x_0x23_39_0x23_13_bit0 -x_0x23_39_0x23_11_bit0 -x_0x23_39_0x23_9_bit0 -x_0x23_39_0x23_8_bit0 -x_0x23_39_0x23_6_bit0 -x_0x23_39_0x23_3_bit0 -x_0x23_39_0x23_1_bit0 -x_0x23_38_0x23_34_bit0 -x_0x23_38_0x23_32_bit0 -x_0x23_38_0x23_30_bit0 -x_0x23_38_0x23_29_bit0 -x_0x23_38_0x23_27_bit0 -x_0x23_38_0x23_26_bit0 -x_0x23_38_0x23_23_bit0 -x_0x23_38_0x23_20_bit0 -x_0x23_38_0x23_18_bit0 -x_0x23_38_0x23_16_bit0 -x_0x23_38_0x23_13_bit0 x_0x23_38_0x23_11_bit0 -x_0x23_38_0x23_9_bit0 -x_0x23_38_0x23_8_bit0 -x_0x23_38_0x23_6_bit0 -x_0x23_38_0x23_3_bit0 -x_0x23_38_0x23_1_bit0 -x_0x23_37_0x23_34_bit0 -x_0x23_37_0x23_32_bit0 -x_0x23_37_0x23_30_bit0 -x_0x23_37_0x23_29_bit0 -x_0x23_37_0x23_27_bit0 -x_0x23_37_0x23_26_bit0 -x_0x23_37_0x23_23_bit0 -x_0x23_37_0x23_20_bit0 -x_0x23_37_0x23_18_bit0 -x_0x23_37_0x23_16_bit0 -x_0x23_37_0x23_13_bit0 -x_0x23_37_0x23_11_bit0 x_0x23_37_0x23_9_bit0 -x_0x23_37_0x23_8_bit0 -x_0x23_37_0x23_6_bit0 -x_0x23_37_0x23_3_bit0 -x_0x23_37_0x23_1_bit0 -x_0x23_36_0x23_34_bit0 -x_0x23_36_0x23_32_bit0 -x_0x23_36_0x23_30_bit0 -x_0x23_36_0x23_29_bit0 -x_0x23_36_0x23_27_bit0 -x_0x23_36_0x23_26_bit0 -x_0x23_36_0x23_23_bit0 -x_0x23_36_0x23_20_bit0 -x_0x23_36_0x23_18_bit0 -x_0x23_36_0x23_16_bit0 -x_0x23_36_0x23_13_bit0 -x_0x23_36_0x23_11_bit0 -x_0x23_36_0x23_9_bit0 -x_0x23_36_0x23_8_bit0 -x_0x23_36_0x23_6_bit0 -x_0x23_36_0x23_3_bit0 -x_0x23_36_0x23_1_bit0 -x_0x23_35_0x23_34_bit0 -x_0x23_35_0x23_32_bit0 -x_0x23_35_0x23_30_bit0 -x_0x23_35_0x23_29_bit0 -x_0x23_35_0x23_27_bit0 -x_0x23_35_0x23_26_bit0 -x_0x23_35_0x23_23_bit0 -x_0x23_35_0x23_20_bit0 -x_0x23_35_0x23_18_bit0 -x_0x23_35_0x23_16_bit0 -x_0x23_35_0x23_13_bit0 -x_0x23_35_0x23_11_bit0 -x_0x23_35_0x23_9_bit0 -x_0x23_35_0x23_8_bit0 -x_0x23_35_0x23_6_bit0 -x_0x23_35_0x23_3_bit0 -x_0x23_35_0x23_1_bit0 -x_0x23_34_0x23_34_bit0 -x_0x23_34_0x23_32_bit0 -x_0x23_34_0x23_30_bit0 -x_0x23_34_0x23_29_bit0 -x_0x23_34_0x23_27_bit0 -x_0x23_34_0x23_26_bit0 -x_0x23_34_0x23_23_bit0 -x_0x23_34_0x23_20_bit0 -x_0x23_34_0x23_18_bit0 x_0x23_34_0x23_16_bit0 -x_0x23_34_0x23_13_bit0 -x_0x23_34_0x23_11_bit0 -x_0x23_34_0x23_9_bit0 -x_0x23_34_0x23_8_bit0 -x_0x23_34_0x23_6_bit0 -x_0x23_34_0x23_3_bit0 -x_0x23_34_0x23_1_bit0 -x_0x23_33_0x23_34_bit0 -x_0x23_33_0x23_32_bit0 -x_0x23_33_0x23_30_bit0 x_0x23_33_0x23_29_bit0 -x_0x23_33_0x23_27_bit0 -x_0x23_33_0x23_26_bit0 -x_0x23_33_0x23_23_bit0 -x_0x23_33_0x23_20_bit0 -x_0x23_33_0x23_18_bit0 -x_0x23_33_0x23_16_bit0 -x_0x23_33_0x23_13_bit0 -x_0x23_33_0x23_11_bit0 -x_0x23_33_0x23_9_bit0 -x_0x23_33_0x23_8_bit0 -x_0x23_33_0x23_6_bit0 -x_0x23_33_0x23_3_bit0 -x_0x23_33_0x23_1_bit0 -x_0x23_32_0x23_34_bit0 -x_0x23_32_0x23_32_bit0 x_0x23_32_0x23_30_bit0 -x_0x23_32_0x23_29_bit0 -x_0x23_32_0x23_27_bit0 -x_0x23_32_0x23_26_bit0 -x_0x23_32_0x23_23_bit0 -x_0x23_32_0x23_20_bit0 -x_0x23_32_0x23_18_bit0 -x_0x23_32_0x23_16_bit0 -x_0x23_32_0x23_13_bit0 -x_0x23_32_0x23_11_bit0 -x_0x23_32_0x23_9_bit0 -x_0x23_32_0x23_8_bit0 -x_0x23_32_0x23_6_bit0 -x_0x23_32_0x23_3_bit0 -x_0x23_32_0x23_1_bit0 -x_0x23_31_0x23_34_bit0 -x_0x23_31_0x23_32_bit0 -x_0x23_31_0x23_30_bit0 -x_0x23_31_0x23_29_bit0 -x_0x23_31_0x23_27_bit0 -x_0x23_31_0x23_26_bit0 -x_0x23_31_0x23_23_bit0 -x_0x23_31_0x23_20_bit0 -x_0x23_31_0x23_18_bit0 -x_0x23_31_0x23_16_bit0 -x_0x23_31_0x23_13_bit0 -x_0x23_31_0x23_11_bit0 -x_0x23_31_0x23_9_bit0 -x_0x23_31_0x23_8_bit0 -x_0x23_31_0x23_6_bit0 -x_0x23_31_0x23_3_bit0 -x_0x23_31_0x23_1_bit0 -x_0x23_30_0x23_34_bit0 -x_0x23_30_0x23_32_bit0 -x_0x23_30_0x23_30_bit0 -x_0x23_30_0x23_29_bit0 -x_0x23_30_0x23_27_bit0 -x_0x23_30_0x23_26_bit0 -x_0x23_30_0x23_23_bit0 -x_0x23_30_0x23_20_bit0 -x_0x23_30_0x23_18_bit0 -x_0x23_30_0x23_16_bit0 -x_0x23_30_0x23_13_bit0 -x_0x23_30_0x23_11_bit0 -x_0x23_30_0x23_9_bit0 -x_0x23_30_0x23_8_bit0 x_0x23_30_0x23_6_bit0 -x_0x23_30_0x23_3_bit0 -x_0x23_30_0x23_1_bit0 -x_0x23_29_0x23_34_bit0 -x_0x23_29_0x23_32_bit0 -x_0x23_29_0x23_30_bit0 -x_0x23_29_0x23_29_bit0 -x_0x23_29_0x23_27_bit0 -x_0x23_29_0x23_26_bit0 -x_0x23_29_0x23_23_bit0 -x_0x23_29_0x23_20_bit0 -x_0x23_29_0x23_18_bit0 -x_0x23_29_0x23_16_bit0 -x_0x23_29_0x23_13_bit0 -x_0x23_29_0x23_11_bit0 -x_0x23_29_0x23_9_bit0 x_0x23_29_0x23_8_bit0 -x_0x23_29_0x23_6_bit0 -x_0x23_29_0x23_3_bit0 -x_0x23_29_0x23_1_bit0 -x_0x23_28_0x23_34_bit0 -x_0x23_28_0x23_32_bit0 -x_0x23_28_0x23_30_bit0 -x_0x23_28_0x23_29_bit0 -x_0x23_28_0x23_27_bit0 -x_0x23_28_0x23_26_bit0 -x_0x23_28_0x23_23_bit0 -x_0x23_28_0x23_20_bit0 x_0x23_28_0x23_18_bit0 -x_0x23_28_0x23_16_bit0 -x_0x23_28_0x23_13_bit0 -x_0x23_28_0x23_11_bit0 -x_0x23_28_0x23_9_bit0 -x_0x23_28_0x23_8_bit0 -x_0x23_28_0x23_6_bit0 -x_0x23_28_0x23_3_bit0 -x_0x23_28_0x23_1_bit0 -x_0x23_27_0x23_34_bit0 -x_0x23_27_0x23_32_bit0 -x_0x23_27_0x23_30_bit0 -x_0x23_27_0x23_29_bit0 x_0x23_27_0x23_27_bit0 -x_0x23_27_0x23_26_bit0 -x_0x23_27_0x23_23_bit0 -x_0x23_27_0x23_20_bit0 -x_0x23_27_0x23_18_bit0 -x_0x23_27_0x23_16_bit0 -x_0x23_27_0x23_13_bit0 -x_0x23_27_0x23_11_bit0 -x_0x23_27_0x23_9_bit0 -x_0x23_27_0x23_8_bit0 -x_0x23_27_0x23_6_bit0 -x_0x23_27_0x23_3_bit0 -x_0x23_27_0x23_1_bit0 -x_0x23_26_0x23_34_bit0 -x_0x23_26_0x23_32_bit0 -x_0x23_26_0x23_30_bit0 -x_0x23_26_0x23_29_bit0 -x_0x23_26_0x23_27_bit0 -x_0x23_26_0x23_26_bit0 -x_0x23_26_0x23_23_bit0 -x_0x23_26_0x23_20_bit0 -x_0x23_26_0x23_18_bit0 -x_0x23_26_0x23_16_bit0 -x_0x23_26_0x23_13_bit0 -x_0x23_26_0x23_11_bit0 -x_0x23_26_0x23_9_bit0 -x_0x23_26_0x23_8_bit0 -x_0x23_26_0x23_6_bit0 -x_0x23_26_0x23_3_bit0 -x_0x23_26_0x23_1_bit0 x_0x23_25_0x23_34_bit0 -x_0x23_25_0x23_32_bit0 -x_0x23_25_0x23_30_bit0 -x_0x23_25_0x23_29_bit0 -x_0x23_25_0x23_27_bit0 -x_0x23_25_0x23_26_bit0 -x_0x23_25_0x23_23_bit0 -x_0x23_25_0x23_20_bit0 -x_0x23_25_0x23_18_bit0 -x_0x23_25_0x23_16_bit0 -x_0x23_25_0x23_13_bit0 -x_0x23_25_0x23_11_bit0 -x_0x23_25_0x23_9_bit0 -x_0x23_25_0x23_8_bit0 -x_0x23_25_0x23_6_bit0 -x_0x23_25_0x23_3_bit0 -x_0x23_25_0x23_1_bit0 -x_0x23_24_0x23_34_bit0 x_0x23_24_0x23_32_bit0 -x_0x23_24_0x23_30_bit0 -x_0x23_24_0x23_29_bit0 -x_0x23_24_0x23_27_bit0 -x_0x23_24_0x23_26_bit0 -x_0x23_24_0x23_23_bit0 -x_0x23_24_0x23_20_bit0 -x_0x23_24_0x23_18_bit0 -x_0x23_24_0x23_16_bit0 -x_0x23_24_0x23_13_bit0 -x_0x23_24_0x23_11_bit0 -x_0x23_24_0x23_9_bit0 -x_0x23_24_0x23_8_bit0 -x_0x23_24_0x23_6_bit0 -x_0x23_24_0x23_3_bit0 -x_0x23_24_0x23_1_bit0 -x_0x23_23_0x23_34_bit0 -x_0x23_23_0x23_32_bit0 -x_0x23_23_0x23_30_bit0 -x_0x23_23_0x23_29_bit0 -x_0x23_23_0x23_27_bit0 -x_0x23_23_0x23_26_bit0 -x_0x23_23_0x23_23_bit0 -x_0x23_23_0x23_20_bit0 -x_0x23_23_0x23_18_bit0 -x_0x23_23_0x23_16_bit0 -x_0x23_23_0x23_13_bit0 -x_0x23_23_0x23_11_bit0 -x_0x23_23_0x23_9_bit0 -x_0x23_23_0x23_8_bit0 -x_0x23_23_0x23_6_bit0 -x_0x23_23_0x23_3_bit0 -x_0x23_23_0x23_1_bit0 -x_0x23_22_0x23_34_bit0 -x_0x23_22_0x23_32_bit0 -x_0x23_22_0x23_30_bit0 -x_0x23_22_0x23_29_bit0 -x_0x23_22_0x23_27_bit0 -x_0x23_22_0x23_26_bit0 -x_0x23_22_0x23_23_bit0 -x_0x23_22_0x23_20_bit0 -x_0x23_22_0x23_18_bit0 -x_0x23_22_0x23_16_bit0 -x_0x23_22_0x23_13_bit0 -x_0x23_22_0x23_11_bit0 -x_0x23_22_0x23_9_bit0 -x_0x23_22_0x23_8_bit0 -x_0x23_22_0x23_6_bit0 -x_0x23_22_0x23_3_bit0 -x_0x23_22_0x23_1_bit0 -x_0x23_21_0x23_34_bit0 -x_0x23_21_0x23_32_bit0 -x_0x23_21_0x23_30_bit0 -x_0x23_21_0x23_29_bit0 -x_0x23_21_0x23_27_bit0 -x_0x23_21_0x23_26_bit0 -x_0x23_21_0x23_23_bit0 -x_0x23_21_0x23_20_bit0 -x_0x23_21_0x23_18_bit0 -x_0x23_21_0x23_16_bit0 -x_0x23_21_0x23_13_bit0 -x_0x23_21_0x23_11_bit0 -x_0x23_21_0x23_9_bit0 -x_0x23_21_0x23_8_bit0 -x_0x23_21_0x23_6_bit0 -x_0x23_21_0x23_3_bit0 -x_0x23_21_0x23_1_bit0 -x_0x23_20_0x23_34_bit0 -x_0x23_20_0x23_32_bit0 -x_0x23_20_0x23_30_bit0 -x_0x23_20_0x23_29_bit0 -x_0x23_20_0x23_27_bit0 -x_0x23_20_0x23_26_bit0 -x_0x23_20_0x23_23_bit0 x_0x23_20_0x23_20_bit0 -x_0x23_20_0x23_18_bit0 -x_0x23_20_0x23_16_bit0 -x_0x23_20_0x23_13_bit0 -x_0x23_20_0x23_11_bit0 -x_0x23_20_0x23_9_bit0 -x_0x23_20_0x23_8_bit0 -x_0x23_20_0x23_6_bit0 -x_0x23_20_0x23_3_bit0 -x_0x23_20_0x23_1_bit0 -x_0x23_19_0x23_34_bit0 -x_0x23_19_0x23_32_bit0 -x_0x23_19_0x23_30_bit0 -x_0x23_19_0x23_29_bit0 -x_0x23_19_0x23_27_bit0 x_0x23_19_0x23_26_bit0 -x_0x23_19_0x23_23_bit0 -x_0x23_19_0x23_20_bit0 -x_0x23_19_0x23_18_bit0 -x_0x23_19_0x23_16_bit0 -x_0x23_19_0x23_13_bit0 -x_0x23_19_0x23_11_bit0 -x_0x23_19_0x23_9_bit0 -x_0x23_19_0x23_8_bit0 -x_0x23_19_0x23_6_bit0 -x_0x23_19_0x23_3_bit0 -x_0x23_19_0x23_1_bit0 -x_0x23_18_0x23_34_bit0 -x_0x23_18_0x23_32_bit0 -x_0x23_18_0x23_30_bit0 -x_0x23_18_0x23_29_bit0 -x_0x23_18_0x23_27_bit0 -x_0x23_18_0x23_26_bit0 -x_0x23_18_0x23_23_bit0 -x_0x23_18_0x23_20_bit0 -x_0x23_18_0x23_18_bit0 -x_0x23_18_0x23_16_bit0 -x_0x23_18_0x23_13_bit0 -x_0x23_18_0x23_11_bit0 -x_0x23_18_0x23_9_bit0 -x_0x23_18_0x23_8_bit0 -x_0x23_18_0x23_6_bit0 -x_0x23_18_0x23_3_bit0 -x_0x23_18_0x23_1_bit0 -x_0x23_17_0x23_34_bit0 -x_0x23_17_0x23_32_bit0 -x_0x23_17_0x23_30_bit0 -x_0x23_17_0x23_29_bit0 -x_0x23_17_0x23_27_bit0 -x_0x23_17_0x23_26_bit0 -x_0x23_17_0x23_23_bit0 -x_0x23_17_0x23_20_bit0 -x_0x23_17_0x23_18_bit0 -x_0x23_17_0x23_16_bit0 -x_0x23_17_0x23_13_bit0 -x_0x23_17_0x23_11_bit0 -x_0x23_17_0x23_9_bit0 -x_0x23_17_0x23_8_bit0 -x_0x23_17_0x23_6_bit0 -x_0x23_17_0x23_3_bit0 -x_0x23_17_0x23_1_bit0 -x_0x23_16_0x23_34_bit0 -x_0x23_16_0x23_32_bit0 -x_0x23_16_0x23_30_bit0 -x_0x23_16_0x23_29_bit0 -x_0x23_16_0x23_27_bit0 -x_0x23_16_0x23_26_bit0 -x_0x23_16_0x23_23_bit0 -x_0x23_16_0x23_20_bit0 -x_0x23_16_0x23_18_bit0 -x_0x23_16_0x23_16_bit0 -x_0x23_16_0x23_13_bit0 -x_0x23_16_0x23_11_bit0 -x_0x23_16_0x23_9_bit0 -x_0x23_16_0x23_8_bit0 -x_0x23_16_0x23_6_bit0 x_0x23_16_0x23_3_bit0 -x_0x23_16_0x23_1_bit0 -x_0x23_15_0x23_34_bit0 -x_0x23_15_0x23_32_bit0 -x_0x23_15_0x23_30_bit0 -x_0x23_15_0x23_29_bit0 -x_0x23_15_0x23_27_bit0 -x_0x23_15_0x23_26_bit0 -x_0x23_15_0x23_23_bit0 -x_0x23_15_0x23_20_bit0 -x_0x23_15_0x23_18_bit0 -x_0x23_15_0x23_16_bit0 -x_0x23_15_0x23_13_bit0 -x_0x23_15_0x23_11_bit0 -x_0x23_15_0x23_9_bit0 -x_0x23_15_0x23_8_bit0 -x_0x23_15_0x23_6_bit0 -x_0x23_15_0x23_3_bit0 -x_0x23_15_0x23_1_bit0 -x_0x23_14_0x23_34_bit0 -x_0x23_14_0x23_32_bit0 -x_0x23_14_0x23_30_bit0 -x_0x23_14_0x23_29_bit0 -x_0x23_14_0x23_27_bit0 -x_0x23_14_0x23_26_bit0 -x_0x23_14_0x23_23_bit0 -x_0x23_14_0x23_20_bit0 -x_0x23_14_0x23_18_bit0 -x_0x23_14_0x23_16_bit0 -x_0x23_14_0x23_13_bit0 -x_0x23_14_0x23_11_bit0 -x_0x23_14_0x23_9_bit0 -x_0x23_14_0x23_8_bit0 -x_0x23_14_0x23_6_bit0 -x_0x23_14_0x23_3_bit0 -x_0x23_14_0x23_1_bit0 -x_0x23_13_0x23_34_bit0 -x_0x23_13_0x23_32_bit0 -x_0x23_13_0x23_30_bit0 -x_0x23_13_0x23_29_bit0 -x_0x23_13_0x23_27_bit0 -x_0x23_13_0x23_26_bit0 -x_0x23_13_0x23_23_bit0 -x_0x23_13_0x23_20_bit0 -x_0x23_13_0x23_18_bit0 -x_0x23_13_0x23_16_bit0 -x_0x23_13_0x23_13_bit0 -x_0x23_13_0x23_11_bit0 -x_0x23_13_0x23_9_bit0 -x_0x23_13_0x23_8_bit0 -x_0x23_13_0x23_6_bit0 -x_0x23_13_0x23_3_bit0 -x_0x23_13_0x23_1_bit0 -x_0x23_12_0x23_34_bit0 -x_0x23_12_0x23_32_bit0 -x_0x23_12_0x23_30_bit0 -x_0x23_12_0x23_29_bit0 -x_0x23_12_0x23_27_bit0 -x_0x23_12_0x23_26_bit0 -x_0x23_12_0x23_23_bit0 -x_0x23_12_0x23_20_bit0 -x_0x23_12_0x23_18_bit0 -x_0x23_12_0x23_16_bit0 -x_0x23_12_0x23_13_bit0 -x_0x23_12_0x23_11_bit0 -x_0x23_12_0x23_9_bit0 -x_0x23_12_0x23_8_bit0 -x_0x23_12_0x23_6_bit0 -x_0x23_12_0x23_3_bit0 -x_0x23_12_0x23_1_bit0 -x_0x23_11_0x23_34_bit0 -x_0x23_11_0x23_32_bit0 -x_0x23_11_0x23_30_bit0 -x_0x23_11_0x23_29_bit0 -x_0x23_11_0x23_27_bit0 -x_0x23_11_0x23_26_bit0 -x_0x23_11_0x23_23_bit0 -x_0x23_11_0x23_20_bit0 -x_0x23_11_0x23_18_bit0 -x_0x23_11_0x23_16_bit0 -x_0x23_11_0x23_13_bit0 -x_0x23_11_0x23_11_bit0 -x_0x23_11_0x23_9_bit0 -x_0x23_11_0x23_8_bit0 -x_0x23_11_0x23_6_bit0 -x_0x23_11_0x23_3_bit0 -x_0x23_11_0x23_1_bit0 -x_0x23_10_0x23_34_bit0 -x_0x23_10_0x23_32_bit0 -x_0x23_10_0x23_30_bit0 -x_0x23_10_0x23_29_bit0 -x_0x23_10_0x23_27_bit0 -x_0x23_10_0x23_26_bit0 -x_0x23_10_0x23_23_bit0 -x_0x23_10_0x23_20_bit0 -x_0x23_10_0x23_18_bit0 -x_0x23_10_0x23_16_bit0 -x_0x23_10_0x23_13_bit0 -x_0x23_10_0x23_11_bit0 -x_0x23_10_0x23_9_bit0 -x_0x23_10_0x23_8_bit0 -x_0x23_10_0x23_6_bit0 -x_0x23_10_0x23_3_bit0 -x_0x23_10_0x23_1_bit0 -x_0x23_9_0x23_34_bit0 -x_0x23_9_0x23_32_bit0 -x_0x23_9_0x23_30_bit0 -x_0x23_9_0x23_29_bit0 -x_0x23_9_0x23_27_bit0 -x_0x23_9_0x23_26_bit0 -x_0x23_9_0x23_23_bit0 -x_0x23_9_0x23_20_bit0 -x_0x23_9_0x23_18_bit0 -x_0x23_9_0x23_16_bit0 -x_0x23_9_0x23_13_bit0 -x_0x23_9_0x23_11_bit0 -x_0x23_9_0x23_9_bit0 -x_0x23_9_0x23_8_bit0 -x_0x23_9_0x23_6_bit0 -x_0x23_9_0x23_3_bit0 -x_0x23_9_0x23_1_bit0 -x_0x23_8_0x23_34_bit0 -x_0x23_8_0x23_32_bit0 -x_0x23_8_0x23_30_bit0 -x_0x23_8_0x23_29_bit0 -x_0x23_8_0x23_27_bit0 -x_0x23_8_0x23_26_bit0 -x_0x23_8_0x23_23_bit0 -x_0x23_8_0x23_20_bit0 -x_0x23_8_0x23_18_bit0 -x_0x23_8_0x23_16_bit0 -x_0x23_8_0x23_13_bit0 -x_0x23_8_0x23_11_bit0 -x_0x23_8_0x23_9_bit0 -x_0x23_8_0x23_8_bit0 -x_0x23_8_0x23_6_bit0 -x_0x23_8_0x23_3_bit0 -x_0x23_8_0x23_1_bit0 -x_0x23_7_0x23_34_bit0 -x_0x23_7_0x23_32_bit0 -x_0x23_7_0x23_30_bit0 -x_0x23_7_0x23_29_bit0 -x_0x23_7_0x23_27_bit0 -x_0x23_7_0x23_26_bit0 -x_0x23_7_0x23_23_bit0 -x_0x23_7_0x23_20_bit0 -x_0x23_7_0x23_18_bit0 -x_0x23_7_0x23_16_bit0 -x_0x23_7_0x23_13_bit0 -x_0x23_7_0x23_11_bit0 -x_0x23_7_0x23_9_bit0 -x_0x23_7_0x23_8_bit0 -x_0x23_7_0x23_6_bit0 -x_0x23_7_0x23_3_bit0 -x_0x23_7_0x23_1_bit0 -x_0x23_6_0x23_34_bit0 -x_0x23_6_0x23_32_bit0 -x_0x23_6_0x23_30_bit0 -x_0x23_6_0x23_29_bit0 -x_0x23_6_0x23_27_bit0 -x_0x23_6_0x23_26_bit0 -x_0x23_6_0x23_23_bit0 -x_0x23_6_0x23_20_bit0 -x_0x23_6_0x23_18_bit0 -x_0x23_6_0x23_16_bit0 -x_0x23_6_0x23_13_bit0 -x_0x23_6_0x23_11_bit0 -x_0x23_6_0x23_9_bit0 -x_0x23_6_0x23_8_bit0 -x_0x23_6_0x23_6_bit0 -x_0x23_6_0x23_3_bit0 -x_0x23_6_0x23_1_bit0 -x_0x23_5_0x23_34_bit0 -x_0x23_5_0x23_32_bit0 -x_0x23_5_0x23_30_bit0 -x_0x23_5_0x23_29_bit0 -x_0x23_5_0x23_27_bit0 -x_0x23_5_0x23_26_bit0 -x_0x23_5_0x23_23_bit0 -x_0x23_5_0x23_20_bit0 -x_0x23_5_0x23_18_bit0 -x_0x23_5_0x23_16_bit0 -x_0x23_5_0x23_13_bit0 -x_0x23_5_0x23_11_bit0 -x_0x23_5_0x23_9_bit0 -x_0x23_5_0x23_8_bit0 -x_0x23_5_0x23_6_bit0 -x_0x23_5_0x23_3_bit0 -x_0x23_5_0x23_1_bit0 -x_0x23_4_0x23_34_bit0 -x_0x23_4_0x23_32_bit0 -x_0x23_4_0x23_30_bit0 -x_0x23_4_0x23_29_bit0 -x_0x23_4_0x23_27_bit0 -x_0x23_4_0x23_26_bit0 -x_0x23_4_0x23_23_bit0 -x_0x23_4_0x23_20_bit0 -x_0x23_4_0x23_18_bit0 -x_0x23_4_0x23_16_bit0 -x_0x23_4_0x23_13_bit0 -x_0x23_4_0x23_11_bit0 -x_0x23_4_0x23_9_bit0 -x_0x23_4_0x23_8_bit0 -x_0x23_4_0x23_6_bit0 -x_0x23_4_0x23_3_bit0 -x_0x23_4_0x23_1_bit0 -x_0x23_3_0x23_34_bit0 -x_0x23_3_0x23_32_bit0 -x_0x23_3_0x23_30_bit0 -x_0x23_3_0x23_29_bit0 -x_0x23_3_0x23_27_bit0 -x_0x23_3_0x23_26_bit0 x_0x23_3_0x23_23_bit0 -x_0x23_3_0x23_20_bit0 -x_0x23_3_0x23_18_bit0 -x_0x23_3_0x23_16_bit0 -x_0x23_3_0x23_13_bit0 -x_0x23_3_0x23_11_bit0 -x_0x23_3_0x23_9_bit0 -x_0x23_3_0x23_8_bit0 -x_0x23_3_0x23_6_bit0 -x_0x23_3_0x23_3_bit0 -x_0x23_3_0x23_1_bit0 -x_0x23_2_0x23_34_bit0 -x_0x23_2_0x23_32_bit0 -x_0x23_2_0x23_30_bit0 -x_0x23_2_0x23_29_bit0 -x_0x23_2_0x23_27_bit0 -x_0x23_2_0x23_26_bit0 -x_0x23_2_0x23_23_bit0 -x_0x23_2_0x23_20_bit0 -x_0x23_2_0x23_18_bit0 -x_0x23_2_0x23_16_bit0 -x_0x23_2_0x23_13_bit0 -x_0x23_2_0x23_11_bit0 -x_0x23_2_0x23_9_bit0 -x_0x23_2_0x23_8_bit0 -x_0x23_2_0x23_6_bit0 -x_0x23_2_0x23_3_bit0 x_0x23_2_0x23_1_bit0 -x_0x23_1_0x23_34_bit0 -x_0x23_1_0x23_32_bit0 -x_0x23_1_0x23_30_bit0 -x_0x23_1_0x23_29_bit0 -x_0x23_1_0x23_27_bit0 -x_0x23_1_0x23_26_bit0 -x_0x23_1_0x23_23_bit0 -x_0x23_1_0x23_20_bit0 -x_0x23_1_0x23_18_bit0 -x_0x23_1_0x23_16_bit0 -x_0x23_1_0x23_13_bit0 -x_0x23_1_0x23_11_bit0 -x_0x23_1_0x23_9_bit0 -x_0x23_1_0x23_8_bit0 -x_0x23_1_0x23_6_bit0 -x_0x23_1_0x23_3_bit0 -x_0x23_1_0x23_1_bit0 -x_0x23_49_0x23_35_bit0 -x_0x23_49_0x23_33_bit0 -x_0x23_49_0x23_31_bit0 -x_0x23_49_0x23_28_bit0 -x_0x23_49_0x23_25_bit0 -x_0x23_49_0x23_24_bit0 -x_0x23_49_0x23_22_bit0 -x_0x23_49_0x23_21_bit0 -x_0x23_49_0x23_19_bit0 -x_0x23_49_0x23_17_bit0 -x_0x23_49_0x23_15_bit0 -x_0x23_49_0x23_14_bit0 -x_0x23_49_0x23_12_bit0 -x_0x23_49_0x23_10_bit0 -x_0x23_49_0x23_7_bit0 -x_0x23_49_0x23_5_bit0 -x_0x23_49_0x23_4_bit0 -x_0x23_49_0x23_2_bit0 -x_0x23_48_0x23_35_bit0 -x_0x23_48_0x23_33_bit0 -x_0x23_48_0x23_31_bit0 -x_0x23_48_0x23_28_bit0 -x_0x23_48_0x23_25_bit0 -x_0x23_48_0x23_24_bit0 -x_0x23_48_0x23_22_bit0 -x_0x23_48_0x23_21_bit0 -x_0x23_48_0x23_19_bit0 -x_0x23_48_0x23_17_bit0 -x_0x23_48_0x23_15_bit0 x_0x23_48_0x23_14_bit0 -x_0x23_48_0x23_12_bit0 -x_0x23_48_0x23_10_bit0 -x_0x23_48_0x23_7_bit0 -x_0x23_48_0x23_5_bit0 -x_0x23_48_0x23_4_bit0 -x_0x23_48_0x23_2_bit0 -x_0x23_47_0x23_35_bit0 -x_0x23_47_0x23_33_bit0 -x_0x23_47_0x23_31_bit0 -x_0x23_47_0x23_28_bit0 -x_0x23_47_0x23_25_bit0 -x_0x23_47_0x23_24_bit0 -x_0x23_47_0x23_22_bit0 -x_0x23_47_0x23_21_bit0 -x_0x23_47_0x23_19_bit0 -x_0x23_47_0x23_17_bit0 -x_0x23_47_0x23_15_bit0 -x_0x23_47_0x23_14_bit0 -x_0x23_47_0x23_12_bit0 -x_0x23_47_0x23_10_bit0 -x_0x23_47_0x23_7_bit0 -x_0x23_47_0x23_5_bit0 -x_0x23_47_0x23_4_bit0 -x_0x23_47_0x23_2_bit0 -x_0x23_46_0x23_35_bit0 -x_0x23_46_0x23_33_bit0 -x_0x23_46_0x23_31_bit0 -x_0x23_46_0x23_28_bit0 -x_0x23_46_0x23_25_bit0 -x_0x23_46_0x23_24_bit0 -x_0x23_46_0x23_22_bit0 -x_0x23_46_0x23_21_bit0 -x_0x23_46_0x23_19_bit0 -x_0x23_46_0x23_17_bit0 -x_0x23_46_0x23_15_bit0 -x_0x23_46_0x23_14_bit0 -x_0x23_46_0x23_12_bit0 -x_0x23_46_0x23_10_bit0 -x_0x23_46_0x23_7_bit0 -x_0x23_46_0x23_5_bit0 -x_0x23_46_0x23_4_bit0 -x_0x23_46_0x23_2_bit0 -x_0x23_45_0x23_35_bit0 -x_0x23_45_0x23_33_bit0 -x_0x23_45_0x23_31_bit0 -x_0x23_45_0x23_28_bit0 -x_0x23_45_0x23_25_bit0 -x_0x23_45_0x23_24_bit0 -x_0x23_45_0x23_22_bit0 -x_0x23_45_0x23_21_bit0 -x_0x23_45_0x23_19_bit0 -x_0x23_45_0x23_17_bit0 -x_0x23_45_0x23_15_bit0 -x_0x23_45_0x23_14_bit0 -x_0x23_45_0x23_12_bit0 x_0x23_45_0x23_10_bit0 -x_0x23_45_0x23_7_bit0 -x_0x23_45_0x23_5_bit0 -x_0x23_45_0x23_4_bit0 -x_0x23_45_0x23_2_bit0 -x_0x23_44_0x23_35_bit0 -x_0x23_44_0x23_33_bit0 -x_0x23_44_0x23_31_bit0 -x_0x23_44_0x23_28_bit0 -x_0x23_44_0x23_25_bit0 -x_0x23_44_0x23_24_bit0 -x_0x23_44_0x23_22_bit0 -x_0x23_44_0x23_21_bit0 -x_0x23_44_0x23_19_bit0 -x_0x23_44_0x23_17_bit0 -x_0x23_44_0x23_15_bit0 -x_0x23_44_0x23_14_bit0 -x_0x23_44_0x23_12_bit0 -x_0x23_44_0x23_10_bit0 -x_0x23_44_0x23_7_bit0 -x_0x23_44_0x23_5_bit0 -x_0x23_44_0x23_4_bit0 -x_0x23_44_0x23_2_bit0 -x_0x23_43_0x23_35_bit0 -x_0x23_43_0x23_33_bit0 -x_0x23_43_0x23_31_bit0 -x_0x23_43_0x23_28_bit0 -x_0x23_43_0x23_25_bit0 -x_0x23_43_0x23_24_bit0 -x_0x23_43_0x23_22_bit0 -x_0x23_43_0x23_21_bit0 -x_0x23_43_0x23_19_bit0 -x_0x23_43_0x23_17_bit0 -x_0x23_43_0x23_15_bit0 -x_0x23_43_0x23_14_bit0 -x_0x23_43_0x23_12_bit0 -x_0x23_43_0x23_10_bit0 -x_0x23_43_0x23_7_bit0 -x_0x23_43_0x23_5_bit0 -x_0x23_43_0x23_4_bit0 -x_0x23_43_0x23_2_bit0 -x_0x23_42_0x23_35_bit0 -x_0x23_42_0x23_33_bit0 -x_0x23_42_0x23_31_bit0 -x_0x23_42_0x23_28_bit0 -x_0x23_42_0x23_25_bit0 -x_0x23_42_0x23_24_bit0 -x_0x23_42_0x23_22_bit0 -x_0x23_42_0x23_21_bit0 -x_0x23_42_0x23_19_bit0 -x_0x23_42_0x23_17_bit0 -x_0x23_42_0x23_15_bit0 -x_0x23_42_0x23_14_bit0 -x_0x23_42_0x23_12_bit0 -x_0x23_42_0x23_10_bit0 -x_0x23_42_0x23_7_bit0 -x_0x23_42_0x23_5_bit0 -x_0x23_42_0x23_4_bit0 -x_0x23_42_0x23_2_bit0 -x_0x23_41_0x23_35_bit0 -x_0x23_41_0x23_33_bit0 -x_0x23_41_0x23_31_bit0 -x_0x23_41_0x23_28_bit0 -x_0x23_41_0x23_25_bit0 -x_0x23_41_0x23_24_bit0 -x_0x23_41_0x23_22_bit0 -x_0x23_41_0x23_21_bit0 -x_0x23_41_0x23_19_bit0 -x_0x23_41_0x23_17_bit0 x_0x23_41_0x23_15_bit0 -x_0x23_41_0x23_14_bit0 -x_0x23_41_0x23_12_bit0 -x_0x23_41_0x23_10_bit0 -x_0x23_41_0x23_7_bit0 -x_0x23_41_0x23_5_bit0 -x_0x23_41_0x23_4_bit0 -x_0x23_41_0x23_2_bit0 -x_0x23_40_0x23_35_bit0 -x_0x23_40_0x23_33_bit0 -x_0x23_40_0x23_31_bit0 -x_0x23_40_0x23_28_bit0 -x_0x23_40_0x23_25_bit0 -x_0x23_40_0x23_24_bit0 -x_0x23_40_0x23_22_bit0 -x_0x23_40_0x23_21_bit0 -x_0x23_40_0x23_19_bit0 -x_0x23_40_0x23_17_bit0 -x_0x23_40_0x23_15_bit0 -x_0x23_40_0x23_14_bit0 -x_0x23_40_0x23_12_bit0 -x_0x23_40_0x23_10_bit0 -x_0x23_40_0x23_7_bit0 -x_0x23_40_0x23_5_bit0 -x_0x23_40_0x23_4_bit0 -x_0x23_40_0x23_2_bit0 -x_0x23_39_0x23_35_bit0 -x_0x23_39_0x23_33_bit0 -x_0x23_39_0x23_31_bit0 -x_0x23_39_0x23_28_bit0 -x_0x23_39_0x23_25_bit0 -x_0x23_39_0x23_24_bit0 -x_0x23_39_0x23_22_bit0 -x_0x23_39_0x23_21_bit0 -x_0x23_39_0x23_19_bit0 -x_0x23_39_0x23_17_bit0 -x_0x23_39_0x23_15_bit0 -x_0x23_39_0x23_14_bit0 x_0x23_39_0x23_12_bit0 -x_0x23_39_0x23_10_bit0 -x_0x23_39_0x23_7_bit0 -x_0x23_39_0x23_5_bit0 -x_0x23_39_0x23_4_bit0 -x_0x23_39_0x23_2_bit0 -x_0x23_38_0x23_35_bit0 -x_0x23_38_0x23_33_bit0 -x_0x23_38_0x23_31_bit0 -x_0x23_38_0x23_28_bit0 -x_0x23_38_0x23_25_bit0 -x_0x23_38_0x23_24_bit0 -x_0x23_38_0x23_22_bit0 -x_0x23_38_0x23_21_bit0 -x_0x23_38_0x23_19_bit0 -x_0x23_38_0x23_17_bit0 -x_0x23_38_0x23_15_bit0 -x_0x23_38_0x23_14_bit0 -x_0x23_38_0x23_12_bit0 -x_0x23_38_0x23_10_bit0 -x_0x23_38_0x23_7_bit0 -x_0x23_38_0x23_5_bit0 -x_0x23_38_0x23_4_bit0 -x_0x23_38_0x23_2_bit0 -x_0x23_37_0x23_35_bit0 -x_0x23_37_0x23_33_bit0 -x_0x23_37_0x23_31_bit0 -x_0x23_37_0x23_28_bit0 -x_0x23_37_0x23_25_bit0 -x_0x23_37_0x23_24_bit0 -x_0x23_37_0x23_22_bit0 -x_0x23_37_0x23_21_bit0 -x_0x23_37_0x23_19_bit0 -x_0x23_37_0x23_17_bit0 -x_0x23_37_0x23_15_bit0 -x_0x23_37_0x23_14_bit0 -x_0x23_37_0x23_12_bit0 -x_0x23_37_0x23_10_bit0 -x_0x23_37_0x23_7_bit0 -x_0x23_37_0x23_5_bit0 -x_0x23_37_0x23_4_bit0 -x_0x23_37_0x23_2_bit0 -x_0x23_36_0x23_35_bit0 -x_0x23_36_0x23_33_bit0 -x_0x23_36_0x23_31_bit0 -x_0x23_36_0x23_28_bit0 -x_0x23_36_0x23_25_bit0 -x_0x23_36_0x23_24_bit0 -x_0x23_36_0x23_22_bit0 -x_0x23_36_0x23_21_bit0 -x_0x23_36_0x23_19_bit0 -x_0x23_36_0x23_17_bit0 -x_0x23_36_0x23_15_bit0 -x_0x23_36_0x23_14_bit0 -x_0x23_36_0x23_12_bit0 -x_0x23_36_0x23_10_bit0 -x_0x23_36_0x23_7_bit0 -x_0x23_36_0x23_5_bit0 -x_0x23_36_0x23_4_bit0 -x_0x23_36_0x23_2_bit0 -x_0x23_35_0x23_35_bit0 -x_0x23_35_0x23_33_bit0 -x_0x23_35_0x23_31_bit0 -x_0x23_35_0x23_28_bit0 -x_0x23_35_0x23_25_bit0 -x_0x23_35_0x23_24_bit0 -x_0x23_35_0x23_22_bit0 -x_0x23_35_0x23_21_bit0 -x_0x23_35_0x23_19_bit0 x_0x23_35_0x23_17_bit0 -x_0x23_35_0x23_15_bit0 -x_0x23_35_0x23_14_bit0 -x_0x23_35_0x23_12_bit0 -x_0x23_35_0x23_10_bit0 -x_0x23_35_0x23_7_bit0 -x_0x23_35_0x23_5_bit0 -x_0x23_35_0x23_4_bit0 -x_0x23_35_0x23_2_bit0 -x_0x23_34_0x23_35_bit0 -x_0x23_34_0x23_33_bit0 -x_0x23_34_0x23_31_bit0 -x_0x23_34_0x23_28_bit0 -x_0x23_34_0x23_25_bit0 -x_0x23_34_0x23_24_bit0 -x_0x23_34_0x23_22_bit0 -x_0x23_34_0x23_21_bit0 -x_0x23_34_0x23_19_bit0 -x_0x23_34_0x23_17_bit0 -x_0x23_34_0x23_15_bit0 -x_0x23_34_0x23_14_bit0 -x_0x23_34_0x23_12_bit0 -x_0x23_34_0x23_10_bit0 -x_0x23_34_0x23_7_bit0 -x_0x23_34_0x23_5_bit0 -x_0x23_34_0x23_4_bit0 -x_0x23_34_0x23_2_bit0 -x_0x23_33_0x23_35_bit0 -x_0x23_33_0x23_33_bit0 -x_0x23_33_0x23_31_bit0 -x_0x23_33_0x23_28_bit0 -x_0x23_33_0x23_25_bit0 -x_0x23_33_0x23_24_bit0 -x_0x23_33_0x23_22_bit0 -x_0x23_33_0x23_21_bit0 -x_0x23_33_0x23_19_bit0 -x_0x23_33_0x23_17_bit0 -x_0x23_33_0x23_15_bit0 -x_0x23_33_0x23_14_bit0 -x_0x23_33_0x23_12_bit0 -x_0x23_33_0x23_10_bit0 -x_0x23_33_0x23_7_bit0 -x_0x23_33_0x23_5_bit0 -x_0x23_33_0x23_4_bit0 -x_0x23_33_0x23_2_bit0 -x_0x23_32_0x23_35_bit0 -x_0x23_32_0x23_33_bit0 -x_0x23_32_0x23_31_bit0 -x_0x23_32_0x23_28_bit0 -x_0x23_32_0x23_25_bit0 -x_0x23_32_0x23_24_bit0 -x_0x23_32_0x23_22_bit0 -x_0x23_32_0x23_21_bit0 -x_0x23_32_0x23_19_bit0 -x_0x23_32_0x23_17_bit0 -x_0x23_32_0x23_15_bit0 -x_0x23_32_0x23_14_bit0 -x_0x23_32_0x23_12_bit0 -x_0x23_32_0x23_10_bit0 -x_0x23_32_0x23_7_bit0 -x_0x23_32_0x23_5_bit0 -x_0x23_32_0x23_4_bit0 -x_0x23_32_0x23_2_bit0 -x_0x23_31_0x23_35_bit0 -x_0x23_31_0x23_33_bit0 x_0x23_31_0x23_31_bit0 -x_0x23_31_0x23_28_bit0 -x_0x23_31_0x23_25_bit0 -x_0x23_31_0x23_24_bit0 -x_0x23_31_0x23_22_bit0 -x_0x23_31_0x23_21_bit0 -x_0x23_31_0x23_19_bit0 -x_0x23_31_0x23_17_bit0 -x_0x23_31_0x23_15_bit0 -x_0x23_31_0x23_14_bit0 -x_0x23_31_0x23_12_bit0 -x_0x23_31_0x23_10_bit0 -x_0x23_31_0x23_7_bit0 -x_0x23_31_0x23_5_bit0 -x_0x23_31_0x23_4_bit0 -x_0x23_31_0x23_2_bit0 -x_0x23_30_0x23_35_bit0 -x_0x23_30_0x23_33_bit0 -x_0x23_30_0x23_31_bit0 -x_0x23_30_0x23_28_bit0 -x_0x23_30_0x23_25_bit0 -x_0x23_30_0x23_24_bit0 -x_0x23_30_0x23_22_bit0 -x_0x23_30_0x23_21_bit0 -x_0x23_30_0x23_19_bit0 -x_0x23_30_0x23_17_bit0 -x_0x23_30_0x23_15_bit0 -x_0x23_30_0x23_14_bit0 -x_0x23_30_0x23_12_bit0 -x_0x23_30_0x23_10_bit0 -x_0x23_30_0x23_7_bit0 -x_0x23_30_0x23_5_bit0 -x_0x23_30_0x23_4_bit0 -x_0x23_30_0x23_2_bit0 -x_0x23_29_0x23_35_bit0 -x_0x23_29_0x23_33_bit0 -x_0x23_29_0x23_31_bit0 -x_0x23_29_0x23_28_bit0 -x_0x23_29_0x23_25_bit0 -x_0x23_29_0x23_24_bit0 -x_0x23_29_0x23_22_bit0 -x_0x23_29_0x23_21_bit0 -x_0x23_29_0x23_19_bit0 -x_0x23_29_0x23_17_bit0 -x_0x23_29_0x23_15_bit0 -x_0x23_29_0x23_14_bit0 -x_0x23_29_0x23_12_bit0 -x_0x23_29_0x23_10_bit0 -x_0x23_29_0x23_7_bit0 -x_0x23_29_0x23_5_bit0 -x_0x23_29_0x23_4_bit0 -x_0x23_29_0x23_2_bit0 -x_0x23_28_0x23_35_bit0 -x_0x23_28_0x23_33_bit0 -x_0x23_28_0x23_31_bit0 -x_0x23_28_0x23_28_bit0 -x_0x23_28_0x23_25_bit0 -x_0x23_28_0x23_24_bit0 -x_0x23_28_0x23_22_bit0 -x_0x23_28_0x23_21_bit0 -x_0x23_28_0x23_19_bit0 -x_0x23_28_0x23_17_bit0 -x_0x23_28_0x23_15_bit0 -x_0x23_28_0x23_14_bit0 -x_0x23_28_0x23_12_bit0 -x_0x23_28_0x23_10_bit0 -x_0x23_28_0x23_7_bit0 -x_0x23_28_0x23_5_bit0 -x_0x23_28_0x23_4_bit0 -x_0x23_28_0x23_2_bit0 -x_0x23_27_0x23_35_bit0 -x_0x23_27_0x23_33_bit0 -x_0x23_27_0x23_31_bit0 -x_0x23_27_0x23_28_bit0 -x_0x23_27_0x23_25_bit0 -x_0x23_27_0x23_24_bit0 -x_0x23_27_0x23_22_bit0 -x_0x23_27_0x23_21_bit0 -x_0x23_27_0x23_19_bit0 -x_0x23_27_0x23_17_bit0 -x_0x23_27_0x23_15_bit0 -x_0x23_27_0x23_14_bit0 -x_0x23_27_0x23_12_bit0 -x_0x23_27_0x23_10_bit0 -x_0x23_27_0x23_7_bit0 -x_0x23_27_0x23_5_bit0 -x_0x23_27_0x23_4_bit0 -x_0x23_27_0x23_2_bit0 -x_0x23_26_0x23_35_bit0 -x_0x23_26_0x23_33_bit0 -x_0x23_26_0x23_31_bit0 x_0x23_26_0x23_28_bit0 -x_0x23_26_0x23_25_bit0 -x_0x23_26_0x23_24_bit0 -x_0x23_26_0x23_22_bit0 -x_0x23_26_0x23_21_bit0 -x_0x23_26_0x23_19_bit0 -x_0x23_26_0x23_17_bit0 -x_0x23_26_0x23_15_bit0 -x_0x23_26_0x23_14_bit0 -x_0x23_26_0x23_12_bit0 -x_0x23_26_0x23_10_bit0 -x_0x23_26_0x23_7_bit0 -x_0x23_26_0x23_5_bit0 -x_0x23_26_0x23_4_bit0 -x_0x23_26_0x23_2_bit0 -x_0x23_25_0x23_35_bit0 -x_0x23_25_0x23_33_bit0 -x_0x23_25_0x23_31_bit0 -x_0x23_25_0x23_28_bit0 -x_0x23_25_0x23_25_bit0 -x_0x23_25_0x23_24_bit0 -x_0x23_25_0x23_22_bit0 -x_0x23_25_0x23_21_bit0 -x_0x23_25_0x23_19_bit0 -x_0x23_25_0x23_17_bit0 -x_0x23_25_0x23_15_bit0 -x_0x23_25_0x23_14_bit0 -x_0x23_25_0x23_12_bit0 -x_0x23_25_0x23_10_bit0 -x_0x23_25_0x23_7_bit0 -x_0x23_25_0x23_5_bit0 -x_0x23_25_0x23_4_bit0 -x_0x23_25_0x23_2_bit0 -x_0x23_24_0x23_35_bit0 -x_0x23_24_0x23_33_bit0 -x_0x23_24_0x23_31_bit0 -x_0x23_24_0x23_28_bit0 -x_0x23_24_0x23_25_bit0 -x_0x23_24_0x23_24_bit0 -x_0x23_24_0x23_22_bit0 -x_0x23_24_0x23_21_bit0 -x_0x23_24_0x23_19_bit0 -x_0x23_24_0x23_17_bit0 -x_0x23_24_0x23_15_bit0 -x_0x23_24_0x23_14_bit0 -x_0x23_24_0x23_12_bit0 -x_0x23_24_0x23_10_bit0 -x_0x23_24_0x23_7_bit0 -x_0x23_24_0x23_5_bit0 -x_0x23_24_0x23_4_bit0 -x_0x23_24_0x23_2_bit0 -x_0x23_23_0x23_35_bit0 -x_0x23_23_0x23_33_bit0 -x_0x23_23_0x23_31_bit0 -x_0x23_23_0x23_28_bit0 -x_0x23_23_0x23_25_bit0 -x_0x23_23_0x23_24_bit0 -x_0x23_23_0x23_22_bit0 -x_0x23_23_0x23_21_bit0 -x_0x23_23_0x23_19_bit0 -x_0x23_23_0x23_17_bit0 -x_0x23_23_0x23_15_bit0 -x_0x23_23_0x23_14_bit0 -x_0x23_23_0x23_12_bit0 -x_0x23_23_0x23_10_bit0 -x_0x23_23_0x23_7_bit0 x_0x23_23_0x23_5_bit0 -x_0x23_23_0x23_4_bit0 -x_0x23_23_0x23_2_bit0 -x_0x23_22_0x23_35_bit0 -x_0x23_22_0x23_33_bit0 -x_0x23_22_0x23_31_bit0 -x_0x23_22_0x23_28_bit0 -x_0x23_22_0x23_25_bit0 -x_0x23_22_0x23_24_bit0 -x_0x23_22_0x23_22_bit0 -x_0x23_22_0x23_21_bit0 -x_0x23_22_0x23_19_bit0 -x_0x23_22_0x23_17_bit0 -x_0x23_22_0x23_15_bit0 -x_0x23_22_0x23_14_bit0 -x_0x23_22_0x23_12_bit0 -x_0x23_22_0x23_10_bit0 x_0x23_22_0x23_7_bit0 -x_0x23_22_0x23_5_bit0 -x_0x23_22_0x23_4_bit0 -x_0x23_22_0x23_2_bit0 -x_0x23_21_0x23_35_bit0 -x_0x23_21_0x23_33_bit0 -x_0x23_21_0x23_31_bit0 -x_0x23_21_0x23_28_bit0 -x_0x23_21_0x23_25_bit0 -x_0x23_21_0x23_24_bit0 -x_0x23_21_0x23_22_bit0 -x_0x23_21_0x23_21_bit0 x_0x23_21_0x23_19_bit0 -x_0x23_21_0x23_17_bit0 -x_0x23_21_0x23_15_bit0 -x_0x23_21_0x23_14_bit0 -x_0x23_21_0x23_12_bit0 -x_0x23_21_0x23_10_bit0 -x_0x23_21_0x23_7_bit0 -x_0x23_21_0x23_5_bit0 -x_0x23_21_0x23_4_bit0 -x_0x23_21_0x23_2_bit0 -x_0x23_20_0x23_35_bit0 -x_0x23_20_0x23_33_bit0 -x_0x23_20_0x23_31_bit0 -x_0x23_20_0x23_28_bit0 -x_0x23_20_0x23_25_bit0 -x_0x23_20_0x23_24_bit0 -x_0x23_20_0x23_22_bit0 -x_0x23_20_0x23_21_bit0 -x_0x23_20_0x23_19_bit0 -x_0x23_20_0x23_17_bit0 -x_0x23_20_0x23_15_bit0 -x_0x23_20_0x23_14_bit0 -x_0x23_20_0x23_12_bit0 -x_0x23_20_0x23_10_bit0 -x_0x23_20_0x23_7_bit0 -x_0x23_20_0x23_5_bit0 -x_0x23_20_0x23_4_bit0 -x_0x23_20_0x23_2_bit0 -x_0x23_19_0x23_35_bit0 -x_0x23_19_0x23_33_bit0 -x_0x23_19_0x23_31_bit0 -x_0x23_19_0x23_28_bit0 -x_0x23_19_0x23_25_bit0 -x_0x23_19_0x23_24_bit0 -x_0x23_19_0x23_22_bit0 -x_0x23_19_0x23_21_bit0 -x_0x23_19_0x23_19_bit0 -x_0x23_19_0x23_17_bit0 -x_0x23_19_0x23_15_bit0 -x_0x23_19_0x23_14_bit0 -x_0x23_19_0x23_12_bit0 -x_0x23_19_0x23_10_bit0 -x_0x23_19_0x23_7_bit0 -x_0x23_19_0x23_5_bit0 -x_0x23_19_0x23_4_bit0 -x_0x23_19_0x23_2_bit0 x_0x23_18_0x23_35_bit0 -x_0x23_18_0x23_33_bit0 -x_0x23_18_0x23_31_bit0 -x_0x23_18_0x23_28_bit0 -x_0x23_18_0x23_25_bit0 -x_0x23_18_0x23_24_bit0 -x_0x23_18_0x23_22_bit0 -x_0x23_18_0x23_21_bit0 -x_0x23_18_0x23_19_bit0 -x_0x23_18_0x23_17_bit0 -x_0x23_18_0x23_15_bit0 -x_0x23_18_0x23_14_bit0 -x_0x23_18_0x23_12_bit0 -x_0x23_18_0x23_10_bit0 -x_0x23_18_0x23_7_bit0 -x_0x23_18_0x23_5_bit0 -x_0x23_18_0x23_4_bit0 -x_0x23_18_0x23_2_bit0 -x_0x23_17_0x23_35_bit0 x_0x23_17_0x23_33_bit0 -x_0x23_17_0x23_31_bit0 -x_0x23_17_0x23_28_bit0 -x_0x23_17_0x23_25_bit0 -x_0x23_17_0x23_24_bit0 -x_0x23_17_0x23_22_bit0 -x_0x23_17_0x23_21_bit0 -x_0x23_17_0x23_19_bit0 -x_0x23_17_0x23_17_bit0 -x_0x23_17_0x23_15_bit0 -x_0x23_17_0x23_14_bit0 -x_0x23_17_0x23_12_bit0 -x_0x23_17_0x23_10_bit0 -x_0x23_17_0x23_7_bit0 -x_0x23_17_0x23_5_bit0 -x_0x23_17_0x23_4_bit0 -x_0x23_17_0x23_2_bit0 -x_0x23_16_0x23_35_bit0 -x_0x23_16_0x23_33_bit0 -x_0x23_16_0x23_31_bit0 -x_0x23_16_0x23_28_bit0 -x_0x23_16_0x23_25_bit0 -x_0x23_16_0x23_24_bit0 -x_0x23_16_0x23_22_bit0 -x_0x23_16_0x23_21_bit0 -x_0x23_16_0x23_19_bit0 -x_0x23_16_0x23_17_bit0 -x_0x23_16_0x23_15_bit0 -x_0x23_16_0x23_14_bit0 -x_0x23_16_0x23_12_bit0 -x_0x23_16_0x23_10_bit0 -x_0x23_16_0x23_7_bit0 -x_0x23_16_0x23_5_bit0 -x_0x23_16_0x23_4_bit0 -x_0x23_16_0x23_2_bit0 -x_0x23_15_0x23_35_bit0 -x_0x23_15_0x23_33_bit0 -x_0x23_15_0x23_31_bit0 -x_0x23_15_0x23_28_bit0 -x_0x23_15_0x23_25_bit0 -x_0x23_15_0x23_24_bit0 -x_0x23_15_0x23_22_bit0 -x_0x23_15_0x23_21_bit0 -x_0x23_15_0x23_19_bit0 -x_0x23_15_0x23_17_bit0 -x_0x23_15_0x23_15_bit0 -x_0x23_15_0x23_14_bit0 -x_0x23_15_0x23_12_bit0 -x_0x23_15_0x23_10_bit0 -x_0x23_15_0x23_7_bit0 -x_0x23_15_0x23_5_bit0 x_0x23_15_0x23_4_bit0 -x_0x23_15_0x23_2_bit0 -x_0x23_14_0x23_35_bit0 -x_0x23_14_0x23_33_bit0 -x_0x23_14_0x23_31_bit0 -x_0x23_14_0x23_28_bit0 -x_0x23_14_0x23_25_bit0 -x_0x23_14_0x23_24_bit0 -x_0x23_14_0x23_22_bit0 -x_0x23_14_0x23_21_bit0 -x_0x23_14_0x23_19_bit0 -x_0x23_14_0x23_17_bit0 -x_0x23_14_0x23_15_bit0 -x_0x23_14_0x23_14_bit0 -x_0x23_14_0x23_12_bit0 -x_0x23_14_0x23_10_bit0 -x_0x23_14_0x23_7_bit0 -x_0x23_14_0x23_5_bit0 -x_0x23_14_0x23_4_bit0 -x_0x23_14_0x23_2_bit0 -x_0x23_13_0x23_35_bit0 -x_0x23_13_0x23_33_bit0 -x_0x23_13_0x23_31_bit0 -x_0x23_13_0x23_28_bit0 -x_0x23_13_0x23_25_bit0 -x_0x23_13_0x23_24_bit0 -x_0x23_13_0x23_22_bit0 -x_0x23_13_0x23_21_bit0 -x_0x23_13_0x23_19_bit0 -x_0x23_13_0x23_17_bit0 -x_0x23_13_0x23_15_bit0 -x_0x23_13_0x23_14_bit0 -x_0x23_13_0x23_12_bit0 -x_0x23_13_0x23_10_bit0 -x_0x23_13_0x23_7_bit0 -x_0x23_13_0x23_5_bit0 -x_0x23_13_0x23_4_bit0 -x_0x23_13_0x23_2_bit0 -x_0x23_12_0x23_35_bit0 -x_0x23_12_0x23_33_bit0 -x_0x23_12_0x23_31_bit0 -x_0x23_12_0x23_28_bit0 -x_0x23_12_0x23_25_bit0 -x_0x23_12_0x23_24_bit0 -x_0x23_12_0x23_22_bit0 x_0x23_12_0x23_21_bit0 -x_0x23_12_0x23_19_bit0 -x_0x23_12_0x23_17_bit0 -x_0x23_12_0x23_15_bit0 -x_0x23_12_0x23_14_bit0 -x_0x23_12_0x23_12_bit0 -x_0x23_12_0x23_10_bit0 -x_0x23_12_0x23_7_bit0 -x_0x23_12_0x23_5_bit0 -x_0x23_12_0x23_4_bit0 -x_0x23_12_0x23_2_bit0 -x_0x23_11_0x23_35_bit0 -x_0x23_11_0x23_33_bit0 -x_0x23_11_0x23_31_bit0 -x_0x23_11_0x23_28_bit0 x_0x23_11_0x23_25_bit0 -x_0x23_11_0x23_24_bit0 -x_0x23_11_0x23_22_bit0 -x_0x23_11_0x23_21_bit0 -x_0x23_11_0x23_19_bit0 -x_0x23_11_0x23_17_bit0 -x_0x23_11_0x23_15_bit0 -x_0x23_11_0x23_14_bit0 -x_0x23_11_0x23_12_bit0 -x_0x23_11_0x23_10_bit0 -x_0x23_11_0x23_7_bit0 -x_0x23_11_0x23_5_bit0 -x_0x23_11_0x23_4_bit0 -x_0x23_11_0x23_2_bit0 -x_0x23_10_0x23_35_bit0 -x_0x23_10_0x23_33_bit0 -x_0x23_10_0x23_31_bit0 -x_0x23_10_0x23_28_bit0 -x_0x23_10_0x23_25_bit0 x_0x23_10_0x23_24_bit0 -x_0x23_10_0x23_22_bit0 -x_0x23_10_0x23_21_bit0 -x_0x23_10_0x23_19_bit0 -x_0x23_10_0x23_17_bit0 -x_0x23_10_0x23_15_bit0 -x_0x23_10_0x23_14_bit0 -x_0x23_10_0x23_12_bit0 -x_0x23_10_0x23_10_bit0 -x_0x23_10_0x23_7_bit0 -x_0x23_10_0x23_5_bit0 -x_0x23_10_0x23_4_bit0 -x_0x23_10_0x23_2_bit0 -x_0x23_9_0x23_35_bit0 -x_0x23_9_0x23_33_bit0 -x_0x23_9_0x23_31_bit0 -x_0x23_9_0x23_28_bit0 -x_0x23_9_0x23_25_bit0 -x_0x23_9_0x23_24_bit0 -x_0x23_9_0x23_22_bit0 -x_0x23_9_0x23_21_bit0 -x_0x23_9_0x23_19_bit0 -x_0x23_9_0x23_17_bit0 -x_0x23_9_0x23_15_bit0 -x_0x23_9_0x23_14_bit0 -x_0x23_9_0x23_12_bit0 -x_0x23_9_0x23_10_bit0 -x_0x23_9_0x23_7_bit0 -x_0x23_9_0x23_5_bit0 -x_0x23_9_0x23_4_bit0 x_0x23_9_0x23_2_bit0 -x_0x23_8_0x23_35_bit0 -x_0x23_8_0x23_33_bit0 -x_0x23_8_0x23_31_bit0 -x_0x23_8_0x23_28_bit0 -x_0x23_8_0x23_25_bit0 -x_0x23_8_0x23_24_bit0 -x_0x23_8_0x23_22_bit0 -x_0x23_8_0x23_21_bit0 -x_0x23_8_0x23_19_bit0 -x_0x23_8_0x23_17_bit0 -x_0x23_8_0x23_15_bit0 -x_0x23_8_0x23_14_bit0 -x_0x23_8_0x23_12_bit0 -x_0x23_8_0x23_10_bit0 -x_0x23_8_0x23_7_bit0 -x_0x23_8_0x23_5_bit0 -x_0x23_8_0x23_4_bit0 -x_0x23_8_0x23_2_bit0 -x_0x23_7_0x23_35_bit0 -x_0x23_7_0x23_33_bit0 -x_0x23_7_0x23_31_bit0 -x_0x23_7_0x23_28_bit0 -x_0x23_7_0x23_25_bit0 -x_0x23_7_0x23_24_bit0 -x_0x23_7_0x23_22_bit0 -x_0x23_7_0x23_21_bit0 -x_0x23_7_0x23_19_bit0 -x_0x23_7_0x23_17_bit0 -x_0x23_7_0x23_15_bit0 -x_0x23_7_0x23_14_bit0 -x_0x23_7_0x23_12_bit0 -x_0x23_7_0x23_10_bit0 -x_0x23_7_0x23_7_bit0 -x_0x23_7_0x23_5_bit0 -x_0x23_7_0x23_4_bit0 -x_0x23_7_0x23_2_bit0 -x_0x23_6_0x23_35_bit0 -x_0x23_6_0x23_33_bit0 -x_0x23_6_0x23_31_bit0 -x_0x23_6_0x23_28_bit0 -x_0x23_6_0x23_25_bit0 -x_0x23_6_0x23_24_bit0 -x_0x23_6_0x23_22_bit0 -x_0x23_6_0x23_21_bit0 -x#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.89 0.97 0.97 2/54 6975
Raw data (stat): 6975 (runsolver) R 6974 25347 25346 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 491201131 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0096 s]
Raw data (loadavg): 0.91 0.97 0.97 2/54 6975
Raw data (stat): 6975 (minisat+) R 6974 25347 25346 0 -1 0 5289 0 0 0 986 12 0 0 25 0 1 0 491201131 23965696 5033 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5851 5033 603 41 0 5810 0
vsize: 23404
[startup+20.0259 s]
Raw data (loadavg): 0.92 0.97 0.97 2/54 6975
Raw data (stat): 6975 (minisat+) R 6974 25347 25346 0 -1 0 5683 0 0 0 1986 14 0 0 25 0 1 0 491201131 25579520 5427 4294967295 134512640 134672761 3221224528 3221223632 134559869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6245 5427 603 41 0 6204 0
vsize: 24980
[startup+30.0264 s]
Raw data (loadavg): 0.93 0.97 0.97 2/54 6975
Raw data (stat): 6975 (minisat+) R 6974 25347 25346 0 -1 0 6013 0 0 0 2984 15 0 0 25 0 1 0 491201131 26931200 5757 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6575 5757 603 41 0 6534 0
vsize: 26300
[startup+40.0274 s]
Raw data (loadavg): 0.94 0.97 0.97 2/54 6975
Raw data (stat): 6975 (minisat+) R 6974 25347 25346 0 -1 0 6347 0 0 0 3982 17 0 0 25 0 1 0 491201131 28286976 6091 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6906 6091 603 41 0 6865 0
vsize: 27624
[startup+50.1373 s]
Raw data (loadavg): 0.95 0.97 0.97 2/54 6975
Raw data (stat): 6975 (minisat+) R 6974 25347 25346 0 -1 0 6697 0 0 0 4993 18 0 0 25 0 1 0 491201131 29757440 6441 4294967295 134512640 134672761 3221224528 3221223712 134558648 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7265 6441 603 41 0 7224 0
vsize: 29060
[startup+60.1371 s]
Raw data (loadavg): 0.96 0.97 0.97 2/54 6975
Raw data (stat): 6975 (minisat+) R 6974 25347 25346 0 -1 0 7086 0 0 0 5988 19 0 0 25 0 1 0 491201131 31371264 6830 4294967295 134512640 134672761 3221224528 3221223632 134555130 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7659 6830 603 41 0 7618 0
vsize: 30636
[startup+70.1638 s]
Raw data (loadavg): 0.96 0.97 0.97 2/54 6975
Raw data (stat): 6975 (minisat+) R 6974 25347 25346 0 -1 0 7699 0 0 0 6989 21 0 0 25 0 1 0 491201131 33943552 7443 4294967295 134512640 134672761 3221224528 3221223712 134558899 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8287 7443 603 41 0 8246 0
vsize: 33148
[startup+80.1859 s]
Raw data (loadavg): 0.97 0.97 0.97 2/54 6975
Raw data (stat): 6975 (minisat+) R 6974 25347 25346 0 -1 0 8248 0 0 0 7989 23 0 0 25 0 1 0 491201131 36102144 7992 4294967295 134512640 134672761 3221224528 3221223680 134561035 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8814 7992 603 41 0 8773 0
vsize: 35256
[startup+90.189 s]
Raw data (loadavg): 0.97 0.97 0.97 2/54 6975
Raw data (stat): 6975 (minisat+) R 6974 25347 25346 0 -1 0 8988 0 0 0 8987 25 0 0 25 0 1 0 491201131 39194624 8732 4294967295 134512640 134672761 3221224528 3221223696 134561378 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9569 8732 603 41 0 9528 0
vsize: 38276
[startup+100.189 s]
Raw data (loadavg): 0.98 0.97 0.97 2/54 6975
Raw data (stat): 6975 (minisat+) R 6974 25347 25346 0 -1 0 9515 0 0 0 9985 27 0 0 25 0 1 0 491201131 41328640 9259 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10090 9259 603 41 0 10049 0
vsize: 40360
[startup+110.19 s]
Raw data (loadavg): 0.98 0.97 0.97 2/54 6975
Raw data (stat): 6975 (minisat+) R 6974 25347 25346 0 -1 0 9911 0 0 0 10984 28 0 0 25 0 1 0 491201131 42942464 9655 4294967295 134512640 134672761 3221224528 3221223696 134560806 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10484 9655 603 41 0 10443 0
vsize: 41936
[startup+120.2 s]
Raw data (loadavg): 0.98 0.97 0.97 2/54 6975
Raw data (stat): 6975 (minisat+) R 6974 25347 25346 0 -1 0 10295 0 0 0 11983 30 0 0 25 0 1 0 491201131 44421120 10039 4294967295 134512640 134672761 3221224528 3221223528 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10845 10039 603 41 0 10804 0
vsize: 43380
[startup+130.212 s]
Raw data (loadavg): 0.98 0.97 0.97 2/54 6975
Raw data (stat): 6975 (minisat+) R 6974 25347 25346 0 -1 0 10583 0 0 0 12984 31 0 0 25 0 1 0 491201131 45621248 10327 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11138 10327 603 41 0 11097 0
vsize: 44552
[startup+140.212 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 6975
Raw data (stat): 6975 (minisat+) R 6974 25347 25346 0 -1 0 10941 0 0 0 13983 32 0 0 25 0 1 0 491201131 47218688 10685 4294967295 134512640 134672761 3221224528 3221223664 134565127 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11528 10685 603 41 0 11487 0
vsize: 46112
[startup+150.212 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 6975
Raw data (stat): 6975 (minisat+) R 6974 25347 25346 0 -1 0 11262 0 0 0 14982 33 0 0 25 0 1 0 491201131 48549888 11006 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11853 11006 603 41 0 11812 0
vsize: 47412
[startup+160.212 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 6975
Raw data (stat): 6975 (minisat+) R 6974 25347 25346 0 -1 0 11529 0 0 0 15981 34 0 0 25 0 1 0 491201131 49627136 11273 4294967295 134512640 134672761 3221224528 3221223728 134557836 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12116 11273 603 41 0 12075 0
vsize: 48464
[startup+170.211 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 6975
Raw data (stat): 6975 (minisat+) R 6974 25347 25346 0 -1 0 11784 0 0 0 16980 35 0 0 25 0 1 0 491201131 50692096 11528 4294967295 134512640 134672761 3221224528 3221223696 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12376 11528 603 41 0 12335 0
vsize: 49504
[startup+180.211 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 6975
Raw data (stat): 6975 (minisat+) R 6974 25347 25346 0 -1 0 12011 0 0 0 17979 36 0 0 25 0 1 0 491201131 51630080 11755 4294967295 134512640 134672761 3221224528 3221223696 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12605 11755 603 41 0 12564 0
vsize: 50420
[startup+190.211 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 6975
Raw data (stat): 6975 (minisat+) R 6974 25347 25346 0 -1 0 12241 0 0 0 18979 37 0 0 25 0 1 0 491201131 52568064 11985 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12834 11985 603 41 0 12793 0
vsize: 51336
[startup+200.211 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 6975
Raw data (stat): 6975 (minisat+) R 6974 25347 25346 0 -1 0 12445 0 0 0 19979 37 0 0 25 0 1 0 491201131 53403648 12189 4294967295 134512640 134672761 3221224528 3221223696 134560912 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13038 12189 603 41 0 12997 0
vsize: 52152
[startup+210.21 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 6975
Raw data (stat): 6975 (minisat+) R 6974 25347 25346 0 -1 0 12621 0 0 0 20978 38 0 0 25 0 1 0 491201131 54083584 12365 4294967295 134512640 134672761 3221224528 3221223696 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13204 12365 603 41 0 13163 0
vsize: 52816
[startup+220.21 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 6975
Raw data (stat): 6975 (minisat+) R 6974 25347 25346 0 -1 0 12823 0 0 0 21978 38 0 0 25 0 1 0 491201131 55025664 12567 4294967295 134512640 134672761 3221224528 3221223696 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13434 12567 603 41 0 13393 0
vsize: 53736
[startup+230.21 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 6975
Raw data (stat): 6975 (minisat+) R 6974 25347 25346 0 -1 0 13054 0 0 0 22977 39 0 0 25 0 1 0 491201131 55992320 12798 4294967295 134512640 134672761 3221224528 3221223696 134561406 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13670 12798 603 41 0 13629 0
vsize: 54680
[startup+240.209 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 6975
Raw data (stat): 6975 (minisat+) R 6974 25347 25346 0 -1 0 13276 0 0 0 23975 41 0 0 25 0 1 0 491201131 56786944 13020 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13864 13020 603 41 0 13823 0
vsize: 55456
[startup+250.21 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 6975
Raw data (stat): 6975 (minisat+) R 6974 25347 25346 0 -1 0 13468 0 0 0 24975 42 0 0 25 0 1 0 491201131 57589760 13212 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14060 13212 603 41 0 14019 0
vsize: 56240
[startup+260.21 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 6975
Raw data (stat): 6975 (minisat+) R 6974 25347 25346 0 -1 0 13647 0 0 0 25974 42 0 0 25 0 1 0 491201131 58294272 13391 4294967295 134512640 134672761 3221224528 3221223664 134560677 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14232 13391 603 41 0 14191 0
vsize: 56928
[startup+270.21 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 6975
Raw data (stat): 6975 (minisat+) R 6974 25347 25346 0 -1 0 13928 0 0 0 26974 43 0 0 25 0 1 0 491201131 59547648 13672 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14538 13672 603 41 0 14497 0
vsize: 58152
[startup+280.209 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 6975
Raw data (stat): 6975 (minisat+) R 6974 25347 25346 0 -1 0 14192 0 0 0 27973 44 0 0 25 0 1 0 491201131 60624896 13936 4294967295 134512640 134672761 3221224528 3221223632 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14801 13936 603 41 0 14760 0
vsize: 59204
[startup+290.209 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 6975
Raw data (stat): 6975 (minisat+) R 6974 25347 25346 0 -1 0 14272 0 0 0 28972 45 0 0 25 0 1 0 491201131 60895232 14016 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14867 14016 603 41 0 14826 0
vsize: 59468
[startup+300.209 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 6975
Raw data (stat): 6975 (minisat+) R 6974 25347 25346 0 -1 0 14272 0 0 0 29971 45 0 0 25 0 1 0 491201131 60895232 14016 4294967295 134512640 134672761 3221224528 3221223712 134559611 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14867 14016 603 41 0 14826 0
vsize: 59468
[startup+310.209 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 6975
Raw data (stat): 6975 (minisat+) R 6974 25347 25346 0 -1 0 14272 0 0 0 30971 45 0 0 25 0 1 0 491201131 60895232 14016 4294967295 134512640 134672761 3221224528 3221223632 134559925 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14867 14016 603 41 0 14826 0
vsize: 59468
[startup+320.209 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 6975
Raw data (stat): 6975 (minisat+) R 6974 25347 25346 0 -1 0 14272 0 0 0 31972 45 0 0 25 0 1 0 491201131 60895232 14016 4294967295 134512640 134672761 3221224528 3221223712 134559540 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14867 14016 603 41 0 14826 0
vsize: 59468
[startup+330.209 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 6975
Raw data (stat): 6975 (minisat+) R 6974 25347 25346 0 -1 0 14272 0 0 0 32972 45 0 0 25 0 1 0 491201131 60895232 14016 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14867 14016 603 41 0 14826 0
vsize: 59468
[startup+340.209 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 6975
Raw data (stat): 6975 (minisat+) R 6974 25347 25346 0 -1 0 14272 0 0 0 33972 45 0 0 25 0 1 0 491201131 60895232 14016 4294967295 134512640 134672761 3221224528 3221223632 134560054 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14867 14016 603 41 0 14826 0
vsize: 59468
[startup+350.209 s]
Raw data (loadavg): 0.99 0.97 0.97 3/54 6975
Raw data (stat): 6975 (minisat+) R 6974 25347 25346 0 -1 0 14272 0 0 0 34972 45 0 0 25 0 1 0 491201131 60895232 14016 4294967295 134512640 134672761 3221224528 3221223632 134559862 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14867 14016 603 41 0 14826 0
vsize: 59468
[startup+360.21 s]
Raw data (loadavg): 0.99 0.97 0.97 3/54 6975
Raw data (stat): 6975 (minisat+) R 6974 25347 25346 0 -1 0 14273 0 0 0 35972 45 0 0 25 0 1 0 491201131 60895232 14017 4294967295 134512640 134672761 3221224528 3221223632 134560031 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14867 14017 603 41 0 14826 0
vsize: 59468
[startup+370.21 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 6975
Raw data (stat): 6975 (minisat+) R 6974 25347 25346 0 -1 0 14273 0 0 0 36973 45 0 0 25 0 1 0 491201131 60895232 14017 4294967295 134512640 134672761 3221224528 3221223632 134560054 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14867 14017 603 41 0 14826 0
vsize: 59468
[startup+380.21 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 6975
Raw data (stat): 6975 (minisat+) R 6974 25347 25346 0 -1 0 14273 0 0 0 37973 45 0 0 25 0 1 0 491201131 60895232 14017 4294967295 134512640 134672761 3221224528 3221223632 134559875 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14867 14017 603 41 0 14826 0
vsize: 59468
[startup+390.209 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 6975
Raw data (stat): 6975 (minisat+) R 6974 25347 25346 0 -1 0 14273 0 0 0 38973 45 0 0 25 0 1 0 491201131 60895232 14017 4294967295 134512640 134672761 3221224528 3221223632 134559872 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14867 14017 603 41 0 14826 0
vsize: 59468
[startup+400.21 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 6975
Raw data (stat): 6975 (minisat+) R 6974 25347 25346 0 -1 0 14273 0 0 0 39973 45 0 0 25 0 1 0 491201131 60895232 14017 4294967295 134512640 134672761 3221224528 3221223632 134560169 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14867 14017 603 41 0 14826 0
vsize: 59468
[startup+410.21 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 6975
Raw data (stat): 6975 (minisat+) R 6974 25347 25346 0 -1 0 14273 0 0 0 40973 45 0 0 25 0 1 0 491201131 60895232 14017 4294967295 134512640 134672761 3221224528 3221223632 134560154 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14867 14017 603 41 0 14826 0
vsize: 59468
[startup+420.209 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 6975
Raw data (stat): 6975 (minisat+) R 6974 25347 25346 0 -1 0 14273 0 0 0 41974 45 0 0 25 0 1 0 491201131 60895232 14017 4294967295 134512640 134672761 3221224528 3221223632 134559955 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14867 14017 603 41 0 14826 0
vsize: 59468
[startup+430.21 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 6975
Raw data (stat): 6975 (minisat+) R 6974 25347 25346 0 -1 0 14273 0 0 0 42974 45 0 0 25 0 1 0 491201131 60895232 14017 4294967295 134512640 134672761 3221224528 3221223680 1074743858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14867 14017 603 41 0 14826 0
vsize: 59468
[startup+440.209 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 6975
Raw data (stat): 6975 (minisat+) R 6974 25347 25346 0 -1 0 14273 0 0 0 43974 45 0 0 25 0 1 0 491201131 60895232 14017 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14867 14017 603 41 0 14826 0
vsize: 59468
[startup+450.21 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 6975
Raw data (stat): 6975 (minisat+) R 6974 25347 25346 0 -1 0 14273 0 0 0 44974 45 0 0 25 0 1 0 491201131 60895232 14017 4294967295 134512640 134672761 3221224528 3221223712 134558662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14867 14017 603 41 0 14826 0
vsize: 59468
[startup+460.21 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 6975
Raw data (stat): 6975 (minisat+) R 6974 25347 25346 0 -1 0 14273 0 0 0 45974 45 0 0 25 0 1 0 491201131 60895232 14017 4294967295 134512640 134672761 3221224528 3221223676 134560631 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14867 14017 603 41 0 14826 0
vsize: 59468
[startup+470.209 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 6975
Raw data (stat): 6975 (minisat+) R 6974 25347 25346 0 -1 0 14273 0 0 0 46974 45 0 0 25 0 1 0 491201131 60895232 14017 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14867 14017 603 41 0 14826 0
vsize: 59468
[startup+480.209 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 6975
Raw data (stat): 6975 (minisat+) R 6974 25347 25346 0 -1 0 14273 0 0 0 47974 45 0 0 25 0 1 0 491201131 60895232 14017 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14867 14017 603 41 0 14826 0
vsize: 59468
[startup+490.209 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 6975
Raw data (stat): 6975 (minisat+) R 6974 25347 25346 0 -1 0 14273 0 0 0 48974 45 0 0 25 0 1 0 491201131 60895232 14017 4294967295 134512640 134672761 3221224528 3221223712 134558656 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14867 14017 603 41 0 14826 0
vsize: 59468
[startup+500.224 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 6975
Raw data (stat): 6975 (minisat+) R 6974 25347 25346 0 -1 0 14454 0 0 0 49976 46 0 0 25 0 1 0 491201131 61698048 14198 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15063 14198 603 41 0 15022 0
vsize: 60252
[startup+510.223 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 6975
Raw data (stat): 6975 (minisat+) R 6974 25347 25346 0 -1 0 14863 0 0 0 50973 47 0 0 25 0 1 0 491201131 63303680 14607 4294967295 134512640 134672761 3221224528 3221223696 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15455 14607 603 41 0 15414 0
vsize: 61820
[startup+520.238 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 6975
Raw data (stat): 6975 (minisat+) R 6974 25347 25346 0 -1 0 15258 0 0 0 51973 49 0 0 25 0 1 0 491201131 64917504 15002 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15849 15002 603 41 0 15808 0
vsize: 63396
[startup+530.252 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 6975
Raw data (stat): 6975 (minisat+) R 6974 25347 25346 0 -1 0 15582 0 0 0 52974 49 0 0 25 0 1 0 491201131 66260992 15326 4294967295 134512640 134672761 3221224528 3221223696 134560833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16177 15326 603 41 0 16136 0
vsize: 64708
[startup+540.265 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 6975
Raw data (stat): 6975 (minisat+) R 6974 25347 25346 0 -1 0 15867 0 0 0 53975 51 0 0 25 0 1 0 491201131 67493888 15611 4294967295 134512640 134672761 3221224528 3221223696 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16478 15611 603 41 0 16437 0
vsize: 65912
[startup+550.273 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 6975
Raw data (stat): 6975 (minisat+) R 6974 25347 25346 0 -1 0 16088 0 0 0 54975 52 0 0 25 0 1 0 491201131 68722688 15832 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16778 15832 603 41 0 16737 0
vsize: 67112
[startup+560.273 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 6975
Raw data (stat): 6975 (minisat+) R 6974 25347 25346 0 -1 0 16328 0 0 0 55975 52 0 0 25 0 1 0 491201131 69820416 16072 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17046 16072 603 41 0 17005 0
vsize: 68184
[startup+570.274 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 6975
Raw data (stat): 6975 (minisat+) R 6974 25347 25346 0 -1 0 16833 0 0 0 56973 54 0 0 25 0 1 0 491201131 71831552 16577 4294967295 134512640 134672761 3221224528 3221223712 134559498 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17537 16577 603 41 0 17496 0
vsize: 70148
[startup+580.273 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 6975
Raw data (stat): 6975 (minisat+) R 6974 25347 25346 0 -1 0 17337 0 0 0 57972 55 0 0 25 0 1 0 491201131 73826304 17081 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18024 17081 603 41 0 17983 0
vsize: 72096
[startup+590.273 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 6975
Raw data (stat): 6975 (minisat+) R 6974 25347 25346 0 -1 0 17826 0 0 0 58971 56 0 0 25 0 1 0 491201131 75825152 17570 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18512 17570 603 41 0 18471 0
vsize: 74048
[startup+600.273 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 6975
Raw data (stat): 6975 (minisat+) R 6974 25347 25346 0 -1 0 18350 0 0 0 59970 57 0 0 25 0 1 0 491201131 78090240 18094 4294967295 134512640 134672761 3221224528 3221223696 134561190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19065 18094 603 41 0 19024 0
vsize: 76260
[startup+610.274 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 6975
Raw data (stat): 6975 (minisat+) R 6974 25347 25346 0 -1 0 18821 0 0 0 60969 58 0 0 25 0 1 0 491201131 79966208 18565 4294967295 134512640 134672761 3221224528 3221223696 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19523 18565 603 41 0 19482 0
vsize: 78092
[startup+620.274 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 6975
Raw data (stat): 6975 (minisat+) R 6974 25347 25346 0 -1 0 19335 0 0 0 61968 59 0 0 25 0 1 0 491201131 82092032 19079 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20042 19079 603 41 0 20001 0
vsize: 80168
[startup+630.273 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 6975
Raw data (stat): 6975 (minisat+) R 6974 25347 25346 0 -1 0 19797 0 0 0 62968 60 0 0 25 0 1 0 491201131 83951616 19541 4294967295 134512640 134672761 3221224528 3221223632 134560318 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20496 19541 603 41 0 20455 0
vsize: 81984
[startup+640.273 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 6975
Raw data (stat): 6975 (minisat+) R 6974 25347 25346 0 -1 0 20263 0 0 0 63967 61 0 0 25 0 1 0 491201131 85811200 20007 4294967295 134512640 134672761 3221224528 3221223632 134560405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20950 20007 603 41 0 20909 0
vsize: 83800
[startup+650.273 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 6975
Raw data (stat): 6975 (minisat+) R 6974 25347 25346 0 -1 0 20694 0 0 0 64966 63 0 0 25 0 1 0 491201131 87543808 20438 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21373 20438 603 41 0 21332 0
vsize: 85492
[startup+660.273 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 6975
Raw data (stat): 6975 (minisat+) R 6974 25347 25346 0 -1 0 21111 0 0 0 65965 63 0 0 25 0 1 0 491201131 89280512 20855 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21797 20855 603 41 0 21756 0
vsize: 87188
[startup+670.273 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 6975
Raw data (stat): 6975 (minisat+) R 6974 25347 25346 0 -1 0 21514 0 0 0 66964 64 0 0 25 0 1 0 491201131 90890240 21258 4294967295 134512640 134672761 3221224528 3221223696 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22190 21258 603 41 0 22149 0
vsize: 88760
[startup+680.273 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 6975
Raw data (stat): 6975 (minisat+) R 6974 25347 25346 0 -1 0 22019 0 0 0 67964 65 0 0 25 0 1 0 491201131 93028352 21763 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22712 21763 603 41 0 22671 0
vsize: 90848
[startup+690.273 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 6975
Raw data (stat): 6975 (minisat+) R 6974 25347 25346 0 -1 0 22464 0 0 0 68963 66 0 0 25 0 1 0 491201131 94748672 22208 4294967295 134512640 134672761 3221224528 3221223632 134560184 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23132 22208 603 41 0 23091 0
vsize: 92528
[startup+700.273 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 6975
Raw data (stat): 6975 (minisat+) R 6974 25347 25346 0 -1 0 22920 0 0 0 69963 66 0 0 25 0 1 0 491201131 96612352 22664 4294967295 134512640 134672761 3221224528 3221223632 134559937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23587 22664 603 41 0 23546 0
vsize: 94348
[startup+710.273 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 6975
Raw data (stat): 6975 (minisat+) R 6974 25347 25346 0 -1 0 23329 0 0 0 70962 67 0 0 25 0 1 0 491201131 98336768 23073 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24008 23073 603 41 0 23967 0
vsize: 96032
[startup+720.272 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 6975
Raw data (stat): 6975 (minisat+) R 6974 25347 25346 0 -1 0 23745 0 0 0 71961 68 0 0 25 0 1 0 491201131 100065280 23489 4294967295 134512640 134672761 3221224528 3221223632 134560054 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24430 23489 603 41 0 24389 0
vsize: 97720
[startup+730.273 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 6975
Raw data (stat): 6975 (minisat+) R 6974 25347 25346 0 -1 0 24142 0 0 0 72960 70 0 0 25 0 1 0 491201131 101654528 23886 4294967295 134512640 134672761 3221224528 3221223632 134560057 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24818 23886 603 41 0 24777 0
vsize: 99272
[startup+740.272 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 6975
Raw data (stat): 6975 (minisat+) R 6974 25347 25346 0 -1 0 24580 0 0 0 73958 72 0 0 25 0 1 0 491201131 103514112 24324 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25272 24324 603 41 0 25231 0
vsize: 101088
[startup+750.272 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 6975
Raw data (stat): 6975 (minisat+) R 6974 25347 25346 0 -1 0 24929 0 0 0 74957 73 0 0 25 0 1 0 491201131 104853504 24673 4294967295 134512640 134672761 3221224528 3221223696 134560806 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25599 24673 603 41 0 25558 0
vsize: 102396
[startup+760.273 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 6975
Raw data (stat): 6975 (minisat+) R 6974 25347 25346 0 -1 0 25318 0 0 0 75956 74 0 0 25 0 1 0 491201131 106455040 25062 4294967295 134512640 134672761 3221224528 3221223696 134561391 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25990 25062 603 41 0 25949 0
vsize: 103960
[startup+770.272 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 6975
Raw data (stat): 6975 (minisat+) R 6974 25347 25346 0 -1 0 25712 0 0 0 76955 75 0 0 25 0 1 0 491201131 108048384 25456 4294967295 134512640 134672761 3221224528 3221223696 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26379 25456 603 41 0 26338 0
vsize: 105516
[startup+780.272 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 6975
Raw data (stat): 6975 (minisat+) R 6974 25347 25346 0 -1 0 26168 0 0 0 77954 76 0 0 25 0 1 0 491201131 109944832 25912 4294967295 134512640 134672761 3221224528 3221223696 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26842 25912 603 41 0 26801 0
vsize: 107368
[startup+790.271 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 6975
Raw data (stat): 6975 (minisat+) R 6974 25347 25346 0 -1 0 26693 0 0 0 78953 77 0 0 25 0 1 0 491201131 112091136 26437 4294967295 134512640 134672761 3221224528 3221223728 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27366 26437 603 41 0 27325 0
vsize: 109464
[startup+800.271 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 6975
Raw data (stat): 6975 (minisat+) R 6974 25347 25346 0 -1 0 27203 0 0 0 79952 78 0 0 25 0 1 0 491201131 114221056 26947 4294967295 134512640 134672761 3221224528 3221223632 134560289 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27886 26947 603 41 0 27845 0
vsize: 111544
[startup+810.27 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 6975
Raw data (stat): 6975 (minisat+) R 6974 25347 25346 0 -1 0 27718 0 0 0 80950 80 0 0 25 0 1 0 491201131 116350976 27462 4294967295 134512640 134672761 3221224528 3221223696 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28406 27462 603 41 0 28365 0
vsize: 113624
[startup+820.27 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 6975
Raw data (stat): 6975 (minisat+) R 6974 25347 25346 0 -1 0 28232 0 0 0 81949 81 0 0 25 0 1 0 491201131 118353920 27976 4294967295 134512640 134672761 3221224528 3221223728 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28895 27976 603 41 0 28854 0
vsize: 115580
[startup+830.269 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 6975
Raw data (stat): 6975 (minisat+) R 6974 25347 25346 0 -1 0 28723 0 0 0 82948 83 0 0 25 0 1 0 491201131 120356864 28467 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29384 28467 603 41 0 29343 0
vsize: 117536
[startup+840.269 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 6975
Raw data (stat): 6975 (minisat+) R 6974 25347 25346 0 -1 0 29159 0 0 0 83947 84 0 0 25 0 1 0 491201131 122232832 28903 4294967295 134512640 134672761 3221224528 3221223632 134560350 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29842 28903 603 41 0 29801 0
vsize: 119368
[startup+850.269 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 6975
Raw data (stat): 6975 (minisat+) R 6974 25347 25346 0 -1 0 29605 0 0 0 84946 85 0 0 25 0 1 0 491201131 123957248 29349 4294967295 134512640 134672761 3221224528 3221223696 134561136 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30263 29349 603 41 0 30222 0
vsize: 121052
[startup+860.269 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 6975
Raw data (stat): 6975 (minisat+) R 6974 25347 25346 0 -1 0 30062 0 0 0 85945 86 0 0 25 0 1 0 491201131 125952000 29806 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30750 29806 603 41 0 30709 0
vsize: 123000
[startup+870.269 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 6975
Raw data (stat): 6975 (minisat+) R 6974 25347 25346 0 -1 0 30519 0 0 0 86944 87 0 0 25 0 1 0 491201131 127705088 30263 4294967295 134512640 134672761 3221224528 3221223632 134559838 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31178 30263 603 41 0 31137 0
vsize: 124712
[startup+880.269 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 6975
Raw data (stat): 6975 (minisat+) R 6974 25347 25346 0 -1 0 30961 0 0 0 87943 89 0 0 25 0 1 0 491201131 129568768 30705 4294967295 134512640 134672761 3221224528 3221223728 134557836 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31633 30705 603 41 0 31592 0
vsize: 126532
[startup+890.269 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 6975
Raw data (stat): 6975 (minisat+) R 6974 25347 25346 0 -1 0 31366 0 0 0 88942 89 0 0 25 0 1 0 491201131 131170304 31110 4294967295 134512640 134672761 3221224528 3221223696 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32024 31110 603 41 0 31983 0
vsize: 128096
[startup+900.268 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 6975
Raw data (stat): 6975 (minisat+) R 6974 25347 25346 0 -1 0 31786 0 0 0 89942 90 0 0 25 0 1 0 491201131 133038080 31530 4294967295 134512640 134672761 3221224528 3221223696 134560825 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32480 31530 603 41 0 32439 0
vsize: 129920
[startup+910.269 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 6975
Raw data (stat): 6975 (minisat+) R 6974 25347 25346 0 -1 0 32205 0 0 0 90940 92 0 0 25 0 1 0 491201131 134631424 31949 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32869 31949 603 41 0 32828 0
vsize: 131476
[startup+920.269 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 6975
Raw data (stat): 6975 (minisat+) R 6974 25347 25346 0 -1 0 32618 0 0 0 91940 93 0 0 25 0 1 0 491201131 136372224 32362 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33294 32362 603 41 0 33253 0
vsize: 133176
[startup+930.268 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 6975
Raw data (stat): 6975 (minisat+) R 6974 25347 25346 0 -1 0 33027 0 0 0 92939 93 0 0 25 0 1 0 491201131 137990144 32771 4294967295 134512640 134672761 3221224528 3221223696 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33689 32771 603 41 0 33648 0
vsize: 134756
[startup+940.268 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 6975
Raw data (stat): 6975 (minisat+) R 6974 25347 25346 0 -1 0 33484 0 0 0 93938 94 0 0 25 0 1 0 491201131 139866112 33228 4294967295 134512640 134672761 3221224528 3221223632 134559838 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34147 33228 603 41 0 34106 0
vsize: 136588
[startup+950.267 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 6975
Raw data (stat): 6975 (minisat+) R 6974 25347 25346 0 -1 0 33883 0 0 0 94937 96 0 0 25 0 1 0 491201131 141590528 33627 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34568 33627 603 41 0 34527 0
vsize: 138272
[startup+960.267 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 6975
Raw data (stat): 6975 (minisat+) R 6974 25347 25346 0 -1 0 34233 0 0 0 95936 97 0 0 25 0 1 0 491201131 143048704 33977 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34924 33977 603 41 0 34883 0
vsize: 139696
[startup+970.267 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 6975
Raw data (stat): 6975 (minisat+) R 6974 25347 25346 0 -1 0 34571 0 0 0 96935 98 0 0 25 0 1 0 491201131 144379904 34315 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35249 34315 603 41 0 35208 0
vsize: 140996
[startup+980.267 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 6975
Raw data (stat): 6975 (minisat+) R 6974 25347 25346 0 -1 0 34913 0 0 0 97935 99 0 0 25 0 1 0 491201131 145833984 34657 4294967295 134512640 134672761 3221224528 3221223696 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35604 34657 603 41 0 35563 0
vsize: 142416
[startup+990.266 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 6975
Raw data (stat): 6975 (minisat+) R 6974 25347 25346 0 -1 0 35289 0 0 0 98933 100 0 0 25 0 1 0 491201131 147300352 35033 4294967295 134512640 134672761 3221224528 3221223632 134559841 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35962 35033 603 41 0 35921 0
vsize: 143848
[startup+1000.27 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 6975
Raw data (stat): 6975 (minisat+) R 6974 25347 25346 0 -1 0 35582 0 0 0 99933 101 0 0 25 0 1 0 491201131 148508672 35326 4294967295 134512640 134672761 3221224528 3221223696 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36257 35326 603 41 0 36216 0
vsize: 145028
[startup+1010.27 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 6975
Raw data (stat): 6975 (minisat+) R 6974 25347 25346 0 -1 0 35825 0 0 0 100932 101 0 0 25 0 1 0 491201131 149651456 35569 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36536 35569 603 41 0 36495 0
vsize: 146144
[startup+1020.27 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 6975
Raw data (stat): 6975 (minisat+) R 6974 25347 25346 0 -1 0 36095 0 0 0 101932 102 0 0 25 0 1 0 491201131 150728704 35839 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36799 35839 603 41 0 36758 0
vsize: 147196
[startup+1030.27 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 6975
Raw data (stat): 6975 (minisat+) R 6974 25347 25346 0 -1 0 36370 0 0 0 102931 103 0 0 25 0 1 0 491201131 151801856 36114 4294967295 134512640 134672761 3221224528 3221223696 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37061 36114 603 41 0 37020 0
vsize: 148244
[startup+1040.27 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 6975
Raw data (stat): 6975 (minisat+) R 6974 25347 25346 0 -1 0 36669 0 0 0 103931 104 0 0 25 0 1 0 491201131 153165824 36413 4294967295 134512640 134672761 3221224528 3221223632 134560224 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37394 36413 603 41 0 37353 0
vsize: 149576
[startup+1050.26 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 6975
Raw data (stat): 6975 (minisat+) R 6974 25347 25346 0 -1 0 36983 0 0 0 104930 104 0 0 25 0 1 0 491201131 154365952 36727 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37687 36727 603 41 0 37646 0
vsize: 150748
[startup+1060.26 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 6975
Raw data (stat): 6975 (minisat+) R 6974 25347 25346 0 -1 0 37194 0 0 0 105929 105 0 0 25 0 1 0 491201131 155308032 36938 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37917 36938 603 41 0 37876 0
vsize: 151668
[startup+1070.26 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 6975
Raw data (stat): 6975 (minisat+) R 6974 25347 25346 0 -1 0 37432 0 0 0 106929 105 0 0 25 0 1 0 491201131 156246016 37176 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38146 37176 603 41 0 38105 0
vsize: 152584
[startup+1080.26 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 6975
Raw data (stat): 6975 (minisat+) R 6974 25347 25346 0 -1 0 37699 0 0 0 107928 106 0 0 25 0 1 0 491201131 157315072 37443 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38407 37443 603 41 0 38366 0
vsize: 153628
[startup+1090.26 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 6975
Raw data (stat): 6975 (minisat+) R 6974 25347 25346 0 -1 0 37930 0 0 0 108928 107 0 0 25 0 1 0 491201131 158257152 37674 4294967295 134512640 134672761 3221224528 3221223696 134561198 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38637 37674 603 41 0 38596 0
vsize: 154548
[startup+1100.26 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 6975
Raw data (stat): 6975 (minisat+) R 6974 25347 25346 0 -1 0 38199 0 0 0 109927 108 0 0 25 0 1 0 491201131 159854592 37943 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39027 37943 603 41 0 38986 0
vsize: 156108
[startup+1110.26 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 6975
Raw data (stat): 6975 (minisat+) R 6974 25347 25346 0 -1 0 38590 0 0 0 110926 109 0 0 25 0 1 0 491201131 161460224 38334 4294967295 134512640 134672761 3221224528 3221223632 134560418 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39419 38334 603 41 0 39378 0
vsize: 157676
[startup+1120.26 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 6975
Raw data (stat): 6975 (minisat+) R 6974 25347 25346 0 -1 0 38928 0 0 0 111925 110 0 0 25 0 1 0 491201131 162791424 38672 4294967295 134512640 134672761 3221224528 3221223696 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39744 38672 603 41 0 39703 0
vsize: 158976
[startup+1130.26 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 6975
Raw data (stat): 6975 (minisat+) R 6974 25347 25346 0 -1 0 39315 0 0 0 112925 110 0 0 25 0 1 0 491201131 164392960 39059 4294967295 134512640 134672761 3221224528 3221223712 134559330 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40135 39059 603 41 0 40094 0
vsize: 160540
[startup+1140.26 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 6975
Raw data (stat): 6975 (minisat+) R 6974 25347 25346 0 -1 0 39659 0 0 0 113924 112 0 0 25 0 1 0 491201131 165851136 39403 4294967295 134512640 134672761 3221224528 3221223696 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40491 39403 603 41 0 40450 0
vsize: 161964
[startup+1150.26 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 6975
Raw data (stat): 6975 (minisat+) R 6974 25347 25346 0 -1 0 39941 0 0 0 114923 112 0 0 25 0 1 0 491201131 167034880 39685 4294967295 134512640 134672761 3221224528 3221223696 134560937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40780 39685 603 41 0 40739 0
vsize: 163120
[startup+1160.26 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 6975
Raw data (stat): 6975 (minisat+) R 6974 25347 25346 0 -1 0 40239 0 0 0 115923 113 0 0 25 0 1 0 491201131 168214528 39983 4294967295 134512640 134672761 3221224528 3221223696 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41068 39983 603 41 0 41027 0
vsize: 164272
[startup+1170.26 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 6975
Raw data (stat): 6975 (minisat+) R 6974 25347 25346 0 -1 0 40511 0 0 0 116922 114 0 0 25 0 1 0 491201131 169283584 40255 4294967295 134512640 134672761 3221224528 3221223696 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41329 40255 603 41 0 41288 0
vsize: 165316
[startup+1180.26 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 6975
Raw data (stat): 6975 (minisat+) R 6974 25347 25346 0 -1 0 40721 0 0 0 117921 115 0 0 25 0 1 0 491201131 170196992 40465 4294967295 134512640 134672761 3221224528 3221223632 134559875 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41552 40465 603 41 0 41511 0
vsize: 166208
[startup+1190.26 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 6975
Raw data (stat): 6975 (minisat+) R 6974 25347 25346 0 -1 0 40940 0 0 0 118921 115 0 0 25 0 1 0 491201131 171143168 40684 4294967295 134512640 134672761 3221224528 3221223696 134561025 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41783 40684 603 41 0 41742 0
vsize: 167132
[startup+1200.26 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 6975
Raw data (stat): 6975 (minisat+) R 6974 25347 25346 0 -1 0 41163 0 0 0 119920 116 0 0 25 0 1 0 491201131 171937792 40907 4294967295 134512640 134672761 3221224528 3221223728 134557836 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41977 40907 603 41 0 41936 0
vsize: 167908
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.35 s]
Raw data (loadavg): 0.99 0.97 0.97 1/54 6975
Raw data (stat): 6975 (minisat+) Z 6974 25347 25346 0 -1 12 41166 0 0 0 119921 124 0 0 25 0 1 0 491201131 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.35
CPU time (s): 1200.46
CPU user time (s): 1199.21
CPU system time (s): 1.24381
CPU usage (%): 100.009
Max. virtual memory (Kb): 167908
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####