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-13-7/MIPLIB/miplib3/normalized-mps-v2-13-7-vpm1.opb
MD5SUMec9e3281577e2d3f7b25c1cc88cac9ea
Bench Categoryoptimization, small integers (OPTSMALLINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function 29
Optimality of the best value was proved NO
Number of terms in the objective function 168
Biggest coefficient in the objective function 1
Number of bits for the biggest coefficient in the objective function 1
Sum of the numbers in the objective function 168
Number of bits of the sum of numbers in the objective function 8
Biggest number in a constraint 102400
Number of bits of the biggest number in a constraint 17
Biggest sum of numbers in a constraint 615983
Number of bits of the biggest sum of numbers20
Best result obtained on this benchmarkSAT
Best CPU time to get the best result obtained on this benchmark1189.02
Number of variables2124
Total number of constraints612
Number of constraints which are clauses0
Number of constraints which are cardinality constraints (but not clauses)168
Number of constraints which are nor clauses,nor cardinality constraints444
Minimum length of a constraint1
Maximum length of a constraint64

Trace number 6238

Launcher Data

LAUNCH ON wulflinc22 THE 2005-09-20 04:44:25 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3404 boxname=wulflinc22 idbench=1060 idsolver=3 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  ec9e3281577e2d3f7b25c1cc88cac9ea  /oldhome/oroussel/tmp/wulflinc22/normalized-mps-v2-13-7-vpm1.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc22/normalized-mps-v2-13-7-vpm1.opb
IDLAUNCH: 3404
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.031
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 890.88

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.031
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:        889212 kB
Buffers:         12392 kB
Cached:         106328 kB
SwapCached:        552 kB
Active:          16880 kB
Inactive:       104464 kB
HighTotal:      131008 kB
HighFree:        23772 kB
LowTotal:       903652 kB
LowFree:        865440 kB
SwapTotal:     2097892 kB
SwapFree:      2096768 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5788 kB
Slab:            18484 kB
Committed_AS:    64300 kB
PageTables:        332 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-09-20 05:04:35 (client local time) WITH STATUS 0 IN 1208.63 SECONDS
stats: 3404 7 1208.63 0

Solver Data

c Parsing PB file...
c Converting 486 PB-constraints to clauses...
c   -- Unit propagations: pppppppppppppppppppppppppppppppppppppppppppppppppppppppp
c   -- Detecting intervals from adjacent constraints: ##############################
c   -- Clauses(.)/Splits(s): (none)
c ---[ 485]---> BDD-cost:    7
c ---[ 484]---> BDD-cost:    7
c ---[ 483]---> BDD-cost:    7
c ---[ 482]---> BDD-cost:    7
c ---[ 481]---> BDD-cost:    7
c ---[ 480]---> BDD-cost:    7
c ---[ 479]---> BDD-cost:    7
c ---[ 478]---> BDD-cost:    7
c ---[ 477]---> BDD-cost:    7
c ---[ 474]---> BDD-cost:    7
c ---[ 473]---> BDD-cost:    7
c ---[ 472]---> BDD-cost:    7
c ---[ 471]---> BDD-cost:    7
c ---[ 468]---> BDD-cost:    7
c ---[ 467]---> BDD-cost:    7
c ---[ 466]---> BDD-cost:    7
c ---[ 465]---> BDD-cost:    7
c ---[ 462]---> BDD-cost:    7
c ---[ 459]---> BDD-cost:    7
c ---[ 458]---> BDD-cost:    7
c ---[ 457]---> BDD-cost:    7
c ---[ 454]---> BDD-cost:    7
c ---[ 453]---> BDD-cost:    7
c ---[ 452]---> BDD-cost:    7
c ---[ 451]---> BDD-cost:    7
c ---[ 450]---> BDD-cost:    7
c ---[ 448]---> BDD-cost:    7
c ---[ 447]---> BDD-cost:    7
c ---[ 446]---> BDD-cost:    7
c ---[ 445]---> BDD-cost:    7
c ---[ 444]---> BDD-cost:    7
c ---[ 441]---> BDD-cost:    7
c ---[ 440]---> BDD-cost:    7
c ---[ 439]---> BDD-cost:    7
c ---[ 433]---> BDD-cost:    7
c ---[ 427]---> BDD-cost:    7
c ---[ 422]---> BDD-cost:    7
c ---[ 421]---> BDD-cost:    7
c ---[ 415]---> BDD-cost:    7
c ---[ 409]---> BDD-cost:    7
c ---[ 408]---> BDD-cost:    7
c ---[ 402]---> BDD-cost:    7
c ---[ 397]---> BDD-cost:    7
c ---[ 396]---> BDD-cost:    7
c ---[ 391]---> BDD-cost:    7
c ---[ 390]---> BDD-cost:    7
c ---[ 386]---> BDD-cost:    7
c ---[ 385]---> BDD-cost:    7
c ---[ 384]---> BDD-cost:    7
c ---[ 380]---> BDD-cost:    7
c ---[ 379]---> BDD-cost:    7
c ---[ 378]---> BDD-cost:    7
c ---[ 374]---> BDD-cost:    7
c ---[ 373]---> BDD-cost:    7
c ---[ 372]---> BDD-cost:    7
c ---[ 368]---> BDD-cost:    7
c ---[ 367]---> BDD-cost:    7
c ---[ 366]---> BDD-cost:    7
c ---[ 365]---> BDD-cost:    7
c ---[ 364]---> BDD-cost:    7
c ---[ 359]---> BDD-cost:    7
c ---[ 353]---> BDD-cost:    7
c ---[ 347]---> BDD-cost:    7
c ---[ 339]---> BDD-cost:    7
c ---[ 333]---> BDD-cost:    7
c ---[ 327]---> BDD-cost:    7
c ---[ 321]---> BDD-cost:    7
c ---[ 317]---> BDD-cost:   14
c ---[ 316]---> BDD-cost:   14
c ---[ 315]---> BDD-cost:   14
c ---[ 314]---> BDD-cost:   14
c ---[ 313]---> BDD-cost:   14
c ---[ 312]---> BDD-cost:   14
c ---[ 310]---> BDD-cost:   14
c ---[ 309]---> BDD-cost:   14
c ---[ 308]---> BDD-cost:   14
c ---[ 307]---> BDD-cost:   14
c ---[ 306]---> BDD-cost:   14
c ---[ 302]---> BDD-cost:   13
c ---[ 301]---> BDD-cost:   13
c ---[ 300]---> BDD-cost:   13
c ---[ 295]---> BDD-cost:   13
c ---[ 294]---> BDD-cost:   13
c ---[ 290]---> BDD-cost:   15
c ---[ 289]---> BDD-cost:   15
c ---[ 288]---> BDD-cost:   15
c ---[ 287]---> BDD-cost:   13
c ---[ 286]---> BDD-cost:   13
c ---[ 285]---> BDD-cost:   13
c ---[ 284]---> BDD-cost:   13
c ---[ 283]---> BDD-cost:   13
c ---[ 282]---> BDD-cost:   13
c ---[ 280]---> BDD-cost:   13
c ---[ 279]---> BDD-cost:   13
c ---[ 278]---> BDD-cost:   13
c ---[ 277]---> BDD-cost:   13
c ---[ 276]---> BDD-cost:   13
c ---[ 274]---> Sorter-cost: 1988     Base: 2 2 2 5 5 2 2 2 2 2 3
c ---[ 264]---> Sorter-cost: 1824     Base: 2 2 2 5 5 2 2 2 3 2 2 2
c ---[ 260]---> Adder-cost: 262   maxlim: 300367   bits: 19/19
c ---[ 258]---> Adder-cost: 262   maxlim: 300367   bits: 19/19
c ---[ 256]---> Sorter-cost: 2565     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 254]---> Sorter-cost: 2565     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 252]---> Adder-cost: 262   maxlim: 261967   bits: 19/18
c ---[ 250]---> Sorter-cost: 1411     Base: 2 2 2 2 5 5 2 2 2 2 2
c ---[ 248]---> Sorter-cost: 2230     Base: 2 2 2 2 2 2 2 2 2 2 2 3 2
c ---[ 246]---> Sorter-cost: 2232     Base: 2 2 2 2 2 2 2 2 2 2 2 3 2
c ---[ 244]---> Sorter-cost: 2232     Base: 2 2 2 2 2 2 2 2 2 2 2 3 2
c ---[ 242]---> Sorter-cost: 2159     Base: 2 2 2 2 2 2 2 2 2 2 3 2 2
c ---[ 236]---> Sorter-cost: 1318     Base: 2 2 2 2 5 5 2 2 2 2 2
c ---[ 234]---> Sorter-cost: 2540     Base: 2 2 2 2 5 5 2 2 2 2 2 2
c ---[ 232]---> Sorter-cost: 1903     Base: 2 2 2 2 2 2 2 2 2 2 2 3
c ---[ 224]---> Sorter-cost: 1580     Base: 2 2 2 5 5 2 2 2 2 2 3
c ---[ 222]---> Adder-cost: 260   maxlim: 219983   bits: 19/18
c ---[ 216]---> Sorter-cost: 1742     Base: 2 2 2 5 5 2 2 2 2 2 2
c ---[ 214]---> Sorter-cost: 2471     Base: 2 2 2 2 2 2 2 2 2 2 2 3 2
c ---[ 212]---> Sorter-cost: 2473     Base: 2 2 2 2 2 2 2 2 2 2 2 3 2
c ---[ 210]---> Sorter-cost: 3095     Base: 2 2 2 2 2 3 5 2 2 2 5
c ---[ 208]---> Adder-cost: 222   maxlim: 103983   bits: 17/17
c ---[ 206]---> Adder-cost: 222   maxlim: 103983   bits: 17/17
c ---[ 204]---> Adder-cost: 222   maxlim: 103983   bits: 17/17
c ---[ 202]---> Adder-cost: 222   maxlim: 103983   bits: 17/17
c ---[ 200]---> Sorter-cost: 1882     Base: 2 2 2 2 5 5 2 2 2 5
c ---[ 198]---> Sorter-cost: 3211     Base: 2 2 2 2 5 5 2 2 2 2 5
c ---[ 196]---> Adder-cost: 254   maxlim: 123183   bits: 18/17
c ---[ 194]---> Adder-cost: 254   maxlim: 123183   bits: 18/17
c ---[ 192]---> Adder-cost: 254   maxlim: 123183   bits: 18/17
c ---[ 191]---> BDD-cost:   33
c ---[ 190]---> Sorter-cost:  269     Base: 2 2 2 2 2 2
c ---[ 189]---> Sorter-cost:  283     Base: 2 2 2 2 2 2
c ---[ 188]---> Sorter-cost:  540     Base: 2 2 2 2 2 2
c ---[ 187]---> Sorter-cost:  761     Base: 2 2 2 2 2 2
c ---[ 186]---> Sorter-cost:  655     Base: 2 2 2 2 2 2
c ---[ 185]---> BDD-cost:   33
c ---[ 184]---> Sorter-cost:  269     Base: 2 2 2 2 2 2
c ---[ 183]---> Sorter-cost:  283     Base: 2 2 2 2 2 2
c ---[ 182]---> Sorter-cost:  520     Base: 2 2 2 2 2 2
c ---[ 181]---> Sorter-cost:  707     Base: 2 2 2 2 2 2
c ---[ 180]---> Sorter-cost:  705     Base: 2 2 2 2 2 2
c ---[ 179]---> BDD-cost:   33
c ---[ 178]---> Sorter-cost:  269     Base: 2 2 2 2 2 2
c ---[ 177]---> Sorter-cost:  274     Base: 2 2 2 2 2 2
c ---[ 176]---> Sorter-cost:  527     Base: 2 2 2 2 2 2
c ---[ 175]---> Sorter-cost:  720     Base: 2 2 2 2 2 2
c ---[ 174]---> Sorter-cost:  692     Base: 2 2 2 2 2 2
c ---[ 173]---> BDD-cost:   33
c ---[ 172]---> Sorter-cost:  253     Base: 2 2 2 2 2 2
c ---[ 171]---> Sorter-cost:  274     Base: 2 2 2 2 2 2
c ---[ 170]---> Sorter-cost:  486     Base: 2 2 2 2 2 2
c ---[ 169]---> Sorter-cost:  695     Base: 2 2 2 2 2 2
c ---[ 168]---> Sorter-cost:  625     Base: 2 2 2 2 2 2
c ---[ 167]---> BDD-cost:    3
c ---[ 166]---> BDD-cost:    3
c ---[ 165]---> BDD-cost:    3
c ---[ 164]---> BDD-cost:    3
c ---[ 163]---> BDD-cost:    3
c ---[ 162]---> BDD-cost:    3
c ---[ 161]---> BDD-cost:    3
c ---[ 160]---> BDD-cost:    3
c ---[ 159]---> BDD-cost:    3
c ---[ 158]---> BDD-cost:    7
c ---[ 157]---> BDD-cost:    7
c ---[ 156]---> BDD-cost:    3
c ---[ 155]---> BDD-cost:    3
c ---[ 154]---> BDD-cost:    3
c ---[ 153]---> BDD-cost:    3
c ---[ 152]---> BDD-cost:    7
c ---[ 151]---> BDD-cost:    7
c ---[ 150]---> BDD-cost:    3
c ---[ 149]---> BDD-cost:    3
c ---[ 148]---> BDD-cost:    3
c ---[ 147]---> BDD-cost:    3
c ---[ 146]---> BDD-cost:    7
c ---[ 145]---> BDD-cost:    7
c ---[ 144]---> BDD-cost:    3
c ---[ 142]---> BDD-cost:    7
c ---[ 141]---> BDD-cost:    3
c ---[ 140]---> BDD-cost:    3
c ---[ 139]---> BDD-cost:    3
c ---[ 138]---> BDD-cost:    7
c ---[ 136]---> BDD-cost:    3
c ---[ 135]---> BDD-cost:    3
c ---[ 134]---> BDD-cost:    3
c ---[ 133]---> BDD-cost:    3
c ---[ 132]---> BDD-cost:    3
c ---[ 130]---> BDD-cost:    3
c ---[ 129]---> BDD-cost:    3
c ---[ 128]---> BDD-cost:    3
c ---[ 127]---> BDD-cost:    3
c ---[ 126]---> BDD-cost:    3
c ---[ 124]---> BDD-cost:    7
c ---[ 123]---> BDD-cost:    3
c ---[ 122]---> BDD-cost:    3
c ---[ 121]---> BDD-cost:    3
c ---[ 120]---> BDD-cost:    7
c ---[ 116]---> BDD-cost:    7
c ---[ 115]---> BDD-cost:    3
c ---[ 114]---> BDD-cost:    6
c ---[ 110]---> BDD-cost:    7
c ---[ 109]---> BDD-cost:    3
c ---[ 108]---> BDD-cost:    6
c ---[ 104]---> BDD-cost:    3
c ---[ 103]---> BDD-cost:    3
c ---[ 102]---> BDD-cost:    5
c ---[  98]---> BDD-cost:    7
c ---[  97]---> BDD-cost:    3
c ---[  96]---> BDD-cost:    6
c ---[  91]---> BDD-cost:    3
c ---[  90]---> BDD-cost:    3
c ---[  85]---> BDD-cost:    7
c ---[  84]---> BDD-cost:    3
c ---[  79]---> BDD-cost:    3
c ---[  78]---> BDD-cost:    3
c ---[  73]---> BDD-cost:    3
c ---[  72]---> BDD-cost:    3
c ---[  68]---> BDD-cost:    3
c ---[  67]---> BDD-cost:    3
c ---[  66]---> BDD-cost:    3
c ---[  62]---> BDD-cost:    3
c ---[  61]---> BDD-cost:    3
c ---[  60]---> BDD-cost:    3
c ---[  56]---> BDD-cost:    3
c ---[  55]---> BDD-cost:    3
c ---[  54]---> BDD-cost:    3
c ---[  50]---> BDD-cost:    3
c ---[  49]---> BDD-cost:    3
c ---[  48]---> BDD-cost:    3
c ---[  47]---> BDD-cost:    3
c ---[  46]---> BDD-cost:    3
c ---[  45]---> BDD-cost:    6
c ---[  44]---> BDD-cost:    6
c ---[  43]---> BDD-cost:    6
c ---[  42]---> BDD-cost:    6
c ---[  41]---> BDD-cost:    3
c ---[  40]---> BDD-cost:    7
c ---[  39]---> BDD-cost:    6
c ---[  38]---> BDD-cost:    6
c ---[  37]---> BDD-cost:    6
c ---[  36]---> BDD-cost:    6
c ---[  35]---> BDD-cost:    3
c ---[  34]---> BDD-cost:    7
c ---[  33]---> BDD-cost:    5
c ---[  32]---> BDD-cost:    5
c ---[  31]---> BDD-cost:    5
c ---[  30]---> BDD-cost:    5
c ---[  29]---> BDD-cost:    3
c ---[  28]---> BDD-cost:    7
c ---[  27]---> BDD-cost:    5
c ---[  26]---> BDD-cost:    5
c ---[  25]---> BDD-cost:    5
c ---[  24]---> BDD-cost:    5
c ---[  22]---> BDD-cost:    7
c ---[  21]---> BDD-cost:    3
c ---[  20]---> BDD-cost:    6
c ---[  19]---> BDD-cost:    6
c ---[  18]---> BDD-cost:    6
c ---[  16]---> BDD-cost:    7
c ---[  15]---> BDD-cost:    3
c ---[  14]---> BDD-cost:    6
c ---[  13]---> BDD-cost:    6
c ---[  12]---> BDD-cost:    6
c ---[  10]---> BDD-cost:    7
c ---[   9]---> BDD-cost:    3
c ---[   8]---> BDD-cost:    6
c ---[   7]---> BDD-cost:    6
c ---[   6]---> BDD-cost:    6
c ---[   4]---> BDD-cost:    6
c ---[   3]---> BDD-cost:    3
c ---[   2]---> BDD-cost:    5
c ---[   1]---> BDD-cost:    5
c ---[   0]---> BDD-cost:    5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  144566   360910 |   48188       0        0     nan |  0.000 % |
c |       100 |  144514   360784 |   53006      98      499     5.1 |  6.116 % |
c |       251 |  144397   360518 |   58307     244     1686     6.9 |  6.175 % |
c |       476 |  144397   360518 |   64138     469     3339     7.1 |  6.175 % |
c |       813 |  144397   360518 |   70552     806     8685    10.8 |  6.175 % |
c |      1319 |  144337   360381 |   77607    1311    24858    19.0 |  6.206 % |
c |      2078 |  144191   360038 |   85367    2057    33401    16.2 |  6.281 % |
c |      3218 |  143818   359196 |   93904    3178    50467    15.9 |  6.486 % |
c |      4926 |  143287   357996 |  103295    4836    72661    15.0 |  6.777 % |
c |      7488 |  143182   357750 |  113624    7385   155213    21.0 |  6.834 % |
c |     11332 |  143082   357526 |  124987   11219   262443    23.4 |  6.886 % |
c |     17098 |  142936   357200 |  137485   16976   448398    26.4 |  6.966 % |
c |     25748 |  142359   355853 |  151234   25578   710280    27.8 |  7.281 % |
c |     38722 |  142203   355504 |  166358   38542  1139672    29.6 |  7.368 % |
c |     58183 |  141905   354826 |  182993   57975  1716418    29.6 |  7.528 % |
c |     87377 |  141473   353854 |  201293   87113  2764142    31.7 |  7.764 % |
c |    131169 |  140881   352461 |  221422  130846  4793681    36.6 |  8.089 % |
c |    196854 |  140827   352341 |  243564  196515  8908564    45.3 |  8.122 % |
c |    295381 |  139397   349113 |  267921   72533  2036665    28.1 |  8.941 % |
c |    443170 |  138341   346669 |  294713  220188  7897187    35.9 |  9.552 % |

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/16662/stat): 16662 (minisat+_script) R 16661 16662 21452 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1855754514 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 0 0 0
Raw data (/proc/16662/statm): 174 3 169 147 0 27 0
[pid=16662] 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=16663
New process pid=16664
New process pid=16665
execve syscall for /bin/sed executable
One traced child (pid=16664) 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=16665) exited with status: 0
One traced child (pid=16663) exited with status: 0
New process pid=16666
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc22/normalized-mps-v2-13-7-vpm1.opb

