Some explanations

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

General information on the benchmark

Namemps-v2-20-10/plato.asu.edu/pub/fctp/normalized-mps-v2-20-10-ran10x10c.opb
MD5SUMda5013babdadf38e39e51a27df2c50f3
Bench Categoryoptimization, big integers (OPTBIGINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function 23566654
Optimality of the best value was proved NO
Number of terms in the objective function 3100
Biggest coefficient in the objective function 4831838208
Number of bits for the biggest coefficient in the objective function 33
Sum of the numbers in the objective function 515495338528
Number of bits of the sum of numbers in the objective function 39
Biggest number in a constraint 4831838208
Number of bits of the biggest number in a constraint 33
Biggest sum of numbers in a constraint 515495338528
Number of bits of the biggest sum of numbers39
Best result obtained on this benchmarkSAT
Best CPU time to get the best result obtained on this benchmark1236.44
Number of variables3100
Total number of constraints120
Number of constraints which are clauses0
Number of constraints which are cardinality constraints (but not clauses)0
Number of constraints which are nor clauses,nor cardinality constraints120
Minimum length of a constraint31
Maximum length of a constraint300

Trace number 4577

Launcher Data

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        686024 kB
Buffers:         41140 kB
Cached:         274520 kB
SwapCached:       1016 kB
Active:         103452 kB
Inactive:       214960 kB
HighTotal:      131008 kB
HighFree:         2240 kB
LowTotal:       903652 kB
LowFree:        683784 kB
SwapTotal:     2097892 kB
SwapFree:      2096404 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5776 kB
Slab:            24540 kB
Committed_AS:    64376 kB
PageTables:        340 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-09-19 18:49:20 (client local time) WITH STATUS 10 IN 1207.31 SECONDS
stats: 3038 7 1207.31 10

Solver Data

c Parsing PB file...
c Converting 140 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ####################
c   -- Clauses(.)/Splits(s): (none)
c ---[ 138]---> Sorter-cost: 2306     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 136]---> Sorter-cost: 2620     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 134]---> Sorter-cost: 2665     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 132]---> Sorter-cost: 2620     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 130]---> Sorter-cost: 2620     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 128]---> Sorter-cost: 2090     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 126]---> Sorter-cost: 2620     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 124]---> Adder-cost: 232   maxlim: 62454   bits: 17/16
c ---[ 122]---> Sorter-cost: 2620     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 120]---> Sorter-cost: 2665     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 118]---> Adder-cost: 216   maxlim: 36854   bits: 16/16
c ---[ 116]---> Sorter-cost: 2693     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 114]---> Adder-cost: 216   maxlim: 36854   bits: 16/16
c ---[ 112]---> Sorter-cost: 2693     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 110]---> Adder-cost: 232   maxlim: 65526   bits: 17/16
c ---[ 108]---> Adder-cost: 232   maxlim: 67574   bits: 17/17
c ---[ 106]---> Sorter-cost: 2661     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 104]---> Sorter-cost: 2661     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 102]---> Sorter-cost: 2693     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 100]---> Adder-cost: 216   maxlim: 36854   bits: 16/16
c ---[  99]---> BDD-cost:   13
c ---[  98]---> BDD-cost:   14
c ---[  97]---> BDD-cost:   13
c ---[  96]---> BDD-cost:   18
c ---[  95]---> BDD-cost:   13
c ---[  94]---> BDD-cost:   18
c ---[  93]---> BDD-cost:   15
c ---[  92]---> BDD-cost:   14
c ---[  91]---> BDD-cost:   18
c ---[  90]---> BDD-cost:   18
c ---[  89]---> BDD-cost:   18
c ---[  88]---> BDD-cost:   13
c ---[  87]---> BDD-cost:   13
c ---[  86]---> BDD-cost:   13
c ---[  85]---> BDD-cost:   16
c ---[  84]---> BDD-cost:   13
c ---[  83]---> BDD-cost:   16
c ---[  82]---> BDD-cost:   15
c ---[  81]---> BDD-cost:   14
c ---[  80]---> BDD-cost:   18
c ---[  79]---> BDD-cost:   16
c ---[  78]---> BDD-cost:   16
c ---[  77]---> BDD-cost:   13
c ---[  76]---> BDD-cost:   14
c ---[  75]---> BDD-cost:   13
c ---[  74]---> BDD-cost:   18
c ---[  73]---> BDD-cost:   13
c ---[  72]---> BDD-cost:   18
c ---[  71]---> BDD-cost:   15
c ---[  70]---> BDD-cost:   14
c ---[  69]---> BDD-cost:   18
c ---[  68]---> BDD-cost:   18
c ---[  67]---> BDD-cost:   18
c ---[  66]---> BDD-cost:   13
c ---[  65]---> BDD-cost:   14
c ---[  64]---> BDD-cost:   13
c ---[  63]---> BDD-cost:   17
c ---[  62]---> BDD-cost:   13
c ---[  61]---> BDD-cost:   17
c ---[  60]---> BDD-cost:   15
c ---[  59]---> BDD-cost:   14
c ---[  58]---> BDD-cost:   17
c ---[  57]---> BDD-cost:   17
c ---[  56]---> BDD-cost:   17
c ---[  55]---> BDD-cost:   13
c ---[  54]---> BDD-cost:   14
c ---[  53]---> BDD-cost:   12
c ---[  52]---> BDD-cost:   12
c ---[  51]---> BDD-cost:   12
c ---[  50]---> BDD-cost:   12
c ---[  49]---> BDD-cost:   12
c ---[  48]---> BDD-cost:   12
c ---[  47]---> BDD-cost:   12
c ---[  46]---> BDD-cost:   12
c ---[  45]---> BDD-cost:   12
c ---[  44]---> BDD-cost:   12
c ---[  43]---> BDD-cost:   14
c ---[  42]---> BDD-cost:   13
c ---[  41]---> BDD-cost:   18
c ---[  40]---> BDD-cost:   13
c ---[  39]---> BDD-cost:   18
c ---[  38]---> BDD-cost:   15
c ---[  37]---> BDD-cost:   14
c ---[  36]---> BDD-cost:   18
c ---[  35]---> BDD-cost:   16
c ---[  34]---> BDD-cost:   18
c ---[  33]---> BDD-cost:   13
c ---[  32]---> BDD-cost:   14
c ---[  31]---> BDD-cost:   13
c ---[  30]---> BDD-cost:   16
c ---[  29]---> BDD-cost:   13
c ---[  28]---> BDD-cost:   16
c ---[  27]---> BDD-cost:   15
c ---[  26]---> BDD-cost:   14
c ---[  25]---> BDD-cost:   16
c ---[  24]---> BDD-cost:   16
c ---[  23]---> BDD-cost:   16
c ---[  22]---> BDD-cost:   13
c ---[  21]---> BDD-cost:   14
c ---[  20]---> BDD-cost:   13
c ---[  19]---> BDD-cost:   18
c ---[  18]---> BDD-cost:   13
c ---[  17]---> BDD-cost:   18
c ---[  16]---> BDD-cost:   15
c ---[  15]---> BDD-cost:   14
c ---[  14]---> BDD-cost:   18
c ---[  13]---> BDD-cost:   18
c ---[  12]---> BDD-cost:   18
c ---[  11]---> BDD-cost:   13
c ---[  10]---> BDD-cost:   13
c ---[   9]---> BDD-cost:   13
c ---[   8]---> BDD-cost:   20
c ---[   7]---> BDD-cost:   13
c ---[   6]---> BDD-cost:   20
c ---[   5]---> BDD-cost:   15
c ---[   4]---> BDD-cost:   14
c ---[   3]---> BDD-cost:   18
c ---[   2]---> BDD-cost:   16
c ---[   1]---> BDD-cost:   20
c ---[   0]---> BDD-cost:   13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  105646   259466 |   35215       0        0     nan |  0.000 % |
c |       100 |  105646   259466 |   38736     100      705     7.0 |  8.015 % |
c |       250 |  105646   259466 |   42610     250     1320     5.3 |  8.015 % |
c |       475 |  105646   259466 |   46871     475     2399     5.1 |  8.015 % |
c |       812 |  105646   259466 |   51558     812     4080     5.0 |  8.015 % |
c |      1320 |  105630   259414 |   56714    1318     6910     5.2 |  8.023 % |
c |      2079 |  105564   259190 |   62385    2070    11012     5.3 |  8.056 % |
c |      3220 |  105403   258818 |   68624    3192    16614     5.2 |  8.175 % |
c |      4928 |  105343   258680 |   75486    4893    26367     5.4 |  8.218 % |
c |      7492 |  105343   258680 |   83035    7457    40139     5.4 |  8.218 % |
c |     11336 |  104896   257599 |   91338   11274    62479     5.5 |  8.574 % |
c |     17102 |  104515   256573 |  100472   16998    98189     5.8 |  8.828 % |
c |     25751 |  104267   255953 |  110519   25590   224926     8.8 |  9.004 % |
c ==============================================================================
c Found solution: 99691608
c ---[   0]---> Adder-cost: 4953   maxlim: 4167112   bits: 23/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     28129 |  138497   378323 |   46165   27955   240787     8.6 |  9.004 % |
c |     28230 |  138497   378323 |   50781   28056   241294     8.6 |  8.019 % |
c |     28380 |  138497   378323 |   55859   28206   242155     8.6 |  8.019 % |
c |     28605 |  138497   378323 |   61445   28431   243648     8.6 |  8.019 % |
c |     28942 |  138497   378323 |   67590   28768   245877     8.5 |  8.019 % |
c ==============================================================================
c Found solution: 97594485
c ---[   0]---> Adder-cost: 35   maxlim: 6264235   bits: 24/23
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     29291 |  138713   379191 |   46237   29116   248666     8.5 |  8.019 % |
c |     29391 |  138656   379060 |   50860   29213   249240     8.5 |  8.089 % |
c |     29541 |  138656   379060 |   55946   29363   250276     8.5 |  8.089 % |
c |     29766 |  138553   378824 |   61541   29587   251627     8.5 |  8.170 % |
c |     30104 |  138553   378824 |   67695   29925   288957     9.7 |  8.170 % |
c |     30611 |  138553   378824 |   74465   30432   292344     9.6 |  8.170 % |
c |     31370 |  138506   378704 |   81911   31187   306203     9.8 |  8.203 % |
c |     32509 |  138506   378704 |   90102   32326   328837    10.2 |  8.203 % |
c ==============================================================================
c Found solution: 65247565
c ---[   0]---> Adder-cost: 20   maxlim: 38611155   bits: 27/26
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     33824 |  138656   379345 |   46218   33638   354051    10.5 |  8.203 % |
c |     33924 |  138656   379345 |   50839   33738   355423    10.5 |  8.233 % |
c |     34074 |  138656   379345 |   55923   33888   357263    10.5 |  8.233 % |
c |     34299 |  138656   379345 |   61516   34113   362594    10.6 |  8.233 % |
c |     34636 |  138640   379293 |   67667   34448   364887    10.6 |  8.240 % |
c |     35144 |  138640   379293 |   74434   34956   369137    10.6 |  8.240 % |
c |     35903 |  138640   379293 |   81878   35715   381275    10.7 |  8.240 % |
c |     37042 |  138640   379293 |   90065   36854   407823    11.1 |  8.240 % |
c |     38750 |  138640   379293 |   99072   38562   464898    12.1 |  8.240 % |
c |     41312 |  138640   379293 |  108979   41124   525472    12.8 |  8.240 % |
c |     45156 |  138640   379293 |  119877   44968   740250    16.5 |  8.240 % |
c ==============================================================================
c Found solution: 64276304
c ---[   0]---> Adder-cost: 0   maxlim: 39582416   bits: 27/26
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     46797 |  138635   379489 |   46211   46605   812650    17.4 |  8.240 % |
c |     46897 |  138635   379489 |   50832   46705   813244    17.4 |  8.293 % |
c |     47049 |  138635   379489 |   55915   46857   814707    17.4 |  8.293 % |
c |     47274 |  138635   379489 |   61506   47082   819373    17.4 |  8.293 % |
c |     47612 |  138635   379489 |   67657   47420   822714    17.3 |  8.293 % |
c |     48118 |  138635   379489 |   74423   47926   829558    17.3 |  8.293 % |
c |     48879 |  138619   379437 |   81865   48684   842322    17.3 |  8.300 % |
c |     50018 |  138562   379309 |   90052   49817   911363    18.3 |  8.340 % |
c |     51727 |  138421   378983 |   99057   51494  1062374    20.6 |  8.436 % |
c |     54289 |  138402   378940 |  108963   54055  1141068    21.1 |  8.447 % |
c |     58136 |  138391   378915 |  119859   57901  1486487    25.7 |  8.455 % |
c |     63902 |  138325   378766 |  131845   63659  1773211    27.9 |  8.500 % |
c |     72551 |  138299   378708 |  145029   72303  2535782    35.1 |  8.519 % |
c ==============================================================================
c Found solution: 62500645
c ---[   0]---> Adder-cost: 0   maxlim: 41358075   bits: 27/26
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     72952 |  138284   378866 |   46094   72701  2555567    35.2 |  8.519 % |
c |     73052 |  138284   378866 |   50703   22769   996443    43.8 |  8.568 % |
c |     73202 |  138284   378866 |   55773   22919   997315    43.5 |  8.568 % |
c |     73428 |  138214   378703 |   61351   23140   998377    43.1 |  8.613 % |
c |     73765 |  138214   378703 |   67486   23477  1001162    42.6 |  8.613 % |
c |     74271 |  138214   378703 |   74234   23983  1007222    42.0 |  8.613 % |
c |     75030 |  138214   378703 |   81658   24742  1064677    43.0 |  8.613 % |
c |     76169 |  138214   378703 |   89824   25881  1071124    41.4 |  8.613 % |
c |     77878 |  138214   378703 |   98806   27590  1141703    41.4 |  8.613 % |
c |     80440 |  138211   378697 |  108687   30151  1348483    44.7 |  8.615 % |
c |     84284 |  137973   378149 |  119555   33991  1406015    41.4 |  8.777 % |
c |     90050 |  137973   378149 |  131511   39757  1620800    40.8 |  8.777 % |
c |     98699 |  137973   378149 |  144662   48406  3294818    68.1 |  8.777 % |
c |    111673 |  137772   377685 |  159128   61361  3814730    62.2 |  8.926 % |
c |    131134 |  137750   377633 |  175041   80820  5408926    66.9 |  8.941 % |
c ==============================================================================
c Found solution: 60904598
c ---[   0]---> Adder-cost: 0   maxlim: 42954122   bits: 27/26
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    132500 |  137776   377892 |   45925   82186  5543726    67.5 |  8.941 % |
c |    132600 |  137776   377892 |   50517   22593   877249    38.8 |  8.969 % |
c |    132750 |  137656   377619 |   55569   22700   877766    38.7 |  9.048 % |
c |    132976 |  137656   377619 |   61126   22926   879059    38.3 |  9.048 % |
c |    133313 |  137613   377522 |   67238   23255   882589    38.0 |  9.081 % |
c |    133819 |  137597   377485 |   73962   23758   886347    37.3 |  9.093 % |
c |    134578 |  137597   377485 |   81358   24517   891943    36.4 |  9.093 % |
c |    135717 |  137597   377485 |   89494   25656   929101    36.2 |  9.093 % |
c |    137425 |  137597   377485 |   98444   27364   988200    36.1 |  9.093 % |
c |    139988 |  137557   377391 |  108288   29923  1029060    34.4 |  9.126 % |
c |    143834 |  137557   377391 |  119117   33769  1389147    41.1 |  9.126 % |
c |    149600 |  137388   377002 |  131029   39512  1617069    40.9 |  9.245 % |
c |    158249 |  137308   376816 |  144132   48153  2365211    49.1 |  9.300 % |
c |    171223 |  137015   376138 |  158545   61110  2975688    48.7 |  9.523 % |
c |    190684 |  136983   376067 |  174400   80569  4215636    52.3 |  9.544 % |
c |    219876 |  136901   375861 |  191840  109745  7879417    71.8 |  9.599 % |
c |    263668 |  136538   375015 |  211024  153513 10857470    70.7 |  9.846 % |
c |    329352 |  136341   374559 |  232126  219170 19164377    87.4 |  9.995 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v -X0_bit_10 X0_bit_9 X0_bit_8 X0_bit_7 -X0_bit_6 X0_bit_5 X0_bit_4 X0_bit_3 -X0_bit_2 -X0_bit_1 -X0_bit0 -X0_bit1 -X0_bit2 -X0_bit3 -X0_bit4 -X0_bit5 -X0_bit6 -X0_bit7 -X0_bit8 -X0_bit9 -X0_bit10 -X0_bit11 -X0_bit12 -X0_bit13 -X0_bit14 -X0_bit15 -X0_bit16 -X0_bit17 -X0_bit18 -X0_bit19 -X1_bit_10 -X1_bit_9 -X1_bit_8 -X1_bit_7 -X1_bit_6 -X1_bit_5 -X1_bit_4 -X1_bit_3 -X1_bit_2 -X1_bit_1 -X1_bit0 -X1_bit1 -X1_bit2 -X1_bit3 -X1_bit4 -X1_bit5 -X1_bit6 -X1_bit7 -X1_bit8 -X1_bit9 -X1_bit10 -X1_bit11 -X1_bit12 -X1_bit13 -X1_bit14 -X1_bit15 -X1_bit16 -X1_bit17 -X1_bit18 -X1_bit19 X2_bit_10 X2_bit_9 -X2_bit_8 -X2_bit_7 X2_bit_6 -X2_bit_5 X2_bit_4 X2_bit_3 -X2_bit_2 -X2_bit_1 -X2_bit0 -X2_bit1 -X2_bit2 -X2_bit3 -X2_bit4 -X2_bit5 -X2_bit6 -X2_bit7 -X2_bit8 -X2_bit9 -X2_bit10 -X2_bit11 -X2_bit12 -X2_bit13 -X2_bit14 -X2_bit15 -X2_bit16 -X2_bit17 -X2_bit18 -X2_bit19 -X3_bit_10 -X3_bit_9 -X3_bit_8 -X3_bit_7 -X3_bit_6 -X3_bit_5 -X3_bit_4 -X3_bit_3 -X3_bit_2 -X3_bit_1 -X3_bit0 -X3_bit1 -X3_bit2 -X3_bit3 -X3_bit4 -X3_bit5 -X3_bit6 -X3_bit7 -X3_bit8 -X3_bit9 -X3_bit10 -X3_bit11 -X3_bit12 -X3_bit13 -X3_bit14 -X3_bit15 -X3_bit16 -X3_bit17 -X3_bit18 -X3_bit19 X4_bit_10 X4_bit_9 X4_bit_8 -X4_bit_7 -X4_bit_6 X4_bit_5 -X4_bit_4 X4_bit_3 -X4_bit_2 -X4_bit_1 -X4_bit0 -X4_bit1 -X4_bit2 -X4_bit3 -X4_bit4 -X4_bit5 -X4_bit6 -X4_bit7 -X4_bit8 -X4_bit9 -X4_bit10 -X4_bit11 -X4_bit12 -X4_bit13 -X4_bit14 -X4_bit15 -X4_bit16 -X4_bit17 -X4_bit18 -X4_bit19 -X5_bit_10 -X5_bit_9 -X5_bit_8 -X5_bit_7 -X5_bit_6 -X5_bit_5 -X5_bit_4 -X5_bit_3 -X5_bit_2 -X5_bit_1 -X5_bit0 -X5_bit1 -X5_bit2 -X5_bit3 -X5_bit4 -X5_bit5 -X5_bit6 -X5_bit7 -X5_bit8 -X5_bit9 -X5_bit10 -X5_bit11 -X5_bit12 -X5_bit13 -X5_bit14 -X5_bit15 -X5_bit16 -X5_bit17 -X5_bit18 -X5_bit19 -X6_bit_10 -X6_bit_9 -X6_bit_8 X6_bit_7 X6_bit_6 -X6_bit_5 -X6_bit_4 X6_bit_3 X6_bit_2 -X6_bit_1 -X6_bit0 X6_bit1 -X6_bit2 -X6_bit3 -X6_bit4 -X6_bit5 -X6_bit6 -X6_bit7 -X6_bit8 -X6_bit9 -X6_bit10 -X6_bit11 -X6_bit12 -X6_bit13 -X6_bit14 -X6_bit15 -X6_bit16 -X6_bit17 -X6_bit18 -X6_bit19 -X7_bit_10 -X7_bit_9 -X7_bit_8 -X7_bit_7 -X7_bit_6 -X7_bit_5 -X7_bit_4 -X7_bit_3 -X7_bit_2 -X7_bit_1 -X7_bit0 -X7_bit1 -X7_bit2 -X7_bit3 -X7_bit4 -X7_bit5 -X7_bit6 -X7_bit7 -X7_bit8 -X7_bit9 -X7_bit10 -X7_bit11 -X7_bit12 -X7_bit13 -X7_bit14 -X7_bit15 -X7_bit16 -X7_bit17 -X7_bit18 -X7_bit19 -X8_bit_10 -X8_bit_9 -X8_bit_8 -X8_bit_7 -X8_bit_6 -X8_bit_5 -X8_bit_4 -X8_bit_3 -X8_bit_2 -X8_bit_1 -X8_bit0 -X8_bit1 -X8_bit2 -X8_bit3 -X8_bit4 -X8_bit5 -X8_bit6 -X8_bit7 -X8_bit8 -X8_bit9 -X8_bit10 -X8_bit11 -X8_bit12 -X8_bit13 -X8_bit14 -X8_bit15 -X8_bit16 -X8_bit17 -X8_bit18 -X8_bit19 -X9_bit_10 -X9_bit_9 -X9_bit_8 -X9_bit_7 -X9_bit_6 -X9_bit_5 -X9_bit_4 -X9_bit_3 -X9_bit_2 -X9_bit_1 -X9_bit0 -X9_bit1 -X9_bit2 -X9_bit3 -X9_bit4 -X9_bit5 -X9_bit6 -X9_bit7 -X9_bit8 -X9_bit9 -X9_bit10 -X9_bit11 -X9_bit12 -X9_bit13 -X9_bit14 -X9_bit15 -X9_bit16 -X9_bit17 -X9_bit18 -X9_bit19 X10_bit_10 X10_bit_9 X10_bit_8 X10_bit_7 -X10_bit_6 X10_bit_5 -X10_bit_4 -X10_bit_3 -X10_bit_2 -X10_bit_1 -X10_bit0 -X10_bit1 -X10_bit2 -X10_bit3 -X10_bit4 -X10_bit5 -X10_bit6 -X10_bit7 -X10_bit8 -X10_bit9 -X10_bit10 -X10_bit11 -X10_bit12 -X10_bit13 -X10_bit14 -X10_bit15 -X10_bit16 -X10_bit17 -X10_bit18 -X10_bit19 X11_bit_10 -X11_bit_9 -X11_bit_8 -X11_bit_7 -X11_bit_6 X11_bit_5 -X11_bit_4 X11_bit_3 X11_bit_2 -X11_bit_1 X11_bit0 X11_bit1 X11_bit2 -X11_bit3 -X11_bit4 -X11_bit5 -X11_bit6 -X11_bit7 -X11_bit8 -X11_bit9 -X11_bit10 -X11_bit11 -X11_bit12 -X11_bit13 -X11_bit14 -X11_bit15 -X11_bit16 -X11_bit17 -X11_bit18 -X11_bit19 -X12_bit_10 -X12_bit_9 -X12_bit_8 -X12_bit_7 -X12_bit_6 -X12_bit_5 -X12_bit_4 -X12_bit_3 -X12_bit_2 -X12_bit_1 -X12_bit0 -X12_bit1 -X12_bit2 -X12_bit3 -X12_bit4 -X12_bit5 -X12_bit6 -X12_bit7 -X12_bit8 -X12_bit9 -X12_bit10 -X12_bit11 -X12_bit12 -X12_bit13 -X12_bit14 -X12_bit15 -X12_bit16 -X12_bit17 -X12_bit18 -X12_bit19 -X13_bit_10 -X13_bit_9 -X13_bit_8 -X13_bit_7 -X13_bit_6 -X13_bit_5 -X13_bit_4 -X13_bit_3 -X13_bit_2 -X13_bit_1 -X13_bit0 -X13_bit1 -X13_bit2 -X13_bit3 -X13_bit4 -X13_bit5 -X13_bit6 -X13_bit7 -X13_bit8 -X13_bit9 -X13_bit10 -X13_bit11 -X13_bit12 -X13_bit13 -X13_bit14 -X13_bit15 -X13_bit16 -X13_bit17 -X13_bit18 -X13_bit19 X14_bit_10 X14_bit_9 X14_bit_8 -X14_bit_7 -X14_bit_6 -X14_bit_5 -X14_bit_4 -X14_bit_3 -X14_bit_2 -X14_bit_1 -X14_bit0 -X14_bit1 -X14_bit2 -X14_bit3 -X14_bit4 -X14_bit5 -X14_bit6 -X14_bit7 -X14_bit8 -X14_bit9 -X14_bit10 -X14_bit11 -X14_bit12 -X14_bit13 -X14_bit14 -X14_bit15 -X14_bit16 -X14_bit17 -X14_bit18 -X14_bit19 -X15_bit_10 X15_bit_9 -X15_bit_8 -X15_bit_7 -X15_bit_6 X15_bit_5 -X15_bit_4 -X15_bit_3 -X15_bit_2 -X15_bit_1 -X15_bit0 -X15_bit1 -X15_bit2 -X15_bit3 -X15_bit4 -X15_bit5 -X15_bit6 -X15_bit7 -X15_bit8 -X15_bit9 -X15_bit10 -X15_bit11 -X15_bit12 -X15_bit13 -X15_bit14 -X15_bit15 -X15_bit16 -X15_bit17 -X15_bit18 -X15_bit19 -X16_bit_10 -X16_bit_9 -X16_bit_8 X16_bit_7 X16_bit_6 -X16_bit_5 -X16_bit_4 X16_bit_3 -X16_bit_2 -X16_bit_1 X16_bit0 -X16_bit1 -X16_bit2 -X16_bit3 -X16_bit4 -X16_bit5 -X16_bit6 -X16_bit7 -X16_bit8 -X16_bit9 -X16_bit10 -X16_bit11 -X16_bit12 -X16_bit13 -X16_bit14 -X16_bit15 -X16_bit16 -X16_bit17 -X16_bit18 -X16_bit19 -X17_bit_10 -X17_bit_9 -X17_bit_8 -X17_bit_7 -X17_bit_6 -X17_bit_5 X17_bit_4 X17_bit_3 -X17_bit_2 -X17_bit_1 -X17_bit0 -X17_bit1 -X17_bit2 -X17_bit3 -X17_bit4 -X17_bit5 -X17_bit6 -X17_bit7 -X17_bit8 -X17_bit9 -X17_bit10 -X17_bit11 -X17_bit12 -X17_bit13 -X17_bit14 -X17_bit15 -X17_bit16 -X17_bit17 -X17_bit18 -X17_bit19 -X18_bit_10 -X18_bit_9 -X18_bit_8 -X18_bit_7 -X18_bit_6 -X18_bit_5 -X18_bit_4 -X18_bit_3 -X18_bit_2 -X18_bit_1 -X18_bit0 -X18_bit1 -X18_bit2 -X18_bit3 -X18_bit4 -X18_bit5 -X18_bit6 -X18_bit7 -X18_bit8 -X18_bit9 -X18_bit10 -X18_bit11 -X18_bit12 -X18_bit13 -X18_bit14 -X18_bit15 -X18_bit16 -X18_bit17 -X18_bit18 -X18_bit19 X19_bit_10 X19_bit_9 X19_bit_8 X19_bit_7 -X19_bit_6 X19_bit_5 -X19_bit_4 X19_bit_3 -X19_bit_2 -X19_bit_1 -X19_bit0 -X19_bit1 -X19_bit2 -X19_bit3 -X19_bit4 -X19_bit5 -X19_bit6 -X19_bit7 -X19_bit8 -X19_bit9 -X19_bit10 -X19_bit11 -X19_bit12 -X19_bit13 -X19_bit14 -X19_bit15 -X19_bit16 -X19_bit17 -X19_bit18 -X19_bit19 -X20_bit_10 X20_bit_9 X20_bit_8 X20_bit_7 -X20_bit_6 X20_bit_5 -X20_bit_4 X20_bit_3 X20_bit_2 -X20_bit_1 -X20_bit0 -X20_bit1 -X20_bit2 -X20_bit3 -X20_bit4 -X20_bit5 -X20_bit6 -X20_bit7 -X20_bit8 -X20_bit9 -X20_bit10 -X20_bit11 -X20_bit12 -X20_bit13 -X20_bit14 -X20_bit15 -X20_bit16 -X20_bit17 -X20_bit18 -X20_bit19 X21_bit_10 -X21_bit_9 X21_bit_8 -X21_bit_7 X21_bit_6 X21_bit_5 X21_bit_4 X21_bit_3 X21_bit_2 X21_bit_1 X21_bit0 -X21_bit1 X21_bit2 -X21_bit3 -X21_bit4 -X21_bit5 -X21_bit6 -X21_bit7 -X21_bit8 -X21_bit9 -X21_bit10 -X21_bit11 -X21_bit12 -X21_bit13 -X21_bit14 -X21_bit15 -X21_bit16 -X21_bit17 -X21_bit18 -X21_bit19 -X22_bit_10 -X22_bit_9 -X22_bit_8 -X22_bit_7 -X22_bit_6 -X22_bit_5 -X22_bit_4 -X22_bit_3 -X22_bit_2 -X22_bit_1 -X22_bit0 -X22_bit1 -X22_bit2 -X22_bit3 -X22_bit4 -X22_bit5 -X22_bit6 -X22_bit7 -X22_bit8 -X22_bit9 -X22_bit10 -X22_bit11 -X22_bit12 -X22_bit13 -X22_bit14 -X22_bit15 -X22_bit16 -X22_bit17 -X22_bit18 -X22_bit19 -X23_bit_10 -X23_bit_9 -X23_bit_8 -X23_bit_7 -X23_bit_6 -X23_bit_5 -X23_bit_4 -X23_bit_3 -X23_bit_2 -X23_bit_1 -X23_bit0 -X23_bit1 -X23_bit2 -X23_bit3 -X23_bit4 -X23_bit5 -X23_bit6 -X23_bit7 -X23_bit8 -X23_bit9 -X23_bit10 -X23_bit11 -X23_bit12 -X23_bit13 -X23_bit14 -X23_bit15 -X23_bit16 -X23_bit17 -X23_bit18 -X23_bit19 X24_bit_10 X24_bit_9 X24_bit_8 X24_bit_7 X24_bit_6 X24_bit_5 X24_bit_4 X24_bit_3 -X24_bit_2 X24_bit_1 X24_bit0 -X24_bit1 -X24_bit2 -X24_bit3 -X24_bit4 -X24_bit5 -X24_bit6 -X24_bit7 -X24_bit8 -X24_bit9 -X24_bit10 -X24_bit11 -X24_bit12 -X24_bit13 -X24_bit14 -X24_bit15 -X24_bit16 -X24_bit17 -X24_bit18 -X24_bit19 X25_bit_10 X25_bit_9 -X25_bit_8 -X25_bit_7 X25_bit_6 X25_bit_5 X25_bit_4 -X25_bit_3 -X25_bit_2 -X25_bit_1 -X25_bit0 -X25_bit1 -X25_bit2 -X25_bit3 -X25_bit4 -X25_bit5 -X25_bit6 -X25_bit7 -X25_bit8 -X25_bit9 -X25_bit10 -X25_bit11 -X25_bit12 -X25_bit13 -X25_bit14 -X25_bit15 -X25_bit16 -X25_bit17 -X25_bit18 -X25_bit19 -X26_bit_10 -X26_bit_9 -X26_bit_8 X26_bit_7 X26_bit_6 X26_bit_5 X26_bit_4 X26_bit_3 X26_bit_2 X26_bit_1 X26_bit0 -X26_bit1 -X26_bit2 -X26_bit3 -X26_bit4 -X26_bit5 -X26_bit6 -X26_bit7 -X26_bit8 -X26_bit9 -X26_bit10 -X26_bit11 -X26_bit12 -X26_bit13 -X26_bit14 -X26_bit15 -X26_bit16 -X26_bit17 -X26_bit18 -X26_bit19 -X27_bit_10 -X27_bit_9 -X27_bit_8 -X27_bit_7 -X27_bit_6 -X27_bit_5 -X27_bit_4 -X27_bit_3 -X27_bit_2 -X27_bit_1 -X27_bit0 -X27_bit1 -X27_bit2 -X27_bit3 -X27_bit4 -X27_bit5 -X27_bit6 -X27_bit7 -X27_bit8 -X27_bit9 -X27_bit10 -X27_bit11 -X27_bit12 -X27_bit13 -X27_bit14 -X27_bit15 -X27_bit16 -X27_bit17 -X27_bit18 -X27_bit19 X28_bit_10 X28_bit_9 -X28_bit_8 -X28_bit_7 X28_bit_6 X28_bit_5 X28_bit_4 X28_bit_3 -X28_bit_2 X28_bit_1 X28_bit0 -X28_bit1 X28_bit2 -X28_bit3 -X28_bit4 -X28_bit5 -X28_bit6 -X28_bit7 -X28_bit8 -X28_bit9 -X28_bit10 -X28_bit11 -X28_bit12 -X28_bit13 -X28_bit14 -X28_bit15 -X28_bit16 -X28_bit17 -X28_bit18 -X28_bit19 -X29_bit_10 -X29_bit_9 -X29_bit_8 -X29_bit_7 -X29_bit_6 -X29_bit_5 -X29_bit_4 -X29_bit_3 -X29_bit_2 -X29_bit_1 -X29_bit0 -X29_bit1 -X29_bit2 -X29_bit3 -X29_bit4 -X29_bit5 -X29_bit6 -X29_bit7 -X29_bit8 -X29_bit9 -X29_bit10 -X29_bit11 -X29_bit12 -X29_bit13 -X29_bit14 -X29_bit15 -X29_bit16 -X29_bit17 -X29_bit18 -X29_bit19 -X30_bit_10 -X30_bit_9 -X30_bit_8 -X30_bit_7 -X30_bit_6 -X30_bit_5 -X30_bit_4 -X30_bit_3 -X30_bit_2 -X30_bit_1 -X30_bit0 -X30_bit1 -X30_bit2 -X30_bit3 -X30_bit4 -X30_bit5 -X30_bit6 -X30_bit7 -X30_bit8 -X30_bit9 -X30_bit10 -X30_bit11 -X30_bit12 -X30_bit13 -X30_bit14 -X30_bit15 -X30_bit16 -X30_bit17 -X30_bit18 -X30_bit19 -X31_bit_10 -X31_bit_9 -X31_bit_8 -X31_bit_7 -X31_bit_6 -X31_bit_5 -X31_bit_4 -X31_bit_3 -X31_bit_2 -X31_bit_1 -X31_bit0 -X31_bit1 -X31_bit2 -X31_bit3 -X31_bit4 -X31_bit5 -X31_bit6 -X31_bit7 -X31_bit8 -X31_bit9 -X31_bit10 -X31_bit11 -X31_bit12 -X31_bit13 -X31_bit14 -X31_bit15 -X31_bit16 -X31_bit17 -X31_bit18 -X31_bit19 -X32_bit_10 -X32_bit_9 -X32_bit_8 -X32_bit_7 -X32_bit_6 -X32_bit_5 -X32_bit_4 -X32_bit_3 -X32_bit_2 -X32_bit_1 -X32_bit0 -X32_bit1 -X32_bit2 -X32_bit3 -X32_bit4 -X32_bit5 -X32_bit6 -X32_bit7 -X32_bit8 -X32_bit9 -X32_bit10 -X32_bit11 -X32_bit12 -X32_bit13 -X32_bit14 -X32_bit15 -X32_bit16 -X32_bit17 -X32_bit18 -X32_bit19 X33_bit_10 X33_bit_9 -X33_bit_8 -X33_bit_7 -X33_bit_6 -X33_bit_5 X33_bit_4 X33_bit_3 X33_bit_2 -X33_bit_1 X33_bit0 -X33_bit1 -X33_bit2 X33_bit3 -X33_bit4 -X33_bit5 -X33_bit6 -X33_bit7 -X33_bit8 -X33_bit9 -X33_bit10 -X33_bit11 -X33_bit12 -X33_bit13 -X33_bit14 -X33_bit15 -X33_bit16 -X33_bit17 -X33_bit18 -X33_bit19 -X34_bit_10 -X34_bit_9 -X34_bit_8 X34_bit_7 -X34_bit_6 X34_bit_5 -X34_bit_4 -X34_bit_3 -X34_bit_2 -X34_bit_1 -X34_bit0 -X34_bit1 -X34_bit2 -X34_bit3 -X34_bit4 -X34_bit5 -X34_bit6 -X34_bit7 -X34_bit8 -X34_bit9 -X34_bit10 -X34_bit11 -X34_bit12 -X34_bit13 -X34_bit14 -X34_bit15 -X34_bit16 -X34_bit17 -X34_bit18 -X34_bit19 X35_bit_10 X35_bit_9 -X35_bit_8 X35_bit_7 X35_bit_6 X35_bit_5 -X35_bit_4 -X35_bit_3 -X35_bit_2 -X35_bit_1 -X35_bit0 -X35_bit1 -X35_bit2 -X35_bit3 -X35_bit4 -X35_bit5 -X35_bit6 -X35_bit7 -X35_bit8 -X35_bit9 -X35_bit10 -X35_bit11 -X35_bit12 -X35_bit13 -X35_bit14 -X35_bit15 -X35_bit16 -X35_bit17 -X35_bit18 -X35_bit19 -X36_bit_10 -X36_bit_9 -X36_bit_8 X36_bit_7 X36_bit_6 -X36_bit_5 -X36_bit_4 X36_bit_3 X36_bit_2 -X36_bit_1 -X36_bit0 -X36_bit1 -X36_bit2 -X36_bit3 -X36_bit4 -X36_bit5 -X36_bit6 -X36_bit7 -X36_bit8 -X36_bit9 -X36_bit10 -X36_bit11 -X36_bit12 -X36_bit13 -X36_bit14 -X36_bit15 -X36_bit16 -X36_bit17 -X36_bit18 -X36_bit19 -X37_bit_10 -X37_bit_9 -X37_bit_8 -X37_bit_7 -X37_bit_6 -X37_bit_5 -X37_bit_4 -X37_bit_3 -X37_bit_2 -X37_bit_1 -X37_bit0 -X37_bit1 -X37_bit2 -X37_bit3 -X37_bit4 -X37_bit5 -X37_bit6 -X37_bit7 -X37_bit8 -X37_bit9 -X37_bit10 -X37_bit11 -X37_bit12 -X37_bit13 -X37_bit14 -X37_bit15 -X37_bit16 -X37_bit17 -X37_bit18 -X37_bit19 X38_bit_10 X38_bit_9 -X38_bit_8 -X38_bit_7 X38_bit_6 X38_bit_5 X38_bit_4 -X38_bit_3 X38_bit_2 X38_bit_1 -X38_bit0 -X38_bit1 -X38_bit2 -X38_bit3 -X38_bit4 -X38_bit5 -X38_bit6 -X38_bit7 -X38_bit8 -X38_bit9 -X38_bit10 -X38_bit11 -X38_bit12 -X38_bit13 -X38_bit14 -X38_bit15 -X38_bit16 -X38_bit17 -X38_bit18 -X38_bit19 X39_bit_10 X39_bit_9 X39_bit_8 X39_bit_7 -X39_bit_6 -X39_bit_5 X39_bit_4 X39_bit_3 -X39_bit_2 -X39_bit_1 -X39_bit0 -X39_bit1 -X39_bit2 -X39_bit3 -X39_bit4 -X39_bit5 -X39_bit6 -X39_bit7 -X39_bit8 -X39_bit9 -X39_bit10 -X39_bit11 -X39_bit12 -X39_bit13 -X39_bit14 -X39_bit15 -X39_bit16 -X39_bit17 -X39_bit18 -X39_bit19 -X40_bit_10 -X40_bit_9 -X40_bit_8 -X40_bit_7 -X40_bit_6 -X40_bit_5 -X40_bit_4 -X40_bit_3 -X40_bit_2 -X40_bit_1 -X40_bit0 -X40_bit1 -X40_bit2 -X40_bit3 -X40_bit4 -X40_bit5 -X40_bit6 -X40_bit7 -X40_bit8 -X40_bit9 -X40_bit10 -X40_bit11 -X40_bit12 -X40_bit13 -X40_bit14 -X40_bit15 -X40_bit16 -X40_bit17 -X40_bit18 -X40_bit19 -X41_bit_10 -X41_bit_9 -X41_bit_8 -X41_bit_7 -X41_bit_6 -X41_bit_5 -X41_bit_4 -X41_bit_3 -X41_bit_2 -X41_bit_1 -X41_bit0 -X41_bit1 -X41_bit2 -X41_bit3 -X41_bit4 -X41_bit5 -X41_bit6 -X41_bit7 -X41_bit8 -X41_bit9 -X41_bit10 -X41_bit11 -X41_bit12 -X41_bit13 -X41_bit14 -X41_bit15 -X41_bit16 -X41_bit17 -X41_bit18 -X41_bit19 X42_bit_10 X42_bit_9 X42_bit_8 X42_bit_7 X42_bit_6 X42_bit_5 X42_bit_4 -X42_bit_3 -X42_bit_2 X42_bit_1 X42_bit0 -X42_bit1 -X42_bit2 -X42_bit3 -X42_bit4 -X42_bit5 -X42_bit6 -X42_bit7 -X42_bit8 -X42_bit9 -X42_bit10 -X42_bit11 -X42_bit12 -X42_bit13 -X42_bit14 -X42_bit15 -X42_bit16 -X42_bit17 -X42_bit18 -X42_bit19 -X43_bit_10 -X43_bit_9 -X43_bit_8 -X43_bit_7 -X43_bit_6 -X43_bit_5 -X43_bit_4 -X43_bit_3 -X43_bit_2 -X43_bit_1 -X43_bit0 -X43_bit1 -X43_bit2 -X43_bit3 -X43_bit4 -X43_bit5 -X43_bit6 -X43_bit7 -X43_bit8 -X43_bit9 -X43_bit10 -X43_bit11 -X43_bit12 -X43_bit13 -X43_bit14 -X43_bit15 -X43_bit16 -X43_bit17 -X43_bit18 -X43_bit19 -X44_bit_10 -X44_bit_9 X44_bit_8 X44_bit_7 X44_bit_6 X44_bit_5 X44_bit_4 X44_bit_3 X44_bit_2 X44_bit_1 -X44_bit0 X44_bit1 -X44_bit2 -X44_bit3 -X44_bit4 -X44_bit5 -X44_bit6 -X44_bit7 -X44_bit8 -X44_bit9 -X44_bit10 -X44_bit11 -X44_bit12 -X44_bit13 -X44_bit14 -X44_bit15 -X44_bit16 -X44_bit17 -X44_bit18 -X44_bit19 X45_bit_10 X45_bit_9 -X45_bit_8 X45_bit_7 X45_bit_6 X45_bit_5 X45_bit_4 X45_bit_3 X45_bit_2 -X45_bit_1 -X45_bit0 X45_bit1 -X45_bit2 -X45_bit3 -X45_bit4 -X45_bit5 -X45_bit6 -X45_bit7 -X45_bit8 -X45_bit9 -X45_bit10 -X45_bit11 -X45_bit12 -X45_bit13 -X45_bit14 -X45_bit15 -X45_bit16 -X45_bit17 -X45_bit18 -X45_bit19 -X46_bit_10 -X46_bit_9 -X46_bit_8 -X46_bit_7 -X46_bit_6 -X46_bit_5 -X46_bit_4 -X46_bit_3 -X46_bit_2 -X46_bit_1 -X46_bit0 -X46_bit1 -X46_bit2 -X46_bit3 -X46_bit4 -X46_bit5 -X46_bit6 -X46_bit7 -X46_bit8 -X46_bit9 -X46_bit10 -X46_bit11 -X46_bit12 -X46_bit13 -X46_bit14 -X46_bit15 -X46_bit16 -X46_bit17 -X46_bit18 -X46_bit19 -X47_bit_10 -X47_bit_9 -X47_bit_8 -X47_bit_7 X47_bit_6 -X47_bit_5 -X47_bit_4 X47_bit_3 X47_bit_2 -X47_bit_1 -X47_bit0 X47_bit1 -X47_bit2 -X47_bit3 -X47_bit4 -X47_bit5 -X47_bit6 -X47_bit7 -X47_bit8 -X47_bit9 -X47_bit10 -X47_bit11 -X47_bit12 -X47_bit13 -X47_bit14 -X47_bit15 -X47_bit16 -X47_bit17 -X47_bit18 -X47_bit19 -X48_bit_10 -X48_bit_9 -X48_bit_8 -X48_bit_7 -X48_bit_6 -X48_bit_5 -X48_bit_4 -X48_bit_3 -X48_bit_2 -X48_bit_1 -X48_bit0 -X48_bit1 -X48_bit2 -X48_bit3 -X48_bit4 -X48_bit5 -X48_bit6 -X48_bit7 -X48_bit8 -X48_bit9 -X48_bit10 -X48_bit11 -X48_bit12 -X48_bit13 -X48_bit14 -X48_bit15 -X48_bit16 -X48_bit17 -X48_bit18 -X48_bit19 -X49_bit_10 X49_bit_9 -X49_bit_8 X49_bit_7 X49_bit_6 X49_bit_5 X49_bit_4 X49_bit_3 X49_bit_2 -X49_bit_1 -X49_bit0 -X49_bit1 -X49_bit2 -X49_bit3 -X49_bit4 -X49_bit5 -X49_bit6 -X49_bit7 -X49_bit8 -X49_bit9 -X49_bit10 -X49_bit11 -X49_bit12 -X49_bit13 -X49_bit14 -X49_bit15 -X49_bit16 -X49_bit17 -X49_bit18 -X49_bit19 -X50_bit_10 -X50_bit_9 -X50_bit_8 -X50_bit_7 -X50_bit_6 -X50_bit_5 -X50_bit_4 -X50_bit_3 -X50_bit_2 -X50_bit_1 -X50_bit0 -X50_bit1 -X50_bit2 -X50_bit3 -X50_bit4 -X50_bit5 -X50_bit6 -X50_bit7 -X50_bit8 -X50_bit9 -X50_bit10 -X50_bit11 -X50_bit12 -X50_bit13 -X50_bit14 -X50_bit15 -X50_bit16 -X50_bit17 -X50_bit18 -X50_bit19 -X51_bit_10 -X51_bit_9 X51_bit_8 -X51_bit_7 X51_bit_6 X51_bit_5 X51_bit_4 -X51_bit_3 X51_bit_2 X51_bit_1 -X51_bit0 -X51_bit1 -X51_bit2 -X51_bit3 -X51_bit4 -X51_bit5 -X51_bit6 -X51_bit7 -X51_bit8 -X51_bit9 -X51_bit10 -X51_bit11 -X51_bit12 -X51_bit13 -X51_bit14 -X51_bit15 -X51_bit16 -X51_bit17 -X51_bit18 -X51_bit19 -X52_bit_10 -X52_bit_9 -X52_bit_8 -X52_bit_7 -X52_bit_6 -X52_bit_5 -X52_bit_4 -X52_bit_3 -X52_bit_2 -X52_bit_1 -X52_bit0 -X52_bit1 -X52_bit2 -X52_bit3 -X52_bit4 -X52_bit5 -X52_bit6 -X52_bit7 -X52_bit8 -X52_bit9 -X52_bit10 -X52_bit11 -X52_bit12 -X52_bit13 -X52_bit14 -X52_bit15 -X52_bit16 -X52_bit17 -X52_bit18 -X52_bit19 -X53_bit_10 -X53_bit_9 -X53_bit_8 -X53_bit_7 -X53_bit_6 -X53_bit_5 -X53_bit_4 -X53_bit_3 -X53_bit_2 -X53_bit_1 -X53_bit0 -X53_bit1 -X53_bit2 -X53_bit3 -X53_bit4 -X53_bit5 -X53_bit6 -X53_bit7 -X53_bit8 -X53_bit9 -X53_bit10 -X53_bit11 -X53_bit12 -X53_bit13 -X53_bit14 -X53_bit15 -X53_bit16 -X53_bit17 -X53_bit18 -X53_bit19 -X54_bit_10 -X54_bit_9 -X54_bit_8 -X54_bit_7 -X54_bit_6 -X54_bit_5 -X54_bit_4 -X54_bit_3 -X54_bit_2 -X54_bit_1 -X54_bit0 -X54_bit1 -X54_bit2 -X54_bit3 -X54_bit4 -X54_bit5 -X54_bit6 -X54_bit7 -X54_bit8 -X54_bit9 -X54_bit10 -X54_bit11 -X54_bit12 -X54_bit13 -X54_bit14 -X54_bit15 -X54_bit16 -X54_bit17 -X54_bit18 -X54_bit19 X55_bit_10 -X55_bit_9 -X55_bit_8 -X55_bit_7 -X55_bit_6 -X55_bit_5 -X55_bit_4 -X55_bit_3 -X55_bit_2 -X55_bit_1 -X55_bit0 -X55_bit1 -X55_bit2 -X55_bit3 -X55_bit4 -X55_bit5 -X55_bit6 -X55_bit7 -X55_bit8 -X55_bit9 -X55_bit10 -X55_bit11 -X55_bit12 -X55_bit13 -X55_bit14 -X55_bit15 -X55_bit16 -X55_bit17 -X55_bit18 -X55_bit19 -X56_bit_10 -X56_bit_9 -X56_bit_8 -X56_bit_7 -X56_bit_6 -X56_bit_5 -X56_bit_4 -X56_bit_3 -X56_bit_2 -X56_bit_1 -X56_bit0 -X56_bit1 -X56_bit2 -X56_bit3 -X56_bit4 -X56_bit5 -X56_bit6 -X56_bit7 -X56_bit8 -X56_bit9 -X56_bit10 -X56_bit11 -X56_bit12 -X56_bit13 -X56_bit14 -X56_bit15 -X56_bit16 -X56_bit17 -X56_bit18 -X56_bit19 -X57_bit_10 -X57_bit_9 -X57_bit_8 -X57_bit_7 -X57_bit_6 -X57_bit_5 -X57_bit_4 -X57_bit_3 -X57_bit_2 -X57_bit_1 -X57_bit0 -X57_bit1 -X57_bit2 -X57_bit3 -X57_bit4 -X57_bit5 -X57_bit6 -X57_bit7 -X57_bit8 -X57_bit9 -X57_bit10 -X57_bit11 -X57_bit12 -X57_bit13 -X57_bit14 -X57_bit15 -X57_bit16 -X57_bit17 -X57_bit18 -X57_bit19 -X58_bit_10 -X58_bit_9 -X58_bit_8 -X58_bit_7 -X58_bit_6 -X58_bit_5 -X58_bit_4 -X58_bit_3 -X58_bit_2 -X58_bit_1 -X58_bit0 -X58_bit1 -X58_bit2 -X58_bit3 -X58_bit4 -X58_bit5 -X58_bit6 -X58_bit7 -X58_bit8 -X58_bit9 -X58_bit10 -X58_bit11 -X58_bit12 -X58_bit13 -X58_bit14 -X58_bit15 -X58_bit16 -X58_bit17 -X58_bit18 -X58_bit19 X59_bit_10 X59_bit_9 -X59_bit_8 X59_bit_7 -X59_bit_6 -X59_bit_5 -X59_bit_4 X59_bit_3 -X59_bit_2 -X59_bit_1 -X59_bit0 -X59_bit1 -X59_bit2 -X59_bit3 -X59_bit4 -X59_bit5 -X59_bit6 -X59_bit7 -X59_bit8 -X59_bit9 -X59_bit10 -X59_bit11 -X59_bit12 -X59_bit13 -X59_bit14 -X59_bit15 -X59_bit16 -X59_bit17 -X59_bit18 -X59_bit19 -X60_bit_10 -X60_bit_9 -X60_bit_8 -X60_bit_7 -X60_bit_6 -X60_bit_5 -X60_bit_4 -X60_bit_3 -X60_bit_2 -X60_bit_1 -X60_bit0 -X60_bit1 -X60_bit2 -X60_bit3 -X60_bit4 -X60_bit5 -X60_bit6 -X60_bit7 -X60_bit8 -X60_bit9 -X60_bit10 -X60_bit11 -X60_bit12 -X60_bit13 -X60_bit14 -X60_bit15 -X60_bit16 -X60_bit17 -X60_bit18 -X60_bit19 -X61_bit_10 -X61_bit_9 -X61_bit_8 -X61_bit_7 -X61_bit_6 -X61_bit_5 -X61_bit_4 -X61_bit_3 -X61_bit_2 -X61_bit_1 -X61_bit0 -X61_bit1 -X61_bit2 -X61_bit3 -X61_bit4 -X61_bit5 -X61_bit6 -X61_bit7 -X61_bit8 -X61_bit9 -X61_bit10 -X61_bit11 -X61_bit12 -X61_bit13 -X61_bit14 -X61_bit15 -X61_bit16 -X61_bit17 -X61_bit18 -X61_bit19 X62_bit_10 X62_bit_9 X62_bit_8 X62_bit_7 X62_bit_6 X62_bit_5 -X62_bit_4 -X62_bit_3 -X62_bit_2 -X62_bit_1 -X62_bit0 -X62_bit1 -X62_bit2 -X62_bit3 -X62_bit4 -X62_bit5 -X62_bit6 -X62_bit7 -X62_bit8 -X62_bit9 -X62_bit10 -X62_bit11 -X62_bit12 -X62_bit13 -X62_bit14 -X62_bit15 -X62_bit16 -X62_bit17 -X62_bit18 -X62_bit19 X63_bit_10 X63_bit_9 X63_bit_8 X63_bit_7 X63_bit_6 X63_bit_5 X63_bit_4 X63_bit_3 -X63_bit_2 X63_bit_1 X63_bit0 -X63_bit1 -X63_bit2 X63_bit3 -X63_bit4 -X63_bit5 -X63_bit6 -X63_bit7 -X63_bit8 -X63_bit9 -X63_bit10 -X63_bit11 -X63_bit12 -X63_bit13 -X63_bit14 -X63_bit15 -X63_bit16 -X63_bit17 -X63_bit18 -X63_bit19 -X64_bit_10 -X64_bit_9 -X64_bit_8 -X64_bit_7 -X64_bit_6 -X64_bit_5 -X64_bit_4 -X64_bit_3 -X64_bit_2 -X64_bit_1 -X64_bit0 -X64_bit1 -X64_bit2 -X64_bit3 -X64_bit4 -X64_bit5 -X64_bit6 -X64_bit7 -X64_bit8 -X64_bit9 -X64_bit10 -X64_bit11 -X64_bit12 -X64_bit13 -X64_bit14 -X64_bit15 -X64_bit16 -X64_bit17 -X64_bit18 -X64_bit19 X65_bit_10 X65_bit_9 X65_bit_8 X65_bit_7 X65_bit_6 X65_bit_5 X65_bit_4 -X65_bit_3 X65_bit_2 -X65_bit_1 -X65_bit0 -X65_bit1 -X65_bit2 -X65_bit3 -X65_bit4 -X65_bit5 -X65_bit6 -X65_bit7 -X65_bit8 -X65_bit9 -X65_bit10 -X65_bit11 -X65_bit12 -X65_bit13 -X65_bit14 -X65_bit15 -X65_bit16 -X65_bit17 -X65_bit18 -X65_bit19 -X66_bit_10 -X66_bit_9 -X66_bit_8 -X66_bit_7 X66_bit_6 X66_bit_5 -X66_bit_4 -X66_bit_3 -X66_bit_2 -X66_bit_1 -X66_bit0 X66_bit1 -X66_bit2 -X66_bit3 -X66_bit4 -X66_bit5 -X66_bit6 -X66_bit7 -X66_bit8 -X66_bit9 -X66_bit10 -X66_bit11 -X66_bit12 -X66_bit13 -X66_bit14 -X66_bit15 -X66_bit16 -X66_bit17 -X66_bit18 -X66_bit19 -X67_bit_10 X67_bit_9 X67_bit_8 X67_bit_7 X67_bit_6 -X67_bit_5 X67_bit_4 X67_bit_3 X67_bit_2 -X67_bit_1 -X67_bit0 X67_bit1 -X67_bit2 -X67_bit3 -X67_bit4 -X67_bit5 -X67_bit6 -X67_bit7 -X67_bit8 -X67_bit9 -X67_bit10 -X67_bit11 -X67_bit12 -X67_bit13 -X67_bit14 -X67_bit15 -X67_bit16 -X67_bit17 -X67_bit18 -X67_bit19 -X68_bit_10 X68_bit_9 X68_bit_8 X68_bit_7 X68_bit_6 X68_bit_5 X68_bit_4 X68_bit_3 -X68_bit_2 -X68_bit_1 -X68_bit0 -X68_bit1 -X68_bit2 -X68_bit3 -X68_bit4 -X68_bit5 -X68_bit6 -X68_bit7 -X68_bit8 -X68_bit9 -X68_bit10 -X68_bit11 -X68_bit12 -X68_bit13 -X68_bit14 -X68_bit15 -X68_bit16 -X68_bit17 -X68_bit18 -X68_bit19 X69_bit_10 X69_bit_9 X69_bit_8 -X69_bit_7 X69_bit_6 X69_bit_5 -X69_bit_4 -X69_bit_3 -X69_bit_2 -X69_bit_1 -X69_bit0 -X69_bit1 -X69_bit2 -X69_bit3 -X69_bit4 -X69_bit5 -X69_bit6 -X69_bit7 -X69_bit8 -X69_bit9 -X69_bit10 -X69_bit11 -X69_bit12 -X69_bit13 -X69_bit14 -X69_bit15 -X69_bit16 -X69_bit17 -X69_bit18 -X69_bit19 X70_bit_10 X70_bit_9 X70_bit_8 -X70_bit_7 X70_bit_6 X70_bit_5 X70_bit_4 X70_bit_3 X70_bit_2 -X70_bit_1 -X70_bit0 -X70_bit1 -X70_bit2 -X70_bit3 -X70_bit4 -X70_bit5 -X70_bit6 -X70_bit7 -X70_bit8 -X70_bit9 -X70_bit10 -X70_bit11 -X70_bit12 -X70_bit13 -X70_bit14 -X70_bit15 -X70_bit16 -X70_bit17 -X70_bit18 -X70_bit19 -X71_bit_10 X71_bit_9 X71_bit_8 -X71_bit_7 X71_bit_6 X71_bit_5 X71_bit_4 X71_bit_3 -X71_bit_2 X71_bit_1 -X71_bit0 X71_bit1 -X71_bit2 -X71_bit3 -X71_bit4 -X71_bit5 -X71_bit6 -X71_bit7 -X71_bit8 -X71_bit9 -X71_bit10 -X71_bit11 -X71_bit12 -X71_bit13 -X71_bit14 -X71_bit15 -X71_bit16 -X71_bit17 -X71_bit18 -X71_bit19 -X72_bit_10 -X72_bit_9 X72_bit_8 -X72_bit_7 X72_bit_6 X72_bit_5 -X72_bit_4 -X72_bit_3 -X72_bit_2 -X72_bit_1 -X72_bit0 -X72_bit1 -X72_bit2 -X72_bit3 -X72_bit4 -X72_bit5 -X72_bit6 -X72_bit7 -X72_bit8 -X72_bit9 -X72_bit10 -X72_bit11 -X72_bit12 -X72_bit13 -X72_bit14 -X72_bit15 -X72_bit16 -X72_bit17 -X72_bit18 -X72_bit19 -X73_bit_10 X73_bit_9 X73_bit_8 X73_bit_7 X73_bit_6 X73_bit_5 X73_bit_4 X73_bit_3 -X73_bit_2 X73_bit_1 -X73_bit0 -X73_bit1 -X73_bit2 -X73_bit3 -X73_bit4 -X73_bit5 -X73_bit6 -X73_bit7 -X73_bit8 -X73_bit9 -X73_bit10 -X73_bit11 -X73_bit12 -X73_bit13 -X73_bit14 -X73_bit15 -X73_bit16 -X73_bit17 -X73_bit18 -X73_bit19 -X74_bit_10 -X74_bit_9 X74_bit_8 -X74_bit_7 -X74_bit_6 -X74_bit_5 -X74_bit_4 -X74_bit_3 -X74_bit_2 -X74_bit_1 X74_bit0 -X74_bit1 -X74_bit2 -X74_bit3 -X74_bit4 -X74_bit5 -X74_bit6 -X74_bit7 -X74_bit8 -X74_bit9 -X74_bit10 -X74_bit11 -X74_bit12 -X74_bit13 -X74_bit14 -X74_bit15 -X74_bit16 -X74_bit17 -X74_bit18 -X74_bit19 X75_bit_10 -X75_bit_9 X75_bit_8 -X75_bit_7 X75_bit_6 X75_bit_5 -X75_bit_4 X75_bit_3 X75_bit_2 X75_bit_1 -X75_bit0 -X75_bit1 -X75_bit2 -X75_bit3 -X75_bit4 -X75_bit5 -X75_bit6 -X75_bit7 -X75_bit8 -X75_bit9 -X75_bit10 -X75_bit11 -X75_bit12 -X75_bit13 -X75_bit14 -X75_bit15 -X75_bit16 -X75_bit17 -X75_bit18 -X75_bit19 -X76_bit_10 -X76_bit_9 -X76_bit_8 -X76_bit_7 -X76_bit_6 -X76_bit_5 -X76_bit_4 -X76_bit_3 -X76_bit_2 -X76_bit_1 -X76_bit0 -X76_bit1 -X76_bit2 -X76_bit3 -X76_bit4 -X76_bit5 -X76_bit6 -X76_bit7 -X76_bit8 -X76_bit9 -X76_bit10 -X76_bit11 -X76_bit12 -X76_bit13 -X76_bit14 -X76_bit15 -X76_bit16 -X76_bit17 -X76_bit18 -X76_bit19 X77_bit_10 -X77_bit_9 -X77_bit_8 -X77_bit_7 X77_bit_6 -X77_bit_5 X77_bit_4 X77_bit_3 X77_bit_2 -X77_bit_1 -X77_bit0 -X77_bit1 -X77_bit2 -X77_bit3 -X77_bit4 -X77_bit5 -X77_bit6 -X77_bit7 -X77_bit8 -X77_bit9 -X77_bit10 -X77_bit11 -X77_bit12 -X77_bit13 -X77_bit14 -X77_bit15 -X77_bit16 -X77_bit17 -X77_bit18 -X77_bit19 -X78_bit_10 -X78_bit_9 -X78_bit_8 -X78_bit_7 -X78_bit_6 -X78_bit_5 -X78_bit_4 -X78_bit_3 -X78_bit_2 -X78_bit_1 -X78_bit0 -X78_bit1 -X78_bit2 -X78_bit3 -X78_bit4 -X78_bit5 -X78_bit6 -X78_bit7 -X78_bit8 -X78_bit9 -X78_bit10 -X78_bit11 -X78_bit12 -X78_bit13 -X78_bit14 -X78_bit15 -X78_bit16 -X78_bit17 -X78_bit18 -X78_bit19 X79_bit_10 X79_bit_9 X79_bit_8 -X79_bit_7 X79_bit_6 -X79_bit_5 X79_bit_4 -X79_bit_3 -X79_bit_2 X79_bit_1 -X79_bit0 -X79_bit1 -X79_bit2 -X79_bit3 -X79_bit4 -X79_bit5 -X79_bit6 -X79_bit7 -X79_bit8 -X79_bit9 -X79_bit10 -X79_bit11 -X79_bit12 -X79_bit13 -X79_bit14 -X79_bit15 -X79_bit16 -X79_bit17 -X79_bit18 -X79_bit19 X80_bit_10 X80_bit_9 X80_bit_8 X80_bit_7 X80_bit_6 -X80_bit_5 -X80_bit_4 X80_bit_3 -X80_bit_2 X80_bit_1 -X80_bit0 -X80_bit1 -X80_bit2 -X80_bit3 -X80_bit4 -X80_bit5 -X80_bit6 -X80_bit7 -X80_bit8 -X80_bit9 -X80_bit10 -X80_bit11 -X80_bit12 -X80_bit13 -X80_bit14 -X80_bit15 -X80_bit16 -X80_bit17 -X80_bit18 -X80_bit19 -X81_bit_10 -X81_bit_9 -X81_bit_8 -X81_bit_7 -X81_bit_6 -X81_bit_5 -X81_bit_4 -X81_bit_3 -X81_bit_2 -X81_bit_1 -X81_bit0 -X81_bit1 -X81_bit2 -X81_bit3 -X81_bit4 -X81_bit5 -X81_bit6 -X81_bit7 -X81_bit8 -X81_bit9 -X81_bit10 -X81_bit11 -X81_bit12 -X81_bit13 -X81_bit14 -X81_bit15 -X81_bit16 -X81_bit17 -X81_bit18 -X81_bit19 X82_bit_10 X82_bit_9 X82_bit_8 -X82_bit_7 X82_bit_6 X82_bit_5 -X82_bit_4 -X82_bit_3 -X82_bit_2 -X82_bit_1 -X82_bit0 -X82_bit1 -X82_bit2 -X82_bit3 -X82_bit4 -X82_bit5 -X82_bit6 -X82_bit7 -X82_bit8 -X82_bit9 -X82_bit10 -X82_bit11 -X82_bit12 -X82_bit13 -X82_bit14 -X82_bit15 -X82_bit16 -X82_bit17 -X82_bit18 -X82_bit19 -X83_bit_10 -X83_bit_9 -X83_bit_8 -X83_bit_7 -X83_bit_6 -X83_bit_5 X83_bit_4 -X83_bit_3 -X83_bit_2 -X83_bit_1 -X83_bit0 -X83_bit1 -X83_bit2 -X83_bit3 -X83_bit4 -X83_bit5 -X83_bit6 -X83_bit7 -X83_bit8 -X83_bit9 -X83_bit10 -X83_bit11 -X83_bit12 -X83_bit13 -X83_bit14 -X83_bit15 -X83_bit16 -X83_bit17 -X83_bit18 -X83_bit19 -X84_bit_10 -X84_bit_9 X84_bit_8 -X84_bit_7 -X84_bit_6 X84_bit_5 -X84_bit_4 -X84_bit_3 -X84_bit_2 -X84_bit_1 -X84_bit0 -X84_bit1 -X84_bit2 -X84_bit3 -X84_bit4 -X84_bit5 -X84_bit6 -X84_bit7 -X84_bit8 -X84_bit9 -X84_bit10 -X84_bit11 -X84_bit12 -X84_bit13 -X84_bit14 -X84_bit15 -X84_bit16 -X84_bit17 -X84_bit18 -X84_bit19 -X85_bit_10 -X85_bit_9 -X85_bit_8 -X85_bit_7 -X85_bit_6 -X85_bit_5 -X85_bit_4 -X85_bit_3 -X85_bit_2 -X85_bit_1 -X85_bit0 -X85_bit1 -X85_bit2 -X85_bit3 -X85_bit4 -X85_bit5 -X85_bit6 -X85_bit7 -X85_bit8 -X85_bit9 -X85_bit10 -X85_bit11 -X85_bit12 -X85_bit13 -X85_bit14 -X85_bit15 -X85_bit16 -X85_bit17 -X85_bit18 -X85_bit19 -X86_bit_10 -X86_bit_9 -X86_bit_8 X86_bit_7 -X86_bit_6 -X86_bit_5 -X86_bit_4 -X86_bit_3 -X86_bit_2 -X86_bit_1 X86_bit0 X86_bit1 -X86_bit2 -X86_bit3 -X86_bit4 -X86_bit5 -X86_bit6 -X86_bit7 -X86_bit8 -X86_bit9 -X86_bit10 -X86_bit11 -X86_bit12 -X86_bit13 -X86_bit14 -X86_bit15 -X86_bit16 -X86_bit17 -X86_bit18 -X86_bit19 -X87_bit_10 -X87_bit_9 -X87_bit_8 -X87_bit_7 -X87_bit_6 -X87_bit_5 X87_bit_4 -X87_bit_3 -X87_bit_2 -X87_bit_1 -X87_bit0 X87_bit1 X87_bit2 -X87_bit3 -X87_bit4 -X87_bit5 -X87_bit6 -X87_bit7 -X87_bit8 -X87_bit9 -X87_bit10 -X87_bit11 -X87_bit12 -X87_bit13 -X87_bit14 -X87_bit15 -X87_bit16 -X87_bit17 -X87_bit18 -X87_bit19 -X88_bit_10 X88_bit_9 X88_bit_8 X88_bit_7 X88_bit_6 X88_bit_5 X88_bit_4 -X88_bit_3 -X88_bit_2 -X88_bit_1 X88_bit0 -X88_bit1 -X88_bit2 -X88_bit3 -X88_bit4 -X88_bit5 -X88_bit6 -X88_bit7 -X88_bit8 -X88_bit9 -X88_bit10 -X88_bit11 -X88_bit12 -X88_bit13 -X88_bit14 -X88_bit15 -X88_bit16 -X88_bit17 -X88_bit18 -X88_bit19 -X89_bit_10 -X89_bit_9 -X89_bit_8 -X89_bit_7 -X89_bit_6 -X89_bit_5 -X89_bit_4 -X89_bit_3 -X89_bit_2 -X89_bit_1 -X89_bit0 -X89_bit1 -X89_bit2 -X89_bit3 -X89_bit4 -X89_bit5 -X89_bit6 -X89_bit7 -X89_bit8 -X89_bit9 -X89_bit10 -X89_bit11 -X89_bit12 -X89_bit13 -X89_bit14 -X89_bit15 -X89_bit16 -X89_bit17 -X89_bit18 -X89_bit19 X90_bit_10 X90_bit_9 X90_bit_8 X90_bit_7 X90_bit_6 -X90_bit_5 -X90_bit_4 X90_bit_3 -X90_bit_2 -X90_bit_1 -X90_bit0 -X90_bit1 -X90_bit2 -X90_bit3 -X90_bit4 -X90_bit5 -X90_bit6 -X90_bit7 -X90_bit8 -X90_bit9 -X90_bit10 -X90_bit11 -X90_bit12 -X90_bit13 -X90_bit14 -X90_bit15 -X90_bit16 -X90_bit17 -X90_bit18 -X90_bit19 -X91_bit_10 -X91_bit_9 -X91_

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/26996/stat): 26996 (minisat+_script) R 26995 26996 9102 0 -1 0 19 0 0 0 0 0 0 0 22 0 1 0 1852021814 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 1 0 0
Raw data (/proc/26996/statm): 174 3 169 147 0 27 0
[pid=26996] 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=26997
New process pid=26998
New process pid=26999
execve syscall for /bin/sed executable
One traced child (pid=26998) 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=26999) exited with status: 0
One traced child (pid=26997) exited with status: 0
New process pid=27000
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc31/normalized-mps-v2-20-10-ran10x10c.opb

