Some explanations

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

General information on the benchmark

Namemps-v2-20-10/MIPLIB/miplib/normalized-mps-v2-20-10-l152lav.opb
MD5SUM00855a9538cee8df79108d56ee6867b4
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.4
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 3861

Launcher Data

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.220
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	: 901.12

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        893520 kB
Buffers:         36328 kB
Cached:          77832 kB
SwapCached:        896 kB
Active:          72056 kB
Inactive:        44756 kB
HighTotal:      131008 kB
HighFree:        51772 kB
LowTotal:       903652 kB
LowFree:        841748 kB
SwapTotal:     2097892 kB
SwapFree:      2096496 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5720 kB
Slab:            18804 kB
Committed_AS:    64168 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-09-19 03:27:09 (client local time) WITH STATUS 0 IN 1206.8 SECONDS
stats: 2859 7 1206.8 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/19136/stat): 19136 (minisat+_script) R 19135 19136 4419 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1846555221 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 1 0 0
Raw data (/proc/19136/statm): 174 3 169 147 0 27 0
[pid=19136] 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=19137
New process pid=19138
New process pid=19139
execve syscall for /bin/sed executable
One traced child (pid=19138) 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=19139) exited with status: 0
One traced child (pid=19137) exited with status: 0
New process pid=19140
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc25/normalized-mps-v2-20-10-l152lav.opb

[startup+10.0038 s]
Raw data (loadavg): 0.94 1.11 1.09 2/57 19140
Raw data (/proc/19136/stat): 19136 (minisat+_script) S 19135 19136 4419 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846555221 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19136/statm): 531 226 485 147 0 384 0
[pid=19136] vsize: 2124
Raw data (/proc/19140/stat): 19140 (minisat+_64-bit) R 19136 19136 4419 0 -1 0 4201 0 0 0 961 18 0 0 25 0 1 0 1846555226 18092032 3811 4294967295 134512640 135094434 3221224432 3221223024 134556853 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19140/statm): 4417 3811 145 145 0 4272 0
[pid=19140] vsize: 17668
Current children cumulated CPU time (s) 9.81
Current children cumulated vsize (Kb) 19792

[startup+20.0054 s]
Raw data (loadavg): 0.95 1.11 1.09 2/57 19140
Raw data (/proc/19136/stat): 19136 (minisat+_script) S 19135 19136 4419 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846555221 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19136/statm): 531 226 485 147 0 384 0
[pid=19136] vsize: 2124
Raw data (/proc/19140/stat): 19140 (minisat+_64-bit) R 19136 19136 4419 0 -1 0 4575 0 0 0 1953 22 0 0 25 0 1 0 1846555226 19628032 4185 4294967295 134512640 135094434 3221224432 3221223092 134553536 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19140/statm): 4792 4185 145 145 0 4647 0
[pid=19140] vsize: 19168
Current children cumulated CPU time (s) 19.77
Current children cumulated vsize (Kb) 21292

[startup+30.007 s]
Raw data (loadavg): 0.96 1.10 1.09 2/57 19140
Raw data (/proc/19136/stat): 19136 (minisat+_script) S 19135 19136 4419 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846555221 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19136/statm): 531 226 485 147 0 384 0
[pid=19136] vsize: 2124
Raw data (/proc/19140/stat): 19140 (minisat+_64-bit) R 19136 19136 4419 0 -1 0 4727 0 0 0 2950 24 0 0 25 0 1 0 1846555226 20275200 4337 4294967295 134512640 135094434 3221224432 3221223072 134558048 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19140/statm): 4950 4337 145 145 0 4805 0
[pid=19140] vsize: 19800
Current children cumulated CPU time (s) 29.76
Current children cumulated vsize (Kb) 21924

[startup+40.0076 s]
Raw data (loadavg): 0.96 1.10 1.09 2/57 19140
Raw data (/proc/19136/stat): 19136 (minisat+_script) S 19135 19136 4419 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846555221 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19136/statm): 531 226 485 147 0 384 0
[pid=19136] vsize: 2124
Raw data (/proc/19140/stat): 19140 (minisat+_64-bit) R 19136 19136 4419 0 -1 0 4840 0 0 0 3947 25 0 0 25 0 1 0 1846555226 20725760 4450 4294967295 134512640 135094434 3221224432 3221223024 134556975 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19140/statm): 5060 4450 145 145 0 4915 0
[pid=19140] vsize: 20240
Current children cumulated CPU time (s) 39.74
Current children cumulated vsize (Kb) 22364

[startup+50.0092 s]
Raw data (loadavg): 0.97 1.09 1.09 2/57 19140
Raw data (/proc/19136/stat): 19136 (minisat+_script) S 19135 19136 4419 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846555221 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19136/statm): 531 226 485 147 0 384 0
[pid=19136] vsize: 2124
Raw data (/proc/19140/stat): 19140 (minisat+_64-bit) R 19136 19136 4419 0 -1 0 5060 0 0 0 4943 27 0 0 25 0 1 0 1846555226 21614592 4670 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19140/statm): 5277 4670 145 145 0 5132 0
[pid=19140] vsize: 21108
Current children cumulated CPU time (s) 49.72
Current children cumulated vsize (Kb) 23232

[startup+60.0098 s]
Raw data (loadavg): 0.97 1.09 1.09 2/57 19140
Raw data (/proc/19136/stat): 19136 (minisat+_script) S 19135 19136 4419 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846555221 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19136/statm): 531 226 485 147 0 384 0
[pid=19136] vsize: 2124
Raw data (/proc/19140/stat): 19140 (minisat+_64-bit) R 19136 19136 4419 0 -1 0 5419 0 0 0 5937 30 0 0 25 0 1 0 1846555226 23126016 5029 4294967295 134512640 135094434 3221224432 3221223088 134557866 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19140/statm): 5646 5029 145 145 0 5501 0
[pid=19140] vsize: 22584
Current children cumulated CPU time (s) 59.69
Current children cumulated vsize (Kb) 24708

[startup+70.0114 s]
Raw data (loadavg): 0.98 1.09 1.09 2/57 19140
Raw data (/proc/19136/stat): 19136 (minisat+_script) S 19135 19136 4419 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846555221 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19136/statm): 531 226 485 147 0 384 0
[pid=19136] vsize: 2124
Raw data (/proc/19140/stat): 19140 (minisat+_64-bit) R 19136 19136 4419 0 -1 0 5817 0 0 0 6931 33 0 0 25 0 1 0 1846555226 24743936 5427 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19140/statm): 6041 5427 145 145 0 5896 0
[pid=19140] vsize: 24164
Current children cumulated CPU time (s) 69.66
Current children cumulated vsize (Kb) 26288

[startup+80.013 s]
Raw data (loadavg): 0.98 1.08 1.09 2/57 19140
Raw data (/proc/19136/stat): 19136 (minisat+_script) S 19135 19136 4419 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846555221 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19136/statm): 531 226 485 147 0 384 0
[pid=19136] vsize: 2124
Raw data (/proc/19140/stat): 19140 (minisat+_64-bit) R 19136 19136 4419 0 -1 0 6124 0 0 0 7925 35 0 0 25 0 1 0 1846555226 25985024 5734 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19140/statm): 6344 5734 145 145 0 6199 0
[pid=19140] vsize: 25376
Current children cumulated CPU time (s) 79.62
Current children cumulated vsize (Kb) 27500

[startup+90.0136 s]
Raw data (loadavg): 0.98 1.08 1.08 2/57 19140
Raw data (/proc/19136/stat): 19136 (minisat+_script) S 19135 19136 4419 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846555221 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19136/statm): 531 226 485 147 0 384 0
[pid=19136] vsize: 2124
Raw data (/proc/19140/stat): 19140 (minisat+_64-bit) R 19136 19136 4419 0 -1 0 6551 0 0 0 8917 38 0 0 25 0 1 0 1846555226 27721728 6161 4294967295 134512640 135094434 3221224432 3221223024 134557031 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19140/statm): 6768 6161 145 145 0 6623 0
[pid=19140] vsize: 27072
Current children cumulated CPU time (s) 89.57
Current children cumulated vsize (Kb) 29196

[startup+100.014 s]
Raw data (loadavg): 0.98 1.08 1.08 2/57 19140
Raw data (/proc/19136/stat): 19136 (minisat+_script) S 19135 19136 4419 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846555221 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19136/statm): 531 226 485 147 0 384 0
[pid=19136] vsize: 2124
Raw data (/proc/19140/stat): 19140 (minisat+_64-bit) R 19136 19136 4419 0 -1 0 7229 0 0 0 9909 42 0 0 25 0 1 0 1846555226 30498816 6839 4294967295 134512640 135094434 3221224432 3221223024 134556802 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19140/statm): 7446 6839 145 145 0 7301 0
[pid=19140] vsize: 29784
Current children cumulated CPU time (s) 99.53
Current children cumulated vsize (Kb) 31908

[startup+110.015 s]
Raw data (loadavg): 0.99 1.07 1.08 2/57 19140
Raw data (/proc/19136/stat): 19136 (minisat+_script) S 19135 19136 4419 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846555221 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19136/statm): 531 226 485 147 0 384 0
[pid=19136] vsize: 2124
Raw data (/proc/19140/stat): 19140 (minisat+_64-bit) R 19136 19136 4419 0 -1 0 7491 0 0 0 10905 43 0 0 25 0 1 0 1846555226 31686656 7101 4294967295 134512640 135094434 3221224432 3221223084 134558255 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19140/statm): 7736 7101 145 145 0 7591 0
[pid=19140] vsize: 30944
Current children cumulated CPU time (s) 109.5
Current children cumulated vsize (Kb) 33068

[startup+120.015 s]
Raw data (loadavg): 0.99 1.07 1.08 2/57 19140
Raw data (/proc/19136/stat): 19136 (minisat+_script) S 19135 19136 4419 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846555221 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19136/statm): 531 226 485 147 0 384 0
[pid=19136] vsize: 2124
Raw data (/proc/19140/stat): 19140 (minisat+_64-bit) R 19136 19136 4419 0 -1 0 7971 0 0 0 11897 46 0 0 25 0 1 0 1846555226 33640448 7581 4294967295 134512640 135094434 3221224432 3221223024 134556823 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19140/statm): 8213 7581 145 145 0 8068 0
[pid=19140] vsize: 32852
Current children cumulated CPU time (s) 119.45
Current children cumulated vsize (Kb) 34976

[startup+130.016 s]
Raw data (loadavg): 0.99 1.07 1.08 2/57 19140
Raw data (/proc/19136/stat): 19136 (minisat+_script) S 19135 19136 4419 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846555221 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19136/statm): 531 226 485 147 0 384 0
[pid=19136] vsize: 2124
Raw data (/proc/19140/stat): 19140 (minisat+_64-bit) R 19136 19136 4419 0 -1 0 8352 0 0 0 12889 50 0 0 25 0 1 0 1846555226 35188736 7962 4294967295 134512640 135094434 3221224432 3221223024 134556851 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19140/statm): 8591 7962 145 145 0 8446 0
[pid=19140] vsize: 34364
Current children cumulated CPU time (s) 129.41
Current children cumulated vsize (Kb) 36488

[startup+140.017 s]
Raw data (loadavg): 0.99 1.07 1.08 2/57 19140
Raw data (/proc/19136/stat): 19136 (minisat+_script) S 19135 19136 4419 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846555221 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19136/statm): 531 226 485 147 0 384 0
[pid=19136] vsize: 2124
Raw data (/proc/19140/stat): 19140 (minisat+_64-bit) R 19136 19136 4419 0 -1 0 8915 0 0 0 13881 53 0 0 25 0 1 0 1846555226 37486592 8525 4294967295 134512640 135094434 3221224432 3221223088 134558225 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19140/statm): 9152 8525 145 145 0 9007 0
[pid=19140] vsize: 36608
Current children cumulated CPU time (s) 139.36
Current children cumulated vsize (Kb) 38732

