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/miplib3/normalized-mps-v2-20-10-vpm1.opb
MD5SUMeb50800dc2fc522dd2f29a347fbab1da
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 benchmark1250.11
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 4551

Launcher Data

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.169
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 899.07

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        875272 kB
Buffers:         33856 kB
Cached:          93028 kB
SwapCached:        752 kB
Active:          69352 kB
Inactive:        60136 kB
HighTotal:      131008 kB
HighFree:        42532 kB
LowTotal:       903652 kB
LowFree:        832740 kB
SwapTotal:     2097892 kB
SwapFree:      2096628 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5728 kB
Slab:            24360 kB
Committed_AS:    64168 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-09-19 18:36:45 (client local time) WITH STATUS 0 IN 1208.93 SECONDS
stats: 3013 7 1208.93 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/18391/stat): 18391 (minisat+_script) R 18390 18391 28974 0 -1 0 19 0 0 0 0 0 0 0 22 0 1 0 1851970754 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 0 0 0
Raw data (/proc/18391/statm): 174 3 169 147 0 27 0
[pid=18391] 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=18392
New process pid=18393
New process pid=18394
execve syscall for /bin/sed executable
One traced child (pid=18393) 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=18394) exited with status: 0
One traced child (pid=18392) exited with status: 0
New process pid=18395
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc27/normalized-mps-v2-20-10-vpm1.opb

[startup+10.0033 s]
Raw data (loadavg): 0.93 0.95 0.91 2/57 18395
Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18391/statm): 531 226 485 147 0 384 0
[pid=18391] vsize: 2124
Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 3829 0 0 0 965 15 0 0 25 0 1 0 1851970759 17580032 3665 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/18395/statm): 4292 3665 145 145 0 4147 0
[pid=18395] vsize: 17168
Current children cumulated CPU time (s) 9.82
Current children cumulated vsize (Kb) 19292

[startup+20.0051 s]
Raw data (loadavg): 0.94 0.96 0.91 2/57 18395
Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18391/statm): 531 226 485 147 0 384 0
[pid=18391] vsize: 2124
Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 4192 0 0 0 1958 19 0 0 25 0 1 0 1851970759 19103744 4028 4294967295 134512640 135094434 3221224432 3221223088 134558123 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/18395/statm): 4664 4028 145 145 0 4519 0
[pid=18395] vsize: 18656
Current children cumulated CPU time (s) 19.79
Current children cumulated vsize (Kb) 20780

[startup+30.007 s]
Raw data (loadavg): 0.95 0.96 0.91 2/57 18395
Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18391/statm): 531 226 485 147 0 384 0
[pid=18391] vsize: 2124
Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 4662 0 0 0 2950 22 0 0 25 0 1 0 1851970759 21094400 4498 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/18395/statm): 5150 4498 145 145 0 5005 0
[pid=18395] vsize: 20600
Current children cumulated CPU time (s) 29.74
Current children cumulated vsize (Kb) 22724

[startup+40.0078 s]
Raw data (loadavg): 0.95 0.96 0.91 2/57 18395
Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18391/statm): 531 226 485 147 0 384 0
[pid=18391] vsize: 2124
Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 5187 0 0 0 3940 27 0 0 25 0 1 0 1851970759 23183360 5023 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/18395/statm): 5660 5023 145 145 0 5515 0
[pid=18395] vsize: 22640
Current children cumulated CPU time (s) 39.69
Current children cumulated vsize (Kb) 24764

[startup+50.0096 s]
Raw data (loadavg): 0.96 0.96 0.91 2/57 18395
Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18391/statm): 531 226 485 147 0 384 0
[pid=18391] vsize: 2124
Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 5602 0 0 0 4931 31 0 0 25 0 1 0 1851970759 24838144 5438 4294967295 134512640 135094434 3221224432 3221223088 134558235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/18395/statm): 6064 5438 145 145 0 5919 0
[pid=18395] vsize: 24256
Current children cumulated CPU time (s) 49.64
Current children cumulated vsize (Kb) 26380

[startup+60.0105 s]
Raw data (loadavg): 0.97 0.96 0.91 2/57 18395
Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18391/statm): 531 226 485 147 0 384 0
[pid=18391] vsize: 2124
Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 6077 0 0 0 5923 35 0 0 25 0 1 0 1851970759 27000832 5913 4294967295 134512640 135094434 3221224432 3221223088 134557920 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/18395/statm): 6592 5913 145 145 0 6447 0
[pid=18395] vsize: 26368
Current children cumulated CPU time (s) 59.6
Current children cumulated vsize (Kb) 28492

[startup+70.0123 s]
Raw data (loadavg): 0.97 0.96 0.91 2/57 18395
Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18391/statm): 531 226 485 147 0 384 0
[pid=18391] vsize: 2124
Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 6375 0 0 0 6917 38 0 0 25 0 1 0 1851970759 28205056 6211 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/18395/statm): 6886 6211 145 145 0 6741 0
[pid=18395] vsize: 27544
Current children cumulated CPU time (s) 69.57
Current children cumulated vsize (Kb) 29668

[startup+80.0141 s]
Raw data (loadavg): 0.98 0.96 0.91 2/57 18395
Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18391/statm): 531 226 485 147 0 384 0
[pid=18391] vsize: 2124
Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 6697 0 0 0 7912 41 0 0 25 0 1 0 1851970759 29523968 6533 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18395/statm): 7208 6533 145 145 0 7063 0
[pid=18395] vsize: 28832
Current children cumulated CPU time (s) 79.55
Current children cumulated vsize (Kb) 30956

[startup+90.0149 s]
Raw data (loadavg): 0.98 0.96 0.91 2/57 18395
Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18391/statm): 531 226 485 147 0 384 0
[pid=18391] vsize: 2124
Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 7021 0 0 0 8906 43 0 0 25 0 1 0 1851970759 30834688 6857 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18395/statm): 7528 6857 145 145 0 7383 0
[pid=18395] vsize: 30112
Current children cumulated CPU time (s) 89.51
Current children cumulated vsize (Kb) 32236

[startup+100.016 s]
Raw data (loadavg): 0.98 0.96 0.91 2/57 18395
Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18391/statm): 531 226 485 147 0 384 0
[pid=18391] vsize: 2124
Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 7309 0 0 0 9901 45 0 0 25 0 1 0 1851970759 31993856 7145 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18395/statm): 7811 7145 145 145 0 7666 0
[pid=18395] vsize: 31244
Current children cumulated CPU time (s) 99.48
Current children cumulated vsize (Kb) 33368

[startup+110.017 s]
Raw data (loadavg): 0.98 0.96 0.91 2/57 18395
Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18391/statm): 531 226 485 147 0 384 0
[pid=18391] vsize: 2124
Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 7551 0 0 0 10897 47 0 0 25 0 1 0 1851970759 32956416 7387 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18395/statm): 8046 7387 145 145 0 7901 0
[pid=18395] vsize: 32184
Current children cumulated CPU time (s) 109.46
Current children cumulated vsize (Kb) 34308

