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:
  1. 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.
  2. SOLVER DATA
    This is the output of the solver (stdout and stderr).
    Note that some very long lines in this section may be truncated by your web browser !
  3. 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.
  4. 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

Namesubmitted/manquinho/ttp/normalized-data6_3.opb
MD5SUM3ce91e964f348d481da3f7741c5768eb
Bench Categoryoptimization, small integers (OPTSMALLINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function 25102
Optimality of the best value was proved NO
Number of terms in the objective function 180
Biggest coefficient in the objective function 1380
Number of bits for the biggest coefficient in the objective function 11
Sum of the numbers in the objective function 116904
Number of bits of the sum of numbers in the objective function 17
Biggest number in a constraint 1380
Number of bits of the biggest number in a constraint 11
Biggest sum of numbers in a constraint 116904
Number of bits of the biggest sum of numbers17
Best result obtained on this benchmarkSAT
Best CPU time to get the best result obtained on this benchmark1189.02
Number of variables540
Total number of constraints4476
Number of constraints which are clauses2532
Number of constraints which are cardinality constraints (but not clauses)264
Number of constraints which are nor clauses,nor cardinality constraints1680
Minimum length of a constraint2
Maximum length of a constraint20

Trace number 2235

Launcher Data

LAUNCH ON wulflinc31 THE 2005-09-18 18:12:27 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=2605 boxname=wulflinc31 idbench=261 idsolver=3 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  3ce91e964f348d481da3f7741c5768eb  /oldhome/oroussel/tmp/wulflinc31/normalized-data6_3.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc31/normalized-data6_3.opb
IDLAUNCH: 2605
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.153
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 888.83

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        692128 kB
Buffers:         35940 kB
Cached:         275844 kB
SwapCached:       1016 kB
Active:         105744 kB
Inactive:       208808 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        691876 kB
SwapTotal:     2097892 kB
SwapFree:      2096404 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5772 kB
Slab:            22296 kB
Committed_AS:    64360 kB
PageTables:        340 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-09-18 18:32:37 (client local time) WITH STATUS 10 IN 1209.63 SECONDS
stats: 2605 7 1209.63 10

Solver Data

c Parsing PB file...
c Converting 4626 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ######################################################################################################################################################
c   -- Clauses(.)/Splits(s): ....................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ---[4624]---> BDD-cost:   17
c ---[4622]---> BDD-cost:   17
c ---[4620]---> BDD-cost:   17
c ---[4618]---> BDD-cost:   17
c ---[4616]---> BDD-cost:   17
c ---[4614]---> BDD-cost:   17
c ---[4612]---> BDD-cost:   17
c ---[4610]---> BDD-cost:   17
c ---[4608]---> BDD-cost:   17
c ---[4606]---> BDD-cost:   17
c ---[4604]---> BDD-cost:   17
c ---[4602]---> BDD-cost:   17
c ---[4600]---> BDD-cost:   17
c ---[4598]---> BDD-cost:   17
c ---[4596]---> BDD-cost:   17
c ---[4594]---> BDD-cost:   17
c ---[4592]---> BDD-cost:   17
c ---[4590]---> BDD-cost:   17
c ---[4588]---> BDD-cost:   17
c ---[4586]---> BDD-cost:   17
c ---[4584]---> BDD-cost:   17
c ---[4582]---> BDD-cost:   17
c ---[4580]---> BDD-cost:   17
c ---[4578]---> BDD-cost:   17
c ---[4576]---> BDD-cost:   17
c ---[4574]---> BDD-cost:   17
c ---[4572]---> BDD-cost:   17
c ---[4570]---> BDD-cost:   17
c ---[4568]---> BDD-cost:   17
c ---[4566]---> BDD-cost:   17
c ---[4265]---> BDD-cost:    7
c ---[4264]---> BDD-cost:    7
c ---[4263]---> BDD-cost:    7
c ---[4262]---> BDD-cost:    7
c ---[4261]---> BDD-cost:    7
c ---[4260]---> BDD-cost:    7
c ---[4259]---> BDD-cost:    7
c ---[4258]---> BDD-cost:    7
c ---[4257]---> BDD-cost:    7
c ---[4256]---> BDD-cost:    7
c ---[4255]---> BDD-cost:    7
c ---[4254]---> BDD-cost:    7
c ---[4253]---> BDD-cost:    7
c ---[4252]---> BDD-cost:    7
c ---[4251]---> BDD-cost:    7
c ---[4250]---> BDD-cost:    7
c ---[4249]---> BDD-cost:    7
c ---[4248]---> BDD-cost:    7
c ---[4247]---> BDD-cost:    7
c ---[4246]---> BDD-cost:    7
c ---[4245]---> BDD-cost:    7
c ---[4244]---> BDD-cost:    7
c ---[4243]---> BDD-cost:    7
c ---[4242]---> BDD-cost:    7
c ---[4241]---> BDD-cost:    7
c ---[4240]---> BDD-cost:    7
c ---[4239]---> BDD-cost:    7
c ---[4238]---> BDD-cost:    7
c ---[4237]---> BDD-cost:    7
c ---[4236]---> BDD-cost:    7
c ---[4235]---> BDD-cost:    7
c ---[4234]---> BDD-cost:    7
c ---[4233]---> BDD-cost:    7
c ---[4232]---> BDD-cost:    7
c ---[4231]---> BDD-cost:    7
c ---[4230]---> BDD-cost:    7
c ---[4229]---> BDD-cost:    7
c ---[4228]---> BDD-cost:    7
c ---[4227]---> BDD-cost:    7
c ---[4226]---> BDD-cost:    7
c ---[4225]---> BDD-cost:    7
c ---[4224]---> BDD-cost:    7
c ---[4223]---> BDD-cost:    7
c ---[4222]---> BDD-cost:    7
c ---[4221]---> BDD-cost:    7
c ---[4220]---> BDD-cost:    7
c ---[4219]---> BDD-cost:    7
c ---[4218]---> BDD-cost:    7
c ---[4217]---> BDD-cost:    7
c ---[4216]---> BDD-cost:    7
c ---[4215]---> BDD-cost:    7
c ---[4214]---> BDD-cost:    7
c ---[4213]---> BDD-cost:    7
c ---[4212]---> BDD-cost:    7
c ---[4211]---> BDD-cost:    7
c ---[4210]---> BDD-cost:    7
c ---[4209]---> BDD-cost:    7
c ---[4208]---> BDD-cost:    7
c ---[4207]---> BDD-cost:    7
c ---[4206]---> BDD-cost:    7
c ---[4204]---> BDD-cost:    9
c ---[4202]---> BDD-cost:    9
c ---[4200]---> BDD-cost:    9
c ---[4198]---> BDD-cost:    9
c ---[4196]---> BDD-cost:    9
c ---[4194]---> BDD-cost:    9
c ---[4192]---> BDD-cost:    9
c ---[4190]---> BDD-cost:    9
c ---[4188]---> BDD-cost:    9
c ---[4186]---> BDD-cost:    9
c ---[4184]---> BDD-cost:    9
c ---[4182]---> BDD-cost:    9
c ---[4180]---> BDD-cost:    9
c ---[4178]---> BDD-cost:    9
c ---[4176]---> BDD-cost:    9
c ---[4174]---> BDD-cost:    9
c ---[4172]---> BDD-cost:    9
c ---[4170]---> BDD-cost:    9
c ---[4168]---> BDD-cost:    9
c ---[4166]---> BDD-cost:    9
c ---[4164]---> BDD-cost:    9
c ---[4162]---> BDD-cost:    9
c ---[4160]---> BDD-cost:    9
c ---[4158]---> BDD-cost:    9
c ---[4156]---> BDD-cost:    9
c ---[4154]---> BDD-cost:    9
c ---[4152]---> BDD-cost:    9
c ---[4150]---> BDD-cost:    9
c ---[4148]---> BDD-cost:    9
c ---[4146]---> BDD-cost:    9
c ---[4144]---> BDD-cost:    9
c ---[4142]---> BDD-cost:    9
c ---[4140]---> BDD-cost:    9
c ---[4138]---> BDD-cost:    9
c ---[4136]---> BDD-cost:    9
c ---[4134]---> BDD-cost:    9
c ---[4132]---> BDD-cost:    9
c ---[4130]---> BDD-cost:    9
c ---[4128]---> BDD-cost:    9
c ---[4126]---> BDD-cost:    9
c ---[4124]---> BDD-cost:    9
c ---[4122]---> BDD-cost:    9
c ---[4120]---> BDD-cost:    9
c ---[4118]---> BDD-cost:    9
c ---[4116]---> BDD-cost:    9
c ---[4114]---> BDD-cost:    9
c ---[4112]---> BDD-cost:    9
c ---[4110]---> BDD-cost:    9
c ---[4108]---> BDD-cost:    9
c ---[4106]---> BDD-cost:    9
c ---[4104]---> BDD-cost:    9
c ---[4102]---> BDD-cost:    9
c ---[4100]---> BDD-cost:    9
c ---[4098]---> BDD-cost:    9
c ---[4096]---> BDD-cost:    9
c ---[4094]---> BDD-cost:    9
c ---[4092]---> BDD-cost:    9
c ---[4090]---> BDD-cost:    9
c ---[4088]---> BDD-cost:    9
c ---[4086]---> BDD-cost:    9
c ---[4079]---> BDD-cost:   64
c ---[4078]---> BDD-cost:   64
c ---[4077]---> BDD-cost:   64
c ---[4076]---> BDD-cost:   64
c ---[4075]---> BDD-cost:   64
c ---[4074]---> BDD-cost:   64
c ---[4067]---> BDD-cost:   67
c ---[4066]---> BDD-cost:   67
c ---[4065]---> BDD-cost:   67
c ---[4064]---> BDD-cost:   67
c ---[4063]---> BDD-cost:   67
c ---[4062]---> BDD-cost:   67
c ---[4055]---> BDD-cost:   67
c ---[4054]---> BDD-cost:   67
c ---[4053]---> BDD-cost:   67
c ---[4052]---> BDD-cost:   67
c ---[4051]---> BDD-cost:   67
c ---[4050]---> BDD-cost:   67
c ---[4043]---> BDD-cost:   67
c ---[4042]---> BDD-cost:   67
c ---[4041]---> BDD-cost:   67
c ---[4040]---> BDD-cost:   67
c ---[4039]---> BDD-cost:   67
c ---[4038]---> BDD-cost:   67
c ---[4031]---> BDD-cost:   67
c ---[4030]---> BDD-cost:   67
c ---[4029]---> BDD-cost:   67
c ---[4028]---> BDD-cost:   67
c ---[4027]---> BDD-cost:   67
c ---[4026]---> BDD-cost:   67
c ---[4019]---> BDD-cost:   67
c ---[4018]---> BDD-cost:   67
c ---[4017]---> BDD-cost:   67
c ---[4016]---> BDD-cost:   67
c ---[4015]---> BDD-cost:   67
c ---[4014]---> BDD-cost:   67
c ---[4007]---> BDD-cost:   67
c ---[4006]---> BDD-cost:   67
c ---[4005]---> BDD-cost:   67
c ---[4004]---> BDD-cost:   67
c ---[4003]---> BDD-cost:   67
c ---[4002]---> BDD-cost:   67
c ---[2050]---> BDD-cost:    7
c ---[2048]---> BDD-cost:    7
c ---[2046]---> BDD-cost:    7
c ---[2044]---> BDD-cost:    7
c ---[2042]---> BDD-cost:    7
c ---[2040]---> BDD-cost:    7
c ---[2038]---> BDD-cost:    7
c ---[2036]---> BDD-cost:    7
c ---[2034]---> BDD-cost:    7
c ---[2032]---> BDD-cost:    7
c ---[2030]---> BDD-cost:    7
c ---[2028]---> BDD-cost:    7
c ---[2026]---> BDD-cost:    7
c ---[2024]---> BDD-cost:    7
c ---[2022]---> BDD-cost:    7
c ---[2020]---> BDD-cost:    7
c ---[2018]---> BDD-cost:    7
c ---[2016]---> BDD-cost:    7
c ---[2014]---> BDD-cost:    7
c ---[2012]---> BDD-cost:    7
c ---[2010]---> BDD-cost:    7
c ---[2008]---> BDD-cost:    7
c ---[2006]---> BDD-cost:    7
c ---[2004]---> BDD-cost:    7
c ---[2002]---> BDD-cost:    7
c ---[2000]---> BDD-cost:    7
c ---[1998]---> BDD-cost:    7
c ---[1996]---> BDD-cost:    7
c ---[1994]---> BDD-cost:    7
c ---[1992]---> BDD-cost:    7
c ---[1990]---> BDD-cost:    7
c ---[1988]---> BDD-cost:    7
c ---[1986]---> BDD-cost:    7
c ---[1984]---> BDD-cost:    7
c ---[1982]---> BDD-cost:    7
c ---[1980]---> BDD-cost:    7
c ---[1978]---> BDD-cost:    7
c ---[1976]---> BDD-cost:    7
c ---[1974]---> BDD-cost:    7
c ---[1972]---> BDD-cost:    7
c ---[1970]---> BDD-cost:    7
c ---[1968]---> BDD-cost:    7
c ---[1966]---> BDD-cost:    7
c ---[1964]---> BDD-cost:    7
c ---[1962]---> BDD-cost:    7
c ---[1960]---> BDD-cost:    7
c ---[1958]---> BDD-cost:    7
c ---[1956]---> BDD-cost:    7
c ---[1954]---> BDD-cost:    7
c ---[1952]---> BDD-cost:    7
c ---[1950]---> BDD-cost:    7
c ---[1948]---> BDD-cost:    7
c ---[1946]---> BDD-cost:    7
c ---[1944]---> BDD-cost:    7
c ---[1942]---> BDD-cost:    7
c ---[1940]---> BDD-cost:    7
c ---[1938]---> BDD-cost:    7
c ---[1936]---> BDD-cost:    7
c ---[1934]---> BDD-cost:    7
c ---[1932]---> BDD-cost:    7
c ---[1931]---> BDD-cost:    7
c ---[1930]---> BDD-cost:    7
c ---[1929]---> BDD-cost:    7
c ---[1928]---> BDD-cost:    7
c ---[1927]---> BDD-cost:    7
c ---[1926]---> BDD-cost:    7
c ---[1925]---> BDD-cost:    7
c ---[1924]---> BDD-cost:    7
c ---[1923]---> BDD-cost:    7
c ---[1922]---> BDD-cost:    7
c ---[1921]---> BDD-cost:    7
c ---[1920]---> BDD-cost:    7
c ---[1919]---> BDD-cost:    9
c ---[1918]---> BDD-cost:    2
c ---[1917]---> BDD-cost:    9
c ---[1916]---> BDD-cost:    2
c ---[1915]---> BDD-cost:    9
c ---[1914]---> BDD-cost:    2
c ---[1913]---> BDD-cost:    9
c ---[1912]---> BDD-cost:    2
c ---[1911]---> BDD-cost:    8
c ---[1910]---> BDD-cost:    2
c ---[1909]---> BDD-cost:    8
c ---[1908]---> BDD-cost:    2
c ---[1907]---> BDD-cost:    8
c ---[1906]---> BDD-cost:    2
c ---[1905]---> BDD-cost:    8
c ---[1904]---> BDD-cost:    2
c ---[1903]---> BDD-cost:    7
c ---[1902]---> BDD-cost:    2
c ---[1901]---> BDD-cost:    7
c ---[1900]---> BDD-cost:    2
c ---[1899]---> BDD-cost:    7
c ---[1898]---> BDD-cost:    2
c ---[1897]---> BDD-cost:    7
c ---[1896]---> BDD-cost:    2
c ---[1895]---> BDD-cost:    6
c ---[1894]---> BDD-cost:    2
c ---[1893]---> BDD-cost:    6
c ---[1892]---> BDD-cost:    2
c ---[1891]---> BDD-cost:    6
c ---[1890]---> BDD-cost:    2
c ---[1889]---> BDD-cost:    6
c ---[1888]---> BDD-cost:    2
c ---[1887]---> BDD-cost:    5
c ---[1886]---> BDD-cost:    2
c ---[1885]---> BDD-cost:    5
c ---[1884]---> BDD-cost:    2
c ---[1883]---> BDD-cost:    5
c ---[1882]---> BDD-cost:    2
c ---[1881]---> BDD-cost:    5
c ---[1880]---> BDD-cost:    2
c ---[1879]---> BDD-cost:    4
c ---[1878]---> BDD-cost:    2
c ---[1877]---> BDD-cost:    4
c ---[1876]---> BDD-cost:    2
c ---[1875]---> BDD-cost:    4
c ---[1874]---> BDD-cost:    2
c ---[1873]---> BDD-cost:    4
c ---[1872]---> BDD-cost:    2
c ---[1871]---> BDD-cost:    3
c ---[1870]---> BDD-cost:    2
c ---[1869]---> BDD-cost:    3
c ---[1868]---> BDD-cost:    2
c ---[1867]---> BDD-cost:    3
c ---[1866]---> BDD-cost:    2
c ---[1865]---> BDD-cost:    3
c ---[1864]---> BDD-cost:    2
c ---[1855]---> BDD-cost:    6
c ---[1854]---> BDD-cost:    2
c ---[1853]---> BDD-cost:    2
c ---[1852]---> BDD-cost:    2
c ---[1851]---> BDD-cost:    2
c ---[1850]---> BDD-cost:    2
c ---[1849]---> BDD-cost:    2
c ---[1848]---> BDD-cost:    2
c ---[1847]---> BDD-cost:    5
c ---[1846]---> BDD-cost:    2
c ---[1845]---> BDD-cost:    2
c ---[1844]---> BDD-cost:    2
c ---[1843]---> BDD-cost:    2
c ---[1842]---> BDD-cost:    2
c ---[1841]---> BDD-cost:    2
c ---[1840]---> BDD-cost:    2
c ---[1839]---> BDD-cost:    4
c ---[1838]---> BDD-cost:    2
c ---[1837]---> BDD-cost:    2
c ---[1836]---> BDD-cost:    2
c ---[1835]---> BDD-cost:    2
c ---[1834]---> BDD-cost:    2
c ---[1833]---> BDD-cost:    2
c ---[1832]---> BDD-cost:    2
c ---[1831]---> BDD-cost:    3
c ---[1830]---> BDD-cost:    2
c ---[1829]---> BDD-cost:    2
c ---[1828]---> BDD-cost:    2
c ---[1827]---> BDD-cost:    2
c ---[1826]---> BDD-cost:    2
c ---[1825]---> BDD-cost:    2
c ---[1824]---> BDD-cost:    2
c ---[1823]---> BDD-cost:    2
c ---[1822]---> BDD-cost:    2
c ---[1821]---> BDD-cost:    2
c ---[1820]---> BDD-cost:    2
c ---[1819]---> BDD-cost:    2
c ---[1818]---> BDD-cost:    2
c ---[1817]---> BDD-cost:    2
c ---[1816]---> BDD-cost:    2
c ---[1815]---> BDD-cost:    4
c ---[1814]---> BDD-cost:    2
c ---[1813]---> BDD-cost:    2
c ---[1812]---> BDD-cost:    2
c ---[1811]---> BDD-cost:    2
c ---[1810]---> BDD-cost:    2
c ---[1809]---> BDD-cost:    2
c ---[1808]---> BDD-cost:    2
c ---[1807]---> BDD-cost:    3
c ---[1806]---> BDD-cost:    2
c ---[1805]---> BDD-cost:    2
c ---[1804]---> BDD-cost:    2
c ---[1803]---> BDD-cost:    2
c ---[1802]---> BDD-cost:    2
c ---[1801]---> BDD-cost:    2
c ---[1800]---> BDD-cost:    2
c ---[1791]---> BDD-cost:    2
c ---[1790]---> BDD-cost:    2
c ---[1789]---> BDD-cost:    2
c ---[1788]---> BDD-cost:    2
c ---[1787]---> BDD-cost:    2
c ---[1786]---> BDD-cost:    2
c ---[1785]---> BDD-cost:    2
c ---[1784]---> BDD-cost:    2
c ---[1783]---> BDD-cost:    2
c ---[1782]---> BDD-cost:    2
c ---[1781]---> BDD-cost:    2
c ---[1780]---> BDD-cost:    2
c ---[1779]---> BDD-cost:    2
c ---[1778]---> BDD-cost:    2
c ---[1777]---> BDD-cost:    2
c ---[1776]---> BDD-cost:    2
c ---[1775]---> BDD-cost:    2
c ---[1774]---> BDD-cost:    2
c ---[1773]---> BDD-cost:    2
c ---[1772]---> BDD-cost:    2
c ---[1771]---> BDD-cost:    2
c ---[1770]---> BDD-cost:    2
c ---[1769]---> BDD-cost:    2
c ---[1768]---> BDD-cost:    2
c ---[1767]---> BDD-cost:    2
c ---[1766]---> BDD-cost:    2
c ---[1765]---> BDD-cost:    2
c ---[1764]---> BDD-cost:    2
c ---[1763]---> BDD-cost:    2
c ---[1762]---> BDD-cost:    2
c ---[1761]---> BDD-cost:    2
c ---[1760]---> BDD-cost:    2
c ---[1759]---> BDD-cost:    2
c ---[1758]---> BDD-cost:    2
c ---[1757]---> BDD-cost:    2
c ---[1756]---> BDD-cost:    2
c ---[1755]---> BDD-cost:    2
c ---[1754]---> BDD-cost:    2
c ---[1753]---> BDD-cost:    2
c ---[1752]---> BDD-cost:    2
c ---[1751]---> BDD-cost:    2
c ---[1750]---> BDD-cost:    2
c ---[1749]---> BDD-cost:    2
c ---[1748]---> BDD-cost:    2
c ---[1747]---> BDD-cost:    2
c ---[1746]---> BDD-cost:    2
c ---[1745]---> BDD-cost:    2
c ---[1744]---> BDD-cost:    2
c ---[1743]---> BDD-cost:    2
c ---[1742]---> BDD-cost:    2
c ---[1741]---> BDD-cost:    2
c ---[1740]---> BDD-cost:    2
c ---[1739]---> BDD-cost:    2
c ---[1738]---> BDD-cost:    2
c ---[1737]---> BDD-cost:    2
c ---[1736]---> BDD-cost:    2
c ---[1727]---> BDD-cost:    2
c ---[1726]---> BDD-cost:    2
c ---[1725]---> BDD-cost:    2
c ---[1724]---> BDD-cost:    2
c ---[1723]---> BDD-cost:    2
c ---[1722]---> BDD-cost:    2
c ---[1721]---> BDD-cost:    2
c ---[1720]---> BDD-cost:    2
c ---[1719]---> BDD-cost:    2
c ---[1718]---> BDD-cost:    2
c ---[1717]---> BDD-cost:    2
c ---[1716]---> BDD-cost:    2
c ---[1715]---> BDD-cost:    2
c ---[1714]---> BDD-cost:    2
c ---[1713]---> BDD-cost:    2
c ---[1712]---> BDD-cost:    2
c ---[1711]---> BDD-cost:    2
c ---[1710]---> BDD-cost:    2
c ---[1709]---> BDD-cost:    2
c ---[1708]---> BDD-cost:    2
c ---[1707]---> BDD-cost:    2
c ---[1706]---> BDD-cost:    2
c ---[1705]---> BDD-cost:    2
c ---[1704]---> BDD-cost:    2
c ---[1703]---> BDD-cost:    2
c ---[1702]---> BDD-cost:    2
c ---[1701]---> BDD-cost:    2
c ---[1700]---> BDD-cost:    2
c ---[1699]---> BDD-cost:    2
c ---[1698]---> BDD-cost:    2
c ---[1697]---> BDD-cost:    2
c ---[1696]---> BDD-cost:    2
c ---[1695]---> BDD-cost:    2
c ---[1694]---> BDD-cost:    2
c ---[1693]---> BDD-cost:    2
c ---[1692]---> BDD-cost:    2
c ---[1691]---> BDD-cost:    2
c ---[1690]---> BDD-cost:    2
c ---[1689]---> BDD-cost:    2
c ---[1688]---> BDD-cost:    2
c ---[1687]---> BDD-cost:    2
c ---[1686]---> BDD-cost:    2
c ---[1685]---> BDD-cost:    2
c ---[1684]---> BDD-cost:    2
c ---[1683]---> BDD-cost:    2
c ---[1682]---> BDD-cost:    2
c ---[1681]---> BDD-cost:    2
c ---[1680]---> BDD-cost:    2
c ---[1679]---> BDD-cost:    2
c ---[1678]---> BDD-cost:    2
c ---[1677]---> BDD-cost:    2
c ---[1676]---> BDD-cost:    2
c ---[1675]---> BDD-cost:    2
c ---[1674]---> BDD-cost:    2
c ---[1673]---> BDD-cost:    2
c ---[1672]---> BDD-cost:    2
c ---[1663]---> BDD-cost:    2
c ---[1662]---> BDD-cost:    2
c ---[1661]---> BDD-cost:    2
c ---[1660]---> BDD-cost:    2
c ---[1659]---> BDD-cost:    2
c ---[1658]---> BDD-cost:    2
c ---[1657]---> BDD-cost:    2
c ---[1656]---> BDD-cost:    2
c ---[1655]---> BDD-cost:    2
c ---[1654]---> BDD-cost:    2
c ---[1653]---> BDD-cost:    2
c ---[1652]---> BDD-cost:    2
c ---[1651]---> BDD-cost:    2
c ---[1650]---> BDD-cost:    2
c ---[1649]---> BDD-cost:    2
c ---[1648]---> BDD-cost:    2
c ---[1647]---> BDD-cost:    2
c ---[1646]---> BDD-cost:    2
c ---[1645]---> BDD-cost:    2
c ---[1644]---> BDD-cost:    2
c ---[1643]---> BDD-cost:    2
c ---[1642]---> BDD-cost:    2
c ---[1641]---> BDD-cost:    2
c ---[1640]---> BDD-cost:    2
c ---[1639]---> BDD-cost:    2
c ---[1638]---> BDD-cost:    2
c ---[1637]---> BDD-cost:    2
c ---[1636]---> BDD-cost:    2
c ---[1635]---> BDD-cost:    2
c ---[1634]---> BDD-cost:    2
c ---[1633]---> BDD-cost:    2
c ---[1632]---> BDD-cost:    2
c ---[1631]---> BDD-cost:    2
c ---[1630]---> BDD-cost:    2
c ---[1629]---> BDD-cost:    2
c ---[1628]---> BDD-cost:    2
c ---[1627]---> BDD-cost:    2
c ---[1626]---> BDD-cost:    2
c ---[1625]---> BDD-cost:    2
c ---[1624]---> BDD-cost:    2
c ---[1623]---> BDD-cost:    2
c ---[1622]---> BDD-cost:    2
c ---[1621]---> BDD-cost:    2
c ---[1620]---> BDD-cost:    2
c ---[1619]---> BDD-cost:    2
c ---[1618]---> BDD-cost:    2
c ---[1617]---> BDD-cost:    2
c ---[1616]---> BDD-cost:    2
c ---[1615]---> BDD-cost:    2
c ---[1614]---> BDD-cost:    2
c ---[1613]---> BDD-cost:    2
c ---[1612]---> BDD-cost:    2
c ---[1611]---> BDD-cost:    2
c ---[1610]---> BDD-cost:    2
c ---[1609]---> BDD-cost:    2
c ---[1608]---> BDD-cost:    2
c ---[1599]---> BDD-cost:    9
c ---[1598]---> BDD-cost:    2
c ---[1597]---> BDD-cost:    9
c ---[1596]---> BDD-cost:    2
c ---[1595]---> BDD-cost:    9
c ---[1594]---> BDD-cost:    2
c ---[1593]---> BDD-cost:    9
c ---[1592]---> BDD-cost:    2
c ---[1591]---> BDD-cost:    8
c ---[1590]---> BDD-cost:    2
c ---[1589]---> BDD-cost:    8
c ---[1588]---> BDD-cost:    2
c ---[1587]---> BDD-cost:    8
c ---[1586]---> BDD-cost:    2
c ---[1585]---> BDD-cost:    8
c ---[1584]---> BDD-cost:    2
c ---[1583]---> BDD-cost:    7
c ---[1582]---> BDD-cost:    2
c ---[1581]---> BDD-cost:    7
c ---[1580]---> BDD-cost:    2
c ---[1579]---> BDD-cost:    7
c ---[1578]---> BDD-cost:    2
c ---[1577]---> BDD-cost:    7
c ---[1576]---> BDD-cost:    2
c ---[1575]---> BDD-cost:    6
c ---[1574]---> BDD-cost:    2
c ---[1573]---> BDD-cost:    6
c ---[1572]---> BDD-cost:    2
c ---[1571]---> BDD-cost:    6
c ---[1570]---> BDD-cost:    2
c ---[1569]---> BDD-cost:    6
c ---[1568]---> BDD-cost:    2
c ---[1567]---> BDD-cost:    5
c ---[1566]---> BDD-cost:    2
c ---[1565]---> BDD-cost:    5
c ---[1564]---> BDD-cost:    2
c ---[1563]---> BDD-cost:    5
c ---[1562]---> BDD-cost:    2
c ---[1561]---> BDD-cost:    5
c ---[1560]---> BDD-cost:    2
c ---[1559]---> BDD-cost:    4
c ---[1558]---> BDD-cost:    2
c ---[1557]---> BDD-cost:    4
c ---[1556]---> BDD-cost:    2
c ---[1555]---> BDD-cost:    4
c ---[1554]---> BDD-cost:    2
c ---[1553]---> BDD-cost:    4
c ---[1552]---> BDD-cost:    2
c ---[1551]---> BDD-cost:    3
c ---[1550]---> BDD-cost:    2
c ---[1549]---> BDD-cost:    3
c ---[1548]---> BDD-cost:    2
c ---[1547]---> BDD-cost:    3
c ---[1546]---> BDD-cost:    2
c ---[1545]---> BDD-cost:    3
c ---[1544]---> BDD-cost:    2
c ---[1535]---> BDD-cost:    6
c ---[1534]---> BDD-cost:    2
c ---[1533]---> BDD-cost:    2
c ---[1532]---> BDD-cost:    2
c ---[1531]---> BDD-cost:    2
c ---[1530]---> BDD-cost:    2
c ---[1529]---> BDD-cost:    2
c ---[1528]---> BDD-cost:    2
c ---[1527]---> BDD-cost:    5
c ---[1526]---> BDD-cost:    2
c ---[1525]---> BDD-cost:    2
c ---[1524]---> BDD-cost:    2
c ---[1523]---> BDD-cost:    2
c ---[1522]---> BDD-cost:    2
c ---[1521]---> BDD-cost:    2
c ---[1520]---> BDD-cost:    2
c ---[1519]---> BDD-cost:    4
c ---[1518]---> BDD-cost:    2
c ---[1517]---> BDD-cost:    2
c ---[1516]---> BDD-cost:    2
c ---[1515]---> BDD-cost:    2
c ---[1514]---> BDD-cost:    2
c ---[1513]---> BDD-cost:    2
c ---[1512]---> BDD-cost:    2
c ---[1511]---> BDD-cost:    3
c ---[1510]---> BDD-cost:    2
c ---[1509]---> BDD-cost:    2
c ---[1508]---> BDD-cost:    2
c ---[1507]---> BDD-cost:    2
c ---[1506]---> BDD-cost:    2
c ---[1505]---> BDD-cost:    2
c ---[1504]---> BDD-cost:    2
c ---[1503]---> BDD-cost:    2
c ---[1502]---> BDD-cost:    2
c ---[1501]---> BDD-cost:    2
c ---[1500]---> BDD-cost:    2
c ---[1499]---> BDD-cost:    2
c ---[1498]---> BDD-cost:    2
c ---[1497]---> BDD-cost:    2
c ---[1496]---> BDD-cost:    2
c ---[1495]---> BDD-cost:    4
c ---[1494]---> BDD-cost:    2
c ---[1493]---> BDD-cost:    2
c ---[1492]---> BDD-cost:    2
c ---[1491]---> BDD-cost:    2
c ---[1490]---> BDD-cost:    2
c ---[1489]---> BDD-cost:    2
c ---[1488]---> BDD-cost:    2
c ---[1487]---> BDD-cost:    3
c ---[1486]---> BDD-cost:    2
c ---[1485]---> BDD-cost:    2
c ---[1484]---> BDD-cost:    2
c ---[1483]---> BDD-cost:    2
c ---[1482]---> BDD-cost:    2
c ---[1481]---> BDD-cost:    2
c ---[1480]---> BDD-cost:    2
c ---[1471]---> BDD-cost:    2
c ---[1470]---> BDD-cost:    2
c ---[1469]---> BDD-cost:    2
c ---[1468]---> BDD-cost:    2
c ---[1467]---> BDD-cost:    2
c ---[1466]---> BDD-cost:    2
c ---[1465]---> BDD-cost:    2
c ---[1464]---> BDD-cost:    2
c ---[1463]---> BDD-cost:    2
c ---[1462]---> BDD-cost:    2
c ---[1461]---> BDD-cost:    2
c ---[1460]---> BDD-cost:    2
c ---[1459]---> BDD-cost:    2
c ---[1458]---> BDD-cost:    2
c ---[1457]---> BDD-cost:    2
c ---[1456]---> BDD-cost:    2
c ---[1455]---> BDD-cost:    2
c ---[1454]---> BDD-cost:    2
c ---[1453]---> BDD-cost:    2
c ---[1452]---> BDD-cost:    2
c ---[1451]---> BDD-cost:    2
c ---[1450]---> BDD-cost:    2
c ---[1449]---> BDD-cost:    2
c ---[1448]---> BDD-cost:    2
c ---[1447]---> BDD-cost:    2
c ---[1446]---> BDD-cost:    2
c ---[1445]---> BDD-cost:    2
c ---[1444]---> BDD-cost:    2
c ---[1443]---> BDD-cost:    2
c ---[1442]---> BDD-cost:    2
c ---[1441]---> BDD-cost:    2
c ---[1440]---> BDD-cost:    2
c ---[1439]---> BDD-cost:    2
c ---[1438]---> BDD-cost:    2
c ---[1437]---> BDD-cost:    2
c ---[1436]---> BDD-cost:    2
c ---[1435]---> BDD-cost:    2
c ---[1434]---> BDD-cost:    2
c ---[1433]---> BDD-cost:    2
c ---[1432]---> BDD-cost:    2
c ---[1431]---> BDD-cost:    2
c ---[1430]---> BDD-cost:    2
c ---[1429]---> BDD-cost:    2
c ---[1428]---> BDD-cost:    2
c ---[1427]---> BDD-cost:    2
c ---[1426]---> BDD-cost:    2
c ---[1425]---> BDD-cost:    2
c ---[1424]---> BDD-cost:    2
c ---[1423]---> BDD-cost:    2
c ---[1422]---> BDD-cost:    2
c ---[1421]---> BDD-cost:    2
c ---[1420]---> BDD-cost:    2
c ---[1419]---> BDD-cost:    2
c ---[1418]---> BDD-cost:    2
c ---[1417]---> BDD-cost:    2
c ---[1416]---> BDD-cost:    2
c ---[1407]---> BDD-cost:    2
c ---[1406]---> BDD-cost:    2
c ---[1405]---> BDD-cost:    2
c ---[1404]---> BDD-cost:    2
c ---[1403]---> BDD-cost:    2
c ---[1402]---> BDD-cost:    2
c ---[1401]---> BDD-cost:    2
c ---[1400]---> BDD-cost:    2
c ---[1399]---> BDD-cost:    2
c ---[1398]---> BDD-cost:    2
c ---[1397]---> BDD-cost:    2
c ---[1396]---> BDD-cost:    2
c ---[1395]---> BDD-cost:    2
c ---[1394]---> BDD-cost:    2
c ---[1393]---> BDD-cost:    2
c ---[1392]---> BDD-cost:    2
c ---[1391]---> BDD-cost:    2
c ---[1390]---> BDD-cost:    2
c ---[1389]---> BDD-cost:    2
c ---[1388]---> BDD-cost:    2
c ---[1387]---> BDD-cost:    2
c ---[1386]---> BDD-cost:    2
c ---[1385]---> BDD-cost:    2
c ---[1384]---> BDD-cost:    2
c ---[1383]---> BDD-cost:    2
c ---[1382]---> BDD-cost:    2
c ---[1381]---> BDD-cost:    2
c ---[1380]---> BDD-cost:    2
c ---[1379]---> BDD-cost:    2
c ---[1378]---> BDD-cost:    2
c ---[1377]---> BDD-cost:    2
c ---[1376]---> BDD-cost:    2
c ---[1375]---> BDD-cost:    2
c ---[1374]---> BDD-cost:    2
c ---[1373]---> BDD-cost:    2
c ---[1372]---> BDD-cost:    2
c ---[1371]---> BDD-cost:    2
c ---[1370]---> BDD-cost:    2
c ---[1369]---> BDD-cost:    2
c ---[1368]---> BDD-cost:    2
c ---[1367]---> BDD-cost:    2
c ---[1366]---> BDD-cost:    2
c ---[1365]---> BDD-cost:    2
c ---[1364]---> BDD-cost:    2
c ---[1363]---> BDD-cost:    2
c ---[1362]---> BDD-cost:    2
c ---[1361]---> BDD-cost:    2
c ---[1360]---> BDD-cost:    2
c ---[1359]---> BDD-cost:    2
c ---[1358]---> BDD-cost:    2
c ---[1357]---> BDD-cost:    2
c ---[1356]---> BDD-cost:    2
c ---[1355]---> BDD-cost:    2
c ---[1354]---> BDD-cost:    2
c ---[1353]---> BDD-cost:    2
c ---[1352]---> BDD-cost:    2
c ---[1343]---> BDD-cost:    2
c ---[1342]---> BDD-cost:    2
c ---[1341]---> BDD-cost:    2
c ---[1340]---> BDD-cost:    2
c ---[1339]---> BDD-cost:    2
c ---[1338]---> BDD-cost:    2
c ---[1337]---> BDD-cost:    2
c ---[1336]---> BDD-cost:    2
c ---[1335]---> BDD-cost:    2
c ---[1334]---> BDD-cost:    2
c ---[1333]---> BDD-cost:    2
c ---[1332]---> BDD-cost:    2
c ---[1331]---> BDD-cost:    2
c ---[1330]---> BDD-cost:    2
c ---[1329]---> BDD-cost:    2
c ---[1328]---> BDD-cost:    2
c ---[1327]---> BDD-cost:    2
c ---[1326]---> BDD-cost:    2
c ---[1325]---> BDD-cost:    2
c ---[1324]---> BDD-cost:    2
c ---[1323]---> BDD-cost:    2
c ---[1322]---> BDD-cost:    2
c ---[1321]---> BDD-cost:    2
c ---[1320]---> BDD-cost:    2
c ---[1319]---> BDD-cost:    2
c ---[1318]---> BDD-cost:    2
c ---[1317]---> BDD-cost:    2
c ---[1316]---> BDD-cost:    2
c ---[1315]---> BDD-cost:    2
c ---[1314]---> BDD-cost:    2
c ---[1313]---> BDD-cost:    2
c ---[1312]---> BDD-cost:    2
c ---[1311]---> BDD-cost:    2
c ---[1310]---> BDD-cost:    2
c ---[1309]---> BDD-cost:    2
c ---[1308]---> BDD-cost:    2
c ---[1307]---> BDD-cost:    2
c ---[1306]---> BDD-cost:    2
c ---[1305]---> BDD-cost:    2
c ---[1304]---> BDD-cost:    2
c ---[1303]---> BDD-cost:    2
c ---[1302]---> BDD-cost:    2
c ---[1301]---> BDD-cost:    2
c ---[1300]---> BDD-cost:    2
c ---[1299]---> BDD-cost:    2
c ---[1298]---> BDD-cost:    2
c ---[1297]---> BDD-cost:    2
c ---[1296]---> BDD-cost:    2
c ---[1295]---> BDD-cost:    2
c ---[1294]---> BDD-cost:    2
c ---[1293]---> BDD-cost:    2
c ---[1292]---> BDD-cost:    2
c ---[1291]---> BDD-cost:    2
c ---[1290]---> BDD-cost:    2
c ---[1289]---> BDD-cost:    2
c ---[1288]---> BDD-cost:    2
c ---[1279]---> BDD-cost:    9
c ---[1278]---> BDD-cost:    2
c ---[1277]---> BDD-cost:    9
c ---[1276]---> BDD-cost:    2
c ---[1275]---> BDD-cost:    9
c ---[1274]---> BDD-cost:    2
c ---[1273]---> BDD-cost:    9
c ---[1272]---> BDD-cost:    2
c ---[1271]---> BDD-cost:    8
c ---[1270]---> BDD-cost:    2
c ---[1269]---> BDD-cost:    8
c ---[1268]---> BDD-cost:    2
c ---[1267]---> BDD-cost:    8
c ---[1266]---> BDD-cost:    2
c ---[1265]---> BDD-cost:    8
c ---[1264]---> BDD-cost:    2
c ---[1263]---> BDD-cost:    7
c ---[1262]---> BDD-cost:    2
c ---[1261]---> BDD-cost:    7
c ---[1260]---> BDD-cost:    2
c ---[1259]---> BDD-cost:    7
c ---[1258]---> BDD-cost:    2
c ---[1257]---> BDD-cost:    7
c ---[1256]---> BDD-cost:    2
c ---[1255]---> BDD-cost:    6
c ---[1254]---> BDD-cost:    2
c ---[1253]---> BDD-cost:    6
c ---[1252]---> BDD-cost:    2
c ---[1251]---> BDD-cost:    6
c ---[1250]---> BDD-cost:    2
c ---[1249]---> BDD-cost:    6
c ---[1248]---> BDD-cost:    2
c ---[1247]---> BDD-cost:    5
c ---[1246]---> BDD-cost:    2
c ---[1245]---> BDD-cost:    5
c ---[1244]---> BDD-cost:    2
c ---[1243]---> BDD-cost:    5
c ---[1242]---> BDD-cost:    2
c ---[1241]---> BDD-cost:    5
c ---[1240]---> BDD-cost:    2
c ---[1239]---> BDD-cost:    4
c ---[1238]---> BDD-cost:    2
c ---[1237]---> BDD-cost:    4
c ---[1236]---> BDD-cost:    2
c ---[1235]---> BDD-cost:    4
c ---[1234]---> BDD-cost:    2
c ---[1233]---> BDD-cost:    4
c ---[1232]---> BDD-cost:    2
c ---[1231]---> BDD-cost:    3
c ---[1230]---> BDD-cost:    2
c ---[1229]---> BDD-cost:    3
c ---[1228]---> BDD-cost:    2
c ---[1227]---> BDD-cost:    3
c ---[1226]---> BDD-cost:    2
c ---[1225]---> BDD-cost:    3
c ---[1224]---> BDD-cost:    2
c ---[1215]---> BDD-cost:    6
c ---[1214]---> BDD-cost:    2
c ---[1213]---> BDD-cost:    2
c ---[1212]---> BDD-cost:    2
c ---[1211]---> BDD-cost:    2
c ---[1210]---> BDD-cost:    2
c ---[1209]---> BDD-cost:    2
c ---[1208]---> BDD-cost:    2
c ---[1207]---> BDD-cost:    5
c ---[1206]---> BDD-cost:    2
c ---[1205]---> BDD-cost:    2
c ---[1204]---> BDD-cost:    2
c ---[1203]---> BDD-cost:    2
c ---[1202]---> BDD-cost:    2
c ---[1201]---> BDD-cost:    2
c ---[1200]---> BDD-cost:    2
c ---[1199]---> BDD-cost:    4
c ---[1198]---> BDD-cost:    2
c ---[1197]---> BDD-cost:    2
c ---[1196]---> BDD-cost:    2
c ---[1195]---> BDD-cost:    2
c ---[1194]---> BDD-cost:    2
c ---[1193]---> BDD-cost:    2
c ---[1192]---> BDD-cost:    2
c ---[1191]---> BDD-cost:    3
c ---[1190]---> BDD-cost:    2
c ---[1189]---> BDD-cost:    2
c ---[1188]---> BDD-cost:    2
c ---[1187]---> BDD-cost:    2
c ---[1186]---> BDD-cost:    2
c ---[1185]---> BDD-cost:    2
c ---[1184]---> BDD-cost:    2
c ---[1183]---> BDD-cost:    2
c ---[1182]---> BDD-cost:    2
c ---[1181]---> BDD-cost:    2
c ---[1180]---> BDD-cost:    2
c ---[1179]---> BDD-cost:    2
c ---[1178]---> BDD-cost:    2
c ---[1177]---> BDD-cost:    2
c ---[1176]---> BDD-cost:    2
c ---[1175]---> BDD-cost:    4
c ---[1174]---> BDD-cost:    2
c ---[1173]---> BDD-cost:    2
c ---[1172]---> BDD-cost:    2
c ---[1171]---> BDD-cost:    2
c ---[1170]---> BDD-cost:    2
c ---[1169]---> BDD-cost:    2
c ---[1168]---> BDD-cost:    2
c ---[1167]---> BDD-cost:    3
c ---[1166]---> BDD-cost:    2
c ---[1165]---> BDD-cost:    2
c ---[1164]---> BDD-cost:    2
c ---[1163]---> BDD-cost:    2
c ---[1162]---> BDD-cost:    2
c ---[1161]---> BDD-cost:    2
c ---[1160]---> BDD-cost:    2
c ---[1151]---> BDD-cost:    2
c ---[1150]---> BDD-cost:    2
c ---[1149]---> BDD-cost:    2
c ---[1148]---> BDD-cost:    2
c ---[1147]---> BDD-cost:    2
c ---[1146]---> BDD-cost:    2
c ---[1145]---> BDD-cost:    2
c ---[1144]---> BDD-cost:    2
c ---[1143]---> BDD-cost:    2
c ---[1142]---> BDD-cost:    2
c ---[1141]---> BDD-cost:    2
c ---[1140]---> BDD-cost:    2
c ---[1139]---> BDD-cost:    2
c ---[1138]---> BDD-cost:    2
c ---[1137]---> BDD-cost:    2
c ---[1136]---> BDD-cost:    2
c ---[1135]---> BDD-cost:    2
c ---[1134]---> BDD-cost:    2
c ---[1133]---> BDD-cost:    2
c ---[1132]---> BDD-cost:    2
c ---[1131]---> BDD-cost:    2
c ---[1130]---> BDD-cost:    2
c ---[1129]---> BDD-cost:    2
c ---[1128]---> BDD-cost:    2
c ---[1127]---> BDD-cost:    2
c ---[1126]---> BDD-cost:    2
c ---[1125]---> BDD-cost:    2
c ---[1124]---> BDD-cost:    2
c ---[1123]---> BDD-cost:    2
c ---[1122]---> BDD-cost:    2
c ---[1121]---> BDD-cost:    2
c ---[1120]---> BDD-cost:    2
c ---[1119]---> BDD-cost:    2
c ---[1118]---> BDD-cost:    2
c ---[1117]---> BDD-cost:    2
c ---[1116]---> BDD-cost:    2
c ---[1115]---> BDD-cost:    2
c ---[1114]---> BDD-cost:    2
c ---[1113]---> BDD-cost:    2
c ---[1112]---> BDD-cost:    2
c ---[1111]---> BDD-cost:    2
c ---[1110]---> BDD-cost:    2
c ---[1109]---> BDD-cost:    2
c ---[1108]---> BDD-cost:    2
c ---[1107]---> BDD-cost:    2
c ---[1106]---> BDD-cost:    2
c ---[1105]---> BDD-cost:    2
c ---[1104]---> BDD-cost:    2
c ---[1103]---> BDD-cost:    2
c ---[1102]---> BDD-cost:    2
c ---[1101]---> BDD-cost:    2
c ---[1100]---> BDD-cost:    2
c ---[1099]---> BDD-cost:    2
c ---[1098]---> BDD-cost:    2
c ---[1097]---> BDD-cost:    2
c ---[1096]---> BDD-cost:    2
c ---[1087]---> BDD-cost:    2
c ---[1086]---> BDD-cost:    2
c ---[1085]---> BDD-cost:    2
c ---[1084]---> BDD-cost:    2
c ---[1083]---> BDD-cost:    2
c ---[1082]---> BDD-cost:    2
c ---[1081]---> BDD-cost:    2
c ---[1080]---> BDD-cost:    2
c ---[1079]---> BDD-cost:    2
c ---[1078]---> BDD-cost:    2
c ---[1077]---> BDD-cost:    2
c ---[1076]---> BDD-cost:    2
c ---[1075]---> BDD-cost:    2
c ---[1074]---> BDD-cost:    2
c ---[1073]---> BDD-cost:    2
c ---[1072]---> BDD-cost:    2
c ---[1071]---> BDD-cost:    2
c ---[1070]---> BDD-cost:    2
c ---[1069]---> BDD-cost:    2
c ---[1068]---> BDD-cost:    2
c ---[1067]---> BDD-cost:    2
c ---[1066]---> BDD-cost:    2
c ---[1065]---> BDD-cost:    2
c ---[1064]---> BDD-cost:    2
c ---[1063]---> BDD-cost:    2
c ---[1062]---> BDD-cost:    2
c ---[1061]---> BDD-cost:    2
c ---[1060]---> BDD-cost:    2
c ---[1059]---> BDD-cost:    2
c ---[1058]---> BDD-cost:    2
c ---[1057]---> BDD-cost:    2
c ---[1056]---> BDD-cost:    2
c ---[1055]---> BDD-cost:    2
c ---[1054]---> BDD-cost:    2
c ---[1053]---> BDD-cost:    2
c ---[1052]---> BDD-cost:    2
c ---[1051]---> BDD-cost:    2
c ---[1050]---> BDD-cost:    2
c ---[1049]---> BDD-cost:    2
c ---[1048]---> BDD-cost:    2
c ---[1047]---> BDD-cost:    2
c ---[1046]---> BDD-cost:    2
c ---[1045]---> BDD-cost:    2
c ---[1044]---> BDD-cost:    2
c ---[1043]---> BDD-cost:    2
c ---[1042]---> BDD-cost:    2
c ---[1041]---> BDD-cost:    2
c ---[1040]---> BDD-cost:    2
c ---[1039]---> BDD-cost:    2
c ---[1038]---> BDD-cost:    2
c ---[1037]---> BDD-cost:    2
c ---[1036]---> BDD-cost:    2
c ---[1035]---> BDD-cost:    2
c ---[1034]---> BDD-cost:    2
c ---[1033]---> BDD-cost:    2
c ---[1032]---> BDD-cost:    2
c ---[1023]---> BDD-cost:    2
c ---[1022]---> BDD-cost:    2
c ---[1021]---> BDD-cost:    2
c ---[1020]---> BDD-cost:    2
c ---[1019]---> BDD-cost:    2
c ---[1018]---> BDD-cost:    2
c ---[1017]---> BDD-cost:    2
c ---[1016]---> BDD-cost:    2
c ---[1015]---> BDD-cost:    2
c ---[1014]---> BDD-cost:    2
c ---[1013]---> BDD-cost:    2
c ---[1012]---> BDD-cost:    2
c ---[1011]---> BDD-cost:    2
c ---[1010]---> BDD-cost:    2
c ---[1009]---> BDD-cost:    2
c ---[1008]---> BDD-cost:    2
c ---[1007]---> BDD-cost:    2
c ---[1006]---> BDD-cost:    2
c ---[1005]---> BDD-cost:    2
c ---[1004]---> BDD-cost:    2
c ---[1003]---> BDD-cost:    2
c ---[1002]---> BDD-cost:    2
c ---[1001]---> BDD-cost:    2
c ---[1000]---> BDD-cost:    2
c ---[ 999]---> BDD-cost:    2
c ---[ 998]---> BDD-cost:    2
c ---[ 997]---> BDD-cost:    2
c ---[ 996]---> BDD-cost:    2
c ---[ 995]---> BDD-cost:    2
c ---[ 994]---> BDD-cost:    2
c ---[ 993]---> BDD-cost:    2
c ---[ 992]---> BDD-cost:    2
c ---[ 991]---> BDD-cost:    2
c ---[ 990]---> BDD-cost:    2
c ---[ 989]---> BDD-cost:    2
c ---[ 988]---> BDD-cost:    2
c ---[ 987]---> BDD-cost:    2
c ---[ 986]---> BDD-cost:    2
c ---[ 985]---> BDD-cost:    2
c ---[ 984]---> BDD-cost:    2
c ---[ 983]---> BDD-cost:    2
c ---[ 982]---> BDD-cost:    2
c ---[ 981]---> BDD-cost:    2
c ---[ 980]---> BDD-cost:    2
c ---[ 979]---> BDD-cost:    2
c ---[ 978]---> BDD-cost:    2
c ---[ 977]---> BDD-cost:    2
c ---[ 976]---> BDD-cost:    2
c ---[ 975]---> BDD-cost:    2
c ---[ 974]---> BDD-cost:    2
c ---[ 973]---> BDD-cost:    2
c ---[ 972]---> BDD-cost:    2
c ---[ 971]---> BDD-cost:    2
c ---[ 970]---> BDD-cost:    2
c ---[ 969]---> BDD-cost:    2
c ---[ 968]---> BDD-cost:    2
c ---[ 959]---> BDD-cost:    9
c ---[ 958]---> BDD-cost:    2
c ---[ 957]---> BDD-cost:    9
c ---[ 956]---> BDD-cost:    2
c ---[ 955]---> BDD-cost:    9
c ---[ 954]---> BDD-cost:    2
c ---[ 953]---> BDD-cost:    9
c ---[ 952]---> BDD-cost:    2
c ---[ 951]---> BDD-cost:    8
c ---[ 950]---> BDD-cost:    2
c ---[ 949]---> BDD-cost:    8
c ---[ 948]---> BDD-cost:    2
c ---[ 947]---> BDD-cost:    8
c ---[ 946]---> BDD-cost:    2
c ---[ 945]---> BDD-cost:    8
c ---[ 944]---> BDD-cost:    2
c ---[ 943]---> BDD-cost:    7
c ---[ 942]---> BDD-cost:    2
c ---[ 941]---> BDD-cost:    7
c ---[ 940]---> BDD-cost:    2
c ---[ 939]---> BDD-cost:    7
c ---[ 938]---> BDD-cost:    2
c ---[ 937]---> BDD-cost:    7
c ---[ 936]---> BDD-cost:    2
c ---[ 935]---> BDD-cost:    6
c ---[ 934]---> BDD-cost:    2
c ---[ 933]---> BDD-cost:    6
c ---[ 932]---> BDD-cost:    2
c ---[ 931]---> BDD-cost:    6
c ---[ 930]---> BDD-cost:    2
c ---[ 929]---> BDD-cost:    6
c ---[ 928]---> BDD-cost:    2
c ---[ 927]---> BDD-cost:    5
c ---[ 926]---> BDD-cost:    2
c ---[ 925]---> BDD-cost:    5
c ---[ 924]---> BDD-cost:    2
c ---[ 923]---> BDD-cost:    5
c ---[ 922]---> BDD-cost:    2
c ---[ 921]---> BDD-cost:    5
c ---[ 920]---> BDD-cost:    2
c ---[ 919]---> BDD-cost:    4
c ---[ 918]---> BDD-cost:    2
c ---[ 917]---> BDD-cost:    4
c ---[ 916]---> BDD-cost:    2
c ---[ 915]---> BDD-cost:    4
c ---[ 914]---> BDD-cost:    2
c ---[ 913]---> BDD-cost:    4
c ---[ 912]---> BDD-cost:    2
c ---[ 911]---> BDD-cost:    3
c ---[ 910]---> BDD-cost:    2
c ---[ 909]---> BDD-cost:    3
c ---[ 908]---> BDD-cost:    2
c ---[ 907]---> BDD-cost:    3
c ---[ 906]---> BDD-cost:    2
c ---[ 905]---> BDD-cost:    3
c ---[ 904]---> BDD-cost:    2
c ---[ 895]---> BDD-cost:    6
c ---[ 894]---> BDD-cost:    2
c ---[ 893]---> BDD-cost:    2
c ---[ 892]---> BDD-cost:    2
c ---[ 891]---> BDD-cost:    2
c ---[ 890]---> BDD-cost:    2
c ---[ 889]---> BDD-cost:    2
c ---[ 888]---> BDD-cost:    2
c ---[ 887]---> BDD-cost:    5
c ---[ 886]---> BDD-cost:    2
c ---[ 885]---> BDD-cost:    2
c ---[ 884]---> BDD-cost:    2
c ---[ 883]---> BDD-cost:    2
c ---[ 882]---> BDD-cost:    2
c ---[ 881]---> BDD-cost:    2
c ---[ 880]---> BDD-cost:    2
c ---[ 879]---> BDD-cost:    4
c ---[ 878]---> BDD-cost:    2
c ---[ 877]---> BDD-cost:    2
c ---[ 876]---> BDD-cost:    2
c ---[ 875]---> BDD-cost:    2
c ---[ 874]---> BDD-cost:    2
c ---[ 873]---> BDD-cost:    2
c ---[ 872]---> BDD-cost:    2
c ---[ 871]---> BDD-cost:    3
c ---[ 870]---> BDD-cost:    2
c ---[ 869]---> BDD-cost:    2
c ---[ 868]---> BDD-cost:    2
c ---[ 867]---> BDD-cost:    2
c ---[ 866]---> BDD-cost:    2
c ---[ 865]---> BDD-cost:    2
c ---[ 864]---> BDD-cost:    2
c ---[ 863]---> BDD-cost:    2
c ---[ 862]---> BDD-cost:    2
c ---[ 861]---> BDD-cost:    2
c ---[ 860]---> BDD-cost:    2
c ---[ 859]---> BDD-cost:    2
c ---[ 858]---> BDD-cost:    2
c ---[ 857]---> BDD-cost:    2
c ---[ 856]---> BDD-cost:    2
c ---[ 855]---> BDD-cost:    4
c ---[ 854]---> BDD-cost:    2
c ---[ 853]---> BDD-cost:    2
c ---[ 852]---> BDD-cost:    2
c ---[ 851]---> BDD-cost:    2
c ---[ 850]---> BDD-cost:    2
c ---[ 849]---> BDD-cost:    2
c ---[ 848]---> BDD-cost:    2
c ---[ 847]---> BDD-cost:    3
c ---[ 846]---> BDD-cost:    2
c ---[ 845]---> BDD-cost:    2
c ---[ 844]---> BDD-cost:    2
c ---[ 843]---> BDD-cost:    2
c ---[ 842]---> BDD-cost:    2
c ---[ 841]---> BDD-cost:    2
c ---[ 840]---> BDD-cost:    2
c ---[ 831]---> BDD-cost:    2
c ---[ 830]---> BDD-cost:    2
c ---[ 829]---> BDD-cost:    2
c ---[ 828]---> BDD-cost:    2
c ---[ 827]---> BDD-cost:    2
c ---[ 826]---> BDD-cost:    2
c ---[ 825]---> BDD-cost:    2
c ---[ 824]---> BDD-cost:    2
c ---[ 823]---> BDD-cost:    2
c ---[ 822]---> BDD-cost:    2
c ---[ 821]---> BDD-cost:    2
c ---[ 820]---> BDD-cost:    2
c ---[ 819]---> BDD-cost:    2
c ---[ 818]---> BDD-cost:    2
c ---[ 817]---> BDD-cost:    2
c ---[ 816]---> BDD-cost:    2
c ---[ 815]---> BDD-cost:    2
c ---[ 814]---> BDD-cost:    2
c ---[ 813]---> BDD-cost:    2
c ---[ 812]---> BDD-cost:    2
c ---[ 811]---> BDD-cost:    2
c ---[ 810]---> BDD-cost:    2
c ---[ 809]---> BDD-cost:    2
c ---[ 808]---> BDD-cost:    2
c ---[ 807]---> BDD-cost:    2
c ---[ 806]---> BDD-cost:    2
c ---[ 805]---> BDD-cost:    2
c ---[ 804]---> BDD-cost:    2
c ---[ 803]---> BDD-cost:    2
c ---[ 802]---> BDD-cost:    2
c ---[ 801]---> BDD-cost:    2
c ---[ 800]---> BDD-cost:    2
c ---[ 799]---> BDD-cost:    2
c ---[ 798]---> BDD-cost:    2
c ---[ 797]---> BDD-cost:    2
c ---[ 796]---> BDD-cost:    2
c ---[ 795]---> BDD-cost:    2
c ---[ 794]---> BDD-cost:    2
c ---[ 793]---> BDD-cost:    2
c ---[ 792]---> BDD-cost:    2
c ---[ 791]---> BDD-cost:    2
c ---[ 790]---> BDD-cost:    2
c ---[ 789]---> BDD-cost:    2
c ---[ 788]---> BDD-cost:    2
c ---[ 787]---> BDD-cost:    2
c ---[ 786]---> BDD-cost:    2
c ---[ 785]---> BDD-cost:    2
c ---[ 784]---> BDD-cost:    2
c ---[ 783]---> BDD-cost:    2
c ---[ 782]---> BDD-cost:    2
c ---[ 781]---> BDD-cost:    2
c ---[ 780]---> BDD-cost:    2
c ---[ 779]---> BDD-cost:    2
c ---[ 778]---> BDD-cost:    2
c ---[ 777]---> BDD-cost:    2
c ---[ 776]---> BDD-cost:    2
c ---[ 767]---> BDD-cost:    2
c ---[ 766]---> BDD-cost:    2
c ---[ 765]---> BDD-cost:    2
c ---[ 764]---> BDD-cost:    2
c ---[ 763]---> BDD-cost:    2
c ---[ 762]---> BDD-cost:    2
c ---[ 761]---> BDD-cost:    2
c ---[ 760]---> BDD-cost:    2
c ---[ 759]---> BDD-cost:    2
c ---[ 758]---> BDD-cost:    2
c ---[ 757]---> BDD-cost:    2
c ---[ 756]---> BDD-cost:    2
c ---[ 755]---> BDD-cost:    2
c ---[ 754]---> BDD-cost:    2
c ---[ 753]---> BDD-cost:    2
c ---[ 752]---> BDD-cost:    2
c ---[ 751]---> BDD-cost:    2
c ---[ 750]---> BDD-cost:    2
c ---[ 749]---> BDD-cost:    2
c ---[ 748]---> BDD-cost:    2
c ---[ 747]---> BDD-cost:    2
c ---[ 746]---> BDD-cost:    2
c ---[ 745]---> BDD-cost:    2
c ---[ 744]---> BDD-cost:    2
c ---[ 743]---> BDD-cost:    2
c ---[ 742]---> BDD-cost:    2
c ---[ 741]---> BDD-cost:    2
c ---[ 740]---> BDD-cost:    2
c ---[ 739]---> BDD-cost:    2
c ---[ 738]---> BDD-cost:    2
c ---[ 737]---> BDD-cost:    2
c ---[ 736]---> BDD-cost:    2
c ---[ 735]---> BDD-cost:    2
c ---[ 734]---> BDD-cost:    2
c ---[ 733]---> BDD-cost:    2
c ---[ 732]---> BDD-cost:    2
c ---[ 731]---> BDD-cost:    2
c ---[ 730]---> BDD-cost:    2
c ---[ 729]---> BDD-cost:    2
c ---[ 728]---> BDD-cost:    2
c ---[ 727]---> BDD-cost:    2
c ---[ 726]---> BDD-cost:    2
c ---[ 725]---> BDD-cost:    2
c ---[ 724]---> BDD-cost:    2
c ---[ 723]---> BDD-cost:    2
c ---[ 722]---> BDD-cost:    2
c ---[ 721]---> BDD-cost:    2
c ---[ 720]---> BDD-cost:    2
c ---[ 719]---> BDD-cost:    2
c ---[ 718]---> BDD-cost:    2
c ---[ 717]---> BDD-cost:    2
c ---[ 716]---> BDD-cost:    2
c ---[ 715]---> BDD-cost:    2
c ---[ 714]---> BDD-cost:    2
c ---[ 713]---> BDD-cost:    2
c ---[ 712]---> BDD-cost:    2
c ---[ 703]---> BDD-cost:    2
c ---[ 702]---> BDD-cost:    2
c ---[ 701]---> BDD-cost:    2
c ---[ 700]---> BDD-cost:    2
c ---[ 699]---> BDD-cost:    2
c ---[ 698]---> BDD-cost:    2
c ---[ 697]---> BDD-cost:    2
c ---[ 696]---> BDD-cost:    2
c ---[ 695]---> BDD-cost:    2
c ---[ 694]---> BDD-cost:    2
c ---[ 693]---> BDD-cost:    2
c ---[ 692]---> BDD-cost:    2
c ---[ 691]---> BDD-cost:    2
c ---[ 690]---> BDD-cost:    2
c ---[ 689]---> BDD-cost:    2
c ---[ 688]---> BDD-cost:    2
c ---[ 687]---> BDD-cost:    2
c ---[ 686]---> BDD-cost:    2
c ---[ 685]---> BDD-cost:    2
c ---[ 684]---> BDD-cost:    2
c ---[ 683]---> BDD-cost:    2
c ---[ 682]---> BDD-cost:    2
c ---[ 681]---> BDD-cost:    2
c ---[ 680]---> BDD-cost:    2
c ---[ 679]---> BDD-cost:    2
c ---[ 678]---> BDD-cost:    2
c ---[ 677]---> BDD-cost:    2
c ---[ 676]---> BDD-cost:    2
c ---[ 675]---> BDD-cost:    2
c ---[ 674]---> BDD-cost:    2
c ---[ 673]---> BDD-cost:    2
c ---[ 672]---> BDD-cost:    2
c ---[ 671]---> BDD-cost:    2
c ---[ 670]---> BDD-cost:    2
c ---[ 669]---> BDD-cost:    2
c ---[ 668]---> BDD-cost:    2
c ---[ 667]---> BDD-cost:    2
c ---[ 666]---> BDD-cost:    2
c ---[ 665]---> BDD-cost:    2
c ---[ 664]---> BDD-cost:    2
c ---[ 663]---> BDD-cost:    2
c ---[ 662]---> BDD-cost:    2
c ---[ 661]---> BDD-cost:    2
c ---[ 660]---> BDD-cost:    2
c ---[ 659]---> BDD-cost:    2
c ---[ 658]---> BDD-cost:    2
c ---[ 657]---> BDD-cost:    2
c ---[ 656]---> BDD-cost:    2
c ---[ 655]---> BDD-cost:    2
c ---[ 654]---> BDD-cost:    2
c ---[ 653]---> BDD-cost:    2
c ---[ 652]---> BDD-cost:    2
c ---[ 651]---> BDD-cost:    2
c ---[ 650]---> BDD-cost:    2
c ---[ 649]---> BDD-cost:    2
c ---[ 648]---> BDD-cost:    2
c ---[ 639]---> BDD-cost:    9
c ---[ 638]---> BDD-cost:    2
c ---[ 637]---> BDD-cost:    9
c ---[ 636]---> BDD-cost:    2
c ---[ 635]---> BDD-cost:    9
c ---[ 634]---> BDD-cost:    2
c ---[ 633]---> BDD-cost:    9
c ---[ 632]---> BDD-cost:    2
c ---[ 631]---> BDD-cost:    8
c ---[ 630]---> BDD-cost:    2
c ---[ 629]---> BDD-cost:    8
c ---[ 628]---> BDD-cost:    2
c ---[ 627]---> BDD-cost:    8
c ---[ 626]---> BDD-cost:    2
c ---[ 625]---> BDD-cost:    8
c ---[ 624]---> BDD-cost:    2
c ---[ 623]---> BDD-cost:    7
c ---[ 622]---> BDD-cost:    2
c ---[ 621]---> BDD-cost:    7
c ---[ 620]---> BDD-cost:    2
c ---[ 619]---> BDD-cost:    7
c ---[ 618]---> BDD-cost:    2
c ---[ 617]---> BDD-cost:    7
c ---[ 616]---> BDD-cost:    2
c ---[ 615]---> BDD-cost:    6
c ---[ 614]---> BDD-cost:    2
c ---[ 613]---> BDD-cost:    6
c ---[ 612]---> BDD-cost:    2
c ---[ 611]---> BDD-cost:    6
c ---[ 610]---> BDD-cost:    2
c ---[ 609]---> BDD-cost:    6
c ---[ 608]---> BDD-cost:    2
c ---[ 607]---> BDD-cost:    5
c ---[ 606]---> BDD-cost:    2
c ---[ 605]---> BDD-cost:    5
c ---[ 604]---> BDD-cost:    2
c ---[ 603]---> BDD-cost:    5
c ---[ 602]---> BDD-cost:    2
c ---[ 601]---> BDD-cost:    5
c ---[ 600]---> BDD-cost:    2
c ---[ 599]---> BDD-cost:    4
c ---[ 598]---> BDD-cost:    2
c ---[ 597]---> BDD-cost:    4
c ---[ 596]---> BDD-cost:    2
c ---[ 595]---> BDD-cost:    4
c ---[ 594]---> BDD-cost:    2
c ---[ 593]---> BDD-cost:    4
c ---[ 592]---> BDD-cost:    2
c ---[ 591]---> BDD-cost:    3
c ---[ 590]---> BDD-cost:    2
c ---[ 589]---> BDD-cost:    3
c ---[ 588]---> BDD-cost:    2
c ---[ 587]---> BDD-cost:    3
c ---[ 586]---> BDD-cost:    2
c ---[ 585]---> BDD-cost:    3
c ---[ 584]---> BDD-cost:    2
c ---[ 575]---> BDD-cost:    6
c ---[ 574]---> BDD-cost:    2
c ---[ 573]---> BDD-cost:    2
c ---[ 572]---> BDD-cost:    2
c ---[ 571]---> BDD-cost:    2
c ---[ 570]---> BDD-cost:    2
c ---[ 569]---> BDD-cost:    2
c ---[ 568]---> BDD-cost:    2
c ---[ 567]---> BDD-cost:    5
c ---[ 566]---> BDD-cost:    2
c ---[ 565]---> BDD-cost:    2
c ---[ 564]---> BDD-cost:    2
c ---[ 563]---> BDD-cost:    2
c ---[ 562]---> BDD-cost:    2
c ---[ 561]---> BDD-cost:    2
c ---[ 560]---> BDD-cost:    2
c ---[ 559]---> BDD-cost:    4
c ---[ 558]---> BDD-cost:    2
c ---[ 557]---> BDD-cost:    2
c ---[ 556]---> BDD-cost:    2
c ---[ 555]---> BDD-cost:    2
c ---[ 554]---> BDD-cost:    2
c ---[ 553]---> BDD-cost:    2
c ---[ 552]---> BDD-cost:    2
c ---[ 551]---> BDD-cost:    3
c ---[ 550]---> BDD-cost:    2
c ---[ 549]---> BDD-cost:    2
c ---[ 548]---> BDD-cost:    2
c ---[ 547]---> BDD-cost:    2
c ---[ 546]---> BDD-cost:    2
c ---[ 545]---> BDD-cost:    2
c ---[ 544]---> BDD-cost:    2
c ---[ 543]---> BDD-cost:    2
c ---[ 542]---> BDD-cost:    2
c ---[ 541]---> BDD-cost:    2
c ---[ 540]---> BDD-cost:    2
c ---[ 539]---> BDD-cost:    2
c ---[ 538]---> BDD-cost:    2
c ---[ 537]---> BDD-cost:    2
c ---[ 536]---> BDD-cost:    2
c ---[ 535]---> BDD-cost:    4
c ---[ 534]---> BDD-cost:    2
c ---[ 533]---> BDD-cost:    2
c ---[ 532]---> BDD-cost:    2
c ---[ 531]---> BDD-cost:    2
c ---[ 530]---> BDD-cost:    2
c ---[ 529]---> BDD-cost:    2
c ---[ 528]---> BDD-cost:    2
c ---[ 527]---> BDD-cost:    3
c ---[ 526]---> BDD-cost:    2
c ---[ 525]---> BDD-cost:    2
c ---[ 524]---> BDD-cost:    2
c ---[ 523]---> BDD-cost:    2
c ---[ 522]---> BDD-cost:    2
c ---[ 521]---> BDD-cost:    2
c ---[ 520]---> BDD-cost:    2
c ---[ 511]---> BDD-cost:    2
c ---[ 510]---> BDD-cost:    2
c ---[ 509]---> BDD-cost:    2
c ---[ 508]---> BDD-cost:    2
c ---[ 507]---> BDD-cost:    2
c ---[ 506]---> BDD-cost:    2
c ---[ 505]---> BDD-cost:    2
c ---[ 504]---> BDD-cost:    2
c ---[ 503]---> BDD-cost:    2
c ---[ 502]---> BDD-cost:    2
c ---[ 501]---> BDD-cost:    2
c ---[ 500]---> BDD-cost:    2
c ---[ 499]---> BDD-cost:    2
c ---[ 498]---> BDD-cost:    2
c ---[ 497]---> BDD-cost:    2
c ---[ 496]---> BDD-cost:    2
c ---[ 495]---> BDD-cost:    2
c ---[ 494]---> BDD-cost:    2
c ---[ 493]---> BDD-cost:    2
c ---[ 492]---> BDD-cost:    2
c ---[ 491]---> BDD-cost:    2
c ---[ 490]---> BDD-cost:    2
c ---[ 489]---> BDD-cost:    2
c ---[ 488]---> BDD-cost:    2
c ---[ 487]---> BDD-cost:    2
c ---[ 486]---> BDD-cost:    2
c ---[ 485]---> BDD-cost:    2
c ---[ 484]---> BDD-cost:    2
c ---[ 483]---> BDD-cost:    2
c ---[ 482]---> BDD-cost:    2
c ---[ 481]---> BDD-cost:    2
c ---[ 480]---> BDD-cost:    2
c ---[ 479]---> BDD-cost:    2
c ---[ 478]---> BDD-cost:    2
c ---[ 477]---> BDD-cost:    2
c ---[ 476]---> BDD-cost:    2
c ---[ 475]---> BDD-cost:    2
c ---[ 474]---> BDD-cost:    2
c ---[ 473]---> BDD-cost:    2
c ---[ 472]---> BDD-cost:    2
c ---[ 471]---> BDD-cost:    2
c ---[ 470]---> BDD-cost:    2
c ---[ 469]---> BDD-cost:    2
c ---[ 468]---> BDD-cost:    2
c ---[ 467]---> BDD-cost:    2
c ---[ 466]---> BDD-cost:    2
c ---[ 465]---> BDD-cost:    2
c ---[ 464]---> BDD-cost:    2
c ---[ 463]---> BDD-cost:    2
c ---[ 462]---> BDD-cost:    2
c ---[ 461]---> BDD-cost:    2
c ---[ 460]---> BDD-cost:    2
c ---[ 459]---> BDD-cost:    2
c ---[ 458]---> BDD-cost:    2
c ---[ 457]---> BDD-cost:    2
c ---[ 456]---> BDD-cost:    2
c ---[ 447]---> BDD-cost:    2
c ---[ 446]---> BDD-cost:    2
c ---[ 445]---> BDD-cost:    2
c ---[ 444]---> BDD-cost:    2
c ---[ 443]---> BDD-cost:    2
c ---[ 442]---> BDD-cost:    2
c ---[ 441]---> BDD-cost:    2
c ---[ 440]---> BDD-cost:    2
c ---[ 439]---> BDD-cost:    2
c ---[ 438]---> BDD-cost:    2
c ---[ 437]---> BDD-cost:    2
c ---[ 436]---> BDD-cost:    2
c ---[ 435]---> BDD-cost:    2
c ---[ 434]---> BDD-cost:    2
c ---[ 433]---> BDD-cost:    2
c ---[ 432]---> BDD-cost:    2
c ---[ 431]---> BDD-cost:    2
c ---[ 430]---> BDD-cost:    2
c ---[ 429]---> BDD-cost:    2
c ---[ 428]---> BDD-cost:    2
c ---[ 427]---> BDD-cost:    2
c ---[ 426]---> BDD-cost:    2
c ---[ 425]---> BDD-cost:    2
c ---[ 424]---> BDD-cost:    2
c ---[ 423]---> BDD-cost:    2
c ---[ 422]---> BDD-cost:    2
c ---[ 421]---> BDD-cost:    2
c ---[ 420]---> BDD-cost:    2
c ---[ 419]---> BDD-cost:    2
c ---[ 418]---> BDD-cost:    2
c ---[ 417]---> BDD-cost:    2
c ---[ 416]---> BDD-cost:    2
c ---[ 415]---> BDD-cost:    2
c ---[ 414]---> BDD-cost:    2
c ---[ 413]---> BDD-cost:    2
c ---[ 412]---> BDD-cost:    2
c ---[ 411]---> BDD-cost:    2
c ---[ 410]---> BDD-cost:    2
c ---[ 409]---> BDD-cost:    2
c ---[ 408]---> BDD-cost:    2
c ---[ 407]---> BDD-cost:    2
c ---[ 406]---> BDD-cost:    2
c ---[ 405]---> BDD-cost:    2
c ---[ 404]---> BDD-cost:    2
c ---[ 403]---> BDD-cost:    2
c ---[ 402]---> BDD-cost:    2
c ---[ 401]---> BDD-cost:    2
c ---[ 400]---> BDD-cost:    2
c ---[ 399]---> BDD-cost:    2
c ---[ 398]---> BDD-cost:    2
c ---[ 397]---> BDD-cost:    2
c ---[ 396]---> BDD-cost:    2
c ---[ 395]---> BDD-cost:    2
c ---[ 394]---> BDD-cost:    2
c ---[ 393]---> BDD-cost:    2
c ---[ 392]---> BDD-cost:    2
c ---[ 383]---> BDD-cost:    2
c ---[ 382]---> BDD-cost:    2
c ---[ 381]---> BDD-cost:    2
c ---[ 380]---> BDD-cost:    2
c ---[ 379]---> BDD-cost:    2
c ---[ 378]---> BDD-cost:    2
c ---[ 377]---> BDD-cost:    2
c ---[ 376]---> BDD-cost:    2
c ---[ 375]---> BDD-cost:    2
c ---[ 374]---> BDD-cost:    2
c ---[ 373]---> BDD-cost:    2
c ---[ 372]---> BDD-cost:    2
c ---[ 371]---> BDD-cost:    2
c ---[ 370]---> BDD-cost:    2
c ---[ 369]---> BDD-cost:    2
c ---[ 368]---> BDD-cost:    2
c ---[ 367]---> BDD-cost:    2
c ---[ 366]---> BDD-cost:    2
c ---[ 365]---> BDD-cost:    2
c ---[ 364]---> BDD-cost:    2
c ---[ 363]---> BDD-cost:    2
c ---[ 362]---> BDD-cost:    2
c ---[ 361]---> BDD-cost:    2
c ---[ 360]---> BDD-cost:    2
c ---[ 359]---> BDD-cost:    2
c ---[ 358]---> BDD-cost:    2
c ---[ 357]---> BDD-cost:    2
c ---[ 356]---> BDD-cost:    2
c ---[ 355]---> BDD-cost:    2
c ---[ 354]---> BDD-cost:    2
c ---[ 353]---> BDD-cost:    2
c ---[ 352]---> BDD-cost:    2
c ---[ 351]---> BDD-cost:    2
c ---[ 350]---> BDD-cost:    2
c ---[ 349]---> BDD-cost:    2
c ---[ 348]---> BDD-cost:    2
c ---[ 347]---> BDD-cost:    2
c ---[ 346]---> BDD-cost:    2
c ---[ 345]---> BDD-cost:    2
c ---[ 344]---> BDD-cost:    2
c ---[ 343]---> BDD-cost:    2
c ---[ 342]---> BDD-cost:    2
c ---[ 341]---> BDD-cost:    2
c ---[ 340]---> BDD-cost:    2
c ---[ 339]---> BDD-cost:    2
c ---[ 338]---> BDD-cost:    2
c ---[ 337]---> BDD-cost:    2
c ---[ 336]---> BDD-cost:    2
c ---[ 335]---> BDD-cost:    2
c ---[ 334]---> BDD-cost:    2
c ---[ 333]---> BDD-cost:    2
c ---[ 332]---> BDD-cost:    2
c ---[ 331]---> BDD-cost:    2
c ---[ 330]---> BDD-cost:    2
c ---[ 329]---> BDD-cost:    2
c ---[ 328]---> BDD-cost:    2
c ---[ 319]---> BDD-cost:    9
c ---[ 318]---> BDD-cost:    2
c ---[ 317]---> BDD-cost:    9
c ---[ 316]---> BDD-cost:    2
c ---[ 315]---> BDD-cost:    9
c ---[ 314]---> BDD-cost:    2
c ---[ 313]---> BDD-cost:    9
c ---[ 312]---> BDD-cost:    2
c ---[ 311]---> BDD-cost:    8
c ---[ 310]---> BDD-cost:    2
c ---[ 309]---> BDD-cost:    8
c ---[ 308]---> BDD-cost:    2
c ---[ 307]---> BDD-cost:    8
c ---[ 306]---> BDD-cost:    2
c ---[ 305]---> BDD-cost:    8
c ---[ 304]---> BDD-cost:    2
c ---[ 303]---> BDD-cost:    7
c ---[ 302]---> BDD-cost:    2
c ---[ 301]---> BDD-cost:    7
c ---[ 300]---> BDD-cost:    2
c ---[ 299]---> BDD-cost:    7
c ---[ 298]---> BDD-cost:    2
c ---[ 297]---> BDD-cost:    7
c ---[ 296]---> BDD-cost:    2
c ---[ 295]---> BDD-cost:    6
c ---[ 294]---> BDD-cost:    2
c ---[ 293]---> BDD-cost:    6
c ---[ 292]---> BDD-cost:    2
c ---[ 291]---> BDD-cost:    6
c ---[ 290]---> BDD-cost:    2
c ---[ 289]---> BDD-cost:    6
c ---[ 288]---> BDD-cost:    2
c ---[ 287]---> BDD-cost:    5
c ---[ 286]---> BDD-cost:    2
c ---[ 285]---> BDD-cost:    5
c ---[ 284]---> BDD-cost:    2
c ---[ 283]---> BDD-cost:    5
c ---[ 282]---> BDD-cost:    2
c ---[ 281]---> BDD-cost:    5
c ---[ 280]---> BDD-cost:    2
c ---[ 279]---> BDD-cost:    4
c ---[ 278]---> BDD-cost:    2
c ---[ 277]---> BDD-cost:    4
c ---[ 276]---> BDD-cost:    2
c ---[ 275]---> BDD-cost:    4
c ---[ 274]---> BDD-cost:    2
c ---[ 273]---> BDD-cost:    4
c ---[ 272]---> BDD-cost:    2
c ---[ 271]---> BDD-cost:    3
c ---[ 270]---> BDD-cost:    2
c ---[ 269]---> BDD-cost:    3
c ---[ 268]---> BDD-cost:    2
c ---[ 267]---> BDD-cost:    3
c ---[ 266]---> BDD-cost:    2
c ---[ 265]---> BDD-cost:    3
c ---[ 264]---> BDD-cost:    2
c ---[ 255]---> BDD-cost:    6
c ---[ 254]---> BDD-cost:    2
c ---[ 253]---> BDD-cost:    2
c ---[ 252]---> BDD-cost:    2
c ---[ 251]---> BDD-cost:    2
c ---[ 250]---> BDD-cost:    2
c ---[ 249]---> BDD-cost:    2
c ---[ 248]---> BDD-cost:    2
c ---[ 247]---> BDD-cost:    5
c ---[ 246]---> BDD-cost:    2
c ---[ 245]---> BDD-cost:    2
c ---[ 244]---> BDD-cost:    2
c ---[ 243]---> BDD-cost:    2
c ---[ 242]---> BDD-cost:    2
c ---[ 241]---> BDD-cost:    2
c ---[ 240]---> BDD-cost:    2
c ---[ 239]---> BDD-cost:    4
c ---[ 238]---> BDD-cost:    2
c ---[ 237]---> BDD-cost:    2
c ---[ 236]---> BDD-cost:    2
c ---[ 235]---> BDD-cost:    2
c ---[ 234]---> BDD-cost:    2
c ---[ 233]---> BDD-cost:    2
c ---[ 232]---> BDD-cost:    2
c ---[ 231]---> BDD-cost:    3
c ---[ 230]---> BDD-cost:    2
c ---[ 229]---> BDD-cost:    2
c ---[ 228]---> BDD-cost:    2
c ---[ 227]---> BDD-cost:    2
c ---[ 226]---> BDD-cost:    2
c ---[ 225]---> BDD-cost:    2
c ---[ 224]---> BDD-cost:    2
c ---[ 223]---> BDD-cost:    2
c ---[ 222]---> BDD-cost:    2
c ---[ 221]---> BDD-cost:    2
c ---[ 220]---> BDD-cost:    2
c ---[ 219]---> BDD-cost:    2
c ---[ 218]---> BDD-cost:    2
c ---[ 217]---> BDD-cost:    2
c ---[ 216]---> BDD-cost:    2
c ---[ 215]---> BDD-cost:    4
c ---[ 214]---> BDD-cost:    2
c ---[ 213]---> BDD-cost:    2
c ---[ 212]---> BDD-cost:    2
c ---[ 211]---> BDD-cost:    2
c ---[ 210]---> BDD-cost:    2
c ---[ 209]---> BDD-cost:    2
c ---[ 208]---> BDD-cost:    2
c ---[ 207]---> BDD-cost:    3
c ---[ 206]---> BDD-cost:    2
c ---[ 205]---> BDD-cost:    2
c ---[ 204]---> BDD-cost:    2
c ---[ 203]---> BDD-cost:    2
c ---[ 202]---> BDD-cost:    2
c ---[ 201]---> BDD-cost:    2
c ---[ 200]---> BDD-cost:    2
c ---[ 191]---> BDD-cost:    2
c ---[ 190]---> BDD-cost:    2
c ---[ 189]---> BDD-cost:    2
c ---[ 188]---> BDD-cost:    2
c ---[ 187]---> BDD-cost:    2
c ---[ 186]---> BDD-cost:    2
c ---[ 185]---> BDD-cost:    2
c ---[ 184]---> BDD-cost:    2
c ---[ 183]---> BDD-cost:    2
c ---[ 182]---> BDD-cost:    2
c ---[ 181]---> BDD-cost:    2
c ---[ 180]---> BDD-cost:    2
c ---[ 179]---> BDD-cost:    2
c ---[ 178]---> BDD-cost:    2
c ---[ 177]---> BDD-cost:    2
c ---[ 176]---> BDD-cost:    2
c ---[ 175]---> BDD-cost:    2
c ---[ 174]---> BDD-cost:    2
c ---[ 173]---> BDD-cost:    2
c ---[ 172]---> BDD-cost:    2
c ---[ 171]---> BDD-cost:    2
c ---[ 170]---> BDD-cost:    2
c ---[ 169]---> BDD-cost:    2
c ---[ 168]---> BDD-cost:    2
c ---[ 167]---> BDD-cost:    2
c ---[ 166]---> BDD-cost:    2
c ---[ 165]---> BDD-cost:    2
c ---[ 164]---> BDD-cost:    2
c ---[ 163]---> BDD-cost:    2
c ---[ 162]---> BDD-cost:    2
c ---[ 161]---> BDD-cost:    2
c ---[ 160]---> BDD-cost:    2
c ---[ 159]---> BDD-cost:    2
c ---[ 158]---> BDD-cost:    2
c ---[ 157]---> BDD-cost:    2
c ---[ 156]---> BDD-cost:    2
c ---[ 155]---> BDD-cost:    2
c ---[ 154]---> BDD-cost:    2
c ---[ 153]---> BDD-cost:    2
c ---[ 152]---> BDD-cost:    2
c ---[ 151]---> BDD-cost:    2
c ---[ 150]---> BDD-cost:    2
c ---[ 149]---> BDD-cost:    2
c ---[ 148]---> BDD-cost:    2
c ---[ 147]---> BDD-cost:    2
c ---[ 146]---> BDD-cost:    2
c ---[ 145]---> BDD-cost:    2
c ---[ 144]---> BDD-cost:    2
c ---[ 143]---> BDD-cost:    2
c ---[ 142]---> BDD-cost:    2
c ---[ 141]---> BDD-cost:    2
c ---[ 140]---> BDD-cost:    2
c ---[ 139]---> BDD-cost:    2
c ---[ 138]---> BDD-cost:    2
c ---[ 137]---> BDD-cost:    2
c ---[ 136]---> BDD-cost:    2
c ---[ 127]---> BDD-cost:    2
c ---[ 126]---> BDD-cost:    2
c ---[ 125]---> BDD-cost:    2
c ---[ 124]---> BDD-cost:    2
c ---[ 123]---> BDD-cost:    2
c ---[ 122]---> BDD-cost:    2
c ---[ 121]---> BDD-cost:    2
c ---[ 120]---> BDD-cost:    2
c ---[ 119]---> BDD-cost:    2
c ---[ 118]---> BDD-cost:    2
c ---[ 117]---> BDD-cost:    2
c ---[ 116]---> BDD-cost:    2
c ---[ 115]---> BDD-cost:    2
c ---[ 114]---> BDD-cost:    2
c ---[ 113]---> BDD-cost:    2
c ---[ 112]---> BDD-cost:    2
c ---[ 111]---> BDD-cost:    2
c ---[ 110]---> BDD-cost:    2
c ---[ 109]---> BDD-cost:    2
c ---[ 108]---> BDD-cost:    2
c ---[ 107]---> BDD-cost:    2
c ---[ 106]---> BDD-cost:    2
c ---[ 105]---> BDD-cost:    2
c ---[ 104]---> BDD-cost:    2
c ---[ 103]---> BDD-cost:    2
c ---[ 102]---> BDD-cost:    2
c ---[ 101]---> BDD-cost:    2
c ---[ 100]---> BDD-cost:    2
c ---[  99]---> BDD-cost:    2
c ---[  98]---> BDD-cost:    2
c ---[  97]---> BDD-cost:    2
c ---[  96]---> BDD-cost:    2
c ---[  95]---> BDD-cost:    2
c ---[  94]---> BDD-cost:    2
c ---[  93]---> BDD-cost:    2
c ---[  92]---> BDD-cost:    2
c ---[  91]---> BDD-cost:    2
c ---[  90]---> BDD-cost:    2
c ---[  89]---> BDD-cost:    2
c ---[  88]---> BDD-cost:    2
c ---[  87]---> BDD-cost:    2
c ---[  86]---> BDD-cost:    2
c ---[  85]---> BDD-cost:    2
c ---[  84]---> BDD-cost:    2
c ---[  83]---> BDD-cost:    2
c ---[  82]---> BDD-cost:    2
c ---[  81]---> BDD-cost:    2
c ---[  80]---> BDD-cost:    2
c ---[  79]---> BDD-cost:    2
c ---[  78]---> BDD-cost:    2
c ---[  77]---> BDD-cost:    2
c ---[  76]---> BDD-cost:    2
c ---[  75]---> BDD-cost:    2
c ---[  74]---> BDD-cost:    2
c ---[  73]---> BDD-cost:    2
c ---[  72]---> BDD-cost:    2
c ---[  63]---> BDD-cost:    2
c ---[  62]---> BDD-cost:    2
c ---[  61]---> BDD-cost:    2
c ---[  60]---> BDD-cost:    2
c ---[  59]---> BDD-cost:    2
c ---[  58]---> BDD-cost:    2
c ---[  57]---> BDD-cost:    2
c ---[  56]---> BDD-cost:    2
c ---[  55]---> BDD-cost:    2
c ---[  54]---> BDD-cost:    2
c ---[  53]---> BDD-cost:    2
c ---[  52]---> BDD-cost:    2
c ---[  51]---> BDD-cost:    2
c ---[  50]---> BDD-cost:    2
c ---[  49]---> BDD-cost:    2
c ---[  48]---> BDD-cost:    2
c ---[  47]---> BDD-cost:    2
c ---[  46]---> BDD-cost:    2
c ---[  45]---> BDD-cost:    2
c ---[  44]---> BDD-cost:    2
c ---[  43]---> BDD-cost:    2
c ---[  42]---> BDD-cost:    2
c ---[  41]---> BDD-cost:    2
c ---[  40]---> BDD-cost:    2
c ---[  39]---> BDD-cost:    2
c ---[  38]---> BDD-cost:    2
c ---[  37]---> BDD-cost:    2
c ---[  36]---> BDD-cost:    2
c ---[  35]---> BDD-cost:    2
c ---[  34]---> BDD-cost:    2
c ---[  33]---> BDD-cost:    2
c ---[  32]---> BDD-cost:    2
c ---[  31]---> BDD-cost:    2
c ---[  30]---> BDD-cost:    2
c ---[  29]---> BDD-cost:    2
c ---[  28]---> BDD-cost:    2
c ---[  27]---> BDD-cost:    2
c ---[  26]---> BDD-cost:    2
c ---[  25]---> BDD-cost:    2
c ---[  24]---> BDD-cost:    2
c ---[  23]---> BDD-cost:    2
c ---[  22]---> BDD-cost:    2
c ---[  21]---> BDD-cost:    2
c ---[  20]---> BDD-cost:    2
c ---[  19]---> BDD-cost:    2
c ---[  18]---> BDD-cost:    2
c ---[  17]---> BDD-cost:    2
c ---[  16]---> BDD-cost:    2
c ---[  15]---> BDD-cost:    2
c ---[  14]---> BDD-cost:    2
c ---[  13]---> BDD-cost:    2
c ---[  12]---> BDD-cost:    2
c ---[  11]---> BDD-cost:    2
c ---[  10]---> BDD-cost:    2
c ---[   9]---> BDD-cost:    2
c ---[   8]---> BDD-cost:    2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   17376    49254 |    5792       0        0     nan |  0.000 % |
c |       100 |   17376    49254 |    6371     100     1326    13.3 | 27.023 % |
c ==============================================================================
c Found solution: 31956
c ---[   0]---> Sorter-cost:36248     Base: 5 2 2 3 5 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       147 |  112281   271036 |   37427     147     1914    13.0 | 27.023 % |
c ==============================================================================
c Found solution: 31563
c ---[   0]---> Sorter-cost:    9     Base: 5 2 2 3 5 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       176 |  113591   274375 |   37863     176     2430    13.8 | 27.023 % |
c |       277 |  113591   274375 |   41649     277     5251    19.0 |  4.757 % |
c ==============================================================================
c Found solution: 31343
c ---[   0]---> Sorter-cost:    6     Base: 5 2 2 3 5 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       382 |  113629   274546 |   37876     382     6306    16.5 |  4.757 % |
c ==============================================================================
c Found solution: 31013
c ---[   0]---> Sorter-cost:    9     Base: 5 2 2 3 5 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       387 |  113644   274619 |   37881     387     6362    16.4 |  4.757 % |
c |       487 |  113644   274619 |   41669     487     9135    18.8 |  4.758 % |
c |       637 |  113596   274511 |   45836     635    10811    17.0 |  4.787 % |
c ==============================================================================
c Found solution: 30586
c ---[   0]---> Sorter-cost:    8     Base: 5 2 2 3 5 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       675 |  113901   275318 |   37967     673    15256    22.7 |  4.787 % |
c ==============================================================================
c Found solution: 28916
c ---[   0]---> Sorter-cost:    7     Base: 5 2 2 3 5 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       739 |  113929   275393 |   37976     737    16345    22.2 |  4.787 % |
c ==============================================================================
c Found solution: 28339
c ---[   0]---> Sorter-cost:    9     Base: 5 2 2 3 5 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       811 |  114074   275750 |   38024     809    17738    21.9 |  4.787 % |
c ==============================================================================
c Found solution: 28118
c ---[   0]---> Sorter-cost:    8     Base: 5 2 2 3 5 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       869 |  114087   275872 |   38029     867    20760    23.9 |  4.787 % |
c |       969 |  114073   275840 |   41831     966    24217    25.1 |  4.772 % |
c |      1120 |  114073   275840 |   46015    1117    39019    34.9 |  4.772 % |
c |      1345 |  114073   275840 |   50616    1342    43692    32.6 |  4.772 % |
c |      1683 |  114073   275840 |   55678    1680    47677    28.4 |  4.772 % |
c |      2195 |  114073   275840 |   61246    2192    54895    25.0 |  4.772 % |
c |      2954 |  114073   275840 |   67370    2951   171086    58.0 |  4.772 % |
c ==============================================================================
c Found solution: 27817
c ---[   0]---> Sorter-cost:    7     Base: 5 2 2 3 5 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      3367 |  114212   276177 |   38070    3364   192128    57.1 |  4.772 % |
c |      3467 |  114212   276177 |   41877    3464   194840    56.2 |  4.765 % |
c |      3617 |  114212   276177 |   46064    3614   206716    57.2 |  4.765 % |
c |      3842 |  114212   276177 |   50671    3839   213401    55.6 |  4.765 % |
c |      4179 |  114212   276177 |   55738    4176   230255    55.1 |  4.765 % |
c |      4686 |  114212   276177 |   61312    4683   242856    51.9 |  4.765 % |
c |      5450 |  114212   276177 |   67443    5447   272764    50.1 |  4.765 % |
c |      6590 |  113989   275672 |   74187    6582   322347    49.0 |  4.915 % |
c |      8299 |  113989   275672 |   81606    8291   447067    53.9 |  4.915 % |
c |     10861 |  113758   275143 |   89767   10843   584131    53.9 |  5.066 % |
c ==============================================================================
c Found solution: 27813
c ---[   0]---> Sorter-cost:    5     Base: 5 2 2 3 5 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     14491 |  113191   273859 |   37730   14454   705837    48.8 |  5.066 % |
c |     14592 |  113118   273692 |   41503   14554   708940    48.7 |  5.499 % |
c |     14742 |  112774   272909 |   45653   14702   711851    48.4 |  5.717 % |
c |     14970 |  112774   272909 |   50218   14930   730505    48.9 |  5.717 % |
c |     15307 |  112774   272909 |   55240   15267   756401    49.5 |  5.717 % |
c |     15813 |  112774   272909 |   60764   15773   787871    50.0 |  5.717 % |
c ==============================================================================
c Found solution: 27795
c ---[   0]---> Sorter-cost:    5     Base: 5 2 2 3 5 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     16057 |  112800   272984 |   37600   16017   809097    50.5 |  5.717 % |
c |     16157 |  112800   272984 |   41360   16117   813107    50.5 |  5.717 % |
c ==============================================================================
c Found solution: 27501
c ---[   0]---> Sorter-cost:    8     Base: 5 2 2 3 5 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     16294 |  112808   273013 |   37602   16254   820930    50.5 |  5.717 % |
c |     16396 |  112808   273013 |   41362   16356   832545    50.9 |  5.718 % |
c |     16547 |  112744   272871 |   45498   16504   833734    50.5 |  5.764 % |
c |     16773 |  112580   272501 |   50048   16707   843676    50.5 |  5.876 % |
c |     17110 |  112580   272501 |   55053   17044   877938    51.5 |  5.876 % |
c |     17616 |  112580   272501 |   60558   17550   917907    52.3 |  5.876 % |
c |     18377 |  112580   272501 |   66614   18311   997681    54.5 |  5.876 % |
c |     19519 |  112545   272422 |   73275   19452  1030099    53.0 |  5.900 % |
c |     21228 |  112157   271542 |   80603   21144  1265877    59.9 |  6.151 % |
c |     23790 |  112109   271433 |   88663   23702  1325656    55.9 |  6.190 % |
c ==============================================================================
c Found solution: 27457
c ---[   0]---> Sorter-cost:    5     Base: 5 2 2 3 5 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     25312 |  112118   271454 |   37372   25224  1393087    55.2 |  6.190 % |
c |     25413 |  112118   271454 |   41109   25325  1396262    55.1 |  6.192 % |
c |     25565 |  112118   271454 |   45220   25477  1400766    55.0 |  6.192 % |
c |     25791 |  112118   271454 |   49742   25703  1417812    55.2 |  6.192 % |
c |     26128 |  112118   271454 |   54716   26040  1426891    54.8 |  6.192 % |
c |     26634 |  112118   271454 |   60187   26546  1439549    54.2 |  6.192 % |
c |     27393 |  112118   271454 |   66206   27305  1524061    55.8 |  6.192 % |
c |     28532 |  111938   271046 |   72827   28436  1620084    57.0 |  6.315 % |
c |     30240 |  111684   270463 |   80110   30142  1789816    59.4 |  6.499 % |
c |     32802 |  111684   270463 |   88121   32704  1914290    58.5 |  6.499 % |
c |     36646 |  111684   270463 |   96933   36548  2269361    62.1 |  6.499 % |
c ==============================================================================
c Found solution: 27360
c ---[   0]---> Sorter-cost:    9     Base: 5 2 2 3 5 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     38116 |  111697   270494 |   37232   38018  2366385    62.2 |  6.499 % |
c |     38217 |  111697   270494 |   40955   38119  2377846    62.4 |  6.500 % |
c |     38368 |  111697   270494 |   45050   38270  2384323    62.3 |  6.500 % |
c |     38593 |  111697   270494 |   49555   38495  2405792    62.5 |  6.500 % |
c |     38930 |  111697   270494 |   54511   38832  2429420    62.6 |  6.500 % |
c |     39437 |  109953   266516 |   59962   39301  2436439    62.0 |  7.736 % |
c |     40196 |  109953   266516 |   65958   40060  2571897    64.2 |  7.736 % |
c |     41335 |  109953   266516 |   72554   41199  2708593    65.7 |  7.736 % |
c ==============================================================================
c Found solution: 27257
c ---[   0]---> Sorter-cost:    6     Base: 5 2 2 3 5 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     42092 |  109961   266535 |   36653   41956  2793630    66.6 |  7.736 % |
c |     42193 |  109961   266535 |   40318   16732  1033515    61.8 |  7.738 % |
c |     42344 |  109961   266535 |   44350   16883  1042761    61.8 |  7.738 % |
c |     42570 |  109961   266535 |   48785   17109  1058246    61.9 |  7.738 % |
c |     42908 |  109961   266535 |   53663   17447  1085007    62.2 |  7.738 % |
c |     43416 |  109961   266535 |   59030   17955  1140854    63.5 |  7.738 % |
c |     44175 |  109961   266535 |   64933   18714  1171895    62.6 |  7.738 % |
c |     45316 |  109961   266535 |   71426   19855  1219126    61.4 |  7.738 % |
c |     47027 |  108578   263358 |   78568   21347  1337574    62.7 |  8.749 % |
c |     49590 |  108578   263358 |   86425   23910  1804189    75.5 |  8.749 % |
c |     53436 |  107972   261973 |   95068   27732  2316612    83.5 |  9.198 % |
c |     59204 |  106915   259561 |  104575   33279  2706898    81.3 |  9.953 % |
c |     67855 |  104663   254383 |  115032   41755  3303359    79.1 | 11.578 % |
c ==============================================================================
c Found solution: 27201
c ---[   0]---> Sorter-cost:    3     Base: 5 2 2 3 5 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     72316 |  104667   254392 |   34889   46216  3745394    81.0 | 11.578 % |
c |     72417 |  104667   254392 |   38377   18616   964264    51.8 | 11.580 % |
c |     72567 |  104667   254392 |   42215   18766   968857    51.6 | 11.580 % |
c |     72792 |  104667   254392 |   46437   18991   976186    51.4 | 11.580 % |
c |     73130 |  104667   254392 |   51080   19329   987298    51.1 | 11.580 % |
c |     73637 |  104667   254392 |   56189   19836  1004080    50.6 | 11.580 % |
c |     74398 |  104667   254392 |   61807   20597  1062430    51.6 | 11.580 % |
c |     75537 |  104667   254392 |   67988   21736  1110020    51.1 | 11.580 % |
c |     77246 |  104667   254392 |   74787   23445  1156496    49.3 | 11.580 % |
c ==============================================================================
c Found solution: 26793
c ---[   0]---> Sorter-cost:    5     Base: 5 2 2 3 5 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     77295 |  104678   254423 |   34892   23494  1161038    49.4 | 11.580 % |
c |     77395 |  104414   253816 |   38381   23586  1162616    49.3 | 11.786 % |
c |     77545 |  104414   253816 |   42219   23736  1166062    49.1 | 11.786 % |
c |     77770 |  104414   253816 |   46441   23961  1184154    49.4 | 11.786 % |
c |     78109 |  104414   253816 |   51085   24300  1191266    49.0 | 11.786 % |
c |     78615 |  104414   253816 |   56193   24806  1203274    48.5 | 11.786 % |
c |     79374 |  104414   253816 |   61813   25565  1260624    49.3 | 11.786 % |
c |     80515 |  104414   253816 |   67994   26706  1379561    51.7 | 11.786 % |
c |     82225 |  104414   253816 |   74794   28416  1486335    52.3 | 11.786 % |
c |     84789 |  104303   253562 |   82273   30430  1604311    52.7 | 11.883 % |
c ==============================================================================
c Found solution: 26443
c ---[   0]---> Sorter-cost:    7     Base: 5 2 2 3 5 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     88501 |  104313   253585 |   34771   34142  1877163    55.0 | 11.883 % |
c |     88601 |  104313   253585 |   38248   34242  1881540    54.9 | 11.884 % |
c |     88752 |  104313   253585 |   42072   34393  1899019    55.2 | 11.884 % |
c |     88978 |  104313   253585 |   46280   34619  1915760    55.3 | 11.884 % |
c |     89315 |  104120   253139 |   50908   34918  1920410    55.0 | 12.031 % |
c |     89822 |  104076   253043 |   55999   35420  1977425    55.8 | 12.072 % |
c |     90582 |  104076   253043 |   61598   36180  2032359    56.2 | 12.072 % |
c |     91722 |  104076   253043 |   67758   37320  2142490    57.4 | 12.072 % |
c |     93432 |  104076   253043 |   74534   39030  2221665    56.9 | 12.072 % |
c |     95995 |  104076   253043 |   81988   41593  2714177    65.3 | 12.072 % |
c |     99840 |  103852   252527 |   90187   45433  2925008    64.4 | 12.234 % |
c |    105606 |  102236   248798 |   99205   51130  3306514    64.7 | 13.455 % |
c |    114257 |  101251   246513 |  109126   59672  3654481    61.2 | 14.215 % |
c ==============================================================================
c Found solution: 26442
c ---[   0]---> Sorter-cost:    9     Base: 5 2 2 3 5 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    122777 |  101262   246540 |   33754   68192  4590117    67.3 | 14.215 % |
c |    122877 |  101262   246540 |   37129   22956  1167913    50.9 | 14.215 % |
c |    123027 |  101262   246540 |   40842   23106  1175108    50.9 | 14.215 % |
c |    123253 |  101262   246540 |   44926   23332  1184804    50.8 | 14.215 % |
c |    123590 |  101262   246540 |   49419   23669  1207074    51.0 | 14.215 % |
c |    124096 |  101262   246540 |   54361   24175  1259017    52.1 | 14.215 % |
c |    124859 |  101262   246540 |   59797   24938  1364639    54.7 | 14.215 % |
c |    126000 |  101262   246540 |   65776   26079  1414687    54.2 | 14.215 % |
c |    127708 |  101262   246540 |   72354   27787  1547195    55.7 | 14.215 % |
c |    130270 |  101262   246540 |   79590   30349  1854960    61.1 | 14.215 % |
c |    134116 |  100870   245638 |   87549   34177  2194864    64.2 | 14.495 % |
c |    139883 |  100870   245638 |   96304   39944  2475013    62.0 | 14.495 % |
c |    148532 |  100870   245638 |  105934   48593  3332642    68.6 | 14.495 % |
c |    161506 |  100870   245638 |  116527   61567  4104866    66.7 | 14.495 % |

Watcher Data

Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing Stack size limit: 67108864 bytes
Enforcing memory limit (will send SIGTERM then SIGKILL): 921600 Kb
Enforcing VSIZE limit: 994918400 bytes
Current StackSize limit: 67108864 bytes
Raw data (/proc/16692/stat): 16692 (minisat+_script) R 16691 16692 9102 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1843280597 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 1 0 0
Raw data (/proc/16692/statm): 174 3 169 147 0 27 0
[pid=16692] vsize: 696
open syscall for file /etc/ld.so.preload
open syscall for file tls/i686/mmx/libtermcap.so.2
open syscall for file tls/i686/libtermcap.so.2
open syscall for file tls/mmx/libtermcap.so.2
open syscall for file tls/libtermcap.so.2
open syscall for file i686/mmx/libtermcap.so.2
open syscall for file i686/libtermcap.so.2
open syscall for file mmx/libtermcap.so.2
open syscall for file libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/tls/i686/mmx/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/tls/i686/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/tls/mmx/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/tls/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/i686/mmx/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/i686/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/mmx/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/libtermcap.so.2
open syscall for file /etc/ld.so.cache
open syscall for file /lib/libtermcap.so.2
open syscall for file tls/i686/mmx/libdl.so.2
open syscall for file tls/i686/libdl.so.2
open syscall for file tls/mmx/libdl.so.2
open syscall for file tls/libdl.so.2
open syscall for file i686/mmx/libdl.so.2
open syscall for file i686/libdl.so.2
open syscall for file mmx/libdl.so.2
open syscall for file libdl.so.2
open syscall for file /oldhome/oroussel/lib/libdl.so.2
open syscall for file /lib/libdl.so.2
open syscall for file tls/i686/mmx/libc.so.6
open syscall for file tls/i686/libc.so.6
open syscall for file tls/mmx/libc.so.6
open syscall for file tls/libc.so.6
open syscall for file i686/mmx/libc.so.6
open syscall for file i686/libc.so.6
open syscall for file mmx/libc.so.6
open syscall for file libc.so.6
open syscall for file /oldhome/oroussel/lib/libc.so.6
open syscall for file /lib/tls/libc.so.6
open syscall for file /dev/tty
open syscall for file /etc/mtab
open syscall for file /proc/meminfo
open syscall for file /oldhome/oroussel/solvers/minisat+_script
New process pid=16693
New process pid=16694
New process pid=16695
execve syscall for /bin/sed executable
One traced child (pid=16694) exited with status: 0
open syscall for file /etc/ld.so.preload
open syscall for file tls/i686/mmx/libc.so.6
open syscall for file tls/i686/libc.so.6
open syscall for file tls/mmx/libc.so.6
open syscall for file tls/libc.so.6
open syscall for file i686/mmx/libc.so.6
open syscall for file i686/libc.so.6
open syscall for file mmx/libc.so.6
open syscall for file libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/i686/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/i686/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/libc.so.6
open syscall for file /oldhome/oroussel/lib/i686/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/i686/libc.so.6
open syscall for file /oldhome/oroussel/lib/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/libc.so.6
open syscall for file /etc/ld.so.cache
open syscall for file /lib/tls/libc.so.6
One traced child (pid=16695) exited with status: 0
One traced child (pid=16693) exited with status: 0
New process pid=16696
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc31/normalized-data6_3.opb

[startup+10.0039 s]
Raw data (loadavg): 0.92 0.95 0.98 2/58 16696
Raw data (/proc/16692/stat): 16692 (minisat+_script) S 16691 16692 9102 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843280597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16692/statm): 531 226 485 147 0 384 0
[pid=16692] vsize: 2124
Raw data (/proc/16696/stat): 16696 (minisat+_64-bit) R 16692 16692 9102 0 -1 0 4316 0 0 0 965 15 0 0 25 0 1 0 1843280602 17182720 3636 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16696/statm): 4195 3636 145 145 0 4050 0
[pid=16696] vsize: 16780
Current children cumulated CPU time (s) 9.81
Current children cumulated vsize (Kb) 18904

