Some explanations

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

General information on the benchmark

Namemps-v2-20-10/plato.asu.edu/pub/milp/normalized-mps-v2-20-10-ran14x18_1.opb
MD5SUMd1752d9737bcd79380522c97c646ca71
Bench Categoryoptimization, big integers (OPTBIGINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function 10877893
Optimality of the best value was proved NO
Number of terms in the objective function 7812
Biggest coefficient in the objective function 5368709120
Number of bits for the biggest coefficient in the objective function 33
Sum of the numbers in the objective function 1450667950777
Number of bits of the sum of numbers in the objective function 41
Biggest number in a constraint 5368709120
Number of bits of the biggest number in a constraint 33
Biggest sum of numbers in a constraint 1450667950777
Number of bits of the biggest sum of numbers41
Best result obtained on this benchmarkSAT
Best CPU time to get the best result obtained on this benchmark1227.68
Number of variables7812
Total number of constraints536
Number of constraints which are clauses0
Number of constraints which are cardinality constraints (but not clauses)252
Number of constraints which are nor clauses,nor cardinality constraints284
Minimum length of a constraint1
Maximum length of a constraint540

Trace number 5904

Launcher Data

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.190
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:        926980 kB
Buffers:          3908 kB
Cached:          77072 kB
SwapCached:        824 kB
Active:          15716 kB
Inactive:        67848 kB
HighTotal:      131008 kB
HighFree:        49980 kB
LowTotal:       903652 kB
LowFree:        877000 kB
SwapTotal:     2097136 kB
SwapFree:      2095740 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5656 kB
Slab:            18216 kB
Committed_AS:    72360 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-09-20 02:06:14 (client local time) WITH STATUS 0 IN 1207.51 SECONDS
stats: 3081 7 1207.51 0

Solver Data

c Parsing PB file...
c Converting 316 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ################################
c   -- Clauses(.)/Splits(s): (none)
c ---[ 314]---> Adder-cost: 488   maxlim: 379886   bits: 19/19
c ---[ 312]---> Adder-cost: 488   maxlim: 381934   bits: 19/19
c ---[ 310]---> Adder-cost: 488   maxlim: 378862   bits: 19/19
c ---[ 308]---> Adder-cost: 490   maxlim: 465902   bits: 19/19
c ---[ 306]---> Adder-cost: 488   maxlim: 378862   bits: 19/19
c ---[ 304]---> Adder-cost: 488   maxlim: 374766   bits: 19/19
c ---[ 302]---> Adder-cost: 488   maxlim: 376814   bits: 19/19
c ---[ 300]---> Adder-cost: 474   maxlim: 260078   bits: 19/18
c ---[ 298]---> Adder-cost: 488   maxlim: 373742   bits: 19/19
c ---[ 296]---> Adder-cost: 488   maxlim: 375790   bits: 19/19
c ---[ 294]---> Adder-cost: 474   maxlim: 260078   bits: 19/18
c ---[ 292]---> Adder-cost: 488   maxlim: 385006   bits: 19/19
c ---[ 290]---> Adder-cost: 488   maxlim: 383982   bits: 19/19
c ---[ 288]---> Adder-cost: 490   maxlim: 460782   bits: 19/19
c ---[ 286]---> Adder-cost: 338   maxlim: 108530   bits: 17/17
c ---[ 284]---> Adder-cost: 364   maxlim: 216050   bits: 18/18
c ---[ 282]---> Adder-cost: 338   maxlim: 107506   bits: 17/17
c ---[ 280]---> Adder-cost: 388   maxlim: 407538   bits: 19/19
c ---[ 278]---> Adder-cost: 364   maxlim: 215026   bits: 18/18
c ---[ 276]---> Adder-cost: 388   maxlim: 403442   bits: 19/19
c ---[ 274]---> Adder-cost: 390   maxlim: 457714   bits: 19/19
c ---[ 272]---> Adder-cost: 390   maxlim: 445426   bits: 19/19
c ---[ 270]---> Adder-cost: 364   maxlim: 218098   bits: 18/18
c ---[ 268]---> Adder-cost: 364   maxlim: 221170   bits: 18/18
c ---[ 266]---> Adder-cost: 388   maxlim: 404466   bits: 19/19
c ---[ 264]---> Adder-cost: 364   maxlim: 218098   bits: 18/18
c ---[ 262]---> Adder-cost: 388   maxlim: 405490   bits: 19/19
c ---[ 260]---> Adder-cost: 338   maxlim: 110578   bits: 17/17
c ---[ 258]---> Adder-cost: 390   maxlim: 455666   bits: 19/19
c ---[ 256]---> Adder-cost: 364   maxlim: 216050   bits: 18/18
c ---[ 254]---> Adder-cost: 388   maxlim: 405490   bits: 19/19
c ---[ 252]---> Adder-cost: 364   maxlim: 220146   bits: 18/18
c ---[ 251]---> BDD-cost:   15
c ---[ 250]---> BDD-cost:   18
c ---[ 249]---> BDD-cost:   16
c ---[ 248]---> BDD-cost:   16
c ---[ 247]---> BDD-cost:   19
c ---[ 246]---> BDD-cost:   17
c ---[ 245]---> BDD-cost:   19
c ---[ 244]---> BDD-cost:   20
c ---[ 243]---> BDD-cost:   20
c ---[ 242]---> BDD-cost:   18
c ---[ 241]---> BDD-cost:   15
c ---[ 240]---> BDD-cost:   15
c ---[ 239]---> BDD-cost:   17
c ---[ 238]---> BDD-cost:   19
c ---[ 237]---> BDD-cost:   17
c ---[ 236]---> BDD-cost:   17
c ---[ 235]---> BDD-cost:   17
c ---[ 234]---> BDD-cost:   14
c ---[ 233]---> BDD-cost:   17
c ---[ 232]---> BDD-cost:   17
c ---[ 231]---> BDD-cost:   17
c ---[ 230]---> BDD-cost:   18
c ---[ 229]---> BDD-cost:   16
c ---[ 228]---> BDD-cost:   17
c ---[ 227]---> BDD-cost:   17
c ---[ 226]---> BDD-cost:   17
c ---[ 225]---> BDD-cost:   17
c ---[ 224]---> BDD-cost:   17
c ---[ 223]---> BDD-cost:   17
c ---[ 222]---> BDD-cost:   17
c ---[ 221]---> BDD-cost:   15
c ---[ 220]---> BDD-cost:   15
c ---[ 219]---> BDD-cost:   18
c ---[ 218]---> BDD-cost:   16
c ---[ 217]---> BDD-cost:   18
c ---[ 216]---> BDD-cost:   20
c ---[ 215]---> BDD-cost:   16
c ---[ 214]---> BDD-cost:   14
c ---[ 213]---> BDD-cost:   16
c ---[ 212]---> BDD-cost:   18
c ---[ 211]---> BDD-cost:   16
c ---[ 210]---> BDD-cost:   18
c ---[ 209]---> BDD-cost:   16
c ---[ 208]---> BDD-cost:   16
c ---[ 207]---> BDD-cost:   17
c ---[ 206]---> BDD-cost:   16
c ---[ 205]---> BDD-cost:   20
c ---[ 204]---> BDD-cost:   16
c ---[ 203]---> BDD-cost:   16
c ---[ 202]---> BDD-cost:   18
c ---[ 201]---> BDD-cost:   15
c ---[ 200]---> BDD-cost:   15
c ---[ 199]---> BDD-cost:   18
c ---[ 198]---> BDD-cost:   20
c ---[ 197]---> BDD-cost:   18
c ---[ 196]---> BDD-cost:   20
c ---[ 195]---> BDD-cost:   14
c ---[ 194]---> BDD-cost:   20
c ---[ 193]---> BDD-cost:   20
c ---[ 192]---> BDD-cost:   18
c ---[ 191]---> BDD-cost:   20
c ---[ 190]---> BDD-cost:   18
c ---[ 189]---> BDD-cost:   16
c ---[ 188]---> BDD-cost:   20
c ---[ 187]---> BDD-cost:   17
c ---[ 186]---> BDD-cost:   20
c ---[ 185]---> BDD-cost:   20
c ---[ 184]---> BDD-cost:   20
c ---[ 183]---> BDD-cost:   18
c ---[ 182]---> BDD-cost:   18
c ---[ 181]---> BDD-cost:   15
c ---[ 180]---> BDD-cost:   15
c ---[ 179]---> BDD-cost:   18
c ---[ 178]---> BDD-cost:   20
c ---[ 177]---> BDD-cost:   18
c ---[ 176]---> BDD-cost:   18
c ---[ 175]---> BDD-cost:   14
c ---[ 174]---> BDD-cost:   22
c ---[ 173]---> BDD-cost:   18
c ---[ 172]---> BDD-cost:   15
c ---[ 171]---> BDD-cost:   18
c ---[ 170]---> BDD-cost:   18
c ---[ 169]---> BDD-cost:   16
c ---[ 168]---> BDD-cost:   19
c ---[ 167]---> BDD-cost:   17
c ---[ 166]---> BDD-cost:   19
c ---[ 165]---> BDD-cost:   22
c ---[ 164]---> BDD-cost:   21
c ---[ 163]---> BDD-cost:   18
c ---[ 162]---> BDD-cost:   15
c ---[ 161]---> BDD-cost:   15
c ---[ 160]---> BDD-cost:   15
c ---[ 159]---> BDD-cost:   18
c ---[ 158]---> BDD-cost:   20
c ---[ 157]---> BDD-cost:   18
c ---[ 156]---> BDD-cost:   18
c ---[ 155]---> BDD-cost:   14
c ---[ 154]---> BDD-cost:   19
c ---[ 153]---> BDD-cost:   18
c ---[ 152]---> BDD-cost:   18
c ---[ 151]---> BDD-cost:   18
c ---[ 150]---> BDD-cost:   18
c ---[ 149]---> BDD-cost:   16
c ---[ 148]---> BDD-cost:   19
c ---[ 147]---> BDD-cost:   17
c ---[ 146]---> BDD-cost:   19
c ---[ 145]---> BDD-cost:   19
c ---[ 144]---> BDD-cost:   19
c ---[ 143]---> BDD-cost:   18
c ---[ 142]---> BDD-cost:   15
c ---[ 141]---> BDD-cost:   15
c ---[ 140]---> BDD-cost:   18
c ---[ 139]---> BDD-cost:   20
c ---[ 138]---> BDD-cost:   20
c ---[ 137]---> BDD-cost:   20
c ---[ 136]---> BDD-cost:   18
c ---[ 135]---> BDD-cost:   18
c ---[ 134]---> BDD-cost:   14
c ---[ 133]---> BDD-cost:   22
c ---[ 132]---> BDD-cost:   18
c ---[ 131]---> BDD-cost:   18
c ---[ 130]---> BDD-cost:   18
c ---[ 129]---> BDD-cost:   16
c ---[ 128]---> BDD-cost:   19
c ---[ 127]---> BDD-cost:   18
c ---[ 126]---> BDD-cost:   17
c ---[ 125]---> BDD-cost:   19
c ---[ 124]---> BDD-cost:   22
c ---[ 123]---> BDD-cost:   22
c ---[ 122]---> BDD-cost:   18
c ---[ 121]---> BDD-cost:   15
c ---[ 120]---> BDD-cost:   15
c ---[ 119]---> BDD-cost:   18
c ---[ 118]---> BDD-cost:   20
c ---[ 117]---> BDD-cost:   18
c ---[ 116]---> BDD-cost:   20
c ---[ 115]---> BDD-cost:   18
c ---[ 114]---> BDD-cost:   14
c ---[ 113]---> BDD-cost:   19
c ---[ 112]---> BDD-cost:   18
c ---[ 111]---> BDD-cost:   18
c ---[ 110]---> BDD-cost:   18
c ---[ 109]---> BDD-cost:   16
c ---[ 108]---> BDD-cost:   19
c ---[ 107]---> BDD-cost:   17
c ---[ 106]---> BDD-cost:   19
c ---[ 105]---> BDD-cost:   14
c ---[ 104]---> BDD-cost:   19
c ---[ 103]---> BDD-cost:   19
c ---[ 102]---> BDD-cost:   18
c ---[ 101]---> BDD-cost:   15
c ---[ 100]---> BDD-cost:   15
c ---[  99]---> BDD-cost:   18
c ---[  98]---> BDD-cost:   20
c ---[  97]---> BDD-cost:   18
c ---[  96]---> BDD-cost:   18
c ---[  95]---> BDD-cost:   14
c ---[  94]---> BDD-cost:   20
c ---[  93]---> BDD-cost:   19
c ---[  92]---> BDD-cost:   18
c ---[  91]---> BDD-cost:   18
c ---[  90]---> BDD-cost:   18
c ---[  89]---> BDD-cost:   16
c ---[  88]---> BDD-cost:   19
c ---[  87]---> BDD-cost:   17
c ---[  86]---> BDD-cost:   19
c ---[  85]---> BDD-cost:   19
c ---[  84]---> BDD-cost:   19
c ---[  83]---> BDD-cost:   18
c ---[  82]---> BDD-cost:   18
c ---[  81]---> BDD-cost:   15
c ---[  80]---> BDD-cost:   20
c ---[  79]---> BDD-cost:   18
c ---[  78]---> BDD-cost:   16
c ---[  77]---> BDD-cost:   19
c ---[  76]---> BDD-cost:   18
c ---[  75]---> BDD-cost:   17
c ---[  74]---> BDD-cost:   20
c ---[  73]---> BDD-cost:   20
c ---[  72]---> BDD-cost:   20
c ---[  71]---> BDD-cost:   18
c ---[  70]---> BDD-cost:   15
c ---[  69]---> BDD-cost:   15
c ---[  68]---> BDD-cost:   18
c ---[  67]---> BDD-cost:   20
c ---[  66]---> BDD-cost:   18
c ---[  65]---> BDD-cost:   18
c ---[  64]---> BDD-cost:   18
c ---[  63]---> BDD-cost:   14
c ---[  62]---> BDD-cost:   17
c ---[  61]---> BDD-cost:   18
c ---[  60]---> BDD-cost:   18
c ---[  59]---> BDD-cost:   18
c ---[  58]---> BDD-cost:   16
c ---[  57]---> BDD-cost:   19
c ---[  56]---> BDD-cost:   17
c ---[  55]---> BDD-cost:   19
c ---[  54]---> BDD-cost:   14
c ---[  53]---> BDD-cost:   17
c ---[  52]---> BDD-cost:   17
c ---[  51]---> BDD-cost:   18
c ---[  50]---> BDD-cost:   15
c ---[  49]---> BDD-cost:   15
c ---[  48]---> BDD-cost:   17
c ---[  47]---> BDD-cost:   17
c ---[  46]---> BDD-cost:   17
c ---[  45]---> BDD-cost:   17
c ---[  44]---> BDD-cost:   14
c ---[  43]---> BDD-cost:   20
c ---[  42]---> BDD-cost:   17
c ---[  41]---> BDD-cost:   17
c ---[  40]---> BDD-cost:   17
c ---[  39]---> BDD-cost:   18
c ---[  38]---> BDD-cost:   16
c ---[  37]---> BDD-cost:   17
c ---[  36]---> BDD-cost:   17
c ---[  35]---> BDD-cost:   17
c ---[  34]---> BDD-cost:   17
c ---[  33]---> BDD-cost:   17
c ---[  32]---> BDD-cost:   18
c ---[  31]---> BDD-cost:   17
c ---[  30]---> BDD-cost:   15
c ---[  29]---> BDD-cost:   15
c ---[  28]---> BDD-cost:   18
c ---[  27]---> BDD-cost:   20
c ---[  26]---> BDD-cost:   18
c ---[  25]---> BDD-cost:   18
c ---[  24]---> BDD-cost:   14
c ---[  23]---> BDD-cost:   20
c ---[  22]---> BDD-cost:   18
c ---[  21]---> BDD-cost:   18
c ---[  20]---> BDD-cost:   18
c ---[  19]---> BDD-cost:   18
c ---[  18]---> BDD-cost:   16
c ---[  17]---> BDD-cost:   19
c ---[  16]---> BDD-cost:   17
c ---[  15]---> BDD-cost:   19
c ---[  14]---> BDD-cost:   20
c ---[  13]---> BDD-cost:   20
c ---[  12]---> BDD-cost:   18
c ---[  11]---> BDD-cost:   15
c ---[  10]---> BDD-cost:   18
c ---[   9]---> BDD-cost:   15
c ---[   8]---> BDD-cost:   18
c ---[   7]---> BDD-cost:   20
c ---[   6]---> BDD-cost:   18
c ---[   5]---> BDD-cost:   18
c ---[   4]---> BDD-cost:   14
c ---[   3]---> BDD-cost:   20
c ---[   2]---> BDD-cost:   18
c ---[   1]---> BDD-cost:   18
c ---[   0]---> BDD-cost:   18
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   96690   336663 |   32230       0        0     nan |  0.000 % |
c |       100 |   96690   336663 |   35453     100      311     3.1 | 23.163 % |
c |       250 |   96581   336296 |   38998     241      746     3.1 | 23.249 % |
c |       475 |   96405   335706 |   42898     440     1437     3.3 | 23.383 % |
c |       812 |   96339   335484 |   47187     765     2476     3.2 | 23.430 % |
c |      1318 |   96007   334356 |   51906    1235     4051     3.3 | 23.688 % |
c |      2077 |   95562   332849 |   57097    1943     6475     3.3 | 24.028 % |
c |      3216 |   95220   331691 |   62807    3049    10430     3.4 | 24.291 % |
c |      4924 |   94533   329356 |   69087    4676    16439     3.5 | 24.812 % |
c |      7486 |   94190   328193 |   75996    7202    32994     4.6 | 25.074 % |
c |     11330 |   94016   327595 |   83596   11032    53560     4.9 | 25.216 % |
c |     17096 |   93968   327439 |   91955   16792    96512     5.7 | 25.255 % |
c |     25745 |   93968   327439 |  101151   25441   852627    33.5 | 25.255 % |
c |     38719 |   93901   327210 |  111266   38405  1127551    29.4 | 25.307 % |
c |     58182 |   93719   326586 |  122393   57845  2484955    43.0 | 25.440 % |
c |     87375 |   93659   326386 |  134632   87030  2988827    34.3 | 25.487 % |
c |    131164 |   93612   326227 |  148095  130814  5137483    39.3 | 25.530 % |
c |    196849 |   93578   326117 |  162905   68955  2299344    33.3 | 25.561 % |
c |    295376 |   93442   325669 |  179196  167463  6223482    37.2 | 25.677 % |
c |    443165 |   93356   325383 |  197115  156030  4776162    30.6 | 25.750 % |
c |    664848 |   93054   324349 |  216827  206010  7341199    35.6 | 25.995 % |

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/3200/stat): 3200 (minisat+_script) R 3199 3200 31915 0 -1 0 19 0 0 0 0 0 0 0 22 0 1 0 1796444161 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 1 0 0
Raw data (/proc/3200/statm): 174 3 169 147 0 27 0
[pid=3200] 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=3201
New process pid=3202
New process pid=3203
execve syscall for /bin/sed executable
One traced child (pid=3202) 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=3203) exited with status: 0
One traced child (pid=3201) exited with status: 0
New process pid=3204
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc3/normalized-mps-v2-20-10-ran14x18_1.opb