[startup+10.0038 s]
Raw data (loadavg): 0.98 0.97 0.91 2/57 16666
Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16662/statm): 531 226 485 147 0 384 0
[pid=16662] vsize: 2124
Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 4497 0 0 0 961 16 0 0 25 0 1 0 1855754519 19361792 4293 4294967295 134512640 135094434 3221224432 3221223088 134557882 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16666/statm): 4727 4293 145 145 0 4582 0
[pid=16666] vsize: 18908
Current children cumulated CPU time (s) 9.78
Current children cumulated vsize (Kb) 21032

[startup+20.0055 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16666
Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16662/statm): 531 226 485 147 0 384 0
[pid=16662] vsize: 2124
Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 4858 0 0 0 1956 19 0 0 25 0 1 0 1855754519 20811776 4654 4294967295 134512640 135094434 3221224432 3221223056 134562095 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16666/statm): 5081 4654 145 145 0 4936 0
[pid=16666] vsize: 20324
Current children cumulated CPU time (s) 19.76
Current children cumulated vsize (Kb) 22448

[startup+30.0062 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16666
Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16662/statm): 531 226 485 147 0 384 0
[pid=16662] vsize: 2124
Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 5236 0 0 0 2949 21 0 0 25 0 1 0 1855754519 22388736 5032 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16666/statm): 5466 5032 145 145 0 5321 0
[pid=16666] vsize: 21864
Current children cumulated CPU time (s) 29.71
Current children cumulated vsize (Kb) 23988

