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-20-10/MIPLIB/miplib2003/normalized-mps-v2-20-10-roll3000.opb
MD5SUMe92110eefe66ae3240a292dc732eb360
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 31
Biggest coefficient in the objective function 1073741824
Number of bits for the biggest coefficient in the objective function 31
Sum of the numbers in the objective function 2147483647
Number of bits of the sum of numbers in the objective function 31
Biggest number in a constraint 1024000000000
Number of bits of the biggest number in a constraint 40
Biggest sum of numbers in a constraint 2123511627775
Number of bits of the biggest sum of numbers41
Best result obtained on this benchmark
Best CPU time to get the best result obtained on this benchmark
Number of variables8902
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 constraint2407

Trace number 3940

Launcher Data

LAUNCH ON wulflinc11 THE 2005-09-19 03:57:55 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=2940 boxname=wulflinc11 idbench=596 idsolver=3 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  e92110eefe66ae3240a292dc732eb360  /oldhome/oroussel/tmp/wulflinc11/normalized-mps-v2-20-10-roll3000.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc11/normalized-mps-v2-20-10-roll3000.opb
IDLAUNCH: 2940
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.028
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	: 2
cpu MHz		: 451.028
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 899.07

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        877708 kB
Buffers:         35664 kB
Cached:          93484 kB
SwapCached:        732 kB
Active:          65152 kB
Inactive:        66624 kB
HighTotal:      131008 kB
HighFree:        35672 kB
LowTotal:       903652 kB
LowFree:        842036 kB
SwapTotal:     2097136 kB
SwapFree:      2095856 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5716 kB
Slab:            19444 kB
Committed_AS:    64168 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-09-19 04:18:05 (client local time) WITH STATUS 0 IN 1208.7 SECONDS
stats: 2940 7 1208.7 0

Solver Data

