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/plato.asu.edu/pub/unibo/normalized-mps-v2-20-10-roll3000.opb
MD5SUMb5e0cd2fd527d211d525adea6c422112
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 5939

Launcher Data

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 450.999
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:        893160 kB
Buffers:         13888 kB
Cached:          98176 kB
SwapCached:        612 kB
Active:          40644 kB
Inactive:        73896 kB
HighTotal:      131008 kB
HighFree:        29372 kB
LowTotal:       903652 kB
LowFree:        863788 kB
SwapTotal:     2097136 kB
SwapFree:      2095848 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5656 kB
Slab:            21284 kB
Committed_AS:    64168 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-09-20 02:31:26 (client local time) WITH STATUS 0 IN 1208.59 SECONDS
stats: 3112 7 1208.59 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/29747/stat): 29747 (minisat+_script) R 29746 29747 31778 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1796597668 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 0 0 0
Raw data (/proc/29747/statm): 174 3 169 147 0 27 0
[pid=29747] 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=29748
New process pid=29749
New process pid=29750
execve syscall for /bin/sed executable
One traced child (pid=29749) 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=29750) exited with status: 0
One traced child (pid=29748) exited with status: 0
New process pid=29751
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc15/normalized-mps-v2-20-10-roll3000.opb

[startup+10.0036 s]
Raw data (loadavg): 0.93 0.98 0.99 2/57 29751
Raw data (/proc/29747/stat): 29747 (minisat+_script) S 29746 29747 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796597668 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29747/statm): 531 226 485 147 0 384 0
[pid=29747] vsize: 2124
Raw data (/proc/29751/stat): 29751 (minisat+_64-bit) R 29747 29747 31778 0 -1 0 3472 0 0 0 958 20 0 0 25 0 1 0 1796597673 13246464 2965 4294967295 134512640 135094434 3221224432 3221220824 134676334 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/29751/statm): 3234 2965 145 145 0 3089 0
[pid=29751] vsize: 12936
Current children cumulated CPU time (s) 9.79
Current children cumulated vsize (Kb) 15060

[startup+20.0044 s]
Raw data (loadavg): 0.94 0.98 0.99 2/57 29751
Raw data (/proc/29747/stat): 29747 (minisat+_script) S 29746 29747 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796597668 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29747/statm): 531 226 485 147 0 384 0
[pid=29747] vsize: 2124
Raw data (/proc/29751/stat): 29751 (minisat+_64-bit) R 29747 29747 31778 0 -1 0 10046 0 0 0 1899 48 0 0 25 0 1 0 1796597673 43196416 9532 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29751/statm): 10546 9532 145 145 0 10401 0
[pid=29751] vsize: 42184
Current children cumulated CPU time (s) 19.48
Current children cumulated vsize (Kb) 44308

[startup+30.0062 s]
Raw data (loadavg): 0.95 0.98 0.99 2/57 29751
Raw data (/proc/29747/stat): 29747 (minisat+_script) S 29746 29747 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796597668 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29747/statm): 531 226 485 147 0 384 0
[pid=29747] vsize: 2124
Raw data (/proc/29751/stat): 29751 (minisat+_64-bit) R 29747 29747 31778 0 -1 0 10097 0 0 0 2898 49 0 0 25 0 1 0 1796597673 43384832 9583 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29751/statm): 10592 9583 145 145 0 10447 0
[pid=29751] vsize: 42368
Current children cumulated CPU time (s) 29.48
Current children cumulated vsize (Kb) 44492

[startup+40.007 s]
Raw data (loadavg): 0.96 0.98 0.99 2/57 29751
Raw data (/proc/29747/stat): 29747 (minisat+_script) S 29746 29747 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796597668 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29747/statm): 531 226 485 147 0 384 0
[pid=29747] vsize: 2124
Raw data (/proc/29751/stat): 29751 (minisat+_64-bit) R 29747 29747 31778 0 -1 0 10124 0 0 0 3898 49 0 0 25 0 1 0 1796597673 43495424 9610 4294967295 134512640 135094434 3221224432 3221223072 134562095 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29751/statm): 10619 9610 145 145 0 10474 0
[pid=29751] vsize: 42476
Current children cumulated CPU time (s) 39.48
Current children cumulated vsize (Kb) 44600

[startup+50.0088 s]
Raw data (loadavg): 0.96 0.98 0.99 2/57 29751
Raw data (/proc/29747/stat): 29747 (minisat+_script) S 29746 29747 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796597668 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29747/statm): 531 226 485 147 0 384 0
[pid=29747] vsize: 2124
Raw data (/proc/29751/stat): 29751 (minisat+_64-bit) R 29747 29747 31778 0 -1 0 10159 0 0 0 4897 49 0 0 25 0 1 0 1796597673 43626496 9645 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29751/statm): 10651 9645 145 145 0 10506 0
[pid=29751] vsize: 42604
Current children cumulated CPU time (s) 49.47
Current children cumulated vsize (Kb) 44728

[startup+60.0097 s]
Raw data (loadavg): 0.97 0.98 0.99 2/57 29751
Raw data (/proc/29747/stat): 29747 (minisat+_script) S 29746 29747 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796597668 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29747/statm): 531 226 485 147 0 384 0
[pid=29747] vsize: 2124
Raw data (/proc/29751/stat): 29751 (minisat+_64-bit) R 29747 29747 31778 0 -1 0 10200 0 0 0 5897 50 0 0 25 0 1 0 1796597673 43814912 9686 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29751/statm): 10697 9686 145 145 0 10552 0
[pid=29751] vsize: 42788
Current children cumulated CPU time (s) 59.48
Current children cumulated vsize (Kb) 44912

[startup+70.0105 s]
Raw data (loadavg): 0.97 0.98 0.99 2/57 29751
Raw data (/proc/29747/stat): 29747 (minisat+_script) S 29746 29747 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796597668 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29747/statm): 531 226 485 147 0 384 0
[pid=29747] vsize: 2124
Raw data (/proc/29751/stat): 29751 (minisat+_64-bit) R 29747 29747 31778 0 -1 0 10265 0 0 0 6896 50 0 0 25 0 1 0 1796597673 44056576 9751 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29751/statm): 10756 9751 145 145 0 10611 0
[pid=29751] vsize: 43024
Current children cumulated CPU time (s) 69.47
Current children cumulated vsize (Kb) 45148

[startup+80.0123 s]
Raw data (loadavg): 0.98 0.98 0.99 2/57 29751
Raw data (/proc/29747/stat): 29747 (minisat+_script) S 29746 29747 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796597668 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29747/statm): 531 226 485 147 0 384 0
[pid=29747] vsize: 2124
Raw data (/proc/29751/stat): 29751 (minisat+_64-bit) R 29747 29747 31778 0 -1 0 10318 0 0 0 7896 50 0 0 25 0 1 0 1796597673 44265472 9804 4294967295 134512640 135094434 3221224432 3221223104 134556288 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29751/statm): 10807 9804 145 145 0 10662 0
[pid=29751] vsize: 43228
Current children cumulated CPU time (s) 79.47
Current children cumulated vsize (Kb) 45352

[startup+90.0131 s]
Raw data (loadavg): 0.98 0.98 0.99 2/57 29751
Raw data (/proc/29747/stat): 29747 (minisat+_script) S 29746 29747 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796597668 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29747/statm): 531 226 485 147 0 384 0
[pid=29747] vsize: 2124
Raw data (/proc/29751/stat): 29751 (minisat+_64-bit) R 29747 29747 31778 0 -1 0 10359 0 0 0 8894 51 0 0 25 0 1 0 1796597673 44429312 9845 4294967295 134512640 135094434 3221224432 3221223092 134553530 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29751/statm): 10847 9845 145 145 0 10702 0
[pid=29751] vsize: 43388
Current children cumulated CPU time (s) 89.46
Current children cumulated vsize (Kb) 45512

[startup+100.014 s]
Raw data (loadavg): 0.98 0.98 0.99 2/57 29751
Raw data (/proc/29747/stat): 29747 (minisat+_script) S 29746 29747 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796597668 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29747/statm): 531 226 485 147 0 384 0
[pid=29747] vsize: 2124
Raw data (/proc/29751/stat): 29751 (minisat+_64-bit) R 29747 29747 31778 0 -1 0 10407 0 0 0 9894 51 0 0 25 0 1 0 1796597673 44683264 9893 4294967295 134512640 135094434 3221224432 3221223024 134556904 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29751/statm): 10909 9893 145 145 0 10764 0
[pid=29751] vsize: 43636
Current children cumulated CPU time (s) 99.46
Current children cumulated vsize (Kb) 45760

[startup+110.015 s]
Raw data (loadavg): 0.98 0.98 0.99 2/57 29751
Raw data (/proc/29747/stat): 29747 (minisat+_script) S 29746 29747 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796597668 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29747/statm): 531 226 485 147 0 384 0
[pid=29747] vsize: 2124
Raw data (/proc/29751/stat): 29751 (minisat+_64-bit) R 29747 29747 31778 0 -1 0 10477 0 0 0 10893 52 0 0 25 0 1 0 1796597673 44961792 9963 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29751/statm): 10977 9963 145 145 0 10832 0
[pid=29751] vsize: 43908
Current children cumulated CPU time (s) 109.46
Current children cumulated vsize (Kb) 46032

[startup+120.016 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 29751
Raw data (/proc/29747/stat): 29747 (minisat+_script) S 29746 29747 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796597668 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29747/statm): 531 226 485 147 0 384 0
[pid=29747] vsize: 2124
Raw data (/proc/29751/stat): 29751 (minisat+_64-bit) R 29747 29747 31778 0 -1 0 10563 0 0 0 11892 52 0 0 25 0 1 0 1796597673 45277184 10049 4294967295 134512640 135094434 3221224432 3221223088 134558221 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29751/statm): 11054 10049 145 145 0 10909 0
[pid=29751] vsize: 44216
Current children cumulated CPU time (s) 119.45
Current children cumulated vsize (Kb) 46340

[startup+130.016 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 29751
Raw data (/proc/29747/stat): 29747 (minisat+_script) S 29746 29747 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796597668 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29747/statm): 531 226 485 147 0 384 0
[pid=29747] vsize: 2124
Raw data (/proc/29751/stat): 29751 (minisat+_64-bit) R 29747 29747 31778 0 -1 0 10613 0 0 0 12892 53 0 0 25 0 1 0 1796597673 45473792 10099 4294967295 134512640 135094434 3221224432 3221223024 134552178 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29751/statm): 11102 10099 145 145 0 10957 0
[pid=29751] vsize: 44408
Current children cumulated CPU time (s) 129.46
Current children cumulated vsize (Kb) 46532