[startup+20.0058 s]
Raw data (loadavg): 0.93 0.95 0.98 2/58 16696
Raw data (/proc/16692/stat): 16692 (minisat+_script) S 16691 16692 9102 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843280597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16692/statm): 531 226 485 147 0 384 0
[pid=16692] vsize: 2124
Raw data (/proc/16696/stat): 16696 (minisat+_64-bit) R 16692 16692 9102 0 -1 0 4365 0 0 0 1963 16 0 0 25 0 1 0 1843280602 17371136 3685 4294967295 134512640 135094434 3221224448 3221223136 134554748 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16696/statm): 4241 3685 145 145 0 4096 0
[pid=16696] vsize: 16964
Current children cumulated CPU time (s) 19.8
Current children cumulated vsize (Kb) 19088

[startup+30.0077 s]
Raw data (loadavg): 0.94 0.95 0.98 2/58 16696
Raw data (/proc/16692/stat): 16692 (minisat+_script) S 16691 16692 9102 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843280597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16692/statm): 531 226 485 147 0 384 0
[pid=16692] vsize: 2124
Raw data (/proc/16696/stat): 16696 (minisat+_64-bit) R 16692 16692 9102 0 -1 0 4595 0 0 0 2961 17 0 0 25 0 1 0 1843280602 17854464 3803 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16696/statm): 4359 3803 145 145 0 4214 0
[pid=16696] vsize: 17436
Current children cumulated CPU time (s) 29.79
Current children cumulated vsize (Kb) 19560