[startup+150.017 s]
Raw data (loadavg): 0.99 1.06 1.08 2/57 19140
Raw data (/proc/19136/stat): 19136 (minisat+_script) S 19135 19136 4419 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846555221 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19136/statm): 531 226 485 147 0 384 0
[pid=19136] vsize: 2124
Raw data (/proc/19140/stat): 19140 (minisat+_64-bit) R 19136 19136 4419 0 -1 0 9491 0 0 0 14872 57 0 0 25 0 1 0 1846555226 39833600 9101 4294967295 134512640 135094434 3221224432 3221223072 134538541 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19140/statm): 9725 9101 145 145 0 9580 0
[pid=19140] vsize: 38900
Current children cumulated CPU time (s) 149.31
Current children cumulated vsize (Kb) 41024

[startup+160.018 s]
Raw data (loadavg): 0.99 1.06 1.08 2/57 19140
Raw data (/proc/19136/stat): 19136 (minisat+_script) S 19135 19136 4419 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846555221 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19136/statm): 531 226 485 147 0 384 0
[pid=19136] vsize: 2124
Raw data (/proc/19140/stat): 19140 (minisat+_64-bit) R 19136 19136 4419 0 -1 0 10045 0 0 0 15863 61 0 0 25 0 1 0 1846555226 42098688 9655 4294967295 134512640 135094434 3221224432 3221223024 134557002 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19140/statm): 10278 9655 145 145 0 10133 0
[pid=19140] vsize: 41112
Current children cumulated CPU time (s) 159.26
Current children cumulated vsize (Kb) 43236

[startup+170.019 s]
Raw data (loadavg): 0.99 1.06 1.08 2/57 19140
Raw data (/proc/19136/stat): 19136 (minisat+_script) S 19135 19136 4419 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846555221 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19136/statm): 531 226 485 147 0 384 0
[pid=19136] vsize: 2124
Raw data (/proc/19140/stat): 19140 (minisat+_64-bit) R 19136 19136 4419 0 -1 0 10550 0 0 0 16856 64 0 0 25 0 1 0 1846555226 44158976 10160 4294967295 134512640 135094434 3221224432 3221223024 134556982 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19140/statm): 10781 10160 145 145 0 10636 0
[pid=19140] vsize: 43124
Current children cumulated CPU time (s) 169.22
Current children cumulated vsize (Kb) 45248

[startup+180.02 s]
Raw data (loadavg): 0.99 1.06 1.08 2/57 19140
Raw data (/proc/19136/stat): 19136 (minisat+_script) S 19135 19136 4419 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846555221 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19136/statm): 531 226 485 147 0 384 0
[pid=19136] vsize: 2124
Raw data (/proc/19140/stat): 19140 (minisat+_64-bit) R 19136 19136 4419 0 -1 0 11042 0 0 0 17848 68 0 0 25 0 1 0 1846555226 46170112 10652 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19140/statm): 11272 10652 145 145 0 11127 0
[pid=19140] vsize: 45088
Current children cumulated CPU time (s) 179.18
Current children cumulated vsize (Kb) 47212

[startup+190.02 s]
Raw data (loadavg): 0.99 1.05 1.07 2/57 19140
Raw data (/proc/19136/stat): 19136 (minisat+_script) S 19135 19136 4419 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846555221 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19136/statm): 531 226 485 147 0 384 0
[pid=19136] vsize: 2124
Raw data (/proc/19140/stat): 19140 (minisat+_64-bit) R 19136 19136 4419 0 -1 0 11507 0 0 0 18841 70 0 0 25 0 1 0 1846555226 48070656 11117 4294967295 134512640 135094434 3221224432 3221223024 134557537 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19140/statm): 11736 11117 145 145 0 11591 0
[pid=19140] vsize: 46944
Current children cumulated CPU time (s) 189.13
Current children cumulated vsize (Kb) 49068

[startup+200.02 s]
Raw data (loadavg): 0.99 1.05 1.07 2/57 19140
Raw data (/proc/19136/stat): 19136 (minisat+_script) S 19135 19136 4419 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846555221 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19136/statm): 531 226 485 147 0 384 0
[pid=19136] vsize: 2124
Raw data (/proc/19140/stat): 19140 (minisat+_64-bit) R 19136 19136 4419 0 -1 0 11930 0 0 0 19835 73 0 0 25 0 1 0 1846555226 49803264 11540 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19140/statm): 12159 11540 145 145 0 12014 0
[pid=19140] vsize: 48636
Current children cumulated CPU time (s) 199.1
Current children cumulated vsize (Kb) 50760

[startup+210.021 s]
Raw data (loadavg): 0.99 1.05 1.07 2/57 19140
Raw data (/proc/19136/stat): 19136 (minisat+_script) S 19135 19136 4419 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846555221 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19136/statm): 531 226 485 147 0 384 0
[pid=19136] vsize: 2124
Raw data (/proc/19140/stat): 19140 (minisat+_64-bit) T 19136 19136 4419 0 -1 0 12300 0 0 0 20830 75 0 0 25 0 1 0 1846555226 51331072 11910 4294967295 134512640 135094434 3221224432 3221222780 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/19140/statm): 12532 11910 145 145 0 12387 0
[pid=19140] vsize: 50128
Current children cumulated CPU time (s) 209.07
Current children cumulated vsize (Kb) 52252

[startup+220.021 s]
Raw data (loadavg): 0.99 1.05 1.07 2/57 19140
Raw data (/proc/19136/stat): 19136 (minisat+_script) S 19135 19136 4419 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846555221 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19136/statm): 531 226 485 147 0 384 0
[pid=19136] vsize: 2124
Raw data (/proc/19140/stat): 19140 (minisat+_64-bit) R 19136 19136 4419 0 -1 0 12615 0 0 0 21824 77 0 0 25 0 1 0 1846555226 52617216 12225 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19140/statm): 12846 12225 145 145 0 12701 0
[pid=19140] vsize: 51384
Current children cumulated CPU time (s) 219.03
Current children cumulated vsize (Kb) 53508

[startup+230.022 s]
Raw data (loadavg): 0.99 1.05 1.07 2/57 19140
Raw data (/proc/19136/stat): 19136 (minisat+_script) S 19135 19136 4419 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846555221 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19136/statm): 531 226 485 147 0 384 0
[pid=19136] vsize: 2124
Raw data (/proc/19140/stat): 19140 (minisat+_64-bit) R 19136 19136 4419 0 -1 0 12931 0 0 0 22820 79 0 0 25 0 1 0 1846555226 53907456 12541 4294967295 134512640 135094434 3221224432 3221223024 134557037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19140/statm): 13161 12541 145 145 0 13016 0
[pid=19140] vsize: 52644
Current children cumulated CPU time (s) 229.01
Current children cumulated vsize (Kb) 54768

[startup+240.023 s]
Raw data (loadavg): 0.99 1.04 1.07 2/57 19140
Raw data (/proc/19136/stat): 19136 (minisat+_script) S 19135 19136 4419 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846555221 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19136/statm): 531 226 485 147 0 384 0
[pid=19136] vsize: 2124
Raw data (/proc/19140/stat): 19140 (minisat+_64-bit) R 19136 19136 4419 0 -1 0 13253 0 0 0 23816 81 0 0 25 0 1 0 1846555226 55218176 12863 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19140/statm): 13481 12863 145 145 0 13336 0
[pid=19140] vsize: 53924
Current children cumulated CPU time (s) 238.99
Current children cumulated vsize (Kb) 56048

[startup+250.023 s]
Raw data (loadavg): 0.99 1.04 1.07 2/57 19140
Raw data (/proc/19136/stat): 19136 (minisat+_script) S 19135 19136 4419 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846555221 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19136/statm): 531 226 485 147 0 384 0
[pid=19136] vsize: 2124
Raw data (/proc/19140/stat): 19140 (minisat+_64-bit) R 19136 19136 4419 0 -1 0 13634 0 0 0 24810 83 0 0 25 0 1 0 1846555226 56770560 13244 4294967295 134512640 135094434 3221224432 3221223024 134556789 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19140/statm): 13860 13244 145 145 0 13715 0
[pid=19140] vsize: 55440
Current children cumulated CPU time (s) 248.95
Current children cumulated vsize (Kb) 57564

[startup+260.024 s]
Raw data (loadavg): 0.99 1.04 1.07 2/57 19140
Raw data (/proc/19136/stat): 19136 (minisat+_script) S 19135 19136 4419 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846555221 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19136/statm): 531 226 485 147 0 384 0
[pid=19136] vsize: 2124
Raw data (/proc/19140/stat): 19140 (minisat+_64-bit) R 19136 19136 4419 0 -1 0 14094 0 0 0 25803 85 0 0 25 0 1 0 1846555226 58658816 13704 4294967295 134512640 135094434 3221224432 3221223024 134556817 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19140/statm): 14321 13704 145 145 0 14176 0
[pid=19140] vsize: 57284
Current children cumulated CPU time (s) 258.9
Current children cumulated vsize (Kb) 59408

[startup+270.025 s]
Raw data (loadavg): 0.99 1.04 1.07 2/57 19140
Raw data (/proc/19136/stat): 19136 (minisat+_script) S 19135 19136 4419 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846555221 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19136/statm): 531 226 485 147 0 384 0
[pid=19136] vsize: 2124
Raw data (/proc/19140/stat): 19140 (minisat+_64-bit) R 19136 19136 4419 0 -1 0 14522 0 0 0 26798 88 0 0 25 0 1 0 1846555226 60403712 14132 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19140/statm): 14747 14132 145 145 0 14602 0
[pid=19140] vsize: 58988
Current children cumulated CPU time (s) 268.88
Current children cumulated vsize (Kb) 61112

[startup+280.025 s]
Raw data (loadavg): 0.99 1.04 1.07 2/57 19140
Raw data (/proc/19136/stat): 19136 (minisat+_script) S 19135 19136 4419 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846555221 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19136/statm): 531 226 485 147 0 384 0
[pid=19136] vsize: 2124
Raw data (/proc/19140/stat): 19140 (minisat+_64-bit) R 19136 19136 4419 0 -1 0 14970 0 0 0 27792 91 0 0 25 0 1 0 1846555226 62226432 14580 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19140/statm): 15192 14580 145 145 0 15047 0
[pid=19140] vsize: 60768
Current children cumulated CPU time (s) 278.85
Current children cumulated vsize (Kb) 62892

[startup+290.026 s]
Raw data (loadavg): 0.99 1.03 1.06 2/57 19140
Raw data (/proc/19136/stat): 19136 (minisat+_script) S 19135 19136 4419 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846555221 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19136/statm): 531 226 485 147 0 384 0
[pid=19136] vsize: 2124
Raw data (/proc/19140/stat): 19140 (minisat+_64-bit) R 19136 19136 4419 0 -1 0 15415 0 0 0 28786 94 0 0 25 0 1 0 1846555226 64040960 15025 4294967295 134512640 135094434 3221224432 3221223024 134557238 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19140/statm): 15635 15025 145 145 0 15490 0
[pid=19140] vsize: 62540
Current children cumulated CPU time (s) 288.82
Current children cumulated vsize (Kb) 64664

