Some explanations

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

General information on the benchmark

Namemps-v2-20-10/MIPLIB/miplib/normalized-mps-v2-20-10-mod010.opb
MD5SUM4f0cac14ed3568050c2c57bb69fdb664
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 3873

Launcher Data

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

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        886160 kB
Buffers:         37220 kB
Cached:          78840 kB
SwapCached:        764 kB
Active:          70312 kB
Inactive:        48328 kB
HighTotal:      131008 kB
HighFree:        49644 kB
LowTotal:       903652 kB
LowFree:        836516 kB
SwapTotal:     2097892 kB
SwapFree:      2096616 kB
Dirty:              40 kB
Writeback:           0 kB
Mapped:           5728 kB
Slab:            24240 kB
Committed_AS:    64168 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-09-19 03:34:52 (client local time) WITH STATUS 0 IN 1206.52 SECONDS
stats: 2869 7 1206.52 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/15322/stat): 15322 (minisat+_script) R 15321 15322 28974 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1846558809 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 0 0 0
Raw data (/proc/15322/statm): 174 3 169 147 0 27 0
[pid=15322] 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=15323
New process pid=15324
New process pid=15325
execve syscall for /bin/sed executable
One traced child (pid=15324) 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=15325) exited with status: 0
One traced child (pid=15323) exited with status: 0
New process pid=15326
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc27/normalized-mps-v2-20-10-mod010.opb

[startup+10.0042 s]
Raw data (loadavg): 0.94 0.97 0.95 2/57 15326
Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15322/statm): 531 226 485 147 0 384 0
[pid=15322] vsize: 2124
Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 5203 0 0 0 957 21 0 0 25 0 1 0 1846558814 20291584 4497 4294967295 134512640 135094434 3221224432 3221223024 134556984 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15326/statm): 4954 4497 145 145 0 4809 0
[pid=15326] vsize: 19816
Current children cumulated CPU time (s) 9.78
Current children cumulated vsize (Kb) 21940

[startup+20.005 s]
Raw data (loadavg): 0.95 0.97 0.95 2/57 15326
Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15322/statm): 531 226 485 147 0 384 0
[pid=15322] vsize: 2124
Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 5771 0 0 0 1948 24 0 0 25 0 1 0 1846558814 22618112 5065 4294967295 134512640 135094434 3221224432 3221223056 134557662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15326/statm): 5522 5065 145 145 0 5377 0
[pid=15326] vsize: 22088
Current children cumulated CPU time (s) 19.72
Current children cumulated vsize (Kb) 24212

[startup+30.0059 s]
Raw data (loadavg): 0.95 0.97 0.95 2/57 15326
Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15322/statm): 531 226 485 147 0 384 0
[pid=15322] vsize: 2124
Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 6319 0 0 0 2940 27 0 0 25 0 1 0 1846558814 24887296 5613 4294967295 134512640 135094434 3221224432 3221223056 134557737 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15326/statm): 6076 5613 145 145 0 5931 0
[pid=15326] vsize: 24304
Current children cumulated CPU time (s) 29.67
Current children cumulated vsize (Kb) 26428

[startup+40.0077 s]
Raw data (loadavg): 0.96 0.97 0.95 2/57 15326
Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15322/statm): 531 226 485 147 0 384 0
[pid=15322] vsize: 2124
Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 7066 0 0 0 3929 31 0 0 25 0 1 0 1846558814 27934720 6360 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15326/statm): 6820 6360 145 145 0 6675 0
[pid=15326] vsize: 27280
Current children cumulated CPU time (s) 39.6
Current children cumulated vsize (Kb) 29404

[startup+50.0085 s]
Raw data (loadavg): 0.97 0.97 0.95 2/57 15326
Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15322/statm): 531 226 485 147 0 384 0
[pid=15322] vsize: 2124
Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 7804 0 0 0 4918 36 0 0 25 0 1 0 1846558814 30949376 7098 4294967295 134512640 135094434 3221224432 3221223024 134556862 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15326/statm): 7556 7098 145 145 0 7411 0
[pid=15326] vsize: 30224
Current children cumulated CPU time (s) 49.54
Current children cumulated vsize (Kb) 32348

[startup+60.0104 s]
Raw data (loadavg): 0.97 0.97 0.95 2/57 15326
Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15322/statm): 531 226 485 147 0 384 0
[pid=15322] vsize: 2124
Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 8427 0 0 0 5907 40 0 0 25 0 1 0 1846558814 33550336 7721 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15326/statm): 8191 7721 145 145 0 8046 0
[pid=15326] vsize: 32764
Current children cumulated CPU time (s) 59.47
Current children cumulated vsize (Kb) 34888

[startup+70.0122 s]
Raw data (loadavg): 0.97 0.97 0.95 2/57 15326
Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15322/statm): 531 226 485 147 0 384 0
[pid=15322] vsize: 2124
Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 9061 0 0 0 6897 45 0 0 25 0 1 0 1846558814 36139008 8355 4294967295 134512640 135094434 3221224432 3221223056 134562104 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15326/statm): 8823 8355 145 145 0 8678 0
[pid=15326] vsize: 35292
Current children cumulated CPU time (s) 69.42
Current children cumulated vsize (Kb) 37416

[startup+80.013 s]
Raw data (loadavg): 0.98 0.97 0.95 2/57 15326
Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15322/statm): 531 226 485 147 0 384 0
[pid=15322] vsize: 2124
Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 9652 0 0 0 7886 48 0 0 25 0 1 0 1846558814 38551552 8946 4294967295 134512640 135094434 3221224432 3221223024 134556789 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15326/statm): 9412 8946 145 145 0 9267 0
[pid=15326] vsize: 37648
Current children cumulated CPU time (s) 79.34
Current children cumulated vsize (Kb) 39772

[startup+90.0138 s]
Raw data (loadavg): 0.98 0.97 0.95 2/57 15326
Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15322/statm): 531 226 485 147 0 384 0
[pid=15322] vsize: 2124
Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 10247 0 0 0 8876 52 0 0 25 0 1 0 1846558814 40988672 9541 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15326/statm): 10007 9541 145 145 0 9862 0
[pid=15326] vsize: 40028
Current children cumulated CPU time (s) 89.28
Current children cumulated vsize (Kb) 42152

[startup+100.015 s]
Raw data (loadavg): 0.98 0.97 0.95 2/57 15326
Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15322/statm): 531 226 485 147 0 384 0
[pid=15322] vsize: 2124
Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 10776 0 0 0 9868 56 0 0 25 0 1 0 1846558814 43155456 10070 4294967295 134512640 135094434 3221224432 3221223088 134558026 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15326/statm): 10536 10070 145 145 0 10391 0
[pid=15326] vsize: 42144
Current children cumulated CPU time (s) 99.24
Current children cumulated vsize (Kb) 44268

[startup+110.017 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 15326
Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15322/statm): 531 226 485 147 0 384 0
[pid=15322] vsize: 2124
Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 11310 0 0 0 10862 58 0 0 25 0 1 0 1846558814 45350912 10604 4294967295 134512640 135094434 3221224432 3221223024 134557037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15326/statm): 11072 10604 145 145 0 10927 0
[pid=15326] vsize: 44288
Current children cumulated CPU time (s) 109.2
Current children cumulated vsize (Kb) 46412