[startup+40.0087 s]
Raw data (loadavg): 0.95 0.96 0.98 2/58 16696
Raw data (/proc/16692/stat): 16692 (minisat+_script) S 16691 16692 9102 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843280597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16692/statm): 531 226 485 147 0 384 0
[pid=16692] vsize: 2124
Raw data (/proc/16696/stat): 16696 (minisat+_64-bit) R 16692 16692 9102 0 -1 0 4729 0 0 0 3957 19 0 0 25 0 1 0 1843280602 18407424 3937 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16696/statm): 4494 3937 145 145 0 4349 0
[pid=16696] vsize: 17976
Current children cumulated CPU time (s) 39.77
Current children cumulated vsize (Kb) 20100

[startup+50.0106 s]
Raw data (loadavg): 0.96 0.96 0.98 2/58 16696
Raw data (/proc/16692/stat): 16692 (minisat+_script) S 16691 16692 9102 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843280597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16692/statm): 531 226 485 147 0 384 0
[pid=16692] vsize: 2124
Raw data (/proc/16696/stat): 16696 (minisat+_64-bit) R 16692 16692 9102 0 -1 0 4833 0 0 0 4956 20 0 0 25 0 1 0 1843280602 18825216 4041 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16696/statm): 4596 4041 145 145 0 4451 0
[pid=16696] vsize: 18384
Current children cumulated CPU time (s) 49.77
Current children cumulated vsize (Kb) 20508