[startup+300.026 s]
Raw data (loadavg): 0.99 1.03 1.06 2/57 19140
Raw data (/proc/19136/stat): 19136 (minisat+_script) S 19135 19136 4419 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846555221 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19136/statm): 531 226 485 147 0 384 0
[pid=19136] vsize: 2124
Raw data (/proc/19140/stat): 19140 (minisat+_64-bit) R 19136 19136 4419 0 -1 0 15874 0 0 0 29778 98 0 0 25 0 1 0 1846555226 66174976 15484 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19140/statm): 16156 15484 145 145 0 16011 0
[pid=19140] vsize: 64624
Current children cumulated CPU time (s) 298.78
Current children cumulated vsize (Kb) 66748

[startup+310.027 s]
Raw data (loadavg): 0.99 1.03 1.06 2/57 19140
Raw data (/proc/19136/stat): 19136 (minisat+_script) S 19135 19136 4419 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846555221 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19136/statm): 531 226 485 147 0 384 0
[pid=19136] vsize: 2124
Raw data (/proc/19140/stat): 19140 (minisat+_64-bit) R 19136 19136 4419 0 -1 0 16304 0 0 0 30772 100 0 0 25 0 1 0 1846555226 67932160 15914 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19140/statm): 16585 15914 145 145 0 16440 0
[pid=19140] vsize: 66340
Current children cumulated CPU time (s) 308.74
Current children cumulated vsize (Kb) 68464

[startup+320.028 s]
Raw data (loadavg): 0.99 1.03 1.06 2/57 19140
Raw data (/proc/19136/stat): 19136 (minisat+_script) S 19135 19136 4419 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846555221 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19136/statm): 531 226 485 147 0 384 0
[pid=19136] vsize: 2124
Raw data (/proc/19140/stat): 19140 (minisat+_64-bit) R 19136 19136 4419 0 -1 0 16627 0 0 0 31767 102 0 0 25 0 1 0 1846555226 69246976 16237 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19140/statm): 16906 16237 145 145 0 16761 0
[pid=19140] vsize: 67624
Current children cumulated CPU time (s) 318.71
Current children cumulated vsize (Kb) 69748

[startup+330.028 s]
Raw data (loadavg): 0.99 1.03 1.06 2/57 19140
Raw data (/proc/19136/stat): 19136 (minisat+_script) S 19135 19136 4419 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846555221 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19136/statm): 531 226 485 147 0 384 0
[pid=19136] vsize: 2124
Raw data (/proc/19140/stat): 19140 (minisat+_64-bit) R 19136 19136 4419 0 -1 0 17023 0 0 0 32761 105 0 0 25 0 1 0 1846555226 70856704 16633 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19140/statm): 17299 16633 145 145 0 17154 0
[pid=19140] vsize: 69196
Current children cumulated CPU time (s) 328.68
Current children cumulated vsize (Kb) 71320

[startup+340.029 s]
Raw data (loadavg): 0.99 1.03 1.06 2/57 19140
Raw data (/proc/19136/stat): 19136 (minisat+_script) S 19135 19136 4419 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846555221 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19136/statm): 531 226 485 147 0 384 0
[pid=19136] vsize: 2124
Raw data (/proc/19140/stat): 19140 (minisat+_64-bit) R 19136 19136 4419 0 -1 0 17554 0 0 0 33753 108 0 0 20 0 1 0 1846555226 73027584 17164 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19140/statm): 17829 17164 145 145 0 17684 0
[pid=19140] vsize: 71316
Current children cumulated CPU time (s) 338.63
Current children cumulated vsize (Kb) 73440

[startup+350.03 s]
Raw data (loadavg): 0.99 1.03 1.06 2/57 19140
Raw data (/proc/19136/stat): 19136 (minisat+_script) S 19135 19136 4419 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846555221 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19136/statm): 531 226 485 147 0 384 0
[pid=19136] vsize: 2124
Raw data (/proc/19140/stat): 19140 (minisat+_64-bit) R 19136 19136 4419 0 -1 0 17990 0 0 0 34746 111 0 0 25 0 1 0 1846555226 74805248 17600 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19140/statm): 18263 17600 145 145 0 18118 0
[pid=19140] vsize: 73052
Current children cumulated CPU time (s) 348.59
Current children cumulated vsize (Kb) 75176

[startup+360.031 s]
Raw data (loadavg): 0.99 1.02 1.06 2/57 19140
Raw data (/proc/19136/stat): 19136 (minisat+_script) S 19135 19136 4419 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846555221 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19136/statm): 531 226 485 147 0 384 0
[pid=19136] vsize: 2124
Raw data (/proc/19140/stat): 19140 (minisat+_64-bit) R 19136 19136 4419 0 -1 0 18513 0 0 0 35738 114 0 0 25 0 1 0 1846555226 76943360 18123 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19140/statm): 18785 18123 145 145 0 18640 0
[pid=19140] vsize: 75140
Current children cumulated CPU time (s) 358.54
Current children cumulated vsize (Kb) 77264

[startup+370.033 s]
Raw data (loadavg): 0.99 1.02 1.06 2/57 19140
Raw data (/proc/19136/stat): 19136 (minisat+_script) S 19135 19136 4419 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846555221 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19136/statm): 531 226 485 147 0 384 0
[pid=19136] vsize: 2124
Raw data (/proc/19140/stat): 19140 (minisat+_64-bit) R 19136 19136 4419 0 -1 0 18939 0 0 0 36731 117 0 0 25 0 1 0 1846555226 78680064 18549 4294967295 134512640 135094434 3221224432 3221223088 134558007 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19140/statm): 19209 18549 145 145 0 19064 0
[pid=19140] vsize: 76836
Current children cumulated CPU time (s) 368.5
Current children cumulated vsize (Kb) 78960

[startup+380.034 s]
Raw data (loadavg): 0.99 1.02 1.06 2/57 19140
Raw data (/proc/19136/stat): 19136 (minisat+_script) S 19135 19136 4419 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846555221 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19136/statm): 531 226 485 147 0 384 0
[pid=19136] vsize: 2124
Raw data (/proc/19140/stat): 19140 (minisat+_64-bit) R 19136 19136 4419 0 -1 0 19387 0 0 0 37723 121 0 0 25 0 1 0 1846555226 80506880 18997 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19140/statm): 19655 18997 145 145 0 19510 0
[pid=19140] vsize: 78620
Current children cumulated CPU time (s) 378.46
Current children cumulated vsize (Kb) 80744

[startup+390.035 s]
Raw data (loadavg): 0.99 1.02 1.06 2/57 19140
Raw data (/proc/19136/stat): 19136 (minisat+_script) S 19135 19136 4419 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846555221 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19136/statm): 531 226 485 147 0 384 0
[pid=19136] vsize: 2124
Raw data (/proc/19140/stat): 19140 (minisat+_64-bit) R 19136 19136 4419 0 -1 0 19849 0 0 0 38715 123 0 0 25 0 1 0 1846555226 82391040 19459 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19140/statm): 20115 19459 145 145 0 19970 0
[pid=19140] vsize: 80460
Current children cumulated CPU time (s) 388.4
Current children cumulated vsize (Kb) 82584

[startup+400.035 s]
Raw data (loadavg): 0.99 1.02 1.05 2/57 19140
Raw data (/proc/19136/stat): 19136 (minisat+_script) S 19135 19136 4419 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846555221 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19136/statm): 531 226 485 147 0 384 0
[pid=19136] vsize: 2124
Raw data (/proc/19140/stat): 19140 (minisat+_64-bit) R 19136 19136 4419 0 -1 0 20301 0 0 0 39709 127 0 0 25 0 1 0 1846555226 84234240 19911 4294967295 134512640 135094434 3221224432 3221223024 134557522 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19140/statm): 20565 19911 145 145 0 20420 0
[pid=19140] vsize: 82260
Current children cumulated CPU time (s) 398.38
Current children cumulated vsize (Kb) 84384

[startup+410.036 s]
Raw data (loadavg): 0.99 1.02 1.05 2/57 19140
Raw data (/proc/19136/stat): 19136 (minisat+_script) S 19135 19136 4419 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846555221 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19136/statm): 531 226 485 147 0 384 0
[pid=19136] vsize: 2124
Raw data (/proc/19140/stat): 19140 (minisat+_64-bit) R 19136 19136 4419 0 -1 0 20707 0 0 0 40701 129 0 0 25 0 1 0 1846555226 85889024 20317 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19140/statm): 20969 20317 145 145 0 20824 0
[pid=19140] vsize: 83876
Current children cumulated CPU time (s) 408.32
Current children cumulated vsize (Kb) 86000

[startup+420.037 s]
Raw data (loadavg): 0.99 1.02 1.05 2/57 19140
Raw data (/proc/19136/stat): 19136 (minisat+_script) S 19135 19136 4419 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846555221 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19136/statm): 531 226 485 147 0 384 0
[pid=19136] vsize: 2124
Raw data (/proc/19140/stat): 19140 (minisat+_64-bit) T 19136 19136 4419 0 -1 0 21067 0 0 0 41695 132 0 0 25 0 1 0 1846555226 87355392 20677 4294967295 134512640 135094434 3221224432 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/19140/statm): 21327 20677 145 145 0 21182 0
[pid=19140] vsize: 85308
Current children cumulated CPU time (s) 418.29
Current children cumulated vsize (Kb) 87432

[startup+430.037 s]
Raw data (loadavg): 0.99 1.02 1.05 2/57 19140
Raw data (/proc/19136/stat): 19136 (minisat+_script) S 19135 19136 4419 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846555221 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19136/statm): 531 226 485 147 0 384 0
[pid=19136] vsize: 2124
Raw data (/proc/19140/stat): 19140 (minisat+_64-bit) R 19136 19136 4419 0 -1 0 21476 0 0 0 42688 135 0 0 25 0 1 0 1846555226 89026560 21086 4294967295 134512640 135094434 3221224432 3221223024 134556961 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19140/statm): 21735 21086 145 145 0 21590 0
[pid=19140] vsize: 86940
Current children cumulated CPU time (s) 428.25
Current children cumulated vsize (Kb) 89064

[startup+440.038 s]
Raw data (loadavg): 0.99 1.02 1.05 2/57 19140
Raw data (/proc/19136/stat): 19136 (minisat+_script) S 19135 19136 4419 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846555221 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19136/statm): 531 226 485 147 0 384 0
[pid=19136] vsize: 2124
Raw data (/proc/19140/stat): 19140 (minisat+_64-bit) R 19136 19136 4419 0 -1 0 21950 0 0 0 43681 139 0 0 25 0 1 0 1846555226 90959872 21560 4294967295 134512640 135094434 3221224432 3221223104 134555583 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19140/statm): 22207 21560 145 145 0 22062 0
[pid=19140] vsize: 88828
Current children cumulated CPU time (s) 438.22
Current children cumulated vsize (Kb) 90952

[startup+450.039 s]
Raw data (loadavg): 0.99 1.02 1.05 2/57 19140
Raw data (/proc/19136/stat): 19136 (minisat+_script) S 19135 19136 4419 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846555221 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19136/statm): 531 226 485 147 0 384 0
[pid=19136] vsize: 2124
Raw data (/proc/19140/stat): 19140 (minisat+_64-bit) R 19136 19136 4419 0 -1 0 22469 0 0 0 44674 142 0 0 25 0 1 0 1846555226 93081600 22079 4294967295 134512640 135094434 3221224432 3221223024 134557500 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19140/statm): 22725 22079 145 145 0 22580 0
[pid=19140] vsize: 90900
Current children cumulated CPU time (s) 448.18
Current children cumulated vsize (Kb) 93024

