Some explanations

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

General information on the benchmark

Namemps-v2-20-10/MIPLIB/miplib2003/normalized-mps-v2-20-10-10teams.opb
MD5SUM1ff3cc3253012886aa21be4feac6111e
Bench Categoryoptimization, small integers (OPTSMALLINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function 924
Optimality of the best value was proved NO
Number of terms in the objective function 1800
Biggest coefficient in the objective function 86
Number of bits for the biggest coefficient in the objective function 7
Sum of the numbers in the objective function 41700
Number of bits of the sum of numbers in the objective function 16
Biggest number in a constraint 86
Number of bits of the biggest number in a constraint 7
Biggest sum of numbers in a constraint 41700
Number of bits of the biggest sum of numbers16
Best result obtained on this benchmarkSAT
Best CPU time to get the best result obtained on this benchmark1189.03
Number of variables1800
Total number of constraints2015
Number of constraints which are clauses0
Number of constraints which are cardinality constraints (but not clauses)2015
Number of constraints which are nor clauses,nor cardinality constraints0
Minimum length of a constraint1
Maximum length of a constraint72

Trace number 4491

Launcher Data

LAUNCH ON wulflinc27 THE 2005-09-19 17:42:21 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=2952 boxname=wulflinc27 idbench=608 idsolver=3 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  1ff3cc3253012886aa21be4feac6111e  /oldhome/oroussel/tmp/wulflinc27/normalized-mps-v2-20-10-10teams.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc27/normalized-mps-v2-20-10-10teams.opb
IDLAUNCH: 2952
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.169
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.169
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:        875540 kB
Buffers:         33784 kB
Cached:          92760 kB
SwapCached:        752 kB
Active:          69288 kB
Inactive:        59904 kB
HighTotal:      131008 kB
HighFree:        42728 kB
LowTotal:       903652 kB
LowFree:        832812 kB
SwapTotal:     2097892 kB
SwapFree:      2096628 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5728 kB
Slab:            24288 kB
Committed_AS:    64168 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-09-19 18:02:31 (client local time) WITH STATUS 10 IN 1207.67 SECONDS
stats: 2952 7 1207.67 10

Solver Data

c Parsing PB file...
c Converting 330 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ########################################################################################################################
c   -- Clauses(.)/Splits(s): (none)
c ---[ 329]---> BDD-cost:  125
c ---[ 328]---> BDD-cost:  185
c ---[ 326]---> BDD-cost:   77
c ---[ 324]---> BDD-cost:   77
c ---[ 322]---> BDD-cost:   77
c ---[ 320]---> BDD-cost:   77
c ---[ 318]---> BDD-cost:   77
c ---[ 316]---> BDD-cost:   77
c ---[ 314]---> BDD-cost:   77
c ---[ 312]---> BDD-cost:   77
c ---[ 310]---> BDD-cost:   77
c ---[ 308]---> BDD-cost:   77
c ---[ 307]---> BDD-cost:  185
c ---[ 305]---> BDD-cost:   77
c ---[ 303]---> BDD-cost:   77
c ---[ 301]---> BDD-cost:   77
c ---[ 299]---> BDD-cost:   77
c ---[ 297]---> BDD-cost:   77
c ---[ 295]---> BDD-cost:   77
c ---[ 293]---> BDD-cost:   77
c ---[ 291]---> BDD-cost:   77
c ---[ 289]---> BDD-cost:   77
c ---[ 288]---> BDD-cost:  125
c ---[ 286]---> BDD-cost:   77
c ---[ 284]---> BDD-cost:   77
c ---[ 282]---> BDD-cost:   77
c ---[ 280]---> BDD-cost:   77
c ---[ 278]---> BDD-cost:   77
c ---[ 276]---> BDD-cost:   77
c ---[ 274]---> BDD-cost:   77
c ---[ 272]---> BDD-cost:   77
c ---[ 270]---> BDD-cost:   77
c ---[ 269]---> BDD-cost:  185
c ---[ 267]---> BDD-cost:   77
c ---[ 265]---> BDD-cost:   77
c ---[ 263]---> BDD-cost:   77
c ---[ 261]---> BDD-cost:   77
c ---[ 259]---> BDD-cost:   77
c ---[ 257]---> BDD-cost:   77
c ---[ 255]---> BDD-cost:   77
c ---[ 253]---> BDD-cost:   77
c ---[ 251]---> BDD-cost:   77
c ---[ 250]---> BDD-cost:  185
c ---[ 248]---> BDD-cost:   70
c ---[ 246]---> BDD-cost:   77
c ---[ 244]---> BDD-cost:   77
c ---[ 242]---> BDD-cost:   77
c ---[ 240]---> BDD-cost:   77
c ---[ 238]---> BDD-cost:   77
c ---[ 236]---> BDD-cost:   77
c ---[ 234]---> BDD-cost:   77
c ---[ 233]---> BDD-cost:  185
c ---[ 231]---> BDD-cost:   77
c ---[ 229]---> BDD-cost:   77
c ---[ 227]---> BDD-cost:   77
c ---[ 225]---> BDD-cost:   77
c ---[ 223]---> BDD-cost:   77
c ---[ 221]---> BDD-cost:   77
c ---[ 219]---> BDD-cost:   77
c ---[ 217]---> BDD-cost:   77
c ---[ 216]---> BDD-cost:  185
c ---[ 214]---> BDD-cost:   70
c ---[ 212]---> BDD-cost:   77
c ---[ 210]---> BDD-cost:   77
c ---[ 208]---> BDD-cost:   77
c ---[ 206]---> BDD-cost:   77
c ---[ 204]---> BDD-cost:   77
c ---[ 202]---> BDD-cost:   77
c ---[ 200]---> BDD-cost:   77
c ---[ 198]---> BDD-cost:   70
c ---[ 197]---> BDD-cost:  185
c ---[ 195]---> BDD-cost:   77
c ---[ 193]---> BDD-cost:   77
c ---[ 191]---> BDD-cost:   77
c ---[ 189]---> BDD-cost:   77
c ---[ 187]---> BDD-cost:   77
c ---[ 185]---> BDD-cost:   77
c ---[ 183]---> BDD-cost:   77
c ---[ 181]---> BDD-cost:   77
c ---[ 179]---> BDD-cost:   77
c ---[ 178]---> BDD-cost:  125
c ---[ 176]---> BDD-cost:   77
c ---[ 174]---> BDD-cost:   77
c ---[ 172]---> BDD-cost:   77
c ---[ 170]---> BDD-cost:   77
c ---[ 168]---> BDD-cost:   77
c ---[ 166]---> BDD-cost:   77
c ---[ 164]---> BDD-cost:   77
c ---[ 162]---> BDD-cost:   77
c ---[ 160]---> BDD-cost:   77
c ---[ 159]---> BDD-cost:  185
c ---[ 157]---> BDD-cost:   77
c ---[ 155]---> BDD-cost:   77
c ---[ 153]---> BDD-cost:   77
c ---[ 151]---> BDD-cost:   77
c ---[ 149]---> BDD-cost:   77
c ---[ 147]---> BDD-cost:   77
c ---[ 145]---> BDD-cost:   77
c ---[ 143]---> BDD-cost:   77
c ---[ 141]---> BDD-cost:   77
c ---[ 140]---> BDD-cost:  185
c ---[ 139]---> BDD-cost:  185
c ---[ 137]---> BDD-cost:   77
c ---[ 135]---> BDD-cost:   77
c ---[ 133]---> BDD-cost:   77
c ---[ 131]---> BDD-cost:   77
c ---[ 129]---> BDD-cost:   77
c ---[ 127]---> BDD-cost:   77
c ---[ 125]---> BDD-cost:   77
c ---[ 123]---> BDD-cost:   77
c ---[ 121]---> BDD-cost:   77
c ---[ 120]---> BDD-cost:  178
c ---[ 118]---> BDD-cost:   77
c ---[ 116]---> BDD-cost:   77
c ---[ 114]---> BDD-cost:   77
c ---[ 112]---> BDD-cost:   77
c ---[ 110]---> BDD-cost:   77
c ---[ 108]---> BDD-cost:   77
c ---[ 106]---> BDD-cost:   77
c ---[ 104]---> BDD-cost:   77
c ---[ 102]---> BDD-cost:   77
c ---[ 101]---> BDD-cost:  185
c ---[  99]---> BDD-cost:   77
c ---[  97]---> BDD-cost:   77
c ---[  95]---> BDD-cost:   77
c ---[  93]---> BDD-cost:   77
c ---[  91]---> BDD-cost:   77
c ---[  89]---> BDD-cost:   77
c ---[  87]---> BDD-cost:   77
c ---[  85]---> BDD-cost:   77
c ---[  83]---> BDD-cost:   77
c ---[  82]---> BDD-cost:  125
c ---[  80]---> BDD-cost:   77
c ---[  79]---> BDD-cost:  185
c ---[  78]---> BDD-cost:  185
c ---[  77]---> BDD-cost:  178
c ---[  76]---> BDD-cost:  185
c ---[  75]---> BDD-cost:  185
c ---[  74]---> BDD-cost:  125
c ---[  73]---> BDD-cost:  185
c ---[  72]---> BDD-cost:  185
c ---[  71]---> BDD-cost:  178
c ---[  70]---> BDD-cost:  185
c ---[  69]---> BDD-cost:  185
c ---[  68]---> BDD-cost:  125
c ---[  67]---> BDD-cost:  185
c ---[  66]---> BDD-cost:  178
c ---[  65]---> BDD-cost:  185
c ---[  64]---> BDD-cost:  185
c ---[  63]---> BDD-cost:  185
c ---[  62]---> BDD-cost:  185
c ---[  61]---> BDD-cost:  125
c ---[  60]---> BDD-cost:  118
c ---[  59]---> BDD-cost:  185
c ---[  58]---> BDD-cost:  185
c ---[  57]---> BDD-cost:  185
c ---[  56]---> BDD-cost:  185
c ---[  55]---> BDD-cost:  178
c ---[  54]---> BDD-cost:  185
c ---[  53]---> BDD-cost:  185
c ---[  52]---> BDD-cost:  185
c ---[  51]---> BDD-cost:  185
c ---[  50]---> BDD-cost:  125
c ---[  49]---> BDD-cost:   76
c ---[  48]---> BDD-cost:   76
c ---[  47]---> BDD-cost:   76
c ---[  46]---> BDD-cost:   76
c ---[  45]---> BDD-cost:   76
c ---[  44]---> BDD-cost:   76
c ---[  43]---> BDD-cost:   76
c ---[  42]---> BDD-cost:   76
c ---[  41]---> BDD-cost:  177
c ---[  40]---> BDD-cost:   77
c ---[  39]---> BDD-cost:   77
c ---[  38]---> BDD-cost:   77
c ---[  37]---> BDD-cost:   77
c ---[  36]---> BDD-cost:   77
c ---[  35]---> BDD-cost:   77
c ---[  34]---> BDD-cost:   77
c ---[  33]---> BDD-cost:   77
c ---[  32]---> BDD-cost:  123
c ---[  31]---> BDD-cost:   77
c ---[  30]---> BDD-cost:   77
c ---[  29]---> BDD-cost:   77
c ---[  28]---> BDD-cost:   77
c ---[  27]---> BDD-cost:   77
c ---[  26]---> BDD-cost:   77
c ---[  25]---> BDD-cost:   77
c ---[  24]---> BDD-cost:   77
c ---[  23]---> BDD-cost:   77
c ---[  22]---> BDD-cost:  183
c ---[  21]---> BDD-cost:   77
c ---[  20]---> BDD-cost:   77
c ---[  19]---> BDD-cost:   77
c ---[  18]---> BDD-cost:   77
c ---[  17]---> BDD-cost:   77
c ---[  16]---> BDD-cost:   77
c ---[  15]---> BDD-cost:   77
c ---[  14]---> BDD-cost:   75
c ---[  13]---> BDD-cost:   77
c ---[  12]---> BDD-cost:  183
c ---[  11]---> BDD-cost:   77
c ---[  10]---> BDD-cost:   77
c ---[   9]---> BDD-cost:   77
c ---[   8]---> BDD-cost:   77
c ---[   7]---> BDD-cost:   77
c ---[   6]---> BDD-cost:   77
c ---[   4]---> BDD-cost:   77
c ---[   2]---> BDD-cost:   77
c ---[   0]---> BDD-cost:   77
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   53221   141547 |   17740       0        0     nan |  0.000 % |
c |       100 |   53221   141547 |   19514     100     2449    24.5 |  1.808 % |
c |       251 |   53221   141547 |   21465     251    20371    81.2 |  1.808 % |
c |       476 |   53221   141547 |   23611     476    41787    87.8 |  1.808 % |
c |       813 |   53221   141547 |   25973     813    88284   108.6 |  1.808 % |
c ==============================================================================
c Found solution: 1004
c ---[   0]---> Adder-cost: 7750   maxlim: 38996   bits: 16/16
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1052 |  107348   334850 |   35782    1052   103950    98.8 |  1.808 % |
c |      1153 |  107348   334850 |   39360    1153   107715    93.4 |  1.396 % |
c |      1304 |  107348   334850 |   43296    1304   116225    89.1 |  1.396 % |
c |      1529 |  107348   334850 |   47625    1529   123219    80.6 |  1.396 % |
c |      1866 |  107348   334850 |   52388    1866   156815    84.0 |  1.396 % |
c ==============================================================================
c Found solution: 1002
c ---[   0]---> Adder-cost: 0   maxlim: 38998   bits: 16/16
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2203 |  107352   334879 |   35784    2203   222373   100.9 |  1.396 % |
c |      2303 |  107352   334879 |   39362    2303   231648   100.6 |  1.403 % |
c |      2454 |  107352   334879 |   43298    2454   238130    97.0 |  1.403 % |
c |      2679 |  107352   334879 |   47628    2679   261418    97.6 |  1.403 % |
c |      3017 |  107352   334879 |   52391    3017   299302    99.2 |  1.403 % |
c |      3523 |  107352   334879 |   57630    3523   358994   101.9 |  1.403 % |
c |      4282 |  107352   334879 |   63393    4282   556963   130.1 |  1.403 % |
c |      5423 |  107352   334879 |   69732    5423   668556   123.3 |  1.403 % |
c |      7131 |  107352   334879 |   76706    7131  1051149   147.4 |  1.403 % |
c |      9693 |  107352   334879 |   84376    9693  1678687   173.2 |  1.403 % |
c ==============================================================================
c Found solution: 996
c ---[   0]---> Adder-cost: 0   maxlim: 39004   bits: 16/16
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     10487 |  107358   334918 |   35786   10487  1847516   176.2 |  1.403 % |
c |     10587 |  107358   334918 |   39364   10587  1855693   175.3 |  1.412 % |
c |     10742 |  107358   334918 |   43301   10742  1874690   174.5 |  1.412 % |
c |     10967 |  107358   334918 |   47631   10967  1906062   173.8 |  1.412 % |
c |     11305 |  107358   334918 |   52394   11305  1959943   173.4 |  1.412 % |
c |     11812 |  107358   334918 |   57633   11812  1996652   169.0 |  1.412 % |
c |     12571 |  107358   334918 |   63397   12571  2137300   170.0 |  1.412 % |
c |     13711 |  107358   334918 |   69736   13711  2382440   173.8 |  1.412 % |
c |     15420 |  107358   334918 |   76710   15420  2702133   175.2 |  1.412 % |
c |     17982 |  107358   334918 |   84381   17982  3128960   174.0 |  1.412 % |
c |     21828 |  107358   334918 |   92819   21828  4322375   198.0 |  1.412 % |
c ==============================================================================
c Found solution: 988
c ---[   0]---> Adder-cost: 0   maxlim: 39012   bits: 16/16
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     26309 |  107364   334954 |   35788   26309  5311365   201.9 |  1.412 % |
c |     26410 |  107364   334954 |   39366   26410  5315345   201.3 |  1.422 % |
c |     26560 |  107364   334954 |   43303   26560  5332309   200.8 |  1.422 % |
c |     26785 |  107364   334954 |   47633   26785  5362018   200.2 |  1.422 % |
c |     27124 |  107364   334954 |   52397   27124  5390674   198.7 |  1.422 % |
c |     27630 |  107364   334954 |   57636   27630  5447812   197.2 |  1.422 % |
c |     28389 |  107364   334954 |   63400   28389  5585909   196.8 |  1.422 % |
c |     29531 |  107364   334954 |   69740   29531  5829841   197.4 |  1.422 % |
c |     31240 |  107364   334954 |   76714   31240  6204331   198.6 |  1.422 % |
c |     33803 |  107364   334954 |   84386   33803  6860637   203.0 |  1.422 % |
c ==============================================================================
c Found solution: 968
c ---[   0]---> Adder-cost: 0   maxlim: 39032   bits: 16/16
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     36639 |  107367   334983 |   35789   36639  7564651   206.5 |  1.422 % |
c |     36739 |  107367   334983 |   39367   14978  2527851   168.8 |  1.432 % |
c |     36890 |  107367   334983 |   43304   15129  2533125   167.4 |  1.432 % |
c |     37115 |  107367   334983 |   47635   15354  2573774   167.6 |  1.432 % |
c |     37454 |  107367   334983 |   52398   15693  2610219   166.3 |  1.432 % |
c |     37961 |  107367   334983 |   57638   16200  2689774   166.0 |  1.432 % |
c |     38720 |  107367   334983 |   63402   16959  2861332   168.7 |  1.432 % |
c |     39859 |  107367   334983 |   69742   18098  3049027   168.5 |  1.432 % |
c |     41567 |  107367   334983 |   76716   19806  3582639   180.9 |  1.432 % |
c |     44129 |  107367   334983 |   84388   22368  4081259   182.5 |  1.432 % |
c |     47975 |  107367   334983 |   92827   26214  4924789   187.9 |  1.432 % |
c |     53742 |  107367   334983 |  102110   31981  6839322   213.9 |  1.432 % |
c |     62393 |  107367   334983 |  112321   40632  9147539   225.1 |  1.432 % |
c |     75367 |  107367   334983 |  123553   53606 13432995   250.6 |  1.432 % |
c |     94828 |  107367   334983 |  135908   73067 18583473   254.3 |  1.432 % |
c ==============================================================================
c Found solution: 962
c ---[   0]---> Adder-cost: 0   maxlim: 39038   bits: 16/16
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    102932 |  107372   335020 |   35790   81171 21091129   259.8 |  1.432 % |
c |    103038 |  107372   335020 |   39369   18351  3797324   206.9 |  1.441 % |
c |    103188 |  107372   335020 |   43305   18501  3819105   206.4 |  1.441 % |
c |    103414 |  107372   335020 |   47636   18727  3851268   205.7 |  1.441 % |
c |    103751 |  107372   335020 |   52400   19064  3898650   204.5 |  1.441 % |
c |    104258 |  107372   335020 |   57640   19571  3960880   202.4 |  1.441 % |
c |    105018 |  107372   335020 |   63404   20331  4055134   199.5 |  1.441 % |
c |    106157 |  107372   335020 |   69744   21470  4306107   200.6 |  1.441 % |
c |    107866 |  107372   335020 |   76719   23179  4672492   201.6 |  1.441 % |
c |    110428 |  107372   335020 |   84390   25741  5195896   201.9 |  1.441 % |
c |    114274 |  107372   335020 |   92830   29587  5870348   198.4 |  1.441 % |
c |    120042 |  107372   335020 |  102113   35355  7088827   200.5 |  1.441 % |
c |    128698 |  107372   335020 |  112324   44011  9766073   221.9 |  1.441 % |
c |    141672 |  107372   335020 |  123556   56985 14217045   249.5 |  1.441 % |
c |    161142 |  107372   335020 |  135912   76455 21190245   277.2 |  1.441 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v -x226_bit0 -x227_bit0 -x228_bit0 -x229_bit0 -x230_bit0 -x231_bit0 -x232_bit0 -x233_bit0 -x234_bit0 -x235_bit0 -x236_bit0 -x237_bit0 -x238_bit0 -x239_bit0 -x240_bit0 -x241_bit0 -x242_bit0 -x243_bit0 x244_bit0 -x245_bit0 -x246_bit0 -x247_bit0 -x248_bit0 -x249_bit0 -x250_bit0 -x251_bit0 -x252_bit0 -x253_bit0 -x254_bit0 -x255_bit0 -x256_bit0 -x257_bit0 -x258_bit0 -x259_bit0 -x260_bit0 -x261_bit0 -x262_bit0 -x263_bit0 -x264_bit0 -x265_bit0 -x266_bit0 -x267_bit0 -x268_bit0 -x269_bit0 -x270_bit0 -x271_bit0 -x272_bit0 -x273_bit0 -x274_bit0 -x275_bit0 -x276_bit0 -x277_bit0 -x278_bit0 -x279_bit0 -x280_bit0 -x281_bit0 -x282_bit0 -x283_bit0 -x284_bit0 -x285_bit0 -x286_bit0 -x287_bit0 -x288_bit0 -x289_bit0 -x290_bit0 -x291_bit0 -x292_bit0 x293_bit0 -x294_bit0 -x295_bit0 -x296_bit0 -x297_bit0 -x298_bit0 -x299_bit0 -x300_bit0 -x301_bit0 -x302_bit0 -x303_bit0 -x304_bit0 -x305_bit0 -x306_bit0 -x307_bit0 -x308_bit0 -x309_bit0 -x310_bit0 -x311_bit0 -x312_bit0 -x313_bit0 -x314_bit0 -x315_bit0 -x316_bit0 -x317_bit0 -x318_bit0 -x319_bit0 -x320_bit0 -x321_bit0 -x322_bit0 -x323_bit0 -x324_bit0 -x325_bit0 -x326_bit0 -x327_bit0 -x328_bit0 -x329_bit0 -x330_bit0 -x331_bit0 -x332_bit0 -x333_bit0 -x334_bit0 -x335_bit0 -x336_bit0 -x337_bit0 -x338_bit0 -x339_bit0 -x340_bit0 -x341_bit0 -x342_bit0 -x343_bit0 -x344_bit0 -x345_bit0 -x346_bit0 -x347_bit0 x348_bit0 -x349_bit0 -x350_bit0 -x351_bit0 -x352_bit0 -x353_bit0 -x354_bit0 -x355_bit0 -x356_bit0 -x357_bit0 -x358_bit0 -x359_bit0 -x360_bit0 -x361_bit0 -x362_bit0 -x363_bit0 -x364_bit0 -x365_bit0 -x366_bit0 -x367_bit0 -x368_bit0 -x369_bit0 -x370_bit0 -x371_bit0 -x372_bit0 -x373_bit0 -x374_bit0 -x375_bit0 -x376_bit0 -x377_bit0 -x378_bit0 -x379_bit0 -x380_bit0 -x381_bit0 -x382_bit0 -x383_bit0 -x384_bit0 -x385_bit0 -x386_bit0 -x387_bit0 -x388_bit0 -x389_bit0 -x390_bit0 -x391_bit0 -x392_bit0 -x393_bit0 -x394_bit0 -x395_bit0 -x396_bit0 -x397_bit0 -x398_bit0 x399_bit0 -x400_bit0 -x401_bit0 -x402_bit0 -x403_bit0 -x404_bit0 -x405_bit0 -x406_bit0 -x407_bit0 -x408_bit0 -x409_bit0 -x410_bit0 -x411_bit0 -x412_bit0 -x413_bit0 -x414_bit0 -x415_bit0 x416_bit0 -x417_bit0 -x418_bit0 -x419_bit0 -x420_bit0 -x421_bit0 -x422_bit0 -x423_bit0 -x424_bit0 -x425_bit0 -x426_bit0 -x427_bit0 -x428_bit0 -x429_bit0 -x430_bit0 -x431_bit0 -x432_bit0 -x433_bit0 -x434_bit0 -x435_bit0 -x436_bit0 -x437_bit0 -x438_bit0 -x439_bit0 -x440_bit0 -x441_bit0 -x442_bit0 -x443_bit0 -x444_bit0 -x445_bit0 -x446_bit0 -x447_bit0 -x448_bit0 -x449_bit0 -x450_bit0 -x451_bit0 -x452_bit0 -x453_bit0 -x454_bit0 -x455_bit0 -x456_bit0 -x457_bit0 -x458_bit0 -x459_bit0 -x460_bit0 -x461_bit0 -x462_bit0 -x463_bit0 -x464_bit0 -x465_bit0 -x466_bit0 -x467_bit0 -x468_bit0 -x469_bit0 -x470_bit0 -x471_bit0 -x472_bit0 -x473_bit0 -x474_bit0 -x475_bit0 -x476_bit0 -x477_bit0 -x478_bit0 -x479_bit0 -x480_bit0 -x481_bit0 -x482_bit0 -x483_bit0 -x484_bit0 x485_bit0 -x486_bit0 -x487_bit0 -x488_bit0 -x489_bit0 -x490_bit0 -x491_bit0 -x492_bit0 -x493_bit0 -x494_bit0 -x495_bit0 -x496_bit0 -x497_bit0 -x498_bit0 -x499_bit0 -x500_bit0 -x501_bit0 -x502_bit0 -x503_bit0 -x504_bit0 -x505_bit0 -x506_bit0 -x507_bit0 -x508_bit0 -x509_bit0 -x510_bit0 -x511_bit0 -x512_bit0 -x513_bit0 -x514_bit0 -x515_bit0 -x516_bit0 x517_bit0 -x518_bit0 -x519_bit0 -x520_bit0 -x521_bit0 -x522_bit0 -x523_bit0 -x524_bit0 -x525_bit0 -x526_bit0 -x527_bit0 -x528_bit0 -x529_bit0 -x530_bit0 -x531_bit0 -x532_bit0 -x533_bit0 -x534_bit0 -x535_bit0 -x536_bit0 -x537_bit0 -x538_bit0 -x539_bit0 -x540_bit0 -x541_bit0 -x542_bit0 -x543_bit0 -x544_bit0 x545_bit0 -x546_bit0 -x547_bit0 -x548_bit0 -x549_bit0 -x550_bit0 -x551_bit0 -x552_bit0 -x553_bit0 -x554_bit0 -x555_bit0 -x556_bit0 -x557_bit0 -x558_bit0 -x559_bit0 -x560_bit0 -x561_bit0 -x562_bit0 -x563_bit0 -x564_bit0 -x565_bit0 -x566_bit0 -x567_bit0 -x568_bit0 -x569_bit0 -x570_bit0 -x571_bit0 -x572_bit0 -x573_bit0 -x574_bit0 -x575_bit0 -x576_bit0 -x577_bit0 -x578_bit0 -x579_bit0 -x580_bit0 -x581_bit0 -x582_bit0 -x583_bit0 -x584_bit0 -x585_bit0 -x586_bit0 -x587_bit0 -x588_bit0 -x589_bit0 -x590_bit0 -x591_bit0 -x592_bit0 -x593_bit0 -x594_bit0 -x595_bit0 -x596_bit0 -x597_bit0 x598_bit0 -x599_bit0 -x600_bit0 -x601_bit0 -x602_bit0 -x603_bit0 -x604_bit0 -x605_bit0 -x606_bit0 -x607_bit0 -x608_bit0 -x609_bit0 -x610_bit0 -x611_bit0 -x612_bit0 -x613_bit0 -x614_bit0 -x615_bit0 -x616_bit0 -x617_bit0 -x618_bit0 -x619_bit0 -x620_bit0 -x621_bit0 -x622_bit0 -x623_bit0 -x624_bit0 -x625_bit0 -x626_bit0 -x627_bit0 -x628_bit0 -x629_bit0 -x630_bit0 -x631_bit0 -x632_bit0 -x633_bit0 -x634_bit0 -x635_bit0 -x636_bit0 -x637_bit0 -x638_bit0 -x639_bit0 -x640_bit0 -x641_bit0 -x642_bit0 -x643_bit0 -x644_bit0 -x645_bit0 -x646_bit0 -x647_bit0 -x648_bit0 -x649_bit0 -x650_bit0 -x651_bit0 -x652_bit0 -x653_bit0 -x654_bit0 -x655_bit0 -x656_bit0 -x657_bit0 -x658_bit0 -x659_bit0 -x660_bit0 -x661_bit0 -x662_bit0 -x663_bit0 -x664_bit0 -x665_bit0 -x666_bit0 -x667_bit0 -x668_bit0 -x669_bit0 -x670_bit0 x671_bit0 -x672_bit0 -x673_bit0 -x674_bit0 -x675_bit0 -x676_bit0 -x677_bit0 -x678_bit0 -x679_bit0 -x680_bit0 -x681_bit0 -x682_bit0 -x683_bit0 -x684_bit0 -x685_bit0 -x686_bit0 -x687_bit0 -x688_bit0 -x689_bit0 -x690_bit0 -x691_bit0 -x692_bit0 -x693_bit0 -x694_bit0 -x695_bit0 -x696_bit0 -x697_bit0 -x698_bit0 -x699_bit0 -x700_bit0 -x701_bit0 x702_bit0 -x703_bit0 -x704_bit0 -x705_bit0 -x706_bit0 -x707_bit0 -x708_bit0 -x709_bit0 -x710_bit0 -x711_bit0 -x712_bit0 -x713_bit0 -x714_bit0 -x715_bit0 -x716_bit0 -x717_bit0 -x718_bit0 -x719_bit0 -x720_bit0 -x721_bit0 -x722_bit0 -x723_bit0 -x724_bit0 -x725_bit0 -x726_bit0 -x727_bit0 -x728_bit0 -x729_bit0 -x730_bit0 -x731_bit0 -x732_bit0 -x733_bit0 -x734_bit0 -x735_bit0 -x736_bit0 -x737_bit0 -x738_bit0 -x739_bit0 x740_bit0 -x741_bit0 -x742_bit0 -x743_bit0 -x744_bit0 -x745_bit0 -x746_bit0 -x747_bit0 -x748_bit0 -x749_bit0 -x750_bit0 -x751_bit0 -x752_bit0 -x753_bit0 -x754_bit0 -x755_bit0 -x756_bit0 -x757_bit0 -x758_bit0 -x759_bit0 -x760_bit0 -x761_bit0 -x762_bit0 -x763_bit0 -x764_bit0 -x765_bit0 -x766_bit0 -x767_bit0 -x768_bit0 -x769_bit0 -x770_bit0 -x771_bit0 -x772_bit0 -x773_bit0 -x774_bit0 -x775_bit0 -x776_bit0 -x777_bit0 -x778_bit0 -x779_bit0 -x780_bit0 -x781_bit0 -x782_bit0 -x783_bit0 -x784_bit0 -x785_bit0 -x786_bit0 -x787_bit0 -x788_bit0 -x789_bit0 -x790_bit0 -x791_bit0 -x792_bit0 -x793_bit0 -x794_bit0 -x795_bit0 -x796_bit0 -x797_bit0 -x798_bit0 -x799_bit0 -x800_bit0 -x801_bit0 x802_bit0 -x803_bit0 -x804_bit0 -x805_bit0 -x806_bit0 -x807_bit0 -x808_bit0 -x809_bit0 -x810_bit0 -x811_bit0 -x812_bit0 -x813_bit0 -x814_bit0 -x815_bit0 -x816_bit0 -x817_bit0 -x818_bit0 -x819_bit0 -x820_bit0 -x821_bit0 -x822_bit0 -x823_bit0 -x824_bit0 -x825_bit0 -x826_bit0 -x827_bit0 -x828_bit0 -x829_bit0 -x830_bit0 -x831_bit0 -x832_bit0 -x833_bit0 -x834_bit0 -x835_bit0 -x836_bit0 -x837_bit0 -x838_bit0 -x839_bit0 -x840_bit0 -x841_bit0 x842_bit0 -x843_bit0 -x844_bit0 -x845_bit0 -x846_bit0 -x847_bit0 -x848_bit0 -x849_bit0 -x850_bit0 -x851_bit0 -x852_bit0 -x853_bit0 -x854_bit0 -x855_bit0 -x856_bit0 -x857_bit0 x858_bit0 -x859_bit0 -x860_bit0 -x861_bit0 -x862_bit0 -x863_bit0 -x864_bit0 -x865_bit0 -x866_bit0 -x867_bit0 -x868_bit0 -x869_bit0 -x870_bit0 -x871_bit0 -x872_bit0 -x873_bit0 -x874_bit0 -x875_bit0 -x876_bit0 -x877_bit0 -x878_bit0 -x879_bit0 -x880_bit0 -x881_bit0 -x882_bit0 -x883_bit0 -x884_bit0 -x885_bit0 -x886_bit0 -x887_bit0 -x888_bit0 -x889_bit0 -x890_bit0 -x891_bit0 -x892_bit0 -x893_bit0 -x894_bit0 -x895_bit0 -x896_bit0 -x897_bit0 -x898_bit0 -x899_bit0 -x900_bit0 -x901_bit0 -x902_bit0 -x903_bit0 -x904_bit0 -x905_bit0 -x906_bit0 -x907_bit0 -x908_bit0 -x909_bit0 -x910_bit0 -x911_bit0 -x912_bit0 -x913_bit0 -x914_bit0 -x915_bit0 -x916_bit0 -x917_bit0 -x918_bit0 -x919_bit0 -x920_bit0 -x921_bit0 -x922_bit0 -x923_bit0 -x924_bit0 -x925_bit0 x926_bit0 -x927_bit0 -x928_bit0 -x929_bit0 -x930_bit0 -x931_bit0 -x932_bit0 -x933_bit0 -x934_bit0 -x935_bit0 -x936_bit0 -x937_bit0 -x938_bit0 -x939_bit0 -x940_bit0 -x941_bit0 -x942_bit0 -x943_bit0 -x944_bit0 -x945_bit0 -x946_bit0 -x947_bit0 -x948_bit0 -x949_bit0 -x950_bit0 -x951_bit0 -x952_bit0 -x953_bit0 -x954_bit0 -x955_bit0 -x956_bit0 -x957_bit0 -x958_bit0 -x959_bit0 -x960_bit0 -x961_bit0 -x962_bit0 -x963_bit0 -x964_bit0 -x965_bit0 -x966_bit0 -x967_bit0 -x968_bit0 -x969_bit0 -x970_bit0 -x971_bit0 -x972_bit0 -x973_bit0 -x974_bit0 -x975_bit0 x976_bit0 -x977_bit0 -x978_bit0 -x979_bit0 -x980_bit0 -x981_bit0 -x982_bit0 -x983_bit0 -x984_bit0 -x985_bit0 -x986_bit0 -x987_bit0 -x988_bit0 -x989_bit0 -x990_bit0 -x991_bit0 -x992_bit0 -x993_bit0 -x994_bit0 -x995_bit0 -x996_bit0 -x997_bit0 -x998_bit0 -x999_bit0 -x1000_bit0 -x1001_bit0 -x1002_bit0 -x1003_bit0 x1004_bit0 -x1005_bit0 -x1006_bit0 -x1007_bit0 -x1008_bit0 -x1009_bit0 -x1010_bit0 -x1011_bit0 -x1012_bit0 -x1013_bit0 -x1014_bit0 -x1015_bit0 -x1016_bit0 -x1017_bit0 -x1018_bit0 -x1019_bit0 -x1020_bit0 -x1021_bit0 -x1022_bit0 -x1023_bit0 -x1024_bit0 -x1025_bit0 -x1026_bit0 -x1027_bit0 -x1028_bit0 -x1029_bit0 -x1030_bit0 -x1031_bit0 -x1032_bit0 -x1033_bit0 -x1034_bit0 -x1035_bit0 -x1036_bit0 -x1037_bit0 -x1038_bit0 -x1039_bit0 -x1040_bit0 -x1041_bit0 -x1042_bit0 -x1043_bit0 -x1044_bit0 -x1045_bit0 -x1046_bit0 -x1047_bit0 -x1048_bit0 -x1049_bit0 -x1050_bit0 -x1051_bit0 -x1052_bit0 -x1053_bit0 -x1054_bit0 -x1055_bit0 -x1056_bit0 -x1057_bit0 -x1058_bit0 -x1059_bit0 -x1060_bit0 -x1061_bit0 -x1062_bit0 -x1063_bit0 -x1064_bit0 -x1065_bit0 -x1066_bit0 -x1067_bit0 -x1068_bit0 -x1069_bit0 -x1070_bit0 -x1071_bit0 -x1072_bit0 x1073_bit0 -x1074_bit0 -x1075_bit0 -x1076_bit0 -x1077_bit0 -x1078_bit0 -x1079_bit0 -x1080_bit0 -x1081_bit0 -x1082_bit0 -x1083_bit0 -x1084_bit0 -x1085_bit0 -x1086_bit0 -x1087_bit0 -x1088_bit0 -x1089_bit0 -x1090_bit0 -x1091_bit0 -x1092_bit0 -x1093_bit0 -x1094_bit0 -x1095_bit0 x1096_bit0 -x1097_bit0 -x1098_bit0 -x1099_bit0 -x1100_bit0 -x1101_bit0 -x1102_bit0 -x1103_bit0 -x1104_bit0 -x1105_bit0 -x1106_bit0 -x1107_bit0 -x1108_bit0 -x1109_bit0 -x1110_bit0 -x1111_bit0 -x1112_bit0 -x1113_bit0 -x1114_bit0 -x1115_bit0 -x1116_bit0 -x1117_bit0 -x1118_bit0 -x1119_bit0 -x1120_bit0 -x1121_bit0 -x1122_bit0 -x1123_bit0 -x1124_bit0 -x1125_bit0 -x1126_bit0 -x1127_bit0 -x1128_bit0 -x1129_bit0 -x1130_bit0 -x1131_bit0 -x1132_bit0 -x1133_bit0 -x1134_bit0 -x1135_bit0 -x1136_bit0 -x1137_bit0 -x1138_bit0 -x1139_bit0 -x1140_bit0 -x1141_bit0 -x1142_bit0 -x1143_bit0 -x1144_bit0 -x1145_bit0 -x1146_bit0 -x1147_bit0 -x1148_bit0 -x1149_bit0 -x1150_bit0 -x1151_bit0 -x1152_bit0 -x1153_bit0 x1154_bit0 -x1155_bit0 -x1156_bit0 -x1157_bit0 -x1158_bit0 -x1159_bit0 -x1160_bit0 -x1161_bit0 -x1162_bit0 -x1163_bit0 -x1164_bit0 -x1165_bit0 -x1166_bit0 -x1167_bit0 -x1168_bit0 -x1169_bit0 -x1170_bit0 -x1171_bit0 -x1172_bit0 -x1173_bit0 -x1174_bit0 -x1175_bit0 -x1176_bit0 -x1177_bit0 -x1178_bit0 -x1179_bit0 -x1180_bit0 -x1181_bit0 -x1182_bit0 -x1183_bit0 -x1184_bit0 -x1185_bit0 -x1186_bit0 -x1187_bit0 -x1188_bit0 -x1189_bit0 -x1190_bit0 -x1191_bit0 -x1192_bit0 -x1193_bit0 -x1194_bit0 -x1195_bit0 -x1196_bit0 -x1197_bit0 -x1198_bit0 -x1199_bit0 -x1200_bit0 -x1201_bit0 -x1202_bit0 -x1203_bit0 -x1204_bit0 -x1205_bit0 -x1206_bit0 -x1207_bit0 -x1208_bit0 -x1209_bit0 -x1210_bit0 -x1211_bit0 x1212_bit0 -x1213_bit0 -x1214_bit0 -x1215_bit0 -x1216_bit0 -x1217_bit0 -x1218_bit0 -x1219_bit0 -x1220_bit0 -x1221_bit0 -x1222_bit0 -x1223_bit0 -x1224_bit0 -x1225_bit0 -x1226_bit0 -x1227_bit0 -x1228_bit0 -x1229_bit0 -x1230_bit0 -x1231_bit0 -x1232_bit0 x1233_bit0 -x1234_bit0 -x1235_bit0 -x1236_bit0 -x1237_bit0 -x1238_bit0 -x1239_bit0 -x1240_bit0 -x1241_bit0 -x1242_bit0 -x1243_bit0 -x1244_bit0 -x1245_bit0 -x1246_bit0 -x1247_bit0 -x1248_bit0 -x1249_bit0 -x1250_bit0 -x1251_bit0 -x1252_bit0 -x1253_bit0 -x1254_bit0 -x1255_bit0 -x1256_bit0 -x1257_bit0 -x1258_bit0 -x1259_bit0 -x1260_bit0 -x1261_bit0 -x1262_bit0 -x1263_bit0 -x1264_bit0 -x1265_bit0 -x1266_bit0 -x1267_bit0 x1268_bit0 -x1269_bit0 -x1270_bit0 -x1271_bit0 -x1272_bit0 -x1273_bit0 -x1274_bit0 -x1275_bit0 -x1276_bit0 -x1277_bit0 -x1278_bit0 -x1279_bit0 -x1280_bit0 -x1281_bit0 -x1282_bit0 -x1283_bit0 -x1284_bit0 -x1285_bit0 -x1286_bit0 -x1287_bit0 -x1288_bit0 -x1289_bit0 -x1290_bit0 -x1291_bit0 -x1292_bit0 -x1293_bit0 -x1294_bit0 -x1295_bit0 -x1296_bit0 -x1297_bit0 -x1298_bit0 -x1299_bit0 -x1300_bit0 -x1301_bit0 -x1302_bit0 -x1303_bit0 -x1304_bit0 -x1305_bit0 -x1306_bit0 -x1307_bit0 -x1308_bit0 -x1309_bit0 -x1310_bit0 -x1311_bit0 -x1312_bit0 -x1313_bit0 -x1314_bit0 -x1315_bit0 -x1316_bit0 -x1317_bit0 -x1318_bit0 -x1319_bit0 -x1320_bit0 -x1321_bit0 -x1322_bit0 -x1323_bit0 -x1324_bit0 -x1325_bit0 -x1326_bit0 -x1327_bit0 -x1328_bit0 -x1329_bit0 x1330_bit0 -x1331_bit0 -x1332_bit0 -x1333_bit0 -x1334_bit0 -x1335_bit0 -x1336_bit0 -x1337_bit0 -x1338_bit0 -x1339_bit0 -x1340_bit0 -x1341_bit0 -x1342_bit0 -x1343_bit0 -x1344_bit0 -x1345_bit0 -x1346_bit0 -x1347_bit0 -x1348_bit0 -x1349_bit0 -x1350_bit0 -x1351_bit0 -x1352_bit0 -x1353_bit0 -x1354_bit0 -x1355_bit0 -x1356_bit0 -x1357_bit0 -x1358_bit0 -x1359_bit0 -x1360_bit0 -x1361_bit0 x1362_bit0 -x1363_bit0 -x1364_bit0 -x1365_bit0 -x1366_bit0 -x1367_bit0 -x1368_bit0 -x1369_bit0 -x1370_bit0 -x1371_bit0 -x1372_bit0 -x1373_bit0 -x1374_bit0 -x1375_bit0 -x1376_bit0 -x1377_bit0 -x1378_bit0 -x1379_bit0 -x1380_bit0 -x1381_bit0 -x1382_bit0 -x1383_bit0 -x1384_bit0 -x1385_bit0 -x1386_bit0 -x1387_bit0 -x1388_bit0 -x1389_bit0 -x1390_bit0 -x1391_bit0 -x1392_bit0 -x1393_bit0 -x1394_bit0 -x1395_bit0 -x1396_bit0 -x1397_bit0 -x1398_bit0 -x1399_bit0 -x1400_bit0 -x1401_bit0 -x1402_bit0 -x1403_bit0 -x1404_bit0 -x1405_bit0 -x1406_bit0 -x1407_bit0 -x1408_bit0 -x1409_bit0 -x1410_bit0 -x1411_bit0 -x1412_bit0 -x1413_bit0 -x1414_bit0 -x1415_bit0 -x1416_bit0 -x1417_bit0 -x1418_bit0 -x1419_bit0 -x1420_bit0 -x1421_bit0 -x1422_bit0 -x1423_bit0 -x1424_bit0 -x1425_bit0 -x1426_bit0 -x1427_bit0 -x1428_bit0 -x1429_bit0 -x1430_bit0 -x1431_bit0 -x1432_bit0 -x1433_bit0 -x1434_bit0 -x1435_bit0 -x1436_bit0 -x1437_bit0 x1438_bit0 -x1439_bit0 -x1440_bit0 -x1441_bit0 x1442_bit0 -x1443_bit0 -x1444_bit0 -x1445_bit0 -x1446_bit0 -x1447_bit0 -x1448_bit0 -x1449_bit0 -x1450_bit0 -x1451_bit0 -x1452_bit0 -x1453_bit0 -x1454_bit0 -x1455_bit0 -x1456_bit0 -x1457_bit0 -x1458_bit0 -x1459_bit0 -x1460_bit0 -x1461_bit0 -x1462_bit0 -x1463_bit0 -x1464_bit0 -x1465_bit0 -x1466_bit0 -x1467_bit0 -x1468_bit0 -x1469_bit0 -x1470_bit0 -x1471_bit0 -x1472_bit0 -x1473_bit0 -x1474_bit0 -x1475_bit0 -x1476_bit0 -x1477_bit0 -x1478_bit0 -x1479_bit0 -x1480_bit0 -x1481_bit0 -x1482_bit0 -x1483_bit0 -x1484_bit0 -x1485_bit0 -x1486_bit0 -x1487_bit0 -x1488_bit0 -x1489_bit0 -x1490_bit0 -x1491_bit0 -x1492_bit0 -x1493_bit0 -x1494_bit0 -x1495_bit0 -x1496_bit0 -x1497_bit0 -x1498_bit0 -x1499_bit0 -x1500_bit0 -x1501_bit0 -x1502_bit0 -x1503_bit0 -x1504_bit0 -x1505_bit0 -x1506_bit0 -x1507_bit0 -x1508_bit0 -x1509_bit0 -x1510_bit0 -x1511_bit0 -x1512_bit0 -x1513_bit0 -x1514_bit0 -x1515_bit0 -x1516_bit0 -x1517_bit0 -x1518_bit0 -x1519_bit0 -x1520_bit0 x1521_bit0 -x1522_bit0 -x1523_bit0 -x1524_bit0 -x1525_bit0 -x1526_bit0 -x1527_bit0 -x1528_bit0 -x1529_bit0 -x1530_bit0 -x1531_bit0 -x1532_bit0 -x1533_bit0 -x1534_bit0 -x1535_bit0 -x1536_bit0 -x1537_bit0 -x1538_bit0 -x1539_bit0 x1540_bit0 -x1541_bit0 -x1542_bit0 -x1543_bit0 -x1544_bit0 -x1545_bit0 -x1546_bit0 -x1547_bit0 -x1548_bit0 -x1549_bit0 -x1550_bit0 -x1551_bit0 -x1552_bit0 -x1553_bit0 -x1554_bit0 -x1555_bit0 -x1556_bit0 -x1557_bit0 -x1558_bit0 -x1559_bit0 -x1560_bit0 -x1561_bit0 -x1562_bit0 -x1563_bit0 -x1564_bit0 -x1565_bit0 -x1566_bit0 -x1567_bit0 -x1568_bit0 -x1569_bit0 -x1570_bit0 -x1571_bit0 -x1572_bit0 -x1573_bit0 -x1574_bit0 -x1575_bit0 -x1576_bit0 -x1577_bit0 -x1578_bit0 -x1579_bit0 -x1580_bit0 -x1581_bit0 -x1582_bit0 -x1583_bit0 -x1584_bit0 -x1585_bit0 -x1586_bit0 -x1587_bit0 -x1588_bit0 -x1589_bit0 -x1590_bit0 -x1591_bit0 -x1592_bit0 -x1593_bit0 -x1594_bit0 -x1595_bit0 -x1596_bit0 -x1597_bit0 -x1598_bit0 -x1599_bit0 -x1600_bit0 -x1601_bit0 -x1602_bit0 -x1603_bit0 -x1604_bit0 -x1605_bit0 -x1606_bit0 -x1607_bit0 -x1608_bit0 -x1609_bit0 -x1610_bit0 -x1611_bit0 -x1612_bit0 -x1613_bit0 -x1614_bit0 x1615_bit0 -x1616_bit0 -x1617_bit0 -x1618_bit0 -x1619_bit0 -x1620_bit0 -x1621_bit0 -x1622_bit0 -x1623_bit0 -x1624_bit0 -x1625_bit0 -x1626_bit0 x1627_bit0 -x1628_bit0 -x1629_bit0 -x1630_bit0 -x1631_bit0 -x1632_bit0 -x1633_bit0 -x1634_bit0 -x1635_bit0 -x1636_bit0 -x1637_bit0 -x1638_bit0 -x1639_bit0 -x1640_bit0 -x1641_bit0 -x1642_bit0 -x1643_bit0 -x1644_bit0 -x1645_bit0 -x1646_bit0 -x1647_bit0 -x1648_bit0 -x1649_bit0 -x1650_bit0 -x1651_bit0 -x1652_bit0 -x1653_bit0 -x1654_bit0 -x1655_bit0 -x1656_bit0 -x1657_bit0 -x1658_bit0 -x1659_bit0 -x1660_bit0 -x1661_bit0 -x1662_bit0 -x1663_bit0 -x1664_bit0 -x1665_bit0 -x1666_bit0 -x1667_bit0 -x1668_bit0 -x1669_bit0 -x1670_bit0 -x1671_bit0 -x1672_bit0 -x1673_bit0 -x1674_bit0 -x1675_bit0 -x1676_bit0 -x1677_bit0 -x1678_bit0 -x1679_bit0 -x1680_bit0 -x1681_bit0 -x1682_bit0 -x1683_bit0 -x1684_bit0 -x1685_bit0 -x1686_bit0 -x1687_bit0 -x1688_bit0 -x1689_bit0 -x1690_bit0 -x1691_bit0 -x1692_bit0 -x1693_bit0 -x1694_bit0 x1695_bit0 -x1696_bit0 -x1697_bit0 -x1698_bit0 -x1699_bit0 -x1700_bit0 -x1701_bit0 -x1702_bit0 -x1703_bit0 -x1704_bit0 -x1705_bit0 -x1706_bit0 -x1707_bit0 -x1708_bit0 -x1709_bit0 -x1710_bit0 -x1711_bit0 -x1712_bit0 -x1713_bit0 -x1714_bit0 -x1715_bit0 -x1716_bit0 -x1717_bit0 -x1718_bit0 -x1719_bit0 -x1720_bit0 -x1721_bit0 -x1722_bit0 -x1723_bit0 -x1724_bit0 -x1725_bit0 -x1726_bit0 -x1727_bit0 -x1728_bit0 -x1729_bit0 -x1730_bit0 x1731_bit0 -x1732_bit0 -x1733_bit0 -x1734_bit0 -x1735_bit0 -x1736_bit0 -x1737_bit0 -x1738_bit0 -x1739_bit0 -x1740_bit0 -x1741_bit0 -x1742_bit0 -x1743_bit0 -x1744_bit0 -x1745_bit0 -x1746_bit0 -x1747_bit0 -x1748_bit0 -x1749_bit0 -x1750_bit0 -x1751_bit0 -x1752_bit0 -x1753_bit0 -x1754_bit0 -x1755_bit0 -x1756_bit0 -x1757_bit0 -x1758_bit0 -x1759_bit0 -x1760_bit0 -x1761_bit0 -x1762_bit0 -x1763_bit0 -x1764_bit0 -x1765_bit0 -x1766_bit0 -x1767_bit0 -x1768_bit0 -x1769_bit0 -x1770_bit0 -x1771_bit0 -x1772_bit0 -x1773_bit0 -x1774_bit0 -x1775_bit0 -x1776_bit0 -x1777_bit0 -x1778_bit0 x1779_bit0 -x1780_bit0 -x1781_bit0 -x1782_bit0 -x1783_bit0 -x1784_bit0 -x1785_bit0 -x1786_bit0 -x1787_bit0 -x1788_bit0 -x1789_bit0 -x1790_bit0 -x1791_bit0 -x1792_bit0 -x1793_bit0 -x1794_bit0 -x1795_bit0 -x1796_bit0 -x1797_bit0 -x1798_bit0 -x1799_bit0 -x1800_bit0 -x1801_bit0 -x1802_bit0 -x1803_bit0 -x1804_bit0 -x1805_bit0 -x1806_bit0 -x1807_bit0 -x1808_bit0 x1809_bit0 -x1810_bit0 -x1811_bit0 -x1812_bit0 -x1813_bit0 -x1814_bit0 -x1815_bit0 -x1816_bit0 -x1817_bit0 -x1818_bit0 -x1819_bit0 -x1820_bit0 -x1821_bit0 -x1822_bit0 -x1823_bit0 -x1824_bit0 -x1825_bit0 -x1826_bit0 -x1827_bit0 -x1828_bit0 -x1829_bit0 -x1830_bit0 -x1831_bit0 -x1832_bit0 -x1833_bit0 -x1834_bit0 -x1835_bit0 -x1836_bit0 -x1837_bit0 -x1838_bit0 -x1839_bit0 -x1840_bit0 -x1841_bit0 -x1842_bit0 -x1843_bit0 -x1844_bit0 -x1845_bit0 -x1846_bit0 -x1847_bit0 -x1848_bit0 -x1849_bit0 -x1850_bit0 -x1851_bit0 -x1852_bit0 -x1853_bit0 -x1854_bit0 -x1855_bit0 -x1856_bit0 -x1857_bit0 -x1858_bit0 -x1859_bit0 -x1860_bit0 -x1861_bit0 -x1862_bit0 -x1863_bit0 -x1864_bit0 -x1865_bit0 -x1866_bit0 -x1867_bit0 -x1868_bit0 -x1869_bit0 -x1870_bit0 -x1871_bit0 -x1872_bit0 -x1873_bit0 -x1874_bit0 -x1875_bit0 -x1876_bit0 -x1877_bit0 -x1878_bit0 x1879_bit0 -x1880_bit0 -x1881_bit0 -x1882_bit0 -x1883_bit0 -x1884_bit0 -x1885_bit0 -x1886_bit0 -x1887_bit0 -x1888_bit0 -x1889_bit0 -x1890_bit0 -x1891_bit0 -x1892_bit0 -x1893_bit0 -x1894_bit0 -x1895_bit0 -x1896_bit0 -x1897_bit0 -x1898_bit0 -x1899_bit0 -x1900_bit0 -x1901_bit0 -x1902_bit0 -x1903_bit0 -x1904_bit0 -x1905_bit0 -x1906_bit0 -x1907_bit0 -x1908_bit0 -x1909_bit0 -x1910_bit0 -x1911_bit0 -x1912_bit0 -x1913_bit0 -x1914_bit0 -x1915_bit0 -x1916_bit0 -x1917_bit0 -x1918_bit0 -x1919_bit0 -x1920_bit0 -x1921_bit0 -x1922_bit0 -x1923_bit0 -x1924_bit0 -x1925_bit0 -x1926_bit0 -x1927_bit0 -x1928_bit0 -x1929_bit0 -x1930_bit0 -x1931_bit0 -x1932_bit0 -x1933_bit0 x1934_bit0 -x1935_bit0 -x1936_bit0 -x1937_bit0 -x1938_bit0 x1939_bit0 -x1940_bit0 -x1941_bit0 -x1942_bit0 -x1943_bit0 -x1944_bit0 -x1945_bit0 -x1946_bit0 -x1947_bit0 -x1948_bit0 -x1949_bit0 -x1950_bit0 -x1951_bit0 -x1952_bit0 -x1953_bit0 -x1954_bit0 -x1955_bit0 -x1956_bit0 -x1957_bit0 -x1958_bit0 -x1959_bit0 -x1960_bit0 -x1961_bit0 -x1962_bit0 -x1963_bit0 -x1964_bit0 -x1965_bit0 -x1966_bit0 -x1967_bit0 -x1968_bit0 -x1969_bit0 -x1970_bit0 -x1971_bit0 -x1972_bit0 -x1973_bit0 -x1974_bit0 -x1975_bit0 -x1976_bit0 -x1977_bit0 -x1978_bit0 -x1979_bit0 -x1980_bit0 -x1981_bit0 -x1982_bit0 -x1983_bit0 -x1984_bit0 -x1985_bit0 -x1986_bit0 -x1987_bit0 -x1988_bit0 -x1989_bit0 -x1990_bit0 -x1991_bit0 -x1992_bit0 -x1993_bit0 -x1994_bit0 -x1995_bit0 -x1996_bit0 x

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/17829/stat): 17829 (minisat+_script) R 17828 17829 28974 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1851765379 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 0 0 0
Raw data (/proc/17829/statm): 174 3 169 147 0 27 0
[pid=17829] 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=17830
New process pid=17831
New process pid=17832
execve syscall for /bin/sed executable
One traced child (pid=17831) exited with status: 0
open syscall for file /etc/ld.so.preload
open syscall for file tls/i686/mmx/libc.so.6
open syscall for file tls/i686/libc.so.6
open syscall for file tls/mmx/libc.so.6
open syscall for file tls/libc.so.6
open syscall for file i686/mmx/libc.so.6
open syscall for file i686/libc.so.6
open syscall for file mmx/libc.so.6
open syscall for file libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/i686/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/i686/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/libc.so.6
open syscall for file /oldhome/oroussel/lib/i686/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/i686/libc.so.6
open syscall for file /oldhome/oroussel/lib/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/libc.so.6
open syscall for file /etc/ld.so.cache
open syscall for file /lib/tls/libc.so.6
One traced child (pid=17832) exited with status: 0
One traced child (pid=17830) exited with status: 0
New process pid=17833
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc27/normalized-mps-v2-20-10-10teams.opb

