Some explanations

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

General information on the benchmark

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

Trace number 4537

Launcher Data

LAUNCH ON wulflinc4 THE 2005-09-19 18:05:39 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=2991 boxname=wulflinc4 idbench=647 idsolver=3 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  ef7064a9be2b712276f7b600af28e2b0  /oldhome/oroussel/tmp/wulflinc4/normalized-mps-v2-20-10-mod010.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc4/normalized-mps-v2-20-10-mod010.opb
IDLAUNCH: 2991
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
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	: 890.88

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
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:        907444 kB
Buffers:         33248 kB
Cached:          68416 kB
SwapCached:        880 kB
Active:          56356 kB
Inactive:        47904 kB
HighTotal:      131008 kB
HighFree:        59332 kB
LowTotal:       903652 kB
LowFree:        848112 kB
SwapTotal:     2097136 kB
SwapFree:      2095648 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5684 kB
Slab:            17256 kB
Committed_AS:    72360 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-09-19 18:25:49 (client local time) WITH STATUS 0 IN 1206.38 SECONDS
stats: 2991 7 1206.38 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/32347/stat): 32347 (minisat+_script) R 32346 32347 6847 0 -1 0 19 0 0 0 0 0 0 0 22 0 1 0 1793679028 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 1 0 0
Raw data (/proc/32347/statm): 174 3 169 147 0 27 0
[pid=32347] 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=32348
New process pid=32349
New process pid=32350
execve syscall for /bin/sed executable
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
One traced child (pid=32349) exited with status: 0
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=32350) exited with status: 0
One traced child (pid=32348) exited with status: 0
New process pid=32351
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc4/normalized-mps-v2-20-10-mod010.opb

[startup+10.0037 s]
Raw data (loadavg): 0.93 0.95 0.87 2/57 32351
Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32347/statm): 531 226 485 147 0 384 0
[pid=32347] vsize: 2124
Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 5213 0 0 0 960 19 0 0 25 0 1 0 1793679033 20332544 4507 4294967295 134512640 135094434 3221224432 3221223104 134556073 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32351/statm): 4964 4507 145 145 0 4819 0
[pid=32351] vsize: 19856
Current children cumulated CPU time (s) 9.79
Current children cumulated vsize (Kb) 21980

[startup+20.0045 s]
Raw data (loadavg): 0.94 0.96 0.88 2/57 32351
Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32347/statm): 531 226 485 147 0 384 0
[pid=32347] vsize: 2124
Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 5775 0 0 0 1951 22 0 0 25 0 1 0 1793679033 22634496 5069 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32351/statm): 5526 5069 145 145 0 5381 0
[pid=32351] vsize: 22104
Current children cumulated CPU time (s) 19.73
Current children cumulated vsize (Kb) 24228

[startup+30.0064 s]
Raw data (loadavg): 0.95 0.96 0.88 2/57 32351
Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32347/statm): 531 226 485 147 0 384 0
[pid=32347] vsize: 2124
Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 6337 0 0 0 2941 26 0 0 25 0 1 0 1793679033 24961024 5631 4294967295 134512640 135094434 3221224432 3221223056 134562108 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32351/statm): 6094 5631 145 145 0 5949 0
[pid=32351] vsize: 24376
Current children cumulated CPU time (s) 29.67
Current children cumulated vsize (Kb) 26500

[startup+40.0072 s]
Raw data (loadavg): 0.95 0.96 0.88 2/57 32351
Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32347/statm): 531 226 485 147 0 384 0
[pid=32347] vsize: 2124
Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 7107 0 0 0 3930 31 0 0 25 0 1 0 1793679033 28098560 6401 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32351/statm): 6860 6401 145 145 0 6715 0
[pid=32351] vsize: 27440
Current children cumulated CPU time (s) 39.61
Current children cumulated vsize (Kb) 29564

[startup+50.0081 s]
Raw data (loadavg): 0.96 0.96 0.88 2/57 32351
Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32347/statm): 531 226 485 147 0 384 0
[pid=32347] vsize: 2124
Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 7841 0 0 0 4919 35 0 0 25 0 1 0 1793679033 31100928 7135 4294967295 134512640 135094434 3221224432 3221223056 134557653 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32351/statm): 7593 7135 145 145 0 7448 0
[pid=32351] vsize: 30372
Current children cumulated CPU time (s) 49.54
Current children cumulated vsize (Kb) 32496

[startup+60.0099 s]
Raw data (loadavg): 0.97 0.96 0.88 2/57 32351
Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32347/statm): 531 226 485 147 0 384 0
[pid=32347] vsize: 2124
Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 8475 0 0 0 5910 39 0 0 25 0 1 0 1793679033 33746944 7769 4294967295 134512640 135094434 3221224432 3221223024 134556851 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32351/statm): 8239 7769 145 145 0 8094 0
[pid=32351] vsize: 32956
Current children cumulated CPU time (s) 59.49
Current children cumulated vsize (Kb) 35080

[startup+70.0108 s]
Raw data (loadavg): 0.97 0.96 0.88 2/57 32351
Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32347/statm): 531 226 485 147 0 384 0
[pid=32347] vsize: 2124
Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 9106 0 0 0 6899 43 0 0 25 0 1 0 1793679033 36323328 8400 4294967295 134512640 135094434 3221224432 3221223024 134557219 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32351/statm): 8868 8400 145 145 0 8723 0
[pid=32351] vsize: 35472
Current children cumulated CPU time (s) 69.42
Current children cumulated vsize (Kb) 37596

[startup+80.0126 s]
Raw data (loadavg): 0.98 0.96 0.88 2/57 32351
Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32347/statm): 531 226 485 147 0 384 0
[pid=32347] vsize: 2124
Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 9710 0 0 0 7888 47 0 0 25 0 1 0 1793679033 38789120 9004 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32351/statm): 9470 9004 145 145 0 9325 0
[pid=32351] vsize: 37880
Current children cumulated CPU time (s) 79.35
Current children cumulated vsize (Kb) 40004

[startup+90.0135 s]
Raw data (loadavg): 0.98 0.96 0.88 2/57 32351
Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32347/statm): 531 226 485 147 0 384 0
[pid=32347] vsize: 2124
Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 10299 0 0 0 8879 51 0 0 25 0 1 0 1793679033 41201664 9593 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32351/statm): 10059 9593 145 145 0 9914 0
[pid=32351] vsize: 40236
Current children cumulated CPU time (s) 89.3
Current children cumulated vsize (Kb) 42360

[startup+100.014 s]
Raw data (loadavg): 0.98 0.96 0.88 2/57 32351
Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32347/statm): 531 226 485 147 0 384 0
[pid=32347] vsize: 2124
Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 10836 0 0 0 9871 55 0 0 25 0 1 0 1793679033 43401216 10130 4294967295 134512640 135094434 3221224432 3221223024 134557042 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32351/statm): 10596 10130 145 145 0 10451 0
[pid=32351] vsize: 42384
Current children cumulated CPU time (s) 99.26
Current children cumulated vsize (Kb) 44508

[startup+110.016 s]
Raw data (loadavg): 0.98 0.96 0.88 2/57 32351
Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32347/statm): 531 226 485 147 0 384 0
[pid=32347] vsize: 2124
Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 11371 0 0 0 10863 58 0 0 25 0 1 0 1793679033 45600768 10665 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32351/statm): 11133 10665 145 145 0 10988 0
[pid=32351] vsize: 44532
Current children cumulated CPU time (s) 109.21
Current children cumulated vsize (Kb) 46656