c Parsing PB file...
c Converting 2918 PB-constraints to clauses...
c   -- Unit propagations: pppppppppppppppppppppp
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:   14
c ---[2460]---> BDD-cost:   14
c ---[2453]---> BDD-cost:   14
c ---[2452]---> BDD-cost:   14
c ---[2450]---> BDD-cost:   14
c ---[2449]---> BDD-cost:   14
c ---[2447]---> BDD-cost:   14
c ---[2446]---> BDD-cost:   14
c ---[2445]---> BDD-cost:   14
c ---[2443]---> BDD-cost:   14
c ---[2442]---> BDD-cost:   14
c ---[2440]---> BDD-cost:   14
c ---[2439]---> BDD-cost:   14
c ---[2438]---> BDD-cost:   14
c ---[2436]---> BDD-cost:   14
c ---[2435]---> BDD-cost:   14
c ---[2433]---> BDD-cost:   14
c ---[2432]---> BDD-cost:   14
c ---[2431]---> BDD-cost:   14
c ---[2429]---> BDD-cost:   14
c ---[2428]---> BDD-cost:   14
c ---[2427]---> BDD-cost:   14
c ---[2426]---> BDD-cost:   14
c ---[2425]---> BDD-cost:   14
c ---[2424]---> BDD-cost:   14
c ---[2422]---> BDD-cost:   14
c ---[2421]---> BDD-cost:   14
c ---[2420]---> BDD-cost:   14
c ---[2419]---> BDD-cost:   14
c ---[2418]---> BDD-cost:   14
c ---[2417]---> BDD-cost:   14
c ---[2415]---> BDD-cost:   14
c ---[2414]---> BDD-cost:   14
c ---[2413]---> BDD-cost:   14
c ---[2412]---> BDD-cost:   14
c ---[2411]---> BDD-cost:   14
c ---[2410]---> BDD-cost:   14
c ---[2407]---> BDD-cost:   14
c ---[2406]---> BDD-cost:   14
c ---[2405]---> BDD-cost:   14
c ---[2403]---> BDD-cost:   14
c ---[2402]---> BDD-cost:   14
c ---[2401]---> BDD-cost:   14
c ---[2400]---> BDD-cost:   14
c ---[2399]---> BDD-cost:   14
c ---[2397]---> BDD-cost:   14
c ---[2396]---> BDD-cost:   14
c ---[2395]---> BDD-cost:   14
c ---[2394]---> BDD-cost:   14
c ---[2393]---> BDD-cost:   14
c ---[2391]---> BDD-cost:   14
c ---[2390]---> BDD-cost:   14
c ---[2389]---> BDD-cost:   14
c ---[2388]---> BDD-cost:   14
c ---[2387]---> BDD-cost:   14
c ---[2385]---> BDD-cost:   14
c ---[2384]---> BDD-cost:   14
c ---[2383]---> BDD-cost:   14
c ---[2382]---> BDD-cost:   14
c ---[2380]---> BDD-cost:   14
c ---[2379]---> BDD-cost:   14
c ---[2378]---> BDD-cost:   14
c ---[2377]---> BDD-cost:   14
c ---[2376]---> BDD-cost:   14
c ---[2375]---> BDD-cost:   14
c ---[2374]---> BDD-cost:   14
c ---[2373]---> BDD-cost:   14
c ---[2372]---> BDD-cost:   14
c ---[2371]---> BDD-cost:   14
c ---[2370]---> BDD-cost:   14
c ---[2369]---> BDD-cost:   14
c ---[2368]---> BDD-cost:   14
c ---[2367]---> BDD-cost:   14
c ---[2366]---> BDD-cost:   14
c ---[2365]---> BDD-cost:   14
c ---[2364]---> BDD-cost:   14
c ---[2363]---> BDD-cost:   14
c ---[2362]---> BDD-cost:   14
c ---[2361]---> BDD-cost:   14
c ---[2360]---> BDD-cost:   14
c ---[2359]---> BDD-cost:   14
c ---[2358]---> BDD-cost:   14
c ---[2357]---> BDD-cost:   14
c ---[2356]---> BDD-cost:   14
c ---[2355]---> BDD-cost:   14
c ---[2354]---> BDD-cost:   14
c ---[2353]---> BDD-cost:   14
c ---[2352]---> BDD-cost:   14
c ---[2351]---> BDD-cost:   14
c ---[2350]---> BDD-cost:   14
c ---[2349]---> BDD-cost:   14
c ---[2348]---> BDD-cost:   14
c ---[2347]---> BDD-cost:   14
c ---[2346]---> BDD-cost:   14
c ---[2345]---> BDD-cost:   14
c ---[2344]---> BDD-cost:   14
c ---[2343]---> BDD-cost:   14
c ---[2342]---> BDD-cost:   14
c ---[2341]---> BDD-cost:   14
c ---[2340]---> BDD-cost:   14
c ---[2339]---> BDD-cost:   14
c ---[2338]---> BDD-cost:   14
c ---[2337]---> BDD-cost:   14
c ---[2336]---> BDD-cost:   14
c ---[2335]---> BDD-cost:   14
c ---[2334]---> BDD-cost:   14
c ---[2333]---> BDD-cost:   14
c ---[2332]---> BDD-cost:   14
c ---[2331]---> BDD-cost:   14
c ---[2330]---> BDD-cost:   14
c ---[2329]---> BDD-cost:   14
c ---[2328]---> BDD-cost:   14
c ---[2327]---> BDD-cost:   14
c ---[2326]---> BDD-cost:   14
c ---[2325]---> BDD-cost:   14
c ---[2324]---> BDD-cost:   14
c ---[2323]---> BDD-cost:   14
c ---[2322]---> BDD-cost:   14
c ---[2321]---> BDD-cost:   14
c ---[2320]---> BDD-cost:   14
c ---[2319]---> BDD-cost:   14
c ---[2318]---> BDD-cost:   14
c ---[2317]---> BDD-cost:   14
c ---[2316]---> BDD-cost:   14
c ---[2315]---> BDD-cost:   14
c ---[2314]---> BDD-cost:   14
c ---[2313]---> BDD-cost:   14
c ---[2312]---> BDD-cost:   14
c ---[2311]---> BDD-cost:   14
c ---[2310]---> BDD-cost:   14
c ---[2309]---> BDD-cost:   14
c ---[2308]---> BDD-cost:   14
c ---[2307]---> BDD-cost:   14
c ---[2306]---> BDD-cost:   14
c ---[2305]---> BDD-cost:   14
c ---[2304]---> BDD-cost:   14
c ---[2303]---> BDD-cost:   14
c ---[2302]---> BDD-cost:   14
c ---[2301]---> BDD-cost:   14
c ---[2300]---> BDD-cost:   14
c ---[2299]---> BDD-cost:   14
c ---[2298]---> BDD-cost:   14
c ---[2297]---> BDD-cost:   14
c ---[2296]---> BDD-cost:   14
c ---[2295]---> BDD-cost:   14
c ---[2294]---> BDD-cost:   14
c ---[2293]---> BDD-cost:   14
c ---[2292]---> BDD-cost:   14
c ---[2291]---> BDD-cost:   14
c ---[2290]---> BDD-cost:   14
c ---[2289]---> BDD-cost:   14
c ---[2288]---> BDD-cost:   14
c ---[2287]---> BDD-cost:   14
c ---[2286]---> BDD-cost:   14
c ---[2285]---> BDD-cost:   14
c ---[2284]---> BDD-cost:   14
c ---[2283]---> BDD-cost:   11
c ---[2282]---> BDD-cost:   11
c ---[2281]---> BDD-cost:   11
c ---[2280]---> BDD-cost:   11
c ---[2279]---> BDD-cost:   11
c ---[2278]---> BDD-cost:  122
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:   76
c ---[1687]---> Adder-cost: 188   maxlim: 104447   bits: 18/17
c ---[1685]---> Adder-cost: 232   maxlim: 120831   bits: 18/17
c ---[1683]---> BDD-cost:   76
c ---[1681]---> Sorter-cost:  334     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1679]---> Sorter-cost: 1319     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1677]---> Adder-cost: 192   maxlim: 117759   bits: 18/17
c ---[1676]---> BDD-cost:    1
c ---[1674]---> Adder-cost: 208   maxlim: 121855   bits: 18/17
c ---[1672]---> Sorter-cost:  529     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1670]---> Adder-cost: 146   maxlim: 106495   bits: 18/17
c ---[1668]---> Adder-cost: 220   maxlim: 120831   bits: 18/17
c ---[1666]---> Sorter-cost:  591     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1664]---> Sorter-cost: 1480     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1662]---> Adder-cost: 180   maxlim: 118783   bits: 18/17
c ---[1660]---> Adder-cost: 154   maxlim: 122879   bits: 18/17
c ---[1658]---> Sorter-cost:  923     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1656]---> Adder-cost: 168   maxlim: 108543   bits: 18/17
c ---[1653]---> Adder-cost: 152   maxlim: 126975   bits: 18/17
c ---[1651]---> Sorter-cost:  917     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1649]---> Sorter-cost: 1659     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1647]---> Adder-cost: 144   maxlim: 120831   bits: 18/17
c ---[1645]---> Adder-cost: 212   maxlim: 126975   bits: 18/17
c ---[1643]---> Sorter-cost: 1065     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1641]---> Adder-cost: 138   maxlim: 109567   bits: 18/17
c ---[1639]---> Adder-cost: 178   maxlim: 130047   bits: 18/17
c ---[1637]---> Sorter-cost: 1097     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1635]---> Sorter-cost: 1708     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1634]---> BDD-cost:    2
c ---[1632]---> Adder-cost: 178   maxlim: 121855   bits: 18/17
c ---[1630]---> Adder-cost: 172   maxlim: 127999   bits: 18/17
c ---[1628]---> Sorter-cost:  405     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1626]---> Sorter-cost: 1226     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1624]---> Adder-cost: 136   maxlim: 110591   bits: 18/17
c ---[1622]---> Adder-cost: 170   maxlim: 131071   bits: 18/17
c ---[1620]---> Sorter-cost: 1771     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1618]---> Adder-cost: 130   maxlim: 122879   bits: 18/17
c ---[1616]---> Adder-cost: 142   maxlim: 125951   bits: 18/17
c ---[1614]---> Sorter-cost:  687     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1611]---> Sorter-cost: 1147     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1609]---> Adder-cost: 130   maxlim: 112639   bits: 18/17
c ---[1607]---> Adder-cost: 172   maxlim: 135167   bits: 18/18
c ---[1605]---> Sorter-cost: 1820     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1603]---> Adder-cost: 132   maxlim: 123903   bits: 18/17
c ---[1601]---> Adder-cost: 158   maxlim: 126975   bits: 18/17
c ---[1599]---> Sorter-cost:  375     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1597]---> Sorter-cost: 1262     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1595]---> Adder-cost: 150   maxlim: 113663   bits: 18/17
c ---[1593]---> Adder-cost: 156   maxlim: 136191   bits: 18/18
c ---[1592]---> BDD-cost:    2
c ---[1590]---> Sorter-cost: 1879     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1588]---> Adder-cost: 140   maxlim: 124927   bits: 18/17
c ---[1586]---> Adder-cost: 186   maxlim: 124927   bits: 18/17
c ---[1584]---> Sorter-cost:  317     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1582]---> Sorter-cost: 1353     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1580]---> Adder-cost: 142   maxlim: 114687   bits: 18/17
c ---[1578]---> Adder-cost: 164   maxlim: 137215   bits: 18/18
c ---[1576]---> BDD-cost:   98
c ---[1574]---> Adder-cost: 154   maxlim: 112639   bits: 18/17
c ---[1572]---> Adder-cost: 142   maxlim: 124927   bits: 18/17
c ---[1571]---> BDD-cost:    8
c ---[1568]---> Sorter-cost: 1474     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1566]---> Adder-cost: 128   maxlim: 115711   bits: 18/17
c ---[1564]---> Adder-cost: 150   maxlim: 138239   bits: 18/18
c ---[1562]---> Sorter-cost:  427     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1560]---> Adder-cost: 132   maxlim: 113663   bits: 18/17
c ---[1558]---> Adder-cost: 130   maxlim: 123903   bits: 18/17
c ---[1556]---> Sorter-cost: 1519     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1554]---> Adder-cost: 130   maxlim: 116735   bits: 18/17
c ---[1552]---> Adder-cost: 160   maxlim: 139263   bits: 18/18
c ---[1550]---> Sorter-cost:  523     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1549]---> BDD-cost:    2
c ---[1547]---> Adder-cost: 124   maxlim: 114687   bits: 18/17
c ---[1545]---> Adder-cost: 120   maxlim: 122879   bits: 18/17
c ---[1543]---> Adder-cost: 110   maxlim: 96255   bits: 17/17
c ---[1541]---> Adder-cost: 134   maxlim: 116735   bits: 18/17
c ---[1539]---> Adder-cost: 256   maxlim: 136191   bits: 18/18
c ---[1537]---> Sorter-cost:  757     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1535]---> Adder-cost: 114   maxlim: 115711   bits: 18/17
c ---[1533]---> Adder-cost: 150   maxlim: 123903   bits: 18/17
c ---[1531]---> Adder-cost: 98   maxlim: 101375   bits: 17/17
c ---[1529]---> Adder-cost: 174   maxlim: 119807   bits: 18/17
c ---[1526]---> Sorter-cost: 1027     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1524]---> Adder-cost: 112   maxlim: 116735   bits: 18/17
c ---[1522]---> Adder-cost: 120   maxlim: 122879   bits: 18/17
c ---[1520]---> BDD-cost:   81
c ---[1518]---> Adder-cost: 188   maxlim: 104447   bits: 18/17
c ---[1516]---> Adder-cost: 234   maxlim: 120831   bits: 18/17
c ---[1514]---> BDD-cost:   81
c ---[1512]---> Sorter-cost:  345     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1510]---> Adder-cost: 124   maxlim: 91135   bits: 17/17
c ---[1508]---> Adder-cost: 180   maxlim: 117759   bits: 18/17
c ---[1507]---> BDD-cost:    1
c ---[1505]---> Adder-cost: 210   maxlim: 121855   bits: 18/17
c ---[1503]---> Sorter-cost:  587     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1501]---> Adder-cost: 146   maxlim: 106495   bits: 18/17
c ---[1499]---> Adder-cost: 222   maxlim: 120831   bits: 18/17
c ---[1497]---> Sorter-cost:  670     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1495]---> Adder-cost: 114   maxlim: 94207   bits: 17/17
c ---[1493]---> Adder-cost: 170   maxlim: 118783   bits: 18/17
c ---[1491]---> Adder-cost: 156   maxlim: 122879   bits: 18/17
c ---[1489]---> Sorter-cost: 1203     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1487]---> Adder-cost: 168   maxlim: 108543   bits: 18/17
c ---[1484]---> Adder-cost: 152   maxlim: 126975   bits: 18/17
c ---[1482]---> Sorter-cost:  964     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1480]---> Adder-cost: 102   maxlim: 98303   bits: 18/17
c ---[1478]---> Adder-cost: 142   maxlim: 120831   bits: 18/17
c ---[1476]---> Adder-cost: 212   maxlim: 126975   bits: 18/17
c ---[1474]---> Sorter-cost: 1236     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1472]---> Adder-cost: 138   maxlim: 109567   bits: 18/17
c ---[1470]---> Adder-cost: 178   maxlim: 130047   bits: 18/17
c ---[1468]---> Sorter-cost: 1365     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1466]---> Adder-cost: 110   maxlim: 101375   bits: 18/17
c ---[1465]---> BDD-cost:    2
c ---[1463]---> Adder-cost: 174   maxlim: 121855   bits: 18/17
c ---[1461]---> Adder-cost: 172   maxlim: 127999   bits: 18/17
c ---[1459]---> Sorter-cost:  365     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1457]---> Sorter-cost: 1368     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1455]---> Adder-cost: 136   maxlim: 110591   bits: 18/17
c ---[1453]---> Adder-cost: 170   maxlim: 131071   bits: 18/17
c ---[1451]---> Adder-cost: 140   maxlim: 104447   bits: 18/17
c ---[1449]---> Adder-cost: 132   maxlim: 122879   bits: 18/17
c ---[1447]---> Adder-cost: 142   maxlim: 125951   bits: 18/17
c ---[1445]---> Sorter-cost:  772     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1442]---> Sorter-cost: 1283     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1440]---> Adder-cost: 130   maxlim: 112639   bits: 18/17
c ---[1438]---> Adder-cost: 176   maxlim: 135167   bits: 18/18
c ---[1436]---> Adder-cost: 118   maxlim: 107519   bits: 18/17
c ---[1434]---> Adder-cost: 134   maxlim: 123903   bits: 18/17
c ---[1432]---> Adder-cost: 158   maxlim: 126975   bits: 18/17
c ---[1430]---> Sorter-cost:  315     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1428]---> Sorter-cost: 1400     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1426]---> Adder-cost: 150   maxlim: 113663   bits: 18/17
c ---[1424]---> Adder-cost: 160   maxlim: 136191   bits: 18/18
c ---[1423]---> BDD-cost:    2
c ---[1421]---> Adder-cost: 126   maxlim: 110591   bits: 18/17
c ---[1419]---> Adder-cost: 142   maxlim: 124927   bits: 18/17
c ---[1417]---> Adder-cost: 186   maxlim: 124927   bits: 18/17
c ---[1415]---> Sorter-cost:  343     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1413]---> Sorter-cost: 1489     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1411]---> Adder-cost: 144   maxlim: 114687   bits: 18/17
c ---[1409]---> Adder-cost: 168   maxlim: 137215   bits: 18/18
c ---[1407]---> BDD-cost:  106
c ---[1405]---> Adder-cost: 120   maxlim: 112639   bits: 18/17
c ---[1403]---> Adder-cost: 144   maxlim: 124927   bits: 18/17
c ---[1400]---> Sorter-cost: 1606     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1398]---> Adder-cost: 130   maxlim: 115711   bits: 18/17
c ---[1396]---> Adder-cost: 154   maxlim: 138239   bits: 18/18
c ---[1394]---> Sorter-cost:  520     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1392]---> Adder-cost: 116   maxlim: 113663   bits: 18/17
c ---[1390]---> Adder-cost: 132   maxlim: 123903   bits: 18/17
c ---[1388]---> Adder-cost: 146   maxlim: 94207   bits: 18/17
c ---[1386]---> Adder-cost: 132   maxlim: 116735   bits: 18/17
c ---[1384]---> Adder-cost: 160   maxlim: 139263   bits: 18/18
c ---[1382]---> Sorter-cost:  712     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1381]---> BDD-cost:    1
c ---[1379]---> Adder-cost: 118   maxlim: 114687   bits: 18/17
c ---[1377]---> Adder-cost: 122   maxlim: 122879   bits: 18/17
c ---[1375]---> Adder-cost: 116   maxlim: 96255   bits: 18/17
c ---[1373]---> Adder-cost: 136   maxlim: 116735   bits: 18/17
c ---[1371]---> Adder-cost: 256   maxlim: 136191   bits: 18/18
c ---[1369]---> Sorter-cost:  854     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1367]---> Adder-cost: 114   maxlim: 115711   bits: 18/17
c ---[1365]---> Adder-cost: 152   maxlim: 123903   bits: 18/17
c ---[1363]---> Adder-cost: 104   maxlim: 101375   bits: 18/17
c ---[1361]---> Adder-cost: 176   maxlim: 119807   bits: 18/17
c ---[1359]---> Sorter-cost:  921     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1355]---> Sorter-cost: 1335     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1353]---> Adder-cost: 112   maxlim: 116735   bits: 18/17
c ---[1351]---> Adder-cost: 122   maxlim: 122879   bits: 18/17
c ---[1349]---> Adder-cost: 250   maxlim: 110591   bits: 18/17
c ---[1347]---> Sorter-cost:  929     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1345]---> Adder-cost: 184   maxlim: 79871   bits: 18/17
c ---[1343]---> Adder-cost: 146   maxlim: 100351   bits: 18/17
c ---[1341]---> Sorter-cost:  567     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1339]---> Adder-cost: 250   maxlim: 110591   bits: 18/17
c ---[1337]---> Sorter-cost:  819     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1336]---> BDD-cost:    2
c ---[1334]---> Adder-cost: 184   maxlim: 79871   bits: 18/17
c ---[1332]---> Adder-cost: 146   maxlim: 100351   bits: 18/17
c ---[1330]---> Sorter-cost:  619     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1329]---> BDD-cost:  111
c ---[1328]---> BDD-cost:  110
c ---[1327]---> BDD-cost:  111
c ---[1326]---> BDD-cost:  111
c ---[1325]---> BDD-cost:  110
c ---[1324]---> BDD-cost:  115
c ---[1323]---> BDD-cost:  114
c ---[1321]---> BDD-cost:  115
c ---[1320]---> BDD-cost:  115
c ---[1319]---> BDD-cost:  114
c ---[1318]---> Sorter-cost:  815     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1317]---> Sorter-cost:  880     Base: 2 2 2 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: 1600   maxlim: 1048575   bits: 21/20
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: 2138   maxlim: 33554431   bits: 26/25
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: 2788   maxlim: 67108863   bits: 27/26
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:   15
c ---[ 450]---> BDD-cost:   16
c ---[ 449]---> BDD-cost:   16
c ---[ 448]---> BDD-cost:   16
c ---[ 446]---> BDD-cost:   17
c ---[ 445]---> BDD-cost:   17
c ---[ 444]---> BDD-cost:   16
c ---[ 443]---> BDD-cost:   16
c ---[ 442]---> BDD-cost:   16
c ---[ 441]---> BDD-cost:    1
c ---[ 440]---> BDD-cost:   17
c ---[ 439]---> BDD-cost:   17
c ---[ 438]---> BDD-cost:   16
c ---[ 437]---> BDD-cost:   17
c ---[ 436]---> BDD-cost:   17
c ---[ 434]---> BDD-cost:   17
c ---[ 433]---> BDD-cost:   16
c ---[ 431]---> BDD-cost:   16
c ---[ 430]---> BDD-cost:    8
c ---[ 429]---> BDD-cost:   18
c ---[ 428]---> BDD-cost:   16
c ---[ 427]---> BDD-cost:   16
c ---[ 426]---> BDD-cost:   17
c ---[ 425]---> BDD-cost:   17
c ---[ 423]---> BDD-cost:   16
c ---[ 421]---> BDD-cost:   17
c ---[ 420]---> BDD-cost:   15
c ---[ 419]---> BDD-cost:   17
c ---[ 417]---> BDD-cost:    8
c ---[ 415]---> BDD-cost:   16
c ---[ 414]---> BDD-cost:   13
c ---[ 410]---> BDD-cost:   16
c ---[ 408]---> BDD-cost:   16
c ---[ 407]---> BDD-cost:   14
c ---[ 405]---> BDD-cost:    8
c ---[ 404]---> BDD-cost:   17
c ---[ 403]---> BDD-cost:   14
c ---[ 402]---> BDD-cost:   18
c ---[ 401]---> BDD-cost:   15
c ---[ 400]---> BDD-cost:   17
c ---[ 399]---> BDD-cost:   14
c ---[ 396]---> BDD-cost:   18
c ---[ 395]---> BDD-cost:   17
c ---[ 394]---> BDD-cost:   18
c ---[ 393]---> BDD-cost:   16
c ---[ 392]---> BDD-cost:    1
c ---[ 391]---> BDD-cost:   15
c ---[ 390]---> BDD-cost:   18
c ---[ 389]---> BDD-cost:   16
c ---[ 388]---> BDD-cost:   16
c ---[ 385]---> BDD-cost:   16
c ---[ 384]---> BDD-cost:   18
c ---[ 383]---> BDD-cost:   17
c ---[ 382]---> BDD-cost:   15
c ---[ 381]---> BDD-cost:   17
c ---[ 380]---> BDD-cost:    2
c ---[ 379]---> BDD-cost:   11
c ---[ 378]---> BDD-cost:   12
c ---[ 377]---> BDD-cost:   12
c ---[ 376]---> BDD-cost:   12
c ---[ 374]---> BDD-cost:   13
c ---[ 373]---> BDD-cost:   12
c ---[ 371]---> BDD-cost:   12
c ---[ 370]---> BDD-cost:   11
c ---[ 369]---> BDD-cost:   12
c ---[ 368]---> BDD-cost:    2
c ---[ 367]---> BDD-cost:   13
c ---[ 366]---> BDD-cost:   13
c ---[ 365]---> BDD-cost:   11
c ---[ 363]---> BDD-cost:   13
c ---[ 361]---> BDD-cost:   12
c ---[ 360]---> BDD-cost:   11
c ---[ 359]---> BDD-cost:   13
c ---[ 358]---> BDD-cost:   14
c ---[ 357]---> BDD-cost:    2
c ---[ 356]---> BDD-cost:   12
c ---[ 355]---> BDD-cost:   14
c ---[ 354]---> BDD-cost:   13
c ---[ 352]---> BDD-cost:   13
c ---[ 351]---> BDD-cost:    1
c ---[ 349]---> BDD-cost:   13
c ---[ 348]---> BDD-cost:   12
c ---[ 347]---> BDD-cost:   12
c ---[ 346]---> BDD-cost:   13
c ---[ 345]---> BDD-cost:   13
c ---[ 344]---> BDD-cost:    1
c ---[ 343]---> BDD-cost:   11
c ---[ 342]---> BDD-cost:   11
c ---[ 341]---> BDD-cost:    9
c ---[ 340]---> BDD-cost:   10
c ---[ 339]---> BDD-cost:   12
c ---[ 337]---> BDD-cost:   12
c ---[ 336]---> BDD-cost:   13
c ---[ 335]---> BDD-cost:   10
c ---[ 334]---> BDD-cost:   12
c ---[ 333]---> BDD-cost:   13
c ---[ 332]---> BDD-cost:    2
c ---[ 331]---> BDD-cost:    9
c ---[ 330]---> BDD-cost:   13
c ---[ 329]---> BDD-cost:   11
c ---[ 328]---> BDD-cost:   11
c ---[ 327]---> BDD-cost:   11
c ---[ 325]---> BDD-cost:   10
c ---[ 323]---> BDD-cost:   10
c ---[ 321]---> BDD-cost:   11
c ---[ 320]---> BDD-cost:    9
c ---[ 319]---> BDD-cost:    2
c ---[ 316]---> BDD-cost:   10
c ---[ 315]---> BDD-cost:   10
c ---[ 312]---> BDD-cost:   12
c ---[ 311]---> BDD-cost:   13
c ---[ 310]---> BDD-cost:   12
c ---[ 309]---> BDD-cost:   12
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:   13
c ---[  15]---> BDD-cost:   15
c ---[  14]---> BDD-cost:   15
c ---[  13]---> BDD-cost:   14
c ---[  12]---> BDD-cost:   14
c ---[  11]---> BDD-cost:   15
c ---[  10]---> BDD-cost:   10
c ---[   9]---> BDD-cost:   14
c ---[   8]---> BDD-cost:   12
c ---[   7]---> BDD-cost:   10
c ---[   6]---> BDD-cost:    9
c ---[   5]---> BDD-cost:   10
c ---[   4]---> BDD-cost:    9
c ---[   3]---> BDD-cost:   10
c ---[   2]---> BDD-cost:    6
c ---[   1]---> BDD-cost:    6
c ---[   0]---> BDD-cost:   10
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  342915  1035443 |  114305       0        0     nan |  0.000 % |
c |       102 |  342856  1035311 |  125735     100     1336    13.4 | 13.751 % |
c |       253 |  342693  1034943 |  138309     246     2560    10.4 | 13.794 % |
c |       479 |  342693  1034943 |  152139     472     9122    19.3 | 13.794 % |
c |       816 |  342303  1034035 |  167353     789    14353    18.2 | 13.892 % |
c |      1322 |  341817  1032928 |  184089    1284    21956    17.1 | 14.025 % |
c |      2081 |  340088  1028946 |  202498    1741    26110    15.0 | 14.499 % |
c |      3222 |  336590  1020812 |  222748    2806    36890    13.1 | 15.402 % |
c |      4930 |  332172  1010551 |  245022    4286    53520    12.5 | 16.665 % |
c |      7493 |  331537  1008747 |  269525    6753    80604    11.9 | 16.781 % |
c |     11337 |  329333  1003367 |  296477   10380   136949    13.2 | 17.352 % |
c |     17103 |  325897   994970 |  326125   15861   237967    15.0 | 18.176 % |
c |     25752 |  319233   979463 |  358738   24256   461877    19.0 | 19.979 % |
c |     38727 |  315933   970772 |  394611   36943   815778    22.1 | 20.730 % |
c |     58190 |  313386   964280 |  434073   56128  1483855    26.4 | 21.354 % |
c |     87382 |  310380   956130 |  477480   82886  2503091    30.2 | 21.949 % |
c |    131176 |  309665   954067 |  525228  126503  4504513    35.6 | 22.091 % |
c |    196861 |  308924   951978 |  577751  192043  8076738    42.1 | 22.235 % |

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/24504/stat): 24504 (minisat+_script) R 24503 24504 9854 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1788602511 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 0 0 0
Raw data (/proc/24504/statm): 174 3 169 147 0 27 0
[pid=24504] 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=24505
New process pid=24506
New process pid=24507
execve syscall for /bin/sed executable
One traced child (pid=24506) 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=24507) exited with status: 0
One traced child (pid=24505) exited with status: 0
New process pid=24508
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc11/normalized-mps-v2-20-10-roll3000.opb

