Some explanations

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

General information on the benchmark

Namemps-v2-20-10/MIPLIB/miplib3/normalized-mps-v2-20-10-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.44
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 4527

Launcher Data

LAUNCH ON wulflinc2 THE 2005-09-19 18:02:18 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=2980 boxname=wulflinc2 idbench=636 idsolver=3 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  9d4ce12b138a2bef65a1f401ec9d1f01  /oldhome/oroussel/tmp/wulflinc2/normalized-mps-v2-20-10-l152lav.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc2/normalized-mps-v2-20-10-l152lav.opb
IDLAUNCH: 2980
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.191
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	: 2
cpu MHz		: 451.191
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:        857184 kB
Buffers:         39840 kB
Cached:         111168 kB
SwapCached:       1040 kB
Active:          64084 kB
Inactive:        89560 kB
HighTotal:      131008 kB
HighFree:        27300 kB
LowTotal:       903652 kB
LowFree:        829884 kB
SwapTotal:     2097136 kB
SwapFree:      2095568 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5700 kB
Slab:            18272 kB
Committed_AS:    72360 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-09-19 18:22:28 (client local time) WITH STATUS 0 IN 1206.72 SECONDS
stats: 2980 7 1206.72 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/28475/stat): 28475 (minisat+_script) R 28474 28475 6872 0 -1 0 19 0 0 0 0 0 0 0 22 0 1 0 1793685383 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 1 0 0
Raw data (/proc/28475/statm): 174 3 169 147 0 27 0
[pid=28475] 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=28476
New process pid=28477
New process pid=28478
execve syscall for /bin/sed executable
One traced child (pid=28477) 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=28478) exited with status: 0
One traced child (pid=28476) exited with status: 0
New process pid=28479
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc2/normalized-mps-v2-20-10-l152lav.opb

[startup+10.0036 s]
Raw data (loadavg): 0.87 0.94 0.79 2/57 28479
Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28475/statm): 531 226 485 147 0 384 0
[pid=28475] vsize: 2124
Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 4202 0 0 0 964 17 0 0 25 0 1 0 1793685388 18096128 3812 4294967295 134512640 135094434 3221224432 3221223044 134563046 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28479/statm): 4418 3812 145 145 0 4273 0
[pid=28479] vsize: 17672
Current children cumulated CPU time (s) 9.82
Current children cumulated vsize (Kb) 19796

[startup+20.0053 s]
Raw data (loadavg): 0.89 0.94 0.80 2/57 28479
Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28475/statm): 531 226 485 147 0 384 0
[pid=28475] vsize: 2124
Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 4576 0 0 0 1957 19 0 0 25 0 1 0 1793685388 19632128 4186 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28479/statm): 4793 4186 145 145 0 4648 0
[pid=28479] vsize: 19172
Current children cumulated CPU time (s) 19.77
Current children cumulated vsize (Kb) 21296

[startup+30.006 s]
Raw data (loadavg): 0.90 0.94 0.80 2/57 28479
Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28475/statm): 531 226 485 147 0 384 0
[pid=28475] vsize: 2124
Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 4727 0 0 0 2954 20 0 0 25 0 1 0 1793685388 20275200 4337 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28479/statm): 4950 4337 145 145 0 4805 0
[pid=28479] vsize: 19800
Current children cumulated CPU time (s) 29.75
Current children cumulated vsize (Kb) 21924

[startup+40.0067 s]
Raw data (loadavg): 0.92 0.94 0.80 2/57 28479
Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28475/statm): 531 226 485 147 0 384 0
[pid=28475] vsize: 2124
Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 4846 0 0 0 3952 21 0 0 25 0 1 0 1793685388 20750336 4456 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28479/statm): 5066 4456 145 145 0 4921 0
[pid=28479] vsize: 20264
Current children cumulated CPU time (s) 39.74
Current children cumulated vsize (Kb) 22388

[startup+50.0074 s]
Raw data (loadavg): 0.93 0.94 0.80 2/57 28479
Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28475/statm): 531 226 485 147 0 384 0
[pid=28475] vsize: 2124
Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 5077 0 0 0 4949 23 0 0 25 0 1 0 1793685388 21680128 4687 4294967295 134512640 135094434 3221224432 3221223024 134556809 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28479/statm): 5293 4687 145 145 0 5148 0
[pid=28479] vsize: 21172
Current children cumulated CPU time (s) 49.73
Current children cumulated vsize (Kb) 23296

[startup+60.0071 s]
Raw data (loadavg): 0.94 0.95 0.80 2/57 28479
Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28475/statm): 531 226 485 147 0 384 0
[pid=28475] vsize: 2124
Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 5461 0 0 0 5943 26 0 0 25 0 1 0 1793685388 23298048 5071 4294967295 134512640 135094434 3221224432 3221223024 134551702 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28479/statm): 5688 5071 145 145 0 5543 0
[pid=28479] vsize: 22752
Current children cumulated CPU time (s) 59.7
Current children cumulated vsize (Kb) 24876

[startup+70.0088 s]
Raw data (loadavg): 0.95 0.95 0.81 2/57 28479
Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28475/statm): 531 226 485 147 0 384 0
[pid=28475] vsize: 2124
Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 5830 0 0 0 6938 28 0 0 25 0 1 0 1793685388 24797184 5440 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28479/statm): 6054 5440 145 145 0 5909 0
[pid=28479] vsize: 24216
Current children cumulated CPU time (s) 69.67
Current children cumulated vsize (Kb) 26340

[startup+80.0095 s]
Raw data (loadavg): 0.96 0.95 0.81 2/57 28479
Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28475/statm): 531 226 485 147 0 384 0
[pid=28475] vsize: 2124
Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 6140 0 0 0 7932 30 0 0 25 0 1 0 1793685388 26050560 5750 4294967295 134512640 135094434 3221224432 3221223044 134563077 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28479/statm): 6360 5750 145 145 0 6215 0
[pid=28479] vsize: 25440
Current children cumulated CPU time (s) 79.63
Current children cumulated vsize (Kb) 27564

[startup+90.0092 s]
Raw data (loadavg): 0.96 0.95 0.81 2/57 28479
Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28475/statm): 531 226 485 147 0 384 0
[pid=28475] vsize: 2124
Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 6610 0 0 0 8924 34 0 0 25 0 1 0 1793685388 27963392 6220 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28479/statm): 6827 6220 145 145 0 6682 0
[pid=28479] vsize: 27308
Current children cumulated CPU time (s) 89.59
Current children cumulated vsize (Kb) 29432

[startup+100.01 s]
Raw data (loadavg): 0.97 0.95 0.81 2/57 28479
Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28475/statm): 531 226 485 147 0 384 0
[pid=28475] vsize: 2124
Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 7286 0 0 0 9914 39 0 0 25 0 1 0 1793685388 30724096 6896 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28479/statm): 7501 6896 145 145 0 7356 0
[pid=28479] vsize: 30004
Current children cumulated CPU time (s) 99.54
Current children cumulated vsize (Kb) 32128

[startup+110.011 s]
Raw data (loadavg): 0.97 0.95 0.81 2/57 28479
Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28475/statm): 531 226 485 147 0 384 0
[pid=28475] vsize: 2124
Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 7537 0 0 0 10911 40 0 0 25 0 1 0 1793685388 31875072 7147 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28479/statm): 7782 7147 145 145 0 7637 0
[pid=28479] vsize: 31128
Current children cumulated CPU time (s) 109.52
Current children cumulated vsize (Kb) 33252

[startup+120.011 s]
Raw data (loadavg): 0.98 0.95 0.82 2/57 28479
Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28475/statm): 531 226 485 147 0 384 0
[pid=28475] vsize: 2124
Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 8024 0 0 0 11904 43 0 0 25 0 1 0 1793685388 33857536 7634 4294967295 134512640 135094434 3221224432 3221223024 134556785 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28479/statm): 8266 7634 145 145 0 8121 0
[pid=28479] vsize: 33064
Current children cumulated CPU time (s) 119.48
Current children cumulated vsize (Kb) 35188