[startup+120.017 s]
Raw data (loadavg): 0.99 0.97 0.89 2/57 32351
Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32347/statm): 531 226 485 147 0 384 0
[pid=32347] vsize: 2124
Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 11957 0 0 0 11853 62 0 0 25 0 1 0 1793679033 48001024 11251 4294967295 134512640 135094434 3221224432 3221223088 134558013 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32351/statm): 11719 11251 145 145 0 11574 0
[pid=32351] vsize: 46876
Current children cumulated CPU time (s) 119.15
Current children cumulated vsize (Kb) 49000

[startup+130.018 s]
Raw data (loadavg): 0.99 0.97 0.89 2/57 32351
Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32347/statm): 531 226 485 147 0 384 0
[pid=32347] vsize: 2124
Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 12658 0 0 0 12841 67 0 0 25 0 1 0 1793679033 50868224 11952 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32351/statm): 12419 11952 145 145 0 12274 0
[pid=32351] vsize: 49676
Current children cumulated CPU time (s) 129.08
Current children cumulated vsize (Kb) 51800

[startup+140.019 s]
Raw data (loadavg): 0.99 0.97 0.89 2/57 32351
Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32347/statm): 531 226 485 147 0 384 0
[pid=32347] vsize: 2124
Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 13327 0 0 0 13831 72 0 0 25 0 1 0 1793679033 53600256 12621 4294967295 134512640 135094434 3221224432 3221223056 134562057 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32351/statm): 13086 12621 145 145 0 12941 0
[pid=32351] vsize: 52344
Current children cumulated CPU time (s) 139.03
Current children cumulated vsize (Kb) 54468

[startup+150.02 s]
Raw data (loadavg): 0.99 0.97 0.89 2/57 32351
Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32347/statm): 531 226 485 147 0 384 0
[pid=32347] vsize: 2124
Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) T 32347 32347 6847 0 -1 0 13970 0 0 0 14821 76 0 0 25 0 1 0 1793679033 56229888 13264 4294967295 134512640 135094434 3221224432 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/32351/statm): 13728 13264 145 145 0 13583 0
[pid=32351] vsize: 54912
Current children cumulated CPU time (s) 148.97
Current children cumulated vsize (Kb) 57036

[startup+160.02 s]
Raw data (loadavg): 0.99 0.97 0.89 2/57 32351
Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32347/statm): 531 226 485 147 0 384 0
[pid=32347] vsize: 2124
Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 14584 0 0 0 15813 80 0 0 25 0 1 0 1793679033 58871808 13878 4294967295 134512640 135094434 3221224432 3221223024 134556806 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32351/statm): 14373 13878 145 145 0 14228 0
[pid=32351] vsize: 57492
Current children cumulated CPU time (s) 158.93
Current children cumulated vsize (Kb) 59616

[startup+170.021 s]
Raw data (loadavg): 0.99 0.97 0.89 2/57 32351
Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32347/statm): 531 226 485 147 0 384 0
[pid=32347] vsize: 2124
Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 15175 0 0 0 16804 84 0 0 25 0 1 0 1793679033 61284352 14469 4294967295 134512640 135094434 3221224432 3221223088 134558007 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32351/statm): 14962 14469 145 145 0 14817 0
[pid=32351] vsize: 59848
Current children cumulated CPU time (s) 168.88
Current children cumulated vsize (Kb) 61972

[startup+180.023 s]
Raw data (loadavg): 0.99 0.97 0.89 2/57 32351
Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32347/statm): 531 226 485 147 0 384 0
[pid=32347] vsize: 2124
Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 15764 0 0 0 17794 88 0 0 22 0 1 0 1793679033 63688704 15058 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32351/statm): 15549 15058 145 145 0 15404 0
[pid=32351] vsize: 62196
Current children cumulated CPU time (s) 178.82
Current children cumulated vsize (Kb) 64320

[startup+190.024 s]
Raw data (loadavg): 0.99 0.97 0.89 2/57 32351
Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32347/statm): 531 226 485 147 0 384 0
[pid=32347] vsize: 2124
Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 16343 0 0 0 18786 93 0 0 25 0 1 0 1793679033 66052096 15637 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32351/statm): 16126 15637 145 145 0 15981 0
[pid=32351] vsize: 64504
Current children cumulated CPU time (s) 188.79
Current children cumulated vsize (Kb) 66628

[startup+200.024 s]
Raw data (loadavg): 0.99 0.97 0.89 2/57 32351
Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32347/statm): 531 226 485 147 0 384 0
[pid=32347] vsize: 2124
Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 16890 0 0 0 19777 97 0 0 25 0 1 0 1793679033 68284416 16184 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32351/statm): 16671 16184 145 145 0 16526 0
[pid=32351] vsize: 66684
Current children cumulated CPU time (s) 198.74
Current children cumulated vsize (Kb) 68808

[startup+210.025 s]
Raw data (loadavg): 0.99 0.97 0.89 2/57 32351
Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32347/statm): 531 226 485 147 0 384 0
[pid=32347] vsize: 2124
Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 17689 0 0 0 20765 103 0 0 25 0 1 0 1793679033 71548928 16983 4294967295 134512640 135094434 3221224432 3221223024 134557518 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32351/statm): 17468 16983 145 145 0 17323 0
[pid=32351] vsize: 69872
Current children cumulated CPU time (s) 208.68
Current children cumulated vsize (Kb) 71996

[startup+220.026 s]
Raw data (loadavg): 0.99 0.97 0.89 2/57 32351
Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32347/statm): 531 226 485 147 0 384 0
[pid=32347] vsize: 2124
Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 18390 0 0 0 21755 107 0 0 25 0 1 0 1793679033 74416128 17684 4294967295 134512640 135094434 3221224432 3221223024 134556806 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32351/statm): 18168 17684 145 145 0 18023 0
[pid=32351] vsize: 72672
Current children cumulated CPU time (s) 218.62
Current children cumulated vsize (Kb) 74796

[startup+230.026 s]
Raw data (loadavg): 0.99 0.97 0.90 2/57 32351
Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32347/statm): 531 226 485 147 0 384 0
[pid=32347] vsize: 2124
Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 19047 0 0 0 22747 111 0 0 25 0 1 0 1793679033 77103104 18341 4294967295 134512640 135094434 3221224432 3221223056 134562104 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32351/statm): 18824 18341 145 145 0 18679 0
[pid=32351] vsize: 75296
Current children cumulated CPU time (s) 228.58
Current children cumulated vsize (Kb) 77420

[startup+240.027 s]
Raw data (loadavg): 0.99 0.97 0.90 2/57 32351
Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32347/statm): 531 226 485 147 0 384 0
[pid=32347] vsize: 2124
Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 19645 0 0 0 23738 113 0 0 25 0 1 0 1793679033 79544320 18939 4294967295 134512640 135094434 3221224432 3221223024 134557230 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32351/statm): 19420 18939 145 145 0 19275 0
[pid=32351] vsize: 77680
Current children cumulated CPU time (s) 238.51
Current children cumulated vsize (Kb) 79804

[startup+250.028 s]
Raw data (loadavg): 0.99 0.97 0.90 2/57 32351
Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32347/statm): 531 226 485 147 0 384 0
[pid=32347] vsize: 2124
Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 20260 0 0 0 24728 118 0 0 25 0 1 0 1793679033 82055168 19554 4294967295 134512640 135094434 3221224432 3221223104 134555811 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32351/statm): 20033 19554 145 145 0 19888 0
[pid=32351] vsize: 80132
Current children cumulated CPU time (s) 248.46
Current children cumulated vsize (Kb) 82256