[startup+10.0034 s]
Raw data (loadavg): 0.93 0.95 0.90 2/57 24508
Raw data (/proc/24504/stat): 24504 (minisat+_script) S 24503 24504 9854 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788602511 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24504/statm): 531 226 485 147 0 384 0
[pid=24504] vsize: 2124
Raw data (/proc/24508/stat): 24508 (minisat+_64-bit) R 24504 24504 9854 0 -1 0 9945 0 0 0 916 39 0 0 25 0 1 0 1788602516 42856448 9432 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24508/statm): 10463 9432 145 145 0 10318 0
[pid=24508] vsize: 41852
Current children cumulated CPU time (s) 9.56
Current children cumulated vsize (Kb) 43976

[startup+20.0042 s]
Raw data (loadavg): 0.94 0.96 0.91 2/57 24508
Raw data (/proc/24504/stat): 24504 (minisat+_script) S 24503 24504 9854 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788602511 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24504/statm): 531 226 485 147 0 384 0
[pid=24504] vsize: 2124
Raw data (/proc/24508/stat): 24508 (minisat+_64-bit) R 24504 24504 9854 0 -1 0 10029 0 0 0 1913 40 0 0 25 0 1 0 1788602516 43175936 9516 4294967295 134512640 135094434 3221224432 3221223120 134558992 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24508/statm): 10541 9516 145 145 0 10396 0
[pid=24508] vsize: 42164
Current children cumulated CPU time (s) 19.54
Current children cumulated vsize (Kb) 44288

[startup+30.006 s]
Raw data (loadavg): 0.95 0.96 0.91 2/57 24508
Raw data (/proc/24504/stat): 24504 (minisat+_script) S 24503 24504 9854 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788602511 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24504/statm): 531 226 485 147 0 384 0
[pid=24504] vsize: 2124
Raw data (/proc/24508/stat): 24508 (minisat+_64-bit) R 24504 24504 9854 0 -1 0 10065 0 0 0 2911 41 0 0 25 0 1 0 1788602516 43294720 9552 4294967295 134512640 135094434 3221224432 3221223092 134553444 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24508/statm): 10570 9552 145 145 0 10425 0
[pid=24508] vsize: 42280
Current children cumulated CPU time (s) 29.53
Current children cumulated vsize (Kb) 44404

[startup+40.0067 s]
Raw data (loadavg): 0.95 0.96 0.91 2/57 24508
Raw data (/proc/24504/stat): 24504 (minisat+_script) S 24503 24504 9854 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788602511 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24504/statm): 531 226 485 147 0 384 0
[pid=24504] vsize: 2124
Raw data (/proc/24508/stat): 24508 (minisat+_64-bit) R 24504 24504 9854 0 -1 0 10098 0 0 0 3910 42 0 0 25 0 1 0 1788602516 43425792 9585 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24508/statm): 10602 9585 145 145 0 10457 0
[pid=24508] vsize: 42408
Current children cumulated CPU time (s) 39.53
Current children cumulated vsize (Kb) 44532

[startup+50.0085 s]
Raw data (loadavg): 0.96 0.96 0.91 2/57 24508
Raw data (/proc/24504/stat): 24504 (minisat+_script) S 24503 24504 9854 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788602511 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24504/statm): 531 226 485 147 0 384 0
[pid=24504] vsize: 2124
Raw data (/proc/24508/stat): 24508 (minisat+_64-bit) R 24504 24504 9854 0 -1 0 10131 0 0 0 4910 42 0 0 25 0 1 0 1788602516 43585536 9618 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24508/statm): 10641 9618 145 145 0 10496 0
[pid=24508] vsize: 42564
Current children cumulated CPU time (s) 49.53
Current children cumulated vsize (Kb) 44688

[startup+60.0093 s]
Raw data (loadavg): 0.97 0.96 0.91 2/57 24508
Raw data (/proc/24504/stat): 24504 (minisat+_script) S 24503 24504 9854 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788602511 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24504/statm): 531 226 485 147 0 384 0
[pid=24504] vsize: 2124
Raw data (/proc/24508/stat): 24508 (minisat+_64-bit) R 24504 24504 9854 0 -1 0 10189 0 0 0 5909 42 0 0 25 0 1 0 1788602516 43798528 9676 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24508/statm): 10693 9676 145 145 0 10548 0
[pid=24508] vsize: 42772
Current children cumulated CPU time (s) 59.52
Current children cumulated vsize (Kb) 44896

[startup+70.0101 s]
Raw data (loadavg): 0.97 0.96 0.91 2/57 24508
Raw data (/proc/24504/stat): 24504 (minisat+_script) S 24503 24504 9854 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788602511 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24504/statm): 531 226 485 147 0 384 0
[pid=24504] vsize: 2124
Raw data (/proc/24508/stat): 24508 (minisat+_64-bit) R 24504 24504 9854 0 -1 0 10257 0 0 0 6908 42 0 0 25 0 1 0 1788602516 44060672 9744 4294967295 134512640 135094434 3221224432 3221223112 134553433 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24508/statm): 10757 9744 145 145 0 10612 0
[pid=24508] vsize: 43028
Current children cumulated CPU time (s) 69.51
Current children cumulated vsize (Kb) 45152

[startup+80.0109 s]
Raw data (loadavg): 0.98 0.96 0.91 2/57 24508
Raw data (/proc/24504/stat): 24504 (minisat+_script) S 24503 24504 9854 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788602511 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24504/statm): 531 226 485 147 0 384 0
[pid=24504] vsize: 2124
Raw data (/proc/24508/stat): 24508 (minisat+_64-bit) R 24504 24504 9854 0 -1 0 10292 0 0 0 7908 42 0 0 25 0 1 0 1788602516 44199936 9779 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24508/statm): 10791 9779 145 145 0 10646 0
[pid=24508] vsize: 43164
Current children cumulated CPU time (s) 79.51
Current children cumulated vsize (Kb) 45288

[startup+90.0117 s]
Raw data (loadavg): 0.98 0.96 0.91 2/57 24508
Raw data (/proc/24504/stat): 24504 (minisat+_script) S 24503 24504 9854 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788602511 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24504/statm): 531 226 485 147 0 384 0
[pid=24504] vsize: 2124
Raw data (/proc/24508/stat): 24508 (minisat+_64-bit) R 24504 24504 9854 0 -1 0 10332 0 0 0 8908 43 0 0 25 0 1 0 1788602516 44425216 9819 4294967295 134512640 135094434 3221224432 3221223056 134557616 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24508/statm): 10846 9819 145 145 0 10701 0
[pid=24508] vsize: 43384
Current children cumulated CPU time (s) 89.52
Current children cumulated vsize (Kb) 45508

[startup+100.012 s]
Raw data (loadavg): 0.98 0.96 0.91 2/57 24508
Raw data (/proc/24504/stat): 24504 (minisat+_script) S 24503 24504 9854 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788602511 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24504/statm): 531 226 485 147 0 384 0
[pid=24504] vsize: 2124
Raw data (/proc/24508/stat): 24508 (minisat+_64-bit) R 24504 24504 9854 0 -1 0 10395 0 0 0 9907 43 0 0 25 0 1 0 1788602516 44675072 9882 4294967295 134512640 135094434 3221224432 3221223088 134558411 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24508/statm): 10907 9882 145 145 0 10762 0
[pid=24508] vsize: 43628
Current children cumulated CPU time (s) 99.51
Current children cumulated vsize (Kb) 45752

[startup+110.013 s]
Raw data (loadavg): 0.98 0.96 0.91 2/57 24508
Raw data (/proc/24504/stat): 24504 (minisat+_script) S 24503 24504 9854 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788602511 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24504/statm): 531 226 485 147 0 384 0
[pid=24504] vsize: 2124
Raw data (/proc/24508/stat): 24508 (minisat+_64-bit) R 24504 24504 9854 0 -1 0 10496 0 0 0 10906 44 0 0 25 0 1 0 1788602516 45047808 9983 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24508/statm): 10998 9983 145 145 0 10853 0
[pid=24508] vsize: 43992
Current children cumulated CPU time (s) 109.51
Current children cumulated vsize (Kb) 46116

[startup+120.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24508
Raw data (/proc/24504/stat): 24504 (minisat+_script) S 24503 24504 9854 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788602511 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24504/statm): 531 226 485 147 0 384 0
[pid=24504] vsize: 2124
Raw data (/proc/24508/stat): 24508 (minisat+_64-bit) R 24504 24504 9854 0 -1 0 10557 0 0 0 11905 44 0 0 25 0 1 0 1788602516 45293568 10044 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24508/statm): 11058 10044 145 145 0 10913 0
[pid=24508] vsize: 44232
Current children cumulated CPU time (s) 119.5
Current children cumulated vsize (Kb) 46356

[startup+130.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24508
Raw data (/proc/24504/stat): 24504 (minisat+_script) S 24503 24504 9854 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788602511 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24504/statm): 531 226 485 147 0 384 0
[pid=24504] vsize: 2124
Raw data (/proc/24508/stat): 24508 (minisat+_64-bit) R 24504 24504 9854 0 -1 0 10623 0 0 0 12904 45 0 0 25 0 1 0 1788602516 45555712 10110 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24508/statm): 11122 10110 145 145 0 10977 0
[pid=24508] vsize: 44488
Current children cumulated CPU time (s) 129.5
Current children cumulated vsize (Kb) 46612

[startup+140.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24508
Raw data (/proc/24504/stat): 24504 (minisat+_script) S 24503 24504 9854 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788602511 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24504/statm): 531 226 485 147 0 384 0
[pid=24504] vsize: 2124
Raw data (/proc/24508/stat): 24508 (minisat+_64-bit) R 24504 24504 9854 0 -1 0 10679 0 0 0 13903 45 0 0 24 0 1 0 1788602516 45780992 10166 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24508/statm): 11177 10166 145 145 0 11032 0
[pid=24508] vsize: 44708
Current children cumulated CPU time (s) 139.49
Current children cumulated vsize (Kb) 46832

[startup+150.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24508
Raw data (/proc/24504/stat): 24504 (minisat+_script) S 24503 24504 9854 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788602511 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24504/statm): 531 226 485 147 0 384 0
[pid=24504] vsize: 2124
Raw data (/proc/24508/stat): 24508 (minisat+_64-bit) R 24504 24504 9854 0 -1 0 10770 0 0 0 14902 46 0 0 25 0 1 0 1788602516 46145536 10257 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24508/statm): 11266 10257 145 145 0 11121 0
[pid=24508] vsize: 45064
Current children cumulated CPU time (s) 149.49
Current children cumulated vsize (Kb) 47188

