Some explanations

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

General information on the benchmark

Namemps-v2-13-7/MIPLIB/miplib3/normalized-mps-v2-13-7-mod010.opb
MD5SUMef7064a9be2b712276f7b600af28e2b0
Bench Categoryoptimization, small integers (OPTSMALLINT)
Has Objective FunctionYES
Satisfiable
(Un)Satisfiability was proved
Best value of the objective function
Optimality of the best value was proved
Number of terms in the objective function 2655
Biggest coefficient in the objective function 266
Number of bits for the biggest coefficient in the objective function 9
Sum of the numbers in the objective function 489211
Number of bits of the sum of numbers in the objective function 19
Biggest number in a constraint 266
Number of bits of the biggest number in a constraint 9
Biggest sum of numbers in a constraint 489211
Number of bits of the biggest sum of numbers19
Best result obtained on this benchmark
Best CPU time to get the best result obtained on this benchmark
Number of variables2655
Total number of constraints2801
Number of constraints which are clauses0
Number of constraints which are cardinality constraints (but not clauses)2800
Number of constraints which are nor clauses,nor cardinality constraints1
Minimum length of a constraint1
Maximum length of a constraint2655

Trace number 6219

Launcher Data

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.190
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:        829952 kB
Buffers:         17328 kB
Cached:         160820 kB
SwapCached:        828 kB
Active:          94772 kB
Inactive:        86020 kB
HighTotal:      131008 kB
HighFree:          896 kB
LowTotal:       903652 kB
LowFree:        829056 kB
SwapTotal:     2097136 kB
SwapFree:      2095740 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5664 kB
Slab:            18264 kB
Committed_AS:    72360 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-09-20 04:50:49 (client local time) WITH STATUS 0 IN 1206.44 SECONDS
stats: 3375 7 1206.44 0

Solver Data

c Parsing PB file...
c Converting 291 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: #################################################################################################################################################
c   -- Clauses(.)/Splits(s): (none)
c ---[ 289]---> BDD-cost:   67
c ---[ 287]---> BDD-cost:  113
c ---[ 285]---> BDD-cost:  181
c ---[ 283]---> BDD-cost:  115
c ---[ 281]---> BDD-cost:   69
c ---[ 279]---> BDD-cost:  125
c ---[ 277]---> BDD-cost:  155
c ---[ 275]---> BDD-cost:   87
c ---[ 273]---> BDD-cost:   97
c ---[ 271]---> BDD-cost:   73
c ---[ 269]---> BDD-cost:  119
c ---[ 267]---> BDD-cost:   45
c ---[ 265]---> BDD-cost:  171
c ---[ 263]---> BDD-cost:  111
c ---[ 261]---> BDD-cost:  149
c ---[ 259]---> BDD-cost:  195
c ---[ 257]---> BDD-cost:  131
c ---[ 255]---> BDD-cost:  123
c ---[ 253]---> BDD-cost:  167
c ---[ 251]---> BDD-cost:  101
c ---[ 249]---> BDD-cost:   97
c ---[ 247]---> BDD-cost:   23
c ---[ 245]---> BDD-cost:  135
c ---[ 243]---> BDD-cost:   59
c ---[ 241]---> BDD-cost:   95
c ---[ 239]---> BDD-cost:   59
c ---[ 237]---> BDD-cost:  133
c ---[ 235]---> BDD-cost:   99
c ---[ 233]---> BDD-cost:  179
c ---[ 231]---> BDD-cost:  111
c ---[ 229]---> BDD-cost:   23
c ---[ 227]---> BDD-cost:   89
c ---[ 225]---> BDD-cost:   95
c ---[ 223]---> BDD-cost:  117
c ---[ 221]---> BDD-cost:   23
c ---[ 219]---> BDD-cost:   51
c ---[ 217]---> BDD-cost:  311
c ---[ 215]---> BDD-cost:  259
c ---[ 213]---> BDD-cost:  169
c ---[ 211]---> BDD-cost:  131
c ---[ 209]---> BDD-cost:  155
c ---[ 207]---> BDD-cost:   89
c ---[ 205]---> BDD-cost:   51
c ---[ 203]---> BDD-cost:  165
c ---[ 201]---> BDD-cost:   75
c ---[ 199]---> BDD-cost:  139
c ---[ 197]---> BDD-cost:   67
c ---[ 195]---> BDD-cost:  173
c ---[ 193]---> BDD-cost:  235
c ---[ 191]---> BDD-cost:  185
c ---[ 189]---> BDD-cost:  127
c ---[ 187]---> BDD-cost:   37
c ---[ 185]---> BDD-cost:   37
c ---[ 183]---> BDD-cost:   91
c ---[ 181]---> BDD-cost:   77
c ---[ 179]---> BDD-cost:   29
c ---[ 177]---> BDD-cost:   77
c ---[ 175]---> BDD-cost:   77
c ---[ 173]---> BDD-cost:  101
c ---[ 171]---> BDD-cost:  131
c ---[ 169]---> BDD-cost:  155
c ---[ 167]---> BDD-cost:  177
c ---[ 165]---> BDD-cost:  143
c ---[ 163]---> BDD-cost:   93
c ---[ 161]---> BDD-cost:   79
c ---[ 159]---> BDD-cost:   53
c ---[ 157]---> BDD-cost:   71
c ---[ 155]---> BDD-cost:  127
c ---[ 153]---> BDD-cost:  127
c ---[ 151]---> BDD-cost:   67
c ---[ 149]---> BDD-cost:   83
c ---[ 147]---> BDD-cost:   47
c ---[ 145]---> BDD-cost:   63
c ---[ 143]---> BDD-cost:  121
c ---[ 141]---> BDD-cost:  155
c ---[ 139]---> BDD-cost:   87
c ---[ 137]---> BDD-cost:   91
c ---[ 135]---> BDD-cost:   47
c ---[ 133]---> BDD-cost:   67
c ---[ 131]---> BDD-cost:   33
c ---[ 129]---> BDD-cost:   91
c ---[ 127]---> BDD-cost:   69
c ---[ 125]---> BDD-cost:    5
c ---[ 123]---> BDD-cost:   47
c ---[ 121]---> BDD-cost:   45
c ---[ 119]---> BDD-cost:   37
c ---[ 117]---> BDD-cost:  117
c ---[ 115]---> BDD-cost:   97
c ---[ 113]---> BDD-cost:   77
c ---[ 111]---> BDD-cost:   97
c ---[ 109]---> BDD-cost:  137
c ---[ 107]---> BDD-cost:  125
c ---[ 105]---> BDD-cost:   79
c ---[ 103]---> BDD-cost:  133
c ---[ 101]---> BDD-cost:  153
c ---[  99]---> BDD-cost:  139
c ---[  97]---> BDD-cost:  125
c ---[  95]---> BDD-cost:    5
c ---[  93]---> BDD-cost:   73
c ---[  91]---> BDD-cost:  157
c ---[  89]---> BDD-cost:  127
c ---[  87]---> BDD-cost:  199
c ---[  85]---> BDD-cost:  121
c ---[  83]---> BDD-cost:  107
c ---[  81]---> BDD-cost:  169
c ---[  79]---> BDD-cost:  113
c ---[  77]---> BDD-cost:  103
c ---[  75]---> BDD-cost:   75
c ---[  73]---> BDD-cost:   97
c ---[  71]---> BDD-cost:  151
c ---[  69]---> BDD-cost:  199
c ---[  67]---> BDD-cost:  109
c ---[  65]---> BDD-cost:  131
c ---[  63]---> BDD-cost:  113
c ---[  61]---> BDD-cost:  173
c ---[  59]---> BDD-cost:  119
c ---[  57]---> BDD-cost:  173
c ---[  55]---> BDD-cost:  119
c ---[  53]---> BDD-cost:   71
c ---[  51]---> BDD-cost:  179
c ---[  49]---> BDD-cost:  241
c ---[  47]---> BDD-cost:  201
c ---[  45]---> BDD-cost:  173
c ---[  43]---> BDD-cost:  147
c ---[  41]---> BDD-cost:  157
c ---[  39]---> BDD-cost:  201
c ---[  37]---> BDD-cost:  129
c ---[  35]---> BDD-cost:  117
c ---[  33]---> BDD-cost:  177
c ---[  31]---> BDD-cost:  123
c ---[  29]---> BDD-cost:  131
c ---[  27]---> BDD-cost:  115
c ---[  25]---> BDD-cost:   51
c ---[  23]---> BDD-cost:  123
c ---[  21]---> BDD-cost:   55
c ---[  19]---> BDD-cost:    5
c ---[  17]---> BDD-cost:   99
c ---[  15]---> BDD-cost:   85
c ---[  13]---> BDD-cost:  109
c ---[  11]---> BDD-cost:  153
c ---[   9]---> BDD-cost:  201
c ---[   7]---> BDD-cost:  133
c ---[   5]---> BDD-cost:  121
c ---[   3]---> BDD-cost:  171
c ---[   1]---> Adder-cost: 5294   maxlim: 2609   bits: 12/12
c ---[   0]---> BDD-cost:  751
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   79291   242194 |   26430       0        0     nan |  0.000 % |
c |       101 |   79216   241933 |   29073      93      735     7.9 |  0.735 % |
c |       253 |   79216   241933 |   31980     245     2664    10.9 |  0.735 % |
c |       478 |   79216   241933 |   35178     470    26790    57.0 |  0.735 % |
c |       816 |   79216   241933 |   38696     808    31842    39.4 |  0.735 % |
c |      1323 |   79216   241933 |   42565    1315    62134    47.3 |  0.735 % |
c |      2082 |   79216   241933 |   46822    2074   107560    51.9 |  0.735 % |
c |      3222 |   79188   241847 |   51504    3207   277140    86.4 |  0.751 % |
c |      4930 |   79188   241847 |   56655    4915   483903    98.5 |  0.751 % |
c |      7493 |   79188   241847 |   62320    7478   739580    98.9 |  0.751 % |
c |     11337 |   79188   241847 |   68552   11322  1362239   120.3 |  0.751 % |
c |     17103 |   79164   241769 |   75407   17085  2978250   174.3 |  0.767 % |
c |     25752 |   79164   241769 |   82948   25734  6444146   250.4 |  0.767 % |
c |     38727 |   79164   241769 |   91243   38709 10596182   273.7 |  0.767 % |
c |     58188 |   79145   241708 |  100367   58167 16215504   278.8 |  0.779 % |
c |     87383 |   79101   241554 |  110404   87356 23978747   274.5 |  0.807 % |
c |    131172 |   79079   241468 |  121445   35237  6368599   180.7 |  0.823 % |
c |    196857 |   78549   239688 |  133589  100806 30304920   300.6 |  1.134 % |

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/4497/stat): 4497 (minisat+_script) R 4496 4497 31915 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1797431705 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 0 0 0
Raw data (/proc/4497/statm): 174 3 169 147 0 27 0
[pid=4497] 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=4498
New process pid=4499
New process pid=4500
execve syscall for /bin/sed executable
One traced child (pid=4499) 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=4500) exited with status: 0
One traced child (pid=4498) exited with status: 0
New process pid=4501
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc3/normalized-mps-v2-13-7-mod010.opb

