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/miplib/normalized-mps-v2-13-7-vpm1.opb
MD5SUM96fe6be9d2b9e3e89a4b05733b0daf45
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 6115

Launcher Data

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.177
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:        857948 kB
Buffers:         25432 kB
Cached:         118416 kB
SwapCached:        856 kB
Active:          33364 kB
Inactive:       113160 kB
HighTotal:      131008 kB
HighFree:        27048 kB
LowTotal:       903652 kB
LowFree:        830900 kB
SwapTotal:     2097892 kB
SwapFree:      2096528 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5732 kB
Slab:            24644 kB
Committed_AS:    64148 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-09-20 03:48:44 (client local time) WITH STATUS 0 IN 1208.64 SECONDS
stats: 3276 7 1208.64 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/27835/stat): 27835 (minisat+_script) R 27834 27835 31027 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1855264836 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 1 0 0
Raw data (/proc/27835/statm): 174 3 169 147 0 27 0
[pid=27835] 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=27836
New process pid=27837
New process pid=27838
execve syscall for /bin/sed executable
One traced child (pid=27837) 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=27838) exited with status: 0
One traced child (pid=27836) exited with status: 0
New process pid=27839
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc18/normalized-mps-v2-13-7-vpm1.opb

[startup+10.004 s]
Raw data (loadavg): 0.93 0.97 0.91 2/57 27839
Raw data (/proc/27835/stat): 27835 (minisat+_script) S 27834 27835 31027 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855264836 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27835/statm): 531 226 485 147 0 384 0
[pid=27835] vsize: 2124
Raw data (/proc/27839/stat): 27839 (minisat+_64-bit) R 27835 27835 31027 0 -1 0 4496 0 0 0 957 18 0 0 25 0 1 0 1855264841 19357696 4292 4294967295 134512640 135094434 3221224432 3221222912 134781572 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27839/statm): 4726 4292 145 145 0 4581 0
[pid=27839] vsize: 18904
Current children cumulated CPU time (s) 9.76
Current children cumulated vsize (Kb) 21028

[startup+20.0059 s]
Raw data (loadavg): 0.94 0.97 0.91 2/57 27839
Raw data (/proc/27835/stat): 27835 (minisat+_script) S 27834 27835 31027 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855264836 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27835/statm): 531 226 485 147 0 384 0
[pid=27835] vsize: 2124
Raw data (/proc/27839/stat): 27839 (minisat+_64-bit) R 27835 27835 31027 0 -1 0 4858 0 0 0 1951 21 0 0 25 0 1 0 1855264841 20811776 4654 4294967295 134512640 135094434 3221224432 3221223120 134554685 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27839/statm): 5081 4654 145 145 0 4936 0
[pid=27839] vsize: 20324
Current children cumulated CPU time (s) 19.73
Current children cumulated vsize (Kb) 22448

[startup+30.0068 s]
Raw data (loadavg): 0.95 0.97 0.91 2/57 27839
Raw data (/proc/27835/stat): 27835 (minisat+_script) S 27834 27835 31027 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855264836 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27835/statm): 531 226 485 147 0 384 0
[pid=27835] vsize: 2124
Raw data (/proc/27839/stat): 27839 (minisat+_64-bit) R 27835 27835 31027 0 -1 0 5239 0 0 0 2944 23 0 0 25 0 1 0 1855264841 22396928 5035 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27839/statm): 5468 5035 145 145 0 5323 0
[pid=27839] vsize: 21872
Current children cumulated CPU time (s) 29.68
Current children cumulated vsize (Kb) 23996

[startup+40.0068 s]
Raw data (loadavg): 0.95 0.97 0.91 2/57 27839
Raw data (/proc/27835/stat): 27835 (minisat+_script) S 27834 27835 31027 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855264836 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27835/statm): 531 226 485 147 0 384 0
[pid=27835] vsize: 2124
Raw data (/proc/27839/stat): 27839 (minisat+_64-bit) R 27835 27835 31027 0 -1 0 5613 0 0 0 3938 26 0 0 25 0 1 0 1855264841 24027136 5409 4294967295 134512640 135094434 3221224432 3221223088 134558187 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27839/statm): 5866 5409 145 145 0 5721 0
[pid=27839] vsize: 23464
Current children cumulated CPU time (s) 39.65
Current children cumulated vsize (Kb) 25588

[startup+50.0077 s]
Raw data (loadavg): 0.96 0.97 0.91 2/57 27839
Raw data (/proc/27835/stat): 27835 (minisat+_script) S 27834 27835 31027 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855264836 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27835/statm): 531 226 485 147 0 384 0
[pid=27835] vsize: 2124
Raw data (/proc/27839/stat): 27839 (minisat+_64-bit) R 27835 27835 31027 0 -1 0 5999 0 0 0 4931 30 0 0 25 0 1 0 1855264841 25575424 5795 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27839/statm): 6244 5795 145 145 0 6099 0
[pid=27839] vsize: 24976
Current children cumulated CPU time (s) 49.62
Current children cumulated vsize (Kb) 27100

[startup+60.0076 s]
Raw data (loadavg): 0.97 0.97 0.91 2/57 27839
Raw data (/proc/27835/stat): 27835 (minisat+_script) S 27834 27835 31027 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855264836 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27835/statm): 531 226 485 147 0 384 0
[pid=27835] vsize: 2124
Raw data (/proc/27839/stat): 27839 (minisat+_64-bit) R 27835 27835 31027 0 -1 0 6338 0 0 0 5925 32 0 0 25 0 1 0 1855264841 26939392 6134 4294967295 134512640 135094434 3221224432 3221223088 134558187 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27839/statm): 6577 6134 145 145 0 6432 0
[pid=27839] vsize: 26308
Current children cumulated CPU time (s) 59.58
Current children cumulated vsize (Kb) 28432

[startup+70.0085 s]
Raw data (loadavg): 0.97 0.97 0.91 2/57 27839
Raw data (/proc/27835/stat): 27835 (minisat+_script) S 27834 27835 31027 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855264836 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27835/statm): 531 226 485 147 0 384 0
[pid=27835] vsize: 2124
Raw data (/proc/27839/stat): 27839 (minisat+_64-bit) R 27835 27835 31027 0 -1 0 6590 0 0 0 6921 34 0 0 25 0 1 0 1855264841 27942912 6386 4294967295 134512640 135094434 3221224432 3221223088 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27839/statm): 6822 6386 145 145 0 6677 0
[pid=27839] vsize: 27288
Current children cumulated CPU time (s) 69.56
Current children cumulated vsize (Kb) 29412

[startup+80.0095 s]
Raw data (loadavg): 0.98 0.97 0.91 2/57 27839
Raw data (/proc/27835/stat): 27835 (minisat+_script) S 27834 27835 31027 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855264836 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27835/statm): 531 226 485 147 0 384 0
[pid=27835] vsize: 2124
Raw data (/proc/27839/stat): 27839 (minisat+_64-bit) R 27835 27835 31027 0 -1 0 6961 0 0 0 7915 37 0 0 25 0 1 0 1855264841 29429760 6757 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27839/statm): 7185 6757 145 145 0 7040 0
[pid=27839] vsize: 28740
Current children cumulated CPU time (s) 79.53
Current children cumulated vsize (Kb) 30864

[startup+90.0104 s]
Raw data (loadavg): 0.98 0.97 0.91 2/57 27839
Raw data (/proc/27835/stat): 27835 (minisat+_script) S 27834 27835 31027 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855264836 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27835/statm): 531 226 485 147 0 384 0
[pid=27835] vsize: 2124
Raw data (/proc/27839/stat): 27839 (minisat+_64-bit) R 27835 27835 31027 0 -1 0 7333 0 0 0 8909 39 0 0 25 0 1 0 1855264841 31195136 7129 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27839/statm): 7616 7129 145 145 0 7471 0
[pid=27839] vsize: 30464
Current children cumulated CPU time (s) 89.49
Current children cumulated vsize (Kb) 32588

[startup+100.011 s]
Raw data (loadavg): 0.98 0.97 0.91 2/57 27839
Raw data (/proc/27835/stat): 27835 (minisat+_script) S 27834 27835 31027 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855264836 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27835/statm): 531 226 485 147 0 384 0
[pid=27835] vsize: 2124
Raw data (/proc/27839/stat): 27839 (minisat+_64-bit) R 27835 27835 31027 0 -1 0 7631 0 0 0 9905 41 0 0 25 0 1 0 1855264841 32382976 7427 4294967295 134512640 135094434 3221224432 3221223056 134562149 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27839/statm): 7906 7427 145 145 0 7761 0
[pid=27839] vsize: 31624
Current children cumulated CPU time (s) 99.47
Current children cumulated vsize (Kb) 33748

[startup+110.012 s]
Raw data (loadavg): 0.98 0.97 0.91 2/57 27839
Raw data (/proc/27835/stat): 27835 (minisat+_script) S 27834 27835 31027 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855264836 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27835/statm): 531 226 485 147 0 384 0
[pid=27835] vsize: 2124
Raw data (/proc/27839/stat): 27839 (minisat+_64-bit) R 27835 27835 31027 0 -1 0 7968 0 0 0 10899 42 0 0 25 0 1 0 1855264841 33738752 7764 4294967295 134512640 135094434 3221224432 3221223092 134553494 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27839/statm): 8237 7764 145 145 0 8092 0
[pid=27839] vsize: 32948
Current children cumulated CPU time (s) 109.42
Current children cumulated vsize (Kb) 35072

[startup+120.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27839
Raw data (/proc/27835/stat): 27835 (minisat+_script) S 27834 27835 31027 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855264836 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27835/statm): 531 226 485 147 0 384 0
[pid=27835] vsize: 2124
Raw data (/proc/27839/stat): 27839 (minisat+_64-bit) R 27835 27835 31027 0 -1 0 8108 0 0 0 11898 43 0 0 25 0 1 0 1855264841 34308096 7904 4294967295 134512640 135094434 3221224432 3221223024 134557157 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27839/statm): 8376 7904 145 145 0 8231 0
[pid=27839] vsize: 33504
Current children cumulated CPU time (s) 119.42
Current children cumulated vsize (Kb) 35628