[startup+10.004 s]
Raw data (loadavg): 0.93 0.95 0.69 2/57 17833
Raw data (/proc/17829/stat): 17829 (minisat+_script) S 17828 17829 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851765379 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17829/statm): 531 226 485 147 0 384 0
[pid=17829] vsize: 2124
Raw data (/proc/17833/stat): 17833 (minisat+_64-bit) R 17829 17829 28974 0 -1 0 8645 0 2 0 933 31 0 0 25 0 1 0 1851765384 31805440 7175 4294967295 134512640 135094434 3221224432 3221223120 134596445 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17833/statm): 7765 7175 145 145 0 7620 0
[pid=17833] vsize: 31060
Current children cumulated CPU time (s) 9.65
Current children cumulated vsize (Kb) 33184

[startup+20.0058 s]
Raw data (loadavg): 0.94 0.95 0.69 2/57 17833
Raw data (/proc/17829/stat): 17829 (minisat+_script) S 17828 17829 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851765379 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17829/statm): 531 226 485 147 0 384 0
[pid=17829] vsize: 2124
Raw data (/proc/17833/stat): 17833 (minisat+_64-bit) R 17829 17829 28974 0 -1 0 8959 0 2 0 1926 34 0 0 25 0 1 0 1851765384 33071104 7489 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17833/statm): 8074 7489 145 145 0 7929 0
[pid=17833] vsize: 32296
Current children cumulated CPU time (s) 19.61
Current children cumulated vsize (Kb) 34420