[startup+10.004 s]
Raw data (loadavg): 0.71 0.89 0.89 2/57 4501
Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4497/statm): 531 226 485 147 0 384 0
[pid=4497] vsize: 2124
Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 5211 0 0 0 958 19 0 0 25 0 1 0 1797431710 20324352 4505 4294967295 134512640 135094434 3221224432 3221223120 134554739 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4501/statm): 4962 4505 145 145 0 4817 0
[pid=4501] vsize: 19848
Current children cumulated CPU time (s) 9.79
Current children cumulated vsize (Kb) 21972

[startup+20.0048 s]
Raw data (loadavg): 0.75 0.90 0.89 2/57 4501
Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4497/statm): 531 226 485 147 0 384 0
[pid=4497] vsize: 2124
Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 5775 0 0 0 1949 23 0 0 25 0 1 0 1797431710 22634496 5069 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4501/statm): 5526 5069 145 145 0 5381 0
[pid=4501] vsize: 22104
Current children cumulated CPU time (s) 19.74
Current children cumulated vsize (Kb) 24228

[startup+30.0057 s]
Raw data (loadavg): 0.79 0.90 0.89 2/57 4501
Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4497/statm): 531 226 485 147 0 384 0
[pid=4497] vsize: 2124
Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 6335 0 0 0 2940 27 0 0 25 0 1 0 1797431710 24952832 5629 4294967295 134512640 135094434 3221224432 3221223056 134562085 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4501/statm): 6092 5629 145 145 0 5947 0
[pid=4501] vsize: 24368
Current children cumulated CPU time (s) 29.69
Current children cumulated vsize (Kb) 26492

[startup+40.0065 s]
Raw data (loadavg): 0.82 0.90 0.89 2/57 4501
Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4497/statm): 531 226 485 147 0 384 0
[pid=4497] vsize: 2124
Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 7103 0 0 0 3928 30 0 0 25 0 1 0 1797431710 28086272 6397 4294967295 134512640 135094434 3221224432 3221223024 134556949 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4501/statm): 6857 6397 145 145 0 6712 0
[pid=4501] vsize: 27428
Current children cumulated CPU time (s) 39.6
Current children cumulated vsize (Kb) 29552

[startup+50.0084 s]
Raw data (loadavg): 0.85 0.91 0.89 2/57 4501
Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4497/statm): 531 226 485 147 0 384 0
[pid=4497] vsize: 2124
Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 7842 0 0 0 4914 36 0 0 25 0 1 0 1797431710 31105024 7136 4294967295 134512640 135094434 3221224432 3221223084 134558036 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4501/statm): 7594 7136 145 145 0 7449 0
[pid=4501] vsize: 30376
Current children cumulated CPU time (s) 49.52
Current children cumulated vsize (Kb) 32500

[startup+60.0092 s]
Raw data (loadavg): 0.87 0.91 0.89 2/57 4501
Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4497/statm): 531 226 485 147 0 384 0
[pid=4497] vsize: 2124
Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 8476 0 0 0 5905 39 0 0 25 0 1 0 1797431710 33751040 7770 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4501/statm): 8240 7770 145 145 0 8095 0
[pid=4501] vsize: 32960
Current children cumulated CPU time (s) 59.46
Current children cumulated vsize (Kb) 35084

[startup+70.01 s]
Raw data (loadavg): 0.89 0.91 0.89 2/57 4501
Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4497/statm): 531 226 485 147 0 384 0
[pid=4497] vsize: 2124
Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 9112 0 0 0 6896 44 0 0 25 0 1 0 1797431710 36347904 8406 4294967295 134512640 135094434 3221224432 3221223120 134554685 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4501/statm): 8874 8406 145 145 0 8729 0
[pid=4501] vsize: 35496
Current children cumulated CPU time (s) 69.42
Current children cumulated vsize (Kb) 37620

[startup+80.0119 s]
Raw data (loadavg): 0.91 0.91 0.89 2/57 4501
Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4497/statm): 531 226 485 147 0 384 0
[pid=4497] vsize: 2124
Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 9720 0 0 0 7887 48 0 0 25 0 1 0 1797431710 38830080 9014 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4501/statm): 9480 9014 145 145 0 9335 0
[pid=4501] vsize: 37920
Current children cumulated CPU time (s) 79.37
Current children cumulated vsize (Kb) 40044

[startup+90.0127 s]
Raw data (loadavg): 0.92 0.92 0.89 2/57 4501
Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4497/statm): 531 226 485 147 0 384 0
[pid=4497] vsize: 2124
Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 10303 0 0 0 8878 52 0 0 25 0 1 0 1797431710 41218048 9597 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4501/statm): 10063 9597 145 145 0 9918 0
[pid=4501] vsize: 40252
Current children cumulated CPU time (s) 89.32
Current children cumulated vsize (Kb) 42376

[startup+100.014 s]
Raw data (loadavg): 0.93 0.92 0.89 2/57 4501
Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4497/statm): 531 226 485 147 0 384 0
[pid=4497] vsize: 2124
Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 10840 0 0 0 9869 56 0 0 25 0 1 0 1797431710 43417600 10134 4294967295 134512640 135094434 3221224432 3221223088 134558011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4501/statm): 10600 10134 145 145 0 10455 0
[pid=4501] vsize: 42400
Current children cumulated CPU time (s) 99.27
Current children cumulated vsize (Kb) 44524

[startup+110.014 s]
Raw data (loadavg): 0.94 0.92 0.90 2/57 4501
Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4497/statm): 531 226 485 147 0 384 0
[pid=4497] vsize: 2124
Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 11374 0 0 0 10863 59 0 0 25 0 1 0 1797431710 45613056 10668 4294967295 134512640 135094434 3221224432 3221223088 134558156 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4501/statm): 11136 10668 145 145 0 10991 0
[pid=4501] vsize: 44544
Current children cumulated CPU time (s) 109.24
Current children cumulated vsize (Kb) 46668

[startup+120.015 s]
Raw data (loadavg): 0.95 0.92 0.90 2/57 4501
Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4497/statm): 531 226 485 147 0 384 0
[pid=4497] vsize: 2124
Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 11957 0 0 0 11854 61 0 0 25 0 1 0 1797431710 48001024 11251 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4501/statm): 11719 11251 145 145 0 11574 0
[pid=4501] vsize: 46876
Current children cumulated CPU time (s) 119.17
Current children cumulated vsize (Kb) 49000