[startup+140.017 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 29751
Raw data (/proc/29747/stat): 29747 (minisat+_script) S 29746 29747 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796597668 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29747/statm): 531 226 485 147 0 384 0
[pid=29747] vsize: 2124
Raw data (/proc/29751/stat): 29751 (minisat+_64-bit) R 29747 29747 31778 0 -1 0 10686 0 0 0 13890 53 0 0 25 0 1 0 1796597673 45768704 10172 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29751/statm): 11174 10172 145 145 0 11029 0
[pid=29751] vsize: 44696
Current children cumulated CPU time (s) 139.44
Current children cumulated vsize (Kb) 46820

[startup+150.019 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 29751
Raw data (/proc/29747/stat): 29747 (minisat+_script) S 29746 29747 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796597668 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29747/statm): 531 226 485 147 0 384 0
[pid=29747] vsize: 2124
Raw data (/proc/29751/stat): 29751 (minisat+_64-bit) R 29747 29747 31778 0 -1 0 10767 0 0 0 14888 54 0 0 25 0 1 0 1796597673 46092288 10253 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29751/statm): 11253 10253 145 145 0 11108 0
[pid=29751] vsize: 45012
Current children cumulated CPU time (s) 149.43
Current children cumulated vsize (Kb) 47136

[startup+160.02 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 29751
Raw data (/proc/29747/stat): 29747 (minisat+_script) S 29746 29747 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796597668 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29747/statm): 531 226 485 147 0 384 0
[pid=29747] vsize: 2124
Raw data (/proc/29751/stat): 29751 (minisat+_64-bit) R 29747 29747 31778 0 -1 0 10836 0 0 0 15887 55 0 0 25 0 1 0 1796597673 46366720 10322 4294967295 134512640 135094434 3221224432 3221223044 134563061 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29751/statm): 11320 10322 145 145 0 11175 0
[pid=29751] vsize: 45280
Current children cumulated CPU time (s) 159.43
Current children cumulated vsize (Kb) 47404

[startup+170.021 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 29751
Raw data (/proc/29747/stat): 29747 (minisat+_script) S 29746 29747 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796597668 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29747/statm): 531 226 485 147 0 384 0
[pid=29747] vsize: 2124
Raw data (/proc/29751/stat): 29751 (minisat+_64-bit) R 29747 29747 31778 0 -1 0 10900 0 0 0 16886 55 0 0 25 0 1 0 1796597673 46620672 10386 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29751/statm): 11382 10386 145 145 0 11237 0
[pid=29751] vsize: 45528
Current children cumulated CPU time (s) 169.42
Current children cumulated vsize (Kb) 47652

[startup+180.022 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 29751
Raw data (/proc/29747/stat): 29747 (minisat+_script) S 29746 29747 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796597668 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29747/statm): 531 226 485 147 0 384 0
[pid=29747] vsize: 2124
Raw data (/proc/29751/stat): 29751 (minisat+_64-bit) R 29747 29747 31778 0 -1 0 10988 0 0 0 17885 56 0 0 25 0 1 0 1796597673 47095808 10474 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29751/statm): 11498 10474 145 145 0 11353 0
[pid=29751] vsize: 45992
Current children cumulated CPU time (s) 179.42
Current children cumulated vsize (Kb) 48116

[startup+190.022 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 29751
Raw data (/proc/29747/stat): 29747 (minisat+_script) S 29746 29747 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796597668 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29747/statm): 531 226 485 147 0 384 0
[pid=29747] vsize: 2124
Raw data (/proc/29751/stat): 29751 (minisat+_64-bit) R 29747 29747 31778 0 -1 0 11046 0 0 0 18884 56 0 0 25 0 1 0 1796597673 47325184 10532 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29751/statm): 11554 10532 145 145 0 11409 0
[pid=29751] vsize: 46216
Current children cumulated CPU time (s) 189.41
Current children cumulated vsize (Kb) 48340

[startup+200.024 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 29751
Raw data (/proc/29747/stat): 29747 (minisat+_script) S 29746 29747 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796597668 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29747/statm): 531 226 485 147 0 384 0
[pid=29747] vsize: 2124
Raw data (/proc/29751/stat): 29751 (minisat+_64-bit) R 29747 29747 31778 0 -1 0 11105 0 0 0 19883 56 0 0 25 0 1 0 1796597673 47562752 10591 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29751/statm): 11612 10591 145 145 0 11467 0
[pid=29751] vsize: 46448
Current children cumulated CPU time (s) 199.4
Current children cumulated vsize (Kb) 48572

[startup+210.025 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 29751
Raw data (/proc/29747/stat): 29747 (minisat+_script) S 29746 29747 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796597668 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29747/statm): 531 226 485 147 0 384 0
[pid=29747] vsize: 2124
Raw data (/proc/29751/stat): 29751 (minisat+_64-bit) R 29747 29747 31778 0 -1 0 11190 0 0 0 20881 58 0 0 25 0 1 0 1796597673 47898624 10676 4294967295 134512640 135094434 3221224432 3221223056 134557627 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29751/statm): 11694 10676 145 145 0 11549 0
[pid=29751] vsize: 46776
Current children cumulated CPU time (s) 209.4
Current children cumulated vsize (Kb) 48900

[startup+220.026 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 29751
Raw data (/proc/29747/stat): 29747 (minisat+_script) S 29746 29747 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796597668 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29747/statm): 531 226 485 147 0 384 0
[pid=29747] vsize: 2124
Raw data (/proc/29751/stat): 29751 (minisat+_64-bit) R 29747 29747 31778 0 -1 0 11261 0 0 0 21879 58 0 0 25 0 1 0 1796597673 48185344 10747 4294967295 134512640 135094434 3221224432 3221223056 134557577 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29751/statm): 11764 10747 145 145 0 11619 0
[pid=29751] vsize: 47056
Current children cumulated CPU time (s) 219.38
Current children cumulated vsize (Kb) 49180

[startup+230.027 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 29751
Raw data (/proc/29747/stat): 29747 (minisat+_script) S 29746 29747 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796597668 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29747/statm): 531 226 485 147 0 384 0
[pid=29747] vsize: 2124
Raw data (/proc/29751/stat): 29751 (minisat+_64-bit) R 29747 29747 31778 0 -1 0 11367 0 0 0 22877 60 0 0 25 0 1 0 1796597673 48611328 10853 4294967295 134512640 135094434 3221224432 3221223056 134557585 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29751/statm): 11868 10853 145 145 0 11723 0
[pid=29751] vsize: 47472
Current children cumulated CPU time (s) 229.38
Current children cumulated vsize (Kb) 49596

[startup+240.027 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 29751
Raw data (/proc/29747/stat): 29747 (minisat+_script) S 29746 29747 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796597668 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29747/statm): 531 226 485 147 0 384 0
[pid=29747] vsize: 2124
Raw data (/proc/29751/stat): 29751 (minisat+_64-bit) R 29747 29747 31778 0 -1 0 11425 0 0 0 23877 60 0 0 25 0 1 0 1796597673 48844800 10911 4294967295 134512640 135094434 3221224432 3221223120 134554709 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29751/statm): 11925 10911 145 145 0 11780 0
[pid=29751] vsize: 47700
Current children cumulated CPU time (s) 239.38
Current children cumulated vsize (Kb) 49824

[startup+250.029 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 29751
Raw data (/proc/29747/stat): 29747 (minisat+_script) S 29746 29747 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796597668 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29747/statm): 531 226 485 147 0 384 0
[pid=29747] vsize: 2124
Raw data (/proc/29751/stat): 29751 (minisat+_64-bit) R 29747 29747 31778 0 -1 0 11476 0 0 0 24876 60 0 0 25 0 1 0 1796597673 49045504 10962 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29751/statm): 11974 10962 145 145 0 11829 0
[pid=29751] vsize: 47896
Current children cumulated CPU time (s) 249.37
Current children cumulated vsize (Kb) 50020

[startup+260.031 s]
Raw data (loadavg): 0.99 0.98 0.99 1/57 29751
Raw data (/proc/29747/stat): 29747 (minisat+_script) S 29746 29747 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796597668 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29747/statm): 531 226 485 147 0 384 0
[pid=29747] vsize: 2124
Raw data (/proc/29751/stat): 29751 (minisat+_64-bit) T 29747 29747 31778 0 -1 0 11554 0 0 0 25875 61 0 0 25 0 1 0 1796597673 49356800 11040 4294967295 134512640 135094434 3221224432 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/29751/statm): 12050 11040 145 145 0 11905 0
[pid=29751] vsize: 48200
Current children cumulated CPU time (s) 259.37
Current children cumulated vsize (Kb) 50324

[startup+270.031 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 29751
Raw data (/proc/29747/stat): 29747 (minisat+_script) S 29746 29747 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796597668 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29747/statm): 531 226 485 147 0 384 0
[pid=29747] vsize: 2124
Raw data (/proc/29751/stat): 29751 (minisat+_64-bit) R 29747 29747 31778 0 -1 0 11623 0 0 0 26874 61 0 0 25 0 1 0 1796597673 49635328 11109 4294967295 134512640 135094434 3221224432 3221223088 134557987 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29751/statm): 12118 11109 145 145 0 11973 0
[pid=29751] vsize: 48472
Current children cumulated CPU time (s) 269.36
Current children cumulated vsize (Kb) 50596

[startup+280.032 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 29751
Raw data (/proc/29747/stat): 29747 (minisat+_script) S 29746 29747 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796597668 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29747/statm): 531 226 485 147 0 384 0
[pid=29747] vsize: 2124
Raw data (/proc/29751/stat): 29751 (minisat+_64-bit) R 29747 29747 31778 0 -1 0 11695 0 0 0 27873 62 0 0 25 0 1 0 1796597673 49922048 11181 4294967295 134512640 135094434 3221224432 3221223088 134558392 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29751/statm): 12188 11181 145 145 0 12043 0
[pid=29751] vsize: 48752
Current children cumulated CPU time (s) 279.36
Current children cumulated vsize (Kb) 50876

