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/plato.asu.edu/pub/unibo/normalized-mps-v2-13-7-roll3000.opb
MD5SUMa7433a26e92d47a3d337e0c2b98bd409
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 6335

Launcher Data

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

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        899612 kB
Buffers:         19588 kB
Cached:          87440 kB
SwapCached:        888 kB
Active:          24152 kB
Inactive:        85544 kB
HighTotal:      131008 kB
HighFree:        40040 kB
LowTotal:       903652 kB
LowFree:        859572 kB
SwapTotal:     2097892 kB
SwapFree:      2096524 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5728 kB
Slab:            19520 kB
Committed_AS:    64168 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-09-20 06:01:24 (client local time) WITH STATUS 0 IN 1208.41 SECONDS
stats: 3497 7 1208.41 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/28408/stat): 28408 (minisat+_script) R 28407 28408 4419 0 -1 0 19 0 0 0 0 0 0 0 22 0 1 0 1856122132 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 1 0 0
Raw data (/proc/28408/statm): 174 3 169 147 0 27 0
[pid=28408] 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=28409
New process pid=28410
New process pid=28411
execve syscall for /bin/sed executable
One traced child (pid=28410) 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=28411) exited with status: 0
One traced child (pid=28409) exited with status: 0
New process pid=28412
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc25/normalized-mps-v2-13-7-roll3000.opb

[startup+10.0041 s]
Raw data (loadavg): 0.93 0.95 0.91 2/57 28412
Raw data (/proc/28408/stat): 28408 (minisat+_script) S 28407 28408 4419 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856122132 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28408/statm): 531 226 485 147 0 384 0
[pid=28408] vsize: 2124
Raw data (/proc/28412/stat): 28412 (minisat+_64-bit) R 28408 28408 4419 0 -1 0 3087 0 0 0 966 15 0 0 25 0 1 0 1856122137 11653120 2591 4294967295 134512640 135094434 3221224432 3221221552 134677065 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28412/statm): 2845 2591 145 145 0 2700 0
[pid=28412] vsize: 11380
Current children cumulated CPU time (s) 9.82
Current children cumulated vsize (Kb) 13504

[startup+20.0057 s]
Raw data (loadavg): 0.94 0.96 0.91 2/57 28412
Raw data (/proc/28408/stat): 28408 (minisat+_script) S 28407 28408 4419 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856122132 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28408/statm): 531 226 485 147 0 384 0
[pid=28408] vsize: 2124
Raw data (/proc/28412/stat): 28412 (minisat+_64-bit) R 28408 28408 4419 0 -1 0 8720 0 0 0 1916 39 0 0 25 0 1 0 1856122137 39190528 8221 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28412/statm): 9568 8221 145 145 0 9423 0
[pid=28412] vsize: 38272
Current children cumulated CPU time (s) 19.56
Current children cumulated vsize (Kb) 40396

[startup+30.0063 s]
Raw data (loadavg): 0.95 0.96 0.91 2/57 28412
Raw data (/proc/28408/stat): 28408 (minisat+_script) S 28407 28408 4419 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856122132 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28408/statm): 531 226 485 147 0 384 0
[pid=28408] vsize: 2124
Raw data (/proc/28412/stat): 28412 (minisat+_64-bit) R 28408 28408 4419 0 -1 0 8753 0 0 0 2916 39 0 0 25 0 1 0 1856122137 39337984 8254 4294967295 134512640 135094434 3221224432 3221223044 134563046 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28412/statm): 9604 8254 145 145 0 9459 0
[pid=28412] vsize: 38416
Current children cumulated CPU time (s) 29.56
Current children cumulated vsize (Kb) 40540

[startup+40.0069 s]
Raw data (loadavg): 0.95 0.96 0.91 2/57 28412
Raw data (/proc/28408/stat): 28408 (minisat+_script) S 28407 28408 4419 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856122132 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28408/statm): 531 226 485 147 0 384 0
[pid=28408] vsize: 2124
Raw data (/proc/28412/stat): 28412 (minisat+_64-bit) R 28408 28408 4419 0 -1 0 8784 0 0 0 3914 40 0 0 25 0 1 0 1856122137 39452672 8285 4294967295 134512640 135094434 3221224432 3221223088 134557950 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28412/statm): 9632 8285 145 145 0 9487 0
[pid=28412] vsize: 38528
Current children cumulated CPU time (s) 39.55
Current children cumulated vsize (Kb) 40652

[startup+50.0075 s]
Raw data (loadavg): 0.96 0.96 0.91 2/57 28412
Raw data (/proc/28408/stat): 28408 (minisat+_script) S 28407 28408 4419 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856122132 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28408/statm): 531 226 485 147 0 384 0
[pid=28408] vsize: 2124
Raw data (/proc/28412/stat): 28412 (minisat+_64-bit) R 28408 28408 4419 0 -1 0 8862 0 0 0 4912 42 0 0 25 0 1 0 1856122137 39780352 8363 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28412/statm): 9712 8363 145 145 0 9567 0
[pid=28412] vsize: 38848
Current children cumulated CPU time (s) 49.55
Current children cumulated vsize (Kb) 40972

[startup+60.0081 s]
Raw data (loadavg): 0.97 0.96 0.91 2/57 28412
Raw data (/proc/28408/stat): 28408 (minisat+_script) S 28407 28408 4419 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856122132 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28408/statm): 531 226 485 147 0 384 0
[pid=28408] vsize: 2124
Raw data (/proc/28412/stat): 28412 (minisat+_64-bit) R 28408 28408 4419 0 -1 0 8924 0 0 0 5911 43 0 0 25 0 1 0 1856122137 40022016 8425 4294967295 134512640 135094434 3221224432 3221223088 134558402 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28412/statm): 9771 8425 145 145 0 9626 0
[pid=28412] vsize: 39084
Current children cumulated CPU time (s) 59.55
Current children cumulated vsize (Kb) 41208

[startup+70.0097 s]
Raw data (loadavg): 0.97 0.96 0.91 2/57 28412
Raw data (/proc/28408/stat): 28408 (minisat+_script) S 28407 28408 4419 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856122132 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28408/statm): 531 226 485 147 0 384 0
[pid=28408] vsize: 2124
Raw data (/proc/28412/stat): 28412 (minisat+_64-bit) R 28408 28408 4419 0 -1 0 9027 0 0 0 6909 43 0 0 25 0 1 0 1856122137 40411136 8528 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28412/statm): 9866 8528 145 145 0 9721 0
[pid=28412] vsize: 39464
Current children cumulated CPU time (s) 69.53
Current children cumulated vsize (Kb) 41588

[startup+80.0103 s]
Raw data (loadavg): 0.98 0.96 0.91 2/57 28412
Raw data (/proc/28408/stat): 28408 (minisat+_script) S 28407 28408 4419 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856122132 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28408/statm): 531 226 485 147 0 384 0
[pid=28408] vsize: 2124
Raw data (/proc/28412/stat): 28412 (minisat+_64-bit) R 28408 28408 4419 0 -1 0 9113 0 0 0 7907 45 0 0 25 0 1 0 1856122137 40816640 8614 4294967295 134512640 135094434 3221224432 3221223056 134557675 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28412/statm): 9965 8614 145 145 0 9820 0
[pid=28412] vsize: 39860
Current children cumulated CPU time (s) 79.53
Current children cumulated vsize (Kb) 41984

[startup+90.0109 s]
Raw data (loadavg): 0.98 0.96 0.91 2/57 28412
Raw data (/proc/28408/stat): 28408 (minisat+_script) S 28407 28408 4419 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856122132 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28408/statm): 531 226 485 147 0 384 0
[pid=28408] vsize: 2124
Raw data (/proc/28412/stat): 28412 (minisat+_64-bit) R 28408 28408 4419 0 -1 0 9215 0 0 0 8905 46 0 0 25 0 1 0 1856122137 41222144 8716 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28412/statm): 10064 8716 145 145 0 9919 0
[pid=28412] vsize: 40256
Current children cumulated CPU time (s) 89.52
Current children cumulated vsize (Kb) 42380

[startup+100.011 s]
Raw data (loadavg): 0.98 0.96 0.91 2/57 28412
Raw data (/proc/28408/stat): 28408 (minisat+_script) S 28407 28408 4419 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856122132 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28408/statm): 531 226 485 147 0 384 0
[pid=28408] vsize: 2124
Raw data (/proc/28412/stat): 28412 (minisat+_64-bit) R 28408 28408 4419 0 -1 0 9296 0 0 0 9902 47 0 0 25 0 1 0 1856122137 41541632 8797 4294967295 134512640 135094434 3221224432 3221223120 134554723 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28412/statm): 10142 8797 145 145 0 9997 0
[pid=28412] vsize: 40568
Current children cumulated CPU time (s) 99.5
Current children cumulated vsize (Kb) 42692

[startup+110.013 s]
Raw data (loadavg): 0.98 0.96 0.91 2/57 28412
Raw data (/proc/28408/stat): 28408 (minisat+_script) S 28407 28408 4419 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856122132 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28408/statm): 531 226 485 147 0 384 0
[pid=28408] vsize: 2124
Raw data (/proc/28412/stat): 28412 (minisat+_64-bit) R 28408 28408 4419 0 -1 0 9377 0 0 0 10901 48 0 0 25 0 1 0 1856122137 41865216 8878 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28412/statm): 10221 8878 145 145 0 10076 0
[pid=28412] vsize: 40884
Current children cumulated CPU time (s) 109.5
Current children cumulated vsize (Kb) 43008

[startup+120.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28412
Raw data (/proc/28408/stat): 28408 (minisat+_script) S 28407 28408 4419 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856122132 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28408/statm): 531 226 485 147 0 384 0
[pid=28408] vsize: 2124
Raw data (/proc/28412/stat): 28412 (minisat+_64-bit) R 28408 28408 4419 0 -1 0 9466 0 0 0 11899 49 0 0 25 0 1 0 1856122137 42209280 8967 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28412/statm): 10305 8967 145 145 0 10160 0
[pid=28412] vsize: 41220
Current children cumulated CPU time (s) 119.49
Current children cumulated vsize (Kb) 43344

