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/fctp/normalized-mps-v2-20-10-ran12x21.opb
MD5SUM592fea06f126ca9b3a8a014f1e413b01
Bench Categoryoptimization, big integers (OPTBIGINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function 10017866
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 1543007621731
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 1543007621731
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 benchmark1228.5
Number of variables7812
Total number of constraints285
Number of constraints which are clauses0
Number of constraints which are cardinality constraints (but not clauses)0
Number of constraints which are nor clauses,nor cardinality constraints285
Minimum length of a constraint31
Maximum length of a constraint630

Trace number 4581

Launcher Data

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.020
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:        920920 kB
Buffers:         19900 kB
Cached:          64424 kB
SwapCached:        676 kB
Active:          10524 kB
Inactive:        76224 kB
HighTotal:      131008 kB
HighFree:        63420 kB
LowTotal:       903652 kB
LowFree:        857500 kB
SwapTotal:     2097892 kB
SwapFree:      2096528 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5704 kB
Slab:            21172 kB
Committed_AS:    64132 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-09-19 18:57:23 (client local time) WITH STATUS 0 IN 1208.24 SECONDS
stats: 3042 7 1208.24 0

Solver Data

c Parsing PB file...
c Converting 318 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: #################################
c   -- Clauses(.)/Splits(s): (none)
c ---[ 316]---> Adder-cost: 548   maxlim: 356331   bits: 19/19
c ---[ 314]---> Adder-cost: 548   maxlim: 361451   bits: 19/19
c ---[ 312]---> Adder-cost: 554   maxlim: 446443   bits: 19/19
c ---[ 310]---> Adder-cost: 548   maxlim: 355307   bits: 19/19
c ---[ 308]---> Adder-cost: 548   maxlim: 349163   bits: 19/19
c ---[ 306]---> Adder-cost: 548   maxlim: 350187   bits: 19/19
c ---[ 304]---> Adder-cost: 548   maxlim: 354283   bits: 19/19
c ---[ 302]---> Adder-cost: 532   maxlim: 235499   bits: 18/18
c ---[ 300]---> Adder-cost: 548   maxlim: 357355   bits: 19/19
c ---[ 298]---> Adder-cost: 548   maxlim: 360427   bits: 19/19
c ---[ 296]---> Adder-cost: 554   maxlim: 414699   bits: 19/19
c ---[ 294]---> Adder-cost: 532   maxlim: 236523   bits: 18/18
c ---[ 292]---> Adder-cost: 264   maxlim: 47092   bits: 16/16
c ---[ 290]---> Adder-cost: 308   maxlim: 188404   bits: 18/18
c ---[ 288]---> Adder-cost: 264   maxlim: 46068   bits: 16/16
c ---[ 286]---> Adder-cost: 328   maxlim: 338932   bits: 19/19
c ---[ 284]---> Adder-cost: 264   maxlim: 47092   bits: 16/16
c ---[ 282]---> Adder-cost: 328   maxlim: 330740   bits: 19/19
c ---[ 280]---> Adder-cost: 286   maxlim: 93172   bits: 17/17
c ---[ 278]---> Adder-cost: 332   maxlim: 374772   bits: 19/19
c ---[ 276]---> Adder-cost: 308   maxlim: 187380   bits: 18/18
c ---[ 274]---> Adder-cost: 286   maxlim: 91124   bits: 17/17
c ---[ 272]---> Adder-cost: 328   maxlim: 332788   bits: 19/19
c ---[ 270]---> Adder-cost: 286   maxlim: 91124   bits: 17/17
c ---[ 268]---> Adder-cost: 264   maxlim: 47092   bits: 16/16
c ---[ 266]---> Adder-cost: 328   maxlim: 332788   bits: 19/19
c ---[ 264]---> Adder-cost: 264   maxlim: 46068   bits: 16/16
c ---[ 262]---> Adder-cost: 328   maxlim: 340980   bits: 19/19
c ---[ 260]---> Adder-cost: 286   maxlim: 93172   bits: 17/17
c ---[ 258]---> Adder-cost: 308   maxlim: 181236   bits: 18/18
c ---[ 256]---> Adder-cost: 332   maxlim: 387060   bits: 19/19
c ---[ 254]---> Adder-cost: 332   maxlim: 393204   bits: 19/19
c ---[ 252]---> Adder-cost: 308   maxlim: 187380   bits: 18/18
c ---[ 251]---> BDD-cost:   13
c ---[ 250]---> BDD-cost:   15
c ---[ 249]---> BDD-cost:   14
c ---[ 248]---> BDD-cost:   18
c ---[ 247]---> BDD-cost:   16
c ---[ 246]---> BDD-cost:   19
c ---[ 245]---> BDD-cost:   16
c ---[ 244]---> BDD-cost:   19
c ---[ 243]---> BDD-cost:   13
c ---[ 242]---> BDD-cost:   15
c ---[ 241]---> BDD-cost:   13
c ---[ 240]---> BDD-cost:   14
c ---[ 239]---> BDD-cost:   17
c ---[ 238]---> BDD-cost:   20
c ---[ 237]---> BDD-cost:   16
c ---[ 236]---> BDD-cost:   17
c ---[ 235]---> BDD-cost:   17
c ---[ 234]---> BDD-cost:   17
c ---[ 233]---> BDD-cost:   18
c ---[ 232]---> BDD-cost:   14
c ---[ 231]---> BDD-cost:   17
c ---[ 230]---> BDD-cost:   13
c ---[ 229]---> BDD-cost:   17
c ---[ 228]---> BDD-cost:   16
c ---[ 227]---> BDD-cost:   13
c ---[ 226]---> BDD-cost:   17
c ---[ 225]---> BDD-cost:   18
c ---[ 224]---> BDD-cost:   16
c ---[ 223]---> BDD-cost:   17
c ---[ 222]---> BDD-cost:   16
c ---[ 221]---> BDD-cost:   17
c ---[ 220]---> BDD-cost:   13
c ---[ 219]---> BDD-cost:   15
c ---[ 218]---> BDD-cost:   13
c ---[ 217]---> BDD-cost:   14
c ---[ 216]---> BDD-cost:   17
c ---[ 215]---> BDD-cost:   20
c ---[ 214]---> BDD-cost:   16
c ---[ 213]---> BDD-cost:   18
c ---[ 212]---> BDD-cost:   20
c ---[ 211]---> BDD-cost:   20
c ---[ 210]---> BDD-cost:   18
c ---[ 209]---> BDD-cost:   14
c ---[ 208]---> BDD-cost:   20
c ---[ 207]---> BDD-cost:   13
c ---[ 206]---> BDD-cost:   20
c ---[ 205]---> BDD-cost:   16
c ---[ 204]---> BDD-cost:   16
c ---[ 203]---> BDD-cost:   20
c ---[ 202]---> BDD-cost:   18
c ---[ 201]---> BDD-cost:   16
c ---[ 200]---> BDD-cost:   20
c ---[ 199]---> BDD-cost:   16
c ---[ 198]---> BDD-cost:   20
c ---[ 197]---> BDD-cost:   13
c ---[ 196]---> BDD-cost:   15
c ---[ 195]---> BDD-cost:   13
c ---[ 194]---> BDD-cost:   17
c ---[ 193]---> BDD-cost:   14
c ---[ 192]---> BDD-cost:   20
c ---[ 191]---> BDD-cost:   16
c ---[ 190]---> BDD-cost:   18
c ---[ 189]---> BDD-cost:   18
c ---[ 188]---> BDD-cost:   18
c ---[ 187]---> BDD-cost:   18
c ---[ 186]---> BDD-cost:   14
c ---[ 185]---> BDD-cost:   18
c ---[ 184]---> BDD-cost:   13
c ---[ 183]---> BDD-cost:   18
c ---[ 182]---> BDD-cost:   18
c ---[ 181]---> BDD-cost:   16
c ---[ 180]---> BDD-cost:   18
c ---[ 179]---> BDD-cost:   18
c ---[ 178]---> BDD-cost:   16
c ---[ 177]---> BDD-cost:   18
c ---[ 176]---> BDD-cost:   16
c ---[ 175]---> BDD-cost:   18
c ---[ 174]---> BDD-cost:   13
c ---[ 173]---> BDD-cost:   15
c ---[ 172]---> BDD-cost:   16
c ---[ 171]---> BDD-cost:   13
c ---[ 170]---> BDD-cost:   14
c ---[ 169]---> BDD-cost:   20
c ---[ 168]---> BDD-cost:   16
c ---[ 167]---> BDD-cost:   18
c ---[ 166]---> BDD-cost:   21
c ---[ 165]---> BDD-cost:   17
c ---[ 164]---> BDD-cost:   18
c ---[ 163]---> BDD-cost:   14
c ---[ 162]---> BDD-cost:   20
c ---[ 161]---> BDD-cost:   17
c ---[ 160]---> BDD-cost:   13
c ---[ 159]---> BDD-cost:   20
c ---[ 158]---> BDD-cost:   16
c ---[ 157]---> BDD-cost:   21
c ---[ 156]---> BDD-cost:   18
c ---[ 155]---> BDD-cost:   16
c ---[ 154]---> BDD-cost:   20
c ---[ 153]---> BDD-cost:   16
c ---[ 152]---> BDD-cost:   20
c ---[ 151]---> BDD-cost:   13
c ---[ 150]---> BDD-cost:   16
c ---[ 149]---> BDD-cost:   15
c ---[ 148]---> BDD-cost:   13
c ---[ 147]---> BDD-cost:   14
c ---[ 146]---> BDD-cost:   18
c ---[ 145]---> BDD-cost:   16
c ---[ 144]---> BDD-cost:   18
c ---[ 143]---> BDD-cost:   18
c ---[ 142]---> BDD-cost:   18
c ---[ 141]---> BDD-cost:   18
c ---[ 140]---> BDD-cost:   14
c ---[ 139]---> BDD-cost:   13
c ---[ 138]---> BDD-cost:   17
c ---[ 137]---> BDD-cost:   18
c ---[ 136]---> BDD-cost:   13
c ---[ 135]---> BDD-cost:   18
c ---[ 134]---> BDD-cost:   16
c ---[ 133]---> BDD-cost:   18
c ---[ 132]---> BDD-cost:   18
c ---[ 131]---> BDD-cost:   16
c ---[ 130]---> BDD-cost:   18
c ---[ 129]---> BDD-cost:   16
c ---[ 128]---> BDD-cost:   18
c ---[ 127]---> BDD-cost:   13
c ---[ 126]---> BDD-cost:   13
c ---[ 125]---> BDD-cost:   15
c ---[ 124]---> BDD-cost:   13
c ---[ 123]---> BDD-cost:   14
c ---[ 122]---> BDD-cost:   20
c ---[ 121]---> BDD-cost:   16
c ---[ 120]---> BDD-cost:   18
c ---[ 119]---> BDD-cost:   17
c ---[ 118]---> BDD-cost:   17
c ---[ 117]---> BDD-cost:   18
c ---[ 116]---> BDD-cost:   15
c ---[ 115]---> BDD-cost:   14
c ---[ 114]---> BDD-cost:   20
c ---[ 113]---> BDD-cost:   13
c ---[ 112]---> BDD-cost:   20
c ---[ 111]---> BDD-cost:   16
c ---[ 110]---> BDD-cost:   17
c ---[ 109]---> BDD-cost:   18
c ---[ 108]---> BDD-cost:   16
c ---[ 107]---> BDD-cost:   20
c ---[ 106]---> BDD-cost:   16
c ---[ 105]---> BDD-cost:   13
c ---[ 104]---> BDD-cost:   20
c ---[ 103]---> BDD-cost:   13
c ---[ 102]---> BDD-cost:   15
c ---[ 101]---> BDD-cost:   13
c ---[ 100]---> BDD-cost:   14
c ---[  99]---> BDD-cost:   20
c ---[  98]---> BDD-cost:   16
c ---[  97]---> BDD-cost:   18
c ---[  96]---> BDD-cost:   20
c ---[  95]---> BDD-cost:   20
c ---[  94]---> BDD-cost:   14
c ---[  93]---> BDD-cost:   18
c ---[  92]---> BDD-cost:   14
c ---[  91]---> BDD-cost:   20
c ---[  90]---> BDD-cost:   13
c ---[  89]---> BDD-cost:   20
c ---[  88]---> BDD-cost:   16
c ---[  87]---> BDD-cost:   20
c ---[  86]---> BDD-cost:   18
c ---[  85]---> BDD-cost:   16
c ---[  84]---> BDD-cost:   20
c ---[  83]---> BDD-cost:   20
c ---[  82]---> BDD-cost:   16
c ---[  81]---> BDD-cost:   20
c ---[  80]---> BDD-cost:   16
c ---[  79]---> BDD-cost:   18
c ---[  78]---> BDD-cost:   20
c ---[  77]---> BDD-cost:   20
c ---[  76]---> BDD-cost:   14
c ---[  75]---> BDD-cost:   18
c ---[  74]---> BDD-cost:   14
c ---[  73]---> BDD-cost:   20
c ---[  72]---> BDD-cost:   13
c ---[  71]---> BDD-cost:   20
c ---[  70]---> BDD-cost:   16
c ---[  69]---> BDD-cost:   20
c ---[  68]---> BDD-cost:   18
c ---[  67]---> BDD-cost:   16
c ---[  66]---> BDD-cost:   20
c ---[  65]---> BDD-cost:   20
c ---[  64]---> BDD-cost:   16
c ---[  63]---> BDD-cost:   20
c ---[  62]---> BDD-cost:   13
c ---[  61]---> BDD-cost:   15
c ---[  60]---> BDD-cost:   13
c ---[  59]---> BDD-cost:   14
c ---[  58]---> BDD-cost:   20
c ---[  57]---> BDD-cost:   16
c ---[  56]---> BDD-cost:   18
c ---[  55]---> BDD-cost:   20
c ---[  54]---> BDD-cost:   16
c ---[  53]---> BDD-cost:   20
c ---[  52]---> BDD-cost:   18
c ---[  51]---> BDD-cost:   14
c ---[  50]---> BDD-cost:   20
c ---[  49]---> BDD-cost:   13
c ---[  48]---> BDD-cost:   20
c ---[  47]---> BDD-cost:   16
c ---[  46]---> BDD-cost:   20
c ---[  45]---> BDD-cost:   18
c ---[  44]---> BDD-cost:   16
c ---[  43]---> BDD-cost:   18
c ---[  42]---> BDD-cost:   20
c ---[  41]---> BDD-cost:   16
c ---[  40]---> BDD-cost:   20
c ---[  39]---> BDD-cost:   13
c ---[  38]---> BDD-cost:   15
c ---[  37]---> BDD-cost:   13
c ---[  36]---> BDD-cost:   14
c ---[  35]---> BDD-cost:   20
c ---[  34]---> BDD-cost:   16
c ---[  33]---> BDD-cost:   18
c ---[  32]---> BDD-cost:   17
c ---[  31]---> BDD-cost:   19
c ---[  30]---> BDD-cost:   19
c ---[  29]---> BDD-cost:   18
c ---[  28]---> BDD-cost:   14
c ---[  27]---> BDD-cost:   20
c ---[  26]---> BDD-cost:   13
c ---[  25]---> BDD-cost:   20
c ---[  24]---> BDD-cost:   16
c ---[  23]---> BDD-cost:   19
c ---[  22]---> BDD-cost:   18
c ---[  21]---> BDD-cost:   17
c ---[  20]---> BDD-cost:   16
c ---[  19]---> BDD-cost:   20
c ---[  18]---> BDD-cost:   16
c ---[  17]---> BDD-cost:   20
c ---[  16]---> BDD-cost:   13
c ---[  15]---> BDD-cost:   15
c ---[  14]---> BDD-cost:   13
c ---[  13]---> BDD-cost:   14
c ---[  12]---> BDD-cost:   20
c ---[  11]---> BDD-cost:   16
c ---[  10]---> BDD-cost:   18
c ---[   9]---> BDD-cost:   18
c ---[   8]---> BDD-cost:   19
c ---[   7]---> BDD-cost:   19
c ---[   6]---> BDD-cost:   18
c ---[   5]---> BDD-cost:   14
c ---[   4]---> BDD-cost:   20
c ---[   3]---> BDD-cost:   13
c ---[   2]---> BDD-cost:   19
c ---[   1]---> BDD-cost:   16
c ---[   0]---> BDD-cost:   19
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   92041   320785 |   30680       0        0     nan |  0.000 % |
c |       100 |   92016   320696 |   33748      96      285     3.0 | 24.788 % |
c |       250 |   91833   320071 |   37122     228      748     3.3 | 24.935 % |
c |       475 |   91732   319720 |   40835     442     1453     3.3 | 25.010 % |
c |       812 |   91523   318995 |   44918     751     2422     3.2 | 25.170 % |
c |      1319 |   91292   318194 |   49410    1228     3919     3.2 | 25.343 % |
c |      2078 |   90925   316925 |   54351    1935     6148     3.2 | 25.614 % |
c |      3217 |   90519   315523 |   59786    3013     9973     3.3 | 25.911 % |
c |      4925 |   90266   314670 |   65765    4685    17820     3.8 | 26.102 % |
c |      7487 |   90134   314226 |   72341    7229    36729     5.1 | 26.208 % |
c |     11331 |   90071   314017 |   79576   11063    63517     5.7 | 26.257 % |
c |     17097 |   90031   313887 |   87533   16824   121353     7.2 | 26.288 % |
c |     25747 |   89950   313612 |   96286   25463   197479     7.8 | 26.350 % |
c |     38721 |   89903   313459 |  105915   38427   579571    15.1 | 26.386 % |
c |     58182 |   89831   313211 |  116507   57880   993219    17.2 | 26.448 % |
c |     87374 |   89768   313000 |  128157   87065  2945483    33.8 | 26.506 % |
c |    131163 |   89745   312925 |  140973  130851  7506718    57.4 | 26.523 % |
c |    196849 |   89519   312159 |  155071   68298  2245227    32.9 | 26.705 % |
c |    295376 |   89439   311891 |  170578   27039  1268265    46.9 | 26.772 % |
c |    443165 |   89190   311082 |  187636  174793  6208804    35.5 | 26.985 % |
c |    664848 |   89015   310505 |  206399   31270  5671313   181.4 | 27.132 % |
c |    997375 |   88904   310138 |  227039  175119  5179968    29.6 | 27.225 % |

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/30555/stat): 30555 (minisat+_script) R 30554 30555 19818 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1852099709 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 1 0 0
Raw data (/proc/30555/statm): 174 3 169 147 0 27 0
[pid=30555] 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=30556
New process pid=30557
New process pid=30558
One traced child (pid=30557) exited with status: 0
execve syscall for /bin/sed executable
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=30558) exited with status: 0
One traced child (pid=30556) exited with status: 0
New process pid=30559
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc29/normalized-mps-v2-20-10-ran12x21.opb