[startup+160.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24508
Raw data (/proc/24504/stat): 24504 (minisat+_script) S 24503 24504 9854 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788602511 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24504/statm): 531 226 485 147 0 384 0
[pid=24504] vsize: 2124
Raw data (/proc/24508/stat): 24508 (minisat+_64-bit) R 24504 24504 9854 0 -1 0 10818 0 0 0 15901 46 0 0 25 0 1 0 1788602516 46333952 10305 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24508/statm): 11312 10305 145 145 0 11167 0
[pid=24508] vsize: 45248
Current children cumulated CPU time (s) 159.48
Current children cumulated vsize (Kb) 47372

[startup+170.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24508
Raw data (/proc/24504/stat): 24504 (minisat+_script) S 24503 24504 9854 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788602511 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24504/statm): 531 226 485 147 0 384 0
[pid=24504] vsize: 2124
Raw data (/proc/24508/stat): 24508 (minisat+_64-bit) R 24504 24504 9854 0 -1 0 10908 0 0 0 16899 47 0 0 25 0 1 0 1788602516 46686208 10395 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24508/statm): 11398 10395 145 145 0 11253 0
[pid=24508] vsize: 45592
Current children cumulated CPU time (s) 169.47
Current children cumulated vsize (Kb) 47716

[startup+180.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24508
Raw data (/proc/24504/stat): 24504 (minisat+_script) S 24503 24504 9854 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788602511 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24504/statm): 531 226 485 147 0 384 0
[pid=24504] vsize: 2124
Raw data (/proc/24508/stat): 24508 (minisat+_64-bit) R 24504 24504 9854 0 -1 0 10981 0 0 0 17899 47 0 0 25 0 1 0 1788602516 47108096 10468 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24508/statm): 11501 10468 145 145 0 11356 0
[pid=24508] vsize: 46004
Current children cumulated CPU time (s) 179.47
Current children cumulated vsize (Kb) 48128

[startup+190.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24508
Raw data (/proc/24504/stat): 24504 (minisat+_script) S 24503 24504 9854 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788602511 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24504/statm): 531 226 485 147 0 384 0
[pid=24504] vsize: 2124
Raw data (/proc/24508/stat): 24508 (minisat+_64-bit) R 24504 24504 9854 0 -1 0 11048 0 0 0 18897 48 0 0 25 0 1 0 1788602516 47374336 10535 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24508/statm): 11566 10535 145 145 0 11421 0
[pid=24508] vsize: 46264
Current children cumulated CPU time (s) 189.46
Current children cumulated vsize (Kb) 48388

[startup+200.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24508
Raw data (/proc/24504/stat): 24504 (minisat+_script) S 24503 24504 9854 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788602511 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24504/statm): 531 226 485 147 0 384 0
[pid=24504] vsize: 2124
Raw data (/proc/24508/stat): 24508 (minisat+_64-bit) R 24504 24504 9854 0 -1 0 11121 0 0 0 19897 48 0 0 25 0 1 0 1788602516 47665152 10608 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24508/statm): 11637 10608 145 145 0 11492 0
[pid=24508] vsize: 46548
Current children cumulated CPU time (s) 199.46
Current children cumulated vsize (Kb) 48672

[startup+210.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24508
Raw data (/proc/24504/stat): 24504 (minisat+_script) S 24503 24504 9854 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788602511 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24504/statm): 531 226 485 147 0 384 0
[pid=24504] vsize: 2124
Raw data (/proc/24508/stat): 24508 (minisat+_64-bit) R 24504 24504 9854 0 -1 0 11187 0 0 0 20896 48 0 0 25 0 1 0 1788602516 47927296 10674 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24508/statm): 11701 10674 145 145 0 11556 0
[pid=24508] vsize: 46804
Current children cumulated CPU time (s) 209.45
Current children cumulated vsize (Kb) 48928

[startup+220.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24508
Raw data (/proc/24504/stat): 24504 (minisat+_script) S 24503 24504 9854 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788602511 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24504/statm): 531 226 485 147 0 384 0
[pid=24504] vsize: 2124
Raw data (/proc/24508/stat): 24508 (minisat+_64-bit) R 24504 24504 9854 0 -1 0 11300 0 0 0 21895 49 0 0 25 0 1 0 1788602516 48386048 10787 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24508/statm): 11813 10787 145 145 0 11668 0
[pid=24508] vsize: 47252
Current children cumulated CPU time (s) 219.45
Current children cumulated vsize (Kb) 49376

[startup+230.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24508
Raw data (/proc/24504/stat): 24504 (minisat+_script) S 24503 24504 9854 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788602511 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24504/statm): 531 226 485 147 0 384 0
[pid=24504] vsize: 2124
Raw data (/proc/24508/stat): 24508 (minisat+_64-bit) R 24504 24504 9854 0 -1 0 11361 0 0 0 22894 49 0 0 25 0 1 0 1788602516 48627712 10848 4294967295 134512640 135094434 3221224432 3221223124 134558984 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24508/statm): 11872 10848 145 145 0 11727 0
[pid=24508] vsize: 47488
Current children cumulated CPU time (s) 229.44
Current children cumulated vsize (Kb) 49612

[startup+240.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24508
Raw data (/proc/24504/stat): 24504 (minisat+_script) S 24503 24504 9854 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788602511 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24504/statm): 531 226 485 147 0 384 0
[pid=24504] vsize: 2124
Raw data (/proc/24508/stat): 24508 (minisat+_64-bit) R 24504 24504 9854 0 -1 0 11419 0 0 0 23893 50 0 0 25 0 1 0 1788602516 48861184 10906 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24508/statm): 11929 10906 145 145 0 11784 0
[pid=24508] vsize: 47716
Current children cumulated CPU time (s) 239.44
Current children cumulated vsize (Kb) 49840

[startup+250.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24508
Raw data (/proc/24504/stat): 24504 (minisat+_script) S 24503 24504 9854 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788602511 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24504/statm): 531 226 485 147 0 384 0
[pid=24504] vsize: 2124
Raw data (/proc/24508/stat): 24508 (minisat+_64-bit) R 24504 24504 9854 0 -1 0 11477 0 0 0 24893 50 0 0 25 0 1 0 1788602516 49090560 10964 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24508/statm): 11985 10964 145 145 0 11840 0
[pid=24508] vsize: 47940
Current children cumulated CPU time (s) 249.44
Current children cumulated vsize (Kb) 50064

[startup+260.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24508
Raw data (/proc/24504/stat): 24504 (minisat+_script) S 24503 24504 9854 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788602511 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24504/statm): 531 226 485 147 0 384 0
[pid=24504] vsize: 2124
Raw data (/proc/24508/stat): 24508 (minisat+_64-bit) R 24504 24504 9854 0 -1 0 11569 0 0 0 25891 50 0 0 25 0 1 0 1788602516 49459200 11056 4294967295 134512640 135094434 3221224432 3221223044 134563046 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24508/statm): 12075 11056 145 145 0 11930 0
[pid=24508] vsize: 48300
Current children cumulated CPU time (s) 259.42
Current children cumulated vsize (Kb) 50424

[startup+270.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24508
Raw data (/proc/24504/stat): 24504 (minisat+_script) S 24503 24504 9854 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788602511 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24504/statm): 531 226 485 147 0 384 0
[pid=24504] vsize: 2124
Raw data (/proc/24508/stat): 24508 (minisat+_64-bit) R 24504 24504 9854 0 -1 0 11631 0 0 0 26890 51 0 0 25 0 1 0 1788602516 49709056 11118 4294967295 134512640 135094434 3221224432 3221223088 134558013 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24508/statm): 12136 11118 145 145 0 11991 0
[pid=24508] vsize: 48544
Current children cumulated CPU time (s) 269.42
Current children cumulated vsize (Kb) 50668

[startup+280.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24508
Raw data (/proc/24504/stat): 24504 (minisat+_script) S 24503 24504 9854 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788602511 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24504/statm): 531 226 485 147 0 384 0
[pid=24504] vsize: 2124
Raw data (/proc/24508/stat): 24508 (minisat+_64-bit) R 24504 24504 9854 0 -1 0 11717 0 0 0 27890 51 0 0 25 0 1 0 1788602516 50061312 11204 4294967295 134512640 135094434 3221224432 3221223064 134557561 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24508/statm): 12222 11204 145 145 0 12077 0
[pid=24508] vsize: 48888
Current children cumulated CPU time (s) 279.42
Current children cumulated vsize (Kb) 51012

[startup+290.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24508
Raw data (/proc/24504/stat): 24504 (minisat+_script) S 24503 24504 9854 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788602511 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24504/statm): 531 226 485 147 0 384 0
[pid=24504] vsize: 2124
Raw data (/proc/24508/stat): 24508 (minisat+_64-bit) R 24504 24504 9854 0 -1 0 11802 0 0 0 28888 52 0 0 25 0 1 0 1788602516 50393088 11289 4294967295 134512640 135094434 3221224432 3221223092 134553536 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24508/statm): 12303 11289 145 145 0 12158 0
[pid=24508] vsize: 49212
Current children cumulated CPU time (s) 289.41
Current children cumulated vsize (Kb) 51336

[startup+300.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24508
Raw data (/proc/24504/stat): 24504 (minisat+_script) S 24503 24504 9854 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788602511 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24504/statm): 531 226 485 147 0 384 0
[pid=24504] vsize: 2124
Raw data (/proc/24508/stat): 24508 (minisat+_64-bit) R 24504 24504 9854 0 -1 0 11902 0 0 0 29886 53 0 0 25 0 1 0 1788602516 50794496 11389 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24508/statm): 12401 11389 145 145 0 12256 0
[pid=24508] vsize: 49604
Current children cumulated CPU time (s) 299.4
Current children cumulated vsize (Kb) 51728

[startup+310.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24508
Raw data (/proc/24504/stat): 24504 (minisat+_script) S 24503 24504 9854 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788602511 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24504/statm): 531 226 485 147 0 384 0
[pid=24504] vsize: 2124
Raw data (/proc/24508/stat): 24508 (minisat+_64-bit) R 24504 24504 9854 0 -1 0 11969 0 0 0 30885 54 0 0 25 0 1 0 1788602516 51060736 11456 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24508/statm): 12466 11456 145 145 0 12321 0
[pid=24508] vsize: 49864
Current children cumulated CPU time (s) 309.4
Current children cumulated vsize (Kb) 51988

[startup+320.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24508
Raw data (/proc/24504/stat): 24504 (minisat+_script) S 24503 24504 9854 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788602511 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24504/statm): 531 226 485 147 0 384 0
[pid=24504] vsize: 2124
Raw data (/proc/24508/stat): 24508 (minisat+_64-bit) R 24504 24504 9854 0 -1 0 12076 0 0 0 31883 55 0 0 25 0 1 0 1788602516 51490816 11563 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24508/statm): 12571 11563 145 145 0 12426 0
[pid=24508] vsize: 50284
Current children cumulated CPU time (s) 319.39
Current children cumulated vsize (Kb) 52408

[startup+330.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24508
Raw data (/proc/24504/stat): 24504 (minisat+_script) S 24503 24504 9854 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788602511 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24504/statm): 531 226 485 147 0 384 0
[pid=24504] vsize: 2124
Raw data (/proc/24508/stat): 24508 (minisat+_64-bit) R 24504 24504 9854 0 -1 0 12168 0 0 0 32881 55 0 0 25 0 1 0 1788602516 51863552 11655 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24508/statm): 12662 11655 145 145 0 12517 0
[pid=24508] vsize: 50648
Current children cumulated CPU time (s) 329.37
Current children cumulated vsize (Kb) 52772

[startup+340.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24508
Raw data (/proc/24504/stat): 24504 (minisat+_script) S 24503 24504 9854 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788602511 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24504/statm): 531 226 485 147 0 384 0
[pid=24504] vsize: 2124
Raw data (/proc/24508/stat): 24508 (minisat+_64-bit) R 24504 24504 9854 0 -1 0 12221 0 0 0 33880 56 0 0 25 0 1 0 1788602516 52080640 11708 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24508/statm): 12715 11708 145 145 0 12570 0
[pid=24508] vsize: 50860
Current children cumulated CPU time (s) 339.37
Current children cumulated vsize (Kb) 52984

[startup+350.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24508
Raw data (/proc/24504/stat): 24504 (minisat+_script) S 24503 24504 9854 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788602511 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24504/statm): 531 226 485 147 0 384 0
[pid=24504] vsize: 2124
Raw data (/proc/24508/stat): 24508 (minisat+_64-bit) R 24504 24504 9854 0 -1 0 12292 0 0 0 34879 56 0 0 25 0 1 0 1788602516 52363264 11779 4294967295 134512640 135094434 3221224432 3221223120 134554750 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24508/statm): 12784 11779 145 145 0 12639 0
[pid=24508] vsize: 51136
Current children cumulated CPU time (s) 349.36
Current children cumulated vsize (Kb) 53260

[startup+360.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24508
Raw data (/proc/24504/stat): 24504 (minisat+_script) S 24503 24504 9854 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788602511 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24504/statm): 531 226 485 147 0 384 0
[pid=24504] vsize: 2124
Raw data (/proc/24508/stat): 24508 (minisat+_64-bit) R 24504 24504 9854 0 -1 0 12347 0 0 0 35878 57 0 0 25 0 1 0 1788602516 52846592 11834 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24508/statm): 12902 11834 145 145 0 12757 0
[pid=24508] vsize: 51608
Current children cumulated CPU time (s) 359.36
Current children cumulated vsize (Kb) 53732

[startup+370.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24508
Raw data (/proc/24504/stat): 24504 (minisat+_script) S 24503 24504 9854 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788602511 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24504/statm): 531 226 485 147 0 384 0
[pid=24504] vsize: 2124
Raw data (/proc/24508/stat): 24508 (minisat+_64-bit) R 24504 24504 9854 0 -1 0 12385 0 0 0 36877 57 0 0 25 0 1 0 1788602516 52998144 11872 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24508/statm): 12939 11872 145 145 0 12794 0
[pid=24508] vsize: 51756
Current children cumulated CPU time (s) 369.35
Current children cumulated vsize (Kb) 53880