[startup+120.018 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 15326
Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15322/statm): 531 226 485 147 0 384 0
[pid=15322] vsize: 2124
Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 11878 0 0 0 11852 62 0 0 25 0 1 0 1846558814 47681536 11172 4294967295 134512640 135094434 3221224432 3221223088 134557860 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15326/statm): 11641 11172 145 145 0 11496 0
[pid=15326] vsize: 46564
Current children cumulated CPU time (s) 119.14
Current children cumulated vsize (Kb) 48688

[startup+130.019 s]
Raw data (loadavg): 0.99 0.97 0.95 1/57 15326
Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15322/statm): 531 226 485 147 0 384 0
[pid=15322] vsize: 2124
Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) T 15322 15322 28974 0 -1 0 12561 0 0 0 12839 68 0 0 25 0 1 0 1846558814 50470912 11855 4294967295 134512640 135094434 3221224432 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/15326/statm): 12322 11855 145 145 0 12177 0
[pid=15326] vsize: 49288
Current children cumulated CPU time (s) 129.07
Current children cumulated vsize (Kb) 51412

[startup+140.02 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 15326
Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15322/statm): 531 226 485 147 0 384 0
[pid=15322] vsize: 2124
Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 13254 0 0 0 13828 73 0 0 25 0 1 0 1846558814 53301248 12548 4294967295 134512640 135094434 3221224432 3221223056 134557604 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15326/statm): 13013 12548 145 145 0 12868 0
[pid=15326] vsize: 52052
Current children cumulated CPU time (s) 139.01
Current children cumulated vsize (Kb) 54176

[startup+150.021 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 15326
Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15322/statm): 531 226 485 147 0 384 0
[pid=15322] vsize: 2124
Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 13895 0 0 0 14818 77 0 0 25 0 1 0 1846558814 55922688 13189 4294967295 134512640 135094434 3221224432 3221223024 134557202 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15326/statm): 13653 13189 145 145 0 13508 0
[pid=15326] vsize: 54612
Current children cumulated CPU time (s) 148.95
Current children cumulated vsize (Kb) 56736

[startup+160.022 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 15326
Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15322/statm): 531 226 485 147 0 384 0
[pid=15322] vsize: 2124
Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 14531 0 0 0 15809 81 0 0 25 0 1 0 1846558814 58654720 13825 4294967295 134512640 135094434 3221224432 3221223088 134557882 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15326/statm): 14320 13825 145 145 0 14175 0
[pid=15326] vsize: 57280
Current children cumulated CPU time (s) 158.9
Current children cumulated vsize (Kb) 59404

[startup+170.022 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 15326
Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15322/statm): 531 226 485 147 0 384 0
[pid=15322] vsize: 2124
Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 15137 0 0 0 16799 85 0 0 25 0 1 0 1846558814 61128704 14431 4294967295 134512640 135094434 3221224432 3221223024 134557213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15326/statm): 14924 14431 145 145 0 14779 0
[pid=15326] vsize: 59696
Current children cumulated CPU time (s) 168.84
Current children cumulated vsize (Kb) 61820

[startup+180.022 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 15326
Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15322/statm): 531 226 485 147 0 384 0
[pid=15322] vsize: 2124
Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 15728 0 0 0 17791 89 0 0 25 0 1 0 1846558814 63541248 15022 4294967295 134512640 135094434 3221224432 3221223024 134556812 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15326/statm): 15513 15022 145 145 0 15368 0
[pid=15326] vsize: 62052
Current children cumulated CPU time (s) 178.8
Current children cumulated vsize (Kb) 64176

[startup+190.023 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 15326
Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15322/statm): 531 226 485 147 0 384 0
[pid=15322] vsize: 2124
Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 16310 0 0 0 18781 93 0 0 25 0 1 0 1846558814 65921024 15604 4294967295 134512640 135094434 3221224432 3221223024 134556949 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15326/statm): 16094 15604 145 145 0 15949 0
[pid=15326] vsize: 64376
Current children cumulated CPU time (s) 188.74
Current children cumulated vsize (Kb) 66500

[startup+200.024 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 15326
Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15322/statm): 531 226 485 147 0 384 0
[pid=15322] vsize: 2124
Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 16870 0 0 0 19772 97 0 0 25 0 1 0 1846558814 68202496 16164 4294967295 134512640 135094434 3221224432 3221223088 134557813 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15326/statm): 16651 16164 145 145 0 16506 0
[pid=15326] vsize: 66604
Current children cumulated CPU time (s) 198.69
Current children cumulated vsize (Kb) 68728

[startup+210.026 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 15326
Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15322/statm): 531 226 485 147 0 384 0
[pid=15322] vsize: 2124
Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 17670 0 0 0 20760 102 0 0 25 0 1 0 1846558814 71471104 16964 4294967295 134512640 135094434 3221224432 3221223024 134557037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15326/statm): 17449 16964 145 145 0 17304 0
[pid=15326] vsize: 69796
Current children cumulated CPU time (s) 208.62
Current children cumulated vsize (Kb) 71920

[startup+220.027 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 15326
Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15322/statm): 531 226 485 147 0 384 0
[pid=15322] vsize: 2124
Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 18381 0 0 0 21751 105 0 0 25 0 1 0 1846558814 74379264 17675 4294967295 134512640 135094434 3221224432 3221223024 134556817 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15326/statm): 18159 17675 145 145 0 18014 0
[pid=15326] vsize: 72636
Current children cumulated CPU time (s) 218.56
Current children cumulated vsize (Kb) 74760

[startup+230.026 s]
Raw data (loadavg): 0.99 0.97 0.95 1/57 15326
Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15322/statm): 531 226 485 147 0 384 0
[pid=15322] vsize: 2124
Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) T 15322 15322 28974 0 -1 0 19045 0 0 0 22740 109 0 0 25 0 1 0 1846558814 77094912 18339 4294967295 134512640 135094434 3221224432 3221222780 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/15326/statm): 18822 18339 145 145 0 18677 0
[pid=15326] vsize: 75288
Current children cumulated CPU time (s) 228.49
Current children cumulated vsize (Kb) 77412

[startup+240.027 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 15326
Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15322/statm): 531 226 485 147 0 384 0
[pid=15322] vsize: 2124
Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 19650 0 0 0 23730 113 0 0 25 0 1 0 1846558814 79564800 18944 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15326/statm): 19425 18944 145 145 0 19280 0
[pid=15326] vsize: 77700
Current children cumulated CPU time (s) 238.43
Current children cumulated vsize (Kb) 79824

[startup+250.028 s]
Raw data (loadavg): 0.99 0.97 0.95 1/57 15326
Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15322/statm): 531 226 485 147 0 384 0
[pid=15322] vsize: 2124
Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) T 15322 15322 28974 0 -1 0 20272 0 0 0 24722 117 0 0 25 0 1 0 1846558814 82104320 19566 4294967295 134512640 135094434 3221224432 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/15326/statm): 20045 19566 145 145 0 19900 0
[pid=15326] vsize: 80180
Current children cumulated CPU time (s) 248.39
Current children cumulated vsize (Kb) 82304

[startup+260.03 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 15326
Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15322/statm): 531 226 485 147 0 384 0
[pid=15322] vsize: 2124
Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 20888 0 0 0 25712 121 0 0 25 0 1 0 1846558814 84627456 20182 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15326/statm): 20661 20182 145 145 0 20516 0
[pid=15326] vsize: 82644
Current children cumulated CPU time (s) 258.33
Current children cumulated vsize (Kb) 84768

