Some explanations

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

General information on the benchmark

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

Trace number 6097

Launcher Data

LAUNCH ON wulflinc4 THE 2005-09-20 03:15:25 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3253 boxname=wulflinc4 idbench=909 idsolver=3 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  4f0cac14ed3568050c2c57bb69fdb664  /oldhome/oroussel/tmp/wulflinc4/normalized-mps-v2-13-7-mod010.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc4/normalized-mps-v2-13-7-mod010.opb
IDLAUNCH: 3253
/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:        880336 kB
Buffers:         33512 kB
Cached:          94352 kB
SwapCached:        860 kB
Active:          37400 kB
Inactive:        93000 kB
HighTotal:      131008 kB
HighFree:        38108 kB
LowTotal:       903652 kB
LowFree:        842228 kB
SwapTotal:     2097136 kB
SwapFree:      2095644 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5520 kB
Slab:            18340 kB
Committed_AS:    72360 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-09-20 03:35:35 (client local time) WITH STATUS 0 IN 1206.32 SECONDS
stats: 3253 7 1206.32 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/8785/stat): 8785 (minisat+_script) R 8784 8785 6847 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1796977982 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 1 0 0
Raw data (/proc/8785/statm): 174 3 169 147 0 27 0
[pid=8785] 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=8786
New process pid=8787
New process pid=8788
execve syscall for /bin/sed executable
One traced child (pid=8787) exited with status: 0
open syscall for file /etc/ld.so.preload
open syscall for file tls/i686/mmx/libc.so.6
open syscall for file tls/i686/libc.so.6
open syscall for file tls/mmx/libc.so.6
open syscall for file tls/libc.so.6
open syscall for file i686/mmx/libc.so.6
open syscall for file i686/libc.so.6
open syscall for file mmx/libc.so.6
open syscall for file libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/i686/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/i686/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/libc.so.6
open syscall for file /oldhome/oroussel/lib/i686/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/i686/libc.so.6
open syscall for file /oldhome/oroussel/lib/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/libc.so.6
open syscall for file /etc/ld.so.cache
open syscall for file /lib/tls/libc.so.6
One traced child (pid=8788) exited with status: 0
One traced child (pid=8786) exited with status: 0
New process pid=8789
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-13-7-mod010.opb

[startup+10.004 s]
Raw data (loadavg): 1.03 0.97 0.73 2/57 8789
Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8785/statm): 531 226 485 147 0 384 0
[pid=8785] vsize: 2124
Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 5208 0 0 0 957 20 0 0 25 0 1 0 1796977987 20312064 4502 4294967295 134512640 135094434 3221224432 3221223024 134557028 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8789/statm): 4959 4502 145 145 0 4814 0
[pid=8789] vsize: 19836
Current children cumulated CPU time (s) 9.78
Current children cumulated vsize (Kb) 21960

[startup+20.0049 s]
Raw data (loadavg): 1.03 0.97 0.73 2/57 8789
Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8785/statm): 531 226 485 147 0 384 0
[pid=8785] vsize: 2124
Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 5774 0 0 0 1946 25 0 0 25 0 1 0 1796977987 22630400 5068 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8789/statm): 5525 5068 145 145 0 5380 0
[pid=8789] vsize: 22100
Current children cumulated CPU time (s) 19.72
Current children cumulated vsize (Kb) 24224

[startup+30.0067 s]
Raw data (loadavg): 1.02 0.97 0.73 2/57 8789
Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8785/statm): 531 226 485 147 0 384 0
[pid=8785] vsize: 2124
Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 6325 0 0 0 2938 28 0 0 25 0 1 0 1796977987 24911872 5619 4294967295 134512640 135094434 3221224432 3221223104 134555574 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8789/statm): 6082 5619 145 145 0 5937 0
[pid=8789] vsize: 24328
Current children cumulated CPU time (s) 29.67
Current children cumulated vsize (Kb) 26452

[startup+40.0076 s]
Raw data (loadavg): 1.02 0.97 0.73 2/57 8789
Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8785/statm): 531 226 485 147 0 384 0
[pid=8785] vsize: 2124
Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 7078 0 0 0 3926 32 0 0 25 0 1 0 1796977987 27983872 6372 4294967295 134512640 135094434 3221224432 3221223024 134557273 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8789/statm): 6832 6372 145 145 0 6687 0
[pid=8789] vsize: 27328
Current children cumulated CPU time (s) 39.59
Current children cumulated vsize (Kb) 29452

[startup+50.0084 s]
Raw data (loadavg): 1.02 0.97 0.74 2/57 8789
Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8785/statm): 531 226 485 147 0 384 0
[pid=8785] vsize: 2124
Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 7812 0 0 0 4915 37 0 0 25 0 1 0 1796977987 30982144 7106 4294967295 134512640 135094434 3221224432 3221223024 134557031 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8789/statm): 7564 7106 145 145 0 7419 0
[pid=8789] vsize: 30256
Current children cumulated CPU time (s) 49.53
Current children cumulated vsize (Kb) 32380

[startup+60.0093 s]
Raw data (loadavg): 1.01 0.97 0.74 2/57 8789
Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8785/statm): 531 226 485 147 0 384 0
[pid=8785] vsize: 2124
Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 8438 0 0 0 5903 41 0 0 25 0 1 0 1796977987 33595392 7732 4294967295 134512640 135094434 3221224432 3221223024 134557230 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8789/statm): 8202 7732 145 145 0 8057 0
[pid=8789] vsize: 32808
Current children cumulated CPU time (s) 59.45
Current children cumulated vsize (Kb) 34932

[startup+70.0101 s]
Raw data (loadavg): 1.01 0.97 0.74 2/57 8789
Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8785/statm): 531 226 485 147 0 384 0
[pid=8785] vsize: 2124
Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 9075 0 0 0 6893 45 0 0 25 0 1 0 1796977987 36196352 8369 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8789/statm): 8837 8369 145 145 0 8692 0
[pid=8789] vsize: 35348
Current children cumulated CPU time (s) 69.39
Current children cumulated vsize (Kb) 37472

[startup+80.012 s]
Raw data (loadavg): 1.01 0.97 0.74 2/57 8789
Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8785/statm): 531 226 485 147 0 384 0
[pid=8785] vsize: 2124
Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 9676 0 0 0 7883 49 0 0 25 0 1 0 1796977987 38649856 8970 4294967295 134512640 135094434 3221224432 3221223024 134556969 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8789/statm): 9436 8970 145 145 0 9291 0
[pid=8789] vsize: 37744
Current children cumulated CPU time (s) 79.33
Current children cumulated vsize (Kb) 39868

[startup+90.0128 s]
Raw data (loadavg): 1.01 0.97 0.74 2/57 8789
Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8785/statm): 531 226 485 147 0 384 0
[pid=8785] vsize: 2124
Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 10273 0 0 0 8874 52 0 0 25 0 1 0 1796977987 41095168 9567 4294967295 134512640 135094434 3221224432 3221223088 134558178 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8789/statm): 10033 9567 145 145 0 9888 0
[pid=8789] vsize: 40132
Current children cumulated CPU time (s) 89.27
Current children cumulated vsize (Kb) 42256

[startup+100.013 s]
Raw data (loadavg): 1.00 0.97 0.75 1/57 8789
Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8785/statm): 531 226 485 147 0 384 0
[pid=8785] vsize: 2124
Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) T 8785 8785 6847 0 -1 0 10807 0 0 0 9865 55 0 0 25 0 1 0 1796977987 43282432 10101 4294967295 134512640 135094434 3221224432 3221222796 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/8789/statm): 10567 10101 145 145 0 10422 0
[pid=8789] vsize: 42268
Current children cumulated CPU time (s) 99.21
Current children cumulated vsize (Kb) 44392

[startup+110.013 s]
Raw data (loadavg): 1.00 0.97 0.75 2/57 8789
Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8785/statm): 531 226 485 147 0 384 0
[pid=8785] vsize: 2124
Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 11346 0 0 0 10857 59 0 0 25 0 1 0 1796977987 45498368 10640 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8789/statm): 11108 10640 145 145 0 10963 0
[pid=8789] vsize: 44432
Current children cumulated CPU time (s) 109.17
Current children cumulated vsize (Kb) 46556