[startup+290.033 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 29751
Raw data (/proc/29747/stat): 29747 (minisat+_script) S 29746 29747 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796597668 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29747/statm): 531 226 485 147 0 384 0
[pid=29747] vsize: 2124
Raw data (/proc/29751/stat): 29751 (minisat+_64-bit) R 29747 29747 31778 0 -1 0 11792 0 0 0 28871 62 0 0 25 0 1 0 1796597673 50319360 11278 4294967295 134512640 135094434 3221224432 3221223056 134557696 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29751/statm): 12285 11278 145 145 0 12140 0
[pid=29751] vsize: 49140
Current children cumulated CPU time (s) 289.34
Current children cumulated vsize (Kb) 51264

[startup+300.033 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 29751
Raw data (/proc/29747/stat): 29747 (minisat+_script) S 29746 29747 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796597668 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29747/statm): 531 226 485 147 0 384 0
[pid=29747] vsize: 2124
Raw data (/proc/29751/stat): 29751 (minisat+_64-bit) R 29747 29747 31778 0 -1 0 11868 0 0 0 29870 63 0 0 25 0 1 0 1796597673 50622464 11354 4294967295 134512640 135094434 3221224432 3221223056 134562104 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29751/statm): 12359 11354 145 145 0 12214 0
[pid=29751] vsize: 49436
Current children cumulated CPU time (s) 299.34
Current children cumulated vsize (Kb) 51560

[startup+310.034 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 29751
Raw data (/proc/29747/stat): 29747 (minisat+_script) S 29746 29747 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796597668 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29747/statm): 531 226 485 147 0 384 0
[pid=29747] vsize: 2124
Raw data (/proc/29751/stat): 29751 (minisat+_64-bit) R 29747 29747 31778 0 -1 0 11963 0 0 0 30868 64 0 0 25 0 1 0 1796597673 51003392 11449 4294967295 134512640 135094434 3221224432 3221223088 134558156 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29751/statm): 12452 11449 145 145 0 12307 0
[pid=29751] vsize: 49808
Current children cumulated CPU time (s) 309.33
Current children cumulated vsize (Kb) 51932

[startup+320.035 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 29751
Raw data (/proc/29747/stat): 29747 (minisat+_script) S 29746 29747 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796597668 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29747/statm): 531 226 485 147 0 384 0
[pid=29747] vsize: 2124
Raw data (/proc/29751/stat): 29751 (minisat+_64-bit) R 29747 29747 31778 0 -1 0 12026 0 0 0 31867 64 0 0 25 0 1 0 1796597673 51253248 11512 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29751/statm): 12513 11512 145 145 0 12368 0
[pid=29751] vsize: 50052
Current children cumulated CPU time (s) 319.32
Current children cumulated vsize (Kb) 52176

[startup+330.036 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 29751
Raw data (/proc/29747/stat): 29747 (minisat+_script) S 29746 29747 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796597668 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29747/statm): 531 226 485 147 0 384 0
[pid=29747] vsize: 2124
Raw data (/proc/29751/stat): 29751 (minisat+_64-bit) R 29747 29747 31778 0 -1 0 12138 0 0 0 32865 65 0 0 25 0 1 0 1796597673 51703808 11624 4294967295 134512640 135094434 3221224432 3221223056 134557685 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29751/statm): 12623 11624 145 145 0 12478 0
[pid=29751] vsize: 50492
Current children cumulated CPU time (s) 329.31
Current children cumulated vsize (Kb) 52616

[startup+340.037 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 29751
Raw data (/proc/29747/stat): 29747 (minisat+_script) S 29746 29747 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796597668 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29747/statm): 531 226 485 147 0 384 0
[pid=29747] vsize: 2124
Raw data (/proc/29751/stat): 29751 (minisat+_64-bit) R 29747 29747 31778 0 -1 0 12227 0 0 0 33864 66 0 0 25 0 1 0 1796597673 52064256 11713 4294967295 134512640 135094434 3221224432 3221223092 134553528 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29751/statm): 12711 11713 145 145 0 12566 0
[pid=29751] vsize: 50844
Current children cumulated CPU time (s) 339.31
Current children cumulated vsize (Kb) 52968

[startup+350.037 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 29751
Raw data (/proc/29747/stat): 29747 (minisat+_script) S 29746 29747 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796597668 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29747/statm): 531 226 485 147 0 384 0
[pid=29747] vsize: 2124
Raw data (/proc/29751/stat): 29751 (minisat+_64-bit) R 29747 29747 31778 0 -1 0 12280 0 0 0 34863 66 0 0 25 0 1 0 1796597673 52273152 11766 4294967295 134512640 135094434 3221224432 3221223092 134553497 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29751/statm): 12762 11766 145 145 0 12617 0
[pid=29751] vsize: 51048
Current children cumulated CPU time (s) 349.3
Current children cumulated vsize (Kb) 53172

[startup+360.038 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 29751
Raw data (/proc/29747/stat): 29747 (minisat+_script) S 29746 29747 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796597668 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29747/statm): 531 226 485 147 0 384 0
[pid=29747] vsize: 2124
Raw data (/proc/29751/stat): 29751 (minisat+_64-bit) R 29747 29747 31778 0 -1 0 12347 0 0 0 35862 66 0 0 25 0 1 0 1796597673 52543488 11833 4294967295 134512640 135094434 3221224432 3221223104 134556073 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29751/statm): 12828 11833 145 145 0 12683 0
[pid=29751] vsize: 51312
Current children cumulated CPU time (s) 359.29
Current children cumulated vsize (Kb) 53436

[startup+370.039 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 29751
Raw data (/proc/29747/stat): 29747 (minisat+_script) S 29746 29747 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796597668 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29747/statm): 531 226 485 147 0 384 0
[pid=29747] vsize: 2124
Raw data (/proc/29751/stat): 29751 (minisat+_64-bit) R 29747 29747 31778 0 -1 0 12400 0 0 0 36860 67 0 0 25 0 1 0 1796597673 53018624 11886 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29751/statm): 12944 11886 145 145 0 12799 0
[pid=29751] vsize: 51776
Current children cumulated CPU time (s) 369.28
Current children cumulated vsize (Kb) 53900

[startup+380.041 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 29751
Raw data (/proc/29747/stat): 29747 (minisat+_script) S 29746 29747 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796597668 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29747/statm): 531 226 485 147 0 384 0
[pid=29747] vsize: 2124
Raw data (/proc/29751/stat): 29751 (minisat+_64-bit) R 29747 29747 31778 0 -1 0 12446 0 0 0 37860 67 0 0 25 0 1 0 1796597673 53198848 11932 4294967295 134512640 135094434 3221224432 3221223088 134558246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29751/statm): 12988 11932 145 145 0 12843 0
[pid=29751] vsize: 51952
Current children cumulated CPU time (s) 379.28
Current children cumulated vsize (Kb) 54076

[startup+390.042 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 29751
Raw data (/proc/29747/stat): 29747 (minisat+_script) S 29746 29747 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796597668 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29747/statm): 531 226 485 147 0 384 0
[pid=29747] vsize: 2124
Raw data (/proc/29751/stat): 29751 (minisat+_64-bit) R 29747 29747 31778 0 -1 0 12511 0 0 0 38859 68 0 0 25 0 1 0 1796597673 53460992 11997 4294967295 134512640 135094434 3221224432 3221223088 134558405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29751/statm): 13052 11997 145 145 0 12907 0
[pid=29751] vsize: 52208
Current children cumulated CPU time (s) 389.28
Current children cumulated vsize (Kb) 54332

[startup+400.044 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 29751
Raw data (/proc/29747/stat): 29747 (minisat+_script) S 29746 29747 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796597668 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29747/statm): 531 226 485 147 0 384 0
[pid=29747] vsize: 2124
Raw data (/proc/29751/stat): 29751 (minisat+_64-bit) R 29747 29747 31778 0 -1 0 12556 0 0 0 39858 68 0 0 25 0 1 0 1796597673 53641216 12042 4294967295 134512640 135094434 3221224432 3221223124 134558984 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29751/statm): 13096 12042 145 145 0 12951 0
[pid=29751] vsize: 52384
Current children cumulated CPU time (s) 399.27
Current children cumulated vsize (Kb) 54508

[startup+410.044 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 29751
Raw data (/proc/29747/stat): 29747 (minisat+_script) S 29746 29747 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796597668 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29747/statm): 531 226 485 147 0 384 0
[pid=29747] vsize: 2124
Raw data (/proc/29751/stat): 29751 (minisat+_64-bit) R 29747 29747 31778 0 -1 0 12658 0 0 0 40857 68 0 0 25 0 1 0 1796597673 54050816 12144 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29751/statm): 13196 12144 145 145 0 13051 0
[pid=29751] vsize: 52784
Current children cumulated CPU time (s) 409.26
Current children cumulated vsize (Kb) 54908

[startup+420.044 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 29751
Raw data (/proc/29747/stat): 29747 (minisat+_script) S 29746 29747 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796597668 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29747/statm): 531 226 485 147 0 384 0
[pid=29747] vsize: 2124
Raw data (/proc/29751/stat): 29751 (minisat+_64-bit) R 29747 29747 31778 0 -1 0 12781 0 0 0 41855 70 0 0 25 0 1 0 1796597673 54550528 12267 4294967295 134512640 135094434 3221224432 3221223088 134557928 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29751/statm): 13318 12267 145 145 0 13173 0
[pid=29751] vsize: 53272
Current children cumulated CPU time (s) 419.26
Current children cumulated vsize (Kb) 55396

[startup+430.046 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 29751
Raw data (/proc/29747/stat): 29747 (minisat+_script) S 29746 29747 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796597668 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29747/statm): 531 226 485 147 0 384 0
[pid=29747] vsize: 2124
Raw data (/proc/29751/stat): 29751 (minisat+_64-bit) R 29747 29747 31778 0 -1 0 12850 0 0 0 42855 70 0 0 25 0 1 0 1796597673 54824960 12336 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29751/statm): 13385 12336 145 145 0 13240 0
[pid=29751] vsize: 53540
Current children cumulated CPU time (s) 429.26
Current children cumulated vsize (Kb) 55664

[startup+440.047 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 29751
Raw data (/proc/29747/stat): 29747 (minisat+_script) S 29746 29747 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796597668 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29747/statm): 531 226 485 147 0 384 0
[pid=29747] vsize: 2124
Raw data (/proc/29751/stat): 29751 (minisat+_64-bit) R 29747 29747 31778 0 -1 0 12940 0 0 0 43853 70 0 0 25 0 1 0 1796597673 55189504 12426 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29751/statm): 13474 12426 145 145 0 13329 0
[pid=29751] vsize: 53896
Current children cumulated CPU time (s) 439.24
Current children cumulated vsize (Kb) 56020

