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

Nameweb/www.ps.uni-sb.de/~walser/benchmarks/course-ass/normalized-ws97-3.opb
MD5SUM77c89bda49ebcdc0428e1292512864a9
Bench Categoryoptimization, medium integers (OPTMEDINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function 3080
Optimality of the best value was proved NO
Number of terms in the objective function 2792
Biggest coefficient in the objective function 1000
Number of bits for the biggest coefficient in the objective function 10
Sum of the numbers in the objective function 1385986
Number of bits of the sum of numbers in the objective function 21
Biggest number in a constraint 1000
Number of bits of the biggest number in a constraint 10
Biggest sum of numbers in a constraint 1385986
Number of bits of the biggest sum of numbers21
Best result obtained on this benchmarkSAT
Best CPU time to get the best result obtained on this benchmark1.12383
Number of variables3300
Total number of constraints5284
Number of constraints which are clauses1364
Number of constraints which are cardinality constraints (but not clauses)3920
Number of constraints which are nor clauses,nor cardinality constraints0
Minimum length of a constraint1
Maximum length of a constraint220

Trace number 2342

Launcher Data

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

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        916520 kB
Buffers:         35368 kB
Cached:          56012 kB
SwapCached:        896 kB
Active:          66176 kB
Inactive:        27864 kB
HighTotal:      131008 kB
HighFree:        73556 kB
LowTotal:       903652 kB
LowFree:        842964 kB
SwapTotal:     2097892 kB
SwapFree:      2096496 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5716 kB
Slab:            18660 kB
Committed_AS:    64168 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-09-18 19:25:48 (client local time) WITH STATUS 0 IN 1207.44 SECONDS
stats: 2727 7 1207.44 0

Solver Data

c Parsing PB file...
c Converting 2572 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ############################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################
c   -- Clauses(.)/Splits(s): ....................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ---[2571]---> Adder-cost: 418   maxlim: 156   bits: 8/8
c ---[2570]---> Adder-cost: 418   maxlim: 156   bits: 8/8
c ---[2569]---> Adder-cost: 418   maxlim: 156   bits: 8/8
c ---[2568]---> Adder-cost: 418   maxlim: 156   bits: 8/8
c ---[2567]---> Adder-cost: 430   maxlim: 193   bits: 8/8
c ---[2566]---> Adder-cost: 430   maxlim: 193   bits: 8/8
c ---[2565]---> Adder-cost: 430   maxlim: 193   bits: 8/8
c ---[2564]---> Adder-cost: 430   maxlim: 193   bits: 8/8
c ---[2563]---> Adder-cost: 430   maxlim: 193   bits: 8/8
c ---[2562]---> Adder-cost: 430   maxlim: 193   bits: 8/8
c ---[2561]---> Adder-cost: 430   maxlim: 193   bits: 8/8
c ---[2560]---> Adder-cost: 430   maxlim: 193   bits: 8/8
c ---[2559]---> Adder-cost: 430   maxlim: 193   bits: 8/8
c ---[2558]---> Adder-cost: 298   maxlim: 96   bits: 8/7
c ---[2557]---> Adder-cost: 298   maxlim: 96   bits: 8/7
c ---[2556]---> Adder-cost: 298   maxlim: 96   bits: 8/7
c ---[2555]---> Adder-cost: 11   maxlim: 41   bits: 7/6
c ---[2554]---> Adder-cost: 11   maxlim: 41   bits: 7/6
c ---[2553]---> Adder-cost: 11   maxlim: 41   bits: 7/6
c ---[2552]---> Adder-cost: 11   maxlim: 41   bits: 7/6
c ---[2551]---> Adder-cost: 58   maxlim: 18   bits: 6/5
c ---[2550]---> Adder-cost: 58   maxlim: 18   bits: 6/5
c ---[2549]---> Adder-cost: 58   maxlim: 18   bits: 6/5
c ---[2548]---> Adder-cost: 58   maxlim: 18   bits: 6/5
c ---[2547]---> Adder-cost: 58   maxlim: 18   bits: 6/5
c ---[2546]---> Adder-cost: 58   maxlim: 18   bits: 6/5
c ---[2545]---> Adder-cost: 58   maxlim: 18   bits: 6/5
c ---[2544]---> Adder-cost: 58   maxlim: 18   bits: 6/5
c ---[2543]---> Adder-cost: 58   maxlim: 18   bits: 6/5
c ---[2542]---> Adder-cost: 28   maxlim: 39   bits: 7/6
c ---[2541]---> Adder-cost: 28   maxlim: 39   bits: 7/6
c ---[2540]---> Adder-cost: 28   maxlim: 39   bits: 7/6
c ---[2538]---> BDD-cost:    5
c ---[2536]---> BDD-cost:   15
c ---[2534]---> BDD-cost:    3
c ---[2532]---> BDD-cost:    5
c ---[2530]---> BDD-cost:   15
c ---[2528]---> BDD-cost:    3
c ---[2526]---> BDD-cost:    5
c ---[2524]---> BDD-cost:   15
c ---[2522]---> BDD-cost:    5
c ---[2520]---> BDD-cost:   15
c ---[2518]---> BDD-cost:    3
c ---[2516]---> BDD-cost:    5
c ---[2514]---> BDD-cost:   15
c ---[2512]---> BDD-cost:    3
c ---[2510]---> BDD-cost:    5
c ---[2508]---> BDD-cost:   15
c ---[2506]---> BDD-cost:    3
c ---[2504]---> BDD-cost:    5
c ---[2502]---> BDD-cost:   15
c ---[2500]---> BDD-cost:    3
c ---[2498]---> BDD-cost:    5
c ---[2496]---> BDD-cost:   15
c ---[2494]---> BDD-cost:    3
c ---[2492]---> BDD-cost:   15
c ---[2490]---> BDD-cost:    3
c ---[2488]---> BDD-cost:    5
c ---[2486]---> BDD-cost:   15
c ---[2484]---> BDD-cost:    5
c ---[2482]---> BDD-cost:   15
c ---[2480]---> BDD-cost:    3
c ---[2478]---> BDD-cost:    5
c ---[2476]---> BDD-cost:   15
c ---[2474]---> BDD-cost:    3
c ---[2472]---> BDD-cost:    5
c ---[2470]---> BDD-cost:   15
c ---[2468]---> BDD-cost:    3
c ---[2466]---> BDD-cost:    5
c ---[2464]---> BDD-cost:   15
c ---[2462]---> BDD-cost:    3
c ---[2460]---> BDD-cost:    5
c ---[2458]---> BDD-cost:   15
c ---[2456]---> BDD-cost:    5
c ---[2454]---> BDD-cost:   15
c ---[2452]---> BDD-cost:    3
c ---[2450]---> BDD-cost:    5
c ---[2448]---> BDD-cost:   15
c ---[2446]---> BDD-cost:    3
c ---[2444]---> BDD-cost:   15
c ---[2442]---> BDD-cost:    5
c ---[2440]---> BDD-cost:   15
c ---[2438]---> BDD-cost:    3
c ---[2436]---> BDD-cost:    5
c ---[2434]---> BDD-cost:   15
c ---[2432]---> BDD-cost:    3
c ---[2430]---> BDD-cost:    5
c ---[2428]---> BDD-cost:   15
c ---[2426]---> BDD-cost:    3
c ---[2424]---> BDD-cost:    5
c ---[2422]---> BDD-cost:   15
c ---[2420]---> BDD-cost:    5
c ---[2418]---> BDD-cost:   15
c ---[2416]---> BDD-cost:    3
c ---[2414]---> BDD-cost:    5
c ---[2412]---> BDD-cost:   15
c ---[2410]---> BDD-cost:    3
c ---[2408]---> BDD-cost:    5
c ---[2406]---> BDD-cost:   15
c ---[2404]---> BDD-cost:    5
c ---[2402]---> BDD-cost:   15
c ---[2400]---> BDD-cost:    3
c ---[2398]---> BDD-cost:    5
c ---[2396]---> BDD-cost:   15
c ---[2394]---> BDD-cost:    5
c ---[2392]---> BDD-cost:   15
c ---[2390]---> BDD-cost:    5
c ---[2388]---> BDD-cost:   15
c ---[2386]---> BDD-cost:    3
c ---[2384]---> BDD-cost:    5
c ---[2382]---> BDD-cost:   15
c ---[2380]---> BDD-cost:    3
c ---[2378]---> BDD-cost:    5
c ---[2376]---> BDD-cost:   15
c ---[2374]---> BDD-cost:    3
c ---[2372]---> BDD-cost:    5
c ---[2370]---> BDD-cost:   15
c ---[2368]---> BDD-cost:    3
c ---[2366]---> BDD-cost:    5
c ---[2364]---> BDD-cost:   15
c ---[2362]---> BDD-cost:    5
c ---[2360]---> BDD-cost:   15
c ---[2358]---> BDD-cost:    5
c ---[2356]---> BDD-cost:   15
c ---[2354]---> BDD-cost:    5
c ---[2352]---> BDD-cost:   15
c ---[2350]---> BDD-cost:    3
c ---[2348]---> BDD-cost:    5
c ---[2346]---> BDD-cost:   15
c ---[2344]---> BDD-cost:    5
c ---[2342]---> BDD-cost:   15
c ---[2340]---> BDD-cost:    3
c ---[2338]---> BDD-cost:    5
c ---[2336]---> BDD-cost:   15
c ---[2334]---> BDD-cost:    5
c ---[2332]---> BDD-cost:   15
c ---[2330]---> BDD-cost:    3
c ---[2328]---> BDD-cost:    5
c ---[2326]---> BDD-cost:   15
c ---[2324]---> BDD-cost:    3
c ---[2322]---> BDD-cost:    5
c ---[2320]---> BDD-cost:   15
c ---[2318]---> BDD-cost:    5
c ---[2316]---> BDD-cost:   15
c ---[2314]---> BDD-cost:    3
c ---[2312]---> BDD-cost:    5
c ---[2310]---> BDD-cost:   15
c ---[2308]---> BDD-cost:    3
c ---[2306]---> BDD-cost:    5
c ---[2304]---> BDD-cost:   15
c ---[2302]---> BDD-cost:    5
c ---[2300]---> BDD-cost:   15
c ---[2298]---> BDD-cost:    5
c ---[2296]---> BDD-cost:   15
c ---[2294]---> BDD-cost:    3
c ---[2292]---> BDD-cost:    5
c ---[2290]---> BDD-cost:   15
c ---[2288]---> BDD-cost:    5
c ---[2286]---> BDD-cost:   15
c ---[2284]---> BDD-cost:    5
c ---[2282]---> BDD-cost:   15
c ---[2280]---> BDD-cost:    5
c ---[2278]---> BDD-cost:   15
c ---[2276]---> BDD-cost:    3
c ---[2274]---> BDD-cost:    5
c ---[2272]---> BDD-cost:   15
c ---[2270]---> BDD-cost:    3
c ---[2268]---> BDD-cost:    5
c ---[2266]---> BDD-cost:   15
c ---[2264]---> BDD-cost:    5
c ---[2262]---> BDD-cost:   15
c ---[2260]---> BDD-cost:    5
c ---[2258]---> BDD-cost:   15
c ---[2256]---> BDD-cost:    5
c ---[2254]---> BDD-cost:   15
c ---[2252]---> BDD-cost:    3
c ---[2250]---> BDD-cost:    5
c ---[2248]---> BDD-cost:   15
c ---[2246]---> BDD-cost:    3
c ---[2244]---> BDD-cost:    5
c ---[2242]---> BDD-cost:   15
c ---[2240]---> BDD-cost:    3
c ---[2238]---> BDD-cost:    5
c ---[2236]---> BDD-cost:   15
c ---[2234]---> BDD-cost:    5
c ---[2232]---> BDD-cost:   15
c ---[2230]---> BDD-cost:    3
c ---[2228]---> BDD-cost:    5
c ---[2226]---> BDD-cost:   15
c ---[2224]---> BDD-cost:    5
c ---[2222]---> BDD-cost:   15
c ---[2220]---> BDD-cost:    3
c ---[2218]---> BDD-cost:    5
c ---[2216]---> BDD-cost:   15
c ---[2214]---> BDD-cost:    3
c ---[2212]---> BDD-cost:    5
c ---[2210]---> BDD-cost:   15
c ---[2208]---> BDD-cost:    3
c ---[2206]---> BDD-cost:    5
c ---[2204]---> BDD-cost:   15
c ---[2202]---> BDD-cost:    3
c ---[2200]---> BDD-cost:    5
c ---[2198]---> BDD-cost:   15
c ---[2196]---> BDD-cost:    5
c ---[2194]---> BDD-cost:   15
c ---[2192]---> BDD-cost:    3
c ---[2190]---> BDD-cost:   15
c ---[2188]---> BDD-cost:    3
c ---[2186]---> BDD-cost:    5
c ---[2184]---> BDD-cost:   15
c ---[2182]---> BDD-cost:    3
c ---[2180]---> BDD-cost:    5
c ---[2178]---> BDD-cost:   15
c ---[2176]---> BDD-cost:    3
c ---[2174]---> BDD-cost:    5
c ---[2172]---> BDD-cost:   15
c ---[2170]---> BDD-cost:    3
c ---[2168]---> BDD-cost:    5
c ---[2166]---> BDD-cost:   15
c ---[2164]---> BDD-cost:    3
c ---[2162]---> BDD-cost:    5
c ---[2160]---> BDD-cost:   15
c ---[2158]---> BDD-cost:    3
c ---[2156]---> BDD-cost:    5
c ---[2154]---> BDD-cost:   15
c ---[2152]---> BDD-cost:    3
c ---[2150]---> BDD-cost:    5
c ---[2148]---> BDD-cost:   15
c ---[2146]---> BDD-cost:    3
c ---[2144]---> BDD-cost:    5
c ---[2142]---> BDD-cost:   15
c ---[2140]---> BDD-cost:    3
c ---[2138]---> BDD-cost:    5
c ---[2136]---> BDD-cost:   15
c ---[2134]---> BDD-cost:    3
c ---[2132]---> BDD-cost:    5
c ---[2130]---> BDD-cost:   15
c ---[2128]---> BDD-cost:    3
c ---[2126]---> BDD-cost:    5
c ---[2124]---> BDD-cost:   15
c ---[2122]---> BDD-cost:    3
c ---[2120]---> BDD-cost:    5
c ---[2118]---> BDD-cost:   15
c ---[2116]---> BDD-cost:    3
c ---[2114]---> BDD-cost:    5
c ---[2112]---> BDD-cost:   15
c ---[2110]---> BDD-cost:    3
c ---[2108]---> BDD-cost:    5
c ---[2106]---> BDD-cost:   15
c ---[2104]---> BDD-cost:   15
c ---[2102]---> BDD-cost:    3
c ---[2100]---> BDD-cost:    5
c ---[2098]---> BDD-cost:   15
c ---[2096]---> BDD-cost:    3
c ---[2094]---> BDD-cost:    5
c ---[2092]---> BDD-cost:   15
c ---[2090]---> BDD-cost:    5
c ---[2088]---> BDD-cost:   15
c ---[2086]---> BDD-cost:    3
c ---[2084]---> BDD-cost:    5
c ---[2082]---> BDD-cost:   15
c ---[2080]---> BDD-cost:    5
c ---[2078]---> BDD-cost:   15
c ---[2076]---> BDD-cost:    3
c ---[2074]---> BDD-cost:    5
c ---[2072]---> BDD-cost:   15
c ---[2070]---> BDD-cost:    3
c ---[2068]---> BDD-cost:    5
c ---[2066]---> BDD-cost:   15
c ---[2064]---> BDD-cost:    5
c ---[2062]---> BDD-cost:   15
c ---[2060]---> BDD-cost:    3
c ---[2058]---> BDD-cost:    5
c ---[2056]---> BDD-cost:   15
c ---[2054]---> BDD-cost:    5
c ---[2052]---> BDD-cost:   15
c ---[2050]---> BDD-cost:    5
c ---[2048]---> BDD-cost:   15
c ---[2046]---> BDD-cost:    5
c ---[2044]---> BDD-cost:   15
c ---[2042]---> BDD-cost:    3
c ---[2040]---> BDD-cost:    5
c ---[2038]---> BDD-cost:   15
c ---[2036]---> BDD-cost:    3
c ---[2034]---> BDD-cost:    5
c ---[2032]---> BDD-cost:   15
c ---[2030]---> BDD-cost:    3
c ---[2028]---> BDD-cost:    5
c ---[2026]---> BDD-cost:   15
c ---[2024]---> BDD-cost:    3
c ---[2022]---> BDD-cost:    5
c ---[2020]---> BDD-cost:   15
c ---[2018]---> BDD-cost:    3
c ---[2016]---> BDD-cost:    5
c ---[2014]---> BDD-cost:   15
c ---[2012]---> BDD-cost:    3
c ---[2010]---> BDD-cost:    5
c ---[2008]---> BDD-cost:   15
c ---[2006]---> BDD-cost:    3
c ---[2004]---> BDD-cost:    5
c ---[2002]---> BDD-cost:   15
c ---[2000]---> BDD-cost:    5
c ---[1998]---> BDD-cost:   15
c ---[1996]---> BDD-cost:    3
c ---[1994]---> BDD-cost:    5
c ---[1992]---> BDD-cost:   15
c ---[1990]---> BDD-cost:    3
c ---[1988]---> BDD-cost:    5
c ---[1986]---> BDD-cost:   15
c ---[1984]---> BDD-cost:    3
c ---[1982]---> BDD-cost:    5
c ---[1980]---> BDD-cost:   15
c ---[1978]---> BDD-cost:    3
c ---[1976]---> BDD-cost:    5
c ---[1974]---> BDD-cost:   15
c ---[1972]---> BDD-cost:    3
c ---[1970]---> BDD-cost:    5
c ---[1968]---> BDD-cost:   15
c ---[1966]---> BDD-cost:    3
c ---[1964]---> BDD-cost:    5
c ---[1962]---> BDD-cost:   15
c ---[1960]---> BDD-cost:    5
c ---[1958]---> BDD-cost:   15
c ---[1956]---> BDD-cost:    5
c ---[1954]---> BDD-cost:   15
c ---[1952]---> BDD-cost:    3
c ---[1950]---> BDD-cost:    5
c ---[1948]---> BDD-cost:   15
c ---[1946]---> BDD-cost:    5
c ---[1944]---> BDD-cost:   15
c ---[1942]---> BDD-cost:    3
c ---[1940]---> BDD-cost:    5
c ---[1938]---> BDD-cost:   15
c ---[1936]---> BDD-cost:    5
c ---[1934]---> BDD-cost:   15
c ---[1932]---> BDD-cost:    3
c ---[1930]---> BDD-cost:    5
c ---[1928]---> BDD-cost:   15
c ---[1926]---> BDD-cost:    3
c ---[1924]---> BDD-cost:    5
c ---[1922]---> BDD-cost:   15
c ---[1920]---> BDD-cost:    5
c ---[1918]---> BDD-cost:   15
c ---[1916]---> BDD-cost:    3
c ---[1914]---> BDD-cost:    5
c ---[1912]---> BDD-cost:   15
c ---[1910]---> BDD-cost:    3
c ---[1908]---> BDD-cost:    5
c ---[1906]---> BDD-cost:   15
c ---[1904]---> BDD-cost:    3
c ---[1902]---> BDD-cost:    5
c ---[1900]---> BDD-cost:   15
c ---[1898]---> BDD-cost:    3
c ---[1896]---> BDD-cost:    5
c ---[1894]---> BDD-cost:   15
c ---[1892]---> BDD-cost:    5
c ---[1890]---> BDD-cost:   15
c ---[1888]---> BDD-cost:    3
c ---[1886]---> BDD-cost:    5
c ---[1884]---> BDD-cost:   15
c ---[1882]---> BDD-cost:    3
c ---[1880]---> BDD-cost:    5
c ---[1878]---> BDD-cost:   15
c ---[1876]---> BDD-cost:    3
c ---[1874]---> BDD-cost:    5
c ---[1872]---> BDD-cost:   15
c ---[1870]---> BDD-cost:    3
c ---[1868]---> BDD-cost:    5
c ---[1866]---> BDD-cost:   15
c ---[1864]---> BDD-cost:    3
c ---[1862]---> BDD-cost:    5
c ---[1860]---> BDD-cost:   15
c ---[1858]---> BDD-cost:    3
c ---[1856]---> BDD-cost:    5
c ---[1854]---> BDD-cost:   15
c ---[1852]---> BDD-cost:    3
c ---[1850]---> BDD-cost:    5
c ---[1848]---> BDD-cost:   15
c ---[1846]---> BDD-cost:    3
c ---[1844]---> BDD-cost:    5
c ---[1842]---> BDD-cost:   15
c ---[1840]---> BDD-cost:    3
c ---[1838]---> BDD-cost:    5
c ---[1836]---> BDD-cost:   15
c ---[1834]---> BDD-cost:    3
c ---[1832]---> BDD-cost:    5
c ---[1830]---> BDD-cost:   15
c ---[1828]---> BDD-cost:    3
c ---[1826]---> BDD-cost:    5
c ---[1824]---> BDD-cost:   15
c ---[1822]---> BDD-cost:    3
c ---[1820]---> BDD-cost:    5
c ---[1818]---> BDD-cost:   15
c ---[1816]---> BDD-cost:    3
c ---[1814]---> BDD-cost:    5
c ---[1812]---> BDD-cost:   15
c ---[1810]---> BDD-cost:    5
c ---[1808]---> BDD-cost:   15
c ---[1806]---> BDD-cost:    5
c ---[1804]---> BDD-cost:   15
c ---[1802]---> BDD-cost:    3
c ---[1800]---> BDD-cost:    5
c ---[1798]---> BDD-cost:   15
c ---[1796]---> BDD-cost:    3
c ---[1794]---> BDD-cost:    5
c ---[1792]---> BDD-cost:   15
c ---[1790]---> BDD-cost:    3
c ---[1788]---> BDD-cost:    5
c ---[1786]---> BDD-cost:   15
c ---[1784]---> BDD-cost:    3
c ---[1782]---> BDD-cost:    5
c ---[1780]---> BDD-cost:   15
c ---[1778]---> BDD-cost:    5
c ---[1776]---> BDD-cost:   15
c ---[1774]---> BDD-cost:    5
c ---[1772]---> BDD-cost:   15
c ---[1770]---> BDD-cost:    5
c ---[1768]---> BDD-cost:   15
c ---[1766]---> BDD-cost:    5
c ---[1764]---> BDD-cost:   15
c ---[1762]---> BDD-cost:    3
c ---[1760]---> BDD-cost:    5
c ---[1758]---> BDD-cost:   15
c ---[1756]---> BDD-cost:    3
c ---[1754]---> BDD-cost:    5
c ---[1752]---> BDD-cost:   15
c ---[1750]---> BDD-cost:    5
c ---[1748]---> BDD-cost:   15
c ---[1746]---> BDD-cost:    3
c ---[1744]---> BDD-cost:    5
c ---[1742]---> BDD-cost:   15
c ---[1740]---> BDD-cost:    3
c ---[1738]---> BDD-cost:    5
c ---[1736]---> BDD-cost:   15
c ---[1734]---> BDD-cost:    3
c ---[1732]---> BDD-cost:    5
c ---[1730]---> BDD-cost:   15
c ---[1728]---> BDD-cost:    3
c ---[1726]---> BDD-cost:   15
c ---[1724]---> BDD-cost:    5
c ---[1722]---> BDD-cost:   15
c ---[1720]---> BDD-cost:    3
c ---[1718]---> BDD-cost:    5
c ---[1716]---> BDD-cost:   15
c ---[1714]---> BDD-cost:    3
c ---[1712]---> BDD-cost:   15
c ---[1710]---> BDD-cost:   15
c ---[1708]---> BDD-cost:    5
c ---[1706]---> BDD-cost:    5
c ---[1704]---> BDD-cost:   15
c ---[1702]---> BDD-cost:    3
c ---[1700]---> BDD-cost:    5
c ---[1698]---> BDD-cost:   15
c ---[1696]---> BDD-cost:    5
c ---[1694]---> BDD-cost:   15
c ---[1692]---> BDD-cost:    5
c ---[1690]---> BDD-cost:   15
c ---[1688]---> BDD-cost:    5
c ---[1686]---> BDD-cost:   15
c ---[1684]---> BDD-cost:    3
c ---[1682]---> BDD-cost:    5
c ---[1680]---> BDD-cost:   15
c ---[1678]---> BDD-cost:    3
c ---[1676]---> BDD-cost:    5
c ---[1674]---> BDD-cost:   15
c ---[1672]---> BDD-cost:    3
c ---[1670]---> BDD-cost:    5
c ---[1668]---> BDD-cost:   15
c ---[1666]---> BDD-cost:    5
c ---[1664]---> BDD-cost:   15
c ---[1662]---> BDD-cost:    3
c ---[1660]---> BDD-cost:    5
c ---[1658]---> BDD-cost:   15
c ---[1656]---> BDD-cost:    3
c ---[1654]---> BDD-cost:    5
c ---[1652]---> BDD-cost:   15
c ---[1650]---> BDD-cost:    3
c ---[1648]---> BDD-cost:    5
c ---[1646]---> BDD-cost:   15
c ---[1644]---> BDD-cost:    3
c ---[1642]---> BDD-cost:    5
c ---[1640]---> BDD-cost:   15
c ---[1638]---> BDD-cost:    3
c ---[1636]---> BDD-cost:    5
c ---[1634]---> BDD-cost:   15
c ---[1632]---> BDD-cost:    3
c ---[1630]---> BDD-cost:   15
c ---[1628]---> BDD-cost:    5
c ---[1626]---> BDD-cost:   15
c ---[1624]---> BDD-cost:    3
c ---[1622]---> BDD-cost:    5
c ---[1620]---> BDD-cost:   15
c ---[1618]---> BDD-cost:    3
c ---[1616]---> BDD-cost:    5
c ---[1614]---> BDD-cost:   15
c ---[1612]---> BDD-cost:    5
c ---[1610]---> BDD-cost:   15
c ---[1608]---> BDD-cost:    3
c ---[1606]---> BDD-cost:    5
c ---[1604]---> BDD-cost:   15
c ---[1602]---> BDD-cost:    5
c ---[1600]---> BDD-cost:   15
c ---[1598]---> BDD-cost:    3
c ---[1596]---> BDD-cost:    5
c ---[1594]---> BDD-cost:   15
c ---[1592]---> BDD-cost:    3
c ---[1590]---> BDD-cost:    5
c ---[1588]---> BDD-cost:   15
c ---[1586]---> BDD-cost:    3
c ---[1584]---> BDD-cost:    5
c ---[1582]---> BDD-cost:   15
c ---[1580]---> BDD-cost:    5
c ---[1578]---> BDD-cost:   15
c ---[1576]---> BDD-cost:    5
c ---[1574]---> BDD-cost:   15
c ---[1572]---> BDD-cost:    3
c ---[1570]---> BDD-cost:    5
c ---[1568]---> BDD-cost:   15
c ---[1566]---> BDD-cost:   15
c ---[1564]---> BDD-cost:    5
c ---[1562]---> BDD-cost:   15
c ---[1560]---> BDD-cost:    3
c ---[1558]---> BDD-cost:    5
c ---[1556]---> BDD-cost:   15
c ---[1554]---> BDD-cost:    3
c ---[1552]---> BDD-cost:    5
c ---[1550]---> BDD-cost:   15
c ---[1548]---> BDD-cost:    3
c ---[1546]---> BDD-cost:    5
c ---[1544]---> BDD-cost:   15
c ---[1542]---> BDD-cost:    3
c ---[1540]---> BDD-cost:    5
c ---[1538]---> BDD-cost:   15
c ---[1536]---> BDD-cost:    5
c ---[1534]---> BDD-cost:   15
c ---[1532]---> BDD-cost:    5
c ---[1530]---> BDD-cost:   15
c ---[1528]---> BDD-cost:    5
c ---[1526]---> BDD-cost:   15
c ---[1524]---> BDD-cost:    3
c ---[1522]---> BDD-cost:    5
c ---[1520]---> BDD-cost:   15
c ---[1518]---> BDD-cost:    3
c ---[1516]---> BDD-cost:    5
c ---[1514]---> BDD-cost:   15
c ---[1512]---> BDD-cost:    5
c ---[1510]---> BDD-cost:   15
c ---[1508]---> BDD-cost:    3
c ---[1506]---> BDD-cost:    5
c ---[1504]---> BDD-cost:   15
c ---[1502]---> BDD-cost:    5
c ---[1500]---> BDD-cost:   15
c ---[1498]---> BDD-cost:    3
c ---[1496]---> BDD-cost:    5
c ---[1494]---> BDD-cost:   15
c ---[1492]---> BDD-cost:    3
c ---[1490]---> BDD-cost:    5
c ---[1488]---> BDD-cost:    3
c ---[1486]---> BDD-cost:    5
c ---[1484]---> BDD-cost:   15
c ---[1482]---> BDD-cost:    3
c ---[1480]---> BDD-cost:    5
c ---[1478]---> BDD-cost:   15
c ---[1476]---> BDD-cost:    3
c ---[1474]---> BDD-cost:    5
c ---[1472]---> BDD-cost:   15
c ---[1470]---> BDD-cost:   15
c ---[1468]---> BDD-cost:    5
c ---[1466]---> BDD-cost:   15
c ---[1464]---> BDD-cost:    5
c ---[1462]---> BDD-cost:   15
c ---[1460]---> BDD-cost:    3
c ---[1458]---> BDD-cost:    5
c ---[1456]---> BDD-cost:   15
c ---[1454]---> BDD-cost:    3
c ---[1452]---> BDD-cost:    5
c ---[1450]---> BDD-cost:    3
c ---[1448]---> BDD-cost:    5
c ---[1446]---> BDD-cost:   15
c ---[1444]---> BDD-cost:    3
c ---[1442]---> BDD-cost:    5
c ---[1440]---> BDD-cost:   15
c ---[1438]---> BDD-cost:    3
c ---[1436]---> BDD-cost:    5
c ---[1434]---> BDD-cost:   15
c ---[1432]---> BDD-cost:    3
c ---[1430]---> BDD-cost:    5
c ---[1428]---> BDD-cost:   15
c ---[1426]---> BDD-cost:    3
c ---[1424]---> BDD-cost:    5
c ---[1422]---> BDD-cost:   15
c ---[1420]---> BDD-cost:    3
c ---[1418]---> BDD-cost:    5
c ---[1416]---> BDD-cost:   15
c ---[1414]---> BDD-cost:    5
c ---[1412]---> BDD-cost:   15
c ---[1410]---> BDD-cost:   15
c ---[1408]---> BDD-cost:    3
c ---[1406]---> BDD-cost:    5
c ---[1404]---> BDD-cost:   15
c ---[1402]---> BDD-cost:    3
c ---[1400]---> BDD-cost:    5
c ---[1398]---> BDD-cost:   15
c ---[1396]---> BDD-cost:    3
c ---[1394]---> BDD-cost:   15
c ---[1392]---> BDD-cost:    5
c ---[1390]---> BDD-cost:   15
c ---[1388]---> BDD-cost:    3
c ---[1386]---> BDD-cost:    5
c ---[1384]---> BDD-cost:    5
c ---[1382]---> BDD-cost:    3
c ---[1380]---> BDD-cost:    5
c ---[1378]---> BDD-cost:    5
c ---[1376]---> BDD-cost:   15
c ---[1374]---> BDD-cost:    3
c ---[1372]---> BDD-cost:    5
c ---[1370]---> BDD-cost:   15
c ---[1368]---> BDD-cost:    3
c ---[1366]---> BDD-cost:    5
c ---[1364]---> BDD-cost:    3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   61319   205646 |   20439       0        0     nan |  0.000 % |
c |       100 |   61319   205646 |   22482     100     2264    22.6 |  4.579 % |
c |       251 |   61260   205447 |   24731     245     3093    12.6 |  4.664 % |
c |       476 |   61218   205307 |   27204     466     4223     9.1 |  4.723 % |
c |       814 |   61152   205085 |   29924     795     6238     7.8 |  4.815 % |
c |      1321 |   61152   205085 |   32917    1302     9324     7.2 |  4.815 % |
c |      2080 |   61046   204737 |   36208    2045    14953     7.3 |  4.953 % |
c |      3219 |   60995   204568 |   39829    3174    31814    10.0 |  5.025 % |
c |      4928 |   60982   204523 |   43812    4810    47925    10.0 |  5.044 % |
c |      7491 |   60982   204523 |   48194    7373    89050    12.1 |  5.044 % |
c |     11335 |   60982   204523 |   53013   11217   150664    13.4 |  5.044 % |
c |     17102 |   60976   204506 |   58314   16982   235337    13.9 |  5.051 % |
c |     25753 |   60929   204356 |   64146   25627   354236    13.8 |  5.110 % |
c |     38729 |   60789   203888 |   70560   38457   543667    14.1 |  5.300 % |
c |     58190 |   60773   203836 |   77617   57914   922406    15.9 |  5.319 % |
c |     87382 |   60769   203820 |   85378   24184   454151    18.8 |  5.326 % |
c |    131172 |   60765   203804 |   93916   67835  2572645    37.9 |  5.332 % |
c |    196857 |   60747   203735 |  103308   44026  2703276    61.4 |  5.365 % |
c |    295383 |   60747   203735 |  113639   50081 14716642   293.9 |  5.365 % |
c |    443175 |   60743   203719 |  125003   95032 22163034   233.2 |  5.372 % |

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/14341/stat): 14341 (minisat+_script) R 14340 14341 4419 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1843666655 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 1 0 0
Raw data (/proc/14341/statm): 174 3 169 147 0 27 0
[pid=14341] 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=14342
New process pid=14343
New process pid=14344
execve syscall for /bin/sed executable
One traced child (pid=14343) 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=14344) exited with status: 0
One traced child (pid=14342) exited with status: 0
New process pid=14345
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc25/normalized-ws97-3.opb