[startup+120.014 s]
Raw data (loadavg): 1.00 0.97 0.75 2/57 8789
Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8785/statm): 531 226 485 147 0 384 0
[pid=8785] vsize: 2124
Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 11929 0 0 0 11848 61 0 0 25 0 1 0 1796977987 47890432 11223 4294967295 134512640 135094434 3221224432 3221223024 134556999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8789/statm): 11692 11223 145 145 0 11547 0
[pid=8789] vsize: 46768
Current children cumulated CPU time (s) 119.1
Current children cumulated vsize (Kb) 48892

[startup+130.015 s]
Raw data (loadavg): 1.00 0.97 0.75 2/57 8789
Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8785/statm): 531 226 485 147 0 384 0
[pid=8785] vsize: 2124
Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 12627 0 0 0 12836 67 0 0 25 0 1 0 1796977987 50741248 11921 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8789/statm): 12388 11921 145 145 0 12243 0
[pid=8789] vsize: 49552
Current children cumulated CPU time (s) 129.04
Current children cumulated vsize (Kb) 51676

[startup+140.016 s]
Raw data (loadavg): 1.00 0.97 0.75 2/57 8789
Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8785/statm): 531 226 485 147 0 384 0
[pid=8785] vsize: 2124
Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 13299 0 0 0 13825 70 0 0 25 0 1 0 1796977987 53485568 12593 4294967295 134512640 135094434 3221224432 3221223024 134557273 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8789/statm): 13058 12593 145 145 0 12913 0
[pid=8789] vsize: 52232
Current children cumulated CPU time (s) 138.96
Current children cumulated vsize (Kb) 54356

[startup+150.017 s]
Raw data (loadavg): 1.00 0.97 0.76 2/57 8789
Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8785/statm): 531 226 485 147 0 384 0
[pid=8785] vsize: 2124
Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 13952 0 0 0 14814 75 0 0 25 0 1 0 1796977987 56156160 13246 4294967295 134512640 135094434 3221224432 3221223104 134556073 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8789/statm): 13710 13246 145 145 0 13565 0
[pid=8789] vsize: 54840
Current children cumulated CPU time (s) 148.9
Current children cumulated vsize (Kb) 56964

[startup+160.018 s]
Raw data (loadavg): 1.00 0.97 0.76 2/57 8789
Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8785/statm): 531 226 485 147 0 384 0
[pid=8785] vsize: 2124
Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 14579 0 0 0 15803 79 0 0 25 0 1 0 1796977987 58851328 13873 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8789/statm): 14368 13873 145 145 0 14223 0
[pid=8789] vsize: 57472
Current children cumulated CPU time (s) 158.83
Current children cumulated vsize (Kb) 59596

[startup+170.019 s]
Raw data (loadavg): 1.00 0.97 0.76 2/57 8789
Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8785/statm): 531 226 485 147 0 384 0
[pid=8785] vsize: 2124
Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 15182 0 0 0 16793 85 0 0 25 0 1 0 1796977987 61313024 14476 4294967295 134512640 135094434 3221224432 3221222896 134780630 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8789/statm): 14969 14476 145 145 0 14824 0
[pid=8789] vsize: 59876
Current children cumulated CPU time (s) 168.79
Current children cumulated vsize (Kb) 62000

[startup+180.02 s]
Raw data (loadavg): 1.00 0.97 0.76 2/57 8789
Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8785/statm): 531 226 485 147 0 384 0
[pid=8785] vsize: 2124
Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 15779 0 0 0 17782 88 0 0 25 0 1 0 1796977987 63750144 15073 4294967295 134512640 135094434 3221224432 3221223088 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8789/statm): 15564 15073 145 145 0 15419 0
[pid=8789] vsize: 62256
Current children cumulated CPU time (s) 178.71
Current children cumulated vsize (Kb) 64380

[startup+190.021 s]
Raw data (loadavg): 1.00 0.97 0.76 2/57 8789
Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8785/statm): 531 226 485 147 0 384 0
[pid=8785] vsize: 2124
Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 16366 0 0 0 18771 94 0 0 25 0 1 0 1796977987 66146304 15660 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8789/statm): 16149 15660 145 145 0 16004 0
[pid=8789] vsize: 64596
Current children cumulated CPU time (s) 188.66
Current children cumulated vsize (Kb) 66720

[startup+200.022 s]
Raw data (loadavg): 1.00 0.97 0.77 2/57 8789
Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8785/statm): 531 226 485 147 0 384 0
[pid=8785] vsize: 2124
Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 16933 0 0 0 19760 100 0 0 25 0 1 0 1796977987 68460544 16227 4294967295 134512640 135094434 3221224432 3221223024 134557273 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8789/statm): 16714 16227 145 145 0 16569 0
[pid=8789] vsize: 66856
Current children cumulated CPU time (s) 198.61
Current children cumulated vsize (Kb) 68980

[startup+210.023 s]
Raw data (loadavg): 1.00 0.97 0.77 2/57 8789
Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8785/statm): 531 226 485 147 0 384 0
[pid=8785] vsize: 2124
Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 17732 0 0 0 20744 106 0 0 25 0 1 0 1796977987 71725056 17026 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8789/statm): 17511 17026 145 145 0 17366 0
[pid=8789] vsize: 70044
Current children cumulated CPU time (s) 208.51
Current children cumulated vsize (Kb) 72168

[startup+220.024 s]
Raw data (loadavg): 1.00 0.97 0.77 2/57 8789
Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8785/statm): 531 226 485 147 0 384 0
[pid=8785] vsize: 2124
Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 18443 0 0 0 21734 111 0 0 25 0 1 0 1796977987 74633216 17737 4294967295 134512640 135094434 3221224432 3221223088 134558022 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8789/statm): 18221 17737 145 145 0 18076 0
[pid=8789] vsize: 72884
Current children cumulated CPU time (s) 218.46
Current children cumulated vsize (Kb) 75008

[startup+230.025 s]
Raw data (loadavg): 1.00 0.97 0.77 2/57 8789
Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8785/statm): 531 226 485 147 0 384 0
[pid=8785] vsize: 2124
Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 19093 0 0 0 22724 115 0 0 25 0 1 0 1796977987 77291520 18387 4294967295 134512640 135094434 3221224432 3221223024 134556785 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8789/statm): 18870 18387 145 145 0 18725 0
[pid=8789] vsize: 75480
Current children cumulated CPU time (s) 228.4
Current children cumulated vsize (Kb) 77604

[startup+240.025 s]
Raw data (loadavg): 1.00 0.97 0.77 2/57 8789
Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8785/statm): 531 226 485 147 0 384 0
[pid=8785] vsize: 2124
Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 19707 0 0 0 23716 120 0 0 25 0 1 0 1796977987 79798272 19001 4294967295 134512640 135094434 3221224432 3221223024 134557429 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8789/statm): 19482 19001 145 145 0 19337 0
[pid=8789] vsize: 77928
Current children cumulated CPU time (s) 238.37
Current children cumulated vsize (Kb) 80052

[startup+250.026 s]
Raw data (loadavg): 1.00 0.97 0.78 2/57 8789
Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8785/statm): 531 226 485 147 0 384 0
[pid=8785] vsize: 2124
Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 20310 0 0 0 24706 123 0 0 25 0 1 0 1796977987 82259968 19604 4294967295 134512640 135094434 3221224432 3221223024 134557131 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8789/statm): 20083 19604 145 145 0 19938 0
[pid=8789] vsize: 80332
Current children cumulated CPU time (s) 248.3
Current children cumulated vsize (Kb) 82456

[startup+260.027 s]
Raw data (loadavg): 1.00 0.97 0.78 2/57 8789
Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8785/statm): 531 226 485 147 0 384 0
[pid=8785] vsize: 2124
Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) T 8785 8785 6847 0 -1 0 20920 0 0 0 25695 128 0 0 25 0 1 0 1796977987 84758528 20214 4294967295 134512640 135094434 3221224432 3221222796 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/8789/statm): 20693 20214 145 145 0 20548 0
[pid=8789] vsize: 82772
Current children cumulated CPU time (s) 258.24
Current children cumulated vsize (Kb) 84896

[startup+270.028 s]
Raw data (loadavg): 1.00 0.97 0.78 2/57 8789
Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8785/statm): 531 226 485 147 0 384 0
[pid=8785] vsize: 2124
Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 21461 0 0 0 26687 132 0 0 25 0 1 0 1796977987 86986752 20755 4294967295 134512640 135094434 3221224432 3221223024 134556904 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8789/statm): 21237 20755 145 145 0 21092 0
[pid=8789] vsize: 84948
Current children cumulated CPU time (s) 268.2
Current children cumulated vsize (Kb) 87072