[startup+270.031 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 15326
Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15322/statm): 531 226 485 147 0 384 0
[pid=15322] vsize: 2124
Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 21442 0 0 0 26704 124 0 0 25 0 1 0 1846558814 86908928 20736 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15326/statm): 21218 20736 145 145 0 21073 0
[pid=15326] vsize: 84872
Current children cumulated CPU time (s) 268.28
Current children cumulated vsize (Kb) 86996

[startup+280.031 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 15326
Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15322/statm): 531 226 485 147 0 384 0
[pid=15322] vsize: 2124
Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 21905 0 0 0 27698 125 0 0 25 0 1 0 1846558814 88801280 21199 4294967295 134512640 135094434 3221224432 3221223024 134557537 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15326/statm): 21680 21199 145 145 0 21535 0
[pid=15326] vsize: 86720
Current children cumulated CPU time (s) 278.23
Current children cumulated vsize (Kb) 88844

[startup+290.031 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 15326
Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15322/statm): 531 226 485 147 0 384 0
[pid=15322] vsize: 2124
Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 22447 0 0 0 28690 128 0 0 25 0 1 0 1846558814 91013120 21741 4294967295 134512640 135094434 3221224432 3221223104 134555943 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15326/statm): 22220 21741 145 145 0 22075 0
[pid=15326] vsize: 88880
Current children cumulated CPU time (s) 288.18
Current children cumulated vsize (Kb) 91004

[startup+300.032 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 15326
Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15322/statm): 531 226 485 147 0 384 0
[pid=15322] vsize: 2124
Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 23030 0 0 0 29681 133 0 0 25 0 1 0 1846558814 93396992 22324 4294967295 134512640 135094434 3221224432 3221223104 134555574 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15326/statm): 22802 22324 145 145 0 22657 0
[pid=15326] vsize: 91208
Current children cumulated CPU time (s) 298.14
Current children cumulated vsize (Kb) 93332

[startup+310.034 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 15326
Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15322/statm): 531 226 485 147 0 384 0
[pid=15322] vsize: 2124
Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 23635 0 0 0 30672 137 0 0 25 0 1 0 1846558814 95866880 22929 4294967295 134512640 135094434 3221224432 3221223120 134554715 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15326/statm): 23405 22929 145 145 0 23260 0
[pid=15326] vsize: 93620
Current children cumulated CPU time (s) 308.09
Current children cumulated vsize (Kb) 95744

[startup+320.035 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 15326
Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15322/statm): 531 226 485 147 0 384 0
[pid=15322] vsize: 2124
Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 24069 0 0 0 31665 140 0 0 25 0 1 0 1846558814 97898496 23363 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15326/statm): 23901 23363 145 145 0 23756 0
[pid=15326] vsize: 95604
Current children cumulated CPU time (s) 318.05
Current children cumulated vsize (Kb) 97728

[startup+330.036 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 15326
Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15322/statm): 531 226 485 147 0 384 0
[pid=15322] vsize: 2124
Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 24667 0 0 0 32655 145 0 0 25 0 1 0 1846558814 100339712 23961 4294967295 134512640 135094434 3221224432 3221223088 134558227 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15326/statm): 24497 23961 145 145 0 24352 0
[pid=15326] vsize: 97988
Current children cumulated CPU time (s) 328
Current children cumulated vsize (Kb) 100112

[startup+340.036 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 15326
Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15322/statm): 531 226 485 147 0 384 0
[pid=15322] vsize: 2124
Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 25091 0 0 0 33648 148 0 0 25 0 1 0 1846558814 102068224 24385 4294967295 134512640 135094434 3221224432 3221223024 134557230 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15326/statm): 24919 24385 145 145 0 24774 0
[pid=15326] vsize: 99676
Current children cumulated CPU time (s) 337.96
Current children cumulated vsize (Kb) 101800

[startup+350.037 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 15326
Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15322/statm): 531 226 485 147 0 384 0
[pid=15322] vsize: 2124
Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 25668 0 0 0 34639 152 0 0 25 0 1 0 1846558814 104423424 24962 4294967295 134512640 135094434 3221224432 3221223024 134556904 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15326/statm): 25494 24962 145 145 0 25349 0
[pid=15326] vsize: 101976
Current children cumulated CPU time (s) 347.91
Current children cumulated vsize (Kb) 104100

[startup+360.039 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 15326
Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15322/statm): 531 226 485 147 0 384 0
[pid=15322] vsize: 2124
Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 26399 0 0 0 35630 156 0 0 25 0 1 0 1846558814 107425792 25693 4294967295 134512640 135094434 3221224432 3221223088 134557903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15326/statm): 26227 25693 145 145 0 26082 0
[pid=15326] vsize: 104908
Current children cumulated CPU time (s) 357.86
Current children cumulated vsize (Kb) 107032

[startup+370.04 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 15326
Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15322/statm): 531 226 485 147 0 384 0
[pid=15322] vsize: 2124
Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 27153 0 0 0 36619 161 0 0 25 0 1 0 1846558814 110510080 26447 4294967295 134512640 135094434 3221224432 3221223024 134556789 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15326/statm): 26980 26447 145 145 0 26835 0
[pid=15326] vsize: 107920
Current children cumulated CPU time (s) 367.8
Current children cumulated vsize (Kb) 110044

[startup+380.041 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 15326
Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15322/statm): 531 226 485 147 0 384 0
[pid=15322] vsize: 2124
Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 27672 0 0 0 37611 165 0 0 25 0 1 0 1846558814 112631808 26966 4294967295 134512640 135094434 3221224432 3221223088 134557996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15326/statm): 27498 26966 145 145 0 27353 0
[pid=15326] vsize: 109992
Current children cumulated CPU time (s) 377.76
Current children cumulated vsize (Kb) 112116

[startup+390.043 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 15326
Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15322/statm): 531 226 485 147 0 384 0
[pid=15322] vsize: 2124
Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 28013 0 0 0 38607 167 0 0 25 0 1 0 1846558814 114012160 27307 4294967295 134512640 135094434 3221224432 3221223088 134557882 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15326/statm): 27835 27307 145 145 0 27690 0
[pid=15326] vsize: 111340
Current children cumulated CPU time (s) 387.74
Current children cumulated vsize (Kb) 113464

[startup+400.043 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 15326
Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15322/statm): 531 226 485 147 0 384 0
[pid=15322] vsize: 2124
Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 28481 0 0 0 39600 171 0 0 25 0 1 0 1846558814 115916800 27775 4294967295 134512640 135094434 3221224432 3221223024 134557230 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15326/statm): 28300 27775 145 145 0 28155 0
[pid=15326] vsize: 113200
Current children cumulated CPU time (s) 397.71
Current children cumulated vsize (Kb) 115324

[startup+410.044 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 15326
Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15322/statm): 531 226 485 147 0 384 0
[pid=15322] vsize: 2124
Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 28905 0 0 0 40594 173 0 0 25 0 1 0 1846558814 117645312 28199 4294967295 134512640 135094434 3221224432 3221223024 134556789 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15326/statm): 28722 28199 145 145 0 28577 0
[pid=15326] vsize: 114888
Current children cumulated CPU time (s) 407.67
Current children cumulated vsize (Kb) 117012

[startup+420.045 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 15326
Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15322/statm): 531 226 485 147 0 384 0
[pid=15322] vsize: 2124
Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 29413 0 0 0 41585 177 0 0 25 0 1 0 1846558814 119717888 28707 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15326/statm): 29228 28707 145 145 0 29083 0
[pid=15326] vsize: 116912
Current children cumulated CPU time (s) 417.62
Current children cumulated vsize (Kb) 119036