[startup+130.012 s]
Raw data (loadavg): 0.98 0.95 0.82 2/57 28479
Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28475/statm): 531 226 485 147 0 384 0
[pid=28475] vsize: 2124
Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 8421 0 0 0 12898 45 0 0 25 0 1 0 1793685388 35471360 8031 4294967295 134512640 135094434 3221224432 3221223024 134556941 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28479/statm): 8660 8031 145 145 0 8515 0
[pid=28479] vsize: 34640
Current children cumulated CPU time (s) 129.44
Current children cumulated vsize (Kb) 36764

[startup+140.012 s]
Raw data (loadavg): 0.98 0.95 0.82 2/57 28479
Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28475/statm): 531 226 485 147 0 384 0
[pid=28475] vsize: 2124
Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 8975 0 0 0 13890 48 0 0 25 0 1 0 1793685388 37728256 8585 4294967295 134512640 135094434 3221224432 3221223024 134557287 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28479/statm): 9211 8585 145 145 0 9066 0
[pid=28479] vsize: 36844
Current children cumulated CPU time (s) 139.39
Current children cumulated vsize (Kb) 38968

[startup+150.012 s]
Raw data (loadavg): 0.98 0.95 0.82 2/57 28479
Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28475/statm): 531 226 485 147 0 384 0
[pid=28475] vsize: 2124
Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 9562 0 0 0 14879 52 0 0 25 0 1 0 1793685388 40124416 9172 4294967295 134512640 135094434 3221224432 3221223024 134557016 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28479/statm): 9796 9172 145 145 0 9651 0
[pid=28479] vsize: 39184
Current children cumulated CPU time (s) 149.32
Current children cumulated vsize (Kb) 41308

[startup+160.013 s]
Raw data (loadavg): 0.99 0.96 0.82 2/57 28479
Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28475/statm): 531 226 485 147 0 384 0
[pid=28475] vsize: 2124
Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 10102 0 0 0 15870 56 0 0 25 0 1 0 1793685388 42328064 9712 4294967295 134512640 135094434 3221224432 3221223024 134557219 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28479/statm): 10334 9712 145 145 0 10189 0
[pid=28479] vsize: 41336
Current children cumulated CPU time (s) 159.27
Current children cumulated vsize (Kb) 43460

[startup+170.014 s]
Raw data (loadavg): 0.99 0.96 0.82 2/57 28479
Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28475/statm): 531 226 485 147 0 384 0
[pid=28475] vsize: 2124
Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 10607 0 0 0 16861 60 0 0 25 0 1 0 1793685388 44392448 10217 4294967295 134512640 135094434 3221224432 3221223024 134556870 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28479/statm): 10838 10217 145 145 0 10693 0
[pid=28479] vsize: 43352
Current children cumulated CPU time (s) 169.22
Current children cumulated vsize (Kb) 45476

[startup+180.015 s]
Raw data (loadavg): 0.99 0.96 0.82 2/57 28479
Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28475/statm): 531 226 485 147 0 384 0
[pid=28475] vsize: 2124
Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 11085 0 0 0 17851 64 0 0 25 0 1 0 1793685388 46346240 10695 4294967295 134512640 135094434 3221224432 3221223024 134557273 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28479/statm): 11315 10695 145 145 0 11170 0
[pid=28479] vsize: 45260
Current children cumulated CPU time (s) 179.16
Current children cumulated vsize (Kb) 47384

[startup+190.015 s]
Raw data (loadavg): 0.99 0.96 0.82 2/57 28479
Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28475/statm): 531 226 485 147 0 384 0
[pid=28475] vsize: 2124
Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 11545 0 0 0 18844 67 0 0 25 0 1 0 1793685388 48230400 11155 4294967295 134512640 135094434 3221224432 3221223024 134556812 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28479/statm): 11775 11155 145 145 0 11630 0
[pid=28479] vsize: 47100
Current children cumulated CPU time (s) 189.12
Current children cumulated vsize (Kb) 49224

[startup+200.016 s]
Raw data (loadavg): 0.99 0.96 0.82 2/57 28479
Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28475/statm): 531 226 485 147 0 384 0
[pid=28475] vsize: 2124
Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 11969 0 0 0 19837 70 0 0 25 0 1 0 1793685388 49967104 11579 4294967295 134512640 135094434 3221224432 3221223024 134557416 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28479/statm): 12199 11579 145 145 0 12054 0
[pid=28479] vsize: 48796
Current children cumulated CPU time (s) 199.08
Current children cumulated vsize (Kb) 50920

[startup+210.017 s]
Raw data (loadavg): 0.99 0.96 0.83 2/57 28479
Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28475/statm): 531 226 485 147 0 384 0
[pid=28475] vsize: 2124
Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 12325 0 0 0 20831 73 0 0 25 0 1 0 1793685388 51433472 11935 4294967295 134512640 135094434 3221224432 3221223024 134557416 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28479/statm): 12557 11935 145 145 0 12412 0
[pid=28479] vsize: 50228
Current children cumulated CPU time (s) 209.05
Current children cumulated vsize (Kb) 52352

[startup+220.018 s]
Raw data (loadavg): 0.99 0.96 0.83 2/57 28479
Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28475/statm): 531 226 485 147 0 384 0
[pid=28475] vsize: 2124
Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 12655 0 0 0 21825 75 0 0 25 0 1 0 1793685388 52781056 12265 4294967295 134512640 135094434 3221224432 3221223088 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28479/statm): 12886 12265 145 145 0 12741 0
[pid=28479] vsize: 51544
Current children cumulated CPU time (s) 219.01
Current children cumulated vsize (Kb) 53668

[startup+230.019 s]
Raw data (loadavg): 0.99 0.96 0.83 2/57 28479
Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28475/statm): 531 226 485 147 0 384 0
[pid=28475] vsize: 2124
Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 12971 0 0 0 22821 78 0 0 25 0 1 0 1793685388 54071296 12581 4294967295 134512640 135094434 3221224432 3221223024 134556806 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28479/statm): 13201 12581 145 145 0 13056 0
[pid=28479] vsize: 52804
Current children cumulated CPU time (s) 229
Current children cumulated vsize (Kb) 54928

[startup+240.019 s]
Raw data (loadavg): 0.99 0.96 0.83 2/57 28479
Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28475/statm): 531 226 485 147 0 384 0
[pid=28475] vsize: 2124
Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 13302 0 0 0 23815 80 0 0 25 0 1 0 1793685388 55418880 12912 4294967295 134512640 135094434 3221224432 3221223024 134557191 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28479/statm): 13530 12912 145 145 0 13385 0
[pid=28479] vsize: 54120
Current children cumulated CPU time (s) 238.96
Current children cumulated vsize (Kb) 56244

[startup+250.019 s]
Raw data (loadavg): 0.99 0.96 0.83 2/57 28479
Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28475/statm): 531 226 485 147 0 384 0
[pid=28475] vsize: 2124
Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 13678 0 0 0 24810 82 0 0 25 0 1 0 1793685388 56950784 13288 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28479/statm): 13904 13288 145 145 0 13759 0
[pid=28479] vsize: 55616
Current children cumulated CPU time (s) 248.93
Current children cumulated vsize (Kb) 57740

[startup+260.02 s]
Raw data (loadavg): 0.99 0.97 0.83 2/57 28479
Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28475/statm): 531 226 485 147 0 384 0
[pid=28475] vsize: 2124
Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 14150 0 0 0 25802 85 0 0 25 0 1 0 1793685388 58888192 13760 4294967295 134512640 135094434 3221224432 3221223088 134558011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28479/statm): 14377 13760 145 145 0 14232 0
[pid=28479] vsize: 57508
Current children cumulated CPU time (s) 258.88
Current children cumulated vsize (Kb) 59632

[startup+270.021 s]
Raw data (loadavg): 0.99 0.97 0.83 2/57 28479
Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28475/statm): 531 226 485 147 0 384 0
[pid=28475] vsize: 2124
Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 14574 0 0 0 26793 89 0 0 25 0 1 0 1793685388 60616704 14184 4294967295 134512640 135094434 3221224432 3221223088 134557872 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28479/statm): 14799 14184 145 145 0 14654 0
[pid=28479] vsize: 59196
Current children cumulated CPU time (s) 268.83
Current children cumulated vsize (Kb) 61320