[startup+450.048 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 29751
Raw data (/proc/29747/stat): 29747 (minisat+_script) S 29746 29747 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796597668 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29747/statm): 531 226 485 147 0 384 0
[pid=29747] vsize: 2124
Raw data (/proc/29751/stat): 29751 (minisat+_64-bit) R 29747 29747 31778 0 -1 0 12963 0 0 0 44853 70 0 0 25 0 1 0 1796597673 55279616 12449 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29751/statm): 13496 12449 145 145 0 13351 0
[pid=29751] vsize: 53984
Current children cumulated CPU time (s) 449.24
Current children cumulated vsize (Kb) 56108

[startup+460.048 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 29751
Raw data (/proc/29747/stat): 29747 (minisat+_script) S 29746 29747 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796597668 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29747/statm): 531 226 485 147 0 384 0
[pid=29747] vsize: 2124
Raw data (/proc/29751/stat): 29751 (minisat+_64-bit) R 29747 29747 31778 0 -1 0 13033 0 0 0 45851 71 0 0 25 0 1 0 1796597673 55562240 12519 4294967295 134512640 135094434 3221224432 3221223056 134557650 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29751/statm): 13565 12519 145 145 0 13420 0
[pid=29751] vsize: 54260
Current children cumulated CPU time (s) 459.23
Current children cumulated vsize (Kb) 56384

[startup+470.049 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 29751
Raw data (/proc/29747/stat): 29747 (minisat+_script) S 29746 29747 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796597668 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29747/statm): 531 226 485 147 0 384 0
[pid=29747] vsize: 2124
Raw data (/proc/29751/stat): 29751 (minisat+_64-bit) R 29747 29747 31778 0 -1 0 13187 0 0 0 46848 72 0 0 25 0 1 0 1796597673 56184832 12673 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29751/statm): 13717 12673 145 145 0 13572 0
[pid=29751] vsize: 54868
Current children cumulated CPU time (s) 469.21
Current children cumulated vsize (Kb) 56992

[startup+480.05 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 29751
Raw data (/proc/29747/stat): 29747 (minisat+_script) S 29746 29747 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796597668 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29747/statm): 531 226 485 147 0 384 0
[pid=29747] vsize: 2124
Raw data (/proc/29751/stat): 29751 (minisat+_64-bit) R 29747 29747 31778 0 -1 0 13298 0 0 0 47846 74 0 0 25 0 1 0 1796597673 56631296 12784 4294967295 134512640 135094434 3221224432 3221223088 134557820 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/29751/statm): 13826 12784 145 145 0 13681 0
[pid=29751] vsize: 55304
Current children cumulated CPU time (s) 479.21
Current children cumulated vsize (Kb) 57428

[startup+490.051 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 29751
Raw data (/proc/29747/stat): 29747 (minisat+_script) S 29746 29747 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796597668 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29747/statm): 531 226 485 147 0 384 0
[pid=29747] vsize: 2124
Raw data (/proc/29751/stat): 29751 (minisat+_64-bit) R 29747 29747 31778 0 -1 0 13378 0 0 0 48843 75 0 0 25 0 1 0 1796597673 56950784 12864 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29751/statm): 13904 12864 145 145 0 13759 0
[pid=29751] vsize: 55616
Current children cumulated CPU time (s) 489.19
Current children cumulated vsize (Kb) 57740

[startup+500.053 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 29751
Raw data (/proc/29747/stat): 29747 (minisat+_script) S 29746 29747 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796597668 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29747/statm): 531 226 485 147 0 384 0
[pid=29747] vsize: 2124
Raw data (/proc/29751/stat): 29751 (minisat+_64-bit) R 29747 29747 31778 0 -1 0 13473 0 0 0 49842 75 0 0 25 0 1 0 1796597673 57331712 12959 4294967295 134512640 135094434 3221224432 3221223120 134554748 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29751/statm): 13997 12959 145 145 0 13852 0
[pid=29751] vsize: 55988
Current children cumulated CPU time (s) 499.18
Current children cumulated vsize (Kb) 58112

[startup+510.054 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 29751
Raw data (/proc/29747/stat): 29747 (minisat+_script) S 29746 29747 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796597668 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29747/statm): 531 226 485 147 0 384 0
[pid=29747] vsize: 2124
Raw data (/proc/29751/stat): 29751 (minisat+_64-bit) R 29747 29747 31778 0 -1 0 13550 0 0 0 50840 76 0 0 25 0 1 0 1796597673 57638912 13036 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29751/statm): 14072 13036 145 145 0 13927 0
[pid=29751] vsize: 56288
Current children cumulated CPU time (s) 509.17
Current children cumulated vsize (Kb) 58412

[startup+520.054 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 29751
Raw data (/proc/29747/stat): 29747 (minisat+_script) S 29746 29747 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796597668 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29747/statm): 531 226 485 147 0 384 0
[pid=29747] vsize: 2124
Raw data (/proc/29751/stat): 29751 (minisat+_64-bit) R 29747 29747 31778 0 -1 0 13635 0 0 0 51840 77 0 0 25 0 1 0 1796597673 57978880 13121 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29751/statm): 14155 13121 145 145 0 14010 0
[pid=29751] vsize: 56620
Current children cumulated CPU time (s) 519.18
Current children cumulated vsize (Kb) 58744

[startup+530.055 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 29751
Raw data (/proc/29747/stat): 29747 (minisat+_script) S 29746 29747 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796597668 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29747/statm): 531 226 485 147 0 384 0
[pid=29747] vsize: 2124
Raw data (/proc/29751/stat): 29751 (minisat+_64-bit) R 29747 29747 31778 0 -1 0 13768 0 0 0 52838 77 0 0 25 0 1 0 1796597673 58519552 13254 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29751/statm): 14287 13254 145 145 0 14142 0
[pid=29751] vsize: 57148
Current children cumulated CPU time (s) 529.16
Current children cumulated vsize (Kb) 59272

[startup+540.056 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 29751
Raw data (/proc/29747/stat): 29747 (minisat+_script) S 29746 29747 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796597668 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29747/statm): 531 226 485 147 0 384 0
[pid=29747] vsize: 2124
Raw data (/proc/29751/stat): 29751 (minisat+_64-bit) R 29747 29747 31778 0 -1 0 13864 0 0 0 53836 78 0 0 25 0 1 0 1796597673 58904576 13350 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29751/statm): 14381 13350 145 145 0 14236 0
[pid=29751] vsize: 57524
Current children cumulated CPU time (s) 539.15
Current children cumulated vsize (Kb) 59648

[startup+550.058 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 29751
Raw data (/proc/29747/stat): 29747 (minisat+_script) S 29746 29747 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796597668 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29747/statm): 531 226 485 147 0 384 0
[pid=29747] vsize: 2124
Raw data (/proc/29751/stat): 29751 (minisat+_64-bit) R 29747 29747 31778 0 -1 0 13991 0 0 0 54833 80 0 0 25 0 1 0 1796597673 59416576 13477 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29751/statm): 14506 13477 145 145 0 14361 0
[pid=29751] vsize: 58024
Current children cumulated CPU time (s) 549.14
Current children cumulated vsize (Kb) 60148

[startup+560.059 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 29751
Raw data (/proc/29747/stat): 29747 (minisat+_script) S 29746 29747 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796597668 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29747/statm): 531 226 485 147 0 384 0
[pid=29747] vsize: 2124
Raw data (/proc/29751/stat): 29751 (minisat+_64-bit) R 29747 29747 31778 0 -1 0 14052 0 0 0 55832 80 0 0 25 0 1 0 1796597673 59654144 13538 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29751/statm): 14564 13538 145 145 0 14419 0
[pid=29751] vsize: 58256
Current children cumulated CPU time (s) 559.13
Current children cumulated vsize (Kb) 60380

[startup+570.059 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 29751
Raw data (/proc/29747/stat): 29747 (minisat+_script) S 29746 29747 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796597668 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29747/statm): 531 226 485 147 0 384 0
[pid=29747] vsize: 2124
Raw data (/proc/29751/stat): 29751 (minisat+_64-bit) R 29747 29747 31778 0 -1 0 14118 0 0 0 56831 81 0 0 25 0 1 0 1796597673 59920384 13604 4294967295 134512640 135094434 3221224432 3221223088 134558235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29751/statm): 14629 13604 145 145 0 14484 0
[pid=29751] vsize: 58516
Current children cumulated CPU time (s) 569.13
Current children cumulated vsize (Kb) 60640

[startup+580.06 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 29751
Raw data (/proc/29747/stat): 29747 (minisat+_script) S 29746 29747 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796597668 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29747/statm): 531 226 485 147 0 384 0
[pid=29747] vsize: 2124
Raw data (/proc/29751/stat): 29751 (minisat+_64-bit) R 29747 29747 31778 0 -1 0 14248 0 0 0 57829 82 0 0 25 0 1 0 1796597673 60452864 13734 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29751/statm): 14759 13734 145 145 0 14614 0
[pid=29751] vsize: 59036
Current children cumulated CPU time (s) 579.12
Current children cumulated vsize (Kb) 61160

[startup+590.061 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 29751
Raw data (/proc/29747/stat): 29747 (minisat+_script) S 29746 29747 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796597668 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29747/statm): 531 226 485 147 0 384 0
[pid=29747] vsize: 2124
Raw data (/proc/29751/stat): 29751 (minisat+_64-bit) R 29747 29747 31778 0 -1 0 14286 0 0 0 58828 82 0 0 25 0 1 0 1796597673 60600320 13772 4294967295 134512640 135094434 3221224432 3221223056 134557714 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29751/statm): 14795 13772 145 145 0 14650 0
[pid=29751] vsize: 59180
Current children cumulated CPU time (s) 589.11
Current children cumulated vsize (Kb) 61304

[startup+600.063 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 29751
Raw data (/proc/29747/stat): 29747 (minisat+_script) S 29746 29747 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796597668 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29747/statm): 531 226 485 147 0 384 0
[pid=29747] vsize: 2124
Raw data (/proc/29751/stat): 29751 (minisat+_64-bit) R 29747 29747 31778 0 -1 0 14319 0 0 0 59828 82 0 0 25 0 1 0 1796597673 60743680 13805 4294967295 134512640 135094434 3221224432 3221223056 134557585 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29751/statm): 14830 13805 145 145 0 14685 0
[pid=29751] vsize: 59320
Current children cumulated CPU time (s) 599.11
Current children cumulated vsize (Kb) 61444

