Some explanations

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

General information on the benchmark

Namemps-v2-13-7/MIPLIB/miplib3/normalized-mps-v2-13-7-l152lav.opb
MD5SUM9d4ce12b138a2bef65a1f401ec9d1f01
Bench Categoryoptimization, small integers (OPTSMALLINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function 4732
Optimality of the best value was proved NO
Number of terms in the objective function 1989
Biggest coefficient in the objective function 268
Number of bits for the biggest coefficient in the objective function 9
Sum of the numbers in the objective function 382524
Number of bits of the sum of numbers in the objective function 19
Biggest number in a constraint 268
Number of bits of the biggest number in a constraint 9
Biggest sum of numbers in a constraint 382524
Number of bits of the biggest sum of numbers19
Best result obtained on this benchmarkSAT
Best CPU time to get the best result obtained on this benchmark1195.7
Number of variables1989
Total number of constraints2086
Number of constraints which are clauses0
Number of constraints which are cardinality constraints (but not clauses)2085
Number of constraints which are nor clauses,nor cardinality constraints1
Minimum length of a constraint1
Maximum length of a constraint1989

Trace number 6208

Launcher Data

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

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        915604 kB
Buffers:         19728 kB
Cached:          69952 kB
SwapCached:        692 kB
Active:          23112 kB
Inactive:        69108 kB
HighTotal:      131008 kB
HighFree:        58744 kB
LowTotal:       903652 kB
LowFree:        856860 kB
SwapTotal:     2097892 kB
SwapFree:      2096628 kB
Dirty:              52 kB
Writeback:           0 kB
Mapped:           5732 kB
Slab:            21148 kB
Committed_AS:    64132 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-09-20 04:43:37 (client local time) WITH STATUS 0 IN 1206.69 SECONDS
stats: 3364 7 1206.69 0

Solver Data

c Parsing PB file...
c Converting 193 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ################################################################################################
c   -- Clauses(.)/Splits(s): (none)
c ---[ 192]---> Adder-cost: 5478   maxlim: 25152   bits: 15/15
c ---[ 190]---> BDD-cost:    3
c ---[ 188]---> BDD-cost:  255
c ---[ 186]---> BDD-cost:  147
c ---[ 184]---> BDD-cost:   83
c ---[ 182]---> BDD-cost:   93
c ---[ 180]---> BDD-cost:  149
c ---[ 178]---> BDD-cost:  235
c ---[ 176]---> BDD-cost:  339
c ---[ 174]---> BDD-cost:   17
c ---[ 172]---> BDD-cost:   21
c ---[ 170]---> BDD-cost:  301
c ---[ 168]---> BDD-cost:  181
c ---[ 166]---> BDD-cost:   87
c ---[ 164]---> BDD-cost:   71
c ---[ 162]---> BDD-cost:   67
c ---[ 160]---> BDD-cost:   57
c ---[ 158]---> BDD-cost:    7
c ---[ 156]---> BDD-cost:   39
c ---[ 154]---> BDD-cost:   85
c ---[ 152]---> BDD-cost:  147
c ---[ 150]---> BDD-cost:  189
c ---[ 148]---> BDD-cost:  211
c ---[ 146]---> BDD-cost:   95
c ---[ 144]---> BDD-cost:   41
c ---[ 142]---> BDD-cost:   35
c ---[ 140]---> BDD-cost:   59
c ---[ 138]---> BDD-cost:  171
c ---[ 136]---> BDD-cost:   59
c ---[ 134]---> BDD-cost:   51
c ---[ 132]---> BDD-cost:  151
c ---[ 130]---> BDD-cost:  147
c ---[ 128]---> BDD-cost:  317
c ---[ 126]---> BDD-cost:  201
c ---[ 124]---> BDD-cost:  105
c ---[ 122]---> BDD-cost:  101
c ---[ 120]---> BDD-cost:  121
c ---[ 118]---> BDD-cost:  133
c ---[ 116]---> BDD-cost:  149
c ---[ 114]---> BDD-cost:  189
c ---[ 112]---> BDD-cost:   77
c ---[ 110]---> BDD-cost:  201
c ---[ 108]---> BDD-cost:   49
c ---[ 106]---> BDD-cost:   81
c ---[ 104]---> BDD-cost:  121
c ---[ 102]---> BDD-cost:  433
c ---[ 100]---> BDD-cost:  191
c ---[  98]---> BDD-cost:   81
c ---[  96]---> BDD-cost:   71
c ---[  94]---> BDD-cost:  103
c ---[  92]---> BDD-cost:   93
c ---[  90]---> BDD-cost:   85
c ---[  88]---> BDD-cost:  189
c ---[  86]---> BDD-cost:  231
c ---[  84]---> BDD-cost:  101
c ---[  82]---> BDD-cost:  109
c ---[  80]---> BDD-cost:  171
c ---[  78]---> BDD-cost:  183
c ---[  76]---> BDD-cost:  173
c ---[  74]---> BDD-cost:  239
c ---[  72]---> BDD-cost:   91
c ---[  70]---> BDD-cost:  271
c ---[  68]---> BDD-cost:  239
c ---[  66]---> BDD-cost:  105
c ---[  64]---> BDD-cost:  117
c ---[  62]---> BDD-cost:  221
c ---[  60]---> BDD-cost:  213
c ---[  58]---> BDD-cost:  145
c ---[  56]---> BDD-cost:  179
c ---[  54]---> BDD-cost:  213
c ---[  52]---> BDD-cost:  143
c ---[  50]---> BDD-cost:  209
c ---[  48]---> BDD-cost:   81
c ---[  46]---> BDD-cost:  205
c ---[  44]---> BDD-cost:   61
c ---[  42]---> BDD-cost:  225
c ---[  40]---> BDD-cost:  129
c ---[  38]---> BDD-cost:  253
c ---[  36]---> BDD-cost:   71
c ---[  34]---> BDD-cost:  203
c ---[  32]---> BDD-cost:   45
c ---[  30]---> BDD-cost:  133
c ---[  28]---> BDD-cost:  323
c ---[  26]---> BDD-cost:  155
c ---[  24]---> BDD-cost:   89
c ---[  22]---> BDD-cost:   93
c ---[  20]---> BDD-cost:   83
c ---[  18]---> BDD-cost:   67
c ---[  16]---> BDD-cost:  133
c ---[  14]---> BDD-cost:  247
c ---[  12]---> BDD-cost:   97
c ---[  10]---> BDD-cost:   97
c ---[   8]---> BDD-cost:  151
c ---[   6]---> BDD-cost:  181
c ---[   4]---> BDD-cost:  151
c ---[   2]---> BDD-cost:  181
c ---[   0]---> Adder-cost: 3598   maxlim: 1961   bits: 11/11
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   97077   314005 |   32359       0        0     nan |  0.000 % |
c |       100 |   96947   313559 |   35594      82     1270    15.5 |  0.582 % |
c |       251 |   96883   313337 |   39154     212    15944    75.2 |  0.639 % |
c |       476 |   96883   313337 |   43069     437    24593    56.3 |  0.639 % |
c |       813 |   96398   311624 |   47376     699    28796    41.2 |  0.981 % |
c |      1320 |   96280   311210 |   52114    1189    64686    54.4 |  1.062 % |
c |      2079 |   96249   311105 |   57325    1943    92323    47.5 |  1.079 % |
c |      3223 |   96179   310853 |   63058    3077   320979   104.3 |  1.123 % |
c |      4931 |   96005   310207 |   69364    4745   498190   105.0 |  1.229 % |
c |      7493 |   95381   308039 |   76300    7204   629523    87.4 |  1.673 % |
c |     11337 |   94537   305108 |   83930   10849   722117    66.6 |  2.263 % |
c |     17103 |   94126   303709 |   92324   16521   986489    59.7 |  2.520 % |
c |     25752 |   93634   301995 |  101556   25094  1804121    71.9 |  2.821 % |
c |     38728 |   93305   300886 |  111712   38012  3779797    99.4 |  3.028 % |
c |     58192 |   93290   300833 |  122883   57465  9794628   170.4 |  3.032 % |
c |     87386 |   93201   300510 |  135171   86640 15885253   183.3 |  3.085 % |
c |    131175 |   93099   300164 |  148688  130408 28212586   216.3 |  3.150 % |
c |    196860 |   92835   299270 |  163557   74455 14452111   194.1 |  3.289 % |

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/28125/stat): 28125 (minisat+_script) R 28124 28125 28974 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1855612431 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 0 0 0
Raw data (/proc/28125/statm): 174 3 169 147 0 27 0
[pid=28125] 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=28126
New process pid=28127
New process pid=28128
execve syscall for /bin/sed executable
One traced child (pid=28127) 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=28128) exited with status: 0
One traced child (pid=28126) exited with status: 0
New process pid=28129
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc27/normalized-mps-v2-13-7-l152lav.opb

[startup+10.0033 s]
Raw data (loadavg): 0.94 0.98 0.93 2/57 28129
Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28125/statm): 531 226 485 147 0 384 0
[pid=28125] vsize: 2124
Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 4203 0 0 0 962 15 0 0 25 0 1 0 1855612436 18100224 3813 4294967295 134512640 135094434 3221224432 3221223088 134558178 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28129/statm): 4419 3813 145 145 0 4274 0
[pid=28129] vsize: 17676
Current children cumulated CPU time (s) 9.79
Current children cumulated vsize (Kb) 19800