[startup+10.0044 s]
Raw data (loadavg): 0.93 0.98 0.91 2/58 27000
Raw data (/proc/26996/stat): 26996 (minisat+_script) S 26995 26996 9102 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1852021814 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26996/statm): 531 226 485 147 0 384 0
[pid=26996] vsize: 2124
Raw data (/proc/27000/stat): 27000 (minisat+_64-bit) R 26996 26996 9102 0 -1 0 3385 0 0 0 969 12 0 0 25 0 1 0 1852021819 15757312 3269 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27000/statm): 3847 3269 145 145 0 3702 0
[pid=27000] vsize: 15388
Current children cumulated CPU time (s) 9.83
Current children cumulated vsize (Kb) 17512

[startup+20.0053 s]
Raw data (loadavg): 0.94 0.98 0.91 2/58 27002
Raw data (/proc/26996/stat): 26996 (minisat+_script) S 26995 26996 9102 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1852021814 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26996/statm): 531 226 485 147 0 384 0
[pid=26996] vsize: 2124
Raw data (/proc/27000/stat): 27000 (minisat+_64-bit) R 26996 26996 9102 0 -1 0 3488 0 0 0 1966 14 0 0 25 0 1 0 1852021819 16203776 3372 4294967295 134512640 135094434 3221224432 3221223056 134562104 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27000/statm): 3956 3372 145 145 0 3811 0
[pid=27000] vsize: 15824
Current children cumulated CPU time (s) 19.82
Current children cumulated vsize (Kb) 17948