[startup+130.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27839
Raw data (/proc/27835/stat): 27835 (minisat+_script) S 27834 27835 31027 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855264836 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27835/statm): 531 226 485 147 0 384 0
[pid=27835] vsize: 2124
Raw data (/proc/27839/stat): 27839 (minisat+_64-bit) R 27835 27835 31027 0 -1 0 8260 0 0 0 12895 44 0 0 25 0 1 0 1855264841 34918400 8056 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27839/statm): 8525 8056 145 145 0 8380 0
[pid=27839] vsize: 34100
Current children cumulated CPU time (s) 129.4
Current children cumulated vsize (Kb) 36224

[startup+140.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27839
Raw data (/proc/27835/stat): 27835 (minisat+_script) S 27834 27835 31027 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855264836 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27835/statm): 531 226 485 147 0 384 0
[pid=27835] vsize: 2124
Raw data (/proc/27839/stat): 27839 (minisat+_64-bit) R 27835 27835 31027 0 -1 0 8501 0 0 0 13891 46 0 0 25 0 1 0 1855264841 35889152 8297 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27839/statm): 8762 8297 145 145 0 8617 0
[pid=27839] vsize: 35048
Current children cumulated CPU time (s) 139.38
Current children cumulated vsize (Kb) 37172

[startup+150.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27839
Raw data (/proc/27835/stat): 27835 (minisat+_script) S 27834 27835 31027 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855264836 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27835/statm): 531 226 485 147 0 384 0
[pid=27835] vsize: 2124
Raw data (/proc/27839/stat): 27839 (minisat+_64-bit) R 27835 27835 31027 0 -1 0 8810 0 0 0 14885 49 0 0 25 0 1 0 1855264841 37154816 8606 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27839/statm): 9071 8606 145 145 0 8926 0
[pid=27839] vsize: 36284
Current children cumulated CPU time (s) 149.35
Current children cumulated vsize (Kb) 38408

[startup+160.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27839
Raw data (/proc/27835/stat): 27835 (minisat+_script) S 27834 27835 31027 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855264836 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27835/statm): 531 226 485 147 0 384 0
[pid=27835] vsize: 2124
Raw data (/proc/27839/stat): 27839 (minisat+_64-bit) R 27835 27835 31027 0 -1 0 9056 0 0 0 15881 51 0 0 25 0 1 0 1855264841 38150144 8852 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27839/statm): 9314 8852 145 145 0 9169 0
[pid=27839] vsize: 37256
Current children cumulated CPU time (s) 159.33
Current children cumulated vsize (Kb) 39380

[startup+170.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27839
Raw data (/proc/27835/stat): 27835 (minisat+_script) S 27834 27835 31027 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855264836 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27835/statm): 531 226 485 147 0 384 0
[pid=27835] vsize: 2124
Raw data (/proc/27839/stat): 27839 (minisat+_64-bit) R 27835 27835 31027 0 -1 0 9427 0 0 0 16874 54 0 0 25 0 1 0 1855264841 39649280 9223 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27839/statm): 9680 9223 145 145 0 9535 0
[pid=27839] vsize: 38720
Current children cumulated CPU time (s) 169.29
Current children cumulated vsize (Kb) 40844

[startup+180.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27839
Raw data (/proc/27835/stat): 27835 (minisat+_script) S 27834 27835 31027 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855264836 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27835/statm): 531 226 485 147 0 384 0
[pid=27835] vsize: 2124
Raw data (/proc/27839/stat): 27839 (minisat+_64-bit) R 27835 27835 31027 0 -1 0 9869 0 0 0 17868 57 0 0 25 0 1 0 1855264841 41443328 9665 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27839/statm): 10118 9665 145 145 0 9973 0
[pid=27839] vsize: 40472
Current children cumulated CPU time (s) 179.26
Current children cumulated vsize (Kb) 42596

[startup+190.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27839
Raw data (/proc/27835/stat): 27835 (minisat+_script) S 27834 27835 31027 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855264836 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27835/statm): 531 226 485 147 0 384 0
[pid=27835] vsize: 2124
Raw data (/proc/27839/stat): 27839 (minisat+_64-bit) R 27835 27835 31027 0 -1 0 10432 0 0 0 18858 61 0 0 25 0 1 0 1855264841 43716608 10228 4294967295 134512640 135094434 3221224432 3221223024 134557310 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27839/statm): 10673 10228 145 145 0 10528 0
[pid=27839] vsize: 42692
Current children cumulated CPU time (s) 189.2
Current children cumulated vsize (Kb) 44816

[startup+200.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27839
Raw data (/proc/27835/stat): 27835 (minisat+_script) S 27834 27835 31027 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855264836 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27835/statm): 531 226 485 147 0 384 0
[pid=27835] vsize: 2124
Raw data (/proc/27839/stat): 27839 (minisat+_64-bit) T 27835 27835 31027 0 -1 0 10802 0 0 0 19852 63 0 0 25 0 1 0 1855264841 45740032 10598 4294967295 134512640 135094434 3221224432 3221222796 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/27839/statm): 11167 10598 145 145 0 11022 0
[pid=27839] vsize: 44668
Current children cumulated CPU time (s) 199.16
Current children cumulated vsize (Kb) 46792

[startup+210.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27839
Raw data (/proc/27835/stat): 27835 (minisat+_script) S 27834 27835 31027 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855264836 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27835/statm): 531 226 485 147 0 384 0
[pid=27835] vsize: 2124
Raw data (/proc/27839/stat): 27839 (minisat+_64-bit) R 27835 27835 31027 0 -1 0 11121 0 0 0 20847 65 0 0 25 0 1 0 1855264841 47026176 10917 4294967295 134512640 135094434 3221224432 3221223088 134557900 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27839/statm): 11481 10917 145 145 0 11336 0
[pid=27839] vsize: 45924
Current children cumulated CPU time (s) 209.13
Current children cumulated vsize (Kb) 48048

[startup+220.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27839
Raw data (/proc/27835/stat): 27835 (minisat+_script) S 27834 27835 31027 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855264836 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27835/statm): 531 226 485 147 0 384 0
[pid=27835] vsize: 2124
Raw data (/proc/27839/stat): 27839 (minisat+_64-bit) R 27835 27835 31027 0 -1 0 11417 0 0 0 21842 67 0 0 25 0 1 0 1855264841 48230400 11213 4294967295 134512640 135094434 3221224432 3221223024 134557199 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27839/statm): 11775 11213 145 145 0 11630 0
[pid=27839] vsize: 47100
Current children cumulated CPU time (s) 219.1
Current children cumulated vsize (Kb) 49224

[startup+230.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27839
Raw data (/proc/27835/stat): 27835 (minisat+_script) S 27834 27835 31027 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855264836 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27835/statm): 531 226 485 147 0 384 0
[pid=27835] vsize: 2124
Raw data (/proc/27839/stat): 27839 (minisat+_64-bit) R 27835 27835 31027 0 -1 0 11689 0 0 0 22838 69 0 0 25 0 1 0 1855264841 49332224 11485 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27839/statm): 12044 11485 145 145 0 11899 0
[pid=27839] vsize: 48176
Current children cumulated CPU time (s) 229.08
Current children cumulated vsize (Kb) 50300

[startup+240.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27839
Raw data (/proc/27835/stat): 27835 (minisat+_script) S 27834 27835 31027 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855264836 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27835/statm): 531 226 485 147 0 384 0
[pid=27835] vsize: 2124
Raw data (/proc/27839/stat): 27839 (minisat+_64-bit) R 27835 27835 31027 0 -1 0 11954 0 0 0 23833 71 0 0 25 0 1 0 1855264841 50409472 11750 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27839/statm): 12307 11750 145 145 0 12162 0
[pid=27839] vsize: 49228
Current children cumulated CPU time (s) 239.05
Current children cumulated vsize (Kb) 51352

[startup+250.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27839
Raw data (/proc/27835/stat): 27835 (minisat+_script) S 27834 27835 31027 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855264836 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27835/statm): 531 226 485 147 0 384 0
[pid=27835] vsize: 2124
Raw data (/proc/27839/stat): 27839 (minisat+_64-bit) R 27835 27835 31027 0 -1 0 12188 0 0 0 24829 73 0 0 25 0 1 0 1855264841 51355648 11984 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27839/statm): 12538 11984 145 145 0 12393 0
[pid=27839] vsize: 50152
Current children cumulated CPU time (s) 249.03
Current children cumulated vsize (Kb) 52276

[startup+260.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27839
Raw data (/proc/27835/stat): 27835 (minisat+_script) S 27834 27835 31027 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855264836 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27835/statm): 531 226 485 147 0 384 0
[pid=27835] vsize: 2124
Raw data (/proc/27839/stat): 27839 (minisat+_64-bit) R 27835 27835 31027 0 -1 0 12416 0 0 0 25826 75 0 0 25 0 1 0 1855264841 52273152 12212 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27839/statm): 12762 12212 145 145 0 12617 0
[pid=27839] vsize: 51048
Current children cumulated CPU time (s) 259.02
Current children cumulated vsize (Kb) 53172

[startup+270.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27839
Raw data (/proc/27835/stat): 27835 (minisat+_script) S 27834 27835 31027 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855264836 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27835/statm): 531 226 485 147 0 384 0
[pid=27835] vsize: 2124
Raw data (/proc/27839/stat): 27839 (minisat+_64-bit) R 27835 27835 31027 0 -1 0 12673 0 0 0 26822 76 0 0 25 0 1 0 1855264841 53313536 12469 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27839/statm): 13016 12469 145 145 0 12871 0
[pid=27839] vsize: 52064
Current children cumulated CPU time (s) 268.99
Current children cumulated vsize (Kb) 54188

[startup+280.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27839
Raw data (/proc/27835/stat): 27835 (minisat+_script) S 27834 27835 31027 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855264836 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27835/statm): 531 226 485 147 0 384 0
[pid=27835] vsize: 2124
Raw data (/proc/27839/stat): 27839 (minisat+_64-bit) R 27835 27835 31027 0 -1 0 12906 0 0 0 27818 78 0 0 25 0 1 0 1855264841 54259712 12702 4294967295 134512640 135094434 3221224432 3221223056 134557612 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27839/statm): 13247 12702 145 145 0 13102 0
[pid=27839] vsize: 52988
Current children cumulated CPU time (s) 278.97
Current children cumulated vsize (Kb) 55112