[startup+30.0076 s]
Raw data (loadavg): 0.95 0.96 0.70 2/57 17833
Raw data (/proc/17829/stat): 17829 (minisat+_script) S 17828 17829 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851765379 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17829/statm): 531 226 485 147 0 384 0
[pid=17829] vsize: 2124
Raw data (/proc/17833/stat): 17833 (minisat+_64-bit) R 17829 17829 28974 0 -1 0 9366 0 2 0 2919 37 0 0 25 0 1 0 1851765384 34725888 7896 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17833/statm): 8478 7896 145 145 0 8333 0
[pid=17833] vsize: 33912
Current children cumulated CPU time (s) 29.57
Current children cumulated vsize (Kb) 36036

[startup+40.0075 s]
Raw data (loadavg): 0.95 0.96 0.70 2/57 17833
Raw data (/proc/17829/stat): 17829 (minisat+_script) S 17828 17829 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851765379 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17829/statm): 531 226 485 147 0 384 0
[pid=17829] vsize: 2124
Raw data (/proc/17833/stat): 17833 (minisat+_64-bit) R 17829 17829 28974 0 -1 0 9776 0 2 0 3911 40 0 0 25 0 1 0 1851765384 36429824 8306 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17833/statm): 8894 8306 145 145 0 8749 0
[pid=17833] vsize: 35576
Current children cumulated CPU time (s) 39.52
Current children cumulated vsize (Kb) 37700