[startup+10.0042 s]
Raw data (loadavg): 0.93 0.97 0.91 2/57 3204
Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3200/statm): 531 226 485 147 0 384 0
[pid=3200] vsize: 2124
Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 2435 0 0 0 974 11 0 0 25 0 1 0 1796444166 10366976 2292 4294967295 134512640 135094434 3221224432 3221223092 134553508 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3204/statm): 2531 2292 145 145 0 2386 0
[pid=3204] vsize: 10124
Current children cumulated CPU time (s) 9.85
Current children cumulated vsize (Kb) 12248

[startup+20.005 s]
Raw data (loadavg): 0.94 0.97 0.91 2/57 3204
Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3200/statm): 531 226 485 147 0 384 0
[pid=3200] vsize: 2124
Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 2488 0 0 0 1973 12 0 0 25 0 1 0 1796444166 10584064 2345 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3204/statm): 2584 2345 145 145 0 2439 0
[pid=3204] vsize: 10336
Current children cumulated CPU time (s) 19.85
Current children cumulated vsize (Kb) 12460

[startup+30.0059 s]
Raw data (loadavg): 0.95 0.97 0.91 2/57 3204
Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3200/statm): 531 226 485 147 0 384 0
[pid=3200] vsize: 2124
Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 2588 0 0 0 2971 13 0 0 25 0 1 0 1796444166 10997760 2445 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3204/statm): 2685 2445 145 145 0 2540 0
[pid=3204] vsize: 10740
Current children cumulated CPU time (s) 29.84
Current children cumulated vsize (Kb) 12864

