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:
  1. 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.
  2. SOLVER DATA
    This is the output of the solver (stdout and stderr).
    Note that some very long lines in this section may be truncated by your web browser !
  3. 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.
  4. 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

Namemps-v2-20-10/plato.asu.edu/pub/fctp/normalized-mps-v2-20-10-ran17x17.opb
MD5SUMa15c04744ea6af8a8a8518cde7c56bce
Bench Categoryoptimization, big integers (OPTBIGINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function 4017978
Optimality of the best value was proved NO
Number of terms in the objective function 8959
Biggest coefficient in the objective function 5368709120
Number of bits for the biggest coefficient in the objective function 33
Sum of the numbers in the objective function 1612776422946
Number of bits of the sum of numbers in the objective function 41
Biggest number in a constraint 5368709120
Number of bits of the biggest number in a constraint 33
Biggest sum of numbers in a constraint 1612776422946
Number of bits of the biggest sum of numbers41
Best result obtained on this benchmarkSAT
Best CPU time to get the best result obtained on this benchmark1226.92
Number of variables8959
Total number of constraints323
Number of constraints which are clauses0
Number of constraints which are cardinality constraints (but not clauses)0
Number of constraints which are nor clauses,nor cardinality constraints323
Minimum length of a constraint31
Maximum length of a constraint510

Trace number 5871

Launcher Data

LAUNCH ON wulflinc27 THE 2005-09-20 01:25:02 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3045 boxname=wulflinc27 idbench=701 idsolver=3 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  a15c04744ea6af8a8a8518cde7c56bce  /oldhome/oroussel/tmp/wulflinc27/normalized-mps-v2-20-10-ran17x17.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc27/normalized-mps-v2-20-10-ran17x17.opb
IDLAUNCH: 3045
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.169
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.169
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:        921760 kB
Buffers:         17004 kB
Cached:          66292 kB
SwapCached:        752 kB
Active:          25564 kB
Inactive:        60388 kB
HighTotal:      131008 kB
HighFree:        62692 kB
LowTotal:       903652 kB
LowFree:        859068 kB
SwapTotal:     2097892 kB
SwapFree:      2096628 kB
Dirty:               4 kB
Writeback:           0 kB
Mapped:           5728 kB
Slab:            21308 kB
Committed_AS:    64132 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-09-20 01:45:13 (client local time) WITH STATUS 0 IN 1208.45 SECONDS
stats: 3045 7 1208.45 0

Solver Data

c Parsing PB file...
c Converting 357 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ##################################
c   -- Clauses(.)/Splits(s): (none)
c ---[ 355]---> Adder-cost: 434   maxlim: 225263   bits: 18/18
c ---[ 353]---> Adder-cost: 406   maxlim: 124911   bits: 17/17
c ---[ 351]---> Adder-cost: 434   maxlim: 223215   bits: 18/18
c ---[ 349]---> Adder-cost: 434   maxlim: 227311   bits: 18/18
c ---[ 347]---> Adder-cost: 456   maxlim: 372719   bits: 19/19
c ---[ 345]---> Adder-cost: 434   maxlim: 228335   bits: 18/18
c ---[ 343]---> Adder-cost: 434   maxlim: 229359   bits: 18/18
c ---[ 341]---> Adder-cost: 456   maxlim: 372719   bits: 19/19
c ---[ 339]---> Adder-cost: 458   maxlim: 431087   bits: 19/19
c ---[ 337]---> Adder-cost: 456   maxlim: 377839   bits: 19/19
c ---[ 335]---> Adder-cost: 456   maxlim: 375791   bits: 19/19
c ---[ 333]---> Adder-cost: 434   maxlim: 222191   bits: 18/18
c ---[ 331]---> Adder-cost: 458   maxlim: 434159   bits: 19/19
c ---[ 329]---> Adder-cost: 456   maxlim: 373743   bits: 19/19
c ---[ 327]---> Adder-cost: 456   maxlim: 381935   bits: 19/19
c ---[ 325]---> Adder-cost: 406   maxlim: 125935   bits: 17/17
c ---[ 323]---> Adder-cost: 406   maxlim: 126959   bits: 17/17
c ---[ 321]---> Adder-cost: 454   maxlim: 367599   bits: 19/19
c ---[ 319]---> Adder-cost: 416   maxlim: 133103   bits: 18/18
c ---[ 317]---> Adder-cost: 438   maxlim: 245743   bits: 18/18
c ---[ 315]---> Adder-cost: 416   maxlim: 135151   bits: 18/18
c ---[ 313]---> Adder-cost: 438   maxlim: 238575   bits: 18/18
c ---[ 311]---> Adder-cost: 454   maxlim: 368623   bits: 19/19
c ---[ 309]---> Adder-cost: 438   maxlim: 241647   bits: 18/18
c ---[ 307]---> Adder-cost: 458   maxlim: 416751   bits: 19/19
c ---[ 305]---> Adder-cost: 454   maxlim: 365551   bits: 19/19
c ---[ 303]---> Adder-cost: 384   maxlim: 66543   bits: 17/17
c ---[ 301]---> Adder-cost: 454   maxlim: 364527   bits: 19/19
c ---[ 299]---> Adder-cost: 454   maxlim: 358383   bits: 19/19
c ---[ 297]---> Adder-cost: 454   maxlim: 361455   bits: 19/19
c ---[ 295]---> Adder-cost: 458   maxlim: 413679   bits: 19/19
c ---[ 293]---> Adder-cost: 454   maxlim: 354287   bits: 19/19
c ---[ 291]---> Adder-cost: 384   maxlim: 66543   bits: 17/17
c ---[ 289]---> Adder-cost: 454   maxlim: 355311   bits: 19/19
c ---[ 288]---> BDD-cost:   16
c ---[ 287]---> BDD-cost:   15
c ---[ 286]---> BDD-cost:   15
c ---[ 285]---> BDD-cost:   17
c ---[ 284]---> BDD-cost:   20
c ---[ 283]---> BDD-cost:   20
c ---[ 282]---> BDD-cost:   15
c ---[ 281]---> BDD-cost:   14
c ---[ 280]---> BDD-cost:   18
c ---[ 279]---> BDD-cost:   19
c ---[ 278]---> BDD-cost:   20
c ---[ 277]---> BDD-cost:   20
c ---[ 276]---> BDD-cost:   20
c ---[ 275]---> BDD-cost:   14
c ---[ 274]---> BDD-cost:   14
c ---[ 273]---> BDD-cost:   20
c ---[ 272]---> BDD-cost:   15
c ---[ 271]---> BDD-cost:   14
c ---[ 270]---> BDD-cost:   18
c ---[ 269]---> BDD-cost:   16
c ---[ 268]---> BDD-cost:   16
c ---[ 267]---> BDD-cost:   20
c ---[ 266]---> BDD-cost:   20
c ---[ 265]---> BDD-cost:   20
c ---[ 264]---> BDD-cost:   16
c ---[ 263]---> BDD-cost:   15
c ---[ 262]---> BDD-cost:   14
c ---[ 261]---> BDD-cost:   20
c ---[ 260]---> BDD-cost:   20
c ---[ 259]---> BDD-cost:   20
c ---[ 258]---> BDD-cost:   20
c ---[ 257]---> BDD-cost:   20
c ---[ 256]---> BDD-cost:   14
c ---[ 255]---> BDD-cost:   20
c ---[ 254]---> BDD-cost:   15
c ---[ 253]---> BDD-cost:   16
c ---[ 252]---> BDD-cost:   14
c ---[ 251]---> BDD-cost:   18
c ---[ 250]---> BDD-cost:   16
c ---[ 249]---> BDD-cost:   16
c ---[ 248]---> BDD-cost:   20
c ---[ 247]---> BDD-cost:   20
c ---[ 246]---> BDD-cost:   16
c ---[ 245]---> BDD-cost:   16
c ---[ 244]---> BDD-cost:   14
c ---[ 243]---> BDD-cost:   16
c ---[ 242]---> BDD-cost:   16
c ---[ 241]---> BDD-cost:   16
c ---[ 240]---> BDD-cost:   16
c ---[ 239]---> BDD-cost:   16
c ---[ 238]---> BDD-cost:   16
c ---[ 237]---> BDD-cost:   14
c ---[ 236]---> BDD-cost:   16
c ---[ 235]---> BDD-cost:   16
c ---[ 234]---> BDD-cost:   14
c ---[ 233]---> BDD-cost:   16
c ---[ 232]---> BDD-cost:   16
c ---[ 231]---> BDD-cost:   16
c ---[ 230]---> BDD-cost:   16
c ---[ 229]---> BDD-cost:   16
c ---[ 228]---> BDD-cost:   16
c ---[ 227]---> BDD-cost:   14
c ---[ 226]---> BDD-cost:   14
c ---[ 225]---> BDD-cost:   14
c ---[ 224]---> BDD-cost:   14
c ---[ 223]---> BDD-cost:   14
c ---[ 222]---> BDD-cost:   14
c ---[ 221]---> BDD-cost:   14
c ---[ 220]---> BDD-cost:   16
c ---[ 219]---> BDD-cost:   14
c ---[ 218]---> BDD-cost:   14
c ---[ 217]---> BDD-cost:   14
c ---[ 216]---> BDD-cost:   14
c ---[ 215]---> BDD-cost:   14
c ---[ 214]---> BDD-cost:   14
c ---[ 213]---> BDD-cost:   14
c ---[ 212]---> BDD-cost:   14
c ---[ 211]---> BDD-cost:   14
c ---[ 210]---> BDD-cost:   14
c ---[ 209]---> BDD-cost:   15
c ---[ 208]---> BDD-cost:   17
c ---[ 207]---> BDD-cost:   15
c ---[ 206]---> BDD-cost:   14
c ---[ 205]---> BDD-cost:   17
c ---[ 204]---> BDD-cost:   17
c ---[ 203]---> BDD-cost:   17
c ---[ 202]---> BDD-cost:   17
c ---[ 201]---> BDD-cost:   17
c ---[ 200]---> BDD-cost:   14
c ---[ 199]---> BDD-cost:   17
c ---[ 198]---> BDD-cost:   15
c ---[ 197]---> BDD-cost:   15
c ---[ 196]---> BDD-cost:   14
c ---[ 195]---> BDD-cost:   17
c ---[ 194]---> BDD-cost:   17
c ---[ 193]---> BDD-cost:   16
c ---[ 192]---> BDD-cost:   17
c ---[ 191]---> BDD-cost:   17
c ---[ 190]---> BDD-cost:   17
c ---[ 189]---> BDD-cost:   15
c ---[ 188]---> BDD-cost:   14
c ---[ 187]---> BDD-cost:   14
c ---[ 186]---> BDD-cost:   17
c ---[ 185]---> BDD-cost:   17
c ---[ 184]---> BDD-cost:   17
c ---[ 183]---> BDD-cost:   17
c ---[ 182]---> BDD-cost:   17
c ---[ 181]---> BDD-cost:   14
c ---[ 180]---> BDD-cost:   17
c ---[ 179]---> BDD-cost:   15
c ---[ 178]---> BDD-cost:   14
c ---[ 177]---> BDD-cost:   17
c ---[ 176]---> BDD-cost:   14
c ---[ 175]---> BDD-cost:   15
c ---[ 174]---> BDD-cost:   17
c ---[ 173]---> BDD-cost:   17
c ---[ 172]---> BDD-cost:   17
c ---[ 171]---> BDD-cost:   17
c ---[ 170]---> BDD-cost:   20
c ---[ 169]---> BDD-cost:   15
c ---[ 168]---> BDD-cost:   14
c ---[ 167]---> BDD-cost:   18
c ---[ 166]---> BDD-cost:   19
c ---[ 165]---> BDD-cost:   20
c ---[ 164]---> BDD-cost:   15
c ---[ 163]---> BDD-cost:   18
c ---[ 162]---> BDD-cost:   18
c ---[ 161]---> BDD-cost:   14
c ---[ 160]---> BDD-cost:   18
c ---[ 159]---> BDD-cost:   15
c ---[ 158]---> BDD-cost:   14
c ---[ 157]---> BDD-cost:   18
c ---[ 156]---> BDD-cost:   16
c ---[ 155]---> BDD-cost:   16
c ---[ 154]---> BDD-cost:   18
c ---[ 153]---> BDD-cost:   15
c ---[ 152]---> BDD-cost:   20
c ---[ 151]---> BDD-cost:   18
c ---[ 150]---> BDD-cost:   15
c ---[ 149]---> BDD-cost:   14
c ---[ 148]---> BDD-cost:   18
c ---[ 147]---> BDD-cost:   18
c ---[ 146]---> BDD-cost:   18
c ---[ 145]---> BDD-cost:   18
c ---[ 144]---> BDD-cost:   18
c ---[ 143]---> BDD-cost:   14
c ---[ 142]---> BDD-cost:   15
c ---[ 141]---> BDD-cost:   18
c ---[ 140]---> BDD-cost:   15
c ---[ 139]---> BDD-cost:   14
c ---[ 138]---> BDD-cost:   18
c ---[ 137]---> BDD-cost:   18
c ---[ 136]---> BDD-cost:   18
c ---[ 135]---> BDD-cost:   18
c ---[ 134]---> BDD-cost:   18
c ---[ 133]---> BDD-cost:   15
c ---[ 132]---> BDD-cost:   15
c ---[ 131]---> BDD-cost:   15
c ---[ 130]---> BDD-cost:   14
c ---[ 129]---> BDD-cost:   15
c ---[ 128]---> BDD-cost:   15
c ---[ 127]---> BDD-cost:   15
c ---[ 126]---> BDD-cost:   15
c ---[ 125]---> BDD-cost:   15
c ---[ 124]---> BDD-cost:   14
c ---[ 123]---> BDD-cost:   15
c ---[ 122]---> BDD-cost:   15
c ---[ 121]---> BDD-cost:   14
c ---[ 120]---> BDD-cost:   14
c ---[ 119]---> BDD-cost:   15
c ---[ 118]---> BDD-cost:   15
c ---[ 117]---> BDD-cost:   15
c ---[ 116]---> BDD-cost:   15
c ---[ 115]---> BDD-cost:   15
c ---[ 114]---> BDD-cost:   20
c ---[ 113]---> BDD-cost:   15
c ---[ 112]---> BDD-cost:   14
c ---[ 111]---> BDD-cost:   18
c ---[ 110]---> BDD-cost:   19
c ---[ 109]---> BDD-cost:   15
c ---[ 108]---> BDD-cost:   20
c ---[ 107]---> BDD-cost:   18
c ---[ 106]---> BDD-cost:   18
c ---[ 105]---> BDD-cost:   14
c ---[ 104]---> BDD-cost:   18
c ---[ 103]---> BDD-cost:   15
c ---[ 102]---> BDD-cost:   14
c ---[ 101]---> BDD-cost:   18
c ---[ 100]---> BDD-cost:   16
c ---[  99]---> BDD-cost:   16
c ---[  98]---> BDD-cost:   15
c ---[  97]---> BDD-cost:   18
c ---[  96]---> BDD-cost:   20
c ---[  95]---> BDD-cost:   20
c ---[  94]---> BDD-cost:   15
c ---[  93]---> BDD-cost:   14
c ---[  92]---> BDD-cost:   18
c ---[  91]---> BDD-cost:   19
c ---[  90]---> BDD-cost:   20
c ---[  89]---> BDD-cost:   22
c ---[  88]---> BDD-cost:   19
c ---[  87]---> BDD-cost:   14
c ---[  86]---> BDD-cost:   14
c ---[  85]---> BDD-cost:   20
c ---[  84]---> BDD-cost:   15
c ---[  83]---> BDD-cost:   14
c ---[  82]---> BDD-cost:   18
c ---[  81]---> BDD-cost:   16
c ---[  80]---> BDD-cost:   16
c ---[  79]---> BDD-cost:   22
c ---[  78]---> BDD-cost:   20
c ---[  77]---> BDD-cost:   15
c ---[  76]---> BDD-cost:   16
c ---[  75]---> BDD-cost:   15
c ---[  74]---> BDD-cost:   15
c ---[  73]---> BDD-cost:   15
c ---[  72]---> BDD-cost:   15
c ---[  71]---> BDD-cost:   20
c ---[  70]---> BDD-cost:   15
c ---[  69]---> BDD-cost:   14
c ---[  68]---> BDD-cost:   18
c ---[  67]---> BDD-cost:   20
c ---[  66]---> BDD-cost:   20
c ---[  65]---> BDD-cost:   16
c ---[  64]---> BDD-cost:   20
c ---[  63]---> BDD-cost:   20
c ---[  62]---> BDD-cost:   14
c ---[  61]---> BDD-cost:   20
c ---[  60]---> BDD-cost:   15
c ---[  59]---> BDD-cost:   14
c ---[  58]---> BDD-cost:   18
c ---[  57]---> BDD-cost:   16
c ---[  56]---> BDD-cost:   16
c ---[  55]---> BDD-cost:   20
c ---[  54]---> BDD-cost:   16
c ---[  53]---> BDD-cost:   20
c ---[  52]---> BDD-cost:   20
c ---[  51]---> BDD-cost:   15
c ---[  50]---> BDD-cost:   14
c ---[  49]---> BDD-cost:   18
c ---[  48]---> BDD-cost:   20
c ---[  47]---> BDD-cost:   20
c ---[  46]---> BDD-cost:   20
c ---[  45]---> BDD-cost:   20
c ---[  44]---> BDD-cost:   14
c ---[  43]---> BDD-cost:   16
c ---[  42]---> BDD-cost:   20
c ---[  41]---> BDD-cost:   15
c ---[  40]---> BDD-cost:   14
c ---[  39]---> BDD-cost:   18
c ---[  38]---> BDD-cost:   16
c ---[  37]---> BDD-cost:   16
c ---[  36]---> BDD-cost:   20
c ---[  35]---> BDD-cost:   20
c ---[  34]---> BDD-cost:   18
c ---[  33]---> BDD-cost:   15
c ---[  32]---> BDD-cost:   16
c ---[  31]---> BDD-cost:   14
c ---[  30]---> BDD-cost:   18
c ---[  29]---> BDD-cost:   18
c ---[  28]---> BDD-cost:   18
c ---[  27]---> BDD-cost:   18
c ---[  26]---> BDD-cost:   18
c ---[  25]---> BDD-cost:   14
c ---[  24]---> BDD-cost:   18
c ---[  23]---> BDD-cost:   15
c ---[  22]---> BDD-cost:   14
c ---[  21]---> BDD-cost:   14
c ---[  20]---> BDD-cost:   18
c ---[  19]---> BDD-cost:   18
c ---[  18]---> BDD-cost:   16
c ---[  17]---> BDD-cost:   18
c ---[  16]---> BDD-cost:   18
c ---[  15]---> BDD-cost:   20
c ---[  14]---> BDD-cost:   15
c ---[  13]---> BDD-cost:   14
c ---[  12]---> BDD-cost:   18
c ---[  11]---> BDD-cost:   19
c ---[  10]---> BDD-cost:   16
c ---[   9]---> BDD-cost:   20
c ---[   8]---> BDD-cost:   17
c ---[   7]---> BDD-cost:   19
c ---[   6]---> BDD-cost:   14
c ---[   5]---> BDD-cost:   20
c ---[   4]---> BDD-cost:   15
c ---[   3]---> BDD-cost:   14
c ---[   2]---> BDD-cost:   18
c ---[   1]---> BDD-cost:   16
c ---[   0]---> BDD-cost:   16
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  107120   373762 |   35706       0        0     nan |  0.000 % |
c |       100 |  107100   373698 |   39276      97      294     3.0 | 24.108 % |
c |       250 |  107028   373454 |   43204     240      734     3.1 | 24.154 % |
c |       475 |  106953   373203 |   47524     456     1409     3.1 | 24.209 % |
c |       812 |  106790   372654 |   52277     775     2429     3.1 | 24.321 % |
c |      1318 |  106452   371492 |   57504    1236     3949     3.2 | 24.545 % |
c |      2077 |  106112   370344 |   63255    1953     6262     3.2 | 24.770 % |
c |      3216 |  105544   368374 |   69580    3004     9729     3.2 | 25.149 % |
c |      4924 |  105009   366565 |   76538    4651    15690     3.4 | 25.517 % |
c |      7486 |  104718   365580 |   84192    7175    25679     3.6 | 25.714 % |
c |     11331 |  104664   365400 |   92612   11013    42539     3.9 | 25.749 % |
c |     17097 |  104655   365371 |  101873   16778    75481     4.5 | 25.757 % |
c |     25746 |  104647   365345 |  112060   25426   220907     8.7 | 25.761 % |
c |     38720 |  104647   365345 |  123266   38400   577326    15.0 | 25.761 % |
c |     58182 |  104647   365345 |  135593   57862  1113303    19.2 | 25.761 % |
c |     87375 |  104622   365260 |  149152   87051  2616975    30.1 | 25.776 % |
c |    131165 |  104391   364461 |  164068  130808  7183223    54.9 | 25.927 % |
c |    196849 |  104045   363277 |  180474   51454  1171711    22.8 | 26.175 % |
c |    295375 |  103774   362344 |  198522  149945  7411888    49.4 | 26.368 % |
c |    443164 |  103578   361664 |  218374  103061  4269302    41.4 | 26.511 % |
c |    664848 |  103310   360772 |  240212  127704  4047362    31.7 | 26.709 % |
c |    997374 |  103004   359762 |  264233  238982 11736812    49.1 | 26.937 % |

Watcher Data

Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing Stack size limit: 67108864 bytes
Enforcing memory limit (will send SIGTERM then SIGKILL): 921600 Kb
Enforcing VSIZE limit: 994918400 bytes
Current StackSize limit: 67108864 bytes
Raw data (/proc/26709/stat): 26709 (minisat+_script) R 26708 26709 28974 0 -1 0 19 0 0 0 0 0 0 0 22 0 1 0 1854541881 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 0 0 0
Raw data (/proc/26709/statm): 174 3 169 147 0 27 0
[pid=26709] vsize: 696
open syscall for file /etc/ld.so.preload
open syscall for file tls/i686/mmx/libtermcap.so.2
open syscall for file tls/i686/libtermcap.so.2
open syscall for file tls/mmx/libtermcap.so.2
open syscall for file tls/libtermcap.so.2
open syscall for file i686/mmx/libtermcap.so.2
open syscall for file i686/libtermcap.so.2
open syscall for file mmx/libtermcap.so.2
open syscall for file libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/tls/i686/mmx/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/tls/i686/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/tls/mmx/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/tls/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/i686/mmx/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/i686/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/mmx/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/libtermcap.so.2
open syscall for file /etc/ld.so.cache
open syscall for file /lib/libtermcap.so.2
open syscall for file tls/i686/mmx/libdl.so.2
open syscall for file tls/i686/libdl.so.2
open syscall for file tls/mmx/libdl.so.2
open syscall for file tls/libdl.so.2
open syscall for file i686/mmx/libdl.so.2
open syscall for file i686/libdl.so.2
open syscall for file mmx/libdl.so.2
open syscall for file libdl.so.2
open syscall for file /oldhome/oroussel/lib/libdl.so.2
open syscall for file /lib/libdl.so.2
open syscall for file tls/i686/mmx/libc.so.6
open syscall for file tls/i686/libc.so.6
open syscall for file tls/mmx/libc.so.6
open syscall for file tls/libc.so.6
open syscall for file i686/mmx/libc.so.6
open syscall for file i686/libc.so.6
open syscall for file mmx/libc.so.6
open syscall for file libc.so.6
open syscall for file /oldhome/oroussel/lib/libc.so.6
open syscall for file /lib/tls/libc.so.6
open syscall for file /dev/tty
open syscall for file /etc/mtab
open syscall for file /proc/meminfo
open syscall for file /oldhome/oroussel/solvers/minisat+_script
New process pid=26710
New process pid=26711
New process pid=26712
execve syscall for /bin/sed executable
One traced child (pid=26711) exited with status: 0
open syscall for file /etc/ld.so.preload
open syscall for file tls/i686/mmx/libc.so.6
open syscall for file tls/i686/libc.so.6
open syscall for file tls/mmx/libc.so.6
open syscall for file tls/libc.so.6
open syscall for file i686/mmx/libc.so.6
open syscall for file i686/libc.so.6
open syscall for file mmx/libc.so.6
open syscall for file libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/i686/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/i686/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/libc.so.6
open syscall for file /oldhome/oroussel/lib/i686/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/i686/libc.so.6
open syscall for file /oldhome/oroussel/lib/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/libc.so.6
open syscall for file /etc/ld.so.cache
open syscall for file /lib/tls/libc.so.6
One traced child (pid=26712) exited with status: 0
One traced child (pid=26710) exited with status: 0
New process pid=26713
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc27/normalized-mps-v2-20-10-ran17x17.opb

[startup+10.0041 s]
Raw data (loadavg): 0.57 0.59 0.74 2/57 26713
Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26709/statm): 531 226 485 147 0 384 0
[pid=26709] vsize: 2124
Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 2650 0 0 0 972 13 0 0 25 0 1 0 1854541886 11206656 2490 4294967295 134512640 135094434 3221224432 3221223092 134553450 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26713/statm): 2736 2490 145 145 0 2591 0
[pid=26713] vsize: 10944
Current children cumulated CPU time (s) 9.87
Current children cumulated vsize (Kb) 13068