[startup+30.0072 s]
Raw data (loadavg): 0.95 0.98 0.91 2/58 27002
Raw data (/proc/26996/stat): 26996 (minisat+_script) S 26995 26996 9102 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1852021814 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26996/statm): 531 226 485 147 0 384 0
[pid=26996] vsize: 2124
Raw data (/proc/27000/stat): 27000 (minisat+_64-bit) R 26996 26996 9102 0 -1 0 3665 0 0 0 2964 15 0 0 25 0 1 0 1852021819 16900096 3549 4294967295 134512640 135094434 3221224432 3221223104 134553523 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27000/statm): 4126 3549 145 145 0 3981 0
[pid=27000] vsize: 16504
Current children cumulated CPU time (s) 29.81
Current children cumulated vsize (Kb) 18628

[startup+40.0082 s]
Raw data (loadavg): 0.96 0.98 0.91 2/58 27002
Raw data (/proc/26996/stat): 26996 (minisat+_script) S 26995 26996 9102 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1852021814 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26996/statm): 531 226 485 147 0 384 0
[pid=26996] vsize: 2124
Raw data (/proc/27000/stat): 27000 (minisat+_64-bit) R 26996 26996 9102 0 -1 0 6918 0 0 0 3944 27 0 0 25 0 1 0 1852021819 28262400 6192 4294967295 134512640 135094434 3221224432 3221223044 134563089 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27000/statm): 6900 6192 145 145 0 6755 0
[pid=27000] vsize: 27600
Current children cumulated CPU time (s) 39.73
Current children cumulated vsize (Kb) 29724