[startup+10.0044 s]
Raw data (loadavg): 0.93 0.95 0.90 2/57 30559
Raw data (/proc/30555/stat): 30555 (minisat+_script) S 30554 30555 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1852099709 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30555/statm): 531 226 485 147 0 384 0
[pid=30555] vsize: 2124
Raw data (/proc/30559/stat): 30559 (minisat+_64-bit) R 30555 30555 19818 0 -1 0 2347 0 0 0 975 11 0 0 25 0 1 0 1852099714 10240000 2205 4294967295 134512640 135094434 3221224432 3221223164 134561658 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30559/statm): 2500 2205 145 145 0 2355 0
[pid=30559] vsize: 10000
Current children cumulated CPU time (s) 9.88
Current children cumulated vsize (Kb) 12124

[startup+20.0052 s]
Raw data (loadavg): 0.94 0.96 0.91 2/57 30559
Raw data (/proc/30555/stat): 30555 (minisat+_script) S 30554 30555 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1852099709 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30555/statm): 531 226 485 147 0 384 0
[pid=30555] vsize: 2124
Raw data (/proc/30559/stat): 30559 (minisat+_64-bit) R 30555 30555 19818 0 -1 0 2405 0 0 0 1973 11 0 0 25 0 1 0 1852099714 10469376 2263 4294967295 134512640 135094434 3221224432 3221223088 134561757 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30559/statm): 2556 2263 145 145 0 2411 0
[pid=30559] vsize: 10224
Current children cumulated CPU time (s) 19.86
Current children cumulated vsize (Kb) 12348

[startup+30.007 s]
Raw data (loadavg): 0.95 0.96 0.91 2/57 30559
Raw data (/proc/30555/stat): 30555 (minisat+_script) S 30554 30555 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1852099709 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30555/statm): 531 226 485 147 0 384 0
[pid=30555] vsize: 2124
Raw data (/proc/30559/stat): 30559 (minisat+_64-bit) R 30555 30555 19818 0 -1 0 2570 0 0 0 2970 13 0 0 25 0 1 0 1852099714 11137024 2428 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30559/statm): 2719 2428 145 145 0 2574 0
[pid=30559] vsize: 10876
Current children cumulated CPU time (s) 29.85
Current children cumulated vsize (Kb) 13000

[startup+40.0078 s]
Raw data (loadavg): 0.95 0.96 0.91 2/57 30559
Raw data (/proc/30555/stat): 30555 (minisat+_script) S 30554 30555 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1852099709 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30555/statm): 531 226 485 147 0 384 0
[pid=30555] vsize: 2124
Raw data (/proc/30559/stat): 30559 (minisat+_64-bit) R 30555 30555 19818 0 -1 0 2736 0 0 0 3966 15 0 0 25 0 1 0 1852099714 11845632 2594 4294967295 134512640 135094434 3221224432 3221223072 134562128 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30559/statm): 2892 2594 145 145 0 2747 0
[pid=30559] vsize: 11568
Current children cumulated CPU time (s) 39.83
Current children cumulated vsize (Kb) 13692

[startup+50.0095 s]
Raw data (loadavg): 0.96 0.96 0.91 2/57 30559
Raw data (/proc/30555/stat): 30555 (minisat+_script) S 30554 30555 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1852099709 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30555/statm): 531 226 485 147 0 384 0
[pid=30555] vsize: 2124
Raw data (/proc/30559/stat): 30559 (minisat+_64-bit) R 30555 30555 19818 0 -1 0 2988 0 0 0 4962 17 0 0 25 0 1 0 1852099714 12840960 2846 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30559/statm): 3135 2846 145 145 0 2990 0
[pid=30559] vsize: 12540
Current children cumulated CPU time (s) 49.81
Current children cumulated vsize (Kb) 14664

[startup+60.0103 s]
Raw data (loadavg): 0.97 0.96 0.91 2/57 30559
Raw data (/proc/30555/stat): 30555 (minisat+_script) S 30554 30555 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1852099709 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30555/statm): 531 226 485 147 0 384 0
[pid=30555] vsize: 2124
Raw data (/proc/30559/stat): 30559 (minisat+_64-bit) R 30555 30555 19818 0 -1 0 3579 0 0 0 5953 21 0 0 25 0 1 0 1852099714 15335424 3437 4294967295 134512640 135094434 3221224432 3221223044 134563059 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30559/statm): 3744 3437 145 145 0 3599 0
[pid=30559] vsize: 14976
Current children cumulated CPU time (s) 59.76
Current children cumulated vsize (Kb) 17100

[startup+70.0111 s]
Raw data (loadavg): 0.97 0.96 0.91 2/57 30559
Raw data (/proc/30555/stat): 30555 (minisat+_script) S 30554 30555 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1852099709 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30555/statm): 531 226 485 147 0 384 0
[pid=30555] vsize: 2124
Raw data (/proc/30559/stat): 30559 (minisat+_64-bit) R 30555 30555 19818 0 -1 0 3940 0 0 0 6946 25 0 0 25 0 1 0 1852099714 16769024 3798 4294967295 134512640 135094434 3221224432 3221223044 134563148 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30559/statm): 4094 3798 145 145 0 3949 0
[pid=30559] vsize: 16376
Current children cumulated CPU time (s) 69.73
Current children cumulated vsize (Kb) 18500

[startup+80.0129 s]
Raw data (loadavg): 0.98 0.96 0.91 2/57 30559
Raw data (/proc/30555/stat): 30555 (minisat+_script) S 30554 30555 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1852099709 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30555/statm): 531 226 485 147 0 384 0
[pid=30555] vsize: 2124
Raw data (/proc/30559/stat): 30559 (minisat+_64-bit) R 30555 30555 19818 0 -1 0 4967 0 0 0 7932 31 0 0 25 0 1 0 1852099714 21192704 4825 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30559/statm): 5174 4825 145 145 0 5029 0
[pid=30559] vsize: 20696
Current children cumulated CPU time (s) 79.65
Current children cumulated vsize (Kb) 22820

[startup+90.0137 s]
Raw data (loadavg): 0.98 0.96 0.91 2/57 30559
Raw data (/proc/30555/stat): 30555 (minisat+_script) S 30554 30555 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1852099709 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30555/statm): 531 226 485 147 0 384 0
[pid=30555] vsize: 2124
Raw data (/proc/30559/stat): 30559 (minisat+_64-bit) R 30555 30555 19818 0 -1 0 5513 0 0 0 8923 35 0 0 25 0 1 0 1852099714 23388160 5371 4294967295 134512640 135094434 3221224432 3221223104 134556244 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30559/statm): 5710 5371 145 145 0 5565 0
[pid=30559] vsize: 22840
Current children cumulated CPU time (s) 89.6
Current children cumulated vsize (Kb) 24964