[startup+380.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24508
Raw data (/proc/24504/stat): 24504 (minisat+_script) S 24503 24504 9854 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788602511 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24504/statm): 531 226 485 147 0 384 0
[pid=24504] vsize: 2124
Raw data (/proc/24508/stat): 24508 (minisat+_64-bit) R 24504 24504 9854 0 -1 0 12460 0 0 0 37876 58 0 0 25 0 1 0 1788602516 53297152 11947 4294967295 134512640 135094434 3221224432 3221223088 134558123 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24508/statm): 13012 11947 145 145 0 12867 0
[pid=24508] vsize: 52048
Current children cumulated CPU time (s) 379.35
Current children cumulated vsize (Kb) 54172

[startup+390.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24508
Raw data (/proc/24504/stat): 24504 (minisat+_script) S 24503 24504 9854 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788602511 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24504/statm): 531 226 485 147 0 384 0
[pid=24504] vsize: 2124
Raw data (/proc/24508/stat): 24508 (minisat+_64-bit) R 24504 24504 9854 0 -1 0 12507 0 0 0 38875 59 0 0 25 0 1 0 1788602516 53485568 11994 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24508/statm): 13058 11994 145 145 0 12913 0
[pid=24508] vsize: 52232
Current children cumulated CPU time (s) 389.35
Current children cumulated vsize (Kb) 54356

[startup+400.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24508
Raw data (/proc/24504/stat): 24504 (minisat+_script) S 24503 24504 9854 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788602511 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24504/statm): 531 226 485 147 0 384 0
[pid=24504] vsize: 2124
Raw data (/proc/24508/stat): 24508 (minisat+_64-bit) R 24504 24504 9854 0 -1 0 12592 0 0 0 39873 60 0 0 25 0 1 0 1788602516 53825536 12079 4294967295 134512640 135094434 3221224432 3221223088 134557875 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24508/statm): 13141 12079 145 145 0 12996 0
[pid=24508] vsize: 52564
Current children cumulated CPU time (s) 399.34
Current children cumulated vsize (Kb) 54688

[startup+410.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24508
Raw data (/proc/24504/stat): 24504 (minisat+_script) S 24503 24504 9854 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788602511 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24504/statm): 531 226 485 147 0 384 0
[pid=24504] vsize: 2124
Raw data (/proc/24508/stat): 24508 (minisat+_64-bit) R 24504 24504 9854 0 -1 0 12728 0 0 0 40871 61 0 0 25 0 1 0 1788602516 54378496 12215 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24508/statm): 13276 12215 145 145 0 13131 0
[pid=24508] vsize: 53104
Current children cumulated CPU time (s) 409.33
Current children cumulated vsize (Kb) 55228

[startup+420.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24508
Raw data (/proc/24504/stat): 24504 (minisat+_script) S 24503 24504 9854 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788602511 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24504/statm): 531 226 485 147 0 384 0
[pid=24504] vsize: 2124
Raw data (/proc/24508/stat): 24508 (minisat+_64-bit) R 24504 24504 9854 0 -1 0 12796 0 0 0 41871 61 0 0 25 0 1 0 1788602516 54648832 12283 4294967295 134512640 135094434 3221224432 3221223104 134555574 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24508/statm): 13342 12283 145 145 0 13197 0
[pid=24508] vsize: 53368
Current children cumulated CPU time (s) 419.33
Current children cumulated vsize (Kb) 55492

[startup+430.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24508
Raw data (/proc/24504/stat): 24504 (minisat+_script) S 24503 24504 9854 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788602511 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24504/statm): 531 226 485 147 0 384 0
[pid=24504] vsize: 2124
Raw data (/proc/24508/stat): 24508 (minisat+_64-bit) R 24504 24504 9854 0 -1 0 12889 0 0 0 42870 62 0 0 25 0 1 0 1788602516 55025664 12376 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24508/statm): 13434 12376 145 145 0 13289 0
[pid=24508] vsize: 53736
Current children cumulated CPU time (s) 429.33
Current children cumulated vsize (Kb) 55860

[startup+440.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24508
Raw data (/proc/24504/stat): 24504 (minisat+_script) S 24503 24504 9854 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788602511 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24504/statm): 531 226 485 147 0 384 0
[pid=24504] vsize: 2124
Raw data (/proc/24508/stat): 24508 (minisat+_64-bit) R 24504 24504 9854 0 -1 0 12919 0 0 0 43870 62 0 0 25 0 1 0 1788602516 55144448 12406 4294967295 134512640 135094434 3221224432 3221223088 134557832 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24508/statm): 13463 12406 145 145 0 13318 0
[pid=24508] vsize: 53852
Current children cumulated CPU time (s) 439.33
Current children cumulated vsize (Kb) 55976

[startup+450.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24508
Raw data (/proc/24504/stat): 24504 (minisat+_script) S 24503 24504 9854 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788602511 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24504/statm): 531 226 485 147 0 384 0
[pid=24504] vsize: 2124
Raw data (/proc/24508/stat): 24508 (minisat+_64-bit) R 24504 24504 9854 0 -1 0 12983 0 0 0 44869 62 0 0 25 0 1 0 1788602516 55402496 12470 4294967295 134512640 135094434 3221224432 3221223056 134557717 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24508/statm): 13526 12470 145 145 0 13381 0
[pid=24508] vsize: 54104
Current children cumulated CPU time (s) 449.32
Current children cumulated vsize (Kb) 56228

[startup+460.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24508
Raw data (/proc/24504/stat): 24504 (minisat+_script) S 24503 24504 9854 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788602511 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24504/statm): 531 226 485 147 0 384 0
[pid=24504] vsize: 2124
Raw data (/proc/24508/stat): 24508 (minisat+_64-bit) R 24504 24504 9854 0 -1 0 13138 0 0 0 45865 64 0 0 25 0 1 0 1788602516 56029184 12625 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24508/statm): 13679 12625 145 145 0 13534 0
[pid=24508] vsize: 54716
Current children cumulated CPU time (s) 459.3
Current children cumulated vsize (Kb) 56840

[startup+470.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24508
Raw data (/proc/24504/stat): 24504 (minisat+_script) S 24503 24504 9854 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788602511 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24504/statm): 531 226 485 147 0 384 0
[pid=24504] vsize: 2124
Raw data (/proc/24508/stat): 24508 (minisat+_64-bit) R 24504 24504 9854 0 -1 0 13245 0 0 0 46863 65 0 0 25 0 1 0 1788602516 56455168 12732 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24508/statm): 13783 12732 145 145 0 13638 0
[pid=24508] vsize: 55132
Current children cumulated CPU time (s) 469.29
Current children cumulated vsize (Kb) 57256

[startup+480.046 s]
Raw data (loadavg): 0.99 0.97 0.91 1/57 24508
Raw data (/proc/24504/stat): 24504 (minisat+_script) S 24503 24504 9854 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788602511 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24504/statm): 531 226 485 147 0 384 0
[pid=24504] vsize: 2124
Raw data (/proc/24508/stat): 24508 (minisat+_64-bit) T 24504 24504 9854 0 -1 0 13327 0 0 0 47862 65 0 0 25 0 1 0 1788602516 56782848 12814 4294967295 134512640 135094434 3221224432 3221222796 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/24508/statm): 13863 12814 145 145 0 13718 0
[pid=24508] vsize: 55452
Current children cumulated CPU time (s) 479.28
Current children cumulated vsize (Kb) 57576

[startup+490.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24508
Raw data (/proc/24504/stat): 24504 (minisat+_script) S 24503 24504 9854 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788602511 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24504/statm): 531 226 485 147 0 384 0
[pid=24504] vsize: 2124
Raw data (/proc/24508/stat): 24508 (minisat+_64-bit) R 24504 24504 9854 0 -1 0 13422 0 0 0 48860 66 0 0 25 0 1 0 1788602516 57163776 12909 4294967295 134512640 135094434 3221224432 3221223024 134557219 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24508/statm): 13956 12909 145 145 0 13811 0
[pid=24508] vsize: 55824
Current children cumulated CPU time (s) 489.27
Current children cumulated vsize (Kb) 57948

[startup+500.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24508
Raw data (/proc/24504/stat): 24504 (minisat+_script) S 24503 24504 9854 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788602511 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24504/statm): 531 226 485 147 0 384 0
[pid=24504] vsize: 2124
Raw data (/proc/24508/stat): 24508 (minisat+_64-bit) R 24504 24504 9854 0 -1 0 13494 0 0 0 49859 66 0 0 25 0 1 0 1788602516 57454592 12981 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24508/statm): 14027 12981 145 145 0 13882 0
[pid=24508] vsize: 56108
Current children cumulated CPU time (s) 499.26
Current children cumulated vsize (Kb) 58232

[startup+510.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24508
Raw data (/proc/24504/stat): 24504 (minisat+_script) S 24503 24504 9854 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788602511 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24504/statm): 531 226 485 147 0 384 0
[pid=24504] vsize: 2124
Raw data (/proc/24508/stat): 24508 (minisat+_64-bit) R 24504 24504 9854 0 -1 0 13583 0 0 0 50859 67 0 0 25 0 1 0 1788602516 57806848 13070 4294967295 134512640 135094434 3221224432 3221223088 134557813 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24508/statm): 14113 13070 145 145 0 13968 0
[pid=24508] vsize: 56452
Current children cumulated CPU time (s) 509.27
Current children cumulated vsize (Kb) 58576

[startup+520.051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24508
Raw data (/proc/24504/stat): 24504 (minisat+_script) S 24503 24504 9854 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788602511 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24504/statm): 531 226 485 147 0 384 0
[pid=24504] vsize: 2124
Raw data (/proc/24508/stat): 24508 (minisat+_64-bit) R 24504 24504 9854 0 -1 0 13722 0 0 0 51857 68 0 0 25 0 1 0 1788602516 58372096 13209 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24508/statm): 14251 13209 145 145 0 14106 0
[pid=24508] vsize: 57004
Current children cumulated CPU time (s) 519.26
Current children cumulated vsize (Kb) 59128

[startup+530.052 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24508
Raw data (/proc/24504/stat): 24504 (minisat+_script) S 24503 24504 9854 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788602511 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24504/statm): 531 226 485 147 0 384 0
[pid=24504] vsize: 2124
Raw data (/proc/24508/stat): 24508 (minisat+_64-bit) R 24504 24504 9854 0 -1 0 13814 0 0 0 52856 68 0 0 25 0 1 0 1788602516 58740736 13301 4294967295 134512640 135094434 3221224432 3221223024 134557230 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24508/statm): 14341 13301 145 145 0 14196 0
[pid=24508] vsize: 57364
Current children cumulated CPU time (s) 529.25
Current children cumulated vsize (Kb) 59488

[startup+540.053 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24508
Raw data (/proc/24504/stat): 24504 (minisat+_script) S 24503 24504 9854 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788602511 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24504/statm): 531 226 485 147 0 384 0
[pid=24504] vsize: 2124
Raw data (/proc/24508/stat): 24508 (minisat+_64-bit) R 24504 24504 9854 0 -1 0 13943 0 0 0 53854 69 0 0 25 0 1 0 1788602516 59260928 13430 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24508/statm): 14468 13430 145 145 0 14323 0
[pid=24508] vsize: 57872
Current children cumulated CPU time (s) 539.24
Current children cumulated vsize (Kb) 59996

[startup+550.055 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24508
Raw data (/proc/24504/stat): 24504 (minisat+_script) S 24503 24504 9854 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788602511 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24504/statm): 531 226 485 147 0 384 0
[pid=24504] vsize: 2124
Raw data (/proc/24508/stat): 24508 (minisat+_64-bit) R 24504 24504 9854 0 -1 0 14008 0 0 0 54854 69 0 0 25 0 1 0 1788602516 59510784 13495 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24508/statm): 14529 13495 145 145 0 14384 0
[pid=24508] vsize: 58116
Current children cumulated CPU time (s) 549.24
Current children cumulated vsize (Kb) 60240

[startup+560.056 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24508
Raw data (/proc/24504/stat): 24504 (minisat+_script) S 24503 24504 9854 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788602511 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24504/statm): 531 226 485 147 0 384 0
[pid=24504] vsize: 2124
Raw data (/proc/24508/stat): 24508 (minisat+_64-bit) R 24504 24504 9854 0 -1 0 14071 0 0 0 55853 70 0 0 25 0 1 0 1788602516 59764736 13558 4294967295 134512640 135094434 3221224432 3221223088 134558402 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24508/statm): 14591 13558 145 145 0 14446 0
[pid=24508] vsize: 58364
Current children cumulated CPU time (s) 559.24
Current children cumulated vsize (Kb) 60488

[startup+570.057 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24508
Raw data (/proc/24504/stat): 24504 (minisat+_script) S 24503 24504 9854 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788602511 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24504/statm): 531 226 485 147 0 384 0
[pid=24504] vsize: 2124
Raw data (/proc/24508/stat): 24508 (minisat+_64-bit) R 24504 24504 9854 0 -1 0 14205 0 0 0 56851 70 0 0 25 0 1 0 1788602516 60313600 13692 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24508/statm): 14725 13692 145 145 0 14580 0
[pid=24508] vsize: 58900
Current children cumulated CPU time (s) 569.22
Current children cumulated vsize (Kb) 61024

[startup+580.058 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24508
Raw data (/proc/24504/stat): 24504 (minisat+_script) S 24503 24504 9854 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788602511 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24504/statm): 531 226 485 147 0 384 0
[pid=24504] vsize: 2124
Raw data (/proc/24508/stat): 24508 (minisat+_64-bit) R 24504 24504 9854 0 -1 0 14241 0 0 0 57851 71 0 0 25 0 1 0 1788602516 60456960 13728 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24508/statm): 14760 13728 145 145 0 14615 0
[pid=24508] vsize: 59040
Current children cumulated CPU time (s) 579.23
Current children cumulated vsize (Kb) 61164