[startup+60.0115 s]
Raw data (loadavg): 0.96 0.96 0.98 2/58 16698
Raw data (/proc/16692/stat): 16692 (minisat+_script) S 16691 16692 9102 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843280597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16692/statm): 531 226 485 147 0 384 0
[pid=16692] vsize: 2124
Raw data (/proc/16696/stat): 16696 (minisat+_64-bit) R 16692 16692 9102 0 -1 0 4949 0 0 0 5954 21 0 0 25 0 1 0 1843280602 19316736 4157 4294967295 134512640 135094434 3221224448 3221223104 134557893 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16696/statm): 4716 4157 145 145 0 4571 0
[pid=16696] vsize: 18864
Current children cumulated CPU time (s) 59.76
Current children cumulated vsize (Kb) 20988

[startup+70.0135 s]
Raw data (loadavg): 0.97 0.96 0.98 2/58 16698
Raw data (/proc/16692/stat): 16692 (minisat+_script) S 16691 16692 9102 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843280597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16692/statm): 531 226 485 147 0 384 0
[pid=16692] vsize: 2124
Raw data (/proc/16696/stat): 16696 (minisat+_64-bit) R 16692 16692 9102 0 -1 0 5093 0 0 0 6951 22 0 0 25 0 1 0 1843280602 19947520 4301 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16696/statm): 4870 4301 145 145 0 4725 0
[pid=16696] vsize: 19480
Current children cumulated CPU time (s) 69.74
Current children cumulated vsize (Kb) 21604