[startup+430.046 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 15326
Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15322/statm): 531 226 485 147 0 384 0
[pid=15322] vsize: 2124
Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 29939 0 0 0 42577 180 0 0 25 0 1 0 1846558814 121864192 29233 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15326/statm): 29752 29233 145 145 0 29607 0
[pid=15326] vsize: 119008
Current children cumulated CPU time (s) 427.57
Current children cumulated vsize (Kb) 121132

[startup+440.047 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 15326
Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15322/statm): 531 226 485 147 0 384 0
[pid=15322] vsize: 2124
Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 30482 0 0 0 43567 184 0 0 25 0 1 0 1846558814 124080128 29776 4294967295 134512640 135094434 3221224432 3221223024 134557537 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15326/statm): 30293 29776 145 145 0 30148 0
[pid=15326] vsize: 121172
Current children cumulated CPU time (s) 437.51
Current children cumulated vsize (Kb) 123296

[startup+450.048 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 15326
Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15322/statm): 531 226 485 147 0 384 0
[pid=15322] vsize: 2124
Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 31186 0 0 0 44557 189 0 0 25 0 1 0 1846558814 126955520 30480 4294967295 134512640 135094434 3221224432 3221223024 134556853 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15326/statm): 30995 30480 145 145 0 30850 0
[pid=15326] vsize: 123980
Current children cumulated CPU time (s) 447.46
Current children cumulated vsize (Kb) 126104

[startup+460.048 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 15326
Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15322/statm): 531 226 485 147 0 384 0
[pid=15322] vsize: 2124
Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 31858 0 0 0 45546 192 0 0 25 0 1 0 1846558814 129703936 31152 4294967295 134512640 135094434 3221224432 3221223088 134558176 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15326/statm): 31666 31152 145 145 0 31521 0
[pid=15326] vsize: 126664
Current children cumulated CPU time (s) 457.38
Current children cumulated vsize (Kb) 128788

[startup+470.049 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 15326
Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15322/statm): 531 226 485 147 0 384 0
[pid=15322] vsize: 2124
Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 32497 0 0 0 46537 197 0 0 25 0 1 0 1846558814 132313088 31791 4294967295 134512640 135094434 3221224432 3221223024 134557302 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15326/statm): 32303 31791 145 145 0 32158 0
[pid=15326] vsize: 129212
Current children cumulated CPU time (s) 467.34
Current children cumulated vsize (Kb) 131336

[startup+480.05 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 15326
Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15322/statm): 531 226 485 147 0 384 0
[pid=15322] vsize: 2124
Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 33063 0 0 0 47528 201 0 0 25 0 1 0 1846558814 134627328 32357 4294967295 134512640 135094434 3221224432 3221223088 134558420 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15326/statm): 32868 32357 145 145 0 32723 0
[pid=15326] vsize: 131472
Current children cumulated CPU time (s) 477.29
Current children cumulated vsize (Kb) 133596

[startup+490.052 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 15326
Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15322/statm): 531 226 485 147 0 384 0
[pid=15322] vsize: 2124
Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 33655 0 0 0 48519 205 0 0 25 0 1 0 1846558814 137052160 32949 4294967295 134512640 135094434 3221224432 3221223088 134558004 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15326/statm): 33460 32949 145 145 0 33315 0
[pid=15326] vsize: 133840
Current children cumulated CPU time (s) 487.24
Current children cumulated vsize (Kb) 135964

[startup+500.053 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 15326
Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15322/statm): 531 226 485 147 0 384 0
[pid=15322] vsize: 2124
Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 34244 0 0 0 49511 209 0 0 25 0 1 0 1846558814 139460608 33538 4294967295 134512640 135094434 3221224432 3221223024 134556951 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15326/statm): 34048 33538 145 145 0 33903 0
[pid=15326] vsize: 136192
Current children cumulated CPU time (s) 497.2
Current children cumulated vsize (Kb) 138316

[startup+510.055 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 15326
Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15322/statm): 531 226 485 147 0 384 0
[pid=15322] vsize: 2124
Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 34711 0 0 0 50504 212 0 0 25 0 1 0 1846558814 141369344 34005 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15326/statm): 34514 34005 145 145 0 34369 0
[pid=15326] vsize: 138056
Current children cumulated CPU time (s) 507.16
Current children cumulated vsize (Kb) 140180

[startup+520.055 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 15326
Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15322/statm): 531 226 485 147 0 384 0
[pid=15322] vsize: 2124
Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 35306 0 0 0 51495 215 0 0 25 0 1 0 1846558814 143802368 34600 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15326/statm): 35108 34600 145 145 0 34963 0
[pid=15326] vsize: 140432
Current children cumulated CPU time (s) 517.1
Current children cumulated vsize (Kb) 142556

[startup+530.055 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 15326
Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15322/statm): 531 226 485 147 0 384 0
[pid=15322] vsize: 2124
Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 35603 0 0 0 52491 217 0 0 25 0 1 0 1846558814 145010688 34897 4294967295 134512640 135094434 3221224432 3221223088 134558174 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15326/statm): 35403 34897 145 145 0 35258 0
[pid=15326] vsize: 141612
Current children cumulated CPU time (s) 527.08
Current children cumulated vsize (Kb) 143736

[startup+540.057 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 15326
Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15322/statm): 531 226 485 147 0 384 0
[pid=15322] vsize: 2124
Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 36228 0 0 0 53482 220 0 0 25 0 1 0 1846558814 147558400 35522 4294967295 134512640 135094434 3221224432 3221223024 134556987 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15326/statm): 36025 35522 145 145 0 35880 0
[pid=15326] vsize: 144100
Current children cumulated CPU time (s) 537.02
Current children cumulated vsize (Kb) 146224

[startup+550.058 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 15326
Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15322/statm): 531 226 485 147 0 384 0
[pid=15322] vsize: 2124
Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 36744 0 0 0 54475 223 0 0 25 0 1 0 1846558814 149663744 36038 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15326/statm): 36539 36038 145 145 0 36394 0
[pid=15326] vsize: 146156
Current children cumulated CPU time (s) 546.98
Current children cumulated vsize (Kb) 148280

[startup+560.059 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 15326
Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15322/statm): 531 226 485 147 0 384 0
[pid=15322] vsize: 2124
Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 37061 0 0 0 55469 226 0 0 25 0 1 0 1846558814 150953984 36355 4294967295 134512640 135094434 3221224432 3221223024 134556785 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15326/statm): 36854 36355 145 145 0 36709 0
[pid=15326] vsize: 147416
Current children cumulated CPU time (s) 556.95
Current children cumulated vsize (Kb) 149540

[startup+570.059 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 15326
Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15322/statm): 531 226 485 147 0 384 0
[pid=15322] vsize: 2124
Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 37465 0 0 0 56462 230 0 0 25 0 1 0 1846558814 152604672 36759 4294967295 134512640 135094434 3221224432 3221223088 134557879 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15326/statm): 37257 36759 145 145 0 37112 0
[pid=15326] vsize: 149028
Current children cumulated CPU time (s) 566.92
Current children cumulated vsize (Kb) 151152

[startup+580.059 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 15326
Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15322/statm): 531 226 485 147 0 384 0
[pid=15322] vsize: 2124
Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 37892 0 0 0 57455 232 0 0 25 0 1 0 1846558814 154349568 37186 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15326/statm): 37683 37186 145 145 0 37538 0
[pid=15326] vsize: 150732
Current children cumulated CPU time (s) 576.87
Current children cumulated vsize (Kb) 152856