[startup+100.015 s]
Raw data (loadavg): 0.98 0.96 0.91 2/57 30559
Raw data (/proc/30555/stat): 30555 (minisat+_script) S 30554 30555 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1852099709 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30555/statm): 531 226 485 147 0 384 0
[pid=30555] vsize: 2124
Raw data (/proc/30559/stat): 30559 (minisat+_64-bit) R 30555 30555 19818 0 -1 0 6456 0 0 0 9906 43 0 0 25 0 1 0 1852099714 27201536 6314 4294967295 134512640 135094434 3221224432 3221223044 134563030 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30559/statm): 6641 6314 145 145 0 6496 0
[pid=30559] vsize: 26564
Current children cumulated CPU time (s) 99.51
Current children cumulated vsize (Kb) 28688

[startup+110.015 s]
Raw data (loadavg): 0.98 0.96 0.91 2/57 30559
Raw data (/proc/30555/stat): 30555 (minisat+_script) S 30554 30555 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1852099709 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30555/statm): 531 226 485 147 0 384 0
[pid=30555] vsize: 2124
Raw data (/proc/30559/stat): 30559 (minisat+_64-bit) T 30555 30555 19818 0 -1 0 7578 0 0 0 10888 50 0 0 25 0 1 0 1852099714 31752192 7436 4294967295 134512640 135094434 3221224432 3221222796 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/30559/statm): 7752 7436 145 145 0 7607 0
[pid=30559] vsize: 31008
Current children cumulated CPU time (s) 109.4
Current children cumulated vsize (Kb) 33132

[startup+120.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 30559
Raw data (/proc/30555/stat): 30555 (minisat+_script) S 30554 30555 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1852099709 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30555/statm): 531 226 485 147 0 384 0
[pid=30555] vsize: 2124
Raw data (/proc/30559/stat): 30559 (minisat+_64-bit) T 30555 30555 19818 0 -1 0 8804 0 0 0 11867 59 0 0 25 0 1 0 1852099714 36757504 8662 4294967295 134512640 135094434 3221224432 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/30559/statm): 8974 8662 145 145 0 8829 0
[pid=30559] vsize: 35896
Current children cumulated CPU time (s) 119.28
Current children cumulated vsize (Kb) 38020

[startup+130.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 30559
Raw data (/proc/30555/stat): 30555 (minisat+_script) S 30554 30555 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1852099709 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30555/statm): 531 226 485 147 0 384 0
[pid=30555] vsize: 2124
Raw data (/proc/30559/stat): 30559 (minisat+_64-bit) R 30555 30555 19818 0 -1 0 10331 0 0 0 12844 67 0 0 25 0 1 0 1852099714 42999808 10189 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30559/statm): 10498 10189 145 145 0 10353 0
[pid=30559] vsize: 41992
Current children cumulated CPU time (s) 129.13
Current children cumulated vsize (Kb) 44116

[startup+140.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 30559
Raw data (/proc/30555/stat): 30555 (minisat+_script) S 30554 30555 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1852099709 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30555/statm): 531 226 485 147 0 384 0
[pid=30555] vsize: 2124
Raw data (/proc/30559/stat): 30559 (minisat+_64-bit) T 30555 30555 19818 0 -1 0 11306 0 0 0 13829 74 0 0 25 0 1 0 1852099714 47521792 11164 4294967295 134512640 135094434 3221224432 3221222780 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/30559/statm): 11602 11164 145 145 0 11457 0
[pid=30559] vsize: 46408
Current children cumulated CPU time (s) 139.05
Current children cumulated vsize (Kb) 48532

[startup+150.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 30559
Raw data (/proc/30555/stat): 30555 (minisat+_script) S 30554 30555 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1852099709 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30555/statm): 531 226 485 147 0 384 0
[pid=30555] vsize: 2124
Raw data (/proc/30559/stat): 30559 (minisat+_64-bit) R 30555 30555 19818 0 -1 0 12288 0 0 0 14813 81 0 0 25 0 1 0 1852099714 51519488 12146 4294967295 134512640 135094434 3221224432 3221223024 134556776 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30559/statm): 12578 12146 145 145 0 12433 0
[pid=30559] vsize: 50312
Current children cumulated CPU time (s) 148.96
Current children cumulated vsize (Kb) 52436

[startup+160.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 30559
Raw data (/proc/30555/stat): 30555 (minisat+_script) S 30554 30555 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1852099709 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30555/statm): 531 226 485 147 0 384 0
[pid=30555] vsize: 2124
Raw data (/proc/30559/stat): 30559 (minisat+_64-bit) R 30555 30555 19818 0 -1 0 12852 0 0 0 15804 85 0 0 25 0 1 0 1852099714 53805056 12710 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30559/statm): 13136 12710 145 145 0 12991 0
[pid=30559] vsize: 52544
Current children cumulated CPU time (s) 158.91
Current children cumulated vsize (Kb) 54668

[startup+170.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 30559
Raw data (/proc/30555/stat): 30555 (minisat+_script) S 30554 30555 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1852099709 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30555/statm): 531 226 485 147 0 384 0
[pid=30555] vsize: 2124
Raw data (/proc/30559/stat): 30559 (minisat+_64-bit) R 30555 30555 19818 0 -1 0 12940 0 0 0 16802 85 0 0 25 0 1 0 1852099714 54157312 12798 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30559/statm): 13222 12798 145 145 0 13077 0
[pid=30559] vsize: 52888
Current children cumulated CPU time (s) 168.89
Current children cumulated vsize (Kb) 55012

[startup+180.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 30559
Raw data (/proc/30555/stat): 30555 (minisat+_script) S 30554 30555 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1852099709 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30555/statm): 531 226 485 147 0 384 0
[pid=30555] vsize: 2124
Raw data (/proc/30559/stat): 30559 (minisat+_64-bit) R 30555 30555 19818 0 -1 0 12940 0 0 0 17802 86 0 0 25 0 1 0 1852099714 54157312 12798 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30559/statm): 13222 12798 145 145 0 13077 0
[pid=30559] vsize: 52888
Current children cumulated CPU time (s) 178.9
Current children cumulated vsize (Kb) 55012

[startup+190.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 30559
Raw data (/proc/30555/stat): 30555 (minisat+_script) S 30554 30555 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1852099709 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30555/statm): 531 226 485 147 0 384 0
[pid=30555] vsize: 2124
Raw data (/proc/30559/stat): 30559 (minisat+_64-bit) R 30555 30555 19818 0 -1 0 12940 0 0 0 18802 86 0 0 25 0 1 0 1852099714 54157312 12798 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30559/statm): 13222 12798 145 145 0 13077 0
[pid=30559] vsize: 52888
Current children cumulated CPU time (s) 188.9
Current children cumulated vsize (Kb) 55012

[startup+200.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 30559
Raw data (/proc/30555/stat): 30555 (minisat+_script) S 30554 30555 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1852099709 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30555/statm): 531 226 485 147 0 384 0
[pid=30555] vsize: 2124
Raw data (/proc/30559/stat): 30559 (minisat+_64-bit) R 30555 30555 19818 0 -1 0 12940 0 0 0 19803 86 0 0 25 0 1 0 1852099714 54157312 12798 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30559/statm): 13222 12798 145 145 0 13077 0
[pid=30559] vsize: 52888
Current children cumulated CPU time (s) 198.91
Current children cumulated vsize (Kb) 55012

[startup+210.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 30559
Raw data (/proc/30555/stat): 30555 (minisat+_script) S 30554 30555 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1852099709 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30555/statm): 531 226 485 147 0 384 0
[pid=30555] vsize: 2124
Raw data (/proc/30559/stat): 30559 (minisat+_64-bit) R 30555 30555 19818 0 -1 0 12940 0 0 0 20803 86 0 0 25 0 1 0 1852099714 54157312 12798 4294967295 134512640 135094434 3221224432 3221223044 134563089 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30559/statm): 13222 12798 145 145 0 13077 0
[pid=30559] vsize: 52888
Current children cumulated CPU time (s) 208.91
Current children cumulated vsize (Kb) 55012

[startup+220.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 30559
Raw data (/proc/30555/stat): 30555 (minisat+_script) S 30554 30555 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1852099709 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30555/statm): 531 226 485 147 0 384 0
[pid=30555] vsize: 2124
Raw data (/proc/30559/stat): 30559 (minisat+_64-bit) R 30555 30555 19818 0 -1 0 12940 0 0 0 21803 86 0 0 25 0 1 0 1852099714 54157312 12798 4294967295 134512640 135094434 3221224432 3221223056 134562104 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30559/statm): 13222 12798 145 145 0 13077 0
[pid=30559] vsize: 52888
Current children cumulated CPU time (s) 218.91
Current children cumulated vsize (Kb) 55012

[startup+230.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 30559
Raw data (/proc/30555/stat): 30555 (minisat+_script) S 30554 30555 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1852099709 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30555/statm): 531 226 485 147 0 384 0
[pid=30555] vsize: 2124
Raw data (/proc/30559/stat): 30559 (minisat+_64-bit) R 30555 30555 19818 0 -1 0 12941 0 0 0 22803 86 0 0 25 0 1 0 1852099714 54157312 12799 4294967295 134512640 135094434 3221224432 3221223088 134557928 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30559/statm): 13222 12799 145 145 0 13077 0
[pid=30559] vsize: 52888
Current children cumulated CPU time (s) 228.91
Current children cumulated vsize (Kb) 55012

[startup+240.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 30559
Raw data (/proc/30555/stat): 30555 (minisat+_script) S 30554 30555 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1852099709 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30555/statm): 531 226 485 147 0 384 0
[pid=30555] vsize: 2124
Raw data (/proc/30559/stat): 30559 (minisat+_64-bit) R 30555 30555 19818 0 -1 0 12941 0 0 0 23803 86 0 0 25 0 1 0 1852099714 54157312 12799 4294967295 134512640 135094434 3221224432 3221223088 134558210 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30559/statm): 13222 12799 145 145 0 13077 0
[pid=30559] vsize: 52888
Current children cumulated CPU time (s) 238.91
Current children cumulated vsize (Kb) 55012

[startup+250.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 30559
Raw data (/proc/30555/stat): 30555 (minisat+_script) S 30554 30555 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1852099709 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30555/statm): 531 226 485 147 0 384 0
[pid=30555] vsize: 2124
Raw data (/proc/30559/stat): 30559 (minisat+_64-bit) R 30555 30555 19818 0 -1 0 12941 0 0 0 24804 86 0 0 25 0 1 0 1852099714 54157312 12799 4294967295 134512640 135094434 3221224432 3221223092 134553515 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30559/statm): 13222 12799 145 145 0 13077 0
[pid=30559] vsize: 52888
Current children cumulated CPU time (s) 248.92
Current children cumulated vsize (Kb) 55012

[startup+260.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 30559
Raw data (/proc/30555/stat): 30555 (minisat+_script) S 30554 30555 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1852099709 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30555/statm): 531 226 485 147 0 384 0
[pid=30555] vsize: 2124
Raw data (/proc/30559/stat): 30559 (minisat+_64-bit) R 30555 30555 19818 0 -1 0 12941 0 0 0 25804 86 0 0 25 0 1 0 1852099714 54157312 12799 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30559/statm): 13222 12799 145 145 0 13077 0
[pid=30559] vsize: 52888
Current children cumulated CPU time (s) 258.92
Current children cumulated vsize (Kb) 55012

[startup+270.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 30559
Raw data (/proc/30555/stat): 30555 (minisat+_script) S 30554 30555 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1852099709 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30555/statm): 531 226 485 147 0 384 0
[pid=30555] vsize: 2124
Raw data (/proc/30559/stat): 30559 (minisat+_64-bit) R 30555 30555 19818 0 -1 0 12941 0 0 0 26804 86 0 0 25 0 1 0 1852099714 54157312 12799 4294967295 134512640 135094434 3221224432 3221223104 134556252 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30559/statm): 13222 12799 145 145 0 13077 0
[pid=30559] vsize: 52888
Current children cumulated CPU time (s) 268.92
Current children cumulated vsize (Kb) 55012

[startup+280.028 s]
Raw data (loadavg): 0.99 0.97 0.91 1/57 30559
Raw data (/proc/30555/stat): 30555 (minisat+_script) S 30554 30555 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1852099709 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30555/statm): 531 226 485 147 0 384 0
[pid=30555] vsize: 2124
Raw data (/proc/30559/stat): 30559 (minisat+_64-bit) T 30555 30555 19818 0 -1 0 12986 0 0 0 27803 87 0 0 25 0 1 0 1852099714 54341632 12844 4294967295 134512640 135094434 3221224432 3221222796 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/30559/statm): 13267 12844 145 145 0 13122 0
[pid=30559] vsize: 53068
Current children cumulated CPU time (s) 278.92
Current children cumulated vsize (Kb) 55192