[startup+120.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 18395
Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18391/statm): 531 226 485 147 0 384 0
[pid=18391] vsize: 2124
Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 7783 0 0 0 11894 48 0 0 25 0 1 0 1851970759 33918976 7619 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18395/statm): 8281 7619 145 145 0 8136 0
[pid=18395] vsize: 33124
Current children cumulated CPU time (s) 119.44
Current children cumulated vsize (Kb) 35248

[startup+130.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 18395
Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18391/statm): 531 226 485 147 0 384 0
[pid=18391] vsize: 2124
Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 7965 0 0 0 12891 49 0 0 25 0 1 0 1851970759 34664448 7801 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18395/statm): 8463 7801 145 145 0 8318 0
[pid=18395] vsize: 33852
Current children cumulated CPU time (s) 129.42
Current children cumulated vsize (Kb) 35976

[startup+140.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 18395
Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18391/statm): 531 226 485 147 0 384 0
[pid=18391] vsize: 2124
Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 8140 0 0 0 13889 50 0 0 25 0 1 0 1851970759 35368960 7976 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18395/statm): 8635 7976 145 145 0 8490 0
[pid=18395] vsize: 34540
Current children cumulated CPU time (s) 139.41
Current children cumulated vsize (Kb) 36664

[startup+150.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 18395
Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18391/statm): 531 226 485 147 0 384 0
[pid=18391] vsize: 2124
Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 8304 0 0 0 14887 51 0 0 25 0 1 0 1851970759 36016128 8140 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18395/statm): 8793 8140 145 145 0 8648 0
[pid=18395] vsize: 35172
Current children cumulated CPU time (s) 149.4
Current children cumulated vsize (Kb) 37296

[startup+160.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 18395
Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18391/statm): 531 226 485 147 0 384 0
[pid=18391] vsize: 2124
Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 8549 0 0 0 15883 52 0 0 25 0 1 0 1851970759 37564416 8385 4294967295 134512640 135094434 3221224432 3221223044 134563043 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18395/statm): 9171 8385 145 145 0 9026 0
[pid=18395] vsize: 36684
Current children cumulated CPU time (s) 159.37
Current children cumulated vsize (Kb) 38808

[startup+170.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 18395
Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18391/statm): 531 226 485 147 0 384 0
[pid=18391] vsize: 2124
Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 8846 0 0 0 16878 55 0 0 25 0 1 0 1851970759 38756352 8682 4294967295 134512640 135094434 3221224432 3221223092 134553499 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18395/statm): 9462 8682 145 145 0 9317 0
[pid=18395] vsize: 37848
Current children cumulated CPU time (s) 169.35
Current children cumulated vsize (Kb) 39972

[startup+180.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 18395
Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18391/statm): 531 226 485 147 0 384 0
[pid=18391] vsize: 2124
Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 9189 0 0 0 17871 57 0 0 25 0 1 0 1851970759 40148992 9025 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18395/statm): 9802 9025 145 145 0 9657 0
[pid=18395] vsize: 39208
Current children cumulated CPU time (s) 179.3
Current children cumulated vsize (Kb) 41332

[startup+190.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 18395
Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18391/statm): 531 226 485 147 0 384 0
[pid=18391] vsize: 2124
Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 9409 0 0 0 18868 58 0 0 25 0 1 0 1851970759 41017344 9245 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18395/statm): 10014 9245 145 145 0 9869 0
[pid=18395] vsize: 40056
Current children cumulated CPU time (s) 189.28
Current children cumulated vsize (Kb) 42180

[startup+200.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 18395
Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18391/statm): 531 226 485 147 0 384 0
[pid=18391] vsize: 2124
Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 9563 0 0 0 19866 59 0 0 25 0 1 0 1851970759 41635840 9399 4294967295 134512640 135094434 3221224432 3221223088 134557884 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18395/statm): 10165 9399 145 145 0 10020 0
[pid=18395] vsize: 40660
Current children cumulated CPU time (s) 199.27
Current children cumulated vsize (Kb) 42784

[startup+210.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 18395
Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18391/statm): 531 226 485 147 0 384 0
[pid=18391] vsize: 2124
Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 9722 0 0 0 20864 60 0 0 25 0 1 0 1851970759 42266624 9558 4294967295 134512640 135094434 3221224432 3221223088 134557937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18395/statm): 10319 9558 145 145 0 10174 0
[pid=18395] vsize: 41276
Current children cumulated CPU time (s) 209.26
Current children cumulated vsize (Kb) 43400

[startup+220.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 18395
Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18391/statm): 531 226 485 147 0 384 0
[pid=18391] vsize: 2124
Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 9875 0 0 0 21862 60 0 0 25 0 1 0 1851970759 42889216 9711 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18395/statm): 10471 9711 145 145 0 10326 0
[pid=18395] vsize: 41884
Current children cumulated CPU time (s) 219.24
Current children cumulated vsize (Kb) 44008

[startup+230.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 18395
Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18391/statm): 531 226 485 147 0 384 0
[pid=18391] vsize: 2124
Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 10031 0 0 0 22860 61 0 0 25 0 1 0 1851970759 43532288 9867 4294967295 134512640 135094434 3221224432 3221223088 134558225 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18395/statm): 10628 9867 145 145 0 10483 0
[pid=18395] vsize: 42512
Current children cumulated CPU time (s) 229.23
Current children cumulated vsize (Kb) 44636

[startup+240.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 18395
Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18391/statm): 531 226 485 147 0 384 0
[pid=18391] vsize: 2124
Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 10166 0 0 0 23859 62 0 0 25 0 1 0 1851970759 44068864 10002 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18395/statm): 10759 10002 145 145 0 10614 0
[pid=18395] vsize: 43036
Current children cumulated CPU time (s) 239.23
Current children cumulated vsize (Kb) 45160

[startup+250.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 18395
Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18391/statm): 531 226 485 147 0 384 0
[pid=18391] vsize: 2124
Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 10300 0 0 0 24857 63 0 0 25 0 1 0 1851970759 44634112 10136 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18395/statm): 10897 10136 145 145 0 10752 0
[pid=18395] vsize: 43588
Current children cumulated CPU time (s) 249.22
Current children cumulated vsize (Kb) 45712

[startup+260.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 18395
Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18391/statm): 531 226 485 147 0 384 0
[pid=18391] vsize: 2124
Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 10412 0 0 0 25854 64 0 0 25 0 1 0 1851970759 45092864 10248 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18395/statm): 11009 10248 145 145 0 10864 0
[pid=18395] vsize: 44036
Current children cumulated CPU time (s) 259.2
Current children cumulated vsize (Kb) 46160

[startup+270.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 18395
Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18391/statm): 531 226 485 147 0 384 0
[pid=18391] vsize: 2124
Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 10527 0 0 0 26852 65 0 0 25 0 1 0 1851970759 45551616 10363 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18395/statm): 11121 10363 145 145 0 10976 0
[pid=18395] vsize: 44484
Current children cumulated CPU time (s) 269.19
Current children cumulated vsize (Kb) 46608