[startup+590.06 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 15326
Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15322/statm): 531 226 485 147 0 384 0
[pid=15322] vsize: 2124
Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 38451 0 0 0 58447 236 0 0 25 0 1 0 1846558814 156631040 37745 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15326/statm): 38240 37745 145 145 0 38095 0
[pid=15326] vsize: 152960
Current children cumulated CPU time (s) 586.83
Current children cumulated vsize (Kb) 155084

[startup+600.061 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 15326
Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15322/statm): 531 226 485 147 0 384 0
[pid=15322] vsize: 2124
Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 38996 0 0 0 59439 239 0 0 25 0 1 0 1846558814 158855168 38290 4294967295 134512640 135094434 3221224432 3221223088 134557846 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15326/statm): 38783 38290 145 145 0 38638 0
[pid=15326] vsize: 155132
Current children cumulated CPU time (s) 596.78
Current children cumulated vsize (Kb) 157256

[startup+610.063 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 15326
Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15322/statm): 531 226 485 147 0 384 0
[pid=15322] vsize: 2124
Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 39456 0 0 0 60432 242 0 0 25 0 1 0 1846558814 160735232 38750 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15326/statm): 39242 38750 145 145 0 39097 0
[pid=15326] vsize: 156968
Current children cumulated CPU time (s) 606.74
Current children cumulated vsize (Kb) 159092

[startup+620.064 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 15326
Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15322/statm): 531 226 485 147 0 384 0
[pid=15322] vsize: 2124
Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 39456 0 0 0 61432 242 0 0 25 0 1 0 1846558814 160735232 38750 4294967295 134512640 135094434 3221224432 3221223024 134556918 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15326/statm): 39242 38750 145 145 0 39097 0
[pid=15326] vsize: 156968
Current children cumulated CPU time (s) 616.74
Current children cumulated vsize (Kb) 159092

[startup+630.064 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 15326
Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15322/statm): 531 226 485 147 0 384 0
[pid=15322] vsize: 2124
Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 39456 0 0 0 62433 242 0 0 25 0 1 0 1846558814 160735232 38750 4294967295 134512640 135094434 3221224432 3221223024 134556969 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15326/statm): 39242 38750 145 145 0 39097 0
[pid=15326] vsize: 156968
Current children cumulated CPU time (s) 626.75
Current children cumulated vsize (Kb) 159092

[startup+640.065 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 15326
Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15322/statm): 531 226 485 147 0 384 0
[pid=15322] vsize: 2124
Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 39456 0 0 0 63433 242 0 0 25 0 1 0 1846558814 160735232 38750 4294967295 134512640 135094434 3221224432 3221223024 134557273 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15326/statm): 39242 38750 145 145 0 39097 0
[pid=15326] vsize: 156968
Current children cumulated CPU time (s) 636.75
Current children cumulated vsize (Kb) 159092

[startup+650.066 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 15326
Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15322/statm): 531 226 485 147 0 384 0
[pid=15322] vsize: 2124
Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 39456 0 0 0 64433 242 0 0 25 0 1 0 1846558814 160735232 38750 4294967295 134512640 135094434 3221224432 3221223088 134558402 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15326/statm): 39242 38750 145 145 0 39097 0
[pid=15326] vsize: 156968
Current children cumulated CPU time (s) 646.75
Current children cumulated vsize (Kb) 159092

[startup+660.067 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 15326
Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15322/statm): 531 226 485 147 0 384 0
[pid=15322] vsize: 2124
Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 39456 0 0 0 65433 242 0 0 25 0 1 0 1846558814 160735232 38750 4294967295 134512640 135094434 3221224432 3221223104 134556454 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15326/statm): 39242 38750 145 145 0 39097 0
[pid=15326] vsize: 156968
Current children cumulated CPU time (s) 656.75
Current children cumulated vsize (Kb) 159092

[startup+670.068 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 15326
Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15322/statm): 531 226 485 147 0 384 0
[pid=15322] vsize: 2124
Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 39456 0 0 0 66432 243 0 0 25 0 1 0 1846558814 160735232 38750 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15326/statm): 39242 38750 145 145 0 39097 0
[pid=15326] vsize: 156968
Current children cumulated CPU time (s) 666.75
Current children cumulated vsize (Kb) 159092

[startup+680.069 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 15326
Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15322/statm): 531 226 485 147 0 384 0
[pid=15322] vsize: 2124
Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 39456 0 0 0 67432 243 0 0 25 0 1 0 1846558814 160735232 38750 4294967295 134512640 135094434 3221224432 3221223024 134557210 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15326/statm): 39242 38750 145 145 0 39097 0
[pid=15326] vsize: 156968
Current children cumulated CPU time (s) 676.75
Current children cumulated vsize (Kb) 159092

[startup+690.069 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 15326
Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15322/statm): 531 226 485 147 0 384 0
[pid=15322] vsize: 2124
Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 39456 0 0 0 68432 243 0 0 25 0 1 0 1846558814 160735232 38750 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15326/statm): 39242 38750 145 145 0 39097 0
[pid=15326] vsize: 156968
Current children cumulated CPU time (s) 686.75
Current children cumulated vsize (Kb) 159092

[startup+700.07 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 15326
Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15322/statm): 531 226 485 147 0 384 0
[pid=15322] vsize: 2124
Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 39456 0 0 0 69433 243 0 0 25 0 1 0 1846558814 160735232 38750 4294967295 134512640 135094434 3221224432 3221223024 134557002 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15326/statm): 39242 38750 145 145 0 39097 0
[pid=15326] vsize: 156968
Current children cumulated CPU time (s) 696.76
Current children cumulated vsize (Kb) 159092

[startup+710.072 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 15326
Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15322/statm): 531 226 485 147 0 384 0
[pid=15322] vsize: 2124
Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 39456 0 0 0 70433 243 0 0 25 0 1 0 1846558814 160735232 38750 4294967295 134512640 135094434 3221224432 3221223024 134557016 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15326/statm): 39242 38750 145 145 0 39097 0
[pid=15326] vsize: 156968
Current children cumulated CPU time (s) 706.76
Current children cumulated vsize (Kb) 159092

[startup+720.073 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 15326
Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15322/statm): 531 226 485 147 0 384 0
[pid=15322] vsize: 2124
Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 39456 0 0 0 71433 243 0 0 25 0 1 0 1846558814 160735232 38750 4294967295 134512640 135094434 3221224432 3221223024 134556809 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15326/statm): 39242 38750 145 145 0 39097 0
[pid=15326] vsize: 156968
Current children cumulated CPU time (s) 716.76
Current children cumulated vsize (Kb) 159092

[startup+730.074 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 15326
Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15322/statm): 531 226 485 147 0 384 0
[pid=15322] vsize: 2124
Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 39456 0 0 0 72433 243 0 0 25 0 1 0 1846558814 160735232 38750 4294967295 134512640 135094434 3221224432 3221223088 134558011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15326/statm): 39242 38750 145 145 0 39097 0
[pid=15326] vsize: 156968
Current children cumulated CPU time (s) 726.76
Current children cumulated vsize (Kb) 159092

[startup+740.074 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 15326
Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15322/statm): 531 226 485 147 0 384 0
[pid=15322] vsize: 2124
Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 39456 0 0 0 73434 243 0 0 25 0 1 0 1846558814 160735232 38750 4294967295 134512640 135094434 3221224432 3221223024 134557485 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15326/statm): 39242 38750 145 145 0 39097 0
[pid=15326] vsize: 156968
Current children cumulated CPU time (s) 736.77
Current children cumulated vsize (Kb) 159092

