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

Namemps-v2-13-7/MIPLIB/miplib2003/normalized-mps-v2-13-7-roll3000.opb
MD5SUM8932ff592f10c4a440d98245533252f1
Bench Categoryoptimization, big integers (OPTBIGINT)
Has Objective FunctionYES
Satisfiable
(Un)Satisfiability was proved
Best value of the objective function
Optimality of the best value was proved
Number of terms in the objective function 21
Biggest coefficient in the objective function 1048576
Number of bits for the biggest coefficient in the objective function 21
Sum of the numbers in the objective function 2097151
Number of bits of the sum of numbers in the objective function 21
Biggest number in a constraint 128000000000
Number of bits of the biggest number in a constraint 37
Biggest sum of numbers in a constraint 265438953471
Number of bits of the biggest sum of numbers38
Best result obtained on this benchmark
Best CPU time to get the best result obtained on this benchmark
Number of variables7611
Total number of constraints3459
Number of constraints which are clauses143
Number of constraints which are cardinality constraints (but not clauses)626
Number of constraints which are nor clauses,nor cardinality constraints2690
Minimum length of a constraint1
Maximum length of a constraint2047

Trace number 6160

Launcher Data

LAUNCH ON wulflinc4 THE 2005-09-20 03:56:26 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3324 boxname=wulflinc4 idbench=980 idsolver=3 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  8932ff592f10c4a440d98245533252f1  /oldhome/oroussel/tmp/wulflinc4/normalized-mps-v2-13-7-roll3000.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc4/normalized-mps-v2-13-7-roll3000.opb
IDLAUNCH: 3324
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.169
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	: 890.88

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        864796 kB
Buffers:         33584 kB
Cached:         109564 kB
SwapCached:        876 kB
Active:          55764 kB
Inactive:        89952 kB
HighTotal:      131008 kB
HighFree:        23912 kB
LowTotal:       903652 kB
LowFree:        840884 kB
SwapTotal:     2097136 kB
SwapFree:      2095644 kB
Dirty:              32 kB
Writeback:           0 kB
Mapped:           5540 kB
Slab:            18428 kB
Committed_AS:    72360 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-09-20 04:16:37 (client local time) WITH STATUS 0 IN 1208.52 SECONDS
stats: 3324 7 1208.52 0

Solver Data