[startup+80.0154 s]
Raw data (loadavg): 0.97 0.96 0.98 2/58 16698
Raw data (/proc/16692/stat): 16692 (minisat+_script) S 16691 16692 9102 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843280597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16692/statm): 531 226 485 147 0 384 0
[pid=16692] vsize: 2124
Raw data (/proc/16696/stat): 16696 (minisat+_64-bit) R 16692 16692 9102 0 -1 0 5332 0 0 0 7947 23 0 0 25 0 1 0 1843280602 20463616 4429 4294967295 134512640 135094434 3221224448 3221223084 134557560 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16696/statm): 4996 4429 145 145 0 4851 0
[pid=16696] vsize: 19984
Current children cumulated CPU time (s) 79.71
Current children cumulated vsize (Kb) 22108

[startup+90.0163 s]
Raw data (loadavg): 0.98 0.96 0.98 2/58 16698
Raw data (/proc/16692/stat): 16692 (minisat+_script) S 16691 16692 9102 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843280597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16692/statm): 531 226 485 147 0 384 0
[pid=16692] vsize: 2124
Raw data (/proc/16696/stat): 16696 (minisat+_64-bit) R 16692 16692 9102 0 -1 0 5654 0 0 0 8945 25 0 0 25 0 1 0 1843280602 20865024 4528 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16696/statm): 5094 4528 145 145 0 4949 0
[pid=16696] vsize: 20376
Current children cumulated CPU time (s) 89.71
Current children cumulated vsize (Kb) 22500

[startup+100.017 s]
Raw data (loadavg): 0.98 0.96 0.98 2/58 16698
Raw data (/proc/16692/stat): 16692 (minisat+_script) S 16691 16692 9102 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843280597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16692/statm): 531 226 485 147 0 384 0
[pid=16692] vsize: 2124
Raw data (/proc/16696/stat): 16696 (minisat+_64-bit) R 16692 16692 9102 0 -1 0 5760 0 0 0 9944 25 0 0 25 0 1 0 1843280602 21356544 4634 4294967295 134512640 135094434 3221224448 3221223104 134558398 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16696/statm): 5214 4634 145 145 0 5069 0
[pid=16696] vsize: 20856
Current children cumulated CPU time (s) 99.7
Current children cumulated vsize (Kb) 22980

[startup+110.018 s]
Raw data (loadavg): 0.98 0.96 0.98 2/58 16698
Raw data (/proc/16692/stat): 16692 (minisat+_script) S 16691 16692 9102 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843280597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16692/statm): 531 226 485 147 0 384 0
[pid=16692] vsize: 2124
Raw data (/proc/16696/stat): 16696 (minisat+_64-bit) R 16692 16692 9102 0 -1 0 5877 0 0 0 10942 26 0 0 25 0 1 0 1843280602 21827584 4751 4294967295 134512640 135094434 3221224448 3221223136 134554731 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16696/statm): 5329 4751 145 145 0 5184 0
[pid=16696] vsize: 21316
Current children cumulated CPU time (s) 109.69
Current children cumulated vsize (Kb) 23440

[startup+120.02 s]
Raw data (loadavg): 0.98 0.96 0.98 2/58 16700
Raw data (/proc/16692/stat): 16692 (minisat+_script) S 16691 16692 9102 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843280597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16692/statm): 531 226 485 147 0 384 0
[pid=16692] vsize: 2124
Raw data (/proc/16696/stat): 16696 (minisat+_64-bit) T 16692 16692 9102 0 -1 0 6146 0 0 0 11938 27 0 0 25 0 1 0 1843280602 22921216 5020 4294967295 134512640 135094434 3221224448 3221222796 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/16696/statm): 5596 5020 145 145 0 5451 0
[pid=16696] vsize: 22384
Current children cumulated CPU time (s) 119.66
Current children cumulated vsize (Kb) 24508

[startup+130.021 s]
Raw data (loadavg): 0.99 0.96 0.98 2/58 16700
Raw data (/proc/16692/stat): 16692 (minisat+_script) S 16691 16692 9102 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843280597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16692/statm): 531 226 485 147 0 384 0
[pid=16692] vsize: 2124
Raw data (/proc/16696/stat): 16696 (minisat+_64-bit) R 16692 16692 9102 0 -1 0 6212 0 0 0 12937 28 0 0 25 0 1 0 1843280602 23183360 5086 4294967295 134512640 135094434 3221224448 3221223060 134563049 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16696/statm): 5660 5086 145 145 0 5515 0
[pid=16696] vsize: 22640
Current children cumulated CPU time (s) 129.66
Current children cumulated vsize (Kb) 24764

[startup+140.021 s]
Raw data (loadavg): 0.99 0.97 0.98 2/58 16700
Raw data (/proc/16692/stat): 16692 (minisat+_script) S 16691 16692 9102 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843280597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16692/statm): 531 226 485 147 0 384 0
[pid=16692] vsize: 2124
Raw data (/proc/16696/stat): 16696 (minisat+_64-bit) R 16692 16692 9102 0 -1 0 6440 0 0 0 13935 29 0 0 25 0 1 0 1843280602 23654400 5203 4294967295 134512640 135094434 3221224448 3221223072 134557596 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16696/statm): 5775 5203 145 145 0 5630 0
[pid=16696] vsize: 23100
Current children cumulated CPU time (s) 139.65
Current children cumulated vsize (Kb) 25224

[startup+150.023 s]
Raw data (loadavg): 0.99 0.97 0.98 2/58 16700
Raw data (/proc/16692/stat): 16692 (minisat+_script) S 16691 16692 9102 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843280597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16692/statm): 531 226 485 147 0 384 0
[pid=16692] vsize: 2124
Raw data (/proc/16696/stat): 16696 (minisat+_64-bit) R 16692 16692 9102 0 -1 0 6548 0 0 0 14934 29 0 0 25 0 1 0 1843280602 24092672 5311 4294967295 134512640 135094434 3221224448 3221223108 134553497 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16696/statm): 5882 5311 145 145 0 5737 0
[pid=16696] vsize: 23528
Current children cumulated CPU time (s) 149.64
Current children cumulated vsize (Kb) 25652

[startup+160.024 s]
Raw data (loadavg): 0.99 0.97 0.98 2/58 16700
Raw data (/proc/16692/stat): 16692 (minisat+_script) S 16691 16692 9102 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843280597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16692/statm): 531 226 485 147 0 384 0
[pid=16692] vsize: 2124
Raw data (/proc/16696/stat): 16696 (minisat+_64-bit) R 16692 16692 9102 0 -1 0 6660 0 0 0 15933 30 0 0 25 0 1 0 1843280602 24543232 5423 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16696/statm): 5992 5423 145 145 0 5847 0
[pid=16696] vsize: 23968
Current children cumulated CPU time (s) 159.64
Current children cumulated vsize (Kb) 26092

[startup+170.025 s]
Raw data (loadavg): 0.99 0.97 0.98 2/58 16700
Raw data (/proc/16692/stat): 16692 (minisat+_script) S 16691 16692 9102 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843280597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16692/statm): 531 226 485 147 0 384 0
[pid=16692] vsize: 2124
Raw data (/proc/16696/stat): 16696 (minisat+_64-bit) R 16692 16692 9102 0 -1 0 6767 0 0 0 16933 30 0 0 25 0 1 0 1843280602 24977408 5530 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16696/statm): 6098 5530 145 145 0 5953 0
[pid=16696] vsize: 24392
Current children cumulated CPU time (s) 169.64
Current children cumulated vsize (Kb) 26516

[startup+180.026 s]
Raw data (loadavg): 0.99 0.97 0.98 2/58 16702
Raw data (/proc/16692/stat): 16692 (minisat+_script) S 16691 16692 9102 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843280597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16692/statm): 531 226 485 147 0 384 0
[pid=16692] vsize: 2124
Raw data (/proc/16696/stat): 16696 (minisat+_64-bit) R 16692 16692 9102 0 -1 0 6861 0 0 0 17931 31 0 0 25 0 1 0 1843280602 25358336 5624 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16696/statm): 6191 5624 145 145 0 6046 0
[pid=16696] vsize: 24764
Current children cumulated CPU time (s) 179.63
Current children cumulated vsize (Kb) 26888

[startup+190.027 s]
Raw data (loadavg): 0.99 0.97 0.98 2/58 16702
Raw data (/proc/16692/stat): 16692 (minisat+_script) S 16691 16692 9102 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843280597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16692/statm): 531 226 485 147 0 384 0
[pid=16692] vsize: 2124
Raw data (/proc/16696/stat): 16696 (minisat+_64-bit) R 16692 16692 9102 0 -1 0 6939 0 0 0 18929 31 0 0 25 0 1 0 1843280602 25673728 5702 4294967295 134512640 135094434 3221224448 3221223136 134554731 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16696/statm): 6268 5702 145 145 0 6123 0
[pid=16696] vsize: 25072
Current children cumulated CPU time (s) 189.61
Current children cumulated vsize (Kb) 27196

[startup+200.028 s]
Raw data (loadavg): 0.99 0.97 0.98 2/58 16702
Raw data (/proc/16692/stat): 16692 (minisat+_script) S 16691 16692 9102 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843280597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16692/statm): 531 226 485 147 0 384 0
[pid=16692] vsize: 2124
Raw data (/proc/16696/stat): 16696 (minisat+_64-bit) R 16692 16692 9102 0 -1 0 7039 0 0 0 19929 32 0 0 25 0 1 0 1843280602 26210304 5802 4294967295 134512640 135094434 3221224448 3221223136 134554731 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16696/statm): 6399 5802 145 145 0 6254 0
[pid=16696] vsize: 25596
Current children cumulated CPU time (s) 199.62
Current children cumulated vsize (Kb) 27720