[startup+50.0093 s]
Raw data (loadavg): 0.96 0.96 0.70 2/57 17833
Raw data (/proc/17829/stat): 17829 (minisat+_script) S 17828 17829 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851765379 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17829/statm): 531 226 485 147 0 384 0
[pid=17829] vsize: 2124
Raw data (/proc/17833/stat): 17833 (minisat+_64-bit) R 17829 17829 28974 0 -1 0 10212 0 2 0 4903 43 0 0 25 0 1 0 1851765384 38207488 8742 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17833/statm): 9328 8742 145 145 0 9183 0
[pid=17833] vsize: 37312
Current children cumulated CPU time (s) 49.47
Current children cumulated vsize (Kb) 39436

[startup+60.0101 s]
Raw data (loadavg): 0.97 0.96 0.71 2/57 17833
Raw data (/proc/17829/stat): 17829 (minisat+_script) S 17828 17829 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851765379 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17829/statm): 531 226 485 147 0 384 0
[pid=17829] vsize: 2124
Raw data (/proc/17833/stat): 17833 (minisat+_64-bit) R 17829 17829 28974 0 -1 0 10713 0 2 0 5897 46 0 0 25 0 1 0 1851765384 39440384 9045 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17833/statm): 9629 9045 145 145 0 9484 0
[pid=17833] vsize: 38516
Current children cumulated CPU time (s) 59.44
Current children cumulated vsize (Kb) 40640

[startup+70.0119 s]
Raw data (loadavg): 0.97 0.96 0.71 2/57 17833
Raw data (/proc/17829/stat): 17829 (minisat+_script) S 17828 17829 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851765379 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17829/statm): 531 226 485 147 0 384 0
[pid=17829] vsize: 2124
Raw data (/proc/17833/stat): 17833 (minisat+_64-bit) R 17829 17829 28974 0 -1 0 11124 0 2 0 6890 50 0 0 25 0 1 0 1851765384 41115648 9456 4294967295 134512640 135094434 3221224432 3221223056 134557737 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17833/statm): 10038 9456 145 145 0 9893 0
[pid=17833] vsize: 40152
Current children cumulated CPU time (s) 69.41
Current children cumulated vsize (Kb) 42276

[startup+80.0127 s]
Raw data (loadavg): 0.98 0.96 0.71 2/57 17833
Raw data (/proc/17829/stat): 17829 (minisat+_script) S 17828 17829 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851765379 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17829/statm): 531 226 485 147 0 384 0
[pid=17829] vsize: 2124
Raw data (/proc/17833/stat): 17833 (minisat+_64-bit) R 17829 17829 28974 0 -1 0 11557 0 2 0 7881 54 0 0 25 0 1 0 1851765384 42946560 9889 4294967295 134512640 135094434 3221224432 3221223024 134557227 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17833/statm): 10485 9889 145 145 0 10340 0
[pid=17833] vsize: 41940
Current children cumulated CPU time (s) 79.36
Current children cumulated vsize (Kb) 44064

[startup+90.0136 s]
Raw data (loadavg): 0.98 0.96 0.71 2/57 17833
Raw data (/proc/17829/stat): 17829 (minisat+_script) S 17828 17829 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851765379 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17829/statm): 531 226 485 147 0 384 0
[pid=17829] vsize: 2124
Raw data (/proc/17833/stat): 17833 (minisat+_64-bit) R 17829 17829 28974 0 -1 0 11986 0 2 0 8873 56 0 0 25 0 1 0 1851765384 44695552 10318 4294967295 134512640 135094434 3221224432 3221223056 134557714 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17833/statm): 10912 10318 145 145 0 10767 0
[pid=17833] vsize: 43648
Current children cumulated CPU time (s) 89.3
Current children cumulated vsize (Kb) 45772

[startup+100.014 s]
Raw data (loadavg): 0.98 0.96 0.72 2/57 17833
Raw data (/proc/17829/stat): 17829 (minisat+_script) S 17828 17829 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851765379 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17829/statm): 531 226 485 147 0 384 0
[pid=17829] vsize: 2124
Raw data (/proc/17833/stat): 17833 (minisat+_64-bit) R 17829 17829 28974 0 -1 0 12413 0 2 0 9866 59 0 0 25 0 1 0 1851765384 46436352 10745 4294967295 134512640 135094434 3221224432 3221223024 134556843 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17833/statm): 11337 10745 145 145 0 11192 0
[pid=17833] vsize: 45348
Current children cumulated CPU time (s) 99.26
Current children cumulated vsize (Kb) 47472

[startup+110.015 s]
Raw data (loadavg): 0.98 0.96 0.72 2/57 17833
Raw data (/proc/17829/stat): 17829 (minisat+_script) S 17828 17829 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851765379 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17829/statm): 531 226 485 147 0 384 0
[pid=17829] vsize: 2124
Raw data (/proc/17833/stat): 17833 (minisat+_64-bit) R 17829 17829 28974 0 -1 0 12878 0 2 0 10860 62 0 0 25 0 1 0 1851765384 48345088 11210 4294967295 134512640 135094434 3221224432 3221223056 134557669 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17833/statm): 11803 11210 145 145 0 11658 0
[pid=17833] vsize: 47212
Current children cumulated CPU time (s) 109.23
Current children cumulated vsize (Kb) 49336

[startup+120.017 s]
Raw data (loadavg): 0.99 0.96 0.72 2/57 17833
Raw data (/proc/17829/stat): 17829 (minisat+_script) S 17828 17829 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851765379 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17829/statm): 531 226 485 147 0 384 0
[pid=17829] vsize: 2124
Raw data (/proc/17833/stat): 17833 (minisat+_64-bit) R 17829 17829 28974 0 -1 0 13238 0 2 0 11853 64 0 0 25 0 1 0 1851765384 49815552 11570 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17833/statm): 12162 11570 145 145 0 12017 0
[pid=17833] vsize: 48648
Current children cumulated CPU time (s) 119.18
Current children cumulated vsize (Kb) 50772

[startup+130.018 s]
Raw data (loadavg): 0.99 0.97 0.73 2/57 17833
Raw data (/proc/17829/stat): 17829 (minisat+_script) S 17828 17829 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851765379 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17829/statm): 531 226 485 147 0 384 0
[pid=17829] vsize: 2124
Raw data (/proc/17833/stat): 17833 (minisat+_64-bit) R 17829 17829 28974 0 -1 0 13643 0 2 0 12847 67 0 0 25 0 1 0 1851765384 51466240 11975 4294967295 134512640 135094434 3221224432 3221223024 134557028 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17833/statm): 12565 11975 145 145 0 12420 0
[pid=17833] vsize: 50260
Current children cumulated CPU time (s) 129.15
Current children cumulated vsize (Kb) 52384

[startup+140.019 s]
Raw data (loadavg): 0.99 0.97 0.73 2/57 17833
Raw data (/proc/17829/stat): 17829 (minisat+_script) S 17828 17829 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851765379 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17829/statm): 531 226 485 147 0 384 0
[pid=17829] vsize: 2124
Raw data (/proc/17833/stat): 17833 (minisat+_64-bit) R 17829 17829 28974 0 -1 0 13989 0 2 0 13842 69 0 0 25 0 1 0 1851765384 52879360 12321 4294967295 134512640 135094434 3221224432 3221223056 134562139 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17833/statm): 12910 12321 145 145 0 12765 0
[pid=17833] vsize: 51640
Current children cumulated CPU time (s) 139.12
Current children cumulated vsize (Kb) 53764

[startup+150.021 s]
Raw data (loadavg): 0.99 0.97 0.73 2/57 17833
Raw data (/proc/17829/stat): 17829 (minisat+_script) S 17828 17829 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851765379 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17829/statm): 531 226 485 147 0 384 0
[pid=17829] vsize: 2124
Raw data (/proc/17833/stat): 17833 (minisat+_64-bit) R 17829 17829 28974 0 -1 0 14468 0 2 0 14836 72 0 0 25 0 1 0 1851765384 54104064 12622 4294967295 134512640 135094434 3221224432 3221223024 134557512 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17833/statm): 13209 12622 145 145 0 13064 0
[pid=17833] vsize: 52836
Current children cumulated CPU time (s) 149.09
Current children cumulated vsize (Kb) 54960

[startup+160.021 s]
Raw data (loadavg): 0.99 0.97 0.73 2/57 17833
Raw data (/proc/17829/stat): 17829 (minisat+_script) S 17828 17829 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851765379 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17829/statm): 531 226 485 147 0 384 0
[pid=17829] vsize: 2124
Raw data (/proc/17833/stat): 17833 (minisat+_64-bit) R 17829 17829 28974 0 -1 0 14820 0 2 0 15831 73 0 0 25 0 1 0 1851765384 55537664 12974 4294967295 134512640 135094434 3221224432 3221223104 134555574 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17833/statm): 13559 12974 145 145 0 13414 0
[pid=17833] vsize: 54236
Current children cumulated CPU time (s) 159.05
Current children cumulated vsize (Kb) 56360

[startup+170.022 s]
Raw data (loadavg): 0.99 0.97 0.73 2/57 17833
Raw data (/proc/17829/stat): 17829 (minisat+_script) S 17828 17829 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851765379 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17829/statm): 531 226 485 147 0 384 0
[pid=17829] vsize: 2124
Raw data (/proc/17833/stat): 17833 (minisat+_64-bit) R 17829 17829 28974 0 -1 0 15192 0 2 0 16825 76 0 0 25 0 1 0 1851765384 57053184 13346 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17833/statm): 13929 13346 145 145 0 13784 0
[pid=17833] vsize: 55716
Current children cumulated CPU time (s) 169.02
Current children cumulated vsize (Kb) 57840

[startup+180.023 s]
Raw data (loadavg): 0.99 0.97 0.74 2/57 17833
Raw data (/proc/17829/stat): 17829 (minisat+_script) S 17828 17829 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851765379 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17829/statm): 531 226 485 147 0 384 0
[pid=17829] vsize: 2124
Raw data (/proc/17833/stat): 17833 (minisat+_64-bit) R 17829 17829 28974 0 -1 0 15602 0 2 0 17818 79 0 0 25 0 1 0 1851765384 58859520 13756 4294967295 134512640 135094434 3221224432 3221223056 134557612 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17833/statm): 14370 13756 145 145 0 14225 0
[pid=17833] vsize: 57480
Current children cumulated CPU time (s) 178.98
Current children cumulated vsize (Kb) 59604

[startup+190.024 s]
Raw data (loadavg): 0.99 0.97 0.74 2/57 17833
Raw data (/proc/17829/stat): 17829 (minisat+_script) S 17828 17829 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851765379 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17829/statm): 531 226 485 147 0 384 0
[pid=17829] vsize: 2124
Raw data (/proc/17833/stat): 17833 (minisat+_64-bit) R 17829 17829 28974 0 -1 0 15992 0 2 0 18811 83 0 0 25 0 1 0 1851765384 60452864 14146 4294967295 134512640 135094434 3221224432 3221223088 134558016 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17833/statm): 14759 14146 145 145 0 14614 0
[pid=17833] vsize: 59036
Current children cumulated CPU time (s) 188.95
Current children cumulated vsize (Kb) 61160

[startup+200.025 s]
Raw data (loadavg): 0.99 0.97 0.74 2/57 17833
Raw data (/proc/17829/stat): 17829 (minisat+_script) S 17828 17829 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851765379 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17829/statm): 531 226 485 147 0 384 0
[pid=17829] vsize: 2124
Raw data (/proc/17833/stat): 17833 (minisat+_64-bit) R 17829 17829 28974 0 -1 0 16382 0 2 0 19803 85 0 0 25 0 1 0 1851765384 62042112 14536 4294967295 134512640 135094434 3221224432 3221223076 134562040 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17833/statm): 15147 14536 145 145 0 15002 0
[pid=17833] vsize: 60588
Current children cumulated CPU time (s) 198.89
Current children cumulated vsize (Kb) 62712

[startup+210.026 s]
Raw data (loadavg): 0.99 0.97 0.74 2/57 17833
Raw data (/proc/17829/stat): 17829 (minisat+_script) S 17828 17829 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851765379 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17829/statm): 531 226 485 147 0 384 0
[pid=17829] vsize: 2124
Raw data (/proc/17833/stat): 17833 (minisat+_64-bit) R 17829 17829 28974 0 -1 0 16766 0 2 0 20799 88 0 0 25 0 1 0 1851765384 62820352 14726 4294967295 134512640 135094434 3221224432 3221223088 134557859 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17833/statm): 15337 14726 145 145 0 15192 0
[pid=17833] vsize: 61348
Current children cumulated CPU time (s) 208.88
Current children cumulated vsize (Kb) 63472