[startup+260.029 s]
Raw data (loadavg): 0.99 0.97 0.90 2/57 32351
Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32347/statm): 531 226 485 147 0 384 0
[pid=32347] vsize: 2124
Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 20869 0 0 0 25719 122 0 0 25 0 1 0 1793679033 84549632 20163 4294967295 134512640 135094434 3221224432 3221223024 134557219 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32351/statm): 20642 20163 145 145 0 20497 0
[pid=32351] vsize: 82568
Current children cumulated CPU time (s) 258.41
Current children cumulated vsize (Kb) 84692

[startup+270.03 s]
Raw data (loadavg): 0.99 0.97 0.90 2/57 32351
Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32347/statm): 531 226 485 147 0 384 0
[pid=32347] vsize: 2124
Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 21418 0 0 0 26711 125 0 0 25 0 1 0 1793679033 86810624 20712 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32351/statm): 21194 20712 145 145 0 21049 0
[pid=32351] vsize: 84776
Current children cumulated CPU time (s) 268.36
Current children cumulated vsize (Kb) 86900

[startup+280.031 s]
Raw data (loadavg): 0.99 0.97 0.90 2/57 32351
Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32347/statm): 531 226 485 147 0 384 0
[pid=32347] vsize: 2124
Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 21858 0 0 0 27704 128 0 0 25 0 1 0 1793679033 88612864 21152 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32351/statm): 21634 21152 145 145 0 21489 0
[pid=32351] vsize: 86536
Current children cumulated CPU time (s) 278.32
Current children cumulated vsize (Kb) 88660

[startup+290.031 s]
Raw data (loadavg): 0.99 0.97 0.90 2/57 32351
Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32347/statm): 531 226 485 147 0 384 0
[pid=32347] vsize: 2124
Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 22406 0 0 0 28695 132 0 0 25 0 1 0 1793679033 90845184 21700 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32351/statm): 22179 21700 145 145 0 22034 0
[pid=32351] vsize: 88716
Current children cumulated CPU time (s) 288.27
Current children cumulated vsize (Kb) 90840

[startup+300.032 s]
Raw data (loadavg): 0.99 0.97 0.90 2/57 32351
Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32347/statm): 531 226 485 147 0 384 0
[pid=32347] vsize: 2124
Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 22985 0 0 0 29686 136 0 0 25 0 1 0 1793679033 93212672 22279 4294967295 134512640 135094434 3221224432 3221223088 134557950 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32351/statm): 22757 22279 145 145 0 22612 0
[pid=32351] vsize: 91028
Current children cumulated CPU time (s) 298.22
Current children cumulated vsize (Kb) 93152

[startup+310.033 s]
Raw data (loadavg): 0.99 0.97 0.90 2/57 32351
Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32347/statm): 531 226 485 147 0 384 0
[pid=32347] vsize: 2124
Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 23592 0 0 0 30676 140 0 0 25 0 1 0 1793679033 95690752 22886 4294967295 134512640 135094434 3221224432 3221223088 134558395 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32351/statm): 23362 22886 145 145 0 23217 0
[pid=32351] vsize: 93448
Current children cumulated CPU time (s) 308.16
Current children cumulated vsize (Kb) 95572

[startup+320.034 s]
Raw data (loadavg): 0.99 0.97 0.90 2/57 32351
Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32347/statm): 531 226 485 147 0 384 0
[pid=32347] vsize: 2124
Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 24035 0 0 0 31668 143 0 0 25 0 1 0 1793679033 97759232 23329 4294967295 134512640 135094434 3221224432 3221223088 134557890 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32351/statm): 23867 23329 145 145 0 23722 0
[pid=32351] vsize: 95468
Current children cumulated CPU time (s) 318.11
Current children cumulated vsize (Kb) 97592

[startup+330.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 32351
Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32347/statm): 531 226 485 147 0 384 0
[pid=32347] vsize: 2124
Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 24625 0 0 0 32660 147 0 0 25 0 1 0 1793679033 100167680 23919 4294967295 134512640 135094434 3221224432 3221223024 134556964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32351/statm): 24455 23919 145 145 0 24310 0
[pid=32351] vsize: 97820
Current children cumulated CPU time (s) 328.07
Current children cumulated vsize (Kb) 99944

[startup+340.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 32351
Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32347/statm): 531 226 485 147 0 384 0
[pid=32347] vsize: 2124
Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 25049 0 0 0 33653 150 0 0 25 0 1 0 1793679033 101896192 24343 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32351/statm): 24877 24343 145 145 0 24732 0
[pid=32351] vsize: 99508
Current children cumulated CPU time (s) 338.03
Current children cumulated vsize (Kb) 101632

[startup+350.037 s]
Raw data (loadavg): 0.99 0.97 0.91 1/57 32351
Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32347/statm): 531 226 485 147 0 384 0
[pid=32347] vsize: 2124
Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) T 32347 32347 6847 0 -1 0 25626 0 0 0 34645 153 0 0 25 0 1 0 1793679033 104251392 24920 4294967295 134512640 135094434 3221224432 3221222796 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/32351/statm): 25452 24920 145 145 0 25307 0
[pid=32351] vsize: 101808
Current children cumulated CPU time (s) 347.98
Current children cumulated vsize (Kb) 103932

[startup+360.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 32351
Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32347/statm): 531 226 485 147 0 384 0
[pid=32347] vsize: 2124
Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 26359 0 0 0 35634 157 0 0 21 0 1 0 1793679033 107261952 25653 4294967295 134512640 135094434 3221224432 3221223056 134557675 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32351/statm): 26187 25653 145 145 0 26042 0
[pid=32351] vsize: 104748
Current children cumulated CPU time (s) 357.91
Current children cumulated vsize (Kb) 106872

[startup+370.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 32351
Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32347/statm): 531 226 485 147 0 384 0
[pid=32347] vsize: 2124
Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 27119 0 0 0 36623 163 0 0 25 0 1 0 1793679033 110370816 26413 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32351/statm): 26946 26413 145 145 0 26801 0
[pid=32351] vsize: 107784
Current children cumulated CPU time (s) 367.86
Current children cumulated vsize (Kb) 109908

[startup+380.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 32351
Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32347/statm): 531 226 485 147 0 384 0
[pid=32347] vsize: 2124
Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 27655 0 0 0 37614 167 0 0 25 0 1 0 1793679033 112562176 26949 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32351/statm): 27481 26949 145 145 0 27336 0
[pid=32351] vsize: 109924
Current children cumulated CPU time (s) 377.81
Current children cumulated vsize (Kb) 112048

[startup+390.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 32351
Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32347/statm): 531 226 485 147 0 384 0
[pid=32347] vsize: 2124
Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 28009 0 0 0 38607 170 0 0 25 0 1 0 1793679033 113995776 27303 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32351/statm): 27831 27303 145 145 0 27686 0
[pid=32351] vsize: 111324
Current children cumulated CPU time (s) 387.77
Current children cumulated vsize (Kb) 113448

[startup+400.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 32351
Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32347/statm): 531 226 485 147 0 384 0
[pid=32347] vsize: 2124
Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 28474 0 0 0 39600 172 0 0 25 0 1 0 1793679033 115888128 27768 4294967295 134512640 135094434 3221224432 3221223024 134556978 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32351/statm): 28293 27768 145 145 0 28148 0
[pid=32351] vsize: 113172
Current children cumulated CPU time (s) 397.72
Current children cumulated vsize (Kb) 115296

[startup+410.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 32351
Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32347/statm): 531 226 485 147 0 384 0
[pid=32347] vsize: 2124
Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 28906 0 0 0 40594 175 0 0 25 0 1 0 1793679033 117649408 28200 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32351/statm): 28723 28200 145 145 0 28578 0
[pid=32351] vsize: 114892
Current children cumulated CPU time (s) 407.69
Current children cumulated vsize (Kb) 117016