[startup+10.0041 s]
Raw data (loadavg): 0.93 0.95 0.97 2/57 14345
Raw data (/proc/14341/stat): 14341 (minisat+_script) S 14340 14341 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843666655 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14341/statm): 531 226 485 147 0 384 0
[pid=14341] vsize: 2124
Raw data (/proc/14345/stat): 14345 (minisat+_64-bit) R 14341 14341 4419 0 -1 0 2060 0 0 0 977 10 0 0 25 0 1 0 1843666660 8716288 2009 4294967295 134512640 135094434 3221224448 3221223060 134563124 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14345/statm): 2128 2009 145 145 0 1983 0
[pid=14345] vsize: 8512
Current children cumulated CPU time (s) 9.88
Current children cumulated vsize (Kb) 10636

[startup+20.0047 s]
Raw data (loadavg): 0.94 0.96 0.97 2/57 14345
Raw data (/proc/14341/stat): 14341 (minisat+_script) S 14340 14341 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843666655 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14341/statm): 531 226 485 147 0 384 0
[pid=14341] vsize: 2124
Raw data (/proc/14345/stat): 14345 (minisat+_64-bit) R 14341 14341 4419 0 -1 0 2554 0 0 0 1970 13 0 0 25 0 1 0 1843666660 10825728 2503 4294967295 134512640 135094434 3221224448 3221223060 134563049 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14345/statm): 2643 2503 145 145 0 2498 0
[pid=14345] vsize: 10572
Current children cumulated CPU time (s) 19.84
Current children cumulated vsize (Kb) 12696