[startup+460.04 s]
Raw data (loadavg): 0.99 1.02 1.05 2/57 19140
Raw data (/proc/19136/stat): 19136 (minisat+_script) S 19135 19136 4419 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846555221 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19136/statm): 531 226 485 147 0 384 0
[pid=19136] vsize: 2124
Raw data (/proc/19140/stat): 19140 (minisat+_64-bit) R 19136 19136 4419 0 -1 0 23009 0 0 0 45666 145 0 0 25 0 1 0 1846555226 95289344 22619 4294967295 134512640 135094434 3221224432 3221223024 134557230 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19140/statm): 23264 22619 145 145 0 23119 0
[pid=19140] vsize: 93056
Current children cumulated CPU time (s) 458.13
Current children cumulated vsize (Kb) 95180

[startup+470.04 s]
Raw data (loadavg): 0.99 1.01 1.05 2/57 19140
Raw data (/proc/19136/stat): 19136 (minisat+_script) S 19135 19136 4419 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846555221 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19136/statm): 531 226 485 147 0 384 0
[pid=19136] vsize: 2124
Raw data (/proc/19140/stat): 19140 (minisat+_64-bit) R 19136 19136 4419 0 -1 0 23518 0 0 0 46657 149 0 0 25 0 1 0 1846555226 97374208 23128 4294967295 134512640 135094434 3221224432 3221223024 134557028 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19140/statm): 23773 23128 145 145 0 23628 0
[pid=19140] vsize: 95092
Current children cumulated CPU time (s) 468.08
Current children cumulated vsize (Kb) 97216

[startup+480.04 s]
Raw data (loadavg): 0.99 1.01 1.05 2/57 19140
Raw data (/proc/19136/stat): 19136 (minisat+_script) S 19135 19136 4419 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846555221 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19136/statm): 531 226 485 147 0 384 0
[pid=19136] vsize: 2124
Raw data (/proc/19140/stat): 19140 (minisat+_64-bit) R 19136 19136 4419 0 -1 0 23895 0 0 0 47651 151 0 0 25 0 1 0 1846555226 98914304 23505 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19140/statm): 24149 23505 145 145 0 24004 0
[pid=19140] vsize: 96596
Current children cumulated CPU time (s) 478.04
Current children cumulated vsize (Kb) 98720

[startup+490.041 s]
Raw data (loadavg): 0.99 1.01 1.05 2/57 19140
Raw data (/proc/19136/stat): 19136 (minisat+_script) S 19135 19136 4419 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846555221 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19136/statm): 531 226 485 147 0 384 0
[pid=19136] vsize: 2124
Raw data (/proc/19140/stat): 19140 (minisat+_64-bit) R 19136 19136 4419 0 -1 0 24303 0 0 0 48644 153 0 0 25 0 1 0 1846555226 100581376 23913 4294967295 134512640 135094434 3221224432 3221223024 134557522 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19140/statm): 24556 23913 145 145 0 24411 0
[pid=19140] vsize: 98224
Current children cumulated CPU time (s) 487.99
Current children cumulated vsize (Kb) 100348

[startup+500.041 s]
Raw data (loadavg): 0.99 1.01 1.04 2/57 19140
Raw data (/proc/19136/stat): 19136 (minisat+_script) S 19135 19136 4419 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846555221 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19136/statm): 531 226 485 147 0 384 0
[pid=19136] vsize: 2124
Raw data (/proc/19140/stat): 19140 (minisat+_64-bit) R 19136 19136 4419 0 -1 0 24542 0 0 0 49639 155 0 0 25 0 1 0 1846555226 101552128 24152 4294967295 134512640 135094434 3221224432 3221223024 134556773 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19140/statm): 24793 24152 145 145 0 24648 0
[pid=19140] vsize: 99172
Current children cumulated CPU time (s) 497.96
Current children cumulated vsize (Kb) 101296

[startup+510.042 s]
Raw data (loadavg): 0.99 1.01 1.04 2/57 19140
Raw data (/proc/19136/stat): 19136 (minisat+_script) S 19135 19136 4419 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846555221 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19136/statm): 531 226 485 147 0 384 0
[pid=19136] vsize: 2124
Raw data (/proc/19140/stat): 19140 (minisat+_64-bit) R 19136 19136 4419 0 -1 0 24970 0 0 0 50630 159 0 0 25 0 1 0 1846555226 103297024 24580 4294967295 134512640 135094434 3221224432 3221223024 134557219 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19140/statm): 25219 24580 145 145 0 25074 0
[pid=19140] vsize: 100876
Current children cumulated CPU time (s) 507.91
Current children cumulated vsize (Kb) 103000

[startup+520.042 s]
Raw data (loadavg): 0.99 1.01 1.04 2/57 19140
Raw data (/proc/19136/stat): 19136 (minisat+_script) S 19135 19136 4419 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846555221 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19136/statm): 531 226 485 147 0 384 0
[pid=19136] vsize: 2124
Raw data (/proc/19140/stat): 19140 (minisat+_64-bit) R 19136 19136 4419 0 -1 0 25444 0 0 0 51623 162 0 0 25 0 1 0 1846555226 105230336 25054 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19140/statm): 25691 25054 145 145 0 25546 0
[pid=19140] vsize: 102764
Current children cumulated CPU time (s) 517.87
Current children cumulated vsize (Kb) 104888

[startup+530.042 s]
Raw data (loadavg): 0.99 1.01 1.04 2/57 19140
Raw data (/proc/19136/stat): 19136 (minisat+_script) S 19135 19136 4419 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846555221 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19136/statm): 531 226 485 147 0 384 0
[pid=19136] vsize: 2124
Raw data (/proc/19140/stat): 19140 (minisat+_64-bit) R 19136 19136 4419 0 -1 0 25935 0 0 0 52616 165 0 0 25 0 1 0 1846555226 107237376 25545 4294967295 134512640 135094434 3221224432 3221223056 134557714 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19140/statm): 26181 25545 145 145 0 26036 0
[pid=19140] vsize: 104724
Current children cumulated CPU time (s) 527.83
Current children cumulated vsize (Kb) 106848

[startup+540.043 s]
Raw data (loadavg): 0.99 1.01 1.04 2/57 19140
Raw data (/proc/19136/stat): 19136 (minisat+_script) S 19135 19136 4419 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846555221 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19136/statm): 531 226 485 147 0 384 0
[pid=19136] vsize: 2124
Raw data (/proc/19140/stat): 19140 (minisat+_64-bit) R 19136 19136 4419 0 -1 0 26365 0 0 0 53610 167 0 0 25 0 1 0 1846555226 108994560 25975 4294967295 134512640 135094434 3221224432 3221223024 134557182 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19140/statm): 26610 25975 145 145 0 26465 0
[pid=19140] vsize: 106440
Current children cumulated CPU time (s) 537.79
Current children cumulated vsize (Kb) 108564

[startup+550.044 s]
Raw data (loadavg): 0.99 1.01 1.04 2/57 19140
Raw data (/proc/19136/stat): 19136 (minisat+_script) S 19135 19136 4419 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846555221 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19136/statm): 531 226 485 147 0 384 0
[pid=19136] vsize: 2124
Raw data (/proc/19140/stat): 19140 (minisat+_64-bit) R 19136 19136 4419 0 -1 0 26790 0 0 0 54605 169 0 0 25 0 1 0 1846555226 110727168 26400 4294967295 134512640 135094434 3221224432 3221223088 134558126 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19140/statm): 27033 26400 145 145 0 26888 0
[pid=19140] vsize: 108132
Current children cumulated CPU time (s) 547.76
Current children cumulated vsize (Kb) 110256

[startup+560.045 s]
Raw data (loadavg): 0.99 1.01 1.04 2/57 19140
Raw data (/proc/19136/stat): 19136 (minisat+_script) S 19135 19136 4419 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846555221 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19136/statm): 531 226 485 147 0 384 0
[pid=19136] vsize: 2124
Raw data (/proc/19140/stat): 19140 (minisat+_64-bit) R 19136 19136 4419 0 -1 0 27252 0 0 0 55598 172 0 0 25 0 1 0 1846555226 112615424 26862 4294967295 134512640 135094434 3221224432 3221223024 134557413 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19140/statm): 27494 26862 145 145 0 27349 0
[pid=19140] vsize: 109976
Current children cumulated CPU time (s) 557.72
Current children cumulated vsize (Kb) 112100

[startup+570.046 s]
Raw data (loadavg): 0.99 1.00 1.04 2/57 19140
Raw data (/proc/19136/stat): 19136 (minisat+_script) S 19135 19136 4419 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846555221 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19136/statm): 531 226 485 147 0 384 0
[pid=19136] vsize: 2124
Raw data (/proc/19140/stat): 19140 (minisat+_64-bit) R 19136 19136 4419 0 -1 0 27665 0 0 0 56590 175 0 0 25 0 1 0 1846555226 114302976 27275 4294967295 134512640 135094434 3221224432 3221223024 134557025 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19140/statm): 27906 27275 145 145 0 27761 0
[pid=19140] vsize: 111624
Current children cumulated CPU time (s) 567.67
Current children cumulated vsize (Kb) 113748

[startup+580.046 s]
Raw data (loadavg): 0.99 1.00 1.04 2/57 19140
Raw data (/proc/19136/stat): 19136 (minisat+_script) S 19135 19136 4419 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846555221 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19136/statm): 531 226 485 147 0 384 0
[pid=19136] vsize: 2124
Raw data (/proc/19140/stat): 19140 (minisat+_64-bit) R 19136 19136 4419 0 -1 0 28063 0 0 0 57585 177 0 0 25 0 1 0 1846555226 115929088 27673 4294967295 134512640 135094434 3221224432 3221223024 134557002 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19140/statm): 28303 27673 145 145 0 28158 0
[pid=19140] vsize: 113212
Current children cumulated CPU time (s) 577.64
Current children cumulated vsize (Kb) 115336

[startup+590.046 s]
Raw data (loadavg): 0.99 1.00 1.04 2/57 19140
Raw data (/proc/19136/stat): 19136 (minisat+_script) S 19135 19136 4419 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846555221 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19136/statm): 531 226 485 147 0 384 0
[pid=19136] vsize: 2124
Raw data (/proc/19140/stat): 19140 (minisat+_64-bit) R 19136 19136 4419 0 -1 0 28456 0 0 0 58580 178 0 0 25 0 1 0 1846555226 117534720 28066 4294967295 134512640 135094434 3221224432 3221223088 134558210 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19140/statm): 28695 28066 145 145 0 28550 0
[pid=19140] vsize: 114780
Current children cumulated CPU time (s) 587.6
Current children cumulated vsize (Kb) 116904

[startup+600.046 s]
Raw data (loadavg): 0.99 1.00 1.03 2/57 19140
Raw data (/proc/19136/stat): 19136 (minisat+_script) S 19135 19136 4419 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846555221 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19136/statm): 531 226 485 147 0 384 0
[pid=19136] vsize: 2124
Raw data (/proc/19140/stat): 19140 (minisat+_64-bit) R 19136 19136 4419 0 -1 0 28787 0 0 0 59574 180 0 0 25 0 1 0 1846555226 118886400 28397 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19140/statm): 29025 28397 145 145 0 28880 0
[pid=19140] vsize: 116100
Current children cumulated CPU time (s) 597.56
Current children cumulated vsize (Kb) 118224