[startup+20.005 s]
Raw data (loadavg): 0.64 0.60 0.74 2/57 26713
Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26709/statm): 531 226 485 147 0 384 0
[pid=26709] vsize: 2124
Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 2668 0 0 0 1972 13 0 0 25 0 1 0 1854541886 11284480 2508 4294967295 134512640 135094434 3221224432 3221223120 134554676 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26713/statm): 2755 2508 145 145 0 2610 0
[pid=26713] vsize: 11020
Current children cumulated CPU time (s) 19.87
Current children cumulated vsize (Kb) 13144

[startup+30.0058 s]
Raw data (loadavg): 0.69 0.62 0.74 2/57 26713
Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26709/statm): 531 226 485 147 0 384 0
[pid=26709] vsize: 2124
Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 2694 0 0 0 2971 14 0 0 25 0 1 0 1854541886 11378688 2534 4294967295 134512640 135094434 3221224432 3221223088 134561734 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26713/statm): 2778 2534 145 145 0 2633 0
[pid=26713] vsize: 11112
Current children cumulated CPU time (s) 29.87
Current children cumulated vsize (Kb) 13236

[startup+40.0066 s]
Raw data (loadavg): 0.74 0.63 0.75 2/57 26713
Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26709/statm): 531 226 485 147 0 384 0
[pid=26709] vsize: 2124
Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 2722 0 0 0 3970 15 0 0 25 0 1 0 1854541886 11505664 2562 4294967295 134512640 135094434 3221224432 3221223044 134563092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26713/statm): 2809 2562 145 145 0 2664 0
[pid=26713] vsize: 11236
Current children cumulated CPU time (s) 39.87
Current children cumulated vsize (Kb) 13360