[startup+40.0069 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16666
Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16662/statm): 531 226 485 147 0 384 0
[pid=16662] vsize: 2124
Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 5611 0 0 0 3944 24 0 0 25 0 1 0 1855754519 24018944 5407 4294967295 134512640 135094434 3221224432 3221223088 134557893 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16666/statm): 5864 5407 145 145 0 5719 0
[pid=16666] vsize: 23456
Current children cumulated CPU time (s) 39.69
Current children cumulated vsize (Kb) 25580

[startup+50.0086 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16666
Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16662/statm): 531 226 485 147 0 384 0
[pid=16662] vsize: 2124
Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 5994 0 0 0 4936 28 0 0 25 0 1 0 1855754519 25554944 5790 4294967295 134512640 135094434 3221224432 3221223044 134563007 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16666/statm): 6239 5790 145 145 0 6094 0
[pid=16666] vsize: 24956
Current children cumulated CPU time (s) 49.65
Current children cumulated vsize (Kb) 27080

[startup+60.0093 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16666
Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16662/statm): 531 226 485 147 0 384 0
[pid=16662] vsize: 2124
Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 6333 0 0 0 5932 30 0 0 25 0 1 0 1855754519 26923008 6129 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16666/statm): 6573 6129 145 145 0 6428 0
[pid=16666] vsize: 26292
Current children cumulated CPU time (s) 59.63
Current children cumulated vsize (Kb) 28416

[startup+70.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16666
Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16662/statm): 531 226 485 147 0 384 0
[pid=16662] vsize: 2124
Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 6585 0 0 0 6927 33 0 0 25 0 1 0 1855754519 27922432 6381 4294967295 134512640 135094434 3221224432 3221223088 134558235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16666/statm): 6817 6381 145 145 0 6672 0
[pid=16666] vsize: 27268
Current children cumulated CPU time (s) 69.61
Current children cumulated vsize (Kb) 29392

[startup+80.0128 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16666
Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16662/statm): 531 226 485 147 0 384 0
[pid=16662] vsize: 2124
Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 6955 0 0 0 7919 36 0 0 25 0 1 0 1855754519 29405184 6751 4294967295 134512640 135094434 3221224432 3221223056 134557681 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16666/statm): 7179 6751 145 145 0 7034 0
[pid=16666] vsize: 28716
Current children cumulated CPU time (s) 79.56
Current children cumulated vsize (Kb) 30840

[startup+90.0135 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16666
Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16662/statm): 531 226 485 147 0 384 0
[pid=16662] vsize: 2124
Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 7330 0 0 0 8911 39 0 0 25 0 1 0 1855754519 31182848 7126 4294967295 134512640 135094434 3221224432 3221223088 134558153 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16666/statm): 7613 7126 145 145 0 7468 0
[pid=16666] vsize: 30452
Current children cumulated CPU time (s) 89.51
Current children cumulated vsize (Kb) 32576

[startup+100.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16666
Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16662/statm): 531 226 485 147 0 384 0
[pid=16662] vsize: 2124
Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 7625 0 0 0 9906 42 0 0 25 0 1 0 1855754519 32358400 7421 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16666/statm): 7900 7421 145 145 0 7755 0
[pid=16666] vsize: 31600
Current children cumulated CPU time (s) 99.49
Current children cumulated vsize (Kb) 33724

[startup+110.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16666
Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16662/statm): 531 226 485 147 0 384 0
[pid=16662] vsize: 2124
Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 7965 0 0 0 10898 45 0 0 25 0 1 0 1855754519 33726464 7761 4294967295 134512640 135094434 3221224432 3221223104 134555574 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16666/statm): 8234 7761 145 145 0 8089 0
[pid=16666] vsize: 32936
Current children cumulated CPU time (s) 109.44
Current children cumulated vsize (Kb) 35060

[startup+120.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16666
Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16662/statm): 531 226 485 147 0 384 0
[pid=16662] vsize: 2124
Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 8105 0 0 0 11896 47 0 0 25 0 1 0 1855754519 34295808 7901 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16666/statm): 8373 7901 145 145 0 8228 0
[pid=16666] vsize: 33492
Current children cumulated CPU time (s) 119.44
Current children cumulated vsize (Kb) 35616

[startup+130.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16666
Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16662/statm): 531 226 485 147 0 384 0
[pid=16662] vsize: 2124
Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 8257 0 0 0 12894 48 0 0 25 0 1 0 1855754519 34906112 8053 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16666/statm): 8522 8053 145 145 0 8377 0
[pid=16666] vsize: 34088
Current children cumulated CPU time (s) 129.43
Current children cumulated vsize (Kb) 36212

[startup+140.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16666
Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16662/statm): 531 226 485 147 0 384 0
[pid=16662] vsize: 2124
Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 8497 0 0 0 13889 49 0 0 25 0 1 0 1855754519 35872768 8293 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16666/statm): 8758 8293 145 145 0 8613 0
[pid=16666] vsize: 35032
Current children cumulated CPU time (s) 139.39
Current children cumulated vsize (Kb) 37156

[startup+150.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16666
Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16662/statm): 531 226 485 147 0 384 0
[pid=16662] vsize: 2124
Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 8806 0 0 0 14883 52 0 0 25 0 1 0 1855754519 37142528 8602 4294967295 134512640 135094434 3221224432 3221222944 134783376 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16666/statm): 9068 8602 145 145 0 8923 0
[pid=16666] vsize: 36272
Current children cumulated CPU time (s) 149.36
Current children cumulated vsize (Kb) 38396

[startup+160.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16666
Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16662/statm): 531 226 485 147 0 384 0
[pid=16662] vsize: 2124
Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 9047 0 0 0 15879 54 0 0 25 0 1 0 1855754519 38113280 8843 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16666/statm): 9305 8843 145 145 0 9160 0
[pid=16666] vsize: 37220
Current children cumulated CPU time (s) 159.34
Current children cumulated vsize (Kb) 39344

[startup+170.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16666
Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16662/statm): 531 226 485 147 0 384 0
[pid=16662] vsize: 2124
Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 9421 0 0 0 16873 57 0 0 25 0 1 0 1855754519 39624704 9217 4294967295 134512640 135094434 3221224432 3221223088 134557872 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16666/statm): 9674 9217 145 145 0 9529 0
[pid=16666] vsize: 38696
Current children cumulated CPU time (s) 169.31
Current children cumulated vsize (Kb) 40820

[startup+180.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16666
Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16662/statm): 531 226 485 147 0 384 0
[pid=16662] vsize: 2124
Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 9852 0 0 0 17864 61 0 0 25 0 1 0 1855754519 41373696 9648 4294967295 134512640 135094434 3221224432 3221223024 134557028 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16666/statm): 10101 9648 145 145 0 9956 0
[pid=16666] vsize: 40404
Current children cumulated CPU time (s) 179.26
Current children cumulated vsize (Kb) 42528