[startup+20.0041 s]
Raw data (loadavg): 0.95 0.98 0.93 2/57 28129
Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28125/statm): 531 226 485 147 0 384 0
[pid=28125] vsize: 2124
Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 4576 0 0 0 1956 17 0 0 25 0 1 0 1855612436 19632128 4186 4294967295 134512640 135094434 3221224432 3221223088 134558405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28129/statm): 4793 4186 145 145 0 4648 0
[pid=28129] vsize: 19172
Current children cumulated CPU time (s) 19.75
Current children cumulated vsize (Kb) 21296

[startup+30.006 s]
Raw data (loadavg): 0.95 0.98 0.93 2/57 28129
Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28125/statm): 531 226 485 147 0 384 0
[pid=28125] vsize: 2124
Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 4727 0 0 0 2953 18 0 0 25 0 1 0 1855612436 20275200 4337 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28129/statm): 4950 4337 145 145 0 4805 0
[pid=28129] vsize: 19800
Current children cumulated CPU time (s) 29.73
Current children cumulated vsize (Kb) 21924

[startup+40.0068 s]
Raw data (loadavg): 0.96 0.98 0.93 2/57 28129
Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28125/statm): 531 226 485 147 0 384 0
[pid=28125] vsize: 2124
Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 4846 0 0 0 3950 19 0 0 25 0 1 0 1855612436 20750336 4456 4294967295 134512640 135094434 3221224432 3221223044 134563121 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28129/statm): 5066 4456 145 145 0 4921 0
[pid=28129] vsize: 20264
Current children cumulated CPU time (s) 39.71
Current children cumulated vsize (Kb) 22388

[startup+50.0076 s]
Raw data (loadavg): 0.97 0.98 0.93 2/57 28129
Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28125/statm): 531 226 485 147 0 384 0
[pid=28125] vsize: 2124
Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 5074 0 0 0 4946 21 0 0 25 0 1 0 1855612436 21667840 4684 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28129/statm): 5290 4684 145 145 0 5145 0
[pid=28129] vsize: 21160
Current children cumulated CPU time (s) 49.69
Current children cumulated vsize (Kb) 23284

[startup+60.0084 s]
Raw data (loadavg): 0.97 0.98 0.93 2/57 28129
Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28125/statm): 531 226 485 147 0 384 0
[pid=28125] vsize: 2124
Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 5459 0 0 0 5941 22 0 0 25 0 1 0 1855612436 23289856 5069 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28129/statm): 5686 5069 145 145 0 5541 0
[pid=28129] vsize: 22744
Current children cumulated CPU time (s) 59.65
Current children cumulated vsize (Kb) 24868

[startup+70.0092 s]
Raw data (loadavg): 0.97 0.98 0.93 2/57 28129
Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28125/statm): 531 226 485 147 0 384 0
[pid=28125] vsize: 2124
Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 5828 0 0 0 6935 25 0 0 25 0 1 0 1855612436 24788992 5438 4294967295 134512640 135094434 3221224432 3221223120 134554748 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28129/statm): 6052 5438 145 145 0 5907 0
[pid=28129] vsize: 24208
Current children cumulated CPU time (s) 69.62
Current children cumulated vsize (Kb) 26332

[startup+80.0101 s]
Raw data (loadavg): 0.98 0.98 0.93 2/57 28129
Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28125/statm): 531 226 485 147 0 384 0
[pid=28125] vsize: 2124
Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 6138 0 0 0 7929 28 0 0 25 0 1 0 1855612436 26042368 5748 4294967295 134512640 135094434 3221224432 3221223088 134557840 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28129/statm): 6358 5748 145 145 0 6213 0
[pid=28129] vsize: 25432
Current children cumulated CPU time (s) 79.59
Current children cumulated vsize (Kb) 27556

[startup+90.0109 s]
Raw data (loadavg): 0.98 0.98 0.93 2/57 28129
Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28125/statm): 531 226 485 147 0 384 0
[pid=28125] vsize: 2124
Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 6606 0 0 0 8921 31 0 0 25 0 1 0 1855612436 27947008 6216 4294967295 134512640 135094434 3221224432 3221223088 134558123 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28129/statm): 6823 6216 145 145 0 6678 0
[pid=28129] vsize: 27292
Current children cumulated CPU time (s) 89.54
Current children cumulated vsize (Kb) 29416

[startup+100.012 s]
Raw data (loadavg): 0.98 0.98 0.93 2/57 28129
Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28125/statm): 531 226 485 147 0 384 0
[pid=28125] vsize: 2124
Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 7283 0 0 0 9912 35 0 0 25 0 1 0 1855612436 30711808 6893 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28129/statm): 7498 6893 145 145 0 7353 0
[pid=28129] vsize: 29992
Current children cumulated CPU time (s) 99.49
Current children cumulated vsize (Kb) 32116

[startup+110.013 s]
Raw data (loadavg): 0.99 0.98 0.93 2/57 28129
Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28125/statm): 531 226 485 147 0 384 0
[pid=28125] vsize: 2124
Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 7536 0 0 0 10908 36 0 0 25 0 1 0 1855612436 31870976 7146 4294967295 134512640 135094434 3221224432 3221223024 134557028 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28129/statm): 7781 7146 145 145 0 7636 0
[pid=28129] vsize: 31124
Current children cumulated CPU time (s) 109.46
Current children cumulated vsize (Kb) 33248

[startup+120.012 s]
Raw data (loadavg): 0.99 0.98 0.93 2/57 28129
Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28125/statm): 531 226 485 147 0 384 0
[pid=28125] vsize: 2124
Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 8022 0 0 0 11900 38 0 0 25 0 1 0 1855612436 33849344 7632 4294967295 134512640 135094434 3221224432 3221223024 134556785 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28129/statm): 8264 7632 145 145 0 8119 0
[pid=28129] vsize: 33056
Current children cumulated CPU time (s) 119.4
Current children cumulated vsize (Kb) 35180

[startup+130.013 s]
Raw data (loadavg): 0.99 0.98 0.93 2/57 28129
Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28125/statm): 531 226 485 147 0 384 0
[pid=28125] vsize: 2124
Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 8413 0 0 0 12891 42 0 0 25 0 1 0 1855612436 35438592 8023 4294967295 134512640 135094434 3221224432 3221223088 134557917 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28129/statm): 8652 8023 145 145 0 8507 0
[pid=28129] vsize: 34608
Current children cumulated CPU time (s) 129.35
Current children cumulated vsize (Kb) 36732

[startup+140.014 s]
Raw data (loadavg): 0.99 0.98 0.93 2/57 28129
Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28125/statm): 531 226 485 147 0 384 0
[pid=28125] vsize: 2124
Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 8967 0 0 0 13883 46 0 0 25 0 1 0 1855612436 37695488 8577 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28129/statm): 9203 8577 145 145 0 9058 0
[pid=28129] vsize: 36812
Current children cumulated CPU time (s) 139.31
Current children cumulated vsize (Kb) 38936

[startup+150.015 s]
Raw data (loadavg): 0.99 0.98 0.93 2/57 28129
Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28125/statm): 531 226 485 147 0 384 0
[pid=28125] vsize: 2124
Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 9555 0 0 0 14873 49 0 0 25 0 1 0 1855612436 40095744 9165 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28129/statm): 9789 9165 145 145 0 9644 0
[pid=28129] vsize: 39156
Current children cumulated CPU time (s) 149.24
Current children cumulated vsize (Kb) 41280

[startup+160.016 s]
Raw data (loadavg): 0.99 0.98 0.93 2/57 28129
Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28125/statm): 531 226 485 147 0 384 0
[pid=28125] vsize: 2124
Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 10100 0 0 0 15866 53 0 0 25 0 1 0 1855612436 42319872 9710 4294967295 134512640 135094434 3221224432 3221223088 134557945 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28129/statm): 10332 9710 145 145 0 10187 0
[pid=28129] vsize: 41328
Current children cumulated CPU time (s) 159.21
Current children cumulated vsize (Kb) 43452

[startup+170.016 s]
Raw data (loadavg): 0.99 0.98 0.93 2/57 28129
Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28125/statm): 531 226 485 147 0 384 0
[pid=28125] vsize: 2124
Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 10607 0 0 0 16857 56 0 0 25 0 1 0 1855612436 44392448 10217 4294967295 134512640 135094434 3221224432 3221223024 134557137 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28129/statm): 10838 10217 145 145 0 10693 0
[pid=28129] vsize: 43352
Current children cumulated CPU time (s) 169.15
Current children cumulated vsize (Kb) 45476

[startup+180.017 s]
Raw data (loadavg): 0.99 0.98 0.93 2/57 28129
Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28125/statm): 531 226 485 147 0 384 0
[pid=28125] vsize: 2124
Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 11089 0 0 0 17849 60 0 0 25 0 1 0 1855612436 46362624 10699 4294967295 134512640 135094434 3221224432 3221223024 134556851 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28129/statm): 11319 10699 145 145 0 11174 0
[pid=28129] vsize: 45276
Current children cumulated CPU time (s) 179.11
Current children cumulated vsize (Kb) 47400