[startup+50.0085 s]
Raw data (loadavg): 0.78 0.64 0.75 2/57 26713
Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26709/statm): 531 226 485 147 0 384 0
[pid=26709] vsize: 2124
Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 2761 0 0 0 4969 15 0 0 25 0 1 0 1854541886 11649024 2601 4294967295 134512640 135094434 3221224432 3221223072 134558048 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26713/statm): 2844 2601 145 145 0 2699 0
[pid=26713] vsize: 11376
Current children cumulated CPU time (s) 49.86
Current children cumulated vsize (Kb) 13500

[startup+60.0103 s]
Raw data (loadavg): 0.81 0.65 0.75 2/57 26713
Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26709/statm): 531 226 485 147 0 384 0
[pid=26709] vsize: 2124
Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 2818 0 0 0 5968 16 0 0 25 0 1 0 1854541886 11927552 2658 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26713/statm): 2912 2658 145 145 0 2767 0
[pid=26713] vsize: 11648
Current children cumulated CPU time (s) 59.86
Current children cumulated vsize (Kb) 13772

[startup+70.0111 s]
Raw data (loadavg): 0.84 0.66 0.75 1/57 26713
Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26709/statm): 531 226 485 147 0 384 0
[pid=26709] vsize: 2124
Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) T 26709 26709 28974 0 -1 0 3695 0 0 0 6956 22 0 0 25 0 1 0 1854541886 15556608 3535 4294967295 134512640 135094434 3221224432 3221222796 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/26713/statm): 3798 3535 145 145 0 3653 0
[pid=26713] vsize: 15192
Current children cumulated CPU time (s) 69.8
Current children cumulated vsize (Kb) 17316

[startup+80.0119 s]
Raw data (loadavg): 0.86 0.67 0.75 2/57 26713
Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26709/statm): 531 226 485 147 0 384 0
[pid=26709] vsize: 2124
Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 4352 0 0 0 7946 26 0 0 25 0 1 0 1854541886 18182144 4192 4294967295 134512640 135094434 3221224432 3221223088 134558162 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26713/statm): 4439 4192 145 145 0 4294 0
[pid=26713] vsize: 17756
Current children cumulated CPU time (s) 79.74
Current children cumulated vsize (Kb) 19880

[startup+90.0128 s]
Raw data (loadavg): 0.88 0.68 0.76 2/57 26713
Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26709/statm): 531 226 485 147 0 384 0
[pid=26709] vsize: 2124
Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 5760 0 0 0 8927 34 0 0 25 0 1 0 1854541886 24125440 5600 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26713/statm): 5890 5600 145 145 0 5745 0
[pid=26713] vsize: 23560
Current children cumulated CPU time (s) 89.63
Current children cumulated vsize (Kb) 25684

[startup+100.014 s]
Raw data (loadavg): 0.90 0.69 0.76 2/57 26713
Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26709/statm): 531 226 485 147 0 384 0
[pid=26709] vsize: 2124
Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 7739 0 0 0 9898 44 0 0 25 0 1 0 1854541886 32174080 7579 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26713/statm): 7855 7579 145 145 0 7710 0
[pid=26713] vsize: 31420
Current children cumulated CPU time (s) 99.44
Current children cumulated vsize (Kb) 33544

[startup+110.015 s]
Raw data (loadavg): 0.92 0.70 0.76 2/57 26713
Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26709/statm): 531 226 485 147 0 384 0
[pid=26709] vsize: 2124
Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 9053 0 0 0 10881 52 0 0 25 0 1 0 1854541886 37490688 8893 4294967295 134512640 135094434 3221224432 3221223024 134557230 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26713/statm): 9153 8893 145 145 0 9008 0
[pid=26713] vsize: 36612
Current children cumulated CPU time (s) 109.35
Current children cumulated vsize (Kb) 38736

[startup+120.016 s]
Raw data (loadavg): 0.93 0.71 0.76 2/57 26713
Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26709/statm): 531 226 485 147 0 384 0
[pid=26709] vsize: 2124
Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 10622 0 0 0 11857 63 0 0 25 0 1 0 1854541886 43896832 10462 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26713/statm): 10717 10462 145 145 0 10572 0
[pid=26713] vsize: 42868
Current children cumulated CPU time (s) 119.22
Current children cumulated vsize (Kb) 44992

[startup+130.016 s]
Raw data (loadavg): 0.94 0.72 0.76 2/57 26713
Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26709/statm): 531 226 485 147 0 384 0
[pid=26709] vsize: 2124
Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 11184 0 0 0 12848 66 0 0 25 0 1 0 1854541886 46206976 11024 4294967295 134512640 135094434 3221224432 3221223044 134563046 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26713/statm): 11281 11024 145 145 0 11136 0
[pid=26713] vsize: 45124
Current children cumulated CPU time (s) 129.16
Current children cumulated vsize (Kb) 47248

[startup+140.017 s]
Raw data (loadavg): 0.95 0.73 0.77 2/57 26713
Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26709/statm): 531 226 485 147 0 384 0
[pid=26709] vsize: 2124
Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 11331 0 0 0 13846 68 0 0 25 0 1 0 1854541886 47316992 11171 4294967295 134512640 135094434 3221224432 3221223088 134558225 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26713/statm): 11552 11171 145 145 0 11407 0
[pid=26713] vsize: 46208
Current children cumulated CPU time (s) 139.16
Current children cumulated vsize (Kb) 48332

[startup+150.018 s]
Raw data (loadavg): 0.96 0.74 0.77 2/57 26713
Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26709/statm): 531 226 485 147 0 384 0
[pid=26709] vsize: 2124
Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 11464 0 0 0 14844 68 0 0 25 0 1 0 1854541886 47837184 11304 4294967295 134512640 135094434 3221224432 3221223092 134553530 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26713/statm): 11679 11304 145 145 0 11534 0
[pid=26713] vsize: 46716
Current children cumulated CPU time (s) 149.14
Current children cumulated vsize (Kb) 48840

[startup+160.019 s]
Raw data (loadavg): 0.96 0.75 0.77 2/57 26713
Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26709/statm): 531 226 485 147 0 384 0
[pid=26709] vsize: 2124
Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 11619 0 0 0 15841 70 0 0 25 0 1 0 1854541886 48447488 11459 4294967295 134512640 135094434 3221224432 3221223072 134562104 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26713/statm): 11828 11459 145 145 0 11683 0
[pid=26713] vsize: 47312
Current children cumulated CPU time (s) 159.13
Current children cumulated vsize (Kb) 49436

