Some explanations

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

General information on the benchmark

Namemps-v2-13-7/MIPLIB/miplib/normalized-mps-v2-13-7-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.32
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 6091

Launcher Data

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        891972 kB
Buffers:         23012 kB
Cached:          90500 kB
SwapCached:        660 kB
Active:          28264 kB
Inactive:        87772 kB
HighTotal:      131008 kB
HighFree:        36904 kB
LowTotal:       903652 kB
LowFree:        855068 kB
SwapTotal:     2097640 kB
SwapFree:      2096408 kB
Dirty:               4 kB
Writeback:           0 kB
Mapped:           5816 kB
Slab:            20944 kB
Committed_AS:    64128 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-09-20 03:31:25 (client local time) WITH STATUS 0 IN 1206.8 SECONDS
stats: 3243 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/20773/stat): 20773 (minisat+_script) R 20772 20773 20115 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1855205456 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 0 0 0
Raw data (/proc/20773/statm): 174 3 169 147 0 27 0
[pid=20773] 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=20774
New process pid=20775
New process pid=20776
execve syscall for /bin/sed executable
One traced child (pid=20775) 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=20776) exited with status: 0
One traced child (pid=20774) exited with status: 0
New process pid=20777
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc28/normalized-mps-v2-13-7-l152lav.opb

[startup+10.0039 s]
Raw data (loadavg): 0.82 0.91 0.72 2/57 20777
Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20773/statm): 531 226 485 147 0 384 0
[pid=20773] vsize: 2124
Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 4205 0 0 0 963 17 0 0 25 0 1 0 1855205461 18108416 3815 4294967295 134512640 135094434 3221224432 3221223024 134557137 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20777/statm): 4421 3815 145 145 0 4276 0
[pid=20777] vsize: 17684
Current children cumulated CPU time (s) 9.81
Current children cumulated vsize (Kb) 19808

[startup+20.0046 s]
Raw data (loadavg): 0.84 0.91 0.73 2/57 20777
Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20773/statm): 531 226 485 147 0 384 0
[pid=20773] vsize: 2124
Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 4576 0 0 0 1957 19 0 0 25 0 1 0 1855205461 19632128 4186 4294967295 134512640 135094434 3221224432 3221223088 134561717 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20777/statm): 4793 4186 145 145 0 4648 0
[pid=20777] vsize: 19172
Current children cumulated CPU time (s) 19.77
Current children cumulated vsize (Kb) 21296

[startup+30.0053 s]
Raw data (loadavg): 0.87 0.92 0.73 2/57 20777
Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20773/statm): 531 226 485 147 0 384 0
[pid=20773] vsize: 2124
Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 4727 0 0 0 2955 20 0 0 25 0 1 0 1855205461 20275200 4337 4294967295 134512640 135094434 3221224432 3221223088 134558218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20777/statm): 4950 4337 145 145 0 4805 0
[pid=20777] vsize: 19800
Current children cumulated CPU time (s) 29.76
Current children cumulated vsize (Kb) 21924

[startup+40.0069 s]
Raw data (loadavg): 0.89 0.92 0.73 2/57 20777
Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20773/statm): 531 226 485 147 0 384 0
[pid=20773] vsize: 2124
Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 4846 0 0 0 3952 22 0 0 25 0 1 0 1855205461 20750336 4456 4294967295 134512640 135094434 3221224432 3221223128 134558980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20777/statm): 5066 4456 145 145 0 4921 0
[pid=20777] vsize: 20264
Current children cumulated CPU time (s) 39.75
Current children cumulated vsize (Kb) 22388

[startup+50.0076 s]
Raw data (loadavg): 0.90 0.92 0.73 2/57 20777
Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20773/statm): 531 226 485 147 0 384 0
[pid=20773] vsize: 2124
Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 5072 0 0 0 4948 24 0 0 25 0 1 0 1855205461 21659648 4682 4294967295 134512640 135094434 3221224432 3221222976 134779242 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20777/statm): 5288 4682 145 145 0 5143 0
[pid=20777] vsize: 21152
Current children cumulated CPU time (s) 49.73
Current children cumulated vsize (Kb) 23276

[startup+60.0083 s]
Raw data (loadavg): 0.92 0.92 0.74 2/57 20777
Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20773/statm): 531 226 485 147 0 384 0
[pid=20773] vsize: 2124
Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 5447 0 0 0 5941 27 0 0 25 0 1 0 1855205461 23240704 5057 4294967295 134512640 135094434 3221224432 3221223024 134556884 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20777/statm): 5674 5057 145 145 0 5529 0
[pid=20777] vsize: 22696
Current children cumulated CPU time (s) 59.69
Current children cumulated vsize (Kb) 24820

[startup+70.0089 s]
Raw data (loadavg): 0.93 0.92 0.74 2/57 20777
Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20773/statm): 531 226 485 147 0 384 0
[pid=20773] vsize: 2124
Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 5824 0 0 0 6934 31 0 0 25 0 1 0 1855205461 24772608 5434 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20777/statm): 6048 5434 145 145 0 5903 0
[pid=20777] vsize: 24192
Current children cumulated CPU time (s) 69.66
Current children cumulated vsize (Kb) 26316

[startup+80.0096 s]
Raw data (loadavg): 0.94 0.93 0.74 2/57 20777
Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20773/statm): 531 226 485 147 0 384 0
[pid=20773] vsize: 2124
Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 6132 0 0 0 7929 33 0 0 25 0 1 0 1855205461 26017792 5742 4294967295 134512640 135094434 3221224432 3221223092 134553499 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20777/statm): 6352 5742 145 145 0 6207 0
[pid=20777] vsize: 25408
Current children cumulated CPU time (s) 79.63
Current children cumulated vsize (Kb) 27532

[startup+90.0103 s]
Raw data (loadavg): 0.95 0.93 0.74 2/57 20777
Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20773/statm): 531 226 485 147 0 384 0
[pid=20773] vsize: 2124
Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 6571 0 0 0 8922 36 0 0 25 0 1 0 1855205461 27803648 6181 4294967295 134512640 135094434 3221224432 3221223056 134562085 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20777/statm): 6788 6181 145 145 0 6643 0
[pid=20777] vsize: 27152
Current children cumulated CPU time (s) 89.59
Current children cumulated vsize (Kb) 29276

[startup+100.011 s]
Raw data (loadavg): 0.96 0.93 0.74 2/57 20777
Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20773/statm): 531 226 485 147 0 384 0
[pid=20773] vsize: 2124
Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 7239 0 0 0 9912 40 0 0 25 0 1 0 1855205461 30535680 6849 4294967295 134512640 135094434 3221224432 3221223088 134558181 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20777/statm): 7455 6849 145 145 0 7310 0
[pid=20777] vsize: 29820
Current children cumulated CPU time (s) 99.53
Current children cumulated vsize (Kb) 31944

[startup+110.012 s]
Raw data (loadavg): 0.96 0.93 0.75 2/57 20777
Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20773/statm): 531 226 485 147 0 384 0
[pid=20773] vsize: 2124
Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 7499 0 0 0 10908 42 0 0 25 0 1 0 1855205461 31719424 7109 4294967295 134512640 135094434 3221224432 3221223088 134558126 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20777/statm): 7744 7109 145 145 0 7599 0
[pid=20777] vsize: 30976
Current children cumulated CPU time (s) 109.51
Current children cumulated vsize (Kb) 33100

[startup+120.012 s]
Raw data (loadavg): 0.97 0.93 0.75 2/57 20777
Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20773/statm): 531 226 485 147 0 384 0
[pid=20773] vsize: 2124
Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 7978 0 0 0 11899 47 0 0 25 0 1 0 1855205461 33669120 7588 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20777/statm): 8220 7588 145 145 0 8075 0
[pid=20777] vsize: 32880
Current children cumulated CPU time (s) 119.47
Current children cumulated vsize (Kb) 35004

[startup+130.013 s]
Raw data (loadavg): 0.97 0.94 0.75 2/57 20777
Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20773/statm): 531 226 485 147 0 384 0
[pid=20773] vsize: 2124
Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 8358 0 0 0 12893 49 0 0 25 0 1 0 1855205461 35213312 7968 4294967295 134512640 135094434 3221224432 3221223024 134556996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20777/statm): 8597 7968 145 145 0 8452 0
[pid=20777] vsize: 34388
Current children cumulated CPU time (s) 129.43
Current children cumulated vsize (Kb) 36512