c Parsing PB file...
c Converting 2918 PB-constraints to clauses...
c   -- Unit propagations: pppppppppppppppppppp
c   -- Detecting intervals from adjacent constraints: ==###########################################################################################################################################################################=###
c   -- Clauses(.)/Splits(s): ...............................................................................................................................................................................................................................................................................................................................................................................................ssssssss.ssssssssssssssssssss.ssssssssssssssssssss.sssssssssssssssssss.ssssssssssssssssss.sssss..............................................................ssssssssssssssssss.ssssssssssssssssssss.ssssssssssssssssss.ss...................................................................................................................................................ss.ss.sssss..sssssssss..sssssss..ssssss..ss.sssss...sssssss.ssssss.sss.sssssssss..ss.s.sss....sss.s.ssss...sss.sssss.s.s.ssss...ss.ss....ss.s..ss..ss...s.sss.ss...ssssss..s..sss..ss.ss..sss.s....sss.......s.ssss..ss.ss..ss.s...sssss..
c ---[2461]---> BDD-cost:   11
c ---[2460]---> BDD-cost:   11
c ---[2453]---> BDD-cost:   11
c ---[2452]---> BDD-cost:   11
c ---[2450]---> BDD-cost:   11
c ---[2449]---> BDD-cost:   11
c ---[2447]---> BDD-cost:   11
c ---[2446]---> BDD-cost:   11
c ---[2445]---> BDD-cost:   11
c ---[2443]---> BDD-cost:   11
c ---[2442]---> BDD-cost:   11
c ---[2440]---> BDD-cost:   11
c ---[2439]---> BDD-cost:   11
c ---[2438]---> BDD-cost:   11
c ---[2436]---> BDD-cost:   11
c ---[2435]---> BDD-cost:   11
c ---[2433]---> BDD-cost:   11
c ---[2432]---> BDD-cost:   11
c ---[2431]---> BDD-cost:   11
c ---[2429]---> BDD-cost:   11
c ---[2428]---> BDD-cost:   11
c ---[2427]---> BDD-cost:   11
c ---[2426]---> BDD-cost:   11
c ---[2425]---> BDD-cost:   11
c ---[2424]---> BDD-cost:   11
c ---[2422]---> BDD-cost:   11
c ---[2421]---> BDD-cost:   11
c ---[2420]---> BDD-cost:   11
c ---[2419]---> BDD-cost:   11
c ---[2418]---> BDD-cost:   11
c ---[2417]---> BDD-cost:   11
c ---[2415]---> BDD-cost:   11
c ---[2414]---> BDD-cost:   11
c ---[2413]---> BDD-cost:   11
c ---[2412]---> BDD-cost:   11
c ---[2411]---> BDD-cost:   11
c ---[2410]---> BDD-cost:   11
c ---[2407]---> BDD-cost:   11
c ---[2406]---> BDD-cost:   11
c ---[2405]---> BDD-cost:   11
c ---[2403]---> BDD-cost:   11
c ---[2402]---> BDD-cost:   11
c ---[2401]---> BDD-cost:   11
c ---[2400]---> BDD-cost:   11
c ---[2399]---> BDD-cost:   11
c ---[2397]---> BDD-cost:   11
c ---[2396]---> BDD-cost:   11
c ---[2395]---> BDD-cost:   11
c ---[2394]---> BDD-cost:   11
c ---[2393]---> BDD-cost:   11
c ---[2391]---> BDD-cost:   11
c ---[2390]---> BDD-cost:   11
c ---[2389]---> BDD-cost:   11
c ---[2388]---> BDD-cost:   11
c ---[2387]---> BDD-cost:   11
c ---[2385]---> BDD-cost:   11
c ---[2384]---> BDD-cost:   11
c ---[2383]---> BDD-cost:   11
c ---[2382]---> BDD-cost:   11
c ---[2380]---> BDD-cost:   11
c ---[2379]---> BDD-cost:   11
c ---[2378]---> BDD-cost:   11
c ---[2377]---> BDD-cost:   11
c ---[2376]---> BDD-cost:   11
c ---[2375]---> BDD-cost:   11
c ---[2374]---> BDD-cost:   11
c ---[2373]---> BDD-cost:   11
c ---[2372]---> BDD-cost:   11
c ---[2371]---> BDD-cost:   11
c ---[2370]---> BDD-cost:   11
c ---[2369]---> BDD-cost:   11
c ---[2368]---> BDD-cost:   11
c ---[2367]---> BDD-cost:   11
c ---[2366]---> BDD-cost:   11
c ---[2365]---> BDD-cost:   11
c ---[2364]---> BDD-cost:   11
c ---[2363]---> BDD-cost:   11
c ---[2362]---> BDD-cost:   11
c ---[2361]---> BDD-cost:   11
c ---[2360]---> BDD-cost:   11
c ---[2359]---> BDD-cost:   11
c ---[2358]---> BDD-cost:   11
c ---[2357]---> BDD-cost:   11
c ---[2356]---> BDD-cost:   11
c ---[2355]---> BDD-cost:   11
c ---[2354]---> BDD-cost:   11
c ---[2353]---> BDD-cost:   11
c ---[2352]---> BDD-cost:   11
c ---[2351]---> BDD-cost:   11
c ---[2350]---> BDD-cost:   11
c ---[2349]---> BDD-cost:   11
c ---[2348]---> BDD-cost:   11
c ---[2347]---> BDD-cost:   11
c ---[2346]---> BDD-cost:   11
c ---[2345]---> BDD-cost:   11
c ---[2344]---> BDD-cost:   11
c ---[2343]---> BDD-cost:   11
c ---[2342]---> BDD-cost:   11
c ---[2341]---> BDD-cost:   11
c ---[2340]---> BDD-cost:   11
c ---[2339]---> BDD-cost:   11
c ---[2338]---> BDD-cost:   11
c ---[2337]---> BDD-cost:   11
c ---[2336]---> BDD-cost:   11
c ---[2335]---> BDD-cost:   11
c ---[2334]---> BDD-cost:   11
c ---[2333]---> BDD-cost:   11
c ---[2332]---> BDD-cost:   11
c ---[2331]---> BDD-cost:   11
c ---[2330]---> BDD-cost:   11
c ---[2329]---> BDD-cost:   11
c ---[2328]---> BDD-cost:   11
c ---[2327]---> BDD-cost:   11
c ---[2326]---> BDD-cost:   11
c ---[2325]---> BDD-cost:   11
c ---[2324]---> BDD-cost:   11
c ---[2323]---> BDD-cost:   11
c ---[2322]---> BDD-cost:   11
c ---[2321]---> BDD-cost:   11
c ---[2320]---> BDD-cost:   11
c ---[2319]---> BDD-cost:   11
c ---[2318]---> BDD-cost:   11
c ---[2317]---> BDD-cost:   11
c ---[2316]---> BDD-cost:   11
c ---[2315]---> BDD-cost:   11
c ---[2314]---> BDD-cost:   11
c ---[2313]---> BDD-cost:   11
c ---[2312]---> BDD-cost:   11
c ---[2311]---> BDD-cost:   11
c ---[2310]---> BDD-cost:   11
c ---[2309]---> BDD-cost:   11
c ---[2308]---> BDD-cost:   11
c ---[2307]---> BDD-cost:   11
c ---[2306]---> BDD-cost:   11
c ---[2305]---> BDD-cost:   11
c ---[2304]---> BDD-cost:   11
c ---[2303]---> BDD-cost:   11
c ---[2302]---> BDD-cost:   11
c ---[2301]---> BDD-cost:   11
c ---[2300]---> BDD-cost:   11
c ---[2299]---> BDD-cost:   11
c ---[2298]---> BDD-cost:   11
c ---[2297]---> BDD-cost:   11
c ---[2296]---> BDD-cost:   11
c ---[2295]---> BDD-cost:   11
c ---[2294]---> BDD-cost:   11
c ---[2293]---> BDD-cost:   11
c ---[2292]---> BDD-cost:   11
c ---[2291]---> BDD-cost:   11
c ---[2290]---> BDD-cost:   11
c ---[2289]---> BDD-cost:   11
c ---[2288]---> BDD-cost:   11
c ---[2287]---> BDD-cost:   11
c ---[2286]---> BDD-cost:   11
c ---[2285]---> BDD-cost:   11
c ---[2284]---> BDD-cost:   11
c ---[2283]---> BDD-cost:    8
c ---[2282]---> BDD-cost:    8
c ---[2281]---> BDD-cost:    8
c ---[2280]---> BDD-cost:    8
c ---[2279]---> BDD-cost:    8
c ---[2278]---> BDD-cost:   86
c ---[2275]---> BDD-cost:  187
c ---[2274]---> BDD-cost:  197
c ---[2273]---> BDD-cost:  137
c ---[2272]---> BDD-cost:  159
c ---[2271]---> BDD-cost:  211
c ---[2270]---> BDD-cost:  131
c ---[2269]---> BDD-cost:   60
c ---[2268]---> BDD-cost:   60
c ---[2267]---> BDD-cost:   91
c ---[2266]---> BDD-cost:  131
c ---[2265]---> BDD-cost:    2
c ---[2264]---> BDD-cost:   92
c ---[2263]---> BDD-cost:  105
c ---[2262]---> BDD-cost:  141
c ---[2261]---> BDD-cost:   92
c ---[2260]---> BDD-cost:  107
c ---[2259]---> BDD-cost:  123
c ---[2258]---> BDD-cost:   60
c ---[2257]---> BDD-cost:   55
c ---[2256]---> BDD-cost:   67
c ---[2255]---> BDD-cost:  105
c ---[2253]---> BDD-cost:   71
c ---[2252]---> BDD-cost:   77
c ---[2251]---> BDD-cost:  105
c ---[2250]---> BDD-cost:   63
c ---[2249]---> BDD-cost:   67
c ---[2248]---> BDD-cost:   55
c ---[2247]---> BDD-cost:   60
c ---[2246]---> BDD-cost:   91
c ---[2245]---> BDD-cost:  131
c ---[2244]---> BDD-cost:   92
c ---[2243]---> BDD-cost:    2
c ---[2242]---> BDD-cost:  105
c ---[2241]---> BDD-cost:  141
c ---[2240]---> BDD-cost:   92
c ---[2239]---> BDD-cost:  107
c ---[2238]---> BDD-cost:  123
c ---[2237]---> BDD-cost:   60
c ---[2236]---> BDD-cost:   77
c ---[2235]---> BDD-cost:   84
c ---[2234]---> BDD-cost:   99
c ---[2233]---> BDD-cost:  141
c ---[2231]---> BDD-cost:  100
c ---[2230]---> BDD-cost:  101
c ---[2229]---> BDD-cost:  131
c ---[2228]---> BDD-cost:   79
c ---[2227]---> BDD-cost:   79
c ---[2226]---> BDD-cost:   55
c ---[2225]---> BDD-cost:   55
c ---[2224]---> BDD-cost:   39
c ---[2223]---> BDD-cost:   63
c ---[2222]---> BDD-cost:   85
c ---[2221]---> BDD-cost:    2
c ---[2220]---> BDD-cost:   55
c ---[2219]---> BDD-cost:   65
c ---[2218]---> BDD-cost:   75
c ---[2217]---> BDD-cost:   34
c ---[2216]---> BDD-cost:   43
c ---[2215]---> BDD-cost:   55
c ---[2214]---> BDD-cost:   39
c ---[2213]---> BDD-cost:   63
c ---[2212]---> BDD-cost:   85
c ---[2211]---> BDD-cost:   55
c ---[2209]---> BDD-cost:   65
c ---[2208]---> BDD-cost:   75
c ---[2207]---> BDD-cost:   34
c ---[2206]---> BDD-cost:   43
c ---[2205]---> BDD-cost:   55
c ---[2204]---> BDD-cost:   39
c ---[2203]---> BDD-cost:   63
c ---[2202]---> BDD-cost:   85
c ---[2201]---> BDD-cost:   55
c ---[2200]---> BDD-cost:   65
c ---[2199]---> BDD-cost:    2
c ---[2198]---> BDD-cost:   75
c ---[2197]---> BDD-cost:   34
c ---[2196]---> BDD-cost:   43
c ---[2195]---> BDD-cost:   61
c ---[2194]---> BDD-cost:   44
c ---[2193]---> BDD-cost:   69
c ---[2192]---> BDD-cost:   91
c ---[2191]---> BDD-cost:   60
c ---[2190]---> BDD-cost:   71
c ---[2189]---> BDD-cost:   81
c ---[2186]---> BDD-cost:   39
c ---[2185]---> BDD-cost:   61
c ---[2184]---> BDD-cost:   44
c ---[2183]---> BDD-cost:   99
c ---[2182]---> BDD-cost:  121
c ---[2181]---> BDD-cost:   84
c ---[2180]---> BDD-cost:  119
c ---[2179]---> BDD-cost:  141
c ---[2178]---> BDD-cost:   87
c ---[2177]---> BDD-cost:    2
c ---[2176]---> BDD-cost:   71
c ---[2175]---> BDD-cost:   81
c ---[2174]---> BDD-cost:   61
c ---[2173]---> BDD-cost:   26
c ---[2172]---> BDD-cost:   53
c ---[2171]---> BDD-cost:   53
c ---[2170]---> BDD-cost:   39
c ---[2169]---> BDD-cost:   22
c ---[2168]---> BDD-cost:   21
c ---[2167]---> BDD-cost:   33
c ---[2166]---> BDD-cost:    2
c ---[2164]---> BDD-cost:   33
c ---[2163]---> BDD-cost:   19
c ---[2162]---> BDD-cost:   26
c ---[2161]---> BDD-cost:   44
c ---[2160]---> BDD-cost:   50
c ---[2159]---> BDD-cost:   48
c ---[2158]---> BDD-cost:   21
c ---[2157]---> BDD-cost:   21
c ---[2156]---> BDD-cost:   33
c ---[2155]---> BDD-cost:   33
c ---[2154]---> BDD-cost:    8
c ---[2153]---> BDD-cost:   21
c ---[2152]---> BDD-cost:   25
c ---[2151]---> BDD-cost:   22
c ---[2150]---> BDD-cost:   21
c ---[2149]---> BDD-cost:   33
c ---[2148]---> BDD-cost:   33
c ---[2147]---> BDD-cost:   21
c ---[2146]---> BDD-cost:   30
c ---[2145]---> BDD-cost:   36
c ---[2144]---> BDD-cost:   28
c ---[2142]---> BDD-cost:   13
c ---[2141]---> BDD-cost:   19
c ---[2140]---> BDD-cost:   11
c ---[2139]---> BDD-cost:   13
c ---[2138]---> BDD-cost:   19
c ---[2137]---> BDD-cost:   11
c ---[2136]---> BDD-cost:   13
c ---[2135]---> BDD-cost:   19
c ---[2134]---> BDD-cost:   11
c ---[2133]---> BDD-cost:   15
c ---[2132]---> BDD-cost:    2
c ---[2131]---> BDD-cost:   21
c ---[2130]---> BDD-cost:   13
c ---[2129]---> BDD-cost:   15
c ---[2128]---> BDD-cost:   30
c ---[2127]---> BDD-cost:   31
c ---[2126]---> BDD-cost:   25
c ---[2110]---> BDD-cost:    2
c ---[2088]---> BDD-cost:    2
c ---[2066]---> BDD-cost:    2
c ---[2043]---> BDD-cost:    8
c ---[2021]---> BDD-cost:    8
c ---[1999]---> BDD-cost:    8
c ---[1993]---> BDD-cost:    9
c ---[1992]---> BDD-cost:   24
c ---[1991]---> BDD-cost:   14
c ---[1990]---> BDD-cost:   29
c ---[1989]---> BDD-cost:    9
c ---[1987]---> BDD-cost:   24
c ---[1985]---> BDD-cost:    1
c ---[1984]---> BDD-cost:   10
c ---[1983]---> BDD-cost:   14
c ---[1981]---> BDD-cost:    3
c ---[1980]---> BDD-cost:    8
c ---[1979]---> BDD-cost:    4
c ---[1977]---> BDD-cost:    2
c ---[1975]---> BDD-cost:    3
c ---[1974]---> BDD-cost:    2
c ---[1973]---> BDD-cost:    4
c ---[1972]---> BDD-cost:    2
c ---[1971]---> BDD-cost:    2
c ---[1970]---> BDD-cost:    3
c ---[1969]---> BDD-cost:    2
c ---[1968]---> BDD-cost:    2
c ---[1966]---> BDD-cost:    2
c ---[1963]---> BDD-cost:    4
c ---[1962]---> BDD-cost:    2
c ---[1961]---> BDD-cost:    3
c ---[1960]---> BDD-cost:   14
c ---[1959]---> BDD-cost:    4
c ---[1958]---> BDD-cost:   14
c ---[1957]---> BDD-cost:    3
c ---[1956]---> BDD-cost:    4
c ---[1954]---> BDD-cost:    2
c ---[1953]---> BDD-cost:    2
c ---[1952]---> BDD-cost:    2
c ---[1951]---> BDD-cost:    3
c ---[1950]---> BDD-cost:    2
c ---[1948]---> BDD-cost:    4
c ---[1947]---> BDD-cost:    2
c ---[1946]---> BDD-cost:    3
c ---[1945]---> BDD-cost:    2
c ---[1944]---> BDD-cost:    2
c ---[1942]---> BDD-cost:    2
c ---[1939]---> BDD-cost:    2
c ---[1938]---> BDD-cost:    2
c ---[1937]---> BDD-cost:    2
c ---[1936]---> BDD-cost:    2
c ---[1933]---> BDD-cost:    2
c ---[1932]---> BDD-cost:    3
c ---[1931]---> BDD-cost:    2
c ---[1930]---> BDD-cost:    4
c ---[1928]---> BDD-cost:    2
c ---[1927]---> BDD-cost:    3
c ---[1926]---> BDD-cost:    2
c ---[1925]---> BDD-cost:    2
c ---[1923]---> BDD-cost:    2
c ---[1921]---> BDD-cost:    4
c ---[1920]---> BDD-cost:    3
c ---[1917]---> BDD-cost:    7
c ---[1916]---> BDD-cost:    4
c ---[1915]---> BDD-cost:    3
c ---[1914]---> BDD-cost:    3
c ---[1913]---> BDD-cost:    2
c ---[1912]---> BDD-cost:    2
c ---[1911]---> BDD-cost:    2
c ---[1907]---> BDD-cost:    2
c ---[1905]---> BDD-cost:    2
c ---[1903]---> BDD-cost:    2
c ---[1902]---> BDD-cost:    2
c ---[1900]---> BDD-cost:    2
c ---[1897]---> BDD-cost:    2
c ---[1896]---> BDD-cost:    2
c ---[1894]---> BDD-cost:    2
c ---[1891]---> BDD-cost:    2
c ---[1889]---> BDD-cost:    2
c ---[1888]---> BDD-cost:    2
c ---[1885]---> BDD-cost:    9
c ---[1883]---> BDD-cost:   24
c ---[1882]---> BDD-cost:    4
c ---[1881]---> BDD-cost:    2
c ---[1880]---> BDD-cost:    2
c ---[1879]---> BDD-cost:    8
c ---[1877]---> BDD-cost:    5
c ---[1876]---> BDD-cost:    3
c ---[1874]---> BDD-cost:    2
c ---[1873]---> BDD-cost:    3
c ---[1869]---> BDD-cost:    2
c ---[1868]---> BDD-cost:    5
c ---[1867]---> BDD-cost:    3
c ---[1864]---> BDD-cost:    3
c ---[1861]---> BDD-cost:    2
c ---[1860]---> BDD-cost:    7
c ---[1859]---> BDD-cost:    5
c ---[1858]---> BDD-cost:    3
c ---[1856]---> BDD-cost:    5
c ---[1855]---> BDD-cost:    3
c ---[1854]---> BDD-cost:    2
c ---[1853]---> BDD-cost:    3
c ---[1851]---> BDD-cost:    5
c ---[1850]---> BDD-cost:    3
c ---[1848]---> BDD-cost:    2
c ---[1847]---> BDD-cost:    3
c ---[1842]---> BDD-cost:    5
c ---[1841]---> BDD-cost:    3
c ---[1840]---> BDD-cost:    8
c ---[1839]---> BDD-cost:    3
c ---[1837]---> BDD-cost:    5
c ---[1836]---> BDD-cost:    3
c ---[1834]---> BDD-cost:    8
c ---[1833]---> BDD-cost:    3
c ---[1829]---> BDD-cost:    5
c ---[1828]---> BDD-cost:    3
c ---[1827]---> BDD-cost:    8
c ---[1826]---> BDD-cost:    5
c ---[1825]---> BDD-cost:    3
c ---[1824]---> BDD-cost:    3
c ---[1822]---> BDD-cost:    3
c ---[1820]---> BDD-cost:    8
c ---[1817]---> BDD-cost:    3
c ---[1815]---> BDD-cost:    8
c ---[1813]---> BDD-cost:    3
c ---[1811]---> BDD-cost:    8
c ---[1808]---> BDD-cost:    2
c ---[1807]---> BDD-cost:    3
c ---[1803]---> BDD-cost:    3
c ---[1801]---> BDD-cost:    2
c ---[1796]---> BDD-cost:   17
c ---[1795]---> BDD-cost:   13
c ---[1794]---> BDD-cost:    9
c ---[1793]---> BDD-cost:    2
c ---[1792]---> BDD-cost:   17
c ---[1791]---> BDD-cost:    9
c ---[1790]---> BDD-cost:    5
c ---[1789]---> BDD-cost:   13
c ---[1788]---> BDD-cost:    9
c ---[1787]---> BDD-cost:    4
c ---[1786]---> BDD-cost:    9
c ---[1785]---> BDD-cost:    4
c ---[1784]---> BDD-cost:   16
c ---[1783]---> BDD-cost:   12
c ---[1781]---> BDD-cost:   12
c ---[1780]---> BDD-cost:    8
c ---[1779]---> BDD-cost:   13
c ---[1778]---> BDD-cost:    9
c ---[1777]---> BDD-cost:    9
c ---[1776]---> BDD-cost:    5
c ---[1775]---> BDD-cost:    9
c ---[1774]---> BDD-cost:    5
c ---[1773]---> BDD-cost:    9
c ---[1772]---> BDD-cost:    5
c ---[1771]---> BDD-cost:    2
c ---[1770]---> BDD-cost:   13
c ---[1769]---> BDD-cost:    9
c ---[1768]---> BDD-cost:    9
c ---[1767]---> BDD-cost:    5
c ---[1766]---> BDD-cost:   13
c ---[1765]---> BDD-cost:    9
c ---[1764]---> BDD-cost:    5
c ---[1763]---> BDD-cost:    9
c ---[1762]---> BDD-cost:    5
c ---[1761]---> BDD-cost:    9
c ---[1759]---> BDD-cost:    5
c ---[1758]---> BDD-cost:    5
c ---[1756]---> BDD-cost:    9
c ---[1755]---> BDD-cost:    5
c ---[1754]---> BDD-cost:    5
c ---[1752]---> BDD-cost:    9
c ---[1751]---> BDD-cost:    5
c ---[1750]---> BDD-cost:    5
c ---[1749]---> BDD-cost:    8
c ---[1747]---> BDD-cost:    9
c ---[1746]---> BDD-cost:    5
c ---[1745]---> BDD-cost:    5
c ---[1744]---> BDD-cost:   21
c ---[1743]---> BDD-cost:   17
c ---[1742]---> BDD-cost:    5
c ---[1741]---> BDD-cost:    9
c ---[1740]---> BDD-cost:   12
c ---[1736]---> BDD-cost:    4
c ---[1735]---> BDD-cost:    5
c ---[1734]---> BDD-cost:    9
c ---[1732]---> BDD-cost:    5
c ---[1731]---> BDD-cost:    4
c ---[1730]---> BDD-cost:    8
c ---[1728]---> BDD-cost:    4
c ---[1727]---> BDD-cost:    4
c ---[1726]---> BDD-cost:    8
c ---[1725]---> BDD-cost:    8
c ---[1723]---> BDD-cost:    4
c ---[1722]---> BDD-cost:    5
c ---[1721]---> BDD-cost:    9
c ---[1719]---> BDD-cost:    5
c ---[1717]---> BDD-cost:    5
c ---[1716]---> BDD-cost:    5
c ---[1714]---> BDD-cost:    9
c ---[1713]---> BDD-cost:    5
c ---[1712]---> BDD-cost:    5
c ---[1711]---> BDD-cost:    9
c ---[1708]---> BDD-cost:    5
c ---[1707]---> BDD-cost:    5
c ---[1704]---> BDD-cost:    8
c ---[1703]---> BDD-cost:    5
c ---[1702]---> BDD-cost:    5
c ---[1699]---> BDD-cost:    5
c ---[1698]---> BDD-cost:    5
c ---[1695]---> BDD-cost:    5
c ---[1691]---> BDD-cost:    5
c ---[1689]---> BDD-cost:   67
c ---[1687]---> Adder-cost: 182   maxlim: 13055   bits: 15/14
c ---[1685]---> Adder-cost: 226   maxlim: 15103   bits: 15/14
c ---[1683]---> BDD-cost:   67
c ---[1681]---> Sorter-cost:  307     Base: 2 2 2 2 2 2 2 2 2
c ---[1679]---> Sorter-cost: 1292     Base: 2 2 2 2 2 2 2 2
c ---[1677]---> Adder-cost: 186   maxlim: 14719   bits: 15/14
c ---[1676]---> BDD-cost:    1
c ---[1674]---> Adder-cost: 202   maxlim: 15231   bits: 15/14
c ---[1672]---> Sorter-cost:  502     Base: 2 2 2 2 2 2 2 2
c ---[1670]---> Adder-cost: 140   maxlim: 13311   bits: 15/14
c ---[1668]---> Adder-cost: 214   maxlim: 15103   bits: 15/14
c ---[1666]---> Sorter-cost:  564     Base: 2 2 2 2 2 2 2 2
c ---[1664]---> Adder-cost: 108   maxlim: 11775   bits: 14/14
c ---[1662]---> Adder-cost: 170   maxlim: 14847   bits: 15/14
c ---[1660]---> Adder-cost: 148   maxlim: 15359   bits: 15/14
c ---[1658]---> Sorter-cost:  896     Base: 2 2 2 2 2 2 2 2
c ---[1656]---> Adder-cost: 162   maxlim: 13567   bits: 15/14
c ---[1653]---> Adder-cost: 146   maxlim: 15871   bits: 15/14
c ---[1651]---> Sorter-cost:  890     Base: 2 2 2 2 2 2 2 2
c ---[1649]---> Adder-cost: 114   maxlim: 12287   bits: 14/14
c ---[1647]---> Adder-cost: 136   maxlim: 15103   bits: 15/14
c ---[1645]---> Adder-cost: 206   maxlim: 15871   bits: 15/14
c ---[1643]---> Sorter-cost: 1038     Base: 2 2 2 2 2 2 2 2
c ---[1641]---> Adder-cost: 132   maxlim: 13695   bits: 15/14
c ---[1639]---> Adder-cost: 172   maxlim: 16255   bits: 15/14
c ---[1637]---> Sorter-cost: 1070     Base: 2 2 2 2 2 2 2 2
c ---[1635]---> Adder-cost: 98   maxlim: 12671   bits: 14/14
c ---[1634]---> BDD-cost:    2
c ---[1632]---> Adder-cost: 166   maxlim: 15231   bits: 15/14
c ---[1630]---> Adder-cost: 166   maxlim: 15999   bits: 15/14
c ---[1628]---> Sorter-cost:  378     Base: 2 2 2 2 2 2 2 2
c ---[1626]---> Sorter-cost: 1199     Base: 2 2 2 2 2 2 2 2
c ---[1624]---> Adder-cost: 130   maxlim: 13823   bits: 15/14
c ---[1622]---> Adder-cost: 164   maxlim: 16383   bits: 15/14
c ---[1620]---> Adder-cost: 128   maxlim: 13055   bits: 14/14
c ---[1618]---> Adder-cost: 124   maxlim: 15359   bits: 15/14
c ---[1616]---> Adder-cost: 136   maxlim: 15743   bits: 15/14
c ---[1614]---> Sorter-cost:  660     Base: 2 2 2 2 2 2 2 2
c ---[1611]---> Sorter-cost: 1120     Base: 2 2 2 2 2 2 2 2
c ---[1609]---> Adder-cost: 124   maxlim: 14079   bits: 15/14
c ---[1607]---> Adder-cost: 166   maxlim: 16895   bits: 15/15
c ---[1605]---> Adder-cost: 106   maxlim: 13439   bits: 14/14
c ---[1603]---> Adder-cost: 126   maxlim: 15487   bits: 15/14
c ---[1601]---> Adder-cost: 152   maxlim: 15871   bits: 15/14
c ---[1599]---> Sorter-cost:  348     Base: 2 2 2 2 2 2 2 2
c ---[1597]---> Sorter-cost: 1235     Base: 2 2 2 2 2 2 2 2
c ---[1595]---> Adder-cost: 144   maxlim: 14207   bits: 15/14
c ---[1593]---> Adder-cost: 150   maxlim: 17023   bits: 15/15
c ---[1592]---> BDD-cost:    2
c ---[1590]---> Adder-cost: 120   maxlim: 13823   bits: 15/14
c ---[1588]---> Adder-cost: 134   maxlim: 15615   bits: 15/14
c ---[1586]---> Adder-cost: 180   maxlim: 15615   bits: 15/14
c ---[1584]---> Sorter-cost:  290     Base: 2 2 2 2 2 2 2 2 2
c ---[1582]---> Sorter-cost: 1326     Base: 2 2 2 2 2 2 2 2
c ---[1580]---> Adder-cost: 136   maxlim: 14335   bits: 15/14
c ---[1578]---> Adder-cost: 158   maxlim: 17151   bits: 15/15
c ---[1576]---> BDD-cost:   89
c ---[1574]---> Adder-cost: 114   maxlim: 14079   bits: 15/14
c ---[1572]---> Adder-cost: 136   maxlim: 15615   bits: 15/14
c ---[1571]---> BDD-cost:    8
c ---[1568]---> Sorter-cost: 1447     Base: 2 2 2 2 2 2 2 2
c ---[1566]---> Adder-cost: 122   maxlim: 14463   bits: 15/14
c ---[1564]---> Adder-cost: 144   maxlim: 17279   bits: 15/15
c ---[1562]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 2
c ---[1560]---> Adder-cost: 110   maxlim: 14207   bits: 15/14
c ---[1558]---> Adder-cost: 124   maxlim: 15487   bits: 15/14
c ---[1556]---> Sorter-cost: 1492     Base: 2 2 2 2 2 2 2 2
c ---[1554]---> Adder-cost: 124   maxlim: 14591   bits: 15/14
c ---[1552]---> Adder-cost: 154   maxlim: 17407   bits: 15/15
c ---[1550]---> Sorter-cost:  570     Base: 2 2 2 2 2 2 2 2
c ---[1549]---> BDD-cost:    2
c ---[1547]---> Adder-cost: 112   maxlim: 14335   bits: 15/14
c ---[1545]---> Adder-cost: 114   maxlim: 15359   bits: 15/14
c ---[1543]---> Adder-cost: 104   maxlim: 12031   bits: 14/14
c ---[1541]---> Adder-cost: 128   maxlim: 14591   bits: 15/14
c ---[1539]---> Adder-cost: 250   maxlim: 17023   bits: 15/15
c ---[1537]---> Sorter-cost:  760     Base: 2 2 2 2 2 2 2 2
c ---[1535]---> Adder-cost: 108   maxlim: 14463   bits: 15/14
c ---[1533]---> Adder-cost: 144   maxlim: 15487   bits: 15/14
c ---[1531]---> Adder-cost: 92   maxlim: 12671   bits: 14/14
c ---[1529]---> Adder-cost: 168   maxlim: 14975   bits: 15/14
c ---[1526]---> Sorter-cost: 1006     Base: 2 2 2 2 2 2 2 2
c ---[1524]---> Adder-cost: 106   maxlim: 14591   bits: 15/14
c ---[1522]---> Adder-cost: 114   maxlim: 15359   bits: 15/14
c ---[1520]---> BDD-cost:   72
c ---[1518]---> Adder-cost: 182   maxlim: 13055   bits: 15/14
c ---[1516]---> Adder-cost: 228   maxlim: 15103   bits: 15/14
c ---[1514]---> BDD-cost:   72
c ---[1512]---> Sorter-cost:  318     Base: 2 2 2 2 2 2 2 2 2 2
c ---[1510]---> Adder-cost: 118   maxlim: 11391   bits: 14/14
c ---[1508]---> Adder-cost: 174   maxlim: 14719   bits: 15/14
c ---[1507]---> BDD-cost:    1
c ---[1505]---> Adder-cost: 204   maxlim: 15231   bits: 15/14
c ---[1503]---> Sorter-cost:  560     Base: 2 2 2 2 2 2 2 2 2
c ---[1501]---> Adder-cost: 140   maxlim: 13311   bits: 15/14
c ---[1499]---> Adder-cost: 216   maxlim: 15103   bits: 15/14
c ---[1497]---> Sorter-cost:  643     Base: 2 2 2 2 2 2 2 2 2
c ---[1495]---> Adder-cost: 108   maxlim: 11775   bits: 14/14
c ---[1493]---> Adder-cost: 164   maxlim: 14847   bits: 15/14
c ---[1491]---> Adder-cost: 150   maxlim: 15359   bits: 15/14
c ---[1489]---> Adder-cost: 86   maxlim: 8831   bits: 14/14
c ---[1487]---> Adder-cost: 162   maxlim: 13567   bits: 15/14
c ---[1484]---> Adder-cost: 146   maxlim: 15871   bits: 15/14
c ---[1482]---> Sorter-cost:  937     Base: 2 2 2 2 2 2 2 2 2
c ---[1480]---> Adder-cost: 96   maxlim: 12287   bits: 15/14
c ---[1478]---> Adder-cost: 136   maxlim: 15103   bits: 15/14
c ---[1476]---> Adder-cost: 206   maxlim: 15871   bits: 15/14
c ---[1474]---> Adder-cost: 84   maxlim: 9343   bits: 14/14
c ---[1472]---> Adder-cost: 132   maxlim: 13695   bits: 15/14
c ---[1470]---> Adder-cost: 172   maxlim: 16255   bits: 15/14
c ---[1468]---> Sorter-cost: 1338     Base: 2 2 2 2 2 2 2 2
c ---[1466]---> Adder-cost: 104   maxlim: 12671   bits: 15/14
c ---[1465]---> BDD-cost:    2
c ---[1463]---> Adder-cost: 168   maxlim: 15231   bits: 15/14
c ---[1461]---> Adder-cost: 166   maxlim: 15999   bits: 15/14
c ---[1459]---> Sorter-cost:  338     Base: 2 2 2 2 2 2 2 2 2 2
c ---[1457]---> Adder-cost: 84   maxlim: 9727   bits: 14/14
c ---[1455]---> Adder-cost: 130   maxlim: 13823   bits: 15/14
c ---[1453]---> Adder-cost: 164   maxlim: 16383   bits: 15/14
c ---[1451]---> Adder-cost: 134   maxlim: 13055   bits: 15/14
c ---[1449]---> Adder-cost: 126   maxlim: 15359   bits: 15/14
c ---[1447]---> Adder-cost: 136   maxlim: 15743   bits: 15/14
c ---[1445]---> Sorter-cost:  767     Base: 2 2 2 2 2 2 2 2 2
c ---[1442]---> Adder-cost: 82   maxlim: 10239   bits: 14/14
c ---[1440]---> Adder-cost: 124   maxlim: 14079   bits: 15/14
c ---[1438]---> Adder-cost: 170   maxlim: 16895   bits: 15/15
c ---[1436]---> Adder-cost: 112   maxlim: 13439   bits: 15/14
c ---[1434]---> Adder-cost: 128   maxlim: 15487   bits: 15/14
c ---[1432]---> Adder-cost: 152   maxlim: 15871   bits: 15/14
c ---[1430]---> Sorter-cost:  288     Base: 2 2 2 2 2 2 2 2 2 2
c ---[1428]---> Adder-cost: 74   maxlim: 10623   bits: 14/14
c ---[1426]---> Adder-cost: 144   maxlim: 14207   bits: 15/14
c ---[1424]---> Adder-cost: 154   maxlim: 17023   bits: 15/15
c ---[1423]---> BDD-cost:    2
c ---[1421]---> Adder-cost: 120   maxlim: 13823   bits: 15/14
c ---[1419]---> Adder-cost: 136   maxlim: 15615   bits: 15/14
c ---[1417]---> Adder-cost: 180   maxlim: 15615   bits: 15/14
c ---[1415]---> Sorter-cost:  316     Base: 2 2 2 2 2 2 2 2 2 2
c ---[1413]---> Adder-cost: 86   maxlim: 11007   bits: 14/14
c ---[1411]---> Adder-cost: 138   maxlim: 14335   bits: 15/14
c ---[1409]---> Adder-cost: 162   maxlim: 17151   bits: 15/15
c ---[1407]---> BDD-cost:   97
c ---[1405]---> Adder-cost: 114   maxlim: 14079   bits: 15/14
c ---[1403]---> Adder-cost: 138   maxlim: 15615   bits: 15/14
c ---[1400]---> Adder-cost: 84   maxlim: 11391   bits: 14/14
c ---[1398]---> Adder-cost: 124   maxlim: 14463   bits: 15/14
c ---[1396]---> Adder-cost: 148   maxlim: 17279   bits: 15/15
c ---[1394]---> Sorter-cost:  493     Base: 2 2 2 2 2 2 2 2 2
c ---[1392]---> Adder-cost: 110   maxlim: 14207   bits: 15/14
c ---[1390]---> Adder-cost: 126   maxlim: 15487   bits: 15/14
c ---[1388]---> Adder-cost: 94   maxlim: 11775   bits: 15/14
c ---[1386]---> Adder-cost: 126   maxlim: 14591   bits: 15/14
c ---[1384]---> Adder-cost: 154   maxlim: 17407   bits: 15/15
c ---[1382]---> Sorter-cost:  685     Base: 2 2 2 2 2 2 2 2 2
c ---[1381]---> BDD-cost:    1
c ---[1379]---> Adder-cost: 112   maxlim: 14335   bits: 15/14
c ---[1377]---> Adder-cost: 116   maxlim: 15359   bits: 15/14
c ---[1375]---> Adder-cost: 110   maxlim: 12031   bits: 15/14
c ---[1373]---> Adder-cost: 130   maxlim: 14591   bits: 15/14
c ---[1371]---> Adder-cost: 250   maxlim: 17023   bits: 15/15
c ---[1369]---> Sorter-cost:  827     Base: 2 2 2 2 2 2 2 2 2
c ---[1367]---> Adder-cost: 108   maxlim: 14463   bits: 15/14
c ---[1365]---> Adder-cost: 146   maxlim: 15487   bits: 15/14
c ---[1363]---> Adder-cost: 98   maxlim: 12671   bits: 15/14
c ---[1361]---> Adder-cost: 170   maxlim: 14975   bits: 15/14
c ---[1359]---> Sorter-cost:  733     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1355]---> Sorter-cost: 1308     Base: 2 2 2 2 2 2 2 2
c ---[1353]---> Adder-cost: 106   maxlim: 14591   bits: 15/14
c ---[1351]---> Adder-cost: 116   maxlim: 15359   bits: 15/14
c ---[1349]---> Adder-cost: 244   maxlim: 13823   bits: 15/14
c ---[1347]---> Sorter-cost:  902     Base: 2 2 2 2 2 2 2 2
c ---[1345]---> Adder-cost: 178   maxlim: 9983   bits: 15/14
c ---[1343]---> Adder-cost: 140   maxlim: 12543   bits: 15/14
c ---[1341]---> Sorter-cost:  540     Base: 2 2 2 2 2 2 2 2 2
c ---[1339]---> Adder-cost: 244   maxlim: 13823   bits: 15/14
c ---[1337]---> Sorter-cost:  792     Base: 2 2 2 2 2 2 2 2 2
c ---[1336]---> BDD-cost:    2
c ---[1334]---> Adder-cost: 178   maxlim: 9983   bits: 15/14
c ---[1332]---> Adder-cost: 140   maxlim: 12543   bits: 15/14
c ---[1330]---> Sorter-cost:  592     Base: 2 2 2 2 2 2 2 2 2
c ---[1329]---> BDD-cost:   84
c ---[1328]---> BDD-cost:   83
c ---[1327]---> BDD-cost:   84
c ---[1326]---> BDD-cost:   84
c ---[1325]---> BDD-cost:   83
c ---[1324]---> BDD-cost:   88
c ---[1323]---> BDD-cost:   87
c ---[1321]---> BDD-cost:   88
c ---[1320]---> BDD-cost:   88
c ---[1319]---> BDD-cost:   87
c ---[1318]---> Sorter-cost:  620     Base: 2 2 2 2 2 2 2 2 2 2
c ---[1317]---> Sorter-cost:  685     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1311]---> BDD-cost:    2
c ---[1289]---> BDD-cost:    1
c ---[1267]---> BDD-cost:    2
c ---[1245]---> BDD-cost:    8
c ---[1234]---> BDD-cost:    8
c ---[1222]---> BDD-cost:    8
c ---[1212]---> BDD-cost:   21
c ---[1210]---> BDD-cost:   23
c ---[1206]---> BDD-cost:   21
c ---[1200]---> BDD-cost:    8
c ---[1187]---> BDD-cost:   21
c ---[1186]---> BDD-cost:   15
c ---[1184]---> BDD-cost:   87
c ---[1183]---> BDD-cost:   84
c ---[1182]---> BDD-cost:   54
c ---[1181]---> BDD-cost:   42
c ---[1179]---> BDD-cost:   24
c ---[1178]---> BDD-cost:    2
c ---[1175]---> BDD-cost:   71
c ---[1174]---> BDD-cost:   54
c ---[1173]---> BDD-cost:   58
c ---[1172]---> BDD-cost:   60
c ---[1171]---> BDD-cost:   25
c ---[1170]---> BDD-cost:   17
c ---[1169]---> BDD-cost:   19
c ---[1168]---> BDD-cost:   17
c ---[1166]---> BDD-cost:   88
c ---[1165]---> BDD-cost:   55
c ---[1164]---> BDD-cost:   66
c ---[1163]---> BDD-cost:   54
c ---[1156]---> BDD-cost:    1
c ---[1134]---> BDD-cost:    1
c ---[1111]---> BDD-cost:    1
c ---[1089]---> BDD-cost:    8
c ---[1067]---> BDD-cost:    8
c ---[1047]---> BDD-cost:    9
c ---[1045]---> BDD-cost:    1
c ---[1037]---> BDD-cost:   21
c ---[1033]---> BDD-cost:    0
c ---[1032]---> BDD-cost:    0
c ---[1031]---> BDD-cost:   38
c ---[1030]---> BDD-cost:    0
c ---[1028]---> BDD-cost:   27
c ---[1027]---> BDD-cost:    0
c ---[1026]---> BDD-cost:   23
c ---[1024]---> BDD-cost:    0
c ---[1023]---> BDD-cost:    2
c ---[1022]---> BDD-cost:    0
c ---[1021]---> BDD-cost:    0
c ---[1020]---> BDD-cost:    0
c ---[1019]---> BDD-cost:    0
c ---[1018]---> BDD-cost:   22
c ---[1017]---> BDD-cost:    0
c ---[1016]---> BDD-cost:    1
c ---[1014]---> BDD-cost:    2
c ---[1012]---> BDD-cost:    1
c ---[1010]---> BDD-cost:    2
c ---[1008]---> BDD-cost:    2
c ---[1006]---> BDD-cost:    1
c ---[1003]---> BDD-cost:    2
c ---[1001]---> BDD-cost:    1
c ---[ 999]---> BDD-cost:    2
c ---[ 997]---> BDD-cost:    8
c ---[ 995]---> BDD-cost:    2
c ---[ 994]---> BDD-cost:    2
c ---[ 992]---> BDD-cost:    1
c ---[ 990]---> BDD-cost:    1
c ---[ 988]---> BDD-cost:    1
c ---[ 986]---> BDD-cost:    8
c ---[ 984]---> BDD-cost:    8
c ---[ 981]---> BDD-cost:    8
c ---[ 979]---> BDD-cost:    1
c ---[ 977]---> BDD-cost:    2
c ---[ 975]---> BDD-cost:    2
c ---[ 973]---> BDD-cost:    2
c ---[ 972]---> BDD-cost:    2
c ---[ 970]---> BDD-cost:    1
c ---[ 968]---> BDD-cost:    2
c ---[ 966]---> BDD-cost:    2
c ---[ 964]---> BDD-cost:    1
c ---[ 962]---> BDD-cost:    2
c ---[ 959]---> BDD-cost:    2
c ---[ 957]---> BDD-cost:    1
c ---[ 955]---> BDD-cost:    2
c ---[ 953]---> BDD-cost:    8
c ---[ 951]---> BDD-cost:    8
c ---[ 950]---> BDD-cost:    2
c ---[ 948]---> BDD-cost:    8
c ---[ 946]---> BDD-cost:    8
c ---[ 944]---> BDD-cost:    1
c ---[ 942]---> BDD-cost:    1
c ---[ 940]---> BDD-cost:    1
c ---[ 938]---> Adder-cost: 1246   maxlim: 131071   bits: 18/17
c ---[ 935]---> BDD-cost:    6
c ---[ 933]---> BDD-cost:    8
c ---[ 931]---> BDD-cost:    8
c ---[ 929]---> BDD-cost:    1
c ---[ 927]---> BDD-cost:    2
c ---[ 926]---> BDD-cost:    2
c ---[ 924]---> BDD-cost:    2
c ---[ 922]---> BDD-cost:    2
c ---[ 920]---> BDD-cost:    1
c ---[ 918]---> BDD-cost:    2
c ---[ 916]---> BDD-cost:    2
c ---[ 913]---> BDD-cost:    1
c ---[ 911]---> BDD-cost:    2
c ---[ 909]---> BDD-cost:    2
c ---[ 907]---> BDD-cost:    1
c ---[ 905]---> BDD-cost:    2
c ---[ 904]---> BDD-cost:    1
c ---[ 902]---> BDD-cost:    1
c ---[ 900]---> BDD-cost:    2
c ---[ 898]---> BDD-cost:    8
c ---[ 896]---> BDD-cost:    2
c ---[ 894]---> BDD-cost:    2
c ---[ 891]---> BDD-cost:    1
c ---[ 889]---> BDD-cost:    1
c ---[ 887]---> BDD-cost:    8
c ---[ 885]---> BDD-cost:    8
c ---[ 883]---> BDD-cost:    1
c ---[ 882]---> BDD-cost:    2
c ---[ 880]---> BDD-cost:    2
c ---[ 878]---> BDD-cost:    2
c ---[ 876]---> BDD-cost:    1
c ---[ 874]---> BDD-cost:    2
c ---[ 872]---> BDD-cost:    1
c ---[ 869]---> BDD-cost:    2
c ---[ 867]---> BDD-cost:    2
c ---[ 865]---> BDD-cost:    8
c ---[ 863]---> BDD-cost:    2
c ---[ 861]---> BDD-cost:    2
c ---[ 860]---> BDD-cost:    2
c ---[ 858]---> BDD-cost:    1
c ---[ 856]---> BDD-cost:    1
c ---[ 854]---> BDD-cost:    8
c ---[ 852]---> BDD-cost:    8
c ---[ 850]---> BDD-cost:    1
c ---[ 847]---> BDD-cost:    2
c ---[ 845]---> BDD-cost:    2
c ---[ 843]---> BDD-cost:    1
c ---[ 841]---> BDD-cost:    2
c ---[ 839]---> BDD-cost:    1
c ---[ 838]---> BDD-cost:    2
c ---[ 836]---> BDD-cost:    2
c ---[ 834]---> BDD-cost:    2
c ---[ 832]---> BDD-cost:    8
c ---[ 830]---> BDD-cost:    1
c ---[ 828]---> BDD-cost:    2
c ---[ 826]---> Adder-cost: 1776   maxlim: 524287   bits: 20/19
c ---[ 823]---> BDD-cost:    1
c ---[ 821]---> BDD-cost:    1
c ---[ 819]---> BDD-cost:    8
c ---[ 817]---> BDD-cost:    8
c ---[ 815]---> BDD-cost:    1
c ---[ 814]---> BDD-cost:    2
c ---[ 812]---> BDD-cost:    2
c ---[ 810]---> BDD-cost:    2
c ---[ 808]---> BDD-cost:    1
c ---[ 806]---> BDD-cost:    2
c ---[ 804]---> BDD-cost:    1
c ---[ 801]---> BDD-cost:    2
c ---[ 799]---> BDD-cost:    2
c ---[ 797]---> BDD-cost:    8
c ---[ 795]---> BDD-cost:    1
c ---[ 793]---> BDD-cost:    2
c ---[ 792]---> BDD-cost:    1
c ---[ 790]---> BDD-cost:    1
c ---[ 788]---> BDD-cost:    6
c ---[ 786]---> BDD-cost:    8
c ---[ 784]---> BDD-cost:    8
c ---[ 782]---> BDD-cost:    1
c ---[ 779]---> BDD-cost:    2
c ---[ 777]---> BDD-cost:    2
c ---[ 775]---> BDD-cost:    1
c ---[ 773]---> BDD-cost:    2
c ---[ 771]---> BDD-cost:    1
c ---[ 770]---> BDD-cost:    2
c ---[ 768]---> BDD-cost:    2
c ---[ 766]---> BDD-cost:    8
c ---[ 764]---> BDD-cost:    8
c ---[ 762]---> BDD-cost:    2
c ---[ 760]---> BDD-cost:    2
c ---[ 757]---> BDD-cost:    1
c ---[ 755]---> BDD-cost:    8
c ---[ 753]---> BDD-cost:    8
c ---[ 751]---> BDD-cost:    8
c ---[ 749]---> BDD-cost:    1
c ---[ 748]---> BDD-cost:    2
c ---[ 746]---> BDD-cost:    2
c ---[ 744]---> BDD-cost:    2
c ---[ 742]---> BDD-cost:    2
c ---[ 740]---> BDD-cost:    2
c ---[ 738]---> BDD-cost:    2
c ---[ 735]---> BDD-cost:    1
c ---[ 733]---> BDD-cost:    2
c ---[ 731]---> BDD-cost:    1
c ---[ 729]---> BDD-cost:    2
c ---[ 727]---> BDD-cost:    2
c ---[ 726]---> BDD-cost:    1
c ---[ 724]---> BDD-cost:    2
c ---[ 722]---> BDD-cost:    2
c ---[ 720]---> BDD-cost:    8
c ---[ 718]---> BDD-cost:    8
c ---[ 714]---> Adder-cost: 2784   maxlim: 2097151   bits: 22/21
c ---[ 702]---> BDD-cost:    2
c ---[ 689]---> BDD-cost:  299
c ---[ 685]---> BDD-cost:  244
c ---[ 680]---> BDD-cost:    2
c ---[ 677]---> BDD-cost:  330
c ---[ 673]---> BDD-cost:  464
c ---[ 672]---> BDD-cost:  137
c ---[ 667]---> BDD-cost:   61
c ---[ 666]---> BDD-cost:  323
c ---[ 665]---> BDD-cost:    4
c ---[ 663]---> BDD-cost:  142
c ---[ 662]---> BDD-cost:  367
c ---[ 661]---> BDD-cost:   95
c ---[ 658]---> BDD-cost:    2
c ---[ 656]---> BDD-cost:  147
c ---[ 653]---> BDD-cost:  174
c ---[ 652]---> BDD-cost:  284
c ---[ 641]---> BDD-cost:  180
c ---[ 640]---> BDD-cost:  296
c ---[ 636]---> BDD-cost:    1
c ---[ 633]---> BDD-cost:   72
c ---[ 630]---> BDD-cost:  233
c ---[ 629]---> BDD-cost:   72
c ---[ 626]---> BDD-cost:   51
c ---[ 622]---> BDD-cost:    0
c ---[ 620]---> BDD-cost:  275
c ---[ 619]---> BDD-cost:   69
c ---[ 616]---> BDD-cost:  150
c ---[ 614]---> BDD-cost:    2
c ---[ 610]---> BDD-cost:  331
c ---[ 609]---> BDD-cost:    4
c ---[ 606]---> BDD-cost:  185
c ---[ 601]---> BDD-cost:   31
c ---[ 599]---> BDD-cost:  262
c ---[ 595]---> BDD-cost:  147
c ---[ 592]---> BDD-cost:  147
c ---[ 591]---> BDD-cost:    1
c ---[ 589]---> BDD-cost:  191
c ---[ 569]---> BDD-cost:    2
c ---[ 557]---> BDD-cost:  182
c ---[ 547]---> BDD-cost:    2
c ---[ 545]---> BDD-cost:  125
c ---[ 541]---> BDD-cost:  208
c ---[ 534]---> BDD-cost:   43
c ---[ 531]---> BDD-cost:   61
c ---[ 530]---> BDD-cost:  161
c ---[ 525]---> BDD-cost:    8
c ---[ 520]---> BDD-cost:   68
c ---[ 503]---> BDD-cost:    2
c ---[ 498]---> BDD-cost:   44
c ---[ 494]---> BDD-cost:   30
c ---[ 492]---> BDD-cost:    2
c ---[ 487]---> BDD-cost:   68
c ---[ 483]---> BDD-cost:   41
c ---[ 480]---> BDD-cost:    1
c ---[ 477]---> BDD-cost:   67
c ---[ 473]---> BDD-cost:   53
c ---[ 467]---> BDD-cost:   64
c ---[ 463]---> BDD-cost:   36
c ---[ 458]---> BDD-cost:    1
c ---[ 457]---> BDD-cost:   73
c ---[ 451]---> BDD-cost:   12
c ---[ 450]---> BDD-cost:   12
c ---[ 449]---> BDD-cost:   12
c ---[ 448]---> BDD-cost:   12
c ---[ 446]---> BDD-cost:   14
c ---[ 445]---> BDD-cost:   14
c ---[ 444]---> BDD-cost:   12
c ---[ 443]---> BDD-cost:   13
c ---[ 442]---> BDD-cost:   12
c ---[ 441]---> BDD-cost:    1
c ---[ 440]---> BDD-cost:   14
c ---[ 439]---> BDD-cost:   14
c ---[ 438]---> BDD-cost:   12
c ---[ 437]---> BDD-cost:   13
c ---[ 436]---> BDD-cost:   13
c ---[ 434]---> BDD-cost:   13
c ---[ 433]---> BDD-cost:   12
c ---[ 431]---> BDD-cost:   12
c ---[ 430]---> BDD-cost:    8
c ---[ 429]---> BDD-cost:   14
c ---[ 428]---> BDD-cost:   12
c ---[ 427]---> BDD-cost:   15
c ---[ 426]---> BDD-cost:   14
c ---[ 425]---> BDD-cost:   13
c ---[ 423]---> BDD-cost:   15
c ---[ 421]---> BDD-cost:   13
c ---[ 420]---> BDD-cost:   14
c ---[ 419]---> BDD-cost:   14
c ---[ 417]---> BDD-cost:    8
c ---[ 415]---> BDD-cost:   15
c ---[ 414]---> BDD-cost:   12
c ---[ 410]---> BDD-cost:   12
c ---[ 408]---> BDD-cost:   15
c ---[ 407]---> BDD-cost:   13
c ---[ 405]---> BDD-cost:    8
c ---[ 404]---> BDD-cost:   13
c ---[ 403]---> BDD-cost:   13
c ---[ 402]---> BDD-cost:   15
c ---[ 401]---> BDD-cost:   14
c ---[ 400]---> BDD-cost:   14
c ---[ 399]---> BDD-cost:   13
c ---[ 396]---> BDD-cost:   14
c ---[ 395]---> BDD-cost:   13
c ---[ 394]---> BDD-cost:   15
c ---[ 393]---> BDD-cost:   12
c ---[ 392]---> BDD-cost:    1
c ---[ 391]---> BDD-cost:   11
c ---[ 390]---> BDD-cost:   14
c ---[ 389]---> BDD-cost:   15
c ---[ 388]---> BDD-cost:   13
c ---[ 385]---> BDD-cost:   15
c ---[ 384]---> BDD-cost:   15
c ---[ 383]---> BDD-cost:   14
c ---[ 382]---> BDD-cost:   14
c ---[ 381]---> BDD-cost:   13
c ---[ 380]---> BDD-cost:    2
c ---[ 379]---> BDD-cost:    8
c ---[ 378]---> BDD-cost:    9
c ---[ 377]---> BDD-cost:    9
c ---[ 376]---> BDD-cost:    8
c ---[ 374]---> BDD-cost:    9
c ---[ 373]---> BDD-cost:    9
c ---[ 371]---> BDD-cost:    9
c ---[ 370]---> BDD-cost:   10
c ---[ 369]---> BDD-cost:    8
c ---[ 368]---> BDD-cost:    2
c ---[ 367]---> BDD-cost:   10
c ---[ 366]---> BDD-cost:   10
c ---[ 365]---> BDD-cost:   10
c ---[ 363]---> BDD-cost:    9
c ---[ 361]---> BDD-cost:    8
c ---[ 360]---> BDD-cost:    7
c ---[ 359]---> BDD-cost:   10
c ---[ 358]---> BDD-cost:   11
c ---[ 357]---> BDD-cost:    2
c ---[ 356]---> BDD-cost:    8
c ---[ 355]---> BDD-cost:   11
c ---[ 354]---> BDD-cost:   10
c ---[ 352]---> BDD-cost:    9
c ---[ 351]---> BDD-cost:    1
c ---[ 349]---> BDD-cost:    9
c ---[ 348]---> BDD-cost:   11
c ---[ 347]---> BDD-cost:    8
c ---[ 346]---> BDD-cost:   10
c ---[ 345]---> BDD-cost:    9
c ---[ 344]---> BDD-cost:    1
c ---[ 343]---> BDD-cost:   10
c ---[ 342]---> BDD-cost:   10
c ---[ 341]---> BDD-cost:    6
c ---[ 340]---> BDD-cost:    6
c ---[ 339]---> BDD-cost:    9
c ---[ 337]---> BDD-cost:    8
c ---[ 336]---> BDD-cost:   10
c ---[ 335]---> BDD-cost:    9
c ---[ 334]---> BDD-cost:    9
c ---[ 333]---> BDD-cost:   10
c ---[ 332]---> BDD-cost:    2
c ---[ 331]---> BDD-cost:    5
c ---[ 330]---> BDD-cost:   10
c ---[ 329]---> BDD-cost:   10
c ---[ 328]---> BDD-cost:   10
c ---[ 327]---> BDD-cost:    8
c ---[ 325]---> BDD-cost:    6
c ---[ 323]---> BDD-cost:    9
c ---[ 321]---> BDD-cost:    8
c ---[ 320]---> BDD-cost:    8
c ---[ 319]---> BDD-cost:    2
c ---[ 316]---> BDD-cost:    6
c ---[ 315]---> BDD-cost:    9
c ---[ 312]---> BDD-cost:    8
c ---[ 311]---> BDD-cost:   10
c ---[ 310]---> BDD-cost:    8
c ---[ 309]---> BDD-cost:    8
c ---[ 308]---> BDD-cost:    1
c ---[ 307]---> BDD-cost:   71
c ---[ 306]---> BDD-cost:  113
c ---[ 305]---> BDD-cost:  134
c ---[ 304]---> BDD-cost:  207
c ---[ 303]---> BDD-cost:  143
c ---[ 302]---> BDD-cost:  157
c ---[ 300]---> BDD-cost:  217
c ---[ 299]---> BDD-cost:  143
c ---[ 298]---> BDD-cost:  147
c ---[ 297]---> BDD-cost:  187
c ---[ 296]---> BDD-cost:  106
c ---[ 295]---> BDD-cost:   63
c ---[ 294]---> BDD-cost:   58
c ---[ 293]---> BDD-cost:   91
c ---[ 292]---> BDD-cost:  131
c ---[ 291]---> BDD-cost:   90
c ---[ 290]---> BDD-cost:    2
c ---[ 289]---> BDD-cost:  105
c ---[ 288]---> BDD-cost:  141
c ---[ 287]---> BDD-cost:   90
c ---[ 286]---> BDD-cost:   95
c ---[ 285]---> BDD-cost:  111
c ---[ 284]---> BDD-cost:   55
c ---[ 283]---> BDD-cost:   66
c ---[ 282]---> BDD-cost:   93
c ---[ 281]---> BDD-cost:  165
c ---[ 280]---> BDD-cost:   73
c ---[ 279]---> BDD-cost:    1
c ---[ 278]---> BDD-cost:    1
c ---[ 277]---> BDD-cost:    1
c ---[ 276]---> BDD-cost:    1
c ---[ 275]---> BDD-cost:    1
c ---[ 274]---> BDD-cost:    1
c ---[ 273]---> BDD-cost:    1
c ---[ 272]---> BDD-cost:    1
c ---[ 271]---> BDD-cost:    1
c ---[ 270]---> BDD-cost:    1
c ---[ 269]---> BDD-cost:    1
c ---[ 268]---> BDD-cost:    1
c ---[ 267]---> BDD-cost:    1
c ---[ 266]---> BDD-cost:    1
c ---[ 265]---> BDD-cost:    1
c ---[ 264]---> BDD-cost:    1
c ---[ 263]---> BDD-cost:    1
c ---[ 262]---> BDD-cost:    1
c ---[ 261]---> BDD-cost:    1
c ---[ 260]---> BDD-cost:    1
c ---[ 259]---> BDD-cost:    1
c ---[ 258]---> BDD-cost:    1
c ---[ 257]---> BDD-cost:    1
c ---[ 256]---> BDD-cost:    1
c ---[ 255]---> BDD-cost:    1
c ---[ 254]---> BDD-cost:    1
c ---[ 253]---> BDD-cost:    1
c ---[ 252]---> BDD-cost:   76
c ---[ 251]---> BDD-cost:   80
c ---[ 250]---> BDD-cost:   64
c ---[ 249]---> BDD-cost:   13
c ---[ 248]---> BDD-cost:   41
c ---[ 247]---> BDD-cost:   48
c ---[ 246]---> BDD-cost:   52
c ---[ 245]---> BDD-cost:   40
c ---[ 244]---> BDD-cost:    1
c ---[ 243]---> BDD-cost:   60
c ---[ 242]---> BDD-cost:   68
c ---[ 241]---> BDD-cost:   72
c ---[ 240]---> BDD-cost:    1
c ---[ 239]---> BDD-cost:   52
c ---[ 238]---> BDD-cost:    1
c ---[ 237]---> BDD-cost:   28
c ---[ 236]---> BDD-cost:    5
c ---[ 235]---> BDD-cost:   25
c ---[ 234]---> BDD-cost:   48
c ---[ 233]---> BDD-cost:   52
c ---[ 232]---> BDD-cost:   44
c ---[ 231]---> BDD-cost:   29
c ---[ 230]---> BDD-cost:   32
c ---[ 229]---> BDD-cost:   28
c ---[ 228]---> BDD-cost:   20
c ---[ 227]---> BDD-cost:   21
c ---[ 226]---> BDD-cost:   29
c ---[ 225]---> BDD-cost:   28
c ---[ 224]---> BDD-cost:   29
c ---[ 223]---> BDD-cost:   32
c ---[ 222]---> BDD-cost:   29
c ---[ 221]---> BDD-cost:   28
c ---[ 220]---> BDD-cost:   41
c ---[ 219]---> BDD-cost:   44
c ---[ 218]---> BDD-cost:   36
c ---[ 217]---> BDD-cost:   46
c ---[ 216]---> BDD-cost:   30
c ---[ 215]---> BDD-cost:   32
c ---[ 214]---> BDD-cost:   44
c ---[ 213]---> BDD-cost:   28
c ---[ 212]---> BDD-cost:   20
c ---[ 211]---> BDD-cost:   30
c ---[ 210]---> BDD-cost:   32
c ---[ 209]---> BDD-cost:   36
c ---[ 208]---> BDD-cost:   80
c ---[ 207]---> BDD-cost:   52
c ---[ 206]---> BDD-cost:    9
c ---[ 205]---> BDD-cost:   72
c ---[ 204]---> BDD-cost:   40
c ---[ 203]---> BDD-cost:   40
c ---[ 202]---> BDD-cost:   40
c ---[ 201]---> BDD-cost:   17
c ---[ 200]---> BDD-cost:   52
c ---[ 199]---> BDD-cost:    9
c ---[ 198]---> BDD-cost:   28
c ---[ 197]---> BDD-cost:   21
c ---[ 196]---> BDD-cost:   29
c ---[ 195]---> BDD-cost:   30
c ---[ 194]---> BDD-cost:   15
c ---[ 193]---> BDD-cost:   14
c ---[ 192]---> BDD-cost:   28
c ---[ 191]---> BDD-cost:   22
c ---[ 190]---> BDD-cost:   25
c ---[ 189]---> BDD-cost:    1
c ---[ 188]---> BDD-cost:    1
c ---[ 187]---> BDD-cost:    1
c ---[ 186]---> BDD-cost:    1
c ---[ 185]---> BDD-cost:    1
c ---[ 184]---> BDD-cost:    1
c ---[ 183]---> BDD-cost:    1
c ---[ 182]---> BDD-cost:    1
c ---[ 181]---> BDD-cost:    1
c ---[ 180]---> BDD-cost:    1
c ---[ 179]---> BDD-cost:    1
c ---[ 178]---> BDD-cost:    1
c ---[ 177]---> BDD-cost:    1
c ---[ 176]---> BDD-cost:    1
c ---[ 175]---> BDD-cost:    1
c ---[ 174]---> BDD-cost:    1
c ---[ 173]---> BDD-cost:    1
c ---[ 172]---> BDD-cost:    1
c ---[ 171]---> BDD-cost:    1
c ---[ 170]---> BDD-cost:    1
c ---[ 169]---> BDD-cost:    1
c ---[ 168]---> BDD-cost:    1
c ---[ 167]---> BDD-cost:    1
c ---[ 166]---> BDD-cost:   48
c ---[ 165]---> BDD-cost:    1
c ---[ 164]---> BDD-cost:    1
c ---[ 163]---> BDD-cost:    1
c ---[ 162]---> BDD-cost:    1
c ---[ 161]---> BDD-cost:    1
c ---[ 160]---> BDD-cost:    1
c ---[ 159]---> BDD-cost:    1
c ---[ 158]---> BDD-cost:    1
c ---[ 157]---> BDD-cost:   40
c ---[ 156]---> BDD-cost:    1
c ---[ 155]---> BDD-cost:    1
c ---[ 154]---> BDD-cost:    1
c ---[ 153]---> BDD-cost:    1
c ---[ 152]---> BDD-cost:    1
c ---[ 151]---> BDD-cost:    2
c ---[ 150]---> BDD-cost:    1
c ---[ 149]---> BDD-cost:   42
c ---[ 148]---> BDD-cost:   32
c ---[ 147]---> BDD-cost:    1
c ---[ 146]---> BDD-cost:   16
c ---[ 145]---> BDD-cost:    1
c ---[ 144]---> BDD-cost:   32
c ---[ 143]---> BDD-cost:    1
c ---[ 142]---> BDD-cost:    1
c ---[ 141]---> BDD-cost:    1
c ---[ 140]---> BDD-cost:    1
c ---[ 139]---> BDD-cost:    1
c ---[ 138]---> BDD-cost:    2
c ---[ 137]---> BDD-cost:    1
c ---[ 136]---> BDD-cost:    1
c ---[ 135]---> BDD-cost:    1
c ---[ 134]---> BDD-cost:   32
c ---[ 133]---> BDD-cost:   34
c ---[ 132]---> BDD-cost:   18
c ---[ 131]---> BDD-cost:   69
c ---[ 130]---> BDD-cost:   94
c ---[ 129]---> BDD-cost:  172
c ---[ 128]---> BDD-cost:    3
c ---[ 127]---> BDD-cost:  184
c ---[ 126]---> BDD-cost:  135
c ---[ 125]---> BDD-cost:  159
c ---[ 124]---> BDD-cost:    1
c ---[ 123]---> BDD-cost:   18
c ---[ 122]---> BDD-cost:  110
c ---[ 121]---> BDD-cost:  118
c ---[ 120]---> BDD-cost:    1
c ---[ 119]---> BDD-cost:    3
c ---[ 118]---> BDD-cost:  127
c ---[ 117]---> BDD-cost:   94
c ---[ 116]---> BDD-cost:    3
c ---[ 115]---> BDD-cost:    1
c ---[ 114]---> BDD-cost:   75
c ---[ 113]---> BDD-cost:  141
c ---[ 112]---> BDD-cost:    1
c ---[ 111]---> BDD-cost:    1
c ---[ 110]---> BDD-cost:   50
c ---[ 109]---> BDD-cost:    1
c ---[ 108]---> BDD-cost:    1
c ---[ 107]---> BDD-cost:   71
c ---[ 106]---> BDD-cost:    1
c ---[ 105]---> BDD-cost:    1
c ---[ 104]---> BDD-cost:  126
c ---[ 103]---> BDD-cost:    1
c ---[ 102]---> BDD-cost:    1
c ---[ 101]---> BDD-cost:    1
c ---[ 100]---> BDD-cost:    1
c ---[  99]---> BDD-cost:   62
c ---[  98]---> BDD-cost:    1
c ---[  97]---> BDD-cost:    1
c ---[  96]---> BDD-cost:    1
c ---[  95]---> BDD-cost:    1
c ---[  94]---> BDD-cost:   35
c ---[  93]---> BDD-cost:  115
c ---[  92]---> BDD-cost:    1
c ---[  91]---> BDD-cost:    2
c ---[  90]---> BDD-cost:    1
c ---[  89]---> BDD-cost:    1
c ---[  88]---> BDD-cost:   36
c ---[  87]---> BDD-cost:   20
c ---[  86]---> BDD-cost:    1
c ---[  85]---> BDD-cost:   20
c ---[  84]---> BDD-cost:    1
c ---[  83]---> BDD-cost:    1
c ---[  82]---> BDD-cost:   16
c ---[  81]---> BDD-cost:    1
c ---[  80]---> BDD-cost:   27
c ---[  79]---> BDD-cost:    1
c ---[  78]---> BDD-cost:   16
c ---[  77]---> BDD-cost:    1
c ---[  76]---> BDD-cost:    1
c ---[  75]---> BDD-cost:   27
c ---[  74]---> BDD-cost:    1
c ---[  73]---> BDD-cost:    1
c ---[  72]---> BDD-cost:    1
c ---[  71]---> BDD-cost:   26
c ---[  70]---> BDD-cost:    1
c ---[  69]---> BDD-cost:    1
c ---[  68]---> BDD-cost:    1
c ---[  67]---> BDD-cost:   84
c ---[  66]---> BDD-cost:    1
c ---[  65]---> BDD-cost:   28
c ---[  64]---> BDD-cost:   38
c ---[  63]---> BDD-cost:  169
c ---[  62]---> BDD-cost:    1
c ---[  61]---> BDD-cost:    1
c ---[  60]---> BDD-cost:    1
c ---[  59]---> BDD-cost:    1
c ---[  58]---> BDD-cost:   60
c ---[  57]---> BDD-cost:    1
c ---[  56]---> BDD-cost:    1
c ---[  55]---> BDD-cost:   62
c ---[  54]---> BDD-cost:    2
c ---[  53]---> BDD-cost:    1
c ---[  52]---> BDD-cost:    1
c ---[  51]---> BDD-cost:    2
c ---[  50]---> BDD-cost:    1
c ---[  49]---> BDD-cost:    1
c ---[  48]---> BDD-cost:  161
c ---[  47]---> BDD-cost:    2
c ---[  46]---> BDD-cost:    1
c ---[  45]---> BDD-cost:   42
c ---[  44]---> BDD-cost:    1
c ---[  43]---> BDD-cost:    1
c ---[  42]---> BDD-cost:    2
c ---[  41]---> BDD-cost:    1
c ---[  40]---> BDD-cost:    1
c ---[  39]---> BDD-cost:    2
c ---[  38]---> BDD-cost:    2
c ---[  37]---> BDD-cost:   49
c ---[  36]---> BDD-cost:   77
c ---[  35]---> BDD-cost:    2
c ---[  34]---> BDD-cost:   40
c ---[  33]---> BDD-cost:    1
c ---[  32]---> BDD-cost:    1
c ---[  31]---> BDD-cost:   58
c ---[  30]---> BDD-cost:   13
c ---[  29]---> BDD-cost:    1
c ---[  28]---> BDD-cost:    1
c ---[  27]---> BDD-cost:    1
c ---[  26]---> BDD-cost:    1
c ---[  25]---> BDD-cost:   17
c ---[  24]---> BDD-cost:    1
c ---[  23]---> BDD-cost:    1
c ---[  22]---> BDD-cost:    1
c ---[  21]---> BDD-cost:    1
c ---[  20]---> BDD-cost:   16
c ---[  19]---> BDD-cost:    1
c ---[  18]---> BDD-cost:    1
c ---[  17]---> BDD-cost:   22
c ---[  16]---> BDD-cost:   10
c ---[  15]---> BDD-cost:   11
c ---[  14]---> BDD-cost:   12
c ---[  13]---> BDD-cost:   10
c ---[  12]---> BDD-cost:   11
c ---[  11]---> BDD-cost:   12
c ---[  10]---> BDD-cost:    6
c ---[   9]---> BDD-cost:   11
c ---[   8]---> BDD-cost:   11
c ---[   7]---> BDD-cost:    7
c ---[   6]---> BDD-cost:    5
c ---[   5]---> BDD-cost:    7
c ---[   4]---> BDD-cost:    5
c ---[   3]---> BDD-cost:    7
c ---[   2]---> BDD-cost:    5
c ---[   1]---> BDD-cost:    2
c ---[   0]---> BDD-cost:    6
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  296752   925023 |   98917       0        0     nan |  0.000 % |
c |       100 |  296580   924636 |  108808      98     1026    10.5 | 13.089 % |
c |       250 |  296542   924553 |  119689     244     2223     9.1 | 13.101 % |
c |       475 |  296272   923943 |  131658     464     4403     9.5 | 13.187 % |
c |       814 |  295430   922023 |  144824     783     7272     9.3 | 13.446 % |
c |      1322 |  295104   921215 |  159306    1274    11994     9.4 | 13.537 % |
c |      2082 |  289888   909184 |  175237    1936    19209     9.9 | 15.283 % |
c |      3221 |  289468   908046 |  192761    3055    30146     9.9 | 15.392 % |
c |      4929 |  288931   906701 |  212037    4704    49270    10.5 | 15.558 % |
c |      7491 |  285525   898830 |  233241    7120    72373    10.2 | 16.684 % |
c |     11335 |  283759   894575 |  256565   10840   151267    14.0 | 17.263 % |
c |     17101 |  282582   891489 |  282221   16488   264265    16.0 | 17.595 % |
c |     25750 |  281686   889057 |  310443   24967   462702    18.5 | 17.839 % |
c |     38724 |  280326   885456 |  341488   37808   841207    22.2 | 18.202 % |
c |     58186 |  279419   882963 |  375637   57179  1427826    25.0 | 18.428 % |
c |     87378 |  277695   877540 |  413200   85781  2393416    27.9 | 18.655 % |
c |    131168 |  274590   868954 |  454520  128673  4031962    31.3 | 19.371 % |
c |    196854 |  273650   865999 |  499973  194049  7306135    37.7 | 19.531 % |

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/9058/stat): 9058 (minisat+_script) R 9057 9058 6847 0 -1 0 19 0 0 0 0 0 0 0 22 0 1 0 1797224201 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 1 0 0
Raw data (/proc/9058/statm): 174 3 169 147 0 27 0
[pid=9058] 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=9059
New process pid=9060
New process pid=9061
execve syscall for /bin/sed executable
One traced child (pid=9060) 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=9061) exited with status: 0
One traced child (pid=9059) exited with status: 0
New process pid=9062
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc4/normalized-mps-v2-13-7-roll3000.opb