[startup+170.02 s]
Raw data (loadavg): 0.97 0.75 0.77 2/57 26713
Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26709/statm): 531 226 485 147 0 384 0
[pid=26709] vsize: 2124
Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 11841 0 0 0 16837 71 0 0 25 0 1 0 1854541886 49328128 11681 4294967295 134512640 135094434 3221224432 3221223088 134561502 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26713/statm): 12043 11681 145 145 0 11898 0
[pid=26713] vsize: 48172
Current children cumulated CPU time (s) 169.1
Current children cumulated vsize (Kb) 50296

[startup+180.021 s]
Raw data (loadavg): 0.97 0.76 0.77 2/57 26713
Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26709/statm): 531 226 485 147 0 384 0
[pid=26709] vsize: 2124
Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 12064 0 0 0 17833 73 0 0 25 0 1 0 1854541886 50216960 11904 4294967295 134512640 135094434 3221224432 3221223092 134553480 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26713/statm): 12260 11904 145 145 0 12115 0
[pid=26713] vsize: 49040
Current children cumulated CPU time (s) 179.08
Current children cumulated vsize (Kb) 51164

[startup+190.022 s]
Raw data (loadavg): 0.98 0.77 0.78 2/57 26713
Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26709/statm): 531 226 485 147 0 384 0
[pid=26709] vsize: 2124
Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 12201 0 0 0 18831 74 0 0 25 0 1 0 1854541886 50753536 12041 4294967295 134512640 135094434 3221224432 3221223088 134558411 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26713/statm): 12391 12041 145 145 0 12246 0
[pid=26713] vsize: 49564
Current children cumulated CPU time (s) 189.07
Current children cumulated vsize (Kb) 51688

[startup+200.023 s]
Raw data (loadavg): 0.98 0.78 0.78 2/57 26713
Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26709/statm): 531 226 485 147 0 384 0
[pid=26709] vsize: 2124
Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 12353 0 0 0 19828 75 0 0 25 0 1 0 1854541886 51355648 12193 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26713/statm): 12538 12193 145 145 0 12393 0
[pid=26713] vsize: 50152
Current children cumulated CPU time (s) 199.05
Current children cumulated vsize (Kb) 52276

[startup+210.024 s]
Raw data (loadavg): 0.98 0.78 0.78 2/57 26713
Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26709/statm): 531 226 485 147 0 384 0
[pid=26709] vsize: 2124
Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 12513 0 0 0 20825 76 0 0 25 0 1 0 1854541886 51990528 12353 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26713/statm): 12693 12353 145 145 0 12548 0
[pid=26713] vsize: 50772
Current children cumulated CPU time (s) 209.03
Current children cumulated vsize (Kb) 52896

[startup+220.024 s]
Raw data (loadavg): 0.98 0.79 0.78 2/57 26713
Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26709/statm): 531 226 485 147 0 384 0
[pid=26709] vsize: 2124
Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 12513 0 0 0 21825 76 0 0 25 0 1 0 1854541886 51990528 12353 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26713/statm): 12693 12353 145 145 0 12548 0
[pid=26713] vsize: 50772
Current children cumulated CPU time (s) 219.03
Current children cumulated vsize (Kb) 52896

[startup+230.025 s]
Raw data (loadavg): 0.99 0.80 0.78 2/57 26713
Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26709/statm): 531 226 485 147 0 384 0
[pid=26709] vsize: 2124
Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 12513 0 0 0 22826 76 0 0 25 0 1 0 1854541886 51990528 12353 4294967295 134512640 135094434 3221224432 3221223072 134562095 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26713/statm): 12693 12353 145 145 0 12548 0
[pid=26713] vsize: 50772
Current children cumulated CPU time (s) 229.04
Current children cumulated vsize (Kb) 52896

[startup+240.026 s]
Raw data (loadavg): 0.99 0.80 0.79 2/57 26713
Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26709/statm): 531 226 485 147 0 384 0
[pid=26709] vsize: 2124
Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 12513 0 0 0 23826 76 0 0 25 0 1 0 1854541886 51990528 12353 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26713/statm): 12693 12353 145 145 0 12548 0
[pid=26713] vsize: 50772
Current children cumulated CPU time (s) 239.04
Current children cumulated vsize (Kb) 52896

[startup+250.026 s]
Raw data (loadavg): 0.99 0.81 0.79 2/57 26713
Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26709/statm): 531 226 485 147 0 384 0
[pid=26709] vsize: 2124
Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 12513 0 0 0 24826 76 0 0 25 0 1 0 1854541886 51990528 12353 4294967295 134512640 135094434 3221224432 3221223088 134558004 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26713/statm): 12693 12353 145 145 0 12548 0
[pid=26713] vsize: 50772
Current children cumulated CPU time (s) 249.04
Current children cumulated vsize (Kb) 52896

[startup+260.028 s]
Raw data (loadavg): 0.99 0.81 0.79 2/57 26713
Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26709/statm): 531 226 485 147 0 384 0
[pid=26709] vsize: 2124
Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 12513 0 0 0 25825 77 0 0 25 0 1 0 1854541886 51990528 12353 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26713/statm): 12693 12353 145 145 0 12548 0
[pid=26713] vsize: 50772
Current children cumulated CPU time (s) 259.04
Current children cumulated vsize (Kb) 52896

[startup+270.029 s]
Raw data (loadavg): 0.99 0.82 0.79 2/57 26713
Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26709/statm): 531 226 485 147 0 384 0
[pid=26709] vsize: 2124
Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 12513 0 0 0 26825 77 0 0 25 0 1 0 1854541886 51990528 12353 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26713/statm): 12693 12353 145 145 0 12548 0
[pid=26713] vsize: 50772
Current children cumulated CPU time (s) 269.04
Current children cumulated vsize (Kb) 52896

[startup+280.028 s]
Raw data (loadavg): 0.99 0.83 0.79 2/57 26713
Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26709/statm): 531 226 485 147 0 384 0
[pid=26709] vsize: 2124
Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 12513 0 0 0 27825 77 0 0 25 0 1 0 1854541886 51990528 12353 4294967295 134512640 135094434 3221224432 3221223088 134557890 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26713/statm): 12693 12353 145 145 0 12548 0
[pid=26713] vsize: 50772
Current children cumulated CPU time (s) 279.04
Current children cumulated vsize (Kb) 52896

[startup+290.03 s]
Raw data (loadavg): 0.99 0.83 0.80 2/57 26713
Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26709/statm): 531 226 485 147 0 384 0
[pid=26709] vsize: 2124
Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 12513 0 0 0 28825 77 0 0 25 0 1 0 1854541886 51990528 12353 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26713/statm): 12693 12353 145 145 0 12548 0
[pid=26713] vsize: 50772
Current children cumulated CPU time (s) 289.04
Current children cumulated vsize (Kb) 52896

[startup+300.031 s]
Raw data (loadavg): 0.99 0.84 0.80 2/57 26713
Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26709/statm): 531 226 485 147 0 384 0
[pid=26709] vsize: 2124
Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 12513 0 0 0 29826 77 0 0 25 0 1 0 1854541886 51990528 12353 4294967295 134512640 135094434 3221224432 3221223044 134563043 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26713/statm): 12693 12353 145 145 0 12548 0
[pid=26713] vsize: 50772
Current children cumulated CPU time (s) 299.05
Current children cumulated vsize (Kb) 52896

[startup+310.032 s]
Raw data (loadavg): 0.99 0.84 0.80 2/57 26713
Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26709/statm): 531 226 485 147 0 384 0
[pid=26709] vsize: 2124
Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 12513 0 0 0 30826 77 0 0 25 0 1 0 1854541886 51990528 12353 4294967295 134512640 135094434 3221224432 3221223088 134550387 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26713/statm): 12693 12353 145 145 0 12548 0
[pid=26713] vsize: 50772
Current children cumulated CPU time (s) 309.05
Current children cumulated vsize (Kb) 52896

[startup+320.033 s]
Raw data (loadavg): 0.99 0.85 0.80 2/57 26713
Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26709/statm): 531 226 485 147 0 384 0
[pid=26709] vsize: 2124
Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 12513 0 0 0 31826 77 0 0 25 0 1 0 1854541886 51990528 12353 4294967295 134512640 135094434 3221224432 3221223088 134558221 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26713/statm): 12693 12353 145 145 0 12548 0
[pid=26713] vsize: 50772
Current children cumulated CPU time (s) 319.05
Current children cumulated vsize (Kb) 52896

[startup+330.033 s]
Raw data (loadavg): 0.99 0.85 0.80 2/57 26713
Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26709/statm): 531 226 485 147 0 384 0
[pid=26709] vsize: 2124
Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 12513 0 0 0 32826 77 0 0 25 0 1 0 1854541886 51990528 12353 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26713/statm): 12693 12353 145 145 0 12548 0
[pid=26713] vsize: 50772
Current children cumulated CPU time (s) 329.05
Current children cumulated vsize (Kb) 52896

[startup+340.034 s]
Raw data (loadavg): 0.99 0.85 0.81 2/57 26713
Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26709/statm): 531 226 485 147 0 384 0
[pid=26709] vsize: 2124
Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 12513 0 0 0 33826 77 0 0 25 0 1 0 1854541886 51990528 12353 4294967295 134512640 135094434 3221224432 3221223088 134558235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26713/statm): 12693 12353 145 145 0 12548 0
[pid=26713] vsize: 50772
Current children cumulated CPU time (s) 339.05
Current children cumulated vsize (Kb) 52896

[startup+350.035 s]
Raw data (loadavg): 0.99 0.86 0.81 2/57 26713
Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26709/statm): 531 226 485 147 0 384 0
[pid=26709] vsize: 2124
Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 12513 0 0 0 34827 77 0 0 25 0 1 0 1854541886 51990528 12353 4294967295 134512640 135094434 3221224432 3221223044 134563055 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26713/statm): 12693 12353 145 145 0 12548 0
[pid=26713] vsize: 50772
Current children cumulated CPU time (s) 349.06
Current children cumulated vsize (Kb) 52896

[startup+360.037 s]
Raw data (loadavg): 0.99 0.86 0.81 2/57 26713
Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26709/statm): 531 226 485 147 0 384 0
[pid=26709] vsize: 2124
Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 12513 0 0 0 35827 77 0 0 25 0 1 0 1854541886 51990528 12353 4294967295 134512640 135094434 3221224432 3221223024 134557366 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26713/statm): 12693 12353 145 145 0 12548 0
[pid=26713] vsize: 50772
Current children cumulated CPU time (s) 359.06
Current children cumulated vsize (Kb) 52896

[startup+370.038 s]
Raw data (loadavg): 0.99 0.87 0.81 2/57 26713
Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26709/statm): 531 226 485 147 0 384 0
[pid=26709] vsize: 2124
Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 12742 0 0 0 36824 79 0 0 25 0 1 0 1854541886 52928512 12582 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26713/statm): 12922 12582 145 145 0 12777 0
[pid=26713] vsize: 51688
Current children cumulated CPU time (s) 369.05
Current children cumulated vsize (Kb) 53812