[startup+610.064 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 29751
Raw data (/proc/29747/stat): 29747 (minisat+_script) S 29746 29747 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796597668 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29747/statm): 531 226 485 147 0 384 0
[pid=29747] vsize: 2124
Raw data (/proc/29751/stat): 29751 (minisat+_64-bit) R 29747 29747 31778 0 -1 0 14414 0 0 0 60826 83 0 0 25 0 1 0 1796597673 61116416 13900 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29751/statm): 14921 13900 145 145 0 14776 0
[pid=29751] vsize: 59684
Current children cumulated CPU time (s) 609.1
Current children cumulated vsize (Kb) 61808

[startup+620.065 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 29751
Raw data (/proc/29747/stat): 29747 (minisat+_script) S 29746 29747 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796597668 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29747/statm): 531 226 485 147 0 384 0
[pid=29747] vsize: 2124
Raw data (/proc/29751/stat): 29751 (minisat+_64-bit) R 29747 29747 31778 0 -1 0 14519 0 0 0 61825 84 0 0 25 0 1 0 1796597673 61550592 14005 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29751/statm): 15027 14005 145 145 0 14882 0
[pid=29751] vsize: 60108
Current children cumulated CPU time (s) 619.1
Current children cumulated vsize (Kb) 62232

[startup+630.065 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 29751
Raw data (/proc/29747/stat): 29747 (minisat+_script) S 29746 29747 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796597668 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29747/statm): 531 226 485 147 0 384 0
[pid=29747] vsize: 2124
Raw data (/proc/29751/stat): 29751 (minisat+_64-bit) R 29747 29747 31778 0 -1 0 14621 0 0 0 62824 85 0 0 25 0 1 0 1796597673 61964288 14107 4294967295 134512640 135094434 3221224432 3221223064 134557561 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29751/statm): 15128 14107 145 145 0 14983 0
[pid=29751] vsize: 60512
Current children cumulated CPU time (s) 629.1
Current children cumulated vsize (Kb) 62636

[startup+640.066 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 29751
Raw data (/proc/29747/stat): 29747 (minisat+_script) S 29746 29747 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796597668 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29747/statm): 531 226 485 147 0 384 0
[pid=29747] vsize: 2124
Raw data (/proc/29751/stat): 29751 (minisat+_64-bit) R 29747 29747 31778 0 -1 0 14740 0 0 0 63822 86 0 0 25 0 1 0 1796597673 62443520 14226 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/29751/statm): 15245 14226 145 145 0 15100 0
[pid=29751] vsize: 60980
Current children cumulated CPU time (s) 639.09
Current children cumulated vsize (Kb) 63104

[startup+650.068 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 29751
Raw data (/proc/29747/stat): 29747 (minisat+_script) S 29746 29747 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796597668 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29747/statm): 531 226 485 147 0 384 0
[pid=29747] vsize: 2124
Raw data (/proc/29751/stat): 29751 (minisat+_64-bit) R 29747 29747 31778 0 -1 0 14831 0 0 0 64820 87 0 0 25 0 1 0 1796597673 62808064 14317 4294967295 134512640 135094434 3221224432 3221223088 134558225 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/29751/statm): 15334 14317 145 145 0 15189 0
[pid=29751] vsize: 61336
Current children cumulated CPU time (s) 649.08
Current children cumulated vsize (Kb) 63460

[startup+660.069 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 29751
Raw data (/proc/29747/stat): 29747 (minisat+_script) S 29746 29747 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796597668 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29747/statm): 531 226 485 147 0 384 0
[pid=29747] vsize: 2124
Raw data (/proc/29751/stat): 29751 (minisat+_64-bit) R 29747 29747 31778 0 -1 0 14899 0 0 0 65818 88 0 0 25 0 1 0 1796597673 63082496 14385 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/29751/statm): 15401 14385 145 145 0 15256 0
[pid=29751] vsize: 61604
Current children cumulated CPU time (s) 659.07
Current children cumulated vsize (Kb) 63728

[startup+670.07 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 29751
Raw data (/proc/29747/stat): 29747 (minisat+_script) S 29746 29747 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796597668 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29747/statm): 531 226 485 147 0 384 0
[pid=29747] vsize: 2124
Raw data (/proc/29751/stat): 29751 (minisat+_64-bit) R 29747 29747 31778 0 -1 0 14993 0 0 0 66816 89 0 0 25 0 1 0 1796597673 63467520 14479 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/29751/statm): 15495 14479 145 145 0 15350 0
[pid=29751] vsize: 61980
Current children cumulated CPU time (s) 669.06
Current children cumulated vsize (Kb) 64104

[startup+680.072 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 29751
Raw data (/proc/29747/stat): 29747 (minisat+_script) S 29746 29747 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796597668 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29747/statm): 531 226 485 147 0 384 0
[pid=29747] vsize: 2124
Raw data (/proc/29751/stat): 29751 (minisat+_64-bit) R 29747 29747 31778 0 -1 0 15082 0 0 0 67813 90 0 0 25 0 1 0 1796597673 63827968 14568 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/29751/statm): 15583 14568 145 145 0 15438 0
[pid=29751] vsize: 62332
Current children cumulated CPU time (s) 679.04
Current children cumulated vsize (Kb) 64456

[startup+690.072 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 29751
Raw data (/proc/29747/stat): 29747 (minisat+_script) S 29746 29747 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796597668 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29747/statm): 531 226 485 147 0 384 0
[pid=29747] vsize: 2124
Raw data (/proc/29751/stat): 29751 (minisat+_64-bit) R 29747 29747 31778 0 -1 0 15190 0 0 0 68811 91 0 0 25 0 1 0 1796597673 64266240 14676 4294967295 134512640 135094434 3221224432 3221223088 134557813 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/29751/statm): 15690 14676 145 145 0 15545 0
[pid=29751] vsize: 62760
Current children cumulated CPU time (s) 689.03
Current children cumulated vsize (Kb) 64884

[startup+700.073 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 29751
Raw data (/proc/29747/stat): 29747 (minisat+_script) S 29746 29747 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796597668 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29747/statm): 531 226 485 147 0 384 0
[pid=29747] vsize: 2124
Raw data (/proc/29751/stat): 29751 (minisat+_64-bit) R 29747 29747 31778 0 -1 0 15309 0 0 0 69809 92 0 0 25 0 1 0 1796597673 64749568 14795 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/29751/statm): 15808 14795 145 145 0 15663 0
[pid=29751] vsize: 63232
Current children cumulated CPU time (s) 699.02
Current children cumulated vsize (Kb) 65356

[startup+710.074 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 29751
Raw data (/proc/29747/stat): 29747 (minisat+_script) S 29746 29747 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796597668 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29747/statm): 531 226 485 147 0 384 0
[pid=29747] vsize: 2124
Raw data (/proc/29751/stat): 29751 (minisat+_64-bit) R 29747 29747 31778 0 -1 0 15409 0 0 0 70807 93 0 0 25 0 1 0 1796597673 65155072 14895 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/29751/statm): 15907 14895 145 145 0 15762 0
[pid=29751] vsize: 63628
Current children cumulated CPU time (s) 709.01
Current children cumulated vsize (Kb) 65752

[startup+720.075 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 29751
Raw data (/proc/29747/stat): 29747 (minisat+_script) S 29746 29747 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796597668 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29747/statm): 531 226 485 147 0 384 0
[pid=29747] vsize: 2124
Raw data (/proc/29751/stat): 29751 (minisat+_64-bit) R 29747 29747 31778 0 -1 0 15517 0 0 0 71804 94 0 0 25 0 1 0 1796597673 65593344 15003 4294967295 134512640 135094434 3221224432 3221223104 134555574 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/29751/statm): 16014 15003 145 145 0 15869 0
[pid=29751] vsize: 64056
Current children cumulated CPU time (s) 718.99
Current children cumulated vsize (Kb) 66180

[startup+730.077 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 29751
Raw data (/proc/29747/stat): 29747 (minisat+_script) S 29746 29747 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796597668 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29747/statm): 531 226 485 147 0 384 0
[pid=29747] vsize: 2124
Raw data (/proc/29751/stat): 29751 (minisat+_64-bit) R 29747 29747 31778 0 -1 0 15608 0 0 0 72802 96 0 0 25 0 1 0 1796597673 65953792 15094 4294967295 134512640 135094434 3221224432 3221223056 134557642 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/29751/statm): 16102 15094 145 145 0 15957 0
[pid=29751] vsize: 64408
Current children cumulated CPU time (s) 728.99
Current children cumulated vsize (Kb) 66532

[startup+740.077 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 29751
Raw data (/proc/29747/stat): 29747 (minisat+_script) S 29746 29747 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796597668 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29747/statm): 531 226 485 147 0 384 0
[pid=29747] vsize: 2124
Raw data (/proc/29751/stat): 29751 (minisat+_64-bit) R 29747 29747 31778 0 -1 0 15703 0 0 0 73800 97 0 0 25 0 1 0 1796597673 66338816 15189 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/29751/statm): 16196 15189 145 145 0 16051 0
[pid=29751] vsize: 64784
Current children cumulated CPU time (s) 738.98
Current children cumulated vsize (Kb) 66908

[startup+750.077 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 29751
Raw data (/proc/29747/stat): 29747 (minisat+_script) S 29746 29747 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796597668 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29747/statm): 531 226 485 147 0 384 0
[pid=29747] vsize: 2124
Raw data (/proc/29751/stat): 29751 (minisat+_64-bit) R 29747 29747 31778 0 -1 0 15835 0 0 0 74797 98 0 0 25 0 1 0 1796597673 66871296 15321 4294967295 134512640 135094434 3221224432 3221223088 134557950 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29751/statm): 16326 15321 145 145 0 16181 0
[pid=29751] vsize: 65304
Current children cumulated CPU time (s) 748.96
Current children cumulated vsize (Kb) 67428