[startup+10.0034 s]
Raw data (loadavg): 0.71 0.92 0.89 2/57 9062
Raw data (/proc/9058/stat): 9058 (minisat+_script) S 9057 9058 6847 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797224201 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9058/statm): 531 226 485 147 0 384 0
[pid=9058] vsize: 2124
Raw data (/proc/9062/stat): 9062 (minisat+_64-bit) R 9058 9058 6847 0 -1 0 8672 0 0 0 922 38 0 0 25 0 1 0 1797224205 38981632 8170 4294967295 134512640 135094434 3221224432 3221223092 134553487 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9062/statm): 9517 8170 145 145 0 9372 0
[pid=9062] vsize: 38068
Current children cumulated CPU time (s) 9.61
Current children cumulated vsize (Kb) 40192

[startup+20.0044 s]
Raw data (loadavg): 0.75 0.92 0.90 2/57 9062
Raw data (/proc/9058/stat): 9058 (minisat+_script) S 9057 9058 6847 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797224201 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9058/statm): 531 226 485 147 0 384 0
[pid=9058] vsize: 2124
Raw data (/proc/9062/stat): 9062 (minisat+_64-bit) R 9058 9058 6847 0 -1 0 8712 0 0 0 1921 39 0 0 25 0 1 0 1797224205 39145472 8210 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9062/statm): 9557 8210 145 145 0 9412 0
[pid=9062] vsize: 38228
Current children cumulated CPU time (s) 19.61
Current children cumulated vsize (Kb) 40352