[startup+290.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27839
Raw data (/proc/27835/stat): 27835 (minisat+_script) S 27834 27835 31027 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855264836 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27835/statm): 531 226 485 147 0 384 0
[pid=27835] vsize: 2124
Raw data (/proc/27839/stat): 27839 (minisat+_64-bit) R 27835 27835 31027 0 -1 0 13132 0 0 0 28814 80 0 0 25 0 1 0 1855264841 55185408 12928 4294967295 134512640 135094434 3221224432 3221223104 134556266 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27839/statm): 13473 12928 145 145 0 13328 0
[pid=27839] vsize: 53892
Current children cumulated CPU time (s) 288.95
Current children cumulated vsize (Kb) 56016

[startup+300.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27839
Raw data (/proc/27835/stat): 27835 (minisat+_script) S 27834 27835 31027 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855264836 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27835/statm): 531 226 485 147 0 384 0
[pid=27835] vsize: 2124
Raw data (/proc/27839/stat): 27839 (minisat+_64-bit) R 27835 27835 31027 0 -1 0 13381 0 0 0 29810 82 0 0 25 0 1 0 1855264841 56184832 13177 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27839/statm): 13717 13177 145 145 0 13572 0
[pid=27839] vsize: 54868
Current children cumulated CPU time (s) 298.93
Current children cumulated vsize (Kb) 56992

[startup+310.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27839
Raw data (/proc/27835/stat): 27835 (minisat+_script) S 27834 27835 31027 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855264836 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27835/statm): 531 226 485 147 0 384 0
[pid=27835] vsize: 2124
Raw data (/proc/27839/stat): 27839 (minisat+_64-bit) R 27835 27835 31027 0 -1 0 13594 0 0 0 30807 83 0 0 25 0 1 0 1855264841 57049088 13390 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27839/statm): 13928 13390 145 145 0 13783 0
[pid=27839] vsize: 55712
Current children cumulated CPU time (s) 308.91
Current children cumulated vsize (Kb) 57836

[startup+320.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27839
Raw data (/proc/27835/stat): 27835 (minisat+_script) S 27834 27835 31027 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855264836 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27835/statm): 531 226 485 147 0 384 0
[pid=27835] vsize: 2124
Raw data (/proc/27839/stat): 27839 (minisat+_64-bit) R 27835 27835 31027 0 -1 0 13776 0 0 0 31804 85 0 0 25 0 1 0 1855264841 57790464 13572 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27839/statm): 14109 13572 145 145 0 13964 0
[pid=27839] vsize: 56436
Current children cumulated CPU time (s) 318.9
Current children cumulated vsize (Kb) 58560

[startup+330.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27839
Raw data (/proc/27835/stat): 27835 (minisat+_script) S 27834 27835 31027 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855264836 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27835/statm): 531 226 485 147 0 384 0
[pid=27835] vsize: 2124
Raw data (/proc/27839/stat): 27839 (minisat+_64-bit) R 27835 27835 31027 0 -1 0 13957 0 0 0 32801 86 0 0 25 0 1 0 1855264841 58523648 13753 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27839/statm): 14288 13753 145 145 0 14143 0
[pid=27839] vsize: 57152
Current children cumulated CPU time (s) 328.88
Current children cumulated vsize (Kb) 59276

[startup+340.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27839
Raw data (/proc/27835/stat): 27835 (minisat+_script) S 27834 27835 31027 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855264836 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27835/statm): 531 226 485 147 0 384 0
[pid=27835] vsize: 2124
Raw data (/proc/27839/stat): 27839 (minisat+_64-bit) R 27835 27835 31027 0 -1 0 14162 0 0 0 33798 87 0 0 25 0 1 0 1855264841 59379712 13958 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27839/statm): 14497 13958 145 145 0 14352 0
[pid=27839] vsize: 57988
Current children cumulated CPU time (s) 338.86
Current children cumulated vsize (Kb) 60112

[startup+350.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27839
Raw data (/proc/27835/stat): 27835 (minisat+_script) S 27834 27835 31027 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855264836 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27835/statm): 531 226 485 147 0 384 0
[pid=27835] vsize: 2124
Raw data (/proc/27839/stat): 27839 (minisat+_64-bit) R 27835 27835 31027 0 -1 0 14372 0 0 0 34795 89 0 0 25 0 1 0 1855264841 60239872 14168 4294967295 134512640 135094434 3221224432 3221223024 134557331 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27839/statm): 14707 14168 145 145 0 14562 0
[pid=27839] vsize: 58828
Current children cumulated CPU time (s) 348.85
Current children cumulated vsize (Kb) 60952

[startup+360.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27839
Raw data (/proc/27835/stat): 27835 (minisat+_script) S 27834 27835 31027 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855264836 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27835/statm): 531 226 485 147 0 384 0
[pid=27835] vsize: 2124
Raw data (/proc/27839/stat): 27839 (minisat+_64-bit) R 27835 27835 31027 0 -1 0 14539 0 0 0 35792 90 0 0 25 0 1 0 1855264841 60940288 14335 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27839/statm): 14878 14335 145 145 0 14733 0
[pid=27839] vsize: 59512
Current children cumulated CPU time (s) 358.83
Current children cumulated vsize (Kb) 61636

[startup+370.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27839
Raw data (/proc/27835/stat): 27835 (minisat+_script) S 27834 27835 31027 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855264836 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27835/statm): 531 226 485 147 0 384 0
[pid=27835] vsize: 2124
Raw data (/proc/27839/stat): 27839 (minisat+_64-bit) R 27835 27835 31027 0 -1 0 14697 0 0 0 36790 91 0 0 25 0 1 0 1855264841 61603840 14493 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27839/statm): 15040 14493 145 145 0 14895 0
[pid=27839] vsize: 60160
Current children cumulated CPU time (s) 368.82
Current children cumulated vsize (Kb) 62284

[startup+380.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27839
Raw data (/proc/27835/stat): 27835 (minisat+_script) S 27834 27835 31027 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855264836 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27835/statm): 531 226 485 147 0 384 0
[pid=27835] vsize: 2124
Raw data (/proc/27839/stat): 27839 (minisat+_64-bit) R 27835 27835 31027 0 -1 0 14852 0 0 0 37788 92 0 0 25 0 1 0 1855264841 62214144 14648 4294967295 134512640 135094434 3221224432 3221223088 134558007 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27839/statm): 15189 14648 145 145 0 15044 0
[pid=27839] vsize: 60756
Current children cumulated CPU time (s) 378.81
Current children cumulated vsize (Kb) 62880

[startup+390.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27839
Raw data (/proc/27835/stat): 27835 (minisat+_script) S 27834 27835 31027 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855264836 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27835/statm): 531 226 485 147 0 384 0
[pid=27835] vsize: 2124
Raw data (/proc/27839/stat): 27839 (minisat+_64-bit) R 27835 27835 31027 0 -1 0 15084 0 0 0 38784 93 0 0 25 0 1 0 1855264841 63139840 14880 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27839/statm): 15415 14880 145 145 0 15270 0
[pid=27839] vsize: 61660
Current children cumulated CPU time (s) 388.78
Current children cumulated vsize (Kb) 63784

[startup+400.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27839
Raw data (/proc/27835/stat): 27835 (minisat+_script) S 27834 27835 31027 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855264836 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27835/statm): 531 226 485 147 0 384 0
[pid=27835] vsize: 2124
Raw data (/proc/27839/stat): 27839 (minisat+_64-bit) R 27835 27835 31027 0 -1 0 15225 0 0 0 39782 94 0 0 25 0 1 0 1855264841 63713280 15021 4294967295 134512640 135094434 3221224432 3221223088 134558007 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27839/statm): 15555 15021 145 145 0 15410 0
[pid=27839] vsize: 62220
Current children cumulated CPU time (s) 398.77
Current children cumulated vsize (Kb) 64344

[startup+410.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27839
Raw data (/proc/27835/stat): 27835 (minisat+_script) S 27834 27835 31027 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855264836 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27835/statm): 531 226 485 147 0 384 0
[pid=27835] vsize: 2124
Raw data (/proc/27839/stat): 27839 (minisat+_64-bit) R 27835 27835 31027 0 -1 0 15379 0 0 0 40779 95 0 0 25 0 1 0 1855264841 64327680 15175 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27839/statm): 15705 15175 145 145 0 15560 0
[pid=27839] vsize: 62820
Current children cumulated CPU time (s) 408.75
Current children cumulated vsize (Kb) 64944

[startup+420.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27839
Raw data (/proc/27835/stat): 27835 (minisat+_script) S 27834 27835 31027 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855264836 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27835/statm): 531 226 485 147 0 384 0
[pid=27835] vsize: 2124
Raw data (/proc/27839/stat): 27839 (minisat+_64-bit) R 27835 27835 31027 0 -1 0 15518 0 0 0 41775 96 0 0 25 0 1 0 1855264841 64884736 15314 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27839/statm): 15841 15314 145 145 0 15696 0
[pid=27839] vsize: 63364
Current children cumulated CPU time (s) 418.72
Current children cumulated vsize (Kb) 65488

[startup+430.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27839
Raw data (/proc/27835/stat): 27835 (minisat+_script) S 27834 27835 31027 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855264836 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27835/statm): 531 226 485 147 0 384 0
[pid=27835] vsize: 2124
Raw data (/proc/27839/stat): 27839 (minisat+_64-bit) R 27835 27835 31027 0 -1 0 15685 0 0 0 42773 97 0 0 25 0 1 0 1855264841 65601536 15481 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27839/statm): 16016 15481 145 145 0 15871 0
[pid=27839] vsize: 64064
Current children cumulated CPU time (s) 428.71
Current children cumulated vsize (Kb) 66188

[startup+440.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27839
Raw data (/proc/27835/stat): 27835 (minisat+_script) S 27834 27835 31027 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855264836 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27835/statm): 531 226 485 147 0 384 0
[pid=27835] vsize: 2124
Raw data (/proc/27839/stat): 27839 (minisat+_64-bit) R 27835 27835 31027 0 -1 0 15826 0 0 0 43771 98 0 0 25 0 1 0 1855264841 66179072 15622 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27839/statm): 16157 15622 145 145 0 16012 0
[pid=27839] vsize: 64628
Current children cumulated CPU time (s) 438.7
Current children cumulated vsize (Kb) 66752