[startup+40.0067 s]
Raw data (loadavg): 0.96 0.97 0.91 2/57 3204
Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3200/statm): 531 226 485 147 0 384 0
[pid=3200] vsize: 2124
Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 3486 0 0 0 3956 19 0 0 25 0 1 0 1796444166 14696448 3343 4294967295 134512640 135094434 3221224432 3221223044 134563083 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3204/statm): 3588 3343 145 145 0 3443 0
[pid=3204] vsize: 14352
Current children cumulated CPU time (s) 39.75
Current children cumulated vsize (Kb) 16476

[startup+50.0075 s]
Raw data (loadavg): 0.96 0.97 0.91 2/57 3204
Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3200/statm): 531 226 485 147 0 384 0
[pid=3200] vsize: 2124
Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 3699 0 0 0 4953 20 0 0 25 0 1 0 1796444166 15667200 3556 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3204/statm): 3825 3556 145 145 0 3680 0
[pid=3204] vsize: 15300
Current children cumulated CPU time (s) 49.73
Current children cumulated vsize (Kb) 17424

[startup+60.0084 s]
Raw data (loadavg): 0.97 0.97 0.91 2/57 3204
Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3200/statm): 531 226 485 147 0 384 0
[pid=3200] vsize: 2124
Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 4103 0 0 0 5947 24 0 0 25 0 1 0 1796444166 17281024 3960 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3204/statm): 4219 3960 145 145 0 4074 0
[pid=3204] vsize: 16876
Current children cumulated CPU time (s) 59.71
Current children cumulated vsize (Kb) 19000

[startup+70.0092 s]
Raw data (loadavg): 0.97 0.97 0.91 2/57 3204
Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3200/statm): 531 226 485 147 0 384 0
[pid=3200] vsize: 2124
Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 5177 0 0 0 6931 31 0 0 25 0 1 0 1796444166 21635072 5034 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3204/statm): 5282 5034 145 145 0 5137 0
[pid=3204] vsize: 21128
Current children cumulated CPU time (s) 69.62
Current children cumulated vsize (Kb) 23252

[startup+80.01 s]
Raw data (loadavg): 0.98 0.97 0.91 2/57 3204
Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3200/statm): 531 226 485 147 0 384 0
[pid=3200] vsize: 2124
Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 5638 0 0 0 7924 34 0 0 25 0 1 0 1796444166 23498752 5495 4294967295 134512640 135094434 3221224432 3221223088 134558235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3204/statm): 5737 5495 145 145 0 5592 0
[pid=3204] vsize: 22948
Current children cumulated CPU time (s) 79.58
Current children cumulated vsize (Kb) 25072

[startup+90.0109 s]
Raw data (loadavg): 0.98 0.97 0.91 2/57 3204
Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3200/statm): 531 226 485 147 0 384 0
[pid=3200] vsize: 2124
Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 5794 0 0 0 8920 35 0 0 25 0 1 0 1796444166 24375296 5651 4294967295 134512640 135094434 3221224432 3221223088 134557928 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3204/statm): 5951 5651 145 145 0 5806 0
[pid=3204] vsize: 23804
Current children cumulated CPU time (s) 89.55
Current children cumulated vsize (Kb) 25928

[startup+100.011 s]
Raw data (loadavg): 0.98 0.97 0.91 2/57 3204
Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3200/statm): 531 226 485 147 0 384 0
[pid=3200] vsize: 2124
Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 6066 0 0 0 9917 37 0 0 25 0 1 0 1796444166 25448448 5923 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3204/statm): 6213 5923 145 145 0 6068 0
[pid=3204] vsize: 24852
Current children cumulated CPU time (s) 99.54
Current children cumulated vsize (Kb) 26976

[startup+110.013 s]
Raw data (loadavg): 0.98 0.97 0.91 2/57 3204
Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3200/statm): 531 226 485 147 0 384 0
[pid=3200] vsize: 2124
Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 6479 0 0 0 10909 40 0 0 25 0 1 0 1796444166 27095040 6336 4294967295 134512640 135094434 3221224432 3221223088 134557903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3204/statm): 6615 6336 145 145 0 6470 0
[pid=3204] vsize: 26460
Current children cumulated CPU time (s) 109.49
Current children cumulated vsize (Kb) 28584

[startup+120.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3204
Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3200/statm): 531 226 485 147 0 384 0
[pid=3200] vsize: 2124
Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 7433 0 0 0 11896 45 0 0 25 0 1 0 1796444166 30941184 7290 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3204/statm): 7554 7290 145 145 0 7409 0
[pid=3204] vsize: 30216
Current children cumulated CPU time (s) 119.41
Current children cumulated vsize (Kb) 32340

[startup+130.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3204
Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3200/statm): 531 226 485 147 0 384 0
[pid=3200] vsize: 2124
Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 7923 0 0 0 12888 49 0 0 25 0 1 0 1796444166 32907264 7780 4294967295 134512640 135094434 3221224432 3221223072 134562104 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3204/statm): 8034 7780 145 145 0 7889 0
[pid=3204] vsize: 32136
Current children cumulated CPU time (s) 129.37
Current children cumulated vsize (Kb) 34260

[startup+140.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3204
Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3200/statm): 531 226 485 147 0 384 0
[pid=3200] vsize: 2124
Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 8616 0 0 0 13877 53 0 0 25 0 1 0 1796444166 35704832 8473 4294967295 134512640 135094434 3221224432 3221223088 134557890 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3204/statm): 8717 8473 145 145 0 8572 0
[pid=3204] vsize: 34868
Current children cumulated CPU time (s) 139.3
Current children cumulated vsize (Kb) 36992

[startup+150.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3204
Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3200/statm): 531 226 485 147 0 384 0
[pid=3200] vsize: 2124
Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 9183 0 0 0 14870 57 0 0 25 0 1 0 1796444166 38522880 9040 4294967295 134512640 135094434 3221224432 3221223088 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3204/statm): 9405 9040 145 145 0 9260 0
[pid=3204] vsize: 37620
Current children cumulated CPU time (s) 149.27
Current children cumulated vsize (Kb) 39744

[startup+160.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3204
Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3200/statm): 531 226 485 147 0 384 0
[pid=3200] vsize: 2124
Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 9392 0 0 0 15868 58 0 0 25 0 1 0 1796444166 39350272 9249 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3204/statm): 9607 9249 145 145 0 9462 0
[pid=3204] vsize: 38428
Current children cumulated CPU time (s) 159.26
Current children cumulated vsize (Kb) 40552

[startup+170.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3204
Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3200/statm): 531 226 485 147 0 384 0
[pid=3200] vsize: 2124
Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 9599 0 0 0 16865 59 0 0 25 0 1 0 1796444166 40165376 9456 4294967295 134512640 135094434 3221224432 3221223088 134557860 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3204/statm): 9806 9456 145 145 0 9661 0
[pid=3204] vsize: 39224
Current children cumulated CPU time (s) 169.24
Current children cumulated vsize (Kb) 41348

[startup+180.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3204
Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3200/statm): 531 226 485 147 0 384 0
[pid=3200] vsize: 2124
Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 9666 0 0 0 17864 60 0 0 25 0 1 0 1796444166 40431616 9523 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3204/statm): 9871 9523 145 145 0 9726 0
[pid=3204] vsize: 39484
Current children cumulated CPU time (s) 179.24
Current children cumulated vsize (Kb) 41608