[startup+420.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 32351
Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32347/statm): 531 226 485 147 0 384 0
[pid=32347] vsize: 2124
Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 29415 0 0 0 41586 178 0 0 25 0 1 0 1793679033 119726080 28709 4294967295 134512640 135094434 3221224432 3221223024 134556843 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32351/statm): 29230 28709 145 145 0 29085 0
[pid=32351] vsize: 116920
Current children cumulated CPU time (s) 417.64
Current children cumulated vsize (Kb) 119044

[startup+430.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 32351
Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32347/statm): 531 226 485 147 0 384 0
[pid=32347] vsize: 2124
Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 29957 0 0 0 42577 182 0 0 25 0 1 0 1793679033 121937920 29251 4294967295 134512640 135094434 3221224432 3221223056 134562085 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32351/statm): 29770 29251 145 145 0 29625 0
[pid=32351] vsize: 119080
Current children cumulated CPU time (s) 427.59
Current children cumulated vsize (Kb) 121204

[startup+440.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 32351
Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32347/statm): 531 226 485 147 0 384 0
[pid=32347] vsize: 2124
Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 30514 0 0 0 43568 185 0 0 25 0 1 0 1793679033 124211200 29808 4294967295 134512640 135094434 3221224432 3221223024 134557421 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32351/statm): 30325 29808 145 145 0 30180 0
[pid=32351] vsize: 121300
Current children cumulated CPU time (s) 437.53
Current children cumulated vsize (Kb) 123424

[startup+450.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 32351
Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32347/statm): 531 226 485 147 0 384 0
[pid=32347] vsize: 2124
Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 31224 0 0 0 44557 190 0 0 25 0 1 0 1793679033 127111168 30518 4294967295 134512640 135094434 3221224432 3221223088 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32351/statm): 31033 30518 145 145 0 30888 0
[pid=32351] vsize: 124132
Current children cumulated CPU time (s) 447.47
Current children cumulated vsize (Kb) 126256

[startup+460.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 32351
Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32347/statm): 531 226 485 147 0 384 0
[pid=32347] vsize: 2124
Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 31908 0 0 0 45545 195 0 0 25 0 1 0 1793679033 129904640 31202 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32351/statm): 31715 31202 145 145 0 31570 0
[pid=32351] vsize: 126860
Current children cumulated CPU time (s) 457.4
Current children cumulated vsize (Kb) 128984

[startup+470.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 32351
Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32347/statm): 531 226 485 147 0 384 0
[pid=32347] vsize: 2124
Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 32548 0 0 0 46535 200 0 0 25 0 1 0 1793679033 132521984 31842 4294967295 134512640 135094434 3221224432 3221223104 134555811 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32351/statm): 32354 31842 145 145 0 32209 0
[pid=32351] vsize: 129416
Current children cumulated CPU time (s) 467.35
Current children cumulated vsize (Kb) 131540

[startup+480.052 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 32351
Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32347/statm): 531 226 485 147 0 384 0
[pid=32347] vsize: 2124
Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 33119 0 0 0 47526 203 0 0 25 0 1 0 1793679033 134856704 32413 4294967295 134512640 135094434 3221224432 3221223072 134557059 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32351/statm): 32924 32413 145 145 0 32779 0
[pid=32351] vsize: 131696
Current children cumulated CPU time (s) 477.29
Current children cumulated vsize (Kb) 133820

[startup+490.052 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 32351
Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32347/statm): 531 226 485 147 0 384 0
[pid=32347] vsize: 2124
Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 33717 0 0 0 48515 207 0 0 25 0 1 0 1793679033 137310208 33011 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32351/statm): 33523 33011 145 145 0 33378 0
[pid=32351] vsize: 134092
Current children cumulated CPU time (s) 487.22
Current children cumulated vsize (Kb) 136216

[startup+500.053 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 32351
Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32347/statm): 531 226 485 147 0 384 0
[pid=32347] vsize: 2124
Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 34307 0 0 0 49506 211 0 0 25 0 1 0 1793679033 139718656 33601 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32351/statm): 34111 33601 145 145 0 33966 0
[pid=32351] vsize: 136444
Current children cumulated CPU time (s) 497.17
Current children cumulated vsize (Kb) 138568

[startup+510.054 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 32351
Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32347/statm): 531 226 485 147 0 384 0
[pid=32347] vsize: 2124
Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 34781 0 0 0 50500 214 0 0 25 0 1 0 1793679033 141651968 34075 4294967295 134512640 135094434 3221224432 3221223024 134556809 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32351/statm): 34583 34075 145 145 0 34438 0
[pid=32351] vsize: 138332
Current children cumulated CPU time (s) 507.14
Current children cumulated vsize (Kb) 140456

[startup+520.055 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 32351
Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32347/statm): 531 226 485 147 0 384 0
[pid=32347] vsize: 2124
Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 35338 0 0 0 51492 217 0 0 25 0 1 0 1793679033 143929344 34632 4294967295 134512640 135094434 3221224432 3221223088 134557875 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32351/statm): 35139 34632 145 145 0 34994 0
[pid=32351] vsize: 140556
Current children cumulated CPU time (s) 517.09
Current children cumulated vsize (Kb) 142680

[startup+530.056 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 32351
Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32347/statm): 531 226 485 147 0 384 0
[pid=32347] vsize: 2124
Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 35691 0 0 0 52485 219 0 0 25 0 1 0 1793679033 145371136 34985 4294967295 134512640 135094434 3221224432 3221223024 134557037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32351/statm): 35491 34985 145 145 0 35346 0
[pid=32351] vsize: 141964
Current children cumulated CPU time (s) 527.04
Current children cumulated vsize (Kb) 144088

[startup+540.057 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 32351
Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32347/statm): 531 226 485 147 0 384 0
[pid=32347] vsize: 2124
Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 36276 0 0 0 53477 223 0 0 25 0 1 0 1793679033 147750912 35570 4294967295 134512640 135094434 3221224432 3221223120 134554793 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32351/statm): 36072 35570 145 145 0 35927 0
[pid=32351] vsize: 144288
Current children cumulated CPU time (s) 537
Current children cumulated vsize (Kb) 146412

[startup+550.058 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 32351
Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32347/statm): 531 226 485 147 0 384 0
[pid=32347] vsize: 2124
Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 36787 0 0 0 54469 227 0 0 25 0 1 0 1793679033 149835776 36081 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32351/statm): 36581 36081 145 145 0 36436 0
[pid=32351] vsize: 146324
Current children cumulated CPU time (s) 546.96
Current children cumulated vsize (Kb) 148448

[startup+560.058 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 32351
Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32347/statm): 531 226 485 147 0 384 0
[pid=32347] vsize: 2124
Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 37113 0 0 0 55462 229 0 0 25 0 1 0 1793679033 151166976 36407 4294967295 134512640 135094434 3221224432 3221223088 134558210 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32351/statm): 36906 36407 145 145 0 36761 0
[pid=32351] vsize: 147624
Current children cumulated CPU time (s) 556.91
Current children cumulated vsize (Kb) 149748

[startup+570.059 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 32351
Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32347/statm): 531 226 485 147 0 384 0
[pid=32347] vsize: 2124
Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 37506 0 0 0 56456 232 0 0 25 0 1 0 1793679033 152768512 36800 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32351/statm): 37297 36800 145 145 0 37152 0
[pid=32351] vsize: 149188
Current children cumulated CPU time (s) 566.88
Current children cumulated vsize (Kb) 151312