[startup+590.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24508
Raw data (/proc/24504/stat): 24504 (minisat+_script) S 24503 24504 9854 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788602511 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24504/statm): 531 226 485 147 0 384 0
[pid=24504] vsize: 2124
Raw data (/proc/24508/stat): 24508 (minisat+_64-bit) R 24504 24504 9854 0 -1 0 14274 0 0 0 58850 71 0 0 25 0 1 0 1788602516 60604416 13761 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24508/statm): 14796 13761 145 145 0 14651 0
[pid=24508] vsize: 59184
Current children cumulated CPU time (s) 589.22
Current children cumulated vsize (Kb) 61308

[startup+600.062 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24508
Raw data (/proc/24504/stat): 24504 (minisat+_script) S 24503 24504 9854 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788602511 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24504/statm): 531 226 485 147 0 384 0
[pid=24504] vsize: 2124
Raw data (/proc/24508/stat): 24508 (minisat+_64-bit) R 24504 24504 9854 0 -1 0 14369 0 0 0 59849 71 0 0 25 0 1 0 1788602516 60981248 13856 4294967295 134512640 135094434 3221224432 3221223104 134556317 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24508/statm): 14888 13856 145 145 0 14743 0
[pid=24508] vsize: 59552
Current children cumulated CPU time (s) 599.21
Current children cumulated vsize (Kb) 61676

[startup+610.063 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24508
Raw data (/proc/24504/stat): 24504 (minisat+_script) S 24503 24504 9854 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788602511 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24504/statm): 531 226 485 147 0 384 0
[pid=24504] vsize: 2124
Raw data (/proc/24508/stat): 24508 (minisat+_64-bit) R 24504 24504 9854 0 -1 0 14474 0 0 0 60848 72 0 0 25 0 1 0 1788602516 61415424 13961 4294967295 134512640 135094434 3221224432 3221222976 134562104 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24508/statm): 14994 13961 145 145 0 14849 0
[pid=24508] vsize: 59976
Current children cumulated CPU time (s) 609.21
Current children cumulated vsize (Kb) 62100

[startup+620.062 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24508
Raw data (/proc/24504/stat): 24504 (minisat+_script) S 24503 24504 9854 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788602511 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24504/statm): 531 226 485 147 0 384 0
[pid=24504] vsize: 2124
Raw data (/proc/24508/stat): 24508 (minisat+_64-bit) R 24504 24504 9854 0 -1 0 14585 0 0 0 61846 72 0 0 25 0 1 0 1788602516 61861888 14072 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24508/statm): 15103 14072 145 145 0 14958 0
[pid=24508] vsize: 60412
Current children cumulated CPU time (s) 619.19
Current children cumulated vsize (Kb) 62536

[startup+630.063 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24508
Raw data (/proc/24504/stat): 24504 (minisat+_script) S 24503 24504 9854 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788602511 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24504/statm): 531 226 485 147 0 384 0
[pid=24504] vsize: 2124
Raw data (/proc/24508/stat): 24508 (minisat+_64-bit) R 24504 24504 9854 0 -1 0 14700 0 0 0 62844 73 0 0 25 0 1 0 1788602516 62324736 14187 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24508/statm): 15216 14187 145 145 0 15071 0
[pid=24508] vsize: 60864
Current children cumulated CPU time (s) 629.18
Current children cumulated vsize (Kb) 62988

[startup+640.064 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24508
Raw data (/proc/24504/stat): 24504 (minisat+_script) S 24503 24504 9854 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788602511 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24504/statm): 531 226 485 147 0 384 0
[pid=24504] vsize: 2124
Raw data (/proc/24508/stat): 24508 (minisat+_64-bit) R 24504 24504 9854 0 -1 0 14789 0 0 0 63842 74 0 0 25 0 1 0 1788602516 62681088 14276 4294967295 134512640 135094434 3221224432 3221223088 134557882 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24508/statm): 15303 14276 145 145 0 15158 0
[pid=24508] vsize: 61212
Current children cumulated CPU time (s) 639.17
Current children cumulated vsize (Kb) 63336

[startup+650.065 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24508
Raw data (/proc/24504/stat): 24504 (minisat+_script) S 24503 24504 9854 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788602511 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24504/statm): 531 226 485 147 0 384 0
[pid=24504] vsize: 2124
Raw data (/proc/24508/stat): 24508 (minisat+_64-bit) R 24504 24504 9854 0 -1 0 14857 0 0 0 64842 75 0 0 25 0 1 0 1788602516 62955520 14344 4294967295 134512640 135094434 3221224432 3221223088 134558007 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24508/statm): 15370 14344 145 145 0 15225 0
[pid=24508] vsize: 61480
Current children cumulated CPU time (s) 649.18
Current children cumulated vsize (Kb) 63604

[startup+660.066 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24508
Raw data (/proc/24504/stat): 24504 (minisat+_script) S 24503 24504 9854 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788602511 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24504/statm): 531 226 485 147 0 384 0
[pid=24504] vsize: 2124
Raw data (/proc/24508/stat): 24508 (minisat+_64-bit) R 24504 24504 9854 0 -1 0 14951 0 0 0 65841 76 0 0 25 0 1 0 1788602516 63340544 14438 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24508/statm): 15464 14438 145 145 0 15319 0
[pid=24508] vsize: 61856
Current children cumulated CPU time (s) 659.18
Current children cumulated vsize (Kb) 63980

[startup+670.066 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24508
Raw data (/proc/24504/stat): 24504 (minisat+_script) S 24503 24504 9854 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788602511 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24504/statm): 531 226 485 147 0 384 0
[pid=24504] vsize: 2124
Raw data (/proc/24508/stat): 24508 (minisat+_64-bit) R 24504 24504 9854 0 -1 0 15040 0 0 0 66839 76 0 0 25 0 1 0 1788602516 63700992 14527 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24508/statm): 15552 14527 145 145 0 15407 0
[pid=24508] vsize: 62208
Current children cumulated CPU time (s) 669.16
Current children cumulated vsize (Kb) 64332

[startup+680.067 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24508
Raw data (/proc/24504/stat): 24504 (minisat+_script) S 24503 24504 9854 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788602511 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24504/statm): 531 226 485 147 0 384 0
[pid=24504] vsize: 2124
Raw data (/proc/24508/stat): 24508 (minisat+_64-bit) R 24504 24504 9854 0 -1 0 15148 0 0 0 67837 77 0 0 25 0 1 0 1788602516 64139264 14635 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24508/statm): 15659 14635 145 145 0 15514 0
[pid=24508] vsize: 62636
Current children cumulated CPU time (s) 679.15
Current children cumulated vsize (Kb) 64760

[startup+690.068 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24508
Raw data (/proc/24504/stat): 24504 (minisat+_script) S 24503 24504 9854 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788602511 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24504/statm): 531 226 485 147 0 384 0
[pid=24504] vsize: 2124
Raw data (/proc/24508/stat): 24508 (minisat+_64-bit) R 24504 24504 9854 0 -1 0 15264 0 0 0 68836 78 0 0 25 0 1 0 1788602516 64614400 14751 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24508/statm): 15775 14751 145 145 0 15630 0
[pid=24508] vsize: 63100
Current children cumulated CPU time (s) 689.15
Current children cumulated vsize (Kb) 65224

[startup+700.069 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24508
Raw data (/proc/24504/stat): 24504 (minisat+_script) S 24503 24504 9854 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788602511 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24504/statm): 531 226 485 147 0 384 0
[pid=24504] vsize: 2124
Raw data (/proc/24508/stat): 24508 (minisat+_64-bit) R 24504 24504 9854 0 -1 0 15367 0 0 0 69834 79 0 0 25 0 1 0 1788602516 65032192 14854 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24508/statm): 15877 14854 145 145 0 15732 0
[pid=24508] vsize: 63508
Current children cumulated CPU time (s) 699.14
Current children cumulated vsize (Kb) 65632

[startup+710.071 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24508
Raw data (/proc/24504/stat): 24504 (minisat+_script) S 24503 24504 9854 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788602511 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24504/statm): 531 226 485 147 0 384 0
[pid=24504] vsize: 2124
Raw data (/proc/24508/stat): 24508 (minisat+_64-bit) R 24504 24504 9854 0 -1 0 15473 0 0 0 70832 80 0 0 25 0 1 0 1788602516 65462272 14960 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24508/statm): 15982 14960 145 145 0 15837 0
[pid=24508] vsize: 63928
Current children cumulated CPU time (s) 709.13
Current children cumulated vsize (Kb) 66052

[startup+720.071 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24508
Raw data (/proc/24504/stat): 24504 (minisat+_script) S 24503 24504 9854 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788602511 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24504/statm): 531 226 485 147 0 384 0
[pid=24504] vsize: 2124
Raw data (/proc/24508/stat): 24508 (minisat+_64-bit) T 24504 24504 9854 0 -1 0 15564 0 0 0 71831 80 0 0 25 0 1 0 1788602516 65818624 15051 4294967295 134512640 135094434 3221224432 3221222796 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/24508/statm): 16069 15051 145 145 0 15924 0
[pid=24508] vsize: 64276
Current children cumulated CPU time (s) 719.12
Current children cumulated vsize (Kb) 66400

[startup+730.072 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24508
Raw data (/proc/24504/stat): 24504 (minisat+_script) S 24503 24504 9854 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788602511 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24504/statm): 531 226 485 147 0 384 0
[pid=24504] vsize: 2124
Raw data (/proc/24508/stat): 24508 (minisat+_64-bit) R 24504 24504 9854 0 -1 0 15657 0 0 0 72829 81 0 0 25 0 1 0 1788602516 66203648 15144 4294967295 134512640 135094434 3221224432 3221223088 134557950 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24508/statm): 16163 15144 145 145 0 16018 0
[pid=24508] vsize: 64652
Current children cumulated CPU time (s) 729.11
Current children cumulated vsize (Kb) 66776

[startup+740.073 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24508
Raw data (/proc/24504/stat): 24504 (minisat+_script) S 24503 24504 9854 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788602511 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24504/statm): 531 226 485 147 0 384 0
[pid=24504] vsize: 2124
Raw data (/proc/24508/stat): 24508 (minisat+_64-bit) R 24504 24504 9854 0 -1 0 15789 0 0 0 73826 82 0 0 25 0 1 0 1788602516 66736128 15276 4294967295 134512640 135094434 3221224432 3221223076 134558040 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24508/statm): 16293 15276 145 145 0 16148 0
[pid=24508] vsize: 65172
Current children cumulated CPU time (s) 739.09
Current children cumulated vsize (Kb) 67296

[startup+750.075 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24508
Raw data (/proc/24504/stat): 24504 (minisat+_script) S 24503 24504 9854 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788602511 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24504/statm): 531 226 485 147 0 384 0
[pid=24504] vsize: 2124
Raw data (/proc/24508/stat): 24508 (minisat+_64-bit) R 24504 24504 9854 0 -1 0 15915 0 0 0 74823 84 0 0 25 0 1 0 1788602516 67239936 15402 4294967295 134512640 135094434 3221224432 3221223056 134557636 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24508/statm): 16416 15402 145 145 0 16271 0
[pid=24508] vsize: 65664
Current children cumulated CPU time (s) 749.08
Current children cumulated vsize (Kb) 67788

[startup+760.076 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24508
Raw data (/proc/24504/stat): 24504 (minisat+_script) S 24503 24504 9854 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788602511 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24504/statm): 531 226 485 147 0 384 0
[pid=24504] vsize: 2124
Raw data (/proc/24508/stat): 24508 (minisat+_64-bit) R 24504 24504 9854 0 -1 0 16008 0 0 0 75821 85 0 0 25 0 1 0 1788602516 68136960 15495 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24508/statm): 16635 15495 145 145 0 16490 0
[pid=24508] vsize: 66540
Current children cumulated CPU time (s) 759.07
Current children cumulated vsize (Kb) 68664

[startup+770.076 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24508
Raw data (/proc/24504/stat): 24504 (minisat+_script) S 24503 24504 9854 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788602511 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24504/statm): 531 226 485 147 0 384 0
[pid=24504] vsize: 2124
Raw data (/proc/24508/stat): 24508 (minisat+_64-bit) R 24504 24504 9854 0 -1 0 16097 0 0 0 76819 86 0 0 25 0 1 0 1788602516 68497408 15584 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24508/statm): 16723 15584 145 145 0 16578 0
[pid=24508] vsize: 66892
Current children cumulated CPU time (s) 769.06
Current children cumulated vsize (Kb) 69016

[startup+780.077 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24508
Raw data (/proc/24504/stat): 24504 (minisat+_script) S 24503 24504 9854 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788602511 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24504/statm): 531 226 485 147 0 384 0
[pid=24504] vsize: 2124
Raw data (/proc/24508/stat): 24508 (minisat+_64-bit) R 24504 24504 9854 0 -1 0 16156 0 0 0 77819 86 0 0 25 0 1 0 1788602516 68730880 15643 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24508/statm): 16780 15643 145 145 0 16635 0
[pid=24508] vsize: 67120
Current children cumulated CPU time (s) 779.06
Current children cumulated vsize (Kb) 69244

[startup+790.078 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24508
Raw data (/proc/24504/stat): 24504 (minisat+_script) S 24503 24504 9854 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788602511 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24504/statm): 531 226 485 147 0 384 0
[pid=24504] vsize: 2124
Raw data (/proc/24508/stat): 24508 (minisat+_64-bit) R 24504 24504 9854 0 -1 0 16268 0 0 0 78817 87 0 0 25 0 1 0 1788602516 69185536 15755 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24508/statm): 16891 15755 145 145 0 16746 0
[pid=24508] vsize: 67564
Current children cumulated CPU time (s) 789.05
Current children cumulated vsize (Kb) 69688

[startup+800.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24508
Raw data (/proc/24504/stat): 24504 (minisat+_script) S 24503 24504 9854 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788602511 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24504/statm): 531 226 485 147 0 384 0
[pid=24504] vsize: 2124
Raw data (/proc/24508/stat): 24508 (minisat+_64-bit) R 24504 24504 9854 0 -1 0 16364 0 0 0 79816 87 0 0 25 0 1 0 1788602516 69562368 15851 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24508/statm): 16983 15851 145 145 0 16838 0
[pid=24508] vsize: 67932
Current children cumulated CPU time (s) 799.04
Current children cumulated vsize (Kb) 70056