[startup+220.027 s]
Raw data (loadavg): 0.99 0.97 0.74 2/57 17833
Raw data (/proc/17829/stat): 17829 (minisat+_script) S 17828 17829 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851765379 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17829/statm): 531 226 485 147 0 384 0
[pid=17829] vsize: 2124
Raw data (/proc/17833/stat): 17833 (minisat+_64-bit) R 17829 17829 28974 0 -1 0 16766 0 2 0 21799 88 0 0 25 0 1 0 1851765384 62820352 14726 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17833/statm): 15337 14726 145 145 0 15192 0
[pid=17833] vsize: 61348
Current children cumulated CPU time (s) 218.88
Current children cumulated vsize (Kb) 63472

[startup+230.028 s]
Raw data (loadavg): 0.99 0.97 0.75 2/57 17833
Raw data (/proc/17829/stat): 17829 (minisat+_script) S 17828 17829 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851765379 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17829/statm): 531 226 485 147 0 384 0
[pid=17829] vsize: 2124
Raw data (/proc/17833/stat): 17833 (minisat+_64-bit) R 17829 17829 28974 0 -1 0 16766 0 2 0 22800 88 0 0 25 0 1 0 1851765384 62820352 14726 4294967295 134512640 135094434 3221224432 3221223024 134556949 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17833/statm): 15337 14726 145 145 0 15192 0
[pid=17833] vsize: 61348
Current children cumulated CPU time (s) 228.89
Current children cumulated vsize (Kb) 63472

[startup+240.029 s]
Raw data (loadavg): 0.99 0.97 0.75 2/57 17833
Raw data (/proc/17829/stat): 17829 (minisat+_script) S 17828 17829 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851765379 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17829/statm): 531 226 485 147 0 384 0
[pid=17829] vsize: 2124
Raw data (/proc/17833/stat): 17833 (minisat+_64-bit) R 17829 17829 28974 0 -1 0 16766 0 2 0 23800 88 0 0 25 0 1 0 1851765384 62820352 14726 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17833/statm): 15337 14726 145 145 0 15192 0
[pid=17833] vsize: 61348
Current children cumulated CPU time (s) 238.89
Current children cumulated vsize (Kb) 63472

[startup+250.03 s]
Raw data (loadavg): 0.99 0.97 0.75 2/57 17833
Raw data (/proc/17829/stat): 17829 (minisat+_script) S 17828 17829 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851765379 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17829/statm): 531 226 485 147 0 384 0
[pid=17829] vsize: 2124
Raw data (/proc/17833/stat): 17833 (minisat+_64-bit) R 17829 17829 28974 0 -1 0 16766 0 2 0 24800 88 0 0 25 0 1 0 1851765384 62820352 14726 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17833/statm): 15337 14726 145 145 0 15192 0
[pid=17833] vsize: 61348
Current children cumulated CPU time (s) 248.89
Current children cumulated vsize (Kb) 63472

[startup+260.031 s]
Raw data (loadavg): 0.99 0.97 0.75 2/57 17833
Raw data (/proc/17829/stat): 17829 (minisat+_script) S 17828 17829 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851765379 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17829/statm): 531 226 485 147 0 384 0
[pid=17829] vsize: 2124
Raw data (/proc/17833/stat): 17833 (minisat+_64-bit) R 17829 17829 28974 0 -1 0 16766 0 2 0 25800 88 0 0 25 0 1 0 1851765384 62820352 14726 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17833/statm): 15337 14726 145 145 0 15192 0
[pid=17833] vsize: 61348
Current children cumulated CPU time (s) 258.89
Current children cumulated vsize (Kb) 63472

[startup+270.032 s]
Raw data (loadavg): 0.99 0.97 0.75 2/57 17833
Raw data (/proc/17829/stat): 17829 (minisat+_script) S 17828 17829 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851765379 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17829/statm): 531 226 485 147 0 384 0
[pid=17829] vsize: 2124
Raw data (/proc/17833/stat): 17833 (minisat+_64-bit) R 17829 17829 28974 0 -1 0 16766 0 2 0 26800 88 0 0 25 0 1 0 1851765384 62820352 14726 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17833/statm): 15337 14726 145 145 0 15192 0
[pid=17833] vsize: 61348
Current children cumulated CPU time (s) 268.89
Current children cumulated vsize (Kb) 63472

[startup+280.032 s]
Raw data (loadavg): 0.99 0.97 0.76 2/57 17833
Raw data (/proc/17829/stat): 17829 (minisat+_script) S 17828 17829 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851765379 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17829/statm): 531 226 485 147 0 384 0
[pid=17829] vsize: 2124
Raw data (/proc/17833/stat): 17833 (minisat+_64-bit) R 17829 17829 28974 0 -1 0 16766 0 2 0 27800 88 0 0 25 0 1 0 1851765384 62820352 14726 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17833/statm): 15337 14726 145 145 0 15192 0
[pid=17833] vsize: 61348
Current children cumulated CPU time (s) 278.89
Current children cumulated vsize (Kb) 63472

[startup+290.033 s]
Raw data (loadavg): 0.99 0.97 0.76 2/57 17833
Raw data (/proc/17829/stat): 17829 (minisat+_script) S 17828 17829 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851765379 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17829/statm): 531 226 485 147 0 384 0
[pid=17829] vsize: 2124
Raw data (/proc/17833/stat): 17833 (minisat+_64-bit) R 17829 17829 28974 0 -1 0 16766 0 2 0 28801 88 0 0 25 0 1 0 1851765384 62820352 14726 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17833/statm): 15337 14726 145 145 0 15192 0
[pid=17833] vsize: 61348
Current children cumulated CPU time (s) 288.9
Current children cumulated vsize (Kb) 63472

[startup+300.035 s]
Raw data (loadavg): 0.99 0.97 0.76 2/57 17833
Raw data (/proc/17829/stat): 17829 (minisat+_script) S 17828 17829 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851765379 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17829/statm): 531 226 485 147 0 384 0
[pid=17829] vsize: 2124
Raw data (/proc/17833/stat): 17833 (minisat+_64-bit) R 17829 17829 28974 0 -1 0 16766 0 2 0 29801 88 0 0 25 0 1 0 1851765384 62820352 14726 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17833/statm): 15337 14726 145 145 0 15192 0
[pid=17833] vsize: 61348
Current children cumulated CPU time (s) 298.9
Current children cumulated vsize (Kb) 63472

[startup+310.036 s]
Raw data (loadavg): 0.99 0.97 0.76 2/57 17833
Raw data (/proc/17829/stat): 17829 (minisat+_script) S 17828 17829 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851765379 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17829/statm): 531 226 485 147 0 384 0
[pid=17829] vsize: 2124
Raw data (/proc/17833/stat): 17833 (minisat+_64-bit) R 17829 17829 28974 0 -1 0 16766 0 2 0 30801 88 0 0 25 0 1 0 1851765384 62820352 14726 4294967295 134512640 135094434 3221224432 3221223056 134557675 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17833/statm): 15337 14726 145 145 0 15192 0
[pid=17833] vsize: 61348
Current children cumulated CPU time (s) 308.9
Current children cumulated vsize (Kb) 63472

[startup+320.037 s]
Raw data (loadavg): 0.99 0.97 0.76 2/57 17833
Raw data (/proc/17829/stat): 17829 (minisat+_script) S 17828 17829 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851765379 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17829/statm): 531 226 485 147 0 384 0
[pid=17829] vsize: 2124
Raw data (/proc/17833/stat): 17833 (minisat+_64-bit) R 17829 17829 28974 0 -1 0 16766 0 2 0 31801 88 0 0 25 0 1 0 1851765384 62820352 14726 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17833/statm): 15337 14726 145 145 0 15192 0
[pid=17833] vsize: 61348
Current children cumulated CPU time (s) 318.9
Current children cumulated vsize (Kb) 63472

[startup+330.037 s]
Raw data (loadavg): 0.99 0.97 0.77 2/57 17833
Raw data (/proc/17829/stat): 17829 (minisat+_script) S 17828 17829 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851765379 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17829/statm): 531 226 485 147 0 384 0
[pid=17829] vsize: 2124
Raw data (/proc/17833/stat): 17833 (minisat+_64-bit) R 17829 17829 28974 0 -1 0 16766 0 2 0 32801 88 0 0 25 0 1 0 1851765384 62820352 14726 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17833/statm): 15337 14726 145 145 0 15192 0
[pid=17833] vsize: 61348
Current children cumulated CPU time (s) 328.9
Current children cumulated vsize (Kb) 63472

[startup+340.037 s]
Raw data (loadavg): 0.99 0.97 0.77 2/57 17833
Raw data (/proc/17829/stat): 17829 (minisat+_script) S 17828 17829 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851765379 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17829/statm): 531 226 485 147 0 384 0
[pid=17829] vsize: 2124
Raw data (/proc/17833/stat): 17833 (minisat+_64-bit) R 17829 17829 28974 0 -1 0 17044 0 2 0 33797 91 0 0 25 0 1 0 1851765384 63959040 15004 4294967295 134512640 135094434 3221224432 3221223084 134558255 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17833/statm): 15615 15004 145 145 0 15470 0
[pid=17833] vsize: 62460
Current children cumulated CPU time (s) 338.89
Current children cumulated vsize (Kb) 64584

[startup+350.038 s]
Raw data (loadavg): 0.99 0.97 0.77 2/57 17833
Raw data (/proc/17829/stat): 17829 (minisat+_script) S 17828 17829 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851765379 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17829/statm): 531 226 485 147 0 384 0
[pid=17829] vsize: 2124
Raw data (/proc/17833/stat): 17833 (minisat+_64-bit) R 17829 17829 28974 0 -1 0 17454 0 2 0 34789 94 0 0 25 0 1 0 1851765384 65634304 15414 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17833/statm): 16024 15414 145 145 0 15879 0
[pid=17833] vsize: 64096
Current children cumulated CPU time (s) 348.84
Current children cumulated vsize (Kb) 66220

[startup+360.039 s]
Raw data (loadavg): 0.99 0.97 0.77 2/57 17833
Raw data (/proc/17829/stat): 17829 (minisat+_script) S 17828 17829 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851765379 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17829/statm): 531 226 485 147 0 384 0
[pid=17829] vsize: 2124
Raw data (/proc/17833/stat): 17833 (minisat+_64-bit) R 17829 17829 28974 0 -1 0 17823 0 2 0 35783 96 0 0 25 0 1 0 1851765384 67141632 15783 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17833/statm): 16392 15783 145 145 0 16247 0
[pid=17833] vsize: 65568
Current children cumulated CPU time (s) 358.8
Current children cumulated vsize (Kb) 67692

[startup+370.04 s]
Raw data (loadavg): 0.99 0.97 0.77 2/57 17833
Raw data (/proc/17829/stat): 17829 (minisat+_script) S 17828 17829 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851765379 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17829/statm): 531 226 485 147 0 384 0
[pid=17829] vsize: 2124
Raw data (/proc/17833/stat): 17833 (minisat+_64-bit) R 17829 17829 28974 0 -1 0 18200 0 2 0 36777 98 0 0 25 0 1 0 1851765384 68673536 16160 4294967295 134512640 135094434 3221224432 3221223088 134557928 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17833/statm): 16766 16160 145 145 0 16621 0
[pid=17833] vsize: 67064
Current children cumulated CPU time (s) 368.76
Current children cumulated vsize (Kb) 69188

[startup+380.041 s]
Raw data (loadavg): 0.99 0.97 0.78 2/57 17833
Raw data (/proc/17829/stat): 17829 (minisat+_script) S 17828 17829 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851765379 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17829/statm): 531 226 485 147 0 384 0
[pid=17829] vsize: 2124
Raw data (/proc/17833/stat): 17833 (minisat+_64-bit) R 17829 17829 28974 0 -1 0 18553 0 2 0 37772 100 0 0 25 0 1 0 1851765384 70111232 16513 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17833/statm): 17117 16513 145 145 0 16972 0
[pid=17833] vsize: 68468
Current children cumulated CPU time (s) 378.73
Current children cumulated vsize (Kb) 70592

[startup+390.041 s]
Raw data (loadavg): 0.99 0.97 0.78 2/57 17833
Raw data (/proc/17829/stat): 17829 (minisat+_script) S 17828 17829 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851765379 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17829/statm): 531 226 485 147 0 384 0
[pid=17829] vsize: 2124
Raw data (/proc/17833/stat): 17833 (minisat+_64-bit) R 17829 17829 28974 0 -1 0 18935 0 2 0 38765 104 0 0 25 0 1 0 1851765384 71671808 16895 4294967295 134512640 135094434 3221224432 3221223104 134556317 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17833/statm): 17498 16895 145 145 0 17353 0
[pid=17833] vsize: 69992
Current children cumulated CPU time (s) 388.7
Current children cumulated vsize (Kb) 72116

[startup+400.042 s]
Raw data (loadavg): 0.99 0.97 0.78 2/57 17833
Raw data (/proc/17829/stat): 17829 (minisat+_script) S 17828 17829 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851765379 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17829/statm): 531 226 485 147 0 384 0
[pid=17829] vsize: 2124
Raw data (/proc/17833/stat): 17833 (minisat+_64-bit) R 17829 17829 28974 0 -1 0 19328 0 2 0 39759 106 0 0 25 0 1 0 1851765384 73277440 17288 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17833/statm): 17890 17288 145 145 0 17745 0
[pid=17833] vsize: 71560
Current children cumulated CPU time (s) 398.66
Current children cumulated vsize (Kb) 73684

[startup+410.043 s]
Raw data (loadavg): 0.99 0.97 0.78 2/57 17833
Raw data (/proc/17829/stat): 17829 (minisat+_script) S 17828 17829 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851765379 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17829/statm): 531 226 485 147 0 384 0
[pid=17829] vsize: 2124
Raw data (/proc/17833/stat): 17833 (minisat+_64-bit) T 17829 17829 28974 0 -1 0 19748 0 2 0 40753 108 0 0 25 0 1 0 1851765384 74993664 17708 4294967295 134512640 135094434 3221224432 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/17833/statm): 18309 17708 145 145 0 18164 0
[pid=17833] vsize: 73236
Current children cumulated CPU time (s) 408.62
Current children cumulated vsize (Kb) 75360

[startup+420.044 s]
Raw data (loadavg): 0.99 0.97 0.78 2/57 17833
Raw data (/proc/17829/stat): 17829 (minisat+_script) S 17828 17829 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851765379 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17829/statm): 531 226 485 147 0 384 0
[pid=17829] vsize: 2124
Raw data (/proc/17833/stat): 17833 (minisat+_64-bit) T 17829 17829 28974 0 -1 0 20199 0 2 0 41747 111 0 0 25 0 1 0 1851765384 76836864 18159 4294967295 134512640 135094434 3221224432 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/17833/statm): 18759 18159 145 145 0 18614 0
[pid=17833] vsize: 75036
Current children cumulated CPU time (s) 418.59
Current children cumulated vsize (Kb) 77160

[startup+430.045 s]
Raw data (loadavg): 0.99 0.97 0.79 2/57 17833
Raw data (/proc/17829/stat): 17829 (minisat+_script) S 17828 17829 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851765379 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17829/statm): 531 226 485 147 0 384 0
[pid=17829] vsize: 2124
Raw data (/proc/17833/stat): 17833 (minisat+_64-bit) R 17829 17829 28974 0 -1 0 20629 0 2 0 42741 114 0 0 25 0 1 0 1851765384 78598144 18589 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17833/statm): 19189 18589 145 145 0 19044 0
[pid=17833] vsize: 76756
Current children cumulated CPU time (s) 428.56
Current children cumulated vsize (Kb) 78880

[startup+440.046 s]
Raw data (loadavg): 0.99 0.97 0.79 2/57 17833
Raw data (/proc/17829/stat): 17829 (minisat+_script) S 17828 17829 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851765379 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17829/statm): 531 226 485 147 0 384 0
[pid=17829] vsize: 2124
Raw data (/proc/17833/stat): 17833 (minisat+_64-bit) R 17829 17829 28974 0 -1 0 21063 0 2 0 43733 117 0 0 25 0 1 0 1851765384 80367616 19023 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17833/statm): 19621 19023 145 145 0 19476 0
[pid=17833] vsize: 78484
Current children cumulated CPU time (s) 438.51
Current children cumulated vsize (Kb) 80608

[startup+450.046 s]
Raw data (loadavg): 0.99 0.97 0.79 2/57 17833
Raw data (/proc/17829/stat): 17829 (minisat+_script) S 17828 17829 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851765379 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17829/statm): 531 226 485 147 0 384 0
[pid=17829] vsize: 2124
Raw data (/proc/17833/stat): 17833 (minisat+_64-bit) R 17829 17829 28974 0 -1 0 21461 0 2 0 44726 119 0 0 25 0 1 0 1851765384 81997824 19421 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17833/statm): 20019 19421 145 145 0 19874 0
[pid=17833] vsize: 80076
Current children cumulated CPU time (s) 448.46
Current children cumulated vsize (Kb) 82200

[startup+460.047 s]
Raw data (loadavg): 0.99 0.97 0.79 2/57 17833
Raw data (/proc/17829/stat): 17829 (minisat+_script) S 17828 17829 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851765379 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17829/statm): 531 226 485 147 0 384 0
[pid=17829] vsize: 2124
Raw data (/proc/17833/stat): 17833 (minisat+_64-bit) R 17829 17829 28974 0 -1 0 21755 0 2 0 45720 122 0 0 25 0 1 0 1851765384 83197952 19715 4294967295 134512640 135094434 3221224432 3221223024 134556802 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17833/statm): 20312 19715 145 145 0 20167 0
[pid=17833] vsize: 81248
Current children cumulated CPU time (s) 458.43
Current children cumulated vsize (Kb) 83372