[startup+50.0101 s]
Raw data (loadavg): 0.96 0.98 0.91 2/58 27002
Raw data (/proc/26996/stat): 26996 (minisat+_script) S 26995 26996 9102 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1852021814 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26996/statm): 531 226 485 147 0 384 0
[pid=26996] vsize: 2124
Raw data (/proc/27000/stat): 27000 (minisat+_64-bit) R 26996 26996 9102 0 -1 0 7114 0 0 0 4942 29 0 0 25 0 1 0 1852021819 28995584 6347 4294967295 134512640 135094434 3221224432 3221223024 134556862 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27000/statm): 7079 6347 145 145 0 6934 0
[pid=27000] vsize: 28316
Current children cumulated CPU time (s) 49.73
Current children cumulated vsize (Kb) 30440

[startup+60.011 s]
Raw data (loadavg): 0.97 0.98 0.91 2/58 27002
Raw data (/proc/26996/stat): 26996 (minisat+_script) S 26995 26996 9102 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1852021814 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26996/statm): 531 226 485 147 0 384 0
[pid=26996] vsize: 2124
Raw data (/proc/27000/stat): 27000 (minisat+_64-bit) R 26996 26996 9102 0 -1 0 7298 0 0 0 5939 31 0 0 25 0 1 0 1852021819 29724672 6531 4294967295 134512640 135094434 3221224432 3221223088 134557900 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27000/statm): 7257 6531 145 145 0 7112 0
[pid=27000] vsize: 29028
Current children cumulated CPU time (s) 59.72
Current children cumulated vsize (Kb) 31152

[startup+70.0119 s]
Raw data (loadavg): 0.97 0.98 0.91 2/58 27002
Raw data (/proc/26996/stat): 26996 (minisat+_script) S 26995 26996 9102 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1852021814 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26996/statm): 531 226 485 147 0 384 0
[pid=26996] vsize: 2124
Raw data (/proc/27000/stat): 27000 (minisat+_64-bit) R 26996 26996 9102 0 -1 0 7588 0 0 0 6932 33 0 0 25 0 1 0 1852021819 30900224 6821 4294967295 134512640 135094434 3221224432 3221223080 134539489 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27000/statm): 7544 6821 145 145 0 7399 0
[pid=27000] vsize: 30176
Current children cumulated CPU time (s) 69.67
Current children cumulated vsize (Kb) 32300

[startup+80.0138 s]
Raw data (loadavg): 0.98 0.98 0.91 2/58 27004
Raw data (/proc/26996/stat): 26996 (minisat+_script) S 26995 26996 9102 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1852021814 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26996/statm): 531 226 485 147 0 384 0
[pid=26996] vsize: 2124
Raw data (/proc/27000/stat): 27000 (minisat+_64-bit) R 26996 26996 9102 0 -1 0 7843 0 0 0 7929 35 0 0 25 0 1 0 1852021819 31760384 7036 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27000/statm): 7754 7036 145 145 0 7609 0
[pid=27000] vsize: 31016
Current children cumulated CPU time (s) 79.66
Current children cumulated vsize (Kb) 33140

[startup+90.0148 s]
Raw data (loadavg): 0.98 0.98 0.91 2/58 27004
Raw data (/proc/26996/stat): 26996 (minisat+_script) S 26995 26996 9102 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1852021814 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26996/statm): 531 226 485 147 0 384 0
[pid=26996] vsize: 2124
Raw data (/proc/27000/stat): 27000 (minisat+_64-bit) R 26996 26996 9102 0 -1 0 8093 0 0 0 8924 37 0 0 25 0 1 0 1852021819 32776192 7286 4294967295 134512640 135094434 3221224432 3221223120 134554723 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27000/statm): 8002 7286 145 145 0 7857 0
[pid=27000] vsize: 32008
Current children cumulated CPU time (s) 89.63
Current children cumulated vsize (Kb) 34132

[startup+100.016 s]
Raw data (loadavg): 0.98 0.98 0.91 2/58 27004
Raw data (/proc/26996/stat): 26996 (minisat+_script) S 26995 26996 9102 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1852021814 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26996/statm): 531 226 485 147 0 384 0
[pid=26996] vsize: 2124
Raw data (/proc/27000/stat): 27000 (minisat+_64-bit) R 26996 26996 9102 0 -1 0 8260 0 0 0 9920 39 0 0 25 0 1 0 1852021819 33456128 7453 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27000/statm): 8168 7453 145 145 0 8023 0
[pid=27000] vsize: 32672
Current children cumulated CPU time (s) 99.61
Current children cumulated vsize (Kb) 34796

[startup+110.017 s]
Raw data (loadavg): 0.98 0.98 0.91 2/58 27004
Raw data (/proc/26996/stat): 26996 (minisat+_script) S 26995 26996 9102 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1852021814 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26996/statm): 531 226 485 147 0 384 0
[pid=26996] vsize: 2124
Raw data (/proc/27000/stat): 27000 (minisat+_64-bit) R 26996 26996 9102 0 -1 0 8459 0 0 0 10915 41 0 0 25 0 1 0 1852021819 34258944 7652 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27000/statm): 8364 7652 145 145 0 8219 0
[pid=27000] vsize: 33456
Current children cumulated CPU time (s) 109.58
Current children cumulated vsize (Kb) 35580

[startup+120.018 s]
Raw data (loadavg): 0.99 0.98 0.91 2/58 27004
Raw data (/proc/26996/stat): 26996 (minisat+_script) S 26995 26996 9102 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1852021814 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26996/statm): 531 226 485 147 0 384 0
[pid=26996] vsize: 2124
Raw data (/proc/27000/stat): 27000 (minisat+_64-bit) R 26996 26996 9102 0 -1 0 8809 0 0 0 11910 43 0 0 25 0 1 0 1852021819 35667968 8002 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27000/statm): 8708 8002 145 145 0 8563 0
[pid=27000] vsize: 34832
Current children cumulated CPU time (s) 119.55
Current children cumulated vsize (Kb) 36956