[startup+140.014 s]
Raw data (loadavg): 0.98 0.94 0.75 2/57 20777
Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20773/statm): 531 226 485 147 0 384 0
[pid=20773] vsize: 2124
Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 8913 0 0 0 13883 52 0 0 25 0 1 0 1855205461 37478400 8523 4294967295 134512640 135094434 3221224432 3221223024 134556802 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20777/statm): 9150 8523 145 145 0 9005 0
[pid=20777] vsize: 36600
Current children cumulated CPU time (s) 139.36
Current children cumulated vsize (Kb) 38724

[startup+150.014 s]
Raw data (loadavg): 0.98 0.94 0.75 2/57 20777
Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20773/statm): 531 226 485 147 0 384 0
[pid=20773] vsize: 2124
Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 9483 0 0 0 14874 56 0 0 25 0 1 0 1855205461 39800832 9093 4294967295 134512640 135094434 3221224432 3221223024 134557025 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20777/statm): 9717 9093 145 145 0 9572 0
[pid=20777] vsize: 38868
Current children cumulated CPU time (s) 149.31
Current children cumulated vsize (Kb) 40992

[startup+160.015 s]
Raw data (loadavg): 0.98 0.94 0.76 2/57 20777
Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20773/statm): 531 226 485 147 0 384 0
[pid=20773] vsize: 2124
Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 10031 0 0 0 15863 60 0 0 25 0 1 0 1855205461 42041344 9641 4294967295 134512640 135094434 3221224432 3221223104 134556073 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20777/statm): 10264 9641 145 145 0 10119 0
[pid=20777] vsize: 41056
Current children cumulated CPU time (s) 159.24
Current children cumulated vsize (Kb) 43180

[startup+170.016 s]
Raw data (loadavg): 0.98 0.94 0.76 2/57 20777
Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20773/statm): 531 226 485 147 0 384 0
[pid=20773] vsize: 2124
Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 10532 0 0 0 16856 63 0 0 25 0 1 0 1855205461 44085248 10142 4294967295 134512640 135094434 3221224432 3221223088 134557896 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20777/statm): 10763 10142 145 145 0 10618 0
[pid=20777] vsize: 43052
Current children cumulated CPU time (s) 169.2
Current children cumulated vsize (Kb) 45176

[startup+180.015 s]
Raw data (loadavg): 0.99 0.94 0.76 2/57 20777
Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20773/statm): 531 226 485 147 0 384 0
[pid=20773] vsize: 2124
Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 11020 0 0 0 17849 65 0 0 25 0 1 0 1855205461 46080000 10630 4294967295 134512640 135094434 3221224432 3221223024 134557273 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20777/statm): 11250 10630 145 145 0 11105 0
[pid=20777] vsize: 45000
Current children cumulated CPU time (s) 179.15
Current children cumulated vsize (Kb) 47124

[startup+190.016 s]
Raw data (loadavg): 0.99 0.94 0.76 2/57 20777
Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20773/statm): 531 226 485 147 0 384 0
[pid=20773] vsize: 2124
Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 11483 0 0 0 18842 68 0 0 25 0 1 0 1855205461 47972352 11093 4294967295 134512640 135094434 3221224432 3221223024 134557512 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20777/statm): 11712 11093 145 145 0 11567 0
[pid=20777] vsize: 46848
Current children cumulated CPU time (s) 189.11
Current children cumulated vsize (Kb) 48972

[startup+200.017 s]
Raw data (loadavg): 0.99 0.95 0.76 2/57 20777
Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20773/statm): 531 226 485 147 0 384 0
[pid=20773] vsize: 2124
Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 11901 0 0 0 19836 71 0 0 25 0 1 0 1855205461 49684480 11511 4294967295 134512640 135094434 3221224432 3221223024 134556978 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20777/statm): 12130 11511 145 145 0 11985 0
[pid=20777] vsize: 48520
Current children cumulated CPU time (s) 199.08
Current children cumulated vsize (Kb) 50644

[startup+210.017 s]
Raw data (loadavg): 0.99 0.95 0.77 2/57 20777
Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20773/statm): 531 226 485 147 0 384 0
[pid=20773] vsize: 2124
Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 12278 0 0 0 20831 73 0 0 25 0 1 0 1855205461 51240960 11888 4294967295 134512640 135094434 3221224432 3221223024 134557514 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20777/statm): 12510 11888 145 145 0 12365 0
[pid=20777] vsize: 50040
Current children cumulated CPU time (s) 209.05
Current children cumulated vsize (Kb) 52164

[startup+220.018 s]
Raw data (loadavg): 0.99 0.95 0.77 2/57 20777
Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20773/statm): 531 226 485 147 0 384 0
[pid=20773] vsize: 2124
Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 12592 0 0 0 21825 75 0 0 25 0 1 0 1855205461 52523008 12202 4294967295 134512640 135094434 3221224432 3221223024 134557273 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20777/statm): 12823 12202 145 145 0 12678 0
[pid=20777] vsize: 51292
Current children cumulated CPU time (s) 219.01
Current children cumulated vsize (Kb) 53416

[startup+230.018 s]
Raw data (loadavg): 0.99 0.95 0.77 2/57 20777
Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20773/statm): 531 226 485 147 0 384 0
[pid=20773] vsize: 2124
Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 12903 0 0 0 22822 76 0 0 25 0 1 0 1855205461 53792768 12513 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20777/statm): 13133 12513 145 145 0 12988 0
[pid=20777] vsize: 52532
Current children cumulated CPU time (s) 228.99
Current children cumulated vsize (Kb) 54656

[startup+240.018 s]
Raw data (loadavg): 0.99 0.95 0.77 2/57 20777
Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20773/statm): 531 226 485 147 0 384 0
[pid=20773] vsize: 2124
Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 13208 0 0 0 23818 78 0 0 25 0 1 0 1855205461 55037952 12818 4294967295 134512640 135094434 3221224432 3221223024 134557248 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20777/statm): 13437 12818 145 145 0 13292 0
[pid=20777] vsize: 53748
Current children cumulated CPU time (s) 238.97
Current children cumulated vsize (Kb) 55872

[startup+250.019 s]
Raw data (loadavg): 0.99 0.95 0.77 2/57 20777
Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20773/statm): 531 226 485 147 0 384 0
[pid=20773] vsize: 2124
Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 13597 0 0 0 24812 81 0 0 25 0 1 0 1855205461 56619008 13207 4294967295 134512640 135094434 3221224432 3221223024 134556862 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20777/statm): 13823 13207 145 145 0 13678 0
[pid=20777] vsize: 55292
Current children cumulated CPU time (s) 248.94
Current children cumulated vsize (Kb) 57416

[startup+260.02 s]
Raw data (loadavg): 1.06 0.97 0.78 2/57 20777
Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20773/statm): 531 226 485 147 0 384 0
[pid=20773] vsize: 2124
Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 14042 0 0 0 25805 84 0 0 25 0 1 0 1855205461 58445824 13652 4294967295 134512640 135094434 3221224432 3221223024 134556964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20777/statm): 14269 13652 145 145 0 14124 0
[pid=20777] vsize: 57076
Current children cumulated CPU time (s) 258.9
Current children cumulated vsize (Kb) 59200

[startup+270.02 s]
Raw data (loadavg): 1.05 0.97 0.78 2/57 20777
Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20773/statm): 531 226 485 147 0 384 0
[pid=20773] vsize: 2124
Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 14475 0 0 0 26798 87 0 0 25 0 1 0 1855205461 60211200 14085 4294967295 134512640 135094434 3221224432 3221223024 134557512 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20777/statm): 14700 14085 145 145 0 14555 0
[pid=20777] vsize: 58800
Current children cumulated CPU time (s) 268.86
Current children cumulated vsize (Kb) 60924

[startup+280.021 s]
Raw data (loadavg): 1.04 0.97 0.79 2/57 20777
Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20773/statm): 531 226 485 147 0 384 0
[pid=20773] vsize: 2124
Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 14939 0 0 0 27791 90 0 0 25 0 1 0 1855205461 62103552 14549 4294967295 134512640 135094434 3221224432 3221223092 134553499 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20777/statm): 15162 14549 145 145 0 15017 0
[pid=20777] vsize: 60648
Current children cumulated CPU time (s) 278.82
Current children cumulated vsize (Kb) 62772