[startup+130.016 s]
Raw data (loadavg): 0.96 0.92 0.90 2/57 4501
Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4497/statm): 531 226 485 147 0 384 0
[pid=4497] vsize: 2124
Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 12660 0 0 0 12842 66 0 0 25 0 1 0 1797431710 50876416 11954 4294967295 134512640 135094434 3221224432 3221223024 134557202 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4501/statm): 12421 11954 145 145 0 12276 0
[pid=4501] vsize: 49684
Current children cumulated CPU time (s) 129.1
Current children cumulated vsize (Kb) 51808

[startup+140.017 s]
Raw data (loadavg): 0.96 0.93 0.90 2/57 4501
Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4497/statm): 531 226 485 147 0 384 0
[pid=4497] vsize: 2124
Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 13334 0 0 0 13831 70 0 0 25 0 1 0 1797431710 53628928 12628 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4501/statm): 13093 12628 145 145 0 12948 0
[pid=4501] vsize: 52372
Current children cumulated CPU time (s) 139.03
Current children cumulated vsize (Kb) 54496

[startup+150.019 s]
Raw data (loadavg): 0.97 0.93 0.90 2/57 4501
Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4497/statm): 531 226 485 147 0 384 0
[pid=4497] vsize: 2124
Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 13995 0 0 0 14821 74 0 0 25 0 1 0 1797431710 56332288 13289 4294967295 134512640 135094434 3221224432 3221223024 134556791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4501/statm): 13753 13289 145 145 0 13608 0
[pid=4501] vsize: 55012
Current children cumulated CPU time (s) 148.97
Current children cumulated vsize (Kb) 57136

[startup+160.02 s]
Raw data (loadavg): 0.97 0.93 0.90 2/57 4501
Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4497/statm): 531 226 485 147 0 384 0
[pid=4497] vsize: 2124
Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 14621 0 0 0 15812 78 0 0 25 0 1 0 1797431710 59023360 13915 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4501/statm): 14410 13915 145 145 0 14265 0
[pid=4501] vsize: 57640
Current children cumulated CPU time (s) 158.92
Current children cumulated vsize (Kb) 59764

[startup+170.02 s]
Raw data (loadavg): 0.98 0.93 0.90 2/57 4501
Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4497/statm): 531 226 485 147 0 384 0
[pid=4497] vsize: 2124
Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 15221 0 0 0 16801 83 0 0 25 0 1 0 1797431710 61472768 14515 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4501/statm): 15008 14515 145 145 0 14863 0
[pid=4501] vsize: 60032
Current children cumulated CPU time (s) 168.86
Current children cumulated vsize (Kb) 62156

[startup+180.021 s]
Raw data (loadavg): 0.98 0.93 0.90 2/57 4501
Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4497/statm): 531 226 485 147 0 384 0
[pid=4497] vsize: 2124
Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 15820 0 0 0 17788 88 0 0 25 0 1 0 1797431710 63913984 15114 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4501/statm): 15604 15114 145 145 0 15459 0
[pid=4501] vsize: 62416
Current children cumulated CPU time (s) 178.78
Current children cumulated vsize (Kb) 64540

[startup+190.022 s]
Raw data (loadavg): 0.98 0.94 0.90 2/57 4501
Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4497/statm): 531 226 485 147 0 384 0
[pid=4497] vsize: 2124
Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 16388 0 0 0 18778 92 0 0 25 0 1 0 1797431710 66236416 15682 4294967295 134512640 135094434 3221224432 3221223024 134557512 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4501/statm): 16171 15682 145 145 0 16026 0
[pid=4501] vsize: 64684
Current children cumulated CPU time (s) 188.72
Current children cumulated vsize (Kb) 66808

[startup+200.023 s]
Raw data (loadavg): 0.98 0.94 0.90 2/57 4501
Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4497/statm): 531 226 485 147 0 384 0
[pid=4497] vsize: 2124
Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 16986 0 0 0 19767 97 0 0 25 0 1 0 1797431710 68677632 16280 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4501/statm): 16767 16280 145 145 0 16622 0
[pid=4501] vsize: 67068
Current children cumulated CPU time (s) 198.66
Current children cumulated vsize (Kb) 69192

[startup+210.024 s]
Raw data (loadavg): 0.99 0.94 0.91 1/57 4501
Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4497/statm): 531 226 485 147 0 384 0
[pid=4497] vsize: 2124
Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) T 4497 4497 31915 0 -1 0 17772 0 0 0 20754 103 0 0 25 0 1 0 1797431710 71888896 17066 4294967295 134512640 135094434 3221224432 3221222796 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/4501/statm): 17551 17066 145 145 0 17406 0
[pid=4501] vsize: 70204
Current children cumulated CPU time (s) 208.59
Current children cumulated vsize (Kb) 72328

[startup+220.025 s]
Raw data (loadavg): 0.99 0.94 0.91 2/57 4501
Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4497/statm): 531 226 485 147 0 384 0
[pid=4497] vsize: 2124
Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 18478 0 0 0 21745 107 0 0 25 0 1 0 1797431710 74776576 17772 4294967295 134512640 135094434 3221224432 3221223024 134557002 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4501/statm): 18256 17772 145 145 0 18111 0
[pid=4501] vsize: 73024
Current children cumulated CPU time (s) 218.54
Current children cumulated vsize (Kb) 75148

[startup+230.025 s]
Raw data (loadavg): 0.99 0.94 0.91 2/57 4501
Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4497/statm): 531 226 485 147 0 384 0
[pid=4497] vsize: 2124
Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 19121 0 0 0 22736 111 0 0 25 0 1 0 1797431710 77406208 18415 4294967295 134512640 135094434 3221224432 3221223024 134557244 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4501/statm): 18898 18415 145 145 0 18753 0
[pid=4501] vsize: 75592
Current children cumulated CPU time (s) 228.49
Current children cumulated vsize (Kb) 77716

[startup+240.026 s]
Raw data (loadavg): 0.99 0.94 0.91 2/57 4501
Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4497/statm): 531 226 485 147 0 384 0
[pid=4497] vsize: 2124
Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 19736 0 0 0 23728 114 0 0 25 0 1 0 1797431710 79917056 19030 4294967295 134512640 135094434 3221224432 3221223024 134557423 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4501/statm): 19511 19030 145 145 0 19366 0
[pid=4501] vsize: 78044
Current children cumulated CPU time (s) 238.44
Current children cumulated vsize (Kb) 80168

[startup+250.027 s]
Raw data (loadavg): 0.99 0.94 0.91 2/57 4501
Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4497/statm): 531 226 485 147 0 384 0
[pid=4497] vsize: 2124
Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 20334 0 0 0 24718 119 0 0 25 0 1 0 1797431710 82358272 19628 4294967295 134512640 135094434 3221224432 3221223088 134557903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4501/statm): 20107 19628 145 145 0 19962 0
[pid=4501] vsize: 80428
Current children cumulated CPU time (s) 248.39
Current children cumulated vsize (Kb) 82552

[startup+260.028 s]
Raw data (loadavg): 0.99 0.95 0.91 2/57 4501
Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4497/statm): 531 226 485 147 0 384 0
[pid=4497] vsize: 2124
Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 20947 0 0 0 25706 123 0 0 25 0 1 0 1797431710 84869120 20241 4294967295 134512640 135094434 3221224432 3221223088 134558227 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4501/statm): 20720 20241 145 145 0 20575 0
[pid=4501] vsize: 82880
Current children cumulated CPU time (s) 258.31
Current children cumulated vsize (Kb) 85004

[startup+270.028 s]
Raw data (loadavg): 0.99 0.95 0.91 2/57 4501
Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4497/statm): 531 226 485 147 0 384 0
[pid=4497] vsize: 2124
Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 21481 0 0 0 26698 127 0 0 25 0 1 0 1797431710 87068672 20775 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4501/statm): 21257 20775 145 145 0 21112 0
[pid=4501] vsize: 85028
Current children cumulated CPU time (s) 268.27
Current children cumulated vsize (Kb) 87152

[startup+280.029 s]
Raw data (loadavg): 0.99 0.95 0.91 2/57 4501
Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4497/statm): 531 226 485 147 0 384 0
[pid=4497] vsize: 2124
Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 21954 0 0 0 27691 129 0 0 25 0 1 0 1797431710 89006080 21248 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4501/statm): 21730 21248 145 145 0 21585 0
[pid=4501] vsize: 86920
Current children cumulated CPU time (s) 278.22
Current children cumulated vsize (Kb) 89044

[startup+290.029 s]
Raw data (loadavg): 0.99 0.95 0.91 1/57 4501
Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4497/statm): 531 226 485 147 0 384 0
[pid=4497] vsize: 2124
Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) T 4497 4497 31915 0 -1 0 22496 0 0 0 28682 132 0 0 25 0 1 0 1797431710 91213824 21790 4294967295 134512640 135094434 3221224432 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/4501/statm): 22269 21790 145 145 0 22124 0
[pid=4501] vsize: 89076
Current children cumulated CPU time (s) 288.16
Current children cumulated vsize (Kb) 91200