[startup+130.018 s]
Raw data (loadavg): 0.99 0.98 0.91 2/58 27004
Raw data (/proc/26996/stat): 26996 (minisat+_script) S 26995 26996 9102 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1852021814 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26996/statm): 531 226 485 147 0 384 0
[pid=26996] vsize: 2124
Raw data (/proc/27000/stat): 27000 (minisat+_64-bit) R 26996 26996 9102 0 -1 0 9373 0 0 0 12902 46 0 0 25 0 1 0 1852021819 38223872 8566 4294967295 134512640 135094434 3221224432 3221223024 134557389 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27000/statm): 9332 8566 145 145 0 9187 0
[pid=27000] vsize: 37328
Current children cumulated CPU time (s) 129.5
Current children cumulated vsize (Kb) 39452

[startup+140.019 s]
Raw data (loadavg): 0.99 0.98 0.91 2/58 27006
Raw data (/proc/26996/stat): 26996 (minisat+_script) S 26995 26996 9102 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1852021814 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26996/statm): 531 226 485 147 0 384 0
[pid=26996] vsize: 2124
Raw data (/proc/27000/stat): 27000 (minisat+_64-bit) R 26996 26996 9102 0 -1 0 9756 0 0 0 13896 49 0 0 25 0 1 0 1852021819 39620608 8908 4294967295 134512640 135094434 3221224432 3221223044 134563055 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27000/statm): 9673 8908 145 145 0 9528 0
[pid=27000] vsize: 38692
Current children cumulated CPU time (s) 139.47
Current children cumulated vsize (Kb) 40816

[startup+150.021 s]
Raw data (loadavg): 0.99 0.98 0.91 2/58 27006
Raw data (/proc/26996/stat): 26996 (minisat+_script) S 26995 26996 9102 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1852021814 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26996/statm): 531 226 485 147 0 384 0
[pid=26996] vsize: 2124
Raw data (/proc/27000/stat): 27000 (minisat+_64-bit) R 26996 26996 9102 0 -1 0 9757 0 0 0 14896 49 0 0 25 0 1 0 1852021819 39620608 8909 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27000/statm): 9673 8909 145 145 0 9528 0
[pid=27000] vsize: 38692
Current children cumulated CPU time (s) 149.47
Current children cumulated vsize (Kb) 40816

[startup+160.022 s]
Raw data (loadavg): 0.99 0.98 0.91 2/58 27006
Raw data (/proc/26996/stat): 26996 (minisat+_script) S 26995 26996 9102 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1852021814 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26996/statm): 531 226 485 147 0 384 0
[pid=26996] vsize: 2124
Raw data (/proc/27000/stat): 27000 (minisat+_64-bit) R 26996 26996 9102 0 -1 0 9758 0 0 0 15897 49 0 0 25 0 1 0 1852021819 39620608 8910 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27000/statm): 9673 8910 145 145 0 9528 0
[pid=27000] vsize: 38692
Current children cumulated CPU time (s) 159.48
Current children cumulated vsize (Kb) 40816

[startup+170.022 s]
Raw data (loadavg): 0.99 0.98 0.91 2/58 27006
Raw data (/proc/26996/stat): 26996 (minisat+_script) S 26995 26996 9102 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1852021814 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26996/statm): 531 226 485 147 0 384 0
[pid=26996] vsize: 2124
Raw data (/proc/27000/stat): 27000 (minisat+_64-bit) R 26996 26996 9102 0 -1 0 9758 0 0 0 16897 49 0 0 25 0 1 0 1852021819 39620608 8910 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27000/statm): 9673 8910 145 145 0 9528 0
[pid=27000] vsize: 38692
Current children cumulated CPU time (s) 169.48
Current children cumulated vsize (Kb) 40816

[startup+180.023 s]
Raw data (loadavg): 0.99 0.98 0.91 2/58 27006
Raw data (/proc/26996/stat): 26996 (minisat+_script) S 26995 26996 9102 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1852021814 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26996/statm): 531 226 485 147 0 384 0
[pid=26996] vsize: 2124
Raw data (/proc/27000/stat): 27000 (minisat+_64-bit) R 26996 26996 9102 0 -1 0 9758 0 0 0 17897 49 0 0 25 0 1 0 1852021819 39620608 8910 4294967295 134512640 135094434 3221224432 3221223120 134554728 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27000/statm): 9673 8910 145 145 0 9528 0
[pid=27000] vsize: 38692
Current children cumulated CPU time (s) 179.48
Current children cumulated vsize (Kb) 40816

[startup+190.024 s]
Raw data (loadavg): 0.99 0.98 0.91 2/58 27006
Raw data (/proc/26996/stat): 26996 (minisat+_script) S 26995 26996 9102 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1852021814 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26996/statm): 531 226 485 147 0 384 0
[pid=26996] vsize: 2124
Raw data (/proc/27000/stat): 27000 (minisat+_64-bit) R 26996 26996 9102 0 -1 0 9758 0 0 0 18897 49 0 0 25 0 1 0 1852021819 39620608 8910 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27000/statm): 9673 8910 145 145 0 9528 0
[pid=27000] vsize: 38692
Current children cumulated CPU time (s) 189.48
Current children cumulated vsize (Kb) 40816

[startup+200.025 s]
Raw data (loadavg): 0.99 0.98 0.91 2/58 27008
Raw data (/proc/26996/stat): 26996 (minisat+_script) S 26995 26996 9102 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1852021814 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26996/statm): 531 226 485 147 0 384 0
[pid=26996] vsize: 2124
Raw data (/proc/27000/stat): 27000 (minisat+_64-bit) R 26996 26996 9102 0 -1 0 9796 0 0 0 19897 50 0 0 25 0 1 0 1852021819 39763968 8948 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27000/statm): 9708 8948 145 145 0 9563 0
[pid=27000] vsize: 38832
Current children cumulated CPU time (s) 199.49
Current children cumulated vsize (Kb) 40956

[startup+210.026 s]
Raw data (loadavg): 0.99 0.98 0.91 2/58 27008
Raw data (/proc/26996/stat): 26996 (minisat+_script) S 26995 26996 9102 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1852021814 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26996/statm): 531 226 485 147 0 384 0
[pid=26996] vsize: 2124
Raw data (/proc/27000/stat): 27000 (minisat+_64-bit) R 26996 26996 9102 0 -1 0 10270 0 0 0 20890 52 0 0 25 0 1 0 1852021819 41705472 9422 4294967295 134512640 135094434 3221224432 3221223088 134557866 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27000/statm): 10182 9422 145 145 0 10037 0
[pid=27000] vsize: 40728
Current children cumulated CPU time (s) 209.44
Current children cumulated vsize (Kb) 42852

[startup+220.027 s]
Raw data (loadavg): 0.99 0.98 0.91 2/58 27008
Raw data (/proc/26996/stat): 26996 (minisat+_script) S 26995 26996 9102 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1852021814 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26996/statm): 531 226 485 147 0 384 0
[pid=26996] vsize: 2124
Raw data (/proc/27000/stat): 27000 (minisat+_64-bit) R 26996 26996 9102 0 -1 0 10425 0 0 0 21885 54 0 0 25 0 1 0 1852021819 42340352 9577 4294967295 134512640 135094434 3221224432 3221223044 134563151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27000/statm): 10337 9577 145 145 0 10192 0
[pid=27000] vsize: 41348
Current children cumulated CPU time (s) 219.41
Current children cumulated vsize (Kb) 43472

[startup+230.028 s]
Raw data (loadavg): 0.99 0.98 0.91 2/58 27008
Raw data (/proc/26996/stat): 26996 (minisat+_script) S 26995 26996 9102 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1852021814 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26996/statm): 531 226 485 147 0 384 0
[pid=26996] vsize: 2124
Raw data (/proc/27000/stat): 27000 (minisat+_64-bit) R 26996 26996 9102 0 -1 0 10725 0 0 0 22880 56 0 0 25 0 1 0 1852021819 43569152 9877 4294967295 134512640 135094434 3221224432 3221223088 134558176 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27000/statm): 10637 9877 145 145 0 10492 0
[pid=27000] vsize: 42548
Current children cumulated CPU time (s) 229.38
Current children cumulated vsize (Kb) 44672

[startup+240.029 s]
Raw data (loadavg): 0.99 0.98 0.91 2/58 27008
Raw data (/proc/26996/stat): 26996 (minisat+_script) S 26995 26996 9102 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1852021814 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26996/statm): 531 226 485 147 0 384 0
[pid=26996] vsize: 2124
Raw data (/proc/27000/stat): 27000 (minisat+_64-bit) R 26996 26996 9102 0 -1 0 10958 0 0 0 23876 58 0 0 25 0 1 0 1852021819 44527616 10110 4294967295 134512640 135094434 3221224432 3221223056 134557737 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27000/statm): 10871 10110 145 145 0 10726 0
[pid=27000] vsize: 43484
Current children cumulated CPU time (s) 239.36
Current children cumulated vsize (Kb) 45608

[startup+250.031 s]
Raw data (loadavg): 0.99 0.98 0.91 2/58 27008
Raw data (/proc/26996/stat): 26996 (minisat+_script) S 26995 26996 9102 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1852021814 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26996/statm): 531 226 485 147 0 384 0
[pid=26996] vsize: 2124
Raw data (/proc/27000/stat): 27000 (minisat+_64-bit) R 26996 26996 9102 0 -1 0 11199 0 0 0 24873 59 0 0 25 0 1 0 1852021819 45506560 10351 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27000/statm): 11110 10351 145 145 0 10965 0
[pid=27000] vsize: 44440
Current children cumulated CPU time (s) 249.34
Current children cumulated vsize (Kb) 46564

[startup+260.031 s]
Raw data (loadavg): 0.99 0.98 0.91 2/58 27010
Raw data (/proc/26996/stat): 26996 (minisat+_script) S 26995 26996 9102 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1852021814 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26996/statm): 531 226 485 147 0 384 0
[pid=26996] vsize: 2124
Raw data (/proc/27000/stat): 27000 (minisat+_64-bit) R 26996 26996 9102 0 -1 0 11429 0 0 0 25871 60 0 0 25 0 1 0 1852021819 46505984 10581 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27000/statm): 11354 10581 145 145 0 11209 0
[pid=27000] vsize: 45416
Current children cumulated CPU time (s) 259.33
Current children cumulated vsize (Kb) 47540

[startup+270.031 s]
Raw data (loadavg): 0.99 0.98 0.91 2/58 27010
Raw data (/proc/26996/stat): 26996 (minisat+_script) S 26995 26996 9102 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1852021814 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26996/statm): 531 226 485 147 0 384 0
[pid=26996] vsize: 2124
Raw data (/proc/27000/stat): 27000 (minisat+_64-bit) R 26996 26996 9102 0 -1 0 11679 0 0 0 26867 62 0 0 25 0 1 0 1852021819 47525888 10831 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27000/statm): 11603 10831 145 145 0 11458 0
[pid=27000] vsize: 46412
Current children cumulated CPU time (s) 269.31
Current children cumulated vsize (Kb) 48536

[startup+280.032 s]
Raw data (loadavg): 0.99 0.98 0.91 2/58 27010
Raw data (/proc/26996/stat): 26996 (minisat+_script) S 26995 26996 9102 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1852021814 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26996/statm): 531 226 485 147 0 384 0
[pid=26996] vsize: 2124
Raw data (/proc/27000/stat): 27000 (minisat+_64-bit) R 26996 26996 9102 0 -1 0 12009 0 0 0 27860 65 0 0 25 0 1 0 1852021819 48877568 11161 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27000/statm): 11933 11161 145 145 0 11788 0
[pid=27000] vsize: 47732
Current children cumulated CPU time (s) 279.27
Current children cumulated vsize (Kb) 49856

[startup+290.033 s]
Raw data (loadavg): 0.99 0.98 0.91 2/58 27010
Raw data (/proc/26996/stat): 26996 (minisat+_script) S 26995 26996 9102 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1852021814 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26996/statm): 531 226 485 147 0 384 0
[pid=26996] vsize: 2124
Raw data (/proc/27000/stat): 27000 (minisat+_64-bit) R 26996 26996 9102 0 -1 0 12351 0 0 0 28854 67 0 0 25 0 1 0 1852021819 50270208 11503 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27000/statm): 12273 11503 145 145 0 12128 0
[pid=27000] vsize: 49092
Current children cumulated CPU time (s) 289.23
Current children cumulated vsize (Kb) 51216

[startup+300.034 s]
Raw data (loadavg): 0.99 0.98 0.91 2/58 27010
Raw data (/proc/26996/stat): 26996 (minisat+_script) S 26995 26996 9102 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1852021814 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26996/statm): 531 226 485 147 0 384 0
[pid=26996] vsize: 2124
Raw data (/proc/27000/stat): 27000 (minisat+_64-bit) R 26996 26996 9102 0 -1 0 12688 0 0 0 29848 70 0 0 25 0 1 0 1852021819 51650560 11840 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27000/statm): 12610 11840 145 145 0 12465 0
[pid=27000] vsize: 50440
Current children cumulated CPU time (s) 299.2
Current children cumulated vsize (Kb) 52564

[startup+310.035 s]
Raw data (loadavg): 0.99 0.98 0.91 2/58 27010
Raw data (/proc/26996/stat): 26996 (minisat+_script) S 26995 26996 9102 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1852021814 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26996/statm): 531 226 485 147 0 384 0
[pid=26996] vsize: 2124
Raw data (/proc/27000/stat): 27000 (minisat+_64-bit) R 26996 26996 9102 0 -1 0 13054 0 0 0 30843 73 0 0 25 0 1 0 1852021819 52973568 12164 4294967295 134512640 135094434 3221224432 3221223084 134558255 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27000/statm): 12933 12164 145 145 0 12788 0
[pid=27000] vsize: 51732
Current children cumulated CPU time (s) 309.18
Current children cumulated vsize (Kb) 53856

[startup+320.035 s]
Raw data (loadavg): 0.99 0.98 0.91 2/58 27012
Raw data (/proc/26996/stat): 26996 (minisat+_script) S 26995 26996 9102 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1852021814 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26996/statm): 531 226 485 147 0 384 0
[pid=26996] vsize: 2124
Raw data (/proc/27000/stat): 27000 (minisat+_64-bit) R 26996 26996 9102 0 -1 0 13054 0 0 0 31844 73 0 0 25 0 1 0 1852021819 52973568 12164 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27000/statm): 12933 12164 145 145 0 12788 0
[pid=27000] vsize: 51732
Current children cumulated CPU time (s) 319.19
Current children cumulated vsize (Kb) 53856

[startup+330.037 s]
Raw data (loadavg): 0.99 0.98 0.91 2/58 27012
Raw data (/proc/26996/stat): 26996 (minisat+_script) S 26995 26996 9102 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1852021814 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26996/statm): 531 226 485 147 0 384 0
[pid=26996] vsize: 2124
Raw data (/proc/27000/stat): 27000 (minisat+_64-bit) R 26996 26996 9102 0 -1 0 13054 0 0 0 32844 73 0 0 25 0 1 0 1852021819 52973568 12164 4294967295 134512640 135094434 3221224432 3221223024 134556902 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27000/statm): 12933 12164 145 145 0 12788 0
[pid=27000] vsize: 51732
Current children cumulated CPU time (s) 329.19
Current children cumulated vsize (Kb) 53856

[startup+340.038 s]
Raw data (loadavg): 0.99 0.98 0.91 2/58 27012
Raw data (/proc/26996/stat): 26996 (minisat+_script) S 26995 26996 9102 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1852021814 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26996/statm): 531 226 485 147 0 384 0
[pid=26996] vsize: 2124
Raw data (/proc/27000/stat): 27000 (minisat+_64-bit) R 26996 26996 9102 0 -1 0 13054 0 0 0 33844 73 0 0 25 0 1 0 1852021819 52973568 12164 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27000/statm): 12933 12164 145 145 0 12788 0
[pid=27000] vsize: 51732
Current children cumulated CPU time (s) 339.19
Current children cumulated vsize (Kb) 53856

[startup+350.039 s]
Raw data (loadavg): 0.99 0.98 0.91 2/58 27012
Raw data (/proc/26996/stat): 26996 (minisat+_script) S 26995 26996 9102 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1852021814 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26996/statm): 531 226 485 147 0 384 0
[pid=26996] vsize: 2124
Raw data (/proc/27000/stat): 27000 (minisat+_64-bit) R 26996 26996 9102 0 -1 0 13054 0 0 0 34844 73 0 0 25 0 1 0 1852021819 52973568 12164 4294967295 134512640 135094434 3221224432 3221223056 134562104 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27000/statm): 12933 12164 145 145 0 12788 0
[pid=27000] vsize: 51732
Current children cumulated CPU time (s) 349.19
Current children cumulated vsize (Kb) 53856

[startup+360.04 s]
Raw data (loadavg): 0.99 0.98 0.91 2/58 27012
Raw data (/proc/26996/stat): 26996 (minisat+_script) S 26995 26996 9102 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1852021814 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26996/statm): 531 226 485 147 0 384 0
[pid=26996] vsize: 2124
Raw data (/proc/27000/stat): 27000 (minisat+_64-bit) R 26996 26996 9102 0 -1 0 13054 0 0 0 35844 73 0 0 25 0 1 0 1852021819 52973568 12164 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27000/statm): 12933 12164 145 145 0 12788 0
[pid=27000] vsize: 51732
Current children cumulated CPU time (s) 359.19
Current children cumulated vsize (Kb) 53856

[startup+370.041 s]
Raw data (loadavg): 0.99 0.98 0.91 2/58 27012
Raw data (/proc/26996/stat): 26996 (minisat+_script) S 26995 26996 9102 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1852021814 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26996/statm): 531 226 485 147 0 384 0
[pid=26996] vsize: 2124
Raw data (/proc/27000/stat): 27000 (minisat+_64-bit) R 26996 26996 9102 0 -1 0 13054 0 0 0 36845 73 0 0 25 0 1 0 1852021819 52973568 12164 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27000/statm): 12933 12164 145 145 0 12788 0
[pid=27000] vsize: 51732
Current children cumulated CPU time (s) 369.2
Current children cumulated vsize (Kb) 53856

[startup+380.042 s]
Raw data (loadavg): 0.99 0.98 0.91 2/58 27014
Raw data (/proc/26996/stat): 26996 (minisat+_script) S 26995 26996 9102 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1852021814 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26996/statm): 531 226 485 147 0 384 0
[pid=26996] vsize: 2124
Raw data (/proc/27000/stat): 27000 (minisat+_64-bit) R 26996 26996 9102 0 -1 0 13054 0 0 0 37845 73 0 0 25 0 1 0 1852021819 52973568 12164 4294967295 134512640 135094434 3221224432 3221223044 134563071 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27000/statm): 12933 12164 145 145 0 12788 0
[pid=27000] vsize: 51732
Current children cumulated CPU time (s) 379.2
Current children cumulated vsize (Kb) 53856

[startup+390.043 s]
Raw data (loadavg): 0.99 0.98 0.91 2/58 27014
Raw data (/proc/26996/stat): 26996 (minisat+_script) S 26995 26996 9102 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1852021814 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26996/statm): 531 226 485 147 0 384 0
[pid=26996] vsize: 2124
Raw data (/proc/27000/stat): 27000 (minisat+_64-bit) R 26996 26996 9102 0 -1 0 13054 0 0 0 38845 73 0 0 25 0 1 0 1852021819 52973568 12164 4294967295 134512640 135094434 3221224432 3221223056 134557565 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27000/statm): 12933 12164 145 145 0 12788 0
[pid=27000] vsize: 51732
Current children cumulated CPU time (s) 389.2
Current children cumulated vsize (Kb) 53856

[startup+400.044 s]
Raw data (loadavg): 0.99 0.98 0.91 2/58 27014
Raw data (/proc/26996/stat): 26996 (minisat+_script) S 26995 26996 9102 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1852021814 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26996/statm): 531 226 485 147 0 384 0
[pid=26996] vsize: 2124
Raw data (/proc/27000/stat): 27000 (minisat+_64-bit) R 26996 26996 9102 0 -1 0 13054 0 0 0 39845 73 0 0 25 0 1 0 1852021819 52973568 12164 4294967295 134512640 135094434 3221224432 3221223088 134557950 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27000/statm): 12933 12164 145 145 0 12788 0
[pid=27000] vsize: 51732
Current children cumulated CPU time (s) 399.2
Current children cumulated vsize (Kb) 53856

