Some explanations

A solver is run under the control of another program named runsolver. runsolver is in charge of imposing the CPU time limit and the memory limit to the solver. It also monitors some information about the process. The trace of the execution of a solver is divided in four parts:
  1. LAUNCHER DATA
    These informations are related to the script which will launch the solver. The most important informations are the command line given to the solver, the md5sum of the different files and the dump of the /proc/cpuinfo and /proc/meminfo which provide some useful information on the computer.
  2. SOLVER DATA
    This is the output of the solver (stdout and stderr).
    Note that some very long lines in this section may be truncated by your web browser !
  3. WATCHER DATA
    This is the informations gathered by the runsolver program. It first prints the different limits. There's a first limit on CPU time set to 1200 seconds. After this time has ellapsed, runsolver sends a SIGTERM and 2 seconds later a SIGKILL to the solver. For safety, there's also another limit set to 1230 seconds which will send a SIGXPU to the solver. The last limit is on the virtual memory used by the process (900Mb).
    Every ten seconds, the runsolver process fetches the content of /proc/loadavg, /proc/pid/stat and /proc/pid/statm (see man proc) and prints it as raw data. This is only recorded in case we need to investigate the behaviour of a solver. The memory used by the solver (vsize) is also given every ten seconds.
    When the solver exits, runsolver prints some informations such as status and time. CPU usage is the ratio CPU Time/Real Time.
  4. VERIFIER DATA
    The output of the solver is piped to a verifier program which will search a value line "v " and, if found, will check that the given interpretation satisfies all constraints.

General information on the benchmark