[startup+280.022 s]
Raw data (loadavg): 0.99 0.97 0.83 2/57 28479
Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28475/statm): 531 226 485 147 0 384 0
[pid=28475] vsize: 2124
Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 15010 0 0 0 27784 92 0 0 25 0 1 0 1793685388 62390272 14620 4294967295 134512640 135094434 3221224432 3221223088 134558126 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28479/statm): 15232 14620 145 145 0 15087 0
[pid=28479] vsize: 60928
Current children cumulated CPU time (s) 278.77
Current children cumulated vsize (Kb) 63052

[startup+290.022 s]
Raw data (loadavg): 0.99 0.97 0.83 2/57 28479
Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28475/statm): 531 226 485 147 0 384 0
[pid=28475] vsize: 2124
Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 15476 0 0 0 28776 96 0 0 25 0 1 0 1793685388 64290816 15086 4294967295 134512640 135094434 3221224432 3221223024 134557141 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28479/statm): 15696 15086 145 145 0 15551 0
[pid=28479] vsize: 62784
Current children cumulated CPU time (s) 288.73
Current children cumulated vsize (Kb) 64908

[startup+300.023 s]
Raw data (loadavg): 0.99 0.97 0.83 2/57 28479
Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28475/statm): 531 226 485 147 0 384 0
[pid=28475] vsize: 2124
Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 15933 0 0 0 29768 99 0 0 25 0 1 0 1793685388 66416640 15543 4294967295 134512640 135094434 3221224432 3221223024 134556815 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28479/statm): 16215 15543 145 145 0 16070 0
[pid=28479] vsize: 64860
Current children cumulated CPU time (s) 298.68
Current children cumulated vsize (Kb) 66984

[startup+310.024 s]
Raw data (loadavg): 0.99 0.97 0.84 2/57 28479
Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28475/statm): 531 226 485 147 0 384 0
[pid=28475] vsize: 2124
Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 16361 0 0 0 30761 102 0 0 25 0 1 0 1793685388 68165632 15971 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28479/statm): 16642 15971 145 145 0 16497 0
[pid=28479] vsize: 66568
Current children cumulated CPU time (s) 308.64
Current children cumulated vsize (Kb) 68692

[startup+320.024 s]
Raw data (loadavg): 0.99 0.97 0.84 2/57 28479
Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28475/statm): 531 226 485 147 0 384 0
[pid=28475] vsize: 2124
Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 16675 0 0 0 31756 105 0 0 25 0 1 0 1793685388 69439488 16285 4294967295 134512640 135094434 3221224432 3221223024 134557037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28479/statm): 16953 16285 145 145 0 16808 0
[pid=28479] vsize: 67812
Current children cumulated CPU time (s) 318.62
Current children cumulated vsize (Kb) 69936

[startup+330.025 s]
Raw data (loadavg): 0.99 0.97 0.84 2/57 28479
Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28475/statm): 531 226 485 147 0 384 0
[pid=28475] vsize: 2124
Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 17087 0 0 0 32749 107 0 0 25 0 1 0 1793685388 71118848 16697 4294967295 134512640 135094434 3221224432 3221223088 134558004 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28479/statm): 17363 16697 145 145 0 17218 0
[pid=28479] vsize: 69452
Current children cumulated CPU time (s) 328.57
Current children cumulated vsize (Kb) 71576

[startup+340.025 s]
Raw data (loadavg): 0.99 0.97 0.84 2/57 28479
Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28475/statm): 531 226 485 147 0 384 0
[pid=28475] vsize: 2124
Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 17624 0 0 0 33741 111 0 0 25 0 1 0 1793685388 73310208 17234 4294967295 134512640 135094434 3221224432 3221223024 134557025 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28479/statm): 17898 17234 145 145 0 17753 0
[pid=28479] vsize: 71592
Current children cumulated CPU time (s) 338.53
Current children cumulated vsize (Kb) 73716

[startup+350.025 s]
Raw data (loadavg): 0.99 0.97 0.84 2/57 28479
Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28475/statm): 531 226 485 147 0 384 0
[pid=28475] vsize: 2124
Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 18085 0 0 0 34733 114 0 0 25 0 1 0 1793685388 75190272 17695 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28479/statm): 18357 17695 145 145 0 18212 0
[pid=28479] vsize: 73428
Current children cumulated CPU time (s) 348.48
Current children cumulated vsize (Kb) 75552

[startup+360.026 s]
Raw data (loadavg): 0.99 0.97 0.84 2/57 28479
Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28475/statm): 531 226 485 147 0 384 0
[pid=28475] vsize: 2124
Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 18595 0 0 0 35725 118 0 0 25 0 1 0 1793685388 77275136 18205 4294967295 134512640 135094434 3221224432 3221223072 134562104 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28479/statm): 18866 18205 145 145 0 18721 0
[pid=28479] vsize: 75464
Current children cumulated CPU time (s) 358.44
Current children cumulated vsize (Kb) 77588

[startup+370.027 s]
Raw data (loadavg): 0.99 0.97 0.84 2/57 28479
Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28475/statm): 531 226 485 147 0 384 0
[pid=28475] vsize: 2124
Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 19034 0 0 0 36717 120 0 0 25 0 1 0 1793685388 79065088 18644 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28479/statm): 19303 18644 145 145 0 19158 0
[pid=28479] vsize: 77212
Current children cumulated CPU time (s) 368.38
Current children cumulated vsize (Kb) 79336

[startup+380.028 s]
Raw data (loadavg): 0.99 0.97 0.84 2/57 28479
Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28475/statm): 531 226 485 147 0 384 0
[pid=28475] vsize: 2124
Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 19480 0 0 0 37709 124 0 0 25 0 1 0 1793685388 80883712 19090 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28479/statm): 19747 19090 145 145 0 19602 0
[pid=28479] vsize: 78988
Current children cumulated CPU time (s) 378.34
Current children cumulated vsize (Kb) 81112

[startup+390.028 s]
Raw data (loadavg): 0.99 0.97 0.84 2/57 28479
Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28475/statm): 531 226 485 147 0 384 0
[pid=28475] vsize: 2124
Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 19936 0 0 0 38702 127 0 0 25 0 1 0 1793685388 82747392 19546 4294967295 134512640 135094434 3221224432 3221223088 134558126 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28479/statm): 20202 19546 145 145 0 20057 0
[pid=28479] vsize: 80808
Current children cumulated CPU time (s) 388.3
Current children cumulated vsize (Kb) 82932

[startup+400.029 s]
Raw data (loadavg): 0.99 0.97 0.84 2/57 28479
Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28475/statm): 531 226 485 147 0 384 0
[pid=28475] vsize: 2124
Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 20404 0 0 0 39693 131 0 0 25 0 1 0 1793685388 84656128 20014 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28479/statm): 20668 20014 145 145 0 20523 0
[pid=28479] vsize: 82672
Current children cumulated CPU time (s) 398.25
Current children cumulated vsize (Kb) 84796

[startup+410.029 s]
Raw data (loadavg): 0.99 0.97 0.85 2/57 28479
Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28475/statm): 531 226 485 147 0 384 0
[pid=28475] vsize: 2124
Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 20780 0 0 0 40686 134 0 0 25 0 1 0 1793685388 86188032 20390 4294967295 134512640 135094434 3221224432 3221223092 134553480 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28479/statm): 21042 20390 145 145 0 20897 0
[pid=28479] vsize: 84168
Current children cumulated CPU time (s) 408.21
Current children cumulated vsize (Kb) 86292

[startup+420.03 s]
Raw data (loadavg): 0.99 0.97 0.85 2/57 28479
Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28475/statm): 531 226 485 147 0 384 0
[pid=28475] vsize: 2124
Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 21145 0 0 0 41679 137 0 0 25 0 1 0 1793685388 87674880 20755 4294967295 134512640 135094434 3221224432 3221223044 134563080 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28479/statm): 21405 20755 145 145 0 21260 0
[pid=28479] vsize: 85620
Current children cumulated CPU time (s) 418.17
Current children cumulated vsize (Kb) 87744

[startup+430.031 s]
Raw data (loadavg): 0.99 0.97 0.85 2/57 28479
Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28475/statm): 531 226 485 147 0 384 0
[pid=28475] vsize: 2124
Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 21564 0 0 0 42673 140 0 0 25 0 1 0 1793685388 89382912 21174 4294967295 134512640 135094434 3221224432 3221223024 134557028 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28479/statm): 21822 21174 145 145 0 21677 0
[pid=28479] vsize: 87288
Current children cumulated CPU time (s) 428.14
Current children cumulated vsize (Kb) 89412