[startup+610.047 s]
Raw data (loadavg): 0.99 1.00 1.03 2/57 19140
Raw data (/proc/19136/stat): 19136 (minisat+_script) S 19135 19136 4419 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846555221 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19136/statm): 531 226 485 147 0 384 0
[pid=19136] vsize: 2124
Raw data (/proc/19140/stat): 19140 (minisat+_64-bit) R 19136 19136 4419 0 -1 0 29264 0 0 0 60566 184 0 0 25 0 1 0 1846555226 120844288 28874 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19140/statm): 29503 28874 145 145 0 29358 0
[pid=19140] vsize: 118012
Current children cumulated CPU time (s) 607.52
Current children cumulated vsize (Kb) 120136

[startup+620.047 s]
Raw data (loadavg): 0.99 1.00 1.03 2/57 19140
Raw data (/proc/19136/stat): 19136 (minisat+_script) S 19135 19136 4419 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846555221 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19136/statm): 531 226 485 147 0 384 0
[pid=19136] vsize: 2124
Raw data (/proc/19140/stat): 19140 (minisat+_64-bit) R 19136 19136 4419 0 -1 0 29788 0 0 0 61558 188 0 0 25 0 1 0 1846555226 122982400 29398 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19140/statm): 30025 29398 145 145 0 29880 0
[pid=19140] vsize: 120100
Current children cumulated CPU time (s) 617.48
Current children cumulated vsize (Kb) 122224

[startup+630.047 s]
Raw data (loadavg): 0.99 1.00 1.03 2/57 19140
Raw data (/proc/19136/stat): 19136 (minisat+_script) S 19135 19136 4419 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846555221 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19136/statm): 531 226 485 147 0 384 0
[pid=19136] vsize: 2124
Raw data (/proc/19140/stat): 19140 (minisat+_64-bit) R 19136 19136 4419 0 -1 0 30414 0 0 0 62548 192 0 0 25 0 1 0 1846555226 125538304 30024 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19140/statm): 30649 30024 145 145 0 30504 0
[pid=19140] vsize: 122596
Current children cumulated CPU time (s) 627.42
Current children cumulated vsize (Kb) 124720

[startup+640.048 s]
Raw data (loadavg): 0.99 1.00 1.03 2/57 19140
Raw data (/proc/19136/stat): 19136 (minisat+_script) S 19135 19136 4419 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846555221 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19136/statm): 531 226 485 147 0 384 0
[pid=19136] vsize: 2124
Raw data (/proc/19140/stat): 19140 (minisat+_64-bit) R 19136 19136 4419 0 -1 0 31055 0 0 0 63538 195 0 0 25 0 1 0 1846555226 128155648 30665 4294967295 134512640 135094434 3221224432 3221223104 134555811 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19140/statm): 31288 30665 145 145 0 31143 0
[pid=19140] vsize: 125152
Current children cumulated CPU time (s) 637.35
Current children cumulated vsize (Kb) 127276

[startup+650.048 s]
Raw data (loadavg): 0.99 1.00 1.03 2/57 19140
Raw data (/proc/19136/stat): 19136 (minisat+_script) S 19135 19136 4419 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846555221 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19136/statm): 531 226 485 147 0 384 0
[pid=19136] vsize: 2124
Raw data (/proc/19140/stat): 19140 (minisat+_64-bit) R 19136 19136 4419 0 -1 0 31444 0 0 0 64533 197 0 0 25 0 1 0 1846555226 129744896 31054 4294967295 134512640 135094434 3221224432 3221223056 134557737 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19140/statm): 31676 31054 145 145 0 31531 0
[pid=19140] vsize: 126704
Current children cumulated CPU time (s) 647.32
Current children cumulated vsize (Kb) 128828

[startup+660.049 s]
Raw data (loadavg): 0.99 1.00 1.03 2/57 19140
Raw data (/proc/19136/stat): 19136 (minisat+_script) S 19135 19136 4419 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846555221 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19136/statm): 531 226 485 147 0 384 0
[pid=19136] vsize: 2124
Raw data (/proc/19140/stat): 19140 (minisat+_64-bit) R 19136 19136 4419 0 -1 0 32035 0 0 0 65526 200 0 0 25 0 1 0 1846555226 132161536 31645 4294967295 134512640 135094434 3221224432 3221223088 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19140/statm): 32266 31645 145 145 0 32121 0
[pid=19140] vsize: 129064
Current children cumulated CPU time (s) 657.28
Current children cumulated vsize (Kb) 131188

[startup+670.05 s]
Raw data (loadavg): 0.99 1.00 1.03 2/57 19140
Raw data (/proc/19136/stat): 19136 (minisat+_script) S 19135 19136 4419 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846555221 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19136/statm): 531 226 485 147 0 384 0
[pid=19136] vsize: 2124
Raw data (/proc/19140/stat): 19140 (minisat+_64-bit) R 19136 19136 4419 0 -1 0 32523 0 0 0 66518 203 0 0 25 0 1 0 1846555226 134152192 32133 4294967295 134512640 135094434 3221224432 3221223024 134557219 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19140/statm): 32752 32133 145 145 0 32607 0
[pid=19140] vsize: 131008
Current children cumulated CPU time (s) 667.23
Current children cumulated vsize (Kb) 133132

[startup+680.05 s]
Raw data (loadavg): 0.99 1.00 1.03 2/57 19140
Raw data (/proc/19136/stat): 19136 (minisat+_script) S 19135 19136 4419 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846555221 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19136/statm): 531 226 485 147 0 384 0
[pid=19136] vsize: 2124
Raw data (/proc/19140/stat): 19140 (minisat+_64-bit) R 19136 19136 4419 0 -1 0 32893 0 0 0 67513 205 0 0 25 0 1 0 1846555226 135667712 32503 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19140/statm): 33122 32503 145 145 0 32977 0
[pid=19140] vsize: 132488
Current children cumulated CPU time (s) 677.2
Current children cumulated vsize (Kb) 134612

[startup+690.051 s]
Raw data (loadavg): 0.99 1.00 1.03 2/57 19140
Raw data (/proc/19136/stat): 19136 (minisat+_script) S 19135 19136 4419 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846555221 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19136/statm): 531 226 485 147 0 384 0
[pid=19136] vsize: 2124
Raw data (/proc/19140/stat): 19140 (minisat+_64-bit) R 19136 19136 4419 0 -1 0 33236 0 0 0 68507 207 0 0 25 0 1 0 1846555226 137060352 32846 4294967295 134512640 135094434 3221224432 3221223024 134557137 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19140/statm): 33462 32846 145 145 0 33317 0
[pid=19140] vsize: 133848
Current children cumulated CPU time (s) 687.16
Current children cumulated vsize (Kb) 135972

[startup+700.052 s]
Raw data (loadavg): 0.99 1.00 1.02 2/57 19140
Raw data (/proc/19136/stat): 19136 (minisat+_script) S 19135 19136 4419 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846555221 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19136/statm): 531 226 485 147 0 384 0
[pid=19136] vsize: 2124
Raw data (/proc/19140/stat): 19140 (minisat+_64-bit) R 19136 19136 4419 0 -1 0 33455 0 0 0 69502 209 0 0 25 0 1 0 1846555226 138477568 33065 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19140/statm): 33808 33065 145 145 0 33663 0
[pid=19140] vsize: 135232
Current children cumulated CPU time (s) 697.13
Current children cumulated vsize (Kb) 137356

[startup+710.052 s]
Raw data (loadavg): 0.99 1.00 1.02 2/57 19140
Raw data (/proc/19136/stat): 19136 (minisat+_script) S 19135 19136 4419 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846555221 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19136/statm): 531 226 485 147 0 384 0
[pid=19136] vsize: 2124
Raw data (/proc/19140/stat): 19140 (minisat+_64-bit) R 19136 19136 4419 0 -1 0 33692 0 0 0 70499 210 0 0 25 0 1 0 1846555226 139440128 33302 4294967295 134512640 135094434 3221224432 3221223024 134556937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19140/statm): 34043 33302 145 145 0 33898 0
[pid=19140] vsize: 136172
Current children cumulated CPU time (s) 707.11
Current children cumulated vsize (Kb) 138296

[startup+720.052 s]
Raw data (loadavg): 0.99 1.00 1.02 2/57 19140
Raw data (/proc/19136/stat): 19136 (minisat+_script) S 19135 19136 4419 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846555221 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19136/statm): 531 226 485 147 0 384 0
[pid=19136] vsize: 2124
Raw data (/proc/19140/stat): 19140 (minisat+_64-bit) R 19136 19136 4419 0 -1 0 34166 0 0 0 71492 213 0 0 25 0 1 0 1846555226 141377536 33776 4294967295 134512640 135094434 3221224432 3221223024 134557366 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19140/statm): 34516 33776 145 145 0 34371 0
[pid=19140] vsize: 138064
Current children cumulated CPU time (s) 717.07
Current children cumulated vsize (Kb) 140188

[startup+730.052 s]
Raw data (loadavg): 0.99 1.00 1.02 2/57 19140
Raw data (/proc/19136/stat): 19136 (minisat+_script) S 19135 19136 4419 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846555221 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19136/statm): 531 226 485 147 0 384 0
[pid=19136] vsize: 2124
Raw data (/proc/19140/stat): 19140 (minisat+_64-bit) R 19136 19136 4419 0 -1 0 34829 0 0 0 72482 217 0 0 25 0 1 0 1846555226 144084992 34439 4294967295 134512640 135094434 3221224432 3221223024 134557350 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19140/statm): 35177 34439 145 145 0 35032 0
[pid=19140] vsize: 140708
Current children cumulated CPU time (s) 727.01
Current children cumulated vsize (Kb) 142832

[startup+740.053 s]
Raw data (loadavg): 0.99 1.00 1.02 2/57 19140
Raw data (/proc/19136/stat): 19136 (minisat+_script) S 19135 19136 4419 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846555221 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19136/statm): 531 226 485 147 0 384 0
[pid=19136] vsize: 2124
Raw data (/proc/19140/stat): 19140 (minisat+_64-bit) R 19136 19136 4419 0 -1 0 35364 0 0 0 73475 219 0 0 25 0 1 0 1846555226 146272256 34974 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19140/statm): 35711 34974 145 145 0 35566 0
[pid=19140] vsize: 142844
Current children cumulated CPU time (s) 736.96
Current children cumulated vsize (Kb) 144968

[startup+750.054 s]
Raw data (loadavg): 0.99 1.00 1.02 2/57 19140
Raw data (/proc/19136/stat): 19136 (minisat+_script) S 19135 19136 4419 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846555221 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19136/statm): 531 226 485 147 0 384 0
[pid=19136] vsize: 2124
Raw data (/proc/19140/stat): 19140 (minisat+_64-bit) R 19136 19136 4419 0 -1 0 35864 0 0 0 74468 222 0 0 25 0 1 0 1846555226 148320256 35474 4294967295 134512640 135094434 3221224432 3221223024 134557518 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19140/statm): 36211 35474 145 145 0 36066 0
[pid=19140] vsize: 144844
Current children cumulated CPU time (s) 746.92
Current children cumulated vsize (Kb) 146968

[startup+760.055 s]
Raw data (loadavg): 0.99 1.00 1.02 2/57 19140
Raw data (/proc/19136/stat): 19136 (minisat+_script) S 19135 19136 4419 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846555221 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19136/statm): 531 226 485 147 0 384 0
[pid=19136] vsize: 2124
Raw data (/proc/19140/stat): 19140 (minisat+_64-bit) R 19136 19136 4419 0 -1 0 36305 0 0 0 75462 224 0 0 25 0 1 0 1846555226 150122496 35915 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19140/statm): 36651 35915 145 145 0 36506 0
[pid=19140] vsize: 146604
Current children cumulated CPU time (s) 756.88
Current children cumulated vsize (Kb) 148728