[startup+30.0083 s]
Raw data (loadavg): 0.95 0.96 0.97 2/57 14345
Raw data (/proc/14341/stat): 14341 (minisat+_script) S 14340 14341 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843666655 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14341/statm): 531 226 485 147 0 384 0
[pid=14341] vsize: 2124
Raw data (/proc/14345/stat): 14345 (minisat+_64-bit) R 14341 14341 4419 0 -1 0 3046 0 0 0 2963 16 0 0 25 0 1 0 1843666660 12795904 2995 4294967295 134512640 135094434 3221224448 3221223088 134562098 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14345/statm): 3124 2995 145 145 0 2979 0
[pid=14345] vsize: 12496
Current children cumulated CPU time (s) 29.8
Current children cumulated vsize (Kb) 14620

[startup+40.0089 s]
Raw data (loadavg): 0.95 0.96 0.97 2/57 14345
Raw data (/proc/14341/stat): 14341 (minisat+_script) S 14340 14341 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843666655 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14341/statm): 531 226 485 147 0 384 0
[pid=14341] vsize: 2124
Raw data (/proc/14345/stat): 14345 (minisat+_64-bit) R 14341 14341 4419 0 -1 0 3643 0 0 0 3953 21 0 0 25 0 1 0 1843666660 15441920 3592 4294967295 134512640 135094434 3221224448 3221223104 134558221 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14345/statm): 3770 3592 145 145 0 3625 0
[pid=14345] vsize: 15080
Current children cumulated CPU time (s) 39.75
Current children cumulated vsize (Kb) 17204

[startup+50.0105 s]
Raw data (loadavg): 0.96 0.96 0.97 2/57 14345
Raw data (/proc/14341/stat): 14341 (minisat+_script) S 14340 14341 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843666655 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14341/statm): 531 226 485 147 0 384 0
[pid=14341] vsize: 2124
Raw data (/proc/14345/stat): 14345 (minisat+_64-bit) R 14341 14341 4419 0 -1 0 3923 0 0 0 4949 22 0 0 25 0 1 0 1843666660 16568320 3872 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14345/statm): 4045 3872 145 145 0 3900 0
[pid=14345] vsize: 16180
Current children cumulated CPU time (s) 49.72
Current children cumulated vsize (Kb) 18304

[startup+60.0111 s]
Raw data (loadavg): 0.97 0.96 0.97 2/57 14345
Raw data (/proc/14341/stat): 14341 (minisat+_script) S 14340 14341 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843666655 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14341/statm): 531 226 485 147 0 384 0
[pid=14341] vsize: 2124
Raw data (/proc/14345/stat): 14345 (minisat+_64-bit) R 14341 14341 4419 0 -1 0 3923 0 0 0 5950 22 0 0 25 0 1 0 1843666660 16568320 3872 4294967295 134512640 135094434 3221224448 3221223120 134556263 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14345/statm): 4045 3872 145 145 0 3900 0
[pid=14345] vsize: 16180
Current children cumulated CPU time (s) 59.73
Current children cumulated vsize (Kb) 18304

[startup+70.0117 s]
Raw data (loadavg): 0.97 0.96 0.97 2/57 14345
Raw data (/proc/14341/stat): 14341 (minisat+_script) S 14340 14341 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843666655 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14341/statm): 531 226 485 147 0 384 0
[pid=14341] vsize: 2124
Raw data (/proc/14345/stat): 14345 (minisat+_64-bit) R 14341 14341 4419 0 -1 0 4275 0 0 0 6945 24 0 0 25 0 1 0 1843666660 18022400 4224 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14345/statm): 4400 4224 145 145 0 4255 0
[pid=14345] vsize: 17600
Current children cumulated CPU time (s) 69.7
Current children cumulated vsize (Kb) 19724

[startup+80.0123 s]
Raw data (loadavg): 0.98 0.96 0.97 2/57 14345
Raw data (/proc/14341/stat): 14341 (minisat+_script) S 14340 14341 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843666655 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14341/statm): 531 226 485 147 0 384 0
[pid=14341] vsize: 2124
Raw data (/proc/14345/stat): 14345 (minisat+_64-bit) R 14341 14341 4419 0 -1 0 5363 0 0 0 7929 31 0 0 25 0 1 0 1843666660 22503424 5312 4294967295 134512640 135094434 3221224448 3221223104 134558210 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14345/statm): 5494 5312 145 145 0 5349 0
[pid=14345] vsize: 21976
Current children cumulated CPU time (s) 79.61
Current children cumulated vsize (Kb) 24100

[startup+90.0129 s]
Raw data (loadavg): 0.98 0.96 0.97 2/57 14345
Raw data (/proc/14341/stat): 14341 (minisat+_script) S 14340 14341 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843666655 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14341/statm): 531 226 485 147 0 384 0
[pid=14341] vsize: 2124
Raw data (/proc/14345/stat): 14345 (minisat+_64-bit) R 14341 14341 4419 0 -1 0 6612 0 0 0 8910 39 0 0 25 0 1 0 1843666660 27615232 6561 4294967295 134512640 135094434 3221224448 3221223040 134557180 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14345/statm): 6742 6561 145 145 0 6597 0
[pid=14345] vsize: 26968
Current children cumulated CPU time (s) 89.5
Current children cumulated vsize (Kb) 29092

[startup+100.013 s]
Raw data (loadavg): 0.98 0.96 0.97 2/57 14345
Raw data (/proc/14341/stat): 14341 (minisat+_script) S 14340 14341 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843666655 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14341/statm): 531 226 485 147 0 384 0
[pid=14341] vsize: 2124
Raw data (/proc/14345/stat): 14345 (minisat+_64-bit) R 14341 14341 4419 0 -1 0 7621 0 0 0 9894 45 0 0 25 0 1 0 1843666660 31703040 7570 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14345/statm): 7740 7570 145 145 0 7595 0
[pid=14345] vsize: 30960
Current children cumulated CPU time (s) 99.4
Current children cumulated vsize (Kb) 33084

[startup+110.014 s]
Raw data (loadavg): 0.98 0.96 0.97 2/57 14345
Raw data (/proc/14341/stat): 14341 (minisat+_script) S 14340 14341 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843666655 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14341/statm): 531 226 485 147 0 384 0
[pid=14341] vsize: 2124
Raw data (/proc/14345/stat): 14345 (minisat+_64-bit) R 14341 14341 4419 0 -1 0 8816 0 0 0 10876 53 0 0 25 0 1 0 1843666660 36581376 8765 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14345/statm): 8931 8765 145 145 0 8786 0
[pid=14345] vsize: 35724
Current children cumulated CPU time (s) 109.3
Current children cumulated vsize (Kb) 37848

[startup+120.014 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 14345
Raw data (/proc/14341/stat): 14341 (minisat+_script) S 14340 14341 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843666655 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14341/statm): 531 226 485 147 0 384 0
[pid=14341] vsize: 2124
Raw data (/proc/14345/stat): 14345 (minisat+_64-bit) R 14341 14341 4419 0 -1 0 8845 0 0 0 11876 53 0 0 25 0 1 0 1843666660 36700160 8794 4294967295 134512640 135094434 3221224448 3221223104 134557950 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14345/statm): 8960 8794 145 145 0 8815 0
[pid=14345] vsize: 35840
Current children cumulated CPU time (s) 119.3
Current children cumulated vsize (Kb) 37964

[startup+130.014 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 14345
Raw data (/proc/14341/stat): 14341 (minisat+_script) S 14340 14341 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843666655 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14341/statm): 531 226 485 147 0 384 0
[pid=14341] vsize: 2124
Raw data (/proc/14345/stat): 14345 (minisat+_64-bit) R 14341 14341 4419 0 -1 0 8845 0 0 0 12876 53 0 0 25 0 1 0 1843666660 36700160 8794 4294967295 134512640 135094434 3221224448 3221223104 134558246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14345/statm): 8960 8794 145 145 0 8815 0
[pid=14345] vsize: 35840
Current children cumulated CPU time (s) 129.3
Current children cumulated vsize (Kb) 37964

