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 18472

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc31 THE 2005-04-21 15:13:45 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=17937 boxname=wulflinc31 idbench=1380 idsolver=10 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  c5ca7819a7dcae16ff6045242cdd1f87  /oldhome/oroussel/tmp/wulflinc31/normalized-mps-v2-13-7-protfold.opb
REAL COMMAND:  minisat+ -ca /oldhome/oroussel/tmp/wulflinc31/normalized-mps-v2-13-7-protfold.opb /oldhome/oroussel/tmp/wulflinc31/normalized-mps-v2-13-7-protfold.opb
IDLAUNCH: 17937
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.153
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	: 3
cpu MHz		: 451.153
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	: 901.12

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        414784 kB
Buffers:         34372 kB
Cached:         556960 kB
SwapCached:        540 kB
Active:         140876 kB
Inactive:       452464 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        414532 kB
SwapTotal:     2097892 kB
SwapFree:      2096468 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5100 kB
Slab:            20776 kB
Committed_AS:    63488 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 15:33:48 (client local time) WITH STATUS 10 IN 1200.24 SECONDS
stats: 17937 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]---> Adder-cost: 64   maxlim: 32   bits: 6/6
c ---[1907]---> Adder-cost: 64   maxlim: 32   bits: 6/6
c ---[1906]---> Adder-cost: 64   maxlim: 32   bits: 6/6
c ---[1905]---> Adder-cost: 64   maxlim: 32   bits: 6/6
c ---[1904]---> Adder-cost: 64   maxlim: 32   bits: 6/6
c ---[1903]---> Adder-cost: 64   maxlim: 32   bits: 6/6
c ---[1902]---> Adder-cost: 64   maxlim: 32   bits: 6/6
c ---[1901]---> Adder-cost: 64   maxlim: 32   bits: 6/6
c ---[1900]---> Adder-cost: 64   maxlim: 32   bits: 6/6
c ---[1899]---> Adder-cost: 64   maxlim: 32   bits: 6/6
c ---[1898]---> Adder-cost: 64   maxlim: 32   bits: 6/6
c ---[1897]---> Adder-cost: 64   maxlim: 32   bits: 6/6
c ---[1896]---> Adder-cost: 64   maxlim: 32   bits: 6/6
c ---[1895]---> Adder-cost: 64   maxlim: 32   bits: 6/6
c ---[1894]---> Adder-cost: 64   maxlim: 32   bits: 6/6
c ---[1893]---> Adder-cost: 64   maxlim: 32   bits: 6/6
c ---[1892]---> Adder-cost: 64   maxlim: 32   bits: 6/6
c ---[1891]---> Adder-cost: 64   maxlim: 32   bits: 6/6
c ---[1890]---> Adder-cost: 64   maxlim: 32   bits: 6/6
c ---[1889]---> Adder-cost: 64   maxlim: 32   bits: 6/6
c ---[1888]---> Adder-cost: 64   maxlim: 32   bits: 6/6
c ---[1887]---> Adder-cost: 64   maxlim: 32   bits: 6/6
c ---[1886]---> Adder-cost: 64   maxlim: 32   bits: 6/6
c ---[1885]---> Adder-cost: 64   maxlim: 32   bits: 6/6
c ---[1884]---> Adder-cost: 64   maxlim: 32   bits: 6/6
c ---[1883]---> Adder-cost: 64   maxlim: 32   bits: 6/6
c ---[1882]---> Adder-cost: 64   maxlim: 32   bits: 6/6
c ---[1881]---> Adder-cost: 64   maxlim: 32   bits: 6/6
c ---[1880]---> Adder-cost: 50   maxlim: 32   bits: 6/6
c ---[1879]---> Adder-cost: 50   maxlim: 32   bits: 6/6
c ---[1878]---> Adder-cost: 50   maxlim: 32   bits: 6/6
c ---[1877]---> Adder-cost: 50   maxlim: 32   bits: 6/6
c ---[1876]---> Adder-cost: 64   maxlim: 32   bits: 6/6
c ---[1875]---> Adder-cost: 50   maxlim: 32   bits: 6/6
c ---[1874]---> Adder-cost: 50   maxlim: 32   bits: 6/6
c ---[1873]---> Adder-cost: 36   maxlim: 32   bits: 6/6
c ---[1872]---> Adder-cost: 36   maxlim: 32   bits: 6/6
c ---[1871]---> Adder-cost: 36   maxlim: 32   bits: 6/6
c ---[1870]---> Adder-cost: 36   maxlim: 32   bits: 6/6
c ---[1869]---> Adder-cost: 36   maxlim: 32   bits: 6/6
c ---[1868]---> Adder-cost: 36   maxlim: 32   bits: 6/6
c ---[1867]---> Adder-cost: 36   maxlim: 32   bits: 6/6
c ---[1866]---> Adder-cost: 36   maxlim: 32   bits: 6/6
c ---[1865]---> Adder-cost: 64   maxlim: 32   bits: 6/6
c ---[1864]---> Adder-cost: 36   maxlim: 32   bits: 6/6
c ---[1863]---> Adder-cost: 36   maxlim: 32   bits: 6/6
c ---[1862]---> Adder-cost: 36   maxlim: 32   bits: 6/6
c ---[1861]---> Adder-cost: 36   maxlim: 32   bits: 6/6
c ---[1860]---> Adder-cost: 36   maxlim: 32   bits: 6/6
c ---[1859]---> Adder-cost: 36   maxlim: 32   bits: 6/6
c ---[1858]---> Adder-cost: 36   maxlim: 32   bits: 6/6
c ---[1857]---> Adder-cost: 50   maxlim: 32   bits: 6/6
c ---[1856]---> Adder-cost: 50   maxlim: 32   bits: 6/6
c ---[1855]---> Adder-cost: 50   maxlim: 32   bits: 6/6
c ---[1854]---> Adder-cost: 64   maxlim: 32   bits: 6/6
c ---[1853]---> Adder-cost: 50   maxlim: 32   bits: 6/6
c ---[1852]---> Adder-cost: 50   maxlim: 32   bits: 6/6
c ---[1851]---> Adder-cost: 50   maxlim: 32   bits: 6/6
c ---[1850]---> Adder-cost: 50   maxlim: 32   bits: 6/6
c ---[1849]---> Adder-cost: 50   maxlim: 32   bits: 6/6
c ---[1848]---> Adder-cost: 50   maxlim: 32   bits: 6/6
c ---[1847]---> Adder-cost: 50   maxlim: 32   bits: 6/6
c ---[1846]---> Adder-cost: 50   maxlim: 32   bits: 6/6
c ---[1845]---> Adder-cost: 50   maxlim: 32   bits: 6/6
c ---[1844]---> Adder-cost: 50   maxlim: 32   bits: 6/6
c ---[1843]---> Adder-cost: 50   maxlim: 32   bits: 6/6
c ---[1842]---> Adder-cost: 64   maxlim: 32   bits: 6/6
c ---[1841]---> Adder-cost: 50   maxlim: 32   bits: 6/6
c ---[1840]---> Adder-cost: 50   maxlim: 32   bits: 6/6
c ---[1839]---> Adder-cost: 36   maxlim: 32   bits: 6/6
c ---[1838]---> Adder-cost: 36   maxlim: 32   bits: 6/6
c ---[1837]---> Adder-cost: 36   maxlim: 32   bits: 6/6
c ---[1836]---> Adder-cost: 50   maxlim: 32   bits: 6/6
c ---[1835]---> Adder-cost: 50   maxlim: 32   bits: 6/6
c ---[1834]---> Adder-cost: 36   maxlim: 32   bits: 6/6
c ---[1833]---> Adder-cost: 36   maxlim: 32   bits: 6/6
c ---[1832]---> Adder-cost: 50   maxlim: 32   bits: 6/6
c ---[1831]---> Adder-cost: 36   maxlim: 32   bits: 6/6
c ---[1830]---> Adder-cost: 36   maxlim: 32   bits: 6/6
c ---[1829]---> Adder-cost: 36   maxlim: 32   bits: 6/6
c ---[1828]---> Adder-cost: 50   maxlim: 32   bits: 6/6
c ---[1827]---> Adder-cost: 50   maxlim: 32   bits: 6/6
c ---[1826]---> Adder-cost: 36   maxlim: 32   bits: 6/6
c ---[1825]---> Adder-cost: 36   maxlim: 32   bits: 6/6
c ---[1824]---> Adder-cost: 36   maxlim: 32   bits: 6/6
c ---[1823]---> Adder-cost: 36   maxlim: 32   bits: 6/6
c ---[1822]---> Adder-cost: 36   maxlim: 32   bits: 6/6
c ---[1821]---> Adder-cost: 36   maxlim: 32   bits: 6/6
c ---[1820]---> Adder-cost: 50   maxlim: 32   bits: 6/6
c ---[1819]---> Adder-cost: 50   maxlim: 32   bits: 6/6
c ---[1818]---> Adder-cost: 36   maxlim: 32   bits: 6/6
c ---[1817]---> Adder-cost: 36   maxlim: 32   bits: 6/6
c ---[1816]---> Adder-cost: 36   maxlim: 32   bits: 6/6
c ---[1815]---> Adder-cost: 36   maxlim: 32   bits: 6/6
c ---[1814]---> Adder-cost: 36   maxlim: 32   bits: 6/6
c ---[1813]---> Adder-cost: 50   maxlim: 32   bits: 6/6
c ---[1812]---> Adder-cost: 50   maxlim: 32   bits: 6/6
c ---[1811]---> Adder-cost: 36   maxlim: 32   bits: 6/6
c ---[1810]---> Adder-cost: 36   maxlim: 32   bits: 6/6
c ---[1809]---> Adder-cost: 36   maxlim: 32   bits: 6/6
c ---[1808]---> Adder-cost: 36   maxlim: 32   bits: 6/6
c ---[1807]---> Adder-cost: 36   maxlim: 32   bits: 6/6
c ---[1806]---> Adder-cost: 36   maxlim: 32   bits: 6/6
c ---[1805]---> Adder-cost: 50   maxlim: 32   bits: 6/6
c ---[1804]---> Adder-cost: 36   maxlim: 32   bits: 6/6
c ---[1803]---> Adder-cost: 36   maxlim: 32   bits: 6/6
c ---[1802]---> Adder-cost: 36   maxlim: 32   bits: 6/6
c ---[1801]---> Adder-cost: 36   maxlim: 32   bits: 6/6
c ---[1800]---> Adder-cost: 36   maxlim: 32   bits: 6/6
c ---[1799]---> Adder-cost: 36   maxlim: 32   bits: 6/6
c ---[1798]---> Adder-cost: 36   maxlim: 32   bits: 6/6
c ---[1797]---> Adder-cost: 36   maxlim: 32   bits: 6/6
c ---[1796]---> Adder-cost: 36   maxlim: 32   bits: 6/6
c ---[1795]---> Adder-cost: 36   maxlim: 32   bits: 6/6
c ---[1794]---> Adder-cost: 36   maxlim: 32   bits: 6/6
c ---[1793]---> Adder-cost: 36   maxlim: 32   bits: 6/6
c ---[1792]---> Adder-cost: 36   maxlim: 32   bits: 6/6
c ---[1791]---> Adder-cost: 36   maxlim: 32   bits: 6/6
c ---[1790]---> Adder-cost: 36   maxlim: 32   bits: 6/6
c ---[1789]---> Adder-cost: 36   maxlim: 32   bits: 6/6
c ---[1787]---> Adder-cost: 1286   maxlim: 816   bits: 10/10
c ---[1785]---> Adder-cost: 1752   maxlim: 864   bits: 10/10
c ---[1783]---> Adder-cost: 92   maxlim: 48   bits: 6/6
c ---[1781]---> Adder-cost: 92   maxlim: 48   bits: 6/6
c ---[1779]---> Adder-cost: 92   maxlim: 48   bits: 6/6
c ---[1777]---> Adder-cost: 92   maxlim: 48   bits: 6/6
c ---[1775]---> Adder-cost: 92   maxlim: 48   bits: 6/6
c ---[1773]---> Adder-cost: 92   maxlim: 48   bits: 6/6
c ---[1771]---> Adder-cost: 92   maxlim: 48   bits: 6/6
c ---[1769]---> Adder-cost: 92   maxlim: 48   bits: 6/6
c ---[1767]---> Adder-cost: 92   maxlim: 48   bits: 6/6
c ---[1765]---> Adder-cost: 92   maxlim: 48   bits: 6/6
c ---[1763]---> Adder-cost: 92   maxlim: 48   bits: 6/6
c ---[1761]---> Adder-cost: 92   maxlim: 48   bits: 6/6
c ---[1759]---> Adder-cost: 92   maxlim: 48   bits: 6/6
c ---[1757]---> Adder-cost: 92   maxlim: 48   bits: 6/6
c ---[1755]---> Adder-cost: 92   maxlim: 48   bits: 6/6
c ---[1753]---> Adder-cost: 92   maxlim: 48   bits: 6/6
c ---[1751]---> Adder-cost: 92   maxlim: 48   bits: 6/6
c ---[1749]---> Adder-cost: 92   maxlim: 48   bits: 6/6
c ---[1747]---> Adder-cost: 92   maxlim: 48   bits: 6/6
c ---[1745]---> Adder-cost: 92   maxlim: 48   bits: 6/6
c ---[1743]---> Adder-cost: 92   maxlim: 48   bits: 6/6
c ---[1741]---> Adder-cost: 92   maxlim: 48   bits: 6/6
c ---[1739]---> Adder-cost: 92   maxlim: 48   bits: 6/6
c ---[1737]---> Adder-cost: 92   maxlim: 48   bits: 6/6
c ---[1735]---> Adder-cost: 92   maxlim: 48   bits: 6/6
c ---[1733]---> Adder-cost: 92   maxlim: 48   bits: 6/6
c ---[1731]---> Adder-cost: 92   maxlim: 48   bits: 6/6
c ---[1729]---> Adder-cost: 92   maxlim: 48   bits: 6/6
c ---[1727]---> Adder-cost: 92   maxlim: 48   bits: 6/6
c ---[1725]---> Adder-cost: 92   maxlim: 48   bits: 6/6
c ---[1723]---> Adder-cost: 92   maxlim: 48   bits: 6/6
c ---[1721]---> Adder-cost: 92   maxlim: 48   bits: 6/6
c ---[1719]---> Adder-cost: 92   maxlim: 48   bits: 6/6
c ---[1717]---> Adder-cost: 92   maxlim: 48   bits: 6/6
c ---[1715]---> Adder-cost: 92   maxlim: 48   bits: 6/6
c ---[1714]---> Adder-cost: 50   maxlim: 33   bits: 6/6
c ---[1713]---> Adder-cost: 50   maxlim: 33   bits: 6/6
c ---[1712]---> Adder-cost: 50   maxlim: 33   bits: 6/6
c ---[1711]---> Adder-cost: 50   maxlim: 33   bits: 6/6
c ---[1710]---> Adder-cost: 50   maxlim: 33   bits: 6/6
c ---[1709]---> Adder-cost: 50   maxlim: 33   bits: 6/6
c ---[1708]---> Adder-cost: 50   maxlim: 33   bits: 6/6
c ---[1707]---> Adder-cost: 50   maxlim: 33   bits: 6/6
c ---[1706]---> Adder-cost: 50   maxlim: 33   bits: 6/6
c ---[1705]---> Adder-cost: 50   maxlim: 33   bits: 6/6
c ---[1704]---> Adder-cost: 50   maxlim: 33   bits: 6/6
c ---[1703]---> Adder-cost: 50   maxlim: 33   bits: 6/6
c ---[1702]---> Adder-cost: 50   maxlim: 33   bits: 6/6
c ---[1701]---> Adder-cost: 50   maxlim: 33   bits: 6/6
c ---[1700]---> Adder-cost: 50   maxlim: 33   bits: 6/6
c ---[1699]---> Adder-cost: 50   maxlim: 33   bits: 6/6
c ---[1698]---> Adder-cost: 50   maxlim: 33   bits: 6/6
c ---[1697]---> Adder-cost: 50   maxlim: 33   bits: 6/6
c ---[1696]---> Adder-cost: 50   maxlim: 33   bits: 6/6
c ---[1695]---> Adder-cost: 50   maxlim: 33   bits: 6/6
c ---[1694]---> Adder-cost: 50   maxlim: 33   bits: 6/6
c ---[1693]---> Adder-cost: 50   maxlim: 33   bits: 6/6
c ---[1692]---> Adder-cost: 50   maxlim: 33   bits: 6/6
c ---[1691]---> Adder-cost: 50   maxlim: 33   bits: 6/6
c ---[1690]---> Adder-cost: 50   maxlim: 33   bits: 6/6
c ---[1689]---> Adder-cost: 50   maxlim: 33   bits: 6/6
c ---[1688]---> Adder-cost: 50   maxlim: 33   bits: 6/6
c ---[1687]---> Adder-cost: 50   maxlim: 33   bits: 6/6
c ---[1686]---> Adder-cost: 50   maxlim: 33   bits: 6/6
c ---[1685]---> Adder-cost: 50   maxlim: 33   bits: 6/6
c ---[1684]---> Adder-cost: 50   maxlim: 33   bits: 6/6
c ---[1683]---> Adder-cost: 50   maxlim: 33   bits: 6/6
c ---[1682]---> Adder-cost: 50   maxlim: 33   bits: 6/6
c ---[1681]---> Adder-cost: 50   maxlim: 33   bits: 6/6
c ---[1680]---> Adder-cost: 50   maxlim: 33   bits: 6/6
c ---[1679]---> Adder-cost: 50   maxlim: 33   bits: 6/6
c ---[1678]---> Adder-cost: 50   maxlim: 33   bits: 6/6
c ---[1677]---> Adder-cost: 50   maxlim: 33   bits: 6/6
c ---[1676]---> Adder-cost: 50   maxlim: 33   bits: 6/6
c ---[1675]---> Adder-cost: 50   maxlim: 33   bits: 6/6
c ---[1674]---> Adder-cost: 50   maxlim: 33   bits: 6/6
c ---[1673]---> Adder-cost: 50   maxlim: 33   bits: 6/6
c ---[1672]---> Adder-cost: 50   maxlim: 33   bits: 6/6
c ---[1671]---> Adder-cost: 50   maxlim: 33   bits: 6/6
c ---[1670]---> Adder-cost: 50   maxlim: 33   bits: 6/6
c ---[1669]---> Adder-cost: 50   maxlim: 33   bits: 6/6
c ---[1668]---> Adder-cost: 50   maxlim: 33   bits: 6/6
c ---[1667]---> Adder-cost: 50   maxlim: 33   bits: 6/6
c ---[1666]---> Adder-cost: 50   maxlim: 33   bits: 6/6
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   89991   327275 |   29997       0        0     nan |  0.000 % |
c |       100 |   89330   325022 |   32996      30       97     3.2 | 14.831 % |
c |       250 |   88541   322351 |   36296      95      293     3.1 | 15.714 % |
c |       475 |   87639   319319 |   39926     217      708     3.3 | 16.707 % |
c |       812 |   86305   314803 |   43918     379     1241     3.3 | 18.081 % |
c |      1318 |   84741   309489 |   48310     678     2284     3.4 | 19.740 % |
c |      2077 |   83689   305923 |   53141    1292     6093     4.7 | 20.781 % |
c |      3216 |   82642   302350 |   58455    2297    14180     6.2 | 21.792 % |
c |      4926 |   80571   295205 |   64301    3773    27831     7.4 | 23.608 % |
c |      7489 |   78145   286889 |   70731    6031    49947     8.3 | 25.969 % |
c |     11335 |   75384   277450 |   77804    9502    98555    10.4 | 28.674 % |
c |     17102 |   72431   267387 |   85584   14819   212086    14.3 | 31.610 % |
c ==============================================================================
c [1mFound solution: -15[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 230   maxlim: 15   bits: 5/4
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     18914 |   72860   269047 |   24286   16460   286339    17.4 | 31.610 % |
c |     19014 |   72748   268665 |   26714   16547   288555    17.4 | 32.190 % |
c |     19165 |   72748   268665 |   29386   16698   294239    17.6 | 32.190 % |
c |     19392 |   72453   267644 |   32324   16894   301558    17.9 | 32.405 % |
c |     19730 |   72181   266714 |   35557   17195   316368    18.4 | 32.621 % |
c |     20236 |   71865   265620 |   39112   17669   355366    20.1 | 32.895 % |
c |     20995 |   71436   264115 |   43024   18362   388655    21.2 | 33.254 % |
c |     22136 |   71278   263565 |   47326   19479   465512    23.9 | 33.427 % |
c |     23844 |   69880   258695 |   52059   20968   582163    27.8 | 34.622 % |
c |     26407 |   68921   255350 |   57265   23371   876358    37.5 | 35.476 % |
c ==============================================================================
c [1mFound solution: -16[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 8   maxlim: 16   bits: 6/5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     27766 |   68536   254028 |   22845   24651  1005205    40.8 | 35.476 % |
c |     27866 |   68460   253770 |   25129   24737  1010220    40.8 | 35.962 % |
c |     28016 |   68387   253533 |   27642   24869  1021888    41.1 | 36.045 % |
c |     28241 |   68074   252448 |   30406   25028  1038609    41.5 | 36.314 % |
c ==============================================================================
c [1mFound solution: -18[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 18   bits: 6/5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     28451 |   68078   252467 |   22692   25238  1067197    42.3 | 36.314 % |
c |     28554 |   67982   252133 |   24961   25330  1072391    42.3 | 36.369 % |
c |     28707 |   67982   252133 |   27457   25483  1097551    43.1 | 36.369 % |
c |     28933 |   67982   252133 |   30203   25709  1135292    44.2 | 36.369 % |
c |     29271 |   67947   252016 |   33223   26042  1164912    44.7 | 36.411 % |
c |     29781 |   67906   251883 |   36545   26542  1223593    46.1 | 36.459 % |
c |     30540 |   67762   251395 |   40200   27278  1293319    47.4 | 36.596 % |
c |     31680 |   67486   250469 |   44220   28371  1412498    49.8 | 36.870 % |
c |     33388 |   67312   249863 |   48642   30047  1620890    53.9 | 37.032 % |
c |     35950 |   66777   248016 |   53506   32509  1997141    61.4 | 37.509 % |
c |     39794 |   66476   246997 |   58857   36292  2792499    76.9 | 37.825 % |
c |     45560 |   66316   246463 |   64742   42024  4171195    99.3 | 37.986 % |
c |     54209 |   65438   243453 |   71217   50451  5839485   115.7 | 38.726 % |
c |     67183 |   65219   242690 |   78338   63352  9879964   156.0 | 38.899 % |
c ==============================================================================
c [1mFound solution: -19[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 19   bits: 6/5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     69321 |   65087   242224 |   21695   65470 10261712   156.7 | 38.899 % |
c |     69422 |   65087   242224 |   23864   22105  3799023   171.9 | 39.005 % |
c |     69572 |   64845   241384 |   26250   22227  3810529   171.4 | 39.202 % |
c |     69799 |   64829   241332 |   28876   22451  3834002   170.8 | 39.219 % |
c |     70136 |   64829   241332 |   31763   22788  3872673   169.9 | 39.219 % |
c |     70643 |   64829   241332 |   34940   23295  3960055   170.0 | 39.219 % |
c |     71402 |   64829   241332 |   38434   24054  4091414   170.1 | 39.219 % |
c |     72544 |   64829   241332 |   42277   25196  4345872   172.5 | 39.219 % |
c |     74252 |   64804   241251 |   46505   26899  4672688   173.7 | 39.249 % |
c |     76814 |   64752   241071 |   51155   29457  4942731   167.8 | 39.279 % |
c ==============================================================================
c [1mFound solution: -20[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 20   bits: 6/5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     80394 |   64755   241084 |   21585   33037  5836756   176.7 | 39.279 % |
c |     80494 |   64755   241084 |   23743   16619  1844839   111.0 | 39.283 % |
c |     80647 |   64755   241084 |   26117   16772  1872584   111.6 | 39.283 % |
c |     80876 |   64755   241084 |   28729   17001  1904871   112.0 | 39.283 % |
c |     81214 |   64755   241084 |   31602   17339  1939781   111.9 | 39.283 % |
c |     81721 |   64755   241084 |   34762   17846  1985083   111.2 | 39.283 % |
c |     82480 |   64755   241084 |   38239   18605  2115465   113.7 | 39.283 % |
c |     83623 |   64738   241025 |   42063   19745  2260362   114.5 | 39.301 % |
c |     85331 |   64727   240982 |   46269   21452  2584228   120.5 | 39.313 % |
c |     87895 |   64541   240334 |   50896   23989  3182607   132.7 | 39.474 % |
c |     91739 |   64530   240291 |   55985   27832  4167615   149.7 | 39.486 % |
c |     97511 |   64487   240144 |   61584   33599  5600118   166.7 | 39.533 % |
c ==============================================================================
c [1mFound solution: -21[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 21   bits: 6/5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    104205 |   64350   239670 |   21450   40272  6895597   171.2 | 39.533 % |
c |    104305 |   64350   239670 |   23595   20080  2692696   134.1 | 39.638 % |
c |    104455 |   64344   239650 |   25954   20226  2703548   133.7 | 39.644 % |
c |    104680 |   64344   239650 |   28549   20451  2749677   134.5 | 39.644 % |
c |    105020 |   64344   239650 |   31404   20791  2837626   136.5 | 39.644 % |
c |    105526 |   64344   239650 |   34545   21297  2889107   135.7 | 39.644 % |
c |    106285 |   64317   239553 |   37999   22053  3013200   136.6 | 39.650 % |
c |    107424 |   64317   239553 |   41799   23192  3184749   137.3 | 39.650 % |
c |    109133 |   64309   239523 |   45979   24899  3441511   138.2 | 39.656 % |
c |    111695 |   64293   239463 |   50577   27458  3896214   141.9 | 39.668 % |
c |    115540 |   64293   239463 |   55635   31303  4458305   142.4 | 39.668 % |
c |    121306 |   64282   239420 |   61199   37067  5773407   155.8 | 39.680 % |
c |    129955 |   64273   239389 |   67319   45712  8424476   184.3 | 39.686 % |
c |    142932 |   64230   239240 |   74051   58683 11534725   196.6 | 39.728 % |
c |    162398 |   64219   239197 |   81456   78147 17154173   219.5 | 39.740 % |
c |    191593 |   63962   238286 |   89601   41890  7827863   186.9 | 40.002 % |
c ==============================================================================
c [1mFound solution: -22[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 22   bits: 6/5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    223310 |   63823   237803 |   21274   73590 16619279   225.8 | 40.002 % |
c |    223410 |   63823   237803 |   23401   21591  3552793   164.5 | 40.131 % |
c |    223560 |   63823   237803 |   25741   21741  3573124   164.3 | 40.131 % |
c |    223785 |   63823   237803 |   28315   21966  3581224   163.0 | 40.131 % |
c |    224123 |   63823   237803 |   31147   22304  3610905   161.9 | 40.131 % |
c |    224629 |   63823   237803 |   34261   22810  3675758   161.1 | 40.131 % |
c |    225389 |   63823   237803 |   37688   23570  3761437   159.6 | 40.131 % |
c |    226528 |   63807   237751 |   41457   24706  3930736   159.1 | 40.149 % |
c |    228237 |   63730   237484 |   45602   26406  4158687   157.5 | 40.209 % |
c |    230799 |   63721   237455 |   50162   28967  4790364   165.4 | 40.221 % |
c |    234643 |   63657   237243 |   55179   32803  5498704   167.6 | 40.280 % |
c |    240409 |   63657   237243 |   60697   38569  7007933   181.7 | 40.280 % |
c |    249058 |   63632   237162 |   66766   47214  9432999   199.8 | 40.310 % |
c |    262035 |   63583   236973 |   73443   60184 12901503   214.4 | 40.358 % |
c |    281498 |   63473   236597 |   80787   79633 17358895   218.0 | 40.477 % |
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#### 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): 1.05 0.98 0.91 1/54 28067
Raw data (stat): 28067 (runsolver) R 28066 23176 23175 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 546058982 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0012 s]
Raw data (loadavg): 1.04 0.98 0.91 2/54 28067
Raw data (stat): 28067 (minisat+) R 28066 23176 23175 0 -1 0 2138 0 0 0 991 5 0 0 25 0 1 0 546058982 11309056 2106 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2761 2106 603 41 0 2720 0
vsize: 11044
[startup+20.0081 s]
Raw data (loadavg): 1.03 0.98 0.91 2/54 28067
Raw data (stat): 28067 (minisat+) R 28066 23176 23175 0 -1 0 2178 0 0 0 1991 6 0 0 25 0 1 0 546058982 11444224 2146 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2794 2146 603 41 0 2753 0
vsize: 11176
[startup+30.0087 s]
Raw data (loadavg): 1.03 0.98 0.91 2/54 28067
Raw data (stat): 28067 (minisat+) R 28066 23176 23175 0 -1 0 2218 0 0 0 2990 6 0 0 25 0 1 0 546058982 11710464 2186 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2859 2186 603 41 0 2818 0
vsize: 11436
[startup+40.0342 s]
Raw data (loadavg): 1.10 0.99 0.92 2/54 28067
Raw data (stat): 28067 (minisat+) R 28066 23176 23175 0 -1 0 2264 0 0 0 3992 7 0 0 25 0 1 0 546058982 11845632 2232 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2892 2232 603 41 0 2851 0
vsize: 11568
[startup+50.0397 s]
Raw data (loadavg): 1.08 0.99 0.92 2/54 28067
Raw data (stat): 28067 (minisat+) R 28066 23176 23175 0 -1 0 2343 0 0 0 4991 7 0 0 25 0 1 0 546058982 12115968 2311 4294967295 134512640 134672761 3221224544 3221223716 134556651 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2958 2311 603 41 0 2917 0
vsize: 11832
[startup+60.0406 s]
Raw data (loadavg): 1.07 0.99 0.92 2/54 28067
Raw data (stat): 28067 (minisat+) R 28066 23176 23175 0 -1 0 2489 0 0 0 5991 7 0 0 25 0 1 0 546058982 12791808 2457 4294967295 134512640 134672761 3221224544 3221223728 134558899 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3123 2457 603 41 0 3082 0
vsize: 12492
[startup+70.0403 s]
Raw data (loadavg): 1.06 0.99 0.92 2/54 28067
Raw data (stat): 28067 (minisat+) R 28066 23176 23175 0 -1 0 2742 0 0 0 6990 8 0 0 25 0 1 0 546058982 13983744 2710 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3414 2710 603 41 0 3373 0
vsize: 13656
[startup+80.0415 s]
Raw data (loadavg): 1.05 0.99 0.92 2/54 28067
Raw data (stat): 28067 (minisat+) R 28066 23176 23175 0 -1 0 3068 0 0 0 7989 10 0 0 25 0 1 0 546058982 15331328 3036 4294967295 134512640 134672761 3221224544 3221223680 134560566 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3743 3036 603 41 0 3702 0
vsize: 14972
[startup+90.0412 s]
Raw data (loadavg): 1.04 0.99 0.92 2/54 28067
Raw data (stat): 28067 (minisat+) R 28066 23176 23175 0 -1 0 3413 0 0 0 8988 11 0 0 25 0 1 0 546058982 16683008 3381 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4073 3382 603 41 0 4032 0
vsize: 16292
[startup+100.041 s]
Raw data (loadavg): 1.04 0.99 0.92 2/54 28067
Raw data (stat): 28067 (minisat+) R 28066 23176 23175 0 -1 0 3804 0 0 0 9987 12 0 0 25 0 1 0 546058982 18300928 3772 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4468 3773 603 41 0 4427 0
vsize: 17872
[startup+110.042 s]
Raw data (loadavg): 1.03 0.99 0.92 2/54 28067
Raw data (stat): 28067 (minisat+) R 28066 23176 23175 0 -1 0 4298 0 0 0 10986 13 0 0 25 0 1 0 546058982 20312064 4266 4294967295 134512640 134672761 3221224544 3221223704 134561029 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4959 4266 603 41 0 4918 0
vsize: 19836
[startup+120.043 s]
Raw data (loadavg): 1.02 0.99 0.92 2/54 28067
Raw data (stat): 28067 (minisat+) R 28066 23176 23175 0 -1 0 4898 0 0 0 11985 14 0 0 25 0 1 0 546058982 22859776 4866 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5581 4866 603 41 0 5540 0
vsize: 22324
[startup+130.044 s]
Raw data (loadavg): 1.02 0.99 0.92 2/54 28067
Raw data (stat): 28067 (minisat+) R 28066 23176 23175 0 -1 0 5565 0 0 0 12982 17 0 0 25 0 1 0 546058982 25690112 5533 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6272 5533 603 41 0 6231 0
vsize: 25088
[startup+140.044 s]
Raw data (loadavg): 1.02 0.99 0.92 2/54 28067
Raw data (stat): 28067 (minisat+) R 28066 23176 23175 0 -1 0 6391 0 0 0 13980 19 0 0 25 0 1 0 546058982 29057024 6359 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7094 6359 603 41 0 7053 0
vsize: 28376
[startup+150.044 s]
Raw data (loadavg): 1.01 0.99 0.92 2/54 28067
Raw data (stat): 28067 (minisat+) R 28066 23176 23175 0 -1 0 7047 0 0 0 14978 21 0 0 25 0 1 0 546058982 31744000 7015 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7750 7015 603 41 0 7709 0
vsize: 31000
[startup+160.044 s]
Raw data (loadavg): 1.01 0.99 0.92 2/54 28067
Raw data (stat): 28067 (minisat+) R 28066 23176 23175 0 -1 0 7755 0 0 0 15976 24 0 0 25 0 1 0 546058982 34557952 7723 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8437 7723 603 41 0 8396 0
vsize: 33748
[startup+170.044 s]
Raw data (loadavg): 1.01 0.99 0.92 2/54 28067
Raw data (stat): 28067 (minisat+) R 28066 23176 23175 0 -1 0 8229 0 0 0 16975 25 0 0 25 0 1 0 546058982 36442112 8197 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8897 8197 603 41 0 8856 0
vsize: 35588
[startup+180.045 s]
Raw data (loadavg): 1.01 0.99 0.92 2/54 28067
Raw data (stat): 28067 (minisat+) R 28066 23176 23175 0 -1 0 8792 0 0 0 17973 27 0 0 25 0 1 0 546058982 38858752 8760 4294967295 134512640 134672761 3221224544 3221223500 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9487 8760 603 41 0 9446 0
vsize: 37948
[startup+190.045 s]
Raw data (loadavg): 1.01 0.99 0.92 2/54 28067
Raw data (stat): 28067 (minisat+) R 28066 23176 23175 0 -1 0 9565 0 0 0 18971 29 0 0 25 0 1 0 546058982 41951232 9533 4294967295 134512640 134672761 3221224544 3221223648 134560344 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10242 9533 603 41 0 10201 0
vsize: 40968
[startup+200.046 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 28067
Raw data (stat): 28067 (minisat+) R 28066 23176 23175 0 -1 0 10305 0 0 0 19969 32 0 0 25 0 1 0 546058982 45006848 10273 4294967295 134512640 134672761 3221224544 3221223544 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10988 10273 603 41 0 10947 0
vsize: 43952
[startup+210.047 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 28067
Raw data (stat): 28067 (minisat+) R 28066 23176 23175 0 -1 0 11024 0 0 0 20966 35 0 0 25 0 1 0 546058982 47955968 10992 4294967295 134512640 134672761 3221224544 3221223712 134560942 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11708 10992 603 41 0 11667 0
vsize: 46832
[startup+220.046 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 28067
Raw data (stat): 28067 (minisat+) R 28066 23176 23175 0 -1 0 11731 0 0 0 21965 36 0 0 25 0 1 0 546058982 50774016 11699 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12396 11699 603 41 0 12355 0
vsize: 49584
[startup+230.047 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 28067
Raw data (stat): 28067 (minisat+) R 28066 23176 23175 0 -1 0 12291 0 0 0 22964 37 0 0 25 0 1 0 546058982 53035008 12259 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12948 12259 603 41 0 12907 0
vsize: 51792
[startup+240.047 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 28067
Raw data (stat): 28067 (minisat+) R 28066 23176 23175 0 -1 0 12757 0 0 0 23961 40 0 0 25 0 1 0 546058982 55062528 12725 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13443 12725 603 41 0 13402 0
vsize: 53772
[startup+250.047 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 28067
Raw data (stat): 28067 (minisat+) R 28066 23176 23175 0 -1 0 13040 0 0 0 24961 40 0 0 25 0 1 0 546058982 56143872 13008 4294967295 134512640 134672761 3221224544 3221223728 134559354 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13707 13008 603 41 0 13666 0
vsize: 54828
[startup+260.047 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 28067
Raw data (stat): 28067 (minisat+) R 28066 23176 23175 0 -1 0 13040 0 0 0 25961 40 0 0 25 0 1 0 546058982 56143872 13008 4294967295 134512640 134672761 3221224544 3221223776 134541817 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13707 13008 603 41 0 13666 0
vsize: 54828
[startup+270.047 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 28067
Raw data (stat): 28067 (minisat+) R 28066 23176 23175 0 -1 0 13040 0 0 0 26961 40 0 0 25 0 1 0 546058982 56143872 13008 4294967295 134512640 134672761 3221224544 3221223648 134560289 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13707 13008 603 41 0 13666 0
vsize: 54828
[startup+280.048 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 28067
Raw data (stat): 28067 (minisat+) R 28066 23176 23175 0 -1 0 13040 0 0 0 27961 41 0 0 25 0 1 0 546058982 56143872 13008 4294967295 134512640 134672761 3221224544 3221223712 134561014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13707 13008 603 41 0 13666 0
vsize: 54828
[startup+290.049 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 28067
Raw data (stat): 28067 (minisat+) R 28066 23176 23175 0 -1 0 13040 0 0 0 28962 41 0 0 25 0 1 0 546058982 56143872 13008 4294967295 134512640 134672761 3221224544 3221223712 134561198 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13707 13008 603 41 0 13666 0
vsize: 54828
[startup+300.049 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 28067
Raw data (stat): 28067 (minisat+) R 28066 23176 23175 0 -1 0 13040 0 0 0 29962 41 0 0 25 0 1 0 546058982 56143872 13008 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13707 13008 603 41 0 13666 0
vsize: 54828
[startup+310.05 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 28067
Raw data (stat): 28067 (minisat+) R 28066 23176 23175 0 -1 0 13040 0 0 0 30962 41 0 0 25 0 1 0 546058982 56143872 13008 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13707 13008 603 41 0 13666 0
vsize: 54828
[startup+320.05 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 28067
Raw data (stat): 28067 (minisat+) R 28066 23176 23175 0 -1 0 13040 0 0 0 31962 41 0 0 25 0 1 0 546058982 56143872 13008 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13707 13008 603 41 0 13666 0
vsize: 54828
[startup+330.051 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 28067
Raw data (stat): 28067 (minisat+) R 28066 23176 23175 0 -1 0 13040 0 0 0 32962 41 0 0 25 0 1 0 546058982 56143872 13008 4294967295 134512640 134672761 3221224544 3221223728 134559161 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13707 13008 603 41 0 13666 0
vsize: 54828
[startup+340.05 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 28067
Raw data (stat): 28067 (minisat+) R 28066 23176 23175 0 -1 0 13040 0 0 0 33962 41 0 0 25 0 1 0 546058982 56143872 13008 4294967295 134512640 134672761 3221224544 3221223712 134561005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13707 13008 603 41 0 13666 0
vsize: 54828
[startup+350.051 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 28067
Raw data (stat): 28067 (minisat+) R 28066 23176 23175 0 -1 0 13040 0 0 0 34963 41 0 0 25 0 1 0 546058982 56143872 13008 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13707 13008 603 41 0 13666 0
vsize: 54828
[startup+360.052 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 28067
Raw data (stat): 28067 (minisat+) R 28066 23176 23175 0 -1 0 13040 0 0 0 35963 41 0 0 25 0 1 0 546058982 56143872 13008 4294967295 134512640 134672761 3221224544 3221223744 134557913 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13707 13008 603 41 0 13666 0
vsize: 54828
[startup+370.051 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 28067
Raw data (stat): 28067 (minisat+) R 28066 23176 23175 0 -1 0 13040 0 0 0 36963 41 0 0 25 0 1 0 546058982 56143872 13008 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13707 13008 603 41 0 13666 0
vsize: 54828
[startup+380.051 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 28067
Raw data (stat): 28067 (minisat+) R 28066 23176 23175 0 -1 0 13040 0 0 0 37963 41 0 0 25 0 1 0 546058982 56143872 13008 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13707 13008 603 41 0 13666 0
vsize: 54828
[startup+390.052 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 28067
Raw data (stat): 28067 (minisat+) R 28066 23176 23175 0 -1 0 13040 0 0 0 38963 41 0 0 25 0 1 0 546058982 56143872 13008 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13707 13008 603 41 0 13666 0
vsize: 54828
[startup+400.052 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 28067
Raw data (stat): 28067 (minisat+) R 28066 23176 23175 0 -1 0 13040 0 0 0 39963 41 0 0 25 0 1 0 546058982 56143872 13008 4294967295 134512640 134672761 3221224544 3221223712 134561261 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13707 13008 603 41 0 13666 0
vsize: 54828
[startup+410.052 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 28067
Raw data (stat): 28067 (minisat+) R 28066 23176 23175 0 -1 0 13040 0 0 0 40963 41 0 0 25 0 1 0 546058982 56143872 13008 4294967295 134512640 134672761 3221224544 3221223648 134560237 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13707 13008 603 41 0 13666 0
vsize: 54828
[startup+420.052 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 28067
Raw data (stat): 28067 (minisat+) R 28066 23176 23175 0 -1 0 13040 0 0 0 41963 41 0 0 25 0 1 0 546058982 56143872 13008 4294967295 134512640 134672761 3221224544 3221223728 134559522 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13707 13008 603 41 0 13666 0
vsize: 54828
[startup+430.053 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 28067
Raw data (stat): 28067 (minisat+) R 28066 23176 23175 0 -1 0 13040 0 0 0 42963 41 0 0 25 0 1 0 546058982 56143872 13008 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13707 13008 603 41 0 13666 0
vsize: 54828
[startup+440.053 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 28067
Raw data (stat): 28067 (minisat+) R 28066 23176 23175 0 -1 0 13040 0 0 0 43964 41 0 0 25 0 1 0 546058982 56143872 13008 4294967295 134512640 134672761 3221224544 3221223712 134560876 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13707 13008 603 41 0 13666 0
vsize: 54828
[startup+450.053 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 28067
Raw data (stat): 28067 (minisat+) R 28066 23176 23175 0 -1 0 13040 0 0 0 44964 41 0 0 25 0 1 0 546058982 56143872 13008 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13707 13008 603 41 0 13666 0
vsize: 54828
[startup+460.054 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 28067
Raw data (stat): 28067 (minisat+) R 28066 23176 23175 0 -1 0 13040 0 0 0 45964 41 0 0 25 0 1 0 546058982 56143872 13008 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13707 13008 603 41 0 13666 0
vsize: 54828
[startup+470.054 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 28067
Raw data (stat): 28067 (minisat+) R 28066 23176 23175 0 -1 0 13502 0 0 0 46962 43 0 0 25 0 1 0 546058982 58023936 13470 4294967295 134512640 134672761 3221224544 3221223648 134560250 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14166 13470 603 41 0 14125 0
vsize: 56664
[startup+480.055 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 28067
Raw data (stat): 28067 (minisat+) R 28066 23176 23175 0 -1 0 14201 0 0 0 47960 45 0 0 25 0 1 0 546058982 60968960 14169 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14885 14169 603 41 0 14844 0
vsize: 59540
[startup+490.056 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 28067
Raw data (stat): 28067 (minisat+) R 28066 23176 23175 0 -1 0 14603 0 0 0 48959 47 0 0 25 0 1 0 546058982 62578688 14571 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15278 14571 603 41 0 15237 0
vsize: 61112
[startup+500.056 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 28067
Raw data (stat): 28067 (minisat+) R 28066 23176 23175 0 -1 0 15453 0 0 0 49957 49 0 0 25 0 1 0 546058982 66056192 15421 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16127 15421 603 41 0 16086 0
vsize: 64508
[startup+510.057 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 28067
Raw data (stat): 28067 (minisat+) R 28066 23176 23175 0 -1 0 16310 0 0 0 50955 52 0 0 25 0 1 0 546058982 69533696 16278 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16976 16278 603 41 0 16935 0
vsize: 67904
[startup+520.057 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 28067
Raw data (stat): 28067 (minisat+) R 28066 23176 23175 0 -1 0 16998 0 0 0 51953 54 0 0 25 0 1 0 546058982 72609792 16966 4294967295 134512640 134672761 3221224544 3221223680 134565045 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17727 16966 603 41 0 17686 0
vsize: 70908
[startup+530.057 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 28067
Raw data (stat): 28067 (minisat+) R 28066 23176 23175 0 -1 0 17803 0 0 0 52952 55 0 0 25 0 1 0 546058982 75935744 17771 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18539 17771 603 41 0 18498 0
vsize: 74156
[startup+540.058 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 28067
Raw data (stat): 28067 (minisat+) R 28066 23176 23175 0 -1 0 18487 0 0 0 53951 56 0 0 25 0 1 0 546058982 78761984 18455 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19229 18455 603 41 0 19188 0
vsize: 76916
[startup+550.057 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 28067
Raw data (stat): 28067 (minisat+) R 28066 23176 23175 0 -1 0 19070 0 0 0 54950 57 0 0 25 0 1 0 546058982 81051648 19038 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19788 19038 603 41 0 19747 0
vsize: 79152
[startup+560.058 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 28067
Raw data (stat): 28067 (minisat+) R 28066 23176 23175 0 -1 0 19543 0 0 0 55949 59 0 0 25 0 1 0 546058982 83070976 19511 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20281 19511 603 41 0 20240 0
vsize: 81124
[startup+570.059 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 28067
Raw data (stat): 28067 (minisat+) R 28066 23176 23175 0 -1 0 19991 0 0 0 56948 60 0 0 25 0 1 0 546058982 84791296 19959 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20701 19959 603 41 0 20660 0
vsize: 82804
[startup+580.06 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 28067
Raw data (stat): 28067 (minisat+) R 28066 23176 23175 0 -1 0 20458 0 0 0 57947 61 0 0 25 0 1 0 546058982 86790144 20426 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21189 20426 603 41 0 21148 0
vsize: 84756
[startup+590.06 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 28067
Raw data (stat): 28067 (minisat+) R 28066 23176 23175 0 -1 0 21036 0 0 0 58945 63 0 0 25 0 1 0 546058982 89071616 21004 4294967295 134512640 134672761 3221224544 3221223712 134561005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21746 21004 603 41 0 21705 0
vsize: 86984
[startup+600.06 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 28067
Raw data (stat): 28067 (minisat+) R 28066 23176 23175 0 -1 0 21560 0 0 0 59945 63 0 0 25 0 1 0 546058982 91205632 21528 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22267 21528 603 41 0 22226 0
vsize: 89068
[startup+610.061 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 28067
Raw data (stat): 28067 (minisat+) R 28066 23176 23175 0 -1 0 22047 0 0 0 60943 65 0 0 25 0 1 0 546058982 93200384 22015 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22754 22015 603 41 0 22713 0
vsize: 91016
[startup+620.061 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 28067
Raw data (stat): 28067 (minisat+) R 28066 23176 23175 0 -1 0 22477 0 0 0 61942 66 0 0 25 0 1 0 546058982 94953472 22445 4294967295 134512640 134672761 3221224544 3221223728 134559045 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23182 22445 603 41 0 23141 0
vsize: 92728
[startup+630.062 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 28067
Raw data (stat): 28067 (minisat+) R 28066 23176 23175 0 -1 0 22882 0 0 0 62941 68 0 0 25 0 1 0 546058982 96677888 22850 4294967295 134512640 134672761 3221224544 3221223692 134560552 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23603 22850 603 41 0 23562 0
vsize: 94412
[startup+640.063 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 28067
Raw data (stat): 28067 (minisat+) R 28066 23176 23175 0 -1 0 23035 0 0 0 63941 68 0 0 25 0 1 0 546058982 97349632 23003 4294967295 134512640 134672761 3221224544 3221223500 1075350790 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23767 23003 603 41 0 23726 0
vsize: 95068
[startup+650.063 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 28067
Raw data (stat): 28067 (minisat+) R 28066 23176 23175 0 -1 0 23035 0 0 0 64941 68 0 0 25 0 1 0 546058982 97349632 23003 4294967295 134512640 134672761 3221224544 3221223648 134560335 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23767 23003 603 41 0 23726 0
vsize: 95068
[startup+660.064 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 28067
Raw data (stat): 28067 (minisat+) R 28066 23176 23175 0 -1 0 23035 0 0 0 65941 68 0 0 25 0 1 0 546058982 97349632 23003 4294967295 134512640 134672761 3221224544 3221223744 134557922 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23767 23003 603 41 0 23726 0
vsize: 95068
[startup+670.064 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 28067
Raw data (stat): 28067 (minisat+) R 28066 23176 23175 0 -1 0 23035 0 0 0 66941 68 0 0 25 0 1 0 546058982 97349632 23003 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23767 23003 603 41 0 23726 0
vsize: 95068
[startup+680.066 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 28067
Raw data (stat): 28067 (minisat+) R 28066 23176 23175 0 -1 0 23035 0 0 0 67942 68 0 0 25 0 1 0 546058982 97349632 23003 4294967295 134512640 134672761 3221224544 3221223712 134560937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23767 23003 603 41 0 23726 0
vsize: 95068
[startup+690.066 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 28067
Raw data (stat): 28067 (minisat+) R 28066 23176 23175 0 -1 0 23035 0 0 0 68942 68 0 0 25 0 1 0 546058982 97349632 23003 4294967295 134512640 134672761 3221224544 3221223648 134560303 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23767 23003 603 41 0 23726 0
vsize: 95068
[startup+700.065 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 28067
Raw data (stat): 28067 (minisat+) R 28066 23176 23175 0 -1 0 23035 0 0 0 69941 68 0 0 25 0 1 0 546058982 97349632 23003 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23767 23003 603 41 0 23726 0
vsize: 95068
[startup+710.067 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 28067
Raw data (stat): 28067 (minisat+) R 28066 23176 23175 0 -1 0 23035 0 0 0 70941 69 0 0 25 0 1 0 546058982 97349632 23003 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23767 23003 603 41 0 23726 0
vsize: 95068
[startup+720.067 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 28067
Raw data (stat): 28067 (minisat+) R 28066 23176 23175 0 -1 0 23035 0 0 0 71940 69 0 0 25 0 1 0 546058982 97349632 23003 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23767 23003 603 41 0 23726 0
vsize: 95068
[startup+730.067 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 28067
Raw data (stat): 28067 (minisat+) R 28066 23176 23175 0 -1 0 23035 0 0 0 72940 69 0 0 25 0 1 0 546058982 97349632 23003 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23767 23003 603 41 0 23726 0
vsize: 95068
[startup+740.068 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 28067
Raw data (stat): 28067 (minisat+) R 28066 23176 23175 0 -1 0 23035 0 0 0 73941 69 0 0 25 0 1 0 546058982 97349632 23003 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23767 23003 603 41 0 23726 0
vsize: 95068
[startup+750.068 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 28067
Raw data (stat): 28067 (minisat+) R 28066 23176 23175 0 -1 0 23035 0 0 0 74941 69 0 0 25 0 1 0 546058982 97349632 23003 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23767 23003 603 41 0 23726 0
vsize: 95068
[startup+760.069 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 28067
Raw data (stat): 28067 (minisat+) R 28066 23176 23175 0 -1 0 23035 0 0 0 75941 69 0 0 25 0 1 0 546058982 97349632 23003 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23767 23003 603 41 0 23726 0
vsize: 95068
[startup+770.069 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 28067
Raw data (stat): 28067 (minisat+) R 28066 23176 23175 0 -1 0 23035 0 0 0 76941 69 0 0 25 0 1 0 546058982 97349632 23003 4294967295 134512640 134672761 3221224544 3221223648 134560246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23767 23003 603 41 0 23726 0
vsize: 95068
[startup+780.07 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 28067
Raw data (stat): 28067 (minisat+) R 28066 23176 23175 0 -1 0 23035 0 0 0 77941 69 0 0 25 0 1 0 546058982 97349632 23003 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23767 23003 603 41 0 23726 0
vsize: 95068
[startup+790.071 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 28067
Raw data (stat): 28067 (minisat+) R 28066 23176 23175 0 -1 0 23035 0 0 0 78941 69 0 0 25 0 1 0 546058982 97349632 23003 4294967295 134512640 134672761 3221224544 3221223648 134555116 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23767 23003 603 41 0 23726 0
vsize: 95068
[startup+800.071 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 28067
Raw data (stat): 28067 (minisat+) R 28066 23176 23175 0 -1 0 23035 0 0 0 79941 69 0 0 25 0 1 0 546058982 97349632 23003 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23767 23003 603 41 0 23726 0
vsize: 95068
[startup+810.072 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 28067
Raw data (stat): 28067 (minisat+) R 28066 23176 23175 0 -1 0 23035 0 0 0 80942 69 0 0 25 0 1 0 546058982 97349632 23003 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23767 23003 603 41 0 23726 0
vsize: 95068
[startup+820.072 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 28067
Raw data (stat): 28067 (minisat+) R 28066 23176 23175 0 -1 0 23035 0 0 0 81942 69 0 0 25 0 1 0 546058982 97349632 23003 4294967295 134512640 134672761 3221224544 3221223696 134561035 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23767 23003 603 41 0 23726 0
vsize: 95068
[startup+830.072 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 28067
Raw data (stat): 28067 (minisat+) R 28066 23176 23175 0 -1 0 23035 0 0 0 82942 69 0 0 25 0 1 0 546058982 97349632 23003 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23767 23003 603 41 0 23726 0
vsize: 95068
[startup+840.073 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 28067
Raw data (stat): 28067 (minisat+) R 28066 23176 23175 0 -1 0 23035 0 0 0 83942 70 0 0 25 0 1 0 546058982 97349632 23003 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23767 23003 603 41 0 23726 0
vsize: 95068
[startup+850.073 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 28067
Raw data (stat): 28067 (minisat+) R 28066 23176 23175 0 -1 0 23035 0 0 0 84942 70 0 0 25 0 1 0 546058982 97349632 23003 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23767 23003 603 41 0 23726 0
vsize: 95068
[startup+860.074 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 28067
Raw data (stat): 28067 (minisat+) R 28066 23176 23175 0 -1 0 23035 0 0 0 85942 70 0 0 25 0 1 0 546058982 97349632 23003 4294967295 134512640 134672761 3221224544 3221223712 134561201 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23767 23003 603 41 0 23726 0
vsize: 95068
[startup+870.074 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 28067
Raw data (stat): 28067 (minisat+) R 28066 23176 23175 0 -1 0 23035 0 0 0 86942 70 0 0 25 0 1 0 546058982 97349632 23003 4294967295 134512640 134672761 3221224544 3221223744 134557828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23767 23003 603 41 0 23726 0
vsize: 95068
[startup+880.075 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 28067
Raw data (stat): 28067 (minisat+) R 28066 23176 23175 0 -1 0 23035 0 0 0 87942 70 0 0 25 0 1 0 546058982 97349632 23003 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23767 23003 603 41 0 23726 0
vsize: 95068
[startup+890.075 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 28067
Raw data (stat): 28067 (minisat+) R 28066 23176 23175 0 -1 0 23035 0 0 0 88942 70 0 0 25 0 1 0 546058982 97349632 23003 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23767 23003 603 41 0 23726 0
vsize: 95068
[startup+900.075 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 28067
Raw data (stat): 28067 (minisat+) R 28066 23176 23175 0 -1 0 23035 0 0 0 89942 70 0 0 25 0 1 0 546058982 97349632 23003 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23767 23003 603 41 0 23726 0
vsize: 95068
[startup+910.076 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 28067
Raw data (stat): 28067 (minisat+) R 28066 23176 23175 0 -1 0 23035 0 0 0 90943 70 0 0 25 0 1 0 546058982 97349632 23003 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23767 23003 603 41 0 23726 0
vsize: 95068
[startup+920.077 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 28067
Raw data (stat): 28067 (minisat+) R 28066 23176 23175 0 -1 0 23035 0 0 0 91943 70 0 0 25 0 1 0 546058982 97349632 23003 4294967295 134512640 134672761 3221224544 3221223648 134555116 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23767 23003 603 41 0 23726 0
vsize: 95068
[startup+930.078 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 28067
Raw data (stat): 28067 (minisat+) R 28066 23176 23175 0 -1 0 23035 0 0 0 92943 70 0 0 25 0 1 0 546058982 97349632 23003 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23767 23003 603 41 0 23726 0
vsize: 95068
[startup+940.078 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 28067
Raw data (stat): 28067 (minisat+) R 28066 23176 23175 0 -1 0 23035 0 0 0 93943 70 0 0 25 0 1 0 546058982 97349632 23003 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23767 23003 603 41 0 23726 0
vsize: 95068
[startup+950.078 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 28067
Raw data (stat): 28067 (minisat+) R 28066 23176 23175 0 -1 0 23035 0 0 0 94943 70 0 0 25 0 1 0 546058982 97349632 23003 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23767 23003 603 41 0 23726 0
vsize: 95068
[startup+960.079 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 28067
Raw data (stat): 28067 (minisat+) R 28066 23176 23175 0 -1 0 23035 0 0 0 95944 70 0 0 25 0 1 0 546058982 97349632 23003 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23767 23003 603 41 0 23726 0
vsize: 95068
[startup+970.079 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 28067
Raw data (stat): 28067 (minisat+) R 28066 23176 23175 0 -1 0 23035 0 0 0 96944 70 0 0 25 0 1 0 546058982 97349632 23003 4294967295 134512640 134672761 3221224544 3221223648 134560405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23767 23003 603 41 0 23726 0
vsize: 95068
[startup+980.08 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 28067
Raw data (stat): 28067 (minisat+) R 28066 23176 23175 0 -1 0 23035 0 0 0 97944 70 0 0 25 0 1 0 546058982 97349632 23003 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23767 23003 603 41 0 23726 0
vsize: 95068
[startup+990.08 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 28067
Raw data (stat): 28067 (minisat+) R 28066 23176 23175 0 -1 0 23035 0 0 0 98944 70 0 0 25 0 1 0 546058982 97349632 23003 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23767 23003 603 41 0 23726 0
vsize: 95068
[startup+1000.08 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 28067
Raw data (stat): 28067 (minisat+) R 28066 23176 23175 0 -1 0 23035 0 0 0 99944 70 0 0 25 0 1 0 546058982 97349632 23003 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23767 23003 603 41 0 23726 0
vsize: 95068
[startup+1010.08 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 28067
Raw data (stat): 28067 (minisat+) R 28066 23176 23175 0 -1 0 23035 0 0 0 100944 70 0 0 25 0 1 0 546058982 97349632 23003 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23767 23003 603 41 0 23726 0
vsize: 95068
[startup+1020.08 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 28067
Raw data (stat): 28067 (minisat+) R 28066 23176 23175 0 -1 0 23035 0 0 0 101944 71 0 0 25 0 1 0 546058982 97349632 23003 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23767 23003 603 41 0 23726 0
vsize: 95068
[startup+1030.08 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 28067
Raw data (stat): 28067 (minisat+) R 28066 23176 23175 0 -1 0 23035 0 0 0 102944 71 0 0 25 0 1 0 546058982 97349632 23003 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23767 23003 603 41 0 23726 0
vsize: 95068
[startup+1040.08 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 28067
Raw data (stat): 28067 (minisat+) R 28066 23176 23175 0 -1 0 23035 0 0 0 103944 71 0 0 25 0 1 0 546058982 97349632 23003 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23767 23003 603 41 0 23726 0
vsize: 95068
[startup+1050.08 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 28067
Raw data (stat): 28067 (minisat+) R 28066 23176 23175 0 -1 0 23035 0 0 0 104945 71 0 0 25 0 1 0 546058982 97349632 23003 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23767 23003 603 41 0 23726 0
vsize: 95068
[startup+1060.08 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 28067
Raw data (stat): 28067 (minisat+) R 28066 23176 23175 0 -1 0 23035 0 0 0 105945 71 0 0 25 0 1 0 546058982 97349632 23003 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23767 23003 603 41 0 23726 0
vsize: 95068
[startup+1070.08 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 28067
Raw data (stat): 28067 (minisat+) R 28066 23176 23175 0 -1 0 23035 0 0 0 106945 71 0 0 25 0 1 0 546058982 97349632 23003 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23767 23003 603 41 0 23726 0
vsize: 95068
[startup+1080.08 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 28067
Raw data (stat): 28067 (minisat+) R 28066 23176 23175 0 -1 0 23035 0 0 0 107945 71 0 0 25 0 1 0 546058982 97349632 23003 4294967295 134512640 134672761 3221224544 3221223668 134566071 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23767 23003 603 41 0 23726 0
vsize: 95068
[startup+1090.09 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 28067
Raw data (stat): 28067 (minisat+) R 28066 23176 23175 0 -1 0 23035 0 0 0 108945 71 0 0 25 0 1 0 546058982 97349632 23003 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23767 23003 603 41 0 23726 0
vsize: 95068
[startup+1100.09 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 28067
Raw data (stat): 28067 (minisat+) R 28066 23176 23175 0 -1 0 23035 0 0 0 109945 71 0 0 25 0 1 0 546058982 97349632 23003 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23767 23003 603 41 0 23726 0
vsize: 95068
[startup+1110.09 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 28067
Raw data (stat): 28067 (minisat+) R 28066 23176 23175 0 -1 0 23035 0 0 0 110946 71 0 0 25 0 1 0 546058982 97349632 23003 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23767 23003 603 41 0 23726 0
vsize: 95068
[startup+1120.09 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 28067
Raw data (stat): 28067 (minisat+) R 28066 23176 23175 0 -1 0 23121 0 0 0 111946 71 0 0 25 0 1 0 546058982 97619968 23089 4294967295 134512640 134672761 3221224544 3221223712 134560931 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23833 23089 603 41 0 23792 0
vsize: 95332
[startup+1130.09 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 28067
Raw data (stat): 28067 (minisat+) R 28066 23176 23175 0 -1 0 23686 0 0 0 112944 73 0 0 25 0 1 0 546058982 100020224 23654 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24419 23654 603 41 0 24378 0
vsize: 97676
[startup+1140.09 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 28067
Raw data (stat): 28067 (minisat+) R 28066 23176 23175 0 -1 0 24177 0 0 0 113944 73 0 0 25 0 1 0 546058982 102019072 24145 4294967295 134512640 134672761 3221224544 3221223712 134560888 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24907 24145 603 41 0 24866 0
vsize: 99628
[startup+1150.09 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 28067
Raw data (stat): 28067 (minisat+) R 28066 23176 23175 0 -1 0 24633 0 0 0 114943 75 0 0 25 0 1 0 546058982 103878656 24601 4294967295 134512640 134672761 3221224544 3221223712 134560917 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25361 24601 603 41 0 25320 0
vsize: 101444
[startup+1160.09 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 28067
Raw data (stat): 28067 (minisat+) R 28066 23176 23175 0 -1 0 25086 0 0 0 115941 76 0 0 25 0 1 0 546058982 105738240 25054 4294967295 134512640 134672761 3221224544 3221223712 134560833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25815 25054 603 41 0 25774 0
vsize: 103260
[startup+1170.09 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 28067
Raw data (stat): 28067 (minisat+) R 28066 23176 23175 0 -1 0 25172 0 0 0 116941 77 0 0 25 0 1 0 546058982 106004480 25140 4294967295 134512640 134672761 3221224544 3221223648 134560402 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25880 25140 603 41 0 25839 0
vsize: 103520
[startup+1180.09 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 28067
Raw data (stat): 28067 (minisat+) R 28066 23176 23175 0 -1 0 25172 0 0 0 117941 77 0 0 25 0 1 0 546058982 106004480 25140 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25880 25140 603 41 0 25839 0
vsize: 103520
[startup+1190.09 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 28067
Raw data (stat): 28067 (minisat+) R 28066 23176 23175 0 -1 0 25172 0 0 0 118941 77 0 0 25 0 1 0 546058982 106004480 25140 4294967295 134512640 134672761 3221224544 3221223712 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25880 25140 603 41 0 25839 0
vsize: 103520
[startup+1200.09 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 28067
Raw data (stat): 28067 (minisat+) R 28066 23176 23175 0 -1 0 25173 0 0 0 119941 77 0 0 25 0 1 0 546058982 106004480 25141 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25880 25141 603 41 0 25839 0
vsize: 103520
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.15 s]
Raw data (loadavg): 1.00 0.99 0.92 1/54 28067
Raw data (stat): 28067 (minisat+) Z 28066 23176 23175 0 -1 12 25176 0 0 0 119942 81 0 0 25 0 1 0 546058982 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.15
CPU time (s): 1200.24
CPU user time (s): 1199.42
CPU system time (s): 0.819875
CPU usage (%): 100.008
Max. virtual memory (Kb): 103520
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####