[startup+190.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3204
Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3200/statm): 531 226 485 147 0 384 0
[pid=3200] vsize: 2124
Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 9666 0 0 0 18864 60 0 0 25 0 1 0 1796444166 40431616 9523 4294967295 134512640 135094434 3221224432 3221223088 134557972 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3204/statm): 9871 9523 145 145 0 9726 0
[pid=3204] vsize: 39484
Current children cumulated CPU time (s) 189.24
Current children cumulated vsize (Kb) 41608

[startup+200.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3204
Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3200/statm): 531 226 485 147 0 384 0
[pid=3200] vsize: 2124
Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 9666 0 0 0 19864 60 0 0 25 0 1 0 1796444166 40431616 9523 4294967295 134512640 135094434 3221224432 3221223068 134557560 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3204/statm): 9871 9523 145 145 0 9726 0
[pid=3204] vsize: 39484
Current children cumulated CPU time (s) 199.24
Current children cumulated vsize (Kb) 41608

[startup+210.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3204
Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3200/statm): 531 226 485 147 0 384 0
[pid=3200] vsize: 2124
Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 9666 0 0 0 20865 60 0 0 25 0 1 0 1796444166 40431616 9523 4294967295 134512640 135094434 3221224432 3221223160 134554333 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3204/statm): 9871 9523 145 145 0 9726 0
[pid=3204] vsize: 39484
Current children cumulated CPU time (s) 209.25
Current children cumulated vsize (Kb) 41608

[startup+220.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3204
Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3200/statm): 531 226 485 147 0 384 0
[pid=3200] vsize: 2124
Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 9666 0 0 0 21865 60 0 0 25 0 1 0 1796444166 40431616 9523 4294967295 134512640 135094434 3221224432 3221223072 134562088 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3204/statm): 9871 9523 145 145 0 9726 0
[pid=3204] vsize: 39484
Current children cumulated CPU time (s) 219.25
Current children cumulated vsize (Kb) 41608

[startup+230.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3204
Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3200/statm): 531 226 485 147 0 384 0
[pid=3200] vsize: 2124
Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 9666 0 0 0 22865 60 0 0 25 0 1 0 1796444166 40431616 9523 4294967295 134512640 135094434 3221224432 3221223088 134557928 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3204/statm): 9871 9523 145 145 0 9726 0
[pid=3204] vsize: 39484
Current children cumulated CPU time (s) 229.25
Current children cumulated vsize (Kb) 41608

[startup+240.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3204
Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3200/statm): 531 226 485 147 0 384 0
[pid=3200] vsize: 2124
Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 9666 0 0 0 23865 60 0 0 25 0 1 0 1796444166 40431616 9523 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3204/statm): 9871 9523 145 145 0 9726 0
[pid=3204] vsize: 39484
Current children cumulated CPU time (s) 239.25
Current children cumulated vsize (Kb) 41608

[startup+250.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3204
Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3200/statm): 531 226 485 147 0 384 0
[pid=3200] vsize: 2124
Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 9666 0 0 0 24865 60 0 0 25 0 1 0 1796444166 40431616 9523 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3204/statm): 9871 9523 145 145 0 9726 0
[pid=3204] vsize: 39484
Current children cumulated CPU time (s) 249.25
Current children cumulated vsize (Kb) 41608

[startup+260.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3204
Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3200/statm): 531 226 485 147 0 384 0
[pid=3200] vsize: 2124
Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 9666 0 0 0 25865 61 0 0 25 0 1 0 1796444166 40431616 9523 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3204/statm): 9871 9523 145 145 0 9726 0
[pid=3204] vsize: 39484
Current children cumulated CPU time (s) 259.26
Current children cumulated vsize (Kb) 41608

[startup+270.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3204
Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3200/statm): 531 226 485 147 0 384 0
[pid=3200] vsize: 2124
Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 9666 0 0 0 26865 61 0 0 25 0 1 0 1796444166 40431616 9523 4294967295 134512640 135094434 3221224432 3221223044 134563083 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3204/statm): 9871 9523 145 145 0 9726 0
[pid=3204] vsize: 39484
Current children cumulated CPU time (s) 269.26
Current children cumulated vsize (Kb) 41608

[startup+280.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3204
Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3200/statm): 531 226 485 147 0 384 0
[pid=3200] vsize: 2124
Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 9666 0 0 0 27865 61 0 0 25 0 1 0 1796444166 40431616 9523 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3204/statm): 9871 9523 145 145 0 9726 0
[pid=3204] vsize: 39484
Current children cumulated CPU time (s) 279.26
Current children cumulated vsize (Kb) 41608

[startup+290.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3204
Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3200/statm): 531 226 485 147 0 384 0
[pid=3200] vsize: 2124
Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 10038 0 0 0 28860 63 0 0 25 0 1 0 1796444166 41975808 9895 4294967295 134512640 135094434 3221224432 3221223088 134557900 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3204/statm): 10248 9895 145 145 0 10103 0
[pid=3204] vsize: 40992
Current children cumulated CPU time (s) 289.23
Current children cumulated vsize (Kb) 43116

[startup+300.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3204
Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3200/statm): 531 226 485 147 0 384 0
[pid=3200] vsize: 2124
Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 10625 0 0 0 29851 67 0 0 25 0 1 0 1796444166 44400640 10482 4294967295 134512640 135094434 3221224432 3221223088 134557846 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3204/statm): 10840 10482 145 145 0 10695 0
[pid=3204] vsize: 43360
Current children cumulated CPU time (s) 299.18
Current children cumulated vsize (Kb) 45484

[startup+310.031 s]
Raw data (loadavg): 0.99 0.97 0.91 1/57 3204
Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3200/statm): 531 226 485 147 0 384 0
[pid=3200] vsize: 2124
Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) T 3200 3200 31915 0 -1 0 10960 0 0 0 30846 69 0 0 25 0 1 0 1796444166 45740032 10817 4294967295 134512640 135094434 3221224432 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/3204/statm): 11167 10817 145 145 0 11022 0
[pid=3204] vsize: 44668
Current children cumulated CPU time (s) 309.15
Current children cumulated vsize (Kb) 46792

[startup+320.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3204
Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3200/statm): 531 226 485 147 0 384 0
[pid=3200] vsize: 2124
Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 11158 0 0 0 31844 71 0 0 25 0 1 0 1796444166 46534656 11015 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3204/statm): 11361 11015 145 145 0 11216 0
[pid=3204] vsize: 45444
Current children cumulated CPU time (s) 319.15
Current children cumulated vsize (Kb) 47568

[startup+330.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3204
Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3200/statm): 531 226 485 147 0 384 0
[pid=3200] vsize: 2124
Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 11302 0 0 0 32842 72 0 0 25 0 1 0 1796444166 47108096 11159 4294967295 134512640 135094434 3221224432 3221223088 134557804 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3204/statm): 11501 11159 145 145 0 11356 0
[pid=3204] vsize: 46004
Current children cumulated CPU time (s) 329.14
Current children cumulated vsize (Kb) 48128

[startup+340.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3204
Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3200/statm): 531 226 485 147 0 384 0
[pid=3200] vsize: 2124
Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 11573 0 0 0 33836 74 0 0 25 0 1 0 1796444166 48181248 11430 4294967295 134512640 135094434 3221224432 3221223044 134563083 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3204/statm): 11763 11430 145 145 0 11618 0
[pid=3204] vsize: 47052
Current children cumulated CPU time (s) 339.1
Current children cumulated vsize (Kb) 49176

[startup+350.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3204
Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3200/statm): 531 226 485 147 0 384 0
[pid=3200] vsize: 2124
Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 11676 0 0 0 34834 75 0 0 25 0 1 0 1796444166 48586752 11533 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3204/statm): 11862 11533 145 145 0 11717 0
[pid=3204] vsize: 47448
Current children cumulated CPU time (s) 349.09
Current children cumulated vsize (Kb) 49572

[startup+360.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3204
Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3200/statm): 531 226 485 147 0 384 0
[pid=3200] vsize: 2124
Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 11676 0 0 0 35834 75 0 0 25 0 1 0 1796444166 48586752 11533 4294967295 134512640 135094434 3221224432 3221223072 134562104 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3204/statm): 11862 11533 145 145 0 11717 0
[pid=3204] vsize: 47448
Current children cumulated CPU time (s) 359.09
Current children cumulated vsize (Kb) 49572

[startup+370.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3204
Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3200/statm): 531 226 485 147 0 384 0
[pid=3200] vsize: 2124
Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 11676 0 0 0 36834 75 0 0 25 0 1 0 1796444166 48586752 11533 4294967295 134512640 135094434 3221224432 3221223044 134563061 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3204/statm): 11862 11533 145 145 0 11717 0
[pid=3204] vsize: 47448
Current children cumulated CPU time (s) 369.09
Current children cumulated vsize (Kb) 49572

[startup+380.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3204
Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3200/statm): 531 226 485 147 0 384 0
[pid=3200] vsize: 2124
Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 11676 0 0 0 37835 75 0 0 25 0 1 0 1796444166 48586752 11533 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3204/statm): 11862 11533 145 145 0 11717 0
[pid=3204] vsize: 47448
Current children cumulated CPU time (s) 379.1
Current children cumulated vsize (Kb) 49572