[startup+130.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28412
Raw data (/proc/28408/stat): 28408 (minisat+_script) S 28407 28408 4419 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856122132 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28408/statm): 531 226 485 147 0 384 0
[pid=28408] vsize: 2124
Raw data (/proc/28412/stat): 28412 (minisat+_64-bit) R 28408 28408 4419 0 -1 0 9562 0 0 0 12897 50 0 0 25 0 1 0 1856122137 42590208 9063 4294967295 134512640 135094434 3221224432 3221223088 134558402 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28412/statm): 10398 9063 145 145 0 10253 0
[pid=28412] vsize: 41592
Current children cumulated CPU time (s) 129.48
Current children cumulated vsize (Kb) 43716

[startup+140.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28412
Raw data (/proc/28408/stat): 28408 (minisat+_script) S 28407 28408 4419 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856122132 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28408/statm): 531 226 485 147 0 384 0
[pid=28408] vsize: 2124
Raw data (/proc/28412/stat): 28412 (minisat+_64-bit) R 28408 28408 4419 0 -1 0 9641 0 0 0 13895 52 0 0 25 0 1 0 1856122137 43040768 9142 4294967295 134512640 135094434 3221224432 3221223088 134557879 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28412/statm): 10508 9142 145 145 0 10363 0
[pid=28412] vsize: 42032
Current children cumulated CPU time (s) 139.48
Current children cumulated vsize (Kb) 44156

[startup+150.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28412
Raw data (/proc/28408/stat): 28408 (minisat+_script) S 28407 28408 4419 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856122132 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28408/statm): 531 226 485 147 0 384 0
[pid=28408] vsize: 2124
Raw data (/proc/28412/stat): 28412 (minisat+_64-bit) R 28408 28408 4419 0 -1 0 9709 0 0 0 14893 53 0 0 25 0 1 0 1856122137 43311104 9210 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28412/statm): 10574 9210 145 145 0 10429 0
[pid=28412] vsize: 42296
Current children cumulated CPU time (s) 149.47
Current children cumulated vsize (Kb) 44420

[startup+160.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28412
Raw data (/proc/28408/stat): 28408 (minisat+_script) S 28407 28408 4419 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856122132 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28408/statm): 531 226 485 147 0 384 0
[pid=28408] vsize: 2124
Raw data (/proc/28412/stat): 28412 (minisat+_64-bit) R 28408 28408 4419 0 -1 0 9795 0 0 0 15891 54 0 0 25 0 1 0 1856122137 43659264 9296 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28412/statm): 10659 9296 145 145 0 10514 0
[pid=28412] vsize: 42636
Current children cumulated CPU time (s) 159.46
Current children cumulated vsize (Kb) 44760

[startup+170.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28412
Raw data (/proc/28408/stat): 28408 (minisat+_script) S 28407 28408 4419 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856122132 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28408/statm): 531 226 485 147 0 384 0
[pid=28408] vsize: 2124
Raw data (/proc/28412/stat): 28412 (minisat+_64-bit) R 28408 28408 4419 0 -1 0 9899 0 0 0 16888 55 0 0 25 0 1 0 1856122137 44068864 9400 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28412/statm): 10759 9400 145 145 0 10614 0
[pid=28412] vsize: 43036
Current children cumulated CPU time (s) 169.44
Current children cumulated vsize (Kb) 45160

[startup+180.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28412
Raw data (/proc/28408/stat): 28408 (minisat+_script) S 28407 28408 4419 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856122132 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28408/statm): 531 226 485 147 0 384 0
[pid=28408] vsize: 2124
Raw data (/proc/28412/stat): 28412 (minisat+_64-bit) R 28408 28408 4419 0 -1 0 9998 0 0 0 17885 57 0 0 25 0 1 0 1856122137 44462080 9499 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28412/statm): 10855 9499 145 145 0 10710 0
[pid=28412] vsize: 43420
Current children cumulated CPU time (s) 179.43
Current children cumulated vsize (Kb) 45544

[startup+190.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28412
Raw data (/proc/28408/stat): 28408 (minisat+_script) S 28407 28408 4419 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856122132 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28408/statm): 531 226 485 147 0 384 0
[pid=28408] vsize: 2124
Raw data (/proc/28412/stat): 28412 (minisat+_64-bit) R 28408 28408 4419 0 -1 0 10098 0 0 0 18883 58 0 0 25 0 1 0 1856122137 44863488 9599 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28412/statm): 10953 9599 145 145 0 10808 0
[pid=28412] vsize: 43812
Current children cumulated CPU time (s) 189.42
Current children cumulated vsize (Kb) 45936

[startup+200.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28412
Raw data (/proc/28408/stat): 28408 (minisat+_script) S 28407 28408 4419 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856122132 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28408/statm): 531 226 485 147 0 384 0
[pid=28408] vsize: 2124
Raw data (/proc/28412/stat): 28412 (minisat+_64-bit) R 28408 28408 4419 0 -1 0 10195 0 0 0 19881 59 0 0 25 0 1 0 1856122137 45248512 9696 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28412/statm): 11047 9696 145 145 0 10902 0
[pid=28412] vsize: 44188
Current children cumulated CPU time (s) 199.41
Current children cumulated vsize (Kb) 46312

[startup+210.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28412
Raw data (/proc/28408/stat): 28408 (minisat+_script) S 28407 28408 4419 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856122132 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28408/statm): 531 226 485 147 0 384 0
[pid=28408] vsize: 2124
Raw data (/proc/28412/stat): 28412 (minisat+_64-bit) R 28408 28408 4419 0 -1 0 10317 0 0 0 20878 60 0 0 25 0 1 0 1856122137 45731840 9818 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28412/statm): 11165 9818 145 145 0 11020 0
[pid=28412] vsize: 44660
Current children cumulated CPU time (s) 209.39
Current children cumulated vsize (Kb) 46784

[startup+220.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28412
Raw data (/proc/28408/stat): 28408 (minisat+_script) S 28407 28408 4419 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856122132 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28408/statm): 531 226 485 147 0 384 0
[pid=28408] vsize: 2124
Raw data (/proc/28412/stat): 28412 (minisat+_64-bit) R 28408 28408 4419 0 -1 0 10413 0 0 0 21876 61 0 0 25 0 1 0 1856122137 46116864 9914 4294967295 134512640 135094434 3221224432 3221223056 134557650 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28412/statm): 11259 9914 145 145 0 11114 0
[pid=28412] vsize: 45036
Current children cumulated CPU time (s) 219.38
Current children cumulated vsize (Kb) 47160

[startup+230.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28412
Raw data (/proc/28408/stat): 28408 (minisat+_script) S 28407 28408 4419 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856122132 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28408/statm): 531 226 485 147 0 384 0
[pid=28408] vsize: 2124
Raw data (/proc/28412/stat): 28412 (minisat+_64-bit) R 28408 28408 4419 0 -1 0 10494 0 0 0 22876 61 0 0 25 0 1 0 1856122137 46440448 9995 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28412/statm): 11338 9995 145 145 0 11193 0
[pid=28412] vsize: 45352
Current children cumulated CPU time (s) 229.38
Current children cumulated vsize (Kb) 47476

[startup+240.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28412
Raw data (/proc/28408/stat): 28408 (minisat+_script) S 28407 28408 4419 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856122132 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28408/statm): 531 226 485 147 0 384 0
[pid=28408] vsize: 2124
Raw data (/proc/28412/stat): 28412 (minisat+_64-bit) R 28408 28408 4419 0 -1 0 10654 0 0 0 23873 62 0 0 25 0 1 0 1856122137 47083520 10155 4294967295 134512640 135094434 3221224432 3221223092 134553487 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28412/statm): 11495 10155 145 145 0 11350 0
[pid=28412] vsize: 45980
Current children cumulated CPU time (s) 239.36
Current children cumulated vsize (Kb) 48104

[startup+250.024 s]
Raw data (loadavg): 0.99 0.97 0.91 1/57 28412
Raw data (/proc/28408/stat): 28408 (minisat+_script) S 28407 28408 4419 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856122132 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28408/statm): 531 226 485 147 0 384 0
[pid=28408] vsize: 2124
Raw data (/proc/28412/stat): 28412 (minisat+_64-bit) T 28408 28408 4419 0 -1 0 10762 0 0 0 24871 62 0 0 25 0 1 0 1856122137 47517696 10263 4294967295 134512640 135094434 3221224432 3221222796 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/28412/statm): 11601 10263 145 145 0 11456 0
[pid=28412] vsize: 46404
Current children cumulated CPU time (s) 249.34
Current children cumulated vsize (Kb) 48528

[startup+260.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28412
Raw data (/proc/28408/stat): 28408 (minisat+_script) S 28407 28408 4419 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856122132 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28408/statm): 531 226 485 147 0 384 0
[pid=28408] vsize: 2124
Raw data (/proc/28412/stat): 28412 (minisat+_64-bit) R 28408 28408 4419 0 -1 0 10841 0 0 0 25870 63 0 0 25 0 1 0 1856122137 47845376 10342 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28412/statm): 11681 10342 145 145 0 11536 0
[pid=28412] vsize: 46724
Current children cumulated CPU time (s) 259.34
Current children cumulated vsize (Kb) 48848

[startup+270.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28412
Raw data (/proc/28408/stat): 28408 (minisat+_script) S 28407 28408 4419 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856122132 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28408/statm): 531 226 485 147 0 384 0
[pid=28408] vsize: 2124
Raw data (/proc/28412/stat): 28412 (minisat+_64-bit) R 28408 28408 4419 0 -1 0 10941 0 0 0 26869 64 0 0 25 0 1 0 1856122137 48246784 10442 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28412/statm): 11779 10442 145 145 0 11634 0
[pid=28412] vsize: 47116
Current children cumulated CPU time (s) 269.34
Current children cumulated vsize (Kb) 49240

[startup+280.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28412
Raw data (/proc/28408/stat): 28408 (minisat+_script) S 28407 28408 4419 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856122132 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28408/statm): 531 226 485 147 0 384 0
[pid=28408] vsize: 2124
Raw data (/proc/28412/stat): 28412 (minisat+_64-bit) R 28408 28408 4419 0 -1 0 11110 0 0 0 27865 65 0 0 25 0 1 0 1856122137 49188864 10611 4294967295 134512640 135094434 3221224432 3221223088 134557903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28412/statm): 12009 10611 145 145 0 11864 0
[pid=28412] vsize: 48036
Current children cumulated CPU time (s) 279.31
Current children cumulated vsize (Kb) 50160