[startup+190.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16666
Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16662/statm): 531 226 485 147 0 384 0
[pid=16662] vsize: 2124
Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 10417 0 0 0 18854 65 0 0 25 0 1 0 1855754519 43655168 10213 4294967295 134512640 135094434 3221224432 3221223024 134557518 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16666/statm): 10658 10213 145 145 0 10513 0
[pid=16666] vsize: 42632
Current children cumulated CPU time (s) 189.2
Current children cumulated vsize (Kb) 44756

[startup+200.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16666
Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16662/statm): 531 226 485 147 0 384 0
[pid=16662] vsize: 2124
Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 10790 0 0 0 19848 68 0 0 25 0 1 0 1855754519 45690880 10586 4294967295 134512640 135094434 3221224432 3221223088 134558178 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16666/statm): 11155 10586 145 145 0 11010 0
[pid=16666] vsize: 44620
Current children cumulated CPU time (s) 199.17
Current children cumulated vsize (Kb) 46744

[startup+210.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16666
Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16662/statm): 531 226 485 147 0 384 0
[pid=16662] vsize: 2124
Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 11112 0 0 0 20842 71 0 0 25 0 1 0 1855754519 46989312 10908 4294967295 134512640 135094434 3221224432 3221223088 134558178 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16666/statm): 11472 10908 145 145 0 11327 0
[pid=16666] vsize: 45888
Current children cumulated CPU time (s) 209.14
Current children cumulated vsize (Kb) 48012

[startup+220.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16666
Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16662/statm): 531 226 485 147 0 384 0
[pid=16662] vsize: 2124
Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 11409 0 0 0 21837 74 0 0 25 0 1 0 1855754519 48197632 11205 4294967295 134512640 135094434 3221224432 3221223088 134557914 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16666/statm): 11767 11205 145 145 0 11622 0
[pid=16666] vsize: 47068
Current children cumulated CPU time (s) 219.12
Current children cumulated vsize (Kb) 49192

[startup+230.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16666
Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16662/statm): 531 226 485 147 0 384 0
[pid=16662] vsize: 2124
Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 11680 0 0 0 22832 75 0 0 25 0 1 0 1855754519 49295360 11476 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16666/statm): 12035 11476 145 145 0 11890 0
[pid=16666] vsize: 48140
Current children cumulated CPU time (s) 229.08
Current children cumulated vsize (Kb) 50264

[startup+240.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16666
Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16662/statm): 531 226 485 147 0 384 0
[pid=16662] vsize: 2124
Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 11946 0 0 0 23826 78 0 0 25 0 1 0 1855754519 50376704 11742 4294967295 134512640 135094434 3221224432 3221223088 134558235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16666/statm): 12299 11742 145 145 0 12154 0
[pid=16666] vsize: 49196
Current children cumulated CPU time (s) 239.05
Current children cumulated vsize (Kb) 51320

[startup+250.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16666
Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16662/statm): 531 226 485 147 0 384 0
[pid=16662] vsize: 2124
Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 12180 0 0 0 24822 79 0 0 25 0 1 0 1855754519 51322880 11976 4294967295 134512640 135094434 3221224432 3221223088 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16666/statm): 12530 11976 145 145 0 12385 0
[pid=16666] vsize: 50120
Current children cumulated CPU time (s) 249.02
Current children cumulated vsize (Kb) 52244

[startup+260.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16666
Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16662/statm): 531 226 485 147 0 384 0
[pid=16662] vsize: 2124
Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 12411 0 0 0 25818 81 0 0 25 0 1 0 1855754519 52252672 12207 4294967295 134512640 135094434 3221224432 3221223024 134557141 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16666/statm): 12757 12207 145 145 0 12612 0
[pid=16666] vsize: 51028
Current children cumulated CPU time (s) 259
Current children cumulated vsize (Kb) 53152

[startup+270.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16666
Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16662/statm): 531 226 485 147 0 384 0
[pid=16662] vsize: 2124
Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 12666 0 0 0 26814 83 0 0 25 0 1 0 1855754519 53284864 12462 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16666/statm): 13009 12462 145 145 0 12864 0
[pid=16666] vsize: 52036
Current children cumulated CPU time (s) 268.98
Current children cumulated vsize (Kb) 54160

[startup+280.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16666
Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16662/statm): 531 226 485 147 0 384 0
[pid=16662] vsize: 2124
Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 12901 0 0 0 27809 85 0 0 25 0 1 0 1855754519 54239232 12697 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16666/statm): 13242 12697 145 145 0 13097 0
[pid=16666] vsize: 52968
Current children cumulated CPU time (s) 278.95
Current children cumulated vsize (Kb) 55092

[startup+290.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16666
Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16662/statm): 531 226 485 147 0 384 0
[pid=16662] vsize: 2124
Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 13126 0 0 0 28805 87 0 0 25 0 1 0 1855754519 55160832 12922 4294967295 134512640 135094434 3221224432 3221223088 134558007 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16666/statm): 13467 12922 145 145 0 13322 0
[pid=16666] vsize: 53868
Current children cumulated CPU time (s) 288.93
Current children cumulated vsize (Kb) 55992

[startup+300.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16666
Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16662/statm): 531 226 485 147 0 384 0
[pid=16662] vsize: 2124
Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 13376 0 0 0 29800 89 0 0 25 0 1 0 1855754519 56164352 13172 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16666/statm): 13712 13172 145 145 0 13567 0
[pid=16666] vsize: 54848
Current children cumulated CPU time (s) 298.9
Current children cumulated vsize (Kb) 56972

[startup+310.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16666
Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16662/statm): 531 226 485 147 0 384 0
[pid=16662] vsize: 2124
Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 13590 0 0 0 30795 91 0 0 25 0 1 0 1855754519 57032704 13386 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16666/statm): 13924 13386 145 145 0 13779 0
[pid=16666] vsize: 55696
Current children cumulated CPU time (s) 308.87
Current children cumulated vsize (Kb) 57820

[startup+320.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16666
Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16662/statm): 531 226 485 147 0 384 0
[pid=16662] vsize: 2124
Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 13772 0 0 0 31791 94 0 0 25 0 1 0 1855754519 57774080 13568 4294967295 134512640 135094434 3221224432 3221223024 134557157 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16666/statm): 14105 13568 145 145 0 13960 0
[pid=16666] vsize: 56420
Current children cumulated CPU time (s) 318.86
Current children cumulated vsize (Kb) 58544

[startup+330.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16666
Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16662/statm): 531 226 485 147 0 384 0
[pid=16662] vsize: 2124
Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 13952 0 0 0 32788 96 0 0 25 0 1 0 1855754519 58503168 13748 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16666/statm): 14283 13748 145 145 0 14138 0
[pid=16666] vsize: 57132
Current children cumulated CPU time (s) 328.85
Current children cumulated vsize (Kb) 59256

[startup+340.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16666
Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16662/statm): 531 226 485 147 0 384 0
[pid=16662] vsize: 2124
Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 14155 0 0 0 33783 98 0 0 25 0 1 0 1855754519 59346944 13951 4294967295 134512640 135094434 3221224432 3221223088 134558126 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16666/statm): 14489 13951 145 145 0 14344 0
[pid=16666] vsize: 57956
Current children cumulated CPU time (s) 338.82
Current children cumulated vsize (Kb) 60080

[startup+350.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16666
Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16662/statm): 531 226 485 147 0 384 0
[pid=16662] vsize: 2124
Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 14366 0 0 0 34777 102 0 0 25 0 1 0 1855754519 60219392 14162 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16666/statm): 14702 14162 145 145 0 14557 0
[pid=16666] vsize: 58808
Current children cumulated CPU time (s) 348.8
Current children cumulated vsize (Kb) 60932

[startup+360.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16666
Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16662/statm): 531 226 485 147 0 384 0
[pid=16662] vsize: 2124
Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 14535 0 0 0 35774 103 0 0 25 0 1 0 1855754519 60923904 14331 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16666/statm): 14874 14331 145 145 0 14729 0
[pid=16666] vsize: 59496
Current children cumulated CPU time (s) 358.78
Current children cumulated vsize (Kb) 61620

[startup+370.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16666
Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16662/statm): 531 226 485 147 0 384 0
[pid=16662] vsize: 2124
Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 14693 0 0 0 36771 105 0 0 25 0 1 0 1855754519 61587456 14489 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16666/statm): 15036 14489 145 145 0 14891 0
[pid=16666] vsize: 60144
Current children cumulated CPU time (s) 368.77
Current children cumulated vsize (Kb) 62268

[startup+380.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16666
Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16662/statm): 531 226 485 147 0 384 0
[pid=16662] vsize: 2124
Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 14845 0 0 0 37768 106 0 0 25 0 1 0 1855754519 62189568 14641 4294967295 134512640 135094434 3221224432 3221223092 134553501 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16666/statm): 15183 14641 145 145 0 15038 0
[pid=16666] vsize: 60732
Current children cumulated CPU time (s) 378.75
Current children cumulated vsize (Kb) 62856

[startup+390.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16666
Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16662/statm): 531 226 485 147 0 384 0
[pid=16662] vsize: 2124
Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 15079 0 0 0 38765 108 0 0 25 0 1 0 1855754519 63119360 14875 4294967295 134512640 135094434 3221224432 3221223088 134558176 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16666/statm): 15410 14875 145 145 0 15265 0
[pid=16666] vsize: 61640
Current children cumulated CPU time (s) 388.74
Current children cumulated vsize (Kb) 63764