[startup+140.015 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 14345
Raw data (/proc/14341/stat): 14341 (minisat+_script) S 14340 14341 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843666655 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14341/statm): 531 226 485 147 0 384 0
[pid=14341] vsize: 2124
Raw data (/proc/14345/stat): 14345 (minisat+_64-bit) R 14341 14341 4419 0 -1 0 8845 0 0 0 13875 53 0 0 25 0 1 0 1843666660 36700160 8794 4294967295 134512640 135094434 3221224448 3221223120 134556242 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14345/statm): 8960 8794 145 145 0 8815 0
[pid=14345] vsize: 35840
Current children cumulated CPU time (s) 139.29
Current children cumulated vsize (Kb) 37964

[startup+150.016 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 14345
Raw data (/proc/14341/stat): 14341 (minisat+_script) S 14340 14341 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843666655 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14341/statm): 531 226 485 147 0 384 0
[pid=14341] vsize: 2124
Raw data (/proc/14345/stat): 14345 (minisat+_64-bit) R 14341 14341 4419 0 -1 0 8845 0 0 0 14875 54 0 0 25 0 1 0 1843666660 36700160 8794 4294967295 134512640 135094434 3221224448 3221223120 134555837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14345/statm): 8960 8794 145 145 0 8815 0
[pid=14345] vsize: 35840
Current children cumulated CPU time (s) 149.3
Current children cumulated vsize (Kb) 37964

[startup+160.016 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 14345
Raw data (/proc/14341/stat): 14341 (minisat+_script) S 14340 14341 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843666655 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14341/statm): 531 226 485 147 0 384 0
[pid=14341] vsize: 2124
Raw data (/proc/14345/stat): 14345 (minisat+_64-bit) R 14341 14341 4419 0 -1 0 9365 0 0 0 15866 57 0 0 25 0 1 0 1843666660 38830080 9314 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14345/statm): 9480 9314 145 145 0 9335 0
[pid=14345] vsize: 37920
Current children cumulated CPU time (s) 159.24
Current children cumulated vsize (Kb) 40044

[startup+170.017 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 14345
Raw data (/proc/14341/stat): 14341 (minisat+_script) S 14340 14341 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843666655 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14341/statm): 531 226 485 147 0 384 0
[pid=14341] vsize: 2124
Raw data (/proc/14345/stat): 14345 (minisat+_64-bit) T 14341 14341 4419 0 -1 0 10646 0 0 0 16848 64 0 0 25 0 1 0 1843666660 44077056 10595 4294967295 134512640 135094434 3221224448 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/14345/statm): 10761 10595 145 145 0 10616 0
[pid=14345] vsize: 43044
Current children cumulated CPU time (s) 169.13
Current children cumulated vsize (Kb) 45168

[startup+180.017 s]
Raw data (loadavg): 0.99 0.97 0.97 1/57 14345
Raw data (/proc/14341/stat): 14341 (minisat+_script) S 14340 14341 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843666655 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14341/statm): 531 226 485 147 0 384 0
[pid=14341] vsize: 2124
Raw data (/proc/14345/stat): 14345 (minisat+_64-bit) T 14341 14341 4419 0 -1 0 11856 0 0 0 17830 70 0 0 25 0 1 0 1843666660 49037312 11805 4294967295 134512640 135094434 3221224448 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/14345/statm): 11972 11805 145 145 0 11827 0
[pid=14345] vsize: 47888
Current children cumulated CPU time (s) 179.01
Current children cumulated vsize (Kb) 50012

[startup+190.018 s]
Raw data (loadavg): 0.99 0.97 0.97 1/57 14345
Raw data (/proc/14341/stat): 14341 (minisat+_script) S 14340 14341 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843666655 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14341/statm): 531 226 485 147 0 384 0
[pid=14341] vsize: 2124
Raw data (/proc/14345/stat): 14345 (minisat+_64-bit) T 14341 14341 4419 0 -1 0 13058 0 0 0 18812 78 0 0 25 0 1 0 1843666660 53964800 13007 4294967295 134512640 135094434 3221224448 3221222828 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/14345/statm): 13175 13007 145 145 0 13030 0
[pid=14345] vsize: 52700
Current children cumulated CPU time (s) 188.91
Current children cumulated vsize (Kb) 54824

[startup+200.019 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 14345
Raw data (/proc/14341/stat): 14341 (minisat+_script) S 14340 14341 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843666655 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14341/statm): 531 226 485 147 0 384 0
[pid=14341] vsize: 2124
Raw data (/proc/14345/stat): 14345 (minisat+_64-bit) R 14341 14341 4419 0 -1 0 14134 0 0 0 19793 86 0 0 25 0 1 0 1843666660 58368000 14083 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14345/statm): 14250 14083 145 145 0 14105 0
[pid=14345] vsize: 57000
Current children cumulated CPU time (s) 198.8
Current children cumulated vsize (Kb) 59124

[startup+210.019 s]
Raw data (loadavg): 0.99 0.97 0.97 1/57 14345
Raw data (/proc/14341/stat): 14341 (minisat+_script) S 14340 14341 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843666655 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14341/statm): 531 226 485 147 0 384 0
[pid=14341] vsize: 2124
Raw data (/proc/14345/stat): 14345 (minisat+_64-bit) T 14341 14341 4419 0 -1 0 15056 0 0 0 20779 91 0 0 25 0 1 0 1843666660 62144512 15005 4294967295 134512640 135094434 3221224448 3221222828 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/14345/statm): 15172 15005 145 145 0 15027 0
[pid=14345] vsize: 60688
Current children cumulated CPU time (s) 208.71
Current children cumulated vsize (Kb) 62812

[startup+220.02 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 14345
Raw data (/proc/14341/stat): 14341 (minisat+_script) S 14340 14341 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843666655 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14341/statm): 531 226 485 147 0 384 0
[pid=14341] vsize: 2124
Raw data (/proc/14345/stat): 14345 (minisat+_64-bit) R 14341 14341 4419 0 -1 0 15858 0 0 0 21765 97 0 0 25 0 1 0 1843666660 65433600 15807 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14345/statm): 15975 15807 145 145 0 15830 0
[pid=14345] vsize: 63900
Current children cumulated CPU time (s) 218.63
Current children cumulated vsize (Kb) 66024

[startup+230.02 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 14345
Raw data (/proc/14341/stat): 14341 (minisat+_script) S 14340 14341 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843666655 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14341/statm): 531 226 485 147 0 384 0
[pid=14341] vsize: 2124
Raw data (/proc/14345/stat): 14345 (minisat+_64-bit) R 14341 14341 4419 0 -1 0 16566 0 0 0 22756 101 0 0 25 0 1 0 1843666660 68329472 16515 4294967295 134512640 135094434 3221224448 3221223040 134557273 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14345/statm): 16682 16515 145 145 0 16537 0
[pid=14345] vsize: 66728
Current children cumulated CPU time (s) 228.58
Current children cumulated vsize (Kb) 68852

[startup+240.021 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 14345
Raw data (/proc/14341/stat): 14341 (minisat+_script) S 14340 14341 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843666655 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14341/statm): 531 226 485 147 0 384 0
[pid=14341] vsize: 2124
Raw data (/proc/14345/stat): 14345 (minisat+_64-bit) T 14341 14341 4419 0 -1 0 17256 0 0 0 23745 104 0 0 25 0 1 0 1843666660 71155712 17205 4294967295 134512640 135094434 3221224448 3221222828 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/14345/statm): 17372 17205 145 145 0 17227 0
[pid=14345] vsize: 69488
Current children cumulated CPU time (s) 238.5
Current children cumulated vsize (Kb) 71612

[startup+250.022 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 14345
Raw data (/proc/14341/stat): 14341 (minisat+_script) S 14340 14341 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843666655 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14341/statm): 531 226 485 147 0 384 0
[pid=14341] vsize: 2124
Raw data (/proc/14345/stat): 14345 (minisat+_64-bit) R 14341 14341 4419 0 -1 0 17914 0 0 0 24735 108 0 0 25 0 1 0 1843666660 73854976 17863 4294967295 134512640 135094434 3221224448 3221223072 134557714 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14345/statm): 18031 17863 145 145 0 17886 0
[pid=14345] vsize: 72124
Current children cumulated CPU time (s) 248.44
Current children cumulated vsize (Kb) 74248

[startup+260.022 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 14345
Raw data (/proc/14341/stat): 14341 (minisat+_script) S 14340 14341 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843666655 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14341/statm): 531 226 485 147 0 384 0
[pid=14341] vsize: 2124
Raw data (/proc/14345/stat): 14345 (minisat+_64-bit) R 14341 14341 4419 0 -1 0 18634 0 0 0 25722 114 0 0 25 0 1 0 1843666660 76795904 18583 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14345/statm): 18749 18583 145 145 0 18604 0
[pid=14345] vsize: 74996
Current children cumulated CPU time (s) 258.37
Current children cumulated vsize (Kb) 77120

[startup+270.022 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 14345
Raw data (/proc/14341/stat): 14341 (minisat+_script) S 14340 14341 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843666655 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14341/statm): 531 226 485 147 0 384 0
[pid=14341] vsize: 2124
Raw data (/proc/14345/stat): 14345 (minisat+_64-bit) R 14341 14341 4419 0 -1 0 19297 0 0 0 26712 117 0 0 25 0 1 0 1843666660 79503360 19246 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14345/statm): 19410 19246 145 145 0 19265 0
[pid=14345] vsize: 77640
Current children cumulated CPU time (s) 268.3
Current children cumulated vsize (Kb) 79764

[startup+280.023 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 14345
Raw data (/proc/14341/stat): 14341 (minisat+_script) S 14340 14341 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843666655 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14341/statm): 531 226 485 147 0 384 0
[pid=14341] vsize: 2124
Raw data (/proc/14345/stat): 14345 (minisat+_64-bit) R 14341 14341 4419 0 -1 0 19897 0 0 0 27703 121 0 0 25 0 1 0 1843666660 81956864 19846 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14345/statm): 20009 19846 145 145 0 19864 0
[pid=14345] vsize: 80036
Current children cumulated CPU time (s) 278.25
Current children cumulated vsize (Kb) 82160

[startup+290.024 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 14345
Raw data (/proc/14341/stat): 14341 (minisat+_script) S 14340 14341 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843666655 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14341/statm): 531 226 485 147 0 384 0
[pid=14341] vsize: 2124
Raw data (/proc/14345/stat): 14345 (minisat+_64-bit) R 14341 14341 4419 0 -1 0 20085 0 0 0 28700 122 0 0 25 0 1 0 1843666660 82726912 20034 4294967295 134512640 135094434 3221224448 3221223104 134558007 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14345/statm): 20197 20034 145 145 0 20052 0
[pid=14345] vsize: 80788
Current children cumulated CPU time (s) 288.23
Current children cumulated vsize (Kb) 82912

[startup+300.025 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 14345
Raw data (/proc/14341/stat): 14341 (minisat+_script) S 14340 14341 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843666655 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14341/statm): 531 226 485 147 0 384 0
[pid=14341] vsize: 2124
Raw data (/proc/14345/stat): 14345 (minisat+_64-bit) R 14341 14341 4419 0 -1 0 20085 0 0 0 29700 122 0 0 25 0 1 0 1843666660 82726912 20034 4294967295 134512640 135094434 3221224448 3221223104 134558402 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14345/statm): 20197 20034 145 145 0 20052 0
[pid=14345] vsize: 80788
Current children cumulated CPU time (s) 298.23
Current children cumulated vsize (Kb) 82912

[startup+310.026 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 14345
Raw data (/proc/14341/stat): 14341 (minisat+_script) S 14340 14341 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843666655 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14341/statm): 531 226 485 147 0 384 0
[pid=14341] vsize: 2124
Raw data (/proc/14345/stat): 14345 (minisat+_64-bit) R 14341 14341 4419 0 -1 0 20086 0 0 0 30700 122 0 0 25 0 1 0 1843666660 82726912 20035 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14345/statm): 20197 20035 145 145 0 20052 0
[pid=14345] vsize: 80788
Current children cumulated CPU time (s) 308.23
Current children cumulated vsize (Kb) 82912

[startup+320.027 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 14345
Raw data (/proc/14341/stat): 14341 (minisat+_script) S 14340 14341 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843666655 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14341/statm): 531 226 485 147 0 384 0
[pid=14341] vsize: 2124
Raw data (/proc/14345/stat): 14345 (minisat+_64-bit) R 14341 14341 4419 0 -1 0 20086 0 0 0 31700 122 0 0 25 0 1 0 1843666660 82726912 20035 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14345/statm): 20197 20035 145 145 0 20052 0
[pid=14345] vsize: 80788
Current children cumulated CPU time (s) 318.23
Current children cumulated vsize (Kb) 82912

[startup+330.027 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 14345
Raw data (/proc/14341/stat): 14341 (minisat+_script) S 14340 14341 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843666655 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14341/statm): 531 226 485 147 0 384 0
[pid=14341] vsize: 2124
Raw data (/proc/14345/stat): 14345 (minisat+_64-bit) R 14341 14341 4419 0 -1 0 20087 0 0 0 32701 122 0 0 25 0 1 0 1843666660 82726912 20036 4294967295 134512640 135094434 3221224448 3221223120 134555574 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14345/statm): 20197 20036 145 145 0 20052 0
[pid=14345] vsize: 80788
Current children cumulated CPU time (s) 328.24
Current children cumulated vsize (Kb) 82912

[startup+340.029 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 14345
Raw data (/proc/14341/stat): 14341 (minisat+_script) S 14340 14341 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843666655 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14341/statm): 531 226 485 147 0 384 0
[pid=14341] vsize: 2124
Raw data (/proc/14345/stat): 14345 (minisat+_64-bit) R 14341 14341 4419 0 -1 0 20090 0 0 0 33701 122 0 0 25 0 1 0 1843666660 82726912 20039 4294967295 134512640 135094434 3221224448 3221223104 134557917 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14345/statm): 20197 20039 145 145 0 20052 0
[pid=14345] vsize: 80788
Current children cumulated CPU time (s) 338.24
Current children cumulated vsize (Kb) 82912

[startup+350.031 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 14345
Raw data (/proc/14341/stat): 14341 (minisat+_script) S 14340 14341 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843666655 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14341/statm): 531 226 485 147 0 384 0
[pid=14341] vsize: 2124
Raw data (/proc/14345/stat): 14345 (minisat+_64-bit) R 14341 14341 4419 0 -1 0 20091 0 0 0 34701 122 0 0 25 0 1 0 1843666660 82726912 20040 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14345/statm): 20197 20040 145 145 0 20052 0
[pid=14345] vsize: 80788
Current children cumulated CPU time (s) 348.24
Current children cumulated vsize (Kb) 82912