[startup+30.0053 s]
Raw data (loadavg): 0.79 0.92 0.90 2/57 9062
Raw data (/proc/9058/stat): 9058 (minisat+_script) S 9057 9058 6847 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797224201 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9058/statm): 531 226 485 147 0 384 0
[pid=9058] vsize: 2124
Raw data (/proc/9062/stat): 9062 (minisat+_64-bit) R 9058 9058 6847 0 -1 0 8749 0 0 0 2920 39 0 0 25 0 1 0 1797224205 39301120 8247 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9062/statm): 9595 8247 145 145 0 9450 0
[pid=9062] vsize: 38380
Current children cumulated CPU time (s) 29.6
Current children cumulated vsize (Kb) 40504

[startup+40.0061 s]
Raw data (loadavg): 0.82 0.93 0.90 2/57 9062
Raw data (/proc/9058/stat): 9058 (minisat+_script) S 9057 9058 6847 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797224201 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9058/statm): 531 226 485 147 0 384 0
[pid=9058] vsize: 2124
Raw data (/proc/9062/stat): 9062 (minisat+_64-bit) R 9058 9058 6847 0 -1 0 8796 0 0 0 3919 40 0 0 25 0 1 0 1797224205 39501824 8294 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9062/statm): 9644 8294 145 145 0 9499 0
[pid=9062] vsize: 38576
Current children cumulated CPU time (s) 39.6
Current children cumulated vsize (Kb) 40700