[startup+390.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3204
Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3200/statm): 531 226 485 147 0 384 0
[pid=3200] vsize: 2124
Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 11676 0 0 0 38835 75 0 0 25 0 1 0 1796444166 48586752 11533 4294967295 134512640 135094434 3221224432 3221223088 134557903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3204/statm): 11862 11533 145 145 0 11717 0
[pid=3204] vsize: 47448
Current children cumulated CPU time (s) 389.1
Current children cumulated vsize (Kb) 49572

[startup+400.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3204
Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3200/statm): 531 226 485 147 0 384 0
[pid=3200] vsize: 2124
Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 11676 0 0 0 39835 75 0 0 25 0 1 0 1796444166 48586752 11533 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3204/statm): 11862 11533 145 145 0 11717 0
[pid=3204] vsize: 47448
Current children cumulated CPU time (s) 399.1
Current children cumulated vsize (Kb) 49572

[startup+410.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3204
Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3200/statm): 531 226 485 147 0 384 0
[pid=3200] vsize: 2124
Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 11676 0 0 0 40835 75 0 0 25 0 1 0 1796444166 48586752 11533 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3204/statm): 11862 11533 145 145 0 11717 0
[pid=3204] vsize: 47448
Current children cumulated CPU time (s) 409.1
Current children cumulated vsize (Kb) 49572

[startup+420.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3204
Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3200/statm): 531 226 485 147 0 384 0
[pid=3200] vsize: 2124
Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 11676 0 0 0 41836 75 0 0 25 0 1 0 1796444166 48586752 11533 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3204/statm): 11862 11533 145 145 0 11717 0
[pid=3204] vsize: 47448
Current children cumulated CPU time (s) 419.11
Current children cumulated vsize (Kb) 49572

[startup+430.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3204
Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3200/statm): 531 226 485 147 0 384 0
[pid=3200] vsize: 2124
Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 11676 0 0 0 42836 75 0 0 25 0 1 0 1796444166 48586752 11533 4294967295 134512640 135094434 3221224432 3221223104 134556266 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3204/statm): 11862 11533 145 145 0 11717 0
[pid=3204] vsize: 47448
Current children cumulated CPU time (s) 429.11
Current children cumulated vsize (Kb) 49572

[startup+440.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3204
Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3200/statm): 531 226 485 147 0 384 0
[pid=3200] vsize: 2124
Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 11676 0 0 0 43836 75 0 0 25 0 1 0 1796444166 48586752 11533 4294967295 134512640 135094434 3221224432 3221223044 134563121 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3204/statm): 11862 11533 145 145 0 11717 0
[pid=3204] vsize: 47448
Current children cumulated CPU time (s) 439.11
Current children cumulated vsize (Kb) 49572

[startup+450.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3204
Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3200/statm): 531 226 485 147 0 384 0
[pid=3200] vsize: 2124
Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 11676 0 0 0 44836 75 0 0 25 0 1 0 1796444166 48586752 11533 4294967295 134512640 135094434 3221224432 3221223044 134563094 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3204/statm): 11862 11533 145 145 0 11717 0
[pid=3204] vsize: 47448
Current children cumulated CPU time (s) 449.11
Current children cumulated vsize (Kb) 49572

[startup+460.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3204
Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3200/statm): 531 226 485 147 0 384 0
[pid=3200] vsize: 2124
Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 11676 0 0 0 45837 75 0 0 25 0 1 0 1796444166 48586752 11533 4294967295 134512640 135094434 3221224432 3221223056 134557685 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3204/statm): 11862 11533 145 145 0 11717 0
[pid=3204] vsize: 47448
Current children cumulated CPU time (s) 459.12
Current children cumulated vsize (Kb) 49572

[startup+470.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3204
Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3200/statm): 531 226 485 147 0 384 0
[pid=3200] vsize: 2124
Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 11676 0 0 0 46837 75 0 0 25 0 1 0 1796444166 48586752 11533 4294967295 134512640 135094434 3221224432 3221223072 134562104 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3204/statm): 11862 11533 145 145 0 11717 0
[pid=3204] vsize: 47448
Current children cumulated CPU time (s) 469.12
Current children cumulated vsize (Kb) 49572

[startup+480.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3204
Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3200/statm): 531 226 485 147 0 384 0
[pid=3200] vsize: 2124
Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 11676 0 0 0 47836 75 0 0 25 0 1 0 1796444166 48586752 11533 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3204/statm): 11862 11533 145 145 0 11717 0
[pid=3204] vsize: 47448
Current children cumulated CPU time (s) 479.11
Current children cumulated vsize (Kb) 49572

[startup+490.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3204
Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3200/statm): 531 226 485 147 0 384 0
[pid=3200] vsize: 2124
Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 11676 0 0 0 48836 75 0 0 25 0 1 0 1796444166 48586752 11533 4294967295 134512640 135094434 3221224432 3221223044 134563055 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3204/statm): 11862 11533 145 145 0 11717 0
[pid=3204] vsize: 47448
Current children cumulated CPU time (s) 489.11
Current children cumulated vsize (Kb) 49572

[startup+500.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3204
Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3200/statm): 531 226 485 147 0 384 0
[pid=3200] vsize: 2124
Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 11676 0 0 0 49836 75 0 0 25 0 1 0 1796444166 48586752 11533 4294967295 134512640 135094434 3221224432 3221223088 134557900 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3204/statm): 11862 11533 145 145 0 11717 0
[pid=3204] vsize: 47448
Current children cumulated CPU time (s) 499.11
Current children cumulated vsize (Kb) 49572

[startup+510.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3204
Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3200/statm): 531 226 485 147 0 384 0
[pid=3200] vsize: 2124
Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 11910 0 0 0 50832 77 0 0 25 0 1 0 1796444166 49532928 11767 4294967295 134512640 135094434 3221224432 3221223088 134557972 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3204/statm): 12093 11767 145 145 0 11948 0
[pid=3204] vsize: 48372
Current children cumulated CPU time (s) 509.09
Current children cumulated vsize (Kb) 50496

[startup+520.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3204
Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3200/statm): 531 226 485 147 0 384 0
[pid=3200] vsize: 2124
Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 12098 0 0 0 51830 78 0 0 25 0 1 0 1796444166 50278400 11955 4294967295 134512640 135094434 3221224432 3221223088 134561460 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3204/statm): 12275 11955 145 145 0 12130 0
[pid=3204] vsize: 49100
Current children cumulated CPU time (s) 519.08
Current children cumulated vsize (Kb) 51224

[startup+530.051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3204
Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3200/statm): 531 226 485 147 0 384 0
[pid=3200] vsize: 2124
Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 12220 0 0 0 52828 79 0 0 25 0 1 0 1796444166 50761728 12077 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3204/statm): 12393 12077 145 145 0 12248 0
[pid=3204] vsize: 49572
Current children cumulated CPU time (s) 529.07
Current children cumulated vsize (Kb) 51696

[startup+540.053 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3204
Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3200/statm): 531 226 485 147 0 384 0
[pid=3200] vsize: 2124
Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 12232 0 0 0 53828 79 0 0 25 0 1 0 1796444166 50806784 12089 4294967295 134512640 135094434 3221224432 3221223088 134558227 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3204/statm): 12404 12089 145 145 0 12259 0
[pid=3204] vsize: 49616
Current children cumulated CPU time (s) 539.07
Current children cumulated vsize (Kb) 51740

[startup+550.053 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3204
Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3200/statm): 531 226 485 147 0 384 0
[pid=3200] vsize: 2124
Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 12232 0 0 0 54829 79 0 0 25 0 1 0 1796444166 50806784 12089 4294967295 134512640 135094434 3221224432 3221223044 134563046 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3204/statm): 12404 12089 145 145 0 12259 0
[pid=3204] vsize: 49616
Current children cumulated CPU time (s) 549.08
Current children cumulated vsize (Kb) 51740

[startup+560.054 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3204
Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3200/statm): 531 226 485 147 0 384 0
[pid=3200] vsize: 2124
Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 12232 0 0 0 55829 79 0 0 25 0 1 0 1796444166 50806784 12089 4294967295 134512640 135094434 3221224432 3221223088 134558235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3204/statm): 12404 12089 145 145 0 12259 0
[pid=3204] vsize: 49616
Current children cumulated CPU time (s) 559.08
Current children cumulated vsize (Kb) 51740

[startup+570.055 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3204
Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3200/statm): 531 226 485 147 0 384 0
[pid=3200] vsize: 2124
Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 12232 0 0 0 56829 79 0 0 25 0 1 0 1796444166 50806784 12089 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3204/statm): 12404 12089 145 145 0 12259 0
[pid=3204] vsize: 49616
Current children cumulated CPU time (s) 569.08
Current children cumulated vsize (Kb) 51740

[startup+580.055 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3204
Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3200/statm): 531 226 485 147 0 384 0
[pid=3200] vsize: 2124
Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 12232 0 0 0 57829 79 0 0 25 0 1 0 1796444166 50806784 12089 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3204/statm): 12404 12089 145 145 0 12259 0
[pid=3204] vsize: 49616
Current children cumulated CPU time (s) 579.08
Current children cumulated vsize (Kb) 51740

[startup+590.056 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3204
Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3200/statm): 531 226 485 147 0 384 0
[pid=3200] vsize: 2124
Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 12232 0 0 0 58829 79 0 0 25 0 1 0 1796444166 50806784 12089 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3204/statm): 12404 12089 145 145 0 12259 0
[pid=3204] vsize: 49616
Current children cumulated CPU time (s) 589.08
Current children cumulated vsize (Kb) 51740