[startup+440.031 s]
Raw data (loadavg): 0.99 0.97 0.85 2/57 28479
Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28475/statm): 531 226 485 147 0 384 0
[pid=28475] vsize: 2124
Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 22058 0 0 0 43663 143 0 0 25 0 1 0 1793685388 91402240 21668 4294967295 134512640 135094434 3221224432 3221223024 134556884 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28479/statm): 22315 21668 145 145 0 22170 0
[pid=28479] vsize: 89260
Current children cumulated CPU time (s) 438.07
Current children cumulated vsize (Kb) 91384

[startup+450.031 s]
Raw data (loadavg): 0.99 0.97 0.85 2/57 28479
Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28475/statm): 531 226 485 147 0 384 0
[pid=28475] vsize: 2124
Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 22600 0 0 0 44654 147 0 0 25 0 1 0 1793685388 93614080 22210 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28479/statm): 22855 22210 145 145 0 22710 0
[pid=28479] vsize: 91420
Current children cumulated CPU time (s) 448.02
Current children cumulated vsize (Kb) 93544

[startup+460.032 s]
Raw data (loadavg): 0.99 0.97 0.85 2/57 28479
Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28475/statm): 531 226 485 147 0 384 0
[pid=28475] vsize: 2124
Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 23127 0 0 0 45647 150 0 0 25 0 1 0 1793685388 95772672 22737 4294967295 134512640 135094434 3221224432 3221223024 134557273 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28479/statm): 23382 22737 145 145 0 23237 0
[pid=28479] vsize: 93528
Current children cumulated CPU time (s) 457.98
Current children cumulated vsize (Kb) 95652

[startup+470.033 s]
Raw data (loadavg): 0.99 0.97 0.85 2/57 28479
Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28475/statm): 531 226 485 147 0 384 0
[pid=28475] vsize: 2124
Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 23624 0 0 0 46641 153 0 0 25 0 1 0 1793685388 97808384 23234 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28479/statm): 23879 23234 145 145 0 23734 0
[pid=28479] vsize: 95516
Current children cumulated CPU time (s) 467.95
Current children cumulated vsize (Kb) 97640

[startup+480.034 s]
Raw data (loadavg): 0.99 0.97 0.85 2/57 28479
Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28475/statm): 531 226 485 147 0 384 0
[pid=28475] vsize: 2124
Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 23979 0 0 0 47635 155 0 0 25 0 1 0 1793685388 99258368 23589 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28479/statm): 24233 23589 145 145 0 24088 0
[pid=28479] vsize: 96932
Current children cumulated CPU time (s) 477.91
Current children cumulated vsize (Kb) 99056

[startup+490.034 s]
Raw data (loadavg): 0.99 0.97 0.85 2/57 28479
Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28475/statm): 531 226 485 147 0 384 0
[pid=28475] vsize: 2124
Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 24351 0 0 0 48627 158 0 0 25 0 1 0 1793685388 100773888 23961 4294967295 134512640 135094434 3221224432 3221223088 134558187 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28479/statm): 24603 23961 145 145 0 24458 0
[pid=28479] vsize: 98412
Current children cumulated CPU time (s) 487.86
Current children cumulated vsize (Kb) 100536

[startup+500.035 s]
Raw data (loadavg): 0.99 0.97 0.85 2/57 28479
Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28475/statm): 531 226 485 147 0 384 0
[pid=28475] vsize: 2124
Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 24654 0 0 0 49621 160 0 0 25 0 1 0 1793685388 102006784 24264 4294967295 134512640 135094434 3221224432 3221223024 134557202 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28479/statm): 24904 24264 145 145 0 24759 0
[pid=28479] vsize: 99616
Current children cumulated CPU time (s) 497.82
Current children cumulated vsize (Kb) 101740

[startup+510.036 s]
Raw data (loadavg): 0.99 0.97 0.85 2/57 28479
Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28475/statm): 531 226 485 147 0 384 0
[pid=28475] vsize: 2124
Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 25090 0 0 0 50614 164 0 0 25 0 1 0 1793685388 103784448 24700 4294967295 134512640 135094434 3221224432 3221223088 134558178 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28479/statm): 25338 24700 145 145 0 25193 0
[pid=28479] vsize: 101352
Current children cumulated CPU time (s) 507.79
Current children cumulated vsize (Kb) 103476

[startup+520.036 s]
Raw data (loadavg): 0.99 0.97 0.86 2/57 28479
Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28475/statm): 531 226 485 147 0 384 0
[pid=28475] vsize: 2124
Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 25581 0 0 0 51608 167 0 0 25 0 1 0 1793685388 105791488 25191 4294967295 134512640 135094434 3221224432 3221223024 134557219 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28479/statm): 25828 25191 145 145 0 25683 0
[pid=28479] vsize: 103312
Current children cumulated CPU time (s) 517.76
Current children cumulated vsize (Kb) 105436

[startup+530.037 s]
Raw data (loadavg): 0.99 0.97 0.86 2/57 28479
Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28475/statm): 531 226 485 147 0 384 0
[pid=28475] vsize: 2124
Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 26042 0 0 0 52601 169 0 0 25 0 1 0 1793685388 107675648 25652 4294967295 134512640 135094434 3221224432 3221223024 134557273 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28479/statm): 26288 25652 145 145 0 26143 0
[pid=28479] vsize: 105152
Current children cumulated CPU time (s) 527.71
Current children cumulated vsize (Kb) 107276

[startup+540.038 s]
Raw data (loadavg): 0.99 0.97 0.86 2/57 28479
Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28475/statm): 531 226 485 147 0 384 0
[pid=28475] vsize: 2124
Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 26469 0 0 0 53594 173 0 0 25 0 1 0 1793685388 109416448 26079 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28479/statm): 26713 26079 145 145 0 26568 0
[pid=28479] vsize: 106852
Current children cumulated CPU time (s) 537.68
Current children cumulated vsize (Kb) 108976

[startup+550.038 s]
Raw data (loadavg): 0.99 0.97 0.86 2/57 28479
Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28475/statm): 531 226 485 147 0 384 0
[pid=28475] vsize: 2124
Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 26914 0 0 0 54586 175 0 0 25 0 1 0 1793685388 111235072 26524 4294967295 134512640 135094434 3221224432 3221223024 134551757 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28479/statm): 27157 26524 145 145 0 27012 0
[pid=28479] vsize: 108628
Current children cumulated CPU time (s) 547.62
Current children cumulated vsize (Kb) 110752

[startup+560.038 s]
Raw data (loadavg): 0.99 0.97 0.86 2/57 28479
Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28475/statm): 531 226 485 147 0 384 0
[pid=28475] vsize: 2124
Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 27359 0 0 0 55579 178 0 0 25 0 1 0 1793685388 113053696 26969 4294967295 134512640 135094434 3221224432 3221223104 134556277 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28479/statm): 27601 26969 145 145 0 27456 0
[pid=28479] vsize: 110404
Current children cumulated CPU time (s) 557.58
Current children cumulated vsize (Kb) 112528

[startup+570.04 s]
Raw data (loadavg): 0.99 0.97 0.86 2/57 28479
Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28475/statm): 531 226 485 147 0 384 0
[pid=28475] vsize: 2124
Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 27771 0 0 0 56573 180 0 0 25 0 1 0 1793685388 114737152 27381 4294967295 134512640 135094434 3221224432 3221223024 134557219 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28479/statm): 28012 27381 145 145 0 27867 0
[pid=28479] vsize: 112048
Current children cumulated CPU time (s) 567.54
Current children cumulated vsize (Kb) 114172

[startup+580.041 s]
Raw data (loadavg): 0.99 0.97 0.86 2/57 28479
Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28475/statm): 531 226 485 147 0 384 0
[pid=28475] vsize: 2124
Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 28166 0 0 0 57568 182 0 0 25 0 1 0 1793685388 116350976 27776 4294967295 134512640 135094434 3221224432 3221223024 134557185 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28479/statm): 28406 27776 145 145 0 28261 0
[pid=28479] vsize: 113624
Current children cumulated CPU time (s) 577.51
Current children cumulated vsize (Kb) 115748