[startup+290.022 s]
Raw data (loadavg): 1.04 0.97 0.79 2/57 20777
Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20773/statm): 531 226 485 147 0 384 0
[pid=20773] vsize: 2124
Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 15338 0 0 0 28785 92 0 0 25 0 1 0 1855205461 63725568 14948 4294967295 134512640 135094434 3221224432 3221223024 134557004 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20777/statm): 15558 14948 145 145 0 15413 0
[pid=20777] vsize: 62232
Current children cumulated CPU time (s) 288.78
Current children cumulated vsize (Kb) 64356

[startup+300.022 s]
Raw data (loadavg): 1.03 0.97 0.79 2/57 20777
Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20773/statm): 531 226 485 147 0 384 0
[pid=20773] vsize: 2124
Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 15807 0 0 0 29777 95 0 0 25 0 1 0 1855205461 65642496 15417 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20777/statm): 16026 15417 145 145 0 15881 0
[pid=20777] vsize: 64104
Current children cumulated CPU time (s) 298.73
Current children cumulated vsize (Kb) 66228

[startup+310.024 s]
Raw data (loadavg): 1.03 0.97 0.79 2/57 20777
Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20773/statm): 531 226 485 147 0 384 0
[pid=20773] vsize: 2124
Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 16256 0 0 0 30770 98 0 0 25 0 1 0 1855205461 67735552 15866 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20777/statm): 16537 15866 145 145 0 16392 0
[pid=20777] vsize: 66148
Current children cumulated CPU time (s) 308.69
Current children cumulated vsize (Kb) 68272

[startup+320.025 s]
Raw data (loadavg): 1.02 0.97 0.79 2/57 20777
Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20773/statm): 531 226 485 147 0 384 0
[pid=20773] vsize: 2124
Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 16585 0 0 0 31764 100 0 0 25 0 1 0 1855205461 69074944 16195 4294967295 134512640 135094434 3221224432 3221223024 134556812 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20777/statm): 16864 16195 145 145 0 16719 0
[pid=20777] vsize: 67456
Current children cumulated CPU time (s) 318.65
Current children cumulated vsize (Kb) 69580

[startup+330.026 s]
Raw data (loadavg): 1.02 0.97 0.79 2/57 20777
Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20773/statm): 531 226 485 147 0 384 0
[pid=20773] vsize: 2124
Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) T 20773 20773 20115 0 -1 0 16943 0 0 0 32757 104 0 0 25 0 1 0 1855205461 70533120 16553 4294967295 134512640 135094434 3221224432 3221222796 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/20777/statm): 17220 16553 145 145 0 17075 0
[pid=20777] vsize: 68880
Current children cumulated CPU time (s) 328.62
Current children cumulated vsize (Kb) 71004

[startup+340.026 s]
Raw data (loadavg): 1.01 0.97 0.80 2/57 20777
Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20773/statm): 531 226 485 147 0 384 0
[pid=20773] vsize: 2124
Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 17458 0 0 0 33749 108 0 0 25 0 1 0 1855205461 72634368 17068 4294967295 134512640 135094434 3221224432 3221223088 134558235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20777/statm): 17733 17068 145 145 0 17588 0
[pid=20777] vsize: 70932
Current children cumulated CPU time (s) 338.58
Current children cumulated vsize (Kb) 73056

[startup+350.027 s]
Raw data (loadavg): 1.01 0.97 0.80 2/57 20777
Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20773/statm): 531 226 485 147 0 384 0
[pid=20773] vsize: 2124
Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 17917 0 0 0 34742 112 0 0 25 0 1 0 1855205461 74506240 17527 4294967295 134512640 135094434 3221224432 3221223088 134558004 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20777/statm): 18190 17527 145 145 0 18045 0
[pid=20777] vsize: 72760
Current children cumulated CPU time (s) 348.55
Current children cumulated vsize (Kb) 74884

[startup+360.028 s]
Raw data (loadavg): 1.01 0.97 0.80 2/57 20777
Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20773/statm): 531 226 485 147 0 384 0
[pid=20773] vsize: 2124
Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 18426 0 0 0 35734 114 0 0 25 0 1 0 1855205461 76587008 18036 4294967295 134512640 135094434 3221224432 3221223024 134557119 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20777/statm): 18698 18036 145 145 0 18553 0
[pid=20777] vsize: 74792
Current children cumulated CPU time (s) 358.49
Current children cumulated vsize (Kb) 76916

[startup+370.028 s]
Raw data (loadavg): 1.01 0.97 0.80 2/57 20777
Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20773/statm): 531 226 485 147 0 384 0
[pid=20773] vsize: 2124
Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 18852 0 0 0 36728 117 0 0 25 0 1 0 1855205461 78323712 18462 4294967295 134512640 135094434 3221224432 3221223024 134556802 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20777/statm): 19122 18462 145 145 0 18977 0
[pid=20777] vsize: 76488
Current children cumulated CPU time (s) 368.46
Current children cumulated vsize (Kb) 78612

[startup+380.028 s]
Raw data (loadavg): 1.01 0.97 0.80 2/57 20777
Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20773/statm): 531 226 485 147 0 384 0
[pid=20773] vsize: 2124
Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 19325 0 0 0 37721 120 0 0 25 0 1 0 1855205461 80252928 18935 4294967295 134512640 135094434 3221224432 3221223092 134553499 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20777/statm): 19593 18935 145 145 0 19448 0
[pid=20777] vsize: 78372
Current children cumulated CPU time (s) 378.42
Current children cumulated vsize (Kb) 80496

[startup+390.029 s]
Raw data (loadavg): 1.00 0.97 0.81 2/57 20777
Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20773/statm): 531 226 485 147 0 384 0
[pid=20773] vsize: 2124
Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 19768 0 0 0 38713 123 0 0 25 0 1 0 1855205461 82059264 19378 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20777/statm): 20034 19378 145 145 0 19889 0
[pid=20777] vsize: 80136
Current children cumulated CPU time (s) 388.37
Current children cumulated vsize (Kb) 82260

[startup+400.029 s]
Raw data (loadavg): 1.00 0.97 0.81 2/57 20777
Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20773/statm): 531 226 485 147 0 384 0
[pid=20773] vsize: 2124
Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 20213 0 0 0 39705 125 0 0 25 0 1 0 1855205461 83877888 19823 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20777/statm): 20478 19823 145 145 0 20333 0
[pid=20777] vsize: 81912
Current children cumulated CPU time (s) 398.31
Current children cumulated vsize (Kb) 84036

[startup+410.03 s]
Raw data (loadavg): 1.00 0.97 0.81 2/57 20777
Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20773/statm): 531 226 485 147 0 384 0
[pid=20773] vsize: 2124
Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 20649 0 0 0 40698 128 0 0 25 0 1 0 1855205461 85655552 20259 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20777/statm): 20912 20259 145 145 0 20767 0
[pid=20777] vsize: 83648
Current children cumulated CPU time (s) 408.27
Current children cumulated vsize (Kb) 85772

[startup+420.031 s]
Raw data (loadavg): 1.00 0.97 0.81 2/57 20777
Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20773/statm): 531 226 485 147 0 384 0
[pid=20773] vsize: 2124
Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 21015 0 0 0 41692 131 0 0 25 0 1 0 1855205461 87146496 20625 4294967295 134512640 135094434 3221224432 3221223024 134556966 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20777/statm): 21276 20625 145 145 0 21131 0
[pid=20777] vsize: 85104
Current children cumulated CPU time (s) 418.24
Current children cumulated vsize (Kb) 87228

[startup+430.031 s]
Raw data (loadavg): 1.00 0.97 0.81 2/57 20777
Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20773/statm): 531 226 485 147 0 384 0
[pid=20773] vsize: 2124
Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 21394 0 0 0 42683 134 0 0 25 0 1 0 1855205461 88690688 21004 4294967295 134512640 135094434 3221224432 3221223088 134558395 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20777/statm): 21653 21004 145 145 0 21508 0
[pid=20777] vsize: 86612
Current children cumulated CPU time (s) 428.18
Current children cumulated vsize (Kb) 88736