[startup+600.057 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3204
Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3200/statm): 531 226 485 147 0 384 0
[pid=3200] vsize: 2124
Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 12232 0 0 0 59830 79 0 0 25 0 1 0 1796444166 50806784 12089 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3204/statm): 12404 12089 145 145 0 12259 0
[pid=3204] vsize: 49616
Current children cumulated CPU time (s) 599.09
Current children cumulated vsize (Kb) 51740

[startup+610.058 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3204
Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3200/statm): 531 226 485 147 0 384 0
[pid=3200] vsize: 2124
Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 12232 0 0 0 60830 79 0 0 25 0 1 0 1796444166 50806784 12089 4294967295 134512640 135094434 3221224432 3221223088 134558398 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3204/statm): 12404 12089 145 145 0 12259 0
[pid=3204] vsize: 49616
Current children cumulated CPU time (s) 609.09
Current children cumulated vsize (Kb) 51740

[startup+620.059 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3204
Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3200/statm): 531 226 485 147 0 384 0
[pid=3200] vsize: 2124
Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 12232 0 0 0 61830 79 0 0 25 0 1 0 1796444166 50806784 12089 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3204/statm): 12404 12089 145 145 0 12259 0
[pid=3204] vsize: 49616
Current children cumulated CPU time (s) 619.09
Current children cumulated vsize (Kb) 51740

[startup+630.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3204
Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3200/statm): 531 226 485 147 0 384 0
[pid=3200] vsize: 2124
Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 12232 0 0 0 62830 79 0 0 25 0 1 0 1796444166 50806784 12089 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3204/statm): 12404 12089 145 145 0 12259 0
[pid=3204] vsize: 49616
Current children cumulated CPU time (s) 629.09
Current children cumulated vsize (Kb) 51740

[startup+640.061 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3204
Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3200/statm): 531 226 485 147 0 384 0
[pid=3200] vsize: 2124
Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 12232 0 0 0 63830 79 0 0 25 0 1 0 1796444166 50806784 12089 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3204/statm): 12404 12089 145 145 0 12259 0
[pid=3204] vsize: 49616
Current children cumulated CPU time (s) 639.09
Current children cumulated vsize (Kb) 51740

[startup+650.062 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3204
Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3200/statm): 531 226 485 147 0 384 0
[pid=3200] vsize: 2124
Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 12232 0 0 0 64831 79 0 0 25 0 1 0 1796444166 50806784 12089 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3204/statm): 12404 12089 145 145 0 12259 0
[pid=3204] vsize: 49616
Current children cumulated CPU time (s) 649.1
Current children cumulated vsize (Kb) 51740

[startup+660.063 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3204
Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3200/statm): 531 226 485 147 0 384 0
[pid=3200] vsize: 2124
Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 12232 0 0 0 65831 79 0 0 25 0 1 0 1796444166 50806784 12089 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3204/statm): 12404 12089 145 145 0 12259 0
[pid=3204] vsize: 49616
Current children cumulated CPU time (s) 659.1
Current children cumulated vsize (Kb) 51740

[startup+670.063 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3204
Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3200/statm): 531 226 485 147 0 384 0
[pid=3200] vsize: 2124
Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 12232 0 0 0 66831 79 0 0 25 0 1 0 1796444166 50806784 12089 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3204/statm): 12404 12089 145 145 0 12259 0
[pid=3204] vsize: 49616
Current children cumulated CPU time (s) 669.1
Current children cumulated vsize (Kb) 51740

[startup+680.064 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3204
Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3200/statm): 531 226 485 147 0 384 0
[pid=3200] vsize: 2124
Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 12232 0 0 0 67831 79 0 0 25 0 1 0 1796444166 50806784 12089 4294967295 134512640 135094434 3221224432 3221223088 134557859 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3204/statm): 12404 12089 145 145 0 12259 0
[pid=3204] vsize: 49616
Current children cumulated CPU time (s) 679.1
Current children cumulated vsize (Kb) 51740

[startup+690.065 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3204
Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3200/statm): 531 226 485 147 0 384 0
[pid=3200] vsize: 2124
Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 12232 0 0 0 68831 79 0 0 25 0 1 0 1796444166 50806784 12089 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3204/statm): 12404 12089 145 145 0 12259 0
[pid=3204] vsize: 49616
Current children cumulated CPU time (s) 689.1
Current children cumulated vsize (Kb) 51740

[startup+700.065 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3204
Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3200/statm): 531 226 485 147 0 384 0
[pid=3200] vsize: 2124
Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 12232 0 0 0 69832 79 0 0 25 0 1 0 1796444166 50806784 12089 4294967295 134512640 135094434 3221224432 3221223104 134555755 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3204/statm): 12404 12089 145 145 0 12259 0
[pid=3204] vsize: 49616
Current children cumulated CPU time (s) 699.11
Current children cumulated vsize (Kb) 51740

[startup+710.067 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3204
Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3200/statm): 531 226 485 147 0 384 0
[pid=3200] vsize: 2124
Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 12232 0 0 0 70832 79 0 0 25 0 1 0 1796444166 50806784 12089 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3204/statm): 12404 12089 145 145 0 12259 0
[pid=3204] vsize: 49616
Current children cumulated CPU time (s) 709.11
Current children cumulated vsize (Kb) 51740

[startup+720.068 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3204
Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3200/statm): 531 226 485 147 0 384 0
[pid=3200] vsize: 2124
Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 12950 0 0 0 71820 84 0 0 25 0 1 0 1796444166 53747712 12807 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3204/statm): 13122 12807 145 145 0 12977 0
[pid=3204] vsize: 52488
Current children cumulated CPU time (s) 719.04
Current children cumulated vsize (Kb) 54612

[startup+730.069 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3204
Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3200/statm): 531 226 485 147 0 384 0
[pid=3200] vsize: 2124
Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 13742 0 0 0 72808 90 0 0 25 0 1 0 1796444166 56995840 13599 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3204/statm): 13915 13599 145 145 0 13770 0
[pid=3204] vsize: 55660
Current children cumulated CPU time (s) 728.98
Current children cumulated vsize (Kb) 57784

[startup+740.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3204
Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3200/statm): 531 226 485 147 0 384 0
[pid=3200] vsize: 2124
Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 13873 0 0 0 73805 92 0 0 25 0 1 0 1796444166 57511936 13730 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3204/statm): 14041 13730 145 145 0 13896 0
[pid=3204] vsize: 56164
Current children cumulated CPU time (s) 738.97
Current children cumulated vsize (Kb) 58288

[startup+750.071 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3204
Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3200/statm): 531 226 485 147 0 384 0
[pid=3200] vsize: 2124
Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 14065 0 0 0 74801 93 0 0 25 0 1 0 1796444166 58273792 13922 4294967295 134512640 135094434 3221224432 3221223044 134563046 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3204/statm): 14227 13922 145 145 0 14082 0
[pid=3204] vsize: 56908
Current children cumulated CPU time (s) 748.94
Current children cumulated vsize (Kb) 59032

[startup+760.072 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3204
Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3200/statm): 531 226 485 147 0 384 0
[pid=3200] vsize: 2124
Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 14163 0 0 0 75800 93 0 0 25 0 1 0 1796444166 58654720 14020 4294967295 134512640 135094434 3221224432 3221223024 134551434 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3204/statm): 14320 14020 145 145 0 14175 0
[pid=3204] vsize: 57280
Current children cumulated CPU time (s) 758.93
Current children cumulated vsize (Kb) 59404

[startup+770.073 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3204
Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3200/statm): 531 226 485 147 0 384 0
[pid=3200] vsize: 2124
Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 14163 0 0 0 76800 93 0 0 25 0 1 0 1796444166 58654720 14020 4294967295 134512640 135094434 3221224432 3221223056 134562104 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3204/statm): 14320 14020 145 145 0 14175 0
[pid=3204] vsize: 57280
Current children cumulated CPU time (s) 768.93
Current children cumulated vsize (Kb) 59404

[startup+780.074 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3204
Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3200/statm): 531 226 485 147 0 384 0
[pid=3200] vsize: 2124
Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 14163 0 0 0 77800 93 0 0 25 0 1 0 1796444166 58654720 14020 4294967295 134512640 135094434 3221224432 3221223088 134557900 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3204/statm): 14320 14020 145 145 0 14175 0
[pid=3204] vsize: 57280
Current children cumulated CPU time (s) 778.93
Current children cumulated vsize (Kb) 59404

[startup+790.075 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3204
Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3200/statm): 531 226 485 147 0 384 0
[pid=3200] vsize: 2124
Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 14163 0 0 0 78801 93 0 0 25 0 1 0 1796444166 58654720 14020 4294967295 134512640 135094434 3221224432 3221223100 134550364 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3204/statm): 14320 14020 145 145 0 14175 0
[pid=3204] vsize: 57280
Current children cumulated CPU time (s) 788.94
Current children cumulated vsize (Kb) 59404

[startup+800.075 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3204
Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3200/statm): 531 226 485 147 0 384 0
[pid=3200] vsize: 2124
Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 14163 0 0 0 79801 93 0 0 25 0 1 0 1796444166 58654720 14020 4294967295 134512640 135094434 3221224432 3221223088 134558218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3204/statm): 14320 14020 145 145 0 14175 0
[pid=3204] vsize: 57280
Current children cumulated CPU time (s) 798.94
Current children cumulated vsize (Kb) 59404