[startup+290.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28412
Raw data (/proc/28408/stat): 28408 (minisat+_script) S 28407 28408 4419 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856122132 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28408/statm): 531 226 485 147 0 384 0
[pid=28408] vsize: 2124
Raw data (/proc/28412/stat): 28412 (minisat+_64-bit) R 28408 28408 4419 0 -1 0 11249 0 0 0 28863 66 0 0 25 0 1 0 1856122137 49750016 10750 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28412/statm): 12146 10750 145 145 0 12001 0
[pid=28412] vsize: 48584
Current children cumulated CPU time (s) 289.3
Current children cumulated vsize (Kb) 50708

[startup+300.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28412
Raw data (/proc/28408/stat): 28408 (minisat+_script) S 28407 28408 4419 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856122132 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28408/statm): 531 226 485 147 0 384 0
[pid=28408] vsize: 2124
Raw data (/proc/28412/stat): 28412 (minisat+_64-bit) R 28408 28408 4419 0 -1 0 11329 0 0 0 29862 66 0 0 25 0 1 0 1856122137 50069504 10830 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28412/statm): 12224 10830 145 145 0 12079 0
[pid=28412] vsize: 48896
Current children cumulated CPU time (s) 299.29
Current children cumulated vsize (Kb) 51020

[startup+310.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28412
Raw data (/proc/28408/stat): 28408 (minisat+_script) S 28407 28408 4419 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856122132 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28408/statm): 531 226 485 147 0 384 0
[pid=28408] vsize: 2124
Raw data (/proc/28412/stat): 28412 (minisat+_64-bit) R 28408 28408 4419 0 -1 0 11396 0 0 0 30862 66 0 0 25 0 1 0 1856122137 50343936 10897 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28412/statm): 12291 10897 145 145 0 12146 0
[pid=28412] vsize: 49164
Current children cumulated CPU time (s) 309.29
Current children cumulated vsize (Kb) 51288

[startup+320.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28412
Raw data (/proc/28408/stat): 28408 (minisat+_script) S 28407 28408 4419 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856122132 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28408/statm): 531 226 485 147 0 384 0
[pid=28408] vsize: 2124
Raw data (/proc/28412/stat): 28412 (minisat+_64-bit) R 28408 28408 4419 0 -1 0 11465 0 0 0 31860 67 0 0 25 0 1 0 1856122137 50622464 10966 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28412/statm): 12359 10966 145 145 0 12214 0
[pid=28412] vsize: 49436
Current children cumulated CPU time (s) 319.28
Current children cumulated vsize (Kb) 51560

[startup+330.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28412
Raw data (/proc/28408/stat): 28408 (minisat+_script) S 28407 28408 4419 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856122132 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28408/statm): 531 226 485 147 0 384 0
[pid=28408] vsize: 2124
Raw data (/proc/28412/stat): 28412 (minisat+_64-bit) R 28408 28408 4419 0 -1 0 11539 0 0 0 32859 67 0 0 25 0 1 0 1856122137 50917376 11040 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28412/statm): 12431 11040 145 145 0 12286 0
[pid=28412] vsize: 49724
Current children cumulated CPU time (s) 329.27
Current children cumulated vsize (Kb) 51848

[startup+340.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28412
Raw data (/proc/28408/stat): 28408 (minisat+_script) S 28407 28408 4419 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856122132 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28408/statm): 531 226 485 147 0 384 0
[pid=28408] vsize: 2124
Raw data (/proc/28412/stat): 28412 (minisat+_64-bit) R 28408 28408 4419 0 -1 0 11638 0 0 0 33856 69 0 0 25 0 1 0 1856122137 51314688 11139 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28412/statm): 12528 11139 145 145 0 12383 0
[pid=28412] vsize: 50112
Current children cumulated CPU time (s) 339.26
Current children cumulated vsize (Kb) 52236

[startup+350.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28412
Raw data (/proc/28408/stat): 28408 (minisat+_script) S 28407 28408 4419 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856122132 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28408/statm): 531 226 485 147 0 384 0
[pid=28408] vsize: 2124
Raw data (/proc/28412/stat): 28412 (minisat+_64-bit) R 28408 28408 4419 0 -1 0 11739 0 0 0 34855 69 0 0 25 0 1 0 1856122137 51728384 11240 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28412/statm): 12629 11240 145 145 0 12484 0
[pid=28412] vsize: 50516
Current children cumulated CPU time (s) 349.25
Current children cumulated vsize (Kb) 52640

[startup+360.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28412
Raw data (/proc/28408/stat): 28408 (minisat+_script) S 28407 28408 4419 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856122132 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28408/statm): 531 226 485 147 0 384 0
[pid=28408] vsize: 2124
Raw data (/proc/28412/stat): 28412 (minisat+_64-bit) R 28408 28408 4419 0 -1 0 11870 0 0 0 35852 71 0 0 25 0 1 0 1856122137 52248576 11371 4294967295 134512640 135094434 3221224432 3221223088 134558016 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28412/statm): 12756 11371 145 145 0 12611 0
[pid=28412] vsize: 51024
Current children cumulated CPU time (s) 359.24
Current children cumulated vsize (Kb) 53148

[startup+370.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28412
Raw data (/proc/28408/stat): 28408 (minisat+_script) S 28407 28408 4419 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856122132 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28408/statm): 531 226 485 147 0 384 0
[pid=28408] vsize: 2124
Raw data (/proc/28412/stat): 28412 (minisat+_64-bit) R 28408 28408 4419 0 -1 0 11975 0 0 0 36850 72 0 0 25 0 1 0 1856122137 52670464 11476 4294967295 134512640 135094434 3221224432 3221223056 134557691 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28412/statm): 12859 11476 145 145 0 12714 0
[pid=28412] vsize: 51436
Current children cumulated CPU time (s) 369.23
Current children cumulated vsize (Kb) 53560

[startup+380.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28412
Raw data (/proc/28408/stat): 28408 (minisat+_script) S 28407 28408 4419 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856122132 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28408/statm): 531 226 485 147 0 384 0
[pid=28408] vsize: 2124
Raw data (/proc/28412/stat): 28412 (minisat+_64-bit) R 28408 28408 4419 0 -1 0 12080 0 0 0 37848 73 0 0 25 0 1 0 1856122137 53092352 11581 4294967295 134512640 135094434 3221224432 3221223024 134557230 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28412/statm): 12962 11581 145 145 0 12817 0
[pid=28412] vsize: 51848
Current children cumulated CPU time (s) 379.22
Current children cumulated vsize (Kb) 53972

[startup+390.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28412
Raw data (/proc/28408/stat): 28408 (minisat+_script) S 28407 28408 4419 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856122132 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28408/statm): 531 226 485 147 0 384 0
[pid=28408] vsize: 2124
Raw data (/proc/28412/stat): 28412 (minisat+_64-bit) R 28408 28408 4419 0 -1 0 12202 0 0 0 38846 73 0 0 25 0 1 0 1856122137 53583872 11703 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28412/statm): 13082 11703 145 145 0 12937 0
[pid=28412] vsize: 52328
Current children cumulated CPU time (s) 389.2
Current children cumulated vsize (Kb) 54452

[startup+400.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28412
Raw data (/proc/28408/stat): 28408 (minisat+_script) S 28407 28408 4419 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856122132 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28408/statm): 531 226 485 147 0 384 0
[pid=28408] vsize: 2124
Raw data (/proc/28412/stat): 28412 (minisat+_64-bit) R 28408 28408 4419 0 -1 0 12276 0 0 0 39845 73 0 0 25 0 1 0 1856122137 53886976 11777 4294967295 134512640 135094434 3221224432 3221223056 134562131 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28412/statm): 13156 11777 145 145 0 13011 0
[pid=28412] vsize: 52624
Current children cumulated CPU time (s) 399.19
Current children cumulated vsize (Kb) 54748

[startup+410.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28412
Raw data (/proc/28408/stat): 28408 (minisat+_script) S 28407 28408 4419 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856122132 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28408/statm): 531 226 485 147 0 384 0
[pid=28408] vsize: 2124
Raw data (/proc/28412/stat): 28412 (minisat+_64-bit) R 28408 28408 4419 0 -1 0 12360 0 0 0 40844 74 0 0 25 0 1 0 1856122137 54218752 11861 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28412/statm): 13237 11861 145 145 0 13092 0
[pid=28412] vsize: 52948
Current children cumulated CPU time (s) 409.19
Current children cumulated vsize (Kb) 55072

[startup+420.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28412
Raw data (/proc/28408/stat): 28408 (minisat+_script) S 28407 28408 4419 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856122132 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28408/statm): 531 226 485 147 0 384 0
[pid=28408] vsize: 2124
Raw data (/proc/28412/stat): 28412 (minisat+_64-bit) R 28408 28408 4419 0 -1 0 12429 0 0 0 41844 75 0 0 25 0 1 0 1856122137 54497280 11930 4294967295 134512640 135094434 3221224432 3221223088 134558402 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28412/statm): 13305 11930 145 145 0 13160 0
[pid=28412] vsize: 53220
Current children cumulated CPU time (s) 419.2
Current children cumulated vsize (Kb) 55344

[startup+430.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28412
Raw data (/proc/28408/stat): 28408 (minisat+_script) S 28407 28408 4419 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856122132 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28408/statm): 531 226 485 147 0 384 0
[pid=28408] vsize: 2124
Raw data (/proc/28412/stat): 28412 (minisat+_64-bit) R 28408 28408 4419 0 -1 0 12519 0 0 0 42843 75 0 0 25 0 1 0 1856122137 54853632 12020 4294967295 134512640 135094434 3221224432 3221223044 134563083 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28412/statm): 13392 12020 145 145 0 13247 0
[pid=28412] vsize: 53568
Current children cumulated CPU time (s) 429.19
Current children cumulated vsize (Kb) 55692

[startup+440.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28412
Raw data (/proc/28408/stat): 28408 (minisat+_script) S 28407 28408 4419 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856122132 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28408/statm): 531 226 485 147 0 384 0
[pid=28408] vsize: 2124
Raw data (/proc/28412/stat): 28412 (minisat+_64-bit) R 28408 28408 4419 0 -1 0 12601 0 0 0 43840 76 0 0 25 0 1 0 1856122137 55189504 12102 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28412/statm): 13474 12102 145 145 0 13329 0
[pid=28412] vsize: 53896
Current children cumulated CPU time (s) 439.17
Current children cumulated vsize (Kb) 56020