[startup+810.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24508
Raw data (/proc/24504/stat): 24504 (minisat+_script) S 24503 24504 9854 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788602511 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24504/statm): 531 226 485 147 0 384 0
[pid=24504] vsize: 2124
Raw data (/proc/24508/stat): 24508 (minisat+_64-bit) R 24504 24504 9854 0 -1 0 16488 0 0 0 80814 88 0 0 25 0 1 0 1788602516 70070272 15975 4294967295 134512640 135094434 3221224432 3221223024 134551906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24508/statm): 17107 15975 145 145 0 16962 0
[pid=24508] vsize: 68428
Current children cumulated CPU time (s) 809.03
Current children cumulated vsize (Kb) 70552

[startup+820.081 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24508
Raw data (/proc/24504/stat): 24504 (minisat+_script) S 24503 24504 9854 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788602511 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24504/statm): 531 226 485 147 0 384 0
[pid=24504] vsize: 2124
Raw data (/proc/24508/stat): 24508 (minisat+_64-bit) R 24504 24504 9854 0 -1 0 16643 0 0 0 81811 89 0 0 25 0 1 0 1788602516 70701056 16130 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24508/statm): 17261 16130 145 145 0 17116 0
[pid=24508] vsize: 69044
Current children cumulated CPU time (s) 819.01
Current children cumulated vsize (Kb) 71168

[startup+830.083 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24508
Raw data (/proc/24504/stat): 24504 (minisat+_script) S 24503 24504 9854 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788602511 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24504/statm): 531 226 485 147 0 384 0
[pid=24504] vsize: 2124
Raw data (/proc/24508/stat): 24508 (minisat+_64-bit) R 24504 24504 9854 0 -1 0 16826 0 0 0 82809 90 0 0 25 0 1 0 1788602516 71442432 16313 4294967295 134512640 135094434 3221224432 3221223076 134558040 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24508/statm): 17442 16313 145 145 0 17297 0
[pid=24508] vsize: 69768
Current children cumulated CPU time (s) 829
Current children cumulated vsize (Kb) 71892

[startup+840.084 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24508
Raw data (/proc/24504/stat): 24504 (minisat+_script) S 24503 24504 9854 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788602511 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24504/statm): 531 226 485 147 0 384 0
[pid=24504] vsize: 2124
Raw data (/proc/24508/stat): 24508 (minisat+_64-bit) R 24504 24504 9854 0 -1 0 17013 0 0 0 83806 91 0 0 25 0 1 0 1788602516 72204288 16500 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24508/statm): 17628 16500 145 145 0 17483 0
[pid=24508] vsize: 70512
Current children cumulated CPU time (s) 838.98
Current children cumulated vsize (Kb) 72636

[startup+850.085 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24508
Raw data (/proc/24504/stat): 24504 (minisat+_script) S 24503 24504 9854 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788602511 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24504/statm): 531 226 485 147 0 384 0
[pid=24504] vsize: 2124
Raw data (/proc/24508/stat): 24508 (minisat+_64-bit) R 24504 24504 9854 0 -1 0 17103 0 0 0 84804 92 0 0 25 0 1 0 1788602516 72564736 16590 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24508/statm): 17716 16590 145 145 0 17571 0
[pid=24508] vsize: 70864
Current children cumulated CPU time (s) 848.97
Current children cumulated vsize (Kb) 72988

[startup+860.085 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24508
Raw data (/proc/24504/stat): 24504 (minisat+_script) S 24503 24504 9854 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788602511 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24504/statm): 531 226 485 147 0 384 0
[pid=24504] vsize: 2124
Raw data (/proc/24508/stat): 24508 (minisat+_64-bit) R 24504 24504 9854 0 -1 0 17222 0 0 0 85802 93 0 0 25 0 1 0 1788602516 73039872 16709 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24508/statm): 17832 16709 145 145 0 17687 0
[pid=24508] vsize: 71328
Current children cumulated CPU time (s) 858.96
Current children cumulated vsize (Kb) 73452

[startup+870.085 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24508
Raw data (/proc/24504/stat): 24504 (minisat+_script) S 24503 24504 9854 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788602511 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24504/statm): 531 226 485 147 0 384 0
[pid=24504] vsize: 2124
Raw data (/proc/24508/stat): 24508 (minisat+_64-bit) R 24504 24504 9854 0 -1 0 17324 0 0 0 86800 93 0 0 25 0 1 0 1788602516 73449472 16811 4294967295 134512640 135094434 3221224432 3221223088 134557925 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24508/statm): 17932 16811 145 145 0 17787 0
[pid=24508] vsize: 71728
Current children cumulated CPU time (s) 868.94
Current children cumulated vsize (Kb) 73852

[startup+880.086 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24508
Raw data (/proc/24504/stat): 24504 (minisat+_script) S 24503 24504 9854 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788602511 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24504/statm): 531 226 485 147 0 384 0
[pid=24504] vsize: 2124
Raw data (/proc/24508/stat): 24508 (minisat+_64-bit) R 24504 24504 9854 0 -1 0 17442 0 0 0 87799 94 0 0 25 0 1 0 1788602516 73932800 16929 4294967295 134512640 135094434 3221224432 3221223092 134553487 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24508/statm): 18050 16929 145 145 0 17905 0
[pid=24508] vsize: 72200
Current children cumulated CPU time (s) 878.94
Current children cumulated vsize (Kb) 74324

[startup+890.087 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24508
Raw data (/proc/24504/stat): 24504 (minisat+_script) S 24503 24504 9854 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788602511 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24504/statm): 531 226 485 147 0 384 0
[pid=24504] vsize: 2124
Raw data (/proc/24508/stat): 24508 (minisat+_64-bit) R 24504 24504 9854 0 -1 0 17523 0 0 0 88798 94 0 0 25 0 1 0 1788602516 74256384 17010 4294967295 134512640 135094434 3221224432 3221223088 134558007 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24508/statm): 18129 17010 145 145 0 17984 0
[pid=24508] vsize: 72516
Current children cumulated CPU time (s) 888.93
Current children cumulated vsize (Kb) 74640

[startup+900.087 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24508
Raw data (/proc/24504/stat): 24504 (minisat+_script) S 24503 24504 9854 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788602511 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24504/statm): 531 226 485 147 0 384 0
[pid=24504] vsize: 2124
Raw data (/proc/24508/stat): 24508 (minisat+_64-bit) R 24504 24504 9854 0 -1 0 17651 0 0 0 89796 95 0 0 25 0 1 0 1788602516 74772480 17138 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24508/statm): 18255 17138 145 145 0 18110 0
[pid=24508] vsize: 73020
Current children cumulated CPU time (s) 898.92
Current children cumulated vsize (Kb) 75144

[startup+910.088 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24508
Raw data (/proc/24504/stat): 24504 (minisat+_script) S 24503 24504 9854 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788602511 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24504/statm): 531 226 485 147 0 384 0
[pid=24504] vsize: 2124
Raw data (/proc/24508/stat): 24508 (minisat+_64-bit) R 24504 24504 9854 0 -1 0 17864 0 0 0 90791 97 0 0 25 0 1 0 1788602516 75649024 17351 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24508/statm): 18469 17351 145 145 0 18324 0
[pid=24508] vsize: 73876
Current children cumulated CPU time (s) 908.89
Current children cumulated vsize (Kb) 76000

[startup+920.089 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24508
Raw data (/proc/24504/stat): 24504 (minisat+_script) S 24503 24504 9854 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788602511 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24504/statm): 531 226 485 147 0 384 0
[pid=24504] vsize: 2124
Raw data (/proc/24508/stat): 24508 (minisat+_64-bit) R 24504 24504 9854 0 -1 0 17952 0 0 0 91790 98 0 0 25 0 1 0 1788602516 76001280 17439 4294967295 134512640 135094434 3221224432 3221223024 134556904 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24508/statm): 18555 17439 145 145 0 18410 0
[pid=24508] vsize: 74220
Current children cumulated CPU time (s) 918.89
Current children cumulated vsize (Kb) 76344

[startup+930.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24508
Raw data (/proc/24504/stat): 24504 (minisat+_script) S 24503 24504 9854 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788602511 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24504/statm): 531 226 485 147 0 384 0
[pid=24504] vsize: 2124
Raw data (/proc/24508/stat): 24508 (minisat+_64-bit) R 24504 24504 9854 0 -1 0 18027 0 0 0 92789 99 0 0 25 0 1 0 1788602516 76304384 17514 4294967295 134512640 135094434 3221224432 3221223088 134557884 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24508/statm): 18629 17514 145 145 0 18484 0
[pid=24508] vsize: 74516
Current children cumulated CPU time (s) 928.89
Current children cumulated vsize (Kb) 76640

[startup+940.091 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24508
Raw data (/proc/24504/stat): 24504 (minisat+_script) S 24503 24504 9854 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788602511 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24504/statm): 531 226 485 147 0 384 0
[pid=24504] vsize: 2124
Raw data (/proc/24508/stat): 24508 (minisat+_64-bit) R 24504 24504 9854 0 -1 0 18113 0 0 0 93788 99 0 0 25 0 1 0 1788602516 76652544 17600 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24508/statm): 18714 17600 145 145 0 18569 0
[pid=24508] vsize: 74856
Current children cumulated CPU time (s) 938.88
Current children cumulated vsize (Kb) 76980

[startup+950.092 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24508
Raw data (/proc/24504/stat): 24504 (minisat+_script) S 24503 24504 9854 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788602511 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24504/statm): 531 226 485 147 0 384 0
[pid=24504] vsize: 2124
Raw data (/proc/24508/stat): 24508 (minisat+_64-bit) R 24504 24504 9854 0 -1 0 18194 0 0 0 94786 99 0 0 25 0 1 0 1788602516 76980224 17681 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24508/statm): 18794 17681 145 145 0 18649 0
[pid=24508] vsize: 75176
Current children cumulated CPU time (s) 948.86
Current children cumulated vsize (Kb) 77300

[startup+960.093 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24508
Raw data (/proc/24504/stat): 24504 (minisat+_script) S 24503 24504 9854 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788602511 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24504/statm): 531 226 485 147 0 384 0
[pid=24504] vsize: 2124
Raw data (/proc/24508/stat): 24508 (minisat+_64-bit) R 24504 24504 9854 0 -1 0 18270 0 0 0 95785 100 0 0 25 0 1 0 1788602516 77287424 17757 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24508/statm): 18869 17757 145 145 0 18724 0
[pid=24508] vsize: 75476
Current children cumulated CPU time (s) 958.86
Current children cumulated vsize (Kb) 77600

[startup+970.094 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24508
Raw data (/proc/24504/stat): 24504 (minisat+_script) S 24503 24504 9854 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788602511 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24504/statm): 531 226 485 147 0 384 0
[pid=24504] vsize: 2124
Raw data (/proc/24508/stat): 24508 (minisat+_64-bit) R 24504 24504 9854 0 -1 0 18360 0 0 0 96784 100 0 0 25 0 1 0 1788602516 77651968 17847 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24508/statm): 18958 17847 145 145 0 18813 0
[pid=24508] vsize: 75832
Current children cumulated CPU time (s) 968.85
Current children cumulated vsize (Kb) 77956

[startup+980.096 s]
Raw data (loadavg): 0.99 0.97 0.91 1/57 24508
Raw data (/proc/24504/stat): 24504 (minisat+_script) S 24503 24504 9854 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788602511 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24504/statm): 531 226 485 147 0 384 0
[pid=24504] vsize: 2124
Raw data (/proc/24508/stat): 24508 (minisat+_64-bit) T 24504 24504 9854 0 -1 0 18443 0 0 0 97782 101 0 0 25 0 1 0 1788602516 77987840 17930 4294967295 134512640 135094434 3221224432 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/24508/statm): 19040 17930 145 145 0 18895 0
[pid=24508] vsize: 76160
Current children cumulated CPU time (s) 978.84
Current children cumulated vsize (Kb) 78284

[startup+990.097 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24508
Raw data (/proc/24504/stat): 24504 (minisat+_script) S 24503 24504 9854 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788602511 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24504/statm): 531 226 485 147 0 384 0
[pid=24504] vsize: 2124
Raw data (/proc/24508/stat): 24508 (minisat+_64-bit) R 24504 24504 9854 0 -1 0 18599 0 0 0 98778 102 0 0 25 0 1 0 1788602516 78639104 18086 4294967295 134512640 135094434 3221224432 3221223088 134557863 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24508/statm): 19199 18086 145 145 0 19054 0
[pid=24508] vsize: 76796
Current children cumulated CPU time (s) 988.81
Current children cumulated vsize (Kb) 78920

[startup+1000.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24508
Raw data (/proc/24504/stat): 24504 (minisat+_script) S 24503 24504 9854 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788602511 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24504/statm): 531 226 485 147 0 384 0
[pid=24504] vsize: 2124
Raw data (/proc/24508/stat): 24508 (minisat+_64-bit) R 24504 24504 9854 0 -1 0 18679 0 0 0 99777 102 0 0 25 0 1 0 1788602516 78966784 18166 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24508/statm): 19279 18166 145 145 0 19134 0
[pid=24508] vsize: 77116
Current children cumulated CPU time (s) 998.8
Current children cumulated vsize (Kb) 79240

[startup+1010.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24508
Raw data (/proc/24504/stat): 24504 (minisat+_script) S 24503 24504 9854 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788602511 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24504/statm): 531 226 485 147 0 384 0
[pid=24504] vsize: 2124
Raw data (/proc/24508/stat): 24508 (minisat+_64-bit) R 24504 24504 9854 0 -1 0 18759 0 0 0 100775 103 0 0 25 0 1 0 1788602516 79290368 18246 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24508/statm): 19358 18246 145 145 0 19213 0
[pid=24508] vsize: 77432
Current children cumulated CPU time (s) 1008.79
Current children cumulated vsize (Kb) 79556