[startup+750.075 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 15326
Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15322/statm): 531 226 485 147 0 384 0
[pid=15322] vsize: 2124
Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 39456 0 0 0 74434 243 0 0 25 0 1 0 1846558814 160735232 38750 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15326/statm): 39242 38750 145 145 0 39097 0
[pid=15326] vsize: 156968
Current children cumulated CPU time (s) 746.77
Current children cumulated vsize (Kb) 159092

[startup+760.076 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 15326
Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15322/statm): 531 226 485 147 0 384 0
[pid=15322] vsize: 2124
Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 39456 0 0 0 75434 243 0 0 25 0 1 0 1846558814 160735232 38750 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15326/statm): 39242 38750 145 145 0 39097 0
[pid=15326] vsize: 156968
Current children cumulated CPU time (s) 756.77
Current children cumulated vsize (Kb) 159092

[startup+770.077 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 15326
Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15322/statm): 531 226 485 147 0 384 0
[pid=15322] vsize: 2124
Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 39456 0 0 0 76434 243 0 0 25 0 1 0 1846558814 160735232 38750 4294967295 134512640 135094434 3221224432 3221223088 134557964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15326/statm): 39242 38750 145 145 0 39097 0
[pid=15326] vsize: 156968
Current children cumulated CPU time (s) 766.77
Current children cumulated vsize (Kb) 159092

[startup+780.078 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 15326
Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15322/statm): 531 226 485 147 0 384 0
[pid=15322] vsize: 2124
Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 39456 0 0 0 77434 243 0 0 25 0 1 0 1846558814 160735232 38750 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15326/statm): 39242 38750 145 145 0 39097 0
[pid=15326] vsize: 156968
Current children cumulated CPU time (s) 776.77
Current children cumulated vsize (Kb) 159092

[startup+790.079 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 15326
Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15322/statm): 531 226 485 147 0 384 0
[pid=15322] vsize: 2124
Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 39456 0 0 0 78434 243 0 0 25 0 1 0 1846558814 160735232 38750 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15326/statm): 39242 38750 145 145 0 39097 0
[pid=15326] vsize: 156968
Current children cumulated CPU time (s) 786.77
Current children cumulated vsize (Kb) 159092

[startup+800.079 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 15326
Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15322/statm): 531 226 485 147 0 384 0
[pid=15322] vsize: 2124
Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 39456 0 0 0 79435 243 0 0 25 0 1 0 1846558814 160735232 38750 4294967295 134512640 135094434 3221224432 3221223024 134557310 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15326/statm): 39242 38750 145 145 0 39097 0
[pid=15326] vsize: 156968
Current children cumulated CPU time (s) 796.78
Current children cumulated vsize (Kb) 159092

[startup+810.081 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 15326
Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15322/statm): 531 226 485 147 0 384 0
[pid=15322] vsize: 2124
Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 39456 0 0 0 80435 243 0 0 25 0 1 0 1846558814 160735232 38750 4294967295 134512640 135094434 3221224432 3221223024 134556809 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15326/statm): 39242 38750 145 145 0 39097 0
[pid=15326] vsize: 156968
Current children cumulated CPU time (s) 806.78
Current children cumulated vsize (Kb) 159092

[startup+820.082 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 15326
Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15322/statm): 531 226 485 147 0 384 0
[pid=15322] vsize: 2124
Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 39456 0 0 0 81435 243 0 0 25 0 1 0 1846558814 160735232 38750 4294967295 134512640 135094434 3221224432 3221223024 134557160 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15326/statm): 39242 38750 145 145 0 39097 0
[pid=15326] vsize: 156968
Current children cumulated CPU time (s) 816.78
Current children cumulated vsize (Kb) 159092

[startup+830.082 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 15326
Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15322/statm): 531 226 485 147 0 384 0
[pid=15322] vsize: 2124
Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 39456 0 0 0 82436 243 0 0 25 0 1 0 1846558814 160735232 38750 4294967295 134512640 135094434 3221224432 3221223088 134557900 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15326/statm): 39242 38750 145 145 0 39097 0
[pid=15326] vsize: 156968
Current children cumulated CPU time (s) 826.79
Current children cumulated vsize (Kb) 159092

[startup+840.083 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 15326
Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15322/statm): 531 226 485 147 0 384 0
[pid=15322] vsize: 2124
Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 39456 0 0 0 83436 244 0 0 25 0 1 0 1846558814 160735232 38750 4294967295 134512640 135094434 3221224432 3221223044 134563046 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15326/statm): 39242 38750 145 145 0 39097 0
[pid=15326] vsize: 156968
Current children cumulated CPU time (s) 836.8
Current children cumulated vsize (Kb) 159092

[startup+850.084 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 15326
Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15322/statm): 531 226 485 147 0 384 0
[pid=15322] vsize: 2124
Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 39456 0 0 0 84436 244 0 0 25 0 1 0 1846558814 160735232 38750 4294967295 134512640 135094434 3221224432 3221223088 134557866 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15326/statm): 39242 38750 145 145 0 39097 0
[pid=15326] vsize: 156968
Current children cumulated CPU time (s) 846.8
Current children cumulated vsize (Kb) 159092

[startup+860.084 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 15326
Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15322/statm): 531 226 485 147 0 384 0
[pid=15322] vsize: 2124
Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 39456 0 0 0 85436 244 0 0 25 0 1 0 1846558814 160735232 38750 4294967295 134512640 135094434 3221224432 3221223024 134557297 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15326/statm): 39242 38750 145 145 0 39097 0
[pid=15326] vsize: 156968
Current children cumulated CPU time (s) 856.8
Current children cumulated vsize (Kb) 159092

[startup+870.085 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 15326
Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15322/statm): 531 226 485 147 0 384 0
[pid=15322] vsize: 2124
Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 39456 0 0 0 86436 244 0 0 25 0 1 0 1846558814 160735232 38750 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15326/statm): 39242 38750 145 145 0 39097 0
[pid=15326] vsize: 156968
Current children cumulated CPU time (s) 866.8
Current children cumulated vsize (Kb) 159092

[startup+880.086 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 15326
Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15322/statm): 531 226 485 147 0 384 0
[pid=15322] vsize: 2124
Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 39456 0 0 0 87436 244 0 0 25 0 1 0 1846558814 160735232 38750 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15326/statm): 39242 38750 145 145 0 39097 0
[pid=15326] vsize: 156968
Current children cumulated CPU time (s) 876.8
Current children cumulated vsize (Kb) 159092

[startup+890.087 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 15326
Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15322/statm): 531 226 485 147 0 384 0
[pid=15322] vsize: 2124
Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 39456 0 0 0 88437 244 0 0 25 0 1 0 1846558814 160735232 38750 4294967295 134512640 135094434 3221224432 3221223024 134556928 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15326/statm): 39242 38750 145 145 0 39097 0
[pid=15326] vsize: 156968
Current children cumulated CPU time (s) 886.81
Current children cumulated vsize (Kb) 159092

[startup+900.088 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 15326
Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15322/statm): 531 226 485 147 0 384 0
[pid=15322] vsize: 2124
Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 39456 0 0 0 89437 244 0 0 25 0 1 0 1846558814 160735232 38750 4294967295 134512640 135094434 3221224432 3221223088 134557863 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15326/statm): 39242 38750 145 145 0 39097 0
[pid=15326] vsize: 156968
Current children cumulated CPU time (s) 896.81
Current children cumulated vsize (Kb) 159092