[startup+300.029 s]
Raw data (loadavg): 0.99 0.95 0.91 2/57 4501
Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4497/statm): 531 226 485 147 0 384 0
[pid=4497] vsize: 2124
Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 23084 0 0 0 29673 135 0 0 25 0 1 0 1797431710 93618176 22378 4294967295 134512640 135094434 3221224432 3221223024 134557421 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4501/statm): 22856 22378 145 145 0 22711 0
[pid=4501] vsize: 91424
Current children cumulated CPU time (s) 298.1
Current children cumulated vsize (Kb) 93548

[startup+310.03 s]
Raw data (loadavg): 0.99 0.95 0.91 2/57 4501
Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4497/statm): 531 226 485 147 0 384 0
[pid=4497] vsize: 2124
Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 23699 0 0 0 30664 140 0 0 25 0 1 0 1797431710 96129024 22993 4294967295 134512640 135094434 3221224432 3221223024 134556990 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4501/statm): 23469 22993 145 145 0 23324 0
[pid=4501] vsize: 93876
Current children cumulated CPU time (s) 308.06
Current children cumulated vsize (Kb) 96000

[startup+320.031 s]
Raw data (loadavg): 0.99 0.95 0.91 2/57 4501
Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4497/statm): 531 226 485 147 0 384 0
[pid=4497] vsize: 2124
Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 24123 0 0 0 31657 143 0 0 25 0 1 0 1797431710 98119680 23417 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4501/statm): 23955 23417 145 145 0 23810 0
[pid=4501] vsize: 95820
Current children cumulated CPU time (s) 318.02
Current children cumulated vsize (Kb) 97944

[startup+330.032 s]
Raw data (loadavg): 0.99 0.95 0.91 2/57 4501
Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4497/statm): 531 226 485 147 0 384 0
[pid=4497] vsize: 2124
Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 24735 0 0 0 32649 146 0 0 25 0 1 0 1797431710 100618240 24029 4294967295 134512640 135094434 3221224432 3221223104 134555568 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4501/statm): 24565 24029 145 145 0 24420 0
[pid=4501] vsize: 98260
Current children cumulated CPU time (s) 327.97
Current children cumulated vsize (Kb) 100384

[startup+340.033 s]
Raw data (loadavg): 0.99 0.95 0.91 2/57 4501
Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4497/statm): 531 226 485 147 0 384 0
[pid=4497] vsize: 2124
Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 25142 0 0 0 33642 151 0 0 25 0 1 0 1797431710 102277120 24436 4294967295 134512640 135094434 3221224432 3221223024 134557421 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4501/statm): 24970 24436 145 145 0 24825 0
[pid=4501] vsize: 99880
Current children cumulated CPU time (s) 337.95
Current children cumulated vsize (Kb) 102004

[startup+350.032 s]
Raw data (loadavg): 0.99 0.95 0.91 2/57 4501
Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4497/statm): 531 226 485 147 0 384 0
[pid=4497] vsize: 2124
Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 25756 0 0 0 34632 155 0 0 25 0 1 0 1797431710 104783872 25050 4294967295 134512640 135094434 3221224432 3221223088 134558235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4501/statm): 25582 25050 145 145 0 25437 0
[pid=4501] vsize: 102328
Current children cumulated CPU time (s) 347.89
Current children cumulated vsize (Kb) 104452

[startup+360.033 s]
Raw data (loadavg): 0.99 0.95 0.91 2/57 4501
Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4497/statm): 531 226 485 147 0 384 0
[pid=4497] vsize: 2124
Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 26491 0 0 0 35619 161 0 0 25 0 1 0 1797431710 107802624 25785 4294967295 134512640 135094434 3221224432 3221223024 134556789 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4501/statm): 26319 25785 145 145 0 26174 0
[pid=4501] vsize: 105276
Current children cumulated CPU time (s) 357.82
Current children cumulated vsize (Kb) 107400

[startup+370.034 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 4501
Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4497/statm): 531 226 485 147 0 384 0
[pid=4497] vsize: 2124
Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 27254 0 0 0 36610 164 0 0 25 0 1 0 1797431710 110923776 26548 4294967295 134512640 135094434 3221224432 3221223088 134558426 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4501/statm): 27081 26548 145 145 0 26936 0
[pid=4501] vsize: 108324
Current children cumulated CPU time (s) 367.76
Current children cumulated vsize (Kb) 110448

[startup+380.035 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 4501
Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4497/statm): 531 226 485 147 0 384 0
[pid=4497] vsize: 2124
Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 27732 0 0 0 37603 167 0 0 25 0 1 0 1797431710 112869376 27026 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4501/statm): 27556 27026 145 145 0 27411 0
[pid=4501] vsize: 110224
Current children cumulated CPU time (s) 377.72
Current children cumulated vsize (Kb) 112348

[startup+390.036 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 4501
Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4497/statm): 531 226 485 147 0 384 0
[pid=4497] vsize: 2124
Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 28056 0 0 0 38597 170 0 0 25 0 1 0 1797431710 114184192 27350 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4501/statm): 27877 27350 145 145 0 27732 0
[pid=4501] vsize: 111508
Current children cumulated CPU time (s) 387.69
Current children cumulated vsize (Kb) 113632

[startup+400.037 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 4501
Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4497/statm): 531 226 485 147 0 384 0
[pid=4497] vsize: 2124
Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 28592 0 0 0 39589 174 0 0 25 0 1 0 1797431710 116371456 27886 4294967295 134512640 135094434 3221224432 3221223088 134557996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4501/statm): 28411 27886 145 145 0 28266 0
[pid=4501] vsize: 113644
Current children cumulated CPU time (s) 397.65
Current children cumulated vsize (Kb) 115768

[startup+410.037 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 4501
Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4497/statm): 531 226 485 147 0 384 0
[pid=4497] vsize: 2124
Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 28992 0 0 0 40582 177 0 0 25 0 1 0 1797431710 118001664 28286 4294967295 134512640 135094434 3221224432 3221223024 134557213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4501/statm): 28809 28286 145 145 0 28664 0
[pid=4501] vsize: 115236
Current children cumulated CPU time (s) 407.61
Current children cumulated vsize (Kb) 117360

[startup+420.037 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 4501
Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4497/statm): 531 226 485 147 0 384 0
[pid=4497] vsize: 2124
Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 29499 0 0 0 41573 181 0 0 25 0 1 0 1797431710 120066048 28793 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4501/statm): 29313 28793 145 145 0 29168 0
[pid=4501] vsize: 117252
Current children cumulated CPU time (s) 417.56
Current children cumulated vsize (Kb) 119376

[startup+430.039 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 4501
Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4497/statm): 531 226 485 147 0 384 0
[pid=4497] vsize: 2124
Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 30058 0 0 0 42565 185 0 0 25 0 1 0 1797431710 122347520 29352 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4501/statm): 29870 29352 145 145 0 29725 0
[pid=4501] vsize: 119480
Current children cumulated CPU time (s) 427.52
Current children cumulated vsize (Kb) 121604

[startup+440.04 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 4501
Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4497/statm): 531 226 485 147 0 384 0
[pid=4497] vsize: 2124
Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 30628 0 0 0 43555 188 0 0 25 0 1 0 1797431710 124674048 29922 4294967295 134512640 135094434 3221224432 3221223104 134556533 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4501/statm): 30438 29922 145 145 0 30293 0
[pid=4501] vsize: 121752
Current children cumulated CPU time (s) 437.45
Current children cumulated vsize (Kb) 123876

[startup+450.04 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 4501
Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4497/statm): 531 226 485 147 0 384 0
[pid=4497] vsize: 2124
Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 31319 0 0 0 44544 194 0 0 25 0 1 0 1797431710 127500288 30613 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4501/statm): 31128 30613 145 145 0 30983 0
[pid=4501] vsize: 124512
Current children cumulated CPU time (s) 447.4
Current children cumulated vsize (Kb) 126636

[startup+460.042 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 4501
Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4497/statm): 531 226 485 147 0 384 0
[pid=4497] vsize: 2124
Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 32011 0 0 0 45532 200 0 0 25 0 1 0 1797431710 130326528 31305 4294967295 134512640 135094434 3221224432 3221223024 134557416 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4501/statm): 31818 31305 145 145 0 31673 0
[pid=4501] vsize: 127272
Current children cumulated CPU time (s) 457.34
Current children cumulated vsize (Kb) 129396

[startup+470.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4501
Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4497/statm): 531 226 485 147 0 384 0
[pid=4497] vsize: 2124
Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 32652 0 0 0 46521 204 0 0 25 0 1 0 1797431710 132947968 31946 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4501/statm): 32458 31946 145 145 0 32313 0
[pid=4501] vsize: 129832
Current children cumulated CPU time (s) 467.27
Current children cumulated vsize (Kb) 131956