[startup+590.04 s]
Raw data (loadavg): 0.99 0.97 0.86 2/57 28479
Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28475/statm): 531 226 485 147 0 384 0
[pid=28475] vsize: 2124
Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) T 28475 28475 6872 0 -1 0 28555 0 0 0 58563 184 0 0 25 0 1 0 1793685388 117940224 28165 4294967295 134512640 135094434 3221224432 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/28479/statm): 28794 28165 145 145 0 28649 0
[pid=28479] vsize: 115176
Current children cumulated CPU time (s) 587.48
Current children cumulated vsize (Kb) 117300

[startup+600.041 s]
Raw data (loadavg): 0.99 0.97 0.86 2/57 28479
Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28475/statm): 531 226 485 147 0 384 0
[pid=28475] vsize: 2124
Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 28899 0 0 0 59559 185 0 0 25 0 1 0 1793685388 119341056 28509 4294967295 134512640 135094434 3221224432 3221223104 134555560 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28479/statm): 29136 28509 145 145 0 28991 0
[pid=28479] vsize: 116544
Current children cumulated CPU time (s) 597.45
Current children cumulated vsize (Kb) 118668

[startup+610.042 s]
Raw data (loadavg): 0.99 0.97 0.86 2/57 28479
Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28475/statm): 531 226 485 147 0 384 0
[pid=28475] vsize: 2124
Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 29410 0 0 0 60552 187 0 0 25 0 1 0 1793685388 121438208 29020 4294967295 134512640 135094434 3221224432 3221223024 134557219 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28479/statm): 29648 29020 145 145 0 29503 0
[pid=28479] vsize: 118592
Current children cumulated CPU time (s) 607.4
Current children cumulated vsize (Kb) 120716

[startup+620.042 s]
Raw data (loadavg): 0.99 0.97 0.87 2/57 28479
Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28475/statm): 531 226 485 147 0 384 0
[pid=28475] vsize: 2124
Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 29922 0 0 0 61546 189 0 0 25 0 1 0 1793685388 123531264 29532 4294967295 134512640 135094434 3221224432 3221223024 134556834 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28479/statm): 30159 29532 145 145 0 30014 0
[pid=28479] vsize: 120636
Current children cumulated CPU time (s) 617.36
Current children cumulated vsize (Kb) 122760

[startup+630.043 s]
Raw data (loadavg): 0.99 0.97 0.87 2/57 28479
Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28475/statm): 531 226 485 147 0 384 0
[pid=28475] vsize: 2124
Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 30616 0 0 0 62534 195 0 0 25 0 1 0 1793685388 126361600 30226 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28479/statm): 30850 30226 145 145 0 30705 0
[pid=28479] vsize: 123400
Current children cumulated CPU time (s) 627.3
Current children cumulated vsize (Kb) 125524

[startup+640.044 s]
Raw data (loadavg): 0.99 0.97 0.87 2/57 28479
Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28475/statm): 531 226 485 147 0 384 0
[pid=28475] vsize: 2124
Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 31234 0 0 0 63524 199 0 0 25 0 1 0 1793685388 128888832 30844 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28479/statm): 31467 30844 145 145 0 31322 0
[pid=28479] vsize: 125868
Current children cumulated CPU time (s) 637.24
Current children cumulated vsize (Kb) 127992

[startup+650.044 s]
Raw data (loadavg): 0.99 0.97 0.87 2/57 28479
Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28475/statm): 531 226 485 147 0 384 0
[pid=28475] vsize: 2124
Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 31622 0 0 0 64518 201 0 0 25 0 1 0 1793685388 130469888 31232 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28479/statm): 31853 31232 145 145 0 31708 0
[pid=28479] vsize: 127412
Current children cumulated CPU time (s) 647.2
Current children cumulated vsize (Kb) 129536

[startup+660.045 s]
Raw data (loadavg): 0.99 0.97 0.87 2/57 28479
Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28475/statm): 531 226 485 147 0 384 0
[pid=28475] vsize: 2124
Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 32181 0 0 0 65510 204 0 0 25 0 1 0 1793685388 132751360 31791 4294967295 134512640 135094434 3221224432 3221223024 134557310 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28479/statm): 32410 31791 145 145 0 32265 0
[pid=28479] vsize: 129640
Current children cumulated CPU time (s) 657.15
Current children cumulated vsize (Kb) 131764

[startup+670.046 s]
Raw data (loadavg): 0.99 0.97 0.87 2/57 28479
Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28475/statm): 531 226 485 147 0 384 0
[pid=28475] vsize: 2124
Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 32691 0 0 0 66500 208 0 0 25 0 1 0 1793685388 134836224 32301 4294967295 134512640 135094434 3221224432 3221223024 134557232 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28479/statm): 32919 32301 145 145 0 32774 0
[pid=28479] vsize: 131676
Current children cumulated CPU time (s) 667.09
Current children cumulated vsize (Kb) 133800

[startup+680.047 s]
Raw data (loadavg): 0.99 0.97 0.87 2/57 28479
Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28475/statm): 531 226 485 147 0 384 0
[pid=28475] vsize: 2124
Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 33028 0 0 0 67495 210 0 0 25 0 1 0 1793685388 136212480 32638 4294967295 134512640 135094434 3221224432 3221223024 134556894 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28479/statm): 33255 32638 145 145 0 33110 0
[pid=28479] vsize: 133020
Current children cumulated CPU time (s) 677.06
Current children cumulated vsize (Kb) 135144

[startup+690.047 s]
Raw data (loadavg): 0.99 0.97 0.87 2/57 28479
Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28475/statm): 531 226 485 147 0 384 0
[pid=28475] vsize: 2124
Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 33334 0 0 0 68490 212 0 0 25 0 1 0 1793685388 137461760 32944 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28479/statm): 33560 32944 145 145 0 33415 0
[pid=28479] vsize: 134240
Current children cumulated CPU time (s) 687.03
Current children cumulated vsize (Kb) 136364

[startup+700.049 s]
Raw data (loadavg): 0.99 0.97 0.87 2/57 28479
Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28475/statm): 531 226 485 147 0 384 0
[pid=28475] vsize: 2124
Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 33528 0 0 0 69486 214 0 0 25 0 1 0 1793685388 138772480 33138 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28479/statm): 33880 33138 145 145 0 33735 0
[pid=28479] vsize: 135520
Current children cumulated CPU time (s) 697.01
Current children cumulated vsize (Kb) 137644

[startup+710.05 s]
Raw data (loadavg): 0.99 0.97 0.87 2/57 28479
Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28475/statm): 531 226 485 147 0 384 0
[pid=28475] vsize: 2124
Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 33821 0 0 0 70481 216 0 0 25 0 1 0 1793685388 139968512 33431 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28479/statm): 34172 33431 145 145 0 34027 0
[pid=28479] vsize: 136688
Current children cumulated CPU time (s) 706.98
Current children cumulated vsize (Kb) 138812

[startup+720.05 s]
Raw data (loadavg): 0.99 0.97 0.88 2/57 28479
Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28475/statm): 531 226 485 147 0 384 0
[pid=28475] vsize: 2124
Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 34368 0 0 0 71473 219 0 0 25 0 1 0 1793685388 142200832 33978 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28479/statm): 34717 33978 145 145 0 34572 0
[pid=28479] vsize: 138868
Current children cumulated CPU time (s) 716.93
Current children cumulated vsize (Kb) 140992

[startup+730.051 s]
Raw data (loadavg): 0.99 0.97 0.88 2/57 28479
Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28475/statm): 531 226 485 147 0 384 0
[pid=28475] vsize: 2124
Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 34975 0 0 0 72463 222 0 0 25 0 1 0 1793685388 144683008 34585 4294967295 134512640 135094434 3221224432 3221223104 134555815 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28479/statm): 35323 34585 145 145 0 35178 0
[pid=28479] vsize: 141292
Current children cumulated CPU time (s) 726.86
Current children cumulated vsize (Kb) 143416