[startup+410.045 s]
Raw data (loadavg): 0.99 0.98 0.91 2/58 27014
Raw data (/proc/26996/stat): 26996 (minisat+_script) S 26995 26996 9102 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1852021814 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26996/statm): 531 226 485 147 0 384 0
[pid=26996] vsize: 2124
Raw data (/proc/27000/stat): 27000 (minisat+_64-bit) R 26996 26996 9102 0 -1 0 13054 0 0 0 40846 73 0 0 25 0 1 0 1852021819 52973568 12164 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27000/statm): 12933 12164 145 145 0 12788 0
[pid=27000] vsize: 51732
Current children cumulated CPU time (s) 409.21
Current children cumulated vsize (Kb) 53856

[startup+420.045 s]
Raw data (loadavg): 0.99 0.98 0.91 2/58 27014
Raw data (/proc/26996/stat): 26996 (minisat+_script) S 26995 26996 9102 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1852021814 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26996/statm): 531 226 485 147 0 384 0
[pid=26996] vsize: 2124
Raw data (/proc/27000/stat): 27000 (minisat+_64-bit) R 26996 26996 9102 0 -1 0 13054 0 0 0 41846 73 0 0 25 0 1 0 1852021819 52973568 12164 4294967295 134512640 135094434 3221224432 3221223088 134558007 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27000/statm): 12933 12164 145 145 0 12788 0
[pid=27000] vsize: 51732
Current children cumulated CPU time (s) 419.21
Current children cumulated vsize (Kb) 53856

[startup+430.047 s]
Raw data (loadavg): 0.99 0.98 0.91 2/58 27014
Raw data (/proc/26996/stat): 26996 (minisat+_script) S 26995 26996 9102 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1852021814 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26996/statm): 531 226 485 147 0 384 0
[pid=26996] vsize: 2124
Raw data (/proc/27000/stat): 27000 (minisat+_64-bit) R 26996 26996 9102 0 -1 0 13054 0 0 0 42846 73 0 0 25 0 1 0 1852021819 52973568 12164 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27000/statm): 12933 12164 145 145 0 12788 0
[pid=27000] vsize: 51732
Current children cumulated CPU time (s) 429.21
Current children cumulated vsize (Kb) 53856

[startup+440.048 s]
Raw data (loadavg): 0.99 0.98 0.91 2/58 27016
Raw data (/proc/26996/stat): 26996 (minisat+_script) S 26995 26996 9102 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1852021814 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26996/statm): 531 226 485 147 0 384 0
[pid=26996] vsize: 2124
Raw data (/proc/27000/stat): 27000 (minisat+_64-bit) R 26996 26996 9102 0 -1 0 13054 0 0 0 43846 73 0 0 25 0 1 0 1852021819 52973568 12164 4294967295 134512640 135094434 3221224432 3221223088 134557835 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27000/statm): 12933 12164 145 145 0 12788 0
[pid=27000] vsize: 51732
Current children cumulated CPU time (s) 439.21
Current children cumulated vsize (Kb) 53856

[startup+450.049 s]
Raw data (loadavg): 0.99 0.98 0.91 2/58 27016
Raw data (/proc/26996/stat): 26996 (minisat+_script) S 26995 26996 9102 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1852021814 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26996/statm): 531 226 485 147 0 384 0
[pid=26996] vsize: 2124
Raw data (/proc/27000/stat): 27000 (minisat+_64-bit) R 26996 26996 9102 0 -1 0 13054 0 0 0 44847 73 0 0 25 0 1 0 1852021819 52973568 12164 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27000/statm): 12933 12164 145 145 0 12788 0
[pid=27000] vsize: 51732
Current children cumulated CPU time (s) 449.22
Current children cumulated vsize (Kb) 53856

[startup+460.05 s]
Raw data (loadavg): 0.99 0.98 0.91 2/58 27016
Raw data (/proc/26996/stat): 26996 (minisat+_script) S 26995 26996 9102 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1852021814 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26996/statm): 531 226 485 147 0 384 0
[pid=26996] vsize: 2124
Raw data (/proc/27000/stat): 27000 (minisat+_64-bit) R 26996 26996 9102 0 -1 0 13055 0 0 0 45847 73 0 0 25 0 1 0 1852021819 52973568 12165 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27000/statm): 12933 12165 145 145 0 12788 0
[pid=27000] vsize: 51732
Current children cumulated CPU time (s) 459.22
Current children cumulated vsize (Kb) 53856

[startup+470.051 s]
Raw data (loadavg): 0.99 0.98 0.91 2/58 27016
Raw data (/proc/26996/stat): 26996 (minisat+_script) S 26995 26996 9102 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1852021814 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26996/statm): 531 226 485 147 0 384 0
[pid=26996] vsize: 2124
Raw data (/proc/27000/stat): 27000 (minisat+_64-bit) R 26996 26996 9102 0 -1 0 13055 0 0 0 46847 73 0 0 25 0 1 0 1852021819 52973568 12165 4294967295 134512640 135094434 3221224432 3221223024 134557350 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27000/statm): 12933 12165 145 145 0 12788 0
[pid=27000] vsize: 51732
Current children cumulated CPU time (s) 469.22
Current children cumulated vsize (Kb) 53856

[startup+480.052 s]
Raw data (loadavg): 0.99 0.98 0.91 2/58 27016
Raw data (/proc/26996/stat): 26996 (minisat+_script) S 26995 26996 9102 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1852021814 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26996/statm): 531 226 485 147 0 384 0
[pid=26996] vsize: 2124
Raw data (/proc/27000/stat): 27000 (minisat+_64-bit) R 26996 26996 9102 0 -1 0 13055 0 0 0 47848 73 0 0 25 0 1 0 1852021819 52973568 12165 4294967295 134512640 135094434 3221224432 3221223084 134558255 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27000/statm): 12933 12165 145 145 0 12788 0
[pid=27000] vsize: 51732
Current children cumulated CPU time (s) 479.23
Current children cumulated vsize (Kb) 53856

[startup+490.053 s]
Raw data (loadavg): 0.99 0.98 0.91 2/58 27016
Raw data (/proc/26996/stat): 26996 (minisat+_script) S 26995 26996 9102 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1852021814 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26996/statm): 531 226 485 147 0 384 0
[pid=26996] vsize: 2124
Raw data (/proc/27000/stat): 27000 (minisat+_64-bit) R 26996 26996 9102 0 -1 0 13060 0 0 0 48848 73 0 0 25 0 1 0 1852021819 52973568 12170 4294967295 134512640 135094434 3221224432 3221223024 134557117 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27000/statm): 12933 12170 145 145 0 12788 0
[pid=27000] vsize: 51732
Current children cumulated CPU time (s) 489.23
Current children cumulated vsize (Kb) 53856

[startup+500.055 s]
Raw data (loadavg): 0.99 0.98 0.91 2/58 27018
Raw data (/proc/26996/stat): 26996 (minisat+_script) S 26995 26996 9102 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1852021814 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26996/statm): 531 226 485 147 0 384 0
[pid=26996] vsize: 2124
Raw data (/proc/27000/stat): 27000 (minisat+_64-bit) R 26996 26996 9102 0 -1 0 13244 0 0 0 49845 74 0 0 25 0 1 0 1852021819 53710848 12354 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27000/statm): 13113 12354 145 145 0 12968 0
[pid=27000] vsize: 52452
Current children cumulated CPU time (s) 499.21
Current children cumulated vsize (Kb) 54576

[startup+510.056 s]
Raw data (loadavg): 0.99 0.98 0.91 2/58 27018
Raw data (/proc/26996/stat): 26996 (minisat+_script) S 26995 26996 9102 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1852021814 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26996/statm): 531 226 485 147 0 384 0
[pid=26996] vsize: 2124
Raw data (/proc/27000/stat): 27000 (minisat+_64-bit) R 26996 26996 9102 0 -1 0 13435 0 0 0 50842 75 0 0 21 0 1 0 1852021819 54501376 12545 4294967295 134512640 135094434 3221224432 3221223088 134557866 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27000/statm): 13306 12545 145 145 0 13161 0
[pid=27000] vsize: 53224
Current children cumulated CPU time (s) 509.19
Current children cumulated vsize (Kb) 55348

[startup+520.057 s]
Raw data (loadavg): 0.99 0.98 0.91 2/58 27018
Raw data (/proc/26996/stat): 26996 (minisat+_script) S 26995 26996 9102 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1852021814 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26996/statm): 531 226 485 147 0 384 0
[pid=26996] vsize: 2124
Raw data (/proc/27000/stat): 27000 (minisat+_64-bit) R 26996 26996 9102 0 -1 0 13959 0 0 0 51833 79 0 0 25 0 1 0 1852021819 56635392 13069 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27000/statm): 13827 13069 145 145 0 13682 0
[pid=27000] vsize: 55308
Current children cumulated CPU time (s) 519.14
Current children cumulated vsize (Kb) 57432

[startup+530.057 s]
Raw data (loadavg): 0.99 0.98 0.91 2/58 27018
Raw data (/proc/26996/stat): 26996 (minisat+_script) S 26995 26996 9102 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1852021814 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26996/statm): 531 226 485 147 0 384 0
[pid=26996] vsize: 2124
Raw data (/proc/27000/stat): 27000 (minisat+_64-bit) R 26996 26996 9102 0 -1 0 14514 0 0 0 52823 83 0 0 25 0 1 0 1852021819 58892288 13624 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27000/statm): 14378 13624 145 145 0 14233 0
[pid=27000] vsize: 57512
Current children cumulated CPU time (s) 529.08
Current children cumulated vsize (Kb) 59636

[startup+540.058 s]
Raw data (loadavg): 0.99 0.98 0.91 2/58 27018
Raw data (/proc/26996/stat): 26996 (minisat+_script) S 26995 26996 9102 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1852021814 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26996/statm): 531 226 485 147 0 384 0
[pid=26996] vsize: 2124
Raw data (/proc/27000/stat): 27000 (minisat+_64-bit) R 26996 26996 9102 0 -1 0 14985 0 0 0 53815 87 0 0 25 0 1 0 1852021819 60809216 14095 4294967295 134512640 135094434 3221224432 3221223088 134558218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27000/statm): 14846 14095 145 145 0 14701 0
[pid=27000] vsize: 59384
Current children cumulated CPU time (s) 539.04
Current children cumulated vsize (Kb) 61508

[startup+550.06 s]
Raw data (loadavg): 0.99 0.98 0.91 2/58 27018
Raw data (/proc/26996/stat): 26996 (minisat+_script) S 26995 26996 9102 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1852021814 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26996/statm): 531 226 485 147 0 384 0
[pid=26996] vsize: 2124
Raw data (/proc/27000/stat): 27000 (minisat+_64-bit) R 26996 26996 9102 0 -1 0 15553 0 0 0 54805 90 0 0 25 0 1 0 1852021819 63119360 14663 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27000/statm): 15410 14663 145 145 0 15265 0
[pid=27000] vsize: 61640
Current children cumulated CPU time (s) 548.97
Current children cumulated vsize (Kb) 63764

[startup+560.061 s]
Raw data (loadavg): 0.99 0.98 0.91 2/58 27020
Raw data (/proc/26996/stat): 26996 (minisat+_script) S 26995 26996 9102 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1852021814 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26996/statm): 531 226 485 147 0 384 0
[pid=26996] vsize: 2124
Raw data (/proc/27000/stat): 27000 (minisat+_64-bit) R 26996 26996 9102 0 -1 0 15794 0 0 0 55800 92 0 0 25 0 1 0 1852021819 64098304 14904 4294967295 134512640 135094434 3221224432 3221223088 134558402 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27000/statm): 15649 14904 145 145 0 15504 0
[pid=27000] vsize: 62596
Current children cumulated CPU time (s) 558.94
Current children cumulated vsize (Kb) 64720

[startup+570.062 s]
Raw data (loadavg): 0.99 0.98 0.91 2/58 27020
Raw data (/proc/26996/stat): 26996 (minisat+_script) S 26995 26996 9102 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1852021814 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26996/statm): 531 226 485 147 0 384 0
[pid=26996] vsize: 2124
Raw data (/proc/27000/stat): 27000 (minisat+_64-bit) R 26996 26996 9102 0 -1 0 16028 0 0 0 56795 95 0 0 25 0 1 0 1852021819 65044480 15138 4294967295 134512640 135094434 3221224432 3221223056 134557565 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27000/statm): 15880 15138 145 145 0 15735 0
[pid=27000] vsize: 63520
Current children cumulated CPU time (s) 568.92
Current children cumulated vsize (Kb) 65644

[startup+580.064 s]
Raw data (loadavg): 0.99 0.98 0.91 2/58 27020
Raw data (/proc/26996/stat): 26996 (minisat+_script) S 26995 26996 9102 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1852021814 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26996/statm): 531 226 485 147 0 384 0
[pid=26996] vsize: 2124
Raw data (/proc/27000/stat): 27000 (minisat+_64-bit) R 26996 26996 9102 0 -1 0 16257 0 0 0 57791 96 0 0 25 0 1 0 1852021819 65974272 15367 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27000/statm): 16107 15367 145 145 0 15962 0
[pid=27000] vsize: 64428
Current children cumulated CPU time (s) 578.89
Current children cumulated vsize (Kb) 66552

[startup+590.065 s]
Raw data (loadavg): 0.99 0.98 0.91 2/58 27020
Raw data (/proc/26996/stat): 26996 (minisat+_script) S 26995 26996 9102 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1852021814 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26996/statm): 531 226 485 147 0 384 0
[pid=26996] vsize: 2124
Raw data (/proc/27000/stat): 27000 (minisat+_64-bit) R 26996 26996 9102 0 -1 0 16440 0 0 0 58788 97 0 0 25 0 1 0 1852021819 66711552 15550 4294967295 134512640 135094434 3221224432 3221223088 134558178 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27000/statm): 16287 15550 145 145 0 16142 0
[pid=27000] vsize: 65148
Current children cumulated CPU time (s) 588.87
Current children cumulated vsize (Kb) 67272

[startup+600.065 s]
Raw data (loadavg): 0.99 0.98 0.91 2/58 27020
Raw data (/proc/26996/stat): 26996 (minisat+_script) S 26995 26996 9102 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1852021814 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26996/statm): 531 226 485 147 0 384 0
[pid=26996] vsize: 2124
Raw data (/proc/27000/stat): 27000 (minisat+_64-bit) R 26996 26996 9102 0 -1 0 16634 0 0 0 59785 98 0 0 25 0 1 0 1852021819 67497984 15744 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27000/statm): 16479 15744 145 145 0 16334 0
[pid=27000] vsize: 65916
Current children cumulated CPU time (s) 598.85
Current children cumulated vsize (Kb) 68040

[startup+610.067 s]
Raw data (loadavg): 0.99 0.98 0.91 2/58 27020
Raw data (/proc/26996/stat): 26996 (minisat+_script) S 26995 26996 9102 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1852021814 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26996/statm): 531 226 485 147 0 384 0
[pid=26996] vsize: 2124
Raw data (/proc/27000/stat): 27000 (minisat+_64-bit) R 26996 26996 9102 0 -1 0 16751 0 0 0 60783 99 0 0 25 0 1 0 1852021819 67969024 15861 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27000/statm): 16594 15861 145 145 0 16449 0
[pid=27000] vsize: 66376
Current children cumulated CPU time (s) 608.84
Current children cumulated vsize (Kb) 68500

[startup+620.067 s]
Raw data (loadavg): 0.99 0.98 0.91 2/58 27022
Raw data (/proc/26996/stat): 26996 (minisat+_script) S 26995 26996 9102 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1852021814 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26996/statm): 531 226 485 147 0 384 0
[pid=26996] vsize: 2124
Raw data (/proc/27000/stat): 27000 (minisat+_64-bit) R 26996 26996 9102 0 -1 0 17093 0 0 0 61776 101 0 0 25 0 1 0 1852021819 69357568 16203 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27000/statm): 16933 16203 145 145 0 16788 0
[pid=27000] vsize: 67732
Current children cumulated CPU time (s) 618.79
Current children cumulated vsize (Kb) 69856

[startup+630.068 s]
Raw data (loadavg): 0.99 0.98 0.91 2/58 27022
Raw data (/proc/26996/stat): 26996 (minisat+_script) S 26995 26996 9102 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1852021814 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26996/statm): 531 226 485 147 0 384 0
[pid=26996] vsize: 2124
Raw data (/proc/27000/stat): 27000 (minisat+_64-bit) R 26996 26996 9102 0 -1 0 17247 0 0 0 62772 103 0 0 25 0 1 0 1852021819 70512640 16357 4294967295 134512640 135094434 3221224432 3221223084 134558255 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27000/statm): 17215 16357 145 145 0 17070 0
[pid=27000] vsize: 68860
Current children cumulated CPU time (s) 628.77
Current children cumulated vsize (Kb) 70984

[startup+640.069 s]
Raw data (loadavg): 0.99 0.98 0.91 2/58 27022
Raw data (/proc/26996/stat): 26996 (minisat+_script) S 26995 26996 9102 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1852021814 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26996/statm): 531 226 485 147 0 384 0
[pid=26996] vsize: 2124
Raw data (/proc/27000/stat): 27000 (minisat+_64-bit) R 26996 26996 9102 0 -1 0 17405 0 0 0 63769 104 0 0 25 0 1 0 1852021819 71139328 16515 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27000/statm): 17368 16515 145 145 0 17223 0
[pid=27000] vsize: 69472
Current children cumulated CPU time (s) 638.75
Current children cumulated vsize (Kb) 71596

[startup+650.069 s]
Raw data (loadavg): 0.99 0.98 0.91 2/58 27022
Raw data (/proc/26996/stat): 26996 (minisat+_script) S 26995 26996 9102 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1852021814 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26996/statm): 531 226 485 147 0 384 0
[pid=26996] vsize: 2124
Raw data (/proc/27000/stat): 27000 (minisat+_64-bit) R 26996 26996 9102 0 -1 0 17638 0 0 0 64764 106 0 0 25 0 1 0 1852021819 72089600 16748 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27000/statm): 17600 16748 145 145 0 17455 0
[pid=27000] vsize: 70400
Current children cumulated CPU time (s) 648.72
Current children cumulated vsize (Kb) 72524

[startup+660.069 s]
Raw data (loadavg): 0.99 0.98 0.91 2/58 27022
Raw data (/proc/26996/stat): 26996 (minisat+_script) S 26995 26996 9102 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1852021814 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26996/statm): 531 226 485 147 0 384 0
[pid=26996] vsize: 2124
Raw data (/proc/27000/stat): 27000 (minisat+_64-bit) R 26996 26996 9102 0 -1 0 17838 0 0 0 65762 107 0 0 25 0 1 0 1852021819 72916992 16948 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27000/statm): 17802 16948 145 145 0 17657 0
[pid=27000] vsize: 71208
Current children cumulated CPU time (s) 658.71
Current children cumulated vsize (Kb) 73332

[startup+670.069 s]
Raw data (loadavg): 0.99 0.98 0.91 2/58 27022
Raw data (/proc/26996/stat): 26996 (minisat+_script) S 26995 26996 9102 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1852021814 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26996/statm): 531 226 485 147 0 384 0
[pid=26996] vsize: 2124
Raw data (/proc/27000/stat): 27000 (minisat+_64-bit) R 26996 26996 9102 0 -1 0 18067 0 0 0 66757 109 0 0 25 0 1 0 1852021819 73842688 17177 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27000/statm): 18028 17177 145 145 0 17883 0
[pid=27000] vsize: 72112
Current children cumulated CPU time (s) 668.68
Current children cumulated vsize (Kb) 74236

[startup+680.07 s]
Raw data (loadavg): 0.99 0.98 0.91 2/58 27024
Raw data (/proc/26996/stat): 26996 (minisat+_script) S 26995 26996 9102 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1852021814 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26996/statm): 531 226 485 147 0 384 0
[pid=26996] vsize: 2124
Raw data (/proc/27000/stat): 27000 (minisat+_64-bit) R 26996 26996 9102 0 -1 0 18275 0 0 0 67752 111 0 0 25 0 1 0 1852021819 74702848 17385 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27000/statm): 18238 17385 145 145 0 18093 0
[pid=27000] vsize: 72952
Current children cumulated CPU time (s) 678.65
Current children cumulated vsize (Kb) 75076