[startup+190.018 s]
Raw data (loadavg): 0.99 0.98 0.93 2/57 28129
Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28125/statm): 531 226 485 147 0 384 0
[pid=28125] vsize: 2124
Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 11545 0 0 0 18841 62 0 0 25 0 1 0 1855612436 48230400 11155 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28129/statm): 11775 11155 145 145 0 11630 0
[pid=28129] vsize: 47100
Current children cumulated CPU time (s) 189.05
Current children cumulated vsize (Kb) 49224

[startup+200.019 s]
Raw data (loadavg): 0.99 0.98 0.93 2/57 28129
Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28125/statm): 531 226 485 147 0 384 0
[pid=28125] vsize: 2124
Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 11970 0 0 0 19834 65 0 0 25 0 1 0 1855612436 49971200 11580 4294967295 134512640 135094434 3221224432 3221223024 134557004 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28129/statm): 12200 11580 145 145 0 12055 0
[pid=28129] vsize: 48800
Current children cumulated CPU time (s) 199.01
Current children cumulated vsize (Kb) 50924

[startup+210.02 s]
Raw data (loadavg): 0.99 0.98 0.93 2/57 28129
Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28125/statm): 531 226 485 147 0 384 0
[pid=28125] vsize: 2124
Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 12325 0 0 0 20829 67 0 0 25 0 1 0 1855612436 51433472 11935 4294967295 134512640 135094434 3221224432 3221223024 134556773 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28129/statm): 12557 11935 145 145 0 12412 0
[pid=28129] vsize: 50228
Current children cumulated CPU time (s) 208.98
Current children cumulated vsize (Kb) 52352

[startup+220.021 s]
Raw data (loadavg): 0.99 0.98 0.93 2/57 28129
Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28125/statm): 531 226 485 147 0 384 0
[pid=28125] vsize: 2124
Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 12654 0 0 0 21822 69 0 0 25 0 1 0 1855612436 52776960 12264 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28129/statm): 12885 12264 145 145 0 12740 0
[pid=28129] vsize: 51540
Current children cumulated CPU time (s) 218.93
Current children cumulated vsize (Kb) 53664

[startup+230.021 s]
Raw data (loadavg): 0.99 0.98 0.93 2/57 28129
Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28125/statm): 531 226 485 147 0 384 0
[pid=28125] vsize: 2124
Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 12967 0 0 0 22817 70 0 0 25 0 1 0 1855612436 54054912 12577 4294967295 134512640 135094434 3221224432 3221223104 134556094 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28129/statm): 13197 12577 145 145 0 13052 0
[pid=28129] vsize: 52788
Current children cumulated CPU time (s) 228.89
Current children cumulated vsize (Kb) 54912

[startup+240.022 s]
Raw data (loadavg): 0.99 0.98 0.93 2/57 28129
Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28125/statm): 531 226 485 147 0 384 0
[pid=28125] vsize: 2124
Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 13299 0 0 0 23812 73 0 0 25 0 1 0 1855612436 55406592 12909 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28129/statm): 13527 12909 145 145 0 13382 0
[pid=28129] vsize: 54108
Current children cumulated CPU time (s) 238.87
Current children cumulated vsize (Kb) 56232

[startup+250.023 s]
Raw data (loadavg): 0.99 0.98 0.93 2/57 28129
Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28125/statm): 531 226 485 147 0 384 0
[pid=28125] vsize: 2124
Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 13671 0 0 0 24807 75 0 0 25 0 1 0 1855612436 56922112 13281 4294967295 134512640 135094434 3221224432 3221223024 134557202 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28129/statm): 13897 13281 145 145 0 13752 0
[pid=28129] vsize: 55588
Current children cumulated CPU time (s) 248.84
Current children cumulated vsize (Kb) 57712

[startup+260.024 s]
Raw data (loadavg): 0.99 0.98 0.93 2/57 28129
Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28125/statm): 531 226 485 147 0 384 0
[pid=28125] vsize: 2124
Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 14142 0 0 0 25799 79 0 0 25 0 1 0 1855612436 58855424 13752 4294967295 134512640 135094434 3221224432 3221223088 134557903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28129/statm): 14369 13752 145 145 0 14224 0
[pid=28129] vsize: 57476
Current children cumulated CPU time (s) 258.8
Current children cumulated vsize (Kb) 59600

[startup+270.025 s]
Raw data (loadavg): 0.99 0.98 0.93 2/57 28129
Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28125/statm): 531 226 485 147 0 384 0
[pid=28125] vsize: 2124
Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 14568 0 0 0 26792 82 0 0 25 0 1 0 1855612436 60592128 14178 4294967295 134512640 135094434 3221224432 3221223024 134556853 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28129/statm): 14793 14178 145 145 0 14648 0
[pid=28129] vsize: 59172
Current children cumulated CPU time (s) 268.76
Current children cumulated vsize (Kb) 61296

[startup+280.027 s]
Raw data (loadavg): 0.99 0.98 0.93 2/57 28129
Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28125/statm): 531 226 485 147 0 384 0
[pid=28125] vsize: 2124
Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 15004 0 0 0 27783 85 0 0 25 0 1 0 1855612436 62365696 14614 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28129/statm): 15226 14614 145 145 0 15081 0
[pid=28129] vsize: 60904
Current children cumulated CPU time (s) 278.7
Current children cumulated vsize (Kb) 63028

[startup+290.027 s]
Raw data (loadavg): 0.99 0.98 0.93 2/57 28129
Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28125/statm): 531 226 485 147 0 384 0
[pid=28125] vsize: 2124
Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 15467 0 0 0 28777 87 0 0 25 0 1 0 1855612436 64253952 15077 4294967295 134512640 135094434 3221224432 3221223024 134556862 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28129/statm): 15687 15077 145 145 0 15542 0
[pid=28129] vsize: 62748
Current children cumulated CPU time (s) 288.66
Current children cumulated vsize (Kb) 64872

[startup+300.028 s]
Raw data (loadavg): 0.99 0.98 0.93 2/57 28129
Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28125/statm): 531 226 485 147 0 384 0
[pid=28125] vsize: 2124
Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 15916 0 0 0 29769 90 0 0 25 0 1 0 1855612436 66347008 15526 4294967295 134512640 135094434 3221224432 3221223024 134557518 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28129/statm): 16198 15526 145 145 0 16053 0
[pid=28129] vsize: 64792
Current children cumulated CPU time (s) 298.61
Current children cumulated vsize (Kb) 66916

[startup+310.029 s]
Raw data (loadavg): 0.99 0.98 0.93 2/57 28129
Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28125/statm): 531 226 485 147 0 384 0
[pid=28125] vsize: 2124
Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 16348 0 0 0 30762 94 0 0 25 0 1 0 1855612436 68112384 15958 4294967295 134512640 135094434 3221224432 3221223024 134556826 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28129/statm): 16629 15958 145 145 0 16484 0
[pid=28129] vsize: 66516
Current children cumulated CPU time (s) 308.58
Current children cumulated vsize (Kb) 68640

[startup+320.029 s]
Raw data (loadavg): 0.99 0.98 0.93 2/57 28129
Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28125/statm): 531 226 485 147 0 384 0
[pid=28125] vsize: 2124
Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 16665 0 0 0 31757 96 0 0 25 0 1 0 1855612436 69402624 16275 4294967295 134512640 135094434 3221224432 3221223088 134557950 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28129/statm): 16944 16275 145 145 0 16799 0
[pid=28129] vsize: 67776
Current children cumulated CPU time (s) 318.55
Current children cumulated vsize (Kb) 69900

[startup+330.03 s]
Raw data (loadavg): 0.99 0.98 0.93 2/57 28129
Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28125/statm): 531 226 485 147 0 384 0
[pid=28125] vsize: 2124
Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 17076 0 0 0 32748 99 0 0 25 0 1 0 1855612436 71073792 16686 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28129/statm): 17352 16686 145 145 0 17207 0
[pid=28129] vsize: 69408
Current children cumulated CPU time (s) 328.49
Current children cumulated vsize (Kb) 71532

[startup+340.031 s]
Raw data (loadavg): 0.99 0.98 0.93 2/57 28129
Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28125/statm): 531 226 485 147 0 384 0
[pid=28125] vsize: 2124
Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 17610 0 0 0 33740 103 0 0 25 0 1 0 1855612436 73252864 17220 4294967295 134512640 135094434 3221224432 3221223088 134558246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28129/statm): 17884 17220 145 145 0 17739 0
[pid=28129] vsize: 71536
Current children cumulated CPU time (s) 338.45
Current children cumulated vsize (Kb) 73660

[startup+350.032 s]
Raw data (loadavg): 0.99 0.98 0.93 2/57 28129
Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28125/statm): 531 226 485 147 0 384 0
[pid=28125] vsize: 2124
Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 18065 0 0 0 34733 106 0 0 25 0 1 0 1855612436 75108352 17675 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28129/statm): 18337 17675 145 145 0 18192 0
[pid=28129] vsize: 73348
Current children cumulated CPU time (s) 348.41
Current children cumulated vsize (Kb) 75472

