PB'05 competition: run trace

Some explanations

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

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

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.177
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:        831468 kB
Buffers:         18708 kB
Cached:         161420 kB
SwapCached:        752 kB
Active:          41952 kB
Inactive:       140180 kB
HighTotal:      131008 kB
HighFree:         5152 kB
LowTotal:       903652 kB
LowFree:        826316 kB
SwapTotal:     2097892 kB
SwapFree:      2096168 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5104 kB
Slab:            15584 kB
Committed_AS:    63816 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 15:33:46 (client local time) WITH STATUS 10 IN 1200.18 SECONDS
stats: 17938 7 1200.18 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 2149 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: #####################################
c   -- Clauses(.)/Splits(s): ..................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ---[1908]---> BDD-cost:   98
c ---[1907]---> BDD-cost:   98
c ---[1906]---> BDD-cost:   98
c ---[1905]---> BDD-cost:   98
c ---[1904]---> BDD-cost:   98
c ---[1903]---> BDD-cost:   98
c ---[1902]---> BDD-cost:   98
c ---[1901]---> BDD-cost:   98
c ---[1900]---> BDD-cost:   98
c ---[1899]---> BDD-cost:   98
c ---[1898]---> BDD-cost:   98
c ---[1897]---> BDD-cost:   98
c ---[1896]---> BDD-cost:   98
c ---[1895]---> BDD-cost:   98
c ---[1894]---> BDD-cost:   98
c ---[1893]---> BDD-cost:   98
c ---[1892]---> BDD-cost:   98
c ---[1891]---> BDD-cost:   98
c ---[1890]---> BDD-cost:   98
c ---[1889]---> BDD-cost:   98
c ---[1888]---> BDD-cost:   98
c ---[1887]---> BDD-cost:   98
c ---[1886]---> BDD-cost:   98
c ---[1885]---> BDD-cost:   98
c ---[1884]---> BDD-cost:   98
c ---[1883]---> BDD-cost:   98
c ---[1882]---> BDD-cost:   98
c ---[1881]---> BDD-cost:   98
c ---[1880]---> BDD-cost:   98
c ---[1879]---> BDD-cost:   98
c ---[1878]---> BDD-cost:   98
c ---[1877]---> BDD-cost:   98
c ---[1876]---> BDD-cost:   98
c ---[1875]---> BDD-cost:   98
c ---[1874]---> BDD-cost:   98
c ---[1873]---> BDD-cost:   98
c ---[1872]---> BDD-cost:   98
c ---[1871]---> BDD-cost:   98
c ---[1870]---> BDD-cost:   98
c ---[1869]---> BDD-cost:   98
c ---[1868]---> BDD-cost:   98
c ---[1867]---> BDD-cost:   98
c ---[1866]---> BDD-cost:   98
c ---[1865]---> BDD-cost:   98
c ---[1864]---> BDD-cost:   98
c ---[1863]---> BDD-cost:   98
c ---[1862]---> BDD-cost:   98
c ---[1861]---> BDD-cost:   98
c ---[1860]---> BDD-cost:   98
c ---[1859]---> BDD-cost:   98
c ---[1858]---> BDD-cost:   98
c ---[1857]---> BDD-cost:   98
c ---[1856]---> BDD-cost:   98
c ---[1855]---> BDD-cost:   98
c ---[1854]---> BDD-cost:   98
c ---[1853]---> BDD-cost:   98
c ---[1852]---> BDD-cost:   98
c ---[1851]---> BDD-cost:   98
c ---[1850]---> BDD-cost:   98
c ---[1849]---> BDD-cost:   98
c ---[1848]---> BDD-cost:   98
c ---[1847]---> BDD-cost:   98
c ---[1846]---> BDD-cost:   98
c ---[1845]---> BDD-cost:   98
c ---[1844]---> BDD-cost:   98
c ---[1843]---> BDD-cost:   98
c ---[1842]---> BDD-cost:   98
c ---[1841]---> BDD-cost:   98
c ---[1840]---> BDD-cost:   98
c ---[1839]---> BDD-cost:   98
c ---[1838]---> BDD-cost:   98
c ---[1837]---> BDD-cost:   98
c ---[1836]---> BDD-cost:   98
c ---[1835]---> BDD-cost:   98
c ---[1834]---> BDD-cost:   98
c ---[1833]---> BDD-cost:   98
c ---[1832]---> BDD-cost:   98
c ---[1831]---> BDD-cost:   98
c ---[1830]---> BDD-cost:   98
c ---[1829]---> BDD-cost:   98
c ---[1828]---> BDD-cost:   98
c ---[1827]---> BDD-cost:   98
c ---[1826]---> BDD-cost:   98
c ---[1825]---> BDD-cost:   98
c ---[1824]---> BDD-cost:   98
c ---[1823]---> BDD-cost:   98
c ---[1822]---> BDD-cost:   98
c ---[1821]---> BDD-cost:   98
c ---[1820]---> BDD-cost:   98
c ---[1819]---> BDD-cost:   98
c ---[1818]---> BDD-cost:   98
c ---[1817]---> BDD-cost:   98
c ---[1816]---> BDD-cost:   98
c ---[1815]---> BDD-cost:   98
c ---[1814]---> BDD-cost:   98
c ---[1813]---> BDD-cost:   98
c ---[1812]---> BDD-cost:   98
c ---[1811]---> BDD-cost:   98
c ---[1810]---> BDD-cost:   98
c ---[1809]---> BDD-cost:   98
c ---[1808]---> BDD-cost:   98
c ---[1807]---> BDD-cost:   98
c ---[1806]---> BDD-cost:   98
c ---[1805]---> BDD-cost:   98
c ---[1804]---> BDD-cost:   98
c ---[1803]---> BDD-cost:   98
c ---[1802]---> BDD-cost:   98
c ---[1801]---> BDD-cost:   98
c ---[1800]---> BDD-cost:   98
c ---[1799]---> BDD-cost:   98
c ---[1798]---> BDD-cost:   98
c ---[1797]---> BDD-cost:   98
c ---[1796]---> BDD-cost:   98
c ---[1795]---> BDD-cost:   98
c ---[1794]---> BDD-cost:   98
c ---[1793]---> BDD-cost:   98
c ---[1792]---> BDD-cost:   98
c ---[1791]---> BDD-cost:   98
c ---[1790]---> BDD-cost:   98
c ---[1789]---> BDD-cost:   98
c ---[1787]---> Adder-cost: 1658   maxlim: 816   bits: 10/10
c ---[1785]---> Adder-cost: 1752   maxlim: 864   bits: 10/10
c ---[1783]---> BDD-cost:   95
c ---[1781]---> BDD-cost:   95
c ---[1779]---> BDD-cost:   95
c ---[1777]---> BDD-cost:   95
c ---[1775]---> BDD-cost:   95
c ---[1773]---> BDD-cost:   95
c ---[1771]---> BDD-cost:   95
c ---[1769]---> BDD-cost:   95
c ---[1767]---> BDD-cost:   95
c ---[1765]---> BDD-cost:   95
c ---[1763]---> BDD-cost:   95
c ---[1761]---> BDD-cost:   95
c ---[1759]---> BDD-cost:   95
c ---[1757]---> BDD-cost:   95
c ---[1755]---> BDD-cost:   95
c ---[1753]---> BDD-cost:   95
c ---[1751]---> BDD-cost:   95
c ---[1749]---> BDD-cost:   95
c ---[1747]---> BDD-cost:   95
c ---[1745]---> BDD-cost:   95
c ---[1743]---> BDD-cost:   95
c ---[1741]---> BDD-cost:   95
c ---[1739]---> BDD-cost:   95
c ---[1737]---> BDD-cost:   95
c ---[1735]---> BDD-cost:   95
c ---[1733]---> BDD-cost:   95
c ---[1731]---> BDD-cost:   95
c ---[1729]---> BDD-cost:   95
c ---[1727]---> BDD-cost:   95
c ---[1725]---> BDD-cost:   95
c ---[1723]---> BDD-cost:   95
c ---[1721]---> BDD-cost:   95
c ---[1719]---> BDD-cost:   95
c ---[1717]---> BDD-cost:   95
c ---[1715]---> BDD-cost:   95
c ---[1714]---> BDD-cost:   67
c ---[1713]---> BDD-cost:   67
c ---[1712]---> BDD-cost:   67
c ---[1711]---> BDD-cost:   67
c ---[1710]---> BDD-cost:   67
c ---[1709]---> BDD-cost:   67
c ---[1708]---> BDD-cost:   67
c ---[1707]---> BDD-cost:   67
c ---[1706]---> BDD-cost:   67
c ---[1705]---> BDD-cost:   67
c ---[1704]---> BDD-cost:   67
c ---[1703]---> BDD-cost:   67
c ---[1702]---> BDD-cost:   67
c ---[1701]---> BDD-cost:   67
c ---[1700]---> BDD-cost:   67
c ---[1699]---> BDD-cost:   67
c ---[1698]---> BDD-cost:   67
c ---[1697]---> BDD-cost:   67
c ---[1696]---> BDD-cost:   67
c ---[1695]---> BDD-cost:   67
c ---[1694]---> BDD-cost:   67
c ---[1693]---> BDD-cost:   67
c ---[1692]---> BDD-cost:   67
c ---[1691]---> BDD-cost:   67
c ---[1690]---> BDD-cost:   67
c ---[1689]---> BDD-cost:   67
c ---[1688]---> BDD-cost:   67
c ---[1687]---> BDD-cost:   67
c ---[1686]---> BDD-cost:   67
c ---[1685]---> BDD-cost:   67
c ---[1684]---> BDD-cost:   67
c ---[1683]---> BDD-cost:   67
c ---[1682]---> BDD-cost:   67
c ---[1681]---> BDD-cost:   67
c ---[1680]---> BDD-cost:   67
c ---[1679]---> BDD-cost:   67
c ---[1678]---> BDD-cost:   67
c ---[1677]---> BDD-cost:   67
c ---[1676]---> BDD-cost:   67
c ---[1675]---> BDD-cost:   67
c ---[1674]---> BDD-cost:   67
c ---[1673]---> BDD-cost:   67
c ---[1672]---> BDD-cost:   67
c ---[1671]---> BDD-cost:   67
c ---[1670]---> BDD-cost:   67
c ---[1669]---> BDD-cost:   67
c ---[1668]---> BDD-cost:   67
c ---[1667]---> BDD-cost:   67
c ---[1666]---> BDD-cost:   67
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |   73107   227153 |   21932       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/23310          
c   -- var.elim.:  2000/23310          
c   -- var.elim.:  3000/23310          
c   -- var.elim.:  4000/23310          
c   -- var.elim.:  5000/23310          
c   -- var.elim.:  6000/23310          
c   -- var.elim.:  7000/23310          
c   -- var.elim.:  8000/23310          
c   -- var.elim.:  9000/23310          
c   -- var.elim.:  10000/23310          
c   -- var.elim.:  11000/23310          
c   -- var.elim.:  12000/23310          
c   -- var.elim.:  13000/23310          
c   -- var.elim.:  14000/23310          
c   -- var.elim.:  15000/23310          
c   -- var.elim.:  16000/23310          
c   -- var.elim.:  17000/23310          
c   -- var.elim.:  18000/23310          
c   -- var.elim.:  19000/23310          
c   -- var.elim.:  20000/23310          
c   -- var.elim.:  21000/23310          
c   -- var.elim.:  22000/23310          
c   -- var.elim.:  23000/23310          
c   -- var.elim.:  23310/23310          
c   -- var.elim.:  1000/1906          
c   -- var.elim.:  1906/1906          
c   -- subsuming                       
c   -- var.elim.:  1000/1278          
c   -- var.elim.:  1278/1278          
c   -- var.elim.:  1000/1267          
c   -- var.elim.:  1267/1267          
c   -- subsuming                       
c   -- var.elim.:  494/494          
c   -- var.elim.:  245/245          
c   -- subsuming                       
c   -- var.elim.:  245/245          
c |         0 |   70903   219836 |      --       0       --      -- |     --   | -2130/-6325
c |         0 |   70903   219836 |   28361       0        0     nan |  0.000 % |
c |       102 |   70903   219836 |   31197     102    12497   122.5 |  1.657 % |
c |       255 |   70903   219836 |   34317     255    22168    86.9 |  1.657 % |
c |       480 |   70903   219836 |   37748     480    41560    86.6 |  1.657 % |
c |       818 |   70903   219836 |   41523     818    86203   105.4 |  1.657 % |
c ==============================================================================
c (current CPU-time: 4.29635 s)
c ==============================================================================
c [1mFound solution: -12[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost: 2744     Base:
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      1034 |   73514   226014 |   22054    1034   105496   102.0 |  1.657 % |
c   -- subsuming                       
c   -- var.elim.:  1000/1841          
c   -- var.elim.:  1841/1841          
c   -- var.elim.:  961/961          
c   -- subsuming                       
c   -- var.elim.:  789/789          
c   -- var.elim.:  152/152          
c |      1034 |   72648   229502 |      --    1034       --      -- |     --   | -862/3500
c |      1034 |   72648   229502 |   29059    1034   105496   102.0 |  1.657 % |
c |      1136 |   72648   229502 |   31965    1136   109036    96.0 |  1.619 % |
c ==============================================================================
c (current CPU-time: 5.62714 s)
c ==============================================================================
c [1mFound solution: -15[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      1248 |   73622   232397 |   22086    1248   116603    93.4 |  1.619 % |
c   -- subsuming                       
c   -- var.elim.:  1000/1837          
c   -- var.elim.:  1837/1837          
c   -- var.elim.:  958/958          
c |      1248 |   72746   232268 |      --    1248       --      -- |     --   | -876/-128
c |      1248 |   72746   232268 |   29098    1248   116603    93.4 |  1.619 % |
c |      1351 |   72746   232268 |   32008    1351   121679    90.1 |  1.621 % |
c |      1502 |   72746   232268 |   35209    1502   135537    90.2 |  1.621 % |
c |      1730 |   72746   232268 |   38729    1730   156468    90.4 |  1.621 % |
c |      2067 |   72746   232268 |   42602    2067   187235    90.6 |  1.621 % |
c |      2577 |   72746   232268 |   46863    2577   246616    95.7 |  1.621 % |
c |      3339 |   72746   232268 |   51549    3339   333857   100.0 |  1.621 % |
c ==============================================================================
c (current CPU-time: 12.6291 s)
c ==============================================================================
c [1mFound solution: -16[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      4023 |   73120   233426 |   21935    4023   419357   104.2 |  1.621 % |
c   -- subsuming                       
c   -- var.elim.:  1000/1289          
c   -- var.elim.:  1289/1289          
c   -- var.elim.:  473/473          
c |      4023 |   72738   231487 |      --    4023       --      -- |     --   | -366/-286
c |      4023 |   72738   231487 |   29095    3970   390077    98.3 |  1.621 % |
c |      4124 |   72738   231487 |   32004    4071   397345    97.6 |  1.633 % |
c |      4275 |   72738   231487 |   35205    4222   420694    99.6 |  1.633 % |
c |      4501 |   72738   231487 |   38725    4448   435652    97.9 |  1.633 % |
c |      4839 |   72738   231487 |   42598    4786   531886   111.1 |  1.634 % |
c |      5346 |   72738   231487 |   46858    5293   594518   112.3 |  1.633 % |
c ==============================================================================
c (current CPU-time: 18.0453 s)
c ==============================================================================
c [1mFound solution: -17[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      6017 |   73081   232522 |   21924    5964   793013   133.0 |  1.633 % |
c   -- subsuming                       
c   -- var.elim.:  948/948          
c   -- var.elim.:  362/362          
c |      6017 |   72770   232170 |      --    5964       --      -- |     --   | -311/-351
c |      6017 |   72770   232170 |   29108    5964   793013   133.0 |  1.633 % |
c |      6118 |   72770   232170 |   32018    6065   801108   132.1 |  1.637 % |
c |      6270 |   72770   232170 |   35220    6217   811426   130.5 |  1.637 % |
c |      6496 |   72770   232170 |   38742    6443   841843   130.7 |  1.637 % |
c |      6836 |   72770   232170 |   42617    6783   882712   130.1 |  1.637 % |
c |      7342 |   72770   232170 |   46878    7289   965313   132.4 |  1.637 % |
c |      8103 |   72770   232170 |   51566    8050  1052595   130.8 |  1.637 % |
c |      9242 |   72770   232170 |   56723    9189  1269609   138.2 |  1.637 % |
c |     10951 |   72770   232170 |   62395   10898  1575974   144.6 |  1.637 % |
c |     13514 |   72770   232170 |   68635   13461  2464067   183.1 |  1.637 % |
c ==============================================================================
c (current CPU-time: 50.5133 s)
c ==============================================================================
c [1mFound solution: -18[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     17246 |   72897   232552 |   21869   17193  3086712   179.5 |  1.637 % |
c   -- subsuming                       
c   -- var.elim.:  675/675          
c   -- var.elim.:  181/181          
c |     17246 |   72761   231431 |      --   17193       --      -- |     --   | -122/-245
c |     17246 |   72761   231431 |   29104   16119  2398781   148.8 |  1.637 % |
c |     17347 |   72761   231431 |   32014   16220  2410050   148.6 |  1.654 % |
c |     17497 |   72761   231431 |   35216   16370  2435208   148.8 |  1.654 % |
c |     17723 |   72761   231431 |   38737   16596  2454865   147.9 |  1.654 % |
c |     18061 |   72761   231431 |   42611   16934  2566301   151.5 |  1.654 % |
c |     18567 |   72761   231431 |   46872   17440  2678894   153.6 |  1.654 % |
c |     19326 |   72761   231431 |   51560   18199  2797834   153.7 |  1.654 % |
c |     20467 |   72761   231431 |   56716   19340  3249336   168.0 |  1.654 % |
c |     22177 |   72761   231431 |   62387   21050  3832947   182.1 |  1.654 % |
c |     24739 |   72761   231431 |   68626   23612  5087448   215.5 |  1.654 % |
c |     28583 |   72761   231431 |   75489   27456  5987186   218.1 |  1.654 % |
c |     34349 |   72761   231431 |   83038   33222  7426733   223.5 |  1.654 % |
c |     42998 |   72761   231431 |   91342   41871 12095550   288.9 |  1.654 % |
c ==============================================================================
c (current CPU-time: 189.022 s)
c ==============================================================================
c [1mFound solution: -19[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     49139 |   73288   232992 |   21986   48012 15141993   315.4 |  1.654 % |
c   -- subsuming                       
c   -- var.elim.:  986/986          
c   -- var.elim.:  518/518          
c |     49139 |   72827   232651 |      --   48012       --      -- |     --   | -461/-340
c |     49139 |   72827   232651 |   29130   48012 15141993   315.4 |  1.654 % |
c |     49242 |   72827   232651 |   32043   14537  6181975   425.3 |  1.657 % |
c |     49394 |   72827   232651 |   35248   14689  6196414   421.8 |  1.657 % |
c |     49621 |   72827   232651 |   38773   14916  6234084   417.9 |  1.657 % |
c |     49962 |   72827   232651 |   42650   15257  6269470   410.9 |  1.657 % |
c |     50472 |   72827   232651 |   46915   15767  6335291   401.8 |  1.657 % |
c |     51231 |   72827   232651 |   51606   16526  6468034   391.4 |  1.657 % |
c |     52371 |   72827   232651 |   56767   17666  6881394   389.5 |  1.657 % |
c |     54081 |   72827   232651 |   62444   19376  7441674   384.1 |  1.657 % |
c |     56643 |   72827   232651 |   68688   21938  7843835   357.5 |  1.657 % |
c ==============================================================================
c (current CPU-time: 221.482 s)
c ==============================================================================
c [1mFound solution: -20[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     58693 |   72842   232713 |   21852   23988  8474508   353.3 |  1.657 % |
c   -- subsuming                       
c   -- var.elim.:  512/512          
c   -- var.elim.:  62/62          
c |     58693 |   72806   232260 |      --   23988       --      -- |     --   | -18/-268
c |     58693 |   72806   232260 |   29122   20799  5914138   284.3 |  1.657 % |
c |     58794 |   72806   232260 |   32034   20900  5924498   283.5 |  1.678 % |
c |     58945 |   72806   232260 |   35238   21051  5940893   282.2 |  1.678 % |
c |     59170 |   72806   232260 |   38761   21276  5981871   281.2 |  1.678 % |
c |     59507 |   72806   232260 |   42638   21613  6016060   278.4 |  1.678 % |
c |     60013 |   72806   232260 |   46901   22119  6121059   276.7 |  1.678 % |
c |     60773 |   72806   232260 |   51592   22879  6321165   276.3 |  1.678 % |
c |     61914 |   72806   232260 |   56751   24020  6548597   272.6 |  1.678 % |
c |     63622 |   72806   232260 |   62426   25728  7296851   283.6 |  1.678 % |
c |     66187 |   72806   232260 |   68669   28293  8512397   300.9 |  1.678 % |
c |     70032 |   72806   232260 |   75536   32138  9709640   302.1 |  1.678 % |
c |     75798 |   72806   232260 |   83089   37904 11383410   300.3 |  1.678 % |
c |     84448 |   72806   232260 |   91398   46554 15469685   332.3 |  1.678 % |
c ==============================================================================
c (current CPU-time: 339.955 s)
c ==============================================================================
c [1mFound solution: -21[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     86487 |   72874   232454 |   21862   48593 16190131   333.2 |  1.678 % |
c   -- subsuming                       
c   -- var.elim.:  110/110          
c   -- var.elim.:  72/72          
c |     86487 |   72842   232502 |      --   48593       --      -- |     --   | -32/49
c |     86487 |   72842   232502 |   29136   48593 16190131   333.2 |  1.678 % |
c |     86588 |   72842   232502 |   32050   15774  5133206   325.4 |  1.682 % |
c |     86740 |   72842   232502 |   35255   15926  5151375   323.5 |  1.682 % |
c |     86966 |   72842   232502 |   38781   16152  5218814   323.1 |  1.682 % |
c |     87305 |   72842   232502 |   42659   16491  5265785   319.3 |  1.682 % |
c |     87813 |   72842   232502 |   46925   16999  5364595   315.6 |  1.682 % |
c |     88572 |   72842   232502 |   51617   17758  5548266   312.4 |  1.682 % |
c |     89717 |   72842   232502 |   56779   18903  5857842   309.9 |  1.682 % |
c |     91426 |   72842   232502 |   62457   20612  6559228   318.2 |  1.682 % |
c |     93990 |   72842   232502 |   68703   23176  7472895   322.4 |  1.682 % |
c |     97835 |   72842   232502 |   75573   27021  9442764   349.5 |  1.682 % |
c |    103601 |   72842   232502 |   83130   32787 11952268   364.5 |  1.682 % |
c |    112250 |   72842   232502 |   91443   41436 15456121   373.0 |  1.682 % |
c |    125226 |   72842   232502 |  100588   54412 23076171   424.1 |  1.682 % |
c |    144690 |   72842   232502 |  110646   73876 35052620   474.5 |  1.682 % |
c |    173882 |   72842   232502 |  121711  103068 50032330   485.4 |  1.682 % |
c ==============================================================================
c (current CPU-time: 858.007 s)
c ==============================================================================
c [1mFound solution: -22[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    174316 |   72852   232534 |   21855  103502 50116639   484.2 |  1.682 % |
c   -- subsuming                       
c   -- var.elim.:  461/461          
c   -- var.elim.:  64/64          
c |    174316 |   72832   232052 |      --  103502       --      -- |     --   | -3/109
c |    174316 |   72832   232052 |   29132   86202 34933409   405.3 |  1.682 % |
c |    174417 |   72832   232052 |   32046   16659  3378465   202.8 |  1.703 % |
c |    174569 |   72832   232052 |   35250   16811  3443668   204.8 |  1.703 % |
c |    174797 |   72832   232052 |   38775   17039  3520878   206.6 |  1.703 % |
c |    175135 |   72832   232052 |   42653   17377  3552509   204.4 |  1.703 % |
c |    175642 |   72832   232052 |   46918   17884  3651203   204.2 |  1.703 % |
c |    176402 |   72832   232052 |   51610   18644  3912186   209.8 |  1.703 % |
c |    177543 |   72832   232052 |   56771   19785  4320295   218.4 |  1.703 % |
c |    179252 |   72832   232052 |   62448   21494  4827429   224.6 |  1.703 % |
c |    181814 |   72832   232052 |   68693   24056  5858609   243.5 |  1.703 % |
c |    185658 |   72832   232052 |   75562   27900  7242915   259.6 |  1.703 % |
c |    191424 |   72832   232052 |   83119   33666 10030636   297.9 |  1.703 % |
c |    200074 |   72832   232052 |   91431   42316 14658225   346.4 |  1.703 % |
c |    213048 |   72832   232052 |  100574   55290 19279975   348.7 |  1.703 % |
c |    232509 |   72832   232052 |  110631   74751 31268501   418.3 |  1.703 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v -N_0x23_1_0x23_2_bit0 -N_0x23_2_0x23_3_bit0 -N_0x23_3_0x23_4_bit0 -N_0x23_4_0x23_5_bit0 -N_0x23_5_0x23_6_bit0 -N_0x23_6_0x23_7_bit0 -N_0x23_8_0x23_9_bit0 N_0x23_9_0x23_10_bit0 -N_0x23_10_0x23_11_bit0 -N_0x23_11_0x23_12_bit0 -N_0x23_12_0x23_13_bit0 -N_0x23_13_0x23_14_bit0 -N_0x23_15_0x23_16_bit0 -N_0x23_16_0x23_17_bit0 -N_0x23_17_0x23_18_bit0 -N_0x23_18_0x23_19_bit0 -N_0x23_19_0x23_20_bit0 N_0x23_20_0x23_21_bit0 -N_0x23_22_0x23_23_bit0 N_0x23_23_0x23_24_bit0 N_0x23_24_0x23_25_bit0 -N_0x23_25_0x23_26_bit0 -N_0x23_26_0x23_27_bit0 -N_0x23_27_0x23_28_bit0 -N_0x23_29_0x23_30_bit0 N_0x23_30_0x23_31_bit0 N_0x23_31_0x23_32_bit0 N_0x23_32_0x23_33_bit0 -N_0x23_33_0x23_34_bit0 -N_0x23_34_0x23_35_bit0 -N_0x23_36_0x23_37_bit0 -N_0x23_37_0x23_38_bit0 -N_0x23_38_0x23_39_bit0 -N_0x23_39_0x23_40_bit0 -N_0x23_40_0x23_41_bit0 -N_0x23_41_0x23_42_bit0 -N_0x23_43_0x23_44_bit0 -N_0x23_44_0x23_45_bit0 -N_0x23_45_0x23_46_bit0 -N_0x23_46_0x23_47_bit0 -N_0x23_47_0x23_48_bit0 -N_0x23_48_0x23_49_bit0 -N_0x23_1_0x23_8_bit0 -N_0x23_2_0x23_9_bit0 -N_0x23_3_0x23_10_bit0 -N_0x23_4_0x23_11_bit0 -N_0x23_5_0x23_12_bit0 -N_0x23_6_0x23_13_bit0 -N_0x23_7_0x23_14_bit0 -N_0x23_8_0x23_15_bit0 -N_0x23_9_0x23_16_bit0 N_0x23_10_0x23_17_bit0 -N_0x23_11_0x23_18_bit0 -N_0x23_12_0x23_19_bit0 -N_0x23_13_0x23_20_bit0 -N_0x23_14_0x23_21_bit0 -N_0x23_15_0x23_22_bit0 -N_0x23_16_0x23_23_bit0 N_0x23_17_0x23_24_bit0 -N_0x23_18_0x23_25_bit0 -N_0x23_19_0x23_26_bit0 N_0x23_20_0x23_27_bit0 -N_0x23_21_0x23_28_bit0 -N_0x23_22_0x23_29_bit0 N_0x23_23_0x23_30_bit0 N_0x23_24_0x23_31_bit0 N_0x23_25_0x23_32_bit0 -N_0x23_26_0x23_33_bit0 -N_0x23_27_0x23_34_bit0 -N_0x23_28_0x23_35_bit0 -N_0x23_29_0x23_36_bit0 -N_0x23_30_0x23_37_bit0 N_0x23_31_0x23_38_bit0 -N_0x23_32_0x23_39_bit0 -N_0x23_33_0x23_40_bit0 -N_0x23_34_0x23_41_bit0 -N_0x23_35_0x23_42_bit0 -N_0x23_36_0x23_43_bit0 -N_0x23_37_0x23_44_bit0 N_0x23_38_0x23_45_bit0 -N_0x23_39_0x23_46_bit0 -N_0x23_40_0x23_47_bit0 -N_0x23_41_0x23_48_bit0 -N_0x23_42_0x23_49_bit0 -N_0x23_1_0x23_9_bit0 -N_0x23_2_0x23_10_bit0 -N_0x23_3_0x23_11_bit0 -N_0x23_4_0x23_12_bit0 -N_0x23_5_0x23_13_bit0 -N_0x23_6_0x23_14_bit0 -N_0x23_8_0x23_16_bit0 N_0x23_9_0x23_17_bit0 -N_0x23_10_0x23_18_bit0 -N_0x23_11_0x23_19_bit0 -N_0x23_12_0x23_20_bit0 -N_0x23_13_0x23_21_bit0 -N_0x23_15_0x23_23_bit0 -N_0x23_16_0x23_24_bit0 N_0x23_17_0x23_25_bit0 -N_0x23_18_0x23_26_bit0 -N_0x23_19_0x23_27_bit0 -N_0x23_20_0x23_28_bit0 -N_0x23_22_0x23_30_bit0 N_0x23_23_0x23_31_bit0 N_0x23_24_0x23_32_bit0 N_0x23_25_0x23_33_bit0 -N_0x23_26_0x23_34_bit0 N_0x23_27_0x23_35_bit0 -N_0x23_29_0x23_37_bit0 N_0x23_30_0x23_38_bit0 -N_0x23_31_0x23_39_bit0 -N_0x23_32_0x23_40_bit0 -N_0x23_33_0x23_41_bit0 -N_0x23_34_0x23_42_bit0 -N_0x23_36_0x23_44_bit0 -N_0x23_37_0x23_45_bit0 -N_0x23_38_0x23_46_bit0 -N_0x23_39_0x23_47_bit0 -N_0x23_40_0x23_48_bit0 -N_0x23_41_0x23_49_bit0 -x_0x23_49_0x23_34_bit0 -x_0x23_49_0x23_32_bit0 -x_0x23_49_0x23_30_bit0 -x_0x23_49_0x23_29_bit0 -x_0x23_49_0x23_27_bit0 -x_0x23_49_0x23_26_bit0 -x_0x23_49_0x23_23_bit0 -x_0x23_49_0x23_20_bit0 -x_0x23_49_0x23_18_bit0 -x_0x23_49_0x23_16_bit0 -x_0x23_49_0x23_13_bit0 -x_0x23_49_0x23_11_bit0 -x_0x23_49_0x23_9_bit0 -x_0x23_49_0x23_8_bit0 -x_0x23_49_0x23_6_bit0 -x_0x23_49_0x23_3_bit0 -x_0x23_49_0x23_1_bit0 -x_0x23_48_0x23_34_bit0 -x_0x23_48_0x23_32_bit0 -x_0x23_48_0x23_30_bit0 -x_0x23_48_0x23_29_bit0 -x_0x23_48_0x23_27_bit0 -x_0x23_48_0x23_26_bit0 x_0x23_48_0x23_23_bit0 -x_0x23_48_0x23_20_bit0 -x_0x23_48_0x23_18_bit0 -x_0x23_48_0x23_16_bit0 -x_0x23_48_0x23_13_bit0 -x_0x23_48_0x23_11_bit0 -x_0x23_48_0x23_9_bit0 -x_0x23_48_0x23_8_bit0 -x_0x23_48_0x23_6_bit0 -x_0x23_48_0x23_3_bit0 -x_0x23_48_0x23_1_bit0 -x_0x23_47_0x23_34_bit0 -x_0x23_47_0x23_32_bit0 -x_0x23_47_0x23_30_bit0 -x_0x23_47_0x23_29_bit0 -x_0x23_47_0x23_27_bit0 -x_0x23_47_0x23_26_bit0 -x_0x23_47_0x23_23_bit0 -x_0x23_47_0x23_20_bit0 -x_0x23_47_0x23_18_bit0 -x_0x23_47_0x23_16_bit0 -x_0x23_47_0x23_13_bit0 -x_0x23_47_0x23_11_bit0 -x_0x23_47_0x23_9_bit0 -x_0x23_47_0x23_8_bit0 -x_0x23_47_0x23_6_bit0 -x_0x23_47_0x23_3_bit0 -x_0x23_47_0x23_1_bit0 -x_0x23_46_0x23_34_bit0 -x_0x23_46_0x23_32_bit0 -x_0x23_46_0x23_30_bit0 -x_0x23_46_0x23_29_bit0 -x_0x23_46_0x23_27_bit0 -x_0x23_46_0x23_26_bit0 -x_0x23_46_0x23_23_bit0 -x_0x23_46_0x23_20_bit0 -x_0x23_46_0x23_18_bit0 -x_0x23_46_0x23_16_bit0 -x_0x23_46_0x23_13_bit0 -x_0x23_46_0x23_11_bit0 -x_0x23_46_0x23_9_bit0 -x_0x23_46_0x23_8_bit0 -x_0x23_46_0x23_6_bit0 -x_0x23_46_0x23_3_bit0 -x_0x23_46_0x23_1_bit0 -x_0x23_45_0x23_34_bit0 -x_0x23_45_0x23_32_bit0 -x_0x23_45_0x23_30_bit0 -x_0x23_45_0x23_29_bit0 -x_0x23_45_0x23_27_bit0 x_0x23_45_0x23_26_bit0 -x_0x23_45_0x23_23_bit0 -x_0x23_45_0x23_20_bit0 -x_0x23_45_0x23_18_bit0 -x_0x23_45_0x23_16_bit0 -x_0x23_45_0x23_13_bit0 -x_0x23_45_0x23_11_bit0 -x_0x23_45_0x23_9_bit0 -x_0x23_45_0x23_8_bit0 -x_0x23_45_0x23_6_bit0 -x_0x23_45_0x23_3_bit0 -x_0x23_45_0x23_1_bit0 -x_0x23_44_0x23_34_bit0 -x_0x23_44_0x23_32_bit0 -x_0x23_44_0x23_30_bit0 -x_0x23_44_0x23_29_bit0 -x_0x23_44_0x23_27_bit0 -x_0x23_44_0x23_26_bit0 -x_0x23_44_0x23_23_bit0 -x_0x23_44_0x23_20_bit0 -x_0x23_44_0x23_18_bit0 -x_0x23_44_0x23_16_bit0 -x_0x23_44_0x23_13_bit0 -x_0x23_44_0x23_11_bit0 -x_0x23_44_0x23_9_bit0 -x_0x23_44_0x23_8_bit0 -x_0x23_44_0x23_6_bit0 -x_0x23_44_0x23_3_bit0 -x_0x23_44_0x23_1_bit0 -x_0x23_43_0x23_34_bit0 -x_0x23_43_0x23_32_bit0 -x_0x23_43_0x23_30_bit0 -x_0x23_43_0x23_29_bit0 -x_0x23_43_0x23_27_bit0 -x_0x23_43_0x23_26_bit0 -x_0x23_43_0x23_23_bit0 -x_0x23_43_0x23_20_bit0 -x_0x23_43_0x23_18_bit0 -x_0x23_43_0x23_16_bit0 -x_0x23_43_0x23_13_bit0 -x_0x23_43_0x23_11_bit0 -x_0x23_43_0x23_9_bit0 -x_0x23_43_0x23_8_bit0 -x_0x23_43_0x23_6_bit0 -x_0x23_43_0x23_3_bit0 -x_0x23_43_0x23_1_bit0 -x_0x23_42_0x23_34_bit0 -x_0x23_42_0x23_32_bit0 -x_0x23_42_0x23_30_bit0 -x_0x23_42_0x23_29_bit0 -x_0x23_42_0x23_27_bit0 -x_0x23_42_0x23_26_bit0 -x_0x23_42_0x23_23_bit0 -x_0x23_42_0x23_20_bit0 -x_0x23_42_0x23_18_bit0 -x_0x23_42_0x23_16_bit0 -x_0x23_42_0x23_13_bit0 -x_0x23_42_0x23_11_bit0 -x_0x23_42_0x23_9_bit0 -x_0x23_42_0x23_8_bit0 -x_0x23_42_0x23_6_bit0 -x_0x23_42_0x23_3_bit0 -x_0x23_42_0x23_1_bit0 -x_0x23_41_0x23_34_bit0 -x_0x23_41_0x23_32_bit0 -x_0x23_41_0x23_30_bit0 -x_0x23_41_0x23_29_bit0 -x_0x23_41_0x23_27_bit0 -x_0x23_41_0x23_26_bit0 -x_0x23_41_0x23_23_bit0 -x_0x23_41_0x23_20_bit0 -x_0x23_41_0x23_18_bit0 -x_0x23_41_0x23_16_bit0 -x_0x23_41_0x23_13_bit0 -x_0x23_41_0x23_11_bit0 -x_0x23_41_0x23_9_bit0 -x_0x23_41_0x23_8_bit0 -x_0x23_41_0x23_6_bit0 -x_0x23_41_0x23_3_bit0 -x_0x23_41_0x23_1_bit0 -x_0x23_40_0x23_34_bit0 -x_0x23_40_0x23_32_bit0 -x_0x23_40_0x23_30_bit0 -x_0x23_40_0x23_29_bit0 -x_0x23_40_0x23_27_bit0 -x_0x23_40_0x23_26_bit0 -x_0x23_40_0x23_23_bit0 -x_0x23_40_0x23_20_bit0 -x_0x23_40_0x23_18_bit0 -x_0x23_40_0x23_16_bit0 -x_0x23_40_0x23_13_bit0 -x_0x23_40_0x23_11_bit0 -x_0x23_40_0x23_9_bit0 -x_0x23_40_0x23_8_bit0 -x_0x23_40_0x23_6_bit0 -x_0x23_40_0x23_3_bit0 -x_0x23_40_0x23_1_bit0 -x_0x23_39_0x23_34_bit0 -x_0x23_39_0x23_32_bit0 -x_0x23_39_0x23_30_bit0 -x_0x23_39_0x23_29_bit0 -x_0x23_39_0x23_27_bit0 -x_0x23_39_0x23_26_bit0 -x_0x23_39_0x23_23_bit0 -x_0x23_39_0x23_20_bit0 -x_0x23_39_0x23_18_bit0 -x_0x23_39_0x23_16_bit0 -x_0x23_39_0x23_13_bit0 -x_0x23_39_0x23_11_bit0 -x_0x23_39_0x23_9_bit0 -x_0x23_39_0x23_8_bit0 -x_0x23_39_0x23_6_bit0 -x_0x23_39_0x23_3_bit0 -x_0x23_39_0x23_1_bit0 -x_0x23_38_0x23_34_bit0 -x_0x23_38_0x23_32_bit0 -x_0x23_38_0x23_30_bit0 -x_0x23_38_0x23_29_bit0 x_0x23_38_0x23_27_bit0 -x_0x23_38_0x23_26_bit0 -x_0x23_38_0x23_23_bit0 -x_0x23_38_0x23_20_bit0 -x_0x23_38_0x23_18_bit0 -x_0x23_38_0x23_16_bit0 -x_0x23_38_0x23_13_bit0 -x_0x23_38_0x23_11_bit0 -x_0x23_38_0x23_9_bit0 -x_0x23_38_0x23_8_bit0 -x_0x23_38_0x23_6_bit0 -x_0x23_38_0x23_3_bit0 -x_0x23_38_0x23_1_bit0 -x_0x23_37_0x23_34_bit0 -x_0x23_37_0x23_32_bit0 -x_0x23_37_0x23_30_bit0 -x_0x23_37_0x23_29_bit0 -x_0x23_37_0x23_27_bit0 -x_0x23_37_0x23_26_bit0 -x_0x23_37_0x23_23_bit0 -x_0x23_37_0x23_20_bit0 -x_0x23_37_0x23_18_bit0 -x_0x23_37_0x23_16_bit0 -x_0x23_37_0x23_13_bit0 -x_0x23_37_0x23_11_bit0 -x_0x23_37_0x23_9_bit0 -x_0x23_37_0x23_8_bit0 -x_0x23_37_0x23_6_bit0 -x_0x23_37_0x23_3_bit0 -x_0x23_37_0x23_1_bit0 -x_0x23_36_0x23_34_bit0 -x_0x23_36_0x23_32_bit0 -x_0x23_36_0x23_30_bit0 -x_0x23_36_0x23_29_bit0 -x_0x23_36_0x23_27_bit0 -x_0x23_36_0x23_26_bit0 -x_0x23_36_0x23_23_bit0 -x_0x23_36_0x23_20_bit0 -x_0x23_36_0x23_18_bit0 -x_0x23_36_0x23_16_bit0 -x_0x23_36_0x23_13_bit0 -x_0x23_36_0x23_11_bit0 -x_0x23_36_0x23_9_bit0 -x_0x23_36_0x23_8_bit0 -x_0x23_36_0x23_6_bit0 -x_0x23_36_0x23_3_bit0 -x_0x23_36_0x23_1_bit0 -x_0x23_35_0x23_34_bit0 -x_0x23_35_0x23_32_bit0 -x_0x23_35_0x23_30_bit0 -x_0x23_35_0x23_29_bit0 -x_0x23_35_0x23_27_bit0 -x_0x23_35_0x23_26_bit0 -x_0x23_35_0x23_23_bit0 x_0x23_35_0x23_20_bit0 -x_0x23_35_0x23_18_bit0 -x_0x23_35_0x23_16_bit0 -x_0x23_35_0x23_13_bit0 -x_0x23_35_0x23_11_bit0 -x_0x23_35_0x23_9_bit0 -x_0x23_35_0x23_8_bit0 -x_0x23_35_0x23_6_bit0 -x_0x23_35_0x23_3_bit0 -x_0x23_35_0x23_1_bit0 -x_0x23_34_0x23_34_bit0 -x_0x23_34_0x23_32_bit0 -x_0x23_34_0x23_30_bit0 -x_0x23_34_0x23_29_bit0 -x_0x23_34_0x23_27_bit0 -x_0x23_34_0x23_26_bit0 -x_0x23_34_0x23_23_bit0 -x_0x23_34_0x23_20_bit0 -x_0x23_34_0x23_18_bit0 -x_0x23_34_0x23_16_bit0 -x_0x23_34_0x23_13_bit0 -x_0x23_34_0x23_11_bit0 -x_0x23_34_0x23_9_bit0 -x_0x23_34_0x23_8_bit0 -x_0x23_34_0x23_6_bit0 -x_0x23_34_0x23_3_bit0 -x_0x23_34_0x23_1_bit0 x_0x23_33_0x23_34_bit0 -x_0x23_33_0x23_32_bit0 -x_0x23_33_0x23_30_bit0 -x_0x23_33_0x23_29_bit0 -x_0x23_33_0x23_27_bit0 -x_0x23_33_0x23_26_bit0 -x_0x23_33_0x23_23_bit0 -x_0x23_33_0x23_20_bit0 -x_0x23_33_0x23_18_bit0 -x_0x23_33_0x23_16_bit0 -x_0x23_33_0x23_13_bit0 -x_0x23_33_0x23_11_bit0 -x_0x23_33_0x23_9_bit0 -x_0x23_33_0x23_8_bit0 -x_0x23_33_0x23_6_bit0 -x_0x23_33_0x23_3_bit0 -x_0x23_33_0x23_1_bit0 -x_0x23_32_0x23_34_bit0 x_0x23_32_0x23_32_bit0 -x_0x23_32_0x23_30_bit0 -x_0x23_32_0x23_29_bit0 -x_0x23_32_0x23_27_bit0 -x_0x23_32_0x23_26_bit0 -x_0x23_32_0x23_23_bit0 -x_0x23_32_0x23_20_bit0 -x_0x23_32_0x23_18_bit0 -x_0x23_32_0x23_16_bit0 -x_0x23_32_0x23_13_bit0 -x_0x23_32_0x23_11_bit0 -x_0x23_32_0x23_9_bit0 -x_0x23_32_0x23_8_bit0 -x_0x23_32_0x23_6_bit0 -x_0x23_32_0x23_3_bit0 -x_0x23_32_0x23_1_bit0 -x_0x23_31_0x23_34_bit0 -x_0x23_31_0x23_32_bit0 x_0x23_31_0x23_30_bit0 -x_0x23_31_0x23_29_bit0 -x_0x23_31_0x23_27_bit0 -x_0x23_31_0x23_26_bit0 -x_0x23_31_0x23_23_bit0 -x_0x23_31_0x23_20_bit0 -x_0x23_31_0x23_18_bit0 -x_0x23_31_0x23_16_bit0 -x_0x23_31_0x23_13_bit0 -x_0x23_31_0x23_11_bit0 -x_0x23_31_0x23_9_bit0 -x_0x23_31_0x23_8_bit0 -x_0x23_31_0x23_6_bit0 -x_0x23_31_0x23_3_bit0 -x_0x23_31_0x23_1_bit0 -x_0x23_30_0x23_34_bit0 -x_0x23_30_0x23_32_bit0 -x_0x23_30_0x23_30_bit0 x_0x23_30_0x23_29_bit0 -x_0x23_30_0x23_27_bit0 -x_0x23_30_0x23_26_bit0 -x_0x23_30_0x23_23_bit0 -x_0x23_30_0x23_20_bit0 -x_0x23_30_0x23_18_bit0 -x_0x23_30_0x23_16_bit0 -x_0x23_30_0x23_13_bit0 -x_0x23_30_0x23_11_bit0 -x_0x23_30_0x23_9_bit0 -x_0x23_30_0x23_8_bit0 -x_0x23_30_0x23_6_bit0 -x_0x23_30_0x23_3_bit0 -x_0x23_30_0x23_1_bit0 -x_0x23_29_0x23_34_bit0 -x_0x23_29_0x23_32_bit0 -x_0x23_29_0x23_30_bit0 -x_0x23_29_0x23_29_bit0 -x_0x23_29_0x23_27_bit0 -x_0x23_29_0x23_26_bit0 -x_0x23_29_0x23_23_bit0 -x_0x23_29_0x23_20_bit0 -x_0x23_29_0x23_18_bit0 -x_0x23_29_0x23_16_bit0 -x_0x23_29_0x23_13_bit0 -x_0x23_29_0x23_11_bit0 -x_0x23_29_0x23_9_bit0 -x_0x23_29_0x23_8_bit0 -x_0x23_29_0x23_6_bit0 -x_0x23_29_0x23_3_bit0 -x_0x23_29_0x23_1_bit0 -x_0x23_28_0x23_34_bit0 -x_0x23_28_0x23_32_bit0 -x_0x23_28_0x23_30_bit0 -x_0x23_28_0x23_29_bit0 -x_0x23_28_0x23_27_bit0 -x_0x23_28_0x23_26_bit0 -x_0x23_28_0x23_23_bit0 -x_0x23_28_0x23_20_bit0 -x_0x23_28_0x23_18_bit0 -x_0x23_28_0x23_16_bit0 -x_0x23_28_0x23_13_bit0 -x_0x23_28_0x23_11_bit0 -x_0x23_28_0x23_9_bit0 -x_0x23_28_0x23_8_bit0 -x_0x23_28_0x23_6_bit0 -x_0x23_28_0x23_3_bit0 -x_0x23_28_0x23_1_bit0 -x_0x23_27_0x23_34_bit0 -x_0x23_27_0x23_32_bit0 -x_0x23_27_0x23_30_bit0 -x_0x23_27_0x23_29_bit0 -x_0x23_27_0x23_27_bit0 -x_0x23_27_0x23_26_bit0 -x_0x23_27_0x23_23_bit0 -x_0x23_27_0x23_20_bit0 -x_0x23_27_0x23_18_bit0 -x_0x23_27_0x23_16_bit0 x_0x23_27_0x23_13_bit0 -x_0x23_27_0x23_11_bit0 -x_0x23_27_0x23_9_bit0 -x_0x23_27_0x23_8_bit0 -x_0x23_27_0x23_6_bit0 -x_0x23_27_0x23_3_bit0 -x_0x23_27_0x23_1_bit0 -x_0x23_26_0x23_34_bit0 -x_0x23_26_0x23_32_bit0 -x_0x23_26_0x23_30_bit0 -x_0x23_26_0x23_29_bit0 -x_0x23_26_0x23_27_bit0 -x_0x23_26_0x23_26_bit0 -x_0x23_26_0x23_23_bit0 -x_0x23_26_0x23_20_bit0 -x_0x23_26_0x23_18_bit0 -x_0x23_26_0x23_16_bit0 -x_0x23_26_0x23_13_bit0 -x_0x23_26_0x23_11_bit0 -x_0x23_26_0x23_9_bit0 -x_0x23_26_0x23_8_bit0 -x_0x23_26_0x23_6_bit0 -x_0x23_26_0x23_3_bit0 -x_0x23_26_0x23_1_bit0 -x_0x23_25_0x23_34_bit0 -x_0x23_25_0x23_32_bit0 -x_0x23_25_0x23_30_bit0 -x_0x23_25_0x23_29_bit0 -x_0x23_25_0x23_27_bit0 -x_0x23_25_0x23_26_bit0 -x_0x23_25_0x23_23_bit0 -x_0x23_25_0x23_20_bit0 -x_0x23_25_0x23_18_bit0 -x_0x23_25_0x23_16_bit0 -x_0x23_25_0x23_13_bit0 x_0x23_25_0x23_11_bit0 -x_0x23_25_0x23_9_bit0 -x_0x23_25_0x23_8_bit0 -x_0x23_25_0x23_6_bit0 -x_0x23_25_0x23_3_bit0 -x_0x23_25_0x23_1_bit0 -x_0x23_24_0x23_34_bit0 -x_0x23_24_0x23_32_bit0 -x_0x23_24_0x23_30_bit0 -x_0x23_24_0x23_29_bit0 -x_0x23_24_0x23_27_bit0 -x_0x23_24_0x23_26_bit0 -x_0x23_24_0x23_23_bit0 -x_0x23_24_0x23_20_bit0 -x_0x23_24_0x23_18_bit0 -x_0x23_24_0x23_16_bit0 -x_0x23_24_0x23_13_bit0 -x_0x23_24_0x23_11_bit0 -x_0x23_24_0x23_9_bit0 -x_0x23_24_0x23_8_bit0 -x_0x23_24_0x23_6_bit0 -x_0x23_24_0x23_3_bit0 x_0x23_24_0x23_1_bit0 -x_0x23_23_0x23_34_bit0 -x_0x23_23_0x23_32_bit0 -x_0x23_23_0x23_30_bit0 -x_0x23_23_0x23_29_bit0 -x_0x23_23_0x23_27_bit0 -x_0x23_23_0x23_26_bit0 -x_0x23_23_0x23_23_bit0 -x_0x23_23_0x23_20_bit0 -x_0x23_23_0x23_18_bit0 -x_0x23_23_0x23_16_bit0 -x_0x23_23_0x23_13_bit0 -x_0x23_23_0x23_11_bit0 -x_0x23_23_0x23_9_bit0 -x_0x23_23_0x23_8_bit0 -x_0x23_23_0x23_6_bit0 x_0x23_23_0x23_3_bit0 -x_0x23_23_0x23_1_bit0 -x_0x23_22_0x23_34_bit0 -x_0x23_22_0x23_32_bit0 -x_0x23_22_0x23_30_bit0 -x_0x23_22_0x23_29_bit0 -x_0x23_22_0x23_27_bit0 -x_0x23_22_0x23_26_bit0 -x_0x23_22_0x23_23_bit0 -x_0x23_22_0x23_20_bit0 -x_0x23_22_0x23_18_bit0 -x_0x23_22_0x23_16_bit0 -x_0x23_22_0x23_13_bit0 -x_0x23_22_0x23_11_bit0 -x_0x23_22_0x23_9_bit0 -x_0x23_22_0x23_8_bit0 -x_0x23_22_0x23_6_bit0 -x_0x23_22_0x23_3_bit0 -x_0x23_22_0x23_1_bit0 -x_0x23_21_0x23_34_bit0 -x_0x23_21_0x23_32_bit0 -x_0x23_21_0x23_30_bit0 -x_0x23_21_0x23_29_bit0 -x_0x23_21_0x23_27_bit0 -x_0x23_21_0x23_26_bit0 -x_0x23_21_0x23_23_bit0 -x_0x23_21_0x23_20_bit0 x_0x23_21_0x23_18_bit0 -x_0x23_21_0x23_16_bit0 -x_0x23_21_0x23_13_bit0 -x_0x23_21_0x23_11_bit0 -x_0x23_21_0x23_9_bit0 -x_0x23_21_0x23_8_bit0 -x_0x23_21_0x23_6_bit0 -x_0x23_21_0x23_3_bit0 -x_0x23_21_0x23_1_bit0 -x_0x23_20_0x23_34_bit0 -x_0x23_20_0x23_32_bit0 -x_0x23_20_0x23_30_bit0 -x_0x23_20_0x23_29_bit0 -x_0x23_20_0x23_27_bit0 -x_0x23_20_0x23_26_bit0 -x_0x23_20_0x23_23_bit0 -x_0x23_20_0x23_20_bit0 -x_0x23_20_0x23_18_bit0 x_0x23_20_0x23_16_bit0 -x_0x23_20_0x23_13_bit0 -x_0x23_20_0x23_11_bit0 -x_0x23_20_0x23_9_bit0 -x_0x23_20_0x23_8_bit0 -x_0x23_20_0x23_6_bit0 -x_0x23_20_0x23_3_bit0 -x_0x23_20_0x23_1_bit0 -x_0x23_19_0x23_34_bit0 -x_0x23_19_0x23_32_bit0 -x_0x23_19_0x23_30_bit0 -x_0x23_19_0x23_29_bit0 -x_0x23_19_0x23_27_bit0 -x_0x23_19_0x23_26_bit0 -x_0x23_19_0x23_23_bit0 -x_0x23_19_0x23_20_bit0 -x_0x23_19_0x23_18_bit0 -x_0x23_19_0x23_16_bit0 -x_0x23_19_0x23_13_bit0 -x_0x23_19_0x23_11_bit0 -x_0x23_19_0x23_9_bit0 -x_0x23_19_0x23_8_bit0 -x_0x23_19_0x23_6_bit0 -x_0x23_19_0x23_3_bit0 -x_0x23_19_0x23_1_bit0 -x_0x23_18_0x23_34_bit0 -x_0x23_18_0x23_32_bit0 -x_0x23_18_0x23_30_bit0 -x_0x23_18_0x23_29_bit0 -x_0x23_18_0x23_27_bit0 -x_0x23_18_0x23_26_bit0 -x_0x23_18_0x23_23_bit0 -x_0x23_18_0x23_20_bit0 -x_0x23_18_0x23_18_bit0 -x_0x23_18_0x23_16_bit0 -x_0x23_18_0x23_13_bit0 -x_0x23_18_0x23_11_bit0 -x_0x23_18_0x23_9_bit0 -x_0x23_18_0x23_8_bit0 -x_0x23_18_0x23_6_bit0 -x_0x23_18_0x23_3_bit0 -x_0x23_18_0x23_1_bit0 -x_0x23_17_0x23_34_bit0 -x_0x23_17_0x23_32_bit0 -x_0x23_17_0x23_30_bit0 -x_0x23_17_0x23_29_bit0 -x_0x23_17_0x23_27_bit0 -x_0x23_17_0x23_26_bit0 -x_0x23_17_0x23_23_bit0 -x_0x23_17_0x23_20_bit0 -x_0x23_17_0x23_18_bit0 -x_0x23_17_0x23_16_bit0 -x_0x23_17_0x23_13_bit0 -x_0x23_17_0x23_11_bit0 x_0x23_17_0x23_9_bit0 -x_0x23_17_0x23_8_bit0 -x_0x23_17_0x23_6_bit0 -x_0x23_17_0x23_3_bit0 -x_0x23_17_0x23_1_bit0 -x_0x23_16_0x23_34_bit0 -x_0x23_16_0x23_32_bit0 -x_0x23_16_0x23_30_bit0 -x_0x23_16_0x23_29_bit0 -x_0x23_16_0x23_27_bit0 -x_0x23_16_0x23_26_bit0 -x_0x23_16_0x23_23_bit0 -x_0x23_16_0x23_20_bit0 -x_0x23_16_0x23_18_bit0 -x_0x23_16_0x23_16_bit0 -x_0x23_16_0x23_13_bit0 -x_0x23_16_0x23_11_bit0 -x_0x23_16_0x23_9_bit0 -x_0x23_16_0x23_8_bit0 -x_0x23_16_0x23_6_bit0 -x_0x23_16_0x23_3_bit0 -x_0x23_16_0x23_1_bit0 -x_0x23_15_0x23_34_bit0 -x_0x23_15_0x23_32_bit0 -x_0x23_15_0x23_30_bit0 -x_0x23_15_0x23_29_bit0 -x_0x23_15_0x23_27_bit0 -x_0x23_15_0x23_26_bit0 -x_0x23_15_0x23_23_bit0 -x_0x23_15_0x23_20_bit0 -x_0x23_15_0x23_18_bit0 -x_0x23_15_0x23_16_bit0 -x_0x23_15_0x23_13_bit0 -x_0x23_15_0x23_11_bit0 -x_0x23_15_0x23_9_bit0 -x_0x23_15_0x23_8_bit0 -x_0x23_15_0x23_6_bit0 -x_0x23_15_0x23_3_bit0 -x_0x23_15_0x23_1_bit0 -x_0x23_14_0x23_34_bit0 -x_0x23_14_0x23_32_bit0 -x_0x23_14_0x23_30_bit0 -x_0x23_14_0x23_29_bit0 -x_0x23_14_0x23_27_bit0 -x_0x23_14_0x23_26_bit0 -x_0x23_14_0x23_23_bit0 -x_0x23_14_0x23_20_bit0 -x_0x23_14_0x23_18_bit0 -x_0x23_14_0x23_16_bit0 -x_0x23_14_0x23_13_bit0 -x_0x23_14_0x23_11_bit0 -x_0x23_14_0x23_9_bit0 -x_0x23_14_0x23_8_bit0 -x_0x23_14_0x23_6_bit0 -x_0x23_14_0x23_3_bit0 -x_0x23_14_0x23_1_bit0 -x_0x23_13_0x23_34_bit0 -x_0x23_13_0x23_32_bit0 -x_0x23_13_0x23_30_bit0 -x_0x23_13_0x23_29_bit0 -x_0x23_13_0x23_27_bit0 -x_0x23_13_0x23_26_bit0 -x_0x23_13_0x23_23_bit0 -x_0x23_13_0x23_20_bit0 -x_0x23_13_0x23_18_bit0 -x_0x23_13_0x23_16_bit0 -x_0x23_13_0x23_13_bit0 -x_0x23_13_0x23_11_bit0 -x_0x23_13_0x23_9_bit0 -x_0x23_13_0x23_8_bit0 -x_0x23_13_0x23_6_bit0 -x_0x23_13_0x23_3_bit0 -x_0x23_13_0x23_1_bit0 -x_0x23_12_0x23_34_bit0 -x_0x23_12_0x23_32_bit0 -x_0x23_12_0x23_30_bit0 -x_0x23_12_0x23_29_bit0 -x_0x23_12_0x23_27_bit0 -x_0x23_12_0x23_26_bit0 -x_0x23_12_0x23_23_bit0 -x_0x23_12_0x23_20_bit0 -x_0x23_12_0x23_18_bit0 -x_0x23_12_0x23_16_bit0 -x_0x23_12_0x23_13_bit0 -x_0x23_12_0x23_11_bit0 -x_0x23_12_0x23_9_bit0 -x_0x23_12_0x23_8_bit0 -x_0x23_12_0x23_6_bit0 -x_0x23_12_0x23_3_bit0 -x_0x23_12_0x23_1_bit0 -x_0x23_11_0x23_34_bit0 -x_0x23_11_0x23_32_bit0 -x_0x23_11_0x23_30_bit0 -x_0x23_11_0x23_29_bit0 -x_0x23_11_0x23_27_bit0 -x_0x23_11_0x23_26_bit0 -x_0x23_11_0x23_23_bit0 -x_0x23_11_0x23_20_bit0 -x_0x23_11_0x23_18_bit0 -x_0x23_11_0x23_16_bit0 -x_0x23_11_0x23_13_bit0 -x_0x23_11_0x23_11_bit0 -x_0x23_11_0x23_9_bit0 -x_0x23_11_0x23_8_bit0 -x_0x23_11_0x23_6_bit0 -x_0x23_11_0x23_3_bit0 -x_0x23_11_0x23_1_bit0 -x_0x23_10_0x23_34_bit0 -x_0x23_10_0x23_32_bit0 -x_0x23_10_0x23_30_bit0 -x_0x23_10_0x23_29_bit0 -x_0x23_10_0x23_27_bit0 -x_0x23_10_0x23_26_bit0 -x_0x23_10_0x23_23_bit0 -x_0x23_10_0x23_20_bit0 -x_0x23_10_0x23_18_bit0 -x_0x23_10_0x23_16_bit0 -x_0x23_10_0x23_13_bit0 -x_0x23_10_0x23_11_bit0 -x_0x23_10_0x23_9_bit0 x_0x23_10_0x23_8_bit0 -x_0x23_10_0x23_6_bit0 -x_0x23_10_0x23_3_bit0 -x_0x23_10_0x23_1_bit0 -x_0x23_9_0x23_34_bit0 -x_0x23_9_0x23_32_bit0 -x_0x23_9_0x23_30_bit0 -x_0x23_9_0x23_29_bit0 -x_0x23_9_0x23_27_bit0 -x_0x23_9_0x23_26_bit0 -x_0x23_9_0x23_23_bit0 -x_0x23_9_0x23_20_bit0 -x_0x23_9_0x23_18_bit0 -x_0x23_9_0x23_16_bit0 -x_0x23_9_0x23_13_bit0 -x_0x23_9_0x23_11_bit0 -x_0x23_9_0x23_9_bit0 -x_0x23_9_0x23_8_bit0 x_0x23_9_0x23_6_bit0 -x_0x23_9_0x23_3_bit0 -x_0x23_9_0x23_1_bit0 -x_0x23_8_0x23_34_bit0 -x_0x23_8_0x23_32_bit0 -x_0x23_8_0x23_30_bit0 -x_0x23_8_0x23_29_bit0 -x_0x23_8_0x23_27_bit0 -x_0x23_8_0x23_26_bit0 -x_0x23_8_0x23_23_bit0 -x_0x23_8_0x23_20_bit0 -x_0x23_8_0x23_18_bit0 -x_0x23_8_0x23_16_bit0 -x_0x23_8_0x23_13_bit0 -x_0x23_8_0x23_11_bit0 -x_0x23_8_0x23_9_bit0 -x_0x23_8_0x23_8_bit0 -x_0x23_8_0x23_6_bit0 -x_0x23_8_0x23_3_bit0 -x_0x23_8_0x23_1_bit0 -x_0x23_7_0x23_34_bit0 -x_0x23_7_0x23_32_bit0 -x_0x23_7_0x23_30_bit0 -x_0x23_7_0x23_29_bit0 -x_0x23_7_0x23_27_bit0 -x_0x23_7_0x23_26_bit0 -x_0x23_7_0x23_23_bit0 -x_0x23_7_0x23_20_bit0 -x_0x23_7_0x23_18_bit0 -x_0x23_7_0x23_16_bit0 -x_0x23_7_0x23_13_bit0 -x_0x23_7_0x23_11_bit0 -x_0x23_7_0x23_9_bit0 -x_0x23_7_0x23_8_bit0 -x_0x23_7_0x23_6_bit0 -x_0x23_7_0x23_3_bit0 -x_0x23_7_0x23_1_bit0 -x_0x23_6_0x23_34_bit0 -x_0x23_6_0x23_32_bit0 -x_0x23_6_0x23_30_bit0 -x_0x23_6_0x23_29_bit0 -x_0x23_6_0x23_27_bit0 -x_0x23_6_0x23_26_bit0 -x_0x23_6_0x23_23_bit0 -x_0x23_6_0x23_20_bit0 -x_0x23_6_0x23_18_bit0 -x_0x23_6_0x23_16_bit0 -x_0x23_6_0x23_13_bit0 -x_0x23_6_0x23_11_bit0 -x_0x23_6_0x23_9_bit0 -x_0x23_6_0x23_8_bit0 -x_0x23_6_0x23_6_bit0 -x_0x23_6_0x23_3_bit0 -x_0x23_6_0x23_1_bit0 -x_0x23_5_0x23_34_bit0 -x_0x23_5_0x23_32_bit0 -x_0x23_5_0x23_30_bit0 -x_0x23_5_0x23_29_bit0 -x_0x23_5_0x23_27_bit0 -x_0x23_5_0x23_26_bit0 -x_0x23_5_0x23_23_bit0 -x_0x23_5_0x23_20_bit0 -x_0x23_5_0x23_18_bit0 -x_0x23_5_0x23_16_bit0 -x_0x23_5_0x23_13_bit0 -x_0x23_5_0x23_11_bit0 -x_0x23_5_0x23_9_bit0 -x_0x23_5_0x23_8_bit0 -x_0x23_5_0x23_6_bit0 -x_0x23_5_0x23_3_bit0 -x_0x23_5_0x23_1_bit0 -x_0x23_4_0x23_34_bit0 -x_0x23_4_0x23_32_bit0 -x_0x23_4_0x23_30_bit0 -x_0x23_4_0x23_29_bit0 -x_0x23_4_0x23_27_bit0 -x_0x23_4_0x23_26_bit0 -x_0x23_4_0x23_23_bit0 -x_0x23_4_0x23_20_bit0 -x_0x23_4_0x23_18_bit0 -x_0x23_4_0x23_16_bit0 -x_0x23_4_0x23_13_bit0 -x_0x23_4_0x23_11_bit0 -x_0x23_4_0x23_9_bit0 -x_0x23_4_0x23_8_bit0 -x_0x23_4_0x23_6_bit0 -x_0x23_4_0x23_3_bit0 -x_0x23_4_0x23_1_bit0 -x_0x23_3_0x23_34_bit0 -x_0x23_3_0x23_32_bit0 -x_0x23_3_0x23_30_bit0 -x_0x23_3_0x23_29_bit0 -x_0x23_3_0x23_27_bit0 -x_0x23_3_0x23_26_bit0 -x_0x23_3_0x23_23_bit0 -x_0x23_3_0x23_20_bit0 -x_0x23_3_0x23_18_bit0 -x_0x23_3_0x23_16_bit0 -x_0x23_3_0x23_13_bit0 -x_0x23_3_0x23_11_bit0 -x_0x23_3_0x23_9_bit0 -x_0x23_3_0x23_8_bit0 -x_0x23_3_0x23_6_bit0 -x_0x23_3_0x23_3_bit0 -x_0x23_3_0x23_1_bit0 -x_0x23_2_0x23_34_bit0 -x_0x23_2_0x23_32_bit0 -x_0x23_2_0x23_30_bit0 -x_0x23_2_0x23_29_bit0 -x_0x23_2_0x23_27_bit0 -x_0x23_2_0x23_26_bit0 -x_0x23_2_0x23_23_bit0 -x_0x23_2_0x23_20_bit0 -x_0x23_2_0x23_18_bit0 -x_0x23_2_0x23_16_bit0 -x_0x23_2_0x23_13_bit0 -x_0x23_2_0x23_11_bit0 -x_0x23_2_0x23_9_bit0 -x_0x23_2_0x23_8_bit0 -x_0x23_2_0x23_6_bit0 -x_0x23_2_0x23_3_bit0 -x_0x23_2_0x23_1_bit0 -x_0x23_1_0x23_34_bit0 -x_0x23_1_0x23_32_bit0 -x_0x23_1_0x23_30_bit0 -x_0x23_1_0x23_29_bit0 -x_0x23_1_0x23_27_bit0 -x_0x23_1_0x23_26_bit0 -x_0x23_1_0x23_23_bit0 -x_0x23_1_0x23_20_bit0 -x_0x23_1_0x23_18_bit0 -x_0x23_1_0x23_16_bit0 -x_0x23_1_0x23_13_bit0 -x_0x23_1_0x23_11_bit0 -x_0x23_1_0x23_9_bit0 -x_0x23_1_0x23_8_bit0 -x_0x23_1_0x23_6_bit0 -x_0x23_1_0x23_3_bit0 -x_0x23_1_0x23_1_bit0 -x_0x23_49_0x23_35_bit0 -x_0x23_49_0x23_33_bit0 -x_0x23_49_0x23_31_bit0 -x_0x23_49_0x23_28_bit0 -x_0x23_49_0x23_25_bit0 -x_0x23_49_0x23_24_bit0 x_0x23_49_0x23_22_bit0 -x_0x23_49_0x23_21_bit0 -x_0x23_49_0x23_19_bit0 -x_0x23_49_0x23_17_bit0 -x_0x23_49_0x23_15_bit0 -x_0x23_49_0x23_14_bit0 -x_0x23_49_0x23_12_bit0 -x_0x23_49_0x23_10_bit0 -x_0x23_49_0x23_7_bit0 -x_0x23_49_0x23_5_bit0 -x_0x23_49_0x23_4_bit0 -x_0x23_49_0x23_2_bit0 -x_0x23_48_0x23_35_bit0 -x_0x23_48_0x23_33_bit0 -x_0x23_48_0x23_31_bit0 -x_0x23_48_0x23_28_bit0 -x_0x23_48_0x23_25_bit0 -x_0x23_48_0x23_24_bit0 -x_0x23_48_0x23_22_bit0 -x_0x23_48_0x23_21_bit0 -x_0x23_48_0x23_19_bit0 -x_0x23_48_0x23_17_bit0 -x_0x23_48_0x23_15_bit0 -x_0x23_48_0x23_14_bit0 -x_0x23_48_0x23_12_bit0 -x_0x23_48_0x23_10_bit0 -x_0x23_48_0x23_7_bit0 -x_0x23_48_0x23_5_bit0 -x_0x23_48_0x23_4_bit0 -x_0x23_48_0x23_2_bit0 -x_0x23_47_0x23_35_bit0 -x_0x23_47_0x23_33_bit0 -x_0x23_47_0x23_31_bit0 -x_0x23_47_0x23_28_bit0 -x_0x23_47_0x23_25_bit0 x_0x23_47_0x23_24_bit0 -x_0x23_47_0x23_22_bit0 -x_0x23_47_0x23_21_bit0 -x_0x23_47_0x23_19_bit0 -x_0x23_47_0x23_17_bit0 -x_0x23_47_0x23_15_bit0 -x_0x23_47_0x23_14_bit0 -x_0x23_47_0x23_12_bit0 -x_0x23_47_0x23_10_bit0 -x_0x23_47_0x23_7_bit0 -x_0x23_47_0x23_5_bit0 -x_0x23_47_0x23_4_bit0 -x_0x23_47_0x23_2_bit0 -x_0x23_46_0x23_35_bit0 -x_0x23_46_0x23_33_bit0 -x_0x23_46_0x23_31_bit0 -x_0x23_46_0x23_28_bit0 x_0x23_46_0x23_25_bit0 -x_0x23_46_0x23_24_bit0 -x_0x23_46_0x23_22_bit0 -x_0x23_46_0x23_21_bit0 -x_0x23_46_0x23_19_bit0 -x_0x23_46_0x23_17_bit0 -x_0x23_46_0x23_15_bit0 -x_0x23_46_0x23_14_bit0 -x_0x23_46_0x23_12_bit0 -x_0x23_46_0x23_10_bit0 -x_0x23_46_0x23_7_bit0 -x_0x23_46_0x23_5_bit0 -x_0x23_46_0x23_4_bit0 -x_0x23_46_0x23_2_bit0 -x_0x23_45_0x23_35_bit0 -x_0x23_45_0x23_33_bit0 -x_0x23_45_0x23_31_bit0 -x_0x23_45_0x23_28_bit0 -x_0x23_45_0x23_25_bit0 -x_0x23_45_0x23_24_bit0 -x_0x23_45_0x23_22_bit0 -x_0x23_45_0x23_21_bit0 -x_0x23_45_0x23_19_bit0 -x_0x23_45_0x23_17_bit0 -x_0x23_45_0x23_15_bit0 -x_0x23_45_0x23_14_bit0 -x_0x23_45_0x23_12_bit0 -x_0x23_45_0x23_10_bit0 -x_0x23_45_0x23_7_bit0 -x_0x23_45_0x23_5_bit0 -x_0x23_45_0x23_4_bit0 -x_0x23_45_0x23_2_bit0 -x_0x23_44_0x23_35_bit0 -x_0x23_44_0x23_33_bit0 -x_0x23_44_0x23_31_bit0 -x_0x23_44_0x23_28_bit0 -x_0x23_44_0x23_25_bit0 -x_0x23_44_0x23_24_bit0 -x_0x23_44_0x23_22_bit0 -x_0x23_44_0x23_21_bit0 -x_0x23_44_0x23_19_bit0 -x_0x23_44_0x23_17_bit0 -x_0x23_44_0x23_15_bit0 -x_0x23_44_0x23_14_bit0 -x_0x23_44_0x23_12_bit0 -x_0x23_44_0x23_10_bit0 -x_0x23_44_0x23_7_bit0 -x_0x23_44_0x23_5_bit0 -x_0x23_44_0x23_4_bit0 -x_0x23_44_0x23_2_bit0 -x_0x23_43_0x23_35_bit0 -x_0x23_43_0x23_33_bit0 -x_0x23_43_0x23_31_bit0 -x_0x23_43_0x23_28_bit0 -x_0x23_43_0x23_25_bit0 -x_0x23_43_0x23_24_bit0 -x_0x23_43_0x23_22_bit0 -x_0x23_43_0x23_21_bit0 -x_0x23_43_0x23_19_bit0 -x_0x23_43_0x23_17_bit0 -x_0x23_43_0x23_15_bit0 -x_0x23_43_0x23_14_bit0 -x_0x23_43_0x23_12_bit0 -x_0x23_43_0x23_10_bit0 -x_0x23_43_0x23_7_bit0 -x_0x23_43_0x23_5_bit0 -x_0x23_43_0x23_4_bit0 -x_0x23_43_0x23_2_bit0 -x_0x23_42_0x23_35_bit0 -x_0x23_42_0x23_33_bit0 -x_0x23_42_0x23_31_bit0 -x_0x23_42_0x23_28_bit0 -x_0x23_42_0x23_25_bit0 -x_0x23_42_0x23_24_bit0 -x_0x23_42_0x23_22_bit0 x_0x23_42_0x23_21_bit0 -x_0x23_42_0x23_19_bit0 -x_0x23_42_0x23_17_bit0 -x_0x23_42_0x23_15_bit0 -x_0x23_42_0x23_14_bit0 -x_0x23_42_0x23_12_bit0 -x_0x23_42_0x23_10_bit0 -x_0x23_42_0x23_7_bit0 -x_0x23_42_0x23_5_bit0 -x_0x23_42_0x23_4_bit0 -x_0x23_42_0x23_2_bit0 x_0x23_41_0x23_35_bit0 -x_0x23_41_0x23_33_bit0 -x_0x23_41_0x23_31_bit0 -x_0x23_41_0x23_28_bit0 -x_0x23_41_0x23_25_bit0 -x_0x23_41_0x23_24_bit0 -x_0x23_41_0x23_22_bit0 -x_0x23_41_0x23_21_bit0 -x_0x23_41_0x23_19_bit0 -x_0x23_41_0x23_17_bit0 -x_0x23_41_0x23_15_bit0 -x_0x23_41_0x23_14_bit0 -x_0x23_41_0x23_12_bit0 -x_0x23_41_0x23_10_bit0 -x_0x23_41_0x23_7_bit0 -x_0x23_41_0x23_5_bit0 -x_0x23_41_0x23_4_bit0 -x_0x23_41_0x23_2_bit0 -x_0x23_40_0x23_35_bit0 x_0x23_40_0x23_33_bit0 -x_0x23_40_0x23_31_bit0 -x_0x23_40_0x23_28_bit0 -x_0x23_40_0x23_25_bit0 -x_0x23_40_0x23_24_bit0 -x_0x23_40_0x23_22_bit0 -x_0x23_40_0x23_21_bit0 -x_0x23_40_0x23_19_bit0 -x_0x23_40_0x23_17_bit0 -x_0x23_40_0x23_15_bit0 -x_0x23_40_0x23_14_bit0 -x_0x23_40_0x23_12_bit0 -x_0x23_40_0x23_10_bit0 -x_0x23_40_0x23_7_bit0 -x_0x23_40_0x23_5_bit0 -x_0x23_40_0x23_4_bit0 -x_0x23_40_0x23_2_bit0 -x_0x23_39_0x23_35_bit0 -x_0x23_39_0x23_33_bit0 x_0x23_39_0x23_31_bit0 -x_0x23_39_0x23_28_bit0 -x_0x23_39_0x23_25_bit0 -x_0x23_39_0x23_24_bit0 -x_0x23_39_0x23_22_bit0 -x_0x23_39_0x23_21_bit0 -x_0x23_39_0x23_19_bit0 -x_0x23_39_0x23_17_bit0 -x_0x23_39_0x23_15_bit0 -x_0x23_39_0x23_14_bit0 -x_0x23_39_0x23_12_bit0 -x_0x23_39_0x23_10_bit0 -x_0x23_39_0x23_7_bit0 -x_0x23_39_0x23_5_bit0 -x_0x23_39_0x23_4_bit0 -x_0x23_39_0x23_2_bit0 -x_0x23_38_0x23_35_bit0 -x_0x23_38_0x23_33_bit0 -x_0x23_38_0x23_31_bit0 -x_0x23_38_0x23_28_bit0 -x_0x23_38_0x23_25_bit0 -x_0x23_38_0x23_24_bit0 -x_0x23_38_0x23_22_bit0 -x_0x23_38_0x23_21_bit0 -x_0x23_38_0x23_19_bit0 -x_0x23_38_0x23_17_bit0 -x_0x23_38_0x23_15_bit0 -x_0x23_38_0x23_14_bit0 -x_0x23_38_0x23_12_bit0 -x_0x23_38_0x23_10_bit0 -x_0x23_38_0x23_7_bit0 -x_0x23_38_0x23_5_bit0 -x_0x23_38_0x23_4_bit0 -x_0x23_38_0x23_2_bit0 -x_0x23_37_0x23_35_bit0 -x_0x23_37_0x23_33_bit0 -x_0x23_37_0x23_31_bit0 x_0x23_37_0x23_28_bit0 -x_0x23_37_0x23_25_bit0 -x_0x23_37_0x23_24_bit0 -x_0x23_37_0x23_22_bit0 -x_0x23_37_0x23_21_bit0 -x_0x23_37_0x23_19_bit0 -x_0x23_37_0x23_17_bit0 -x_0x23_37_0x23_15_bit0 -x_0x23_37_0x23_14_bit0 -x_0x23_37_0x23_12_bit0 -x_0x23_37_0x23_10_bit0 -x_0x23_37_0x23_7_bit0 -x_0x23_37_0x23_5_bit0 -x_0x23_37_0x23_4_bit0 -x_0x23_37_0x23_2_bit0 -x_0x23_36_0x23_35_bit0 -x_0x23_36_0x23_33_bit0 -x_0x23_36_0x23_31_bit0 -x_0x23_36_0x23_28_bit0 -x_0x23_36_0x23_25_bit0 -x_0x23_36_0x23_24_bit0 -x_0x23_36_0x23_22_bit0 -x_0x23_36_0x23_21_bit0 -x_0x23_36_0x23_19_bit0 -x_0x23_36_0x23_17_bit0 -x_0x23_36_0x23_15_bit0 -x_0x23_36_0x23_14_bit0 -x_0x23_36_0x23_12_bit0 -x_0x23_36_0x23_10_bit0 -x_0x23_36_0x23_7_bit0 -x_0x23_36_0x23_5_bit0 -x_0x23_36_0x23_4_bit0 -x_0x23_36_0x23_2_bit0 -x_0x23_35_0x23_35_bit0 -x_0x23_35_0x23_33_bit0 -x_0x23_35_0x23_31_bit0 -x_0x23_35_0x23_28_bit0 -x_0x23_35_0x23_25_bit0 -x_0x23_35_0x23_24_bit0 -x_0x23_35_0x23_22_bit0 -x_0x23_35_0x23_21_bit0 -x_0x23_35_0x23_19_bit0 -x_0x23_35_0x23_17_bit0 -x_0x23_35_0x23_15_bit0 -x_0x23_35_0x23_14_bit0 -x_0x23_35_0x23_12_bit0 -x_0x23_35_0x23_10_bit0 -x_0x23_35_0x23_7_bit0 -x_0x23_35_0x23_5_bit0 -x_0x23_35_0x23_4_bit0 -x_0x23_35_0x23_2_bit0 -x_0x23_34_0x23_35_bit0 -x_0x23_34_0x23_33_bit0 -x_0x23_34_0x23_31_bit0 -x_0x23_34_0x23_28_bit0 -x_0x23_34_0x23_25_bit0 -x_0x23_34_0x23_24_bit0 -x_0x23_34_0x23_22_bit0 -x_0x23_34_0x23_21_bit0 -x_0x23_34_0x23_19_bit0 -x_0x23_34_0x23_17_bit0 -x_0x23_34_0x23_15_bit0 -x_0x23_34_0x23_14_bit0 -x_0x23_34_0x23_12_bit0 -x_0x23_34_0x23_10_bit0 -x_0x23_34_0x23_7_bit0 -x_0x23_34_0x23_5_bit0 -x_0x23_34_0x23_4_bit0 -x_0x23_34_0x23_2_bit0 -x_0x23_33_0x23_35_bit0 -x_0x23_33_0x23_33_bit0 -x_0x23_33_0x23_31_bit0 -x_0x23_33_0x23_28_bit0 -x_0x23_33_0x23_25_bit0 -x_0x23_33_0x23_24_bit0 -x_0x23_33_0x23_22_bit0 -x_0x23_33_0x23_21_bit0 -x_0x23_33_0x23_19_bit0 -x_0x23_33_0x23_17_bit0 -x_0x23_33_0x23_15_bit0 -x_0x23_33_0x23_14_bit0 -x_0x23_33_0x23_12_bit0 -x_0x23_33_0x23_10_bit0 -x_0x23_33_0x23_7_bit0 -x_0x23_33_0x23_5_bit0 -x_0x23_33_0x23_4_bit0 -x_0x23_33_0x23_2_bit0 -x_0x23_32_0x23_35_bit0 -x_0x23_32_0x23_33_bit0 -x_0x23_32_0x23_31_bit0 -x_0x23_32_0x23_28_bit0 -x_0x23_32_0x23_25_bit0 -x_0x23_32_0x23_24_bit0 -x_0x23_32_0x23_22_bit0 -x_0x23_32_0x23_21_bit0 -x_0x23_32_0x23_19_bit0 -x_0x23_32_0x23_17_bit0 -x_0x23_32_0x23_15_bit0 -x_0x23_32_0x23_14_bit0 -x_0x23_32_0x23_12_bit0 -x_0x23_32_0x23_10_bit0 -x_0x23_32_0x23_7_bit0 -x_0x23_32_0x23_5_bit0 -x_0x23_32_0x23_4_bit0 -x_0x23_32_0x23_2_bit0 -x_0x23_31_0x23_35_bit0 -x_0x23_31_0x23_33_bit0 -x_0x23_31_0x23_31_bit0 -x_0x23_31_0x23_28_bit0 -x_0x23_31_0x23_25_bit0 -x_0x23_31_0x23_24_bit0 -x_0x23_31_0x23_22_bit0 -x_0x23_31_0x23_21_bit0 -x_0x23_31_0x23_19_bit0 -x_0x23_31_0x23_17_bit0 -x_0x23_31_0x23_15_bit0 -x_0x23_31_0x23_14_bit0 -x_0x23_31_0x23_12_bit0 -x_0x23_31_0x23_10_bit0 -x_0x23_31_0x23_7_bit0 -x_0x23_31_0x23_5_bit0 -x_0x23_31_0x23_4_bit0 -x_0x23_31_0x23_2_bit0 -x_0x23_30_0x23_35_bit0 -x_0x23_30_0x23_33_bit0 -x_0x23_30_0x23_31_bit0 -x_0x23_30_0x23_28_bit0 -x_0x23_30_0x23_25_bit0 -x_0x23_30_0x23_24_bit0 -x_0x23_30_0x23_22_bit0 -x_0x23_30_0x23_21_bit0 -x_0x23_30_0x23_19_bit0 -x_0x23_30_0x23_17_bit0 -x_0x23_30_0x23_15_bit0 -x_0x23_30_0x23_14_bit0 -x_0x23_30_0x23_12_bit0 -x_0x23_30_0x23_10_bit0 -x_0x23_30_0x23_7_bit0 -x_0x23_30_0x23_5_bit0 -x_0x23_30_0x23_4_bit0 -x_0x23_30_0x23_2_bit0 -x_0x23_29_0x23_35_bit0 -x_0x23_29_0x23_33_bit0 -x_0x23_29_0x23_31_bit0 -x_0x23_29_0x23_28_bit0 -x_0x23_29_0x23_25_bit0 -x_0x23_29_0x23_24_bit0 -x_0x23_29_0x23_22_bit0 -x_0x23_29_0x23_21_bit0 -x_0x23_29_0x23_19_bit0 -x_0x23_29_0x23_17_bit0 -x_0x23_29_0x23_15_bit0 -x_0x23_29_0x23_14_bit0 -x_0x23_29_0x23_12_bit0 -x_0x23_29_0x23_10_bit0 -x_0x23_29_0x23_7_bit0 -x_0x23_29_0x23_5_bit0 -x_0x23_29_0x23_4_bit0 -x_0x23_29_0x23_2_bit0 -x_0x23_28_0x23_35_bit0 -x_0x23_28_0x23_33_bit0 -x_0x23_28_0x23_31_bit0 -x_0x23_28_0x23_28_bit0 -x_0x23_28_0x23_25_bit0 -x_0x23_28_0x23_24_bit0 -x_0x23_28_0x23_22_bit0 -x_0x23_28_0x23_21_bit0 x_0x23_28_0x23_19_bit0 -x_0x23_28_0x23_17_bit0 -x_0x23_28_0x23_15_bit0 -x_0x23_28_0x23_14_bit0 -x_0x23_28_0x23_12_bit0 -x_0x23_28_0x23_10_bit0 -x_0x23_28_0x23_7_bit0 -x_0x23_28_0x23_5_bit0 -x_0x23_28_0x23_4_bit0 -x_0x23_28_0x23_2_bit0 -x_0x23_27_0x23_35_bit0 -x_0x23_27_0x23_33_bit0 -x_0x23_27_0x23_31_bit0 -x_0x23_27_0x23_28_bit0 -x_0x23_27_0x23_25_bit0 -x_0x23_27_0x23_24_bit0 -x_0x23_27_0x23_22_bit0 -x_0x23_27_0x23_21_bit0 -x_0x23_27_0x23_19_bit0 -x_0x23_27_0x23_17_bit0 -x_0x23_27_0x23_15_bit0 -x_0x23_27_0x23_14_bit0 -x_0x23_27_0x23_12_bit0 -x_0x23_27_0x23_10_bit0 -x_0x23_27_0x23_7_bit0 -x_0x23_27_0x23_5_bit0 -x_0x23_27_0x23_4_bit0 -x_0x23_27_0x23_2_bit0 -x_0x23_26_0x23_35_bit0 -x_0x23_26_0x23_33_bit0 -x_0x23_26_0x23_31_bit0 -x_0x23_26_0x23_28_bit0 -x_0x23_26_0x23_25_bit0 -x_0x23_26_0x23_24_bit0 -x_0x23_26_0x23_22_bit0 -x_0x23_26_0x23_21_bit0 -x_0x23_26_0x23_19_bit0 -x_0x23_26_0x23_17_bit0 -x_0x23_26_0x23_15_bit0 -x_0x23_26_0x23_14_bit0 x_0x23_26_0x23_12_bit0 -x_0x23_26_0x23_10_bit0 -x_0x23_26_0x23_7_bit0 -x_0x23_26_0x23_5_bit0 -x_0x23_26_0x23_4_bit0 -x_0x23_26_0x23_2_bit0 -x_0x23_25_0x23_35_bit0 -x_0x23_25_0x23_33_bit0 -x_0x23_25_0x23_31_bit0 -x_0x23_25_0x23_28_bit0 -x_0x23_25_0x23_25_bit0 -x_0x23_25_0x23_24_bit0 -x_0x23_25_0x23_22_bit0 -x_0x23_25_0x23_21_bit0 -x_0x23_25_0x23_19_bit0 -x_0x23_25_0x23_17_bit0 -x_0x23_25_0x23_15_bit0 -x_0x23_25_0x23_14_bit0 -x_0x23_25_0x23_12_bit0 -x_0x23_25_0x23_10_bit0 -x_0x23_25_0x23_7_bit0 -x_0x23_25_0x23_5_bit0 -x_0x23_25_0x23_4_bit0 -x_0x23_25_0x23_2_bit0 -x_0x23_24_0x23_35_bit0 -x_0x23_24_0x23_33_bit0 -x_0x23_24_0x23_31_bit0 -x_0x23_24_0x23_28_bit0 -x_0x23_24_0x23_25_bit0 -x_0x23_24_0x23_24_bit0 -x_0x23_24_0x23_22_bit0 -x_0x23_24_0x23_21_bit0 -x_0x23_24_0x23_19_bit0 -x_0x23_24_0x23_17_bit0 -x_0x23_24_0x23_15_bit0 -x_0x23_24_0x23_14_bit0 -x_0x23_24_0x23_12_bit0 -x_0x23_24_0x23_10_bit0 -x_0x23_24_0x23_7_bit0 -x_0x23_24_0x23_5_bit0 -x_0x23_24_0x23_4_bit0 -x_0x23_24_0x23_2_bit0 -x_0x23_23_0x23_35_bit0 -x_0x23_23_0x23_33_bit0 -x_0x23_23_0x23_31_bit0 -x_0x23_23_0x23_28_bit0 -x_0x23_23_0x23_25_bit0 -x_0x23_23_0x23_24_bit0 -x_0x23_23_0x23_22_bit0 -x_0x23_23_0x23_21_bit0 -x_0x23_23_0x23_19_bit0 -x_0x23_23_0x23_17_bit0 -x_0x23_23_0x23_15_bit0 -x_0x23_23_0x23_14_bit0 -x_0x23_23_0x23_12_bit0 -x_0x23_23_0x23_10_bit0 -x_0x23_23_0x23_7_bit0 -x_0x23_23_0x23_5_bit0 -x_0x23_23_0x23_4_bit0 -x_0x23_23_0x23_2_bit0 -x_0x23_22_0x23_35_bit0 -x_0x23_22_0x23_33_bit0 -x_0x23_22_0x23_31_bit0 -x_0x23_22_0x23_28_bit0 -x_0x23_22_0x23_25_bit0 -x_0x23_22_0x23_24_bit0 -x_0x23_22_0x23_22_bit0 -x_0x23_22_0x23_21_bit0 -x_0x23_22_0x23_19_bit0 -x_0x23_22_0x23_17_bit0 -x_0x23_22_0x23_15_bit0 -x_0x23_22_0x23_14_bit0 -x_0x23_22_0x23_12_bit0 -x_0x23_22_0x23_10_bit0 -x_0x23_22_0x23_7_bit0 -x_0x23_22_0x23_5_bit0 -x_0x23_22_0x23_4_bit0 -x_0x23_22_0x23_2_bit0 -x_0x23_21_0x23_35_bit0 -x_0x23_21_0x23_33_bit0 -x_0x23_21_0x23_31_bit0 -x_0x23_21_0x23_28_bit0 -x_0x23_21_0x23_25_bit0 -x_0x23_21_0x23_24_bit0 -x_0x23_21_0x23_22_bit0 -x_0x23_21_0x23_21_bit0 -x_0x23_21_0x23_19_bit0 -x_0x23_21_0x23_17_bit0 -x_0x23_21_0x23_15_bit0 -x_0x23_21_0x23_14_bit0 -x_0x23_21_0x23_12_bit0 -x_0x23_21_0x23_10_bit0 -x_0x23_21_0x23_7_bit0 -x_0x23_21_0x23_5_bit0 -x_0x23_21_0x23_4_bit0 -x_0x23_21_0x23_2_bit0 -x_0x23_20_0x23_35_bit0 -x_0x23_20_0x23_33_bit0 -x_0x23_20_0x23_31_bit0 -x_0x23_20_0x23_28_bit0 -x_0x23_20_0x23_25_bit0 -x_0x23_20_0x23_24_bit0 -x_0x23_20_0x23_22_bit0 -x_0x23_20_0x23_21_bit0 -x_0x23_20_0x23_19_bit0 -x_0x23_20_0x23_17_bit0 -x_0x23_20_0x23_15_bit0 -x_0x23_20_0x23_14_bit0 -x_0x23_20_0x23_12_bit0 -x_0x23_20_0x23_10_bit0 -x_0x23_20_0x23_7_bit0 -x_0x23_20_0x23_5_bit0 -x_0x23_20_0x23_4_bit0 -x_0x23_20_0x23_2_bit0 -x_0x23_19_0x23_35_bit0 -x_0x23_19_0x23_33_bit0 -x_0x23_19_0x23_31_bit0 -x_0x23_19_0x23_28_bit0 -x_0x23_19_0x23_25_bit0 -x_0x23_19_0x23_24_bit0 -x_0x23_19_0x23_22_bit0 -x_0x23_19_0x23_21_bit0 -x_0x23_19_0x23_19_bit0 -x_0x23_19_0x23_17_bit0 -x_0x23_19_0x23_15_bit0 x_0x23_19_0x23_14_bit0 -x_0x23_19_0x23_12_bit0 -x_0x23_19_0x23_10_bit0 -x_0x23_19_0x23_7_bit0 -x_0x23_19_0x23_5_bit0 -x_0x23_19_0x23_4_bit0 -x_0x23_19_0x23_2_bit0 -x_0x23_18_0x23_35_bit0 -x_0x23_18_0x23_33_bit0 -x_0x23_18_0x23_31_bit0 -x_0x23_18_0x23_28_bit0 -x_0x23_18_0x23_25_bit0 -x_0x23_18_0x23_24_bit0 -x_0x23_18_0x23_22_bit0 -x_0x23_18_0x23_21_bit0 -x_0x23_18_0x23_19_bit0 -x_0x23_18_0x23_17_bit0 -x_0x23_18_0x23_15_bit0 -x_0x23_18_0x23_14_bit0 -x_0x23_18_0x23_12_bit0 x_0x23_18_0x23_10_bit0 -x_0x23_18_0x23_7_bit0 -x_0x23_18_0x23_5_bit0 -x_0x23_18_0x23_4_bit0 -x_0x23_18_0x23_2_bit0 -x_0x23_17_0x23_35_bit0 -x_0x23_17_0x23_33_bit0 -x_0x23_17_0x23_31_bit0 -x_0x23_17_0x23_28_bit0 -x_0x23_17_0x23_25_bit0 -x_0x23_17_0x23_24_bit0 -x_0x23_17_0x23_22_bit0 -x_0x23_17_0x23_21_bit0 -x_0x23_17_0x23_19_bit0 -x_0x23_17_0x23_17_bit0 -x_0x23_17_0x23_15_bit0 -x_0x23_17_0x23_14_bit0 -x_0x23_17_0x23_12_bit0 -x_0x23_17_0x23_10_bit0 -x_0x23_17_0x23_7_bit0 -x_0x23_17_0x23_5_bit0 -x_0x23_17_0x23_4_bit0 -x_0x23_17_0x23_2_bit0 -x_0x23_16_0x23_35_bit0 -x_0x23_16_0x23_33_bit0 -x_0x23_16_0x23_31_bit0 -x_0x23_16_0x23_28_bit0 -x_0x23_16_0x23_25_bit0 -x_0x23_16_0x23_24_bit0 -x_0x23_16_0x23_22_bit0 -x_0x23_16_0x23_21_bit0 -x_0x23_16_0x23_19_bit0 -x_0x23_16_0x23_17_bit0 -x_0x23_16_0x23_15_bit0 -x_0x23_16_0x23_14_bit0 -x_0x23_16_0x23_12_bit0 -x_0x23_16_0x23_10_bit0 -x_0x23_16_0x23_7_bit0 -x_0x23_16_0x23_5_bit0 -x_0x23_16_0x23_4_bit0 x_0x23_16_0x23_2_bit0 -x_0x23_15_0x23_35_bit0 -x_0x23_15_0x23_33_bit0 -x_0x23_15_0x23_31_bit0 -x_0x23_15_0x23_28_bit0 -x_0x23_15_0x23_25_bit0 -x_0x23_15_0x23_24_bit0 -x_0x23_15_0x23_22_bit0 -x_0x23_15_0x23_21_bit0 -x_0x23_15_0x23_19_bit0 -x_0x23_15_0x23_17_bit0 -x_0x23_15_0x23_15_bit0 -x_0x23_15_0x23_14_bit0 -x_0x23_15_0x23_12_bit0 -x_0x23_15_0x23_10_bit0 -x_0x23_15_0x23_7_bit0 -x_0x23_15_0x23_5_bit0 x_0x23_15_0x23_4_bit0 -x_0x23_15_0x23_2_bit0 -x_0x23_14_0x23_35_bit0 -x_0x23_14_0x23_33_bit0 -x_0x23_14_0x23_31_bit0 -x_0x23_14_0x23_28_bit0 -x_0x23_14_0x23_25_bit0 -x_0x23_14_0x23_24_bit0 -x_0x23_14_0x23_22_bit0 -x_0x23_14_0x23_21_bit0 -x_0x23_14_0x23_19_bit0 -x_0x23_14_0x23_17_bit0 -x_0x23_14_0x23_15_bit0 -x_0x23_14_0x23_14_bit0 -x_0x23_14_0x23_12_bit0 -x_0x23_14_0x23_10_bit0 -x_0x23_14_0x23_7_bit0 -x_0x23_14_0x23_5_bit0 -x_0x23_14_0x23_4_bit0 -x_0x23_14_0x23_2_bit0 -x_0x23_13_0x23_35_bit0 -x_0x23_13_0x23_33_bit0 -x_0x23_13_0x23_31_bit0 -x_0x23_13_0x23_28_bit0 -x_0x23_13_0x23_25_bit0 -x_0x23_13_0x23_24_bit0 -x_0x23_13_0x23_22_bit0 -x_0x23_13_0x23_21_bit0 -x_0x23_13_0x23_19_bit0 x_0x23_13_0x23_17_bit0 -x_0x23_13_0x23_15_bit0 -x_0x23_13_0x23_14_bit0 -x_0x23_13_0x23_12_bit0 -x_0x23_13_0x23_10_bit0 -x_0x23_13_0x23_7_bit0 -x_0x23_13_0x23_5_bit0 -x_0x23_13_0x23_4_bit0 -x_0x23_13_0x23_2_bit0 -x_0x23_12_0x23_35_bit0 -x_0x23_12_0x23_33_bit0 -x_0x23_12_0x23_31_bit0 -x_0x23_12_0x23_28_bit0 -x_0x23_12_0x23_25_bit0 -x_0x23_12_0x23_24_bit0 -x_0x23_12_0x23_22_bit0 -x_0x23_12_0x23_21_bit0 -x_0x23_12_0x23_19_bit0 -x_0x23_12_0x23_17_bit0 x_0x23_12_0x23_15_bit0 -x_0x23_12_0x23_14_bit0 -x_0x23_12_0x23_12_bit0 -x_0x23_12_0x23_10_bit0 -x_0x23_12_0x23_7_bit0 -x_0x23_12_0x23_5_bit0 -x_0x23_12_0x23_4_bit0 -x_0x23_12_0x23_2_bit0 -x_0x23_11_0x23_35_bit0 -x_0x23_11_0x23_33_bit0 -x_0x23_11_0x23_31_bit0 -x_0x23_11_0x23_28_bit0 -x_0x23_11_0x23_25_bit0 -x_0x23_11_0x23_24_bit0 -x_0x23_11_0x23_22_bit0 -x_0x23_11_0x23_21_bit0 -x_0x23_11_0x23_19_bit0 -x_0x23_11_0x23_17_bit0 -x_0x23_11_0x23_15_bit0 -x_0x23_11_0x23_14_bit0 -x_0x23_11_0x23_12_bit0 -x_0x23_11_0x23_10_bit0 -x_0x23_11_0x23_7_bit0 -x_0x23_11_0x23_5_bit0 -x_0x23_11_0x23_4_bit0 -x_0x23_11_0x23_2_bit0 -x_0x23_10_0x23_35_bit0 -x_0x23_10_0x23_33_bit0 -x_0x23_10_0x23_31_bit0 -x_0x23_10_0x23_28_bit0 -x_0x23_10_0x23_25_bit0 -x_0x23_10_0x23_24_bit0 -x_0x23_10_0x23_22_bit0 -x_0x23_10_0x23_21_bit0 -x_0x23_10_0x23_19_bit0 -x_0x23_10_0x23_17_bit0 -x_0x23_10_0x23_15_bit0 -x_0x23_10_0x23_14_bit0 -x_0x23_10_0x23_12_bit0 -x_0x23_10_0x23_10_bit0 -x_0x23_10_0x23_7_bit0 -x_0x23_10_0x23_5_bit0 -x_0x23_10_0x23_4_bit0 -x_0x23_10_0x23_2_bit0 -x_0x23_9_0x23_35_bit0 -x_0x23_9_0x23_33_bit0 -x_0x23_9_0x23_31_bit0 -x_0x23_9_0x23_28_bit0 -x_0x23_9_0x23_25_bit0 -x_0x23_9_0x23_24_bit0 -x_0x23_9_0x23_22_bit0 -x_0x23_9_0x23_21_bit0 -x_0x23_9_0x23_19_bit0 -x_0x23_9_0x23_17_bit0 -x_0x23_9_0x23_15_bit0 -x_0x23_9_0x23_14_bit0 -x_0x23_9_0x23_12_bit0 -x_0x23_9_0x23_10_bit0 -x_0x23_9_0x23_7_bit0 -x_0x23_9_0x23_5_bit0 -x_0x23_9_0x23_4_bit0 -x_0x23_9_0x23_2_bit0 -x_0x23_8_0x23_35_bit0 -x_0x23_8_0x23_33_bit0 -x_0x23_8_0x23_31_bit0 -x_0x23_8_0x23_28_bit0 -x_0x23_8_0x23_25_bit0 -x_0x23_8_0x23_24_bit0 -x_0x23_8_0x23_22_bit0 -x_0x23_8_0x23_21_bit0 -x_0x23_8_0x23_19_bit0 -x_0x23_8_0x23_17_bit0 -x_0x23_8_0x23_15_bit0 -x_0x23_8_0x23_14_bit0 -x_0x23_8_0x23_12_bit0 -x_0x23_8_0x23_10_bit0 -x_0x23_8_0x23_7_bit0 x_0x23_8_0x23_5_bit0 -x_0x23_8_0x23_4_bit0 -x_0x23_8_0x23_2_bit0 -x_0x23_7_0x23_35_bit0 -x_0x23_7_0x23_33_bit0 -x_0x23_7_0x23_31_bit0 -x_0x23_7_0x23_28_bit0 -x_0x23_7_0x23_25_bit0 -x_0x23_7_0x23_24_bit0 -x_0x23_7_0x23_22_bit0 -x_0x23_7_0x23_21_bit0 -x_0x23_7_0x23_19_bit0 -x_0x23_7_0x23_17_bit0 -x_0x23_7_0x23_15_bit0 -x_0x23_7_0x23_14_bit0 -x_0x23_7_0x23_12_bit0 -x_0x23_7_0x23_10_bit0 -x_0x23_7_0x23_7_bit0 -x_0x23_7_0x23_5_bit0 -x_0x23_7_0x23_4_bit0 -x_0x23_7_0x23_2_bit0 -x_0x23_6_0x23_35_bit0 -x_0x23_6_0x23_33_bit0 -x_0x23_6_0x23_31_bit0 -x_0x23_6_0x23_28_bit0 -x_0x23_6_0x23_25_bit0 -x_0x23_6_0x23_24_bit0 -x_0x23_6_0x23_22_bit0 -x_0x23_6_0x23_21_bit0 -x_0x23_6_0x23_19_bit0 -x_0x23_6_0x23_17_bit0 -x_0x23_6_0x23_15_bit0 -x_0x23_6_0x23_14_bit0 -x_0x23_6_0x23_12_bit0 -x_0x23_6_0x23_10_bit0 -x_0x23_6_0x23_7_bit0 -x_0x23_6_0x23_5_bit0 -x_0x23_6_0x23_4_bit0 -x_0x23_6_0x23_2_bit0 -x_0x23_5_0x23_35_bit0 -x_0x23_5_0x23_33_bit0 -x_0x23_5_0x23_31_bit0 -x_0x23_5_0x23_28_bit0 -x_0x23_5_0x23_25_bit0 -x_0x23_5_0x23_24_bit0 -x_0x23_5_0x23_22_bit0 -x_0x23_5_0x23_21_bit0 -x_0x23_5_0x23_19_bit0 -x_0x23_5_0x23_17_bit0 -x_0x23_5_0x23_15_bit0 -x_0x23_5_0x23_14_bit0 -x_0x23_5_0x23_12_bit0 -x_0x23_5_0x23_10_bit0 -x_0x23_5_0x23_7_bit0 -x_0x23_5_0x23_5_bit0 -x_0x23_5_0x23_4_bit0 -x_0x23_5_0x23_2_bit0 -x_0x23_4_0x23_35_bit0 -x_0x23_4_0x23_33_bit0 -x_0x23_4_0x23_31_bit0 -x_0x23_4_0x23_28_bit0 -x_0x23_4_0x23_25_bit0 -x_0x23_4_0x23_24_bit0 -x_0x23_4_0x23_22_bit0 -x_0x23_4_0x23_21_bit0 -x_0x23_4_0x23_19_bit0 -x_0x23_4_0x23_17_bit0 -x_0x23_4_0x23_15_bit0 -x_0x23_4_0x23_14_bit0 -x_0x23_4_0x23_12_bit0 -x_0x23_4_0x23_10_bit0 -x_0x23_4_0x23_7_bit0 -x_0x23_4_0x23_5_bit0 -x_0x23_4_0x23_4_bit0 -x_0x23_4_0x23_2_bit0 -x_0x23_3_0x23_35_bit0 -x_0x23_3_0x23_33_bit0 -x_0x23_3_0x23_31_bit0 -x_0x23_3_0x23_28_bit0 -x_0x23_3_0x23_25_bit0 -x_0x23_3_0x23_24_bit0 -x_0x23_3_0x23_22_bit0 -x_0x23_3_0x23_21_bit0 -x_0x23_3_0x23_19_bit0 -x_0x23_3_0x2#### 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.62 0.88 0.88 2/55 798
Raw data (stat): 798 (runsolver) R 797 20024 20023 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 546064219 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.0009 s]
Raw data (loadavg): 0.68 0.88 0.88 2/55 798
Raw data (stat): 798 (minisat+) R 797 20024 20023 0 -1 0 6944 0 0 0 980 18 0 0 25 0 1 0 546064219 23216128 4885 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5668 4885 603 41 0 5627 0
vsize: 22672
[startup+20.0014 s]
Raw data (loadavg): 0.73 0.89 0.88 2/55 798
Raw data (stat): 798 (minisat+) R 797 20024 20023 0 -1 0 8779 0 0 0 1963 23 0 0 25 0 1 0 546064219 26112000 5602 4294967295 134512640 134672761 3221224544 3221223728 134615627 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6375 5602 603 41 0 6334 0
vsize: 25500
[startup+30.0013 s]
Raw data (loadavg): 0.77 0.89 0.89 2/55 798
Raw data (stat): 798 (minisat+) R 797 20024 20023 0 -1 0 9200 0 0 0 2961 25 0 0 25 0 1 0 546064219 27885568 6023 4294967295 134512640 134672761 3221224544 3221223584 134612684 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6808 6023 603 41 0 6767 0
vsize: 27232
[startup+40.0042 s]
Raw data (loadavg): 0.81 0.89 0.89 2/55 798
Raw data (stat): 798 (minisat+) R 797 20024 20023 0 -1 0 10267 0 0 0 3958 29 0 0 25 0 1 0 546064219 32337920 7090 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7895 7090 603 41 0 7854 0
vsize: 31580
[startup+50.0182 s]
Raw data (loadavg): 0.84 0.90 0.89 2/55 798
Raw data (stat): 798 (minisat+) R 797 20024 20023 0 -1 0 10874 0 0 0 4956 32 0 0 25 0 1 0 546064219 34865152 7697 4294967295 134512640 134672761 3221224544 3221223728 134615940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8512 7697 603 41 0 8471 0
vsize: 34048
[startup+60.0191 s]
Raw data (loadavg): 0.86 0.90 0.89 2/55 798
Raw data (stat): 798 (minisat+) R 797 20024 20023 0 -1 0 11832 0 0 0 5953 35 0 0 25 0 1 0 546064219 36081664 8025 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8809 8025 603 41 0 8768 0
vsize: 35236
[startup+70.0196 s]
Raw data (loadavg): 0.88 0.90 0.89 2/55 798
Raw data (stat): 798 (minisat+) R 797 20024 20023 0 -1 0 12753 0 0 0 6951 37 0 0 25 0 1 0 546064219 39886848 8946 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9738 8946 603 41 0 9697 0
vsize: 38952
[startup+80.0199 s]
Raw data (loadavg): 0.90 0.90 0.89 2/55 798
Raw data (stat): 798 (minisat+) R 797 20024 20023 0 -1 0 13831 0 0 0 7948 40 0 0 25 0 1 0 546064219 44343296 10024 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10826 10024 603 41 0 10785 0
vsize: 43304
[startup+90.0198 s]
Raw data (loadavg): 0.91 0.91 0.89 2/55 798
Raw data (stat): 798 (minisat+) R 797 20024 20023 0 -1 0 14510 0 0 0 8946 42 0 0 25 0 1 0 546064219 47071232 10703 4294967295 134512640 134672761 3221224544 3221223728 134615594 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11492 10703 603 41 0 11451 0
vsize: 45968
[startup+100.02 s]
Raw data (loadavg): 0.93 0.91 0.89 2/55 798
Raw data (stat): 798 (minisat+) R 797 20024 20023 0 -1 0 15353 0 0 0 9944 45 0 0 25 0 1 0 546064219 50499584 11546 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12329 11546 603 41 0 12288 0
vsize: 49316
[startup+110.021 s]
Raw data (loadavg): 0.94 0.91 0.89 2/55 798
Raw data (stat): 798 (minisat+) R 797 20024 20023 0 -1 0 15998 0 0 0 10942 47 0 0 25 0 1 0 546064219 53141504 12191 4294967295 134512640 134672761 3221224544 3221223728 134615523 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12974 12191 603 41 0 12933 0
vsize: 51896
[startup+120.022 s]
Raw data (loadavg): 0.95 0.91 0.89 2/55 800
Raw data (stat): 798 (minisat+) R 797 20024 20023 0 -1 0 17036 0 0 0 11940 49 0 0 25 0 1 0 546064219 57462784 13229 4294967295 134512640 134672761 3221224544 3221223728 134615916 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14029 13229 603 41 0 13988 0
vsize: 56116
[startup+130.022 s]
Raw data (loadavg): 0.95 0.92 0.89 2/55 800
Raw data (stat): 798 (minisat+) R 797 20024 20023 0 -1 0 18184 0 0 0 12937 52 0 0 25 0 1 0 546064219 62181376 14377 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15181 14377 603 41 0 15140 0
vsize: 60724
[startup+140.022 s]
Raw data (loadavg): 0.96 0.92 0.90 2/55 800
Raw data (stat): 798 (minisat+) R 797 20024 20023 0 -1 0 19315 0 0 0 13934 55 0 0 25 0 1 0 546064219 66867200 15508 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16325 15508 603 41 0 16284 0
vsize: 65300
[startup+150.023 s]
Raw data (loadavg): 0.97 0.92 0.90 2/55 800
Raw data (stat): 798 (minisat+) R 797 20024 20023 0 -1 0 20462 0 0 0 14930 59 0 0 25 0 1 0 546064219 71557120 16655 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17470 16655 603 41 0 17429 0
vsize: 69880
[startup+160.025 s]
Raw data (loadavg): 0.97 0.92 0.90 2/55 800
Raw data (stat): 798 (minisat+) R 797 20024 20023 0 -1 0 21244 0 0 0 15929 61 0 0 25 0 1 0 546064219 74698752 17437 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18237 17437 603 41 0 18196 0
vsize: 72948
[startup+170.025 s]
Raw data (loadavg): 0.98 0.92 0.90 2/55 800
Raw data (stat): 798 (minisat+) R 797 20024 20023 0 -1 0 22103 0 0 0 16927 63 0 0 25 0 1 0 546064219 78237696 18296 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19101 18296 603 41 0 19060 0
vsize: 76404
[startup+180.025 s]
Raw data (loadavg): 0.98 0.93 0.90 2/55 800
Raw data (stat): 798 (minisat+) R 797 20024 20023 0 -1 0 22995 0 0 0 17923 67 0 0 25 0 1 0 546064219 81866752 19188 4294967295 134512640 134672761 3221224544 3221223584 134612981 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19987 19188 603 41 0 19946 0
vsize: 79948
[startup+190.026 s]
Raw data (loadavg): 0.98 0.93 0.90 2/55 800
Raw data (stat): 798 (minisat+) R 797 20024 20023 0 -1 0 24760 0 0 0 18918 72 0 0 25 0 1 0 546064219 87265280 20502 4294967295 134512640 134672761 3221224544 3221223264 134542429 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21305 20502 603 41 0 21264 0
vsize: 85220
[startup+200.026 s]
Raw data (loadavg): 0.98 0.93 0.90 2/55 800
Raw data (stat): 798 (minisat+) R 797 20024 20023 0 -1 0 24768 0 0 0 19917 73 0 0 25 0 1 0 546064219 87265280 20510 4294967295 134512640 134672761 3221224544 3221223584 134612510 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21305 20510 603 41 0 21264 0
vsize: 85220
[startup+210.027 s]
Raw data (loadavg): 0.99 0.93 0.90 2/55 800
Raw data (stat): 798 (minisat+) R 797 20024 20023 0 -1 0 24768 0 0 0 20917 73 0 0 25 0 1 0 546064219 87265280 20510 4294967295 134512640 134672761 3221224544 3221223728 134615991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21305 20510 603 41 0 21264 0
vsize: 85220
[startup+220.028 s]
Raw data (loadavg): 0.99 0.93 0.90 2/55 800
Raw data (stat): 798 (minisat+) R 797 20024 20023 0 -1 0 24768 0 0 0 21917 73 0 0 25 0 1 0 546064219 87265280 20510 4294967295 134512640 134672761 3221224544 3221223728 134615665 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21305 20510 603 41 0 21264 0
vsize: 85220
[startup+230.028 s]
Raw data (loadavg): 0.99 0.94 0.90 2/55 800
Raw data (stat): 798 (minisat+) R 797 20024 20023 0 -1 0 25344 0 0 0 22915 76 0 0 25 0 1 0 546064219 86306816 20294 4294967295 134512640 134672761 3221224544 3221223728 134615693 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21071 20294 603 41 0 21030 0
vsize: 84284
[startup+240.027 s]
Raw data (loadavg): 0.99 0.94 0.91 2/55 800
Raw data (stat): 798 (minisat+) R 797 20024 20023 0 -1 0 25344 0 0 0 23915 76 0 0 25 0 1 0 546064219 86306816 20294 4294967295 134512640 134672761 3221224544 3221223536 134615627 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21071 20294 603 41 0 21030 0
vsize: 84284
[startup+250.028 s]
Raw data (loadavg): 0.99 0.94 0.91 2/55 800
Raw data (stat): 798 (minisat+) R 797 20024 20023 0 -1 0 25344 0 0 0 24915 76 0 0 25 0 1 0 546064219 86306816 20294 4294967295 134512640 134672761 3221224544 3221223584 134612867 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21071 20294 603 41 0 21030 0
vsize: 84284
[startup+260.029 s]
Raw data (loadavg): 0.99 0.94 0.91 2/55 800
Raw data (stat): 798 (minisat+) R 797 20024 20023 0 -1 0 25344 0 0 0 25916 76 0 0 25 0 1 0 546064219 86306816 20294 4294967295 134512640 134672761 3221224544 3221223728 134615601 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21071 20294 603 41 0 21030 0
vsize: 84284
[startup+270.029 s]
Raw data (loadavg): 0.99 0.94 0.91 2/55 800
Raw data (stat): 798 (minisat+) R 797 20024 20023 0 -1 0 25344 0 0 0 26916 76 0 0 25 0 1 0 546064219 86306816 20294 4294967295 134512640 134672761 3221224544 3221223728 134615739 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21071 20294 603 41 0 21030 0
vsize: 84284
[startup+280.029 s]
Raw data (loadavg): 0.99 0.94 0.91 2/55 800
Raw data (stat): 798 (minisat+) R 797 20024 20023 0 -1 0 25344 0 0 0 27916 76 0 0 25 0 1 0 546064219 86306816 20294 4294967295 134512640 134672761 3221224544 3221223680 134614690 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21071 20294 603 41 0 21030 0
vsize: 84284
[startup+290.03 s]
Raw data (loadavg): 0.99 0.94 0.91 2/55 800
Raw data (stat): 798 (minisat+) R 797 20024 20023 0 -1 0 25344 0 0 0 28916 76 0 0 25 0 1 0 546064219 86306816 20294 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21071 20294 603 41 0 21030 0
vsize: 84284
[startup+300.03 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 800
Raw data (stat): 798 (minisat+) R 797 20024 20023 0 -1 0 25344 0 0 0 29916 76 0 0 25 0 1 0 546064219 86306816 20294 4294967295 134512640 134672761 3221224544 3221223728 134615807 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21071 20294 603 41 0 21030 0
vsize: 84284
[startup+310.032 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 800
Raw data (stat): 798 (minisat+) R 797 20024 20023 0 -1 0 25344 0 0 0 30916 76 0 0 25 0 1 0 546064219 86306816 20294 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21071 20294 603 41 0 21030 0
vsize: 84284
[startup+320.032 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 800
Raw data (stat): 798 (minisat+) R 797 20024 20023 0 -1 0 25344 0 0 0 31917 76 0 0 25 0 1 0 546064219 86306816 20294 4294967295 134512640 134672761 3221224544 3221223584 134612892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21071 20294 603 41 0 21030 0
vsize: 84284
[startup+330.032 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 800
Raw data (stat): 798 (minisat+) R 797 20024 20023 0 -1 0 25594 0 0 0 32916 76 0 0 25 0 1 0 546064219 87363584 20544 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21329 20544 603 41 0 21288 0
vsize: 85316
[startup+340.032 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 800
Raw data (stat): 798 (minisat+) R 797 20024 20023 0 -1 0 26373 0 0 0 33915 78 0 0 25 0 1 0 546064219 90517504 21323 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22099 21323 603 41 0 22058 0
vsize: 88396
[startup+350.033 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 800
Raw data (stat): 798 (minisat+) R 797 20024 20023 0 -1 0 27372 0 0 0 34912 81 0 0 25 0 1 0 546064219 92520448 21791 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22588 21791 603 41 0 22547 0
vsize: 90352
[startup+360.034 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 800
Raw data (stat): 798 (minisat+) R 797 20024 20023 0 -1 0 27372 0 0 0 35911 81 0 0 25 0 1 0 546064219 92520448 21791 4294967295 134512640 134672761 3221224544 3221223668 134566077 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22588 21791 603 41 0 22547 0
vsize: 90352
[startup+370.034 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 800
Raw data (stat): 798 (minisat+) R 797 20024 20023 0 -1 0 27372 0 0 0 36910 81 0 0 25 0 1 0 546064219 92520448 21791 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22588 21791 603 41 0 22547 0
vsize: 90352
[startup+380.034 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 800
Raw data (stat): 798 (minisat+) R 797 20024 20023 0 -1 0 27372 0 0 0 37910 81 0 0 25 0 1 0 546064219 92520448 21791 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22588 21791 603 41 0 22547 0
vsize: 90352
[startup+390.035 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 800
Raw data (stat): 798 (minisat+) R 797 20024 20023 0 -1 0 27372 0 0 0 38910 81 0 0 25 0 1 0 546064219 92520448 21791 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22588 21791 603 41 0 22547 0
vsize: 90352
[startup+400.036 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 800
Raw data (stat): 798 (minisat+) R 797 20024 20023 0 -1 0 27372 0 0 0 39910 81 0 0 25 0 1 0 546064219 92520448 21791 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22588 21791 603 41 0 22547 0
vsize: 90352
[startup+410.036 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 800
Raw data (stat): 798 (minisat+) R 797 20024 20023 0 -1 0 27372 0 0 0 40911 81 0 0 25 0 1 0 546064219 92520448 21791 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22588 21791 603 41 0 22547 0
vsize: 90352
[startup+420.037 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 802
Raw data (stat): 798 (minisat+) R 797 20024 20023 0 -1 0 27373 0 0 0 41911 81 0 0 25 0 1 0 546064219 92520448 21792 4294967295 134512640 134672761 3221224544 3221223728 134615611 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22588 21792 603 41 0 22547 0
vsize: 90352
[startup+430.038 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 802
Raw data (stat): 798 (minisat+) R 797 20024 20023 0 -1 0 27373 0 0 0 42911 81 0 0 25 0 1 0 546064219 92520448 21792 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22588 21792 603 41 0 22547 0
vsize: 90352
[startup+440.038 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 802
Raw data (stat): 798 (minisat+) R 797 20024 20023 0 -1 0 27373 0 0 0 43911 81 0 0 25 0 1 0 546064219 92520448 21792 4294967295 134512640 134672761 3221224544 3221223584 134612668 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22588 21792 603 41 0 22547 0
vsize: 90352
[startup+450.038 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 802
Raw data (stat): 798 (minisat+) R 797 20024 20023 0 -1 0 27373 0 0 0 44911 81 0 0 25 0 1 0 546064219 92520448 21792 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22588 21792 603 41 0 22547 0
vsize: 90352
[startup+460.039 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 802
Raw data (stat): 798 (minisat+) R 797 20024 20023 0 -1 0 27373 0 0 0 45912 81 0 0 25 0 1 0 546064219 92520448 21792 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22588 21792 603 41 0 22547 0
vsize: 90352
[startup+470.039 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 802
Raw data (stat): 798 (minisat+) R 797 20024 20023 0 -1 0 27977 0 0 0 46910 83 0 0 25 0 1 0 546064219 94990336 22396 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23191 22396 603 41 0 23150 0
vsize: 92764
[startup+480.039 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 802
Raw data (stat): 798 (minisat+) R 797 20024 20023 0 -1 0 28941 0 0 0 47907 86 0 0 25 0 1 0 546064219 98938880 23360 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24155 23360 603 41 0 24114 0
vsize: 96620
[startup+490.04 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 802
Raw data (stat): 798 (minisat+) R 797 20024 20023 0 -1 0 29969 0 0 0 48904 89 0 0 25 0 1 0 546064219 103112704 24388 4294967295 134512640 134672761 3221224544 3221223728 134615916 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25174 24388 603 41 0 25133 0
vsize: 100696
[startup+500.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 802
Raw data (stat): 798 (minisat+) R 797 20024 20023 0 -1 0 30978 0 0 0 49902 92 0 0 25 0 1 0 546064219 107257856 25397 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26186 25397 603 41 0 26145 0
vsize: 104744
[startup+510.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 802
Raw data (stat): 798 (minisat+) R 797 20024 20023 0 -1 0 32232 0 0 0 50899 95 0 0 25 0 1 0 546064219 112353280 26651 4294967295 134512640 134672761 3221224544 3221223356 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27430 26651 603 41 0 27389 0
vsize: 109720
[startup+520.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 802
Raw data (stat): 798 (minisat+) R 797 20024 20023 0 -1 0 33195 0 0 0 51897 97 0 0 25 0 1 0 546064219 116264960 27614 4294967295 134512640 134672761 3221224544 3221223584 134612684 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28418 27615 603 41 0 28377 0
vsize: 113540
[startup+530.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 802
Raw data (stat): 798 (minisat+) R 797 20024 20023 0 -1 0 34029 0 0 0 52895 99 0 0 25 0 1 0 546064219 119771136 28448 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29241 28448 603 41 0 29200 0
vsize: 116964
[startup+540.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 802
Raw data (stat): 798 (minisat+) R 797 20024 20023 0 -1 0 34963 0 0 0 53893 101 0 0 25 0 1 0 546064219 123551744 29382 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30164 29382 603 41 0 30123 0
vsize: 120656
[startup+550.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 802
Raw data (stat): 798 (minisat+) R 797 20024 20023 0 -1 0 35953 0 0 0 54891 104 0 0 25 0 1 0 546064219 127610880 30372 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31155 30372 603 41 0 31114 0
vsize: 124620
[startup+560.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 802
Raw data (stat): 798 (minisat+) R 797 20024 20023 0 -1 0 37044 0 0 0 55889 106 0 0 25 0 1 0 546064219 132055040 31463 4294967295 134512640 134672761 3221224544 3221223584 134613740 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32240 31463 603 41 0 32199 0
vsize: 128960
[startup+570.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 802
Raw data (stat): 798 (minisat+) R 797 20024 20023 0 -1 0 38065 0 0 0 56886 109 0 0 25 0 1 0 546064219 136253440 32484 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33265 32484 603 41 0 33224 0
vsize: 133060
[startup+580.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 802
Raw data (stat): 798 (minisat+) R 797 20024 20023 0 -1 0 39100 0 0 0 57884 111 0 0 25 0 1 0 546064219 140427264 33519 4294967295 134512640 134672761 3221224544 3221223728 134615828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34284 33519 603 41 0 34243 0
vsize: 137136
[startup+590.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 802
Raw data (stat): 798 (minisat+) R 797 20024 20023 0 -1 0 39941 0 0 0 58883 113 0 0 25 0 1 0 546064219 143933440 34360 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35140 34360 603 41 0 35099 0
vsize: 140560
[startup+600.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 802
Raw data (stat): 798 (minisat+) R 797 20024 20023 0 -1 0 40764 0 0 0 59881 115 0 0 25 0 1 0 546064219 147603456 35183 4294967295 134512640 134672761 3221224544 3221223584 134614228 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36036 35183 603 41 0 35995 0
vsize: 144144
[startup+610.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 802
Raw data (stat): 798 (minisat+) R 797 20024 20023 0 -1 0 41639 0 0 0 60879 117 0 0 25 0 1 0 546064219 151146496 36058 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36901 36058 603 41 0 36860 0
vsize: 147604
[startup+620.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 802
Raw data (stat): 798 (minisat+) R 797 20024 20023 0 -1 0 42534 0 0 0 61877 119 0 0 25 0 1 0 546064219 154820608 36953 4294967295 134512640 134672761 3221224544 3221223584 134614228 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37798 36953 603 41 0 37757 0
vsize: 151192
[startup+630.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 802
Raw data (stat): 798 (minisat+) R 797 20024 20023 0 -1 0 43380 0 0 0 62875 121 0 0 25 0 1 0 546064219 158208000 37799 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38625 37799 603 41 0 38584 0
vsize: 154500
[startup+640.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 802
Raw data (stat): 798 (minisat+) R 797 20024 20023 0 -1 0 44407 0 0 0 63873 123 0 0 25 0 1 0 546064219 162488320 38826 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39670 38826 603 41 0 39629 0
vsize: 158680
[startup+650.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 802
Raw data (stat): 798 (minisat+) R 797 20024 20023 0 -1 0 45318 0 0 0 64871 125 0 0 25 0 1 0 546064219 166117376 39737 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40556 39737 603 41 0 40515 0
vsize: 162224
[startup+660.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 802
Raw data (stat): 798 (minisat+) R 797 20024 20023 0 -1 0 46023 0 0 0 65870 126 0 0 25 0 1 0 546064219 169115648 40442 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41288 40442 603 41 0 41247 0
vsize: 165152
[startup+670.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 802
Raw data (stat): 798 (minisat+) R 797 20024 20023 0 -1 0 46839 0 0 0 66868 129 0 0 25 0 1 0 546064219 172363776 41258 4294967295 134512640 134672761 3221224544 3221223796 134617908 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42081 41258 603 41 0 42040 0
vsize: 168324
[startup+680.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 802
Raw data (stat): 798 (minisat+) R 797 20024 20023 0 -1 0 47863 0 0 0 67866 131 0 0 25 0 1 0 546064219 176537600 42282 4294967295 134512640 134672761 3221224544 3221223728 134616023 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43100 42282 603 41 0 43059 0
vsize: 172400
[startup+690.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 802
Raw data (stat): 798 (minisat+) R 797 20024 20023 0 -1 0 48925 0 0 0 68863 134 0 0 25 0 1 0 546064219 180944896 43344 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44176 43344 603 41 0 44135 0
vsize: 176704
[startup+700.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 802
Raw data (stat): 798 (minisat+) R 797 20024 20023 0 -1 0 49821 0 0 0 69860 137 0 0 25 0 1 0 546064219 184594432 44240 4294967295 134512640 134672761 3221224544 3221223728 134615627 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45067 44240 603 41 0 45026 0
vsize: 180268
[startup+710.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 802
Raw data (stat): 798 (minisat+) R 797 20024 20023 0 -1 0 50766 0 0 0 70859 139 0 0 25 0 1 0 546064219 188387328 45185 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45993 45185 603 41 0 45952 0
vsize: 183972
[startup+720.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 804
Raw data (stat): 798 (minisat+) R 797 20024 20023 0 -1 0 51404 0 0 0 71858 140 0 0 25 0 1 0 546064219 191012864 45823 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 46634 45823 603 41 0 46593 0
vsize: 186536
[startup+730.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 804
Raw data (stat): 798 (minisat+) R 797 20024 20023 0 -1 0 52204 0 0 0 72856 142 0 0 25 0 1 0 546064219 194387968 46623 4294967295 134512640 134672761 3221224544 3221223728 134615994 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 47458 46623 603 41 0 47417 0
vsize: 189832
[startup+740.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 804
Raw data (stat): 798 (minisat+) R 797 20024 20023 0 -1 0 53263 0 0 0 73854 144 0 0 25 0 1 0 546064219 198684672 47682 4294967295 134512640 134672761 3221224544 3221223728 134615919 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48507 47682 603 41 0 48466 0
vsize: 194028
[startup+750.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 804
Raw data (stat): 798 (minisat+) R 797 20024 20023 0 -1 0 53963 0 0 0 74853 145 0 0 25 0 1 0 546064219 201519104 48382 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49199 48382 603 41 0 49158 0
vsize: 196796
[startup+760.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 804
Raw data (stat): 798 (minisat+) R 797 20024 20023 0 -1 0 54686 0 0 0 75851 147 0 0 25 0 1 0 546064219 204533760 49105 4294967295 134512640 134672761 3221224544 3221223728 134615720 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49935 49105 603 41 0 49894 0
vsize: 199740
[startup+770.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 804
Raw data (stat): 798 (minisat+) R 797 20024 20023 0 -1 0 55173 0 0 0 76849 149 0 0 25 0 1 0 546064219 206503936 49592 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 50416 49592 603 41 0 50375 0
vsize: 201664
[startup+780.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 804
Raw data (stat): 798 (minisat+) R 797 20024 20023 0 -1 0 55520 0 0 0 77849 150 0 0 25 0 1 0 546064219 207826944 49939 4294967295 134512640 134672761 3221224544 3221223584 134612682 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 50739 49939 603 41 0 50698 0
vsize: 202956
[startup+790.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 804
Raw data (stat): 798 (minisat+) R 797 20024 20023 0 -1 0 55998 0 0 0 78847 152 0 0 25 0 1 0 546064219 209805312 50417 4294967295 134512640 134672761 3221224544 3221223728 134615929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 51222 50417 603 41 0 51181 0
vsize: 204888
[startup+800.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 804
Raw data (stat): 798 (minisat+) R 797 20024 20023 0 -1 0 56675 0 0 0 79846 154 0 0 25 0 1 0 546064219 212541440 51094 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 51890 51094 603 41 0 51849 0
vsize: 207560
[startup+810.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 804
Raw data (stat): 798 (minisat+) R 797 20024 20023 0 -1 0 57575 0 0 0 80844 156 0 0 25 0 1 0 546064219 216219648 51994 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 52788 51994 603 41 0 52747 0
vsize: 211152
[startup+820.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 804
Raw data (stat): 798 (minisat+) R 797 20024 20023 0 -1 0 58420 0 0 0 81841 158 0 0 25 0 1 0 546064219 219750400 52839 4294967295 134512640 134672761 3221224544 3221223728 134615919 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 53650 52839 603 41 0 53609 0
vsize: 214600
[startup+830.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 804
Raw data (stat): 798 (minisat+) R 797 20024 20023 0 -1 0 59004 0 0 0 82840 159 0 0 25 0 1 0 546064219 222068736 53423 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 54216 53423 603 41 0 54175 0
vsize: 216864
[startup+840.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 804
Raw data (stat): 798 (minisat+) R 797 20024 20023 0 -1 0 59797 0 0 0 83838 162 0 0 25 0 1 0 546064219 225316864 54216 4294967295 134512640 134672761 3221224544 3221223680 134614576 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 55009 54216 603 41 0 54968 0
vsize: 220036
[startup+850.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 804
Raw data (stat): 798 (minisat+) R 797 20024 20023 0 -1 0 60768 0 0 0 84836 164 0 0 25 0 1 0 546064219 229330944 55187 4294967295 134512640 134672761 3221224544 3221223536 134565045 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 55989 55187 603 41 0 55948 0
vsize: 223956
[startup+860.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 804
Raw data (stat): 798 (minisat+) R 797 20024 20023 0 -1 0 62254 0 0 0 85833 168 0 0 25 0 1 0 546064219 233267200 56142 4294967295 134512640 134672761 3221224544 3221223800 134616373 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 56950 56142 603 41 0 56909 0
vsize: 227800
[startup+870.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 804
Raw data (stat): 798 (minisat+) R 797 20024 20023 0 -1 0 62254 0 0 0 86832 168 0 0 25 0 1 0 546064219 233267200 56142 4294967295 134512640 134672761 3221224544 3221223728 134615652 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 56950 56142 603 41 0 56909 0
vsize: 227800
[startup+880.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 804
Raw data (stat): 798 (minisat+) R 797 20024 20023 0 -1 0 62254 0 0 0 87832 168 0 0 25 0 1 0 546064219 233267200 56142 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 56950 56142 603 41 0 56909 0
vsize: 227800
[startup+890.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 804
Raw data (stat): 798 (minisat+) R 797 20024 20023 0 -1 0 62254 0 0 0 88832 168 0 0 25 0 1 0 546064219 233267200 56142 4294967295 134512640 134672761 3221224544 3221223584 134612628 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 56950 56142 603 41 0 56909 0
vsize: 227800
[startup+900.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 804
Raw data (stat): 798 (minisat+) R 797 20024 20023 0 -1 0 62254 0 0 0 89832 168 0 0 25 0 1 0 546064219 233267200 56142 4294967295 134512640 134672761 3221224544 3221223416 1075353072 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 56950 56142 603 41 0 56909 0
vsize: 227800
[startup+910.051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 804
Raw data (stat): 798 (minisat+) R 797 20024 20023 0 -1 0 62254 0 0 0 90832 168 0 0 25 0 1 0 546064219 233267200 56142 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 56950 56142 603 41 0 56909 0
vsize: 227800
[startup+920.051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 804
Raw data (stat): 798 (minisat+) R 797 20024 20023 0 -1 0 62254 0 0 0 91833 168 0 0 25 0 1 0 546064219 233267200 56142 4294967295 134512640 134672761 3221224544 3221223728 134615594 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 56950 56142 603 41 0 56909 0
vsize: 227800
[startup+930.051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 804
Raw data (stat): 798 (minisat+) R 797 20024 20023 0 -1 0 62254 0 0 0 92833 168 0 0 25 0 1 0 546064219 233267200 56142 4294967295 134512640 134672761 3221224544 3221223728 134615676 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 56950 56142 603 41 0 56909 0
vsize: 227800
[startup+940.051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 804
Raw data (stat): 798 (minisat+) R 797 20024 20023 0 -1 0 62254 0 0 0 93833 168 0 0 25 0 1 0 546064219 233267200 56142 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 56950 56142 603 41 0 56909 0
vsize: 227800
[startup+950.051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 804
Raw data (stat): 798 (minisat+) R 797 20024 20023 0 -1 0 62254 0 0 0 94833 168 0 0 25 0 1 0 546064219 233267200 56142 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 56950 56142 603 41 0 56909 0
vsize: 227800
[startup+960.052 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 804
Raw data (stat): 798 (minisat+) R 797 20024 20023 0 -1 0 62254 0 0 0 95833 168 0 0 25 0 1 0 546064219 233267200 56142 4294967295 134512640 134672761 3221224544 3221223584 134612684 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 56950 56142 603 41 0 56909 0
vsize: 227800
[startup+970.053 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 804
Raw data (stat): 798 (minisat+) R 797 20024 20023 0 -1 0 62254 0 0 0 96833 168 0 0 25 0 1 0 546064219 233267200 56142 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 56950 56142 603 41 0 56909 0
vsize: 227800
[startup+980.053 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 804
Raw data (stat): 798 (minisat+) R 797 20024 20023 0 -1 0 62254 0 0 0 97834 168 0 0 25 0 1 0 546064219 233267200 56142 4294967295 134512640 134672761 3221224544 3221223584 134614266 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 56950 56142 603 41 0 56909 0
vsize: 227800
[startup+990.053 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 804
Raw data (stat): 798 (minisat+) R 797 20024 20023 0 -1 0 62254 0 0 0 98834 168 0 0 25 0 1 0 546064219 233267200 56142 4294967295 134512640 134672761 3221224544 3221223728 134615665 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 56950 56142 603 41 0 56909 0
vsize: 227800
[startup+1000.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 804
Raw data (stat): 798 (minisat+) R 797 20024 20023 0 -1 0 62254 0 0 0 99834 168 0 0 25 0 1 0 546064219 233267200 56142 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 56950 56142 603 41 0 56909 0
vsize: 227800
[startup+1010.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 804
Raw data (stat): 798 (minisat+) R 797 20024 20023 0 -1 0 62254 0 0 0 100834 168 0 0 25 0 1 0 546064219 233267200 56142 4294967295 134512640 134672761 3221224544 3221223536 134565127 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 56950 56142 603 41 0 56909 0
vsize: 227800
[startup+1020.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 806
Raw data (stat): 798 (minisat+) R 797 20024 20023 0 -1 0 62254 0 0 0 101834 168 0 0 25 0 1 0 546064219 233267200 56142 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 56950 56142 603 41 0 56909 0
vsize: 227800
[startup+1030.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 806
Raw data (stat): 798 (minisat+) R 797 20024 20023 0 -1 0 62254 0 0 0 102834 168 0 0 25 0 1 0 546064219 233267200 56142 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 56950 56142 603 41 0 56909 0
vsize: 227800
[startup+1040.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 806
Raw data (stat): 798 (minisat+) R 797 20024 20023 0 -1 0 62254 0 0 0 103835 168 0 0 25 0 1 0 546064219 233267200 56142 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 56950 56142 603 41 0 56909 0
vsize: 227800
[startup+1050.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 806
Raw data (stat): 798 (minisat+) R 797 20024 20023 0 -1 0 62254 0 0 0 104835 168 0 0 25 0 1 0 546064219 233267200 56142 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 56950 56142 603 41 0 56909 0
vsize: 227800
[startup+1060.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 806
Raw data (stat): 798 (minisat+) R 797 20024 20023 0 -1 0 62254 0 0 0 105835 168 0 0 25 0 1 0 546064219 233267200 56142 4294967295 134512640 134672761 3221224544 3221223728 134615838 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 56950 56142 603 41 0 56909 0
vsize: 227800
[startup+1070.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 806
Raw data (stat): 798 (minisat+) R 797 20024 20023 0 -1 0 62254 0 0 0 106835 168 0 0 25 0 1 0 546064219 233267200 56142 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 56950 56142 603 41 0 56909 0
vsize: 227800
[startup+1080.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 806
Raw data (stat): 798 (minisat+) R 797 20024 20023 0 -1 0 62254 0 0 0 107835 168 0 0 25 0 1 0 546064219 233267200 56142 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 56950 56142 603 41 0 56909 0
vsize: 227800
[startup+1090.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 806
Raw data (stat): 798 (minisat+) R 797 20024 20023 0 -1 0 62254 0 0 0 108836 168 0 0 25 0 1 0 546064219 233267200 56142 4294967295 134512640 134672761 3221224544 3221223744 134610661 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 56950 56142 603 41 0 56909 0
vsize: 227800
[startup+1100.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 806
Raw data (stat): 798 (minisat+) R 797 20024 20023 0 -1 0 62254 0 0 0 109836 168 0 0 25 0 1 0 546064219 233267200 56142 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 56950 56142 603 41 0 56909 0
vsize: 227800
[startup+1110.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 806
Raw data (stat): 798 (minisat+) R 797 20024 20023 0 -1 0 62254 0 0 0 110836 168 0 0 25 0 1 0 546064219 233267200 56142 4294967295 134512640 134672761 3221224544 3221223584 134612601 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 56950 56142 603 41 0 56909 0
vsize: 227800
[startup+1120.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 806
Raw data (stat): 798 (minisat+) R 797 20024 20023 0 -1 0 62254 0 0 0 111836 168 0 0 25 0 1 0 546064219 233267200 56142 4294967295 134512640 134672761 3221224544 3221223648 134603947 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 56950 56142 603 41 0 56909 0
vsize: 227800
[startup+1130.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 806
Raw data (stat): 798 (minisat+) R 797 20024 20023 0 -1 0 62254 0 0 0 112837 168 0 0 25 0 1 0 546064219 233267200 56142 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 56950 56142 603 41 0 56909 0
vsize: 227800
[startup+1140.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 806
Raw data (stat): 798 (minisat+) R 797 20024 20023 0 -1 0 62254 0 0 0 113837 168 0 0 25 0 1 0 546064219 233267200 56142 4294967295 134512640 134672761 3221224544 3221223584 134614207 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 56950 56142 603 41 0 56909 0
vsize: 227800
[startup+1150.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 806
Raw data (stat): 798 (minisat+) R 797 20024 20023 0 -1 0 62254 0 0 0 114837 168 0 0 25 0 1 0 546064219 233267200 56142 4294967295 134512640 134672761 3221224544 3221223728 134615749 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 56950 56142 603 41 0 56909 0
vsize: 227800
[startup+1160.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 806
Raw data (stat): 798 (minisat+) R 797 20024 20023 0 -1 0 62254 0 0 0 115837 168 0 0 25 0 1 0 546064219 233267200 56142 4294967295 134512640 134672761 3221224544 3221223728 134615749 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 56950 56142 603 41 0 56909 0
vsize: 227800
[startup+1170.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 806
Raw data (stat): 798 (minisat+) R 797 20024 20023 0 -1 0 62254 0 0 0 116837 168 0 0 25 0 1 0 546064219 233267200 56142 4294967295 134512640 134672761 3221224544 3221223584 134612783 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 56950 56142 603 41 0 56909 0
vsize: 227800
[startup+1180.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 806
Raw data (stat): 798 (minisat+) R 797 20024 20023 0 -1 0 62254 0 0 0 117837 168 0 0 25 0 1 0 546064219 233267200 56142 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 56950 56142 603 41 0 56909 0
vsize: 227800
[startup+1190.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 806
Raw data (stat): 798 (minisat+) R 797 20024 20023 0 -1 0 62254 0 0 0 118837 168 0 0 25 0 1 0 546064219 233267200 56142 4294967295 134512640 134672761 3221224544 3221223584 134612614 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 56950 56142 603 41 0 56909 0
vsize: 227800
[startup+1200.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 806
Raw data (stat): 798 (minisat+) R 797 20024 20023 0 -1 0 62254 0 0 0 119838 168 0 0 25 0 1 0 546064219 233267200 56142 4294967295 134512640 134672761 3221224544 3221223728 134615617 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 56950 56142 603 41 0 56909 0
vsize: 227800
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.18 s]
Raw data (loadavg): 0.99 0.97 0.91 1/55 806
Raw data (stat): 798 (minisat+) Z 797 20024 20023 0 -1 12 62255 0 0 0 119838 179 0 0 25 0 1 0 546064219 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.18
CPU time (s): 1200.18
CPU user time (s): 1198.38
CPU system time (s): 1.79573
CPU usage (%): 100
Max. virtual memory (Kb): 227800
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####