[startup+210.028 s]
Raw data (loadavg): 0.99 0.97 0.98 2/58 16702
Raw data (/proc/16692/stat): 16692 (minisat+_script) S 16691 16692 9102 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843280597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16692/statm): 531 226 485 147 0 384 0
[pid=16692] vsize: 2124
Raw data (/proc/16696/stat): 16696 (minisat+_64-bit) R 16692 16692 9102 0 -1 0 7147 0 0 0 20927 32 0 0 25 0 1 0 1843280602 26644480 5910 4294967295 134512640 135094434 3221224448 3221223120 134556266 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16696/statm): 6505 5910 145 145 0 6360 0
[pid=16696] vsize: 26020
Current children cumulated CPU time (s) 209.6
Current children cumulated vsize (Kb) 28144

[startup+220.03 s]
Raw data (loadavg): 0.99 0.97 0.98 2/58 16702
Raw data (/proc/16692/stat): 16692 (minisat+_script) S 16691 16692 9102 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843280597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16692/statm): 531 226 485 147 0 384 0
[pid=16692] vsize: 2124
Raw data (/proc/16696/stat): 16696 (minisat+_64-bit) R 16692 16692 9102 0 -1 0 7290 0 0 0 21926 33 0 0 25 0 1 0 1843280602 27226112 6053 4294967295 134512640 135094434 3221224448 3221223040 134557180 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16696/statm): 6647 6053 145 145 0 6502 0
[pid=16696] vsize: 26588
Current children cumulated CPU time (s) 219.6
Current children cumulated vsize (Kb) 28712

[startup+230.031 s]
Raw data (loadavg): 0.99 0.97 0.98 2/58 16702
Raw data (/proc/16692/stat): 16692 (minisat+_script) S 16691 16692 9102 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843280597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16692/statm): 531 226 485 147 0 384 0
[pid=16692] vsize: 2124
Raw data (/proc/16696/stat): 16696 (minisat+_64-bit) R 16692 16692 9102 0 -1 0 7390 0 0 0 22925 34 0 0 25 0 1 0 1843280602 27631616 6153 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16696/statm): 6746 6153 145 145 0 6601 0
[pid=16696] vsize: 26984
Current children cumulated CPU time (s) 229.6
Current children cumulated vsize (Kb) 29108

[startup+240.032 s]
Raw data (loadavg): 0.99 0.97 0.98 2/58 16704
Raw data (/proc/16692/stat): 16692 (minisat+_script) S 16691 16692 9102 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843280597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16692/statm): 531 226 485 147 0 384 0
[pid=16692] vsize: 2124
Raw data (/proc/16696/stat): 16696 (minisat+_64-bit) R 16692 16692 9102 0 -1 0 7604 0 0 0 23923 35 0 0 25 0 1 0 1843280602 28049408 6256 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16696/statm): 6848 6256 145 145 0 6703 0
[pid=16696] vsize: 27392
Current children cumulated CPU time (s) 239.59
Current children cumulated vsize (Kb) 29516

[startup+250.033 s]
Raw data (loadavg): 0.99 0.97 0.98 2/58 16704
Raw data (/proc/16692/stat): 16692 (minisat+_script) S 16691 16692 9102 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843280597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16692/statm): 531 226 485 147 0 384 0
[pid=16692] vsize: 2124
Raw data (/proc/16696/stat): 16696 (minisat+_64-bit) R 16692 16692 9102 0 -1 0 7692 0 0 0 24922 35 0 0 25 0 1 0 1843280602 28405760 6344 4294967295 134512640 135094434 3221224448 3221223084 134557639 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16696/statm): 6935 6344 145 145 0 6790 0
[pid=16696] vsize: 27740
Current children cumulated CPU time (s) 249.58
Current children cumulated vsize (Kb) 29864

[startup+260.034 s]
Raw data (loadavg): 0.99 0.97 0.98 2/58 16704
Raw data (/proc/16692/stat): 16692 (minisat+_script) S 16691 16692 9102 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843280597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16692/statm): 531 226 485 147 0 384 0
[pid=16692] vsize: 2124
Raw data (/proc/16696/stat): 16696 (minisat+_64-bit) R 16692 16692 9102 0 -1 0 7832 0 0 0 25920 36 0 0 25 0 1 0 1843280602 28975104 6484 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16696/statm): 7074 6484 145 145 0 6929 0
[pid=16696] vsize: 28296
Current children cumulated CPU time (s) 259.57
Current children cumulated vsize (Kb) 30420

[startup+270.036 s]
Raw data (loadavg): 0.99 0.97 0.98 2/58 16704
Raw data (/proc/16692/stat): 16692 (minisat+_script) S 16691 16692 9102 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843280597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16692/statm): 531 226 485 147 0 384 0
[pid=16692] vsize: 2124
Raw data (/proc/16696/stat): 16696 (minisat+_64-bit) R 16692 16692 9102 0 -1 0 7959 0 0 0 26919 36 0 0 25 0 1 0 1843280602 29491200 6611 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16696/statm): 7200 6611 145 145 0 7055 0
[pid=16696] vsize: 28800
Current children cumulated CPU time (s) 269.56
Current children cumulated vsize (Kb) 30924

[startup+280.037 s]
Raw data (loadavg): 0.99 0.97 0.98 2/58 16704
Raw data (/proc/16692/stat): 16692 (minisat+_script) S 16691 16692 9102 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843280597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16692/statm): 531 226 485 147 0 384 0
[pid=16692] vsize: 2124
Raw data (/proc/16696/stat): 16696 (minisat+_64-bit) R 16692 16692 9102 0 -1 0 8056 0 0 0 27919 37 0 0 25 0 1 0 1843280602 29892608 6708 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16696/statm): 7298 6708 145 145 0 7153 0
[pid=16696] vsize: 29192
Current children cumulated CPU time (s) 279.57
Current children cumulated vsize (Kb) 31316

[startup+290.038 s]
Raw data (loadavg): 0.99 0.97 0.98 2/58 16704
Raw data (/proc/16692/stat): 16692 (minisat+_script) S 16691 16692 9102 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843280597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16692/statm): 531 226 485 147 0 384 0
[pid=16692] vsize: 2124
Raw data (/proc/16696/stat): 16696 (minisat+_64-bit) R 16692 16692 9102 0 -1 0 8178 0 0 0 28918 37 0 0 25 0 1 0 1843280602 29933568 6719 4294967295 134512640 135094434 3221224448 3221223120 134556252 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16696/statm): 7308 6719 145 145 0 7163 0
[pid=16696] vsize: 29232
Current children cumulated CPU time (s) 289.56
Current children cumulated vsize (Kb) 31356

[startup+300.039 s]
Raw data (loadavg): 0.99 0.97 0.98 2/58 16706
Raw data (/proc/16692/stat): 16692 (minisat+_script) S 16691 16692 9102 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843280597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16692/statm): 531 226 485 147 0 384 0
[pid=16692] vsize: 2124
Raw data (/proc/16696/stat): 16696 (minisat+_64-bit) R 16692 16692 9102 0 -1 0 8178 0 0 0 29918 37 0 0 25 0 1 0 1843280602 29933568 6719 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16696/statm): 7308 6719 145 145 0 7163 0
[pid=16696] vsize: 29232
Current children cumulated CPU time (s) 299.56
Current children cumulated vsize (Kb) 31356

[startup+310.04 s]
Raw data (loadavg): 0.99 0.97 0.98 2/58 16706
Raw data (/proc/16692/stat): 16692 (minisat+_script) S 16691 16692 9102 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843280597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16692/statm): 531 226 485 147 0 384 0
[pid=16692] vsize: 2124
Raw data (/proc/16696/stat): 16696 (minisat+_64-bit) R 16692 16692 9102 0 -1 0 8178 0 0 0 30918 37 0 0 25 0 1 0 1843280602 29933568 6719 4294967295 134512640 135094434 3221224448 3221223104 134557846 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16696/statm): 7308 6719 145 145 0 7163 0
[pid=16696] vsize: 29232
Current children cumulated CPU time (s) 309.56
Current children cumulated vsize (Kb) 31356

[startup+320.041 s]
Raw data (loadavg): 0.99 0.97 0.98 2/58 16706
Raw data (/proc/16692/stat): 16692 (minisat+_script) S 16691 16692 9102 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843280597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16692/statm): 531 226 485 147 0 384 0
[pid=16692] vsize: 2124
Raw data (/proc/16696/stat): 16696 (minisat+_64-bit) R 16692 16692 9102 0 -1 0 8178 0 0 0 31918 37 0 0 25 0 1 0 1843280602 29933568 6719 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16696/statm): 7308 6719 145 145 0 7163 0
[pid=16696] vsize: 29232
Current children cumulated CPU time (s) 319.56
Current children cumulated vsize (Kb) 31356

[startup+330.043 s]
Raw data (loadavg): 0.99 0.97 0.98 2/58 16706
Raw data (/proc/16692/stat): 16692 (minisat+_script) S 16691 16692 9102 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843280597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16692/statm): 531 226 485 147 0 384 0
[pid=16692] vsize: 2124
Raw data (/proc/16696/stat): 16696 (minisat+_64-bit) R 16692 16692 9102 0 -1 0 8178 0 0 0 32919 37 0 0 25 0 1 0 1843280602 29933568 6719 4294967295 134512640 135094434 3221224448 3221223108 134553528 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16696/statm): 7308 6719 145 145 0 7163 0
[pid=16696] vsize: 29232
Current children cumulated CPU time (s) 329.57
Current children cumulated vsize (Kb) 31356

[startup+340.044 s]
Raw data (loadavg): 0.99 0.97 0.98 2/58 16706
Raw data (/proc/16692/stat): 16692 (minisat+_script) S 16691 16692 9102 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843280597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16692/statm): 531 226 485 147 0 384 0
[pid=16692] vsize: 2124
Raw data (/proc/16696/stat): 16696 (minisat+_64-bit) R 16692 16692 9102 0 -1 0 8178 0 0 0 33919 37 0 0 25 0 1 0 1843280602 29933568 6719 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16696/statm): 7308 6719 145 145 0 7163 0
[pid=16696] vsize: 29232
Current children cumulated CPU time (s) 339.57
Current children cumulated vsize (Kb) 31356

[startup+350.045 s]
Raw data (loadavg): 0.99 0.97 0.98 2/58 16706
Raw data (/proc/16692/stat): 16692 (minisat+_script) S 16691 16692 9102 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843280597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16692/statm): 531 226 485 147 0 384 0
[pid=16692] vsize: 2124
Raw data (/proc/16696/stat): 16696 (minisat+_64-bit) R 16692 16692 9102 0 -1 0 8178 0 0 0 34919 37 0 0 25 0 1 0 1843280602 29933568 6719 4294967295 134512640 135094434 3221224448 3221223120 134556499 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16696/statm): 7308 6719 145 145 0 7163 0
[pid=16696] vsize: 29232
Current children cumulated CPU time (s) 349.57
Current children cumulated vsize (Kb) 31356

[startup+360.045 s]
Raw data (loadavg): 0.99 0.97 0.98 2/58 16708
Raw data (/proc/16692/stat): 16692 (minisat+_script) S 16691 16692 9102 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843280597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16692/statm): 531 226 485 147 0 384 0
[pid=16692] vsize: 2124
Raw data (/proc/16696/stat): 16696 (minisat+_64-bit) R 16692 16692 9102 0 -1 0 8178 0 0 0 35919 37 0 0 25 0 1 0 1843280602 29933568 6719 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16696/statm): 7308 6719 145 145 0 7163 0
[pid=16696] vsize: 29232
Current children cumulated CPU time (s) 359.57
Current children cumulated vsize (Kb) 31356

[startup+370.046 s]
Raw data (loadavg): 0.99 0.97 0.98 2/58 16708
Raw data (/proc/16692/stat): 16692 (minisat+_script) S 16691 16692 9102 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843280597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16692/statm): 531 226 485 147 0 384 0
[pid=16692] vsize: 2124
Raw data (/proc/16696/stat): 16696 (minisat+_64-bit) R 16692 16692 9102 0 -1 0 8178 0 0 0 36919 37 0 0 25 0 1 0 1843280602 29933568 6719 4294967295 134512640 135094434 3221224448 3221223104 134557846 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16696/statm): 7308 6719 145 145 0 7163 0
[pid=16696] vsize: 29232
Current children cumulated CPU time (s) 369.57
Current children cumulated vsize (Kb) 31356

[startup+380.047 s]
Raw data (loadavg): 0.99 0.97 0.98 2/58 16708
Raw data (/proc/16692/stat): 16692 (minisat+_script) S 16691 16692 9102 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843280597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16692/statm): 531 226 485 147 0 384 0
[pid=16692] vsize: 2124
Raw data (/proc/16696/stat): 16696 (minisat+_64-bit) R 16692 16692 9102 0 -1 0 8178 0 0 0 37920 37 0 0 25 0 1 0 1843280602 29933568 6719 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16696/statm): 7308 6719 145 145 0 7163 0
[pid=16696] vsize: 29232
Current children cumulated CPU time (s) 379.58
Current children cumulated vsize (Kb) 31356

[startup+390.048 s]
Raw data (loadavg): 0.99 0.97 0.98 2/58 16708
Raw data (/proc/16692/stat): 16692 (minisat+_script) S 16691 16692 9102 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843280597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16692/statm): 531 226 485 147 0 384 0
[pid=16692] vsize: 2124
Raw data (/proc/16696/stat): 16696 (minisat+_64-bit) R 16692 16692 9102 0 -1 0 8178 0 0 0 38920 37 0 0 25 0 1 0 1843280602 29933568 6719 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16696/statm): 7308 6719 145 145 0 7163 0
[pid=16696] vsize: 29232
Current children cumulated CPU time (s) 389.58
Current children cumulated vsize (Kb) 31356

[startup+400.05 s]
Raw data (loadavg): 0.99 0.97 0.98 2/58 16708
Raw data (/proc/16692/stat): 16692 (minisat+_script) S 16691 16692 9102 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843280597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16692/statm): 531 226 485 147 0 384 0
[pid=16692] vsize: 2124
Raw data (/proc/16696/stat): 16696 (minisat+_64-bit) R 16692 16692 9102 0 -1 0 8204 0 0 0 39920 38 0 0 25 0 1 0 1843280602 30040064 6745 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16696/statm): 7334 6745 145 145 0 7189 0
[pid=16696] vsize: 29336
Current children cumulated CPU time (s) 399.59
Current children cumulated vsize (Kb) 31460

[startup+410.051 s]
Raw data (loadavg): 0.99 0.97 0.98 2/58 16708
Raw data (/proc/16692/stat): 16692 (minisat+_script) S 16691 16692 9102 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843280597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16692/statm): 531 226 485 147 0 384 0
[pid=16692] vsize: 2124
Raw data (/proc/16696/stat): 16696 (minisat+_64-bit) R 16692 16692 9102 0 -1 0 8297 0 0 0 40917 39 0 0 25 0 1 0 1843280602 30420992 6838 4294967295 134512640 135094434 3221224448 3221223040 134556964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16696/statm): 7427 6838 145 145 0 7282 0
[pid=16696] vsize: 29708
Current children cumulated CPU time (s) 409.57
Current children cumulated vsize (Kb) 31832

[startup+420.052 s]
Raw data (loadavg): 0.99 0.97 0.98 2/58 16710
Raw data (/proc/16692/stat): 16692 (minisat+_script) S 16691 16692 9102 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843280597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16692/statm): 531 226 485 147 0 384 0
[pid=16692] vsize: 2124
Raw data (/proc/16696/stat): 16696 (minisat+_64-bit) R 16692 16692 9102 0 -1 0 8418 0 0 0 41916 39 0 0 25 0 1 0 1843280602 30920704 6959 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16696/statm): 7549 6959 145 145 0 7404 0
[pid=16696] vsize: 30196
Current children cumulated CPU time (s) 419.56
Current children cumulated vsize (Kb) 32320

[startup+430.053 s]
Raw data (loadavg): 0.99 0.97 0.98 2/58 16710
Raw data (/proc/16692/stat): 16692 (minisat+_script) S 16691 16692 9102 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843280597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16692/statm): 531 226 485 147 0 384 0
[pid=16692] vsize: 2124
Raw data (/proc/16696/stat): 16696 (minisat+_64-bit) R 16692 16692 9102 0 -1 0 8502 0 0 0 42915 40 0 0 25 0 1 0 1843280602 31260672 7043 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16696/statm): 7632 7043 145 145 0 7487 0
[pid=16696] vsize: 30528
Current children cumulated CPU time (s) 429.56
Current children cumulated vsize (Kb) 32652

[startup+440.053 s]
Raw data (loadavg): 0.99 0.97 0.98 2/58 16710
Raw data (/proc/16692/stat): 16692 (minisat+_script) S 16691 16692 9102 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843280597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16692/statm): 531 226 485 147 0 384 0
[pid=16692] vsize: 2124
Raw data (/proc/16696/stat): 16696 (minisat+_64-bit) R 16692 16692 9102 0 -1 0 8590 0 0 0 43913 41 0 0 25 0 1 0 1843280602 31621120 7131 4294967295 134512640 135094434 3221224448 3221223072 134557596 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16696/statm): 7720 7131 145 145 0 7575 0
[pid=16696] vsize: 30880
Current children cumulated CPU time (s) 439.55
Current children cumulated vsize (Kb) 33004

[startup+450.054 s]
Raw data (loadavg): 0.99 0.97 0.98 2/58 16710
Raw data (/proc/16692/stat): 16692 (minisat+_script) S 16691 16692 9102 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843280597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16692/statm): 531 226 485 147 0 384 0
[pid=16692] vsize: 2124
Raw data (/proc/16696/stat): 16696 (minisat+_64-bit) R 16692 16692 9102 0 -1 0 8686 0 0 0 44912 41 0 0 25 0 1 0 1843280602 32014336 7227 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16696/statm): 7816 7227 145 145 0 7671 0
[pid=16696] vsize: 31264
Current children cumulated CPU time (s) 449.54
Current children cumulated vsize (Kb) 33388

[startup+460.055 s]
Raw data (loadavg): 0.99 0.97 0.98 2/58 16710
Raw data (/proc/16692/stat): 16692 (minisat+_script) S 16691 16692 9102 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843280597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16692/statm): 531 226 485 147 0 384 0
[pid=16692] vsize: 2124
Raw data (/proc/16696/stat): 16696 (minisat+_64-bit) R 16692 16692 9102 0 -1 0 8772 0 0 0 45911 42 0 0 25 0 1 0 1843280602 32362496 7313 4294967295 134512640 135094434 3221224448 3221223100 134558255 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16696/statm): 7901 7313 145 145 0 7756 0
[pid=16696] vsize: 31604
Current children cumulated CPU time (s) 459.54
Current children cumulated vsize (Kb) 33728

[startup+470.057 s]
Raw data (loadavg): 0.99 0.97 0.98 2/58 16710
Raw data (/proc/16692/stat): 16692 (minisat+_script) S 16691 16692 9102 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843280597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16692/statm): 531 226 485 147 0 384 0
[pid=16692] vsize: 2124
Raw data (/proc/16696/stat): 16696 (minisat+_64-bit) R 16692 16692 9102 0 -1 0 8879 0 0 0 46910 43 0 0 25 0 1 0 1843280602 32796672 7420 4294967295 134512640 135094434 3221224448 3221223072 134557596 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16696/statm): 8007 7420 145 145 0 7862 0
[pid=16696] vsize: 32028
Current children cumulated CPU time (s) 469.54
Current children cumulated vsize (Kb) 34152

[startup+480.058 s]
Raw data (loadavg): 0.99 0.97 0.98 2/58 16712
Raw data (/proc/16692/stat): 16692 (minisat+_script) S 16691 16692 9102 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843280597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16692/statm): 531 226 485 147 0 384 0
[pid=16692] vsize: 2124
Raw data (/proc/16696/stat): 16696 (minisat+_64-bit) R 16692 16692 9102 0 -1 0 8976 0 0 0 47908 43 0 0 25 0 1 0 1843280602 33189888 7517 4294967295 134512640 135094434 3221224448 3221223104 134557866 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16696/statm): 8103 7517 145 145 0 7958 0
[pid=16696] vsize: 32412
Current children cumulated CPU time (s) 479.52
Current children cumulated vsize (Kb) 34536

[startup+490.058 s]
Raw data (loadavg): 0.99 0.97 0.98 2/58 16712
Raw data (/proc/16692/stat): 16692 (minisat+_script) S 16691 16692 9102 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843280597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16692/statm): 531 226 485 147 0 384 0
[pid=16692] vsize: 2124
Raw data (/proc/16696/stat): 16696 (minisat+_64-bit) R 16692 16692 9102 0 -1 0 9069 0 0 0 48908 44 0 0 25 0 1 0 1843280602 33566720 7610 4294967295 134512640 135094434 3221224448 3221223120 134555252 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16696/statm): 8195 7610 145 145 0 8050 0
[pid=16696] vsize: 32780
Current children cumulated CPU time (s) 489.53
Current children cumulated vsize (Kb) 34904

[startup+500.059 s]
Raw data (loadavg): 0.99 0.97 0.98 2/58 16712
Raw data (/proc/16692/stat): 16692 (minisat+_script) S 16691 16692 9102 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843280597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16692/statm): 531 226 485 147 0 384 0
[pid=16692] vsize: 2124
Raw data (/proc/16696/stat): 16696 (minisat+_64-bit) R 16692 16692 9102 0 -1 0 9164 0 0 0 49906 44 0 0 25 0 1 0 1843280602 33955840 7705 4294967295 134512640 135094434 3221224448 3221223104 134557849 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16696/statm): 8290 7705 145 145 0 8145 0
[pid=16696] vsize: 33160
Current children cumulated CPU time (s) 499.51
Current children cumulated vsize (Kb) 35284

[startup+510.06 s]
Raw data (loadavg): 0.99 0.97 0.98 2/58 16712
Raw data (/proc/16692/stat): 16692 (minisat+_script) S 16691 16692 9102 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843280597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16692/statm): 531 226 485 147 0 384 0
[pid=16692] vsize: 2124
Raw data (/proc/16696/stat): 16696 (minisat+_64-bit) R 16692 16692 9102 0 -1 0 9317 0 0 0 50905 45 0 0 25 0 1 0 1843280602 34123776 7747 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16696/statm): 8331 7747 145 145 0 8186 0
[pid=16696] vsize: 33324
Current children cumulated CPU time (s) 509.51
Current children cumulated vsize (Kb) 35448

[startup+520.062 s]
Raw data (loadavg): 0.99 0.97 0.98 2/58 16712
Raw data (/proc/16692/stat): 16692 (minisat+_script) S 16691 16692 9102 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843280597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16692/statm): 531 226 485 147 0 384 0
[pid=16692] vsize: 2124
Raw data (/proc/16696/stat): 16696 (minisat+_64-bit) R 16692 16692 9102 0 -1 0 9317 0 0 0 51905 45 0 0 25 0 1 0 1843280602 34123776 7747 4294967295 134512640 135094434 3221224448 3221223072 134557650 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16696/statm): 8331 7747 145 145 0 8186 0
[pid=16696] vsize: 33324
Current children cumulated CPU time (s) 519.51
Current children cumulated vsize (Kb) 35448

[startup+530.063 s]
Raw data (loadavg): 0.99 0.97 0.98 2/58 16712
Raw data (/proc/16692/stat): 16692 (minisat+_script) S 16691 16692 9102 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843280597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16692/statm): 531 226 485 147 0 384 0
[pid=16692] vsize: 2124
Raw data (/proc/16696/stat): 16696 (minisat+_64-bit) R 16692 16692 9102 0 -1 0 9317 0 0 0 52905 45 0 0 25 0 1 0 1843280602 34123776 7747 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16696/statm): 8331 7747 145 145 0 8186 0
[pid=16696] vsize: 33324
Current children cumulated CPU time (s) 529.51
Current children cumulated vsize (Kb) 35448

[startup+540.064 s]
Raw data (loadavg): 0.99 0.97 0.98 2/58 16714
Raw data (/proc/16692/stat): 16692 (minisat+_script) S 16691 16692 9102 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843280597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16692/statm): 531 226 485 147 0 384 0
[pid=16692] vsize: 2124
Raw data (/proc/16696/stat): 16696 (minisat+_64-bit) R 16692 16692 9102 0 -1 0 9325 0 0 0 53906 45 0 0 25 0 1 0 1843280602 34156544 7755 4294967295 134512640 135094434 3221224448 3221223104 134558405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16696/statm): 8339 7755 145 145 0 8194 0
[pid=16696] vsize: 33356
Current children cumulated CPU time (s) 539.52
Current children cumulated vsize (Kb) 35480