[startup+360.033 s]
Raw data (loadavg): 0.99 0.98 0.93 2/57 28129
Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28125/statm): 531 226 485 147 0 384 0
[pid=28125] vsize: 2124
Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 18582 0 0 0 35726 109 0 0 25 0 1 0 1855612436 77221888 18192 4294967295 134512640 135094434 3221224432 3221223024 134556785 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28129/statm): 18853 18192 145 145 0 18708 0
[pid=28129] vsize: 75412
Current children cumulated CPU time (s) 358.37
Current children cumulated vsize (Kb) 77536

[startup+370.034 s]
Raw data (loadavg): 0.99 0.98 0.93 2/57 28129
Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28125/statm): 531 226 485 147 0 384 0
[pid=28125] vsize: 2124
Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 19020 0 0 0 36719 112 0 0 25 0 1 0 1855612436 79007744 18630 4294967295 134512640 135094434 3221224432 3221223104 134555821 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28129/statm): 19289 18630 145 145 0 19144 0
[pid=28129] vsize: 77156
Current children cumulated CPU time (s) 368.33
Current children cumulated vsize (Kb) 79280

[startup+380.035 s]
Raw data (loadavg): 0.99 0.98 0.93 2/57 28129
Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28125/statm): 531 226 485 147 0 384 0
[pid=28125] vsize: 2124
Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 19468 0 0 0 37711 115 0 0 25 0 1 0 1855612436 80838656 19078 4294967295 134512640 135094434 3221224432 3221223024 134557208 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28129/statm): 19736 19078 145 145 0 19591 0
[pid=28129] vsize: 78944
Current children cumulated CPU time (s) 378.28
Current children cumulated vsize (Kb) 81068

[startup+390.036 s]
Raw data (loadavg): 0.99 0.98 0.93 2/57 28129
Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28125/statm): 531 226 485 147 0 384 0
[pid=28125] vsize: 2124
Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 19923 0 0 0 38704 118 0 0 25 0 1 0 1855612436 82694144 19533 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28129/statm): 20189 19533 145 145 0 20044 0
[pid=28129] vsize: 80756
Current children cumulated CPU time (s) 388.24
Current children cumulated vsize (Kb) 82880

[startup+400.036 s]
Raw data (loadavg): 0.99 0.98 0.93 2/57 28129
Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28125/statm): 531 226 485 147 0 384 0
[pid=28125] vsize: 2124
Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 20387 0 0 0 39698 121 0 0 25 0 1 0 1855612436 84586496 19997 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28129/statm): 20651 19997 145 145 0 20506 0
[pid=28129] vsize: 82604
Current children cumulated CPU time (s) 398.21
Current children cumulated vsize (Kb) 84728

[startup+410.037 s]
Raw data (loadavg): 0.99 0.98 0.93 2/57 28129
Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28125/statm): 531 226 485 147 0 384 0
[pid=28125] vsize: 2124
Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 20780 0 0 0 40692 124 0 0 25 0 1 0 1855612436 86188032 20390 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28129/statm): 21042 20390 145 145 0 20897 0
[pid=28129] vsize: 84168
Current children cumulated CPU time (s) 408.18
Current children cumulated vsize (Kb) 86292

[startup+420.038 s]
Raw data (loadavg): 0.99 0.98 0.93 2/57 28129
Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28125/statm): 531 226 485 147 0 384 0
[pid=28125] vsize: 2124
Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 21135 0 0 0 41685 125 0 0 25 0 1 0 1855612436 87633920 20745 4294967295 134512640 135094434 3221224432 3221223024 134556964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28129/statm): 21395 20745 145 145 0 21250 0
[pid=28129] vsize: 85580
Current children cumulated CPU time (s) 418.12
Current children cumulated vsize (Kb) 87704

[startup+430.039 s]
Raw data (loadavg): 0.99 0.98 0.93 2/57 28129
Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28125/statm): 531 226 485 147 0 384 0
[pid=28125] vsize: 2124
Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 21547 0 0 0 42678 129 0 0 25 0 1 0 1855612436 89313280 21157 4294967295 134512640 135094434 3221224432 3221223024 134556980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28129/statm): 21805 21157 145 145 0 21660 0
[pid=28129] vsize: 87220
Current children cumulated CPU time (s) 428.09
Current children cumulated vsize (Kb) 89344

[startup+440.039 s]
Raw data (loadavg): 0.99 0.98 0.93 2/57 28129
Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28125/statm): 531 226 485 147 0 384 0
[pid=28125] vsize: 2124
Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 22039 0 0 0 43670 132 0 0 25 0 1 0 1855612436 91324416 21649 4294967295 134512640 135094434 3221224432 3221223024 134556851 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28129/statm): 22296 21649 145 145 0 22151 0
[pid=28129] vsize: 89184
Current children cumulated CPU time (s) 438.04
Current children cumulated vsize (Kb) 91308

[startup+450.041 s]
Raw data (loadavg): 0.99 0.98 0.93 2/57 28129
Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28125/statm): 531 226 485 147 0 384 0
[pid=28125] vsize: 2124
Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 22573 0 0 0 44663 134 0 0 25 0 1 0 1855612436 93503488 22183 4294967295 134512640 135094434 3221224432 3221223024 134556847 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28129/statm): 22828 22183 145 145 0 22683 0
[pid=28129] vsize: 91312
Current children cumulated CPU time (s) 447.99
Current children cumulated vsize (Kb) 93436

[startup+460.041 s]
Raw data (loadavg): 0.99 0.98 0.93 2/57 28129
Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28125/statm): 531 226 485 147 0 384 0
[pid=28125] vsize: 2124
Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 23105 0 0 0 45654 138 0 0 25 0 1 0 1855612436 95682560 22715 4294967295 134512640 135094434 3221224432 3221223024 134557042 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28129/statm): 23360 22715 145 145 0 23215 0
[pid=28129] vsize: 93440
Current children cumulated CPU time (s) 457.94
Current children cumulated vsize (Kb) 95564

[startup+470.041 s]
Raw data (loadavg): 0.99 0.98 0.93 2/57 28129
Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28125/statm): 531 226 485 147 0 384 0
[pid=28125] vsize: 2124
Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 23607 0 0 0 46648 140 0 0 25 0 1 0 1855612436 97738752 23217 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28129/statm): 23862 23217 145 145 0 23717 0
[pid=28129] vsize: 95448
Current children cumulated CPU time (s) 467.9
Current children cumulated vsize (Kb) 97572

[startup+480.042 s]
Raw data (loadavg): 0.99 0.98 0.93 2/57 28129
Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28125/statm): 531 226 485 147 0 384 0
[pid=28125] vsize: 2124
Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 23960 0 0 0 47642 143 0 0 25 0 1 0 1855612436 99180544 23570 4294967295 134512640 135094434 3221224432 3221223024 134557152 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28129/statm): 24214 23570 145 145 0 24069 0
[pid=28129] vsize: 96856
Current children cumulated CPU time (s) 477.87
Current children cumulated vsize (Kb) 98980

[startup+490.043 s]
Raw data (loadavg): 0.99 0.98 0.93 2/57 28129
Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28125/statm): 531 226 485 147 0 384 0
[pid=28125] vsize: 2124
Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 24337 0 0 0 48637 145 0 0 25 0 1 0 1855612436 100716544 23947 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28129/statm): 24589 23947 145 145 0 24444 0
[pid=28129] vsize: 98356
Current children cumulated CPU time (s) 487.84
Current children cumulated vsize (Kb) 100480

[startup+500.044 s]
Raw data (loadavg): 0.99 0.98 0.93 2/57 28129
Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28125/statm): 531 226 485 147 0 384 0
[pid=28125] vsize: 2124
Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 24634 0 0 0 49632 147 0 0 25 0 1 0 1855612436 101924864 24244 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28129/statm): 24884 24244 145 145 0 24739 0
[pid=28129] vsize: 99536
Current children cumulated CPU time (s) 497.81
Current children cumulated vsize (Kb) 101660

[startup+510.045 s]
Raw data (loadavg): 0.99 0.98 0.93 2/57 28129
Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28125/statm): 531 226 485 147 0 384 0
[pid=28125] vsize: 2124
Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 25070 0 0 0 50626 151 0 0 25 0 1 0 1855612436 103706624 24680 4294967295 134512640 135094434 3221224432 3221223056 134557737 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28129/statm): 25319 24680 145 145 0 25174 0
[pid=28129] vsize: 101276
Current children cumulated CPU time (s) 507.79
Current children cumulated vsize (Kb) 103400

[startup+520.045 s]
Raw data (loadavg): 0.99 0.98 0.93 2/57 28129
Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28125/statm): 531 226 485 147 0 384 0
[pid=28125] vsize: 2124
Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 25554 0 0 0 51617 155 0 0 25 0 1 0 1855612436 105680896 25164 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28129/statm): 25801 25164 145 145 0 25656 0
[pid=28129] vsize: 103204
Current children cumulated CPU time (s) 517.74
Current children cumulated vsize (Kb) 105328

[startup+530.046 s]
Raw data (loadavg): 0.99 0.98 0.93 2/57 28129
Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28125/statm): 531 226 485 147 0 384 0
[pid=28125] vsize: 2124
Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 26025 0 0 0 52610 157 0 0 25 0 1 0 1855612436 107606016 25635 4294967295 134512640 135094434 3221224432 3221223024 134557133 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28129/statm): 26271 25635 145 145 0 26126 0
[pid=28129] vsize: 105084
Current children cumulated CPU time (s) 527.69
Current children cumulated vsize (Kb) 107208