[startup+280.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 18395
Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18391/statm): 531 226 485 147 0 384 0
[pid=18391] vsize: 2124
Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 10650 0 0 0 27850 67 0 0 25 0 1 0 1851970759 46067712 10486 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18395/statm): 11247 10486 145 145 0 11102 0
[pid=18395] vsize: 44988
Current children cumulated CPU time (s) 279.19
Current children cumulated vsize (Kb) 47112

[startup+290.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 18395
Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18391/statm): 531 226 485 147 0 384 0
[pid=18391] vsize: 2124
Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 10768 0 0 0 28848 67 0 0 25 0 1 0 1851970759 46563328 10604 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18395/statm): 11368 10604 145 145 0 11223 0
[pid=18395] vsize: 45472
Current children cumulated CPU time (s) 289.17
Current children cumulated vsize (Kb) 47596

[startup+300.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 18395
Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18391/statm): 531 226 485 147 0 384 0
[pid=18391] vsize: 2124
Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 10893 0 0 0 29847 68 0 0 25 0 1 0 1851970759 47054848 10729 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18395/statm): 11488 10729 145 145 0 11343 0
[pid=18395] vsize: 45952
Current children cumulated CPU time (s) 299.17
Current children cumulated vsize (Kb) 48076

[startup+310.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 18395
Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18391/statm): 531 226 485 147 0 384 0
[pid=18391] vsize: 2124
Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 11007 0 0 0 30845 69 0 0 25 0 1 0 1851970759 47554560 10843 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18395/statm): 11610 10843 145 145 0 11465 0
[pid=18395] vsize: 46440
Current children cumulated CPU time (s) 309.16
Current children cumulated vsize (Kb) 48564

[startup+320.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 18395
Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18391/statm): 531 226 485 147 0 384 0
[pid=18391] vsize: 2124
Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 11104 0 0 0 31844 69 0 0 25 0 1 0 1851970759 47927296 10940 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18395/statm): 11701 10940 145 145 0 11556 0
[pid=18395] vsize: 46804
Current children cumulated CPU time (s) 319.15
Current children cumulated vsize (Kb) 48928

[startup+330.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 18395
Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18391/statm): 531 226 485 147 0 384 0
[pid=18391] vsize: 2124
Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 11202 0 0 0 32842 70 0 0 25 0 1 0 1851970759 48312320 11038 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18395/statm): 11795 11038 145 145 0 11650 0
[pid=18395] vsize: 47180
Current children cumulated CPU time (s) 329.14
Current children cumulated vsize (Kb) 49304

[startup+340.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 18395
Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18391/statm): 531 226 485 147 0 384 0
[pid=18391] vsize: 2124
Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 11436 0 0 0 33838 71 0 0 25 0 1 0 1851970759 49295360 11272 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/18395/statm): 12035 11272 145 145 0 11890 0
[pid=18395] vsize: 48140
Current children cumulated CPU time (s) 339.11
Current children cumulated vsize (Kb) 50264

[startup+350.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 18395
Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18391/statm): 531 226 485 147 0 384 0
[pid=18391] vsize: 2124
Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 11671 0 0 0 34835 73 0 0 25 0 1 0 1851970759 50323456 11507 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/18395/statm): 12286 11507 145 145 0 12141 0
[pid=18395] vsize: 49144
Current children cumulated CPU time (s) 349.1
Current children cumulated vsize (Kb) 51268

[startup+360.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 18395
Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18391/statm): 531 226 485 147 0 384 0
[pid=18391] vsize: 2124
Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 11885 0 0 0 35830 74 0 0 25 0 1 0 1851970759 51216384 11721 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/18395/statm): 12504 11721 145 145 0 12359 0
[pid=18395] vsize: 50016
Current children cumulated CPU time (s) 359.06
Current children cumulated vsize (Kb) 52140

[startup+370.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 18395
Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18391/statm): 531 226 485 147 0 384 0
[pid=18391] vsize: 2124
Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 12085 0 0 0 36826 76 0 0 25 0 1 0 1851970759 52035584 11921 4294967295 134512640 135094434 3221224432 3221223088 134557875 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/18395/statm): 12704 11921 145 145 0 12559 0
[pid=18395] vsize: 50816
Current children cumulated CPU time (s) 369.04
Current children cumulated vsize (Kb) 52940

[startup+380.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 18395
Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18391/statm): 531 226 485 147 0 384 0
[pid=18391] vsize: 2124
Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 12280 0 0 0 37821 78 0 0 25 0 1 0 1851970759 52854784 12116 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/18395/statm): 12904 12116 145 145 0 12759 0
[pid=18395] vsize: 51616
Current children cumulated CPU time (s) 379.01
Current children cumulated vsize (Kb) 53740

[startup+390.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 18395
Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18391/statm): 531 226 485 147 0 384 0
[pid=18391] vsize: 2124
Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 12567 0 0 0 38816 81 0 0 25 0 1 0 1851970759 54001664 12403 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/18395/statm): 13184 12403 145 145 0 13039 0
[pid=18395] vsize: 52736
Current children cumulated CPU time (s) 388.99
Current children cumulated vsize (Kb) 54860

[startup+400.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 18395
Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18391/statm): 531 226 485 147 0 384 0
[pid=18391] vsize: 2124
Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 12772 0 0 0 39813 82 0 0 25 0 1 0 1851970759 54816768 12608 4294967295 134512640 135094434 3221224432 3221223088 134557972 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/18395/statm): 13383 12608 145 145 0 13238 0
[pid=18395] vsize: 53532
Current children cumulated CPU time (s) 398.97
Current children cumulated vsize (Kb) 55656

[startup+410.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 18395
Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18391/statm): 531 226 485 147 0 384 0
[pid=18391] vsize: 2124
Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 12806 0 0 0 40813 83 0 0 25 0 1 0 1851970759 54956032 12642 4294967295 134512640 135094434 3221224432 3221223088 134557900 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18395/statm): 13417 12642 145 145 0 13272 0
[pid=18395] vsize: 53668
Current children cumulated CPU time (s) 408.98
Current children cumulated vsize (Kb) 55792

[startup+420.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 18395
Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18391/statm): 531 226 485 147 0 384 0
[pid=18391] vsize: 2124
Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 12806 0 0 0 41813 83 0 0 25 0 1 0 1851970759 54956032 12642 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18395/statm): 13417 12642 145 145 0 13272 0
[pid=18395] vsize: 53668
Current children cumulated CPU time (s) 418.98
Current children cumulated vsize (Kb) 55792

[startup+430.051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 18395
Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18391/statm): 531 226 485 147 0 384 0
[pid=18391] vsize: 2124
Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 12806 0 0 0 42813 83 0 0 25 0 1 0 1851970759 54956032 12642 4294967295 134512640 135094434 3221224432 3221223088 134558235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18395/statm): 13417 12642 145 145 0 13272 0
[pid=18395] vsize: 53668
Current children cumulated CPU time (s) 428.98
Current children cumulated vsize (Kb) 55792

[startup+440.052 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 18395
Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18391/statm): 531 226 485 147 0 384 0
[pid=18391] vsize: 2124
Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 12807 0 0 0 43814 83 0 0 25 0 1 0 1851970759 54956032 12643 4294967295 134512640 135094434 3221224432 3221223088 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18395/statm): 13417 12643 145 145 0 13272 0
[pid=18395] vsize: 53668
Current children cumulated CPU time (s) 438.99
Current children cumulated vsize (Kb) 55792

