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:3-13,25,26.opb
MD5SUM	85cf0fb6ed84e77eea7ef88259fe2fe8
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	16.5575
Number of variables	4644
Total number of constraints	35898
Number of constraints which are clauses	30228
Number of constraints which are cardinality constraints (but not clauses)	5592
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 5281

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

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        736936 kB
Buffers:         37304 kB
Cached:         219532 kB
SwapCached:          0 kB
Active:          82880 kB
Inactive:       176856 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        736684 kB
SwapTotal:     2097892 kB
SwapFree:      2097892 kB
Dirty:              24 kB
Writeback:           0 kB
Mapped:           6928 kB
Slab:            32208 kB
Committed_AS:    63492 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-13 23:35:22 (client local time) WITH STATUS 0 IN 1200.23 SECONDS
stats: 3745 7 1200.23 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 31428 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ##############################################################################################################################################################################
c   -- Clauses(.)/Splits(s): ....................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ---[31427]---> Adder-cost: 48   maxlim: 61   bits: 7/6
c ---[31426]---> Adder-cost: 48   maxlim: 61   bits: 7/6
c ---[31425]---> Adder-cost: 48   maxlim: 61   bits: 7/6
c ---[31424]---> Adder-cost: 48   maxlim: 61   bits: 7/6
c ---[31423]---> Adder-cost: 48   maxlim: 61   bits: 7/6
c ---[31422]---> Adder-cost: 48   maxlim: 61   bits: 7/6
c ---[31421]---> Adder-cost: 64   maxlim: 86   bits: 7/7
c ---[31420]---> Adder-cost: 64   maxlim: 86   bits: 7/7
c ---[31419]---> Adder-cost: 64   maxlim: 86   bits: 7/7
c ---[31418]---> Adder-cost: 64   maxlim: 86   bits: 7/7
c ---[31417]---> Adder-cost: 64   maxlim: 86   bits: 7/7
c ---[31416]---> Adder-cost: 64   maxlim: 86   bits: 7/7
c ---[31415]---> Adder-cost: 64   maxlim: 85   bits: 7/7
c ---[31414]---> Adder-cost: 64   maxlim: 85   bits: 7/7
c ---[31413]---> Adder-cost: 64   maxlim: 85   bits: 7/7
c ---[31412]---> Adder-cost: 64   maxlim: 85   bits: 7/7
c ---[31411]---> Adder-cost: 64   maxlim: 85   bits: 7/7
c ---[31410]---> Adder-cost: 64   maxlim: 85   bits: 7/7
c ---[31409]---> Adder-cost: 64   maxlim: 85   bits: 7/7
c ---[31408]---> Adder-cost: 64   maxlim: 85   bits: 7/7
c ---[31407]---> Adder-cost: 64   maxlim: 85   bits: 7/7
c ---[31406]---> Adder-cost: 64   maxlim: 85   bits: 7/7
c ---[31405]---> Adder-cost: 64   maxlim: 85   bits: 7/7
c ---[31404]---> Adder-cost: 64   maxlim: 85   bits: 7/7
c ---[31403]---> Adder-cost: 64   maxlim: 85   bits: 7/7
c ---[31402]---> Adder-cost: 64   maxlim: 85   bits: 7/7
c ---[31401]---> Adder-cost: 64   maxlim: 85   bits: 7/7
c ---[31400]---> Adder-cost: 64   maxlim: 85   bits: 7/7
c ---[31399]---> Adder-cost: 64   maxlim: 85   bits: 7/7
c ---[31398]---> Adder-cost: 64   maxlim: 85   bits: 7/7
c ---[31397]---> Adder-cost: 64   maxlim: 84   bits: 7/7
c ---[31396]---> Adder-cost: 64   maxlim: 84   bits: 7/7
c ---[31395]---> Adder-cost: 64   maxlim: 84   bits: 7/7
c ---[31394]---> Adder-cost: 64   maxlim: 84   bits: 7/7
c ---[31393]---> Adder-cost: 64   maxlim: 84   bits: 7/7
c ---[31392]---> Adder-cost: 64   maxlim: 84   bits: 7/7
c ---[31391]---> Adder-cost: 64   maxlim: 85   bits: 7/7
c ---[31390]---> Adder-cost: 64   maxlim: 85   bits: 7/7
c ---[31389]---> Adder-cost: 64   maxlim: 85   bits: 7/7
c ---[31388]---> Adder-cost: 64   maxlim: 85   bits: 7/7
c ---[31387]---> Adder-cost: 64   maxlim: 85   bits: 7/7
c ---[31386]---> Adder-cost: 64   maxlim: 85   bits: 7/7
c ---[31385]---> Adder-cost: 64   maxlim: 85   bits: 7/7
c ---[31384]---> Adder-cost: 64   maxlim: 85   bits: 7/7
c ---[31383]---> Adder-cost: 64   maxlim: 85   bits: 7/7
c ---[31382]---> Adder-cost: 64   maxlim: 85   bits: 7/7
c ---[31381]---> Adder-cost: 64   maxlim: 85   bits: 7/7
c ---[31380]---> Adder-cost: 64   maxlim: 85   bits: 7/7
c ---[31379]---> Adder-cost: 64   maxlim: 85   bits: 7/7
c ---[31378]---> Adder-cost: 64   maxlim: 85   bits: 7/7
c ---[31377]---> Adder-cost: 64   maxlim: 85   bits: 7/7
c ---[31376]---> Adder-cost: 64   maxlim: 85   bits: 7/7
c ---[31375]---> Adder-cost: 64   maxlim: 85   bits: 7/7
c ---[31374]---> Adder-cost: 64   maxlim: 85   bits: 7/7
c ---[31373]---> Adder-cost: 64   maxlim: 83   bits: 7/7
c ---[31372]---> Adder-cost: 64   maxlim: 83   bits: 7/7
c ---[31371]---> Adder-cost: 64   maxlim: 83   bits: 7/7
c ---[31370]---> Adder-cost: 64   maxlim: 83   bits: 7/7
c ---[31369]---> Adder-cost: 64   maxlim: 83   bits: 7/7
c ---[31368]---> Adder-cost: 64   maxlim: 83   bits: 7/7
c ---[31367]---> Adder-cost: 64   maxlim: 83   bits: 7/7
c ---[31366]---> Adder-cost: 64   maxlim: 83   bits: 7/7
c ---[31365]---> Adder-cost: 64   maxlim: 83   bits: 7/7
c ---[31364]---> Adder-cost: 64   maxlim: 83   bits: 7/7
c ---[31363]---> Adder-cost: 64   maxlim: 83   bits: 7/7
c ---[31362]---> Adder-cost: 64   maxlim: 83   bits: 7/7
c ---[31361]---> Adder-cost: 58   maxlim: 75   bits: 7/7
c ---[31360]---> Adder-cost: 58   maxlim: 75   bits: 7/7
c ---[31359]---> Adder-cost: 58   maxlim: 75   bits: 7/7
c ---[31358]---> Adder-cost: 58   maxlim: 75   bits: 7/7
c ---[31357]---> Adder-cost: 58   maxlim: 75   bits: 7/7
c ---[31356]---> Adder-cost: 58   maxlim: 75   bits: 7/7
c ---[31355]---> Adder-cost: 58   maxlim: 75   bits: 7/7
c ---[31354]---> Adder-cost: 58   maxlim: 75   bits: 7/7
c ---[31353]---> Adder-cost: 58   maxlim: 75   bits: 7/7
c ---[31352]---> Adder-cost: 58   maxlim: 75   bits: 7/7
c ---[31351]---> Adder-cost: 58   maxlim: 75   bits: 7/7
c ---[31350]---> Adder-cost: 58   maxlim: 75   bits: 7/7
c ---[31348]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31346]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31344]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31342]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31340]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31338]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31336]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31334]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31332]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31330]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31328]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31326]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31324]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31322]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31320]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31318]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31316]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31314]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31312]---> Adder-cost: 20   maxlim: 11   bits: 4/4
c ---[31310]---> Adder-cost: 20   maxlim: 11   bits: 4/4
c ---[31308]---> Adder-cost: 20   maxlim: 11   bits: 4/4
c ---[31306]---> Adder-cost: 20   maxlim: 11   bits: 4/4
c ---[31304]---> Adder-cost: 20   maxlim: 11   bits: 4/4
c ---[31302]---> Adder-cost: 20   maxlim: 11   bits: 4/4
c ---[31300]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31298]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31296]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31294]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31292]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31290]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31288]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31286]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31284]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31282]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31280]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31278]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31276]---> Adder-cost: 20   maxlim: 11   bits: 4/4
c ---[31274]---> Adder-cost: 20   maxlim: 11   bits: 4/4
c ---[31272]---> Adder-cost: 20   maxlim: 11   bits: 4/4
c ---[31270]---> Adder-cost: 20   maxlim: 11   bits: 4/4
c ---[31268]---> Adder-cost: 20   maxlim: 11   bits: 4/4
c ---[31266]---> Adder-cost: 20   maxlim: 11   bits: 4/4
c ---[31264]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[31262]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[31260]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[31258]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[31256]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[31254]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[31252]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31250]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31248]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31246]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31244]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31242]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31240]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31238]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31236]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31234]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31232]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31230]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31228]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31226]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31224]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31222]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31220]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31218]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31216]---> Adder-cost: 20   maxlim: 11   bits: 4/4
c ---[31214]---> Adder-cost: 20   maxlim: 11   bits: 4/4
c ---[31212]---> Adder-cost: 20   maxlim: 11   bits: 4/4
c ---[31210]---> Adder-cost: 20   maxlim: 11   bits: 4/4
c ---[31208]---> Adder-cost: 20   maxlim: 11   bits: 4/4
c ---[31206]---> Adder-cost: 20   maxlim: 11   bits: 4/4
c ---[31204]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31202]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31200]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31198]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31196]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31194]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31192]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31190]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31188]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31186]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31184]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31182]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31180]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31178]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31176]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31174]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31172]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31170]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31168]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31166]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31164]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31162]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31160]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31158]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31156]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31154]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31152]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31150]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31148]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31146]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31144]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31142]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31140]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31138]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31136]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31134]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31132]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31130]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31128]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31126]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31124]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31122]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31120]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31118]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31116]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31114]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31112]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31110]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31108]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31106]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31104]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31102]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31100]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31098]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31096]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31094]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31092]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31090]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31088]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31086]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31084]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31082]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31080]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31078]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31076]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31074]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31072]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31070]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31068]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31066]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31064]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31062]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31060]---> Adder-cost: 20   maxlim: 12   bits: 4/4
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: 16   maxlim: 9   bits: 4/4
c ---[31046]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[31044]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[31042]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[31040]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[31038]---> Adder-cost: 16   maxlim: 9   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: 20   maxlim: 12   bits: 4/4
c ---[31020]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31018]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31016]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31014]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31012]---> Adder-cost: 20   maxlim: 12   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 ---[31001]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31000]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30999]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30998]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30997]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30996]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30995]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30994]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30993]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30992]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30991]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30990]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30989]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30988]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30987]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30986]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30985]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30984]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30983]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30982]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30981]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30980]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30979]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30978]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30977]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30976]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30975]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30974]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30973]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30972]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30971]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30970]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30969]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30968]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30967]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30966]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30965]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30964]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30963]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30962]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30961]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30960]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30959]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30958]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30957]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30956]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30955]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30954]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30953]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30952]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30951]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30950]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30949]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30948]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30947]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30946]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30945]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30944]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30943]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30942]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30941]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30940]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30939]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30938]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30937]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30936]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30935]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30934]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30933]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30932]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30931]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30930]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30929]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30928]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30927]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30926]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30925]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30924]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30923]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30922]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30921]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30920]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30919]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30918]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30917]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30916]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30915]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30914]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30913]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30912]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30911]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30910]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30909]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30908]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30907]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30906]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30905]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30904]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30903]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30902]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30901]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30900]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30899]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30898]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30897]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30896]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30895]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30894]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30893]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30892]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30891]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30890]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30889]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30888]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30887]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30886]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30885]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30884]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30883]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30882]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30881]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30880]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30879]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30878]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30877]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30876]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30875]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30874]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30873]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30872]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30871]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30870]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30869]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30868]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30867]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30866]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30865]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30864]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30863]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30862]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30861]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30860]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30859]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30858]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30857]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30856]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30855]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30854]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30853]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30852]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30851]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30850]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30849]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30848]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30847]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30846]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30845]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30844]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30843]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30842]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30841]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30840]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30839]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30838]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30837]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30836]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30835]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30834]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30833]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30832]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30831]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30830]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30829]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30828]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30827]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30826]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30825]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30824]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30823]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30822]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30821]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30820]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30819]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30818]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30817]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30816]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30815]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30814]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30813]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30812]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30811]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30810]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30809]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30808]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30807]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30806]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30805]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30804]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30803]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30802]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30801]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30800]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30799]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30798]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30797]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30796]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30795]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30794]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30793]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30792]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30791]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30790]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30789]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30788]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30787]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30786]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30785]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30784]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30783]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30782]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30781]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30780]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30779]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30778]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30777]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30776]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30775]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30774]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30773]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30772]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30771]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30770]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30769]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30768]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30767]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30766]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30765]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30764]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30763]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30762]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30761]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30760]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30759]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30758]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30757]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30756]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30755]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30754]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30753]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30752]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30751]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30750]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30749]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30748]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30747]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30746]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30745]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30744]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30743]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30742]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30741]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30740]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30739]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30738]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30737]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30736]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30735]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30734]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30733]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30732]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30731]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30730]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30729]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30728]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30727]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30726]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30725]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30724]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30723]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30722]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30721]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30720]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30719]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30718]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30717]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30716]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30715]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30714]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30713]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30712]---> Adder-cost: 8   maxlim: 4   bits: 3/3
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 ---[ 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 |  112596   379962 |   37532       0        0     nan |  0.000 % |
c |       100 |  111987   377896 |   41285      30       80     2.7 | 16.983 % |
c |       250 |  111218   375304 |   45413     103      319     3.1 | 17.675 % |
c |       476 |  110483   372795 |   49955     257      889     3.5 | 18.294 % |
c |       814 |  110093   371463 |   54950     556     2026     3.6 | 18.620 % |
c |      1320 |  109673   370043 |   60445    1006     3977     4.0 | 18.966 % |
c |      2079 |  108710   366821 |   66490    1648     6944     4.2 | 19.790 % |
c |      3218 |  107860   363994 |   73139    2663    12211     4.6 | 20.486 % |
c |      4927 |  106580   359751 |   80453    4114    19772     4.8 | 21.582 % |
c |      7491 |  104908   354222 |   88498    6360    31497     5.0 | 23.024 % |
c |     11335 |  102047   344823 |   97348    9622    48282     5.0 | 25.485 % |
c |     17101 |   99630   336889 |  107083   14918    77511     5.2 | 27.570 % |
c |     25750 |   98571   333364 |  117791   23187   158309     6.8 | 28.442 % |
c |     38724 |   98182   332074 |  129570   35921   519883    14.5 | 28.749 % |
c |     58188 |   97052   328334 |  142527   55063   860735    15.6 | 29.665 % |
c |     87381 |   96258   325704 |  156780   83976  1704224    20.3 | 30.303 % |
c |    131173 |   95664   323755 |  172458  127605  4269068    33.5 | 30.805 % |
c |    196857 |   95173   322129 |  189704   38517  3098699    80.5 | 31.190 % |
c |    295384 |   94701   320570 |  208674  136906 13339558    97.4 | 31.540 % |
c |    443173 |   94522   319981 |  229542   93567 10107465   108.0 | 31.682 % |
#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.85 0.95 0.90 2/54 15175
Raw data (stat): 15175 (runsolver) R 15174 11931 11930 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 479830961 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0001 s]
Raw data (loadavg): 0.87 0.95 0.90 2/54 15175
Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 2747 0 0 0 991 7 0 0 25 0 1 0 479830961 13230080 2721 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3230 2721 603 41 0 3189 0
vsize: 12920
[startup+20.0006 s]
Raw data (loadavg): 0.89 0.96 0.91 2/54 15175
Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 2761 0 0 0 1991 7 0 0 25 0 1 0 479830961 13230080 2735 4294967295 134512640 134672761 3221224560 3221223732 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3230 2735 603 41 0 3189 0
vsize: 12920
[startup+30.0009 s]
Raw data (loadavg): 0.91 0.96 0.91 2/54 15175
Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 2778 0 0 0 2991 7 0 0 25 0 1 0 479830961 13365248 2752 4294967295 134512640 134672761 3221224560 3221223728 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3263 2752 603 41 0 3222 0
vsize: 13052
[startup+40.0007 s]
Raw data (loadavg): 0.92 0.96 0.91 2/54 15175
Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 2799 0 0 0 3990 7 0 0 25 0 1 0 479830961 13365248 2773 4294967295 134512640 134672761 3221224560 3221223684 134566077 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3263 2773 603 41 0 3222 0
vsize: 13052
[startup+50.0011 s]
Raw data (loadavg): 0.93 0.96 0.91 2/54 15175
Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 2808 0 0 0 4989 7 0 0 25 0 1 0 479830961 13500416 2782 4294967295 134512640 134672761 3221224560 3221223732 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3296 2782 603 41 0 3255 0
vsize: 13184
[startup+60.0013 s]
Raw data (loadavg): 0.94 0.96 0.91 2/54 15175
Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 2826 0 0 0 5989 8 0 0 25 0 1 0 479830961 13500416 2800 4294967295 134512640 134672761 3221224560 3221223732 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3296 2800 603 41 0 3255 0
vsize: 13184
[startup+70.0021 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 15175
Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 2841 0 0 0 6989 8 0 0 25 0 1 0 479830961 13635584 2815 4294967295 134512640 134672761 3221224560 3221223776 134557507 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3329 2815 603 41 0 3288 0
vsize: 13316
[startup+80.0025 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 15175
Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 2864 0 0 0 7988 9 0 0 25 0 1 0 479830961 13770752 2838 4294967295 134512640 134672761 3221224560 3221223732 134556660 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3362 2838 603 41 0 3321 0
vsize: 13448
[startup+90.0023 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 15175
Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 2888 0 0 0 8988 9 0 0 25 0 1 0 479830961 13770752 2862 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3362 2862 603 41 0 3321 0
vsize: 13448
[startup+100.002 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 15175
Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 2928 0 0 0 9988 10 0 0 25 0 1 0 479830961 14049280 2902 4294967295 134512640 134672761 3221224560 3221223760 134561972 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3430 2902 603 41 0 3389 0
vsize: 13720
[startup+110.003 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 15175
Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 3012 0 0 0 10987 10 0 0 25 0 1 0 479830961 14319616 2986 4294967295 134512640 134672761 3221224560 3221223712 134565103 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3496 2986 603 41 0 3455 0
vsize: 13984
[startup+120.004 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 15175
Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 3501 0 0 0 11985 12 0 0 25 0 1 0 479830961 16478208 3475 4294967295 134512640 134672761 3221224560 3221223728 134561207 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4023 3475 603 41 0 3982 0
vsize: 16092
[startup+130.004 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 15175
Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 3631 0 0 0 12984 13 0 0 25 0 1 0 479830961 16883712 3605 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4122 3605 603 41 0 4081 0
vsize: 16488
[startup+140.003 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 15175
Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 3779 0 0 0 13983 14 0 0 25 0 1 0 479830961 17551360 3753 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4285 3753 603 41 0 4244 0
vsize: 17140
[startup+150.004 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 15175
Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 3970 0 0 0 14982 15 0 0 25 0 1 0 479830961 18223104 3944 4294967295 134512640 134672761 3221224560 3221223684 134566057 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4449 3944 603 41 0 4408 0
vsize: 17796
[startup+160.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15175
Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 4152 0 0 0 15981 17 0 0 25 0 1 0 479830961 19025920 4126 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4645 4126 603 41 0 4604 0
vsize: 18580
[startup+170.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15175
Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 4332 0 0 0 16980 17 0 0 25 0 1 0 479830961 19697664 4306 4294967295 134512640 134672761 3221224560 3221223684 134566034 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4809 4306 603 41 0 4768 0
vsize: 19236
[startup+180.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15175
Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 4603 0 0 0 17979 18 0 0 25 0 1 0 479830961 21037056 4577 4294967295 134512640 134672761 3221224560 3221223744 134559498 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5136 4577 603 41 0 5095 0
vsize: 20544
[startup+190.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15175
Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 4998 0 0 0 18978 20 0 0 25 0 1 0 479830961 22659072 4972 4294967295 134512640 134672761 3221224560 3221223744 134559274 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5532 4972 603 41 0 5491 0
vsize: 22128
[startup+200.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15175
Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 5311 0 0 0 19977 21 0 0 25 0 1 0 479830961 23871488 5285 4294967295 134512640 134672761 3221224560 3221223732 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5828 5285 603 41 0 5787 0
vsize: 23312
[startup+210.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15175
Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 5593 0 0 0 20976 22 0 0 25 0 1 0 479830961 25088000 5567 4294967295 134512640 134672761 3221224560 3221223696 134565127 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6125 5567 603 41 0 6084 0
vsize: 24500
[startup+220.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15175
Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 5910 0 0 0 21975 24 0 0 25 0 1 0 479830961 26300416 5884 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6421 5884 603 41 0 6380 0
vsize: 25684
[startup+230.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15175
Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 6255 0 0 0 22973 25 0 0 25 0 1 0 479830961 27652096 6229 4294967295 134512640 134672761 3221224560 3221223728 134560839 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6751 6229 603 41 0 6710 0
vsize: 27004
[startup+240.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15175
Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 6889 0 0 0 23971 28 0 0 25 0 1 0 479830961 30212096 6863 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7376 6863 603 41 0 7335 0
vsize: 29504
[startup+250.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15175
Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 7653 0 0 0 24969 29 0 0 25 0 1 0 479830961 33312768 7627 4294967295 134512640 134672761 3221224560 3221223684 134566034 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8133 7627 603 41 0 8092 0
vsize: 32532
[startup+260.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15175
Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 8643 0 0 0 25968 31 0 0 25 0 1 0 479830961 37871616 8617 4294967295 134512640 134672761 3221224560 3221223696 134560557 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9246 8617 603 41 0 9205 0
vsize: 36984
[startup+270.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15175
Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 9461 0 0 0 26965 34 0 0 25 0 1 0 479830961 41234432 9435 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10067 9435 603 41 0 10026 0
vsize: 40268
[startup+280.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15175
Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 10014 0 0 0 27964 36 0 0 25 0 1 0 479830961 43515904 9988 4294967295 134512640 134672761 3221224560 3221223732 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10624 9988 603 41 0 10583 0
vsize: 42496
[startup+290.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15175
Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 10846 0 0 0 28961 38 0 0 25 0 1 0 479830961 46870528 10820 4294967295 134512640 134672761 3221224560 3221223732 134556651 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11443 10820 603 41 0 11402 0
vsize: 45772
[startup+300.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15175
Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 11625 0 0 0 29959 40 0 0 25 0 1 0 479830961 49967104 11599 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12199 11599 603 41 0 12158 0
vsize: 48796
[startup+310.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15175
Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 12013 0 0 0 30959 41 0 0 25 0 1 0 479830961 51580928 11987 4294967295 134512640 134672761 3221224560 3221223732 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12593 11987 603 41 0 12552 0
vsize: 50372
[startup+320.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15175
Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 12690 0 0 0 31958 42 0 0 25 0 1 0 479830961 54272000 12664 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13250 12664 603 41 0 13209 0
vsize: 53000
[startup+330.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15175
Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 13302 0 0 0 32956 44 0 0 25 0 1 0 479830961 56827904 13276 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13874 13276 603 41 0 13833 0
vsize: 55496
[startup+340.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15175
Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 13870 0 0 0 33954 46 0 0 25 0 1 0 479830961 59109376 13844 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14431 13844 603 41 0 14390 0
vsize: 57724
[startup+350.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15175
Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 14322 0 0 0 34953 47 0 0 25 0 1 0 479830961 60989440 14296 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14890 14296 603 41 0 14849 0
vsize: 59560
[startup+360.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15175
Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 14322 0 0 0 35953 47 0 0 25 0 1 0 479830961 60989440 14296 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14890 14296 603 41 0 14849 0
vsize: 59560
[startup+370.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15175
Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 14322 0 0 0 36953 47 0 0 25 0 1 0 479830961 60989440 14296 4294967295 134512640 134672761 3221224560 3221223728 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14890 14296 603 41 0 14849 0
vsize: 59560
[startup+380.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15175
Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 14322 0 0 0 37953 47 0 0 25 0 1 0 479830961 60989440 14296 4294967295 134512640 134672761 3221224560 3221223728 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14890 14296 603 41 0 14849 0
vsize: 59560
[startup+390.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15175
Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 14322 0 0 0 38953 47 0 0 25 0 1 0 479830961 60989440 14296 4294967295 134512640 134672761 3221224560 3221223728 134561198 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14890 14296 603 41 0 14849 0
vsize: 59560
[startup+400.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15175
Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 14322 0 0 0 39953 47 0 0 25 0 1 0 479830961 60989440 14296 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14890 14296 603 41 0 14849 0
vsize: 59560
[startup+410.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15175
Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 14322 0 0 0 40953 47 0 0 25 0 1 0 479830961 60989440 14296 4294967295 134512640 134672761 3221224560 3221223732 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14890 14296 603 41 0 14849 0
vsize: 59560
[startup+420.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15175
Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 14322 0 0 0 41954 47 0 0 25 0 1 0 479830961 60989440 14296 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14890 14296 603 41 0 14849 0
vsize: 59560
[startup+430.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15175
Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 14322 0 0 0 42954 48 0 0 25 0 1 0 479830961 60989440 14296 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14890 14296 603 41 0 14849 0
vsize: 59560
[startup+440.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15175
Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 14322 0 0 0 43954 48 0 0 25 0 1 0 479830961 60989440 14296 4294967295 134512640 134672761 3221224560 3221223728 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14890 14296 603 41 0 14849 0
vsize: 59560
[startup+450.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15175
Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 14322 0 0 0 44954 48 0 0 25 0 1 0 479830961 60989440 14296 4294967295 134512640 134672761 3221224560 3221223728 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14890 14296 603 41 0 14849 0
vsize: 59560
[startup+460.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15175
Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 14322 0 0 0 45954 48 0 0 25 0 1 0 479830961 60989440 14296 4294967295 134512640 134672761 3221224560 3221223732 134556667 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14890 14296 603 41 0 14849 0
vsize: 59560
[startup+470.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15175
Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 14322 0 0 0 46954 48 0 0 25 0 1 0 479830961 60989440 14296 4294967295 134512640 134672761 3221224560 3221223728 134560882 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14890 14296 603 41 0 14849 0
vsize: 59560
[startup+480.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15175
Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 14737 0 0 0 47953 49 0 0 25 0 1 0 479830961 62730240 14711 4294967295 134512640 134672761 3221224560 3221223728 134560882 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15315 14711 603 41 0 15274 0
vsize: 61260
[startup+490.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15175
Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 15302 0 0 0 48952 50 0 0 25 0 1 0 479830961 65024000 15276 4294967295 134512640 134672761 3221224560 3221223728 134560858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15875 15276 603 41 0 15834 0
vsize: 63500
[startup+500.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15175
Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 15840 0 0 0 49951 52 0 0 25 0 1 0 479830961 67178496 15814 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16401 15814 603 41 0 16360 0
vsize: 65604
[startup+510.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15175
Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 16263 0 0 0 50950 52 0 0 25 0 1 0 479830961 68947968 16237 4294967295 134512640 134672761 3221224560 3221223732 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16833 16237 603 41 0 16792 0
vsize: 67332
[startup+520.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15175
Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 16667 0 0 0 51949 54 0 0 25 0 1 0 479830961 70692864 16641 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17259 16641 603 41 0 17218 0
vsize: 69036
[startup+530.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15175
Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 17027 0 0 0 52948 55 0 0 25 0 1 0 479830961 72175616 17001 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17621 17001 603 41 0 17580 0
vsize: 70484
[startup+540.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15175
Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 17513 0 0 0 53946 57 0 0 25 0 1 0 479830961 74194944 17487 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18114 17487 603 41 0 18073 0
vsize: 72456
[startup+550.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15175
Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 17863 0 0 0 54946 58 0 0 25 0 1 0 479830961 75546624 17837 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18444 17837 603 41 0 18403 0
vsize: 73776
[startup+560.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15175
Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 18250 0 0 0 55945 59 0 0 25 0 1 0 479830961 77144064 18224 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18834 18224 603 41 0 18793 0
vsize: 75336
[startup+570.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15175
Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 18757 0 0 0 56944 60 0 0 25 0 1 0 479830961 79278080 18731 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19355 18731 603 41 0 19314 0
vsize: 77420
[startup+580.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15175
Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 19097 0 0 0 57942 62 0 0 25 0 1 0 479830961 80625664 19071 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19684 19071 603 41 0 19643 0
vsize: 78736
[startup+590.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15175
Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 19511 0 0 0 58942 62 0 0 25 0 1 0 479830961 82366464 19485 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20109 19485 603 41 0 20068 0
vsize: 80436
[startup+600.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15175
Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 19917 0 0 0 59940 64 0 0 25 0 1 0 479830961 84099072 19891 4294967295 134512640 134672761 3221224560 3221223728 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20532 19891 603 41 0 20491 0
vsize: 82128
[startup+610.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15175
Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 20316 0 0 0 60940 64 0 0 25 0 1 0 479830961 85716992 20290 4294967295 134512640 134672761 3221224560 3221223744 134558899 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20927 20290 603 41 0 20886 0
vsize: 83708
[startup+620.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15175
Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 20764 0 0 0 61938 66 0 0 25 0 1 0 479830961 87568384 20738 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21379 20738 603 41 0 21338 0
vsize: 85516
[startup+630.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15175
Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 21246 0 0 0 62937 68 0 0 25 0 1 0 479830961 89550848 21220 4294967295 134512640 134672761 3221224560 3221223728 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21863 21220 603 41 0 21822 0
vsize: 87452
[startup+640.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15175
Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 21653 0 0 0 63936 69 0 0 25 0 1 0 479830961 91279360 21627 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22285 21628 603 41 0 22244 0
vsize: 89140
[startup+650.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15175
Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 22054 0 0 0 64934 71 0 0 25 0 1 0 479830961 92872704 22028 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22674 22028 603 41 0 22633 0
vsize: 90696
[startup+660.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15175
Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 22448 0 0 0 65932 73 0 0 25 0 1 0 479830961 94470144 22422 4294967295 134512640 134672761 3221224560 3221223664 134560224 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23064 22422 603 41 0 23023 0
vsize: 92256
[startup+670.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15175
Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 22815 0 0 0 66932 74 0 0 25 0 1 0 479830961 96055296 22789 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23451 22789 603 41 0 23410 0
vsize: 93804
[startup+680.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15175
Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 23160 0 0 0 67931 75 0 0 25 0 1 0 479830961 97386496 23134 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23776 23134 603 41 0 23735 0
vsize: 95104
[startup+690.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15175
Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 23493 0 0 0 68930 76 0 0 25 0 1 0 479830961 98848768 23467 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24133 23467 603 41 0 24092 0
vsize: 96532
[startup+700.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15175
Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 23828 0 0 0 69930 76 0 0 25 0 1 0 479830961 100294656 23802 4294967295 134512640 134672761 3221224560 3221223480 1075351236 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24486 23802 603 41 0 24445 0
vsize: 97944
[startup+710.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15175
Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 24179 0 0 0 70929 77 0 0 25 0 1 0 479830961 101793792 24153 4294967295 134512640 134672761 3221224560 3221223728 134560942 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24852 24153 603 41 0 24811 0
vsize: 99408
[startup+720.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15175
Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 24525 0 0 0 71929 78 0 0 25 0 1 0 479830961 103124992 24499 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25177 24499 603 41 0 25136 0
vsize: 100708
[startup+730.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15175
Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 24914 0 0 0 72928 79 0 0 25 0 1 0 479830961 104722432 24888 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25567 24888 603 41 0 25526 0
vsize: 102268
[startup+740.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15175
Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 25266 0 0 0 73927 80 0 0 25 0 1 0 479830961 106188800 25240 4294967295 134512640 134672761 3221224560 3221223728 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25925 25240 603 41 0 25884 0
vsize: 103700
[startup+750.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15175
Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 25584 0 0 0 74927 80 0 0 25 0 1 0 479830961 107511808 25558 4294967295 134512640 134672761 3221224560 3221223664 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26248 25558 603 41 0 26207 0
vsize: 104992
[startup+760.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15175
Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 25912 0 0 0 75926 81 0 0 25 0 1 0 479830961 108847104 25886 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26574 25886 603 41 0 26533 0
vsize: 106296
[startup+770.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15175
Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 26211 0 0 0 76926 82 0 0 25 0 1 0 479830961 110059520 26185 4294967295 134512640 134672761 3221224560 3221223728 134561226 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26870 26185 603 41 0 26829 0
vsize: 107480
[startup+780.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15175
Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 26528 0 0 0 77925 83 0 0 25 0 1 0 479830961 111394816 26502 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27196 26502 603 41 0 27155 0
vsize: 108784
[startup+790.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15175
Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 26843 0 0 0 78925 84 0 0 25 0 1 0 479830961 112599040 26817 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27490 26817 603 41 0 27449 0
vsize: 109960
[startup+800.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15175
Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 27195 0 0 0 79924 84 0 0 25 0 1 0 479830961 114053120 27169 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27845 27169 603 41 0 27804 0
vsize: 111380
[startup+810.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15175
Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 27504 0 0 0 80924 85 0 0 25 0 1 0 479830961 115388416 27478 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28171 27478 603 41 0 28130 0
vsize: 112684
[startup+820.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15175
Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 27814 0 0 0 81923 85 0 0 25 0 1 0 479830961 116584448 27788 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28463 27788 603 41 0 28422 0
vsize: 113852
[startup+830.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15175
Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 28085 0 0 0 82922 86 0 0 25 0 1 0 479830961 117780480 28059 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28755 28059 603 41 0 28714 0
vsize: 115020
[startup+840.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15175
Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 28338 0 0 0 83922 87 0 0 25 0 1 0 479830961 118714368 28312 4294967295 134512640 134672761 3221224560 3221223728 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28983 28312 603 41 0 28942 0
vsize: 115932
[startup+850.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15175
Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 28639 0 0 0 84921 88 0 0 25 0 1 0 479830961 119943168 28613 4294967295 134512640 134672761 3221224560 3221223728 134560871 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29283 28613 603 41 0 29242 0
vsize: 117132
[startup+860.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15175
Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 28903 0 0 0 85920 90 0 0 25 0 1 0 479830961 121028608 28877 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29548 28877 603 41 0 29507 0
vsize: 118192
[startup+870.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15175
Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 29258 0 0 0 86919 90 0 0 25 0 1 0 479830961 122593280 29232 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29930 29232 603 41 0 29889 0
vsize: 119720
[startup+880.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15175
Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 29551 0 0 0 87919 91 0 0 25 0 1 0 479830961 123826176 29525 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30231 29525 603 41 0 30190 0
vsize: 120924
[startup+890.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15175
Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 29805 0 0 0 88918 92 0 0 25 0 1 0 479830961 124903424 29779 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30494 29779 603 41 0 30453 0
vsize: 121976
[startup+900.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15175
Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 30025 0 0 0 89918 92 0 0 25 0 1 0 479830961 125841408 29999 4294967295 134512640 134672761 3221224560 3221223728 134560874 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30723 29999 603 41 0 30682 0
vsize: 122892
[startup+910.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15175
Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 30307 0 0 0 90917 93 0 0 25 0 1 0 479830961 127049728 30281 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31018 30281 603 41 0 30977 0
vsize: 124072
[startup+920.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15175
Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 30781 0 0 0 91916 95 0 0 25 0 1 0 479830961 128909312 30755 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31472 30755 603 41 0 31431 0
vsize: 125888
[startup+930.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15175
Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 31267 0 0 0 92914 96 0 0 25 0 1 0 479830961 130916352 31241 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31962 31241 603 41 0 31921 0
vsize: 127848
[startup+940.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15175
Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 31571 0 0 0 93913 97 0 0 25 0 1 0 479830961 132120576 31545 4294967295 134512640 134672761 3221224560 3221223664 134554642 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32256 31545 603 41 0 32215 0
vsize: 129024
[startup+950.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15175
Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 31572 0 0 0 94914 97 0 0 25 0 1 0 479830961 132120576 31546 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32256 31546 603 41 0 32215 0
vsize: 129024
[startup+960.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15175
Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 31572 0 0 0 95914 98 0 0 25 0 1 0 479830961 132120576 31546 4294967295 134512640 134672761 3221224560 3221223728 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32256 31546 603 41 0 32215 0
vsize: 129024
[startup+970.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15175
Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 31572 0 0 0 96914 98 0 0 25 0 1 0 479830961 132120576 31546 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32256 31546 603 41 0 32215 0
vsize: 129024
[startup+980.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15175
Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 31572 0 0 0 97914 98 0 0 25 0 1 0 479830961 132120576 31546 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32256 31546 603 41 0 32215 0
vsize: 129024
[startup+990.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15175
Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 31572 0 0 0 98914 98 0 0 25 0 1 0 479830961 132120576 31546 4294967295 134512640 134672761 3221224560 3221223664 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32256 31546 603 41 0 32215 0
vsize: 129024
[startup+1000.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15175
Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 31572 0 0 0 99914 98 0 0 25 0 1 0 479830961 132120576 31546 4294967295 134512640 134672761 3221224560 3221223728 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32256 31546 603 41 0 32215 0
vsize: 129024
[startup+1010.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15175
Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 31573 0 0 0 100914 98 0 0 25 0 1 0 479830961 132120576 31547 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32256 31547 603 41 0 32215 0
vsize: 129024
[startup+1020.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15175
Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 31573 0 0 0 101914 98 0 0 25 0 1 0 479830961 132120576 31547 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32256 31547 603 41 0 32215 0
vsize: 129024
[startup+1030.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15175
Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 31573 0 0 0 102915 98 0 0 25 0 1 0 479830961 132120576 31547 4294967295 134512640 134672761 3221224560 3221223744 134559405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32256 31547 603 41 0 32215 0
vsize: 129024
[startup+1040.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15175
Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 31573 0 0 0 103915 98 0 0 25 0 1 0 479830961 132120576 31547 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32256 31547 603 41 0 32215 0
vsize: 129024
[startup+1050.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15175
Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 31575 0 0 0 104915 98 0 0 25 0 1 0 479830961 132120576 31549 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32256 31549 603 41 0 32215 0
vsize: 129024
[startup+1060.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15175
Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 31578 0 0 0 105915 98 0 0 25 0 1 0 479830961 132120576 31552 4294967295 134512640 134672761 3221224560 3221223728 134560931 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32256 31552 603 41 0 32215 0
vsize: 129024
[startup+1070.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15175
Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 31578 0 0 0 106915 98 0 0 25 0 1 0 479830961 132120576 31552 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32256 31552 603 41 0 32215 0
vsize: 129024
[startup+1080.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15175
Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 31578 0 0 0 107915 98 0 0 25 0 1 0 479830961 132120576 31552 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32256 31552 603 41 0 32215 0
vsize: 129024
[startup+1090.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15175
Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 31578 0 0 0 108915 98 0 0 25 0 1 0 479830961 132120576 31552 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32256 31552 603 41 0 32215 0
vsize: 129024
[startup+1100.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15175
Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 31578 0 0 0 109915 98 0 0 25 0 1 0 479830961 132120576 31552 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32256 31552 603 41 0 32215 0
vsize: 129024
[startup+1110.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15175
Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 31578 0 0 0 110916 98 0 0 25 0 1 0 479830961 132120576 31552 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32256 31552 603 41 0 32215 0
vsize: 129024
[startup+1120.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15175
Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 31578 0 0 0 111916 98 0 0 25 0 1 0 479830961 132120576 31552 4294967295 134512640 134672761 3221224560 3221223728 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32256 31552 603 41 0 32215 0
vsize: 129024
[startup+1130.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15175
Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 31579 0 0 0 112916 98 0 0 25 0 1 0 479830961 132120576 31553 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32256 31553 603 41 0 32215 0
vsize: 129024
[startup+1140.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15175
Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 31579 0 0 0 113916 98 0 0 25 0 1 0 479830961 132120576 31553 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32256 31553 603 41 0 32215 0
vsize: 129024
[startup+1150.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15175
Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 31579 0 0 0 114916 98 0 0 25 0 1 0 479830961 132120576 31553 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32256 31553 603 41 0 32215 0
vsize: 129024
[startup+1160.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15175
Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 31579 0 0 0 115917 98 0 0 25 0 1 0 479830961 132120576 31553 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32256 31553 603 41 0 32215 0
vsize: 129024
[startup+1170.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15175
Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 31579 0 0 0 116917 99 0 0 25 0 1 0 479830961 132120576 31553 4294967295 134512640 134672761 3221224560 3221223664 134559872 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32256 31553 603 41 0 32215 0
vsize: 129024
[startup+1180.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15175
Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 31579 0 0 0 117917 99 0 0 25 0 1 0 479830961 132120576 31553 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32256 31553 603 41 0 32215 0
vsize: 129024
[startup+1190.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15175
Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 31579 0 0 0 118917 99 0 0 25 0 1 0 479830961 132120576 31553 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32256 31553 603 41 0 32215 0
vsize: 129024
[startup+1200.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15175
Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 31579 0 0 0 119917 99 0 0 25 0 1 0 479830961 132120576 31553 4294967295 134512640 134672761 3221224560 3221223728 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32256 31553 603 41 0 32215 0
vsize: 129024
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.09 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 15175
Raw data (stat): 15175 (minisat+) Z 15174 11931 11930 0 -1 12 31581 0 0 0 119917 105 0 0 25 0 1 0 479830961 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.09
CPU time (s): 1200.23
CPU user time (s): 1199.18
CPU system time (s): 1.05084
CPU usage (%): 100.011
Max. virtual memory (Kb): 129024
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####