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/mps-v2-13-7/plato.asu.edu/pub/unibo/normalized-mps-v2-13-7-roll3000.opb
MD5SUM	a7433a26e92d47a3d337e0c2b98bd409
Bench Category	optimization, big integers (OPTBIGINT)
Has Objective Function	YES
Satisfiable	NO
(Un)Satisfiability was proved
Best value of the objective function
Optimality of the best value was proved
Number of terms in the objective function	21
Biggest coefficient in the objective function	1048576
Number of bits for the biggest coefficient in the objective function	21
Sum of the numbers in the objective function	2097151
Number of bits of the sum of numbers in the objective function	21
Biggest number in a constraint	128000000000
Number of bits of the biggest number in a constraint	37
Biggest sum of numbers in a constraint	265438953471
Number of bits of the biggest sum of numbers	38
Best result obtained on this benchmark	UNSAT
Best CPU time to get the best result obtained on this benchmark	2.57861
Number of variables	7611
Total number of constraints	3459
Number of constraints which are clauses	143
Number of constraints which are cardinality constraints (but not clauses)	626
Number of constraints which are nor clauses,nor cardinality constraints	2690
Minimum length of a constraint	1
Maximum length of a constraint	2047
Trace number 31340

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc9 THE 2005-05-26 00:20:39 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=22739 boxname=wulflinc9 idbench=1555 idsolver=15 numberseed=0
MD5SUM SOLVER: 34d34154b8ad81f02ee98439942e0814  /oldhome/oroussel/solvers/minisat+_script
MD5SUM BENCH:  a7433a26e92d47a3d337e0c2b98bd409  /oldhome/oroussel/tmp/wulflinc9/normalized-mps-v2-13-7-roll3000.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc9/normalized-mps-v2-13-7-roll3000.opb
IDLAUNCH: 22739
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.242
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 888.83

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.242
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:        506824 kB
Buffers:         38208 kB
Cached:         467876 kB
SwapCached:        584 kB
Active:          23392 kB
Inactive:       484736 kB
HighTotal:      131008 kB
HighFree:        21644 kB
LowTotal:       903652 kB
LowFree:        485180 kB
SwapTotal:     2097136 kB
SwapFree:      2095648 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5100 kB
Slab:            14032 kB
Committed_AS:    63596 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-05-26 00:41:09 (client local time) WITH STATUS 152 IN 1229.88 SECONDS
stats: 22739 7 1229.88 152
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 2918 PB-constraints to clauses...
c   -- Unit propagations: pppppppppppppppppppp
c   -- Detecting intervals from adjacent constraints: ==###########################################################################################################################################################################=###
c   -- Clauses(.)/Splits(s): ...............................................................................................................................................................................................................................................................................................................................................................................................ssssssss.ssssssssssssssssssss.ssssssssssssssssssss.sssssssssssssssssss.ssssssssssssssssss.sssss..............................................................ssssssssssssssssss.ssssssssssssssssssss.ssssssssssssssssss.ss...................................................................................................................................................ss.ss.sssss..sssssssss..sssssss..ssssss..ss.sssss...sssssss.ssssss.sss.sssssssss..ss.s.sss....sss.s.ssss...sss.sssss.s.s.ssss...ss.ss....ss.s..ss..ss...s.sss.ss...ssssss..s..sss..ss.ss..sss.s....sss.......s.ssss..ss.ss..ss.s...sssss..
c ---[2461]---> BDD-cost:   11
c ---[2460]---> BDD-cost:   11
c ---[2453]---> BDD-cost:   11
c ---[2452]---> BDD-cost:   11
c ---[2450]---> BDD-cost:   11
c ---[2449]---> BDD-cost:   11
c ---[2447]---> BDD-cost:   11
c ---[2446]---> BDD-cost:   11
c ---[2445]---> BDD-cost:   11
c ---[2443]---> BDD-cost:   11
c ---[2442]---> BDD-cost:   11
c ---[2440]---> BDD-cost:   11
c ---[2439]---> BDD-cost:   11
c ---[2438]---> BDD-cost:   11
c ---[2436]---> BDD-cost:   11
c ---[2435]---> BDD-cost:   11
c ---[2433]---> BDD-cost:   11
c ---[2432]---> BDD-cost:   11
c ---[2431]---> BDD-cost:   11
c ---[2429]---> BDD-cost:   11
c ---[2428]---> BDD-cost:   11
c ---[2427]---> BDD-cost:   11
c ---[2426]---> BDD-cost:   11
c ---[2425]---> BDD-cost:   11
c ---[2424]---> BDD-cost:   11
c ---[2422]---> BDD-cost:   11
c ---[2421]---> BDD-cost:   11
c ---[2420]---> BDD-cost:   11
c ---[2419]---> BDD-cost:   11
c ---[2418]---> BDD-cost:   11
c ---[2417]---> BDD-cost:   11
c ---[2415]---> BDD-cost:   11
c ---[2414]---> BDD-cost:   11
c ---[2413]---> BDD-cost:   11
c ---[2412]---> BDD-cost:   11
c ---[2411]---> BDD-cost:   11
c ---[2410]---> BDD-cost:   11
c ---[2407]---> BDD-cost:   11
c ---[2406]---> BDD-cost:   11
c ---[2405]---> BDD-cost:   11
c ---[2403]---> BDD-cost:   11
c ---[2402]---> BDD-cost:   11
c ---[2401]---> BDD-cost:   11
c ---[2400]---> BDD-cost:   11
c ---[2399]---> BDD-cost:   11
c ---[2397]---> BDD-cost:   11
c ---[2396]---> BDD-cost:   11
c ---[2395]---> BDD-cost:   11
c ---[2394]---> BDD-cost:   11
c ---[2393]---> BDD-cost:   11
c ---[2391]---> BDD-cost:   11
c ---[2390]---> BDD-cost:   11
c ---[2389]---> BDD-cost:   11
c ---[2388]---> BDD-cost:   11
c ---[2387]---> BDD-cost:   11
c ---[2385]---> BDD-cost:   11
c ---[2384]---> BDD-cost:   11
c ---[2383]---> BDD-cost:   11
c ---[2382]---> BDD-cost:   11
c ---[2380]---> BDD-cost:   11
c ---[2379]---> BDD-cost:   11
c ---[2378]---> BDD-cost:   11
c ---[2377]---> BDD-cost:   11
c ---[2376]---> BDD-cost:   11
c ---[2375]---> BDD-cost:   11
c ---[2374]---> BDD-cost:   11
c ---[2373]---> BDD-cost:   11
c ---[2372]---> BDD-cost:   11
c ---[2371]---> BDD-cost:   11
c ---[2370]---> BDD-cost:   11
c ---[2369]---> BDD-cost:   11
c ---[2368]---> BDD-cost:   11
c ---[2367]---> BDD-cost:   11
c ---[2366]---> BDD-cost:   11
c ---[2365]---> BDD-cost:   11
c ---[2364]---> BDD-cost:   11
c ---[2363]---> BDD-cost:   11
c ---[2362]---> BDD-cost:   11
c ---[2361]---> BDD-cost:   11
c ---[2360]---> BDD-cost:   11
c ---[2359]---> BDD-cost:   11
c ---[2358]---> BDD-cost:   11
c ---[2357]---> BDD-cost:   11
c ---[2356]---> BDD-cost:   11
c ---[2355]---> BDD-cost:   11
c ---[2354]---> BDD-cost:   11
c ---[2353]---> BDD-cost:   11
c ---[2352]---> BDD-cost:   11
c ---[2351]---> BDD-cost:   11
c ---[2350]---> BDD-cost:   11
c ---[2349]---> BDD-cost:   11
c ---[2348]---> BDD-cost:   11
c ---[2347]---> BDD-cost:   11
c ---[2346]---> BDD-cost:   11
c ---[2345]---> BDD-cost:   11
c ---[2344]---> BDD-cost:   11
c ---[2343]---> BDD-cost:   11
c ---[2342]---> BDD-cost:   11
c ---[2341]---> BDD-cost:   11
c ---[2340]---> BDD-cost:   11
c ---[2339]---> BDD-cost:   11
c ---[2338]---> BDD-cost:   11
c ---[2337]---> BDD-cost:   11
c ---[2336]---> BDD-cost:   11
c ---[2335]---> BDD-cost:   11
c ---[2334]---> BDD-cost:   11
c ---[2333]---> BDD-cost:   11
c ---[2332]---> BDD-cost:   11
c ---[2331]---> BDD-cost:   11
c ---[2330]---> BDD-cost:   11
c ---[2329]---> BDD-cost:   11
c ---[2328]---> BDD-cost:   11
c ---[2327]---> BDD-cost:   11
c ---[2326]---> BDD-cost:   11
c ---[2325]---> BDD-cost:   11
c ---[2324]---> BDD-cost:   11
c ---[2323]---> BDD-cost:   11
c ---[2322]---> BDD-cost:   11
c ---[2321]---> BDD-cost:   11
c ---[2320]---> BDD-cost:   11
c ---[2319]---> BDD-cost:   11
c ---[2318]---> BDD-cost:   11
c ---[2317]---> BDD-cost:   11
c ---[2316]---> BDD-cost:   11
c ---[2315]---> BDD-cost:   11
c ---[2314]---> BDD-cost:   11
c ---[2313]---> BDD-cost:   11
c ---[2312]---> BDD-cost:   11
c ---[2311]---> BDD-cost:   11
c ---[2310]---> BDD-cost:   11
c ---[2309]---> BDD-cost:   11
c ---[2308]---> BDD-cost:   11
c ---[2307]---> BDD-cost:   11
c ---[2306]---> BDD-cost:   11
c ---[2305]---> BDD-cost:   11
c ---[2304]---> BDD-cost:   11
c ---[2303]---> BDD-cost:   11
c ---[2302]---> BDD-cost:   11
c ---[2301]---> BDD-cost:   11
c ---[2300]---> BDD-cost:   11
c ---[2299]---> BDD-cost:   11
c ---[2298]---> BDD-cost:   11
c ---[2297]---> BDD-cost:   11
c ---[2296]---> BDD-cost:   11
c ---[2295]---> BDD-cost:   11
c ---[2294]---> BDD-cost:   11
c ---[2293]---> BDD-cost:   11
c ---[2292]---> BDD-cost:   11
c ---[2291]---> BDD-cost:   11
c ---[2290]---> BDD-cost:   11
c ---[2289]---> BDD-cost:   11
c ---[2288]---> BDD-cost:   11
c ---[2287]---> BDD-cost:   11
c ---[2286]---> BDD-cost:   11
c ---[2285]---> BDD-cost:   11
c ---[2284]---> BDD-cost:   11
c ---[2283]---> BDD-cost:    8
c ---[2282]---> BDD-cost:    8
c ---[2281]---> BDD-cost:    8
c ---[2280]---> BDD-cost:    8
c ---[2279]---> BDD-cost:    8
c ---[2278]---> BDD-cost:   86
c ---[2275]---> BDD-cost:  187
c ---[2274]---> BDD-cost:  197
c ---[2273]---> BDD-cost:  137
c ---[2272]---> BDD-cost:  159
c ---[2271]---> BDD-cost:  211
c ---[2270]---> BDD-cost:  131
c ---[2269]---> BDD-cost:   60
c ---[2268]---> BDD-cost:   60
c ---[2267]---> BDD-cost:   91
c ---[2266]---> BDD-cost:  131
c ---[2265]---> BDD-cost:    2
c ---[2264]---> BDD-cost:   92
c ---[2263]---> BDD-cost:  105
c ---[2262]---> BDD-cost:  141
c ---[2261]---> BDD-cost:   92
c ---[2260]---> BDD-cost:  107
c ---[2259]---> BDD-cost:  123
c ---[2258]---> BDD-cost:   60
c ---[2257]---> BDD-cost:   55
c ---[2256]---> BDD-cost:   67
c ---[2255]---> BDD-cost:  105
c ---[2253]---> BDD-cost:   71
c ---[2252]---> BDD-cost:   77
c ---[2251]---> BDD-cost:  105
c ---[2250]---> BDD-cost:   63
c ---[2249]---> BDD-cost:   67
c ---[2248]---> BDD-cost:   55
c ---[2247]---> BDD-cost:   60
c ---[2246]---> BDD-cost:   91
c ---[2245]---> BDD-cost:  131
c ---[2244]---> BDD-cost:   92
c ---[2243]---> BDD-cost:    2
c ---[2242]---> BDD-cost:  105
c ---[2241]---> BDD-cost:  141
c ---[2240]---> BDD-cost:   92
c ---[2239]---> BDD-cost:  107
c ---[2238]---> BDD-cost:  123
c ---[2237]---> BDD-cost:   60
c ---[2236]---> BDD-cost:   77
c ---[2235]---> BDD-cost:   84
c ---[2234]---> BDD-cost:   99
c ---[2233]---> BDD-cost:  141
c ---[2231]---> BDD-cost:  100
c ---[2230]---> BDD-cost:  101
c ---[2229]---> BDD-cost:  131
c ---[2228]---> BDD-cost:   79
c ---[2227]---> BDD-cost:   79
c ---[2226]---> BDD-cost:   55
c ---[2225]---> BDD-cost:   55
c ---[2224]---> BDD-cost:   39
c ---[2223]---> BDD-cost:   63
c ---[2222]---> BDD-cost:   85
c ---[2221]---> BDD-cost:    2
c ---[2220]---> BDD-cost:   55
c ---[2219]---> BDD-cost:   65
c ---[2218]---> BDD-cost:   75
c ---[2217]---> BDD-cost:   34
c ---[2216]---> BDD-cost:   43
c ---[2215]---> BDD-cost:   55
c ---[2214]---> BDD-cost:   39
c ---[2213]---> BDD-cost:   63
c ---[2212]---> BDD-cost:   85
c ---[2211]---> BDD-cost:   55
c ---[2209]---> BDD-cost:   65
c ---[2208]---> BDD-cost:   75
c ---[2207]---> BDD-cost:   34
c ---[2206]---> BDD-cost:   43
c ---[2205]---> BDD-cost:   55
c ---[2204]---> BDD-cost:   39
c ---[2203]---> BDD-cost:   63
c ---[2202]---> BDD-cost:   85
c ---[2201]---> BDD-cost:   55
c ---[2200]---> BDD-cost:   65
c ---[2199]---> BDD-cost:    2
c ---[2198]---> BDD-cost:   75
c ---[2197]---> BDD-cost:   34
c ---[2196]---> BDD-cost:   43
c ---[2195]---> BDD-cost:   61
c ---[2194]---> BDD-cost:   44
c ---[2193]---> BDD-cost:   69
c ---[2192]---> BDD-cost:   91
c ---[2191]---> BDD-cost:   60
c ---[2190]---> BDD-cost:   71
c ---[2189]---> BDD-cost:   81
c ---[2186]---> BDD-cost:   39
c ---[2185]---> BDD-cost:   61
c ---[2184]---> BDD-cost:   44
c ---[2183]---> BDD-cost:   99
c ---[2182]---> BDD-cost:  121
c ---[2181]---> BDD-cost:   84
c ---[2180]---> BDD-cost:  119
c ---[2179]---> BDD-cost:  141
c ---[2178]---> BDD-cost:   87
c ---[2177]---> BDD-cost:    2
c ---[2176]---> BDD-cost:   71
c ---[2175]---> BDD-cost:   81
c ---[2174]---> BDD-cost:   61
c ---[2173]---> BDD-cost:   26
c ---[2172]---> BDD-cost:   53
c ---[2171]---> BDD-cost:   53
c ---[2170]---> BDD-cost:   39
c ---[2169]---> BDD-cost:   22
c ---[2168]---> BDD-cost:   21
c ---[2167]---> BDD-cost:   33
c ---[2166]---> BDD-cost:    2
c ---[2164]---> BDD-cost:   33
c ---[2163]---> BDD-cost:   19
c ---[2162]---> BDD-cost:   26
c ---[2161]---> BDD-cost:   44
c ---[2160]---> BDD-cost:   50
c ---[2159]---> BDD-cost:   48
c ---[2158]---> BDD-cost:   21
c ---[2157]---> BDD-cost:   21
c ---[2156]---> BDD-cost:   33
c ---[2155]---> BDD-cost:   33
c ---[2154]---> BDD-cost:    8
c ---[2153]---> BDD-cost:   21
c ---[2152]---> BDD-cost:   25
c ---[2151]---> BDD-cost:   22
c ---[2150]---> BDD-cost:   21
c ---[2149]---> BDD-cost:   33
c ---[2148]---> BDD-cost:   33
c ---[2147]---> BDD-cost:   21
c ---[2146]---> BDD-cost:   30
c ---[2145]---> BDD-cost:   36
c ---[2144]---> BDD-cost:   28
c ---[2142]---> BDD-cost:   13
c ---[2141]---> BDD-cost:   19
c ---[2140]---> BDD-cost:   11
c ---[2139]---> BDD-cost:   13
c ---[2138]---> BDD-cost:   19
c ---[2137]---> BDD-cost:   11
c ---[2136]---> BDD-cost:   13
c ---[2135]---> BDD-cost:   19
c ---[2134]---> BDD-cost:   11
c ---[2133]---> BDD-cost:   15
c ---[2132]---> BDD-cost:    2
c ---[2131]---> BDD-cost:   21
c ---[2130]---> BDD-cost:   13
c ---[2129]---> BDD-cost:   15
c ---[2128]---> BDD-cost:   30
c ---[2127]---> BDD-cost:   31
c ---[2126]---> BDD-cost:   25
c ---[2110]---> BDD-cost:    2
c ---[2088]---> BDD-cost:    2
c ---[2066]---> BDD-cost:    2
c ---[2043]---> BDD-cost:    8
c ---[2021]---> BDD-cost:    8
c ---[1999]---> BDD-cost:    8
c ---[1993]---> BDD-cost:    9
c ---[1992]---> BDD-cost:   24
c ---[1991]---> BDD-cost:   14
c ---[1990]---> BDD-cost:   29
c ---[1989]---> BDD-cost:    9
c ---[1987]---> BDD-cost:   24
c ---[1985]---> BDD-cost:    1
c ---[1984]---> BDD-cost:   10
c ---[1983]---> BDD-cost:   14
c ---[1981]---> BDD-cost:    3
c ---[1980]---> BDD-cost:    8
c ---[1979]---> BDD-cost:    4
c ---[1977]---> BDD-cost:    2
c ---[1975]---> BDD-cost:    3
c ---[1974]---> BDD-cost:    2
c ---[1973]---> BDD-cost:    4
c ---[1972]---> BDD-cost:    2
c ---[1971]---> BDD-cost:    2
c ---[1970]---> BDD-cost:    3
c ---[1969]---> BDD-cost:    2
c ---[1968]---> BDD-cost:    2
c ---[1966]---> BDD-cost:    2
c ---[1963]---> BDD-cost:    4
c ---[1962]---> BDD-cost:    2
c ---[1961]---> BDD-cost:    3
c ---[1960]---> BDD-cost:   14
c ---[1959]---> BDD-cost:    4
c ---[1958]---> BDD-cost:   14
c ---[1957]---> BDD-cost:    3
c ---[1956]---> BDD-cost:    4
c ---[1954]---> BDD-cost:    2
c ---[1953]---> BDD-cost:    2
c ---[1952]---> BDD-cost:    2
c ---[1951]---> BDD-cost:    3
c ---[1950]---> BDD-cost:    2
c ---[1948]---> BDD-cost:    4
c ---[1947]---> BDD-cost:    2
c ---[1946]---> BDD-cost:    3
c ---[1945]---> BDD-cost:    2
c ---[1944]---> BDD-cost:    2
c ---[1942]---> BDD-cost:    2
c ---[1939]---> BDD-cost:    2
c ---[1938]---> BDD-cost:    2
c ---[1937]---> BDD-cost:    2
c ---[1936]---> BDD-cost:    2
c ---[1933]---> BDD-cost:    2
c ---[1932]---> BDD-cost:    3
c ---[1931]---> BDD-cost:    2
c ---[1930]---> BDD-cost:    4
c ---[1928]---> BDD-cost:    2
c ---[1927]---> BDD-cost:    3
c ---[1926]---> BDD-cost:    2
c ---[1925]---> BDD-cost:    2
c ---[1923]---> BDD-cost:    2
c ---[1921]---> BDD-cost:    4
c ---[1920]---> BDD-cost:    3
c ---[1917]---> BDD-cost:    7
c ---[1916]---> BDD-cost:    4
c ---[1915]---> BDD-cost:    3
c ---[1914]---> BDD-cost:    3
c ---[1913]---> BDD-cost:    2
c ---[1912]---> BDD-cost:    2
c ---[1911]---> BDD-cost:    2
c ---[1907]---> BDD-cost:    2
c ---[1905]---> BDD-cost:    2
c ---[1903]---> BDD-cost:    2
c ---[1902]---> BDD-cost:    2
c ---[1900]---> BDD-cost:    2
c ---[1897]---> BDD-cost:    2
c ---[1896]---> BDD-cost:    2
c ---[1894]---> BDD-cost:    2
c ---[1891]---> BDD-cost:    2
c ---[1889]---> BDD-cost:    2
c ---[1888]---> BDD-cost:    2
c ---[1885]---> BDD-cost:    9
c ---[1883]---> BDD-cost:   24
c ---[1882]---> BDD-cost:    4
c ---[1881]---> BDD-cost:    2
c ---[1880]---> BDD-cost:    2
c ---[1879]---> BDD-cost:    8
c ---[1877]---> BDD-cost:    5
c ---[1876]---> BDD-cost:    3
c ---[1874]---> BDD-cost:    2
c ---[1873]---> BDD-cost:    3
c ---[1869]---> BDD-cost:    2
c ---[1868]---> BDD-cost:    5
c ---[1867]---> BDD-cost:    3
c ---[1864]---> BDD-cost:    3
c ---[1861]---> BDD-cost:    2
c ---[1860]---> BDD-cost:    7
c ---[1859]---> BDD-cost:    5
c ---[1858]---> BDD-cost:    3
c ---[1856]---> BDD-cost:    5
c ---[1855]---> BDD-cost:    3
c ---[1854]---> BDD-cost:    2
c ---[1853]---> BDD-cost:    3
c ---[1851]---> BDD-cost:    5
c ---[1850]---> BDD-cost:    3
c ---[1848]---> BDD-cost:    2
c ---[1847]---> BDD-cost:    3
c ---[1842]---> BDD-cost:    5
c ---[1841]---> BDD-cost:    3
c ---[1840]---> BDD-cost:    8
c ---[1839]---> BDD-cost:    3
c ---[1837]---> BDD-cost:    5
c ---[1836]---> BDD-cost:    3
c ---[1834]---> BDD-cost:    8
c ---[1833]---> BDD-cost:    3
c ---[1829]---> BDD-cost:    5
c ---[1828]---> BDD-cost:    3
c ---[1827]---> BDD-cost:    8
c ---[1826]---> BDD-cost:    5
c ---[1825]---> BDD-cost:    3
c ---[1824]---> BDD-cost:    3
c ---[1822]---> BDD-cost:    3
c ---[1820]---> BDD-cost:    8
c ---[1817]---> BDD-cost:    3
c ---[1815]---> BDD-cost:    8
c ---[1813]---> BDD-cost:    3
c ---[1811]---> BDD-cost:    8
c ---[1808]---> BDD-cost:    2
c ---[1807]---> BDD-cost:    3
c ---[1803]---> BDD-cost:    3
c ---[1801]---> BDD-cost:    2
c ---[1796]---> BDD-cost:   17
c ---[1795]---> BDD-cost:   13
c ---[1794]---> BDD-cost:    9
c ---[1793]---> BDD-cost:    2
c ---[1792]---> BDD-cost:   17
c ---[1791]---> BDD-cost:    9
c ---[1790]---> BDD-cost:    5
c ---[1789]---> BDD-cost:   13
c ---[1788]---> BDD-cost:    9
c ---[1787]---> BDD-cost:    4
c ---[1786]---> BDD-cost:    9
c ---[1785]---> BDD-cost:    4
c ---[1784]---> BDD-cost:   16
c ---[1783]---> BDD-cost:   12
c ---[1781]---> BDD-cost:   12
c ---[1780]---> BDD-cost:    8
c ---[1779]---> BDD-cost:   13
c ---[1778]---> BDD-cost:    9
c ---[1777]---> BDD-cost:    9
c ---[1776]---> BDD-cost:    5
c ---[1775]---> BDD-cost:    9
c ---[1774]---> BDD-cost:    5
c ---[1773]---> BDD-cost:    9
c ---[1772]---> BDD-cost:    5
c ---[1771]---> BDD-cost:    2
c ---[1770]---> BDD-cost:   13
c ---[1769]---> BDD-cost:    9
c ---[1768]---> BDD-cost:    9
c ---[1767]---> BDD-cost:    5
c ---[1766]---> BDD-cost:   13
c ---[1765]---> BDD-cost:    9
c ---[1764]---> BDD-cost:    5
c ---[1763]---> BDD-cost:    9
c ---[1762]---> BDD-cost:    5
c ---[1761]---> BDD-cost:    9
c ---[1759]---> BDD-cost:    5
c ---[1758]---> BDD-cost:    5
c ---[1756]---> BDD-cost:    9
c ---[1755]---> BDD-cost:    5
c ---[1754]---> BDD-cost:    5
c ---[1752]---> BDD-cost:    9
c ---[1751]---> BDD-cost:    5
c ---[1750]---> BDD-cost:    5
c ---[1749]---> BDD-cost:    8
c ---[1747]---> BDD-cost:    9
c ---[1746]---> BDD-cost:    5
c ---[1745]---> BDD-cost:    5
c ---[1744]---> BDD-cost:   21
c ---[1743]---> BDD-cost:   17
c ---[1742]---> BDD-cost:    5
c ---[1741]---> BDD-cost:    9
c ---[1740]---> BDD-cost:   12
c ---[1736]---> BDD-cost:    4
c ---[1735]---> BDD-cost:    5
c ---[1734]---> BDD-cost:    9
c ---[1732]---> BDD-cost:    5
c ---[1731]---> BDD-cost:    4
c ---[1730]---> BDD-cost:    8
c ---[1728]---> BDD-cost:    4
c ---[1727]---> BDD-cost:    4
c ---[1726]---> BDD-cost:    8
c ---[1725]---> BDD-cost:    8
c ---[1723]---> BDD-cost:    4
c ---[1722]---> BDD-cost:    5
c ---[1721]---> BDD-cost:    9
c ---[1719]---> BDD-cost:    5
c ---[1717]---> BDD-cost:    5
c ---[1716]---> BDD-cost:    5
c ---[1714]---> BDD-cost:    9
c ---[1713]---> BDD-cost:    5
c ---[1712]---> BDD-cost:    5
c ---[1711]---> BDD-cost:    9
c ---[1708]---> BDD-cost:    5
c ---[1707]---> BDD-cost:    5
c ---[1704]---> BDD-cost:    8
c ---[1703]---> BDD-cost:    5
c ---[1702]---> BDD-cost:    5
c ---[1699]---> BDD-cost:    5
c ---[1698]---> BDD-cost:    5
c ---[1695]---> BDD-cost:    5
c ---[1691]---> BDD-cost:    5
c ---[1689]---> BDD-cost:   67
c ---[1687]---> Adder-cost: 182   maxlim: 13055   bits: 15/14
c ---[1685]---> Adder-cost: 226   maxlim: 15103   bits: 15/14
c ---[1683]---> BDD-cost:   67
c ---[1681]---> Sorter-cost:  307     Base: 2 2 2 2 2 2 2 2 2
c ---[1679]---> Sorter-cost: 1292     Base: 2 2 2 2 2 2 2 2
c ---[1677]---> Adder-cost: 186   maxlim: 14719   bits: 15/14
c ---[1676]---> BDD-cost:    1
c ---[1674]---> Adder-cost: 202   maxlim: 15231   bits: 15/14
c ---[1672]---> Sorter-cost:  502     Base: 2 2 2 2 2 2 2 2
c ---[1670]---> Adder-cost: 140   maxlim: 13311   bits: 15/14
c ---[1668]---> Adder-cost: 214   maxlim: 15103   bits: 15/14
c ---[1666]---> Sorter-cost:  564     Base: 2 2 2 2 2 2 2 2
c ---[1664]---> Adder-cost: 108   maxlim: 11775   bits: 14/14
c ---[1662]---> Adder-cost: 170   maxlim: 14847   bits: 15/14
c ---[1660]---> Adder-cost: 148   maxlim: 15359   bits: 15/14
c ---[1658]---> Sorter-cost:  896     Base: 2 2 2 2 2 2 2 2
c ---[1656]---> Adder-cost: 162   maxlim: 13567   bits: 15/14
c ---[1653]---> Adder-cost: 146   maxlim: 15871   bits: 15/14
c ---[1651]---> Sorter-cost:  890     Base: 2 2 2 2 2 2 2 2
c ---[1649]---> Adder-cost: 114   maxlim: 12287   bits: 14/14
c ---[1647]---> Adder-cost: 136   maxlim: 15103   bits: 15/14
c ---[1645]---> Adder-cost: 206   maxlim: 15871   bits: 15/14
c ---[1643]---> Sorter-cost: 1038     Base: 2 2 2 2 2 2 2 2
c ---[1641]---> Adder-cost: 132   maxlim: 13695   bits: 15/14
c ---[1639]---> Adder-cost: 172   maxlim: 16255   bits: 15/14
c ---[1637]---> Sorter-cost: 1070     Base: 2 2 2 2 2 2 2 2
c ---[1635]---> Adder-cost: 98   maxlim: 12671   bits: 14/14
c ---[1634]---> BDD-cost:    2
c ---[1632]---> Adder-cost: 166   maxlim: 15231   bits: 15/14
c ---[1630]---> Adder-cost: 166   maxlim: 15999   bits: 15/14
c ---[1628]---> Sorter-cost:  378     Base: 2 2 2 2 2 2 2 2
c ---[1626]---> Sorter-cost: 1199     Base: 2 2 2 2 2 2 2 2
c ---[1624]---> Adder-cost: 130   maxlim: 13823   bits: 15/14
c ---[1622]---> Adder-cost: 164   maxlim: 16383   bits: 15/14
c ---[1620]---> Adder-cost: 128   maxlim: 13055   bits: 14/14
c ---[1618]---> Adder-cost: 124   maxlim: 15359   bits: 15/14
c ---[1616]---> Adder-cost: 136   maxlim: 15743   bits: 15/14
c ---[1614]---> Sorter-cost:  660     Base: 2 2 2 2 2 2 2 2
c ---[1611]---> Sorter-cost: 1120     Base: 2 2 2 2 2 2 2 2
c ---[1609]---> Adder-cost: 124   maxlim: 14079   bits: 15/14
c ---[1607]---> Adder-cost: 166   maxlim: 16895   bits: 15/15
c ---[1605]---> Adder-cost: 106   maxlim: 13439   bits: 14/14
c ---[1603]---> Adder-cost: 126   maxlim: 15487   bits: 15/14
c ---[1601]---> Adder-cost: 152   maxlim: 15871   bits: 15/14
c ---[1599]---> Sorter-cost:  348     Base: 2 2 2 2 2 2 2 2
c ---[1597]---> Sorter-cost: 1235     Base: 2 2 2 2 2 2 2 2
c ---[1595]---> Adder-cost: 144   maxlim: 14207   bits: 15/14
c ---[1593]---> Adder-cost: 150   maxlim: 17023   bits: 15/15
c ---[1592]---> BDD-cost:    2
c ---[1590]---> Adder-cost: 120   maxlim: 13823   bits: 15/14
c ---[1588]---> Adder-cost: 134   maxlim: 15615   bits: 15/14
c ---[1586]---> Adder-cost: 180   maxlim: 15615   bits: 15/14
c ---[1584]---> Sorter-cost:  290     Base: 2 2 2 2 2 2 2 2 2
c ---[1582]---> Sorter-cost: 1326     Base: 2 2 2 2 2 2 2 2
c ---[1580]---> Adder-cost: 136   maxlim: 14335   bits: 15/14
c ---[1578]---> Adder-cost: 158   maxlim: 17151   bits: 15/15
c ---[1576]---> BDD-cost:   89
c ---[1574]---> Adder-cost: 114   maxlim: 14079   bits: 15/14
c ---[1572]---> Adder-cost: 136   maxlim: 15615   bits: 15/14
c ---[1571]---> BDD-cost:    8
c ---[1568]---> Sorter-cost: 1447     Base: 2 2 2 2 2 2 2 2
c ---[1566]---> Adder-cost: 122   maxlim: 14463   bits: 15/14
c ---[1564]---> Adder-cost: 144   maxlim: 17279   bits: 15/15
c ---[1562]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 2
c ---[1560]---> Adder-cost: 110   maxlim: 14207   bits: 15/14
c ---[1558]---> Adder-cost: 124   maxlim: 15487   bits: 15/14
c ---[1556]---> Sorter-cost: 1492     Base: 2 2 2 2 2 2 2 2
c ---[1554]---> Adder-cost: 124   maxlim: 14591   bits: 15/14
c ---[1552]---> Adder-cost: 154   maxlim: 17407   bits: 15/15
c ---[1550]---> Sorter-cost:  570     Base: 2 2 2 2 2 2 2 2
c ---[1549]---> BDD-cost:    2
c ---[1547]---> Adder-cost: 112   maxlim: 14335   bits: 15/14
c ---[1545]---> Adder-cost: 114   maxlim: 15359   bits: 15/14
c ---[1543]---> Adder-cost: 104   maxlim: 12031   bits: 14/14
c ---[1541]---> Adder-cost: 128   maxlim: 14591   bits: 15/14
c ---[1539]---> Adder-cost: 250   maxlim: 17023   bits: 15/15
c ---[1537]---> Sorter-cost:  760     Base: 2 2 2 2 2 2 2 2
c ---[1535]---> Adder-cost: 108   maxlim: 14463   bits: 15/14
c ---[1533]---> Adder-cost: 144   maxlim: 15487   bits: 15/14
c ---[1531]---> Adder-cost: 92   maxlim: 12671   bits: 14/14
c ---[1529]---> Adder-cost: 168   maxlim: 14975   bits: 15/14
c ---[1526]---> Sorter-cost: 1006     Base: 2 2 2 2 2 2 2 2
c ---[1524]---> Adder-cost: 106   maxlim: 14591   bits: 15/14
c ---[1522]---> Adder-cost: 114   maxlim: 15359   bits: 15/14
c ---[1520]---> BDD-cost:   72
c ---[1518]---> Adder-cost: 182   maxlim: 13055   bits: 15/14
c ---[1516]---> Adder-cost: 228   maxlim: 15103   bits: 15/14
c ---[1514]---> BDD-cost:   72
c ---[1512]---> Sorter-cost:  318     Base: 2 2 2 2 2 2 2 2 2 2
c ---[1510]---> Adder-cost: 118   maxlim: 11391   bits: 14/14
c ---[1508]---> Adder-cost: 174   maxlim: 14719   bits: 15/14
c ---[1507]---> BDD-cost:    1
c ---[1505]---> Adder-cost: 204   maxlim: 15231   bits: 15/14
c ---[1503]---> Sorter-cost:  560     Base: 2 2 2 2 2 2 2 2 2
c ---[1501]---> Adder-cost: 140   maxlim: 13311   bits: 15/14
c ---[1499]---> Adder-cost: 216   maxlim: 15103   bits: 15/14
c ---[1497]---> Sorter-cost:  643     Base: 2 2 2 2 2 2 2 2 2
c ---[1495]---> Adder-cost: 108   maxlim: 11775   bits: 14/14
c ---[1493]---> Adder-cost: 164   maxlim: 14847   bits: 15/14
c ---[1491]---> Adder-cost: 150   maxlim: 15359   bits: 15/14
c ---[1489]---> Adder-cost: 86   maxlim: 8831   bits: 14/14
c ---[1487]---> Adder-cost: 162   maxlim: 13567   bits: 15/14
c ---[1484]---> Adder-cost: 146   maxlim: 15871   bits: 15/14
c ---[1482]---> Sorter-cost:  937     Base: 2 2 2 2 2 2 2 2 2
c ---[1480]---> Adder-cost: 96   maxlim: 12287   bits: 15/14
c ---[1478]---> Adder-cost: 136   maxlim: 15103   bits: 15/14
c ---[1476]---> Adder-cost: 206   maxlim: 15871   bits: 15/14
c ---[1474]---> Adder-cost: 84   maxlim: 9343   bits: 14/14
c ---[1472]---> Adder-cost: 132   maxlim: 13695   bits: 15/14
c ---[1470]---> Adder-cost: 172   maxlim: 16255   bits: 15/14
c ---[1468]---> Sorter-cost: 1338     Base: 2 2 2 2 2 2 2 2
c ---[1466]---> Adder-cost: 104   maxlim: 12671   bits: 15/14
c ---[1465]---> BDD-cost:    2
c ---[1463]---> Adder-cost: 168   maxlim: 15231   bits: 15/14
c ---[1461]---> Adder-cost: 166   maxlim: 15999   bits: 15/14
c ---[1459]---> Sorter-cost:  338     Base: 2 2 2 2 2 2 2 2 2 2
c ---[1457]---> Adder-cost: 84   maxlim: 9727   bits: 14/14
c ---[1455]---> Adder-cost: 130   maxlim: 13823   bits: 15/14
c ---[1453]---> Adder-cost: 164   maxlim: 16383   bits: 15/14
c ---[1451]---> Adder-cost: 134   maxlim: 13055   bits: 15/14
c ---[1449]---> Adder-cost: 126   maxlim: 15359   bits: 15/14
c ---[1447]---> Adder-cost: 136   maxlim: 15743   bits: 15/14
c ---[1445]---> Sorter-cost:  767     Base: 2 2 2 2 2 2 2 2 2
c ---[1442]---> Adder-cost: 82   maxlim: 10239   bits: 14/14
c ---[1440]---> Adder-cost: 124   maxlim: 14079   bits: 15/14
c ---[1438]---> Adder-cost: 170   maxlim: 16895   bits: 15/15
c ---[1436]---> Adder-cost: 112   maxlim: 13439   bits: 15/14
c ---[1434]---> Adder-cost: 128   maxlim: 15487   bits: 15/14
c ---[1432]---> Adder-cost: 152   maxlim: 15871   bits: 15/14
c ---[1430]---> Sorter-cost:  288     Base: 2 2 2 2 2 2 2 2 2 2
c ---[1428]---> Adder-cost: 74   maxlim: 10623   bits: 14/14
c ---[1426]---> Adder-cost: 144   maxlim: 14207   bits: 15/14
c ---[1424]---> Adder-cost: 154   maxlim: 17023   bits: 15/15
c ---[1423]---> BDD-cost:    2
c ---[1421]---> Adder-cost: 120   maxlim: 13823   bits: 15/14
c ---[1419]---> Adder-cost: 136   maxlim: 15615   bits: 15/14
c ---[1417]---> Adder-cost: 180   maxlim: 15615   bits: 15/14
c ---[1415]---> Sorter-cost:  316     Base: 2 2 2 2 2 2 2 2 2 2
c ---[1413]---> Adder-cost: 86   maxlim: 11007   bits: 14/14
c ---[1411]---> Adder-cost: 138   maxlim: 14335   bits: 15/14
c ---[1409]---> Adder-cost: 162   maxlim: 17151   bits: 15/15
c ---[1407]---> BDD-cost:   97
c ---[1405]---> Adder-cost: 114   maxlim: 14079   bits: 15/14
c ---[1403]---> Adder-cost: 138   maxlim: 15615   bits: 15/14
c ---[1400]---> Adder-cost: 84   maxlim: 11391   bits: 14/14
c ---[1398]---> Adder-cost: 124   maxlim: 14463   bits: 15/14
c ---[1396]---> Adder-cost: 148   maxlim: 17279   bits: 15/15
c ---[1394]---> Sorter-cost:  493     Base: 2 2 2 2 2 2 2 2 2
c ---[1392]---> Adder-cost: 110   maxlim: 14207   bits: 15/14
c ---[1390]---> Adder-cost: 126   maxlim: 15487   bits: 15/14
c ---[1388]---> Adder-cost: 94   maxlim: 11775   bits: 15/14
c ---[1386]---> Adder-cost: 126   maxlim: 14591   bits: 15/14
c ---[1384]---> Adder-cost: 154   maxlim: 17407   bits: 15/15
c ---[1382]---> Sorter-cost:  685     Base: 2 2 2 2 2 2 2 2 2
c ---[1381]---> BDD-cost:    1
c ---[1379]---> Adder-cost: 112   maxlim: 14335   bits: 15/14
c ---[1377]---> Adder-cost: 116   maxlim: 15359   bits: 15/14
c ---[1375]---> Adder-cost: 110   maxlim: 12031   bits: 15/14
c ---[1373]---> Adder-cost: 130   maxlim: 14591   bits: 15/14
c ---[1371]---> Adder-cost: 250   maxlim: 17023   bits: 15/15
c ---[1369]---> Sorter-cost:  827     Base: 2 2 2 2 2 2 2 2 2
c ---[1367]---> Adder-cost: 108   maxlim: 14463   bits: 15/14
c ---[1365]---> Adder-cost: 146   maxlim: 15487   bits: 15/14
c ---[1363]---> Adder-cost: 98   maxlim: 12671   bits: 15/14
c ---[1361]---> Adder-cost: 170   maxlim: 14975   bits: 15/14
c ---[1359]---> Sorter-cost:  733     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1355]---> Sorter-cost: 1308     Base: 2 2 2 2 2 2 2 2
c ---[1353]---> Adder-cost: 106   maxlim: 14591   bits: 15/14
c ---[1351]---> Adder-cost: 116   maxlim: 15359   bits: 15/14
c ---[1349]---> Adder-cost: 244   maxlim: 13823   bits: 15/14
c ---[1347]---> Sorter-cost:  902     Base: 2 2 2 2 2 2 2 2
c ---[1345]---> Adder-cost: 178   maxlim: 9983   bits: 15/14
c ---[1343]---> Adder-cost: 140   maxlim: 12543   bits: 15/14
c ---[1341]---> Sorter-cost:  540     Base: 2 2 2 2 2 2 2 2 2
c ---[1339]---> Adder-cost: 244   maxlim: 13823   bits: 15/14
c ---[1337]---> Sorter-cost:  792     Base: 2 2 2 2 2 2 2 2 2
c ---[1336]---> BDD-cost:    2
c ---[1334]---> Adder-cost: 178   maxlim: 9983   bits: 15/14
c ---[1332]---> Adder-cost: 140   maxlim: 12543   bits: 15/14
c ---[1330]---> Sorter-cost:  592     Base: 2 2 2 2 2 2 2 2 2
c ---[1329]---> BDD-cost:   84
c ---[1328]---> BDD-cost:   83
c ---[1327]---> BDD-cost:   84
c ---[1326]---> BDD-cost:   84
c ---[1325]---> BDD-cost:   83
c ---[1324]---> BDD-cost:   88
c ---[1323]---> BDD-cost:   87
c ---[1321]---> BDD-cost:   88
c ---[1320]---> BDD-cost:   88
c ---[1319]---> BDD-cost:   87
c ---[1318]---> Sorter-cost:  620     Base: 2 2 2 2 2 2 2 2 2 2
c ---[1317]---> Sorter-cost:  685     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1311]---> BDD-cost:    2
c ---[1289]---> BDD-cost:    1
c ---[1267]---> BDD-cost:    2
c ---[1245]---> BDD-cost:    8
c ---[1234]---> BDD-cost:    8
c ---[1222]---> BDD-cost:    8
c ---[1212]---> BDD-cost:   21
c ---[1210]---> BDD-cost:   23
c ---[1206]---> BDD-cost:   21
c ---[1200]---> BDD-cost:    8
c ---[1187]---> BDD-cost:   21
c ---[1186]---> BDD-cost:   15
c ---[1184]---> BDD-cost:   87
c ---[1183]---> BDD-cost:   84
c ---[1182]---> BDD-cost:   54
c ---[1181]---> BDD-cost:   42
c ---[1179]---> BDD-cost:   24
c ---[1178]---> BDD-cost:    2
c ---[1175]---> BDD-cost:   71
c ---[1174]---> BDD-cost:   54
c ---[1173]---> BDD-cost:   58
c ---[1172]---> BDD-cost:   60
c ---[1171]---> BDD-cost:   25
c ---[1170]---> BDD-cost:   17
c ---[1169]---> BDD-cost:   19
c ---[1168]---> BDD-cost:   17
c ---[1166]---> BDD-cost:   88
c ---[1165]---> BDD-cost:   55
c ---[1164]---> BDD-cost:   66
c ---[1163]---> BDD-cost:   54
c ---[1156]---> BDD-cost:    1
c ---[1134]---> BDD-cost:    1
c ---[1111]---> BDD-cost:    1
c ---[1089]---> BDD-cost:    8
c ---[1067]---> BDD-cost:    8
c ---[1047]---> BDD-cost:    9
c ---[1045]---> BDD-cost:    1
c ---[1037]---> BDD-cost:   21
c ---[1033]---> BDD-cost:    0
c ---[1032]---> BDD-cost:    0
c ---[1031]---> BDD-cost:   38
c ---[1030]---> BDD-cost:    0
c ---[1028]---> BDD-cost:   27
c ---[1027]---> BDD-cost:    0
c ---[1026]---> BDD-cost:   23
c ---[1024]---> BDD-cost:    0
c ---[1023]---> BDD-cost:    2
c ---[1022]---> BDD-cost:    0
c ---[1021]---> BDD-cost:    0
c ---[1020]---> BDD-cost:    0
c ---[1019]---> BDD-cost:    0
c ---[1018]---> BDD-cost:   22
c ---[1017]---> BDD-cost:    0
c ---[1016]---> BDD-cost:    1
c ---[1014]---> BDD-cost:    2
c ---[1012]---> BDD-cost:    1
c ---[1010]---> BDD-cost:    2
c ---[1008]---> BDD-cost:    2
c ---[1006]---> BDD-cost:    1
c ---[1003]---> BDD-cost:    2
c ---[1001]---> BDD-cost:    1
c ---[ 999]---> BDD-cost:    2
c ---[ 997]---> BDD-cost:    8
c ---[ 995]---> BDD-cost:    2
c ---[ 994]---> BDD-cost:    2
c ---[ 992]---> BDD-cost:    1
c ---[ 990]---> BDD-cost:    1
c ---[ 988]---> BDD-cost:    1
c ---[ 986]---> BDD-cost:    8
c ---[ 984]---> BDD-cost:    8
c ---[ 981]---> BDD-cost:    8
c ---[ 979]---> BDD-cost:    1
c ---[ 977]---> BDD-cost:    2
c ---[ 975]---> BDD-cost:    2
c ---[ 973]---> BDD-cost:    2
c ---[ 972]---> BDD-cost:    2
c ---[ 970]---> BDD-cost:    1
c ---[ 968]---> BDD-cost:    2
c ---[ 966]---> BDD-cost:    2
c ---[ 964]---> BDD-cost:    1
c ---[ 962]---> BDD-cost:    2
c ---[ 959]---> BDD-cost:    2
c ---[ 957]---> BDD-cost:    1
c ---[ 955]---> BDD-cost:    2
c ---[ 953]---> BDD-cost:    8
c ---[ 951]---> BDD-cost:    8
c ---[ 950]---> BDD-cost:    2
c ---[ 948]---> BDD-cost:    8
c ---[ 946]---> BDD-cost:    8
c ---[ 944]---> BDD-cost:    1
c ---[ 942]---> BDD-cost:    1
c ---[ 940]---> BDD-cost:    1
c ---[ 938]---> Adder-cost: 1246   maxlim: 131071   bits: 18/17
c ---[ 935]---> BDD-cost:    6
c ---[ 933]---> BDD-cost:    8
c ---[ 931]---> BDD-cost:    8
c ---[ 929]---> BDD-cost:    1
c ---[ 927]---> BDD-cost:    2
c ---[ 926]---> BDD-cost:    2
c ---[ 924]---> BDD-cost:    2
c ---[ 922]---> BDD-cost:    2
c ---[ 920]---> BDD-cost:    1
c ---[ 918]---> BDD-cost:    2
c ---[ 916]---> BDD-cost:    2
c ---[ 913]---> BDD-cost:    1
c ---[ 911]---> BDD-cost:    2
c ---[ 909]---> BDD-cost:    2
c ---[ 907]---> BDD-cost:    1
c ---[ 905]---> BDD-cost:    2
c ---[ 904]---> BDD-cost:    1
c ---[ 902]---> BDD-cost:    1
c ---[ 900]---> BDD-cost:    2
c ---[ 898]---> BDD-cost:    8
c ---[ 896]---> BDD-cost:    2
c ---[ 894]---> BDD-cost:    2
c ---[ 891]---> BDD-cost:    1
c ---[ 889]---> BDD-cost:    1
c ---[ 887]---> BDD-cost:    8
c ---[ 885]---> BDD-cost:    8
c ---[ 883]---> BDD-cost:    1
c ---[ 882]---> BDD-cost:    2
c ---[ 880]---> BDD-cost:    2
c ---[ 878]---> BDD-cost:    2
c ---[ 876]---> BDD-cost:    1
c ---[ 874]---> BDD-cost:    2
c ---[ 872]---> BDD-cost:    1
c ---[ 869]---> BDD-cost:    2
c ---[ 867]---> BDD-cost:    2
c ---[ 865]---> BDD-cost:    8
c ---[ 863]---> BDD-cost:    2
c ---[ 861]---> BDD-cost:    2
c ---[ 860]---> BDD-cost:    2
c ---[ 858]---> BDD-cost:    1
c ---[ 856]---> BDD-cost:    1
c ---[ 854]---> BDD-cost:    8
c ---[ 852]---> BDD-cost:    8
c ---[ 850]---> BDD-cost:    1
c ---[ 847]---> BDD-cost:    2
c ---[ 845]---> BDD-cost:    2
c ---[ 843]---> BDD-cost:    1
c ---[ 841]---> BDD-cost:    2
c ---[ 839]---> BDD-cost:    1
c ---[ 838]---> BDD-cost:    2
c ---[ 836]---> BDD-cost:    2
c ---[ 834]---> BDD-cost:    2
c ---[ 832]---> BDD-cost:    8
c ---[ 830]---> BDD-cost:    1
c ---[ 828]---> BDD-cost:    2
c ---[ 826]---> Adder-cost: 1776   maxlim: 524287   bits: 20/19
c ---[ 823]---> BDD-cost:    1
c ---[ 821]---> BDD-cost:    1
c ---[ 819]---> BDD-cost:    8
c ---[ 817]---> BDD-cost:    8
c ---[ 815]---> BDD-cost:    1
c ---[ 814]---> BDD-cost:    2
c ---[ 812]---> BDD-cost:    2
c ---[ 810]---> BDD-cost:    2
c ---[ 808]---> BDD-cost:    1
c ---[ 806]---> BDD-cost:    2
c ---[ 804]---> BDD-cost:    1
c ---[ 801]---> BDD-cost:    2
c ---[ 799]---> BDD-cost:    2
c ---[ 797]---> BDD-cost:    8
c ---[ 795]---> BDD-cost:    1
c ---[ 793]---> BDD-cost:    2
c ---[ 792]---> BDD-cost:    1
c ---[ 790]---> BDD-cost:    1
c ---[ 788]---> BDD-cost:    6
c ---[ 786]---> BDD-cost:    8
c ---[ 784]---> BDD-cost:    8
c ---[ 782]---> BDD-cost:    1
c ---[ 779]---> BDD-cost:    2
c ---[ 777]---> BDD-cost:    2
c ---[ 775]---> BDD-cost:    1
c ---[ 773]---> BDD-cost:    2
c ---[ 771]---> BDD-cost:    1
c ---[ 770]---> BDD-cost:    2
c ---[ 768]---> BDD-cost:    2
c ---[ 766]---> BDD-cost:    8
c ---[ 764]---> BDD-cost:    8
c ---[ 762]---> BDD-cost:    2
c ---[ 760]---> BDD-cost:    2
c ---[ 757]---> BDD-cost:    1
c ---[ 755]---> BDD-cost:    8
c ---[ 753]---> BDD-cost:    8
c ---[ 751]---> BDD-cost:    8
c ---[ 749]---> BDD-cost:    1
c ---[ 748]---> BDD-cost:    2
c ---[ 746]---> BDD-cost:    2
c ---[ 744]---> BDD-cost:    2
c ---[ 742]---> BDD-cost:    2
c ---[ 740]---> BDD-cost:    2
c ---[ 738]---> BDD-cost:    2
c ---[ 735]---> BDD-cost:    1
c ---[ 733]---> BDD-cost:    2
c ---[ 731]---> BDD-cost:    1
c ---[ 729]---> BDD-cost:    2
c ---[ 727]---> BDD-cost:    2
c ---[ 726]---> BDD-cost:    1
c ---[ 724]---> BDD-cost:    2
c ---[ 722]---> BDD-cost:    2
c ---[ 720]---> BDD-cost:    8
c ---[ 718]---> BDD-cost:    8
c ---[ 714]---> Adder-cost: 2784   maxlim: 2097151   bits: 22/21
c ---[ 702]---> BDD-cost:    2
c ---[ 689]---> BDD-cost:  299
c ---[ 685]---> BDD-cost:  244
c ---[ 680]---> BDD-cost:    2
c ---[ 677]---> BDD-cost:  330
c ---[ 673]---> BDD-cost:  464
c ---[ 672]---> BDD-cost:  137
c ---[ 667]---> BDD-cost:   61
c ---[ 666]---> BDD-cost:  323
c ---[ 665]---> BDD-cost:    4
c ---[ 663]---> BDD-cost:  142
c ---[ 662]---> BDD-cost:  367
c ---[ 661]---> BDD-cost:   95
c ---[ 658]---> BDD-cost:    2
c ---[ 656]---> BDD-cost:  147
c ---[ 653]---> BDD-cost:  174
c ---[ 652]---> BDD-cost:  284
c ---[ 641]---> BDD-cost:  180
c ---[ 640]---> BDD-cost:  296
c ---[ 636]---> BDD-cost:    1
c ---[ 633]---> BDD-cost:   72
c ---[ 630]---> BDD-cost:  233
c ---[ 629]---> BDD-cost:   72
c ---[ 626]---> BDD-cost:   51
c ---[ 622]---> BDD-cost:    0
c ---[ 620]---> BDD-cost:  275
c ---[ 619]---> BDD-cost:   69
c ---[ 616]---> BDD-cost:  150
c ---[ 614]---> BDD-cost:    2
c ---[ 610]---> BDD-cost:  331
c ---[ 609]---> BDD-cost:    4
c ---[ 606]---> BDD-cost:  185
c ---[ 601]---> BDD-cost:   31
c ---[ 599]---> BDD-cost:  262
c ---[ 595]---> BDD-cost:  147
c ---[ 592]---> BDD-cost:  147
c ---[ 591]---> BDD-cost:    1
c ---[ 589]---> BDD-cost:  191
c ---[ 569]---> BDD-cost:    2
c ---[ 557]---> BDD-cost:  182
c ---[ 547]---> BDD-cost:    2
c ---[ 545]---> BDD-cost:  125
c ---[ 541]---> BDD-cost:  208
c ---[ 534]---> BDD-cost:   43
c ---[ 531]---> BDD-cost:   61
c ---[ 530]---> BDD-cost:  161
c ---[ 525]---> BDD-cost:    8
c ---[ 520]---> BDD-cost:   68
c ---[ 503]---> BDD-cost:    2
c ---[ 498]---> BDD-cost:   44
c ---[ 494]---> BDD-cost:   30
c ---[ 492]---> BDD-cost:    2
c ---[ 487]---> BDD-cost:   68
c ---[ 483]---> BDD-cost:   41
c ---[ 480]---> BDD-cost:    1
c ---[ 477]---> BDD-cost:   67
c ---[ 473]---> BDD-cost:   53
c ---[ 467]---> BDD-cost:   64
c ---[ 463]---> BDD-cost:   36
c ---[ 458]---> BDD-cost:    1
c ---[ 457]---> BDD-cost:   73
c ---[ 451]---> BDD-cost:   12
c ---[ 450]---> BDD-cost:   12
c ---[ 449]---> BDD-cost:   12
c ---[ 448]---> BDD-cost:   12
c ---[ 446]---> BDD-cost:   14
c ---[ 445]---> BDD-cost:   14
c ---[ 444]---> BDD-cost:   12
c ---[ 443]---> BDD-cost:   13
c ---[ 442]---> BDD-cost:   12
c ---[ 441]---> BDD-cost:    1
c ---[ 440]---> BDD-cost:   14
c ---[ 439]---> BDD-cost:   14
c ---[ 438]---> BDD-cost:   12
c ---[ 437]---> BDD-cost:   13
c ---[ 436]---> BDD-cost:   13
c ---[ 434]---> BDD-cost:   13
c ---[ 433]---> BDD-cost:   12
c ---[ 431]---> BDD-cost:   12
c ---[ 430]---> BDD-cost:    8
c ---[ 429]---> BDD-cost:   14
c ---[ 428]---> BDD-cost:   12
c ---[ 427]---> BDD-cost:   15
c ---[ 426]---> BDD-cost:   14
c ---[ 425]---> BDD-cost:   13
c ---[ 423]---> BDD-cost:   15
c ---[ 421]---> BDD-cost:   13
c ---[ 420]---> BDD-cost:   14
c ---[ 419]---> BDD-cost:   14
c ---[ 417]---> BDD-cost:    8
c ---[ 415]---> BDD-cost:   15
c ---[ 414]---> BDD-cost:   12
c ---[ 410]---> BDD-cost:   12
c ---[ 408]---> BDD-cost:   15
c ---[ 407]---> BDD-cost:   13
c ---[ 405]---> BDD-cost:    8
c ---[ 404]---> BDD-cost:   13
c ---[ 403]---> BDD-cost:   13
c ---[ 402]---> BDD-cost:   15
c ---[ 401]---> BDD-cost:   14
c ---[ 400]---> BDD-cost:   14
c ---[ 399]---> BDD-cost:   13
c ---[ 396]---> BDD-cost:   14
c ---[ 395]---> BDD-cost:   13
c ---[ 394]---> BDD-cost:   15
c ---[ 393]---> BDD-cost:   12
c ---[ 392]---> BDD-cost:    1
c ---[ 391]---> BDD-cost:   11
c ---[ 390]---> BDD-cost:   14
c ---[ 389]---> BDD-cost:   15
c ---[ 388]---> BDD-cost:   13
c ---[ 385]---> BDD-cost:   15
c ---[ 384]---> BDD-cost:   15
c ---[ 383]---> BDD-cost:   14
c ---[ 382]---> BDD-cost:   14
c ---[ 381]---> BDD-cost:   13
c ---[ 380]---> BDD-cost:    2
c ---[ 379]---> BDD-cost:    8
c ---[ 378]---> BDD-cost:    9
c ---[ 377]---> BDD-cost:    9
c ---[ 376]---> BDD-cost:    8
c ---[ 374]---> BDD-cost:    9
c ---[ 373]---> BDD-cost:    9
c ---[ 371]---> BDD-cost:    9
c ---[ 370]---> BDD-cost:   10
c ---[ 369]---> BDD-cost:    8
c ---[ 368]---> BDD-cost:    2
c ---[ 367]---> BDD-cost:   10
c ---[ 366]---> BDD-cost:   10
c ---[ 365]---> BDD-cost:   10
c ---[ 363]---> BDD-cost:    9
c ---[ 361]---> BDD-cost:    8
c ---[ 360]---> BDD-cost:    7
c ---[ 359]---> BDD-cost:   10
c ---[ 358]---> BDD-cost:   11
c ---[ 357]---> BDD-cost:    2
c ---[ 356]---> BDD-cost:    8
c ---[ 355]---> BDD-cost:   11
c ---[ 354]---> BDD-cost:   10
c ---[ 352]---> BDD-cost:    9
c ---[ 351]---> BDD-cost:    1
c ---[ 349]---> BDD-cost:    9
c ---[ 348]---> BDD-cost:   11
c ---[ 347]---> BDD-cost:    8
c ---[ 346]---> BDD-cost:   10
c ---[ 345]---> BDD-cost:    9
c ---[ 344]---> BDD-cost:    1
c ---[ 343]---> BDD-cost:   10
c ---[ 342]---> BDD-cost:   10
c ---[ 341]---> BDD-cost:    6
c ---[ 340]---> BDD-cost:    6
c ---[ 339]---> BDD-cost:    9
c ---[ 337]---> BDD-cost:    8
c ---[ 336]---> BDD-cost:   10
c ---[ 335]---> BDD-cost:    9
c ---[ 334]---> BDD-cost:    9
c ---[ 333]---> BDD-cost:   10
c ---[ 332]---> BDD-cost:    2
c ---[ 331]---> BDD-cost:    5
c ---[ 330]---> BDD-cost:   10
c ---[ 329]---> BDD-cost:   10
c ---[ 328]---> BDD-cost:   10
c ---[ 327]---> BDD-cost:    8
c ---[ 325]---> BDD-cost:    6
c ---[ 323]---> BDD-cost:    9
c ---[ 321]---> BDD-cost:    8
c ---[ 320]---> BDD-cost:    8
c ---[ 319]---> BDD-cost:    2
c ---[ 316]---> BDD-cost:    6
c ---[ 315]---> BDD-cost:    9
c ---[ 312]---> BDD-cost:    8
c ---[ 311]---> BDD-cost:   10
c ---[ 310]---> BDD-cost:    8
c ---[ 309]---> BDD-cost:    8
c ---[ 308]---> BDD-cost:    1
c ---[ 307]---> BDD-cost:   71
c ---[ 306]---> BDD-cost:  113
c ---[ 305]---> BDD-cost:  134
c ---[ 304]---> BDD-cost:  207
c ---[ 303]---> BDD-cost:  143
c ---[ 302]---> BDD-cost:  157
c ---[ 300]---> BDD-cost:  217
c ---[ 299]---> BDD-cost:  143
c ---[ 298]---> BDD-cost:  147
c ---[ 297]---> BDD-cost:  187
c ---[ 296]---> BDD-cost:  106
c ---[ 295]---> BDD-cost:   63
c ---[ 294]---> BDD-cost:   58
c ---[ 293]---> BDD-cost:   91
c ---[ 292]---> BDD-cost:  131
c ---[ 291]---> BDD-cost:   90
c ---[ 290]---> BDD-cost:    2
c ---[ 289]---> BDD-cost:  105
c ---[ 288]---> BDD-cost:  141
c ---[ 287]---> BDD-cost:   90
c ---[ 286]---> BDD-cost:   95
c ---[ 285]---> BDD-cost:  111
c ---[ 284]---> BDD-cost:   55
c ---[ 283]---> BDD-cost:   66
c ---[ 282]---> BDD-cost:   93
c ---[ 281]---> BDD-cost:  165
c ---[ 280]---> BDD-cost:   73
c ---[ 279]---> BDD-cost:    1
c ---[ 278]---> BDD-cost:    1
c ---[ 277]---> BDD-cost:    1
c ---[ 276]---> BDD-cost:    1
c ---[ 275]---> BDD-cost:    1
c ---[ 274]---> BDD-cost:    1
c ---[ 273]---> BDD-cost:    1
c ---[ 272]---> BDD-cost:    1
c ---[ 271]---> BDD-cost:    1
c ---[ 270]---> BDD-cost:    1
c ---[ 269]---> BDD-cost:    1
c ---[ 268]---> BDD-cost:    1
c ---[ 267]---> BDD-cost:    1
c ---[ 266]---> BDD-cost:    1
c ---[ 265]---> BDD-cost:    1
c ---[ 264]---> BDD-cost:    1
c ---[ 263]---> BDD-cost:    1
c ---[ 262]---> BDD-cost:    1
c ---[ 261]---> BDD-cost:    1
c ---[ 260]---> BDD-cost:    1
c ---[ 259]---> BDD-cost:    1
c ---[ 258]---> BDD-cost:    1
c ---[ 257]---> BDD-cost:    1
c ---[ 256]---> BDD-cost:    1
c ---[ 255]---> BDD-cost:    1
c ---[ 254]---> BDD-cost:    1
c ---[ 253]---> BDD-cost:    1
c ---[ 252]---> BDD-cost:   76
c ---[ 251]---> BDD-cost:   80
c ---[ 250]---> BDD-cost:   64
c ---[ 249]---> BDD-cost:   13
c ---[ 248]---> BDD-cost:   41
c ---[ 247]---> BDD-cost:   48
c ---[ 246]---> BDD-cost:   52
c ---[ 245]---> BDD-cost:   40
c ---[ 244]---> BDD-cost:    1
c ---[ 243]---> BDD-cost:   60
c ---[ 242]---> BDD-cost:   68
c ---[ 241]---> BDD-cost:   72
c ---[ 240]---> BDD-cost:    1
c ---[ 239]---> BDD-cost:   52
c ---[ 238]---> BDD-cost:    1
c ---[ 237]---> BDD-cost:   28
c ---[ 236]---> BDD-cost:    5
c ---[ 235]---> BDD-cost:   25
c ---[ 234]---> BDD-cost:   48
c ---[ 233]---> BDD-cost:   52
c ---[ 232]---> BDD-cost:   44
c ---[ 231]---> BDD-cost:   29
c ---[ 230]---> BDD-cost:   32
c ---[ 229]---> BDD-cost:   28
c ---[ 228]---> BDD-cost:   20
c ---[ 227]---> BDD-cost:   21
c ---[ 226]---> BDD-cost:   29
c ---[ 225]---> BDD-cost:   28
c ---[ 224]---> BDD-cost:   29
c ---[ 223]---> BDD-cost:   32
c ---[ 222]---> BDD-cost:   29
c ---[ 221]---> BDD-cost:   28
c ---[ 220]---> BDD-cost:   41
c ---[ 219]---> BDD-cost:   44
c ---[ 218]---> BDD-cost:   36
c ---[ 217]---> BDD-cost:   46
c ---[ 216]---> BDD-cost:   30
c ---[ 215]---> BDD-cost:   32
c ---[ 214]---> BDD-cost:   44
c ---[ 213]---> BDD-cost:   28
c ---[ 212]---> BDD-cost:   20
c ---[ 211]---> BDD-cost:   30
c ---[ 210]---> BDD-cost:   32
c ---[ 209]---> BDD-cost:   36
c ---[ 208]---> BDD-cost:   80
c ---[ 207]---> BDD-cost:   52
c ---[ 206]---> BDD-cost:    9
c ---[ 205]---> BDD-cost:   72
c ---[ 204]---> BDD-cost:   40
c ---[ 203]---> BDD-cost:   40
c ---[ 202]---> BDD-cost:   40
c ---[ 201]---> BDD-cost:   17
c ---[ 200]---> BDD-cost:   52
c ---[ 199]---> BDD-cost:    9
c ---[ 198]---> BDD-cost:   28
c ---[ 197]---> BDD-cost:   21
c ---[ 196]---> BDD-cost:   29
c ---[ 195]---> BDD-cost:   30
c ---[ 194]---> BDD-cost:   15
c ---[ 193]---> BDD-cost:   14
c ---[ 192]---> BDD-cost:   28
c ---[ 191]---> BDD-cost:   22
c ---[ 190]---> BDD-cost:   25
c ---[ 189]---> BDD-cost:    1
c ---[ 188]---> BDD-cost:    1
c ---[ 187]---> BDD-cost:    1
c ---[ 186]---> BDD-cost:    1
c ---[ 185]---> BDD-cost:    1
c ---[ 184]---> BDD-cost:    1
c ---[ 183]---> BDD-cost:    1
c ---[ 182]---> BDD-cost:    1
c ---[ 181]---> BDD-cost:    1
c ---[ 180]---> BDD-cost:    1
c ---[ 179]---> BDD-cost:    1
c ---[ 178]---> BDD-cost:    1
c ---[ 177]---> BDD-cost:    1
c ---[ 176]---> BDD-cost:    1
c ---[ 175]---> BDD-cost:    1
c ---[ 174]---> BDD-cost:    1
c ---[ 173]---> BDD-cost:    1
c ---[ 172]---> BDD-cost:    1
c ---[ 171]---> BDD-cost:    1
c ---[ 170]---> BDD-cost:    1
c ---[ 169]---> BDD-cost:    1
c ---[ 168]---> BDD-cost:    1
c ---[ 167]---> BDD-cost:    1
c ---[ 166]---> BDD-cost:   48
c ---[ 165]---> BDD-cost:    1
c ---[ 164]---> BDD-cost:    1
c ---[ 163]---> BDD-cost:    1
c ---[ 162]---> BDD-cost:    1
c ---[ 161]---> BDD-cost:    1
c ---[ 160]---> BDD-cost:    1
c ---[ 159]---> BDD-cost:    1
c ---[ 158]---> BDD-cost:    1
c ---[ 157]---> BDD-cost:   40
c ---[ 156]---> BDD-cost:    1
c ---[ 155]---> BDD-cost:    1
c ---[ 154]---> BDD-cost:    1
c ---[ 153]---> BDD-cost:    1
c ---[ 152]---> BDD-cost:    1
c ---[ 151]---> BDD-cost:    2
c ---[ 150]---> BDD-cost:    1
c ---[ 149]---> BDD-cost:   42
c ---[ 148]---> BDD-cost:   32
c ---[ 147]---> BDD-cost:    1
c ---[ 146]---> BDD-cost:   16
c ---[ 145]---> BDD-cost:    1
c ---[ 144]---> BDD-cost:   32
c ---[ 143]---> BDD-cost:    1
c ---[ 142]---> BDD-cost:    1
c ---[ 141]---> BDD-cost:    1
c ---[ 140]---> BDD-cost:    1
c ---[ 139]---> BDD-cost:    1
c ---[ 138]---> BDD-cost:    2
c ---[ 137]---> BDD-cost:    1
c ---[ 136]---> BDD-cost:    1
c ---[ 135]---> BDD-cost:    1
c ---[ 134]---> BDD-cost:   32
c ---[ 133]---> BDD-cost:   34
c ---[ 132]---> BDD-cost:   18
c ---[ 131]---> BDD-cost:   69
c ---[ 130]---> BDD-cost:   94
c ---[ 129]---> BDD-cost:  172
c ---[ 128]---> BDD-cost:    3
c ---[ 127]---> BDD-cost:  184
c ---[ 126]---> BDD-cost:  135
c ---[ 125]---> BDD-cost:  159
c ---[ 124]---> BDD-cost:    1
c ---[ 123]---> BDD-cost:   18
c ---[ 122]---> BDD-cost:  110
c ---[ 121]---> BDD-cost:  118
c ---[ 120]---> BDD-cost:    1
c ---[ 119]---> BDD-cost:    3
c ---[ 118]---> BDD-cost:  127
c ---[ 117]---> BDD-cost:   94
c ---[ 116]---> BDD-cost:    3
c ---[ 115]---> BDD-cost:    1
c ---[ 114]---> BDD-cost:   75
c ---[ 113]---> BDD-cost:  141
c ---[ 112]---> BDD-cost:    1
c ---[ 111]---> BDD-cost:    1
c ---[ 110]---> BDD-cost:   50
c ---[ 109]---> BDD-cost:    1
c ---[ 108]---> BDD-cost:    1
c ---[ 107]---> BDD-cost:   71
c ---[ 106]---> BDD-cost:    1
c ---[ 105]---> BDD-cost:    1
c ---[ 104]---> BDD-cost:  126
c ---[ 103]---> BDD-cost:    1
c ---[ 102]---> BDD-cost:    1
c ---[ 101]---> BDD-cost:    1
c ---[ 100]---> BDD-cost:    1
c ---[  99]---> BDD-cost:   62
c ---[  98]---> BDD-cost:    1
c ---[  97]---> BDD-cost:    1
c ---[  96]---> BDD-cost:    1
c ---[  95]---> BDD-cost:    1
c ---[  94]---> BDD-cost:   35
c ---[  93]---> BDD-cost:  115
c ---[  92]---> BDD-cost:    1
c ---[  91]---> BDD-cost:    2
c ---[  90]---> BDD-cost:    1
c ---[  89]---> BDD-cost:    1
c ---[  88]---> BDD-cost:   36
c ---[  87]---> BDD-cost:   20
c ---[  86]---> BDD-cost:    1
c ---[  85]---> BDD-cost:   20
c ---[  84]---> BDD-cost:    1
c ---[  83]---> BDD-cost:    1
c ---[  82]---> BDD-cost:   16
c ---[  81]---> BDD-cost:    1
c ---[  80]---> BDD-cost:   27
c ---[  79]---> BDD-cost:    1
c ---[  78]---> BDD-cost:   16
c ---[  77]---> BDD-cost:    1
c ---[  76]---> BDD-cost:    1
c ---[  75]---> BDD-cost:   27
c ---[  74]---> BDD-cost:    1
c ---[  73]---> BDD-cost:    1
c ---[  72]---> BDD-cost:    1
c ---[  71]---> BDD-cost:   26
c ---[  70]---> BDD-cost:    1
c ---[  69]---> BDD-cost:    1
c ---[  68]---> BDD-cost:    1
c ---[  67]---> BDD-cost:   84
c ---[  66]---> BDD-cost:    1
c ---[  65]---> BDD-cost:   28
c ---[  64]---> BDD-cost:   38
c ---[  63]---> BDD-cost:  169
c ---[  62]---> BDD-cost:    1
c ---[  61]---> BDD-cost:    1
c ---[  60]---> BDD-cost:    1
c ---[  59]---> BDD-cost:    1
c ---[  58]---> BDD-cost:   60
c ---[  57]---> BDD-cost:    1
c ---[  56]---> BDD-cost:    1
c ---[  55]---> BDD-cost:   62
c ---[  54]---> BDD-cost:    2
c ---[  53]---> BDD-cost:    1
c ---[  52]---> BDD-cost:    1
c ---[  51]---> BDD-cost:    2
c ---[  50]---> BDD-cost:    1
c ---[  49]---> BDD-cost:    1
c ---[  48]---> BDD-cost:  161
c ---[  47]---> BDD-cost:    2
c ---[  46]---> BDD-cost:    1
c ---[  45]---> BDD-cost:   42
c ---[  44]---> BDD-cost:    1
c ---[  43]---> BDD-cost:    1
c ---[  42]---> BDD-cost:    2
c ---[  41]---> BDD-cost:    1
c ---[  40]---> BDD-cost:    1
c ---[  39]---> BDD-cost:    2
c ---[  38]---> BDD-cost:    2
c ---[  37]---> BDD-cost:   49
c ---[  36]---> BDD-cost:   77
c ---[  35]---> BDD-cost:    2
c ---[  34]---> BDD-cost:   40
c ---[  33]---> BDD-cost:    1
c ---[  32]---> BDD-cost:    1
c ---[  31]---> BDD-cost:   58
c ---[  30]---> BDD-cost:   13
c ---[  29]---> BDD-cost:    1
c ---[  28]---> BDD-cost:    1
c ---[  27]---> BDD-cost:    1
c ---[  26]---> BDD-cost:    1
c ---[  25]---> BDD-cost:   17
c ---[  24]---> BDD-cost:    1
c ---[  23]---> BDD-cost:    1
c ---[  22]---> BDD-cost:    1
c ---[  21]---> BDD-cost:    1
c ---[  20]---> BDD-cost:   16
c ---[  19]---> BDD-cost:    1
c ---[  18]---> BDD-cost:    1
c ---[  17]---> BDD-cost:   22
c ---[  16]---> BDD-cost:   10
c ---[  15]---> BDD-cost:   11
c ---[  14]---> BDD-cost:   12
c ---[  13]---> BDD-cost:   10
c ---[  12]---> BDD-cost:   11
c ---[  11]---> BDD-cost:   12
c ---[  10]---> BDD-cost:    6
c ---[   9]---> BDD-cost:   11
c ---[   8]---> BDD-cost:   11
c ---[   7]---> BDD-cost:    7
c ---[   6]---> BDD-cost:    5
c ---[   5]---> BDD-cost:    7
c ---[   4]---> BDD-cost:    5
c ---[   3]---> BDD-cost:    7
c ---[   2]---> BDD-cost:    5
c ---[   1]---> BDD-cost:    2
c ---[   0]---> BDD-cost:    6
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  296752   925023 |   98917       0        0     nan |  0.000 % |
c |       100 |  296580   924636 |  108808      98     1026    10.5 | 13.089 % |
c |       250 |  296542   924553 |  119689     244     2223     9.1 | 13.101 % |
c |       475 |  296272   923943 |  131658     464     4403     9.5 | 13.187 % |
c |       814 |  295430   922023 |  144824     783     7272     9.3 | 13.446 % |
c |      1322 |  295104   921215 |  159306    1274    11994     9.4 | 13.537 % |
c |      2082 |  289888   909184 |  175237    1936    19209     9.9 | 15.283 % |
c |      3221 |  289468   908046 |  192761    3055    30146     9.9 | 15.392 % |
c |      4929 |  288931   906701 |  212037    4704    49270    10.5 | 15.558 % |
c |      7491 |  285525   898830 |  233241    7120    72373    10.2 | 16.684 % |
c |     11335 |  283759   894575 |  256565   10840   151267    14.0 | 17.263 % |
c |     17101 |  282582   891489 |  282221   16488   264265    16.0 | 17.595 % |
c |     25750 |  281686   889057 |  310443   24967   462702    18.5 | 17.839 % |
c |     38724 |  280326   885456 |  341488   37808   841207    22.2 | 18.202 % |
c |     58186 |  279419   882963 |  375637   57179  1427826    25.0 | 18.428 % |
c |     87378 |  277695   877540 |  413200   85781  2393416    27.9 | 18.655 % |
c |    131168 |  274590   868954 |  454520  128673  4031962    31.3 | 19.371 % |
c |    196854 |  273650   865999 |  499973  194049  7306135    37.7 | 19.531 % |
/oldhome/oroussel/solvers/minisat+_script: line 9: 25703 CPU time limit exceeded $XDIR/minisat+_64-bit_static -try "$@"
#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.84 0.95 0.91 2/54 25699
Raw data (stat): 25699 (runsolver) R 25698 3944 3943 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 784931834 1052672 99 4294967295 134512640 135381576 3221224480 3221219688 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0012 s]
Raw data (loadavg): 0.87 0.95 0.91 2/55 25703
Raw data (stat): 25699 (minisat+_script) S 25698 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784931834 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+20.0025 s]
Raw data (loadavg): 0.89 0.95 0.91 2/55 25703
Raw data (stat): 25699 (minisat+_script) S 25698 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784931834 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+30.0033 s]
Raw data (loadavg): 0.90 0.95 0.91 2/55 25703
Raw data (stat): 25699 (minisat+_script) S 25698 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784931834 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+40.0036 s]
Raw data (loadavg): 0.92 0.96 0.91 2/55 25703
Raw data (stat): 25699 (minisat+_script) S 25698 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784931834 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+50.0039 s]
Raw data (loadavg): 0.93 0.96 0.91 2/55 25703
Raw data (stat): 25699 (minisat+_script) S 25698 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784931834 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+60.0038 s]
Raw data (loadavg): 0.94 0.96 0.91 2/55 25703
Raw data (stat): 25699 (minisat+_script) S 25698 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784931834 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+70.0054 s]
Raw data (loadavg): 0.95 0.96 0.91 2/55 25703
Raw data (stat): 25699 (minisat+_script) S 25698 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784931834 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+80.0064 s]
Raw data (loadavg): 0.96 0.96 0.91 2/55 25703
Raw data (stat): 25699 (minisat+_script) S 25698 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784931834 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+90.0062 s]
Raw data (loadavg): 0.96 0.96 0.91 2/55 25703
Raw data (stat): 25699 (minisat+_script) S 25698 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784931834 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+100.008 s]
Raw data (loadavg): 0.97 0.96 0.91 2/55 25703
Raw data (stat): 25699 (minisat+_script) S 25698 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784931834 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+110.008 s]
Raw data (loadavg): 0.97 0.96 0.91 2/55 25703
Raw data (stat): 25699 (minisat+_script) S 25698 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784931834 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+120.009 s]
Raw data (loadavg): 0.98 0.96 0.91 2/55 25703
Raw data (stat): 25699 (minisat+_script) S 25698 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784931834 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+130.009 s]
Raw data (loadavg): 0.98 0.96 0.91 2/55 25703
Raw data (stat): 25699 (minisat+_script) S 25698 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784931834 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+140.009 s]
Raw data (loadavg): 0.98 0.97 0.91 2/55 25703
Raw data (stat): 25699 (minisat+_script) S 25698 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784931834 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+150.01 s]
Raw data (loadavg): 0.98 0.97 0.91 2/55 25703
Raw data (stat): 25699 (minisat+_script) S 25698 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784931834 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+160.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25703
Raw data (stat): 25699 (minisat+_script) S 25698 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784931834 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+170.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25703
Raw data (stat): 25699 (minisat+_script) S 25698 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784931834 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+180.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25703
Raw data (stat): 25699 (minisat+_script) S 25698 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784931834 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+190.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25703
Raw data (stat): 25699 (minisat+_script) S 25698 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784931834 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+200.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25703
Raw data (stat): 25699 (minisat+_script) S 25698 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784931834 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+210.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25703
Raw data (stat): 25699 (minisat+_script) S 25698 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784931834 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+220.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25703
Raw data (stat): 25699 (minisat+_script) S 25698 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784931834 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+230.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25703
Raw data (stat): 25699 (minisat+_script) S 25698 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784931834 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+240.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25703
Raw data (stat): 25699 (minisat+_script) S 25698 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784931834 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+250.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25703
Raw data (stat): 25699 (minisat+_script) S 25698 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784931834 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+260.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25703
Raw data (stat): 25699 (minisat+_script) S 25698 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784931834 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+270.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25703
Raw data (stat): 25699 (minisat+_script) S 25698 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784931834 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+280.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25703
Raw data (stat): 25699 (minisat+_script) S 25698 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784931834 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+290.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25703
Raw data (stat): 25699 (minisat+_script) S 25698 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784931834 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+300.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25703
Raw data (stat): 25699 (minisat+_script) S 25698 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784931834 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+310.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25703
Raw data (stat): 25699 (minisat+_script) S 25698 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784931834 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+320.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25703
Raw data (stat): 25699 (minisat+_script) S 25698 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784931834 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+330.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25703
Raw data (stat): 25699 (minisat+_script) S 25698 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784931834 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+340.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25703
Raw data (stat): 25699 (minisat+_script) S 25698 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784931834 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+350.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25703
Raw data (stat): 25699 (minisat+_script) S 25698 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784931834 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+360.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25703
Raw data (stat): 25699 (minisat+_script) S 25698 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784931834 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+370.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25703
Raw data (stat): 25699 (minisat+_script) S 25698 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784931834 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+380.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25703
Raw data (stat): 25699 (minisat+_script) S 25698 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784931834 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+390.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25703
Raw data (stat): 25699 (minisat+_script) S 25698 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784931834 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+400.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25703
Raw data (stat): 25699 (minisat+_script) S 25698 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784931834 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+410.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25703
Raw data (stat): 25699 (minisat+_script) S 25698 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784931834 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+420.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25703
Raw data (stat): 25699 (minisat+_script) S 25698 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784931834 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+430.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25703
Raw data (stat): 25699 (minisat+_script) S 25698 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784931834 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+440.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25703
Raw data (stat): 25699 (minisat+_script) S 25698 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784931834 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+450.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25703
Raw data (stat): 25699 (minisat+_script) S 25698 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784931834 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+460.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25703
Raw data (stat): 25699 (minisat+_script) S 25698 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784931834 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+470.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25703
Raw data (stat): 25699 (minisat+_script) S 25698 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784931834 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+480.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25703
Raw data (stat): 25699 (minisat+_script) S 25698 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784931834 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+490.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25703
Raw data (stat): 25699 (minisat+_script) S 25698 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784931834 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+500.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25703
Raw data (stat): 25699 (minisat+_script) S 25698 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784931834 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+510.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25703
Raw data (stat): 25699 (minisat+_script) S 25698 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784931834 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+520.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25703
Raw data (stat): 25699 (minisat+_script) S 25698 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784931834 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+530.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25703
Raw data (stat): 25699 (minisat+_script) S 25698 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784931834 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+540.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25703
Raw data (stat): 25699 (minisat+_script) S 25698 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784931834 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+550.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25703
Raw data (stat): 25699 (minisat+_script) S 25698 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784931834 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+560.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25703
Raw data (stat): 25699 (minisat+_script) S 25698 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784931834 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+570.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25703
Raw data (stat): 25699 (minisat+_script) S 25698 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784931834 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+580.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25703
Raw data (stat): 25699 (minisat+_script) S 25698 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784931834 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+590.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25703
Raw data (stat): 25699 (minisat+_script) S 25698 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784931834 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+600.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25703
Raw data (stat): 25699 (minisat+_script) S 25698 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784931834 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+610.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25703
Raw data (stat): 25699 (minisat+_script) S 25698 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784931834 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+620.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25703
Raw data (stat): 25699 (minisat+_script) S 25698 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784931834 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+630.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25703
Raw data (stat): 25699 (minisat+_script) S 25698 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784931834 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+640.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25703
Raw data (stat): 25699 (minisat+_script) S 25698 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784931834 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+650.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25703
Raw data (stat): 25699 (minisat+_script) S 25698 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784931834 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+660.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25703
Raw data (stat): 25699 (minisat+_script) S 25698 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784931834 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+670.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25703
Raw data (stat): 25699 (minisat+_script) S 25698 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784931834 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+680.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25703
Raw data (stat): 25699 (minisat+_script) S 25698 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784931834 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+690.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25703
Raw data (stat): 25699 (minisat+_script) S 25698 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784931834 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+700.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25703
Raw data (stat): 25699 (minisat+_script) S 25698 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784931834 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+710.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25703
Raw data (stat): 25699 (minisat+_script) S 25698 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784931834 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+720.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25703
Raw data (stat): 25699 (minisat+_script) S 25698 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784931834 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+730.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25703
Raw data (stat): 25699 (minisat+_script) S 25698 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784931834 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+740.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25703
Raw data (stat): 25699 (minisat+_script) S 25698 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784931834 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+750.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25703
Raw data (stat): 25699 (minisat+_script) S 25698 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784931834 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+760.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25703
Raw data (stat): 25699 (minisat+_script) S 25698 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784931834 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+770.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25703
Raw data (stat): 25699 (minisat+_script) S 25698 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784931834 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+780.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25703
Raw data (stat): 25699 (minisat+_script) S 25698 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784931834 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+790.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25703
Raw data (stat): 25699 (minisat+_script) S 25698 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784931834 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+800.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25703
Raw data (stat): 25699 (minisat+_script) S 25698 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784931834 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+810.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25703
Raw data (stat): 25699 (minisat+_script) S 25698 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784931834 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+820.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25703
Raw data (stat): 25699 (minisat+_script) S 25698 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784931834 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+830.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25703
Raw data (stat): 25699 (minisat+_script) S 25698 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784931834 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+840.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25703
Raw data (stat): 25699 (minisat+_script) S 25698 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784931834 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+850.051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25703
Raw data (stat): 25699 (minisat+_script) S 25698 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784931834 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+860.051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25703
Raw data (stat): 25699 (minisat+_script) S 25698 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784931834 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+870.052 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25703
Raw data (stat): 25699 (minisat+_script) S 25698 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784931834 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+880.053 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25703
Raw data (stat): 25699 (minisat+_script) S 25698 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784931834 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+890.053 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25703
Raw data (stat): 25699 (minisat+_script) S 25698 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784931834 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+900.053 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25703
Raw data (stat): 25699 (minisat+_script) S 25698 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784931834 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+910.053 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25703
Raw data (stat): 25699 (minisat+_script) S 25698 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784931834 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+920.053 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25703
Raw data (stat): 25699 (minisat+_script) S 25698 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784931834 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+930.054 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25703
Raw data (stat): 25699 (minisat+_script) S 25698 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784931834 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+940.053 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25703
Raw data (stat): 25699 (minisat+_script) S 25698 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784931834 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+950.053 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25703
Raw data (stat): 25699 (minisat+_script) S 25698 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784931834 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+960.053 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25703
Raw data (stat): 25699 (minisat+_script) S 25698 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784931834 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+970.054 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25703
Raw data (stat): 25699 (minisat+_script) S 25698 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784931834 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+980.055 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25703
Raw data (stat): 25699 (minisat+_script) S 25698 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784931834 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+990.055 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25703
Raw data (stat): 25699 (minisat+_script) S 25698 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784931834 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1000.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25703
Raw data (stat): 25699 (minisat+_script) S 25698 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784931834 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1010.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25703
Raw data (stat): 25699 (minisat+_script) S 25698 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784931834 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1020.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25703
Raw data (stat): 25699 (minisat+_script) S 25698 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784931834 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1030.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25703
Raw data (stat): 25699 (minisat+_script) S 25698 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784931834 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1040.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25703
Raw data (stat): 25699 (minisat+_script) S 25698 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784931834 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1050.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25703
Raw data (stat): 25699 (minisat+_script) S 25698 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784931834 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1060.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25703
Raw data (stat): 25699 (minisat+_script) S 25698 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784931834 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1070.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25703
Raw data (stat): 25699 (minisat+_script) S 25698 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784931834 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1080.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25703
Raw data (stat): 25699 (minisat+_script) S 25698 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784931834 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1090.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25703
Raw data (stat): 25699 (minisat+_script) S 25698 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784931834 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1100.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25703
Raw data (stat): 25699 (minisat+_script) S 25698 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784931834 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1110.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25703
Raw data (stat): 25699 (minisat+_script) S 25698 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784931834 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1120.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25703
Raw data (stat): 25699 (minisat+_script) S 25698 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784931834 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1130.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25703
Raw data (stat): 25699 (minisat+_script) S 25698 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784931834 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1140.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25703
Raw data (stat): 25699 (minisat+_script) S 25698 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784931834 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1150.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25703
Raw data (stat): 25699 (minisat+_script) S 25698 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784931834 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1160.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25703
Raw data (stat): 25699 (minisat+_script) S 25698 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784931834 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1170.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25703
Raw data (stat): 25699 (minisat+_script) S 25698 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784931834 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1180.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25703
Raw data (stat): 25699 (minisat+_script) S 25698 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784931834 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1190.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25703
Raw data (stat): 25699 (minisat+_script) S 25698 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784931834 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1200.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25703
Raw data (stat): 25699 (minisat+_script) S 25698 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784931834 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1210.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25703
Raw data (stat): 25699 (minisat+_script) S 25698 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784931834 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1220.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25703
Raw data (stat): 25699 (minisat+_script) S 25698 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784931834 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1229.77 s]
Raw data (loadavg): 0.99 0.97 0.91 1/53 25703
Raw data (stat): 25699 (minisat+_script) S 25698 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784931834 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 0

Child status: 152
Real time (s): 1229.77
CPU time (s): 1229.88
CPU user time (s): 1228.9
CPU system time (s): 0.979851
CPU usage (%): 100.009
Max. virtual memory (Kb): 2124
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####