[startup+450.053 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 18395
Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18391/statm): 531 226 485 147 0 384 0
[pid=18391] vsize: 2124
Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 12807 0 0 0 44814 83 0 0 25 0 1 0 1851970759 54956032 12643 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18395/statm): 13417 12643 145 145 0 13272 0
[pid=18395] vsize: 53668
Current children cumulated CPU time (s) 448.99
Current children cumulated vsize (Kb) 55792

[startup+460.053 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 18395
Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18391/statm): 531 226 485 147 0 384 0
[pid=18391] vsize: 2124
Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 12808 0 0 0 45814 83 0 0 25 0 1 0 1851970759 54956032 12644 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18395/statm): 13417 12644 145 145 0 13272 0
[pid=18395] vsize: 53668
Current children cumulated CPU time (s) 458.99
Current children cumulated vsize (Kb) 55792

[startup+470.054 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 18395
Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18391/statm): 531 226 485 147 0 384 0
[pid=18391] vsize: 2124
Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 12808 0 0 0 46814 83 0 0 25 0 1 0 1851970759 54956032 12644 4294967295 134512640 135094434 3221224432 3221223088 134557917 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18395/statm): 13417 12644 145 145 0 13272 0
[pid=18395] vsize: 53668
Current children cumulated CPU time (s) 468.99
Current children cumulated vsize (Kb) 55792

[startup+480.055 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 18395
Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18391/statm): 531 226 485 147 0 384 0
[pid=18391] vsize: 2124
Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 12808 0 0 0 47814 84 0 0 25 0 1 0 1851970759 54956032 12644 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/18395/statm): 13417 12644 145 145 0 13272 0
[pid=18395] vsize: 53668
Current children cumulated CPU time (s) 479
Current children cumulated vsize (Kb) 55792

[startup+490.056 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 18395
Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18391/statm): 531 226 485 147 0 384 0
[pid=18391] vsize: 2124
Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 12808 0 0 0 48813 84 0 0 25 0 1 0 1851970759 54956032 12644 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18395/statm): 13417 12644 145 145 0 13272 0
[pid=18395] vsize: 53668
Current children cumulated CPU time (s) 488.99
Current children cumulated vsize (Kb) 55792

[startup+500.058 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 18395
Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18391/statm): 531 226 485 147 0 384 0
[pid=18391] vsize: 2124
Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 12808 0 0 0 49814 84 0 0 25 0 1 0 1851970759 54956032 12644 4294967295 134512640 135094434 3221224432 3221223088 134558221 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18395/statm): 13417 12644 145 145 0 13272 0
[pid=18395] vsize: 53668
Current children cumulated CPU time (s) 499
Current children cumulated vsize (Kb) 55792

[startup+510.059 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 18395
Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18391/statm): 531 226 485 147 0 384 0
[pid=18391] vsize: 2124
Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 12808 0 0 0 50814 84 0 0 25 0 1 0 1851970759 54956032 12644 4294967295 134512640 135094434 3221224432 3221223088 134558420 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18395/statm): 13417 12644 145 145 0 13272 0
[pid=18395] vsize: 53668
Current children cumulated CPU time (s) 509
Current children cumulated vsize (Kb) 55792

[startup+520.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 18395
Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18391/statm): 531 226 485 147 0 384 0
[pid=18391] vsize: 2124
Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 12808 0 0 0 51814 84 0 0 25 0 1 0 1851970759 54956032 12644 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18395/statm): 13417 12644 145 145 0 13272 0
[pid=18395] vsize: 53668
Current children cumulated CPU time (s) 519
Current children cumulated vsize (Kb) 55792

[startup+530.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 18395
Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18391/statm): 531 226 485 147 0 384 0
[pid=18391] vsize: 2124
Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 12808 0 0 0 52814 84 0 0 25 0 1 0 1851970759 54956032 12644 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18395/statm): 13417 12644 145 145 0 13272 0
[pid=18395] vsize: 53668
Current children cumulated CPU time (s) 529
Current children cumulated vsize (Kb) 55792

[startup+540.061 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 18395
Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18391/statm): 531 226 485 147 0 384 0
[pid=18391] vsize: 2124
Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 12810 0 0 0 53815 84 0 0 25 0 1 0 1851970759 54956032 12646 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18395/statm): 13417 12646 145 145 0 13272 0
[pid=18395] vsize: 53668
Current children cumulated CPU time (s) 539.01
Current children cumulated vsize (Kb) 55792

[startup+550.063 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 18395
Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18391/statm): 531 226 485 147 0 384 0
[pid=18391] vsize: 2124
Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 12810 0 0 0 54815 84 0 0 25 0 1 0 1851970759 54956032 12646 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18395/statm): 13417 12646 145 145 0 13272 0
[pid=18395] vsize: 53668
Current children cumulated CPU time (s) 549.01
Current children cumulated vsize (Kb) 55792

[startup+560.064 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 18395
Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18391/statm): 531 226 485 147 0 384 0
[pid=18391] vsize: 2124
Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 12810 0 0 0 55815 84 0 0 25 0 1 0 1851970759 54956032 12646 4294967295 134512640 135094434 3221224432 3221223056 134557737 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18395/statm): 13417 12646 145 145 0 13272 0
[pid=18395] vsize: 53668
Current children cumulated CPU time (s) 559.01
Current children cumulated vsize (Kb) 55792

[startup+570.065 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 18395
Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18391/statm): 531 226 485 147 0 384 0
[pid=18391] vsize: 2124
Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 12810 0 0 0 56815 84 0 0 25 0 1 0 1851970759 54956032 12646 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18395/statm): 13417 12646 145 145 0 13272 0
[pid=18395] vsize: 53668
Current children cumulated CPU time (s) 569.01
Current children cumulated vsize (Kb) 55792

[startup+580.066 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 18395
Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18391/statm): 531 226 485 147 0 384 0
[pid=18391] vsize: 2124
Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 12810 0 0 0 57815 84 0 0 25 0 1 0 1851970759 54956032 12646 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18395/statm): 13417 12646 145 145 0 13272 0
[pid=18395] vsize: 53668
Current children cumulated CPU time (s) 579.01
Current children cumulated vsize (Kb) 55792

[startup+590.067 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 18395
Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18391/statm): 531 226 485 147 0 384 0
[pid=18391] vsize: 2124
Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 12811 0 0 0 58816 84 0 0 25 0 1 0 1851970759 54956032 12647 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18395/statm): 13417 12647 145 145 0 13272 0
[pid=18395] vsize: 53668
Current children cumulated CPU time (s) 589.02
Current children cumulated vsize (Kb) 55792

[startup+600.068 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 18395
Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18391/statm): 531 226 485 147 0 384 0
[pid=18391] vsize: 2124
Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 12811 0 0 0 59816 85 0 0 25 0 1 0 1851970759 54956032 12647 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18395/statm): 13417 12647 145 145 0 13272 0
[pid=18395] vsize: 53668
Current children cumulated CPU time (s) 599.03
Current children cumulated vsize (Kb) 55792