[startup+440.032 s]
Raw data (loadavg): 1.00 0.97 0.82 2/57 20777
Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20773/statm): 531 226 485 147 0 384 0
[pid=20773] vsize: 2124
Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 21856 0 0 0 43674 139 0 0 25 0 1 0 1855205461 90574848 21466 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20777/statm): 22113 21466 145 145 0 21968 0
[pid=20777] vsize: 88452
Current children cumulated CPU time (s) 438.14
Current children cumulated vsize (Kb) 90576

[startup+450.033 s]
Raw data (loadavg): 1.00 0.97 0.82 2/57 20777
Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20773/statm): 531 226 485 147 0 384 0
[pid=20773] vsize: 2124
Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 22372 0 0 0 44667 141 0 0 25 0 1 0 1855205461 92684288 21982 4294967295 134512640 135094434 3221224432 3221223024 134556933 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20777/statm): 22628 21982 145 145 0 22483 0
[pid=20777] vsize: 90512
Current children cumulated CPU time (s) 448.09
Current children cumulated vsize (Kb) 92636

[startup+460.033 s]
Raw data (loadavg): 1.00 0.97 0.82 2/57 20777
Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20773/statm): 531 226 485 147 0 384 0
[pid=20773] vsize: 2124
Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 22901 0 0 0 45660 144 0 0 25 0 1 0 1855205461 94851072 22511 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20777/statm): 23157 22511 145 145 0 23012 0
[pid=20777] vsize: 92628
Current children cumulated CPU time (s) 458.05
Current children cumulated vsize (Kb) 94752

[startup+470.034 s]
Raw data (loadavg): 1.00 0.97 0.82 2/57 20777
Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20773/statm): 531 226 485 147 0 384 0
[pid=20773] vsize: 2124
Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 23415 0 0 0 46652 148 0 0 25 0 1 0 1855205461 96956416 23025 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20777/statm): 23671 23025 145 145 0 23526 0
[pid=20777] vsize: 94684
Current children cumulated CPU time (s) 468.01
Current children cumulated vsize (Kb) 96808

[startup+480.034 s]
Raw data (loadavg): 1.00 0.97 0.82 2/57 20777
Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20773/statm): 531 226 485 147 0 384 0
[pid=20773] vsize: 2124
Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 23824 0 0 0 47646 150 0 0 25 0 1 0 1855205461 98623488 23434 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20777/statm): 24078 23434 145 145 0 23933 0
[pid=20777] vsize: 96312
Current children cumulated CPU time (s) 477.97
Current children cumulated vsize (Kb) 98436

[startup+490.034 s]
Raw data (loadavg): 1.00 0.97 0.82 2/57 20777
Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20773/statm): 531 226 485 147 0 384 0
[pid=20773] vsize: 2124
Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 24200 0 0 0 48641 153 0 0 25 0 1 0 1855205461 100159488 23810 4294967295 134512640 135094434 3221224432 3221223024 134557131 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20777/statm): 24453 23810 145 145 0 24308 0
[pid=20777] vsize: 97812
Current children cumulated CPU time (s) 487.95
Current children cumulated vsize (Kb) 99936

[startup+500.035 s]
Raw data (loadavg): 1.00 0.97 0.82 2/57 20777
Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20773/statm): 531 226 485 147 0 384 0
[pid=20773] vsize: 2124
Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 24469 0 0 0 49636 156 0 0 23 0 1 0 1855205461 101253120 24079 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20777/statm): 24720 24079 145 145 0 24575 0
[pid=20777] vsize: 98880
Current children cumulated CPU time (s) 497.93
Current children cumulated vsize (Kb) 101004

[startup+510.037 s]
Raw data (loadavg): 1.00 0.97 0.82 2/57 20777
Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20773/statm): 531 226 485 147 0 384 0
[pid=20773] vsize: 2124
Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 24870 0 0 0 50629 158 0 0 25 0 1 0 1855205461 102887424 24480 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20777/statm): 25119 24480 145 145 0 24974 0
[pid=20777] vsize: 100476
Current children cumulated CPU time (s) 507.88
Current children cumulated vsize (Kb) 102600

[startup+520.037 s]
Raw data (loadavg): 1.00 0.97 0.83 2/57 20777
Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20773/statm): 531 226 485 147 0 384 0
[pid=20773] vsize: 2124
Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 25325 0 0 0 51622 162 0 0 25 0 1 0 1855205461 104747008 24935 4294967295 134512640 135094434 3221224432 3221223024 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20777/statm): 25573 24935 145 145 0 25428 0
[pid=20777] vsize: 102292
Current children cumulated CPU time (s) 517.85
Current children cumulated vsize (Kb) 104416

[startup+530.038 s]
Raw data (loadavg): 1.00 0.97 0.83 2/57 20777
Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20773/statm): 531 226 485 147 0 384 0
[pid=20773] vsize: 2124
Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 25828 0 0 0 52614 165 0 0 25 0 1 0 1855205461 106803200 25438 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20777/statm): 26075 25438 145 145 0 25930 0
[pid=20777] vsize: 104300
Current children cumulated CPU time (s) 527.8
Current children cumulated vsize (Kb) 106424

[startup+540.039 s]
Raw data (loadavg): 1.00 0.97 0.83 2/57 20777
Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20773/statm): 531 226 485 147 0 384 0
[pid=20773] vsize: 2124
Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 26241 0 0 0 53606 168 0 0 25 0 1 0 1855205461 108486656 25851 4294967295 134512640 135094434 3221224432 3221222912 134780857 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20777/statm): 26486 25851 145 145 0 26341 0
[pid=20777] vsize: 105944
Current children cumulated CPU time (s) 537.75
Current children cumulated vsize (Kb) 108068

[startup+550.039 s]
Raw data (loadavg): 1.00 0.97 0.83 2/57 20777
Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20773/statm): 531 226 485 147 0 384 0
[pid=20773] vsize: 2124
Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 26664 0 0 0 54600 171 0 0 25 0 1 0 1855205461 110215168 26274 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20777/statm): 26908 26274 145 145 0 26763 0
[pid=20777] vsize: 107632
Current children cumulated CPU time (s) 547.72
Current children cumulated vsize (Kb) 109756

[startup+560.041 s]
Raw data (loadavg): 1.00 0.97 0.83 2/57 20777
Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20773/statm): 531 226 485 147 0 384 0
[pid=20773] vsize: 2124
Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 27132 0 0 0 55593 173 0 0 25 0 1 0 1855205461 112128000 26742 4294967295 134512640 135094434 3221224432 3221223024 134556966 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20777/statm): 27375 26742 145 145 0 27230 0
[pid=20777] vsize: 109500
Current children cumulated CPU time (s) 557.67
Current children cumulated vsize (Kb) 111624

[startup+570.043 s]
Raw data (loadavg): 1.00 0.97 0.83 2/57 20777
Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20773/statm): 531 226 485 147 0 384 0
[pid=20773] vsize: 2124
Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 27549 0 0 0 56586 176 0 0 25 0 1 0 1855205461 113831936 27159 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20777/statm): 27791 27159 145 145 0 27646 0
[pid=20777] vsize: 111164
Current children cumulated CPU time (s) 567.63
Current children cumulated vsize (Kb) 113288

[startup+580.043 s]
Raw data (loadavg): 1.00 0.97 0.83 2/57 20777
Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20773/statm): 531 226 485 147 0 384 0
[pid=20773] vsize: 2124
Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 27962 0 0 0 57579 179 0 0 25 0 1 0 1855205461 115515392 27572 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20777/statm): 28202 27572 145 145 0 28057 0
[pid=20777] vsize: 112808
Current children cumulated CPU time (s) 577.59
Current children cumulated vsize (Kb) 114932

[startup+590.045 s]
Raw data (loadavg): 1.00 0.97 0.83 2/57 20777
Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20773/statm): 531 226 485 147 0 384 0
[pid=20773] vsize: 2124
Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 28341 0 0 0 58574 182 0 0 25 0 1 0 1855205461 117063680 27951 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20777/statm): 28580 27951 145 145 0 28435 0
[pid=20777] vsize: 114320
Current children cumulated CPU time (s) 587.57
Current children cumulated vsize (Kb) 116444

[startup+600.046 s]
Raw data (loadavg): 1.00 0.97 0.83 2/57 20777
Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20773/statm): 531 226 485 147 0 384 0
[pid=20773] vsize: 2124
Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 28701 0 0 0 59568 184 0 0 25 0 1 0 1855205461 118534144 28311 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20777/statm): 28939 28311 145 145 0 28794 0
[pid=20777] vsize: 115756
Current children cumulated CPU time (s) 597.53
Current children cumulated vsize (Kb) 117880