[startup+580.059 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 32351
Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32347/statm): 531 226 485 147 0 384 0
[pid=32347] vsize: 2124
Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 37955 0 0 0 57448 235 0 0 25 0 1 0 1793679033 154603520 37249 4294967295 134512640 135094434 3221224432 3221223024 134556802 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32351/statm): 37745 37249 145 145 0 37600 0
[pid=32351] vsize: 150980
Current children cumulated CPU time (s) 576.83
Current children cumulated vsize (Kb) 153104

[startup+590.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 32351
Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32347/statm): 531 226 485 147 0 384 0
[pid=32347] vsize: 2124
Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 38500 0 0 0 58439 240 0 0 25 0 1 0 1793679033 156831744 37794 4294967295 134512640 135094434 3221224432 3221223064 134557561 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32351/statm): 38289 37794 145 145 0 38144 0
[pid=32351] vsize: 153156
Current children cumulated CPU time (s) 586.79
Current children cumulated vsize (Kb) 155280

[startup+600.061 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 32351
Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32347/statm): 531 226 485 147 0 384 0
[pid=32347] vsize: 2124
Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 39054 0 0 0 59431 244 0 0 25 0 1 0 1793679033 159092736 38348 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32351/statm): 38841 38348 145 145 0 38696 0
[pid=32351] vsize: 155364
Current children cumulated CPU time (s) 596.75
Current children cumulated vsize (Kb) 157488

[startup+610.063 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 32351
Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32347/statm): 531 226 485 147 0 384 0
[pid=32347] vsize: 2124
Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 39456 0 0 0 60426 246 0 0 25 0 1 0 1793679033 160735232 38750 4294967295 134512640 135094434 3221224432 3221223024 134557152 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32351/statm): 39242 38750 145 145 0 39097 0
[pid=32351] vsize: 156968
Current children cumulated CPU time (s) 606.72
Current children cumulated vsize (Kb) 159092

[startup+620.063 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 32351
Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32347/statm): 531 226 485 147 0 384 0
[pid=32347] vsize: 2124
Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 39456 0 0 0 61425 247 0 0 25 0 1 0 1793679033 160735232 38750 4294967295 134512640 135094434 3221224432 3221223024 134557004 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32351/statm): 39242 38750 145 145 0 39097 0
[pid=32351] vsize: 156968
Current children cumulated CPU time (s) 616.72
Current children cumulated vsize (Kb) 159092

[startup+630.063 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 32351
Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32347/statm): 531 226 485 147 0 384 0
[pid=32347] vsize: 2124
Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 39456 0 0 0 62425 247 0 0 25 0 1 0 1793679033 160735232 38750 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32351/statm): 39242 38750 145 145 0 39097 0
[pid=32351] vsize: 156968
Current children cumulated CPU time (s) 626.72
Current children cumulated vsize (Kb) 159092

[startup+640.065 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 32351
Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32347/statm): 531 226 485 147 0 384 0
[pid=32347] vsize: 2124
Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 39456 0 0 0 63424 247 0 0 25 0 1 0 1793679033 160735232 38750 4294967295 134512640 135094434 3221224432 3221223024 134556975 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32351/statm): 39242 38750 145 145 0 39097 0
[pid=32351] vsize: 156968
Current children cumulated CPU time (s) 636.71
Current children cumulated vsize (Kb) 159092

[startup+650.066 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 32351
Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32347/statm): 531 226 485 147 0 384 0
[pid=32347] vsize: 2124
Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 39456 0 0 0 64424 248 0 0 25 0 1 0 1793679033 160735232 38750 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32351/statm): 39242 38750 145 145 0 39097 0
[pid=32351] vsize: 156968
Current children cumulated CPU time (s) 646.72
Current children cumulated vsize (Kb) 159092

[startup+660.068 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 32351
Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32347/statm): 531 226 485 147 0 384 0
[pid=32347] vsize: 2124
Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 39456 0 0 0 65423 248 0 0 25 0 1 0 1793679033 160735232 38750 4294967295 134512640 135094434 3221224432 3221223088 134557792 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32351/statm): 39242 38750 145 145 0 39097 0
[pid=32351] vsize: 156968
Current children cumulated CPU time (s) 656.71
Current children cumulated vsize (Kb) 159092

[startup+670.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 32351
Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32347/statm): 531 226 485 147 0 384 0
[pid=32347] vsize: 2124
Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 39456 0 0 0 66423 248 0 0 25 0 1 0 1793679033 160735232 38750 4294967295 134512640 135094434 3221224432 3221223024 134557528 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32351/statm): 39242 38750 145 145 0 39097 0
[pid=32351] vsize: 156968
Current children cumulated CPU time (s) 666.71
Current children cumulated vsize (Kb) 159092

[startup+680.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 32351
Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32347/statm): 531 226 485 147 0 384 0
[pid=32347] vsize: 2124
Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 39456 0 0 0 67422 249 0 0 25 0 1 0 1793679033 160735232 38750 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32351/statm): 39242 38750 145 145 0 39097 0
[pid=32351] vsize: 156968
Current children cumulated CPU time (s) 676.71
Current children cumulated vsize (Kb) 159092

[startup+690.071 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 32351
Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32347/statm): 531 226 485 147 0 384 0
[pid=32347] vsize: 2124
Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 39456 0 0 0 68422 249 0 0 25 0 1 0 1793679033 160735232 38750 4294967295 134512640 135094434 3221224432 3221223088 134558019 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32351/statm): 39242 38750 145 145 0 39097 0
[pid=32351] vsize: 156968
Current children cumulated CPU time (s) 686.71
Current children cumulated vsize (Kb) 159092

[startup+700.071 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 32351
Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32347/statm): 531 226 485 147 0 384 0
[pid=32347] vsize: 2124
Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 39456 0 0 0 69422 250 0 0 25 0 1 0 1793679033 160735232 38750 4294967295 134512640 135094434 3221224432 3221223024 134556789 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32351/statm): 39242 38750 145 145 0 39097 0
[pid=32351] vsize: 156968
Current children cumulated CPU time (s) 696.72
Current children cumulated vsize (Kb) 159092

[startup+710.073 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 32351
Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32347/statm): 531 226 485 147 0 384 0
[pid=32347] vsize: 2124
Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 39456 0 0 0 70421 250 0 0 25 0 1 0 1793679033 160735232 38750 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32351/statm): 39242 38750 145 145 0 39097 0
[pid=32351] vsize: 156968
Current children cumulated CPU time (s) 706.71
Current children cumulated vsize (Kb) 159092

[startup+720.074 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 32351
Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32347/statm): 531 226 485 147 0 384 0
[pid=32347] vsize: 2124
Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 39456 0 0 0 71421 250 0 0 25 0 1 0 1793679033 160735232 38750 4294967295 134512640 135094434 3221224432 3221223072 134558048 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32351/statm): 39242 38750 145 145 0 39097 0
[pid=32351] vsize: 156968
Current children cumulated CPU time (s) 716.71
Current children cumulated vsize (Kb) 159092

[startup+730.075 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 32351
Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32347/statm): 531 226 485 147 0 384 0
[pid=32347] vsize: 2124
Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 39456 0 0 0 72421 251 0 0 25 0 1 0 1793679033 160735232 38750 4294967295 134512640 135094434 3221224432 3221223024 134556941 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32351/statm): 39242 38750 145 145 0 39097 0
[pid=32351] vsize: 156968
Current children cumulated CPU time (s) 726.72
Current children cumulated vsize (Kb) 159092