[startup+400.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16666
Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16662/statm): 531 226 485 147 0 384 0
[pid=16662] vsize: 2124
Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 15220 0 0 0 39762 110 0 0 25 0 1 0 1855754519 63692800 15016 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16666/statm): 15550 15016 145 145 0 15405 0
[pid=16666] vsize: 62200
Current children cumulated CPU time (s) 398.73
Current children cumulated vsize (Kb) 64324

[startup+410.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16666
Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16662/statm): 531 226 485 147 0 384 0
[pid=16662] vsize: 2124
Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 15374 0 0 0 40758 112 0 0 25 0 1 0 1855754519 64307200 15170 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16666/statm): 15700 15170 145 145 0 15555 0
[pid=16666] vsize: 62800
Current children cumulated CPU time (s) 408.71
Current children cumulated vsize (Kb) 64924

[startup+420.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16666
Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16662/statm): 531 226 485 147 0 384 0
[pid=16662] vsize: 2124
Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 15515 0 0 0 41756 112 0 0 25 0 1 0 1855754519 64872448 15311 4294967295 134512640 135094434 3221224432 3221223088 134558019 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16666/statm): 15838 15311 145 145 0 15693 0
[pid=16666] vsize: 63352
Current children cumulated CPU time (s) 418.69
Current children cumulated vsize (Kb) 65476

[startup+430.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16666
Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16662/statm): 531 226 485 147 0 384 0
[pid=16662] vsize: 2124
Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 15681 0 0 0 42753 114 0 0 25 0 1 0 1855754519 65585152 15477 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16666/statm): 16012 15477 145 145 0 15867 0
[pid=16666] vsize: 64048
Current children cumulated CPU time (s) 428.68
Current children cumulated vsize (Kb) 66172

[startup+440.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16666
Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16662/statm): 531 226 485 147 0 384 0
[pid=16662] vsize: 2124
Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 15823 0 0 0 43751 115 0 0 25 0 1 0 1855754519 66166784 15619 4294967295 134512640 135094434 3221224432 3221223056 134562092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16666/statm): 16154 15619 145 145 0 16009 0
[pid=16666] vsize: 64616
Current children cumulated CPU time (s) 438.67
Current children cumulated vsize (Kb) 66740

[startup+450.051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16666
Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16662/statm): 531 226 485 147 0 384 0
[pid=16662] vsize: 2124
Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 15956 0 0 0 44749 117 0 0 25 0 1 0 1855754519 66699264 15752 4294967295 134512640 135094434 3221224432 3221223088 134558284 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16666/statm): 16284 15752 145 145 0 16139 0
[pid=16666] vsize: 65136
Current children cumulated CPU time (s) 448.67
Current children cumulated vsize (Kb) 67260

[startup+460.052 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16666
Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16662/statm): 531 226 485 147 0 384 0
[pid=16662] vsize: 2124
Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 16087 0 0 0 45746 119 0 0 25 0 1 0 1855754519 67223552 15883 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16666/statm): 16412 15883 145 145 0 16267 0
[pid=16666] vsize: 65648
Current children cumulated CPU time (s) 458.66
Current children cumulated vsize (Kb) 67772

[startup+470.053 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16666
Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16662/statm): 531 226 485 147 0 384 0
[pid=16662] vsize: 2124
Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 16201 0 0 0 46744 120 0 0 25 0 1 0 1855754519 67682304 15997 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16666/statm): 16524 15997 145 145 0 16379 0
[pid=16666] vsize: 66096
Current children cumulated CPU time (s) 468.65
Current children cumulated vsize (Kb) 68220

[startup+480.053 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16666
Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16662/statm): 531 226 485 147 0 384 0
[pid=16662] vsize: 2124
Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 16308 0 0 0 47742 120 0 0 25 0 1 0 1855754519 68104192 16104 4294967295 134512640 135094434 3221224432 3221223104 134556499 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16666/statm): 16627 16104 145 145 0 16482 0
[pid=16666] vsize: 66508
Current children cumulated CPU time (s) 478.63
Current children cumulated vsize (Kb) 68632

[startup+490.054 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16666
Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16662/statm): 531 226 485 147 0 384 0
[pid=16662] vsize: 2124
Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 16418 0 0 0 48740 122 0 0 25 0 1 0 1855754519 68571136 16214 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16666/statm): 16741 16214 145 145 0 16596 0
[pid=16666] vsize: 66964
Current children cumulated CPU time (s) 488.63
Current children cumulated vsize (Kb) 69088

[startup+500.056 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16666
Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16662/statm): 531 226 485 147 0 384 0
[pid=16662] vsize: 2124
Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 16545 0 0 0 49738 123 0 0 25 0 1 0 1855754519 69120000 16341 4294967295 134512640 135094434 3221224432 3221223088 134557903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16666/statm): 16875 16341 145 145 0 16730 0
[pid=16666] vsize: 67500
Current children cumulated CPU time (s) 498.62
Current children cumulated vsize (Kb) 69624

[startup+510.056 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16666
Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16662/statm): 531 226 485 147 0 384 0
[pid=16662] vsize: 2124
Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 16654 0 0 0 50735 125 0 0 25 0 1 0 1855754519 69566464 16450 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16666/statm): 16984 16450 145 145 0 16839 0
[pid=16666] vsize: 67936
Current children cumulated CPU time (s) 508.61
Current children cumulated vsize (Kb) 70060

[startup+520.057 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16666
Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16662/statm): 531 226 485 147 0 384 0
[pid=16662] vsize: 2124
Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 16763 0 0 0 51733 125 0 0 25 0 1 0 1855754519 70000640 16559 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16666/statm): 17090 16559 145 145 0 16945 0
[pid=16666] vsize: 68360
Current children cumulated CPU time (s) 518.59
Current children cumulated vsize (Kb) 70484

[startup+530.058 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16666
Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16662/statm): 531 226 485 147 0 384 0
[pid=16662] vsize: 2124
Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 16868 0 0 0 52731 127 0 0 25 0 1 0 1855754519 70426624 16664 4294967295 134512640 135094434 3221224432 3221223088 134557884 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16666/statm): 17194 16664 145 145 0 17049 0
[pid=16666] vsize: 68776
Current children cumulated CPU time (s) 528.59
Current children cumulated vsize (Kb) 70900

[startup+540.059 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16666
Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16662/statm): 531 226 485 147 0 384 0
[pid=16662] vsize: 2124
Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 16971 0 0 0 53728 128 0 0 25 0 1 0 1855754519 70836224 16767 4294967295 134512640 135094434 3221224432 3221223088 134557937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16666/statm): 17294 16767 145 145 0 17149 0
[pid=16666] vsize: 69176
Current children cumulated CPU time (s) 538.57
Current children cumulated vsize (Kb) 71300

[startup+550.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16666
Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16662/statm): 531 226 485 147 0 384 0
[pid=16662] vsize: 2124
Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 17068 0 0 0 54727 129 0 0 25 0 1 0 1855754519 71225344 16864 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16666/statm): 17389 16864 145 145 0 17244 0
[pid=16666] vsize: 69556
Current children cumulated CPU time (s) 548.57
Current children cumulated vsize (Kb) 71680

[startup+560.061 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16666
Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16662/statm): 531 226 485 147 0 384 0
[pid=16662] vsize: 2124
Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 17193 0 0 0 55725 130 0 0 25 0 1 0 1855754519 71761920 16989 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16666/statm): 17520 16989 145 145 0 17375 0
[pid=16666] vsize: 70080
Current children cumulated CPU time (s) 558.56
Current children cumulated vsize (Kb) 72204

[startup+570.063 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16666
Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16662/statm): 531 226 485 147 0 384 0
[pid=16662] vsize: 2124
Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 17337 0 0 0 56721 132 0 0 25 0 1 0 1855754519 72335360 17133 4294967295 134512640 135094434 3221224432 3221223088 134557937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16666/statm): 17660 17133 145 145 0 17515 0
[pid=16666] vsize: 70640
Current children cumulated CPU time (s) 568.54
Current children cumulated vsize (Kb) 72764

[startup+580.063 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16666
Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16662/statm): 531 226 485 147 0 384 0
[pid=16662] vsize: 2124
Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 17495 0 0 0 57718 133 0 0 25 0 1 0 1855754519 73011200 17291 4294967295 134512640 135094434 3221224432 3221223088 134558126 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16666/statm): 17825 17291 145 145 0 17680 0
[pid=16666] vsize: 71300
Current children cumulated CPU time (s) 578.52
Current children cumulated vsize (Kb) 73424

[startup+590.064 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16666
Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16662/statm): 531 226 485 147 0 384 0
[pid=16662] vsize: 2124
Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 17615 0 0 0 58716 134 0 0 25 0 1 0 1855754519 73494528 17411 4294967295 134512640 135094434 3221224432 3221223088 134558016 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16666/statm): 17943 17411 145 145 0 17798 0
[pid=16666] vsize: 71772
Current children cumulated CPU time (s) 588.51
Current children cumulated vsize (Kb) 73896

[startup+600.066 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16666
Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16662/statm): 531 226 485 147 0 384 0
[pid=16662] vsize: 2124
Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 17773 0 0 0 59714 135 0 0 25 0 1 0 1855754519 74121216 17569 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16666/statm): 18096 17569 145 145 0 17951 0
[pid=16666] vsize: 72384
Current children cumulated CPU time (s) 598.5
Current children cumulated vsize (Kb) 74508

