PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/web/www.ps.uni-sb.de/~walser/benchmarks/course-ass/normalized-ss97-2.opb
MD5SUM	5e8935802e4aa1a1ac8f2a923d842947
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	22547
Optimality of the best value was proved	NO
Number of terms in the objective function	6892
Biggest coefficient in the objective function	667
Number of bits for the biggest coefficient in the objective function	10
Sum of the numbers in the objective function	371779
Number of bits of the sum of numbers in the objective function	19
Biggest number in a constraint	667
Number of bits of the biggest number in a constraint	10
Biggest sum of numbers in a constraint	371779
Number of bits of the biggest sum of numbers	19
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1175.07
Number of variables	8405
Total number of constraints	19071
Number of constraints which are clauses	9918
Number of constraints which are cardinality constraints (but not clauses)	9153
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	1
Maximum length of a constraint	351
Trace number 5275

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc9 THE 2005-04-13 23:12:07 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3738 boxname=wulflinc9 idbench=354 idsolver=10 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  5e8935802e4aa1a1ac8f2a923d842947  /oldhome/oroussel/tmp/wulflinc9/normalized-ss97-2.opb
REAL COMMAND:  minisat+ -ca /oldhome/oroussel/tmp/wulflinc9/normalized-ss97-2.opb /oldhome/oroussel/tmp/wulflinc9/normalized-ss97-2.opb
IDLAUNCH: 3738
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.242
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.242
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:        907080 kB
Buffers:         34420 kB
Cached:          73068 kB
SwapCached:        564 kB
Active:          52544 kB
Inactive:        58356 kB
HighTotal:      131008 kB
HighFree:        53984 kB
LowTotal:       903652 kB
LowFree:        853096 kB
SwapTotal:     2097136 kB
SwapFree:      2096572 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6928 kB
Slab:            11132 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-13 23:32:09 (client local time) WITH STATUS 0 IN 1200.29 SECONDS
stats: 3738 7 1200.29 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 11366 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ############################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################
c   -- Clauses(.)/Splits(s): ..............................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ---[11365]---> Adder-cost: 686   maxlim: 311   bits: 9/9
c ---[11364]---> Adder-cost: 686   maxlim: 311   bits: 9/9
c ---[11363]---> Adder-cost: 686   maxlim: 311   bits: 9/9
c ---[11362]---> Adder-cost: 686   maxlim: 311   bits: 9/9
c ---[11361]---> Adder-cost: 686   maxlim: 311   bits: 9/9
c ---[11360]---> Adder-cost: 686   maxlim: 311   bits: 9/9
c ---[11359]---> Adder-cost: 686   maxlim: 311   bits: 9/9
c ---[11358]---> Adder-cost: 686   maxlim: 311   bits: 9/9
c ---[11357]---> Adder-cost: 686   maxlim: 311   bits: 9/9
c ---[11356]---> Adder-cost: 686   maxlim: 311   bits: 9/9
c ---[11355]---> Adder-cost: 688   maxlim: 321   bits: 9/9
c ---[11354]---> Adder-cost: 688   maxlim: 321   bits: 9/9
c ---[11353]---> Adder-cost: 688   maxlim: 321   bits: 9/9
c ---[11352]---> Adder-cost: 688   maxlim: 321   bits: 9/9
c ---[11351]---> Adder-cost: 688   maxlim: 321   bits: 9/9
c ---[11350]---> Adder-cost: 688   maxlim: 321   bits: 9/9
c ---[11349]---> Adder-cost: 688   maxlim: 321   bits: 9/9
c ---[11348]---> Adder-cost: 688   maxlim: 321   bits: 9/9
c ---[11347]---> Adder-cost: 688   maxlim: 321   bits: 9/9
c ---[11346]---> Adder-cost: 688   maxlim: 321   bits: 9/9
c ---[11345]---> Adder-cost: 688   maxlim: 321   bits: 9/9
c ---[11344]---> Adder-cost: 688   maxlim: 321   bits: 9/9
c ---[11343]---> Adder-cost: 688   maxlim: 321   bits: 9/9
c ---[11342]---> Adder-cost: 688   maxlim: 321   bits: 9/9
c ---[11341]---> Adder-cost: 46   maxlim: 26   bits: 6/5
c ---[11340]---> Adder-cost: 46   maxlim: 26   bits: 6/5
c ---[11339]---> Adder-cost: 46   maxlim: 26   bits: 6/5
c ---[11338]---> Adder-cost: 46   maxlim: 26   bits: 6/5
c ---[11337]---> Adder-cost: 46   maxlim: 26   bits: 6/5
c ---[11336]---> Adder-cost: 46   maxlim: 26   bits: 6/5
c ---[11335]---> Adder-cost: 46   maxlim: 26   bits: 6/5
c ---[11334]---> Adder-cost: 46   maxlim: 26   bits: 6/5
c ---[11333]---> Adder-cost: 46   maxlim: 26   bits: 6/5
c ---[11332]---> Adder-cost: 46   maxlim: 26   bits: 6/5
c ---[11331]---> Adder-cost: 9   maxlim: 21   bits: 6/5
c ---[11330]---> Adder-cost: 9   maxlim: 21   bits: 6/5
c ---[11329]---> Adder-cost: 9   maxlim: 21   bits: 6/5
c ---[11328]---> Adder-cost: 9   maxlim: 21   bits: 6/5
c ---[11327]---> Adder-cost: 9   maxlim: 21   bits: 6/5
c ---[11326]---> Adder-cost: 9   maxlim: 21   bits: 6/5
c ---[11325]---> Adder-cost: 9   maxlim: 21   bits: 6/5
c ---[11324]---> Adder-cost: 9   maxlim: 21   bits: 6/5
c ---[11323]---> Adder-cost: 9   maxlim: 21   bits: 6/5
c ---[11322]---> Adder-cost: 9   maxlim: 21   bits: 6/5
c ---[11321]---> Adder-cost: 9   maxlim: 21   bits: 6/5
c ---[11320]---> Adder-cost: 9   maxlim: 21   bits: 6/5
c ---[11319]---> Adder-cost: 9   maxlim: 21   bits: 6/5
c ---[11318]---> Adder-cost: 9   maxlim: 21   bits: 6/5
c ---[11316]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[11314]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[11312]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[11310]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[11308]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[11306]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[11304]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[11302]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[11300]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[11298]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[11296]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[11294]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[11292]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[11290]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[11288]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[11286]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[11284]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[11282]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[11280]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[11278]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[11276]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[11274]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[11272]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[11270]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[11268]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[11266]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[11264]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[11262]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[11260]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[11258]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[11256]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[11254]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[11252]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[11250]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[11248]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[11246]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[11244]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[11242]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[11240]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[11238]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[11236]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[11234]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[11232]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[11230]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[11228]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[11226]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[11224]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[11222]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[11220]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[11218]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[11216]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[11214]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[11212]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[11210]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[11208]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[11206]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[11204]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[11202]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[11200]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[11198]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[11196]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[11194]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[11192]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[11190]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[11188]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[11186]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[11184]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[11182]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[11180]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[11178]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[11176]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[11174]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[11172]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[11170]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[11168]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[11166]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[11164]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[11162]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[11160]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[11158]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[11156]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[11154]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[11152]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[11150]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[11148]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[11146]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[11144]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[11142]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[11140]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[11138]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[11136]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[11134]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[11132]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[11130]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[11128]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[11126]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[11124]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[11122]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[11120]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[11118]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[11116]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[11114]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[11112]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[11110]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[11108]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[11106]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[11104]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[11102]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[11100]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[11098]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[11096]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[11094]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[11092]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[11090]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[11088]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[11086]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[11084]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[11082]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[11080]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[11078]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[11076]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[11074]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[11072]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[11070]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[11068]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[11066]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[11064]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[11062]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[11060]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[11058]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[11056]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[11054]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[11052]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[11050]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[11048]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[11046]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[11044]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[11042]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[11040]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[11038]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[11036]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[11034]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[11032]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[11030]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[11028]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[11026]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[11024]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[11022]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[11020]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[11018]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[11016]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[11014]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[11012]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[11010]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[11008]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[11006]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[11004]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[11002]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[11000]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10998]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10996]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10994]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10992]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10990]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10988]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10986]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10984]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10982]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10980]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10978]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10976]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10974]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10972]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10970]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10968]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10966]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10964]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10962]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10960]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10958]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10956]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10954]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10952]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10950]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10948]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10946]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10944]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10942]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10940]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10938]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10936]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10934]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10932]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10930]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10928]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10926]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10924]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10922]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10920]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10918]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10916]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10914]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10912]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10910]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10908]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10906]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10904]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10902]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10900]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10898]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10896]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10894]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10892]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10890]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10888]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10886]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10884]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10882]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10880]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10878]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10876]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10874]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10872]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10870]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10868]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10866]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10864]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10862]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10860]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10858]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10856]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10854]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10852]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10850]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10848]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10846]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10844]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10842]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10840]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10838]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10836]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10834]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10832]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10830]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10828]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10826]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10824]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10822]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10820]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10818]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10816]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10814]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10812]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10810]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10808]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10806]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10804]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10802]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10800]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10798]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10796]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10794]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10792]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10790]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10788]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10786]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10784]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10782]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10780]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10778]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10776]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10774]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10772]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10770]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10768]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10766]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10764]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10762]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10760]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10758]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10756]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10754]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10752]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10750]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10748]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10746]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10744]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10742]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10740]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10738]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10736]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10734]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10732]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10730]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10728]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10726]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10724]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10722]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10720]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10718]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10716]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10714]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10712]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10710]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10708]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10706]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10704]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10702]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10700]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10698]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10696]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10694]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10692]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10690]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10688]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10686]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10684]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10682]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10680]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10678]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10676]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10674]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10672]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10670]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10668]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10666]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10664]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10662]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10660]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10658]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10656]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10654]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10652]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10650]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10648]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10646]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10644]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10642]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10640]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10638]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10636]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10634]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10632]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10630]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10628]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10626]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10624]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10622]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10620]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10618]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10616]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10614]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10612]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10610]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10608]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10606]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10604]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10602]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10600]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10598]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10596]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10594]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10592]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10590]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10588]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10586]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10584]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10582]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10580]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10578]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10576]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10574]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10572]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10570]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10568]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10566]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10564]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10562]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10560]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10558]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10556]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10554]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10552]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10550]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10548]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10546]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10544]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10542]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10540]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10538]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10536]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10534]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10532]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10530]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10528]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10526]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10524]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10522]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10520]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10518]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10516]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10514]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10512]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10510]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10508]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10506]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10504]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10502]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10500]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10498]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10496]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10494]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10492]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10490]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10488]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10486]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10484]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10482]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10480]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10478]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10476]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10474]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10472]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10470]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10468]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10466]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10464]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10462]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10460]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10458]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10456]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10454]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10452]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10450]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10448]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10446]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10444]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10442]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10440]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10438]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10436]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10434]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10432]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10430]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10428]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10426]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10424]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10422]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10420]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10418]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10416]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10414]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10412]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10410]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10408]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10406]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10404]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10402]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10400]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10398]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10396]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10394]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10392]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10390]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10388]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10386]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10384]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10382]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10380]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10378]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10376]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10374]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10372]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10370]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10368]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10366]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10364]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10362]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10360]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10358]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10356]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10354]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10352]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10350]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10348]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10346]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10344]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10342]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10340]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10338]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10336]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10334]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10332]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10330]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10328]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10326]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10324]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10322]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10320]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10318]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10316]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10314]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10312]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10310]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10308]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10306]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10304]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10302]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10300]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10298]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10296]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10294]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10292]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10290]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10288]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10286]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10284]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10282]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10280]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10278]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10276]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10274]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10272]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10270]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10268]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10266]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10264]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10262]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10260]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10258]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10256]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10254]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10252]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10250]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10248]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10246]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10244]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10242]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10240]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10238]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10236]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10234]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10232]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10230]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10228]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10226]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10224]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10222]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10220]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10218]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10216]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10214]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10212]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10210]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10208]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10206]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10204]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10202]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10200]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10198]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10196]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10194]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10192]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10190]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10188]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10186]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10184]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10182]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10180]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10178]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10176]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10174]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10172]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10170]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10168]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10166]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10164]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10162]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10160]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10158]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10156]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10154]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10152]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10150]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10148]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10146]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10144]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10142]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10140]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10138]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10136]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10134]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10132]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10130]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10128]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10126]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10124]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10122]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10120]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10118]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10116]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10114]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10112]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10110]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10108]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10106]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10104]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10102]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10100]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10098]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10096]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10094]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10092]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10090]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10088]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10086]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10084]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10082]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10080]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10078]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10076]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10074]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10072]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10070]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10068]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10066]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10064]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10062]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10060]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10058]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10056]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10054]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10052]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10050]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10048]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10046]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10044]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10042]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10040]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10038]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10036]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10034]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10032]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10030]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10028]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10026]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10024]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10022]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10020]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10018]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10016]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10014]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10012]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10010]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10008]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10006]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10004]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[10002]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[10000]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[9998]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[9996]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[9994]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[9992]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[9990]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[9988]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[9986]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[9984]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[9982]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[9980]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[9978]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[9976]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[9974]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[9972]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[9970]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[9968]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[9966]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[9964]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[9962]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[9960]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[9958]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[9956]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[9954]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[9952]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[9950]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[9948]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[9946]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[9944]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[9942]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[9940]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[9938]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[9936]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[9934]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[9932]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[9930]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[9928]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[9926]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[9924]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[9922]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[9920]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[9918]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  201333   700273 |   67111       0        0     nan |  0.000 % |
c |       101 |  201167   699721 |   73822      85      254     3.0 | 14.405 % |
c |       251 |  200858   698698 |   81204     201      664     3.3 | 14.537 % |
c |       477 |  200523   697591 |   89324     389     1267     3.3 | 14.686 % |
c |       814 |  199949   695691 |   98257     664     2140     3.2 | 14.929 % |
c |      1320 |  199201   693183 |  108082    1085     3533     3.3 | 15.250 % |
c |      2079 |  198019   689201 |  118891    1718     5783     3.4 | 15.765 % |
c |      3218 |  197116   686184 |  130780    2752    11419     4.1 | 16.147 % |
c |      4926 |  195100   679435 |  143858    4236    19705     4.7 | 17.046 % |
c |      7488 |  192327   670159 |  158244    6474    29255     4.5 | 18.288 % |
c |     11332 |  188289   656650 |  174068    9827    44867     4.6 | 20.143 % |
c |     17098 |  183052   639215 |  191475   14975    71425     4.8 | 22.576 % |
c |     25747 |  179693   628037 |  210623   23170   115660     5.0 | 24.147 % |
c |     38723 |  179203   626395 |  231685   36084   303856     8.4 | 24.367 % |
c |     58184 |  179134   626165 |  254853   55536   812591    14.6 | 24.399 % |
c |     87377 |  179095   626036 |  280339   84724 10604405   125.2 | 24.416 % |
c |    131169 |  179086   626007 |  308373  128514 18609828   144.8 | 24.421 % |
c |    196853 |  179028   625813 |  339210  194186 27918123   143.8 | 24.448 % |
#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.85 0.95 0.91 2/54 1199
Raw data (stat): 1199 (runsolver) R 1198 30854 30853 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 421593014 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 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.87 0.95 0.91 2/54 1199
Raw data (stat): 1199 (minisat+) R 1198 30854 30853 0 -1 0 4450 0 0 0 985 12 0 0 25 0 1 0 421593014 21417984 4306 4294967295 134512640 134672761 3221224576 3221223712 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5229 4306 603 41 0 5188 0
vsize: 20916
[startup+20.0009 s]
Raw data (loadavg): 0.89 0.96 0.91 2/54 1199
Raw data (stat): 1199 (minisat+) R 1198 30854 30853 0 -1 0 4479 0 0 0 1984 13 0 0 25 0 1 0 421593014 21553152 4335 4294967295 134512640 134672761 3221224576 3221223792 134561997 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5262 4335 603 41 0 5221 0
vsize: 21048
[startup+30.002 s]
Raw data (loadavg): 0.91 0.96 0.91 2/54 1199
Raw data (stat): 1199 (minisat+) R 1198 30854 30853 0 -1 0 4489 0 0 0 2984 13 0 0 25 0 1 0 421593014 21553152 4345 4294967295 134512640 134672761 3221224576 3221223748 134556653 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5262 4345 603 41 0 5221 0
vsize: 21048
[startup+40.0018 s]
Raw data (loadavg): 0.92 0.96 0.91 2/54 1199
Raw data (stat): 1199 (minisat+) R 1198 30854 30853 0 -1 0 4497 0 0 0 3984 14 0 0 25 0 1 0 421593014 21696512 4353 4294967295 134512640 134672761 3221224576 3221223748 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5297 4353 603 41 0 5256 0
vsize: 21188
[startup+50.0021 s]
Raw data (loadavg): 0.93 0.96 0.91 2/54 1199
Raw data (stat): 1199 (minisat+) R 1198 30854 30853 0 -1 0 4503 0 0 0 4984 14 0 0 25 0 1 0 421593014 21696512 4359 4294967295 134512640 134672761 3221224576 3221223748 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5297 4359 603 41 0 5256 0
vsize: 21188
[startup+60.0024 s]
Raw data (loadavg): 0.94 0.96 0.91 2/54 1199
Raw data (stat): 1199 (minisat+) R 1198 30854 30853 0 -1 0 4511 0 0 0 5983 14 0 0 25 0 1 0 421593014 21696512 4367 4294967295 134512640 134672761 3221224576 3221223748 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5297 4367 603 41 0 5256 0
vsize: 21188
[startup+70.0031 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 1199
Raw data (stat): 1199 (minisat+) R 1198 30854 30853 0 -1 0 4513 0 0 0 6983 14 0 0 25 0 1 0 421593014 21696512 4369 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5297 4369 603 41 0 5256 0
vsize: 21188
[startup+80.0035 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 1199
Raw data (stat): 1199 (minisat+) R 1198 30854 30853 0 -1 0 4520 0 0 0 7983 15 0 0 25 0 1 0 421593014 21696512 4376 4294967295 134512640 134672761 3221224576 3221223700 134566100 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5297 4376 603 41 0 5256 0
vsize: 21188
[startup+90.0037 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 1199
Raw data (stat): 1199 (minisat+) R 1198 30854 30853 0 -1 0 4525 0 0 0 8983 15 0 0 25 0 1 0 421593014 21696512 4381 4294967295 134512640 134672761 3221224576 3221223776 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5297 4381 603 41 0 5256 0
vsize: 21188
[startup+100.004 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 1199
Raw data (stat): 1199 (minisat+) R 1198 30854 30853 0 -1 0 4529 0 0 0 9982 15 0 0 25 0 1 0 421593014 21696512 4385 4294967295 134512640 134672761 3221224576 3221223728 134565045 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5297 4385 603 41 0 5256 0
vsize: 21188
[startup+110.005 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 1199
Raw data (stat): 1199 (minisat+) R 1198 30854 30853 0 -1 0 4532 0 0 0 10982 16 0 0 25 0 1 0 421593014 21827584 4388 4294967295 134512640 134672761 3221224576 3221223748 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5329 4388 603 41 0 5288 0
vsize: 21316
[startup+120.006 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 1199
Raw data (stat): 1199 (minisat+) R 1198 30854 30853 0 -1 0 4543 0 0 0 11982 16 0 0 25 0 1 0 421593014 21827584 4399 4294967295 134512640 134672761 3221224576 3221223744 134561415 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5329 4399 603 41 0 5288 0
vsize: 21316
[startup+130.007 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 1199
Raw data (stat): 1199 (minisat+) R 1198 30854 30853 0 -1 0 4545 0 0 0 12981 17 0 0 25 0 1 0 421593014 21827584 4401 4294967295 134512640 134672761 3221224576 3221223748 134556649 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5329 4401 603 41 0 5288 0
vsize: 21316
[startup+140.007 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 1199
Raw data (stat): 1199 (minisat+) R 1198 30854 30853 0 -1 0 4550 0 0 0 13981 17 0 0 25 0 1 0 421593014 21827584 4406 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5329 4406 603 41 0 5288 0
vsize: 21316
[startup+150.008 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 1199
Raw data (stat): 1199 (minisat+) R 1198 30854 30853 0 -1 0 4556 0 0 0 14981 17 0 0 25 0 1 0 421593014 21827584 4412 4294967295 134512640 134672761 3221224576 3221223744 134561382 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5329 4412 603 41 0 5288 0
vsize: 21316
[startup+160.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1199
Raw data (stat): 1199 (minisat+) R 1198 30854 30853 0 -1 0 4559 0 0 0 15980 18 0 0 25 0 1 0 421593014 21962752 4415 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5362 4415 603 41 0 5321 0
vsize: 21448
[startup+170.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1199
Raw data (stat): 1199 (minisat+) R 1198 30854 30853 0 -1 0 4561 0 0 0 16979 18 0 0 25 0 1 0 421593014 21962752 4417 4294967295 134512640 134672761 3221224576 3221223700 134566034 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5362 4417 603 41 0 5321 0
vsize: 21448
[startup+180.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1199
Raw data (stat): 1199 (minisat+) R 1198 30854 30853 0 -1 0 4564 0 0 0 17979 18 0 0 25 0 1 0 421593014 21962752 4420 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5362 4420 603 41 0 5321 0
vsize: 21448
[startup+190.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1199
Raw data (stat): 1199 (minisat+) R 1198 30854 30853 0 -1 0 4568 0 0 0 18979 18 0 0 25 0 1 0 421593014 21962752 4424 4294967295 134512640 134672761 3221224576 3221223748 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5362 4424 603 41 0 5321 0
vsize: 21448
[startup+200.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1199
Raw data (stat): 1199 (minisat+) R 1198 30854 30853 0 -1 0 4571 0 0 0 19979 19 0 0 25 0 1 0 421593014 21962752 4427 4294967295 134512640 134672761 3221224576 3221223728 134565073 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5362 4427 603 41 0 5321 0
vsize: 21448
[startup+210.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1199
Raw data (stat): 1199 (minisat+) R 1198 30854 30853 0 -1 0 4575 0 0 0 20978 19 0 0 25 0 1 0 421593014 21962752 4431 4294967295 134512640 134672761 3221224576 3221223744 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5362 4431 603 41 0 5321 0
vsize: 21448
[startup+220.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1199
Raw data (stat): 1199 (minisat+) R 1198 30854 30853 0 -1 0 4578 0 0 0 21978 20 0 0 25 0 1 0 421593014 21962752 4434 4294967295 134512640 134672761 3221224576 3221223728 134565080 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5362 4434 603 41 0 5321 0
vsize: 21448
[startup+230.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1199
Raw data (stat): 1199 (minisat+) R 1198 30854 30853 0 -1 0 4598 0 0 0 22977 20 0 0 25 0 1 0 421593014 22171648 4454 4294967295 134512640 134672761 3221224576 3221223728 134565083 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5413 4454 603 41 0 5372 0
vsize: 21652
[startup+240.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1199
Raw data (stat): 1199 (minisat+) R 1198 30854 30853 0 -1 0 4599 0 0 0 23977 20 0 0 25 0 1 0 421593014 22171648 4455 4294967295 134512640 134672761 3221224576 3221223748 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5413 4455 603 41 0 5372 0
vsize: 21652
[startup+250.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1199
Raw data (stat): 1199 (minisat+) R 1198 30854 30853 0 -1 0 4600 0 0 0 24976 21 0 0 25 0 1 0 421593014 22171648 4456 4294967295 134512640 134672761 3221224576 3221223700 134566034 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5413 4456 603 41 0 5372 0
vsize: 21652
[startup+260.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1199
Raw data (stat): 1199 (minisat+) R 1198 30854 30853 0 -1 0 4605 0 0 0 25976 21 0 0 25 0 1 0 421593014 22171648 4461 4294967295 134512640 134672761 3221224576 3221223760 134557999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5413 4461 603 41 0 5372 0
vsize: 21652
[startup+270.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1199
Raw data (stat): 1199 (minisat+) R 1198 30854 30853 0 -1 0 4621 0 0 0 26975 22 0 0 25 0 1 0 421593014 22171648 4477 4294967295 134512640 134672761 3221224576 3221223748 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5413 4477 603 41 0 5372 0
vsize: 21652
[startup+280.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1199
Raw data (stat): 1199 (minisat+) R 1198 30854 30853 0 -1 0 4662 0 0 0 27975 22 0 0 25 0 1 0 421593014 22306816 4518 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5446 4518 603 41 0 5405 0
vsize: 21784
[startup+290.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1199
Raw data (stat): 1199 (minisat+) R 1198 30854 30853 0 -1 0 4723 0 0 0 28975 23 0 0 25 0 1 0 421593014 22577152 4579 4294967295 134512640 134672761 3221224576 3221223744 134565029 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5512 4579 603 41 0 5471 0
vsize: 22048
[startup+300.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1199
Raw data (stat): 1199 (minisat+) R 1198 30854 30853 0 -1 0 4846 0 0 0 29974 23 0 0 25 0 1 0 421593014 23240704 4702 4294967295 134512640 134672761 3221224576 3221223776 134557830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5674 4702 603 41 0 5633 0
vsize: 22696
[startup+310.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1199
Raw data (stat): 1199 (minisat+) R 1198 30854 30853 0 -1 0 5072 0 0 0 30972 25 0 0 25 0 1 0 421593014 24051712 4928 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5872 4928 603 41 0 5831 0
vsize: 23488
[startup+320.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1199
Raw data (stat): 1199 (minisat+) R 1198 30854 30853 0 -1 0 5467 0 0 0 31971 26 0 0 25 0 1 0 421593014 25665536 5323 4294967295 134512640 134672761 3221224576 3221223748 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6266 5323 603 41 0 6225 0
vsize: 25064
[startup+330.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1199
Raw data (stat): 1199 (minisat+) R 1198 30854 30853 0 -1 0 6307 0 0 0 32968 29 0 0 25 0 1 0 421593014 29028352 6163 4294967295 134512640 134672761 3221224576 3221223760 134558761 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7087 6163 603 41 0 7046 0
vsize: 28348
[startup+340.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1199
Raw data (stat): 1199 (minisat+) R 1198 30854 30853 0 -1 0 7921 0 0 0 33962 34 0 0 25 0 1 0 421593014 35876864 7777 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8759 7777 603 41 0 8718 0
vsize: 35036
[startup+350.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1199
Raw data (stat): 1199 (minisat+) R 1198 30854 30853 0 -1 0 9295 0 0 0 34959 38 0 0 25 0 1 0 421593014 41545728 9151 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10143 9151 603 41 0 10102 0
vsize: 40572
[startup+360.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1199
Raw data (stat): 1199 (minisat+) R 1198 30854 30853 0 -1 0 10700 0 0 0 35955 42 0 0 25 0 1 0 421593014 47296512 10556 4294967295 134512640 134672761 3221224576 3221223680 134560402 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11547 10556 603 41 0 11506 0
vsize: 46188
[startup+370.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1199
Raw data (stat): 1199 (minisat+) R 1198 30854 30853 0 -1 0 11952 0 0 0 36952 46 0 0 25 0 1 0 421593014 52355072 11808 4294967295 134512640 134672761 3221224576 3221223680 134560402 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12782 11808 603 41 0 12741 0
vsize: 51128
[startup+380.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1199
Raw data (stat): 1199 (minisat+) R 1198 30854 30853 0 -1 0 13163 0 0 0 37949 48 0 0 25 0 1 0 421593014 57344000 13019 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14000 13019 603 41 0 13959 0
vsize: 56000
[startup+390.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1199
Raw data (stat): 1199 (minisat+) R 1198 30854 30853 0 -1 0 14119 0 0 0 38947 51 0 0 25 0 1 0 421593014 61259776 13975 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14956 13975 603 41 0 14915 0
vsize: 59824
[startup+400.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1199
Raw data (stat): 1199 (minisat+) R 1198 30854 30853 0 -1 0 15033 0 0 0 39944 54 0 0 25 0 1 0 421593014 65036288 14889 4294967295 134512640 134672761 3221224576 3221223680 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15878 14889 603 41 0 15837 0
vsize: 63512
[startup+410.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1199
Raw data (stat): 1199 (minisat+) R 1198 30854 30853 0 -1 0 15860 0 0 0 40942 56 0 0 25 0 1 0 421593014 68411392 15716 4294967295 134512640 134672761 3221224576 3221223680 134555211 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16702 15716 603 41 0 16661 0
vsize: 66808
[startup+420.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1199
Raw data (stat): 1199 (minisat+) R 1198 30854 30853 0 -1 0 17337 0 0 0 41939 59 0 0 25 0 1 0 421593014 74342400 17193 4294967295 134512640 134672761 3221224576 3221223744 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18150 17193 603 41 0 18109 0
vsize: 72600
[startup+430.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1199
Raw data (stat): 1199 (minisat+) R 1198 30854 30853 0 -1 0 18455 0 0 0 42937 62 0 0 25 0 1 0 421593014 78929920 18311 4294967295 134512640 134672761 3221224576 3221223716 134560629 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19270 18311 603 41 0 19229 0
vsize: 77080
[startup+440.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1199
Raw data (stat): 1199 (minisat+) R 1198 30854 30853 0 -1 0 19381 0 0 0 43935 64 0 0 25 0 1 0 421593014 82706432 19237 4294967295 134512640 134672761 3221224576 3221223680 134560246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20192 19237 603 41 0 20151 0
vsize: 80768
[startup+450.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1199
Raw data (stat): 1199 (minisat+) R 1198 30854 30853 0 -1 0 20214 0 0 0 44932 67 0 0 25 0 1 0 421593014 86106112 20070 4294967295 134512640 134672761 3221224576 3221223760 134559498 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21022 20070 603 41 0 20981 0
vsize: 84088
[startup+460.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1199
Raw data (stat): 1199 (minisat+) R 1198 30854 30853 0 -1 0 20977 0 0 0 45929 70 0 0 25 0 1 0 421593014 89194496 20833 4294967295 134512640 134672761 3221224576 3221223744 134560994 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21776 20833 603 41 0 21735 0
vsize: 87104
[startup+470.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1199
Raw data (stat): 1199 (minisat+) R 1198 30854 30853 0 -1 0 21610 0 0 0 46928 71 0 0 25 0 1 0 421593014 91758592 21466 4294967295 134512640 134672761 3221224576 3221223744 134561292 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22402 21466 603 41 0 22361 0
vsize: 89608
[startup+480.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1199
Raw data (stat): 1199 (minisat+) R 1198 30854 30853 0 -1 0 22279 0 0 0 47927 72 0 0 25 0 1 0 421593014 94588928 22135 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23093 22135 603 41 0 23052 0
vsize: 92372
[startup+490.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1199
Raw data (stat): 1199 (minisat+) R 1198 30854 30853 0 -1 0 22859 0 0 0 48926 74 0 0 25 0 1 0 421593014 96935936 22715 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23666 22715 603 41 0 23625 0
vsize: 94664
[startup+500.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1199
Raw data (stat): 1199 (minisat+) R 1198 30854 30853 0 -1 0 23473 0 0 0 49924 76 0 0 25 0 1 0 421593014 99516416 23329 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24296 23329 603 41 0 24255 0
vsize: 97184
[startup+510.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1199
Raw data (stat): 1199 (minisat+) R 1198 30854 30853 0 -1 0 24146 0 0 0 50922 78 0 0 25 0 1 0 421593014 102211584 24002 4294967295 134512640 134672761 3221224576 3221223712 134560688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24954 24002 603 41 0 24913 0
vsize: 99816
[startup+520.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1199
Raw data (stat): 1199 (minisat+) R 1198 30854 30853 0 -1 0 25349 0 0 0 51919 81 0 0 25 0 1 0 421593014 107724800 25205 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26300 25205 603 41 0 26259 0
vsize: 105200
[startup+530.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1199
Raw data (stat): 1199 (minisat+) R 1198 30854 30853 0 -1 0 26445 0 0 0 52916 85 0 0 25 0 1 0 421593014 112164864 26301 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27384 26301 603 41 0 27343 0
vsize: 109536
[startup+540.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1199
Raw data (stat): 1199 (minisat+) R 1198 30854 30853 0 -1 0 27173 0 0 0 53914 87 0 0 25 0 1 0 421593014 115134464 27029 4294967295 134512640 134672761 3221224576 3221223744 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28109 27029 603 41 0 28068 0
vsize: 112436
[startup+550.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1199
Raw data (stat): 1199 (minisat+) R 1198 30854 30853 0 -1 0 27972 0 0 0 54912 88 0 0 25 0 1 0 421593014 118374400 27828 4294967295 134512640 134672761 3221224576 3221223760 134559332 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28900 27828 603 41 0 28859 0
vsize: 115600
[startup+560.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1199
Raw data (stat): 1199 (minisat+) R 1198 30854 30853 0 -1 0 29159 0 0 0 55909 92 0 0 25 0 1 0 421593014 123224064 29015 4294967295 134512640 134672761 3221224576 3221223744 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30084 29015 603 41 0 30043 0
vsize: 120336
[startup+570.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1199
Raw data (stat): 1199 (minisat+) R 1198 30854 30853 0 -1 0 30106 0 0 0 56906 95 0 0 25 0 1 0 421593014 127127552 29962 4294967295 134512640 134672761 3221224576 3221223680 134560402 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31037 29963 603 41 0 30996 0
vsize: 124148
[startup+580.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1199
Raw data (stat): 1199 (minisat+) R 1198 30854 30853 0 -1 0 31011 0 0 0 57904 97 0 0 25 0 1 0 421593014 130764800 30867 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31925 30867 603 41 0 31884 0
vsize: 127700
[startup+590.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1199
Raw data (stat): 1199 (minisat+) R 1198 30854 30853 0 -1 0 31769 0 0 0 58902 99 0 0 25 0 1 0 421593014 133865472 31625 4294967295 134512640 134672761 3221224576 3221223680 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32682 31625 603 41 0 32641 0
vsize: 130728
[startup+600.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1199
Raw data (stat): 1199 (minisat+) R 1198 30854 30853 0 -1 0 32391 0 0 0 59901 100 0 0 25 0 1 0 421593014 136417280 32247 4294967295 134512640 134672761 3221224576 3221223744 134561375 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33305 32247 603 41 0 33264 0
vsize: 133220
[startup+610.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1199
Raw data (stat): 1199 (minisat+) R 1198 30854 30853 0 -1 0 33304 0 0 0 60899 103 0 0 25 0 1 0 421593014 140201984 33160 4294967295 134512640 134672761 3221224576 3221223680 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34229 33160 603 41 0 34188 0
vsize: 136916
[startup+620.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1199
Raw data (stat): 1199 (minisat+) R 1198 30854 30853 0 -1 0 34233 0 0 0 61897 105 0 0 25 0 1 0 421593014 143970304 34089 4294967295 134512640 134672761 3221224576 3221223744 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35149 34089 603 41 0 35108 0
vsize: 140596
[startup+630.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1199
Raw data (stat): 1199 (minisat+) R 1198 30854 30853 0 -1 0 35199 0 0 0 62895 108 0 0 25 0 1 0 421593014 147873792 35055 4294967295 134512640 134672761 3221224576 3221223680 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36102 35055 603 41 0 36061 0
vsize: 144408
[startup+640.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1199
Raw data (stat): 1199 (minisat+) R 1198 30854 30853 0 -1 0 36523 0 0 0 63891 112 0 0 25 0 1 0 421593014 153276416 36379 4294967295 134512640 134672761 3221224576 3221223744 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37421 36379 603 41 0 37380 0
vsize: 149684
[startup+650.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1199
Raw data (stat): 1199 (minisat+) R 1198 30854 30853 0 -1 0 37809 0 0 0 64888 114 0 0 25 0 1 0 421593014 158568448 37665 4294967295 134512640 134672761 3221224576 3221223680 134560252 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38713 37665 603 41 0 38672 0
vsize: 154852
[startup+660.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1199
Raw data (stat): 1199 (minisat+) R 1198 30854 30853 0 -1 0 38973 0 0 0 65885 118 0 0 25 0 1 0 421593014 163295232 38829 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39867 38829 603 41 0 39826 0
vsize: 159468
[startup+670.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1199
Raw data (stat): 1199 (minisat+) R 1198 30854 30853 0 -1 0 40091 0 0 0 66882 121 0 0 25 0 1 0 421593014 167890944 39947 4294967295 134512640 134672761 3221224576 3221223680 134560347 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40989 39947 603 41 0 40948 0
vsize: 163956
[startup+680.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1199
Raw data (stat): 1199 (minisat+) R 1198 30854 30853 0 -1 0 41216 0 0 0 67880 123 0 0 25 0 1 0 421593014 172503040 41072 4294967295 134512640 134672761 3221224576 3221223680 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42115 41072 603 41 0 42074 0
vsize: 168460
[startup+690.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1199
Raw data (stat): 1199 (minisat+) R 1198 30854 30853 0 -1 0 42264 0 0 0 68878 125 0 0 25 0 1 0 421593014 176685056 42120 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43136 42120 603 41 0 43095 0
vsize: 172544
[startup+700.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1199
Raw data (stat): 1199 (minisat+) R 1198 30854 30853 0 -1 0 43355 0 0 0 69877 126 0 0 25 0 1 0 421593014 181174272 43211 4294967295 134512640 134672761 3221224576 3221223680 134560370 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44232 43211 603 41 0 44191 0
vsize: 176928
[startup+710.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1199
Raw data (stat): 1199 (minisat+) R 1198 30854 30853 0 -1 0 44339 0 0 0 70875 129 0 0 25 0 1 0 421593014 185270272 44195 4294967295 134512640 134672761 3221224576 3221223680 134560246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45232 44195 603 41 0 45191 0
vsize: 180928
[startup+720.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1199
Raw data (stat): 1199 (minisat+) R 1198 30854 30853 0 -1 0 45468 0 0 0 71873 131 0 0 25 0 1 0 421593014 189878272 45324 4294967295 134512640 134672761 3221224576 3221223680 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46357 45324 603 41 0 46316 0
vsize: 185428
[startup+730.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1199
Raw data (stat): 1199 (minisat+) R 1198 30854 30853 0 -1 0 46563 0 0 0 72870 134 0 0 25 0 1 0 421593014 194371584 46419 4294967295 134512640 134672761 3221224576 3221223680 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47454 46419 603 41 0 47413 0
vsize: 189816
[startup+740.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1199
Raw data (stat): 1199 (minisat+) R 1198 30854 30853 0 -1 0 47440 0 0 0 73868 136 0 0 25 0 1 0 421593014 197902336 47296 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48316 47296 603 41 0 48275 0
vsize: 193264
[startup+750.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1199
Raw data (stat): 1199 (minisat+) R 1198 30854 30853 0 -1 0 48202 0 0 0 74866 138 0 0 25 0 1 0 421593014 201023488 48058 4294967295 134512640 134672761 3221224576 3221223680 134559905 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 49078 48058 603 41 0 49037 0
vsize: 196312
[startup+760.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1199
Raw data (stat): 1199 (minisat+) R 1198 30854 30853 0 -1 0 48968 0 0 0 75864 140 0 0 25 0 1 0 421593014 204128256 48824 4294967295 134512640 134672761 3221224576 3221223680 134560370 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 49836 48824 603 41 0 49795 0
vsize: 199344
[startup+770.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1199
Raw data (stat): 1199 (minisat+) R 1198 30854 30853 0 -1 0 49799 0 0 0 76862 143 0 0 25 0 1 0 421593014 207499264 49655 4294967295 134512640 134672761 3221224576 3221223760 134559498 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 50659 49655 603 41 0 50618 0
vsize: 202636
[startup+780.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1199
Raw data (stat): 1199 (minisat+) R 1198 30854 30853 0 -1 0 50648 0 0 0 77861 144 0 0 25 0 1 0 421593014 211013632 50504 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 51517 50504 603 41 0 51476 0
vsize: 206068
[startup+790.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1199
Raw data (stat): 1199 (minisat+) R 1198 30854 30853 0 -1 0 51414 0 0 0 78859 146 0 0 25 0 1 0 421593014 214237184 51270 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 52304 51270 603 41 0 52263 0
vsize: 209216
[startup+800.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1199
Raw data (stat): 1199 (minisat+) R 1198 30854 30853 0 -1 0 52280 0 0 0 79857 148 0 0 25 0 1 0 421593014 217763840 52136 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 53165 52136 603 41 0 53124 0
vsize: 212660
[startup+810.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1199
Raw data (stat): 1199 (minisat+) R 1198 30854 30853 0 -1 0 53052 0 0 0 80856 150 0 0 25 0 1 0 421593014 220876800 52908 4294967295 134512640 134672761 3221224576 3221223648 134553557 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 53925 52908 603 41 0 53884 0
vsize: 215700
[startup+820.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1199
Raw data (stat): 1199 (minisat+) R 1198 30854 30853 0 -1 0 53814 0 0 0 81854 152 0 0 25 0 1 0 421593014 223985664 53670 4294967295 134512640 134672761 3221224576 3221223744 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 54684 53670 603 41 0 54643 0
vsize: 218736
[startup+830.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1199
Raw data (stat): 1199 (minisat+) R 1198 30854 30853 0 -1 0 54485 0 0 0 82853 153 0 0 25 0 1 0 421593014 226791424 54341 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55369 54341 603 41 0 55328 0
vsize: 221476
[startup+840.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1199
Raw data (stat): 1199 (minisat+) R 1198 30854 30853 0 -1 0 55185 0 0 0 83851 155 0 0 25 0 1 0 421593014 229629952 55041 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 56062 55041 603 41 0 56021 0
vsize: 224248
[startup+850.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1199
Raw data (stat): 1199 (minisat+) R 1198 30854 30853 0 -1 0 55979 0 0 0 84850 157 0 0 25 0 1 0 421593014 232849408 55835 4294967295 134512640 134672761 3221224576 3221223680 134559866 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 56848 55835 603 41 0 56807 0
vsize: 227392
[startup+860.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1199
Raw data (stat): 1199 (minisat+) R 1198 30854 30853 0 -1 0 56653 0 0 0 85848 158 0 0 25 0 1 0 421593014 235667456 56509 4294967295 134512640 134672761 3221224576 3221223680 134560326 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 57536 56509 603 41 0 57495 0
vsize: 230144
[startup+870.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1199
Raw data (stat): 1199 (minisat+) R 1198 30854 30853 0 -1 0 57349 0 0 0 86847 160 0 0 25 0 1 0 421593014 238489600 57205 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58225 57205 603 41 0 58184 0
vsize: 232900
[startup+880.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1199
Raw data (stat): 1199 (minisat+) R 1198 30854 30853 0 -1 0 58162 0 0 0 87846 161 0 0 25 0 1 0 421593014 241745920 58018 4294967295 134512640 134672761 3221224576 3221223680 134555116 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 59020 58018 603 41 0 58979 0
vsize: 236080
[startup+890.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1199
Raw data (stat): 1199 (minisat+) R 1198 30854 30853 0 -1 0 58961 0 0 0 88845 162 0 0 25 0 1 0 421593014 245129216 58817 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 59846 58817 603 41 0 59805 0
vsize: 239384
[startup+900.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1199
Raw data (stat): 1199 (minisat+) R 1198 30854 30853 0 -1 0 59699 0 0 0 89843 164 0 0 25 0 1 0 421593014 248111104 59555 4294967295 134512640 134672761 3221224576 3221223744 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 60574 59555 603 41 0 60533 0
vsize: 242296
[startup+910.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1199
Raw data (stat): 1199 (minisat+) R 1198 30854 30853 0 -1 0 60434 0 0 0 90842 166 0 0 25 0 1 0 421593014 251072512 60290 4294967295 134512640 134672761 3221224576 3221223760 134559354 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61297 60291 603 41 0 61256 0
vsize: 245188
[startup+920.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1199
Raw data (stat): 1199 (minisat+) R 1198 30854 30853 0 -1 0 61272 0 0 0 91840 168 0 0 25 0 1 0 421593014 254492672 61128 4294967295 134512640 134672761 3221224576 3221223744 134561118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 62132 61128 603 41 0 62091 0
vsize: 248528
[startup+930.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1199
Raw data (stat): 1199 (minisat+) R 1198 30854 30853 0 -1 0 62047 0 0 0 92838 170 0 0 25 0 1 0 421593014 257748992 61903 4294967295 134512640 134672761 3221224576 3221223680 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 62927 61903 603 41 0 62886 0
vsize: 251708
[startup+940.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1199
Raw data (stat): 1199 (minisat+) R 1198 30854 30853 0 -1 0 62758 0 0 0 93837 171 0 0 25 0 1 0 421593014 260608000 62614 4294967295 134512640 134672761 3221224576 3221223744 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 63625 62614 603 41 0 63584 0
vsize: 254500
[startup+950.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1199
Raw data (stat): 1199 (minisat+) R 1198 30854 30853 0 -1 0 63425 0 0 0 94836 173 0 0 25 0 1 0 421593014 263331840 63281 4294967295 134512640 134672761 3221224576 3221223680 134560231 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 64290 63281 603 41 0 64249 0
vsize: 257160
[startup+960.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1199
Raw data (stat): 1199 (minisat+) R 1198 30854 30853 0 -1 0 64023 0 0 0 95835 174 0 0 25 0 1 0 421593014 265777152 63879 4294967295 134512640 134672761 3221224576 3221223744 134560906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 64887 63879 603 41 0 64846 0
vsize: 259548
[startup+970.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1199
Raw data (stat): 1199 (minisat+) R 1198 30854 30853 0 -1 0 64650 0 0 0 96833 175 0 0 25 0 1 0 421593014 268353536 64506 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65516 64506 603 41 0 65475 0
vsize: 262064
[startup+980.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1199
Raw data (stat): 1199 (minisat+) R 1198 30854 30853 0 -1 0 65206 0 0 0 97833 176 0 0 25 0 1 0 421593014 270655488 65062 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 66078 65062 603 41 0 66037 0
vsize: 264312
[startup+990.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1199
Raw data (stat): 1199 (minisat+) R 1198 30854 30853 0 -1 0 65753 0 0 0 98831 178 0 0 25 0 1 0 421593014 272830464 65609 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 66609 65609 603 41 0 66568 0
vsize: 266436
[startup+1000.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1199
Raw data (stat): 1199 (minisat+) R 1198 30854 30853 0 -1 0 66455 0 0 0 99830 180 0 0 25 0 1 0 421593014 275812352 66311 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 67337 66311 603 41 0 67296 0
vsize: 269348
[startup+1010.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1199
Raw data (stat): 1199 (minisat+) R 1198 30854 30853 0 -1 0 67027 0 0 0 100828 181 0 0 25 0 1 0 421593014 278110208 66883 4294967295 134512640 134672761 3221224576 3221223680 134560379 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 67898 66884 603 41 0 67857 0
vsize: 271592
[startup+1020.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1199
Raw data (stat): 1199 (minisat+) R 1198 30854 30853 0 -1 0 67583 0 0 0 101827 183 0 0 25 0 1 0 421593014 280403968 67439 4294967295 134512640 134672761 3221224576 3221223680 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 68458 67439 603 41 0 68417 0
vsize: 273832
[startup+1030.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1199
Raw data (stat): 1199 (minisat+) R 1198 30854 30853 0 -1 0 68244 0 0 0 102826 184 0 0 25 0 1 0 421593014 283115520 68100 4294967295 134512640 134672761 3221224576 3221223744 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69120 68100 603 41 0 69079 0
vsize: 276480
[startup+1040.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1199
Raw data (stat): 1199 (minisat+) R 1198 30854 30853 0 -1 0 68849 0 0 0 103824 186 0 0 25 0 1 0 421593014 285556736 68705 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69716 68705 603 41 0 69675 0
vsize: 278864
[startup+1050.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1199
Raw data (stat): 1199 (minisat+) R 1198 30854 30853 0 -1 0 69511 0 0 0 104823 187 0 0 25 0 1 0 421593014 288272384 69367 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 70379 69367 603 41 0 70338 0
vsize: 281516
[startup+1060.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1199
Raw data (stat): 1199 (minisat+) R 1198 30854 30853 0 -1 0 70126 0 0 0 105822 189 0 0 25 0 1 0 421593014 290738176 69982 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 70981 69982 603 41 0 70940 0
vsize: 283924
[startup+1070.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1199
Raw data (stat): 1199 (minisat+) R 1198 30854 30853 0 -1 0 70756 0 0 0 106821 189 0 0 25 0 1 0 421593014 293326848 70612 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 71613 70612 603 41 0 71572 0
vsize: 286452
[startup+1080.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1199
Raw data (stat): 1199 (minisat+) R 1198 30854 30853 0 -1 0 71313 0 0 0 107820 191 0 0 25 0 1 0 421593014 295645184 71169 4294967295 134512640 134672761 3221224576 3221223744 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 72179 71169 603 41 0 72138 0
vsize: 288716
[startup+1090.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1199
Raw data (stat): 1199 (minisat+) R 1198 30854 30853 0 -1 0 71875 0 0 0 108819 192 0 0 25 0 1 0 421593014 297951232 71731 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 72742 71731 603 41 0 72701 0
vsize: 290968
[startup+1100.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1199
Raw data (stat): 1199 (minisat+) R 1198 30854 30853 0 -1 0 72481 0 0 0 109818 193 0 0 25 0 1 0 421593014 300523520 72337 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 73370 72337 603 41 0 73329 0
vsize: 293480
[startup+1110.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1199
Raw data (stat): 1199 (minisat+) R 1198 30854 30853 0 -1 0 73024 0 0 0 110817 194 0 0 25 0 1 0 421593014 303722496 72880 4294967295 134512640 134672761 3221224576 3221223760 134558899 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 74151 72880 603 41 0 74110 0
vsize: 296604
[startup+1120.03 s]
Raw data (loadavg): 1.07 0.99 0.91 2/54 1199
Raw data (stat): 1199 (minisat+) R 1198 30854 30853 0 -1 0 73630 0 0 0 111816 196 0 0 25 0 1 0 421593014 306278400 73486 4294967295 134512640 134672761 3221224576 3221223744 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 74775 73486 603 41 0 74734 0
vsize: 299100
[startup+1130.03 s]
Raw data (loadavg): 1.06 0.99 0.91 2/54 1199
Raw data (stat): 1199 (minisat+) R 1198 30854 30853 0 -1 0 74234 0 0 0 112815 197 0 0 25 0 1 0 421593014 308707328 74090 4294967295 134512640 134672761 3221224576 3221223744 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 75368 74090 603 41 0 75327 0
vsize: 301472
[startup+1140.03 s]
Raw data (loadavg): 1.05 0.99 0.91 2/54 1199
Raw data (stat): 1199 (minisat+) R 1198 30854 30853 0 -1 0 74859 0 0 0 113813 199 0 0 25 0 1 0 421593014 311291904 74715 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 75999 74715 603 41 0 75958 0
vsize: 303996
[startup+1150.03 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 1199
Raw data (stat): 1199 (minisat+) R 1198 30854 30853 0 -1 0 75381 0 0 0 114812 200 0 0 25 0 1 0 421593014 313335808 75237 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 76498 75237 603 41 0 76457 0
vsize: 305992
[startup+1160.03 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 1199
Raw data (stat): 1199 (minisat+) R 1198 30854 30853 0 -1 0 76045 0 0 0 115811 201 0 0 25 0 1 0 421593014 316059648 75901 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 77163 75901 603 41 0 77122 0
vsize: 308652
[startup+1170.03 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 1199
Raw data (stat): 1199 (minisat+) R 1198 30854 30853 0 -1 0 76711 0 0 0 116810 203 0 0 25 0 1 0 421593014 318795776 76567 4294967295 134512640 134672761 3221224576 3221223680 134559914 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 77831 76567 603 41 0 77790 0
vsize: 311324
[startup+1180.03 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 1199
Raw data (stat): 1199 (minisat+) R 1198 30854 30853 0 -1 0 77314 0 0 0 117808 204 0 0 25 0 1 0 421593014 321359872 77170 4294967295 134512640 134672761 3221224576 3221223744 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 78457 77170 603 41 0 78416 0
vsize: 313828
[startup+1190.03 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 1199
Raw data (stat): 1199 (minisat+) R 1198 30854 30853 0 -1 0 77989 0 0 0 118807 206 0 0 25 0 1 0 421593014 324104192 77845 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 79127 77845 603 41 0 79086 0
vsize: 316508
[startup+1200.03 s]
Raw data (loadavg): 1.09 1.00 0.92 2/54 1199
Raw data (stat): 1199 (minisat+) R 1198 30854 30853 0 -1 0 78640 0 0 0 119806 207 0 0 25 0 1 0 421593014 326696960 78496 4294967295 134512640 134672761 3221224576 3221223744 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 79760 78496 603 41 0 79719 0
vsize: 319040
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.18 s]
Raw data (loadavg): 1.09 1.00 0.92 1/54 1199
Raw data (stat): 1199 (minisat+) Z 1198 30854 30853 0 -1 12 78642 0 0 0 119806 221 0 0 25 0 1 0 421593014 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.18
CPU time (s): 1200.29
CPU user time (s): 1198.07
CPU system time (s): 2.21966
CPU usage (%): 100.009
Max. virtual memory (Kb): 319040
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####