[startup+1020.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24508
Raw data (/proc/24504/stat): 24504 (minisat+_script) S 24503 24504 9854 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788602511 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24504/statm): 531 226 485 147 0 384 0
[pid=24504] vsize: 2124
Raw data (/proc/24508/stat): 24508 (minisat+_64-bit) R 24504 24504 9854 0 -1 0 18839 0 0 0 101775 103 0 0 25 0 1 0 1788602516 79650816 18326 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24508/statm): 19446 18326 145 145 0 19301 0
[pid=24508] vsize: 77784
Current children cumulated CPU time (s) 1018.79
Current children cumulated vsize (Kb) 79908

[startup+1030.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24508
Raw data (/proc/24504/stat): 24504 (minisat+_script) S 24503 24504 9854 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788602511 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24504/statm): 531 226 485 147 0 384 0
[pid=24504] vsize: 2124
Raw data (/proc/24508/stat): 24508 (minisat+_64-bit) R 24504 24504 9854 0 -1 0 18905 0 0 0 102774 104 0 0 25 0 1 0 1788602516 79929344 18392 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24508/statm): 19514 18392 145 145 0 19369 0
[pid=24508] vsize: 78056
Current children cumulated CPU time (s) 1028.79
Current children cumulated vsize (Kb) 80180

[startup+1040.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24508
Raw data (/proc/24504/stat): 24504 (minisat+_script) S 24503 24504 9854 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788602511 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24504/statm): 531 226 485 147 0 384 0
[pid=24504] vsize: 2124
Raw data (/proc/24508/stat): 24508 (minisat+_64-bit) R 24504 24504 9854 0 -1 0 18958 0 0 0 103773 104 0 0 25 0 1 0 1788602516 80142336 18445 4294967295 134512640 135094434 3221224432 3221223088 134557945 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24508/statm): 19566 18445 145 145 0 19421 0
[pid=24508] vsize: 78264
Current children cumulated CPU time (s) 1038.78
Current children cumulated vsize (Kb) 80388

[startup+1050.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24508
Raw data (/proc/24504/stat): 24504 (minisat+_script) S 24503 24504 9854 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788602511 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24504/statm): 531 226 485 147 0 384 0
[pid=24504] vsize: 2124
Raw data (/proc/24508/stat): 24508 (minisat+_64-bit) R 24504 24504 9854 0 -1 0 19077 0 0 0 104771 105 0 0 25 0 1 0 1788602516 80617472 18564 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24508/statm): 19682 18564 145 145 0 19537 0
[pid=24508] vsize: 78728
Current children cumulated CPU time (s) 1048.77
Current children cumulated vsize (Kb) 80852

[startup+1060.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24508
Raw data (/proc/24504/stat): 24504 (minisat+_script) S 24503 24504 9854 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788602511 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24504/statm): 531 226 485 147 0 384 0
[pid=24504] vsize: 2124
Raw data (/proc/24508/stat): 24508 (minisat+_64-bit) R 24504 24504 9854 0 -1 0 19148 0 0 0 105770 105 0 0 25 0 1 0 1788602516 80904192 18635 4294967295 134512640 135094434 3221224432 3221223056 134557612 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24508/statm): 19752 18635 145 145 0 19607 0
[pid=24508] vsize: 79008
Current children cumulated CPU time (s) 1058.76
Current children cumulated vsize (Kb) 81132

[startup+1070.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24508
Raw data (/proc/24504/stat): 24504 (minisat+_script) S 24503 24504 9854 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788602511 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24504/statm): 531 226 485 147 0 384 0
[pid=24504] vsize: 2124
Raw data (/proc/24508/stat): 24508 (minisat+_64-bit) R 24504 24504 9854 0 -1 0 19228 0 0 0 106769 106 0 0 25 0 1 0 1788602516 81227776 18715 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24508/statm): 19831 18715 145 145 0 19686 0
[pid=24508] vsize: 79324
Current children cumulated CPU time (s) 1068.76
Current children cumulated vsize (Kb) 81448

[startup+1080.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24508
Raw data (/proc/24504/stat): 24504 (minisat+_script) S 24503 24504 9854 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788602511 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24504/statm): 531 226 485 147 0 384 0
[pid=24504] vsize: 2124
Raw data (/proc/24508/stat): 24508 (minisat+_64-bit) R 24504 24504 9854 0 -1 0 19301 0 0 0 107767 107 0 0 25 0 1 0 1788602516 81522688 18788 4294967295 134512640 135094434 3221224432 3221223088 134558395 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24508/statm): 19903 18788 145 145 0 19758 0
[pid=24508] vsize: 79612
Current children cumulated CPU time (s) 1078.75
Current children cumulated vsize (Kb) 81736

[startup+1090.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24508
Raw data (/proc/24504/stat): 24504 (minisat+_script) S 24503 24504 9854 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788602511 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24504/statm): 531 226 485 147 0 384 0
[pid=24504] vsize: 2124
Raw data (/proc/24508/stat): 24508 (minisat+_64-bit) R 24504 24504 9854 0 -1 0 19358 0 0 0 108766 107 0 0 25 0 1 0 1788602516 81752064 18845 4294967295 134512640 135094434 3221224432 3221223088 134558225 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24508/statm): 19959 18845 145 145 0 19814 0
[pid=24508] vsize: 79836
Current children cumulated CPU time (s) 1088.74
Current children cumulated vsize (Kb) 81960

[startup+1100.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24508
Raw data (/proc/24504/stat): 24504 (minisat+_script) S 24503 24504 9854 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788602511 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24504/statm): 531 226 485 147 0 384 0
[pid=24504] vsize: 2124
Raw data (/proc/24508/stat): 24508 (minisat+_64-bit) R 24504 24504 9854 0 -1 0 19434 0 0 0 109765 108 0 0 25 0 1 0 1788602516 82071552 18921 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24508/statm): 20037 18921 145 145 0 19892 0
[pid=24508] vsize: 80148
Current children cumulated CPU time (s) 1098.74
Current children cumulated vsize (Kb) 82272

[startup+1110.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24508
Raw data (/proc/24504/stat): 24504 (minisat+_script) S 24503 24504 9854 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788602511 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24504/statm): 531 226 485 147 0 384 0
[pid=24504] vsize: 2124
Raw data (/proc/24508/stat): 24508 (minisat+_64-bit) R 24504 24504 9854 0 -1 0 19501 0 0 0 110763 109 0 0 25 0 1 0 1788602516 82333696 18988 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24508/statm): 20101 18988 145 145 0 19956 0
[pid=24508] vsize: 80404
Current children cumulated CPU time (s) 1108.73
Current children cumulated vsize (Kb) 82528

[startup+1120.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24508
Raw data (/proc/24504/stat): 24504 (minisat+_script) S 24503 24504 9854 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788602511 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24504/statm): 531 226 485 147 0 384 0
[pid=24504] vsize: 2124
Raw data (/proc/24508/stat): 24508 (minisat+_64-bit) R 24504 24504 9854 0 -1 0 19579 0 0 0 111762 109 0 0 25 0 1 0 1788602516 82640896 19066 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24508/statm): 20176 19066 145 145 0 20031 0
[pid=24508] vsize: 80704
Current children cumulated CPU time (s) 1118.72
Current children cumulated vsize (Kb) 82828

[startup+1130.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24508
Raw data (/proc/24504/stat): 24504 (minisat+_script) S 24503 24504 9854 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788602511 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24504/statm): 531 226 485 147 0 384 0
[pid=24504] vsize: 2124
Raw data (/proc/24508/stat): 24508 (minisat+_64-bit) R 24504 24504 9854 0 -1 0 19652 0 0 0 112761 110 0 0 25 0 1 0 1788602516 82935808 19139 4294967295 134512640 135094434 3221224432 3221223088 134557875 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24508/statm): 20248 19139 145 145 0 20103 0
[pid=24508] vsize: 80992
Current children cumulated CPU time (s) 1128.72
Current children cumulated vsize (Kb) 83116

[startup+1140.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24508
Raw data (/proc/24504/stat): 24504 (minisat+_script) S 24503 24504 9854 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788602511 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24504/statm): 531 226 485 147 0 384 0
[pid=24504] vsize: 2124
Raw data (/proc/24508/stat): 24508 (minisat+_64-bit) R 24504 24504 9854 0 -1 0 19719 0 0 0 113760 111 0 0 25 0 1 0 1788602516 83206144 19206 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24508/statm): 20314 19206 145 145 0 20169 0
[pid=24508] vsize: 81256
Current children cumulated CPU time (s) 1138.72
Current children cumulated vsize (Kb) 83380

[startup+1150.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24508
Raw data (/proc/24504/stat): 24504 (minisat+_script) S 24503 24504 9854 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788602511 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24504/statm): 531 226 485 147 0 384 0
[pid=24504] vsize: 2124
Raw data (/proc/24508/stat): 24508 (minisat+_64-bit) R 24504 24504 9854 0 -1 0 19793 0 0 0 114758 112 0 0 25 0 1 0 1788602516 83505152 19280 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24508/statm): 20387 19280 145 145 0 20242 0
[pid=24508] vsize: 81548
Current children cumulated CPU time (s) 1148.71
Current children cumulated vsize (Kb) 83672

[startup+1160.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24508
Raw data (/proc/24504/stat): 24504 (minisat+_script) S 24503 24504 9854 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788602511 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24504/statm): 531 226 485 147 0 384 0
[pid=24504] vsize: 2124
Raw data (/proc/24508/stat): 24508 (minisat+_64-bit) R 24504 24504 9854 0 -1 0 19891 0 0 0 115755 113 0 0 25 0 1 0 1788602516 83890176 19378 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24508/statm): 20481 19378 145 145 0 20336 0
[pid=24508] vsize: 81924
Current children cumulated CPU time (s) 1158.69
Current children cumulated vsize (Kb) 84048

[startup+1170.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24508
Raw data (/proc/24504/stat): 24504 (minisat+_script) S 24503 24504 9854 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788602511 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24504/statm): 531 226 485 147 0 384 0
[pid=24504] vsize: 2124
Raw data (/proc/24508/stat): 24508 (minisat+_64-bit) R 24504 24504 9854 0 -1 0 19967 0 0 0 116754 114 0 0 25 0 1 0 1788602516 84201472 19454 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24508/statm): 20557 19454 145 145 0 20412 0
[pid=24508] vsize: 82228
Current children cumulated CPU time (s) 1168.69
Current children cumulated vsize (Kb) 84352

[startup+1180.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24508
Raw data (/proc/24504/stat): 24504 (minisat+_script) S 24503 24504 9854 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788602511 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24504/statm): 531 226 485 147 0 384 0
[pid=24504] vsize: 2124
Raw data (/proc/24508/stat): 24508 (minisat+_64-bit) R 24504 24504 9854 0 -1 0 20037 0 0 0 117753 114 0 0 25 0 1 0 1788602516 84475904 19524 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24508/statm): 20624 19524 145 145 0 20479 0
[pid=24508] vsize: 82496
Current children cumulated CPU time (s) 1178.68
Current children cumulated vsize (Kb) 84620

[startup+1190.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24508
Raw data (/proc/24504/stat): 24504 (minisat+_script) S 24503 24504 9854 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788602511 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24504/statm): 531 226 485 147 0 384 0
[pid=24504] vsize: 2124
Raw data (/proc/24508/stat): 24508 (minisat+_64-bit) R 24504 24504 9854 0 -1 0 20141 0 0 0 118751 115 0 0 25 0 1 0 1788602516 84893696 19628 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24508/statm): 20726 19628 145 145 0 20581 0
[pid=24508] vsize: 82904
Current children cumulated CPU time (s) 1188.67
Current children cumulated vsize (Kb) 85028

[startup+1200.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24508
Raw data (/proc/24504/stat): 24504 (minisat+_script) S 24503 24504 9854 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788602511 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24504/statm): 531 226 485 147 0 384 0
[pid=24504] vsize: 2124
Raw data (/proc/24508/stat): 24508 (minisat+_64-bit) R 24504 24504 9854 0 -1 0 20211 0 0 0 119750 115 0 0 25 0 1 0 1788602516 85180416 19698 4294967295 134512640 135094434 3221224432 3221223088 134558426 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24508/statm): 20796 19698 145 145 0 20651 0
[pid=24508] vsize: 83184
Current children cumulated CPU time (s) 1198.66
Current children cumulated vsize (Kb) 85308

[startup+1210.12 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24508
Raw data (/proc/24504/stat): 24504 (minisat+_script) S 24503 24504 9854 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788602511 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24504/statm): 531 226 485 147 0 384 0
[pid=24504] vsize: 2124
Raw data (/proc/24508/stat): 24508 (minisat+_64-bit) R 24504 24504 9854 0 -1 0 20257 0 0 0 120749 116 0 0 25 0 1 0 1788602516 85364736 19744 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24508/statm): 20841 19744 145 145 0 20696 0
[pid=24508] vsize: 83364
Current children cumulated CPU time (s) 1208.66
Current children cumulated vsize (Kb) 85488



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.12 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24508
Raw data (/proc/24504/stat): 24504 (minisat+_script) S 24503 24504 9854 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788602511 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24504/statm): 531 226 485 147 0 384 0
[pid=24504] vsize: 2124
Raw data (/proc/24508/stat): 24508 (minisat+_64-bit) R 24504 24504 9854 0 -1 0 20257 0 0 0 120750 116 0 0 25 0 1 0 1788602516 85364736 19744 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24508/statm): 20841 19744 145 145 0 20696 0
[pid=24508] vsize: 83364
Current children cumulated CPU time (s) 1208.67
Current children cumulated vsize (Kb) 85488

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

Child status: 0
Real time (s): 1210.16
CPU time (s): 1208.7
CPU user time (s): 1207.5
CPU system time (s): 1.20282
CPU usage (%): 99.8799
Max. virtual memory (cumulated for all children) (Kb): 85488

Verifier Data

ERROR: no interpretation found !