[startup+480.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4501
Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4497/statm): 531 226 485 147 0 384 0
[pid=4497] vsize: 2124
Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 33225 0 0 0 47513 208 0 0 25 0 1 0 1797431710 135290880 32519 4294967295 134512640 135094434 3221224432 3221223024 134557416 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4501/statm): 33030 32519 145 145 0 32885 0
[pid=4501] vsize: 132120
Current children cumulated CPU time (s) 477.23
Current children cumulated vsize (Kb) 134244

[startup+490.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4501
Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4497/statm): 531 226 485 147 0 384 0
[pid=4497] vsize: 2124
Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 33810 0 0 0 48506 212 0 0 25 0 1 0 1797431710 137687040 33104 4294967295 134512640 135094434 3221224432 3221223024 134557537 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4501/statm): 33615 33104 145 145 0 33470 0
[pid=4501] vsize: 134460
Current children cumulated CPU time (s) 487.2
Current children cumulated vsize (Kb) 136584

[startup+500.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4501
Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4497/statm): 531 226 485 147 0 384 0
[pid=4497] vsize: 2124
Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 34380 0 0 0 49497 216 0 0 25 0 1 0 1797431710 140017664 33674 4294967295 134512640 135094434 3221224432 3221223088 134557945 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4501/statm): 34184 33674 145 145 0 34039 0
[pid=4501] vsize: 136736
Current children cumulated CPU time (s) 497.15
Current children cumulated vsize (Kb) 138860

[startup+510.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4501
Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4497/statm): 531 226 485 147 0 384 0
[pid=4497] vsize: 2124
Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 34869 0 0 0 50489 219 0 0 25 0 1 0 1797431710 142012416 34163 4294967295 134512640 135094434 3221224432 3221223024 134551702 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4501/statm): 34671 34163 145 145 0 34526 0
[pid=4501] vsize: 138684
Current children cumulated CPU time (s) 507.1
Current children cumulated vsize (Kb) 140808

[startup+520.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4501
Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4497/statm): 531 226 485 147 0 384 0
[pid=4497] vsize: 2124
Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 35352 0 0 0 51482 222 0 0 25 0 1 0 1797431710 143986688 34646 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4501/statm): 35153 34646 145 145 0 35008 0
[pid=4501] vsize: 140612
Current children cumulated CPU time (s) 517.06
Current children cumulated vsize (Kb) 142736

[startup+530.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4501
Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4497/statm): 531 226 485 147 0 384 0
[pid=4497] vsize: 2124
Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 35818 0 0 0 52474 225 0 0 25 0 1 0 1797431710 145887232 35112 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4501/statm): 35617 35112 145 145 0 35472 0
[pid=4501] vsize: 142468
Current children cumulated CPU time (s) 527.01
Current children cumulated vsize (Kb) 144592

[startup+540.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4501
Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4497/statm): 531 226 485 147 0 384 0
[pid=4497] vsize: 2124
Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 36346 0 0 0 53466 229 0 0 25 0 1 0 1797431710 148037632 35640 4294967295 134512640 135094434 3221224432 3221223024 134557429 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4501/statm): 36142 35640 145 145 0 35997 0
[pid=4501] vsize: 144568
Current children cumulated CPU time (s) 536.97
Current children cumulated vsize (Kb) 146692

[startup+550.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4501
Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4497/statm): 531 226 485 147 0 384 0
[pid=4497] vsize: 2124
Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 36865 0 0 0 54458 233 0 0 25 0 1 0 1797431710 150155264 36159 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4501/statm): 36659 36159 145 145 0 36514 0
[pid=4501] vsize: 146636
Current children cumulated CPU time (s) 546.93
Current children cumulated vsize (Kb) 148760

[startup+560.052 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4501
Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4497/statm): 531 226 485 147 0 384 0
[pid=4497] vsize: 2124
Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 37164 0 0 0 55452 235 0 0 25 0 1 0 1797431710 151375872 36458 4294967295 134512640 135094434 3221224432 3221223024 134556964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4501/statm): 36957 36458 145 145 0 36812 0
[pid=4501] vsize: 147828
Current children cumulated CPU time (s) 556.89
Current children cumulated vsize (Kb) 149952

[startup+570.053 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4501
Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4497/statm): 531 226 485 147 0 384 0
[pid=4497] vsize: 2124
Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 37602 0 0 0 56445 238 0 0 25 0 1 0 1797431710 153165824 36896 4294967295 134512640 135094434 3221224432 3221223104 134556252 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4501/statm): 37394 36896 145 145 0 37249 0
[pid=4501] vsize: 149576
Current children cumulated CPU time (s) 566.85
Current children cumulated vsize (Kb) 151700

[startup+580.055 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4501
Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4497/statm): 531 226 485 147 0 384 0
[pid=4497] vsize: 2124
Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 38056 0 0 0 57437 242 0 0 25 0 1 0 1797431710 155017216 37350 4294967295 134512640 135094434 3221224432 3221223024 134557236 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4501/statm): 37846 37350 145 145 0 37701 0
[pid=4501] vsize: 151384
Current children cumulated CPU time (s) 576.81
Current children cumulated vsize (Kb) 153508

[startup+590.056 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4501
Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4497/statm): 531 226 485 147 0 384 0
[pid=4497] vsize: 2124
Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 38606 0 0 0 58428 246 0 0 25 0 1 0 1797431710 157261824 37900 4294967295 134512640 135094434 3221224432 3221223024 134556862 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4501/statm): 38394 37900 145 145 0 38249 0
[pid=4501] vsize: 153576
Current children cumulated CPU time (s) 586.76
Current children cumulated vsize (Kb) 155700

[startup+600.056 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4501
Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4497/statm): 531 226 485 147 0 384 0
[pid=4497] vsize: 2124
Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 39175 0 0 0 59419 249 0 0 25 0 1 0 1797431710 159588352 38469 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4501/statm): 38962 38469 145 145 0 38817 0
[pid=4501] vsize: 155848
Current children cumulated CPU time (s) 596.7
Current children cumulated vsize (Kb) 157972

[startup+610.057 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4501
Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4497/statm): 531 226 485 147 0 384 0
[pid=4497] vsize: 2124
Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 39456 0 0 0 60414 252 0 0 25 0 1 0 1797431710 160735232 38750 4294967295 134512640 135094434 3221224432 3221223024 134557518 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4501/statm): 39242 38750 145 145 0 39097 0
[pid=4501] vsize: 156968
Current children cumulated CPU time (s) 606.68
Current children cumulated vsize (Kb) 159092

[startup+620.058 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4501
Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4497/statm): 531 226 485 147 0 384 0
[pid=4497] vsize: 2124
Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 39456 0 0 0 61414 252 0 0 25 0 1 0 1797431710 160735232 38750 4294967295 134512640 135094434 3221224432 3221223088 134558007 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4501/statm): 39242 38750 145 145 0 39097 0
[pid=4501] vsize: 156968
Current children cumulated CPU time (s) 616.68
Current children cumulated vsize (Kb) 159092

[startup+630.059 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4501
Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4497/statm): 531 226 485 147 0 384 0
[pid=4497] vsize: 2124
Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 39456 0 0 0 62415 252 0 0 25 0 1 0 1797431710 160735232 38750 4294967295 134512640 135094434 3221224432 3221223104 134556450 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4501/statm): 39242 38750 145 145 0 39097 0
[pid=4501] vsize: 156968
Current children cumulated CPU time (s) 626.69
Current children cumulated vsize (Kb) 159092

[startup+640.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4501
Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4497/statm): 531 226 485 147 0 384 0
[pid=4497] vsize: 2124
Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 39456 0 0 0 63415 252 0 0 25 0 1 0 1797431710 160735232 38750 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4501/statm): 39242 38750 145 145 0 39097 0
[pid=4501] vsize: 156968
Current children cumulated CPU time (s) 636.69
Current children cumulated vsize (Kb) 159092

[startup+650.061 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4501
Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4497/statm): 531 226 485 147 0 384 0
[pid=4497] vsize: 2124
Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 39456 0 0 0 64415 252 0 0 25 0 1 0 1797431710 160735232 38750 4294967295 134512640 135094434 3221224432 3221223104 134555673 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4501/statm): 39242 38750 145 145 0 39097 0
[pid=4501] vsize: 156968
Current children cumulated CPU time (s) 646.69
Current children cumulated vsize (Kb) 159092

[startup+660.061 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4501
Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4497/statm): 531 226 485 147 0 384 0
[pid=4497] vsize: 2124
Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 39456 0 0 0 65415 252 0 0 25 0 1 0 1797431710 160735232 38750 4294967295 134512640 135094434 3221224432 3221223088 134558029 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4501/statm): 39242 38750 145 145 0 39097 0
[pid=4501] vsize: 156968
Current children cumulated CPU time (s) 656.69
Current children cumulated vsize (Kb) 159092