[startup+50.008 s]
Raw data (loadavg): 0.85 0.93 0.90 2/57 9062
Raw data (/proc/9058/stat): 9058 (minisat+_script) S 9057 9058 6847 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797224201 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9058/statm): 531 226 485 147 0 384 0
[pid=9058] vsize: 2124
Raw data (/proc/9062/stat): 9062 (minisat+_64-bit) R 9058 9058 6847 0 -1 0 8877 0 0 0 4917 41 0 0 25 0 1 0 1797224205 39821312 8375 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9062/statm): 9722 8375 145 145 0 9577 0
[pid=9062] vsize: 38888
Current children cumulated CPU time (s) 49.59
Current children cumulated vsize (Kb) 41012

[startup+60.0089 s]
Raw data (loadavg): 0.87 0.93 0.90 2/57 9062
Raw data (/proc/9058/stat): 9058 (minisat+_script) S 9057 9058 6847 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797224201 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9058/statm): 531 226 485 147 0 384 0
[pid=9058] vsize: 2124
Raw data (/proc/9062/stat): 9062 (minisat+_64-bit) R 9058 9058 6847 0 -1 0 8971 0 0 0 5915 42 0 0 25 0 1 0 1797224205 40173568 8469 4294967295 134512640 135094434 3221224432 3221223104 134555568 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9062/statm): 9808 8469 145 145 0 9663 0
[pid=9062] vsize: 39232
Current children cumulated CPU time (s) 59.58
Current children cumulated vsize (Kb) 41356

[startup+70.0098 s]
Raw data (loadavg): 0.89 0.93 0.90 2/57 9062
Raw data (/proc/9058/stat): 9058 (minisat+_script) S 9057 9058 6847 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797224201 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9058/statm): 531 226 485 147 0 384 0
[pid=9058] vsize: 2124
Raw data (/proc/9062/stat): 9062 (minisat+_64-bit) R 9058 9058 6847 0 -1 0 9065 0 0 0 6912 44 0 0 25 0 1 0 1797224205 40611840 8563 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9062/statm): 9915 8563 145 145 0 9770 0
[pid=9062] vsize: 39660
Current children cumulated CPU time (s) 69.57
Current children cumulated vsize (Kb) 41784

[startup+80.0117 s]
Raw data (loadavg): 0.91 0.93 0.90 2/57 9062
Raw data (/proc/9058/stat): 9058 (minisat+_script) S 9057 9058 6847 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797224201 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9058/statm): 531 226 485 147 0 384 0
[pid=9058] vsize: 2124
Raw data (/proc/9062/stat): 9062 (minisat+_64-bit) R 9058 9058 6847 0 -1 0 9165 0 0 0 7910 45 0 0 25 0 1 0 1797224205 41009152 8663 4294967295 134512640 135094434 3221224432 3221223088 134557879 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9062/statm): 10012 8663 145 145 0 9867 0
[pid=9062] vsize: 40048
Current children cumulated CPU time (s) 79.56
Current children cumulated vsize (Kb) 42172

[startup+90.0126 s]
Raw data (loadavg): 0.92 0.94 0.90 2/57 9062
Raw data (/proc/9058/stat): 9058 (minisat+_script) S 9057 9058 6847 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797224201 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9058/statm): 531 226 485 147 0 384 0
[pid=9058] vsize: 2124
Raw data (/proc/9062/stat): 9062 (minisat+_64-bit) R 9058 9058 6847 0 -1 0 9249 0 0 0 8908 46 0 0 25 0 1 0 1797224205 41340928 8747 4294967295 134512640 135094434 3221224432 3221223088 134557846 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9062/statm): 10093 8747 145 145 0 9948 0
[pid=9062] vsize: 40372
Current children cumulated CPU time (s) 89.55
Current children cumulated vsize (Kb) 42496

[startup+100.014 s]
Raw data (loadavg): 0.93 0.94 0.90 2/57 9062
Raw data (/proc/9058/stat): 9058 (minisat+_script) S 9057 9058 6847 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797224201 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9058/statm): 531 226 485 147 0 384 0
[pid=9058] vsize: 2124
Raw data (/proc/9062/stat): 9062 (minisat+_64-bit) R 9058 9058 6847 0 -1 0 9332 0 0 0 9905 48 0 0 25 0 1 0 1797224205 41672704 8830 4294967295 134512640 135094434 3221224432 3221223124 134558984 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9062/statm): 10174 8830 145 145 0 10029 0
[pid=9062] vsize: 40696
Current children cumulated CPU time (s) 99.54
Current children cumulated vsize (Kb) 42820

[startup+110.015 s]
Raw data (loadavg): 0.94 0.94 0.90 2/57 9062
Raw data (/proc/9058/stat): 9058 (minisat+_script) S 9057 9058 6847 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797224201 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9058/statm): 531 226 485 147 0 384 0
[pid=9058] vsize: 2124
Raw data (/proc/9062/stat): 9062 (minisat+_64-bit) R 9058 9058 6847 0 -1 0 9417 0 0 0 10903 49 0 0 25 0 1 0 1797224205 42000384 8915 4294967295 134512640 135094434 3221224432 3221223056 134557598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9062/statm): 10254 8915 145 145 0 10109 0
[pid=9062] vsize: 41016
Current children cumulated CPU time (s) 109.53
Current children cumulated vsize (Kb) 43140

[startup+120.016 s]
Raw data (loadavg): 0.95 0.94 0.91 2/57 9062
Raw data (/proc/9058/stat): 9058 (minisat+_script) S 9057 9058 6847 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797224201 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9058/statm): 531 226 485 147 0 384 0
[pid=9058] vsize: 2124
Raw data (/proc/9062/stat): 9062 (minisat+_64-bit) R 9058 9058 6847 0 -1 0 9516 0 0 0 11901 50 0 0 25 0 1 0 1797224205 42393600 9014 4294967295 134512640 135094434 3221224432 3221223088 134557846 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9062/statm): 10350 9014 145 145 0 10205 0
[pid=9062] vsize: 41400
Current children cumulated CPU time (s) 119.52
Current children cumulated vsize (Kb) 43524

[startup+130.017 s]
Raw data (loadavg): 0.96 0.94 0.91 2/57 9062
Raw data (/proc/9058/stat): 9058 (minisat+_script) S 9057 9058 6847 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797224201 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9058/statm): 531 226 485 147 0 384 0
[pid=9058] vsize: 2124
Raw data (/proc/9062/stat): 9062 (minisat+_64-bit) R 9058 9058 6847 0 -1 0 9614 0 0 0 12899 52 0 0 25 0 1 0 1797224205 42917888 9112 4294967295 134512640 135094434 3221224432 3221223120 134554709 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9062/statm): 10478 9112 145 145 0 10333 0
[pid=9062] vsize: 41912
Current children cumulated CPU time (s) 129.52
Current children cumulated vsize (Kb) 44036

[startup+140.018 s]
Raw data (loadavg): 0.96 0.94 0.91 2/57 9062
Raw data (/proc/9058/stat): 9058 (minisat+_script) S 9057 9058 6847 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797224201 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9058/statm): 531 226 485 147 0 384 0
[pid=9058] vsize: 2124
Raw data (/proc/9062/stat): 9062 (minisat+_64-bit) R 9058 9058 6847 0 -1 0 9671 0 0 0 13897 53 0 0 25 0 1 0 1797224205 43147264 9169 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9062/statm): 10534 9169 145 145 0 10389 0
[pid=9062] vsize: 42136
Current children cumulated CPU time (s) 139.51
Current children cumulated vsize (Kb) 44260

[startup+150.02 s]
Raw data (loadavg): 0.97 0.94 0.91 2/57 9062
Raw data (/proc/9058/stat): 9058 (minisat+_script) S 9057 9058 6847 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797224201 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9058/statm): 531 226 485 147 0 384 0
[pid=9058] vsize: 2124
Raw data (/proc/9062/stat): 9062 (minisat+_64-bit) R 9058 9058 6847 0 -1 0 9758 0 0 0 14896 54 0 0 25 0 1 0 1797224205 43495424 9256 4294967295 134512640 135094434 3221224432 3221223072 134558264 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9062/statm): 10619 9256 145 145 0 10474 0
[pid=9062] vsize: 42476
Current children cumulated CPU time (s) 149.51
Current children cumulated vsize (Kb) 44600

[startup+160.021 s]
Raw data (loadavg): 0.97 0.95 0.91 2/57 9062
Raw data (/proc/9058/stat): 9058 (minisat+_script) S 9057 9058 6847 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797224201 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9058/statm): 531 226 485 147 0 384 0
[pid=9058] vsize: 2124
Raw data (/proc/9062/stat): 9062 (minisat+_64-bit) R 9058 9058 6847 0 -1 0 9867 0 0 0 15894 54 0 0 25 0 1 0 1797224205 43929600 9365 4294967295 134512640 135094434 3221224432 3221223088 134557937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9062/statm): 10725 9365 145 145 0 10580 0
[pid=9062] vsize: 42900
Current children cumulated CPU time (s) 159.49
Current children cumulated vsize (Kb) 45024

[startup+170.022 s]
Raw data (loadavg): 0.98 0.95 0.91 2/57 9062
Raw data (/proc/9058/stat): 9058 (minisat+_script) S 9057 9058 6847 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797224201 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9058/statm): 531 226 485 147 0 384 0
[pid=9058] vsize: 2124
Raw data (/proc/9062/stat): 9062 (minisat+_64-bit) R 9058 9058 6847 0 -1 0 9956 0 0 0 16893 55 0 0 25 0 1 0 1797224205 44285952 9454 4294967295 134512640 135094434 3221224432 3221223088 134558426 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9062/statm): 10812 9454 145 145 0 10667 0
[pid=9062] vsize: 43248
Current children cumulated CPU time (s) 169.49
Current children cumulated vsize (Kb) 45372

[startup+180.023 s]
Raw data (loadavg): 0.98 0.95 0.91 2/57 9062
Raw data (/proc/9058/stat): 9058 (minisat+_script) S 9057 9058 6847 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797224201 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9058/statm): 531 226 485 147 0 384 0
[pid=9058] vsize: 2124
Raw data (/proc/9062/stat): 9062 (minisat+_64-bit) R 9058 9058 6847 0 -1 0 10061 0 0 0 17891 55 0 0 25 0 1 0 1797224205 44703744 9559 4294967295 134512640 135094434 3221224432 3221223056 134562078 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9062/statm): 10914 9559 145 145 0 10769 0
[pid=9062] vsize: 43656
Current children cumulated CPU time (s) 179.47
Current children cumulated vsize (Kb) 45780

[startup+190.023 s]
Raw data (loadavg): 0.98 0.95 0.91 2/57 9062
Raw data (/proc/9058/stat): 9058 (minisat+_script) S 9057 9058 6847 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797224201 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9058/statm): 531 226 485 147 0 384 0
[pid=9058] vsize: 2124
Raw data (/proc/9062/stat): 9062 (minisat+_64-bit) R 9058 9058 6847 0 -1 0 10162 0 0 0 18889 56 0 0 25 0 1 0 1797224205 45109248 9660 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9062/statm): 11013 9660 145 145 0 10868 0
[pid=9062] vsize: 44052
Current children cumulated CPU time (s) 189.46
Current children cumulated vsize (Kb) 46176

[startup+200.025 s]
Raw data (loadavg): 0.98 0.95 0.91 2/57 9062
Raw data (/proc/9058/stat): 9058 (minisat+_script) S 9057 9058 6847 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797224201 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9058/statm): 531 226 485 147 0 384 0
[pid=9058] vsize: 2124
Raw data (/proc/9062/stat): 9062 (minisat+_64-bit) R 9058 9058 6847 0 -1 0 10282 0 0 0 19887 57 0 0 25 0 1 0 1797224205 45580288 9780 4294967295 134512640 135094434 3221224432 3221223056 134557598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9062/statm): 11128 9780 145 145 0 10983 0
[pid=9062] vsize: 44512
Current children cumulated CPU time (s) 199.45
Current children cumulated vsize (Kb) 46636

[startup+210.026 s]
Raw data (loadavg): 0.99 0.95 0.91 2/57 9062
Raw data (/proc/9058/stat): 9058 (minisat+_script) S 9057 9058 6847 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797224201 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9058/statm): 531 226 485 147 0 384 0
[pid=9058] vsize: 2124
Raw data (/proc/9062/stat): 9062 (minisat+_64-bit) R 9058 9058 6847 0 -1 0 10377 0 0 0 20886 58 0 0 25 0 1 0 1797224205 45957120 9875 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9062/statm): 11220 9875 145 145 0 11075 0
[pid=9062] vsize: 44880
Current children cumulated CPU time (s) 209.45
Current children cumulated vsize (Kb) 47004

[startup+220.027 s]
Raw data (loadavg): 0.99 0.95 0.91 2/57 9062
Raw data (/proc/9058/stat): 9058 (minisat+_script) S 9057 9058 6847 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797224201 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9058/statm): 531 226 485 147 0 384 0
[pid=9058] vsize: 2124
Raw data (/proc/9062/stat): 9062 (minisat+_64-bit) R 9058 9058 6847 0 -1 0 10464 0 0 0 21884 58 0 0 25 0 1 0 1797224205 46305280 9962 4294967295 134512640 135094434 3221224432 3221223092 134553489 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9062/statm): 11305 9962 145 145 0 11160 0
[pid=9062] vsize: 45220
Current children cumulated CPU time (s) 219.43
Current children cumulated vsize (Kb) 47344

[startup+230.028 s]
Raw data (loadavg): 0.99 0.95 0.91 2/57 9062
Raw data (/proc/9058/stat): 9058 (minisat+_script) S 9057 9058 6847 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797224201 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9058/statm): 531 226 485 147 0 384 0
[pid=9058] vsize: 2124
Raw data (/proc/9062/stat): 9062 (minisat+_64-bit) R 9058 9058 6847 0 -1 0 10622 0 0 0 22881 60 0 0 25 0 1 0 1797224205 46940160 10120 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9062/statm): 11460 10120 145 145 0 11315 0
[pid=9062] vsize: 45840
Current children cumulated CPU time (s) 229.42
Current children cumulated vsize (Kb) 47964

[startup+240.028 s]
Raw data (loadavg): 0.99 0.95 0.91 2/57 9062
Raw data (/proc/9058/stat): 9058 (minisat+_script) S 9057 9058 6847 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797224201 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9058/statm): 531 226 485 147 0 384 0
[pid=9058] vsize: 2124
Raw data (/proc/9062/stat): 9062 (minisat+_64-bit) R 9058 9058 6847 0 -1 0 10718 0 0 0 23880 61 0 0 25 0 1 0 1797224205 47325184 10216 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9062/statm): 11554 10216 145 145 0 11409 0
[pid=9062] vsize: 46216
Current children cumulated CPU time (s) 239.42
Current children cumulated vsize (Kb) 48340

[startup+250.03 s]
Raw data (loadavg): 0.99 0.95 0.91 2/57 9062
Raw data (/proc/9058/stat): 9058 (minisat+_script) S 9057 9058 6847 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797224201 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9058/statm): 531 226 485 147 0 384 0
[pid=9058] vsize: 2124
Raw data (/proc/9062/stat): 9062 (minisat+_64-bit) R 9058 9058 6847 0 -1 0 10808 0 0 0 24878 61 0 0 25 0 1 0 1797224205 47697920 10306 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9062/statm): 11645 10306 145 145 0 11500 0
[pid=9062] vsize: 46580
Current children cumulated CPU time (s) 249.4
Current children cumulated vsize (Kb) 48704

[startup+260.03 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 9062
Raw data (/proc/9058/stat): 9058 (minisat+_script) S 9057 9058 6847 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797224201 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9058/statm): 531 226 485 147 0 384 0
[pid=9058] vsize: 2124
Raw data (/proc/9062/stat): 9062 (minisat+_64-bit) R 9058 9058 6847 0 -1 0 10909 0 0 0 25877 62 0 0 25 0 1 0 1797224205 48103424 10407 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9062/statm): 11744 10407 145 145 0 11599 0
[pid=9062] vsize: 46976
Current children cumulated CPU time (s) 259.4
Current children cumulated vsize (Kb) 49100

[startup+270.03 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 9062
Raw data (/proc/9058/stat): 9058 (minisat+_script) S 9057 9058 6847 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797224201 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9058/statm): 531 226 485 147 0 384 0
[pid=9058] vsize: 2124
Raw data (/proc/9062/stat): 9062 (minisat+_64-bit) R 9058 9058 6847 0 -1 0 11059 0 0 0 26874 64 0 0 25 0 1 0 1797224205 48967680 10557 4294967295 134512640 135094434 3221224432 3221223088 134557937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9062/statm): 11955 10557 145 145 0 11810 0
[pid=9062] vsize: 47820
Current children cumulated CPU time (s) 269.39
Current children cumulated vsize (Kb) 49944

[startup+280.031 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 9062
Raw data (/proc/9058/stat): 9058 (minisat+_script) S 9057 9058 6847 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797224201 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9058/statm): 531 226 485 147 0 384 0
[pid=9058] vsize: 2124
Raw data (/proc/9062/stat): 9062 (minisat+_64-bit) R 9058 9058 6847 0 -1 0 11217 0 0 0 27872 64 0 0 25 0 1 0 1797224205 49606656 10715 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9062/statm): 12111 10715 145 145 0 11966 0
[pid=9062] vsize: 48444
Current children cumulated CPU time (s) 279.37
Current children cumulated vsize (Kb) 50568

[startup+290.032 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 9062
Raw data (/proc/9058/stat): 9058 (minisat+_script) S 9057 9058 6847 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797224201 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9058/statm): 531 226 485 147 0 384 0
[pid=9058] vsize: 2124
Raw data (/proc/9062/stat): 9062 (minisat+_64-bit) R 9058 9058 6847 0 -1 0 11292 0 0 0 28871 65 0 0 25 0 1 0 1797224205 49905664 10790 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9062/statm): 12184 10790 145 145 0 12039 0
[pid=9062] vsize: 48736
Current children cumulated CPU time (s) 289.37
Current children cumulated vsize (Kb) 50860

[startup+300.033 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 9062
Raw data (/proc/9058/stat): 9058 (minisat+_script) S 9057 9058 6847 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797224201 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9058/statm): 531 226 485 147 0 384 0
[pid=9058] vsize: 2124
Raw data (/proc/9062/stat): 9062 (minisat+_64-bit) R 9058 9058 6847 0 -1 0 11358 0 0 0 29870 65 0 0 25 0 1 0 1797224205 50176000 10856 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9062/statm): 12250 10856 145 145 0 12105 0
[pid=9062] vsize: 49000
Current children cumulated CPU time (s) 299.36
Current children cumulated vsize (Kb) 51124

[startup+310.034 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 9062
Raw data (/proc/9058/stat): 9058 (minisat+_script) S 9057 9058 6847 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797224201 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9058/statm): 531 226 485 147 0 384 0
[pid=9058] vsize: 2124
Raw data (/proc/9062/stat): 9062 (minisat+_64-bit) R 9058 9058 6847 0 -1 0 11435 0 0 0 30867 66 0 0 25 0 1 0 1797224205 50483200 10933 4294967295 134512640 135094434 3221224432 3221223088 134557872 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9062/statm): 12325 10933 145 145 0 12180 0
[pid=9062] vsize: 49300
Current children cumulated CPU time (s) 309.34
Current children cumulated vsize (Kb) 51424