[startup+450.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28412
Raw data (/proc/28408/stat): 28408 (minisat+_script) S 28407 28408 4419 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856122132 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28408/statm): 531 226 485 147 0 384 0
[pid=28408] vsize: 2124
Raw data (/proc/28412/stat): 28412 (minisat+_64-bit) R 28408 28408 4419 0 -1 0 12704 0 0 0 44839 77 0 0 25 0 1 0 1856122137 55599104 12205 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28412/statm): 13574 12205 145 145 0 13429 0
[pid=28412] vsize: 54296
Current children cumulated CPU time (s) 449.17
Current children cumulated vsize (Kb) 56420

[startup+460.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28412
Raw data (/proc/28408/stat): 28408 (minisat+_script) S 28407 28408 4419 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856122132 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28408/statm): 531 226 485 147 0 384 0
[pid=28408] vsize: 2124
Raw data (/proc/28412/stat): 28412 (minisat+_64-bit) R 28408 28408 4419 0 -1 0 12771 0 0 0 45837 77 0 0 25 0 1 0 1856122137 55861248 12272 4294967295 134512640 135094434 3221224432 3221223104 134556426 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28412/statm): 13638 12272 145 145 0 13493 0
[pid=28412] vsize: 54552
Current children cumulated CPU time (s) 459.15
Current children cumulated vsize (Kb) 56676

[startup+470.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28412
Raw data (/proc/28408/stat): 28408 (minisat+_script) S 28407 28408 4419 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856122132 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28408/statm): 531 226 485 147 0 384 0
[pid=28408] vsize: 2124
Raw data (/proc/28412/stat): 28412 (minisat+_64-bit) R 28408 28408 4419 0 -1 0 12917 0 0 0 46835 78 0 0 25 0 1 0 1856122137 56446976 12418 4294967295 134512640 135094434 3221224432 3221223056 134557696 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28412/statm): 13781 12418 145 145 0 13636 0
[pid=28412] vsize: 55124
Current children cumulated CPU time (s) 469.14
Current children cumulated vsize (Kb) 57248

[startup+480.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28412
Raw data (/proc/28408/stat): 28408 (minisat+_script) S 28407 28408 4419 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856122132 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28408/statm): 531 226 485 147 0 384 0
[pid=28408] vsize: 2124
Raw data (/proc/28412/stat): 28412 (minisat+_64-bit) R 28408 28408 4419 0 -1 0 13040 0 0 0 47833 79 0 0 25 0 1 0 1856122137 56958976 12541 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28412/statm): 13906 12541 145 145 0 13761 0
[pid=28412] vsize: 55624
Current children cumulated CPU time (s) 479.13
Current children cumulated vsize (Kb) 57748

[startup+490.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28412
Raw data (/proc/28408/stat): 28408 (minisat+_script) S 28407 28408 4419 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856122132 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28408/statm): 531 226 485 147 0 384 0
[pid=28408] vsize: 2124
Raw data (/proc/28412/stat): 28412 (minisat+_64-bit) R 28408 28408 4419 0 -1 0 13240 0 0 0 48829 81 0 0 25 0 1 0 1856122137 57757696 12741 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28412/statm): 14101 12741 145 145 0 13956 0
[pid=28412] vsize: 56404
Current children cumulated CPU time (s) 489.11
Current children cumulated vsize (Kb) 58528

[startup+500.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28412
Raw data (/proc/28408/stat): 28408 (minisat+_script) S 28407 28408 4419 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856122132 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28408/statm): 531 226 485 147 0 384 0
[pid=28408] vsize: 2124
Raw data (/proc/28412/stat): 28412 (minisat+_64-bit) R 28408 28408 4419 0 -1 0 13336 0 0 0 49828 81 0 0 25 0 1 0 1856122137 58150912 12837 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28412/statm): 14197 12837 145 145 0 14052 0
[pid=28412] vsize: 56788
Current children cumulated CPU time (s) 499.1
Current children cumulated vsize (Kb) 58912

[startup+510.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28412
Raw data (/proc/28408/stat): 28408 (minisat+_script) S 28407 28408 4419 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856122132 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28408/statm): 531 226 485 147 0 384 0
[pid=28408] vsize: 2124
Raw data (/proc/28412/stat): 28412 (minisat+_64-bit) R 28408 28408 4419 0 -1 0 13424 0 0 0 50826 82 0 0 25 0 1 0 1856122137 58494976 12925 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28412/statm): 14281 12925 145 145 0 14136 0
[pid=28412] vsize: 57124
Current children cumulated CPU time (s) 509.09
Current children cumulated vsize (Kb) 59248

[startup+520.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28412
Raw data (/proc/28408/stat): 28408 (minisat+_script) S 28407 28408 4419 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856122132 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28408/statm): 531 226 485 147 0 384 0
[pid=28408] vsize: 2124
Raw data (/proc/28412/stat): 28412 (minisat+_64-bit) R 28408 28408 4419 0 -1 0 13526 0 0 0 51824 83 0 0 25 0 1 0 1856122137 58904576 13027 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28412/statm): 14381 13027 145 145 0 14236 0
[pid=28412] vsize: 57524
Current children cumulated CPU time (s) 519.08
Current children cumulated vsize (Kb) 59648

[startup+530.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28412
Raw data (/proc/28408/stat): 28408 (minisat+_script) S 28407 28408 4419 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856122132 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28408/statm): 531 226 485 147 0 384 0
[pid=28408] vsize: 2124
Raw data (/proc/28412/stat): 28412 (minisat+_64-bit) R 28408 28408 4419 0 -1 0 13612 0 0 0 52823 83 0 0 25 0 1 0 1856122137 59248640 13113 4294967295 134512640 135094434 3221224432 3221223092 134553536 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28412/statm): 14465 13113 145 145 0 14320 0
[pid=28412] vsize: 57860
Current children cumulated CPU time (s) 529.07
Current children cumulated vsize (Kb) 59984

[startup+540.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28412
Raw data (/proc/28408/stat): 28408 (minisat+_script) S 28407 28408 4419 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856122132 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28408/statm): 531 226 485 147 0 384 0
[pid=28408] vsize: 2124
Raw data (/proc/28412/stat): 28412 (minisat+_64-bit) R 28408 28408 4419 0 -1 0 13697 0 0 0 53822 84 0 0 25 0 1 0 1856122137 59596800 13198 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28412/statm): 14550 13198 145 145 0 14405 0
[pid=28412] vsize: 58200
Current children cumulated CPU time (s) 539.07
Current children cumulated vsize (Kb) 60324

[startup+550.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28412
Raw data (/proc/28408/stat): 28408 (minisat+_script) S 28407 28408 4419 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856122132 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28408/statm): 531 226 485 147 0 384 0
[pid=28408] vsize: 2124
Raw data (/proc/28412/stat): 28412 (minisat+_64-bit) R 28408 28408 4419 0 -1 0 13766 0 0 0 54821 84 0 0 25 0 1 0 1856122137 59875328 13267 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28412/statm): 14618 13267 145 145 0 14473 0
[pid=28412] vsize: 58472
Current children cumulated CPU time (s) 549.06
Current children cumulated vsize (Kb) 60596

[startup+560.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28412
Raw data (/proc/28408/stat): 28408 (minisat+_script) S 28407 28408 4419 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856122132 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28408/statm): 531 226 485 147 0 384 0
[pid=28408] vsize: 2124
Raw data (/proc/28412/stat): 28412 (minisat+_64-bit) R 28408 28408 4419 0 -1 0 13851 0 0 0 55820 85 0 0 25 0 1 0 1856122137 60219392 13352 4294967295 134512640 135094434 3221224432 3221223024 134557421 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28412/statm): 14702 13352 145 145 0 14557 0
[pid=28412] vsize: 58808
Current children cumulated CPU time (s) 559.06
Current children cumulated vsize (Kb) 60932

[startup+570.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28412
Raw data (/proc/28408/stat): 28408 (minisat+_script) S 28407 28408 4419 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856122132 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28408/statm): 531 226 485 147 0 384 0
[pid=28408] vsize: 2124
Raw data (/proc/28412/stat): 28412 (minisat+_64-bit) R 28408 28408 4419 0 -1 0 13955 0 0 0 56818 86 0 0 25 0 1 0 1856122137 60641280 13456 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28412/statm): 14805 13456 145 145 0 14660 0
[pid=28412] vsize: 59220
Current children cumulated CPU time (s) 569.05
Current children cumulated vsize (Kb) 61344

[startup+580.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28412
Raw data (/proc/28408/stat): 28408 (minisat+_script) S 28407 28408 4419 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856122132 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28408/statm): 531 226 485 147 0 384 0
[pid=28408] vsize: 2124
Raw data (/proc/28412/stat): 28412 (minisat+_64-bit) R 28408 28408 4419 0 -1 0 14053 0 0 0 57816 87 0 0 25 0 1 0 1856122137 61034496 13554 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28412/statm): 14901 13554 145 145 0 14756 0
[pid=28412] vsize: 59604
Current children cumulated CPU time (s) 579.04
Current children cumulated vsize (Kb) 61728

[startup+590.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28412
Raw data (/proc/28408/stat): 28408 (minisat+_script) S 28407 28408 4419 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856122132 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28408/statm): 531 226 485 147 0 384 0
[pid=28408] vsize: 2124
Raw data (/proc/28412/stat): 28412 (minisat+_64-bit) R 28408 28408 4419 0 -1 0 14123 0 0 0 58815 87 0 0 25 0 1 0 1856122137 61837312 13624 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28412/statm): 15097 13624 145 145 0 14952 0
[pid=28412] vsize: 60388
Current children cumulated CPU time (s) 589.03
Current children cumulated vsize (Kb) 62512

[startup+600.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28412
Raw data (/proc/28408/stat): 28408 (minisat+_script) S 28407 28408 4419 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856122132 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28408/statm): 531 226 485 147 0 384 0
[pid=28408] vsize: 2124
Raw data (/proc/28412/stat): 28412 (minisat+_64-bit) R 28408 28408 4419 0 -1 0 14216 0 0 0 59814 88 0 0 25 0 1 0 1856122137 62210048 13717 4294967295 134512640 135094434 3221224432 3221223024 134557429 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28412/statm): 15188 13717 145 145 0 15043 0
[pid=28412] vsize: 60752
Current children cumulated CPU time (s) 599.03
Current children cumulated vsize (Kb) 62876

