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/ppp-problems/normalized-ppp:1-11,19,21.opb
MD5SUM	552cc7fcebca47ae66a3cb1c13679513
Bench Category	no optimization function (SAT)
Has Objective Function	NO
Satisfiable
(Un)Satisfiability was proved
Best value of the objective function
Optimality of the best value was proved
Number of terms in the objective function	0
Biggest coefficient in the objective function	0
Number of bits for the biggest coefficient in the objective function	0
Sum of the numbers in the objective function	0
Number of bits of the sum of numbers in the objective function	0
Biggest number in a constraint	10
Number of bits of the biggest number in a constraint	4
Biggest sum of numbers in a constraint	103
Number of bits of the biggest sum of numbers	7
Best result obtained on this benchmark
Best CPU time to get the best result obtained on this benchmark
Number of variables	4602
Total number of constraints	34781
Number of constraints which are clauses	29160
Number of constraints which are cardinality constraints (but not clauses)	5543
Number of constraints which are nor clauses,nor cardinality constraints	78
Minimum length of a constraint	1
Maximum length of a constraint	29
Trace number 5279

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc31 THE 2005-04-13 23:14:42 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3743 boxname=wulflinc31 idbench=359 idsolver=10 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  552cc7fcebca47ae66a3cb1c13679513  /oldhome/oroussel/tmp/wulflinc31/normalized-ppp:1-11,19,21.opb
REAL COMMAND:  minisat+ -ca /oldhome/oroussel/tmp/wulflinc31/normalized-ppp:1-11,19,21.opb /oldhome/oroussel/tmp/wulflinc31/normalized-ppp:1-11,19,21.opb
IDLAUNCH: 3743
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.153
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.153
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:        906908 kB
Buffers:         34740 kB
Cached:          54220 kB
SwapCached:        392 kB
Active:          50904 kB
Inactive:        41232 kB
HighTotal:      131008 kB
HighFree:        73080 kB
LowTotal:       903652 kB
LowFree:        833828 kB
SwapTotal:     2097892 kB
SwapFree:      2097452 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6832 kB
Slab:            29968 kB
Committed_AS:    63488 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-13 23:34:44 (client local time) WITH STATUS 0 IN 1200.26 SECONDS
stats: 3743 7 1200.26 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 30353 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ##############################################################################################################################################################################
c   -- Clauses(.)/Splits(s): ........................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ---[30352]---> Adder-cost: 50   maxlim: 60   bits: 7/6
c ---[30351]---> Adder-cost: 50   maxlim: 60   bits: 7/6
c ---[30350]---> Adder-cost: 50   maxlim: 60   bits: 7/6
c ---[30349]---> Adder-cost: 50   maxlim: 60   bits: 7/6
c ---[30348]---> Adder-cost: 50   maxlim: 60   bits: 7/6
c ---[30347]---> Adder-cost: 50   maxlim: 60   bits: 7/6
c ---[30346]---> Adder-cost: 50   maxlim: 60   bits: 7/6
c ---[30345]---> Adder-cost: 50   maxlim: 60   bits: 7/6
c ---[30344]---> Adder-cost: 50   maxlim: 60   bits: 7/6
c ---[30343]---> Adder-cost: 50   maxlim: 60   bits: 7/6
c ---[30342]---> Adder-cost: 50   maxlim: 60   bits: 7/6
c ---[30341]---> Adder-cost: 50   maxlim: 60   bits: 7/6
c ---[30340]---> Adder-cost: 66   maxlim: 84   bits: 7/7
c ---[30339]---> Adder-cost: 66   maxlim: 84   bits: 7/7
c ---[30338]---> Adder-cost: 66   maxlim: 84   bits: 7/7
c ---[30337]---> Adder-cost: 66   maxlim: 84   bits: 7/7
c ---[30336]---> Adder-cost: 66   maxlim: 84   bits: 7/7
c ---[30335]---> Adder-cost: 66   maxlim: 84   bits: 7/7
c ---[30334]---> Adder-cost: 66   maxlim: 84   bits: 7/7
c ---[30333]---> Adder-cost: 66   maxlim: 84   bits: 7/7
c ---[30332]---> Adder-cost: 66   maxlim: 84   bits: 7/7
c ---[30331]---> Adder-cost: 66   maxlim: 84   bits: 7/7
c ---[30330]---> Adder-cost: 66   maxlim: 84   bits: 7/7
c ---[30329]---> Adder-cost: 66   maxlim: 84   bits: 7/7
c ---[30328]---> Adder-cost: 66   maxlim: 84   bits: 7/7
c ---[30327]---> Adder-cost: 66   maxlim: 84   bits: 7/7
c ---[30326]---> Adder-cost: 66   maxlim: 84   bits: 7/7
c ---[30325]---> Adder-cost: 66   maxlim: 84   bits: 7/7
c ---[30324]---> Adder-cost: 66   maxlim: 84   bits: 7/7
c ---[30323]---> Adder-cost: 66   maxlim: 84   bits: 7/7
c ---[30322]---> Adder-cost: 66   maxlim: 83   bits: 7/7
c ---[30321]---> Adder-cost: 66   maxlim: 83   bits: 7/7
c ---[30320]---> Adder-cost: 66   maxlim: 83   bits: 7/7
c ---[30319]---> Adder-cost: 66   maxlim: 83   bits: 7/7
c ---[30318]---> Adder-cost: 66   maxlim: 83   bits: 7/7
c ---[30317]---> Adder-cost: 66   maxlim: 83   bits: 7/7
c ---[30316]---> Adder-cost: 66   maxlim: 84   bits: 7/7
c ---[30315]---> Adder-cost: 66   maxlim: 84   bits: 7/7
c ---[30314]---> Adder-cost: 66   maxlim: 84   bits: 7/7
c ---[30313]---> Adder-cost: 66   maxlim: 84   bits: 7/7
c ---[30312]---> Adder-cost: 66   maxlim: 84   bits: 7/7
c ---[30311]---> Adder-cost: 66   maxlim: 84   bits: 7/7
c ---[30310]---> Adder-cost: 66   maxlim: 84   bits: 7/7
c ---[30309]---> Adder-cost: 66   maxlim: 84   bits: 7/7
c ---[30308]---> Adder-cost: 66   maxlim: 84   bits: 7/7
c ---[30307]---> Adder-cost: 66   maxlim: 84   bits: 7/7
c ---[30306]---> Adder-cost: 66   maxlim: 84   bits: 7/7
c ---[30305]---> Adder-cost: 66   maxlim: 84   bits: 7/7
c ---[30304]---> Adder-cost: 66   maxlim: 84   bits: 7/7
c ---[30303]---> Adder-cost: 66   maxlim: 84   bits: 7/7
c ---[30302]---> Adder-cost: 66   maxlim: 84   bits: 7/7
c ---[30301]---> Adder-cost: 66   maxlim: 84   bits: 7/7
c ---[30300]---> Adder-cost: 66   maxlim: 84   bits: 7/7
c ---[30299]---> Adder-cost: 66   maxlim: 84   bits: 7/7
c ---[30298]---> Adder-cost: 66   maxlim: 82   bits: 7/7
c ---[30297]---> Adder-cost: 66   maxlim: 82   bits: 7/7
c ---[30296]---> Adder-cost: 66   maxlim: 82   bits: 7/7
c ---[30295]---> Adder-cost: 66   maxlim: 82   bits: 7/7
c ---[30294]---> Adder-cost: 66   maxlim: 82   bits: 7/7
c ---[30293]---> Adder-cost: 66   maxlim: 82   bits: 7/7
c ---[30292]---> Adder-cost: 66   maxlim: 82   bits: 7/7
c ---[30291]---> Adder-cost: 66   maxlim: 82   bits: 7/7
c ---[30290]---> Adder-cost: 66   maxlim: 82   bits: 7/7
c ---[30289]---> Adder-cost: 66   maxlim: 82   bits: 7/7
c ---[30288]---> Adder-cost: 66   maxlim: 82   bits: 7/7
c ---[30287]---> Adder-cost: 66   maxlim: 82   bits: 7/7
c ---[30286]---> Adder-cost: 62   maxlim: 79   bits: 7/7
c ---[30285]---> Adder-cost: 62   maxlim: 79   bits: 7/7
c ---[30284]---> Adder-cost: 62   maxlim: 79   bits: 7/7
c ---[30283]---> Adder-cost: 62   maxlim: 79   bits: 7/7
c ---[30282]---> Adder-cost: 62   maxlim: 79   bits: 7/7
c ---[30281]---> Adder-cost: 62   maxlim: 79   bits: 7/7
c ---[30280]---> Adder-cost: 50   maxlim: 60   bits: 7/6
c ---[30279]---> Adder-cost: 50   maxlim: 60   bits: 7/6
c ---[30278]---> Adder-cost: 50   maxlim: 60   bits: 7/6
c ---[30277]---> Adder-cost: 50   maxlim: 60   bits: 7/6
c ---[30276]---> Adder-cost: 50   maxlim: 60   bits: 7/6
c ---[30275]---> Adder-cost: 50   maxlim: 60   bits: 7/6
c ---[30273]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30271]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30269]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30267]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30265]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30263]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30261]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30259]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30257]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30255]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30253]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30251]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30249]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30247]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30245]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30243]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30241]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30239]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30237]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[30235]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[30233]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[30231]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[30229]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[30227]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[30225]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30223]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30221]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30219]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30217]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30215]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30213]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30211]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30209]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30207]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30205]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30203]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30201]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[30199]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[30197]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[30195]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[30193]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[30191]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[30189]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[30187]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[30185]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[30183]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[30181]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[30179]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[30177]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30175]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30173]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30171]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30169]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30167]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30165]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30163]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30161]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30159]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30157]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30155]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30153]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30151]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30149]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30147]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30145]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30143]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30141]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30139]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30137]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30135]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30133]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30131]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30129]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30127]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30125]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30123]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30121]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30119]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30117]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30115]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30113]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30111]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30109]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30107]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30105]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30103]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30101]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30099]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30097]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30095]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30093]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30091]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30089]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30087]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30085]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30083]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30081]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30079]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30077]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30075]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30073]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30071]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30069]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30067]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30065]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30063]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30061]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30059]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30057]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[30055]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[30053]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[30051]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[30049]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[30047]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[30045]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30043]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30041]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30039]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30037]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30035]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30033]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30031]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30029]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30027]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30025]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30023]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30021]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30019]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30017]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30015]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30013]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30011]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30009]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30007]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30005]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30003]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30001]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[29999]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[29997]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[29995]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[29993]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[29991]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[29989]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[29987]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[29985]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[29983]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[29981]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[29979]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[29977]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[29975]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[29973]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[29971]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[29969]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[29967]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[29965]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[29963]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[29961]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[29959]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[29957]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[29955]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[29953]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[29951]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[29949]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[29947]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[29945]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[29943]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[29941]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[29939]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[29937]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[29935]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[29933]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[29931]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[29929]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[29927]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[29926]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29925]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29924]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29923]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29922]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29921]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29920]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29919]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29918]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29917]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29916]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29915]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29914]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29913]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29912]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29911]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29910]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29909]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29908]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29907]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29906]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29905]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29904]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29903]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29902]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29901]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29900]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29899]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29898]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29897]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29896]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29895]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29894]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29893]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29892]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29891]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29890]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29889]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29888]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29887]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29886]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29885]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29884]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29883]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29882]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29881]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29880]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29879]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29878]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29877]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29876]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29875]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29874]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29873]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29872]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29871]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29870]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29869]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29868]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29867]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29866]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29865]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29864]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29863]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29862]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29861]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29860]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29859]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29858]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29857]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29856]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29855]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29854]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29853]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29852]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29851]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29850]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29849]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29848]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29847]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29846]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29845]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29844]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29843]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29842]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29841]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29840]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29839]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29838]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29837]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29836]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29835]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29834]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29833]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29832]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29831]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29830]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29829]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29828]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29827]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29826]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29825]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29824]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29823]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29822]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29821]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29820]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29819]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29818]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29817]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29816]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29815]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29814]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29813]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29812]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29811]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29810]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29809]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29808]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29807]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29806]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29805]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29804]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29803]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29802]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29801]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29800]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29799]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29798]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29797]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29796]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29795]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29794]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29793]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29792]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29791]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29790]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29789]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29788]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29787]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29786]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29785]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29784]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29783]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29782]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29781]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29780]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29779]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29778]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29777]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29776]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29775]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29774]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29773]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29772]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29771]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29770]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29769]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29768]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29767]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29766]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29765]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29764]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29763]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29762]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29761]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29760]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29759]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29758]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29757]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29756]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29755]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29754]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29753]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29752]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29751]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29750]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29749]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29748]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29747]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29746]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29745]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29744]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29743]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29742]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29741]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29740]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29739]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29738]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29737]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29736]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29735]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29734]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29733]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29732]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29731]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29730]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29729]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29728]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29727]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29726]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29725]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29724]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29723]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29722]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29721]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29720]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29719]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29718]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29717]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29716]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29715]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29714]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29713]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29712]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29711]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29710]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29709]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29708]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29707]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29706]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29705]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29704]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29703]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29702]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29701]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29700]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29699]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29698]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29697]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29696]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29695]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29694]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29693]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29692]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29691]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29690]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29689]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29688]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29687]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29686]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29685]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29684]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29683]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29682]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29681]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29680]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29679]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29678]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29677]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29676]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29675]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29674]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29673]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29672]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29671]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29670]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29669]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29668]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29667]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29666]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29665]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29664]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29663]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29662]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29661]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29660]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29659]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29658]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29657]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29656]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29655]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29654]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29653]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29652]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29651]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29650]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29649]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29648]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29647]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29646]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29645]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29644]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29643]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29642]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29641]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29640]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29639]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29638]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29637]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29636]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29635]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29634]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29633]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29632]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29631]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29630]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29629]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29628]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29627]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29626]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29625]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29624]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29623]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29622]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29621]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29620]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29619]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29618]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29617]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29616]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29615]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29614]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29613]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29612]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29611]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29610]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29609]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29608]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29607]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29606]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29605]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29604]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29603]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29602]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29601]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29600]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29599]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29598]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29597]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29596]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29595]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29594]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29593]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29592]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29591]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29590]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29589]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29588]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29587]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29586]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29585]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29584]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29583]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29582]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29581]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29580]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29579]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29578]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29577]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29576]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29575]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29574]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29573]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29572]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29571]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29570]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29569]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29568]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29567]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29566]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 405]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 404]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 403]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 402]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 401]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 400]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 399]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 398]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 397]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 396]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 395]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 394]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 393]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 392]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 391]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 390]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 389]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 388]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 387]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 386]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 385]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 384]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 383]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 382]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 381]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 380]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 379]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 378]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 377]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 376]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 375]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 374]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 373]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 372]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 371]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 370]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 369]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 368]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 367]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 366]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 365]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 364]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 363]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 362]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 361]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 360]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 359]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 358]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 357]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 356]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 355]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 354]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 353]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 352]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 351]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 350]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 349]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 348]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 347]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 346]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 345]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 344]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 343]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 342]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 341]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 340]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 339]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 338]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 337]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 336]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 335]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 334]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 333]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 332]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 331]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 330]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 329]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 328]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 327]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 326]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 325]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 324]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 323]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 322]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 321]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 320]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 319]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 318]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 317]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 316]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 315]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 314]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 313]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 312]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 311]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 310]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 309]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 308]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 307]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 306]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 305]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 304]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 303]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 302]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 301]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 300]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 299]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 298]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 297]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 296]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 295]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 294]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 293]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 292]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 291]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 290]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 289]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 288]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 287]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 286]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 285]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 284]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 283]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 282]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 281]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 280]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 279]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 278]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 277]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 276]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 275]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 274]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 273]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 272]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 271]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 270]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 269]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 268]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 267]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 266]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 265]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 264]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 263]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 262]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 261]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 260]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 259]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 258]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 257]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 256]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 255]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 254]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 253]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 252]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 251]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 250]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 249]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 248]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 247]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 246]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 245]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 244]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 243]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 242]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 241]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 240]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 239]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 238]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 237]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 236]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 235]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 234]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 233]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 232]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 231]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 230]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 229]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 228]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 227]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 226]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 225]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 224]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 223]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 222]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 221]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 220]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 219]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 218]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 217]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 216]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 215]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 214]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 213]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 212]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 211]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 210]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 209]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 208]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 207]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 206]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 205]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 204]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 203]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 202]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 201]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 200]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 199]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 198]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 197]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 196]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 195]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 194]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 193]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 192]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 191]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 190]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 189]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 188]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 187]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 186]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 185]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 184]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 183]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 182]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 181]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 180]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 179]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 178]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 177]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 176]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 175]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 174]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 173]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 172]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 171]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 170]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 169]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 168]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 167]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 166]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 165]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 164]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 163]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 162]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 161]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 160]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 159]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 158]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 157]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 156]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 155]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 154]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 153]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 152]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 151]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 150]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 149]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 148]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 147]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 146]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 145]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 144]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 143]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 142]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 141]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 140]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 139]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 138]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 137]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 136]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 135]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 134]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 133]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 132]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 131]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 130]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 129]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 128]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 127]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 126]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 125]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 124]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 123]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 122]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 121]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 120]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 119]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 118]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 117]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 116]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 115]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 114]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 113]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 112]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 111]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 110]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 109]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 108]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 107]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 106]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 105]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 104]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 103]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 102]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 101]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 100]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[  99]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[  98]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[  97]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[  96]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[  95]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[  94]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[  93]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[  92]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[  91]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[  90]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[  89]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[  88]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[  87]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[  86]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[  85]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[  84]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[  83]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[  82]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[  81]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[  80]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[  79]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[  78]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[  77]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[  76]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[  75]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[  74]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[  73]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[  72]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[  71]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[  70]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[  69]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[  68]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[  67]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[  66]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[  65]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[  64]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[  63]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[  62]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[  61]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[  60]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[  59]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[  58]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[  57]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[  56]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[  55]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[  54]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[  53]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[  52]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[  51]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[  50]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[  49]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[  48]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[  47]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[  46]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[  45]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[  44]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[  43]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[  42]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[  41]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[  40]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[  39]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[  38]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[  37]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[  36]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[  35]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[  34]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[  33]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[  32]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[  31]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[  30]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[  29]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[  28]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[  27]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[  26]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[  25]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[  24]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[  23]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[  22]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[  21]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[  20]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[  19]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[  18]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[  17]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[  16]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[  15]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[  14]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[  13]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[  12]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[  11]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[  10]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[   9]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[   8]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[   7]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[   6]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[   5]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[   4]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[   3]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[   2]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[   1]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[   0]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  110737   373892 |   36912       0        0     nan |  0.000 % |
c |       100 |  110064   371616 |   40603      25       70     2.8 | 17.173 % |
c |       251 |  109288   368973 |   44663      99      399     4.0 | 17.873 % |
c |       476 |  108642   366785 |   49129     255     1011     4.0 | 18.436 % |
c |       815 |  108290   365583 |   54042     555     2617     4.7 | 18.730 % |
c |      1321 |  107688   363548 |   59447     975     5055     5.2 | 19.234 % |
c |      2080 |  107097   361559 |   65391    1650     8252     5.0 | 19.753 % |
c |      3219 |  106363   359094 |   71931    2688    13534     5.0 | 20.370 % |
c |      4927 |  105464   356113 |   79124    4268    22498     5.3 | 21.139 % |
c |      7489 |  104152   351760 |   87036    6641    35658     5.4 | 22.245 % |
c |     11333 |  102525   346396 |   95740   10190    57377     5.6 | 23.621 % |
c |     17100 |  100882   340977 |  105314   15643   107516     6.9 | 25.006 % |
c |     25749 |   99737   337219 |  115845   24086   220058     9.1 | 25.985 % |
c |     38723 |   98860   334332 |  127430   36864   564787    15.3 | 26.729 % |
c |     58185 |   97906   331178 |  140173   56100  1211213    21.6 | 27.542 % |
c |     87377 |   97367   329417 |  154190   85175  3053640    35.9 | 28.027 % |
c |    131169 |   96588   326857 |  169609  128792  7709761    59.9 | 28.688 % |
c |    196859 |   96375   326165 |  186570   39451  4309130   109.2 | 28.878 % |
c |    295386 |   96113   325311 |  205227  137930 18027445   130.7 | 29.104 % |
#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.85 0.95 0.90 2/54 26868
Raw data (stat): 26868 (runsolver) R 26867 23176 23175 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 479816935 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0001 s]
Raw data (loadavg): 0.87 0.95 0.90 2/54 26868
Raw data (stat): 26868 (minisat+) R 26867 23176 23175 0 -1 0 2726 0 0 0 991 7 0 0 25 0 1 0 479816935 13275136 2698 4294967295 134512640 134672761 3221224560 3221223732 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3241 2698 603 41 0 3200 0
vsize: 12964
[startup+20.0004 s]
Raw data (loadavg): 0.89 0.96 0.91 2/54 26868
Raw data (stat): 26868 (minisat+) R 26867 23176 23175 0 -1 0 2741 0 0 0 1991 8 0 0 25 0 1 0 479816935 13275136 2713 4294967295 134512640 134672761 3221224560 3221223732 134556660 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3241 2713 603 41 0 3200 0
vsize: 12964
[startup+30.0014 s]
Raw data (loadavg): 0.91 0.96 0.91 2/54 26868
Raw data (stat): 26868 (minisat+) R 26867 23176 23175 0 -1 0 2757 0 0 0 2991 8 0 0 25 0 1 0 479816935 13410304 2729 4294967295 134512640 134672761 3221224560 3221223728 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3274 2729 603 41 0 3233 0
vsize: 13096
[startup+40.0009 s]
Raw data (loadavg): 0.92 0.96 0.91 2/54 26868
Raw data (stat): 26868 (minisat+) R 26867 23176 23175 0 -1 0 2782 0 0 0 3990 9 0 0 25 0 1 0 479816935 13545472 2754 4294967295 134512640 134672761 3221224560 3221223760 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3307 2754 603 41 0 3266 0
vsize: 13228
[startup+50.0022 s]
Raw data (loadavg): 0.93 0.96 0.91 2/54 26868
Raw data (stat): 26868 (minisat+) R 26867 23176 23175 0 -1 0 2802 0 0 0 4989 9 0 0 25 0 1 0 479816935 13545472 2774 4294967295 134512640 134672761 3221224560 3221223732 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3307 2774 603 41 0 3266 0
vsize: 13228
[startup+60.0031 s]
Raw data (loadavg): 0.94 0.96 0.91 2/54 26868
Raw data (stat): 26868 (minisat+) R 26867 23176 23175 0 -1 0 2829 0 0 0 5989 10 0 0 25 0 1 0 479816935 13680640 2801 4294967295 134512640 134672761 3221224560 3221223756 134556584 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3340 2801 603 41 0 3299 0
vsize: 13360
[startup+70.0037 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 26868
Raw data (stat): 26868 (minisat+) R 26867 23176 23175 0 -1 0 2871 0 0 0 6988 10 0 0 25 0 1 0 479816935 13815808 2843 4294967295 134512640 134672761 3221224560 3221223776 134561999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3373 2843 603 41 0 3332 0
vsize: 13492
[startup+80.005 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 26868
Raw data (stat): 26868 (minisat+) R 26867 23176 23175 0 -1 0 2963 0 0 0 7987 11 0 0 25 0 1 0 479816935 14221312 2935 4294967295 134512640 134672761 3221224560 3221223732 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3472 2935 603 41 0 3431 0
vsize: 13888
[startup+90.005 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 26868
Raw data (stat): 26868 (minisat+) R 26867 23176 23175 0 -1 0 3055 0 0 0 8987 12 0 0 25 0 1 0 479816935 14626816 3027 4294967295 134512640 134672761 3221224560 3221223684 134566034 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3571 3027 603 41 0 3530 0
vsize: 14284
[startup+100.005 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 26868
Raw data (stat): 26868 (minisat+) R 26867 23176 23175 0 -1 0 3173 0 0 0 9986 13 0 0 25 0 1 0 479816935 15163392 3145 4294967295 134512640 134672761 3221224560 3221223684 134566077 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3702 3145 603 41 0 3661 0
vsize: 14808
[startup+110.006 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 26868
Raw data (stat): 26868 (minisat+) R 26867 23176 23175 0 -1 0 3512 0 0 0 10985 14 0 0 25 0 1 0 479816935 16629760 3484 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4060 3484 603 41 0 4019 0
vsize: 16240
[startup+120.007 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 26868
Raw data (stat): 26868 (minisat+) R 26867 23176 23175 0 -1 0 3856 0 0 0 11985 14 0 0 25 0 1 0 479816935 17977344 3828 4294967295 134512640 134672761 3221224560 3221223760 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4389 3828 603 41 0 4348 0
vsize: 17556
[startup+130.007 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 26868
Raw data (stat): 26868 (minisat+) R 26867 23176 23175 0 -1 0 4191 0 0 0 12984 16 0 0 25 0 1 0 479816935 19329024 4163 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4719 4163 603 41 0 4678 0
vsize: 18876
[startup+140.007 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 26868
Raw data (stat): 26868 (minisat+) R 26867 23176 23175 0 -1 0 4476 0 0 0 13983 16 0 0 25 0 1 0 479816935 20406272 4448 4294967295 134512640 134672761 3221224560 3221223728 134561385 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4982 4448 603 41 0 4941 0
vsize: 19928
[startup+150.008 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 26868
Raw data (stat): 26868 (minisat+) R 26867 23176 23175 0 -1 0 4916 0 0 0 14982 18 0 0 25 0 1 0 479816935 22282240 4888 4294967295 134512640 134672761 3221224560 3221223728 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5440 4888 603 41 0 5399 0
vsize: 21760
[startup+160.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26868
Raw data (stat): 26868 (minisat+) R 26867 23176 23175 0 -1 0 5670 0 0 0 15979 21 0 0 25 0 1 0 479816935 25604096 5642 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6251 5642 603 41 0 6210 0
vsize: 25004
[startup+170.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26868
Raw data (stat): 26868 (minisat+) R 26867 23176 23175 0 -1 0 6387 0 0 0 16977 23 0 0 25 0 1 0 479816935 28426240 6359 4294967295 134512640 134672761 3221224560 3221223728 134560937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6940 6359 603 41 0 6899 0
vsize: 27760
[startup+180.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26868
Raw data (stat): 26868 (minisat+) R 26867 23176 23175 0 -1 0 6751 0 0 0 17976 24 0 0 25 0 1 0 479816935 29913088 6723 4294967295 134512640 134672761 3221224560 3221223732 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7303 6723 603 41 0 7262 0
vsize: 29212
[startup+190.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26868
Raw data (stat): 26868 (minisat+) R 26867 23176 23175 0 -1 0 7112 0 0 0 18975 26 0 0 25 0 1 0 479816935 31399936 7084 4294967295 134512640 134672761 3221224560 3221223776 134561999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7666 7084 603 41 0 7625 0
vsize: 30664
[startup+200.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26868
Raw data (stat): 26868 (minisat+) R 26867 23176 23175 0 -1 0 7471 0 0 0 19974 27 0 0 25 0 1 0 479816935 32882688 7443 4294967295 134512640 134672761 3221224560 3221223728 134560909 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8028 7443 603 41 0 7987 0
vsize: 32112
[startup+210.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26868
Raw data (stat): 26868 (minisat+) R 26867 23176 23175 0 -1 0 7994 0 0 0 20972 29 0 0 25 0 1 0 479816935 34906112 7966 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8522 7966 603 41 0 8481 0
vsize: 34088
[startup+220.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26868
Raw data (stat): 26868 (minisat+) R 26867 23176 23175 0 -1 0 8983 0 0 0 21969 32 0 0 25 0 1 0 479816935 38912000 8955 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9500 8955 603 41 0 9459 0
vsize: 38000
[startup+230.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26868
Raw data (stat): 26868 (minisat+) R 26867 23176 23175 0 -1 0 9701 0 0 0 22967 34 0 0 25 0 1 0 479816935 41865216 9673 4294967295 134512640 134672761 3221224560 3221223728 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10221 9673 603 41 0 10180 0
vsize: 40884
[startup+240.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26868
Raw data (stat): 26868 (minisat+) R 26867 23176 23175 0 -1 0 10562 0 0 0 23966 35 0 0 25 0 1 0 479816935 45355008 10534 4294967295 134512640 134672761 3221224560 3221223728 134561118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11073 10534 603 41 0 11032 0
vsize: 44292
[startup+250.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26868
Raw data (stat): 26868 (minisat+) R 26867 23176 23175 0 -1 0 11247 0 0 0 24965 37 0 0 25 0 1 0 479816935 48173056 11219 4294967295 134512640 134672761 3221224560 3221223728 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11761 11219 603 41 0 11720 0
vsize: 47044
[startup+260.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26868
Raw data (stat): 26868 (minisat+) R 26867 23176 23175 0 -1 0 11903 0 0 0 25963 39 0 0 25 0 1 0 479816935 50855936 11875 4294967295 134512640 134672761 3221224560 3221223728 134560920 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12416 11875 603 41 0 12375 0
vsize: 49664
[startup+270.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26868
Raw data (stat): 26868 (minisat+) R 26867 23176 23175 0 -1 0 12498 0 0 0 26961 41 0 0 25 0 1 0 479816935 53796864 12470 4294967295 134512640 134672761 3221224560 3221223696 134560675 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13134 12470 603 41 0 13093 0
vsize: 52536
[startup+280.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26868
Raw data (stat): 26868 (minisat+) R 26867 23176 23175 0 -1 0 12852 0 0 0 27960 42 0 0 25 0 1 0 479816935 55291904 12824 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13499 12824 603 41 0 13458 0
vsize: 53996
[startup+290.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26868
Raw data (stat): 26868 (minisat+) R 26867 23176 23175 0 -1 0 13427 0 0 0 28958 45 0 0 25 0 1 0 479816935 57565184 13399 4294967295 134512640 134672761 3221224560 3221223664 134560057 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14054 13399 603 41 0 14013 0
vsize: 56216
[startup+300.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26868
Raw data (stat): 26868 (minisat+) R 26867 23176 23175 0 -1 0 14002 0 0 0 29956 47 0 0 25 0 1 0 479816935 59977728 13974 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14643 13974 603 41 0 14602 0
vsize: 58572
[startup+310.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26868
Raw data (stat): 26868 (minisat+) R 26867 23176 23175 0 -1 0 14346 0 0 0 30955 48 0 0 25 0 1 0 479816935 61317120 14318 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14970 14318 603 41 0 14929 0
vsize: 59880
[startup+320.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26868
Raw data (stat): 26868 (minisat+) R 26867 23176 23175 0 -1 0 14742 0 0 0 31954 49 0 0 25 0 1 0 479816935 62922752 14714 4294967295 134512640 134672761 3221224560 3221223728 134561118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15362 14714 603 41 0 15321 0
vsize: 61448
[startup+330.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26868
Raw data (stat): 26868 (minisat+) R 26867 23176 23175 0 -1 0 15156 0 0 0 32953 50 0 0 25 0 1 0 479816935 64675840 15128 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15790 15128 603 41 0 15749 0
vsize: 63160
[startup+340.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26868
Raw data (stat): 26868 (minisat+) R 26867 23176 23175 0 -1 0 15565 0 0 0 33952 52 0 0 25 0 1 0 479816935 66412544 15537 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16214 15537 603 41 0 16173 0
vsize: 64856
[startup+350.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26868
Raw data (stat): 26868 (minisat+) R 26867 23176 23175 0 -1 0 15970 0 0 0 34951 53 0 0 25 0 1 0 479816935 68001792 15942 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16602 15942 603 41 0 16561 0
vsize: 66408
[startup+360.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26868
Raw data (stat): 26868 (minisat+) R 26867 23176 23175 0 -1 0 16333 0 0 0 35950 54 0 0 25 0 1 0 479816935 69492736 16305 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16966 16305 603 41 0 16925 0
vsize: 67864
[startup+370.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26868
Raw data (stat): 26868 (minisat+) R 26867 23176 23175 0 -1 0 16734 0 0 0 36949 55 0 0 25 0 1 0 479816935 71094272 16706 4294967295 134512640 134672761 3221224560 3221223728 134560937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17357 16706 603 41 0 17316 0
vsize: 69428
[startup+380.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26868
Raw data (stat): 26868 (minisat+) R 26867 23176 23175 0 -1 0 17090 0 0 0 37948 56 0 0 25 0 1 0 479816935 72556544 17062 4294967295 134512640 134672761 3221224560 3221223732 134556660 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17714 17062 603 41 0 17673 0
vsize: 70856
[startup+390.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26868
Raw data (stat): 26868 (minisat+) R 26867 23176 23175 0 -1 0 17407 0 0 0 38947 57 0 0 25 0 1 0 479816935 73904128 17379 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18043 17379 603 41 0 18002 0
vsize: 72172
[startup+400.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26868
Raw data (stat): 26868 (minisat+) R 26867 23176 23175 0 -1 0 17816 0 0 0 39946 59 0 0 25 0 1 0 479816935 75517952 17788 4294967295 134512640 134672761 3221224560 3221223728 134560937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18437 17788 603 41 0 18396 0
vsize: 73748
[startup+410.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26868
Raw data (stat): 26868 (minisat+) R 26867 23176 23175 0 -1 0 18227 0 0 0 40945 60 0 0 25 0 1 0 479816935 77254656 18199 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18861 18199 603 41 0 18820 0
vsize: 75444
[startup+420.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26868
Raw data (stat): 26868 (minisat+) R 26867 23176 23175 0 -1 0 18569 0 0 0 41944 61 0 0 25 0 1 0 479816935 78594048 18541 4294967295 134512640 134672761 3221224560 3221223760 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19188 18541 603 41 0 19147 0
vsize: 76752
[startup+430.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26868
Raw data (stat): 26868 (minisat+) R 26867 23176 23175 0 -1 0 18902 0 0 0 42944 62 0 0 25 0 1 0 479816935 80072704 18874 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19549 18874 603 41 0 19508 0
vsize: 78196
[startup+440.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26868
Raw data (stat): 26868 (minisat+) R 26867 23176 23175 0 -1 0 19226 0 0 0 43943 63 0 0 25 0 1 0 479816935 81412096 19198 4294967295 134512640 134672761 3221224560 3221223728 134561207 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19876 19198 603 41 0 19835 0
vsize: 79504
[startup+450.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26868
Raw data (stat): 26868 (minisat+) R 26867 23176 23175 0 -1 0 19396 0 0 0 44943 63 0 0 25 0 1 0 479816935 82092032 19368 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20042 19368 603 41 0 20001 0
vsize: 80168
[startup+460.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26868
Raw data (stat): 26868 (minisat+) R 26867 23176 23175 0 -1 0 19396 0 0 0 45943 63 0 0 25 0 1 0 479816935 82092032 19368 4294967295 134512640 134672761 3221224560 3221223728 134560852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20042 19368 603 41 0 20001 0
vsize: 80168
[startup+470.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26868
Raw data (stat): 26868 (minisat+) R 26867 23176 23175 0 -1 0 19396 0 0 0 46943 63 0 0 25 0 1 0 479816935 82092032 19368 4294967295 134512640 134672761 3221224560 3221223728 134561205 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20042 19368 603 41 0 20001 0
vsize: 80168
[startup+480.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26868
Raw data (stat): 26868 (minisat+) R 26867 23176 23175 0 -1 0 19396 0 0 0 47943 63 0 0 25 0 1 0 479816935 82092032 19368 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20042 19368 603 41 0 20001 0
vsize: 80168
[startup+490.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26868
Raw data (stat): 26868 (minisat+) R 26867 23176 23175 0 -1 0 19396 0 0 0 48942 63 0 0 25 0 1 0 479816935 82092032 19368 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20042 19368 603 41 0 20001 0
vsize: 80168
[startup+500.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26868
Raw data (stat): 26868 (minisat+) R 26867 23176 23175 0 -1 0 19396 0 0 0 49943 63 0 0 25 0 1 0 479816935 82092032 19368 4294967295 134512640 134672761 3221224560 3221223664 134560285 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20042 19368 603 41 0 20001 0
vsize: 80168
[startup+510.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26868
Raw data (stat): 26868 (minisat+) R 26867 23176 23175 0 -1 0 19396 0 0 0 50943 63 0 0 25 0 1 0 479816935 82092032 19368 4294967295 134512640 134672761 3221224560 3221223732 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20042 19368 603 41 0 20001 0
vsize: 80168
[startup+520.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26868
Raw data (stat): 26868 (minisat+) R 26867 23176 23175 0 -1 0 19396 0 0 0 51943 63 0 0 25 0 1 0 479816935 82092032 19368 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20042 19368 603 41 0 20001 0
vsize: 80168
[startup+530.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26868
Raw data (stat): 26868 (minisat+) R 26867 23176 23175 0 -1 0 19396 0 0 0 52943 63 0 0 25 0 1 0 479816935 82092032 19368 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20042 19368 603 41 0 20001 0
vsize: 80168
[startup+540.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26868
Raw data (stat): 26868 (minisat+) R 26867 23176 23175 0 -1 0 19396 0 0 0 53943 63 0 0 25 0 1 0 479816935 82092032 19368 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20042 19368 603 41 0 20001 0
vsize: 80168
[startup+550.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26868
Raw data (stat): 26868 (minisat+) R 26867 23176 23175 0 -1 0 19397 0 0 0 54944 63 0 0 25 0 1 0 479816935 82092032 19369 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20042 19369 603 41 0 20001 0
vsize: 80168
[startup+560.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26868
Raw data (stat): 26868 (minisat+) R 26867 23176 23175 0 -1 0 19399 0 0 0 55944 63 0 0 25 0 1 0 479816935 82092032 19371 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20042 19371 603 41 0 20001 0
vsize: 80168
[startup+570.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26868
Raw data (stat): 26868 (minisat+) R 26867 23176 23175 0 -1 0 19400 0 0 0 56944 63 0 0 25 0 1 0 479816935 82092032 19372 4294967295 134512640 134672761 3221224560 3221223728 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20042 19372 603 41 0 20001 0
vsize: 80168
[startup+580.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26868
Raw data (stat): 26868 (minisat+) R 26867 23176 23175 0 -1 0 19400 0 0 0 57944 63 0 0 25 0 1 0 479816935 82092032 19372 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20042 19372 603 41 0 20001 0
vsize: 80168
[startup+590.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26868
Raw data (stat): 26868 (minisat+) R 26867 23176 23175 0 -1 0 19401 0 0 0 58944 63 0 0 25 0 1 0 479816935 82092032 19373 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20042 19373 603 41 0 20001 0
vsize: 80168
[startup+600.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26868
Raw data (stat): 26868 (minisat+) R 26867 23176 23175 0 -1 0 19402 0 0 0 59944 63 0 0 25 0 1 0 479816935 82092032 19374 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20042 19374 603 41 0 20001 0
vsize: 80168
[startup+610.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26868
Raw data (stat): 26868 (minisat+) R 26867 23176 23175 0 -1 0 19402 0 0 0 60945 63 0 0 25 0 1 0 479816935 82092032 19374 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20042 19374 603 41 0 20001 0
vsize: 80168
[startup+620.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26868
Raw data (stat): 26868 (minisat+) R 26867 23176 23175 0 -1 0 19402 0 0 0 61945 63 0 0 25 0 1 0 479816935 82092032 19374 4294967295 134512640 134672761 3221224560 3221223728 134560858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20042 19374 603 41 0 20001 0
vsize: 80168
[startup+630.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26868
Raw data (stat): 26868 (minisat+) R 26867 23176 23175 0 -1 0 19402 0 0 0 62945 63 0 0 25 0 1 0 479816935 82092032 19374 4294967295 134512640 134672761 3221224560 3221223728 134560906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20042 19374 603 41 0 20001 0
vsize: 80168
[startup+640.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26868
Raw data (stat): 26868 (minisat+) R 26867 23176 23175 0 -1 0 19402 0 0 0 63945 63 0 0 25 0 1 0 479816935 82092032 19374 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20042 19374 603 41 0 20001 0
vsize: 80168
[startup+650.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26868
Raw data (stat): 26868 (minisat+) R 26867 23176 23175 0 -1 0 19403 0 0 0 64945 63 0 0 25 0 1 0 479816935 82092032 19375 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20042 19375 603 41 0 20001 0
vsize: 80168
[startup+660.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26868
Raw data (stat): 26868 (minisat+) R 26867 23176 23175 0 -1 0 19405 0 0 0 65946 63 0 0 25 0 1 0 479816935 82092032 19377 4294967295 134512640 134672761 3221224560 3221223728 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20042 19377 603 41 0 20001 0
vsize: 80168
[startup+670.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26868
Raw data (stat): 26868 (minisat+) R 26867 23176 23175 0 -1 0 19405 0 0 0 66946 63 0 0 25 0 1 0 479816935 82092032 19377 4294967295 134512640 134672761 3221224560 3221223728 134561127 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20042 19377 603 41 0 20001 0
vsize: 80168
[startup+680.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26868
Raw data (stat): 26868 (minisat+) R 26867 23176 23175 0 -1 0 19405 0 0 0 67946 63 0 0 25 0 1 0 479816935 82092032 19377 4294967295 134512640 134672761 3221224560 3221223728 134560920 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20042 19377 603 41 0 20001 0
vsize: 80168
[startup+690.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26868
Raw data (stat): 26868 (minisat+) R 26867 23176 23175 0 -1 0 19405 0 0 0 68946 63 0 0 25 0 1 0 479816935 82092032 19377 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20042 19377 603 41 0 20001 0
vsize: 80168
[startup+700.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26868
Raw data (stat): 26868 (minisat+) R 26867 23176 23175 0 -1 0 19405 0 0 0 69946 63 0 0 25 0 1 0 479816935 82092032 19377 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20042 19377 603 41 0 20001 0
vsize: 80168
[startup+710.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26868
Raw data (stat): 26868 (minisat+) R 26867 23176 23175 0 -1 0 19405 0 0 0 70947 63 0 0 25 0 1 0 479816935 82092032 19377 4294967295 134512640 134672761 3221224560 3221223728 134560858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20042 19377 603 41 0 20001 0
vsize: 80168
[startup+720.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26868
Raw data (stat): 26868 (minisat+) R 26867 23176 23175 0 -1 0 19405 0 0 0 71947 63 0 0 25 0 1 0 479816935 82092032 19377 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20042 19377 603 41 0 20001 0
vsize: 80168
[startup+730.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26868
Raw data (stat): 26868 (minisat+) R 26867 23176 23175 0 -1 0 19405 0 0 0 72947 63 0 0 25 0 1 0 479816935 82092032 19377 4294967295 134512640 134672761 3221224560 3221223664 134560243 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20042 19377 603 41 0 20001 0
vsize: 80168
[startup+740.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26868
Raw data (stat): 26868 (minisat+) R 26867 23176 23175 0 -1 0 19405 0 0 0 73947 63 0 0 25 0 1 0 479816935 82092032 19377 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20042 19377 603 41 0 20001 0
vsize: 80168
[startup+750.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26868
Raw data (stat): 26868 (minisat+) R 26867 23176 23175 0 -1 0 19405 0 0 0 74947 63 0 0 25 0 1 0 479816935 82092032 19377 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20042 19377 603 41 0 20001 0
vsize: 80168
[startup+760.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26868
Raw data (stat): 26868 (minisat+) R 26867 23176 23175 0 -1 0 19407 0 0 0 75947 63 0 0 25 0 1 0 479816935 82092032 19379 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20042 19379 603 41 0 20001 0
vsize: 80168
[startup+770.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26868
Raw data (stat): 26868 (minisat+) R 26867 23176 23175 0 -1 0 19616 0 0 0 76947 64 0 0 25 0 1 0 479816935 82915328 19588 4294967295 134512640 134672761 3221224560 3221223728 134561156 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20243 19588 603 41 0 20202 0
vsize: 80972
[startup+780.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26868
Raw data (stat): 26868 (minisat+) R 26867 23176 23175 0 -1 0 19859 0 0 0 77946 65 0 0 25 0 1 0 479816935 83980288 19831 4294967295 134512640 134672761 3221224560 3221223728 134560912 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20503 19831 603 41 0 20462 0
vsize: 82012
[startup+790.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26868
Raw data (stat): 26868 (minisat+) R 26867 23176 23175 0 -1 0 20088 0 0 0 78946 65 0 0 25 0 1 0 479816935 84918272 20060 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20732 20060 603 41 0 20691 0
vsize: 82928
[startup+800.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26868
Raw data (stat): 26868 (minisat+) R 26867 23176 23175 0 -1 0 20327 0 0 0 79946 66 0 0 25 0 1 0 479816935 85852160 20299 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20960 20299 603 41 0 20919 0
vsize: 83840
[startup+810.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26868
Raw data (stat): 26868 (minisat+) R 26867 23176 23175 0 -1 0 20591 0 0 0 80945 67 0 0 25 0 1 0 479816935 86913024 20563 4294967295 134512640 134672761 3221224560 3221223728 134560937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21219 20563 603 41 0 21178 0
vsize: 84876
[startup+820.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26868
Raw data (stat): 26868 (minisat+) R 26867 23176 23175 0 -1 0 20840 0 0 0 81944 67 0 0 25 0 1 0 479816935 87973888 20812 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21478 20812 603 41 0 21437 0
vsize: 85912
[startup+830.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26868
Raw data (stat): 26868 (minisat+) R 26867 23176 23175 0 -1 0 21097 0 0 0 82944 68 0 0 25 0 1 0 479816935 89047040 21069 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21740 21069 603 41 0 21699 0
vsize: 86960
[startup+840.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26868
Raw data (stat): 26868 (minisat+) R 26867 23176 23175 0 -1 0 21339 0 0 0 83943 69 0 0 25 0 1 0 479816935 89997312 21311 4294967295 134512640 134672761 3221224560 3221223728 134560895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21972 21311 603 41 0 21931 0
vsize: 87888
[startup+850.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26868
Raw data (stat): 26868 (minisat+) R 26867 23176 23175 0 -1 0 21577 0 0 0 84943 69 0 0 25 0 1 0 479816935 91062272 21549 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22232 21549 603 41 0 22191 0
vsize: 88928
[startup+860.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26868
Raw data (stat): 26868 (minisat+) R 26867 23176 23175 0 -1 0 21847 0 0 0 85943 70 0 0 25 0 1 0 479816935 92225536 21819 4294967295 134512640 134672761 3221224560 3221223728 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22516 21819 603 41 0 22475 0
vsize: 90064
[startup+870.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26868
Raw data (stat): 26868 (minisat+) R 26867 23176 23175 0 -1 0 22088 0 0 0 86942 71 0 0 25 0 1 0 479816935 93302784 22060 4294967295 134512640 134672761 3221224560 3221223728 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22779 22060 603 41 0 22738 0
vsize: 91116
[startup+880.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26868
Raw data (stat): 26868 (minisat+) R 26867 23176 23175 0 -1 0 22247 0 0 0 87942 71 0 0 25 0 1 0 479816935 93995008 22219 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22948 22219 603 41 0 22907 0
vsize: 91792
[startup+890.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26868
Raw data (stat): 26868 (minisat+) R 26867 23176 23175 0 -1 0 22407 0 0 0 88941 72 0 0 25 0 1 0 479816935 94666752 22379 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23112 22379 603 41 0 23071 0
vsize: 92448
[startup+900.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26868
Raw data (stat): 26868 (minisat+) R 26867 23176 23175 0 -1 0 22623 0 0 0 89941 72 0 0 25 0 1 0 479816935 95604736 22595 4294967295 134512640 134672761 3221224560 3221223728 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23341 22595 603 41 0 23300 0
vsize: 93364
[startup+910.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26868
Raw data (stat): 26868 (minisat+) R 26867 23176 23175 0 -1 0 22867 0 0 0 90941 72 0 0 25 0 1 0 479816935 96534528 22839 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23568 22839 603 41 0 23527 0
vsize: 94272
[startup+920.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26868
Raw data (stat): 26868 (minisat+) R 26867 23176 23175 0 -1 0 23051 0 0 0 91941 73 0 0 25 0 1 0 479816935 97349632 23023 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23767 23023 603 41 0 23726 0
vsize: 95068
[startup+930.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26868
Raw data (stat): 26868 (minisat+) R 26867 23176 23175 0 -1 0 23312 0 0 0 92940 74 0 0 25 0 1 0 479816935 98414592 23284 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24027 23284 603 41 0 23986 0
vsize: 96108
[startup+940.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26868
Raw data (stat): 26868 (minisat+) R 26867 23176 23175 0 -1 0 23523 0 0 0 93940 74 0 0 25 0 1 0 479816935 99373056 23495 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24261 23495 603 41 0 24220 0
vsize: 97044
[startup+950.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26868
Raw data (stat): 26868 (minisat+) R 26867 23176 23175 0 -1 0 23670 0 0 0 94939 75 0 0 25 0 1 0 479816935 99938304 23642 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24399 23642 603 41 0 24358 0
vsize: 97596
[startup+960.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26868
Raw data (stat): 26868 (minisat+) R 26867 23176 23175 0 -1 0 23867 0 0 0 95939 75 0 0 25 0 1 0 479816935 100765696 23839 4294967295 134512640 134672761 3221224560 3221223728 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24601 23839 603 41 0 24560 0
vsize: 98404
[startup+970.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26868
Raw data (stat): 26868 (minisat+) R 26867 23176 23175 0 -1 0 24023 0 0 0 96939 76 0 0 25 0 1 0 479816935 101441536 23995 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24766 23995 603 41 0 24725 0
vsize: 99064
[startup+980.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26868
Raw data (stat): 26868 (minisat+) R 26867 23176 23175 0 -1 0 24201 0 0 0 97939 76 0 0 25 0 1 0 479816935 102281216 24173 4294967295 134512640 134672761 3221224560 3221223728 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24971 24173 603 41 0 24930 0
vsize: 99884
[startup+990.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26868
Raw data (stat): 26868 (minisat+) R 26867 23176 23175 0 -1 0 24362 0 0 0 98938 76 0 0 25 0 1 0 479816935 102952960 24334 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25135 24334 603 41 0 25094 0
vsize: 100540
[startup+1000.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26868
Raw data (stat): 26868 (minisat+) R 26867 23176 23175 0 -1 0 24536 0 0 0 99938 77 0 0 25 0 1 0 479816935 103620608 24508 4294967295 134512640 134672761 3221224560 3221223728 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25298 24508 603 41 0 25257 0
vsize: 101192
[startup+1010.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26868
Raw data (stat): 26868 (minisat+) R 26867 23176 23175 0 -1 0 24736 0 0 0 100938 78 0 0 25 0 1 0 479816935 104423424 24708 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25494 24708 603 41 0 25453 0
vsize: 101976
[startup+1020.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26868
Raw data (stat): 26868 (minisat+) R 26867 23176 23175 0 -1 0 24928 0 0 0 101937 78 0 0 25 0 1 0 479816935 105226240 24900 4294967295 134512640 134672761 3221224560 3221223728 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25690 24900 603 41 0 25649 0
vsize: 102760
[startup+1030.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26868
Raw data (stat): 26868 (minisat+) R 26867 23176 23175 0 -1 0 25114 0 0 0 102937 79 0 0 25 0 1 0 479816935 106020864 25086 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25884 25086 603 41 0 25843 0
vsize: 103536
[startup+1040.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26868
Raw data (stat): 26868 (minisat+) R 26867 23176 23175 0 -1 0 25287 0 0 0 103937 79 0 0 25 0 1 0 479816935 106692608 25259 4294967295 134512640 134672761 3221224560 3221223728 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26048 25259 603 41 0 26007 0
vsize: 104192
[startup+1050.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26868
Raw data (stat): 26868 (minisat+) R 26867 23176 23175 0 -1 0 25478 0 0 0 104937 79 0 0 25 0 1 0 479816935 107499520 25450 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26245 25450 603 41 0 26204 0
vsize: 104980
[startup+1060.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26868
Raw data (stat): 26868 (minisat+) R 26867 23176 23175 0 -1 0 25693 0 0 0 105936 80 0 0 25 0 1 0 479816935 108429312 25665 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26472 25665 603 41 0 26431 0
vsize: 105888
[startup+1070.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26868
Raw data (stat): 26868 (minisat+) R 26867 23176 23175 0 -1 0 25918 0 0 0 106936 81 0 0 25 0 1 0 479816935 109268992 25890 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26677 25890 603 41 0 26636 0
vsize: 106708
[startup+1080.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26868
Raw data (stat): 26868 (minisat+) R 26867 23176 23175 0 -1 0 26135 0 0 0 107935 81 0 0 25 0 1 0 479816935 110231552 26107 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26912 26107 603 41 0 26871 0
vsize: 107648
[startup+1090.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26868
Raw data (stat): 26868 (minisat+) R 26867 23176 23175 0 -1 0 26345 0 0 0 108935 82 0 0 25 0 1 0 479816935 111026176 26317 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27106 26317 603 41 0 27065 0
vsize: 108424
[startup+1100.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26868
Raw data (stat): 26868 (minisat+) R 26867 23176 23175 0 -1 0 26521 0 0 0 109935 82 0 0 25 0 1 0 479816935 111923200 26493 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27325 26493 603 41 0 27284 0
vsize: 109300
[startup+1110.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26868
Raw data (stat): 26868 (minisat+) R 26867 23176 23175 0 -1 0 26696 0 0 0 110934 83 0 0 25 0 1 0 479816935 112603136 26668 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27491 26668 603 41 0 27450 0
vsize: 109964
[startup+1120.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26868
Raw data (stat): 26868 (minisat+) R 26867 23176 23175 0 -1 0 26928 0 0 0 111934 84 0 0 25 0 1 0 479816935 113549312 26900 4294967295 134512640 134672761 3221224560 3221223728 134561139 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27722 26900 603 41 0 27681 0
vsize: 110888
[startup+1130.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26868
Raw data (stat): 26868 (minisat+) R 26867 23176 23175 0 -1 0 27105 0 0 0 112934 84 0 0 25 0 1 0 479816935 114343936 27077 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27916 27077 603 41 0 27875 0
vsize: 111664
[startup+1140.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26868
Raw data (stat): 26868 (minisat+) R 26867 23176 23175 0 -1 0 27298 0 0 0 113933 85 0 0 25 0 1 0 479816935 115179520 27270 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28120 27270 603 41 0 28079 0
vsize: 112480
[startup+1150.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26868
Raw data (stat): 26868 (minisat+) R 26867 23176 23175 0 -1 0 27473 0 0 0 114933 86 0 0 25 0 1 0 479816935 115920896 27445 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28301 27445 603 41 0 28260 0
vsize: 113204
[startup+1160.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26868
Raw data (stat): 26868 (minisat+) R 26867 23176 23175 0 -1 0 27679 0 0 0 115932 86 0 0 25 0 1 0 479816935 116719616 27651 4294967295 134512640 134672761 3221224560 3221223728 134560920 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28496 27651 603 41 0 28455 0
vsize: 113984
[startup+1170.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26868
Raw data (stat): 26868 (minisat+) R 26867 23176 23175 0 -1 0 27870 0 0 0 116932 87 0 0 25 0 1 0 479816935 117514240 27842 4294967295 134512640 134672761 3221224560 3221223728 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28690 27842 603 41 0 28649 0
vsize: 114760
[startup+1180.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26868
Raw data (stat): 26868 (minisat+) R 26867 23176 23175 0 -1 0 28062 0 0 0 117931 88 0 0 25 0 1 0 479816935 118312960 28034 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28885 28034 603 41 0 28844 0
vsize: 115540
[startup+1190.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26868
Raw data (stat): 26868 (minisat+) R 26867 23176 23175 0 -1 0 28274 0 0 0 118930 89 0 0 25 0 1 0 479816935 119242752 28246 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29112 28246 603 41 0 29071 0
vsize: 116448
[startup+1200.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26868
Raw data (stat): 26868 (minisat+) R 26867 23176 23175 0 -1 0 28438 0 0 0 119930 89 0 0 25 0 1 0 479816935 119914496 28410 4294967295 134512640 134672761 3221224560 3221223732 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29276 28410 603 41 0 29235 0
vsize: 117104
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.11 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 26868
Raw data (stat): 26868 (minisat+) Z 26867 23176 23175 0 -1 12 28440 0 0 0 119930 94 0 0 25 0 1 0 479816935 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.1
CPU time (s): 1200.26
CPU user time (s): 1199.31
CPU system time (s): 0.948855
CPU usage (%): 100.013
Max. virtual memory (Kb): 117104
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####