[startup+360.031 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 14345
Raw data (/proc/14341/stat): 14341 (minisat+_script) S 14340 14341 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843666655 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14341/statm): 531 226 485 147 0 384 0
[pid=14341] vsize: 2124
Raw data (/proc/14345/stat): 14345 (minisat+_64-bit) R 14341 14341 4419 0 -1 0 20091 0 0 0 35702 122 0 0 25 0 1 0 1843666660 82726912 20040 4294967295 134512640 135094434 3221224448 3221223104 134558126 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14345/statm): 20197 20040 145 145 0 20052 0
[pid=14345] vsize: 80788
Current children cumulated CPU time (s) 358.25
Current children cumulated vsize (Kb) 82912

[startup+370.032 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 14345
Raw data (/proc/14341/stat): 14341 (minisat+_script) S 14340 14341 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843666655 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14341/statm): 531 226 485 147 0 384 0
[pid=14341] vsize: 2124
Raw data (/proc/14345/stat): 14345 (minisat+_64-bit) R 14341 14341 4419 0 -1 0 20091 0 0 0 36702 122 0 0 25 0 1 0 1843666660 82726912 20040 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14345/statm): 20197 20040 145 145 0 20052 0
[pid=14345] vsize: 80788
Current children cumulated CPU time (s) 368.25
Current children cumulated vsize (Kb) 82912

[startup+380.033 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 14345
Raw data (/proc/14341/stat): 14341 (minisat+_script) S 14340 14341 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843666655 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14341/statm): 531 226 485 147 0 384 0
[pid=14341] vsize: 2124
Raw data (/proc/14345/stat): 14345 (minisat+_64-bit) R 14341 14341 4419 0 -1 0 20091 0 0 0 37702 122 0 0 25 0 1 0 1843666660 82726912 20040 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14345/statm): 20197 20040 145 145 0 20052 0
[pid=14345] vsize: 80788
Current children cumulated CPU time (s) 378.25
Current children cumulated vsize (Kb) 82912

[startup+390.034 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 14345
Raw data (/proc/14341/stat): 14341 (minisat+_script) S 14340 14341 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843666655 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14341/statm): 531 226 485 147 0 384 0
[pid=14341] vsize: 2124
Raw data (/proc/14345/stat): 14345 (minisat+_64-bit) R 14341 14341 4419 0 -1 0 20091 0 0 0 38702 122 0 0 25 0 1 0 1843666660 82726912 20040 4294967295 134512640 135094434 3221224448 3221223104 134558019 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14345/statm): 20197 20040 145 145 0 20052 0
[pid=14345] vsize: 80788
Current children cumulated CPU time (s) 388.25
Current children cumulated vsize (Kb) 82912

[startup+400.034 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 14345
Raw data (/proc/14341/stat): 14341 (minisat+_script) S 14340 14341 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843666655 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14341/statm): 531 226 485 147 0 384 0
[pid=14341] vsize: 2124
Raw data (/proc/14345/stat): 14345 (minisat+_64-bit) R 14341 14341 4419 0 -1 0 20091 0 0 0 39703 122 0 0 25 0 1 0 1843666660 82726912 20040 4294967295 134512640 135094434 3221224448 3221223104 134557849 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14345/statm): 20197 20040 145 145 0 20052 0
[pid=14345] vsize: 80788
Current children cumulated CPU time (s) 398.26
Current children cumulated vsize (Kb) 82912

[startup+410.035 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 14345
Raw data (/proc/14341/stat): 14341 (minisat+_script) S 14340 14341 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843666655 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14341/statm): 531 226 485 147 0 384 0
[pid=14341] vsize: 2124
Raw data (/proc/14345/stat): 14345 (minisat+_64-bit) R 14341 14341 4419 0 -1 0 20091 0 0 0 40703 122 0 0 25 0 1 0 1843666660 82726912 20040 4294967295 134512640 135094434 3221224448 3221223040 134557273 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14345/statm): 20197 20040 145 145 0 20052 0
[pid=14345] vsize: 80788
Current children cumulated CPU time (s) 408.26
Current children cumulated vsize (Kb) 82912

[startup+420.036 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 14345
Raw data (/proc/14341/stat): 14341 (minisat+_script) S 14340 14341 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843666655 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14341/statm): 531 226 485 147 0 384 0
[pid=14341] vsize: 2124
Raw data (/proc/14345/stat): 14345 (minisat+_64-bit) R 14341 14341 4419 0 -1 0 20091 0 0 0 41703 122 0 0 25 0 1 0 1843666660 82726912 20040 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14345/statm): 20197 20040 145 145 0 20052 0
[pid=14345] vsize: 80788
Current children cumulated CPU time (s) 418.26
Current children cumulated vsize (Kb) 82912

[startup+430.036 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 14345
Raw data (/proc/14341/stat): 14341 (minisat+_script) S 14340 14341 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843666655 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14341/statm): 531 226 485 147 0 384 0
[pid=14341] vsize: 2124
Raw data (/proc/14345/stat): 14345 (minisat+_64-bit) R 14341 14341 4419 0 -1 0 20091 0 0 0 42702 123 0 0 25 0 1 0 1843666660 82726912 20040 4294967295 134512640 135094434 3221224448 3221223104 134558009 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14345/statm): 20197 20040 145 145 0 20052 0
[pid=14345] vsize: 80788
Current children cumulated CPU time (s) 428.26
Current children cumulated vsize (Kb) 82912

[startup+440.037 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 14345
Raw data (/proc/14341/stat): 14341 (minisat+_script) S 14340 14341 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843666655 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14341/statm): 531 226 485 147 0 384 0
[pid=14341] vsize: 2124
Raw data (/proc/14345/stat): 14345 (minisat+_64-bit) R 14341 14341 4419 0 -1 0 20091 0 0 0 43702 123 0 0 25 0 1 0 1843666660 82726912 20040 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14345/statm): 20197 20040 145 145 0 20052 0
[pid=14345] vsize: 80788
Current children cumulated CPU time (s) 438.26
Current children cumulated vsize (Kb) 82912

[startup+450.038 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 14345
Raw data (/proc/14341/stat): 14341 (minisat+_script) S 14340 14341 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843666655 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14341/statm): 531 226 485 147 0 384 0
[pid=14341] vsize: 2124
Raw data (/proc/14345/stat): 14345 (minisat+_64-bit) R 14341 14341 4419 0 -1 0 20091 0 0 0 44702 123 0 0 25 0 1 0 1843666660 82726912 20040 4294967295 134512640 135094434 3221224448 3221223104 134557860 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14345/statm): 20197 20040 145 145 0 20052 0
[pid=14345] vsize: 80788
Current children cumulated CPU time (s) 448.26
Current children cumulated vsize (Kb) 82912

[startup+460.038 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 14345
Raw data (/proc/14341/stat): 14341 (minisat+_script) S 14340 14341 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843666655 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14341/statm): 531 226 485 147 0 384 0
[pid=14341] vsize: 2124
Raw data (/proc/14345/stat): 14345 (minisat+_64-bit) R 14341 14341 4419 0 -1 0 21105 0 0 0 45687 130 0 0 25 0 1 0 1843666660 86880256 21054 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14345/statm): 21211 21054 145 145 0 21066 0
[pid=14345] vsize: 84844
Current children cumulated CPU time (s) 458.18
Current children cumulated vsize (Kb) 86968

[startup+470.039 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 14345
Raw data (/proc/14341/stat): 14341 (minisat+_script) S 14340 14341 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843666655 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14341/statm): 531 226 485 147 0 384 0
[pid=14341] vsize: 2124
Raw data (/proc/14345/stat): 14345 (minisat+_64-bit) R 14341 14341 4419 0 -1 0 22164 0 0 0 46670 136 0 0 25 0 1 0 1843666660 91230208 22113 4294967295 134512640 135094434 3221224448 3221223104 134558016 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14345/statm): 22273 22113 145 145 0 22128 0
[pid=14345] vsize: 89092
Current children cumulated CPU time (s) 468.07
Current children cumulated vsize (Kb) 91216

[startup+480.039 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 14345
Raw data (/proc/14341/stat): 14341 (minisat+_script) S 14340 14341 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843666655 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14341/statm): 531 226 485 147 0 384 0
[pid=14341] vsize: 2124
Raw data (/proc/14345/stat): 14345 (minisat+_64-bit) R 14341 14341 4419 0 -1 0 23220 0 0 0 47654 142 0 0 25 0 1 0 1843666660 95567872 23169 4294967295 134512640 135094434 3221224448 3221223104 134558235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14345/statm): 23332 23169 145 145 0 23187 0
[pid=14345] vsize: 93328
Current children cumulated CPU time (s) 477.97
Current children cumulated vsize (Kb) 95452

[startup+490.04 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 14345
Raw data (/proc/14341/stat): 14341 (minisat+_script) S 14340 14341 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843666655 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14341/statm): 531 226 485 147 0 384 0
[pid=14341] vsize: 2124
Raw data (/proc/14345/stat): 14345 (minisat+_64-bit) R 14341 14341 4419 0 -1 0 23881 0 0 0 48643 147 0 0 25 0 1 0 1843666660 98279424 23830 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14345/statm): 23994 23830 145 145 0 23849 0
[pid=14345] vsize: 95976
Current children cumulated CPU time (s) 487.91
Current children cumulated vsize (Kb) 98100

[startup+500.039 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 14345
Raw data (/proc/14341/stat): 14341 (minisat+_script) S 14340 14341 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843666655 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14341/statm): 531 226 485 147 0 384 0
[pid=14341] vsize: 2124
Raw data (/proc/14345/stat): 14345 (minisat+_64-bit) R 14341 14341 4419 0 -1 0 24668 0 0 0 49631 152 0 0 25 0 1 0 1843666660 101531648 24617 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14345/statm): 24788 24617 145 145 0 24643 0
[pid=14345] vsize: 99152
Current children cumulated CPU time (s) 497.84
Current children cumulated vsize (Kb) 101276

[startup+510.04 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 14345
Raw data (/proc/14341/stat): 14341 (minisat+_script) S 14340 14341 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843666655 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14341/statm): 531 226 485 147 0 384 0
[pid=14341] vsize: 2124
Raw data (/proc/14345/stat): 14345 (minisat+_64-bit) R 14341 14341 4419 0 -1 0 25562 0 0 0 50618 158 0 0 25 0 1 0 1843666660 105177088 25511 4294967295 134512640 135094434 3221224448 3221223104 134558013 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14345/statm): 25678 25511 145 145 0 25533 0
[pid=14345] vsize: 102712
Current children cumulated CPU time (s) 507.77
Current children cumulated vsize (Kb) 104836

[startup+520.042 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 14345
Raw data (/proc/14341/stat): 14341 (minisat+_script) S 14340 14341 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843666655 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14341/statm): 531 226 485 147 0 384 0
[pid=14341] vsize: 2124
Raw data (/proc/14345/stat): 14345 (minisat+_64-bit) R 14341 14341 4419 0 -1 0 25562 0 0 0 51618 158 0 0 25 0 1 0 1843666660 105177088 25511 4294967295 134512640 135094434 3221224448 3221223104 134558218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14345/statm): 25678 25511 145 145 0 25533 0
[pid=14345] vsize: 102712
Current children cumulated CPU time (s) 517.77
Current children cumulated vsize (Kb) 104836

[startup+530.042 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 14345
Raw data (/proc/14341/stat): 14341 (minisat+_script) S 14340 14341 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843666655 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14341/statm): 531 226 485 147 0 384 0
[pid=14341] vsize: 2124
Raw data (/proc/14345/stat): 14345 (minisat+_64-bit) R 14341 14341 4419 0 -1 0 25562 0 0 0 52618 158 0 0 25 0 1 0 1843666660 105177088 25511 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14345/statm): 25678 25511 145 145 0 25533 0
[pid=14345] vsize: 102712
Current children cumulated CPU time (s) 527.77
Current children cumulated vsize (Kb) 104836

[startup+540.043 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 14345
Raw data (/proc/14341/stat): 14341 (minisat+_script) S 14340 14341 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843666655 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14341/statm): 531 226 485 147 0 384 0
[pid=14341] vsize: 2124
Raw data (/proc/14345/stat): 14345 (minisat+_64-bit) R 14341 14341 4419 0 -1 0 25562 0 0 0 53618 159 0 0 25 0 1 0 1843666660 105177088 25511 4294967295 134512640 135094434 3221224448 3221223104 134558208 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14345/statm): 25678 25511 145 145 0 25533 0
[pid=14345] vsize: 102712
Current children cumulated CPU time (s) 537.78
Current children cumulated vsize (Kb) 104836

[startup+550.043 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 14345
Raw data (/proc/14341/stat): 14341 (minisat+_script) S 14340 14341 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843666655 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14341/statm): 531 226 485 147 0 384 0
[pid=14341] vsize: 2124
Raw data (/proc/14345/stat): 14345 (minisat+_64-bit) R 14341 14341 4419 0 -1 0 25562 0 0 0 54618 159 0 0 25 0 1 0 1843666660 105177088 25511 4294967295 134512640 135094434 3221224448 3221223104 134557996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14345/statm): 25678 25511 145 145 0 25533 0
[pid=14345] vsize: 102712
Current children cumulated CPU time (s) 547.78
Current children cumulated vsize (Kb) 104836

[startup+560.043 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 14345
Raw data (/proc/14341/stat): 14341 (minisat+_script) S 14340 14341 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843666655 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14341/statm): 531 226 485 147 0 384 0
[pid=14341] vsize: 2124
Raw data (/proc/14345/stat): 14345 (minisat+_64-bit) R 14341 14341 4419 0 -1 0 25562 0 0 0 55618 159 0 0 25 0 1 0 1843666660 105177088 25511 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14345/statm): 25678 25511 145 145 0 25533 0
[pid=14345] vsize: 102712
Current children cumulated CPU time (s) 557.78
Current children cumulated vsize (Kb) 104836

[startup+570.044 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 14345
Raw data (/proc/14341/stat): 14341 (minisat+_script) S 14340 14341 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843666655 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14341/statm): 531 226 485 147 0 384 0
[pid=14341] vsize: 2124
Raw data (/proc/14345/stat): 14345 (minisat+_64-bit) R 14341 14341 4419 0 -1 0 25562 0 0 0 56619 159 0 0 25 0 1 0 1843666660 105177088 25511 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14345/statm): 25678 25511 145 145 0 25533 0
[pid=14345] vsize: 102712
Current children cumulated CPU time (s) 567.79
Current children cumulated vsize (Kb) 104836