[startup+290.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 30559
Raw data (/proc/30555/stat): 30555 (minisat+_script) S 30554 30555 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1852099709 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30555/statm): 531 226 485 147 0 384 0
[pid=30555] vsize: 2124
Raw data (/proc/30559/stat): 30559 (minisat+_64-bit) R 30555 30555 19818 0 -1 0 13602 0 0 0 28794 91 0 0 25 0 1 0 1852099714 56864768 13460 4294967295 134512640 135094434 3221224432 3221223120 134554723 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30559/statm): 13883 13460 145 145 0 13738 0
[pid=30559] vsize: 55532
Current children cumulated CPU time (s) 288.87
Current children cumulated vsize (Kb) 57656

[startup+300.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 30559
Raw data (/proc/30555/stat): 30555 (minisat+_script) S 30554 30555 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1852099709 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30555/statm): 531 226 485 147 0 384 0
[pid=30555] vsize: 2124
Raw data (/proc/30559/stat): 30559 (minisat+_64-bit) R 30555 30555 19818 0 -1 0 14612 0 0 0 29776 99 0 0 25 0 1 0 1852099714 60989440 14470 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30559/statm): 14890 14470 145 145 0 14745 0
[pid=30559] vsize: 59560
Current children cumulated CPU time (s) 298.77
Current children cumulated vsize (Kb) 61684

[startup+310.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 30559
Raw data (/proc/30555/stat): 30555 (minisat+_script) S 30554 30555 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1852099709 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30555/statm): 531 226 485 147 0 384 0
[pid=30555] vsize: 2124
Raw data (/proc/30559/stat): 30559 (minisat+_64-bit) R 30555 30555 19818 0 -1 0 15329 0 0 0 30764 104 0 0 25 0 1 0 1852099714 63897600 15187 4294967295 134512640 135094434 3221224432 3221223092 134553508 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30559/statm): 15600 15187 145 145 0 15455 0
[pid=30559] vsize: 62400
Current children cumulated CPU time (s) 308.7
Current children cumulated vsize (Kb) 64524

[startup+320.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 30559
Raw data (/proc/30555/stat): 30555 (minisat+_script) S 30554 30555 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1852099709 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30555/statm): 531 226 485 147 0 384 0
[pid=30555] vsize: 2124
Raw data (/proc/30559/stat): 30559 (minisat+_64-bit) R 30555 30555 19818 0 -1 0 15329 0 0 0 31764 104 0 0 25 0 1 0 1852099714 63897600 15187 4294967295 134512640 135094434 3221224432 3221223104 134554891 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30559/statm): 15600 15187 145 145 0 15455 0
[pid=30559] vsize: 62400
Current children cumulated CPU time (s) 318.7
Current children cumulated vsize (Kb) 64524

[startup+330.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 30559
Raw data (/proc/30555/stat): 30555 (minisat+_script) S 30554 30555 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1852099709 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30555/statm): 531 226 485 147 0 384 0
[pid=30555] vsize: 2124
Raw data (/proc/30559/stat): 30559 (minisat+_64-bit) R 30555 30555 19818 0 -1 0 15329 0 0 0 32764 105 0 0 25 0 1 0 1852099714 63897600 15187 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30559/statm): 15600 15187 145 145 0 15455 0
[pid=30559] vsize: 62400
Current children cumulated CPU time (s) 328.71
Current children cumulated vsize (Kb) 64524

[startup+340.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 30559
Raw data (/proc/30555/stat): 30555 (minisat+_script) S 30554 30555 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1852099709 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30555/statm): 531 226 485 147 0 384 0
[pid=30555] vsize: 2124
Raw data (/proc/30559/stat): 30559 (minisat+_64-bit) R 30555 30555 19818 0 -1 0 15329 0 0 0 33764 105 0 0 25 0 1 0 1852099714 63897600 15187 4294967295 134512640 135094434 3221224432 3221223088 134558235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30559/statm): 15600 15187 145 145 0 15455 0
[pid=30559] vsize: 62400
Current children cumulated CPU time (s) 338.71
Current children cumulated vsize (Kb) 64524

[startup+350.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 30559
Raw data (/proc/30555/stat): 30555 (minisat+_script) S 30554 30555 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1852099709 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30555/statm): 531 226 485 147 0 384 0
[pid=30555] vsize: 2124
Raw data (/proc/30559/stat): 30559 (minisat+_64-bit) R 30555 30555 19818 0 -1 0 15329 0 0 0 34764 105 0 0 25 0 1 0 1852099714 63897600 15187 4294967295 134512640 135094434 3221224432 3221223088 134558402 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30559/statm): 15600 15187 145 145 0 15455 0
[pid=30559] vsize: 62400
Current children cumulated CPU time (s) 348.71
Current children cumulated vsize (Kb) 64524

[startup+360.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 30559
Raw data (/proc/30555/stat): 30555 (minisat+_script) S 30554 30555 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1852099709 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30555/statm): 531 226 485 147 0 384 0
[pid=30555] vsize: 2124
Raw data (/proc/30559/stat): 30559 (minisat+_64-bit) R 30555 30555 19818 0 -1 0 15329 0 0 0 35764 105 0 0 25 0 1 0 1852099714 63897600 15187 4294967295 134512640 135094434 3221224432 3221223044 134563007 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30559/statm): 15600 15187 145 145 0 15455 0
[pid=30559] vsize: 62400
Current children cumulated CPU time (s) 358.71
Current children cumulated vsize (Kb) 64524

[startup+370.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 30559
Raw data (/proc/30555/stat): 30555 (minisat+_script) S 30554 30555 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1852099709 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30555/statm): 531 226 485 147 0 384 0
[pid=30555] vsize: 2124
Raw data (/proc/30559/stat): 30559 (minisat+_64-bit) R 30555 30555 19818 0 -1 0 15329 0 0 0 36764 106 0 0 25 0 1 0 1852099714 63897600 15187 4294967295 134512640 135094434 3221224432 3221223084 134561534 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30559/statm): 15600 15187 145 145 0 15455 0
[pid=30559] vsize: 62400
Current children cumulated CPU time (s) 368.72
Current children cumulated vsize (Kb) 64524

[startup+380.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 30559
Raw data (/proc/30555/stat): 30555 (minisat+_script) S 30554 30555 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1852099709 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30555/statm): 531 226 485 147 0 384 0
[pid=30555] vsize: 2124
Raw data (/proc/30559/stat): 30559 (minisat+_64-bit) R 30555 30555 19818 0 -1 0 15329 0 0 0 37764 106 0 0 25 0 1 0 1852099714 63897600 15187 4294967295 134512640 135094434 3221224432 3221223092 134553501 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30559/statm): 15600 15187 145 145 0 15455 0
[pid=30559] vsize: 62400
Current children cumulated CPU time (s) 378.72
Current children cumulated vsize (Kb) 64524

[startup+390.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 30559
Raw data (/proc/30555/stat): 30555 (minisat+_script) S 30554 30555 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1852099709 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30555/statm): 531 226 485 147 0 384 0
[pid=30555] vsize: 2124
Raw data (/proc/30559/stat): 30559 (minisat+_64-bit) R 30555 30555 19818 0 -1 0 15329 0 0 0 38764 106 0 0 25 0 1 0 1852099714 63897600 15187 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30559/statm): 15600 15187 145 145 0 15455 0
[pid=30559] vsize: 62400
Current children cumulated CPU time (s) 388.72
Current children cumulated vsize (Kb) 64524

[startup+400.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 30559
Raw data (/proc/30555/stat): 30555 (minisat+_script) S 30554 30555 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1852099709 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30555/statm): 531 226 485 147 0 384 0
[pid=30555] vsize: 2124
Raw data (/proc/30559/stat): 30559 (minisat+_64-bit) R 30555 30555 19818 0 -1 0 15329 0 0 0 39764 106 0 0 25 0 1 0 1852099714 63897600 15187 4294967295 134512640 135094434 3221224432 3221223120 134554709 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30559/statm): 15600 15187 145 145 0 15455 0
[pid=30559] vsize: 62400
Current children cumulated CPU time (s) 398.72
Current children cumulated vsize (Kb) 64524

[startup+410.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 30559
Raw data (/proc/30555/stat): 30555 (minisat+_script) S 30554 30555 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1852099709 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30555/statm): 531 226 485 147 0 384 0
[pid=30555] vsize: 2124
Raw data (/proc/30559/stat): 30559 (minisat+_64-bit) R 30555 30555 19818 0 -1 0 15330 0 0 0 40764 106 0 0 25 0 1 0 1852099714 63897600 15188 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30559/statm): 15600 15188 145 145 0 15455 0
[pid=30559] vsize: 62400
Current children cumulated CPU time (s) 408.72
Current children cumulated vsize (Kb) 64524

[startup+420.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 30559
Raw data (/proc/30555/stat): 30555 (minisat+_script) S 30554 30555 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1852099709 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30555/statm): 531 226 485 147 0 384 0
[pid=30555] vsize: 2124
Raw data (/proc/30559/stat): 30559 (minisat+_64-bit) R 30555 30555 19818 0 -1 0 15330 0 0 0 41764 106 0 0 25 0 1 0 1852099714 63897600 15188 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30559/statm): 15600 15188 145 145 0 15455 0
[pid=30559] vsize: 62400
Current children cumulated CPU time (s) 418.72
Current children cumulated vsize (Kb) 64524

[startup+430.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 30559
Raw data (/proc/30555/stat): 30555 (minisat+_script) S 30554 30555 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1852099709 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30555/statm): 531 226 485 147 0 384 0
[pid=30555] vsize: 2124
Raw data (/proc/30559/stat): 30559 (minisat+_64-bit) R 30555 30555 19818 0 -1 0 15330 0 0 0 42765 106 0 0 25 0 1 0 1852099714 63897600 15188 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30559/statm): 15600 15188 145 145 0 15455 0
[pid=30559] vsize: 62400
Current children cumulated CPU time (s) 428.73
Current children cumulated vsize (Kb) 64524

[startup+440.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 30559
Raw data (/proc/30555/stat): 30555 (minisat+_script) S 30554 30555 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1852099709 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30555/statm): 531 226 485 147 0 384 0
[pid=30555] vsize: 2124
Raw data (/proc/30559/stat): 30559 (minisat+_64-bit) R 30555 30555 19818 0 -1 0 15330 0 0 0 43765 107 0 0 25 0 1 0 1852099714 63897600 15188 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30559/statm): 15600 15188 145 145 0 15455 0
[pid=30559] vsize: 62400
Current children cumulated CPU time (s) 438.74
Current children cumulated vsize (Kb) 64524

[startup+450.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 30559
Raw data (/proc/30555/stat): 30555 (minisat+_script) S 30554 30555 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1852099709 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30555/statm): 531 226 485 147 0 384 0
[pid=30555] vsize: 2124
Raw data (/proc/30559/stat): 30559 (minisat+_64-bit) R 30555 30555 19818 0 -1 0 15333 0 0 0 44765 107 0 0 25 0 1 0 1852099714 63897600 15191 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30559/statm): 15600 15191 145 145 0 15455 0
[pid=30559] vsize: 62400
Current children cumulated CPU time (s) 448.74
Current children cumulated vsize (Kb) 64524

[startup+460.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 30559
Raw data (/proc/30555/stat): 30555 (minisat+_script) S 30554 30555 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1852099709 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30555/statm): 531 226 485 147 0 384 0
[pid=30555] vsize: 2124
Raw data (/proc/30559/stat): 30559 (minisat+_64-bit) R 30555 30555 19818 0 -1 0 15340 0 0 0 45765 107 0 0 25 0 1 0 1852099714 63897600 15198 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30559/statm): 15600 15198 145 145 0 15455 0
[pid=30559] vsize: 62400
Current children cumulated CPU time (s) 458.74
Current children cumulated vsize (Kb) 64524

[startup+470.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 30559
Raw data (/proc/30555/stat): 30555 (minisat+_script) S 30554 30555 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1852099709 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30555/statm): 531 226 485 147 0 384 0
[pid=30555] vsize: 2124
Raw data (/proc/30559/stat): 30559 (minisat+_64-bit) R 30555 30555 19818 0 -1 0 15346 0 0 0 46765 107 0 0 25 0 1 0 1852099714 63897600 15204 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30559/statm): 15600 15204 145 145 0 15455 0
[pid=30559] vsize: 62400
Current children cumulated CPU time (s) 468.74
Current children cumulated vsize (Kb) 64524

[startup+480.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 30559
Raw data (/proc/30555/stat): 30555 (minisat+_script) S 30554 30555 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1852099709 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30555/statm): 531 226 485 147 0 384 0
[pid=30555] vsize: 2124
Raw data (/proc/30559/stat): 30559 (minisat+_64-bit) R 30555 30555 19818 0 -1 0 15352 0 0 0 47764 108 0 0 25 0 1 0 1852099714 63897600 15210 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30559/statm): 15600 15210 145 145 0 15455 0
[pid=30559] vsize: 62400
Current children cumulated CPU time (s) 478.74
Current children cumulated vsize (Kb) 64524