Namemps-v2-20-10/MIPLIB/miplib/normalized-mps-v2-20-10-vpm1.opb
MD5SUM9d68724ddc6098af63bcc619f21688cc
Bench Categoryoptimization, medium integers (OPTMEDINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function 28
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 819200
Number of bits of the biggest number in a constraint 20
Biggest sum of numbers in a constraint 4941871
Number of bits of the biggest sum of numbers23
Best result obtained on this benchmarkSAT
Best CPU time to get the best result obtained on this benchmark1249.78
Number of variables2754
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 constraint82

Trace number 3889

Launcher Data

LAUNCH ON wulflinc17 THE 2005-09-19 03:26:28 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=2892 boxname=wulflinc17 idbench=548 idsolver=3 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  9d68724ddc6098af63bcc619f21688cc  /oldhome/oroussel/tmp/wulflinc17/normalized-mps-v2-20-10-vpm1.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc17/normalized-mps-v2-20-10-vpm1.opb
IDLAUNCH: 2892
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.072
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.072
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:        913360 kB
Buffers:         34776 kB
Cached:          59364 kB
SwapCached:        516 kB
Active:          56748 kB
Inactive:        39840 kB
HighTotal:      131008 kB
HighFree:        67592 kB
LowTotal:       903652 kB
LowFree:        845768 kB
SwapTotal:     2097892 kB
SwapFree:      2096672 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5680 kB
Slab:            18968 kB
Committed_AS:    64184 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-09-19 03:46:39 (client local time) WITH STATUS 0 IN 1208.91 SECONDS
stats: 2892 7 1208.91 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:   10
c ---[ 484]---> BDD-cost:   10
c ---[ 483]---> BDD-cost:   10
c ---[ 482]---> BDD-cost:   10
c ---[ 481]---> BDD-cost:   10
c ---[ 480]---> BDD-cost:   10
c ---[ 479]---> BDD-cost:   10
c ---[ 478]---> BDD-cost:   10
c ---[ 477]---> BDD-cost:   10
c ---[ 474]---> BDD-cost:   10
c ---[ 473]---> BDD-cost:   10
c ---[ 472]---> BDD-cost:   10
c ---[ 471]---> BDD-cost:   10
c ---[ 468]---> BDD-cost:   10
c ---[ 467]---> BDD-cost:   10
c ---[ 466]---> BDD-cost:   10
c ---[ 465]---> BDD-cost:   10
c ---[ 462]---> BDD-cost:   10
c ---[ 459]---> BDD-cost:   10
c ---[ 458]---> BDD-cost:   10
c ---[ 457]---> BDD-cost:   10
c ---[ 454]---> BDD-cost:   10
c ---[ 453]---> BDD-cost:   10
c ---[ 452]---> BDD-cost:   10
c ---[ 451]---> BDD-cost:   10
c ---[ 450]---> BDD-cost:   10
c ---[ 448]---> BDD-cost:   10
c ---[ 447]---> BDD-cost:   10
c ---[ 446]---> BDD-cost:   10
c ---[ 445]---> BDD-cost:   10
c ---[ 444]---> BDD-cost:   10
c ---[ 441]---> BDD-cost:   10
c ---[ 440]---> BDD-cost:   10
c ---[ 439]---> BDD-cost:   10
c ---[ 433]---> BDD-cost:   10
c ---[ 427]---> BDD-cost:   10
c ---[ 422]---> BDD-cost:   10
c ---[ 421]---> BDD-cost:   10
c ---[ 415]---> BDD-cost:   10
c ---[ 409]---> BDD-cost:   10
c ---[ 408]---> BDD-cost:   10
c ---[ 402]---> BDD-cost:   10
c ---[ 397]---> BDD-cost:   10
c ---[ 396]---> BDD-cost:   10
c ---[ 391]---> BDD-cost:   10
c ---[ 390]---> BDD-cost:   10
c ---[ 386]---> BDD-cost:   10
c ---[ 385]---> BDD-cost:   10
c ---[ 384]---> BDD-cost:   10
c ---[ 380]---> BDD-cost:   10
c ---[ 379]---> BDD-cost:   10
c ---[ 378]---> BDD-cost:   10
c ---[ 374]---> BDD-cost:   10
c ---[ 373]---> BDD-cost:   10
c ---[ 372]---> BDD-cost:   10
c ---[ 368]---> BDD-cost:   10
c ---[ 367]---> BDD-cost:   10
c ---[ 366]---> BDD-cost:   10
c ---[ 365]---> BDD-cost:   10
c ---[ 364]---> BDD-cost:   10
c ---[ 359]---> BDD-cost:   10
c ---[ 353]---> BDD-cost:   10
c ---[ 347]---> BDD-cost:   10
c ---[ 339]---> BDD-cost:   10
c ---[ 333]---> BDD-cost:   10
c ---[ 327]---> BDD-cost:   10
c ---[ 321]---> BDD-cost:   10
c ---[ 317]---> BDD-cost:   17
c ---[ 316]---> BDD-cost:   17
c ---[ 315]---> BDD-cost:   17
c ---[ 314]---> BDD-cost:   17
c ---[ 313]---> BDD-cost:   17
c ---[ 312]---> BDD-cost:   17
c ---[ 310]---> BDD-cost:   17
c ---[ 309]---> BDD-cost:   17
c ---[ 308]---> BDD-cost:   17
c ---[ 307]---> BDD-cost:   17
c ---[ 306]---> BDD-cost:   17
c ---[ 302]---> BDD-cost:   16
c ---[ 301]---> BDD-cost:   16
c ---[ 300]---> BDD-cost:   16
c ---[ 295]---> BDD-cost:   16
c ---[ 294]---> BDD-cost:   16
c ---[ 290]---> BDD-cost:   18
c ---[ 289]---> BDD-cost:   18
c ---[ 288]---> BDD-cost:   18
c ---[ 287]---> BDD-cost:   16
c ---[ 286]---> BDD-cost:   16
c ---[ 285]---> BDD-cost:   16
c ---[ 284]---> BDD-cost:   16
c ---[ 283]---> BDD-cost:   16
c ---[ 282]---> BDD-cost:   16
c ---[ 280]---> BDD-cost:   16
c ---[ 279]---> BDD-cost:   16
c ---[ 278]---> BDD-cost:   16
c ---[ 277]---> BDD-cost:   16
c ---[ 276]---> BDD-cost:   16
c ---[ 274]---> Sorter-cost: 3227     Base: 2 2 2 5 5 2 2 2 2 2 2 2 2 3
c ---[ 264]---> Sorter-cost: 3277     Base: 2 2 2 5 5 2 2 2 2 2 2 3 2 2 2
c ---[ 260]---> Adder-cost: 352   maxlim: 2411343   bits: 22/22
c ---[ 258]---> Adder-cost: 352   maxlim: 2411343   bits: 22/22
c ---[ 256]---> Adder-cost: 330   maxlim: 1694543   bits: 21/21
c ---[ 254]---> Adder-cost: 330   maxlim: 1694543   bits: 21/21
c ---[ 252]---> Adder-cost: 352   maxlim: 2104143   bits: 22/22
c ---[ 250]---> Sorter-cost: 2487     Base: 2 2 2 2 2 2 2 2 5 5 2 2 2 2
c ---[ 248]---> Adder-cost: 304   maxlim: 2309043   bits: 22/22
c ---[ 246]---> Adder-cost: 304   maxlim: 2104243   bits: 22/22
c ---[ 244]---> Adder-cost: 304   maxlim: 2104243   bits: 22/22
c ---[ 242]---> Adder-cost: 288   maxlim: 1694643   bits: 21/21
c ---[ 236]---> Sorter-cost: 2294     Base: 2 2 2 2 5 5 2 2 2 2 2 2 2 2
c ---[ 234]---> Adder-cost: 312   maxlim: 2587171   bits: 22/22
c ---[ 232]---> Adder-cost: 260   maxlim: 897571   bits: 20/20
c ---[ 224]---> Sorter-cost: 2815     Base: 2 2 2 5 5 2 2 2 2 2 2 2 2 3
c ---[ 222]---> Adder-cost: 350   maxlim: 1768271   bits: 22/21
c ---[ 216]---> Adder-cost: 274   maxlim: 1228100   bits: 21/21
c ---[ 214]---> Adder-cost: 312   maxlim: 1957187   bits: 22/21
c ---[ 212]---> Adder-cost: 312   maxlim: 1854787   bits: 22/21
c ---[ 210]---> Adder-cost: 390   maxlim: 2279471   bits: 22/22
c ---[ 208]---> Adder-cost: 332   maxlim: 845871   bits: 20/20
c ---[ 206]---> Adder-cost: 332   maxlim: 845871   bits: 20/20
c ---[ 204]---> Adder-cost: 332   maxlim: 845871   bits: 20/20
c ---[ 202]---> Adder-cost: 332   maxlim: 845871   bits: 20/20
c ---[ 200]---> Sorter-cost: 3241     Base: 2 2 2 2 5 5 2 2 2 2 2 2 5
c ---[ 198]---> Adder-cost: 440   maxlim: 3713071   bits: 23/22
c ---[ 196]---> Adder-cost: 368   maxlim: 999471   bits: 21/20
c ---[ 194]---> Adder-cost: 368   maxlim: 999471   bits: 21/20
c ---[ 192]---> Adder-cost: 368   maxlim: 999471   bits: 21/20
c ---[ 191]---> BDD-cost:   48
c ---[ 190]---> Sorter-cost:  386     Base: 2 2 2 2 2 2 2 2 2
c ---[ 189]---> Sorter-cost:  400     Base: 2 2 2 2 2 2 2 2 2
c ---[ 188]---> Sorter-cost:  801     Base: 2 2 2 2 2 2 2 2 2
c ---[ 187]---> Sorter-cost: 1088     Base: 2 2 2 2 2 2 2 2 2
c ---[ 186]---> Sorter-cost:  982     Base: 2 2 2 2 2 2 2 2 2
c ---[ 185]---> BDD-cost:   48
c ---[ 184]---> Sorter-cost:  386     Base: 2 2 2 2 2 2 2 2 2
c ---[ 183]---> Sorter-cost:  400     Base: 2 2 2 2 2 2 2 2 2
c ---[ 182]---> Sorter-cost:  781     Base: 2 2 2 2 2 2 2 2 2
c ---[ 181]---> Sorter-cost: 1034     Base: 2 2 2 2 2 2 2 2 2
c ---[ 180]---> Sorter-cost: 1032     Base: 2 2 2 2 2 2 2 2 2
c ---[ 179]---> BDD-cost:   48
c ---[ 178]---> Sorter-cost:  386     Base: 2 2 2 2 2 2 2 2 2
c ---[ 177]---> Sorter-cost:  391     Base: 2 2 2 2 2 2 2 2 2
c ---[ 176]---> Sorter-cost:  788     Base: 2 2 2 2 2 2 2 2 2
c ---[ 175]---> Sorter-cost: 1047     Base: 2 2 2 2 2 2 2 2 2
c ---[ 174]---> Sorter-cost: 1019     Base: 2 2 2 2 2 2 2 2 2
c ---[ 173]---> BDD-cost:   48
c ---[ 172]---> Sorter-cost:  370     Base: 2 2 2 2 2 2 2 2 2
c ---[ 171]---> Sorter-cost:  391     Base: 2 2 2 2 2 2 2 2 2
c ---[ 170]---> Sorter-cost:  747     Base: 2 2 2 2 2 2 2 2 2
c ---[ 169]---> Sorter-cost: 1022     Base: 2 2 2 2 2 2 2 2 2
c ---[ 168]---> Sorter-cost:  952     Base: 2 2 2 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:   10
c ---[ 157]---> BDD-cost:   10
c ---[ 156]---> BDD-cost:    3
c ---[ 155]---> BDD-cost:    3
c ---[ 154]---> BDD-cost:    3
c ---[ 153]---> BDD-cost:    3
c ---[ 152]---> BDD-cost:   10
c ---[ 151]---> BDD-cost:   10
c ---[ 150]---> BDD-cost:    3
c ---[ 149]---> BDD-cost:    3
c ---[ 148]---> BDD-cost:    3
c ---[ 147]---> BDD-cost:    3
c ---[ 146]---> BDD-cost:   10
c ---[ 145]---> BDD-cost:   10
c ---[ 144]---> BDD-cost:    3
c ---[ 142]---> BDD-cost:   10
c ---[ 141]---> BDD-cost:    3
c ---[ 140]---> BDD-cost:    3
c ---[ 139]---> BDD-cost:    3
c ---[ 138]---> BDD-cost:   10
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:   10
c ---[ 123]---> BDD-cost:    3
c ---[ 122]---> BDD-cost:    3
c ---[ 121]---> BDD-cost:    3
c ---[ 120]---> BDD-cost:   10
c ---[ 116]---> BDD-cost:   10
c ---[ 115]---> BDD-cost:    3
c ---[ 114]---> BDD-cost:    9
c ---[ 110]---> BDD-cost:   10
c ---[ 109]---> BDD-cost:    3
c ---[ 108]---> BDD-cost:    9
c ---[ 104]---> BDD-cost:    3
c ---[ 103]---> BDD-cost:    3
c ---[ 102]---> BDD-cost:    9
c ---[  98]---> BDD-cost:   10
c ---[  97]---> BDD-cost:    3
c ---[  96]---> BDD-cost:    9
c ---[  91]---> BDD-cost:    3
c ---[  90]---> BDD-cost:    3
c ---[  85]---> BDD-cost:   10
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:    9
c ---[  44]---> BDD-cost:    9
c ---[  43]---> BDD-cost:    9
c ---[  42]---> BDD-cost:    9
c ---[  41]---> BDD-cost:    3
c ---[  40]---> BDD-cost:   10
c ---[  39]---> BDD-cost:    9
c ---[  38]---> BDD-cost:    9
c ---[  37]---> BDD-cost:    9
c ---[  36]---> BDD-cost:    9
c ---[  35]---> BDD-cost:    3
c ---[  34]---> BDD-cost:   10
c ---[  33]---> BDD-cost:    8
c ---[  32]---> BDD-cost:    8
c ---[  31]---> BDD-cost:    8
c ---[  30]---> BDD-cost:    8
c ---[  29]---> BDD-cost:    3
c ---[  28]---> BDD-cost:   10
c ---[  27]---> BDD-cost:    8
c ---[  26]---> BDD-cost:    8
c ---[  25]---> BDD-cost:    8
c ---[  24]---> BDD-cost:    8
c ---[  22]---> BDD-cost:   10
c ---[  21]---> BDD-cost:    3
c ---[  20]---> BDD-cost:    9
c ---[  19]---> BDD-cost:    9
c ---[  18]---> BDD-cost:    9
c ---[  16]---> BDD-cost:   10
c ---[  15]---> BDD-cost:    3
c ---[  14]---> BDD-cost:    9
c ---[  13]---> BDD-cost:    9
c ---[  12]---> BDD-cost:    9
c ---[  10]---> BDD-cost:   10
c ---[   9]---> BDD-cost:    3
c ---[   8]---> BDD-cost:    9
c ---[   7]---> BDD-cost:    9
c ---[   6]---> BDD-cost:    9
c ---[   4]---> BDD-cost:    9
c ---[   3]---> BDD-cost:    3
c ---[   2]---> BDD-cost:    8
c ---[   1]---> BDD-cost:    8
c ---[   0]---> BDD-cost:    8
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  131984   372097 |   43994       0        0     nan |  0.000 % |
c |       100 |  131893   371869 |   48393      95      337     3.5 |  6.825 % |
c |       251 |  131833   371735 |   53232     243     1128     4.6 |  6.864 % |
c |       477 |  131829   371726 |   58556     468     2452     5.2 |  6.866 % |
c |       814 |  131829   371726 |   64411     805     5904     7.3 |  6.866 % |
c |      1320 |  131829   371726 |   70852    1311    10060     7.7 |  6.866 % |
c |      2080 |  131766   371585 |   77938    2067    16552     8.0 |  6.907 % |
c |      3219 |  131743   371526 |   85731    3204    31361     9.8 |  6.920 % |
c |      4927 |  131369   370664 |   94305    4894    54229    11.1 |  7.176 % |
c |      7489 |  131191   370240 |  103735    7441    89422    12.0 |  7.292 % |
c |     11334 |  130995   369791 |  114109   11272   134396    11.9 |  7.424 % |
c |     17100 |  130634   368964 |  125520   17026   227613    13.4 |  7.656 % |
c |     25749 |  130363   368341 |  138072   25650   343214    13.4 |  7.839 % |
c |     38724 |  130286   368151 |  151879   38609   624446    16.2 |  7.891 % |
c |     58185 |  130217   367957 |  167067   58063  1081641    18.6 |  7.930 % |
c |     87378 |  129973   367396 |  183773   87223  2028744    23.3 |  8.121 % |
c |    131167 |  129742   366846 |  202151  130997  3412336    26.0 |  8.296 % |
c |    196851 |  129657   366617 |  222366  196649  5557731    28.3 |  8.350 % |
c |    295378 |  129331   365820 |  244603   90242  2391247    26.5 |  8.577 % |
c |    443167 |  128851   364608 |  269063  237959  7047781    29.6 |  8.910 % |
c |    664850 |  128325   363313 |  295969  213696  6326538    29.6 |  9.280 % |

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/31050/stat): 31050 (minisat+_script) R 31049 31050 19316 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1846669924 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 1 0 0
Raw data (/proc/31050/statm): 174 3 169 147 0 27 0
[pid=31050] 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=31051
New process pid=31052
New process pid=31053
execve syscall for /bin/sed executable
One traced child (pid=31052) 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=31053) exited with status: 0
One traced child (pid=31051) exited with status: 0
New process pid=31054
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc17/normalized-mps-v2-20-10-vpm1.opb

