PB'05 competition: run trace

Some explanations

A solver is run under the control of another program named runsolver. runsolver is in charge of imposing the CPU time limit and the memory limit to the solver. It also monitors some information about the process. The trace of the execution of a solver is divided in four parts:
LAUNCHER DATA
These informations are related to the script which will launch the solver. The most important informations are the command line given to the solver, the md5sum of the different files and the dump of the /proc/cpuinfo and /proc/meminfo which provide some useful information on the computer.
SOLVER DATA
This is the output of the solver (stdout and stderr).
WATCHER DATA
This is the informations gathered by the runsolver program. It first prints the different limits. There's a first limit on CPU time set to 1200 seconds. After this time has ellapsed, runsolver sends a SIGTERM and 2 seconds later a SIGKILL to the solver. For safety, there's also another limit set to 1230 seconds which will send a SIGXPU to the solver. The last limit is on the virtual memory used by the process (900Mb).
Every ten seconds, the runsolver process fetches the content of /proc/loadavg, /proc/pid/stat and /proc/pid/statm (see man proc) and prints it as raw data. This is only recorded in case we need to investigate the behaviour of a solver. The memory used by the solver (vsize) is also given every ten seconds.
When the solver exits, runsolver prints some informations such as status and time. CPU usage is the ratio CPU Time/Real Time.
VERIFIER DATA
The output of the solver is piped to a verifier program which will search a value line "v " and, if found, will check that the given interpretation satisfies all constraints.
General information on the benchmark

