PB'05 competition: run trace

Some explanations

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

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

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

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        564856 kB
Buffers:           488 kB
Cached:         443416 kB
SwapCached:          0 kB
Active:          16952 kB
Inactive:       430088 kB
HighTotal:      131008 kB
HighFree:        39256 kB
LowTotal:       903652 kB
LowFree:        525600 kB
SwapTotal:     2097136 kB
SwapFree:      2096968 kB
Dirty:              36 kB
Writeback:           0 kB
Mapped:           7220 kB
Slab:            17000 kB
Committed_AS:    92808 kB
PageTables:        344 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 08:20:42 (client local time) WITH STATUS 10 IN 1200.28 SECONDS
stats: 12945 7 1200.28 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): 0.94 0.96 0.91 2/56 24974
Raw data (stat): 24974 (runsolver) R 24973 12452 12451 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 428397735 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.0002 s]
Raw data (loadavg): 0.95 0.96 0.91 2/56 24974
Raw data (stat): 24974 (minisat+) R 24973 12452 12451 0 -1 0 2138 0 0 0 992 6 0 0 25 0 1 0 428397735 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.003 s]
Raw data (loadavg): 0.96 0.96 0.91 2/56 24974
Raw data (stat): 24974 (minisat+) R 24973 12452 12451 0 -1 0 2178 0 0 0 1992 7 0 0 25 0 1 0 428397735 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.0037 s]
Raw data (loadavg): 1.04 0.98 0.92 2/56 24976
Raw data (stat): 24974 (minisat+) R 24973 12452 12451 0 -1 0 2218 0 0 0 2991 7 0 0 25 0 1 0 428397735 11710464 2186 4294967295 134512640 134672761 3221224544 3221223716 134556671 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2859 2186 603 41 0 2818 0
vsize: 11436
[startup+40.0035 s]
Raw data (loadavg): 1.03 0.98 0.92 2/56 24978
Raw data (stat): 24974 (minisat+) R 24973 12452 12451 0 -1 0 2264 0 0 0 3991 7 0 0 25 0 1 0 428397735 11845632 2232 4294967295 134512640 134672761 3221224544 3221223716 134556618 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2892 2232 603 41 0 2851 0
vsize: 11568
[startup+50.0072 s]
Raw data (loadavg): 1.03 0.98 0.92 2/56 24978
Raw data (stat): 24974 (minisat+) R 24973 12452 12451 0 -1 0 2344 0 0 0 4991 7 0 0 25 0 1 0 428397735 12115968 2312 4294967295 134512640 134672761 3221224544 3221223716 134556680 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2958 2312 603 41 0 2917 0
vsize: 11832
[startup+60.007 s]
Raw data (loadavg): 1.02 0.98 0.92 2/56 24978
Raw data (stat): 24974 (minisat+) R 24973 12452 12451 0 -1 0 2498 0 0 0 5991 8 0 0 25 0 1 0 428397735 12791808 2466 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3123 2466 603 41 0 3082 0
vsize: 12492
[startup+70.0068 s]
Raw data (loadavg): 1.02 0.98 0.92 2/56 24978
Raw data (stat): 24974 (minisat+) R 24973 12452 12451 0 -1 0 2751 0 0 0 6990 9 0 0 25 0 1 0 428397735 13983744 2719 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3414 2719 603 41 0 3373 0
vsize: 13656
[startup+80.0076 s]
Raw data (loadavg): 1.02 0.98 0.92 2/56 24978
Raw data (stat): 24974 (minisat+) R 24973 12452 12451 0 -1 0 3104 0 0 0 7989 10 0 0 25 0 1 0 428397735 15466496 3072 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3776 3072 603 41 0 3735 0
vsize: 15104
[startup+90.0077 s]
Raw data (loadavg): 1.01 0.98 0.92 2/56 24978
Raw data (stat): 24974 (minisat+) R 24973 12452 12451 0 -1 0 3479 0 0 0 8988 11 0 0 25 0 1 0 428397735 16953344 3447 4294967295 134512640 134672761 3221224544 3221223712 134560858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4139 3447 603 41 0 4098 0
vsize: 16556
[startup+100.008 s]
Raw data (loadavg): 1.01 0.98 0.92 2/56 24978
Raw data (stat): 24974 (minisat+) R 24973 12452 12451 0 -1 0 3865 0 0 0 9987 12 0 0 25 0 1 0 428397735 18571264 3833 4294967295 134512640 134672761 3221224544 3221223716 134556627 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4534 3833 603 41 0 4493 0
vsize: 18136
[startup+110.009 s]
Raw data (loadavg): 1.01 0.98 0.92 2/56 24978
Raw data (stat): 24974 (minisat+) R 24973 12452 12451 0 -1 0 4340 0 0 0 10985 14 0 0 25 0 1 0 428397735 20447232 4308 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4992 4308 603 41 0 4951 0
vsize: 19968
[startup+120.009 s]
Raw data (loadavg): 1.01 0.98 0.92 2/56 24978
Raw data (stat): 24974 (minisat+) R 24973 12452 12451 0 -1 0 4977 0 0 0 11984 16 0 0 25 0 1 0 428397735 23265280 4945 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5680 4945 603 41 0 5639 0
vsize: 22720
[startup+130.01 s]
Raw data (loadavg): 1.00 0.98 0.92 2/56 24978
Raw data (stat): 24974 (minisat+) R 24973 12452 12451 0 -1 0 5699 0 0 0 12982 18 0 0 25 0 1 0 428397735 26226688 5667 4294967295 134512640 134672761 3221224544 3221223648 134560529 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6403 5667 603 41 0 6362 0
vsize: 25612
[startup+140.009 s]
Raw data (loadavg): 1.00 0.98 0.92 2/56 24978
Raw data (stat): 24974 (minisat+) R 24973 12452 12451 0 -1 0 6542 0 0 0 13980 20 0 0 25 0 1 0 428397735 29593600 6510 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7225 6510 603 41 0 7184 0
vsize: 28900
[startup+150.01 s]
Raw data (loadavg): 1.00 0.98 0.92 2/56 24978
Raw data (stat): 24974 (minisat+) R 24973 12452 12451 0 -1 0 7177 0 0 0 14979 21 0 0 25 0 1 0 428397735 32280576 7145 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7881 7145 603 41 0 7840 0
vsize: 31524
[startup+160.01 s]
Raw data (loadavg): 1.00 0.98 0.92 2/56 24978
Raw data (stat): 24974 (minisat+) R 24973 12452 12451 0 -1 0 7820 0 0 0 15977 23 0 0 25 0 1 0 428397735 34828288 7788 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8503 7788 603 41 0 8462 0
vsize: 34012
[startup+170.01 s]
Raw data (loadavg): 1.00 0.98 0.92 2/56 24978
Raw data (stat): 24974 (minisat+) R 24973 12452 12451 0 -1 0 8322 0 0 0 16975 25 0 0 25 0 1 0 428397735 36847616 8290 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8996 8290 603 41 0 8955 0
vsize: 35984
[startup+180.011 s]
Raw data (loadavg): 1.00 0.98 0.92 2/56 24978
Raw data (stat): 24974 (minisat+) R 24973 12452 12451 0 -1 0 8951 0 0 0 17974 26 0 0 25 0 1 0 428397735 39395328 8919 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9618 8919 603 41 0 9577 0
vsize: 38472
[startup+190.011 s]
Raw data (loadavg): 1.00 0.98 0.92 2/56 24978
Raw data (stat): 24974 (minisat+) R 24973 12452 12451 0 -1 0 9732 0 0 0 18972 29 0 0 25 0 1 0 428397735 42606592 9700 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10402 9700 603 41 0 10361 0
vsize: 41608
[startup+200.011 s]
Raw data (loadavg): 1.00 0.98 0.92 2/56 24978
Raw data (stat): 24974 (minisat+) R 24973 12452 12451 0 -1 0 10460 0 0 0 19970 31 0 0 25 0 1 0 428397735 45674496 10428 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11151 10428 603 41 0 11110 0
vsize: 44604
[startup+210.011 s]
Raw data (loadavg): 1.00 0.98 0.92 2/56 24978
Raw data (stat): 24974 (minisat+) R 24973 12452 12451 0 -1 0 11197 0 0 0 20967 34 0 0 25 0 1 0 428397735 48631808 11165 4294967295 134512640 134672761 3221224544 3221223648 134560252 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11873 11165 603 41 0 11832 0
vsize: 47492
[startup+220.012 s]
Raw data (loadavg): 1.00 0.98 0.92 2/56 24978
Raw data (stat): 24974 (minisat+) R 24973 12452 12451 0 -1 0 11908 0 0 0 21965 36 0 0 25 0 1 0 428397735 51576832 11876 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12592 11876 603 41 0 12551 0
vsize: 50368
[startup+230.013 s]
Raw data (loadavg): 1.00 0.98 0.92 2/56 24978
Raw data (stat): 24974 (minisat+) R 24973 12452 12451 0 -1 0 12419 0 0 0 22963 38 0 0 25 0 1 0 428397735 53575680 12387 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13080 12387 603 41 0 13039 0
vsize: 52320
[startup+240.012 s]
Raw data (loadavg): 1.00 0.98 0.92 2/56 24978
Raw data (stat): 24974 (minisat+) R 24973 12452 12451 0 -1 0 12886 0 0 0 23962 39 0 0 25 0 1 0 428397735 55468032 12854 4294967295 134512640 134672761 3221224544 3221223712 134561205 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13542 12854 603 41 0 13501 0
vsize: 54168
[startup+250.012 s]
Raw data (loadavg): 1.00 0.98 0.92 2/56 24978
Raw data (stat): 24974 (minisat+) R 24973 12452 12451 0 -1 0 13040 0 0 0 24962 40 0 0 25 0 1 0 428397735 56143872 13008 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13707 13008 603 41 0 13666 0
vsize: 54828
[startup+260.013 s]
Raw data (loadavg): 1.00 0.98 0.92 2/56 24978
Raw data (stat): 24974 (minisat+) R 24973 12452 12451 0 -1 0 13040 0 0 0 25962 40 0 0 25 0 1 0 428397735 56143872 13008 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13707 13008 603 41 0 13666 0
vsize: 54828
[startup+270.013 s]
Raw data (loadavg): 1.00 0.98 0.92 2/56 24980
Raw data (stat): 24974 (minisat+) R 24973 12452 12451 0 -1 0 13040 0 0 0 26962 40 0 0 25 0 1 0 428397735 56143872 13008 4294967295 134512640 134672761 3221224544 3221223648 134559887 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13707 13008 603 41 0 13666 0
vsize: 54828
[startup+280.014 s]
Raw data (loadavg): 1.00 0.98 0.92 2/56 24980
Raw data (stat): 24974 (minisat+) R 24973 12452 12451 0 -1 0 13040 0 0 0 27962 40 0 0 25 0 1 0 428397735 56143872 13008 4294967295 134512640 134672761 3221224544 3221223712 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13707 13008 603 41 0 13666 0
vsize: 54828
[startup+290.014 s]
Raw data (loadavg): 1.00 0.98 0.92 2/56 24980
Raw data (stat): 24974 (minisat+) R 24973 12452 12451 0 -1 0 13040 0 0 0 28962 40 0 0 25 0 1 0 428397735 56143872 13008 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13707 13008 603 41 0 13666 0
vsize: 54828
[startup+300.014 s]
Raw data (loadavg): 1.00 0.98 0.92 2/56 24980
Raw data (stat): 24974 (minisat+) R 24973 12452 12451 0 -1 0 13040 0 0 0 29962 40 0 0 25 0 1 0 428397735 56143872 13008 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13707 13008 603 41 0 13666 0
vsize: 54828
[startup+310.014 s]
Raw data (loadavg): 1.00 0.98 0.92 2/56 24980
Raw data (stat): 24974 (minisat+) R 24973 12452 12451 0 -1 0 13040 0 0 0 30962 40 0 0 25 0 1 0 428397735 56143872 13008 4294967295 134512640 134672761 3221224544 3221223728 134558667 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13707 13008 603 41 0 13666 0
vsize: 54828
[startup+320.014 s]
Raw data (loadavg): 1.00 0.98 0.92 2/56 24980
Raw data (stat): 24974 (minisat+) R 24973 12452 12451 0 -1 0 13040 0 0 0 31962 41 0 0 25 0 1 0 428397735 56143872 13008 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13707 13008 603 41 0 13666 0
vsize: 54828
[startup+330.015 s]
Raw data (loadavg): 1.00 0.98 0.92 2/56 24980
Raw data (stat): 24974 (minisat+) R 24973 12452 12451 0 -1 0 13040 0 0 0 32962 41 0 0 25 0 1 0 428397735 56143872 13008 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13707 13008 603 41 0 13666 0
vsize: 54828
[startup+340.015 s]
Raw data (loadavg): 1.00 0.98 0.92 2/56 24980
Raw data (stat): 24974 (minisat+) R 24973 12452 12451 0 -1 0 13040 0 0 0 33962 41 0 0 25 0 1 0 428397735 56143872 13008 4294967295 134512640 134672761 3221224544 3221223712 134561201 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13707 13008 603 41 0 13666 0
vsize: 54828
[startup+350.015 s]
Raw data (loadavg): 1.00 0.98 0.92 2/56 24980
Raw data (stat): 24974 (minisat+) R 24973 12452 12451 0 -1 0 13040 0 0 0 34962 41 0 0 25 0 1 0 428397735 56143872 13008 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13707 13008 603 41 0 13666 0
vsize: 54828
[startup+360.016 s]
Raw data (loadavg): 1.00 0.98 0.92 2/56 24980
Raw data (stat): 24974 (minisat+) R 24973 12452 12451 0 -1 0 13040 0 0 0 35962 41 0 0 25 0 1 0 428397735 56143872 13008 4294967295 134512640 134672761 3221224544 3221223712 134560822 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13707 13008 603 41 0 13666 0
vsize: 54828
[startup+370.016 s]
Raw data (loadavg): 1.00 0.98 0.92 2/56 24980
Raw data (stat): 24974 (minisat+) R 24973 12452 12451 0 -1 0 13040 0 0 0 36962 41 0 0 25 0 1 0 428397735 56143872 13008 4294967295 134512640 134672761 3221224544 3221223680 134560688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13707 13008 603 41 0 13666 0
vsize: 54828
[startup+380.016 s]
Raw data (loadavg): 1.00 0.98 0.92 2/56 24980
Raw data (stat): 24974 (minisat+) R 24973 12452 12451 0 -1 0 13040 0 0 0 37962 41 0 0 25 0 1 0 428397735 56143872 13008 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13707 13008 603 41 0 13666 0
vsize: 54828
[startup+390.018 s]
Raw data (loadavg): 1.00 0.98 0.92 2/56 24980
Raw data (stat): 24974 (minisat+) R 24973 12452 12451 0 -1 0 13040 0 0 0 38962 41 0 0 25 0 1 0 428397735 56143872 13008 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13707 13008 603 41 0 13666 0
vsize: 54828
[startup+400.017 s]
Raw data (loadavg): 1.00 0.98 0.92 2/56 24980
Raw data (stat): 24974 (minisat+) R 24973 12452 12451 0 -1 0 13040 0 0 0 39962 42 0 0 25 0 1 0 428397735 56143872 13008 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13707 13008 603 41 0 13666 0
vsize: 54828
[startup+410.017 s]
Raw data (loadavg): 1.00 0.98 0.92 2/56 24980
Raw data (stat): 24974 (minisat+) R 24973 12452 12451 0 -1 0 13040 0 0 0 40962 42 0 0 25 0 1 0 428397735 56143872 13008 4294967295 134512640 134672761 3221224544 3221223648 134560229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13707 13008 603 41 0 13666 0
vsize: 54828
[startup+420.017 s]
Raw data (loadavg): 1.00 0.98 0.92 2/56 24980
Raw data (stat): 24974 (minisat+) R 24973 12452 12451 0 -1 0 13040 0 0 0 41962 42 0 0 25 0 1 0 428397735 56143872 13008 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13707 13008 603 41 0 13666 0
vsize: 54828
[startup+430.017 s]
Raw data (loadavg): 1.00 0.98 0.92 2/56 24980
Raw data (stat): 24974 (minisat+) R 24973 12452 12451 0 -1 0 13040 0 0 0 42962 42 0 0 25 0 1 0 428397735 56143872 13008 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13707 13008 603 41 0 13666 0
vsize: 54828
[startup+440.017 s]
Raw data (loadavg): 1.00 0.98 0.92 2/56 24980
Raw data (stat): 24974 (minisat+) R 24973 12452 12451 0 -1 0 13040 0 0 0 43962 42 0 0 25 0 1 0 428397735 56143872 13008 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13707 13008 603 41 0 13666 0
vsize: 54828
[startup+450.017 s]
Raw data (loadavg): 1.00 0.98 0.92 2/56 24980
Raw data (stat): 24974 (minisat+) R 24973 12452 12451 0 -1 0 13040 0 0 0 44962 42 0 0 25 0 1 0 428397735 56143872 13008 4294967295 134512640 134672761 3221224544 3221223728 134559356 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13707 13008 603 41 0 13666 0
vsize: 54828
[startup+460.018 s]
Raw data (loadavg): 1.00 0.98 0.92 2/56 24980
Raw data (stat): 24974 (minisat+) R 24973 12452 12451 0 -1 0 13196 0 0 0 45962 43 0 0 25 0 1 0 428397735 56811520 13164 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13870 13164 603 41 0 13829 0
vsize: 55480
[startup+470.017 s]
Raw data (loadavg): 1.00 0.98 0.92 2/56 24980
Raw data (stat): 24974 (minisat+) R 24973 12452 12451 0 -1 0 13907 0 0 0 46959 45 0 0 25 0 1 0 428397735 59764736 13875 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14591 13875 603 41 0 14550 0
vsize: 58364
[startup+480.018 s]
Raw data (loadavg): 1.00 0.98 0.92 2/56 24980
Raw data (stat): 24974 (minisat+) R 24973 12452 12451 0 -1 0 14414 0 0 0 47958 47 0 0 25 0 1 0 428397735 61767680 14382 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15080 14382 603 41 0 15039 0
vsize: 60320
[startup+490.019 s]
Raw data (loadavg): 1.00 0.98 0.92 2/56 24980
Raw data (stat): 24974 (minisat+) R 24973 12452 12451 0 -1 0 15075 0 0 0 48956 49 0 0 25 0 1 0 428397735 64450560 15043 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15735 15043 603 41 0 15694 0
vsize: 62940
[startup+500.019 s]
Raw data (loadavg): 1.00 0.98 0.92 2/56 24980
Raw data (stat): 24974 (minisat+) R 24973 12452 12451 0 -1 0 15997 0 0 0 49954 51 0 0 25 0 1 0 428397735 68321280 15965 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16680 15965 603 41 0 16639 0
vsize: 66720
[startup+510.019 s]
Raw data (loadavg): 1.00 0.98 0.92 2/56 24980
Raw data (stat): 24974 (minisat+) R 24973 12452 12451 0 -1 0 16720 0 0 0 50952 53 0 0 25 0 1 0 428397735 71274496 16688 4294967295 134512640 134672761 3221224544 3221223648 134560215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17401 16688 603 41 0 17360 0
vsize: 69604
[startup+520.018 s]
Raw data (loadavg): 1.00 0.98 0.92 2/56 24980
Raw data (stat): 24974 (minisat+) R 24973 12452 12451 0 -1 0 17514 0 0 0 51950 55 0 0 25 0 1 0 428397735 74735616 17482 4294967295 134512640 134672761 3221224544 3221223648 134560529 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18246 17482 603 41 0 18205 0
vsize: 72984
[startup+530.019 s]
Raw data (loadavg): 1.00 0.98 0.92 2/56 24980
Raw data (stat): 24974 (minisat+) R 24973 12452 12451 0 -1 0 18273 0 0 0 52948 58 0 0 25 0 1 0 428397735 77824000 18241 4294967295 134512640 134672761 3221224544 3221223744 134557820 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19000 18241 603 41 0 18959 0
vsize: 76000
[startup+540.019 s]
Raw data (loadavg): 1.00 0.98 0.92 2/56 24980
Raw data (stat): 24974 (minisat+) R 24973 12452 12451 0 -1 0 18901 0 0 0 53947 59 0 0 25 0 1 0 428397735 80379904 18869 4294967295 134512640 134672761 3221224544 3221223668 134566109 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19624 18869 603 41 0 19583 0
vsize: 78496
[startup+550.019 s]
Raw data (loadavg): 1.00 0.98 0.92 2/56 24980
Raw data (stat): 24974 (minisat+) R 24973 12452 12451 0 -1 0 19419 0 0 0 54946 60 0 0 25 0 1 0 428397735 82538496 19387 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20151 19387 603 41 0 20110 0
vsize: 80604
[startup+560.02 s]
Raw data (loadavg): 1.00 0.98 0.92 2/56 24980
Raw data (stat): 24974 (minisat+) R 24973 12452 12451 0 -1 0 19859 0 0 0 55944 62 0 0 25 0 1 0 428397735 84377600 19827 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20600 19827 603 41 0 20559 0
vsize: 82400
[startup+570.02 s]
Raw data (loadavg): 1.00 0.98 0.92 2/56 24982
Raw data (stat): 24974 (minisat+) R 24973 12452 12451 0 -1 0 20332 0 0 0 56942 64 0 0 25 0 1 0 428397735 86253568 20300 4294967295 134512640 134672761 3221224544 3221223680 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21058 20300 603 41 0 21017 0
vsize: 84232
[startup+580.02 s]
Raw data (loadavg): 1.00 0.98 0.92 2/56 24982
Raw data (stat): 24974 (minisat+) R 24973 12452 12451 0 -1 0 20902 0 0 0 57941 66 0 0 25 0 1 0 428397735 88535040 20870 4294967295 134512640 134672761 3221224544 3221223712 134561207 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21615 20870 603 41 0 21574 0
vsize: 86460
[startup+590.02 s]
Raw data (loadavg): 1.00 0.98 0.92 2/56 24982
Raw data (stat): 24974 (minisat+) R 24973 12452 12451 0 -1 0 21463 0 0 0 58939 68 0 0 25 0 1 0 428397735 90804224 21431 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22169 21431 603 41 0 22128 0
vsize: 88676
[startup+600.02 s]
Raw data (loadavg): 1.00 0.98 0.92 2/56 24982
Raw data (stat): 24974 (minisat+) R 24973 12452 12451 0 -1 0 21951 0 0 0 59938 69 0 0 25 0 1 0 428397735 92803072 21919 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22657 21919 603 41 0 22616 0
vsize: 90628
[startup+610.019 s]
Raw data (loadavg): 1.00 0.98 0.92 2/56 24982
Raw data (stat): 24974 (minisat+) R 24973 12452 12451 0 -1 0 22407 0 0 0 60937 70 0 0 25 0 1 0 428397735 94683136 22375 4294967295 134512640 134672761 3221224544 3221223712 134560858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23116 22375 603 41 0 23075 0
vsize: 92464
[startup+620.019 s]
Raw data (loadavg): 1.00 0.98 0.92 2/56 24982
Raw data (stat): 24974 (minisat+) R 24973 12452 12451 0 -1 0 22871 0 0 0 61935 72 0 0 25 0 1 0 428397735 96677888 22839 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23603 22839 603 41 0 23562 0
vsize: 94412
[startup+630.021 s]
Raw data (loadavg): 1.00 0.98 0.92 2/56 24982
Raw data (stat): 24974 (minisat+) R 24973 12452 12451 0 -1 0 23035 0 0 0 62935 72 0 0 25 0 1 0 428397735 97349632 23003 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23767 23003 603 41 0 23726 0
vsize: 95068
[startup+640.021 s]
Raw data (loadavg): 1.00 0.98 0.92 2/56 24982
Raw data (stat): 24974 (minisat+) R 24973 12452 12451 0 -1 0 23035 0 0 0 63935 72 0 0 25 0 1 0 428397735 97349632 23003 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23767 23003 603 41 0 23726 0
vsize: 95068
[startup+650.021 s]
Raw data (loadavg): 1.00 0.98 0.92 2/56 24982
Raw data (stat): 24974 (minisat+) R 24973 12452 12451 0 -1 0 23035 0 0 0 64935 73 0 0 25 0 1 0 428397735 97349632 23003 4294967295 134512640 134672761 3221224544 3221223712 134561372 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23767 23003 603 41 0 23726 0
vsize: 95068
[startup+660.02 s]
Raw data (loadavg): 1.00 0.98 0.92 2/56 24982
Raw data (stat): 24974 (minisat+) R 24973 12452 12451 0 -1 0 23035 0 0 0 65935 73 0 0 25 0 1 0 428397735 97349632 23003 4294967295 134512640 134672761 3221224544 3221223716 134556651 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23767 23003 603 41 0 23726 0
vsize: 95068
[startup+670.02 s]
Raw data (loadavg): 1.00 0.98 0.92 2/56 24982
Raw data (stat): 24974 (minisat+) R 24973 12452 12451 0 -1 0 23035 0 0 0 66935 73 0 0 25 0 1 0 428397735 97349632 23003 4294967295 134512640 134672761 3221224544 3221223648 134560361 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23767 23003 603 41 0 23726 0
vsize: 95068
[startup+680.021 s]
Raw data (loadavg): 1.00 0.98 0.92 2/56 24982
Raw data (stat): 24974 (minisat+) R 24973 12452 12451 0 -1 0 23035 0 0 0 67935 73 0 0 25 0 1 0 428397735 97349632 23003 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23767 23003 603 41 0 23726 0
vsize: 95068
[startup+690.021 s]
Raw data (loadavg): 1.00 0.98 0.92 2/56 24982
Raw data (stat): 24974 (minisat+) R 24973 12452 12451 0 -1 0 23035 0 0 0 68935 73 0 0 25 0 1 0 428397735 97349632 23003 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23767 23003 603 41 0 23726 0
vsize: 95068
[startup+700.021 s]
Raw data (loadavg): 1.00 0.98 0.92 2/56 24982
Raw data (stat): 24974 (minisat+) R 24973 12452 12451 0 -1 0 23035 0 0 0 69935 73 0 0 25 0 1 0 428397735 97349632 23003 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23767 23003 603 41 0 23726 0
vsize: 95068
[startup+710.021 s]
Raw data (loadavg): 1.00 0.98 0.92 2/56 24982
Raw data (stat): 24974 (minisat+) R 24973 12452 12451 0 -1 0 23035 0 0 0 70935 73 0 0 25 0 1 0 428397735 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+720.021 s]
Raw data (loadavg): 1.00 0.98 0.92 2/56 24982
Raw data (stat): 24974 (minisat+) R 24973 12452 12451 0 -1 0 23035 0 0 0 71935 73 0 0 25 0 1 0 428397735 97349632 23003 4294967295 134512640 134672761 3221224544 3221223648 134560402 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.022 s]
Raw data (loadavg): 1.00 0.98 0.92 2/56 24982
Raw data (stat): 24974 (minisat+) R 24973 12452 12451 0 -1 0 23035 0 0 0 72935 73 0 0 25 0 1 0 428397735 97349632 23003 4294967295 134512640 134672761 3221224544 3221223712 134561385 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23767 23003 603 41 0 23726 0
vsize: 95068
[startup+740.023 s]
Raw data (loadavg): 1.00 0.98 0.92 2/56 24982
Raw data (stat): 24974 (minisat+) R 24973 12452 12451 0 -1 0 23035 0 0 0 73936 73 0 0 25 0 1 0 428397735 97349632 23003 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23767 23003 603 41 0 23726 0
vsize: 95068
[startup+750.023 s]
Raw data (loadavg): 1.00 0.98 0.92 2/56 24982
Raw data (stat): 24974 (minisat+) R 24973 12452 12451 0 -1 0 23035 0 0 0 74936 73 0 0 25 0 1 0 428397735 97349632 23003 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23767 23003 603 41 0 23726 0
vsize: 95068
[startup+760.023 s]
Raw data (loadavg): 1.00 0.98 0.92 2/56 24982
Raw data (stat): 24974 (minisat+) R 24973 12452 12451 0 -1 0 23035 0 0 0 75936 74 0 0 25 0 1 0 428397735 97349632 23003 4294967295 134512640 134672761 3221224544 3221223648 134560361 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23767 23003 603 41 0 23726 0
vsize: 95068
[startup+770.023 s]
Raw data (loadavg): 1.00 0.98 0.92 2/56 24982
Raw data (stat): 24974 (minisat+) R 24973 12452 12451 0 -1 0 23035 0 0 0 76936 74 0 0 25 0 1 0 428397735 97349632 23003 4294967295 134512640 134672761 3221224544 3221223680 134560661 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23767 23003 603 41 0 23726 0
vsize: 95068
[startup+780.024 s]
Raw data (loadavg): 1.00 0.98 0.92 2/56 24982
Raw data (stat): 24974 (minisat+) R 24973 12452 12451 0 -1 0 23035 0 0 0 77936 74 0 0 25 0 1 0 428397735 97349632 23003 4294967295 134512640 134672761 3221224544 3221223712 134560876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23767 23003 603 41 0 23726 0
vsize: 95068
[startup+790.024 s]
Raw data (loadavg): 1.00 0.98 0.92 2/56 24982
Raw data (stat): 24974 (minisat+) R 24973 12452 12451 0 -1 0 23035 0 0 0 78936 74 0 0 25 0 1 0 428397735 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+800.023 s]
Raw data (loadavg): 1.00 0.98 0.92 2/56 24982
Raw data (stat): 24974 (minisat+) R 24973 12452 12451 0 -1 0 23035 0 0 0 79936 74 0 0 25 0 1 0 428397735 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+810.024 s]
Raw data (loadavg): 1.00 0.98 0.92 2/56 24982
Raw data (stat): 24974 (minisat+) R 24973 12452 12451 0 -1 0 23035 0 0 0 80936 74 0 0 25 0 1 0 428397735 97349632 23003 4294967295 134512640 134672761 3221224544 3221223744 134557836 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23767 23003 603 41 0 23726 0
vsize: 95068
[startup+820.023 s]
Raw data (loadavg): 1.00 0.98 0.92 2/56 24982
Raw data (stat): 24974 (minisat+) R 24973 12452 12451 0 -1 0 23035 0 0 0 81936 74 0 0 25 0 1 0 428397735 97349632 23003 4294967295 134512640 134672761 3221224544 3221223648 134560285 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23767 23003 603 41 0 23726 0
vsize: 95068
[startup+830.024 s]
Raw data (loadavg): 1.00 0.98 0.92 2/56 24982
Raw data (stat): 24974 (minisat+) R 24973 12452 12451 0 -1 0 23035 0 0 0 82936 75 0 0 25 0 1 0 428397735 97349632 23003 4294967295 134512640 134672761 3221224544 3221223844 134556639 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23767 23003 603 41 0 23726 0
vsize: 95068
[startup+840.024 s]
Raw data (loadavg): 1.00 0.98 0.92 2/56 24982
Raw data (stat): 24974 (minisat+) R 24973 12452 12451 0 -1 0 23035 0 0 0 83936 75 0 0 25 0 1 0 428397735 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+850.023 s]
Raw data (loadavg): 1.00 0.98 0.92 2/56 24982
Raw data (stat): 24974 (minisat+) R 24973 12452 12451 0 -1 0 23035 0 0 0 84936 75 0 0 25 0 1 0 428397735 97349632 23003 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23767 23003 603 41 0 23726 0
vsize: 95068
[startup+860.024 s]
Raw data (loadavg): 1.00 0.98 0.92 2/56 24982
Raw data (stat): 24974 (minisat+) R 24973 12452 12451 0 -1 0 23035 0 0 0 85936 75 0 0 25 0 1 0 428397735 97349632 23003 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23767 23003 603 41 0 23726 0
vsize: 95068
[startup+870.025 s]
Raw data (loadavg): 1.00 0.98 0.92 2/56 24984
Raw data (stat): 24974 (minisat+) R 24973 12452 12451 0 -1 0 23035 0 0 0 86936 75 0 0 25 0 1 0 428397735 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+880.025 s]
Raw data (loadavg): 1.00 0.98 0.92 2/56 24984
Raw data (stat): 24974 (minisat+) R 24973 12452 12451 0 -1 0 23035 0 0 0 87936 75 0 0 25 0 1 0 428397735 97349632 23003 4294967295 134512640 134672761 3221224544 3221223680 134560709 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23767 23003 603 41 0 23726 0
vsize: 95068
[startup+890.025 s]
Raw data (loadavg): 1.00 0.98 0.92 2/56 24984
Raw data (stat): 24974 (minisat+) R 24973 12452 12451 0 -1 0 23035 0 0 0 88936 75 0 0 25 0 1 0 428397735 97349632 23003 4294967295 134512640 134672761 3221224544 3221223712 134561118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23767 23003 603 41 0 23726 0
vsize: 95068
[startup+900.025 s]
Raw data (loadavg): 1.00 0.98 0.92 2/56 24984
Raw data (stat): 24974 (minisat+) R 24973 12452 12451 0 -1 0 23035 0 0 0 89936 75 0 0 25 0 1 0 428397735 97349632 23003 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23767 23003 603 41 0 23726 0
vsize: 95068
[startup+910.025 s]
Raw data (loadavg): 1.00 0.98 0.92 2/56 24984
Raw data (stat): 24974 (minisat+) R 24973 12452 12451 0 -1 0 23035 0 0 0 90936 75 0 0 25 0 1 0 428397735 97349632 23003 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23767 23003 603 41 0 23726 0
vsize: 95068
[startup+920.033 s]
Raw data (loadavg): 1.00 0.98 0.92 2/56 24984
Raw data (stat): 24974 (minisat+) R 24973 12452 12451 0 -1 0 23035 0 0 0 91937 76 0 0 25 0 1 0 428397735 97349632 23003 4294967295 134512640 134672761 3221224544 3221223744 134557922 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23767 23003 603 41 0 23726 0
vsize: 95068
[startup+930.04 s]
Raw data (loadavg): 1.00 0.98 0.92 2/56 24984
Raw data (stat): 24974 (minisat+) R 24973 12452 12451 0 -1 0 23035 0 0 0 92937 76 0 0 25 0 1 0 428397735 97349632 23003 4294967295 134512640 134672761 3221224544 3221223712 134561021 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23767 23003 603 41 0 23726 0
vsize: 95068
[startup+940.039 s]
Raw data (loadavg): 1.00 0.98 0.92 2/56 24984
Raw data (stat): 24974 (minisat+) R 24973 12452 12451 0 -1 0 23035 0 0 0 93937 76 0 0 25 0 1 0 428397735 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+950.039 s]
Raw data (loadavg): 1.00 0.98 0.92 2/56 24984
Raw data (stat): 24974 (minisat+) R 24973 12452 12451 0 -1 0 23035 0 0 0 94937 76 0 0 25 0 1 0 428397735 97349632 23003 4294967295 134512640 134672761 3221224544 3221223728 134559340 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23767 23003 603 41 0 23726 0
vsize: 95068
[startup+960.04 s]
Raw data (loadavg): 1.00 0.98 0.92 2/56 24984
Raw data (stat): 24974 (minisat+) R 24973 12452 12451 0 -1 0 23035 0 0 0 95937 76 0 0 25 0 1 0 428397735 97349632 23003 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23767 23003 603 41 0 23726 0
vsize: 95068
[startup+970.04 s]
Raw data (loadavg): 1.00 0.98 0.92 2/56 24984
Raw data (stat): 24974 (minisat+) R 24973 12452 12451 0 -1 0 23035 0 0 0 96938 76 0 0 25 0 1 0 428397735 97349632 23003 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23767 23003 603 41 0 23726 0
vsize: 95068
[startup+980.041 s]
Raw data (loadavg): 1.00 0.98 0.92 2/56 24984
Raw data (stat): 24974 (minisat+) R 24973 12452 12451 0 -1 0 23035 0 0 0 97938 77 0 0 25 0 1 0 428397735 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+990.047 s]
Raw data (loadavg): 1.00 0.98 0.92 2/56 24984
Raw data (stat): 24974 (minisat+) R 24973 12452 12451 0 -1 0 23035 0 0 0 98938 77 0 0 25 0 1 0 428397735 97349632 23003 4294967295 134512640 134672761 3221224544 3221223712 134560906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23767 23003 603 41 0 23726 0
vsize: 95068
[startup+1000.05 s]
Raw data (loadavg): 1.00 0.98 0.92 2/56 24984
Raw data (stat): 24974 (minisat+) R 24973 12452 12451 0 -1 0 23035 0 0 0 99938 77 0 0 25 0 1 0 428397735 97349632 23003 4294967295 134512640 134672761 3221224544 3221223648 134559835 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23767 23003 603 41 0 23726 0
vsize: 95068
[startup+1010.05 s]
Raw data (loadavg): 1.00 0.98 0.92 2/56 24984
Raw data (stat): 24974 (minisat+) R 24973 12452 12451 0 -1 0 23035 0 0 0 100938 77 0 0 25 0 1 0 428397735 97349632 23003 4294967295 134512640 134672761 3221224544 3221223744 134557828 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.05 s]
Raw data (loadavg): 1.00 0.98 0.92 2/56 24984
Raw data (stat): 24974 (minisat+) R 24973 12452 12451 0 -1 0 23035 0 0 0 101938 77 0 0 25 0 1 0 428397735 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+1030.05 s]
Raw data (loadavg): 1.00 0.98 0.92 2/56 24984
Raw data (stat): 24974 (minisat+) R 24973 12452 12451 0 -1 0 23035 0 0 0 102938 78 0 0 25 0 1 0 428397735 97349632 23003 4294967295 134512640 134672761 3221224544 3221223728 134558645 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23767 23003 603 41 0 23726 0
vsize: 95068
[startup+1040.05 s]
Raw data (loadavg): 1.00 0.98 0.92 2/56 24984
Raw data (stat): 24974 (minisat+) R 24973 12452 12451 0 -1 0 23035 0 0 0 103938 78 0 0 25 0 1 0 428397735 97349632 23003 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23767 23003 603 41 0 23726 0
vsize: 95068
[startup+1050.05 s]
Raw data (loadavg): 1.00 0.98 0.92 2/56 24984
Raw data (stat): 24974 (minisat+) R 24973 12452 12451 0 -1 0 23035 0 0 0 104938 78 0 0 25 0 1 0 428397735 97349632 23003 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23767 23003 603 41 0 23726 0
vsize: 95068
[startup+1060.06 s]
Raw data (loadavg): 1.00 0.98 0.92 2/56 24984
Raw data (stat): 24974 (minisat+) R 24973 12452 12451 0 -1 0 23035 0 0 0 105939 78 0 0 25 0 1 0 428397735 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+1070.06 s]
Raw data (loadavg): 1.00 0.98 0.92 2/56 24984
Raw data (stat): 24974 (minisat+) R 24973 12452 12451 0 -1 0 23035 0 0 0 106939 78 0 0 25 0 1 0 428397735 97349632 23003 4294967295 134512640 134672761 3221224544 3221223648 134560529 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23767 23003 603 41 0 23726 0
vsize: 95068
[startup+1080.06 s]
Raw data (loadavg): 1.00 0.98 0.92 2/56 24984
Raw data (stat): 24974 (minisat+) R 24973 12452 12451 0 -1 0 23035 0 0 0 107939 78 0 0 25 0 1 0 428397735 97349632 23003 4294967295 134512640 134672761 3221224544 3221223648 134560289 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23767 23003 603 41 0 23726 0
vsize: 95068
[startup+1090.06 s]
Raw data (loadavg): 1.00 0.98 0.92 2/56 24984
Raw data (stat): 24974 (minisat+) R 24973 12452 12451 0 -1 0 23035 0 0 0 108939 79 0 0 25 0 1 0 428397735 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+1100.06 s]
Raw data (loadavg): 1.00 0.98 0.92 2/56 24984
Raw data (stat): 24974 (minisat+) R 24973 12452 12451 0 -1 0 23035 0 0 0 109939 79 0 0 25 0 1 0 428397735 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+1110.06 s]
Raw data (loadavg): 1.00 0.98 0.92 2/56 24984
Raw data (stat): 24974 (minisat+) R 24973 12452 12451 0 -1 0 23578 0 0 0 110937 80 0 0 25 0 1 0 428397735 99483648 23546 4294967295 134512640 134672761 3221224544 3221223744 134557830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24288 23546 603 41 0 24247 0
vsize: 97152
[startup+1120.06 s]
Raw data (loadavg): 1.00 0.98 0.92 2/56 24984
Raw data (stat): 24974 (minisat+) R 24973 12452 12451 0 -1 0 24111 0 0 0 111935 82 0 0 25 0 1 0 428397735 101748736 24079 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24841 24079 603 41 0 24800 0
vsize: 99364
[startup+1130.07 s]
Raw data (loadavg): 1.00 0.98 0.92 2/56 24984
Raw data (stat): 24974 (minisat+) R 24973 12452 12451 0 -1 0 24570 0 0 0 112936 83 0 0 25 0 1 0 428397735 103612416 24538 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25296 24538 603 41 0 25255 0
vsize: 101184
[startup+1140.07 s]
Raw data (loadavg): 1.00 0.98 0.92 2/56 24984
Raw data (stat): 24974 (minisat+) R 24973 12452 12451 0 -1 0 25045 0 0 0 113934 85 0 0 25 0 1 0 428397735 105472000 25013 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25750 25013 603 41 0 25709 0
vsize: 103000
[startup+1150.07 s]
Raw data (loadavg): 1.00 0.98 0.92 2/56 24984
Raw data (stat): 24974 (minisat+) R 24973 12452 12451 0 -1 0 25172 0 0 0 114934 85 0 0 25 0 1 0 428397735 106004480 25140 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25880 25140 603 41 0 25839 0
vsize: 103520
[startup+1160.07 s]
Raw data (loadavg): 1.00 0.98 0.92 2/56 24984
Raw data (stat): 24974 (minisat+) R 24973 12452 12451 0 -1 0 25172 0 0 0 115934 86 0 0 25 0 1 0 428397735 106004480 25140 4294967295 134512640 134672761 3221224544 3221223728 134559405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25880 25140 603 41 0 25839 0
vsize: 103520
[startup+1170.09 s]
Raw data (loadavg): 1.00 0.98 0.92 2/56 24986
Raw data (stat): 24974 (minisat+) R 24973 12452 12451 0 -1 0 25172 0 0 0 116935 86 0 0 25 0 1 0 428397735 106004480 25140 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25880 25140 603 41 0 25839 0
vsize: 103520
[startup+1180.09 s]
Raw data (loadavg): 1.00 0.98 0.92 2/56 24986
Raw data (stat): 24974 (minisat+) R 24973 12452 12451 0 -1 0 25173 0 0 0 117935 86 0 0 25 0 1 0 428397735 106004480 25141 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25880 25141 603 41 0 25839 0
vsize: 103520
[startup+1190.09 s]
Raw data (loadavg): 1.00 0.98 0.92 2/56 24986
Raw data (stat): 24974 (minisat+) R 24973 12452 12451 0 -1 0 25173 0 0 0 118935 86 0 0 25 0 1 0 428397735 106004480 25141 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25880 25141 603 41 0 25839 0
vsize: 103520
[startup+1200.09 s]
Raw data (loadavg): 1.00 0.98 0.92 2/56 24986
Raw data (stat): 24974 (minisat+) R 24973 12452 12451 0 -1 0 25174 0 0 0 119936 86 0 0 25 0 1 0 428397735 106004480 25142 4294967295 134512640 134672761 3221224544 3221223616 134553544 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25880 25142 603 41 0 25839 0
vsize: 103520
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.29 s]
Raw data (loadavg): 1.00 0.98 0.92 1/56 24986
Raw data (stat): 24974 (minisat+) Z 24973 12452 12451 0 -1 12 25177 0 0 0 119936 91 0 0 22 0 1 0 428397735 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.29
CPU time (s): 1200.28
CPU user time (s): 1199.37
CPU system time (s): 0.913861
CPU usage (%): 99.9992
Max. virtual memory (Kb): 103520
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####