[startup+740.052 s]
Raw data (loadavg): 0.99 0.97 0.88 2/57 28479
Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28475/statm): 531 226 485 147 0 384 0
[pid=28475] vsize: 2124
Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 35509 0 0 0 73455 225 0 0 25 0 1 0 1793685388 146866176 35119 4294967295 134512640 135094434 3221224432 3221223024 134557372 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28479/statm): 35856 35119 145 145 0 35711 0
[pid=28479] vsize: 143424
Current children cumulated CPU time (s) 736.81
Current children cumulated vsize (Kb) 145548

[startup+750.053 s]
Raw data (loadavg): 0.99 0.97 0.88 2/57 28479
Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28475/statm): 531 226 485 147 0 384 0
[pid=28475] vsize: 2124
Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 35983 0 0 0 74449 228 0 0 25 0 1 0 1793685388 148803584 35593 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28479/statm): 36329 35593 145 145 0 36184 0
[pid=28479] vsize: 145316
Current children cumulated CPU time (s) 746.78
Current children cumulated vsize (Kb) 147440

[startup+760.053 s]
Raw data (loadavg): 0.99 0.97 0.88 2/57 28479
Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28475/statm): 531 226 485 147 0 384 0
[pid=28475] vsize: 2124
Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 36464 0 0 0 75443 231 0 0 25 0 1 0 1793685388 150769664 36074 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28479/statm): 36809 36074 145 145 0 36664 0
[pid=28479] vsize: 147236
Current children cumulated CPU time (s) 756.75
Current children cumulated vsize (Kb) 149360

[startup+770.054 s]
Raw data (loadavg): 0.99 0.97 0.88 2/57 28479
Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28475/statm): 531 226 485 147 0 384 0
[pid=28475] vsize: 2124
Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 36923 0 0 0 76434 235 0 0 25 0 1 0 1793685388 152645632 36533 4294967295 134512640 135094434 3221224432 3221223024 134557248 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28479/statm): 37267 36533 145 145 0 37122 0
[pid=28479] vsize: 149068
Current children cumulated CPU time (s) 766.7
Current children cumulated vsize (Kb) 151192

[startup+780.055 s]
Raw data (loadavg): 0.99 0.97 0.88 2/57 28479
Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28475/statm): 531 226 485 147 0 384 0
[pid=28475] vsize: 2124
Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 37324 0 0 0 77428 237 0 0 25 0 1 0 1793685388 154284032 36934 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28479/statm): 37667 36934 145 145 0 37522 0
[pid=28479] vsize: 150668
Current children cumulated CPU time (s) 776.66
Current children cumulated vsize (Kb) 152792

[startup+790.055 s]
Raw data (loadavg): 0.99 0.97 0.88 2/57 28479
Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28475/statm): 531 226 485 147 0 384 0
[pid=28475] vsize: 2124
Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 37666 0 0 0 78421 241 0 0 25 0 1 0 1793685388 155680768 37276 4294967295 134512640 135094434 3221224432 3221223024 134556999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28479/statm): 38008 37276 145 145 0 37863 0
[pid=28479] vsize: 152032
Current children cumulated CPU time (s) 786.63
Current children cumulated vsize (Kb) 154156

[startup+800.056 s]
Raw data (loadavg): 0.99 0.97 0.88 2/57 28479
Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28475/statm): 531 226 485 147 0 384 0
[pid=28475] vsize: 2124
Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 38074 0 0 0 79416 243 0 0 25 0 1 0 1793685388 157351936 37684 4294967295 134512640 135094434 3221224432 3221223024 134556802 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28479/statm): 38416 37684 145 145 0 38271 0
[pid=28479] vsize: 153664
Current children cumulated CPU time (s) 796.6
Current children cumulated vsize (Kb) 155788

[startup+810.058 s]
Raw data (loadavg): 0.99 0.97 0.88 2/57 28479
Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28475/statm): 531 226 485 147 0 384 0
[pid=28475] vsize: 2124
Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 38485 0 0 0 80411 245 0 0 25 0 1 0 1793685388 159031296 38095 4294967295 134512640 135094434 3221224432 3221223056 134562051 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28479/statm): 38826 38095 145 145 0 38681 0
[pid=28479] vsize: 155304
Current children cumulated CPU time (s) 806.57
Current children cumulated vsize (Kb) 157428

[startup+820.058 s]
Raw data (loadavg): 0.99 0.97 0.89 2/57 28479
Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28475/statm): 531 226 485 147 0 384 0
[pid=28475] vsize: 2124
Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 38754 0 0 0 81407 248 0 0 25 0 1 0 1793685388 160129024 38364 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28479/statm): 39094 38364 145 145 0 38949 0
[pid=28479] vsize: 156376
Current children cumulated CPU time (s) 816.56
Current children cumulated vsize (Kb) 158500

[startup+830.059 s]
Raw data (loadavg): 0.99 0.97 0.89 2/57 28479
Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28475/statm): 531 226 485 147 0 384 0
[pid=28475] vsize: 2124
Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 38859 0 0 0 82407 248 0 0 25 0 1 0 1793685388 160555008 38469 4294967295 134512640 135094434 3221224432 3221223024 134556864 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28479/statm): 39198 38469 145 145 0 39053 0
[pid=28479] vsize: 156792
Current children cumulated CPU time (s) 826.56
Current children cumulated vsize (Kb) 158916

[startup+840.06 s]
Raw data (loadavg): 0.99 0.97 0.89 2/57 28479
Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28475/statm): 531 226 485 147 0 384 0
[pid=28475] vsize: 2124
Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 38859 0 0 0 83407 248 0 0 25 0 1 0 1793685388 160555008 38469 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28479/statm): 39198 38469 145 145 0 39053 0
[pid=28479] vsize: 156792
Current children cumulated CPU time (s) 836.56
Current children cumulated vsize (Kb) 158916

[startup+850.061 s]
Raw data (loadavg): 0.99 0.97 0.89 2/57 28479
Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28475/statm): 531 226 485 147 0 384 0
[pid=28475] vsize: 2124
Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 38859 0 0 0 84407 248 0 0 25 0 1 0 1793685388 160555008 38469 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28479/statm): 39198 38469 145 145 0 39053 0
[pid=28479] vsize: 156792
Current children cumulated CPU time (s) 846.56
Current children cumulated vsize (Kb) 158916

[startup+860.06 s]
Raw data (loadavg): 0.99 0.97 0.89 2/57 28479
Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28475/statm): 531 226 485 147 0 384 0
[pid=28475] vsize: 2124
Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 38859 0 0 0 85407 248 0 0 25 0 1 0 1793685388 160555008 38469 4294967295 134512640 135094434 3221224432 3221223056 134557714 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28479/statm): 39198 38469 145 145 0 39053 0
[pid=28479] vsize: 156792
Current children cumulated CPU time (s) 856.56
Current children cumulated vsize (Kb) 158916

[startup+870.062 s]
Raw data (loadavg): 0.99 0.97 0.89 2/57 28479
Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28475/statm): 531 226 485 147 0 384 0
[pid=28475] vsize: 2124
Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 38859 0 0 0 86408 248 0 0 25 0 1 0 1793685388 160555008 38469 4294967295 134512640 135094434 3221224432 3221223024 134557028 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28479/statm): 39198 38469 145 145 0 39053 0
[pid=28479] vsize: 156792
Current children cumulated CPU time (s) 866.57
Current children cumulated vsize (Kb) 158916

[startup+880.063 s]
Raw data (loadavg): 0.99 0.97 0.89 2/57 28479
Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28475/statm): 531 226 485 147 0 384 0
[pid=28475] vsize: 2124
Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 38859 0 0 0 87408 248 0 0 25 0 1 0 1793685388 160555008 38469 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28479/statm): 39198 38469 145 145 0 39053 0
[pid=28479] vsize: 156792
Current children cumulated CPU time (s) 876.57
Current children cumulated vsize (Kb) 158916

[startup+890.062 s]
Raw data (loadavg): 0.99 0.97 0.89 2/57 28479
Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28475/statm): 531 226 485 147 0 384 0
[pid=28475] vsize: 2124
Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 38859 0 0 0 88408 248 0 0 25 0 1 0 1793685388 160555008 38469 4294967295 134512640 135094434 3221224432 3221223088 134558187 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28479/statm): 39198 38469 145 145 0 39053 0
[pid=28479] vsize: 156792
Current children cumulated CPU time (s) 886.57
Current children cumulated vsize (Kb) 158916