Name	normalized-opb/web/www.ps.uni-sb.de/~walser/benchmarks/course-ass/normalized-ws97-3.opb
MD5SUM	77c89bda49ebcdc0428e1292512864a9
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	3080
Optimality of the best value was proved	NO
Number of terms in the objective function	2792
Biggest coefficient in the objective function	1000
Number of bits for the biggest coefficient in the objective function	10
Sum of the numbers in the objective function	1385986
Number of bits of the sum of numbers in the objective function	21
Biggest number in a constraint	1000
Number of bits of the biggest number in a constraint	10
Biggest sum of numbers in a constraint	1385986
Number of bits of the biggest sum of numbers	21
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.07184
Number of variables	3300
Total number of constraints	5284
Number of constraints which are clauses	1364
Number of constraints which are cardinality constraints (but not clauses)	3920
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	1
Maximum length of a constraint	220
Trace number 5277

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

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        890612 kB
Buffers:         33800 kB
Cached:          74812 kB
SwapCached:       2636 kB
Active:          47988 kB
Inactive:        66112 kB
HighTotal:      131008 kB
HighFree:        52472 kB
LowTotal:       903652 kB
LowFree:        838140 kB
SwapTotal:     2097892 kB
SwapFree:      2095256 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6928 kB
Slab:            24404 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-13 23:34:10 (client local time) WITH STATUS 0 IN 1200.21 SECONDS
stats: 3741 7 1200.21 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 2572 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ############################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################
c   -- Clauses(.)/Splits(s): ....................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ---[2571]---> Adder-cost: 418   maxlim: 156   bits: 8/8
c ---[2570]---> Adder-cost: 418   maxlim: 156   bits: 8/8
c ---[2569]---> Adder-cost: 418   maxlim: 156   bits: 8/8
c ---[2568]---> Adder-cost: 418   maxlim: 156   bits: 8/8
c ---[2567]---> Adder-cost: 430   maxlim: 193   bits: 8/8
c ---[2566]---> Adder-cost: 430   maxlim: 193   bits: 8/8
c ---[2565]---> Adder-cost: 430   maxlim: 193   bits: 8/8
c ---[2564]---> Adder-cost: 430   maxlim: 193   bits: 8/8
c ---[2563]---> Adder-cost: 430   maxlim: 193   bits: 8/8
c ---[2562]---> Adder-cost: 430   maxlim: 193   bits: 8/8
c ---[2561]---> Adder-cost: 430   maxlim: 193   bits: 8/8
c ---[2560]---> Adder-cost: 430   maxlim: 193   bits: 8/8
c ---[2559]---> Adder-cost: 430   maxlim: 193   bits: 8/8
c ---[2558]---> Adder-cost: 298   maxlim: 96   bits: 8/7
c ---[2557]---> Adder-cost: 298   maxlim: 96   bits: 8/7
c ---[2556]---> Adder-cost: 298   maxlim: 96   bits: 8/7
c ---[2555]---> Adder-cost: 11   maxlim: 41   bits: 7/6
c ---[2554]---> Adder-cost: 11   maxlim: 41   bits: 7/6
c ---[2553]---> Adder-cost: 11   maxlim: 41   bits: 7/6
c ---[2552]---> Adder-cost: 11   maxlim: 41   bits: 7/6
c ---[2551]---> Adder-cost: 58   maxlim: 18   bits: 6/5
c ---[2550]---> Adder-cost: 58   maxlim: 18   bits: 6/5
c ---[2549]---> Adder-cost: 58   maxlim: 18   bits: 6/5
c ---[2548]---> Adder-cost: 58   maxlim: 18   bits: 6/5
c ---[2547]---> Adder-cost: 58   maxlim: 18   bits: 6/5
c ---[2546]---> Adder-cost: 58   maxlim: 18   bits: 6/5
c ---[2545]---> Adder-cost: 58   maxlim: 18   bits: 6/5
c ---[2544]---> Adder-cost: 58   maxlim: 18   bits: 6/5
c ---[2543]---> Adder-cost: 58   maxlim: 18   bits: 6/5
c ---[2542]---> Adder-cost: 28   maxlim: 39   bits: 7/6
c ---[2541]---> Adder-cost: 28   maxlim: 39   bits: 7/6
c ---[2540]---> Adder-cost: 28   maxlim: 39   bits: 7/6
c ---[2538]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[2536]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[2534]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[2532]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[2530]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[2528]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[2526]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[2524]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[2522]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[2520]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[2518]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[2516]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[2514]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[2512]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[2510]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[2508]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[2506]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[2504]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[2502]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[2500]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[2498]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[2496]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[2494]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[2492]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[2490]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[2488]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[2486]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[2484]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[2482]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[2480]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[2478]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[2476]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[2474]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[2472]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[2470]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[2468]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[2466]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[2464]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[2462]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[2460]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[2458]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[2456]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[2454]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[2452]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[2450]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[2448]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[2446]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[2444]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[2442]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[2440]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[2438]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[2436]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[2434]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[2432]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[2430]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[2428]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[2426]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[2424]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[2422]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[2420]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[2418]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[2416]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[2414]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[2412]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[2410]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[2408]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[2406]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[2404]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[2402]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[2400]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[2398]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[2396]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[2394]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[2392]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[2390]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[2388]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[2386]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[2384]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[2382]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[2380]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[2378]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[2376]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[2374]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[2372]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[2370]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[2368]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[2366]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[2364]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[2362]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[2360]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[2358]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[2356]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[2354]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[2352]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[2350]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[2348]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[2346]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[2344]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[2342]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[2340]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[2338]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[2336]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[2334]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[2332]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[2330]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[2328]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[2326]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[2324]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[2322]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[2320]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[2318]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[2316]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[2314]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[2312]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[2310]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[2308]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[2306]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[2304]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[2302]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[2300]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[2298]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[2296]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[2294]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[2292]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[2290]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[2288]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[2286]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[2284]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[2282]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[2280]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[2278]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[2276]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[2274]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[2272]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[2270]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[2268]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[2266]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[2264]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[2262]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[2260]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[2258]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[2256]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[2254]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[2252]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[2250]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[2248]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[2246]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[2244]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[2242]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[2240]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[2238]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[2236]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[2234]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[2232]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[2230]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[2228]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[2226]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[2224]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[2222]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[2220]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[2218]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[2216]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[2214]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[2212]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[2210]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[2208]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[2206]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[2204]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[2202]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[2200]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[2198]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[2196]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[2194]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[2192]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[2190]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[2188]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[2186]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[2184]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[2182]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[2180]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[2178]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[2176]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[2174]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[2172]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[2170]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[2168]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[2166]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[2164]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[2162]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[2160]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[2158]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[2156]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[2154]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[2152]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[2150]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[2148]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[2146]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[2144]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[2142]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[2140]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[2138]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[2136]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[2134]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[2132]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[2130]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[2128]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[2126]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[2124]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[2122]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[2120]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[2118]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[2116]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[2114]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[2112]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[2110]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[2108]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[2106]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[2104]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[2102]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[2100]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[2098]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[2096]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[2094]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[2092]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[2090]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[2088]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[2086]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[2084]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[2082]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[2080]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[2078]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[2076]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[2074]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[2072]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[2070]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[2068]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[2066]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[2064]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[2062]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[2060]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[2058]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[2056]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[2054]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[2052]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[2050]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[2048]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[2046]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[2044]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[2042]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[2040]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[2038]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[2036]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[2034]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[2032]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[2030]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[2028]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[2026]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[2024]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[2022]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[2020]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[2018]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[2016]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[2014]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[2012]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[2010]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[2008]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[2006]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[2004]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[2002]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[2000]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1998]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[1996]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[1994]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1992]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[1990]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[1988]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1986]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[1984]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[1982]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1980]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[1978]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[1976]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1974]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[1972]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[1970]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1968]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[1966]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[1964]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1962]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[1960]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1958]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[1956]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1954]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[1952]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[1950]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1948]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[1946]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1944]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[1942]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[1940]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1938]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[1936]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1934]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[1932]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[1930]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1928]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[1926]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[1924]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1922]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[1920]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1918]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[1916]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[1914]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1912]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[1910]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[1908]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1906]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[1904]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[1902]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1900]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[1898]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[1896]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1894]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[1892]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1890]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[1888]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[1886]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1884]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[1882]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[1880]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1878]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[1876]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[1874]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1872]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[1870]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[1868]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1866]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[1864]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[1862]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1860]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[1858]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[1856]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1854]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[1852]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[1850]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1848]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[1846]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[1844]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1842]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[1840]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[1838]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1836]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[1834]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[1832]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1830]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[1828]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[1826]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1824]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[1822]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[1820]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1818]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[1816]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[1814]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1812]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[1810]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1808]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[1806]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1804]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[1802]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[1800]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1798]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[1796]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[1794]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1792]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[1790]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[1788]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1786]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[1784]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[1782]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1780]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[1778]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1776]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[1774]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1772]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[1770]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1768]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[1766]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1764]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[1762]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[1760]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1758]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[1756]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[1754]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1752]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[1750]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1748]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[1746]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[1744]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1742]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[1740]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[1738]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1736]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[1734]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[1732]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1730]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[1728]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[1726]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[1724]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1722]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[1720]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[1718]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1716]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[1714]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[1712]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[1710]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[1708]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1706]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1704]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[1702]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[1700]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1698]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[1696]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1694]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[1692]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1690]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[1688]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1686]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[1684]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[1682]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1680]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[1678]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[1676]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1674]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[1672]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[1670]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1668]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[1666]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1664]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[1662]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[1660]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1658]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[1656]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[1654]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1652]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[1650]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[1648]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1646]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[1644]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[1642]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1640]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[1638]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[1636]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1634]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[1632]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[1630]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[1628]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1626]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[1624]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[1622]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1620]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[1618]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[1616]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1614]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[1612]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1610]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[1608]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[1606]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1604]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[1602]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1600]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[1598]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[1596]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1594]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[1592]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[1590]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1588]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[1586]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[1584]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1582]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[1580]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1578]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[1576]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1574]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[1572]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[1570]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1568]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[1566]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[1564]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1562]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[1560]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[1558]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1556]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[1554]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[1552]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1550]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[1548]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[1546]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1544]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[1542]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[1540]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1538]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[1536]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1534]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[1532]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1530]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[1528]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1526]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[1524]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[1522]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1520]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[1518]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[1516]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1514]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[1512]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1510]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[1508]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[1506]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1504]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[1502]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1500]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[1498]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[1496]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1494]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[1492]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[1490]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1488]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[1486]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1484]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[1482]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[1480]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1478]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[1476]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[1474]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1472]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[1470]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[1468]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1466]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[1464]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1462]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[1460]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[1458]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1456]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[1454]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[1452]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1450]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[1448]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1446]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[1444]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[1442]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1440]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[1438]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[1436]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1434]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[1432]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[1430]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1428]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[1426]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[1424]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1422]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[1420]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[1418]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1416]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[1414]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1412]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[1410]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[1408]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[1406]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1404]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[1402]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[1400]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1398]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[1396]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[1394]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[1392]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1390]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[1388]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[1386]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1384]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1382]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[1380]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1378]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1376]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[1374]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[1372]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1370]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[1368]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[1366]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1364]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   67649   237824 |   22549       0        0     nan |  0.000 % |
c |       103 |   67614   237716 |   24803      98      656     6.7 | 24.899 % |
c |       253 |   67470   237242 |   27284     231     1159     5.0 | 25.058 % |
c |       479 |   67309   236719 |   30012     434     1934     4.5 | 25.217 % |
c |       816 |   67216   236422 |   33013     756     3048     4.0 | 25.309 % |
c |      1323 |   67118   236122 |   36315    1250     5134     4.1 | 25.425 % |
c |      2084 |   67069   235966 |   39946    2006    10914     5.4 | 25.492 % |
c |      3224 |   67062   235943 |   43941    3145    19569     6.2 | 25.498 % |
c |      4935 |   67036   235855 |   48335    4854    49783    10.3 | 25.535 % |
c |      7499 |   67036   235855 |   53169    7418   190584    25.7 | 25.535 % |
c |     11344 |   67036   235855 |   58486   11263   408949    36.3 | 25.535 % |
c |     17110 |   67036   235855 |   64334   17029   976501    57.3 | 25.535 % |
c |     25762 |   66977   235656 |   70768   25676  1576920    61.4 | 25.615 % |
c |     38736 |   66951   235568 |   77845   38648  2391816    61.9 | 25.651 % |
c |     58199 |   66944   235545 |   85629   58110  3865184    66.5 | 25.657 % |
c |     87393 |   66944   235545 |   94192   87304  6722976    77.0 | 25.657 % |
c |    131182 |   66930   235499 |  103612   46326  3259941    70.4 | 25.670 % |
c |    196866 |   66930   235499 |  113973   21171  2425101   114.5 | 25.670 % |
c |    295392 |   66805   235095 |  125370   15124  1506621    99.6 | 25.829 % |
c |    443181 |   66709   234779 |  137907   46985  5109849   108.8 | 25.939 % |
#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.93 0.97 0.91 2/54 31713
Raw data (stat): 31713 (runsolver) R 31712 27565 27564 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 479825548 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0001 s]
Raw data (loadavg): 0.94 0.97 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 27565 27564 0 -1 0 2822 0 0 0 990 8 0 0 25 0 1 0 479825548 13303808 2798 4294967295 134512640 134672761 3221224576 3221223636 1075346557 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3248 2798 603 41 0 3207 0
vsize: 12992
[startup+20.0007 s]
Raw data (loadavg): 0.95 0.97 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 27565 27564 0 -1 0 4183 0 0 0 1986 11 0 0 25 0 1 0 479825548 19050496 4159 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4651 4159 603 41 0 4610 0
vsize: 18604
[startup+30.0003 s]
Raw data (loadavg): 0.95 0.97 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 27565 27564 0 -1 0 5163 0 0 0 2982 15 0 0 25 0 1 0 479825548 22945792 5139 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5602 5139 603 41 0 5561 0
vsize: 22408
[startup+40.0005 s]
Raw data (loadavg): 0.96 0.97 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 27565 27564 0 -1 0 5795 0 0 0 3981 16 0 0 25 0 1 0 479825548 25501696 5771 4294967295 134512640 134672761 3221224576 3221223744 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6226 5771 603 41 0 6185 0
vsize: 24904
[startup+50.0007 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 27565 27564 0 -1 0 6430 0 0 0 4979 18 0 0 25 0 1 0 479825548 28102656 6406 4294967295 134512640 134672761 3221224576 3221223744 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6861 6406 603 41 0 6820 0
vsize: 27444
[startup+60.0004 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 27565 27564 0 -1 0 7192 0 0 0 5977 20 0 0 25 0 1 0 479825548 31461376 7168 4294967295 134512640 134672761 3221224576 3221223776 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7681 7168 603 41 0 7640 0
vsize: 30724
[startup+70.0014 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 27565 27564 0 -1 0 7795 0 0 0 6976 22 0 0 25 0 1 0 479825548 34041856 7771 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8311 7771 603 41 0 8270 0
vsize: 33244
[startup+80.0009 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 27565 27564 0 -1 0 8332 0 0 0 7973 24 0 0 25 0 1 0 479825548 36200448 8308 4294967295 134512640 134672761 3221224576 3221223744 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8838 8308 603 41 0 8797 0
vsize: 35352
[startup+90.0006 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 27565 27564 0 -1 0 8792 0 0 0 8972 26 0 0 25 0 1 0 479825548 38100992 8768 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9302 8768 603 41 0 9261 0
vsize: 37208
[startup+100.001 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 27565 27564 0 -1 0 9214 0 0 0 9971 27 0 0 25 0 1 0 479825548 39862272 9190 4294967295 134512640 134672761 3221224576 3221223744 134560926 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9732 9190 603 41 0 9691 0
vsize: 38928
[startup+110.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 27565 27564 0 -1 0 9580 0 0 0 10970 28 0 0 25 0 1 0 479825548 41345024 9556 4294967295 134512640 134672761 3221224576 3221223728 134565073 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10094 9556 603 41 0 10053 0
vsize: 40376
[startup+120.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 27565 27564 0 -1 0 10094 0 0 0 11968 31 0 0 25 0 1 0 479825548 43364352 10070 4294967295 134512640 134672761 3221224576 3221223744 134561198 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10587 10070 603 41 0 10546 0
vsize: 42348
[startup+130.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 27565 27564 0 -1 0 10523 0 0 0 12966 33 0 0 25 0 1 0 479825548 45105152 10499 4294967295 134512640 134672761 3221224576 3221223744 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11012 10499 603 41 0 10971 0
vsize: 44048
[startup+140.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 27565 27564 0 -1 0 10523 0 0 0 13966 33 0 0 25 0 1 0 479825548 45105152 10499 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11012 10499 603 41 0 10971 0
vsize: 44048
[startup+150.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 27565 27564 0 -1 0 10523 0 0 0 14966 33 0 0 25 0 1 0 479825548 45105152 10499 4294967295 134512640 134672761 3221224576 3221223744 134561003 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11012 10499 603 41 0 10971 0
vsize: 44048
[startup+160.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 27565 27564 0 -1 0 10523 0 0 0 15966 33 0 0 25 0 1 0 479825548 45105152 10499 4294967295 134512640 134672761 3221224576 3221223680 134555084 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11012 10499 603 41 0 10971 0
vsize: 44048
[startup+170.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 27565 27564 0 -1 0 10523 0 0 0 16967 33 0 0 25 0 1 0 479825548 45105152 10499 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11012 10499 603 41 0 10971 0
vsize: 44048
[startup+180.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 27565 27564 0 -1 0 10523 0 0 0 17966 33 0 0 25 0 1 0 479825548 45105152 10499 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11012 10499 603 41 0 10971 0
vsize: 44048
[startup+190.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 27565 27564 0 -1 0 10523 0 0 0 18967 33 0 0 25 0 1 0 479825548 45105152 10499 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11012 10499 603 41 0 10971 0
vsize: 44048
[startup+200.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 27565 27564 0 -1 0 10523 0 0 0 19967 33 0 0 25 0 1 0 479825548 45105152 10499 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11012 10499 603 41 0 10971 0
vsize: 44048
[startup+210.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 27565 27564 0 -1 0 10523 0 0 0 20967 33 0 0 25 0 1 0 479825548 45105152 10499 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11012 10499 603 41 0 10971 0
vsize: 44048
[startup+220.004 s]
Raw data (loadavg): 1.07 0.99 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 27565 27564 0 -1 0 10523 0 0 0 21967 33 0 0 25 0 1 0 479825548 45105152 10499 4294967295 134512640 134672761 3221224576 3221223744 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11012 10499 603 41 0 10971 0
vsize: 44048
[startup+230.003 s]
Raw data (loadavg): 1.06 0.99 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 27565 27564 0 -1 0 10523 0 0 0 22967 33 0 0 25 0 1 0 479825548 45105152 10499 4294967295 134512640 134672761 3221224576 3221223744 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11012 10499 603 41 0 10971 0
vsize: 44048
[startup+240.003 s]
Raw data (loadavg): 1.05 0.99 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 27565 27564 0 -1 0 10523 0 0 0 23967 33 0 0 25 0 1 0 479825548 45105152 10499 4294967295 134512640 134672761 3221224576 3221223744 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11012 10499 603 41 0 10971 0
vsize: 44048
[startup+250.004 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 27565 27564 0 -1 0 10852 0 0 0 24967 34 0 0 25 0 1 0 479825548 46448640 10828 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11340 10828 603 41 0 11299 0
vsize: 45360
[startup+260.003 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 27565 27564 0 -1 0 11231 0 0 0 25966 36 0 0 25 0 1 0 479825548 48050176 11207 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11731 11207 603 41 0 11690 0
vsize: 46924
[startup+270.004 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 27565 27564 0 -1 0 11606 0 0 0 26965 37 0 0 25 0 1 0 479825548 49643520 11582 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12120 11582 603 41 0 12079 0
vsize: 48480
[startup+280.004 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 27565 27564 0 -1 0 11948 0 0 0 27964 38 0 0 25 0 1 0 479825548 50974720 11924 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12445 11924 603 41 0 12404 0
vsize: 49780
[startup+290.004 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 27565 27564 0 -1 0 12329 0 0 0 28963 38 0 0 25 0 1 0 479825548 52604928 12305 4294967295 134512640 134672761 3221224576 3221223680 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12843 12305 603 41 0 12802 0
vsize: 51372
[startup+300.004 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 27565 27564 0 -1 0 12708 0 0 0 29962 40 0 0 25 0 1 0 479825548 54214656 12684 4294967295 134512640 134672761 3221224576 3221223744 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13236 12684 603 41 0 13195 0
vsize: 52944
[startup+310.004 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 27565 27564 0 -1 0 13066 0 0 0 30961 41 0 0 25 0 1 0 479825548 55656448 13042 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13588 13042 603 41 0 13547 0
vsize: 54352
[startup+320.005 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 27565 27564 0 -1 0 13431 0 0 0 31960 42 0 0 25 0 1 0 479825548 57135104 13407 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13949 13407 603 41 0 13908 0
vsize: 55796
[startup+330.005 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 27565 27564 0 -1 0 13768 0 0 0 32959 43 0 0 25 0 1 0 479825548 58556416 13744 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14296 13744 603 41 0 14255 0
vsize: 57184
[startup+340.005 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 27565 27564 0 -1 0 14074 0 0 0 33959 44 0 0 25 0 1 0 479825548 59899904 14050 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14624 14050 603 41 0 14583 0
vsize: 58496
[startup+350.006 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 27565 27564 0 -1 0 14338 0 0 0 34958 45 0 0 25 0 1 0 479825548 60993536 14314 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14891 14314 603 41 0 14850 0
vsize: 59564
[startup+360.005 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 27565 27564 0 -1 0 14565 0 0 0 35958 46 0 0 25 0 1 0 479825548 61939712 14541 4294967295 134512640 134672761 3221224576 3221223744 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15122 14541 603 41 0 15081 0
vsize: 60488
[startup+370.005 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 27565 27564 0 -1 0 14851 0 0 0 36957 47 0 0 25 0 1 0 479825548 63078400 14827 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15400 14827 603 41 0 15359 0
vsize: 61600
[startup+380.005 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 27565 27564 0 -1 0 14919 0 0 0 37957 47 0 0 25 0 1 0 479825548 63348736 14895 4294967295 134512640 134672761 3221224576 3221223744 134561145 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15466 14895 603 41 0 15425 0
vsize: 61864
[startup+390.005 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 27565 27564 0 -1 0 14919 0 0 0 38956 47 0 0 25 0 1 0 479825548 63348736 14895 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15466 14895 603 41 0 15425 0
vsize: 61864
[startup+400.006 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 27565 27564 0 -1 0 14919 0 0 0 39957 47 0 0 25 0 1 0 479825548 63348736 14895 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15466 14895 603 41 0 15425 0
vsize: 61864
[startup+410.005 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 27565 27564 0 -1 0 14919 0 0 0 40957 47 0 0 25 0 1 0 479825548 63348736 14895 4294967295 134512640 134672761 3221224576 3221223744 134560825 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15466 14895 603 41 0 15425 0
vsize: 61864
[startup+420.005 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 27565 27564 0 -1 0 14919 0 0 0 41957 47 0 0 25 0 1 0 479825548 63348736 14895 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15466 14895 603 41 0 15425 0
vsize: 61864
[startup+430.005 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 27565 27564 0 -1 0 14919 0 0 0 42957 47 0 0 25 0 1 0 479825548 63348736 14895 4294967295 134512640 134672761 3221224576 3221223724 134560631 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15466 14895 603 41 0 15425 0
vsize: 61864
[startup+440.006 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 27565 27564 0 -1 0 14919 0 0 0 43957 47 0 0 25 0 1 0 479825548 63348736 14895 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15466 14895 603 41 0 15425 0
vsize: 61864
[startup+450.006 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 27565 27564 0 -1 0 14919 0 0 0 44957 47 0 0 25 0 1 0 479825548 63348736 14895 4294967295 134512640 134672761 3221224576 3221223744 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15466 14895 603 41 0 15425 0
vsize: 61864
[startup+460.006 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 27565 27564 0 -1 0 14919 0 0 0 45957 47 0 0 25 0 1 0 479825548 63348736 14895 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15466 14895 603 41 0 15425 0
vsize: 61864
[startup+470.006 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 27565 27564 0 -1 0 14919 0 0 0 46957 47 0 0 25 0 1 0 479825548 63348736 14895 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15466 14895 603 41 0 15425 0
vsize: 61864
[startup+480.006 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 27565 27564 0 -1 0 14919 0 0 0 47958 47 0 0 25 0 1 0 479825548 63348736 14895 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15466 14895 603 41 0 15425 0
vsize: 61864
[startup+490.006 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 27565 27564 0 -1 0 14919 0 0 0 48958 47 0 0 25 0 1 0 479825548 63348736 14895 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15466 14895 603 41 0 15425 0
vsize: 61864
[startup+500.006 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 27565 27564 0 -1 0 14919 0 0 0 49958 47 0 0 25 0 1 0 479825548 63348736 14895 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15466 14895 603 41 0 15425 0
vsize: 61864
[startup+510.006 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 27565 27564 0 -1 0 14919 0 0 0 50958 47 0 0 25 0 1 0 479825548 63348736 14895 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15466 14895 603 41 0 15425 0
vsize: 61864
[startup+520.006 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 27565 27564 0 -1 0 14919 0 0 0 51958 47 0 0 25 0 1 0 479825548 63348736 14895 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15466 14895 603 41 0 15425 0
vsize: 61864
[startup+530.006 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 27565 27564 0 -1 0 14920 0 0 0 52958 47 0 0 25 0 1 0 479825548 63348736 14896 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15466 14896 603 41 0 15425 0
vsize: 61864
[startup+540.006 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 27565 27564 0 -1 0 14924 0 0 0 53958 47 0 0 25 0 1 0 479825548 63348736 14900 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15466 14900 603 41 0 15425 0
vsize: 61864
[startup+550.006 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 27565 27564 0 -1 0 14927 0 0 0 54958 48 0 0 25 0 1 0 479825548 63348736 14903 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15466 14903 603 41 0 15425 0
vsize: 61864
[startup+560.006 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 27565 27564 0 -1 0 14930 0 0 0 55959 48 0 0 25 0 1 0 479825548 63348736 14906 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15466 14906 603 41 0 15425 0
vsize: 61864
[startup+570.006 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 27565 27564 0 -1 0 14930 0 0 0 56958 48 0 0 25 0 1 0 479825548 63262720 14902 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15445 14902 603 41 0 15404 0
vsize: 61780
[startup+580.007 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 27565 27564 0 -1 0 14930 0 0 0 57957 48 0 0 25 0 1 0 479825548 63262720 14902 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15445 14902 603 41 0 15404 0
vsize: 61780
[startup+590.007 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 27565 27564 0 -1 0 14930 0 0 0 58957 48 0 0 25 0 1 0 479825548 63262720 14902 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15445 14902 603 41 0 15404 0
vsize: 61780
[startup+600.006 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 27565 27564 0 -1 0 14930 0 0 0 59958 48 0 0 25 0 1 0 479825548 63262720 14902 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15445 14902 603 41 0 15404 0
vsize: 61780
[startup+610.006 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 27565 27564 0 -1 0 14930 0 0 0 60958 48 0 0 25 0 1 0 479825548 63262720 14902 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15445 14902 603 41 0 15404 0
vsize: 61780
[startup+620.007 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 27565 27564 0 -1 0 14930 0 0 0 61958 48 0 0 25 0 1 0 479825548 63262720 14902 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15445 14902 603 41 0 15404 0
vsize: 61780
[startup+630.007 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 27565 27564 0 -1 0 14930 0 0 0 62958 48 0 0 25 0 1 0 479825548 63262720 14902 4294967295 134512640 134672761 3221224576 3221223744 134560988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15445 14902 603 41 0 15404 0
vsize: 61780
[startup+640.007 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 27565 27564 0 -1 0 14930 0 0 0 63958 48 0 0 25 0 1 0 479825548 63262720 14902 4294967295 134512640 134672761 3221224576 3221223680 134560171 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15445 14902 603 41 0 15404 0
vsize: 61780
[startup+650.007 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 27565 27564 0 -1 0 14930 0 0 0 64958 48 0 0 25 0 1 0 479825548 63262720 14902 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15445 14902 603 41 0 15404 0
vsize: 61780
[startup+660.007 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 27565 27564 0 -1 0 14930 0 0 0 65958 48 0 0 25 0 1 0 479825548 63262720 14902 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15445 14902 603 41 0 15404 0
vsize: 61780
[startup+670.008 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 27565 27564 0 -1 0 14930 0 0 0 66959 49 0 0 25 0 1 0 479825548 63262720 14902 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15445 14902 603 41 0 15404 0
vsize: 61780
[startup+680.007 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 27565 27564 0 -1 0 14931 0 0 0 67959 49 0 0 25 0 1 0 479825548 63262720 14903 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15445 14903 603 41 0 15404 0
vsize: 61780
[startup+690.007 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 27565 27564 0 -1 0 14931 0 0 0 68959 49 0 0 25 0 1 0 479825548 63262720 14903 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15445 14903 603 41 0 15404 0
vsize: 61780
[startup+700.007 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 27565 27564 0 -1 0 14931 0 0 0 69959 49 0 0 25 0 1 0 479825548 63262720 14903 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15445 14903 603 41 0 15404 0
vsize: 61780
[startup+710.006 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 27565 27564 0 -1 0 14931 0 0 0 70959 49 0 0 25 0 1 0 479825548 63262720 14903 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15445 14903 603 41 0 15404 0
vsize: 61780
[startup+720.006 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 27565 27564 0 -1 0 14931 0 0 0 71959 49 0 0 25 0 1 0 479825548 63262720 14903 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15445 14903 603 41 0 15404 0
vsize: 61780
[startup+730.006 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 27565 27564 0 -1 0 14931 0 0 0 72959 49 0 0 25 0 1 0 479825548 63262720 14903 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15445 14903 603 41 0 15404 0
vsize: 61780
[startup+740.007 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 27565 27564 0 -1 0 15103 0 0 0 73959 50 0 0 25 0 1 0 479825548 64065536 15075 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15641 15075 603 41 0 15600 0
vsize: 62564
[startup+750.006 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 27565 27564 0 -1 0 15383 0 0 0 74958 51 0 0 25 0 1 0 479825548 65159168 15355 4294967295 134512640 134672761 3221224576 3221223744 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15908 15355 603 41 0 15867 0
vsize: 63632
[startup+760.007 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 27565 27564 0 -1 0 15702 0 0 0 75957 52 0 0 25 0 1 0 479825548 66506752 15674 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16237 15674 603 41 0 16196 0
vsize: 64948
[startup+770.007 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 27565 27564 0 -1 0 16030 0 0 0 76956 53 0 0 25 0 1 0 479825548 67850240 16002 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16565 16002 603 41 0 16524 0
vsize: 66260
[startup+780.007 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 27565 27564 0 -1 0 16442 0 0 0 77955 54 0 0 25 0 1 0 479825548 69595136 16414 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16991 16414 603 41 0 16950 0
vsize: 67964
[startup+790.008 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 27565 27564 0 -1 0 16856 0 0 0 78954 55 0 0 25 0 1 0 479825548 71208960 16828 4294967295 134512640 134672761 3221224576 3221223700 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17385 16828 603 41 0 17344 0
vsize: 69540
[startup+800.007 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 27565 27564 0 -1 0 17230 0 0 0 79952 57 0 0 25 0 1 0 479825548 72699904 17202 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17749 17202 603 41 0 17708 0
vsize: 70996
[startup+810.007 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 27565 27564 0 -1 0 17366 0 0 0 80952 57 0 0 25 0 1 0 479825548 73236480 17338 4294967295 134512640 134672761 3221224576 3221223680 134560370 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17880 17338 603 41 0 17839 0
vsize: 71520
[startup+820.008 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 27565 27564 0 -1 0 17366 0 0 0 81953 57 0 0 25 0 1 0 479825548 73236480 17338 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17880 17338 603 41 0 17839 0
vsize: 71520
[startup+830.007 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 27565 27564 0 -1 0 17366 0 0 0 82953 57 0 0 25 0 1 0 479825548 73236480 17338 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17880 17338 603 41 0 17839 0
vsize: 71520
[startup+840.007 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 27565 27564 0 -1 0 17368 0 0 0 83953 57 0 0 25 0 1 0 479825548 73236480 17340 4294967295 134512640 134672761 3221224576 3221223744 134560876 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17880 17340 603 41 0 17839 0
vsize: 71520
[startup+850.008 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 27565 27564 0 -1 0 17368 0 0 0 84953 57 0 0 25 0 1 0 479825548 73236480 17340 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17880 17340 603 41 0 17839 0
vsize: 71520
[startup+860.007 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 27565 27564 0 -1 0 17368 0 0 0 85953 57 0 0 25 0 1 0 479825548 73236480 17340 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17880 17340 603 41 0 17839 0
vsize: 71520
[startup+870.007 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 27565 27564 0 -1 0 17368 0 0 0 86953 57 0 0 25 0 1 0 479825548 73236480 17340 4294967295 134512640 134672761 3221224576 3221223712 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17880 17340 603 41 0 17839 0
vsize: 71520
[startup+880.007 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 27565 27564 0 -1 0 17368 0 0 0 87953 57 0 0 25 0 1 0 479825548 73236480 17340 4294967295 134512640 134672761 3221224576 3221223744 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17880 17340 603 41 0 17839 0
vsize: 71520
[startup+890.007 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 27565 27564 0 -1 0 17368 0 0 0 88953 58 0 0 25 0 1 0 479825548 73236480 17340 4294967295 134512640 134672761 3221224576 3221223744 134560895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17880 17340 603 41 0 17839 0
vsize: 71520
[startup+900.007 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 27565 27564 0 -1 0 17368 0 0 0 89953 58 0 0 25 0 1 0 479825548 73236480 17340 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17880 17340 603 41 0 17839 0
vsize: 71520
[startup+910.007 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 27565 27564 0 -1 0 17368 0 0 0 90953 58 0 0 25 0 1 0 479825548 73236480 17340 4294967295 134512640 134672761 3221224576 3221223760 134559354 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17880 17340 603 41 0 17839 0
vsize: 71520
[startup+920.008 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 27565 27564 0 -1 0 17368 0 0 0 91953 58 0 0 25 0 1 0 479825548 73236480 17340 4294967295 134512640 134672761 3221224576 3221223744 134560858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17880 17340 603 41 0 17839 0
vsize: 71520
[startup+930.007 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 27565 27564 0 -1 0 17368 0 0 0 92953 58 0 0 25 0 1 0 479825548 73236480 17340 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17880 17340 603 41 0 17839 0
vsize: 71520
[startup+940.008 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 27565 27564 0 -1 0 17368 0 0 0 93953 58 0 0 25 0 1 0 479825548 73236480 17340 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17880 17340 603 41 0 17839 0
vsize: 71520
[startup+950.008 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 27565 27564 0 -1 0 17368 0 0 0 94954 58 0 0 25 0 1 0 479825548 73236480 17340 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17880 17340 603 41 0 17839 0
vsize: 71520
[startup+960.008 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 27565 27564 0 -1 0 17368 0 0 0 95954 58 0 0 25 0 1 0 479825548 73236480 17340 4294967295 134512640 134672761 3221224576 3221223728 134565083 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17880 17340 603 41 0 17839 0
vsize: 71520
[startup+970.008 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 27565 27564 0 -1 0 17370 0 0 0 96954 58 0 0 25 0 1 0 479825548 73236480 17342 4294967295 134512640 134672761 3221224576 3221223744 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17880 17342 603 41 0 17839 0
vsize: 71520
[startup+980.008 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 27565 27564 0 -1 0 17370 0 0 0 97954 58 0 0 25 0 1 0 479825548 73236480 17342 4294967295 134512640 134672761 3221224576 3221223744 134561207 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17880 17342 603 41 0 17839 0
vsize: 71520
[startup+990.008 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 27565 27564 0 -1 0 17370 0 0 0 98954 58 0 0 25 0 1 0 479825548 73236480 17342 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17880 17342 603 41 0 17839 0
vsize: 71520
[startup+1000.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 27565 27564 0 -1 0 17370 0 0 0 99954 58 0 0 25 0 1 0 479825548 73236480 17342 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17880 17342 603 41 0 17839 0
vsize: 71520
[startup+1010.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 27565 27564 0 -1 0 17370 0 0 0 100954 58 0 0 25 0 1 0 479825548 73236480 17342 4294967295 134512640 134672761 3221224576 3221223744 134560852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17880 17342 603 41 0 17839 0
vsize: 71520
[startup+1020.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 27565 27564 0 -1 0 17370 0 0 0 101955 58 0 0 25 0 1 0 479825548 73236480 17342 4294967295 134512640 134672761 3221224576 3221223744 134561207 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17880 17342 603 41 0 17839 0
vsize: 71520
[startup+1030.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 27565 27564 0 -1 0 17370 0 0 0 102955 58 0 0 25 0 1 0 479825548 73236480 17342 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17880 17342 603 41 0 17839 0
vsize: 71520
[startup+1040.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 27565 27564 0 -1 0 17524 0 0 0 103954 59 0 0 25 0 1 0 479825548 73908224 17496 4294967295 134512640 134672761 3221224576 3221223744 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18044 17496 603 41 0 18003 0
vsize: 72176
[startup+1050.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 27565 27564 0 -1 0 17825 0 0 0 104953 60 0 0 25 0 1 0 479825548 75243520 17797 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18370 17797 603 41 0 18329 0
vsize: 73480
[startup+1060.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 27565 27564 0 -1 0 18116 0 0 0 105952 62 0 0 25 0 1 0 479825548 76451840 18088 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18665 18088 603 41 0 18624 0
vsize: 74660
[startup+1070.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 27565 27564 0 -1 0 18397 0 0 0 106951 63 0 0 25 0 1 0 479825548 77660160 18369 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18960 18369 603 41 0 18919 0
vsize: 75840
[startup+1080.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 27565 27564 0 -1 0 18687 0 0 0 107950 64 0 0 25 0 1 0 479825548 78729216 18659 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19221 18659 603 41 0 19180 0
vsize: 76884
[startup+1090.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 27565 27564 0 -1 0 18957 0 0 0 108949 65 0 0 25 0 1 0 479825548 79945728 18929 4294967295 134512640 134672761 3221224576 3221223744 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19518 18929 603 41 0 19477 0
vsize: 78072
[startup+1100.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 27565 27564 0 -1 0 19216 0 0 0 109949 66 0 0 25 0 1 0 479825548 81022976 19188 4294967295 134512640 134672761 3221224576 3221223744 134561008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19781 19188 603 41 0 19740 0
vsize: 79124
[startup+1110.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 27565 27564 0 -1 0 19498 0 0 0 110948 66 0 0 25 0 1 0 479825548 82104320 19470 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20045 19470 603 41 0 20004 0
vsize: 80180
[startup+1120.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 27565 27564 0 -1 0 19772 0 0 0 111947 67 0 0 25 0 1 0 479825548 83329024 19744 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20344 19744 603 41 0 20303 0
vsize: 81376
[startup+1130.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 27565 27564 0 -1 0 20016 0 0 0 112947 68 0 0 25 0 1 0 479825548 84791296 19988 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20701 19988 603 41 0 20660 0
vsize: 82804
[startup+1140.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 27565 27564 0 -1 0 20248 0 0 0 113946 69 0 0 25 0 1 0 479825548 85733376 20220 4294967295 134512640 134672761 3221224576 3221223744 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20931 20220 603 41 0 20890 0
vsize: 83724
[startup+1150.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 27565 27564 0 -1 0 20453 0 0 0 114946 69 0 0 25 0 1 0 479825548 86663168 20425 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21158 20425 603 41 0 21117 0
vsize: 84632
[startup+1160.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 27565 27564 0 -1 0 20688 0 0 0 115945 70 0 0 25 0 1 0 479825548 87576576 20660 4294967295 134512640 134672761 3221224576 3221223744 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21381 20660 603 41 0 21340 0
vsize: 85524
[startup+1170.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 27565 27564 0 -1 0 20927 0 0 0 116945 71 0 0 25 0 1 0 479825548 88518656 20899 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21611 20899 603 41 0 21570 0
vsize: 86444
[startup+1180.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 27565 27564 0 -1 0 21154 0 0 0 117945 71 0 0 25 0 1 0 479825548 89587712 21126 4294967295 134512640 134672761 3221224576 3221223744 134561218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21872 21126 603 41 0 21831 0
vsize: 87488
[startup+1190.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 27565 27564 0 -1 0 21380 0 0 0 118944 72 0 0 25 0 1 0 479825548 90542080 21352 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22105 21352 603 41 0 22064 0
vsize: 88420
[startup+1200.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 27565 27564 0 -1 0 21504 0 0 0 119944 73 0 0 25 0 1 0 479825548 90947584 21476 4294967295 134512640 134672761 3221224576 3221223680 134554662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22204 21476 603 41 0 22163 0
vsize: 88816
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.05 s]
Raw data (loadavg): 1.00 0.99 0.91 1/54 31713
Raw data (stat): 31713 (minisat+) Z 31712 27565 27564 0 -1 12 21506 0 0 0 119944 77 0 0 25 0 1 0 479825548 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 0
Real time (s): 1200.05
CPU time (s): 1200.21
CPU user time (s): 1199.44
CPU system time (s): 0.770882
CPU usage (%): 100.013
Max. virtual memory (Kb): 88816
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####