[startup+610.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28412
Raw data (/proc/28408/stat): 28408 (minisat+_script) S 28407 28408 4419 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856122132 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28408/statm): 531 226 485 147 0 384 0
[pid=28408] vsize: 2124
Raw data (/proc/28412/stat): 28412 (minisat+_64-bit) R 28408 28408 4419 0 -1 0 14283 0 0 0 60813 88 0 0 25 0 1 0 1856122137 62484480 13784 4294967295 134512640 135094434 3221224432 3221223056 134557630 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28412/statm): 15255 13784 145 145 0 15110 0
[pid=28412] vsize: 61020
Current children cumulated CPU time (s) 609.02
Current children cumulated vsize (Kb) 63144

[startup+620.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28412
Raw data (/proc/28408/stat): 28408 (minisat+_script) S 28407 28408 4419 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856122132 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28408/statm): 531 226 485 147 0 384 0
[pid=28408] vsize: 2124
Raw data (/proc/28412/stat): 28412 (minisat+_64-bit) R 28408 28408 4419 0 -1 0 14378 0 0 0 61811 89 0 0 25 0 1 0 1856122137 62869504 13879 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28412/statm): 15349 13879 145 145 0 15204 0
[pid=28412] vsize: 61396
Current children cumulated CPU time (s) 619.01
Current children cumulated vsize (Kb) 63520

[startup+630.051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28412
Raw data (/proc/28408/stat): 28408 (minisat+_script) S 28407 28408 4419 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856122132 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28408/statm): 531 226 485 147 0 384 0
[pid=28408] vsize: 2124
Raw data (/proc/28412/stat): 28412 (minisat+_64-bit) R 28408 28408 4419 0 -1 0 14464 0 0 0 62809 90 0 0 25 0 1 0 1856122137 63217664 13965 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28412/statm): 15434 13965 145 145 0 15289 0
[pid=28412] vsize: 61736
Current children cumulated CPU time (s) 629
Current children cumulated vsize (Kb) 63860

[startup+640.051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28412
Raw data (/proc/28408/stat): 28408 (minisat+_script) S 28407 28408 4419 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856122132 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28408/statm): 531 226 485 147 0 384 0
[pid=28408] vsize: 2124
Raw data (/proc/28412/stat): 28412 (minisat+_64-bit) R 28408 28408 4419 0 -1 0 14557 0 0 0 63807 91 0 0 25 0 1 0 1856122137 63586304 14058 4294967295 134512640 135094434 3221224432 3221223088 134558178 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28412/statm): 15524 14058 145 145 0 15379 0
[pid=28412] vsize: 62096
Current children cumulated CPU time (s) 638.99
Current children cumulated vsize (Kb) 64220

[startup+650.052 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28412
Raw data (/proc/28408/stat): 28408 (minisat+_script) S 28407 28408 4419 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856122132 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28408/statm): 531 226 485 147 0 384 0
[pid=28408] vsize: 2124
Raw data (/proc/28412/stat): 28412 (minisat+_64-bit) R 28408 28408 4419 0 -1 0 14686 0 0 0 64805 91 0 0 25 0 1 0 1856122137 64110592 14187 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28412/statm): 15652 14187 145 145 0 15507 0
[pid=28412] vsize: 62608
Current children cumulated CPU time (s) 648.97
Current children cumulated vsize (Kb) 64732

[startup+660.052 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28412
Raw data (/proc/28408/stat): 28408 (minisat+_script) S 28407 28408 4419 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856122132 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28408/statm): 531 226 485 147 0 384 0
[pid=28408] vsize: 2124
Raw data (/proc/28412/stat): 28412 (minisat+_64-bit) R 28408 28408 4419 0 -1 0 14773 0 0 0 65803 92 0 0 25 0 1 0 1856122137 64450560 14274 4294967295 134512640 135094434 3221224432 3221223056 134557565 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28412/statm): 15735 14274 145 145 0 15590 0
[pid=28412] vsize: 62940
Current children cumulated CPU time (s) 658.96
Current children cumulated vsize (Kb) 65064

[startup+670.053 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28412
Raw data (/proc/28408/stat): 28408 (minisat+_script) S 28407 28408 4419 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856122132 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28408/statm): 531 226 485 147 0 384 0
[pid=28408] vsize: 2124
Raw data (/proc/28412/stat): 28412 (minisat+_64-bit) R 28408 28408 4419 0 -1 0 14902 0 0 0 66802 93 0 0 25 0 1 0 1856122137 65003520 14403 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28412/statm): 15870 14403 145 145 0 15725 0
[pid=28412] vsize: 63480
Current children cumulated CPU time (s) 668.96
Current children cumulated vsize (Kb) 65604

[startup+680.053 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28412
Raw data (/proc/28408/stat): 28408 (minisat+_script) S 28407 28408 4419 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856122132 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28408/statm): 531 226 485 147 0 384 0
[pid=28408] vsize: 2124
Raw data (/proc/28412/stat): 28412 (minisat+_64-bit) R 28408 28408 4419 0 -1 0 14985 0 0 0 67800 94 0 0 25 0 1 0 1856122137 65339392 14486 4294967295 134512640 135094434 3221224432 3221223024 134557273 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28412/statm): 15952 14486 145 145 0 15807 0
[pid=28412] vsize: 63808
Current children cumulated CPU time (s) 678.95
Current children cumulated vsize (Kb) 65932

[startup+690.054 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28412
Raw data (/proc/28408/stat): 28408 (minisat+_script) S 28407 28408 4419 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856122132 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28408/statm): 531 226 485 147 0 384 0
[pid=28408] vsize: 2124
Raw data (/proc/28412/stat): 28412 (minisat+_64-bit) R 28408 28408 4419 0 -1 0 15061 0 0 0 68800 95 0 0 25 0 1 0 1856122137 65650688 14562 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28412/statm): 16028 14562 145 145 0 15883 0
[pid=28412] vsize: 64112
Current children cumulated CPU time (s) 688.96
Current children cumulated vsize (Kb) 66236

[startup+700.055 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28412
Raw data (/proc/28408/stat): 28408 (minisat+_script) S 28407 28408 4419 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856122132 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28408/statm): 531 226 485 147 0 384 0
[pid=28408] vsize: 2124
Raw data (/proc/28412/stat): 28412 (minisat+_64-bit) R 28408 28408 4419 0 -1 0 15175 0 0 0 69797 95 0 0 25 0 1 0 1856122137 66113536 14676 4294967295 134512640 135094434 3221224432 3221223024 134556862 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28412/statm): 16141 14676 145 145 0 15996 0
[pid=28412] vsize: 64564
Current children cumulated CPU time (s) 698.93
Current children cumulated vsize (Kb) 66688

[startup+710.054 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28412
Raw data (/proc/28408/stat): 28408 (minisat+_script) S 28407 28408 4419 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856122132 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28408/statm): 531 226 485 147 0 384 0
[pid=28408] vsize: 2124
Raw data (/proc/28412/stat): 28412 (minisat+_64-bit) R 28408 28408 4419 0 -1 0 15264 0 0 0 70796 96 0 0 25 0 1 0 1856122137 66473984 14765 4294967295 134512640 135094434 3221224432 3221223088 134558026 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28412/statm): 16229 14765 145 145 0 16084 0
[pid=28412] vsize: 64916
Current children cumulated CPU time (s) 708.93
Current children cumulated vsize (Kb) 67040

[startup+720.055 s]
Raw data (loadavg): 0.99 0.97 0.91 1/57 28412
Raw data (/proc/28408/stat): 28408 (minisat+_script) S 28407 28408 4419 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856122132 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28408/statm): 531 226 485 147 0 384 0
[pid=28408] vsize: 2124
Raw data (/proc/28412/stat): 28412 (minisat+_64-bit) T 28408 28408 4419 0 -1 0 15356 0 0 0 71794 97 0 0 25 0 1 0 1856122137 66838528 14857 4294967295 134512640 135094434 3221224432 3221222796 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/28412/statm): 16318 14857 145 145 0 16173 0
[pid=28412] vsize: 65272
Current children cumulated CPU time (s) 718.92
Current children cumulated vsize (Kb) 67396

[startup+730.056 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28412
Raw data (/proc/28408/stat): 28408 (minisat+_script) S 28407 28408 4419 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856122132 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28408/statm): 531 226 485 147 0 384 0
[pid=28408] vsize: 2124
Raw data (/proc/28412/stat): 28412 (minisat+_64-bit) R 28408 28408 4419 0 -1 0 15503 0 0 0 72791 98 0 0 25 0 1 0 1856122137 67432448 15004 4294967295 134512640 135094434 3221224432 3221223120 134554705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28412/statm): 16463 15004 145 145 0 16318 0
[pid=28412] vsize: 65852
Current children cumulated CPU time (s) 728.9
Current children cumulated vsize (Kb) 67976

[startup+740.056 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28412
Raw data (/proc/28408/stat): 28408 (minisat+_script) S 28407 28408 4419 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856122132 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28408/statm): 531 226 485 147 0 384 0
[pid=28408] vsize: 2124
Raw data (/proc/28412/stat): 28412 (minisat+_64-bit) R 28408 28408 4419 0 -1 0 15638 0 0 0 73788 99 0 0 25 0 1 0 1856122137 67981312 15139 4294967295 134512640 135094434 3221224432 3221223088 134557903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28412/statm): 16597 15139 145 145 0 16452 0
[pid=28412] vsize: 66388
Current children cumulated CPU time (s) 738.88
Current children cumulated vsize (Kb) 68512

[startup+750.057 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28412
Raw data (/proc/28408/stat): 28408 (minisat+_script) S 28407 28408 4419 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856122132 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28408/statm): 531 226 485 147 0 384 0
[pid=28408] vsize: 2124
Raw data (/proc/28412/stat): 28412 (minisat+_64-bit) R 28408 28408 4419 0 -1 0 15835 0 0 0 74784 101 0 0 25 0 1 0 1856122137 68784128 15336 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28412/statm): 16793 15336 145 145 0 16648 0
[pid=28412] vsize: 67172
Current children cumulated CPU time (s) 748.86
Current children cumulated vsize (Kb) 69296