[startup+470.048 s]
Raw data (loadavg): 0.99 0.97 0.79 2/57 17833
Raw data (/proc/17829/stat): 17829 (minisat+_script) S 17828 17829 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851765379 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17829/statm): 531 226 485 147 0 384 0
[pid=17829] vsize: 2124
Raw data (/proc/17833/stat): 17833 (minisat+_64-bit) R 17829 17829 28974 0 -1 0 22082 0 2 0 46715 125 0 0 25 0 1 0 1851765384 84533248 20042 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17833/statm): 20638 20042 145 145 0 20493 0
[pid=17833] vsize: 82552
Current children cumulated CPU time (s) 468.41
Current children cumulated vsize (Kb) 84676

[startup+480.049 s]
Raw data (loadavg): 0.99 0.97 0.79 2/57 17833
Raw data (/proc/17829/stat): 17829 (minisat+_script) S 17828 17829 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851765379 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17829/statm): 531 226 485 147 0 384 0
[pid=17829] vsize: 2124
Raw data (/proc/17833/stat): 17833 (minisat+_64-bit) R 17829 17829 28974 0 -1 0 22414 0 2 0 47709 127 0 0 25 0 1 0 1851765384 85889024 20374 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17833/statm): 20969 20374 145 145 0 20824 0
[pid=17833] vsize: 83876
Current children cumulated CPU time (s) 478.37
Current children cumulated vsize (Kb) 86000

[startup+490.05 s]
Raw data (loadavg): 0.99 0.97 0.80 2/57 17833
Raw data (/proc/17829/stat): 17829 (minisat+_script) S 17828 17829 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851765379 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17829/statm): 531 226 485 147 0 384 0
[pid=17829] vsize: 2124
Raw data (/proc/17833/stat): 17833 (minisat+_64-bit) R 17829 17829 28974 0 -1 0 22751 0 2 0 48702 130 0 0 25 0 1 0 1851765384 87265280 20711 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17833/statm): 21305 20711 145 145 0 21160 0
[pid=17833] vsize: 85220
Current children cumulated CPU time (s) 488.33
Current children cumulated vsize (Kb) 87344

[startup+500.051 s]
Raw data (loadavg): 0.99 0.97 0.80 2/57 17833
Raw data (/proc/17829/stat): 17829 (minisat+_script) S 17828 17829 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851765379 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17829/statm): 531 226 485 147 0 384 0
[pid=17829] vsize: 2124
Raw data (/proc/17833/stat): 17833 (minisat+_64-bit) R 17829 17829 28974 0 -1 0 23037 0 2 0 49697 132 0 0 25 0 1 0 1851765384 88428544 20997 4294967295 134512640 135094434 3221224432 3221223088 134558235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17833/statm): 21589 20997 145 145 0 21444 0
[pid=17833] vsize: 86356
Current children cumulated CPU time (s) 498.3
Current children cumulated vsize (Kb) 88480

[startup+510.052 s]
Raw data (loadavg): 0.99 0.97 0.80 2/57 17833
Raw data (/proc/17829/stat): 17829 (minisat+_script) S 17828 17829 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851765379 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17829/statm): 531 226 485 147 0 384 0
[pid=17829] vsize: 2124
Raw data (/proc/17833/stat): 17833 (minisat+_64-bit) R 17829 17829 28974 0 -1 0 23358 0 2 0 50689 136 0 0 25 0 1 0 1851765384 89739264 21318 4294967295 134512640 135094434 3221224432 3221223088 134558029 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17833/statm): 21909 21318 145 145 0 21764 0
[pid=17833] vsize: 87636
Current children cumulated CPU time (s) 508.26
Current children cumulated vsize (Kb) 89760

[startup+520.053 s]
Raw data (loadavg): 0.99 0.97 0.80 2/57 17833
Raw data (/proc/17829/stat): 17829 (minisat+_script) S 17828 17829 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851765379 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17829/statm): 531 226 485 147 0 384 0
[pid=17829] vsize: 2124
Raw data (/proc/17833/stat): 17833 (minisat+_64-bit) R 17829 17829 28974 0 -1 0 23734 0 2 0 51684 137 0 0 25 0 1 0 1851765384 91271168 21694 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17833/statm): 22283 21694 145 145 0 22138 0
[pid=17833] vsize: 89132
Current children cumulated CPU time (s) 518.22
Current children cumulated vsize (Kb) 91256

[startup+530.054 s]
Raw data (loadavg): 0.99 0.97 0.80 2/57 17833
Raw data (/proc/17829/stat): 17829 (minisat+_script) S 17828 17829 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851765379 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17829/statm): 531 226 485 147 0 384 0
[pid=17829] vsize: 2124
Raw data (/proc/17833/stat): 17833 (minisat+_64-bit) R 17829 17829 28974 0 -1 0 24089 0 2 0 52679 139 0 0 25 0 1 0 1851765384 92725248 22049 4294967295 134512640 135094434 3221224432 3221223088 134558174 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17833/statm): 22638 22049 145 145 0 22493 0
[pid=17833] vsize: 90552
Current children cumulated CPU time (s) 528.19
Current children cumulated vsize (Kb) 92676

[startup+540.055 s]
Raw data (loadavg): 0.99 0.97 0.81 2/57 17833
Raw data (/proc/17829/stat): 17829 (minisat+_script) S 17828 17829 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851765379 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17829/statm): 531 226 485 147 0 384 0
[pid=17829] vsize: 2124
Raw data (/proc/17833/stat): 17833 (minisat+_64-bit) R 17829 17829 28974 0 -1 0 24422 0 2 0 53674 142 0 0 25 0 1 0 1851765384 94081024 22382 4294967295 134512640 135094434 3221224432 3221223088 134557937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17833/statm): 22969 22382 145 145 0 22824 0
[pid=17833] vsize: 91876
Current children cumulated CPU time (s) 538.17
Current children cumulated vsize (Kb) 94000

[startup+550.056 s]
Raw data (loadavg): 0.99 0.97 0.81 2/57 17833
Raw data (/proc/17829/stat): 17829 (minisat+_script) S 17828 17829 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851765379 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17829/statm): 531 226 485 147 0 384 0
[pid=17829] vsize: 2124
Raw data (/proc/17833/stat): 17833 (minisat+_64-bit) R 17829 17829 28974 0 -1 0 24744 0 2 0 54668 144 0 0 25 0 1 0 1851765384 95395840 22704 4294967295 134512640 135094434 3221224432 3221223120 134554793 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17833/statm): 23290 22704 145 145 0 23145 0
[pid=17833] vsize: 93160
Current children cumulated CPU time (s) 548.13
Current children cumulated vsize (Kb) 95284

[startup+560.056 s]
Raw data (loadavg): 0.99 0.97 0.81 2/57 17833
Raw data (/proc/17829/stat): 17829 (minisat+_script) S 17828 17829 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851765379 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17829/statm): 531 226 485 147 0 384 0
[pid=17829] vsize: 2124
Raw data (/proc/17833/stat): 17833 (minisat+_64-bit) R 17829 17829 28974 0 -1 0 25070 0 2 0 55662 146 0 0 25 0 1 0 1851765384 96727040 23030 4294967295 134512640 135094434 3221224432 3221223024 134556793 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17833/statm): 23615 23030 145 145 0 23470 0
[pid=17833] vsize: 94460
Current children cumulated CPU time (s) 558.09
Current children cumulated vsize (Kb) 96584

[startup+570.057 s]
Raw data (loadavg): 0.99 0.97 0.81 2/57 17833
Raw data (/proc/17829/stat): 17829 (minisat+_script) S 17828 17829 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851765379 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17829/statm): 531 226 485 147 0 384 0
[pid=17829] vsize: 2124
Raw data (/proc/17833/stat): 17833 (minisat+_64-bit) R 17829 17829 28974 0 -1 0 25393 0 2 0 56657 149 0 0 25 0 1 0 1851765384 98041856 23353 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17833/statm): 23936 23353 145 145 0 23791 0
[pid=17833] vsize: 95744
Current children cumulated CPU time (s) 568.07
Current children cumulated vsize (Kb) 97868

[startup+580.058 s]
Raw data (loadavg): 0.99 0.97 0.81 2/57 17833
Raw data (/proc/17829/stat): 17829 (minisat+_script) S 17828 17829 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851765379 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17829/statm): 531 226 485 147 0 384 0
[pid=17829] vsize: 2124
Raw data (/proc/17833/stat): 17833 (minisat+_64-bit) R 17829 17829 28974 0 -1 0 25709 0 2 0 57652 151 0 0 25 0 1 0 1851765384 99332096 23669 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17833/statm): 24251 23669 145 145 0 24106 0
[pid=17833] vsize: 97004
Current children cumulated CPU time (s) 578.04
Current children cumulated vsize (Kb) 99128

[startup+590.059 s]
Raw data (loadavg): 0.99 0.97 0.82 2/57 17833
Raw data (/proc/17829/stat): 17829 (minisat+_script) S 17828 17829 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851765379 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17829/statm): 531 226 485 147 0 384 0
[pid=17829] vsize: 2124
Raw data (/proc/17833/stat): 17833 (minisat+_64-bit) R 17829 17829 28974 0 -1 0 26063 0 2 0 58647 153 0 0 25 0 1 0 1851765384 101040128 24023 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17833/statm): 24668 24023 145 145 0 24523 0
[pid=17833] vsize: 98672
Current children cumulated CPU time (s) 588.01
Current children cumulated vsize (Kb) 100796

[startup+600.06 s]
Raw data (loadavg): 0.99 0.97 0.82 2/57 17833
Raw data (/proc/17829/stat): 17829 (minisat+_script) S 17828 17829 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851765379 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17829/statm): 531 226 485 147 0 384 0
[pid=17829] vsize: 2124
Raw data (/proc/17833/stat): 17833 (minisat+_64-bit) R 17829 17829 28974 0 -1 0 26356 0 2 0 59641 155 0 0 25 0 1 0 1851765384 102236160 24316 4294967295 134512640 135094434 3221224432 3221223088 134558281 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17833/statm): 24960 24316 145 145 0 24815 0
[pid=17833] vsize: 99840
Current children cumulated CPU time (s) 597.97
Current children cumulated vsize (Kb) 101964

[startup+610.061 s]
Raw data (loadavg): 0.99 0.97 0.82 2/57 17833
Raw data (/proc/17829/stat): 17829 (minisat+_script) S 17828 17829 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851765379 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17829/statm): 531 226 485 147 0 384 0
[pid=17829] vsize: 2124
Raw data (/proc/17833/stat): 17833 (minisat+_64-bit) R 17829 17829 28974 0 -1 0 26704 0 2 0 60637 157 0 0 25 0 1 0 1851765384 103657472 24664 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17833/statm): 25307 24664 145 145 0 25162 0
[pid=17833] vsize: 101228
Current children cumulated CPU time (s) 607.95
Current children cumulated vsize (Kb) 103352

[startup+620.062 s]
Raw data (loadavg): 0.99 0.97 0.82 2/57 17833
Raw data (/proc/17829/stat): 17829 (minisat+_script) S 17828 17829 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851765379 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17829/statm): 531 226 485 147 0 384 0
[pid=17829] vsize: 2124
Raw data (/proc/17833/stat): 17833 (minisat+_64-bit) R 17829 17829 28974 0 -1 0 27021 0 2 0 61632 160 0 0 25 0 1 0 1851765384 104951808 24981 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17833/statm): 25623 24981 145 145 0 25478 0
[pid=17833] vsize: 102492
Current children cumulated CPU time (s) 617.93
Current children cumulated vsize (Kb) 104616

[startup+630.063 s]
Raw data (loadavg): 0.99 0.97 0.82 2/57 17833
Raw data (/proc/17829/stat): 17829 (minisat+_script) S 17828 17829 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851765379 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17829/statm): 531 226 485 147 0 384 0
[pid=17829] vsize: 2124
Raw data (/proc/17833/stat): 17833 (minisat+_64-bit) R 17829 17829 28974 0 -1 0 27331 0 2 0 62626 163 0 0 25 0 1 0 1851765384 106213376 25291 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17833/statm): 25931 25291 145 145 0 25786 0
[pid=17833] vsize: 103724
Current children cumulated CPU time (s) 627.9
Current children cumulated vsize (Kb) 105848

[startup+640.064 s]
Raw data (loadavg): 0.99 0.97 0.82 2/57 17833
Raw data (/proc/17829/stat): 17829 (minisat+_script) S 17828 17829 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851765379 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17829/statm): 531 226 485 147 0 384 0
[pid=17829] vsize: 2124
Raw data (/proc/17833/stat): 17833 (minisat+_64-bit) R 17829 17829 28974 0 -1 0 27716 0 2 0 63621 165 0 0 25 0 1 0 1851765384 107786240 25676 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17833/statm): 26315 25676 145 145 0 26170 0
[pid=17833] vsize: 105260
Current children cumulated CPU time (s) 637.87
Current children cumulated vsize (Kb) 107384

[startup+650.065 s]
Raw data (loadavg): 0.99 0.97 0.82 2/57 17833
Raw data (/proc/17829/stat): 17829 (minisat+_script) S 17828 17829 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851765379 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17829/statm): 531 226 485 147 0 384 0
[pid=17829] vsize: 2124
Raw data (/proc/17833/stat): 17833 (minisat+_64-bit) R 17829 17829 28974 0 -1 0 28076 0 2 0 64616 168 0 0 25 0 1 0 1851765384 109256704 26036 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17833/statm): 26674 26036 145 145 0 26529 0
[pid=17833] vsize: 106696
Current children cumulated CPU time (s) 647.85
Current children cumulated vsize (Kb) 108820

[startup+660.066 s]
Raw data (loadavg): 0.99 0.97 0.82 2/57 17833
Raw data (/proc/17829/stat): 17829 (minisat+_script) S 17828 17829 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851765379 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17829/statm): 531 226 485 147 0 384 0
[pid=17829] vsize: 2124
Raw data (/proc/17833/stat): 17833 (minisat+_64-bit) R 17829 17829 28974 0 -1 0 28407 0 2 0 65611 170 0 0 25 0 1 0 1851765384 110608384 26367 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17833/statm): 27004 26367 145 145 0 26859 0
[pid=17833] vsize: 108016
Current children cumulated CPU time (s) 657.82
Current children cumulated vsize (Kb) 110140

[startup+670.067 s]
Raw data (loadavg): 0.99 0.97 0.83 2/57 17833
Raw data (/proc/17829/stat): 17829 (minisat+_script) S 17828 17829 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851765379 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17829/statm): 531 226 485 147 0 384 0
[pid=17829] vsize: 2124
Raw data (/proc/17833/stat): 17833 (minisat+_64-bit) R 17829 17829 28974 0 -1 0 28808 0 2 0 66605 172 0 0 25 0 1 0 1851765384 112246784 26768 4294967295 134512640 135094434 3221224432 3221223104 134556543 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17833/statm): 27404 26768 145 145 0 27259 0
[pid=17833] vsize: 109616
Current children cumulated CPU time (s) 667.78
Current children cumulated vsize (Kb) 111740

[startup+680.068 s]
Raw data (loadavg): 0.99 0.97 0.83 2/57 17833
Raw data (/proc/17829/stat): 17829 (minisat+_script) S 17828 17829 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851765379 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17829/statm): 531 226 485 147 0 384 0
[pid=17829] vsize: 2124
Raw data (/proc/17833/stat): 17833 (minisat+_64-bit) R 17829 17829 28974 0 -1 0 29151 0 2 0 67600 175 0 0 25 0 1 0 1851765384 113647616 27111 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17833/statm): 27746 27111 145 145 0 27601 0
[pid=17833] vsize: 110984
Current children cumulated CPU time (s) 677.76
Current children cumulated vsize (Kb) 113108

[startup+690.068 s]
Raw data (loadavg): 0.99 0.97 0.83 2/57 17833
Raw data (/proc/17829/stat): 17829 (minisat+_script) S 17828 17829 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851765379 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17829/statm): 531 226 485 147 0 384 0
[pid=17829] vsize: 2124
Raw data (/proc/17833/stat): 17833 (minisat+_64-bit) R 17829 17829 28974 0 -1 0 29487 0 2 0 68595 178 0 0 25 0 1 0 1851765384 115019776 27447 4294967295 134512640 135094434 3221224432 3221223088 134558187 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17833/statm): 28081 27447 145 145 0 27936 0
[pid=17833] vsize: 112324
Current children cumulated CPU time (s) 687.74
Current children cumulated vsize (Kb) 114448

[startup+700.069 s]
Raw data (loadavg): 0.99 0.97 0.83 1/57 17833
Raw data (/proc/17829/stat): 17829 (minisat+_script) S 17828 17829 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851765379 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17829/statm): 531 226 485 147 0 384 0
[pid=17829] vsize: 2124
Raw data (/proc/17833/stat): 17833 (minisat+_64-bit) T 17829 17829 28974 0 -1 0 29852 0 2 0 69590 180 0 0 25 0 1 0 1851765384 116510720 27812 4294967295 134512640 135094434 3221224432 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/17833/statm): 28445 27812 145 145 0 28300 0
[pid=17833] vsize: 113780
Current children cumulated CPU time (s) 697.71
Current children cumulated vsize (Kb) 115904

[startup+710.07 s]
Raw data (loadavg): 0.99 0.97 0.83 2/57 17833
Raw data (/proc/17829/stat): 17829 (minisat+_script) S 17828 17829 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851765379 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17829/statm): 531 226 485 147 0 384 0
[pid=17829] vsize: 2124
Raw data (/proc/17833/stat): 17833 (minisat+_64-bit) R 17829 17829 28974 0 -1 0 30212 0 2 0 70586 182 0 0 25 0 1 0 1851765384 117981184 28172 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17833/statm): 28804 28172 145 145 0 28659 0
[pid=17833] vsize: 115216
Current children cumulated CPU time (s) 707.69
Current children cumulated vsize (Kb) 117340

[startup+720.071 s]
Raw data (loadavg): 0.99 0.97 0.83 2/57 17833
Raw data (/proc/17829/stat): 17829 (minisat+_script) S 17828 17829 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851765379 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17829/statm): 531 226 485 147 0 384 0
[pid=17829] vsize: 2124
Raw data (/proc/17833/stat): 17833 (minisat+_64-bit) R 17829 17829 28974 0 -1 0 30590 0 2 0 71580 184 0 0 25 0 1 0 1851765384 119525376 28550 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17833/statm): 29181 28550 145 145 0 29036 0
[pid=17833] vsize: 116724
Current children cumulated CPU time (s) 717.65
Current children cumulated vsize (Kb) 118848