[startup+10.0032 s]
Raw data (loadavg): 0.78 0.94 0.98 2/57 31054
Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31050/statm): 531 226 485 147 0 384 0
[pid=31050] vsize: 2124
Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 3832 0 0 0 962 17 0 0 25 0 1 0 1846669929 17592320 3668 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31054/statm): 4295 3668 145 145 0 4150 0
[pid=31054] vsize: 17180
Current children cumulated CPU time (s) 9.8
Current children cumulated vsize (Kb) 19304

[startup+20.0038 s]
Raw data (loadavg): 0.81 0.94 0.98 2/57 31054
Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31050/statm): 531 226 485 147 0 384 0
[pid=31050] vsize: 2124
Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 4196 0 0 0 1957 20 0 0 25 0 1 0 1846669929 19120128 4032 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31054/statm): 4668 4032 145 145 0 4523 0
[pid=31054] vsize: 18672
Current children cumulated CPU time (s) 19.78
Current children cumulated vsize (Kb) 20796

[startup+30.0044 s]
Raw data (loadavg): 0.84 0.94 0.98 2/57 31054
Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31050/statm): 531 226 485 147 0 384 0
[pid=31050] vsize: 2124
Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 4670 0 0 0 2948 23 0 0 25 0 1 0 1846669929 21131264 4506 4294967295 134512640 135094434 3221224432 3221223088 134557925 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31054/statm): 5159 4506 145 145 0 5014 0
[pid=31054] vsize: 20636
Current children cumulated CPU time (s) 29.72
Current children cumulated vsize (Kb) 22760

[startup+40.0051 s]
Raw data (loadavg): 0.86 0.94 0.98 2/57 31054
Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31050/statm): 531 226 485 147 0 384 0
[pid=31050] vsize: 2124
Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 5198 0 0 0 3938 27 0 0 25 0 1 0 1846669929 23228416 5034 4294967295 134512640 135094434 3221224432 3221223088 134557900 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31054/statm): 5671 5034 145 145 0 5526 0
[pid=31054] vsize: 22684
Current children cumulated CPU time (s) 39.66
Current children cumulated vsize (Kb) 24808

[startup+50.0067 s]
Raw data (loadavg): 0.88 0.94 0.98 2/57 31054
Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31050/statm): 531 226 485 147 0 384 0
[pid=31050] vsize: 2124
Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 5617 0 0 0 4928 31 0 0 25 0 1 0 1846669929 24899584 5453 4294967295 134512640 135094434 3221224432 3221223104 134556252 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31054/statm): 6079 5453 145 145 0 5934 0
[pid=31054] vsize: 24316
Current children cumulated CPU time (s) 49.6
Current children cumulated vsize (Kb) 26440

[startup+60.0072 s]
Raw data (loadavg): 0.90 0.94 0.98 1/57 31054
Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31050/statm): 531 226 485 147 0 384 0
[pid=31050] vsize: 2124
Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) T 31050 31050 19316 0 -1 0 6086 0 0 0 5920 34 0 0 25 0 1 0 1846669929 27041792 5922 4294967295 134512640 135094434 3221224432 3221222796 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/31054/statm): 6602 5922 145 145 0 6457 0
[pid=31054] vsize: 26408
Current children cumulated CPU time (s) 59.55
Current children cumulated vsize (Kb) 28532

[startup+70.0078 s]
Raw data (loadavg): 0.92 0.95 0.98 2/57 31054
Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31050/statm): 531 226 485 147 0 384 0
[pid=31050] vsize: 2124
Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 6382 0 0 0 6914 37 0 0 25 0 1 0 1846669929 28233728 6218 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31054/statm): 6893 6218 145 145 0 6748 0
[pid=31054] vsize: 27572
Current children cumulated CPU time (s) 69.52
Current children cumulated vsize (Kb) 29696

[startup+80.0094 s]
Raw data (loadavg): 0.93 0.95 0.98 2/57 31054
Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31050/statm): 531 226 485 147 0 384 0
[pid=31050] vsize: 2124
Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 6701 0 0 0 7909 38 0 0 25 0 1 0 1846669929 29540352 6537 4294967295 134512640 135094434 3221224432 3221223088 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31054/statm): 7212 6537 145 145 0 7067 0
[pid=31054] vsize: 28848
Current children cumulated CPU time (s) 79.48
Current children cumulated vsize (Kb) 30972

[startup+90.01 s]
Raw data (loadavg): 0.94 0.95 0.98 2/57 31054
Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31050/statm): 531 226 485 147 0 384 0
[pid=31050] vsize: 2124
Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 7021 0 0 0 8903 41 0 0 25 0 1 0 1846669929 30834688 6857 4294967295 134512640 135094434 3221224432 3221223088 134558235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31054/statm): 7528 6857 145 145 0 7383 0
[pid=31054] vsize: 30112
Current children cumulated CPU time (s) 89.45
Current children cumulated vsize (Kb) 32236

[startup+100.011 s]
Raw data (loadavg): 0.95 0.95 0.98 2/57 31054
Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31050/statm): 531 226 485 147 0 384 0
[pid=31050] vsize: 2124
Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 7304 0 0 0 9898 43 0 0 25 0 1 0 1846669929 31977472 7140 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31054/statm): 7807 7140 145 145 0 7662 0
[pid=31054] vsize: 31228
Current children cumulated CPU time (s) 99.42
Current children cumulated vsize (Kb) 33352

[startup+110.012 s]
Raw data (loadavg): 0.95 0.95 0.98 2/57 31054
Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31050/statm): 531 226 485 147 0 384 0
[pid=31050] vsize: 2124
Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 7540 0 0 0 10894 44 0 0 25 0 1 0 1846669929 32911360 7376 4294967295 134512640 135094434 3221224432 3221223088 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31054/statm): 8035 7376 145 145 0 7890 0
[pid=31054] vsize: 32140
Current children cumulated CPU time (s) 109.39
Current children cumulated vsize (Kb) 34264

[startup+120.013 s]
Raw data (loadavg): 0.96 0.95 0.98 2/57 31054
Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31050/statm): 531 226 485 147 0 384 0
[pid=31050] vsize: 2124
Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 7762 0 0 0 11890 46 0 0 25 0 1 0 1846669929 33824768 7598 4294967295 134512640 135094434 3221224432 3221223088 134557996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31054/statm): 8258 7598 145 145 0 8113 0
[pid=31054] vsize: 33032
Current children cumulated CPU time (s) 119.37
Current children cumulated vsize (Kb) 35156

[startup+130.013 s]
Raw data (loadavg): 0.97 0.95 0.98 2/57 31054
Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31050/statm): 531 226 485 147 0 384 0
[pid=31050] vsize: 2124
Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 7954 0 0 0 12888 47 0 0 25 0 1 0 1846669929 34619392 7790 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31054/statm): 8452 7790 145 145 0 8307 0
[pid=31054] vsize: 33808
Current children cumulated CPU time (s) 129.36
Current children cumulated vsize (Kb) 35932

[startup+140.014 s]
Raw data (loadavg): 0.97 0.95 0.98 2/57 31054
Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31050/statm): 531 226 485 147 0 384 0
[pid=31050] vsize: 2124
Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 8131 0 0 0 13886 47 0 0 25 0 1 0 1846669929 35332096 7967 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31054/statm): 8626 7967 145 145 0 8481 0
[pid=31054] vsize: 34504
Current children cumulated CPU time (s) 139.34
Current children cumulated vsize (Kb) 36628

[startup+150.016 s]
Raw data (loadavg): 0.98 0.95 0.98 2/57 31054
Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31050/statm): 531 226 485 147 0 384 0
[pid=31050] vsize: 2124
Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 8291 0 0 0 14884 48 0 0 25 0 1 0 1846669929 35966976 8127 4294967295 134512640 135094434 3221224432 3221223104 134556085 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31054/statm): 8781 8127 145 145 0 8636 0
[pid=31054] vsize: 35124
Current children cumulated CPU time (s) 149.33
Current children cumulated vsize (Kb) 37248

[startup+160.016 s]
Raw data (loadavg): 0.98 0.95 0.98 2/57 31054
Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31050/statm): 531 226 485 147 0 384 0
[pid=31050] vsize: 2124
Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 8519 0 0 0 15880 50 0 0 25 0 1 0 1846669929 37441536 8355 4294967295 134512640 135094434 3221224432 3221223024 134556864 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31054/statm): 9141 8355 145 145 0 8996 0
[pid=31054] vsize: 36564
Current children cumulated CPU time (s) 159.31
Current children cumulated vsize (Kb) 38688

[startup+170.017 s]
Raw data (loadavg): 0.98 0.95 0.98 2/57 31054
Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31050/statm): 531 226 485 147 0 384 0
[pid=31050] vsize: 2124
Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 8823 0 0 0 16874 53 0 0 25 0 1 0 1846669929 38658048 8659 4294967295 134512640 135094434 3221224432 3221223088 134557860 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31054/statm): 9438 8659 145 145 0 9293 0
[pid=31054] vsize: 37752
Current children cumulated CPU time (s) 169.28
Current children cumulated vsize (Kb) 39876

[startup+180.017 s]
Raw data (loadavg): 0.98 0.96 0.98 2/57 31054
Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31050/statm): 531 226 485 147 0 384 0
[pid=31050] vsize: 2124
Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 9159 0 0 0 17869 55 0 0 25 0 1 0 1846669929 40038400 8995 4294967295 134512640 135094434 3221224432 3221223088 134557945 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31054/statm): 9775 8995 145 145 0 9630 0
[pid=31054] vsize: 39100
Current children cumulated CPU time (s) 179.25
Current children cumulated vsize (Kb) 41224