[startup+770.055 s]
Raw data (loadavg): 0.99 1.00 1.02 2/57 19140
Raw data (/proc/19136/stat): 19136 (minisat+_script) S 19135 19136 4419 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846555221 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19136/statm): 531 226 485 147 0 384 0
[pid=19136] vsize: 2124
Raw data (/proc/19140/stat): 19140 (minisat+_64-bit) R 19136 19136 4419 0 -1 0 36761 0 0 0 76456 227 0 0 25 0 1 0 1846555226 151982080 36371 4294967295 134512640 135094434 3221224432 3221223088 134558240 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19140/statm): 37105 36371 145 145 0 36960 0
[pid=19140] vsize: 148420
Current children cumulated CPU time (s) 766.85
Current children cumulated vsize (Kb) 150544

[startup+780.055 s]
Raw data (loadavg): 0.99 1.00 1.02 2/57 19140
Raw data (/proc/19136/stat): 19136 (minisat+_script) S 19135 19136 4419 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846555221 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19136/statm): 531 226 485 147 0 384 0
[pid=19136] vsize: 2124
Raw data (/proc/19140/stat): 19140 (minisat+_64-bit) R 19136 19136 4419 0 -1 0 37267 0 0 0 77448 231 0 0 25 0 1 0 1846555226 154050560 36877 4294967295 134512640 135094434 3221224432 3221223024 134557512 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19140/statm): 37610 36877 145 145 0 37465 0
[pid=19140] vsize: 150440
Current children cumulated CPU time (s) 776.81
Current children cumulated vsize (Kb) 152564

[startup+790.056 s]
Raw data (loadavg): 0.99 1.00 1.02 2/57 19140
Raw data (/proc/19136/stat): 19136 (minisat+_script) S 19135 19136 4419 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846555221 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19136/statm): 531 226 485 147 0 384 0
[pid=19136] vsize: 2124
Raw data (/proc/19140/stat): 19140 (minisat+_64-bit) R 19136 19136 4419 0 -1 0 37532 0 0 0 78443 233 0 0 25 0 1 0 1846555226 155131904 37142 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19140/statm): 37874 37142 145 145 0 37729 0
[pid=19140] vsize: 151496
Current children cumulated CPU time (s) 786.78
Current children cumulated vsize (Kb) 153620

[startup+800.057 s]
Raw data (loadavg): 0.99 1.00 1.02 2/57 19140
Raw data (/proc/19136/stat): 19136 (minisat+_script) S 19135 19136 4419 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846555221 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19136/statm): 531 226 485 147 0 384 0
[pid=19136] vsize: 2124
Raw data (/proc/19140/stat): 19140 (minisat+_64-bit) R 19136 19136 4419 0 -1 0 37941 0 0 0 79436 235 0 0 25 0 1 0 1846555226 156803072 37551 4294967295 134512640 135094434 3221224432 3221223024 134556802 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19140/statm): 38282 37551 145 145 0 38137 0
[pid=19140] vsize: 153128
Current children cumulated CPU time (s) 796.73
Current children cumulated vsize (Kb) 155252

[startup+810.057 s]
Raw data (loadavg): 0.99 1.00 1.01 2/57 19140
Raw data (/proc/19136/stat): 19136 (minisat+_script) S 19135 19136 4419 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846555221 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19136/statm): 531 226 485 147 0 384 0
[pid=19136] vsize: 2124
Raw data (/proc/19140/stat): 19140 (minisat+_64-bit) R 19136 19136 4419 0 -1 0 38334 0 0 0 80431 238 0 0 25 0 1 0 1846555226 158416896 37944 4294967295 134512640 135094434 3221224432 3221223024 134557141 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19140/statm): 38676 37944 145 145 0 38531 0
[pid=19140] vsize: 154704
Current children cumulated CPU time (s) 806.71
Current children cumulated vsize (Kb) 156828

[startup+820.058 s]
Raw data (loadavg): 0.99 1.00 1.01 2/57 19140
Raw data (/proc/19136/stat): 19136 (minisat+_script) S 19135 19136 4419 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846555221 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19136/statm): 531 226 485 147 0 384 0
[pid=19136] vsize: 2124
Raw data (/proc/19140/stat): 19140 (minisat+_64-bit) R 19136 19136 4419 0 -1 0 38716 0 0 0 81424 241 0 0 25 0 1 0 1846555226 159977472 38326 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19140/statm): 39057 38326 145 145 0 38912 0
[pid=19140] vsize: 156228
Current children cumulated CPU time (s) 816.67
Current children cumulated vsize (Kb) 158352

[startup+830.058 s]
Raw data (loadavg): 0.99 1.00 1.01 2/57 19140
Raw data (/proc/19136/stat): 19136 (minisat+_script) S 19135 19136 4419 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846555221 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19136/statm): 531 226 485 147 0 384 0
[pid=19136] vsize: 2124
Raw data (/proc/19140/stat): 19140 (minisat+_64-bit) R 19136 19136 4419 0 -1 0 38859 0 0 0 82422 242 0 0 25 0 1 0 1846555226 160555008 38469 4294967295 134512640 135094434 3221224432 3221221148 134563373 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19140/statm): 39198 38469 145 145 0 39053 0
[pid=19140] vsize: 156792
Current children cumulated CPU time (s) 826.66
Current children cumulated vsize (Kb) 158916

[startup+840.059 s]
Raw data (loadavg): 0.99 1.00 1.01 2/57 19140
Raw data (/proc/19136/stat): 19136 (minisat+_script) S 19135 19136 4419 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846555221 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19136/statm): 531 226 485 147 0 384 0
[pid=19136] vsize: 2124
Raw data (/proc/19140/stat): 19140 (minisat+_64-bit) R 19136 19136 4419 0 -1 0 38859 0 0 0 83422 242 0 0 25 0 1 0 1846555226 160555008 38469 4294967295 134512640 135094434 3221224432 3221223088 134558395 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19140/statm): 39198 38469 145 145 0 39053 0
[pid=19140] vsize: 156792
Current children cumulated CPU time (s) 836.66
Current children cumulated vsize (Kb) 158916

[startup+850.061 s]
Raw data (loadavg): 0.99 1.00 1.01 2/57 19140
Raw data (/proc/19136/stat): 19136 (minisat+_script) S 19135 19136 4419 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846555221 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19136/statm): 531 226 485 147 0 384 0
[pid=19136] vsize: 2124
Raw data (/proc/19140/stat): 19140 (minisat+_64-bit) R 19136 19136 4419 0 -1 0 38859 0 0 0 84422 242 0 0 25 0 1 0 1846555226 160555008 38469 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19140/statm): 39198 38469 145 145 0 39053 0
[pid=19140] vsize: 156792
Current children cumulated CPU time (s) 846.66
Current children cumulated vsize (Kb) 158916

[startup+860.061 s]
Raw data (loadavg): 0.99 1.00 1.01 2/57 19140
Raw data (/proc/19136/stat): 19136 (minisat+_script) S 19135 19136 4419 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846555221 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19136/statm): 531 226 485 147 0 384 0
[pid=19136] vsize: 2124
Raw data (/proc/19140/stat): 19140 (minisat+_64-bit) R 19136 19136 4419 0 -1 0 38859 0 0 0 85423 242 0 0 25 0 1 0 1846555226 160555008 38469 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19140/statm): 39198 38469 145 145 0 39053 0
[pid=19140] vsize: 156792
Current children cumulated CPU time (s) 856.67
Current children cumulated vsize (Kb) 158916

[startup+870.062 s]
Raw data (loadavg): 0.99 1.00 1.01 2/57 19140
Raw data (/proc/19136/stat): 19136 (minisat+_script) S 19135 19136 4419 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846555221 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19136/statm): 531 226 485 147 0 384 0
[pid=19136] vsize: 2124
Raw data (/proc/19140/stat): 19140 (minisat+_64-bit) R 19136 19136 4419 0 -1 0 38859 0 0 0 86423 242 0 0 25 0 1 0 1846555226 160555008 38469 4294967295 134512640 135094434 3221224432 3221223056 134562104 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19140/statm): 39198 38469 145 145 0 39053 0
[pid=19140] vsize: 156792
Current children cumulated CPU time (s) 866.67
Current children cumulated vsize (Kb) 158916

[startup+880.062 s]
Raw data (loadavg): 0.99 1.00 1.01 2/57 19140
Raw data (/proc/19136/stat): 19136 (minisat+_script) S 19135 19136 4419 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846555221 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19136/statm): 531 226 485 147 0 384 0
[pid=19136] vsize: 2124
Raw data (/proc/19140/stat): 19140 (minisat+_64-bit) R 19136 19136 4419 0 -1 0 38859 0 0 0 87423 242 0 0 25 0 1 0 1846555226 160555008 38469 4294967295 134512640 135094434 3221224432 3221223024 134557202 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19140/statm): 39198 38469 145 145 0 39053 0
[pid=19140] vsize: 156792
Current children cumulated CPU time (s) 876.67
Current children cumulated vsize (Kb) 158916

[startup+890.063 s]
Raw data (loadavg): 0.99 1.00 1.01 2/57 19140
Raw data (/proc/19136/stat): 19136 (minisat+_script) S 19135 19136 4419 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846555221 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19136/statm): 531 226 485 147 0 384 0
[pid=19136] vsize: 2124
Raw data (/proc/19140/stat): 19140 (minisat+_64-bit) R 19136 19136 4419 0 -1 0 38859 0 0 0 88423 243 0 0 25 0 1 0 1846555226 160555008 38469 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19140/statm): 39198 38469 145 145 0 39053 0
[pid=19140] vsize: 156792
Current children cumulated CPU time (s) 886.68
Current children cumulated vsize (Kb) 158916

[startup+900.064 s]
Raw data (loadavg): 0.99 1.00 1.01 2/57 19140
Raw data (/proc/19136/stat): 19136 (minisat+_script) S 19135 19136 4419 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846555221 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19136/statm): 531 226 485 147 0 384 0
[pid=19136] vsize: 2124
Raw data (/proc/19140/stat): 19140 (minisat+_64-bit) R 19136 19136 4419 0 -1 0 38859 0 0 0 89423 243 0 0 25 0 1 0 1846555226 160555008 38469 4294967295 134512640 135094434 3221224432 3221223024 134557133 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19140/statm): 39198 38469 145 145 0 39053 0
[pid=19140] vsize: 156792
Current children cumulated CPU time (s) 896.68
Current children cumulated vsize (Kb) 158916

[startup+910.064 s]
Raw data (loadavg): 0.99 1.00 1.00 2/57 19140
Raw data (/proc/19136/stat): 19136 (minisat+_script) S 19135 19136 4419 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846555221 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19136/statm): 531 226 485 147 0 384 0
[pid=19136] vsize: 2124
Raw data (/proc/19140/stat): 19140 (minisat+_64-bit) R 19136 19136 4419 0 -1 0 38859 0 0 0 90423 243 0 0 25 0 1 0 1846555226 160555008 38469 4294967295 134512640 135094434 3221224432 3221223024 134556862 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19140/statm): 39198 38469 145 145 0 39053 0
[pid=19140] vsize: 156792
Current children cumulated CPU time (s) 906.68
Current children cumulated vsize (Kb) 158916