[startup+730.071 s]
Raw data (loadavg): 0.99 0.97 0.83 2/57 17833
Raw data (/proc/17829/stat): 17829 (minisat+_script) S 17828 17829 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851765379 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17829/statm): 531 226 485 147 0 384 0
[pid=17829] vsize: 2124
Raw data (/proc/17833/stat): 17833 (minisat+_64-bit) R 17829 17829 28974 0 -1 0 30897 0 2 0 72576 186 0 0 25 0 1 0 1851765384 119996416 28666 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17833/statm): 29296 28666 145 145 0 29151 0
[pid=17833] vsize: 117184
Current children cumulated CPU time (s) 727.63
Current children cumulated vsize (Kb) 119308

[startup+740.072 s]
Raw data (loadavg): 0.99 0.97 0.83 2/57 17833
Raw data (/proc/17829/stat): 17829 (minisat+_script) S 17828 17829 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851765379 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17829/statm): 531 226 485 147 0 384 0
[pid=17829] vsize: 2124
Raw data (/proc/17833/stat): 17833 (minisat+_64-bit) R 17829 17829 28974 0 -1 0 30897 0 2 0 73577 186 0 0 25 0 1 0 1851765384 119996416 28666 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17833/statm): 29296 28666 145 145 0 29151 0
[pid=17833] vsize: 117184
Current children cumulated CPU time (s) 737.64
Current children cumulated vsize (Kb) 119308

[startup+750.073 s]
Raw data (loadavg): 0.99 0.97 0.83 2/57 17833
Raw data (/proc/17829/stat): 17829 (minisat+_script) S 17828 17829 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851765379 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17829/statm): 531 226 485 147 0 384 0
[pid=17829] vsize: 2124
Raw data (/proc/17833/stat): 17833 (minisat+_64-bit) R 17829 17829 28974 0 -1 0 30897 0 2 0 74577 186 0 0 25 0 1 0 1851765384 119996416 28666 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17833/statm): 29296 28666 145 145 0 29151 0
[pid=17833] vsize: 117184
Current children cumulated CPU time (s) 747.64
Current children cumulated vsize (Kb) 119308

[startup+760.074 s]
Raw data (loadavg): 0.99 0.97 0.83 2/57 17833
Raw data (/proc/17829/stat): 17829 (minisat+_script) S 17828 17829 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851765379 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17829/statm): 531 226 485 147 0 384 0
[pid=17829] vsize: 2124
Raw data (/proc/17833/stat): 17833 (minisat+_64-bit) R 17829 17829 28974 0 -1 0 30897 0 2 0 75577 186 0 0 25 0 1 0 1851765384 119996416 28666 4294967295 134512640 135094434 3221224432 3221223120 134554788 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17833/statm): 29296 28666 145 145 0 29151 0
[pid=17833] vsize: 117184
Current children cumulated CPU time (s) 757.64
Current children cumulated vsize (Kb) 119308

[startup+770.075 s]
Raw data (loadavg): 0.99 0.97 0.83 2/57 17833
Raw data (/proc/17829/stat): 17829 (minisat+_script) S 17828 17829 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851765379 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17829/statm): 531 226 485 147 0 384 0
[pid=17829] vsize: 2124
Raw data (/proc/17833/stat): 17833 (minisat+_64-bit) R 17829 17829 28974 0 -1 0 30897 0 2 0 76577 187 0 0 25 0 1 0 1851765384 119996416 28666 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17833/statm): 29296 28666 145 145 0 29151 0
[pid=17833] vsize: 117184
Current children cumulated CPU time (s) 767.65
Current children cumulated vsize (Kb) 119308

[startup+780.076 s]
Raw data (loadavg): 0.99 0.97 0.84 2/57 17833
Raw data (/proc/17829/stat): 17829 (minisat+_script) S 17828 17829 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851765379 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17829/statm): 531 226 485 147 0 384 0
[pid=17829] vsize: 2124
Raw data (/proc/17833/stat): 17833 (minisat+_64-bit) R 17829 17829 28974 0 -1 0 30897 0 2 0 77577 187 0 0 25 0 1 0 1851765384 119996416 28666 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17833/statm): 29296 28666 145 145 0 29151 0
[pid=17833] vsize: 117184
Current children cumulated CPU time (s) 777.65
Current children cumulated vsize (Kb) 119308

[startup+790.076 s]
Raw data (loadavg): 0.99 0.97 0.84 2/57 17833
Raw data (/proc/17829/stat): 17829 (minisat+_script) S 17828 17829 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851765379 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17829/statm): 531 226 485 147 0 384 0
[pid=17829] vsize: 2124
Raw data (/proc/17833/stat): 17833 (minisat+_64-bit) R 17829 17829 28974 0 -1 0 30897 0 2 0 78577 187 0 0 25 0 1 0 1851765384 119996416 28666 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17833/statm): 29296 28666 145 145 0 29151 0
[pid=17833] vsize: 117184
Current children cumulated CPU time (s) 787.65
Current children cumulated vsize (Kb) 119308

[startup+800.077 s]
Raw data (loadavg): 0.99 0.97 0.84 2/57 17833
Raw data (/proc/17829/stat): 17829 (minisat+_script) S 17828 17829 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851765379 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17829/statm): 531 226 485 147 0 384 0
[pid=17829] vsize: 2124
Raw data (/proc/17833/stat): 17833 (minisat+_64-bit) R 17829 17829 28974 0 -1 0 30897 0 2 0 79578 187 0 0 25 0 1 0 1851765384 119996416 28666 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17833/statm): 29296 28666 145 145 0 29151 0
[pid=17833] vsize: 117184
Current children cumulated CPU time (s) 797.66
Current children cumulated vsize (Kb) 119308

[startup+810.078 s]
Raw data (loadavg): 0.99 0.97 0.84 2/57 17833
Raw data (/proc/17829/stat): 17829 (minisat+_script) S 17828 17829 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851765379 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17829/statm): 531 226 485 147 0 384 0
[pid=17829] vsize: 2124
Raw data (/proc/17833/stat): 17833 (minisat+_64-bit) R 17829 17829 28974 0 -1 0 30897 0 2 0 80578 187 0 0 25 0 1 0 1851765384 119996416 28666 4294967295 134512640 135094434 3221224432 3221223024 134556789 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17833/statm): 29296 28666 145 145 0 29151 0
[pid=17833] vsize: 117184
Current children cumulated CPU time (s) 807.66
Current children cumulated vsize (Kb) 119308

[startup+820.079 s]
Raw data (loadavg): 0.99 0.97 0.84 2/57 17833
Raw data (/proc/17829/stat): 17829 (minisat+_script) S 17828 17829 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851765379 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17829/statm): 531 226 485 147 0 384 0
[pid=17829] vsize: 2124
Raw data (/proc/17833/stat): 17833 (minisat+_64-bit) R 17829 17829 28974 0 -1 0 30897 0 2 0 81578 187 0 0 25 0 1 0 1851765384 119996416 28666 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17833/statm): 29296 28666 145 145 0 29151 0
[pid=17833] vsize: 117184
Current children cumulated CPU time (s) 817.66
Current children cumulated vsize (Kb) 119308

[startup+830.08 s]
Raw data (loadavg): 0.99 0.97 0.84 2/57 17833
Raw data (/proc/17829/stat): 17829 (minisat+_script) S 17828 17829 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851765379 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17829/statm): 531 226 485 147 0 384 0
[pid=17829] vsize: 2124
Raw data (/proc/17833/stat): 17833 (minisat+_64-bit) R 17829 17829 28974 0 -1 0 30897 0 2 0 82578 187 0 0 25 0 1 0 1851765384 119996416 28666 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17833/statm): 29296 28666 145 145 0 29151 0
[pid=17833] vsize: 117184
Current children cumulated CPU time (s) 827.66
Current children cumulated vsize (Kb) 119308

[startup+840.08 s]
Raw data (loadavg): 0.99 0.97 0.84 2/57 17833
Raw data (/proc/17829/stat): 17829 (minisat+_script) S 17828 17829 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851765379 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17829/statm): 531 226 485 147 0 384 0
[pid=17829] vsize: 2124
Raw data (/proc/17833/stat): 17833 (minisat+_64-bit) R 17829 17829 28974 0 -1 0 30897 0 2 0 83578 187 0 0 25 0 1 0 1851765384 119996416 28666 4294967295 134512640 135094434 3221224432 3221223024 134557514 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17833/statm): 29296 28666 145 145 0 29151 0
[pid=17833] vsize: 117184
Current children cumulated CPU time (s) 837.66
Current children cumulated vsize (Kb) 119308

[startup+850.081 s]
Raw data (loadavg): 0.99 0.97 0.84 2/57 17833
Raw data (/proc/17829/stat): 17829 (minisat+_script) S 17828 17829 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851765379 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17829/statm): 531 226 485 147 0 384 0
[pid=17829] vsize: 2124
Raw data (/proc/17833/stat): 17833 (minisat+_64-bit) R 17829 17829 28974 0 -1 0 30897 0 2 0 84578 187 0 0 25 0 1 0 1851765384 119996416 28666 4294967295 134512640 135094434 3221224432 3221223088 134558007 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17833/statm): 29296 28666 145 145 0 29151 0
[pid=17833] vsize: 117184
Current children cumulated CPU time (s) 847.66
Current children cumulated vsize (Kb) 119308

[startup+860.082 s]
Raw data (loadavg): 0.99 0.97 0.84 2/57 17833
Raw data (/proc/17829/stat): 17829 (minisat+_script) S 17828 17829 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851765379 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17829/statm): 531 226 485 147 0 384 0
[pid=17829] vsize: 2124
Raw data (/proc/17833/stat): 17833 (minisat+_64-bit) R 17829 17829 28974 0 -1 0 30897 0 2 0 85578 187 0 0 25 0 1 0 1851765384 119996416 28666 4294967295 134512640 135094434 3221224432 3221223024 134557537 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17833/statm): 29296 28666 145 145 0 29151 0
[pid=17833] vsize: 117184
Current children cumulated CPU time (s) 857.66
Current children cumulated vsize (Kb) 119308

[startup+870.083 s]
Raw data (loadavg): 0.99 0.97 0.84 2/57 17833
Raw data (/proc/17829/stat): 17829 (minisat+_script) S 17828 17829 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851765379 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17829/statm): 531 226 485 147 0 384 0
[pid=17829] vsize: 2124
Raw data (/proc/17833/stat): 17833 (minisat+_64-bit) R 17829 17829 28974 0 -1 0 30897 0 2 0 86579 187 0 0 25 0 1 0 1851765384 119996416 28666 4294967295 134512640 135094434 3221224432 3221223024 134557236 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17833/statm): 29296 28666 145 145 0 29151 0
[pid=17833] vsize: 117184
Current children cumulated CPU time (s) 867.67
Current children cumulated vsize (Kb) 119308

[startup+880.084 s]
Raw data (loadavg): 0.99 0.97 0.85 2/57 17833
Raw data (/proc/17829/stat): 17829 (minisat+_script) S 17828 17829 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851765379 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17829/statm): 531 226 485 147 0 384 0
[pid=17829] vsize: 2124
Raw data (/proc/17833/stat): 17833 (minisat+_64-bit) R 17829 17829 28974 0 -1 0 30897 0 2 0 87579 187 0 0 25 0 1 0 1851765384 119996416 28666 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17833/statm): 29296 28666 145 145 0 29151 0
[pid=17833] vsize: 117184
Current children cumulated CPU time (s) 877.67
Current children cumulated vsize (Kb) 119308

[startup+890.085 s]
Raw data (loadavg): 0.99 0.97 0.85 2/57 17833
Raw data (/proc/17829/stat): 17829 (minisat+_script) S 17828 17829 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851765379 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17829/statm): 531 226 485 147 0 384 0
[pid=17829] vsize: 2124
Raw data (/proc/17833/stat): 17833 (minisat+_64-bit) R 17829 17829 28974 0 -1 0 30897 0 2 0 88579 187 0 0 25 0 1 0 1851765384 119996416 28666 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17833/statm): 29296 28666 145 145 0 29151 0
[pid=17833] vsize: 117184
Current children cumulated CPU time (s) 887.67
Current children cumulated vsize (Kb) 119308

[startup+900.085 s]
Raw data (loadavg): 0.99 0.97 0.85 2/57 17833
Raw data (/proc/17829/stat): 17829 (minisat+_script) S 17828 17829 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851765379 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17829/statm): 531 226 485 147 0 384 0
[pid=17829] vsize: 2124
Raw data (/proc/17833/stat): 17833 (minisat+_64-bit) R 17829 17829 28974 0 -1 0 30897 0 2 0 89579 188 0 0 25 0 1 0 1851765384 119996416 28666 4294967295 134512640 135094434 3221224432 3221223024 134557334 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17833/statm): 29296 28666 145 145 0 29151 0
[pid=17833] vsize: 117184
Current children cumulated CPU time (s) 897.68
Current children cumulated vsize (Kb) 119308

[startup+910.086 s]
Raw data (loadavg): 0.99 0.97 0.85 2/57 17833
Raw data (/proc/17829/stat): 17829 (minisat+_script) S 17828 17829 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851765379 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17829/statm): 531 226 485 147 0 384 0
[pid=17829] vsize: 2124
Raw data (/proc/17833/stat): 17833 (minisat+_64-bit) R 17829 17829 28974 0 -1 0 30897 0 2 0 90579 188 0 0 25 0 1 0 1851765384 119996416 28666 4294967295 134512640 135094434 3221224432 3221223088 134557840 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17833/statm): 29296 28666 145 145 0 29151 0
[pid=17833] vsize: 117184
Current children cumulated CPU time (s) 907.68
Current children cumulated vsize (Kb) 119308

[startup+920.088 s]
Raw data (loadavg): 0.99 0.97 0.85 2/57 17833
Raw data (/proc/17829/stat): 17829 (minisat+_script) S 17828 17829 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851765379 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17829/statm): 531 226 485 147 0 384 0
[pid=17829] vsize: 2124
Raw data (/proc/17833/stat): 17833 (minisat+_64-bit) R 17829 17829 28974 0 -1 0 30897 0 2 0 91580 188 0 0 25 0 1 0 1851765384 119996416 28666 4294967295 134512640 135094434 3221224432 3221223088 134557896 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17833/statm): 29296 28666 145 145 0 29151 0
[pid=17833] vsize: 117184
Current children cumulated CPU time (s) 917.69
Current children cumulated vsize (Kb) 119308

[startup+930.089 s]
Raw data (loadavg): 0.99 0.97 0.85 2/57 17833
Raw data (/proc/17829/stat): 17829 (minisat+_script) S 17828 17829 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851765379 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17829/statm): 531 226 485 147 0 384 0
[pid=17829] vsize: 2124
Raw data (/proc/17833/stat): 17833 (minisat+_64-bit) R 17829 17829 28974 0 -1 0 30897 0 2 0 92580 188 0 0 25 0 1 0 1851765384 119996416 28666 4294967295 134512640 135094434 3221224432 3221223024 134556739 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17833/statm): 29296 28666 145 145 0 29151 0
[pid=17833] vsize: 117184
Current children cumulated CPU time (s) 927.69
Current children cumulated vsize (Kb) 119308

[startup+940.089 s]
Raw data (loadavg): 0.99 0.97 0.85 2/57 17833
Raw data (/proc/17829/stat): 17829 (minisat+_script) S 17828 17829 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851765379 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17829/statm): 531 226 485 147 0 384 0
[pid=17829] vsize: 2124
Raw data (/proc/17833/stat): 17833 (minisat+_64-bit) R 17829 17829 28974 0 -1 0 30897 0 2 0 93580 188 0 0 25 0 1 0 1851765384 119996416 28666 4294967295 134512640 135094434 3221224432 3221223088 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17833/statm): 29296 28666 145 145 0 29151 0
[pid=17833] vsize: 117184
Current children cumulated CPU time (s) 937.69
Current children cumulated vsize (Kb) 119308

[startup+950.09 s]
Raw data (loadavg): 0.99 0.97 0.85 2/57 17833
Raw data (/proc/17829/stat): 17829 (minisat+_script) S 17828 17829 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851765379 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17829/statm): 531 226 485 147 0 384 0
[pid=17829] vsize: 2124
Raw data (/proc/17833/stat): 17833 (minisat+_64-bit) R 17829 17829 28974 0 -1 0 30897 0 2 0 94580 188 0 0 25 0 1 0 1851765384 119996416 28666 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17833/statm): 29296 28666 145 145 0 29151 0
[pid=17833] vsize: 117184
Current children cumulated CPU time (s) 947.69
Current children cumulated vsize (Kb) 119308

[startup+960.091 s]
Raw data (loadavg): 0.99 0.97 0.85 2/57 17833
Raw data (/proc/17829/stat): 17829 (minisat+_script) S 17828 17829 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851765379 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17829/statm): 531 226 485 147 0 384 0
[pid=17829] vsize: 2124
Raw data (/proc/17833/stat): 17833 (minisat+_64-bit) R 17829 17829 28974 0 -1 0 30897 0 2 0 95580 188 0 0 25 0 1 0 1851765384 119996416 28666 4294967295 134512640 135094434 3221224432 3221223024 134557360 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17833/statm): 29296 28666 145 145 0 29151 0
[pid=17833] vsize: 117184
Current children cumulated CPU time (s) 957.69
Current children cumulated vsize (Kb) 119308

[startup+970.092 s]
Raw data (loadavg): 0.99 0.97 0.85 2/57 17833
Raw data (/proc/17829/stat): 17829 (minisat+_script) S 17828 17829 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851765379 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17829/statm): 531 226 485 147 0 384 0
[pid=17829] vsize: 2124
Raw data (/proc/17833/stat): 17833 (minisat+_64-bit) R 17829 17829 28974 0 -1 0 30897 0 2 0 96581 188 0 0 25 0 1 0 1851765384 119996416 28666 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17833/statm): 29296 28666 145 145 0 29151 0
[pid=17833] vsize: 117184
Current children cumulated CPU time (s) 967.7
Current children cumulated vsize (Kb) 119308