[startup+740.076 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 32351
Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32347/statm): 531 226 485 147 0 384 0
[pid=32347] vsize: 2124
Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 39456 0 0 0 73420 251 0 0 25 0 1 0 1793679033 160735232 38750 4294967295 134512640 135094434 3221224432 3221223024 134557300 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32351/statm): 39242 38750 145 145 0 39097 0
[pid=32351] vsize: 156968
Current children cumulated CPU time (s) 736.71
Current children cumulated vsize (Kb) 159092

[startup+750.077 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 32351
Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32347/statm): 531 226 485 147 0 384 0
[pid=32347] vsize: 2124
Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 39456 0 0 0 74420 251 0 0 25 0 1 0 1793679033 160735232 38750 4294967295 134512640 135094434 3221224432 3221223104 134556454 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32351/statm): 39242 38750 145 145 0 39097 0
[pid=32351] vsize: 156968
Current children cumulated CPU time (s) 746.71
Current children cumulated vsize (Kb) 159092

[startup+760.079 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 32351
Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32347/statm): 531 226 485 147 0 384 0
[pid=32347] vsize: 2124
Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 39456 0 0 0 75419 252 0 0 25 0 1 0 1793679033 160735232 38750 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32351/statm): 39242 38750 145 145 0 39097 0
[pid=32351] vsize: 156968
Current children cumulated CPU time (s) 756.71
Current children cumulated vsize (Kb) 159092

[startup+770.079 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 32351
Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32347/statm): 531 226 485 147 0 384 0
[pid=32347] vsize: 2124
Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 39456 0 0 0 76419 252 0 0 25 0 1 0 1793679033 160735232 38750 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32351/statm): 39242 38750 145 145 0 39097 0
[pid=32351] vsize: 156968
Current children cumulated CPU time (s) 766.71
Current children cumulated vsize (Kb) 159092

[startup+780.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 32351
Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32347/statm): 531 226 485 147 0 384 0
[pid=32347] vsize: 2124
Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 39456 0 0 0 77419 252 0 0 25 0 1 0 1793679033 160735232 38750 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32351/statm): 39242 38750 145 145 0 39097 0
[pid=32351] vsize: 156968
Current children cumulated CPU time (s) 776.71
Current children cumulated vsize (Kb) 159092

[startup+790.081 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 32351
Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32347/statm): 531 226 485 147 0 384 0
[pid=32347] vsize: 2124
Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 39456 0 0 0 78417 254 0 0 25 0 1 0 1793679033 160735232 38750 4294967295 134512640 135094434 3221224432 3221223088 134557875 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32351/statm): 39242 38750 145 145 0 39097 0
[pid=32351] vsize: 156968
Current children cumulated CPU time (s) 786.71
Current children cumulated vsize (Kb) 159092

[startup+800.082 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 32351
Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32347/statm): 531 226 485 147 0 384 0
[pid=32347] vsize: 2124
Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 39456 0 0 0 79416 255 0 0 25 0 1 0 1793679033 160735232 38750 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32351/statm): 39242 38750 145 145 0 39097 0
[pid=32351] vsize: 156968
Current children cumulated CPU time (s) 796.71
Current children cumulated vsize (Kb) 159092

[startup+810.084 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 32351
Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32347/statm): 531 226 485 147 0 384 0
[pid=32347] vsize: 2124
Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 39456 0 0 0 80415 256 0 0 25 0 1 0 1793679033 160735232 38750 4294967295 134512640 135094434 3221224432 3221223024 134556982 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32351/statm): 39242 38750 145 145 0 39097 0
[pid=32351] vsize: 156968
Current children cumulated CPU time (s) 806.71
Current children cumulated vsize (Kb) 159092

[startup+820.085 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 32351
Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32347/statm): 531 226 485 147 0 384 0
[pid=32347] vsize: 2124
Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 39456 0 0 0 81414 257 0 0 25 0 1 0 1793679033 160735232 38750 4294967295 134512640 135094434 3221224432 3221223104 134555568 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32351/statm): 39242 38750 145 145 0 39097 0
[pid=32351] vsize: 156968
Current children cumulated CPU time (s) 816.71
Current children cumulated vsize (Kb) 159092

[startup+830.085 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 32351
Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32347/statm): 531 226 485 147 0 384 0
[pid=32347] vsize: 2124
Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 39456 0 0 0 82414 257 0 0 25 0 1 0 1793679033 160735232 38750 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32351/statm): 39242 38750 145 145 0 39097 0
[pid=32351] vsize: 156968
Current children cumulated CPU time (s) 826.71
Current children cumulated vsize (Kb) 159092

[startup+840.087 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 32351
Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32347/statm): 531 226 485 147 0 384 0
[pid=32347] vsize: 2124
Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 39456 0 0 0 83413 258 0 0 25 0 1 0 1793679033 160735232 38750 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32351/statm): 39242 38750 145 145 0 39097 0
[pid=32351] vsize: 156968
Current children cumulated CPU time (s) 836.71
Current children cumulated vsize (Kb) 159092

[startup+850.087 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 32351
Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32347/statm): 531 226 485 147 0 384 0
[pid=32347] vsize: 2124
Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 39456 0 0 0 84412 259 0 0 25 0 1 0 1793679033 160735232 38750 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32351/statm): 39242 38750 145 145 0 39097 0
[pid=32351] vsize: 156968
Current children cumulated CPU time (s) 846.71
Current children cumulated vsize (Kb) 159092

[startup+860.088 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 32351
Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32347/statm): 531 226 485 147 0 384 0
[pid=32347] vsize: 2124
Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 39456 0 0 0 85412 259 0 0 25 0 1 0 1793679033 160735232 38750 4294967295 134512640 135094434 3221224432 3221223088 134558235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32351/statm): 39242 38750 145 145 0 39097 0
[pid=32351] vsize: 156968
Current children cumulated CPU time (s) 856.71
Current children cumulated vsize (Kb) 159092

[startup+870.089 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 32351
Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32347/statm): 531 226 485 147 0 384 0
[pid=32347] vsize: 2124
Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 39456 0 0 0 86411 260 0 0 25 0 1 0 1793679033 160735232 38750 4294967295 134512640 135094434 3221224432 3221223024 134557232 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32351/statm): 39242 38750 145 145 0 39097 0
[pid=32351] vsize: 156968
Current children cumulated CPU time (s) 866.71
Current children cumulated vsize (Kb) 159092

[startup+880.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 32351
Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32347/statm): 531 226 485 147 0 384 0
[pid=32347] vsize: 2124
Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 39456 0 0 0 87411 260 0 0 25 0 1 0 1793679033 160735232 38750 4294967295 134512640 135094434 3221224432 3221223088 134557866 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32351/statm): 39242 38750 145 145 0 39097 0
[pid=32351] vsize: 156968
Current children cumulated CPU time (s) 876.71
Current children cumulated vsize (Kb) 159092

[startup+890.091 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 32351
Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32347/statm): 531 226 485 147 0 384 0
[pid=32347] vsize: 2124
Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 39456 0 0 0 88411 260 0 0 25 0 1 0 1793679033 160735232 38750 4294967295 134512640 135094434 3221224432 3221223088 134557893 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32351/statm): 39242 38750 145 145 0 39097 0
[pid=32351] vsize: 156968
Current children cumulated CPU time (s) 886.71
Current children cumulated vsize (Kb) 159092

[startup+900.092 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 32351
Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32347/statm): 531 226 485 147 0 384 0
[pid=32347] vsize: 2124
Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 39456 0 0 0 89410 260 0 0 25 0 1 0 1793679033 160735232 38750 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32351/statm): 39242 38750 145 145 0 39097 0
[pid=32351] vsize: 156968
Current children cumulated CPU time (s) 896.7
Current children cumulated vsize (Kb) 159092

