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-13.opb
MD5SUM	4caec1e880871fcef3276cf001aca352
Bench Category	no optimization function (SAT)
Has Objective Function	NO
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	0
Optimality of the best value was proved	NO
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	104
Number of bits of the biggest sum of numbers	7
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	7.63384
Number of variables	4632
Total number of constraints	35596
Number of constraints which are clauses	29940
Number of constraints which are cardinality constraints (but not clauses)	5578
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 5283

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc22 THE 2005-04-13 23:16:27 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3747 boxname=wulflinc22 idbench=363 idsolver=10 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  4caec1e880871fcef3276cf001aca352  /oldhome/oroussel/tmp/wulflinc22/normalized-ppp:1-13.opb
REAL COMMAND:  minisat+ -ca /oldhome/oroussel/tmp/wulflinc22/normalized-ppp:1-13.opb /oldhome/oroussel/tmp/wulflinc22/normalized-ppp:1-13.opb
IDLAUNCH: 3747
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.031
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	: 890.88

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        854276 kB
Buffers:         31672 kB
Cached:         105368 kB
SwapCached:        524 kB
Active:          47544 kB
Inactive:        92856 kB
HighTotal:      131008 kB
HighFree:        21924 kB
LowTotal:       903652 kB
LowFree:        832352 kB
SwapTotal:     2097892 kB
SwapFree:      2097368 kB
Dirty:              36 kB
Writeback:           0 kB
Mapped:           6924 kB
Slab:            34528 kB
Committed_AS:    63480 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-13 23:36:30 (client local time) WITH STATUS 0 IN 1200.25 SECONDS
stats: 3747 7 1200.25 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 31138 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ##############################################################################################################################################################################
c   -- Clauses(.)/Splits(s): ....................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ---[31137]---> Adder-cost: 48   maxlim: 61   bits: 7/6
c ---[31136]---> Adder-cost: 48   maxlim: 61   bits: 7/6
c ---[31135]---> Adder-cost: 48   maxlim: 61   bits: 7/6
c ---[31134]---> Adder-cost: 48   maxlim: 61   bits: 7/6
c ---[31133]---> Adder-cost: 48   maxlim: 61   bits: 7/6
c ---[31132]---> Adder-cost: 48   maxlim: 61   bits: 7/6
c ---[31131]---> Adder-cost: 64   maxlim: 86   bits: 7/7
c ---[31130]---> Adder-cost: 64   maxlim: 86   bits: 7/7
c ---[31129]---> Adder-cost: 64   maxlim: 86   bits: 7/7
c ---[31128]---> Adder-cost: 64   maxlim: 86   bits: 7/7
c ---[31127]---> Adder-cost: 64   maxlim: 86   bits: 7/7
c ---[31126]---> Adder-cost: 64   maxlim: 86   bits: 7/7
c ---[31125]---> Adder-cost: 64   maxlim: 85   bits: 7/7
c ---[31124]---> Adder-cost: 64   maxlim: 85   bits: 7/7
c ---[31123]---> Adder-cost: 64   maxlim: 85   bits: 7/7
c ---[31122]---> Adder-cost: 64   maxlim: 85   bits: 7/7
c ---[31121]---> Adder-cost: 64   maxlim: 85   bits: 7/7
c ---[31120]---> Adder-cost: 64   maxlim: 85   bits: 7/7
c ---[31119]---> Adder-cost: 64   maxlim: 85   bits: 7/7
c ---[31118]---> Adder-cost: 64   maxlim: 85   bits: 7/7
c ---[31117]---> Adder-cost: 64   maxlim: 85   bits: 7/7
c ---[31116]---> Adder-cost: 64   maxlim: 85   bits: 7/7
c ---[31115]---> Adder-cost: 64   maxlim: 85   bits: 7/7
c ---[31114]---> Adder-cost: 64   maxlim: 85   bits: 7/7
c ---[31113]---> Adder-cost: 64   maxlim: 85   bits: 7/7
c ---[31112]---> Adder-cost: 64   maxlim: 85   bits: 7/7
c ---[31111]---> Adder-cost: 64   maxlim: 85   bits: 7/7
c ---[31110]---> Adder-cost: 64   maxlim: 85   bits: 7/7
c ---[31109]---> Adder-cost: 64   maxlim: 85   bits: 7/7
c ---[31108]---> Adder-cost: 64   maxlim: 85   bits: 7/7
c ---[31107]---> Adder-cost: 64   maxlim: 84   bits: 7/7
c ---[31106]---> Adder-cost: 64   maxlim: 84   bits: 7/7
c ---[31105]---> Adder-cost: 64   maxlim: 84   bits: 7/7
c ---[31104]---> Adder-cost: 64   maxlim: 84   bits: 7/7
c ---[31103]---> Adder-cost: 64   maxlim: 84   bits: 7/7
c ---[31102]---> Adder-cost: 64   maxlim: 84   bits: 7/7
c ---[31101]---> Adder-cost: 64   maxlim: 85   bits: 7/7
c ---[31100]---> Adder-cost: 64   maxlim: 85   bits: 7/7
c ---[31099]---> Adder-cost: 64   maxlim: 85   bits: 7/7
c ---[31098]---> Adder-cost: 64   maxlim: 85   bits: 7/7
c ---[31097]---> Adder-cost: 64   maxlim: 85   bits: 7/7
c ---[31096]---> Adder-cost: 64   maxlim: 85   bits: 7/7
c ---[31095]---> Adder-cost: 64   maxlim: 85   bits: 7/7
c ---[31094]---> Adder-cost: 64   maxlim: 85   bits: 7/7
c ---[31093]---> Adder-cost: 64   maxlim: 85   bits: 7/7
c ---[31092]---> Adder-cost: 64   maxlim: 85   bits: 7/7
c ---[31091]---> Adder-cost: 64   maxlim: 85   bits: 7/7
c ---[31090]---> Adder-cost: 64   maxlim: 85   bits: 7/7
c ---[31089]---> Adder-cost: 64   maxlim: 85   bits: 7/7
c ---[31088]---> Adder-cost: 64   maxlim: 85   bits: 7/7
c ---[31087]---> Adder-cost: 64   maxlim: 85   bits: 7/7
c ---[31086]---> Adder-cost: 64   maxlim: 85   bits: 7/7
c ---[31085]---> Adder-cost: 64   maxlim: 85   bits: 7/7
c ---[31084]---> Adder-cost: 64   maxlim: 85   bits: 7/7
c ---[31083]---> Adder-cost: 64   maxlim: 83   bits: 7/7
c ---[31082]---> Adder-cost: 64   maxlim: 83   bits: 7/7
c ---[31081]---> Adder-cost: 64   maxlim: 83   bits: 7/7
c ---[31080]---> Adder-cost: 64   maxlim: 83   bits: 7/7
c ---[31079]---> Adder-cost: 64   maxlim: 83   bits: 7/7
c ---[31078]---> Adder-cost: 64   maxlim: 83   bits: 7/7
c ---[31077]---> Adder-cost: 64   maxlim: 83   bits: 7/7
c ---[31076]---> Adder-cost: 64   maxlim: 83   bits: 7/7
c ---[31075]---> Adder-cost: 64   maxlim: 83   bits: 7/7
c ---[31074]---> Adder-cost: 64   maxlim: 83   bits: 7/7
c ---[31073]---> Adder-cost: 64   maxlim: 83   bits: 7/7
c ---[31072]---> Adder-cost: 64   maxlim: 83   bits: 7/7
c ---[31071]---> Adder-cost: 58   maxlim: 80   bits: 7/7
c ---[31070]---> Adder-cost: 58   maxlim: 80   bits: 7/7
c ---[31069]---> Adder-cost: 58   maxlim: 80   bits: 7/7
c ---[31068]---> Adder-cost: 58   maxlim: 80   bits: 7/7
c ---[31067]---> Adder-cost: 58   maxlim: 80   bits: 7/7
c ---[31066]---> Adder-cost: 58   maxlim: 80   bits: 7/7
c ---[31065]---> Adder-cost: 48   maxlim: 61   bits: 7/6
c ---[31064]---> Adder-cost: 48   maxlim: 61   bits: 7/6
c ---[31063]---> Adder-cost: 48   maxlim: 61   bits: 7/6
c ---[31062]---> Adder-cost: 48   maxlim: 61   bits: 7/6
c ---[31061]---> Adder-cost: 48   maxlim: 61   bits: 7/6
c ---[31060]---> Adder-cost: 48   maxlim: 61   bits: 7/6
c ---[31058]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31056]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31054]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31052]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31050]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31048]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31046]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31044]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31042]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31040]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31038]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31036]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31034]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31032]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31030]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31028]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31026]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31024]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31022]---> Adder-cost: 16   maxlim: 10   bits: 4/4
c ---[31020]---> Adder-cost: 16   maxlim: 10   bits: 4/4
c ---[31018]---> Adder-cost: 16   maxlim: 10   bits: 4/4
c ---[31016]---> Adder-cost: 16   maxlim: 10   bits: 4/4
c ---[31014]---> Adder-cost: 16   maxlim: 10   bits: 4/4
c ---[31012]---> Adder-cost: 16   maxlim: 10   bits: 4/4
c ---[31010]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31008]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31006]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31004]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31002]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31000]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30998]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30996]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30994]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30992]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30990]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30988]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30986]---> Adder-cost: 16   maxlim: 10   bits: 4/4
c ---[30984]---> Adder-cost: 16   maxlim: 10   bits: 4/4
c ---[30982]---> Adder-cost: 16   maxlim: 10   bits: 4/4
c ---[30980]---> Adder-cost: 16   maxlim: 10   bits: 4/4
c ---[30978]---> Adder-cost: 16   maxlim: 10   bits: 4/4
c ---[30976]---> Adder-cost: 16   maxlim: 10   bits: 4/4
c ---[30974]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[30972]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[30970]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[30968]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[30966]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[30964]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[30962]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30960]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30958]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30956]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30954]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30952]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30950]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30948]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30946]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30944]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30942]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30940]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30938]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30936]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30934]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30932]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30930]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30928]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30926]---> Adder-cost: 16   maxlim: 10   bits: 4/4
c ---[30924]---> Adder-cost: 16   maxlim: 10   bits: 4/4
c ---[30922]---> Adder-cost: 16   maxlim: 10   bits: 4/4
c ---[30920]---> Adder-cost: 16   maxlim: 10   bits: 4/4
c ---[30918]---> Adder-cost: 16   maxlim: 10   bits: 4/4
c ---[30916]---> Adder-cost: 16   maxlim: 10   bits: 4/4
c ---[30914]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30912]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30910]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30908]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30906]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30904]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30902]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30900]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30898]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30896]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30894]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30892]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30890]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30888]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30886]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30884]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30882]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30880]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30878]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30876]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30874]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30872]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30870]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30868]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30866]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30864]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30862]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30860]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30858]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30856]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30854]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30852]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30850]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30848]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30846]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30844]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30842]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30840]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30838]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30836]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30834]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30832]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30830]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30828]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30826]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30824]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30822]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30820]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30818]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30816]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30814]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30812]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30810]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30808]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30806]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30804]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30802]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30800]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30798]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30796]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30794]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30792]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30790]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30788]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30786]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30784]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30782]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30780]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30778]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30776]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30774]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30772]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30770]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30768]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30766]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30764]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30762]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30760]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30758]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30756]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30754]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30752]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30750]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30748]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30746]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30744]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30742]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30740]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30738]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30736]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30734]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30732]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30730]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30728]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30726]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30724]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30722]---> Adder-cost: 16   maxlim: 10   bits: 4/4
c ---[30720]---> Adder-cost: 16   maxlim: 10   bits: 4/4
c ---[30718]---> Adder-cost: 16   maxlim: 10   bits: 4/4
c ---[30716]---> Adder-cost: 16   maxlim: 10   bits: 4/4
c ---[30714]---> Adder-cost: 16   maxlim: 10   bits: 4/4
c ---[30712]---> Adder-cost: 16   maxlim: 10   bits: 4/4
c ---[30711]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30710]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30709]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30708]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30707]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30706]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30705]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30704]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30703]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30702]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30701]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30700]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30699]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30698]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30697]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30696]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30695]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30694]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30693]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30692]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30691]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30690]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30689]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30688]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30687]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30686]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30685]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30684]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30683]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30682]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30681]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30680]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30679]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30678]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30677]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30676]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30675]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30674]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30673]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30672]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30671]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30670]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30669]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30668]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30667]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30666]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30665]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30664]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30663]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30662]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30661]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30660]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30659]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30658]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30657]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30656]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30655]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30654]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30653]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30652]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30651]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30650]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30649]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30648]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30647]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30646]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30645]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30644]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30643]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30642]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30641]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30640]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30639]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30638]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30637]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30636]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30635]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30634]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30633]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30632]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30631]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30630]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30629]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30628]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30627]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30626]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30625]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30624]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30623]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30622]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30621]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30620]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30619]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30618]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30617]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30616]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30615]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30614]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30613]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30612]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30611]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30610]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30609]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30608]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30607]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30606]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30605]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30604]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30603]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30602]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30601]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30600]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30599]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30598]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30597]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30596]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30595]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30594]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30593]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30592]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30591]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30590]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30589]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30588]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30587]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30586]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30585]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30584]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30583]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30582]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30581]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30580]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30579]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30578]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30577]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30576]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30575]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30574]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30573]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30572]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30571]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30570]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30569]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30568]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30567]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30566]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30565]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30564]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30563]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30562]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30561]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30560]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30559]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30558]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30557]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30556]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30555]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30554]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30553]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30552]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30551]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30550]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30549]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30548]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30547]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30546]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30545]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30544]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30543]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30542]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30541]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30540]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30539]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30538]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30537]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30536]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30535]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30534]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30533]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30532]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30531]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30530]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30529]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30528]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30527]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30526]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30525]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30524]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30523]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30522]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30521]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30520]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30519]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30518]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30517]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30516]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30515]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30514]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30513]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30512]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30511]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30510]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30509]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30508]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30507]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30506]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30505]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30504]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30503]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30502]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30501]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30500]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30499]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30498]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30497]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30496]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30495]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30494]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30493]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30492]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30491]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30490]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30489]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30488]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30487]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30486]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30485]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30484]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30483]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30482]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30481]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30480]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30479]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30478]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30477]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30476]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30475]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30474]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30473]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30472]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30471]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30470]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30469]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30468]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30467]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30466]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30465]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30464]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30463]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30462]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30461]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30460]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30459]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30458]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30457]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30456]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30455]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30454]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30453]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30452]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30451]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30450]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30449]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30448]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30447]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30446]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30445]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30444]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30443]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30442]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30441]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30440]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30439]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30438]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30437]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30436]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30435]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30434]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30433]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30432]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30431]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30430]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30429]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30428]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30427]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30426]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30425]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30424]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30423]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30422]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30421]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30420]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30419]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30418]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30417]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30416]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30415]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30414]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30413]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30412]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30411]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30410]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30409]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30408]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30407]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30406]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30405]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30404]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30403]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30402]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30401]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30400]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30399]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30398]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30397]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30396]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30395]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30394]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30393]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30392]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30391]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30390]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30389]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30388]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30387]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30386]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30385]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30384]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30383]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30382]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30381]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30380]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30379]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30378]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30377]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30376]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30375]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30374]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30373]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30372]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30371]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30370]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30369]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30368]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30367]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30366]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30365]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30364]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30363]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30362]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30361]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30360]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30359]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30358]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30357]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30356]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30355]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30354]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30353]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30352]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30351]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30350]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30349]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30348]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30347]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30346]---> 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 |  111464   376282 |   37154       0        0     nan |  0.000 % |
c |       100 |  110754   373874 |   40869      20       50     2.5 | 17.319 % |
c |       250 |  109895   370959 |   44956      76      271     3.6 | 18.103 % |
c |       475 |  109153   368435 |   49451     228      826     3.6 | 18.740 % |
c |       812 |  108712   366951 |   54397     506     2195     4.3 | 19.098 % |
c |      1318 |  108203   365219 |   59836     939     4427     4.7 | 19.520 % |
c |      2077 |  107388   362505 |   65820    1591     7475     4.7 | 20.211 % |
c |      3216 |  106353   359084 |   72402    2545    12378     4.9 | 21.093 % |
c |      4927 |  105147   355067 |   79642    3985    19800     5.0 | 22.088 % |
c |      7490 |  104870   354158 |   87607    6434    45255     7.0 | 22.324 % |
c |     11336 |  104781   353868 |   96367   10254   164670    16.1 | 22.392 % |
c |     17102 |  104702   353603 |  106004   15999   591369    37.0 | 22.451 % |
c |     25751 |  104597   353260 |  116605   24630  1353382    54.9 | 22.534 % |
c |     38727 |  104366   352489 |  128265   37520  2772480    73.9 | 22.716 % |
c |     58189 |  104182   351880 |  141092   56934  5445601    95.6 | 22.868 % |
c |     87383 |  103680   350211 |  155201   84676  8829598   104.3 | 23.294 % |
c |    131172 |  103440   349422 |  170721  128401 14490557   112.9 | 23.495 % |
c |    196858 |  103409   349317 |  187793   35837  4157474   116.0 | 23.520 % |
#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.85 0.97 0.91 2/54 29859
Raw data (stat): 29859 (runsolver) R 29858 26298 26297 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 479838496 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0007 s]
Raw data (loadavg): 0.87 0.97 0.91 2/54 29859
Raw data (stat): 29859 (minisat+) R 29858 26298 26297 0 -1 0 2721 0 0 0 992 7 0 0 25 0 1 0 479838496 13172736 2694 4294967295 134512640 134672761 3221224560 3221223764 134561964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3216 2694 603 41 0 3175 0
vsize: 12864
[startup+20.0017 s]
Raw data (loadavg): 0.89 0.97 0.91 2/54 29859
Raw data (stat): 29859 (minisat+) R 29858 26298 26297 0 -1 0 2740 0 0 0 1992 7 0 0 25 0 1 0 479838496 13172736 2713 4294967295 134512640 134672761 3221224560 3221223732 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3216 2713 603 41 0 3175 0
vsize: 12864
[startup+30.0011 s]
Raw data (loadavg): 0.91 0.97 0.91 2/54 29859
Raw data (stat): 29859 (minisat+) R 29858 26298 26297 0 -1 0 2756 0 0 0 2992 7 0 0 25 0 1 0 479838496 13307904 2729 4294967295 134512640 134672761 3221224560 3221223732 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3249 2729 603 41 0 3208 0
vsize: 12996
[startup+40.0008 s]
Raw data (loadavg): 0.92 0.97 0.91 2/54 29859
Raw data (stat): 29859 (minisat+) R 29858 26298 26297 0 -1 0 3595 0 0 0 3989 10 0 0 25 0 1 0 479838496 16715776 3568 4294967295 134512640 134672761 3221224560 3221223728 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4081 3568 603 41 0 4040 0
vsize: 16324
[startup+50.002 s]
Raw data (loadavg): 0.93 0.97 0.91 2/54 29859
Raw data (stat): 29859 (minisat+) R 29858 26298 26297 0 -1 0 4601 0 0 0 4986 13 0 0 25 0 1 0 479838496 20877312 4574 4294967295 134512640 134672761 3221224560 3221223664 134560264 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5097 4574 603 41 0 5056 0
vsize: 20388
[startup+60.0022 s]
Raw data (loadavg): 0.94 0.97 0.91 2/54 29859
Raw data (stat): 29859 (minisat+) R 29858 26298 26297 0 -1 0 5296 0 0 0 5984 16 0 0 25 0 1 0 479838496 23822336 5269 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5816 5269 603 41 0 5775 0
vsize: 23264
[startup+70.003 s]
Raw data (loadavg): 0.95 0.97 0.91 2/54 29859
Raw data (stat): 29859 (minisat+) R 29858 26298 26297 0 -1 0 6126 0 0 0 6981 18 0 0 25 0 1 0 479838496 27160576 6099 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6631 6099 603 41 0 6590 0
vsize: 26524
[startup+80.0031 s]
Raw data (loadavg): 0.96 0.97 0.91 2/54 29859
Raw data (stat): 29859 (minisat+) R 29858 26298 26297 0 -1 0 6754 0 0 0 7979 20 0 0 25 0 1 0 479838496 29712384 6727 4294967295 134512640 134672761 3221224560 3221223728 134560876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7254 6727 603 41 0 7213 0
vsize: 29016
[startup+90.0034 s]
Raw data (loadavg): 0.96 0.97 0.91 2/54 29859
Raw data (stat): 29859 (minisat+) R 29858 26298 26297 0 -1 0 7388 0 0 0 8978 22 0 0 25 0 1 0 479838496 32378880 7361 4294967295 134512640 134672761 3221224560 3221223728 134560917 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7905 7361 603 41 0 7864 0
vsize: 31620
[startup+100.003 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 29859
Raw data (stat): 29859 (minisat+) R 29858 26298 26297 0 -1 0 8116 0 0 0 9975 25 0 0 25 0 1 0 479838496 35307520 8089 4294967295 134512640 134672761 3221224560 3221223728 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8620 8089 603 41 0 8579 0
vsize: 34480
[startup+110.004 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 29859
Raw data (stat): 29859 (minisat+) R 29858 26298 26297 0 -1 0 8751 0 0 0 10974 26 0 0 25 0 1 0 479838496 37986304 8724 4294967295 134512640 134672761 3221224560 3221223728 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9274 8724 603 41 0 9233 0
vsize: 37096
[startup+120.004 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 29859
Raw data (stat): 29859 (minisat+) R 29858 26298 26297 0 -1 0 9234 0 0 0 11972 28 0 0 25 0 1 0 479838496 39866368 9207 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9733 9207 603 41 0 9692 0
vsize: 38932
[startup+130.004 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 29859
Raw data (stat): 29859 (minisat+) R 29858 26298 26297 0 -1 0 9704 0 0 0 12971 30 0 0 25 0 1 0 479838496 41885696 9677 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10226 9677 603 41 0 10185 0
vsize: 40904
[startup+140.004 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 29859
Raw data (stat): 29859 (minisat+) R 29858 26298 26297 0 -1 0 10035 0 0 0 13970 31 0 0 25 0 1 0 479838496 43237376 10008 4294967295 134512640 134672761 3221224560 3221223732 134556667 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10556 10008 603 41 0 10515 0
vsize: 42224
[startup+150.005 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 29859
Raw data (stat): 29859 (minisat+) R 29858 26298 26297 0 -1 0 10430 0 0 0 14969 32 0 0 25 0 1 0 479838496 45109248 10403 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11013 10403 603 41 0 10972 0
vsize: 44052
[startup+160.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29859
Raw data (stat): 29859 (minisat+) R 29858 26298 26297 0 -1 0 10670 0 0 0 15968 33 0 0 25 0 1 0 479838496 46043136 10643 4294967295 134512640 134672761 3221224560 3221223728 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11241 10643 603 41 0 11200 0
vsize: 44964
[startup+170.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29859
Raw data (stat): 29859 (minisat+) R 29858 26298 26297 0 -1 0 11011 0 0 0 16967 34 0 0 25 0 1 0 479838496 47403008 10984 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11573 10984 603 41 0 11532 0
vsize: 46292
[startup+180.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29859
Raw data (stat): 29859 (minisat+) R 29858 26298 26297 0 -1 0 11260 0 0 0 17966 35 0 0 25 0 1 0 479838496 48476160 11233 4294967295 134512640 134672761 3221224560 3221223728 134561207 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11835 11233 603 41 0 11794 0
vsize: 47340
[startup+190.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29859
Raw data (stat): 29859 (minisat+) R 29858 26298 26297 0 -1 0 11643 0 0 0 18965 37 0 0 25 0 1 0 479838496 49942528 11616 4294967295 134512640 134672761 3221224560 3221223728 134560895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12193 11616 603 41 0 12152 0
vsize: 48772
[startup+200.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29859
Raw data (stat): 29859 (minisat+) R 29858 26298 26297 0 -1 0 12027 0 0 0 19963 38 0 0 25 0 1 0 479838496 51548160 12000 4294967295 134512640 134672761 3221224560 3221223728 134560895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12585 12000 603 41 0 12544 0
vsize: 50340
[startup+210.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29859
Raw data (stat): 29859 (minisat+) R 29858 26298 26297 0 -1 0 12545 0 0 0 20962 40 0 0 25 0 1 0 479838496 53694464 12518 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13109 12518 603 41 0 13068 0
vsize: 52436
[startup+220.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29859
Raw data (stat): 29859 (minisat+) R 29858 26298 26297 0 -1 0 12864 0 0 0 21961 41 0 0 25 0 1 0 479838496 55046144 12837 4294967295 134512640 134672761 3221224560 3221223732 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13439 12837 603 41 0 13398 0
vsize: 53756
[startup+230.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29859
Raw data (stat): 29859 (minisat+) R 29858 26298 26297 0 -1 0 13074 0 0 0 22960 42 0 0 25 0 1 0 479838496 55857152 13047 4294967295 134512640 134672761 3221224560 3221223728 134561207 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13637 13047 603 41 0 13596 0
vsize: 54548
[startup+240.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29859
Raw data (stat): 29859 (minisat+) R 29858 26298 26297 0 -1 0 13503 0 0 0 23958 44 0 0 25 0 1 0 479838496 57610240 13476 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14065 13476 603 41 0 14024 0
vsize: 56260
[startup+250.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29859
Raw data (stat): 29859 (minisat+) R 29858 26298 26297 0 -1 0 13862 0 0 0 24957 45 0 0 25 0 1 0 479838496 59088896 13835 4294967295 134512640 134672761 3221224560 3221223732 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14426 13835 603 41 0 14385 0
vsize: 57704
[startup+260.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29859
Raw data (stat): 29859 (minisat+) R 29858 26298 26297 0 -1 0 14257 0 0 0 25956 46 0 0 25 0 1 0 479838496 60694528 14230 4294967295 134512640 134672761 3221224560 3221223728 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14818 14230 603 41 0 14777 0
vsize: 59272
[startup+270.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29859
Raw data (stat): 29859 (minisat+) R 29858 26298 26297 0 -1 0 14634 0 0 0 26954 48 0 0 25 0 1 0 479838496 62300160 14607 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15210 14607 603 41 0 15169 0
vsize: 60840
[startup+280.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29859
Raw data (stat): 29859 (minisat+) R 29858 26298 26297 0 -1 0 14996 0 0 0 27953 50 0 0 25 0 1 0 479838496 63758336 14969 4294967295 134512640 134672761 3221224560 3221223728 134561154 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15566 14969 603 41 0 15525 0
vsize: 62264
[startup+290.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29859
Raw data (stat): 29859 (minisat+) R 29858 26298 26297 0 -1 0 15257 0 0 0 28951 51 0 0 25 0 1 0 479838496 64835584 15230 4294967295 134512640 134672761 3221224560 3221223732 134556680 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15829 15230 603 41 0 15788 0
vsize: 63316
[startup+300.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29859
Raw data (stat): 29859 (minisat+) R 29858 26298 26297 0 -1 0 15615 0 0 0 29950 53 0 0 25 0 1 0 479838496 66301952 15588 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16187 15588 603 41 0 16146 0
vsize: 64748
[startup+310.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29859
Raw data (stat): 29859 (minisat+) R 29858 26298 26297 0 -1 0 15932 0 0 0 30949 54 0 0 25 0 1 0 479838496 67514368 15905 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16483 15905 603 41 0 16442 0
vsize: 65932
[startup+320.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29859
Raw data (stat): 29859 (minisat+) R 29858 26298 26297 0 -1 0 16353 0 0 0 31949 55 0 0 25 0 1 0 479838496 69279744 16326 4294967295 134512640 134672761 3221224560 3221223744 134559498 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16914 16326 603 41 0 16873 0
vsize: 67656
[startup+330.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29859
Raw data (stat): 29859 (minisat+) R 29858 26298 26297 0 -1 0 16736 0 0 0 32947 56 0 0 25 0 1 0 479838496 70889472 16709 4294967295 134512640 134672761 3221224560 3221223728 134560858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17307 16709 603 41 0 17266 0
vsize: 69228
[startup+340.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29859
Raw data (stat): 29859 (minisat+) R 29858 26298 26297 0 -1 0 17099 0 0 0 33947 57 0 0 25 0 1 0 479838496 72364032 17072 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17667 17072 603 41 0 17626 0
vsize: 70668
[startup+350.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29859
Raw data (stat): 29859 (minisat+) R 29858 26298 26297 0 -1 0 17446 0 0 0 34946 58 0 0 25 0 1 0 479838496 73707520 17419 4294967295 134512640 134672761 3221224560 3221223728 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17995 17419 603 41 0 17954 0
vsize: 71980
[startup+360.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29859
Raw data (stat): 29859 (minisat+) R 29858 26298 26297 0 -1 0 17794 0 0 0 35945 59 0 0 25 0 1 0 479838496 75186176 17767 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18356 17767 603 41 0 18315 0
vsize: 73424
[startup+370.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29859
Raw data (stat): 29859 (minisat+) R 29858 26298 26297 0 -1 0 18099 0 0 0 36944 60 0 0 25 0 1 0 479838496 76423168 18072 4294967295 134512640 134672761 3221224560 3221223728 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18658 18072 603 41 0 18617 0
vsize: 74632
[startup+380.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29859
Raw data (stat): 29859 (minisat+) R 29858 26298 26297 0 -1 0 18409 0 0 0 37943 61 0 0 25 0 1 0 479838496 77635584 18382 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18954 18382 603 41 0 18913 0
vsize: 75816
[startup+390.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29859
Raw data (stat): 29859 (minisat+) R 29858 26298 26297 0 -1 0 18740 0 0 0 38942 62 0 0 25 0 1 0 479838496 78979072 18713 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19282 18713 603 41 0 19241 0
vsize: 77128
[startup+400.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29859
Raw data (stat): 29859 (minisat+) R 29858 26298 26297 0 -1 0 18959 0 0 0 39942 63 0 0 25 0 1 0 479838496 79937536 18932 4294967295 134512640 134672761 3221224560 3221223732 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19516 18932 603 41 0 19475 0
vsize: 78064
[startup+410.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29859
Raw data (stat): 29859 (minisat+) R 29858 26298 26297 0 -1 0 19100 0 0 0 40941 64 0 0 25 0 1 0 479838496 80625664 19073 4294967295 134512640 134672761 3221224560 3221223732 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19684 19073 603 41 0 19643 0
vsize: 78736
[startup+420.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29859
Raw data (stat): 29859 (minisat+) R 29858 26298 26297 0 -1 0 19308 0 0 0 41941 64 0 0 25 0 1 0 479838496 81977344 19281 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20014 19281 603 41 0 19973 0
vsize: 80056
[startup+430.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29859
Raw data (stat): 29859 (minisat+) R 29858 26298 26297 0 -1 0 19543 0 0 0 42940 65 0 0 25 0 1 0 479838496 82919424 19516 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20244 19516 603 41 0 20203 0
vsize: 80976
[startup+440.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29859
Raw data (stat): 29859 (minisat+) R 29858 26298 26297 0 -1 0 19794 0 0 0 43939 66 0 0 25 0 1 0 479838496 83996672 19767 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20507 19767 603 41 0 20466 0
vsize: 82028
[startup+450.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29859
Raw data (stat): 29859 (minisat+) R 29858 26298 26297 0 -1 0 20067 0 0 0 44938 67 0 0 25 0 1 0 479838496 85090304 20040 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20774 20040 603 41 0 20733 0
vsize: 83096
[startup+460.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29859
Raw data (stat): 29859 (minisat+) R 29858 26298 26297 0 -1 0 20308 0 0 0 45938 68 0 0 25 0 1 0 479838496 86036480 20281 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21005 20281 603 41 0 20964 0
vsize: 84020
[startup+470.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29859
Raw data (stat): 29859 (minisat+) R 29858 26298 26297 0 -1 0 20555 0 0 0 46937 69 0 0 25 0 1 0 479838496 87126016 20528 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21271 20528 603 41 0 21230 0
vsize: 85084
[startup+480.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29859
Raw data (stat): 29859 (minisat+) R 29858 26298 26297 0 -1 0 20832 0 0 0 47936 70 0 0 25 0 1 0 479838496 88223744 20805 4294967295 134512640 134672761 3221224560 3221223728 134561154 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21539 20805 603 41 0 21498 0
vsize: 86156
[startup+490.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29859
Raw data (stat): 29859 (minisat+) R 29858 26298 26297 0 -1 0 21083 0 0 0 48936 71 0 0 25 0 1 0 479838496 89235456 21056 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21786 21056 603 41 0 21745 0
vsize: 87144
[startup+500.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29859
Raw data (stat): 29859 (minisat+) R 29858 26298 26297 0 -1 0 21319 0 0 0 49935 72 0 0 25 0 1 0 479838496 90181632 21292 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22017 21292 603 41 0 21976 0
vsize: 88068
[startup+510.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29859
Raw data (stat): 29859 (minisat+) R 29858 26298 26297 0 -1 0 21603 0 0 0 50934 72 0 0 25 0 1 0 479838496 91389952 21576 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22312 21576 603 41 0 22271 0
vsize: 89248
[startup+520.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29859
Raw data (stat): 29859 (minisat+) R 29858 26298 26297 0 -1 0 21869 0 0 0 51933 74 0 0 25 0 1 0 479838496 92512256 21842 4294967295 134512640 134672761 3221224560 3221223728 134560874 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22586 21842 603 41 0 22545 0
vsize: 90344
[startup+530.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29859
Raw data (stat): 29859 (minisat+) R 29858 26298 26297 0 -1 0 22135 0 0 0 52933 74 0 0 25 0 1 0 479838496 93622272 22108 4294967295 134512640 134672761 3221224560 3221223728 134561207 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22857 22108 603 41 0 22816 0
vsize: 91428
[startup+540.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29859
Raw data (stat): 29859 (minisat+) R 29858 26298 26297 0 -1 0 22337 0 0 0 53933 75 0 0 25 0 1 0 479838496 94433280 22310 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23055 22310 603 41 0 23014 0
vsize: 92220
[startup+550.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29859
Raw data (stat): 29859 (minisat+) R 29858 26298 26297 0 -1 0 22573 0 0 0 54932 76 0 0 25 0 1 0 479838496 95379456 22546 4294967295 134512640 134672761 3221224560 3221223744 134559340 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23286 22546 603 41 0 23245 0
vsize: 93144
[startup+560.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29859
Raw data (stat): 29859 (minisat+) R 29858 26298 26297 0 -1 0 22791 0 0 0 55931 77 0 0 25 0 1 0 479838496 96190464 22764 4294967295 134512640 134672761 3221224560 3221223748 1075346941 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23484 22764 603 41 0 23443 0
vsize: 93936
[startup+570.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29859
Raw data (stat): 29859 (minisat+) R 29858 26298 26297 0 -1 0 23019 0 0 0 56931 77 0 0 25 0 1 0 479838496 97128448 22992 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23713 22992 603 41 0 23672 0
vsize: 94852
[startup+580.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29859
Raw data (stat): 29859 (minisat+) R 29858 26298 26297 0 -1 0 23264 0 0 0 57930 78 0 0 25 0 1 0 479838496 98181120 23237 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23970 23237 603 41 0 23929 0
vsize: 95880
[startup+590.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29859
Raw data (stat): 29859 (minisat+) R 29858 26298 26297 0 -1 0 23520 0 0 0 58929 79 0 0 25 0 1 0 479838496 99262464 23493 4294967295 134512640 134672761 3221224560 3221223760 134557800 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24234 23493 603 41 0 24193 0
vsize: 96936
[startup+600.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29859
Raw data (stat): 29859 (minisat+) R 29858 26298 26297 0 -1 0 23769 0 0 0 59929 80 0 0 25 0 1 0 479838496 100208640 23742 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24465 23742 603 41 0 24424 0
vsize: 97860
[startup+610.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29859
Raw data (stat): 29859 (minisat+) R 29858 26298 26297 0 -1 0 24017 0 0 0 60929 80 0 0 25 0 1 0 479838496 101302272 23990 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24732 23990 603 41 0 24691 0
vsize: 98928
[startup+620.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29859
Raw data (stat): 29859 (minisat+) R 29858 26298 26297 0 -1 0 24247 0 0 0 61928 81 0 0 25 0 1 0 479838496 102248448 24220 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24963 24220 603 41 0 24922 0
vsize: 99852
[startup+630.015 s]
Raw data (loadavg): 0.99 0.97 0.91 3/54 29859
Raw data (stat): 29859 (minisat+) R 29858 26298 26297 0 -1 0 24467 0 0 0 62928 82 0 0 25 0 1 0 479838496 103092224 24440 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25169 24440 603 41 0 25128 0
vsize: 100676
[startup+640.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29859
Raw data (stat): 29859 (minisat+) R 29858 26298 26297 0 -1 0 24658 0 0 0 63927 83 0 0 25 0 1 0 479838496 103903232 24631 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25367 24631 603 41 0 25326 0
vsize: 101468
[startup+650.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29859
Raw data (stat): 29859 (minisat+) R 29858 26298 26297 0 -1 0 24869 0 0 0 64927 83 0 0 25 0 1 0 479838496 104714240 24842 4294967295 134512640 134672761 3221224560 3221223728 134560988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25565 24842 603 41 0 25524 0
vsize: 102260
[startup+660.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29859
Raw data (stat): 29859 (minisat+) R 29858 26298 26297 0 -1 0 25026 0 0 0 65926 84 0 0 25 0 1 0 479838496 105385984 24999 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25729 24999 603 41 0 25688 0
vsize: 102916
[startup+670.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29859
Raw data (stat): 29859 (minisat+) R 29858 26298 26297 0 -1 0 25236 0 0 0 66926 84 0 0 25 0 1 0 479838496 106430464 25209 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25984 25209 603 41 0 25943 0
vsize: 103936
[startup+680.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29859
Raw data (stat): 29859 (minisat+) R 29858 26298 26297 0 -1 0 25409 0 0 0 67925 85 0 0 25 0 1 0 479838496 107102208 25382 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26148 25382 603 41 0 26107 0
vsize: 104592
[startup+690.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29859
Raw data (stat): 29859 (minisat+) R 29858 26298 26297 0 -1 0 25545 0 0 0 68925 86 0 0 25 0 1 0 479838496 107667456 25518 4294967295 134512640 134672761 3221224560 3221223664 134554656 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26286 25518 603 41 0 26245 0
vsize: 105144
[startup+700.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29859
Raw data (stat): 29859 (minisat+) R 29858 26298 26297 0 -1 0 25545 0 0 0 69925 86 0 0 25 0 1 0 479838496 107667456 25518 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26286 25518 603 41 0 26245 0
vsize: 105144
[startup+710.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29859
Raw data (stat): 29859 (minisat+) R 29858 26298 26297 0 -1 0 25545 0 0 0 70925 86 0 0 25 0 1 0 479838496 107667456 25518 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26286 25518 603 41 0 26245 0
vsize: 105144
[startup+720.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29859
Raw data (stat): 29859 (minisat+) R 29858 26298 26297 0 -1 0 25547 0 0 0 71925 86 0 0 25 0 1 0 479838496 107667456 25520 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26286 25520 603 41 0 26245 0
vsize: 105144
[startup+730.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29859
Raw data (stat): 29859 (minisat+) R 29858 26298 26297 0 -1 0 25549 0 0 0 72925 86 0 0 25 0 1 0 479838496 107667456 25522 4294967295 134512640 134672761 3221224560 3221223664 134559851 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26286 25522 603 41 0 26245 0
vsize: 105144
[startup+740.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29859
Raw data (stat): 29859 (minisat+) R 29858 26298 26297 0 -1 0 25550 0 0 0 73925 86 0 0 25 0 1 0 479838496 107667456 25523 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26286 25523 603 41 0 26245 0
vsize: 105144
[startup+750.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29859
Raw data (stat): 29859 (minisat+) R 29858 26298 26297 0 -1 0 25553 0 0 0 74925 86 0 0 25 0 1 0 479838496 107667456 25526 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26286 25526 603 41 0 26245 0
vsize: 105144
[startup+760.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29859
Raw data (stat): 29859 (minisat+) R 29858 26298 26297 0 -1 0 25553 0 0 0 75925 86 0 0 25 0 1 0 479838496 107667456 25526 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26286 25526 603 41 0 26245 0
vsize: 105144
[startup+770.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29859
Raw data (stat): 29859 (minisat+) R 29858 26298 26297 0 -1 0 25553 0 0 0 76925 86 0 0 25 0 1 0 479838496 107667456 25526 4294967295 134512640 134672761 3221224560 3221223728 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26286 25526 603 41 0 26245 0
vsize: 105144
[startup+780.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29859
Raw data (stat): 29859 (minisat+) R 29858 26298 26297 0 -1 0 25553 0 0 0 77925 86 0 0 25 0 1 0 479838496 107667456 25526 4294967295 134512640 134672761 3221224560 3221223728 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26286 25526 603 41 0 26245 0
vsize: 105144
[startup+790.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29859
Raw data (stat): 29859 (minisat+) R 29858 26298 26297 0 -1 0 25553 0 0 0 78925 86 0 0 25 0 1 0 479838496 107667456 25526 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26286 25526 603 41 0 26245 0
vsize: 105144
[startup+800.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29859
Raw data (stat): 29859 (minisat+) R 29858 26298 26297 0 -1 0 25554 0 0 0 79925 87 0 0 25 0 1 0 479838496 107667456 25527 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26286 25527 603 41 0 26245 0
vsize: 105144
[startup+810.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29859
Raw data (stat): 29859 (minisat+) R 29858 26298 26297 0 -1 0 25554 0 0 0 80925 87 0 0 25 0 1 0 479838496 107667456 25527 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26286 25527 603 41 0 26245 0
vsize: 105144
[startup+820.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29859
Raw data (stat): 29859 (minisat+) R 29858 26298 26297 0 -1 0 25554 0 0 0 81925 87 0 0 25 0 1 0 479838496 107667456 25527 4294967295 134512640 134672761 3221224560 3221223732 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26286 25527 603 41 0 26245 0
vsize: 105144
[startup+830.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29859
Raw data (stat): 29859 (minisat+) R 29858 26298 26297 0 -1 0 25554 0 0 0 82925 87 0 0 25 0 1 0 479838496 107667456 25527 4294967295 134512640 134672761 3221224560 3221223732 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26286 25527 603 41 0 26245 0
vsize: 105144
[startup+840.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29859
Raw data (stat): 29859 (minisat+) R 29858 26298 26297 0 -1 0 25554 0 0 0 83925 87 0 0 25 0 1 0 479838496 107667456 25527 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26286 25527 603 41 0 26245 0
vsize: 105144
[startup+850.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29859
Raw data (stat): 29859 (minisat+) R 29858 26298 26297 0 -1 0 25556 0 0 0 84925 87 0 0 25 0 1 0 479838496 107667456 25529 4294967295 134512640 134672761 3221224560 3221223728 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26286 25529 603 41 0 26245 0
vsize: 105144
[startup+860.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29859
Raw data (stat): 29859 (minisat+) R 29858 26298 26297 0 -1 0 25556 0 0 0 85925 87 0 0 25 0 1 0 479838496 107667456 25529 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26286 25529 603 41 0 26245 0
vsize: 105144
[startup+870.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29859
Raw data (stat): 29859 (minisat+) R 29858 26298 26297 0 -1 0 25556 0 0 0 86925 87 0 0 25 0 1 0 479838496 107667456 25529 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26286 25529 603 41 0 26245 0
vsize: 105144
[startup+880.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29859
Raw data (stat): 29859 (minisat+) R 29858 26298 26297 0 -1 0 25556 0 0 0 87926 87 0 0 25 0 1 0 479838496 107667456 25529 4294967295 134512640 134672761 3221224560 3221223732 134556639 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26286 25529 603 41 0 26245 0
vsize: 105144
[startup+890.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29859
Raw data (stat): 29859 (minisat+) R 29858 26298 26297 0 -1 0 25556 0 0 0 88926 87 0 0 25 0 1 0 479838496 107667456 25529 4294967295 134512640 134672761 3221224560 3221223684 134566043 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26286 25529 603 41 0 26245 0
vsize: 105144
[startup+900.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29859
Raw data (stat): 29859 (minisat+) R 29858 26298 26297 0 -1 0 25556 0 0 0 89926 87 0 0 25 0 1 0 479838496 107667456 25529 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26286 25529 603 41 0 26245 0
vsize: 105144
[startup+910.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29859
Raw data (stat): 29859 (minisat+) R 29858 26298 26297 0 -1 0 25556 0 0 0 90926 87 0 0 25 0 1 0 479838496 107667456 25529 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26286 25529 603 41 0 26245 0
vsize: 105144
[startup+920.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29859
Raw data (stat): 29859 (minisat+) R 29858 26298 26297 0 -1 0 25556 0 0 0 91926 87 0 0 25 0 1 0 479838496 107667456 25529 4294967295 134512640 134672761 3221224560 3221223728 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26286 25529 603 41 0 26245 0
vsize: 105144
[startup+930.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29859
Raw data (stat): 29859 (minisat+) R 29858 26298 26297 0 -1 0 25556 0 0 0 92926 87 0 0 25 0 1 0 479838496 107667456 25529 4294967295 134512640 134672761 3221224560 3221223732 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26286 25529 603 41 0 26245 0
vsize: 105144
[startup+940.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29859
Raw data (stat): 29859 (minisat+) R 29858 26298 26297 0 -1 0 25556 0 0 0 93926 87 0 0 25 0 1 0 479838496 107667456 25529 4294967295 134512640 134672761 3221224560 3221223728 134560876 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26286 25529 603 41 0 26245 0
vsize: 105144
[startup+950.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29859
Raw data (stat): 29859 (minisat+) R 29858 26298 26297 0 -1 0 25556 0 0 0 94927 87 0 0 25 0 1 0 479838496 107667456 25529 4294967295 134512640 134672761 3221224560 3221223732 134556667 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26286 25529 603 41 0 26245 0
vsize: 105144
[startup+960.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29859
Raw data (stat): 29859 (minisat+) R 29858 26298 26297 0 -1 0 25556 0 0 0 95927 87 0 0 25 0 1 0 479838496 107667456 25529 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26286 25529 603 41 0 26245 0
vsize: 105144
[startup+970.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29859
Raw data (stat): 29859 (minisat+) R 29858 26298 26297 0 -1 0 25556 0 0 0 96927 87 0 0 25 0 1 0 479838496 107667456 25529 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26286 25529 603 41 0 26245 0
vsize: 105144
[startup+980.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29859
Raw data (stat): 29859 (minisat+) R 29858 26298 26297 0 -1 0 25556 0 0 0 97927 87 0 0 25 0 1 0 479838496 107667456 25529 4294967295 134512640 134672761 3221224560 3221223728 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26286 25529 603 41 0 26245 0
vsize: 105144
[startup+990.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29859
Raw data (stat): 29859 (minisat+) R 29858 26298 26297 0 -1 0 25556 0 0 0 98927 87 0 0 25 0 1 0 479838496 107667456 25529 4294967295 134512640 134672761 3221224560 3221223732 134556667 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26286 25529 603 41 0 26245 0
vsize: 105144
[startup+1000.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29859
Raw data (stat): 29859 (minisat+) R 29858 26298 26297 0 -1 0 25558 0 0 0 99928 87 0 0 25 0 1 0 479838496 107667456 25531 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26286 25531 603 41 0 26245 0
vsize: 105144
[startup+1010.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29859
Raw data (stat): 29859 (minisat+) R 29858 26298 26297 0 -1 0 25560 0 0 0 100928 88 0 0 25 0 1 0 479838496 107667456 25533 4294967295 134512640 134672761 3221224560 3221223728 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26286 25533 603 41 0 26245 0
vsize: 105144
[startup+1020.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29859
Raw data (stat): 29859 (minisat+) R 29858 26298 26297 0 -1 0 25561 0 0 0 101928 88 0 0 25 0 1 0 479838496 107667456 25534 4294967295 134512640 134672761 3221224560 3221223664 134560054 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26286 25534 603 41 0 26245 0
vsize: 105144
[startup+1030.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29859
Raw data (stat): 29859 (minisat+) R 29858 26298 26297 0 -1 0 25561 0 0 0 102928 88 0 0 25 0 1 0 479838496 107667456 25534 4294967295 134512640 134672761 3221224560 3221223744 134559538 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26286 25534 603 41 0 26245 0
vsize: 105144
[startup+1040.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29859
Raw data (stat): 29859 (minisat+) R 29858 26298 26297 0 -1 0 25561 0 0 0 103928 88 0 0 25 0 1 0 479838496 107667456 25534 4294967295 134512640 134672761 3221224560 3221223732 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26286 25534 603 41 0 26245 0
vsize: 105144
[startup+1050.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29859
Raw data (stat): 29859 (minisat+) R 29858 26298 26297 0 -1 0 25561 0 0 0 104928 88 0 0 25 0 1 0 479838496 107667456 25534 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26286 25534 603 41 0 26245 0
vsize: 105144
[startup+1060.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29859
Raw data (stat): 29859 (minisat+) R 29858 26298 26297 0 -1 0 25561 0 0 0 105928 88 0 0 25 0 1 0 479838496 107667456 25534 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26286 25534 603 41 0 26245 0
vsize: 105144
[startup+1070.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29859
Raw data (stat): 29859 (minisat+) R 29858 26298 26297 0 -1 0 25561 0 0 0 106929 88 0 0 25 0 1 0 479838496 107667456 25534 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26286 25534 603 41 0 26245 0
vsize: 105144
[startup+1080.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29859
Raw data (stat): 29859 (minisat+) R 29858 26298 26297 0 -1 0 25561 0 0 0 107929 88 0 0 25 0 1 0 479838496 107667456 25534 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26286 25534 603 41 0 26245 0
vsize: 105144
[startup+1090.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29859
Raw data (stat): 29859 (minisat+) R 29858 26298 26297 0 -1 0 25561 0 0 0 108929 88 0 0 25 0 1 0 479838496 107667456 25534 4294967295 134512640 134672761 3221224560 3221223728 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26286 25534 603 41 0 26245 0
vsize: 105144
[startup+1100.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29859
Raw data (stat): 29859 (minisat+) R 29858 26298 26297 0 -1 0 25562 0 0 0 109929 88 0 0 25 0 1 0 479838496 107667456 25535 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26286 25535 603 41 0 26245 0
vsize: 105144
[startup+1110.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29859
Raw data (stat): 29859 (minisat+) R 29858 26298 26297 0 -1 0 25562 0 0 0 110930 88 0 0 25 0 1 0 479838496 107667456 25535 4294967295 134512640 134672761 3221224560 3221223728 134560852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26286 25535 603 41 0 26245 0
vsize: 105144
[startup+1120.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29859
Raw data (stat): 29859 (minisat+) R 29858 26298 26297 0 -1 0 25562 0 0 0 111930 88 0 0 25 0 1 0 479838496 107667456 25535 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26286 25535 603 41 0 26245 0
vsize: 105144
[startup+1130.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29859
Raw data (stat): 29859 (minisat+) R 29858 26298 26297 0 -1 0 25566 0 0 0 112930 88 0 0 25 0 1 0 479838496 107667456 25539 4294967295 134512640 134672761 3221224560 3221223728 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26286 25539 603 41 0 26245 0
vsize: 105144
[startup+1140.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29859
Raw data (stat): 29859 (minisat+) R 29858 26298 26297 0 -1 0 25566 0 0 0 113930 88 0 0 25 0 1 0 479838496 107667456 25539 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26286 25539 603 41 0 26245 0
vsize: 105144
[startup+1150.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29859
Raw data (stat): 29859 (minisat+) R 29858 26298 26297 0 -1 0 25567 0 0 0 114930 88 0 0 25 0 1 0 479838496 107667456 25540 4294967295 134512640 134672761 3221224560 3221223728 134560920 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26286 25540 603 41 0 26245 0
vsize: 105144
[startup+1160.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29859
Raw data (stat): 29859 (minisat+) R 29858 26298 26297 0 -1 0 25569 0 0 0 115930 88 0 0 25 0 1 0 479838496 107667456 25542 4294967295 134512640 134672761 3221224560 3221223728 134560906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26286 25542 603 41 0 26245 0
vsize: 105144
[startup+1170.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29859
Raw data (stat): 29859 (minisat+) R 29858 26298 26297 0 -1 0 25569 0 0 0 116930 88 0 0 25 0 1 0 479838496 107667456 25542 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26286 25542 603 41 0 26245 0
vsize: 105144
[startup+1180.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29859
Raw data (stat): 29859 (minisat+) R 29858 26298 26297 0 -1 0 25569 0 0 0 117930 88 0 0 25 0 1 0 479838496 107667456 25542 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26286 25542 603 41 0 26245 0
vsize: 105144
[startup+1190.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29859
Raw data (stat): 29859 (minisat+) R 29858 26298 26297 0 -1 0 25569 0 0 0 118930 88 0 0 25 0 1 0 479838496 107667456 25542 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26286 25542 603 41 0 26245 0
vsize: 105144
[startup+1200.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29859
Raw data (stat): 29859 (minisat+) R 29858 26298 26297 0 -1 0 25569 0 0 0 119931 88 0 0 25 0 1 0 479838496 107667456 25542 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26286 25542 603 41 0 26245 0
vsize: 105144
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.07 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 29859
Raw data (stat): 29859 (minisat+) Z 29858 26298 26297 0 -1 12 25571 0 0 0 119931 93 0 0 25 0 1 0 479838496 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 0
Real time (s): 1200.07
CPU time (s): 1200.25
CPU user time (s): 1199.31
CPU system time (s): 0.938857
CPU usage (%): 100.015
Max. virtual memory (Kb): 105144
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####