[startup+490.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 30559
Raw data (/proc/30555/stat): 30555 (minisat+_script) S 30554 30555 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1852099709 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30555/statm): 531 226 485 147 0 384 0
[pid=30555] vsize: 2124
Raw data (/proc/30559/stat): 30559 (minisat+_64-bit) R 30555 30555 19818 0 -1 0 15359 0 0 0 48764 108 0 0 25 0 1 0 1852099714 63897600 15217 4294967295 134512640 135094434 3221224432 3221223044 134563055 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30559/statm): 15600 15217 145 145 0 15455 0
[pid=30559] vsize: 62400
Current children cumulated CPU time (s) 488.74
Current children cumulated vsize (Kb) 64524

[startup+500.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 30559
Raw data (/proc/30555/stat): 30555 (minisat+_script) S 30554 30555 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1852099709 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30555/statm): 531 226 485 147 0 384 0
[pid=30555] vsize: 2124
Raw data (/proc/30559/stat): 30559 (minisat+_64-bit) R 30555 30555 19818 0 -1 0 15368 0 0 0 49765 108 0 0 25 0 1 0 1852099714 63897600 15226 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30559/statm): 15600 15226 145 145 0 15455 0
[pid=30559] vsize: 62400
Current children cumulated CPU time (s) 498.75
Current children cumulated vsize (Kb) 64524

[startup+510.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 30559
Raw data (/proc/30555/stat): 30555 (minisat+_script) S 30554 30555 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1852099709 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30555/statm): 531 226 485 147 0 384 0
[pid=30555] vsize: 2124
Raw data (/proc/30559/stat): 30559 (minisat+_64-bit) R 30555 30555 19818 0 -1 0 15372 0 0 0 50765 108 0 0 25 0 1 0 1852099714 63897600 15230 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30559/statm): 15600 15230 145 145 0 15455 0
[pid=30559] vsize: 62400
Current children cumulated CPU time (s) 508.75
Current children cumulated vsize (Kb) 64524

[startup+520.051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 30559
Raw data (/proc/30555/stat): 30555 (minisat+_script) S 30554 30555 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1852099709 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30555/statm): 531 226 485 147 0 384 0
[pid=30555] vsize: 2124
Raw data (/proc/30559/stat): 30559 (minisat+_64-bit) R 30555 30555 19818 0 -1 0 15372 0 0 0 51765 108 0 0 25 0 1 0 1852099714 63897600 15230 4294967295 134512640 135094434 3221224432 3221223104 134555769 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30559/statm): 15600 15230 145 145 0 15455 0
[pid=30559] vsize: 62400
Current children cumulated CPU time (s) 518.75
Current children cumulated vsize (Kb) 64524

[startup+530.053 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 30559
Raw data (/proc/30555/stat): 30555 (minisat+_script) S 30554 30555 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1852099709 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30555/statm): 531 226 485 147 0 384 0
[pid=30555] vsize: 2124
Raw data (/proc/30559/stat): 30559 (minisat+_64-bit) R 30555 30555 19818 0 -1 0 15372 0 0 0 52765 108 0 0 25 0 1 0 1852099714 63897600 15230 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30559/statm): 15600 15230 145 145 0 15455 0
[pid=30559] vsize: 62400
Current children cumulated CPU time (s) 528.75
Current children cumulated vsize (Kb) 64524

[startup+540.054 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 30559
Raw data (/proc/30555/stat): 30555 (minisat+_script) S 30554 30555 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1852099709 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30555/statm): 531 226 485 147 0 384 0
[pid=30555] vsize: 2124
Raw data (/proc/30559/stat): 30559 (minisat+_64-bit) R 30555 30555 19818 0 -1 0 15372 0 0 0 53765 108 0 0 25 0 1 0 1852099714 63897600 15230 4294967295 134512640 135094434 3221224432 3221223088 134558235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30559/statm): 15600 15230 145 145 0 15455 0
[pid=30559] vsize: 62400
Current children cumulated CPU time (s) 538.75
Current children cumulated vsize (Kb) 64524

[startup+550.055 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 30559
Raw data (/proc/30555/stat): 30555 (minisat+_script) S 30554 30555 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1852099709 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30555/statm): 531 226 485 147 0 384 0
[pid=30555] vsize: 2124
Raw data (/proc/30559/stat): 30559 (minisat+_64-bit) R 30555 30555 19818 0 -1 0 15372 0 0 0 54766 108 0 0 25 0 1 0 1852099714 63897600 15230 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30559/statm): 15600 15230 145 145 0 15455 0
[pid=30559] vsize: 62400
Current children cumulated CPU time (s) 548.76
Current children cumulated vsize (Kb) 64524

[startup+560.056 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 30559
Raw data (/proc/30555/stat): 30555 (minisat+_script) S 30554 30555 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1852099709 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30555/statm): 531 226 485 147 0 384 0
[pid=30555] vsize: 2124
Raw data (/proc/30559/stat): 30559 (minisat+_64-bit) R 30555 30555 19818 0 -1 0 15372 0 0 0 55766 108 0 0 25 0 1 0 1852099714 63897600 15230 4294967295 134512640 135094434 3221224432 3221223044 134563069 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30559/statm): 15600 15230 145 145 0 15455 0
[pid=30559] vsize: 62400
Current children cumulated CPU time (s) 558.76
Current children cumulated vsize (Kb) 64524

[startup+570.056 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 30559
Raw data (/proc/30555/stat): 30555 (minisat+_script) S 30554 30555 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1852099709 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30555/statm): 531 226 485 147 0 384 0
[pid=30555] vsize: 2124
Raw data (/proc/30559/stat): 30559 (minisat+_64-bit) R 30555 30555 19818 0 -1 0 15372 0 0 0 56766 108 0 0 25 0 1 0 1852099714 63897600 15230 4294967295 134512640 135094434 3221224432 3221223088 134558398 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30559/statm): 15600 15230 145 145 0 15455 0
[pid=30559] vsize: 62400
Current children cumulated CPU time (s) 568.76
Current children cumulated vsize (Kb) 64524

[startup+580.057 s]
Raw data (loadavg): 1.14 1.00 0.92 2/57 30559
Raw data (/proc/30555/stat): 30555 (minisat+_script) S 30554 30555 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1852099709 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30555/statm): 531 226 485 147 0 384 0
[pid=30555] vsize: 2124
Raw data (/proc/30559/stat): 30559 (minisat+_64-bit) R 30555 30555 19818 0 -1 0 15372 0 0 0 57766 109 0 0 25 0 1 0 1852099714 63897600 15230 4294967295 134512640 135094434 3221224432 3221223088 134558184 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30559/statm): 15600 15230 145 145 0 15455 0
[pid=30559] vsize: 62400
Current children cumulated CPU time (s) 578.77
Current children cumulated vsize (Kb) 64524

[startup+590.058 s]
Raw data (loadavg): 1.12 1.00 0.92 2/57 30559
Raw data (/proc/30555/stat): 30555 (minisat+_script) S 30554 30555 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1852099709 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30555/statm): 531 226 485 147 0 384 0
[pid=30555] vsize: 2124
Raw data (/proc/30559/stat): 30559 (minisat+_64-bit) R 30555 30555 19818 0 -1 0 15372 0 0 0 58766 109 0 0 25 0 1 0 1852099714 63897600 15230 4294967295 134512640 135094434 3221224432 3221223088 134558435 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30559/statm): 15600 15230 145 145 0 15455 0
[pid=30559] vsize: 62400
Current children cumulated CPU time (s) 588.77
Current children cumulated vsize (Kb) 64524

[startup+600.06 s]
Raw data (loadavg): 1.10 1.00 0.92 2/57 30559
Raw data (/proc/30555/stat): 30555 (minisat+_script) S 30554 30555 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1852099709 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30555/statm): 531 226 485 147 0 384 0
[pid=30555] vsize: 2124
Raw data (/proc/30559/stat): 30559 (minisat+_64-bit) R 30555 30555 19818 0 -1 0 15372 0 0 0 59766 109 0 0 25 0 1 0 1852099714 63897600 15230 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30559/statm): 15600 15230 145 145 0 15455 0
[pid=30559] vsize: 62400
Current children cumulated CPU time (s) 598.77
Current children cumulated vsize (Kb) 64524

[startup+610.061 s]
Raw data (loadavg): 1.08 1.00 0.92 2/57 30559
Raw data (/proc/30555/stat): 30555 (minisat+_script) S 30554 30555 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1852099709 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30555/statm): 531 226 485 147 0 384 0
[pid=30555] vsize: 2124
Raw data (/proc/30559/stat): 30559 (minisat+_64-bit) R 30555 30555 19818 0 -1 0 15372 0 0 0 60767 109 0 0 25 0 1 0 1852099714 63897600 15230 4294967295 134512640 135094434 3221224432 3221223072 134562110 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30559/statm): 15600 15230 145 145 0 15455 0
[pid=30559] vsize: 62400
Current children cumulated CPU time (s) 608.78
Current children cumulated vsize (Kb) 64524

[startup+620.062 s]
Raw data (loadavg): 1.07 1.00 0.92 2/57 30559
Raw data (/proc/30555/stat): 30555 (minisat+_script) S 30554 30555 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1852099709 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30555/statm): 531 226 485 147 0 384 0
[pid=30555] vsize: 2124
Raw data (/proc/30559/stat): 30559 (minisat+_64-bit) R 30555 30555 19818 0 -1 0 15372 0 0 0 61767 109 0 0 25 0 1 0 1852099714 63897600 15230 4294967295 134512640 135094434 3221224432 3221223056 134557717 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30559/statm): 15600 15230 145 145 0 15455 0
[pid=30559] vsize: 62400
Current children cumulated CPU time (s) 618.78
Current children cumulated vsize (Kb) 64524

[startup+630.062 s]
Raw data (loadavg): 1.06 1.00 0.92 2/57 30559
Raw data (/proc/30555/stat): 30555 (minisat+_script) S 30554 30555 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1852099709 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30555/statm): 531 226 485 147 0 384 0
[pid=30555] vsize: 2124
Raw data (/proc/30559/stat): 30559 (minisat+_64-bit) R 30555 30555 19818 0 -1 0 15372 0 0 0 62767 109 0 0 25 0 1 0 1852099714 63897600 15230 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30559/statm): 15600 15230 145 145 0 15455 0
[pid=30559] vsize: 62400
Current children cumulated CPU time (s) 628.78
Current children cumulated vsize (Kb) 64524

[startup+640.063 s]
Raw data (loadavg): 1.05 1.00 0.92 2/57 30559
Raw data (/proc/30555/stat): 30555 (minisat+_script) S 30554 30555 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1852099709 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30555/statm): 531 226 485 147 0 384 0
[pid=30555] vsize: 2124
Raw data (/proc/30559/stat): 30559 (minisat+_64-bit) R 30555 30555 19818 0 -1 0 15372 0 0 0 63767 109 0 0 25 0 1 0 1852099714 63897600 15230 4294967295 134512640 135094434 3221224432 3221223044 134563104 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30559/statm): 15600 15230 145 145 0 15455 0
[pid=30559] vsize: 62400
Current children cumulated CPU time (s) 638.78
Current children cumulated vsize (Kb) 64524

[startup+650.064 s]
Raw data (loadavg): 1.04 1.00 0.92 3/57 30559
Raw data (/proc/30555/stat): 30555 (minisat+_script) S 30554 30555 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1852099709 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30555/statm): 531 226 485 147 0 384 0
[pid=30555] vsize: 2124
Raw data (/proc/30559/stat): 30559 (minisat+_64-bit) R 30555 30555 19818 0 -1 0 15372 0 0 0 64767 109 0 0 25 0 1 0 1852099714 63897600 15230 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30559/statm): 15600 15230 145 145 0 15455 0
[pid=30559] vsize: 62400
Current children cumulated CPU time (s) 648.78
Current children cumulated vsize (Kb) 64524

[startup+660.065 s]
Raw data (loadavg): 1.04 1.00 0.92 2/57 30559
Raw data (/proc/30555/stat): 30555 (minisat+_script) S 30554 30555 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1852099709 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30555/statm): 531 226 485 147 0 384 0
[pid=30555] vsize: 2124
Raw data (/proc/30559/stat): 30559 (minisat+_64-bit) R 30555 30555 19818 0 -1 0 15372 0 0 0 65767 109 0 0 25 0 1 0 1852099714 63897600 15230 4294967295 134512640 135094434 3221224432 3221223024 134556862 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30559/statm): 15600 15230 145 145 0 15455 0
[pid=30559] vsize: 62400
Current children cumulated CPU time (s) 658.78
Current children cumulated vsize (Kb) 64524