[startup+540.047 s]
Raw data (loadavg): 0.99 0.98 0.93 2/57 28129
Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28125/statm): 531 226 485 147 0 384 0
[pid=28125] vsize: 2124
Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 26451 0 0 0 53604 160 0 0 25 0 1 0 1855612436 109346816 26061 4294967295 134512640 135094434 3221224432 3221223024 134556789 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28129/statm): 26696 26061 145 145 0 26551 0
[pid=28129] vsize: 106784
Current children cumulated CPU time (s) 537.66
Current children cumulated vsize (Kb) 108908

[startup+550.048 s]
Raw data (loadavg): 0.99 0.98 0.93 2/57 28129
Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28125/statm): 531 226 485 147 0 384 0
[pid=28125] vsize: 2124
Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 26892 0 0 0 54595 165 0 0 25 0 1 0 1855612436 111144960 26502 4294967295 134512640 135094434 3221224432 3221223024 134557141 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28129/statm): 27135 26502 145 145 0 26990 0
[pid=28129] vsize: 108540
Current children cumulated CPU time (s) 547.62
Current children cumulated vsize (Kb) 110664

[startup+560.049 s]
Raw data (loadavg): 0.99 0.98 0.93 2/57 28129
Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28125/statm): 531 226 485 147 0 384 0
[pid=28125] vsize: 2124
Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 27342 0 0 0 55588 168 0 0 25 0 1 0 1855612436 112984064 26952 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28129/statm): 27584 26952 145 145 0 27439 0
[pid=28129] vsize: 110336
Current children cumulated CPU time (s) 557.58
Current children cumulated vsize (Kb) 112460

[startup+570.049 s]
Raw data (loadavg): 0.99 0.98 0.93 2/57 28129
Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28125/statm): 531 226 485 147 0 384 0
[pid=28125] vsize: 2124
Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 27750 0 0 0 56581 172 0 0 25 0 1 0 1855612436 114651136 27360 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28129/statm): 27991 27360 145 145 0 27846 0
[pid=28129] vsize: 111964
Current children cumulated CPU time (s) 567.55
Current children cumulated vsize (Kb) 114088

[startup+580.05 s]
Raw data (loadavg): 0.99 0.98 0.93 2/57 28129
Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28125/statm): 531 226 485 147 0 384 0
[pid=28125] vsize: 2124
Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 28145 0 0 0 57572 175 0 0 25 0 1 0 1855612436 116264960 27755 4294967295 134512640 135094434 3221224432 3221223024 134556958 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28129/statm): 28385 27755 145 145 0 28240 0
[pid=28129] vsize: 113540
Current children cumulated CPU time (s) 577.49
Current children cumulated vsize (Kb) 115664

[startup+590.051 s]
Raw data (loadavg): 0.99 0.98 0.93 2/57 28129
Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28125/statm): 531 226 485 147 0 384 0
[pid=28125] vsize: 2124
Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 28540 0 0 0 58567 178 0 0 25 0 1 0 1855612436 117878784 28150 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28129/statm): 28779 28150 145 145 0 28634 0
[pid=28129] vsize: 115116
Current children cumulated CPU time (s) 587.47
Current children cumulated vsize (Kb) 117240

[startup+600.052 s]
Raw data (loadavg): 0.99 0.98 0.93 2/57 28129
Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28125/statm): 531 226 485 147 0 384 0
[pid=28125] vsize: 2124
Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 28872 0 0 0 59562 180 0 0 25 0 1 0 1855612436 119230464 28482 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28129/statm): 29109 28482 145 145 0 28964 0
[pid=28129] vsize: 116436
Current children cumulated CPU time (s) 597.44
Current children cumulated vsize (Kb) 118560

[startup+610.053 s]
Raw data (loadavg): 0.99 0.98 0.93 2/57 28129
Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28125/statm): 531 226 485 147 0 384 0
[pid=28125] vsize: 2124
Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 29378 0 0 0 60554 183 0 0 25 0 1 0 1855612436 121307136 28988 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28129/statm): 29616 28988 145 145 0 29471 0
[pid=28129] vsize: 118464
Current children cumulated CPU time (s) 607.39
Current children cumulated vsize (Kb) 120588

[startup+620.054 s]
Raw data (loadavg): 0.99 0.98 0.93 1/57 28129
Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28125/statm): 531 226 485 147 0 384 0
[pid=28125] vsize: 2124
Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) T 28125 28125 28974 0 -1 0 29897 0 0 0 61547 186 0 0 25 0 1 0 1855612436 123428864 29507 4294967295 134512640 135094434 3221224432 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/28129/statm): 30134 29507 145 145 0 29989 0
[pid=28129] vsize: 120536
Current children cumulated CPU time (s) 617.35
Current children cumulated vsize (Kb) 122660

[startup+630.055 s]
Raw data (loadavg): 0.99 0.98 0.93 2/57 28129
Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28125/statm): 531 226 485 147 0 384 0
[pid=28125] vsize: 2124
Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 30586 0 0 0 62535 191 0 0 25 0 1 0 1855612436 126238720 30196 4294967295 134512640 135094434 3221224432 3221223024 134557537 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28129/statm): 30820 30196 145 145 0 30675 0
[pid=28129] vsize: 123280
Current children cumulated CPU time (s) 627.28
Current children cumulated vsize (Kb) 125404

[startup+640.056 s]
Raw data (loadavg): 0.99 0.98 0.93 2/57 28129
Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28125/statm): 531 226 485 147 0 384 0
[pid=28125] vsize: 2124
Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 31194 0 0 0 63527 194 0 0 25 0 1 0 1855612436 128724992 30804 4294967295 134512640 135094434 3221224432 3221223024 134557002 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28129/statm): 31427 30804 145 145 0 31282 0
[pid=28129] vsize: 125708
Current children cumulated CPU time (s) 637.23
Current children cumulated vsize (Kb) 127832

[startup+650.057 s]
Raw data (loadavg): 0.99 0.98 0.93 2/57 28129
Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28125/statm): 531 226 485 147 0 384 0
[pid=28125] vsize: 2124
Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 31576 0 0 0 64520 198 0 0 24 0 1 0 1855612436 130281472 31186 4294967295 134512640 135094434 3221224432 3221223024 134557182 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28129/statm): 31807 31186 145 145 0 31662 0
[pid=28129] vsize: 127228
Current children cumulated CPU time (s) 647.2
Current children cumulated vsize (Kb) 129352

[startup+660.058 s]
Raw data (loadavg): 0.99 0.98 0.93 2/57 28129
Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28125/statm): 531 226 485 147 0 384 0
[pid=28125] vsize: 2124
Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 32149 0 0 0 65512 201 0 0 25 0 1 0 1855612436 132624384 31759 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28129/statm): 32379 31759 145 145 0 32234 0
[pid=28129] vsize: 129516
Current children cumulated CPU time (s) 657.15
Current children cumulated vsize (Kb) 131640

[startup+670.059 s]
Raw data (loadavg): 0.99 0.98 0.93 2/57 28129
Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28125/statm): 531 226 485 147 0 384 0
[pid=28125] vsize: 2124
Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 32635 0 0 0 66503 206 0 0 25 0 1 0 1855612436 134610944 32245 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28129/statm): 32864 32245 145 145 0 32719 0
[pid=28129] vsize: 131456
Current children cumulated CPU time (s) 667.11
Current children cumulated vsize (Kb) 133580

[startup+680.06 s]
Raw data (loadavg): 0.99 0.98 0.93 2/57 28129
Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28125/statm): 531 226 485 147 0 384 0
[pid=28125] vsize: 2124
Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 32982 0 0 0 67496 209 0 0 24 0 1 0 1855612436 136024064 32592 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28129/statm): 33209 32592 145 145 0 33064 0
[pid=28129] vsize: 132836
Current children cumulated CPU time (s) 677.07
Current children cumulated vsize (Kb) 134960

[startup+690.06 s]
Raw data (loadavg): 0.99 0.98 0.93 2/57 28129
Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28125/statm): 531 226 485 147 0 384 0
[pid=28125] vsize: 2124
Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 33304 0 0 0 68491 211 0 0 25 0 1 0 1855612436 137338880 32914 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28129/statm): 33530 32914 145 145 0 33385 0
[pid=28129] vsize: 134120
Current children cumulated CPU time (s) 687.04
Current children cumulated vsize (Kb) 136244

[startup+700.061 s]
Raw data (loadavg): 0.99 0.98 0.93 2/57 28129
Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28125/statm): 531 226 485 147 0 384 0
[pid=28125] vsize: 2124
Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 33508 0 0 0 69486 214 0 0 25 0 1 0 1855612436 138690560 33118 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28129/statm): 33860 33118 145 145 0 33715 0
[pid=28129] vsize: 135440
Current children cumulated CPU time (s) 697.02
Current children cumulated vsize (Kb) 137564

[startup+710.062 s]
Raw data (loadavg): 0.99 0.98 0.93 2/57 28129
Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28125/statm): 531 226 485 147 0 384 0
[pid=28125] vsize: 2124
Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 33789 0 0 0 70481 215 0 0 25 0 1 0 1855612436 139837440 33399 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28129/statm): 34140 33399 145 145 0 33995 0
[pid=28129] vsize: 136560
Current children cumulated CPU time (s) 706.98
Current children cumulated vsize (Kb) 138684