[startup+810.076 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3204
Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3200/statm): 531 226 485 147 0 384 0
[pid=3200] vsize: 2124
Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 14163 0 0 0 80801 94 0 0 25 0 1 0 1796444166 58654720 14020 4294967295 134512640 135094434 3221224432 3221223088 134561757 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3204/statm): 14320 14020 145 145 0 14175 0
[pid=3204] vsize: 57280
Current children cumulated CPU time (s) 808.95
Current children cumulated vsize (Kb) 59404

[startup+820.077 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3204
Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3200/statm): 531 226 485 147 0 384 0
[pid=3200] vsize: 2124
Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 14163 0 0 0 81801 94 0 0 25 0 1 0 1796444166 58654720 14020 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3204/statm): 14320 14020 145 145 0 14175 0
[pid=3204] vsize: 57280
Current children cumulated CPU time (s) 818.95
Current children cumulated vsize (Kb) 59404

[startup+830.078 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3204
Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3200/statm): 531 226 485 147 0 384 0
[pid=3200] vsize: 2124
Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 14163 0 0 0 82801 94 0 0 25 0 1 0 1796444166 58654720 14020 4294967295 134512640 135094434 3221224432 3221223088 134558126 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3204/statm): 14320 14020 145 145 0 14175 0
[pid=3204] vsize: 57280
Current children cumulated CPU time (s) 828.95
Current children cumulated vsize (Kb) 59404

[startup+840.079 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3204
Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3200/statm): 531 226 485 147 0 384 0
[pid=3200] vsize: 2124
Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 14163 0 0 0 83801 94 0 0 25 0 1 0 1796444166 58654720 14020 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3204/statm): 14320 14020 145 145 0 14175 0
[pid=3204] vsize: 57280
Current children cumulated CPU time (s) 838.95
Current children cumulated vsize (Kb) 59404

[startup+850.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3204
Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3200/statm): 531 226 485 147 0 384 0
[pid=3200] vsize: 2124
Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 14163 0 0 0 84802 94 0 0 25 0 1 0 1796444166 58654720 14020 4294967295 134512640 135094434 3221224432 3221223056 134557616 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3204/statm): 14320 14020 145 145 0 14175 0
[pid=3204] vsize: 57280
Current children cumulated CPU time (s) 848.96
Current children cumulated vsize (Kb) 59404

[startup+860.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3204
Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3200/statm): 531 226 485 147 0 384 0
[pid=3200] vsize: 2124
Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 14163 0 0 0 85802 94 0 0 25 0 1 0 1796444166 58654720 14020 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3204/statm): 14320 14020 145 145 0 14175 0
[pid=3204] vsize: 57280
Current children cumulated CPU time (s) 858.96
Current children cumulated vsize (Kb) 59404

[startup+870.081 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3204
Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3200/statm): 531 226 485 147 0 384 0
[pid=3200] vsize: 2124
Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 14163 0 0 0 86802 94 0 0 25 0 1 0 1796444166 58654720 14020 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3204/statm): 14320 14020 145 145 0 14175 0
[pid=3204] vsize: 57280
Current children cumulated CPU time (s) 868.96
Current children cumulated vsize (Kb) 59404

[startup+880.081 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3204
Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3200/statm): 531 226 485 147 0 384 0
[pid=3200] vsize: 2124
Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 14163 0 0 0 87802 94 0 0 25 0 1 0 1796444166 58654720 14020 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3204/statm): 14320 14020 145 145 0 14175 0
[pid=3204] vsize: 57280
Current children cumulated CPU time (s) 878.96
Current children cumulated vsize (Kb) 59404

[startup+890.083 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3204
Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3200/statm): 531 226 485 147 0 384 0
[pid=3200] vsize: 2124
Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 14163 0 0 0 88802 94 0 0 25 0 1 0 1796444166 58654720 14020 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3204/statm): 14320 14020 145 145 0 14175 0
[pid=3204] vsize: 57280
Current children cumulated CPU time (s) 888.96
Current children cumulated vsize (Kb) 59404

[startup+900.084 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3204
Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3200/statm): 531 226 485 147 0 384 0
[pid=3200] vsize: 2124
Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 14163 0 0 0 89802 94 0 0 25 0 1 0 1796444166 58654720 14020 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3204/statm): 14320 14020 145 145 0 14175 0
[pid=3204] vsize: 57280
Current children cumulated CPU time (s) 898.96
Current children cumulated vsize (Kb) 59404

[startup+910.085 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3204
Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3200/statm): 531 226 485 147 0 384 0
[pid=3200] vsize: 2124
Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 14163 0 0 0 90802 94 0 0 25 0 1 0 1796444166 58654720 14020 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3204/statm): 14320 14020 145 145 0 14175 0
[pid=3204] vsize: 57280
Current children cumulated CPU time (s) 908.96
Current children cumulated vsize (Kb) 59404

[startup+920.085 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3204
Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3200/statm): 531 226 485 147 0 384 0
[pid=3200] vsize: 2124
Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 15121 0 0 0 91790 98 0 0 25 0 1 0 1796444166 62590976 14978 4294967295 134512640 135094434 3221224432 3221223104 134556252 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3204/statm): 15281 14978 145 145 0 15136 0
[pid=3204] vsize: 61124
Current children cumulated CPU time (s) 918.88
Current children cumulated vsize (Kb) 63248

[startup+930.086 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3204
Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3200/statm): 531 226 485 147 0 384 0
[pid=3200] vsize: 2124
Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) T 3200 3200 31915 0 -1 0 16382 0 0 0 92768 108 0 0 25 0 1 0 1796444166 67760128 16239 4294967295 134512640 135094434 3221224432 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/3204/statm): 16543 16239 145 145 0 16398 0
[pid=3204] vsize: 66172
Current children cumulated CPU time (s) 928.76
Current children cumulated vsize (Kb) 68296

[startup+940.087 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3204
Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3200/statm): 531 226 485 147 0 384 0
[pid=3200] vsize: 2124
Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) T 3200 3200 31915 0 -1 0 17339 0 0 0 93752 114 0 0 25 0 1 0 1796444166 71684096 17196 4294967295 134512640 135094434 3221224432 3221222796 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/3204/statm): 17501 17196 145 145 0 17356 0
[pid=3204] vsize: 70004
Current children cumulated CPU time (s) 938.66
Current children cumulated vsize (Kb) 72128

[startup+950.087 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3204
Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3200/statm): 531 226 485 147 0 384 0
[pid=3200] vsize: 2124
Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 18244 0 0 0 94738 121 0 0 25 0 1 0 1796444166 75419648 18101 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3204/statm): 18413 18101 145 145 0 18268 0
[pid=3204] vsize: 73652
Current children cumulated CPU time (s) 948.59
Current children cumulated vsize (Kb) 75776

[startup+960.089 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3204
Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3200/statm): 531 226 485 147 0 384 0
[pid=3200] vsize: 2124
Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 19257 0 0 0 95722 127 0 0 25 0 1 0 1796444166 79568896 19114 4294967295 134512640 135094434 3221224432 3221223088 134557884 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3204/statm): 19426 19114 145 145 0 19281 0
[pid=3204] vsize: 77704
Current children cumulated CPU time (s) 958.49
Current children cumulated vsize (Kb) 79828

[startup+970.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3204
Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3200/statm): 531 226 485 147 0 384 0
[pid=3200] vsize: 2124
Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 20240 0 0 0 96708 134 0 0 25 0 1 0 1796444166 83615744 20097 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3204/statm): 20414 20097 145 145 0 20269 0
[pid=3204] vsize: 81656
Current children cumulated CPU time (s) 968.42
Current children cumulated vsize (Kb) 83780

[startup+980.091 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3204
Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3200/statm): 531 226 485 147 0 384 0
[pid=3200] vsize: 2124
Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 21193 0 0 0 97693 141 0 0 25 0 1 0 1796444166 87531520 21050 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3204/statm): 21370 21050 145 145 0 21225 0
[pid=3204] vsize: 85480
Current children cumulated CPU time (s) 978.34
Current children cumulated vsize (Kb) 87604

[startup+990.092 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3204
Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3200/statm): 531 226 485 147 0 384 0
[pid=3200] vsize: 2124
Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 21948 0 0 0 98679 147 0 0 25 0 1 0 1796444166 90644480 21805 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3204/statm): 22130 21805 145 145 0 21985 0
[pid=3204] vsize: 88520
Current children cumulated CPU time (s) 988.26
Current children cumulated vsize (Kb) 90644

[startup+1000.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3204
Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3200/statm): 531 226 485 147 0 384 0
[pid=3200] vsize: 2124
Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 22772 0 0 0 99665 152 0 0 25 0 1 0 1796444166 94101504 22629 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3204/statm): 22974 22629 145 145 0 22829 0
[pid=3204] vsize: 91896
Current children cumulated CPU time (s) 998.17
Current children cumulated vsize (Kb) 94020

[startup+1010.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3204
Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3200/statm): 531 226 485 147 0 384 0
[pid=3200] vsize: 2124
Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 23605 0 0 0 100650 158 0 0 25 0 1 0 1796444166 97554432 23462 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3204/statm): 23817 23462 145 145 0 23672 0
[pid=3204] vsize: 95268
Current children cumulated CPU time (s) 1008.08
Current children cumulated vsize (Kb) 97392

[startup+1020.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3204
Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3200/statm): 531 226 485 147 0 384 0
[pid=3200] vsize: 2124
Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 24385 0 0 0 101635 164 0 0 25 0 1 0 1796444166 100737024 24242 4294967295 134512640 135094434 3221224432 3221223104 134556252 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3204/statm): 24594 24242 145 145 0 24449 0
[pid=3204] vsize: 98376
Current children cumulated CPU time (s) 1017.99
Current children cumulated vsize (Kb) 100500