[startup+380.038 s]
Raw data (loadavg): 0.99 0.87 0.81 2/57 26713
Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26709/statm): 531 226 485 147 0 384 0
[pid=26709] vsize: 2124
Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 13511 0 0 0 37813 83 0 0 25 0 1 0 1854541886 56078336 13351 4294967295 134512640 135094434 3221224432 3221223088 134561766 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26713/statm): 13691 13351 145 145 0 13546 0
[pid=26713] vsize: 54764
Current children cumulated CPU time (s) 378.98
Current children cumulated vsize (Kb) 56888

[startup+390.038 s]
Raw data (loadavg): 0.99 0.87 0.81 2/57 26713
Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26709/statm): 531 226 485 147 0 384 0
[pid=26709] vsize: 2124
Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 13866 0 0 0 38807 86 0 0 25 0 1 0 1854541886 57524224 13706 4294967295 134512640 135094434 3221224432 3221223024 134557522 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26713/statm): 14044 13706 145 145 0 13899 0
[pid=26713] vsize: 56176
Current children cumulated CPU time (s) 388.95
Current children cumulated vsize (Kb) 58300

[startup+400.039 s]
Raw data (loadavg): 0.99 0.88 0.82 2/57 26713
Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26709/statm): 531 226 485 147 0 384 0
[pid=26709] vsize: 2124
Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 14272 0 0 0 39800 90 0 0 25 0 1 0 1854541886 59154432 14112 4294967295 134512640 135094434 3221224432 3221223100 134553438 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26713/statm): 14442 14112 145 145 0 14297 0
[pid=26713] vsize: 57768
Current children cumulated CPU time (s) 398.92
Current children cumulated vsize (Kb) 59892

[startup+410.041 s]
Raw data (loadavg): 0.99 0.88 0.82 2/57 26713
Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26709/statm): 531 226 485 147 0 384 0
[pid=26709] vsize: 2124
Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 14418 0 0 0 40797 91 0 0 25 0 1 0 1854541886 59731968 14258 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26713/statm): 14583 14258 145 145 0 14438 0
[pid=26713] vsize: 58332
Current children cumulated CPU time (s) 408.9
Current children cumulated vsize (Kb) 60456

[startup+420.042 s]
Raw data (loadavg): 0.99 0.89 0.82 2/57 26713
Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26709/statm): 531 226 485 147 0 384 0
[pid=26709] vsize: 2124
Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 15215 0 0 0 41784 97 0 0 25 0 1 0 1854541886 62959616 15055 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26713/statm): 15371 15055 145 145 0 15226 0
[pid=26713] vsize: 61484
Current children cumulated CPU time (s) 418.83
Current children cumulated vsize (Kb) 63608

[startup+430.043 s]
Raw data (loadavg): 0.99 0.89 0.82 2/57 26713
Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26709/statm): 531 226 485 147 0 384 0
[pid=26709] vsize: 2124
Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 16314 0 0 0 42767 104 0 0 25 0 1 0 1854541886 67473408 16154 4294967295 134512640 135094434 3221224432 3221223024 134557416 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26713/statm): 16473 16154 145 145 0 16328 0
[pid=26713] vsize: 65892
Current children cumulated CPU time (s) 428.73
Current children cumulated vsize (Kb) 68016

[startup+440.044 s]
Raw data (loadavg): 0.99 0.89 0.82 2/57 26713
Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26709/statm): 531 226 485 147 0 384 0
[pid=26709] vsize: 2124
Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 16609 0 0 0 43762 107 0 0 25 0 1 0 1854541886 68669440 16449 4294967295 134512640 135094434 3221224432 3221223044 134563145 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26713/statm): 16765 16449 145 145 0 16620 0
[pid=26713] vsize: 67060
Current children cumulated CPU time (s) 438.71
Current children cumulated vsize (Kb) 69184

[startup+450.044 s]
Raw data (loadavg): 0.99 0.89 0.82 2/57 26713
Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26709/statm): 531 226 485 147 0 384 0
[pid=26709] vsize: 2124
Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 16609 0 0 0 44762 107 0 0 25 0 1 0 1854541886 68669440 16449 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26713/statm): 16765 16449 145 145 0 16620 0
[pid=26713] vsize: 67060
Current children cumulated CPU time (s) 448.71
Current children cumulated vsize (Kb) 69184

[startup+460.046 s]
Raw data (loadavg): 0.99 0.90 0.82 2/57 26713
Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26709/statm): 531 226 485 147 0 384 0
[pid=26709] vsize: 2124
Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 16609 0 0 0 45762 108 0 0 25 0 1 0 1854541886 68669440 16449 4294967295 134512640 135094434 3221224432 3221223104 134554886 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26713/statm): 16765 16449 145 145 0 16620 0
[pid=26713] vsize: 67060
Current children cumulated CPU time (s) 458.72
Current children cumulated vsize (Kb) 69184

[startup+470.048 s]
Raw data (loadavg): 0.99 0.90 0.82 2/57 26713
Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26709/statm): 531 226 485 147 0 384 0
[pid=26709] vsize: 2124
Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 16609 0 0 0 46761 108 0 0 25 0 1 0 1854541886 68669440 16449 4294967295 134512640 135094434 3221224432 3221223076 134558040 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26713/statm): 16765 16449 145 145 0 16620 0
[pid=26713] vsize: 67060
Current children cumulated CPU time (s) 468.71
Current children cumulated vsize (Kb) 69184

[startup+480.049 s]
Raw data (loadavg): 0.99 0.90 0.83 2/57 26713
Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26709/statm): 531 226 485 147 0 384 0
[pid=26709] vsize: 2124
Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 16609 0 0 0 47761 108 0 0 25 0 1 0 1854541886 68669440 16449 4294967295 134512640 135094434 3221224432 3221223088 134557928 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26713/statm): 16765 16449 145 145 0 16620 0
[pid=26713] vsize: 67060
Current children cumulated CPU time (s) 478.71
Current children cumulated vsize (Kb) 69184

[startup+490.051 s]
Raw data (loadavg): 0.99 0.91 0.83 2/57 26713
Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26709/statm): 531 226 485 147 0 384 0
[pid=26709] vsize: 2124
Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 16609 0 0 0 48760 109 0 0 25 0 1 0 1854541886 68669440 16449 4294967295 134512640 135094434 3221224432 3221223044 134563083 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26713/statm): 16765 16449 145 145 0 16620 0
[pid=26713] vsize: 67060
Current children cumulated CPU time (s) 488.71
Current children cumulated vsize (Kb) 69184

[startup+500.051 s]
Raw data (loadavg): 0.99 0.91 0.83 2/57 26713
Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26709/statm): 531 226 485 147 0 384 0
[pid=26709] vsize: 2124
Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 16609 0 0 0 49760 110 0 0 25 0 1 0 1854541886 68669440 16449 4294967295 134512640 135094434 3221224432 3221223104 134555943 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26713/statm): 16765 16449 145 145 0 16620 0
[pid=26713] vsize: 67060
Current children cumulated CPU time (s) 498.72
Current children cumulated vsize (Kb) 69184

[startup+510.052 s]
Raw data (loadavg): 0.99 0.91 0.83 2/57 26713
Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26709/statm): 531 226 485 147 0 384 0
[pid=26709] vsize: 2124
Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 16609 0 0 0 50759 110 0 0 25 0 1 0 1854541886 68669440 16449 4294967295 134512640 135094434 3221224432 3221223024 134556724 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26713/statm): 16765 16449 145 145 0 16620 0
[pid=26713] vsize: 67060
Current children cumulated CPU time (s) 508.71
Current children cumulated vsize (Kb) 69184

[startup+520.053 s]
Raw data (loadavg): 0.99 0.91 0.83 2/57 26713
Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26709/statm): 531 226 485 147 0 384 0
[pid=26709] vsize: 2124
Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 16609 0 0 0 51759 111 0 0 25 0 1 0 1854541886 68669440 16449 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26713/statm): 16765 16449 145 145 0 16620 0
[pid=26713] vsize: 67060
Current children cumulated CPU time (s) 518.72
Current children cumulated vsize (Kb) 69184

[startup+530.054 s]
Raw data (loadavg): 0.99 0.92 0.83 2/57 26713
Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26709/statm): 531 226 485 147 0 384 0
[pid=26709] vsize: 2124
Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 16609 0 0 0 52758 112 0 0 25 0 1 0 1854541886 68669440 16449 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26713/statm): 16765 16449 145 145 0 16620 0
[pid=26713] vsize: 67060
Current children cumulated CPU time (s) 528.72
Current children cumulated vsize (Kb) 69184

[startup+540.056 s]
Raw data (loadavg): 0.99 0.92 0.83 2/57 26713
Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26709/statm): 531 226 485 147 0 384 0
[pid=26709] vsize: 2124
Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 16609 0 0 0 53758 112 0 0 25 0 1 0 1854541886 68669440 16449 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26713/statm): 16765 16449 145 145 0 16620 0
[pid=26713] vsize: 67060
Current children cumulated CPU time (s) 538.72
Current children cumulated vsize (Kb) 69184

[startup+550.057 s]
Raw data (loadavg): 0.99 0.92 0.83 2/57 26713
Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26709/statm): 531 226 485 147 0 384 0
[pid=26709] vsize: 2124
Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 16609 0 0 0 54758 113 0 0 25 0 1 0 1854541886 68669440 16449 4294967295 134512640 135094434 3221224432 3221223088 134557903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26713/statm): 16765 16449 145 145 0 16620 0
[pid=26713] vsize: 67060
Current children cumulated CPU time (s) 548.73
Current children cumulated vsize (Kb) 69184

[startup+560.057 s]
Raw data (loadavg): 0.99 0.92 0.83 2/57 26713
Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26709/statm): 531 226 485 147 0 384 0
[pid=26709] vsize: 2124
Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 16609 0 0 0 55757 113 0 0 25 0 1 0 1854541886 68669440 16449 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26713/statm): 16765 16449 145 145 0 16620 0
[pid=26713] vsize: 67060
Current children cumulated CPU time (s) 558.72
Current children cumulated vsize (Kb) 69184

[startup+570.058 s]
Raw data (loadavg): 0.99 0.92 0.83 2/57 26713
Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26709/statm): 531 226 485 147 0 384 0
[pid=26709] vsize: 2124
Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 16609 0 0 0 56757 114 0 0 25 0 1 0 1854541886 68669440 16449 4294967295 134512640 135094434 3221224432 3221223184 134559282 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26713/statm): 16765 16449 145 145 0 16620 0
[pid=26713] vsize: 67060
Current children cumulated CPU time (s) 568.73
Current children cumulated vsize (Kb) 69184

[startup+580.059 s]
Raw data (loadavg): 0.99 0.93 0.84 2/57 26713
Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26709/statm): 531 226 485 147 0 384 0
[pid=26709] vsize: 2124
Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 16609 0 0 0 57756 114 0 0 25 0 1 0 1854541886 68669440 16449 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26713/statm): 16765 16449 145 145 0 16620 0
[pid=26713] vsize: 67060
Current children cumulated CPU time (s) 578.72
Current children cumulated vsize (Kb) 69184

[startup+590.061 s]
Raw data (loadavg): 0.99 0.93 0.84 2/57 26713
Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26709/statm): 531 226 485 147 0 384 0
[pid=26709] vsize: 2124
Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 16610 0 0 0 58756 115 0 0 25 0 1 0 1854541886 68669440 16450 4294967295 134512640 135094434 3221224432 3221223088 134557928 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26713/statm): 16765 16450 145 145 0 16620 0
[pid=26713] vsize: 67060
Current children cumulated CPU time (s) 588.73
Current children cumulated vsize (Kb) 69184