[startup+450.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27839
Raw data (/proc/27835/stat): 27835 (minisat+_script) S 27834 27835 31027 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855264836 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27835/statm): 531 226 485 147 0 384 0
[pid=27835] vsize: 2124
Raw data (/proc/27839/stat): 27839 (minisat+_64-bit) R 27835 27835 31027 0 -1 0 15961 0 0 0 44768 99 0 0 25 0 1 0 1855264841 66719744 15757 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27839/statm): 16289 15757 145 145 0 16144 0
[pid=27839] vsize: 65156
Current children cumulated CPU time (s) 448.68
Current children cumulated vsize (Kb) 67280

[startup+460.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27839
Raw data (/proc/27835/stat): 27835 (minisat+_script) S 27834 27835 31027 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855264836 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27835/statm): 531 226 485 147 0 384 0
[pid=27835] vsize: 2124
Raw data (/proc/27839/stat): 27839 (minisat+_64-bit) R 27835 27835 31027 0 -1 0 16090 0 0 0 45766 100 0 0 25 0 1 0 1855264841 67235840 15886 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27839/statm): 16415 15886 145 145 0 16270 0
[pid=27839] vsize: 65660
Current children cumulated CPU time (s) 458.67
Current children cumulated vsize (Kb) 67784

[startup+470.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27839
Raw data (/proc/27835/stat): 27835 (minisat+_script) S 27834 27835 31027 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855264836 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27835/statm): 531 226 485 147 0 384 0
[pid=27835] vsize: 2124
Raw data (/proc/27839/stat): 27839 (minisat+_64-bit) R 27835 27835 31027 0 -1 0 16204 0 0 0 46764 101 0 0 25 0 1 0 1855264841 67694592 16000 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27839/statm): 16527 16000 145 145 0 16382 0
[pid=27839] vsize: 66108
Current children cumulated CPU time (s) 468.66
Current children cumulated vsize (Kb) 68232

[startup+480.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27839
Raw data (/proc/27835/stat): 27835 (minisat+_script) S 27834 27835 31027 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855264836 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27835/statm): 531 226 485 147 0 384 0
[pid=27835] vsize: 2124
Raw data (/proc/27839/stat): 27839 (minisat+_64-bit) R 27835 27835 31027 0 -1 0 16311 0 0 0 47761 102 0 0 25 0 1 0 1855264841 68116480 16107 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27839/statm): 16630 16107 145 145 0 16485 0
[pid=27839] vsize: 66520
Current children cumulated CPU time (s) 478.64
Current children cumulated vsize (Kb) 68644

[startup+490.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27839
Raw data (/proc/27835/stat): 27835 (minisat+_script) S 27834 27835 31027 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855264836 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27835/statm): 531 226 485 147 0 384 0
[pid=27835] vsize: 2124
Raw data (/proc/27839/stat): 27839 (minisat+_64-bit) R 27835 27835 31027 0 -1 0 16422 0 0 0 48759 103 0 0 25 0 1 0 1855264841 68587520 16218 4294967295 134512640 135094434 3221224432 3221223024 134556802 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27839/statm): 16745 16218 145 145 0 16600 0
[pid=27839] vsize: 66980
Current children cumulated CPU time (s) 488.63
Current children cumulated vsize (Kb) 69104

[startup+500.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27839
Raw data (/proc/27835/stat): 27835 (minisat+_script) S 27834 27835 31027 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855264836 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27835/statm): 531 226 485 147 0 384 0
[pid=27835] vsize: 2124
Raw data (/proc/27839/stat): 27839 (minisat+_64-bit) R 27835 27835 31027 0 -1 0 16550 0 0 0 49757 104 0 0 25 0 1 0 1855264841 69136384 16346 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27839/statm): 16879 16346 145 145 0 16734 0
[pid=27839] vsize: 67516
Current children cumulated CPU time (s) 498.62
Current children cumulated vsize (Kb) 69640

[startup+510.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27839
Raw data (/proc/27835/stat): 27835 (minisat+_script) S 27834 27835 31027 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855264836 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27835/statm): 531 226 485 147 0 384 0
[pid=27835] vsize: 2124
Raw data (/proc/27839/stat): 27839 (minisat+_64-bit) R 27835 27835 31027 0 -1 0 16657 0 0 0 50756 105 0 0 25 0 1 0 1855264841 69578752 16453 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27839/statm): 16987 16453 145 145 0 16842 0
[pid=27839] vsize: 67948
Current children cumulated CPU time (s) 508.62
Current children cumulated vsize (Kb) 70072

[startup+520.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27839
Raw data (/proc/27835/stat): 27835 (minisat+_script) S 27834 27835 31027 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855264836 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27835/statm): 531 226 485 147 0 384 0
[pid=27835] vsize: 2124
Raw data (/proc/27839/stat): 27839 (minisat+_64-bit) R 27835 27835 31027 0 -1 0 16767 0 0 0 51753 106 0 0 25 0 1 0 1855264841 70017024 16563 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27839/statm): 17094 16563 145 145 0 16949 0
[pid=27839] vsize: 68376
Current children cumulated CPU time (s) 518.6
Current children cumulated vsize (Kb) 70500

[startup+530.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27839
Raw data (/proc/27835/stat): 27835 (minisat+_script) S 27834 27835 31027 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855264836 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27835/statm): 531 226 485 147 0 384 0
[pid=27835] vsize: 2124
Raw data (/proc/27839/stat): 27839 (minisat+_64-bit) R 27835 27835 31027 0 -1 0 16872 0 0 0 52752 107 0 0 25 0 1 0 1855264841 70443008 16668 4294967295 134512640 135094434 3221224432 3221223088 134557900 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27839/statm): 17198 16668 145 145 0 17053 0
[pid=27839] vsize: 68792
Current children cumulated CPU time (s) 528.6
Current children cumulated vsize (Kb) 70916

[startup+540.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27839
Raw data (/proc/27835/stat): 27835 (minisat+_script) S 27834 27835 31027 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855264836 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27835/statm): 531 226 485 147 0 384 0
[pid=27835] vsize: 2124
Raw data (/proc/27839/stat): 27839 (minisat+_64-bit) R 27835 27835 31027 0 -1 0 16974 0 0 0 53751 107 0 0 25 0 1 0 1855264841 70848512 16770 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27839/statm): 17297 16770 145 145 0 17152 0
[pid=27839] vsize: 69188
Current children cumulated CPU time (s) 538.59
Current children cumulated vsize (Kb) 71312

[startup+550.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27839
Raw data (/proc/27835/stat): 27835 (minisat+_script) S 27834 27835 31027 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855264836 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27835/statm): 531 226 485 147 0 384 0
[pid=27835] vsize: 2124
Raw data (/proc/27839/stat): 27839 (minisat+_64-bit) R 27835 27835 31027 0 -1 0 17072 0 0 0 54749 107 0 0 25 0 1 0 1855264841 71241728 16868 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27839/statm): 17393 16868 145 145 0 17248 0
[pid=27839] vsize: 69572
Current children cumulated CPU time (s) 548.57
Current children cumulated vsize (Kb) 71696

[startup+560.051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27839
Raw data (/proc/27835/stat): 27835 (minisat+_script) S 27834 27835 31027 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855264836 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27835/statm): 531 226 485 147 0 384 0
[pid=27835] vsize: 2124
Raw data (/proc/27839/stat): 27839 (minisat+_64-bit) R 27835 27835 31027 0 -1 0 17200 0 0 0 55747 108 0 0 25 0 1 0 1855264841 71786496 16996 4294967295 134512640 135094434 3221224432 3221223088 134557925 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27839/statm): 17526 16996 145 145 0 17381 0
[pid=27839] vsize: 70104
Current children cumulated CPU time (s) 558.56
Current children cumulated vsize (Kb) 72228

[startup+570.053 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27839
Raw data (/proc/27835/stat): 27835 (minisat+_script) S 27834 27835 31027 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855264836 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27835/statm): 531 226 485 147 0 384 0
[pid=27835] vsize: 2124
Raw data (/proc/27839/stat): 27839 (minisat+_64-bit) R 27835 27835 31027 0 -1 0 17340 0 0 0 56743 110 0 0 25 0 1 0 1855264841 72347648 17136 4294967295 134512640 135094434 3221224432 3221223088 134557950 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27839/statm): 17663 17136 145 145 0 17518 0
[pid=27839] vsize: 70652
Current children cumulated CPU time (s) 568.54
Current children cumulated vsize (Kb) 72776

[startup+580.054 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27839
Raw data (/proc/27835/stat): 27835 (minisat+_script) S 27834 27835 31027 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855264836 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27835/statm): 531 226 485 147 0 384 0
[pid=27835] vsize: 2124
Raw data (/proc/27839/stat): 27839 (minisat+_64-bit) R 27835 27835 31027 0 -1 0 17502 0 0 0 57741 112 0 0 25 0 1 0 1855264841 73035776 17298 4294967295 134512640 135094434 3221224432 3221223088 134558235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27839/statm): 17831 17298 145 145 0 17686 0
[pid=27839] vsize: 71324
Current children cumulated CPU time (s) 578.54
Current children cumulated vsize (Kb) 73448

[startup+590.054 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27839
Raw data (/proc/27835/stat): 27835 (minisat+_script) S 27834 27835 31027 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855264836 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27835/statm): 531 226 485 147 0 384 0
[pid=27835] vsize: 2124
Raw data (/proc/27839/stat): 27839 (minisat+_64-bit) R 27835 27835 31027 0 -1 0 17618 0 0 0 58739 113 0 0 25 0 1 0 1855264841 73506816 17414 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27839/statm): 17946 17414 145 145 0 17801 0
[pid=27839] vsize: 71784
Current children cumulated CPU time (s) 588.53
Current children cumulated vsize (Kb) 73908

[startup+600.055 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27839
Raw data (/proc/27835/stat): 27835 (minisat+_script) S 27834 27835 31027 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855264836 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27835/statm): 531 226 485 147 0 384 0
[pid=27835] vsize: 2124
Raw data (/proc/27839/stat): 27839 (minisat+_64-bit) R 27835 27835 31027 0 -1 0 17777 0 0 0 59737 113 0 0 25 0 1 0 1855264841 74133504 17573 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27839/statm): 18099 17573 145 145 0 17954 0
[pid=27839] vsize: 72396
Current children cumulated CPU time (s) 598.51
Current children cumulated vsize (Kb) 74520