[startup+760.078 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 29751
Raw data (/proc/29747/stat): 29747 (minisat+_script) S 29746 29747 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796597668 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29747/statm): 531 226 485 147 0 384 0
[pid=29747] vsize: 2124
Raw data (/proc/29751/stat): 29751 (minisat+_64-bit) R 29747 29747 31778 0 -1 0 15958 0 0 0 75794 99 0 0 25 0 1 0 1796597673 67362816 15444 4294967295 134512640 135094434 3221224432 3221223104 134556517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29751/statm): 16446 15444 145 145 0 16301 0
[pid=29751] vsize: 65784
Current children cumulated CPU time (s) 758.94
Current children cumulated vsize (Kb) 67908

[startup+770.079 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 29751
Raw data (/proc/29747/stat): 29747 (minisat+_script) S 29746 29747 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796597668 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29747/statm): 531 226 485 147 0 384 0
[pid=29747] vsize: 2124
Raw data (/proc/29751/stat): 29751 (minisat+_64-bit) R 29747 29747 31778 0 -1 0 16052 0 0 0 76793 100 0 0 25 0 1 0 1796597673 68263936 15538 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29751/statm): 16666 15538 145 145 0 16521 0
[pid=29751] vsize: 66664
Current children cumulated CPU time (s) 768.94
Current children cumulated vsize (Kb) 68788

[startup+780.08 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 29751
Raw data (/proc/29747/stat): 29747 (minisat+_script) S 29746 29747 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796597668 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29747/statm): 531 226 485 147 0 384 0
[pid=29747] vsize: 2124
Raw data (/proc/29751/stat): 29751 (minisat+_64-bit) R 29747 29747 31778 0 -1 0 16142 0 0 0 77791 101 0 0 25 0 1 0 1796597673 68628480 15628 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29751/statm): 16755 15628 145 145 0 16610 0
[pid=29751] vsize: 67020
Current children cumulated CPU time (s) 778.93
Current children cumulated vsize (Kb) 69144

[startup+790.081 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 29751
Raw data (/proc/29747/stat): 29747 (minisat+_script) S 29746 29747 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796597668 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29747/statm): 531 226 485 147 0 384 0
[pid=29747] vsize: 2124
Raw data (/proc/29751/stat): 29751 (minisat+_64-bit) R 29747 29747 31778 0 -1 0 16198 0 0 0 78790 101 0 0 25 0 1 0 1796597673 68849664 15684 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29751/statm): 16809 15684 145 145 0 16664 0
[pid=29751] vsize: 67236
Current children cumulated CPU time (s) 788.92
Current children cumulated vsize (Kb) 69360

[startup+800.081 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 29751
Raw data (/proc/29747/stat): 29747 (minisat+_script) S 29746 29747 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796597668 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29747/statm): 531 226 485 147 0 384 0
[pid=29747] vsize: 2124
Raw data (/proc/29751/stat): 29751 (minisat+_64-bit) R 29747 29747 31778 0 -1 0 16312 0 0 0 79788 102 0 0 25 0 1 0 1796597673 69316608 15798 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29751/statm): 16923 15798 145 145 0 16778 0
[pid=29751] vsize: 67692
Current children cumulated CPU time (s) 798.91
Current children cumulated vsize (Kb) 69816

[startup+810.082 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 29751
Raw data (/proc/29747/stat): 29747 (minisat+_script) S 29746 29747 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796597668 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29747/statm): 531 226 485 147 0 384 0
[pid=29747] vsize: 2124
Raw data (/proc/29751/stat): 29751 (minisat+_64-bit) R 29747 29747 31778 0 -1 0 16402 0 0 0 80786 103 0 0 25 0 1 0 1796597673 69677056 15888 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29751/statm): 17011 15888 145 145 0 16866 0
[pid=29751] vsize: 68044
Current children cumulated CPU time (s) 808.9
Current children cumulated vsize (Kb) 70168

[startup+820.083 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 29751
Raw data (/proc/29747/stat): 29747 (minisat+_script) S 29746 29747 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796597668 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29747/statm): 531 226 485 147 0 384 0
[pid=29747] vsize: 2124
Raw data (/proc/29751/stat): 29751 (minisat+_64-bit) R 29747 29747 31778 0 -1 0 16514 0 0 0 81784 103 0 0 25 0 1 0 1796597673 70131712 16000 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29751/statm): 17122 16000 145 145 0 16977 0
[pid=29751] vsize: 68488
Current children cumulated CPU time (s) 818.88
Current children cumulated vsize (Kb) 70612

[startup+830.084 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 29751
Raw data (/proc/29747/stat): 29747 (minisat+_script) S 29746 29747 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796597668 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29747/statm): 531 226 485 147 0 384 0
[pid=29747] vsize: 2124
Raw data (/proc/29751/stat): 29751 (minisat+_64-bit) R 29747 29747 31778 0 -1 0 16675 0 0 0 82783 104 0 0 25 0 1 0 1796597673 70791168 16161 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29751/statm): 17283 16161 145 145 0 17138 0
[pid=29751] vsize: 69132
Current children cumulated CPU time (s) 828.88
Current children cumulated vsize (Kb) 71256

[startup+840.085 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 29751
Raw data (/proc/29747/stat): 29747 (minisat+_script) S 29746 29747 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796597668 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29747/statm): 531 226 485 147 0 384 0
[pid=29747] vsize: 2124
Raw data (/proc/29751/stat): 29751 (minisat+_64-bit) R 29747 29747 31778 0 -1 0 16849 0 0 0 83779 105 0 0 25 0 1 0 1796597673 71499776 16335 4294967295 134512640 135094434 3221224432 3221223056 134562104 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29751/statm): 17456 16335 145 145 0 17311 0
[pid=29751] vsize: 69824
Current children cumulated CPU time (s) 838.85
Current children cumulated vsize (Kb) 71948

[startup+850.086 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 29751
Raw data (/proc/29747/stat): 29747 (minisat+_script) S 29746 29747 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796597668 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29747/statm): 531 226 485 147 0 384 0
[pid=29747] vsize: 2124
Raw data (/proc/29751/stat): 29751 (minisat+_64-bit) R 29747 29747 31778 0 -1 0 17040 0 0 0 84775 107 0 0 25 0 1 0 1796597673 72273920 16526 4294967295 134512640 135094434 3221224432 3221223088 134558187 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29751/statm): 17645 16526 145 145 0 17500 0
[pid=29751] vsize: 70580
Current children cumulated CPU time (s) 848.83
Current children cumulated vsize (Kb) 72704

[startup+860.086 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 29751
Raw data (/proc/29747/stat): 29747 (minisat+_script) S 29746 29747 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796597668 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29747/statm): 531 226 485 147 0 384 0
[pid=29747] vsize: 2124
Raw data (/proc/29751/stat): 29751 (minisat+_64-bit) R 29747 29747 31778 0 -1 0 17133 0 0 0 85773 108 0 0 25 0 1 0 1796597673 72650752 16619 4294967295 134512640 135094434 3221224432 3221223088 134557903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29751/statm): 17737 16619 145 145 0 17592 0
[pid=29751] vsize: 70948
Current children cumulated CPU time (s) 858.82
Current children cumulated vsize (Kb) 73072

[startup+870.086 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 29751
Raw data (/proc/29747/stat): 29747 (minisat+_script) S 29746 29747 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796597668 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29747/statm): 531 226 485 147 0 384 0
[pid=29747] vsize: 2124
Raw data (/proc/29751/stat): 29751 (minisat+_64-bit) R 29747 29747 31778 0 -1 0 17255 0 0 0 86772 108 0 0 25 0 1 0 1796597673 73138176 16741 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29751/statm): 17856 16741 145 145 0 17711 0
[pid=29751] vsize: 71424
Current children cumulated CPU time (s) 868.81
Current children cumulated vsize (Kb) 73548

[startup+880.087 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 29751
Raw data (/proc/29747/stat): 29747 (minisat+_script) S 29746 29747 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796597668 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29747/statm): 531 226 485 147 0 384 0
[pid=29747] vsize: 2124
Raw data (/proc/29751/stat): 29751 (minisat+_64-bit) R 29747 29747 31778 0 -1 0 17351 0 0 0 87770 109 0 0 25 0 1 0 1796597673 73519104 16837 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29751/statm): 17949 16837 145 145 0 17804 0
[pid=29751] vsize: 71796
Current children cumulated CPU time (s) 878.8
Current children cumulated vsize (Kb) 73920

[startup+890.088 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 29751
Raw data (/proc/29747/stat): 29747 (minisat+_script) S 29746 29747 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796597668 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29747/statm): 531 226 485 147 0 384 0
[pid=29747] vsize: 2124
Raw data (/proc/29751/stat): 29751 (minisat+_64-bit) R 29747 29747 31778 0 -1 0 17479 0 0 0 88769 110 0 0 25 0 1 0 1796597673 74043392 16965 4294967295 134512640 135094434 3221224432 3221223088 134557950 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29751/statm): 18077 16965 145 145 0 17932 0
[pid=29751] vsize: 72308
Current children cumulated CPU time (s) 888.8
Current children cumulated vsize (Kb) 74432

[startup+900.088 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 29751
Raw data (/proc/29747/stat): 29747 (minisat+_script) S 29746 29747 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796597668 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29747/statm): 531 226 485 147 0 384 0
[pid=29747] vsize: 2124
Raw data (/proc/29751/stat): 29751 (minisat+_64-bit) R 29747 29747 31778 0 -1 0 17552 0 0 0 89768 110 0 0 25 0 1 0 1796597673 74338304 17038 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29751/statm): 18149 17038 145 145 0 18004 0
[pid=29751] vsize: 72596
Current children cumulated CPU time (s) 898.79
Current children cumulated vsize (Kb) 74720

[startup+910.088 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 29751
Raw data (/proc/29747/stat): 29747 (minisat+_script) S 29746 29747 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796597668 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29747/statm): 531 226 485 147 0 384 0
[pid=29747] vsize: 2124
Raw data (/proc/29751/stat): 29751 (minisat+_64-bit) R 29747 29747 31778 0 -1 0 17668 0 0 0 90766 111 0 0 25 0 1 0 1796597673 74801152 17154 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29751/statm): 18262 17154 145 145 0 18117 0
[pid=29751] vsize: 73048
Current children cumulated CPU time (s) 908.78
Current children cumulated vsize (Kb) 75172