[startup+600.062 s]
Raw data (loadavg): 0.99 0.93 0.84 2/57 26713
Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26709/statm): 531 226 485 147 0 384 0
[pid=26709] vsize: 2124
Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 16610 0 0 0 59756 115 0 0 25 0 1 0 1854541886 68669440 16450 4294967295 134512640 135094434 3221224432 3221223072 134562098 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26713/statm): 16765 16450 145 145 0 16620 0
[pid=26713] vsize: 67060
Current children cumulated CPU time (s) 598.73
Current children cumulated vsize (Kb) 69184

[startup+610.064 s]
Raw data (loadavg): 0.99 0.93 0.84 2/57 26713
Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26709/statm): 531 226 485 147 0 384 0
[pid=26709] vsize: 2124
Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 16610 0 0 0 60755 116 0 0 25 0 1 0 1854541886 68669440 16450 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26713/statm): 16765 16450 145 145 0 16620 0
[pid=26713] vsize: 67060
Current children cumulated CPU time (s) 608.73
Current children cumulated vsize (Kb) 69184

[startup+620.064 s]
Raw data (loadavg): 0.99 0.93 0.84 2/57 26713
Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26709/statm): 531 226 485 147 0 384 0
[pid=26709] vsize: 2124
Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 16610 0 0 0 61755 117 0 0 25 0 1 0 1854541886 68669440 16450 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26713/statm): 16765 16450 145 145 0 16620 0
[pid=26713] vsize: 67060
Current children cumulated CPU time (s) 618.74
Current children cumulated vsize (Kb) 69184

[startup+630.065 s]
Raw data (loadavg): 0.99 0.94 0.84 2/57 26713
Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26709/statm): 531 226 485 147 0 384 0
[pid=26709] vsize: 2124
Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 16610 0 0 0 62754 117 0 0 25 0 1 0 1854541886 68669440 16450 4294967295 134512640 135094434 3221224432 3221223088 134557956 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26713/statm): 16765 16450 145 145 0 16620 0
[pid=26713] vsize: 67060
Current children cumulated CPU time (s) 628.73
Current children cumulated vsize (Kb) 69184

[startup+640.067 s]
Raw data (loadavg): 0.99 0.94 0.84 2/57 26713
Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26709/statm): 531 226 485 147 0 384 0
[pid=26709] vsize: 2124
Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 16610 0 0 0 63754 118 0 0 25 0 1 0 1854541886 68669440 16450 4294967295 134512640 135094434 3221224432 3221223088 134558235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26713/statm): 16765 16450 145 145 0 16620 0
[pid=26713] vsize: 67060
Current children cumulated CPU time (s) 638.74
Current children cumulated vsize (Kb) 69184

[startup+650.068 s]
Raw data (loadavg): 0.99 0.94 0.84 2/57 26713
Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26709/statm): 531 226 485 147 0 384 0
[pid=26709] vsize: 2124
Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 16610 0 0 0 64754 118 0 0 25 0 1 0 1854541886 68669440 16450 4294967295 134512640 135094434 3221224432 3221223104 134555842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26713/statm): 16765 16450 145 145 0 16620 0
[pid=26713] vsize: 67060
Current children cumulated CPU time (s) 648.74
Current children cumulated vsize (Kb) 69184

[startup+660.069 s]
Raw data (loadavg): 0.99 0.94 0.84 2/57 26713
Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26709/statm): 531 226 485 147 0 384 0
[pid=26709] vsize: 2124
Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 16610 0 0 0 65753 118 0 0 25 0 1 0 1854541886 68669440 16450 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26713/statm): 16765 16450 145 145 0 16620 0
[pid=26713] vsize: 67060
Current children cumulated CPU time (s) 658.73
Current children cumulated vsize (Kb) 69184

[startup+670.069 s]
Raw data (loadavg): 0.99 0.94 0.84 2/57 26713
Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26709/statm): 531 226 485 147 0 384 0
[pid=26709] vsize: 2124
Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 16610 0 0 0 66753 119 0 0 25 0 1 0 1854541886 68669440 16450 4294967295 134512640 135094434 3221224432 3221223044 134563055 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26713/statm): 16765 16450 145 145 0 16620 0
[pid=26713] vsize: 67060
Current children cumulated CPU time (s) 668.74
Current children cumulated vsize (Kb) 69184

[startup+680.07 s]
Raw data (loadavg): 0.99 0.94 0.85 2/57 26713
Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26709/statm): 531 226 485 147 0 384 0
[pid=26709] vsize: 2124
Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 16610 0 0 0 67753 119 0 0 25 0 1 0 1854541886 68669440 16450 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26713/statm): 16765 16450 145 145 0 16620 0
[pid=26713] vsize: 67060
Current children cumulated CPU time (s) 678.74
Current children cumulated vsize (Kb) 69184

[startup+690.071 s]
Raw data (loadavg): 0.99 0.94 0.85 2/57 26713
Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26709/statm): 531 226 485 147 0 384 0
[pid=26709] vsize: 2124
Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 16610 0 0 0 68753 119 0 0 25 0 1 0 1854541886 68669440 16450 4294967295 134512640 135094434 3221224432 3221223092 134553480 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26713/statm): 16765 16450 145 145 0 16620 0
[pid=26713] vsize: 67060
Current children cumulated CPU time (s) 688.74
Current children cumulated vsize (Kb) 69184

[startup+700.072 s]
Raw data (loadavg): 0.99 0.95 0.85 2/57 26713
Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26709/statm): 531 226 485 147 0 384 0
[pid=26709] vsize: 2124
Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 16619 0 0 0 69753 119 0 0 25 0 1 0 1854541886 68669440 16459 4294967295 134512640 135094434 3221224432 3221223072 134562104 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26713/statm): 16765 16459 145 145 0 16620 0
[pid=26713] vsize: 67060
Current children cumulated CPU time (s) 698.74
Current children cumulated vsize (Kb) 69184

[startup+710.074 s]
Raw data (loadavg): 0.99 0.95 0.85 2/57 26713
Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26709/statm): 531 226 485 147 0 384 0
[pid=26709] vsize: 2124
Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 16624 0 0 0 70754 119 0 0 25 0 1 0 1854541886 68669440 16464 4294967295 134512640 135094434 3221224432 3221223024 134551463 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26713/statm): 16765 16464 145 145 0 16620 0
[pid=26713] vsize: 67060
Current children cumulated CPU time (s) 708.75
Current children cumulated vsize (Kb) 69184

[startup+720.075 s]
Raw data (loadavg): 0.99 0.95 0.85 2/57 26713
Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26709/statm): 531 226 485 147 0 384 0
[pid=26709] vsize: 2124
Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 16624 0 0 0 71754 119 0 0 25 0 1 0 1854541886 68669440 16464 4294967295 134512640 135094434 3221224432 3221223088 134558007 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26713/statm): 16765 16464 145 145 0 16620 0
[pid=26713] vsize: 67060
Current children cumulated CPU time (s) 718.75
Current children cumulated vsize (Kb) 69184

[startup+730.075 s]
Raw data (loadavg): 0.99 0.95 0.85 2/57 26713
Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26709/statm): 531 226 485 147 0 384 0
[pid=26709] vsize: 2124
Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 16624 0 0 0 72754 119 0 0 25 0 1 0 1854541886 68669440 16464 4294967295 134512640 135094434 3221224432 3221223072 134562082 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26713/statm): 16765 16464 145 145 0 16620 0
[pid=26713] vsize: 67060
Current children cumulated CPU time (s) 728.75
Current children cumulated vsize (Kb) 69184

[startup+740.076 s]
Raw data (loadavg): 0.99 0.95 0.85 2/57 26713
Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26709/statm): 531 226 485 147 0 384 0
[pid=26709] vsize: 2124
Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 16624 0 0 0 73754 119 0 0 25 0 1 0 1854541886 68669440 16464 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26713/statm): 16765 16464 145 145 0 16620 0
[pid=26713] vsize: 67060
Current children cumulated CPU time (s) 738.75
Current children cumulated vsize (Kb) 69184

[startup+750.077 s]
Raw data (loadavg): 0.99 0.95 0.85 2/57 26713
Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26709/statm): 531 226 485 147 0 384 0
[pid=26709] vsize: 2124
Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 16624 0 0 0 74754 119 0 0 25 0 1 0 1854541886 68669440 16464 4294967295 134512640 135094434 3221224432 3221223120 134554824 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26713/statm): 16765 16464 145 145 0 16620 0
[pid=26713] vsize: 67060
Current children cumulated CPU time (s) 748.75
Current children cumulated vsize (Kb) 69184

[startup+760.079 s]
Raw data (loadavg): 0.99 0.95 0.85 2/57 26713
Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26709/statm): 531 226 485 147 0 384 0
[pid=26709] vsize: 2124
Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 16624 0 0 0 75755 119 0 0 25 0 1 0 1854541886 68669440 16464 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26713/statm): 16765 16464 145 145 0 16620 0
[pid=26713] vsize: 67060
Current children cumulated CPU time (s) 758.76
Current children cumulated vsize (Kb) 69184

[startup+770.08 s]
Raw data (loadavg): 0.99 0.95 0.85 2/57 26713
Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26709/statm): 531 226 485 147 0 384 0
[pid=26709] vsize: 2124
Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 16624 0 0 0 76755 119 0 0 25 0 1 0 1854541886 68669440 16464 4294967295 134512640 135094434 3221224432 3221223084 134561534 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26713/statm): 16765 16464 145 145 0 16620 0
[pid=26713] vsize: 67060
Current children cumulated CPU time (s) 768.76
Current children cumulated vsize (Kb) 69184

[startup+780.081 s]
Raw data (loadavg): 0.99 0.95 0.85 2/57 26713
Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26709/statm): 531 226 485 147 0 384 0
[pid=26709] vsize: 2124
Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 16624 0 0 0 77755 119 0 0 25 0 1 0 1854541886 68669440 16464 4294967295 134512640 135094434 3221224432 3221223104 134556317 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26713/statm): 16765 16464 145 145 0 16620 0
[pid=26713] vsize: 67060
Current children cumulated CPU time (s) 778.76
Current children cumulated vsize (Kb) 69184

[startup+790.081 s]
Raw data (loadavg): 0.99 0.95 0.86 2/57 26713
Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26709/statm): 531 226 485 147 0 384 0
[pid=26709] vsize: 2124
Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 16624 0 0 0 78755 119 0 0 25 0 1 0 1854541886 68669440 16464 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26713/statm): 16765 16464 145 145 0 16620 0
[pid=26713] vsize: 67060
Current children cumulated CPU time (s) 788.76
Current children cumulated vsize (Kb) 69184

[startup+800.082 s]
Raw data (loadavg): 0.99 0.95 0.86 2/57 26713
Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26709/statm): 531 226 485 147 0 384 0
[pid=26709] vsize: 2124
Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 16624 0 0 0 79755 120 0 0 25 0 1 0 1854541886 68669440 16464 4294967295 134512640 135094434 3221224432 3221223088 134557937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26713/statm): 16765 16464 145 145 0 16620 0
[pid=26713] vsize: 67060
Current children cumulated CPU time (s) 798.77
Current children cumulated vsize (Kb) 69184