[startup+670.066 s]
Raw data (loadavg): 1.03 1.00 0.92 2/57 30559
Raw data (/proc/30555/stat): 30555 (minisat+_script) S 30554 30555 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1852099709 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30555/statm): 531 226 485 147 0 384 0
[pid=30555] vsize: 2124
Raw data (/proc/30559/stat): 30559 (minisat+_64-bit) R 30555 30555 19818 0 -1 0 15372 0 0 0 66767 109 0 0 25 0 1 0 1852099714 63897600 15230 4294967295 134512640 135094434 3221224432 3221223088 134558029 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30559/statm): 15600 15230 145 145 0 15455 0
[pid=30559] vsize: 62400
Current children cumulated CPU time (s) 668.78
Current children cumulated vsize (Kb) 64524

[startup+680.067 s]
Raw data (loadavg): 1.02 1.00 0.92 2/57 30559
Raw data (/proc/30555/stat): 30555 (minisat+_script) S 30554 30555 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1852099709 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30555/statm): 531 226 485 147 0 384 0
[pid=30555] vsize: 2124
Raw data (/proc/30559/stat): 30559 (minisat+_64-bit) R 30555 30555 19818 0 -1 0 15372 0 0 0 67768 110 0 0 25 0 1 0 1852099714 63897600 15230 4294967295 134512640 135094434 3221224432 3221223088 134558210 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30559/statm): 15600 15230 145 145 0 15455 0
[pid=30559] vsize: 62400
Current children cumulated CPU time (s) 678.8
Current children cumulated vsize (Kb) 64524

[startup+690.067 s]
Raw data (loadavg): 1.02 1.00 0.92 2/57 30559
Raw data (/proc/30555/stat): 30555 (minisat+_script) S 30554 30555 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1852099709 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30555/statm): 531 226 485 147 0 384 0
[pid=30555] vsize: 2124
Raw data (/proc/30559/stat): 30559 (minisat+_64-bit) R 30555 30555 19818 0 -1 0 15372 0 0 0 68768 110 0 0 25 0 1 0 1852099714 63897600 15230 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30559/statm): 15600 15230 145 145 0 15455 0
[pid=30559] vsize: 62400
Current children cumulated CPU time (s) 688.8
Current children cumulated vsize (Kb) 64524

[startup+700.068 s]
Raw data (loadavg): 1.02 1.00 0.92 2/57 30559
Raw data (/proc/30555/stat): 30555 (minisat+_script) S 30554 30555 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1852099709 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30555/statm): 531 226 485 147 0 384 0
[pid=30555] vsize: 2124
Raw data (/proc/30559/stat): 30559 (minisat+_64-bit) R 30555 30555 19818 0 -1 0 16053 0 0 0 69756 115 0 0 25 0 1 0 1852099714 66686976 15911 4294967295 134512640 135094434 3221224432 3221223024 134557413 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30559/statm): 16281 15911 145 145 0 16136 0
[pid=30559] vsize: 65124
Current children cumulated CPU time (s) 698.73
Current children cumulated vsize (Kb) 67248

[startup+710.069 s]
Raw data (loadavg): 1.01 1.00 0.92 2/57 30559
Raw data (/proc/30555/stat): 30555 (minisat+_script) S 30554 30555 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1852099709 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30555/statm): 531 226 485 147 0 384 0
[pid=30555] vsize: 2124
Raw data (/proc/30559/stat): 30559 (minisat+_64-bit) R 30555 30555 19818 0 -1 0 16846 0 0 0 70744 120 0 0 25 0 1 0 1852099714 69935104 16704 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30559/statm): 17074 16704 145 145 0 16929 0
[pid=30559] vsize: 68296
Current children cumulated CPU time (s) 708.66
Current children cumulated vsize (Kb) 70420

[startup+720.07 s]
Raw data (loadavg): 1.01 1.00 0.92 2/57 30559
Raw data (/proc/30555/stat): 30555 (minisat+_script) S 30554 30555 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1852099709 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30555/statm): 531 226 485 147 0 384 0
[pid=30555] vsize: 2124
Raw data (/proc/30559/stat): 30559 (minisat+_64-bit) R 30555 30555 19818 0 -1 0 17683 0 0 0 71731 125 0 0 25 0 1 0 1852099714 73363456 17541 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30559/statm): 17911 17541 145 145 0 17766 0
[pid=30559] vsize: 71644
Current children cumulated CPU time (s) 718.58
Current children cumulated vsize (Kb) 73768

[startup+730.071 s]
Raw data (loadavg): 1.01 1.00 0.92 2/57 30559
Raw data (/proc/30555/stat): 30555 (minisat+_script) S 30554 30555 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1852099709 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30555/statm): 531 226 485 147 0 384 0
[pid=30555] vsize: 2124
Raw data (/proc/30559/stat): 30559 (minisat+_64-bit) R 30555 30555 19818 0 -1 0 18443 0 0 0 72718 131 0 0 25 0 1 0 1852099714 76476416 18301 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30559/statm): 18671 18301 145 145 0 18526 0
[pid=30559] vsize: 74684
Current children cumulated CPU time (s) 728.51
Current children cumulated vsize (Kb) 76808

[startup+740.071 s]
Raw data (loadavg): 1.01 1.00 0.92 2/57 30559
Raw data (/proc/30555/stat): 30555 (minisat+_script) S 30554 30555 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1852099709 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30555/statm): 531 226 485 147 0 384 0
[pid=30555] vsize: 2124
Raw data (/proc/30559/stat): 30559 (minisat+_64-bit) R 30555 30555 19818 0 -1 0 19123 0 0 0 73706 136 0 0 25 0 1 0 1852099714 79261696 18981 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30559/statm): 19351 18981 145 145 0 19206 0
[pid=30559] vsize: 77404
Current children cumulated CPU time (s) 738.44
Current children cumulated vsize (Kb) 79528

[startup+750.073 s]
Raw data (loadavg): 1.01 1.00 0.92 2/57 30559
Raw data (/proc/30555/stat): 30555 (minisat+_script) S 30554 30555 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1852099709 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30555/statm): 531 226 485 147 0 384 0
[pid=30555] vsize: 2124
Raw data (/proc/30559/stat): 30559 (minisat+_64-bit) R 30555 30555 19818 0 -1 0 19764 0 0 0 74695 141 0 0 25 0 1 0 1852099714 81891328 19622 4294967295 134512640 135094434 3221224432 3221223088 134557996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30559/statm): 19993 19622 145 145 0 19848 0
[pid=30559] vsize: 79972
Current children cumulated CPU time (s) 748.38
Current children cumulated vsize (Kb) 82096

[startup+760.074 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 30559
Raw data (/proc/30555/stat): 30555 (minisat+_script) S 30554 30555 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1852099709 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30555/statm): 531 226 485 147 0 384 0
[pid=30555] vsize: 2124
Raw data (/proc/30559/stat): 30559 (minisat+_64-bit) R 30555 30555 19818 0 -1 0 20424 0 0 0 75684 147 0 0 25 0 1 0 1852099714 84598784 20282 4294967295 134512640 135094434 3221224432 3221223024 134557360 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30559/statm): 20654 20282 145 145 0 20509 0
[pid=30559] vsize: 82616
Current children cumulated CPU time (s) 758.33
Current children cumulated vsize (Kb) 84740

[startup+770.075 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 30559
Raw data (/proc/30555/stat): 30555 (minisat+_script) S 30554 30555 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1852099709 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30555/statm): 531 226 485 147 0 384 0
[pid=30555] vsize: 2124
Raw data (/proc/30559/stat): 30559 (minisat+_64-bit) R 30555 30555 19818 0 -1 0 21072 0 0 0 76672 152 0 0 25 0 1 0 1852099714 87261184 20930 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30559/statm): 21304 20930 145 145 0 21159 0
[pid=30559] vsize: 85216
Current children cumulated CPU time (s) 768.26
Current children cumulated vsize (Kb) 87340

[startup+780.077 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 30559
Raw data (/proc/30555/stat): 30555 (minisat+_script) S 30554 30555 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1852099709 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30555/statm): 531 226 485 147 0 384 0
[pid=30555] vsize: 2124
Raw data (/proc/30559/stat): 30559 (minisat+_64-bit) R 30555 30555 19818 0 -1 0 21712 0 0 0 77660 156 0 0 25 0 1 0 1852099714 89874432 21570 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30559/statm): 21942 21570 145 145 0 21797 0
[pid=30559] vsize: 87768
Current children cumulated CPU time (s) 778.18
Current children cumulated vsize (Kb) 89892

[startup+790.078 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 30559
Raw data (/proc/30555/stat): 30555 (minisat+_script) S 30554 30555 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1852099709 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30555/statm): 531 226 485 147 0 384 0
[pid=30555] vsize: 2124
Raw data (/proc/30559/stat): 30559 (minisat+_64-bit) R 30555 30555 19818 0 -1 0 22196 0 0 0 78651 161 0 0 25 0 1 0 1852099714 91856896 22054 4294967295 134512640 135094434 3221224432 3221223088 134558225 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30559/statm): 22426 22054 145 145 0 22281 0
[pid=30559] vsize: 89704
Current children cumulated CPU time (s) 788.14
Current children cumulated vsize (Kb) 91828

[startup+800.079 s]
Raw data (loadavg): 1.00 1.00 0.92 3/57 30559
Raw data (/proc/30555/stat): 30555 (minisat+_script) S 30554 30555 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1852099709 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30555/statm): 531 226 485 147 0 384 0
[pid=30555] vsize: 2124
Raw data (/proc/30559/stat): 30559 (minisat+_64-bit) R 30555 30555 19818 0 -1 0 22196 0 0 0 79651 161 0 0 25 0 1 0 1852099714 91856896 22054 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30559/statm): 22426 22054 145 145 0 22281 0
[pid=30559] vsize: 89704
Current children cumulated CPU time (s) 798.14
Current children cumulated vsize (Kb) 91828

[startup+810.081 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 30559
Raw data (/proc/30555/stat): 30555 (minisat+_script) S 30554 30555 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1852099709 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30555/statm): 531 226 485 147 0 384 0
[pid=30555] vsize: 2124
Raw data (/proc/30559/stat): 30559 (minisat+_64-bit) R 30555 30555 19818 0 -1 0 22196 0 0 0 80651 161 0 0 25 0 1 0 1852099714 91856896 22054 4294967295 134512640 135094434 3221224432 3221223024 134557219 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30559/statm): 22426 22054 145 145 0 22281 0
[pid=30559] vsize: 89704
Current children cumulated CPU time (s) 808.14
Current children cumulated vsize (Kb) 91828

[startup+820.082 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 30559
Raw data (/proc/30555/stat): 30555 (minisat+_script) S 30554 30555 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1852099709 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30555/statm): 531 226 485 147 0 384 0
[pid=30555] vsize: 2124
Raw data (/proc/30559/stat): 30559 (minisat+_64-bit) R 30555 30555 19818 0 -1 0 22197 0 0 0 81651 161 0 0 25 0 1 0 1852099714 91856896 22055 4294967295 134512640 135094434 3221224432 3221223088 134561502 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30559/statm): 22426 22055 145 145 0 22281 0
[pid=30559] vsize: 89704
Current children cumulated CPU time (s) 818.14
Current children cumulated vsize (Kb) 91828

[startup+830.083 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 30559
Raw data (/proc/30555/stat): 30555 (minisat+_script) S 30554 30555 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1852099709 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30555/statm): 531 226 485 147 0 384 0
[pid=30555] vsize: 2124
Raw data (/proc/30559/stat): 30559 (minisat+_64-bit) R 30555 30555 19818 0 -1 0 22197 0 0 0 82650 161 0 0 25 0 1 0 1852099714 91856896 22055 4294967295 134512640 135094434 3221224432 3221223044 134563163 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30559/statm): 22426 22055 145 145 0 22281 0
[pid=30559] vsize: 89704
Current children cumulated CPU time (s) 828.13
Current children cumulated vsize (Kb) 91828

[startup+840.084 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 30559
Raw data (/proc/30555/stat): 30555 (minisat+_script) S 30554 30555 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1852099709 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30555/statm): 531 226 485 147 0 384 0
[pid=30555] vsize: 2124
Raw data (/proc/30559/stat): 30559 (minisat+_64-bit) R 30555 30555 19818 0 -1 0 22197 0 0 0 83649 162 0 0 25 0 1 0 1852099714 91856896 22055 4294967295 134512640 135094434 3221224432 3221223088 134561757 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30559/statm): 22426 22055 145 145 0 22281 0
[pid=30559] vsize: 89704
Current children cumulated CPU time (s) 838.13
Current children cumulated vsize (Kb) 91828

