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 5064

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.037
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:        890892 kB
Buffers:         33500 kB
Cached:          76264 kB
SwapCached:         56 kB
Active:          46332 kB
Inactive:        66452 kB
HighTotal:      131008 kB
HighFree:        50568 kB
LowTotal:       903652 kB
LowFree:        840324 kB
SwapTotal:     2097892 kB
SwapFree:      2097836 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           7028 kB
Slab:            25276 kB
Committed_AS:    63712 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-13 22:12:14 (client local time) WITH STATUS 0 IN 1200.27 SECONDS
stats: 3182 7 1200.27 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 |  163148   532482 |   54382       0        0     nan |  0.000 % |
c |       101 |  163065   532193 |   59820      88      845     9.6 |  2.413 % |
c |       251 |  163030   532076 |   65802     236     4687    19.9 |  2.428 % |
c |       476 |  162996   531958 |   72382     458     5330    11.6 |  2.448 % |
c |       813 |  162928   531722 |   79620     786     6347     8.1 |  2.483 % |
c |      1319 |  162913   531669 |   87582    1290     8281     6.4 |  2.488 % |
c |      2078 |  162778   531194 |   96341    2013    10744     5.3 |  2.553 % |
c |      3217 |  162672   530818 |  105975    3126    14721     4.7 |  2.608 % |
c |      4925 |  162597   530553 |  116572    4817    22980     4.8 |  2.647 % |
c |      7488 |  162472   530140 |  128229    7356    36896     5.0 |  2.712 % |
c |     11332 |  162366   529766 |  141052   11185    65646     5.9 |  2.765 % |
c |     17100 |  162104   528846 |  155158   16884   142757     8.5 |  2.894 % |
c |     25749 |  162095   528817 |  170674   25532   380187    14.9 |  2.899 % |
c |     38725 |  161875   528055 |  187741   38461   664055    17.3 |  3.006 % |
c |     58187 |  161751   527627 |  206515   57901  1199343    20.7 |  3.069 % |
c |     87379 |  161616   527167 |  227167   87062  1920374    22.1 |  3.133 % |
c |    131168 |  161597   527102 |  249883  130849  3438083    26.3 |  3.143 % |
c |    196852 |  161509   526798 |  274872  196513 13008984    66.2 |  3.186 % |
c |    295380 |  161509   526798 |  302359  295041 45134801   153.0 |  3.186 % |
#### 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.84 0.94 0.90 2/55 26295
Raw data (stat): 26295 (runsolver) R 26294 22929 22928 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 479329895 1052672 99 4294967295 134512640 135381576 3221224528 3221219772 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0015 s]
Raw data (loadavg): 0.87 0.94 0.90 2/55 26295
Raw data (stat): 26295 (minisat+) R 26294 22929 22928 0 -1 0 4176 0 0 0 986 12 0 0 25 0 1 0 479329895 20250624 4031 4294967295 134512640 134672761 3221224640 3221223812 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4944 4031 603 41 0 4903 0
vsize: 19776
[startup+20.002 s]
Raw data (loadavg): 0.89 0.94 0.90 2/55 26295
Raw data (stat): 26295 (minisat+) R 26294 22929 22928 0 -1 0 4201 0 0 0 1985 13 0 0 25 0 1 0 479329895 20385792 4056 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4977 4056 603 41 0 4936 0
vsize: 19908
[startup+30.0018 s]
Raw data (loadavg): 0.90 0.94 0.90 2/55 26295
Raw data (stat): 26295 (minisat+) R 26294 22929 22928 0 -1 0 4231 0 0 0 2985 13 0 0 25 0 1 0 479329895 20520960 4086 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5010 4086 603 41 0 4969 0
vsize: 20040
[startup+40.003 s]
Raw data (loadavg): 0.92 0.94 0.90 2/55 26295
Raw data (stat): 26295 (minisat+) R 26294 22929 22928 0 -1 0 4280 0 0 0 3985 14 0 0 25 0 1 0 479329895 20656128 4135 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5043 4135 603 41 0 5002 0
vsize: 20172
[startup+50.0034 s]
Raw data (loadavg): 0.93 0.94 0.90 2/55 26295
Raw data (stat): 26295 (minisat+) R 26294 22929 22928 0 -1 0 4343 0 0 0 4984 14 0 0 25 0 1 0 479329895 20926464 4198 4294967295 134512640 134672761 3221224640 3221223764 134566057 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5109 4198 603 41 0 5068 0
vsize: 20436
[startup+60.0042 s]
Raw data (loadavg): 0.94 0.95 0.90 2/55 26295
Raw data (stat): 26295 (minisat+) R 26294 22929 22928 0 -1 0 4740 0 0 0 5983 16 0 0 25 0 1 0 479329895 22614016 4595 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5521 4595 603 41 0 5480 0
vsize: 22084
[startup+70.0054 s]
Raw data (loadavg): 0.95 0.95 0.91 2/55 26295
Raw data (stat): 26295 (minisat+) R 26294 22929 22928 0 -1 0 4921 0 0 0 6982 17 0 0 25 0 1 0 479329895 23289856 4776 4294967295 134512640 134672761 3221224640 3221223824 134559340 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5686 4776 603 41 0 5645 0
vsize: 22744
[startup+80.0063 s]
Raw data (loadavg): 0.96 0.95 0.91 2/55 26295
Raw data (stat): 26295 (minisat+) R 26294 22929 22928 0 -1 0 5141 0 0 0 7981 18 0 0 25 0 1 0 479329895 24363008 4996 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5948 4996 603 41 0 5907 0
vsize: 23792
[startup+90.0066 s]
Raw data (loadavg): 0.96 0.95 0.91 2/55 26295
Raw data (stat): 26295 (minisat+) R 26294 22929 22928 0 -1 0 5374 0 0 0 8981 18 0 0 25 0 1 0 479329895 25309184 5229 4294967295 134512640 134672761 3221224640 3221223808 134560968 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6179 5229 603 41 0 6138 0
vsize: 24716
[startup+100.007 s]
Raw data (loadavg): 0.97 0.95 0.91 2/55 26295
Raw data (stat): 26295 (minisat+) R 26294 22929 22928 0 -1 0 5869 0 0 0 9979 20 0 0 25 0 1 0 479329895 27299840 5724 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6665 5724 603 41 0 6624 0
vsize: 26660
[startup+110.007 s]
Raw data (loadavg): 0.97 0.95 0.91 2/55 26295
Raw data (stat): 26295 (minisat+) R 26294 22929 22928 0 -1 0 6058 0 0 0 10978 21 0 0 25 0 1 0 479329895 27971584 5913 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6829 5913 603 41 0 6788 0
vsize: 27316
[startup+120.008 s]
Raw data (loadavg): 0.98 0.95 0.91 2/55 26295
Raw data (stat): 26295 (minisat+) R 26294 22929 22928 0 -1 0 6515 0 0 0 11976 23 0 0 25 0 1 0 479329895 30126080 6370 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7355 6370 603 41 0 7314 0
vsize: 29420
[startup+130.008 s]
Raw data (loadavg): 0.98 0.95 0.91 2/55 26295
Raw data (stat): 26295 (minisat+) R 26294 22929 22928 0 -1 0 6557 0 0 0 12976 24 0 0 25 0 1 0 479329895 30261248 6412 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7388 6412 603 41 0 7347 0
vsize: 29552
[startup+140.009 s]
Raw data (loadavg): 0.98 0.95 0.91 2/55 26295
Raw data (stat): 26295 (minisat+) R 26294 22929 22928 0 -1 0 6851 0 0 0 13975 25 0 0 25 0 1 0 479329895 31469568 6706 4294967295 134512640 134672761 3221224640 3221223812 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7683 6706 603 41 0 7642 0
vsize: 30732
[startup+150.01 s]
Raw data (loadavg): 0.98 0.95 0.91 2/55 26295
Raw data (stat): 26295 (minisat+) R 26294 22929 22928 0 -1 0 7412 0 0 0 14973 27 0 0 25 0 1 0 479329895 33636352 7267 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8212 7267 603 41 0 8171 0
vsize: 32848
[startup+160.01 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 26295
Raw data (stat): 26295 (minisat+) R 26294 22929 22928 0 -1 0 7878 0 0 0 15971 28 0 0 25 0 1 0 479329895 35524608 7733 4294967295 134512640 134672761 3221224640 3221223824 134558632 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8673 7733 603 41 0 8632 0
vsize: 34692
[startup+170.01 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 26295
Raw data (stat): 26295 (minisat+) R 26294 22929 22928 0 -1 0 8175 0 0 0 16971 29 0 0 25 0 1 0 479329895 36737024 8030 4294967295 134512640 134672761 3221224640 3221223776 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8969 8030 603 41 0 8928 0
vsize: 35876
[startup+180.01 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 26295
Raw data (stat): 26295 (minisat+) R 26294 22929 22928 0 -1 0 8437 0 0 0 17969 31 0 0 25 0 1 0 479329895 37801984 8292 4294967295 134512640 134672761 3221224640 3221223712 134553549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9229 8292 603 41 0 9188 0
vsize: 36916
[startup+190.011 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 26295
Raw data (stat): 26295 (minisat+) R 26294 22929 22928 0 -1 0 8856 0 0 0 18969 31 0 0 25 0 1 0 479329895 39944192 8711 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9752 8711 603 41 0 9711 0
vsize: 39008
[startup+200.011 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 26295
Raw data (stat): 26295 (minisat+) R 26294 22929 22928 0 -1 0 9239 0 0 0 19967 33 0 0 25 0 1 0 479329895 41562112 9094 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10147 9094 603 41 0 10106 0
vsize: 40588
[startup+210.012 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 26295
Raw data (stat): 26295 (minisat+) R 26294 22929 22928 0 -1 0 9797 0 0 0 20966 35 0 0 25 0 1 0 479329895 43859968 9652 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10708 9652 603 41 0 10667 0
vsize: 42832
[startup+220.012 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 26295
Raw data (stat): 26295 (minisat+) R 26294 22929 22928 0 -1 0 10329 0 0 0 21964 37 0 0 25 0 1 0 479329895 46014464 10184 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11234 10184 603 41 0 11193 0
vsize: 44936
[startup+230.012 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 26295
Raw data (stat): 26295 (minisat+) R 26294 22929 22928 0 -1 0 10860 0 0 0 22963 38 0 0 25 0 1 0 479329895 48173056 10715 4294967295 134512640 134672761 3221224640 3221223744 134559925 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11761 10715 603 41 0 11720 0
vsize: 47044
[startup+240.012 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 26297
Raw data (stat): 26295 (minisat+) R 26294 22929 22928 0 -1 0 11402 0 0 0 23961 40 0 0 25 0 1 0 479329895 50327552 11257 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12287 11257 603 41 0 12246 0
vsize: 49148
[startup+250.012 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 26297
Raw data (stat): 26295 (minisat+) R 26294 22929 22928 0 -1 0 11894 0 0 0 24959 42 0 0 25 0 1 0 479329895 52355072 11749 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12782 11749 603 41 0 12741 0
vsize: 51128
[startup+260.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26297
Raw data (stat): 26295 (minisat+) R 26294 22929 22928 0 -1 0 12389 0 0 0 25957 44 0 0 25 0 1 0 479329895 54382592 12244 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13277 12244 603 41 0 13236 0
vsize: 53108
[startup+270.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26297
Raw data (stat): 26295 (minisat+) R 26294 22929 22928 0 -1 0 12878 0 0 0 26955 46 0 0 25 0 1 0 479329895 56401920 12733 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13770 12733 603 41 0 13729 0
vsize: 55080
[startup+280.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26297
Raw data (stat): 26295 (minisat+) R 26294 22929 22928 0 -1 0 13341 0 0 0 27953 48 0 0 25 0 1 0 479329895 58290176 13196 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14231 13196 603 41 0 14190 0
vsize: 56924
[startup+290.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26297
Raw data (stat): 26295 (minisat+) R 26294 22929 22928 0 -1 0 13809 0 0 0 28951 50 0 0 25 0 1 0 479329895 60170240 13664 4294967295 134512640 134672761 3221224640 3221223808 134561201 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14690 13664 603 41 0 14649 0
vsize: 58760
[startup+300.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26297
Raw data (stat): 26295 (minisat+) R 26294 22929 22928 0 -1 0 14254 0 0 0 29950 51 0 0 25 0 1 0 479329895 62062592 14109 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15152 14109 603 41 0 15111 0
vsize: 60608
[startup+310.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26297
Raw data (stat): 26295 (minisat+) R 26294 22929 22928 0 -1 0 14719 0 0 0 30948 53 0 0 25 0 1 0 479329895 63942656 14574 4294967295 134512640 134672761 3221224640 3221223824 134559588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15611 14574 603 41 0 15570 0
vsize: 62444
[startup+320.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26297
Raw data (stat): 26295 (minisat+) R 26294 22929 22928 0 -1 0 15170 0 0 0 31947 55 0 0 25 0 1 0 479329895 65843200 15025 4294967295 134512640 134672761 3221224640 3221223824 134559354 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16075 15025 603 41 0 16034 0
vsize: 64300
[startup+330.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26297
Raw data (stat): 26295 (minisat+) R 26294 22929 22928 0 -1 0 15575 0 0 0 32945 57 0 0 25 0 1 0 479329895 67452928 15430 4294967295 134512640 134672761 3221224640 3221223744 134559949 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16468 15430 603 41 0 16427 0
vsize: 65872
[startup+340.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26297
Raw data (stat): 26295 (minisat+) R 26294 22929 22928 0 -1 0 15984 0 0 0 33943 59 0 0 25 0 1 0 479329895 69091328 15839 4294967295 134512640 134672761 3221224640 3221223744 134559937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16868 15839 603 41 0 16827 0
vsize: 67472
[startup+350.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26297
Raw data (stat): 26295 (minisat+) R 26294 22929 22928 0 -1 0 16398 0 0 0 34942 61 0 0 25 0 1 0 479329895 70705152 16253 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17262 16253 603 41 0 17221 0
vsize: 69048
[startup+360.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26297
Raw data (stat): 26295 (minisat+) R 26294 22929 22928 0 -1 0 16775 0 0 0 35940 62 0 0 25 0 1 0 479329895 72323072 16630 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17657 16630 603 41 0 17616 0
vsize: 70628
[startup+370.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26297
Raw data (stat): 26295 (minisat+) R 26294 22929 22928 0 -1 0 17196 0 0 0 36938 64 0 0 25 0 1 0 479329895 74104832 17051 4294967295 134512640 134672761 3221224640 3221223744 134560218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18092 17051 603 41 0 18051 0
vsize: 72368
[startup+380.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26297
Raw data (stat): 26295 (minisat+) R 26294 22929 22928 0 -1 0 17601 0 0 0 37937 66 0 0 25 0 1 0 479329895 75739136 17456 4294967295 134512640 134672761 3221224640 3221223808 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18491 17456 603 41 0 18450 0
vsize: 73964
[startup+390.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26297
Raw data (stat): 26295 (minisat+) R 26294 22929 22928 0 -1 0 18117 0 0 0 38936 67 0 0 25 0 1 0 479329895 77897728 17972 4294967295 134512640 134672761 3221224640 3221223808 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19018 17972 603 41 0 18977 0
vsize: 76072
[startup+400.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26297
Raw data (stat): 26295 (minisat+) R 26294 22929 22928 0 -1 0 18630 0 0 0 39934 68 0 0 25 0 1 0 479329895 79921152 18485 4294967295 134512640 134672761 3221224640 3221223808 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19512 18485 603 41 0 19471 0
vsize: 78048
[startup+410.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26297
Raw data (stat): 26295 (minisat+) R 26294 22929 22928 0 -1 0 19046 0 0 0 40933 70 0 0 25 0 1 0 479329895 81539072 18901 4294967295 134512640 134672761 3221224640 3221223796 134564777 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19907 18901 603 41 0 19866 0
vsize: 79628
[startup+420.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26297
Raw data (stat): 26295 (minisat+) R 26294 22929 22928 0 -1 0 19349 0 0 0 41932 71 0 0 25 0 1 0 479329895 82755584 19204 4294967295 134512640 134672761 3221224640 3221223808 134561148 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20204 19204 603 41 0 20163 0
vsize: 80816
[startup+430.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26297
Raw data (stat): 26295 (minisat+) R 26294 22929 22928 0 -1 0 19685 0 0 0 42931 72 0 0 25 0 1 0 479329895 84107264 19540 4294967295 134512640 134672761 3221224640 3221223808 134560855 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20534 19540 603 41 0 20493 0
vsize: 82136
[startup+440.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26297
Raw data (stat): 26295 (minisat+) R 26294 22929 22928 0 -1 0 20417 0 0 0 43929 75 0 0 25 0 1 0 479329895 87199744 20272 4294967295 134512640 134672761 3221224640 3221223824 134558930 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21289 20272 603 41 0 21248 0
vsize: 85156
[startup+450.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26297
Raw data (stat): 26295 (minisat+) R 26294 22929 22928 0 -1 0 21088 0 0 0 44927 76 0 0 25 0 1 0 479329895 89899008 20943 4294967295 134512640 134672761 3221224640 3221223744 134560289 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21948 20943 603 41 0 21907 0
vsize: 87792
[startup+460.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26297
Raw data (stat): 26295 (minisat+) R 26294 22929 22928 0 -1 0 21721 0 0 0 45925 79 0 0 25 0 1 0 479329895 92446720 21576 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22570 21576 603 41 0 22529 0
vsize: 90280
[startup+470.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26297
Raw data (stat): 26295 (minisat+) R 26294 22929 22928 0 -1 0 22353 0 0 0 46923 80 0 0 25 0 1 0 479329895 95002624 22208 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23194 22208 603 41 0 23153 0
vsize: 92776
[startup+480.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26350
Raw data (stat): 26295 (minisat+) R 26294 22929 22928 0 -1 0 23019 0 0 0 47916 87 0 0 25 0 1 0 479329895 97701888 22874 4294967295 134512640 134672761 3221224640 3221223596 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23853 22874 603 41 0 23812 0
vsize: 95412
[startup+490.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26350
Raw data (stat): 26295 (minisat+) R 26294 22929 22928 0 -1 0 23651 0 0 0 48915 89 0 0 25 0 1 0 479329895 100401152 23506 4294967295 134512640 134672761 3221224640 3221223744 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24512 23506 603 41 0 24471 0
vsize: 98048
[startup+500.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26350
Raw data (stat): 26295 (minisat+) R 26294 22929 22928 0 -1 0 24360 0 0 0 49913 91 0 0 25 0 1 0 479329895 103239680 24215 4294967295 134512640 134672761 3221224640 3221223596 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25205 24215 603 41 0 25164 0
vsize: 100820
[startup+510.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26350
Raw data (stat): 26295 (minisat+) R 26294 22929 22928 0 -1 0 25045 0 0 0 50910 93 0 0 25 0 1 0 479329895 106074112 24900 4294967295 134512640 134672761 3221224640 3221223744 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25897 24900 603 41 0 25856 0
vsize: 103588
[startup+520.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26350
Raw data (stat): 26295 (minisat+) R 26294 22929 22928 0 -1 0 25692 0 0 0 51909 95 0 0 25 0 1 0 479329895 108650496 25547 4294967295 134512640 134672761 3221224640 3221223744 134560218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26526 25547 603 41 0 26485 0
vsize: 106104
[startup+530.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26350
Raw data (stat): 26295 (minisat+) R 26294 22929 22928 0 -1 0 26326 0 0 0 52907 97 0 0 25 0 1 0 479329895 111218688 26181 4294967295 134512640 134672761 3221224640 3221223744 134560405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27153 26181 603 41 0 27112 0
vsize: 108612
[startup+540.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26352
Raw data (stat): 26295 (minisat+) R 26294 22929 22928 0 -1 0 26971 0 0 0 53906 99 0 0 25 0 1 0 479329895 113917952 26826 4294967295 134512640 134672761 3221224640 3221223808 134560882 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27812 26826 603 41 0 27771 0
vsize: 111248
[startup+550.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26354
Raw data (stat): 26295 (minisat+) R 26294 22929 22928 0 -1 0 27610 0 0 0 54904 101 0 0 25 0 1 0 479329895 116477952 27465 4294967295 134512640 134672761 3221224640 3221223808 134560808 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28437 27465 603 41 0 28396 0
vsize: 113748
[startup+560.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26354
Raw data (stat): 26295 (minisat+) R 26294 22929 22928 0 -1 0 28265 0 0 0 55902 103 0 0 25 0 1 0 479329895 119177216 28120 4294967295 134512640 134672761 3221224640 3221223808 134560895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29096 28120 603 41 0 29055 0
vsize: 116384
[startup+570.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26354
Raw data (stat): 26295 (minisat+) R 26294 22929 22928 0 -1 0 28851 0 0 0 56900 105 0 0 25 0 1 0 479329895 121593856 28706 4294967295 134512640 134672761 3221224640 3221223808 134561148 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29686 28706 603 41 0 29645 0
vsize: 118744
[startup+580.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26354
Raw data (stat): 26295 (minisat+) R 26294 22929 22928 0 -1 0 29399 0 0 0 57899 106 0 0 25 0 1 0 479329895 123891712 29254 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30247 29254 603 41 0 30206 0
vsize: 120988
[startup+590.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26354
Raw data (stat): 26295 (minisat+) R 26294 22929 22928 0 -1 0 29943 0 0 0 58898 107 0 0 25 0 1 0 479329895 126058496 29798 4294967295 134512640 134672761 3221224640 3221223744 134560506 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30776 29798 603 41 0 30735 0
vsize: 123104
[startup+600.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26354
Raw data (stat): 26295 (minisat+) R 26294 22929 22928 0 -1 0 30510 0 0 0 59897 109 0 0 25 0 1 0 479329895 128475136 30365 4294967295 134512640 134672761 3221224640 3221223808 134560917 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31366 30365 603 41 0 31325 0
vsize: 125464
[startup+610.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26354
Raw data (stat): 26295 (minisat+) R 26294 22929 22928 0 -1 0 31046 0 0 0 60895 111 0 0 25 0 1 0 479329895 130629632 30901 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31892 30901 603 41 0 31851 0
vsize: 127568
[startup+620.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26354
Raw data (stat): 26295 (minisat+) R 26294 22929 22928 0 -1 0 31605 0 0 0 61894 112 0 0 25 0 1 0 479329895 132907008 31460 4294967295 134512640 134672761 3221224640 3221223808 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32448 31460 603 41 0 32407 0
vsize: 129792
[startup+630.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26354
Raw data (stat): 26295 (minisat+) R 26294 22929 22928 0 -1 0 32226 0 0 0 62893 113 0 0 25 0 1 0 479329895 135450624 32081 4294967295 134512640 134672761 3221224640 3221223808 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33069 32081 603 41 0 33028 0
vsize: 132276
[startup+640.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26354
Raw data (stat): 26295 (minisat+) R 26294 22929 22928 0 -1 0 32748 0 0 0 63892 114 0 0 25 0 1 0 479329895 137617408 32603 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33598 32603 603 41 0 33557 0
vsize: 134392
[startup+650.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26354
Raw data (stat): 26295 (minisat+) R 26294 22929 22928 0 -1 0 33275 0 0 0 64891 115 0 0 25 0 1 0 479329895 139767808 33130 4294967295 134512640 134672761 3221224640 3221223744 134560252 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34123 33130 603 41 0 34082 0
vsize: 136492
[startup+660.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26354
Raw data (stat): 26295 (minisat+) R 26294 22929 22928 0 -1 0 33838 0 0 0 65890 117 0 0 25 0 1 0 479329895 142045184 33693 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34679 33693 603 41 0 34638 0
vsize: 138716
[startup+670.027 s]
Raw data (loadavg): 0.99 0.97 0.91 3/55 26354
Raw data (stat): 26295 (minisat+) R 26294 22929 22928 0 -1 0 34388 0 0 0 66889 118 0 0 25 0 1 0 479329895 144330752 34243 4294967295 134512640 134672761 3221224640 3221223808 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35237 34243 603 41 0 35196 0
vsize: 140948
[startup+680.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26354
Raw data (stat): 26295 (minisat+) R 26294 22929 22928 0 -1 0 34998 0 0 0 67887 120 0 0 25 0 1 0 479329895 146763776 34853 4294967295 134512640 134672761 3221224640 3221223744 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35831 34853 603 41 0 35790 0
vsize: 143324
[startup+690.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26354
Raw data (stat): 26295 (minisat+) R 26294 22929 22928 0 -1 0 35557 0 0 0 68886 121 0 0 25 0 1 0 479329895 149114880 35412 4294967295 134512640 134672761 3221224640 3221223808 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36405 35412 603 41 0 36364 0
vsize: 145620
[startup+700.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26354
Raw data (stat): 26295 (minisat+) R 26294 22929 22928 0 -1 0 36070 0 0 0 69885 122 0 0 25 0 1 0 479329895 151265280 35925 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36930 35925 603 41 0 36889 0
vsize: 147720
[startup+710.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26354
Raw data (stat): 26295 (minisat+) R 26294 22929 22928 0 -1 0 36586 0 0 0 70884 123 0 0 25 0 1 0 479329895 153288704 36441 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37424 36441 603 41 0 37383 0
vsize: 149696
[startup+720.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26354
Raw data (stat): 26295 (minisat+) R 26294 22929 22928 0 -1 0 37092 0 0 0 71883 124 0 0 25 0 1 0 479329895 155451392 36947 4294967295 134512640 134672761 3221224640 3221223744 134560136 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37952 36947 603 41 0 37911 0
vsize: 151808
[startup+730.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26354
Raw data (stat): 26295 (minisat+) R 26294 22929 22928 0 -1 0 37594 0 0 0 72883 125 0 0 25 0 1 0 479329895 158535680 37449 4294967295 134512640 134672761 3221224640 3221223744 134559964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38705 37449 603 41 0 38664 0
vsize: 154820
[startup+740.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26354
Raw data (stat): 26295 (minisat+) R 26294 22929 22928 0 -1 0 38044 0 0 0 73881 127 0 0 25 0 1 0 479329895 160419840 37899 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39165 37899 603 41 0 39124 0
vsize: 156660
[startup+750.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26354
Raw data (stat): 26295 (minisat+) R 26294 22929 22928 0 -1 0 38481 0 0 0 74880 128 0 0 25 0 1 0 479329895 162172928 38336 4294967295 134512640 134672761 3221224640 3221223808 134560852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39593 38336 603 41 0 39552 0
vsize: 158372
[startup+760.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26354
Raw data (stat): 26295 (minisat+) R 26294 22929 22928 0 -1 0 38972 0 0 0 75879 129 0 0 25 0 1 0 479329895 164204544 38827 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40089 38827 603 41 0 40048 0
vsize: 160356
[startup+770.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26354
Raw data (stat): 26295 (minisat+) R 26294 22929 22928 0 -1 0 39484 0 0 0 76878 131 0 0 25 0 1 0 479329895 166219776 39339 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40581 39339 603 41 0 40540 0
vsize: 162324
[startup+780.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26354
Raw data (stat): 26295 (minisat+) R 26294 22929 22928 0 -1 0 39964 0 0 0 77876 133 0 0 25 0 1 0 479329895 168230912 39819 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41072 39819 603 41 0 41031 0
vsize: 164288
[startup+790.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26356
Raw data (stat): 26295 (minisat+) R 26294 22929 22928 0 -1 0 40402 0 0 0 78876 134 0 0 25 0 1 0 479329895 169975808 40257 4294967295 134512640 134672761 3221224640 3221223744 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41498 40257 603 41 0 41457 0
vsize: 165992
[startup+800.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26356
Raw data (stat): 26295 (minisat+) R 26294 22929 22928 0 -1 0 40807 0 0 0 79875 134 0 0 25 0 1 0 479329895 171581440 40662 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41890 40662 603 41 0 41849 0
vsize: 167560
[startup+810.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26356
Raw data (stat): 26295 (minisat+) R 26294 22929 22928 0 -1 0 41238 0 0 0 80874 136 0 0 25 0 1 0 479329895 173465600 41093 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42350 41093 603 41 0 42309 0
vsize: 169400
[startup+820.031 s]
Raw data (loadavg): 0.99 0.97 0.91 3/55 26356
Raw data (stat): 26295 (minisat+) R 26294 22929 22928 0 -1 0 41676 0 0 0 81872 138 0 0 25 0 1 0 479329895 175226880 41531 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42780 41531 603 41 0 42739 0
vsize: 171120
[startup+830.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26356
Raw data (stat): 26295 (minisat+) R 26294 22929 22928 0 -1 0 42123 0 0 0 82871 139 0 0 25 0 1 0 479329895 176975872 41978 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43207 41978 603 41 0 43166 0
vsize: 172828
[startup+840.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26358
Raw data (stat): 26295 (minisat+) R 26294 22929 22928 0 -1 0 42583 0 0 0 83871 139 0 0 25 0 1 0 479329895 178855936 42438 4294967295 134512640 134672761 3221224640 3221223744 134560218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43666 42438 603 41 0 43625 0
vsize: 174664
[startup+850.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26358
Raw data (stat): 26295 (minisat+) R 26294 22929 22928 0 -1 0 43008 0 0 0 84870 141 0 0 25 0 1 0 479329895 180600832 42863 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44092 42863 603 41 0 44051 0
vsize: 176368
[startup+860.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26358
Raw data (stat): 26295 (minisat+) R 26294 22929 22928 0 -1 0 43458 0 0 0 85870 141 0 0 25 0 1 0 479329895 182484992 43313 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44552 43313 603 41 0 44511 0
vsize: 178208
[startup+870.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26358
Raw data (stat): 26295 (minisat+) R 26294 22929 22928 0 -1 0 43898 0 0 0 86869 142 0 0 25 0 1 0 479329895 184250368 43753 4294967295 134512640 134672761 3221224640 3221223776 134560677 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44983 43753 603 41 0 44942 0
vsize: 179932
[startup+880.038 s]
Raw data (loadavg): 0.99 0.97 0.91 3/55 26358
Raw data (stat): 26295 (minisat+) R 26294 22929 22928 0 -1 0 44375 0 0 0 87868 144 0 0 25 0 1 0 479329895 186261504 44230 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45474 44230 603 41 0 45433 0
vsize: 181896
[startup+890.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26358
Raw data (stat): 26295 (minisat+) R 26294 22929 22928 0 -1 0 44848 0 0 0 88867 145 0 0 25 0 1 0 479329895 188182528 44703 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45943 44703 603 41 0 45902 0
vsize: 183772
[startup+900.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26358
Raw data (stat): 26295 (minisat+) R 26294 22929 22928 0 -1 0 45283 0 0 0 89866 145 0 0 25 0 1 0 479329895 190070784 45138 4294967295 134512640 134672761 3221224640 3221223744 134560134 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 46404 45138 603 41 0 46363 0
vsize: 185616
[startup+910.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26358
Raw data (stat): 26295 (minisat+) R 26294 22929 22928 0 -1 0 45686 0 0 0 90865 147 0 0 25 0 1 0 479329895 191684608 45541 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 46798 45541 603 41 0 46757 0
vsize: 187192
[startup+920.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26358
Raw data (stat): 26295 (minisat+) R 26294 22929 22928 0 -1 0 46115 0 0 0 91865 148 0 0 25 0 1 0 479329895 193429504 45970 4294967295 134512640 134672761 3221224640 3221223808 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 47224 45970 603 41 0 47183 0
vsize: 188896
[startup+930.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26358
Raw data (stat): 26295 (minisat+) R 26294 22929 22928 0 -1 0 46539 0 0 0 92863 149 0 0 25 0 1 0 479329895 195174400 46394 4294967295 134512640 134672761 3221224640 3221223808 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 47650 46394 603 41 0 47609 0
vsize: 190600
[startup+940.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26358
Raw data (stat): 26295 (minisat+) R 26294 22929 22928 0 -1 0 46978 0 0 0 93862 150 0 0 25 0 1 0 479329895 196915200 46833 4294967295 134512640 134672761 3221224640 3221223744 134560514 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48075 46833 603 41 0 48034 0
vsize: 192300
[startup+950.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26358
Raw data (stat): 26295 (minisat+) R 26294 22929 22928 0 -1 0 47366 0 0 0 94862 151 0 0 25 0 1 0 479329895 198565888 47221 4294967295 134512640 134672761 3221224640 3221223808 134560864 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48478 47221 603 41 0 48437 0
vsize: 193912
[startup+960.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26358
Raw data (stat): 26295 (minisat+) R 26294 22929 22928 0 -1 0 47768 0 0 0 95861 152 0 0 25 0 1 0 479329895 200179712 47623 4294967295 134512640 134672761 3221224640 3221223744 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48872 47623 603 41 0 48831 0
vsize: 195488
[startup+970.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26358
Raw data (stat): 26295 (minisat+) R 26294 22929 22928 0 -1 0 48167 0 0 0 96861 152 0 0 25 0 1 0 479329895 201916416 48022 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49296 48022 603 41 0 49255 0
vsize: 197184
[startup+980.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26358
Raw data (stat): 26295 (minisat+) R 26294 22929 22928 0 -1 0 48647 0 0 0 97860 154 0 0 25 0 1 0 479329895 203800576 48502 4294967295 134512640 134672761 3221224640 3221223808 134560937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49756 48502 603 41 0 49715 0
vsize: 199024
[startup+990.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26358
Raw data (stat): 26295 (minisat+) R 26294 22929 22928 0 -1 0 49066 0 0 0 98859 154 0 0 25 0 1 0 479329895 205422592 48921 4294967295 134512640 134672761 3221224640 3221223788 134560552 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 50152 48921 603 41 0 50111 0
vsize: 200608
[startup+1000.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26358
Raw data (stat): 26295 (minisat+) R 26294 22929 22928 0 -1 0 49426 0 0 0 99858 155 0 0 25 0 1 0 479329895 207056896 49281 4294967295 134512640 134672761 3221224640 3221223808 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 50551 49281 603 41 0 50510 0
vsize: 202204
[startup+1010.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26358
Raw data (stat): 26295 (minisat+) R 26294 22929 22928 0 -1 0 49845 0 0 0 100857 157 0 0 25 0 1 0 479329895 208674816 49700 4294967295 134512640 134672761 3221224640 3221223744 134559925 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 50946 49700 603 41 0 50905 0
vsize: 203784
[startup+1020.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26358
Raw data (stat): 26295 (minisat+) R 26294 22929 22928 0 -1 0 50297 0 0 0 101856 158 0 0 25 0 1 0 479329895 210575360 50152 4294967295 134512640 134672761 3221224640 3221223808 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 51410 50152 603 41 0 51369 0
vsize: 205640
[startup+1030.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26358
Raw data (stat): 26295 (minisat+) R 26294 22929 22928 0 -1 0 50773 0 0 0 102854 160 0 0 25 0 1 0 479329895 212463616 50628 4294967295 134512640 134672761 3221224640 3221223808 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 51871 50628 603 41 0 51830 0
vsize: 207484
[startup+1040.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26358
Raw data (stat): 26295 (minisat+) R 26294 22929 22928 0 -1 0 51212 0 0 0 103853 161 0 0 25 0 1 0 479329895 214351872 51067 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 52332 51067 603 41 0 52291 0
vsize: 209328
[startup+1050.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26358
Raw data (stat): 26295 (minisat+) R 26294 22929 22928 0 -1 0 51553 0 0 0 104853 162 0 0 25 0 1 0 479329895 215699456 51408 4294967295 134512640 134672761 3221224640 3221223640 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 52661 51408 603 41 0 52620 0
vsize: 210644
[startup+1060.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26358
Raw data (stat): 26295 (minisat+) R 26294 22929 22928 0 -1 0 51907 0 0 0 105852 163 0 0 25 0 1 0 479329895 217051136 51762 4294967295 134512640 134672761 3221224640 3221223808 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 52991 51762 603 41 0 52950 0
vsize: 211964
[startup+1070.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26358
Raw data (stat): 26295 (minisat+) R 26294 22929 22928 0 -1 0 52184 0 0 0 106851 164 0 0 25 0 1 0 479329895 218136576 52039 4294967295 134512640 134672761 3221224640 3221223744 134554677 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 53256 52039 603 41 0 53215 0
vsize: 213024
[startup+1080.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26358
Raw data (stat): 26295 (minisat+) R 26294 22929 22928 0 -1 0 52184 0 0 0 107851 164 0 0 25 0 1 0 479329895 218136576 52039 4294967295 134512640 134672761 3221224640 3221223596 1075350790 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 53256 52039 603 41 0 53215 0
vsize: 213024
[startup+1090.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26358
Raw data (stat): 26295 (minisat+) R 26294 22929 22928 0 -1 0 52184 0 0 0 108851 164 0 0 25 0 1 0 479329895 218136576 52039 4294967295 134512640 134672761 3221224640 3221223792 134565076 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 53256 52039 603 41 0 53215 0
vsize: 213024
[startup+1100.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26358
Raw data (stat): 26295 (minisat+) R 26294 22929 22928 0 -1 0 52184 0 0 0 109851 164 0 0 25 0 1 0 479329895 218136576 52039 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 53256 52039 603 41 0 53215 0
vsize: 213024
[startup+1110.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26358
Raw data (stat): 26295 (minisat+) R 26294 22929 22928 0 -1 0 52184 0 0 0 110851 164 0 0 25 0 1 0 479329895 218136576 52039 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 53256 52039 603 41 0 53215 0
vsize: 213024
[startup+1120.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26358
Raw data (stat): 26295 (minisat+) R 26294 22929 22928 0 -1 0 52184 0 0 0 111851 164 0 0 25 0 1 0 479329895 218136576 52039 4294967295 134512640 134672761 3221224640 3221223808 134560855 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 53256 52039 603 41 0 53215 0
vsize: 213024
[startup+1130.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26358
Raw data (stat): 26295 (minisat+) R 26294 22929 22928 0 -1 0 52184 0 0 0 112852 164 0 0 25 0 1 0 479329895 218136576 52039 4294967295 134512640 134672761 3221224640 3221223808 134560845 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 53256 52039 603 41 0 53215 0
vsize: 213024
[startup+1140.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26360
Raw data (stat): 26295 (minisat+) R 26294 22929 22928 0 -1 0 52184 0 0 0 113852 164 0 0 25 0 1 0 479329895 218136576 52039 4294967295 134512640 134672761 3221224640 3221223764 134566068 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 53256 52039 603 41 0 53215 0
vsize: 213024
[startup+1150.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26360
Raw data (stat): 26295 (minisat+) R 26294 22929 22928 0 -1 0 52184 0 0 0 114852 164 0 0 25 0 1 0 479329895 218136576 52039 4294967295 134512640 134672761 3221224640 3221223840 134557922 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 53256 52039 603 41 0 53215 0
vsize: 213024
[startup+1160.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26360
Raw data (stat): 26295 (minisat+) R 26294 22929 22928 0 -1 0 52184 0 0 0 115852 164 0 0 25 0 1 0 479329895 218136576 52039 4294967295 134512640 134672761 3221224640 3221223744 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 53256 52039 603 41 0 53215 0
vsize: 213024
[startup+1170.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26360
Raw data (stat): 26295 (minisat+) R 26294 22929 22928 0 -1 0 52184 0 0 0 116852 164 0 0 25 0 1 0 479329895 218136576 52039 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 53256 52039 603 41 0 53215 0
vsize: 213024
[startup+1180.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26360
Raw data (stat): 26295 (minisat+) R 26294 22929 22928 0 -1 0 52184 0 0 0 117852 164 0 0 25 0 1 0 479329895 218136576 52039 4294967295 134512640 134672761 3221224640 3221223744 134560248 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 53256 52039 603 41 0 53215 0
vsize: 213024
[startup+1190.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26360
Raw data (stat): 26295 (minisat+) R 26294 22929 22928 0 -1 0 52184 0 0 0 118852 164 0 0 25 0 1 0 479329895 218136576 52039 4294967295 134512640 134672761 3221224640 3221223776 134565073 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 53256 52039 603 41 0 53215 0
vsize: 213024
[startup+1200.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26360
Raw data (stat): 26295 (minisat+) R 26294 22929 22928 0 -1 0 52184 0 0 0 119853 164 0 0 25 0 1 0 479329895 218136576 52039 4294967295 134512640 134672761 3221224640 3221223808 134561385 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 53256 52039 603 41 0 53215 0
vsize: 213024
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.14 s]
Raw data (loadavg): 0.99 0.97 0.91 1/55 26360
Raw data (stat): 26295 (minisat+) Z 26294 22929 22928 0 -1 12 52186 0 0 0 119853 174 0 0 25 0 1 0 479329895 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 0
Real time (s): 1200.14
CPU time (s): 1200.27
CPU user time (s): 1198.53
CPU system time (s): 1.74273
CPU usage (%): 100.011
Max. virtual memory (Kb): 213024
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####