[startup+280.029 s]
Raw data (loadavg): 1.00 0.97 0.78 2/57 8789
Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8785/statm): 531 226 485 147 0 384 0
[pid=8785] vsize: 2124
Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 21917 0 0 0 27680 134 0 0 25 0 1 0 1796977987 88854528 21211 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8789/statm): 21693 21211 145 145 0 21548 0
[pid=8789] vsize: 86772
Current children cumulated CPU time (s) 278.15
Current children cumulated vsize (Kb) 88896

[startup+290.03 s]
Raw data (loadavg): 1.00 0.97 0.78 2/57 8789
Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8785/statm): 531 226 485 147 0 384 0
[pid=8785] vsize: 2124
Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 22460 0 0 0 28672 137 0 0 25 0 1 0 1796977987 91066368 21754 4294967295 134512640 135094434 3221224432 3221223072 134558043 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8789/statm): 22233 21754 145 145 0 22088 0
[pid=8789] vsize: 88932
Current children cumulated CPU time (s) 288.1
Current children cumulated vsize (Kb) 91056

[startup+300.031 s]
Raw data (loadavg): 1.00 0.97 0.79 2/57 8789
Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8785/statm): 531 226 485 147 0 384 0
[pid=8785] vsize: 2124
Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 23041 0 0 0 29663 142 0 0 25 0 1 0 1796977987 93442048 22335 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8789/statm): 22813 22335 145 145 0 22668 0
[pid=8789] vsize: 91252
Current children cumulated CPU time (s) 298.06
Current children cumulated vsize (Kb) 93376

[startup+310.031 s]
Raw data (loadavg): 1.00 0.97 0.79 2/57 8789
Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8785/statm): 531 226 485 147 0 384 0
[pid=8785] vsize: 2124
Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 23647 0 0 0 30654 145 0 0 25 0 1 0 1796977987 95916032 22941 4294967295 134512640 135094434 3221224432 3221223024 134556802 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8789/statm): 23417 22941 145 145 0 23272 0
[pid=8789] vsize: 93668
Current children cumulated CPU time (s) 308
Current children cumulated vsize (Kb) 95792

[startup+320.032 s]
Raw data (loadavg): 1.00 0.97 0.79 2/57 8789
Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8785/statm): 531 226 485 147 0 384 0
[pid=8785] vsize: 2124
Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 24077 0 0 0 31645 149 0 0 25 0 1 0 1796977987 97931264 23371 4294967295 134512640 135094434 3221224432 3221223088 134557900 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8789/statm): 23909 23371 145 145 0 23764 0
[pid=8789] vsize: 95636
Current children cumulated CPU time (s) 317.95
Current children cumulated vsize (Kb) 97760

[startup+330.033 s]
Raw data (loadavg): 1.00 0.97 0.79 2/57 8789
Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8785/statm): 531 226 485 147 0 384 0
[pid=8785] vsize: 2124
Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 24680 0 0 0 32636 152 0 0 25 0 1 0 1796977987 100392960 23974 4294967295 134512640 135094434 3221224432 3221223024 134557213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8789/statm): 24510 23974 145 145 0 24365 0
[pid=8789] vsize: 98040
Current children cumulated CPU time (s) 327.89
Current children cumulated vsize (Kb) 100164

[startup+340.034 s]
Raw data (loadavg): 1.00 0.97 0.79 2/57 8789
Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8785/statm): 531 226 485 147 0 384 0
[pid=8785] vsize: 2124
Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 25107 0 0 0 33629 155 0 0 25 0 1 0 1796977987 102133760 24401 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8789/statm): 24935 24401 145 145 0 24790 0
[pid=8789] vsize: 99740
Current children cumulated CPU time (s) 337.85
Current children cumulated vsize (Kb) 101864

[startup+350.034 s]
Raw data (loadavg): 1.00 0.97 0.79 2/57 8789
Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8785/statm): 531 226 485 147 0 384 0
[pid=8785] vsize: 2124
Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 25686 0 0 0 34619 160 0 0 25 0 1 0 1796977987 104497152 24980 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8789/statm): 25512 24980 145 145 0 25367 0
[pid=8789] vsize: 102048
Current children cumulated CPU time (s) 347.8
Current children cumulated vsize (Kb) 104172

[startup+360.036 s]
Raw data (loadavg): 1.00 0.97 0.80 2/57 8789
Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8785/statm): 531 226 485 147 0 384 0
[pid=8785] vsize: 2124
Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 26416 0 0 0 35609 165 0 0 25 0 1 0 1796977987 107495424 25710 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8789/statm): 26244 25710 145 145 0 26099 0
[pid=8789] vsize: 104976
Current children cumulated CPU time (s) 357.75
Current children cumulated vsize (Kb) 107100

[startup+370.036 s]
Raw data (loadavg): 1.00 0.97 0.80 3/57 8789
Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8785/statm): 531 226 485 147 0 384 0
[pid=8785] vsize: 2124
Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 27172 0 0 0 36600 169 0 0 25 0 1 0 1796977987 110587904 26466 4294967295 134512640 135094434 3221224432 3221223024 134557377 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8789/statm): 26999 26466 145 145 0 26854 0
[pid=8789] vsize: 107996
Current children cumulated CPU time (s) 367.7
Current children cumulated vsize (Kb) 110120

[startup+380.037 s]
Raw data (loadavg): 1.00 0.97 0.80 2/57 8789
Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8785/statm): 531 226 485 147 0 384 0
[pid=8785] vsize: 2124
Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 27685 0 0 0 37591 173 0 0 25 0 1 0 1796977987 112685056 26979 4294967295 134512640 135094434 3221224432 3221223024 134557028 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8789/statm): 27511 26979 145 145 0 27366 0
[pid=8789] vsize: 110044
Current children cumulated CPU time (s) 377.65
Current children cumulated vsize (Kb) 112168

[startup+390.038 s]
Raw data (loadavg): 1.00 0.97 0.80 2/57 8789
Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8785/statm): 531 226 485 147 0 384 0
[pid=8785] vsize: 2124
Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 28016 0 0 0 38585 175 0 0 25 0 1 0 1796977987 114024448 27310 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8789/statm): 27838 27310 145 145 0 27693 0
[pid=8789] vsize: 111352
Current children cumulated CPU time (s) 387.61
Current children cumulated vsize (Kb) 113476

[startup+400.038 s]
Raw data (loadavg): 1.00 0.97 0.80 2/57 8789
Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8785/statm): 531 226 485 147 0 384 0
[pid=8785] vsize: 2124
Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 28499 0 0 0 39577 179 0 0 25 0 1 0 1796977987 115990528 27793 4294967295 134512640 135094434 3221224432 3221223088 134557937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8789/statm): 28318 27793 145 145 0 28173 0
[pid=8789] vsize: 113272
Current children cumulated CPU time (s) 397.57
Current children cumulated vsize (Kb) 115396

[startup+410.039 s]
Raw data (loadavg): 1.00 0.97 0.81 2/57 8789
Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8785/statm): 531 226 485 147 0 384 0
[pid=8785] vsize: 2124
Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 28909 0 0 0 40569 182 0 0 25 0 1 0 1796977987 117661696 28203 4294967295 134512640 135094434 3221224432 3221223088 134558286 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8789/statm): 28726 28203 145 145 0 28581 0
[pid=8789] vsize: 114904
Current children cumulated CPU time (s) 407.52
Current children cumulated vsize (Kb) 117028

[startup+420.04 s]
Raw data (loadavg): 1.00 0.97 0.81 2/57 8789
Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8785/statm): 531 226 485 147 0 384 0
[pid=8785] vsize: 2124
Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 29417 0 0 0 41561 186 0 0 25 0 1 0 1796977987 119734272 28711 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8789/statm): 29232 28711 145 145 0 29087 0
[pid=8789] vsize: 116928
Current children cumulated CPU time (s) 417.48
Current children cumulated vsize (Kb) 119052

[startup+430.041 s]
Raw data (loadavg): 1.00 0.97 0.81 2/57 8789
Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8785/statm): 531 226 485 147 0 384 0
[pid=8785] vsize: 2124
Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 29953 0 0 0 42553 189 0 0 25 0 1 0 1796977987 121921536 29247 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8789/statm): 29766 29247 145 145 0 29621 0
[pid=8789] vsize: 119064
Current children cumulated CPU time (s) 427.43
Current children cumulated vsize (Kb) 121188