[startup+610.047 s]
Raw data (loadavg): 1.00 0.97 0.83 2/57 20777
Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20773/statm): 531 226 485 147 0 384 0
[pid=20773] vsize: 2124
Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 29120 0 0 0 60560 188 0 0 25 0 1 0 1855205461 120254464 28730 4294967295 134512640 135094434 3221224432 3221223120 134554676 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20777/statm): 29359 28730 145 145 0 29214 0
[pid=20777] vsize: 117436
Current children cumulated CPU time (s) 607.49
Current children cumulated vsize (Kb) 119560

[startup+620.048 s]
Raw data (loadavg): 1.00 0.97 0.83 2/57 20777
Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20773/statm): 531 226 485 147 0 384 0
[pid=20773] vsize: 2124
Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 29643 0 0 0 61550 192 0 0 25 0 1 0 1855205461 122392576 29253 4294967295 134512640 135094434 3221224432 3221223104 134555769 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20777/statm): 29881 29253 145 145 0 29736 0
[pid=20777] vsize: 119524
Current children cumulated CPU time (s) 617.43
Current children cumulated vsize (Kb) 121648

[startup+630.049 s]
Raw data (loadavg): 1.00 0.97 0.84 2/57 20777
Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20773/statm): 531 226 485 147 0 384 0
[pid=20773] vsize: 2124
Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 30204 0 0 0 62540 196 0 0 25 0 1 0 1855205461 124682240 29814 4294967295 134512640 135094434 3221224432 3221223024 134556993 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20777/statm): 30440 29814 145 145 0 30295 0
[pid=20777] vsize: 121760
Current children cumulated CPU time (s) 627.37
Current children cumulated vsize (Kb) 123884

[startup+640.05 s]
Raw data (loadavg): 1.00 0.97 0.84 2/57 20777
Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20773/statm): 531 226 485 147 0 384 0
[pid=20773] vsize: 2124
Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 30924 0 0 0 63529 201 0 0 25 0 1 0 1855205461 127623168 30534 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20777/statm): 31158 30534 145 145 0 31013 0
[pid=20777] vsize: 124632
Current children cumulated CPU time (s) 637.31
Current children cumulated vsize (Kb) 126756

[startup+650.051 s]
Raw data (loadavg): 1.00 0.97 0.84 2/57 20777
Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20773/statm): 531 226 485 147 0 384 0
[pid=20773] vsize: 2124
Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 31314 0 0 0 64523 203 0 0 25 0 1 0 1855205461 129212416 30924 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20777/statm): 31546 30924 145 145 0 31401 0
[pid=20777] vsize: 126184
Current children cumulated CPU time (s) 647.27
Current children cumulated vsize (Kb) 128308

[startup+660.052 s]
Raw data (loadavg): 1.00 0.97 0.84 2/57 20777
Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20773/statm): 531 226 485 147 0 384 0
[pid=20773] vsize: 2124
Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 31855 0 0 0 65515 206 0 0 25 0 1 0 1855205461 131424256 31465 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20777/statm): 32086 31465 145 145 0 31941 0
[pid=20777] vsize: 128344
Current children cumulated CPU time (s) 657.22
Current children cumulated vsize (Kb) 130468

[startup+670.053 s]
Raw data (loadavg): 1.00 0.97 0.84 2/57 20777
Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20773/statm): 531 226 485 147 0 384 0
[pid=20773] vsize: 2124
Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 32371 0 0 0 66509 209 0 0 25 0 1 0 1855205461 133529600 31981 4294967295 134512640 135094434 3221224432 3221223088 134558169 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20777/statm): 32600 31981 145 145 0 32455 0
[pid=20777] vsize: 130400
Current children cumulated CPU time (s) 667.19
Current children cumulated vsize (Kb) 132524

[startup+680.053 s]
Raw data (loadavg): 1.00 0.97 0.84 2/57 20777
Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20773/statm): 531 226 485 147 0 384 0
[pid=20773] vsize: 2124
Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 32840 0 0 0 67503 211 0 0 25 0 1 0 1855205461 135446528 32450 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20777/statm): 33068 32450 145 145 0 32923 0
[pid=20777] vsize: 132272
Current children cumulated CPU time (s) 677.15
Current children cumulated vsize (Kb) 134396

[startup+690.054 s]
Raw data (loadavg): 1.00 0.97 0.84 2/57 20777
Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20773/statm): 531 226 485 147 0 384 0
[pid=20773] vsize: 2124
Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 33137 0 0 0 68498 214 0 0 25 0 1 0 1855205461 136654848 32747 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20777/statm): 33363 32747 145 145 0 33218 0
[pid=20777] vsize: 133452
Current children cumulated CPU time (s) 687.13
Current children cumulated vsize (Kb) 135576

[startup+700.055 s]
Raw data (loadavg): 1.00 0.97 0.84 2/57 20777
Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20773/statm): 531 226 485 147 0 384 0
[pid=20773] vsize: 2124
Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 33436 0 0 0 69492 217 0 0 25 0 1 0 1855205461 138399744 33046 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20777/statm): 33789 33046 145 145 0 33644 0
[pid=20777] vsize: 135156
Current children cumulated CPU time (s) 697.1
Current children cumulated vsize (Kb) 137280

[startup+710.056 s]
Raw data (loadavg): 1.00 0.97 0.84 2/57 20777
Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20773/statm): 531 226 485 147 0 384 0
[pid=20773] vsize: 2124
Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 33583 0 0 0 70488 218 0 0 25 0 1 0 1855205461 138997760 33193 4294967295 134512640 135094434 3221224432 3221223088 134558402 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20777/statm): 33935 33193 145 145 0 33790 0
[pid=20777] vsize: 135740
Current children cumulated CPU time (s) 707.07
Current children cumulated vsize (Kb) 137864

[startup+720.057 s]
Raw data (loadavg): 1.00 0.97 0.84 2/57 20777
Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20773/statm): 531 226 485 147 0 384 0
[pid=20773] vsize: 2124
Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 34004 0 0 0 71481 222 0 0 25 0 1 0 1855205461 140713984 33614 4294967295 134512640 135094434 3221224432 3221223024 134557141 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20777/statm): 34354 33614 145 145 0 34209 0
[pid=20777] vsize: 137416
Current children cumulated CPU time (s) 717.04
Current children cumulated vsize (Kb) 139540

[startup+730.058 s]
Raw data (loadavg): 1.00 0.97 0.85 2/57 20777
Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20773/statm): 531 226 485 147 0 384 0
[pid=20773] vsize: 2124
Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 34588 0 0 0 72472 226 0 0 25 0 1 0 1855205461 143101952 34198 4294967295 134512640 135094434 3221224432 3221223024 134557141 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20777/statm): 34937 34198 145 145 0 34792 0
[pid=20777] vsize: 139748
Current children cumulated CPU time (s) 726.99
Current children cumulated vsize (Kb) 141872

[startup+740.058 s]
Raw data (loadavg): 1.00 0.97 0.85 2/57 20777
Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20773/statm): 531 226 485 147 0 384 0
[pid=20773] vsize: 2124
Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 35150 0 0 0 73463 230 0 0 25 0 1 0 1855205461 145399808 34760 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20777/statm): 35498 34760 145 145 0 35353 0
[pid=20777] vsize: 141992
Current children cumulated CPU time (s) 736.94
Current children cumulated vsize (Kb) 144116

[startup+750.06 s]
Raw data (loadavg): 1.00 0.97 0.85 1/57 20777
Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20773/statm): 531 226 485 147 0 384 0
[pid=20773] vsize: 2124
Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) T 20773 20773 20115 0 -1 0 35669 0 0 0 74455 234 0 0 25 0 1 0 1855205461 147521536 35279 4294967295 134512640 135094434 3221224432 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/20777/statm): 36016 35279 145 145 0 35871 0
[pid=20777] vsize: 144064
Current children cumulated CPU time (s) 746.9
Current children cumulated vsize (Kb) 146188

