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 6033

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc28 THE 2005-04-14 03:11:50 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=4493 boxname=wulflinc28 idbench=357 idsolver=12 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  77c89bda49ebcdc0428e1292512864a9  /oldhome/oroussel/tmp/wulflinc28/normalized-ws97-3.opb
REAL COMMAND:  minisat+ -cb -gs /oldhome/oroussel/tmp/wulflinc28/normalized-ws97-3.opb /oldhome/oroussel/tmp/wulflinc28/normalized-ws97-3.opb
IDLAUNCH: 4493
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.077
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.077
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:        884328 kB
Buffers:         35812 kB
Cached:          77744 kB
SwapCached:          4 kB
Active:          53828 kB
Inactive:        63480 kB
HighTotal:      131008 kB
HighFree:        48776 kB
LowTotal:       903652 kB
LowFree:        835552 kB
SwapTotal:     2097640 kB
SwapFree:      2097636 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6920 kB
Slab:            27536 kB
Committed_AS:    63472 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-14 03:31:53 (client local time) WITH STATUS 10 IN 1200.24 SECONDS
stats: 4493 7 1200.24 10
#### 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   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
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   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
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   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
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   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
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 
c *** TERMINATED ***
s SATISFIABLE
v v861 -v1081 -v1741 -v2994 v2 -v432 v862 -v1082 -v1302 v2842 -v2995 -v3148 v3 v863 -v1083 -v4 v219 v864 -v1084 -v1524 -v2996 v3149 v5 v865 -v1085 -v1745 -v2997 v6 -v221 -v651 -v866 -v1086 v1526 -v1746 -v1966 v2998 -v3151 -v7 v222 -v652 -v867 -v1087 -v1527 -v1747 v1967 v2999 -v3152 -v8 v223 -v868 -v1088 -v1528 v2188 -v2408 -v2628 -v3000 v3153 v869 -v1529 v2848 -v3001 -v3154 v224 -v439 -v654 -v1310 -v1530 -v1750 -v1970 v225 -v440 -v871 -v1091 -v1311 -v1531 -v1751 v2849 -v3002 v226 -v441 -v1312 -v1532 v1752 v2850 -v442 v657 -v1313 -v1973 v2851 -v13 v228 -v874 -v1094 v1754 v3005 v229 -v659 -v1535 v1975 -v2635 v446 -v877 -v1097 -v1317 v1757 -v2854 v3007 v1758 -v17 v232 -v662 -v879 v1099 -v1539 -v1759 -v1979 -v3008 v3161 v233 -v663 -v880 -v1100 -v1540 -v1760 v1980 v3009 v19 -v881 -v1101 v2201 v3010 -v3163 v665 v882 -v1102 -v1982 v21 -v451 v883 -v1103 -v1323 v2858 -v3011 -v3164 v237 -v1544 v2424 v23 -v2205 -v24 v239 -v454 v886 -v1106 -v1326 -v1546 v2860 -v3013 -v3166 v455 -v1327 v1767 -v456 v1328 -v1768 -v27 v242 v889 -v1109 -v1549 -v3014 v3167 v28 -v243 -v890 -v1110 v1550 v3015 -v3168 -v244 -v891 -v1111 v1551 -v2431 v3016 -v30 v245 -v460 -v892 v1112 -v1332 -v1552 v2864 -v3017 -v3170 v462 -v1334 v1774 v248 v895 -v1115 -v1555 -v34 v249 -v464 -v896 -v1116 -v1336 -v1556 v2865 -v3018 -v3171 v35 v897 -v1117 -v36 v251 -v466 -v898 -v1118 v1338 -v1778 -v2866 -v3019 v3172 v682 v1779 -v1999 v38 -v900 -v1120 v2440 v3020 -v3173 v39 -v901 -v1121 v2221 -v2441 -v2661 v3021 -v3174 -v40 v255 -v1562 -v41 v256 -v1563 v2663 -v3175 v42 -v904 -v1124 v2444 v3023 -v3176 -v43 v258 -v1565 v259 v906 -v1126 -v1566 -v45 v260 v907 -v1127 -v1567 -v3024 v3177 v46 -v908 v1128 v47 v909 -v1129 -v48 v693 v910 -v1130 -v2010 -v49 v264 -v694 -v911 -v1131 -v1571 -v1791 v2011 v3025 -v3178 -v50 v265 -v695 -v912 v1132 -v1572 -v1792 -v2012 -v3026 v3179 v266 -v913 -v1133 -v1573 v1793 -v52 v267 -v697 -v914 -v1134 -v1574 -v1794 v2014 v698 v1795 -v2015 v54 -v699 -v916 -v1136 -v1796 v2016 v3027 -v3180 -v485 v700 -v1357 -v2017 -v2457 v2677 v2875 -v486 v701 -v918 -v1138 -v1358 v1798 -v2018 v2876 -v3029 v272 -v1579 v2459 v703 -v920 -v1140 -v2020 v2680 v3030 v704 v1801 -v2021 v490 -v922 -v1142 -v1362 v1802 -v2878 v3031 v276 -v491 -v1363 -v1583 -v1803 -v2879 v277 -v492 -v707 -v924 v1144 -v1364 -v1584 -v1804 -v2024 -v2880 -v3033 v278 -v925 -v1145 -v1585 v1805 v3034 v64 -v926 v1146 v495 -v927 -v1147 -v1367 v1807 -v2882 v3035 -v928 -v1148 v2028 -v3036 v3189 v281 -v711 -v929 -v1149 -v1589 v2029 -v3037 v282 -v930 -v1150 -v1590 -v1810 -v3038 v713 v931 -v1151 -v1811 -v2031 -v2471 -v2691 -v3039 -v69 -v932 -v1152 -v2692 -v3040 -v3193 -v500 -v933 -v1153 -v1373 -v1813 -v2473 -v2693 -v2888 -v3041 -v71 -v286 -v1154 -v1374 -v1594 -v1814 v2889 -v3042 -v3195 -v72 -v935 v1155 -v2695 -v3043 v3196 v73 -v503 -v936 v1156 -v1376 v2891 -v3044 -v3197 v719 -v937 -v1157 v1817 -v2037 v3045 v720 -v938 -v1158 -v2038 -v2258 -v2478 -v2698 v3046 v291 -v939 -v1159 -v1599 -v1819 v2259 -v2479 -v2699 v3047 -v77 -v292 -v507 -v940 -v1160 -v1380 -v1600 -v2895 -v3048 v3201 -v508 -v941 -v1161 -v1381 -v2261 v2896 -v3049 -v79 -v509 -v724 -v942 -v1162 -v1382 -v2042 v2703 v3203 -v510 v725 -v944 -v1164 -v1384 -v2044 v2898 -v3051 -v81 v296 -v945 -v1165 -v1605 v2705 v82 -v946 -v1166 v1386 v3052 -v3205 v83 v2707 v299 -v948 -v1168 -v1608 v2268 -v2488 v3053 -v300 -v515 -v1389 v1609 -v1829 v2901 v301 -v516 -v950 -v1170 v1390 -v1610 v87 -v732 -v951 -v1171 v2051 v3055 -v3208 -v88 v303 -v518 -v952 -v1172 v1392 -v1612 -v2712 v89 -v519 v1393 v520 v954 -v1174 -v1394 v306 -v521 -v1395 -v1615 -v1835 v2903 -v92 v307 -v1176 v1396 -v1616 -v1836 -v2904 -v3057 v3210 -v93 -v308 v523 -v957 -v1617 v2057 v2905 -v3058 v94 -v958 -v1178 v2498 v3059 -v3212 v95 -v310 -v740 -v959 -v1179 -v1619 -v1839 v2059 v3060 -v3213 -v741 -v960 -v1180 v2060 v3061 v97 -v312 -v527 -v961 -v1181 -v1401 v1621 v2909 -v3062 -v3215 -v98 v528 -v743 -v962 -v1182 -v1402 v2062 -v314 v529 -v963 -v1183 -v1403 v1623 -v1843 -v2910 v3063 v100 -v315 -v530 -v964 -v1404 v1624 v2911 -v3064 -v3217 -v316 v531 -v965 -v1185 -v1405 v1625 -v2912 -v3065 v3218 -v532 v747 -v1406 -v2066 v2913 -v318 -v967 -v1187 -v1627 -v1847 -v3067 -v319 -v534 v749 -v1408 v1628 -v1848 -v2068 v2915 v535 -v750 -v1409 -v1849 -v2069 v2729 v106 -v751 -v970 -v1190 -v1850 v2070 v322 -v537 -v1411 -v1631 -v1851 v2731 v2916 v108 -v972 -v1192 v2292 -v2512 -v2732 v109 -v324 -v539 -v973 -v1193 -v1413 v1633 -v1853 v2917 -v3070 -v3223 v325 v974 -v1194 -v1634 v756 -v975 -v1195 v1855 -v2075 v3071 -v327 v542 -v976 -v1196 -v1416 v1636 -v2919 v3072 v758 -v977 -v1197 -v2077 -v114 v329 -v544 -v978 -v1198 v1418 -v1638 -v2920 -v3073 v3226 -v115 v330 -v979 -v1199 v1419 -v1639 -v2921 -v3074 v3227 -v116 -v331 -v546 -v980 v1200 -v1420 -v1640 v2922 -v3075 -v3228 -v117 v547 -v762 -v981 v1201 -v1421 -v2081 -v2923 -v3076 v3229 v333 -v1642 v119 -v549 -v764 -v983 v1203 -v1423 -v2083 v2924 -v3077 -v3230 -v120 v550 -v765 -v984 -v1204 -v1424 -v2084 -v2925 -v3078 v3231 v121 -v336 -v551 -v766 -v985 -v1205 -v1425 v1645 -v1865 -v2085 v2926 -v3079 -v3232 v122 -v552 -v767 -v986 -v1206 -v1426 -v2086 v2927 -v3080 -v3233 -v768 -v987 v1207 -v1867 -v2087 -v3081 v124 -v988 v1208 -v3082 -v3235 -v340 v770 -v989 v1209 -v1649 -v1869 -v2089 -v3083 v126 -v990 -v1210 -v1870 -v2090 -v2530 v2750 v3084 -v3237 v557 -v991 -v1211 -v1431 v2311 -v2932 -v3085 v128 -v343 -v3239 -v129 v344 -v993 v1213 -v1653 -v3087 v3240 v130 -v345 -v560 -v1434 -v1874 v2935 -v3241 -v995 -v1215 -v1875 v2755 v3089 -v347 v562 -v777 -v1436 -v1656 -v1876 v2096 -v348 v563 -v778 -v1437 v1657 -v1877 -v2097 v998 -v1218 -v1878 -v2758 -v3090 -v135 -v780 -v999 v1219 -v2099 -v2938 -v3091 v3244 v136 -v566 -v1000 -v1220 v1440 -v2939 v3092 -v3245 -v782 -v1001 -v1221 -v1881 v2101 v3093 v783 -v1002 -v1222 -v1882 -v2102 v2762 -v354 -v784 -v1663 -v1883 v2103 -v355 v570 -v785 -v1444 -v1664 -v1884 v2104 v356 -v571 -v786 v1445 -v1665 -v1885 -v2105 v142 -v357 -v787 -v1006 -v1226 -v1666 -v1886 v2106 v3094 -v3247 -v143 -v358 v788 -v1007 v1227 -v1667 -v1887 -v2107 -v3095 v3248 -v359 -v1008 -v1228 v1668 v145 -v575 -v1009 v1229 -v1449 v2943 -v3096 -v3249 v146 -v361 -v576 -v1010 -v1230 -v1450 -v1670 v2944 -v3097 -v3250 -v362 v792 -v1011 -v1231 -v1671 -v1891 -v2111 v3098 -v148 v2772 v3252 -v2553 v2773 -v149 v364 -v794 -v1014 -v1234 -v1674 -v1894 v2114 -v3100 v3253 v795 -v2115 -v2556 v2776 -v1017 v1237 -v151 v366 -v581 v797 -v2118 v2558 -v368 -v1019 -v1239 -v1679 v154 v2340 v370 -v1021 v1241 -v1681 -v156 v586 -v1022 v1242 -v1462 -v2950 -v3103 v3256 v372 -v587 -v802 -v1463 -v1683 -v1903 v2123 v2951 v373 -v588 -v803 -v1024 -v1244 v1464 -v1684 -v1904 -v2124 -v2952 v3105 -v159 v374 -v589 -v1025 -v1245 -v1465 -v1685 v2785 -v160 -v590 v805 -v1026 -v1246 v1466 -v2126 -v2953 v3106 -v3259 v161 -v1027 -v1247 v1907 v3107 -v3260 -v162 v592 -v1028 v1248 -v1468 -v2955 -v3108 v3261 -v163 -v378 v808 -v1029 v1249 -v1689 -v1909 -v2129 -v3109 v3262 -v164 -v1030 v1250 -v1910 -v3110 v3263 v810 -v1031 -v1251 -v2131 v2571 v3111 v1912 -v166 -v596 -v1033 -v1253 -v1473 -v2959 -v3112 v3265 -v167 -v382 v812 -v1034 -v1254 -v1694 -v1914 -v2134 -v3113 v3266 v813 v1915 -v2135 -v169 v599 -v1036 v1256 -v1476 -v2961 -v3114 v3267 v170 v2797 -v171 -v1038 -v1258 v2798 -v3115 v3268 -v172 -v387 -v1039 v1259 -v1919 -v3116 -v173 -v388 -v603 -v1040 -v1260 -v1480 v1700 -v2964 -v3117 v3270 -v174 -v389 -v1041 -v1261 -v1481 v1701 v390 -v1702 v1922 -v176 -v391 -v1703 v3271 v392 -v1704 v1924 v1925 -v178 -v393 -v608 -v1046 -v1266 v1486 -v1706 -v1926 -v2966 -v3119 v3272 v179 -v1047 -v1267 v2807 v3120 -v3273 -v180 -v395 v610 -v825 -v1488 v1708 -v2148 -v2968 v3274 -v396 v611 -v1049 -v1269 -v1489 v1709 -v2969 v3122 -v2370 v2810 -v398 v1051 -v1271 -v1711 -v184 -v399 v829 v1712 -v1932 -v2152 -v615 v830 -v1493 -v2153 -v2593 v2813 v2970 -v186 -v616 v1494 -v2594 -v2971 v3277 -v403 -v1056 -v1276 -v1716 -v1936 v3125 v189 v2377 -v405 v620 -v835 -v1058 -v1278 -v1498 -v1718 v2158 -v2973 v3126 -v621 -v1059 -v1279 v1499 -v1939 -v2974 v3127 v837 v3128 v408 -v1060 -v1280 -v1720 -v2600 v2820 v3129 v839 -v1061 -v1281 -v1941 -v2161 -v2601 v2821 v3130 v195 v1062 -v1282 v1503 -v2163 -v196 -v1944 -v197 v627 -v842 -v1065 -v1285 -v1505 -v2165 -v2978 -v3131 v3284 -v413 -v1066 -v1286 -v1726 -v1946 v2606 v3132 -v414 -v629 v2980 -v200 -v415 v630 -v1067 -v1287 -v1507 v1727 -v2981 -v3134 v3287 -v201 v631 -v1068 -v1288 -v1508 -v2982 -v3135 v3288 v202 -v1069 -v1289 v2829 v3136 -v3289 -v203 v633 -v848 v1070 -v1290 -v1510 -v2170 -v2984 -v3137 v3290 v419 -v1071 -v1291 -v1731 v1951 v3138 -v420 -v1732 v851 -v1073 -v1293 -v1953 -v2173 -v1074 -v1294 -v3139 -v422 -v1075 -v1295 -v1955 v2615 -v2835 v3140 -v423 -v1076 -v1296 -v2616 v2836 v3141 v1517 -v2177 -v424 -v1078 -v1298 -v1738 -v1958 -v3142 v211 -v426 v3143 -v3296 v427 v213 -v428 -v643 -v1079 -v1299 v1519 -v1739 -v2991 v3144 -v3297 v214 -v429 -v644 -v1080 -v1300 v1520 -v1740 -v2992 v3145 -v3298 -v645 v860 v2993 -v216 -v1521 -v2181 -v2401 -v2621 -v217 -v647 -v1522 -v1742 -v1962 -v2182 -v2402 -v2622 -v2183 -v2403 -v2623 -v434 -v649 -v1304 -v1744 -v1964 -v2184 -v2404 -v2624 -v2843 -v220 -v650 -v1525 -v1965 -v2185 -v2405 -v2625 -v2186 -v2406 -v2626 -v2187 -v2407 -v2627 -v438 -v653 -v1308 -v1748 -v1968 -v2847 -v2189 -v2409 -v2629 -v2190 -v2410 -v2630 -v11 -v872 -v1092 -v2192 -v2412 -v2632 -v3003 -v3156 -v12 -v227 -v873 -v1093 v1533 -v1753 -v2193 -v2413 -v2633 -v3004 -v3157 -v658 -v1974 -v2194 -v2414 -v2634 -v444 -v875 -v1095 -v1315 -v1755 -v2195 -v2415 -v15 -v2196 -v2416 -v2636 -v3159 -v16 -v231 -v661 -v1537 -v1977 -v2197 -v3160 -v878 -v1098 -v1318 -v1538 -v1978 -v2198 -v2418 -v2638 -v447 -v1319 -v2199 -v2419 -v2639 -v2855 -v18 -v448 -v1320 -v2200 -v2420 -v2640 -v2856 -v3162 -v234 -v449 -v664 -v1321 -v1541 -v1761 -v1981 -v2421 -v2641 -v2857 -v20 -v235 -v450 -v1322 -v1542 -v1762 -v2202 -v2422 -v2642 -v236 -v666 -v1543 -v1763 -v1983 -v2203 -v2423 -v2643 -v22 -v452 -v1324 -v2204 -v2859 -v3165 -v238 -v668 -v885 -v1105 -v1545 -v1765 -v1985 -v2425 -v2645 -v669 -v1766 -v1986 -v2206 -v2426 -v2646 -v25 -v2207 -v2427 -v26 -v2208 -v2428 -v457 -v672 -v1329 -v1769 -v1989 -v2209 -v2429 -v2649 -v2861 -v458 -v673 -v1330 -v1770 -v1990 -v2210 -v2430 -v2650 -v2862 -v459 -v674 -v1331 -v1991 -v2863 -v675 -v1772 -v1992 -v2212 -v2432 -v2652 -v32 -v247 -v677 -v894 -v1114 -v1554 -v1994 -v2214 -v2434 -v2654 -v33 -v463 -v678 -v1335 -v1775 -v1995 -v2215 -v2435 -v2655 -v2216 -v2436 -v2656 -v250 -v465 -v680 -v1337 -v1557 -v1777 -v1997 -v2217 -v2437 -v2657 -v681 -v1998 -v2218 -v2438 -v2658 -v37 -v252 -v467 -v899 -v1119 -v1339 -v1559 -v2219 -v2439 -v2659 -v253 -v468 -v683 -v1340 -v1560 -v1780 -v2000 -v2220 -v2660 -v2867 -v254 -v469 -v684 -v1341 -v1561 -v1781 -v2001 -v2868 -v470 -v685 v902 -v1122 -v1342 -v1782 -v2002 -v2222 -v2442 -v2662 -v257 -v472 -v687 -v1344 -v1564 -v1784 -v2004 -v2224 -v2664 -v2870 -v473 -v688 v905 -v1125 -v1345 -v1785 -v2005 -v2225 -v2445 -v2665 -v44 -v474 -v689 -v1346 -v1786 -v2006 -v2226 -v2446 -v2666 -v475 -v690 -v1347 -v1787 -v2007 -v2227 -v2447 -v2667 -v2871 -v261 -v476 -v691 -v1348 -v1568 -v1788 -v2008 -v2228 -v2448 -v2668 -v262 -v477 -v692 -v1349 -v1569 -v1789 -v2009 -v2229 -v2449 -v2669 -v263 -v478 -v1350 -v1570 -v1790 -v479 -v1351 -v2231 -v2451 -v2671 -v2872 -v480 -v1352 -v2232 -v2452 -v2672 -v2873 -v51 -v481 -v696 -v1353 -v2013 -v2233 -v2453 -v2673 -v482 -v1354 -v2234 -v2454 -v2674 -v53 -v268 -v483 -v915 -v1135 -v1355 -v1575 -v2235 -v2455 -v2675 -v269 -v484 -v1356 -v1576 -v2236 -v2456 -v2676 -v2874 -v55 -v270 -v917 -v1137 -v1577 -v1797 -v2237 -v3028 -v3181 -v56 -v271 -v1578 -v2238 -v2458 -v2678 -v3182 -v57 -v487 -v702 -v919 -v1139 -v1359 -v1799 -v2019 -v2239 -v2679 -v58 -v273 -v488 -v1360 -v1580 -v1800 -v2240 -v2460 -v2877 -v3183 -v59 -v274 -v489 -v921 -v1141 -v1361 -v1581 -v2241 -v2461 -v2681 -v60 -v275 -v705 -v1582 -v2022 -v2242 -v2462 -v2682 -v3184 -v2243 -v2463 -v2683 -v2244 -v2464 -v2684 -v63 -v493 -v708 -v1365 -v2025 -v2245 -v2465 -v2685 -v2881 -v3187 -v279 -v494 -v709 -v1366 -v1586 -v1806 -v2026 -v2246 -v2466 -v2686 -v65 -v280 -v710 -v1587 -v2027 -v2247 -v2467 -v2687 -v3188 -v1368 -v1588 -v1808 -v2248 -v2468 -v2688 -v2883 -v496 -v1369 -v1809 -v2249 -v2469 -v2689 -v2884 -v497 -v1370 -v2250 -v2470 -v2690 -v2885 -v68 -v498 -v1371 -v2251 v2886 -v3192 -v284 -v499 v714 -v1372 -v1592 -v1812 -v2032 -v2252 v2472 v2887 -v70 -v285 v715 -v1593 -v2033 v2253 v3194 -v287 v502 -v717 -v1375 -v1595 -v1815 -v2035 -v2255 -v2475 -v2890 -v288 -v718 -v1596 -v1816 -v2036 -v2256 -v2476 -v2696 -v74 -v289 -v504 -v1377 -v1597 -v2257 -v2477 -v2697 -v2892 -v3198 -v75 -v290 -v505 -v1378 -v1598 -v2893 -v3199 -v76 -v506 -v721 -v1379 -v2039 -v2894 -v3200 -v78 -v293 v723 -v1601 v1821 -v2041 -v2481 -v2701 -v3202 v294 -v1602 v1822 -v2262 -v2482 -v2702 -v943 -v1163 -v1383 -v1603 -v1823 -v2043 -v2263 -v2483 -v2897 -v3050 -v80 -v295 v1604 -v1824 -v2264 -v2484 -v2704 -v3204 -v511 -v726 -v1385 -v1825 -v2045 -v2265 -v2485 -v297 -v1606 -v1826 -v2266 -v2486 -v2706 -v298 -v513 -v728 -v947 -v1167 -v1387 -v1607 -v1827 -v2047 -v2267 -v84 -v514 -v729 -v1388 -v1828 -v2048 -v2708 -v2900 -v3206 -v2269 -v2489 -v2709 -v86 -v731 -v1830 -v2050 -v2270 -v2490 -v2710 -v302 -v517 -v1391 -v1611 -v1831 -v2271 -v2491 -v2711 -v2902 -v733 -v1832 -v2052 -v2272 -v2492 -v304 -v734 -v953 -v1173 -v1613 -v1833 -v2053 -v2273 -v2493 -v2713 -v90 -v305 -v735 -v1614 -v1834 -v2054 -v2274 -v2494 -v2714 -v2275 -v2495 -v2715 -v738 -v1837 -v2277 -v2497 -v2717 -v3211 -v524 -v1398 -v2278 -v2906 -v525 -v1399 -v2279 -v2499 -v2719 -v2907 -v96 -v311 -v1620 -v2280 -v2500 -v2720 -v3214 -v2281 -v2501 -v2721 -v313 -v1622 -v1842 -v2282 -v2502 -v2722 -v99 -v744 -v2063 -v2283 -v2503 -v2723 -v3216 -v2284 -v2504 -v2724 -v746 -v1845 -v2065 -v2285 -v2505 -v2725 -v102 -v317 -v966 -v1186 -v1626 -v1846 -v2286 v2506 -v2726 -v3066 -v3219 -v104 -v968 -v1188 -v2288 -v2508 -v2728 -v3068 -v3221 -v321 -v536 -v1410 -v1630 -v2290 -v2510 -v2730 -v107 -v752 -v971 -v1191 -v2071 -v2291 -v2511 -v3069 -v3222 -v323 -v538 -v753 -v1412 -v1632 -v1852 -v2072 -v754 -v2073 -v2293 -v2513 -v2733 -v110 -v540 -v755 -v1414 -v1854 -v2074 -v2294 -v2514 -v2734 -v111 -v326 -v541 -v1415 -v1635 -v2295 -v2515 -v2735 -v2918 -v3224 -v112 -v757 -v2076 -v2296 -v2516 -v2736 -v3225 -v113 -v328 -v1637 -v2297 -v2517 -v2298 -v2518 -v2738 -v2299 -v2519 -v2739 -v2300 -v2520 -v2740 -v332 -v1641 -v2301 -v118 -v548 -v763 -v982 -v1202 -v1422 -v1862 -v2082 -v2522 -v2742 -v334 -v1643 -v1863 -v2303 -v2523 -v2743 -v335 -v1644 -v2305 -v2525 -v2745 -v337 -v1646 -v1866 -v2306 -v338 -v1647 -v2307 -v2527 -v2747 -v769 -v1868 -v2088 -v2308 -v2528 -v2748 -v555 -v1429 -v2309 -v2529 -v2749 -v2930 -v556 -v1430 -v2310 -v2931 -v342 -v772 -v1651 -v1871 -v2091 -v2531 -v2751 -v2312 -v2313 -v2533 -v2753 -v2314 -v131 -v561 -v1435 -v2936 -v3242 -v132 -v996 -v1216 -v2316 -v2536 -v2756 -v133 -v997 -v1217 -v2317 -v2537 -v2757 -v564 -v1438 -v2937 -v350 -v1659 -v1879 -v2319 -v2539 -v2759 -v351 -v781 -v1660 -v1880 -v2100 -v2320 -v2540 -v2760 -v352 -v567 -v1441 -v1661 -v2321 -v2541 -v2761 -v2940 -v138 -v353 -v568 -v1442 -v1662 -v2322 -v2542 -v139 -v1003 -v1223 -v2323 -v2543 -v2763 -v140 -v1004 -v1224 -v2324 -v2544 -v2764 -v2325 -v2545 -v2765 -v572 -v1446 -v2326 -v2546 -v2766 -v2941 -v573 -v1447 -v2327 -v2547 -v2767 -v2942 -v574 -v789 -v1448 -v1888 -v2108 -v2328 -v2548 -v2768 -v360 -v790 -v1669 -v1889 -v2109 -v2329 -v2549 -v2769 -v147 -v577 -v1451 -v2945 -v3251 -v579 -v1454 -v2334 -v2554 -v2774 -v2947 -v365 -v1675 -v1016 -v1236 -v1456 -v1676 -v1896 -v2116 -v2336 -v1457 -v1677 -v1897 -v2337 -v2557 -v2777 -v796 -v152 -v367 -v582 -v1018 -v1238 -v1458 -v1678 -v1898 -v2338 -v2778 -v2949 -v3102 v3255 -v798 -v2119 -v2339 -v2559 -v2779 -v369 -v584 -v799 -v1460 -v1680 -v1900 -v2120 -v2560 -v2780 -v155 -v585 -v800 -v1461 -v1901 -v2121 -v2341 -v2561 -v2781 -v371 -v801 -v1682 -v1902 -v2122 -v2342 -v2562 -v2782 -v157 -v1023 -v1243 -v2343 -v2563 -v2783 -v3104 -v3257 -v158 -v2344 -v2564 -v2784 -v3258 -v804 -v1905 -v2125 -v2345 -v2565 -v375 -v1686 -v1906 -v2346 -v2566 -v2786 -v376 -v591 -v806 -v1467 -v1687 -v2127 -v2347 -v2567 -v2787 -v2954 -v377 -v807 -v1688 -v1908 -v2128 -v2348 -v2568 -v2788 -v593 -v1469 -v2349 -v2569 -v2789 -v2956 -v594 -v1470 -v2350 -v2570 -v2790 -v2957 -v380 -v595 -v1471 -v1691 -v1911 -v2351 -v2791 -v2958 -v1032 -v1252 -v1472 -v1692 -v2132 -v2352 -v2572 -v2792 -v2353 -v2573 -v2793 -v597 -v1474 -v2354 -v2960 -v168 -v383 -v598 -v1035 -v1255 -v1475 -v1695 -v2355 -v2575 -v2795 -v384 -v814 -v1696 -v1916 -v2136 -v2356 -v2576 -v2796 -v385 -v600 -v815 -v1037 -v1257 -v1477 -v1697 -v1917 -v2137 -v2357 -v2577 -v817 -v2139 -v2359 -v2579 -v2799 -v2360 -v2580 -v2800 -v2361 -v2581 -v2801 -v175 -v605 -v820 -v1042 -v1262 -v1482 -v2142 -v2362 -v2582 -v2802 -v2363 -v2583 -v2803 -v177 -v607 -v822 -v1044 -v1264 -v1484 -v2144 -v2364 -v2584 -v2804 -v1045 -v1265 -v1485 -v1705 -v2145 -v2365 -v2585 -v2805 -v394 -v609 -v824 -v1487 -v1707 -v1927 -v2147 -v2367 -v2587 -v2967 -v1048 -v1268 -v1928 -v2368 -v2588 -v2808 -v3121 -v181 -v826 -v1929 -v2149 -v2369 -v2589 -v2809 -v3275 -v397 -v612 -v827 -v1050 -v1270 -v1490 -v1710 -v1930 -v2150 -v183 -v613 v828 -v1491 -v1931 -v2151 -v2371 -v2591 -v2811 -v2372 -v2592 -v2812 -v185 -v400 -v1053 -v1273 -v1713 -v3123 -v3276 -v618 -v833 -v1496 -v2156 -v2972 -v404 -v619 -v834 -v1057 -v1277 -v1497 -v1717 -v1937 -v2157 -v2597 -v2817 -v1938 -v2378 -v2598 -v2818 -v836 -v2159 -v2379 -v2599 -v2819 -v192 -v407 -v622 -v2975 -v3281 -v193 -v623 -v838 -v1500 -v1940 -v2160 -v2380 -v2976 -v3282 -v194 -v409 -v624 -v1501 -v1721 -v2381 -v2977 -v3283 -v410 -v625 -v840 -v1502 -v1722 -v1942 -v2162 -v2382 -v2602 -v2822 -v1063 -v1283 -v1723 -v1943 -v2383 -v2603 -v2823 -v412 -v1725 -v1945 -v2385 -v628 -v843 -v1506 -v2166 -v2386 -v2979 -v2387 -v2607 -v2827 -v416 -v1728 -v417 -v632 -v847 -v1509 -v1729 -v1949 -v2169 -v2389 -v2609 -v2983 -v418 -v1730 -v1950 -v2390 -v2610 -v2830 -v204 -v634 -v849 -v1511 -v2171 -v2391 -v2611 -v2831 -v2985 -v3291 v205 -v635 -v850 -v1072 -v1292 -v1512 -v1952 -v2172 -v2612 -v2832 -v636 -v1513 -v2393 -v2613 -v2833 -v207 -v637 -v1515 -v2987 -v3293 -v208 -v638 -v1516 -v2396 -v2988 -v3294 -v1077 -v1297 -v1737 -v1957 -v2397 -v2617 -v2837 -v641 -v856 -v2990 -v212 -v642 -v857 -v858 -v1959 -v2179 -v2399 -v2619 -v2839 -v859 -v1960 -v2180 -v2400 -v2620 -v2840 -v215 -v3146 -v3299 one -v1 -v9 -v10 -v14 v29 -v31 -v61 -v62 -v66 -v67 -v85 -v91 -v101 -v103 -v105 -v123 -v125 -v127 -v134 v137 -v141 v144 -v150 v153 -v165 v182 -v187 v188 -v190 v191 v198 -v199 -v206 -v209 -v210 -v218 -v230 -v240 -v241 -v246 -v283 -v309 -v320 -v339 -v341 -v346 -v349 -v363 -v379 -v381 -v386 -v401 -v402 -v406 -v411 -v421 -v425 -v430 v431 -v433 -v435 -v436 -v437 -v443 -v445 -v453 v461 -v471 -v501 -v512 -v522 v526 v533 -v543 -v545 v553 -v554 -v558 -v559 v565 v569 v578 -v580 -v583 v601 v602 v604 -v606 -v614 v617 -v626 -v639 v640 -v646 -v648 -v655 -v656 v660 -v667 -v670 v671 -v676 -v679 -v686 -v706 -v712 v716 v722 -v727 v730 -v736 -v737 -v739 -v742 -v745 -v748 -v759 -v760 v761 -v771 -v773 -v774 -v775 v776 v779 -v791 -v793 v809 v811 -v816 v818 -v819 v821 v823 v831 -v832 v841 v844 -v845 -v846 v852 v853 v854 -v855 v870 -v876 -v884 -v887 -v888 -v893 -v903 -v923 -v934 -v949 -v955 -v956 -v969 -v992 -v994 -v1005 -v1012 -v1013 -v1015 -v1020 -v1043 -v1052 -v1054 -v1055 -v1064 -v1089 -v1090 -v1096 -v1104 -v1107 -v1108 -v1113 -v1123 -v1143 -v1169 -v1175 -v1177 -v1184 -v1189 -v1212 -v1214 -v1225 -v1232 -v1233 -v1235 -v1240 -v1263 -v1272 -v1274 -v1275 -v1284 -v1301 -v1303 -v1305 -v1306 -v1307 -v1309 -v1314 -v1316 v1325 -v1333 -v1343 -v1397 -v1400 -v1407 -v1417 -v1427 -v1428 -v1432 -v1433 -v1439 -v1443 -v1452 -v1453 v1455 v1459 -v1478 -v1479 v1483 -v1492 -v1495 v1504 -v1514 v1518 -v1523 -v1534 v1536 -v1547 -v1548 -v1553 -v1558 -v1591 -v1618 -v1629 -v1648 -v1650 -v1652 -v1654 -v1655 -v1658 -v1672 -v1673 -v1690 v1693 -v1698 -v1699 -v1714 v1715 -v1719 -v1724 v1733 -v1734 -v1735 -v1736 -v1743 -v1749 -v1756 -v1764 -v1771 -v1773 -v1776 -v1783 v1818 -v1820 -v1838 -v1840 -v1841 -v1844 -v1856 -v1857 -v1858 -v1859 -v1860 -v1861 -v1864 -v1872 -v1873 -v1890 -v1892 -v1893 -v1895 -v1899 -v1913 -v1918 -v1920 -v1921 -v1923 -v1933 -v1934 -v1935 -v1947 -v1948 -v1954 -v1956 -v1961 -v1963 -v1969 -v1971 -v1972 -v1976 -v1984 -v1987 -v1988 -v1993 v1996 -v2003 v2023 v2030 -v2034 -v2040 -v2046 -v2049 v2055 -v2056 -v2058 -v2061 -v2064 -v2067 -v2078 -v2079 -v2080 -v2092 -v2093 -v2094 -v2095 -v2098 -v2110 -v2112 -v2113 -v2117 -v2130 -v2133 -v2138 -v2140 -v2141 -v2143 -v2146 -v2154 -v2155 -v2164 -v2167 -v2168 -v2174 -v2175 -v2176 -v2178 -v2191 -v2211 v2213 -v2223 -v2230 v2254 v2260 -v2276 v2287 -v2289 v2302 v2304 -v2315 -v2318 v2330 v2331 -#### 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.97 0.91 2/54 20622
Raw data (stat): 20622 (runsolver) R 20621 10614 10613 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 481257253 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 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.0015 s]
Raw data (loadavg): 0.87 0.97 0.91 2/54 20622
Raw data (stat): 20622 (minisat+) R 20621 10614 10613 0 -1 0 21840 0 0 0 944 53 0 0 25 0 1 0 481257253 94203904 21151 4294967295 134512640 134672761 3221224560 3221218156 1075346698 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22999 21151 603 41 0 22958 0
vsize: 91996
[startup+20.0015 s]
Raw data (loadavg): 0.89 0.97 0.91 2/54 20622
Raw data (stat): 20622 (minisat+) R 20621 10614 10613 0 -1 0 23411 0 0 0 1940 57 0 0 25 0 1 0 481257253 99340288 22722 4294967295 134512640 134672761 3221224560 3221223732 134556660 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24253 22722 603 41 0 24212 0
vsize: 97012
[startup+30.0013 s]
Raw data (loadavg): 0.91 0.97 0.91 2/54 20622
Raw data (stat): 20622 (minisat+) R 20621 10614 10613 0 -1 0 23411 0 0 0 2940 58 0 0 25 0 1 0 481257253 99340288 22722 4294967295 134512640 134672761 3221224560 3221223732 134556660 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24253 22722 603 41 0 24212 0
vsize: 97012
[startup+40.0013 s]
Raw data (loadavg): 0.92 0.97 0.91 2/54 20622
Raw data (stat): 20622 (minisat+) R 20621 10614 10613 0 -1 0 23411 0 0 0 3939 58 0 0 25 0 1 0 481257253 99340288 22722 4294967295 134512640 134672761 3221224560 3221223732 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24253 22722 603 41 0 24212 0
vsize: 97012
[startup+50.0016 s]
Raw data (loadavg): 0.93 0.97 0.91 2/54 20622
Raw data (stat): 20622 (minisat+) R 20621 10614 10613 0 -1 0 23414 0 0 0 4938 58 0 0 25 0 1 0 481257253 99340288 22725 4294967295 134512640 134672761 3221224560 3221223732 134556627 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24253 22725 603 41 0 24212 0
vsize: 97012
[startup+60.0022 s]
Raw data (loadavg): 0.94 0.97 0.91 2/54 20622
Raw data (stat): 20622 (minisat+) R 20621 10614 10613 0 -1 0 23416 0 0 0 5938 58 0 0 25 0 1 0 481257253 99340288 22727 4294967295 134512640 134672761 3221224560 3221223732 134556667 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24253 22727 603 41 0 24212 0
vsize: 97012
[startup+70.0022 s]
Raw data (loadavg): 0.95 0.97 0.91 2/54 20622
Raw data (stat): 20622 (minisat+) R 20621 10614 10613 0 -1 0 23416 0 0 0 6939 58 0 0 25 0 1 0 481257253 99340288 22727 4294967295 134512640 134672761 3221224560 3221223732 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24253 22727 603 41 0 24212 0
vsize: 97012
[startup+80.0016 s]
Raw data (loadavg): 0.96 0.97 0.91 2/54 20622
Raw data (stat): 20622 (minisat+) R 20621 10614 10613 0 -1 0 23416 0 0 0 7939 58 0 0 25 0 1 0 481257253 99340288 22727 4294967295 134512640 134672761 3221224560 3221223732 134556602 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24253 22727 603 41 0 24212 0
vsize: 97012
[startup+90.0013 s]
Raw data (loadavg): 0.96 0.97 0.91 2/54 20622
Raw data (stat): 20622 (minisat+) R 20621 10614 10613 0 -1 0 23416 0 0 0 8939 58 0 0 25 0 1 0 481257253 99340288 22727 4294967295 134512640 134672761 3221224560 3221223732 134556667 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24253 22727 603 41 0 24212 0
vsize: 97012
[startup+100.001 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 20622
Raw data (stat): 20622 (minisat+) R 20621 10614 10613 0 -1 0 23416 0 0 0 9939 58 0 0 25 0 1 0 481257253 99340288 22727 4294967295 134512640 134672761 3221224560 3221223732 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24253 22727 603 41 0 24212 0
vsize: 97012
[startup+110.002 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 20622
Raw data (stat): 20622 (minisat+) R 20621 10614 10613 0 -1 0 23416 0 0 0 10939 58 0 0 25 0 1 0 481257253 99340288 22727 4294967295 134512640 134672761 3221224560 3221223732 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24253 22727 603 41 0 24212 0
vsize: 97012
[startup+120.001 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 20622
Raw data (stat): 20622 (minisat+) R 20621 10614 10613 0 -1 0 23416 0 0 0 11939 58 0 0 25 0 1 0 481257253 99340288 22727 4294967295 134512640 134672761 3221224560 3221223732 134556653 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24253 22727 603 41 0 24212 0
vsize: 97012
[startup+130.001 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 20622
Raw data (stat): 20622 (minisat+) R 20621 10614 10613 0 -1 0 23418 0 0 0 12940 58 0 0 25 0 1 0 481257253 99340288 22729 4294967295 134512640 134672761 3221224560 3221223732 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24253 22729 603 41 0 24212 0
vsize: 97012
[startup+140.002 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 20622
Raw data (stat): 20622 (minisat+) R 20621 10614 10613 0 -1 0 23418 0 0 0 13939 58 0 0 25 0 1 0 481257253 99340288 22729 4294967295 134512640 134672761 3221224560 3221223732 134556653 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24253 22729 603 41 0 24212 0
vsize: 97012
[startup+150.001 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 20622
Raw data (stat): 20622 (minisat+) R 20621 10614 10613 0 -1 0 23418 0 0 0 14940 58 0 0 25 0 1 0 481257253 99340288 22729 4294967295 134512640 134672761 3221224560 3221223732 134556627 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24253 22729 603 41 0 24212 0
vsize: 97012
[startup+160.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20622
Raw data (stat): 20622 (minisat+) R 20621 10614 10613 0 -1 0 23418 0 0 0 15940 58 0 0 25 0 1 0 481257253 99340288 22729 4294967295 134512640 134672761 3221224560 3221223732 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24253 22729 603 41 0 24212 0
vsize: 97012
[startup+170.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20622
Raw data (stat): 20622 (minisat+) R 20621 10614 10613 0 -1 0 23419 0 0 0 16940 58 0 0 25 0 1 0 481257253 99340288 22730 4294967295 134512640 134672761 3221224560 3221223732 134556660 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24253 22730 603 41 0 24212 0
vsize: 97012
[startup+180.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20622
Raw data (stat): 20622 (minisat+) R 20621 10614 10613 0 -1 0 23419 0 0 0 17940 58 0 0 25 0 1 0 481257253 99340288 22730 4294967295 134512640 134672761 3221224560 3221223764 134561964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24253 22730 603 41 0 24212 0
vsize: 97012
[startup+190.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20622
Raw data (stat): 20622 (minisat+) R 20621 10614 10613 0 -1 0 23419 0 0 0 18940 58 0 0 25 0 1 0 481257253 99340288 22730 4294967295 134512640 134672761 3221224560 3221223732 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24253 22730 603 41 0 24212 0
vsize: 97012
[startup+200.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20622
Raw data (stat): 20622 (minisat+) R 20621 10614 10613 0 -1 0 23436 0 0 0 19940 58 0 0 25 0 1 0 481257253 99340288 22747 4294967295 134512640 134672761 3221224560 3221223764 134561964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24253 22747 603 41 0 24212 0
vsize: 97012
[startup+210 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20622
Raw data (stat): 20622 (minisat+) R 20621 10614 10613 0 -1 0 23440 0 0 0 20940 58 0 0 25 0 1 0 481257253 99340288 22751 4294967295 134512640 134672761 3221224560 3221223732 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24253 22751 603 41 0 24212 0
vsize: 97012
[startup+220.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20622
Raw data (stat): 20622 (minisat+) R 20621 10614 10613 0 -1 0 23440 0 0 0 21941 58 0 0 25 0 1 0 481257253 99340288 22751 4294967295 134512640 134672761 3221224560 3221223732 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24253 22751 603 41 0 24212 0
vsize: 97012
[startup+230 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20622
Raw data (stat): 20622 (minisat+) R 20621 10614 10613 0 -1 0 23440 0 0 0 22941 58 0 0 25 0 1 0 481257253 99340288 22751 4294967295 134512640 134672761 3221224560 3221223732 134556680 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24253 22751 603 41 0 24212 0
vsize: 97012
[startup+240 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20622
Raw data (stat): 20622 (minisat+) R 20621 10614 10613 0 -1 0 23440 0 0 0 23941 58 0 0 25 0 1 0 481257253 99340288 22751 4294967295 134512640 134672761 3221224560 3221223732 134556643 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24253 22751 603 41 0 24212 0
vsize: 97012
[startup+249.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20622
Raw data (stat): 20622 (minisat+) R 20621 10614 10613 0 -1 0 23442 0 0 0 24941 59 0 0 25 0 1 0 481257253 99479552 22753 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24287 22753 603 41 0 24246 0
vsize: 97148
[startup+260 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20622
Raw data (stat): 20622 (minisat+) R 20621 10614 10613 0 -1 0 23442 0 0 0 25941 59 0 0 25 0 1 0 481257253 99479552 22753 4294967295 134512640 134672761 3221224560 3221223732 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24287 22753 603 41 0 24246 0
vsize: 97148
[startup+270 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20622
Raw data (stat): 20622 (minisat+) R 20621 10614 10613 0 -1 0 23442 0 0 0 26941 59 0 0 25 0 1 0 481257253 99479552 22753 4294967295 134512640 134672761 3221224560 3221223732 134556639 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24287 22753 603 41 0 24246 0
vsize: 97148
[startup+280 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20622
Raw data (stat): 20622 (minisat+) R 20621 10614 10613 0 -1 0 23443 0 0 0 27941 59 0 0 25 0 1 0 481257253 99479552 22754 4294967295 134512640 134672761 3221224560 3221223732 134556639 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24287 22754 603 41 0 24246 0
vsize: 97148
[startup+290 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20622
Raw data (stat): 20622 (minisat+) R 20621 10614 10613 0 -1 0 23462 0 0 0 28942 59 0 0 25 0 1 0 481257253 99479552 22773 4294967295 134512640 134672761 3221224560 3221223728 134560885 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24287 22773 603 41 0 24246 0
vsize: 97148
[startup+300 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20622
Raw data (stat): 20622 (minisat+) R 20621 10614 10613 0 -1 0 23463 0 0 0 29942 59 0 0 25 0 1 0 481257253 99479552 22774 4294967295 134512640 134672761 3221224560 3221223732 134556643 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24287 22774 603 41 0 24246 0
vsize: 97148
[startup+310 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20622
Raw data (stat): 20622 (minisat+) R 20621 10614 10613 0 -1 0 23472 0 0 0 30942 59 0 0 25 0 1 0 481257253 99479552 22783 4294967295 134512640 134672761 3221224560 3221223732 134556651 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24287 22783 603 41 0 24246 0
vsize: 97148
[startup+320 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20622
Raw data (stat): 20622 (minisat+) R 20621 10614 10613 0 -1 0 23473 0 0 0 31942 59 0 0 25 0 1 0 481257253 99479552 22784 4294967295 134512640 134672761 3221224560 3221223764 134561964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24287 22784 603 41 0 24246 0
vsize: 97148
[startup+330 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20622
Raw data (stat): 20622 (minisat+) R 20621 10614 10613 0 -1 0 23474 0 0 0 32942 59 0 0 25 0 1 0 481257253 99479552 22785 4294967295 134512640 134672761 3221224560 3221223732 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24287 22785 603 41 0 24246 0
vsize: 97148
[startup+340 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20622
Raw data (stat): 20622 (minisat+) R 20621 10614 10613 0 -1 0 23475 0 0 0 33942 59 0 0 25 0 1 0 481257253 99479552 22786 4294967295 134512640 134672761 3221224560 3221223732 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24287 22786 603 41 0 24246 0
vsize: 97148
[startup+349.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20622
Raw data (stat): 20622 (minisat+) R 20621 10614 10613 0 -1 0 23476 0 0 0 34942 59 0 0 25 0 1 0 481257253 99479552 22787 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24287 22787 603 41 0 24246 0
vsize: 97148
[startup+360 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20622
Raw data (stat): 20622 (minisat+) R 20621 10614 10613 0 -1 0 23478 0 0 0 35943 59 0 0 25 0 1 0 481257253 99479552 22789 4294967295 134512640 134672761 3221224560 3221223764 134561964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24287 22789 603 41 0 24246 0
vsize: 97148
[startup+370 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20622
Raw data (stat): 20622 (minisat+) R 20621 10614 10613 0 -1 0 23482 0 0 0 36943 59 0 0 25 0 1 0 481257253 99479552 22793 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24287 22793 603 41 0 24246 0
vsize: 97148
[startup+379.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20622
Raw data (stat): 20622 (minisat+) R 20621 10614 10613 0 -1 0 23511 0 0 0 37943 59 0 0 25 0 1 0 481257253 99479552 22822 4294967295 134512640 134672761 3221224560 3221223732 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24287 22822 603 41 0 24246 0
vsize: 97148
[startup+390 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20622
Raw data (stat): 20622 (minisat+) R 20621 10614 10613 0 -1 0 23550 0 0 0 38943 59 0 0 25 0 1 0 481257253 99614720 22861 4294967295 134512640 134672761 3221224560 3221223664 134560402 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24320 22861 603 41 0 24279 0
vsize: 97280
[startup+400 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20622
Raw data (stat): 20622 (minisat+) R 20621 10614 10613 0 -1 0 23587 0 0 0 39943 59 0 0 25 0 1 0 481257253 99749888 22898 4294967295 134512640 134672761 3221224560 3221223664 134560506 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24353 22898 603 41 0 24312 0
vsize: 97412
[startup+410 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20622
Raw data (stat): 20622 (minisat+) R 20621 10614 10613 0 -1 0 23626 0 0 0 40943 59 0 0 25 0 1 0 481257253 99885056 22937 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24386 22937 603 41 0 24345 0
vsize: 97544
[startup+420 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20622
Raw data (stat): 20622 (minisat+) R 20621 10614 10613 0 -1 0 24085 0 0 0 41942 61 0 0 25 0 1 0 481257253 101797888 23396 4294967295 134512640 134672761 3221224560 3221223728 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24853 23396 603 41 0 24812 0
vsize: 99412
[startup+430 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20622
Raw data (stat): 20622 (minisat+) R 20621 10614 10613 0 -1 0 24427 0 0 0 42941 62 0 0 25 0 1 0 481257253 103288832 23738 4294967295 134512640 134672761 3221224560 3221223732 134556618 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25217 23738 603 41 0 25176 0
vsize: 100868
[startup+440 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20622
Raw data (stat): 20622 (minisat+) R 20621 10614 10613 0 -1 0 24458 0 0 0 43941 62 0 0 25 0 1 0 481257253 103288832 23769 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25217 23769 603 41 0 25176 0
vsize: 100868
[startup+450 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20622
Raw data (stat): 20622 (minisat+) R 20621 10614 10613 0 -1 0 24872 0 0 0 44940 63 0 0 25 0 1 0 481257253 105041920 24183 4294967295 134512640 134672761 3221224560 3221223664 134560504 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25645 24183 603 41 0 25604 0
vsize: 102580
[startup+460.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20622
Raw data (stat): 20622 (minisat+) R 20621 10614 10613 0 -1 0 25273 0 0 0 45940 63 0 0 25 0 1 0 481257253 106786816 24584 4294967295 134512640 134672761 3221224560 3221223664 134560396 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26071 24584 603 41 0 26030 0
vsize: 104284
[startup+470.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20622
Raw data (stat): 20622 (minisat+) R 20621 10614 10613 0 -1 0 25408 0 0 0 46940 64 0 0 25 0 1 0 481257253 107323392 24719 4294967295 134512640 134672761 3221224560 3221223732 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26202 24719 603 41 0 26161 0
vsize: 104808
[startup+480.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20622
Raw data (stat): 20622 (minisat+) R 20621 10614 10613 0 -1 0 25419 0 0 0 47940 64 0 0 25 0 1 0 481257253 107323392 24730 4294967295 134512640 134672761 3221224560 3221223732 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26202 24730 603 41 0 26161 0
vsize: 104808
[startup+490.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20622
Raw data (stat): 20622 (minisat+) R 20621 10614 10613 0 -1 0 25470 0 0 0 48940 64 0 0 25 0 1 0 481257253 107593728 24781 4294967295 134512640 134672761 3221224560 3221223664 134560226 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26268 24781 603 41 0 26227 0
vsize: 105072
[startup+500 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20622
Raw data (stat): 20622 (minisat+) R 20621 10614 10613 0 -1 0 25696 0 0 0 49939 65 0 0 25 0 1 0 481257253 108523520 25007 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26495 25007 603 41 0 26454 0
vsize: 105980
[startup+510 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20622
Raw data (stat): 20622 (minisat+) R 20621 10614 10613 0 -1 0 26027 0 0 0 50938 66 0 0 25 0 1 0 481257253 109858816 25338 4294967295 134512640 134672761 3221224560 3221223664 134559847 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26821 25338 603 41 0 26780 0
vsize: 107284
[startup+520 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20622
Raw data (stat): 20622 (minisat+) R 20621 10614 10613 0 -1 0 26160 0 0 0 51938 66 0 0 25 0 1 0 481257253 110391296 25471 4294967295 134512640 134672761 3221224560 3221223664 134560289 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26951 25471 603 41 0 26910 0
vsize: 107804
[startup+530 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20622
Raw data (stat): 20622 (minisat+) R 20621 10614 10613 0 -1 0 26230 0 0 0 52938 66 0 0 25 0 1 0 481257253 110661632 25541 4294967295 134512640 134672761 3221224560 3221223664 134560158 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27017 25541 603 41 0 26976 0
vsize: 108068
[startup+540 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20622
Raw data (stat): 20622 (minisat+) R 20621 10614 10613 0 -1 0 26267 0 0 0 53939 66 0 0 25 0 1 0 481257253 110796800 25578 4294967295 134512640 134672761 3221224560 3221223760 134557828 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27050 25578 603 41 0 27009 0
vsize: 108200
[startup+550 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20622
Raw data (stat): 20622 (minisat+) R 20621 10614 10613 0 -1 0 26620 0 0 0 54937 67 0 0 25 0 1 0 481257253 112250880 25931 4294967295 134512640 134672761 3221224560 3221223664 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27405 25931 603 41 0 27364 0
vsize: 109620
[startup+560 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20622
Raw data (stat): 20622 (minisat+) R 20621 10614 10613 0 -1 0 27090 0 0 0 55937 68 0 0 25 0 1 0 481257253 114122752 26401 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27862 26401 603 41 0 27821 0
vsize: 111448
[startup+570 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20622
Raw data (stat): 20622 (minisat+) R 20621 10614 10613 0 -1 0 27198 0 0 0 56936 69 0 0 25 0 1 0 481257253 114528256 26509 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27961 26509 603 41 0 27920 0
vsize: 111844
[startup+580 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20622
Raw data (stat): 20622 (minisat+) R 20621 10614 10613 0 -1 0 27269 0 0 0 57936 69 0 0 25 0 1 0 481257253 114798592 26580 4294967295 134512640 134672761 3221224560 3221223664 134560260 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28027 26580 603 41 0 27986 0
vsize: 112108
[startup+590 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20622
Raw data (stat): 20622 (minisat+) R 20621 10614 10613 0 -1 0 27338 0 0 0 58936 70 0 0 25 0 1 0 481257253 115204096 26649 4294967295 134512640 134672761 3221224560 3221223664 134560246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28126 26649 603 41 0 28085 0
vsize: 112504
[startup+600 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20622
Raw data (stat): 20622 (minisat+) R 20621 10614 10613 0 -1 0 27413 0 0 0 59936 70 0 0 25 0 1 0 481257253 115470336 26724 4294967295 134512640 134672761 3221224560 3221223664 134560504 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28191 26724 603 41 0 28150 0
vsize: 112764
[startup+610 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20622
Raw data (stat): 20622 (minisat+) R 20621 10614 10613 0 -1 0 27467 0 0 0 60936 70 0 0 25 0 1 0 481257253 115605504 26778 4294967295 134512640 134672761 3221224560 3221223664 134560264 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28224 26778 603 41 0 28183 0
vsize: 112896
[startup+619.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20622
Raw data (stat): 20622 (minisat+) R 20621 10614 10613 0 -1 0 27565 0 0 0 61936 70 0 0 25 0 1 0 481257253 116019200 26876 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28325 26876 603 41 0 28284 0
vsize: 113300
[startup+629.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20622
Raw data (stat): 20622 (minisat+) R 20621 10614 10613 0 -1 0 27630 0 0 0 62936 70 0 0 25 0 1 0 481257253 116289536 26941 4294967295 134512640 134672761 3221224560 3221223664 134560289 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28391 26941 603 41 0 28350 0
vsize: 113564
[startup+640 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20622
Raw data (stat): 20622 (minisat+) R 20621 10614 10613 0 -1 0 27694 0 0 0 63936 70 0 0 25 0 1 0 481257253 116559872 27005 4294967295 134512640 134672761 3221224560 3221223664 134560246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28457 27005 603 41 0 28416 0
vsize: 113828
[startup+649.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20622
Raw data (stat): 20622 (minisat+) R 20621 10614 10613 0 -1 0 27762 0 0 0 64936 71 0 0 25 0 1 0 481257253 117092352 27073 4294967295 134512640 134672761 3221224560 3221223664 134560514 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28587 27073 603 41 0 28546 0
vsize: 114348
[startup+659.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20622
Raw data (stat): 20622 (minisat+) R 20621 10614 10613 0 -1 0 27819 0 0 0 65936 71 0 0 25 0 1 0 481257253 117358592 27130 4294967295 134512640 134672761 3221224560 3221223664 134560246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28652 27130 603 41 0 28611 0
vsize: 114608
[startup+669.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20622
Raw data (stat): 20622 (minisat+) R 20621 10614 10613 0 -1 0 27883 0 0 0 66936 71 0 0 25 0 1 0 481257253 117624832 27194 4294967295 134512640 134672761 3221224560 3221223728 134561118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28717 27194 603 41 0 28676 0
vsize: 114868
[startup+679.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20622
Raw data (stat): 20622 (minisat+) R 20621 10614 10613 0 -1 0 27979 0 0 0 67936 71 0 0 25 0 1 0 481257253 118030336 27290 4294967295 134512640 134672761 3221224560 3221223664 134560218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28816 27290 603 41 0 28775 0
vsize: 115264
[startup+689.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20622
Raw data (stat): 20622 (minisat+) R 20621 10614 10613 0 -1 0 28038 0 0 0 68936 71 0 0 25 0 1 0 481257253 118300672 27349 4294967295 134512640 134672761 3221224560 3221223732 134556602 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28882 27349 603 41 0 28841 0
vsize: 115528
[startup+699.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20622
Raw data (stat): 20622 (minisat+) R 20621 10614 10613 0 -1 0 28079 0 0 0 69936 71 0 0 25 0 1 0 481257253 118435840 27390 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28915 27390 603 41 0 28874 0
vsize: 115660
[startup+709.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20622
Raw data (stat): 20622 (minisat+) R 20621 10614 10613 0 -1 0 28212 0 0 0 70936 72 0 0 25 0 1 0 481257253 118976512 27523 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29047 27523 603 41 0 29006 0
vsize: 116188
[startup+719.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20622
Raw data (stat): 20622 (minisat+) R 20621 10614 10613 0 -1 0 28283 0 0 0 71936 72 0 0 25 0 1 0 481257253 119246848 27594 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29113 27594 603 41 0 29072 0
vsize: 116452
[startup+729.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20622
Raw data (stat): 20622 (minisat+) R 20621 10614 10613 0 -1 0 28366 0 0 0 72935 73 0 0 25 0 1 0 481257253 119517184 27677 4294967295 134512640 134672761 3221224560 3221223728 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29179 27677 603 41 0 29138 0
vsize: 116716
[startup+739.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20622
Raw data (stat): 20622 (minisat+) R 20621 10614 10613 0 -1 0 28410 0 0 0 73935 73 0 0 25 0 1 0 481257253 119783424 27721 4294967295 134512640 134672761 3221224560 3221223728 134561391 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29244 27721 603 41 0 29203 0
vsize: 116976
[startup+749.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20622
Raw data (stat): 20622 (minisat+) R 20621 10614 10613 0 -1 0 28444 0 0 0 74935 73 0 0 25 0 1 0 481257253 119918592 27755 4294967295 134512640 134672761 3221224560 3221223728 134561372 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29277 27755 603 41 0 29236 0
vsize: 117108
[startup+759.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20622
Raw data (stat): 20622 (minisat+) R 20621 10614 10613 0 -1 0 28878 0 0 0 75934 75 0 0 25 0 1 0 481257253 136237056 28138 4294967295 134512640 134672761 3221224560 3221223728 134561382 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33261 28138 603 41 0 33220 0
vsize: 133044
[startup+770 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20622
Raw data (stat): 20622 (minisat+) R 20621 10614 10613 0 -1 0 29006 0 0 0 76933 75 0 0 25 0 1 0 481257253 136777728 28266 4294967295 134512640 134672761 3221224560 3221223728 134560839 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33393 28266 603 41 0 33352 0
vsize: 133572
[startup+779.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20622
Raw data (stat): 20622 (minisat+) R 20621 10614 10613 0 -1 0 29451 0 0 0 77933 76 0 0 25 0 1 0 481257253 138670080 28711 4294967295 134512640 134672761 3221224560 3221223664 134560169 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33855 28711 603 41 0 33814 0
vsize: 135420
[startup+789.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20622
Raw data (stat): 20622 (minisat+) R 20621 10614 10613 0 -1 0 29722 0 0 0 78932 77 0 0 25 0 1 0 481257253 139440128 28932 4294967295 134512640 134672761 3221224560 3221223664 134559859 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34043 28932 603 41 0 34002 0
vsize: 136172
[startup+800 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20622
Raw data (stat): 20622 (minisat+) R 20621 10614 10613 0 -1 0 29908 0 0 0 79932 77 0 0 25 0 1 0 481257253 140247040 29118 4294967295 134512640 134672761 3221224560 3221223664 134560396 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34240 29118 603 41 0 34199 0
vsize: 136960
[startup+809.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20622
Raw data (stat): 20622 (minisat+) R 20621 10614 10613 0 -1 0 30017 0 0 0 80932 77 0 0 25 0 1 0 481257253 140652544 29227 4294967295 134512640 134672761 3221224560 3221223664 134560418 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34339 29227 603 41 0 34298 0
vsize: 137356
[startup+819.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20622
Raw data (stat): 20622 (minisat+) R 20621 10614 10613 0 -1 0 30182 0 0 0 81932 77 0 0 25 0 1 0 481257253 141049856 29341 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34436 29341 603 41 0 34395 0
vsize: 137744
[startup+829.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20622
Raw data (stat): 20622 (minisat+) R 20621 10614 10613 0 -1 0 30208 0 0 0 82932 77 0 0 25 0 1 0 481257253 141185024 29367 4294967295 134512640 134672761 3221224560 3221223696 134560654 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34469 29367 603 41 0 34428 0
vsize: 137876
[startup+839.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20622
Raw data (stat): 20622 (minisat+) R 20621 10614 10613 0 -1 0 30277 0 0 0 83932 77 0 0 25 0 1 0 481257253 141451264 29436 4294967295 134512640 134672761 3221224560 3221223760 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34534 29436 603 41 0 34493 0
vsize: 138136
[startup+849.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20622
Raw data (stat): 20622 (minisat+) R 20621 10614 10613 0 -1 0 30315 0 0 0 84932 78 0 0 25 0 1 0 481257253 141582336 29474 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34566 29474 603 41 0 34525 0
vsize: 138264
[startup+860 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20622
Raw data (stat): 20622 (minisat+) R 20621 10614 10613 0 -1 0 30371 0 0 0 85932 78 0 0 25 0 1 0 481257253 141852672 29530 4294967295 134512640 134672761 3221224560 3221223696 134560673 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34632 29530 603 41 0 34591 0
vsize: 138528
[startup+870 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20622
Raw data (stat): 20622 (minisat+) R 20621 10614 10613 0 -1 0 30439 0 0 0 86932 78 0 0 25 0 1 0 481257253 142118912 29598 4294967295 134512640 134672761 3221224560 3221223728 134560852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34697 29598 603 41 0 34656 0
vsize: 138788
[startup+880.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20622
Raw data (stat): 20622 (minisat+) R 20621 10614 10613 0 -1 0 30500 0 0 0 87932 79 0 0 25 0 1 0 481257253 142385152 29659 4294967295 134512640 134672761 3221224560 3221223728 134561261 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34762 29659 603 41 0 34721 0
vsize: 139048
[startup+890.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20622
Raw data (stat): 20622 (minisat+) R 20621 10614 10613 0 -1 0 30553 0 0 0 88932 79 0 0 25 0 1 0 481257253 142516224 29712 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34794 29712 603 41 0 34753 0
vsize: 139176
[startup+900 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20622
Raw data (stat): 20622 (minisat+) R 20621 10614 10613 0 -1 0 30602 0 0 0 89932 79 0 0 25 0 1 0 481257253 142778368 29761 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34858 29761 603 41 0 34817 0
vsize: 139432
[startup+910.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20622
Raw data (stat): 20622 (minisat+) R 20621 10614 10613 0 -1 0 30651 0 0 0 90932 79 0 0 25 0 1 0 481257253 142913536 29810 4294967295 134512640 134672761 3221224560 3221223728 134560871 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34891 29810 603 41 0 34850 0
vsize: 139564
[startup+920.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20622
Raw data (stat): 20622 (minisat+) R 20621 10614 10613 0 -1 0 30720 0 0 0 91932 80 0 0 25 0 1 0 481257253 143187968 29879 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34958 29879 603 41 0 34917 0
vsize: 139832
[startup+930 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20622
Raw data (stat): 20622 (minisat+) R 20621 10614 10613 0 -1 0 30771 0 0 0 92932 80 0 0 25 0 1 0 481257253 143458304 29930 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35024 29930 603 41 0 34983 0
vsize: 140096
[startup+940.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20622
Raw data (stat): 20622 (minisat+) R 20621 10614 10613 0 -1 0 30827 0 0 0 93932 80 0 0 25 0 1 0 481257253 143728640 29986 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35090 29986 603 41 0 35049 0
vsize: 140360
[startup+950.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20622
Raw data (stat): 20622 (minisat+) R 20621 10614 10613 0 -1 0 30881 0 0 0 94932 80 0 0 25 0 1 0 481257253 143859712 30040 4294967295 134512640 134672761 3221224560 3221223760 134557836 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35122 30040 603 41 0 35081 0
vsize: 140488
[startup+960.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20622
Raw data (stat): 20622 (minisat+) R 20621 10614 10613 0 -1 0 30943 0 0 0 95932 81 0 0 25 0 1 0 481257253 144138240 30102 4294967295 134512640 134672761 3221224560 3221223728 134561375 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35190 30102 603 41 0 35149 0
vsize: 140760
[startup+970.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20622
Raw data (stat): 20622 (minisat+) R 20621 10614 10613 0 -1 0 30994 0 0 0 96931 81 0 0 25 0 1 0 481257253 144404480 30153 4294967295 134512640 134672761 3221224560 3221223728 134560833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35255 30153 603 41 0 35214 0
vsize: 141020
[startup+980.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20622
Raw data (stat): 20622 (minisat+) R 20621 10614 10613 0 -1 0 31056 0 0 0 97931 81 0 0 25 0 1 0 481257253 144543744 30215 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35289 30215 603 41 0 35248 0
vsize: 141156
[startup+990 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20622
Raw data (stat): 20622 (minisat+) R 20621 10614 10613 0 -1 0 31110 0 0 0 98931 81 0 0 25 0 1 0 481257253 144814080 30269 4294967295 134512640 134672761 3221224560 3221223696 134560640 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35355 30269 603 41 0 35314 0
vsize: 141420
[startup+1000 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20622
Raw data (stat): 20622 (minisat+) R 20621 10614 10613 0 -1 0 31162 0 0 0 99931 81 0 0 25 0 1 0 481257253 145084416 30321 4294967295 134512640 134672761 3221224560 3221223664 134560008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35421 30321 603 41 0 35380 0
vsize: 141684
[startup+1010 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20622
Raw data (stat): 20622 (minisat+) R 20621 10614 10613 0 -1 0 31219 0 0 0 100931 82 0 0 25 0 1 0 481257253 145743872 30378 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35582 30378 603 41 0 35541 0
vsize: 142328
[startup+1020 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20622
Raw data (stat): 20622 (minisat+) R 20621 10614 10613 0 -1 0 31287 0 0 0 101932 82 0 0 25 0 1 0 481257253 146022400 30446 4294967295 134512640 134672761 3221224560 3221223728 134561234 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35650 30446 603 41 0 35609 0
vsize: 142600
[startup+1030 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20622
Raw data (stat): 20622 (minisat+) R 20621 10614 10613 0 -1 0 31338 0 0 0 102932 82 0 0 25 0 1 0 481257253 146288640 30497 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35715 30497 603 41 0 35674 0
vsize: 142860
[startup+1040 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20622
Raw data (stat): 20622 (minisat+) R 20621 10614 10613 0 -1 0 31388 0 0 0 103932 82 0 0 25 0 1 0 481257253 146554880 30547 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35780 30547 603 41 0 35739 0
vsize: 143120
[startup+1050 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20622
Raw data (stat): 20622 (minisat+) R 20621 10614 10613 0 -1 0 31449 0 0 0 104932 82 0 0 25 0 1 0 481257253 146710528 30608 4294967295 134512640 134672761 3221224560 3221223728 134561375 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35818 30608 603 41 0 35777 0
vsize: 143272
[startup+1060 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20622
Raw data (stat): 20622 (minisat+) R 20621 10614 10613 0 -1 0 31509 0 0 0 105932 82 0 0 25 0 1 0 481257253 146972672 30668 4294967295 134512640 134672761 3221224560 3221223760 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35882 30668 603 41 0 35841 0
vsize: 143528
[startup+1070 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20622
Raw data (stat): 20622 (minisat+) R 20621 10614 10613 0 -1 0 31563 0 0 0 106932 82 0 0 25 0 1 0 481257253 147238912 30722 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35947 30722 603 41 0 35906 0
vsize: 143788
[startup+1080 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20622
Raw data (stat): 20622 (minisat+) R 20621 10614 10613 0 -1 0 31610 0 0 0 107932 82 0 0 25 0 1 0 481257253 147369984 30769 4294967295 134512640 134672761 3221224560 3221223728 134560855 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35979 30769 603 41 0 35938 0
vsize: 143916
[startup+1090 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20622
Raw data (stat): 20622 (minisat+) R 20621 10614 10613 0 -1 0 31669 0 0 0 108932 83 0 0 25 0 1 0 481257253 147644416 30828 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36046 30828 603 41 0 36005 0
vsize: 144184
[startup+1100 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20622
Raw data (stat): 20622 (minisat+) R 20621 10614 10613 0 -1 0 31719 0 0 0 109932 83 0 0 25 0 1 0 481257253 147902464 30878 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36109 30878 603 41 0 36068 0
vsize: 144436
[startup+1110 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20622
Raw data (stat): 20622 (minisat+) R 20621 10614 10613 0 -1 0 31767 0 0 0 110932 83 0 0 25 0 1 0 481257253 148037632 30926 4294967295 134512640 134672761 3221224560 3221223760 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36142 30926 603 41 0 36101 0
vsize: 144568
[startup+1120 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20622
Raw data (stat): 20622 (minisat+) R 20621 10614 10613 0 -1 0 31804 0 0 0 111932 83 0 0 25 0 1 0 481257253 148168704 30963 4294967295 134512640 134672761 3221224560 3221223728 134560937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36174 30963 603 41 0 36133 0
vsize: 144696
[startup+1130 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20622
Raw data (stat): 20622 (minisat+) R 20621 10614 10613 0 -1 0 31886 0 0 0 112932 83 0 0 25 0 1 0 481257253 148582400 31045 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36275 31045 603 41 0 36234 0
vsize: 145100
[startup+1140 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20622
Raw data (stat): 20622 (minisat+) R 20621 10614 10613 0 -1 0 31934 0 0 0 113932 84 0 0 25 0 1 0 481257253 148713472 31093 4294967295 134512640 134672761 3221224560 3221223696 134560632 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36307 31093 603 41 0 36266 0
vsize: 145228
[startup+1150 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20622
Raw data (stat): 20622 (minisat+) R 20621 10614 10613 0 -1 0 31988 0 0 0 114932 84 0 0 25 0 1 0 481257253 148979712 31147 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36372 31147 603 41 0 36331 0
vsize: 145488
[startup+1160 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20622
Raw data (stat): 20622 (minisat+) R 20621 10614 10613 0 -1 0 32029 0 0 0 115932 84 0 0 25 0 1 0 481257253 149114880 31188 4294967295 134512640 134672761 3221224560 3221223760 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36405 31188 603 41 0 36364 0
vsize: 145620
[startup+1170 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20622
Raw data (stat): 20622 (minisat+) R 20621 10614 10613 0 -1 0 32100 0 0 0 116932 84 0 0 25 0 1 0 481257253 149409792 31259 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36477 31259 603 41 0 36436 0
vsize: 145908
[startup+1180 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20622
Raw data (stat): 20622 (minisat+) R 20621 10614 10613 0 -1 0 32155 0 0 0 117932 84 0 0 25 0 1 0 481257253 149676032 31314 4294967295 134512640 134672761 3221224560 3221223728 134561161 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36542 31315 603 41 0 36501 0
vsize: 146168
[startup+1190 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20622
Raw data (stat): 20622 (minisat+) R 20621 10614 10613 0 -1 0 32209 0 0 0 118932 85 0 0 25 0 1 0 481257253 149807104 31368 4294967295 134512640 134672761 3221224560 3221223744 134558662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36574 31368 603 41 0 36533 0
vsize: 146296
[startup+1200 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20622
Raw data (stat): 20622 (minisat+) R 20621 10614 10613 0 -1 0 32242 0 0 0 119931 85 0 0 25 0 1 0 481257253 149938176 31401 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36606 31401 603 41 0 36565 0
vsize: 146424
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.07 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 20622
Raw data (stat): 20622 (minisat+) Z 20621 10614 10613 0 -1 12 32245 0 0 0 119932 91 0 0 25 0 1 0 481257253 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.07
CPU time (s): 1200.24
CPU user time (s): 1199.32
CPU system time (s): 0.91986
CPU usage (%): 100.014
Max. virtual memory (Kb): 146424
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####