[startup+440.041 s]
Raw data (loadavg): 1.00 0.97 0.81 2/57 8789
Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8785/statm): 531 226 485 147 0 384 0
[pid=8785] vsize: 2124
Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 30507 0 0 0 43545 192 0 0 25 0 1 0 1796977987 124182528 29801 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8789/statm): 30318 29801 145 145 0 30173 0
[pid=8789] vsize: 121272
Current children cumulated CPU time (s) 437.38
Current children cumulated vsize (Kb) 123396

[startup+450.042 s]
Raw data (loadavg): 1.00 0.97 0.81 2/57 8789
Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8785/statm): 531 226 485 147 0 384 0
[pid=8785] vsize: 2124
Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 31206 0 0 0 44534 197 0 0 25 0 1 0 1796977987 127037440 30500 4294967295 134512640 135094434 3221224432 3221223024 134556864 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8789/statm): 31015 30500 145 145 0 30870 0
[pid=8789] vsize: 124060
Current children cumulated CPU time (s) 447.32
Current children cumulated vsize (Kb) 126184

[startup+460.043 s]
Raw data (loadavg): 1.00 0.97 0.82 2/57 8789
Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8785/statm): 531 226 485 147 0 384 0
[pid=8785] vsize: 2124
Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 31880 0 0 0 45523 202 0 0 25 0 1 0 1796977987 129789952 31174 4294967295 134512640 135094434 3221224432 3221223024 134556958 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8789/statm): 31687 31174 145 145 0 31542 0
[pid=8789] vsize: 126748
Current children cumulated CPU time (s) 457.26
Current children cumulated vsize (Kb) 128872

[startup+470.044 s]
Raw data (loadavg): 1.00 0.97 0.82 2/57 8789
Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8785/statm): 531 226 485 147 0 384 0
[pid=8785] vsize: 2124
Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 32516 0 0 0 46512 206 0 0 25 0 1 0 1796977987 132390912 31810 4294967295 134512640 135094434 3221224432 3221223120 134554739 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8789/statm): 32322 31810 145 145 0 32177 0
[pid=8789] vsize: 129288
Current children cumulated CPU time (s) 467.19
Current children cumulated vsize (Kb) 131412

[startup+480.045 s]
Raw data (loadavg): 1.00 0.97 0.82 2/57 8789
Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8785/statm): 531 226 485 147 0 384 0
[pid=8785] vsize: 2124
Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 33081 0 0 0 47504 210 0 0 25 0 1 0 1796977987 134701056 32375 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8789/statm): 32886 32375 145 145 0 32741 0
[pid=8789] vsize: 131544
Current children cumulated CPU time (s) 477.15
Current children cumulated vsize (Kb) 133668

[startup+490.046 s]
Raw data (loadavg): 1.00 0.97 0.82 2/57 8789
Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8785/statm): 531 226 485 147 0 384 0
[pid=8785] vsize: 2124
Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 33670 0 0 0 48495 213 0 0 25 0 1 0 1796977987 137113600 32964 4294967295 134512640 135094434 3221224432 3221223104 134555950 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8789/statm): 33475 32964 145 145 0 33330 0
[pid=8789] vsize: 133900
Current children cumulated CPU time (s) 487.09
Current children cumulated vsize (Kb) 136024

[startup+500.045 s]
Raw data (loadavg): 1.00 0.97 0.82 2/57 8789
Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8785/statm): 531 226 485 147 0 384 0
[pid=8785] vsize: 2124
Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 34259 0 0 0 49487 217 0 0 25 0 1 0 1796977987 139522048 33553 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8789/statm): 34063 33553 145 145 0 33918 0
[pid=8789] vsize: 136252
Current children cumulated CPU time (s) 497.05
Current children cumulated vsize (Kb) 138376

[startup+510.046 s]
Raw data (loadavg): 1.00 0.97 0.82 2/57 8789
Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8785/statm): 531 226 485 147 0 384 0
[pid=8785] vsize: 2124
Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 34713 0 0 0 50479 221 0 0 25 0 1 0 1796977987 141377536 34007 4294967295 134512640 135094434 3221224432 3221223088 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8789/statm): 34516 34007 145 145 0 34371 0
[pid=8789] vsize: 138064
Current children cumulated CPU time (s) 507.01
Current children cumulated vsize (Kb) 140188

[startup+520.047 s]
Raw data (loadavg): 1.00 0.97 0.82 2/57 8789
Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8785/statm): 531 226 485 147 0 384 0
[pid=8785] vsize: 2124
Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 35305 0 0 0 51470 225 0 0 25 0 1 0 1796977987 143798272 34599 4294967295 134512640 135094434 3221224432 3221223120 134554723 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8789/statm): 35107 34599 145 145 0 34962 0
[pid=8789] vsize: 140428
Current children cumulated CPU time (s) 516.96
Current children cumulated vsize (Kb) 142552

[startup+530.048 s]
Raw data (loadavg): 1.00 0.97 0.82 2/57 8789
Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8785/statm): 531 226 485 147 0 384 0
[pid=8785] vsize: 2124
Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 35597 0 0 0 52466 226 0 0 25 0 1 0 1796977987 144986112 34891 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8789/statm): 35397 34891 145 145 0 35252 0
[pid=8789] vsize: 141588
Current children cumulated CPU time (s) 526.93
Current children cumulated vsize (Kb) 143712

[startup+540.049 s]
Raw data (loadavg): 1.00 0.97 0.83 2/57 8789
Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8785/statm): 531 226 485 147 0 384 0
[pid=8785] vsize: 2124
Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 36204 0 0 0 53456 230 0 0 25 0 1 0 1796977987 147460096 35498 4294967295 134512640 135094434 3221224432 3221223024 134557528 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8789/statm): 36001 35498 145 145 0 35856 0
[pid=8789] vsize: 144004
Current children cumulated CPU time (s) 536.87
Current children cumulated vsize (Kb) 146128

[startup+550.05 s]
Raw data (loadavg): 1.00 0.97 0.83 2/57 8789
Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8785/statm): 531 226 485 147 0 384 0
[pid=8785] vsize: 2124
Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) T 8785 8785 6847 0 -1 0 36726 0 0 0 54450 233 0 0 25 0 1 0 1796977987 149590016 36020 4294967295 134512640 135094434 3221224432 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/8789/statm): 36521 36020 145 145 0 36376 0
[pid=8789] vsize: 146084
Current children cumulated CPU time (s) 546.84
Current children cumulated vsize (Kb) 148208

[startup+560.05 s]
Raw data (loadavg): 1.00 0.97 0.83 2/57 8789
Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8785/statm): 531 226 485 147 0 384 0
[pid=8785] vsize: 2124
Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 37040 0 0 0 55446 235 0 0 25 0 1 0 1796977987 150872064 36334 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8789/statm): 36834 36334 145 145 0 36689 0
[pid=8789] vsize: 147336
Current children cumulated CPU time (s) 556.82
Current children cumulated vsize (Kb) 149460

[startup+570.051 s]
Raw data (loadavg): 1.00 0.97 0.83 2/57 8789
Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8785/statm): 531 226 485 147 0 384 0
[pid=8785] vsize: 2124
Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 37425 0 0 0 56439 238 0 0 25 0 1 0 1796977987 152440832 36719 4294967295 134512640 135094434 3221224432 3221223024 134556958 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8789/statm): 37217 36719 145 145 0 37072 0
[pid=8789] vsize: 148868
Current children cumulated CPU time (s) 566.78
Current children cumulated vsize (Kb) 150992

[startup+580.052 s]
Raw data (loadavg): 1.00 0.97 0.83 2/57 8789
Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8785/statm): 531 226 485 147 0 384 0
[pid=8785] vsize: 2124
Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 37859 0 0 0 57432 241 0 0 25 0 1 0 1796977987 154214400 37153 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8789/statm): 37650 37153 145 145 0 37505 0
[pid=8789] vsize: 150600
Current children cumulated CPU time (s) 576.74
Current children cumulated vsize (Kb) 152724

[startup+590.053 s]
Raw data (loadavg): 1.00 0.97 0.83 2/57 8789
Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8785/statm): 531 226 485 147 0 384 0
[pid=8785] vsize: 2124
Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 38382 0 0 0 58423 245 0 0 25 0 1 0 1796977987 156348416 37676 4294967295 134512640 135094434 3221224432 3221223056 134562104 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8789/statm): 38171 37676 145 145 0 38026 0
[pid=8789] vsize: 152684
Current children cumulated CPU time (s) 586.69
Current children cumulated vsize (Kb) 154808