[startup+910.089 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 15326
Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15322/statm): 531 226 485 147 0 384 0
[pid=15322] vsize: 2124
Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 39456 0 0 0 90437 244 0 0 25 0 1 0 1846558814 160735232 38750 4294967295 134512640 135094434 3221224432 3221223024 134556984 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15326/statm): 39242 38750 145 145 0 39097 0
[pid=15326] vsize: 156968
Current children cumulated CPU time (s) 906.81
Current children cumulated vsize (Kb) 159092

[startup+920.089 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 15326
Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15322/statm): 531 226 485 147 0 384 0
[pid=15322] vsize: 2124
Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 39456 0 0 0 91437 244 0 0 25 0 1 0 1846558814 160735232 38750 4294967295 134512640 135094434 3221224432 3221223024 134556806 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15326/statm): 39242 38750 145 145 0 39097 0
[pid=15326] vsize: 156968
Current children cumulated CPU time (s) 916.81
Current children cumulated vsize (Kb) 159092

[startup+930.09 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 15326
Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15322/statm): 531 226 485 147 0 384 0
[pid=15322] vsize: 2124
Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 39456 0 0 0 92437 244 0 0 25 0 1 0 1846558814 160735232 38750 4294967295 134512640 135094434 3221224432 3221223024 134556999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15326/statm): 39242 38750 145 145 0 39097 0
[pid=15326] vsize: 156968
Current children cumulated CPU time (s) 926.81
Current children cumulated vsize (Kb) 159092

[startup+940.091 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 15326
Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15322/statm): 531 226 485 147 0 384 0
[pid=15322] vsize: 2124
Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 39456 0 0 0 93438 244 0 0 25 0 1 0 1846558814 160735232 38750 4294967295 134512640 135094434 3221224432 3221223104 134556266 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15326/statm): 39242 38750 145 145 0 39097 0
[pid=15326] vsize: 156968
Current children cumulated CPU time (s) 936.82
Current children cumulated vsize (Kb) 159092

[startup+950.092 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 15326
Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15322/statm): 531 226 485 147 0 384 0
[pid=15322] vsize: 2124
Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 39456 0 0 0 94437 244 0 0 25 0 1 0 1846558814 160735232 38750 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15326/statm): 39242 38750 145 145 0 39097 0
[pid=15326] vsize: 156968
Current children cumulated CPU time (s) 946.81
Current children cumulated vsize (Kb) 159092

[startup+960.093 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 15326
Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15322/statm): 531 226 485 147 0 384 0
[pid=15322] vsize: 2124
Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 39456 0 0 0 95438 244 0 0 25 0 1 0 1846558814 160735232 38750 4294967295 134512640 135094434 3221224432 3221223024 134556809 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15326/statm): 39242 38750 145 145 0 39097 0
[pid=15326] vsize: 156968
Current children cumulated CPU time (s) 956.82
Current children cumulated vsize (Kb) 159092

[startup+970.093 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 15326
Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15322/statm): 531 226 485 147 0 384 0
[pid=15322] vsize: 2124
Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 39456 0 0 0 96438 244 0 0 25 0 1 0 1846558814 160735232 38750 4294967295 134512640 135094434 3221224432 3221223088 134558221 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15326/statm): 39242 38750 145 145 0 39097 0
[pid=15326] vsize: 156968
Current children cumulated CPU time (s) 966.82
Current children cumulated vsize (Kb) 159092

[startup+980.093 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 15326
Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15322/statm): 531 226 485 147 0 384 0
[pid=15322] vsize: 2124
Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 39456 0 0 0 97438 244 0 0 25 0 1 0 1846558814 160735232 38750 4294967295 134512640 135094434 3221224432 3221223088 134558395 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15326/statm): 39242 38750 145 145 0 39097 0
[pid=15326] vsize: 156968
Current children cumulated CPU time (s) 976.82
Current children cumulated vsize (Kb) 159092

[startup+990.095 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 15326
Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15322/statm): 531 226 485 147 0 384 0
[pid=15322] vsize: 2124
Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 39456 0 0 0 98438 244 0 0 25 0 1 0 1846558814 160735232 38750 4294967295 134512640 135094434 3221224432 3221223024 134556999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15326/statm): 39242 38750 145 145 0 39097 0
[pid=15326] vsize: 156968
Current children cumulated CPU time (s) 986.82
Current children cumulated vsize (Kb) 159092

[startup+1000.1 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 15326
Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15322/statm): 531 226 485 147 0 384 0
[pid=15322] vsize: 2124
Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 39456 0 0 0 99438 244 0 0 25 0 1 0 1846558814 160735232 38750 4294967295 134512640 135094434 3221224432 3221223056 134557696 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15326/statm): 39242 38750 145 145 0 39097 0
[pid=15326] vsize: 156968
Current children cumulated CPU time (s) 996.82
Current children cumulated vsize (Kb) 159092

[startup+1010.1 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 15326
Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15322/statm): 531 226 485 147 0 384 0
[pid=15322] vsize: 2124
Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 39456 0 0 0 100439 244 0 0 25 0 1 0 1846558814 160735232 38750 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15326/statm): 39242 38750 145 145 0 39097 0
[pid=15326] vsize: 156968
Current children cumulated CPU time (s) 1006.83
Current children cumulated vsize (Kb) 159092

[startup+1020.1 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 15326
Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15322/statm): 531 226 485 147 0 384 0
[pid=15322] vsize: 2124
Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 39456 0 0 0 101439 244 0 0 25 0 1 0 1846558814 160735232 38750 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15326/statm): 39242 38750 145 145 0 39097 0
[pid=15326] vsize: 156968
Current children cumulated CPU time (s) 1016.83
Current children cumulated vsize (Kb) 159092

[startup+1030.1 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 15326
Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15322/statm): 531 226 485 147 0 384 0
[pid=15322] vsize: 2124
Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 39456 0 0 0 102439 244 0 0 25 0 1 0 1846558814 160735232 38750 4294967295 134512640 135094434 3221224432 3221223104 134556317 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15326/statm): 39242 38750 145 145 0 39097 0
[pid=15326] vsize: 156968
Current children cumulated CPU time (s) 1026.83
Current children cumulated vsize (Kb) 159092

[startup+1040.1 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 15326
Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15322/statm): 531 226 485 147 0 384 0
[pid=15322] vsize: 2124
Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 39456 0 0 0 103439 244 0 0 25 0 1 0 1846558814 160735232 38750 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15326/statm): 39242 38750 145 145 0 39097 0
[pid=15326] vsize: 156968
Current children cumulated CPU time (s) 1036.83
Current children cumulated vsize (Kb) 159092

[startup+1050.1 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 15326
Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15322/statm): 531 226 485 147 0 384 0
[pid=15322] vsize: 2124
Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 39456 0 0 0 104439 244 0 0 25 0 1 0 1846558814 160735232 38750 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15326/statm): 39242 38750 145 145 0 39097 0
[pid=15326] vsize: 156968
Current children cumulated CPU time (s) 1046.83
Current children cumulated vsize (Kb) 159092

[startup+1060.1 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 15326
Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15322/statm): 531 226 485 147 0 384 0
[pid=15322] vsize: 2124
Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 39456 0 0 0 105439 244 0 0 25 0 1 0 1846558814 160735232 38750 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15326/statm): 39242 38750 145 145 0 39097 0
[pid=15326] vsize: 156968
Current children cumulated CPU time (s) 1056.83
Current children cumulated vsize (Kb) 159092