[startup+920.089 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 29751
Raw data (/proc/29747/stat): 29747 (minisat+_script) S 29746 29747 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796597668 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29747/statm): 531 226 485 147 0 384 0
[pid=29747] vsize: 2124
Raw data (/proc/29751/stat): 29751 (minisat+_64-bit) R 29747 29747 31778 0 -1 0 17887 0 0 0 91762 112 0 0 25 0 1 0 1796597673 75702272 17373 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/29751/statm): 18482 17373 145 145 0 18337 0
[pid=29751] vsize: 73928
Current children cumulated CPU time (s) 918.75
Current children cumulated vsize (Kb) 76052

[startup+930.09 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 29751
Raw data (/proc/29747/stat): 29747 (minisat+_script) S 29746 29747 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796597668 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29747/statm): 531 226 485 147 0 384 0
[pid=29747] vsize: 2124
Raw data (/proc/29751/stat): 29751 (minisat+_64-bit) R 29747 29747 31778 0 -1 0 17981 0 0 0 92760 114 0 0 25 0 1 0 1796597673 76087296 17467 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/29751/statm): 18576 17467 145 145 0 18431 0
[pid=29751] vsize: 74304
Current children cumulated CPU time (s) 928.75
Current children cumulated vsize (Kb) 76428

[startup+940.091 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 29751
Raw data (/proc/29747/stat): 29747 (minisat+_script) S 29746 29747 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796597668 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29747/statm): 531 226 485 147 0 384 0
[pid=29747] vsize: 2124
Raw data (/proc/29751/stat): 29751 (minisat+_64-bit) R 29747 29747 31778 0 -1 0 18057 0 0 0 93759 114 0 0 25 0 1 0 1796597673 76394496 17543 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29751/statm): 18651 17543 145 145 0 18506 0
[pid=29751] vsize: 74604
Current children cumulated CPU time (s) 938.74
Current children cumulated vsize (Kb) 76728

[startup+950.092 s]
Raw data (loadavg): 0.99 0.98 0.99 1/57 29751
Raw data (/proc/29747/stat): 29747 (minisat+_script) S 29746 29747 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796597668 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29747/statm): 531 226 485 147 0 384 0
[pid=29747] vsize: 2124
Raw data (/proc/29751/stat): 29751 (minisat+_64-bit) T 29747 29747 31778 0 -1 0 18141 0 0 0 94757 115 0 0 25 0 1 0 1796597673 76730368 17627 4294967295 134512640 135094434 3221224432 3221222796 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/29751/statm): 18733 17627 145 145 0 18588 0
[pid=29751] vsize: 74932
Current children cumulated CPU time (s) 948.73
Current children cumulated vsize (Kb) 77056

[startup+960.093 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 29751
Raw data (/proc/29747/stat): 29747 (minisat+_script) S 29746 29747 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796597668 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29747/statm): 531 226 485 147 0 384 0
[pid=29747] vsize: 2124
Raw data (/proc/29751/stat): 29751 (minisat+_64-bit) R 29747 29747 31778 0 -1 0 18222 0 0 0 95756 116 0 0 25 0 1 0 1796597673 77058048 17708 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29751/statm): 18813 17708 145 145 0 18668 0
[pid=29751] vsize: 75252
Current children cumulated CPU time (s) 958.73
Current children cumulated vsize (Kb) 77376

[startup+970.093 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 29751
Raw data (/proc/29747/stat): 29747 (minisat+_script) S 29746 29747 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796597668 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29747/statm): 531 226 485 147 0 384 0
[pid=29747] vsize: 2124
Raw data (/proc/29751/stat): 29751 (minisat+_64-bit) R 29747 29747 31778 0 -1 0 18297 0 0 0 96754 116 0 0 25 0 1 0 1796597673 77361152 17783 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29751/statm): 18887 17783 145 145 0 18742 0
[pid=29751] vsize: 75548
Current children cumulated CPU time (s) 968.71
Current children cumulated vsize (Kb) 77672

[startup+980.095 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 29751
Raw data (/proc/29747/stat): 29747 (minisat+_script) S 29746 29747 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796597668 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29747/statm): 531 226 485 147 0 384 0
[pid=29747] vsize: 2124
Raw data (/proc/29751/stat): 29751 (minisat+_64-bit) R 29747 29747 31778 0 -1 0 18387 0 0 0 97753 117 0 0 25 0 1 0 1796597673 77725696 17873 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29751/statm): 18976 17873 145 145 0 18831 0
[pid=29751] vsize: 75904
Current children cumulated CPU time (s) 978.71
Current children cumulated vsize (Kb) 78028

[startup+990.096 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 29751
Raw data (/proc/29747/stat): 29747 (minisat+_script) S 29746 29747 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796597668 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29747/statm): 531 226 485 147 0 384 0
[pid=29747] vsize: 2124
Raw data (/proc/29751/stat): 29751 (minisat+_64-bit) R 29747 29747 31778 0 -1 0 18459 0 0 0 98752 117 0 0 25 0 1 0 1796597673 78012416 17945 4294967295 134512640 135094434 3221224432 3221223088 134558295 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29751/statm): 19046 17945 145 145 0 18901 0
[pid=29751] vsize: 76184
Current children cumulated CPU time (s) 988.7
Current children cumulated vsize (Kb) 78308

[startup+1000.1 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 29751
Raw data (/proc/29747/stat): 29747 (minisat+_script) S 29746 29747 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796597668 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29747/statm): 531 226 485 147 0 384 0
[pid=29747] vsize: 2124
Raw data (/proc/29751/stat): 29751 (minisat+_64-bit) R 29747 29747 31778 0 -1 0 18625 0 0 0 99749 118 0 0 25 0 1 0 1796597673 78696448 18111 4294967295 134512640 135094434 3221224432 3221223088 134558181 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29751/statm): 19213 18111 145 145 0 19068 0
[pid=29751] vsize: 76852
Current children cumulated CPU time (s) 998.68
Current children cumulated vsize (Kb) 78976

[startup+1010.1 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 29751
Raw data (/proc/29747/stat): 29747 (minisat+_script) S 29746 29747 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796597668 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29747/statm): 531 226 485 147 0 384 0
[pid=29747] vsize: 2124
Raw data (/proc/29751/stat): 29751 (minisat+_64-bit) R 29747 29747 31778 0 -1 0 18691 0 0 0 100748 118 0 0 25 0 1 0 1796597673 78966784 18177 4294967295 134512640 135094434 3221224432 3221223024 134557219 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29751/statm): 19279 18177 145 145 0 19134 0
[pid=29751] vsize: 77116
Current children cumulated CPU time (s) 1008.67
Current children cumulated vsize (Kb) 79240

[startup+1020.1 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 29751
Raw data (/proc/29747/stat): 29747 (minisat+_script) S 29746 29747 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796597668 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29747/statm): 531 226 485 147 0 384 0
[pid=29747] vsize: 2124
Raw data (/proc/29751/stat): 29751 (minisat+_64-bit) R 29747 29747 31778 0 -1 0 18789 0 0 0 101747 119 0 0 25 0 1 0 1796597673 79376384 18275 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29751/statm): 19379 18275 145 145 0 19234 0
[pid=29751] vsize: 77516
Current children cumulated CPU time (s) 1018.67
Current children cumulated vsize (Kb) 79640

[startup+1030.1 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 29751
Raw data (/proc/29747/stat): 29747 (minisat+_script) S 29746 29747 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796597668 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29747/statm): 531 226 485 147 0 384 0
[pid=29747] vsize: 2124
Raw data (/proc/29751/stat): 29751 (minisat+_64-bit) R 29747 29747 31778 0 -1 0 18865 0 0 0 102746 119 0 0 25 0 1 0 1796597673 79708160 18351 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29751/statm): 19460 18351 145 145 0 19315 0
[pid=29751] vsize: 77840
Current children cumulated CPU time (s) 1028.66
Current children cumulated vsize (Kb) 79964

[startup+1040.1 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 29751
Raw data (/proc/29747/stat): 29747 (minisat+_script) S 29746 29747 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796597668 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29747/statm): 531 226 485 147 0 384 0
[pid=29747] vsize: 2124
Raw data (/proc/29751/stat): 29751 (minisat+_64-bit) R 29747 29747 31778 0 -1 0 18936 0 0 0 103746 119 0 0 25 0 1 0 1796597673 80003072 18422 4294967295 134512640 135094434 3221224432 3221223084 134558255 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29751/statm): 19532 18422 145 145 0 19387 0
[pid=29751] vsize: 78128
Current children cumulated CPU time (s) 1038.66
Current children cumulated vsize (Kb) 80252

[startup+1050.1 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 29751
Raw data (/proc/29747/stat): 29747 (minisat+_script) S 29746 29747 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796597668 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29747/statm): 531 226 485 147 0 384 0
[pid=29747] vsize: 2124
Raw data (/proc/29751/stat): 29751 (minisat+_64-bit) R 29747 29747 31778 0 -1 0 18994 0 0 0 104745 119 0 0 25 0 1 0 1796597673 80248832 18480 4294967295 134512640 135094434 3221224432 3221223092 134553508 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29751/statm): 19592 18480 145 145 0 19447 0
[pid=29751] vsize: 78368
Current children cumulated CPU time (s) 1048.65
Current children cumulated vsize (Kb) 80492

[startup+1060.1 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 29751
Raw data (/proc/29747/stat): 29747 (minisat+_script) S 29746 29747 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796597668 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29747/statm): 531 226 485 147 0 384 0
[pid=29747] vsize: 2124
Raw data (/proc/29751/stat): 29751 (minisat+_64-bit) R 29747 29747 31778 0 -1 0 19101 0 0 0 105744 120 0 0 25 0 1 0 1796597673 80678912 18587 4294967295 134512640 135094434 3221224432 3221223104 134556082 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29751/statm): 19697 18587 145 145 0 19552 0
[pid=29751] vsize: 78788
Current children cumulated CPU time (s) 1058.65
Current children cumulated vsize (Kb) 80912

[startup+1070.1 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 29751
Raw data (/proc/29747/stat): 29747 (minisat+_script) S 29746 29747 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796597668 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29747/statm): 531 226 485 147 0 384 0
[pid=29747] vsize: 2124
Raw data (/proc/29751/stat): 29751 (minisat+_64-bit) R 29747 29747 31778 0 -1 0 19170 0 0 0 106743 121 0 0 25 0 1 0 1796597673 80953344 18656 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29751/statm): 19764 18656 145 145 0 19619 0
[pid=29751] vsize: 79056
Current children cumulated CPU time (s) 1068.65
Current children cumulated vsize (Kb) 81180