[startup+610.069 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 18395
Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18391/statm): 531 226 485 147 0 384 0
[pid=18391] vsize: 2124
Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 12811 0 0 0 60816 85 0 0 25 0 1 0 1851970759 54956032 12647 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18395/statm): 13417 12647 145 145 0 13272 0
[pid=18395] vsize: 53668
Current children cumulated CPU time (s) 609.03
Current children cumulated vsize (Kb) 55792

[startup+620.071 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 18395
Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18391/statm): 531 226 485 147 0 384 0
[pid=18391] vsize: 2124
Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 12811 0 0 0 61816 85 0 0 25 0 1 0 1851970759 54956032 12647 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18395/statm): 13417 12647 145 145 0 13272 0
[pid=18395] vsize: 53668
Current children cumulated CPU time (s) 619.03
Current children cumulated vsize (Kb) 55792

[startup+630.072 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 18395
Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18391/statm): 531 226 485 147 0 384 0
[pid=18391] vsize: 2124
Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 12812 0 0 0 62816 85 0 0 25 0 1 0 1851970759 54956032 12648 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18395/statm): 13417 12648 145 145 0 13272 0
[pid=18395] vsize: 53668
Current children cumulated CPU time (s) 629.03
Current children cumulated vsize (Kb) 55792

[startup+640.073 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 18395
Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18391/statm): 531 226 485 147 0 384 0
[pid=18391] vsize: 2124
Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 12812 0 0 0 63817 85 0 0 25 0 1 0 1851970759 54956032 12648 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18395/statm): 13417 12648 145 145 0 13272 0
[pid=18395] vsize: 53668
Current children cumulated CPU time (s) 639.04
Current children cumulated vsize (Kb) 55792

[startup+650.073 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 18395
Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18391/statm): 531 226 485 147 0 384 0
[pid=18391] vsize: 2124
Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 12812 0 0 0 64817 85 0 0 25 0 1 0 1851970759 54956032 12648 4294967295 134512640 135094434 3221224432 3221223088 134558178 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18395/statm): 13417 12648 145 145 0 13272 0
[pid=18395] vsize: 53668
Current children cumulated CPU time (s) 649.04
Current children cumulated vsize (Kb) 55792

[startup+660.074 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 18395
Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18391/statm): 531 226 485 147 0 384 0
[pid=18391] vsize: 2124
Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 12812 0 0 0 65817 85 0 0 25 0 1 0 1851970759 54956032 12648 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18395/statm): 13417 12648 145 145 0 13272 0
[pid=18395] vsize: 53668
Current children cumulated CPU time (s) 659.04
Current children cumulated vsize (Kb) 55792

[startup+670.076 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 18395
Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18391/statm): 531 226 485 147 0 384 0
[pid=18391] vsize: 2124
Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 12814 0 0 0 66817 85 0 0 25 0 1 0 1851970759 54956032 12650 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18395/statm): 13417 12650 145 145 0 13272 0
[pid=18395] vsize: 53668
Current children cumulated CPU time (s) 669.04
Current children cumulated vsize (Kb) 55792

[startup+680.077 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 18395
Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18391/statm): 531 226 485 147 0 384 0
[pid=18391] vsize: 2124
Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 12814 0 0 0 67817 85 0 0 25 0 1 0 1851970759 54956032 12650 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18395/statm): 13417 12650 145 145 0 13272 0
[pid=18395] vsize: 53668
Current children cumulated CPU time (s) 679.04
Current children cumulated vsize (Kb) 55792

[startup+690.078 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 18395
Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18391/statm): 531 226 485 147 0 384 0
[pid=18391] vsize: 2124
Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 12815 0 0 0 68818 85 0 0 25 0 1 0 1851970759 54956032 12651 4294967295 134512640 135094434 3221224432 3221223088 134558019 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18395/statm): 13417 12651 145 145 0 13272 0
[pid=18395] vsize: 53668
Current children cumulated CPU time (s) 689.05
Current children cumulated vsize (Kb) 55792

[startup+700.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 18395
Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18391/statm): 531 226 485 147 0 384 0
[pid=18391] vsize: 2124
Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 12840 0 0 0 69818 85 0 0 25 0 1 0 1851970759 55050240 12676 4294967295 134512640 135094434 3221224432 3221223088 134555980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18395/statm): 13440 12676 145 145 0 13295 0
[pid=18395] vsize: 53760
Current children cumulated CPU time (s) 699.05
Current children cumulated vsize (Kb) 55884

[startup+710.081 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 18395
Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18391/statm): 531 226 485 147 0 384 0
[pid=18391] vsize: 2124
Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 13002 0 0 0 70815 87 0 0 25 0 1 0 1851970759 55726080 12838 4294967295 134512640 135094434 3221224432 3221223088 134558123 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18395/statm): 13605 12838 145 145 0 13460 0
[pid=18395] vsize: 54420
Current children cumulated CPU time (s) 709.04
Current children cumulated vsize (Kb) 56544

[startup+720.081 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 18395
Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18391/statm): 531 226 485 147 0 384 0
[pid=18391] vsize: 2124
Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 13116 0 0 0 71813 88 0 0 25 0 1 0 1851970759 56193024 12952 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18395/statm): 13719 12952 145 145 0 13574 0
[pid=18395] vsize: 54876
Current children cumulated CPU time (s) 719.03
Current children cumulated vsize (Kb) 57000

[startup+730.083 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 18395
Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18391/statm): 531 226 485 147 0 384 0
[pid=18391] vsize: 2124
Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 13280 0 0 0 72810 89 0 0 25 0 1 0 1851970759 56918016 13116 4294967295 134512640 135094434 3221224432 3221223088 134557890 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18395/statm): 13896 13116 145 145 0 13751 0
[pid=18395] vsize: 55584
Current children cumulated CPU time (s) 729.01
Current children cumulated vsize (Kb) 57708

[startup+740.084 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 18395
Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18391/statm): 531 226 485 147 0 384 0
[pid=18391] vsize: 2124
Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 13410 0 0 0 73808 90 0 0 25 0 1 0 1851970759 57487360 13246 4294967295 134512640 135094434 3221224432 3221223104 134555599 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18395/statm): 14035 13246 145 145 0 13890 0
[pid=18395] vsize: 56140
Current children cumulated CPU time (s) 739
Current children cumulated vsize (Kb) 58264

[startup+750.085 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 18395
Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18391/statm): 531 226 485 147 0 384 0
[pid=18391] vsize: 2124
Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 13532 0 0 0 74807 90 0 0 25 0 1 0 1851970759 57987072 13368 4294967295 134512640 135094434 3221224432 3221223088 134558187 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18395/statm): 14157 13368 145 145 0 14012 0
[pid=18395] vsize: 56628
Current children cumulated CPU time (s) 748.99
Current children cumulated vsize (Kb) 58752