[startup+760.057 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28412
Raw data (/proc/28408/stat): 28408 (minisat+_script) S 28407 28408 4419 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856122132 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28408/statm): 531 226 485 147 0 384 0
[pid=28408] vsize: 2124
Raw data (/proc/28412/stat): 28412 (minisat+_64-bit) R 28408 28408 4419 0 -1 0 15960 0 0 0 75781 102 0 0 25 0 1 0 1856122137 69279744 15461 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28412/statm): 16914 15461 145 145 0 16769 0
[pid=28412] vsize: 67656
Current children cumulated CPU time (s) 758.84
Current children cumulated vsize (Kb) 69780

[startup+770.058 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28412
Raw data (/proc/28408/stat): 28408 (minisat+_script) S 28407 28408 4419 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856122132 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28408/statm): 531 226 485 147 0 384 0
[pid=28408] vsize: 2124
Raw data (/proc/28412/stat): 28412 (minisat+_64-bit) R 28408 28408 4419 0 -1 0 16131 0 0 0 76778 103 0 0 25 0 1 0 1856122137 70008832 15632 4294967295 134512640 135094434 3221224432 3221223024 134557219 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28412/statm): 17092 15632 145 145 0 16947 0
[pid=28412] vsize: 68368
Current children cumulated CPU time (s) 768.82
Current children cumulated vsize (Kb) 70492

[startup+780.058 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28412
Raw data (/proc/28408/stat): 28408 (minisat+_script) S 28407 28408 4419 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856122132 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28408/statm): 531 226 485 147 0 384 0
[pid=28408] vsize: 2124
Raw data (/proc/28412/stat): 28412 (minisat+_64-bit) R 28408 28408 4419 0 -1 0 16217 0 0 0 77777 104 0 0 25 0 1 0 1856122137 70361088 15718 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28412/statm): 17178 15718 145 145 0 17033 0
[pid=28412] vsize: 68712
Current children cumulated CPU time (s) 778.82
Current children cumulated vsize (Kb) 70836

[startup+790.059 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28412
Raw data (/proc/28408/stat): 28408 (minisat+_script) S 28407 28408 4419 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856122132 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28408/statm): 531 226 485 147 0 384 0
[pid=28408] vsize: 2124
Raw data (/proc/28412/stat): 28412 (minisat+_64-bit) R 28408 28408 4419 0 -1 0 16327 0 0 0 78776 104 0 0 25 0 1 0 1856122137 70815744 15828 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28412/statm): 17289 15828 145 145 0 17144 0
[pid=28412] vsize: 69156
Current children cumulated CPU time (s) 788.81
Current children cumulated vsize (Kb) 71280

[startup+800.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28412
Raw data (/proc/28408/stat): 28408 (minisat+_script) S 28407 28408 4419 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856122132 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28408/statm): 531 226 485 147 0 384 0
[pid=28408] vsize: 2124
Raw data (/proc/28412/stat): 28412 (minisat+_64-bit) R 28408 28408 4419 0 -1 0 16432 0 0 0 79774 105 0 0 25 0 1 0 1856122137 71237632 15933 4294967295 134512640 135094434 3221224432 3221223088 134558235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28412/statm): 17392 15933 145 145 0 17247 0
[pid=28412] vsize: 69568
Current children cumulated CPU time (s) 798.8
Current children cumulated vsize (Kb) 71692

[startup+810.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28412
Raw data (/proc/28408/stat): 28408 (minisat+_script) S 28407 28408 4419 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856122132 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28408/statm): 531 226 485 147 0 384 0
[pid=28408] vsize: 2124
Raw data (/proc/28412/stat): 28412 (minisat+_64-bit) R 28408 28408 4419 0 -1 0 16505 0 0 0 80774 105 0 0 25 0 1 0 1856122137 71532544 16006 4294967295 134512640 135094434 3221224432 3221223088 134557964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28412/statm): 17464 16006 145 145 0 17319 0
[pid=28412] vsize: 69856
Current children cumulated CPU time (s) 808.8
Current children cumulated vsize (Kb) 71980

[startup+820.061 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28412
Raw data (/proc/28408/stat): 28408 (minisat+_script) S 28407 28408 4419 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856122132 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28408/statm): 531 226 485 147 0 384 0
[pid=28408] vsize: 2124
Raw data (/proc/28412/stat): 28412 (minisat+_64-bit) R 28408 28408 4419 0 -1 0 16573 0 0 0 81772 106 0 0 25 0 1 0 1856122137 71819264 16074 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28412/statm): 17534 16074 145 145 0 17389 0
[pid=28412] vsize: 70136
Current children cumulated CPU time (s) 818.79
Current children cumulated vsize (Kb) 72260

[startup+830.062 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28412
Raw data (/proc/28408/stat): 28408 (minisat+_script) S 28407 28408 4419 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856122132 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28408/statm): 531 226 485 147 0 384 0
[pid=28408] vsize: 2124
Raw data (/proc/28412/stat): 28412 (minisat+_64-bit) R 28408 28408 4419 0 -1 0 16630 0 0 0 82771 107 0 0 25 0 1 0 1856122137 72048640 16131 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28412/statm): 17590 16131 145 145 0 17445 0
[pid=28412] vsize: 70360
Current children cumulated CPU time (s) 828.79
Current children cumulated vsize (Kb) 72484

[startup+840.062 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28412
Raw data (/proc/28408/stat): 28408 (minisat+_script) S 28407 28408 4419 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856122132 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28408/statm): 531 226 485 147 0 384 0
[pid=28408] vsize: 2124
Raw data (/proc/28412/stat): 28412 (minisat+_64-bit) R 28408 28408 4419 0 -1 0 16699 0 0 0 83770 108 0 0 25 0 1 0 1856122137 72331264 16200 4294967295 134512640 135094434 3221224432 3221223088 134558426 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28412/statm): 17659 16200 145 145 0 17514 0
[pid=28412] vsize: 70636
Current children cumulated CPU time (s) 838.79
Current children cumulated vsize (Kb) 72760

[startup+850.063 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28412
Raw data (/proc/28408/stat): 28408 (minisat+_script) S 28407 28408 4419 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856122132 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28408/statm): 531 226 485 147 0 384 0
[pid=28408] vsize: 2124
Raw data (/proc/28412/stat): 28412 (minisat+_64-bit) R 28408 28408 4419 0 -1 0 16753 0 0 0 84769 108 0 0 25 0 1 0 1856122137 72544256 16254 4294967295 134512640 135094434 3221224432 3221223088 134557882 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28412/statm): 17711 16254 145 145 0 17566 0
[pid=28412] vsize: 70844
Current children cumulated CPU time (s) 848.78
Current children cumulated vsize (Kb) 72968

[startup+860.062 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28412
Raw data (/proc/28408/stat): 28408 (minisat+_script) S 28407 28408 4419 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856122132 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28408/statm): 531 226 485 147 0 384 0
[pid=28408] vsize: 2124
Raw data (/proc/28412/stat): 28412 (minisat+_64-bit) R 28408 28408 4419 0 -1 0 16810 0 0 0 85769 108 0 0 25 0 1 0 1856122137 72777728 16311 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28412/statm): 17768 16311 145 145 0 17623 0
[pid=28412] vsize: 71072
Current children cumulated CPU time (s) 858.78
Current children cumulated vsize (Kb) 73196

[startup+870.063 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28412
Raw data (/proc/28408/stat): 28408 (minisat+_script) S 28407 28408 4419 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856122132 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28408/statm): 531 226 485 147 0 384 0
[pid=28408] vsize: 2124
Raw data (/proc/28412/stat): 28412 (minisat+_64-bit) R 28408 28408 4419 0 -1 0 16862 0 0 0 86768 109 0 0 25 0 1 0 1856122137 72990720 16363 4294967295 134512640 135094434 3221224432 3221223088 134557884 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28412/statm): 17820 16363 145 145 0 17675 0
[pid=28412] vsize: 71280
Current children cumulated CPU time (s) 868.78
Current children cumulated vsize (Kb) 73404

[startup+880.066 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28412
Raw data (/proc/28408/stat): 28408 (minisat+_script) S 28407 28408 4419 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856122132 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28408/statm): 531 226 485 147 0 384 0
[pid=28408] vsize: 2124
Raw data (/proc/28412/stat): 28412 (minisat+_64-bit) R 28408 28408 4419 0 -1 0 16928 0 0 0 87767 109 0 0 25 0 1 0 1856122137 73256960 16429 4294967295 134512640 135094434 3221224432 3221223088 134558035 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28412/statm): 17885 16429 145 145 0 17740 0
[pid=28412] vsize: 71540
Current children cumulated CPU time (s) 878.77
Current children cumulated vsize (Kb) 73664

[startup+890.066 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28412
Raw data (/proc/28408/stat): 28408 (minisat+_script) S 28407 28408 4419 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856122132 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28408/statm): 531 226 485 147 0 384 0
[pid=28408] vsize: 2124
Raw data (/proc/28412/stat): 28412 (minisat+_64-bit) R 28408 28408 4419 0 -1 0 17031 0 0 0 88765 110 0 0 25 0 1 0 1856122137 73666560 16532 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28412/statm): 17985 16532 145 145 0 17840 0
[pid=28412] vsize: 71940
Current children cumulated CPU time (s) 888.76
Current children cumulated vsize (Kb) 74064

[startup+900.067 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28412
Raw data (/proc/28408/stat): 28408 (minisat+_script) S 28407 28408 4419 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856122132 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28408/statm): 531 226 485 147 0 384 0
[pid=28408] vsize: 2124
Raw data (/proc/28412/stat): 28412 (minisat+_64-bit) R 28408 28408 4419 0 -1 0 17127 0 0 0 89764 110 0 0 25 0 1 0 1856122137 74055680 16628 4294967295 134512640 135094434 3221224432 3221223056 134557650 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28412/statm): 18080 16628 145 145 0 17935 0
[pid=28412] vsize: 72320
Current children cumulated CPU time (s) 898.75
Current children cumulated vsize (Kb) 74444

[startup+910.067 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28412
Raw data (/proc/28408/stat): 28408 (minisat+_script) S 28407 28408 4419 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856122132 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28408/statm): 531 226 485 147 0 384 0
[pid=28408] vsize: 2124
Raw data (/proc/28412/stat): 28412 (minisat+_64-bit) R 28408 28408 4419 0 -1 0 17238 0 0 0 90762 111 0 0 25 0 1 0 1856122137 74506240 16739 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28412/statm): 18190 16739 145 145 0 18045 0
[pid=28412] vsize: 72760
Current children cumulated CPU time (s) 908.74
Current children cumulated vsize (Kb) 74884