[startup+690.071 s]
Raw data (loadavg): 0.99 0.98 0.91 2/58 27024
Raw data (/proc/26996/stat): 26996 (minisat+_script) S 26995 26996 9102 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1852021814 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26996/statm): 531 226 485 147 0 384 0
[pid=26996] vsize: 2124
Raw data (/proc/27000/stat): 27000 (minisat+_64-bit) R 26996 26996 9102 0 -1 0 18492 0 0 0 68750 112 0 0 25 0 1 0 1852021819 75591680 17602 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27000/statm): 18455 17602 145 145 0 18310 0
[pid=27000] vsize: 73820
Current children cumulated CPU time (s) 688.64
Current children cumulated vsize (Kb) 75944

[startup+700.072 s]
Raw data (loadavg): 0.99 0.98 0.91 2/58 27024
Raw data (/proc/26996/stat): 26996 (minisat+_script) S 26995 26996 9102 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1852021814 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26996/statm): 531 226 485 147 0 384 0
[pid=26996] vsize: 2124
Raw data (/proc/27000/stat): 27000 (minisat+_64-bit) R 26996 26996 9102 0 -1 0 18709 0 0 0 69746 114 0 0 25 0 1 0 1852021819 76480512 17819 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27000/statm): 18672 17819 145 145 0 18527 0
[pid=27000] vsize: 74688
Current children cumulated CPU time (s) 698.62
Current children cumulated vsize (Kb) 76812

[startup+710.073 s]
Raw data (loadavg): 0.99 0.98 0.91 2/58 27024
Raw data (/proc/26996/stat): 26996 (minisat+_script) S 26995 26996 9102 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1852021814 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26996/statm): 531 226 485 147 0 384 0
[pid=26996] vsize: 2124
Raw data (/proc/27000/stat): 27000 (minisat+_64-bit) R 26996 26996 9102 0 -1 0 18911 0 0 0 70743 115 0 0 25 0 1 0 1852021819 77287424 18021 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27000/statm): 18869 18021 145 145 0 18724 0
[pid=27000] vsize: 75476
Current children cumulated CPU time (s) 708.6
Current children cumulated vsize (Kb) 77600

[startup+720.074 s]
Raw data (loadavg): 0.99 0.98 0.91 2/58 27024
Raw data (/proc/26996/stat): 26996 (minisat+_script) S 26995 26996 9102 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1852021814 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26996/statm): 531 226 485 147 0 384 0
[pid=26996] vsize: 2124
Raw data (/proc/27000/stat): 27000 (minisat+_64-bit) R 26996 26996 9102 0 -1 0 19117 0 0 0 71739 116 0 0 25 0 1 0 1852021819 78118912 18227 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27000/statm): 19072 18227 145 145 0 18927 0
[pid=27000] vsize: 76288
Current children cumulated CPU time (s) 718.57
Current children cumulated vsize (Kb) 78412

[startup+730.076 s]
Raw data (loadavg): 0.99 0.98 0.91 2/58 27024
Raw data (/proc/26996/stat): 26996 (minisat+_script) S 26995 26996 9102 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1852021814 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26996/statm): 531 226 485 147 0 384 0
[pid=26996] vsize: 2124
Raw data (/proc/27000/stat): 27000 (minisat+_64-bit) R 26996 26996 9102 0 -1 0 19566 0 0 0 72732 119 0 0 25 0 1 0 1852021819 79949824 18676 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27000/statm): 19519 18676 145 145 0 19374 0
[pid=27000] vsize: 78076
Current children cumulated CPU time (s) 728.53
Current children cumulated vsize (Kb) 80200

[startup+740.077 s]
Raw data (loadavg): 0.99 0.98 0.91 2/58 27026
Raw data (/proc/26996/stat): 26996 (minisat+_script) S 26995 26996 9102 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1852021814 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26996/statm): 531 226 485 147 0 384 0
[pid=26996] vsize: 2124
Raw data (/proc/27000/stat): 27000 (minisat+_64-bit) R 26996 26996 9102 0 -1 0 19803 0 0 0 73729 121 0 0 25 0 1 0 1852021819 80916480 18913 4294967295 134512640 135094434 3221224432 3221223088 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27000/statm): 19755 18913 145 145 0 19610 0
[pid=27000] vsize: 79020
Current children cumulated CPU time (s) 738.52
Current children cumulated vsize (Kb) 81144

[startup+750.078 s]
Raw data (loadavg): 0.99 0.98 0.91 2/58 27026
Raw data (/proc/26996/stat): 26996 (minisat+_script) S 26995 26996 9102 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1852021814 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26996/statm): 531 226 485 147 0 384 0
[pid=26996] vsize: 2124
Raw data (/proc/27000/stat): 27000 (minisat+_64-bit) R 26996 26996 9102 0 -1 0 20276 0 0 0 74721 124 0 0 25 0 1 0 1852021819 82845696 19386 4294967295 134512640 135094434 3221224432 3221223088 134558295 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27000/statm): 20226 19386 145 145 0 20081 0
[pid=27000] vsize: 80904
Current children cumulated CPU time (s) 748.47
Current children cumulated vsize (Kb) 83028

[startup+760.079 s]
Raw data (loadavg): 0.99 0.98 0.91 2/58 27026
Raw data (/proc/26996/stat): 26996 (minisat+_script) S 26995 26996 9102 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1852021814 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26996/statm): 531 226 485 147 0 384 0
[pid=26996] vsize: 2124
Raw data (/proc/27000/stat): 27000 (minisat+_64-bit) R 26996 26996 9102 0 -1 0 20807 0 0 0 75711 128 0 0 25 0 1 0 1852021819 85012480 19917 4294967295 134512640 135094434 3221224432 3221223024 134556785 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27000/statm): 20755 19917 145 145 0 20610 0
[pid=27000] vsize: 83020
Current children cumulated CPU time (s) 758.41
Current children cumulated vsize (Kb) 85144

[startup+770.079 s]
Raw data (loadavg): 0.99 0.98 0.91 2/58 27026
Raw data (/proc/26996/stat): 26996 (minisat+_script) S 26995 26996 9102 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1852021814 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26996/statm): 531 226 485 147 0 384 0
[pid=26996] vsize: 2124
Raw data (/proc/27000/stat): 27000 (minisat+_64-bit) R 26996 26996 9102 0 -1 0 21340 0 0 0 76706 131 0 0 25 0 1 0 1852021819 87187456 20450 4294967295 134512640 135094434 3221224432 3221223024 134556812 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27000/statm): 21286 20450 145 145 0 21141 0
[pid=27000] vsize: 85144
Current children cumulated CPU time (s) 768.39
Current children cumulated vsize (Kb) 87268

[startup+780.08 s]
Raw data (loadavg): 0.99 0.98 0.91 2/58 27026
Raw data (/proc/26996/stat): 26996 (minisat+_script) S 26995 26996 9102 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1852021814 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26996/statm): 531 226 485 147 0 384 0
[pid=26996] vsize: 2124
Raw data (/proc/27000/stat): 27000 (minisat+_64-bit) R 26996 26996 9102 0 -1 0 21889 0 0 0 77699 134 0 0 25 0 1 0 1852021819 89432064 20999 4294967295 134512640 135094434 3221224432 3221223024 134557401 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27000/statm): 21834 20999 145 145 0 21689 0
[pid=27000] vsize: 87336
Current children cumulated CPU time (s) 778.35
Current children cumulated vsize (Kb) 89460

[startup+790.081 s]
Raw data (loadavg): 0.99 0.98 0.91 2/58 27026
Raw data (/proc/26996/stat): 26996 (minisat+_script) S 26995 26996 9102 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1852021814 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26996/statm): 531 226 485 147 0 384 0
[pid=26996] vsize: 2124
Raw data (/proc/27000/stat): 27000 (minisat+_64-bit) R 26996 26996 9102 0 -1 0 22396 0 0 0 78692 137 0 0 25 0 1 0 1852021819 91504640 21506 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27000/statm): 22340 21506 145 145 0 22195 0
[pid=27000] vsize: 89360
Current children cumulated CPU time (s) 788.31
Current children cumulated vsize (Kb) 91484

[startup+800.081 s]
Raw data (loadavg): 0.99 0.98 0.91 2/58 27028
Raw data (/proc/26996/stat): 26996 (minisat+_script) S 26995 26996 9102 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1852021814 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26996/statm): 531 226 485 147 0 384 0
[pid=26996] vsize: 2124
Raw data (/proc/27000/stat): 27000 (minisat+_64-bit) T 26996 26996 9102 0 -1 0 22877 0 0 0 79689 138 0 0 25 0 1 0 1852021819 93470720 21987 4294967295 134512640 135094434 3221224432 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/27000/statm): 22820 21987 145 145 0 22675 0
[pid=27000] vsize: 91280
Current children cumulated CPU time (s) 798.29
Current children cumulated vsize (Kb) 93404

[startup+810.082 s]
Raw data (loadavg): 0.99 0.98 0.91 2/58 27028
Raw data (/proc/26996/stat): 26996 (minisat+_script) S 26995 26996 9102 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1852021814 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26996/statm): 531 226 485 147 0 384 0
[pid=26996] vsize: 2124
Raw data (/proc/27000/stat): 27000 (minisat+_64-bit) R 26996 26996 9102 0 -1 0 23303 0 0 0 80685 140 0 0 25 0 1 0 1852021819 95215616 22413 4294967295 134512640 135094434 3221224432 3221223024 134557202 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27000/statm): 23246 22413 145 145 0 23101 0
[pid=27000] vsize: 92984
Current children cumulated CPU time (s) 808.27
Current children cumulated vsize (Kb) 95108

[startup+820.082 s]
Raw data (loadavg): 0.99 0.98 0.91 2/58 27028
Raw data (/proc/26996/stat): 26996 (minisat+_script) S 26995 26996 9102 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1852021814 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26996/statm): 531 226 485 147 0 384 0
[pid=26996] vsize: 2124
Raw data (/proc/27000/stat): 27000 (minisat+_64-bit) R 26996 26996 9102 0 -1 0 23753 0 0 0 81681 142 0 0 25 0 1 0 1852021819 97054720 22863 4294967295 134512640 135094434 3221224432 3221223088 134558126 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27000/statm): 23695 22863 145 145 0 23550 0
[pid=27000] vsize: 94780
Current children cumulated CPU time (s) 818.25
Current children cumulated vsize (Kb) 96904

[startup+830.083 s]
Raw data (loadavg): 0.99 0.98 0.91 2/58 27028
Raw data (/proc/26996/stat): 26996 (minisat+_script) S 26995 26996 9102 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1852021814 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26996/statm): 531 226 485 147 0 384 0
[pid=26996] vsize: 2124
Raw data (/proc/27000/stat): 27000 (minisat+_64-bit) R 26996 26996 9102 0 -1 0 24184 0 0 0 82677 145 0 0 25 0 1 0 1852021819 98820096 23294 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27000/statm): 24126 23294 145 145 0 23981 0
[pid=27000] vsize: 96504
Current children cumulated CPU time (s) 828.24
Current children cumulated vsize (Kb) 98628

[startup+840.084 s]
Raw data (loadavg): 0.99 0.98 0.91 2/58 27028
Raw data (/proc/26996/stat): 26996 (minisat+_script) S 26995 26996 9102 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1852021814 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26996/statm): 531 226 485 147 0 384 0
[pid=26996] vsize: 2124
Raw data (/proc/27000/stat): 27000 (minisat+_64-bit) R 26996 26996 9102 0 -1 0 24617 0 0 0 83673 146 0 0 25 0 1 0 1852021819 100589568 23727 4294967295 134512640 135094434 3221224432 3221223024 134556815 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27000/statm): 24558 23727 145 145 0 24413 0
[pid=27000] vsize: 98232
Current children cumulated CPU time (s) 838.21
Current children cumulated vsize (Kb) 100356

[startup+850.085 s]
Raw data (loadavg): 0.99 0.98 0.91 2/58 27028
Raw data (/proc/26996/stat): 26996 (minisat+_script) S 26995 26996 9102 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1852021814 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26996/statm): 531 226 485 147 0 384 0
[pid=26996] vsize: 2124
Raw data (/proc/27000/stat): 27000 (minisat+_64-bit) R 26996 26996 9102 0 -1 0 24740 0 0 0 84672 147 0 0 25 0 1 0 1852021819 101097472 23850 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27000/statm): 24682 23850 145 145 0 24537 0
[pid=27000] vsize: 98728
Current children cumulated CPU time (s) 848.21
Current children cumulated vsize (Kb) 100852

[startup+860.086 s]
Raw data (loadavg): 0.99 0.98 0.91 2/58 27030
Raw data (/proc/26996/stat): 26996 (minisat+_script) S 26995 26996 9102 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1852021814 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26996/statm): 531 226 485 147 0 384 0
[pid=26996] vsize: 2124
Raw data (/proc/27000/stat): 27000 (minisat+_64-bit) R 26996 26996 9102 0 -1 0 24895 0 0 0 85670 148 0 0 25 0 1 0 1852021819 101720064 24005 4294967295 134512640 135094434 3221224432 3221223088 134558016 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27000/statm): 24834 24005 145 145 0 24689 0
[pid=27000] vsize: 99336
Current children cumulated CPU time (s) 858.2
Current children cumulated vsize (Kb) 101460

[startup+870.087 s]
Raw data (loadavg): 0.99 0.98 0.91 2/58 27030
Raw data (/proc/26996/stat): 26996 (minisat+_script) S 26995 26996 9102 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1852021814 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26996/statm): 531 226 485 147 0 384 0
[pid=26996] vsize: 2124
Raw data (/proc/27000/stat): 27000 (minisat+_64-bit) R 26996 26996 9102 0 -1 0 25054 0 0 0 86667 149 0 0 25 0 1 0 1852021819 102408192 24164 4294967295 134512640 135094434 3221224432 3221223024 134557002 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27000/statm): 25002 24164 145 145 0 24857 0
[pid=27000] vsize: 100008
Current children cumulated CPU time (s) 868.18
Current children cumulated vsize (Kb) 102132

[startup+880.088 s]
Raw data (loadavg): 0.99 0.98 0.91 2/58 27030
Raw data (/proc/26996/stat): 26996 (minisat+_script) S 26995 26996 9102 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1852021814 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26996/statm): 531 226 485 147 0 384 0
[pid=26996] vsize: 2124
Raw data (/proc/27000/stat): 27000 (minisat+_64-bit) R 26996 26996 9102 0 -1 0 25241 0 0 0 87665 150 0 0 25 0 1 0 1852021819 103182336 24351 4294967295 134512640 135094434 3221224432 3221223088 134558210 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27000/statm): 25191 24351 145 145 0 25046 0
[pid=27000] vsize: 100764
Current children cumulated CPU time (s) 878.17
Current children cumulated vsize (Kb) 102888

[startup+890.089 s]
Raw data (loadavg): 0.99 0.98 0.91 2/58 27030
Raw data (/proc/26996/stat): 26996 (minisat+_script) S 26995 26996 9102 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1852021814 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26996/statm): 531 226 485 147 0 384 0
[pid=26996] vsize: 2124
Raw data (/proc/27000/stat): 27000 (minisat+_64-bit) R 26996 26996 9102 0 -1 0 25397 0 0 0 88664 151 0 0 25 0 1 0 1852021819 103833600 24507 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27000/statm): 25350 24507 145 145 0 25205 0
[pid=27000] vsize: 101400
Current children cumulated CPU time (s) 888.17
Current children cumulated vsize (Kb) 103524

[startup+900.09 s]
Raw data (loadavg): 0.99 0.98 0.91 2/58 27030
Raw data (/proc/26996/stat): 26996 (minisat+_script) S 26995 26996 9102 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1852021814 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26996/statm): 531 226 485 147 0 384 0
[pid=26996] vsize: 2124
Raw data (/proc/27000/stat): 27000 (minisat+_64-bit) R 26996 26996 9102 0 -1 0 25572 0 0 0 89661 152 0 0 25 0 1 0 1852021819 104546304 24682 4294967295 134512640 135094434 3221224432 3221223088 134557950 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27000/statm): 25524 24682 145 145 0 25379 0
[pid=27000] vsize: 102096
Current children cumulated CPU time (s) 898.15
Current children cumulated vsize (Kb) 104220

[startup+910.091 s]
Raw data (loadavg): 0.99 0.98 0.91 2/58 27030
Raw data (/proc/26996/stat): 26996 (minisat+_script) S 26995 26996 9102 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1852021814 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26996/statm): 531 226 485 147 0 384 0
[pid=26996] vsize: 2124
Raw data (/proc/27000/stat): 27000 (minisat+_64-bit) R 26996 26996 9102 0 -1 0 25750 0 0 0 90658 153 0 0 25 0 1 0 1852021819 105267200 24860 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27000/statm): 25700 24860 145 145 0 25555 0
[pid=27000] vsize: 102800
Current children cumulated CPU time (s) 908.13
Current children cumulated vsize (Kb) 104924

[startup+920.092 s]
Raw data (loadavg): 0.99 0.98 0.91 2/58 27032
Raw data (/proc/26996/stat): 26996 (minisat+_script) S 26995 26996 9102 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1852021814 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26996/statm): 531 226 485 147 0 384 0
[pid=26996] vsize: 2124
Raw data (/proc/27000/stat): 27000 (minisat+_64-bit) R 26996 26996 9102 0 -1 0 25909 0 0 0 91655 154 0 0 25 0 1 0 1852021819 105906176 25019 4294967295 134512640 135094434 3221224432 3221223088 134557872 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27000/statm): 25856 25019 145 145 0 25711 0
[pid=27000] vsize: 103424
Current children cumulated CPU time (s) 918.11
Current children cumulated vsize (Kb) 105548

[startup+930.093 s]
Raw data (loadavg): 0.99 0.98 0.91 2/58 27032
Raw data (/proc/26996/stat): 26996 (minisat+_script) S 26995 26996 9102 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1852021814 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26996/statm): 531 226 485 147 0 384 0
[pid=26996] vsize: 2124
Raw data (/proc/27000/stat): 27000 (minisat+_64-bit) R 26996 26996 9102 0 -1 0 26065 0 0 0 92653 155 0 0 25 0 1 0 1852021819 106528768 25175 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27000/statm): 26008 25175 145 145 0 25863 0
[pid=27000] vsize: 104032
Current children cumulated CPU time (s) 928.1
Current children cumulated vsize (Kb) 106156

[startup+940.094 s]
Raw data (loadavg): 0.99 0.98 0.91 2/58 27032
Raw data (/proc/26996/stat): 26996 (minisat+_script) S 26995 26996 9102 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1852021814 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26996/statm): 531 226 485 147 0 384 0
[pid=26996] vsize: 2124
Raw data (/proc/27000/stat): 27000 (minisat+_64-bit) R 26996 26996 9102 0 -1 0 26226 0 0 0 93650 156 0 0 25 0 1 0 1852021819 107184128 25336 4294967295 134512640 135094434 3221224432 3221223088 134557884 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27000/statm): 26168 25336 145 145 0 26023 0
[pid=27000] vsize: 104672
Current children cumulated CPU time (s) 938.08
Current children cumulated vsize (Kb) 106796

[startup+950.094 s]
Raw data (loadavg): 0.99 0.98 0.91 2/58 27032
Raw data (/proc/26996/stat): 26996 (minisat+_script) S 26995 26996 9102 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1852021814 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26996/statm): 531 226 485 147 0 384 0
[pid=26996] vsize: 2124
Raw data (/proc/27000/stat): 27000 (minisat+_64-bit) R 26996 26996 9102 0 -1 0 26388 0 0 0 94648 157 0 0 25 0 1 0 1852021819 107847680 25498 4294967295 134512640 135094434 3221224432 3221223088 134558218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27000/statm): 26330 25498 145 145 0 26185 0
[pid=27000] vsize: 105320
Current children cumulated CPU time (s) 948.07
Current children cumulated vsize (Kb) 107444