[startup+190.018 s]
Raw data (loadavg): 0.99 0.96 0.98 2/57 31054
Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31050/statm): 531 226 485 147 0 384 0
[pid=31050] vsize: 2124
Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 9381 0 0 0 18865 57 0 0 25 0 1 0 1846669929 40910848 9217 4294967295 134512640 135094434 3221224432 3221223088 134557840 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31054/statm): 9988 9217 145 145 0 9843 0
[pid=31054] vsize: 39952
Current children cumulated CPU time (s) 189.23
Current children cumulated vsize (Kb) 42076

[startup+200.019 s]
Raw data (loadavg): 0.99 0.96 0.98 2/57 31054
Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31050/statm): 531 226 485 147 0 384 0
[pid=31050] vsize: 2124
Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 9538 0 0 0 19863 58 0 0 25 0 1 0 1846669929 41533440 9374 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31054/statm): 10140 9374 145 145 0 9995 0
[pid=31054] vsize: 40560
Current children cumulated CPU time (s) 199.22
Current children cumulated vsize (Kb) 42684

[startup+210.019 s]
Raw data (loadavg): 0.99 0.96 0.98 2/57 31054
Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31050/statm): 531 226 485 147 0 384 0
[pid=31050] vsize: 2124
Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 9695 0 0 0 20860 59 0 0 25 0 1 0 1846669929 42160128 9531 4294967295 134512640 135094434 3221224432 3221223088 134557863 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31054/statm): 10293 9531 145 145 0 10148 0
[pid=31054] vsize: 41172
Current children cumulated CPU time (s) 209.2
Current children cumulated vsize (Kb) 43296

[startup+220.02 s]
Raw data (loadavg): 0.99 0.96 0.98 2/57 31054
Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31050/statm): 531 226 485 147 0 384 0
[pid=31050] vsize: 2124
Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 9848 0 0 0 21857 61 0 0 25 0 1 0 1846669929 42782720 9684 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31054/statm): 10445 9684 145 145 0 10300 0
[pid=31054] vsize: 41780
Current children cumulated CPU time (s) 219.19
Current children cumulated vsize (Kb) 43904

[startup+230.02 s]
Raw data (loadavg): 0.99 0.96 0.98 2/57 31054
Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31050/statm): 531 226 485 147 0 384 0
[pid=31050] vsize: 2124
Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 10003 0 0 0 22855 62 0 0 25 0 1 0 1846669929 43417600 9839 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31054/statm): 10600 9839 145 145 0 10455 0
[pid=31054] vsize: 42400
Current children cumulated CPU time (s) 229.18
Current children cumulated vsize (Kb) 44524

[startup+240.021 s]
Raw data (loadavg): 0.99 0.96 0.98 2/57 31054
Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31050/statm): 531 226 485 147 0 384 0
[pid=31050] vsize: 2124
Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 10138 0 0 0 23853 64 0 0 25 0 1 0 1846669929 43958272 9974 4294967295 134512640 135094434 3221224432 3221223120 134554739 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31054/statm): 10732 9974 145 145 0 10587 0
[pid=31054] vsize: 42928
Current children cumulated CPU time (s) 239.18
Current children cumulated vsize (Kb) 45052

[startup+250.022 s]
Raw data (loadavg): 0.99 0.96 0.98 2/57 31054
Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31050/statm): 531 226 485 147 0 384 0
[pid=31050] vsize: 2124
Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 10267 0 0 0 24850 65 0 0 25 0 1 0 1846669929 44486656 10103 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31054/statm): 10861 10103 145 145 0 10716 0
[pid=31054] vsize: 43444
Current children cumulated CPU time (s) 249.16
Current children cumulated vsize (Kb) 45568

[startup+260.022 s]
Raw data (loadavg): 0.99 0.96 0.98 2/57 31054
Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31050/statm): 531 226 485 147 0 384 0
[pid=31050] vsize: 2124
Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 10386 0 0 0 25849 66 0 0 25 0 1 0 1846669929 44990464 10222 4294967295 134512640 135094434 3221224432 3221223104 134556170 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31054/statm): 10984 10222 145 145 0 10839 0
[pid=31054] vsize: 43936
Current children cumulated CPU time (s) 259.16
Current children cumulated vsize (Kb) 46060

[startup+270.023 s]
Raw data (loadavg): 0.99 0.96 0.98 2/57 31054
Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31050/statm): 531 226 485 147 0 384 0
[pid=31050] vsize: 2124
Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 10498 0 0 0 26847 66 0 0 25 0 1 0 1846669929 45441024 10334 4294967295 134512640 135094434 3221224432 3221223088 134557950 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31054/statm): 11094 10334 145 145 0 10949 0
[pid=31054] vsize: 44376
Current children cumulated CPU time (s) 269.14
Current children cumulated vsize (Kb) 46500

[startup+280.024 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 31054
Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31050/statm): 531 226 485 147 0 384 0
[pid=31050] vsize: 2124
Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 10619 0 0 0 27846 67 0 0 25 0 1 0 1846669929 45944832 10455 4294967295 134512640 135094434 3221224432 3221223088 134558218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31054/statm): 11217 10455 145 145 0 11072 0
[pid=31054] vsize: 44868
Current children cumulated CPU time (s) 279.14
Current children cumulated vsize (Kb) 46992

[startup+290.024 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 31054
Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31050/statm): 531 226 485 147 0 384 0
[pid=31050] vsize: 2124
Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 10736 0 0 0 28845 68 0 0 25 0 1 0 1846669929 46440448 10572 4294967295 134512640 135094434 3221224432 3221223088 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31054/statm): 11338 10572 145 145 0 11193 0
[pid=31054] vsize: 45352
Current children cumulated CPU time (s) 289.14
Current children cumulated vsize (Kb) 47476

[startup+300.025 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 31054
Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31050/statm): 531 226 485 147 0 384 0
[pid=31050] vsize: 2124
Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 10857 0 0 0 29843 69 0 0 25 0 1 0 1846669929 46911488 10693 4294967295 134512640 135094434 3221224432 3221223088 134558218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31054/statm): 11453 10693 145 145 0 11308 0
[pid=31054] vsize: 45812
Current children cumulated CPU time (s) 299.13
Current children cumulated vsize (Kb) 47936

[startup+310.025 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 31054
Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31050/statm): 531 226 485 147 0 384 0
[pid=31050] vsize: 2124
Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 10973 0 0 0 30841 70 0 0 25 0 1 0 1846669929 47374336 10809 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31054/statm): 11566 10809 145 145 0 11421 0
[pid=31054] vsize: 46264
Current children cumulated CPU time (s) 309.12
Current children cumulated vsize (Kb) 48388

[startup+320.026 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 31054
Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31050/statm): 531 226 485 147 0 384 0
[pid=31050] vsize: 2124
Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 11075 0 0 0 31840 70 0 0 25 0 1 0 1846669929 47816704 10911 4294967295 134512640 135094434 3221224432 3221223088 134558187 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31054/statm): 11674 10911 145 145 0 11529 0
[pid=31054] vsize: 46696
Current children cumulated CPU time (s) 319.11
Current children cumulated vsize (Kb) 48820

[startup+330.027 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 31054
Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31050/statm): 531 226 485 147 0 384 0
[pid=31050] vsize: 2124
Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 11172 0 0 0 32839 71 0 0 25 0 1 0 1846669929 48193536 11008 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31054/statm): 11766 11008 145 145 0 11621 0
[pid=31054] vsize: 47064
Current children cumulated CPU time (s) 329.11
Current children cumulated vsize (Kb) 49188

[startup+340.028 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 31054
Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31050/statm): 531 226 485 147 0 384 0
[pid=31050] vsize: 2124
Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 11328 0 0 0 33835 72 0 0 25 0 1 0 1846669929 48828416 11164 4294967295 134512640 135094434 3221224432 3221223104 134555957 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31054/statm): 11921 11164 145 145 0 11776 0
[pid=31054] vsize: 47684
Current children cumulated CPU time (s) 339.08
Current children cumulated vsize (Kb) 49808

[startup+350.03 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 31054
Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31050/statm): 531 226 485 147 0 384 0
[pid=31050] vsize: 2124
Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 11588 0 0 0 34831 75 0 0 25 0 1 0 1846669929 49934336 11424 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31054/statm): 12191 11424 145 145 0 12046 0
[pid=31054] vsize: 48764
Current children cumulated CPU time (s) 349.07
Current children cumulated vsize (Kb) 50888

[startup+360.03 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 31054
Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31050/statm): 531 226 485 147 0 384 0
[pid=31050] vsize: 2124
Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 11807 0 0 0 35828 76 0 0 25 0 1 0 1846669929 50892800 11643 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31054/statm): 12425 11643 145 145 0 12280 0
[pid=31054] vsize: 49700
Current children cumulated CPU time (s) 359.05
Current children cumulated vsize (Kb) 51824

[startup+370.031 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 31054
Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31050/statm): 531 226 485 147 0 384 0
[pid=31050] vsize: 2124
Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 12017 0 0 0 36824 78 0 0 25 0 1 0 1846669929 51773440 11853 4294967295 134512640 135094434 3221224432 3221223120 134554751 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31054/statm): 12640 11853 145 145 0 12495 0
[pid=31054] vsize: 50560
Current children cumulated CPU time (s) 369.03
Current children cumulated vsize (Kb) 52684

