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-13-7/MIPLIB/miplib2003/normalized-mps-v2-13-7-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	1176.86
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 15313

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc8 THE 2005-04-21 03:55:24 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=17939 boxname=wulflinc8 idbench=1380 idsolver=12 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  c5ca7819a7dcae16ff6045242cdd1f87  /oldhome/oroussel/tmp/wulflinc8/normalized-mps-v2-13-7-protfold.opb
REAL COMMAND:  minisat+ -cb -gs /oldhome/oroussel/tmp/wulflinc8/normalized-mps-v2-13-7-protfold.opb /oldhome/oroussel/tmp/wulflinc8/normalized-mps-v2-13-7-protfold.opb
IDLAUNCH: 17939
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.007
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	: 888.83

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.007
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:        602520 kB
Buffers:         34428 kB
Cached:         375136 kB
SwapCached:          0 kB
Active:         169616 kB
Inactive:       242816 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        602268 kB
SwapTotal:     2097136 kB
SwapFree:      2097136 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6948 kB
Slab:            14104 kB
Committed_AS:    63596 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 04:15:27 (client local time) WITH STATUS 10 IN 1200.24 SECONDS
stats: 17939 7 1200.24 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.86 0.95 0.91 1/54 22103
Raw data (stat): 22103 (runsolver) D 22102 26667 26666 0 -1 64 4 0 0 0 0 0 0 0 18 0 1 0 470216159 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 135158418 0 2147483391 7 90112 3225161850 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0014 s]
Raw data (loadavg): 0.88 0.96 0.91 2/54 22103
Raw data (stat): 22103 (minisat+) R 22102 26667 26666 0 -1 0 5288 0 0 0 973 14 0 0 25 0 1 0 470216159 23965696 5032 4294967295 134512640 134672761 3221224528 3221223632 134560381 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5851 5032 603 41 0 5810 0
vsize: 23404
[startup+20.0053 s]
Raw data (loadavg): 0.90 0.96 0.91 2/54 22103
Raw data (stat): 22103 (minisat+) R 22102 26667 26666 0 -1 0 5685 0 0 0 1972 15 0 0 25 0 1 0 470216159 25579520 5429 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6245 5429 603 41 0 6204 0
vsize: 24980
[startup+30.0099 s]
Raw data (loadavg): 0.91 0.96 0.91 2/54 22103
Raw data (stat): 22103 (minisat+) R 22102 26667 26666 0 -1 0 6017 0 0 0 2969 17 0 0 25 0 1 0 470216159 26931200 5761 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6575 5761 603 41 0 6534 0
vsize: 26300
[startup+40.011 s]
Raw data (loadavg): 0.93 0.96 0.91 2/54 22103
Raw data (stat): 22103 (minisat+) R 22102 26667 26666 0 -1 0 6350 0 0 0 3968 19 0 0 25 0 1 0 470216159 28286976 6094 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6906 6094 603 41 0 6865 0
vsize: 27624
[startup+50.0114 s]
Raw data (loadavg): 0.94 0.96 0.91 2/54 22103
Raw data (stat): 22103 (minisat+) R 22102 26667 26666 0 -1 0 6697 0 0 0 4966 20 0 0 25 0 1 0 470216159 29757440 6441 4294967295 134512640 134672761 3221224528 3221223696 134561167 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.0121 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 22103
Raw data (stat): 22103 (minisat+) R 22102 26667 26666 0 -1 0 7087 0 0 0 5965 21 0 0 25 0 1 0 470216159 31371264 6831 4294967295 134512640 134672761 3221224528 3221223696 134561406 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7659 6831 603 41 0 7618 0
vsize: 30636
[startup+70.0129 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 22103
Raw data (stat): 22103 (minisat+) R 22102 26667 26666 0 -1 0 7699 0 0 0 6962 24 0 0 25 0 1 0 470216159 33943552 7443 4294967295 134512640 134672761 3221224528 3221223632 134560370 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.0146 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 22103
Raw data (stat): 22103 (minisat+) R 22102 26667 26666 0 -1 0 8248 0 0 0 7960 26 0 0 25 0 1 0 470216159 36102144 7992 4294967295 134512640 134672761 3221224528 3221223696 134561151 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.0154 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 22103
Raw data (stat): 22103 (minisat+) R 22102 26667 26666 0 -1 0 8981 0 0 0 8957 28 0 0 25 0 1 0 470216159 39059456 8725 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9536 8725 603 41 0 9495 0
vsize: 38144
[startup+100.015 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 22103
Raw data (stat): 22103 (minisat+) R 22102 26667 26666 0 -1 0 9501 0 0 0 9956 30 0 0 25 0 1 0 470216159 41193472 9245 4294967295 134512640 134672761 3221224528 3221223696 134560846 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10057 9245 603 41 0 10016 0
vsize: 40228
[startup+110.017 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 22103
Raw data (stat): 22103 (minisat+) R 22102 26667 26666 0 -1 0 9896 0 0 0 10954 31 0 0 25 0 1 0 470216159 42807296 9640 4294967295 134512640 134672761 3221224528 3221223696 134560937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10451 9640 603 41 0 10410 0
vsize: 41804
[startup+120.018 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 22103
Raw data (stat): 22103 (minisat+) R 22102 26667 26666 0 -1 0 10275 0 0 0 11953 33 0 0 25 0 1 0 470216159 44421120 10019 4294967295 134512640 134672761 3221224528 3221223632 134560510 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10845 10019 603 41 0 10804 0
vsize: 43380
[startup+130.018 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 22103
Raw data (stat): 22103 (minisat+) R 22102 26667 26666 0 -1 0 10561 0 0 0 12951 34 0 0 25 0 1 0 470216159 45486080 10305 4294967295 134512640 134672761 3221224528 3221223696 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11105 10305 603 41 0 11064 0
vsize: 44420
[startup+140.019 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 22103
Raw data (stat): 22103 (minisat+) R 22102 26667 26666 0 -1 0 10911 0 0 0 13949 36 0 0 25 0 1 0 470216159 47087616 10655 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11496 10655 603 41 0 11455 0
vsize: 45984
[startup+150.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22103
Raw data (stat): 22103 (minisat+) R 22102 26667 26666 0 -1 0 11237 0 0 0 14948 38 0 0 25 0 1 0 470216159 48418816 10981 4294967295 134512640 134672761 3221224528 3221223632 134559872 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11821 10981 603 41 0 11780 0
vsize: 47284
[startup+160.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22103
Raw data (stat): 22103 (minisat+) R 22102 26667 26666 0 -1 0 11500 0 0 0 15946 39 0 0 25 0 1 0 470216159 49496064 11244 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12084 11244 603 41 0 12043 0
vsize: 48336
[startup+170.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22103
Raw data (stat): 22103 (minisat+) R 22102 26667 26666 0 -1 0 11753 0 0 0 16945 40 0 0 25 0 1 0 470216159 50561024 11497 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12344 11497 603 41 0 12303 0
vsize: 49376
[startup+180.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22103
Raw data (stat): 22103 (minisat+) R 22102 26667 26666 0 -1 0 11975 0 0 0 17943 42 0 0 25 0 1 0 470216159 51363840 11719 4294967295 134512640 134672761 3221224528 3221223696 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12540 11719 603 41 0 12499 0
vsize: 50160
[startup+190.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22103
Raw data (stat): 22103 (minisat+) R 22102 26667 26666 0 -1 0 12205 0 0 0 18941 43 0 0 25 0 1 0 470216159 52301824 11949 4294967295 134512640 134672761 3221224528 3221223712 134558687 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12769 11949 603 41 0 12728 0
vsize: 51076
[startup+200.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22103
Raw data (stat): 22103 (minisat+) R 22102 26667 26666 0 -1 0 12413 0 0 0 19940 44 0 0 25 0 1 0 470216159 53268480 12157 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13005 12157 603 41 0 12964 0
vsize: 52020
[startup+210.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22103
Raw data (stat): 22103 (minisat+) R 22102 26667 26666 0 -1 0 12581 0 0 0 20939 45 0 0 25 0 1 0 470216159 53948416 12325 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13171 12325 603 41 0 13130 0
vsize: 52684
[startup+220.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22103
Raw data (stat): 22103 (minisat+) R 22102 26667 26666 0 -1 0 12773 0 0 0 21938 46 0 0 25 0 1 0 470216159 54755328 12517 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13368 12517 603 41 0 13327 0
vsize: 53472
[startup+230.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22103
Raw data (stat): 22103 (minisat+) R 22102 26667 26666 0 -1 0 13000 0 0 0 22937 47 0 0 25 0 1 0 470216159 55693312 12744 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13597 12744 603 41 0 13556 0
vsize: 54388
[startup+240.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22103
Raw data (stat): 22103 (minisat+) R 22102 26667 26666 0 -1 0 13237 0 0 0 23936 48 0 0 25 0 1 0 470216159 56655872 12981 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13832 12981 603 41 0 13791 0
vsize: 55328
[startup+250.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22103
Raw data (stat): 22103 (minisat+) R 22102 26667 26666 0 -1 0 13412 0 0 0 24935 50 0 0 25 0 1 0 470216159 57454592 13156 4294967295 134512640 134672761 3221224528 3221223664 134560557 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14027 13156 603 41 0 13986 0
vsize: 56108
[startup+260.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22103
Raw data (stat): 22103 (minisat+) R 22102 26667 26666 0 -1 0 13595 0 0 0 25934 51 0 0 25 0 1 0 470216159 58159104 13339 4294967295 134512640 134672761 3221224528 3221223696 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14199 13339 603 41 0 14158 0
vsize: 56796
[startup+270.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22103
Raw data (stat): 22103 (minisat+) R 22102 26667 26666 0 -1 0 13826 0 0 0 26933 51 0 0 25 0 1 0 470216159 59150336 13570 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14441 13570 603 41 0 14400 0
vsize: 57764
[startup+280.031 s]
Raw data (loadavg): 1.07 0.99 0.91 2/59 22129
Raw data (stat): 22103 (minisat+) R 22102 26667 26666 0 -1 0 14168 0 0 0 27927 57 0 0 25 0 1 0 470216159 60489728 13912 4294967295 134512640 134672761 3221224528 3221223632 134560184 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14768 13912 603 41 0 14727 0
vsize: 59072
[startup+290.034 s]
Raw data (loadavg): 1.14 1.00 0.92 2/54 22156
Raw data (stat): 22103 (minisat+) R 22102 26667 26666 0 -1 0 14272 0 0 0 28924 60 0 0 25 0 1 0 470216159 60895232 14016 4294967295 134512640 134672761 3221224528 3221223728 134557836 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14867 14016 603 41 0 14826 0
vsize: 59468
[startup+300.033 s]
Raw data (loadavg): 1.11 1.00 0.92 2/54 22156
Raw data (stat): 22103 (minisat+) R 22102 26667 26666 0 -1 0 14272 0 0 0 29924 60 0 0 25 0 1 0 470216159 60895232 14016 4294967295 134512640 134672761 3221224528 3221223696 134560839 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.034 s]
Raw data (loadavg): 1.10 1.00 0.92 2/54 22156
Raw data (stat): 22103 (minisat+) R 22102 26667 26666 0 -1 0 14272 0 0 0 30924 60 0 0 25 0 1 0 470216159 60895232 14016 4294967295 134512640 134672761 3221224528 3221223728 134557828 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.035 s]
Raw data (loadavg): 1.08 1.00 0.92 2/54 22156
Raw data (stat): 22103 (minisat+) R 22102 26667 26666 0 -1 0 14272 0 0 0 31924 60 0 0 25 0 1 0 470216159 60895232 14016 4294967295 134512640 134672761 3221224528 3221223728 134557836 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.035 s]
Raw data (loadavg): 1.07 1.00 0.92 2/54 22156
Raw data (stat): 22103 (minisat+) R 22102 26667 26666 0 -1 0 14272 0 0 0 32923 61 0 0 25 0 1 0 470216159 60895232 14016 4294967295 134512640 134672761 3221224528 3221223696 134560830 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.036 s]
Raw data (loadavg): 1.06 1.00 0.92 2/54 22156
Raw data (stat): 22103 (minisat+) R 22102 26667 26666 0 -1 0 14272 0 0 0 33923 61 0 0 25 0 1 0 470216159 60895232 14016 4294967295 134512640 134672761 3221224528 3221223632 134559914 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.035 s]
Raw data (loadavg): 1.05 1.00 0.92 2/54 22158
Raw data (stat): 22103 (minisat+) R 22102 26667 26666 0 -1 0 14272 0 0 0 34923 61 0 0 25 0 1 0 470216159 60895232 14016 4294967295 134512640 134672761 3221224528 3221223632 134560025 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.036 s]
Raw data (loadavg): 1.04 1.00 0.92 2/54 22158
Raw data (stat): 22103 (minisat+) R 22102 26667 26666 0 -1 0 14273 0 0 0 35923 61 0 0 25 0 1 0 470216159 60895232 14017 4294967295 134512640 134672761 3221224528 3221223632 134559925 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.035 s]
Raw data (loadavg): 1.03 1.00 0.92 2/54 22158
Raw data (stat): 22103 (minisat+) R 22102 26667 26666 0 -1 0 14273 0 0 0 36922 62 0 0 25 0 1 0 470216159 60895232 14017 4294967295 134512640 134672761 3221224528 3221223632 134560402 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.035 s]
Raw data (loadavg): 1.03 1.00 0.92 2/54 22158
Raw data (stat): 22103 (minisat+) R 22102 26667 26666 0 -1 0 14273 0 0 0 37922 62 0 0 25 0 1 0 470216159 60895232 14017 4294967295 134512640 134672761 3221224528 3221223632 134559914 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.036 s]
Raw data (loadavg): 1.02 1.00 0.92 2/54 22158
Raw data (stat): 22103 (minisat+) R 22102 26667 26666 0 -1 0 14273 0 0 0 38922 62 0 0 25 0 1 0 470216159 60895232 14017 4294967295 134512640 134672761 3221224528 3221223696 134561201 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.036 s]
Raw data (loadavg): 1.02 1.00 0.92 2/54 22158
Raw data (stat): 22103 (minisat+) R 22102 26667 26666 0 -1 0 14273 0 0 0 39922 62 0 0 25 0 1 0 470216159 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+410.037 s]
Raw data (loadavg): 1.02 1.00 0.92 2/54 22158
Raw data (stat): 22103 (minisat+) R 22102 26667 26666 0 -1 0 14273 0 0 0 40921 63 0 0 25 0 1 0 470216159 60895232 14017 4294967295 134512640 134672761 3221224528 3221223632 134559835 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.036 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 22158
Raw data (stat): 22103 (minisat+) R 22102 26667 26666 0 -1 0 14273 0 0 0 41921 63 0 0 25 0 1 0 470216159 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+430.036 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 22158
Raw data (stat): 22103 (minisat+) R 22102 26667 26666 0 -1 0 14273 0 0 0 42920 63 0 0 25 0 1 0 470216159 60895232 14017 4294967295 134512640 134672761 3221224528 3221223632 134559979 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.036 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 22158
Raw data (stat): 22103 (minisat+) R 22102 26667 26666 0 -1 0 14273 0 0 0 43920 63 0 0 25 0 1 0 470216159 60895232 14017 4294967295 134512640 134672761 3221224528 3221223696 134560954 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.036 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 22158
Raw data (stat): 22103 (minisat+) R 22102 26667 26666 0 -1 0 14273 0 0 0 44920 64 0 0 25 0 1 0 470216159 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+460.037 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 22158
Raw data (stat): 22103 (minisat+) R 22102 26667 26666 0 -1 0 14273 0 0 0 45920 64 0 0 25 0 1 0 470216159 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+470.048 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 22158
Raw data (stat): 22103 (minisat+) R 22102 26667 26666 0 -1 0 14273 0 0 0 46920 64 0 0 24 0 1 0 470216159 60895232 14017 4294967295 134512640 134672761 3221224528 3221223920 134563586 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.047 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 22158
Raw data (stat): 22103 (minisat+) R 22102 26667 26666 0 -1 0 14273 0 0 0 47919 64 0 0 25 0 1 0 470216159 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.048 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 22158
Raw data (stat): 22103 (minisat+) R 22102 26667 26666 0 -1 0 14273 0 0 0 48919 65 0 0 25 0 1 0 470216159 60895232 14017 4294967295 134512640 134672761 3221224528 3221223696 134561218 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.048 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 22158
Raw data (stat): 22103 (minisat+) R 22102 26667 26666 0 -1 0 14330 0 0 0 49919 65 0 0 25 0 1 0 470216159 61165568 14074 4294967295 134512640 134672761 3221224528 3221223728 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14933 14074 603 41 0 14892 0
vsize: 59732
[startup+510.048 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 22158
Raw data (stat): 22103 (minisat+) R 22102 26667 26666 0 -1 0 14739 0 0 0 50918 66 0 0 25 0 1 0 470216159 62898176 14483 4294967295 134512640 134672761 3221224528 3221223728 134557830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15356 14483 603 41 0 15315 0
vsize: 61424
[startup+520.048 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 22158
Raw data (stat): 22103 (minisat+) R 22102 26667 26666 0 -1 0 15138 0 0 0 51917 67 0 0 25 0 1 0 470216159 64516096 14882 4294967295 134512640 134672761 3221224528 3221223696 134561375 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15751 14882 603 41 0 15710 0
vsize: 63004
[startup+530.048 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 22158
Raw data (stat): 22103 (minisat+) R 22102 26667 26666 0 -1 0 15486 0 0 0 52915 68 0 0 25 0 1 0 470216159 65855488 15230 4294967295 134512640 134672761 3221224528 3221223660 1075347104 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16078 15230 603 41 0 16037 0
vsize: 64312
[startup+540.049 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 22158
Raw data (stat): 22103 (minisat+) R 22102 26667 26666 0 -1 0 15786 0 0 0 53914 70 0 0 25 0 1 0 470216159 67088384 15530 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16379 15530 603 41 0 16338 0
vsize: 65516
[startup+550.048 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 22158
Raw data (stat): 22103 (minisat+) R 22102 26667 26666 0 -1 0 16029 0 0 0 54913 71 0 0 25 0 1 0 470216159 68173824 15773 4294967295 134512640 134672761 3221224528 3221223632 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16644 15773 603 41 0 16603 0
vsize: 66576
[startup+560.048 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 22158
Raw data (stat): 22103 (minisat+) R 22102 26667 26666 0 -1 0 16212 0 0 0 55912 72 0 0 25 0 1 0 470216159 69279744 15956 4294967295 134512640 134672761 3221224528 3221223712 134559569 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16914 15956 603 41 0 16873 0
vsize: 67656
[startup+570.049 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 22158
Raw data (stat): 22103 (minisat+) R 22102 26667 26666 0 -1 0 16660 0 0 0 56911 73 0 0 25 0 1 0 470216159 71155712 16404 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17372 16404 603 41 0 17331 0
vsize: 69488
[startup+580.049 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 22158
Raw data (stat): 22103 (minisat+) R 22102 26667 26666 0 -1 0 17172 0 0 0 57909 75 0 0 25 0 1 0 470216159 73158656 16916 4294967295 134512640 134672761 3221224528 3221223632 134560370 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17861 16916 603 41 0 17820 0
vsize: 71444
[startup+590.05 s]
Raw data (loadavg): 1.07 1.02 0.93 2/54 22158
Raw data (stat): 22103 (minisat+) R 22102 26667 26666 0 -1 0 17659 0 0 0 58908 76 0 0 25 0 1 0 470216159 75157504 17403 4294967295 134512640 134672761 3221224528 3221223632 134560424 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18349 17403 603 41 0 18308 0
vsize: 73396
[startup+600.051 s]
Raw data (loadavg): 1.06 1.02 0.93 2/54 22160
Raw data (stat): 22103 (minisat+) R 22102 26667 26666 0 -1 0 18180 0 0 0 59906 78 0 0 25 0 1 0 470216159 77303808 17924 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18873 17924 603 41 0 18832 0
vsize: 75492
[startup+610.051 s]
Raw data (loadavg): 1.05 1.01 0.93 2/54 22160
Raw data (stat): 22103 (minisat+) R 22102 26667 26666 0 -1 0 18651 0 0 0 60904 80 0 0 25 0 1 0 470216159 79294464 18395 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19359 18395 603 41 0 19318 0
vsize: 77436
[startup+620.051 s]
Raw data (loadavg): 1.04 1.01 0.93 2/54 22160
Raw data (stat): 22103 (minisat+) R 22102 26667 26666 0 -1 0 19151 0 0 0 61902 82 0 0 25 0 1 0 470216159 81309696 18895 4294967295 134512640 134672761 3221224528 3221223696 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19851 18895 603 41 0 19810 0
vsize: 79404
[startup+630.051 s]
Raw data (loadavg): 1.04 1.01 0.93 2/54 22160
Raw data (stat): 22103 (minisat+) R 22102 26667 26666 0 -1 0 19679 0 0 0 62901 83 0 0 25 0 1 0 470216159 83423232 19423 4294967295 134512640 134672761 3221224528 3221223696 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20367 19423 603 41 0 20326 0
vsize: 81468
[startup+640.052 s]
Raw data (loadavg): 1.03 1.01 0.93 2/54 22160
Raw data (stat): 22103 (minisat+) R 22102 26667 26666 0 -1 0 20087 0 0 0 63900 84 0 0 25 0 1 0 470216159 85147648 19831 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20788 19831 603 41 0 20747 0
vsize: 83152
[startup+650.051 s]
Raw data (loadavg): 1.02 1.01 0.93 2/54 22160
Raw data (stat): 22103 (minisat+) R 22102 26667 26666 0 -1 0 20567 0 0 0 64899 86 0 0 25 0 1 0 470216159 87007232 20311 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21242 20311 603 41 0 21201 0
vsize: 84968
[startup+660.052 s]
Raw data (loadavg): 1.02 1.01 0.93 2/54 22160
Raw data (stat): 22103 (minisat+) R 22102 26667 26666 0 -1 0 20990 0 0 0 65898 87 0 0 25 0 1 0 470216159 88743936 20734 4294967295 134512640 134672761 3221224528 3221223696 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21666 20734 603 41 0 21625 0
vsize: 86664
[startup+670.052 s]
Raw data (loadavg): 1.02 1.01 0.93 2/54 22160
Raw data (stat): 22103 (minisat+) R 22102 26667 26666 0 -1 0 21366 0 0 0 66896 88 0 0 25 0 1 0 470216159 90349568 21110 4294967295 134512640 134672761 3221224528 3221223632 134560405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22058 21110 603 41 0 22017 0
vsize: 88232
[startup+680.053 s]
Raw data (loadavg): 1.01 1.01 0.93 2/54 22160
Raw data (stat): 22103 (minisat+) R 22102 26667 26666 0 -1 0 21821 0 0 0 67895 89 0 0 25 0 1 0 470216159 92229632 21565 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22517 21565 603 41 0 22476 0
vsize: 90068
[startup+690.053 s]
Raw data (loadavg): 1.01 1.01 0.93 2/54 22160
Raw data (stat): 22103 (minisat+) R 22102 26667 26666 0 -1 0 22331 0 0 0 68894 91 0 0 25 0 1 0 470216159 94216192 22075 4294967295 134512640 134672761 3221224528 3221223632 134559872 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23002 22075 603 41 0 22961 0
vsize: 92008
[startup+700.053 s]
Raw data (loadavg): 1.01 1.01 0.93 2/54 22160
Raw data (stat): 22103 (minisat+) R 22102 26667 26666 0 -1 0 22788 0 0 0 69893 92 0 0 25 0 1 0 470216159 96092160 22532 4294967295 134512640 134672761 3221224528 3221223652 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23460 22532 603 41 0 23419 0
vsize: 93840
[startup+710.054 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 22160
Raw data (stat): 22103 (minisat+) R 22102 26667 26666 0 -1 0 23200 0 0 0 70892 93 0 0 25 0 1 0 470216159 97812480 22944 4294967295 134512640 134672761 3221224528 3221223632 134560289 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23880 22944 603 41 0 23839 0
vsize: 95520
[startup+720.156 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 22160
Raw data (stat): 22103 (minisat+) R 22102 26667 26666 0 -1 0 23614 0 0 0 71900 94 0 0 25 0 1 0 470216159 99532800 23358 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24300 23358 603 41 0 24259 0
vsize: 97200
[startup+730.155 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 22160
Raw data (stat): 22103 (minisat+) R 22102 26667 26666 0 -1 0 24015 0 0 0 72900 95 0 0 25 0 1 0 470216159 101126144 23759 4294967295 134512640 134672761 3221224528 3221223632 134560289 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24689 23759 603 41 0 24648 0
vsize: 98756
[startup+740.158 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 22160
Raw data (stat): 22103 (minisat+) R 22102 26667 26666 0 -1 0 24402 0 0 0 73899 96 0 0 25 0 1 0 470216159 102699008 24146 4294967295 134512640 134672761 3221224528 3221223696 134560845 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25073 24146 603 41 0 25032 0
vsize: 100292
[startup+750.159 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 22160
Raw data (stat): 22103 (minisat+) R 22102 26667 26666 0 -1 0 24814 0 0 0 74898 97 0 0 25 0 1 0 470216159 104452096 24558 4294967295 134512640 134672761 3221224528 3221223696 134560937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25501 24558 603 41 0 25460 0
vsize: 102004
[startup+760.163 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 22160
Raw data (stat): 22103 (minisat+) R 22102 26667 26666 0 -1 0 25169 0 0 0 75897 98 0 0 25 0 1 0 470216159 105926656 24913 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25861 24913 603 41 0 25820 0
vsize: 103444
[startup+770.163 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 22160
Raw data (stat): 22103 (minisat+) R 22102 26667 26666 0 -1 0 25554 0 0 0 76896 100 0 0 25 0 1 0 470216159 107388928 25298 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26218 25298 603 41 0 26177 0
vsize: 104872
[startup+780.163 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 22160
Raw data (stat): 22103 (minisat+) R 22102 26667 26666 0 -1 0 26027 0 0 0 77894 102 0 0 25 0 1 0 470216159 109404160 25771 4294967295 134512640 134672761 3221224528 3221223632 134555128 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26710 25771 603 41 0 26669 0
vsize: 106840
[startup+790.165 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 22160
Raw data (stat): 22103 (minisat+) R 22102 26667 26666 0 -1 0 26505 0 0 0 78893 103 0 0 25 0 1 0 470216159 111288320 26249 4294967295 134512640 134672761 3221224528 3221223692 134561235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27170 26249 603 41 0 27129 0
vsize: 108680
[startup+800.164 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 22160
Raw data (stat): 22103 (minisat+) R 22102 26667 26666 0 -1 0 27029 0 0 0 79891 105 0 0 25 0 1 0 470216159 113422336 26773 4294967295 134512640 134672761 3221224528 3221223632 134560410 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27691 26773 603 41 0 27650 0
vsize: 110764
[startup+810.165 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 22160
Raw data (stat): 22103 (minisat+) R 22102 26667 26666 0 -1 0 27529 0 0 0 80890 106 0 0 25 0 1 0 470216159 115552256 27273 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28211 27273 603 41 0 28170 0
vsize: 112844
[startup+820.165 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 22160
Raw data (stat): 22103 (minisat+) R 22102 26667 26666 0 -1 0 28034 0 0 0 81888 108 0 0 25 0 1 0 470216159 117563392 27778 4294967295 134512640 134672761 3221224528 3221223632 134560510 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28702 27778 603 41 0 28661 0
vsize: 114808
[startup+830.166 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 22160
Raw data (stat): 22103 (minisat+) R 22102 26667 26666 0 -1 0 28541 0 0 0 82886 110 0 0 25 0 1 0 470216159 119689216 28285 4294967295 134512640 134672761 3221224528 3221223696 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29221 28285 603 41 0 29180 0
vsize: 116884
[startup+840.166 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 22160
Raw data (stat): 22103 (minisat+) R 22102 26667 26666 0 -1 0 29024 0 0 0 83885 111 0 0 25 0 1 0 470216159 121692160 28768 4294967295 134512640 134672761 3221224528 3221223632 134559872 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29710 28768 603 41 0 29669 0
vsize: 118840
[startup+850.166 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 22160
Raw data (stat): 22103 (minisat+) R 22102 26667 26666 0 -1 0 29430 0 0 0 84884 112 0 0 25 0 1 0 470216159 123297792 29174 4294967295 134512640 134672761 3221224528 3221223632 134560373 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30102 29174 603 41 0 30061 0
vsize: 120408
[startup+860.166 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 22160
Raw data (stat): 22103 (minisat+) R 22102 26667 26666 0 -1 0 29893 0 0 0 85882 114 0 0 25 0 1 0 470216159 125149184 29637 4294967295 134512640 134672761 3221224528 3221223664 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30554 29637 603 41 0 30513 0
vsize: 122216
[startup+870.166 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 22160
Raw data (stat): 22103 (minisat+) R 22102 26667 26666 0 -1 0 30357 0 0 0 86880 116 0 0 25 0 1 0 470216159 127156224 30101 4294967295 134512640 134672761 3221224528 3221223696 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31044 30101 603 41 0 31003 0
vsize: 124176
[startup+880.167 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 22160
Raw data (stat): 22103 (minisat+) R 22102 26667 26666 0 -1 0 30816 0 0 0 87879 117 0 0 25 0 1 0 470216159 129028096 30560 4294967295 134512640 134672761 3221224528 3221223696 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31501 30560 603 41 0 31460 0
vsize: 126004
[startup+890.167 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 22160
Raw data (stat): 22103 (minisat+) R 22102 26667 26666 0 -1 0 31214 0 0 0 88878 119 0 0 25 0 1 0 470216159 130637824 30958 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31894 30958 603 41 0 31853 0
vsize: 127576
[startup+900.167 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 22160
Raw data (stat): 22103 (minisat+) R 22102 26667 26666 0 -1 0 31635 0 0 0 89876 120 0 0 25 0 1 0 470216159 132370432 31379 4294967295 134512640 134672761 3221224528 3221223696 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32317 31379 603 41 0 32276 0
vsize: 129268
[startup+910.168 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 22160
Raw data (stat): 22103 (minisat+) R 22102 26667 26666 0 -1 0 32048 0 0 0 90874 122 0 0 25 0 1 0 470216159 134103040 31792 4294967295 134512640 134672761 3221224528 3221223632 134560291 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32740 31792 603 41 0 32699 0
vsize: 130960
[startup+920.169 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 22160
Raw data (stat): 22103 (minisat+) R 22102 26667 26666 0 -1 0 32459 0 0 0 91874 122 0 0 25 0 1 0 470216159 135696384 32203 4294967295 134512640 134672761 3221224528 3221223712 134558761 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33129 32203 603 41 0 33088 0
vsize: 132516
[startup+930.176 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 22160
Raw data (stat): 22103 (minisat+) R 22102 26667 26666 0 -1 0 32881 0 0 0 92873 124 0 0 25 0 1 0 470216159 137453568 32625 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33558 32625 603 41 0 33517 0
vsize: 134232
[startup+940.179 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 22160
Raw data (stat): 22103 (minisat+) R 22102 26667 26666 0 -1 0 33305 0 0 0 93872 125 0 0 25 0 1 0 470216159 139190272 33049 4294967295 134512640 134672761 3221224528 3221223696 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33982 33049 603 41 0 33941 0
vsize: 135928
[startup+950.195 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 22160
Raw data (stat): 22103 (minisat+) R 22102 26667 26666 0 -1 0 33745 0 0 0 94872 127 0 0 25 0 1 0 470216159 140931072 33489 4294967295 134512640 134672761 3221224528 3221223696 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34407 33489 603 41 0 34366 0
vsize: 137628
[startup+960.216 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 22160
Raw data (stat): 22103 (minisat+) R 22102 26667 26666 0 -1 0 34123 0 0 0 95873 128 0 0 25 0 1 0 470216159 142503936 33867 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34791 33867 603 41 0 34750 0
vsize: 139164
[startup+970.223 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 22160
Raw data (stat): 22103 (minisat+) R 22102 26667 26666 0 -1 0 34433 0 0 0 96873 128 0 0 25 0 1 0 470216159 143839232 34177 4294967295 134512640 134672761 3221224528 3221223696 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35117 34177 603 41 0 35076 0
vsize: 140468
[startup+980.224 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 22160
Raw data (stat): 22103 (minisat+) R 22102 26667 26666 0 -1 0 34785 0 0 0 97872 130 0 0 25 0 1 0 470216159 145309696 34529 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35476 34529 603 41 0 35435 0
vsize: 141904
[startup+990.227 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 22160
Raw data (stat): 22103 (minisat+) R 22102 26667 26666 0 -1 0 35136 0 0 0 98871 131 0 0 25 0 1 0 470216159 146759680 34880 4294967295 134512640 134672761 3221224528 3221223632 134555116 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35830 34880 603 41 0 35789 0
vsize: 143320
[startup+1000.39 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 22160
Raw data (stat): 22103 (minisat+) R 22102 26667 26666 0 -1 0 35482 0 0 0 99887 132 0 0 25 0 1 0 470216159 148094976 35226 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36156 35226 603 41 0 36115 0
vsize: 144624
[startup+1010.4 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 22160
Raw data (stat): 22103 (minisat+) R 22102 26667 26666 0 -1 0 35739 0 0 0 100886 134 0 0 25 0 1 0 470216159 149184512 35483 4294967295 134512640 134672761 3221224528 3221223632 134560218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36422 35483 603 41 0 36381 0
vsize: 145688
[startup+1020.4 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 22160
Raw data (stat): 22103 (minisat+) R 22102 26667 26666 0 -1 0 35989 0 0 0 101886 134 0 0 25 0 1 0 470216159 150327296 35733 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36701 35733 603 41 0 36660 0
vsize: 146804
[startup+1030.4 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 22160
Raw data (stat): 22103 (minisat+) R 22102 26667 26666 0 -1 0 36270 0 0 0 102885 136 0 0 25 0 1 0 470216159 151396352 36014 4294967295 134512640 134672761 3221224528 3221223632 134560226 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36962 36014 603 41 0 36921 0
vsize: 147848
[startup+1040.4 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 22160
Raw data (stat): 22103 (minisat+) R 22102 26667 26666 0 -1 0 36566 0 0 0 103883 137 0 0 25 0 1 0 470216159 152600576 36310 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37256 36310 603 41 0 37215 0
vsize: 149024
[startup+1050.4 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 22160
Raw data (stat): 22103 (minisat+) R 22102 26667 26666 0 -1 0 36842 0 0 0 104883 138 0 0 25 0 1 0 470216159 153825280 36586 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37555 36586 603 41 0 37514 0
vsize: 150220
[startup+1060.41 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 22160
Raw data (stat): 22103 (minisat+) R 22102 26667 26666 0 -1 0 37118 0 0 0 105873 139 0 0 25 0 1 0 470216159 154906624 36862 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37819 36862 603 41 0 37778 0
vsize: 151276
[startup+1070.42 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 22160
Raw data (stat): 22103 (minisat+) R 22102 26667 26666 0 -1 0 37327 0 0 0 106873 140 0 0 25 0 1 0 470216159 155844608 37071 4294967295 134512640 134672761 3221224528 3221223696 134561372 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38048 37071 603 41 0 38007 0
vsize: 152192
[startup+1080.42 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 22160
Raw data (stat): 22103 (minisat+) R 22102 26667 26666 0 -1 0 37602 0 0 0 107873 141 0 0 25 0 1 0 470216159 156913664 37346 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38309 37346 603 41 0 38268 0
vsize: 153236
[startup+1090.42 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 22160
Raw data (stat): 22103 (minisat+) R 22102 26667 26666 0 -1 0 37840 0 0 0 108871 142 0 0 25 0 1 0 470216159 157851648 37584 4294967295 134512640 134672761 3221224528 3221223696 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38538 37584 603 41 0 38497 0
vsize: 154152
[startup+1100.42 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 22160
Raw data (stat): 22103 (minisat+) R 22102 26667 26666 0 -1 0 38101 0 0 0 109870 143 0 0 25 0 1 0 470216159 159453184 37845 4294967295 134512640 134672761 3221224528 3221223696 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38929 37845 603 41 0 38888 0
vsize: 155716
[startup+1110.42 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 22160
Raw data (stat): 22103 (minisat+) R 22102 26667 26666 0 -1 0 38426 0 0 0 110870 144 0 0 25 0 1 0 470216159 160796672 38170 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39257 38170 603 41 0 39216 0
vsize: 157028
[startup+1120.42 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 22160
Raw data (stat): 22103 (minisat+) R 22102 26667 26666 0 -1 0 38794 0 0 0 111869 145 0 0 25 0 1 0 470216159 162254848 38538 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39613 38538 603 41 0 39572 0
vsize: 158452
[startup+1130.42 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 22160
Raw data (stat): 22103 (minisat+) R 22102 26667 26666 0 -1 0 39142 0 0 0 112868 146 0 0 25 0 1 0 470216159 163725312 38886 4294967295 134512640 134672761 3221224528 3221223664 134560688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39972 38886 603 41 0 39931 0
vsize: 159888
[startup+1140.43 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 22160
Raw data (stat): 22103 (minisat+) R 22102 26667 26666 0 -1 0 39532 0 0 0 113867 147 0 0 25 0 1 0 470216159 165326848 39276 4294967295 134512640 134672761 3221224528 3221223632 134560318 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40363 39276 603 41 0 40322 0
vsize: 161452
[startup+1150.43 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 22160
Raw data (stat): 22103 (minisat+) R 22102 26667 26666 0 -1 0 39829 0 0 0 114866 148 0 0 25 0 1 0 470216159 166510592 39573 4294967295 134512640 134672761 3221224528 3221223696 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40652 39573 603 41 0 40611 0
vsize: 162608
[startup+1160.43 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 22160
Raw data (stat): 22103 (minisat+) R 22102 26667 26666 0 -1 0 40128 0 0 0 115865 150 0 0 25 0 1 0 470216159 167694336 39872 4294967295 134512640 134672761 3221224528 3221223728 134557830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40941 39872 603 41 0 40900 0
vsize: 163764
[startup+1170.43 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 22160
Raw data (stat): 22103 (minisat+) R 22102 26667 26666 0 -1 0 40401 0 0 0 116865 150 0 0 25 0 1 0 470216159 168886272 40145 4294967295 134512640 134672761 3221224528 3221223664 134560688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41232 40145 603 41 0 41191 0
vsize: 164928
[startup+1180.43 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 22160
Raw data (stat): 22103 (minisat+) R 22102 26667 26666 0 -1 0 40616 0 0 0 117864 151 0 0 25 0 1 0 470216159 169676800 40360 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41425 40360 603 41 0 41384 0
vsize: 165700
[startup+1190.43 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 22160
Raw data (stat): 22103 (minisat+) R 22102 26667 26666 0 -1 0 40823 0 0 0 118864 151 0 0 25 0 1 0 470216159 170614784 40567 4294967295 134512640 134672761 3221224528 3221223632 134559949 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41654 40567 603 41 0 41613 0
vsize: 166616
[startup+1200.43 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 22160
Raw data (stat): 22103 (minisat+) R 22102 26667 26666 0 -1 0 41059 0 0 0 119863 152 0 0 25 0 1 0 470216159 171544576 40803 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41881 40803 603 41 0 41840 0
vsize: 167524
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.52 s]
Raw data (loadavg): 1.00 1.00 0.93 1/54 22160
Raw data (stat): 22103 (minisat+) Z 22102 26667 26666 0 -1 12 41062 0 0 0 119864 160 0 0 25 0 1 0 470216159 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 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.52
CPU time (s): 1200.24
CPU user time (s): 1198.64
CPU system time (s): 1.60076
CPU usage (%): 99.9768
Max. virtual memory (Kb): 167524
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####