[startup+550.065 s]
Raw data (loadavg): 0.99 0.97 0.98 2/58 16714
Raw data (/proc/16692/stat): 16692 (minisat+_script) S 16691 16692 9102 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843280597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16692/statm): 531 226 485 147 0 384 0
[pid=16692] vsize: 2124
Raw data (/proc/16696/stat): 16696 (minisat+_64-bit) R 16692 16692 9102 0 -1 0 9325 0 0 0 54906 45 0 0 25 0 1 0 1843280602 34156544 7755 4294967295 134512640 135094434 3221224448 3221223104 134557860 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16696/statm): 8339 7755 145 145 0 8194 0
[pid=16696] vsize: 33356
Current children cumulated CPU time (s) 549.52
Current children cumulated vsize (Kb) 35480

[startup+560.066 s]
Raw data (loadavg): 0.99 0.97 0.98 2/58 16714
Raw data (/proc/16692/stat): 16692 (minisat+_script) S 16691 16692 9102 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843280597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16692/statm): 531 226 485 147 0 384 0
[pid=16692] vsize: 2124
Raw data (/proc/16696/stat): 16696 (minisat+_64-bit) R 16692 16692 9102 0 -1 0 9325 0 0 0 55906 45 0 0 25 0 1 0 1843280602 34156544 7755 4294967295 134512640 135094434 3221224448 3221223072 134557596 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16696/statm): 8339 7755 145 145 0 8194 0
[pid=16696] vsize: 33356
Current children cumulated CPU time (s) 559.52
Current children cumulated vsize (Kb) 35480

[startup+570.068 s]
Raw data (loadavg): 0.99 0.97 0.98 2/58 16714
Raw data (/proc/16692/stat): 16692 (minisat+_script) S 16691 16692 9102 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843280597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16692/statm): 531 226 485 147 0 384 0
[pid=16692] vsize: 2124
Raw data (/proc/16696/stat): 16696 (minisat+_64-bit) R 16692 16692 9102 0 -1 0 9325 0 0 0 56906 45 0 0 25 0 1 0 1843280602 34156544 7755 4294967295 134512640 135094434 3221224448 3221223040 134556826 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16696/statm): 8339 7755 145 145 0 8194 0
[pid=16696] vsize: 33356
Current children cumulated CPU time (s) 569.52
Current children cumulated vsize (Kb) 35480

[startup+580.069 s]
Raw data (loadavg): 0.99 0.97 0.98 2/58 16714
Raw data (/proc/16692/stat): 16692 (minisat+_script) S 16691 16692 9102 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843280597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16692/statm): 531 226 485 147 0 384 0
[pid=16692] vsize: 2124
Raw data (/proc/16696/stat): 16696 (minisat+_64-bit) R 16692 16692 9102 0 -1 0 9325 0 0 0 57907 45 0 0 25 0 1 0 1843280602 34156544 7755 4294967295 134512640 135094434 3221224448 3221223104 134558221 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16696/statm): 8339 7755 145 145 0 8194 0
[pid=16696] vsize: 33356
Current children cumulated CPU time (s) 579.53
Current children cumulated vsize (Kb) 35480

[startup+590.07 s]
Raw data (loadavg): 0.99 0.97 0.98 2/58 16714
Raw data (/proc/16692/stat): 16692 (minisat+_script) S 16691 16692 9102 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843280597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16692/statm): 531 226 485 147 0 384 0
[pid=16692] vsize: 2124
Raw data (/proc/16696/stat): 16696 (minisat+_64-bit) R 16692 16692 9102 0 -1 0 9325 0 0 0 58907 45 0 0 25 0 1 0 1843280602 34156544 7755 4294967295 134512640 135094434 3221224448 3221223104 134557815 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16696/statm): 8339 7755 145 145 0 8194 0
[pid=16696] vsize: 33356
Current children cumulated CPU time (s) 589.53
Current children cumulated vsize (Kb) 35480

[startup+600.071 s]
Raw data (loadavg): 0.99 0.97 0.98 2/58 16716
Raw data (/proc/16692/stat): 16692 (minisat+_script) S 16691 16692 9102 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843280597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16692/statm): 531 226 485 147 0 384 0
[pid=16692] vsize: 2124
Raw data (/proc/16696/stat): 16696 (minisat+_64-bit) R 16692 16692 9102 0 -1 0 9325 0 0 0 59907 45 0 0 25 0 1 0 1843280602 34156544 7755 4294967295 134512640 135094434 3221224448 3221223120 134555566 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16696/statm): 8339 7755 145 145 0 8194 0
[pid=16696] vsize: 33356
Current children cumulated CPU time (s) 599.53
Current children cumulated vsize (Kb) 35480

[startup+610.072 s]
Raw data (loadavg): 0.99 0.97 0.98 2/58 16716
Raw data (/proc/16692/stat): 16692 (minisat+_script) S 16691 16692 9102 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843280597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16692/statm): 531 226 485 147 0 384 0
[pid=16692] vsize: 2124
Raw data (/proc/16696/stat): 16696 (minisat+_64-bit) R 16692 16692 9102 0 -1 0 9377 0 0 0 60907 45 0 0 25 0 1 0 1843280602 34197504 7765 4294967295 134512640 135094434 3221224448 3221223040 134556851 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16696/statm): 8349 7765 145 145 0 8204 0
[pid=16696] vsize: 33396
Current children cumulated CPU time (s) 609.53
Current children cumulated vsize (Kb) 35520

[startup+620.073 s]
Raw data (loadavg): 0.99 0.97 0.98 2/58 16716
Raw data (/proc/16692/stat): 16692 (minisat+_script) S 16691 16692 9102 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843280597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16692/statm): 531 226 485 147 0 384 0
[pid=16692] vsize: 2124
Raw data (/proc/16696/stat): 16696 (minisat+_64-bit) R 16692 16692 9102 0 -1 0 9377 0 0 0 61907 45 0 0 25 0 1 0 1843280602 34197504 7765 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16696/statm): 8349 7765 145 145 0 8204 0
[pid=16696] vsize: 33396
Current children cumulated CPU time (s) 619.53
Current children cumulated vsize (Kb) 35520

[startup+630.073 s]
Raw data (loadavg): 0.99 0.97 0.98 2/58 16716
Raw data (/proc/16692/stat): 16692 (minisat+_script) S 16691 16692 9102 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843280597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16692/statm): 531 226 485 147 0 384 0
[pid=16692] vsize: 2124
Raw data (/proc/16696/stat): 16696 (minisat+_64-bit) R 16692 16692 9102 0 -1 0 9377 0 0 0 62908 45 0 0 25 0 1 0 1843280602 34197504 7765 4294967295 134512640 135094434 3221224448 3221223072 134557596 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16696/statm): 8349 7765 145 145 0 8204 0
[pid=16696] vsize: 33396
Current children cumulated CPU time (s) 629.54
Current children cumulated vsize (Kb) 35520

[startup+640.074 s]
Raw data (loadavg): 0.99 0.97 0.98 2/58 16716
Raw data (/proc/16692/stat): 16692 (minisat+_script) S 16691 16692 9102 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843280597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16692/statm): 531 226 485 147 0 384 0
[pid=16692] vsize: 2124
Raw data (/proc/16696/stat): 16696 (minisat+_64-bit) R 16692 16692 9102 0 -1 0 9377 0 0 0 63908 45 0 0 25 0 1 0 1843280602 34197504 7765 4294967295 134512640 135094434 3221224448 3221223072 134557574 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16696/statm): 8349 7765 145 145 0 8204 0
[pid=16696] vsize: 33396
Current children cumulated CPU time (s) 639.54
Current children cumulated vsize (Kb) 35520

[startup+650.075 s]
Raw data (loadavg): 0.99 0.97 0.98 2/58 16716
Raw data (/proc/16692/stat): 16692 (minisat+_script) S 16691 16692 9102 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843280597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16692/statm): 531 226 485 147 0 384 0
[pid=16692] vsize: 2124
Raw data (/proc/16696/stat): 16696 (minisat+_64-bit) R 16692 16692 9102 0 -1 0 9377 0 0 0 64908 45 0 0 25 0 1 0 1843280602 34197504 7765 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16696/statm): 8349 7765 145 145 0 8204 0
[pid=16696] vsize: 33396
Current children cumulated CPU time (s) 649.54
Current children cumulated vsize (Kb) 35520

[startup+660.076 s]
Raw data (loadavg): 0.99 0.97 0.98 2/58 16718
Raw data (/proc/16692/stat): 16692 (minisat+_script) S 16691 16692 9102 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843280597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16692/statm): 531 226 485 147 0 384 0
[pid=16692] vsize: 2124
Raw data (/proc/16696/stat): 16696 (minisat+_64-bit) R 16692 16692 9102 0 -1 0 9377 0 0 0 65908 45 0 0 25 0 1 0 1843280602 34197504 7765 4294967295 134512640 135094434 3221224448 3221223120 134556242 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16696/statm): 8349 7765 145 145 0 8204 0
[pid=16696] vsize: 33396
Current children cumulated CPU time (s) 659.54
Current children cumulated vsize (Kb) 35520

[startup+670.077 s]
Raw data (loadavg): 0.99 0.97 0.98 2/58 16718
Raw data (/proc/16692/stat): 16692 (minisat+_script) S 16691 16692 9102 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843280597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16692/statm): 531 226 485 147 0 384 0
[pid=16692] vsize: 2124
Raw data (/proc/16696/stat): 16696 (minisat+_64-bit) R 16692 16692 9102 0 -1 0 9377 0 0 0 66909 45 0 0 25 0 1 0 1843280602 34197504 7765 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16696/statm): 8349 7765 145 145 0 8204 0
[pid=16696] vsize: 33396
Current children cumulated CPU time (s) 669.55
Current children cumulated vsize (Kb) 35520

[startup+680.078 s]
Raw data (loadavg): 0.99 0.97 0.98 2/58 16718
Raw data (/proc/16692/stat): 16692 (minisat+_script) S 16691 16692 9102 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843280597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16692/statm): 531 226 485 147 0 384 0
[pid=16692] vsize: 2124
Raw data (/proc/16696/stat): 16696 (minisat+_64-bit) R 16692 16692 9102 0 -1 0 9377 0 0 0 67909 45 0 0 25 0 1 0 1843280602 34197504 7765 4294967295 134512640 135094434 3221224448 3221223072 134562104 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16696/statm): 8349 7765 145 145 0 8204 0
[pid=16696] vsize: 33396
Current children cumulated CPU time (s) 679.55
Current children cumulated vsize (Kb) 35520

[startup+690.079 s]
Raw data (loadavg): 0.99 0.97 0.98 2/58 16718
Raw data (/proc/16692/stat): 16692 (minisat+_script) S 16691 16692 9102 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843280597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16692/statm): 531 226 485 147 0 384 0
[pid=16692] vsize: 2124
Raw data (/proc/16696/stat): 16696 (minisat+_64-bit) R 16692 16692 9102 0 -1 0 9379 0 0 0 68909 45 0 0 25 0 1 0 1843280602 34197504 7767 4294967295 134512640 135094434 3221224448 3221223104 134558007 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16696/statm): 8349 7767 145 145 0 8204 0
[pid=16696] vsize: 33396
Current children cumulated CPU time (s) 689.55
Current children cumulated vsize (Kb) 35520

[startup+700.08 s]
Raw data (loadavg): 0.99 0.97 0.98 2/58 16718
Raw data (/proc/16692/stat): 16692 (minisat+_script) S 16691 16692 9102 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843280597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16692/statm): 531 226 485 147 0 384 0
[pid=16692] vsize: 2124
Raw data (/proc/16696/stat): 16696 (minisat+_64-bit) R 16692 16692 9102 0 -1 0 9380 0 0 0 69909 45 0 0 25 0 1 0 1843280602 34197504 7768 4294967295 134512640 135094434 3221224448 3221223104 134557875 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16696/statm): 8349 7768 145 145 0 8204 0
[pid=16696] vsize: 33396
Current children cumulated CPU time (s) 699.55
Current children cumulated vsize (Kb) 35520

[startup+710.081 s]
Raw data (loadavg): 0.99 0.97 0.98 2/58 16718
Raw data (/proc/16692/stat): 16692 (minisat+_script) S 16691 16692 9102 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843280597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16692/statm): 531 226 485 147 0 384 0
[pid=16692] vsize: 2124
Raw data (/proc/16696/stat): 16696 (minisat+_64-bit) R 16692 16692 9102 0 -1 0 9381 0 0 0 70910 45 0 0 25 0 1 0 1843280602 34197504 7769 4294967295 134512640 135094434 3221224448 3221223108 134553444 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16696/statm): 8349 7769 145 145 0 8204 0
[pid=16696] vsize: 33396
Current children cumulated CPU time (s) 709.56
Current children cumulated vsize (Kb) 35520

[startup+720.083 s]
Raw data (loadavg): 0.99 0.97 0.98 2/58 16720
Raw data (/proc/16692/stat): 16692 (minisat+_script) S 16691 16692 9102 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843280597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16692/statm): 531 226 485 147 0 384 0
[pid=16692] vsize: 2124
Raw data (/proc/16696/stat): 16696 (minisat+_64-bit) R 16692 16692 9102 0 -1 0 9384 0 0 0 71910 45 0 0 25 0 1 0 1843280602 34197504 7772 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16696/statm): 8349 7772 145 145 0 8204 0
[pid=16696] vsize: 33396
Current children cumulated CPU time (s) 719.56
Current children cumulated vsize (Kb) 35520

[startup+730.084 s]
Raw data (loadavg): 0.99 0.97 0.98 2/58 16720
Raw data (/proc/16692/stat): 16692 (minisat+_script) S 16691 16692 9102 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843280597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16692/statm): 531 226 485 147 0 384 0
[pid=16692] vsize: 2124
Raw data (/proc/16696/stat): 16696 (minisat+_64-bit) R 16692 16692 9102 0 -1 0 9386 0 0 0 72910 45 0 0 25 0 1 0 1843280602 34197504 7774 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16696/statm): 8349 7774 145 145 0 8204 0
[pid=16696] vsize: 33396
Current children cumulated CPU time (s) 729.56
Current children cumulated vsize (Kb) 35520

[startup+740.084 s]
Raw data (loadavg): 0.99 0.97 0.98 2/58 16720
Raw data (/proc/16692/stat): 16692 (minisat+_script) S 16691 16692 9102 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843280597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16692/statm): 531 226 485 147 0 384 0
[pid=16692] vsize: 2124
Raw data (/proc/16696/stat): 16696 (minisat+_64-bit) R 16692 16692 9102 0 -1 0 9388 0 0 0 73910 45 0 0 25 0 1 0 1843280602 34197504 7776 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16696/statm): 8349 7776 145 145 0 8204 0
[pid=16696] vsize: 33396
Current children cumulated CPU time (s) 739.56
Current children cumulated vsize (Kb) 35520

[startup+750.086 s]
Raw data (loadavg): 0.99 0.97 0.98 2/58 16720
Raw data (/proc/16692/stat): 16692 (minisat+_script) S 16691 16692 9102 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843280597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16692/statm): 531 226 485 147 0 384 0
[pid=16692] vsize: 2124
Raw data (/proc/16696/stat): 16696 (minisat+_64-bit) R 16692 16692 9102 0 -1 0 9389 0 0 0 74910 46 0 0 25 0 1 0 1843280602 34197504 7777 4294967295 134512640 135094434 3221224448 3221223040 134556964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16696/statm): 8349 7777 145 145 0 8204 0
[pid=16696] vsize: 33396
Current children cumulated CPU time (s) 749.57
Current children cumulated vsize (Kb) 35520

[startup+760.087 s]
Raw data (loadavg): 0.99 0.97 0.98 2/58 16720
Raw data (/proc/16692/stat): 16692 (minisat+_script) S 16691 16692 9102 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843280597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16692/statm): 531 226 485 147 0 384 0
[pid=16692] vsize: 2124
Raw data (/proc/16696/stat): 16696 (minisat+_64-bit) R 16692 16692 9102 0 -1 0 9504 0 0 0 75909 46 0 0 25 0 1 0 1843280602 34668544 7892 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16696/statm): 8464 7892 145 145 0 8319 0
[pid=16696] vsize: 33856
Current children cumulated CPU time (s) 759.56
Current children cumulated vsize (Kb) 35980

[startup+770.088 s]
Raw data (loadavg): 0.99 0.97 0.98 2/58 16720
Raw data (/proc/16692/stat): 16692 (minisat+_script) S 16691 16692 9102 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843280597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16692/statm): 531 226 485 147 0 384 0
[pid=16692] vsize: 2124
Raw data (/proc/16696/stat): 16696 (minisat+_64-bit) R 16692 16692 9102 0 -1 0 9620 0 0 0 76907 47 0 0 25 0 1 0 1843280602 35135488 8008 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16696/statm): 8578 8008 145 145 0 8433 0
[pid=16696] vsize: 34312
Current children cumulated CPU time (s) 769.55
Current children cumulated vsize (Kb) 36436

[startup+780.09 s]
Raw data (loadavg): 0.99 0.97 0.98 2/58 16722
Raw data (/proc/16692/stat): 16692 (minisat+_script) S 16691 16692 9102 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843280597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16692/statm): 531 226 485 147 0 384 0
[pid=16692] vsize: 2124
Raw data (/proc/16696/stat): 16696 (minisat+_64-bit) R 16692 16692 9102 0 -1 0 9705 0 0 0 77907 47 0 0 25 0 1 0 1843280602 35479552 8093 4294967295 134512640 135094434 3221224448 3221223104 134558426 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16696/statm): 8662 8093 145 145 0 8517 0
[pid=16696] vsize: 34648
Current children cumulated CPU time (s) 779.55
Current children cumulated vsize (Kb) 36772

[startup+790.089 s]
Raw data (loadavg): 0.99 0.97 0.98 2/58 16722
Raw data (/proc/16692/stat): 16692 (minisat+_script) S 16691 16692 9102 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843280597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16692/statm): 531 226 485 147 0 384 0
[pid=16692] vsize: 2124
Raw data (/proc/16696/stat): 16696 (minisat+_64-bit) R 16692 16692 9102 0 -1 0 9809 0 0 0 78906 48 0 0 25 0 1 0 1843280602 35901440 8197 4294967295 134512640 135094434 3221224448 3221223072 134562155 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16696/statm): 8765 8197 145 145 0 8620 0
[pid=16696] vsize: 35060
Current children cumulated CPU time (s) 789.55
Current children cumulated vsize (Kb) 37184

[startup+800.09 s]
Raw data (loadavg): 0.99 0.97 0.98 2/58 16722
Raw data (/proc/16692/stat): 16692 (minisat+_script) S 16691 16692 9102 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843280597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16692/statm): 531 226 485 147 0 384 0
[pid=16692] vsize: 2124
Raw data (/proc/16696/stat): 16696 (minisat+_64-bit) R 16692 16692 9102 0 -1 0 9908 0 0 0 79905 49 0 0 25 0 1 0 1843280602 36302848 8296 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16696/statm): 8863 8296 145 145 0 8718 0
[pid=16696] vsize: 35452
Current children cumulated CPU time (s) 799.55
Current children cumulated vsize (Kb) 37576

[startup+810.091 s]
Raw data (loadavg): 0.99 0.97 0.98 2/58 16722
Raw data (/proc/16692/stat): 16692 (minisat+_script) S 16691 16692 9102 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843280597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16692/statm): 531 226 485 147 0 384 0
[pid=16692] vsize: 2124
Raw data (/proc/16696/stat): 16696 (minisat+_64-bit) R 16692 16692 9102 0 -1 0 10015 0 0 0 80903 50 0 0 25 0 1 0 1843280602 36737024 8403 4294967295 134512640 135094434 3221224448 3221223120 134556517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16696/statm): 8969 8403 145 145 0 8824 0
[pid=16696] vsize: 35876
Current children cumulated CPU time (s) 809.54
Current children cumulated vsize (Kb) 38000

[startup+820.093 s]
Raw data (loadavg): 0.99 0.97 0.98 2/58 16722
Raw data (/proc/16692/stat): 16692 (minisat+_script) S 16691 16692 9102 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843280597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16692/statm): 531 226 485 147 0 384 0
[pid=16692] vsize: 2124
Raw data (/proc/16696/stat): 16696 (minisat+_64-bit) R 16692 16692 9102 0 -1 0 10106 0 0 0 81902 50 0 0 25 0 1 0 1843280602 37367808 8494 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16696/statm): 9123 8494 145 145 0 8978 0
[pid=16696] vsize: 36492
Current children cumulated CPU time (s) 819.53
Current children cumulated vsize (Kb) 38616

[startup+830.094 s]
Raw data (loadavg): 0.99 0.97 0.98 2/58 16722
Raw data (/proc/16692/stat): 16692 (minisat+_script) S 16691 16692 9102 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843280597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16692/statm): 531 226 485 147 0 384 0
[pid=16692] vsize: 2124
Raw data (/proc/16696/stat): 16696 (minisat+_64-bit) R 16692 16692 9102 0 -1 0 10213 0 0 0 82902 51 0 0 25 0 1 0 1843280602 37801984 8601 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16696/statm): 9229 8601 145 145 0 9084 0
[pid=16696] vsize: 36916
Current children cumulated CPU time (s) 829.54
Current children cumulated vsize (Kb) 39040

[startup+840.095 s]
Raw data (loadavg): 0.99 0.97 0.98 2/58 16724
Raw data (/proc/16692/stat): 16692 (minisat+_script) S 16691 16692 9102 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843280597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16692/statm): 531 226 485 147 0 384 0
[pid=16692] vsize: 2124
Raw data (/proc/16696/stat): 16696 (minisat+_64-bit) R 16692 16692 9102 0 -1 0 10332 0 0 0 83901 52 0 0 25 0 1 0 1843280602 38285312 8720 4294967295 134512640 135094434 3221224448 3221223072 134562101 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16696/statm): 9347 8720 145 145 0 9202 0
[pid=16696] vsize: 37388
Current children cumulated CPU time (s) 839.54
Current children cumulated vsize (Kb) 39512

[startup+850.096 s]
Raw data (loadavg): 0.99 0.97 0.98 2/58 16724
Raw data (/proc/16692/stat): 16692 (minisat+_script) S 16691 16692 9102 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843280597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16692/statm): 531 226 485 147 0 384 0
[pid=16692] vsize: 2124
Raw data (/proc/16696/stat): 16696 (minisat+_64-bit) R 16692 16692 9102 0 -1 0 10529 0 0 0 84899 53 0 0 25 0 1 0 1843280602 38637568 8806 4294967295 134512640 135094434 3221224448 3221223096 134558258 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16696/statm): 9433 8806 145 145 0 9288 0
[pid=16696] vsize: 37732
Current children cumulated CPU time (s) 849.53
Current children cumulated vsize (Kb) 39856

[startup+860.097 s]
Raw data (loadavg): 0.99 0.97 0.98 2/58 16724
Raw data (/proc/16692/stat): 16692 (minisat+_script) S 16691 16692 9102 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843280597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16692/statm): 531 226 485 147 0 384 0
[pid=16692] vsize: 2124
Raw data (/proc/16696/stat): 16696 (minisat+_64-bit) R 16692 16692 9102 0 -1 0 10529 0 0 0 85899 53 0 0 25 0 1 0 1843280602 38637568 8806 4294967295 134512640 135094434 3221224448 3221223120 134556410 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16696/statm): 9433 8806 145 145 0 9288 0
[pid=16696] vsize: 37732
Current children cumulated CPU time (s) 859.53
Current children cumulated vsize (Kb) 39856

[startup+870.099 s]
Raw data (loadavg): 0.99 0.97 0.98 2/58 16724
Raw data (/proc/16692/stat): 16692 (minisat+_script) S 16691 16692 9102 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843280597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16692/statm): 531 226 485 147 0 384 0
[pid=16692] vsize: 2124
Raw data (/proc/16696/stat): 16696 (minisat+_64-bit) R 16692 16692 9102 0 -1 0 10529 0 0 0 86899 53 0 0 25 0 1 0 1843280602 38637568 8806 4294967295 134512640 135094434 3221224448 3221223104 134557875 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16696/statm): 9433 8806 145 145 0 9288 0
[pid=16696] vsize: 37732
Current children cumulated CPU time (s) 869.53
Current children cumulated vsize (Kb) 39856

[startup+880.1 s]
Raw data (loadavg): 0.99 0.97 0.98 2/58 16724
Raw data (/proc/16692/stat): 16692 (minisat+_script) S 16691 16692 9102 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843280597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16692/statm): 531 226 485 147 0 384 0
[pid=16692] vsize: 2124
Raw data (/proc/16696/stat): 16696 (minisat+_64-bit) R 16692 16692 9102 0 -1 0 10529 0 0 0 87900 53 0 0 25 0 1 0 1843280602 38637568 8806 4294967295 134512640 135094434 3221224448 3221223104 134557948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16696/statm): 9433 8806 145 145 0 9288 0
[pid=16696] vsize: 37732
Current children cumulated CPU time (s) 879.54
Current children cumulated vsize (Kb) 39856

[startup+890.101 s]
Raw data (loadavg): 0.99 0.97 0.98 2/58 16724
Raw data (/proc/16692/stat): 16692 (minisat+_script) S 16691 16692 9102 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843280597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16692/statm): 531 226 485 147 0 384 0
[pid=16692] vsize: 2124
Raw data (/proc/16696/stat): 16696 (minisat+_64-bit) R 16692 16692 9102 0 -1 0 10529 0 0 0 88900 53 0 0 25 0 1 0 1843280602 38637568 8806 4294967295 134512640 135094434 3221224448 3221223120 134555574 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16696/statm): 9433 8806 145 145 0 9288 0
[pid=16696] vsize: 37732
Current children cumulated CPU time (s) 889.54
Current children cumulated vsize (Kb) 39856