[startup+380.032 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 31054
Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31050/statm): 531 226 485 147 0 384 0
[pid=31050] vsize: 2124
Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 12219 0 0 0 37821 80 0 0 25 0 1 0 1846669929 52604928 12055 4294967295 134512640 135094434 3221224432 3221223088 134558187 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31054/statm): 12843 12055 145 145 0 12698 0
[pid=31054] vsize: 51372
Current children cumulated CPU time (s) 379.02
Current children cumulated vsize (Kb) 53496

[startup+390.032 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 31054
Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31050/statm): 531 226 485 147 0 384 0
[pid=31050] vsize: 2124
Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 12468 0 0 0 38817 81 0 0 25 0 1 0 1846669929 53604352 12304 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31054/statm): 13087 12304 145 145 0 12942 0
[pid=31054] vsize: 52348
Current children cumulated CPU time (s) 388.99
Current children cumulated vsize (Kb) 54472

[startup+400.033 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 31054
Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31050/statm): 531 226 485 147 0 384 0
[pid=31050] vsize: 2124
Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 12708 0 0 0 39813 83 0 0 25 0 1 0 1846669929 54571008 12544 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31054/statm): 13323 12544 145 145 0 13178 0
[pid=31054] vsize: 53292
Current children cumulated CPU time (s) 398.97
Current children cumulated vsize (Kb) 55416

[startup+410.033 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 31054
Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31050/statm): 531 226 485 147 0 384 0
[pid=31050] vsize: 2124
Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 12806 0 0 0 40811 84 0 0 25 0 1 0 1846669929 54956032 12642 4294967295 134512640 135094434 3221224432 3221223024 134551463 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31054/statm): 13417 12642 145 145 0 13272 0
[pid=31054] vsize: 53668
Current children cumulated CPU time (s) 408.96
Current children cumulated vsize (Kb) 55792

[startup+420.034 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 31054
Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31050/statm): 531 226 485 147 0 384 0
[pid=31050] vsize: 2124
Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 12806 0 0 0 41811 84 0 0 25 0 1 0 1846669929 54956032 12642 4294967295 134512640 135094434 3221224432 3221223088 134557859 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31054/statm): 13417 12642 145 145 0 13272 0
[pid=31054] vsize: 53668
Current children cumulated CPU time (s) 418.96
Current children cumulated vsize (Kb) 55792

[startup+430.036 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 31054
Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31050/statm): 531 226 485 147 0 384 0
[pid=31050] vsize: 2124
Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 12806 0 0 0 42811 85 0 0 25 0 1 0 1846669929 54956032 12642 4294967295 134512640 135094434 3221224432 3221223088 134558405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31054/statm): 13417 12642 145 145 0 13272 0
[pid=31054] vsize: 53668
Current children cumulated CPU time (s) 428.97
Current children cumulated vsize (Kb) 55792

[startup+440.036 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 31054
Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31050/statm): 531 226 485 147 0 384 0
[pid=31050] vsize: 2124
Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 12806 0 0 0 43811 85 0 0 25 0 1 0 1846669929 54956032 12642 4294967295 134512640 135094434 3221224432 3221223024 134557336 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31054/statm): 13417 12642 145 145 0 13272 0
[pid=31054] vsize: 53668
Current children cumulated CPU time (s) 438.97
Current children cumulated vsize (Kb) 55792

[startup+450.037 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 31054
Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31050/statm): 531 226 485 147 0 384 0
[pid=31050] vsize: 2124
Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 12807 0 0 0 44812 85 0 0 25 0 1 0 1846669929 54956032 12643 4294967295 134512640 135094434 3221224432 3221223056 134557642 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31054/statm): 13417 12643 145 145 0 13272 0
[pid=31054] vsize: 53668
Current children cumulated CPU time (s) 448.98
Current children cumulated vsize (Kb) 55792

[startup+460.037 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 31054
Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31050/statm): 531 226 485 147 0 384 0
[pid=31050] vsize: 2124
Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 12808 0 0 0 45812 85 0 0 25 0 1 0 1846669929 54956032 12644 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31054/statm): 13417 12644 145 145 0 13272 0
[pid=31054] vsize: 53668
Current children cumulated CPU time (s) 458.98
Current children cumulated vsize (Kb) 55792

[startup+470.038 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 31054
Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31050/statm): 531 226 485 147 0 384 0
[pid=31050] vsize: 2124
Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 12808 0 0 0 46812 85 0 0 25 0 1 0 1846669929 54956032 12644 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31054/statm): 13417 12644 145 145 0 13272 0
[pid=31054] vsize: 53668
Current children cumulated CPU time (s) 468.98
Current children cumulated vsize (Kb) 55792

[startup+480.039 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 31054
Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31050/statm): 531 226 485 147 0 384 0
[pid=31050] vsize: 2124
Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 12808 0 0 0 47812 85 0 0 25 0 1 0 1846669929 54956032 12644 4294967295 134512640 135094434 3221224432 3221223088 134557884 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31054/statm): 13417 12644 145 145 0 13272 0
[pid=31054] vsize: 53668
Current children cumulated CPU time (s) 478.98
Current children cumulated vsize (Kb) 55792

[startup+490.039 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 31054
Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31050/statm): 531 226 485 147 0 384 0
[pid=31050] vsize: 2124
Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 12808 0 0 0 48812 85 0 0 25 0 1 0 1846669929 54956032 12644 4294967295 134512640 135094434 3221224432 3221223056 134557665 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31054/statm): 13417 12644 145 145 0 13272 0
[pid=31054] vsize: 53668
Current children cumulated CPU time (s) 488.98
Current children cumulated vsize (Kb) 55792

[startup+500.04 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 31054
Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31050/statm): 531 226 485 147 0 384 0
[pid=31050] vsize: 2124
Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 12808 0 0 0 49812 85 0 0 25 0 1 0 1846669929 54956032 12644 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31054/statm): 13417 12644 145 145 0 13272 0
[pid=31054] vsize: 53668
Current children cumulated CPU time (s) 498.98
Current children cumulated vsize (Kb) 55792

[startup+510.04 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 31054
Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31050/statm): 531 226 485 147 0 384 0
[pid=31050] vsize: 2124
Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 12808 0 0 0 50812 85 0 0 25 0 1 0 1846669929 54956032 12644 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31054/statm): 13417 12644 145 145 0 13272 0
[pid=31054] vsize: 53668
Current children cumulated CPU time (s) 508.98
Current children cumulated vsize (Kb) 55792

[startup+520.041 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 31054
Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31050/statm): 531 226 485 147 0 384 0
[pid=31050] vsize: 2124
Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 12808 0 0 0 51812 85 0 0 25 0 1 0 1846669929 54956032 12644 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31054/statm): 13417 12644 145 145 0 13272 0
[pid=31054] vsize: 53668
Current children cumulated CPU time (s) 518.98
Current children cumulated vsize (Kb) 55792

[startup+530.042 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 31054
Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31050/statm): 531 226 485 147 0 384 0
[pid=31050] vsize: 2124
Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 12808 0 0 0 52813 85 0 0 25 0 1 0 1846669929 54956032 12644 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31054/statm): 13417 12644 145 145 0 13272 0
[pid=31054] vsize: 53668
Current children cumulated CPU time (s) 528.99
Current children cumulated vsize (Kb) 55792

[startup+540.042 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 31054
Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31050/statm): 531 226 485 147 0 384 0
[pid=31050] vsize: 2124
Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 12810 0 0 0 53813 85 0 0 25 0 1 0 1846669929 54956032 12646 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31054/statm): 13417 12646 145 145 0 13272 0
[pid=31054] vsize: 53668
Current children cumulated CPU time (s) 538.99
Current children cumulated vsize (Kb) 55792

[startup+550.042 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 31054
Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31050/statm): 531 226 485 147 0 384 0
[pid=31050] vsize: 2124
Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 12810 0 0 0 54813 85 0 0 25 0 1 0 1846669929 54956032 12646 4294967295 134512640 135094434 3221224432 3221223088 134558225 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31054/statm): 13417 12646 145 145 0 13272 0
[pid=31054] vsize: 53668
Current children cumulated CPU time (s) 548.99
Current children cumulated vsize (Kb) 55792

[startup+560.042 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 31054
Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31050/statm): 531 226 485 147 0 384 0
[pid=31050] vsize: 2124
Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 12810 0 0 0 55813 85 0 0 25 0 1 0 1846669929 54956032 12646 4294967295 134512640 135094434 3221224432 3221223056 134557655 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31054/statm): 13417 12646 145 145 0 13272 0
[pid=31054] vsize: 53668
Current children cumulated CPU time (s) 558.99
Current children cumulated vsize (Kb) 55792

[startup+570.043 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 31054
Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31050/statm): 531 226 485 147 0 384 0
[pid=31050] vsize: 2124
Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 12810 0 0 0 56813 85 0 0 25 0 1 0 1846669929 54956032 12646 4294967295 134512640 135094434 3221224432 3221223088 134557937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31054/statm): 13417 12646 145 145 0 13272 0
[pid=31054] vsize: 53668
Current children cumulated CPU time (s) 568.99
Current children cumulated vsize (Kb) 55792

[startup+580.044 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 31054
Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31050/statm): 531 226 485 147 0 384 0
[pid=31050] vsize: 2124
Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 12810 0 0 0 57814 85 0 0 25 0 1 0 1846669929 54956032 12646 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31054/statm): 13417 12646 145 145 0 13272 0
[pid=31054] vsize: 53668
Current children cumulated CPU time (s) 579
Current children cumulated vsize (Kb) 55792

[startup+590.044 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 31054
Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31050/statm): 531 226 485 147 0 384 0
[pid=31050] vsize: 2124
Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 12811 0 0 0 58814 85 0 0 25 0 1 0 1846669929 54956032 12647 4294967295 134512640 135094434 3221224432 3221223068 134557560 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31054/statm): 13417 12647 145 145 0 13272 0
[pid=31054] vsize: 53668
Current children cumulated CPU time (s) 589
Current children cumulated vsize (Kb) 55792