[startup+610.056 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27839
Raw data (/proc/27835/stat): 27835 (minisat+_script) S 27834 27835 31027 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855264836 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27835/statm): 531 226 485 147 0 384 0
[pid=27835] vsize: 2124
Raw data (/proc/27839/stat): 27839 (minisat+_64-bit) R 27835 27835 31027 0 -1 0 17885 0 0 0 60736 114 0 0 25 0 1 0 1855264841 74567680 17681 4294967295 134512640 135094434 3221224432 3221223088 134558011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27839/statm): 18205 17681 145 145 0 18060 0
[pid=27839] vsize: 72820
Current children cumulated CPU time (s) 608.51
Current children cumulated vsize (Kb) 74944

[startup+620.057 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27839
Raw data (/proc/27835/stat): 27835 (minisat+_script) S 27834 27835 31027 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855264836 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27835/statm): 531 226 485 147 0 384 0
[pid=27835] vsize: 2124
Raw data (/proc/27839/stat): 27839 (minisat+_64-bit) R 27835 27835 31027 0 -1 0 18031 0 0 0 61734 115 0 0 25 0 1 0 1855264841 75182080 17827 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27839/statm): 18355 17827 145 145 0 18210 0
[pid=27839] vsize: 73420
Current children cumulated CPU time (s) 618.5
Current children cumulated vsize (Kb) 75544

[startup+630.058 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27839
Raw data (/proc/27835/stat): 27835 (minisat+_script) S 27834 27835 31027 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855264836 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27835/statm): 531 226 485 147 0 384 0
[pid=27835] vsize: 2124
Raw data (/proc/27839/stat): 27839 (minisat+_64-bit) R 27835 27835 31027 0 -1 0 18207 0 0 0 62730 116 0 0 25 0 1 0 1855264841 75898880 18003 4294967295 134512640 135094434 3221224432 3221222896 134780778 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27839/statm): 18530 18003 145 145 0 18385 0
[pid=27839] vsize: 74120
Current children cumulated CPU time (s) 628.47
Current children cumulated vsize (Kb) 76244

[startup+640.058 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27839
Raw data (/proc/27835/stat): 27835 (minisat+_script) S 27834 27835 31027 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855264836 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27835/statm): 531 226 485 147 0 384 0
[pid=27835] vsize: 2124
Raw data (/proc/27839/stat): 27839 (minisat+_64-bit) R 27835 27835 31027 0 -1 0 18249 0 0 0 63730 116 0 0 25 0 1 0 1855264841 76066816 18045 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27839/statm): 18571 18045 145 145 0 18426 0
[pid=27839] vsize: 74284
Current children cumulated CPU time (s) 638.47
Current children cumulated vsize (Kb) 76408

[startup+650.059 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27839
Raw data (/proc/27835/stat): 27835 (minisat+_script) S 27834 27835 31027 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855264836 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27835/statm): 531 226 485 147 0 384 0
[pid=27835] vsize: 2124
Raw data (/proc/27839/stat): 27839 (minisat+_64-bit) R 27835 27835 31027 0 -1 0 18249 0 0 0 64730 116 0 0 25 0 1 0 1855264841 76066816 18045 4294967295 134512640 135094434 3221224432 3221223044 134563059 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27839/statm): 18571 18045 145 145 0 18426 0
[pid=27839] vsize: 74284
Current children cumulated CPU time (s) 648.47
Current children cumulated vsize (Kb) 76408

[startup+660.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27839
Raw data (/proc/27835/stat): 27835 (minisat+_script) S 27834 27835 31027 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855264836 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27835/statm): 531 226 485 147 0 384 0
[pid=27835] vsize: 2124
Raw data (/proc/27839/stat): 27839 (minisat+_64-bit) R 27835 27835 31027 0 -1 0 18249 0 0 0 65731 116 0 0 25 0 1 0 1855264841 76066816 18045 4294967295 134512640 135094434 3221224432 3221223044 134563071 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27839/statm): 18571 18045 145 145 0 18426 0
[pid=27839] vsize: 74284
Current children cumulated CPU time (s) 658.48
Current children cumulated vsize (Kb) 76408

[startup+670.061 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27839
Raw data (/proc/27835/stat): 27835 (minisat+_script) S 27834 27835 31027 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855264836 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27835/statm): 531 226 485 147 0 384 0
[pid=27835] vsize: 2124
Raw data (/proc/27839/stat): 27839 (minisat+_64-bit) R 27835 27835 31027 0 -1 0 18249 0 0 0 66731 116 0 0 25 0 1 0 1855264841 76066816 18045 4294967295 134512640 135094434 3221224432 3221223024 134556933 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27839/statm): 18571 18045 145 145 0 18426 0
[pid=27839] vsize: 74284
Current children cumulated CPU time (s) 668.48
Current children cumulated vsize (Kb) 76408

[startup+680.062 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27839
Raw data (/proc/27835/stat): 27835 (minisat+_script) S 27834 27835 31027 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855264836 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27835/statm): 531 226 485 147 0 384 0
[pid=27835] vsize: 2124
Raw data (/proc/27839/stat): 27839 (minisat+_64-bit) R 27835 27835 31027 0 -1 0 18249 0 0 0 67731 116 0 0 25 0 1 0 1855264841 76066816 18045 4294967295 134512640 135094434 3221224432 3221223104 134555574 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27839/statm): 18571 18045 145 145 0 18426 0
[pid=27839] vsize: 74284
Current children cumulated CPU time (s) 678.48
Current children cumulated vsize (Kb) 76408

[startup+690.063 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27839
Raw data (/proc/27835/stat): 27835 (minisat+_script) S 27834 27835 31027 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855264836 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27835/statm): 531 226 485 147 0 384 0
[pid=27835] vsize: 2124
Raw data (/proc/27839/stat): 27839 (minisat+_64-bit) R 27835 27835 31027 0 -1 0 18249 0 0 0 68731 116 0 0 25 0 1 0 1855264841 76066816 18045 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27839/statm): 18571 18045 145 145 0 18426 0
[pid=27839] vsize: 74284
Current children cumulated CPU time (s) 688.48
Current children cumulated vsize (Kb) 76408

[startup+700.064 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27839
Raw data (/proc/27835/stat): 27835 (minisat+_script) S 27834 27835 31027 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855264836 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27835/statm): 531 226 485 147 0 384 0
[pid=27835] vsize: 2124
Raw data (/proc/27839/stat): 27839 (minisat+_64-bit) R 27835 27835 31027 0 -1 0 18249 0 0 0 69731 117 0 0 25 0 1 0 1855264841 76066816 18045 4294967295 134512640 135094434 3221224432 3221223024 134557202 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27839/statm): 18571 18045 145 145 0 18426 0
[pid=27839] vsize: 74284
Current children cumulated CPU time (s) 698.49
Current children cumulated vsize (Kb) 76408

[startup+710.065 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27839
Raw data (/proc/27835/stat): 27835 (minisat+_script) S 27834 27835 31027 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855264836 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27835/statm): 531 226 485 147 0 384 0
[pid=27835] vsize: 2124
Raw data (/proc/27839/stat): 27839 (minisat+_64-bit) R 27835 27835 31027 0 -1 0 18250 0 0 0 70731 117 0 0 25 0 1 0 1855264841 76066816 18046 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27839/statm): 18571 18046 145 145 0 18426 0
[pid=27839] vsize: 74284
Current children cumulated CPU time (s) 708.49
Current children cumulated vsize (Kb) 76408

[startup+720.066 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27839
Raw data (/proc/27835/stat): 27835 (minisat+_script) S 27834 27835 31027 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855264836 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27835/statm): 531 226 485 147 0 384 0
[pid=27835] vsize: 2124
Raw data (/proc/27839/stat): 27839 (minisat+_64-bit) R 27835 27835 31027 0 -1 0 18250 0 0 0 71731 117 0 0 25 0 1 0 1855264841 76066816 18046 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27839/statm): 18571 18046 145 145 0 18426 0
[pid=27839] vsize: 74284
Current children cumulated CPU time (s) 718.49
Current children cumulated vsize (Kb) 76408

[startup+730.067 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27839
Raw data (/proc/27835/stat): 27835 (minisat+_script) S 27834 27835 31027 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855264836 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27835/statm): 531 226 485 147 0 384 0
[pid=27835] vsize: 2124
Raw data (/proc/27839/stat): 27839 (minisat+_64-bit) R 27835 27835 31027 0 -1 0 18250 0 0 0 72731 117 0 0 25 0 1 0 1855264841 76066816 18046 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27839/statm): 18571 18046 145 145 0 18426 0
[pid=27839] vsize: 74284
Current children cumulated CPU time (s) 728.49
Current children cumulated vsize (Kb) 76408

[startup+740.068 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27839
Raw data (/proc/27835/stat): 27835 (minisat+_script) S 27834 27835 31027 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855264836 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27835/statm): 531 226 485 147 0 384 0
[pid=27835] vsize: 2124
Raw data (/proc/27839/stat): 27839 (minisat+_64-bit) R 27835 27835 31027 0 -1 0 18250 0 0 0 73732 117 0 0 25 0 1 0 1855264841 76066816 18046 4294967295 134512640 135094434 3221224432 3221223092 134553528 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27839/statm): 18571 18046 145 145 0 18426 0
[pid=27839] vsize: 74284
Current children cumulated CPU time (s) 738.5
Current children cumulated vsize (Kb) 76408

[startup+750.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27839
Raw data (/proc/27835/stat): 27835 (minisat+_script) S 27834 27835 31027 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855264836 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27835/statm): 531 226 485 147 0 384 0
[pid=27835] vsize: 2124
Raw data (/proc/27839/stat): 27839 (minisat+_64-bit) R 27835 27835 31027 0 -1 0 18250 0 0 0 74732 117 0 0 25 0 1 0 1855264841 76066816 18046 4294967295 134512640 135094434 3221224432 3221223024 134551908 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27839/statm): 18571 18046 145 145 0 18426 0
[pid=27839] vsize: 74284
Current children cumulated CPU time (s) 748.5
Current children cumulated vsize (Kb) 76408

[startup+760.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27839
Raw data (/proc/27835/stat): 27835 (minisat+_script) S 27834 27835 31027 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855264836 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27835/statm): 531 226 485 147 0 384 0
[pid=27835] vsize: 2124
Raw data (/proc/27839/stat): 27839 (minisat+_64-bit) R 27835 27835 31027 0 -1 0 18252 0 0 0 75732 117 0 0 25 0 1 0 1855264841 76066816 18048 4294967295 134512640 135094434 3221224432 3221223068 134557639 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27839/statm): 18571 18048 145 145 0 18426 0
[pid=27839] vsize: 74284
Current children cumulated CPU time (s) 758.5
Current children cumulated vsize (Kb) 76408