[startup+720.062 s]
Raw data (loadavg): 0.99 0.98 0.93 2/57 28129
Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28125/statm): 531 226 485 147 0 384 0
[pid=28125] vsize: 2124
Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) T 28125 28125 28974 0 -1 0 34296 0 0 0 71473 219 0 0 25 0 1 0 1855612436 141910016 33906 4294967295 134512640 135094434 3221224432 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/28129/statm): 34646 33906 145 145 0 34501 0
[pid=28129] vsize: 138584
Current children cumulated CPU time (s) 716.94
Current children cumulated vsize (Kb) 140708

[startup+730.063 s]
Raw data (loadavg): 0.99 0.98 0.93 2/57 28129
Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28125/statm): 531 226 485 147 0 384 0
[pid=28125] vsize: 2124
Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 34922 0 0 0 72464 223 0 0 25 0 1 0 1855612436 144465920 34532 4294967295 134512640 135094434 3221224432 3221223056 134557696 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28129/statm): 35270 34532 145 145 0 35125 0
[pid=28129] vsize: 141080
Current children cumulated CPU time (s) 726.89
Current children cumulated vsize (Kb) 143204

[startup+740.063 s]
Raw data (loadavg): 0.99 0.98 0.93 2/57 28129
Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28125/statm): 531 226 485 147 0 384 0
[pid=28125] vsize: 2124
Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 35465 0 0 0 73456 226 0 0 25 0 1 0 1855612436 146685952 35075 4294967295 134512640 135094434 3221224432 3221223024 134557137 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28129/statm): 35812 35075 145 145 0 35667 0
[pid=28129] vsize: 143248
Current children cumulated CPU time (s) 736.84
Current children cumulated vsize (Kb) 145372

[startup+750.064 s]
Raw data (loadavg): 0.99 0.98 0.93 2/57 28129
Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28125/statm): 531 226 485 147 0 384 0
[pid=28125] vsize: 2124
Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 35951 0 0 0 74448 229 0 0 25 0 1 0 1855612436 148672512 35561 4294967295 134512640 135094434 3221224432 3221223024 134556941 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28129/statm): 36297 35561 145 145 0 36152 0
[pid=28129] vsize: 145188
Current children cumulated CPU time (s) 746.79
Current children cumulated vsize (Kb) 147312

[startup+760.065 s]
Raw data (loadavg): 0.99 0.98 0.93 2/57 28129
Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28125/statm): 531 226 485 147 0 384 0
[pid=28125] vsize: 2124
Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 36396 0 0 0 75443 231 0 0 25 0 1 0 1855612436 150491136 36006 4294967295 134512640 135094434 3221224432 3221223024 134557028 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28129/statm): 36741 36006 145 145 0 36596 0
[pid=28129] vsize: 146964
Current children cumulated CPU time (s) 756.76
Current children cumulated vsize (Kb) 149088

[startup+770.065 s]
Raw data (loadavg): 0.99 0.98 0.93 2/57 28129
Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28125/statm): 531 226 485 147 0 384 0
[pid=28125] vsize: 2124
Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 36873 0 0 0 76436 234 0 0 25 0 1 0 1855612436 152440832 36483 4294967295 134512640 135094434 3221224432 3221223104 134555568 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28129/statm): 37217 36483 145 145 0 37072 0
[pid=28129] vsize: 148868
Current children cumulated CPU time (s) 766.72
Current children cumulated vsize (Kb) 150992

[startup+780.066 s]
Raw data (loadavg): 0.99 0.98 0.93 2/57 28129
Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28125/statm): 531 226 485 147 0 384 0
[pid=28125] vsize: 2124
Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 37288 0 0 0 77431 237 0 0 25 0 1 0 1855612436 154132480 36898 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28129/statm): 37630 36898 145 145 0 37485 0
[pid=28129] vsize: 150520
Current children cumulated CPU time (s) 776.7
Current children cumulated vsize (Kb) 152644

[startup+790.067 s]
Raw data (loadavg): 0.99 0.98 0.93 2/57 28129
Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28125/statm): 531 226 485 147 0 384 0
[pid=28125] vsize: 2124
Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 37614 0 0 0 78424 239 0 0 25 0 1 0 1855612436 155467776 37224 4294967295 134512640 135094434 3221224432 3221223056 134557593 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28129/statm): 37956 37224 145 145 0 37811 0
[pid=28129] vsize: 151824
Current children cumulated CPU time (s) 786.65
Current children cumulated vsize (Kb) 153948

[startup+800.068 s]
Raw data (loadavg): 0.99 0.98 0.93 2/57 28129
Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28125/statm): 531 226 485 147 0 384 0
[pid=28125] vsize: 2124
Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 38039 0 0 0 79418 241 0 0 25 0 1 0 1855612436 157204480 37649 4294967295 134512640 135094434 3221224432 3221223104 134556295 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28129/statm): 38380 37649 145 145 0 38235 0
[pid=28129] vsize: 153520
Current children cumulated CPU time (s) 796.61
Current children cumulated vsize (Kb) 155644

[startup+810.069 s]
Raw data (loadavg): 0.99 0.98 0.93 2/57 28129
Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28125/statm): 531 226 485 147 0 384 0
[pid=28125] vsize: 2124
Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 38431 0 0 0 80412 244 0 0 25 0 1 0 1855612436 158810112 38041 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28129/statm): 38772 38041 145 145 0 38627 0
[pid=28129] vsize: 155088
Current children cumulated CPU time (s) 806.58
Current children cumulated vsize (Kb) 157212

[startup+820.07 s]
Raw data (loadavg): 0.99 0.98 0.93 2/57 28129
Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28125/statm): 531 226 485 147 0 384 0
[pid=28125] vsize: 2124
Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 38754 0 0 0 81408 246 0 0 25 0 1 0 1855612436 160129024 38364 4294967295 134512640 135094434 3221224432 3221223092 134553480 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28129/statm): 39094 38364 145 145 0 38949 0
[pid=28129] vsize: 156376
Current children cumulated CPU time (s) 816.56
Current children cumulated vsize (Kb) 158500

[startup+830.071 s]
Raw data (loadavg): 0.99 0.98 0.93 2/57 28129
Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28125/statm): 531 226 485 147 0 384 0
[pid=28125] vsize: 2124
Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 38859 0 0 0 82406 247 0 0 25 0 1 0 1855612436 160555008 38469 4294967295 134512640 135094434 3221224432 3221223024 134556961 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28129/statm): 39198 38469 145 145 0 39053 0
[pid=28129] vsize: 156792
Current children cumulated CPU time (s) 826.55
Current children cumulated vsize (Kb) 158916

[startup+840.072 s]
Raw data (loadavg): 0.99 0.98 0.93 2/57 28129
Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28125/statm): 531 226 485 147 0 384 0
[pid=28125] vsize: 2124
Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 38859 0 0 0 83407 247 0 0 25 0 1 0 1855612436 160555008 38469 4294967295 134512640 135094434 3221224432 3221223024 134557528 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28129/statm): 39198 38469 145 145 0 39053 0
[pid=28129] vsize: 156792
Current children cumulated CPU time (s) 836.56
Current children cumulated vsize (Kb) 158916

[startup+850.073 s]
Raw data (loadavg): 0.99 0.98 0.93 2/57 28129
Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28125/statm): 531 226 485 147 0 384 0
[pid=28125] vsize: 2124
Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 38859 0 0 0 84407 247 0 0 25 0 1 0 1855612436 160555008 38469 4294967295 134512640 135094434 3221224432 3221223024 134556866 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28129/statm): 39198 38469 145 145 0 39053 0
[pid=28129] vsize: 156792
Current children cumulated CPU time (s) 846.56
Current children cumulated vsize (Kb) 158916

[startup+860.073 s]
Raw data (loadavg): 0.99 0.98 0.93 2/57 28129
Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28125/statm): 531 226 485 147 0 384 0
[pid=28125] vsize: 2124
Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 38859 0 0 0 85407 247 0 0 25 0 1 0 1855612436 160555008 38469 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28129/statm): 39198 38469 145 145 0 39053 0
[pid=28129] vsize: 156792
Current children cumulated CPU time (s) 856.56
Current children cumulated vsize (Kb) 158916

[startup+870.074 s]
Raw data (loadavg): 0.99 0.98 0.93 2/57 28129
Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28125/statm): 531 226 485 147 0 384 0
[pid=28125] vsize: 2124
Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 38859 0 0 0 86407 247 0 0 25 0 1 0 1855612436 160555008 38469 4294967295 134512640 135094434 3221224432 3221223024 134557196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28129/statm): 39198 38469 145 145 0 39053 0
[pid=28129] vsize: 156792
Current children cumulated CPU time (s) 866.56
Current children cumulated vsize (Kb) 158916

[startup+880.075 s]
Raw data (loadavg): 0.99 0.98 0.93 2/57 28129
Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28125/statm): 531 226 485 147 0 384 0
[pid=28125] vsize: 2124
Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 38859 0 0 0 87407 247 0 0 25 0 1 0 1855612436 160555008 38469 4294967295 134512640 135094434 3221224432 3221223088 134557956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28129/statm): 39198 38469 145 145 0 39053 0
[pid=28129] vsize: 156792
Current children cumulated CPU time (s) 876.56
Current children cumulated vsize (Kb) 158916