[startup+920.065 s]
Raw data (loadavg): 0.99 1.00 1.00 2/57 19140
Raw data (/proc/19136/stat): 19136 (minisat+_script) S 19135 19136 4419 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846555221 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19136/statm): 531 226 485 147 0 384 0
[pid=19136] vsize: 2124
Raw data (/proc/19140/stat): 19140 (minisat+_64-bit) R 19136 19136 4419 0 -1 0 38859 0 0 0 91424 243 0 0 25 0 1 0 1846555226 160555008 38469 4294967295 134512640 135094434 3221224432 3221223092 134553499 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19140/statm): 39198 38469 145 145 0 39053 0
[pid=19140] vsize: 156792
Current children cumulated CPU time (s) 916.69
Current children cumulated vsize (Kb) 158916

[startup+930.065 s]
Raw data (loadavg): 0.99 1.00 1.00 2/57 19140
Raw data (/proc/19136/stat): 19136 (minisat+_script) S 19135 19136 4419 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846555221 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19136/statm): 531 226 485 147 0 384 0
[pid=19136] vsize: 2124
Raw data (/proc/19140/stat): 19140 (minisat+_64-bit) R 19136 19136 4419 0 -1 0 38859 0 0 0 92424 243 0 0 25 0 1 0 1846555226 160555008 38469 4294967295 134512640 135094434 3221224432 3221223044 134563046 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19140/statm): 39198 38469 145 145 0 39053 0
[pid=19140] vsize: 156792
Current children cumulated CPU time (s) 926.69
Current children cumulated vsize (Kb) 158916

[startup+940.065 s]
Raw data (loadavg): 0.99 1.00 1.00 2/57 19140
Raw data (/proc/19136/stat): 19136 (minisat+_script) S 19135 19136 4419 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846555221 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19136/statm): 531 226 485 147 0 384 0
[pid=19136] vsize: 2124
Raw data (/proc/19140/stat): 19140 (minisat+_64-bit) R 19136 19136 4419 0 -1 0 38859 0 0 0 93424 243 0 0 25 0 1 0 1846555226 160555008 38469 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19140/statm): 39198 38469 145 145 0 39053 0
[pid=19140] vsize: 156792
Current children cumulated CPU time (s) 936.69
Current children cumulated vsize (Kb) 158916

[startup+950.066 s]
Raw data (loadavg): 0.99 1.00 1.00 2/57 19140
Raw data (/proc/19136/stat): 19136 (minisat+_script) S 19135 19136 4419 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846555221 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19136/statm): 531 226 485 147 0 384 0
[pid=19136] vsize: 2124
Raw data (/proc/19140/stat): 19140 (minisat+_64-bit) R 19136 19136 4419 0 -1 0 38859 0 0 0 94424 243 0 0 25 0 1 0 1846555226 160555008 38469 4294967295 134512640 135094434 3221224432 3221223104 134556505 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19140/statm): 39198 38469 145 145 0 39053 0
[pid=19140] vsize: 156792
Current children cumulated CPU time (s) 946.69
Current children cumulated vsize (Kb) 158916

[startup+960.066 s]
Raw data (loadavg): 0.99 1.00 1.00 2/57 19140
Raw data (/proc/19136/stat): 19136 (minisat+_script) S 19135 19136 4419 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846555221 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19136/statm): 531 226 485 147 0 384 0
[pid=19136] vsize: 2124
Raw data (/proc/19140/stat): 19140 (minisat+_64-bit) R 19136 19136 4419 0 -1 0 38859 0 0 0 95424 243 0 0 25 0 1 0 1846555226 160555008 38469 4294967295 134512640 135094434 3221224432 3221223024 134556773 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19140/statm): 39198 38469 145 145 0 39053 0
[pid=19140] vsize: 156792
Current children cumulated CPU time (s) 956.69
Current children cumulated vsize (Kb) 158916

[startup+970.066 s]
Raw data (loadavg): 0.99 1.00 1.00 2/57 19140
Raw data (/proc/19136/stat): 19136 (minisat+_script) S 19135 19136 4419 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846555221 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19136/statm): 531 226 485 147 0 384 0
[pid=19136] vsize: 2124
Raw data (/proc/19140/stat): 19140 (minisat+_64-bit) R 19136 19136 4419 0 -1 0 38859 0 0 0 96424 243 0 0 25 0 1 0 1846555226 160555008 38469 4294967295 134512640 135094434 3221224432 3221223024 134557042 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19140/statm): 39198 38469 145 145 0 39053 0
[pid=19140] vsize: 156792
Current children cumulated CPU time (s) 966.69
Current children cumulated vsize (Kb) 158916

[startup+980.066 s]
Raw data (loadavg): 0.99 1.00 1.00 2/57 19140
Raw data (/proc/19136/stat): 19136 (minisat+_script) S 19135 19136 4419 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846555221 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19136/statm): 531 226 485 147 0 384 0
[pid=19136] vsize: 2124
Raw data (/proc/19140/stat): 19140 (minisat+_64-bit) R 19136 19136 4419 0 -1 0 38859 0 0 0 97424 243 0 0 25 0 1 0 1846555226 160555008 38469 4294967295 134512640 135094434 3221224432 3221223024 134556773 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19140/statm): 39198 38469 145 145 0 39053 0
[pid=19140] vsize: 156792
Current children cumulated CPU time (s) 976.69
Current children cumulated vsize (Kb) 158916

[startup+990.067 s]
Raw data (loadavg): 0.99 1.00 1.00 2/57 19140
Raw data (/proc/19136/stat): 19136 (minisat+_script) S 19135 19136 4419 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846555221 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19136/statm): 531 226 485 147 0 384 0
[pid=19136] vsize: 2124
Raw data (/proc/19140/stat): 19140 (minisat+_64-bit) R 19136 19136 4419 0 -1 0 38859 0 0 0 98425 243 0 0 25 0 1 0 1846555226 160555008 38469 4294967295 134512640 135094434 3221224432 3221223088 134557964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19140/statm): 39198 38469 145 145 0 39053 0
[pid=19140] vsize: 156792
Current children cumulated CPU time (s) 986.7
Current children cumulated vsize (Kb) 158916

[startup+1000.07 s]
Raw data (loadavg): 0.99 1.00 1.00 2/57 19140
Raw data (/proc/19136/stat): 19136 (minisat+_script) S 19135 19136 4419 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846555221 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19136/statm): 531 226 485 147 0 384 0
[pid=19136] vsize: 2124
Raw data (/proc/19140/stat): 19140 (minisat+_64-bit) R 19136 19136 4419 0 -1 0 38859 0 0 0 99425 243 0 0 25 0 1 0 1846555226 160555008 38469 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19140/statm): 39198 38469 145 145 0 39053 0
[pid=19140] vsize: 156792
Current children cumulated CPU time (s) 996.7
Current children cumulated vsize (Kb) 158916

[startup+1010.07 s]
Raw data (loadavg): 0.99 1.00 1.00 2/57 19140
Raw data (/proc/19136/stat): 19136 (minisat+_script) S 19135 19136 4419 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846555221 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19136/statm): 531 226 485 147 0 384 0
[pid=19136] vsize: 2124
Raw data (/proc/19140/stat): 19140 (minisat+_64-bit) R 19136 19136 4419 0 -1 0 38859 0 0 0 100425 243 0 0 25 0 1 0 1846555226 160555008 38469 4294967295 134512640 135094434 3221224432 3221223024 134556823 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19140/statm): 39198 38469 145 145 0 39053 0
[pid=19140] vsize: 156792
Current children cumulated CPU time (s) 1006.7
Current children cumulated vsize (Kb) 158916

[startup+1020.07 s]
Raw data (loadavg): 0.99 1.00 1.00 2/57 19140
Raw data (/proc/19136/stat): 19136 (minisat+_script) S 19135 19136 4419 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846555221 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19136/statm): 531 226 485 147 0 384 0
[pid=19136] vsize: 2124
Raw data (/proc/19140/stat): 19140 (minisat+_64-bit) R 19136 19136 4419 0 -1 0 38859 0 0 0 101425 243 0 0 25 0 1 0 1846555226 160555008 38469 4294967295 134512640 135094434 3221224432 3221223088 134557859 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19140/statm): 39198 38469 145 145 0 39053 0
[pid=19140] vsize: 156792
Current children cumulated CPU time (s) 1016.7
Current children cumulated vsize (Kb) 158916

[startup+1030.07 s]
Raw data (loadavg): 0.99 1.00 1.00 2/57 19140
Raw data (/proc/19136/stat): 19136 (minisat+_script) S 19135 19136 4419 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846555221 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19136/statm): 531 226 485 147 0 384 0
[pid=19136] vsize: 2124
Raw data (/proc/19140/stat): 19140 (minisat+_64-bit) R 19136 19136 4419 0 -1 0 38859 0 0 0 102425 243 0 0 25 0 1 0 1846555226 160555008 38469 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19140/statm): 39198 38469 145 145 0 39053 0
[pid=19140] vsize: 156792
Current children cumulated CPU time (s) 1026.7
Current children cumulated vsize (Kb) 158916

[startup+1040.07 s]
Raw data (loadavg): 0.99 1.00 1.00 2/57 19140
Raw data (/proc/19136/stat): 19136 (minisat+_script) S 19135 19136 4419 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846555221 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19136/statm): 531 226 485 147 0 384 0
[pid=19136] vsize: 2124
Raw data (/proc/19140/stat): 19140 (minisat+_64-bit) R 19136 19136 4419 0 -1 0 38859 0 0 0 103426 243 0 0 25 0 1 0 1846555226 160555008 38469 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19140/statm): 39198 38469 145 145 0 39053 0
[pid=19140] vsize: 156792
Current children cumulated CPU time (s) 1036.71
Current children cumulated vsize (Kb) 158916

[startup+1050.07 s]
Raw data (loadavg): 0.99 1.00 1.00 2/57 19140
Raw data (/proc/19136/stat): 19136 (minisat+_script) S 19135 19136 4419 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846555221 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19136/statm): 531 226 485 147 0 384 0
[pid=19136] vsize: 2124
Raw data (/proc/19140/stat): 19140 (minisat+_64-bit) R 19136 19136 4419 0 -1 0 38859 0 0 0 104425 243 0 0 25 0 1 0 1846555226 160555008 38469 4294967295 134512640 135094434 3221224432 3221223024 134556980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19140/statm): 39198 38469 145 145 0 39053 0
[pid=19140] vsize: 156792
Current children cumulated CPU time (s) 1046.7
Current children cumulated vsize (Kb) 158916

[startup+1060.07 s]
Raw data (loadavg): 0.99 1.00 1.00 2/57 19140
Raw data (/proc/19136/stat): 19136 (minisat+_script) S 19135 19136 4419 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846555221 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19136/statm): 531 226 485 147 0 384 0
[pid=19136] vsize: 2124
Raw data (/proc/19140/stat): 19140 (minisat+_64-bit) R 19136 19136 4419 0 -1 0 38859 0 0 0 105425 244 0 0 25 0 1 0 1846555226 160555008 38469 4294967295 134512640 135094434 3221224432 3221223024 134557407 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19140/statm): 39198 38469 145 145 0 39053 0
[pid=19140] vsize: 156792
Current children cumulated CPU time (s) 1056.71
Current children cumulated vsize (Kb) 158916

[startup+1070.07 s]
Raw data (loadavg): 0.99 1.00 1.00 2/57 19140
Raw data (/proc/19136/stat): 19136 (minisat+_script) S 19135 19136 4419 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846555221 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19136/statm): 531 226 485 147 0 384 0
[pid=19136] vsize: 2124
Raw data (/proc/19140/stat): 19140 (minisat+_64-bit) R 19136 19136 4419 0 -1 0 38859 0 0 0 106425 244 0 0 25 0 1 0 1846555226 160555008 38469 4294967295 134512640 135094434 3221224432 3221223024 134557416 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19140/statm): 39198 38469 145 145 0 39053 0
[pid=19140] vsize: 156792
Current children cumulated CPU time (s) 1066.71
Current children cumulated vsize (Kb) 158916