[startup+850.085 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 30559
Raw data (/proc/30555/stat): 30555 (minisat+_script) S 30554 30555 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1852099709 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30555/statm): 531 226 485 147 0 384 0
[pid=30555] vsize: 2124
Raw data (/proc/30559/stat): 30559 (minisat+_64-bit) R 30555 30555 19818 0 -1 0 22197 0 0 0 84649 162 0 0 25 0 1 0 1852099714 91856896 22055 4294967295 134512640 135094434 3221224432 3221223060 134562984 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30559/statm): 22426 22055 145 145 0 22281 0
[pid=30559] vsize: 89704
Current children cumulated CPU time (s) 848.13
Current children cumulated vsize (Kb) 91828

[startup+860.086 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 30559
Raw data (/proc/30555/stat): 30555 (minisat+_script) S 30554 30555 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1852099709 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30555/statm): 531 226 485 147 0 384 0
[pid=30555] vsize: 2124
Raw data (/proc/30559/stat): 30559 (minisat+_64-bit) R 30555 30555 19818 0 -1 0 22197 0 0 0 85649 162 0 0 25 0 1 0 1852099714 91856896 22055 4294967295 134512640 135094434 3221224432 3221223088 134557860 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30559/statm): 22426 22055 145 145 0 22281 0
[pid=30559] vsize: 89704
Current children cumulated CPU time (s) 858.13
Current children cumulated vsize (Kb) 91828

[startup+870.087 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 30559
Raw data (/proc/30555/stat): 30555 (minisat+_script) S 30554 30555 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1852099709 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30555/statm): 531 226 485 147 0 384 0
[pid=30555] vsize: 2124
Raw data (/proc/30559/stat): 30559 (minisat+_64-bit) R 30555 30555 19818 0 -1 0 22197 0 0 0 86649 162 0 0 25 0 1 0 1852099714 91856896 22055 4294967295 134512640 135094434 3221224432 3221223044 134563055 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30559/statm): 22426 22055 145 145 0 22281 0
[pid=30559] vsize: 89704
Current children cumulated CPU time (s) 868.13
Current children cumulated vsize (Kb) 91828

[startup+880.088 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 30559
Raw data (/proc/30555/stat): 30555 (minisat+_script) S 30554 30555 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1852099709 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30555/statm): 531 226 485 147 0 384 0
[pid=30555] vsize: 2124
Raw data (/proc/30559/stat): 30559 (minisat+_64-bit) R 30555 30555 19818 0 -1 0 22197 0 0 0 87650 162 0 0 25 0 1 0 1852099714 91856896 22055 4294967295 134512640 135094434 3221224432 3221223088 134557950 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30559/statm): 22426 22055 145 145 0 22281 0
[pid=30559] vsize: 89704
Current children cumulated CPU time (s) 878.14
Current children cumulated vsize (Kb) 91828

[startup+890.089 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 30559
Raw data (/proc/30555/stat): 30555 (minisat+_script) S 30554 30555 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1852099709 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30555/statm): 531 226 485 147 0 384 0
[pid=30555] vsize: 2124
Raw data (/proc/30559/stat): 30559 (minisat+_64-bit) R 30555 30555 19818 0 -1 0 22197 0 0 0 88650 162 0 0 25 0 1 0 1852099714 91856896 22055 4294967295 134512640 135094434 3221224432 3221223104 134556242 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30559/statm): 22426 22055 145 145 0 22281 0
[pid=30559] vsize: 89704
Current children cumulated CPU time (s) 888.14
Current children cumulated vsize (Kb) 91828

[startup+900.089 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 30559
Raw data (/proc/30555/stat): 30555 (minisat+_script) S 30554 30555 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1852099709 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30555/statm): 531 226 485 147 0 384 0
[pid=30555] vsize: 2124
Raw data (/proc/30559/stat): 30559 (minisat+_64-bit) R 30555 30555 19818 0 -1 0 22197 0 0 0 89648 164 0 0 25 0 1 0 1852099714 91856896 22055 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30559/statm): 22426 22055 145 145 0 22281 0
[pid=30559] vsize: 89704
Current children cumulated CPU time (s) 898.14
Current children cumulated vsize (Kb) 91828

[startup+910.09 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 30559
Raw data (/proc/30555/stat): 30555 (minisat+_script) S 30554 30555 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1852099709 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30555/statm): 531 226 485 147 0 384 0
[pid=30555] vsize: 2124
Raw data (/proc/30559/stat): 30559 (minisat+_64-bit) R 30555 30555 19818 0 -1 0 22197 0 0 0 90648 164 0 0 25 0 1 0 1852099714 91856896 22055 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30559/statm): 22426 22055 145 145 0 22281 0
[pid=30559] vsize: 89704
Current children cumulated CPU time (s) 908.14
Current children cumulated vsize (Kb) 91828

[startup+920.09 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 30559
Raw data (/proc/30555/stat): 30555 (minisat+_script) S 30554 30555 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1852099709 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30555/statm): 531 226 485 147 0 384 0
[pid=30555] vsize: 2124
Raw data (/proc/30559/stat): 30559 (minisat+_64-bit) R 30555 30555 19818 0 -1 0 22197 0 0 0 91648 165 0 0 25 0 1 0 1852099714 91856896 22055 4294967295 134512640 135094434 3221224432 3221223088 134557863 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30559/statm): 22426 22055 145 145 0 22281 0
[pid=30559] vsize: 89704
Current children cumulated CPU time (s) 918.15
Current children cumulated vsize (Kb) 91828

[startup+930.091 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 30559
Raw data (/proc/30555/stat): 30555 (minisat+_script) S 30554 30555 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1852099709 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30555/statm): 531 226 485 147 0 384 0
[pid=30555] vsize: 2124
Raw data (/proc/30559/stat): 30559 (minisat+_64-bit) R 30555 30555 19818 0 -1 0 22197 0 0 0 92648 165 0 0 25 0 1 0 1852099714 91856896 22055 4294967295 134512640 135094434 3221224432 3221223044 134563066 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30559/statm): 22426 22055 145 145 0 22281 0
[pid=30559] vsize: 89704
Current children cumulated CPU time (s) 928.15
Current children cumulated vsize (Kb) 91828

[startup+940.091 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 30559
Raw data (/proc/30555/stat): 30555 (minisat+_script) S 30554 30555 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1852099709 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30555/statm): 531 226 485 147 0 384 0
[pid=30555] vsize: 2124
Raw data (/proc/30559/stat): 30559 (minisat+_64-bit) R 30555 30555 19818 0 -1 0 22197 0 0 0 93648 165 0 0 25 0 1 0 1852099714 91856896 22055 4294967295 134512640 135094434 3221224432 3221223088 134558007 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30559/statm): 22426 22055 145 145 0 22281 0
[pid=30559] vsize: 89704
Current children cumulated CPU time (s) 938.15
Current children cumulated vsize (Kb) 91828

[startup+950.091 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 30559
Raw data (/proc/30555/stat): 30555 (minisat+_script) S 30554 30555 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1852099709 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30555/statm): 531 226 485 147 0 384 0
[pid=30555] vsize: 2124
Raw data (/proc/30559/stat): 30559 (minisat+_64-bit) R 30555 30555 19818 0 -1 0 22197 0 0 0 94648 166 0 0 25 0 1 0 1852099714 91856896 22055 4294967295 134512640 135094434 3221224432 3221223044 134563046 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30559/statm): 22426 22055 145 145 0 22281 0
[pid=30559] vsize: 89704
Current children cumulated CPU time (s) 948.16
Current children cumulated vsize (Kb) 91828

[startup+960.092 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 30559
Raw data (/proc/30555/stat): 30555 (minisat+_script) S 30554 30555 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1852099709 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30555/statm): 531 226 485 147 0 384 0
[pid=30555] vsize: 2124
Raw data (/proc/30559/stat): 30559 (minisat+_64-bit) R 30555 30555 19818 0 -1 0 22197 0 0 0 95647 166 0 0 25 0 1 0 1852099714 91856896 22055 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30559/statm): 22426 22055 145 145 0 22281 0
[pid=30559] vsize: 89704
Current children cumulated CPU time (s) 958.15
Current children cumulated vsize (Kb) 91828

[startup+970.093 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 30559
Raw data (/proc/30555/stat): 30555 (minisat+_script) S 30554 30555 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1852099709 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30555/statm): 531 226 485 147 0 384 0
[pid=30555] vsize: 2124
Raw data (/proc/30559/stat): 30559 (minisat+_64-bit) R 30555 30555 19818 0 -1 0 22197 0 0 0 96648 166 0 0 25 0 1 0 1852099714 91856896 22055 4294967295 134512640 135094434 3221224432 3221223088 134558178 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30559/statm): 22426 22055 145 145 0 22281 0
[pid=30559] vsize: 89704
Current children cumulated CPU time (s) 968.16
Current children cumulated vsize (Kb) 91828

[startup+980.094 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 30559
Raw data (/proc/30555/stat): 30555 (minisat+_script) S 30554 30555 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1852099709 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30555/statm): 531 226 485 147 0 384 0
[pid=30555] vsize: 2124
Raw data (/proc/30559/stat): 30559 (minisat+_64-bit) R 30555 30555 19818 0 -1 0 22197 0 0 0 97647 167 0 0 25 0 1 0 1852099714 91856896 22055 4294967295 134512640 135094434 3221224432 3221223088 134558235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30559/statm): 22426 22055 145 145 0 22281 0
[pid=30559] vsize: 89704
Current children cumulated CPU time (s) 978.16
Current children cumulated vsize (Kb) 91828

[startup+990.095 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 30559
Raw data (/proc/30555/stat): 30555 (minisat+_script) S 30554 30555 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1852099709 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30555/statm): 531 226 485 147 0 384 0
[pid=30555] vsize: 2124
Raw data (/proc/30559/stat): 30559 (minisat+_64-bit) R 30555 30555 19818 0 -1 0 22197 0 0 0 98648 167 0 0 25 0 1 0 1852099714 91856896 22055 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30559/statm): 22426 22055 145 145 0 22281 0
[pid=30559] vsize: 89704
Current children cumulated CPU time (s) 988.17
Current children cumulated vsize (Kb) 91828

[startup+1000.1 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 30559
Raw data (/proc/30555/stat): 30555 (minisat+_script) S 30554 30555 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1852099709 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30555/statm): 531 226 485 147 0 384 0
[pid=30555] vsize: 2124
Raw data (/proc/30559/stat): 30559 (minisat+_64-bit) R 30555 30555 19818 0 -1 0 22197 0 0 0 99648 167 0 0 25 0 1 0 1852099714 91856896 22055 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30559/statm): 22426 22055 145 145 0 22281 0
[pid=30559] vsize: 89704
Current children cumulated CPU time (s) 998.17
Current children cumulated vsize (Kb) 91828

[startup+1010.1 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 30559
Raw data (/proc/30555/stat): 30555 (minisat+_script) S 30554 30555 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1852099709 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30555/statm): 531 226 485 147 0 384 0
[pid=30555] vsize: 2124
Raw data (/proc/30559/stat): 30559 (minisat+_64-bit) R 30555 30555 19818 0 -1 0 22197 0 0 0 100648 167 0 0 25 0 1 0 1852099714 91856896 22055 4294967295 134512640 135094434 3221224432 3221223088 134561757 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30559/statm): 22426 22055 145 145 0 22281 0
[pid=30559] vsize: 89704
Current children cumulated CPU time (s) 1008.17
Current children cumulated vsize (Kb) 91828

[startup+1020.1 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 30559
Raw data (/proc/30555/stat): 30555 (minisat+_script) S 30554 30555 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1852099709 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30555/statm): 531 226 485 147 0 384 0
[pid=30555] vsize: 2124
Raw data (/proc/30559/stat): 30559 (minisat+_64-bit) R 30555 30555 19818 0 -1 0 22202 0 0 0 101648 167 0 0 25 0 1 0 1852099714 91856896 22060 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30559/statm): 22426 22060 145 145 0 22281 0
[pid=30559] vsize: 89704
Current children cumulated CPU time (s) 1018.17
Current children cumulated vsize (Kb) 91828

[startup+1030.1 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 30559
Raw data (/proc/30555/stat): 30555 (minisat+_script) S 30554 30555 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1852099709 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30555/statm): 531 226 485 147 0 384 0
[pid=30555] vsize: 2124
Raw data (/proc/30559/stat): 30559 (minisat+_64-bit) R 30555 30555 19818 0 -1 0 22207 0 0 0 102648 167 0 0 25 0 1 0 1852099714 91856896 22065 4294967295 134512640 135094434 3221224432 3221223024 134551454 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30559/statm): 22426 22065 145 145 0 22281 0
[pid=30559] vsize: 89704
Current children cumulated CPU time (s) 1028.17
Current children cumulated vsize (Kb) 91828