[startup+760.061 s]
Raw data (loadavg): 1.00 0.97 0.85 2/57 20777
Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20773/statm): 531 226 485 147 0 384 0
[pid=20773] vsize: 2124
Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 36115 0 0 0 75448 237 0 0 25 0 1 0 1855205461 149344256 35725 4294967295 134512640 135094434 3221224432 3221223024 134556864 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20777/statm): 36461 35725 145 145 0 36316 0
[pid=20777] vsize: 145844
Current children cumulated CPU time (s) 756.86
Current children cumulated vsize (Kb) 147968

[startup+770.061 s]
Raw data (loadavg): 1.00 0.97 0.85 2/57 20777
Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20773/statm): 531 226 485 147 0 384 0
[pid=20773] vsize: 2124
Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 36587 0 0 0 76443 239 0 0 25 0 1 0 1855205461 151273472 36197 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20777/statm): 36932 36197 145 145 0 36787 0
[pid=20777] vsize: 147728
Current children cumulated CPU time (s) 766.83
Current children cumulated vsize (Kb) 149852

[startup+780.062 s]
Raw data (loadavg): 1.00 0.97 0.85 2/57 20777
Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20773/statm): 531 226 485 147 0 384 0
[pid=20773] vsize: 2124
Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 37073 0 0 0 77436 242 0 0 25 0 1 0 1855205461 153255936 36683 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20777/statm): 37416 36683 145 145 0 37271 0
[pid=20777] vsize: 149664
Current children cumulated CPU time (s) 776.79
Current children cumulated vsize (Kb) 151788

[startup+790.063 s]
Raw data (loadavg): 1.00 0.97 0.85 2/57 20777
Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20773/statm): 531 226 485 147 0 384 0
[pid=20773] vsize: 2124
Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 37406 0 0 0 78432 243 0 0 25 0 1 0 1855205461 154619904 37016 4294967295 134512640 135094434 3221224432 3221223024 134556826 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20777/statm): 37749 37016 145 145 0 37604 0
[pid=20777] vsize: 150996
Current children cumulated CPU time (s) 786.76
Current children cumulated vsize (Kb) 153120

[startup+800.063 s]
Raw data (loadavg): 1.00 0.97 0.85 2/57 20777
Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20773/statm): 531 226 485 147 0 384 0
[pid=20773] vsize: 2124
Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 37766 0 0 0 79425 247 0 0 25 0 1 0 1855205461 156086272 37376 4294967295 134512640 135094434 3221224432 3221223024 134557119 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20777/statm): 38107 37376 145 145 0 37962 0
[pid=20777] vsize: 152428
Current children cumulated CPU time (s) 796.73
Current children cumulated vsize (Kb) 154552

[startup+810.065 s]
Raw data (loadavg): 1.00 0.97 0.85 2/57 20777
Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20773/statm): 531 226 485 147 0 384 0
[pid=20773] vsize: 2124
Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 38156 0 0 0 80419 249 0 0 25 0 1 0 1855205461 157687808 37766 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20777/statm): 38498 37766 145 145 0 38353 0
[pid=20777] vsize: 153992
Current children cumulated CPU time (s) 806.69
Current children cumulated vsize (Kb) 156116

[startup+820.066 s]
Raw data (loadavg): 1.00 0.97 0.85 2/57 20777
Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20773/statm): 531 226 485 147 0 384 0
[pid=20773] vsize: 2124
Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 38585 0 0 0 81413 252 0 0 25 0 1 0 1855205461 159440896 38195 4294967295 134512640 135094434 3221224432 3221223024 134556961 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20777/statm): 38926 38195 145 145 0 38781 0
[pid=20777] vsize: 155704
Current children cumulated CPU time (s) 816.66
Current children cumulated vsize (Kb) 157828

[startup+830.066 s]
Raw data (loadavg): 1.00 0.97 0.86 2/57 20777
Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20773/statm): 531 226 485 147 0 384 0
[pid=20773] vsize: 2124
Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 38788 0 0 0 82409 254 0 0 25 0 1 0 1855205461 160268288 38398 4294967295 134512640 135094434 3221224432 3221223088 134558225 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20777/statm): 39128 38398 145 145 0 38983 0
[pid=20777] vsize: 156512
Current children cumulated CPU time (s) 826.64
Current children cumulated vsize (Kb) 158636

[startup+840.067 s]
Raw data (loadavg): 1.00 0.97 0.86 2/57 20777
Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20773/statm): 531 226 485 147 0 384 0
[pid=20773] vsize: 2124
Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 38859 0 0 0 83408 255 0 0 25 0 1 0 1855205461 160555008 38469 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20777/statm): 39198 38469 145 145 0 39053 0
[pid=20777] vsize: 156792
Current children cumulated CPU time (s) 836.64
Current children cumulated vsize (Kb) 158916

[startup+850.068 s]
Raw data (loadavg): 1.00 0.97 0.86 2/57 20777
Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20773/statm): 531 226 485 147 0 384 0
[pid=20773] vsize: 2124
Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 38859 0 0 0 84408 255 0 0 25 0 1 0 1855205461 160555008 38469 4294967295 134512640 135094434 3221224432 3221223024 134557028 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20777/statm): 39198 38469 145 145 0 39053 0
[pid=20777] vsize: 156792
Current children cumulated CPU time (s) 846.64
Current children cumulated vsize (Kb) 158916

[startup+860.068 s]
Raw data (loadavg): 1.00 0.97 0.86 2/57 20777
Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20773/statm): 531 226 485 147 0 384 0
[pid=20773] vsize: 2124
Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 38859 0 0 0 85409 255 0 0 25 0 1 0 1855205461 160555008 38469 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20777/statm): 39198 38469 145 145 0 39053 0
[pid=20777] vsize: 156792
Current children cumulated CPU time (s) 856.65
Current children cumulated vsize (Kb) 158916

[startup+870.069 s]
Raw data (loadavg): 1.00 0.97 0.86 2/57 20777
Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20773/statm): 531 226 485 147 0 384 0
[pid=20773] vsize: 2124
Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 38859 0 0 0 86409 255 0 0 25 0 1 0 1855205461 160555008 38469 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20777/statm): 39198 38469 145 145 0 39053 0
[pid=20777] vsize: 156792
Current children cumulated CPU time (s) 866.65
Current children cumulated vsize (Kb) 158916

[startup+880.07 s]
Raw data (loadavg): 1.00 0.97 0.86 2/57 20777
Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20773/statm): 531 226 485 147 0 384 0
[pid=20773] vsize: 2124
Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 38859 0 0 0 87409 255 0 0 25 0 1 0 1855205461 160555008 38469 4294967295 134512640 135094434 3221224432 3221223104 134555811 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20777/statm): 39198 38469 145 145 0 39053 0
[pid=20777] vsize: 156792
Current children cumulated CPU time (s) 876.65
Current children cumulated vsize (Kb) 158916

[startup+890.07 s]
Raw data (loadavg): 1.00 0.97 0.86 2/57 20777
Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20773/statm): 531 226 485 147 0 384 0
[pid=20773] vsize: 2124
Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 38859 0 0 0 88409 255 0 0 25 0 1 0 1855205461 160555008 38469 4294967295 134512640 135094434 3221224432 3221223024 134556847 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20777/statm): 39198 38469 145 145 0 39053 0
[pid=20777] vsize: 156792
Current children cumulated CPU time (s) 886.65
Current children cumulated vsize (Kb) 158916

[startup+900.071 s]
Raw data (loadavg): 1.00 0.97 0.86 2/57 20777
Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20773/statm): 531 226 485 147 0 384 0
[pid=20773] vsize: 2124
Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 38859 0 0 0 89409 255 0 0 25 0 1 0 1855205461 160555008 38469 4294967295 134512640 135094434 3221224432 3221223104 134555232 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20777/statm): 39198 38469 145 145 0 39053 0
[pid=20777] vsize: 156792
Current children cumulated CPU time (s) 896.65
Current children cumulated vsize (Kb) 158916

[startup+910.073 s]
Raw data (loadavg): 1.00 0.97 0.86 2/57 20777
Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20773/statm): 531 226 485 147 0 384 0
[pid=20773] vsize: 2124
Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 38859 0 0 0 90409 255 0 0 25 0 1 0 1855205461 160555008 38469 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20777/statm): 39198 38469 145 145 0 39053 0
[pid=20777] vsize: 156792
Current children cumulated CPU time (s) 906.65
Current children cumulated vsize (Kb) 158916