[startup+770.072 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27839
Raw data (/proc/27835/stat): 27835 (minisat+_script) S 27834 27835 31027 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855264836 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27835/statm): 531 226 485 147 0 384 0
[pid=27835] vsize: 2124
Raw data (/proc/27839/stat): 27839 (minisat+_64-bit) R 27835 27835 31027 0 -1 0 18252 0 0 0 76732 117 0 0 25 0 1 0 1855264841 76066816 18048 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27839/statm): 18571 18048 145 145 0 18426 0
[pid=27839] vsize: 74284
Current children cumulated CPU time (s) 768.5
Current children cumulated vsize (Kb) 76408

[startup+780.072 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27839
Raw data (/proc/27835/stat): 27835 (minisat+_script) S 27834 27835 31027 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855264836 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27835/statm): 531 226 485 147 0 384 0
[pid=27835] vsize: 2124
Raw data (/proc/27839/stat): 27839 (minisat+_64-bit) R 27835 27835 31027 0 -1 0 18252 0 0 0 77732 117 0 0 25 0 1 0 1855264841 76066816 18048 4294967295 134512640 135094434 3221224432 3221223088 134557866 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27839/statm): 18571 18048 145 145 0 18426 0
[pid=27839] vsize: 74284
Current children cumulated CPU time (s) 778.5
Current children cumulated vsize (Kb) 76408

[startup+790.072 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27839
Raw data (/proc/27835/stat): 27835 (minisat+_script) S 27834 27835 31027 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855264836 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27835/statm): 531 226 485 147 0 384 0
[pid=27835] vsize: 2124
Raw data (/proc/27839/stat): 27839 (minisat+_64-bit) R 27835 27835 31027 0 -1 0 18252 0 0 0 78733 117 0 0 25 0 1 0 1855264841 76066816 18048 4294967295 134512640 135094434 3221224432 3221223088 134557866 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27839/statm): 18571 18048 145 145 0 18426 0
[pid=27839] vsize: 74284
Current children cumulated CPU time (s) 788.51
Current children cumulated vsize (Kb) 76408

[startup+800.074 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27839
Raw data (/proc/27835/stat): 27835 (minisat+_script) S 27834 27835 31027 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855264836 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27835/statm): 531 226 485 147 0 384 0
[pid=27835] vsize: 2124
Raw data (/proc/27839/stat): 27839 (minisat+_64-bit) R 27835 27835 31027 0 -1 0 18252 0 0 0 79733 117 0 0 25 0 1 0 1855264841 76066816 18048 4294967295 134512640 135094434 3221224432 3221223104 134556317 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27839/statm): 18571 18048 145 145 0 18426 0
[pid=27839] vsize: 74284
Current children cumulated CPU time (s) 798.51
Current children cumulated vsize (Kb) 76408

[startup+810.075 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27839
Raw data (/proc/27835/stat): 27835 (minisat+_script) S 27834 27835 31027 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855264836 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27835/statm): 531 226 485 147 0 384 0
[pid=27835] vsize: 2124
Raw data (/proc/27839/stat): 27839 (minisat+_64-bit) R 27835 27835 31027 0 -1 0 18252 0 0 0 80733 117 0 0 25 0 1 0 1855264841 76066816 18048 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27839/statm): 18571 18048 145 145 0 18426 0
[pid=27839] vsize: 74284
Current children cumulated CPU time (s) 808.51
Current children cumulated vsize (Kb) 76408

[startup+820.077 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27839
Raw data (/proc/27835/stat): 27835 (minisat+_script) S 27834 27835 31027 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855264836 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27835/statm): 531 226 485 147 0 384 0
[pid=27835] vsize: 2124
Raw data (/proc/27839/stat): 27839 (minisat+_64-bit) R 27835 27835 31027 0 -1 0 18254 0 0 0 81734 117 0 0 25 0 1 0 1855264841 76066816 18050 4294967295 134512640 135094434 3221224432 3221223088 134557937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27839/statm): 18571 18050 145 145 0 18426 0
[pid=27839] vsize: 74284
Current children cumulated CPU time (s) 818.52
Current children cumulated vsize (Kb) 76408

[startup+830.078 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27839
Raw data (/proc/27835/stat): 27835 (minisat+_script) S 27834 27835 31027 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855264836 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27835/statm): 531 226 485 147 0 384 0
[pid=27835] vsize: 2124
Raw data (/proc/27839/stat): 27839 (minisat+_64-bit) R 27835 27835 31027 0 -1 0 18255 0 0 0 82734 117 0 0 25 0 1 0 1855264841 76066816 18051 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27839/statm): 18571 18051 145 145 0 18426 0
[pid=27839] vsize: 74284
Current children cumulated CPU time (s) 828.52
Current children cumulated vsize (Kb) 76408

[startup+840.079 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27839
Raw data (/proc/27835/stat): 27835 (minisat+_script) S 27834 27835 31027 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855264836 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27835/statm): 531 226 485 147 0 384 0
[pid=27835] vsize: 2124
Raw data (/proc/27839/stat): 27839 (minisat+_64-bit) R 27835 27835 31027 0 -1 0 18265 0 0 0 83734 117 0 0 25 0 1 0 1855264841 76132352 18061 4294967295 134512640 135094434 3221224432 3221223088 134557896 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27839/statm): 18587 18061 145 145 0 18442 0
[pid=27839] vsize: 74348
Current children cumulated CPU time (s) 838.52
Current children cumulated vsize (Kb) 76472

[startup+850.081 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27839
Raw data (/proc/27835/stat): 27835 (minisat+_script) S 27834 27835 31027 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855264836 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27835/statm): 531 226 485 147 0 384 0
[pid=27835] vsize: 2124
Raw data (/proc/27839/stat): 27839 (minisat+_64-bit) R 27835 27835 31027 0 -1 0 18278 0 0 0 84734 117 0 0 25 0 1 0 1855264841 76197888 18074 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27839/statm): 18603 18074 145 145 0 18458 0
[pid=27839] vsize: 74412
Current children cumulated CPU time (s) 848.52
Current children cumulated vsize (Kb) 76536

[startup+860.082 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27839
Raw data (/proc/27835/stat): 27835 (minisat+_script) S 27834 27835 31027 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855264836 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27835/statm): 531 226 485 147 0 384 0
[pid=27835] vsize: 2124
Raw data (/proc/27839/stat): 27839 (minisat+_64-bit) R 27835 27835 31027 0 -1 0 18279 0 0 0 85734 117 0 0 25 0 1 0 1855264841 76197888 18075 4294967295 134512640 135094434 3221224432 3221223088 134557872 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27839/statm): 18603 18075 145 145 0 18458 0
[pid=27839] vsize: 74412
Current children cumulated CPU time (s) 858.52
Current children cumulated vsize (Kb) 76536

[startup+870.083 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27839
Raw data (/proc/27835/stat): 27835 (minisat+_script) S 27834 27835 31027 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855264836 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27835/statm): 531 226 485 147 0 384 0
[pid=27835] vsize: 2124
Raw data (/proc/27839/stat): 27839 (minisat+_64-bit) R 27835 27835 31027 0 -1 0 18280 0 0 0 86734 117 0 0 25 0 1 0 1855264841 76197888 18076 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27839/statm): 18603 18076 145 145 0 18458 0
[pid=27839] vsize: 74412
Current children cumulated CPU time (s) 868.52
Current children cumulated vsize (Kb) 76536

[startup+880.084 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27839
Raw data (/proc/27835/stat): 27835 (minisat+_script) S 27834 27835 31027 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855264836 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27835/statm): 531 226 485 147 0 384 0
[pid=27835] vsize: 2124
Raw data (/proc/27839/stat): 27839 (minisat+_64-bit) R 27835 27835 31027 0 -1 0 18290 0 0 0 87735 117 0 0 25 0 1 0 1855264841 76263424 18086 4294967295 134512640 135094434 3221224432 3221223024 134557202 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27839/statm): 18619 18086 145 145 0 18474 0
[pid=27839] vsize: 74476
Current children cumulated CPU time (s) 878.53
Current children cumulated vsize (Kb) 76600

[startup+890.085 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27839
Raw data (/proc/27835/stat): 27835 (minisat+_script) S 27834 27835 31027 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855264836 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27835/statm): 531 226 485 147 0 384 0
[pid=27835] vsize: 2124
Raw data (/proc/27839/stat): 27839 (minisat+_64-bit) R 27835 27835 31027 0 -1 0 18290 0 0 0 88735 117 0 0 25 0 1 0 1855264841 76263424 18086 4294967295 134512640 135094434 3221224432 3221223056 134562051 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27839/statm): 18619 18086 145 145 0 18474 0
[pid=27839] vsize: 74476
Current children cumulated CPU time (s) 888.53
Current children cumulated vsize (Kb) 76600

[startup+900.086 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27839
Raw data (/proc/27835/stat): 27835 (minisat+_script) S 27834 27835 31027 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855264836 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27835/statm): 531 226 485 147 0 384 0
[pid=27835] vsize: 2124
Raw data (/proc/27839/stat): 27839 (minisat+_64-bit) R 27835 27835 31027 0 -1 0 18290 0 0 0 89735 117 0 0 25 0 1 0 1855264841 76263424 18086 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27839/statm): 18619 18086 145 145 0 18474 0
[pid=27839] vsize: 74476
Current children cumulated CPU time (s) 898.53
Current children cumulated vsize (Kb) 76600

[startup+910.087 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27839
Raw data (/proc/27835/stat): 27835 (minisat+_script) S 27834 27835 31027 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855264836 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27835/statm): 531 226 485 147 0 384 0
[pid=27835] vsize: 2124
Raw data (/proc/27839/stat): 27839 (minisat+_64-bit) R 27835 27835 31027 0 -1 0 18290 0 0 0 90735 117 0 0 25 0 1 0 1855264841 76263424 18086 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27839/statm): 18619 18086 145 145 0 18474 0
[pid=27839] vsize: 74476
Current children cumulated CPU time (s) 908.53
Current children cumulated vsize (Kb) 76600