[startup+1080.1 s]
Raw data (loadavg): 0.99 0.98 0.99 1/57 29751
Raw data (/proc/29747/stat): 29747 (minisat+_script) S 29746 29747 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796597668 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29747/statm): 531 226 485 147 0 384 0
[pid=29747] vsize: 2124
Raw data (/proc/29751/stat): 29751 (minisat+_64-bit) T 29747 29747 31778 0 -1 0 19252 0 0 0 107740 122 0 0 25 0 1 0 1796597673 81281024 18738 4294967295 134512640 135094434 3221224432 3221222796 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/29751/statm): 19844 18738 145 145 0 19699 0
[pid=29751] vsize: 79376
Current children cumulated CPU time (s) 1078.63
Current children cumulated vsize (Kb) 81500

[startup+1090.1 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 29751
Raw data (/proc/29747/stat): 29747 (minisat+_script) S 29746 29747 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796597668 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29747/statm): 531 226 485 147 0 384 0
[pid=29747] vsize: 2124
Raw data (/proc/29751/stat): 29751 (minisat+_64-bit) R 29747 29747 31778 0 -1 0 19331 0 0 0 108738 123 0 0 25 0 1 0 1796597673 81600512 18817 4294967295 134512640 135094434 3221224432 3221223088 134558221 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29751/statm): 19922 18817 145 145 0 19777 0
[pid=29751] vsize: 79688
Current children cumulated CPU time (s) 1088.62
Current children cumulated vsize (Kb) 81812

[startup+1100.1 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 29751
Raw data (/proc/29747/stat): 29747 (minisat+_script) S 29746 29747 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796597668 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29747/statm): 531 226 485 147 0 384 0
[pid=29747] vsize: 2124
Raw data (/proc/29751/stat): 29751 (minisat+_64-bit) R 29747 29747 31778 0 -1 0 19387 0 0 0 109737 123 0 0 25 0 1 0 1796597673 81825792 18873 4294967295 134512640 135094434 3221224432 3221223136 134558999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29751/statm): 19977 18873 145 145 0 19832 0
[pid=29751] vsize: 79908
Current children cumulated CPU time (s) 1098.61
Current children cumulated vsize (Kb) 82032

[startup+1110.1 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 29751
Raw data (/proc/29747/stat): 29747 (minisat+_script) S 29746 29747 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796597668 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29747/statm): 531 226 485 147 0 384 0
[pid=29747] vsize: 2124
Raw data (/proc/29751/stat): 29751 (minisat+_64-bit) R 29747 29747 31778 0 -1 0 19464 0 0 0 110736 124 0 0 25 0 1 0 1796597673 82137088 18950 4294967295 134512640 135094434 3221224432 3221223088 134557823 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29751/statm): 20053 18950 145 145 0 19908 0
[pid=29751] vsize: 80212
Current children cumulated CPU time (s) 1108.61
Current children cumulated vsize (Kb) 82336

[startup+1120.11 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 29751
Raw data (/proc/29747/stat): 29747 (minisat+_script) S 29746 29747 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796597668 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29747/statm): 531 226 485 147 0 384 0
[pid=29747] vsize: 2124
Raw data (/proc/29751/stat): 29751 (minisat+_64-bit) R 29747 29747 31778 0 -1 0 19520 0 0 0 111736 124 0 0 25 0 1 0 1796597673 82366464 19006 4294967295 134512640 135094434 3221224432 3221223056 134557696 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29751/statm): 20109 19006 145 145 0 19964 0
[pid=29751] vsize: 80436
Current children cumulated CPU time (s) 1118.61
Current children cumulated vsize (Kb) 82560

[startup+1130.11 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 29751
Raw data (/proc/29747/stat): 29747 (minisat+_script) S 29746 29747 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796597668 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29747/statm): 531 226 485 147 0 384 0
[pid=29747] vsize: 2124
Raw data (/proc/29751/stat): 29751 (minisat+_64-bit) R 29747 29747 31778 0 -1 0 19602 0 0 0 112734 125 0 0 25 0 1 0 1796597673 82698240 19088 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29751/statm): 20190 19088 145 145 0 20045 0
[pid=29751] vsize: 80760
Current children cumulated CPU time (s) 1128.6
Current children cumulated vsize (Kb) 82884

[startup+1140.11 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 29751
Raw data (/proc/29747/stat): 29747 (minisat+_script) S 29746 29747 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796597668 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29747/statm): 531 226 485 147 0 384 0
[pid=29747] vsize: 2124
Raw data (/proc/29751/stat): 29751 (minisat+_64-bit) R 29747 29747 31778 0 -1 0 19674 0 0 0 113733 125 0 0 25 0 1 0 1796597673 82984960 19160 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29751/statm): 20260 19160 145 145 0 20115 0
[pid=29751] vsize: 81040
Current children cumulated CPU time (s) 1138.59
Current children cumulated vsize (Kb) 83164

[startup+1150.11 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 29751
Raw data (/proc/29747/stat): 29747 (minisat+_script) S 29746 29747 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796597668 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29747/statm): 531 226 485 147 0 384 0
[pid=29747] vsize: 2124
Raw data (/proc/29751/stat): 29751 (minisat+_64-bit) R 29747 29747 31778 0 -1 0 19739 0 0 0 114732 126 0 0 25 0 1 0 1796597673 83243008 19225 4294967295 134512640 135094434 3221224432 3221223064 134557561 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29751/statm): 20323 19225 145 145 0 20178 0
[pid=29751] vsize: 81292
Current children cumulated CPU time (s) 1148.59
Current children cumulated vsize (Kb) 83416

[startup+1160.11 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 29751
Raw data (/proc/29747/stat): 29747 (minisat+_script) S 29746 29747 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796597668 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29747/statm): 531 226 485 147 0 384 0
[pid=29747] vsize: 2124
Raw data (/proc/29751/stat): 29751 (minisat+_64-bit) R 29747 29747 31778 0 -1 0 19812 0 0 0 115731 127 0 0 25 0 1 0 1796597673 83537920 19298 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29751/statm): 20395 19298 145 145 0 20250 0
[pid=29751] vsize: 81580
Current children cumulated CPU time (s) 1158.59
Current children cumulated vsize (Kb) 83704

[startup+1170.11 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 29751
Raw data (/proc/29747/stat): 29747 (minisat+_script) S 29746 29747 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796597668 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29747/statm): 531 226 485 147 0 384 0
[pid=29747] vsize: 2124
Raw data (/proc/29751/stat): 29751 (minisat+_64-bit) R 29747 29747 31778 0 -1 0 19909 0 0 0 116729 127 0 0 25 0 1 0 1796597673 83922944 19395 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29751/statm): 20489 19395 145 145 0 20344 0
[pid=29751] vsize: 81956
Current children cumulated CPU time (s) 1168.57
Current children cumulated vsize (Kb) 84080

[startup+1180.11 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 29751
Raw data (/proc/29747/stat): 29747 (minisat+_script) S 29746 29747 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796597668 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29747/statm): 531 226 485 147 0 384 0
[pid=29747] vsize: 2124
Raw data (/proc/29751/stat): 29751 (minisat+_64-bit) R 29747 29747 31778 0 -1 0 19994 0 0 0 117727 129 0 0 25 0 1 0 1796597673 84267008 19480 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29751/statm): 20573 19480 145 145 0 20428 0
[pid=29751] vsize: 82292
Current children cumulated CPU time (s) 1178.57
Current children cumulated vsize (Kb) 84416

[startup+1190.11 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 29751
Raw data (/proc/29747/stat): 29747 (minisat+_script) S 29746 29747 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796597668 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29747/statm): 531 226 485 147 0 384 0
[pid=29747] vsize: 2124
Raw data (/proc/29751/stat): 29751 (minisat+_64-bit) R 29747 29747 31778 0 -1 0 20060 0 0 0 118726 129 0 0 25 0 1 0 1796597673 84533248 19546 4294967295 134512640 135094434 3221224432 3221223080 134558258 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29751/statm): 20638 19546 145 145 0 20493 0
[pid=29751] vsize: 82552
Current children cumulated CPU time (s) 1188.56
Current children cumulated vsize (Kb) 84676

[startup+1200.11 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 29751
Raw data (/proc/29747/stat): 29747 (minisat+_script) S 29746 29747 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796597668 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29747/statm): 531 226 485 147 0 384 0
[pid=29747] vsize: 2124
Raw data (/proc/29751/stat): 29751 (minisat+_64-bit) R 29747 29747 31778 0 -1 0 20150 0 0 0 119725 129 0 0 25 0 1 0 1796597673 84885504 19636 4294967295 134512640 135094434 3221224432 3221223056 134557696 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29751/statm): 20724 19636 145 145 0 20579 0
[pid=29751] vsize: 82896
Current children cumulated CPU time (s) 1198.55
Current children cumulated vsize (Kb) 85020

[startup+1210.11 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 29751
Raw data (/proc/29747/stat): 29747 (minisat+_script) S 29746 29747 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796597668 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29747/statm): 531 226 485 147 0 384 0
[pid=29747] vsize: 2124
Raw data (/proc/29751/stat): 29751 (minisat+_64-bit) R 29747 29747 31778 0 -1 0 20229 0 0 0 120724 129 0 0 25 0 1 0 1796597673 85213184 19715 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29751/statm): 20804 19715 145 145 0 20659 0
[pid=29751] vsize: 83216
Current children cumulated CPU time (s) 1208.54
Current children cumulated vsize (Kb) 85340



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.11 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 29751
Raw data (/proc/29747/stat): 29747 (minisat+_script) S 29746 29747 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796597668 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29747/statm): 531 226 485 147 0 384 0
[pid=29747] vsize: 2124
Raw data (/proc/29751/stat): 29751 (minisat+_64-bit) R 29747 29747 31778 0 -1 0 20229 0 0 0 120725 129 0 0 25 0 1 0 1796597673 85213184 19715 4294967295 134512640 135094434 3221224432 3221223056 134557717 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29751/statm): 20804 19715 145 145 0 20659 0
[pid=29751] vsize: 83216
Current children cumulated CPU time (s) 1208.55
Current children cumulated vsize (Kb) 85340

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

Child status: 0
Real time (s): 1210.15
CPU time (s): 1208.59
CPU user time (s): 1207.25
CPU system time (s): 1.3368
CPU usage (%): 99.8706
Max. virtual memory (cumulated for all children) (Kb): 85340

Verifier Data

ERROR: no interpretation found !