PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/web/www.ps.uni-sb.de/~walser/benchmarks/ppp-problems/normalized-ppp:1,3-13,19.opb
MD5SUM	fa67033d6a242cf79309b3804f79a4fe
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	102
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	15.8556
Number of variables	4608
Total number of constraints	34956
Number of constraints which are clauses	29328
Number of constraints which are cardinality constraints (but not clauses)	5550
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 5280

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

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        851728 kB
Buffers:         40192 kB
Cached:         118316 kB
SwapCached:          0 kB
Active:         107884 kB
Inactive:        53704 kB
HighTotal:      131008 kB
HighFree:        20020 kB
LowTotal:       903652 kB
LowFree:        831708 kB
SwapTotal:     2097136 kB
SwapFree:      2097136 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           7200 kB
Slab:            15724 kB
Committed_AS:    92820 kB
PageTables:        344 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-13 23:34:53 (client local time) WITH STATUS 0 IN 1200.24 SECONDS
stats: 3744 7 1200.24 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 30522 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ##############################################################################################################################################################################
c   -- Clauses(.)/Splits(s): ................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ---[30521]---> Adder-cost: 50   maxlim: 59   bits: 7/6
c ---[30520]---> Adder-cost: 50   maxlim: 59   bits: 7/6
c ---[30519]---> Adder-cost: 50   maxlim: 59   bits: 7/6
c ---[30518]---> Adder-cost: 50   maxlim: 59   bits: 7/6
c ---[30517]---> Adder-cost: 50   maxlim: 59   bits: 7/6
c ---[30516]---> Adder-cost: 50   maxlim: 59   bits: 7/6
c ---[30515]---> Adder-cost: 66   maxlim: 84   bits: 7/7
c ---[30514]---> Adder-cost: 66   maxlim: 84   bits: 7/7
c ---[30513]---> Adder-cost: 66   maxlim: 84   bits: 7/7
c ---[30512]---> Adder-cost: 66   maxlim: 84   bits: 7/7
c ---[30511]---> Adder-cost: 66   maxlim: 84   bits: 7/7
c ---[30510]---> Adder-cost: 66   maxlim: 84   bits: 7/7
c ---[30509]---> Adder-cost: 66   maxlim: 83   bits: 7/7
c ---[30508]---> Adder-cost: 66   maxlim: 83   bits: 7/7
c ---[30507]---> Adder-cost: 66   maxlim: 83   bits: 7/7
c ---[30506]---> Adder-cost: 66   maxlim: 83   bits: 7/7
c ---[30505]---> Adder-cost: 66   maxlim: 83   bits: 7/7
c ---[30504]---> Adder-cost: 66   maxlim: 83   bits: 7/7
c ---[30503]---> Adder-cost: 66   maxlim: 83   bits: 7/7
c ---[30502]---> Adder-cost: 66   maxlim: 83   bits: 7/7
c ---[30501]---> Adder-cost: 66   maxlim: 83   bits: 7/7
c ---[30500]---> Adder-cost: 66   maxlim: 83   bits: 7/7
c ---[30499]---> Adder-cost: 66   maxlim: 83   bits: 7/7
c ---[30498]---> Adder-cost: 66   maxlim: 83   bits: 7/7
c ---[30497]---> Adder-cost: 66   maxlim: 83   bits: 7/7
c ---[30496]---> Adder-cost: 66   maxlim: 83   bits: 7/7
c ---[30495]---> Adder-cost: 66   maxlim: 83   bits: 7/7
c ---[30494]---> Adder-cost: 66   maxlim: 83   bits: 7/7
c ---[30493]---> Adder-cost: 66   maxlim: 83   bits: 7/7
c ---[30492]---> Adder-cost: 66   maxlim: 83   bits: 7/7
c ---[30491]---> Adder-cost: 66   maxlim: 82   bits: 7/7
c ---[30490]---> Adder-cost: 66   maxlim: 82   bits: 7/7
c ---[30489]---> Adder-cost: 66   maxlim: 82   bits: 7/7
c ---[30488]---> Adder-cost: 66   maxlim: 82   bits: 7/7
c ---[30487]---> Adder-cost: 66   maxlim: 82   bits: 7/7
c ---[30486]---> Adder-cost: 66   maxlim: 82   bits: 7/7
c ---[30485]---> Adder-cost: 66   maxlim: 83   bits: 7/7
c ---[30484]---> Adder-cost: 66   maxlim: 83   bits: 7/7
c ---[30483]---> Adder-cost: 66   maxlim: 83   bits: 7/7
c ---[30482]---> Adder-cost: 66   maxlim: 83   bits: 7/7
c ---[30481]---> Adder-cost: 66   maxlim: 83   bits: 7/7
c ---[30480]---> Adder-cost: 66   maxlim: 83   bits: 7/7
c ---[30479]---> Adder-cost: 66   maxlim: 83   bits: 7/7
c ---[30478]---> Adder-cost: 66   maxlim: 83   bits: 7/7
c ---[30477]---> Adder-cost: 66   maxlim: 83   bits: 7/7
c ---[30476]---> Adder-cost: 66   maxlim: 83   bits: 7/7
c ---[30475]---> Adder-cost: 66   maxlim: 83   bits: 7/7
c ---[30474]---> Adder-cost: 66   maxlim: 83   bits: 7/7
c ---[30473]---> Adder-cost: 66   maxlim: 83   bits: 7/7
c ---[30472]---> Adder-cost: 66   maxlim: 83   bits: 7/7
c ---[30471]---> Adder-cost: 66   maxlim: 83   bits: 7/7
c ---[30470]---> Adder-cost: 66   maxlim: 83   bits: 7/7
c ---[30469]---> Adder-cost: 66   maxlim: 83   bits: 7/7
c ---[30468]---> Adder-cost: 66   maxlim: 83   bits: 7/7
c ---[30467]---> Adder-cost: 66   maxlim: 81   bits: 7/7
c ---[30466]---> Adder-cost: 66   maxlim: 81   bits: 7/7
c ---[30465]---> Adder-cost: 66   maxlim: 81   bits: 7/7
c ---[30464]---> Adder-cost: 66   maxlim: 81   bits: 7/7
c ---[30463]---> Adder-cost: 66   maxlim: 81   bits: 7/7
c ---[30462]---> Adder-cost: 66   maxlim: 81   bits: 7/7
c ---[30461]---> Adder-cost: 66   maxlim: 81   bits: 7/7
c ---[30460]---> Adder-cost: 66   maxlim: 81   bits: 7/7
c ---[30459]---> Adder-cost: 66   maxlim: 81   bits: 7/7
c ---[30458]---> Adder-cost: 66   maxlim: 81   bits: 7/7
c ---[30457]---> Adder-cost: 66   maxlim: 81   bits: 7/7
c ---[30456]---> Adder-cost: 66   maxlim: 81   bits: 7/7
c ---[30455]---> Adder-cost: 50   maxlim: 59   bits: 7/6
c ---[30454]---> Adder-cost: 50   maxlim: 59   bits: 7/6
c ---[30453]---> Adder-cost: 50   maxlim: 59   bits: 7/6
c ---[30452]---> Adder-cost: 50   maxlim: 59   bits: 7/6
c ---[30451]---> Adder-cost: 50   maxlim: 59   bits: 7/6
c ---[30450]---> Adder-cost: 50   maxlim: 59   bits: 7/6
c ---[30449]---> Adder-cost: 50   maxlim: 59   bits: 7/6
c ---[30448]---> Adder-cost: 50   maxlim: 59   bits: 7/6
c ---[30447]---> Adder-cost: 50   maxlim: 59   bits: 7/6
c ---[30446]---> Adder-cost: 50   maxlim: 59   bits: 7/6
c ---[30445]---> Adder-cost: 50   maxlim: 59   bits: 7/6
c ---[30444]---> Adder-cost: 50   maxlim: 59   bits: 7/6
c ---[30442]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30440]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30438]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30436]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30434]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30432]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30430]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30428]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30426]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30424]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30422]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30420]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30418]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30416]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30414]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30412]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30410]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30408]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30406]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[30404]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[30402]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[30400]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[30398]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[30396]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[30394]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30392]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30390]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30388]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30386]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30384]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30382]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30380]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30378]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30376]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30374]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30372]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30370]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[30368]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[30366]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[30364]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[30362]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[30360]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[30358]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[30356]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[30354]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[30352]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[30350]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[30348]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[30346]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30344]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30342]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30340]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30338]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30336]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30334]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30332]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30330]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30328]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30326]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30324]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30322]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30320]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30318]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30316]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30314]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30312]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30310]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[30308]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[30306]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[30304]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[30302]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[30300]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[30298]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30296]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30294]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30292]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30290]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30288]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30286]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30284]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30282]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30280]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30278]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30276]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30274]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30272]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30270]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30268]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30266]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30264]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30262]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30260]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30258]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30256]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30254]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30252]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30250]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30248]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30246]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30244]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30242]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30240]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30238]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30236]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30234]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30232]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30230]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30228]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30226]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30224]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30222]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30220]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30218]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30216]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30214]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30212]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30210]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30208]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30206]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30204]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30202]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30200]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30198]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30196]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30194]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30192]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30190]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30188]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30186]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30184]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30182]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30180]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30178]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30176]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30174]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30172]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30170]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30168]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30166]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30164]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30162]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30160]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30158]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30156]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30154]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30152]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30150]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30148]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30146]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30144]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30142]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30140]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30138]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30136]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30134]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30132]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30130]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30128]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30126]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30124]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30122]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30120]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30118]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[30116]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[30114]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[30112]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[30110]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[30108]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[30106]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30104]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30102]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30100]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30098]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30096]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30095]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30094]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30093]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30092]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30091]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30090]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30089]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30088]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30087]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30086]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30085]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30084]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30083]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30082]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30081]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30080]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30079]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30078]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30077]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30076]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30075]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30074]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30073]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30072]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30071]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30070]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30069]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30068]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30067]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30066]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30065]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30064]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30063]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30062]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30061]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30060]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30059]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30058]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30057]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30056]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30055]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30054]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30053]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30052]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30051]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30050]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30049]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30048]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30047]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30046]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30045]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30044]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30043]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30042]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30041]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30040]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30039]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30038]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30037]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30036]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30035]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30034]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30033]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30032]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30031]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30030]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30029]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30028]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30027]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30026]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30025]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30024]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30023]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30022]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30021]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30020]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30019]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30018]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30017]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30016]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30015]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30014]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30013]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30012]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30011]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30010]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30009]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30008]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30007]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30006]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30005]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30004]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30003]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30002]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30001]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30000]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29999]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29998]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29997]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29996]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29995]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29994]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29993]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29992]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29991]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29990]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29989]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29988]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29987]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29986]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29985]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29984]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29983]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29982]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29981]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29980]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29979]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29978]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29977]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29976]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29975]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29974]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29973]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29972]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29971]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29970]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29969]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29968]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29967]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29966]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29965]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29964]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29963]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29962]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29961]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29960]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29959]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29958]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29957]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29956]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29955]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29954]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29953]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29952]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29951]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29950]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29949]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29948]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29947]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29946]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29945]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29944]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29943]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29942]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29941]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29940]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29939]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29938]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29937]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29936]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29935]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29934]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29933]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29932]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29931]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29930]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29929]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29928]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29927]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29926]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29925]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29924]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29923]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29922]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29921]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29920]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29919]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29918]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29917]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29916]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29915]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29914]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29913]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29912]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29911]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29910]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29909]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29908]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29907]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29906]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29905]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29904]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29903]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29902]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29901]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29900]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29899]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29898]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29897]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29896]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29895]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29894]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29893]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29892]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29891]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29890]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29889]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29888]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29887]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29886]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29885]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29884]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29883]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29882]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29881]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29880]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29879]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29878]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29877]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29876]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29875]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29874]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29873]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29872]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29871]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29870]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29869]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29868]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29867]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29866]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29865]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29864]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29863]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29862]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29861]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29860]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29859]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29858]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29857]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29856]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29855]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29854]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29853]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29852]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29851]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29850]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29849]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29848]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29847]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29846]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29845]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29844]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29843]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29842]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29841]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29840]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29839]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29838]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29837]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29836]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29835]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29834]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29833]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29832]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29831]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29830]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29829]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29828]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29827]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29826]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29825]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29824]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29823]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29822]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29821]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29820]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29819]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29818]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29817]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29816]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29815]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29814]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29813]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29812]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29811]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29810]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29809]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29808]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29807]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29806]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29805]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29804]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29803]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29802]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29801]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29800]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29799]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29798]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29797]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29796]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29795]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29794]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29793]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29792]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29791]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29790]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29789]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29788]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29787]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29786]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29785]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29784]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29783]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29782]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29781]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29780]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29779]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29778]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29777]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29776]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29775]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29774]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29773]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29772]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29771]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29770]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29769]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29768]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29767]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29766]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29765]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29764]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29763]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29762]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29761]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29760]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29759]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29758]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29757]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29756]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29755]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29754]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29753]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29752]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29751]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29750]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29749]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29748]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29747]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29746]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29745]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29744]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29743]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29742]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29741]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29740]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29739]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29738]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29737]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29736]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29735]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[29734]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 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 |  110544   372762 |   36848       0        0     nan |  0.000 % |
c |       100 |  109852   370421 |   40532      23       63     2.7 | 16.952 % |
c |       250 |  109045   367691 |   44586      80      242     3.0 | 17.689 % |
c |       475 |  108465   365722 |   49044     251      991     3.9 | 18.205 % |
c |       814 |  108153   364666 |   53949     553     2434     4.4 | 18.456 % |
c |      1320 |  107815   363532 |   59344    1017     4914     4.8 | 18.726 % |
c |      2080 |  106928   360531 |   65278    1677     8026     4.8 | 19.483 % |
c |      3219 |  105759   356633 |   71806    2664    12887     4.8 | 20.441 % |
c |      4928 |  104860   353648 |   78986    4248    21828     5.1 | 21.233 % |
c |      7490 |  104090   351099 |   86885    6687    36570     5.5 | 21.877 % |
c |     11334 |  102750   346704 |   95574   10315    59110     5.7 | 23.012 % |
c |     17100 |  100980   340872 |  105131   15802   101505     6.4 | 24.555 % |
c |     25750 |   98972   334240 |  115644   24068   192047     8.0 | 26.300 % |
c |     38725 |   97160   328238 |  127209   36642   424049    11.6 | 27.775 % |
c |     58187 |   95910   324119 |  139930   55806  1588848    28.5 | 28.826 % |
c |     87380 |   95140   321580 |  153923   84851  3820497    45.0 | 29.470 % |
c |    131169 |   95096   321436 |  169315  128634  9333585    72.6 | 29.505 % |
c |    196854 |   94937   320917 |  186247   38190  4571157   119.7 | 29.637 % |
#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.93 0.97 0.91 2/56 16889
Raw data (stat): 16889 (runsolver) R 16888 12452 12451 0 -1 64 4 0 0 0 0 0 0 0 20 0 1 0 364754591 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0006 s]
Raw data (loadavg): 0.94 0.97 0.91 2/56 16889
Raw data (stat): 16889 (minisat+) R 16888 12452 12451 0 -1 0 2723 0 0 0 990 9 0 0 25 0 1 0 364754591 13185024 2695 4294967295 134512640 134672761 3221224560 3221223776 134561990 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3219 2695 603 41 0 3178 0
vsize: 12876
[startup+20.0021 s]
Raw data (loadavg): 0.95 0.97 0.91 2/56 16889
Raw data (stat): 16889 (minisat+) R 16888 12452 12451 0 -1 0 2736 0 0 0 1990 9 0 0 25 0 1 0 364754591 13320192 2708 4294967295 134512640 134672761 3221224560 3221223724 134564522 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3252 2708 603 41 0 3211 0
vsize: 13008
[startup+30.0022 s]
Raw data (loadavg): 0.95 0.97 0.91 2/56 16889
Raw data (stat): 16889 (minisat+) R 16888 12452 12451 0 -1 0 2751 0 0 0 2990 9 0 0 25 0 1 0 364754591 13320192 2723 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3252 2723 603 41 0 3211 0
vsize: 13008
[startup+40.002 s]
Raw data (loadavg): 0.96 0.97 0.91 2/56 16889
Raw data (stat): 16889 (minisat+) R 16888 12452 12451 0 -1 0 2791 0 0 0 3989 10 0 0 25 0 1 0 364754591 13455360 2763 4294967295 134512640 134672761 3221224560 3221223684 134566118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3285 2763 603 41 0 3244 0
vsize: 13140
[startup+50.0028 s]
Raw data (loadavg): 0.97 0.97 0.91 2/56 16889
Raw data (stat): 16889 (minisat+) R 16888 12452 12451 0 -1 0 2821 0 0 0 4989 10 0 0 25 0 1 0 364754591 13725696 2793 4294967295 134512640 134672761 3221224560 3221223684 134566057 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3351 2793 603 41 0 3310 0
vsize: 13404
[startup+60.0035 s]
Raw data (loadavg): 0.97 0.97 0.91 2/56 16889
Raw data (stat): 16889 (minisat+) R 16888 12452 12451 0 -1 0 2849 0 0 0 5989 10 0 0 25 0 1 0 364754591 13725696 2821 4294967295 134512640 134672761 3221224560 3221223776 134561997 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3351 2821 603 41 0 3310 0
vsize: 13404
[startup+70.0044 s]
Raw data (loadavg): 0.97 0.97 0.91 2/56 16889
Raw data (stat): 16889 (minisat+) R 16888 12452 12451 0 -1 0 2898 0 0 0 6989 11 0 0 25 0 1 0 364754591 13987840 2870 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3415 2870 603 41 0 3374 0
vsize: 13660
[startup+80.0049 s]
Raw data (loadavg): 0.98 0.97 0.91 2/56 16889
Raw data (stat): 16889 (minisat+) R 16888 12452 12451 0 -1 0 2960 0 0 0 7988 11 0 0 25 0 1 0 364754591 14196736 2932 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3466 2932 603 41 0 3425 0
vsize: 13864
[startup+90.0049 s]
Raw data (loadavg): 0.98 0.97 0.91 2/56 16891
Raw data (stat): 16889 (minisat+) R 16888 12452 12451 0 -1 0 3039 0 0 0 8988 11 0 0 25 0 1 0 364754591 14602240 3011 4294967295 134512640 134672761 3221224560 3221223732 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3565 3011 603 41 0 3524 0
vsize: 14260
[startup+100.005 s]
Raw data (loadavg): 0.98 0.97 0.91 2/56 16891
Raw data (stat): 16889 (minisat+) R 16888 12452 12451 0 -1 0 3134 0 0 0 9988 12 0 0 25 0 1 0 364754591 14872576 3106 4294967295 134512640 134672761 3221224560 3221223732 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3631 3106 603 41 0 3590 0
vsize: 14524
[startup+110.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16891
Raw data (stat): 16889 (minisat+) R 16888 12452 12451 0 -1 0 3258 0 0 0 10988 13 0 0 25 0 1 0 364754591 15413248 3230 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3763 3230 603 41 0 3722 0
vsize: 15052
[startup+120.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16891
Raw data (stat): 16889 (minisat+) R 16888 12452 12451 0 -1 0 3399 0 0 0 11987 13 0 0 25 0 1 0 364754591 16068608 3371 4294967295 134512640 134672761 3221224560 3221223728 134561400 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3923 3371 603 41 0 3882 0
vsize: 15692
[startup+130.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16891
Raw data (stat): 16889 (minisat+) R 16888 12452 12451 0 -1 0 3585 0 0 0 12987 14 0 0 25 0 1 0 364754591 16871424 3557 4294967295 134512640 134672761 3221224560 3221223684 134566034 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4119 3557 603 41 0 4078 0
vsize: 16476
[startup+140.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16891
Raw data (stat): 16889 (minisat+) R 16888 12452 12451 0 -1 0 3730 0 0 0 13987 14 0 0 25 0 1 0 364754591 17412096 3702 4294967295 134512640 134672761 3221224560 3221223732 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4251 3702 603 41 0 4210 0
vsize: 17004
[startup+150.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16891
Raw data (stat): 16889 (minisat+) R 16888 12452 12451 0 -1 0 4745 0 0 0 14984 17 0 0 25 0 1 0 364754591 21598208 4717 4294967295 134512640 134672761 3221224560 3221223732 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5273 4717 603 41 0 5232 0
vsize: 21092
[startup+160.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16891
Raw data (stat): 16889 (minisat+) R 16888 12452 12451 0 -1 0 5003 0 0 0 15983 18 0 0 25 0 1 0 364754591 22679552 4975 4294967295 134512640 134672761 3221224560 3221223732 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5537 4975 603 41 0 5496 0
vsize: 22148
[startup+170.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16891
Raw data (stat): 16889 (minisat+) R 16888 12452 12451 0 -1 0 5202 0 0 0 16983 18 0 0 25 0 1 0 364754591 23347200 5174 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5700 5174 603 41 0 5659 0
vsize: 22800
[startup+180.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16891
Raw data (stat): 16889 (minisat+) R 16888 12452 12451 0 -1 0 5637 0 0 0 17981 20 0 0 25 0 1 0 364754591 25493504 5609 4294967295 134512640 134672761 3221224560 3221223728 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6224 5609 603 41 0 6183 0
vsize: 24896
[startup+190.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16891
Raw data (stat): 16889 (minisat+) R 16888 12452 12451 0 -1 0 6680 0 0 0 18978 23 0 0 25 0 1 0 364754591 29667328 6652 4294967295 134512640 134672761 3221224560 3221223728 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7243 6652 603 41 0 7202 0
vsize: 28972
[startup+200.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16891
Raw data (stat): 16889 (minisat+) R 16888 12452 12451 0 -1 0 7373 0 0 0 19976 25 0 0 25 0 1 0 364754591 32485376 7345 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7931 7345 603 41 0 7890 0
vsize: 31724
[startup+210.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16891
Raw data (stat): 16889 (minisat+) R 16888 12452 12451 0 -1 0 8030 0 0 0 20975 27 0 0 25 0 1 0 364754591 35160064 8002 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8584 8002 603 41 0 8543 0
vsize: 34336
[startup+220.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16891
Raw data (stat): 16889 (minisat+) R 16888 12452 12451 0 -1 0 8788 0 0 0 21972 30 0 0 25 0 1 0 364754591 38240256 8760 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9336 8760 603 41 0 9295 0
vsize: 37344
[startup+230.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16891
Raw data (stat): 16889 (minisat+) R 16888 12452 12451 0 -1 0 9311 0 0 0 22971 31 0 0 25 0 1 0 364754591 40378368 9283 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9858 9283 603 41 0 9817 0
vsize: 39432
[startup+240.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16891
Raw data (stat): 16889 (minisat+) R 16888 12452 12451 0 -1 0 9808 0 0 0 23969 33 0 0 25 0 1 0 364754591 42409984 9780 4294967295 134512640 134672761 3221224560 3221223728 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10354 9780 603 41 0 10313 0
vsize: 41416
[startup+250.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16891
Raw data (stat): 16889 (minisat+) R 16888 12452 12451 0 -1 0 10347 0 0 0 24967 35 0 0 25 0 1 0 364754591 44683264 10319 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10909 10319 603 41 0 10868 0
vsize: 43636
[startup+260.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16891
Raw data (stat): 16889 (minisat+) R 16888 12452 12451 0 -1 0 10837 0 0 0 25966 36 0 0 25 0 1 0 364754591 46592000 10809 4294967295 134512640 134672761 3221224560 3221223728 134561005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11375 10809 603 41 0 11334 0
vsize: 45500
[startup+270.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16891
Raw data (stat): 16889 (minisat+) R 16888 12452 12451 0 -1 0 11287 0 0 0 26965 38 0 0 25 0 1 0 364754591 48476160 11259 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11835 11259 603 41 0 11794 0
vsize: 47340
[startup+280.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16891
Raw data (stat): 16889 (minisat+) R 16888 12452 12451 0 -1 0 11751 0 0 0 27963 39 0 0 25 0 1 0 364754591 50368512 11723 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12297 11723 603 41 0 12256 0
vsize: 49188
[startup+290.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16891
Raw data (stat): 16889 (minisat+) R 16888 12452 12451 0 -1 0 12144 0 0 0 28962 41 0 0 25 0 1 0 364754591 51970048 12116 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12688 12116 603 41 0 12647 0
vsize: 50752
[startup+300.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16891
Raw data (stat): 16889 (minisat+) R 16888 12452 12451 0 -1 0 12503 0 0 0 29960 43 0 0 25 0 1 0 364754591 53456896 12475 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13051 12475 603 41 0 13010 0
vsize: 52204
[startup+310.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16891
Raw data (stat): 16889 (minisat+) R 16888 12452 12451 0 -1 0 12868 0 0 0 30959 44 0 0 25 0 1 0 364754591 54931456 12840 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13411 12840 603 41 0 13370 0
vsize: 53644
[startup+320.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16891
Raw data (stat): 16889 (minisat+) R 16888 12452 12451 0 -1 0 13254 0 0 0 31958 46 0 0 25 0 1 0 364754591 56516608 13226 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13798 13226 603 41 0 13757 0
vsize: 55192
[startup+330.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16891
Raw data (stat): 16889 (minisat+) R 16888 12452 12451 0 -1 0 13673 0 0 0 32956 47 0 0 25 0 1 0 364754591 58245120 13645 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14220 13645 603 41 0 14179 0
vsize: 56880
[startup+340.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16891
Raw data (stat): 16889 (minisat+) R 16888 12452 12451 0 -1 0 14075 0 0 0 33956 48 0 0 25 0 1 0 364754591 60534784 14047 4294967295 134512640 134672761 3221224560 3221223728 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14779 14047 603 41 0 14738 0
vsize: 59116
[startup+350.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16891
Raw data (stat): 16889 (minisat+) R 16888 12452 12451 0 -1 0 14407 0 0 0 34955 49 0 0 25 0 1 0 364754591 61886464 14379 4294967295 134512640 134672761 3221224560 3221223732 134556667 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15109 14379 603 41 0 15068 0
vsize: 60436
[startup+360.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16891
Raw data (stat): 16889 (minisat+) R 16888 12452 12451 0 -1 0 14709 0 0 0 35954 50 0 0 25 0 1 0 364754591 63082496 14681 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15401 14681 603 41 0 15360 0
vsize: 61604
[startup+370.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16891
Raw data (stat): 16889 (minisat+) R 16888 12452 12451 0 -1 0 15084 0 0 0 36953 51 0 0 25 0 1 0 364754591 64675840 15056 4294967295 134512640 134672761 3221224560 3221223728 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15790 15056 603 41 0 15749 0
vsize: 63160
[startup+380.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16891
Raw data (stat): 16889 (minisat+) R 16888 12452 12451 0 -1 0 15484 0 0 0 37952 53 0 0 25 0 1 0 364754591 66281472 15456 4294967295 134512640 134672761 3221224560 3221223728 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16182 15456 603 41 0 16141 0
vsize: 64728
[startup+390.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16893
Raw data (stat): 16889 (minisat+) R 16888 12452 12451 0 -1 0 15865 0 0 0 38950 55 0 0 25 0 1 0 364754591 67874816 15837 4294967295 134512640 134672761 3221224560 3221223728 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16571 15837 603 41 0 16530 0
vsize: 66284
[startup+400.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16893
Raw data (stat): 16889 (minisat+) R 16888 12452 12451 0 -1 0 16231 0 0 0 39949 56 0 0 25 0 1 0 364754591 69345280 16203 4294967295 134512640 134672761 3221224560 3221223728 134560852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16930 16203 603 41 0 16889 0
vsize: 67720
[startup+410.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16893
Raw data (stat): 16889 (minisat+) R 16888 12452 12451 0 -1 0 16566 0 0 0 40948 57 0 0 25 0 1 0 364754591 70684672 16538 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17257 16538 603 41 0 17216 0
vsize: 69028
[startup+420.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16893
Raw data (stat): 16889 (minisat+) R 16888 12452 12451 0 -1 0 16858 0 0 0 41948 57 0 0 25 0 1 0 364754591 71876608 16830 4294967295 134512640 134672761 3221224560 3221223744 134559373 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17548 16830 603 41 0 17507 0
vsize: 70192
[startup+430.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16893
Raw data (stat): 16889 (minisat+) R 16888 12452 12451 0 -1 0 17150 0 0 0 42946 59 0 0 25 0 1 0 364754591 73072640 17122 4294967295 134512640 134672761 3221224560 3221223728 134561154 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17840 17122 603 41 0 17799 0
vsize: 71360
[startup+440.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16893
Raw data (stat): 16889 (minisat+) R 16888 12452 12451 0 -1 0 17454 0 0 0 43945 60 0 0 25 0 1 0 364754591 74285056 17426 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18136 17426 603 41 0 18095 0
vsize: 72544
[startup+450.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16893
Raw data (stat): 16889 (minisat+) R 16888 12452 12451 0 -1 0 17750 0 0 0 44944 61 0 0 25 0 1 0 364754591 75489280 17722 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18430 17722 603 41 0 18389 0
vsize: 73720
[startup+460.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16893
Raw data (stat): 16889 (minisat+) R 16888 12452 12451 0 -1 0 18028 0 0 0 45943 63 0 0 25 0 1 0 364754591 76681216 18000 4294967295 134512640 134672761 3221224560 3221223728 134561145 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18721 18000 603 41 0 18680 0
vsize: 74884
[startup+470.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16893
Raw data (stat): 16889 (minisat+) R 16888 12452 12451 0 -1 0 18251 0 0 0 46943 63 0 0 25 0 1 0 364754591 77651968 18223 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18958 18223 603 41 0 18917 0
vsize: 75832
[startup+480.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16893
Raw data (stat): 16889 (minisat+) R 16888 12452 12451 0 -1 0 18481 0 0 0 47942 64 0 0 25 0 1 0 364754591 78589952 18453 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19187 18453 603 41 0 19146 0
vsize: 76748
[startup+490.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16893
Raw data (stat): 16889 (minisat+) R 16888 12452 12451 0 -1 0 18735 0 0 0 48941 65 0 0 25 0 1 0 364754591 79527936 18707 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19416 18707 603 41 0 19375 0
vsize: 77664
[startup+500.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16893
Raw data (stat): 16889 (minisat+) R 16888 12452 12451 0 -1 0 18939 0 0 0 49941 66 0 0 25 0 1 0 364754591 80375808 18911 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19623 18911 603 41 0 19582 0
vsize: 78492
[startup+510.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16893
Raw data (stat): 16889 (minisat+) R 16888 12452 12451 0 -1 0 19190 0 0 0 50939 67 0 0 25 0 1 0 364754591 81448960 19162 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19885 19162 603 41 0 19844 0
vsize: 79540
[startup+520.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16893
Raw data (stat): 16889 (minisat+) R 16888 12452 12451 0 -1 0 19450 0 0 0 51938 68 0 0 25 0 1 0 364754591 82518016 19422 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20146 19422 603 41 0 20105 0
vsize: 80584
[startup+530.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16893
Raw data (stat): 16889 (minisat+) R 16888 12452 12451 0 -1 0 19712 0 0 0 52938 69 0 0 25 0 1 0 364754591 83587072 19684 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20407 19684 603 41 0 20366 0
vsize: 81628
[startup+540.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16893
Raw data (stat): 16889 (minisat+) R 16888 12452 12451 0 -1 0 20035 0 0 0 53937 70 0 0 25 0 1 0 364754591 84918272 20007 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20732 20007 603 41 0 20691 0
vsize: 82928
[startup+550.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16893
Raw data (stat): 16889 (minisat+) R 16888 12452 12451 0 -1 0 20329 0 0 0 54936 71 0 0 25 0 1 0 364754591 86114304 20301 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21024 20301 603 41 0 20983 0
vsize: 84096
[startup+560.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16893
Raw data (stat): 16889 (minisat+) R 16888 12452 12451 0 -1 0 20663 0 0 0 55935 72 0 0 25 0 1 0 364754591 87437312 20635 4294967295 134512640 134672761 3221224560 3221223728 134561133 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21347 20635 603 41 0 21306 0
vsize: 85388
[startup+570.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16893
Raw data (stat): 16889 (minisat+) R 16888 12452 12451 0 -1 0 20725 0 0 0 56935 73 0 0 25 0 1 0 364754591 87703552 20697 4294967295 134512640 134672761 3221224560 3221223744 134559498 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21412 20697 603 41 0 21371 0
vsize: 85648
[startup+580.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16893
Raw data (stat): 16889 (minisat+) R 16888 12452 12451 0 -1 0 20725 0 0 0 57935 73 0 0 25 0 1 0 364754591 87703552 20697 4294967295 134512640 134672761 3221224560 3221223728 134561139 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21412 20697 603 41 0 21371 0
vsize: 85648
[startup+590.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16893
Raw data (stat): 16889 (minisat+) R 16888 12452 12451 0 -1 0 20728 0 0 0 58935 73 0 0 25 0 1 0 364754591 87703552 20700 4294967295 134512640 134672761 3221224560 3221223728 134561145 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21412 20700 603 41 0 21371 0
vsize: 85648
[startup+600.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16893
Raw data (stat): 16889 (minisat+) R 16888 12452 12451 0 -1 0 20728 0 0 0 59935 73 0 0 25 0 1 0 364754591 87703552 20700 4294967295 134512640 134672761 3221224560 3221223728 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21412 20700 603 41 0 21371 0
vsize: 85648
[startup+610.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16893
Raw data (stat): 16889 (minisat+) R 16888 12452 12451 0 -1 0 20728 0 0 0 60935 73 0 0 25 0 1 0 364754591 87703552 20700 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21412 20700 603 41 0 21371 0
vsize: 85648
[startup+620.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16893
Raw data (stat): 16889 (minisat+) R 16888 12452 12451 0 -1 0 20728 0 0 0 61935 73 0 0 25 0 1 0 364754591 87703552 20700 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21412 20700 603 41 0 21371 0
vsize: 85648
[startup+630.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16893
Raw data (stat): 16889 (minisat+) R 16888 12452 12451 0 -1 0 20728 0 0 0 62935 73 0 0 25 0 1 0 364754591 87703552 20700 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21412 20700 603 41 0 21371 0
vsize: 85648
[startup+640.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16893
Raw data (stat): 16889 (minisat+) R 16888 12452 12451 0 -1 0 20730 0 0 0 63935 73 0 0 25 0 1 0 364754591 87703552 20702 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21412 20702 603 41 0 21371 0
vsize: 85648
[startup+650.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16893
Raw data (stat): 16889 (minisat+) R 16888 12452 12451 0 -1 0 20730 0 0 0 64935 73 0 0 25 0 1 0 364754591 87703552 20702 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21412 20702 603 41 0 21371 0
vsize: 85648
[startup+660.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16893
Raw data (stat): 16889 (minisat+) R 16888 12452 12451 0 -1 0 20731 0 0 0 65935 73 0 0 25 0 1 0 364754591 87703552 20703 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21412 20703 603 41 0 21371 0
vsize: 85648
[startup+670.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16893
Raw data (stat): 16889 (minisat+) R 16888 12452 12451 0 -1 0 20732 0 0 0 66935 74 0 0 25 0 1 0 364754591 87703552 20704 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21412 20704 603 41 0 21371 0
vsize: 85648
[startup+680.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16893
Raw data (stat): 16889 (minisat+) R 16888 12452 12451 0 -1 0 20732 0 0 0 67935 74 0 0 25 0 1 0 364754591 87703552 20704 4294967295 134512640 134672761 3221224560 3221223728 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21412 20704 603 41 0 21371 0
vsize: 85648
[startup+690.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16895
Raw data (stat): 16889 (minisat+) R 16888 12452 12451 0 -1 0 20732 0 0 0 68936 74 0 0 25 0 1 0 364754591 87703552 20704 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21412 20704 603 41 0 21371 0
vsize: 85648
[startup+700.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16895
Raw data (stat): 16889 (minisat+) R 16888 12452 12451 0 -1 0 20732 0 0 0 69936 74 0 0 25 0 1 0 364754591 87703552 20704 4294967295 134512640 134672761 3221224560 3221223728 134560912 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21412 20704 603 41 0 21371 0
vsize: 85648
[startup+710.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16895
Raw data (stat): 16889 (minisat+) R 16888 12452 12451 0 -1 0 20733 0 0 0 70936 74 0 0 25 0 1 0 364754591 87703552 20705 4294967295 134512640 134672761 3221224560 3221223728 134561154 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21412 20705 603 41 0 21371 0
vsize: 85648
[startup+720.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16895
Raw data (stat): 16889 (minisat+) R 16888 12452 12451 0 -1 0 20733 0 0 0 71936 74 0 0 25 0 1 0 364754591 87703552 20705 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21412 20705 603 41 0 21371 0
vsize: 85648
[startup+730.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16895
Raw data (stat): 16889 (minisat+) R 16888 12452 12451 0 -1 0 20734 0 0 0 72936 74 0 0 25 0 1 0 364754591 87703552 20706 4294967295 134512640 134672761 3221224560 3221223744 134559405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21412 20706 603 41 0 21371 0
vsize: 85648
[startup+740.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16895
Raw data (stat): 16889 (minisat+) R 16888 12452 12451 0 -1 0 20734 0 0 0 73936 74 0 0 25 0 1 0 364754591 87703552 20706 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21412 20706 603 41 0 21371 0
vsize: 85648
[startup+750.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16895
Raw data (stat): 16889 (minisat+) R 16888 12452 12451 0 -1 0 20734 0 0 0 74937 74 0 0 25 0 1 0 364754591 87703552 20706 4294967295 134512640 134672761 3221224560 3221223728 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21412 20706 603 41 0 21371 0
vsize: 85648
[startup+760.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16895
Raw data (stat): 16889 (minisat+) R 16888 12452 12451 0 -1 0 20734 0 0 0 75937 74 0 0 25 0 1 0 364754591 87703552 20706 4294967295 134512640 134672761 3221224560 3221223728 134561118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21412 20706 603 41 0 21371 0
vsize: 85648
[startup+770.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16895
Raw data (stat): 16889 (minisat+) R 16888 12452 12451 0 -1 0 20734 0 0 0 76937 74 0 0 25 0 1 0 364754591 87703552 20706 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21412 20706 603 41 0 21371 0
vsize: 85648
[startup+780.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16895
Raw data (stat): 16889 (minisat+) R 16888 12452 12451 0 -1 0 20734 0 0 0 77937 74 0 0 25 0 1 0 364754591 87703552 20706 4294967295 134512640 134672761 3221224560 3221223728 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21412 20706 603 41 0 21371 0
vsize: 85648
[startup+790.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16895
Raw data (stat): 16889 (minisat+) R 16888 12452 12451 0 -1 0 20734 0 0 0 78937 74 0 0 25 0 1 0 364754591 87703552 20706 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21412 20706 603 41 0 21371 0
vsize: 85648
[startup+800.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16895
Raw data (stat): 16889 (minisat+) R 16888 12452 12451 0 -1 0 20735 0 0 0 79937 74 0 0 25 0 1 0 364754591 87703552 20707 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21412 20707 603 41 0 21371 0
vsize: 85648
[startup+810.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16895
Raw data (stat): 16889 (minisat+) R 16888 12452 12451 0 -1 0 20737 0 0 0 80937 74 0 0 25 0 1 0 364754591 87703552 20709 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21412 20709 603 41 0 21371 0
vsize: 85648
[startup+820.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16895
Raw data (stat): 16889 (minisat+) R 16888 12452 12451 0 -1 0 20737 0 0 0 81938 74 0 0 25 0 1 0 364754591 87703552 20709 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21412 20709 603 41 0 21371 0
vsize: 85648
[startup+830.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16895
Raw data (stat): 16889 (minisat+) R 16888 12452 12451 0 -1 0 20737 0 0 0 82938 74 0 0 25 0 1 0 364754591 87703552 20709 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21412 20709 603 41 0 21371 0
vsize: 85648
[startup+840.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16895
Raw data (stat): 16889 (minisat+) R 16888 12452 12451 0 -1 0 20743 0 0 0 83938 74 0 0 25 0 1 0 364754591 87703552 20715 4294967295 134512640 134672761 3221224560 3221223728 134560895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21412 20715 603 41 0 21371 0
vsize: 85648
[startup+850.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16895
Raw data (stat): 16889 (minisat+) R 16888 12452 12451 0 -1 0 20743 0 0 0 84938 74 0 0 25 0 1 0 364754591 87703552 20715 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21412 20715 603 41 0 21371 0
vsize: 85648
[startup+860.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16895
Raw data (stat): 16889 (minisat+) R 16888 12452 12451 0 -1 0 20743 0 0 0 85938 74 0 0 25 0 1 0 364754591 87703552 20715 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21412 20715 603 41 0 21371 0
vsize: 85648
[startup+870.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16895
Raw data (stat): 16889 (minisat+) R 16888 12452 12451 0 -1 0 20743 0 0 0 86939 74 0 0 25 0 1 0 364754591 87703552 20715 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21412 20715 603 41 0 21371 0
vsize: 85648
[startup+880.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16895
Raw data (stat): 16889 (minisat+) R 16888 12452 12451 0 -1 0 20743 0 0 0 87939 74 0 0 25 0 1 0 364754591 87703552 20715 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21412 20715 603 41 0 21371 0
vsize: 85648
[startup+890.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16895
Raw data (stat): 16889 (minisat+) R 16888 12452 12451 0 -1 0 20743 0 0 0 88939 74 0 0 25 0 1 0 364754591 87703552 20715 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21412 20715 603 41 0 21371 0
vsize: 85648
[startup+900.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16895
Raw data (stat): 16889 (minisat+) R 16888 12452 12451 0 -1 0 20743 0 0 0 89939 74 0 0 25 0 1 0 364754591 87703552 20715 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21412 20715 603 41 0 21371 0
vsize: 85648
[startup+910.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16895
Raw data (stat): 16889 (minisat+) R 16888 12452 12451 0 -1 0 20747 0 0 0 90939 74 0 0 25 0 1 0 364754591 87703552 20719 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21412 20719 603 41 0 21371 0
vsize: 85648
[startup+920.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16895
Raw data (stat): 16889 (minisat+) R 16888 12452 12451 0 -1 0 20747 0 0 0 91940 74 0 0 25 0 1 0 364754591 87703552 20719 4294967295 134512640 134672761 3221224560 3221223728 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21412 20719 603 41 0 21371 0
vsize: 85648
[startup+930.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16895
Raw data (stat): 16889 (minisat+) R 16888 12452 12451 0 -1 0 20747 0 0 0 92940 74 0 0 25 0 1 0 364754591 87703552 20719 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21412 20719 603 41 0 21371 0
vsize: 85648
[startup+940.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16895
Raw data (stat): 16889 (minisat+) R 16888 12452 12451 0 -1 0 20747 0 0 0 93940 74 0 0 25 0 1 0 364754591 87703552 20719 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21412 20719 603 41 0 21371 0
vsize: 85648
[startup+950.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16895
Raw data (stat): 16889 (minisat+) R 16888 12452 12451 0 -1 0 20747 0 0 0 94940 74 0 0 25 0 1 0 364754591 87703552 20719 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21412 20719 603 41 0 21371 0
vsize: 85648
[startup+960.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16895
Raw data (stat): 16889 (minisat+) R 16888 12452 12451 0 -1 0 20876 0 0 0 95940 74 0 0 25 0 1 0 364754591 88240128 20848 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21543 20848 603 41 0 21502 0
vsize: 86172
[startup+970.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16895
Raw data (stat): 16889 (minisat+) R 16888 12452 12451 0 -1 0 21077 0 0 0 96939 75 0 0 25 0 1 0 364754591 89034752 21049 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21737 21049 603 41 0 21696 0
vsize: 86948
[startup+980.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16895
Raw data (stat): 16889 (minisat+) R 16888 12452 12451 0 -1 0 21257 0 0 0 97938 76 0 0 25 0 1 0 364754591 89833472 21229 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21932 21229 603 41 0 21891 0
vsize: 87728
[startup+990.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16897
Raw data (stat): 16889 (minisat+) R 16888 12452 12451 0 -1 0 21437 0 0 0 98938 77 0 0 25 0 1 0 364754591 90628096 21409 4294967295 134512640 134672761 3221224560 3221223728 134561375 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22126 21409 603 41 0 22085 0
vsize: 88504
[startup+1000.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16897
Raw data (stat): 16889 (minisat+) R 16888 12452 12451 0 -1 0 21632 0 0 0 99938 77 0 0 25 0 1 0 364754591 91422720 21604 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22320 21604 603 41 0 22279 0
vsize: 89280
[startup+1010.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16897
Raw data (stat): 16889 (minisat+) R 16888 12452 12451 0 -1 0 21875 0 0 0 100937 78 0 0 25 0 1 0 364754591 92487680 21847 4294967295 134512640 134672761 3221224560 3221223728 134561115 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22580 21847 603 41 0 22539 0
vsize: 90320
[startup+1020.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16897
Raw data (stat): 16889 (minisat+) R 16888 12452 12451 0 -1 0 22088 0 0 0 101937 78 0 0 25 0 1 0 364754591 93454336 22060 4294967295 134512640 134672761 3221224560 3221223728 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22816 22060 603 41 0 22775 0
vsize: 91264
[startup+1030.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16897
Raw data (stat): 16889 (minisat+) R 16888 12452 12451 0 -1 0 22313 0 0 0 102936 79 0 0 25 0 1 0 364754591 94257152 22285 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23012 22285 603 41 0 22971 0
vsize: 92048
[startup+1040.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16897
Raw data (stat): 16889 (minisat+) R 16888 12452 12451 0 -1 0 22547 0 0 0 103936 80 0 0 25 0 1 0 364754591 95342592 22519 4294967295 134512640 134672761 3221224560 3221223728 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23277 22519 603 41 0 23236 0
vsize: 93108
[startup+1050.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16897
Raw data (stat): 16889 (minisat+) R 16888 12452 12451 0 -1 0 22779 0 0 0 104936 80 0 0 25 0 1 0 364754591 96305152 22751 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23512 22751 603 41 0 23471 0
vsize: 94048
[startup+1060.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16897
Raw data (stat): 16889 (minisat+) R 16888 12452 12451 0 -1 0 22967 0 0 0 105935 81 0 0 25 0 1 0 364754591 97222656 22939 4294967295 134512640 134672761 3221224560 3221223728 134561375 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23736 22939 603 41 0 23695 0
vsize: 94944
[startup+1070.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16897
Raw data (stat): 16889 (minisat+) R 16888 12452 12451 0 -1 0 23135 0 0 0 106935 81 0 0 25 0 1 0 364754591 97886208 23107 4294967295 134512640 134672761 3221224560 3221223728 134561205 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23898 23107 603 41 0 23857 0
vsize: 95592
[startup+1080.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16897
Raw data (stat): 16889 (minisat+) R 16888 12452 12451 0 -1 0 23344 0 0 0 107934 82 0 0 25 0 1 0 364754591 98799616 23316 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24121 23316 603 41 0 24080 0
vsize: 96484
[startup+1090.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16897
Raw data (stat): 16889 (minisat+) R 16888 12452 12451 0 -1 0 23534 0 0 0 108934 83 0 0 25 0 1 0 364754591 99590144 23506 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24314 23506 603 41 0 24273 0
vsize: 97256
[startup+1100.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16897
Raw data (stat): 16889 (minisat+) R 16888 12452 12451 0 -1 0 23754 0 0 0 109933 84 0 0 25 0 1 0 364754591 100515840 23726 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24540 23726 603 41 0 24499 0
vsize: 98160
[startup+1110.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16897
Raw data (stat): 16889 (minisat+) R 16888 12452 12451 0 -1 0 23949 0 0 0 110933 84 0 0 25 0 1 0 364754591 101306368 23921 4294967295 134512640 134672761 3221224560 3221223728 134561145 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24733 23921 603 41 0 24692 0
vsize: 98932
[startup+1120.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16897
Raw data (stat): 16889 (minisat+) R 16888 12452 12451 0 -1 0 24168 0 0 0 111932 85 0 0 25 0 1 0 364754591 102236160 24140 4294967295 134512640 134672761 3221224560 3221223664 134560418 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24960 24140 603 41 0 24919 0
vsize: 99840
[startup+1130.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16897
Raw data (stat): 16889 (minisat+) R 16888 12452 12451 0 -1 0 24388 0 0 0 112932 86 0 0 25 0 1 0 364754591 103157760 24360 4294967295 134512640 134672761 3221224560 3221223728 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25185 24360 603 41 0 25144 0
vsize: 100740
[startup+1140.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16897
Raw data (stat): 16889 (minisat+) R 16888 12452 12451 0 -1 0 24613 0 0 0 113931 86 0 0 25 0 1 0 364754591 104275968 24585 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25458 24585 603 41 0 25417 0
vsize: 101832
[startup+1150.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16897
Raw data (stat): 16889 (minisat+) R 16888 12452 12451 0 -1 0 24810 0 0 0 114931 87 0 0 25 0 1 0 364754591 105066496 24782 4294967295 134512640 134672761 3221224560 3221223728 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25651 24782 603 41 0 25610 0
vsize: 102604
[startup+1160.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16897
Raw data (stat): 16889 (minisat+) R 16888 12452 12451 0 -1 0 25014 0 0 0 115930 88 0 0 25 0 1 0 364754591 105857024 24986 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25844 24986 603 41 0 25803 0
vsize: 103376
[startup+1170.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16897
Raw data (stat): 16889 (minisat+) R 16888 12452 12451 0 -1 0 25220 0 0 0 116930 88 0 0 25 0 1 0 364754591 106688512 25192 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26047 25192 603 41 0 26006 0
vsize: 104188
[startup+1180.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16897
Raw data (stat): 16889 (minisat+) R 16888 12452 12451 0 -1 0 25418 0 0 0 117930 89 0 0 25 0 1 0 364754591 107479040 25390 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26240 25390 603 41 0 26199 0
vsize: 104960
[startup+1190.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16897
Raw data (stat): 16889 (minisat+) R 16888 12452 12451 0 -1 0 25627 0 0 0 118929 89 0 0 25 0 1 0 364754591 108408832 25599 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26467 25599 603 41 0 26426 0
vsize: 105868
[startup+1200.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16897
Raw data (stat): 16889 (minisat+) R 16888 12452 12451 0 -1 0 25850 0 0 0 119929 90 0 0 25 0 1 0 364754591 109338624 25822 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26694 25822 603 41 0 26653 0
vsize: 106776
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.08 s]
Raw data (loadavg): 0.99 0.97 0.91 1/56 16897
Raw data (stat): 16889 (minisat+) Z 16888 12452 12451 0 -1 12 25852 0 0 0 119929 95 0 0 25 0 1 0 364754591 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 0
Real time (s): 1200.08
CPU time (s): 1200.24
CPU user time (s): 1199.29
CPU system time (s): 0.950855
CPU usage (%): 100.014
Max. virtual memory (Kb): 106776
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####