[startup+600.045 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 31054
Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31050/statm): 531 226 485 147 0 384 0
[pid=31050] vsize: 2124
Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 12811 0 0 0 59814 85 0 0 25 0 1 0 1846669929 54956032 12647 4294967295 134512640 135094434 3221224432 3221223088 134558172 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31054/statm): 13417 12647 145 145 0 13272 0
[pid=31054] vsize: 53668
Current children cumulated CPU time (s) 599
Current children cumulated vsize (Kb) 55792

[startup+610.045 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 31054
Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31050/statm): 531 226 485 147 0 384 0
[pid=31050] vsize: 2124
Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 12811 0 0 0 60814 85 0 0 25 0 1 0 1846669929 54956032 12647 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31054/statm): 13417 12647 145 145 0 13272 0
[pid=31054] vsize: 53668
Current children cumulated CPU time (s) 609
Current children cumulated vsize (Kb) 55792

[startup+620.046 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 31054
Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31050/statm): 531 226 485 147 0 384 0
[pid=31050] vsize: 2124
Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 12811 0 0 0 61815 85 0 0 25 0 1 0 1846669929 54956032 12647 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31054/statm): 13417 12647 145 145 0 13272 0
[pid=31054] vsize: 53668
Current children cumulated CPU time (s) 619.01
Current children cumulated vsize (Kb) 55792

[startup+630.048 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 31054
Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31050/statm): 531 226 485 147 0 384 0
[pid=31050] vsize: 2124
Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 12811 0 0 0 62815 85 0 0 25 0 1 0 1846669929 54956032 12647 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31054/statm): 13417 12647 145 145 0 13272 0
[pid=31054] vsize: 53668
Current children cumulated CPU time (s) 629.01
Current children cumulated vsize (Kb) 55792

[startup+640.048 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 31054
Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31050/statm): 531 226 485 147 0 384 0
[pid=31050] vsize: 2124
Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 12812 0 0 0 63815 85 0 0 25 0 1 0 1846669929 54956032 12648 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31054/statm): 13417 12648 145 145 0 13272 0
[pid=31054] vsize: 53668
Current children cumulated CPU time (s) 639.01
Current children cumulated vsize (Kb) 55792

[startup+650.049 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 31054
Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31050/statm): 531 226 485 147 0 384 0
[pid=31050] vsize: 2124
Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 12812 0 0 0 64815 85 0 0 25 0 1 0 1846669929 54956032 12648 4294967295 134512640 135094434 3221224432 3221223088 134557976 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31054/statm): 13417 12648 145 145 0 13272 0
[pid=31054] vsize: 53668
Current children cumulated CPU time (s) 649.01
Current children cumulated vsize (Kb) 55792

[startup+660.049 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 31054
Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31050/statm): 531 226 485 147 0 384 0
[pid=31050] vsize: 2124
Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 12812 0 0 0 65816 85 0 0 25 0 1 0 1846669929 54956032 12648 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31054/statm): 13417 12648 145 145 0 13272 0
[pid=31054] vsize: 53668
Current children cumulated CPU time (s) 659.02
Current children cumulated vsize (Kb) 55792

[startup+670.05 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 31054
Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31050/statm): 531 226 485 147 0 384 0
[pid=31050] vsize: 2124
Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 12812 0 0 0 66816 85 0 0 25 0 1 0 1846669929 54956032 12648 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31054/statm): 13417 12648 145 145 0 13272 0
[pid=31054] vsize: 53668
Current children cumulated CPU time (s) 669.02
Current children cumulated vsize (Kb) 55792

[startup+680.051 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 31054
Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31050/statm): 531 226 485 147 0 384 0
[pid=31050] vsize: 2124
Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 12814 0 0 0 67816 86 0 0 25 0 1 0 1846669929 54956032 12650 4294967295 134512640 135094434 3221224432 3221223088 134558187 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31054/statm): 13417 12650 145 145 0 13272 0
[pid=31054] vsize: 53668
Current children cumulated CPU time (s) 679.03
Current children cumulated vsize (Kb) 55792

[startup+690.051 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 31054
Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31050/statm): 531 226 485 147 0 384 0
[pid=31050] vsize: 2124
Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 12814 0 0 0 68816 86 0 0 25 0 1 0 1846669929 54956032 12650 4294967295 134512640 135094434 3221224432 3221223088 134558235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31054/statm): 13417 12650 145 145 0 13272 0
[pid=31054] vsize: 53668
Current children cumulated CPU time (s) 689.03
Current children cumulated vsize (Kb) 55792

[startup+700.052 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 31054
Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31050/statm): 531 226 485 147 0 384 0
[pid=31050] vsize: 2124
Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 12815 0 0 0 69816 86 0 0 25 0 1 0 1846669929 54956032 12651 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31054/statm): 13417 12651 145 145 0 13272 0
[pid=31054] vsize: 53668
Current children cumulated CPU time (s) 699.03
Current children cumulated vsize (Kb) 55792

[startup+710.052 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 31054
Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31050/statm): 531 226 485 147 0 384 0
[pid=31050] vsize: 2124
Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 12848 0 0 0 70816 86 0 0 25 0 1 0 1846669929 55083008 12684 4294967295 134512640 135094434 3221224432 3221223072 134562139 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31054/statm): 13448 12684 145 145 0 13303 0
[pid=31054] vsize: 53792
Current children cumulated CPU time (s) 709.03
Current children cumulated vsize (Kb) 55916

[startup+720.053 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 31054
Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31050/statm): 531 226 485 147 0 384 0
[pid=31050] vsize: 2124
Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 13011 0 0 0 71812 87 0 0 25 0 1 0 1846669929 55767040 12847 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31054/statm): 13615 12847 145 145 0 13470 0
[pid=31054] vsize: 54460
Current children cumulated CPU time (s) 719
Current children cumulated vsize (Kb) 56584

[startup+730.054 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 31054
Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31050/statm): 531 226 485 147 0 384 0
[pid=31050] vsize: 2124
Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 13123 0 0 0 72810 88 0 0 25 0 1 0 1846669929 56221696 12959 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31054/statm): 13726 12959 145 145 0 13581 0
[pid=31054] vsize: 54904
Current children cumulated CPU time (s) 728.99
Current children cumulated vsize (Kb) 57028

[startup+740.054 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 31054
Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31050/statm): 531 226 485 147 0 384 0
[pid=31050] vsize: 2124
Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 13284 0 0 0 73807 90 0 0 25 0 1 0 1846669929 56930304 13120 4294967295 134512640 135094434 3221224432 3221223088 134558235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31054/statm): 13899 13120 145 145 0 13754 0
[pid=31054] vsize: 55596
Current children cumulated CPU time (s) 738.98
Current children cumulated vsize (Kb) 57720

[startup+750.055 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 31054
Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31050/statm): 531 226 485 147 0 384 0
[pid=31050] vsize: 2124
Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 13410 0 0 0 74806 91 0 0 25 0 1 0 1846669929 57487360 13246 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31054/statm): 14035 13246 145 145 0 13890 0
[pid=31054] vsize: 56140
Current children cumulated CPU time (s) 748.98
Current children cumulated vsize (Kb) 58264

[startup+760.055 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 31054
Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31050/statm): 531 226 485 147 0 384 0
[pid=31050] vsize: 2124
Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 13528 0 0 0 75803 92 0 0 25 0 1 0 1846669929 57970688 13364 4294967295 134512640 135094434 3221224432 3221223088 134557964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31054/statm): 14153 13364 145 145 0 14008 0
[pid=31054] vsize: 56612
Current children cumulated CPU time (s) 758.96
Current children cumulated vsize (Kb) 58736

[startup+770.056 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 31054
Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31050/statm): 531 226 485 147 0 384 0
[pid=31050] vsize: 2124
Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 13710 0 0 0 76801 93 0 0 25 0 1 0 1846669929 58740736 13546 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31054/statm): 14341 13546 145 145 0 14196 0
[pid=31054] vsize: 57364
Current children cumulated CPU time (s) 768.95
Current children cumulated vsize (Kb) 59488

[startup+780.057 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 31054
Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31050/statm): 531 226 485 147 0 384 0
[pid=31050] vsize: 2124
Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) T 31050 31050 19316 0 -1 0 13842 0 0 0 77799 94 0 0 25 0 1 0 1846669929 59273216 13678 4294967295 134512640 135094434 3221224432 3221222796 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/31054/statm): 14471 13678 145 145 0 14326 0
[pid=31054] vsize: 57884
Current children cumulated CPU time (s) 778.94
Current children cumulated vsize (Kb) 60008

[startup+790.057 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 31054
Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31050/statm): 531 226 485 147 0 384 0
[pid=31050] vsize: 2124
Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 14043 0 0 0 78795 95 0 0 25 0 1 0 1846669929 60100608 13879 4294967295 134512640 135094434 3221224432 3221223088 134558162 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31054/statm): 14673 13879 145 145 0 14528 0
[pid=31054] vsize: 58692
Current children cumulated CPU time (s) 788.91
Current children cumulated vsize (Kb) 60816

[startup+800.058 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 31054
Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31050/statm): 531 226 485 147 0 384 0
[pid=31050] vsize: 2124
Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 14269 0 0 0 79792 97 0 0 25 0 1 0 1846669929 61042688 14105 4294967295 134512640 135094434 3221224432 3221223056 134557714 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31054/statm): 14903 14105 145 145 0 14758 0
[pid=31054] vsize: 59612
Current children cumulated CPU time (s) 798.9
Current children cumulated vsize (Kb) 61736