[startup+760.086 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 18395
Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18391/statm): 531 226 485 147 0 384 0
[pid=18391] vsize: 2124
Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 13717 0 0 0 75804 92 0 0 25 0 1 0 1851970759 58765312 13553 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18395/statm): 14347 13553 145 145 0 14202 0
[pid=18395] vsize: 57388
Current children cumulated CPU time (s) 758.98
Current children cumulated vsize (Kb) 59512

[startup+770.087 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 18395
Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18391/statm): 531 226 485 147 0 384 0
[pid=18391] vsize: 2124
Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 13850 0 0 0 76802 92 0 0 25 0 1 0 1851970759 59305984 13686 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18395/statm): 14479 13686 145 145 0 14334 0
[pid=18395] vsize: 57916
Current children cumulated CPU time (s) 768.96
Current children cumulated vsize (Kb) 60040

[startup+780.088 s]
Raw data (loadavg): 0.99 0.97 0.91 1/57 18395
Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18391/statm): 531 226 485 147 0 384 0
[pid=18391] vsize: 2124
Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) T 18391 18391 28974 0 -1 0 14129 0 0 0 77797 95 0 0 25 0 1 0 1851970759 60444672 13965 4294967295 134512640 135094434 3221224432 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/18395/statm): 14757 13965 145 145 0 14612 0
[pid=18395] vsize: 59028
Current children cumulated CPU time (s) 778.94
Current children cumulated vsize (Kb) 61152

[startup+790.089 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 18395
Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18391/statm): 531 226 485 147 0 384 0
[pid=18391] vsize: 2124
Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 14283 0 0 0 78795 95 0 0 25 0 1 0 1851970759 61095936 14119 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18395/statm): 14916 14119 145 145 0 14771 0
[pid=18395] vsize: 59664
Current children cumulated CPU time (s) 788.92
Current children cumulated vsize (Kb) 61788

[startup+800.091 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 18395
Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18391/statm): 531 226 485 147 0 384 0
[pid=18391] vsize: 2124
Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 14376 0 0 0 79794 96 0 0 25 0 1 0 1851970759 61489152 14212 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18395/statm): 15012 14212 145 145 0 14867 0
[pid=18395] vsize: 60048
Current children cumulated CPU time (s) 798.92
Current children cumulated vsize (Kb) 62172

[startup+810.092 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 18395
Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18391/statm): 531 226 485 147 0 384 0
[pid=18391] vsize: 2124
Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 14484 0 0 0 80792 97 0 0 25 0 1 0 1851970759 61919232 14320 4294967295 134512640 135094434 3221224432 3221223056 134557696 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18395/statm): 15117 14320 145 145 0 14972 0
[pid=18395] vsize: 60468
Current children cumulated CPU time (s) 808.91
Current children cumulated vsize (Kb) 62592

[startup+820.094 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 18395
Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18391/statm): 531 226 485 147 0 384 0
[pid=18391] vsize: 2124
Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 14584 0 0 0 81790 98 0 0 25 0 1 0 1851970759 62308352 14420 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18395/statm): 15212 14420 145 145 0 15067 0
[pid=18395] vsize: 60848
Current children cumulated CPU time (s) 818.9
Current children cumulated vsize (Kb) 62972

[startup+830.094 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 18395
Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18391/statm): 531 226 485 147 0 384 0
[pid=18391] vsize: 2124
Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 14672 0 0 0 82788 98 0 0 25 0 1 0 1851970759 62676992 14508 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18395/statm): 15302 14508 145 145 0 15157 0
[pid=18395] vsize: 61208
Current children cumulated CPU time (s) 828.88
Current children cumulated vsize (Kb) 63332

[startup+840.095 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 18395
Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18391/statm): 531 226 485 147 0 384 0
[pid=18391] vsize: 2124
Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 14769 0 0 0 83786 99 0 0 25 0 1 0 1851970759 63066112 14605 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18395/statm): 15397 14605 145 145 0 15252 0
[pid=18395] vsize: 61588
Current children cumulated CPU time (s) 838.87
Current children cumulated vsize (Kb) 63712

[startup+850.097 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 18395
Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18391/statm): 531 226 485 147 0 384 0
[pid=18391] vsize: 2124
Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 14901 0 0 0 84785 100 0 0 25 0 1 0 1851970759 64700416 14737 4294967295 134512640 135094434 3221224432 3221223088 134557860 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18395/statm): 15796 14737 145 145 0 15651 0
[pid=18395] vsize: 63184
Current children cumulated CPU time (s) 848.87
Current children cumulated vsize (Kb) 65308

[startup+860.098 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 18395
Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18391/statm): 531 226 485 147 0 384 0
[pid=18391] vsize: 2124
Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 15304 0 0 0 85778 103 0 0 25 0 1 0 1851970759 66314240 15140 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18395/statm): 16190 15140 145 145 0 16045 0
[pid=18395] vsize: 64760
Current children cumulated CPU time (s) 858.83
Current children cumulated vsize (Kb) 66884

[startup+870.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 18395
Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18391/statm): 531 226 485 147 0 384 0
[pid=18391] vsize: 2124
Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 15354 0 0 0 86778 104 0 0 25 0 1 0 1851970759 66519040 15190 4294967295 134512640 135094434 3221224432 3221223088 134558235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18395/statm): 16240 15190 145 145 0 16095 0
[pid=18395] vsize: 64960
Current children cumulated CPU time (s) 868.84
Current children cumulated vsize (Kb) 67084

[startup+880.101 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 18395
Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18391/statm): 531 226 485 147 0 384 0
[pid=18391] vsize: 2124
Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 15354 0 0 0 87778 104 0 0 25 0 1 0 1851970759 66519040 15190 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18395/statm): 16240 15190 145 145 0 16095 0
[pid=18395] vsize: 64960
Current children cumulated CPU time (s) 878.84
Current children cumulated vsize (Kb) 67084

[startup+890.101 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 18395
Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18391/statm): 531 226 485 147 0 384 0
[pid=18391] vsize: 2124
Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 15354 0 0 0 88779 104 0 0 25 0 1 0 1851970759 66519040 15190 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18395/statm): 16240 15190 145 145 0 16095 0
[pid=18395] vsize: 64960
Current children cumulated CPU time (s) 888.85
Current children cumulated vsize (Kb) 67084

[startup+900.102 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 18395
Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18391/statm): 531 226 485 147 0 384 0
[pid=18391] vsize: 2124
Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 15355 0 0 0 89779 104 0 0 25 0 1 0 1851970759 66519040 15191 4294967295 134512640 135094434 3221224432 3221223088 134558022 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18395/statm): 16240 15191 145 145 0 16095 0
[pid=18395] vsize: 64960
Current children cumulated CPU time (s) 898.85
Current children cumulated vsize (Kb) 67084

[startup+910.103 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 18395
Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18391/statm): 531 226 485 147 0 384 0
[pid=18391] vsize: 2124
Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 15355 0 0 0 90779 104 0 0 25 0 1 0 1851970759 66519040 15191 4294967295 134512640 135094434 3221224432 3221223056 134557633 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18395/statm): 16240 15191 145 145 0 16095 0
[pid=18395] vsize: 64960
Current children cumulated CPU time (s) 908.85
Current children cumulated vsize (Kb) 67084