[startup+900.064 s]
Raw data (loadavg): 0.99 0.97 0.89 2/57 28479
Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28475/statm): 531 226 485 147 0 384 0
[pid=28475] vsize: 2124
Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 38859 0 0 0 89408 248 0 0 25 0 1 0 1793685388 160555008 38469 4294967295 134512640 135094434 3221224432 3221223088 134557937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28479/statm): 39198 38469 145 145 0 39053 0
[pid=28479] vsize: 156792
Current children cumulated CPU time (s) 896.57
Current children cumulated vsize (Kb) 158916

[startup+910.065 s]
Raw data (loadavg): 0.99 0.97 0.89 2/57 28479
Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28475/statm): 531 226 485 147 0 384 0
[pid=28475] vsize: 2124
Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 38859 0 0 0 90408 248 0 0 25 0 1 0 1793685388 160555008 38469 4294967295 134512640 135094434 3221224432 3221223024 134557302 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28479/statm): 39198 38469 145 145 0 39053 0
[pid=28479] vsize: 156792
Current children cumulated CPU time (s) 906.57
Current children cumulated vsize (Kb) 158916

[startup+920.065 s]
Raw data (loadavg): 0.99 0.97 0.89 2/57 28479
Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28475/statm): 531 226 485 147 0 384 0
[pid=28475] vsize: 2124
Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 38859 0 0 0 91409 248 0 0 25 0 1 0 1793685388 160555008 38469 4294967295 134512640 135094434 3221224432 3221223088 134557900 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28479/statm): 39198 38469 145 145 0 39053 0
[pid=28479] vsize: 156792
Current children cumulated CPU time (s) 916.58
Current children cumulated vsize (Kb) 158916

[startup+930.067 s]
Raw data (loadavg): 0.99 0.97 0.90 2/57 28479
Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28475/statm): 531 226 485 147 0 384 0
[pid=28475] vsize: 2124
Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 38859 0 0 0 92409 248 0 0 25 0 1 0 1793685388 160555008 38469 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28479/statm): 39198 38469 145 145 0 39053 0
[pid=28479] vsize: 156792
Current children cumulated CPU time (s) 926.58
Current children cumulated vsize (Kb) 158916

[startup+940.068 s]
Raw data (loadavg): 0.99 0.97 0.90 2/57 28479
Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28475/statm): 531 226 485 147 0 384 0
[pid=28475] vsize: 2124
Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 38859 0 0 0 93409 248 0 0 25 0 1 0 1793685388 160555008 38469 4294967295 134512640 135094434 3221224432 3221223024 134557152 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28479/statm): 39198 38469 145 145 0 39053 0
[pid=28479] vsize: 156792
Current children cumulated CPU time (s) 936.58
Current children cumulated vsize (Kb) 158916

[startup+950.068 s]
Raw data (loadavg): 0.99 0.97 0.90 2/57 28479
Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28475/statm): 531 226 485 147 0 384 0
[pid=28475] vsize: 2124
Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 38859 0 0 0 94410 248 0 0 25 0 1 0 1793685388 160555008 38469 4294967295 134512640 135094434 3221224432 3221223024 134556802 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28479/statm): 39198 38469 145 145 0 39053 0
[pid=28479] vsize: 156792
Current children cumulated CPU time (s) 946.59
Current children cumulated vsize (Kb) 158916

[startup+960.069 s]
Raw data (loadavg): 0.99 0.97 0.90 2/57 28479
Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28475/statm): 531 226 485 147 0 384 0
[pid=28475] vsize: 2124
Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 38859 0 0 0 95410 248 0 0 25 0 1 0 1793685388 160555008 38469 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28479/statm): 39198 38469 145 145 0 39053 0
[pid=28479] vsize: 156792
Current children cumulated CPU time (s) 956.59
Current children cumulated vsize (Kb) 158916

[startup+970.07 s]
Raw data (loadavg): 0.99 0.97 0.90 2/57 28479
Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28475/statm): 531 226 485 147 0 384 0
[pid=28475] vsize: 2124
Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 38859 0 0 0 96410 248 0 0 25 0 1 0 1793685388 160555008 38469 4294967295 134512640 135094434 3221224432 3221223024 134557219 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28479/statm): 39198 38469 145 145 0 39053 0
[pid=28479] vsize: 156792
Current children cumulated CPU time (s) 966.59
Current children cumulated vsize (Kb) 158916

[startup+980.071 s]
Raw data (loadavg): 0.99 0.97 0.90 2/57 28479
Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28475/statm): 531 226 485 147 0 384 0
[pid=28475] vsize: 2124
Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 38859 0 0 0 97410 248 0 0 25 0 1 0 1793685388 160555008 38469 4294967295 134512640 135094434 3221224432 3221223024 134557182 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28479/statm): 39198 38469 145 145 0 39053 0
[pid=28479] vsize: 156792
Current children cumulated CPU time (s) 976.59
Current children cumulated vsize (Kb) 158916

[startup+990.071 s]
Raw data (loadavg): 0.99 0.97 0.90 2/57 28479
Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28475/statm): 531 226 485 147 0 384 0
[pid=28475] vsize: 2124
Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 38859 0 0 0 98411 248 0 0 25 0 1 0 1793685388 160555008 38469 4294967295 134512640 135094434 3221224432 3221223024 134556978 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28479/statm): 39198 38469 145 145 0 39053 0
[pid=28479] vsize: 156792
Current children cumulated CPU time (s) 986.6
Current children cumulated vsize (Kb) 158916

[startup+1000.07 s]
Raw data (loadavg): 0.99 0.97 0.90 2/57 28479
Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28475/statm): 531 226 485 147 0 384 0
[pid=28475] vsize: 2124
Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 38859 0 0 0 99411 248 0 0 25 0 1 0 1793685388 160555008 38469 4294967295 134512640 135094434 3221224432 3221223024 134557025 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28479/statm): 39198 38469 145 145 0 39053 0
[pid=28479] vsize: 156792
Current children cumulated CPU time (s) 996.6
Current children cumulated vsize (Kb) 158916

[startup+1010.07 s]
Raw data (loadavg): 0.99 0.97 0.90 2/57 28479
Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28475/statm): 531 226 485 147 0 384 0
[pid=28475] vsize: 2124
Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 38859 0 0 0 100411 248 0 0 25 0 1 0 1793685388 160555008 38469 4294967295 134512640 135094434 3221224432 3221223092 134553536 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28479/statm): 39198 38469 145 145 0 39053 0
[pid=28479] vsize: 156792
Current children cumulated CPU time (s) 1006.6
Current children cumulated vsize (Kb) 158916

[startup+1020.07 s]
Raw data (loadavg): 0.99 0.97 0.90 2/57 28479
Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28475/statm): 531 226 485 147 0 384 0
[pid=28475] vsize: 2124
Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 38859 0 0 0 101411 248 0 0 25 0 1 0 1793685388 160555008 38469 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28479/statm): 39198 38469 145 145 0 39053 0
[pid=28479] vsize: 156792
Current children cumulated CPU time (s) 1016.6
Current children cumulated vsize (Kb) 158916

[startup+1030.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28479
Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28475/statm): 531 226 485 147 0 384 0
[pid=28475] vsize: 2124
Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 38859 0 0 0 102412 248 0 0 25 0 1 0 1793685388 160555008 38469 4294967295 134512640 135094434 3221224432 3221223024 134557002 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28479/statm): 39198 38469 145 145 0 39053 0
[pid=28479] vsize: 156792
Current children cumulated CPU time (s) 1026.61
Current children cumulated vsize (Kb) 158916

[startup+1040.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28479
Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28475/statm): 531 226 485 147 0 384 0
[pid=28475] vsize: 2124
Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 38859 0 0 0 103412 249 0 0 25 0 1 0 1793685388 160555008 38469 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28479/statm): 39198 38469 145 145 0 39053 0
[pid=28479] vsize: 156792
Current children cumulated CPU time (s) 1036.62
Current children cumulated vsize (Kb) 158916