[startup+980.093 s]
Raw data (loadavg): 0.99 0.97 0.86 2/57 17833
Raw data (/proc/17829/stat): 17829 (minisat+_script) S 17828 17829 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851765379 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17829/statm): 531 226 485 147 0 384 0
[pid=17829] vsize: 2124
Raw data (/proc/17833/stat): 17833 (minisat+_64-bit) R 17829 17829 28974 0 -1 0 30897 0 2 0 97581 188 0 0 25 0 1 0 1851765384 119996416 28666 4294967295 134512640 135094434 3221224432 3221223104 134555568 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17833/statm): 29296 28666 145 145 0 29151 0
[pid=17833] vsize: 117184
Current children cumulated CPU time (s) 977.7
Current children cumulated vsize (Kb) 119308

[startup+990.094 s]
Raw data (loadavg): 0.99 0.97 0.86 2/57 17833
Raw data (/proc/17829/stat): 17829 (minisat+_script) S 17828 17829 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851765379 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17829/statm): 531 226 485 147 0 384 0
[pid=17829] vsize: 2124
Raw data (/proc/17833/stat): 17833 (minisat+_64-bit) R 17829 17829 28974 0 -1 0 30897 0 2 0 98581 188 0 0 25 0 1 0 1851765384 119996416 28666 4294967295 134512640 135094434 3221224432 3221223104 134555566 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17833/statm): 29296 28666 145 145 0 29151 0
[pid=17833] vsize: 117184
Current children cumulated CPU time (s) 987.7
Current children cumulated vsize (Kb) 119308

[startup+1000.09 s]
Raw data (loadavg): 0.99 0.97 0.86 2/57 17833
Raw data (/proc/17829/stat): 17829 (minisat+_script) S 17828 17829 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851765379 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17829/statm): 531 226 485 147 0 384 0
[pid=17829] vsize: 2124
Raw data (/proc/17833/stat): 17833 (minisat+_64-bit) R 17829 17829 28974 0 -1 0 30897 0 2 0 99581 188 0 0 25 0 1 0 1851765384 119996416 28666 4294967295 134512640 135094434 3221224432 3221223084 134558255 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17833/statm): 29296 28666 145 145 0 29151 0
[pid=17833] vsize: 117184
Current children cumulated CPU time (s) 997.7
Current children cumulated vsize (Kb) 119308

[startup+1010.1 s]
Raw data (loadavg): 0.99 0.97 0.86 2/57 17833
Raw data (/proc/17829/stat): 17829 (minisat+_script) S 17828 17829 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851765379 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17829/statm): 531 226 485 147 0 384 0
[pid=17829] vsize: 2124
Raw data (/proc/17833/stat): 17833 (minisat+_64-bit) R 17829 17829 28974 0 -1 0 30897 0 2 0 100582 188 0 0 25 0 1 0 1851765384 119996416 28666 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17833/statm): 29296 28666 145 145 0 29151 0
[pid=17833] vsize: 117184
Current children cumulated CPU time (s) 1007.71
Current children cumulated vsize (Kb) 119308

[startup+1020.1 s]
Raw data (loadavg): 0.99 0.97 0.86 2/57 17833
Raw data (/proc/17829/stat): 17829 (minisat+_script) S 17828 17829 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851765379 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17829/statm): 531 226 485 147 0 384 0
[pid=17829] vsize: 2124
Raw data (/proc/17833/stat): 17833 (minisat+_64-bit) R 17829 17829 28974 0 -1 0 30897 0 2 0 101582 188 0 0 25 0 1 0 1851765384 119996416 28666 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17833/statm): 29296 28666 145 145 0 29151 0
[pid=17833] vsize: 117184
Current children cumulated CPU time (s) 1017.71
Current children cumulated vsize (Kb) 119308

[startup+1030.1 s]
Raw data (loadavg): 0.99 0.97 0.86 2/57 17833
Raw data (/proc/17829/stat): 17829 (minisat+_script) S 17828 17829 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851765379 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17829/statm): 531 226 485 147 0 384 0
[pid=17829] vsize: 2124
Raw data (/proc/17833/stat): 17833 (minisat+_64-bit) R 17829 17829 28974 0 -1 0 30897 0 2 0 102582 188 0 0 25 0 1 0 1851765384 119996416 28666 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17833/statm): 29296 28666 145 145 0 29151 0
[pid=17833] vsize: 117184
Current children cumulated CPU time (s) 1027.71
Current children cumulated vsize (Kb) 119308

[startup+1040.1 s]
Raw data (loadavg): 0.99 0.97 0.86 2/57 17833
Raw data (/proc/17829/stat): 17829 (minisat+_script) S 17828 17829 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851765379 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17829/statm): 531 226 485 147 0 384 0
[pid=17829] vsize: 2124
Raw data (/proc/17833/stat): 17833 (minisat+_64-bit) R 17829 17829 28974 0 -1 0 30897 0 2 0 103582 188 0 0 25 0 1 0 1851765384 119996416 28666 4294967295 134512640 135094434 3221224432 3221223088 134558210 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17833/statm): 29296 28666 145 145 0 29151 0
[pid=17833] vsize: 117184
Current children cumulated CPU time (s) 1037.71
Current children cumulated vsize (Kb) 119308

[startup+1050.1 s]
Raw data (loadavg): 0.99 0.97 0.86 2/57 17833
Raw data (/proc/17829/stat): 17829 (minisat+_script) S 17828 17829 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851765379 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17829/statm): 531 226 485 147 0 384 0
[pid=17829] vsize: 2124
Raw data (/proc/17833/stat): 17833 (minisat+_64-bit) R 17829 17829 28974 0 -1 0 30897 0 2 0 104583 188 0 0 25 0 1 0 1851765384 119996416 28666 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17833/statm): 29296 28666 145 145 0 29151 0
[pid=17833] vsize: 117184
Current children cumulated CPU time (s) 1047.72
Current children cumulated vsize (Kb) 119308

[startup+1060.1 s]
Raw data (loadavg): 0.99 0.97 0.86 2/57 17833
Raw data (/proc/17829/stat): 17829 (minisat+_script) S 17828 17829 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851765379 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17829/statm): 531 226 485 147 0 384 0
[pid=17829] vsize: 2124
Raw data (/proc/17833/stat): 17833 (minisat+_64-bit) R 17829 17829 28974 0 -1 0 30897 0 2 0 105583 188 0 0 25 0 1 0 1851765384 119996416 28666 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17833/statm): 29296 28666 145 145 0 29151 0
[pid=17833] vsize: 117184
Current children cumulated CPU time (s) 1057.72
Current children cumulated vsize (Kb) 119308

[startup+1070.1 s]
Raw data (loadavg): 0.99 0.97 0.86 2/57 17833
Raw data (/proc/17829/stat): 17829 (minisat+_script) S 17828 17829 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851765379 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17829/statm): 531 226 485 147 0 384 0
[pid=17829] vsize: 2124
Raw data (/proc/17833/stat): 17833 (minisat+_64-bit) R 17829 17829 28974 0 -1 0 30897 0 2 0 106583 188 0 0 25 0 1 0 1851765384 119996416 28666 4294967295 134512640 135094434 3221224432 3221223056 134557685 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17833/statm): 29296 28666 145 145 0 29151 0
[pid=17833] vsize: 117184
Current children cumulated CPU time (s) 1067.72
Current children cumulated vsize (Kb) 119308

[startup+1080.1 s]
Raw data (loadavg): 0.99 0.97 0.87 2/57 17833
Raw data (/proc/17829/stat): 17829 (minisat+_script) S 17828 17829 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851765379 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17829/statm): 531 226 485 147 0 384 0
[pid=17829] vsize: 2124
Raw data (/proc/17833/stat): 17833 (minisat+_64-bit) R 17829 17829 28974 0 -1 0 30897 0 2 0 107583 188 0 0 25 0 1 0 1851765384 119996416 28666 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17833/statm): 29296 28666 145 145 0 29151 0
[pid=17833] vsize: 117184
Current children cumulated CPU time (s) 1077.72
Current children cumulated vsize (Kb) 119308

[startup+1090.1 s]
Raw data (loadavg): 0.99 0.97 0.87 2/57 17833
Raw data (/proc/17829/stat): 17829 (minisat+_script) S 17828 17829 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851765379 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17829/statm): 531 226 485 147 0 384 0
[pid=17829] vsize: 2124
Raw data (/proc/17833/stat): 17833 (minisat+_64-bit) R 17829 17829 28974 0 -1 0 30897 0 2 0 108584 188 0 0 25 0 1 0 1851765384 119996416 28666 4294967295 134512640 135094434 3221224432 3221223024 134556866 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17833/statm): 29296 28666 145 145 0 29151 0
[pid=17833] vsize: 117184
Current children cumulated CPU time (s) 1087.73
Current children cumulated vsize (Kb) 119308

[startup+1100.1 s]
Raw data (loadavg): 0.99 0.97 0.87 2/57 17833
Raw data (/proc/17829/stat): 17829 (minisat+_script) S 17828 17829 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851765379 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17829/statm): 531 226 485 147 0 384 0
[pid=17829] vsize: 2124
Raw data (/proc/17833/stat): 17833 (minisat+_64-bit) R 17829 17829 28974 0 -1 0 30897 0 2 0 109584 188 0 0 25 0 1 0 1851765384 119996416 28666 4294967295 134512640 135094434 3221224432 3221223040 134539496 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17833/statm): 29296 28666 145 145 0 29151 0
[pid=17833] vsize: 117184
Current children cumulated CPU time (s) 1097.73
Current children cumulated vsize (Kb) 119308

[startup+1110.11 s]
Raw data (loadavg): 0.99 0.97 0.87 2/57 17833
Raw data (/proc/17829/stat): 17829 (minisat+_script) S 17828 17829 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851765379 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17829/statm): 531 226 485 147 0 384 0
[pid=17829] vsize: 2124
Raw data (/proc/17833/stat): 17833 (minisat+_64-bit) R 17829 17829 28974 0 -1 0 30897 0 2 0 110584 189 0 0 25 0 1 0 1851765384 119996416 28666 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17833/statm): 29296 28666 145 145 0 29151 0
[pid=17833] vsize: 117184
Current children cumulated CPU time (s) 1107.74
Current children cumulated vsize (Kb) 119308

[startup+1120.11 s]
Raw data (loadavg): 0.99 0.97 0.87 2/57 17833
Raw data (/proc/17829/stat): 17829 (minisat+_script) S 17828 17829 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851765379 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17829/statm): 531 226 485 147 0 384 0
[pid=17829] vsize: 2124
Raw data (/proc/17833/stat): 17833 (minisat+_64-bit) R 17829 17829 28974 0 -1 0 30897 0 2 0 111584 189 0 0 25 0 1 0 1851765384 119996416 28666 4294967295 134512640 135094434 3221224432 3221223088 134558181 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17833/statm): 29296 28666 145 145 0 29151 0
[pid=17833] vsize: 117184
Current children cumulated CPU time (s) 1117.74
Current children cumulated vsize (Kb) 119308

[startup+1130.11 s]
Raw data (loadavg): 0.99 0.97 0.87 2/57 17833
Raw data (/proc/17829/stat): 17829 (minisat+_script) S 17828 17829 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851765379 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17829/statm): 531 226 485 147 0 384 0
[pid=17829] vsize: 2124
Raw data (/proc/17833/stat): 17833 (minisat+_64-bit) R 17829 17829 28974 0 -1 0 30897 0 2 0 112584 189 0 0 25 0 1 0 1851765384 119996416 28666 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17833/statm): 29296 28666 145 145 0 29151 0
[pid=17833] vsize: 117184
Current children cumulated CPU time (s) 1127.74
Current children cumulated vsize (Kb) 119308

[startup+1140.11 s]
Raw data (loadavg): 0.99 0.97 0.87 2/57 17833
Raw data (/proc/17829/stat): 17829 (minisat+_script) S 17828 17829 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851765379 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17829/statm): 531 226 485 147 0 384 0
[pid=17829] vsize: 2124
Raw data (/proc/17833/stat): 17833 (minisat+_64-bit) R 17829 17829 28974 0 -1 0 30897 0 2 0 113585 189 0 0 25 0 1 0 1851765384 119996416 28666 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17833/statm): 29296 28666 145 145 0 29151 0
[pid=17833] vsize: 117184
Current children cumulated CPU time (s) 1137.75
Current children cumulated vsize (Kb) 119308

[startup+1150.11 s]
Raw data (loadavg): 0.99 0.97 0.87 2/57 17833
Raw data (/proc/17829/stat): 17829 (minisat+_script) S 17828 17829 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851765379 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17829/statm): 531 226 485 147 0 384 0
[pid=17829] vsize: 2124
Raw data (/proc/17833/stat): 17833 (minisat+_64-bit) R 17829 17829 28974 0 -1 0 30897 0 2 0 114585 189 0 0 25 0 1 0 1851765384 119996416 28666 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17833/statm): 29296 28666 145 145 0 29151 0
[pid=17833] vsize: 117184
Current children cumulated CPU time (s) 1147.75
Current children cumulated vsize (Kb) 119308

[startup+1160.11 s]
Raw data (loadavg): 0.99 0.97 0.87 2/57 17833
Raw data (/proc/17829/stat): 17829 (minisat+_script) S 17828 17829 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851765379 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17829/statm): 531 226 485 147 0 384 0
[pid=17829] vsize: 2124
Raw data (/proc/17833/stat): 17833 (minisat+_64-bit) R 17829 17829 28974 0 -1 0 30897 0 2 0 115585 189 0 0 25 0 1 0 1851765384 119996416 28666 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17833/statm): 29296 28666 145 145 0 29151 0
[pid=17833] vsize: 117184
Current children cumulated CPU time (s) 1157.75
Current children cumulated vsize (Kb) 119308

[startup+1170.11 s]
Raw data (loadavg): 0.99 0.97 0.87 2/57 17833
Raw data (/proc/17829/stat): 17829 (minisat+_script) S 17828 17829 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851765379 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17829/statm): 531 226 485 147 0 384 0
[pid=17829] vsize: 2124
Raw data (/proc/17833/stat): 17833 (minisat+_64-bit) R 17829 17829 28974 0 -1 0 30897 0 2 0 116585 189 0 0 25 0 1 0 1851765384 119996416 28666 4294967295 134512640 135094434 3221224432 3221223088 134558235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17833/statm): 29296 28666 145 145 0 29151 0
[pid=17833] vsize: 117184
Current children cumulated CPU time (s) 1167.75
Current children cumulated vsize (Kb) 119308

[startup+1180.11 s]
Raw data (loadavg): 0.99 0.97 0.87 2/57 17833
Raw data (/proc/17829/stat): 17829 (minisat+_script) S 17828 17829 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851765379 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17829/statm): 531 226 485 147 0 384 0
[pid=17829] vsize: 2124
Raw data (/proc/17833/stat): 17833 (minisat+_64-bit) R 17829 17829 28974 0 -1 0 31179 0 2 0 117579 191 0 0 25 0 1 0 1851765384 121151488 28948 4294967295 134512640 135094434 3221224432 3221223056 134557696 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17833/statm): 29578 28948 145 145 0 29433 0
[pid=17833] vsize: 118312
Current children cumulated CPU time (s) 1177.71
Current children cumulated vsize (Kb) 120436

[startup+1190.11 s]
Raw data (loadavg): 0.99 0.97 0.88 2/57 17833
Raw data (/proc/17829/stat): 17829 (minisat+_script) S 17828 17829 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851765379 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17829/statm): 531 226 485 147 0 384 0
[pid=17829] vsize: 2124
Raw data (/proc/17833/stat): 17833 (minisat+_64-bit) R 17829 17829 28974 0 -1 0 31493 0 2 0 118574 193 0 0 25 0 1 0 1851765384 122437632 29262 4294967295 134512640 135094434 3221224432 3221223024 134556949 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17833/statm): 29892 29262 145 145 0 29747 0
[pid=17833] vsize: 119568
Current children cumulated CPU time (s) 1187.68
Current children cumulated vsize (Kb) 121692

[startup+1200.11 s]
Raw data (loadavg): 0.99 0.97 0.88 2/57 17833
Raw data (/proc/17829/stat): 17829 (minisat+_script) S 17828 17829 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851765379 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17829/statm): 531 226 485 147 0 384 0
[pid=17829] vsize: 2124
Raw data (/proc/17833/stat): 17833 (minisat+_64-bit) R 17829 17829 28974 0 -1 0 31860 0 2 0 119568 195 0 0 25 0 1 0 1851765384 123940864 29629 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17833/statm): 30259 29629 145 145 0 30114 0
[pid=17833] vsize: 121036
Current children cumulated CPU time (s) 1197.64
Current children cumulated vsize (Kb) 123160

[startup+1210.11 s]
Raw data (loadavg): 0.99 0.97 0.88 2/57 17833
Raw data (/proc/17829/stat): 17829 (minisat+_script) S 17828 17829 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851765379 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17829/statm): 531 226 485 147 0 384 0
[pid=17829] vsize: 2124
Raw data (/proc/17833/stat): 17833 (minisat+_64-bit) R 17829 17829 28974 0 -1 0 32199 0 2 0 120562 198 0 0 25 0 1 0 1851765384 125329408 29968 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17833/statm): 30598 29968 145 145 0 30453 0
[pid=17833] vsize: 122392
Current children cumulated CPU time (s) 1207.61
Current children cumulated vsize (Kb) 124516



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.12 s]
Raw data (loadavg): 0.99 0.97 0.88 2/57 17833
Raw data (/proc/17829/stat): 17829 (minisat+_script) S 17828 17829 28974 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851765379 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/17829/statm): 531 226 485 147 0 384 0
[pid=17829] vsize: 2124
Raw data (/proc/17833/stat): 17833 (minisat+_64-bit) R 17829 17829 28974 0 -1 0 32199 0 2 0 120562 198 0 0 25 0 1 0 1851765384 125329408 29968 4294967295 134512640 135094434 3221224432 3221223056 134562085 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17833/statm): 30598 29968 145 145 0 30453 0
[pid=17833] vsize: 122392
Current children cumulated CPU time (s) 1207.61
Current children cumulated vsize (Kb) 124516

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

Child status: 10
Real time (s): 1210.18
CPU time (s): 1207.67
CPU user time (s): 1205.63
CPU system time (s): 2.04069
CPU usage (%): 99.7924
Max. virtual memory (cumulated for all children) (Kb): 124516

Verifier Data

ERROR: no interpretation found !