[startup+670.062 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4501
Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4497/statm): 531 226 485 147 0 384 0
[pid=4497] vsize: 2124
Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 39456 0 0 0 66415 253 0 0 25 0 1 0 1797431710 160735232 38750 4294967295 134512640 135094434 3221224432 3221223024 134557133 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4501/statm): 39242 38750 145 145 0 39097 0
[pid=4501] vsize: 156968
Current children cumulated CPU time (s) 666.7
Current children cumulated vsize (Kb) 159092

[startup+680.064 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4501
Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4497/statm): 531 226 485 147 0 384 0
[pid=4497] vsize: 2124
Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 39456 0 0 0 67414 253 0 0 25 0 1 0 1797431710 160735232 38750 4294967295 134512640 135094434 3221224432 3221223024 134557202 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4501/statm): 39242 38750 145 145 0 39097 0
[pid=4501] vsize: 156968
Current children cumulated CPU time (s) 676.69
Current children cumulated vsize (Kb) 159092

[startup+690.065 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4501
Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4497/statm): 531 226 485 147 0 384 0
[pid=4497] vsize: 2124
Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 39456 0 0 0 68414 253 0 0 25 0 1 0 1797431710 160735232 38750 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4501/statm): 39242 38750 145 145 0 39097 0
[pid=4501] vsize: 156968
Current children cumulated CPU time (s) 686.69
Current children cumulated vsize (Kb) 159092

[startup+700.066 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4501
Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4497/statm): 531 226 485 147 0 384 0
[pid=4497] vsize: 2124
Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 39456 0 0 0 69414 253 0 0 25 0 1 0 1797431710 160735232 38750 4294967295 134512640 135094434 3221224432 3221223024 134557416 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4501/statm): 39242 38750 145 145 0 39097 0
[pid=4501] vsize: 156968
Current children cumulated CPU time (s) 696.69
Current children cumulated vsize (Kb) 159092

[startup+710.067 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4501
Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4497/statm): 531 226 485 147 0 384 0
[pid=4497] vsize: 2124
Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 39456 0 0 0 70414 253 0 0 25 0 1 0 1797431710 160735232 38750 4294967295 134512640 135094434 3221224432 3221223024 134557421 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4501/statm): 39242 38750 145 145 0 39097 0
[pid=4501] vsize: 156968
Current children cumulated CPU time (s) 706.69
Current children cumulated vsize (Kb) 159092

[startup+720.066 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4501
Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4497/statm): 531 226 485 147 0 384 0
[pid=4497] vsize: 2124
Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 39456 0 0 0 71415 253 0 0 25 0 1 0 1797431710 160735232 38750 4294967295 134512640 135094434 3221224432 3221223024 134557002 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4501/statm): 39242 38750 145 145 0 39097 0
[pid=4501] vsize: 156968
Current children cumulated CPU time (s) 716.7
Current children cumulated vsize (Kb) 159092

[startup+730.067 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4501
Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4497/statm): 531 226 485 147 0 384 0
[pid=4497] vsize: 2124
Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 39456 0 0 0 72415 253 0 0 25 0 1 0 1797431710 160735232 38750 4294967295 134512640 135094434 3221224432 3221223024 134556853 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4501/statm): 39242 38750 145 145 0 39097 0
[pid=4501] vsize: 156968
Current children cumulated CPU time (s) 726.7
Current children cumulated vsize (Kb) 159092

[startup+740.068 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4501
Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4497/statm): 531 226 485 147 0 384 0
[pid=4497] vsize: 2124
Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 39456 0 0 0 73415 253 0 0 25 0 1 0 1797431710 160735232 38750 4294967295 134512640 135094434 3221224432 3221223088 134557996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4501/statm): 39242 38750 145 145 0 39097 0
[pid=4501] vsize: 156968
Current children cumulated CPU time (s) 736.7
Current children cumulated vsize (Kb) 159092

[startup+750.068 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4501
Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4497/statm): 531 226 485 147 0 384 0
[pid=4497] vsize: 2124
Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 39456 0 0 0 74415 253 0 0 25 0 1 0 1797431710 160735232 38750 4294967295 134512640 135094434 3221224432 3221223024 134551920 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4501/statm): 39242 38750 145 145 0 39097 0
[pid=4501] vsize: 156968
Current children cumulated CPU time (s) 746.7
Current children cumulated vsize (Kb) 159092

[startup+760.069 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4501
Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4497/statm): 531 226 485 147 0 384 0
[pid=4497] vsize: 2124
Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 39456 0 0 0 75415 253 0 0 25 0 1 0 1797431710 160735232 38750 4294967295 134512640 135094434 3221224432 3221223024 134556990 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4501/statm): 39242 38750 145 145 0 39097 0
[pid=4501] vsize: 156968
Current children cumulated CPU time (s) 756.7
Current children cumulated vsize (Kb) 159092

[startup+770.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4501
Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4497/statm): 531 226 485 147 0 384 0
[pid=4497] vsize: 2124
Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 39456 0 0 0 76415 253 0 0 25 0 1 0 1797431710 160735232 38750 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4501/statm): 39242 38750 145 145 0 39097 0
[pid=4501] vsize: 156968
Current children cumulated CPU time (s) 766.7
Current children cumulated vsize (Kb) 159092

[startup+780.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4501
Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4497/statm): 531 226 485 147 0 384 0
[pid=4497] vsize: 2124
Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 39456 0 0 0 77416 253 0 0 25 0 1 0 1797431710 160735232 38750 4294967295 134512640 135094434 3221224432 3221223088 134558178 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4501/statm): 39242 38750 145 145 0 39097 0
[pid=4501] vsize: 156968
Current children cumulated CPU time (s) 776.71
Current children cumulated vsize (Kb) 159092

[startup+790.071 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4501
Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4497/statm): 531 226 485 147 0 384 0
[pid=4497] vsize: 2124
Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 39456 0 0 0 78416 253 0 0 25 0 1 0 1797431710 160735232 38750 4294967295 134512640 135094434 3221224432 3221223024 134557230 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4501/statm): 39242 38750 145 145 0 39097 0
[pid=4501] vsize: 156968
Current children cumulated CPU time (s) 786.71
Current children cumulated vsize (Kb) 159092

[startup+800.071 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4501
Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4497/statm): 531 226 485 147 0 384 0
[pid=4497] vsize: 2124
Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 39456 0 0 0 79416 254 0 0 25 0 1 0 1797431710 160735232 38750 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4501/statm): 39242 38750 145 145 0 39097 0
[pid=4501] vsize: 156968
Current children cumulated CPU time (s) 796.72
Current children cumulated vsize (Kb) 159092

[startup+810.072 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4501
Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4497/statm): 531 226 485 147 0 384 0
[pid=4497] vsize: 2124
Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 39456 0 0 0 80416 254 0 0 25 0 1 0 1797431710 160735232 38750 4294967295 134512640 135094434 3221224432 3221223024 134556851 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4501/statm): 39242 38750 145 145 0 39097 0
[pid=4501] vsize: 156968
Current children cumulated CPU time (s) 806.72
Current children cumulated vsize (Kb) 159092

[startup+820.073 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4501
Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4497/statm): 531 226 485 147 0 384 0
[pid=4497] vsize: 2124
Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 39456 0 0 0 81416 254 0 0 25 0 1 0 1797431710 160735232 38750 4294967295 134512640 135094434 3221224432 3221223024 134557196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4501/statm): 39242 38750 145 145 0 39097 0
[pid=4501] vsize: 156968
Current children cumulated CPU time (s) 816.72
Current children cumulated vsize (Kb) 159092

[startup+830.074 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4501
Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4497/statm): 531 226 485 147 0 384 0
[pid=4497] vsize: 2124
Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 39456 0 0 0 82416 254 0 0 25 0 1 0 1797431710 160735232 38750 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4501/statm): 39242 38750 145 145 0 39097 0
[pid=4501] vsize: 156968
Current children cumulated CPU time (s) 826.72
Current children cumulated vsize (Kb) 159092

[startup+840.074 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4501
Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4497/statm): 531 226 485 147 0 384 0
[pid=4497] vsize: 2124
Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 39456 0 0 0 83417 254 0 0 25 0 1 0 1797431710 160735232 38750 4294967295 134512640 135094434 3221224432 3221223024 134556773 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4501/statm): 39242 38750 145 145 0 39097 0
[pid=4501] vsize: 156968
Current children cumulated CPU time (s) 836.73
Current children cumulated vsize (Kb) 159092