[startup+890.076 s]
Raw data (loadavg): 0.99 0.98 0.93 2/57 28129
Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28125/statm): 531 226 485 147 0 384 0
[pid=28125] vsize: 2124
Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 38859 0 0 0 88407 247 0 0 25 0 1 0 1855612436 160555008 38469 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28129/statm): 39198 38469 145 145 0 39053 0
[pid=28129] vsize: 156792
Current children cumulated CPU time (s) 886.56
Current children cumulated vsize (Kb) 158916

[startup+900.078 s]
Raw data (loadavg): 0.99 0.98 0.93 2/57 28129
Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28125/statm): 531 226 485 147 0 384 0
[pid=28125] vsize: 2124
Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 38859 0 0 0 89408 247 0 0 25 0 1 0 1855612436 160555008 38469 4294967295 134512640 135094434 3221224432 3221223044 134563055 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28129/statm): 39198 38469 145 145 0 39053 0
[pid=28129] vsize: 156792
Current children cumulated CPU time (s) 896.57
Current children cumulated vsize (Kb) 158916

[startup+910.078 s]
Raw data (loadavg): 0.99 0.98 0.93 2/57 28129
Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28125/statm): 531 226 485 147 0 384 0
[pid=28125] vsize: 2124
Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 38859 0 0 0 90408 247 0 0 25 0 1 0 1855612436 160555008 38469 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28129/statm): 39198 38469 145 145 0 39053 0
[pid=28129] vsize: 156792
Current children cumulated CPU time (s) 906.57
Current children cumulated vsize (Kb) 158916

[startup+920.078 s]
Raw data (loadavg): 0.99 0.98 0.93 2/57 28129
Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28125/statm): 531 226 485 147 0 384 0
[pid=28125] vsize: 2124
Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 38859 0 0 0 91408 247 0 0 25 0 1 0 1855612436 160555008 38469 4294967295 134512640 135094434 3221224432 3221223024 134557328 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28129/statm): 39198 38469 145 145 0 39053 0
[pid=28129] vsize: 156792
Current children cumulated CPU time (s) 916.57
Current children cumulated vsize (Kb) 158916

[startup+930.079 s]
Raw data (loadavg): 0.99 0.98 0.93 2/57 28129
Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28125/statm): 531 226 485 147 0 384 0
[pid=28125] vsize: 2124
Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 38859 0 0 0 92408 247 0 0 25 0 1 0 1855612436 160555008 38469 4294967295 134512640 135094434 3221224432 3221223088 134557964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28129/statm): 39198 38469 145 145 0 39053 0
[pid=28129] vsize: 156792
Current children cumulated CPU time (s) 926.57
Current children cumulated vsize (Kb) 158916

[startup+940.08 s]
Raw data (loadavg): 0.99 0.98 0.93 2/57 28129
Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28125/statm): 531 226 485 147 0 384 0
[pid=28125] vsize: 2124
Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 38859 0 0 0 93409 247 0 0 25 0 1 0 1855612436 160555008 38469 4294967295 134512640 135094434 3221224432 3221223024 134556964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28129/statm): 39198 38469 145 145 0 39053 0
[pid=28129] vsize: 156792
Current children cumulated CPU time (s) 936.58
Current children cumulated vsize (Kb) 158916

[startup+950.081 s]
Raw data (loadavg): 0.99 0.98 0.93 2/57 28129
Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28125/statm): 531 226 485 147 0 384 0
[pid=28125] vsize: 2124
Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 38859 0 0 0 94409 247 0 0 25 0 1 0 1855612436 160555008 38469 4294967295 134512640 135094434 3221224432 3221223024 134557152 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28129/statm): 39198 38469 145 145 0 39053 0
[pid=28129] vsize: 156792
Current children cumulated CPU time (s) 946.58
Current children cumulated vsize (Kb) 158916

[startup+960.082 s]
Raw data (loadavg): 0.99 0.98 0.93 2/57 28129
Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28125/statm): 531 226 485 147 0 384 0
[pid=28125] vsize: 2124
Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 38859 0 0 0 95409 247 0 0 25 0 1 0 1855612436 160555008 38469 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28129/statm): 39198 38469 145 145 0 39053 0
[pid=28129] vsize: 156792
Current children cumulated CPU time (s) 956.58
Current children cumulated vsize (Kb) 158916

[startup+970.082 s]
Raw data (loadavg): 0.99 0.98 0.93 2/57 28129
Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28125/statm): 531 226 485 147 0 384 0
[pid=28125] vsize: 2124
Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 38859 0 0 0 96409 247 0 0 25 0 1 0 1855612436 160555008 38469 4294967295 134512640 135094434 3221224432 3221223024 134556966 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28129/statm): 39198 38469 145 145 0 39053 0
[pid=28129] vsize: 156792
Current children cumulated CPU time (s) 966.58
Current children cumulated vsize (Kb) 158916

[startup+980.083 s]
Raw data (loadavg): 0.99 0.98 0.93 2/57 28129
Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28125/statm): 531 226 485 147 0 384 0
[pid=28125] vsize: 2124
Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 38859 0 0 0 97409 247 0 0 25 0 1 0 1855612436 160555008 38469 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28129/statm): 39198 38469 145 145 0 39053 0
[pid=28129] vsize: 156792
Current children cumulated CPU time (s) 976.58
Current children cumulated vsize (Kb) 158916

[startup+990.084 s]
Raw data (loadavg): 0.99 0.98 0.93 2/57 28129
Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28125/statm): 531 226 485 147 0 384 0
[pid=28125] vsize: 2124
Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 38859 0 0 0 98410 247 0 0 25 0 1 0 1855612436 160555008 38469 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28129/statm): 39198 38469 145 145 0 39053 0
[pid=28129] vsize: 156792
Current children cumulated CPU time (s) 986.59
Current children cumulated vsize (Kb) 158916

[startup+1000.08 s]
Raw data (loadavg): 0.99 0.98 0.93 2/57 28129
Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28125/statm): 531 226 485 147 0 384 0
[pid=28125] vsize: 2124
Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 38859 0 0 0 99410 247 0 0 25 0 1 0 1855612436 160555008 38469 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28129/statm): 39198 38469 145 145 0 39053 0
[pid=28129] vsize: 156792
Current children cumulated CPU time (s) 996.59
Current children cumulated vsize (Kb) 158916

[startup+1010.09 s]
Raw data (loadavg): 0.99 0.98 0.93 2/57 28129
Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28125/statm): 531 226 485 147 0 384 0
[pid=28125] vsize: 2124
Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 38859 0 0 0 100410 247 0 0 25 0 1 0 1855612436 160555008 38469 4294967295 134512640 135094434 3221224432 3221223024 134557488 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28129/statm): 39198 38469 145 145 0 39053 0
[pid=28129] vsize: 156792
Current children cumulated CPU time (s) 1006.59
Current children cumulated vsize (Kb) 158916

[startup+1020.09 s]
Raw data (loadavg): 0.99 0.98 0.93 2/57 28129
Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28125/statm): 531 226 485 147 0 384 0
[pid=28125] vsize: 2124
Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 38859 0 0 0 101410 247 0 0 25 0 1 0 1855612436 160555008 38469 4294967295 134512640 135094434 3221224432 3221223088 134557872 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28129/statm): 39198 38469 145 145 0 39053 0
[pid=28129] vsize: 156792
Current children cumulated CPU time (s) 1016.59
Current children cumulated vsize (Kb) 158916

[startup+1030.09 s]
Raw data (loadavg): 0.99 0.98 0.93 2/57 28129
Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28125/statm): 531 226 485 147 0 384 0
[pid=28125] vsize: 2124
Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 38859 0 0 0 102410 248 0 0 25 0 1 0 1855612436 160555008 38469 4294967295 134512640 135094434 3221224432 3221223024 134557360 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28129/statm): 39198 38469 145 145 0 39053 0
[pid=28129] vsize: 156792
Current children cumulated CPU time (s) 1026.6
Current children cumulated vsize (Kb) 158916

[startup+1040.09 s]
Raw data (loadavg): 0.99 0.98 0.93 2/57 28129
Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28125/statm): 531 226 485 147 0 384 0
[pid=28125] vsize: 2124
Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 38859 0 0 0 103410 248 0 0 25 0 1 0 1855612436 160555008 38469 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28129/statm): 39198 38469 145 145 0 39053 0
[pid=28129] vsize: 156792
Current children cumulated CPU time (s) 1036.6
Current children cumulated vsize (Kb) 158916

[startup+1050.09 s]
Raw data (loadavg): 0.99 0.98 0.93 2/57 28129
Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28125/statm): 531 226 485 147 0 384 0
[pid=28125] vsize: 2124
Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 38859 0 0 0 104410 248 0 0 25 0 1 0 1855612436 160555008 38469 4294967295 134512640 135094434 3221224432 3221223088 134558187 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28129/statm): 39198 38469 145 145 0 39053 0
[pid=28129] vsize: 156792
Current children cumulated CPU time (s) 1046.6
Current children cumulated vsize (Kb) 158916