[startup+910.094 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 32351
Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32347/statm): 531 226 485 147 0 384 0
[pid=32347] vsize: 2124
Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 39456 0 0 0 90410 261 0 0 25 0 1 0 1793679033 160735232 38750 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32351/statm): 39242 38750 145 145 0 39097 0
[pid=32351] vsize: 156968
Current children cumulated CPU time (s) 906.71
Current children cumulated vsize (Kb) 159092

[startup+920.095 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 32351
Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32347/statm): 531 226 485 147 0 384 0
[pid=32347] vsize: 2124
Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 39456 0 0 0 91410 261 0 0 25 0 1 0 1793679033 160735232 38750 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32351/statm): 39242 38750 145 145 0 39097 0
[pid=32351] vsize: 156968
Current children cumulated CPU time (s) 916.71
Current children cumulated vsize (Kb) 159092

[startup+930.094 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 32351
Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32347/statm): 531 226 485 147 0 384 0
[pid=32347] vsize: 2124
Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 39456 0 0 0 92409 262 0 0 25 0 1 0 1793679033 160735232 38750 4294967295 134512640 135094434 3221224432 3221223024 134557016 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32351/statm): 39242 38750 145 145 0 39097 0
[pid=32351] vsize: 156968
Current children cumulated CPU time (s) 926.71
Current children cumulated vsize (Kb) 159092

[startup+940.096 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 32351
Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32347/statm): 531 226 485 147 0 384 0
[pid=32347] vsize: 2124
Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 39456 0 0 0 93409 262 0 0 25 0 1 0 1793679033 160735232 38750 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32351/statm): 39242 38750 145 145 0 39097 0
[pid=32351] vsize: 156968
Current children cumulated CPU time (s) 936.71
Current children cumulated vsize (Kb) 159092

[startup+950.097 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 32351
Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32347/statm): 531 226 485 147 0 384 0
[pid=32347] vsize: 2124
Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 39456 0 0 0 94409 262 0 0 25 0 1 0 1793679033 160735232 38750 4294967295 134512640 135094434 3221224432 3221223024 134557022 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32351/statm): 39242 38750 145 145 0 39097 0
[pid=32351] vsize: 156968
Current children cumulated CPU time (s) 946.71
Current children cumulated vsize (Kb) 159092

[startup+960.099 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 32351
Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32347/statm): 531 226 485 147 0 384 0
[pid=32347] vsize: 2124
Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 39456 0 0 0 95408 262 0 0 25 0 1 0 1793679033 160735232 38750 4294967295 134512640 135094434 3221224432 3221223024 134557537 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32351/statm): 39242 38750 145 145 0 39097 0
[pid=32351] vsize: 156968
Current children cumulated CPU time (s) 956.7
Current children cumulated vsize (Kb) 159092

[startup+970.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 32351
Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32347/statm): 531 226 485 147 0 384 0
[pid=32347] vsize: 2124
Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 39456 0 0 0 96408 263 0 0 25 0 1 0 1793679033 160735232 38750 4294967295 134512640 135094434 3221224432 3221223056 134557696 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32351/statm): 39242 38750 145 145 0 39097 0
[pid=32351] vsize: 156968
Current children cumulated CPU time (s) 966.71
Current children cumulated vsize (Kb) 159092

[startup+980.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 32351
Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32347/statm): 531 226 485 147 0 384 0
[pid=32347] vsize: 2124
Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 39456 0 0 0 97407 263 0 0 25 0 1 0 1793679033 160735232 38750 4294967295 134512640 135094434 3221224432 3221223088 134557829 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32351/statm): 39242 38750 145 145 0 39097 0
[pid=32351] vsize: 156968
Current children cumulated CPU time (s) 976.7
Current children cumulated vsize (Kb) 159092

[startup+990.101 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 32351
Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32347/statm): 531 226 485 147 0 384 0
[pid=32347] vsize: 2124
Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 39456 0 0 0 98406 264 0 0 25 0 1 0 1793679033 160735232 38750 4294967295 134512640 135094434 3221224432 3221223024 134556789 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32351/statm): 39242 38750 145 145 0 39097 0
[pid=32351] vsize: 156968
Current children cumulated CPU time (s) 986.7
Current children cumulated vsize (Kb) 159092

[startup+1000.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 32351
Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32347/statm): 531 226 485 147 0 384 0
[pid=32347] vsize: 2124
Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 39456 0 0 0 99406 264 0 0 25 0 1 0 1793679033 160735232 38750 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32351/statm): 39242 38750 145 145 0 39097 0
[pid=32351] vsize: 156968
Current children cumulated CPU time (s) 996.7
Current children cumulated vsize (Kb) 159092

[startup+1010.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 32351
Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32347/statm): 531 226 485 147 0 384 0
[pid=32347] vsize: 2124
Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 39456 0 0 0 100406 264 0 0 25 0 1 0 1793679033 160735232 38750 4294967295 134512640 135094434 3221224432 3221223024 134556785 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32351/statm): 39242 38750 145 145 0 39097 0
[pid=32351] vsize: 156968
Current children cumulated CPU time (s) 1006.7
Current children cumulated vsize (Kb) 159092

[startup+1020.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 32351
Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32347/statm): 531 226 485 147 0 384 0
[pid=32347] vsize: 2124
Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 39456 0 0 0 101405 265 0 0 25 0 1 0 1793679033 160735232 38750 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32351/statm): 39242 38750 145 145 0 39097 0
[pid=32351] vsize: 156968
Current children cumulated CPU time (s) 1016.7
Current children cumulated vsize (Kb) 159092

[startup+1030.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 32351
Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32347/statm): 531 226 485 147 0 384 0
[pid=32347] vsize: 2124
Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 39456 0 0 0 102405 265 0 0 25 0 1 0 1793679033 160735232 38750 4294967295 134512640 135094434 3221224432 3221223024 134556812 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32351/statm): 39242 38750 145 145 0 39097 0
[pid=32351] vsize: 156968
Current children cumulated CPU time (s) 1026.7
Current children cumulated vsize (Kb) 159092

[startup+1040.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 32351
Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32347/statm): 531 226 485 147 0 384 0
[pid=32347] vsize: 2124
Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 39456 0 0 0 103404 266 0 0 25 0 1 0 1793679033 160735232 38750 4294967295 134512640 135094434 3221224432 3221223024 134556802 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32351/statm): 39242 38750 145 145 0 39097 0
[pid=32351] vsize: 156968
Current children cumulated CPU time (s) 1036.7
Current children cumulated vsize (Kb) 159092

[startup+1050.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 32351
Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32347/statm): 531 226 485 147 0 384 0
[pid=32347] vsize: 2124
Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 39456 0 0 0 104404 266 0 0 25 0 1 0 1793679033 160735232 38750 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32351/statm): 39242 38750 145 145 0 39097 0
[pid=32351] vsize: 156968
Current children cumulated CPU time (s) 1046.7
Current children cumulated vsize (Kb) 159092

[startup+1060.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 32351
Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32347/statm): 531 226 485 147 0 384 0
[pid=32347] vsize: 2124
Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 39456 0 0 0 105404 266 0 0 25 0 1 0 1793679033 160735232 38750 4294967295 134512640 135094434 3221224432 3221223088 134558019 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32351/statm): 39242 38750 145 145 0 39097 0
[pid=32351] vsize: 156968
Current children cumulated CPU time (s) 1056.7
Current children cumulated vsize (Kb) 159092

[startup+1070.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 32351
Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32347/statm): 531 226 485 147 0 384 0
[pid=32347] vsize: 2124
Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 39456 0 0 0 106403 267 0 0 25 0 1 0 1793679033 160735232 38750 4294967295 134512640 135094434 3221224432 3221223088 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32351/statm): 39242 38750 145 145 0 39097 0
[pid=32351] vsize: 156968
Current children cumulated CPU time (s) 1066.7
Current children cumulated vsize (Kb) 159092