[startup+850.075 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4501
Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4497/statm): 531 226 485 147 0 384 0
[pid=4497] vsize: 2124
Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 39456 0 0 0 84417 254 0 0 25 0 1 0 1797431710 160735232 38750 4294967295 134512640 135094434 3221224432 3221223088 134557840 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4501/statm): 39242 38750 145 145 0 39097 0
[pid=4501] vsize: 156968
Current children cumulated CPU time (s) 846.73
Current children cumulated vsize (Kb) 159092

[startup+860.076 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4501
Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4497/statm): 531 226 485 147 0 384 0
[pid=4497] vsize: 2124
Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 39456 0 0 0 85417 254 0 0 25 0 1 0 1797431710 160735232 38750 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4501/statm): 39242 38750 145 145 0 39097 0
[pid=4501] vsize: 156968
Current children cumulated CPU time (s) 856.73
Current children cumulated vsize (Kb) 159092

[startup+870.076 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4501
Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4497/statm): 531 226 485 147 0 384 0
[pid=4497] vsize: 2124
Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 39456 0 0 0 86417 254 0 0 25 0 1 0 1797431710 160735232 38750 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4501/statm): 39242 38750 145 145 0 39097 0
[pid=4501] vsize: 156968
Current children cumulated CPU time (s) 866.73
Current children cumulated vsize (Kb) 159092

[startup+880.078 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4501
Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4497/statm): 531 226 485 147 0 384 0
[pid=4497] vsize: 2124
Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 39456 0 0 0 87417 254 0 0 25 0 1 0 1797431710 160735232 38750 4294967295 134512640 135094434 3221224432 3221223104 134556252 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4501/statm): 39242 38750 145 145 0 39097 0
[pid=4501] vsize: 156968
Current children cumulated CPU time (s) 876.73
Current children cumulated vsize (Kb) 159092

[startup+890.079 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4501
Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4497/statm): 531 226 485 147 0 384 0
[pid=4497] vsize: 2124
Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 39456 0 0 0 88418 254 0 0 25 0 1 0 1797431710 160735232 38750 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4501/statm): 39242 38750 145 145 0 39097 0
[pid=4501] vsize: 156968
Current children cumulated CPU time (s) 886.74
Current children cumulated vsize (Kb) 159092

[startup+900.078 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4501
Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4497/statm): 531 226 485 147 0 384 0
[pid=4497] vsize: 2124
Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 39456 0 0 0 89418 254 0 0 25 0 1 0 1797431710 160735232 38750 4294967295 134512640 135094434 3221224432 3221223088 134558178 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4501/statm): 39242 38750 145 145 0 39097 0
[pid=4501] vsize: 156968
Current children cumulated CPU time (s) 896.74
Current children cumulated vsize (Kb) 159092

[startup+910.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4501
Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4497/statm): 531 226 485 147 0 384 0
[pid=4497] vsize: 2124
Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 39456 0 0 0 90418 254 0 0 25 0 1 0 1797431710 160735232 38750 4294967295 134512640 135094434 3221224432 3221223024 134556990 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4501/statm): 39242 38750 145 145 0 39097 0
[pid=4501] vsize: 156968
Current children cumulated CPU time (s) 906.74
Current children cumulated vsize (Kb) 159092

[startup+920.081 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4501
Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4497/statm): 531 226 485 147 0 384 0
[pid=4497] vsize: 2124
Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 39456 0 0 0 91418 254 0 0 25 0 1 0 1797431710 160735232 38750 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4501/statm): 39242 38750 145 145 0 39097 0
[pid=4501] vsize: 156968
Current children cumulated CPU time (s) 916.74
Current children cumulated vsize (Kb) 159092

[startup+930.082 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4501
Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4497/statm): 531 226 485 147 0 384 0
[pid=4497] vsize: 2124
Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 39456 0 0 0 92419 254 0 0 25 0 1 0 1797431710 160735232 38750 4294967295 134512640 135094434 3221224432 3221223104 134555758 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4501/statm): 39242 38750 145 145 0 39097 0
[pid=4501] vsize: 156968
Current children cumulated CPU time (s) 926.75
Current children cumulated vsize (Kb) 159092

[startup+940.083 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4501
Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4497/statm): 531 226 485 147 0 384 0
[pid=4497] vsize: 2124
Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 39456 0 0 0 93419 254 0 0 25 0 1 0 1797431710 160735232 38750 4294967295 134512640 135094434 3221224432 3221223056 134562098 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4501/statm): 39242 38750 145 145 0 39097 0
[pid=4501] vsize: 156968
Current children cumulated CPU time (s) 936.75
Current children cumulated vsize (Kb) 159092

[startup+950.084 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4501
Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4497/statm): 531 226 485 147 0 384 0
[pid=4497] vsize: 2124
Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 39456 0 0 0 94419 254 0 0 25 0 1 0 1797431710 160735232 38750 4294967295 134512640 135094434 3221224432 3221223068 134557639 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4501/statm): 39242 38750 145 145 0 39097 0
[pid=4501] vsize: 156968
Current children cumulated CPU time (s) 946.75
Current children cumulated vsize (Kb) 159092

[startup+960.085 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4501
Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4497/statm): 531 226 485 147 0 384 0
[pid=4497] vsize: 2124
Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 39456 0 0 0 95419 254 0 0 25 0 1 0 1797431710 160735232 38750 4294967295 134512640 135094434 3221224432 3221223024 134557522 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4501/statm): 39242 38750 145 145 0 39097 0
[pid=4501] vsize: 156968
Current children cumulated CPU time (s) 956.75
Current children cumulated vsize (Kb) 159092

[startup+970.085 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4501
Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4497/statm): 531 226 485 147 0 384 0
[pid=4497] vsize: 2124
Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 39456 0 0 0 96419 254 0 0 25 0 1 0 1797431710 160735232 38750 4294967295 134512640 135094434 3221224432 3221223088 134557866 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4501/statm): 39242 38750 145 145 0 39097 0
[pid=4501] vsize: 156968
Current children cumulated CPU time (s) 966.75
Current children cumulated vsize (Kb) 159092

[startup+980.087 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4501
Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4497/statm): 531 226 485 147 0 384 0
[pid=4497] vsize: 2124
Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 39456 0 0 0 97420 254 0 0 25 0 1 0 1797431710 160735232 38750 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4501/statm): 39242 38750 145 145 0 39097 0
[pid=4501] vsize: 156968
Current children cumulated CPU time (s) 976.76
Current children cumulated vsize (Kb) 159092

[startup+990.088 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4501
Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4497/statm): 531 226 485 147 0 384 0
[pid=4497] vsize: 2124
Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 39456 0 0 0 98420 254 0 0 25 0 1 0 1797431710 160735232 38750 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4501/statm): 39242 38750 145 145 0 39097 0
[pid=4501] vsize: 156968
Current children cumulated CPU time (s) 986.76
Current children cumulated vsize (Kb) 159092

[startup+1000.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4501
Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4497/statm): 531 226 485 147 0 384 0
[pid=4497] vsize: 2124
Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 39456 0 0 0 99420 254 0 0 25 0 1 0 1797431710 160735232 38750 4294967295 134512640 135094434 3221224432 3221223088 134558221 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4501/statm): 39242 38750 145 145 0 39097 0
[pid=4501] vsize: 156968
Current children cumulated CPU time (s) 996.76
Current children cumulated vsize (Kb) 159092

[startup+1010.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4501
Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4497/statm): 531 226 485 147 0 384 0
[pid=4497] vsize: 2124
Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 39456 0 0 0 100420 254 0 0 25 0 1 0 1797431710 160735232 38750 4294967295 134512640 135094434 3221224432 3221223024 134556904 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4501/statm): 39242 38750 145 145 0 39097 0
[pid=4501] vsize: 156968
Current children cumulated CPU time (s) 1006.76
Current children cumulated vsize (Kb) 159092

[startup+1020.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4501
Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4497/statm): 531 226 485 147 0 384 0
[pid=4497] vsize: 2124
Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 39456 0 0 0 101421 254 0 0 25 0 1 0 1797431710 160735232 38750 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4501/statm): 39242 38750 145 145 0 39097 0
[pid=4501] vsize: 156968
Current children cumulated CPU time (s) 1016.77
Current children cumulated vsize (Kb) 159092

[startup+1030.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4501
Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4497/statm): 531 226 485 147 0 384 0
[pid=4497] vsize: 2124
Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 39456 0 0 0 102421 254 0 0 25 0 1 0 1797431710 160735232 38750 4294967295 134512640 135094434 3221224432 3221223060 134557564 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4501/statm): 39242 38750 145 145 0 39097 0
[pid=4501] vsize: 156968
Current children cumulated CPU time (s) 1026.77
Current children cumulated vsize (Kb) 159092

[startup+1040.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4501
Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4497/statm): 531 226 485 147 0 384 0
[pid=4497] vsize: 2124
Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 39456 0 0 0 103421 254 0 0 25 0 1 0 1797431710 160735232 38750 4294967295 134512640 135094434 3221224432 3221223024 134557002 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4501/statm): 39242 38750 145 145 0 39097 0
[pid=4501] vsize: 156968
Current children cumulated CPU time (s) 1036.77
Current children cumulated vsize (Kb) 159092