[startup+1030.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3204
Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3200/statm): 531 226 485 147 0 384 0
[pid=3200] vsize: 2124
Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 25222 0 0 0 102621 170 0 0 25 0 1 0 1796444166 104173568 25079 4294967295 134512640 135094434 3221224432 3221223104 134556252 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3204/statm): 25433 25079 145 145 0 25288 0
[pid=3204] vsize: 101732
Current children cumulated CPU time (s) 1027.91
Current children cumulated vsize (Kb) 103856

[startup+1040.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3204
Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3200/statm): 531 226 485 147 0 384 0
[pid=3200] vsize: 2124
Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 26098 0 0 0 103606 176 0 0 25 0 1 0 1796444166 107769856 25955 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3204/statm): 26311 25955 145 145 0 26166 0
[pid=3204] vsize: 105244
Current children cumulated CPU time (s) 1037.82
Current children cumulated vsize (Kb) 107368

[startup+1050.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3204
Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3200/statm): 531 226 485 147 0 384 0
[pid=3200] vsize: 2124
Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 26841 0 0 0 104594 181 0 0 25 0 1 0 1796444166 110833664 26698 4294967295 134512640 135094434 3221224432 3221223088 134558016 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3204/statm): 27059 26698 145 145 0 26914 0
[pid=3204] vsize: 108236
Current children cumulated CPU time (s) 1047.75
Current children cumulated vsize (Kb) 110360

[startup+1060.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3204
Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3200/statm): 531 226 485 147 0 384 0
[pid=3200] vsize: 2124
Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 27516 0 0 0 105579 187 0 0 25 0 1 0 1796444166 113590272 27373 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3204/statm): 27732 27373 145 145 0 27587 0
[pid=3204] vsize: 110928
Current children cumulated CPU time (s) 1057.66
Current children cumulated vsize (Kb) 113052

[startup+1070.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3204
Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3200/statm): 531 226 485 147 0 384 0
[pid=3200] vsize: 2124
Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 28171 0 0 0 106567 193 0 0 25 0 1 0 1796444166 116244480 28028 4294967295 134512640 135094434 3221224432 3221223088 134558004 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3204/statm): 28380 28028 145 145 0 28235 0
[pid=3204] vsize: 113520
Current children cumulated CPU time (s) 1067.6
Current children cumulated vsize (Kb) 115644

[startup+1080.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3204
Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3200/statm): 531 226 485 147 0 384 0
[pid=3200] vsize: 2124
Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 28846 0 0 0 107556 198 0 0 25 0 1 0 1796444166 119037952 28703 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3204/statm): 29062 28703 145 145 0 28917 0
[pid=3204] vsize: 116248
Current children cumulated CPU time (s) 1077.54
Current children cumulated vsize (Kb) 118372

[startup+1090.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3204
Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3200/statm): 531 226 485 147 0 384 0
[pid=3200] vsize: 2124
Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 29442 0 0 0 108547 201 0 0 25 0 1 0 1796444166 121458688 29299 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3204/statm): 29653 29299 145 145 0 29508 0
[pid=3204] vsize: 118612
Current children cumulated CPU time (s) 1087.48
Current children cumulated vsize (Kb) 120736

[startup+1100.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3204
Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3200/statm): 531 226 485 147 0 384 0
[pid=3200] vsize: 2124
Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 30064 0 0 0 109537 206 0 0 25 0 1 0 1796444166 124006400 29921 4294967295 134512640 135094434 3221224432 3221223088 134558007 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3204/statm): 30275 29921 145 145 0 30130 0
[pid=3204] vsize: 121100
Current children cumulated CPU time (s) 1097.43
Current children cumulated vsize (Kb) 123224

[startup+1110.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3204
Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3200/statm): 531 226 485 147 0 384 0
[pid=3200] vsize: 2124
Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 30145 0 0 0 110536 206 0 0 25 0 1 0 1796444166 124358656 30002 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3204/statm): 30361 30002 145 145 0 30216 0
[pid=3204] vsize: 121444
Current children cumulated CPU time (s) 1107.42
Current children cumulated vsize (Kb) 123568

[startup+1120.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3204
Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3200/statm): 531 226 485 147 0 384 0
[pid=3200] vsize: 2124
Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 30145 0 0 0 111537 206 0 0 25 0 1 0 1796444166 124358656 30002 4294967295 134512640 135094434 3221224432 3221223088 134558126 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3204/statm): 30361 30002 145 145 0 30216 0
[pid=3204] vsize: 121444
Current children cumulated CPU time (s) 1117.43
Current children cumulated vsize (Kb) 123568

[startup+1130.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3204
Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3200/statm): 531 226 485 147 0 384 0
[pid=3200] vsize: 2124
Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 30145 0 0 0 112537 206 0 0 25 0 1 0 1796444166 124358656 30002 4294967295 134512640 135094434 3221224432 3221223044 134563055 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3204/statm): 30361 30002 145 145 0 30216 0
[pid=3204] vsize: 121444
Current children cumulated CPU time (s) 1127.43
Current children cumulated vsize (Kb) 123568

[startup+1140.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3204
Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3200/statm): 531 226 485 147 0 384 0
[pid=3200] vsize: 2124
Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 30145 0 0 0 113537 206 0 0 25 0 1 0 1796444166 124358656 30002 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3204/statm): 30361 30002 145 145 0 30216 0
[pid=3204] vsize: 121444
Current children cumulated CPU time (s) 1137.43
Current children cumulated vsize (Kb) 123568

[startup+1150.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3204
Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3200/statm): 531 226 485 147 0 384 0
[pid=3200] vsize: 2124
Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 30145 0 0 0 114537 206 0 0 25 0 1 0 1796444166 124358656 30002 4294967295 134512640 135094434 3221224432 3221223088 134557875 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3204/statm): 30361 30002 145 145 0 30216 0
[pid=3204] vsize: 121444
Current children cumulated CPU time (s) 1147.43
Current children cumulated vsize (Kb) 123568

[startup+1160.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3204
Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3200/statm): 531 226 485 147 0 384 0
[pid=3200] vsize: 2124
Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 30145 0 0 0 115538 206 0 0 25 0 1 0 1796444166 124358656 30002 4294967295 134512640 135094434 3221224432 3221223044 134563066 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3204/statm): 30361 30002 145 145 0 30216 0
[pid=3204] vsize: 121444
Current children cumulated CPU time (s) 1157.44
Current children cumulated vsize (Kb) 123568

[startup+1170.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3204
Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3200/statm): 531 226 485 147 0 384 0
[pid=3200] vsize: 2124
Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 30145 0 0 0 116538 206 0 0 25 0 1 0 1796444166 124358656 30002 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3204/statm): 30361 30002 145 145 0 30216 0
[pid=3204] vsize: 121444
Current children cumulated CPU time (s) 1167.44
Current children cumulated vsize (Kb) 123568

[startup+1180.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3204
Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3200/statm): 531 226 485 147 0 384 0
[pid=3200] vsize: 2124
Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 30145 0 0 0 117538 206 0 0 25 0 1 0 1796444166 124358656 30002 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3204/statm): 30361 30002 145 145 0 30216 0
[pid=3204] vsize: 121444
Current children cumulated CPU time (s) 1177.44
Current children cumulated vsize (Kb) 123568

[startup+1190.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3204
Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3200/statm): 531 226 485 147 0 384 0
[pid=3200] vsize: 2124
Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 30145 0 0 0 118538 206 0 0 25 0 1 0 1796444166 124358656 30002 4294967295 134512640 135094434 3221224432 3221223044 134563061 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3204/statm): 30361 30002 145 145 0 30216 0
[pid=3204] vsize: 121444
Current children cumulated CPU time (s) 1187.44
Current children cumulated vsize (Kb) 123568

[startup+1200.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3204
Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3200/statm): 531 226 485 147 0 384 0
[pid=3200] vsize: 2124
Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 30145 0 0 0 119539 206 0 0 25 0 1 0 1796444166 124358656 30002 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3204/statm): 30361 30002 145 145 0 30216 0
[pid=3204] vsize: 121444
Current children cumulated CPU time (s) 1197.45
Current children cumulated vsize (Kb) 123568

[startup+1210.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3204
Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3200/statm): 531 226 485 147 0 384 0
[pid=3200] vsize: 2124
Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 30145 0 0 0 120539 206 0 0 25 0 1 0 1796444166 124358656 30002 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3204/statm): 30361 30002 145 145 0 30216 0
[pid=3204] vsize: 121444
Current children cumulated CPU time (s) 1207.45
Current children cumulated vsize (Kb) 123568



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3204
Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3200/statm): 531 226 485 147 0 384 0
[pid=3200] vsize: 2124
Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 30145 0 0 0 120539 206 0 0 25 0 1 0 1796444166 124358656 30002 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3204/statm): 30361 30002 145 145 0 30216 0
[pid=3204] vsize: 121444
Current children cumulated CPU time (s) 1207.45
Current children cumulated vsize (Kb) 123568

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

Child status: 0
Real time (s): 1210.17
CPU time (s): 1207.51
CPU user time (s): 1205.39
CPU system time (s): 2.12068
CPU usage (%): 99.7803
Max. virtual memory (cumulated for all children) (Kb): 123568

Verifier Data

ERROR: no interpretation found !