[startup+810.083 s]
Raw data (loadavg): 0.99 0.96 0.86 2/57 26713
Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26709/statm): 531 226 485 147 0 384 0
[pid=26709] vsize: 2124
Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 16624 0 0 0 80755 120 0 0 25 0 1 0 1854541886 68669440 16464 4294967295 134512640 135094434 3221224432 3221223104 134555811 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26713/statm): 16765 16464 145 145 0 16620 0
[pid=26713] vsize: 67060
Current children cumulated CPU time (s) 808.77
Current children cumulated vsize (Kb) 69184

[startup+820.084 s]
Raw data (loadavg): 0.99 0.96 0.86 2/57 26713
Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26709/statm): 531 226 485 147 0 384 0
[pid=26709] vsize: 2124
Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 16624 0 0 0 81755 120 0 0 25 0 1 0 1854541886 68669440 16464 4294967295 134512640 135094434 3221224432 3221223024 134551967 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26713/statm): 16765 16464 145 145 0 16620 0
[pid=26713] vsize: 67060
Current children cumulated CPU time (s) 818.77
Current children cumulated vsize (Kb) 69184

[startup+830.085 s]
Raw data (loadavg): 0.99 0.96 0.86 2/57 26713
Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26709/statm): 531 226 485 147 0 384 0
[pid=26709] vsize: 2124
Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 16624 0 0 0 82756 120 0 0 25 0 1 0 1854541886 68669440 16464 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26713/statm): 16765 16464 145 145 0 16620 0
[pid=26713] vsize: 67060
Current children cumulated CPU time (s) 828.78
Current children cumulated vsize (Kb) 69184

[startup+840.085 s]
Raw data (loadavg): 0.99 0.96 0.86 2/57 26713
Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26709/statm): 531 226 485 147 0 384 0
[pid=26709] vsize: 2124
Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 16624 0 0 0 83756 120 0 0 25 0 1 0 1854541886 68669440 16464 4294967295 134512640 135094434 3221224432 3221223088 134558167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26713/statm): 16765 16464 145 145 0 16620 0
[pid=26713] vsize: 67060
Current children cumulated CPU time (s) 838.78
Current children cumulated vsize (Kb) 69184

[startup+850.086 s]
Raw data (loadavg): 0.99 0.96 0.86 2/57 26713
Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26709/statm): 531 226 485 147 0 384 0
[pid=26709] vsize: 2124
Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 16624 0 0 0 84756 120 0 0 25 0 1 0 1854541886 68669440 16464 4294967295 134512640 135094434 3221224432 3221223044 134563046 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26713/statm): 16765 16464 145 145 0 16620 0
[pid=26713] vsize: 67060
Current children cumulated CPU time (s) 848.78
Current children cumulated vsize (Kb) 69184

[startup+860.087 s]
Raw data (loadavg): 0.99 0.96 0.86 2/57 26713
Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26709/statm): 531 226 485 147 0 384 0
[pid=26709] vsize: 2124
Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 16624 0 0 0 85756 120 0 0 25 0 1 0 1854541886 68669440 16464 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26713/statm): 16765 16464 145 145 0 16620 0
[pid=26713] vsize: 67060
Current children cumulated CPU time (s) 858.78
Current children cumulated vsize (Kb) 69184

[startup+870.088 s]
Raw data (loadavg): 0.99 0.96 0.86 2/57 26713
Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26709/statm): 531 226 485 147 0 384 0
[pid=26709] vsize: 2124
Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 17104 0 0 0 86750 122 0 0 25 0 1 0 1854541886 70651904 16944 4294967295 134512640 135094434 3221224432 3221223044 134563059 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26713/statm): 17249 16944 145 145 0 17104 0
[pid=26713] vsize: 68996
Current children cumulated CPU time (s) 868.74
Current children cumulated vsize (Kb) 71120

[startup+880.089 s]
Raw data (loadavg): 0.99 0.96 0.86 2/57 26713
Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26709/statm): 531 226 485 147 0 384 0
[pid=26709] vsize: 2124
Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 17241 0 0 0 87748 124 0 0 25 0 1 0 1854541886 71225344 17081 4294967295 134512640 135094434 3221224432 3221223088 134558178 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26713/statm): 17389 17081 145 145 0 17244 0
[pid=26713] vsize: 69556
Current children cumulated CPU time (s) 878.74
Current children cumulated vsize (Kb) 71680

[startup+890.09 s]
Raw data (loadavg): 0.99 0.96 0.87 2/57 26713
Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26709/statm): 531 226 485 147 0 384 0
[pid=26709] vsize: 2124
Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 17363 0 0 0 88746 124 0 0 25 0 1 0 1854541886 71733248 17203 4294967295 134512640 135094434 3221224432 3221223088 134558218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26713/statm): 17513 17203 145 145 0 17368 0
[pid=26713] vsize: 70052
Current children cumulated CPU time (s) 888.72
Current children cumulated vsize (Kb) 72176

[startup+900.09 s]
Raw data (loadavg): 0.99 0.96 0.87 2/57 26713
Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26709/statm): 531 226 485 147 0 384 0
[pid=26709] vsize: 2124
Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 17538 0 0 0 89743 125 0 0 25 0 1 0 1854541886 72450048 17378 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26713/statm): 17688 17378 145 145 0 17543 0
[pid=26713] vsize: 70752
Current children cumulated CPU time (s) 898.7
Current children cumulated vsize (Kb) 72876

[startup+910.092 s]
Raw data (loadavg): 0.99 0.97 0.87 2/57 26713
Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26709/statm): 531 226 485 147 0 384 0
[pid=26709] vsize: 2124
Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 17733 0 0 0 90741 127 0 0 25 0 1 0 1854541886 73236480 17573 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26713/statm): 17880 17573 145 145 0 17735 0
[pid=26713] vsize: 71520
Current children cumulated CPU time (s) 908.7
Current children cumulated vsize (Kb) 73644

[startup+920.093 s]
Raw data (loadavg): 0.99 0.97 0.87 2/57 26713
Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26709/statm): 531 226 485 147 0 384 0
[pid=26709] vsize: 2124
Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 18031 0 0 0 91735 128 0 0 25 0 1 0 1854541886 74428416 17871 4294967295 134512640 135094434 3221224432 3221223088 134557820 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26713/statm): 18171 17871 145 145 0 18026 0
[pid=26713] vsize: 72684
Current children cumulated CPU time (s) 918.65
Current children cumulated vsize (Kb) 74808

[startup+930.093 s]
Raw data (loadavg): 0.99 0.97 0.87 2/57 26713
Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26709/statm): 531 226 485 147 0 384 0
[pid=26709] vsize: 2124
Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 18373 0 0 0 92729 130 0 0 25 0 1 0 1854541886 75796480 18213 4294967295 134512640 135094434 3221224432 3221223088 134558004 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26713/statm): 18505 18213 145 145 0 18360 0
[pid=26713] vsize: 74020
Current children cumulated CPU time (s) 928.61
Current children cumulated vsize (Kb) 76144

[startup+940.095 s]
Raw data (loadavg): 0.99 0.97 0.87 2/57 26713
Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26709/statm): 531 226 485 147 0 384 0
[pid=26709] vsize: 2124
Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 18457 0 0 0 93728 131 0 0 25 0 1 0 1854541886 76132352 18297 4294967295 134512640 135094434 3221224432 3221223088 134557900 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26713/statm): 18587 18297 145 145 0 18442 0
[pid=26713] vsize: 74348
Current children cumulated CPU time (s) 938.61
Current children cumulated vsize (Kb) 76472

[startup+950.095 s]
Raw data (loadavg): 0.99 0.97 0.87 2/57 26713
Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26709/statm): 531 226 485 147 0 384 0
[pid=26709] vsize: 2124
Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 18457 0 0 0 94728 131 0 0 25 0 1 0 1854541886 76132352 18297 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26713/statm): 18587 18297 145 145 0 18442 0
[pid=26713] vsize: 74348
Current children cumulated CPU time (s) 948.61
Current children cumulated vsize (Kb) 76472

[startup+960.096 s]
Raw data (loadavg): 0.99 0.97 0.87 2/57 26713
Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26709/statm): 531 226 485 147 0 384 0
[pid=26709] vsize: 2124
Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 18457 0 0 0 95729 131 0 0 25 0 1 0 1854541886 76132352 18297 4294967295 134512640 135094434 3221224432 3221223056 134557696 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26713/statm): 18587 18297 145 145 0 18442 0
[pid=26713] vsize: 74348
Current children cumulated CPU time (s) 958.62
Current children cumulated vsize (Kb) 76472

[startup+970.097 s]
Raw data (loadavg): 0.99 0.97 0.87 2/57 26713
Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26709/statm): 531 226 485 147 0 384 0
[pid=26709] vsize: 2124
Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 18457 0 0 0 96729 131 0 0 25 0 1 0 1854541886 76132352 18297 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26713/statm): 18587 18297 145 145 0 18442 0
[pid=26713] vsize: 74348
Current children cumulated CPU time (s) 968.62
Current children cumulated vsize (Kb) 76472

[startup+980.097 s]
Raw data (loadavg): 0.99 0.97 0.87 2/57 26713
Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26709/statm): 531 226 485 147 0 384 0
[pid=26709] vsize: 2124
Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 18457 0 0 0 97729 131 0 0 25 0 1 0 1854541886 76132352 18297 4294967295 134512640 135094434 3221224432 3221223088 134557863 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26713/statm): 18587 18297 145 145 0 18442 0
[pid=26713] vsize: 74348
Current children cumulated CPU time (s) 978.62
Current children cumulated vsize (Kb) 76472

[startup+990.098 s]
Raw data (loadavg): 0.99 0.97 0.88 2/57 26713
Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26709/statm): 531 226 485 147 0 384 0
[pid=26709] vsize: 2124
Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 18457 0 0 0 98729 131 0 0 25 0 1 0 1854541886 76132352 18297 4294967295 134512640 135094434 3221224432 3221223088 134550389 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26713/statm): 18587 18297 145 145 0 18442 0
[pid=26713] vsize: 74348
Current children cumulated CPU time (s) 988.62
Current children cumulated vsize (Kb) 76472

[startup+1000.1 s]
Raw data (loadavg): 0.99 0.97 0.88 2/57 26713
Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26709/statm): 531 226 485 147 0 384 0
[pid=26709] vsize: 2124
Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 18457 0 0 0 99730 131 0 0 25 0 1 0 1854541886 76132352 18297 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26713/statm): 18587 18297 145 145 0 18442 0
[pid=26713] vsize: 74348
Current children cumulated CPU time (s) 998.63
Current children cumulated vsize (Kb) 76472

[startup+1010.1 s]
Raw data (loadavg): 0.99 0.97 0.88 2/57 26713
Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26709/statm): 531 226 485 147 0 384 0
[pid=26709] vsize: 2124
Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 18457 0 0 0 100730 131 0 0 25 0 1 0 1854541886 76132352 18297 4294967295 134512640 135094434 3221224432 3221223044 134563071 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26713/statm): 18587 18297 145 145 0 18442 0
[pid=26713] vsize: 74348
Current children cumulated CPU time (s) 1008.63
Current children cumulated vsize (Kb) 76472