[startup+810.058 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 31054
Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31050/statm): 531 226 485 147 0 384 0
[pid=31050] vsize: 2124
Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 14367 0 0 0 80791 98 0 0 25 0 1 0 1846669929 61452288 14203 4294967295 134512640 135094434 3221224432 3221223056 134557726 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31054/statm): 15003 14203 145 145 0 14858 0
[pid=31054] vsize: 60012
Current children cumulated CPU time (s) 808.9
Current children cumulated vsize (Kb) 62136

[startup+820.059 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 31054
Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31050/statm): 531 226 485 147 0 384 0
[pid=31050] vsize: 2124
Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 14474 0 0 0 81789 98 0 0 25 0 1 0 1846669929 61878272 14310 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31054/statm): 15107 14310 145 145 0 14962 0
[pid=31054] vsize: 60428
Current children cumulated CPU time (s) 818.88
Current children cumulated vsize (Kb) 62552

[startup+830.06 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 31054
Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31050/statm): 531 226 485 147 0 384 0
[pid=31050] vsize: 2124
Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 14564 0 0 0 82788 99 0 0 25 0 1 0 1846669929 62230528 14400 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31054/statm): 15193 14400 145 145 0 15048 0
[pid=31054] vsize: 60772
Current children cumulated CPU time (s) 828.88
Current children cumulated vsize (Kb) 62896

[startup+840.06 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 31054
Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31050/statm): 531 226 485 147 0 384 0
[pid=31050] vsize: 2124
Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 14655 0 0 0 83786 100 0 0 25 0 1 0 1846669929 62607360 14491 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31054/statm): 15285 14491 145 145 0 15140 0
[pid=31054] vsize: 61140
Current children cumulated CPU time (s) 838.87
Current children cumulated vsize (Kb) 63264

[startup+850.061 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 31054
Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31050/statm): 531 226 485 147 0 384 0
[pid=31050] vsize: 2124
Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 14754 0 0 0 84785 100 0 0 25 0 1 0 1846669929 63004672 14590 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31054/statm): 15382 14590 145 145 0 15237 0
[pid=31054] vsize: 61528
Current children cumulated CPU time (s) 848.86
Current children cumulated vsize (Kb) 63652

[startup+860.061 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 31054
Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31050/statm): 531 226 485 147 0 384 0
[pid=31050] vsize: 2124
Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 14861 0 0 0 85784 101 0 0 25 0 1 0 1846669929 64520192 14697 4294967295 134512640 135094434 3221224432 3221223092 134553515 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31054/statm): 15752 14697 145 145 0 15607 0
[pid=31054] vsize: 63008
Current children cumulated CPU time (s) 858.86
Current children cumulated vsize (Kb) 65132

[startup+870.062 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 31054
Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31050/statm): 531 226 485 147 0 384 0
[pid=31050] vsize: 2124
Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 15266 0 0 0 86777 103 0 0 25 0 1 0 1846669929 66162688 15102 4294967295 134512640 135094434 3221224432 3221223088 134558178 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31054/statm): 16153 15102 145 145 0 16008 0
[pid=31054] vsize: 64612
Current children cumulated CPU time (s) 868.81
Current children cumulated vsize (Kb) 66736

[startup+880.063 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 31054
Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31050/statm): 531 226 485 147 0 384 0
[pid=31050] vsize: 2124
Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 15354 0 0 0 87775 104 0 0 25 0 1 0 1846669929 66519040 15190 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31054/statm): 16240 15190 145 145 0 16095 0
[pid=31054] vsize: 64960
Current children cumulated CPU time (s) 878.8
Current children cumulated vsize (Kb) 67084

[startup+890.063 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 31054
Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31050/statm): 531 226 485 147 0 384 0
[pid=31050] vsize: 2124
Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 15354 0 0 0 88775 104 0 0 25 0 1 0 1846669929 66519040 15190 4294967295 134512640 135094434 3221224432 3221223104 134556302 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31054/statm): 16240 15190 145 145 0 16095 0
[pid=31054] vsize: 64960
Current children cumulated CPU time (s) 888.8
Current children cumulated vsize (Kb) 67084

[startup+900.064 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 31054
Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31050/statm): 531 226 485 147 0 384 0
[pid=31050] vsize: 2124
Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 15354 0 0 0 89775 104 0 0 25 0 1 0 1846669929 66519040 15190 4294967295 134512640 135094434 3221224432 3221223088 134558426 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31054/statm): 16240 15190 145 145 0 16095 0
[pid=31054] vsize: 64960
Current children cumulated CPU time (s) 898.8
Current children cumulated vsize (Kb) 67084

[startup+910.064 s]
Raw data (loadavg): 0.99 0.97 0.98 3/57 31054
Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31050/statm): 531 226 485 147 0 384 0
[pid=31050] vsize: 2124
Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 15355 0 0 0 90775 104 0 0 25 0 1 0 1846669929 66519040 15191 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31054/statm): 16240 15191 145 145 0 16095 0
[pid=31054] vsize: 64960
Current children cumulated CPU time (s) 908.8
Current children cumulated vsize (Kb) 67084

[startup+920.065 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 31054
Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31050/statm): 531 226 485 147 0 384 0
[pid=31050] vsize: 2124
Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 15355 0 0 0 91776 104 0 0 25 0 1 0 1846669929 66519040 15191 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31054/statm): 16240 15191 145 145 0 16095 0
[pid=31054] vsize: 64960
Current children cumulated CPU time (s) 918.81
Current children cumulated vsize (Kb) 67084

[startup+930.067 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 31054
Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31050/statm): 531 226 485 147 0 384 0
[pid=31050] vsize: 2124
Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 15355 0 0 0 92776 104 0 0 25 0 1 0 1846669929 66519040 15191 4294967295 134512640 135094434 3221224432 3221223088 134557860 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31054/statm): 16240 15191 145 145 0 16095 0
[pid=31054] vsize: 64960
Current children cumulated CPU time (s) 928.81
Current children cumulated vsize (Kb) 67084

[startup+940.067 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 31054
Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31050/statm): 531 226 485 147 0 384 0
[pid=31050] vsize: 2124
Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 15355 0 0 0 93776 104 0 0 25 0 1 0 1846669929 66519040 15191 4294967295 134512640 135094434 3221224432 3221223088 134557818 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31054/statm): 16240 15191 145 145 0 16095 0
[pid=31054] vsize: 64960
Current children cumulated CPU time (s) 938.81
Current children cumulated vsize (Kb) 67084

[startup+950.068 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 31054
Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31050/statm): 531 226 485 147 0 384 0
[pid=31050] vsize: 2124
Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 15355 0 0 0 94776 104 0 0 25 0 1 0 1846669929 66519040 15191 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31054/statm): 16240 15191 145 145 0 16095 0
[pid=31054] vsize: 64960
Current children cumulated CPU time (s) 948.81
Current children cumulated vsize (Kb) 67084

[startup+960.068 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 31054
Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31050/statm): 531 226 485 147 0 384 0
[pid=31050] vsize: 2124
Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 15355 0 0 0 95776 105 0 0 25 0 1 0 1846669929 66519040 15191 4294967295 134512640 135094434 3221224432 3221223044 134563083 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31054/statm): 16240 15191 145 145 0 16095 0
[pid=31054] vsize: 64960
Current children cumulated CPU time (s) 958.82
Current children cumulated vsize (Kb) 67084

[startup+970.068 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 31054
Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31050/statm): 531 226 485 147 0 384 0
[pid=31050] vsize: 2124
Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 15365 0 0 0 96777 105 0 0 25 0 1 0 1846669929 66584576 15201 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31054/statm): 16256 15201 145 145 0 16111 0
[pid=31054] vsize: 65024
Current children cumulated CPU time (s) 968.83
Current children cumulated vsize (Kb) 67148

[startup+980.069 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 31054
Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31050/statm): 531 226 485 147 0 384 0
[pid=31050] vsize: 2124
Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 15370 0 0 0 97777 105 0 0 25 0 1 0 1846669929 66613248 15206 4294967295 134512640 135094434 3221224432 3221223088 134558235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31054/statm): 16263 15206 145 145 0 16118 0
[pid=31054] vsize: 65052
Current children cumulated CPU time (s) 978.83
Current children cumulated vsize (Kb) 67176

[startup+990.069 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 31054
Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31050/statm): 531 226 485 147 0 384 0
[pid=31050] vsize: 2124
Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 15377 0 0 0 98777 105 0 0 25 0 1 0 1846669929 66646016 15213 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31054/statm): 16271 15213 145 145 0 16126 0
[pid=31054] vsize: 65084
Current children cumulated CPU time (s) 988.83
Current children cumulated vsize (Kb) 67208

[startup+1000.07 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 31054
Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31050/statm): 531 226 485 147 0 384 0
[pid=31050] vsize: 2124
Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 15377 0 0 0 99777 105 0 0 25 0 1 0 1846669929 66646016 15213 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31054/statm): 16271 15213 145 145 0 16126 0
[pid=31054] vsize: 65084
Current children cumulated CPU time (s) 998.83
Current children cumulated vsize (Kb) 67208

[startup+1010.07 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 31054
Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31050/statm): 531 226 485 147 0 384 0
[pid=31050] vsize: 2124
Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 15379 0 0 0 100778 105 0 0 25 0 1 0 1846669929 66646016 15215 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31054/statm): 16271 15215 145 145 0 16126 0
[pid=31054] vsize: 65084
Current children cumulated CPU time (s) 1008.84
Current children cumulated vsize (Kb) 67208

[startup+1020.07 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 31054
Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31050/statm): 531 226 485 147 0 384 0
[pid=31050] vsize: 2124
Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 15379 0 0 0 101778 105 0 0 25 0 1 0 1846669929 66646016 15215 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31054/statm): 16271 15215 145 145 0 16126 0
[pid=31054] vsize: 65084
Current children cumulated CPU time (s) 1018.84
Current children cumulated vsize (Kb) 67208