[startup+320.035 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 9062
Raw data (/proc/9058/stat): 9058 (minisat+_script) S 9057 9058 6847 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797224201 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9058/statm): 531 226 485 147 0 384 0
[pid=9058] vsize: 2124
Raw data (/proc/9062/stat): 9062 (minisat+_64-bit) R 9058 9058 6847 0 -1 0 11510 0 0 0 31866 67 0 0 25 0 1 0 1797224205 50782208 11008 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9062/statm): 12398 11008 145 145 0 12253 0
[pid=9062] vsize: 49592
Current children cumulated CPU time (s) 319.34
Current children cumulated vsize (Kb) 51716

[startup+330.036 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 9062
Raw data (/proc/9058/stat): 9058 (minisat+_script) S 9057 9058 6847 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797224201 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9058/statm): 531 226 485 147 0 384 0
[pid=9058] vsize: 2124
Raw data (/proc/9062/stat): 9062 (minisat+_64-bit) R 9058 9058 6847 0 -1 0 11592 0 0 0 32865 68 0 0 25 0 1 0 1797224205 51118080 11090 4294967295 134512640 135094434 3221224432 3221223088 134557879 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9062/statm): 12480 11090 145 145 0 12335 0
[pid=9062] vsize: 49920
Current children cumulated CPU time (s) 329.34
Current children cumulated vsize (Kb) 52044

[startup+340.036 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 9062
Raw data (/proc/9058/stat): 9058 (minisat+_script) S 9057 9058 6847 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797224201 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9058/statm): 531 226 485 147 0 384 0
[pid=9058] vsize: 2124
Raw data (/proc/9062/stat): 9062 (minisat+_64-bit) R 9058 9058 6847 0 -1 0 11700 0 0 0 33863 69 0 0 25 0 1 0 1797224205 51544064 11198 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9062/statm): 12584 11198 145 145 0 12439 0
[pid=9062] vsize: 50336
Current children cumulated CPU time (s) 339.33
Current children cumulated vsize (Kb) 52460

[startup+350.038 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 9062
Raw data (/proc/9058/stat): 9058 (minisat+_script) S 9057 9058 6847 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797224201 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9058/statm): 531 226 485 147 0 384 0
[pid=9058] vsize: 2124
Raw data (/proc/9062/stat): 9062 (minisat+_64-bit) R 9058 9058 6847 0 -1 0 11834 0 0 0 34861 70 0 0 25 0 1 0 1797224205 52092928 11332 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9062/statm): 12718 11332 145 145 0 12573 0
[pid=9062] vsize: 50872
Current children cumulated CPU time (s) 349.32
Current children cumulated vsize (Kb) 52996

[startup+360.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9062
Raw data (/proc/9058/stat): 9058 (minisat+_script) S 9057 9058 6847 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797224201 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9058/statm): 531 226 485 147 0 384 0
[pid=9058] vsize: 2124
Raw data (/proc/9062/stat): 9062 (minisat+_64-bit) R 9058 9058 6847 0 -1 0 11939 0 0 0 35859 71 0 0 25 0 1 0 1797224205 52510720 11437 4294967295 134512640 135094434 3221224432 3221223088 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9062/statm): 12820 11437 145 145 0 12675 0
[pid=9062] vsize: 51280
Current children cumulated CPU time (s) 359.31
Current children cumulated vsize (Kb) 53404

[startup+370.041 s]
Raw data (loadavg): 0.99 0.97 0.91 1/57 9062
Raw data (/proc/9058/stat): 9058 (minisat+_script) S 9057 9058 6847 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797224201 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9058/statm): 531 226 485 147 0 384 0
[pid=9058] vsize: 2124
Raw data (/proc/9062/stat): 9062 (minisat+_64-bit) T 9058 9058 6847 0 -1 0 12046 0 0 0 36865 72 0 0 25 0 1 0 1797224205 52944896 11544 4294967295 134512640 135094434 3221224432 3221222796 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/9062/statm): 12926 11544 145 145 0 12781 0
[pid=9062] vsize: 51704
Current children cumulated CPU time (s) 369.38
Current children cumulated vsize (Kb) 53828

[startup+380.152 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9062
Raw data (/proc/9058/stat): 9058 (minisat+_script) S 9057 9058 6847 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797224201 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9058/statm): 531 226 485 147 0 384 0
[pid=9058] vsize: 2124
Raw data (/proc/9062/stat): 9062 (minisat+_64-bit) R 9058 9058 6847 0 -1 0 12170 0 0 0 37863 74 0 0 25 0 1 0 1797224205 53440512 11668 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9062/statm): 13047 11668 145 145 0 12902 0
[pid=9062] vsize: 52188
Current children cumulated CPU time (s) 379.38
Current children cumulated vsize (Kb) 54312

[startup+390.153 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9062
Raw data (/proc/9058/stat): 9058 (minisat+_script) S 9057 9058 6847 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797224201 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9058/statm): 531 226 485 147 0 384 0
[pid=9058] vsize: 2124
Raw data (/proc/9062/stat): 9062 (minisat+_64-bit) R 9058 9058 6847 0 -1 0 12243 0 0 0 38862 74 0 0 25 0 1 0 1797224205 53743616 11741 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9062/statm): 13121 11741 145 145 0 12976 0
[pid=9062] vsize: 52484
Current children cumulated CPU time (s) 389.37
Current children cumulated vsize (Kb) 54608

[startup+400.155 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9062
Raw data (/proc/9058/stat): 9058 (minisat+_script) S 9057 9058 6847 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797224201 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9058/statm): 531 226 485 147 0 384 0
[pid=9058] vsize: 2124
Raw data (/proc/9062/stat): 9062 (minisat+_64-bit) R 9058 9058 6847 0 -1 0 12332 0 0 0 39861 74 0 0 25 0 1 0 1797224205 54095872 11830 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9062/statm): 13207 11830 145 145 0 13062 0
[pid=9062] vsize: 52828
Current children cumulated CPU time (s) 399.36
Current children cumulated vsize (Kb) 54952

[startup+410.155 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9062
Raw data (/proc/9058/stat): 9058 (minisat+_script) S 9057 9058 6847 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797224201 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9058/statm): 531 226 485 147 0 384 0
[pid=9058] vsize: 2124
Raw data (/proc/9062/stat): 9062 (minisat+_64-bit) R 9058 9058 6847 0 -1 0 12403 0 0 0 40860 76 0 0 25 0 1 0 1797224205 54374400 11901 4294967295 134512640 135094434 3221224432 3221223092 134553501 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9062/statm): 13275 11901 145 145 0 13130 0
[pid=9062] vsize: 53100
Current children cumulated CPU time (s) 409.37
Current children cumulated vsize (Kb) 55224

[startup+420.156 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9062
Raw data (/proc/9058/stat): 9058 (minisat+_script) S 9057 9058 6847 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797224201 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9058/statm): 531 226 485 147 0 384 0
[pid=9058] vsize: 2124
Raw data (/proc/9062/stat): 9062 (minisat+_64-bit) R 9058 9058 6847 0 -1 0 12491 0 0 0 41857 77 0 0 25 0 1 0 1797224205 54726656 11989 4294967295 134512640 135094434 3221224432 3221223088 134558187 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9062/statm): 13361 11989 145 145 0 13216 0
[pid=9062] vsize: 53444
Current children cumulated CPU time (s) 419.35
Current children cumulated vsize (Kb) 55568

[startup+430.158 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9062
Raw data (/proc/9058/stat): 9058 (minisat+_script) S 9057 9058 6847 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797224201 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9058/statm): 531 226 485 147 0 384 0
[pid=9058] vsize: 2124
Raw data (/proc/9062/stat): 9062 (minisat+_64-bit) R 9058 9058 6847 0 -1 0 12573 0 0 0 42855 78 0 0 25 0 1 0 1797224205 55062528 12071 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9062/statm): 13443 12071 145 145 0 13298 0
[pid=9062] vsize: 53772
Current children cumulated CPU time (s) 429.34
Current children cumulated vsize (Kb) 55896

[startup+440.159 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9062
Raw data (/proc/9058/stat): 9058 (minisat+_script) S 9057 9058 6847 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797224201 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9058/statm): 531 226 485 147 0 384 0
[pid=9058] vsize: 2124
Raw data (/proc/9062/stat): 9062 (minisat+_64-bit) R 9058 9058 6847 0 -1 0 12675 0 0 0 43853 79 0 0 25 0 1 0 1797224205 55476224 12173 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9062/statm): 13544 12173 145 145 0 13399 0
[pid=9062] vsize: 54176
Current children cumulated CPU time (s) 439.33
Current children cumulated vsize (Kb) 56300

[startup+450.16 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9062
Raw data (/proc/9058/stat): 9058 (minisat+_script) S 9057 9058 6847 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797224201 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9058/statm): 531 226 485 147 0 384 0
[pid=9058] vsize: 2124
Raw data (/proc/9062/stat): 9062 (minisat+_64-bit) R 9058 9058 6847 0 -1 0 12740 0 0 0 44852 80 0 0 25 0 1 0 1797224205 55734272 12238 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9062/statm): 13607 12238 145 145 0 13462 0
[pid=9062] vsize: 54428
Current children cumulated CPU time (s) 449.33
Current children cumulated vsize (Kb) 56552

[startup+460.161 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9062
Raw data (/proc/9058/stat): 9058 (minisat+_script) S 9057 9058 6847 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797224201 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9058/statm): 531 226 485 147 0 384 0
[pid=9058] vsize: 2124
Raw data (/proc/9062/stat): 9062 (minisat+_64-bit) R 9058 9058 6847 0 -1 0 12887 0 0 0 45849 81 0 0 25 0 1 0 1797224205 56328192 12385 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9062/statm): 13752 12385 145 145 0 13607 0
[pid=9062] vsize: 55008
Current children cumulated CPU time (s) 459.31
Current children cumulated vsize (Kb) 57132

[startup+470.162 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9062
Raw data (/proc/9058/stat): 9058 (minisat+_script) S 9057 9058 6847 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797224201 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9058/statm): 531 226 485 147 0 384 0
[pid=9058] vsize: 2124
Raw data (/proc/9062/stat): 9062 (minisat+_64-bit) R 9058 9058 6847 0 -1 0 13010 0 0 0 46847 82 0 0 25 0 1 0 1797224205 56840192 12508 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9062/statm): 13877 12508 145 145 0 13732 0
[pid=9062] vsize: 55508
Current children cumulated CPU time (s) 469.3
Current children cumulated vsize (Kb) 57632

[startup+480.163 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9062
Raw data (/proc/9058/stat): 9058 (minisat+_script) S 9057 9058 6847 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797224201 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9058/statm): 531 226 485 147 0 384 0
[pid=9058] vsize: 2124
Raw data (/proc/9062/stat): 9062 (minisat+_64-bit) R 9058 9058 6847 0 -1 0 13213 0 0 0 47842 85 0 0 25 0 1 0 1797224205 57647104 12711 4294967295 134512640 135094434 3221224432 3221223088 134558029 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9062/statm): 14074 12711 145 145 0 13929 0
[pid=9062] vsize: 56296
Current children cumulated CPU time (s) 479.28
Current children cumulated vsize (Kb) 58420

[startup+490.163 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9062
Raw data (/proc/9058/stat): 9058 (minisat+_script) S 9057 9058 6847 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797224201 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9058/statm): 531 226 485 147 0 384 0
[pid=9058] vsize: 2124
Raw data (/proc/9062/stat): 9062 (minisat+_64-bit) R 9058 9058 6847 0 -1 0 13311 0 0 0 48840 86 0 0 25 0 1 0 1797224205 58040320 12809 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9062/statm): 14170 12809 145 145 0 14025 0
[pid=9062] vsize: 56680
Current children cumulated CPU time (s) 489.27
Current children cumulated vsize (Kb) 58804

[startup+500.165 s]
Raw data (loadavg): 1.07 0.99 0.91 2/57 9062
Raw data (/proc/9058/stat): 9058 (minisat+_script) S 9057 9058 6847 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797224201 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9058/statm): 531 226 485 147 0 384 0
[pid=9058] vsize: 2124
Raw data (/proc/9062/stat): 9062 (minisat+_64-bit) R 9058 9058 6847 0 -1 0 13395 0 0 0 49839 86 0 0 25 0 1 0 1797224205 58376192 12893 4294967295 134512640 135094434 3221224432 3221223088 134557863 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9062/statm): 14252 12893 145 145 0 14107 0
[pid=9062] vsize: 57008
Current children cumulated CPU time (s) 499.26
Current children cumulated vsize (Kb) 59132

[startup+510.166 s]
Raw data (loadavg): 1.06 0.99 0.91 2/57 9062
Raw data (/proc/9058/stat): 9058 (minisat+_script) S 9057 9058 6847 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797224201 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9058/statm): 531 226 485 147 0 384 0
[pid=9058] vsize: 2124
Raw data (/proc/9062/stat): 9062 (minisat+_64-bit) R 9058 9058 6847 0 -1 0 13497 0 0 0 50838 87 0 0 25 0 1 0 1797224205 58785792 12995 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9062/statm): 14352 12995 145 145 0 14207 0
[pid=9062] vsize: 57408
Current children cumulated CPU time (s) 509.26
Current children cumulated vsize (Kb) 59532

[startup+520.166 s]
Raw data (loadavg): 1.05 0.99 0.91 2/57 9062
Raw data (/proc/9058/stat): 9058 (minisat+_script) S 9057 9058 6847 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797224201 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9058/statm): 531 226 485 147 0 384 0
[pid=9058] vsize: 2124
Raw data (/proc/9062/stat): 9062 (minisat+_64-bit) R 9058 9058 6847 0 -1 0 13583 0 0 0 51836 88 0 0 25 0 1 0 1797224205 59125760 13081 4294967295 134512640 135094434 3221224432 3221223092 134553491 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9062/statm): 14435 13081 145 145 0 14290 0
[pid=9062] vsize: 57740
Current children cumulated CPU time (s) 519.25
Current children cumulated vsize (Kb) 59864

[startup+530.167 s]
Raw data (loadavg): 1.04 0.99 0.91 2/57 9062
Raw data (/proc/9058/stat): 9058 (minisat+_script) S 9057 9058 6847 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797224201 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9058/statm): 531 226 485 147 0 384 0
[pid=9058] vsize: 2124
Raw data (/proc/9062/stat): 9062 (minisat+_64-bit) R 9058 9058 6847 0 -1 0 13666 0 0 0 52835 88 0 0 25 0 1 0 1797224205 59478016 13164 4294967295 134512640 135094434 3221224432 3221223088 134557925 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9062/statm): 14521 13164 145 145 0 14376 0
[pid=9062] vsize: 58084
Current children cumulated CPU time (s) 529.24
Current children cumulated vsize (Kb) 60208

[startup+540.168 s]
Raw data (loadavg): 1.04 0.99 0.91 2/57 9062
Raw data (/proc/9058/stat): 9058 (minisat+_script) S 9057 9058 6847 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797224201 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9058/statm): 531 226 485 147 0 384 0
[pid=9058] vsize: 2124
Raw data (/proc/9062/stat): 9062 (minisat+_64-bit) R 9058 9058 6847 0 -1 0 13735 0 0 0 53833 89 0 0 25 0 1 0 1797224205 59752448 13233 4294967295 134512640 135094434 3221224432 3221223064 134557561 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9062/statm): 14588 13233 145 145 0 14443 0
[pid=9062] vsize: 58352
Current children cumulated CPU time (s) 539.23
Current children cumulated vsize (Kb) 60476

[startup+550.169 s]
Raw data (loadavg): 1.03 0.99 0.91 2/57 9062
Raw data (/proc/9058/stat): 9058 (minisat+_script) S 9057 9058 6847 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797224201 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9058/statm): 531 226 485 147 0 384 0
[pid=9058] vsize: 2124
Raw data (/proc/9062/stat): 9062 (minisat+_64-bit) R 9058 9058 6847 0 -1 0 13817 0 0 0 54832 90 0 0 25 0 1 0 1797224205 60084224 13315 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9062/statm): 14669 13315 145 145 0 14524 0
[pid=9062] vsize: 58676
Current children cumulated CPU time (s) 549.23
Current children cumulated vsize (Kb) 60800

[startup+560.169 s]
Raw data (loadavg): 1.03 0.99 0.91 2/57 9062
Raw data (/proc/9058/stat): 9058 (minisat+_script) S 9057 9058 6847 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797224201 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9058/statm): 531 226 485 147 0 384 0
[pid=9058] vsize: 2124
Raw data (/proc/9062/stat): 9062 (minisat+_64-bit) R 9058 9058 6847 0 -1 0 13924 0 0 0 55830 91 0 0 25 0 1 0 1797224205 60514304 13422 4294967295 134512640 135094434 3221224432 3221223024 134557031 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9062/statm): 14774 13422 145 145 0 14629 0
[pid=9062] vsize: 59096
Current children cumulated CPU time (s) 559.22
Current children cumulated vsize (Kb) 61220

[startup+570.17 s]
Raw data (loadavg): 1.02 0.99 0.91 2/57 9062
Raw data (/proc/9058/stat): 9058 (minisat+_script) S 9057 9058 6847 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797224201 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9058/statm): 531 226 485 147 0 384 0
[pid=9058] vsize: 2124
Raw data (/proc/9062/stat): 9062 (minisat+_64-bit) R 9058 9058 6847 0 -1 0 14022 0 0 0 56827 92 0 0 25 0 1 0 1797224205 60903424 13520 4294967295 134512640 135094434 3221224432 3221223068 134557639 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9062/statm): 14869 13520 145 145 0 14724 0
[pid=9062] vsize: 59476
Current children cumulated CPU time (s) 569.2
Current children cumulated vsize (Kb) 61600

[startup+580.171 s]
Raw data (loadavg): 1.02 0.99 0.91 2/57 9062
Raw data (/proc/9058/stat): 9058 (minisat+_script) S 9057 9058 6847 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797224201 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9058/statm): 531 226 485 147 0 384 0
[pid=9058] vsize: 2124
Raw data (/proc/9062/stat): 9062 (minisat+_64-bit) R 9058 9058 6847 0 -1 0 14092 0 0 0 57826 92 0 0 25 0 1 0 1797224205 61706240 13590 4294967295 134512640 135094434 3221224432 3221223120 134554723 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9062/statm): 15065 13590 145 145 0 14920 0
[pid=9062] vsize: 60260
Current children cumulated CPU time (s) 579.19
Current children cumulated vsize (Kb) 62384

[startup+590.171 s]
Raw data (loadavg): 1.01 0.99 0.91 2/57 9062
Raw data (/proc/9058/stat): 9058 (minisat+_script) S 9057 9058 6847 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797224201 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9058/statm): 531 226 485 147 0 384 0
[pid=9058] vsize: 2124
Raw data (/proc/9062/stat): 9062 (minisat+_64-bit) R 9058 9058 6847 0 -1 0 14185 0 0 0 58825 93 0 0 25 0 1 0 1797224205 62078976 13683 4294967295 134512640 135094434 3221224432 3221223088 134558184 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9062/statm): 15156 13683 145 145 0 15011 0
[pid=9062] vsize: 60624
Current children cumulated CPU time (s) 589.19
Current children cumulated vsize (Kb) 62748

[startup+600.173 s]
Raw data (loadavg): 1.01 0.99 0.91 2/57 9062
Raw data (/proc/9058/stat): 9058 (minisat+_script) S 9057 9058 6847 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797224201 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9058/statm): 531 226 485 147 0 384 0
[pid=9058] vsize: 2124
Raw data (/proc/9062/stat): 9062 (minisat+_64-bit) R 9058 9058 6847 0 -1 0 14251 0 0 0 59823 94 0 0 25 0 1 0 1797224205 62345216 13749 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9062/statm): 15221 13749 145 145 0 15076 0
[pid=9062] vsize: 60884
Current children cumulated CPU time (s) 599.18
Current children cumulated vsize (Kb) 63008

[startup+610.174 s]
Raw data (loadavg): 1.01 0.99 0.91 2/57 9062
Raw data (/proc/9058/stat): 9058 (minisat+_script) S 9057 9058 6847 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797224201 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9058/statm): 531 226 485 147 0 384 0
[pid=9058] vsize: 2124
Raw data (/proc/9062/stat): 9062 (minisat+_64-bit) R 9058 9058 6847 0 -1 0 14345 0 0 0 60821 95 0 0 25 0 1 0 1797224205 62734336 13843 4294967295 134512640 135094434 3221224432 3221223088 134558235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9062/statm): 15316 13843 145 145 0 15171 0
[pid=9062] vsize: 61264
Current children cumulated CPU time (s) 609.17
Current children cumulated vsize (Kb) 63388