[startup+600.053 s]
Raw data (loadavg): 1.00 0.97 0.83 2/57 8789
Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8785/statm): 531 226 485 147 0 384 0
[pid=8785] vsize: 2124
Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 38926 0 0 0 59415 248 0 0 25 0 1 0 1796977987 158572544 38220 4294967295 134512640 135094434 3221224432 3221223024 134556834 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8789/statm): 38714 38220 145 145 0 38569 0
[pid=8789] vsize: 154856
Current children cumulated CPU time (s) 596.64
Current children cumulated vsize (Kb) 156980

[startup+610.054 s]
Raw data (loadavg): 1.00 0.97 0.83 2/57 8789
Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8785/statm): 531 226 485 147 0 384 0
[pid=8785] vsize: 2124
Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 39456 0 0 0 60409 252 0 0 25 0 1 0 1796977987 160735232 38750 4294967295 134512640 135094434 3221224432 3221223056 134553308 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8789/statm): 39242 38750 145 145 0 39097 0
[pid=8789] vsize: 156968
Current children cumulated CPU time (s) 606.62
Current children cumulated vsize (Kb) 159092

[startup+620.055 s]
Raw data (loadavg): 1.00 0.97 0.83 2/57 8789
Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8785/statm): 531 226 485 147 0 384 0
[pid=8785] vsize: 2124
Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 39456 0 0 0 61409 252 0 0 25 0 1 0 1796977987 160735232 38750 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8789/statm): 39242 38750 145 145 0 39097 0
[pid=8789] vsize: 156968
Current children cumulated CPU time (s) 616.62
Current children cumulated vsize (Kb) 159092

[startup+630.055 s]
Raw data (loadavg): 1.00 0.97 0.83 2/57 8789
Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8785/statm): 531 226 485 147 0 384 0
[pid=8785] vsize: 2124
Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 39456 0 0 0 62409 252 0 0 25 0 1 0 1796977987 160735232 38750 4294967295 134512640 135094434 3221224432 3221223084 134562168 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8789/statm): 39242 38750 145 145 0 39097 0
[pid=8789] vsize: 156968
Current children cumulated CPU time (s) 626.62
Current children cumulated vsize (Kb) 159092

[startup+640.056 s]
Raw data (loadavg): 1.00 0.97 0.83 2/57 8789
Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8785/statm): 531 226 485 147 0 384 0
[pid=8785] vsize: 2124
Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 39456 0 0 0 63409 252 0 0 25 0 1 0 1796977987 160735232 38750 4294967295 134512640 135094434 3221224432 3221223024 134557514 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8789/statm): 39242 38750 145 145 0 39097 0
[pid=8789] vsize: 156968
Current children cumulated CPU time (s) 636.62
Current children cumulated vsize (Kb) 159092

[startup+650.057 s]
Raw data (loadavg): 1.00 0.97 0.84 2/57 8789
Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8785/statm): 531 226 485 147 0 384 0
[pid=8785] vsize: 2124
Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 39456 0 0 0 64410 252 0 0 25 0 1 0 1796977987 160735232 38750 4294967295 134512640 135094434 3221224432 3221223024 134556791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8789/statm): 39242 38750 145 145 0 39097 0
[pid=8789] vsize: 156968
Current children cumulated CPU time (s) 646.63
Current children cumulated vsize (Kb) 159092

[startup+660.058 s]
Raw data (loadavg): 1.00 0.97 0.84 2/57 8789
Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8785/statm): 531 226 485 147 0 384 0
[pid=8785] vsize: 2124
Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 39456 0 0 0 65410 252 0 0 25 0 1 0 1796977987 160735232 38750 4294967295 134512640 135094434 3221224432 3221223024 134556785 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8789/statm): 39242 38750 145 145 0 39097 0
[pid=8789] vsize: 156968
Current children cumulated CPU time (s) 656.63
Current children cumulated vsize (Kb) 159092

[startup+670.059 s]
Raw data (loadavg): 1.00 0.97 0.84 2/57 8789
Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8785/statm): 531 226 485 147 0 384 0
[pid=8785] vsize: 2124
Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 39456 0 0 0 66410 252 0 0 25 0 1 0 1796977987 160735232 38750 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8789/statm): 39242 38750 145 145 0 39097 0
[pid=8789] vsize: 156968
Current children cumulated CPU time (s) 666.63
Current children cumulated vsize (Kb) 159092

[startup+680.06 s]
Raw data (loadavg): 1.00 0.97 0.84 2/57 8789
Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8785/statm): 531 226 485 147 0 384 0
[pid=8785] vsize: 2124
Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 39456 0 0 0 67409 252 0 0 25 0 1 0 1796977987 160735232 38750 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8789/statm): 39242 38750 145 145 0 39097 0
[pid=8789] vsize: 156968
Current children cumulated CPU time (s) 676.62
Current children cumulated vsize (Kb) 159092

[startup+690.061 s]
Raw data (loadavg): 1.00 0.97 0.84 2/57 8789
Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8785/statm): 531 226 485 147 0 384 0
[pid=8785] vsize: 2124
Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 39456 0 0 0 68408 253 0 0 25 0 1 0 1796977987 160735232 38750 4294967295 134512640 135094434 3221224432 3221223024 134556776 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8789/statm): 39242 38750 145 145 0 39097 0
[pid=8789] vsize: 156968
Current children cumulated CPU time (s) 686.62
Current children cumulated vsize (Kb) 159092

[startup+700.061 s]
Raw data (loadavg): 1.00 0.97 0.84 2/57 8789
Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8785/statm): 531 226 485 147 0 384 0
[pid=8785] vsize: 2124
Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 39456 0 0 0 69408 253 0 0 25 0 1 0 1796977987 160735232 38750 4294967295 134512640 135094434 3221224432 3221223024 134556894 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8789/statm): 39242 38750 145 145 0 39097 0
[pid=8789] vsize: 156968
Current children cumulated CPU time (s) 696.62
Current children cumulated vsize (Kb) 159092

[startup+710.063 s]
Raw data (loadavg): 1.00 0.97 0.84 2/57 8789
Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8785/statm): 531 226 485 147 0 384 0
[pid=8785] vsize: 2124
Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 39456 0 0 0 70408 253 0 0 25 0 1 0 1796977987 160735232 38750 4294967295 134512640 135094434 3221224432 3221223024 134556851 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8789/statm): 39242 38750 145 145 0 39097 0
[pid=8789] vsize: 156968
Current children cumulated CPU time (s) 706.62
Current children cumulated vsize (Kb) 159092

[startup+720.064 s]
Raw data (loadavg): 1.00 0.97 0.84 2/57 8789
Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8785/statm): 531 226 485 147 0 384 0
[pid=8785] vsize: 2124
Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 39456 0 0 0 71408 254 0 0 25 0 1 0 1796977987 160735232 38750 4294967295 134512640 135094434 3221224432 3221223024 134556941 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8789/statm): 39242 38750 145 145 0 39097 0
[pid=8789] vsize: 156968
Current children cumulated CPU time (s) 716.63
Current children cumulated vsize (Kb) 159092

[startup+730.065 s]
Raw data (loadavg): 1.00 0.97 0.84 2/57 8789
Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8785/statm): 531 226 485 147 0 384 0
[pid=8785] vsize: 2124
Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 39456 0 0 0 72407 254 0 0 25 0 1 0 1796977987 160735232 38750 4294967295 134512640 135094434 3221224432 3221223088 134557964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8789/statm): 39242 38750 145 145 0 39097 0
[pid=8789] vsize: 156968
Current children cumulated CPU time (s) 726.62
Current children cumulated vsize (Kb) 159092

[startup+740.066 s]
Raw data (loadavg): 1.00 0.97 0.84 2/57 8789
Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8785/statm): 531 226 485 147 0 384 0
[pid=8785] vsize: 2124
Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 39456 0 0 0 73407 254 0 0 25 0 1 0 1796977987 160735232 38750 4294967295 134512640 135094434 3221224432 3221223024 134557213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8789/statm): 39242 38750 145 145 0 39097 0
[pid=8789] vsize: 156968
Current children cumulated CPU time (s) 736.62
Current children cumulated vsize (Kb) 159092

[startup+750.067 s]
Raw data (loadavg): 1.00 0.97 0.85 2/57 8789
Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8785/statm): 531 226 485 147 0 384 0
[pid=8785] vsize: 2124
Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 39456 0 0 0 74407 254 0 0 25 0 1 0 1796977987 160735232 38750 4294967295 134512640 135094434 3221224432 3221223024 134556862 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8789/statm): 39242 38750 145 145 0 39097 0
[pid=8789] vsize: 156968
Current children cumulated CPU time (s) 746.62
Current children cumulated vsize (Kb) 159092