[startup+580.045 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 14345
Raw data (/proc/14341/stat): 14341 (minisat+_script) S 14340 14341 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843666655 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14341/statm): 531 226 485 147 0 384 0
[pid=14341] vsize: 2124
Raw data (/proc/14345/stat): 14345 (minisat+_64-bit) R 14341 14341 4419 0 -1 0 25562 0 0 0 57619 159 0 0 25 0 1 0 1843666660 105177088 25511 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14345/statm): 25678 25511 145 145 0 25533 0
[pid=14345] vsize: 102712
Current children cumulated CPU time (s) 577.79
Current children cumulated vsize (Kb) 104836

[startup+590.046 s]
Raw data (loadavg): 0.99 0.97 0.97 3/57 14345
Raw data (/proc/14341/stat): 14341 (minisat+_script) S 14340 14341 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843666655 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14341/statm): 531 226 485 147 0 384 0
[pid=14341] vsize: 2124
Raw data (/proc/14345/stat): 14345 (minisat+_64-bit) R 14341 14341 4419 0 -1 0 25562 0 0 0 58619 159 0 0 25 0 1 0 1843666660 105177088 25511 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14345/statm): 25678 25511 145 145 0 25533 0
[pid=14345] vsize: 102712
Current children cumulated CPU time (s) 587.79
Current children cumulated vsize (Kb) 104836

[startup+600.045 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 14345
Raw data (/proc/14341/stat): 14341 (minisat+_script) S 14340 14341 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843666655 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14341/statm): 531 226 485 147 0 384 0
[pid=14341] vsize: 2124
Raw data (/proc/14345/stat): 14345 (minisat+_64-bit) R 14341 14341 4419 0 -1 0 25562 0 0 0 59619 159 0 0 25 0 1 0 1843666660 105177088 25511 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14345/statm): 25678 25511 145 145 0 25533 0
[pid=14345] vsize: 102712
Current children cumulated CPU time (s) 597.79
Current children cumulated vsize (Kb) 104836

[startup+610.046 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 14345
Raw data (/proc/14341/stat): 14341 (minisat+_script) S 14340 14341 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843666655 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14341/statm): 531 226 485 147 0 384 0
[pid=14341] vsize: 2124
Raw data (/proc/14345/stat): 14345 (minisat+_64-bit) R 14341 14341 4419 0 -1 0 25562 0 0 0 60619 159 0 0 25 0 1 0 1843666660 105177088 25511 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14345/statm): 25678 25511 145 145 0 25533 0
[pid=14345] vsize: 102712
Current children cumulated CPU time (s) 607.79
Current children cumulated vsize (Kb) 104836

[startup+620.047 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 14345
Raw data (/proc/14341/stat): 14341 (minisat+_script) S 14340 14341 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843666655 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14341/statm): 531 226 485 147 0 384 0
[pid=14341] vsize: 2124
Raw data (/proc/14345/stat): 14345 (minisat+_64-bit) R 14341 14341 4419 0 -1 0 25562 0 0 0 61619 159 0 0 25 0 1 0 1843666660 105177088 25511 4294967295 134512640 135094434 3221224448 3221223104 134558164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14345/statm): 25678 25511 145 145 0 25533 0
[pid=14345] vsize: 102712
Current children cumulated CPU time (s) 617.79
Current children cumulated vsize (Kb) 104836

[startup+630.047 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 14345
Raw data (/proc/14341/stat): 14341 (minisat+_script) S 14340 14341 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843666655 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14341/statm): 531 226 485 147 0 384 0
[pid=14341] vsize: 2124
Raw data (/proc/14345/stat): 14345 (minisat+_64-bit) R 14341 14341 4419 0 -1 0 25562 0 0 0 62620 159 0 0 25 0 1 0 1843666660 105177088 25511 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14345/statm): 25678 25511 145 145 0 25533 0
[pid=14345] vsize: 102712
Current children cumulated CPU time (s) 627.8
Current children cumulated vsize (Kb) 104836

[startup+640.048 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 14345
Raw data (/proc/14341/stat): 14341 (minisat+_script) S 14340 14341 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843666655 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14341/statm): 531 226 485 147 0 384 0
[pid=14341] vsize: 2124
Raw data (/proc/14345/stat): 14345 (minisat+_64-bit) R 14341 14341 4419 0 -1 0 25562 0 0 0 63620 159 0 0 25 0 1 0 1843666660 105177088 25511 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14345/statm): 25678 25511 145 145 0 25533 0
[pid=14345] vsize: 102712
Current children cumulated CPU time (s) 637.8
Current children cumulated vsize (Kb) 104836

[startup+650.048 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 14345
Raw data (/proc/14341/stat): 14341 (minisat+_script) S 14340 14341 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843666655 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14341/statm): 531 226 485 147 0 384 0
[pid=14341] vsize: 2124
Raw data (/proc/14345/stat): 14345 (minisat+_64-bit) R 14341 14341 4419 0 -1 0 25562 0 0 0 64620 159 0 0 25 0 1 0 1843666660 105177088 25511 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14345/statm): 25678 25511 145 145 0 25533 0
[pid=14345] vsize: 102712
Current children cumulated CPU time (s) 647.8
Current children cumulated vsize (Kb) 104836

[startup+660.05 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 14345
Raw data (/proc/14341/stat): 14341 (minisat+_script) S 14340 14341 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843666655 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14341/statm): 531 226 485 147 0 384 0
[pid=14341] vsize: 2124
Raw data (/proc/14345/stat): 14345 (minisat+_64-bit) R 14341 14341 4419 0 -1 0 25562 0 0 0 65620 159 0 0 25 0 1 0 1843666660 105177088 25511 4294967295 134512640 135094434 3221224448 3221223060 134563049 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14345/statm): 25678 25511 145 145 0 25533 0
[pid=14345] vsize: 102712
Current children cumulated CPU time (s) 657.8
Current children cumulated vsize (Kb) 104836

[startup+670.051 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 14345
Raw data (/proc/14341/stat): 14341 (minisat+_script) S 14340 14341 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843666655 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14341/statm): 531 226 485 147 0 384 0
[pid=14341] vsize: 2124
Raw data (/proc/14345/stat): 14345 (minisat+_64-bit) R 14341 14341 4419 0 -1 0 25562 0 0 0 66621 159 0 0 25 0 1 0 1843666660 105177088 25511 4294967295 134512640 135094434 3221224448 3221223040 134557375 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14345/statm): 25678 25511 145 145 0 25533 0
[pid=14345] vsize: 102712
Current children cumulated CPU time (s) 667.81
Current children cumulated vsize (Kb) 104836

[startup+680.051 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 14345
Raw data (/proc/14341/stat): 14341 (minisat+_script) S 14340 14341 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843666655 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14341/statm): 531 226 485 147 0 384 0
[pid=14341] vsize: 2124
Raw data (/proc/14345/stat): 14345 (minisat+_64-bit) R 14341 14341 4419 0 -1 0 25563 0 0 0 67621 159 0 0 25 0 1 0 1843666660 105177088 25512 4294967295 134512640 135094434 3221224448 3221223104 134558208 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14345/statm): 25678 25512 145 145 0 25533 0
[pid=14345] vsize: 102712
Current children cumulated CPU time (s) 677.81
Current children cumulated vsize (Kb) 104836

[startup+690.052 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 14345
Raw data (/proc/14341/stat): 14341 (minisat+_script) S 14340 14341 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843666655 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14341/statm): 531 226 485 147 0 384 0
[pid=14341] vsize: 2124
Raw data (/proc/14345/stat): 14345 (minisat+_64-bit) R 14341 14341 4419 0 -1 0 25563 0 0 0 68621 159 0 0 25 0 1 0 1843666660 105177088 25512 4294967295 134512640 135094434 3221224448 3221223104 134558011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14345/statm): 25678 25512 145 145 0 25533 0
[pid=14345] vsize: 102712
Current children cumulated CPU time (s) 687.81
Current children cumulated vsize (Kb) 104836

[startup+700.053 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 14345
Raw data (/proc/14341/stat): 14341 (minisat+_script) S 14340 14341 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843666655 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14341/statm): 531 226 485 147 0 384 0
[pid=14341] vsize: 2124
Raw data (/proc/14345/stat): 14345 (minisat+_64-bit) R 14341 14341 4419 0 -1 0 25563 0 0 0 69621 159 0 0 25 0 1 0 1843666660 105177088 25512 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14345/statm): 25678 25512 145 145 0 25533 0
[pid=14345] vsize: 102712
Current children cumulated CPU time (s) 697.81
Current children cumulated vsize (Kb) 104836

[startup+710.053 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 14345
Raw data (/proc/14341/stat): 14341 (minisat+_script) S 14340 14341 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843666655 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14341/statm): 531 226 485 147 0 384 0
[pid=14341] vsize: 2124
Raw data (/proc/14345/stat): 14345 (minisat+_64-bit) R 14341 14341 4419 0 -1 0 25563 0 0 0 70621 159 0 0 25 0 1 0 1843666660 105177088 25512 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14345/statm): 25678 25512 145 145 0 25533 0
[pid=14345] vsize: 102712
Current children cumulated CPU time (s) 707.81
Current children cumulated vsize (Kb) 104836

[startup+720.053 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 14345
Raw data (/proc/14341/stat): 14341 (minisat+_script) S 14340 14341 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843666655 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14341/statm): 531 226 485 147 0 384 0
[pid=14341] vsize: 2124
Raw data (/proc/14345/stat): 14345 (minisat+_64-bit) R 14341 14341 4419 0 -1 0 25563 0 0 0 71622 159 0 0 25 0 1 0 1843666660 105177088 25512 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14345/statm): 25678 25512 145 145 0 25533 0
[pid=14345] vsize: 102712
Current children cumulated CPU time (s) 717.82
Current children cumulated vsize (Kb) 104836

[startup+730.054 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 14345
Raw data (/proc/14341/stat): 14341 (minisat+_script) S 14340 14341 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843666655 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14341/statm): 531 226 485 147 0 384 0
[pid=14341] vsize: 2124
Raw data (/proc/14345/stat): 14345 (minisat+_64-bit) R 14341 14341 4419 0 -1 0 25563 0 0 0 72622 159 0 0 25 0 1 0 1843666660 105177088 25512 4294967295 134512640 135094434 3221224448 3221223120 134555563 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14345/statm): 25678 25512 145 145 0 25533 0
[pid=14345] vsize: 102712
Current children cumulated CPU time (s) 727.82
Current children cumulated vsize (Kb) 104836

[startup+740.055 s]
Raw data (loadavg): 0.99 0.97 0.97 3/57 14345
Raw data (/proc/14341/stat): 14341 (minisat+_script) S 14340 14341 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843666655 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14341/statm): 531 226 485 147 0 384 0
[pid=14341] vsize: 2124
Raw data (/proc/14345/stat): 14345 (minisat+_64-bit) R 14341 14341 4419 0 -1 0 25563 0 0 0 73622 159 0 0 25 0 1 0 1843666660 105177088 25512 4294967295 134512640 135094434 3221224448 3221223104 134558016 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14345/statm): 25678 25512 145 145 0 25533 0
[pid=14345] vsize: 102712
Current children cumulated CPU time (s) 737.82
Current children cumulated vsize (Kb) 104836

[startup+750.056 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 14345
Raw data (/proc/14341/stat): 14341 (minisat+_script) S 14340 14341 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843666655 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14341/statm): 531 226 485 147 0 384 0
[pid=14341] vsize: 2124
Raw data (/proc/14345/stat): 14345 (minisat+_64-bit) R 14341 14341 4419 0 -1 0 25595 0 0 0 74622 160 0 0 25 0 1 0 1843666660 105308160 25544 4294967295 134512640 135094434 3221224448 3221223040 134557219 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14345/statm): 25710 25544 145 145 0 25565 0
[pid=14345] vsize: 102840
Current children cumulated CPU time (s) 747.83
Current children cumulated vsize (Kb) 104964

[startup+760.056 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 14345
Raw data (/proc/14341/stat): 14341 (minisat+_script) S 14340 14341 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843666655 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14341/statm): 531 226 485 147 0 384 0
[pid=14341] vsize: 2124
Raw data (/proc/14345/stat): 14345 (minisat+_64-bit) R 14341 14341 4419 0 -1 0 26049 0 0 0 75614 162 0 0 25 0 1 0 1843666660 107171840 25998 4294967295 134512640 135094434 3221224448 3221223088 134562098 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14345/statm): 26165 25998 145 145 0 26020 0
[pid=14345] vsize: 104660
Current children cumulated CPU time (s) 757.77
Current children cumulated vsize (Kb) 106784

[startup+770.057 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 14345
Raw data (/proc/14341/stat): 14341 (minisat+_script) S 14340 14341 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843666655 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14341/statm): 531 226 485 147 0 384 0
[pid=14341] vsize: 2124
Raw data (/proc/14345/stat): 14345 (minisat+_64-bit) R 14341 14341 4419 0 -1 0 26293 0 0 0 76610 164 0 0 25 0 1 0 1843666660 108171264 26242 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14345/statm): 26409 26242 145 145 0 26264 0
[pid=14345] vsize: 105636
Current children cumulated CPU time (s) 767.75
Current children cumulated vsize (Kb) 107760

[startup+780.057 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 14345
Raw data (/proc/14341/stat): 14341 (minisat+_script) S 14340 14341 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843666655 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14341/statm): 531 226 485 147 0 384 0
[pid=14341] vsize: 2124
Raw data (/proc/14345/stat): 14345 (minisat+_64-bit) R 14341 14341 4419 0 -1 0 26817 0 0 0 77602 168 0 0 25 0 1 0 1843666660 110317568 26766 4294967295 134512640 135094434 3221224448 3221223104 134557903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14345/statm): 26933 26766 145 145 0 26788 0
[pid=14345] vsize: 107732
Current children cumulated CPU time (s) 777.71
Current children cumulated vsize (Kb) 109856

[startup+790.058 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 14345
Raw data (/proc/14341/stat): 14341 (minisat+_script) S 14340 14341 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843666655 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14341/statm): 531 226 485 147 0 384 0
[pid=14341] vsize: 2124
Raw data (/proc/14345/stat): 14345 (minisat+_64-bit) R 14341 14341 4419 0 -1 0 27468 0 0 0 78592 171 0 0 25 0 1 0 1843666660 112984064 27417 4294967295 134512640 135094434 3221224448 3221223104 134557950 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14345/statm): 27584 27417 145 145 0 27439 0
[pid=14345] vsize: 110336
Current children cumulated CPU time (s) 787.64
Current children cumulated vsize (Kb) 112460