[startup+920.068 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28412
Raw data (/proc/28408/stat): 28408 (minisat+_script) S 28407 28408 4419 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856122132 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28408/statm): 531 226 485 147 0 384 0
[pid=28408] vsize: 2124
Raw data (/proc/28412/stat): 28412 (minisat+_64-bit) R 28408 28408 4419 0 -1 0 17349 0 0 0 91759 113 0 0 25 0 1 0 1856122137 74952704 16850 4294967295 134512640 135094434 3221224432 3221223088 134557950 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28412/statm): 18299 16850 145 145 0 18154 0
[pid=28412] vsize: 73196
Current children cumulated CPU time (s) 918.73
Current children cumulated vsize (Kb) 75320

[startup+930.069 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28412
Raw data (/proc/28408/stat): 28408 (minisat+_script) S 28407 28408 4419 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856122132 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28408/statm): 531 226 485 147 0 384 0
[pid=28408] vsize: 2124
Raw data (/proc/28412/stat): 28412 (minisat+_64-bit) R 28408 28408 4419 0 -1 0 17431 0 0 0 92758 113 0 0 25 0 1 0 1856122137 75288576 16932 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28412/statm): 18381 16932 145 145 0 18236 0
[pid=28412] vsize: 73524
Current children cumulated CPU time (s) 928.72
Current children cumulated vsize (Kb) 75648

[startup+940.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28412
Raw data (/proc/28408/stat): 28408 (minisat+_script) S 28407 28408 4419 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856122132 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28408/statm): 531 226 485 147 0 384 0
[pid=28408] vsize: 2124
Raw data (/proc/28412/stat): 28412 (minisat+_64-bit) R 28408 28408 4419 0 -1 0 17572 0 0 0 93756 114 0 0 25 0 1 0 1856122137 75857920 17073 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28412/statm): 18520 17073 145 145 0 18375 0
[pid=28412] vsize: 74080
Current children cumulated CPU time (s) 938.71
Current children cumulated vsize (Kb) 76204

[startup+950.071 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28412
Raw data (/proc/28408/stat): 28408 (minisat+_script) S 28407 28408 4419 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856122132 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28408/statm): 531 226 485 147 0 384 0
[pid=28408] vsize: 2124
Raw data (/proc/28412/stat): 28412 (minisat+_64-bit) R 28408 28408 4419 0 -1 0 17857 0 0 0 94751 117 0 0 25 0 1 0 1856122137 77012992 17358 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28412/statm): 18802 17358 145 145 0 18657 0
[pid=28412] vsize: 75208
Current children cumulated CPU time (s) 948.69
Current children cumulated vsize (Kb) 77332

[startup+960.071 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28412
Raw data (/proc/28408/stat): 28408 (minisat+_script) S 28407 28408 4419 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856122132 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28408/statm): 531 226 485 147 0 384 0
[pid=28408] vsize: 2124
Raw data (/proc/28412/stat): 28412 (minisat+_64-bit) R 28408 28408 4419 0 -1 0 17970 0 0 0 95748 118 0 0 25 0 1 0 1856122137 77471744 17471 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28412/statm): 18914 17471 145 145 0 18769 0
[pid=28412] vsize: 75656
Current children cumulated CPU time (s) 958.67
Current children cumulated vsize (Kb) 77780

[startup+970.071 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28412
Raw data (/proc/28408/stat): 28408 (minisat+_script) S 28407 28408 4419 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856122132 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28408/statm): 531 226 485 147 0 384 0
[pid=28408] vsize: 2124
Raw data (/proc/28412/stat): 28412 (minisat+_64-bit) R 28408 28408 4419 0 -1 0 18026 0 0 0 96746 119 0 0 25 0 1 0 1856122137 77697024 17527 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28412/statm): 18969 17527 145 145 0 18824 0
[pid=28412] vsize: 75876
Current children cumulated CPU time (s) 968.66
Current children cumulated vsize (Kb) 78000

[startup+980.072 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28412
Raw data (/proc/28408/stat): 28408 (minisat+_script) S 28407 28408 4419 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856122132 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28408/statm): 531 226 485 147 0 384 0
[pid=28408] vsize: 2124
Raw data (/proc/28412/stat): 28412 (minisat+_64-bit) R 28408 28408 4419 0 -1 0 18076 0 0 0 97745 119 0 0 25 0 1 0 1856122137 77901824 17577 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28412/statm): 19019 17577 145 145 0 18874 0
[pid=28412] vsize: 76076
Current children cumulated CPU time (s) 978.65
Current children cumulated vsize (Kb) 78200

[startup+990.072 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28412
Raw data (/proc/28408/stat): 28408 (minisat+_script) S 28407 28408 4419 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856122132 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28408/statm): 531 226 485 147 0 384 0
[pid=28408] vsize: 2124
Raw data (/proc/28412/stat): 28412 (minisat+_64-bit) R 28408 28408 4419 0 -1 0 18136 0 0 0 98745 120 0 0 25 0 1 0 1856122137 78159872 17637 4294967295 134512640 135094434 3221224432 3221223088 134557884 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28412/statm): 19082 17637 145 145 0 18937 0
[pid=28412] vsize: 76328
Current children cumulated CPU time (s) 988.66
Current children cumulated vsize (Kb) 78452

[startup+1000.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28412
Raw data (/proc/28408/stat): 28408 (minisat+_script) S 28407 28408 4419 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856122132 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28408/statm): 531 226 485 147 0 384 0
[pid=28408] vsize: 2124
Raw data (/proc/28412/stat): 28412 (minisat+_64-bit) R 28408 28408 4419 0 -1 0 18214 0 0 0 99744 120 0 0 25 0 1 0 1856122137 78467072 17715 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28412/statm): 19157 17715 145 145 0 19012 0
[pid=28412] vsize: 76628
Current children cumulated CPU time (s) 998.65
Current children cumulated vsize (Kb) 78752

[startup+1010.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28412
Raw data (/proc/28408/stat): 28408 (minisat+_script) S 28407 28408 4419 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856122132 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28408/statm): 531 226 485 147 0 384 0
[pid=28408] vsize: 2124
Raw data (/proc/28412/stat): 28412 (minisat+_64-bit) R 28408 28408 4419 0 -1 0 18364 0 0 0 100741 121 0 0 25 0 1 0 1856122137 79097856 17865 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28412/statm): 19311 17865 145 145 0 19166 0
[pid=28412] vsize: 77244
Current children cumulated CPU time (s) 1008.63
Current children cumulated vsize (Kb) 79368

[startup+1020.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28412
Raw data (/proc/28408/stat): 28408 (minisat+_script) S 28407 28408 4419 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856122132 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28408/statm): 531 226 485 147 0 384 0
[pid=28408] vsize: 2124
Raw data (/proc/28412/stat): 28412 (minisat+_64-bit) R 28408 28408 4419 0 -1 0 18427 0 0 0 101740 122 0 0 25 0 1 0 1856122137 79351808 17928 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28412/statm): 19373 17928 145 145 0 19228 0
[pid=28412] vsize: 77492
Current children cumulated CPU time (s) 1018.63
Current children cumulated vsize (Kb) 79616

[startup+1030.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28412
Raw data (/proc/28408/stat): 28408 (minisat+_script) S 28407 28408 4419 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856122132 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28408/statm): 531 226 485 147 0 384 0
[pid=28408] vsize: 2124
Raw data (/proc/28412/stat): 28412 (minisat+_64-bit) R 28408 28408 4419 0 -1 0 18578 0 0 0 102738 123 0 0 25 0 1 0 1856122137 79958016 18079 4294967295 134512640 135094434 3221224432 3221223056 134562057 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28412/statm): 19521 18079 145 145 0 19376 0
[pid=28412] vsize: 78084
Current children cumulated CPU time (s) 1028.62
Current children cumulated vsize (Kb) 80208

[startup+1040.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28412
Raw data (/proc/28408/stat): 28408 (minisat+_script) S 28407 28408 4419 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856122132 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28408/statm): 531 226 485 147 0 384 0
[pid=28408] vsize: 2124
Raw data (/proc/28412/stat): 28412 (minisat+_64-bit) R 28408 28408 4419 0 -1 0 18730 0 0 0 103736 124 0 0 25 0 1 0 1856122137 80568320 18231 4294967295 134512640 135094434 3221224432 3221223120 134554723 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28412/statm): 19670 18231 145 145 0 19525 0
[pid=28412] vsize: 78680
Current children cumulated CPU time (s) 1038.61
Current children cumulated vsize (Kb) 80804

[startup+1050.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28412
Raw data (/proc/28408/stat): 28408 (minisat+_script) S 28407 28408 4419 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856122132 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28408/statm): 531 226 485 147 0 384 0
[pid=28408] vsize: 2124
Raw data (/proc/28412/stat): 28412 (minisat+_64-bit) R 28408 28408 4419 0 -1 0 18830 0 0 0 104734 125 0 0 25 0 1 0 1856122137 80977920 18331 4294967295 134512640 135094434 3221224432 3221223044 134563046 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28412/statm): 19770 18331 145 145 0 19625 0
[pid=28412] vsize: 79080
Current children cumulated CPU time (s) 1048.6
Current children cumulated vsize (Kb) 81204

[startup+1060.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28412
Raw data (/proc/28408/stat): 28408 (minisat+_script) S 28407 28408 4419 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856122132 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28408/statm): 531 226 485 147 0 384 0
[pid=28408] vsize: 2124
Raw data (/proc/28412/stat): 28412 (minisat+_64-bit) R 28408 28408 4419 0 -1 0 18944 0 0 0 105732 126 0 0 25 0 1 0 1856122137 81457152 18445 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28412/statm): 19887 18445 145 145 0 19742 0
[pid=28412] vsize: 79548
Current children cumulated CPU time (s) 1058.59
Current children cumulated vsize (Kb) 81672

[startup+1070.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28412
Raw data (/proc/28408/stat): 28408 (minisat+_script) S 28407 28408 4419 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856122132 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28408/statm): 531 226 485 147 0 384 0
[pid=28408] vsize: 2124
Raw data (/proc/28412/stat): 28412 (minisat+_64-bit) R 28408 28408 4419 0 -1 0 19044 0 0 0 106731 127 0 0 25 0 1 0 1856122137 81858560 18545 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28412/statm): 19985 18545 145 145 0 19840 0
[pid=28412] vsize: 79940
Current children cumulated CPU time (s) 1068.59
Current children cumulated vsize (Kb) 82064