[startup+760.067 s]
Raw data (loadavg): 1.00 0.97 0.85 2/57 8789
Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8785/statm): 531 226 485 147 0 384 0
[pid=8785] vsize: 2124
Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 39456 0 0 0 75407 254 0 0 25 0 1 0 1796977987 160735232 38750 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8789/statm): 39242 38750 145 145 0 39097 0
[pid=8789] vsize: 156968
Current children cumulated CPU time (s) 756.62
Current children cumulated vsize (Kb) 159092

[startup+770.068 s]
Raw data (loadavg): 1.00 0.97 0.85 2/57 8789
Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8785/statm): 531 226 485 147 0 384 0
[pid=8785] vsize: 2124
Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 39456 0 0 0 76406 255 0 0 25 0 1 0 1796977987 160735232 38750 4294967295 134512640 135094434 3221224432 3221223024 134556851 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8789/statm): 39242 38750 145 145 0 39097 0
[pid=8789] vsize: 156968
Current children cumulated CPU time (s) 766.62
Current children cumulated vsize (Kb) 159092

[startup+780.07 s]
Raw data (loadavg): 1.00 0.97 0.85 2/57 8789
Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8785/statm): 531 226 485 147 0 384 0
[pid=8785] vsize: 2124
Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 39456 0 0 0 77406 255 0 0 25 0 1 0 1796977987 160735232 38750 4294967295 134512640 135094434 3221224432 3221223104 134556538 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8789/statm): 39242 38750 145 145 0 39097 0
[pid=8789] vsize: 156968
Current children cumulated CPU time (s) 776.62
Current children cumulated vsize (Kb) 159092

[startup+790.071 s]
Raw data (loadavg): 1.00 0.97 0.85 2/57 8789
Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8785/statm): 531 226 485 147 0 384 0
[pid=8785] vsize: 2124
Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 39456 0 0 0 78406 255 0 0 25 0 1 0 1796977987 160735232 38750 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8789/statm): 39242 38750 145 145 0 39097 0
[pid=8789] vsize: 156968
Current children cumulated CPU time (s) 786.62
Current children cumulated vsize (Kb) 159092

[startup+800.072 s]
Raw data (loadavg): 1.00 0.97 0.85 2/57 8789
Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8785/statm): 531 226 485 147 0 384 0
[pid=8785] vsize: 2124
Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 39456 0 0 0 79403 257 0 0 25 0 1 0 1796977987 160735232 38750 4294967295 134512640 135094434 3221224432 3221223024 134556699 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8789/statm): 39242 38750 145 145 0 39097 0
[pid=8789] vsize: 156968
Current children cumulated CPU time (s) 796.61
Current children cumulated vsize (Kb) 159092

[startup+810.074 s]
Raw data (loadavg): 1.00 0.97 0.85 2/57 8789
Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8785/statm): 531 226 485 147 0 384 0
[pid=8785] vsize: 2124
Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 39456 0 0 0 80403 258 0 0 25 0 1 0 1796977987 160735232 38750 4294967295 134512640 135094434 3221224432 3221223024 134557500 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8789/statm): 39242 38750 145 145 0 39097 0
[pid=8789] vsize: 156968
Current children cumulated CPU time (s) 806.62
Current children cumulated vsize (Kb) 159092

[startup+820.074 s]
Raw data (loadavg): 1.00 0.97 0.85 2/57 8789
Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8785/statm): 531 226 485 147 0 384 0
[pid=8785] vsize: 2124
Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 39456 0 0 0 81402 259 0 0 25 0 1 0 1796977987 160735232 38750 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8789/statm): 39242 38750 145 145 0 39097 0
[pid=8789] vsize: 156968
Current children cumulated CPU time (s) 816.62
Current children cumulated vsize (Kb) 159092

[startup+830.076 s]
Raw data (loadavg): 1.00 0.97 0.85 2/57 8789
Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8785/statm): 531 226 485 147 0 384 0
[pid=8785] vsize: 2124
Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 39456 0 0 0 82402 259 0 0 25 0 1 0 1796977987 160735232 38750 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8789/statm): 39242 38750 145 145 0 39097 0
[pid=8789] vsize: 156968
Current children cumulated CPU time (s) 826.62
Current children cumulated vsize (Kb) 159092

[startup+840.077 s]
Raw data (loadavg): 1.00 0.97 0.85 2/57 8789
Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8785/statm): 531 226 485 147 0 384 0
[pid=8785] vsize: 2124
Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 39456 0 0 0 83401 260 0 0 25 0 1 0 1796977987 160735232 38750 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8789/statm): 39242 38750 145 145 0 39097 0
[pid=8789] vsize: 156968
Current children cumulated CPU time (s) 836.62
Current children cumulated vsize (Kb) 159092

[startup+850.078 s]
Raw data (loadavg): 1.00 0.97 0.86 2/57 8789
Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8785/statm): 531 226 485 147 0 384 0
[pid=8785] vsize: 2124
Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 39456 0 0 0 84401 260 0 0 25 0 1 0 1796977987 160735232 38750 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8789/statm): 39242 38750 145 145 0 39097 0
[pid=8789] vsize: 156968
Current children cumulated CPU time (s) 846.62
Current children cumulated vsize (Kb) 159092

[startup+860.079 s]
Raw data (loadavg): 1.00 0.97 0.86 2/57 8789
Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8785/statm): 531 226 485 147 0 384 0
[pid=8785] vsize: 2124
Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 39456 0 0 0 85400 260 0 0 25 0 1 0 1796977987 160735232 38750 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8789/statm): 39242 38750 145 145 0 39097 0
[pid=8789] vsize: 156968
Current children cumulated CPU time (s) 856.61
Current children cumulated vsize (Kb) 159092

[startup+870.08 s]
Raw data (loadavg): 1.00 0.97 0.86 2/57 8789
Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8785/statm): 531 226 485 147 0 384 0
[pid=8785] vsize: 2124
Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 39456 0 0 0 86400 261 0 0 25 0 1 0 1796977987 160735232 38750 4294967295 134512640 135094434 3221224432 3221223024 134556862 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8789/statm): 39242 38750 145 145 0 39097 0
[pid=8789] vsize: 156968
Current children cumulated CPU time (s) 866.62
Current children cumulated vsize (Kb) 159092

[startup+880.081 s]
Raw data (loadavg): 1.00 0.97 0.86 2/57 8789
Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8785/statm): 531 226 485 147 0 384 0
[pid=8785] vsize: 2124
Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 39456 0 0 0 87399 262 0 0 25 0 1 0 1796977987 160735232 38750 4294967295 134512640 135094434 3221224432 3221223024 134557227 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8789/statm): 39242 38750 145 145 0 39097 0
[pid=8789] vsize: 156968
Current children cumulated CPU time (s) 876.62
Current children cumulated vsize (Kb) 159092

[startup+890.081 s]
Raw data (loadavg): 1.00 0.97 0.86 2/57 8789
Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8785/statm): 531 226 485 147 0 384 0
[pid=8785] vsize: 2124
Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 39456 0 0 0 88398 262 0 0 25 0 1 0 1796977987 160735232 38750 4294967295 134512640 135094434 3221224432 3221223024 134556964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8789/statm): 39242 38750 145 145 0 39097 0
[pid=8789] vsize: 156968
Current children cumulated CPU time (s) 886.61
Current children cumulated vsize (Kb) 159092

[startup+900.082 s]
Raw data (loadavg): 1.00 0.97 0.86 2/57 8789
Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8785/statm): 531 226 485 147 0 384 0
[pid=8785] vsize: 2124
Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 39456 0 0 0 89398 262 0 0 25 0 1 0 1796977987 160735232 38750 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8789/statm): 39242 38750 145 145 0 39097 0
[pid=8789] vsize: 156968
Current children cumulated CPU time (s) 896.61
Current children cumulated vsize (Kb) 159092

[startup+910.083 s]
Raw data (loadavg): 1.00 0.97 0.86 2/57 8789
Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8785/statm): 531 226 485 147 0 384 0
[pid=8785] vsize: 2124
Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 39456 0 0 0 90397 263 0 0 25 0 1 0 1796977987 160735232 38750 4294967295 134512640 135094434 3221224432 3221223024 134556964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8789/statm): 39242 38750 145 145 0 39097 0
[pid=8789] vsize: 156968
Current children cumulated CPU time (s) 906.61
Current children cumulated vsize (Kb) 159092

