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 6452

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.077
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:        880952 kB
Buffers:         36016 kB
Cached:          80600 kB
SwapCached:          4 kB
Active:          56860 kB
Inactive:        63524 kB
HighTotal:      131008 kB
HighFree:        45864 kB
LowTotal:       903652 kB
LowFree:        835088 kB
SwapTotal:     2097640 kB
SwapFree:      2097636 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6920 kB
Slab:            27840 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-14 05:21:24 (client local time) WITH STATUS 0 IN 1200.24 SECONDS
stats: 4866 7 1200.24 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]---> BDD-cost:   17
c ---[11314]---> BDD-cost:   25
c ---[11312]---> BDD-cost:   17
c ---[11310]---> BDD-cost:   25
c ---[11308]---> BDD-cost:   17
c ---[11306]---> BDD-cost:   25
c ---[11304]---> BDD-cost:   17
c ---[11302]---> BDD-cost:   25
c ---[11300]---> BDD-cost:   17
c ---[11298]---> BDD-cost:   25
c ---[11296]---> BDD-cost:   17
c ---[11294]---> BDD-cost:   25
c ---[11292]---> BDD-cost:   17
c ---[11290]---> BDD-cost:   25
c ---[11288]---> BDD-cost:   17
c ---[11286]---> BDD-cost:   25
c ---[11284]---> BDD-cost:   17
c ---[11282]---> BDD-cost:   25
c ---[11280]---> BDD-cost:   17
c ---[11278]---> BDD-cost:   25
c ---[11276]---> BDD-cost:   17
c ---[11274]---> BDD-cost:   25
c ---[11272]---> BDD-cost:   17
c ---[11270]---> BDD-cost:   25
c ---[11268]---> BDD-cost:   17
c ---[11266]---> BDD-cost:   25
c ---[11264]---> BDD-cost:   17
c ---[11262]---> BDD-cost:   25
c ---[11260]---> BDD-cost:   17
c ---[11258]---> BDD-cost:   25
c ---[11256]---> BDD-cost:   17
c ---[11254]---> BDD-cost:   25
c ---[11252]---> BDD-cost:   17
c ---[11250]---> BDD-cost:   25
c ---[11248]---> BDD-cost:   17
c ---[11246]---> BDD-cost:   25
c ---[11244]---> BDD-cost:   17
c ---[11242]---> BDD-cost:   25
c ---[11240]---> BDD-cost:   17
c ---[11238]---> BDD-cost:   25
c ---[11236]---> BDD-cost:   17
c ---[11234]---> BDD-cost:   25
c ---[11232]---> BDD-cost:   17
c ---[11230]---> BDD-cost:   25
c ---[11228]---> BDD-cost:   17
c ---[11226]---> BDD-cost:   25
c ---[11224]---> BDD-cost:   17
c ---[11222]---> BDD-cost:   25
c ---[11220]---> BDD-cost:   17
c ---[11218]---> BDD-cost:   25
c ---[11216]---> BDD-cost:   17
c ---[11214]---> BDD-cost:   25
c ---[11212]---> BDD-cost:   17
c ---[11210]---> BDD-cost:   25
c ---[11208]---> BDD-cost:   17
c ---[11206]---> BDD-cost:   25
c ---[11204]---> BDD-cost:   17
c ---[11202]---> BDD-cost:   25
c ---[11200]---> BDD-cost:   17
c ---[11198]---> BDD-cost:   25
c ---[11196]---> BDD-cost:   17
c ---[11194]---> BDD-cost:   25
c ---[11192]---> BDD-cost:   17
c ---[11190]---> BDD-cost:   25
c ---[11188]---> BDD-cost:   17
c ---[11186]---> BDD-cost:   25
c ---[11184]---> BDD-cost:   17
c ---[11182]---> BDD-cost:   25
c ---[11180]---> BDD-cost:   17
c ---[11178]---> BDD-cost:   25
c ---[11176]---> BDD-cost:   17
c ---[11174]---> BDD-cost:   25
c ---[11172]---> BDD-cost:   17
c ---[11170]---> BDD-cost:   25
c ---[11168]---> BDD-cost:   17
c ---[11166]---> BDD-cost:   25
c ---[11164]---> BDD-cost:   17
c ---[11162]---> BDD-cost:   25
c ---[11160]---> BDD-cost:   17
c ---[11158]---> BDD-cost:   25
c ---[11156]---> BDD-cost:   17
c ---[11154]---> BDD-cost:   25
c ---[11152]---> BDD-cost:   17
c ---[11150]---> BDD-cost:   25
c ---[11148]---> BDD-cost:   17
c ---[11146]---> BDD-cost:   25
c ---[11144]---> BDD-cost:   17
c ---[11142]---> BDD-cost:   25
c ---[11140]---> BDD-cost:   17
c ---[11138]---> BDD-cost:   25
c ---[11136]---> BDD-cost:   17
c ---[11134]---> BDD-cost:   25
c ---[11132]---> BDD-cost:   17
c ---[11130]---> BDD-cost:   25
c ---[11128]---> BDD-cost:   17
c ---[11126]---> BDD-cost:   25
c ---[11124]---> BDD-cost:   17
c ---[11122]---> BDD-cost:   25
c ---[11120]---> BDD-cost:   17
c ---[11118]---> BDD-cost:   25
c ---[11116]---> BDD-cost:   17
c ---[11114]---> BDD-cost:   25
c ---[11112]---> BDD-cost:   17
c ---[11110]---> BDD-cost:   25
c ---[11108]---> BDD-cost:   17
c ---[11106]---> BDD-cost:   25
c ---[11104]---> BDD-cost:   17
c ---[11102]---> BDD-cost:   25
c ---[11100]---> BDD-cost:   25
c ---[11098]---> BDD-cost:   17
c ---[11096]---> BDD-cost:   25
c ---[11094]---> BDD-cost:   17
c ---[11092]---> BDD-cost:   25
c ---[11090]---> BDD-cost:   17
c ---[11088]---> BDD-cost:   25
c ---[11086]---> BDD-cost:   17
c ---[11084]---> BDD-cost:   25
c ---[11082]---> BDD-cost:   17
c ---[11080]---> BDD-cost:   25
c ---[11078]---> BDD-cost:   17
c ---[11076]---> BDD-cost:   25
c ---[11074]---> BDD-cost:   17
c ---[11072]---> BDD-cost:   25
c ---[11070]---> BDD-cost:   25
c ---[11068]---> BDD-cost:   17
c ---[11066]---> BDD-cost:   25
c ---[11064]---> BDD-cost:   17
c ---[11062]---> BDD-cost:   25
c ---[11060]---> BDD-cost:   17
c ---[11058]---> BDD-cost:   25
c ---[11056]---> BDD-cost:   17
c ---[11054]---> BDD-cost:   25
c ---[11052]---> BDD-cost:   17
c ---[11050]---> BDD-cost:   25
c ---[11048]---> BDD-cost:   17
c ---[11046]---> BDD-cost:   25
c ---[11044]---> BDD-cost:   17
c ---[11042]---> BDD-cost:   25
c ---[11040]---> BDD-cost:   17
c ---[11038]---> BDD-cost:   25
c ---[11036]---> BDD-cost:   17
c ---[11034]---> BDD-cost:   25
c ---[11032]---> BDD-cost:   17
c ---[11030]---> BDD-cost:   25
c ---[11028]---> BDD-cost:   17
c ---[11026]---> BDD-cost:   25
c ---[11024]---> BDD-cost:   17
c ---[11022]---> BDD-cost:   25
c ---[11020]---> BDD-cost:   17
c ---[11018]---> BDD-cost:   25
c ---[11016]---> BDD-cost:   17
c ---[11014]---> BDD-cost:   25
c ---[11012]---> BDD-cost:   17
c ---[11010]---> BDD-cost:   25
c ---[11008]---> BDD-cost:   25
c ---[11006]---> BDD-cost:   17
c ---[11004]---> BDD-cost:   25
c ---[11002]---> BDD-cost:   17
c ---[11000]---> BDD-cost:   25
c ---[10998]---> BDD-cost:   17
c ---[10996]---> BDD-cost:   25
c ---[10994]---> BDD-cost:   17
c ---[10992]---> BDD-cost:   25
c ---[10990]---> BDD-cost:   17
c ---[10988]---> BDD-cost:   25
c ---[10986]---> BDD-cost:   17
c ---[10984]---> BDD-cost:   25
c ---[10982]---> BDD-cost:   17
c ---[10980]---> BDD-cost:   25
c ---[10978]---> BDD-cost:   17
c ---[10976]---> BDD-cost:   25
c ---[10974]---> BDD-cost:   17
c ---[10972]---> BDD-cost:   25
c ---[10970]---> BDD-cost:   17
c ---[10968]---> BDD-cost:   25
c ---[10966]---> BDD-cost:   17
c ---[10964]---> BDD-cost:   25
c ---[10962]---> BDD-cost:   17
c ---[10960]---> BDD-cost:   25
c ---[10958]---> BDD-cost:   17
c ---[10956]---> BDD-cost:   25
c ---[10954]---> BDD-cost:   17
c ---[10952]---> BDD-cost:   25
c ---[10950]---> BDD-cost:   17
c ---[10948]---> BDD-cost:   25
c ---[10946]---> BDD-cost:   17
c ---[10944]---> BDD-cost:   25
c ---[10942]---> BDD-cost:   17
c ---[10940]---> BDD-cost:   25
c ---[10938]---> BDD-cost:   17
c ---[10936]---> BDD-cost:   25
c ---[10934]---> BDD-cost:   17
c ---[10932]---> BDD-cost:   25
c ---[10930]---> BDD-cost:   17
c ---[10928]---> BDD-cost:   25
c ---[10926]---> BDD-cost:   17
c ---[10924]---> BDD-cost:   25
c ---[10922]---> BDD-cost:   17
c ---[10920]---> BDD-cost:   25
c ---[10918]---> BDD-cost:   17
c ---[10916]---> BDD-cost:   25
c ---[10914]---> BDD-cost:   17
c ---[10912]---> BDD-cost:   25
c ---[10910]---> BDD-cost:   17
c ---[10908]---> BDD-cost:   25
c ---[10906]---> BDD-cost:   25
c ---[10904]---> BDD-cost:   17
c ---[10902]---> BDD-cost:   25
c ---[10900]---> BDD-cost:   17
c ---[10898]---> BDD-cost:   25
c ---[10896]---> BDD-cost:   17
c ---[10894]---> BDD-cost:   25
c ---[10892]---> BDD-cost:   17
c ---[10890]---> BDD-cost:   25
c ---[10888]---> BDD-cost:   17
c ---[10886]---> BDD-cost:   25
c ---[10884]---> BDD-cost:   17
c ---[10882]---> BDD-cost:   25
c ---[10880]---> BDD-cost:   17
c ---[10878]---> BDD-cost:   25
c ---[10876]---> BDD-cost:   17
c ---[10874]---> BDD-cost:   25
c ---[10872]---> BDD-cost:   17
c ---[10870]---> BDD-cost:   25
c ---[10868]---> BDD-cost:   17
c ---[10866]---> BDD-cost:   25
c ---[10864]---> BDD-cost:   17
c ---[10862]---> BDD-cost:   25
c ---[10860]---> BDD-cost:   17
c ---[10858]---> BDD-cost:   25
c ---[10856]---> BDD-cost:   17
c ---[10854]---> BDD-cost:   25
c ---[10852]---> BDD-cost:   17
c ---[10850]---> BDD-cost:   25
c ---[10848]---> BDD-cost:   17
c ---[10846]---> BDD-cost:   25
c ---[10844]---> BDD-cost:   17
c ---[10842]---> BDD-cost:   25
c ---[10840]---> BDD-cost:   17
c ---[10838]---> BDD-cost:   25
c ---[10836]---> BDD-cost:   17
c ---[10834]---> BDD-cost:   25
c ---[10832]---> BDD-cost:   17
c ---[10830]---> BDD-cost:   25
c ---[10828]---> BDD-cost:   17
c ---[10826]---> BDD-cost:   25
c ---[10824]---> BDD-cost:   17
c ---[10822]---> BDD-cost:   25
c ---[10820]---> BDD-cost:   17
c ---[10818]---> BDD-cost:   25
c ---[10816]---> BDD-cost:   17
c ---[10814]---> BDD-cost:   25
c ---[10812]---> BDD-cost:   17
c ---[10810]---> BDD-cost:   25
c ---[10808]---> BDD-cost:   17
c ---[10806]---> BDD-cost:   25
c ---[10804]---> BDD-cost:   17
c ---[10802]---> BDD-cost:   25
c ---[10800]---> BDD-cost:   17
c ---[10798]---> BDD-cost:   25
c ---[10796]---> BDD-cost:   17
c ---[10794]---> BDD-cost:   25
c ---[10792]---> BDD-cost:   17
c ---[10790]---> BDD-cost:   25
c ---[10788]---> BDD-cost:   17
c ---[10786]---> BDD-cost:   25
c ---[10784]---> BDD-cost:   17
c ---[10782]---> BDD-cost:   25
c ---[10780]---> BDD-cost:   17
c ---[10778]---> BDD-cost:   25
c ---[10776]---> BDD-cost:   17
c ---[10774]---> BDD-cost:   25
c ---[10772]---> BDD-cost:   17
c ---[10770]---> BDD-cost:   25
c ---[10768]---> BDD-cost:   17
c ---[10766]---> BDD-cost:   25
c ---[10764]---> BDD-cost:   17
c ---[10762]---> BDD-cost:   25
c ---[10760]---> BDD-cost:   17
c ---[10758]---> BDD-cost:   25
c ---[10756]---> BDD-cost:   17
c ---[10754]---> BDD-cost:   25
c ---[10752]---> BDD-cost:   17
c ---[10750]---> BDD-cost:   25
c ---[10748]---> BDD-cost:   17
c ---[10746]---> BDD-cost:   25
c ---[10744]---> BDD-cost:   17
c ---[10742]---> BDD-cost:   25
c ---[10740]---> BDD-cost:   17
c ---[10738]---> BDD-cost:   25
c ---[10736]---> BDD-cost:   17
c ---[10734]---> BDD-cost:   25
c ---[10732]---> BDD-cost:   17
c ---[10730]---> BDD-cost:   25
c ---[10728]---> BDD-cost:   17
c ---[10726]---> BDD-cost:   25
c ---[10724]---> BDD-cost:   17
c ---[10722]---> BDD-cost:   25
c ---[10720]---> BDD-cost:   17
c ---[10718]---> BDD-cost:   25
c ---[10716]---> BDD-cost:   17
c ---[10714]---> BDD-cost:   25
c ---[10712]---> BDD-cost:   17
c ---[10710]---> BDD-cost:   25
c ---[10708]---> BDD-cost:   17
c ---[10706]---> BDD-cost:   25
c ---[10704]---> BDD-cost:   17
c ---[10702]---> BDD-cost:   25
c ---[10700]---> BDD-cost:   17
c ---[10698]---> BDD-cost:   25
c ---[10696]---> BDD-cost:   17
c ---[10694]---> BDD-cost:   25
c ---[10692]---> BDD-cost:   17
c ---[10690]---> BDD-cost:   25
c ---[10688]---> BDD-cost:   17
c ---[10686]---> BDD-cost:   25
c ---[10684]---> BDD-cost:   17
c ---[10682]---> BDD-cost:   25
c ---[10680]---> BDD-cost:   17
c ---[10678]---> BDD-cost:   25
c ---[10676]---> BDD-cost:   17
c ---[10674]---> BDD-cost:   25
c ---[10672]---> BDD-cost:   17
c ---[10670]---> BDD-cost:   25
c ---[10668]---> BDD-cost:   17
c ---[10666]---> BDD-cost:   25
c ---[10664]---> BDD-cost:   17
c ---[10662]---> BDD-cost:   25
c ---[10660]---> BDD-cost:   17
c ---[10658]---> BDD-cost:   25
c ---[10656]---> BDD-cost:   17
c ---[10654]---> BDD-cost:   25
c ---[10652]---> BDD-cost:   17
c ---[10650]---> BDD-cost:   25
c ---[10648]---> BDD-cost:   17
c ---[10646]---> BDD-cost:   25
c ---[10644]---> BDD-cost:   17
c ---[10642]---> BDD-cost:   25
c ---[10640]---> BDD-cost:   17
c ---[10638]---> BDD-cost:   25
c ---[10636]---> BDD-cost:   17
c ---[10634]---> BDD-cost:   25
c ---[10632]---> BDD-cost:   17
c ---[10630]---> BDD-cost:   25
c ---[10628]---> BDD-cost:   17
c ---[10626]---> BDD-cost:   25
c ---[10624]---> BDD-cost:   17
c ---[10622]---> BDD-cost:   25
c ---[10620]---> BDD-cost:   25
c ---[10618]---> BDD-cost:   17
c ---[10616]---> BDD-cost:   25
c ---[10614]---> BDD-cost:   17
c ---[10612]---> BDD-cost:   25
c ---[10610]---> BDD-cost:   17
c ---[10608]---> BDD-cost:   25
c ---[10606]---> BDD-cost:   17
c ---[10604]---> BDD-cost:   25
c ---[10602]---> BDD-cost:   17
c ---[10600]---> BDD-cost:   25
c ---[10598]---> BDD-cost:   17
c ---[10596]---> BDD-cost:   25
c ---[10594]---> BDD-cost:   17
c ---[10592]---> BDD-cost:   25
c ---[10590]---> BDD-cost:   17
c ---[10588]---> BDD-cost:   17
c ---[10586]---> BDD-cost:   25
c ---[10584]---> BDD-cost:   17
c ---[10582]---> BDD-cost:   25
c ---[10580]---> BDD-cost:   17
c ---[10578]---> BDD-cost:   25
c ---[10576]---> BDD-cost:   17
c ---[10574]---> BDD-cost:   25
c ---[10572]---> BDD-cost:   17
c ---[10570]---> BDD-cost:   25
c ---[10568]---> BDD-cost:   17
c ---[10566]---> BDD-cost:   25
c ---[10564]---> BDD-cost:   17
c ---[10562]---> BDD-cost:   25
c ---[10560]---> BDD-cost:   17
c ---[10558]---> BDD-cost:   25
c ---[10556]---> BDD-cost:   17
c ---[10554]---> BDD-cost:   25
c ---[10552]---> BDD-cost:   17
c ---[10550]---> BDD-cost:   25
c ---[10548]---> BDD-cost:   17
c ---[10546]---> BDD-cost:   25
c ---[10544]---> BDD-cost:   17
c ---[10542]---> BDD-cost:   25
c ---[10540]---> BDD-cost:   17
c ---[10538]---> BDD-cost:   25
c ---[10536]---> BDD-cost:   17
c ---[10534]---> BDD-cost:   25
c ---[10532]---> BDD-cost:   17
c ---[10530]---> BDD-cost:   25
c ---[10528]---> BDD-cost:   17
c ---[10526]---> BDD-cost:   25
c ---[10524]---> BDD-cost:   17
c ---[10522]---> BDD-cost:   25
c ---[10520]---> BDD-cost:   17
c ---[10518]---> BDD-cost:   25
c ---[10516]---> BDD-cost:   17
c ---[10514]---> BDD-cost:   25
c ---[10512]---> BDD-cost:   17
c ---[10510]---> BDD-cost:   25
c ---[10508]---> BDD-cost:   17
c ---[10506]---> BDD-cost:   25
c ---[10504]---> BDD-cost:   17
c ---[10502]---> BDD-cost:   25
c ---[10500]---> BDD-cost:   17
c ---[10498]---> BDD-cost:   25
c ---[10496]---> BDD-cost:   17
c ---[10494]---> BDD-cost:   25
c ---[10492]---> BDD-cost:   17
c ---[10490]---> BDD-cost:   25
c ---[10488]---> BDD-cost:   17
c ---[10486]---> BDD-cost:   25
c ---[10484]---> BDD-cost:   17
c ---[10482]---> BDD-cost:   25
c ---[10480]---> BDD-cost:   17
c ---[10478]---> BDD-cost:   25
c ---[10476]---> BDD-cost:   17
c ---[10474]---> BDD-cost:   25
c ---[10472]---> BDD-cost:   17
c ---[10470]---> BDD-cost:   25
c ---[10468]---> BDD-cost:   17
c ---[10466]---> BDD-cost:   25
c ---[10464]---> BDD-cost:   17
c ---[10462]---> BDD-cost:   25
c ---[10460]---> BDD-cost:   17
c ---[10458]---> BDD-cost:   25
c ---[10456]---> BDD-cost:   17
c ---[10454]---> BDD-cost:   25
c ---[10452]---> BDD-cost:   17
c ---[10450]---> BDD-cost:   25
c ---[10448]---> BDD-cost:   17
c ---[10446]---> BDD-cost:   25
c ---[10444]---> BDD-cost:   17
c ---[10442]---> BDD-cost:   25
c ---[10440]---> BDD-cost:   17
c ---[10438]---> BDD-cost:   25
c ---[10436]---> BDD-cost:   17
c ---[10434]---> BDD-cost:   25
c ---[10432]---> BDD-cost:   17
c ---[10430]---> BDD-cost:   25
c ---[10428]---> BDD-cost:   17
c ---[10426]---> BDD-cost:   25
c ---[10424]---> BDD-cost:   17
c ---[10422]---> BDD-cost:   25
c ---[10420]---> BDD-cost:   17
c ---[10418]---> BDD-cost:   25
c ---[10416]---> BDD-cost:   17
c ---[10414]---> BDD-cost:   25
c ---[10412]---> BDD-cost:   17
c ---[10410]---> BDD-cost:   25
c ---[10408]---> BDD-cost:   17
c ---[10406]---> BDD-cost:   17
c ---[10404]---> BDD-cost:   25
c ---[10402]---> BDD-cost:   17
c ---[10400]---> BDD-cost:   25
c ---[10398]---> BDD-cost:   17
c ---[10396]---> BDD-cost:   25
c ---[10394]---> BDD-cost:   17
c ---[10392]---> BDD-cost:   25
c ---[10390]---> BDD-cost:   17
c ---[10388]---> BDD-cost:   25
c ---[10386]---> BDD-cost:   17
c ---[10384]---> BDD-cost:   25
c ---[10382]---> BDD-cost:   17
c ---[10380]---> BDD-cost:   25
c ---[10378]---> BDD-cost:   17
c ---[10376]---> BDD-cost:   25
c ---[10374]---> BDD-cost:   17
c ---[10372]---> BDD-cost:   25
c ---[10370]---> BDD-cost:   17
c ---[10368]---> BDD-cost:   25
c ---[10366]---> BDD-cost:   17
c ---[10364]---> BDD-cost:   25
c ---[10362]---> BDD-cost:   17
c ---[10360]---> BDD-cost:   25
c ---[10358]---> BDD-cost:   17
c ---[10356]---> BDD-cost:   25
c ---[10354]---> BDD-cost:   17
c ---[10352]---> BDD-cost:   25
c ---[10350]---> BDD-cost:   17
c ---[10348]---> BDD-cost:   25
c ---[10346]---> BDD-cost:   17
c ---[10344]---> BDD-cost:   25
c ---[10342]---> BDD-cost:   17
c ---[10340]---> BDD-cost:   25
c ---[10338]---> BDD-cost:   17
c ---[10336]---> BDD-cost:   25
c ---[10334]---> BDD-cost:   17
c ---[10332]---> BDD-cost:   25
c ---[10330]---> BDD-cost:   17
c ---[10328]---> BDD-cost:   25
c ---[10326]---> BDD-cost:   17
c ---[10324]---> BDD-cost:   25
c ---[10322]---> BDD-cost:   17
c ---[10320]---> BDD-cost:   25
c ---[10318]---> BDD-cost:   17
c ---[10316]---> BDD-cost:   25
c ---[10314]---> BDD-cost:   17
c ---[10312]---> BDD-cost:   25
c ---[10310]---> BDD-cost:   17
c ---[10308]---> BDD-cost:   25
c ---[10306]---> BDD-cost:   17
c ---[10304]---> BDD-cost:   25
c ---[10302]---> BDD-cost:   17
c ---[10300]---> BDD-cost:   25
c ---[10298]---> BDD-cost:   17
c ---[10296]---> BDD-cost:   25
c ---[10294]---> BDD-cost:   17
c ---[10292]---> BDD-cost:   25
c ---[10290]---> BDD-cost:   17
c ---[10288]---> BDD-cost:   25
c ---[10286]---> BDD-cost:   17
c ---[10284]---> BDD-cost:   25
c ---[10282]---> BDD-cost:   17
c ---[10280]---> BDD-cost:   25
c ---[10278]---> BDD-cost:   17
c ---[10276]---> BDD-cost:   25
c ---[10274]---> BDD-cost:   17
c ---[10272]---> BDD-cost:   25
c ---[10270]---> BDD-cost:   17
c ---[10268]---> BDD-cost:   25
c ---[10266]---> BDD-cost:   17
c ---[10264]---> BDD-cost:   25
c ---[10262]---> BDD-cost:   17
c ---[10260]---> BDD-cost:   25
c ---[10258]---> BDD-cost:   17
c ---[10256]---> BDD-cost:   25
c ---[10254]---> BDD-cost:   17
c ---[10252]---> BDD-cost:   25
c ---[10250]---> BDD-cost:   17
c ---[10248]---> BDD-cost:   25
c ---[10246]---> BDD-cost:   17
c ---[10244]---> BDD-cost:   25
c ---[10242]---> BDD-cost:   17
c ---[10240]---> BDD-cost:   25
c ---[10238]---> BDD-cost:   17
c ---[10236]---> BDD-cost:   25
c ---[10234]---> BDD-cost:   17
c ---[10232]---> BDD-cost:   25
c ---[10230]---> BDD-cost:   17
c ---[10228]---> BDD-cost:   25
c ---[10226]---> BDD-cost:   17
c ---[10224]---> BDD-cost:   25
c ---[10222]---> BDD-cost:   17
c ---[10220]---> BDD-cost:   25
c ---[10218]---> BDD-cost:   17
c ---[10216]---> BDD-cost:   25
c ---[10214]---> BDD-cost:   17
c ---[10212]---> BDD-cost:   25
c ---[10210]---> BDD-cost:   25
c ---[10208]---> BDD-cost:   17
c ---[10206]---> BDD-cost:   25
c ---[10204]---> BDD-cost:   17
c ---[10202]---> BDD-cost:   25
c ---[10200]---> BDD-cost:   17
c ---[10198]---> BDD-cost:   25
c ---[10196]---> BDD-cost:   17
c ---[10194]---> BDD-cost:   25
c ---[10192]---> BDD-cost:   17
c ---[10190]---> BDD-cost:   25
c ---[10188]---> BDD-cost:   17
c ---[10186]---> BDD-cost:   25
c ---[10184]---> BDD-cost:   17
c ---[10182]---> BDD-cost:   25
c ---[10180]---> BDD-cost:   17
c ---[10178]---> BDD-cost:   25
c ---[10176]---> BDD-cost:   17
c ---[10174]---> BDD-cost:   25
c ---[10172]---> BDD-cost:   17
c ---[10170]---> BDD-cost:   25
c ---[10168]---> BDD-cost:   17
c ---[10166]---> BDD-cost:   25
c ---[10164]---> BDD-cost:   17
c ---[10162]---> BDD-cost:   25
c ---[10160]---> BDD-cost:   17
c ---[10158]---> BDD-cost:   25
c ---[10156]---> BDD-cost:   17
c ---[10154]---> BDD-cost:   25
c ---[10152]---> BDD-cost:   25
c ---[10150]---> BDD-cost:   17
c ---[10148]---> BDD-cost:   25
c ---[10146]---> BDD-cost:   17
c ---[10144]---> BDD-cost:   25
c ---[10142]---> BDD-cost:   17
c ---[10140]---> BDD-cost:   25
c ---[10138]---> BDD-cost:   17
c ---[10136]---> BDD-cost:   25
c ---[10134]---> BDD-cost:   17
c ---[10132]---> BDD-cost:   25
c ---[10130]---> BDD-cost:   17
c ---[10128]---> BDD-cost:   17
c ---[10126]---> BDD-cost:   25
c ---[10124]---> BDD-cost:   17
c ---[10122]---> BDD-cost:   25
c ---[10120]---> BDD-cost:   17
c ---[10118]---> BDD-cost:   25
c ---[10116]---> BDD-cost:   17
c ---[10114]---> BDD-cost:   25
c ---[10112]---> BDD-cost:   17
c ---[10110]---> BDD-cost:   25
c ---[10108]---> BDD-cost:   17
c ---[10106]---> BDD-cost:   25
c ---[10104]---> BDD-cost:   17
c ---[10102]---> BDD-cost:   25
c ---[10100]---> BDD-cost:   17
c ---[10098]---> BDD-cost:   25
c ---[10096]---> BDD-cost:   17
c ---[10094]---> BDD-cost:   25
c ---[10092]---> BDD-cost:   17
c ---[10090]---> BDD-cost:   25
c ---[10088]---> BDD-cost:   17
c ---[10086]---> BDD-cost:   25
c ---[10084]---> BDD-cost:   17
c ---[10082]---> BDD-cost:   25
c ---[10080]---> BDD-cost:   17
c ---[10078]---> BDD-cost:   25
c ---[10076]---> BDD-cost:   17
c ---[10074]---> BDD-cost:   25
c ---[10072]---> BDD-cost:   17
c ---[10070]---> BDD-cost:   17
c ---[10068]---> BDD-cost:   25
c ---[10066]---> BDD-cost:   17
c ---[10064]---> BDD-cost:   25
c ---[10062]---> BDD-cost:   17
c ---[10060]---> BDD-cost:   25
c ---[10058]---> BDD-cost:   17
c ---[10056]---> BDD-cost:   25
c ---[10054]---> BDD-cost:   17
c ---[10052]---> BDD-cost:   25
c ---[10050]---> BDD-cost:   17
c ---[10048]---> BDD-cost:   25
c ---[10046]---> BDD-cost:   17
c ---[10044]---> BDD-cost:   25
c ---[10042]---> BDD-cost:   17
c ---[10040]---> BDD-cost:   25
c ---[10038]---> BDD-cost:   17
c ---[10036]---> BDD-cost:   25
c ---[10034]---> BDD-cost:   17
c ---[10032]---> BDD-cost:   25
c ---[10030]---> BDD-cost:   17
c ---[10028]---> BDD-cost:   25
c ---[10026]---> BDD-cost:   17
c ---[10024]---> BDD-cost:   25
c ---[10022]---> BDD-cost:   17
c ---[10020]---> BDD-cost:   25
c ---[10018]---> BDD-cost:   17
c ---[10016]---> BDD-cost:   25
c ---[10014]---> BDD-cost:   17
c ---[10012]---> BDD-cost:   25
c ---[10010]---> BDD-cost:   17
c ---[10008]---> BDD-cost:   25
c ---[10006]---> BDD-cost:   17
c ---[10004]---> BDD-cost:   25
c ---[10002]---> BDD-cost:   17
c ---[10000]---> BDD-cost:   25
c ---[9998]---> BDD-cost:   17
c ---[9996]---> BDD-cost:   25
c ---[9994]---> BDD-cost:   17
c ---[9992]---> BDD-cost:   25
c ---[9990]---> BDD-cost:   17
c ---[9988]---> BDD-cost:   25
c ---[9986]---> BDD-cost:   17
c ---[9984]---> BDD-cost:   25
c ---[9982]---> BDD-cost:   17
c ---[9980]---> BDD-cost:   25
c ---[9978]---> BDD-cost:   17
c ---[9976]---> BDD-cost:   25
c ---[9974]---> BDD-cost:   17
c ---[9972]---> BDD-cost:   25
c ---[9970]---> BDD-cost:   17
c ---[9968]---> BDD-cost:   25
c ---[9966]---> BDD-cost:   17
c ---[9964]---> BDD-cost:   25
c ---[9962]---> BDD-cost:   17
c ---[9960]---> BDD-cost:   25
c ---[9958]---> BDD-cost:   17
c ---[9956]---> BDD-cost:   25
c ---[9954]---> BDD-cost:   17
c ---[9952]---> BDD-cost:   25
c ---[9950]---> BDD-cost:   17
c ---[9948]---> BDD-cost:   25
c ---[9946]---> BDD-cost:   17
c ---[9944]---> BDD-cost:   25
c ---[9942]---> BDD-cost:   17
c ---[9940]---> BDD-cost:   25
c ---[9938]---> BDD-cost:   17
c ---[9936]---> BDD-cost:   25
c ---[9934]---> BDD-cost:   17
c ---[9932]---> BDD-cost:   25
c ---[9930]---> BDD-cost:   17
c ---[9928]---> BDD-cost:   25
c ---[9926]---> BDD-cost:   17
c ---[9924]---> BDD-cost:   25
c ---[9922]---> BDD-cost:   17
c ---[9920]---> BDD-cost:   17
c ---[9918]---> BDD-cost:   25
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  191072   616174 |   63690       0        0     nan |  0.000 % |
c |       100 |  191000   615928 |   70059      90      837     9.3 |  2.406 % |
c |       250 |  190957   615781 |   77064     234     1255     5.4 |  2.423 % |
c |       475 |  190894   615567 |   84771     452     2000     4.4 |  2.453 % |
c |       812 |  190732   615022 |   93248     772     3004     3.9 |  2.528 % |
c |      1318 |  190571   614487 |  102573    1252     4633     3.7 |  2.600 % |
c |      2077 |  190497   614243 |  112830    1995     7416     3.7 |  2.635 % |
c |      3216 |  190380   613854 |  124113    3113    11772     3.8 |  2.687 % |
c |      4925 |  190272   613494 |  136525    4809    21987     4.6 |  2.735 % |
c |      7487 |  190126   613004 |  150177    7352    37487     5.1 |  2.802 % |
c |     11331 |  189934   612352 |  165195   11161    90879     8.1 |  2.889 % |
c |     17097 |  189559   611102 |  181715   16871   177777    10.5 |  3.051 % |
c |     25746 |  189512   610948 |  199886   25511   404008    15.8 |  3.074 % |
c |     38721 |  189385   610523 |  219875   38468  1258755    32.7 |  3.131 % |
c |     58182 |  189268   610134 |  241862   57910  1635523    28.2 |  3.183 % |
c |     87376 |  189268   610134 |  266048   87104  8363765    96.0 |  3.183 % |
c |    131166 |  189251   610073 |  292653  130892 13195753   100.8 |  3.188 % |
c |    196850 |  189216   609954 |  321919  196571 23756560   120.9 |  3.203 % |
c |    295377 |  189192   609872 |  354111  295093 30276393   102.6 |  3.211 % |
c |    443166 |  189117   609613 |  389522  104624  4341650    41.5 |  3.241 % |
c |    664850 |  189111   609593 |  428474  326307 19066116    58.4 |  3.243 % |
#### 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.90 0.98 0.91 2/54 21728
Raw data (stat): 21728 (runsolver) R 21727 10614 10613 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 481914513 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.0002 s]
Raw data (loadavg): 0.91 0.98 0.91 2/54 21730
Raw data (stat): 21728 (minisat+) R 21727 10614 10613 0 -1 0 4355 0 0 0 986 11 0 0 25 0 1 0 481914513 20926464 4210 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5109 4210 603 41 0 5068 0
vsize: 20436
[startup+20.0001 s]
Raw data (loadavg): 0.92 0.98 0.91 2/54 21730
Raw data (stat): 21728 (minisat+) R 21727 10614 10613 0 -1 0 4379 0 0 0 1986 12 0 0 25 0 1 0 481914513 21061632 4234 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5142 4234 603 41 0 5101 0
vsize: 20568
[startup+30.0003 s]
Raw data (loadavg): 0.94 0.98 0.91 2/54 21730
Raw data (stat): 21728 (minisat+) R 21727 10614 10613 0 -1 0 4409 0 0 0 2985 12 0 0 25 0 1 0 481914513 21061632 4264 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5142 4264 603 41 0 5101 0
vsize: 20568
[startup+40.0004 s]
Raw data (loadavg): 0.95 0.98 0.91 2/54 21730
Raw data (stat): 21728 (minisat+) R 21727 10614 10613 0 -1 0 4481 0 0 0 3984 13 0 0 25 0 1 0 481914513 21389312 4336 4294967295 134512640 134672761 3221224576 3221223700 134566043 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5222 4336 603 41 0 5181 0
vsize: 20888
[startup+50.0008 s]
Raw data (loadavg): 0.95 0.98 0.91 2/54 21730
Raw data (stat): 21728 (minisat+) R 21727 10614 10613 0 -1 0 4587 0 0 0 4984 13 0 0 25 0 1 0 481914513 21790720 4442 4294967295 134512640 134672761 3221224576 3221223700 134566071 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5320 4442 603 41 0 5279 0
vsize: 21280
[startup+60.0001 s]
Raw data (loadavg): 0.96 0.98 0.91 2/54 21730
Raw data (stat): 21728 (minisat+) R 21727 10614 10613 0 -1 0 4735 0 0 0 5983 14 0 0 25 0 1 0 481914513 22515712 4590 4294967295 134512640 134672761 3221224576 3221223744 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5497 4590 603 41 0 5456 0
vsize: 21988
[startup+70.0002 s]
Raw data (loadavg): 0.97 0.98 0.91 2/54 21730
Raw data (stat): 21728 (minisat+) R 21727 10614 10613 0 -1 0 5163 0 0 0 6982 15 0 0 25 0 1 0 481914513 24125440 5018 4294967295 134512640 134672761 3221224576 3221223748 134556646 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5890 5018 603 41 0 5849 0
vsize: 23560
[startup+80.0008 s]
Raw data (loadavg): 0.97 0.98 0.91 2/54 21730
Raw data (stat): 21728 (minisat+) R 21727 10614 10613 0 -1 0 5349 0 0 0 7982 15 0 0 25 0 1 0 481914513 25063424 5204 4294967295 134512640 134672761 3221224576 3221223532 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6119 5204 603 41 0 6078 0
vsize: 24476
[startup+90.0002 s]
Raw data (loadavg): 0.97 0.98 0.91 2/54 21730
Raw data (stat): 21728 (minisat+) R 21727 10614 10613 0 -1 0 5979 0 0 0 8980 17 0 0 25 0 1 0 481914513 27619328 5834 4294967295 134512640 134672761 3221224576 3221223700 134566082 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6743 5834 603 41 0 6702 0
vsize: 26972
[startup+100 s]
Raw data (loadavg): 0.98 0.98 0.91 2/54 21730
Raw data (stat): 21728 (minisat+) R 21727 10614 10613 0 -1 0 6229 0 0 0 9980 18 0 0 25 0 1 0 481914513 28565504 6084 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6974 6084 603 41 0 6933 0
vsize: 27896
[startup+110.001 s]
Raw data (loadavg): 0.98 0.98 0.91 2/54 21730
Raw data (stat): 21728 (minisat+) R 21727 10614 10613 0 -1 0 6452 0 0 0 10979 19 0 0 25 0 1 0 481914513 29507584 6307 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7204 6307 603 41 0 7163 0
vsize: 28816
[startup+120 s]
Raw data (loadavg): 0.98 0.98 0.91 2/54 21730
Raw data (stat): 21728 (minisat+) R 21727 10614 10613 0 -1 0 6923 0 0 0 11978 20 0 0 25 0 1 0 481914513 31395840 6778 4294967295 134512640 134672761 3221224576 3221223656 1075347118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7665 6778 603 41 0 7624 0
vsize: 30660
[startup+130 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 21730
Raw data (stat): 21728 (minisat+) R 21727 10614 10613 0 -1 0 7915 0 0 0 12976 22 0 0 25 0 1 0 481914513 35696640 7770 4294967295 134512640 134672761 3221224576 3221223680 134560289 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8715 7770 603 41 0 8674 0
vsize: 34860
[startup+140.001 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 21730
Raw data (stat): 21728 (minisat+) R 21727 10614 10613 0 -1 0 8846 0 0 0 13974 24 0 0 25 0 1 0 481914513 39583744 8701 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9664 8701 603 41 0 9623 0
vsize: 38656
[startup+150.001 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 21730
Raw data (stat): 21728 (minisat+) R 21727 10614 10613 0 -1 0 9720 0 0 0 14972 26 0 0 25 0 1 0 481914513 43032576 9575 4294967295 134512640 134672761 3221224576 3221223760 134559340 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10506 9575 603 41 0 10465 0
vsize: 42024
[startup+160.001 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 21730
Raw data (stat): 21728 (minisat+) R 21727 10614 10613 0 -1 0 10511 0 0 0 15970 28 0 0 25 0 1 0 481914513 46256128 10366 4294967295 134512640 134672761 3221224576 3221223760 134559498 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11293 10366 603 41 0 11252 0
vsize: 45172
[startup+170.001 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 21730
Raw data (stat): 21728 (minisat+) R 21727 10614 10613 0 -1 0 11276 0 0 0 16969 30 0 0 25 0 1 0 481914513 49471488 11131 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12078 11131 603 41 0 12037 0
vsize: 48312
[startup+180.001 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 21730
Raw data (stat): 21728 (minisat+) R 21727 10614 10613 0 -1 0 11999 0 0 0 17967 32 0 0 25 0 1 0 481914513 52445184 11854 4294967295 134512640 134672761 3221224576 3221223744 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12804 11854 603 41 0 12763 0
vsize: 51216
[startup+190.001 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 21730
Raw data (stat): 21728 (minisat+) R 21727 10614 10613 0 -1 0 12713 0 0 0 18966 33 0 0 25 0 1 0 481914513 55259136 12568 4294967295 134512640 134672761 3221224576 3221223724 134560552 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13491 12568 603 41 0 13450 0
vsize: 53964
[startup+200.002 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 21730
Raw data (stat): 21728 (minisat+) R 21727 10614 10613 0 -1 0 13351 0 0 0 19965 35 0 0 25 0 1 0 481914513 57946112 13206 4294967295 134512640 134672761 3221224576 3221223680 134560418 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14147 13206 603 41 0 14106 0
vsize: 56588
[startup+210.002 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 21730
Raw data (stat): 21728 (minisat+) R 21727 10614 10613 0 -1 0 13730 0 0 0 20964 35 0 0 25 0 1 0 481914513 59428864 13585 4294967295 134512640 134672761 3221224576 3221223576 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14509 13585 603 41 0 14468 0
vsize: 58036
[startup+220.002 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 21730
Raw data (stat): 21728 (minisat+) R 21727 10614 10613 0 -1 0 14325 0 0 0 21963 36 0 0 25 0 1 0 481914513 61857792 14180 4294967295 134512640 134672761 3221224576 3221223744 134560852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15102 14180 603 41 0 15061 0
vsize: 60408
[startup+230.003 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 21730
Raw data (stat): 21728 (minisat+) R 21727 10614 10613 0 -1 0 15406 0 0 0 22960 40 0 0 25 0 1 0 481914513 66306048 15261 4294967295 134512640 134672761 3221224576 3221223680 134559925 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16188 15261 603 41 0 16147 0
vsize: 64752
[startup+240.004 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 21730
Raw data (stat): 21728 (minisat+) R 21727 10614 10613 0 -1 0 16385 0 0 0 23958 42 0 0 25 0 1 0 481914513 70217728 16240 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17143 16240 603 41 0 17102 0
vsize: 68572
[startup+250.004 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 21730
Raw data (stat): 21728 (minisat+) R 21727 10614 10613 0 -1 0 17347 0 0 0 24956 44 0 0 25 0 1 0 481914513 74244096 17202 4294967295 134512640 134672761 3221224576 3221223680 134560154 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18126 17202 603 41 0 18085 0
vsize: 72504
[startup+260.004 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 21730
Raw data (stat): 21728 (minisat+) R 21727 10614 10613 0 -1 0 18151 0 0 0 25954 46 0 0 25 0 1 0 481914513 77467648 18006 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18913 18006 603 41 0 18872 0
vsize: 75652
[startup+270.003 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 21730
Raw data (stat): 21728 (minisat+) R 21727 10614 10613 0 -1 0 18432 0 0 0 26954 47 0 0 25 0 1 0 481914513 78540800 18287 4294967295 134512640 134672761 3221224576 3221223744 134561372 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19175 18287 603 41 0 19134 0
vsize: 76700
[startup+280.003 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 21730
Raw data (stat): 21728 (minisat+) R 21727 10614 10613 0 -1 0 18820 0 0 0 27953 47 0 0 25 0 1 0 481914513 80678912 18675 4294967295 134512640 134672761 3221224576 3221223744 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19697 18675 603 41 0 19656 0
vsize: 78788
[startup+290.003 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 21730
Raw data (stat): 21728 (minisat+) R 21727 10614 10613 0 -1 0 19578 0 0 0 28952 49 0 0 25 0 1 0 481914513 83779584 19433 4294967295 134512640 134672761 3221224576 3221223744 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20454 19433 603 41 0 20413 0
vsize: 81816
[startup+300.004 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 21730
Raw data (stat): 21728 (minisat+) R 21727 10614 10613 0 -1 0 20434 0 0 0 29949 52 0 0 25 0 1 0 481914513 87277568 20289 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21308 20289 603 41 0 21267 0
vsize: 85232
[startup+310.003 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 21732
Raw data (stat): 21728 (minisat+) R 21727 10614 10613 0 -1 0 20801 0 0 0 30948 53 0 0 25 0 1 0 481914513 88756224 20656 4294967295 134512640 134672761 3221224576 3221223744 134560855 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21669 20656 603 41 0 21628 0
vsize: 86676
[startup+320.003 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 21732
Raw data (stat): 21728 (minisat+) R 21727 10614 10613 0 -1 0 21643 0 0 0 31946 55 0 0 25 0 1 0 481914513 92110848 21498 4294967295 134512640 134672761 3221224576 3221223744 134561198 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22488 21498 603 41 0 22447 0
vsize: 89952
[startup+330.003 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 21732
Raw data (stat): 21728 (minisat+) R 21727 10614 10613 0 -1 0 22630 0 0 0 32944 57 0 0 25 0 1 0 481914513 96153600 22485 4294967295 134512640 134672761 3221224576 3221223576 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23475 22485 603 41 0 23434 0
vsize: 93900
[startup+340.003 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 21732
Raw data (stat): 21728 (minisat+) R 21727 10614 10613 0 -1 0 23524 0 0 0 33943 59 0 0 25 0 1 0 481914513 99778560 23379 4294967295 134512640 134672761 3221224576 3221223680 134559925 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24360 23379 603 41 0 24319 0
vsize: 97440
[startup+350.004 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 21732
Raw data (stat): 21728 (minisat+) R 21727 10614 10613 0 -1 0 24397 0 0 0 34940 62 0 0 25 0 1 0 481914513 103403520 24252 4294967295 134512640 134672761 3221224576 3221223576 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25245 24252 603 41 0 25204 0
vsize: 100980
[startup+360.005 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 21732
Raw data (stat): 21728 (minisat+) R 21727 10614 10613 0 -1 0 25263 0 0 0 35938 64 0 0 25 0 1 0 481914513 106897408 25118 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26098 25118 603 41 0 26057 0
vsize: 104392
[startup+370.005 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 21732
Raw data (stat): 21728 (minisat+) R 21727 10614 10613 0 -1 0 26082 0 0 0 36936 66 0 0 25 0 1 0 481914513 110260224 25937 4294967295 134512640 134672761 3221224576 3221223680 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26919 25937 603 41 0 26878 0
vsize: 107676
[startup+380.005 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 21732
Raw data (stat): 21728 (minisat+) R 21727 10614 10613 0 -1 0 26789 0 0 0 37934 68 0 0 25 0 1 0 481914513 113238016 26644 4294967295 134512640 134672761 3221224576 3221223680 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27646 26644 603 41 0 27605 0
vsize: 110584
[startup+390.006 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 21732
Raw data (stat): 21728 (minisat+) R 21727 10614 10613 0 -1 0 27476 0 0 0 38933 70 0 0 25 0 1 0 481914513 115937280 27331 4294967295 134512640 134672761 3221224576 3221223744 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28305 27331 603 41 0 28264 0
vsize: 113220
[startup+400.006 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 21732
Raw data (stat): 21728 (minisat+) R 21727 10614 10613 0 -1 0 28184 0 0 0 39931 72 0 0 25 0 1 0 481914513 118906880 28039 4294967295 134512640 134672761 3221224576 3221223680 134560246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29030 28039 603 41 0 28989 0
vsize: 116120
[startup+410.005 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 21732
Raw data (stat): 21728 (minisat+) R 21727 10614 10613 0 -1 0 28695 0 0 0 40929 74 0 0 25 0 1 0 481914513 120946688 28550 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29528 28550 603 41 0 29487 0
vsize: 118112
[startup+420.005 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 21732
Raw data (stat): 21728 (minisat+) R 21727 10614 10613 0 -1 0 29080 0 0 0 41928 75 0 0 25 0 1 0 481914513 122568704 28935 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29924 28935 603 41 0 29883 0
vsize: 119696
[startup+430.006 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 21732
Raw data (stat): 21728 (minisat+) R 21727 10614 10613 0 -1 0 29771 0 0 0 42926 78 0 0 25 0 1 0 481914513 125255680 29626 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30580 29626 603 41 0 30539 0
vsize: 122320
[startup+440.005 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 21732
Raw data (stat): 21728 (minisat+) R 21727 10614 10613 0 -1 0 30097 0 0 0 43925 78 0 0 25 0 1 0 481914513 126603264 29952 4294967295 134512640 134672761 3221224576 3221223680 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30909 29952 603 41 0 30868 0
vsize: 123636
[startup+450.006 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 21732
Raw data (stat): 21728 (minisat+) R 21727 10614 10613 0 -1 0 30626 0 0 0 44924 79 0 0 25 0 1 0 481914513 128761856 30481 4294967295 134512640 134672761 3221224576 3221223680 134559914 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31436 30481 603 41 0 31395 0
vsize: 125744
[startup+460.007 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 21732
Raw data (stat): 21728 (minisat+) R 21727 10614 10613 0 -1 0 31382 0 0 0 45922 81 0 0 25 0 1 0 481914513 131850240 31237 4294967295 134512640 134672761 3221224576 3221223744 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32190 31237 603 41 0 32149 0
vsize: 128760
[startup+470.006 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 21732
Raw data (stat): 21728 (minisat+) R 21727 10614 10613 0 -1 0 31990 0 0 0 46921 83 0 0 25 0 1 0 481914513 134402048 31845 4294967295 134512640 134672761 3221224576 3221223680 134559866 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32813 31846 603 41 0 32772 0
vsize: 131252
[startup+480.007 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 21732
Raw data (stat): 21728 (minisat+) R 21727 10614 10613 0 -1 0 32810 0 0 0 47919 85 0 0 25 0 1 0 481914513 137629696 32665 4294967295 134512640 134672761 3221224576 3221223532 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33601 32665 603 41 0 33560 0
vsize: 134404
[startup+490.008 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 21732
Raw data (stat): 21728 (minisat+) R 21727 10614 10613 0 -1 0 33626 0 0 0 48916 88 0 0 25 0 1 0 481914513 140980224 33481 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34419 33481 603 41 0 34378 0
vsize: 137676
[startup+500.008 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 21732
Raw data (stat): 21728 (minisat+) R 21727 10614 10613 0 -1 0 33987 0 0 0 49915 89 0 0 25 0 1 0 481914513 142458880 33842 4294967295 134512640 134672761 3221224576 3221223840 134562166 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34780 33842 603 41 0 34739 0
vsize: 139120
[startup+510.008 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 21732
Raw data (stat): 21728 (minisat+) R 21727 10614 10613 0 -1 0 34405 0 0 0 50914 90 0 0 25 0 1 0 481914513 144080896 34260 4294967295 134512640 134672761 3221224576 3221223744 134560858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35176 34260 603 41 0 35135 0
vsize: 140704
[startup+520.008 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 21732
Raw data (stat): 21728 (minisat+) R 21727 10614 10613 0 -1 0 34674 0 0 0 51914 91 0 0 25 0 1 0 481914513 145289216 34529 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35471 34529 603 41 0 35430 0
vsize: 141884
[startup+530.008 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 21732
Raw data (stat): 21728 (minisat+) R 21727 10614 10613 0 -1 0 34903 0 0 0 52913 92 0 0 25 0 1 0 481914513 146100224 34758 4294967295 134512640 134672761 3221224576 3221223744 134560948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35669 34759 603 41 0 35628 0
vsize: 142676
[startup+540.008 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 21732
Raw data (stat): 21728 (minisat+) R 21727 10614 10613 0 -1 0 35305 0 0 0 53912 93 0 0 25 0 1 0 481914513 147718144 35160 4294967295 134512640 134672761 3221224576 3221223744 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36064 35160 603 41 0 36023 0
vsize: 144256
[startup+550.009 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 21732
Raw data (stat): 21728 (minisat+) R 21727 10614 10613 0 -1 0 35881 0 0 0 54911 95 0 0 25 0 1 0 481914513 151105536 35736 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36891 35736 603 41 0 36850 0
vsize: 147564
[startup+560.009 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 21732
Raw data (stat): 21728 (minisat+) R 21727 10614 10613 0 -1 0 36257 0 0 0 55910 96 0 0 25 0 1 0 481914513 152674304 36112 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37274 36112 603 41 0 37233 0
vsize: 149096
[startup+570.009 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 21732
Raw data (stat): 21728 (minisat+) R 21727 10614 10613 0 -1 0 36614 0 0 0 56909 97 0 0 25 0 1 0 481914513 154152960 36469 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37635 36469 603 41 0 37594 0
vsize: 150540
[startup+580.009 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 21732
Raw data (stat): 21728 (minisat+) R 21727 10614 10613 0 -1 0 36909 0 0 0 57908 98 0 0 25 0 1 0 481914513 155369472 36764 4294967295 134512640 134672761 3221224576 3221223744 134560882 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37932 36764 603 41 0 37891 0
vsize: 151728
[startup+590.009 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 21732
Raw data (stat): 21728 (minisat+) R 21727 10614 10613 0 -1 0 37199 0 0 0 58907 99 0 0 25 0 1 0 481914513 156585984 37054 4294967295 134512640 134672761 3221224576 3221223748 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38229 37054 603 41 0 38188 0
vsize: 152916
[startup+600.01 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 21732
Raw data (stat): 21728 (minisat+) R 21727 10614 10613 0 -1 0 37477 0 0 0 59906 100 0 0 25 0 1 0 481914513 157675520 37332 4294967295 134512640 134672761 3221224576 3221223712 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38495 37332 603 41 0 38454 0
vsize: 153980
[startup+610.011 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 21732
Raw data (stat): 21728 (minisat+) R 21727 10614 10613 0 -1 0 37666 0 0 0 60905 101 0 0 25 0 1 0 481914513 158486528 37521 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38693 37521 603 41 0 38652 0
vsize: 154772
[startup+620.01 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 21732
Raw data (stat): 21728 (minisat+) R 21727 10614 10613 0 -1 0 38020 0 0 0 61904 102 0 0 25 0 1 0 481914513 159834112 37875 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39022 37875 603 41 0 38981 0
vsize: 156088
[startup+630.011 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 21732
Raw data (stat): 21728 (minisat+) R 21727 10614 10613 0 -1 0 38125 0 0 0 62904 103 0 0 25 0 1 0 481914513 160239616 37980 4294967295 134512640 134672761 3221224576 3221223700 134566049 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39121 37980 603 41 0 39080 0
vsize: 156484
[startup+640.011 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 21732
Raw data (stat): 21728 (minisat+) R 21727 10614 10613 0 -1 0 38474 0 0 0 63902 104 0 0 25 0 1 0 481914513 161718272 38329 4294967295 134512640 134672761 3221224576 3221223700 134566049 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39482 38329 603 41 0 39441 0
vsize: 157928
[startup+650.011 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 21732
Raw data (stat): 21728 (minisat+) R 21727 10614 10613 0 -1 0 39178 0 0 0 64901 106 0 0 25 0 1 0 481914513 164536320 39033 4294967295 134512640 134672761 3221224576 3221223744 134560895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40170 39033 603 41 0 40129 0
vsize: 160680
[startup+660.011 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 21732
Raw data (stat): 21728 (minisat+) R 21727 10614 10613 0 -1 0 39678 0 0 0 65899 107 0 0 25 0 1 0 481914513 166551552 39533 4294967295 134512640 134672761 3221224576 3221223744 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40662 39533 603 41 0 40621 0
vsize: 162648
[startup+670.011 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 21732
Raw data (stat): 21728 (minisat+) R 21727 10614 10613 0 -1 0 40086 0 0 0 66898 108 0 0 25 0 1 0 481914513 168300544 39941 4294967295 134512640 134672761 3221224576 3221223744 134560906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41089 39941 603 41 0 41048 0
vsize: 164356
[startup+680.012 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 21732
Raw data (stat): 21728 (minisat+) R 21727 10614 10613 0 -1 0 40465 0 0 0 67898 109 0 0 25 0 1 0 481914513 169779200 40320 4294967295 134512640 134672761 3221224576 3221223680 134559872 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41450 40320 603 41 0 41409 0
vsize: 165800
[startup+690.012 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 21732
Raw data (stat): 21728 (minisat+) R 21727 10614 10613 0 -1 0 40802 0 0 0 68898 109 0 0 25 0 1 0 481914513 171196416 40657 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41796 40657 603 41 0 41755 0
vsize: 167184
[startup+700.012 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 21732
Raw data (stat): 21728 (minisat+) R 21727 10614 10613 0 -1 0 41124 0 0 0 69897 110 0 0 25 0 1 0 481914513 172425216 40979 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42096 40979 603 41 0 42055 0
vsize: 168384
[startup+710.012 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 21732
Raw data (stat): 21728 (minisat+) R 21727 10614 10613 0 -1 0 41401 0 0 0 70896 111 0 0 25 0 1 0 481914513 173654016 41256 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42396 41256 603 41 0 42355 0
vsize: 169584
[startup+720.011 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 21732
Raw data (stat): 21728 (minisat+) R 21727 10614 10613 0 -1 0 41689 0 0 0 71895 112 0 0 25 0 1 0 481914513 174862336 41544 4294967295 134512640 134672761 3221224576 3221223744 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42691 41544 603 41 0 42650 0
vsize: 170764
[startup+730.012 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 21732
Raw data (stat): 21728 (minisat+) R 21727 10614 10613 0 -1 0 41966 0 0 0 72895 113 0 0 25 0 1 0 481914513 176062464 41821 4294967295 134512640 134672761 3221224576 3221223744 134561372 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42984 41821 603 41 0 42943 0
vsize: 171936
[startup+740.012 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 21732
Raw data (stat): 21728 (minisat+) R 21727 10614 10613 0 -1 0 41997 0 0 0 73895 113 0 0 25 0 1 0 481914513 176201728 41852 4294967295 134512640 134672761 3221224576 3221223700 134566100 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43018 41852 603 41 0 42977 0
vsize: 172072
[startup+750.012 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 21732
Raw data (stat): 21728 (minisat+) R 21727 10614 10613 0 -1 0 41997 0 0 0 74895 113 0 0 25 0 1 0 481914513 176201728 41852 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43018 41852 603 41 0 42977 0
vsize: 172072
[startup+760.013 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 21732
Raw data (stat): 21728 (minisat+) R 21727 10614 10613 0 -1 0 41997 0 0 0 75896 113 0 0 25 0 1 0 481914513 176201728 41852 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43018 41852 603 41 0 42977 0
vsize: 172072
[startup+770.013 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 21732
Raw data (stat): 21728 (minisat+) R 21727 10614 10613 0 -1 0 41997 0 0 0 76896 113 0 0 25 0 1 0 481914513 176201728 41852 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43018 41852 603 41 0 42977 0
vsize: 172072
[startup+780.013 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 21732
Raw data (stat): 21728 (minisat+) R 21727 10614 10613 0 -1 0 41997 0 0 0 77896 113 0 0 25 0 1 0 481914513 176201728 41852 4294967295 134512640 134672761 3221224576 3221223744 134560942 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43018 41852 603 41 0 42977 0
vsize: 172072
[startup+790.013 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 21732
Raw data (stat): 21728 (minisat+) R 21727 10614 10613 0 -1 0 41997 0 0 0 78896 113 0 0 25 0 1 0 481914513 176201728 41852 4294967295 134512640 134672761 3221224576 3221223744 134560852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43018 41852 603 41 0 42977 0
vsize: 172072
[startup+800.014 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 21732
Raw data (stat): 21728 (minisat+) R 21727 10614 10613 0 -1 0 41997 0 0 0 79896 113 0 0 25 0 1 0 481914513 176201728 41852 4294967295 134512640 134672761 3221224576 3221223680 134560529 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43018 41852 603 41 0 42977 0
vsize: 172072
[startup+810.013 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 21732
Raw data (stat): 21728 (minisat+) R 21727 10614 10613 0 -1 0 41997 0 0 0 80897 113 0 0 25 0 1 0 481914513 176201728 41852 4294967295 134512640 134672761 3221224576 3221223760 134558629 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43018 41852 603 41 0 42977 0
vsize: 172072
[startup+820.013 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 21732
Raw data (stat): 21728 (minisat+) R 21727 10614 10613 0 -1 0 41997 0 0 0 81897 113 0 0 25 0 1 0 481914513 176201728 41852 4294967295 134512640 134672761 3221224576 3221223776 134557903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43018 41852 603 41 0 42977 0
vsize: 172072
[startup+830.014 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 21732
Raw data (stat): 21728 (minisat+) R 21727 10614 10613 0 -1 0 41997 0 0 0 82897 113 0 0 25 0 1 0 481914513 176201728 41852 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43018 41852 603 41 0 42977 0
vsize: 172072
[startup+840.013 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 21732
Raw data (stat): 21728 (minisat+) R 21727 10614 10613 0 -1 0 41998 0 0 0 83897 113 0 0 25 0 1 0 481914513 176201728 41853 4294967295 134512640 134672761 3221224576 3221223776 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43018 41853 603 41 0 42977 0
vsize: 172072
[startup+850.014 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 21732
Raw data (stat): 21728 (minisat+) R 21727 10614 10613 0 -1 0 41998 0 0 0 84897 113 0 0 25 0 1 0 481914513 176201728 41853 4294967295 134512640 134672761 3221224576 3221223760 134558656 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43018 41853 603 41 0 42977 0
vsize: 172072
[startup+860.014 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 21732
Raw data (stat): 21728 (minisat+) R 21727 10614 10613 0 -1 0 41998 0 0 0 85897 113 0 0 25 0 1 0 481914513 176201728 41853 4294967295 134512640 134672761 3221224576 3221223744 134560888 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43018 41853 603 41 0 42977 0
vsize: 172072
[startup+870.013 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 21732
Raw data (stat): 21728 (minisat+) R 21727 10614 10613 0 -1 0 41998 0 0 0 86898 113 0 0 25 0 1 0 481914513 176201728 41853 4294967295 134512640 134672761 3221224576 3221223744 134564448 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43018 41853 603 41 0 42977 0
vsize: 172072
[startup+880.013 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 21732
Raw data (stat): 21728 (minisat+) R 21727 10614 10613 0 -1 0 41998 0 0 0 87898 113 0 0 25 0 1 0 481914513 176201728 41853 4294967295 134512640 134672761 3221224576 3221223700 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43018 41853 603 41 0 42977 0
vsize: 172072
[startup+890.013 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 21732
Raw data (stat): 21728 (minisat+) R 21727 10614 10613 0 -1 0 41998 0 0 0 88897 113 0 0 25 0 1 0 481914513 176201728 41853 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43018 41853 603 41 0 42977 0
vsize: 172072
[startup+900.014 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 21732
Raw data (stat): 21728 (minisat+) R 21727 10614 10613 0 -1 0 41998 0 0 0 89897 113 0 0 25 0 1 0 481914513 176201728 41853 4294967295 134512640 134672761 3221224576 3221223712 134560579 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43018 41853 603 41 0 42977 0
vsize: 172072
[startup+910.013 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 21732
Raw data (stat): 21728 (minisat+) R 21727 10614 10613 0 -1 0 41998 0 0 0 90897 113 0 0 25 0 1 0 481914513 176201728 41853 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43018 41853 603 41 0 42977 0
vsize: 172072
[startup+920.013 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 21732
Raw data (stat): 21728 (minisat+) R 21727 10614 10613 0 -1 0 41998 0 0 0 91897 113 0 0 25 0 1 0 481914513 176201728 41853 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43018 41853 603 41 0 42977 0
vsize: 172072
[startup+930.013 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 21732
Raw data (stat): 21728 (minisat+) R 21727 10614 10613 0 -1 0 41998 0 0 0 92898 113 0 0 25 0 1 0 481914513 176201728 41853 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43018 41853 603 41 0 42977 0
vsize: 172072
[startup+940.013 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 21732
Raw data (stat): 21728 (minisat+) R 21727 10614 10613 0 -1 0 41998 0 0 0 93898 113 0 0 25 0 1 0 481914513 176201728 41853 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43018 41853 603 41 0 42977 0
vsize: 172072
[startup+950.014 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 21732
Raw data (stat): 21728 (minisat+) R 21727 10614 10613 0 -1 0 41998 0 0 0 94898 113 0 0 25 0 1 0 481914513 176201728 41853 4294967295 134512640 134672761 3221224576 3221223680 134560381 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43018 41853 603 41 0 42977 0
vsize: 172072
[startup+960.014 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 21732
Raw data (stat): 21728 (minisat+) R 21727 10614 10613 0 -1 0 41998 0 0 0 95898 113 0 0 25 0 1 0 481914513 176201728 41853 4294967295 134512640 134672761 3221224576 3221223760 134559161 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43018 41853 603 41 0 42977 0
vsize: 172072
[startup+970.013 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 21732
Raw data (stat): 21728 (minisat+) R 21727 10614 10613 0 -1 0 41998 0 0 0 96898 113 0 0 25 0 1 0 481914513 176201728 41853 4294967295 134512640 134672761 3221224576 3221223712 134565056 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43018 41853 603 41 0 42977 0
vsize: 172072
[startup+980.014 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 21732
Raw data (stat): 21728 (minisat+) R 21727 10614 10613 0 -1 0 41998 0 0 0 97899 113 0 0 25 0 1 0 481914513 176201728 41853 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43018 41853 603 41 0 42977 0
vsize: 172072
[startup+990.013 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 21732
Raw data (stat): 21728 (minisat+) R 21727 10614 10613 0 -1 0 41998 0 0 0 98899 113 0 0 25 0 1 0 481914513 176201728 41853 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43018 41853 603 41 0 42977 0
vsize: 172072
[startup+1000.01 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 21732
Raw data (stat): 21728 (minisat+) R 21727 10614 10613 0 -1 0 41998 0 0 0 99899 113 0 0 25 0 1 0 481914513 176201728 41853 4294967295 134512640 134672761 3221224576 3221223744 134561205 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43018 41853 603 41 0 42977 0
vsize: 172072
[startup+1010.01 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 21732
Raw data (stat): 21728 (minisat+) R 21727 10614 10613 0 -1 0 41998 0 0 0 100899 113 0 0 25 0 1 0 481914513 176201728 41853 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43018 41853 603 41 0 42977 0
vsize: 172072
[startup+1020.01 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 21732
Raw data (stat): 21728 (minisat+) R 21727 10614 10613 0 -1 0 42000 0 0 0 101899 113 0 0 25 0 1 0 481914513 176201728 41855 4294967295 134512640 134672761 3221224576 3221223744 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43018 41855 603 41 0 42977 0
vsize: 172072
[startup+1030.01 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 21732
Raw data (stat): 21728 (minisat+) R 21727 10614 10613 0 -1 0 42000 0 0 0 102900 113 0 0 25 0 1 0 481914513 176201728 41855 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43018 41855 603 41 0 42977 0
vsize: 172072
[startup+1040.02 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 21732
Raw data (stat): 21728 (minisat+) R 21727 10614 10613 0 -1 0 42000 0 0 0 103900 113 0 0 25 0 1 0 481914513 176201728 41855 4294967295 134512640 134672761 3221224576 3221223744 134561198 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43018 41855 603 41 0 42977 0
vsize: 172072
[startup+1050.02 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 21732
Raw data (stat): 21728 (minisat+) R 21727 10614 10613 0 -1 0 42000 0 0 0 104900 113 0 0 25 0 1 0 481914513 176201728 41855 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43018 41855 603 41 0 42977 0
vsize: 172072
[startup+1060.02 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 21732
Raw data (stat): 21728 (minisat+) R 21727 10614 10613 0 -1 0 42000 0 0 0 105900 113 0 0 25 0 1 0 481914513 176201728 41855 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43018 41855 603 41 0 42977 0
vsize: 172072
[startup+1070.02 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 21732
Raw data (stat): 21728 (minisat+) R 21727 10614 10613 0 -1 0 42000 0 0 0 106900 113 0 0 25 0 1 0 481914513 176201728 41855 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43018 41855 603 41 0 42977 0
vsize: 172072
[startup+1080.02 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 21732
Raw data (stat): 21728 (minisat+) R 21727 10614 10613 0 -1 0 42000 0 0 0 107901 113 0 0 25 0 1 0 481914513 176201728 41855 4294967295 134512640 134672761 3221224576 3221223744 134561156 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43018 41855 603 41 0 42977 0
vsize: 172072
[startup+1090.02 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 21732
Raw data (stat): 21728 (minisat+) R 21727 10614 10613 0 -1 0 42001 0 0 0 108901 113 0 0 25 0 1 0 481914513 176201728 41856 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43018 41856 603 41 0 42977 0
vsize: 172072
[startup+1100.02 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 21732
Raw data (stat): 21728 (minisat+) R 21727 10614 10613 0 -1 0 42001 0 0 0 109901 113 0 0 25 0 1 0 481914513 176201728 41856 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43018 41856 603 41 0 42977 0
vsize: 172072
[startup+1110.02 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 21732
Raw data (stat): 21728 (minisat+) R 21727 10614 10613 0 -1 0 42001 0 0 0 110901 113 0 0 25 0 1 0 481914513 176201728 41856 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43018 41856 603 41 0 42977 0
vsize: 172072
[startup+1120.02 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 21732
Raw data (stat): 21728 (minisat+) R 21727 10614 10613 0 -1 0 42001 0 0 0 111901 113 0 0 25 0 1 0 481914513 176201728 41856 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43018 41856 603 41 0 42977 0
vsize: 172072
[startup+1130.02 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 21732
Raw data (stat): 21728 (minisat+) R 21727 10614 10613 0 -1 0 42001 0 0 0 112902 113 0 0 25 0 1 0 481914513 176201728 41856 4294967295 134512640 134672761 3221224576 3221223744 134560912 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43018 41856 603 41 0 42977 0
vsize: 172072
[startup+1140.02 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 21732
Raw data (stat): 21728 (minisat+) R 21727 10614 10613 0 -1 0 42001 0 0 0 113902 113 0 0 25 0 1 0 481914513 176201728 41856 4294967295 134512640 134672761 3221224576 3221223744 134561212 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43018 41856 603 41 0 42977 0
vsize: 172072
[startup+1150.02 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 21732
Raw data (stat): 21728 (minisat+) R 21727 10614 10613 0 -1 0 42001 0 0 0 114902 113 0 0 25 0 1 0 481914513 176201728 41856 4294967295 134512640 134672761 3221224576 3221223744 134560920 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43018 41856 603 41 0 42977 0
vsize: 172072
[startup+1160.02 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 21732
Raw data (stat): 21728 (minisat+) R 21727 10614 10613 0 -1 0 42001 0 0 0 115902 113 0 0 25 0 1 0 481914513 176201728 41856 4294967295 134512640 134672761 3221224576 3221223744 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43018 41856 603 41 0 42977 0
vsize: 172072
[startup+1170.02 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 21732
Raw data (stat): 21728 (minisat+) R 21727 10614 10613 0 -1 0 42001 0 0 0 116902 113 0 0 25 0 1 0 481914513 176201728 41856 4294967295 134512640 134672761 3221224576 3221223744 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43018 41856 603 41 0 42977 0
vsize: 172072
[startup+1180.02 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 21732
Raw data (stat): 21728 (minisat+) R 21727 10614 10613 0 -1 0 42001 0 0 0 117903 113 0 0 25 0 1 0 481914513 176201728 41856 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43018 41856 603 41 0 42977 0
vsize: 172072
[startup+1190.02 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 21732
Raw data (stat): 21728 (minisat+) R 21727 10614 10613 0 -1 0 42001 0 0 0 118902 113 0 0 25 0 1 0 481914513 176201728 41856 4294967295 134512640 134672761 3221224576 3221223700 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43018 41856 603 41 0 42977 0
vsize: 172072
[startup+1200.02 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 21732
Raw data (stat): 21728 (minisat+) R 21727 10614 10613 0 -1 0 42001 0 0 0 119902 113 0 0 25 0 1 0 481914513 176201728 41856 4294967295 134512640 134672761 3221224576 3221223748 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43018 41856 603 41 0 42977 0
vsize: 172072
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.1 s]
Raw data (loadavg): 0.99 0.98 0.91 1/54 21732
Raw data (stat): 21728 (minisat+) Z 21727 10614 10613 0 -1 12 42003 0 0 0 119902 121 0 0 25 0 1 0 481914513 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 0
Real time (s): 1200.1
CPU time (s): 1200.24
CPU user time (s): 1199.03
CPU system time (s): 1.21681
CPU usage (%): 100.012
Max. virtual memory (Kb): 172072
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####