[startup+920.088 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27839
Raw data (/proc/27835/stat): 27835 (minisat+_script) S 27834 27835 31027 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855264836 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27835/statm): 531 226 485 147 0 384 0
[pid=27835] vsize: 2124
Raw data (/proc/27839/stat): 27839 (minisat+_64-bit) R 27835 27835 31027 0 -1 0 18290 0 0 0 91736 117 0 0 25 0 1 0 1855264841 76263424 18086 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27839/statm): 18619 18086 145 145 0 18474 0
[pid=27839] vsize: 74476
Current children cumulated CPU time (s) 918.54
Current children cumulated vsize (Kb) 76600

[startup+930.089 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27839
Raw data (/proc/27835/stat): 27835 (minisat+_script) S 27834 27835 31027 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855264836 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27835/statm): 531 226 485 147 0 384 0
[pid=27835] vsize: 2124
Raw data (/proc/27839/stat): 27839 (minisat+_64-bit) R 27835 27835 31027 0 -1 0 18291 0 0 0 92736 117 0 0 25 0 1 0 1855264841 76263424 18087 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27839/statm): 18619 18087 145 145 0 18474 0
[pid=27839] vsize: 74476
Current children cumulated CPU time (s) 928.54
Current children cumulated vsize (Kb) 76600

[startup+940.089 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27839
Raw data (/proc/27835/stat): 27835 (minisat+_script) S 27834 27835 31027 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855264836 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27835/statm): 531 226 485 147 0 384 0
[pid=27835] vsize: 2124
Raw data (/proc/27839/stat): 27839 (minisat+_64-bit) R 27835 27835 31027 0 -1 0 18292 0 0 0 93736 117 0 0 25 0 1 0 1855264841 76263424 18088 4294967295 134512640 135094434 3221224432 3221223104 134555599 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27839/statm): 18619 18088 145 145 0 18474 0
[pid=27839] vsize: 74476
Current children cumulated CPU time (s) 938.54
Current children cumulated vsize (Kb) 76600

[startup+950.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27839
Raw data (/proc/27835/stat): 27835 (minisat+_script) S 27834 27835 31027 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855264836 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27835/statm): 531 226 485 147 0 384 0
[pid=27835] vsize: 2124
Raw data (/proc/27839/stat): 27839 (minisat+_64-bit) R 27835 27835 31027 0 -1 0 18293 0 0 0 94736 117 0 0 25 0 1 0 1855264841 76263424 18089 4294967295 134512640 135094434 3221224432 3221223044 134563043 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27839/statm): 18619 18089 145 145 0 18474 0
[pid=27839] vsize: 74476
Current children cumulated CPU time (s) 948.54
Current children cumulated vsize (Kb) 76600

[startup+960.091 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27839
Raw data (/proc/27835/stat): 27835 (minisat+_script) S 27834 27835 31027 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855264836 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27835/statm): 531 226 485 147 0 384 0
[pid=27835] vsize: 2124
Raw data (/proc/27839/stat): 27839 (minisat+_64-bit) R 27835 27835 31027 0 -1 0 18293 0 0 0 95737 117 0 0 25 0 1 0 1855264841 76263424 18089 4294967295 134512640 135094434 3221224432 3221223104 134555869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27839/statm): 18619 18089 145 145 0 18474 0
[pid=27839] vsize: 74476
Current children cumulated CPU time (s) 958.55
Current children cumulated vsize (Kb) 76600

[startup+970.092 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27839
Raw data (/proc/27835/stat): 27835 (minisat+_script) S 27834 27835 31027 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855264836 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27835/statm): 531 226 485 147 0 384 0
[pid=27835] vsize: 2124
Raw data (/proc/27839/stat): 27839 (minisat+_64-bit) R 27835 27835 31027 0 -1 0 18293 0 0 0 96737 117 0 0 25 0 1 0 1855264841 76263424 18089 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27839/statm): 18619 18089 145 145 0 18474 0
[pid=27839] vsize: 74476
Current children cumulated CPU time (s) 968.55
Current children cumulated vsize (Kb) 76600

[startup+980.093 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27839
Raw data (/proc/27835/stat): 27835 (minisat+_script) S 27834 27835 31027 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855264836 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27835/statm): 531 226 485 147 0 384 0
[pid=27835] vsize: 2124
Raw data (/proc/27839/stat): 27839 (minisat+_64-bit) R 27835 27835 31027 0 -1 0 18293 0 0 0 97737 117 0 0 25 0 1 0 1855264841 76263424 18089 4294967295 134512640 135094434 3221224432 3221223024 134556809 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27839/statm): 18619 18089 145 145 0 18474 0
[pid=27839] vsize: 74476
Current children cumulated CPU time (s) 978.55
Current children cumulated vsize (Kb) 76600

[startup+990.094 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27839
Raw data (/proc/27835/stat): 27835 (minisat+_script) S 27834 27835 31027 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855264836 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27835/statm): 531 226 485 147 0 384 0
[pid=27835] vsize: 2124
Raw data (/proc/27839/stat): 27839 (minisat+_64-bit) R 27835 27835 31027 0 -1 0 18293 0 0 0 98737 117 0 0 25 0 1 0 1855264841 76263424 18089 4294967295 134512640 135094434 3221224432 3221223088 134557840 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27839/statm): 18619 18089 145 145 0 18474 0
[pid=27839] vsize: 74476
Current children cumulated CPU time (s) 988.55
Current children cumulated vsize (Kb) 76600

[startup+1000.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27839
Raw data (/proc/27835/stat): 27835 (minisat+_script) S 27834 27835 31027 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855264836 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27835/statm): 531 226 485 147 0 384 0
[pid=27835] vsize: 2124
Raw data (/proc/27839/stat): 27839 (minisat+_64-bit) R 27835 27835 31027 0 -1 0 18293 0 0 0 99737 117 0 0 25 0 1 0 1855264841 76263424 18089 4294967295 134512640 135094434 3221224432 3221223088 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27839/statm): 18619 18089 145 145 0 18474 0
[pid=27839] 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 27839
Raw data (/proc/27835/stat): 27835 (minisat+_script) S 27834 27835 31027 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855264836 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27835/statm): 531 226 485 147 0 384 0
[pid=27835] vsize: 2124
Raw data (/proc/27839/stat): 27839 (minisat+_64-bit) R 27835 27835 31027 0 -1 0 18293 0 0 0 100738 117 0 0 25 0 1 0 1855264841 76263424 18089 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27839/statm): 18619 18089 145 145 0 18474 0
[pid=27839] vsize: 74476
Current children cumulated CPU time (s) 1008.56
Current children cumulated vsize (Kb) 76600

[startup+1020.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27839
Raw data (/proc/27835/stat): 27835 (minisat+_script) S 27834 27835 31027 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855264836 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27835/statm): 531 226 485 147 0 384 0
[pid=27835] vsize: 2124
Raw data (/proc/27839/stat): 27839 (minisat+_64-bit) R 27835 27835 31027 0 -1 0 18293 0 0 0 101738 117 0 0 25 0 1 0 1855264841 76263424 18089 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27839/statm): 18619 18089 145 145 0 18474 0
[pid=27839] vsize: 74476
Current children cumulated CPU time (s) 1018.56
Current children cumulated vsize (Kb) 76600

[startup+1030.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27839
Raw data (/proc/27835/stat): 27835 (minisat+_script) S 27834 27835 31027 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855264836 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27835/statm): 531 226 485 147 0 384 0
[pid=27835] vsize: 2124
Raw data (/proc/27839/stat): 27839 (minisat+_64-bit) R 27835 27835 31027 0 -1 0 18293 0 0 0 102738 117 0 0 25 0 1 0 1855264841 76263424 18089 4294967295 134512640 135094434 3221224432 3221223092 134553487 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27839/statm): 18619 18089 145 145 0 18474 0
[pid=27839] vsize: 74476
Current children cumulated CPU time (s) 1028.56
Current children cumulated vsize (Kb) 76600

[startup+1040.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27839
Raw data (/proc/27835/stat): 27835 (minisat+_script) S 27834 27835 31027 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855264836 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27835/statm): 531 226 485 147 0 384 0
[pid=27835] vsize: 2124
Raw data (/proc/27839/stat): 27839 (minisat+_64-bit) R 27835 27835 31027 0 -1 0 18293 0 0 0 103739 117 0 0 25 0 1 0 1855264841 76263424 18089 4294967295 134512640 135094434 3221224432 3221223088 134557928 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27839/statm): 18619 18089 145 145 0 18474 0
[pid=27839] vsize: 74476
Current children cumulated CPU time (s) 1038.57
Current children cumulated vsize (Kb) 76600

[startup+1050.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27839
Raw data (/proc/27835/stat): 27835 (minisat+_script) S 27834 27835 31027 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855264836 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27835/statm): 531 226 485 147 0 384 0
[pid=27835] vsize: 2124
Raw data (/proc/27839/stat): 27839 (minisat+_64-bit) R 27835 27835 31027 0 -1 0 18309 0 0 0 104737 118 0 0 25 0 1 0 1855264841 76328960 18105 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27839/statm): 18635 18105 145 145 0 18490 0
[pid=27839] vsize: 74540
Current children cumulated CPU time (s) 1048.56
Current children cumulated vsize (Kb) 76664

[startup+1060.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27839
Raw data (/proc/27835/stat): 27835 (minisat+_script) S 27834 27835 31027 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855264836 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27835/statm): 531 226 485 147 0 384 0
[pid=27835] vsize: 2124
Raw data (/proc/27839/stat): 27839 (minisat+_64-bit) R 27835 27835 31027 0 -1 0 18316 0 0 0 105737 118 0 0 25 0 1 0 1855264841 76328960 18112 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27839/statm): 18635 18112 145 145 0 18490 0
[pid=27839] vsize: 74540
Current children cumulated CPU time (s) 1058.56
Current children cumulated vsize (Kb) 76664

[startup+1070.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27839
Raw data (/proc/27835/stat): 27835 (minisat+_script) S 27834 27835 31027 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855264836 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27835/statm): 531 226 485 147 0 384 0
[pid=27835] vsize: 2124
Raw data (/proc/27839/stat): 27839 (minisat+_64-bit) R 27835 27835 31027 0 -1 0 18316 0 0 0 106738 118 0 0 25 0 1 0 1855264841 76328960 18112 4294967295 134512640 135094434 3221224432 3221223088 134558402 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27839/statm): 18635 18112 145 145 0 18490 0
[pid=27839] vsize: 74540
Current children cumulated CPU time (s) 1068.57
Current children cumulated vsize (Kb) 76664

