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 5651

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc25 THE 2005-04-14 01:17:58 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=4117 boxname=wulflinc25 idbench=357 idsolver=11 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  77c89bda49ebcdc0428e1292512864a9  /oldhome/oroussel/tmp/wulflinc25/normalized-ws97-3.opb
REAL COMMAND:  minisat+ -S /oldhome/oroussel/tmp/wulflinc25/normalized-ws97-3.opb /oldhome/oroussel/tmp/wulflinc25/normalized-ws97-3.opb
IDLAUNCH: 4117
/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:        894064 kB
Buffers:         34484 kB
Cached:          71492 kB
SwapCached:         36 kB
Active:          48816 kB
Inactive:        60080 kB
HighTotal:      131008 kB
HighFree:        55804 kB
LowTotal:       903652 kB
LowFree:        838260 kB
SwapTotal:     2097892 kB
SwapFree:      2097856 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6920 kB
Slab:            26196 kB
Committed_AS:    63480 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-14 01:38:00 (client local time) WITH STATUS 0 IN 1200.28 SECONDS
stats: 4117 7 1200.28 0
#### 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]---> 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 =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |   61403   205934 |   18420       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/14458          
c   -- var.elim.:  2000/14458          
c   -- var.elim.:  3000/14458          
c   -- var.elim.:  4000/14458          
c   -- var.elim.:  5000/14458          
c   -- var.elim.:  6000/14458          
c   -- var.elim.:  7000/14458          
c   -- var.elim.:  8000/14458          
c   -- var.elim.:  9000/14458          
c   -- var.elim.:  10000/14458          
c   -- var.elim.:  11000/14458          
c   -- var.elim.:  12000/14458          
c   -- var.elim.:  13000/14458          
c   -- var.elim.:  14000/14458          
c   -- var.elim.:  14458/14458          
c   -- var.elim.:  1000/4045          
c   -- var.elim.:  2000/4045          
c   -- var.elim.:  3000/4045          
c   -- var.elim.:  4000/4045          
c   -- var.elim.:  4045/4045          
c   -- var.elim.:  18/18          
c   -- subsuming                       
c   -- var.elim.:  1000/1985          
c   -- var.elim.:  1985/1985          
c   -- var.elim.:  1000/1767          
c   -- var.elim.:  1767/1767          
c   -- subsuming                       
c   -- var.elim.:  672/672          
c |         0 |   57720   193893 |      --       0       --      -- |     --   | -3586/-9758
c |         0 |   57720   193893 |   23088       0        0     nan |  0.000 % |
c |       100 |   57720   193893 |   25396     100     1809    18.1 |  6.179 % |
c |       250 |   57720   193893 |   27936     250     2956    11.8 |  6.178 % |
c |       475 |   57720   193893 |   30730     475     3834     8.1 |  6.178 % |
c |       815 |   57720   193893 |   33803     815     5484     6.7 |  6.178 % |
c |      1321 |   57716   193870 |   37180    1318    11222     8.5 |  6.186 % |
c |      2080 |   57716   193870 |   40898    2077    14655     7.1 |  6.186 % |
c |      3219 |   57716   193870 |   44988    3216    21907     6.8 |  6.186 % |
c |      4927 |   57716   193870 |   49487    4924    43631     8.9 |  6.186 % |
c |      7489#### 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.99 1.00 0.92 2/54 32539
Raw data (stat): 32539 (runsolver) R 32538 28099 28098 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 480579141 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0008 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 32539
Raw data (stat): 32539 (minisat+) R 32538 28099 28098 0 -1 0 3872 0 0 0 988 10 0 0 25 0 1 0 480579141 16351232 3554 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3992 3554 603 41 0 3951 0
vsize: 15968
[startup+20.0012 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 32539
Raw data (stat): 32539 (minisat+) R 32538 28099 28098 0 -1 0 5163 0 0 0 1984 14 0 0 25 0 1 0 480579141 21528576 4845 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5256 4845 603 41 0 5215 0
vsize: 21024
[startup+30.0015 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 32539
Raw data (stat): 32539 (minisat+) R 32538 28099 28098 0 -1 0 6264 0 0 0 2980 18 0 0 25 0 1 0 480579141 26165248 5946 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6388 5946 603 41 0 6347 0
vsize: 25552
[startup+40.0014 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 32539
Raw data (stat): 32539 (minisat+) R 32538 28099 28098 0 -1 0 6992 0 0 0 3978 20 0 0 25 0 1 0 480579141 29081600 6674 4294967295 134512640 134672761 3221224576 3221223760 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7100 6674 603 41 0 7059 0
vsize: 28400
[startup+50.002 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 32539
Raw data (stat): 32539 (minisat+) R 32538 28099 28098 0 -1 0 7517 0 0 0 4976 22 0 0 25 0 1 0 480579141 31191040 7199 4294967295 134512640 134672761 3221224576 3221223760 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7615 7199 603 41 0 7574 0
vsize: 30460
[startup+60.0013 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 32539
Raw data (stat): 32539 (minisat+) R 32538 28099 28098 0 -1 0 7952 0 0 0 5975 24 0 0 25 0 1 0 480579141 32927744 7634 4294967295 134512640 134672761 3221224576 3221223760 134615739 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8039 7634 603 41 0 7998 0
vsize: 32156
[startup+70.0012 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 32539
Raw data (stat): 32539 (minisat+) R 32538 28099 28098 0 -1 0 8333 0 0 0 6974 25 0 0 25 0 1 0 480579141 34783232 8015 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8492 8015 603 41 0 8451 0
vsize: 33968
[startup+80.0018 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 32539
Raw data (stat): 32539 (minisat+) R 32538 28099 28098 0 -1 0 8702 0 0 0 7973 26 0 0 25 0 1 0 480579141 36229120 8384 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8845 8384 603 41 0 8804 0
vsize: 35380
[startup+90.0011 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 32539
Raw data (stat): 32539 (minisat+) R 32538 28099 28098 0 -1 0 9067 0 0 0 8972 27 0 0 25 0 1 0 480579141 37847040 8749 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9240 8749 603 41 0 9199 0
vsize: 36960
[startup+100.002 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 32539
Raw data (stat): 32539 (minisat+) R 32538 28099 28098 0 -1 0 9389 0 0 0 9971 29 0 0 25 0 1 0 480579141 39161856 9071 4294967295 134512640 134672761 3221224576 3221223760 134615632 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9561 9071 603 41 0 9520 0
vsize: 38244
[startup+110.003 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 32539
Raw data (stat): 32539 (minisat+) R 32538 28099 28098 0 -1 0 9725 0 0 0 10970 30 0 0 25 0 1 0 480579141 40509440 9407 4294967295 134512640 134672761 3221224576 3221223760 134615940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9890 9407 603 41 0 9849 0
vsize: 39560
[startup+120.002 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 32539
Raw data (stat): 32539 (minisat+) R 32538 28099 28098 0 -1 0 10351 0 0 0 11967 33 0 0 25 0 1 0 480579141 43032576 10033 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10506 10033 603 41 0 10465 0
vsize: 42024
[startup+130.002 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 32539
Raw data (stat): 32539 (minisat+) R 32538 28099 28098 0 -1 0 10840 0 0 0 12966 34 0 0 25 0 1 0 480579141 44720128 10425 4294967295 134512640 134672761 3221224576 3221223344 1075352446 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10918 10425 603 41 0 10877 0
vsize: 43672
[startup+140.001 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 32539
Raw data (stat): 32539 (minisat+) R 32538 28099 28098 0 -1 0 10840 0 0 0 13966 34 0 0 25 0 1 0 480579141 44720128 10425 4294967295 134512640 134672761 3221224576 3221223760 134615571 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10918 10425 603 41 0 10877 0
vsize: 43672
[startup+150.002 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 32539
Raw data (stat): 32539 (minisat+) R 32538 28099 28098 0 -1 0 10840 0 0 0 14966 35 0 0 25 0 1 0 480579141 44720128 10425 4294967295 134512640 134672761 3221224576 3221223616 134603459 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10918 10425 603 41 0 10877 0
vsize: 43672
[startup+160.002 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 32539
Raw data (stat): 32539 (minisat+) R 32538 28099 28098 0 -1 0 10840 0 0 0 15966 35 0 0 25 0 1 0 480579141 44720128 10425 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10918 10425 603 41 0 10877 0
vsize: 43672
[startup+170.001 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 32539
Raw data (stat): 32539 (minisat+) R 32538 28099 28098 0 -1 0 10840 0 0 0 16966 35 0 0 25 0 1 0 480579141 44720128 10425 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10918 10425 603 41 0 10877 0
vsize: 43672
[startup+180.002 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 32539
Raw data (stat): 32539 (minisat+) R 32538 28099 28098 0 -1 0 10840 0 0 0 17966 35 0 0 25 0 1 0 480579141 44720128 10425 4294967295 134512640 134672761 3221224576 3221223760 134615693 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10918 10425 603 41 0 10877 0
vsize: 43672
[startup+190.001 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 32539
Raw data (stat): 32539 (minisat+) R 32538 28099 28098 0 -1 0 10840 0 0 0 18967 35 0 0 25 0 1 0 480579141 44720128 10425 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10918 10425 603 41 0 10877 0
vsize: 43672
[startup+200.002 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 32539
Raw data (stat): 32539 (minisat+) R 32538 28099 28098 0 -1 0 10896 0 0 0 19967 35 0 0 25 0 1 0 480579141 44982272 10481 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10982 10481 603 41 0 10941 0
vsize: 43928
[startup+210.001 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 32539
Raw data (stat): 32539 (minisat+) R 32538 28099 28098 0 -1 0 11533 0 0 0 20965 37 0 0 25 0 1 0 480579141 47620096 11118 4294967295 134512640 134672761 3221224576 3221223700 134566027 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11626 11118 603 41 0 11585 0
vsize: 46504
[startup+220.001 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 32539
Raw data (stat): 32539 (minisat+) R 32538 28099 28098 0 -1 0 12086 0 0 0 21964 38 0 0 25 0 1 0 480579141 49864704 11671 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12174 11671 603 41 0 12133 0
vsize: 48696
[startup+230.002 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 32539
Raw data (stat): 32539 (minisat+) R 32538 28099 28098 0 -1 0 12567 0 0 0 22961 41 0 0 25 0 1 0 480579141 51859456 12152 4294967295 134512640 134672761 3221224576 3221223760 134615564 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12661 12152 603 41 0 12620 0
vsize: 50644
[startup+240.002 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 32539
Raw data (stat): 32539 (minisat+) R 32538 28099 28098 0 -1 0 13041 0 0 0 23960 42 0 0 25 0 1 0 480579141 53825536 12626 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13141 12626 603 41 0 13100 0
vsize: 52564
[startup+250.003 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 32539
Raw data (stat): 32539 (minisat+) R 32538 28099 28098 0 -1 0 13538 0 0 0 24959 44 0 0 25 0 1 0 480579141 55816192 13123 4294967295 134512640 134672761 3221224576 3221223776 134610709 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13627 13123 603 41 0 13586 0
vsize: 54508
[startup+260.004 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 32539
Raw data (stat): 32539 (minisat+) R 32538 28099 28098 0 -1 0 14086 0 0 0 25957 46 0 0 25 0 1 0 480579141 58064896 13671 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14176 13671 603 41 0 14135 0
vsize: 56704
[startup+270.003 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 32539
Raw data (stat): 32539 (minisat+) R 32538 28099 28098 0 -1 0 14692 0 0 0 26956 47 0 0 25 0 1 0 480579141 60575744 14277 4294967295 134512640 134672761 3221224576 3221223680 134604307 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14789 14277 603 41 0 14748 0
vsize: 59156
[startup+280.003 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 32539
Raw data (stat): 32539 (minisat+) R 32538 28099 28098 0 -1 0 15218 0 0 0 27954 49 0 0 25 0 1 0 480579141 62705664 14803 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15309 14803 603 41 0 15268 0
vsize: 61236
[startup+290.004 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 32539
Raw data (stat): 32539 (minisat+) R 32538 28099 28098 0 -1 0 15469 0 0 0 28954 50 0 0 25 0 1 0 480579141 63197184 14948 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15429 14948 603 41 0 15388 0
vsize: 61716
[startup+300.004 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 32539
Raw data (stat): 32539 (minisat+) R 32538 28099 28098 0 -1 0 15469 0 0 0 29954 50 0 0 25 0 1 0 480579141 63197184 14948 4294967295 134512640 134672761 3221224576 3221223760 134615720 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15429 14948 603 41 0 15388 0
vsize: 61716
[startup+310.004 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 32539
Raw data (stat): 32539 (minisat+) R 32538 28099 28098 0 -1 0 15469 0 0 0 30954 50 0 0 25 0 1 0 480579141 63197184 14948 4294967295 134512640 134672761 3221224576 3221223616 134612975 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15429 14948 603 41 0 15388 0
vsize: 61716
[startup+320.003 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 32539
Raw data (stat): 32539 (minisat+) R 32538 28099 28098 0 -1 0 15469 0 0 0 31954 50 0 0 25 0 1 0 480579141 63197184 14948 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15429 14948 603 41 0 15388 0
vsize: 61716
[startup+330.004 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 32539
Raw data (stat): 32539 (minisat+) R 32538 28099 28098 0 -1 0 15469 0 0 0 32954 50 0 0 25 0 1 0 480579141 63197184 14948 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15429 14948 603 41 0 15388 0
vsize: 61716
[startup+340.003 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 32539
Raw data (stat): 32539 (minisat+) R 32538 28099 28098 0 -1 0 15469 0 0 0 33954 50 0 0 25 0 1 0 480579141 63197184 14948 4294967295 134512640 134672761 3221224576 3221223760 134615752 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15429 14948 603 41 0 15388 0
vsize: 61716
[startup+350.004 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 32539
Raw data (stat): 32539 (minisat+) R 32538 28099 28098 0 -1 0 15469 0 0 0 34954 50 0 0 25 0 1 0 480579141 63197184 14948 4294967295 134512640 134672761 3221224576 3221223760 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15429 14948 603 41 0 15388 0
vsize: 61716
[startup+360.004 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 32539
Raw data (stat): 32539 (minisat+) R 32538 28099 28098 0 -1 0 15469 0 0 0 35955 50 0 0 25 0 1 0 480579141 63197184 14948 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15429 14948 603 41 0 15388 0
vsize: 61716
[startup+370.004 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 32539
Raw data (stat): 32539 (minisat+) R 32538 28099 28098 0 -1 0 15469 0 0 0 36955 50 0 0 25 0 1 0 480579141 63197184 14948 4294967295 134512640 134672761 3221224576 3221223760 134615919 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15429 14948 603 41 0 15388 0
vsize: 61716
[startup+380.005 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 32539
Raw data (stat): 32539 (minisat+) R 32538 28099 28098 0 -1 0 15469 0 0 0 37955 50 0 0 25 0 1 0 480579141 63197184 14948 4294967295 134512640 134672761 3221224576 3221223760 134615693 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15429 14948 603 41 0 15388 0
vsize: 61716
[startup+390.005 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 32539
Raw data (stat): 32539 (minisat+) R 32538 28099 28098 0 -1 0 15469 0 0 0 38955 50 0 0 25 0 1 0 480579141 63197184 14948 4294967295 134512640 134672761 3221224576 3221223760 134615828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15429 14948 603 41 0 15388 0
vsize: 61716
[startup+400.006 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 32539
Raw data (stat): 32539 (minisat+) R 32538 28099 28098 0 -1 0 15469 0 0 0 39956 50 0 0 25 0 1 0 480579141 63197184 14948 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15429 14948 603 41 0 15388 0
vsize: 61716
[startup+410.006 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 32539
Raw data (stat): 32539 (minisat+) R 32538 28099 28098 0 -1 0 15469 0 0 0 40956 50 0 0 25 0 1 0 480579141 63197184 14948 4294967295 134512640 134672761 3221224576 3221223760 134615916 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15429 14948 603 41 0 15388 0
vsize: 61716
[startup+420.005 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 32539
Raw data (stat): 32539 (minisat+) R 32538 28099 28098 0 -1 0 15469 0 0 0 41956 50 0 0 25 0 1 0 480579141 63197184 14948 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15429 14948 603 41 0 15388 0
vsize: 61716
[startup+430.006 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 32539
Raw data (stat): 32539 (minisat+) R 32538 28099 28098 0 -1 0 15469 0 0 0 42956 50 0 0 25 0 1 0 480579141 63197184 14948 4294967295 134512640 134672761 3221224576 3221223760 134615752 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15429 14948 603 41 0 15388 0
vsize: 61716
[startup+440.006 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 32539
Raw data (stat): 32539 (minisat+) R 32538 28099 28098 0 -1 0 15469 0 0 0 43956 50 0 0 25 0 1 0 480579141 63197184 14948 4294967295 134512640 134672761 3221224576 3221223760 134615747 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15429 14948 603 41 0 15388 0
vsize: 61716
[startup+450.006 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 32539
Raw data (stat): 32539 (minisat+) R 32538 28099 28098 0 -1 0 15565 0 0 0 44956 50 0 0 25 0 1 0 480579141 63594496 15044 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15526 15044 603 41 0 15485 0
vsize: 62104
[startup+460.007 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 32539
Raw data (stat): 32539 (minisat+) R 32538 28099 28098 0 -1 0 15880 0 0 0 45955 52 0 0 25 0 1 0 480579141 64970752 15359 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15862 15359 603 41 0 15821 0
vsize: 63448
[startup+470.007 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 32539
Raw data (stat): 32539 (minisat+) R 32538 28099 28098 0 -1 0 16147 0 0 0 46954 53 0 0 25 0 1 0 480579141 66031616 15626 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16121 15626 603 41 0 16080 0
vsize: 64484
[startup+480.007 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 32539
Raw data (stat): 32539 (minisat+) R 32538 28099 28098 0 -1 0 16414 0 0 0 47953 54 0 0 25 0 1 0 480579141 67239936 15893 4294967295 134512640 134672761 3221224576 3221223760 134615608 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16416 15893 603 41 0 16375 0
vsize: 65664
[startup+490.007 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 32539
Raw data (stat): 32539 (minisat+) R 32538 28099 28098 0 -1 0 16670 0 0 0 48952 56 0 0 25 0 1 0 480579141 68300800 16149 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16675 16149 603 41 0 16634 0
vsize: 66700
[startup+500.007 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 32539
Raw data (stat): 32539 (minisat+) R 32538 28099 28098 0 -1 0 16897 0 0 0 49951 57 0 0 25 0 1 0 480579141 69242880 16376 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16905 16376 603 41 0 16864 0
vsize: 67620
[startup+510.007 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 32539
Raw data (stat): 32539 (minisat+) R 32538 28099 28098 0 -1 0 17141 0 0 0 50951 57 0 0 25 0 1 0 480579141 70176768 16620 4294967295 134512640 134672761 3221224576 3221223760 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17133 16620 603 41 0 17092 0
vsize: 68532
[startup+520.006 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 32539
Raw data (stat): 32539 (minisat+) R 32538 28099 28098 0 -1 0 17363 0 0 0 51950 58 0 0 25 0 1 0 480579141 71102464 16842 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17359 16842 603 41 0 17318 0
vsize: 69436
[startup+530.007 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 32539
Raw data (stat): 32539 (minisat+) R 32538 28099 28098 0 -1 0 17570 0 0 0 52950 59 0 0 25 0 1 0 480579141 72040448 17049 4294967295 134512640 134672761 3221224576 3221223760 134615681 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17588 17049 603 41 0 17547 0
vsize: 70352
[startup+540.007 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 32539
Raw data (stat): 32539 (minisat+) R 32538 28099 28098 0 -1 0 17766 0 0 0 53949 59 0 0 25 0 1 0 480579141 72826880 17245 4294967295 134512640 134672761 3221224576 3221223616 134614402 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17780 17245 603 41 0 17739 0
vsize: 71120
[startup+550.008 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 32539
Raw data (stat): 32539 (minisat+) R 32538 28099 28098 0 -1 0 18010 0 0 0 54948 60 0 0 25 0 1 0 480579141 73773056 17489 4294967295 134512640 134672761 3221224576 3221223712 134614727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18011 17489 603 41 0 17970 0
vsize: 72044
[startup+560.009 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 32539
Raw data (stat): 32539 (minisat+) R 32538 28099 28098 0 -1 0 18221 0 0 0 55948 61 0 0 25 0 1 0 480579141 74575872 17700 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18207 17700 603 41 0 18166 0
vsize: 72828
[startup+570.008 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 32539
Raw data (stat): 32539 (minisat+) R 32538 28099 28098 0 -1 0 18400 0 0 0 56947 62 0 0 25 0 1 0 480579141 74788864 17763 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18259 17763 603 41 0 18218 0
vsize: 73036
[startup+580.008 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 32539
Raw data (stat): 32539 (minisat+) R 32538 28099 28098 0 -1 0 18400 0 0 0 57947 62 0 0 25 0 1 0 480579141 74788864 17763 4294967295 134512640 134672761 3221224576 3221223760 134615581 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18259 17763 603 41 0 18218 0
vsize: 73036
[startup+590.008 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 32539
Raw data (stat): 32539 (minisat+) R 32538 28099 28098 0 -1 0 18400 0 0 0 58948 62 0 0 25 0 1 0 480579141 74788864 17763 4294967295 134512640 134672761 3221224576 3221223760 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18259 17763 603 41 0 18218 0
vsize: 73036
[startup+600.008 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 32539
Raw data (stat): 32539 (minisat+) R 32538 28099 28098 0 -1 0 18400 0 0 0 59948 62 0 0 25 0 1 0 480579141 74788864 17763 4294967295 134512640 134672761 3221224576 3221223616 134612878 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18259 17763 603 41 0 18218 0
vsize: 73036
[startup+610.008 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 32539
Raw data (stat): 32539 (minisat+) R 32538 28099 28098 0 -1 0 18400 0 0 0 60948 62 0 0 25 0 1 0 480579141 74788864 17763 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18259 17763 603 41 0 18218 0
vsize: 73036
[startup+620.007 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 32539
Raw data (stat): 32539 (minisat+) R 32538 28099 28098 0 -1 0 18400 0 0 0 61948 62 0 0 25 0 1 0 480579141 74788864 17763 4294967295 134512640 134672761 3221224576 3221223760 134615804 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18259 17763 603 41 0 18218 0
vsize: 73036
[startup+630.008 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 32539
Raw data (stat): 32539 (minisat+) R 32538 28099 28098 0 -1 0 18400 0 0 0 62948 62 0 0 25 0 1 0 480579141 74788864 17763 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18259 17763 603 41 0 18218 0
vsize: 73036
[startup+640.008 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 32539
Raw data (stat): 32539 (minisat+) R 32538 28099 28098 0 -1 0 18400 0 0 0 63948 62 0 0 25 0 1 0 480579141 74788864 17763 4294967295 134512640 134672761 3221224576 3221223760 134615736 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18259 17763 603 41 0 18218 0
vsize: 73036
[startup+650.009 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 32539
Raw data (stat): 32539 (minisat+) R 32538 28099 28098 0 -1 0 18400 0 0 0 64948 62 0 0 25 0 1 0 480579141 74788864 17763 4294967295 134512640 134672761 3221224576 3221223760 134615736 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18259 17763 603 41 0 18218 0
vsize: 73036
[startup+660.009 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 32539
Raw data (stat): 32539 (minisat+) R 32538 28099 28098 0 -1 0 18400 0 0 0 65948 62 0 0 25 0 1 0 480579141 74788864 17763 4294967295 134512640 134672761 3221224576 3221223760 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18259 17763 603 41 0 18218 0
vsize: 73036
[startup+670.008 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 32539
Raw data (stat): 32539 (minisat+) R 32538 28099 28098 0 -1 0 18400 0 0 0 66948 62 0 0 25 0 1 0 480579141 74788864 17763 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18259 17763 603 41 0 18218 0
vsize: 73036
[startup+680.009 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 32539
Raw data (stat): 32539 (minisat+) R 32538 28099 28098 0 -1 0 19247 0 0 0 67947 64 0 0 25 0 1 0 480579141 78348288 18610 4294967295 134512640 134672761 3221224576 3221223760 134615921 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19128 18610 603 41 0 19087 0
vsize: 76512
[startup+690.009 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 32539
Raw data (stat): 32539 (minisat+) R 32538 28099 28098 0 -1 0 20393 0 0 0 68944 67 0 0 25 0 1 0 480579141 82939904 19756 4294967295 134512640 134672761 3221224576 3221223408 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20249 19756 603 41 0 20208 0
vsize: 80996
[startup+700.009 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 32539
Raw data (stat): 32539 (minisat+) R 32538 28099 28098 0 -1 0 21483 0 0 0 69941 71 0 0 25 0 1 0 480579141 87420928 20846 4294967295 134512640 134672761 3221224576 3221223760 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21343 20846 603 41 0 21302 0
vsize: 85372
[startup+710.009 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 32539
Raw data (stat): 32539 (minisat+) R 32538 28099 28098 0 -1 0 22481 0 0 0 70938 74 0 0 25 0 1 0 480579141 91512832 21844 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22342 21844 603 41 0 22301 0
vsize: 89368
[startup+720.009 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 32539
Raw data (stat): 32539 (minisat+) R 32538 28099 28098 0 -1 0 23333 0 0 0 71936 76 0 0 25 0 1 0 480579141 94986240 22696 4294967295 134512640 134672761 3221224576 3221223760 134615741 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23190 22696 603 41 0 23149 0
vsize: 92760
[startup+730.009 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 32539
Raw data (stat): 32539 (minisat+) R 32538 28099 28098 0 -1 0 24244 0 0 0 72934 78 0 0 25 0 1 0 480579141 98811904 23607 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24124 23607 603 41 0 24083 0
vsize: 96496
[startup+740.009 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 32539
Raw data (stat): 32539 (minisat+) R 32538 28099 28098 0 -1 0 25182 0 0 0 73931 81 0 0 25 0 1 0 480579141 103051264 24545 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25159 24545 603 41 0 25118 0
vsize: 100636
[startup+750.008 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 32539
Raw data (stat): 32539 (minisat+) R 32538 28099 28098 0 -1 0 26083 0 0 0 74928 84 0 0 25 0 1 0 480579141 106758144 25446 4294967295 134512640 134672761 3221224576 3221223748 134615856 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26064 25446 603 41 0 26023 0
vsize: 104256
[startup+760.008 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 32539
Raw data (stat): 32539 (minisat+) R 32538 28099 28098 0 -1 0 26391 0 0 0 75927 85 0 0 25 0 1 0 480579141 107405312 25622 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26222 25622 603 41 0 26181 0
vsize: 104888
[startup+770.008 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 32539
Raw data (stat): 32539 (minisat+) R 32538 28099 28098 0 -1 0 26391 0 0 0 76928 85 0 0 25 0 1 0 480579141 107405312 25622 4294967295 134512640 134672761 3221224576 3221223760 134615665 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26222 25622 603 41 0 26181 0
vsize: 104888
[startup+780.008 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 32539
Raw data (stat): 32539 (minisat+) R 32538 28099 28098 0 -1 0 26391 0 0 0 77928 85 0 0 25 0 1 0 480579141 107405312 25622 4294967295 134512640 134672761 3221224576 3221223760 134615758 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26222 25622 603 41 0 26181 0
vsize: 104888
[startup+790.008 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 32539
Raw data (stat): 32539 (minisat+) R 32538 28099 28098 0 -1 0 26391 0 0 0 78928 85 0 0 25 0 1 0 480579141 107405312 25622 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26222 25622 603 41 0 26181 0
vsize: 104888
[startup+800.007 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 32539
Raw data (stat): 32539 (minisat+) R 32538 28099 28098 0 -1 0 26391 0 0 0 79928 85 0 0 25 0 1 0 480579141 107405312 25622 4294967295 134512640 134672761 3221224576 3221223616 134612771 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26222 25622 603 41 0 26181 0
vsize: 104888
[startup+810.008 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 32539
Raw data (stat): 32539 (minisat+) R 32538 28099 28098 0 -1 0 26391 0 0 0 80928 85 0 0 25 0 1 0 480579141 107405312 25622 4294967295 134512640 134672761 3221224576 3221223760 134615749 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26222 25622 603 41 0 26181 0
vsize: 104888
[startup+820.007 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 32539
Raw data (stat): 32539 (minisat+) R 32538 28099 28098 0 -1 0 26391 0 0 0 81928 85 0 0 25 0 1 0 480579141 107405312 25622 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26222 25622 603 41 0 26181 0
vsize: 104888
[startup+830.008 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 32539
Raw data (stat): 32539 (minisat+) R 32538 28099 28098 0 -1 0 26391 0 0 0 82928 85 0 0 25 0 1 0 480579141 107405312 25622 4294967295 134512640 134672761 3221224576 3221223760 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26222 25622 603 41 0 26181 0
vsize: 104888
[startup+840.008 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 32539
Raw data (stat): 32539 (minisat+) R 32538 28099 28098 0 -1 0 26391 0 0 0 83928 86 0 0 25 0 1 0 480579141 107405312 25622 4294967295 134512640 134672761 3221224576 3221223760 134615788 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26222 25622 603 41 0 26181 0
vsize: 104888
[startup+850.008 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 32539
Raw data (stat): 32539 (minisat+) R 32538 28099 28098 0 -1 0 26391 0 0 0 84928 86 0 0 25 0 1 0 480579141 107405312 25622 4294967295 134512640 134672761 3221224576 3221223760 134615828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26222 25622 603 41 0 26181 0
vsize: 104888
[startup+860.008 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 32539
Raw data (stat): 32539 (minisat+) R 32538 28099 28098 0 -1 0 26391 0 0 0 85929 86 0 0 25 0 1 0 480579141 107405312 25622 4294967295 134512640 134672761 3221224576 3221223760 134615807 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26222 25622 603 41 0 26181 0
vsize: 104888
[startup+870.007 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 32539
Raw data (stat): 32539 (minisat+) R 32538 28099 28098 0 -1 0 26391 0 0 0 86929 86 0 0 25 0 1 0 480579141 107405312 25622 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26222 25622 603 41 0 26181 0
vsize: 104888
[startup+880.007 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 32539
Raw data (stat): 32539 (minisat+) R 32538 28099 28098 0 -1 0 26391 0 0 0 87929 86 0 0 25 0 1 0 480579141 107405312 25622 4294967295 134512640 134672761 3221224576 3221223700 134566071 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26222 25622 603 41 0 26181 0
vsize: 104888
[startup+890.007 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 32539
Raw data (stat): 32539 (minisat+) R 32538 28099 28098 0 -1 0 26392 0 0 0 88929 86 0 0 25 0 1 0 480579141 107405312 25623 4294967295 134512640 134672761 3221224576 3221223580 134619829 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26222 25623 603 41 0 26181 0
vsize: 104888
[startup+900.007 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 32539
Raw data (stat): 32539 (minisat+) R 32538 28099 28098 0 -1 0 26392 0 0 0 89929 86 0 0 25 0 1 0 480579141 107405312 25623 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26222 25623 603 41 0 26181 0
vsize: 104888
[startup+910.007 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 32539
Raw data (stat): 32539 (minisat+) R 32538 28099 28098 0 -1 0 26392 0 0 0 90929 86 0 0 25 0 1 0 480579141 107405312 25623 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26222 25623 603 41 0 26181 0
vsize: 104888
[startup+920.006 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 32539
Raw data (stat): 32539 (minisat+) R 32538 28099 28098 0 -1 0 26669 0 0 0 91929 87 0 0 25 0 1 0 480579141 108589056 25900 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26511 25900 603 41 0 26470 0
vsize: 106044
[startup+930.007 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 32539
Raw data (stat): 32539 (minisat+) R 32538 28099 28098 0 -1 0 27234 0 0 0 92926 89 0 0 25 0 1 0 480579141 110977024 26465 4294967295 134512640 134672761 3221224576 3221223760 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27094 26465 603 41 0 27053 0
vsize: 108376
[startup+940.007 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 32539
Raw data (stat): 32539 (minisat+) R 32538 28099 28098 0 -1 0 27695 0 0 0 93925 90 0 0 25 0 1 0 480579141 112824320 26926 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27545 26926 603 41 0 27504 0
vsize: 110180
[startup+950.007 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 32539
Raw data (stat): 32539 (minisat+) R 32538 28099 28098 0 -1 0 28239 0 0 0 94924 92 0 0 25 0 1 0 480579141 115097600 27470 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28100 27470 603 41 0 28059 0
vsize: 112400
[startup+960.007 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 32539
Raw data (stat): 32539 (minisat+) R 32538 28099 28098 0 -1 0 28757 0 0 0 95922 93 0 0 25 0 1 0 480579141 117211136 27988 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28616 27988 603 41 0 28575 0
vsize: 114464
[startup+970.006 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 32539
Raw data (stat): 32539 (minisat+) R 32538 28099 28098 0 -1 0 29277 0 0 0 96921 95 0 0 25 0 1 0 480579141 119328768 28508 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29133 28508 603 41 0 29092 0
vsize: 116532
[startup+980.007 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 32539
Raw data (stat): 32539 (minisat+) R 32538 28099 28098 0 -1 0 29777 0 0 0 97920 97 0 0 25 0 1 0 480579141 121438208 29008 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29648 29008 603 41 0 29607 0
vsize: 118592
[startup+990.006 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 32539
Raw data (stat): 32539 (minisat+) R 32538 28099 28098 0 -1 0 30255 0 0 0 98918 98 0 0 25 0 1 0 480579141 123420672 29486 4294967295 134512640 134672761 3221224576 3221223760 134615681 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30132 29486 603 41 0 30091 0
vsize: 120528
[startup+1000.01 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 32539
Raw data (stat): 32539 (minisat+) R 32538 28099 28098 0 -1 0 30729 0 0 0 99917 100 0 0 25 0 1 0 480579141 125317120 29960 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30595 29960 603 41 0 30554 0
vsize: 122380
[startup+1010.01 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 32539
Raw data (stat): 32539 (minisat+) R 32538 28099 28098 0 -1 0 31177 0 0 0 100916 101 0 0 25 0 1 0 480579141 127160320 30408 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31045 30408 603 41 0 31004 0
vsize: 124180
[startup+1020.01 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 32539
Raw data (stat): 32539 (minisat+) R 32538 28099 28098 0 -1 0 31617 0 0 0 101915 102 0 0 25 0 1 0 480579141 129015808 30848 4294967295 134512640 134672761 3221224576 3221223760 134615693 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31498 30848 603 41 0 31457 0
vsize: 125992
[startup+1030.01 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 32539
Raw data (stat): 32539 (minisat+) R 32538 28099 28098 0 -1 0 32041 0 0 0 102914 103 0 0 25 0 1 0 480579141 130736128 31272 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31918 31272 603 41 0 31877 0
vsize: 127672
[startup+1040.01 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 32539
Raw data (stat): 32539 (minisat+) R 32538 28099 28098 0 -1 0 32422 0 0 0 103913 104 0 0 25 0 1 0 480579141 132337664 31653 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32309 31653 603 41 0 32268 0
vsize: 129236
[startup+1050.01 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 32539
Raw data (stat): 32539 (minisat+) R 32538 28099 28098 0 -1 0 32829 0 0 0 104912 105 0 0 25 0 1 0 480579141 134111232 32060 4294967295 134512640 134672761 3221224576 3221223760 134615830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32742 32060 603 41 0 32701 0
vsize: 130968
[startup+1060.01 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 32539
Raw data (stat): 32539 (minisat+) R 32538 28099 28098 0 -1 0 33175 0 0 0 105911 107 0 0 25 0 1 0 480579141 135450624 32406 4294967295 134512640 134672761 3221224576 3221223760 134616005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33069 32406 603 41 0 33028 0
vsize: 132276
[startup+1070.01 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 32539
Raw data (stat): 32539 (minisat+) R 32538 28099 28098 0 -1 0 33546 0 0 0 106910 108 0 0 25 0 1 0 480579141 137039872 32777 4294967295 134512640 134672761 3221224576 3221223760 134615708 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33457 32777 603 41 0 33416 0
vsize: 133828
[startup+1080.01 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 32539
Raw data (stat): 32539 (minisat+) R 32538 28099 28098 0 -1 0 33856 0 0 0 107908 110 0 0 25 0 1 0 480579141 138227712 33087 4294967295 134512640 134672761 3221224576 3221223760 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33747 33087 603 41 0 33706 0
vsize: 134988
[startup+1090.01 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 32539
Raw data (stat): 32539 (minisat+) R 32538 28099 28098 0 -1 0 34177 0 0 0 108908 110 0 0 25 0 1 0 480579141 139542528 33408 4294967295 134512640 134672761 3221224576 3221223760 134615940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34068 33408 603 41 0 34027 0
vsize: 136272
[startup+1100.01 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 32539
Raw data (stat): 32539 (minisat+) R 32538 28099 28098 0 -1 0 34516 0 0 0 109907 111 0 0 25 0 1 0 480579141 141000704 33747 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34424 33747 603 41 0 34383 0
vsize: 137696
[startup+1110.01 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 32539
Raw data (stat): 32539 (minisat+) R 32538 28099 28098 0 -1 0 34827 0 0 0 110906 113 0 0 25 0 1 0 480579141 142315520 34058 4294967295 134512640 134672761 3221224576 3221223760 134615526 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34745 34058 603 41 0 34704 0
vsize: 138980
[startup+1120.01 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 32539
Raw data (stat): 32539 (minisat+) R 32538 28099 28098 0 -1 0 35167 0 0 0 111905 114 0 0 25 0 1 0 480579141 143638528 34398 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35068 34398 603 41 0 35027 0
vsize: 140272
[startup+1130.01 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 32539
Raw data (stat): 32539 (minisat+) R 32538 28099 28098 0 -1 0 35490 0 0 0 112904 115 0 0 25 0 1 0 480579141 144953344 34721 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35389 34721 603 41 0 35348 0
vsize: 141556
[startup+1140.01 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 32539
Raw data (stat): 32539 (minisat+) R 32538 28099 28098 0 -1 0 35796 0 0 0 113904 115 0 0 25 0 1 0 480579141 146305024 35027 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35719 35027 603 41 0 35678 0
vsize: 142876
[startup+1150.01 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 32539
Raw data (stat): 32539 (minisat+) R 32538 28099 28098 0 -1 0 36041 0 0 0 114902 117 0 0 25 0 1 0 480579141 147230720 35272 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35945 35272 603 41 0 35904 0
vsize: 143780
[startup+1160.01 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 32539
Raw data (stat): 32539 (minisat+) R 32538 28099 28098 0 -1 0 36390 0 0 0 115901 118 0 0 25 0 1 0 480579141 148692992 35621 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36302 35621 603 41 0 36261 0
vsize: 145208
[startup+1170.01 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 32539
Raw data (stat): 32539 (minisat+) R 32538 28099 28098 0 -1 0 36687 0 0 0 116900 119 0 0 25 0 1 0 480579141 149983232 35918 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36617 35918 603 41 0 36576 0
vsize: 146468
[startup+1180.01 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 32539
Raw data (stat): 32539 (minisat+) R 32538 28099 28098 0 -1 0 36984 0 0 0 117899 121 0 0 25 0 1 0 480579141 151171072 36215 4294967295 134512640 134672761 3221224576 3221223760 134615708 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36907 36215 603 41 0 36866 0
vsize: 147628
[startup+1190.01 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 32539
Raw data (stat): 32539 (minisat+) R 32538 28099 28098 0 -1 0 37290 0 0 0 118898 122 0 0 25 0 1 0 480579141 152358912 36521 4294967295 134512640 134672761 3221224576 3221223760 134615608 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37197 36521 603 41 0 37156 0
vsize: 148788
[startup+1200.01 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 32539
Raw data (stat): 32539 (minisat+) R 32538 28099 28098 0 -1 0 37593 0 0 0 119898 122 0 0 25 0 1 0 480579141 153702400 36824 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37525 36824 603 41 0 37484 0
vsize: 150100
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.08 s]
Raw data (loadavg): 0.99 1.00 0.92 1/54 32539
Raw data (stat): 32539 (minisat+) Z 32538 28099 28098 0 -1 12 37593 0 0 0 119898 129 0 0 25 0 1 0 480579141 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 0
Real time (s): 1200.08
CPU time (s): 1200.28
CPU user time (s): 1198.98
CPU system time (s): 1.2978
CPU usage (%): 100.017
Max. virtual memory (Kb): 150100
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####