PB'05 competition: run trace

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:
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.
SOLVER DATA
This is the output of the solver (stdout and stderr).
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.
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

Name	normalized-opb/web/www.ps.uni-sb.de/~walser/benchmarks/course-ass/normalized-ws97-3.opb
MD5SUM	77c89bda49ebcdc0428e1292512864a9
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
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 numbers	21
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.07184
Number of variables	3300
Total number of constraints	5284
Number of constraints which are clauses	1364
Number of constraints which are cardinality constraints (but not clauses)	3920
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	1
Maximum length of a constraint	220
Trace number 31731

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

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        885732 kB
Buffers:         33388 kB
Cached:          90700 kB
SwapCached:        692 kB
Active:          63324 kB
Inactive:        63092 kB
HighTotal:      131008 kB
HighFree:        37408 kB
LowTotal:       903652 kB
LowFree:        848324 kB
SwapTotal:     2097136 kB
SwapFree:      2095440 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5780 kB
Slab:            16708 kB
Committed_AS:    92716 kB
PageTables:        332 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-05-27 06:16:33 (client local time) WITH STATUS 152 IN 1229.89 SECONDS
stats: 23111 7 1229.89 152
#### END LAUNCHER DATA ####
#### BEGIN 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]---> BDD-cost: 9262
c ---[2570]---> BDD-cost: 9262
c ---[2569]---> BDD-cost: 9262
c ---[2568]---> BDD-cost: 9262
c ---[2567]---> BDD-cost: 5237
c ---[2566]---> BDD-cost: 5237
c ---[2565]---> BDD-cost: 5237
c ---[2564]---> BDD-cost: 5237
c ---[2563]---> BDD-cost: 5237
c ---[2562]---> BDD-cost: 5237
c ---[2561]---> BDD-cost: 5237
c ---[2560]---> BDD-cost: 5237
c ---[2559]---> BDD-cost: 5237
c ---[2558]---> BDD-cost: 5528
c ---[2557]---> BDD-cost: 5528
c ---[2556]---> BDD-cost: 5528
c ---[2555]---> BDD-cost:  714
c ---[2554]---> BDD-cost:  714
c ---[2553]---> BDD-cost:  714
c ---[2552]---> BDD-cost:  714
c ---[2551]---> BDD-cost:  152
c ---[2550]---> BDD-cost:  152
c ---[2549]---> BDD-cost:  152
c ---[2548]---> BDD-cost:  152
c ---[2547]---> BDD-cost:  152
c ---[2546]---> BDD-cost:  152
c ---[2545]---> BDD-cost:  152
c ---[2544]---> BDD-cost:  152
c ---[2543]---> BDD-cost:  152
c ---[2542]---> BDD-cost:  680
c ---[2541]---> BDD-cost:  680
c ---[2540]---> BDD-cost:  680
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 |  537724  1601378 |  179241       0        0     nan |  0.000 % |
c |       100 |  537724  1601378 |  197165     100    20513   205.1 |  0.539 % |
c |       250 |  537724  1601378 |  216881     250    30153   120.6 |  0.539 % |
c |       475 |  537724  1601378 |  238569     475    42904    90.3 |  0.539 % |
c |       812 |  537724  1601378 |  262426     812    62967    77.5 |  0.539 % |
c ==============================================================================
c [1mFound solution: 95144[0m
c ---[   0]---> Sorter-cost:169346     Base: 5 5 5 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1071 |  888559  2420790 |  296186    1071    67716    63.2 |  0.539 % |
c |      1171 |  886591  2416313 |  325804    1135    68447    60.3 |  0.465 % |
c |      1322 |  881993  2405745 |  358385    1202    68484    57.0 |  1.002 % |
c |      1547 |  876233  2392448 |  394223    1321    68874    52.1 |  1.695 % |
c |      1884 |  868059  2373602 |  433645    1538    71418    46.4 |  2.666 % |
c |      2390 |  852586  2337840 |  477010    1744    70317    40.3 |  4.519 % |
c |      3149 |  829977  2285538 |  524711    2155    72038    33.4 |  7.292 % |
c |      4288 |  804829  2227238 |  577182    2893    76379    26.4 | 10.387 % |
c |      5996 |  781657  2173434 |  634900    3997    81027    20.3 | 13.283 % |
c |      8558 |  749674  2099071 |  698391    5470   100339    18.3 | 17.310 % |
c |     12403 |  738019  2071925 |  768230    8768   120385    13.7 | 18.800 % |
c |     18169 |  733693  2061818 |  845053   14221   190657    13.4 | 19.365 % |
c |     26819 |  733354  2061027 |  929558   22827  1100112    48.2 | 19.408 % |
c |     39794 |  731759  2057280 | 1022514   35568  2007540    56.4 | 19.625 % |
c |     59255 |  728070  2048646 | 1124765   54629  3564475    65.2 | 20.112 % |
c |     88447 |  725744  2043215 | 1237242   83530  4690156    56.1 | 20.416 % |
c ==============================================================================
c [1mFound solution: 54141[0m
c ---[   0]---> Sorter-cost:    9     Base: 5 5 5 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     92752 |  726510  2045044 |  242170   87820  4815470    54.8 | 20.416 % |
c |     92852 |  726510  2045044 |  266387   87920  4818138    54.8 | 20.580 % |
c |     93002 |  726510  2045044 |  293025   88070  4819634    54.7 | 20.580 % |
c |     93228 |  726510  2045044 |  322328   88296  4822025    54.6 | 20.580 % |
c |     93566 |  726510  2045044 |  354561   88634  4843897    54.7 | 20.580 % |
c |     94074 |  726510  2045044 |  390017   89142  4868709    54.6 | 20.580 % |
c |     94834 |  726510  2045044 |  429018   89902  4880678    54.3 | 20.580 % |
c |     95973 |  726500  2045021 |  471920   91036  4911845    54.0 | 20.581 % |
c |     97681 |  726500  2045021 |  519112   92744  5256023    56.7 | 20.581 % |
c |    100246 |  726500  2045021 |  571024   95309  5326091    55.9 | 20.581 % |
c ==============================================================================
c [1mFound solution: 26112[0m
c ---[   0]---> Sorter-cost:    9     Base: 5 5 5 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    101563 |  727410  2047175 |  242470   96626  5462862    56.5 | 20.581 % |
c |    101674 |  727410  2047175 |  266717   96737  5472944    56.6 | 20.752 % |
c |    101825 |  727410  2047175 |  293388   96888  5478028    56.5 | 20.752 % |
c |    102052 |  727410  2047175 |  322727   97115  5538379    57.0 | 20.752 % |
c |    102390 |  727410  2047175 |  355000   97453  5548312    56.9 | 20.752 % |
c |    102898 |  727410  2047175 |  390500   97961  5583025    57.0 | 20.752 % |
c |    103659 |  727410  2047175 |  429550   98722  5648162    57.2 | 20.752 % |
c |    104799 |  727410  2047175 |  472505   99862  5752991    57.6 | 20.752 % |
c ==============================================================================
c [1mFound solution: 20106[0m
c ---[   0]---> Sorter-cost:    8     Base: 5 5 5 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    105630 |  727458  2047310 |  242486  100693  5798081    57.6 | 20.752 % |
c |    105730 |  727458  2047310 |  266734  100793  5802915    57.6 | 20.751 % |
c |    105881 |  727458  2047310 |  293408  100944  5808157    57.5 | 20.751 % |
c |    106108 |  727458  2047310 |  322748  101171  5809597    57.4 | 20.751 % |
c |    106445 |  727458  2047310 |  355023  101508  5814013    57.3 | 20.751 % |
c |    106951 |  727458  2047310 |  390526  102014  5830785    57.2 | 20.751 % |
c |    107710 |  727458  2047310 |  429578  102773  5838502    56.8 | 20.751 % |
c |    108849 |  727458  2047310 |  472536  103912  5859063    56.4 | 20.751 % |
c |    110557 |  727186  2046677 |  519790  105615  5884633    55.7 | 20.787 % |
c |    113121 |  727186  2046677 |  571769  108179  5942474    54.9 | 20.787 % |
c |    116967 |  727186  2046677 |  628946  112025  6029587    53.8 | 20.787 % |
c |    122734 |  727186  2046677 |  691840  117792  6187151    52.5 | 20.787 % |
c |    131385 |  727186  2046677 |  761024  126443  6431502    50.9 | 20.787 % |
c |    144360 |  727186  2046677 |  837127  139418  6807271    48.8 | 20.787 % |
c |    163821 |  727186  2046677 |  920840  158879  7358830    46.3 | 20.787 % |
/oldhome/oroussel/solvers/minisat+_script: line 9:  1530 CPU time limit exceeded $XDIR/minisat+_64-bit_static -try "$@"
#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.85 0.94 0.90 2/55 1525
Raw data (stat): 1525 (runsolver) R 1524 8378 8377 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 738730362 1052672 99 4294967295 134512640 135381576 3221224480 3221219688 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0001 s]
Raw data (loadavg): 0.87 0.94 0.90 2/56 1530
Raw data (stat): 1525 (minisat+_script) S 1524 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738730362 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+20.0008 s]
Raw data (loadavg): 0.89 0.94 0.90 2/56 1530
Raw data (stat): 1525 (minisat+_script) S 1524 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738730362 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+30.0015 s]
Raw data (loadavg): 0.91 0.94 0.90 2/56 1530
Raw data (stat): 1525 (minisat+_script) S 1524 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738730362 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+40.0013 s]
Raw data (loadavg): 0.92 0.94 0.90 2/56 1530
Raw data (stat): 1525 (minisat+_script) S 1524 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738730362 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+50.0021 s]
Raw data (loadavg): 0.93 0.94 0.90 2/56 1530
Raw data (stat): 1525 (minisat+_script) S 1524 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738730362 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+60.0019 s]
Raw data (loadavg): 0.94 0.95 0.91 2/56 1530
Raw data (stat): 1525 (minisat+_script) S 1524 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738730362 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+70.0027 s]
Raw data (loadavg): 0.95 0.95 0.91 2/56 1530
Raw data (stat): 1525 (minisat+_script) S 1524 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738730362 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+80.0035 s]
Raw data (loadavg): 0.96 0.95 0.91 2/56 1530
Raw data (stat): 1525 (minisat+_script) S 1524 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738730362 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+90.004 s]
Raw data (loadavg): 0.96 0.95 0.91 2/56 1530
Raw data (stat): 1525 (minisat+_script) S 1524 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738730362 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+100.004 s]
Raw data (loadavg): 0.97 0.95 0.91 2/56 1530
Raw data (stat): 1525 (minisat+_script) S 1524 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738730362 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+110.004 s]
Raw data (loadavg): 0.97 0.95 0.91 2/56 1530
Raw data (stat): 1525 (minisat+_script) S 1524 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738730362 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+120.005 s]
Raw data (loadavg): 0.98 0.95 0.91 2/56 1530
Raw data (stat): 1525 (minisat+_script) S 1524 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738730362 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+130.004 s]
Raw data (loadavg): 0.98 0.95 0.91 2/56 1530
Raw data (stat): 1525 (minisat+_script) S 1524 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738730362 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+140.004 s]
Raw data (loadavg): 0.98 0.95 0.91 2/56 1530
Raw data (stat): 1525 (minisat+_script) S 1524 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738730362 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+150.006 s]
Raw data (loadavg): 0.98 0.95 0.91 2/56 1530
Raw data (stat): 1525 (minisat+_script) S 1524 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738730362 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+160.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/56 1530
Raw data (stat): 1525 (minisat+_script) S 1524 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738730362 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+170.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/56 1530
Raw data (stat): 1525 (minisat+_script) S 1524 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738730362 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+180.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/56 1530
Raw data (stat): 1525 (minisat+_script) S 1524 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738730362 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+190.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/56 1530
Raw data (stat): 1525 (minisat+_script) S 1524 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738730362 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+200.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/56 1530
Raw data (stat): 1525 (minisat+_script) S 1524 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738730362 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+210.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/56 1530
Raw data (stat): 1525 (minisat+_script) S 1524 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738730362 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+220.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/56 1530
Raw data (stat): 1525 (minisat+_script) S 1524 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738730362 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+230.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/56 1530
Raw data (stat): 1525 (minisat+_script) S 1524 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738730362 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+240.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/56 1530
Raw data (stat): 1525 (minisat+_script) S 1524 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738730362 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+250.007 s]
Raw data (loadavg): 1.22 1.01 0.93 2/56 1585
Raw data (stat): 1525 (minisat+_script) S 1524 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738730362 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+260.011 s]
Raw data (loadavg): 1.18 1.01 0.93 2/56 1585
Raw data (stat): 1525 (minisat+_script) S 1524 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738730362 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+270.012 s]
Raw data (loadavg): 1.15 1.01 0.93 2/56 1585
Raw data (stat): 1525 (minisat+_script) S 1524 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738730362 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+280.011 s]
Raw data (loadavg): 1.13 1.01 0.93 2/56 1585
Raw data (stat): 1525 (minisat+_script) S 1524 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738730362 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+290.011 s]
Raw data (loadavg): 1.11 1.01 0.93 2/56 1585
Raw data (stat): 1525 (minisat+_script) S 1524 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738730362 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+300.011 s]
Raw data (loadavg): 1.09 1.01 0.93 2/56 1587
Raw data (stat): 1525 (minisat+_script) S 1524 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738730362 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+310.01 s]
Raw data (loadavg): 1.08 1.01 0.93 2/56 1589
Raw data (stat): 1525 (minisat+_script) S 1524 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738730362 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+320.011 s]
Raw data (loadavg): 1.06 1.01 0.93 2/56 1589
Raw data (stat): 1525 (minisat+_script) S 1524 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738730362 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+330.012 s]
Raw data (loadavg): 1.05 1.01 0.93 2/56 1589
Raw data (stat): 1525 (minisat+_script) S 1524 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738730362 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+340.012 s]
Raw data (loadavg): 1.05 1.00 0.93 2/56 1589
Raw data (stat): 1525 (minisat+_script) S 1524 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738730362 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+350.012 s]
Raw data (loadavg): 1.04 1.00 0.93 2/56 1589
Raw data (stat): 1525 (minisat+_script) S 1524 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738730362 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+360.011 s]
Raw data (loadavg): 1.03 1.00 0.93 2/56 1589
Raw data (stat): 1525 (minisat+_script) S 1524 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738730362 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+370.012 s]
Raw data (loadavg): 1.03 1.00 0.93 2/56 1589
Raw data (stat): 1525 (minisat+_script) S 1524 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738730362 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+380.012 s]
Raw data (loadavg): 1.02 1.00 0.93 2/56 1589
Raw data (stat): 1525 (minisat+_script) S 1524 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738730362 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+390.012 s]
Raw data (loadavg): 1.02 1.00 0.93 2/56 1589
Raw data (stat): 1525 (minisat+_script) S 1524 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738730362 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+400.012 s]
Raw data (loadavg): 1.02 1.00 0.93 2/56 1589
Raw data (stat): 1525 (minisat+_script) S 1524 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738730362 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+410.012 s]
Raw data (loadavg): 1.01 1.00 0.93 2/56 1589
Raw data (stat): 1525 (minisat+_script) S 1524 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738730362 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+420.013 s]
Raw data (loadavg): 1.01 1.00 0.93 2/56 1589
Raw data (stat): 1525 (minisat+_script) S 1524 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738730362 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+430.014 s]
Raw data (loadavg): 1.01 1.00 0.93 2/56 1589
Raw data (stat): 1525 (minisat+_script) S 1524 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738730362 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+440.014 s]
Raw data (loadavg): 1.01 1.00 0.93 2/56 1589
Raw data (stat): 1525 (minisat+_script) S 1524 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738730362 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+450.014 s]
Raw data (loadavg): 1.00 1.00 0.93 2/56 1589
Raw data (stat): 1525 (minisat+_script) S 1524 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738730362 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+460.014 s]
Raw data (loadavg): 1.00 1.00 0.93 2/56 1589
Raw data (stat): 1525 (minisat+_script) S 1524 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738730362 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+470.015 s]
Raw data (loadavg): 1.00 1.00 0.93 2/56 1589
Raw data (stat): 1525 (minisat+_script) S 1524 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738730362 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+480.015 s]
Raw data (loadavg): 1.00 1.00 0.93 2/56 1589
Raw data (stat): 1525 (minisat+_script) S 1524 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738730362 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+490.014 s]
Raw data (loadavg): 1.00 1.00 0.93 2/56 1589
Raw data (stat): 1525 (minisat+_script) S 1524 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738730362 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+500.014 s]
Raw data (loadavg): 1.00 1.00 0.93 2/56 1589
Raw data (stat): 1525 (minisat+_script) S 1524 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738730362 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+510.014 s]
Raw data (loadavg): 1.00 1.00 0.93 2/56 1589
Raw data (stat): 1525 (minisat+_script) S 1524 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738730362 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+520.015 s]
Raw data (loadavg): 1.00 1.00 0.93 2/56 1589
Raw data (stat): 1525 (minisat+_script) S 1524 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738730362 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+530.015 s]
Raw data (loadavg): 1.00 1.00 0.93 2/56 1589
Raw data (stat): 1525 (minisat+_script) S 1524 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738730362 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+540.014 s]
Raw data (loadavg): 1.00 1.00 0.93 2/56 1589
Raw data (stat): 1525 (minisat+_script) S 1524 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738730362 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+550.015 s]
Raw data (loadavg): 1.00 1.00 0.93 2/56 1589
Raw data (stat): 1525 (minisat+_script) S 1524 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738730362 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+560.015 s]
Raw data (loadavg): 1.00 1.00 0.93 2/56 1591
Raw data (stat): 1525 (minisat+_script) S 1524 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738730362 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+570.016 s]
Raw data (loadavg): 1.00 1.00 0.93 2/56 1591
Raw data (stat): 1525 (minisat+_script) S 1524 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738730362 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+580.016 s]
Raw data (loadavg): 1.00 1.00 0.93 2/56 1591
Raw data (stat): 1525 (minisat+_script) S 1524 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738730362 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+590.016 s]
Raw data (loadavg): 1.00 1.00 0.93 2/56 1591
Raw data (stat): 1525 (minisat+_script) S 1524 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738730362 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+600.016 s]
Raw data (loadavg): 1.00 1.00 0.93 2/56 1591
Raw data (stat): 1525 (minisat+_script) S 1524 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738730362 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+610.016 s]
Raw data (loadavg): 1.00 1.00 0.93 2/56 1591
Raw data (stat): 1525 (minisat+_script) S 1524 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738730362 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+620.017 s]
Raw data (loadavg): 1.00 1.00 0.93 2/56 1591
Raw data (stat): 1525 (minisat+_script) S 1524 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738730362 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+630.017 s]
Raw data (loadavg): 1.00 1.00 0.93 2/56 1591
Raw data (stat): 1525 (minisat+_script) S 1524 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738730362 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+640.016 s]
Raw data (loadavg): 1.00 1.00 0.93 2/56 1591
Raw data (stat): 1525 (minisat+_script) S 1524 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738730362 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+650.016 s]
Raw data (loadavg): 1.00 1.00 0.93 2/56 1591
Raw data (stat): 1525 (minisat+_script) S 1524 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738730362 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+660.016 s]
Raw data (loadavg): 1.00 1.00 0.93 2/56 1591
Raw data (stat): 1525 (minisat+_script) S 1524 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738730362 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+670.015 s]
Raw data (loadavg): 1.00 1.00 0.93 2/56 1591
Raw data (stat): 1525 (minisat+_script) S 1524 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738730362 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+680.016 s]
Raw data (loadavg): 1.08 1.02 0.93 2/56 1591
Raw data (stat): 1525 (minisat+_script) S 1524 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738730362 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+690.017 s]
Raw data (loadavg): 1.14 1.03 0.94 2/56 1591
Raw data (stat): 1525 (minisat+_script) S 1524 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738730362 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+700.017 s]
Raw data (loadavg): 1.12 1.03 0.94 2/56 1591
Raw data (stat): 1525 (minisat+_script) S 1524 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738730362 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+710.017 s]
Raw data (loadavg): 1.10 1.03 0.94 2/56 1591
Raw data (stat): 1525 (minisat+_script) S 1524 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738730362 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+720.016 s]
Raw data (loadavg): 1.08 1.03 0.94 2/56 1591
Raw data (stat): 1525 (minisat+_script) S 1524 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738730362 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+730.016 s]
Raw data (loadavg): 1.07 1.03 0.94 2/56 1591
Raw data (stat): 1525 (minisat+_script) S 1524 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738730362 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+740.016 s]
Raw data (loadavg): 1.06 1.03 0.94 2/56 1591
Raw data (stat): 1525 (minisat+_script) S 1524 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738730362 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+750.016 s]
Raw data (loadavg): 1.05 1.02 0.94 2/56 1591
Raw data (stat): 1525 (minisat+_script) S 1524 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738730362 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+760.017 s]
Raw data (loadavg): 1.04 1.02 0.94 2/56 1591
Raw data (stat): 1525 (minisat+_script) S 1524 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738730362 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+770.016 s]
Raw data (loadavg): 1.04 1.02 0.94 2/56 1591
Raw data (stat): 1525 (minisat+_script) S 1524 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738730362 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+780.016 s]
Raw data (loadavg): 1.03 1.02 0.94 2/56 1591
Raw data (stat): 1525 (minisat+_script) S 1524 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738730362 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+790.016 s]
Raw data (loadavg): 1.02 1.02 0.94 2/56 1591
Raw data (stat): 1525 (minisat+_script) S 1524 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738730362 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+800.016 s]
Raw data (loadavg): 1.02 1.02 0.94 2/56 1591
Raw data (stat): 1525 (minisat+_script) S 1524 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738730362 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+810.016 s]
Raw data (loadavg): 1.02 1.02 0.94 2/56 1591
Raw data (stat): 1525 (minisat+_script) S 1524 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738730362 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+820.015 s]
Raw data (loadavg): 1.01 1.02 0.94 2/56 1591
Raw data (stat): 1525 (minisat+_script) S 1524 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738730362 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+830.015 s]
Raw data (loadavg): 1.01 1.02 0.94 2/56 1591
Raw data (stat): 1525 (minisat+_script) S 1524 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738730362 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+840.015 s]
Raw data (loadavg): 1.01 1.02 0.94 2/56 1591
Raw data (stat): 1525 (minisat+_script) S 1524 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738730362 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+850.015 s]
Raw data (loadavg): 1.01 1.01 0.94 2/56 1591
Raw data (stat): 1525 (minisat+_script) S 1524 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738730362 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+860.014 s]
Raw data (loadavg): 1.01 1.01 0.94 2/56 1591
Raw data (stat): 1525 (minisat+_script) S 1524 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738730362 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+870.015 s]
Raw data (loadavg): 1.00 1.01 0.94 2/56 1591
Raw data (stat): 1525 (minisat+_script) S 1524 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738730362 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+880.015 s]
Raw data (loadavg): 1.00 1.01 0.94 2/56 1591
Raw data (stat): 1525 (minisat+_script) S 1524 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738730362 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+890.015 s]
Raw data (loadavg): 1.00 1.01 0.94 2/56 1591
Raw data (stat): 1525 (minisat+_script) S 1524 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738730362 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+900.014 s]
Raw data (loadavg): 1.00 1.01 0.94 2/56 1591
Raw data (stat): 1525 (minisat+_script) S 1524 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738730362 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+910.015 s]
Raw data (loadavg): 1.00 1.01 0.94 2/56 1591
Raw data (stat): 1525 (minisat+_script) S 1524 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738730362 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+920.015 s]
Raw data (loadavg): 1.00 1.01 0.94 2/56 1591
Raw data (stat): 1525 (minisat+_script) S 1524 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738730362 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+930.015 s]
Raw data (loadavg): 1.00 1.01 0.94 2/56 1591
Raw data (stat): 1525 (minisat+_script) S 1524 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738730362 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+940.015 s]
Raw data (loadavg): 1.00 1.01 0.94 2/56 1591
Raw data (stat): 1525 (minisat+_script) S 1524 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738730362 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+950.015 s]
Raw data (loadavg): 1.00 1.00 0.94 2/56 1591
Raw data (stat): 1525 (minisat+_script) S 1524 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738730362 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+960.015 s]
Raw data (loadavg): 1.00 1.00 0.94 2/56 1591
Raw data (stat): 1525 (minisat+_script) S 1524 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738730362 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+970.015 s]
Raw data (loadavg): 1.00 1.00 0.94 2/56 1591
Raw data (stat): 1525 (minisat+_script) S 1524 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738730362 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+980.016 s]
Raw data (loadavg): 1.00 1.00 0.94 2/56 1591
Raw data (stat): 1525 (minisat+_script) S 1524 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738730362 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+990.016 s]
Raw data (loadavg): 1.00 1.00 0.94 2/56 1591
Raw data (stat): 1525 (minisat+_script) S 1524 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738730362 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1000.02 s]
Raw data (loadavg): 1.00 1.00 0.94 2/56 1591
Raw data (stat): 1525 (minisat+_script) S 1524 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738730362 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1010.02 s]
Raw data (loadavg): 1.00 1.00 0.94 2/56 1591
Raw data (stat): 1525 (minisat+_script) S 1524 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738730362 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1020.02 s]
Raw data (loadavg): 1.00 1.00 0.94 2/56 1591
Raw data (stat): 1525 (minisat+_script) S 1524 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738730362 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1030.02 s]
Raw data (loadavg): 1.00 1.00 0.94 2/56 1591
Raw data (stat): 1525 (minisat+_script) S 1524 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738730362 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1040.02 s]
Raw data (loadavg): 1.00 1.00 0.94 2/56 1591
Raw data (stat): 1525 (minisat+_script) S 1524 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738730362 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1050.02 s]
Raw data (loadavg): 1.00 1.00 0.94 2/56 1591
Raw data (stat): 1525 (minisat+_script) S 1524 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738730362 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1060.02 s]
Raw data (loadavg): 1.00 1.00 0.94 2/56 1591
Raw data (stat): 1525 (minisat+_script) S 1524 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738730362 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1070.02 s]
Raw data (loadavg): 1.00 1.00 0.94 2/56 1591
Raw data (stat): 1525 (minisat+_script) S 1524 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738730362 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1080.02 s]
Raw data (loadavg): 1.00 1.00 0.94 2/56 1591
Raw data (stat): 1525 (minisat+_script) S 1524 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738730362 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1090.02 s]
Raw data (loadavg): 1.00 1.00 0.94 2/56 1591
Raw data (stat): 1525 (minisat+_script) S 1524 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738730362 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1100.01 s]
Raw data (loadavg): 1.00 1.00 0.94 2/56 1591
Raw data (stat): 1525 (minisat+_script) S 1524 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738730362 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1110.02 s]
Raw data (loadavg): 1.00 1.00 0.94 2/56 1591
Raw data (stat): 1525 (minisat+_script) S 1524 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738730362 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1120.02 s]
Raw data (loadavg): 1.00 1.00 0.94 2/56 1591
Raw data (stat): 1525 (minisat+_script) S 1524 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738730362 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1130.02 s]
Raw data (loadavg): 1.00 1.00 0.94 2/56 1591
Raw data (stat): 1525 (minisat+_script) S 1524 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738730362 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1140.02 s]
Raw data (loadavg): 1.00 1.00 0.94 2/56 1591
Raw data (stat): 1525 (minisat+_script) S 1524 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738730362 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1150.01 s]
Raw data (loadavg): 1.00 1.00 0.94 2/56 1591
Raw data (stat): 1525 (minisat+_script) S 1524 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738730362 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1160.02 s]
Raw data (loadavg): 1.00 1.00 0.94 2/56 1591
Raw data (stat): 1525 (minisat+_script) S 1524 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738730362 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1170.02 s]
Raw data (loadavg): 1.00 1.00 0.94 2/56 1591
Raw data (stat): 1525 (minisat+_script) S 1524 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738730362 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1180.02 s]
Raw data (loadavg): 1.00 1.00 0.94 2/56 1591
Raw data (stat): 1525 (minisat+_script) S 1524 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738730362 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1190.02 s]
Raw data (loadavg): 1.00 1.00 0.94 2/56 1591
Raw data (stat): 1525 (minisat+_script) S 1524 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738730362 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1200.02 s]
Raw data (loadavg): 1.00 1.00 0.94 2/56 1591
Raw data (stat): 1525 (minisat+_script) S 1524 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738730362 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1210.02 s]
Raw data (loadavg): 1.00 1.00 0.94 2/56 1591
Raw data (stat): 1525 (minisat+_script) S 1524 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738730362 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1220.02 s]
Raw data (loadavg): 1.00 1.00 0.94 2/56 1591
Raw data (stat): 1525 (minisat+_script) S 1524 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738730362 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1229.74 s]
Raw data (loadavg): 1.00 1.00 0.94 1/54 1591
Raw data (stat): 1525 (minisat+_script) S 1524 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 738730362 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 0

Child status: 152
Real time (s): 1229.74
CPU time (s): 1229.89
CPU user time (s): 1228.94
CPU system time (s): 0.955854
CPU usage (%): 100.012
Max. virtual memory (Kb): 2124
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####