PB'05 competition: run trace

Some explanations

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

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

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc29 THE 2005-04-22 00:30:36 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=12946 boxname=wulflinc29 idbench=996 idsolver=11 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  c5ca7819a7dcae16ff6045242cdd1f87  /oldhome/oroussel/tmp/wulflinc29/normalized-mps-v2-20-10-protfold.opb
REAL COMMAND:  minisat+ -S /oldhome/oroussel/tmp/wulflinc29/normalized-mps-v2-20-10-protfold.opb /oldhome/oroussel/tmp/wulflinc29/normalized-mps-v2-20-10-protfold.opb
IDLAUNCH: 12946
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.020
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.020
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:        464500 kB
Buffers:         24224 kB
Cached:         521968 kB
SwapCached:       1616 kB
Active:          66316 kB
Inactive:       482968 kB
HighTotal:      131008 kB
HighFree:         5572 kB
LowTotal:       903652 kB
LowFree:        458928 kB
SwapTotal:     2097892 kB
SwapFree:      2095360 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5092 kB
Slab:            15228 kB
Committed_AS:    63604 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-22 00:50:39 (client local time) WITH STATUS 10 IN 1200.26 SECONDS
stats: 12946 7 1200.26 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.26135 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.58915 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.6441 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.0832 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.8833 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: 190.794 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: 223.328 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: 341.501 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: 859.524 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.94 0.97 0.92 2/54 9932
Raw data (stat): 9932 (runsolver) R 9931 27222 27221 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 549411687 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0003 s]
Raw data (loadavg): 0.95 0.97 0.92 2/54 9932
Raw data (stat): 9932 (minisat+) R 9931 27222 27221 0 -1 0 6944 0 0 0 970 21 0 0 25 0 1 0 549411687 23216128 4885 4294967295 134512640 134672761 3221224544 3221223744 134610707 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.0021 s]
Raw data (loadavg): 0.96 0.97 0.92 2/54 9932
Raw data (stat): 9932 (minisat+) R 9931 27222 27221 0 -1 0 8779 0 0 0 1963 26 0 0 25 0 1 0 549411687 26112000 5602 4294967295 134512640 134672761 3221224544 3221223736 134619688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6375 5602 603 41 0 6334 0
vsize: 25500
[startup+30.0095 s]
Raw data (loadavg): 0.96 0.97 0.92 2/54 9932
Raw data (stat): 9932 (minisat+) R 9931 27222 27221 0 -1 0 9197 0 0 0 2962 27 0 0 25 0 1 0 549411687 27885568 6020 4294967295 134512640 134672761 3221224544 3221223728 134615948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6808 6020 603 41 0 6767 0
vsize: 27232
[startup+40.0126 s]
Raw data (loadavg): 0.97 0.97 0.92 2/54 9932
Raw data (stat): 9932 (minisat+) R 9931 27222 27221 0 -1 0 10260 0 0 0 3959 30 0 0 25 0 1 0 549411687 32206848 7083 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7863 7083 603 41 0 7822 0
vsize: 31452
[startup+50.0134 s]
Raw data (loadavg): 1.05 0.99 0.93 2/54 9932
Raw data (stat): 9932 (minisat+) R 9931 27222 27221 0 -1 0 10843 0 0 0 4957 32 0 0 25 0 1 0 549411687 34734080 7666 4294967295 134512640 134672761 3221224544 3221223376 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8480 7666 603 41 0 8439 0
vsize: 33920
[startup+60.0137 s]
Raw data (loadavg): 1.04 0.99 0.93 2/54 9932
Raw data (stat): 9932 (minisat+) R 9931 27222 27221 0 -1 0 11832 0 0 0 5954 36 0 0 25 0 1 0 549411687 36081664 8025 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8809 8025 603 41 0 8768 0
vsize: 35236
[startup+70.014 s]
Raw data (loadavg): 1.03 0.99 0.93 2/54 9932
Raw data (stat): 9932 (minisat+) R 9931 27222 27221 0 -1 0 12697 0 0 0 6950 39 0 0 25 0 1 0 549411687 39628800 8890 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9675 8890 603 41 0 9634 0
vsize: 38700
[startup+80.0267 s]
Raw data (loadavg): 1.03 0.99 0.93 2/54 9932
Raw data (stat): 9932 (minisat+) R 9931 27222 27221 0 -1 0 13790 0 0 0 7950 41 0 0 25 0 1 0 549411687 44081152 9983 4294967295 134512640 134672761 3221224544 3221223584 134612972 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10762 9983 603 41 0 10721 0
vsize: 43048
[startup+90.0278 s]
Raw data (loadavg): 1.02 0.99 0.93 2/54 9932
Raw data (stat): 9932 (minisat+) R 9931 27222 27221 0 -1 0 14451 0 0 0 8947 43 0 0 25 0 1 0 549411687 46809088 10644 4294967295 134512640 134672761 3221224544 3221223728 134616001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11428 10644 603 41 0 11387 0
vsize: 45712
[startup+100.033 s]
Raw data (loadavg): 1.02 0.99 0.93 2/54 9932
Raw data (stat): 9932 (minisat+) R 9931 27222 27221 0 -1 0 15298 0 0 0 9946 46 0 0 25 0 1 0 549411687 50233344 11491 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12264 11491 603 41 0 12223 0
vsize: 49056
[startup+110.037 s]
Raw data (loadavg): 1.02 0.99 0.93 2/54 9932
Raw data (stat): 9932 (minisat+) R 9931 27222 27221 0 -1 0 15966 0 0 0 10945 47 0 0 25 0 1 0 549411687 53010432 12159 4294967295 134512640 134672761 3221224544 3221223536 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12942 12159 603 41 0 12901 0
vsize: 51768
[startup+120.04 s]
Raw data (loadavg): 1.01 0.99 0.93 2/54 9932
Raw data (stat): 9932 (minisat+) R 9931 27222 27221 0 -1 0 16927 0 0 0 11943 49 0 0 25 0 1 0 549411687 57077760 13120 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13935 13120 603 41 0 13894 0
vsize: 55740
[startup+130.051 s]
Raw data (loadavg): 1.01 0.99 0.93 2/54 9932
Raw data (stat): 9932 (minisat+) R 9931 27222 27221 0 -1 0 18072 0 0 0 12942 52 0 0 25 0 1 0 549411687 61792256 14265 4294967295 134512640 134672761 3221224544 3221223584 134612684 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15086 14268 603 41 0 15045 0
vsize: 60344
[startup+140.051 s]
Raw data (loadavg): 1.01 0.99 0.93 2/54 9932
Raw data (stat): 9932 (minisat+) R 9931 27222 27221 0 -1 0 19215 0 0 0 13938 56 0 0 25 0 1 0 549411687 66490368 15408 4294967295 134512640 134672761 3221224544 3221223696 134565086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16233 15408 603 41 0 16192 0
vsize: 64932
[startup+150.052 s]
Raw data (loadavg): 1.01 0.99 0.93 2/54 9932
Raw data (stat): 9932 (minisat+) R 9931 27222 27221 0 -1 0 20323 0 0 0 14936 58 0 0 25 0 1 0 549411687 70914048 16516 4294967295 134512640 134672761 3221224544 3221223648 134604543 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17313 16516 603 41 0 17272 0
vsize: 69252
[startup+160.052 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 9932
Raw data (stat): 9932 (minisat+) R 9931 27222 27221 0 -1 0 21147 0 0 0 15933 61 0 0 25 0 1 0 549411687 74301440 17340 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18140 17340 603 41 0 18099 0
vsize: 72560
[startup+170.053 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 9932
Raw data (stat): 9932 (minisat+) R 9931 27222 27221 0 -1 0 21966 0 0 0 16932 63 0 0 25 0 1 0 549411687 77713408 18159 4294967295 134512640 134672761 3221224544 3221223728 134615708 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18973 18159 603 41 0 18932 0
vsize: 75892
[startup+180.053 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 9932
Raw data (stat): 9932 (minisat+) R 9931 27222 27221 0 -1 0 22839 0 0 0 17929 65 0 0 25 0 1 0 549411687 81219584 19032 4294967295 134512640 134672761 3221224544 3221223728 134615940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19829 19032 603 41 0 19788 0
vsize: 79316
[startup+190.054 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 9932
Raw data (stat): 9932 (minisat+) R 9931 27222 27221 0 -1 0 23809 0 0 0 18926 69 0 0 25 0 1 0 549411687 85262336 20002 4294967295 134512640 134672761 3221224544 3221223584 134614280 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20816 20002 603 41 0 20775 0
vsize: 83264
[startup+200.054 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 9932
Raw data (stat): 9932 (minisat+) R 9931 27222 27221 0 -1 0 24768 0 0 0 19922 73 0 0 25 0 1 0 549411687 87265280 20510 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21305 20510 603 41 0 21264 0
vsize: 85220
[startup+210.054 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 9932
Raw data (stat): 9932 (minisat+) R 9931 27222 27221 0 -1 0 24768 0 0 0 20921 73 0 0 25 0 1 0 549411687 87265280 20510 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21305 20510 603 41 0 21264 0
vsize: 85220
[startup+220.055 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 9932
Raw data (stat): 9932 (minisat+) R 9931 27222 27221 0 -1 0 24768 0 0 0 21922 73 0 0 25 0 1 0 549411687 87265280 20510 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21305 20510 603 41 0 21264 0
vsize: 85220
[startup+230.055 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 9932
Raw data (stat): 9932 (minisat+) R 9931 27222 27221 0 -1 0 25344 0 0 0 22920 75 0 0 25 0 1 0 549411687 86306816 20294 4294967295 134512640 134672761 3221224544 3221223744 134610707 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.055 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 9932
Raw data (stat): 9932 (minisat+) R 9931 27222 27221 0 -1 0 25344 0 0 0 23920 75 0 0 25 0 1 0 549411687 86306816 20294 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21071 20294 603 41 0 21030 0
vsize: 84284
[startup+250.056 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 9932
Raw data (stat): 9932 (minisat+) R 9931 27222 27221 0 -1 0 25344 0 0 0 24920 75 0 0 25 0 1 0 549411687 86306816 20294 4294967295 134512640 134672761 3221224544 3221223728 134615838 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21071 20294 603 41 0 21030 0
vsize: 84284
[startup+260.056 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 9932
Raw data (stat): 9932 (minisat+) R 9931 27222 27221 0 -1 0 25344 0 0 0 25920 75 0 0 25 0 1 0 549411687 86306816 20294 4294967295 134512640 134672761 3221224544 3221223728 134615758 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21071 20294 603 41 0 21030 0
vsize: 84284
[startup+270.056 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 9932
Raw data (stat): 9932 (minisat+) R 9931 27222 27221 0 -1 0 25344 0 0 0 26920 75 0 0 25 0 1 0 549411687 86306816 20294 4294967295 134512640 134672761 3221224544 3221223536 134565098 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21071 20294 603 41 0 21030 0
vsize: 84284
[startup+280.056 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 9932
Raw data (stat): 9932 (minisat+) R 9931 27222 27221 0 -1 0 25344 0 0 0 27920 75 0 0 25 0 1 0 549411687 86306816 20294 4294967295 134512640 134672761 3221224544 3221223584 134614274 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21071 20294 603 41 0 21030 0
vsize: 84284
[startup+290.056 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 9932
Raw data (stat): 9932 (minisat+) R 9931 27222 27221 0 -1 0 25344 0 0 0 28921 75 0 0 25 0 1 0 549411687 86306816 20294 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21071 20294 603 41 0 21030 0
vsize: 84284
[startup+300.056 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 9932
Raw data (stat): 9932 (minisat+) R 9931 27222 27221 0 -1 0 25344 0 0 0 29921 75 0 0 25 0 1 0 549411687 86306816 20294 4294967295 134512640 134672761 3221224544 3221223728 134615627 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21071 20294 603 41 0 21030 0
vsize: 84284
[startup+310.056 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 9932
Raw data (stat): 9932 (minisat+) R 9931 27222 27221 0 -1 0 25344 0 0 0 30921 75 0 0 25 0 1 0 549411687 86306816 20294 4294967295 134512640 134672761 3221224544 3221223584 134614280 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21071 20294 603 41 0 21030 0
vsize: 84284
[startup+320.057 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 9932
Raw data (stat): 9932 (minisat+) R 9931 27222 27221 0 -1 0 25344 0 0 0 31921 75 0 0 25 0 1 0 549411687 86306816 20294 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21071 20294 603 41 0 21030 0
vsize: 84284
[startup+330.056 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 9932
Raw data (stat): 9932 (minisat+) R 9931 27222 27221 0 -1 0 25373 0 0 0 32921 75 0 0 25 0 1 0 549411687 86437888 20323 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21103 20323 603 41 0 21062 0
vsize: 84412
[startup+340.057 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 9932
Raw data (stat): 9932 (minisat+) R 9931 27222 27221 0 -1 0 26246 0 0 0 33919 77 0 0 25 0 1 0 549411687 90120192 21196 4294967295 134512640 134672761 3221224544 3221223584 134603527 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22002 21196 603 41 0 21961 0
vsize: 88008
[startup+350.057 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 9932
Raw data (stat): 9932 (minisat+) R 9931 27222 27221 0 -1 0 27372 0 0 0 34915 81 0 0 25 0 1 0 549411687 92520448 21791 4294967295 134512640 134672761 3221224544 3221223728 134615594 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.057 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 9932
Raw data (stat): 9932 (minisat+) R 9931 27222 27221 0 -1 0 27372 0 0 0 35915 81 0 0 25 0 1 0 549411687 92520448 21791 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22588 21791 603 41 0 22547 0
vsize: 90352
[startup+370.071 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 9932
Raw data (stat): 9932 (minisat+) R 9931 27222 27221 0 -1 0 27372 0 0 0 36916 81 0 0 25 0 1 0 549411687 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+380.071 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 9932
Raw data (stat): 9932 (minisat+) R 9931 27222 27221 0 -1 0 27372 0 0 0 37916 81 0 0 25 0 1 0 549411687 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+390.072 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 9932
Raw data (stat): 9932 (minisat+) R 9931 27222 27221 0 -1 0 27372 0 0 0 38917 81 0 0 25 0 1 0 549411687 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.072 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 9932
Raw data (stat): 9932 (minisat+) R 9931 27222 27221 0 -1 0 27372 0 0 0 39916 81 0 0 25 0 1 0 549411687 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+410.072 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 9932
Raw data (stat): 9932 (minisat+) R 9931 27222 27221 0 -1 0 27372 0 0 0 40916 81 0 0 25 0 1 0 549411687 92520448 21791 4294967295 134512640 134672761 3221224544 3221223744 134610661 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22588 21791 603 41 0 22547 0
vsize: 90352
[startup+420.071 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 9932
Raw data (stat): 9932 (minisat+) R 9931 27222 27221 0 -1 0 27373 0 0 0 41916 81 0 0 25 0 1 0 549411687 92520448 21792 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22588 21792 603 41 0 22547 0
vsize: 90352
[startup+430.072 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 9932
Raw data (stat): 9932 (minisat+) R 9931 27222 27221 0 -1 0 27373 0 0 0 42916 81 0 0 25 0 1 0 549411687 92520448 21792 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22588 21792 603 41 0 22547 0
vsize: 90352
[startup+440.072 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 9932
Raw data (stat): 9932 (minisat+) R 9931 27222 27221 0 -1 0 27373 0 0 0 43916 81 0 0 25 0 1 0 549411687 92520448 21792 4294967295 134512640 134672761 3221224544 3221223728 134615749 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22588 21792 603 41 0 22547 0
vsize: 90352
[startup+450.072 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 9932
Raw data (stat): 9932 (minisat+) R 9931 27222 27221 0 -1 0 27373 0 0 0 44916 81 0 0 25 0 1 0 549411687 92520448 21792 4294967295 134512640 134672761 3221224544 3221223680 134614690 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22588 21792 603 41 0 22547 0
vsize: 90352
[startup+460.072 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 9932
Raw data (stat): 9932 (minisat+) R 9931 27222 27221 0 -1 0 27373 0 0 0 45917 81 0 0 25 0 1 0 549411687 92520448 21792 4294967295 134512640 134672761 3221224544 3221223728 134615741 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22588 21792 603 41 0 22547 0
vsize: 90352
[startup+470.072 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 9932
Raw data (stat): 9932 (minisat+) R 9931 27222 27221 0 -1 0 27817 0 0 0 46915 83 0 0 25 0 1 0 549411687 94343168 22236 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23033 22236 603 41 0 22992 0
vsize: 92132
[startup+480.072 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 9932
Raw data (stat): 9932 (minisat+) R 9931 27222 27221 0 -1 0 28851 0 0 0 47913 85 0 0 25 0 1 0 549411687 98537472 23270 4294967295 134512640 134672761 3221224544 3221223728 134615732 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24057 23270 603 41 0 24016 0
vsize: 96228
[startup+490.077 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 9932
Raw data (stat): 9932 (minisat+) R 9931 27222 27221 0 -1 0 29855 0 0 0 48911 87 0 0 25 0 1 0 549411687 102723584 24274 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25079 24274 603 41 0 25038 0
vsize: 100316
[startup+500.077 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 9932
Raw data (stat): 9932 (minisat+) R 9931 27222 27221 0 -1 0 30846 0 0 0 49909 90 0 0 25 0 1 0 549411687 106741760 25265 4294967295 134512640 134672761 3221224544 3221223728 134615919 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26060 25265 603 41 0 26019 0
vsize: 104240
[startup+510.077 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 9932
Raw data (stat): 9932 (minisat+) R 9931 27222 27221 0 -1 0 32108 0 0 0 50906 93 0 0 25 0 1 0 549411687 111828992 26527 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27302 26527 603 41 0 27261 0
vsize: 109208
[startup+520.09 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 9932
Raw data (stat): 9932 (minisat+) R 9931 27222 27221 0 -1 0 33031 0 0 0 51905 95 0 0 25 0 1 0 549411687 115617792 27450 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28227 27450 603 41 0 28186 0
vsize: 112908
[startup+530.099 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 9932
Raw data (stat): 9932 (minisat+) R 9931 27222 27221 0 -1 0 33979 0 0 0 52904 97 0 0 25 0 1 0 549411687 119508992 28398 4294967295 134512640 134672761 3221224544 3221223680 134614741 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29177 28398 603 41 0 29136 0
vsize: 116708
[startup+540.1 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 9932
Raw data (stat): 9932 (minisat+) R 9931 27222 27221 0 -1 0 34855 0 0 0 53902 99 0 0 25 0 1 0 549411687 123154432 29274 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30067 29274 603 41 0 30026 0
vsize: 120268
[startup+550.1 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 9932
Raw data (stat): 9932 (minisat+) R 9931 27222 27221 0 -1 0 35823 0 0 0 54900 101 0 0 25 0 1 0 549411687 127078400 30242 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31025 30242 603 41 0 30984 0
vsize: 124100
[startup+560.1 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 9932
Raw data (stat): 9932 (minisat+) R 9931 27222 27221 0 -1 0 36913 0 0 0 55898 104 0 0 25 0 1 0 549411687 131522560 31332 4294967295 134512640 134672761 3221224544 3221223356 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32110 31333 603 41 0 32069 0
vsize: 128440
[startup+570.101 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 9932
Raw data (stat): 9932 (minisat+) R 9931 27222 27221 0 -1 0 37924 0 0 0 56895 107 0 0 25 0 1 0 549411687 135598080 32343 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33105 32343 603 41 0 33064 0
vsize: 132420
[startup+580.1 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 9932
Raw data (stat): 9932 (minisat+) R 9931 27222 27221 0 -1 0 38931 0 0 0 57893 109 0 0 25 0 1 0 549411687 139780096 33350 4294967295 134512640 134672761 3221224544 3221223728 134615720 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34126 33350 603 41 0 34085 0
vsize: 136504
[startup+590.101 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 9932
Raw data (stat): 9932 (minisat+) R 9931 27222 27221 0 -1 0 39831 0 0 0 58891 111 0 0 25 0 1 0 549411687 143405056 34250 4294967295 134512640 134672761 3221224544 3221223728 134616005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35011 34250 603 41 0 34970 0
vsize: 140044
[startup+600.102 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 9932
Raw data (stat): 9932 (minisat+) R 9931 27222 27221 0 -1 0 40675 0 0 0 59890 113 0 0 25 0 1 0 549411687 147206144 35094 4294967295 134512640 134672761 3221224544 3221223728 134615608 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35939 35094 603 41 0 35898 0
vsize: 143756
[startup+610.102 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 9932
Raw data (stat): 9932 (minisat+) R 9931 27222 27221 0 -1 0 41550 0 0 0 60888 115 0 0 25 0 1 0 549411687 150757376 35969 4294967295 134512640 134672761 3221224544 3221223728 134615794 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36806 35969 603 41 0 36765 0
vsize: 147224
[startup+620.102 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 9932
Raw data (stat): 9932 (minisat+) R 9931 27222 27221 0 -1 0 42407 0 0 0 61886 117 0 0 25 0 1 0 549411687 154296320 36826 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37670 36826 603 41 0 37629 0
vsize: 150680
[startup+630.102 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 9932
Raw data (stat): 9932 (minisat+) R 9931 27222 27221 0 -1 0 43288 0 0 0 62885 119 0 0 25 0 1 0 549411687 157802496 37707 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38526 37707 603 41 0 38485 0
vsize: 154104
[startup+640.103 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 9932
Raw data (stat): 9932 (minisat+) R 9931 27222 27221 0 -1 0 44245 0 0 0 63882 122 0 0 25 0 1 0 549411687 161718272 38664 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39482 38664 603 41 0 39441 0
vsize: 157928
[startup+650.102 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 9932
Raw data (stat): 9932 (minisat+) R 9931 27222 27221 0 -1 0 45182 0 0 0 64880 123 0 0 25 0 1 0 549411687 165597184 39601 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40429 39601 603 41 0 40388 0
vsize: 161716
[startup+660.103 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 9932
Raw data (stat): 9932 (minisat+) R 9931 27222 27221 0 -1 0 45932 0 0 0 65879 125 0 0 25 0 1 0 549411687 168726528 40351 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41193 40351 603 41 0 41152 0
vsize: 164772
[startup+670.103 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 9932
Raw data (stat): 9932 (minisat+) R 9931 27222 27221 0 -1 0 46727 0 0 0 66877 127 0 0 25 0 1 0 549411687 171974656 41146 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41986 41146 603 41 0 41945 0
vsize: 167944
[startup+680.103 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 9932
Raw data (stat): 9932 (minisat+) R 9931 27222 27221 0 -1 0 47714 0 0 0 67874 130 0 0 25 0 1 0 549411687 176017408 42133 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42973 42133 603 41 0 42932 0
vsize: 171892
[startup+690.104 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 9932
Raw data (stat): 9932 (minisat+) R 9931 27222 27221 0 -1 0 48773 0 0 0 68872 132 0 0 25 0 1 0 549411687 180301824 43192 4294967295 134512640 134672761 3221224544 3221223584 134613822 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44019 43192 603 41 0 43978 0
vsize: 176076
[startup+700.104 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 9932
Raw data (stat): 9932 (minisat+) R 9931 27222 27221 0 -1 0 49661 0 0 0 69870 134 0 0 25 0 1 0 549411687 183939072 44080 4294967295 134512640 134672761 3221224544 3221223584 134603512 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44907 44080 603 41 0 44866 0
vsize: 179628
[startup+710.104 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 9932
Raw data (stat): 9932 (minisat+) R 9931 27222 27221 0 -1 0 50694 0 0 0 70868 137 0 0 25 0 1 0 549411687 188125184 45113 4294967295 134512640 134672761 3221224544 3221223728 134615801 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45929 45113 603 41 0 45888 0
vsize: 183716
[startup+720.104 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 9932
Raw data (stat): 9932 (minisat+) R 9931 27222 27221 0 -1 0 51302 0 0 0 71866 139 0 0 25 0 1 0 549411687 190627840 45721 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46540 45721 603 41 0 46499 0
vsize: 186160
[startup+730.105 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 9932
Raw data (stat): 9932 (minisat+) R 9931 27222 27221 0 -1 0 52086 0 0 0 72865 141 0 0 25 0 1 0 549411687 193867776 46505 4294967295 134512640 134672761 3221224544 3221223728 134615720 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47331 46505 603 41 0 47290 0
vsize: 189324
[startup+740.106 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 9932
Raw data (stat): 9932 (minisat+) R 9931 27222 27221 0 -1 0 53119 0 0 0 73863 143 0 0 25 0 1 0 549411687 198037504 47538 4294967295 134512640 134672761 3221224544 3221223584 134612478 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48349 47540 603 41 0 48308 0
vsize: 193396
[startup+750.106 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 9932
Raw data (stat): 9932 (minisat+) R 9931 27222 27221 0 -1 0 53882 0 0 0 74861 145 0 0 25 0 1 0 549411687 201134080 48301 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 49105 48301 603 41 0 49064 0
vsize: 196420
[startup+760.106 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 9932
Raw data (stat): 9932 (minisat+) R 9931 27222 27221 0 -1 0 54571 0 0 0 75859 147 0 0 25 0 1 0 549411687 204013568 48990 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 49808 48990 603 41 0 49767 0
vsize: 199232
[startup+770.106 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 9932
Raw data (stat): 9932 (minisat+) R 9931 27222 27221 0 -1 0 55110 0 0 0 76858 148 0 0 25 0 1 0 549411687 206241792 49529 4294967295 134512640 134672761 3221224544 3221223584 134612981 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 50352 49529 603 41 0 50311 0
vsize: 201408
[startup+780.106 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 9932
Raw data (stat): 9932 (minisat+) R 9931 27222 27221 0 -1 0 55463 0 0 0 77856 150 0 0 25 0 1 0 549411687 207695872 49882 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 50707 49882 603 41 0 50666 0
vsize: 202828
[startup+790.107 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 9932
Raw data (stat): 9932 (minisat+) R 9931 27222 27221 0 -1 0 55912 0 0 0 78855 151 0 0 25 0 1 0 549411687 209543168 50331 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 51158 50332 603 41 0 51117 0
vsize: 204632
[startup+800.107 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 9932
Raw data (stat): 9932 (minisat+) R 9931 27222 27221 0 -1 0 56549 0 0 0 79853 153 0 0 25 0 1 0 549411687 212025344 50968 4294967295 134512640 134672761 3221224544 3221223728 134615683 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 51764 50968 603 41 0 51723 0
vsize: 207056
[startup+810.107 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 9932
Raw data (stat): 9932 (minisat+) R 9931 27222 27221 0 -1 0 57432 0 0 0 80851 156 0 0 25 0 1 0 549411687 215699456 51851 4294967295 134512640 134672761 3221224544 3221223784 134612357 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 52661 51851 603 41 0 52620 0
vsize: 210644
[startup+820.108 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 9932
Raw data (stat): 9932 (minisat+) R 9931 27222 27221 0 -1 0 58290 0 0 0 81849 158 0 0 25 0 1 0 549411687 219222016 52709 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 53521 52709 603 41 0 53480 0
vsize: 214084
[startup+830.108 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 9932
Raw data (stat): 9932 (minisat+) R 9931 27222 27221 0 -1 0 58953 0 0 0 82846 161 0 0 25 0 1 0 549411687 221945856 53372 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 54186 53372 603 41 0 54145 0
vsize: 216744
[startup+840.109 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 9932
Raw data (stat): 9932 (minisat+) R 9931 27222 27221 0 -1 0 59620 0 0 0 83845 163 0 0 25 0 1 0 549411687 224657408 54039 4294967295 134512640 134672761 3221224544 3221223744 134610654 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 54848 54039 603 41 0 54807 0
vsize: 219392
[startup+850.109 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 9932
Raw data (stat): 9932 (minisat+) R 9931 27222 27221 0 -1 0 60717 0 0 0 84841 167 0 0 25 0 1 0 549411687 229195776 55136 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55956 55136 603 41 0 55915 0
vsize: 223824
[startup+860.108 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 9932
Raw data (stat): 9932 (minisat+) R 9931 27222 27221 0 -1 0 61290 0 0 0 85840 168 0 0 25 0 1 0 549411687 231424000 55709 4294967295 134512640 134672761 3221224544 3221223728 134615741 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 56500 55709 603 41 0 56459 0
vsize: 226000
[startup+870.109 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 9932
Raw data (stat): 9932 (minisat+) R 9931 27222 27221 0 -1 0 62254 0 0 0 86836 171 0 0 25 0 1 0 549411687 233267200 56142 4294967295 134512640 134672761 3221224544 3221223728 134615625 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.109 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 9932
Raw data (stat): 9932 (minisat+) R 9931 27222 27221 0 -1 0 62254 0 0 0 87836 171 0 0 25 0 1 0 549411687 233267200 56142 4294967295 134512640 134672761 3221224544 3221223728 134615711 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 56950 56142 603 41 0 56909 0
vsize: 227800
[startup+890.109 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 9932
Raw data (stat): 9932 (minisat+) R 9931 27222 27221 0 -1 0 62254 0 0 0 88837 171 0 0 25 0 1 0 549411687 233267200 56142 4294967295 134512640 134672761 3221224544 3221223728 134615948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 56950 56142 603 41 0 56909 0
vsize: 227800
[startup+900.11 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 9932
Raw data (stat): 9932 (minisat+) R 9931 27222 27221 0 -1 0 62254 0 0 0 89837 171 0 0 25 0 1 0 549411687 233267200 56142 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 56950 56142 603 41 0 56909 0
vsize: 227800
[startup+910.11 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 9932
Raw data (stat): 9932 (minisat+) R 9931 27222 27221 0 -1 0 62254 0 0 0 90837 171 0 0 25 0 1 0 549411687 233267200 56142 4294967295 134512640 134672761 3221224544 3221223680 134614690 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 56950 56142 603 41 0 56909 0
vsize: 227800
[startup+920.111 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 9932
Raw data (stat): 9932 (minisat+) R 9931 27222 27221 0 -1 0 62254 0 0 0 91837 171 0 0 25 0 1 0 549411687 233267200 56142 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 56950 56142 603 41 0 56909 0
vsize: 227800
[startup+930.111 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 9932
Raw data (stat): 9932 (minisat+) R 9931 27222 27221 0 -1 0 62254 0 0 0 92837 171 0 0 25 0 1 0 549411687 233267200 56142 4294967295 134512640 134672761 3221224544 3221223728 134615732 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 56950 56142 603 41 0 56909 0
vsize: 227800
[startup+940.111 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 9932
Raw data (stat): 9932 (minisat+) R 9931 27222 27221 0 -1 0 62254 0 0 0 93838 171 0 0 25 0 1 0 549411687 233267200 56142 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 56950 56142 603 41 0 56909 0
vsize: 227800
[startup+950.111 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 9932
Raw data (stat): 9932 (minisat+) R 9931 27222 27221 0 -1 0 62254 0 0 0 94838 171 0 0 25 0 1 0 549411687 233267200 56142 4294967295 134512640 134672761 3221224544 3221223744 134610688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 56950 56142 603 41 0 56909 0
vsize: 227800
[startup+960.111 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 9932
Raw data (stat): 9932 (minisat+) R 9931 27222 27221 0 -1 0 62254 0 0 0 95838 171 0 0 25 0 1 0 549411687 233267200 56142 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 56950 56142 603 41 0 56909 0
vsize: 227800
[startup+970.112 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 9932
Raw data (stat): 9932 (minisat+) R 9931 27222 27221 0 -1 0 62254 0 0 0 96838 171 0 0 25 0 1 0 549411687 233267200 56142 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 56950 56142 603 41 0 56909 0
vsize: 227800
[startup+980.111 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 9932
Raw data (stat): 9932 (minisat+) R 9931 27222 27221 0 -1 0 62254 0 0 0 97838 171 0 0 25 0 1 0 549411687 233267200 56142 4294967295 134512640 134672761 3221224544 3221223728 134615804 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 56950 56142 603 41 0 56909 0
vsize: 227800
[startup+990.112 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 9932
Raw data (stat): 9932 (minisat+) R 9931 27222 27221 0 -1 0 62254 0 0 0 98839 171 0 0 25 0 1 0 549411687 233267200 56142 4294967295 134512640 134672761 3221224544 3221223728 134615828 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 56950 56142 603 41 0 56909 0
vsize: 227800
[startup+1000.11 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 9932
Raw data (stat): 9932 (minisat+) R 9931 27222 27221 0 -1 0 62254 0 0 0 99839 171 0 0 25 0 1 0 549411687 233267200 56142 4294967295 134512640 134672761 3221224544 3221223584 134613818 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 56950 56142 603 41 0 56909 0
vsize: 227800
[startup+1010.11 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 9932
Raw data (stat): 9932 (minisat+) R 9931 27222 27221 0 -1 0 62254 0 0 0 100839 171 0 0 25 0 1 0 549411687 233267200 56142 4294967295 134512640 134672761 3221224544 3221223728 134615739 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 56950 56142 603 41 0 56909 0
vsize: 227800
[startup+1020.11 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 9932
Raw data (stat): 9932 (minisat+) R 9931 27222 27221 0 -1 0 62254 0 0 0 101839 171 0 0 25 0 1 0 549411687 233267200 56142 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 56950 56142 603 41 0 56909 0
vsize: 227800
[startup+1030.11 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 9932
Raw data (stat): 9932 (minisat+) R 9931 27222 27221 0 -1 0 62254 0 0 0 102839 171 0 0 25 0 1 0 549411687 233267200 56142 4294967295 134512640 134672761 3221224544 3221223728 134615739 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 56950 56142 603 41 0 56909 0
vsize: 227800
[startup+1040.11 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 9932
Raw data (stat): 9932 (minisat+) R 9931 27222 27221 0 -1 0 62254 0 0 0 103840 171 0 0 25 0 1 0 549411687 233267200 56142 4294967295 134512640 134672761 3221224544 3221223728 134615758 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 56950 56142 603 41 0 56909 0
vsize: 227800
[startup+1050.11 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 9932
Raw data (stat): 9932 (minisat+) R 9931 27222 27221 0 -1 0 62254 0 0 0 104840 171 0 0 25 0 1 0 549411687 233267200 56142 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 56950 56142 603 41 0 56909 0
vsize: 227800
[startup+1060.11 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 9932
Raw data (stat): 9932 (minisat+) R 9931 27222 27221 0 -1 0 62254 0 0 0 105840 171 0 0 25 0 1 0 549411687 233267200 56142 4294967295 134512640 134672761 3221224544 3221223728 134615671 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 56950 56142 603 41 0 56909 0
vsize: 227800
[startup+1070.11 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 9932
Raw data (stat): 9932 (minisat+) R 9931 27222 27221 0 -1 0 62254 0 0 0 106840 171 0 0 25 0 1 0 549411687 233267200 56142 4294967295 134512640 134672761 3221224544 3221223728 134615627 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 56950 56142 603 41 0 56909 0
vsize: 227800
[startup+1080.11 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 9932
Raw data (stat): 9932 (minisat+) R 9931 27222 27221 0 -1 0 62254 0 0 0 107840 171 0 0 25 0 1 0 549411687 233267200 56142 4294967295 134512640 134672761 3221224544 3221223744 134610686 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 56950 56142 603 41 0 56909 0
vsize: 227800
[startup+1090.11 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 9932
Raw data (stat): 9932 (minisat+) R 9931 27222 27221 0 -1 0 62254 0 0 0 108840 171 0 0 25 0 1 0 549411687 233267200 56142 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 56950 56142 603 41 0 56909 0
vsize: 227800
[startup+1100.11 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 9932
Raw data (stat): 9932 (minisat+) R 9931 27222 27221 0 -1 0 62254 0 0 0 109841 171 0 0 25 0 1 0 549411687 233267200 56142 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 56950 56142 603 41 0 56909 0
vsize: 227800
[startup+1110.11 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 9932
Raw data (stat): 9932 (minisat+) R 9931 27222 27221 0 -1 0 62254 0 0 0 110841 171 0 0 25 0 1 0 549411687 233267200 56142 4294967295 134512640 134672761 3221224544 3221223728 134615673 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 56950 56142 603 41 0 56909 0
vsize: 227800
[startup+1120.12 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 9932
Raw data (stat): 9932 (minisat+) R 9931 27222 27221 0 -1 0 62254 0 0 0 111841 171 0 0 25 0 1 0 549411687 233267200 56142 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 56950 56142 603 41 0 56909 0
vsize: 227800
[startup+1130.12 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 9932
Raw data (stat): 9932 (minisat+) R 9931 27222 27221 0 -1 0 62254 0 0 0 112841 171 0 0 25 0 1 0 549411687 233267200 56142 4294967295 134512640 134672761 3221224544 3221223708 134614476 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 56950 56142 603 41 0 56909 0
vsize: 227800
[startup+1140.12 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 9932
Raw data (stat): 9932 (minisat+) R 9931 27222 27221 0 -1 0 62254 0 0 0 113841 171 0 0 25 0 1 0 549411687 233267200 56142 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 56950 56142 603 41 0 56909 0
vsize: 227800
[startup+1150.12 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 9932
Raw data (stat): 9932 (minisat+) R 9931 27222 27221 0 -1 0 62254 0 0 0 114842 171 0 0 25 0 1 0 549411687 233267200 56142 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 56950 56142 603 41 0 56909 0
vsize: 227800
[startup+1160.11 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 9932
Raw data (stat): 9932 (minisat+) R 9931 27222 27221 0 -1 0 62254 0 0 0 115842 171 0 0 25 0 1 0 549411687 233267200 56142 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 56950 56142 603 41 0 56909 0
vsize: 227800
[startup+1170.11 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 9932
Raw data (stat): 9932 (minisat+) R 9931 27222 27221 0 -1 0 62254 0 0 0 116842 171 0 0 25 0 1 0 549411687 233267200 56142 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 56950 56142 603 41 0 56909 0
vsize: 227800
[startup+1180.12 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 9932
Raw data (stat): 9932 (minisat+) R 9931 27222 27221 0 -1 0 62254 0 0 0 117842 171 0 0 25 0 1 0 549411687 233267200 56142 4294967295 134512640 134672761 3221224544 3221223584 134613012 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 56950 56142 603 41 0 56909 0
vsize: 227800
[startup+1190.11 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 9932
Raw data (stat): 9932 (minisat+) R 9931 27222 27221 0 -1 0 62254 0 0 0 118842 171 0 0 25 0 1 0 549411687 233267200 56142 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 56950 56142 603 41 0 56909 0
vsize: 227800
[startup+1200.12 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 9932
Raw data (stat): 9932 (minisat+) R 9931 27222 27221 0 -1 0 62254 0 0 0 119842 171 0 0 25 0 1 0 549411687 233267200 56142 4294967295 134512640 134672761 3221224544 3221223728 134615720 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 56950 56142 603 41 0 56909 0
vsize: 227800
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.23 s]
Raw data (loadavg): 1.00 0.99 0.93 1/54 9932
Raw data (stat): 9932 (minisat+) Z 9931 27222 27221 0 -1 12 62255 0 0 0 119843 182 0 0 25 0 1 0 549411687 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.23
CPU time (s): 1200.26
CPU user time (s): 1198.43
CPU system time (s): 1.82572
CPU usage (%): 100.002
Max. virtual memory (Kb): 227800
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####