[startup+920.104 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 18395
Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18391/statm): 531 226 485 147 0 384 0
[pid=18391] vsize: 2124
Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 15355 0 0 0 91779 104 0 0 25 0 1 0 1851970759 66519040 15191 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18395/statm): 16240 15191 145 145 0 16095 0
[pid=18395] vsize: 64960
Current children cumulated CPU time (s) 918.85
Current children cumulated vsize (Kb) 67084

[startup+930.105 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 18395
Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18391/statm): 531 226 485 147 0 384 0
[pid=18391] vsize: 2124
Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 15355 0 0 0 92779 104 0 0 25 0 1 0 1851970759 66519040 15191 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18395/statm): 16240 15191 145 145 0 16095 0
[pid=18395] vsize: 64960
Current children cumulated CPU time (s) 928.85
Current children cumulated vsize (Kb) 67084

[startup+940.106 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 18395
Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18391/statm): 531 226 485 147 0 384 0
[pid=18391] vsize: 2124
Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 15355 0 0 0 93779 104 0 0 25 0 1 0 1851970759 66519040 15191 4294967295 134512640 135094434 3221224432 3221223024 134551918 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18395/statm): 16240 15191 145 145 0 16095 0
[pid=18395] vsize: 64960
Current children cumulated CPU time (s) 938.85
Current children cumulated vsize (Kb) 67084

[startup+950.106 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 18395
Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18391/statm): 531 226 485 147 0 384 0
[pid=18391] vsize: 2124
Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 15365 0 0 0 94779 104 0 0 25 0 1 0 1851970759 66584576 15201 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18395/statm): 16256 15201 145 145 0 16111 0
[pid=18395] vsize: 65024
Current children cumulated CPU time (s) 948.85
Current children cumulated vsize (Kb) 67148

[startup+960.107 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 18395
Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18391/statm): 531 226 485 147 0 384 0
[pid=18391] vsize: 2124
Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 15365 0 0 0 95779 104 0 0 25 0 1 0 1851970759 66584576 15201 4294967295 134512640 135094434 3221224432 3221223088 134557964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18395/statm): 16256 15201 145 145 0 16111 0
[pid=18395] vsize: 65024
Current children cumulated CPU time (s) 958.85
Current children cumulated vsize (Kb) 67148

[startup+970.108 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 18395
Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18391/statm): 531 226 485 147 0 384 0
[pid=18391] vsize: 2124
Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 15377 0 0 0 96778 105 0 0 25 0 1 0 1851970759 66646016 15213 4294967295 134512640 135094434 3221224432 3221223088 134558153 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18395/statm): 16271 15213 145 145 0 16126 0
[pid=18395] vsize: 65084
Current children cumulated CPU time (s) 968.85
Current children cumulated vsize (Kb) 67208

[startup+980.111 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 18395
Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18391/statm): 531 226 485 147 0 384 0
[pid=18391] vsize: 2124
Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 15377 0 0 0 97778 106 0 0 25 0 1 0 1851970759 66646016 15213 4294967295 134512640 135094434 3221224432 3221223088 134557937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18395/statm): 16271 15213 145 145 0 16126 0
[pid=18395] vsize: 65084
Current children cumulated CPU time (s) 978.86
Current children cumulated vsize (Kb) 67208

[startup+990.112 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 18395
Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18391/statm): 531 226 485 147 0 384 0
[pid=18391] vsize: 2124
Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 15379 0 0 0 98778 106 0 0 25 0 1 0 1851970759 66646016 15215 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18395/statm): 16271 15215 145 145 0 16126 0
[pid=18395] vsize: 65084
Current children cumulated CPU time (s) 988.86
Current children cumulated vsize (Kb) 67208

[startup+1000.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 18395
Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18391/statm): 531 226 485 147 0 384 0
[pid=18391] vsize: 2124
Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 15379 0 0 0 99778 106 0 0 25 0 1 0 1851970759 66646016 15215 4294967295 134512640 135094434 3221224432 3221223088 134558178 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18395/statm): 16271 15215 145 145 0 16126 0
[pid=18395] vsize: 65084
Current children cumulated CPU time (s) 998.86
Current children cumulated vsize (Kb) 67208

[startup+1010.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 18395
Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18391/statm): 531 226 485 147 0 384 0
[pid=18391] vsize: 2124
Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 15379 0 0 0 100778 107 0 0 25 0 1 0 1851970759 66646016 15215 4294967295 134512640 135094434 3221224432 3221223056 134557669 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18395/statm): 16271 15215 145 145 0 16126 0
[pid=18395] vsize: 65084
Current children cumulated CPU time (s) 1008.87
Current children cumulated vsize (Kb) 67208

[startup+1020.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 18395
Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18391/statm): 531 226 485 147 0 384 0
[pid=18391] vsize: 2124
Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 15379 0 0 0 101779 107 0 0 25 0 1 0 1851970759 66646016 15215 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18395/statm): 16271 15215 145 145 0 16126 0
[pid=18395] vsize: 65084
Current children cumulated CPU time (s) 1018.88
Current children cumulated vsize (Kb) 67208

[startup+1030.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 18395
Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18391/statm): 531 226 485 147 0 384 0
[pid=18391] vsize: 2124
Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 15379 0 0 0 102778 107 0 0 25 0 1 0 1851970759 66646016 15215 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18395/statm): 16271 15215 145 145 0 16126 0
[pid=18395] vsize: 65084
Current children cumulated CPU time (s) 1028.87
Current children cumulated vsize (Kb) 67208

[startup+1040.12 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 18395
Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18391/statm): 531 226 485 147 0 384 0
[pid=18391] vsize: 2124
Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 15379 0 0 0 103779 107 0 0 25 0 1 0 1851970759 66646016 15215 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18395/statm): 16271 15215 145 145 0 16126 0
[pid=18395] vsize: 65084
Current children cumulated CPU time (s) 1038.88
Current children cumulated vsize (Kb) 67208

[startup+1050.12 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 18395
Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18391/statm): 531 226 485 147 0 384 0
[pid=18391] vsize: 2124
Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 15379 0 0 0 104779 107 0 0 25 0 1 0 1851970759 66646016 15215 4294967295 134512640 135094434 3221224432 3221223088 134558002 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18395/statm): 16271 15215 145 145 0 16126 0
[pid=18395] vsize: 65084
Current children cumulated CPU time (s) 1048.88
Current children cumulated vsize (Kb) 67208

[startup+1060.12 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 18395
Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18391/statm): 531 226 485 147 0 384 0
[pid=18391] vsize: 2124
Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 15379 0 0 0 105779 107 0 0 25 0 1 0 1851970759 66646016 15215 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18395/statm): 16271 15215 145 145 0 16126 0
[pid=18395] vsize: 65084
Current children cumulated CPU time (s) 1058.88
Current children cumulated vsize (Kb) 67208

[startup+1070.12 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 18395
Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18391/statm): 531 226 485 147 0 384 0
[pid=18391] vsize: 2124
Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 15379 0 0 0 106779 107 0 0 25 0 1 0 1851970759 66646016 15215 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18395/statm): 16271 15215 145 145 0 16126 0
[pid=18395] vsize: 65084
Current children cumulated CPU time (s) 1068.88
Current children cumulated vsize (Kb) 67208