[startup+1080.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27839
Raw data (/proc/27835/stat): 27835 (minisat+_script) S 27834 27835 31027 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855264836 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27835/statm): 531 226 485 147 0 384 0
[pid=27835] vsize: 2124
Raw data (/proc/27839/stat): 27839 (minisat+_64-bit) R 27835 27835 31027 0 -1 0 18316 0 0 0 107738 118 0 0 25 0 1 0 1855264841 76328960 18112 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27839/statm): 18635 18112 145 145 0 18490 0
[pid=27839] vsize: 74540
Current children cumulated CPU time (s) 1078.57
Current children cumulated vsize (Kb) 76664

[startup+1090.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27839
Raw data (/proc/27835/stat): 27835 (minisat+_script) S 27834 27835 31027 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855264836 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27835/statm): 531 226 485 147 0 384 0
[pid=27835] vsize: 2124
Raw data (/proc/27839/stat): 27839 (minisat+_64-bit) R 27835 27835 31027 0 -1 0 18329 0 0 0 108738 118 0 0 25 0 1 0 1855264841 76394496 18125 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27839/statm): 18651 18125 145 145 0 18506 0
[pid=27839] vsize: 74604
Current children cumulated CPU time (s) 1088.57
Current children cumulated vsize (Kb) 76728

[startup+1100.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27839
Raw data (/proc/27835/stat): 27835 (minisat+_script) S 27834 27835 31027 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855264836 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27835/statm): 531 226 485 147 0 384 0
[pid=27835] vsize: 2124
Raw data (/proc/27839/stat): 27839 (minisat+_64-bit) R 27835 27835 31027 0 -1 0 18331 0 0 0 109738 118 0 0 25 0 1 0 1855264841 76394496 18127 4294967295 134512640 135094434 3221224432 3221223092 134553491 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27839/statm): 18651 18127 145 145 0 18506 0
[pid=27839] vsize: 74604
Current children cumulated CPU time (s) 1098.57
Current children cumulated vsize (Kb) 76728

[startup+1110.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27839
Raw data (/proc/27835/stat): 27835 (minisat+_script) S 27834 27835 31027 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855264836 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27835/statm): 531 226 485 147 0 384 0
[pid=27835] vsize: 2124
Raw data (/proc/27839/stat): 27839 (minisat+_64-bit) R 27835 27835 31027 0 -1 0 18331 0 0 0 110738 118 0 0 25 0 1 0 1855264841 76394496 18127 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27839/statm): 18651 18127 145 145 0 18506 0
[pid=27839] vsize: 74604
Current children cumulated CPU time (s) 1108.57
Current children cumulated vsize (Kb) 76728

[startup+1120.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27839
Raw data (/proc/27835/stat): 27835 (minisat+_script) S 27834 27835 31027 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855264836 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27835/statm): 531 226 485 147 0 384 0
[pid=27835] vsize: 2124
Raw data (/proc/27839/stat): 27839 (minisat+_64-bit) R 27835 27835 31027 0 -1 0 18331 0 0 0 111739 118 0 0 25 0 1 0 1855264841 76394496 18127 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27839/statm): 18651 18127 145 145 0 18506 0
[pid=27839] vsize: 74604
Current children cumulated CPU time (s) 1118.58
Current children cumulated vsize (Kb) 76728

[startup+1130.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27839
Raw data (/proc/27835/stat): 27835 (minisat+_script) S 27834 27835 31027 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855264836 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27835/statm): 531 226 485 147 0 384 0
[pid=27835] vsize: 2124
Raw data (/proc/27839/stat): 27839 (minisat+_64-bit) R 27835 27835 31027 0 -1 0 18331 0 0 0 112739 118 0 0 25 0 1 0 1855264841 76394496 18127 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27839/statm): 18651 18127 145 145 0 18506 0
[pid=27839] vsize: 74604
Current children cumulated CPU time (s) 1128.58
Current children cumulated vsize (Kb) 76728

[startup+1140.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27839
Raw data (/proc/27835/stat): 27835 (minisat+_script) S 27834 27835 31027 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855264836 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27835/statm): 531 226 485 147 0 384 0
[pid=27835] vsize: 2124
Raw data (/proc/27839/stat): 27839 (minisat+_64-bit) R 27835 27835 31027 0 -1 0 18331 0 0 0 113739 118 0 0 25 0 1 0 1855264841 76394496 18127 4294967295 134512640 135094434 3221224432 3221223044 134563089 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27839/statm): 18651 18127 145 145 0 18506 0
[pid=27839] vsize: 74604
Current children cumulated CPU time (s) 1138.58
Current children cumulated vsize (Kb) 76728

[startup+1150.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27839
Raw data (/proc/27835/stat): 27835 (minisat+_script) S 27834 27835 31027 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855264836 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27835/statm): 531 226 485 147 0 384 0
[pid=27835] vsize: 2124
Raw data (/proc/27839/stat): 27839 (minisat+_64-bit) R 27835 27835 31027 0 -1 0 18331 0 0 0 114739 119 0 0 25 0 1 0 1855264841 76394496 18127 4294967295 134512640 135094434 3221224432 3221223088 134558019 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27839/statm): 18651 18127 145 145 0 18506 0
[pid=27839] vsize: 74604
Current children cumulated CPU time (s) 1148.59
Current children cumulated vsize (Kb) 76728

[startup+1160.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27839
Raw data (/proc/27835/stat): 27835 (minisat+_script) S 27834 27835 31027 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855264836 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27835/statm): 531 226 485 147 0 384 0
[pid=27835] vsize: 2124
Raw data (/proc/27839/stat): 27839 (minisat+_64-bit) R 27835 27835 31027 0 -1 0 18332 0 0 0 115739 119 0 0 25 0 1 0 1855264841 76394496 18128 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27839/statm): 18651 18128 145 145 0 18506 0
[pid=27839] vsize: 74604
Current children cumulated CPU time (s) 1158.59
Current children cumulated vsize (Kb) 76728

[startup+1170.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27839
Raw data (/proc/27835/stat): 27835 (minisat+_script) S 27834 27835 31027 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855264836 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27835/statm): 531 226 485 147 0 384 0
[pid=27835] vsize: 2124
Raw data (/proc/27839/stat): 27839 (minisat+_64-bit) R 27835 27835 31027 0 -1 0 18335 0 0 0 116740 119 0 0 25 0 1 0 1855264841 76394496 18131 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27839/statm): 18651 18131 145 145 0 18506 0
[pid=27839] vsize: 74604
Current children cumulated CPU time (s) 1168.6
Current children cumulated vsize (Kb) 76728

[startup+1180.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27839
Raw data (/proc/27835/stat): 27835 (minisat+_script) S 27834 27835 31027 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855264836 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27835/statm): 531 226 485 147 0 384 0
[pid=27835] vsize: 2124
Raw data (/proc/27839/stat): 27839 (minisat+_64-bit) R 27835 27835 31027 0 -1 0 18337 0 0 0 117740 119 0 0 25 0 1 0 1855264841 76394496 18133 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27839/statm): 18651 18133 145 145 0 18506 0
[pid=27839] vsize: 74604
Current children cumulated CPU time (s) 1178.6
Current children cumulated vsize (Kb) 76728

[startup+1190.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27839
Raw data (/proc/27835/stat): 27835 (minisat+_script) S 27834 27835 31027 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855264836 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27835/statm): 531 226 485 147 0 384 0
[pid=27835] vsize: 2124
Raw data (/proc/27839/stat): 27839 (minisat+_64-bit) R 27835 27835 31027 0 -1 0 18341 0 0 0 118740 119 0 0 25 0 1 0 1855264841 76394496 18137 4294967295 134512640 135094434 3221224432 3221223024 134556993 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27839/statm): 18651 18137 145 145 0 18506 0
[pid=27839] vsize: 74604
Current children cumulated CPU time (s) 1188.6
Current children cumulated vsize (Kb) 76728

[startup+1200.12 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27839
Raw data (/proc/27835/stat): 27835 (minisat+_script) S 27834 27835 31027 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855264836 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27835/statm): 531 226 485 147 0 384 0
[pid=27835] vsize: 2124
Raw data (/proc/27839/stat): 27839 (minisat+_64-bit) R 27835 27835 31027 0 -1 0 18343 0 0 0 119740 119 0 0 25 0 1 0 1855264841 76394496 18139 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27839/statm): 18651 18139 145 145 0 18506 0
[pid=27839] vsize: 74604
Current children cumulated CPU time (s) 1198.6
Current children cumulated vsize (Kb) 76728

[startup+1210.12 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27839
Raw data (/proc/27835/stat): 27835 (minisat+_script) S 27834 27835 31027 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855264836 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27835/statm): 531 226 485 147 0 384 0
[pid=27835] vsize: 2124
Raw data (/proc/27839/stat): 27839 (minisat+_64-bit) R 27835 27835 31027 0 -1 0 18371 0 0 0 120740 119 0 0 25 0 1 0 1855264841 77549568 18167 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27839/statm): 18933 18167 145 145 0 18788 0
[pid=27839] vsize: 75732
Current children cumulated CPU time (s) 1208.6
Current children cumulated vsize (Kb) 77856



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.12 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27839
Raw data (/proc/27835/stat): 27835 (minisat+_script) S 27834 27835 31027 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855264836 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27835/statm): 531 226 485 147 0 384 0
[pid=27835] vsize: 2124
Raw data (/proc/27839/stat): 27839 (minisat+_64-bit) R 27835 27835 31027 0 -1 0 18371 0 0 0 120740 119 0 0 25 0 1 0 1855264841 77549568 18167 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27839/statm): 18933 18167 145 145 0 18788 0
[pid=27839] vsize: 75732
Current children cumulated CPU time (s) 1208.6
Current children cumulated vsize (Kb) 77856

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

Child status: 0
Real time (s): 1210.16
CPU time (s): 1208.64
CPU user time (s): 1207.41
CPU system time (s): 1.22681
CPU usage (%): 99.8743
Max. virtual memory (cumulated for all children) (Kb): 77856

Verifier Data

ERROR: no interpretation found !