[startup+610.067 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16666
Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16662/statm): 531 226 485 147 0 384 0
[pid=16662] vsize: 2124
Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 17881 0 0 0 60712 137 0 0 25 0 1 0 1855754519 74551296 17677 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16666/statm): 18201 17677 145 145 0 18056 0
[pid=16666] vsize: 72804
Current children cumulated CPU time (s) 608.5
Current children cumulated vsize (Kb) 74928

[startup+620.068 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16666
Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16662/statm): 531 226 485 147 0 384 0
[pid=16662] vsize: 2124
Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 18026 0 0 0 61711 137 0 0 25 0 1 0 1855754519 75161600 17822 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16666/statm): 18350 17822 145 145 0 18205 0
[pid=16666] vsize: 73400
Current children cumulated CPU time (s) 618.49
Current children cumulated vsize (Kb) 75524

[startup+630.069 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16666
Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16662/statm): 531 226 485 147 0 384 0
[pid=16662] vsize: 2124
Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 18200 0 0 0 62709 138 0 0 25 0 1 0 1855754519 75870208 17996 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16666/statm): 18523 17996 145 145 0 18378 0
[pid=16666] vsize: 74092
Current children cumulated CPU time (s) 628.48
Current children cumulated vsize (Kb) 76216

[startup+640.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16666
Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16662/statm): 531 226 485 147 0 384 0
[pid=16662] vsize: 2124
Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 18249 0 0 0 63707 139 0 0 25 0 1 0 1855754519 76066816 18045 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16666/statm): 18571 18045 145 145 0 18426 0
[pid=16666] vsize: 74284
Current children cumulated CPU time (s) 638.47
Current children cumulated vsize (Kb) 76408

[startup+650.071 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16666
Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16662/statm): 531 226 485 147 0 384 0
[pid=16662] vsize: 2124
Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 18249 0 0 0 64707 140 0 0 25 0 1 0 1855754519 76066816 18045 4294967295 134512640 135094434 3221224432 3221223056 134557696 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16666/statm): 18571 18045 145 145 0 18426 0
[pid=16666] vsize: 74284
Current children cumulated CPU time (s) 648.48
Current children cumulated vsize (Kb) 76408

[startup+660.072 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16666
Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16662/statm): 531 226 485 147 0 384 0
[pid=16662] vsize: 2124
Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 18249 0 0 0 65707 140 0 0 25 0 1 0 1855754519 76066816 18045 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16666/statm): 18571 18045 145 145 0 18426 0
[pid=16666] vsize: 74284
Current children cumulated CPU time (s) 658.48
Current children cumulated vsize (Kb) 76408

[startup+670.074 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16666
Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16662/statm): 531 226 485 147 0 384 0
[pid=16662] vsize: 2124
Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 18249 0 0 0 66707 140 0 0 25 0 1 0 1855754519 76066816 18045 4294967295 134512640 135094434 3221224432 3221223056 134557717 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16666/statm): 18571 18045 145 145 0 18426 0
[pid=16666] vsize: 74284
Current children cumulated CPU time (s) 668.48
Current children cumulated vsize (Kb) 76408

[startup+680.076 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16666
Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16662/statm): 531 226 485 147 0 384 0
[pid=16662] vsize: 2124
Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 18249 0 0 0 67706 141 0 0 25 0 1 0 1855754519 76066816 18045 4294967295 134512640 135094434 3221224432 3221223092 134553536 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16666/statm): 18571 18045 145 145 0 18426 0
[pid=16666] vsize: 74284
Current children cumulated CPU time (s) 678.48
Current children cumulated vsize (Kb) 76408

[startup+690.076 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16666
Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16662/statm): 531 226 485 147 0 384 0
[pid=16662] vsize: 2124
Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 18249 0 0 0 68706 142 0 0 25 0 1 0 1855754519 76066816 18045 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16666/statm): 18571 18045 145 145 0 18426 0
[pid=16666] vsize: 74284
Current children cumulated CPU time (s) 688.49
Current children cumulated vsize (Kb) 76408

[startup+700.077 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16666
Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16662/statm): 531 226 485 147 0 384 0
[pid=16662] vsize: 2124
Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 18249 0 0 0 69705 142 0 0 25 0 1 0 1855754519 76066816 18045 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16666/statm): 18571 18045 145 145 0 18426 0
[pid=16666] vsize: 74284
Current children cumulated CPU time (s) 698.48
Current children cumulated vsize (Kb) 76408

[startup+710.078 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16666
Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16662/statm): 531 226 485 147 0 384 0
[pid=16662] vsize: 2124
Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 18249 0 0 0 70704 143 0 0 25 0 1 0 1855754519 76066816 18045 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16666/statm): 18571 18045 145 145 0 18426 0
[pid=16666] vsize: 74284
Current children cumulated CPU time (s) 708.48
Current children cumulated vsize (Kb) 76408

[startup+720.079 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16666
Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16662/statm): 531 226 485 147 0 384 0
[pid=16662] vsize: 2124
Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 18250 0 0 0 71704 143 0 0 25 0 1 0 1855754519 76066816 18046 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16666/statm): 18571 18046 145 145 0 18426 0
[pid=16666] vsize: 74284
Current children cumulated CPU time (s) 718.48
Current children cumulated vsize (Kb) 76408

[startup+730.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16666
Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16662/statm): 531 226 485 147 0 384 0
[pid=16662] vsize: 2124
Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 18250 0 0 0 72704 143 0 0 25 0 1 0 1855754519 76066816 18046 4294967295 134512640 135094434 3221224432 3221223088 134558235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16666/statm): 18571 18046 145 145 0 18426 0
[pid=16666] vsize: 74284
Current children cumulated CPU time (s) 728.48
Current children cumulated vsize (Kb) 76408

[startup+740.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16666
Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16662/statm): 531 226 485 147 0 384 0
[pid=16662] vsize: 2124
Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 18250 0 0 0 73704 143 0 0 25 0 1 0 1855754519 76066816 18046 4294967295 134512640 135094434 3221224432 3221223092 134553491 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16666/statm): 18571 18046 145 145 0 18426 0
[pid=16666] vsize: 74284
Current children cumulated CPU time (s) 738.48
Current children cumulated vsize (Kb) 76408

[startup+750.082 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16666
Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16662/statm): 531 226 485 147 0 384 0
[pid=16662] vsize: 2124
Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 18250 0 0 0 74705 143 0 0 25 0 1 0 1855754519 76066816 18046 4294967295 134512640 135094434 3221224432 3221223088 134558172 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16666/statm): 18571 18046 145 145 0 18426 0
[pid=16666] vsize: 74284
Current children cumulated CPU time (s) 748.49
Current children cumulated vsize (Kb) 76408

[startup+760.082 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16666
Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16662/statm): 531 226 485 147 0 384 0
[pid=16662] vsize: 2124
Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 18252 0 0 0 75705 143 0 0 25 0 1 0 1855754519 76066816 18048 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16666/statm): 18571 18048 145 145 0 18426 0
[pid=16666] vsize: 74284
Current children cumulated CPU time (s) 758.49
Current children cumulated vsize (Kb) 76408

[startup+770.083 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16666
Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16662/statm): 531 226 485 147 0 384 0
[pid=16662] vsize: 2124
Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 18252 0 0 0 76705 143 0 0 25 0 1 0 1855754519 76066816 18048 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16666/statm): 18571 18048 145 145 0 18426 0
[pid=16666] vsize: 74284
Current children cumulated CPU time (s) 768.49
Current children cumulated vsize (Kb) 76408

[startup+780.084 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16666
Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16662/statm): 531 226 485 147 0 384 0
[pid=16662] vsize: 2124
Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 18252 0 0 0 77706 143 0 0 25 0 1 0 1855754519 76066816 18048 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16666/statm): 18571 18048 145 145 0 18426 0
[pid=16666] vsize: 74284
Current children cumulated CPU time (s) 778.5
Current children cumulated vsize (Kb) 76408

[startup+790.084 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16666
Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16662/statm): 531 226 485 147 0 384 0
[pid=16662] vsize: 2124
Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 18252 0 0 0 78706 143 0 0 25 0 1 0 1855754519 76066816 18048 4294967295 134512640 135094434 3221224432 3221223088 134557860 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16666/statm): 18571 18048 145 145 0 18426 0
[pid=16666] vsize: 74284
Current children cumulated CPU time (s) 788.5
Current children cumulated vsize (Kb) 76408

[startup+800.085 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16666
Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16662/statm): 531 226 485 147 0 384 0
[pid=16662] vsize: 2124
Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 18252 0 0 0 79706 143 0 0 25 0 1 0 1855754519 76066816 18048 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16666/statm): 18571 18048 145 145 0 18426 0
[pid=16666] vsize: 74284
Current children cumulated CPU time (s) 798.5
Current children cumulated vsize (Kb) 76408

[startup+810.086 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16666
Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16662/statm): 531 226 485 147 0 384 0
[pid=16662] vsize: 2124
Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 18252 0 0 0 80706 143 0 0 25 0 1 0 1855754519 76066816 18048 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16666/statm): 18571 18048 145 145 0 18426 0
[pid=16666] vsize: 74284
Current children cumulated CPU time (s) 808.5
Current children cumulated vsize (Kb) 76408

[startup+820.087 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16666
Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16662/statm): 531 226 485 147 0 384 0
[pid=16662] vsize: 2124
Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 18253 0 0 0 81706 143 0 0 25 0 1 0 1855754519 76066816 18049 4294967295 134512640 135094434 3221224432 3221223088 134558395 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16666/statm): 18571 18049 145 145 0 18426 0
[pid=16666] vsize: 74284
Current children cumulated CPU time (s) 818.5
Current children cumulated vsize (Kb) 76408