[startup+920.084 s]
Raw data (loadavg): 1.00 0.97 0.86 2/57 8789
Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8785/statm): 531 226 485 147 0 384 0
[pid=8785] vsize: 2124
Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 39456 0 0 0 91397 263 0 0 25 0 1 0 1796977987 160735232 38750 4294967295 134512640 135094434 3221224432 3221223088 134558178 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8789/statm): 39242 38750 145 145 0 39097 0
[pid=8789] vsize: 156968
Current children cumulated CPU time (s) 916.61
Current children cumulated vsize (Kb) 159092

[startup+930.086 s]
Raw data (loadavg): 1.00 0.97 0.86 2/57 8789
Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8785/statm): 531 226 485 147 0 384 0
[pid=8785] vsize: 2124
Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 39456 0 0 0 92397 263 0 0 25 0 1 0 1796977987 160735232 38750 4294967295 134512640 135094434 3221224432 3221223088 134557856 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8789/statm): 39242 38750 145 145 0 39097 0
[pid=8789] vsize: 156968
Current children cumulated CPU time (s) 926.61
Current children cumulated vsize (Kb) 159092

[startup+940.087 s]
Raw data (loadavg): 1.00 0.97 0.86 2/57 8789
Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8785/statm): 531 226 485 147 0 384 0
[pid=8785] vsize: 2124
Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 39456 0 0 0 93397 264 0 0 25 0 1 0 1796977987 160735232 38750 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8789/statm): 39242 38750 145 145 0 39097 0
[pid=8789] vsize: 156968
Current children cumulated CPU time (s) 936.62
Current children cumulated vsize (Kb) 159092

[startup+950.087 s]
Raw data (loadavg): 1.00 0.97 0.87 2/57 8789
Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8785/statm): 531 226 485 147 0 384 0
[pid=8785] vsize: 2124
Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 39456 0 0 0 94396 264 0 0 25 0 1 0 1796977987 160735232 38750 4294967295 134512640 135094434 3221224432 3221223024 134556975 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8789/statm): 39242 38750 145 145 0 39097 0
[pid=8789] vsize: 156968
Current children cumulated CPU time (s) 946.61
Current children cumulated vsize (Kb) 159092

[startup+960.089 s]
Raw data (loadavg): 1.00 0.97 0.87 2/57 8789
Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8785/statm): 531 226 485 147 0 384 0
[pid=8785] vsize: 2124
Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 39456 0 0 0 95396 264 0 0 25 0 1 0 1796977987 160735232 38750 4294967295 134512640 135094434 3221224432 3221223024 134557037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8789/statm): 39242 38750 145 145 0 39097 0
[pid=8789] vsize: 156968
Current children cumulated CPU time (s) 956.61
Current children cumulated vsize (Kb) 159092

[startup+970.09 s]
Raw data (loadavg): 1.00 0.97 0.87 2/57 8789
Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8785/statm): 531 226 485 147 0 384 0
[pid=8785] vsize: 2124
Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 39456 0 0 0 96396 265 0 0 25 0 1 0 1796977987 160735232 38750 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8789/statm): 39242 38750 145 145 0 39097 0
[pid=8789] vsize: 156968
Current children cumulated CPU time (s) 966.62
Current children cumulated vsize (Kb) 159092

[startup+980.091 s]
Raw data (loadavg): 1.00 0.97 0.87 2/57 8789
Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8785/statm): 531 226 485 147 0 384 0
[pid=8785] vsize: 2124
Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 39456 0 0 0 97395 265 0 0 25 0 1 0 1796977987 160735232 38750 4294967295 134512640 135094434 3221224432 3221223024 134556812 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8789/statm): 39242 38750 145 145 0 39097 0
[pid=8789] vsize: 156968
Current children cumulated CPU time (s) 976.61
Current children cumulated vsize (Kb) 159092

[startup+990.092 s]
Raw data (loadavg): 1.00 0.97 0.87 2/57 8789
Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8785/statm): 531 226 485 147 0 384 0
[pid=8785] vsize: 2124
Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 39456 0 0 0 98395 265 0 0 25 0 1 0 1796977987 160735232 38750 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8789/statm): 39242 38750 145 145 0 39097 0
[pid=8789] vsize: 156968
Current children cumulated CPU time (s) 986.61
Current children cumulated vsize (Kb) 159092

[startup+1000.09 s]
Raw data (loadavg): 1.00 0.97 0.87 2/57 8789
Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8785/statm): 531 226 485 147 0 384 0
[pid=8785] vsize: 2124
Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 39456 0 0 0 99395 266 0 0 25 0 1 0 1796977987 160735232 38750 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8789/statm): 39242 38750 145 145 0 39097 0
[pid=8789] vsize: 156968
Current children cumulated CPU time (s) 996.62
Current children cumulated vsize (Kb) 159092

[startup+1010.09 s]
Raw data (loadavg): 1.00 0.97 0.87 2/57 8789
Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8785/statm): 531 226 485 147 0 384 0
[pid=8785] vsize: 2124
Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 39456 0 0 0 100395 266 0 0 25 0 1 0 1796977987 160735232 38750 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8789/statm): 39242 38750 145 145 0 39097 0
[pid=8789] vsize: 156968
Current children cumulated CPU time (s) 1006.62
Current children cumulated vsize (Kb) 159092

[startup+1020.1 s]
Raw data (loadavg): 1.00 0.97 0.87 2/57 8789
Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8785/statm): 531 226 485 147 0 384 0
[pid=8785] vsize: 2124
Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 39456 0 0 0 101394 267 0 0 25 0 1 0 1796977987 160735232 38750 4294967295 134512640 135094434 3221224432 3221223088 134557996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8789/statm): 39242 38750 145 145 0 39097 0
[pid=8789] vsize: 156968
Current children cumulated CPU time (s) 1016.62
Current children cumulated vsize (Kb) 159092

[startup+1030.1 s]
Raw data (loadavg): 1.00 0.97 0.87 2/57 8789
Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8785/statm): 531 226 485 147 0 384 0
[pid=8785] vsize: 2124
Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 39456 0 0 0 102394 267 0 0 25 0 1 0 1796977987 160735232 38750 4294967295 134512640 135094434 3221224432 3221223088 134558235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8789/statm): 39242 38750 145 145 0 39097 0
[pid=8789] vsize: 156968
Current children cumulated CPU time (s) 1026.62
Current children cumulated vsize (Kb) 159092

[startup+1040.1 s]
Raw data (loadavg): 1.00 0.97 0.87 2/57 8789
Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8785/statm): 531 226 485 147 0 384 0
[pid=8785] vsize: 2124
Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 39456 0 0 0 103394 267 0 0 25 0 1 0 1796977987 160735232 38750 4294967295 134512640 135094434 3221224432 3221223092 134553480 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8789/statm): 39242 38750 145 145 0 39097 0
[pid=8789] vsize: 156968
Current children cumulated CPU time (s) 1036.62
Current children cumulated vsize (Kb) 159092

[startup+1050.1 s]
Raw data (loadavg): 1.00 0.97 0.87 2/57 8789
Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8785/statm): 531 226 485 147 0 384 0
[pid=8785] vsize: 2124
Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 39456 0 0 0 104395 267 0 0 25 0 1 0 1796977987 160735232 38750 4294967295 134512640 135094434 3221224432 3221223092 134553508 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8789/statm): 39242 38750 145 145 0 39097 0
[pid=8789] vsize: 156968
Current children cumulated CPU time (s) 1046.63
Current children cumulated vsize (Kb) 159092

[startup+1060.1 s]
Raw data (loadavg): 1.00 0.97 0.88 2/57 8789
Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8785/statm): 531 226 485 147 0 384 0
[pid=8785] vsize: 2124
Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 39456 0 0 0 105395 267 0 0 25 0 1 0 1796977987 160735232 38750 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8789/statm): 39242 38750 145 145 0 39097 0
[pid=8789] vsize: 156968
Current children cumulated CPU time (s) 1056.63
Current children cumulated vsize (Kb) 159092

[startup+1070.1 s]
Raw data (loadavg): 1.00 0.97 0.88 2/57 8789
Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8785/statm): 531 226 485 147 0 384 0
[pid=8785] vsize: 2124
Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 39456 0 0 0 106395 267 0 0 25 0 1 0 1796977987 160735232 38750 4294967295 134512640 135094434 3221224432 3221223104 134556317 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8789/statm): 39242 38750 145 145 0 39097 0
[pid=8789] vsize: 156968
Current children cumulated CPU time (s) 1066.63
Current children cumulated vsize (Kb) 159092