[startup+1080.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28412
Raw data (/proc/28408/stat): 28408 (minisat+_script) S 28407 28408 4419 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856122132 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28408/statm): 531 226 485 147 0 384 0
[pid=28408] vsize: 2124
Raw data (/proc/28412/stat): 28412 (minisat+_64-bit) R 28408 28408 4419 0 -1 0 19409 0 0 0 107725 129 0 0 25 0 1 0 1856122137 83341312 18910 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28412/statm): 20347 18910 145 145 0 20202 0
[pid=28412] vsize: 81388
Current children cumulated CPU time (s) 1078.55
Current children cumulated vsize (Kb) 83512

[startup+1090.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28412
Raw data (/proc/28408/stat): 28408 (minisat+_script) S 28407 28408 4419 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856122132 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28408/statm): 531 226 485 147 0 384 0
[pid=28408] vsize: 2124
Raw data (/proc/28412/stat): 28412 (minisat+_64-bit) R 28408 28408 4419 0 -1 0 19524 0 0 0 108723 130 0 0 25 0 1 0 1856122137 83800064 19025 4294967295 134512640 135094434 3221224432 3221223072 134558048 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28412/statm): 20459 19025 145 145 0 20314 0
[pid=28412] vsize: 81836
Current children cumulated CPU time (s) 1088.54
Current children cumulated vsize (Kb) 83960

[startup+1100.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28412
Raw data (/proc/28408/stat): 28408 (minisat+_script) S 28407 28408 4419 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856122132 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28408/statm): 531 226 485 147 0 384 0
[pid=28408] vsize: 2124
Raw data (/proc/28412/stat): 28412 (minisat+_64-bit) R 28408 28408 4419 0 -1 0 19648 0 0 0 109721 131 0 0 25 0 1 0 1856122137 84299776 19149 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28412/statm): 20581 19149 145 145 0 20436 0
[pid=28412] vsize: 82324
Current children cumulated CPU time (s) 1098.53
Current children cumulated vsize (Kb) 84448

[startup+1110.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28412
Raw data (/proc/28408/stat): 28408 (minisat+_script) S 28407 28408 4419 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856122132 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28408/statm): 531 226 485 147 0 384 0
[pid=28408] vsize: 2124
Raw data (/proc/28412/stat): 28412 (minisat+_64-bit) R 28408 28408 4419 0 -1 0 19748 0 0 0 110721 131 0 0 25 0 1 0 1856122137 84709376 19249 4294967295 134512640 135094434 3221224432 3221223088 134557903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28412/statm): 20681 19249 145 145 0 20536 0
[pid=28412] vsize: 82724
Current children cumulated CPU time (s) 1108.53
Current children cumulated vsize (Kb) 84848

[startup+1120.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28412
Raw data (/proc/28408/stat): 28408 (minisat+_script) S 28407 28408 4419 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856122132 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28408/statm): 531 226 485 147 0 384 0
[pid=28408] vsize: 2124
Raw data (/proc/28412/stat): 28412 (minisat+_64-bit) R 28408 28408 4419 0 -1 0 19851 0 0 0 111719 132 0 0 25 0 1 0 1856122137 85118976 19352 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28412/statm): 20781 19352 145 145 0 20636 0
[pid=28412] vsize: 83124
Current children cumulated CPU time (s) 1118.52
Current children cumulated vsize (Kb) 85248

[startup+1130.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28412
Raw data (/proc/28408/stat): 28408 (minisat+_script) S 28407 28408 4419 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856122132 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28408/statm): 531 226 485 147 0 384 0
[pid=28408] vsize: 2124
Raw data (/proc/28412/stat): 28412 (minisat+_64-bit) R 28408 28408 4419 0 -1 0 20022 0 0 0 112716 133 0 0 25 0 1 0 1856122137 85811200 19523 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28412/statm): 20950 19523 145 145 0 20805 0
[pid=28412] vsize: 83800
Current children cumulated CPU time (s) 1128.5
Current children cumulated vsize (Kb) 85924

[startup+1140.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28412
Raw data (/proc/28408/stat): 28408 (minisat+_script) S 28407 28408 4419 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856122132 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28408/statm): 531 226 485 147 0 384 0
[pid=28408] vsize: 2124
Raw data (/proc/28412/stat): 28412 (minisat+_64-bit) R 28408 28408 4419 0 -1 0 20178 0 0 0 113713 134 0 0 25 0 1 0 1856122137 86454272 19679 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28412/statm): 21107 19679 145 145 0 20962 0
[pid=28412] vsize: 84428
Current children cumulated CPU time (s) 1138.48
Current children cumulated vsize (Kb) 86552

[startup+1150.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28412
Raw data (/proc/28408/stat): 28408 (minisat+_script) S 28407 28408 4419 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856122132 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28408/statm): 531 226 485 147 0 384 0
[pid=28408] vsize: 2124
Raw data (/proc/28412/stat): 28412 (minisat+_64-bit) R 28408 28408 4419 0 -1 0 20247 0 0 0 114712 135 0 0 25 0 1 0 1856122137 86728704 19748 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28412/statm): 21174 19748 145 145 0 21029 0
[pid=28412] vsize: 84696
Current children cumulated CPU time (s) 1148.48
Current children cumulated vsize (Kb) 86820

[startup+1160.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28412
Raw data (/proc/28408/stat): 28408 (minisat+_script) S 28407 28408 4419 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856122132 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28408/statm): 531 226 485 147 0 384 0
[pid=28408] vsize: 2124
Raw data (/proc/28412/stat): 28412 (minisat+_64-bit) R 28408 28408 4419 0 -1 0 20357 0 0 0 115711 136 0 0 25 0 1 0 1856122137 87187456 19858 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28412/statm): 21286 19858 145 145 0 21141 0
[pid=28412] vsize: 85144
Current children cumulated CPU time (s) 1158.48
Current children cumulated vsize (Kb) 87268

[startup+1170.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28412
Raw data (/proc/28408/stat): 28408 (minisat+_script) S 28407 28408 4419 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856122132 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28408/statm): 531 226 485 147 0 384 0
[pid=28408] vsize: 2124
Raw data (/proc/28412/stat): 28412 (minisat+_64-bit) R 28408 28408 4419 0 -1 0 20510 0 0 0 116708 137 0 0 25 0 1 0 1856122137 87805952 20011 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28412/statm): 21437 20011 145 145 0 21292 0
[pid=28412] vsize: 85748
Current children cumulated CPU time (s) 1168.46
Current children cumulated vsize (Kb) 87872

[startup+1180.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28412
Raw data (/proc/28408/stat): 28408 (minisat+_script) S 28407 28408 4419 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856122132 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28408/statm): 531 226 485 147 0 384 0
[pid=28408] vsize: 2124
Raw data (/proc/28412/stat): 28412 (minisat+_64-bit) R 28408 28408 4419 0 -1 0 20706 0 0 0 117705 139 0 0 25 0 1 0 1856122137 88596480 20207 4294967295 134512640 135094434 3221224432 3221223088 134558235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28412/statm): 21630 20207 145 145 0 21485 0
[pid=28412] vsize: 86520
Current children cumulated CPU time (s) 1178.45
Current children cumulated vsize (Kb) 88644

[startup+1190.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28412
Raw data (/proc/28408/stat): 28408 (minisat+_script) S 28407 28408 4419 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856122132 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28408/statm): 531 226 485 147 0 384 0
[pid=28408] vsize: 2124
Raw data (/proc/28412/stat): 28412 (minisat+_64-bit) R 28408 28408 4419 0 -1 0 20947 0 0 0 118701 141 0 0 25 0 1 0 1856122137 89579520 20448 4294967295 134512640 135094434 3221224432 3221223024 134556806 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28412/statm): 21870 20448 145 145 0 21725 0
[pid=28412] vsize: 87480
Current children cumulated CPU time (s) 1188.43
Current children cumulated vsize (Kb) 89604

[startup+1200.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28412
Raw data (/proc/28408/stat): 28408 (minisat+_script) S 28407 28408 4419 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856122132 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28408/statm): 531 226 485 147 0 384 0
[pid=28408] vsize: 2124
Raw data (/proc/28412/stat): 28412 (minisat+_64-bit) R 28408 28408 4419 0 -1 0 21209 0 0 0 119697 142 0 0 25 0 1 0 1856122137 90644480 20710 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28412/statm): 22130 20710 145 145 0 21985 0
[pid=28412] vsize: 88520
Current children cumulated CPU time (s) 1198.4
Current children cumulated vsize (Kb) 90644

[startup+1210.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28412
Raw data (/proc/28408/stat): 28408 (minisat+_script) S 28407 28408 4419 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856122132 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28408/statm): 531 226 485 147 0 384 0
[pid=28408] vsize: 2124
Raw data (/proc/28412/stat): 28412 (minisat+_64-bit) R 28408 28408 4419 0 -1 0 21485 0 0 0 120691 145 0 0 25 0 1 0 1856122137 91770880 20986 4294967295 134512640 135094434 3221224432 3221223024 134557500 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28412/statm): 22405 20986 145 145 0 22260 0
[pid=28412] vsize: 89620
Current children cumulated CPU time (s) 1208.37
Current children cumulated vsize (Kb) 91744



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28412
Raw data (/proc/28408/stat): 28408 (minisat+_script) S 28407 28408 4419 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856122132 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28408/statm): 531 226 485 147 0 384 0
[pid=28408] vsize: 2124
Raw data (/proc/28412/stat): 28412 (minisat+_64-bit) R 28408 28408 4419 0 -1 0 21485 0 0 0 120691 145 0 0 25 0 1 0 1856122137 91770880 20986 4294967295 134512640 135094434 3221224432 3221223024 134557416 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28412/statm): 22405 20986 145 145 0 22260 0
[pid=28412] vsize: 89620
Current children cumulated CPU time (s) 1208.37
Current children cumulated vsize (Kb) 91744

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

Child status: 0
Real time (s): 1210.13
CPU time (s): 1208.41
CPU user time (s): 1206.91
CPU system time (s): 1.49277
CPU usage (%): 99.8577
Max. virtual memory (cumulated for all children) (Kb): 91744

Verifier Data

ERROR: no interpretation found !