[startup+960.096 s]
Raw data (loadavg): 0.99 0.98 0.91 2/58 27032
Raw data (/proc/26996/stat): 26996 (minisat+_script) S 26995 26996 9102 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1852021814 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26996/statm): 531 226 485 147 0 384 0
[pid=26996] vsize: 2124
Raw data (/proc/27000/stat): 27000 (minisat+_64-bit) R 26996 26996 9102 0 -1 0 26531 0 0 0 95646 158 0 0 25 0 1 0 1852021819 108421120 25641 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27000/statm): 26470 25641 145 145 0 26325 0
[pid=27000] vsize: 105880
Current children cumulated CPU time (s) 958.06
Current children cumulated vsize (Kb) 108004

[startup+970.096 s]
Raw data (loadavg): 0.99 0.98 0.91 2/58 27032
Raw data (/proc/26996/stat): 26996 (minisat+_script) S 26995 26996 9102 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1852021814 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26996/statm): 531 226 485 147 0 384 0
[pid=26996] vsize: 2124
Raw data (/proc/27000/stat): 27000 (minisat+_64-bit) R 26996 26996 9102 0 -1 0 26681 0 0 0 96644 158 0 0 25 0 1 0 1852021819 109064192 25791 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27000/statm): 26627 25791 145 145 0 26482 0
[pid=27000] vsize: 106508
Current children cumulated CPU time (s) 968.04
Current children cumulated vsize (Kb) 108632

[startup+980.097 s]
Raw data (loadavg): 0.99 0.98 0.91 2/58 27034
Raw data (/proc/26996/stat): 26996 (minisat+_script) S 26995 26996 9102 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1852021814 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26996/statm): 531 226 485 147 0 384 0
[pid=26996] vsize: 2124
Raw data (/proc/27000/stat): 27000 (minisat+_64-bit) R 26996 26996 9102 0 -1 0 26856 0 0 0 97641 160 0 0 25 0 1 0 1852021819 109801472 25966 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27000/statm): 26807 25966 145 145 0 26662 0
[pid=27000] vsize: 107228
Current children cumulated CPU time (s) 978.03
Current children cumulated vsize (Kb) 109352

[startup+990.098 s]
Raw data (loadavg): 0.99 0.98 0.91 2/58 27034
Raw data (/proc/26996/stat): 26996 (minisat+_script) S 26995 26996 9102 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1852021814 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26996/statm): 531 226 485 147 0 384 0
[pid=26996] vsize: 2124
Raw data (/proc/27000/stat): 27000 (minisat+_64-bit) R 26996 26996 9102 0 -1 0 27016 0 0 0 98638 161 0 0 25 0 1 0 1852021819 110440448 26126 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27000/statm): 26963 26126 145 145 0 26818 0
[pid=27000] vsize: 107852
Current children cumulated CPU time (s) 988.01
Current children cumulated vsize (Kb) 109976

[startup+1000.1 s]
Raw data (loadavg): 0.99 0.98 0.91 2/58 27034
Raw data (/proc/26996/stat): 26996 (minisat+_script) S 26995 26996 9102 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1852021814 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26996/statm): 531 226 485 147 0 384 0
[pid=26996] vsize: 2124
Raw data (/proc/27000/stat): 27000 (minisat+_64-bit) R 26996 26996 9102 0 -1 0 27187 0 0 0 99637 161 0 0 25 0 1 0 1852021819 111235072 26297 4294967295 134512640 135094434 3221224432 3221223088 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27000/statm): 27157 26297 145 145 0 27012 0
[pid=27000] vsize: 108628
Current children cumulated CPU time (s) 998
Current children cumulated vsize (Kb) 110752

[startup+1010.1 s]
Raw data (loadavg): 0.99 0.98 0.91 2/58 27034
Raw data (/proc/26996/stat): 26996 (minisat+_script) S 26995 26996 9102 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1852021814 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26996/statm): 531 226 485 147 0 384 0
[pid=26996] vsize: 2124
Raw data (/proc/27000/stat): 27000 (minisat+_64-bit) R 26996 26996 9102 0 -1 0 27349 0 0 0 100634 162 0 0 25 0 1 0 1852021819 111898624 26459 4294967295 134512640 135094434 3221224432 3221223088 134558181 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27000/statm): 27319 26459 145 145 0 27174 0
[pid=27000] vsize: 109276
Current children cumulated CPU time (s) 1007.98
Current children cumulated vsize (Kb) 111400

[startup+1020.1 s]
Raw data (loadavg): 0.99 0.98 0.91 2/58 27034
Raw data (/proc/26996/stat): 26996 (minisat+_script) S 26995 26996 9102 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1852021814 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26996/statm): 531 226 485 147 0 384 0
[pid=26996] vsize: 2124
Raw data (/proc/27000/stat): 27000 (minisat+_64-bit) R 26996 26996 9102 0 -1 0 27497 0 0 0 101632 163 0 0 25 0 1 0 1852021819 112504832 26607 4294967295 134512640 135094434 3221224432 3221223088 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27000/statm): 27467 26607 145 145 0 27322 0
[pid=27000] vsize: 109868
Current children cumulated CPU time (s) 1017.97
Current children cumulated vsize (Kb) 111992

[startup+1030.1 s]
Raw data (loadavg): 0.99 0.98 0.91 2/58 27034
Raw data (/proc/26996/stat): 26996 (minisat+_script) S 26995 26996 9102 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1852021814 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26996/statm): 531 226 485 147 0 384 0
[pid=26996] vsize: 2124
Raw data (/proc/27000/stat): 27000 (minisat+_64-bit) R 26996 26996 9102 0 -1 0 27649 0 0 0 102631 163 0 0 25 0 1 0 1852021819 113184768 26759 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27000/statm): 27633 26759 145 145 0 27488 0
[pid=27000] vsize: 110532
Current children cumulated CPU time (s) 1027.96
Current children cumulated vsize (Kb) 112656

[startup+1040.1 s]
Raw data (loadavg): 0.99 0.98 0.91 2/58 27036
Raw data (/proc/26996/stat): 26996 (minisat+_script) S 26995 26996 9102 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1852021814 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26996/statm): 531 226 485 147 0 384 0
[pid=26996] vsize: 2124
Raw data (/proc/27000/stat): 27000 (minisat+_64-bit) R 26996 26996 9102 0 -1 0 27826 0 0 0 103629 164 0 0 25 0 1 0 1852021819 113917952 26936 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27000/statm): 27812 26936 145 145 0 27667 0
[pid=27000] vsize: 111248
Current children cumulated CPU time (s) 1037.95
Current children cumulated vsize (Kb) 113372

[startup+1050.1 s]
Raw data (loadavg): 0.99 0.98 0.91 2/58 27036
Raw data (/proc/26996/stat): 26996 (minisat+_script) S 26995 26996 9102 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1852021814 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26996/statm): 531 226 485 147 0 384 0
[pid=26996] vsize: 2124
Raw data (/proc/27000/stat): 27000 (minisat+_64-bit) R 26996 26996 9102 0 -1 0 27983 0 0 0 104626 166 0 0 25 0 1 0 1852021819 114610176 27093 4294967295 134512640 135094434 3221224432 3221223104 134555599 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27000/statm): 27981 27093 145 145 0 27836 0
[pid=27000] vsize: 111924
Current children cumulated CPU time (s) 1047.94
Current children cumulated vsize (Kb) 114048

[startup+1060.1 s]
Raw data (loadavg): 0.99 0.98 0.91 2/58 27036
Raw data (/proc/26996/stat): 26996 (minisat+_script) S 26995 26996 9102 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1852021814 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26996/statm): 531 226 485 147 0 384 0
[pid=26996] vsize: 2124
Raw data (/proc/27000/stat): 27000 (minisat+_64-bit) R 26996 26996 9102 0 -1 0 28136 0 0 0 105624 167 0 0 25 0 1 0 1852021819 115232768 27246 4294967295 134512640 135094434 3221224432 3221223088 134557956 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27000/statm): 28133 27246 145 145 0 27988 0
[pid=27000] vsize: 112532
Current children cumulated CPU time (s) 1057.93
Current children cumulated vsize (Kb) 114656

[startup+1070.11 s]
Raw data (loadavg): 0.99 0.98 0.91 2/58 27036
Raw data (/proc/26996/stat): 26996 (minisat+_script) S 26995 26996 9102 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1852021814 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26996/statm): 531 226 485 147 0 384 0
[pid=26996] vsize: 2124
Raw data (/proc/27000/stat): 27000 (minisat+_64-bit) R 26996 26996 9102 0 -1 0 28225 0 0 0 106623 168 0 0 25 0 1 0 1852021819 115593216 27335 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27000/statm): 28221 27335 145 145 0 28076 0
[pid=27000] vsize: 112884
Current children cumulated CPU time (s) 1067.93
Current children cumulated vsize (Kb) 115008

[startup+1080.11 s]
Raw data (loadavg): 0.99 0.98 0.91 2/58 27036
Raw data (/proc/26996/stat): 26996 (minisat+_script) S 26995 26996 9102 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1852021814 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26996/statm): 531 226 485 147 0 384 0
[pid=26996] vsize: 2124
Raw data (/proc/27000/stat): 27000 (minisat+_64-bit) R 26996 26996 9102 0 -1 0 28633 0 0 0 107616 171 0 0 25 0 1 0 1852021819 117252096 27743 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27000/statm): 28626 27743 145 145 0 28481 0
[pid=27000] vsize: 114504
Current children cumulated CPU time (s) 1077.89
Current children cumulated vsize (Kb) 116628

[startup+1090.11 s]
Raw data (loadavg): 0.99 0.98 0.91 2/58 27036
Raw data (/proc/26996/stat): 26996 (minisat+_script) S 26995 26996 9102 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1852021814 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26996/statm): 531 226 485 147 0 384 0
[pid=26996] vsize: 2124
Raw data (/proc/27000/stat): 27000 (minisat+_64-bit) R 26996 26996 9102 0 -1 0 29356 0 0 0 108605 176 0 0 25 0 1 0 1852021819 120201216 28466 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27000/statm): 29346 28466 145 145 0 29201 0
[pid=27000] vsize: 117384
Current children cumulated CPU time (s) 1087.83
Current children cumulated vsize (Kb) 119508

[startup+1100.11 s]
Raw data (loadavg): 0.99 0.98 0.91 2/58 27038
Raw data (/proc/26996/stat): 26996 (minisat+_script) S 26995 26996 9102 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1852021814 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26996/statm): 531 226 485 147 0 384 0
[pid=26996] vsize: 2124
Raw data (/proc/27000/stat): 27000 (minisat+_64-bit) R 26996 26996 9102 0 -1 0 30060 0 0 0 109594 180 0 0 25 0 1 0 1852021819 123072512 29170 4294967295 134512640 135094434 3221224432 3221223088 134557925 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27000/statm): 30047 29170 145 145 0 29902 0
[pid=27000] vsize: 120188
Current children cumulated CPU time (s) 1097.76
Current children cumulated vsize (Kb) 122312

[startup+1110.11 s]
Raw data (loadavg): 0.99 0.98 0.91 2/58 27038
Raw data (/proc/26996/stat): 26996 (minisat+_script) S 26995 26996 9102 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1852021814 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26996/statm): 531 226 485 147 0 384 0
[pid=26996] vsize: 2124
Raw data (/proc/27000/stat): 27000 (minisat+_64-bit) R 26996 26996 9102 0 -1 0 30708 0 0 0 110584 185 0 0 25 0 1 0 1852021819 125718528 29818 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27000/statm): 30693 29818 145 145 0 30548 0
[pid=27000] vsize: 122772
Current children cumulated CPU time (s) 1107.71
Current children cumulated vsize (Kb) 124896

[startup+1120.11 s]
Raw data (loadavg): 0.99 0.98 0.91 2/58 27038
Raw data (/proc/26996/stat): 26996 (minisat+_script) S 26995 26996 9102 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1852021814 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26996/statm): 531 226 485 147 0 384 0
[pid=26996] vsize: 2124
Raw data (/proc/27000/stat): 27000 (minisat+_64-bit) R 26996 26996 9102 0 -1 0 31258 0 0 0 111575 189 0 0 25 0 1 0 1852021819 127959040 30368 4294967295 134512640 135094434 3221224432 3221223056 134562057 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27000/statm): 31240 30368 145 145 0 31095 0
[pid=27000] vsize: 124960
Current children cumulated CPU time (s) 1117.66
Current children cumulated vsize (Kb) 127084

[startup+1130.11 s]
Raw data (loadavg): 0.99 0.98 0.91 2/58 27038
Raw data (/proc/26996/stat): 26996 (minisat+_script) S 26995 26996 9102 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1852021814 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26996/statm): 531 226 485 147 0 384 0
[pid=26996] vsize: 2124
Raw data (/proc/27000/stat): 27000 (minisat+_64-bit) R 26996 26996 9102 0 -1 0 31884 0 0 0 112568 192 0 0 25 0 1 0 1852021819 130519040 30994 4294967295 134512640 135094434 3221224432 3221223024 134557199 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27000/statm): 31865 30994 145 145 0 31720 0
[pid=27000] vsize: 127460
Current children cumulated CPU time (s) 1127.62
Current children cumulated vsize (Kb) 129584

[startup+1140.11 s]
Raw data (loadavg): 0.99 0.98 0.91 2/58 27038
Raw data (/proc/26996/stat): 26996 (minisat+_script) S 26995 26996 9102 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1852021814 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26996/statm): 531 226 485 147 0 384 0
[pid=26996] vsize: 2124
Raw data (/proc/27000/stat): 27000 (minisat+_64-bit) R 26996 26996 9102 0 -1 0 32529 0 0 0 113560 195 0 0 25 0 1 0 1852021819 133152768 31639 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27000/statm): 32508 31639 145 145 0 32363 0
[pid=27000] vsize: 130032
Current children cumulated CPU time (s) 1137.57
Current children cumulated vsize (Kb) 132156

[startup+1150.11 s]
Raw data (loadavg): 0.99 0.98 0.91 2/58 27038
Raw data (/proc/26996/stat): 26996 (minisat+_script) S 26995 26996 9102 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1852021814 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26996/statm): 531 226 485 147 0 384 0
[pid=26996] vsize: 2124
Raw data (/proc/27000/stat): 27000 (minisat+_64-bit) R 26996 26996 9102 0 -1 0 33231 0 0 0 114551 199 0 0 25 0 1 0 1852021819 136019968 32341 4294967295 134512640 135094434 3221224432 3221223024 134556918 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27000/statm): 33208 32341 145 145 0 33063 0
[pid=27000] vsize: 132832
Current children cumulated CPU time (s) 1147.52
Current children cumulated vsize (Kb) 134956

[startup+1160.11 s]
Raw data (loadavg): 0.99 0.98 0.91 1/58 27040
Raw data (/proc/26996/stat): 26996 (minisat+_script) S 26995 26996 9102 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1852021814 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26996/statm): 531 226 485 147 0 384 0
[pid=26996] vsize: 2124
Raw data (/proc/27000/stat): 27000 (minisat+_64-bit) T 26996 26996 9102 0 -1 0 34007 0 0 0 115541 204 0 0 23 0 1 0 1852021819 139194368 33117 4294967295 134512640 135094434 3221224432 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/27000/statm): 33983 33117 145 145 0 33838 0
[pid=27000] vsize: 135932
Current children cumulated CPU time (s) 1157.47
Current children cumulated vsize (Kb) 138056

[startup+1170.11 s]
Raw data (loadavg): 0.99 0.98 0.91 2/58 27040
Raw data (/proc/26996/stat): 26996 (minisat+_script) S 26995 26996 9102 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1852021814 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26996/statm): 531 226 485 147 0 384 0
[pid=26996] vsize: 2124
Raw data (/proc/27000/stat): 27000 (minisat+_64-bit) R 26996 26996 9102 0 -1 0 34752 0 0 0 116534 207 0 0 25 0 1 0 1852021819 142237696 33862 4294967295 134512640 135094434 3221224432 3221223088 134558218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27000/statm): 34726 33862 145 145 0 34581 0
[pid=27000] vsize: 138904
Current children cumulated CPU time (s) 1167.43
Current children cumulated vsize (Kb) 141028

[startup+1180.11 s]
Raw data (loadavg): 0.99 0.98 0.91 2/58 27040
Raw data (/proc/26996/stat): 26996 (minisat+_script) S 26995 26996 9102 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1852021814 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26996/statm): 531 226 485 147 0 384 0
[pid=26996] vsize: 2124
Raw data (/proc/27000/stat): 27000 (minisat+_64-bit) R 26996 26996 9102 0 -1 0 35494 0 0 0 117525 211 0 0 25 0 1 0 1852021819 145272832 34604 4294967295 134512640 135094434 3221224432 3221223024 134557230 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27000/statm): 35467 34604 145 145 0 35322 0
[pid=27000] vsize: 141868
Current children cumulated CPU time (s) 1177.38
Current children cumulated vsize (Kb) 143992

[startup+1190.12 s]
Raw data (loadavg): 0.99 0.98 0.91 2/58 27040
Raw data (/proc/26996/stat): 26996 (minisat+_script) S 26995 26996 9102 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1852021814 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26996/statm): 531 226 485 147 0 384 0
[pid=26996] vsize: 2124
Raw data (/proc/27000/stat): 27000 (minisat+_64-bit) R 26996 26996 9102 0 -1 0 36179 0 0 0 118519 214 0 0 25 0 1 0 1852021819 148074496 35289 4294967295 134512640 135094434 3221224432 3221223056 134557645 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27000/statm): 36151 35289 145 145 0 36006 0
[pid=27000] vsize: 144604
Current children cumulated CPU time (s) 1187.35
Current children cumulated vsize (Kb) 146728

[startup+1200.12 s]
Raw data (loadavg): 0.99 0.98 0.91 2/58 27040
Raw data (/proc/26996/stat): 26996 (minisat+_script) S 26995 26996 9102 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1852021814 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26996/statm): 531 226 485 147 0 384 0
[pid=26996] vsize: 2124
Raw data (/proc/27000/stat): 27000 (minisat+_64-bit) R 26996 26996 9102 0 -1 0 36760 0 0 0 119511 217 0 0 25 0 1 0 1852021819 150446080 35870 4294967295 134512640 135094434 3221224432 3221223024 134551908 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27000/statm): 36730 35870 145 145 0 36585 0
[pid=27000] vsize: 146920
Current children cumulated CPU time (s) 1197.3
Current children cumulated vsize (Kb) 149044

[startup+1210.12 s]
Raw data (loadavg): 0.99 0.98 0.91 2/58 27040
Raw data (/proc/26996/stat): 26996 (minisat+_script) S 26995 26996 9102 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1852021814 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26996/statm): 531 226 485 147 0 384 0
[pid=26996] vsize: 2124
Raw data (/proc/27000/stat): 27000 (minisat+_64-bit) T 26996 26996 9102 0 -1 0 37384 0 0 0 120501 221 0 0 25 0 1 0 1852021819 152993792 36494 4294967295 134512640 135094434 3221224432 3221222796 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/27000/statm): 37352 36494 145 145 0 37207 0
[pid=27000] vsize: 149408
Current children cumulated CPU time (s) 1207.24
Current children cumulated vsize (Kb) 151532



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.12 s]
Raw data (loadavg): 0.99 0.98 0.91 1/58 27040
Raw data (/proc/26996/stat): 26996 (minisat+_script) S 26995 26996 9102 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1852021814 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26996/statm): 531 226 485 147 0 384 0
[pid=26996] vsize: 2124
Raw data (/proc/27000/stat): 27000 (minisat+_64-bit) T 26996 26996 9102 0 -1 0 37384 0 0 0 120501 221 0 0 25 0 1 0 1852021819 152993792 36494 4294967295 134512640 135094434 3221224432 3221222796 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/27000/statm): 37352 36494 145 145 0 37207 0
[pid=27000] vsize: 149408
Current children cumulated CPU time (s) 1207.24
Current children cumulated vsize (Kb) 151532

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

Child status: 10
Real time (s): 1210.2
CPU time (s): 1207.31
CPU user time (s): 1205.02
CPU system time (s): 2.28865
CPU usage (%): 99.7614
Max. virtual memory (cumulated for all children) (Kb): 151532

Verifier Data

ERROR: no interpretation found !