[startup+1080.12 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 18395
Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18391/statm): 531 226 485 147 0 384 0
[pid=18391] vsize: 2124
Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 15381 0 0 0 107779 108 0 0 25 0 1 0 1851970759 66646016 15217 4294967295 134512640 135094434 3221224432 3221223088 134557890 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18395/statm): 16271 15217 145 145 0 16126 0
[pid=18395] vsize: 65084
Current children cumulated CPU time (s) 1078.89
Current children cumulated vsize (Kb) 67208

[startup+1090.12 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 18395
Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18391/statm): 531 226 485 147 0 384 0
[pid=18391] vsize: 2124
Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 15381 0 0 0 108779 108 0 0 25 0 1 0 1851970759 66646016 15217 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18395/statm): 16271 15217 145 145 0 16126 0
[pid=18395] vsize: 65084
Current children cumulated CPU time (s) 1088.89
Current children cumulated vsize (Kb) 67208

[startup+1100.12 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 18395
Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18391/statm): 531 226 485 147 0 384 0
[pid=18391] vsize: 2124
Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 15381 0 0 0 109780 108 0 0 25 0 1 0 1851970759 66646016 15217 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18395/statm): 16271 15217 145 145 0 16126 0
[pid=18395] vsize: 65084
Current children cumulated CPU time (s) 1098.9
Current children cumulated vsize (Kb) 67208

[startup+1110.12 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 18395
Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18391/statm): 531 226 485 147 0 384 0
[pid=18391] vsize: 2124
Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 15381 0 0 0 110780 108 0 0 25 0 1 0 1851970759 66646016 15217 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18395/statm): 16271 15217 145 145 0 16126 0
[pid=18395] vsize: 65084
Current children cumulated CPU time (s) 1108.9
Current children cumulated vsize (Kb) 67208

[startup+1120.12 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 18395
Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18391/statm): 531 226 485 147 0 384 0
[pid=18391] vsize: 2124
Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 15381 0 0 0 111780 108 0 0 25 0 1 0 1851970759 66646016 15217 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18395/statm): 16271 15217 145 145 0 16126 0
[pid=18395] vsize: 65084
Current children cumulated CPU time (s) 1118.9
Current children cumulated vsize (Kb) 67208

[startup+1130.12 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 18395
Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18391/statm): 531 226 485 147 0 384 0
[pid=18391] vsize: 2124
Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 15381 0 0 0 112780 108 0 0 25 0 1 0 1851970759 66646016 15217 4294967295 134512640 135094434 3221224432 3221223088 134558126 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18395/statm): 16271 15217 145 145 0 16126 0
[pid=18395] vsize: 65084
Current children cumulated CPU time (s) 1128.9
Current children cumulated vsize (Kb) 67208

[startup+1140.12 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 18395
Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18391/statm): 531 226 485 147 0 384 0
[pid=18391] vsize: 2124
Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 15392 0 0 0 113780 108 0 0 25 0 1 0 1851970759 66711552 15228 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18395/statm): 16287 15228 145 145 0 16142 0
[pid=18395] vsize: 65148
Current children cumulated CPU time (s) 1138.9
Current children cumulated vsize (Kb) 67272

[startup+1150.13 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 18395
Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18391/statm): 531 226 485 147 0 384 0
[pid=18391] vsize: 2124
Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 15392 0 0 0 114780 108 0 0 25 0 1 0 1851970759 66711552 15228 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18395/statm): 16287 15228 145 145 0 16142 0
[pid=18395] vsize: 65148
Current children cumulated CPU time (s) 1148.9
Current children cumulated vsize (Kb) 67272

[startup+1160.13 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 18395
Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18391/statm): 531 226 485 147 0 384 0
[pid=18391] vsize: 2124
Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 15392 0 0 0 115781 108 0 0 25 0 1 0 1851970759 66711552 15228 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18395/statm): 16287 15228 145 145 0 16142 0
[pid=18395] vsize: 65148
Current children cumulated CPU time (s) 1158.91
Current children cumulated vsize (Kb) 67272

[startup+1170.13 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 18395
Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18391/statm): 531 226 485 147 0 384 0
[pid=18391] vsize: 2124
Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 15392 0 0 0 116781 108 0 0 25 0 1 0 1851970759 66711552 15228 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18395/statm): 16287 15228 145 145 0 16142 0
[pid=18395] vsize: 65148
Current children cumulated CPU time (s) 1168.91
Current children cumulated vsize (Kb) 67272

[startup+1180.13 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 18395
Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18391/statm): 531 226 485 147 0 384 0
[pid=18391] vsize: 2124
Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 15392 0 0 0 117781 108 0 0 25 0 1 0 1851970759 66711552 15228 4294967295 134512640 135094434 3221224432 3221223068 134557639 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18395/statm): 16287 15228 145 145 0 16142 0
[pid=18395] vsize: 65148
Current children cumulated CPU time (s) 1178.91
Current children cumulated vsize (Kb) 67272

[startup+1190.13 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 18395
Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18391/statm): 531 226 485 147 0 384 0
[pid=18391] vsize: 2124
Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 15404 0 0 0 118781 108 0 0 25 0 1 0 1851970759 66777088 15240 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/18395/statm): 16303 15240 145 145 0 16158 0
[pid=18395] vsize: 65212
Current children cumulated CPU time (s) 1188.91
Current children cumulated vsize (Kb) 67336

[startup+1200.13 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 18395
Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18391/statm): 531 226 485 147 0 384 0
[pid=18391] vsize: 2124
Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 15404 0 0 0 119780 109 0 0 25 0 1 0 1851970759 66777088 15240 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18395/statm): 16303 15240 145 145 0 16158 0
[pid=18395] vsize: 65212
Current children cumulated CPU time (s) 1198.91
Current children cumulated vsize (Kb) 67336

[startup+1210.13 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 18395
Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18391/statm): 531 226 485 147 0 384 0
[pid=18391] vsize: 2124
Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 15414 0 0 0 120781 109 0 0 25 0 1 0 1851970759 66842624 15250 4294967295 134512640 135094434 3221224432 3221223088 134557964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18395/statm): 16319 15250 145 145 0 16174 0
[pid=18395] vsize: 65276
Current children cumulated CPU time (s) 1208.92
Current children cumulated vsize (Kb) 67400



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.13 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 18395
Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18391/statm): 531 226 485 147 0 384 0
[pid=18391] vsize: 2124
Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 15414 0 0 0 120781 109 0 0 25 0 1 0 1851970759 66842624 15250 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18395/statm): 16319 15250 145 145 0 16174 0
[pid=18395] vsize: 65276
Current children cumulated CPU time (s) 1208.92
Current children cumulated vsize (Kb) 67400

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

Child status: 0
Real time (s): 1210.17
CPU time (s): 1208.93
CPU user time (s): 1207.81
CPU system time (s): 1.11883
CPU usage (%): 99.898
Max. virtual memory (cumulated for all children) (Kb): 67400

Verifier Data

ERROR: no interpretation found !