[startup+920.073 s]
Raw data (loadavg): 1.00 0.97 0.86 2/57 20777
Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20773/statm): 531 226 485 147 0 384 0
[pid=20773] vsize: 2124
Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 38859 0 0 0 91410 255 0 0 25 0 1 0 1855205461 160555008 38469 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20777/statm): 39198 38469 145 145 0 39053 0
[pid=20777] vsize: 156792
Current children cumulated CPU time (s) 916.66
Current children cumulated vsize (Kb) 158916

[startup+930.074 s]
Raw data (loadavg): 1.00 0.97 0.87 2/57 20777
Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20773/statm): 531 226 485 147 0 384 0
[pid=20773] vsize: 2124
Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 38859 0 0 0 92410 255 0 0 25 0 1 0 1855205461 160555008 38469 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20777/statm): 39198 38469 145 145 0 39053 0
[pid=20777] vsize: 156792
Current children cumulated CPU time (s) 926.66
Current children cumulated vsize (Kb) 158916

[startup+940.075 s]
Raw data (loadavg): 1.00 0.97 0.87 2/57 20777
Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20773/statm): 531 226 485 147 0 384 0
[pid=20773] vsize: 2124
Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 38859 0 0 0 93410 255 0 0 25 0 1 0 1855205461 160555008 38469 4294967295 134512640 135094434 3221224432 3221223024 134557310 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20777/statm): 39198 38469 145 145 0 39053 0
[pid=20777] vsize: 156792
Current children cumulated CPU time (s) 936.66
Current children cumulated vsize (Kb) 158916

[startup+950.075 s]
Raw data (loadavg): 1.00 0.97 0.87 2/57 20777
Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20773/statm): 531 226 485 147 0 384 0
[pid=20773] vsize: 2124
Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 38859 0 0 0 94411 255 0 0 25 0 1 0 1855205461 160555008 38469 4294967295 134512640 135094434 3221224432 3221223024 134556809 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20777/statm): 39198 38469 145 145 0 39053 0
[pid=20777] vsize: 156792
Current children cumulated CPU time (s) 946.67
Current children cumulated vsize (Kb) 158916

[startup+960.076 s]
Raw data (loadavg): 1.00 0.97 0.87 2/57 20777
Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20773/statm): 531 226 485 147 0 384 0
[pid=20773] vsize: 2124
Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 38859 0 0 0 95411 255 0 0 25 0 1 0 1855205461 160555008 38469 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20777/statm): 39198 38469 145 145 0 39053 0
[pid=20777] vsize: 156792
Current children cumulated CPU time (s) 956.67
Current children cumulated vsize (Kb) 158916

[startup+970.077 s]
Raw data (loadavg): 1.00 0.97 0.87 2/57 20777
Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20773/statm): 531 226 485 147 0 384 0
[pid=20773] vsize: 2124
Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 38859 0 0 0 96411 255 0 0 25 0 1 0 1855205461 160555008 38469 4294967295 134512640 135094434 3221224432 3221223088 134557900 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20777/statm): 39198 38469 145 145 0 39053 0
[pid=20777] vsize: 156792
Current children cumulated CPU time (s) 966.67
Current children cumulated vsize (Kb) 158916

[startup+980.077 s]
Raw data (loadavg): 1.00 0.97 0.87 2/57 20777
Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20773/statm): 531 226 485 147 0 384 0
[pid=20773] vsize: 2124
Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 38859 0 0 0 97411 255 0 0 25 0 1 0 1855205461 160555008 38469 4294967295 134512640 135094434 3221224432 3221223024 134557522 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20777/statm): 39198 38469 145 145 0 39053 0
[pid=20777] vsize: 156792
Current children cumulated CPU time (s) 976.67
Current children cumulated vsize (Kb) 158916

[startup+990.078 s]
Raw data (loadavg): 1.00 0.97 0.87 2/57 20777
Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20773/statm): 531 226 485 147 0 384 0
[pid=20773] vsize: 2124
Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 38859 0 0 0 98411 255 0 0 25 0 1 0 1855205461 160555008 38469 4294967295 134512640 135094434 3221224432 3221223024 134556789 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20777/statm): 39198 38469 145 145 0 39053 0
[pid=20777] vsize: 156792
Current children cumulated CPU time (s) 986.67
Current children cumulated vsize (Kb) 158916

[startup+1000.08 s]
Raw data (loadavg): 1.00 0.97 0.87 2/57 20777
Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20773/statm): 531 226 485 147 0 384 0
[pid=20773] vsize: 2124
Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 38859 0 0 0 99411 255 0 0 25 0 1 0 1855205461 160555008 38469 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20777/statm): 39198 38469 145 145 0 39053 0
[pid=20777] vsize: 156792
Current children cumulated CPU time (s) 996.67
Current children cumulated vsize (Kb) 158916

[startup+1010.08 s]
Raw data (loadavg): 1.00 0.97 0.87 2/57 20777
Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20773/statm): 531 226 485 147 0 384 0
[pid=20773] vsize: 2124
Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 38859 0 0 0 100412 255 0 0 25 0 1 0 1855205461 160555008 38469 4294967295 134512640 135094434 3221224432 3221223024 134557413 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20777/statm): 39198 38469 145 145 0 39053 0
[pid=20777] vsize: 156792
Current children cumulated CPU time (s) 1006.68
Current children cumulated vsize (Kb) 158916

[startup+1020.08 s]
Raw data (loadavg): 1.00 0.97 0.87 2/57 20777
Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20773/statm): 531 226 485 147 0 384 0
[pid=20773] vsize: 2124
Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 38859 0 0 0 101410 257 0 0 25 0 1 0 1855205461 160555008 38469 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20777/statm): 39198 38469 145 145 0 39053 0
[pid=20777] vsize: 156792
Current children cumulated CPU time (s) 1016.68
Current children cumulated vsize (Kb) 158916

[startup+1030.08 s]
Raw data (loadavg): 1.00 0.97 0.87 2/57 20777
Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20773/statm): 531 226 485 147 0 384 0
[pid=20773] vsize: 2124
Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 38859 0 0 0 102410 257 0 0 25 0 1 0 1855205461 160555008 38469 4294967295 134512640 135094434 3221224432 3221223088 134558221 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20777/statm): 39198 38469 145 145 0 39053 0
[pid=20777] vsize: 156792
Current children cumulated CPU time (s) 1026.68
Current children cumulated vsize (Kb) 158916

[startup+1040.08 s]
Raw data (loadavg): 1.00 0.97 0.88 2/57 20777
Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20773/statm): 531 226 485 147 0 384 0
[pid=20773] vsize: 2124
Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 38859 0 0 0 103410 258 0 0 25 0 1 0 1855205461 160555008 38469 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20777/statm): 39198 38469 145 145 0 39053 0
[pid=20777] vsize: 156792
Current children cumulated CPU time (s) 1036.69
Current children cumulated vsize (Kb) 158916

[startup+1050.08 s]
Raw data (loadavg): 1.00 0.97 0.88 2/57 20777
Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20773/statm): 531 226 485 147 0 384 0
[pid=20773] vsize: 2124
Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 38859 0 0 0 104409 258 0 0 25 0 1 0 1855205461 160555008 38469 4294967295 134512640 135094434 3221224432 3221223088 134557846 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20777/statm): 39198 38469 145 145 0 39053 0
[pid=20777] vsize: 156792
Current children cumulated CPU time (s) 1046.68
Current children cumulated vsize (Kb) 158916

[startup+1060.08 s]
Raw data (loadavg): 1.00 0.97 0.88 2/57 20777
Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20773/statm): 531 226 485 147 0 384 0
[pid=20773] vsize: 2124
Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 38859 0 0 0 105409 259 0 0 25 0 1 0 1855205461 160555008 38469 4294967295 134512640 135094434 3221224432 3221223088 134558178 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20777/statm): 39198 38469 145 145 0 39053 0
[pid=20777] vsize: 156792
Current children cumulated CPU time (s) 1056.69
Current children cumulated vsize (Kb) 158916

[startup+1070.08 s]
Raw data (loadavg): 1.00 0.97 0.88 2/57 20777
Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20773/statm): 531 226 485 147 0 384 0
[pid=20773] vsize: 2124
Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 38859 0 0 0 106409 259 0 0 25 0 1 0 1855205461 160555008 38469 4294967295 134512640 135094434 3221224432 3221223024 134557227 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20777/statm): 39198 38469 145 145 0 39053 0
[pid=20777] vsize: 156792
Current children cumulated CPU time (s) 1066.69
Current children cumulated vsize (Kb) 158916