[startup+830.087 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16666
Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16662/statm): 531 226 485 147 0 384 0
[pid=16662] vsize: 2124
Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 18254 0 0 0 82707 143 0 0 25 0 1 0 1855754519 76066816 18050 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16666/statm): 18571 18050 145 145 0 18426 0
[pid=16666] vsize: 74284
Current children cumulated CPU time (s) 828.51
Current children cumulated vsize (Kb) 76408

[startup+840.088 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16666
Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16662/statm): 531 226 485 147 0 384 0
[pid=16662] vsize: 2124
Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 18265 0 0 0 83707 143 0 0 25 0 1 0 1855754519 76132352 18061 4294967295 134512640 135094434 3221224432 3221223088 134557937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16666/statm): 18587 18061 145 145 0 18442 0
[pid=16666] vsize: 74348
Current children cumulated CPU time (s) 838.51
Current children cumulated vsize (Kb) 76472

[startup+850.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16666
Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16662/statm): 531 226 485 147 0 384 0
[pid=16662] vsize: 2124
Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 18278 0 0 0 84707 143 0 0 25 0 1 0 1855754519 76197888 18074 4294967295 134512640 135094434 3221224432 3221223088 134557835 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16666/statm): 18603 18074 145 145 0 18458 0
[pid=16666] vsize: 74412
Current children cumulated CPU time (s) 848.51
Current children cumulated vsize (Kb) 76536

[startup+860.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16666
Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16662/statm): 531 226 485 147 0 384 0
[pid=16662] vsize: 2124
Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 18279 0 0 0 85707 143 0 0 25 0 1 0 1855754519 76197888 18075 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16666/statm): 18603 18075 145 145 0 18458 0
[pid=16666] vsize: 74412
Current children cumulated CPU time (s) 858.51
Current children cumulated vsize (Kb) 76536

[startup+870.091 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16666
Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16662/statm): 531 226 485 147 0 384 0
[pid=16662] vsize: 2124
Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 18280 0 0 0 86708 143 0 0 25 0 1 0 1855754519 76197888 18076 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16666/statm): 18603 18076 145 145 0 18458 0
[pid=16666] vsize: 74412
Current children cumulated CPU time (s) 868.52
Current children cumulated vsize (Kb) 76536

[startup+880.092 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16666
Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16662/statm): 531 226 485 147 0 384 0
[pid=16662] vsize: 2124
Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 18290 0 0 0 87708 143 0 0 25 0 1 0 1855754519 76263424 18086 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16666/statm): 18619 18086 145 145 0 18474 0
[pid=16666] vsize: 74476
Current children cumulated CPU time (s) 878.52
Current children cumulated vsize (Kb) 76600

[startup+890.093 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16666
Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16662/statm): 531 226 485 147 0 384 0
[pid=16662] vsize: 2124
Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 18290 0 0 0 88708 143 0 0 25 0 1 0 1855754519 76263424 18086 4294967295 134512640 135094434 3221224432 3221223024 134557199 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16666/statm): 18619 18086 145 145 0 18474 0
[pid=16666] vsize: 74476
Current children cumulated CPU time (s) 888.52
Current children cumulated vsize (Kb) 76600

[startup+900.093 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16666
Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16662/statm): 531 226 485 147 0 384 0
[pid=16662] vsize: 2124
Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 18290 0 0 0 89708 143 0 0 25 0 1 0 1855754519 76263424 18086 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16666/statm): 18619 18086 145 145 0 18474 0
[pid=16666] vsize: 74476
Current children cumulated CPU time (s) 898.52
Current children cumulated vsize (Kb) 76600

[startup+910.094 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16666
Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16662/statm): 531 226 485 147 0 384 0
[pid=16662] vsize: 2124
Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 18290 0 0 0 90709 143 0 0 25 0 1 0 1855754519 76263424 18086 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16666/statm): 18619 18086 145 145 0 18474 0
[pid=16666] vsize: 74476
Current children cumulated CPU time (s) 908.53
Current children cumulated vsize (Kb) 76600

[startup+920.095 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16666
Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16662/statm): 531 226 485 147 0 384 0
[pid=16662] vsize: 2124
Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 18290 0 0 0 91709 143 0 0 25 0 1 0 1855754519 76263424 18086 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16666/statm): 18619 18086 145 145 0 18474 0
[pid=16666] vsize: 74476
Current children cumulated CPU time (s) 918.53
Current children cumulated vsize (Kb) 76600

[startup+930.095 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16666
Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16662/statm): 531 226 485 147 0 384 0
[pid=16662] vsize: 2124
Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 18290 0 0 0 92709 143 0 0 25 0 1 0 1855754519 76263424 18086 4294967295 134512640 135094434 3221224432 3221223088 134558420 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16666/statm): 18619 18086 145 145 0 18474 0
[pid=16666] vsize: 74476
Current children cumulated CPU time (s) 928.53
Current children cumulated vsize (Kb) 76600

[startup+940.095 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16666
Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16662/statm): 531 226 485 147 0 384 0
[pid=16662] vsize: 2124
Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 18292 0 0 0 93709 143 0 0 25 0 1 0 1855754519 76263424 18088 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16666/statm): 18619 18088 145 145 0 18474 0
[pid=16666] vsize: 74476
Current children cumulated CPU time (s) 938.53
Current children cumulated vsize (Kb) 76600

[startup+950.097 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16666
Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16662/statm): 531 226 485 147 0 384 0
[pid=16662] vsize: 2124
Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 18293 0 0 0 94710 143 0 0 25 0 1 0 1855754519 76263424 18089 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16666/statm): 18619 18089 145 145 0 18474 0
[pid=16666] vsize: 74476
Current children cumulated CPU time (s) 948.54
Current children cumulated vsize (Kb) 76600

[startup+960.098 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16666
Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16662/statm): 531 226 485 147 0 384 0
[pid=16662] vsize: 2124
Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 18293 0 0 0 95710 143 0 0 25 0 1 0 1855754519 76263424 18089 4294967295 134512640 135094434 3221224432 3221223104 134556549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16666/statm): 18619 18089 145 145 0 18474 0
[pid=16666] vsize: 74476
Current children cumulated CPU time (s) 958.54
Current children cumulated vsize (Kb) 76600

[startup+970.098 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16666
Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16662/statm): 531 226 485 147 0 384 0
[pid=16662] vsize: 2124
Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 18293 0 0 0 96710 143 0 0 25 0 1 0 1855754519 76263424 18089 4294967295 134512640 135094434 3221224432 3221223088 134558276 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16666/statm): 18619 18089 145 145 0 18474 0
[pid=16666] vsize: 74476
Current children cumulated CPU time (s) 968.54
Current children cumulated vsize (Kb) 76600

[startup+980.099 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16666
Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16662/statm): 531 226 485 147 0 384 0
[pid=16662] vsize: 2124
Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 18293 0 0 0 97710 143 0 0 25 0 1 0 1855754519 76263424 18089 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16666/statm): 18619 18089 145 145 0 18474 0
[pid=16666] vsize: 74476
Current children cumulated CPU time (s) 978.54
Current children cumulated vsize (Kb) 76600

[startup+990.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16666
Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16662/statm): 531 226 485 147 0 384 0
[pid=16662] vsize: 2124
Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 18293 0 0 0 98710 143 0 0 25 0 1 0 1855754519 76263424 18089 4294967295 134512640 135094434 3221224432 3221223024 134557031 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16666/statm): 18619 18089 145 145 0 18474 0
[pid=16666] vsize: 74476
Current children cumulated CPU time (s) 988.54
Current children cumulated vsize (Kb) 76600

[startup+1000.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16666
Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16662/statm): 531 226 485 147 0 384 0
[pid=16662] vsize: 2124
Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 18293 0 0 0 99711 143 0 0 25 0 1 0 1855754519 76263424 18089 4294967295 134512640 135094434 3221224432 3221223024 134557404 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16666/statm): 18619 18089 145 145 0 18474 0
[pid=16666] vsize: 74476
Current children cumulated CPU time (s) 998.55
Current children cumulated vsize (Kb) 76600

[startup+1010.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16666
Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16662/statm): 531 226 485 147 0 384 0
[pid=16662] vsize: 2124
Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 18293 0 0 0 100711 143 0 0 25 0 1 0 1855754519 76263424 18089 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16666/statm): 18619 18089 145 145 0 18474 0
[pid=16666] vsize: 74476
Current children cumulated CPU time (s) 1008.55
Current children cumulated vsize (Kb) 76600

[startup+1020.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16666
Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16662/statm): 531 226 485 147 0 384 0
[pid=16662] vsize: 2124
Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 18293 0 0 0 101711 143 0 0 25 0 1 0 1855754519 76263424 18089 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16666/statm): 18619 18089 145 145 0 18474 0
[pid=16666] vsize: 74476
Current children cumulated CPU time (s) 1018.55
Current children cumulated vsize (Kb) 76600

[startup+1030.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16666
Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16662/statm): 531 226 485 147 0 384 0
[pid=16662] vsize: 2124
Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 18293 0 0 0 102711 143 0 0 25 0 1 0 1855754519 76263424 18089 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16666/statm): 18619 18089 145 145 0 18474 0
[pid=16666] vsize: 74476
Current children cumulated CPU time (s) 1028.55
Current children cumulated vsize (Kb) 76600

[startup+1040.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16666
Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16662/statm): 531 226 485 147 0 384 0
[pid=16662] vsize: 2124
Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 18293 0 0 0 103712 143 0 0 25 0 1 0 1855754519 76263424 18089 4294967295 134512640 135094434 3221224432 3221223104 134555957 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16666/statm): 18619 18089 145 145 0 18474 0
[pid=16666] vsize: 74476
Current children cumulated CPU time (s) 1038.56
Current children cumulated vsize (Kb) 76600