[startup+1040.1 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 30559
Raw data (/proc/30555/stat): 30555 (minisat+_script) S 30554 30555 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1852099709 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30555/statm): 531 226 485 147 0 384 0
[pid=30555] vsize: 2124
Raw data (/proc/30559/stat): 30559 (minisat+_64-bit) R 30555 30555 19818 0 -1 0 22207 0 0 0 103648 168 0 0 25 0 1 0 1852099714 91856896 22065 4294967295 134512640 135094434 3221224432 3221223088 134558235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30559/statm): 22426 22065 145 145 0 22281 0
[pid=30559] vsize: 89704
Current children cumulated CPU time (s) 1038.18
Current children cumulated vsize (Kb) 91828

[startup+1050.1 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 30559
Raw data (/proc/30555/stat): 30555 (minisat+_script) S 30554 30555 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1852099709 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30555/statm): 531 226 485 147 0 384 0
[pid=30555] vsize: 2124
Raw data (/proc/30559/stat): 30559 (minisat+_64-bit) R 30555 30555 19818 0 -1 0 22207 0 0 0 104648 168 0 0 25 0 1 0 1852099714 91856896 22065 4294967295 134512640 135094434 3221224432 3221223044 134563083 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30559/statm): 22426 22065 145 145 0 22281 0
[pid=30559] vsize: 89704
Current children cumulated CPU time (s) 1048.18
Current children cumulated vsize (Kb) 91828

[startup+1060.1 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 30559
Raw data (/proc/30555/stat): 30555 (minisat+_script) S 30554 30555 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1852099709 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30555/statm): 531 226 485 147 0 384 0
[pid=30555] vsize: 2124
Raw data (/proc/30559/stat): 30559 (minisat+_64-bit) R 30555 30555 19818 0 -1 0 22207 0 0 0 105648 168 0 0 25 0 1 0 1852099714 91856896 22065 4294967295 134512640 135094434 3221224432 3221223044 134563124 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30559/statm): 22426 22065 145 145 0 22281 0
[pid=30559] vsize: 89704
Current children cumulated CPU time (s) 1058.18
Current children cumulated vsize (Kb) 91828

[startup+1070.1 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 30559
Raw data (/proc/30555/stat): 30555 (minisat+_script) S 30554 30555 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1852099709 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30555/statm): 531 226 485 147 0 384 0
[pid=30555] vsize: 2124
Raw data (/proc/30559/stat): 30559 (minisat+_64-bit) R 30555 30555 19818 0 -1 0 22207 0 0 0 106648 168 0 0 25 0 1 0 1852099714 91856896 22065 4294967295 134512640 135094434 3221224432 3221223024 134552003 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30559/statm): 22426 22065 145 145 0 22281 0
[pid=30559] vsize: 89704
Current children cumulated CPU time (s) 1068.18
Current children cumulated vsize (Kb) 91828

[startup+1080.1 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 30559
Raw data (/proc/30555/stat): 30555 (minisat+_script) S 30554 30555 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1852099709 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30555/statm): 531 226 485 147 0 384 0
[pid=30555] vsize: 2124
Raw data (/proc/30559/stat): 30559 (minisat+_64-bit) R 30555 30555 19818 0 -1 0 22207 0 0 0 107648 168 0 0 25 0 1 0 1852099714 91856896 22065 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30559/statm): 22426 22065 145 145 0 22281 0
[pid=30559] vsize: 89704
Current children cumulated CPU time (s) 1078.18
Current children cumulated vsize (Kb) 91828

[startup+1090.1 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 30559
Raw data (/proc/30555/stat): 30555 (minisat+_script) S 30554 30555 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1852099709 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30555/statm): 531 226 485 147 0 384 0
[pid=30555] vsize: 2124
Raw data (/proc/30559/stat): 30559 (minisat+_64-bit) R 30555 30555 19818 0 -1 0 22207 0 0 0 108648 168 0 0 25 0 1 0 1852099714 91856896 22065 4294967295 134512640 135094434 3221224432 3221223092 134553491 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30559/statm): 22426 22065 145 145 0 22281 0
[pid=30559] vsize: 89704
Current children cumulated CPU time (s) 1088.18
Current children cumulated vsize (Kb) 91828

[startup+1100.1 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 30559
Raw data (/proc/30555/stat): 30555 (minisat+_script) S 30554 30555 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1852099709 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30555/statm): 531 226 485 147 0 384 0
[pid=30555] vsize: 2124
Raw data (/proc/30559/stat): 30559 (minisat+_64-bit) R 30555 30555 19818 0 -1 0 22207 0 0 0 109649 168 0 0 25 0 1 0 1852099714 91856896 22065 4294967295 134512640 135094434 3221224432 3221223088 134561757 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30559/statm): 22426 22065 145 145 0 22281 0
[pid=30559] vsize: 89704
Current children cumulated CPU time (s) 1098.19
Current children cumulated vsize (Kb) 91828

[startup+1110.1 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 30559
Raw data (/proc/30555/stat): 30555 (minisat+_script) S 30554 30555 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1852099709 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30555/statm): 531 226 485 147 0 384 0
[pid=30555] vsize: 2124
Raw data (/proc/30559/stat): 30559 (minisat+_64-bit) R 30555 30555 19818 0 -1 0 22207 0 0 0 110649 168 0 0 25 0 1 0 1852099714 91856896 22065 4294967295 134512640 135094434 3221224432 3221223044 134563043 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30559/statm): 22426 22065 145 145 0 22281 0
[pid=30559] vsize: 89704
Current children cumulated CPU time (s) 1108.19
Current children cumulated vsize (Kb) 91828

[startup+1120.1 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 30559
Raw data (/proc/30555/stat): 30555 (minisat+_script) S 30554 30555 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1852099709 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30555/statm): 531 226 485 147 0 384 0
[pid=30555] vsize: 2124
Raw data (/proc/30559/stat): 30559 (minisat+_64-bit) R 30555 30555 19818 0 -1 0 22207 0 0 0 111649 168 0 0 25 0 1 0 1852099714 91856896 22065 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30559/statm): 22426 22065 145 145 0 22281 0
[pid=30559] vsize: 89704
Current children cumulated CPU time (s) 1118.19
Current children cumulated vsize (Kb) 91828

[startup+1130.1 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 30559
Raw data (/proc/30555/stat): 30555 (minisat+_script) S 30554 30555 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1852099709 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30555/statm): 531 226 485 147 0 384 0
[pid=30555] vsize: 2124
Raw data (/proc/30559/stat): 30559 (minisat+_64-bit) R 30555 30555 19818 0 -1 0 22207 0 0 0 112649 169 0 0 25 0 1 0 1852099714 91856896 22065 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30559/statm): 22426 22065 145 145 0 22281 0
[pid=30559] vsize: 89704
Current children cumulated CPU time (s) 1128.2
Current children cumulated vsize (Kb) 91828

[startup+1140.11 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 30559
Raw data (/proc/30555/stat): 30555 (minisat+_script) S 30554 30555 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1852099709 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30555/statm): 531 226 485 147 0 384 0
[pid=30555] vsize: 2124
Raw data (/proc/30559/stat): 30559 (minisat+_64-bit) R 30555 30555 19818 0 -1 0 22207 0 0 0 113649 169 0 0 25 0 1 0 1852099714 91856896 22065 4294967295 134512640 135094434 3221224432 3221223072 134562057 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30559/statm): 22426 22065 145 145 0 22281 0
[pid=30559] vsize: 89704
Current children cumulated CPU time (s) 1138.2
Current children cumulated vsize (Kb) 91828

[startup+1150.11 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 30559
Raw data (/proc/30555/stat): 30555 (minisat+_script) S 30554 30555 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1852099709 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30555/statm): 531 226 485 147 0 384 0
[pid=30555] vsize: 2124
Raw data (/proc/30559/stat): 30559 (minisat+_64-bit) R 30555 30555 19818 0 -1 0 22207 0 0 0 114649 169 0 0 25 0 1 0 1852099714 91856896 22065 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30559/statm): 22426 22065 145 145 0 22281 0
[pid=30559] vsize: 89704
Current children cumulated CPU time (s) 1148.2
Current children cumulated vsize (Kb) 91828

[startup+1160.11 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 30559
Raw data (/proc/30555/stat): 30555 (minisat+_script) S 30554 30555 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1852099709 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30555/statm): 531 226 485 147 0 384 0
[pid=30555] vsize: 2124
Raw data (/proc/30559/stat): 30559 (minisat+_64-bit) R 30555 30555 19818 0 -1 0 22207 0 0 0 115649 169 0 0 25 0 1 0 1852099714 91856896 22065 4294967295 134512640 135094434 3221224432 3221223088 134557945 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30559/statm): 22426 22065 145 145 0 22281 0
[pid=30559] vsize: 89704
Current children cumulated CPU time (s) 1158.2
Current children cumulated vsize (Kb) 91828

[startup+1170.11 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 30559
Raw data (/proc/30555/stat): 30555 (minisat+_script) S 30554 30555 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1852099709 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30555/statm): 531 226 485 147 0 384 0
[pid=30555] vsize: 2124
Raw data (/proc/30559/stat): 30559 (minisat+_64-bit) R 30555 30555 19818 0 -1 0 22207 0 0 0 116650 169 0 0 25 0 1 0 1852099714 91856896 22065 4294967295 134512640 135094434 3221224432 3221223088 134558178 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30559/statm): 22426 22065 145 145 0 22281 0
[pid=30559] vsize: 89704
Current children cumulated CPU time (s) 1168.21
Current children cumulated vsize (Kb) 91828

[startup+1180.11 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 30559
Raw data (/proc/30555/stat): 30555 (minisat+_script) S 30554 30555 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1852099709 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30555/statm): 531 226 485 147 0 384 0
[pid=30555] vsize: 2124
Raw data (/proc/30559/stat): 30559 (minisat+_64-bit) R 30555 30555 19818 0 -1 0 22207 0 0 0 117649 169 0 0 25 0 1 0 1852099714 91856896 22065 4294967295 134512640 135094434 3221224432 3221223024 134556941 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30559/statm): 22426 22065 145 145 0 22281 0
[pid=30559] vsize: 89704
Current children cumulated CPU time (s) 1178.2
Current children cumulated vsize (Kb) 91828

[startup+1190.11 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 30559
Raw data (/proc/30555/stat): 30555 (minisat+_script) S 30554 30555 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1852099709 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30555/statm): 531 226 485 147 0 384 0
[pid=30555] vsize: 2124
Raw data (/proc/30559/stat): 30559 (minisat+_64-bit) R 30555 30555 19818 0 -1 0 22207 0 0 0 118649 169 0 0 25 0 1 0 1852099714 91856896 22065 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30559/statm): 22426 22065 145 145 0 22281 0
[pid=30559] vsize: 89704
Current children cumulated CPU time (s) 1188.2
Current children cumulated vsize (Kb) 91828

[startup+1200.11 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 30559
Raw data (/proc/30555/stat): 30555 (minisat+_script) S 30554 30555 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1852099709 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30555/statm): 531 226 485 147 0 384 0
[pid=30555] vsize: 2124
Raw data (/proc/30559/stat): 30559 (minisat+_64-bit) R 30555 30555 19818 0 -1 0 22207 0 0 0 119648 169 0 0 25 0 1 0 1852099714 91856896 22065 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30559/statm): 22426 22065 145 145 0 22281 0
[pid=30559] vsize: 89704
Current children cumulated CPU time (s) 1198.19
Current children cumulated vsize (Kb) 91828

[startup+1210.11 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 30559
Raw data (/proc/30555/stat): 30555 (minisat+_script) S 30554 30555 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1852099709 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30555/statm): 531 226 485 147 0 384 0
[pid=30555] vsize: 2124
Raw data (/proc/30559/stat): 30559 (minisat+_64-bit) R 30555 30555 19818 0 -1 0 22207 0 0 0 120649 169 0 0 25 0 1 0 1852099714 91856896 22065 4294967295 134512640 135094434 3221224432 3221223104 134556073 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30559/statm): 22426 22065 145 145 0 22281 0
[pid=30559] vsize: 89704
Current children cumulated CPU time (s) 1208.2
Current children cumulated vsize (Kb) 91828



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.11 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 30559
Raw data (/proc/30555/stat): 30555 (minisat+_script) S 30554 30555 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1852099709 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30555/statm): 531 226 485 147 0 384 0
[pid=30555] vsize: 2124
Raw data (/proc/30559/stat): 30559 (minisat+_64-bit) R 30555 30555 19818 0 -1 0 22207 0 0 0 120649 169 0 0 25 0 1 0 1852099714 91856896 22065 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30559/statm): 22426 22065 145 145 0 22281 0
[pid=30559] vsize: 89704
Current children cumulated CPU time (s) 1208.2
Current children cumulated vsize (Kb) 91828

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

Child status: 0
Real time (s): 1210.16
CPU time (s): 1208.24
CPU user time (s): 1206.49
CPU system time (s): 1.74273
CPU usage (%): 99.8413
Max. virtual memory (cumulated for all children) (Kb): 91828

Verifier Data

ERROR: no interpretation found !