[startup+1080.09 s]
Raw data (loadavg): 1.00 0.97 0.88 2/57 20777
Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20773/statm): 531 226 485 147 0 384 0
[pid=20773] vsize: 2124
Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 38859 0 0 0 107409 259 0 0 25 0 1 0 1855205461 160555008 38469 4294967295 134512640 135094434 3221224432 3221223024 134556789 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20777/statm): 39198 38469 145 145 0 39053 0
[pid=20777] vsize: 156792
Current children cumulated CPU time (s) 1076.69
Current children cumulated vsize (Kb) 158916

[startup+1090.09 s]
Raw data (loadavg): 1.00 0.97 0.88 2/57 20777
Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20773/statm): 531 226 485 147 0 384 0
[pid=20773] vsize: 2124
Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 38859 0 0 0 108409 259 0 0 25 0 1 0 1855205461 160555008 38469 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20777/statm): 39198 38469 145 145 0 39053 0
[pid=20777] vsize: 156792
Current children cumulated CPU time (s) 1086.69
Current children cumulated vsize (Kb) 158916

[startup+1100.09 s]
Raw data (loadavg): 1.00 0.97 0.88 2/57 20777
Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20773/statm): 531 226 485 147 0 384 0
[pid=20773] vsize: 2124
Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 38859 0 0 0 109409 260 0 0 25 0 1 0 1855205461 160555008 38469 4294967295 134512640 135094434 3221224432 3221223088 134558210 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20777/statm): 39198 38469 145 145 0 39053 0
[pid=20777] vsize: 156792
Current children cumulated CPU time (s) 1096.7
Current children cumulated vsize (Kb) 158916

[startup+1110.09 s]
Raw data (loadavg): 1.00 0.97 0.88 2/57 20777
Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20773/statm): 531 226 485 147 0 384 0
[pid=20773] vsize: 2124
Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 38859 0 0 0 110410 260 0 0 25 0 1 0 1855205461 160555008 38469 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20777/statm): 39198 38469 145 145 0 39053 0
[pid=20777] vsize: 156792
Current children cumulated CPU time (s) 1106.71
Current children cumulated vsize (Kb) 158916

[startup+1120.09 s]
Raw data (loadavg): 1.00 0.97 0.88 2/57 20777
Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20773/statm): 531 226 485 147 0 384 0
[pid=20773] vsize: 2124
Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 38859 0 0 0 111410 260 0 0 25 0 1 0 1855205461 160555008 38469 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20777/statm): 39198 38469 145 145 0 39053 0
[pid=20777] vsize: 156792
Current children cumulated CPU time (s) 1116.71
Current children cumulated vsize (Kb) 158916

[startup+1130.09 s]
Raw data (loadavg): 1.00 0.97 0.88 2/57 20777
Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20773/statm): 531 226 485 147 0 384 0
[pid=20773] vsize: 2124
Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 38859 0 0 0 112410 260 0 0 25 0 1 0 1855205461 160555008 38469 4294967295 134512640 135094434 3221224432 3221223088 134558395 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20777/statm): 39198 38469 145 145 0 39053 0
[pid=20777] vsize: 156792
Current children cumulated CPU time (s) 1126.71
Current children cumulated vsize (Kb) 158916

[startup+1140.09 s]
Raw data (loadavg): 1.00 0.97 0.89 2/57 20777
Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20773/statm): 531 226 485 147 0 384 0
[pid=20773] vsize: 2124
Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 38859 0 0 0 113410 260 0 0 25 0 1 0 1855205461 160555008 38469 4294967295 134512640 135094434 3221224432 3221223024 134556990 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20777/statm): 39198 38469 145 145 0 39053 0
[pid=20777] vsize: 156792
Current children cumulated CPU time (s) 1136.71
Current children cumulated vsize (Kb) 158916

[startup+1150.09 s]
Raw data (loadavg): 1.00 0.97 0.89 2/57 20777
Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20773/statm): 531 226 485 147 0 384 0
[pid=20773] vsize: 2124
Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 38859 0 0 0 114410 260 0 0 25 0 1 0 1855205461 160555008 38469 4294967295 134512640 135094434 3221224432 3221223024 134557494 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20777/statm): 39198 38469 145 145 0 39053 0
[pid=20777] vsize: 156792
Current children cumulated CPU time (s) 1146.71
Current children cumulated vsize (Kb) 158916

[startup+1160.09 s]
Raw data (loadavg): 1.00 0.97 0.89 2/57 20777
Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20773/statm): 531 226 485 147 0 384 0
[pid=20773] vsize: 2124
Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 38859 0 0 0 115410 260 0 0 25 0 1 0 1855205461 160555008 38469 4294967295 134512640 135094434 3221224432 3221223024 134556931 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20777/statm): 39198 38469 145 145 0 39053 0
[pid=20777] vsize: 156792
Current children cumulated CPU time (s) 1156.71
Current children cumulated vsize (Kb) 158916

[startup+1170.09 s]
Raw data (loadavg): 1.00 0.97 0.89 2/57 20777
Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20773/statm): 531 226 485 147 0 384 0
[pid=20773] vsize: 2124
Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 38859 0 0 0 116410 260 0 0 25 0 1 0 1855205461 160555008 38469 4294967295 134512640 135094434 3221224432 3221223088 134558022 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20777/statm): 39198 38469 145 145 0 39053 0
[pid=20777] vsize: 156792
Current children cumulated CPU time (s) 1166.71
Current children cumulated vsize (Kb) 158916

[startup+1180.09 s]
Raw data (loadavg): 1.00 0.97 0.89 2/57 20777
Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20773/statm): 531 226 485 147 0 384 0
[pid=20773] vsize: 2124
Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 38859 0 0 0 117410 260 0 0 25 0 1 0 1855205461 160555008 38469 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20777/statm): 39198 38469 145 145 0 39053 0
[pid=20777] vsize: 156792
Current children cumulated CPU time (s) 1176.71
Current children cumulated vsize (Kb) 158916

[startup+1190.09 s]
Raw data (loadavg): 1.00 0.97 0.89 2/57 20777
Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20773/statm): 531 226 485 147 0 384 0
[pid=20773] vsize: 2124
Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 38859 0 0 0 118411 260 0 0 25 0 1 0 1855205461 160555008 38469 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20777/statm): 39198 38469 145 145 0 39053 0
[pid=20777] vsize: 156792
Current children cumulated CPU time (s) 1186.72
Current children cumulated vsize (Kb) 158916

[startup+1200.09 s]
Raw data (loadavg): 1.00 0.97 0.89 2/57 20777
Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20773/statm): 531 226 485 147 0 384 0
[pid=20773] vsize: 2124
Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 38859 0 0 0 119411 261 0 0 25 0 1 0 1855205461 160555008 38469 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20777/statm): 39198 38469 145 145 0 39053 0
[pid=20777] vsize: 156792
Current children cumulated CPU time (s) 1196.73
Current children cumulated vsize (Kb) 158916

[startup+1210.09 s]
Raw data (loadavg): 1.00 0.97 0.89 2/57 20777
Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20773/statm): 531 226 485 147 0 384 0
[pid=20773] vsize: 2124
Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 38859 0 0 0 120411 261 0 0 25 0 1 0 1855205461 160555008 38469 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20777/statm): 39198 38469 145 145 0 39053 0
[pid=20777] vsize: 156792
Current children cumulated CPU time (s) 1206.73
Current children cumulated vsize (Kb) 158916



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.1 s]
Raw data (loadavg): 1.00 0.97 0.89 2/57 20777
Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/20773/statm): 531 226 485 147 0 384 0
[pid=20773] vsize: 2124
Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 38859 0 0 0 120411 261 0 0 25 0 1 0 1855205461 160555008 38469 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20777/statm): 39198 38469 145 145 0 39053 0
[pid=20777] vsize: 156792
Current children cumulated CPU time (s) 1206.73
Current children cumulated vsize (Kb) 158916

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

Child status: 0
Real time (s): 1210.17
CPU time (s): 1206.8
CPU user time (s): 1204.11
CPU system time (s): 2.68359
CPU usage (%): 99.7213
Max. virtual memory (cumulated for all children) (Kb): 158916

Verifier Data

ERROR: no interpretation found !