[startup+1020.1 s]
Raw data (loadavg): 0.99 0.97 0.88 2/57 26713
Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26709/statm): 531 226 485 147 0 384 0
[pid=26709] vsize: 2124
Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 18457 0 0 0 101730 131 0 0 25 0 1 0 1854541886 76132352 18297 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26713/statm): 18587 18297 145 145 0 18442 0
[pid=26713] vsize: 74348
Current children cumulated CPU time (s) 1018.63
Current children cumulated vsize (Kb) 76472

[startup+1030.1 s]
Raw data (loadavg): 0.99 0.97 0.88 2/57 26713
Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26709/statm): 531 226 485 147 0 384 0
[pid=26709] vsize: 2124
Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 18457 0 0 0 102730 131 0 0 25 0 1 0 1854541886 76132352 18297 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26713/statm): 18587 18297 145 145 0 18442 0
[pid=26713] vsize: 74348
Current children cumulated CPU time (s) 1028.63
Current children cumulated vsize (Kb) 76472

[startup+1040.1 s]
Raw data (loadavg): 0.99 0.97 0.88 2/57 26713
Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26709/statm): 531 226 485 147 0 384 0
[pid=26709] vsize: 2124
Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 18457 0 0 0 103730 131 0 0 25 0 1 0 1854541886 76132352 18297 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26713/statm): 18587 18297 145 145 0 18442 0
[pid=26713] vsize: 74348
Current children cumulated CPU time (s) 1038.63
Current children cumulated vsize (Kb) 76472

[startup+1050.1 s]
Raw data (loadavg): 0.99 0.97 0.88 2/57 26713
Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26709/statm): 531 226 485 147 0 384 0
[pid=26709] vsize: 2124
Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 18457 0 0 0 104730 132 0 0 25 0 1 0 1854541886 76132352 18297 4294967295 134512640 135094434 3221224432 3221223072 134562149 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26713/statm): 18587 18297 145 145 0 18442 0
[pid=26713] vsize: 74348
Current children cumulated CPU time (s) 1048.64
Current children cumulated vsize (Kb) 76472

[startup+1060.1 s]
Raw data (loadavg): 0.99 0.97 0.88 2/57 26713
Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26709/statm): 531 226 485 147 0 384 0
[pid=26709] vsize: 2124
Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 18457 0 0 0 105729 133 0 0 25 0 1 0 1854541886 76132352 18297 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26713/statm): 18587 18297 145 145 0 18442 0
[pid=26713] vsize: 74348
Current children cumulated CPU time (s) 1058.64
Current children cumulated vsize (Kb) 76472

[startup+1070.11 s]
Raw data (loadavg): 0.99 0.97 0.88 2/57 26713
Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26709/statm): 531 226 485 147 0 384 0
[pid=26709] vsize: 2124
Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 18457 0 0 0 106729 133 0 0 25 0 1 0 1854541886 76132352 18297 4294967295 134512640 135094434 3221224432 3221223088 134557964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26713/statm): 18587 18297 145 145 0 18442 0
[pid=26713] vsize: 74348
Current children cumulated CPU time (s) 1068.64
Current children cumulated vsize (Kb) 76472

[startup+1080.11 s]
Raw data (loadavg): 0.99 0.97 0.88 2/57 26713
Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26709/statm): 531 226 485 147 0 384 0
[pid=26709] vsize: 2124
Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 18457 0 0 0 107729 134 0 0 25 0 1 0 1854541886 76132352 18297 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26713/statm): 18587 18297 145 145 0 18442 0
[pid=26713] vsize: 74348
Current children cumulated CPU time (s) 1078.65
Current children cumulated vsize (Kb) 76472

[startup+1090.11 s]
Raw data (loadavg): 0.99 0.97 0.89 2/57 26713
Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26709/statm): 531 226 485 147 0 384 0
[pid=26709] vsize: 2124
Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 18457 0 0 0 108730 134 0 0 25 0 1 0 1854541886 76132352 18297 4294967295 134512640 135094434 3221224432 3221223088 134557879 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26713/statm): 18587 18297 145 145 0 18442 0
[pid=26713] vsize: 74348
Current children cumulated CPU time (s) 1088.66
Current children cumulated vsize (Kb) 76472

[startup+1100.11 s]
Raw data (loadavg): 0.99 0.97 0.89 2/57 26713
Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26709/statm): 531 226 485 147 0 384 0
[pid=26709] vsize: 2124
Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 18457 0 0 0 109729 134 0 0 25 0 1 0 1854541886 76132352 18297 4294967295 134512640 135094434 3221224432 3221223088 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26713/statm): 18587 18297 145 145 0 18442 0
[pid=26713] vsize: 74348
Current children cumulated CPU time (s) 1098.65
Current children cumulated vsize (Kb) 76472

[startup+1110.11 s]
Raw data (loadavg): 0.99 0.97 0.89 2/57 26713
Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26709/statm): 531 226 485 147 0 384 0
[pid=26709] vsize: 2124
Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 18457 0 0 0 110729 134 0 0 25 0 1 0 1854541886 76132352 18297 4294967295 134512640 135094434 3221224432 3221223088 134558007 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26713/statm): 18587 18297 145 145 0 18442 0
[pid=26713] vsize: 74348
Current children cumulated CPU time (s) 1108.65
Current children cumulated vsize (Kb) 76472

[startup+1120.11 s]
Raw data (loadavg): 0.99 0.97 0.89 2/57 26713
Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26709/statm): 531 226 485 147 0 384 0
[pid=26709] vsize: 2124
Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 18457 0 0 0 111730 134 0 0 25 0 1 0 1854541886 76132352 18297 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26713/statm): 18587 18297 145 145 0 18442 0
[pid=26713] vsize: 74348
Current children cumulated CPU time (s) 1118.66
Current children cumulated vsize (Kb) 76472

[startup+1130.11 s]
Raw data (loadavg): 0.99 0.97 0.89 2/57 26713
Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26709/statm): 531 226 485 147 0 384 0
[pid=26709] vsize: 2124
Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 18457 0 0 0 112730 134 0 0 25 0 1 0 1854541886 76132352 18297 4294967295 134512640 135094434 3221224432 3221223024 134551918 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26713/statm): 18587 18297 145 145 0 18442 0
[pid=26713] vsize: 74348
Current children cumulated CPU time (s) 1128.66
Current children cumulated vsize (Kb) 76472

[startup+1140.11 s]
Raw data (loadavg): 0.99 0.97 0.89 2/57 26713
Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26709/statm): 531 226 485 147 0 384 0
[pid=26709] vsize: 2124
Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 18457 0 0 0 113730 134 0 0 25 0 1 0 1854541886 76132352 18297 4294967295 134512640 135094434 3221224432 3221223088 134557972 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26713/statm): 18587 18297 145 145 0 18442 0
[pid=26713] vsize: 74348
Current children cumulated CPU time (s) 1138.66
Current children cumulated vsize (Kb) 76472

[startup+1150.11 s]
Raw data (loadavg): 0.99 0.97 0.89 2/57 26713
Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26709/statm): 531 226 485 147 0 384 0
[pid=26709] vsize: 2124
Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 19245 0 0 0 114716 140 0 0 25 0 1 0 1854541886 79368192 19085 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26713/statm): 19377 19085 145 145 0 19232 0
[pid=26713] vsize: 77508
Current children cumulated CPU time (s) 1148.58
Current children cumulated vsize (Kb) 79632

[startup+1160.11 s]
Raw data (loadavg): 0.99 0.97 0.89 2/57 26713
Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26709/statm): 531 226 485 147 0 384 0
[pid=26709] vsize: 2124
Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 19921 0 0 0 115704 145 0 0 25 0 1 0 1854541886 82169856 19761 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26713/statm): 20061 19761 145 145 0 19916 0
[pid=26713] vsize: 80244
Current children cumulated CPU time (s) 1158.51
Current children cumulated vsize (Kb) 82368

[startup+1170.11 s]
Raw data (loadavg): 0.99 0.97 0.89 2/57 26713
Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26709/statm): 531 226 485 147 0 384 0
[pid=26709] vsize: 2124
Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 20129 0 0 0 116702 146 0 0 25 0 1 0 1854541886 83021824 19969 4294967295 134512640 135094434 3221224432 3221223088 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26713/statm): 20269 19969 145 145 0 20124 0
[pid=26713] vsize: 81076
Current children cumulated CPU time (s) 1168.5
Current children cumulated vsize (Kb) 83200

[startup+1180.12 s]
Raw data (loadavg): 0.99 0.97 0.89 2/57 26713
Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26709/statm): 531 226 485 147 0 384 0
[pid=26709] vsize: 2124
Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 20352 0 0 0 117699 147 0 0 25 0 1 0 1854541886 83935232 20192 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26713/statm): 20492 20192 145 145 0 20347 0
[pid=26713] vsize: 81968
Current children cumulated CPU time (s) 1178.48
Current children cumulated vsize (Kb) 84092

[startup+1190.12 s]
Raw data (loadavg): 0.99 0.97 0.89 2/57 26713
Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26709/statm): 531 226 485 147 0 384 0
[pid=26709] vsize: 2124
Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 20461 0 0 0 118696 148 0 0 25 0 1 0 1854541886 84389888 20301 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26713/statm): 20603 20301 145 145 0 20458 0
[pid=26713] vsize: 82412
Current children cumulated CPU time (s) 1188.46
Current children cumulated vsize (Kb) 84536

[startup+1200.12 s]
Raw data (loadavg): 0.99 0.97 0.90 2/57 26713
Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26709/statm): 531 226 485 147 0 384 0
[pid=26709] vsize: 2124
Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 20624 0 0 0 119693 149 0 0 25 0 1 0 1854541886 85045248 20464 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26713/statm): 20763 20464 145 145 0 20618 0
[pid=26713] vsize: 83052
Current children cumulated CPU time (s) 1198.44
Current children cumulated vsize (Kb) 85176

[startup+1210.12 s]
Raw data (loadavg): 0.99 0.97 0.90 2/57 26713
Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26709/statm): 531 226 485 147 0 384 0
[pid=26709] vsize: 2124
Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 20934 0 0 0 120688 152 0 0 25 0 1 0 1854541886 86282240 20774 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26713/statm): 21065 20774 145 145 0 20920 0
[pid=26713] vsize: 84260
Current children cumulated CPU time (s) 1208.42
Current children cumulated vsize (Kb) 86384



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.12 s]
Raw data (loadavg): 0.99 0.97 0.90 2/57 26713
Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26709/statm): 531 226 485 147 0 384 0
[pid=26709] vsize: 2124
Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 20934 0 0 0 120688 152 0 0 25 0 1 0 1854541886 86282240 20774 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26713/statm): 21065 20774 145 145 0 20920 0
[pid=26713] vsize: 84260
Current children cumulated CPU time (s) 1208.42
Current children cumulated vsize (Kb) 86384

Sending SIGTERM to -26709
Sleeping 2 seconds
One traced child (pid=26709) ended because it received signal 15 (SIGTERM)
One traced child (pid=26713) exited with status: 0
All traced children have exited ! Game is over.

Child status: 0
Real time (s): 1210.16
CPU time (s): 1208.45
CPU user time (s): 1206.88
CPU system time (s): 1.56276
CPU usage (%): 99.858
Max. virtual memory (cumulated for all children) (Kb): 86384

Verifier Data

ERROR: no interpretation found !