[startup+1050.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4501
Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4497/statm): 531 226 485 147 0 384 0
[pid=4497] vsize: 2124
Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 39456 0 0 0 104421 254 0 0 25 0 1 0 1797431710 160735232 38750 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4501/statm): 39242 38750 145 145 0 39097 0
[pid=4501] vsize: 156968
Current children cumulated CPU time (s) 1046.77
Current children cumulated vsize (Kb) 159092

[startup+1060.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4501
Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4497/statm): 531 226 485 147 0 384 0
[pid=4497] vsize: 2124
Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 39456 0 0 0 105419 256 0 0 25 0 1 0 1797431710 160735232 38750 4294967295 134512640 135094434 3221224432 3221223088 134558178 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4501/statm): 39242 38750 145 145 0 39097 0
[pid=4501] vsize: 156968
Current children cumulated CPU time (s) 1056.77
Current children cumulated vsize (Kb) 159092

[startup+1070.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4501
Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4497/statm): 531 226 485 147 0 384 0
[pid=4497] vsize: 2124
Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 39456 0 0 0 106418 256 0 0 25 0 1 0 1797431710 160735232 38750 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4501/statm): 39242 38750 145 145 0 39097 0
[pid=4501] vsize: 156968
Current children cumulated CPU time (s) 1066.76
Current children cumulated vsize (Kb) 159092

[startup+1080.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4501
Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4497/statm): 531 226 485 147 0 384 0
[pid=4497] vsize: 2124
Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 39456 0 0 0 107418 257 0 0 25 0 1 0 1797431710 160735232 38750 4294967295 134512640 135094434 3221224432 3221223088 134558227 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4501/statm): 39242 38750 145 145 0 39097 0
[pid=4501] vsize: 156968
Current children cumulated CPU time (s) 1076.77
Current children cumulated vsize (Kb) 159092

[startup+1090.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4501
Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4497/statm): 531 226 485 147 0 384 0
[pid=4497] vsize: 2124
Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 39456 0 0 0 108418 257 0 0 25 0 1 0 1797431710 160735232 38750 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4501/statm): 39242 38750 145 145 0 39097 0
[pid=4501] vsize: 156968
Current children cumulated CPU time (s) 1086.77
Current children cumulated vsize (Kb) 159092

[startup+1100.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4501
Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4497/statm): 531 226 485 147 0 384 0
[pid=4497] vsize: 2124
Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 39456 0 0 0 109418 257 0 0 25 0 1 0 1797431710 160735232 38750 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4501/statm): 39242 38750 145 145 0 39097 0
[pid=4501] vsize: 156968
Current children cumulated CPU time (s) 1096.77
Current children cumulated vsize (Kb) 159092

[startup+1110.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4501
Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4497/statm): 531 226 485 147 0 384 0
[pid=4497] vsize: 2124
Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 39535 0 0 0 110418 257 0 0 25 0 1 0 1797431710 161058816 38829 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4501/statm): 39321 38829 145 145 0 39176 0
[pid=4501] vsize: 157284
Current children cumulated CPU time (s) 1106.77
Current children cumulated vsize (Kb) 159408

[startup+1120.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4501
Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4497/statm): 531 226 485 147 0 384 0
[pid=4497] vsize: 2124
Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 39889 0 0 0 111412 260 0 0 25 0 1 0 1797431710 162508800 39183 4294967295 134512640 135094434 3221224432 3221223024 134557028 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4501/statm): 39675 39183 145 145 0 39530 0
[pid=4501] vsize: 158700
Current children cumulated CPU time (s) 1116.74
Current children cumulated vsize (Kb) 160824

[startup+1130.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4501
Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4497/statm): 531 226 485 147 0 384 0
[pid=4497] vsize: 2124
Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 40297 0 0 0 112407 262 0 0 25 0 1 0 1797431710 164179968 39591 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4501/statm): 40083 39591 145 145 0 39938 0
[pid=4501] vsize: 160332
Current children cumulated CPU time (s) 1126.71
Current children cumulated vsize (Kb) 162456

[startup+1140.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4501
Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4497/statm): 531 226 485 147 0 384 0
[pid=4497] vsize: 2124
Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) T 4497 4497 31915 0 -1 0 40962 0 0 0 113400 265 0 0 25 0 1 0 1797431710 166895616 40256 4294967295 134512640 135094434 3221224432 3221222796 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/4501/statm): 40746 40256 145 145 0 40601 0
[pid=4501] vsize: 162984
Current children cumulated CPU time (s) 1136.67
Current children cumulated vsize (Kb) 165108

[startup+1150.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4501
Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4497/statm): 531 226 485 147 0 384 0
[pid=4497] vsize: 2124
Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 41488 0 0 0 114394 267 0 0 25 0 1 0 1797431710 169050112 40782 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4501/statm): 41272 40782 145 145 0 41127 0
[pid=4501] vsize: 165088
Current children cumulated CPU time (s) 1146.63
Current children cumulated vsize (Kb) 167212

[startup+1160.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4501
Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4497/statm): 531 226 485 147 0 384 0
[pid=4497] vsize: 2124
Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 42013 0 0 0 115388 270 0 0 25 0 1 0 1797431710 171200512 41307 4294967295 134512640 135094434 3221224432 3221223056 134557650 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4501/statm): 41797 41307 145 145 0 41652 0
[pid=4501] vsize: 167188
Current children cumulated CPU time (s) 1156.6
Current children cumulated vsize (Kb) 169312

[startup+1170.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4501
Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4497/statm): 531 226 485 147 0 384 0
[pid=4497] vsize: 2124
Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 42503 0 0 0 116381 273 0 0 25 0 1 0 1797431710 173203456 41797 4294967295 134512640 135094434 3221224432 3221223024 134557273 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4501/statm): 42286 41797 145 145 0 42141 0
[pid=4501] vsize: 169144
Current children cumulated CPU time (s) 1166.56
Current children cumulated vsize (Kb) 171268

[startup+1180.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4501
Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4497/statm): 531 226 485 147 0 384 0
[pid=4497] vsize: 2124
Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 42982 0 0 0 117374 276 0 0 25 0 1 0 1797431710 175157248 42276 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4501/statm): 42763 42276 145 145 0 42618 0
[pid=4501] vsize: 171052
Current children cumulated CPU time (s) 1176.52
Current children cumulated vsize (Kb) 173176

[startup+1190.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4501
Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4497/statm): 531 226 485 147 0 384 0
[pid=4497] vsize: 2124
Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) T 4497 4497 31915 0 -1 0 43690 0 0 0 118364 280 0 0 25 0 1 0 1797431710 178053120 42984 4294967295 134512640 135094434 3221224432 3221222796 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/4501/statm): 43470 42984 145 145 0 43325 0
[pid=4501] vsize: 173880
Current children cumulated CPU time (s) 1186.46
Current children cumulated vsize (Kb) 176004

[startup+1200.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4501
Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4497/statm): 531 226 485 147 0 384 0
[pid=4497] vsize: 2124
Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 44425 0 0 0 119355 284 0 0 25 0 1 0 1797431710 181059584 43719 4294967295 134512640 135094434 3221224432 3221223024 134557421 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4501/statm): 44204 43719 145 145 0 44059 0
[pid=4501] vsize: 176816
Current children cumulated CPU time (s) 1196.41
Current children cumulated vsize (Kb) 178940

[startup+1210.1 s]
Raw data (loadavg): 1.07 0.99 0.91 2/57 4501
Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4497/statm): 531 226 485 147 0 384 0
[pid=4497] vsize: 2124
Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 45047 0 0 0 120347 287 0 0 25 0 1 0 1797431710 183603200 44341 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4501/statm): 44825 44341 145 145 0 44680 0
[pid=4501] vsize: 179300
Current children cumulated CPU time (s) 1206.36
Current children cumulated vsize (Kb) 181424



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.1 s]
Raw data (loadavg): 1.07 0.99 0.91 2/57 4501
Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4497/statm): 531 226 485 147 0 384 0
[pid=4497] vsize: 2124
Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 45047 0 0 0 120348 287 0 0 25 0 1 0 1797431710 183603200 44341 4294967295 134512640 135094434 3221224432 3221223088 134558235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4501/statm): 44825 44341 145 145 0 44680 0
[pid=4501] vsize: 179300
Current children cumulated CPU time (s) 1206.37
Current children cumulated vsize (Kb) 181424

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

Child status: 0
Real time (s): 1210.19
CPU time (s): 1206.44
CPU user time (s): 1203.48
CPU system time (s): 2.95755
CPU usage (%): 99.69
Max. virtual memory (cumulated for all children) (Kb): 181424

Verifier Data

ERROR: no interpretation found !