[startup+1050.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16666
Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16662/statm): 531 226 485 147 0 384 0
[pid=16662] vsize: 2124
Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 18294 0 0 0 104711 143 0 0 25 0 1 0 1855754519 76263424 18090 4294967295 134512640 135094434 3221224432 3221223088 134557996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16666/statm): 18619 18090 145 145 0 18474 0
[pid=16666] vsize: 74476
Current children cumulated CPU time (s) 1048.55
Current children cumulated vsize (Kb) 76600

[startup+1060.1 s]
Raw data (loadavg): 1.07 0.99 0.91 2/57 16666
Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16662/statm): 531 226 485 147 0 384 0
[pid=16662] vsize: 2124
Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 18313 0 0 0 105711 143 0 0 25 0 1 0 1855754519 76328960 18109 4294967295 134512640 135094434 3221224432 3221223088 134557976 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16666/statm): 18635 18109 145 145 0 18490 0
[pid=16666] vsize: 74540
Current children cumulated CPU time (s) 1058.55
Current children cumulated vsize (Kb) 76664

[startup+1070.1 s]
Raw data (loadavg): 1.06 0.99 0.91 2/57 16666
Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16662/statm): 531 226 485 147 0 384 0
[pid=16662] vsize: 2124
Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 18316 0 0 0 106712 143 0 0 25 0 1 0 1855754519 76328960 18112 4294967295 134512640 135094434 3221224432 3221223088 134558004 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16666/statm): 18635 18112 145 145 0 18490 0
[pid=16666] vsize: 74540
Current children cumulated CPU time (s) 1068.56
Current children cumulated vsize (Kb) 76664

[startup+1080.1 s]
Raw data (loadavg): 1.05 0.99 0.91 2/57 16666
Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16662/statm): 531 226 485 147 0 384 0
[pid=16662] vsize: 2124
Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 18316 0 0 0 107712 143 0 0 25 0 1 0 1855754519 76328960 18112 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16666/statm): 18635 18112 145 145 0 18490 0
[pid=16666] vsize: 74540
Current children cumulated CPU time (s) 1078.56
Current children cumulated vsize (Kb) 76664

[startup+1090.1 s]
Raw data (loadavg): 1.04 0.99 0.91 2/57 16666
Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16662/statm): 531 226 485 147 0 384 0
[pid=16662] vsize: 2124
Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 18328 0 0 0 108712 143 0 0 25 0 1 0 1855754519 76394496 18124 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16666/statm): 18651 18124 145 145 0 18506 0
[pid=16666] vsize: 74604
Current children cumulated CPU time (s) 1088.56
Current children cumulated vsize (Kb) 76728

[startup+1100.11 s]
Raw data (loadavg): 1.04 0.99 0.91 2/57 16666
Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16662/statm): 531 226 485 147 0 384 0
[pid=16662] vsize: 2124
Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 18331 0 0 0 109712 143 0 0 25 0 1 0 1855754519 76394496 18127 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16666/statm): 18651 18127 145 145 0 18506 0
[pid=16666] vsize: 74604
Current children cumulated CPU time (s) 1098.56
Current children cumulated vsize (Kb) 76728

[startup+1110.11 s]
Raw data (loadavg): 1.03 0.99 0.91 2/57 16666
Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16662/statm): 531 226 485 147 0 384 0
[pid=16662] vsize: 2124
Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 18331 0 0 0 110713 143 0 0 25 0 1 0 1855754519 76394496 18127 4294967295 134512640 135094434 3221224432 3221223024 134556984 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16666/statm): 18651 18127 145 145 0 18506 0
[pid=16666] vsize: 74604
Current children cumulated CPU time (s) 1108.57
Current children cumulated vsize (Kb) 76728

[startup+1120.11 s]
Raw data (loadavg): 1.03 0.99 0.91 2/57 16666
Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16662/statm): 531 226 485 147 0 384 0
[pid=16662] vsize: 2124
Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 18331 0 0 0 111713 143 0 0 25 0 1 0 1855754519 76394496 18127 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16666/statm): 18651 18127 145 145 0 18506 0
[pid=16666] vsize: 74604
Current children cumulated CPU time (s) 1118.57
Current children cumulated vsize (Kb) 76728

[startup+1130.11 s]
Raw data (loadavg): 1.02 0.99 0.91 2/57 16666
Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16662/statm): 531 226 485 147 0 384 0
[pid=16662] vsize: 2124
Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 18331 0 0 0 112713 143 0 0 25 0 1 0 1855754519 76394496 18127 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16666/statm): 18651 18127 145 145 0 18506 0
[pid=16666] vsize: 74604
Current children cumulated CPU time (s) 1128.57
Current children cumulated vsize (Kb) 76728

[startup+1140.11 s]
Raw data (loadavg): 1.02 0.99 0.91 2/57 16666
Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16662/statm): 531 226 485 147 0 384 0
[pid=16662] vsize: 2124
Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 18331 0 0 0 113713 143 0 0 25 0 1 0 1855754519 76394496 18127 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16666/statm): 18651 18127 145 145 0 18506 0
[pid=16666] vsize: 74604
Current children cumulated CPU time (s) 1138.57
Current children cumulated vsize (Kb) 76728

[startup+1150.11 s]
Raw data (loadavg): 1.01 0.99 0.91 2/57 16666
Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16662/statm): 531 226 485 147 0 384 0
[pid=16662] vsize: 2124
Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 18331 0 0 0 114713 143 0 0 25 0 1 0 1855754519 76394496 18127 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16666/statm): 18651 18127 145 145 0 18506 0
[pid=16666] vsize: 74604
Current children cumulated CPU time (s) 1148.57
Current children cumulated vsize (Kb) 76728

[startup+1160.11 s]
Raw data (loadavg): 1.01 0.99 0.91 2/57 16666
Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16662/statm): 531 226 485 147 0 384 0
[pid=16662] vsize: 2124
Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 18331 0 0 0 115714 143 0 0 25 0 1 0 1855754519 76394496 18127 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16666/statm): 18651 18127 145 145 0 18506 0
[pid=16666] vsize: 74604
Current children cumulated CPU time (s) 1158.58
Current children cumulated vsize (Kb) 76728

[startup+1170.11 s]
Raw data (loadavg): 1.01 0.99 0.91 2/57 16666
Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16662/statm): 531 226 485 147 0 384 0
[pid=16662] vsize: 2124
Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 18333 0 0 0 116714 143 0 0 25 0 1 0 1855754519 76394496 18129 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16666/statm): 18651 18129 145 145 0 18506 0
[pid=16666] vsize: 74604
Current children cumulated CPU time (s) 1168.58
Current children cumulated vsize (Kb) 76728

[startup+1180.11 s]
Raw data (loadavg): 1.09 1.00 0.92 2/57 16666
Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16662/statm): 531 226 485 147 0 384 0
[pid=16662] vsize: 2124
Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 18336 0 0 0 117714 143 0 0 25 0 1 0 1855754519 76394496 18132 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16666/statm): 18651 18132 145 145 0 18506 0
[pid=16666] vsize: 74604
Current children cumulated CPU time (s) 1178.58
Current children cumulated vsize (Kb) 76728

[startup+1190.11 s]
Raw data (loadavg): 1.07 1.00 0.92 2/57 16666
Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16662/statm): 531 226 485 147 0 384 0
[pid=16662] vsize: 2124
Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 18338 0 0 0 118714 143 0 0 25 0 1 0 1855754519 76394496 18134 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16666/statm): 18651 18134 145 145 0 18506 0
[pid=16666] vsize: 74604
Current children cumulated CPU time (s) 1188.58
Current children cumulated vsize (Kb) 76728

[startup+1200.11 s]
Raw data (loadavg): 1.06 1.00 0.92 2/57 16666
Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16662/statm): 531 226 485 147 0 384 0
[pid=16662] vsize: 2124
Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 18341 0 0 0 119715 143 0 0 25 0 1 0 1855754519 76394496 18137 4294967295 134512640 135094434 3221224432 3221223024 134557416 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16666/statm): 18651 18137 145 145 0 18506 0
[pid=16666] vsize: 74604
Current children cumulated CPU time (s) 1198.59
Current children cumulated vsize (Kb) 76728

[startup+1210.11 s]
Raw data (loadavg): 1.05 1.00 0.92 2/57 16666
Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16662/statm): 531 226 485 147 0 384 0
[pid=16662] vsize: 2124
Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 18344 0 0 0 120715 143 0 0 25 0 1 0 1855754519 77443072 18140 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16666/statm): 18907 18140 145 145 0 18762 0
[pid=16666] vsize: 75628
Current children cumulated CPU time (s) 1208.59
Current children cumulated vsize (Kb) 77752



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.11 s]
Raw data (loadavg): 1.05 1.00 0.92 2/57 16666
Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16662/statm): 531 226 485 147 0 384 0
[pid=16662] vsize: 2124
Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 18344 0 0 0 120715 143 0 0 25 0 1 0 1855754519 77443072 18140 4294967295 134512640 135094434 3221224432 3221223088 134557925 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16666/statm): 18907 18140 145 145 0 18762 0
[pid=16666] vsize: 75628
Current children cumulated CPU time (s) 1208.59
Current children cumulated vsize (Kb) 77752

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

Child status: 0
Real time (s): 1210.15
CPU time (s): 1208.63
CPU user time (s): 1207.15
CPU system time (s): 1.47178
CPU usage (%): 99.874
Max. virtual memory (cumulated for all children) (Kb): 77752

Verifier Data

ERROR: no interpretation found !