[startup+1060.09 s]
Raw data (loadavg): 0.99 0.98 0.93 2/57 28129
Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28125/statm): 531 226 485 147 0 384 0
[pid=28125] vsize: 2124
Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 38859 0 0 0 105410 248 0 0 25 0 1 0 1855612436 160555008 38469 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28129/statm): 39198 38469 145 145 0 39053 0
[pid=28129] vsize: 156792
Current children cumulated CPU time (s) 1056.6
Current children cumulated vsize (Kb) 158916

[startup+1070.09 s]
Raw data (loadavg): 0.99 0.98 0.93 2/57 28129
Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28125/statm): 531 226 485 147 0 384 0
[pid=28125] vsize: 2124
Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 38859 0 0 0 106410 248 0 0 25 0 1 0 1855612436 160555008 38469 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28129/statm): 39198 38469 145 145 0 39053 0
[pid=28129] vsize: 156792
Current children cumulated CPU time (s) 1066.6
Current children cumulated vsize (Kb) 158916

[startup+1080.09 s]
Raw data (loadavg): 0.99 0.98 0.93 2/57 28129
Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28125/statm): 531 226 485 147 0 384 0
[pid=28125] vsize: 2124
Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 38859 0 0 0 107410 248 0 0 25 0 1 0 1855612436 160555008 38469 4294967295 134512640 135094434 3221224432 3221223024 134556802 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28129/statm): 39198 38469 145 145 0 39053 0
[pid=28129] vsize: 156792
Current children cumulated CPU time (s) 1076.6
Current children cumulated vsize (Kb) 158916

[startup+1090.09 s]
Raw data (loadavg): 0.99 0.98 0.93 2/57 28129
Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28125/statm): 531 226 485 147 0 384 0
[pid=28125] vsize: 2124
Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 38859 0 0 0 108410 248 0 0 25 0 1 0 1855612436 160555008 38469 4294967295 134512640 135094434 3221224432 3221223024 134556817 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28129/statm): 39198 38469 145 145 0 39053 0
[pid=28129] vsize: 156792
Current children cumulated CPU time (s) 1086.6
Current children cumulated vsize (Kb) 158916

[startup+1100.09 s]
Raw data (loadavg): 0.99 0.98 0.93 2/57 28129
Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28125/statm): 531 226 485 147 0 384 0
[pid=28125] vsize: 2124
Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 38859 0 0 0 109411 248 0 0 25 0 1 0 1855612436 160555008 38469 4294967295 134512640 135094434 3221224432 3221223024 134557372 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28129/statm): 39198 38469 145 145 0 39053 0
[pid=28129] vsize: 156792
Current children cumulated CPU time (s) 1096.61
Current children cumulated vsize (Kb) 158916

[startup+1110.09 s]
Raw data (loadavg): 0.99 0.98 0.93 2/57 28129
Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28125/statm): 531 226 485 147 0 384 0
[pid=28125] vsize: 2124
Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 38859 0 0 0 110411 248 0 0 25 0 1 0 1855612436 160555008 38469 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28129/statm): 39198 38469 145 145 0 39053 0
[pid=28129] vsize: 156792
Current children cumulated CPU time (s) 1106.61
Current children cumulated vsize (Kb) 158916

[startup+1120.09 s]
Raw data (loadavg): 0.99 0.98 0.93 2/57 28129
Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28125/statm): 531 226 485 147 0 384 0
[pid=28125] vsize: 2124
Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 38859 0 0 0 111411 248 0 0 25 0 1 0 1855612436 160555008 38469 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28129/statm): 39198 38469 145 145 0 39053 0
[pid=28129] vsize: 156792
Current children cumulated CPU time (s) 1116.61
Current children cumulated vsize (Kb) 158916

[startup+1130.09 s]
Raw data (loadavg): 0.99 0.98 0.93 2/57 28129
Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28125/statm): 531 226 485 147 0 384 0
[pid=28125] vsize: 2124
Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 38859 0 0 0 112411 248 0 0 25 0 1 0 1855612436 160555008 38469 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28129/statm): 39198 38469 145 145 0 39053 0
[pid=28129] vsize: 156792
Current children cumulated CPU time (s) 1126.61
Current children cumulated vsize (Kb) 158916

[startup+1140.09 s]
Raw data (loadavg): 0.99 0.98 0.93 2/57 28129
Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28125/statm): 531 226 485 147 0 384 0
[pid=28125] vsize: 2124
Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 38859 0 0 0 113411 248 0 0 25 0 1 0 1855612436 160555008 38469 4294967295 134512640 135094434 3221224432 3221223088 134558225 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28129/statm): 39198 38469 145 145 0 39053 0
[pid=28129] vsize: 156792
Current children cumulated CPU time (s) 1136.61
Current children cumulated vsize (Kb) 158916

[startup+1150.1 s]
Raw data (loadavg): 0.99 0.98 0.93 2/57 28129
Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28125/statm): 531 226 485 147 0 384 0
[pid=28125] vsize: 2124
Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 38859 0 0 0 114410 249 0 0 25 0 1 0 1855612436 160555008 38469 4294967295 134512640 135094434 3221224432 3221223024 134557416 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28129/statm): 39198 38469 145 145 0 39053 0
[pid=28129] vsize: 156792
Current children cumulated CPU time (s) 1146.61
Current children cumulated vsize (Kb) 158916

[startup+1160.1 s]
Raw data (loadavg): 0.99 0.98 0.93 2/57 28129
Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28125/statm): 531 226 485 147 0 384 0
[pid=28125] vsize: 2124
Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 38859 0 0 0 115410 250 0 0 25 0 1 0 1855612436 160555008 38469 4294967295 134512640 135094434 3221224432 3221223024 134556806 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28129/statm): 39198 38469 145 145 0 39053 0
[pid=28129] vsize: 156792
Current children cumulated CPU time (s) 1156.62
Current children cumulated vsize (Kb) 158916

[startup+1170.1 s]
Raw data (loadavg): 0.99 0.98 0.93 2/57 28129
Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28125/statm): 531 226 485 147 0 384 0
[pid=28125] vsize: 2124
Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 38859 0 0 0 116410 250 0 0 25 0 1 0 1855612436 160555008 38469 4294967295 134512640 135094434 3221224432 3221223024 134557202 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28129/statm): 39198 38469 145 145 0 39053 0
[pid=28129] vsize: 156792
Current children cumulated CPU time (s) 1166.62
Current children cumulated vsize (Kb) 158916

[startup+1180.1 s]
Raw data (loadavg): 0.99 0.98 0.93 2/57 28129
Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28125/statm): 531 226 485 147 0 384 0
[pid=28125] vsize: 2124
Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 38859 0 0 0 117410 250 0 0 25 0 1 0 1855612436 160555008 38469 4294967295 134512640 135094434 3221224432 3221223024 134557416 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28129/statm): 39198 38469 145 145 0 39053 0
[pid=28129] vsize: 156792
Current children cumulated CPU time (s) 1176.62
Current children cumulated vsize (Kb) 158916

[startup+1190.1 s]
Raw data (loadavg): 0.99 0.98 0.93 2/57 28129
Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28125/statm): 531 226 485 147 0 384 0
[pid=28125] vsize: 2124
Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 38859 0 0 0 118410 250 0 0 25 0 1 0 1855612436 160555008 38469 4294967295 134512640 135094434 3221224432 3221223024 134556802 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28129/statm): 39198 38469 145 145 0 39053 0
[pid=28129] vsize: 156792
Current children cumulated CPU time (s) 1186.62
Current children cumulated vsize (Kb) 158916

[startup+1200.1 s]
Raw data (loadavg): 0.99 0.98 0.93 2/57 28129
Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28125/statm): 531 226 485 147 0 384 0
[pid=28125] vsize: 2124
Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 38859 0 0 0 119410 250 0 0 25 0 1 0 1855612436 160555008 38469 4294967295 134512640 135094434 3221224432 3221223024 134557020 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28129/statm): 39198 38469 145 145 0 39053 0
[pid=28129] vsize: 156792
Current children cumulated CPU time (s) 1196.62
Current children cumulated vsize (Kb) 158916

[startup+1210.1 s]
Raw data (loadavg): 0.99 0.98 0.93 2/57 28129
Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28125/statm): 531 226 485 147 0 384 0
[pid=28125] vsize: 2124
Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 38859 0 0 0 120410 251 0 0 25 0 1 0 1855612436 160555008 38469 4294967295 134512640 135094434 3221224432 3221223104 134556421 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28129/statm): 39198 38469 145 145 0 39053 0
[pid=28129] vsize: 156792
Current children cumulated CPU time (s) 1206.63
Current children cumulated vsize (Kb) 158916



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.1 s]
Raw data (loadavg): 0.99 0.98 0.93 2/57 28129
Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28125/statm): 531 226 485 147 0 384 0
[pid=28125] vsize: 2124
Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 38859 0 0 0 120410 251 0 0 25 0 1 0 1855612436 160555008 38469 4294967295 134512640 135094434 3221224432 3221223024 134556966 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28129/statm): 39198 38469 145 145 0 39053 0
[pid=28129] vsize: 156792
Current children cumulated CPU time (s) 1206.63
Current children cumulated vsize (Kb) 158916

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

Child status: 0
Real time (s): 1210.18
CPU time (s): 1206.69
CPU user time (s): 1204.11
CPU system time (s): 2.58461
CPU usage (%): 99.7121
Max. virtual memory (cumulated for all children) (Kb): 158916

Verifier Data

ERROR: no interpretation found !