[startup+800.059 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 14345
Raw data (/proc/14341/stat): 14341 (minisat+_script) S 14340 14341 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843666655 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14341/statm): 531 226 485 147 0 384 0
[pid=14341] vsize: 2124
Raw data (/proc/14345/stat): 14345 (minisat+_64-bit) R 14341 14341 4419 0 -1 0 28645 0 0 0 79574 180 0 0 25 0 1 0 1843666660 117805056 28594 4294967295 134512640 135094434 3221224448 3221223040 134551876 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14345/statm): 28761 28594 145 145 0 28616 0
[pid=14345] vsize: 115044
Current children cumulated CPU time (s) 797.55
Current children cumulated vsize (Kb) 117168

[startup+810.059 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 14345
Raw data (/proc/14341/stat): 14341 (minisat+_script) S 14340 14341 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843666655 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14341/statm): 531 226 485 147 0 384 0
[pid=14341] vsize: 2124
Raw data (/proc/14345/stat): 14345 (minisat+_64-bit) R 14341 14341 4419 0 -1 0 29596 0 0 0 80560 185 0 0 25 0 1 0 1843666660 121679872 29545 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14345/statm): 29707 29545 145 145 0 29562 0
[pid=14345] vsize: 118828
Current children cumulated CPU time (s) 807.46
Current children cumulated vsize (Kb) 120952

[startup+820.06 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 14345
Raw data (/proc/14341/stat): 14341 (minisat+_script) S 14340 14341 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843666655 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14341/statm): 531 226 485 147 0 384 0
[pid=14341] vsize: 2124
Raw data (/proc/14345/stat): 14345 (minisat+_64-bit) R 14341 14341 4419 0 -1 0 30671 0 0 0 81542 192 0 0 25 0 1 0 1843666660 126582784 30620 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14345/statm): 30904 30620 145 145 0 30759 0
[pid=14345] vsize: 123616
Current children cumulated CPU time (s) 817.35
Current children cumulated vsize (Kb) 125740

[startup+830.06 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 14345
Raw data (/proc/14341/stat): 14341 (minisat+_script) S 14340 14341 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843666655 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14341/statm): 531 226 485 147 0 384 0
[pid=14341] vsize: 2124
Raw data (/proc/14345/stat): 14345 (minisat+_64-bit) R 14341 14341 4419 0 -1 0 30709 0 0 0 82542 192 0 0 25 0 1 0 1843666660 126738432 30658 4294967295 134512640 135094434 3221224448 3221223104 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14345/statm): 30942 30658 145 145 0 30797 0
[pid=14345] vsize: 123768
Current children cumulated CPU time (s) 827.35
Current children cumulated vsize (Kb) 125892

[startup+840.061 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 14345
Raw data (/proc/14341/stat): 14341 (minisat+_script) S 14340 14341 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843666655 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14341/statm): 531 226 485 147 0 384 0
[pid=14341] vsize: 2124
Raw data (/proc/14345/stat): 14345 (minisat+_64-bit) R 14341 14341 4419 0 -1 0 30709 0 0 0 83543 192 0 0 25 0 1 0 1843666660 126738432 30658 4294967295 134512640 135094434 3221224448 3221223104 134557914 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14345/statm): 30942 30658 145 145 0 30797 0
[pid=14345] vsize: 123768
Current children cumulated CPU time (s) 837.36
Current children cumulated vsize (Kb) 125892

[startup+850.062 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 14345
Raw data (/proc/14341/stat): 14341 (minisat+_script) S 14340 14341 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843666655 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14341/statm): 531 226 485 147 0 384 0
[pid=14341] vsize: 2124
Raw data (/proc/14345/stat): 14345 (minisat+_64-bit) R 14341 14341 4419 0 -1 0 30709 0 0 0 84543 192 0 0 25 0 1 0 1843666660 126738432 30658 4294967295 134512640 135094434 3221224448 3221223040 134557485 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14345/statm): 30942 30658 145 145 0 30797 0
[pid=14345] vsize: 123768
Current children cumulated CPU time (s) 847.36
Current children cumulated vsize (Kb) 125892

[startup+860.062 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 14345
Raw data (/proc/14341/stat): 14341 (minisat+_script) S 14340 14341 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843666655 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14341/statm): 531 226 485 147 0 384 0
[pid=14341] vsize: 2124
Raw data (/proc/14345/stat): 14345 (minisat+_64-bit) R 14341 14341 4419 0 -1 0 30709 0 0 0 85543 192 0 0 25 0 1 0 1843666660 126738432 30658 4294967295 134512640 135094434 3221224448 3221223040 134557202 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14345/statm): 30942 30658 145 145 0 30797 0
[pid=14345] vsize: 123768
Current children cumulated CPU time (s) 857.36
Current children cumulated vsize (Kb) 125892

[startup+870.063 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 14345
Raw data (/proc/14341/stat): 14341 (minisat+_script) S 14340 14341 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843666655 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14341/statm): 531 226 485 147 0 384 0
[pid=14341] vsize: 2124
Raw data (/proc/14345/stat): 14345 (minisat+_64-bit) R 14341 14341 4419 0 -1 0 30709 0 0 0 86543 192 0 0 25 0 1 0 1843666660 126738432 30658 4294967295 134512640 135094434 3221224448 3221223120 134555687 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14345/statm): 30942 30658 145 145 0 30797 0
[pid=14345] vsize: 123768
Current children cumulated CPU time (s) 867.36
Current children cumulated vsize (Kb) 125892

[startup+880.064 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 14345
Raw data (/proc/14341/stat): 14341 (minisat+_script) S 14340 14341 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843666655 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14341/statm): 531 226 485 147 0 384 0
[pid=14341] vsize: 2124
Raw data (/proc/14345/stat): 14345 (minisat+_64-bit) R 14341 14341 4419 0 -1 0 30709 0 0 0 87543 192 0 0 25 0 1 0 1843666660 126738432 30658 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14345/statm): 30942 30658 145 145 0 30797 0
[pid=14345] vsize: 123768
Current children cumulated CPU time (s) 877.36
Current children cumulated vsize (Kb) 125892

[startup+890.065 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 14345
Raw data (/proc/14341/stat): 14341 (minisat+_script) S 14340 14341 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843666655 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14341/statm): 531 226 485 147 0 384 0
[pid=14341] vsize: 2124
Raw data (/proc/14345/stat): 14345 (minisat+_64-bit) R 14341 14341 4419 0 -1 0 30709 0 0 0 88544 193 0 0 25 0 1 0 1843666660 126738432 30658 4294967295 134512640 135094434 3221224448 3221223104 134555975 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14345/statm): 30942 30658 145 145 0 30797 0
[pid=14345] vsize: 123768
Current children cumulated CPU time (s) 887.38
Current children cumulated vsize (Kb) 125892

[startup+900.065 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 14345
Raw data (/proc/14341/stat): 14341 (minisat+_script) S 14340 14341 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843666655 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14341/statm): 531 226 485 147 0 384 0
[pid=14341] vsize: 2124
Raw data (/proc/14345/stat): 14345 (minisat+_64-bit) R 14341 14341 4419 0 -1 0 30710 0 0 0 89544 193 0 0 25 0 1 0 1843666660 126738432 30659 4294967295 134512640 135094434 3221224448 3221223104 134557950 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14345/statm): 30942 30659 145 145 0 30797 0
[pid=14345] vsize: 123768
Current children cumulated CPU time (s) 897.38
Current children cumulated vsize (Kb) 125892

[startup+910.066 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 14345
Raw data (/proc/14341/stat): 14341 (minisat+_script) S 14340 14341 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843666655 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14341/statm): 531 226 485 147 0 384 0
[pid=14341] vsize: 2124
Raw data (/proc/14345/stat): 14345 (minisat+_64-bit) R 14341 14341 4419 0 -1 0 30711 0 0 0 90544 193 0 0 25 0 1 0 1843666660 126738432 30660 4294967295 134512640 135094434 3221224448 3221223060 134563049 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14345/statm): 30942 30660 145 145 0 30797 0
[pid=14345] vsize: 123768
Current children cumulated CPU time (s) 907.38
Current children cumulated vsize (Kb) 125892

[startup+920.067 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 14345
Raw data (/proc/14341/stat): 14341 (minisat+_script) S 14340 14341 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843666655 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14341/statm): 531 226 485 147 0 384 0
[pid=14341] vsize: 2124
Raw data (/proc/14345/stat): 14345 (minisat+_64-bit) R 14341 14341 4419 0 -1 0 30711 0 0 0 91544 193 0 0 25 0 1 0 1843666660 126738432 30660 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14345/statm): 30942 30660 145 145 0 30797 0
[pid=14345] vsize: 123768
Current children cumulated CPU time (s) 917.38
Current children cumulated vsize (Kb) 125892

[startup+930.067 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 14345
Raw data (/proc/14341/stat): 14341 (minisat+_script) S 14340 14341 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843666655 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14341/statm): 531 226 485 147 0 384 0
[pid=14341] vsize: 2124
Raw data (/proc/14345/stat): 14345 (minisat+_64-bit) R 14341 14341 4419 0 -1 0 30711 0 0 0 92545 193 0 0 25 0 1 0 1843666660 126738432 30660 4294967295 134512640 135094434 3221224448 3221223072 134557683 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14345/statm): 30942 30660 145 145 0 30797 0
[pid=14345] vsize: 123768
Current children cumulated CPU time (s) 927.39
Current children cumulated vsize (Kb) 125892

[startup+940.068 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 14345
Raw data (/proc/14341/stat): 14341 (minisat+_script) S 14340 14341 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843666655 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14341/statm): 531 226 485 147 0 384 0
[pid=14341] vsize: 2124
Raw data (/proc/14345/stat): 14345 (minisat+_64-bit) R 14341 14341 4419 0 -1 0 30711 0 0 0 93545 193 0 0 25 0 1 0 1843666660 126738432 30660 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14345/statm): 30942 30660 145 145 0 30797 0
[pid=14345] vsize: 123768
Current children cumulated CPU time (s) 937.39
Current children cumulated vsize (Kb) 125892

[startup+950.069 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 14345
Raw data (/proc/14341/stat): 14341 (minisat+_script) S 14340 14341 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843666655 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14341/statm): 531 226 485 147 0 384 0
[pid=14341] vsize: 2124
Raw data (/proc/14345/stat): 14345 (minisat+_64-bit) R 14341 14341 4419 0 -1 0 30711 0 0 0 94545 193 0 0 25 0 1 0 1843666660 126738432 30660 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14345/statm): 30942 30660 145 145 0 30797 0
[pid=14345] vsize: 123768
Current children cumulated CPU time (s) 947.39
Current children cumulated vsize (Kb) 125892

[startup+960.069 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 14345
Raw data (/proc/14341/stat): 14341 (minisat+_script) S 14340 14341 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843666655 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14341/statm): 531 226 485 147 0 384 0
[pid=14341] vsize: 2124
Raw data (/proc/14345/stat): 14345 (minisat+_64-bit) R 14341 14341 4419 0 -1 0 30711 0 0 0 95545 193 0 0 25 0 1 0 1843666660 126738432 30660 4294967295 134512640 135094434 3221224448 3221223120 134555680 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14345/statm): 30942 30660 145 145 0 30797 0
[pid=14345] vsize: 123768
Current children cumulated CPU time (s) 957.39
Current children cumulated vsize (Kb) 125892

[startup+970.07 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 14345
Raw data (/proc/14341/stat): 14341 (minisat+_script) S 14340 14341 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843666655 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14341/statm): 531 226 485 147 0 384 0
[pid=14341] vsize: 2124
Raw data (/proc/14345/stat): 14345 (minisat+_64-bit) R 14341 14341 4419 0 -1 0 30711 0 0 0 96545 193 0 0 25 0 1 0 1843666660 126738432 30660 4294967295 134512640 135094434 3221224448 3221222992 134562104 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14345/statm): 30942 30660 145 145 0 30797 0
[pid=14345] vsize: 123768
Current children cumulated CPU time (s) 967.39
Current children cumulated vsize (Kb) 125892

[startup+980.071 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 14345
Raw data (/proc/14341/stat): 14341 (minisat+_script) S 14340 14341 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843666655 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14341/statm): 531 226 485 147 0 384 0
[pid=14341] vsize: 2124
Raw data (/proc/14345/stat): 14345 (minisat+_64-bit) R 14341 14341 4419 0 -1 0 30711 0 0 0 97546 193 0 0 25 0 1 0 1843666660 126738432 30660 4294967295 134512640 135094434 3221224448 3221223072 134557726 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14345/statm): 30942 30660 145 145 0 30797 0
[pid=14345] vsize: 123768
Current children cumulated CPU time (s) 977.4
Current children cumulated vsize (Kb) 125892

[startup+990.071 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 14345
Raw data (/proc/14341/stat): 14341 (minisat+_script) S 14340 14341 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843666655 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14341/statm): 531 226 485 147 0 384 0
[pid=14341] vsize: 2124
Raw data (/proc/14345/stat): 14345 (minisat+_64-bit) R 14341 14341 4419 0 -1 0 30711 0 0 0 98546 193 0 0 25 0 1 0 1843666660 126738432 30660 4294967295 134512640 135094434 3221224448 3221223040 134557248 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14345/statm): 30942 30660 145 145 0 30797 0
[pid=14345] vsize: 123768
Current children cumulated CPU time (s) 987.4
Current children cumulated vsize (Kb) 125892

[startup+1000.07 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 14345
Raw data (/proc/14341/stat): 14341 (minisat+_script) S 14340 14341 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843666655 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14341/statm): 531 226 485 147 0 384 0
[pid=14341] vsize: 2124
Raw data (/proc/14345/stat): 14345 (minisat+_64-bit) R 14341 14341 4419 0 -1 0 30711 0 0 0 99546 193 0 0 25 0 1 0 1843666660 126738432 30660 4294967295 134512640 135094434 3221224448 3221223120 134556317 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14345/statm): 30942 30660 145 145 0 30797 0
[pid=14345] vsize: 123768
Current children cumulated CPU time (s) 997.4
Current children cumulated vsize (Kb) 125892