[startup+620.174 s]
Raw data (loadavg): 1.01 0.99 0.91 2/57 9062
Raw data (/proc/9058/stat): 9058 (minisat+_script) S 9057 9058 6847 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797224201 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9058/statm): 531 226 485 147 0 384 0
[pid=9058] vsize: 2124
Raw data (/proc/9062/stat): 9062 (minisat+_64-bit) R 9058 9058 6847 0 -1 0 14433 0 0 0 61820 95 0 0 25 0 1 0 1797224205 63086592 13931 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9062/statm): 15402 13931 145 145 0 15257 0
[pid=9062] vsize: 61608
Current children cumulated CPU time (s) 619.16
Current children cumulated vsize (Kb) 63732

[startup+630.174 s]
Raw data (loadavg): 1.01 0.99 0.91 2/57 9062
Raw data (/proc/9058/stat): 9058 (minisat+_script) S 9057 9058 6847 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797224201 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9058/statm): 531 226 485 147 0 384 0
[pid=9058] vsize: 2124
Raw data (/proc/9062/stat): 9062 (minisat+_64-bit) R 9058 9058 6847 0 -1 0 14522 0 0 0 62819 95 0 0 25 0 1 0 1797224205 63438848 14020 4294967295 134512640 135094434 3221224432 3221223088 134558181 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9062/statm): 15488 14020 145 145 0 15343 0
[pid=9062] vsize: 61952
Current children cumulated CPU time (s) 629.15
Current children cumulated vsize (Kb) 64076

[startup+640.175 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 9062
Raw data (/proc/9058/stat): 9058 (minisat+_script) S 9057 9058 6847 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797224201 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9058/statm): 531 226 485 147 0 384 0
[pid=9058] vsize: 2124
Raw data (/proc/9062/stat): 9062 (minisat+_64-bit) R 9058 9058 6847 0 -1 0 14655 0 0 0 63817 97 0 0 25 0 1 0 1797224205 63983616 14153 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9062/statm): 15621 14153 145 145 0 15476 0
[pid=9062] vsize: 62484
Current children cumulated CPU time (s) 639.15
Current children cumulated vsize (Kb) 64608

[startup+650.176 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 9062
Raw data (/proc/9058/stat): 9058 (minisat+_script) S 9057 9058 6847 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797224201 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9058/statm): 531 226 485 147 0 384 0
[pid=9058] vsize: 2124
Raw data (/proc/9062/stat): 9062 (minisat+_64-bit) R 9058 9058 6847 0 -1 0 14741 0 0 0 64814 98 0 0 25 0 1 0 1797224205 64323584 14239 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9062/statm): 15704 14239 145 145 0 15559 0
[pid=9062] vsize: 62816
Current children cumulated CPU time (s) 649.13
Current children cumulated vsize (Kb) 64940

[startup+660.177 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 9062
Raw data (/proc/9058/stat): 9058 (minisat+_script) S 9057 9058 6847 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797224201 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9058/statm): 531 226 485 147 0 384 0
[pid=9058] vsize: 2124
Raw data (/proc/9062/stat): 9062 (minisat+_64-bit) R 9058 9058 6847 0 -1 0 14865 0 0 0 65811 99 0 0 25 0 1 0 1797224205 64860160 14363 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9062/statm): 15835 14363 145 145 0 15690 0
[pid=9062] vsize: 63340
Current children cumulated CPU time (s) 659.11
Current children cumulated vsize (Kb) 65464

[startup+670.178 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 9062
Raw data (/proc/9058/stat): 9058 (minisat+_script) S 9057 9058 6847 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797224201 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9058/statm): 531 226 485 147 0 384 0
[pid=9058] vsize: 2124
Raw data (/proc/9062/stat): 9062 (minisat+_64-bit) R 9058 9058 6847 0 -1 0 14952 0 0 0 66810 100 0 0 25 0 1 0 1797224205 65208320 14450 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9062/statm): 15920 14450 145 145 0 15775 0
[pid=9062] vsize: 63680
Current children cumulated CPU time (s) 669.11
Current children cumulated vsize (Kb) 65804

[startup+680.179 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 9062
Raw data (/proc/9058/stat): 9058 (minisat+_script) S 9057 9058 6847 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797224201 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9058/statm): 531 226 485 147 0 384 0
[pid=9058] vsize: 2124
Raw data (/proc/9062/stat): 9062 (minisat+_64-bit) R 9058 9058 6847 0 -1 0 15030 0 0 0 67809 101 0 0 25 0 1 0 1797224205 65519616 14528 4294967295 134512640 135094434 3221224432 3221223088 134557937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9062/statm): 15996 14528 145 145 0 15851 0
[pid=9062] vsize: 63984
Current children cumulated CPU time (s) 679.11
Current children cumulated vsize (Kb) 66108

[startup+690.18 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 9062
Raw data (/proc/9058/stat): 9058 (minisat+_script) S 9057 9058 6847 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797224201 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9058/statm): 531 226 485 147 0 384 0
[pid=9058] vsize: 2124
Raw data (/proc/9062/stat): 9062 (minisat+_64-bit) R 9058 9058 6847 0 -1 0 15144 0 0 0 68807 102 0 0 25 0 1 0 1797224205 65986560 14642 4294967295 134512640 135094434 3221224432 3221223172 134559691 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9062/statm): 16110 14642 145 145 0 15965 0
[pid=9062] vsize: 64440
Current children cumulated CPU time (s) 689.1
Current children cumulated vsize (Kb) 66564

[startup+700.182 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 9062
Raw data (/proc/9058/stat): 9058 (minisat+_script) S 9057 9058 6847 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797224201 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9058/statm): 531 226 485 147 0 384 0
[pid=9058] vsize: 2124
Raw data (/proc/9062/stat): 9062 (minisat+_64-bit) R 9058 9058 6847 0 -1 0 15235 0 0 0 69805 103 0 0 25 0 1 0 1797224205 66355200 14733 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9062/statm): 16200 14733 145 145 0 16055 0
[pid=9062] vsize: 64800
Current children cumulated CPU time (s) 699.09
Current children cumulated vsize (Kb) 66924

[startup+710.182 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 9062
Raw data (/proc/9058/stat): 9058 (minisat+_script) S 9057 9058 6847 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797224201 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9058/statm): 531 226 485 147 0 384 0
[pid=9058] vsize: 2124
Raw data (/proc/9062/stat): 9062 (minisat+_64-bit) R 9058 9058 6847 0 -1 0 15325 0 0 0 70802 104 0 0 25 0 1 0 1797224205 66715648 14823 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9062/statm): 16288 14823 145 145 0 16143 0
[pid=9062] vsize: 65152
Current children cumulated CPU time (s) 709.07
Current children cumulated vsize (Kb) 67276

[startup+720.183 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 9062
Raw data (/proc/9058/stat): 9058 (minisat+_script) S 9057 9058 6847 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797224201 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9058/statm): 531 226 485 147 0 384 0
[pid=9058] vsize: 2124
Raw data (/proc/9062/stat): 9062 (minisat+_64-bit) R 9058 9058 6847 0 -1 0 15472 0 0 0 71799 106 0 0 25 0 1 0 1797224205 67305472 14970 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9062/statm): 16432 14970 145 145 0 16287 0
[pid=9062] vsize: 65728
Current children cumulated CPU time (s) 719.06
Current children cumulated vsize (Kb) 67852

[startup+730.184 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 9062
Raw data (/proc/9058/stat): 9058 (minisat+_script) S 9057 9058 6847 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797224201 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9058/statm): 531 226 485 147 0 384 0
[pid=9058] vsize: 2124
Raw data (/proc/9062/stat): 9062 (minisat+_64-bit) R 9058 9058 6847 0 -1 0 15605 0 0 0 72797 107 0 0 25 0 1 0 1797224205 67842048 15103 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9062/statm): 16563 15103 145 145 0 16418 0
[pid=9062] vsize: 66252
Current children cumulated CPU time (s) 729.05
Current children cumulated vsize (Kb) 68376

[startup+740.185 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 9062
Raw data (/proc/9058/stat): 9058 (minisat+_script) S 9057 9058 6847 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797224201 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9058/statm): 531 226 485 147 0 384 0
[pid=9058] vsize: 2124
Raw data (/proc/9062/stat): 9062 (minisat+_64-bit) R 9058 9058 6847 0 -1 0 15804 0 0 0 73793 108 0 0 25 0 1 0 1797224205 68653056 15302 4294967295 134512640 135094434 3221224432 3221223088 134557860 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9062/statm): 16761 15302 145 145 0 16616 0
[pid=9062] vsize: 67044
Current children cumulated CPU time (s) 739.02
Current children cumulated vsize (Kb) 69168

[startup+750.186 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 9062
Raw data (/proc/9058/stat): 9058 (minisat+_script) S 9057 9058 6847 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797224201 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9058/statm): 531 226 485 147 0 384 0
[pid=9058] vsize: 2124
Raw data (/proc/9062/stat): 9062 (minisat+_64-bit) R 9058 9058 6847 0 -1 0 15931 0 0 0 74791 109 0 0 25 0 1 0 1797224205 69160960 15429 4294967295 134512640 135094434 3221224432 3221223092 134553480 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9062/statm): 16885 15429 145 145 0 16740 0
[pid=9062] vsize: 67540
Current children cumulated CPU time (s) 749.01
Current children cumulated vsize (Kb) 69664

[startup+760.187 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 9062
Raw data (/proc/9058/stat): 9058 (minisat+_script) S 9057 9058 6847 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797224201 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9058/statm): 531 226 485 147 0 384 0
[pid=9058] vsize: 2124
Raw data (/proc/9062/stat): 9062 (minisat+_64-bit) R 9058 9058 6847 0 -1 0 16095 0 0 0 75788 110 0 0 25 0 1 0 1797224205 69861376 15593 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9062/statm): 17056 15593 145 145 0 16911 0
[pid=9062] vsize: 68224
Current children cumulated CPU time (s) 758.99
Current children cumulated vsize (Kb) 70348

[startup+770.187 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 9062
Raw data (/proc/9058/stat): 9058 (minisat+_script) S 9057 9058 6847 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797224201 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9058/statm): 531 226 485 147 0 384 0
[pid=9058] vsize: 2124
Raw data (/proc/9062/stat): 9062 (minisat+_64-bit) R 9058 9058 6847 0 -1 0 16183 0 0 0 76786 111 0 0 25 0 1 0 1797224205 70217728 15681 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9062/statm): 17143 15681 145 145 0 16998 0
[pid=9062] vsize: 68572
Current children cumulated CPU time (s) 768.98
Current children cumulated vsize (Kb) 70696

[startup+780.187 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 9062
Raw data (/proc/9058/stat): 9058 (minisat+_script) S 9057 9058 6847 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797224201 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9058/statm): 531 226 485 147 0 384 0
[pid=9058] vsize: 2124
Raw data (/proc/9062/stat): 9062 (minisat+_64-bit) R 9058 9058 6847 0 -1 0 16296 0 0 0 77785 112 0 0 25 0 1 0 1797224205 70684672 15794 4294967295 134512640 135094434 3221224432 3221223088 134557950 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9062/statm): 17257 15794 145 145 0 17112 0
[pid=9062] vsize: 69028
Current children cumulated CPU time (s) 778.98
Current children cumulated vsize (Kb) 71152

[startup+790.188 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 9062
Raw data (/proc/9058/stat): 9058 (minisat+_script) S 9057 9058 6847 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797224201 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9058/statm): 531 226 485 147 0 384 0
[pid=9058] vsize: 2124
Raw data (/proc/9062/stat): 9062 (minisat+_64-bit) R 9058 9058 6847 0 -1 0 16402 0 0 0 78783 112 0 0 25 0 1 0 1797224205 71110656 15900 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9062/statm): 17361 15900 145 145 0 17216 0
[pid=9062] vsize: 69444
Current children cumulated CPU time (s) 788.96
Current children cumulated vsize (Kb) 71568

[startup+800.189 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 9062
Raw data (/proc/9058/stat): 9058 (minisat+_script) S 9057 9058 6847 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797224201 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9058/statm): 531 226 485 147 0 384 0
[pid=9058] vsize: 2124
Raw data (/proc/9062/stat): 9062 (minisat+_64-bit) R 9058 9058 6847 0 -1 0 16468 0 0 0 79782 113 0 0 25 0 1 0 1797224205 71372800 15966 4294967295 134512640 135094434 3221224432 3221223104 134555568 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9062/statm): 17425 15966 145 145 0 17280 0
[pid=9062] vsize: 69700
Current children cumulated CPU time (s) 798.96
Current children cumulated vsize (Kb) 71824

[startup+810.19 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 9062
Raw data (/proc/9058/stat): 9058 (minisat+_script) S 9057 9058 6847 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797224201 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9058/statm): 531 226 485 147 0 384 0
[pid=9058] vsize: 2124
Raw data (/proc/9062/stat): 9062 (minisat+_64-bit) R 9058 9058 6847 0 -1 0 16539 0 0 0 80781 114 0 0 25 0 1 0 1797224205 71667712 16037 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9062/statm): 17497 16037 145 145 0 17352 0
[pid=9062] vsize: 69988
Current children cumulated CPU time (s) 808.96
Current children cumulated vsize (Kb) 72112

[startup+820.19 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 9062
Raw data (/proc/9058/stat): 9058 (minisat+_script) S 9057 9058 6847 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797224201 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9058/statm): 531 226 485 147 0 384 0
[pid=9058] vsize: 2124
Raw data (/proc/9062/stat): 9062 (minisat+_64-bit) R 9058 9058 6847 0 -1 0 16599 0 0 0 81780 114 0 0 25 0 1 0 1797224205 71909376 16097 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9062/statm): 17556 16097 145 145 0 17411 0
[pid=9062] vsize: 70224
Current children cumulated CPU time (s) 818.95
Current children cumulated vsize (Kb) 72348

[startup+830.191 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 9062
Raw data (/proc/9058/stat): 9058 (minisat+_script) S 9057 9058 6847 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797224201 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9058/statm): 531 226 485 147 0 384 0
[pid=9058] vsize: 2124
Raw data (/proc/9062/stat): 9062 (minisat+_64-bit) R 9058 9058 6847 0 -1 0 16668 0 0 0 82779 115 0 0 25 0 1 0 1797224205 72192000 16166 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9062/statm): 17625 16166 145 145 0 17480 0
[pid=9062] vsize: 70500
Current children cumulated CPU time (s) 828.95
Current children cumulated vsize (Kb) 72624

[startup+840.192 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 9062
Raw data (/proc/9058/stat): 9058 (minisat+_script) S 9057 9058 6847 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797224201 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9058/statm): 531 226 485 147 0 384 0
[pid=9058] vsize: 2124
Raw data (/proc/9062/stat): 9062 (minisat+_64-bit) R 9058 9058 6847 0 -1 0 16724 0 0 0 83778 115 0 0 25 0 1 0 1797224205 72413184 16222 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9062/statm): 17679 16222 145 145 0 17534 0
[pid=9062] vsize: 70716
Current children cumulated CPU time (s) 838.94
Current children cumulated vsize (Kb) 72840

[startup+850.192 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 9062
Raw data (/proc/9058/stat): 9058 (minisat+_script) S 9057 9058 6847 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797224201 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9058/statm): 531 226 485 147 0 384 0
[pid=9058] vsize: 2124
Raw data (/proc/9062/stat): 9062 (minisat+_64-bit) R 9058 9058 6847 0 -1 0 16779 0 0 0 84778 115 0 0 25 0 1 0 1797224205 72634368 16277 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9062/statm): 17733 16277 145 145 0 17588 0
[pid=9062] vsize: 70932
Current children cumulated CPU time (s) 848.94
Current children cumulated vsize (Kb) 73056

[startup+860.193 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 9062
Raw data (/proc/9058/stat): 9058 (minisat+_script) S 9057 9058 6847 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797224201 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9058/statm): 531 226 485 147 0 384 0
[pid=9058] vsize: 2124
Raw data (/proc/9062/stat): 9062 (minisat+_64-bit) R 9058 9058 6847 0 -1 0 16837 0 0 0 85777 115 0 0 25 0 1 0 1797224205 72871936 16335 4294967295 134512640 135094434 3221224432 3221223088 134557849 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9062/statm): 17791 16335 145 145 0 17646 0
[pid=9062] vsize: 71164
Current children cumulated CPU time (s) 858.93
Current children cumulated vsize (Kb) 73288

[startup+870.193 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 9062
Raw data (/proc/9058/stat): 9058 (minisat+_script) S 9057 9058 6847 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797224201 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9058/statm): 531 226 485 147 0 384 0
[pid=9058] vsize: 2124
Raw data (/proc/9062/stat): 9062 (minisat+_64-bit) R 9058 9058 6847 0 -1 0 16895 0 0 0 86776 116 0 0 25 0 1 0 1797224205 73105408 16393 4294967295 134512640 135094434 3221224432 3221223088 134558227 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9062/statm): 17848 16393 145 145 0 17703 0
[pid=9062] vsize: 71392
Current children cumulated CPU time (s) 868.93
Current children cumulated vsize (Kb) 73516

[startup+880.194 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 9062
Raw data (/proc/9058/stat): 9058 (minisat+_script) S 9057 9058 6847 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797224201 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9058/statm): 531 226 485 147 0 384 0
[pid=9058] vsize: 2124
Raw data (/proc/9062/stat): 9062 (minisat+_64-bit) R 9058 9058 6847 0 -1 0 16993 0 0 0 87774 116 0 0 25 0 1 0 1797224205 73498624 16491 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9062/statm): 17944 16491 145 145 0 17799 0
[pid=9062] vsize: 71776
Current children cumulated CPU time (s) 878.91
Current children cumulated vsize (Kb) 73900

[startup+890.195 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 9062
Raw data (/proc/9058/stat): 9058 (minisat+_script) S 9057 9058 6847 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797224201 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9058/statm): 531 226 485 147 0 384 0
[pid=9058] vsize: 2124
Raw data (/proc/9062/stat): 9062 (minisat+_64-bit) R 9058 9058 6847 0 -1 0 17095 0 0 0 88773 117 0 0 25 0 1 0 1797224205 73912320 16593 4294967295 134512640 135094434 3221224432 3221223056 134557565 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9062/statm): 18045 16593 145 145 0 17900 0
[pid=9062] vsize: 72180
Current children cumulated CPU time (s) 888.91
Current children cumulated vsize (Kb) 74304

[startup+900.196 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 9062
Raw data (/proc/9058/stat): 9058 (minisat+_script) S 9057 9058 6847 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797224201 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9058/statm): 531 226 485 147 0 384 0
[pid=9058] vsize: 2124
Raw data (/proc/9062/stat): 9062 (minisat+_64-bit) R 9058 9058 6847 0 -1 0 17198 0 0 0 89772 118 0 0 25 0 1 0 1797224205 74330112 16696 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9062/statm): 18147 16696 145 145 0 18002 0
[pid=9062] vsize: 72588
Current children cumulated CPU time (s) 898.91
Current children cumulated vsize (Kb) 74712

[startup+910.197 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 9062
Raw data (/proc/9058/stat): 9058 (minisat+_script) S 9057 9058 6847 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797224201 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9058/statm): 531 226 485 147 0 384 0
[pid=9058] vsize: 2124
Raw data (/proc/9062/stat): 9062 (minisat+_64-bit) R 9058 9058 6847 0 -1 0 17314 0 0 0 90770 118 0 0 25 0 1 0 1797224205 74801152 16812 4294967295 134512640 135094434 3221224432 3221223056 134557696 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9062/statm): 18262 16812 145 145 0 18117 0
[pid=9062] vsize: 73048
Current children cumulated CPU time (s) 908.89
Current children cumulated vsize (Kb) 75172

[startup+920.197 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 9062
Raw data (/proc/9058/stat): 9058 (minisat+_script) S 9057 9058 6847 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797224201 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9058/statm): 531 226 485 147 0 384 0
[pid=9058] vsize: 2124
Raw data (/proc/9062/stat): 9062 (minisat+_64-bit) R 9058 9058 6847 0 -1 0 17399 0 0 0 91768 119 0 0 25 0 1 0 1797224205 75145216 16897 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9062/statm): 18346 16897 145 145 0 18201 0
[pid=9062] vsize: 73384
Current children cumulated CPU time (s) 918.88
Current children cumulated vsize (Kb) 75508