[startup+1080.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 32351
Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32347/statm): 531 226 485 147 0 384 0
[pid=32347] vsize: 2124
Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 39456 0 0 0 107402 268 0 0 25 0 1 0 1793679033 160735232 38750 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32351/statm): 39242 38750 145 145 0 39097 0
[pid=32351] vsize: 156968
Current children cumulated CPU time (s) 1076.7
Current children cumulated vsize (Kb) 159092

[startup+1090.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 32351
Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32347/statm): 531 226 485 147 0 384 0
[pid=32347] vsize: 2124
Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 39456 0 0 0 108402 268 0 0 25 0 1 0 1793679033 160735232 38750 4294967295 134512640 135094434 3221224432 3221223024 134557037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32351/statm): 39242 38750 145 145 0 39097 0
[pid=32351] vsize: 156968
Current children cumulated CPU time (s) 1086.7
Current children cumulated vsize (Kb) 159092

[startup+1100.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 32351
Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32347/statm): 531 226 485 147 0 384 0
[pid=32347] vsize: 2124
Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 39456 0 0 0 109402 268 0 0 25 0 1 0 1793679033 160735232 38750 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32351/statm): 39242 38750 145 145 0 39097 0
[pid=32351] vsize: 156968
Current children cumulated CPU time (s) 1096.7
Current children cumulated vsize (Kb) 159092

[startup+1110.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 32351
Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32347/statm): 531 226 485 147 0 384 0
[pid=32347] vsize: 2124
Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 39554 0 0 0 110400 269 0 0 25 0 1 0 1793679033 161136640 38848 4294967295 134512640 135094434 3221224432 3221223088 134558126 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32351/statm): 39340 38848 145 145 0 39195 0
[pid=32351] vsize: 157360
Current children cumulated CPU time (s) 1106.69
Current children cumulated vsize (Kb) 159484

[startup+1120.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 32351
Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32347/statm): 531 226 485 147 0 384 0
[pid=32347] vsize: 2124
Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 39960 0 0 0 111394 271 0 0 25 0 1 0 1793679033 162799616 39254 4294967295 134512640 135094434 3221224432 3221223024 134557512 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32351/statm): 39746 39254 145 145 0 39601 0
[pid=32351] vsize: 158984
Current children cumulated CPU time (s) 1116.65
Current children cumulated vsize (Kb) 161108

[startup+1130.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 32351
Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32347/statm): 531 226 485 147 0 384 0
[pid=32347] vsize: 2124
Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 40355 0 0 0 112388 274 0 0 25 0 1 0 1793679033 164417536 39649 4294967295 134512640 135094434 3221224432 3221223024 134556812 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32351/statm): 40141 39649 145 145 0 39996 0
[pid=32351] vsize: 160564
Current children cumulated CPU time (s) 1126.62
Current children cumulated vsize (Kb) 162688

[startup+1140.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 32351
Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32347/statm): 531 226 485 147 0 384 0
[pid=32347] vsize: 2124
Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 41050 0 0 0 113380 278 0 0 25 0 1 0 1793679033 167256064 40344 4294967295 134512640 135094434 3221224432 3221223024 134557219 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32351/statm): 40834 40344 145 145 0 40689 0
[pid=32351] vsize: 163336
Current children cumulated CPU time (s) 1136.58
Current children cumulated vsize (Kb) 165460

[startup+1150.12 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 32351
Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32347/statm): 531 226 485 147 0 384 0
[pid=32347] vsize: 2124
Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 41523 0 0 0 114374 280 0 0 25 0 1 0 1793679033 169193472 40817 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32351/statm): 41307 40817 145 145 0 41162 0
[pid=32351] vsize: 165228
Current children cumulated CPU time (s) 1146.54
Current children cumulated vsize (Kb) 167352

[startup+1160.12 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 32351
Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32347/statm): 531 226 485 147 0 384 0
[pid=32347] vsize: 2124
Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 42084 0 0 0 115368 283 0 0 25 0 1 0 1793679033 171491328 41378 4294967295 134512640 135094434 3221224432 3221223024 134557522 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32351/statm): 41868 41378 145 145 0 41723 0
[pid=32351] vsize: 167472
Current children cumulated CPU time (s) 1156.51
Current children cumulated vsize (Kb) 169596

[startup+1170.12 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 32351
Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32347/statm): 531 226 485 147 0 384 0
[pid=32347] vsize: 2124
Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 42549 0 0 0 116363 285 0 0 25 0 1 0 1793679033 173387776 41843 4294967295 134512640 135094434 3221224432 3221223024 134556990 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32351/statm): 42331 41843 145 145 0 42186 0
[pid=32351] vsize: 169324
Current children cumulated CPU time (s) 1166.48
Current children cumulated vsize (Kb) 171448

[startup+1180.12 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 32351
Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32347/statm): 531 226 485 147 0 384 0
[pid=32347] vsize: 2124
Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 43048 0 0 0 117356 288 0 0 25 0 1 0 1793679033 175427584 42342 4294967295 134512640 135094434 3221224432 3221223024 134557273 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32351/statm): 42829 42342 145 145 0 42684 0
[pid=32351] vsize: 171316
Current children cumulated CPU time (s) 1176.44
Current children cumulated vsize (Kb) 173440

[startup+1190.12 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 32351
Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32347/statm): 531 226 485 147 0 384 0
[pid=32347] vsize: 2124
Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 43769 0 0 0 118348 291 0 0 25 0 1 0 1793679033 178376704 43063 4294967295 134512640 135094434 3221224432 3221223024 134556904 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32351/statm): 43549 43063 145 145 0 43404 0
[pid=32351] vsize: 174196
Current children cumulated CPU time (s) 1186.39
Current children cumulated vsize (Kb) 176320

[startup+1200.12 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 32351
Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32347/statm): 531 226 485 147 0 384 0
[pid=32347] vsize: 2124
Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 44502 0 0 0 119338 296 0 0 23 0 1 0 1793679033 181374976 43796 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32351/statm): 44281 43796 145 145 0 44136 0
[pid=32351] vsize: 177124
Current children cumulated CPU time (s) 1196.34
Current children cumulated vsize (Kb) 179248

[startup+1210.12 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 32351
Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32347/statm): 531 226 485 147 0 384 0
[pid=32347] vsize: 2124
Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 45116 0 0 0 120329 300 0 0 25 0 1 0 1793679033 183885824 44410 4294967295 134512640 135094434 3221224432 3221223024 134557219 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32351/statm): 44894 44410 145 145 0 44749 0
[pid=32351] vsize: 179576
Current children cumulated CPU time (s) 1206.29
Current children cumulated vsize (Kb) 181700



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.12 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 32351
Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/32347/statm): 531 226 485 147 0 384 0
[pid=32347] vsize: 2124
Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 45116 0 0 0 120329 300 0 0 25 0 1 0 1793679033 183885824 44410 4294967295 134512640 135094434 3221224432 3221223024 134556791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32351/statm): 44894 44410 145 145 0 44749 0
[pid=32351] vsize: 179576
Current children cumulated CPU time (s) 1206.29
Current children cumulated vsize (Kb) 181700

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

Child status: 0
Real time (s): 1210.21
CPU time (s): 1206.38
CPU user time (s): 1203.3
CPU system time (s): 3.08453
CPU usage (%): 99.684
Max. virtual memory (cumulated for all children) (Kb): 181700

Verifier Data

ERROR: no interpretation found !