[startup+1010.07 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 14345
Raw data (/proc/14341/stat): 14341 (minisat+_script) S 14340 14341 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843666655 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14341/statm): 531 226 485 147 0 384 0
[pid=14341] vsize: 2124
Raw data (/proc/14345/stat): 14345 (minisat+_64-bit) R 14341 14341 4419 0 -1 0 30711 0 0 0 100546 193 0 0 25 0 1 0 1843666660 126738432 30660 4294967295 134512640 135094434 3221224448 3221223040 134557180 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14345/statm): 30942 30660 145 145 0 30797 0
[pid=14345] vsize: 123768
Current children cumulated CPU time (s) 1007.4
Current children cumulated vsize (Kb) 125892

[startup+1020.07 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 14345
Raw data (/proc/14341/stat): 14341 (minisat+_script) S 14340 14341 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843666655 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14341/statm): 531 226 485 147 0 384 0
[pid=14341] vsize: 2124
Raw data (/proc/14345/stat): 14345 (minisat+_64-bit) R 14341 14341 4419 0 -1 0 30711 0 0 0 101546 193 0 0 25 0 1 0 1843666660 126738432 30660 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14345/statm): 30942 30660 145 145 0 30797 0
[pid=14345] vsize: 123768
Current children cumulated CPU time (s) 1017.4
Current children cumulated vsize (Kb) 125892

[startup+1030.07 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 14345
Raw data (/proc/14341/stat): 14341 (minisat+_script) S 14340 14341 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843666655 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14341/statm): 531 226 485 147 0 384 0
[pid=14341] vsize: 2124
Raw data (/proc/14345/stat): 14345 (minisat+_64-bit) R 14341 14341 4419 0 -1 0 30711 0 0 0 102546 193 0 0 25 0 1 0 1843666660 126738432 30660 4294967295 134512640 135094434 3221224448 3221223104 134558240 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14345/statm): 30942 30660 145 145 0 30797 0
[pid=14345] vsize: 123768
Current children cumulated CPU time (s) 1027.4
Current children cumulated vsize (Kb) 125892

[startup+1040.07 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 14345
Raw data (/proc/14341/stat): 14341 (minisat+_script) S 14340 14341 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843666655 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14341/statm): 531 226 485 147 0 384 0
[pid=14341] vsize: 2124
Raw data (/proc/14345/stat): 14345 (minisat+_64-bit) R 14341 14341 4419 0 -1 0 30711 0 0 0 103546 193 0 0 25 0 1 0 1843666660 126738432 30660 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14345/statm): 30942 30660 145 145 0 30797 0
[pid=14345] vsize: 123768
Current children cumulated CPU time (s) 1037.4
Current children cumulated vsize (Kb) 125892

[startup+1050.07 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 14345
Raw data (/proc/14341/stat): 14341 (minisat+_script) S 14340 14341 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843666655 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14341/statm): 531 226 485 147 0 384 0
[pid=14341] vsize: 2124
Raw data (/proc/14345/stat): 14345 (minisat+_64-bit) R 14341 14341 4419 0 -1 0 30711 0 0 0 104547 193 0 0 25 0 1 0 1843666660 126738432 30660 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14345/statm): 30942 30660 145 145 0 30797 0
[pid=14345] vsize: 123768
Current children cumulated CPU time (s) 1047.41
Current children cumulated vsize (Kb) 125892

[startup+1060.07 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 14345
Raw data (/proc/14341/stat): 14341 (minisat+_script) S 14340 14341 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843666655 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14341/statm): 531 226 485 147 0 384 0
[pid=14341] vsize: 2124
Raw data (/proc/14345/stat): 14345 (minisat+_64-bit) R 14341 14341 4419 0 -1 0 30711 0 0 0 105547 193 0 0 25 0 1 0 1843666660 126738432 30660 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14345/statm): 30942 30660 145 145 0 30797 0
[pid=14345] vsize: 123768
Current children cumulated CPU time (s) 1057.41
Current children cumulated vsize (Kb) 125892

[startup+1070.07 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 14345
Raw data (/proc/14341/stat): 14341 (minisat+_script) S 14340 14341 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843666655 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14341/statm): 531 226 485 147 0 384 0
[pid=14341] vsize: 2124
Raw data (/proc/14345/stat): 14345 (minisat+_64-bit) R 14341 14341 4419 0 -1 0 30711 0 0 0 106547 193 0 0 25 0 1 0 1843666660 126738432 30660 4294967295 134512640 135094434 3221224448 3221223040 134557363 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14345/statm): 30942 30660 145 145 0 30797 0
[pid=14345] vsize: 123768
Current children cumulated CPU time (s) 1067.41
Current children cumulated vsize (Kb) 125892

[startup+1080.07 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 14345
Raw data (/proc/14341/stat): 14341 (minisat+_script) S 14340 14341 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843666655 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14341/statm): 531 226 485 147 0 384 0
[pid=14341] vsize: 2124
Raw data (/proc/14345/stat): 14345 (minisat+_64-bit) R 14341 14341 4419 0 -1 0 30711 0 0 0 107547 193 0 0 25 0 1 0 1843666660 126738432 30660 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14345/statm): 30942 30660 145 145 0 30797 0
[pid=14345] vsize: 123768
Current children cumulated CPU time (s) 1077.41
Current children cumulated vsize (Kb) 125892

[startup+1090.08 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 14345
Raw data (/proc/14341/stat): 14341 (minisat+_script) S 14340 14341 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843666655 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14341/statm): 531 226 485 147 0 384 0
[pid=14341] vsize: 2124
Raw data (/proc/14345/stat): 14345 (minisat+_64-bit) R 14341 14341 4419 0 -1 0 30711 0 0 0 108548 193 0 0 25 0 1 0 1843666660 126738432 30660 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14345/statm): 30942 30660 145 145 0 30797 0
[pid=14345] vsize: 123768
Current children cumulated CPU time (s) 1087.42
Current children cumulated vsize (Kb) 125892

[startup+1100.08 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 14345
Raw data (/proc/14341/stat): 14341 (minisat+_script) S 14340 14341 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843666655 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14341/statm): 531 226 485 147 0 384 0
[pid=14341] vsize: 2124
Raw data (/proc/14345/stat): 14345 (minisat+_64-bit) R 14341 14341 4419 0 -1 0 30915 0 0 0 109545 195 0 0 25 0 1 0 1843666660 127574016 30864 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14345/statm): 31146 30864 145 145 0 31001 0
[pid=14345] vsize: 124584
Current children cumulated CPU time (s) 1097.41
Current children cumulated vsize (Kb) 126708

[startup+1110.08 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 14345
Raw data (/proc/14341/stat): 14341 (minisat+_script) S 14340 14341 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843666655 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14341/statm): 531 226 485 147 0 384 0
[pid=14341] vsize: 2124
Raw data (/proc/14345/stat): 14345 (minisat+_64-bit) R 14341 14341 4419 0 -1 0 31399 0 0 0 110536 199 0 0 25 0 1 0 1843666660 129556480 31348 4294967295 134512640 135094434 3221224448 3221223104 134558004 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14345/statm): 31630 31348 145 145 0 31485 0
[pid=14345] vsize: 126520
Current children cumulated CPU time (s) 1107.36
Current children cumulated vsize (Kb) 128644

[startup+1120.08 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 14345
Raw data (/proc/14341/stat): 14341 (minisat+_script) S 14340 14341 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843666655 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14341/statm): 531 226 485 147 0 384 0
[pid=14341] vsize: 2124
Raw data (/proc/14345/stat): 14345 (minisat+_64-bit) R 14341 14341 4419 0 -1 0 31399 0 0 0 111536 199 0 0 25 0 1 0 1843666660 129556480 31348 4294967295 134512640 135094434 3221224448 3221223120 134555748 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14345/statm): 31630 31348 145 145 0 31485 0
[pid=14345] vsize: 126520
Current children cumulated CPU time (s) 1117.36
Current children cumulated vsize (Kb) 128644

[startup+1130.08 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 14345
Raw data (/proc/14341/stat): 14341 (minisat+_script) S 14340 14341 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843666655 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14341/statm): 531 226 485 147 0 384 0
[pid=14341] vsize: 2124
Raw data (/proc/14345/stat): 14345 (minisat+_64-bit) R 14341 14341 4419 0 -1 0 31399 0 0 0 112536 199 0 0 25 0 1 0 1843666660 129556480 31348 4294967295 134512640 135094434 3221224448 3221223040 134556789 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14345/statm): 31630 31348 145 145 0 31485 0
[pid=14345] vsize: 126520
Current children cumulated CPU time (s) 1127.36
Current children cumulated vsize (Kb) 128644

[startup+1140.08 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 14345
Raw data (/proc/14341/stat): 14341 (minisat+_script) S 14340 14341 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843666655 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14341/statm): 531 226 485 147 0 384 0
[pid=14341] vsize: 2124
Raw data (/proc/14345/stat): 14345 (minisat+_64-bit) R 14341 14341 4419 0 -1 0 31399 0 0 0 113537 199 0 0 25 0 1 0 1843666660 129556480 31348 4294967295 134512640 135094434 3221224448 3221223040 134557230 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14345/statm): 31630 31348 145 145 0 31485 0
[pid=14345] vsize: 126520
Current children cumulated CPU time (s) 1137.37
Current children cumulated vsize (Kb) 128644

[startup+1150.08 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 14345
Raw data (/proc/14341/stat): 14341 (minisat+_script) S 14340 14341 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843666655 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14341/statm): 531 226 485 147 0 384 0
[pid=14341] vsize: 2124
Raw data (/proc/14345/stat): 14345 (minisat+_64-bit) R 14341 14341 4419 0 -1 0 31399 0 0 0 114537 199 0 0 25 0 1 0 1843666660 129556480 31348 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14345/statm): 31630 31348 145 145 0 31485 0
[pid=14345] vsize: 126520
Current children cumulated CPU time (s) 1147.37
Current children cumulated vsize (Kb) 128644

[startup+1160.08 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 14345
Raw data (/proc/14341/stat): 14341 (minisat+_script) S 14340 14341 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843666655 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14341/statm): 531 226 485 147 0 384 0
[pid=14341] vsize: 2124
Raw data (/proc/14345/stat): 14345 (minisat+_64-bit) R 14341 14341 4419 0 -1 0 31399 0 0 0 115537 199 0 0 25 0 1 0 1843666660 129556480 31348 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14345/statm): 31630 31348 145 145 0 31485 0
[pid=14345] vsize: 126520
Current children cumulated CPU time (s) 1157.37
Current children cumulated vsize (Kb) 128644

[startup+1170.08 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 14345
Raw data (/proc/14341/stat): 14341 (minisat+_script) S 14340 14341 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843666655 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14341/statm): 531 226 485 147 0 384 0
[pid=14341] vsize: 2124
Raw data (/proc/14345/stat): 14345 (minisat+_64-bit) R 14341 14341 4419 0 -1 0 31399 0 0 0 116537 199 0 0 25 0 1 0 1843666660 129556480 31348 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14345/statm): 31630 31348 145 145 0 31485 0
[pid=14345] vsize: 126520
Current children cumulated CPU time (s) 1167.37
Current children cumulated vsize (Kb) 128644

[startup+1180.08 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 14345
Raw data (/proc/14341/stat): 14341 (minisat+_script) S 14340 14341 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843666655 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14341/statm): 531 226 485 147 0 384 0
[pid=14341] vsize: 2124
Raw data (/proc/14345/stat): 14345 (minisat+_64-bit) R 14341 14341 4419 0 -1 0 31399 0 0 0 117538 199 0 0 25 0 1 0 1843666660 129556480 31348 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14345/statm): 31630 31348 145 145 0 31485 0
[pid=14345] vsize: 126520
Current children cumulated CPU time (s) 1177.38
Current children cumulated vsize (Kb) 128644

[startup+1190.08 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 14345
Raw data (/proc/14341/stat): 14341 (minisat+_script) S 14340 14341 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843666655 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14341/statm): 531 226 485 147 0 384 0
[pid=14341] vsize: 2124
Raw data (/proc/14345/stat): 14345 (minisat+_64-bit) R 14341 14341 4419 0 -1 0 31399 0 0 0 118538 199 0 0 25 0 1 0 1843666660 129556480 31348 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14345/statm): 31630 31348 145 145 0 31485 0
[pid=14345] vsize: 126520
Current children cumulated CPU time (s) 1187.38
Current children cumulated vsize (Kb) 128644

[startup+1200.08 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 14345
Raw data (/proc/14341/stat): 14341 (minisat+_script) S 14340 14341 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843666655 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14341/statm): 531 226 485 147 0 384 0
[pid=14341] vsize: 2124
Raw data (/proc/14345/stat): 14345 (minisat+_64-bit) R 14341 14341 4419 0 -1 0 31399 0 0 0 119538 199 0 0 25 0 1 0 1843666660 129556480 31348 4294967295 134512640 135094434 3221224448 3221223104 134557884 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14345/statm): 31630 31348 145 145 0 31485 0
[pid=14345] vsize: 126520
Current children cumulated CPU time (s) 1197.38
Current children cumulated vsize (Kb) 128644

[startup+1210.08 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 14345
Raw data (/proc/14341/stat): 14341 (minisat+_script) S 14340 14341 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843666655 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14341/statm): 531 226 485 147 0 384 0
[pid=14341] vsize: 2124
Raw data (/proc/14345/stat): 14345 (minisat+_64-bit) R 14341 14341 4419 0 -1 0 31399 0 0 0 120538 199 0 0 25 0 1 0 1843666660 129556480 31348 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14345/statm): 31630 31348 145 145 0 31485 0
[pid=14345] vsize: 126520
Current children cumulated CPU time (s) 1207.38
Current children cumulated vsize (Kb) 128644



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.08 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 14345
Raw data (/proc/14341/stat): 14341 (minisat+_script) S 14340 14341 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843666655 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14341/statm): 531 226 485 147 0 384 0
[pid=14341] vsize: 2124
Raw data (/proc/14345/stat): 14345 (minisat+_64-bit) R 14341 14341 4419 0 -1 0 31399 0 0 0 120538 199 0 0 25 0 1 0 1843666660 129556480 31348 4294967295 134512640 135094434 3221224448 3221223104 134558395 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14345/statm): 31630 31348 145 145 0 31485 0
[pid=14345] vsize: 126520
Current children cumulated CPU time (s) 1207.38
Current children cumulated vsize (Kb) 128644

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

Child status: 0
Real time (s): 1210.15
CPU time (s): 1207.44
CPU user time (s): 1205.39
CPU system time (s): 2.05669
CPU usage (%): 99.7763
Max. virtual memory (cumulated for all children) (Kb): 128644

Verifier Data

ERROR: no interpretation found !