[startup+930.198 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 9062
Raw data (/proc/9058/stat): 9058 (minisat+_script) S 9057 9058 6847 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797224201 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9058/statm): 531 226 485 147 0 384 0
[pid=9058] vsize: 2124
Raw data (/proc/9062/stat): 9062 (minisat+_64-bit) R 9058 9058 6847 0 -1 0 17522 0 0 0 92766 120 0 0 25 0 1 0 1797224205 75644928 17020 4294967295 134512640 135094434 3221224432 3221223044 134563024 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9062/statm): 18468 17020 145 145 0 18323 0
[pid=9062] vsize: 73872
Current children cumulated CPU time (s) 928.87
Current children cumulated vsize (Kb) 75996

[startup+940.199 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 9062
Raw data (/proc/9058/stat): 9058 (minisat+_script) S 9057 9058 6847 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797224201 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9058/statm): 531 226 485 147 0 384 0
[pid=9058] vsize: 2124
Raw data (/proc/9062/stat): 9062 (minisat+_64-bit) R 9058 9058 6847 0 -1 0 17784 0 0 0 93761 122 0 0 25 0 1 0 1797224205 76709888 17282 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9062/statm): 18728 17282 145 145 0 18583 0
[pid=9062] vsize: 74912
Current children cumulated CPU time (s) 938.84
Current children cumulated vsize (Kb) 77036

[startup+950.201 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 9062
Raw data (/proc/9058/stat): 9058 (minisat+_script) S 9057 9058 6847 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797224201 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9058/statm): 531 226 485 147 0 384 0
[pid=9058] vsize: 2124
Raw data (/proc/9062/stat): 9062 (minisat+_64-bit) R 9058 9058 6847 0 -1 0 17936 0 0 0 94758 123 0 0 25 0 1 0 1797224205 77328384 17434 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9062/statm): 18879 17434 145 145 0 18734 0
[pid=9062] vsize: 75516
Current children cumulated CPU time (s) 948.82
Current children cumulated vsize (Kb) 77640

[startup+960.202 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 9062
Raw data (/proc/9058/stat): 9058 (minisat+_script) S 9057 9058 6847 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797224201 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9058/statm): 531 226 485 147 0 384 0
[pid=9058] vsize: 2124
Raw data (/proc/9062/stat): 9062 (minisat+_64-bit) R 9058 9058 6847 0 -1 0 17994 0 0 0 95758 124 0 0 25 0 1 0 1797224205 77561856 17492 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9062/statm): 18936 17492 145 145 0 18791 0
[pid=9062] vsize: 75744
Current children cumulated CPU time (s) 958.83
Current children cumulated vsize (Kb) 77868

[startup+970.203 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 9062
Raw data (/proc/9058/stat): 9058 (minisat+_script) S 9057 9058 6847 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797224201 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9058/statm): 531 226 485 147 0 384 0
[pid=9058] vsize: 2124
Raw data (/proc/9062/stat): 9062 (minisat+_64-bit) R 9058 9058 6847 0 -1 0 18043 0 0 0 96757 124 0 0 25 0 1 0 1797224205 77762560 17541 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9062/statm): 18985 17541 145 145 0 18840 0
[pid=9062] vsize: 75940
Current children cumulated CPU time (s) 968.82
Current children cumulated vsize (Kb) 78064

[startup+980.204 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 9062
Raw data (/proc/9058/stat): 9058 (minisat+_script) S 9057 9058 6847 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797224201 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9058/statm): 531 226 485 147 0 384 0
[pid=9058] vsize: 2124
Raw data (/proc/9062/stat): 9062 (minisat+_64-bit) T 9058 9058 6847 0 -1 0 18101 0 0 0 97756 125 0 0 25 0 1 0 1797224205 78000128 17599 4294967295 134512640 135094434 3221224432 3221222796 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/9062/statm): 19043 17599 145 145 0 18898 0
[pid=9062] vsize: 76172
Current children cumulated CPU time (s) 978.82
Current children cumulated vsize (Kb) 78296

[startup+990.204 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 9062
Raw data (/proc/9058/stat): 9058 (minisat+_script) S 9057 9058 6847 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797224201 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9058/statm): 531 226 485 147 0 384 0
[pid=9058] vsize: 2124
Raw data (/proc/9062/stat): 9062 (minisat+_64-bit) R 9058 9058 6847 0 -1 0 18164 0 0 0 98756 125 0 0 25 0 1 0 1797224205 78262272 17662 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9062/statm): 19107 17662 145 145 0 18962 0
[pid=9062] vsize: 76428
Current children cumulated CPU time (s) 988.82
Current children cumulated vsize (Kb) 78552

[startup+1000.21 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 9062
Raw data (/proc/9058/stat): 9058 (minisat+_script) S 9057 9058 6847 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797224201 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9058/statm): 531 226 485 147 0 384 0
[pid=9058] vsize: 2124
Raw data (/proc/9062/stat): 9062 (minisat+_64-bit) R 9058 9058 6847 0 -1 0 18323 0 0 0 99753 126 0 0 25 0 1 0 1797224205 78934016 17821 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9062/statm): 19271 17821 145 145 0 19126 0
[pid=9062] vsize: 77084
Current children cumulated CPU time (s) 998.8
Current children cumulated vsize (Kb) 79208

[startup+1010.21 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 9062
Raw data (/proc/9058/stat): 9058 (minisat+_script) S 9057 9058 6847 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797224201 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9058/statm): 531 226 485 147 0 384 0
[pid=9058] vsize: 2124
Raw data (/proc/9062/stat): 9062 (minisat+_64-bit) R 9058 9058 6847 0 -1 0 18393 0 0 0 100753 126 0 0 25 0 1 0 1797224205 79212544 17891 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9062/statm): 19339 17891 145 145 0 19194 0
[pid=9062] vsize: 77356
Current children cumulated CPU time (s) 1008.8
Current children cumulated vsize (Kb) 79480

[startup+1020.21 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 9062
Raw data (/proc/9058/stat): 9058 (minisat+_script) S 9057 9058 6847 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797224201 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9058/statm): 531 226 485 147 0 384 0
[pid=9058] vsize: 2124
Raw data (/proc/9062/stat): 9062 (minisat+_64-bit) R 9058 9058 6847 0 -1 0 18537 0 0 0 101750 128 0 0 25 0 1 0 1797224205 79790080 18035 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9062/statm): 19480 18035 145 145 0 19335 0
[pid=9062] vsize: 77920
Current children cumulated CPU time (s) 1018.79
Current children cumulated vsize (Kb) 80044

[startup+1030.21 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 9062
Raw data (/proc/9058/stat): 9058 (minisat+_script) S 9057 9058 6847 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797224201 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9058/statm): 531 226 485 147 0 384 0
[pid=9058] vsize: 2124
Raw data (/proc/9062/stat): 9062 (minisat+_64-bit) R 9058 9058 6847 0 -1 0 18687 0 0 0 102748 129 0 0 25 0 1 0 1797224205 80392192 18185 4294967295 134512640 135094434 3221224432 3221223088 134557903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9062/statm): 19627 18185 145 145 0 19482 0
[pid=9062] vsize: 78508
Current children cumulated CPU time (s) 1028.78
Current children cumulated vsize (Kb) 80632

[startup+1040.21 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 9062
Raw data (/proc/9058/stat): 9058 (minisat+_script) S 9057 9058 6847 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797224201 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9058/statm): 531 226 485 147 0 384 0
[pid=9058] vsize: 2124
Raw data (/proc/9062/stat): 9062 (minisat+_64-bit) R 9058 9058 6847 0 -1 0 18784 0 0 0 103746 130 0 0 25 0 1 0 1797224205 80789504 18282 4294967295 134512640 135094434 3221224432 3221223120 134554676 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9062/statm): 19724 18282 145 145 0 19579 0
[pid=9062] vsize: 78896
Current children cumulated CPU time (s) 1038.77
Current children cumulated vsize (Kb) 81020

[startup+1050.21 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 9062
Raw data (/proc/9058/stat): 9058 (minisat+_script) S 9057 9058 6847 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797224201 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9058/statm): 531 226 485 147 0 384 0
[pid=9058] vsize: 2124
Raw data (/proc/9062/stat): 9062 (minisat+_64-bit) R 9058 9058 6847 0 -1 0 18899 0 0 0 104745 130 0 0 25 0 1 0 1797224205 81272832 18397 4294967295 134512640 135094434 3221224432 3221223088 134558210 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9062/statm): 19842 18397 145 145 0 19697 0
[pid=9062] vsize: 79368
Current children cumulated CPU time (s) 1048.76
Current children cumulated vsize (Kb) 81492

[startup+1060.21 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 9062
Raw data (/proc/9058/stat): 9058 (minisat+_script) S 9057 9058 6847 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797224201 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9058/statm): 531 226 485 147 0 384 0
[pid=9058] vsize: 2124
Raw data (/proc/9062/stat): 9062 (minisat+_64-bit) R 9058 9058 6847 0 -1 0 18990 0 0 0 105744 131 0 0 25 0 1 0 1797224205 81633280 18488 4294967295 134512640 135094434 3221224432 3221223068 134557560 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9062/statm): 19930 18488 145 145 0 19785 0
[pid=9062] vsize: 79720
Current children cumulated CPU time (s) 1058.76
Current children cumulated vsize (Kb) 81844

[startup+1070.21 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 9062
Raw data (/proc/9058/stat): 9058 (minisat+_script) S 9057 9058 6847 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797224201 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9058/statm): 531 226 485 147 0 384 0
[pid=9058] vsize: 2124
Raw data (/proc/9062/stat): 9062 (minisat+_64-bit) R 9058 9058 6847 0 -1 0 19320 0 0 0 106737 134 0 0 25 0 1 0 1797224205 82976768 18818 4294967295 134512640 135094434 3221224432 3221223104 134555574 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9062/statm): 20258 18818 145 145 0 20113 0
[pid=9062] vsize: 81032
Current children cumulated CPU time (s) 1068.72
Current children cumulated vsize (Kb) 83156

[startup+1080.21 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 9062
Raw data (/proc/9058/stat): 9058 (minisat+_script) S 9057 9058 6847 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797224201 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9058/statm): 531 226 485 147 0 384 0
[pid=9058] vsize: 2124
Raw data (/proc/9062/stat): 9062 (minisat+_64-bit) R 9058 9058 6847 0 -1 0 19486 0 0 0 107735 134 0 0 25 0 1 0 1797224205 83640320 18984 4294967295 134512640 135094434 3221224432 3221223056 134557691 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9062/statm): 20420 18984 145 145 0 20275 0
[pid=9062] vsize: 81680
Current children cumulated CPU time (s) 1078.7
Current children cumulated vsize (Kb) 83804

[startup+1090.21 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 9062
Raw data (/proc/9058/stat): 9058 (minisat+_script) S 9057 9058 6847 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797224201 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9058/statm): 531 226 485 147 0 384 0
[pid=9058] vsize: 2124
Raw data (/proc/9062/stat): 9062 (minisat+_64-bit) R 9058 9058 6847 0 -1 0 19598 0 0 0 108733 135 0 0 25 0 1 0 1797224205 84090880 19096 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9062/statm): 20530 19096 145 145 0 20385 0
[pid=9062] vsize: 82120
Current children cumulated CPU time (s) 1088.69
Current children cumulated vsize (Kb) 84244

[startup+1100.21 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 9062
Raw data (/proc/9058/stat): 9058 (minisat+_script) S 9057 9058 6847 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797224201 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9058/statm): 531 226 485 147 0 384 0
[pid=9058] vsize: 2124
Raw data (/proc/9062/stat): 9062 (minisat+_64-bit) R 9058 9058 6847 0 -1 0 19703 0 0 0 109732 136 0 0 25 0 1 0 1797224205 84525056 19201 4294967295 134512640 135094434 3221224432 3221223120 134554723 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9062/statm): 20636 19201 145 145 0 20491 0
[pid=9062] vsize: 82544
Current children cumulated CPU time (s) 1098.69
Current children cumulated vsize (Kb) 84668

[startup+1110.21 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 9062
Raw data (/proc/9058/stat): 9058 (minisat+_script) S 9057 9058 6847 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797224201 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9058/statm): 531 226 485 147 0 384 0
[pid=9058] vsize: 2124
Raw data (/proc/9062/stat): 9062 (minisat+_64-bit) R 9058 9058 6847 0 -1 0 19806 0 0 0 110730 136 0 0 25 0 1 0 1797224205 84942848 19304 4294967295 134512640 135094434 3221224432 3221223088 134557920 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9062/statm): 20738 19304 145 145 0 20593 0
[pid=9062] vsize: 82952
Current children cumulated CPU time (s) 1108.67
Current children cumulated vsize (Kb) 85076

[startup+1120.22 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 9062
Raw data (/proc/9058/stat): 9058 (minisat+_script) S 9057 9058 6847 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797224201 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9058/statm): 531 226 485 147 0 384 0
[pid=9058] vsize: 2124
Raw data (/proc/9062/stat): 9062 (minisat+_64-bit) R 9058 9058 6847 0 -1 0 19955 0 0 0 111727 138 0 0 25 0 1 0 1797224205 85540864 19453 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9062/statm): 20884 19453 145 145 0 20739 0
[pid=9062] vsize: 83536
Current children cumulated CPU time (s) 1118.66
Current children cumulated vsize (Kb) 85660

[startup+1130.22 s]
Raw data (loadavg): 1.00 0.99 0.91 1/57 9062
Raw data (/proc/9058/stat): 9058 (minisat+_script) S 9057 9058 6847 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797224201 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9058/statm): 531 226 485 147 0 384 0
[pid=9058] vsize: 2124
Raw data (/proc/9062/stat): 9062 (minisat+_64-bit) T 9058 9058 6847 0 -1 0 20112 0 0 0 112724 139 0 0 25 0 1 0 1797224205 86175744 19610 4294967295 134512640 135094434 3221224432 3221222796 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/9062/statm): 21039 19610 145 145 0 20894 0
[pid=9062] vsize: 84156
Current children cumulated CPU time (s) 1128.64
Current children cumulated vsize (Kb) 86280

[startup+1140.22 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 9062
Raw data (/proc/9058/stat): 9058 (minisat+_script) S 9057 9058 6847 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797224201 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9058/statm): 531 226 485 147 0 384 0
[pid=9058] vsize: 2124
Raw data (/proc/9062/stat): 9062 (minisat+_64-bit) R 9058 9058 6847 0 -1 0 20210 0 0 0 113722 140 0 0 25 0 1 0 1797224205 86573056 19708 4294967295 134512640 135094434 3221224432 3221223104 134556266 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9062/statm): 21136 19708 145 145 0 20991 0
[pid=9062] vsize: 84544
Current children cumulated CPU time (s) 1138.63
Current children cumulated vsize (Kb) 86668

[startup+1150.22 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 9062
Raw data (/proc/9058/stat): 9058 (minisat+_script) S 9057 9058 6847 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797224201 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9058/statm): 531 226 485 147 0 384 0
[pid=9058] vsize: 2124
Raw data (/proc/9062/stat): 9062 (minisat+_64-bit) R 9058 9058 6847 0 -1 0 20296 0 0 0 114721 140 0 0 25 0 1 0 1797224205 86933504 19794 4294967295 134512640 135094434 3221224432 3221223072 134562104 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9062/statm): 21224 19794 145 145 0 21079 0
[pid=9062] vsize: 84896
Current children cumulated CPU time (s) 1148.62
Current children cumulated vsize (Kb) 87020

[startup+1160.22 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 9062
Raw data (/proc/9058/stat): 9058 (minisat+_script) S 9057 9058 6847 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797224201 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9058/statm): 531 226 485 147 0 384 0
[pid=9058] vsize: 2124
Raw data (/proc/9062/stat): 9062 (minisat+_64-bit) R 9058 9058 6847 0 -1 0 20450 0 0 0 115719 141 0 0 25 0 1 0 1797224205 87556096 19948 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9062/statm): 21376 19948 145 145 0 21231 0
[pid=9062] vsize: 85504
Current children cumulated CPU time (s) 1158.61
Current children cumulated vsize (Kb) 87628

[startup+1170.22 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 9062
Raw data (/proc/9058/stat): 9058 (minisat+_script) S 9057 9058 6847 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797224201 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9058/statm): 531 226 485 147 0 384 0
[pid=9058] vsize: 2124
Raw data (/proc/9062/stat): 9062 (minisat+_64-bit) R 9058 9058 6847 0 -1 0 20632 0 0 0 116715 143 0 0 25 0 1 0 1797224205 88293376 20130 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9062/statm): 21556 20130 145 145 0 21411 0
[pid=9062] vsize: 86224
Current children cumulated CPU time (s) 1168.59
Current children cumulated vsize (Kb) 88348

[startup+1180.22 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 9062
Raw data (/proc/9058/stat): 9058 (minisat+_script) S 9057 9058 6847 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797224201 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9058/statm): 531 226 485 147 0 384 0
[pid=9058] vsize: 2124
Raw data (/proc/9062/stat): 9062 (minisat+_64-bit) R 9058 9058 6847 0 -1 0 20858 0 0 0 117711 145 0 0 25 0 1 0 1797224205 89210880 20356 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9062/statm): 21780 20356 145 145 0 21635 0
[pid=9062] vsize: 87120
Current children cumulated CPU time (s) 1178.57
Current children cumulated vsize (Kb) 89244

[startup+1190.22 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 9062
Raw data (/proc/9058/stat): 9058 (minisat+_script) S 9057 9058 6847 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797224201 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9058/statm): 531 226 485 147 0 384 0
[pid=9058] vsize: 2124
Raw data (/proc/9062/stat): 9062 (minisat+_64-bit) R 9058 9058 6847 0 -1 0 21121 0 0 0 118706 147 0 0 25 0 1 0 1797224205 90284032 20619 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9062/statm): 22042 20619 145 145 0 21897 0
[pid=9062] vsize: 88168
Current children cumulated CPU time (s) 1188.54
Current children cumulated vsize (Kb) 90292

[startup+1200.22 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 9062
Raw data (/proc/9058/stat): 9058 (minisat+_script) S 9057 9058 6847 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797224201 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9058/statm): 531 226 485 147 0 384 0
[pid=9058] vsize: 2124
Raw data (/proc/9062/stat): 9062 (minisat+_64-bit) R 9058 9058 6847 0 -1 0 21397 0 0 0 119701 149 0 0 25 0 1 0 1797224205 91406336 20895 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9062/statm): 22316 20895 145 145 0 22171 0
[pid=9062] vsize: 89264
Current children cumulated CPU time (s) 1198.51
Current children cumulated vsize (Kb) 91388

[startup+1210.23 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 9062
Raw data (/proc/9058/stat): 9058 (minisat+_script) S 9057 9058 6847 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797224201 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9058/statm): 531 226 485 147 0 384 0
[pid=9058] vsize: 2124
Raw data (/proc/9062/stat): 9062 (minisat+_64-bit) R 9058 9058 6847 0 -1 0 21698 0 0 0 120695 151 0 0 25 0 1 0 1797224205 92639232 21196 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9062/statm): 22617 21196 145 145 0 22472 0
[pid=9062] vsize: 90468
Current children cumulated CPU time (s) 1208.47
Current children cumulated vsize (Kb) 92592



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.23 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 9062
Raw data (/proc/9058/stat): 9058 (minisat+_script) S 9057 9058 6847 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797224201 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9058/statm): 531 226 485 147 0 384 0
[pid=9058] vsize: 2124
Raw data (/proc/9062/stat): 9062 (minisat+_64-bit) R 9058 9058 6847 0 -1 0 21698 0 0 0 120695 151 0 0 25 0 1 0 1797224205 92639232 21196 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9062/statm): 22617 21196 145 145 0 22472 0
[pid=9062] vsize: 90468
Current children cumulated CPU time (s) 1208.47
Current children cumulated vsize (Kb) 92592

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

Child status: 0
Real time (s): 1210.27
CPU time (s): 1208.52
CPU user time (s): 1206.96
CPU system time (s): 1.55776
CPU usage (%): 99.8552
Max. virtual memory (cumulated for all children) (Kb): 92592

Verifier Data

ERROR: no interpretation found !