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-dg012142.opb
MD5SUM	d2a2dc4ff7a501b7efb12f8e274e186d
Bench Category	optimization, big integers (OPTBIGINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	2147483647
Optimality of the best value was proved	NO
Number of terms in the objective function	16640
Biggest coefficient in the objective function	5242880000
Number of bits for the biggest coefficient in the objective function	33
Sum of the numbers in the objective function	1683190350400
Number of bits of the sum of numbers in the objective function	41
Biggest number in a constraint	5242880000
Number of bits of the biggest number in a constraint	33
Biggest sum of numbers in a constraint	1683190350400
Number of bits of the biggest sum of numbers	41
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1269.98
Number of variables	29440
Total number of constraints	6310
Number of constraints which are clauses	40
Number of constraints which are cardinality constraints (but not clauses)	0
Number of constraints which are nor clauses,nor cardinality constraints	6270
Minimum length of a constraint	1
Maximum length of a constraint	251
Trace number 13939

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc11 THE 2005-04-20 22:16:43 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=20110 boxname=wulflinc11 idbench=1547 idsolver=12 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  d2a2dc4ff7a501b7efb12f8e274e186d  /oldhome/oroussel/tmp/wulflinc11/normalized-mps-v2-13-7-dg012142.opb
REAL COMMAND:  minisat+ -cb -gs /oldhome/oroussel/tmp/wulflinc11/normalized-mps-v2-13-7-dg012142.opb /oldhome/oroussel/tmp/wulflinc11/normalized-mps-v2-13-7-dg012142.opb
IDLAUNCH: 20110
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.028
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.028
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:        969748 kB
Buffers:           252 kB
Cached:          43472 kB
SwapCached:          0 kB
Active:          25792 kB
Inactive:        20700 kB
HighTotal:      131008 kB
HighFree:        84252 kB
LowTotal:       903652 kB
LowFree:        885496 kB
SwapTotal:     2097136 kB
SwapFree:      2097048 kB
Dirty:              40 kB
Writeback:           0 kB
Mapped:           6816 kB
Slab:            12772 kB
Committed_AS:    63488 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-20 22:36:46 (client local time) WITH STATUS 0 IN 1200.59 SECONDS
stats: 20110 7 1200.59 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 2731 PB-constraints to clauses...
c   -- Unit propagations: ppppppppppppppppppppppppppppppppppppppppppppppppppp
c   -- Detecting intervals from adjacent constraints: ################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################
c   -- Clauses(.)/Splits(s): sssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssss
c ---[2771]---> BDD-cost:  393
c ---[2768]---> BDD-cost:  590
c ---[2766]---> BDD-cost:  601
c ---[2758]---> BDD-cost:  647
c ---[2744]---> BDD-cost:  714
c ---[2742]---> BDD-cost:  714
c ---[2740]---> BDD-cost: 1305
c ---[2738]---> BDD-cost: 1305
c ---[2736]---> BDD-cost:  163
c ---[2734]---> BDD-cost:  163
c ---[2732]---> BDD-cost:  163
c ---[2730]---> BDD-cost:  163
c ---[2728]---> BDD-cost:  163
c ---[2726]---> BDD-cost:  163
c ---[2724]---> BDD-cost:  163
c ---[2722]---> BDD-cost:  163
c ---[2720]---> BDD-cost:  163
c ---[2718]---> BDD-cost:  163
c ---[2716]---> BDD-cost:  329
c ---[2714]---> BDD-cost:  163
c ---[2712]---> BDD-cost:  163
c ---[2710]---> BDD-cost:  163
c ---[2708]---> BDD-cost:  329
c ---[2706]---> BDD-cost:  163
c ---[2704]---> BDD-cost:  163
c ---[2702]---> BDD-cost:  163
c ---[2700]---> BDD-cost:  163
c ---[2698]---> BDD-cost:  163
c ---[2696]---> BDD-cost:  331
c ---[2694]---> BDD-cost:  163
c ---[2692]---> BDD-cost:  329
c ---[2690]---> BDD-cost:  163
c ---[2688]---> BDD-cost:  172
c ---[2686]---> BDD-cost:  163
c ---[2684]---> BDD-cost:  163
c ---[2682]---> BDD-cost:  163
c ---[2680]---> BDD-cost:  163
c ---[2678]---> BDD-cost:  163
c ---[2676]---> BDD-cost: 1022
c ---[2674]---> BDD-cost: 1028
c ---[2672]---> BDD-cost: 1028
c ---[2670]---> BDD-cost: 1000
c ---[2668]---> BDD-cost: 1000
c ---[2666]---> BDD-cost: 1000
c ---[2664]---> BDD-cost:  980
c ---[2662]---> BDD-cost:  954
c ---[2660]---> BDD-cost:  944
c ---[2658]---> BDD-cost:  924
c ---[2656]---> BDD-cost:  900
c ---[2654]---> BDD-cost:  888
c ---[2652]---> BDD-cost:  850
c ---[2650]---> BDD-cost:  832
c ---[2648]---> BDD-cost:  756
c ---[2646]---> BDD-cost: 1022
c ---[2644]---> BDD-cost: 1028
c ---[2642]---> BDD-cost: 1028
c ---[2640]---> BDD-cost: 1000
c ---[2638]---> BDD-cost: 1000
c ---[2636]---> BDD-cost: 1000
c ---[2634]---> BDD-cost:  980
c ---[2632]---> BDD-cost:  954
c ---[2630]---> BDD-cost:  944
c ---[2628]---> BDD-cost:  924
c ---[2626]---> BDD-cost:  900
c ---[2624]---> BDD-cost:  888
c ---[2622]---> BDD-cost:  850
c ---[2620]---> BDD-cost:  832
c ---[2618]---> BDD-cost:  756
c ---[2616]---> BDD-cost: 1712
c ---[2614]---> BDD-cost: 1718
c ---[2612]---> BDD-cost: 1718
c ---[2610]---> BDD-cost: 1690
c ---[2608]---> BDD-cost: 1668
c ---[2606]---> BDD-cost: 1668
c ---[2604]---> BDD-cost: 1648
c ---[2602]---> BDD-cost: 1601
c ---[2600]---> BDD-cost: 1589
c ---[2598]---> BDD-cost: 1547
c ---[2596]---> BDD-cost: 1504
c ---[2594]---> BDD-cost: 1460
c ---[2592]---> BDD-cost: 1403
c ---[2590]---> BDD-cost: 1345
c ---[2588]---> BDD-cost: 1227
c ---[2586]---> BDD-cost: 1712
c ---[2584]---> BDD-cost: 1718
c ---[2582]---> BDD-cost: 1718
c ---[2580]---> BDD-cost: 1690
c ---[2578]---> BDD-cost: 1668
c ---[2576]---> BDD-cost: 1668
c ---[2574]---> BDD-cost: 1648
c ---[2572]---> BDD-cost: 1601
c ---[2570]---> BDD-cost: 1589
c ---[2568]---> BDD-cost: 1547
c ---[2566]---> BDD-cost: 1504
c ---[2564]---> BDD-cost: 1460
c ---[2562]---> BDD-cost: 1403
c ---[2560]---> BDD-cost: 1345
c ---[2558]---> BDD-cost: 1227
c ---[2556]---> BDD-cost:  331
c ---[2554]---> BDD-cost:  337
c ---[2552]---> BDD-cost:  337
c ---[2550]---> BDD-cost:  326
c ---[2548]---> BDD-cost:  326
c ---[2546]---> BDD-cost:  326
c ---[2544]---> BDD-cost:  326
c ---[2542]---> BDD-cost:  315
c ---[2540]---> BDD-cost:  315
c ---[2538]---> BDD-cost:  315
c ---[2536]---> BDD-cost:  304
c ---[2534]---> BDD-cost:  304
c ---[2532]---> BDD-cost:  304
c ---[2530]---> BDD-cost:  293
c ---[2528]---> BDD-cost:  282
c ---[2526]---> BDD-cost:  331
c ---[2524]---> BDD-cost:  337
c ---[2522]---> BDD-cost:  337
c ---[2520]---> BDD-cost:  326
c ---[2518]---> BDD-cost:  326
c ---[2516]---> BDD-cost:  326
c ---[2514]---> BDD-cost:  326
c ---[2512]---> BDD-cost:  315
c ---[2510]---> BDD-cost:  315
c ---[2508]---> BDD-cost:  315
c ---[2506]---> BDD-cost:  304
c ---[2504]---> BDD-cost:  304
c ---[2502]---> BDD-cost:  304
c ---[2500]---> BDD-cost:  293
c ---[2498]---> BDD-cost:  282
c ---[2496]---> BDD-cost:  331
c ---[2494]---> BDD-cost:  337
c ---[2492]---> BDD-cost:  337
c ---[2490]---> BDD-cost:  326
c ---[2488]---> BDD-cost:  326
c ---[2486]---> BDD-cost:  326
c ---[2484]---> BDD-cost:  326
c ---[2482]---> BDD-cost:  315
c ---[2480]---> BDD-cost:  315
c ---[2478]---> BDD-cost:  315
c ---[2476]---> BDD-cost:  304
c ---[2474]---> BDD-cost:  304
c ---[2472]---> BDD-cost:  304
c ---[2470]---> BDD-cost:  293
c ---[2468]---> BDD-cost:  282
c ---[2466]---> BDD-cost:  331
c ---[2464]---> BDD-cost:  337
c ---[2462]---> BDD-cost:  337
c ---[2460]---> BDD-cost:  326
c ---[2458]---> BDD-cost:  326
c ---[2456]---> BDD-cost:  326
c ---[2454]---> BDD-cost:  326
c ---[2452]---> BDD-cost:  315
c ---[2450]---> BDD-cost:  315
c ---[2448]---> BDD-cost:  315
c ---[2446]---> BDD-cost:  304
c ---[2444]---> BDD-cost:  304
c ---[2442]---> BDD-cost:  304
c ---[2440]---> BDD-cost:  293
c ---[2438]---> BDD-cost:  282
c ---[2436]---> BDD-cost:  331
c ---[2434]---> BDD-cost:  337
c ---[2432]---> BDD-cost:  337
c ---[2430]---> BDD-cost:  337
c ---[2428]---> BDD-cost:  337
c ---[2426]---> BDD-cost:  337
c ---[2424]---> BDD-cost:  326
c ---[2422]---> BDD-cost:  326
c ---[2420]---> BDD-cost:  326
c ---[2418]---> BDD-cost:  315
c ---[2416]---> BDD-cost:  315
c ---[2414]---> BDD-cost:  304
c ---[2412]---> BDD-cost:  304
c ---[2410]---> BDD-cost:  293
c ---[2408]---> BDD-cost:  282
c ---[2406]---> BDD-cost:  331
c ---[2404]---> BDD-cost:  337
c ---[2402]---> BDD-cost:  337
c ---[2400]---> BDD-cost:  337
c ---[2398]---> BDD-cost:  337
c ---[2396]---> BDD-cost:  337
c ---[2394]---> BDD-cost:  326
c ---[2392]---> BDD-cost:  326
c ---[2390]---> BDD-cost:  326
c ---[2388]---> BDD-cost:  315
c ---[2386]---> BDD-cost:  315
c ---[2384]---> BDD-cost:  304
c ---[2382]---> BDD-cost:  304
c ---[2380]---> BDD-cost:  293
c ---[2378]---> BDD-cost:  282
c ---[2376]---> BDD-cost:  331
c ---[2374]---> BDD-cost:  337
c ---[2372]---> BDD-cost:  337
c ---[2370]---> BDD-cost:  337
c ---[2368]---> BDD-cost:  337
c ---[2366]---> BDD-cost:  337
c ---[2364]---> BDD-cost:  326
c ---[2362]---> BDD-cost:  326
c ---[2360]---> BDD-cost:  326
c ---[2358]---> BDD-cost:  315
c ---[2356]---> BDD-cost:  315
c ---[2354]---> BDD-cost:  304
c ---[2352]---> BDD-cost:  304
c ---[2350]---> BDD-cost:  293
c ---[2348]---> BDD-cost:  282
c ---[2346]---> BDD-cost:  331
c ---[2344]---> BDD-cost:  337
c ---[2342]---> BDD-cost:  337
c ---[2340]---> BDD-cost:  337
c ---[2338]---> BDD-cost:  337
c ---[2336]---> BDD-cost:  337
c ---[2334]---> BDD-cost:  326
c ---[2332]---> BDD-cost:  326
c ---[2330]---> BDD-cost:  326
c ---[2328]---> BDD-cost:  315
c ---[2326]---> BDD-cost:  315
c ---[2324]---> BDD-cost:  304
c ---[2322]---> BDD-cost:  304
c ---[2320]---> BDD-cost:  293
c ---[2318]---> BDD-cost:  282
c ---[2316]---> BDD-cost:  331
c ---[2314]---> BDD-cost:  337
c ---[2312]---> BDD-cost:  337
c ---[2310]---> BDD-cost:  337
c ---[2308]---> BDD-cost:  337
c ---[2306]---> BDD-cost:  337
c ---[2304]---> BDD-cost:  326
c ---[2302]---> BDD-cost:  326
c ---[2300]---> BDD-cost:  326
c ---[2298]---> BDD-cost:  315
c ---[2296]---> BDD-cost:  315
c ---[2294]---> BDD-cost:  304
c ---[2292]---> BDD-cost:  304
c ---[2290]---> BDD-cost:  293
c ---[2288]---> BDD-cost:  282
c ---[2286]---> BDD-cost:  331
c ---[2284]---> BDD-cost:  337
c ---[2282]---> BDD-cost:  337
c ---[2280]---> BDD-cost:  326
c ---[2278]---> BDD-cost:  326
c ---[2276]---> BDD-cost:  326
c ---[2274]---> BDD-cost:  326
c ---[2272]---> BDD-cost:  315
c ---[2270]---> BDD-cost:  315
c ---[2268]---> BDD-cost:  315
c ---[2266]---> BDD-cost:  304
c ---[2264]---> BDD-cost:  304
c ---[2262]---> BDD-cost:  304
c ---[2260]---> BDD-cost:  293
c ---[2258]---> BDD-cost:  282
c ---[2256]---> BDD-cost:  557
c ---[2254]---> BDD-cost:  557
c ---[2252]---> BDD-cost:  557
c ---[2250]---> BDD-cost:  538
c ---[2248]---> BDD-cost:  538
c ---[2246]---> BDD-cost:  538
c ---[2244]---> BDD-cost:  538
c ---[2242]---> BDD-cost:  515
c ---[2240]---> BDD-cost:  515
c ---[2238]---> BDD-cost:  515
c ---[2236]---> BDD-cost:  492
c ---[2234]---> BDD-cost:  492
c ---[2232]---> BDD-cost:  492
c ---[2230]---> BDD-cost:  469
c ---[2228]---> BDD-cost:  446
c ---[2226]---> BDD-cost:  331
c ---[2224]---> BDD-cost:  337
c ---[2222]---> BDD-cost:  337
c ---[2220]---> BDD-cost:  326
c ---[2218]---> BDD-cost:  326
c ---[2216]---> BDD-cost:  326
c ---[2214]---> BDD-cost:  326
c ---[2212]---> BDD-cost:  315
c ---[2210]---> BDD-cost:  315
c ---[2208]---> BDD-cost:  315
c ---[2206]---> BDD-cost:  304
c ---[2204]---> BDD-cost:  304
c ---[2202]---> BDD-cost:  304
c ---[2200]---> BDD-cost:  293
c ---[2198]---> BDD-cost:  282
c ---[2196]---> BDD-cost:  331
c ---[2194]---> BDD-cost:  337
c ---[2192]---> BDD-cost:  337
c ---[2190]---> BDD-cost:  326
c ---[2188]---> BDD-cost:  326
c ---[2186]---> BDD-cost:  326
c ---[2184]---> BDD-cost:  326
c ---[2182]---> BDD-cost:  315
c ---[2180]---> BDD-cost:  315
c ---[2178]---> BDD-cost:  315
c ---[2176]---> BDD-cost:  304
c ---[2174]---> BDD-cost:  304
c ---[2172]---> BDD-cost:  304
c ---[2170]---> BDD-cost:  293
c ---[2168]---> BDD-cost:  282
c ---[2166]---> BDD-cost:  331
c ---[2164]---> BDD-cost:  337
c ---[2162]---> BDD-cost:  337
c ---[2160]---> BDD-cost:  326
c ---[2158]---> BDD-cost:  326
c ---[2156]---> BDD-cost:  326
c ---[2154]---> BDD-cost:  326
c ---[2152]---> BDD-cost:  315
c ---[2150]---> BDD-cost:  315
c ---[2148]---> BDD-cost:  315
c ---[2146]---> BDD-cost:  304
c ---[2144]---> BDD-cost:  304
c ---[2142]---> BDD-cost:  304
c ---[2140]---> BDD-cost:  293
c ---[2138]---> BDD-cost:  282
c ---[2136]---> BDD-cost:  557
c ---[2134]---> BDD-cost:  557
c ---[2132]---> BDD-cost:  557
c ---[2130]---> BDD-cost:  557
c ---[2128]---> BDD-cost:  557
c ---[2126]---> BDD-cost:  557
c ---[2124]---> BDD-cost:  538
c ---[2122]---> BDD-cost:  538
c ---[2120]---> BDD-cost:  538
c ---[2118]---> BDD-cost:  515
c ---[2116]---> BDD-cost:  515
c ---[2114]---> BDD-cost:  492
c ---[2112]---> BDD-cost:  492
c ---[2110]---> BDD-cost:  469
c ---[2108]---> BDD-cost:  446
c ---[2106]---> BDD-cost:  331
c ---[2104]---> BDD-cost:  337
c ---[2102]---> BDD-cost:  337
c ---[2100]---> BDD-cost:  337
c ---[2098]---> BDD-cost:  337
c ---[2096]---> BDD-cost:  337
c ---[2094]---> BDD-cost:  326
c ---[2092]---> BDD-cost:  326
c ---[2090]---> BDD-cost:  326
c ---[2088]---> BDD-cost:  315
c ---[2086]---> BDD-cost:  315
c ---[2084]---> BDD-cost:  304
c ---[2082]---> BDD-cost:  304
c ---[2080]---> BDD-cost:  293
c ---[2078]---> BDD-cost:  282
c ---[2076]---> BDD-cost:  331
c ---[2074]---> BDD-cost:  337
c ---[2072]---> BDD-cost:  337
c ---[2070]---> BDD-cost:  337
c ---[2068]---> BDD-cost:  337
c ---[2066]---> BDD-cost:  337
c ---[2064]---> BDD-cost:  326
c ---[2062]---> BDD-cost:  326
c ---[2060]---> BDD-cost:  326
c ---[2058]---> BDD-cost:  315
c ---[2056]---> BDD-cost:  315
c ---[2054]---> BDD-cost:  304
c ---[2052]---> BDD-cost:  304
c ---[2050]---> BDD-cost:  293
c ---[2048]---> BDD-cost:  282
c ---[2046]---> BDD-cost:  331
c ---[2044]---> BDD-cost:  337
c ---[2042]---> BDD-cost:  337
c ---[2040]---> BDD-cost:  337
c ---[2038]---> BDD-cost:  337
c ---[2036]---> BDD-cost:  337
c ---[2034]---> BDD-cost:  326
c ---[2032]---> BDD-cost:  326
c ---[2030]---> BDD-cost:  326
c ---[2028]---> BDD-cost:  315
c ---[2026]---> BDD-cost:  315
c ---[2024]---> BDD-cost:  304
c ---[2022]---> BDD-cost:  304
c ---[2020]---> BDD-cost:  293
c ---[2018]---> BDD-cost:  282
c ---[2016]---> BDD-cost:  331
c ---[2014]---> BDD-cost:  337
c ---[2012]---> BDD-cost:  337
c ---[2010]---> BDD-cost:  337
c ---[2008]---> BDD-cost:  337
c ---[2006]---> BDD-cost:  337
c ---[2004]---> BDD-cost:  326
c ---[2002]---> BDD-cost:  326
c ---[2000]---> BDD-cost:  326
c ---[1998]---> BDD-cost:  315
c ---[1996]---> BDD-cost:  315
c ---[1994]---> BDD-cost:  304
c ---[1992]---> BDD-cost:  304
c ---[1990]---> BDD-cost:  293
c ---[1988]---> BDD-cost:  282
c ---[1986]---> BDD-cost:  331
c ---[1984]---> BDD-cost:  337
c ---[1982]---> BDD-cost:  337
c ---[1980]---> BDD-cost:  326
c ---[1978]---> BDD-cost:  326
c ---[1976]---> BDD-cost:  326
c ---[1974]---> BDD-cost:  326
c ---[1972]---> BDD-cost:  315
c ---[1970]---> BDD-cost:  315
c ---[1968]---> BDD-cost:  315
c ---[1966]---> BDD-cost:  304
c ---[1964]---> BDD-cost:  304
c ---[1962]---> BDD-cost:  304
c ---[1960]---> BDD-cost:  293
c ---[1958]---> BDD-cost:  282
c ---[1956]---> BDD-cost:  561
c ---[1954]---> BDD-cost:  561
c ---[1952]---> BDD-cost:  561
c ---[1950]---> BDD-cost:  549
c ---[1948]---> BDD-cost:  549
c ---[1946]---> BDD-cost:  549
c ---[1944]---> BDD-cost:  544
c ---[1942]---> BDD-cost:  530
c ---[1940]---> BDD-cost:  530
c ---[1938]---> BDD-cost:  524
c ---[1936]---> BDD-cost:  507
c ---[1934]---> BDD-cost:  507
c ---[1932]---> BDD-cost:  501
c ---[1930]---> BDD-cost:  478
c ---[1928]---> BDD-cost:  455
c ---[1926]---> BDD-cost:  331
c ---[1924]---> BDD-cost:  337
c ---[1922]---> BDD-cost:  337
c ---[1920]---> BDD-cost:  326
c ---[1918]---> BDD-cost:  326
c ---[1916]---> BDD-cost:  326
c ---[1914]---> BDD-cost:  326
c ---[1912]---> BDD-cost:  315
c ---[1910]---> BDD-cost:  315
c ---[1908]---> BDD-cost:  315
c ---[1906]---> BDD-cost:  304
c ---[1904]---> BDD-cost:  304
c ---[1902]---> BDD-cost:  304
c ---[1900]---> BDD-cost:  293
c ---[1898]---> BDD-cost:  282
c ---[1896]---> BDD-cost:  557
c ---[1894]---> BDD-cost:  557
c ---[1892]---> BDD-cost:  557
c ---[1890]---> BDD-cost:  538
c ---[1888]---> BDD-cost:  538
c ---[1886]---> BDD-cost:  538
c ---[1884]---> BDD-cost:  538
c ---[1882]---> BDD-cost:  515
c ---[1880]---> BDD-cost:  515
c ---[1878]---> BDD-cost:  515
c ---[1876]---> BDD-cost:  492
c ---[1874]---> BDD-cost:  492
c ---[1872]---> BDD-cost:  492
c ---[1870]---> BDD-cost:  469
c ---[1868]---> BDD-cost:  446
c ---[1866]---> BDD-cost:  331
c ---[1864]---> BDD-cost:  337
c ---[1862]---> BDD-cost:  337
c ---[1860]---> BDD-cost:  326
c ---[1858]---> BDD-cost:  326
c ---[1856]---> BDD-cost:  326
c ---[1854]---> BDD-cost:  326
c ---[1852]---> BDD-cost:  315
c ---[1850]---> BDD-cost:  315
c ---[1848]---> BDD-cost:  315
c ---[1846]---> BDD-cost:  304
c ---[1844]---> BDD-cost:  304
c ---[1842]---> BDD-cost:  304
c ---[1840]---> BDD-cost:  293
c ---[1838]---> BDD-cost:  282
c ---[1836]---> BDD-cost:  344
c ---[1834]---> BDD-cost:  344
c ---[1832]---> BDD-cost:  344
c ---[1830]---> BDD-cost:  344
c ---[1828]---> BDD-cost:  344
c ---[1826]---> BDD-cost:  344
c ---[1824]---> BDD-cost:  337
c ---[1822]---> BDD-cost:  337
c ---[1820]---> BDD-cost:  337
c ---[1818]---> BDD-cost:  326
c ---[1816]---> BDD-cost:  326
c ---[1814]---> BDD-cost:  315
c ---[1812]---> BDD-cost:  315
c ---[1810]---> BDD-cost:  304
c ---[1808]---> BDD-cost:  293
c ---[1806]---> BDD-cost:  331
c ---[1804]---> BDD-cost:  337
c ---[1802]---> BDD-cost:  337
c ---[1800]---> BDD-cost:  337
c ---[1798]---> BDD-cost:  337
c ---[1796]---> BDD-cost:  337
c ---[1794]---> BDD-cost:  326
c ---[1792]---> BDD-cost:  326
c ---[1790]---> BDD-cost:  326
c ---[1788]---> BDD-cost:  315
c ---[1786]---> BDD-cost:  315
c ---[1784]---> BDD-cost:  304
c ---[1782]---> BDD-cost:  304
c ---[1780]---> BDD-cost:  293
c ---[1778]---> BDD-cost:  282
c ---[1776]---> BDD-cost:  331
c ---[1774]---> BDD-cost:  337
c ---[1772]---> BDD-cost:  337
c ---[1770]---> BDD-cost:  337
c ---[1768]---> BDD-cost:  337
c ---[1766]---> BDD-cost:  337
c ---[1764]---> BDD-cost:  326
c ---[1762]---> BDD-cost:  326
c ---[1760]---> BDD-cost:  326
c ---[1758]---> BDD-cost:  315
c ---[1756]---> BDD-cost:  315
c ---[1754]---> BDD-cost:  304
c ---[1752]---> BDD-cost:  304
c ---[1750]---> BDD-cost:  293
c ---[1748]---> BDD-cost:  282
c ---[1746]---> BDD-cost:  331
c ---[1744]---> BDD-cost:  337
c ---[1742]---> BDD-cost:  337
c ---[1740]---> BDD-cost:  337
c ---[1738]---> BDD-cost:  337
c ---[1736]---> BDD-cost:  337
c ---[1734]---> BDD-cost:  326
c ---[1732]---> BDD-cost:  326
c ---[1730]---> BDD-cost:  326
c ---[1728]---> BDD-cost:  315
c ---[1726]---> BDD-cost:  315
c ---[1724]---> BDD-cost:  304
c ---[1722]---> BDD-cost:  304
c ---[1720]---> BDD-cost:  293
c ---[1718]---> BDD-cost:  282
c ---[1716]---> BDD-cost:  331
c ---[1714]---> BDD-cost:  337
c ---[1712]---> BDD-cost:  337
c ---[1710]---> BDD-cost:  337
c ---[1708]---> BDD-cost:  337
c ---[1706]---> BDD-cost:  337
c ---[1704]---> BDD-cost:  326
c ---[1702]---> BDD-cost:  326
c ---[1700]---> BDD-cost:  326
c ---[1698]---> BDD-cost:  315
c ---[1696]---> BDD-cost:  315
c ---[1694]---> BDD-cost:  304
c ---[1692]---> BDD-cost:  304
c ---[1690]---> BDD-cost:  293
c ---[1688]---> BDD-cost:  282
c ---[1686]---> BDD-cost:  331
c ---[1684]---> BDD-cost:  337
c ---[1682]---> BDD-cost:  337
c ---[1680]---> BDD-cost:  337
c ---[1678]---> BDD-cost:  337
c ---[1676]---> BDD-cost:  337
c ---[1674]---> BDD-cost:  326
c ---[1672]---> BDD-cost:  326
c ---[1670]---> BDD-cost:  326
c ---[1668]---> BDD-cost:  315
c ---[1666]---> BDD-cost:  315
c ---[1664]---> BDD-cost:  304
c ---[1662]---> BDD-cost:  304
c ---[1660]---> BDD-cost:  293
c ---[1658]---> BDD-cost:  282
c ---[1656]---> BDD-cost:   66
c ---[1654]---> BDD-cost:   57
c ---[1652]---> BDD-cost:   53
c ---[1650]---> BDD-cost:   66
c ---[1648]---> BDD-cost:   55
c ---[1646]---> BDD-cost:   57
c ---[1644]---> BDD-cost:  173
c ---[1642]---> BDD-cost:  183
c ---[1640]---> BDD-cost:  190
c ---[1638]---> BDD-cost:  177
c ---[1636]---> BDD-cost:  171
c ---[1634]---> BDD-cost:  186
c ---[1632]---> BDD-cost:  183
c ---[1630]---> BDD-cost:  183
c ---[1628]---> BDD-cost:  184
c ---[1626]---> BDD-cost:  178
c ---[1624]---> BDD-cost:  179
c ---[1622]---> BDD-cost:  179
c ---[1620]---> BDD-cost:  174
c ---[1618]---> BDD-cost:  174
c ---[1616]---> BDD-cost:  166
c ---[1614]---> BDD-cost:  158
c ---[1612]---> BDD-cost:  171
c ---[1610]---> BDD-cost:  175
c ---[1608]---> BDD-cost:  177
c ---[1606]---> BDD-cost:  184
c ---[1604]---> BDD-cost:  184
c ---[1602]---> BDD-cost:  181
c ---[1600]---> BDD-cost:  179
c ---[1598]---> BDD-cost:  176
c ---[1596]---> BDD-cost:  179
c ---[1594]---> BDD-cost:  167
c ---[1592]---> BDD-cost:  174
c ---[1590]---> BDD-cost:  168
c ---[1588]---> BDD-cost:  169
c ---[1586]---> BDD-cost:  164
c ---[1584]---> BDD-cost:  158
c ---[1582]---> BDD-cost:  171
c ---[1580]---> BDD-cost:  178
c ---[1578]---> BDD-cost:  185
c ---[1576]---> BDD-cost:  189
c ---[1574]---> BDD-cost:  180
c ---[1572]---> BDD-cost:  184
c ---[1570]---> BDD-cost:  181
c ---[1568]---> BDD-cost:  184
c ---[1566]---> BDD-cost:  176
c ---[1564]---> BDD-cost:  179
c ---[1562]---> BDD-cost:  179
c ---[1560]---> BDD-cost:  171
c ---[1558]---> BDD-cost:  174
c ---[1556]---> BDD-cost:  164
c ---[1554]---> BDD-cost:  173
c ---[1552]---> BDD-cost:  183
c ---[1550]---> BDD-cost:  184
c ---[1548]---> BDD-cost:  191
c ---[1546]---> BDD-cost:  194
c ---[1544]---> BDD-cost:  194
c ---[1542]---> BDD-cost:  191
c ---[1540]---> BDD-cost:  177
c ---[1538]---> BDD-cost:  189
c ---[1536]---> BDD-cost:  189
c ---[1534]---> BDD-cost:  172
c ---[1532]---> BDD-cost:  181
c ---[1530]---> BDD-cost:  179
c ---[1528]---> BDD-cost:  179
c ---[1526]---> BDD-cost:  174
c ---[1524]---> BDD-cost:  164
c ---[1522]---> BDD-cost:  171
c ---[1520]---> BDD-cost:  175
c ---[1518]---> BDD-cost:  182
c ---[1516]---> BDD-cost:  184
c ---[1514]---> BDD-cost:  169
c ---[1512]---> BDD-cost:  178
c ---[1510]---> BDD-cost:  184
c ---[1508]---> BDD-cost:  169
c ---[1506]---> BDD-cost:  176
c ---[1504]---> BDD-cost:  179
c ---[1502]---> BDD-cost:  168
c ---[1500]---> BDD-cost:  168
c ---[1498]---> BDD-cost:  169
c ---[1496]---> BDD-cost:  164
c ---[1494]---> BDD-cost:  158
c ---[1492]---> BDD-cost:  171
c ---[1490]---> BDD-cost:  163
c ---[1488]---> BDD-cost:  185
c ---[1486]---> BDD-cost:  189
c ---[1484]---> BDD-cost:  183
c ---[1482]---> BDD-cost:  186
c ---[1480]---> BDD-cost:  184
c ---[1478]---> BDD-cost:  178
c ---[1476]---> BDD-cost:  184
c ---[1474]---> BDD-cost:  179
c ---[1472]---> BDD-cost:  173
c ---[1470]---> BDD-cost:  174
c ---[1468]---> BDD-cost:  169
c ---[1466]---> BDD-cost:  155
c ---[1465]---> BDD-cost:   63
c ---[1464]---> BDD-cost:   78
c ---[1463]---> BDD-cost:   78
c ---[1462]---> BDD-cost:   78
c ---[1461]---> BDD-cost:   74
c ---[1460]---> BDD-cost:   74
c ---[1459]---> BDD-cost:   74
c ---[1458]---> BDD-cost:   74
c ---[1457]---> BDD-cost:   74
c ---[1456]---> BDD-cost:   59
c ---[1455]---> BDD-cost:   74
c ---[1454]---> BDD-cost:   74
c ---[1453]---> BDD-cost:   74
c ---[1452]---> BDD-cost:   63
c ---[1451]---> BDD-cost:   63
c ---[1450]---> BDD-cost:   59
c ---[1449]---> BDD-cost:   74
c ---[1448]---> BDD-cost:   74
c ---[1447]---> BDD-cost:   74
c ---[1446]---> BDD-cost:   74
c ---[1445]---> BDD-cost:   74
c ---[1444]---> BDD-cost:   74
c ---[1443]---> BDD-cost:   63
c ---[1442]---> BDD-cost:   67
c ---[1441]---> BDD-cost:   88
c ---[1440]---> BDD-cost:   88
c ---[1439]---> BDD-cost:   88
c ---[1438]---> BDD-cost:   88
c ---[1437]---> BDD-cost:   88
c ---[1436]---> BDD-cost:   88
c ---[1435]---> BDD-cost:   88
c ---[1434]---> BDD-cost:   84
c ---[1433]---> BDD-cost:   84
c ---[1432]---> BDD-cost:   84
c ---[1431]---> BDD-cost:   63
c ---[1430]---> BDD-cost:   84
c ---[1429]---> BDD-cost:   84
c ---[1428]---> BDD-cost:   84
c ---[1427]---> BDD-cost:   84
c ---[1426]---> BDD-cost:   70
c ---[1425]---> BDD-cost:   63
c ---[1424]---> BDD-cost:   84
c ---[1423]---> BDD-cost:   84
c ---[1422]---> BDD-cost:   84
c ---[1421]---> BDD-cost:   84
c ---[1420]---> BDD-cost:   84
c ---[1419]---> BDD-cost:   84
c ---[1418]---> BDD-cost:   84
c ---[1417]---> BDD-cost:   75
c ---[1416]---> BDD-cost:  102
c ---[1415]---> BDD-cost:  102
c ---[1414]---> BDD-cost:  102
c ---[1413]---> BDD-cost:   98
c ---[1412]---> BDD-cost:   98
c ---[1411]---> BDD-cost:   98
c ---[1410]---> BDD-cost:   98
c ---[1409]---> BDD-cost:   84
c ---[1408]---> BDD-cost:   75
c ---[1407]---> BDD-cost:  102
c ---[1406]---> BDD-cost:  102
c ---[1405]---> BDD-cost:  102
c ---[1404]---> BDD-cost:   98
c ---[1403]---> BDD-cost:   98
c ---[1402]---> BDD-cost:   98
c ---[1401]---> BDD-cost:   98
c ---[1400]---> BDD-cost:   84
c ---[1399]---> BDD-cost:   75
c ---[1398]---> BDD-cost:  102
c ---[1397]---> BDD-cost:  102
c ---[1396]---> BDD-cost:  102
c ---[1395]---> BDD-cost:  102
c ---[1394]---> BDD-cost:  102
c ---[1393]---> BDD-cost:  102
c ---[1392]---> BDD-cost:   98
c ---[1391]---> BDD-cost:   98
c ---[1390]---> BDD-cost:   98
c ---[1389]---> BDD-cost:   75
c ---[1388]---> BDD-cost:  102
c ---[1387]---> BDD-cost:  102
c ---[1386]---> BDD-cost:  102
c ---[1385]---> BDD-cost:  102
c ---[1384]---> BDD-cost:  102
c ---[1383]---> BDD-cost:  102
c ---[1382]---> BDD-cost:   98
c ---[1381]---> BDD-cost:   98
c ---[1380]---> BDD-cost:   98
c ---[1379]---> BDD-cost:   74
c ---[1378]---> BDD-cost:  109
c ---[1377]---> BDD-cost:  109
c ---[1376]---> BDD-cost:   74
c ---[1375]---> BDD-cost:  109
c ---[1374]---> BDD-cost:  109
c ---[1373]---> BDD-cost:   74
c ---[1372]---> BDD-cost:  109
c ---[1371]---> BDD-cost:  109
c ---[1370]---> BDD-cost:   74
c ---[1369]---> BDD-cost:  109
c ---[1368]---> BDD-cost:  109
c ---[1367]---> BDD-cost:   74
c ---[1366]---> BDD-cost:  109
c ---[1365]---> BDD-cost:  109
c ---[1364]---> BDD-cost:  109
c ---[1363]---> BDD-cost:  109
c ---[1362]---> BDD-cost:  109
c ---[1361]---> BDD-cost:   74
c ---[1360]---> BDD-cost:  109
c ---[1359]---> BDD-cost:  109
c ---[1358]---> BDD-cost:  109
c ---[1357]---> BDD-cost:  109
c ---[1356]---> BDD-cost:  109
c ---[1355]---> BDD-cost:   74
c ---[1354]---> BDD-cost:  109
c ---[1353]---> BDD-cost:  109
c ---[1352]---> BDD-cost:  109
c ---[1351]---> BDD-cost:  109
c ---[1350]---> BDD-cost:  109
c ---[1349]---> BDD-cost:   74
c ---[1348]---> BDD-cost:  109
c ---[1347]---> BDD-cost:  109
c ---[1346]---> BDD-cost:  109
c ---[1345]---> BDD-cost:  109
c ---[1344]---> BDD-cost:  109
c ---[1343]---> BDD-cost:   74
c ---[1342]---> BDD-cost:  109
c ---[1341]---> BDD-cost:  109
c ---[1340]---> BDD-cost:  109
c ---[1339]---> BDD-cost:  109
c ---[1338]---> BDD-cost:  109
c ---[1337]---> BDD-cost:   81
c ---[1336]---> BDD-cost:  117
c ---[1335]---> BDD-cost:  117
c ---[1334]---> BDD-cost:  117
c ---[1333]---> BDD-cost:  109
c ---[1332]---> BDD-cost:  109
c ---[1331]---> BDD-cost:  109
c ---[1330]---> BDD-cost:   81
c ---[1329]---> BDD-cost:  117
c ---[1328]---> BDD-cost:  117
c ---[1327]---> BDD-cost:  117
c ---[1326]---> BDD-cost:  117
c ---[1325]---> BDD-cost:  117
c ---[1324]---> BDD-cost:  117
c ---[1323]---> BDD-cost:  109
c ---[1322]---> BDD-cost:  109
c ---[1321]---> BDD-cost:   74
c ---[1320]---> BDD-cost:  109
c ---[1319]---> BDD-cost:  109
c ---[1318]---> BDD-cost:  109
c ---[1317]---> BDD-cost:   74
c ---[1316]---> BDD-cost:  109
c ---[1315]---> BDD-cost:  109
c ---[1314]---> BDD-cost:  109
c ---[1313]---> BDD-cost:   74
c ---[1312]---> BDD-cost:  109
c ---[1311]---> BDD-cost:  109
c ---[1310]---> BDD-cost:  109
c ---[1309]---> BDD-cost:   74
c ---[1308]---> BDD-cost:  109
c ---[1307]---> BDD-cost:  109
c ---[1306]---> BDD-cost:  109
c ---[1305]---> BDD-cost:   77
c ---[1304]---> BDD-cost:  107
c ---[1303]---> BDD-cost:  107
c ---[1302]---> BDD-cost:  107
c ---[1301]---> BDD-cost:  107
c ---[1300]---> BDD-cost:  107
c ---[1299]---> BDD-cost:  107
c ---[1298]---> BDD-cost:   96
c ---[1297]---> BDD-cost:   77
c ---[1296]---> BDD-cost:  107
c ---[1295]---> BDD-cost:  107
c ---[1294]---> BDD-cost:  107
c ---[1293]---> BDD-cost:   96
c ---[1292]---> BDD-cost:   96
c ---[1291]---> BDD-cost:   77
c ---[1290]---> BDD-cost:  107
c ---[1289]---> BDD-cost:  107
c ---[1288]---> BDD-cost:  107
c ---[1287]---> BDD-cost:  107
c ---[1286]---> BDD-cost:  107
c ---[1285]---> BDD-cost:  107
c ---[1284]---> BDD-cost:   96
c ---[1283]---> BDD-cost:   67
c ---[1282]---> BDD-cost:   67
c ---[1281]---> BDD-cost:   67
c ---[1280]---> BDD-cost:   67
c ---[1279]---> BDD-cost:   67
c ---[1278]---> BDD-cost:   16
c ---[1277]---> BDD-cost:   27
c ---[1276]---> BDD-cost:   27
c ---[1275]---> BDD-cost:   26
c ---[1274]---> BDD-cost:   25
c ---[1273]---> BDD-cost:   25
c ---[1272]---> BDD-cost:   25
c ---[1271]---> BDD-cost:   25
c ---[1270]---> BDD-cost:   25
c ---[1269]---> BDD-cost:   23
c ---[1268]---> BDD-cost:   22
c ---[1267]---> BDD-cost:   20
c ---[1266]---> BDD-cost:   21
c ---[1265]---> BDD-cost:   18
c ---[1264]---> BDD-cost:   19
c ---[1263]---> BDD-cost:   16
c ---[1262]---> BDD-cost:   15
c ---[1261]---> BDD-cost:   24
c ---[1260]---> BDD-cost:   24
c ---[1259]---> BDD-cost:   25
c ---[1258]---> BDD-cost:   23
c ---[1257]---> BDD-cost:   23
c ---[1256]---> BDD-cost:   22
c ---[1255]---> BDD-cost:   23
c ---[1254]---> BDD-cost:   21
c ---[1253]---> BDD-cost:   20
c ---[1252]---> BDD-cost:   19
c ---[1251]---> BDD-cost:   21
c ---[1250]---> BDD-cost:   19
c ---[1249]---> BDD-cost:   14
c ---[1248]---> BDD-cost:   15
c ---[1247]---> BDD-cost:   15
c ---[1245]---> BDD-cost:   23
c ---[1244]---> BDD-cost:   22
c ---[1243]---> BDD-cost:   25
c ---[1242]---> BDD-cost:   23
c ---[1241]---> BDD-cost:   25
c ---[1240]---> BDD-cost:   20
c ---[1239]---> BDD-cost:   20
c ---[1238]---> BDD-cost:   23
c ---[1237]---> BDD-cost:   23
c ---[1236]---> BDD-cost:   19
c ---[1235]---> BDD-cost:   20
c ---[1234]---> BDD-cost:   21
c ---[1233]---> BDD-cost:   18
c ---[1232]---> BDD-cost:   17
c ---[1231]---> BDD-cost:   15
c ---[1229]---> BDD-cost:   26
c ---[1228]---> BDD-cost:   24
c ---[1227]---> BDD-cost:   27
c ---[1226]---> BDD-cost:   27
c ---[1225]---> BDD-cost:   27
c ---[1224]---> BDD-cost:   25
c ---[1223]---> BDD-cost:   27
c ---[1222]---> BDD-cost:   25
c ---[1221]---> BDD-cost:   25
c ---[1220]---> BDD-cost:   24
c ---[1219]---> BDD-cost:   23
c ---[1218]---> BDD-cost:   23
c ---[1217]---> BDD-cost:   21
c ---[1216]---> BDD-cost:   20
c ---[1215]---> BDD-cost:   19
c ---[1214]---> BDD-cost:   15
c ---[1213]---> BDD-cost:   25
c ---[1212]---> BDD-cost:   20
c ---[1211]---> BDD-cost:   25
c ---[1210]---> BDD-cost:   25
c ---[1209]---> BDD-cost:   23
c ---[1208]---> BDD-cost:   21
c ---[1207]---> BDD-cost:   21
c ---[1206]---> BDD-cost:   18
c ---[1205]---> BDD-cost:   23
c ---[1204]---> BDD-cost:   21
c ---[1203]---> BDD-cost:   21
c ---[1202]---> BDD-cost:   17
c ---[1201]---> BDD-cost:   14
c ---[1200]---> BDD-cost:   15
c ---[1199]---> BDD-cost:   15
c ---[1197]---> BDD-cost:   24
c ---[1196]---> BDD-cost:   24
c ---[1195]---> BDD-cost:   25
c ---[1194]---> BDD-cost:   25
c ---[1193]---> BDD-cost:   23
c ---[1192]---> BDD-cost:   25
c ---[1191]---> BDD-cost:   25
c ---[1190]---> BDD-cost:   23
c ---[1189]---> BDD-cost:   20
c ---[1188]---> BDD-cost:   21
c ---[1187]---> BDD-cost:   21
c ---[1186]---> BDD-cost:   19
c ---[1185]---> BDD-cost:   16
c ---[1184]---> BDD-cost:   17
c ---[1183]---> BDD-cost:   12
c ---[1182]---> BDD-cost:   18
c ---[1181]---> BDD-cost:   31
c ---[1180]---> BDD-cost:   31
c ---[1179]---> BDD-cost:   31
c ---[1178]---> BDD-cost:   29
c ---[1177]---> BDD-cost:   27
c ---[1176]---> BDD-cost:   29
c ---[1175]---> BDD-cost:   29
c ---[1174]---> BDD-cost:   25
c ---[1173]---> BDD-cost:   27
c ---[1172]---> BDD-cost:   25
c ---[1171]---> BDD-cost:   24
c ---[1170]---> BDD-cost:   24
c ---[1169]---> BDD-cost:   25
c ---[1168]---> BDD-cost:   23
c ---[1167]---> BDD-cost:   21
c ---[1166]---> BDD-cost:   18
c ---[1165]---> BDD-cost:   31
c ---[1164]---> BDD-cost:   31
c ---[1163]---> BDD-cost:   31
c ---[1162]---> BDD-cost:   29
c ---[1161]---> BDD-cost:   27
c ---[1160]---> BDD-cost:   29
c ---[1159]---> BDD-cost:   29
c ---[1158]---> BDD-cost:   25
c ---[1157]---> BDD-cost:   27
c ---[1156]---> BDD-cost:   25
c ---[1155]---> BDD-cost:   24
c ---[1154]---> BDD-cost:   24
c ---[1153]---> BDD-cost:   25
c ---[1152]---> BDD-cost:   23
c ---[1151]---> BDD-cost:   21
c ---[1150]---> BDD-cost:   18
c ---[1149]---> BDD-cost:   28
c ---[1148]---> BDD-cost:   31
c ---[1147]---> BDD-cost:   31
c ---[1146]---> BDD-cost:   31
c ---[1145]---> BDD-cost:   31
c ---[1144]---> BDD-cost:   30
c ---[1143]---> BDD-cost:   23
c ---[1142]---> BDD-cost:   29
c ---[1141]---> BDD-cost:   28
c ---[1140]---> BDD-cost:   27
c ---[1139]---> BDD-cost:   23
c ---[1138]---> BDD-cost:   24
c ---[1137]---> BDD-cost:   25
c ---[1136]---> BDD-cost:   21
c ---[1135]---> BDD-cost:   16
c ---[1134]---> BDD-cost:   18
c ---[1133]---> BDD-cost:   28
c ---[1132]---> BDD-cost:   31
c ---[1131]---> BDD-cost:   31
c ---[1130]---> BDD-cost:   31
c ---[1129]---> BDD-cost:   31
c ---[1128]---> BDD-cost:   30
c ---[1127]---> BDD-cost:   23
c ---[1126]---> BDD-cost:   29
c ---[1125]---> BDD-cost:   28
c ---[1124]---> BDD-cost:   27
c ---[1123]---> BDD-cost:   23
c ---[1122]---> BDD-cost:   24
c ---[1121]---> BDD-cost:   25
c ---[1120]---> BDD-cost:   21
c ---[1119]---> BDD-cost:   16
c ---[1118]---> BDD-cost:   18
c ---[1117]---> BDD-cost:   31
c ---[1116]---> BDD-cost:   31
c ---[1115]---> BDD-cost:   31
c ---[1114]---> BDD-cost:   29
c ---[1113]---> BDD-cost:   27
c ---[1112]---> BDD-cost:   29
c ---[1111]---> BDD-cost:   29
c ---[1110]---> BDD-cost:   25
c ---[1109]---> BDD-cost:   27
c ---[1108]---> BDD-cost:   25
c ---[1107]---> BDD-cost:   24
c ---[1106]---> BDD-cost:   24
c ---[1105]---> BDD-cost:   25
c ---[1104]---> BDD-cost:   23
c ---[1103]---> BDD-cost:   21
c ---[1102]---> BDD-cost:   18
c ---[1101]---> BDD-cost:   31
c ---[1100]---> BDD-cost:   31
c ---[1099]---> BDD-cost:   31
c ---[1098]---> BDD-cost:   29
c ---[1097]---> BDD-cost:   27
c ---[1096]---> BDD-cost:   29
c ---[1095]---> BDD-cost:   29
c ---[1094]---> BDD-cost:   25
c ---[1093]---> BDD-cost:   27
c ---[1092]---> BDD-cost:   25
c ---[1091]---> BDD-cost:   24
c ---[1090]---> BDD-cost:   24
c ---[1089]---> BDD-cost:   25
c ---[1088]---> BDD-cost:   23
c ---[1087]---> BDD-cost:   21
c ---[1086]---> BDD-cost:   18
c ---[1085]---> BDD-cost:   31
c ---[1084]---> BDD-cost:   31
c ---[1083]---> BDD-cost:   31
c ---[1082]---> BDD-cost:   29
c ---[1081]---> BDD-cost:   27
c ---[1080]---> BDD-cost:   29
c ---[1079]---> BDD-cost:   29
c ---[1078]---> BDD-cost:   25
c ---[1077]---> BDD-cost:   27
c ---[1076]---> BDD-cost:   25
c ---[1075]---> BDD-cost:   24
c ---[1074]---> BDD-cost:   24
c ---[1073]---> BDD-cost:   25
c ---[1072]---> BDD-cost:   23
c ---[1071]---> BDD-cost:   21
c ---[1070]---> BDD-cost:   18
c ---[1069]---> BDD-cost:   31
c ---[1068]---> BDD-cost:   31
c ---[1067]---> BDD-cost:   31
c ---[1066]---> BDD-cost:   29
c ---[1065]---> BDD-cost:   27
c ---[1064]---> BDD-cost:   29
c ---[1063]---> BDD-cost:   29
c ---[1062]---> BDD-cost:   25
c ---[1061]---> BDD-cost:   27
c ---[1060]---> BDD-cost:   25
c ---[1059]---> BDD-cost:   24
c ---[1058]---> BDD-cost:   24
c ---[1057]---> BDD-cost:   25
c ---[1056]---> BDD-cost:   23
c ---[1055]---> BDD-cost:   21
c ---[1054]---> BDD-cost:   18
c ---[1053]---> BDD-cost:   28
c ---[1052]---> BDD-cost:   31
c ---[1051]---> BDD-cost:   31
c ---[1050]---> BDD-cost:   31
c ---[1049]---> BDD-cost:   31
c ---[1048]---> BDD-cost:   30
c ---[1047]---> BDD-cost:   23
c ---[1046]---> BDD-cost:   29
c ---[1045]---> BDD-cost:   28
c ---[1044]---> BDD-cost:   27
c ---[1043]---> BDD-cost:   23
c ---[1042]---> BDD-cost:   24
c ---[1041]---> BDD-cost:   25
c ---[1040]---> BDD-cost:   21
c ---[1039]---> BDD-cost:   16
c ---[1038]---> BDD-cost:   18
c ---[1037]---> BDD-cost:   28
c ---[1036]---> BDD-cost:   31
c ---[1035]---> BDD-cost:   31
c ---[1034]---> BDD-cost:   31
c ---[1033]---> BDD-cost:   31
c ---[1032]---> BDD-cost:   30
c ---[1031]---> BDD-cost:   23
c ---[1030]---> BDD-cost:   29
c ---[1029]---> BDD-cost:   28
c ---[1028]---> BDD-cost:   27
c ---[1027]---> BDD-cost:   23
c ---[1026]---> BDD-cost:   24
c ---[1025]---> BDD-cost:   25
c ---[1024]---> BDD-cost:   21
c ---[1023]---> BDD-cost:   16
c ---[1022]---> BDD-cost:   18
c ---[1021]---> BDD-cost:   28
c ---[1020]---> BDD-cost:   31
c ---[1019]---> BDD-cost:   31
c ---[1018]---> BDD-cost:   31
c ---[1017]---> BDD-cost:   31
c ---[1016]---> BDD-cost:   30
c ---[1015]---> BDD-cost:   23
c ---[1014]---> BDD-cost:   29
c ---[1013]---> BDD-cost:   28
c ---[1012]---> BDD-cost:   27
c ---[1011]---> BDD-cost:   23
c ---[1010]---> BDD-cost:   24
c ---[1009]---> BDD-cost:   25
c ---[1008]---> BDD-cost:   21
c ---[1007]---> BDD-cost:   16
c ---[1006]---> BDD-cost:   18
c ---[1005]---> BDD-cost:   28
c ---[1004]---> BDD-cost:   31
c ---[1003]---> BDD-cost:   31
c ---[1002]---> BDD-cost:   31
c ---[1001]---> BDD-cost:   31
c ---[1000]---> BDD-cost:   30
c ---[ 999]---> BDD-cost:   23
c ---[ 998]---> BDD-cost:   29
c ---[ 997]---> BDD-cost:   28
c ---[ 996]---> BDD-cost:   27
c ---[ 995]---> BDD-cost:   23
c ---[ 994]---> BDD-cost:   24
c ---[ 993]---> BDD-cost:   25
c ---[ 992]---> BDD-cost:   21
c ---[ 991]---> BDD-cost:   16
c ---[ 990]---> BDD-cost:   18
c ---[ 989]---> BDD-cost:   28
c ---[ 988]---> BDD-cost:   31
c ---[ 987]---> BDD-cost:   31
c ---[ 986]---> BDD-cost:   31
c ---[ 985]---> BDD-cost:   31
c ---[ 984]---> BDD-cost:   30
c ---[ 983]---> BDD-cost:   23
c ---[ 982]---> BDD-cost:   29
c ---[ 981]---> BDD-cost:   28
c ---[ 980]---> BDD-cost:   27
c ---[ 979]---> BDD-cost:   23
c ---[ 978]---> BDD-cost:   24
c ---[ 977]---> BDD-cost:   25
c ---[ 976]---> BDD-cost:   21
c ---[ 975]---> BDD-cost:   16
c ---[ 974]---> BDD-cost:   18
c ---[ 973]---> BDD-cost:   31
c ---[ 972]---> BDD-cost:   31
c ---[ 971]---> BDD-cost:   31
c ---[ 970]---> BDD-cost:   29
c ---[ 969]---> BDD-cost:   27
c ---[ 968]---> BDD-cost:   29
c ---[ 967]---> BDD-cost:   29
c ---[ 966]---> BDD-cost:   25
c ---[ 965]---> BDD-cost:   27
c ---[ 964]---> BDD-cost:   25
c ---[ 963]---> BDD-cost:   24
c ---[ 962]---> BDD-cost:   24
c ---[ 961]---> BDD-cost:   25
c ---[ 960]---> BDD-cost:   23
c ---[ 959]---> BDD-cost:   21
c ---[ 958]---> BDD-cost:   19
c ---[ 957]---> BDD-cost:   32
c ---[ 956]---> BDD-cost:   32
c ---[ 955]---> BDD-cost:   32
c ---[ 954]---> BDD-cost:   30
c ---[ 953]---> BDD-cost:   28
c ---[ 952]---> BDD-cost:   30
c ---[ 951]---> BDD-cost:   30
c ---[ 950]---> BDD-cost:   26
c ---[ 949]---> BDD-cost:   28
c ---[ 948]---> BDD-cost:   26
c ---[ 947]---> BDD-cost:   25
c ---[ 946]---> BDD-cost:   25
c ---[ 945]---> BDD-cost:   26
c ---[ 944]---> BDD-cost:   24
c ---[ 943]---> BDD-cost:   22
c ---[ 942]---> BDD-cost:   18
c ---[ 941]---> BDD-cost:   31
c ---[ 940]---> BDD-cost:   31
c ---[ 939]---> BDD-cost:   31
c ---[ 938]---> BDD-cost:   29
c ---[ 937]---> BDD-cost:   27
c ---[ 936]---> BDD-cost:   29
c ---[ 935]---> BDD-cost:   29
c ---[ 934]---> BDD-cost:   25
c ---[ 933]---> BDD-cost:   27
c ---[ 932]---> BDD-cost:   25
c ---[ 931]---> BDD-cost:   24
c ---[ 930]---> BDD-cost:   24
c ---[ 929]---> BDD-cost:   25
c ---[ 928]---> BDD-cost:   23
c ---[ 927]---> BDD-cost:   21
c ---[ 926]---> BDD-cost:   18
c ---[ 925]---> BDD-cost:   31
c ---[ 924]---> BDD-cost:   31
c ---[ 923]---> BDD-cost:   31
c ---[ 922]---> BDD-cost:   29
c ---[ 921]---> BDD-cost:   27
c ---[ 920]---> BDD-cost:   29
c ---[ 919]---> BDD-cost:   29
c ---[ 918]---> BDD-cost:   25
c ---[ 917]---> BDD-cost:   27
c ---[ 916]---> BDD-cost:   25
c ---[ 915]---> BDD-cost:   24
c ---[ 914]---> BDD-cost:   24
c ---[ 913]---> BDD-cost:   25
c ---[ 912]---> BDD-cost:   23
c ---[ 911]---> BDD-cost:   21
c ---[ 910]---> BDD-cost:   18
c ---[ 909]---> BDD-cost:   31
c ---[ 908]---> BDD-cost:   31
c ---[ 907]---> BDD-cost:   31
c ---[ 906]---> BDD-cost:   29
c ---[ 905]---> BDD-cost:   27
c ---[ 904]---> BDD-cost:   29
c ---[ 903]---> BDD-cost:   29
c ---[ 902]---> BDD-cost:   25
c ---[ 901]---> BDD-cost:   27
c ---[ 900]---> BDD-cost:   25
c ---[ 899]---> BDD-cost:   24
c ---[ 898]---> BDD-cost:   24
c ---[ 897]---> BDD-cost:   25
c ---[ 896]---> BDD-cost:   23
c ---[ 895]---> BDD-cost:   21
c ---[ 894]---> BDD-cost:   19
c ---[ 893]---> BDD-cost:   29
c ---[ 892]---> BDD-cost:   32
c ---[ 891]---> BDD-cost:   32
c ---[ 890]---> BDD-cost:   32
c ---[ 889]---> BDD-cost:   32
c ---[ 888]---> BDD-cost:   31
c ---[ 887]---> BDD-cost:   24
c ---[ 886]---> BDD-cost:   30
c ---[ 885]---> BDD-cost:   29
c ---[ 884]---> BDD-cost:   28
c ---[ 883]---> BDD-cost:   24
c ---[ 882]---> BDD-cost:   25
c ---[ 881]---> BDD-cost:   26
c ---[ 880]---> BDD-cost:   22
c ---[ 879]---> BDD-cost:   17
c ---[ 878]---> BDD-cost:   18
c ---[ 877]---> BDD-cost:   28
c ---[ 876]---> BDD-cost:   31
c ---[ 875]---> BDD-cost:   31
c ---[ 874]---> BDD-cost:   31
c ---[ 873]---> BDD-cost:   31
c ---[ 872]---> BDD-cost:   30
c ---[ 871]---> BDD-cost:   23
c ---[ 870]---> BDD-cost:   29
c ---[ 869]---> BDD-cost:   28
c ---[ 868]---> BDD-cost:   27
c ---[ 867]---> BDD-cost:   23
c ---[ 866]---> BDD-cost:   24
c ---[ 865]---> BDD-cost:   25
c ---[ 864]---> BDD-cost:   21
c ---[ 863]---> BDD-cost:   16
c ---[ 862]---> BDD-cost:   18
c ---[ 861]---> BDD-cost:   28
c ---[ 860]---> BDD-cost:   31
c ---[ 859]---> BDD-cost:   31
c ---[ 858]---> BDD-cost:   31
c ---[ 857]---> BDD-cost:   31
c ---[ 856]---> BDD-cost:   30
c ---[ 855]---> BDD-cost:   23
c ---[ 854]---> BDD-cost:   29
c ---[ 853]---> BDD-cost:   28
c ---[ 852]---> BDD-cost:   27
c ---[ 851]---> BDD-cost:   23
c ---[ 850]---> BDD-cost:   24
c ---[ 849]---> BDD-cost:   25
c ---[ 848]---> BDD-cost:   21
c ---[ 847]---> BDD-cost:   16
c ---[ 846]---> BDD-cost:   18
c ---[ 845]---> BDD-cost:   28
c ---[ 844]---> BDD-cost:   31
c ---[ 843]---> BDD-cost:   31
c ---[ 842]---> BDD-cost:   31
c ---[ 841]---> BDD-cost:   31
c ---[ 840]---> BDD-cost:   30
c ---[ 839]---> BDD-cost:   23
c ---[ 838]---> BDD-cost:   29
c ---[ 837]---> BDD-cost:   28
c ---[ 836]---> BDD-cost:   27
c ---[ 835]---> BDD-cost:   23
c ---[ 834]---> BDD-cost:   24
c ---[ 833]---> BDD-cost:   25
c ---[ 832]---> BDD-cost:   21
c ---[ 831]---> BDD-cost:   16
c ---[ 830]---> BDD-cost:   18
c ---[ 829]---> BDD-cost:   28
c ---[ 828]---> BDD-cost:   31
c ---[ 827]---> BDD-cost:   31
c ---[ 826]---> BDD-cost:   31
c ---[ 825]---> BDD-cost:   31
c ---[ 824]---> BDD-cost:   30
c ---[ 823]---> BDD-cost:   23
c ---[ 822]---> BDD-cost:   29
c ---[ 821]---> BDD-cost:   28
c ---[ 820]---> BDD-cost:   27
c ---[ 819]---> BDD-cost:   23
c ---[ 818]---> BDD-cost:   24
c ---[ 817]---> BDD-cost:   25
c ---[ 816]---> BDD-cost:   21
c ---[ 815]---> BDD-cost:   16
c ---[ 814]---> BDD-cost:   18
c ---[ 813]---> BDD-cost:   31
c ---[ 812]---> BDD-cost:   31
c ---[ 811]---> BDD-cost:   31
c ---[ 810]---> BDD-cost:   29
c ---[ 809]---> BDD-cost:   27
c ---[ 808]---> BDD-cost:   29
c ---[ 807]---> BDD-cost:   29
c ---[ 806]---> BDD-cost:   25
c ---[ 805]---> BDD-cost:   27
c ---[ 804]---> BDD-cost:   25
c ---[ 803]---> BDD-cost:   24
c ---[ 802]---> BDD-cost:   24
c ---[ 801]---> BDD-cost:   25
c ---[ 800]---> BDD-cost:   23
c ---[ 799]---> BDD-cost:   21
c ---[ 797]---> BDD-cost:   33
c ---[ 796]---> BDD-cost:   33
c ---[ 795]---> BDD-cost:   33
c ---[ 794]---> BDD-cost:   33
c ---[ 793]---> BDD-cost:   31
c ---[ 792]---> BDD-cost:   33
c ---[ 791]---> BDD-cost:   31
c ---[ 790]---> BDD-cost:   29
c ---[ 789]---> BDD-cost:   31
c ---[ 788]---> BDD-cost:   27
c ---[ 787]---> BDD-cost:   28
c ---[ 786]---> BDD-cost:   28
c ---[ 785]---> BDD-cost:   27
c ---[ 784]---> BDD-cost:   25
c ---[ 783]---> BDD-cost:   23
c ---[ 782]---> BDD-cost:   18
c ---[ 781]---> BDD-cost:   31
c ---[ 780]---> BDD-cost:   31
c ---[ 779]---> BDD-cost:   31
c ---[ 778]---> BDD-cost:   29
c ---[ 777]---> BDD-cost:   27
c ---[ 776]---> BDD-cost:   29
c ---[ 775]---> BDD-cost:   29
c ---[ 774]---> BDD-cost:   25
c ---[ 773]---> BDD-cost:   27
c ---[ 772]---> BDD-cost:   25
c ---[ 771]---> BDD-cost:   24
c ---[ 770]---> BDD-cost:   24
c ---[ 769]---> BDD-cost:   25
c ---[ 768]---> BDD-cost:   23
c ---[ 767]---> BDD-cost:   21
c ---[ 766]---> BDD-cost:   19
c ---[ 765]---> BDD-cost:   32
c ---[ 764]---> BDD-cost:   32
c ---[ 763]---> BDD-cost:   32
c ---[ 762]---> BDD-cost:   30
c ---[ 761]---> BDD-cost:   28
c ---[ 760]---> BDD-cost:   30
c ---[ 759]---> BDD-cost:   30
c ---[ 758]---> BDD-cost:   26
c ---[ 757]---> BDD-cost:   28
c ---[ 756]---> BDD-cost:   26
c ---[ 755]---> BDD-cost:   25
c ---[ 754]---> BDD-cost:   25
c ---[ 753]---> BDD-cost:   26
c ---[ 752]---> BDD-cost:   24
c ---[ 751]---> BDD-cost:   22
c ---[ 750]---> BDD-cost:   18
c ---[ 749]---> BDD-cost:   31
c ---[ 748]---> BDD-cost:   31
c ---[ 747]---> BDD-cost:   31
c ---[ 746]---> BDD-cost:   29
c ---[ 745]---> BDD-cost:   27
c ---[ 744]---> BDD-cost:   29
c ---[ 743]---> BDD-cost:   29
c ---[ 742]---> BDD-cost:   25
c ---[ 741]---> BDD-cost:   27
c ---[ 740]---> BDD-cost:   25
c ---[ 739]---> BDD-cost:   24
c ---[ 738]---> BDD-cost:   24
c ---[ 737]---> BDD-cost:   25
c ---[ 736]---> BDD-cost:   23
c ---[ 735]---> BDD-cost:   21
c ---[ 734]---> BDD-cost:   19
c ---[ 733]---> BDD-cost:   29
c ---[ 732]---> BDD-cost:   32
c ---[ 731]---> BDD-cost:   32
c ---[ 730]---> BDD-cost:   32
c ---[ 729]---> BDD-cost:   32
c ---[ 728]---> BDD-cost:   31
c ---[ 727]---> BDD-cost:   24
c ---[ 726]---> BDD-cost:   30
c ---[ 725]---> BDD-cost:   29
c ---[ 724]---> BDD-cost:   28
c ---[ 723]---> BDD-cost:   24
c ---[ 722]---> BDD-cost:   25
c ---[ 721]---> BDD-cost:   26
c ---[ 720]---> BDD-cost:   22
c ---[ 719]---> BDD-cost:   17
c ---[ 718]---> BDD-cost:   18
c ---[ 717]---> BDD-cost:   28
c ---[ 716]---> BDD-cost:   31
c ---[ 715]---> BDD-cost:   31
c ---[ 714]---> BDD-cost:   31
c ---[ 713]---> BDD-cost:   31
c ---[ 712]---> BDD-cost:   30
c ---[ 711]---> BDD-cost:   23
c ---[ 710]---> BDD-cost:   29
c ---[ 709]---> BDD-cost:   28
c ---[ 708]---> BDD-cost:   27
c ---[ 707]---> BDD-cost:   23
c ---[ 706]---> BDD-cost:   24
c ---[ 705]---> BDD-cost:   25
c ---[ 704]---> BDD-cost:   21
c ---[ 703]---> BDD-cost:   16
c ---[ 702]---> BDD-cost:   18
c ---[ 701]---> BDD-cost:   28
c ---[ 700]---> BDD-cost:   31
c ---[ 699]---> BDD-cost:   31
c ---[ 698]---> BDD-cost:   31
c ---[ 697]---> BDD-cost:   31
c ---[ 696]---> BDD-cost:   30
c ---[ 695]---> BDD-cost:   23
c ---[ 694]---> BDD-cost:   29
c ---[ 693]---> BDD-cost:   28
c ---[ 692]---> BDD-cost:   27
c ---[ 691]---> BDD-cost:   23
c ---[ 690]---> BDD-cost:   24
c ---[ 689]---> BDD-cost:   25
c ---[ 688]---> BDD-cost:   21
c ---[ 687]---> BDD-cost:   16
c ---[ 686]---> BDD-cost:   18
c ---[ 685]---> BDD-cost:   28
c ---[ 684]---> BDD-cost:   31
c ---[ 683]---> BDD-cost:   31
c ---[ 682]---> BDD-cost:   31
c ---[ 681]---> BDD-cost:   31
c ---[ 680]---> BDD-cost:   30
c ---[ 679]---> BDD-cost:   23
c ---[ 678]---> BDD-cost:   29
c ---[ 677]---> BDD-cost:   28
c ---[ 676]---> BDD-cost:   27
c ---[ 675]---> BDD-cost:   23
c ---[ 674]---> BDD-cost:   24
c ---[ 673]---> BDD-cost:   25
c ---[ 672]---> BDD-cost:   21
c ---[ 671]---> BDD-cost:   16
c ---[ 670]---> BDD-cost:   18
c ---[ 669]---> BDD-cost:   28
c ---[ 668]---> BDD-cost:   31
c ---[ 667]---> BDD-cost:   31
c ---[ 666]---> BDD-cost:   31
c ---[ 665]---> BDD-cost:   31
c ---[ 664]---> BDD-cost:   30
c ---[ 663]---> BDD-cost:   23
c ---[ 662]---> BDD-cost:   29
c ---[ 661]---> BDD-cost:   28
c ---[ 660]---> BDD-cost:   27
c ---[ 659]---> BDD-cost:   23
c ---[ 658]---> BDD-cost:   24
c ---[ 657]---> BDD-cost:   25
c ---[ 656]---> BDD-cost:   21
c ---[ 655]---> BDD-cost:   16
c ---[ 654]---> BDD-cost:   18
c ---[ 653]---> BDD-cost:   28
c ---[ 652]---> BDD-cost:   31
c ---[ 651]---> BDD-cost:   31
c ---[ 650]---> BDD-cost:   31
c ---[ 649]---> BDD-cost:   31
c ---[ 648]---> BDD-cost:   30
c ---[ 647]---> BDD-cost:   23
c ---[ 646]---> BDD-cost:   29
c ---[ 645]---> BDD-cost:   28
c ---[ 644]---> BDD-cost:   27
c ---[ 643]---> BDD-cost:   23
c ---[ 642]---> BDD-cost:   24
c ---[ 641]---> BDD-cost:   25
c ---[ 640]---> BDD-cost:   21
c ---[ 639]---> BDD-cost:   16
c ---[ 638]---> BDD-cost:  307
c ---[ 637]---> BDD-cost:  590
c ---[ 636]---> BDD-cost:  590
c ---[ 635]---> BDD-cost:  590
c ---[ 634]---> BDD-cost:  574
c ---[ 633]---> BDD-cost:  574
c ---[ 632]---> BDD-cost:  574
c ---[ 623]---> BDD-cost:  311
c ---[ 622]---> BDD-cost:  572
c ---[ 621]---> BDD-cost:  572
c ---[ 620]---> BDD-cost:  572
c ---[ 619]---> BDD-cost:  572
c ---[ 618]---> BDD-cost:  564
c ---[ 617]---> BDD-cost:  564
c ---[ 616]---> BDD-cost:  564
c ---[ 608]---> BDD-cost:  555
c ---[ 607]---> BDD-cost: 1076
c ---[ 606]---> BDD-cost: 1076
c ---[ 605]---> BDD-cost: 1076
c ---[ 604]---> BDD-cost: 1066
c ---[ 603]---> BDD-cost: 1066
c ---[ 602]---> BDD-cost: 1066
c ---[ 601]---> BDD-cost: 1055
c ---[ 600]---> BDD-cost: 1037
c ---[ 599]---> BDD-cost: 1038
c ---[ 598]---> BDD-cost: 1020
c ---[ 597]---> BDD-cost: 1002
c ---[ 596]---> BDD-cost:  978
c ---[ 595]---> BDD-cost:  978
c ---[ 593]---> BDD-cost: 2375
c ---[ 592]---> BDD-cost: 3690
c ---[ 591]---> BDD-cost: 3690
c ---[ 590]---> BDD-cost: 3691
c ---[ 589]---> BDD-cost: 3667
c ---[ 588]---> BDD-cost: 3667
c ---[ 587]---> BDD-cost: 3667
c ---[ 586]---> BDD-cost: 3632
c ---[ 585]---> BDD-cost: 3588
c ---[ 584]---> BDD-cost: 3588
c ---[ 583]---> BDD-cost: 3521
c ---[ 582]---> BDD-cost: 3444
c ---[ 581]---> BDD-cost: 3334
c ---[ 580]---> BDD-cost: 3334
c ---[ 578]---> BDD-cost: 2901
c ---[ 577]---> BDD-cost: 6541
c ---[ 576]---> BDD-cost: 6541
c ---[ 575]---> BDD-cost: 6541
c ---[ 574]---> BDD-cost: 6514
c ---[ 573]---> BDD-cost: 6514
c ---[ 572]---> BDD-cost: 6514
c ---[ 571]---> BDD-cost: 6484
c ---[ 570]---> BDD-cost: 6433
c ---[ 569]---> BDD-cost: 6433
c ---[ 568]---> BDD-cost: 6376
c ---[ 567]---> BDD-cost: 6274
c ---[ 566]---> BDD-cost: 6162
c ---[ 565]---> BDD-cost: 6162
c ---[ 563]---> BDD-cost: 3448
c ---[ 562]---> BDD-cost: 7617
c ---[ 561]---> BDD-cost: 7617
c ---[ 560]---> BDD-cost: 7617
c ---[ 559]---> BDD-cost: 7596
c ---[ 558]---> BDD-cost: 7596
c ---[ 557]---> BDD-cost: 7596
c ---[ 556]---> BDD-cost: 7557
c ---[ 555]---> BDD-cost: 7515
c ---[ 554]---> BDD-cost: 7515
c ---[ 553]---> BDD-cost: 7433
c ---[ 552]---> BDD-cost: 7348
c ---[ 551]---> BDD-cost: 7224
c ---[ 550]---> BDD-cost: 7187
c ---[ 548]---> BDD-cost:    3
c ---[ 547]---> BDD-cost:    6
c ---[ 546]---> BDD-cost:  784
c ---[ 545]---> BDD-cost:  764
c ---[ 544]---> BDD-cost:  801
c ---[ 543]---> BDD-cost:  801
c ---[ 542]---> BDD-cost: 1004
c ---[ 541]---> BDD-cost: 1000
c ---[ 540]---> BDD-cost: 1004
c ---[ 539]---> BDD-cost: 1000
c ---[ 538]---> BDD-cost: 1629
c ---[ 537]---> BDD-cost: 1586
c ---[ 536]---> BDD-cost: 1242
c ---[ 535]---> BDD-cost: 1978
c ---[ 534]---> BDD-cost: 1538
c ---[ 533]---> BDD-cost: 1529
c ---[ 532]---> BDD-cost: 1534
c ---[ 531]---> BDD-cost:    6
c ---[ 530]---> BDD-cost:    6
c ---[ 529]---> BDD-cost:    4
c ---[ 528]---> BDD-cost:    5
c ---[ 527]---> BDD-cost:    5
c ---[ 526]---> BDD-cost:    5
c ---[ 525]---> BDD-cost:    6
c ---[ 524]---> BDD-cost:    5
c ---[ 523]---> BDD-cost:    5
c ---[ 522]---> BDD-cost:    6
c ---[ 521]---> BDD-cost:    7
c ---[ 520]---> BDD-cost:    7
c ---[ 519]---> BDD-cost:    6
c ---[ 518]---> BDD-cost:    3
c ---[ 517]---> BDD-cost:    6
c ---[ 516]---> BDD-cost:    5
c ---[ 515]---> BDD-cost:    5
c ---[ 514]---> BDD-cost:    3
c ---[ 513]---> BDD-cost:    6
c ---[ 512]---> BDD-cost:    5
c ---[ 511]---> BDD-cost:    3
c ---[ 510]---> BDD-cost:  579
c ---[ 509]---> BDD-cost:  623
c ---[ 508]---> BDD-cost:  615
c ---[ 507]---> BDD-cost:  391
c ---[ 506]---> BDD-cost:  345
c ---[ 505]---> BDD-cost:  539
c ---[ 504]---> BDD-cost:  635
c ---[ 503]---> BDD-cost:  647
c ---[ 502]---> BDD-cost:  345
c ---[ 501]---> BDD-cost: 1123
c ---[ 500]---> BDD-cost: 1024
c ---[ 499]---> BDD-cost:  812
c ---[ 498]---> BDD-cost:  859
c ---[ 497]---> BDD-cost:  797
c ---[ 496]---> BDD-cost: 1218
c ---[ 495]---> BDD-cost:  871
c ---[ 494]---> BDD-cost:  922
c ---[ 493]---> BDD-cost:  559
c ---[ 492]---> BDD-cost:  868
c ---[ 491]---> BDD-cost:  556
c ---[ 490]---> BDD-cost:  920
c ---[ 489]---> BDD-cost:  512
c ---[ 488]---> BDD-cost: 1042
c ---[ 487]---> BDD-cost: 1038
c ---[ 486]---> BDD-cost: 1715
c ---[ 485]---> BDD-cost: 1038
c ---[ 484]---> BDD-cost: 1739
c ---[ 483]---> BDD-cost: 1712
c ---[ 482]---> BDD-cost: 1033
c ---[ 481]---> BDD-cost: 1721
c ---[ 480]---> BDD-cost: 1045
c ---[ 479]---> BDD-cost: 1029
c ---[ 478]---> BDD-cost: 1246
c ---[ 477]---> BDD-cost:  755
c ---[ 476]---> BDD-cost:  705
c ---[ 475]---> BDD-cost:  959
c ---[ 474]---> BDD-cost: 1169
c ---[ 473]---> BDD-cost: 1241
c ---[ 472]---> BDD-cost:  755
c ---[ 471]---> BDD-cost:  702
c ---[ 470]---> BDD-cost: 1238
c ---[ 469]---> BDD-cost:  702
c ---[ 468]---> BDD-cost:  702
c ---[ 467]---> BDD-cost: 1703
c ---[ 466]---> BDD-cost: 1292
c ---[ 465]---> BDD-cost: 2715
c ---[ 464]---> BDD-cost: 2136
c ---[ 463]---> BDD-cost: 2136
c ---[ 462]---> BDD-cost: 1292
c ---[ 461]---> BDD-cost: 2124
c ---[ 460]---> BDD-cost: 1288
c ---[ 459]---> BDD-cost:  987
c ---[ 458]---> BDD-cost:  925
c ---[ 457]---> BDD-cost: 3909
c ---[ 456]---> BDD-cost: 3734
c ---[ 455]---> BDD-cost: 2108
c ---[ 454]---> BDD-cost:  925
c ---[ 453]---> BDD-cost: 3163
c ---[ 452]---> BDD-cost: 2547
c ---[ 451]---> BDD-cost: 1523
c ---[ 450]---> BDD-cost:  925
c ---[ 449]---> BDD-cost: 2066
c ---[ 448]---> BDD-cost: 2341
c ---[ 447]---> BDD-cost: 3287
c ---[ 446]---> BDD-cost: 1585
c ---[ 445]---> BDD-cost: 3299
c ---[ 444]---> BDD-cost: 2618
c ---[ 443]---> BDD-cost: 1596
c ---[ 442]---> BDD-cost: 1585
c ---[ 441]---> BDD-cost: 3282
c ---[ 440]---> BDD-cost: 2613
c ---[ 439]---> BDD-cost: 1591
c ---[ 438]---> BDD-cost: 1572
c ---[ 437]---> BDD-cost: 3291
c ---[ 436]---> BDD-cost: 2622
c ---[ 435]---> BDD-cost: 1596
c ---[ 434]---> BDD-cost: 1581
c ---[ 433]---> BDD-cost:    4
c ---[ 432]---> BDD-cost:    6
c ---[ 431]---> BDD-cost:    2
c ---[ 430]---> BDD-cost:    6
c ---[ 429]---> BDD-cost:   12
c ---[ 428]---> BDD-cost:    4
c ---[ 427]---> BDD-cost:    5
c ---[ 426]---> BDD-cost:    5
c ---[ 425]---> BDD-cost:    3
c ---[ 424]---> BDD-cost:    5
c ---[ 423]---> BDD-cost:    3
c ---[ 422]---> BDD-cost:    6
c ---[ 421]---> BDD-cost:    6
c ---[ 420]---> BDD-cost:    3
c ---[ 419]---> BDD-cost:    4
c ---[ 418]---> BDD-cost:    4
c ---[ 417]---> BDD-cost:    5
c ---[ 416]---> BDD-cost:    7
c ---[ 415]---> BDD-cost:    4
c ---[ 414]---> BDD-cost:    2
c ---[ 413]---> BDD-cost:    7
c ---[ 412]---> BDD-cost:   11
c ---[ 411]---> BDD-cost:    5
c ---[ 410]---> BDD-cost:    3
c ---[ 409]---> BDD-cost:    4
c ---[ 408]---> BDD-cost:    8
c ---[ 407]---> BDD-cost:   10
c ---[ 406]---> BDD-cost:    4
c ---[ 405]---> BDD-cost:    5
c ---[ 404]---> BDD-cost:  530
c ---[ 403]---> BDD-cost:  399
c ---[ 402]---> BDD-cost:  408
c ---[ 401]---> BDD-cost:  391
c ---[ 400]---> BDD-cost:  606
c ---[ 399]---> BDD-cost:  401
c ---[ 398]---> BDD-cost:  399
c ---[ 397]---> BDD-cost:  391
c ---[ 396]---> BDD-cost:  382
c ---[ 395]---> BDD-cost: 1003
c ---[ 394]---> BDD-cost: 1227
c ---[ 393]---> BDD-cost:  832
c ---[ 392]---> BDD-cost:  836
c ---[ 391]---> BDD-cost:  836
c ---[ 390]---> BDD-cost:  786
c ---[ 389]---> BDD-cost: 1112
c ---[ 388]---> BDD-cost: 1326
c ---[ 387]---> BDD-cost:  825
c ---[ 386]---> BDD-cost:  789
c ---[ 385]---> BDD-cost:  762
c ---[ 384]---> BDD-cost:  583
c ---[ 383]---> BDD-cost:  572
c ---[ 382]---> BDD-cost:  759
c ---[ 381]---> BDD-cost:  580
c ---[ 380]---> BDD-cost:  569
c ---[ 379]---> BDD-cost:  821
c ---[ 378]---> BDD-cost:  587
c ---[ 377]---> BDD-cost:  583
c ---[ 376]---> BDD-cost:  572
c ---[ 375]---> BDD-cost:  559
c ---[ 374]---> BDD-cost: 1191
c ---[ 373]---> BDD-cost:  917
c ---[ 372]---> BDD-cost:  569
c ---[ 371]---> BDD-cost:  556
c ---[ 370]---> BDD-cost: 1623
c ---[ 369]---> BDD-cost: 1096
c ---[ 368]---> BDD-cost: 1081
c ---[ 367]---> BDD-cost: 1033
c ---[ 366]---> BDD-cost: 1557
c ---[ 365]---> BDD-cost: 1931
c ---[ 364]---> BDD-cost: 1600
c ---[ 363]---> BDD-cost: 1077
c ---[ 362]---> BDD-cost: 1029
c ---[ 361]---> BDD-cost: 1927
c ---[ 360]---> BDD-cost: 1605
c ---[ 359]---> BDD-cost: 1077
c ---[ 358]---> BDD-cost: 1029
c ---[ 357]---> BDD-cost: 1000
c ---[ 356]---> BDD-cost: 1081
c ---[ 355]---> BDD-cost: 1038
c ---[ 354]---> BDD-cost: 1564
c ---[ 353]---> BDD-cost: 1934
c ---[ 352]---> BDD-cost: 1077
c ---[ 351]---> BDD-cost: 1012
c ---[ 350]---> BDD-cost: 1627
c ---[ 349]---> BDD-cost: 1238
c ---[ 348]---> BDD-cost:  772
c ---[ 347]---> BDD-cost: 1355
c ---[ 346]---> BDD-cost: 1643
c ---[ 345]---> BDD-cost: 1076
c ---[ 344]---> BDD-cost: 1065
c ---[ 343]---> BDD-cost: 1042
c ---[ 342]---> BDD-cost: 1021
c ---[ 341]---> BDD-cost: 1021
c ---[ 340]---> BDD-cost:  789
c ---[ 339]---> BDD-cost:  772
c ---[ 338]---> BDD-cost: 1027
c ---[ 337]---> BDD-cost:  795
c ---[ 336]---> BDD-cost:  789
c ---[ 335]---> BDD-cost:  772
c ---[ 334]---> BDD-cost:  755
c ---[ 333]---> BDD-cost: 1584
c ---[ 332]---> BDD-cost: 1238
c ---[ 331]---> BDD-cost:  772
c ---[ 330]---> BDD-cost:  755
c ---[ 329]---> BDD-cost: 2484
c ---[ 328]---> BDD-cost: 1648
c ---[ 327]---> BDD-cost: 2144
c ---[ 326]---> BDD-cost: 2120
c ---[ 325]---> BDD-cost: 1338
c ---[ 324]---> BDD-cost: 1278
c ---[ 323]---> BDD-cost: 1242
c ---[ 322]---> BDD-cost: 1338
c ---[ 321]---> BDD-cost: 1292
c ---[ 320]---> BDD-cost: 1912
c ---[ 319]---> BDD-cost: 1338
c ---[ 318]---> BDD-cost: 1221
c ---[ 317]---> BDD-cost: 1908
c ---[ 316]---> BDD-cost: 1334
c ---[ 315]---> BDD-cost: 2096
c ---[ 314]---> BDD-cost: 1609
c ---[ 313]---> BDD-cost: 1609
c ---[ 312]---> BDD-cost: 1037
c ---[ 311]---> BDD-cost: 1008
c ---[ 310]---> BDD-cost: 5792
c ---[ 309]---> BDD-cost: 6223
c ---[ 308]---> BDD-cost: 4011
c ---[ 307]---> BDD-cost: 3868
c ---[ 306]---> BDD-cost: 1609
c ---[ 305]---> BDD-cost: 1031
c ---[ 304]---> BDD-cost: 1008
c ---[ 303]---> BDD-cost:  987
c ---[ 302]---> BDD-cost: 1670
c ---[ 301]---> BDD-cost: 1635
c ---[ 300]---> BDD-cost: 1606
c ---[ 299]---> BDD-cost: 1528
c ---[ 298]---> BDD-cost: 1609
c ---[ 297]---> BDD-cost: 1008
c ---[ 296]---> BDD-cost:  987
c ---[ 295]---> BDD-cost: 4008
c ---[ 294]---> BDD-cost: 2986
c ---[ 293]---> BDD-cost: 2002
c ---[ 292]---> BDD-cost: 1928
c ---[ 291]---> BDD-cost: 3299
c ---[ 290]---> BDD-cost: 2440
c ---[ 289]---> BDD-cost: 2618
c ---[ 288]---> BDD-cost: 1651
c ---[ 287]---> BDD-cost: 1596
c ---[ 286]---> BDD-cost: 1577
c ---[ 285]---> BDD-cost: 1534
c ---[ 284]---> BDD-cost: 2644
c ---[ 283]---> BDD-cost: 2607
c ---[ 282]---> BDD-cost: 1651
c ---[ 281]---> BDD-cost: 1596
c ---[ 280]---> BDD-cost: 2640
c ---[ 279]---> BDD-cost: 2325
c ---[ 278]---> BDD-cost: 1651
c ---[ 277]---> BDD-cost: 2623
c ---[ 276]---> BDD-cost: 2320
c ---[ 275]---> BDD-cost: 1646
c ---[ 274]---> BDD-cost: 2632
c ---[ 273]---> BDD-cost: 2325
c ---[ 272]---> BDD-cost: 1651
c ---[ 271]---> BDD-cost:    5
c ---[ 270]---> BDD-cost:    2
c ---[ 269]---> BDD-cost:    1
c ---[ 268]---> BDD-cost:    4
c ---[ 267]---> BDD-cost:    2
c ---[ 266]---> BDD-cost:    5
c ---[ 265]---> BDD-cost:    1
c ---[ 264]---> BDD-cost:    5
c ---[ 263]---> BDD-cost:    2
c ---[ 262]---> BDD-cost:    5
c ---[ 261]---> BDD-cost:  612
c ---[ 260]---> BDD-cost:  356
c ---[ 259]---> BDD-cost: 1242
c ---[ 258]---> BDD-cost:  523
c ---[ 257]---> BDD-cost:  898
c ---[ 256]---> BDD-cost:  756
c ---[ 255]---> BDD-cost:  868
c ---[ 254]---> BDD-cost:    1
c ---[ 253]---> BDD-cost:  759
c ---[ 252]---> BDD-cost:  865
c ---[ 251]---> BDD-cost:  584
c ---[ 250]---> BDD-cost:  580
c ---[ 249]---> BDD-cost: 1438
c ---[ 248]---> BDD-cost: 1596
c ---[ 247]---> BDD-cost: 1721
c ---[ 246]---> BDD-cost: 1721
c ---[ 245]---> BDD-cost: 1096
c ---[ 244]---> BDD-cost: 1717
c ---[ 243]---> BDD-cost: 1557
c ---[ 242]---> BDD-cost: 1927
c ---[ 241]---> BDD-cost: 1609
c ---[ 240]---> BDD-cost: 1605
c ---[ 239]---> BDD-cost: 1545
c ---[ 238]---> BDD-cost: 1539
c ---[ 237]---> BDD-cost: 1169
c ---[ 236]---> BDD-cost: 1021
c ---[ 235]---> BDD-cost: 1163
c ---[ 234]---> BDD-cost:  789
c ---[ 233]---> BDD-cost: 2215
c ---[ 232]---> BDD-cost: 2949
c ---[ 231]---> BDD-cost: 2670
c ---[ 230]---> BDD-cost: 1912
c ---[ 229]---> BDD-cost: 2379
c ---[ 228]---> BDD-cost: 1988
c ---[ 227]---> BDD-cost: 1270
c ---[ 226]---> BDD-cost: 1242
c ---[ 225]---> BDD-cost: 2379
c ---[ 224]---> BDD-cost: 1988
c ---[ 223]---> BDD-cost: 1270
c ---[ 222]---> BDD-cost: 1234
c ---[ 221]---> BDD-cost: 2375
c ---[ 220]---> BDD-cost: 2128
c ---[ 219]---> BDD-cost: 1270
c ---[ 218]---> BDD-cost: 1708
c ---[ 217]---> BDD-cost: 5393
c ---[ 216]---> BDD-cost: 5788
c ---[ 215]---> BDD-cost: 5985
c ---[ 214]---> BDD-cost: 3631
c ---[ 213]---> BDD-cost: 2046
c ---[ 212]---> BDD-cost: 1516
c ---[ 211]---> BDD-cost: 3087
c ---[ 210]---> BDD-cost: 2389
c ---[ 209]---> BDD-cost: 1695
c ---[ 208]---> BDD-cost: 1498
c ---[ 207]---> BDD-cost: 2772
c ---[ 206]---> BDD-cost: 1048
c ---[ 205]---> BDD-cost: 1031
c ---[ 204]---> BDD-cost:  932
c ---[ 203]---> BDD-cost: 2850
c ---[ 202]---> BDD-cost: 3533
c ---[ 201]---> BDD-cost: 3219
c ---[ 200]---> BDD-cost: 2618
c ---[ 199]---> BDD-cost: 1534
c ---[ 198]---> BDD-cost: 2897
c ---[ 197]---> BDD-cost: 2432
c ---[ 196]---> BDD-cost: 1685
c ---[ 195]---> BDD-cost: 2892
c ---[ 194]---> BDD-cost: 2427
c ---[ 193]---> BDD-cost: 1676
c ---[ 192]---> BDD-cost: 2897
c ---[ 191]---> BDD-cost: 2436
c ---[ 190]---> BDD-cost: 1681
c ---[ 189]---> BDD-cost:   13
c ---[ 188]---> BDD-cost:   10
c ---[ 187]---> BDD-cost: 1239
c ---[ 186]---> BDD-cost: 1189
c ---[ 185]---> BDD-cost:  581
c ---[ 184]---> BDD-cost:  509
c ---[ 183]---> BDD-cost: 1150
c ---[ 182]---> BDD-cost: 1186
c ---[ 181]---> BDD-cost:  584
c ---[ 180]---> BDD-cost:    1
c ---[ 179]---> BDD-cost: 1434
c ---[ 178]---> BDD-cost: 1605
c ---[ 177]---> BDD-cost: 1553
c ---[ 176]---> BDD-cost: 1430
c ---[ 175]---> BDD-cost: 1430
c ---[ 174]---> BDD-cost: 1169
c ---[ 173]---> BDD-cost:  783
c ---[ 172]---> BDD-cost: 2071
c ---[ 171]---> BDD-cost: 1550
c ---[ 170]---> BDD-cost:  795
c ---[ 169]---> BDD-cost: 1098
c ---[ 168]---> BDD-cost: 1214
c ---[ 167]---> BDD-cost: 1733
c ---[ 166]---> BDD-cost: 2379
c ---[ 165]---> BDD-cost: 2685
c ---[ 164]---> BDD-cost: 1980
c ---[ 163]---> BDD-cost:    1
c ---[ 162]---> BDD-cost: 2509
c ---[ 161]---> BDD-cost: 2116
c ---[ 160]---> BDD-cost:    1
c ---[ 159]---> BDD-cost: 4113
c ---[ 158]---> BDD-cost: 1702
c ---[ 157]---> BDD-cost: 1042
c ---[ 156]---> BDD-cost: 2470
c ---[ 155]---> BDD-cost: 1702
c ---[ 154]---> BDD-cost: 2096
c ---[ 153]---> BDD-cost: 2105
c ---[ 152]---> BDD-cost: 2640
c ---[ 151]---> BDD-cost: 2897
c ---[ 150]---> BDD-cost: 1681
c ---[ 149]---> BDD-cost: 2325
c ---[ 148]---> BDD-cost: 2432
c ---[ 147]---> BDD-cost:  636
c ---[ 146]---> BDD-cost:  498
c ---[ 145]---> BDD-cost:  914
c ---[ 144]---> BDD-cost: 1092
c ---[ 143]---> BDD-cost: 2017
c ---[ 142]---> BDD-cost: 1602
c ---[ 141]---> BDD-cost: 1539
c ---[ 140]---> BDD-cost: 1584
c ---[ 139]---> BDD-cost: 1211
c ---[ 138]---> BDD-cost: 2374
c ---[ 137]---> BDD-cost: 2482
c ---[ 136]---> BDD-cost: 1904
c ---[ 135]---> BDD-cost: 1354
c ---[ 134]---> BDD-cost: 1354
c ---[ 133]---> BDD-cost: 2723
c ---[ 132]---> BDD-cost:   18
c ---[ 131]---> BDD-cost:  475
c ---[ 130]---> BDD-cost: 5065
c ---[ 129]---> BDD-cost: 2148
c ---[ 128]---> BDD-cost: 1853
c ---[ 127]---> BDD-cost:    2
c ---[ 126]---> BDD-cost: 2897
c ---[ 125]---> BDD-cost:    1
c ---[ 124]---> BDD-cost:    9
c ---[ 123]---> BDD-cost:    8
c ---[ 122]---> BDD-cost:    7
c ---[ 121]---> BDD-cost:  806
c ---[ 120]---> BDD-cost: 1213
c ---[ 119]---> BDD-cost: 1494
c ---[ 118]---> BDD-cost: 1224
c ---[ 117]---> BDD-cost:  348
c ---[ 116]---> BDD-cost: 1183
c ---[ 115]---> BDD-cost:  895
c ---[ 114]---> BDD-cost: 1147
c ---[ 113]---> BDD-cost: 1210
c ---[ 112]---> BDD-cost: 1557
c ---[ 111]---> BDD-cost: 1927
c ---[ 110]---> BDD-cost: 1755
c ---[ 109]---> BDD-cost: 1592
c ---[ 108]---> BDD-cost: 1592
c ---[ 107]---> BDD-cost: 1578
c ---[ 106]---> BDD-cost:  789
c ---[ 105]---> BDD-cost: 1762
c ---[ 104]---> BDD-cost: 1762
c ---[ 103]---> BDD-cost: 1762
c ---[ 102]---> BDD-cost: 1976
c ---[ 101]---> BDD-cost: 1976
c ---[ 100]---> BDD-cost:  788
c ---[  99]---> BDD-cost: 2086
c ---[  98]---> BDD-cost: 1983
c ---[  97]---> BDD-cost:   53
c ---[  96]---> BDD-cost:   22
c ---[  95]---> BDD-cost:   22
c ---[  94]---> BDD-cost:   22
c ---[  93]---> BDD-cost:    2
c ---[  92]---> BDD-cost:   22
c ---[  91]---> BDD-cost:    7
c ---[  90]---> BDD-cost:   10
c ---[  89]---> BDD-cost:    6
c ---[  88]---> BDD-cost:   10
c ---[  87]---> BDD-cost:    1
c ---[  86]---> BDD-cost:    1
c ---[  85]---> BDD-cost: 2156
c ---[  84]---> BDD-cost: 1980
c ---[  83]---> BDD-cost:   28
c ---[  82]---> BDD-cost:    1
c ---[  81]---> BDD-cost: 1983
c ---[  80]---> BDD-cost:    2
c ---[  79]---> BDD-cost: 2663
c ---[  78]---> BDD-cost:    2
c ---[  77]---> BDD-cost:    4
c ---[  76]---> BDD-cost:    7
c ---[  75]---> BDD-cost:    9
c ---[  74]---> BDD-cost:    9
c ---[  73]---> BDD-cost:  813
c ---[  72]---> BDD-cost:   14
c ---[  71]---> BDD-cost:   18
c ---[  70]---> BDD-cost: 1592
c ---[  69]---> BDD-cost: 1558
c ---[  68]---> BDD-cost: 1232
c ---[  67]---> BDD-cost:    2
c ---[  66]---> BDD-cost:   22
c ---[  65]---> BDD-cost: 1523
c ---[  64]---> BDD-cost: 1523
c ---[  63]---> BDD-cost:    1
c ---[  62]---> BDD-cost:  849
c ---[  61]---> BDD-cost:  343
c ---[  60]---> BDD-cost: 1320
c ---[  59]---> BDD-cost: 1205
c ---[  58]---> BDD-cost:    1
c ---[  57]---> BDD-cost: 1916
c ---[  56]---> BDD-cost: 1518
c ---[  55]---> BDD-cost:    5
c ---[  54]---> BDD-cost:    9
c ---[  53]---> BDD-cost:    1
c ---[  52]---> BDD-cost: 2166
c ---[  51]---> BDD-cost:  807
c ---[  50]---> BDD-cost:  986
c ---[  49]---> BDD-cost:  233
c ---[  48]---> BDD-cost:  711
c ---[  47]---> BDD-cost:  747
c ---[  46]---> BDD-cost:  378
c ---[  45]---> BDD-cost:  521
c ---[  44]---> BDD-cost:  532
c ---[  43]---> BDD-cost:  490
c ---[  42]---> BDD-cost:  225
c ---[  41]---> BDD-cost:  544
c ---[  40]---> BDD-cost:    7
c ---[  39]---> BDD-cost:    8
c ---[  38]---> BDD-cost:   10
c ---[  37]---> BDD-cost:   47
c ---[  36]---> BDD-cost:  460
c ---[  35]---> BDD-cost:    2
c ---[  34]---> BDD-cost:  501
c ---[  33]---> BDD-cost:  276
c ---[  32]---> BDD-cost:    4
c ---[  31]---> BDD-cost:   18
c ---[  30]---> BDD-cost:  813
c ---[  29]---> BDD-cost:  387
c ---[  28]---> BDD-cost:  644
c ---[  27]---> BDD-cost:   22
c ---[  26]---> BDD-cost:  923
c ---[  25]---> BDD-cost:  278
c ---[  24]---> BDD-cost:   63
c ---[  23]---> BDD-cost:  881
c ---[  22]---> BDD-cost:   13
c ---[  21]---> BDD-cost:   13
c ---[  20]---> BDD-cost:   12
c ---[  19]---> BDD-cost:   17
c ---[  18]---> BDD-cost:  562
c ---[  17]---> BDD-cost:  554
c ---[  16]---> BDD-cost:  543
c ---[  15]---> BDD-cost:  528
c ---[  14]---> BDD-cost:  499
c ---[  13]---> BDD-cost:  458
c ---[  12]---> BDD-cost:  279
c ---[  11]---> BDD-cost:  204
c ---[  10]---> BDD-cost:  545
c ---[   9]---> BDD-cost:  545
c ---[   8]---> BDD-cost:  534
c ---[   7]---> BDD-cost:  512
c ---[   6]---> BDD-cost:  499
c ---[   5]---> BDD-cost:  342
c ---[   4]---> BDD-cost:  231
c ---[   3]---> BDD-cost:  737
c ---[   2]---> BDD-cost: 2600
c ---[   1]---> BDD-cost: 5681
c ---[   0]---> BDD-cost: 6629
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 | 3229928  9413141 | 1076642       0        0     nan |  0.000 % |
c |       100 | 3229912  9413096 | 1184306      96      405     4.2 |  0.333 % |
c |       250 | 3229872  9412988 | 1302736     240      976     4.1 |  0.334 % |
c |       475 | 3229787  9412757 | 1433010     452     1895     4.2 |  0.337 % |
c |       812 | 3229761  9412687 | 1576311     783     4502     5.7 |  0.338 % |
c |      1318 | 3229761  9412687 | 1733942    1289    15478    12.0 |  0.338 % |
c |      2077 | 3229733  9412613 | 1907336    2043    24132    11.8 |  0.339 % |
c |      3216 | 3229717  9412581 | 2098070    3173    40827    12.9 |  0.339 % |
c |      4924 | 3229679  9412500 | 2307877    4863    71711    14.7 |  0.341 % |
c |      7487 | 3229613  9412338 | 2538665    7407   124236    16.8 |  0.343 % |
c |     11331 | 3229611  9412334 | 2792532   11250   196740    17.5 |  0.343 % |
c |     17098 | 3229601  9412314 | 3071785   17012   357291    21.0 |  0.344 % |
c |     25747 | 3229601  9412314 | 3378963   25661   551636    21.5 |  0.344 % |
c |     38724 | 3229543  9412175 | 3716860   38611   830527    21.5 |  0.346 % |
c |     58185 | 3229536  9412161 | 4088546   58071  1637590    28.2 |  0.346 % |
c |     87379 | 3229536  9412161 | 4497400   87265  2560784    29.3 |  0.346 % |
c |    131169 | 3229536  9412161 | 4947140  131055  4521494    34.5 |  0.346 % |
c |    196853 | 3229536  9412161 | 5441854  196739  7567660    38.5 |  0.346 % |
c |    295380 | 3229525  9412136 | 5986040  295259 12818956    43.4 |  0.346 % |
#### 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): 1.04 1.20 1.08 2/54 23743
Raw data (stat): 23743 (runsolver) R 23742 32461 32460 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 481746173 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0002 s]
Raw data (loadavg): 1.03 1.19 1.08 2/54 23743
Raw data (stat): 23743 (minisat+) R 23742 32461 32460 0 -1 0 33692 0 1 0 904 90 0 0 25 0 1 0 481746173 157835264 30859 4294967295 134512640 134672761 3221224528 3221220720 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38534 30860 603 41 0 38493 0
vsize: 154136
[startup+20.0009 s]
Raw data (loadavg): 1.03 1.18 1.08 2/54 23743
Raw data (stat): 23743 (minisat+) R 23742 32461 32460 0 -1 0 97382 0 1 0 1751 243 0 0 25 0 1 0 481746173 470007808 94549 4294967295 134512640 134672761 3221224528 3221171952 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 114748 94550 603 41 0 114707 0
vsize: 458992
[startup+30.0007 s]
Raw data (loadavg): 1.02 1.18 1.08 2/54 23743
Raw data (stat): 23743 (minisat+) R 23742 32461 32460 0 -1 0 98547 0 1 0 2748 246 0 0 25 0 1 0 481746173 474472448 95714 4294967295 134512640 134672761 3221224528 3221223520 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 115838 95714 603 41 0 115797 0
vsize: 463352
[startup+40.0004 s]
Raw data (loadavg): 1.02 1.17 1.08 2/54 23743
Raw data (stat): 23743 (minisat+) R 23742 32461 32460 0 -1 0 98791 0 1 0 3747 247 0 0 25 0 1 0 481746173 475553792 95958 4294967295 134512640 134672761 3221224528 3221223700 134556685 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 116102 95958 603 41 0 116061 0
vsize: 464408
[startup+50.0016 s]
Raw data (loadavg): 1.01 1.16 1.08 2/54 23743
Raw data (stat): 23743 (minisat+) R 23742 32461 32460 0 -1 0 99177 0 1 0 4745 249 0 0 25 0 1 0 481746173 476905472 96344 4294967295 134512640 134672761 3221224528 3221223696 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 116432 96344 603 41 0 116391 0
vsize: 465728
[startup+60.002 s]
Raw data (loadavg): 1.01 1.16 1.08 2/54 23743
Raw data (stat): 23743 (minisat+) R 23742 32461 32460 0 -1 0 99450 0 1 0 5745 250 0 0 25 0 1 0 481746173 477847552 96617 4294967295 134512640 134672761 3221224528 3221223700 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 116662 96617 603 41 0 116621 0
vsize: 466648
[startup+70.0028 s]
Raw data (loadavg): 1.01 1.15 1.08 2/54 23743
Raw data (stat): 23743 (minisat+) R 23742 32461 32460 0 -1 0 99450 0 1 0 6745 250 0 0 25 0 1 0 481746173 477847552 96617 4294967295 134512640 134672761 3221224528 3221223700 134556685 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 116662 96617 603 41 0 116621 0
vsize: 466648
[startup+80.0036 s]
Raw data (loadavg): 1.01 1.15 1.08 2/54 23743
Raw data (stat): 23743 (minisat+) R 23742 32461 32460 0 -1 0 99763 0 1 0 7744 251 0 0 25 0 1 0 481746173 478928896 96930 4294967295 134512640 134672761 3221224528 3221223700 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 116926 96930 603 41 0 116885 0
vsize: 467704
[startup+90.0033 s]
Raw data (loadavg): 1.01 1.14 1.07 2/54 23743
Raw data (stat): 23743 (minisat+) R 23742 32461 32460 0 -1 0 99878 0 1 0 8743 252 0 0 25 0 1 0 481746173 479469568 97045 4294967295 134512640 134672761 3221224528 3221223700 134556660 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 117058 97045 603 41 0 117017 0
vsize: 468232
[startup+100.004 s]
Raw data (loadavg): 1.00 1.14 1.07 2/54 23743
Raw data (stat): 23743 (minisat+) R 23742 32461 32460 0 -1 0 99991 0 1 0 9743 252 0 0 25 0 1 0 481746173 479875072 97158 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 117157 97158 603 41 0 117116 0
vsize: 468628
[startup+110.005 s]
Raw data (loadavg): 1.00 1.13 1.07 2/54 23743
Raw data (stat): 23743 (minisat+) R 23742 32461 32460 0 -1 0 100234 0 1 0 10742 253 0 0 25 0 1 0 481746173 480952320 97401 4294967295 134512640 134672761 3221224528 3221223676 134560552 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 117420 97401 603 41 0 117379 0
vsize: 469680
[startup+120.007 s]
Raw data (loadavg): 1.00 1.13 1.07 2/54 23743
Raw data (stat): 23743 (minisat+) R 23742 32461 32460 0 -1 0 100455 0 1 0 11741 254 0 0 25 0 1 0 481746173 481849344 97622 4294967295 134512640 134672761 3221224528 3221223696 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 117639 97622 603 41 0 117598 0
vsize: 470556
[startup+130.007 s]
Raw data (loadavg): 1.00 1.12 1.07 2/54 23743
Raw data (stat): 23743 (minisat+) R 23742 32461 32460 0 -1 0 100583 0 1 0 12740 255 0 0 25 0 1 0 481746173 482381824 97750 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 117769 97750 603 41 0 117728 0
vsize: 471076
[startup+140.006 s]
Raw data (loadavg): 1.00 1.12 1.07 2/54 23743
Raw data (stat): 23743 (minisat+) R 23742 32461 32460 0 -1 0 100686 0 1 0 13740 256 0 0 25 0 1 0 481746173 482783232 97853 4294967295 134512640 134672761 3221224528 3221223696 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 117867 97853 603 41 0 117826 0
vsize: 471468
[startup+150.007 s]
Raw data (loadavg): 1.00 1.11 1.07 2/54 23743
Raw data (stat): 23743 (minisat+) R 23742 32461 32460 0 -1 0 100757 0 1 0 14740 256 0 0 25 0 1 0 481746173 483053568 97924 4294967295 134512640 134672761 3221224528 3221223632 134555179 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 117933 97924 603 41 0 117892 0
vsize: 471732
[startup+160.007 s]
Raw data (loadavg): 1.00 1.11 1.07 2/54 23743
Raw data (stat): 23743 (minisat+) R 23742 32461 32460 0 -1 0 100866 0 1 0 15740 256 0 0 25 0 1 0 481746173 483454976 98033 4294967295 134512640 134672761 3221224528 3221223700 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 118031 98033 603 41 0 117990 0
vsize: 472124
[startup+170.008 s]
Raw data (loadavg): 1.00 1.11 1.07 2/54 23743
Raw data (stat): 23743 (minisat+) R 23742 32461 32460 0 -1 0 101085 0 1 0 16740 257 0 0 25 0 1 0 481746173 484265984 98252 4294967295 134512640 134672761 3221224528 3221223696 134560942 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 118229 98252 603 41 0 118188 0
vsize: 472916
[startup+180.008 s]
Raw data (loadavg): 1.00 1.10 1.07 2/54 23743
Raw data (stat): 23743 (minisat+) R 23742 32461 32460 0 -1 0 101245 0 1 0 17739 258 0 0 25 0 1 0 481746173 485064704 98412 4294967295 134512640 134672761 3221224528 3221223728 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 118424 98412 603 41 0 118383 0
vsize: 473696
[startup+190.009 s]
Raw data (loadavg): 1.00 1.10 1.06 2/54 23743
Raw data (stat): 23743 (minisat+) R 23742 32461 32460 0 -1 0 101372 0 1 0 18739 258 0 0 25 0 1 0 481746173 485470208 98539 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 118523 98539 603 41 0 118482 0
vsize: 474092
[startup+200.01 s]
Raw data (loadavg): 1.00 1.09 1.06 2/54 23743
Raw data (stat): 23743 (minisat+) R 23742 32461 32460 0 -1 0 101467 0 1 0 19738 259 0 0 25 0 1 0 481746173 485867520 98634 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 118620 98634 603 41 0 118579 0
vsize: 474480
[startup+210.011 s]
Raw data (loadavg): 1.00 1.09 1.06 2/54 23743
Raw data (stat): 23743 (minisat+) R 23742 32461 32460 0 -1 0 101506 0 1 0 20738 260 0 0 25 0 1 0 481746173 486002688 98673 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 118653 98673 603 41 0 118612 0
vsize: 474612
[startup+220.012 s]
Raw data (loadavg): 1.00 1.09 1.06 2/54 23743
Raw data (stat): 23743 (minisat+) R 23742 32461 32460 0 -1 0 101613 0 1 0 21738 260 0 0 25 0 1 0 481746173 486535168 98780 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 118783 98780 603 41 0 118742 0
vsize: 475132
[startup+230.012 s]
Raw data (loadavg): 1.00 1.08 1.06 2/54 23743
Raw data (stat): 23743 (minisat+) R 23742 32461 32460 0 -1 0 101739 0 1 0 22737 260 0 0 25 0 1 0 481746173 486940672 98906 4294967295 134512640 134672761 3221224528 3221223696 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 118882 98906 603 41 0 118841 0
vsize: 475528
[startup+240.011 s]
Raw data (loadavg): 1.00 1.08 1.06 2/54 23743
Raw data (stat): 23743 (minisat+) R 23742 32461 32460 0 -1 0 101895 0 1 0 23737 261 0 0 25 0 1 0 481746173 487608320 99062 4294967295 134512640 134672761 3221224528 3221223728 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 119045 99062 603 41 0 119004 0
vsize: 476180
[startup+250.012 s]
Raw data (loadavg): 1.00 1.08 1.06 2/54 23743
Raw data (stat): 23743 (minisat+) R 23742 32461 32460 0 -1 0 102099 0 1 0 24736 262 0 0 25 0 1 0 481746173 488419328 99266 4294967295 134512640 134672761 3221224528 3221223664 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 119243 99266 603 41 0 119202 0
vsize: 476972
[startup+260.013 s]
Raw data (loadavg): 1.00 1.07 1.06 2/54 23743
Raw data (stat): 23743 (minisat+) R 23742 32461 32460 0 -1 0 102278 0 1 0 25736 262 0 0 25 0 1 0 481746173 489091072 99445 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 119407 99445 603 41 0 119366 0
vsize: 477628
[startup+270.013 s]
Raw data (loadavg): 1.00 1.07 1.06 2/54 23743
Raw data (stat): 23743 (minisat+) R 23742 32461 32460 0 -1 0 102491 0 1 0 26736 263 0 0 25 0 1 0 481746173 490024960 99658 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 119635 99658 603 41 0 119594 0
vsize: 478540
[startup+280.013 s]
Raw data (loadavg): 1.00 1.07 1.06 2/54 23743
Raw data (stat): 23743 (minisat+) R 23742 32461 32460 0 -1 0 102760 0 1 0 27734 264 0 0 25 0 1 0 481746173 491352064 99927 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 119959 99927 603 41 0 119918 0
vsize: 479836
[startup+290.014 s]
Raw data (loadavg): 1.00 1.07 1.06 2/54 23743
Raw data (stat): 23743 (minisat+) R 23742 32461 32460 0 -1 0 102990 0 1 0 28733 266 0 0 25 0 1 0 481746173 492318720 100157 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 120195 100157 603 41 0 120154 0
vsize: 480780
[startup+300.015 s]
Raw data (loadavg): 1.00 1.06 1.05 2/54 23743
Raw data (stat): 23743 (minisat+) R 23742 32461 32460 0 -1 0 103160 0 1 0 29733 267 0 0 25 0 1 0 481746173 493006848 100327 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 120363 100327 603 41 0 120322 0
vsize: 481452
[startup+310.015 s]
Raw data (loadavg): 1.00 1.06 1.05 2/54 23743
Raw data (stat): 23743 (minisat+) R 23742 32461 32460 0 -1 0 103705 0 1 0 30731 268 0 0 25 0 1 0 481746173 495153152 100872 4294967295 134512640 134672761 3221224528 3221223632 134559760 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 120887 100872 603 41 0 120846 0
vsize: 483548
[startup+320.016 s]
Raw data (loadavg): 1.00 1.06 1.05 2/54 23743
Raw data (stat): 23743 (minisat+) R 23742 32461 32460 0 -1 0 103985 0 1 0 31730 269 0 0 25 0 1 0 481746173 496234496 101152 4294967295 134512640 134672761 3221224528 3221223696 134560988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 121151 101152 603 41 0 121110 0
vsize: 484604
[startup+330.017 s]
Raw data (loadavg): 1.00 1.06 1.05 2/54 23743
Raw data (stat): 23743 (minisat+) R 23742 32461 32460 0 -1 0 104362 0 1 0 32729 271 0 0 25 0 1 0 481746173 497827840 101529 4294967295 134512640 134672761 3221224528 3221223696 134560852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 121540 101529 603 41 0 121499 0
vsize: 486160
[startup+340.017 s]
Raw data (loadavg): 1.00 1.05 1.05 2/54 23743
Raw data (stat): 23743 (minisat+) R 23742 32461 32460 0 -1 0 104574 0 1 0 33728 271 0 0 25 0 1 0 481746173 498630656 101741 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 121736 101741 603 41 0 121695 0
vsize: 486944
[startup+350.018 s]
Raw data (loadavg): 1.00 1.05 1.05 2/54 23743
Raw data (stat): 23743 (minisat+) R 23742 32461 32460 0 -1 0 104729 0 1 0 34728 272 0 0 25 0 1 0 481746173 499298304 101896 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 121899 101896 603 41 0 121858 0
vsize: 487596
[startup+360.025 s]
Raw data (loadavg): 1.00 1.05 1.05 2/54 23743
Raw data (stat): 23743 (minisat+) R 23742 32461 32460 0 -1 0 104995 0 1 0 35728 273 0 0 25 0 1 0 481746173 500375552 102162 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 122162 102162 603 41 0 122121 0
vsize: 488648
[startup+370.025 s]
Raw data (loadavg): 1.00 1.05 1.05 2/54 23743
Raw data (stat): 23743 (minisat+) R 23742 32461 32460 0 -1 0 105118 0 1 0 36727 275 0 0 25 0 1 0 481746173 500903936 102285 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 122291 102285 603 41 0 122250 0
vsize: 489164
[startup+380.027 s]
Raw data (loadavg): 1.00 1.05 1.05 2/54 23743
Raw data (stat): 23743 (minisat+) R 23742 32461 32460 0 -1 0 105220 0 1 0 37727 275 0 0 25 0 1 0 481746173 501313536 102387 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 122391 102387 603 41 0 122350 0
vsize: 489564
[startup+390.027 s]
Raw data (loadavg): 1.00 1.04 1.05 2/54 23743
Raw data (stat): 23743 (minisat+) R 23742 32461 32460 0 -1 0 105314 0 1 0 38726 276 0 0 25 0 1 0 481746173 501719040 102481 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 122490 102481 603 41 0 122449 0
vsize: 489960
[startup+400.028 s]
Raw data (loadavg): 1.00 1.04 1.04 2/54 23743
Raw data (stat): 23743 (minisat+) R 23742 32461 32460 0 -1 0 105397 0 1 0 39725 277 0 0 25 0 1 0 481746173 501989376 102564 4294967295 134512640 134672761 3221224528 3221223696 134560988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 122556 102564 603 41 0 122515 0
vsize: 490224
[startup+410.028 s]
Raw data (loadavg): 1.00 1.04 1.04 2/54 23743
Raw data (stat): 23743 (minisat+) R 23742 32461 32460 0 -1 0 105510 0 1 0 40725 277 0 0 25 0 1 0 481746173 502525952 102677 4294967295 134512640 134672761 3221224528 3221223696 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 122687 102677 603 41 0 122646 0
vsize: 490748
[startup+420.028 s]
Raw data (loadavg): 1.00 1.04 1.04 2/54 23743
Raw data (stat): 23743 (minisat+) R 23742 32461 32460 0 -1 0 105609 0 1 0 41725 277 0 0 25 0 1 0 481746173 502796288 102776 4294967295 134512640 134672761 3221224528 3221223664 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 122753 102776 603 41 0 122712 0
vsize: 491012
[startup+430.029 s]
Raw data (loadavg): 1.00 1.04 1.04 2/54 23743
Raw data (stat): 23743 (minisat+) R 23742 32461 32460 0 -1 0 105731 0 1 0 42725 278 0 0 25 0 1 0 481746173 503328768 102898 4294967295 134512640 134672761 3221224528 3221223664 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 122883 102898 603 41 0 122842 0
vsize: 491532
[startup+440.029 s]
Raw data (loadavg): 1.00 1.03 1.04 2/54 23743
Raw data (stat): 23743 (minisat+) R 23742 32461 32460 0 -1 0 105807 0 1 0 43725 278 0 0 25 0 1 0 481746173 503730176 102974 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 122981 102974 603 41 0 122940 0
vsize: 491924
[startup+450.03 s]
Raw data (loadavg): 1.00 1.03 1.04 2/54 23743
Raw data (stat): 23743 (minisat+) R 23742 32461 32460 0 -1 0 105901 0 1 0 44724 279 0 0 25 0 1 0 481746173 503996416 103068 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 123046 103068 603 41 0 123005 0
vsize: 492184
[startup+460.03 s]
Raw data (loadavg): 1.00 1.03 1.04 2/54 23743
Raw data (stat): 23743 (minisat+) R 23742 32461 32460 0 -1 0 105993 0 1 0 45724 279 0 0 25 0 1 0 481746173 504397824 103160 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 123144 103160 603 41 0 123103 0
vsize: 492576
[startup+470.032 s]
Raw data (loadavg): 1.00 1.03 1.04 2/54 23743
Raw data (stat): 23743 (minisat+) R 23742 32461 32460 0 -1 0 106108 0 1 0 46723 280 0 0 25 0 1 0 481746173 505462784 103275 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 123404 103275 603 41 0 123363 0
vsize: 493616
[startup+480.032 s]
Raw data (loadavg): 1.00 1.03 1.04 2/54 23743
Raw data (stat): 23743 (minisat+) R 23742 32461 32460 0 -1 0 106385 0 1 0 47722 281 0 0 25 0 1 0 481746173 506540032 103552 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 123667 103552 603 41 0 123626 0
vsize: 494668
[startup+490.033 s]
Raw data (loadavg): 1.00 1.03 1.04 2/54 23743
Raw data (stat): 23743 (minisat+) R 23742 32461 32460 0 -1 0 106631 0 1 0 48721 282 0 0 25 0 1 0 481746173 507506688 103798 4294967295 134512640 134672761 3221224528 3221223664 134560673 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 123903 103798 603 41 0 123862 0
vsize: 495612
[startup+500.034 s]
Raw data (loadavg): 1.00 1.03 1.03 2/54 23743
Raw data (stat): 23743 (minisat+) R 23742 32461 32460 0 -1 0 106843 0 1 0 49720 283 0 0 25 0 1 0 481746173 508350464 104010 4294967295 134512640 134672761 3221224528 3221223696 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 124109 104010 603 41 0 124068 0
vsize: 496436
[startup+510.033 s]
Raw data (loadavg): 1.00 1.02 1.03 2/54 23743
Raw data (stat): 23743 (minisat+) R 23742 32461 32460 0 -1 0 107018 0 1 0 50720 284 0 0 25 0 1 0 481746173 509038592 104185 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 124277 104185 603 41 0 124236 0
vsize: 497108
[startup+520.034 s]
Raw data (loadavg): 1.00 1.02 1.03 2/54 23743
Raw data (stat): 23743 (minisat+) R 23742 32461 32460 0 -1 0 107197 0 1 0 51719 285 0 0 25 0 1 0 481746173 509894656 104364 4294967295 134512640 134672761 3221224528 3221223632 134560504 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 124486 104364 603 41 0 124445 0
vsize: 497944
[startup+530.034 s]
Raw data (loadavg): 1.00 1.02 1.03 2/54 23743
Raw data (stat): 23743 (minisat+) R 23742 32461 32460 0 -1 0 107430 0 1 0 52718 286 0 0 25 0 1 0 481746173 510828544 104597 4294967295 134512640 134672761 3221224528 3221223652 134566047 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 124714 104597 603 41 0 124673 0
vsize: 498856
[startup+540.034 s]
Raw data (loadavg): 1.00 1.02 1.03 2/54 23743
Raw data (stat): 23743 (minisat+) R 23742 32461 32460 0 -1 0 107604 0 1 0 53718 287 0 0 25 0 1 0 481746173 511500288 104771 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 124878 104771 603 41 0 124837 0
vsize: 499512
[startup+550.034 s]
Raw data (loadavg): 1.00 1.02 1.03 2/54 23743
Raw data (stat): 23743 (minisat+) R 23742 32461 32460 0 -1 0 108008 0 1 0 54717 288 0 0 25 0 1 0 481746173 513232896 105175 4294967295 134512640 134672761 3221224528 3221223664 134560677 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125301 105175 603 41 0 125260 0
vsize: 501204
[startup+560.037 s]
Raw data (loadavg): 1.00 1.02 1.03 2/54 23743
Raw data (stat): 23743 (minisat+) R 23742 32461 32460 0 -1 0 108639 0 1 0 55715 290 0 0 25 0 1 0 481746173 515792896 105806 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125926 105806 603 41 0 125885 0
vsize: 503704
[startup+570.038 s]
Raw data (loadavg): 1.00 1.02 1.03 2/54 23743
Raw data (stat): 23743 (minisat+) R 23742 32461 32460 0 -1 0 109141 0 1 0 56714 291 0 0 25 0 1 0 481746173 517791744 106308 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 126414 106308 603 41 0 126373 0
vsize: 505656
[startup+580.04 s]
Raw data (loadavg): 1.00 1.02 1.03 2/54 23743
Raw data (stat): 23743 (minisat+) R 23742 32461 32460 0 -1 0 109544 0 1 0 57713 292 0 0 25 0 1 0 481746173 519393280 106711 4294967295 134512640 134672761 3221224528 3221223696 134560867 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 126805 106711 603 41 0 126764 0
vsize: 507220
[startup+590.04 s]
Raw data (loadavg): 1.00 1.02 1.03 2/54 23743
Raw data (stat): 23743 (minisat+) R 23742 32461 32460 0 -1 0 109918 0 1 0 58712 294 0 0 25 0 1 0 481746173 521007104 107085 4294967295 134512640 134672761 3221224528 3221223632 134560510 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 127199 107085 603 41 0 127158 0
vsize: 508796
[startup+600.047 s]
Raw data (loadavg): 1.00 1.02 1.02 2/54 23743
Raw data (stat): 23743 (minisat+) R 23742 32461 32460 0 -1 0 110006 0 1 0 59712 294 0 0 25 0 1 0 481746173 521273344 107173 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 127264 107173 603 41 0 127223 0
vsize: 509056
[startup+610.151 s]
Raw data (loadavg): 1.00 1.02 1.02 2/54 23743
Raw data (stat): 23743 (minisat+) R 23742 32461 32460 0 -1 0 110076 0 1 0 60723 294 0 0 25 0 1 0 481746173 521543680 107243 4294967295 134512640 134672761 3221224528 3221223696 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 127330 107243 603 41 0 127289 0
vsize: 509320
[startup+620.153 s]
Raw data (loadavg): 1.00 1.01 1.02 2/54 23743
Raw data (stat): 23743 (minisat+) R 23742 32461 32460 0 -1 0 110315 0 1 0 61722 295 0 0 25 0 1 0 481746173 522489856 107482 4294967295 134512640 134672761 3221224528 3221223712 134558662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 127561 107482 603 41 0 127520 0
vsize: 510244
[startup+630.153 s]
Raw data (loadavg): 1.00 1.01 1.02 2/54 23743
Raw data (stat): 23743 (minisat+) R 23742 32461 32460 0 -1 0 110440 0 1 0 62722 295 0 0 25 0 1 0 481746173 523030528 107607 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 127693 107607 603 41 0 127652 0
vsize: 510772
[startup+640.171 s]
Raw data (loadavg): 1.00 1.01 1.02 2/54 23743
Raw data (stat): 23743 (minisat+) R 23742 32461 32460 0 -1 0 110579 0 1 0 63723 296 0 0 25 0 1 0 481746173 523563008 107746 4294967295 134512640 134672761 3221224528 3221223696 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 127823 107746 603 41 0 127782 0
vsize: 511292
[startup+650.191 s]
Raw data (loadavg): 1.00 1.01 1.02 2/54 23743
Raw data (stat): 23743 (minisat+) R 23742 32461 32460 0 -1 0 110725 0 1 0 64725 296 0 0 25 0 1 0 481746173 524099584 107892 4294967295 134512640 134672761 3221224528 3221223728 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 127954 107892 603 41 0 127913 0
vsize: 511816
[startup+660.195 s]
Raw data (loadavg): 1.00 1.01 1.02 2/54 23743
Raw data (stat): 23743 (minisat+) R 23742 32461 32460 0 -1 0 110843 0 1 0 65726 297 0 0 25 0 1 0 481746173 524492800 108010 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 128050 108010 603 41 0 128009 0
vsize: 512200
[startup+670.196 s]
Raw data (loadavg): 1.00 1.01 1.02 2/54 23743
Raw data (stat): 23743 (minisat+) R 23742 32461 32460 0 -1 0 110888 0 1 0 66726 297 0 0 25 0 1 0 481746173 524763136 108055 4294967295 134512640 134672761 3221224528 3221223664 134560688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 128116 108055 603 41 0 128075 0
vsize: 512464
[startup+680.202 s]
Raw data (loadavg): 1.00 1.01 1.02 2/54 23743
Raw data (stat): 23743 (minisat+) R 23742 32461 32460 0 -1 0 110931 0 1 0 67726 297 0 0 25 0 1 0 481746173 524898304 108098 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 128149 108098 603 41 0 128108 0
vsize: 512596
[startup+690.201 s]
Raw data (loadavg): 1.00 1.01 1.02 2/54 23743
Raw data (stat): 23743 (minisat+) R 23742 32461 32460 0 -1 0 111085 0 1 0 68726 298 0 0 25 0 1 0 481746173 525582336 108252 4294967295 134512640 134672761 3221224528 3221223696 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 128316 108252 603 41 0 128275 0
vsize: 513264
[startup+700.202 s]
Raw data (loadavg): 1.00 1.01 1.02 2/54 23743
Raw data (stat): 23743 (minisat+) R 23742 32461 32460 0 -1 0 111224 0 1 0 69725 298 0 0 25 0 1 0 481746173 526114816 108391 4294967295 134512640 134672761 3221224528 3221223696 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 128446 108391 603 41 0 128405 0
vsize: 513784
[startup+710.203 s]
Raw data (loadavg): 1.00 1.01 1.01 2/54 23743
Raw data (stat): 23743 (minisat+) R 23742 32461 32460 0 -1 0 111373 0 1 0 70725 299 0 0 25 0 1 0 481746173 526651392 108540 4294967295 134512640 134672761 3221224528 3221223728 134557852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 128577 108540 603 41 0 128536 0
vsize: 514308
[startup+720.204 s]
Raw data (loadavg): 1.00 1.00 1.01 2/54 23743
Raw data (stat): 23743 (minisat+) R 23742 32461 32460 0 -1 0 111626 0 1 0 71724 300 0 0 25 0 1 0 481746173 527716352 108793 4294967295 134512640 134672761 3221224528 3221223728 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 128837 108793 603 41 0 128796 0
vsize: 515348
[startup+730.204 s]
Raw data (loadavg): 1.00 1.00 1.01 2/54 23743
Raw data (stat): 23743 (minisat+) R 23742 32461 32460 0 -1 0 111867 0 1 0 72724 301 0 0 25 0 1 0 481746173 528662528 109034 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 129068 109034 603 41 0 129027 0
vsize: 516272
[startup+740.203 s]
Raw data (loadavg): 1.00 1.00 1.01 2/54 23743
Raw data (stat): 23743 (minisat+) R 23742 32461 32460 0 -1 0 112122 0 1 0 73722 302 0 0 25 0 1 0 481746173 529739776 109289 4294967295 134512640 134672761 3221224528 3221223664 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 129331 109289 603 41 0 129290 0
vsize: 517324
[startup+750.204 s]
Raw data (loadavg): 1.00 1.00 1.01 2/54 23743
Raw data (stat): 23743 (minisat+) R 23742 32461 32460 0 -1 0 112356 0 1 0 74721 303 0 0 25 0 1 0 481746173 530673664 109523 4294967295 134512640 134672761 3221224528 3221223596 1075346600 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 129559 109523 603 41 0 129518 0
vsize: 518236
[startup+760.204 s]
Raw data (loadavg): 1.00 1.00 1.01 2/54 23743
Raw data (stat): 23743 (minisat+) R 23742 32461 32460 0 -1 0 112631 0 1 0 75721 304 0 0 25 0 1 0 481746173 531750912 109798 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 129822 109798 603 41 0 129781 0
vsize: 519288
[startup+770.206 s]
Raw data (loadavg): 1.00 1.00 1.01 2/54 23743
Raw data (stat): 23743 (minisat+) R 23742 32461 32460 0 -1 0 112967 0 1 0 76720 305 0 0 25 0 1 0 481746173 533090304 110134 4294967295 134512640 134672761 3221224528 3221223696 134561190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 130149 110134 603 41 0 130108 0
vsize: 520596
[startup+780.206 s]
Raw data (loadavg): 1.00 1.00 1.01 2/54 23743
Raw data (stat): 23743 (minisat+) R 23742 32461 32460 0 -1 0 113307 0 1 0 77720 306 0 0 25 0 1 0 481746173 534429696 110474 4294967295 134512640 134672761 3221224528 3221223544 1075352992 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 130476 110474 603 41 0 130435 0
vsize: 521904
[startup+790.205 s]
Raw data (loadavg): 1.00 1.00 1.01 2/54 23743
Raw data (stat): 23743 (minisat+) R 23742 32461 32460 0 -1 0 113644 0 1 0 78719 307 0 0 25 0 1 0 481746173 535908352 110811 4294967295 134512640 134672761 3221224528 3221223696 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 130837 110811 603 41 0 130796 0
vsize: 523348
[startup+800.206 s]
Raw data (loadavg): 1.00 1.00 1.01 2/54 23743
Raw data (stat): 23743 (minisat+) R 23742 32461 32460 0 -1 0 113954 0 1 0 79718 308 0 0 25 0 1 0 481746173 538173440 111121 4294967295 134512640 134672761 3221224528 3221223696 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 131390 111121 603 41 0 131349 0
vsize: 525560
[startup+810.207 s]
Raw data (loadavg): 1.00 1.00 1.00 2/54 23743
Raw data (stat): 23743 (minisat+) R 23742 32461 32460 0 -1 0 114264 0 1 0 80716 310 0 0 25 0 1 0 481746173 539394048 111431 4294967295 134512640 134672761 3221224528 3221223632 134560224 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 131688 111431 603 41 0 131647 0
vsize: 526752
[startup+820.208 s]
Raw data (loadavg): 1.00 1.00 1.00 2/54 23743
Raw data (stat): 23743 (minisat+) R 23742 32461 32460 0 -1 0 114512 0 1 0 81715 311 0 0 25 0 1 0 481746173 540467200 111679 4294967295 134512640 134672761 3221224528 3221223696 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 131950 111679 603 41 0 131909 0
vsize: 527800
[startup+830.208 s]
Raw data (loadavg): 1.00 1.00 1.00 2/54 23743
Raw data (stat): 23743 (minisat+) R 23742 32461 32460 0 -1 0 114780 0 1 0 82715 312 0 0 25 0 1 0 481746173 541564928 111947 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 132218 111947 603 41 0 132177 0
vsize: 528872
[startup+840.208 s]
Raw data (loadavg): 1.00 1.00 1.00 2/54 23743
Raw data (stat): 23743 (minisat+) R 23742 32461 32460 0 -1 0 115023 0 1 0 83714 312 0 0 25 0 1 0 481746173 542519296 112190 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 132451 112190 603 41 0 132410 0
vsize: 529804
[startup+850.209 s]
Raw data (loadavg): 1.00 1.00 1.00 2/54 23743
Raw data (stat): 23743 (minisat+) R 23742 32461 32460 0 -1 0 115263 0 1 0 84714 313 0 0 25 0 1 0 481746173 543457280 112430 4294967295 134512640 134672761 3221224528 3221223728 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 132680 112430 603 41 0 132639 0
vsize: 530720
[startup+860.209 s]
Raw data (loadavg): 1.00 1.00 1.00 2/54 23743
Raw data (stat): 23743 (minisat+) R 23742 32461 32460 0 -1 0 115505 0 1 0 85714 313 0 0 25 0 1 0 481746173 544534528 112672 4294967295 134512640 134672761 3221224528 3221223696 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 132943 112672 603 41 0 132902 0
vsize: 531772
[startup+870.21 s]
Raw data (loadavg): 1.00 1.00 1.00 2/54 23743
Raw data (stat): 23743 (minisat+) R 23742 32461 32460 0 -1 0 115737 0 1 0 86713 314 0 0 25 0 1 0 481746173 545341440 112904 4294967295 134512640 134672761 3221224528 3221223484 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 133140 112904 603 41 0 133099 0
vsize: 532560
[startup+880.21 s]
Raw data (loadavg): 1.00 1.00 1.00 2/54 23743
Raw data (stat): 23743 (minisat+) R 23742 32461 32460 0 -1 0 115964 0 1 0 87712 315 0 0 25 0 1 0 481746173 546308096 113131 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 133376 113131 603 41 0 133335 0
vsize: 533504
[startup+890.211 s]
Raw data (loadavg): 1.00 1.00 1.00 2/54 23743
Raw data (stat): 23743 (minisat+) R 23742 32461 32460 0 -1 0 116210 0 1 0 88712 316 0 0 25 0 1 0 481746173 547389440 113377 4294967295 134512640 134672761 3221224528 3221223696 134561375 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 133640 113377 603 41 0 133599 0
vsize: 534560
[startup+900.211 s]
Raw data (loadavg): 1.00 1.00 1.00 2/54 23743
Raw data (stat): 23743 (minisat+) R 23742 32461 32460 0 -1 0 116365 0 1 0 89711 317 0 0 25 0 1 0 481746173 548061184 113532 4294967295 134512640 134672761 3221224528 3221223696 134560797 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 133804 113532 603 41 0 133763 0
vsize: 535216
[startup+910.212 s]
Raw data (loadavg): 1.00 1.00 1.00 2/54 23743
Raw data (stat): 23743 (minisat+) R 23742 32461 32460 0 -1 0 116478 0 1 0 90710 317 0 0 25 0 1 0 481746173 548462592 113645 4294967295 134512640 134672761 3221224528 3221223664 134560703 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 133902 113645 603 41 0 133861 0
vsize: 535608
[startup+920.213 s]
Raw data (loadavg): 1.00 1.00 1.00 2/54 23743
Raw data (stat): 23743 (minisat+) R 23742 32461 32460 0 -1 0 116582 0 1 0 91709 318 0 0 25 0 1 0 481746173 548868096 113749 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 134001 113749 603 41 0 133960 0
vsize: 536004
[startup+930.212 s]
Raw data (loadavg): 1.00 1.00 1.00 2/54 23743
Raw data (stat): 23743 (minisat+) R 23742 32461 32460 0 -1 0 116664 0 1 0 92709 318 0 0 25 0 1 0 481746173 549265408 113831 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 134098 113831 603 41 0 134057 0
vsize: 536392
[startup+940.212 s]
Raw data (loadavg): 1.00 1.00 1.00 2/54 23743
Raw data (stat): 23743 (minisat+) R 23742 32461 32460 0 -1 0 116729 0 1 0 93709 319 0 0 25 0 1 0 481746173 549531648 113896 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 134163 113896 603 41 0 134122 0
vsize: 536652
[startup+950.213 s]
Raw data (loadavg): 1.00 1.00 1.00 2/54 23743
Raw data (stat): 23743 (minisat+) R 23742 32461 32460 0 -1 0 116792 0 1 0 94709 319 0 0 25 0 1 0 481746173 549666816 113959 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 134196 113959 603 41 0 134155 0
vsize: 536784
[startup+960.214 s]
Raw data (loadavg): 1.00 1.00 1.00 2/54 23743
Raw data (stat): 23743 (minisat+) R 23742 32461 32460 0 -1 0 116860 0 1 0 95709 319 0 0 25 0 1 0 481746173 549933056 114027 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 134261 114027 603 41 0 134220 0
vsize: 537044
[startup+970.221 s]
Raw data (loadavg): 1.00 1.00 1.00 2/54 23743
Raw data (stat): 23743 (minisat+) R 23742 32461 32460 0 -1 0 116932 0 1 0 96709 319 0 0 25 0 1 0 481746173 550334464 114099 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 134359 114099 603 41 0 134318 0
vsize: 537436
[startup+980.23 s]
Raw data (loadavg): 1.00 1.00 1.00 2/54 23743
Raw data (stat): 23743 (minisat+) R 23742 32461 32460 0 -1 0 117002 0 1 0 97710 320 0 0 25 0 1 0 481746173 550608896 114169 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 134426 114169 603 41 0 134385 0
vsize: 537704
[startup+990.23 s]
Raw data (loadavg): 1.00 1.00 1.00 2/54 23743
Raw data (stat): 23743 (minisat+) R 23742 32461 32460 0 -1 0 117068 0 1 0 98710 320 0 0 25 0 1 0 481746173 550879232 114235 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 134492 114235 603 41 0 134451 0
vsize: 537968
[startup+1000.23 s]
Raw data (loadavg): 1.00 1.00 1.00 2/54 23743
Raw data (stat): 23743 (minisat+) R 23742 32461 32460 0 -1 0 117143 0 1 0 99710 320 0 0 25 0 1 0 481746173 551174144 114310 4294967295 134512640 134672761 3221224528 3221223632 134559887 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 134564 114310 603 41 0 134523 0
vsize: 538256
[startup+1010.23 s]
Raw data (loadavg): 1.00 1.00 1.00 2/54 23743
Raw data (stat): 23743 (minisat+) R 23742 32461 32460 0 -1 0 117213 0 1 0 100710 320 0 0 25 0 1 0 481746173 551440384 114380 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 134629 114380 603 41 0 134588 0
vsize: 538516
[startup+1020.23 s]
Raw data (loadavg): 1.00 1.00 1.00 2/54 23743
Raw data (stat): 23743 (minisat+) R 23742 32461 32460 0 -1 0 117289 0 1 0 101711 320 0 0 25 0 1 0 481746173 551710720 114456 4294967295 134512640 134672761 3221224528 3221223632 134560287 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 134695 114456 603 41 0 134654 0
vsize: 538780
[startup+1030.23 s]
Raw data (loadavg): 1.00 1.00 1.00 2/54 23743
Raw data (stat): 23743 (minisat+) R 23742 32461 32460 0 -1 0 117376 0 1 0 102710 321 0 0 25 0 1 0 481746173 552116224 114543 4294967295 134512640 134672761 3221224528 3221223696 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 134794 114543 603 41 0 134753 0
vsize: 539176
[startup+1040.23 s]
Raw data (loadavg): 1.00 1.00 1.00 2/54 23743
Raw data (stat): 23743 (minisat+) R 23742 32461 32460 0 -1 0 117456 0 1 0 103710 321 0 0 25 0 1 0 481746173 552382464 114623 4294967295 134512640 134672761 3221224528 3221223728 134557800 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 134859 114623 603 41 0 134818 0
vsize: 539436
[startup+1050.23 s]
Raw data (loadavg): 1.00 1.00 1.00 2/54 23743
Raw data (stat): 23743 (minisat+) R 23742 32461 32460 0 -1 0 117530 0 1 0 104711 321 0 0 25 0 1 0 481746173 552652800 114697 4294967295 134512640 134672761 3221224528 3221223664 134560688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 134925 114697 603 41 0 134884 0
vsize: 539700
[startup+1060.23 s]
Raw data (loadavg): 1.00 1.00 1.00 2/54 23743
Raw data (stat): 23743 (minisat+) R 23742 32461 32460 0 -1 0 117601 0 1 0 105710 321 0 0 25 0 1 0 481746173 552935424 114768 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 134994 114768 603 41 0 134953 0
vsize: 539976
[startup+1070.23 s]
Raw data (loadavg): 1.00 1.00 1.00 2/54 23743
Raw data (stat): 23743 (minisat+) R 23742 32461 32460 0 -1 0 117682 0 1 0 106710 322 0 0 25 0 1 0 481746173 553340928 114849 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 135093 114849 603 41 0 135052 0
vsize: 540372
[startup+1080.23 s]
Raw data (loadavg): 1.00 1.00 1.00 2/54 23743
Raw data (stat): 23743 (minisat+) R 23742 32461 32460 0 -1 0 117753 0 1 0 107710 322 0 0 25 0 1 0 481746173 553611264 114920 4294967295 134512640 134672761 3221224528 3221223696 134560876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 135159 114920 603 41 0 135118 0
vsize: 540636
[startup+1090.23 s]
Raw data (loadavg): 1.00 1.00 1.00 2/54 23743
Raw data (stat): 23743 (minisat+) R 23742 32461 32460 0 -1 0 117827 0 1 0 108710 322 0 0 25 0 1 0 481746173 553881600 114994 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 135225 114994 603 41 0 135184 0
vsize: 540900
[startup+1100.23 s]
Raw data (loadavg): 1.00 1.00 1.00 2/54 23743
Raw data (stat): 23743 (minisat+) R 23742 32461 32460 0 -1 0 117915 0 1 0 109710 323 0 0 25 0 1 0 481746173 554344448 115082 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 135338 115082 603 41 0 135297 0
vsize: 541352
[startup+1110.23 s]
Raw data (loadavg): 1.00 1.00 1.00 2/54 23743
Raw data (stat): 23743 (minisat+) R 23742 32461 32460 0 -1 0 117967 0 1 0 110710 323 0 0 25 0 1 0 481746173 554475520 115134 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 135370 115134 603 41 0 135329 0
vsize: 541480
[startup+1120.24 s]
Raw data (loadavg): 1.00 1.00 1.00 2/54 23743
Raw data (stat): 23743 (minisat+) R 23742 32461 32460 0 -1 0 118033 0 1 0 111710 323 0 0 25 0 1 0 481746173 554737664 115200 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 135434 115200 603 41 0 135393 0
vsize: 541736
[startup+1130.24 s]
Raw data (loadavg): 1.00 1.00 1.00 2/54 23743
Raw data (stat): 23743 (minisat+) R 23742 32461 32460 0 -1 0 118107 0 1 0 112710 323 0 0 25 0 1 0 481746173 555081728 115274 4294967295 134512640 134672761 3221224528 3221223696 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 135518 115274 603 41 0 135477 0
vsize: 542072
[startup+1140.24 s]
Raw data (loadavg): 1.00 1.00 1.00 2/54 23743
Raw data (stat): 23743 (minisat+) R 23742 32461 32460 0 -1 0 118161 0 1 0 113711 323 0 0 25 0 1 0 481746173 555347968 115328 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 135583 115328 603 41 0 135542 0
vsize: 542332
[startup+1150.24 s]
Raw data (loadavg): 1.00 1.00 1.00 2/54 23743
Raw data (stat): 23743 (minisat+) R 23742 32461 32460 0 -1 0 118221 0 1 0 114711 324 0 0 25 0 1 0 481746173 555479040 115388 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 135615 115388 603 41 0 135574 0
vsize: 542460
[startup+1160.24 s]
Raw data (loadavg): 1.00 1.00 1.00 2/54 23743
Raw data (stat): 23743 (minisat+) R 23742 32461 32460 0 -1 0 118287 0 1 0 115711 324 0 0 25 0 1 0 481746173 555749376 115454 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 135681 115454 603 41 0 135640 0
vsize: 542724
[startup+1170.25 s]
Raw data (loadavg): 1.00 1.00 1.00 2/54 23743
Raw data (stat): 23743 (minisat+) R 23742 32461 32460 0 -1 0 118353 0 1 0 116711 324 0 0 25 0 1 0 481746173 556019712 115520 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 135747 115520 603 41 0 135706 0
vsize: 542988
[startup+1180.24 s]
Raw data (loadavg): 1.00 1.00 1.00 2/54 23743
Raw data (stat): 23743 (minisat+) R 23742 32461 32460 0 -1 0 118417 0 1 0 117710 324 0 0 25 0 1 0 481746173 556290048 115584 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 135813 115584 603 41 0 135772 0
vsize: 543252
[startup+1190.24 s]
Raw data (loadavg): 1.00 1.00 1.00 2/54 23743
Raw data (stat): 23743 (minisat+) R 23742 32461 32460 0 -1 0 118471 0 1 0 118710 325 0 0 25 0 1 0 481746173 556560384 115638 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 135879 115638 603 41 0 135838 0
vsize: 543516
[startup+1200.25 s]
Raw data (loadavg): 1.00 1.00 1.00 2/54 23743
Raw data (stat): 23743 (minisat+) R 23742 32461 32460 0 -1 0 118522 0 1 0 119711 325 0 0 25 0 1 0 481746173 556695552 115689 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 135912 115689 603 41 0 135871 0
vsize: 543648
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.48 s]
Raw data (loadavg): 1.00 1.00 1.00 1/54 23743
Raw data (stat): 23743 (minisat+) Z 23742 32461 32460 0 -1 12 118524 0 1 0 119711 348 0 0 25 0 1 0 481746173 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 0
Real time (s): 1200.48
CPU time (s): 1200.59
CPU user time (s): 1197.11
CPU system time (s): 3.48247
CPU usage (%): 100.01
Max. virtual memory (Kb): 543648
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####