[startup+1080.07 s]
Raw data (loadavg): 0.99 1.00 1.00 2/57 19140
Raw data (/proc/19136/stat): 19136 (minisat+_script) S 19135 19136 4419 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846555221 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19136/statm): 531 226 485 147 0 384 0
[pid=19136] vsize: 2124
Raw data (/proc/19140/stat): 19140 (minisat+_64-bit) R 19136 19136 4419 0 -1 0 38859 0 0 0 107425 244 0 0 25 0 1 0 1846555226 160555008 38469 4294967295 134512640 135094434 3221224432 3221223024 134557512 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19140/statm): 39198 38469 145 145 0 39053 0
[pid=19140] vsize: 156792
Current children cumulated CPU time (s) 1076.71
Current children cumulated vsize (Kb) 158916

[startup+1090.07 s]
Raw data (loadavg): 0.99 1.00 1.00 2/57 19140
Raw data (/proc/19136/stat): 19136 (minisat+_script) S 19135 19136 4419 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846555221 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19136/statm): 531 226 485 147 0 384 0
[pid=19136] vsize: 2124
Raw data (/proc/19140/stat): 19140 (minisat+_64-bit) R 19136 19136 4419 0 -1 0 38859 0 0 0 108425 244 0 0 25 0 1 0 1846555226 160555008 38469 4294967295 134512640 135094434 3221224432 3221223024 134557028 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19140/statm): 39198 38469 145 145 0 39053 0
[pid=19140] vsize: 156792
Current children cumulated CPU time (s) 1086.71
Current children cumulated vsize (Kb) 158916

[startup+1100.07 s]
Raw data (loadavg): 0.99 1.00 1.00 2/57 19140
Raw data (/proc/19136/stat): 19136 (minisat+_script) S 19135 19136 4419 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846555221 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19136/statm): 531 226 485 147 0 384 0
[pid=19136] vsize: 2124
Raw data (/proc/19140/stat): 19140 (minisat+_64-bit) R 19136 19136 4419 0 -1 0 38859 0 0 0 109426 244 0 0 25 0 1 0 1846555226 160555008 38469 4294967295 134512640 135094434 3221224432 3221223072 134562108 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19140/statm): 39198 38469 145 145 0 39053 0
[pid=19140] vsize: 156792
Current children cumulated CPU time (s) 1096.72
Current children cumulated vsize (Kb) 158916

[startup+1110.07 s]
Raw data (loadavg): 0.99 1.00 1.00 2/57 19140
Raw data (/proc/19136/stat): 19136 (minisat+_script) S 19135 19136 4419 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846555221 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19136/statm): 531 226 485 147 0 384 0
[pid=19136] vsize: 2124
Raw data (/proc/19140/stat): 19140 (minisat+_64-bit) R 19136 19136 4419 0 -1 0 38859 0 0 0 110426 244 0 0 25 0 1 0 1846555226 160555008 38469 4294967295 134512640 135094434 3221224432 3221223056 134557669 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19140/statm): 39198 38469 145 145 0 39053 0
[pid=19140] vsize: 156792
Current children cumulated CPU time (s) 1106.72
Current children cumulated vsize (Kb) 158916

[startup+1120.07 s]
Raw data (loadavg): 0.99 1.00 1.00 2/57 19140
Raw data (/proc/19136/stat): 19136 (minisat+_script) S 19135 19136 4419 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846555221 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19136/statm): 531 226 485 147 0 384 0
[pid=19136] vsize: 2124
Raw data (/proc/19140/stat): 19140 (minisat+_64-bit) R 19136 19136 4419 0 -1 0 38859 0 0 0 111426 244 0 0 25 0 1 0 1846555226 160555008 38469 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19140/statm): 39198 38469 145 145 0 39053 0
[pid=19140] vsize: 156792
Current children cumulated CPU time (s) 1116.72
Current children cumulated vsize (Kb) 158916

[startup+1130.07 s]
Raw data (loadavg): 0.99 1.00 1.00 2/57 19140
Raw data (/proc/19136/stat): 19136 (minisat+_script) S 19135 19136 4419 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846555221 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19136/statm): 531 226 485 147 0 384 0
[pid=19136] vsize: 2124
Raw data (/proc/19140/stat): 19140 (minisat+_64-bit) R 19136 19136 4419 0 -1 0 38859 0 0 0 112426 244 0 0 25 0 1 0 1846555226 160555008 38469 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19140/statm): 39198 38469 145 145 0 39053 0
[pid=19140] vsize: 156792
Current children cumulated CPU time (s) 1126.72
Current children cumulated vsize (Kb) 158916

[startup+1140.07 s]
Raw data (loadavg): 0.99 1.00 1.00 2/57 19140
Raw data (/proc/19136/stat): 19136 (minisat+_script) S 19135 19136 4419 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846555221 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19136/statm): 531 226 485 147 0 384 0
[pid=19136] vsize: 2124
Raw data (/proc/19140/stat): 19140 (minisat+_64-bit) R 19136 19136 4419 0 -1 0 38859 0 0 0 113426 244 0 0 25 0 1 0 1846555226 160555008 38469 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19140/statm): 39198 38469 145 145 0 39053 0
[pid=19140] vsize: 156792
Current children cumulated CPU time (s) 1136.72
Current children cumulated vsize (Kb) 158916

[startup+1150.07 s]
Raw data (loadavg): 0.99 1.00 1.00 2/57 19140
Raw data (/proc/19136/stat): 19136 (minisat+_script) S 19135 19136 4419 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846555221 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19136/statm): 531 226 485 147 0 384 0
[pid=19136] vsize: 2124
Raw data (/proc/19140/stat): 19140 (minisat+_64-bit) R 19136 19136 4419 0 -1 0 38859 0 0 0 114427 244 0 0 25 0 1 0 1846555226 160555008 38469 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19140/statm): 39198 38469 145 145 0 39053 0
[pid=19140] vsize: 156792
Current children cumulated CPU time (s) 1146.73
Current children cumulated vsize (Kb) 158916

[startup+1160.08 s]
Raw data (loadavg): 0.99 1.00 1.00 2/57 19140
Raw data (/proc/19136/stat): 19136 (minisat+_script) S 19135 19136 4419 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846555221 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19136/statm): 531 226 485 147 0 384 0
[pid=19136] vsize: 2124
Raw data (/proc/19140/stat): 19140 (minisat+_64-bit) R 19136 19136 4419 0 -1 0 38859 0 0 0 115427 244 0 0 25 0 1 0 1846555226 160555008 38469 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19140/statm): 39198 38469 145 145 0 39053 0
[pid=19140] vsize: 156792
Current children cumulated CPU time (s) 1156.73
Current children cumulated vsize (Kb) 158916

[startup+1170.08 s]
Raw data (loadavg): 0.99 1.00 1.00 2/57 19140
Raw data (/proc/19136/stat): 19136 (minisat+_script) S 19135 19136 4419 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846555221 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19136/statm): 531 226 485 147 0 384 0
[pid=19136] vsize: 2124
Raw data (/proc/19140/stat): 19140 (minisat+_64-bit) R 19136 19136 4419 0 -1 0 38859 0 0 0 116427 244 0 0 25 0 1 0 1846555226 160555008 38469 4294967295 134512640 135094434 3221224432 3221223024 134556851 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19140/statm): 39198 38469 145 145 0 39053 0
[pid=19140] vsize: 156792
Current children cumulated CPU time (s) 1166.73
Current children cumulated vsize (Kb) 158916

[startup+1180.08 s]
Raw data (loadavg): 0.99 1.00 1.00 2/57 19140
Raw data (/proc/19136/stat): 19136 (minisat+_script) S 19135 19136 4419 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846555221 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19136/statm): 531 226 485 147 0 384 0
[pid=19136] vsize: 2124
Raw data (/proc/19140/stat): 19140 (minisat+_64-bit) R 19136 19136 4419 0 -1 0 38859 0 0 0 117427 244 0 0 25 0 1 0 1846555226 160555008 38469 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19140/statm): 39198 38469 145 145 0 39053 0
[pid=19140] vsize: 156792
Current children cumulated CPU time (s) 1176.73
Current children cumulated vsize (Kb) 158916

[startup+1190.08 s]
Raw data (loadavg): 0.99 1.00 1.00 2/57 19140
Raw data (/proc/19136/stat): 19136 (minisat+_script) S 19135 19136 4419 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846555221 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19136/statm): 531 226 485 147 0 384 0
[pid=19136] vsize: 2124
Raw data (/proc/19140/stat): 19140 (minisat+_64-bit) R 19136 19136 4419 0 -1 0 38859 0 0 0 118427 244 0 0 25 0 1 0 1846555226 160555008 38469 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19140/statm): 39198 38469 145 145 0 39053 0
[pid=19140] vsize: 156792
Current children cumulated CPU time (s) 1186.73
Current children cumulated vsize (Kb) 158916

[startup+1200.08 s]
Raw data (loadavg): 0.99 1.00 1.00 2/57 19140
Raw data (/proc/19136/stat): 19136 (minisat+_script) S 19135 19136 4419 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846555221 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19136/statm): 531 226 485 147 0 384 0
[pid=19136] vsize: 2124
Raw data (/proc/19140/stat): 19140 (minisat+_64-bit) R 19136 19136 4419 0 -1 0 38859 0 0 0 119428 244 0 0 25 0 1 0 1846555226 160555008 38469 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19140/statm): 39198 38469 145 145 0 39053 0
[pid=19140] vsize: 156792
Current children cumulated CPU time (s) 1196.74
Current children cumulated vsize (Kb) 158916

[startup+1210.08 s]
Raw data (loadavg): 0.99 1.00 1.00 2/57 19140
Raw data (/proc/19136/stat): 19136 (minisat+_script) S 19135 19136 4419 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846555221 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19136/statm): 531 226 485 147 0 384 0
[pid=19136] vsize: 2124
Raw data (/proc/19140/stat): 19140 (minisat+_64-bit) R 19136 19136 4419 0 -1 0 38859 0 0 0 120428 244 0 0 25 0 1 0 1846555226 160555008 38469 4294967295 134512640 135094434 3221224432 3221223024 134556699 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19140/statm): 39198 38469 145 145 0 39053 0
[pid=19140] vsize: 156792
Current children cumulated CPU time (s) 1206.74
Current children cumulated vsize (Kb) 158916



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.08 s]
Raw data (loadavg): 0.99 1.00 1.00 2/57 19140
Raw data (/proc/19136/stat): 19136 (minisat+_script) S 19135 19136 4419 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846555221 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19136/statm): 531 226 485 147 0 384 0
[pid=19136] vsize: 2124
Raw data (/proc/19140/stat): 19140 (minisat+_64-bit) R 19136 19136 4419 0 -1 0 38859 0 0 0 120428 244 0 0 25 0 1 0 1846555226 160555008 38469 4294967295 134512640 135094434 3221224432 3221223024 134557528 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19140/statm): 39198 38469 145 145 0 39053 0
[pid=19140] vsize: 156792
Current children cumulated CPU time (s) 1206.74
Current children cumulated vsize (Kb) 158916

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

Child status: 0
Real time (s): 1210.15
CPU time (s): 1206.8
CPU user time (s): 1204.28
CPU system time (s): 2.51662
CPU usage (%): 99.723
Max. virtual memory (cumulated for all children) (Kb): 158916

Verifier Data

ERROR: no interpretation found !