[startup+1030.07 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 31054
Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31050/statm): 531 226 485 147 0 384 0
[pid=31050] vsize: 2124
Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 15379 0 0 0 102778 105 0 0 25 0 1 0 1846669929 66646016 15215 4294967295 134512640 135094434 3221224432 3221223088 134558153 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31054/statm): 16271 15215 145 145 0 16126 0
[pid=31054] vsize: 65084
Current children cumulated CPU time (s) 1028.84
Current children cumulated vsize (Kb) 67208

[startup+1040.07 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 31054
Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31050/statm): 531 226 485 147 0 384 0
[pid=31050] vsize: 2124
Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 15379 0 0 0 103778 105 0 0 25 0 1 0 1846669929 66646016 15215 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31054/statm): 16271 15215 145 145 0 16126 0
[pid=31054] vsize: 65084
Current children cumulated CPU time (s) 1038.84
Current children cumulated vsize (Kb) 67208

[startup+1050.07 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 31054
Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31050/statm): 531 226 485 147 0 384 0
[pid=31050] vsize: 2124
Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 15379 0 0 0 104778 105 0 0 25 0 1 0 1846669929 66646016 15215 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31054/statm): 16271 15215 145 145 0 16126 0
[pid=31054] vsize: 65084
Current children cumulated CPU time (s) 1048.84
Current children cumulated vsize (Kb) 67208

[startup+1060.07 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 31054
Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31050/statm): 531 226 485 147 0 384 0
[pid=31050] vsize: 2124
Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 15379 0 0 0 105779 105 0 0 25 0 1 0 1846669929 66646016 15215 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31054/statm): 16271 15215 145 145 0 16126 0
[pid=31054] vsize: 65084
Current children cumulated CPU time (s) 1058.85
Current children cumulated vsize (Kb) 67208

[startup+1070.07 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 31054
Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31050/statm): 531 226 485 147 0 384 0
[pid=31050] vsize: 2124
Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 15379 0 0 0 106779 105 0 0 25 0 1 0 1846669929 66646016 15215 4294967295 134512640 135094434 3221224432 3221223088 134557884 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31054/statm): 16271 15215 145 145 0 16126 0
[pid=31054] vsize: 65084
Current children cumulated CPU time (s) 1068.85
Current children cumulated vsize (Kb) 67208

[startup+1080.08 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 31054
Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31050/statm): 531 226 485 147 0 384 0
[pid=31050] vsize: 2124
Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 15379 0 0 0 107779 105 0 0 25 0 1 0 1846669929 66646016 15215 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31054/statm): 16271 15215 145 145 0 16126 0
[pid=31054] vsize: 65084
Current children cumulated CPU time (s) 1078.85
Current children cumulated vsize (Kb) 67208

[startup+1090.08 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 31054
Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31050/statm): 531 226 485 147 0 384 0
[pid=31050] vsize: 2124
Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 15379 0 0 0 108779 105 0 0 25 0 1 0 1846669929 66646016 15215 4294967295 134512640 135094434 3221224432 3221223088 134558169 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31054/statm): 16271 15215 145 145 0 16126 0
[pid=31054] vsize: 65084
Current children cumulated CPU time (s) 1088.85
Current children cumulated vsize (Kb) 67208

[startup+1100.08 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 31054
Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31050/statm): 531 226 485 147 0 384 0
[pid=31050] vsize: 2124
Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 15381 0 0 0 109780 105 0 0 25 0 1 0 1846669929 66646016 15217 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31054/statm): 16271 15217 145 145 0 16126 0
[pid=31054] vsize: 65084
Current children cumulated CPU time (s) 1098.86
Current children cumulated vsize (Kb) 67208

[startup+1110.08 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 31054
Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31050/statm): 531 226 485 147 0 384 0
[pid=31050] vsize: 2124
Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 15381 0 0 0 110780 105 0 0 25 0 1 0 1846669929 66646016 15217 4294967295 134512640 135094434 3221224432 3221223088 134558178 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31054/statm): 16271 15217 145 145 0 16126 0
[pid=31054] vsize: 65084
Current children cumulated CPU time (s) 1108.86
Current children cumulated vsize (Kb) 67208

[startup+1120.08 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 31054
Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31050/statm): 531 226 485 147 0 384 0
[pid=31050] vsize: 2124
Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 15381 0 0 0 111780 105 0 0 25 0 1 0 1846669929 66646016 15217 4294967295 134512640 135094434 3221224432 3221223120 134554667 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31054/statm): 16271 15217 145 145 0 16126 0
[pid=31054] vsize: 65084
Current children cumulated CPU time (s) 1118.86
Current children cumulated vsize (Kb) 67208

[startup+1130.08 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 31054
Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31050/statm): 531 226 485 147 0 384 0
[pid=31050] vsize: 2124
Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 15381 0 0 0 112780 105 0 0 25 0 1 0 1846669929 66646016 15217 4294967295 134512640 135094434 3221224432 3221223088 134558420 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31054/statm): 16271 15217 145 145 0 16126 0
[pid=31054] vsize: 65084
Current children cumulated CPU time (s) 1128.86
Current children cumulated vsize (Kb) 67208

[startup+1140.08 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 31054
Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31050/statm): 531 226 485 147 0 384 0
[pid=31050] vsize: 2124
Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 15381 0 0 0 113780 105 0 0 25 0 1 0 1846669929 66646016 15217 4294967295 134512640 135094434 3221224432 3221223088 134558221 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31054/statm): 16271 15217 145 145 0 16126 0
[pid=31054] vsize: 65084
Current children cumulated CPU time (s) 1138.86
Current children cumulated vsize (Kb) 67208

[startup+1150.08 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 31054
Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31050/statm): 531 226 485 147 0 384 0
[pid=31050] vsize: 2124
Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 15381 0 0 0 114781 105 0 0 25 0 1 0 1846669929 66646016 15217 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31054/statm): 16271 15217 145 145 0 16126 0
[pid=31054] vsize: 65084
Current children cumulated CPU time (s) 1148.87
Current children cumulated vsize (Kb) 67208

[startup+1160.08 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 31054
Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31050/statm): 531 226 485 147 0 384 0
[pid=31050] vsize: 2124
Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 15392 0 0 0 115781 105 0 0 25 0 1 0 1846669929 66711552 15228 4294967295 134512640 135094434 3221224432 3221223088 134558238 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31054/statm): 16287 15228 145 145 0 16142 0
[pid=31054] vsize: 65148
Current children cumulated CPU time (s) 1158.87
Current children cumulated vsize (Kb) 67272

[startup+1170.08 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 31054
Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31050/statm): 531 226 485 147 0 384 0
[pid=31050] vsize: 2124
Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 15392 0 0 0 116781 105 0 0 25 0 1 0 1846669929 66711552 15228 4294967295 134512640 135094434 3221224432 3221223088 134558169 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31054/statm): 16287 15228 145 145 0 16142 0
[pid=31054] vsize: 65148
Current children cumulated CPU time (s) 1168.87
Current children cumulated vsize (Kb) 67272

[startup+1180.08 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 31054
Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31050/statm): 531 226 485 147 0 384 0
[pid=31050] vsize: 2124
Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 15392 0 0 0 117781 105 0 0 25 0 1 0 1846669929 66711552 15228 4294967295 134512640 135094434 3221224432 3221223088 134558126 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31054/statm): 16287 15228 145 145 0 16142 0
[pid=31054] vsize: 65148
Current children cumulated CPU time (s) 1178.87
Current children cumulated vsize (Kb) 67272

[startup+1190.08 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 31054
Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31050/statm): 531 226 485 147 0 384 0
[pid=31050] vsize: 2124
Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 15392 0 0 0 118781 106 0 0 25 0 1 0 1846669929 66711552 15228 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31054/statm): 16287 15228 145 145 0 16142 0
[pid=31054] vsize: 65148
Current children cumulated CPU time (s) 1188.88
Current children cumulated vsize (Kb) 67272

[startup+1200.08 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 31054
Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31050/statm): 531 226 485 147 0 384 0
[pid=31050] vsize: 2124
Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 15392 0 0 0 119781 106 0 0 25 0 1 0 1846669929 66711552 15228 4294967295 134512640 135094434 3221224432 3221223024 134557219 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31054/statm): 16287 15228 145 145 0 16142 0
[pid=31054] vsize: 65148
Current children cumulated CPU time (s) 1198.88
Current children cumulated vsize (Kb) 67272

[startup+1210.08 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 31054
Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31050/statm): 531 226 485 147 0 384 0
[pid=31050] vsize: 2124
Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 15404 0 0 0 120781 106 0 0 25 0 1 0 1846669929 66777088 15240 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31054/statm): 16303 15240 145 145 0 16158 0
[pid=31054] vsize: 65212
Current children cumulated CPU time (s) 1208.88
Current children cumulated vsize (Kb) 67336



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.09 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 31054
Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31050/statm): 531 226 485 147 0 384 0
[pid=31050] vsize: 2124
Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 15404 0 0 0 120781 106 0 0 25 0 1 0 1846669929 66777088 15240 4294967295 134512640 135094434 3221224432 3221223056 134557669 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31054/statm): 16303 15240 145 145 0 16158 0
[pid=31054] vsize: 65212
Current children cumulated CPU time (s) 1208.88
Current children cumulated vsize (Kb) 67336

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

Child status: 0
Real time (s): 1210.12
CPU time (s): 1208.91
CPU user time (s): 1207.82
CPU system time (s): 1.09583
CPU usage (%): 99.9003
Max. virtual memory (cumulated for all children) (Kb): 67336

Verifier Data

ERROR: no interpretation found !