[startup+1080.1 s]
Raw data (loadavg): 1.00 0.97 0.88 2/57 8789
Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8785/statm): 531 226 485 147 0 384 0
[pid=8785] vsize: 2124
Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 39456 0 0 0 107395 267 0 0 25 0 1 0 1796977987 160735232 38750 4294967295 134512640 135094434 3221224432 3221223088 134558227 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8789/statm): 39242 38750 145 145 0 39097 0
[pid=8789] vsize: 156968
Current children cumulated CPU time (s) 1076.63
Current children cumulated vsize (Kb) 159092

[startup+1090.1 s]
Raw data (loadavg): 1.00 0.97 0.88 2/57 8789
Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8785/statm): 531 226 485 147 0 384 0
[pid=8785] vsize: 2124
Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 39456 0 0 0 108395 267 0 0 25 0 1 0 1796977987 160735232 38750 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8789/statm): 39242 38750 145 145 0 39097 0
[pid=8789] vsize: 156968
Current children cumulated CPU time (s) 1086.63
Current children cumulated vsize (Kb) 159092

[startup+1100.1 s]
Raw data (loadavg): 1.00 0.97 0.88 2/57 8789
Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8785/statm): 531 226 485 147 0 384 0
[pid=8785] vsize: 2124
Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 39456 0 0 0 109395 267 0 0 25 0 1 0 1796977987 160735232 38750 4294967295 134512640 135094434 3221224432 3221223024 134557028 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8789/statm): 39242 38750 145 145 0 39097 0
[pid=8789] vsize: 156968
Current children cumulated CPU time (s) 1096.63
Current children cumulated vsize (Kb) 159092

[startup+1110.1 s]
Raw data (loadavg): 1.00 0.97 0.88 2/57 8789
Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8785/statm): 531 226 485 147 0 384 0
[pid=8785] vsize: 2124
Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 39456 0 0 0 110396 267 0 0 25 0 1 0 1796977987 160735232 38750 4294967295 134512640 135094434 3221224432 3221223088 134558178 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8789/statm): 39242 38750 145 145 0 39097 0
[pid=8789] vsize: 156968
Current children cumulated CPU time (s) 1106.64
Current children cumulated vsize (Kb) 159092

[startup+1120.1 s]
Raw data (loadavg): 1.00 0.97 0.88 1/57 8789
Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8785/statm): 531 226 485 147 0 384 0
[pid=8785] vsize: 2124
Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) T 8785 8785 6847 0 -1 0 39721 0 0 0 111391 269 0 0 25 0 1 0 1796977987 161820672 39015 4294967295 134512640 135094434 3221224432 3221222796 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/8789/statm): 39507 39015 145 145 0 39362 0
[pid=8789] vsize: 158028
Current children cumulated CPU time (s) 1116.61
Current children cumulated vsize (Kb) 160152

[startup+1130.11 s]
Raw data (loadavg): 1.00 0.97 0.88 2/57 8789
Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8785/statm): 531 226 485 147 0 384 0
[pid=8785] vsize: 2124
Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 40183 0 0 0 112386 271 0 0 25 0 1 0 1796977987 163713024 39477 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8789/statm): 39969 39477 145 145 0 39824 0
[pid=8789] vsize: 159876
Current children cumulated CPU time (s) 1126.58
Current children cumulated vsize (Kb) 162000

[startup+1140.11 s]
Raw data (loadavg): 1.00 0.97 0.88 2/57 8789
Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8785/statm): 531 226 485 147 0 384 0
[pid=8785] vsize: 2124
Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 40671 0 0 0 113380 274 0 0 25 0 1 0 1796977987 165707776 39965 4294967295 134512640 135094434 3221224432 3221223024 134557232 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8789/statm): 40456 39965 145 145 0 40311 0
[pid=8789] vsize: 161824
Current children cumulated CPU time (s) 1136.55
Current children cumulated vsize (Kb) 163948

[startup+1150.11 s]
Raw data (loadavg): 1.08 0.99 0.89 2/57 8789
Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8785/statm): 531 226 485 147 0 384 0
[pid=8785] vsize: 2124
Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 41354 0 0 0 114373 277 0 0 25 0 1 0 1796977987 168501248 40648 4294967295 134512640 135094434 3221224432 3221223024 134557141 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8789/statm): 41138 40648 145 145 0 40993 0
[pid=8789] vsize: 164552
Current children cumulated CPU time (s) 1146.51
Current children cumulated vsize (Kb) 166676

[startup+1160.11 s]
Raw data (loadavg): 1.07 0.99 0.89 2/57 8789
Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8785/statm): 531 226 485 147 0 384 0
[pid=8785] vsize: 2124
Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 41792 0 0 0 115368 279 0 0 25 0 1 0 1796977987 170295296 41086 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8789/statm): 41576 41086 145 145 0 41431 0
[pid=8789] vsize: 166304
Current children cumulated CPU time (s) 1156.48
Current children cumulated vsize (Kb) 168428

[startup+1170.11 s]
Raw data (loadavg): 1.06 0.99 0.89 2/57 8789
Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8785/statm): 531 226 485 147 0 384 0
[pid=8785] vsize: 2124
Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 42307 0 0 0 116362 282 0 0 25 0 1 0 1796977987 172400640 41601 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8789/statm): 42090 41601 145 145 0 41945 0
[pid=8789] vsize: 168360
Current children cumulated CPU time (s) 1166.45
Current children cumulated vsize (Kb) 170484

[startup+1180.11 s]
Raw data (loadavg): 1.05 0.99 0.89 2/57 8789
Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8785/statm): 531 226 485 147 0 384 0
[pid=8785] vsize: 2124
Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 42794 0 0 0 117353 286 0 0 25 0 1 0 1796977987 174391296 42088 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8789/statm): 42576 42088 145 145 0 42431 0
[pid=8789] vsize: 170304
Current children cumulated CPU time (s) 1176.4
Current children cumulated vsize (Kb) 172428

[startup+1190.11 s]
Raw data (loadavg): 1.04 0.99 0.89 2/57 8789
Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8785/statm): 531 226 485 147 0 384 0
[pid=8785] vsize: 2124
Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) T 8785 8785 6847 0 -1 0 43370 0 0 0 118344 289 0 0 25 0 1 0 1796977987 176746496 42664 4294967295 134512640 135094434 3221224432 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/8789/statm): 43151 42664 145 145 0 43006 0
[pid=8789] vsize: 172604
Current children cumulated CPU time (s) 1186.34
Current children cumulated vsize (Kb) 174728

[startup+1200.11 s]
Raw data (loadavg): 1.03 0.99 0.89 2/57 8789
Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8785/statm): 531 226 485 147 0 384 0
[pid=8785] vsize: 2124
Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 44092 0 0 0 119335 294 0 0 25 0 1 0 1796977987 179699712 43386 4294967295 134512640 135094434 3221224432 3221223024 134557375 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8789/statm): 43872 43386 145 145 0 43727 0
[pid=8789] vsize: 175488
Current children cumulated CPU time (s) 1196.3
Current children cumulated vsize (Kb) 177612

[startup+1210.11 s]
Raw data (loadavg): 1.03 0.99 0.90 1/57 8789
Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8785/statm): 531 226 485 147 0 384 0
[pid=8785] vsize: 2124
Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) T 8785 8785 6847 0 -1 0 44789 0 0 0 120323 299 0 0 25 0 1 0 1796977987 182550528 44083 4294967295 134512640 135094434 3221224432 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/8789/statm): 44568 44083 145 145 0 44423 0
[pid=8789] vsize: 178272
Current children cumulated CPU time (s) 1206.23
Current children cumulated vsize (Kb) 180396



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.11 s]
Raw data (loadavg): 1.03 0.99 0.90 1/57 8789
Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8785/statm): 531 226 485 147 0 384 0
[pid=8785] vsize: 2124
Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) T 8785 8785 6847 0 -1 0 44789 0 0 0 120323 299 0 0 25 0 1 0 1796977987 182550528 44083 4294967295 134512640 135094434 3221224432 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/8789/statm): 44568 44083 145 145 0 44423 0
[pid=8789] vsize: 178272
Current children cumulated CPU time (s) 1206.23
Current children cumulated vsize (Kb) 180396

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

Child status: 0
Real time (s): 1210.2
CPU time (s): 1206.32
CPU user time (s): 1203.24
CPU system time (s): 3.07853
CPU usage (%): 99.6795
Max. virtual memory (cumulated for all children) (Kb): 180396

Verifier Data

ERROR: no interpretation found !