[startup+900.102 s]
Raw data (loadavg): 0.99 0.97 0.98 2/58 16726
Raw data (/proc/16692/stat): 16692 (minisat+_script) S 16691 16692 9102 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843280597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16692/statm): 531 226 485 147 0 384 0
[pid=16692] vsize: 2124
Raw data (/proc/16696/stat): 16696 (minisat+_64-bit) R 16692 16692 9102 0 -1 0 10529 0 0 0 89900 53 0 0 25 0 1 0 1843280602 38637568 8806 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16696/statm): 9433 8806 145 145 0 9288 0
[pid=16696] vsize: 37732
Current children cumulated CPU time (s) 899.54
Current children cumulated vsize (Kb) 39856

[startup+910.103 s]
Raw data (loadavg): 0.99 0.97 0.98 2/58 16726
Raw data (/proc/16692/stat): 16692 (minisat+_script) S 16691 16692 9102 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843280597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16692/statm): 531 226 485 147 0 384 0
[pid=16692] vsize: 2124
Raw data (/proc/16696/stat): 16696 (minisat+_64-bit) R 16692 16692 9102 0 -1 0 10529 0 0 0 90900 53 0 0 25 0 1 0 1843280602 38637568 8806 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16696/statm): 9433 8806 145 145 0 9288 0
[pid=16696] vsize: 37732
Current children cumulated CPU time (s) 909.54
Current children cumulated vsize (Kb) 39856

[startup+920.105 s]
Raw data (loadavg): 0.99 0.97 0.98 2/58 16726
Raw data (/proc/16692/stat): 16692 (minisat+_script) S 16691 16692 9102 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843280597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16692/statm): 531 226 485 147 0 384 0
[pid=16692] vsize: 2124
Raw data (/proc/16696/stat): 16696 (minisat+_64-bit) R 16692 16692 9102 0 -1 0 10529 0 0 0 91901 53 0 0 25 0 1 0 1843280602 38637568 8806 4294967295 134512640 135094434 3221224448 3221223104 134557987 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16696/statm): 9433 8806 145 145 0 9288 0
[pid=16696] vsize: 37732
Current children cumulated CPU time (s) 919.55
Current children cumulated vsize (Kb) 39856

[startup+930.106 s]
Raw data (loadavg): 0.99 0.97 0.98 2/58 16726
Raw data (/proc/16692/stat): 16692 (minisat+_script) S 16691 16692 9102 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843280597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16692/statm): 531 226 485 147 0 384 0
[pid=16692] vsize: 2124
Raw data (/proc/16696/stat): 16696 (minisat+_64-bit) R 16692 16692 9102 0 -1 0 10529 0 0 0 92901 53 0 0 25 0 1 0 1843280602 38637568 8806 4294967295 134512640 135094434 3221224448 3221223104 134558135 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16696/statm): 9433 8806 145 145 0 9288 0
[pid=16696] vsize: 37732
Current children cumulated CPU time (s) 929.55
Current children cumulated vsize (Kb) 39856

[startup+940.107 s]
Raw data (loadavg): 0.99 0.97 0.98 2/58 16726
Raw data (/proc/16692/stat): 16692 (minisat+_script) S 16691 16692 9102 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843280597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16692/statm): 531 226 485 147 0 384 0
[pid=16692] vsize: 2124
Raw data (/proc/16696/stat): 16696 (minisat+_64-bit) R 16692 16692 9102 0 -1 0 10529 0 0 0 93901 53 0 0 25 0 1 0 1843280602 38637568 8806 4294967295 134512640 135094434 3221224448 3221223072 134557711 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16696/statm): 9433 8806 145 145 0 9288 0
[pid=16696] vsize: 37732
Current children cumulated CPU time (s) 939.55
Current children cumulated vsize (Kb) 39856

[startup+950.108 s]
Raw data (loadavg): 0.99 0.97 0.98 2/58 16726
Raw data (/proc/16692/stat): 16692 (minisat+_script) S 16691 16692 9102 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843280597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16692/statm): 531 226 485 147 0 384 0
[pid=16692] vsize: 2124
Raw data (/proc/16696/stat): 16696 (minisat+_64-bit) R 16692 16692 9102 0 -1 0 10529 0 0 0 94901 53 0 0 25 0 1 0 1843280602 38637568 8806 4294967295 134512640 135094434 3221224448 3221223072 134557728 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16696/statm): 9433 8806 145 145 0 9288 0
[pid=16696] vsize: 37732
Current children cumulated CPU time (s) 949.55
Current children cumulated vsize (Kb) 39856

[startup+960.109 s]
Raw data (loadavg): 0.99 0.97 0.98 2/58 16728
Raw data (/proc/16692/stat): 16692 (minisat+_script) S 16691 16692 9102 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843280597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16692/statm): 531 226 485 147 0 384 0
[pid=16692] vsize: 2124
Raw data (/proc/16696/stat): 16696 (minisat+_64-bit) R 16692 16692 9102 0 -1 0 10529 0 0 0 95902 53 0 0 25 0 1 0 1843280602 38637568 8806 4294967295 134512640 135094434 3221224448 3221223104 134557948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16696/statm): 9433 8806 145 145 0 9288 0
[pid=16696] vsize: 37732
Current children cumulated CPU time (s) 959.56
Current children cumulated vsize (Kb) 39856

[startup+970.11 s]
Raw data (loadavg): 0.99 0.97 0.98 2/58 16728
Raw data (/proc/16692/stat): 16692 (minisat+_script) S 16691 16692 9102 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843280597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16692/statm): 531 226 485 147 0 384 0
[pid=16692] vsize: 2124
Raw data (/proc/16696/stat): 16696 (minisat+_64-bit) R 16692 16692 9102 0 -1 0 10529 0 0 0 96902 53 0 0 25 0 1 0 1843280602 38637568 8806 4294967295 134512640 135094434 3221224448 3221223120 134556540 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16696/statm): 9433 8806 145 145 0 9288 0
[pid=16696] vsize: 37732
Current children cumulated CPU time (s) 969.56
Current children cumulated vsize (Kb) 39856

[startup+980.111 s]
Raw data (loadavg): 0.99 0.97 0.98 2/58 16728
Raw data (/proc/16692/stat): 16692 (minisat+_script) S 16691 16692 9102 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843280597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16692/statm): 531 226 485 147 0 384 0
[pid=16692] vsize: 2124
Raw data (/proc/16696/stat): 16696 (minisat+_64-bit) R 16692 16692 9102 0 -1 0 10529 0 0 0 97902 53 0 0 25 0 1 0 1843280602 38637568 8806 4294967295 134512640 135094434 3221224448 3221223072 134557565 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16696/statm): 9433 8806 145 145 0 9288 0
[pid=16696] vsize: 37732
Current children cumulated CPU time (s) 979.56
Current children cumulated vsize (Kb) 39856

[startup+990.112 s]
Raw data (loadavg): 0.99 0.97 0.98 2/58 16728
Raw data (/proc/16692/stat): 16692 (minisat+_script) S 16691 16692 9102 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843280597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16692/statm): 531 226 485 147 0 384 0
[pid=16692] vsize: 2124
Raw data (/proc/16696/stat): 16696 (minisat+_64-bit) R 16692 16692 9102 0 -1 0 10529 0 0 0 98902 53 0 0 25 0 1 0 1843280602 38637568 8806 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16696/statm): 9433 8806 145 145 0 9288 0
[pid=16696] vsize: 37732
Current children cumulated CPU time (s) 989.56
Current children cumulated vsize (Kb) 39856

[startup+1000.11 s]
Raw data (loadavg): 0.99 0.97 0.98 2/58 16728
Raw data (/proc/16692/stat): 16692 (minisat+_script) S 16691 16692 9102 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843280597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16692/statm): 531 226 485 147 0 384 0
[pid=16692] vsize: 2124
Raw data (/proc/16696/stat): 16696 (minisat+_64-bit) R 16692 16692 9102 0 -1 0 10529 0 0 0 99903 53 0 0 25 0 1 0 1843280602 38637568 8806 4294967295 134512640 135094434 3221224448 3221223072 134562108 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16696/statm): 9433 8806 145 145 0 9288 0
[pid=16696] vsize: 37732
Current children cumulated CPU time (s) 999.57
Current children cumulated vsize (Kb) 39856

[startup+1010.11 s]
Raw data (loadavg): 0.99 0.97 0.98 2/58 16728
Raw data (/proc/16692/stat): 16692 (minisat+_script) S 16691 16692 9102 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843280597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16692/statm): 531 226 485 147 0 384 0
[pid=16692] vsize: 2124
Raw data (/proc/16696/stat): 16696 (minisat+_64-bit) R 16692 16692 9102 0 -1 0 10529 0 0 0 100903 53 0 0 25 0 1 0 1843280602 38637568 8806 4294967295 134512640 135094434 3221224448 3221223104 134557884 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16696/statm): 9433 8806 145 145 0 9288 0
[pid=16696] vsize: 37732
Current children cumulated CPU time (s) 1009.57
Current children cumulated vsize (Kb) 39856

[startup+1020.12 s]
Raw data (loadavg): 0.99 0.97 0.98 2/58 16730
Raw data (/proc/16692/stat): 16692 (minisat+_script) S 16691 16692 9102 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843280597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16692/statm): 531 226 485 147 0 384 0
[pid=16692] vsize: 2124
Raw data (/proc/16696/stat): 16696 (minisat+_64-bit) R 16692 16692 9102 0 -1 0 10529 0 0 0 101903 53 0 0 25 0 1 0 1843280602 38637568 8806 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16696/statm): 9433 8806 145 145 0 9288 0
[pid=16696] vsize: 37732
Current children cumulated CPU time (s) 1019.57
Current children cumulated vsize (Kb) 39856

[startup+1030.12 s]
Raw data (loadavg): 0.99 0.97 0.98 2/58 16730
Raw data (/proc/16692/stat): 16692 (minisat+_script) S 16691 16692 9102 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843280597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16692/statm): 531 226 485 147 0 384 0
[pid=16692] vsize: 2124
Raw data (/proc/16696/stat): 16696 (minisat+_64-bit) R 16692 16692 9102 0 -1 0 10529 0 0 0 102903 53 0 0 25 0 1 0 1843280602 38637568 8806 4294967295 134512640 135094434 3221224448 3221223040 134557042 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16696/statm): 9433 8806 145 145 0 9288 0
[pid=16696] vsize: 37732
Current children cumulated CPU time (s) 1029.57
Current children cumulated vsize (Kb) 39856

[startup+1040.12 s]
Raw data (loadavg): 0.99 0.97 0.98 2/58 16730
Raw data (/proc/16692/stat): 16692 (minisat+_script) S 16691 16692 9102 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843280597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16692/statm): 531 226 485 147 0 384 0
[pid=16692] vsize: 2124
Raw data (/proc/16696/stat): 16696 (minisat+_64-bit) R 16692 16692 9102 0 -1 0 10529 0 0 0 103904 53 0 0 25 0 1 0 1843280602 38637568 8806 4294967295 134512640 135094434 3221224448 3221223092 134558261 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16696/statm): 9433 8806 145 145 0 9288 0
[pid=16696] vsize: 37732
Current children cumulated CPU time (s) 1039.58
Current children cumulated vsize (Kb) 39856

[startup+1050.12 s]
Raw data (loadavg): 0.99 0.97 0.98 2/58 16730
Raw data (/proc/16692/stat): 16692 (minisat+_script) S 16691 16692 9102 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843280597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16692/statm): 531 226 485 147 0 384 0
[pid=16692] vsize: 2124
Raw data (/proc/16696/stat): 16696 (minisat+_64-bit) R 16692 16692 9102 0 -1 0 10529 0 0 0 104904 53 0 0 25 0 1 0 1843280602 38637568 8806 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16696/statm): 9433 8806 145 145 0 9288 0
[pid=16696] vsize: 37732
Current children cumulated CPU time (s) 1049.58
Current children cumulated vsize (Kb) 39856

[startup+1060.12 s]
Raw data (loadavg): 0.99 0.97 0.98 2/58 16730
Raw data (/proc/16692/stat): 16692 (minisat+_script) S 16691 16692 9102 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843280597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16692/statm): 531 226 485 147 0 384 0
[pid=16692] vsize: 2124
Raw data (/proc/16696/stat): 16696 (minisat+_64-bit) R 16692 16692 9102 0 -1 0 10529 0 0 0 105904 53 0 0 25 0 1 0 1843280602 38637568 8806 4294967295 134512640 135094434 3221224448 3221223104 134557879 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16696/statm): 9433 8806 145 145 0 9288 0
[pid=16696] vsize: 37732
Current children cumulated CPU time (s) 1059.58
Current children cumulated vsize (Kb) 39856

[startup+1070.12 s]
Raw data (loadavg): 0.99 0.97 0.98 2/58 16730
Raw data (/proc/16692/stat): 16692 (minisat+_script) S 16691 16692 9102 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843280597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16692/statm): 531 226 485 147 0 384 0
[pid=16692] vsize: 2124
Raw data (/proc/16696/stat): 16696 (minisat+_64-bit) R 16692 16692 9102 0 -1 0 10529 0 0 0 106904 53 0 0 25 0 1 0 1843280602 38637568 8806 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16696/statm): 9433 8806 145 145 0 9288 0
[pid=16696] vsize: 37732
Current children cumulated CPU time (s) 1069.58
Current children cumulated vsize (Kb) 39856

[startup+1080.12 s]
Raw data (loadavg): 0.99 0.97 0.98 2/58 16732
Raw data (/proc/16692/stat): 16692 (minisat+_script) S 16691 16692 9102 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843280597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16692/statm): 531 226 485 147 0 384 0
[pid=16692] vsize: 2124
Raw data (/proc/16696/stat): 16696 (minisat+_64-bit) R 16692 16692 9102 0 -1 0 10529 0 0 0 107904 53 0 0 25 0 1 0 1843280602 38637568 8806 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16696/statm): 9433 8806 145 145 0 9288 0
[pid=16696] vsize: 37732
Current children cumulated CPU time (s) 1079.58
Current children cumulated vsize (Kb) 39856

[startup+1090.12 s]
Raw data (loadavg): 0.99 0.97 0.98 2/58 16732
Raw data (/proc/16692/stat): 16692 (minisat+_script) S 16691 16692 9102 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843280597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16692/statm): 531 226 485 147 0 384 0
[pid=16692] vsize: 2124
Raw data (/proc/16696/stat): 16696 (minisat+_64-bit) R 16692 16692 9102 0 -1 0 10529 0 0 0 108905 53 0 0 25 0 1 0 1843280602 38637568 8806 4294967295 134512640 135094434 3221224448 3221223072 134557737 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16696/statm): 9433 8806 145 145 0 9288 0
[pid=16696] vsize: 37732
Current children cumulated CPU time (s) 1089.59
Current children cumulated vsize (Kb) 39856

[startup+1100.12 s]
Raw data (loadavg): 0.99 0.97 0.98 2/58 16732
Raw data (/proc/16692/stat): 16692 (minisat+_script) S 16691 16692 9102 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843280597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16692/statm): 531 226 485 147 0 384 0
[pid=16692] vsize: 2124
Raw data (/proc/16696/stat): 16696 (minisat+_64-bit) R 16692 16692 9102 0 -1 0 10529 0 0 0 109905 53 0 0 25 0 1 0 1843280602 38637568 8806 4294967295 134512640 135094434 3221224448 3221223104 134557823 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16696/statm): 9433 8806 145 145 0 9288 0
[pid=16696] vsize: 37732
Current children cumulated CPU time (s) 1099.59
Current children cumulated vsize (Kb) 39856

[startup+1110.12 s]
Raw data (loadavg): 0.99 0.97 0.98 2/58 16732
Raw data (/proc/16692/stat): 16692 (minisat+_script) S 16691 16692 9102 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843280597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16692/statm): 531 226 485 147 0 384 0
[pid=16692] vsize: 2124
Raw data (/proc/16696/stat): 16696 (minisat+_64-bit) R 16692 16692 9102 0 -1 0 10529 0 0 0 110905 53 0 0 25 0 1 0 1843280602 38637568 8806 4294967295 134512640 135094434 3221224448 3221223092 134558040 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16696/statm): 9433 8806 145 145 0 9288 0
[pid=16696] vsize: 37732
Current children cumulated CPU time (s) 1109.59
Current children cumulated vsize (Kb) 39856

[startup+1120.13 s]
Raw data (loadavg): 0.99 0.97 0.98 2/58 16732
Raw data (/proc/16692/stat): 16692 (minisat+_script) S 16691 16692 9102 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843280597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16692/statm): 531 226 485 147 0 384 0
[pid=16692] vsize: 2124
Raw data (/proc/16696/stat): 16696 (minisat+_64-bit) R 16692 16692 9102 0 -1 0 10529 0 0 0 111905 53 0 0 25 0 1 0 1843280602 38637568 8806 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16696/statm): 9433 8806 145 145 0 9288 0
[pid=16696] vsize: 37732
Current children cumulated CPU time (s) 1119.59
Current children cumulated vsize (Kb) 39856

[startup+1130.13 s]
Raw data (loadavg): 0.99 0.97 0.98 2/58 16732
Raw data (/proc/16692/stat): 16692 (minisat+_script) S 16691 16692 9102 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843280597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16692/statm): 531 226 485 147 0 384 0
[pid=16692] vsize: 2124
Raw data (/proc/16696/stat): 16696 (minisat+_64-bit) R 16692 16692 9102 0 -1 0 10529 0 0 0 112906 53 0 0 25 0 1 0 1843280602 38637568 8806 4294967295 134512640 135094434 3221224448 3221223104 134557950 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16696/statm): 9433 8806 145 145 0 9288 0
[pid=16696] vsize: 37732
Current children cumulated CPU time (s) 1129.6
Current children cumulated vsize (Kb) 39856

[startup+1140.13 s]
Raw data (loadavg): 0.99 0.97 0.98 2/58 16734
Raw data (/proc/16692/stat): 16692 (minisat+_script) S 16691 16692 9102 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843280597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16692/statm): 531 226 485 147 0 384 0
[pid=16692] vsize: 2124
Raw data (/proc/16696/stat): 16696 (minisat+_64-bit) R 16692 16692 9102 0 -1 0 10529 0 0 0 113906 53 0 0 25 0 1 0 1843280602 38637568 8806 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16696/statm): 9433 8806 145 145 0 9288 0
[pid=16696] vsize: 37732
Current children cumulated CPU time (s) 1139.6
Current children cumulated vsize (Kb) 39856

[startup+1150.13 s]
Raw data (loadavg): 0.99 0.97 0.98 2/58 16734
Raw data (/proc/16692/stat): 16692 (minisat+_script) S 16691 16692 9102 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843280597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16692/statm): 531 226 485 147 0 384 0
[pid=16692] vsize: 2124
Raw data (/proc/16696/stat): 16696 (minisat+_64-bit) R 16692 16692 9102 0 -1 0 10529 0 0 0 114906 53 0 0 25 0 1 0 1843280602 38637568 8806 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16696/statm): 9433 8806 145 145 0 9288 0
[pid=16696] vsize: 37732
Current children cumulated CPU time (s) 1149.6
Current children cumulated vsize (Kb) 39856

[startup+1160.13 s]
Raw data (loadavg): 0.99 0.97 0.98 2/58 16734
Raw data (/proc/16692/stat): 16692 (minisat+_script) S 16691 16692 9102 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843280597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16692/statm): 531 226 485 147 0 384 0
[pid=16692] vsize: 2124
Raw data (/proc/16696/stat): 16696 (minisat+_64-bit) R 16692 16692 9102 0 -1 0 10529 0 0 0 115906 53 0 0 25 0 1 0 1843280602 38637568 8806 4294967295 134512640 135094434 3221224448 3221223072 134557714 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16696/statm): 9433 8806 145 145 0 9288 0
[pid=16696] vsize: 37732
Current children cumulated CPU time (s) 1159.6
Current children cumulated vsize (Kb) 39856

[startup+1170.13 s]
Raw data (loadavg): 0.99 0.97 0.98 2/58 16734
Raw data (/proc/16692/stat): 16692 (minisat+_script) S 16691 16692 9102 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843280597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16692/statm): 531 226 485 147 0 384 0
[pid=16692] vsize: 2124
Raw data (/proc/16696/stat): 16696 (minisat+_64-bit) R 16692 16692 9102 0 -1 0 10529 0 0 0 116907 53 0 0 25 0 1 0 1843280602 38637568 8806 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16696/statm): 9433 8806 145 145 0 9288 0
[pid=16696] vsize: 37732
Current children cumulated CPU time (s) 1169.61
Current children cumulated vsize (Kb) 39856

[startup+1180.13 s]
Raw data (loadavg): 0.99 0.97 0.98 2/58 16734
Raw data (/proc/16692/stat): 16692 (minisat+_script) S 16691 16692 9102 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843280597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16692/statm): 531 226 485 147 0 384 0
[pid=16692] vsize: 2124
Raw data (/proc/16696/stat): 16696 (minisat+_64-bit) R 16692 16692 9102 0 -1 0 10529 0 0 0 117907 53 0 0 25 0 1 0 1843280602 38637568 8806 4294967295 134512640 135094434 3221224448 3221223104 134557872 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16696/statm): 9433 8806 145 145 0 9288 0
[pid=16696] vsize: 37732
Current children cumulated CPU time (s) 1179.61
Current children cumulated vsize (Kb) 39856

[startup+1190.13 s]
Raw data (loadavg): 0.99 0.97 0.98 2/58 16734
Raw data (/proc/16692/stat): 16692 (minisat+_script) S 16691 16692 9102 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843280597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16692/statm): 531 226 485 147 0 384 0
[pid=16692] vsize: 2124
Raw data (/proc/16696/stat): 16696 (minisat+_64-bit) R 16692 16692 9102 0 -1 0 10529 0 0 0 118907 53 0 0 25 0 1 0 1843280602 38637568 8806 4294967295 134512640 135094434 3221224448 3221223104 134557928 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16696/statm): 9433 8806 145 145 0 9288 0
[pid=16696] vsize: 37732
Current children cumulated CPU time (s) 1189.61
Current children cumulated vsize (Kb) 39856

[startup+1200.13 s]
Raw data (loadavg): 0.99 0.97 0.98 2/58 16736
Raw data (/proc/16692/stat): 16692 (minisat+_script) S 16691 16692 9102 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843280597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16692/statm): 531 226 485 147 0 384 0
[pid=16692] vsize: 2124
Raw data (/proc/16696/stat): 16696 (minisat+_64-bit) R 16692 16692 9102 0 -1 0 10529 0 0 0 119907 53 0 0 25 0 1 0 1843280602 38637568 8806 4294967295 134512640 135094434 3221224448 3221223120 134556252 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16696/statm): 9433 8806 145 145 0 9288 0
[pid=16696] vsize: 37732
Current children cumulated CPU time (s) 1199.61
Current children cumulated vsize (Kb) 39856

[startup+1210.14 s]
Raw data (loadavg): 0.99 0.97 0.98 2/58 16736
Raw data (/proc/16692/stat): 16692 (minisat+_script) S 16691 16692 9102 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843280597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16692/statm): 531 226 485 147 0 384 0
[pid=16692] vsize: 2124
Raw data (/proc/16696/stat): 16696 (minisat+_64-bit) R 16692 16692 9102 0 -1 0 10529 0 0 0 120907 53 0 0 25 0 1 0 1843280602 38637568 8806 4294967295 134512640 135094434 3221224448 3221223040 134556812 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16696/statm): 9433 8806 145 145 0 9288 0
[pid=16696] vsize: 37732
Current children cumulated CPU time (s) 1209.61
Current children cumulated vsize (Kb) 39856



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.14 s]
Raw data (loadavg): 0.99 0.97 0.98 2/58 16736
Raw data (/proc/16692/stat): 16692 (minisat+_script) S 16691 16692 9102 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843280597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16692/statm): 531 226 485 147 0 384 0
[pid=16692] vsize: 2124
Raw data (/proc/16696/stat): 16696 (minisat+_64-bit) R 16692 16692 9102 0 -1 0 10529 0 0 0 120907 53 0 0 25 0 1 0 1843280602 38637568 8806 4294967295 134512640 135094434 3221224448 3221223040 134556812 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16696/statm): 9433 8806 145 145 0 9288 0
[pid=16696] vsize: 37732
Current children cumulated CPU time (s) 1209.61
Current children cumulated vsize (Kb) 39856

Sending SIGTERM to -16692
Sleeping 2 seconds
One traced child (pid=16692) ended because it received signal 15 (SIGTERM)
One traced child (pid=16696) exited with status: 10
All traced children have exited ! Game is over.

Child status: 10
Real time (s): 1210.16
CPU time (s): 1209.63
CPU user time (s): 1209.08
CPU system time (s): 0.556915
CPU usage (%): 99.9568
Max. virtual memory (cumulated for all children) (Kb): 39856

Verifier Data

ERROR: no interpretation found !