[startup+1070.1 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 15326
Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15322/statm): 531 226 485 147 0 384 0
[pid=15322] vsize: 2124
Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 39456 0 0 0 106439 245 0 0 25 0 1 0 1846558814 160735232 38750 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15326/statm): 39242 38750 145 145 0 39097 0
[pid=15326] vsize: 156968
Current children cumulated CPU time (s) 1066.84
Current children cumulated vsize (Kb) 159092

[startup+1080.1 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 15326
Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15322/statm): 531 226 485 147 0 384 0
[pid=15322] vsize: 2124
Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 39456 0 0 0 107439 245 0 0 25 0 1 0 1846558814 160735232 38750 4294967295 134512640 135094434 3221224432 3221223104 134555945 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15326/statm): 39242 38750 145 145 0 39097 0
[pid=15326] vsize: 156968
Current children cumulated CPU time (s) 1076.84
Current children cumulated vsize (Kb) 159092

[startup+1090.1 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 15326
Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15322/statm): 531 226 485 147 0 384 0
[pid=15322] vsize: 2124
Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 39456 0 0 0 108439 245 0 0 25 0 1 0 1846558814 160735232 38750 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15326/statm): 39242 38750 145 145 0 39097 0
[pid=15326] vsize: 156968
Current children cumulated CPU time (s) 1086.84
Current children cumulated vsize (Kb) 159092

[startup+1100.1 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 15326
Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15322/statm): 531 226 485 147 0 384 0
[pid=15322] vsize: 2124
Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 39456 0 0 0 109438 246 0 0 25 0 1 0 1846558814 160735232 38750 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15326/statm): 39242 38750 145 145 0 39097 0
[pid=15326] vsize: 156968
Current children cumulated CPU time (s) 1096.84
Current children cumulated vsize (Kb) 159092

[startup+1110.1 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 15326
Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15322/statm): 531 226 485 147 0 384 0
[pid=15322] vsize: 2124
Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 39534 0 0 0 110435 248 0 0 25 0 1 0 1846558814 161054720 38828 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15326/statm): 39320 38828 145 145 0 39175 0
[pid=15326] vsize: 157280
Current children cumulated CPU time (s) 1106.83
Current children cumulated vsize (Kb) 159404

[startup+1120.1 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 15326
Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15322/statm): 531 226 485 147 0 384 0
[pid=15322] vsize: 2124
Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 39887 0 0 0 111431 249 0 0 25 0 1 0 1846558814 162500608 39181 4294967295 134512640 135094434 3221224432 3221223024 134557273 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15326/statm): 39673 39181 145 145 0 39528 0
[pid=15326] vsize: 158692
Current children cumulated CPU time (s) 1116.8
Current children cumulated vsize (Kb) 160816

[startup+1130.1 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 15326
Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15322/statm): 531 226 485 147 0 384 0
[pid=15322] vsize: 2124
Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 40300 0 0 0 112426 252 0 0 25 0 1 0 1846558814 164192256 39594 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15326/statm): 40086 39594 145 145 0 39941 0
[pid=15326] vsize: 160344
Current children cumulated CPU time (s) 1126.78
Current children cumulated vsize (Kb) 162468

[startup+1140.1 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 15326
Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15322/statm): 531 226 485 147 0 384 0
[pid=15322] vsize: 2124
Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 40971 0 0 0 113418 256 0 0 25 0 1 0 1846558814 166932480 40265 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15326/statm): 40755 40265 145 145 0 40610 0
[pid=15326] vsize: 163020
Current children cumulated CPU time (s) 1136.74
Current children cumulated vsize (Kb) 165144

[startup+1150.11 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 15326
Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15322/statm): 531 226 485 147 0 384 0
[pid=15322] vsize: 2124
Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 41496 0 0 0 114411 259 0 0 25 0 1 0 1846558814 169082880 40790 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15326/statm): 41280 40790 145 145 0 41135 0
[pid=15326] vsize: 165120
Current children cumulated CPU time (s) 1146.7
Current children cumulated vsize (Kb) 167244

[startup+1160.11 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 15326
Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15322/statm): 531 226 485 147 0 384 0
[pid=15322] vsize: 2124
Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 42029 0 0 0 115404 263 0 0 25 0 1 0 1846558814 171266048 41323 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15326/statm): 41813 41323 145 145 0 41668 0
[pid=15326] vsize: 167252
Current children cumulated CPU time (s) 1156.67
Current children cumulated vsize (Kb) 169376

[startup+1170.11 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 15326
Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15322/statm): 531 226 485 147 0 384 0
[pid=15322] vsize: 2124
Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 42519 0 0 0 116398 266 0 0 25 0 1 0 1846558814 173268992 41813 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15326/statm): 42302 41813 145 145 0 42157 0
[pid=15326] vsize: 169208
Current children cumulated CPU time (s) 1166.64
Current children cumulated vsize (Kb) 171332

[startup+1180.11 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 15326
Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15322/statm): 531 226 485 147 0 384 0
[pid=15322] vsize: 2124
Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 43001 0 0 0 117391 269 0 0 25 0 1 0 1846558814 175235072 42295 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15326/statm): 42782 42295 145 145 0 42637 0
[pid=15326] vsize: 171128
Current children cumulated CPU time (s) 1176.6
Current children cumulated vsize (Kb) 173252

[startup+1190.11 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 15326
Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15322/statm): 531 226 485 147 0 384 0
[pid=15322] vsize: 2124
Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 43727 0 0 0 118382 274 0 0 25 0 1 0 1846558814 178204672 43021 4294967295 134512640 135094434 3221224432 3221223024 134556789 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15326/statm): 43507 43021 145 145 0 43362 0
[pid=15326] vsize: 174028
Current children cumulated CPU time (s) 1186.56
Current children cumulated vsize (Kb) 176152

[startup+1200.11 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 15326
Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15322/statm): 531 226 485 147 0 384 0
[pid=15322] vsize: 2124
Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 44460 0 0 0 119372 277 0 0 25 0 1 0 1846558814 181202944 43754 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15326/statm): 44239 43754 145 145 0 44094 0
[pid=15326] vsize: 176956
Current children cumulated CPU time (s) 1196.49
Current children cumulated vsize (Kb) 179080

[startup+1210.11 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 15326
Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15322/statm): 531 226 485 147 0 384 0
[pid=15322] vsize: 2124
Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) T 15322 15322 28974 0 -1 0 45079 0 0 0 120364 279 0 0 25 0 1 0 1846558814 183734272 44373 4294967295 134512640 135094434 3221224432 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/15326/statm): 44857 44373 145 145 0 44712 0
[pid=15326] vsize: 179428
Current children cumulated CPU time (s) 1206.43
Current children cumulated vsize (Kb) 181552



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.11 s]
Raw data (loadavg): 0.99 0.97 0.95 1/57 15326
Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15322/statm): 531 226 485 147 0 384 0
[pid=15322] vsize: 2124
Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) T 15322 15322 28974 0 -1 0 45079 0 0 0 120364 279 0 0 25 0 1 0 1846558814 183734272 44373 4294967295 134512640 135094434 3221224432 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/15326/statm): 44857 44373 145 145 0 44712 0
[pid=15326] vsize: 179428
Current children cumulated CPU time (s) 1206.43
Current children cumulated vsize (Kb) 181552

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

Child status: 0
Real time (s): 1210.2
CPU time (s): 1206.52
CPU user time (s): 1203.65
CPU system time (s): 2.87656
CPU usage (%): 99.6965
Max. virtual memory (cumulated for all children) (Kb): 181552

Verifier Data

ERROR: no interpretation found !