[startup+1050.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28479
Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28475/statm): 531 226 485 147 0 384 0
[pid=28475] vsize: 2124
Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 38859 0 0 0 104411 249 0 0 25 0 1 0 1793685388 160555008 38469 4294967295 134512640 135094434 3221224432 3221223104 134556244 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28479/statm): 39198 38469 145 145 0 39053 0
[pid=28479] vsize: 156792
Current children cumulated CPU time (s) 1046.61
Current children cumulated vsize (Kb) 158916

[startup+1060.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28479
Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28475/statm): 531 226 485 147 0 384 0
[pid=28475] vsize: 2124
Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 38859 0 0 0 105411 249 0 0 25 0 1 0 1793685388 160555008 38469 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28479/statm): 39198 38469 145 145 0 39053 0
[pid=28479] vsize: 156792
Current children cumulated CPU time (s) 1056.61
Current children cumulated vsize (Kb) 158916

[startup+1070.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28479
Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28475/statm): 531 226 485 147 0 384 0
[pid=28475] vsize: 2124
Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 38859 0 0 0 106412 249 0 0 25 0 1 0 1793685388 160555008 38469 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28479/statm): 39198 38469 145 145 0 39053 0
[pid=28479] vsize: 156792
Current children cumulated CPU time (s) 1066.62
Current children cumulated vsize (Kb) 158916

[startup+1080.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28479
Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28475/statm): 531 226 485 147 0 384 0
[pid=28475] vsize: 2124
Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 38859 0 0 0 107412 249 0 0 25 0 1 0 1793685388 160555008 38469 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28479/statm): 39198 38469 145 145 0 39053 0
[pid=28479] vsize: 156792
Current children cumulated CPU time (s) 1076.62
Current children cumulated vsize (Kb) 158916

[startup+1090.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28479
Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28475/statm): 531 226 485 147 0 384 0
[pid=28475] vsize: 2124
Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 38859 0 0 0 108412 249 0 0 25 0 1 0 1793685388 160555008 38469 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28479/statm): 39198 38469 145 145 0 39053 0
[pid=28479] vsize: 156792
Current children cumulated CPU time (s) 1086.62
Current children cumulated vsize (Kb) 158916

[startup+1100.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28479
Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28475/statm): 531 226 485 147 0 384 0
[pid=28475] vsize: 2124
Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 38859 0 0 0 109412 249 0 0 25 0 1 0 1793685388 160555008 38469 4294967295 134512640 135094434 3221224432 3221223024 134557297 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28479/statm): 39198 38469 145 145 0 39053 0
[pid=28479] vsize: 156792
Current children cumulated CPU time (s) 1096.62
Current children cumulated vsize (Kb) 158916

[startup+1110.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28479
Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28475/statm): 531 226 485 147 0 384 0
[pid=28475] vsize: 2124
Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 38859 0 0 0 110413 249 0 0 25 0 1 0 1793685388 160555008 38469 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28479/statm): 39198 38469 145 145 0 39053 0
[pid=28479] vsize: 156792
Current children cumulated CPU time (s) 1106.63
Current children cumulated vsize (Kb) 158916

[startup+1120.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28479
Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28475/statm): 531 226 485 147 0 384 0
[pid=28475] vsize: 2124
Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 38859 0 0 0 111413 249 0 0 25 0 1 0 1793685388 160555008 38469 4294967295 134512640 135094434 3221224432 3221223024 134556785 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28479/statm): 39198 38469 145 145 0 39053 0
[pid=28479] vsize: 156792
Current children cumulated CPU time (s) 1116.63
Current children cumulated vsize (Kb) 158916

[startup+1130.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28479
Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28475/statm): 531 226 485 147 0 384 0
[pid=28475] vsize: 2124
Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 38859 0 0 0 112413 249 0 0 25 0 1 0 1793685388 160555008 38469 4294967295 134512640 135094434 3221224432 3221223024 134556817 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28479/statm): 39198 38469 145 145 0 39053 0
[pid=28479] vsize: 156792
Current children cumulated CPU time (s) 1126.63
Current children cumulated vsize (Kb) 158916

[startup+1140.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28479
Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28475/statm): 531 226 485 147 0 384 0
[pid=28475] vsize: 2124
Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 38859 0 0 0 113413 249 0 0 25 0 1 0 1793685388 160555008 38469 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28479/statm): 39198 38469 145 145 0 39053 0
[pid=28479] vsize: 156792
Current children cumulated CPU time (s) 1136.63
Current children cumulated vsize (Kb) 158916

[startup+1150.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28479
Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28475/statm): 531 226 485 147 0 384 0
[pid=28475] vsize: 2124
Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 38859 0 0 0 114414 249 0 0 25 0 1 0 1793685388 160555008 38469 4294967295 134512640 135094434 3221224432 3221223024 134557230 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28479/statm): 39198 38469 145 145 0 39053 0
[pid=28479] vsize: 156792
Current children cumulated CPU time (s) 1146.64
Current children cumulated vsize (Kb) 158916

[startup+1160.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28479
Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28475/statm): 531 226 485 147 0 384 0
[pid=28475] vsize: 2124
Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 38859 0 0 0 115414 249 0 0 25 0 1 0 1793685388 160555008 38469 4294967295 134512640 135094434 3221224432 3221223024 134556789 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28479/statm): 39198 38469 145 145 0 39053 0
[pid=28479] vsize: 156792
Current children cumulated CPU time (s) 1156.64
Current children cumulated vsize (Kb) 158916

[startup+1170.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28479
Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28475/statm): 531 226 485 147 0 384 0
[pid=28475] vsize: 2124
Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 38859 0 0 0 116414 249 0 0 25 0 1 0 1793685388 160555008 38469 4294967295 134512640 135094434 3221224432 3221223104 134555574 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28479/statm): 39198 38469 145 145 0 39053 0
[pid=28479] vsize: 156792
Current children cumulated CPU time (s) 1166.64
Current children cumulated vsize (Kb) 158916

[startup+1180.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28479
Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28475/statm): 531 226 485 147 0 384 0
[pid=28475] vsize: 2124
Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 38859 0 0 0 117414 249 0 0 25 0 1 0 1793685388 160555008 38469 4294967295 134512640 135094434 3221224432 3221223088 134558178 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28479/statm): 39198 38469 145 145 0 39053 0
[pid=28479] vsize: 156792
Current children cumulated CPU time (s) 1176.64
Current children cumulated vsize (Kb) 158916

[startup+1190.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28479
Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28475/statm): 531 226 485 147 0 384 0
[pid=28475] vsize: 2124
Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 38859 0 0 0 118415 249 0 0 25 0 1 0 1793685388 160555008 38469 4294967295 134512640 135094434 3221224432 3221223072 134558269 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28479/statm): 39198 38469 145 145 0 39053 0
[pid=28479] vsize: 156792
Current children cumulated CPU time (s) 1186.65
Current children cumulated vsize (Kb) 158916

[startup+1200.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28479
Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28475/statm): 531 226 485 147 0 384 0
[pid=28475] vsize: 2124
Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 38859 0 0 0 119415 249 0 0 25 0 1 0 1793685388 160555008 38469 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28479/statm): 39198 38469 145 145 0 39053 0
[pid=28479] vsize: 156792
Current children cumulated CPU time (s) 1196.65
Current children cumulated vsize (Kb) 158916

[startup+1210.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28479
Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28475/statm): 531 226 485 147 0 384 0
[pid=28475] vsize: 2124
Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 38859 0 0 0 120415 249 0 0 25 0 1 0 1793685388 160555008 38469 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28479/statm): 39198 38469 145 145 0 39053 0
[pid=28479] vsize: 156792
Current children cumulated CPU time (s) 1206.65
Current children cumulated vsize (Kb) 158916



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28479
Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28475/statm): 531 226 485 147 0 384 0
[pid=28475] vsize: 2124
Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 38859 0 0 0 120415 249 0 0 25 0 1 0 1793685388 160555008 38469 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28479/statm): 39198 38469 145 145 0 39053 0
[pid=28479] vsize: 156792
Current children cumulated CPU time (s) 1206.65
Current children cumulated vsize (Kb) 158916

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

Child status: 0
Real time (s): 1210.17
CPU time (s): 1206.72
CPU user time (s): 1204.16
CPU system time (s): 2.56661
CPU usage (%): 99.7156
Max. virtual memory (cumulated for all children) (Kb): 158916

Verifier Data

ERROR: no interpretation found !