Some explanations

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

General information on the benchmark

Namemps-v2-13-7/MIPLIB/miplib3/normalized-mps-v2-13-7-gt2.opb
MD5SUMf1382105ee9fb79777762a53cf6a73c1
Bench Categoryoptimization, medium integers (OPTMEDINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function 21166
Optimality of the best value was proved YES
Number of terms in the objective function 304
Biggest coefficient in the objective function 62376
Number of bits for the biggest coefficient in the objective function 16
Sum of the numbers in the objective function 3092598
Number of bits of the sum of numbers in the objective function 22
Biggest number in a constraint 62376
Number of bits of the biggest number in a constraint 16
Biggest sum of numbers in a constraint 3092598
Number of bits of the biggest sum of numbers22
Best result obtained on this benchmarkOPTIMUM FOUND
Best CPU time to get the best result obtained on this benchmark29.0836
Number of variables556
Total number of constraints217
Number of constraints which are clauses0
Number of constraints which are cardinality constraints (but not clauses)26
Number of constraints which are nor clauses,nor cardinality constraints191
Minimum length of a constraint1
Maximum length of a constraint48

Trace number 6205

Launcher Data

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.031
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 899.07

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        891124 kB
Buffers:         10572 kB
Cached:         106176 kB
SwapCached:        552 kB
Active:          16700 kB
Inactive:       102644 kB
HighTotal:      131008 kB
HighFree:        23996 kB
LowTotal:       903652 kB
LowFree:        867128 kB
SwapTotal:     2097892 kB
SwapFree:      2096768 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5788 kB
Slab:            18468 kB
Committed_AS:    64300 kB
PageTables:        332 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-09-20 04:42:16 (client local time) WITH STATUS 10 IN 1208.32 SECONDS
stats: 3362 7 1208.32 10

Solver Data

c Parsing PB file...
c Converting 180 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ........................................................................................ssssssssss
c ---[ 189]---> BDD-cost:    2
c ---[ 188]---> BDD-cost:    2
c ---[ 187]---> BDD-cost:    2
c ---[ 186]---> BDD-cost:    2
c ---[ 185]---> BDD-cost:    2
c ---[ 184]---> BDD-cost:    2
c ---[ 183]---> BDD-cost:    2
c ---[ 182]---> BDD-cost:    2
c ---[ 157]---> BDD-cost:    3
c ---[ 156]---> BDD-cost:    3
c ---[ 155]---> BDD-cost:    3
c ---[ 154]---> BDD-cost:    3
c ---[ 153]---> BDD-cost:    3
c ---[ 152]---> BDD-cost:    3
c ---[ 151]---> BDD-cost:    3
c ---[ 150]---> BDD-cost:    3
c ---[ 149]---> BDD-cost:    3
c ---[ 148]---> BDD-cost:    3
c ---[ 147]---> BDD-cost:    3
c ---[ 146]---> BDD-cost:    3
c ---[ 141]---> BDD-cost:    3
c ---[ 140]---> BDD-cost:    3
c ---[ 139]---> BDD-cost:    3
c ---[ 138]---> BDD-cost:    3
c ---[ 137]---> BDD-cost:    3
c ---[ 136]---> BDD-cost:    3
c ---[ 135]---> BDD-cost:    3
c ---[ 134]---> BDD-cost:    3
c ---[ 120]---> BDD-cost:    2
c ---[ 119]---> BDD-cost:    2
c ---[ 117]---> BDD-cost:    2
c ---[ 113]---> BDD-cost:    2
c ---[ 112]---> BDD-cost:    2
c ---[ 110]---> BDD-cost:    2
c ---[ 106]---> BDD-cost:    2
c ---[ 105]---> BDD-cost:    2
c ---[ 103]---> BDD-cost:    2
c ---[  99]---> BDD-cost:    2
c ---[  98]---> BDD-cost:    2
c ---[  96]---> BDD-cost:    2
c ---[  92]---> BDD-cost:    2
c ---[  91]---> BDD-cost:    2
c ---[  89]---> BDD-cost:    2
c ---[  85]---> BDD-cost:    2
c ---[  84]---> BDD-cost:    2
c ---[  82]---> BDD-cost:    2
c ---[  78]---> BDD-cost:    2
c ---[  77]---> BDD-cost:    2
c ---[  75]---> BDD-cost:    2
c ---[  71]---> BDD-cost:    2
c ---[  70]---> BDD-cost:    2
c ---[  68]---> BDD-cost:    2
c ---[  64]---> BDD-cost:    2
c ---[  63]---> BDD-cost:    2
c ---[  61]---> BDD-cost:    2
c ---[  57]---> BDD-cost:    2
c ---[  56]---> BDD-cost:    2
c ---[  54]---> BDD-cost:    2
c ---[  50]---> BDD-cost:    2
c ---[  49]---> BDD-cost:    2
c ---[  47]---> BDD-cost:    2
c ---[  43]---> BDD-cost:    2
c ---[  42]---> BDD-cost:    2
c ---[  40]---> BDD-cost:    2
c ---[  37]---> BDD-cost:  107
c ---[  36]---> Sorter-cost:  778     Base: 2 2 2
c ---[  35]---> Sorter-cost:  777     Base: 2 2 2
c ---[  34]---> BDD-cost:   21
c ---[  33]---> BDD-cost:  128
c ---[  32]---> BDD-cost:  183
c ---[  31]---> BDD-cost:   25
c ---[  30]---> Sorter-cost:  379     Base: 2 2 2
c ---[  29]---> BDD-cost:  111
c ---[  28]---> BDD-cost:  128
c ---[  27]---> BDD-cost:  105
c ---[  26]---> Sorter-cost:  778     Base: 2 2 2
c ---[  25]---> BDD-cost:  111
c ---[  24]---> BDD-cost:  105
c ---[  23]---> BDD-cost:   54
c ---[  22]---> BDD-cost:   54
c ---[  21]---> BDD-cost:   21
c ---[  15]---> Adder-cost: 273   maxlim: 12127   bits: 15/14
c ---[   9]---> Sorter-cost: 2085     Base: 2 5 2 2 2
c ---[   8]---> BDD-cost:   76
c ---[   7]---> Sorter-cost: 2550     Base: 2 5 2 2 2
c ---[   6]---> Adder-cost: 223   maxlim: 249   bits: 9/8
c ---[   5]---> BDD-cost:   48
c ---[   4]---> BDD-cost:  114
c ---[   3]---> BDD-cost:   55
c ---[   2]---> Sorter-cost: 2935     Base: 2 5 2 2 2 2
c ---[   1]---> Adder-cost: 212   maxlim: 230   bits: 9/8
c ---[   0]---> BDD-cost:   92
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   30742    79537 |   10247       0        0     nan |  0.000 % |
c |       100 |   30742    79537 |   11271     100      544     5.4 |  0.987 % |
c |       250 |   30742    79537 |   12398     250     2459     9.8 |  0.986 % |
c |       477 |   30742    79537 |   13638     477     3973     8.3 |  0.986 % |
c ==============================================================================
c Found solution: 175459
c ---[   0]---> Sorter-cost:92424     Base: 2 2 2 3 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       637 |  284458   671673 |   94819     637    11349    17.8 |  0.986 % |
c |       737 |  284437   671627 |  104300     735    12835    17.5 |  0.117 % |
c |       887 |  284035   670723 |  114730     880    13845    15.7 |  0.221 % |
c |      1114 |  284035   670723 |  126204    1107    15250    13.8 |  0.221 % |
c |      1451 |  284035   670723 |  138824    1444    17597    12.2 |  0.221 % |
c |      1958 |  282828   667995 |  152706    1939    63559    32.8 |  0.549 % |
c |      2717 |  282661   667617 |  167977    2697   148878    55.2 |  0.596 % |
c |      3856 |  271841   642801 |  184775    3781   190178    50.3 |  3.911 % |
c |      5565 |  267485   632765 |  203252    5455   244772    44.9 |  5.294 % |
c |      8129 |  258374   611785 |  223578    7920   366516    46.3 |  8.175 % |
c |     11974 |  255958   606212 |  245936   11748   726453    61.8 |  8.939 % |
c |     17740 |  250695   594032 |  270529   17444  1194291    68.5 | 10.666 % |
c |     26390 |  249167   590517 |  297582   26068  1851301    71.0 | 11.165 % |
c |     39364 |  243608   577673 |  327340   38951  2440127    62.6 | 12.969 % |
c ==============================================================================
c Found solution: 174126
c ---[   0]---> Sorter-cost:70620     Base: 2 2 2 3 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     57904 |  404098   950841 |  134699   57401  4098734    71.4 | 12.969 % |
c |     58008 |  403639   949827 |  148168   57502  4100867    71.3 | 14.245 % |
c |     58159 |  402994   948375 |  162985   57644  4103732    71.2 | 14.375 % |
c |     58384 |  402994   948375 |  179284   57869  4109174    71.0 | 14.375 % |
c |     58721 |  401268   944466 |  197212   58185  4111678    70.7 | 14.715 % |
c |     59229 |  401268   944466 |  216934   58693  4136023    70.5 | 14.715 % |
c |     59988 |  401268   944466 |  238627   59452  4283010    72.0 | 14.715 % |
c |     61127 |  401110   944098 |  262490   60582  4296313    70.9 | 14.748 % |
c |     62836 |  400965   943764 |  288739   62290  4391753    70.5 | 14.776 % |
c |     65398 |  397076   934924 |  317613   64748  4501421    69.5 | 15.543 % |
c |     69242 |  396305   933196 |  349374   68585  4939320    72.0 | 15.693 % |
c ==============================================================================
c Found solution: 172189
c ---[   0]---> Sorter-cost:69141     Base: 2 2 2 3 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     73398 |  544035  1277084 |  181345   72562  5065701    69.8 | 15.693 % |
c |     73498 |  544035  1277084 |  199479   72662  5068684    69.8 | 16.507 % |
c |     73648 |  544035  1277084 |  219427   72812  5070213    69.6 | 16.507 % |
c |     73873 |  543068  1274852 |  241370   72952  5097260    69.9 | 16.641 % |
c |     74210 |  540987  1270145 |  265507   73257  5099628    69.6 | 16.928 % |
c |     74716 |  540190  1268331 |  292057   73706  5103053    69.2 | 17.043 % |
c |     75475 |  536077  1259024 |  321263   74187  5111911    68.9 | 17.612 % |
c |     76614 |  536077  1259024 |  353390   75326  5156748    68.5 | 17.612 % |
c |     78323 |  530933  1247267 |  388729   76556  5221852    68.2 | 18.328 % |
c ==============================================================================
c Found solution: 165654
c ---[   0]---> Sorter-cost:   12     Base: 2 2 2 3 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     78741 |  531464  1248864 |  177154   76974  5254301    68.3 | 18.328 % |
c |     78842 |  530814  1247415 |  194869   77072  5256580    68.2 | 18.396 % |
c |     78994 |  530399  1246465 |  214356   77218  5264119    68.2 | 18.455 % |
c |     79219 |  530399  1246465 |  235791   77443  5280849    68.2 | 18.455 % |
c |     79556 |  530293  1246228 |  259371   77779  5290167    68.0 | 18.466 % |
c |     80062 |  530239  1246109 |  285308   78283  5319511    68.0 | 18.473 % |
c |     80821 |  530239  1246109 |  313839   79042  5399819    68.3 | 18.473 % |
c |     81960 |  530034  1245656 |  345223   80180  5665661    70.7 | 18.500 % |
c |     83669 |  524072  1232048 |  379745   81399  5764458    70.8 | 19.341 % |
c |     86231 |  522340  1228063 |  417719   83937  5900609    70.3 | 19.584 % |
c ==============================================================================
c Found solution: 165192
c ---[   0]---> Sorter-cost:68242     Base: 2 2 2 3 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     87232 |  675287  1583479 |  225095   84938  6115837    72.0 | 19.584 % |
c |     87332 |  675287  1583479 |  247604   85038  6117351    71.9 | 19.030 % |
c |     87483 |  673704  1579889 |  272364   85180  6121380    71.9 | 19.205 % |
c |     87709 |  673704  1579889 |  299601   85406  6147900    72.0 | 19.205 % |
c |     88046 |  673704  1579889 |  329561   85743  6190662    72.2 | 19.205 % |
c |     88553 |  673704  1579889 |  362517   86250  6204900    71.9 | 19.205 % |
c |     89314 |  673704  1579889 |  398769   87011  6265601    72.0 | 19.205 % |
c |     90456 |  668664  1568463 |  438646   88034  6376824    72.4 | 19.756 % |
c |     92164 |  666346  1563278 |  482511   89724  6660716    74.2 | 20.003 % |
c |     94726 |  666346  1563278 |  530762   92286  7009786    76.0 | 20.003 % |
c |     98570 |  664362  1558830 |  583838   96127  7652673    79.6 | 20.223 % |
c ==============================================================================
c Found solution: 164617
c ---[   0]---> Sorter-cost:   14     Base: 2 2 2 3 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     98680 |  664408  1559385 |  221469   96237  7659605    79.6 | 20.223 % |
c |     98781 |  664408  1559385 |  243615   96338  7666260    79.6 | 20.222 % |
c |     98931 |  663882  1558213 |  267977   96478  7669094    79.5 | 20.280 % |
c |     99156 |  663882  1558213 |  294775   96703  7674639    79.4 | 20.280 % |
c |     99494 |  663882  1558213 |  324252   97041  7682075    79.2 | 20.280 % |
c |    100000 |  662711  1555549 |  356678   97537  7702428    79.0 | 20.411 % |
c |    100761 |  658022  1544826 |  392345   98090  7724938    78.8 | 20.924 % |
c |    101902 |  657896  1544545 |  431580   99228  7828742    78.9 | 20.939 % |
c |    103612 |  656006  1540264 |  474738  100809  7919978    78.6 | 21.151 % |
c |    106174 |  653447  1534433 |  522212  103311  8338281    80.7 | 21.441 % |
c |    110018 |  653447  1534433 |  574433  107155  8992194    83.9 | 21.441 % |
c |    115784 |  650518  1527749 |  631876  112772  9214928    81.7 | 21.761 % |
c |    124433 |  650518  1527749 |  695064  121421  9889029    81.4 | 21.761 % |
c ==============================================================================
c Found solution: 163483
c ---[   0]---> Sorter-cost:   12     Base: 2 2 2 3 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    131430 |  646191  1517922 |  215397  128336 10361434    80.7 | 21.761 % |
c |    131530 |  646191  1517922 |  236936  128436 10366789    80.7 | 22.242 % |
c |    131680 |  646026  1517552 |  260630  128583 10382200    80.7 | 22.260 % |
c |    131906 |  646026  1517552 |  286693  128809 10384118    80.6 | 22.260 % |
c |    132243 |  646026  1517552 |  315362  129146 10387012    80.4 | 22.260 % |
c |    132750 |  645201  1515676 |  346899  129631 10391486    80.2 | 22.349 % |
c |    133510 |  642926  1510464 |  381588  130236 10419037    80.0 | 22.602 % |
c |    134650 |  642926  1510464 |  419747  131376 10465729    79.7 | 22.602 % |
c ==============================================================================
c Found solution: 161824
c ---[   0]---> Sorter-cost:   12     Base: 2 2 2 3 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    135225 |  642822  1510228 |  214274  131950 10510329    79.7 | 22.602 % |
c |    135328 |  642822  1510228 |  235701  132053 10515914    79.6 | 22.614 % |
c |    135478 |  642047  1508455 |  259271  132190 10518344    79.6 | 22.694 % |
c |    135703 |  642047  1508455 |  285198  132415 10522658    79.5 | 22.694 % |
c |    136040 |  641491  1507180 |  313718  132743 10524190    79.3 | 22.755 % |
c |    136547 |  641393  1506955 |  345090  133249 10584627    79.4 | 22.766 % |
c |    137306 |  641201  1506523 |  379599  134000 10677526    79.7 | 22.785 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v -x_0x2e__0x2e__0x2e_0101_bit0 -x_0x2e__0x2e__0x2e_0101_bit1 -x_0x2e__0x2e__0x2e_0101_bit2 -x_0x2e__0x2e__0x2e_0101_bit3 -x_0x2e__0x2e__0x2e_0201_bit0 -x_0x2e__0x2e__0x2e_0201_bit1 -x_0x2e__0x2e__0x2e_0201_bit2 -x_0x2e__0x2e__0x2e_0201_bit3 -x_0x2e__0x2e__0x2e_0301_bit0 -x_0x2e__0x2e__0x2e_0301_bit1 x_0x2e__0x2e__0x2e_0301_bit2 -x_0x2e__0x2e__0x2e_0301_bit3 -x_0x2e__0x2e__0x2e_0401_bit0 -x_0x2e__0x2e__0x2e_0401_bit1 -x_0x2e__0x2e__0x2e_0401_bit2 -x_0x2e__0x2e__0x2e_0401_bit3 -x_0x2e__0x2e__0x2e_0701_bit0 -x_0x2e__0x2e__0x2e_0701_bit1 -x_0x2e__0x2e__0x2e_0701_bit2 -x_0x2e__0x2e__0x2e_0701_bit3 -x_0x2e__0x2e__0x2e_0801_bit0 -x_0x2e__0x2e__0x2e_0801_bit1 -x_0x2e__0x2e__0x2e_0801_bit2 -x_0x2e__0x2e__0x2e_0801_bit3 x_0x2e__0x2e__0x2e_0901_bit0 -x_0x2e__0x2e__0x2e_0901_bit1 x_0x2e__0x2e__0x2e_0901_bit2 -x_0x2e__0x2e__0x2e_0901_bit3 -x_0x2e__0x2e__0x2e_1001_bit0 -x_0x2e__0x2e__0x2e_1001_bit1 -x_0x2e__0x2e__0x2e_1001_bit2 -x_0x2e__0x2e__0x2e_1001_bit3 -x_0x2e__0x2e__0x2e_0102_bit0 -x_0x2e__0x2e__0x2e_0102_bit1 -x_0x2e__0x2e__0x2e_0102_bit2 -x_0x2e__0x2e__0x2e_0102_bit3 -x_0x2e__0x2e__0x2e_0202_bit0 -x_0x2e__0x2e__0x2e_0202_bit1 -x_0x2e__0x2e__0x2e_0202_bit2 -x_0x2e__0x2e__0x2e_0202_bit3 -x_0x2e__0x2e__0x2e_0302_bit0 -x_0x2e__0x2e__0x2e_0302_bit1 -x_0x2e__0x2e__0x2e_0302_bit2 x_0x2e__0x2e__0x2e_0302_bit3 -x_0x2e__0x2e__0x2e_0402_bit0 -x_0x2e__0x2e__0x2e_0402_bit1 -x_0x2e__0x2e__0x2e_0402_bit2 -x_0x2e__0x2e__0x2e_0402_bit3 -x_0x2e__0x2e__0x2e_0502_bit0 -x_0x2e__0x2e__0x2e_0502_bit1 x_0x2e__0x2e__0x2e_0502_bit2 -x_0x2e__0x2e__0x2e_0502_bit3 -x_0x2e__0x2e__0x2e_0602_bit0 -x_0x2e__0x2e__0x2e_0602_bit1 -x_0x2e__0x2e__0x2e_0602_bit2 -x_0x2e__0x2e__0x2e_0602_bit3 -x_0x2e__0x2e__0x2e_0702_bit0 -x_0x2e__0x2e__0x2e_0702_bit1 -x_0x2e__0x2e__0x2e_0702_bit2 -x_0x2e__0x2e__0x2e_0702_bit3 -x_0x2e__0x2e__0x2e_0802_bit0 -x_0x2e__0x2e__0x2e_0802_bit1 -x_0x2e__0x2e__0x2e_0802_bit2 -x_0x2e__0x2e__0x2e_0802_bit3 -x_0x2e__0x2e__0x2e_0902_bit0 -x_0x2e__0x2e__0x2e_0902_bit1 -x_0x2e__0x2e__0x2e_0902_bit2 -x_0x2e__0x2e__0x2e_0902_bit3 -x_0x2e__0x2e__0x2e_1002_bit0 -x_0x2e__0x2e__0x2e_1002_bit1 -x_0x2e__0x2e__0x2e_1002_bit2 -x_0x2e__0x2e__0x2e_1002_bit3 -x_0x2e__0x2e__0x2e_1102_bit0 x_0x2e__0x2e__0x2e_1102_bit1 -x_0x2e__0x2e__0x2e_1102_bit2 -x_0x2e__0x2e__0x2e_1102_bit3 -x_0x2e__0x2e__0x2e_1202_bit0 -x_0x2e__0x2e__0x2e_1202_bit1 -x_0x2e__0x2e__0x2e_1202_bit2 -x_0x2e__0x2e__0x2e_1202_bit3 x_0x2e__0x2e__0x2e_0103_bit0 -x_0x2e__0x2e__0x2e_0103_bit1 -x_0x2e__0x2e__0x2e_0103_bit2 -x_0x2e__0x2e__0x2e_0103_bit3 x_0x2e__0x2e__0x2e_0203_bit0 -x_0x2e__0x2e__0x2e_0203_bit1 x_0x2e__0x2e__0x2e_0203_bit2 -x_0x2e__0x2e__0x2e_0203_bit3 -x_0x2e__0x2e__0x2e_0303_bit0 x_0x2e__0x2e__0x2e_0303_bit1 -x_0x2e__0x2e__0x2e_0303_bit2 -x_0x2e__0x2e__0x2e_0303_bit3 x_0x2e__0x2e__0x2e_0403_bit0 -x_0x2e__0x2e__0x2e_0403_bit1 -x_0x2e__0x2e__0x2e_0403_bit2 -x_0x2e__0x2e__0x2e_0403_bit3 -x_0x2e__0x2e__0x2e_0503_bit0 -x_0x2e__0x2e__0x2e_0503_bit1 -x_0x2e__0x2e__0x2e_0503_bit2 -x_0x2e__0x2e__0x2e_0503_bit3 -x_0x2e__0x2e__0x2e_0603_bit0 -x_0x2e__0x2e__0x2e_0603_bit1 -x_0x2e__0x2e__0x2e_0603_bit2 -x_0x2e__0x2e__0x2e_0603_bit3 x_0x2e__0x2e__0x2e_0703_bit0 -x_0x2e__0x2e__0x2e_0703_bit1 -x_0x2e__0x2e__0x2e_0703_bit2 -x_0x2e__0x2e__0x2e_0703_bit3 x_0x2e__0x2e__0x2e_0803_bit0 -x_0x2e__0x2e__0x2e_0803_bit1 -x_0x2e__0x2e__0x2e_0803_bit2 -x_0x2e__0x2e__0x2e_0803_bit3 -x_0x2e__0x2e__0x2e_0903_bit0 x_0x2e__0x2e__0x2e_0903_bit1 -x_0x2e__0x2e__0x2e_0903_bit2 -x_0x2e__0x2e__0x2e_0903_bit3 x_0x2e__0x2e__0x2e_1003_bit0 -x_0x2e__0x2e__0x2e_1003_bit1 -x_0x2e__0x2e__0x2e_1003_bit2 -x_0x2e__0x2e__0x2e_1003_bit3 -x_0x2e__0x2e__0x2e_1103_bit0 -x_0x2e__0x2e__0x2e_1103_bit1 -x_0x2e__0x2e__0x2e_1103_bit2 -x_0x2e__0x2e__0x2e_1103_bit3 -x_0x2e__0x2e__0x2e_1203_bit0 -x_0x2e__0x2e__0x2e_1203_bit1 -x_0x2e__0x2e__0x2e_1203_bit2 -x_0x2e__0x2e__0x2e_1203_bit3 -x_0x2e__0x2e__0x2e_0104_bit0 -x_0x2e__0x2e__0x2e_0204_bit0 -x_0x2e__0x2e__0x2e_0304_bit0 -x_0x2e__0x2e__0x2e_0404_bit0 -x_0x2e__0x2e__0x2e_0504_bit0 -x_0x2e__0x2e__0x2e_0604_bit0 -x_0x2e__0x2e__0x2e_0704_bit0 -x_0x2e__0x2e__0x2e_0804_bit0 -x_0x2e__0x2e__0x2e_0904_bit0 -x_0x2e__0x2e__0x2e_1004_bit0 -x_0x2e__0x2e__0x2e_1104_bit0 x_0x2e__0x2e__0x2e_1204_bit0 -x_0x2e__0x2e__0x2e_0105_bit0 -x_0x2e__0x2e__0x2e_0105_bit1 -x_0x2e__0x2e__0x2e_0105_bit2 -x_0x2e__0x2e__0x2e_0205_bit0 -x_0x2e__0x2e__0x2e_0205_bit1 -x_0x2e__0x2e__0x2e_0205_bit2 -x_0x2e__0x2e__0x2e_0305_bit0 -x_0x2e__0x2e__0x2e_0305_bit1 -x_0x2e__0x2e__0x2e_0305_bit2 -x_0x2e__0x2e__0x2e_0405_bit0 -x_0x2e__0x2e__0x2e_0405_bit1 -x_0x2e__0x2e__0x2e_0405_bit2 x_0x2e__0x2e__0x2e_0505_bit0 -x_0x2e__0x2e__0x2e_0505_bit1 -x_0x2e__0x2e__0x2e_0505_bit2 x_0x2e__0x2e__0x2e_0605_bit0 -x_0x2e__0x2e__0x2e_0605_bit1 -x_0x2e__0x2e__0x2e_0605_bit2 -x_0x2e__0x2e__0x2e_0705_bit0 -x_0x2e__0x2e__0x2e_0705_bit1 -x_0x2e__0x2e__0x2e_0705_bit2 -x_0x2e__0x2e__0x2e_0805_bit0 -x_0x2e__0x2e__0x2e_0805_bit1 -x_0x2e__0x2e__0x2e_0805_bit2 -x_0x2e__0x2e__0x2e_0905_bit0 -x_0x2e__0x2e__0x2e_0905_bit1 -x_0x2e__0x2e__0x2e_0905_bit2 -x_0x2e__0x2e__0x2e_1005_bit0 -x_0x2e__0x2e__0x2e_1005_bit1 -x_0x2e__0x2e__0x2e_1005_bit2 x_0x2e__0x2e__0x2e_1105_bit0 -x_0x2e__0x2e__0x2e_1105_bit1 -x_0x2e__0x2e__0x2e_1105_bit2 x_0x2e__0x2e__0x2e_1205_bit0 -x_0x2e__0x2e__0x2e_1205_bit1 -x_0x2e__0x2e__0x2e_1205_bit2 -x_0x2e__0x2e__0x2e_0106_bit0 -x_0x2e__0x2e__0x2e_0106_bit1 -x_0x2e__0x2e__0x2e_0106_bit2 -x_0x2e__0x2e__0x2e_0106_bit3 -x_0x2e__0x2e__0x2e_0206_bit0 -x_0x2e__0x2e__0x2e_0206_bit1 -x_0x2e__0x2e__0x2e_0206_bit2 -x_0x2e__0x2e__0x2e_0206_bit3 -x_0x2e__0x2e__0x2e_0306_bit0 -x_0x2e__0x2e__0x2e_0306_bit1 x_0x2e__0x2e__0x2e_0306_bit2 -x_0x2e__0x2e__0x2e_0306_bit3 -x_0x2e__0x2e__0x2e_0406_bit0 -x_0x2e__0x2e__0x2e_0406_bit1 -x_0x2e__0x2e__0x2e_0406_bit2 -x_0x2e__0x2e__0x2e_0406_bit3 -x_0x2e__0x2e__0x2e_0506_bit0 -x_0x2e__0x2e__0x2e_0506_bit1 -x_0x2e__0x2e__0x2e_0506_bit2 -x_0x2e__0x2e__0x2e_0506_bit3 -x_0x2e__0x2e__0x2e_0606_bit0 -x_0x2e__0x2e__0x2e_0606_bit1 -x_0x2e__0x2e__0x2e_0606_bit2 -x_0x2e__0x2e__0x2e_0606_bit3 -x_0x2e__0x2e__0x2e_0706_bit0 -x_0x2e__0x2e__0x2e_0706_bit1 -x_0x2e__0x2e__0x2e_0706_bit2 -x_0x2e__0x2e__0x2e_0706_bit3 -x_0x2e__0x2e__0x2e_0806_bit0 -x_0x2e__0x2e__0x2e_0806_bit1 -x_0x2e__0x2e__0x2e_0806_bit2 -x_0x2e__0x2e__0x2e_0806_bit3 -x_0x2e__0x2e__0x2e_0906_bit0 -x_0x2e__0x2e__0x2e_0906_bit1 x_0x2e__0x2e__0x2e_0906_bit2 -x_0x2e__0x2e__0x2e_0906_bit3 -x_0x2e__0x2e__0x2e_1006_bit0 -x_0x2e__0x2e__0x2e_1006_bit1 -x_0x2e__0x2e__0x2e_1006_bit2 -x_0x2e__0x2e__0x2e_1006_bit3 -x_0x2e__0x2e__0x2e_1106_bit0 -x_0x2e__0x2e__0x2e_1106_bit1 -x_0x2e__0x2e__0x2e_1106_bit2 -x_0x2e__0x2e__0x2e_1106_bit3 -x_0x2e__0x2e__0x2e_1206_bit0 -x_0x2e__0x2e__0x2e_1206_bit1 -x_0x2e__0x2e__0x2e_1206_bit2 -x_0x2e__0x2e__0x2e_1206_bit3 x_0x2e__0x2e__0x2e_0507_bit0 -x_0x2e__0x2e__0x2e_0507_bit1 -x_0x2e__0x2e__0x2e_0507_bit2 x_0x2e__0x2e__0x2e_0607_bit0 -x_0x2e__0x2e__0x2e_0607_bit1 -x_0x2e__0x2e__0x2e_0607_bit2 x_0x2e__0x2e__0x2e_1107_bit0 -x_0x2e__0x2e__0x2e_1107_bit1 -x_0x2e__0x2e__0x2e_1107_bit2 x_0x2e__0x2e__0x2e_1207_bit0 -x_0x2e__0x2e__0x2e_1207_bit1 -x_0x2e__0x2e__0x2e_1207_bit2 -x_0x2e__0x2e__0x2e_0108_bit0 -x_0x2e__0x2e__0x2e_0108_bit1 -x_0x2e__0x2e__0x2e_0108_bit2 -x_0x2e__0x2e__0x2e_0108_bit3 -x_0x2e__0x2e__0x2e_0208_bit0 -x_0x2e__0x2e__0x2e_0208_bit1 -x_0x2e__0x2e__0x2e_0208_bit2 -x_0x2e__0x2e__0x2e_0208_bit3 -x_0x2e__0x2e__0x2e_0308_bit0 x_0x2e__0x2e__0x2e_0308_bit1 -x_0x2e__0x2e__0x2e_0308_bit2 x_0x2e__0x2e__0x2e_0308_bit3 -x_0x2e__0x2e__0x2e_0408_bit0 -x_0x2e__0x2e__0x2e_0408_bit1 -x_0x2e__0x2e__0x2e_0408_bit2 -x_0x2e__0x2e__0x2e_0408_bit3 -x_0x2e__0x2e__0x2e_0708_bit0 -x_0x2e__0x2e__0x2e_0708_bit1 -x_0x2e__0x2e__0x2e_0708_bit2 -x_0x2e__0x2e__0x2e_0708_bit3 -x_0x2e__0x2e__0x2e_0808_bit0 -x_0x2e__0x2e__0x2e_0808_bit1 -x_0x2e__0x2e__0x2e_0808_bit2 -x_0x2e__0x2e__0x2e_0808_bit3 -x_0x2e__0x2e__0x2e_0908_bit0 x_0x2e__0x2e__0x2e_0908_bit1 -x_0x2e__0x2e__0x2e_0908_bit2 -x_0x2e__0x2e__0x2e_0908_bit3 -x_0x2e__0x2e__0x2e_1008_bit0 -x_0x2e__0x2e__0x2e_1008_bit1 -x_0x2e__0x2e__0x2e_1008_bit2 -x_0x2e__0x2e__0x2e_1008_bit3 -x_0x2e__0x2e__0x2e_0109_bit0 -x_0x2e__0x2e__0x2e_0109_bit1 -x_0x2e__0x2e__0x2e_0109_bit2 -x_0x2e__0x2e__0x2e_0209_bit0 -x_0x2e__0x2e__0x2e_0209_bit1 -x_0x2e__0x2e__0x2e_0209_bit2 -x_0x2e__0x2e__0x2e_0309_bit0 -x_0x2e__0x2e__0x2e_0309_bit1 -x_0x2e__0x2e__0x2e_0309_bit2 -x_0x2e__0x2e__0x2e_0409_bit0 -x_0x2e__0x2e__0x2e_0409_bit1 -x_0x2e__0x2e__0x2e_0409_bit2 -x_0x2e__0x2e__0x2e_0509_bit0 -x_0x2e__0x2e__0x2e_0509_bit1 -x_0x2e__0x2e__0x2e_0509_bit2 x_0x2e__0x2e__0x2e_0609_bit0 x_0x2e__0x2e__0x2e_0609_bit1 -x_0x2e__0x2e__0x2e_0609_bit2 -x_0x2e__0x2e__0x2e_0709_bit0 -x_0x2e__0x2e__0x2e_0709_bit1 -x_0x2e__0x2e__0x2e_0709_bit2 x_0x2e__0x2e__0x2e_0809_bit0 -x_0x2e__0x2e__0x2e_0809_bit1 -x_0x2e__0x2e__0x2e_0809_bit2 -x_0x2e__0x2e__0x2e_0909_bit0 -x_0x2e__0x2e__0x2e_0909_bit1 -x_0x2e__0x2e__0x2e_0909_bit2 x_0x2e__0x2e__0x2e_1009_bit0 -x_0x2e__0x2e__0x2e_1009_bit1 -x_0x2e__0x2e__0x2e_1009_bit2 -x_0x2e__0x2e__0x2e_1109_bit0 -x_0x2e__0x2e__0x2e_1109_bit1 -x_0x2e__0x2e__0x2e_1109_bit2 -x_0x2e__0x2e__0x2e_1209_bit0 -x_0x2e__0x2e__0x2e_1209_bit1 -x_0x2e__0x2e__0x2e_1209_bit2 -x_0x2e__0x2e__0x2e_0110_bit0 -x_0x2e__0x2e__0x2e_0110_bit1 x_0x2e__0x2e__0x2e_0110_bit2 -x_0x2e__0x2e__0x2e_0111_bit0 -x_0x2e__0x2e__0x2e_0111_bit1 -x_0x2e__0x2e__0x2e_0111_bit2 -x_0x2e__0x2e__0x2e_0112_bit0 -x_0x2e__0x2e__0x2e_0112_bit1 -x_0x2e__0x2e__0x2e_0112_bit2 -x_0x2e__0x2e__0x2e_0112_bit3 x_0x2e__0x2e__0x2e_0113_bit0 -x_0x2e__0x2e__0x2e_0113_bit1 -x_0x2e__0x2e__0x2e_0113_bit2 -x_0x2e__0x2e__0x2e_0114_bit0 -x_0x2e__0x2e__0x2e_0114_bit1 -x_0x2e__0x2e__0x2e_0114_bit2 -x_0x2e__0x2e__0x2e_0115_bit0 x_0x2e__0x2e__0x2e_0115_bit1 x_0x2e__0x2e__0x2e_0116_bit0 -x_0x2e__0x2e__0x2e_0116_bit1 -x_0x2e__0x2e__0x2e_0117_bit0 -x_0x2e__0x2e__0x2e_0210_bit0 -x_0x2e__0x2e__0x2e_0210_bit1 -x_0x2e__0x2e__0x2e_0210_bit2 -x_0x2e__0x2e__0x2e_0211_bit0 -x_0x2e__0x2e__0x2e_0211_bit1 -x_0x2e__0x2e__0x2e_0211_bit2 -x_0x2e__0x2e__0x2e_0212_bit0 -x_0x2e__0x2e__0x2e_0212_bit1 -x_0x2e__0x2e__0x2e_0212_bit2 -x_0x2e__0x2e__0x2e_0212_bit3 -x_0x2e__0x2e__0x2e_0213_bit0 -x_0x2e__0x2e__0x2e_0213_bit1 -x_0x2e__0x2e__0x2e_0213_bit2 -x_0x2e__0x2e__0x2e_0214_bit0 -x_0x2e__0x2e__0x2e_0214_bit1 -x_0x2e__0x2e__0x2e_0214_bit2 -x_0x2e__0x2e__0x2e_0215_bit0 -x_0x2e__0x2e__0x2e_0215_bit1 -x_0x2e__0x2e__0x2e_0216_bit0 -x_0x2e__0x2e__0x2e_0216_bit1 -x_0x2e__0x2e__0x2e_0217_bit0 -x_0x2e__0x2e__0x2e_0310_bit0 -x_0x2e__0x2e__0x2e_0310_bit1 -x_0x2e__0x2e__0x2e_0310_bit2 -x_0x2e__0x2e__0x2e_0311_bit0 -x_0x2e__0x2e__0x2e_0311_bit1 -x_0x2e__0x2e__0x2e_0311_bit2 -x_0x2e__0x2e__0x2e_0312_bit0 -x_0x2e__0x2e__0x2e_0312_bit1 -x_0x2e__0x2e__0x2e_0312_bit2 -x_0x2e__0x2e__0x2e_0312_bit3 -x_0x2e__0x2e__0x2e_0313_bit0 -x_0x2e__0x2e__0x2e_0313_bit1 -x_0x2e__0x2e__0x2e_0313_bit2 -x_0x2e__0x2e__0x2e_0314_bit0 -x_0x2e__0x2e__0x2e_0314_bit1 -x_0x2e__0x2e__0x2e_0314_bit2 -x_0x2e__0x2e__0x2e_0315_bit0 -x_0x2e__0x2e__0x2e_0315_bit1 -x_0x2e__0x2e__0x2e_0316_bit0 -x_0x2e__0x2e__0x2e_0316_bit1 -x_0x2e__0x2e__0x2e_0317_bit0 -x_0x2e__0x2e__0x2e_0410_bit0 -x_0x2e__0x2e__0x2e_0410_bit1 -x_0x2e__0x2e__0x2e_0410_bit2 -x_0x2e__0x2e__0x2e_0411_bit0 -x_0x2e__0x2e__0x2e_0411_bit1 -x_0x2e__0x2e__0x2e_0411_bit2 -x_0x2e__0x2e__0x2e_0412_bit0 -x_0x2e__0x2e__0x2e_0412_bit1 -x_0x2e__0x2e__0x2e_0412_bit2 x_0x2e__0x2e__0x2e_0412_bit3 -x_0x2e__0x2e__0x2e_0413_bit0 -x_0x2e__0x2e__0x2e_0413_bit1 -x_0x2e__0x2e__0x2e_0413_bit2 -x_0x2e__0x2e__0x2e_0414_bit0 -x_0x2e__0x2e__0x2e_0414_bit1 -x_0x2e__0x2e__0x2e_0414_bit2 -x_0x2e__0x2e__0x2e_0415_bit0 -x_0x2e__0x2e__0x2e_0415_bit1 -x_0x2e__0x2e__0x2e_0416_bit0 -x_0x2e__0x2e__0x2e_0416_bit1 -x_0x2e__0x2e__0x2e_0417_bit0 -x_0x2e__0x2e__0x2e_0510_bit0 -x_0x2e__0x2e__0x2e_0510_bit1 -x_0x2e__0x2e__0x2e_0510_bit2 -x_0x2e__0x2e__0x2e_0511_bit0 -x_0x2e__0x2e__0x2e_0511_bit1 -x_0x2e__0x2e__0x2e_0511_bit2 -x_0x2e__0x2e__0x2e_0512_bit0 -x_0x2e__0x2e__0x2e_0512_bit1 -x_0x2e__0x2e__0x2e_0512_bit2 -x_0x2e__0x2e__0x2e_0512_bit3 -x_0x2e__0x2e__0x2e_0513_bit0 -x_0x2e__0x2e__0x2e_0513_bit1 -x_0x2e__0x2e__0x2e_0513_bit2 -x_0x2e__0x2e__0x2e_0514_bit0 -x_0x2e__0x2e__0x2e_0514_bit1 -x_0x2e__0x2e__0x2e_0514_bit2 -x_0x2e__0x2e__0x2e_0515_bit0 -x_0x2e__0x2e__0x2e_0515_bit1 -x_0x2e__0x2e__0x2e_0516_bit0 -x_0x2e__0x2e__0x2e_0516_bit1 -x_0x2e__0x2e__0x2e_0517_bit0 -x_0x2e__0x2e__0x2e_0610_bit0 -x_0x2e__0x2e__0x2e_0610_bit1 -x_0x2e__0x2e__0x2e_0610_bit2 -x_0x2e__0x2e__0x2e_0611_bit0 -x_0x2e__0x2e__0x2e_0611_bit1 -x_0x2e__0x2e__0x2e_0611_bit2 -x_0x2e__0x2e__0x2e_0612_bit0 -x_0x2e__0x2e__0x2e_0612_bit1 -x_0x2e__0x2e__0x2e_0612_bit2 -x_0x2e__0x2e__0x2e_0612_bit3 -x_0x2e__0x2e__0x2e_0613_bit0 -x_0x2e__0x2e__0x2e_0613_bit1 -x_0x2e__0x2e__0x2e_0613_bit2 -x_0x2e__0x2e__0x2e_0614_bit0 -x_0x2e__0x2e__0x2e_0614_bit1 -x_0x2e__0x2e__0x2e_0614_bit2 -x_0x2e__0x2e__0x2e_0615_bit0 -x_0x2e__0x2e__0x2e_0615_bit1 -x_0x2e__0x2e__0x2e_0616_bit0 -x_0x2e__0x2e__0x2e_0616_bit1 -x_0x2e__0x2e__0x2e_0617_bit0 -x_0x2e__0x2e__0x2e_0710_bit0 -x_0x2e__0x2e__0x2e_0710_bit1 -x_0x2e__0x2e__0x2e_0710_bit2 -x_0x2e__0x2e__0x2e_0711_bit0 -x_0x2e__0x2e__0x2e_0711_bit1 -x_0x2e__0x2e__0x2e_0711_bit2 -x_0x2e__0x2e__0x2e_0712_bit0 -x_0x2e__0x2e__0x2e_0712_bit1 -x_0x2e__0x2e__0x2e_0712_bit2 -x_0x2e__0x2e__0x2e_0712_bit3 x_0x2e__0x2e__0x2e_0713_bit0 -x_0x2e__0x2e__0x2e_0713_bit1 -x_0x2e__0x2e__0x2e_0713_bit2 -x_0x2e__0x2e__0x2e_0714_bit0 x_0x2e__0x2e__0x2e_0714_bit1 -x_0x2e__0x2e__0x2e_0714_bit2 -x_0x2e__0x2e__0x2e_0715_bit0 -x_0x2e__0x2e__0x2e_0715_bit1 -x_0x2e__0x2e__0x2e_0716_bit0 -x_0x2e__0x2e__0x2e_0716_bit1 -x_0x2e__0x2e__0x2e_0717_bit0 -x_0x2e__0x2e__0x2e_0810_bit0 -x_0x2e__0x2e__0x2e_0810_bit1 -x_0x2e__0x2e__0x2e_0810_bit2 -x_0x2e__0x2e__0x2e_0811_bit0 -x_0x2e__0x2e__0x2e_0811_bit1 -x_0x2e__0x2e__0x2e_0811_bit2 -x_0x2e__0x2e__0x2e_0812_bit0 -x_0x2e__0x2e__0x2e_0812_bit1 -x_0x2e__0x2e__0x2e_0812_bit2 -x_0x2e__0x2e__0x2e_0812_bit3 -x_0x2e__0x2e__0x2e_0813_bit0 -x_0x2e__0x2e__0x2e_0813_bit1 -x_0x2e__0x2e__0x2e_0813_bit2 -x_0x2e__0x2e__0x2e_0814_bit0 -x_0x2e__0x2e__0x2e_0814_bit1 -x_0x2e__0x2e__0x2e_0814_bit2 -x_0x2e__0x2e__0x2e_0815_bit0 -x_0x2e__0x2e__0x2e_0815_bit1 -x_0x2e__0x2e__0x2e_0816_bit0 -x_0x2e__0x2e__0x2e_0816_bit1 -x_0x2e__0x2e__0x2e_0817_bit0 x_0x2e__0x2e__0x2e_0910_bit0 -x_0x2e__0x2e__0x2e_0910_bit1 -x_0x2e__0x2e__0x2e_0910_bit2 -x_0x2e__0x2e__0x2e_0911_bit0 -x_0x2e__0x2e__0x2e_0911_bit1 x_0x2e__0x2e__0x2e_0911_bit2 -x_0x2e__0x2e__0x2e_0912_bit0 -x_0x2e__0x2e__0x2e_0912_bit1 -x_0x2e__0x2e__0x2e_0912_bit2 -x_0x2e__0x2e__0x2e_0912_bit3 x_0x2e__0x2e__0x2e_0913_bit0 -x_0x2e__0x2e__0x2e_0913_bit1 -x_0x2e__0x2e__0x2e_0913_bit2 x_0x2e__0x2e__0x2e_0914_bit0 -x_0x2e__0x2e__0x2e_0914_bit1 -x_0x2e__0x2e__0x2e_0914_bit2 -x_0x2e__0x2e__0x2e_0915_bit0 -x_0x2e__0x2e__0x2e_0915_bit1 -x_0x2e__0x2e__0x2e_0916_bit0 -x_0x2e__0x2e__0x2e_0916_bit1 -x_0x2e__0x2e__0x2e_0917_bit0 -x_0x2e__0x2e__0x2e_1010_bit0 -x_0x2e__0x2e__0x2e_1010_bit1 -x_0x2e__0x2e__0x2e_1010_bit2 -x_0x2e__0x2e__0x2e_1011_bit0 -x_0x2e__0x2e__0x2e_1011_bit1 -x_0x2e__0x2e__0x2e_1011_bit2 -x_0x2e__0x2e__0x2e_1012_bit0 -x_0x2e__0x2e__0x2e_1012_bit1 -x_0x2e__0x2e__0x2e_1012_bit2 -x_0x2e__0x2e__0x2e_1012_bit3 -x_0x2e__0x2e__0x2e_1013_bit0 -x_0x2e__0x2e__0x2e_1013_bit1 -x_0x2e__0x2e__0x2e_1013_bit2 -x_0x2e__0x2e__0x2e_1014_bit0 -x_0x2e__0x2e__0x2e_1014_bit1 -x_0x2e__0x2e__0x2e_1014_bit2 -x_0x2e__0x2e__0x2e_1015_bit0 -x_0x2e__0x2e__0x2e_1015_bit1 -x_0x2e__0x2e__0x2e_1016_bit0 -x_0x2e__0x2e__0x2e_1016_bit1 -x_0x2e__0x2e__0x2e_1017_bit0 x_0x2e__0x2e__0x2e_1110_bit0 -x_0x2e__0x2e__0x2e_1110_bit1 -x_0x2e__0x2e__0x2e_1110_bit2 -x_0x2e__0x2e__0x2e_1111_bit0 -x_0x2e__0x2e__0x2e_1111_bit1 -x_0x2e__0x2e__0x2e_1111_bit2 x_0x2e__0x2e__0x2e_1112_bit0 -x_0x2e__0x2e__0x2e_1112_bit1 -x_0x2e__0x2e__0x2e_1112_bit2 -x_0x2e__0x2e__0x2e_1112_bit3 x_0x2e__0x2e__0x2e_1113_bit0 -x_0x2e__0x2e__0x2e_1113_bit1 -x_0x2e__0x2e__0x2e_1113_bit2 -x_0x2e__0x2e__0x2e_1114_bit0 -x_0x2e__0x2e__0x2e_1114_bit1 -x_0x2e__0x2e__0x2e_1114_bit2 -x_0x2e__0x2e__0x2e_1115_bit0 -x_0x2e__0x2e__0x2e_1115_bit1 -x_0x2e__0x2e__0x2e_1116_bit0 -x_0x2e__0x2e__0x2e_1116_bit1 x_0x2e__0x2e__0x2e_1117_bit0 -x_0x2e__0x2e__0x2e_1210_bit0 -x_0x2e__0x2e__0x2e_1210_bit1 -x_0x2e__0x2e__0x2e_1210_bit2 -x_0x2e__0x2e__0x2e_1211_bit0 -x_0x2e__0x2e__0x2e_1211_bit1 -x_0x2e__0x2e__0x2e_1211_bit2 -x_0x2e__0x2e__0x2e_1212_bit0 -x_0x2e__0x2e__0x2e_1212_bit1 -x_0x2e__0x2e__0x2e_1212_bit2 -x_0x2e__0x2e__0x2e_1212_bit3 -x_0x2e__0x2e__0x2e_1213_bit0 -x_0x2e__0x2

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/16437/stat): 16437 (minisat+_script) R 16436 16437 21452 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1855620567 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 0 0 0
Raw data (/proc/16437/statm): 174 3 169 147 0 27 0
[pid=16437] 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=16438
New process pid=16439
New process pid=16440
execve syscall for /bin/sed executable
One traced child (pid=16439) 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=16440) exited with status: 0
One traced child (pid=16438) exited with status: 0
New process pid=16441
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc22/normalized-mps-v2-13-7-gt2.opb

[startup+10.0035 s]
Raw data (loadavg): 0.93 0.95 0.90 2/57 16441
Raw data (/proc/16437/stat): 16437 (minisat+_script) S 16436 16437 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855620567 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16437/statm): 531 226 485 147 0 384 0
[pid=16437] vsize: 2124
Raw data (/proc/16441/stat): 16441 (minisat+_64-bit) R 16437 16437 21452 0 -1 0 8677 0 0 0 932 33 0 0 25 0 1 0 1855620572 36802560 8019 4294967295 134512640 135094434 3221224448 3221223108 134553482 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16441/statm): 8985 8019 145 145 0 8840 0
[pid=16441] vsize: 35940
Current children cumulated CPU time (s) 9.66
Current children cumulated vsize (Kb) 38064

[startup+20.0042 s]
Raw data (loadavg): 0.94 0.96 0.91 2/57 16441
Raw data (/proc/16437/stat): 16437 (minisat+_script) S 16436 16437 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855620567 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16437/statm): 531 226 485 147 0 384 0
[pid=16437] vsize: 2124
Raw data (/proc/16441/stat): 16441 (minisat+_64-bit) R 16437 16437 21452 0 -1 0 8866 0 0 0 1930 34 0 0 25 0 1 0 1855620572 37457920 8208 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16441/statm): 9145 8208 145 145 0 9000 0
[pid=16441] vsize: 36580
Current children cumulated CPU time (s) 19.65
Current children cumulated vsize (Kb) 38704

[startup+30.0049 s]
Raw data (loadavg): 0.95 0.96 0.91 2/57 16441
Raw data (/proc/16437/stat): 16437 (minisat+_script) S 16436 16437 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855620567 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16437/statm): 531 226 485 147 0 384 0
[pid=16437] vsize: 2124
Raw data (/proc/16441/stat): 16441 (minisat+_64-bit) R 16437 16437 21452 0 -1 0 8921 0 0 0 2929 35 0 0 25 0 1 0 1855620572 37691392 8263 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16441/statm): 9202 8263 145 145 0 9057 0
[pid=16441] vsize: 36808
Current children cumulated CPU time (s) 29.65
Current children cumulated vsize (Kb) 38932

[startup+40.0056 s]
Raw data (loadavg): 0.95 0.96 0.91 2/57 16441
Raw data (/proc/16437/stat): 16437 (minisat+_script) S 16436 16437 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855620567 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16437/statm): 531 226 485 147 0 384 0
[pid=16437] vsize: 2124
Raw data (/proc/16441/stat): 16441 (minisat+_64-bit) R 16437 16437 21452 0 -1 0 9009 0 0 0 3928 36 0 0 25 0 1 0 1855620572 38043648 8351 4294967295 134512640 135094434 3221224448 3221223104 134557863 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16441/statm): 9288 8351 145 145 0 9143 0
[pid=16441] vsize: 37152
Current children cumulated CPU time (s) 39.65
Current children cumulated vsize (Kb) 39276

[startup+50.0064 s]
Raw data (loadavg): 0.96 0.96 0.91 2/57 16441
Raw data (/proc/16437/stat): 16437 (minisat+_script) S 16436 16437 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855620567 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16437/statm): 531 226 485 147 0 384 0
[pid=16437] vsize: 2124
Raw data (/proc/16441/stat): 16441 (minisat+_64-bit) R 16437 16437 21452 0 -1 0 9232 0 0 0 4926 37 0 0 25 0 1 0 1855620572 38977536 8574 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16441/statm): 9516 8574 145 145 0 9371 0
[pid=16441] vsize: 38064
Current children cumulated CPU time (s) 49.64
Current children cumulated vsize (Kb) 40188

[startup+60.0071 s]
Raw data (loadavg): 0.97 0.96 0.91 2/57 16441
Raw data (/proc/16437/stat): 16437 (minisat+_script) S 16436 16437 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855620567 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16437/statm): 531 226 485 147 0 384 0
[pid=16437] vsize: 2124
Raw data (/proc/16441/stat): 16441 (minisat+_64-bit) R 16437 16437 21452 0 -1 0 9393 0 0 0 5923 38 0 0 25 0 1 0 1855620572 39632896 8735 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16441/statm): 9676 8735 145 145 0 9531 0
[pid=16441] vsize: 38704
Current children cumulated CPU time (s) 59.62
Current children cumulated vsize (Kb) 40828

[startup+70.0078 s]
Raw data (loadavg): 0.97 0.96 0.91 2/57 16441
Raw data (/proc/16437/stat): 16437 (minisat+_script) S 16436 16437 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855620567 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16437/statm): 531 226 485 147 0 384 0
[pid=16437] vsize: 2124
Raw data (/proc/16441/stat): 16441 (minisat+_64-bit) R 16437 16437 21452 0 -1 0 9480 0 0 0 6922 39 0 0 25 0 1 0 1855620572 39985152 8822 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16441/statm): 9762 8822 145 145 0 9617 0
[pid=16441] vsize: 39048
Current children cumulated CPU time (s) 69.62
Current children cumulated vsize (Kb) 41172

[startup+80.0085 s]
Raw data (loadavg): 0.98 0.96 0.91 2/57 16441
Raw data (/proc/16437/stat): 16437 (minisat+_script) S 16436 16437 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855620567 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16437/statm): 531 226 485 147 0 384 0
[pid=16437] vsize: 2124
Raw data (/proc/16441/stat): 16441 (minisat+_64-bit) R 16437 16437 21452 0 -1 0 9803 0 0 0 7916 41 0 0 25 0 1 0 1855620572 41295872 9145 4294967295 134512640 135094434 3221224448 3221223040 134557180 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16441/statm): 10082 9145 145 145 0 9937 0
[pid=16441] vsize: 40328
Current children cumulated CPU time (s) 79.58
Current children cumulated vsize (Kb) 42452

[startup+90.0092 s]
Raw data (loadavg): 0.98 0.96 0.91 2/57 16441
Raw data (/proc/16437/stat): 16437 (minisat+_script) S 16436 16437 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855620567 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16437/statm): 531 226 485 147 0 384 0
[pid=16437] vsize: 2124
Raw data (/proc/16441/stat): 16441 (minisat+_64-bit) R 16437 16437 21452 0 -1 0 10011 0 0 0 8913 42 0 0 25 0 1 0 1855620572 42205184 9353 4294967295 134512640 135094434 3221224448 3221223040 134557537 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16441/statm): 10304 9353 145 145 0 10159 0
[pid=16441] vsize: 41216
Current children cumulated CPU time (s) 89.56
Current children cumulated vsize (Kb) 43340

[startup+100.01 s]
Raw data (loadavg): 0.98 0.96 0.91 2/57 16441
Raw data (/proc/16437/stat): 16437 (minisat+_script) S 16436 16437 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855620567 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16437/statm): 531 226 485 147 0 384 0
[pid=16437] vsize: 2124
Raw data (/proc/16441/stat): 16441 (minisat+_64-bit) R 16437 16437 21452 0 -1 0 10155 0 0 0 9911 43 0 0 25 0 1 0 1855620572 42790912 9497 4294967295 134512640 135094434 3221224448 3221223072 134557574 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16441/statm): 10447 9497 145 145 0 10302 0
[pid=16441] vsize: 41788
Current children cumulated CPU time (s) 99.55
Current children cumulated vsize (Kb) 43912

[startup+110.011 s]
Raw data (loadavg): 0.98 0.96 0.91 2/57 16441
Raw data (/proc/16437/stat): 16437 (minisat+_script) S 16436 16437 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855620567 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16437/statm): 531 226 485 147 0 384 0
[pid=16437] vsize: 2124
Raw data (/proc/16441/stat): 16441 (minisat+_64-bit) R 16437 16437 21452 0 -1 0 10324 0 0 0 10908 44 0 0 25 0 1 0 1855620572 43479040 9666 4294967295 134512640 135094434 3221224448 3221223072 134557568 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16441/statm): 10615 9666 145 145 0 10470 0
[pid=16441] vsize: 42460
Current children cumulated CPU time (s) 109.53
Current children cumulated vsize (Kb) 44584

[startup+120.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16441
Raw data (/proc/16437/stat): 16437 (minisat+_script) S 16436 16437 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855620567 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16437/statm): 531 226 485 147 0 384 0
[pid=16437] vsize: 2124
Raw data (/proc/16441/stat): 16441 (minisat+_64-bit) R 16437 16437 21452 0 -1 0 10436 0 0 0 11906 45 0 0 25 0 1 0 1855620572 43925504 9778 4294967295 134512640 135094434 3221224448 3221223108 134553508 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16441/statm): 10724 9778 145 145 0 10579 0
[pid=16441] vsize: 42896
Current children cumulated CPU time (s) 119.52
Current children cumulated vsize (Kb) 45020

[startup+130.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16441
Raw data (/proc/16437/stat): 16437 (minisat+_script) S 16436 16437 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855620567 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16437/statm): 531 226 485 147 0 384 0
[pid=16437] vsize: 2124
Raw data (/proc/16441/stat): 16441 (minisat+_64-bit) R 16437 16437 21452 0 -1 0 10715 0 0 0 12900 48 0 0 25 0 1 0 1855620572 45056000 10057 4294967295 134512640 135094434 3221224448 3221223072 134557596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16441/statm): 11000 10057 145 145 0 10855 0
[pid=16441] vsize: 44000
Current children cumulated CPU time (s) 129.49
Current children cumulated vsize (Kb) 46124

[startup+140.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16441
Raw data (/proc/16437/stat): 16437 (minisat+_script) S 16436 16437 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855620567 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16437/statm): 531 226 485 147 0 384 0
[pid=16437] vsize: 2124
Raw data (/proc/16441/stat): 16441 (minisat+_64-bit) R 16437 16437 21452 0 -1 0 10773 0 0 0 13900 48 0 0 25 0 1 0 1855620572 45285376 10115 4294967295 134512640 135094434 3221224448 3221223108 134553497 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16441/statm): 11056 10115 145 145 0 10911 0
[pid=16441] vsize: 44224
Current children cumulated CPU time (s) 139.49
Current children cumulated vsize (Kb) 46348

[startup+150.013 s]
Raw data (loadavg): 1.06 0.98 0.91 2/57 16441
Raw data (/proc/16437/stat): 16437 (minisat+_script) S 16436 16437 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855620567 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16437/statm): 531 226 485 147 0 384 0
[pid=16437] vsize: 2124
Raw data (/proc/16441/stat): 16441 (minisat+_64-bit) R 16437 16437 21452 0 -1 0 10981 0 0 0 14897 49 0 0 25 0 1 0 1855620572 46120960 10323 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16441/statm): 11260 10323 145 145 0 11115 0
[pid=16441] vsize: 45040
Current children cumulated CPU time (s) 149.47
Current children cumulated vsize (Kb) 47164

[startup+160.014 s]
Raw data (loadavg): 1.05 0.98 0.91 2/57 16441
Raw data (/proc/16437/stat): 16437 (minisat+_script) S 16436 16437 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855620567 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16437/statm): 531 226 485 147 0 384 0
[pid=16437] vsize: 2124
Raw data (/proc/16441/stat): 16441 (minisat+_64-bit) R 16437 16437 21452 0 -1 0 11265 0 0 0 15892 51 0 0 25 0 1 0 1855620572 47398912 10607 4294967295 134512640 135094434 3221224448 3221223104 134558402 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16441/statm): 11572 10607 145 145 0 11427 0
[pid=16441] vsize: 46288
Current children cumulated CPU time (s) 159.44
Current children cumulated vsize (Kb) 48412

[startup+170.015 s]
Raw data (loadavg): 1.04 0.98 0.91 2/57 16441
Raw data (/proc/16437/stat): 16437 (minisat+_script) S 16436 16437 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855620567 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16437/statm): 531 226 485 147 0 384 0
[pid=16437] vsize: 2124
Raw data (/proc/16441/stat): 16441 (minisat+_64-bit) R 16437 16437 21452 0 -1 0 11507 0 0 0 16889 53 0 0 25 0 1 0 1855620572 48381952 10849 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16441/statm): 11812 10849 145 145 0 11667 0
[pid=16441] vsize: 47248
Current children cumulated CPU time (s) 169.43
Current children cumulated vsize (Kb) 49372

[startup+180.016 s]
Raw data (loadavg): 1.04 0.98 0.91 2/57 16441
Raw data (/proc/16437/stat): 16437 (minisat+_script) S 16436 16437 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855620567 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16437/statm): 531 226 485 147 0 384 0
[pid=16437] vsize: 2124
Raw data (/proc/16441/stat): 16441 (minisat+_64-bit) R 16437 16437 21452 0 -1 0 11788 0 0 0 17887 54 0 0 25 0 1 0 1855620572 49528832 11130 4294967295 134512640 135094434 3221224448 3221223040 134557227 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16441/statm): 12092 11130 145 145 0 11947 0
[pid=16441] vsize: 48368
Current children cumulated CPU time (s) 179.42
Current children cumulated vsize (Kb) 50492

[startup+190.016 s]
Raw data (loadavg): 1.03 0.98 0.91 2/57 16441
Raw data (/proc/16437/stat): 16437 (minisat+_script) S 16436 16437 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855620567 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16437/statm): 531 226 485 147 0 384 0
[pid=16437] vsize: 2124
Raw data (/proc/16441/stat): 16441 (minisat+_64-bit) R 16437 16437 21452 0 -1 0 12010 0 0 0 18886 54 0 0 25 0 1 0 1855620572 50434048 11352 4294967295 134512640 135094434 3221224448 3221223040 134557407 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16441/statm): 12313 11352 145 145 0 12168 0
[pid=16441] vsize: 49252
Current children cumulated CPU time (s) 189.41
Current children cumulated vsize (Kb) 51376

[startup+200.017 s]
Raw data (loadavg): 1.03 0.98 0.91 2/57 16441
Raw data (/proc/16437/stat): 16437 (minisat+_script) S 16436 16437 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855620567 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16437/statm): 531 226 485 147 0 384 0
[pid=16437] vsize: 2124
Raw data (/proc/16441/stat): 16441 (minisat+_64-bit) R 16437 16437 21452 0 -1 0 12202 0 0 0 19885 55 0 0 25 0 1 0 1855620572 51273728 11544 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16441/statm): 12518 11544 145 145 0 12373 0
[pid=16441] vsize: 50072
Current children cumulated CPU time (s) 199.41
Current children cumulated vsize (Kb) 52196

[startup+210.018 s]
Raw data (loadavg): 1.02 0.98 0.91 2/57 16441
Raw data (/proc/16437/stat): 16437 (minisat+_script) S 16436 16437 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855620567 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16437/statm): 531 226 485 147 0 384 0
[pid=16437] vsize: 2124
Raw data (/proc/16441/stat): 16441 (minisat+_64-bit) T 16437 16437 21452 0 -1 0 12290 0 0 0 20884 55 0 0 25 0 1 0 1855620572 51630080 11632 4294967295 134512640 135094434 3221224448 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/16441/statm): 12605 11632 145 145 0 12460 0
[pid=16441] vsize: 50420
Current children cumulated CPU time (s) 209.4
Current children cumulated vsize (Kb) 52544

[startup+220.018 s]
Raw data (loadavg): 1.02 0.98 0.91 2/57 16441
Raw data (/proc/16437/stat): 16437 (minisat+_script) S 16436 16437 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855620567 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16437/statm): 531 226 485 147 0 384 0
[pid=16437] vsize: 2124
Raw data (/proc/16441/stat): 16441 (minisat+_64-bit) R 16437 16437 21452 0 -1 0 12386 0 0 0 21882 56 0 0 25 0 1 0 1855620572 52019200 11728 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16441/statm): 12700 11728 145 145 0 12555 0
[pid=16441] vsize: 50800
Current children cumulated CPU time (s) 219.39
Current children cumulated vsize (Kb) 52924

[startup+230.018 s]
Raw data (loadavg): 1.01 0.98 0.91 2/57 16441
Raw data (/proc/16437/stat): 16437 (minisat+_script) S 16436 16437 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855620567 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16437/statm): 531 226 485 147 0 384 0
[pid=16437] vsize: 2124
Raw data (/proc/16441/stat): 16441 (minisat+_64-bit) R 16437 16437 21452 0 -1 0 12508 0 0 0 22881 57 0 0 25 0 1 0 1855620572 52514816 11850 4294967295 134512640 135094434 3221224448 3221223136 134554731 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16441/statm): 12821 11850 145 145 0 12676 0
[pid=16441] vsize: 51284
Current children cumulated CPU time (s) 229.39
Current children cumulated vsize (Kb) 53408

[startup+240.019 s]
Raw data (loadavg): 1.01 0.98 0.91 2/57 16441
Raw data (/proc/16437/stat): 16437 (minisat+_script) S 16436 16437 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855620567 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16437/statm): 531 226 485 147 0 384 0
[pid=16437] vsize: 2124
Raw data (/proc/16441/stat): 16441 (minisat+_64-bit) R 16437 16437 21452 0 -1 0 12640 0 0 0 23879 58 0 0 25 0 1 0 1855620572 53051392 11982 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16441/statm): 12952 11982 145 145 0 12807 0
[pid=16441] vsize: 51808
Current children cumulated CPU time (s) 239.38
Current children cumulated vsize (Kb) 53932

[startup+250.02 s]
Raw data (loadavg): 1.01 0.98 0.91 2/57 16441
Raw data (/proc/16437/stat): 16437 (minisat+_script) S 16436 16437 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855620567 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16437/statm): 531 226 485 147 0 384 0
[pid=16437] vsize: 2124
Raw data (/proc/16441/stat): 16441 (minisat+_64-bit) R 16437 16437 21452 0 -1 0 12764 0 0 0 24877 59 0 0 25 0 1 0 1855620572 53542912 12106 4294967295 134512640 135094434 3221224448 3221223072 134562104 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16441/statm): 13072 12106 145 145 0 12927 0
[pid=16441] vsize: 52288
Current children cumulated CPU time (s) 249.37
Current children cumulated vsize (Kb) 54412

[startup+260.02 s]
Raw data (loadavg): 1.01 0.98 0.91 2/57 16441
Raw data (/proc/16437/stat): 16437 (minisat+_script) S 16436 16437 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855620567 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16437/statm): 531 226 485 147 0 384 0
[pid=16437] vsize: 2124
Raw data (/proc/16441/stat): 16441 (minisat+_64-bit) R 16437 16437 21452 0 -1 0 12935 0 0 0 25875 60 0 0 25 0 1 0 1855620572 54247424 12277 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16441/statm): 13244 12277 145 145 0 13099 0
[pid=16441] vsize: 52976
Current children cumulated CPU time (s) 259.36
Current children cumulated vsize (Kb) 55100

[startup+270.021 s]
Raw data (loadavg): 1.01 0.98 0.91 2/57 16441
Raw data (/proc/16437/stat): 16437 (minisat+_script) S 16436 16437 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855620567 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16437/statm): 531 226 485 147 0 384 0
[pid=16437] vsize: 2124
Raw data (/proc/16441/stat): 16441 (minisat+_64-bit) R 16437 16437 21452 0 -1 0 13112 0 0 0 26873 61 0 0 25 0 1 0 1855620572 54968320 12454 4294967295 134512640 135094434 3221224448 3221223104 134558221 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16441/statm): 13420 12454 145 145 0 13275 0
[pid=16441] vsize: 53680
Current children cumulated CPU time (s) 269.35
Current children cumulated vsize (Kb) 55804

[startup+280.022 s]
Raw data (loadavg): 1.00 0.98 0.91 2/57 16441
Raw data (/proc/16437/stat): 16437 (minisat+_script) S 16436 16437 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855620567 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16437/statm): 531 226 485 147 0 384 0
[pid=16437] vsize: 2124
Raw data (/proc/16441/stat): 16441 (minisat+_64-bit) R 16437 16437 21452 0 -1 0 13850 0 0 0 27869 63 0 0 25 0 1 0 1855620572 57036800 12902 4294967295 134512640 135094434 3221224448 3221221472 134676539 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16441/statm): 13925 12902 145 145 0 13780 0
[pid=16441] vsize: 55700
Current children cumulated CPU time (s) 279.33
Current children cumulated vsize (Kb) 57824

[startup+290.022 s]
Raw data (loadavg): 1.00 0.98 0.91 2/57 16441
Raw data (/proc/16437/stat): 16437 (minisat+_script) S 16436 16437 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855620567 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16437/statm): 531 226 485 147 0 384 0
[pid=16437] vsize: 2124
Raw data (/proc/16441/stat): 16441 (minisat+_64-bit) R 16437 16437 21452 0 -1 0 19017 0 0 0 28831 82 0 0 25 0 1 0 1855620572 81887232 17739 4294967295 134512640 135094434 3221224448 3221223104 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16441/statm): 19992 17739 145 145 0 19847 0
[pid=16441] vsize: 79968
Current children cumulated CPU time (s) 289.14
Current children cumulated vsize (Kb) 82092

[startup+300.023 s]
Raw data (loadavg): 1.00 0.98 0.91 2/57 16441
Raw data (/proc/16437/stat): 16437 (minisat+_script) S 16436 16437 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855620567 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16437/statm): 531 226 485 147 0 384 0
[pid=16437] vsize: 2124
Raw data (/proc/16441/stat): 16441 (minisat+_64-bit) R 16437 16437 21452 0 -1 0 19120 0 0 0 29830 83 0 0 25 0 1 0 1855620572 82153472 17842 4294967295 134512640 135094434 3221224448 3221223040 134556789 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16441/statm): 20057 17842 145 145 0 19912 0
[pid=16441] vsize: 80228
Current children cumulated CPU time (s) 299.14
Current children cumulated vsize (Kb) 82352

[startup+310.024 s]
Raw data (loadavg): 1.00 0.98 0.91 2/57 16441
Raw data (/proc/16437/stat): 16437 (minisat+_script) S 16436 16437 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855620567 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16437/statm): 531 226 485 147 0 384 0
[pid=16437] vsize: 2124
Raw data (/proc/16441/stat): 16441 (minisat+_64-bit) R 16437 16437 21452 0 -1 0 19255 0 0 0 30828 83 0 0 25 0 1 0 1855620572 82702336 17977 4294967295 134512640 135094434 3221224448 3221223072 134562085 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16441/statm): 20191 17977 145 145 0 20046 0
[pid=16441] vsize: 80764
Current children cumulated CPU time (s) 309.12
Current children cumulated vsize (Kb) 82888

[startup+320.025 s]
Raw data (loadavg): 1.00 0.98 0.91 2/57 16441
Raw data (/proc/16437/stat): 16437 (minisat+_script) S 16436 16437 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855620567 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16437/statm): 531 226 485 147 0 384 0
[pid=16437] vsize: 2124
Raw data (/proc/16441/stat): 16441 (minisat+_64-bit) R 16437 16437 21452 0 -1 0 19393 0 0 0 31826 84 0 0 25 0 1 0 1855620572 83275776 18115 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16441/statm): 20331 18115 145 145 0 20186 0
[pid=16441] vsize: 81324
Current children cumulated CPU time (s) 319.11
Current children cumulated vsize (Kb) 83448

[startup+330.025 s]
Raw data (loadavg): 1.00 0.98 0.91 2/57 16441
Raw data (/proc/16437/stat): 16437 (minisat+_script) S 16436 16437 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855620567 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16437/statm): 531 226 485 147 0 384 0
[pid=16437] vsize: 2124
Raw data (/proc/16441/stat): 16441 (minisat+_64-bit) R 16437 16437 21452 0 -1 0 19452 0 0 0 32825 85 0 0 25 0 1 0 1855620572 83509248 18174 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16441/statm): 20388 18174 145 145 0 20243 0
[pid=16441] vsize: 81552
Current children cumulated CPU time (s) 329.11
Current children cumulated vsize (Kb) 83676

[startup+340.026 s]
Raw data (loadavg): 1.00 0.98 0.91 2/57 16441
Raw data (/proc/16437/stat): 16437 (minisat+_script) S 16436 16437 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855620567 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16437/statm): 531 226 485 147 0 384 0
[pid=16437] vsize: 2124
Raw data (/proc/16441/stat): 16441 (minisat+_64-bit) R 16437 16437 21452 0 -1 0 19516 0 0 0 33825 85 0 0 25 0 1 0 1855620572 83763200 18238 4294967295 134512640 135094434 3221224448 3221223108 134553536 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16441/statm): 20450 18238 145 145 0 20305 0
[pid=16441] vsize: 81800
Current children cumulated CPU time (s) 339.11
Current children cumulated vsize (Kb) 83924

[startup+350.026 s]
Raw data (loadavg): 1.00 0.98 0.91 2/57 16441
Raw data (/proc/16437/stat): 16437 (minisat+_script) S 16436 16437 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855620567 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16437/statm): 531 226 485 147 0 384 0
[pid=16437] vsize: 2124
Raw data (/proc/16441/stat): 16441 (minisat+_64-bit) R 16437 16437 21452 0 -1 0 19834 0 0 0 34820 87 0 0 25 0 1 0 1855620572 85327872 18556 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16441/statm): 20832 18556 145 145 0 20687 0
[pid=16441] vsize: 83328
Current children cumulated CPU time (s) 349.08
Current children cumulated vsize (Kb) 85452

[startup+360.027 s]
Raw data (loadavg): 1.00 0.98 0.91 2/57 16441
Raw data (/proc/16437/stat): 16437 (minisat+_script) S 16436 16437 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855620567 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16437/statm): 531 226 485 147 0 384 0
[pid=16437] vsize: 2124
Raw data (/proc/16441/stat): 16441 (minisat+_64-bit) R 16437 16437 21452 0 -1 0 20015 0 0 0 35818 88 0 0 25 0 1 0 1855620572 86069248 18737 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16441/statm): 21013 18737 145 145 0 20868 0
[pid=16441] vsize: 84052
Current children cumulated CPU time (s) 359.07
Current children cumulated vsize (Kb) 86176

[startup+370.028 s]
Raw data (loadavg): 1.00 0.98 0.91 2/57 16441
Raw data (/proc/16437/stat): 16437 (minisat+_script) S 16436 16437 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855620567 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16437/statm): 531 226 485 147 0 384 0
[pid=16437] vsize: 2124
Raw data (/proc/16441/stat): 16441 (minisat+_64-bit) R 16437 16437 21452 0 -1 0 20028 0 0 0 36818 88 0 0 25 0 1 0 1855620572 86118400 18750 4294967295 134512640 135094434 3221224448 3221223108 134553482 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16441/statm): 21025 18750 145 145 0 20880 0
[pid=16441] vsize: 84100
Current children cumulated CPU time (s) 369.07
Current children cumulated vsize (Kb) 86224

[startup+380.029 s]
Raw data (loadavg): 1.00 0.98 0.91 2/57 16441
Raw data (/proc/16437/stat): 16437 (minisat+_script) S 16436 16437 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855620567 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16437/statm): 531 226 485 147 0 384 0
[pid=16437] vsize: 2124
Raw data (/proc/16441/stat): 16441 (minisat+_64-bit) R 16437 16437 21452 0 -1 0 20104 0 0 0 37817 89 0 0 25 0 1 0 1855620572 86441984 18826 4294967295 134512640 135094434 3221224448 3221223104 134558405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16441/statm): 21104 18826 145 145 0 20959 0
[pid=16441] vsize: 84416
Current children cumulated CPU time (s) 379.07
Current children cumulated vsize (Kb) 86540

[startup+390.031 s]
Raw data (loadavg): 1.00 0.98 0.91 2/57 16441
Raw data (/proc/16437/stat): 16437 (minisat+_script) S 16436 16437 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855620567 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16437/statm): 531 226 485 147 0 384 0
[pid=16437] vsize: 2124
Raw data (/proc/16441/stat): 16441 (minisat+_64-bit) R 16437 16437 21452 0 -1 0 20118 0 0 0 38817 89 0 0 25 0 1 0 1855620572 86495232 18840 4294967295 134512640 135094434 3221224448 3221223072 134557696 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16441/statm): 21117 18840 145 145 0 20972 0
[pid=16441] vsize: 84468
Current children cumulated CPU time (s) 389.07
Current children cumulated vsize (Kb) 86592

[startup+400.031 s]
Raw data (loadavg): 1.00 0.98 0.91 2/57 16441
Raw data (/proc/16437/stat): 16437 (minisat+_script) S 16436 16437 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855620567 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16437/statm): 531 226 485 147 0 384 0
[pid=16437] vsize: 2124
Raw data (/proc/16441/stat): 16441 (minisat+_64-bit) R 16437 16437 21452 0 -1 0 25081 0 0 0 39779 107 0 0 23 0 1 0 1855620572 101781504 23513 4294967295 134512640 135094434 3221224448 3221223104 134557846 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16441/statm): 24849 23513 145 145 0 24704 0
[pid=16441] vsize: 99396
Current children cumulated CPU time (s) 398.87
Current children cumulated vsize (Kb) 101520

[startup+410.032 s]
Raw data (loadavg): 1.00 0.98 0.91 2/57 16441
Raw data (/proc/16437/stat): 16437 (minisat+_script) S 16436 16437 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855620567 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16437/statm): 531 226 485 147 0 384 0
[pid=16437] vsize: 2124
Raw data (/proc/16441/stat): 16441 (minisat+_64-bit) R 16437 16437 21452 0 -1 0 25164 0 0 0 40779 107 0 0 25 0 1 0 1855620572 101920768 23596 4294967295 134512640 135094434 3221224448 3221223040 134556864 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16441/statm): 24883 23596 145 145 0 24738 0
[pid=16441] vsize: 99532
Current children cumulated CPU time (s) 408.87
Current children cumulated vsize (Kb) 101656

[startup+420.033 s]
Raw data (loadavg): 1.00 0.98 0.91 2/57 16441
Raw data (/proc/16437/stat): 16437 (minisat+_script) S 16436 16437 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855620567 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16437/statm): 531 226 485 147 0 384 0
[pid=16437] vsize: 2124
Raw data (/proc/16441/stat): 16441 (minisat+_64-bit) R 16437 16437 21452 0 -1 0 25179 0 0 0 41779 107 0 0 25 0 1 0 1855620572 101965824 23611 4294967295 134512640 135094434 3221224448 3221223108 134553497 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16441/statm): 24894 23611 145 145 0 24749 0
[pid=16441] vsize: 99576
Current children cumulated CPU time (s) 418.87
Current children cumulated vsize (Kb) 101700

[startup+430.033 s]
Raw data (loadavg): 1.00 0.98 0.91 2/57 16441
Raw data (/proc/16437/stat): 16437 (minisat+_script) S 16436 16437 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855620567 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16437/statm): 531 226 485 147 0 384 0
[pid=16437] vsize: 2124
Raw data (/proc/16441/stat): 16441 (minisat+_64-bit) R 16437 16437 21452 0 -1 0 25282 0 0 0 42777 108 0 0 25 0 1 0 1855620572 102350848 23714 4294967295 134512640 135094434 3221224448 3221223060 134563071 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16441/statm): 24988 23714 145 145 0 24843 0
[pid=16441] vsize: 99952
Current children cumulated CPU time (s) 428.86
Current children cumulated vsize (Kb) 102076

[startup+440.034 s]
Raw data (loadavg): 1.00 0.98 0.91 2/57 16441
Raw data (/proc/16437/stat): 16437 (minisat+_script) S 16436 16437 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855620567 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16437/statm): 531 226 485 147 0 384 0
[pid=16437] vsize: 2124
Raw data (/proc/16441/stat): 16441 (minisat+_64-bit) R 16437 16437 21452 0 -1 0 25314 0 0 0 43777 108 0 0 25 0 1 0 1855620572 102481920 23746 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16441/statm): 25020 23746 145 145 0 24875 0
[pid=16441] vsize: 100080
Current children cumulated CPU time (s) 438.86
Current children cumulated vsize (Kb) 102204

[startup+450.035 s]
Raw data (loadavg): 1.00 0.98 0.91 2/57 16441
Raw data (/proc/16437/stat): 16437 (minisat+_script) S 16436 16437 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855620567 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16437/statm): 531 226 485 147 0 384 0
[pid=16437] vsize: 2124
Raw data (/proc/16441/stat): 16441 (minisat+_64-bit) R 16437 16437 21452 0 -1 0 26013 0 0 0 44773 111 0 0 25 0 1 0 1855620572 104505344 24155 4294967295 134512640 135094434 3221224448 3221221472 134676542 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16441/statm): 25514 24155 145 145 0 25369 0
[pid=16441] vsize: 102056
Current children cumulated CPU time (s) 448.85
Current children cumulated vsize (Kb) 104180

[startup+460.037 s]
Raw data (loadavg): 1.00 0.98 0.91 2/57 16441
Raw data (/proc/16437/stat): 16437 (minisat+_script) S 16436 16437 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855620567 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16437/statm): 531 226 485 147 0 384 0
[pid=16437] vsize: 2124
Raw data (/proc/16441/stat): 16441 (minisat+_64-bit) R 16437 16437 21452 0 -1 0 26020 0 0 0 45773 111 0 0 25 0 1 0 1855620572 104505344 24162 4294967295 134512640 135094434 3221224448 3221223108 134553499 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16441/statm): 25514 24162 145 145 0 25369 0
[pid=16441] vsize: 102056
Current children cumulated CPU time (s) 458.85
Current children cumulated vsize (Kb) 104180

[startup+470.037 s]
Raw data (loadavg): 1.00 0.98 0.91 2/57 16441
Raw data (/proc/16437/stat): 16437 (minisat+_script) S 16436 16437 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855620567 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16437/statm): 531 226 485 147 0 384 0
[pid=16437] vsize: 2124
Raw data (/proc/16441/stat): 16441 (minisat+_64-bit) R 16437 16437 21452 0 -1 0 26022 0 0 0 46773 111 0 0 25 0 1 0 1855620572 104505344 24164 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16441/statm): 25514 24164 145 145 0 25369 0
[pid=16441] vsize: 102056
Current children cumulated CPU time (s) 468.85
Current children cumulated vsize (Kb) 104180

[startup+480.038 s]
Raw data (loadavg): 1.00 0.98 0.91 2/57 16441
Raw data (/proc/16437/stat): 16437 (minisat+_script) S 16436 16437 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855620567 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16437/statm): 531 226 485 147 0 384 0
[pid=16437] vsize: 2124
Raw data (/proc/16441/stat): 16441 (minisat+_64-bit) R 16437 16437 21452 0 -1 0 26025 0 0 0 47774 111 0 0 25 0 1 0 1855620572 104505344 24167 4294967295 134512640 135094434 3221224448 3221223104 134557948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16441/statm): 25514 24167 145 145 0 25369 0
[pid=16441] vsize: 102056
Current children cumulated CPU time (s) 478.86
Current children cumulated vsize (Kb) 104180

[startup+490.039 s]
Raw data (loadavg): 1.00 0.98 0.91 2/57 16441
Raw data (/proc/16437/stat): 16437 (minisat+_script) S 16436 16437 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855620567 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16437/statm): 531 226 485 147 0 384 0
[pid=16437] vsize: 2124
Raw data (/proc/16441/stat): 16441 (minisat+_64-bit) R 16437 16437 21452 0 -1 0 26093 0 0 0 48773 112 0 0 25 0 1 0 1855620572 104783872 24235 4294967295 134512640 135094434 3221224448 3221223040 134557180 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16441/statm): 25582 24235 145 145 0 25437 0
[pid=16441] vsize: 102328
Current children cumulated CPU time (s) 488.86
Current children cumulated vsize (Kb) 104452

[startup+500.039 s]
Raw data (loadavg): 1.00 0.98 0.91 2/57 16441
Raw data (/proc/16437/stat): 16437 (minisat+_script) S 16436 16437 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855620567 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16437/statm): 531 226 485 147 0 384 0
[pid=16437] vsize: 2124
Raw data (/proc/16441/stat): 16441 (minisat+_64-bit) R 16437 16437 21452 0 -1 0 26157 0 0 0 49772 112 0 0 25 0 1 0 1855620572 105041920 24299 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16441/statm): 25645 24299 145 145 0 25500 0
[pid=16441] vsize: 102580
Current children cumulated CPU time (s) 498.85
Current children cumulated vsize (Kb) 104704

[startup+510.041 s]
Raw data (loadavg): 1.00 0.98 0.91 2/57 16441
Raw data (/proc/16437/stat): 16437 (minisat+_script) S 16436 16437 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855620567 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16437/statm): 531 226 485 147 0 384 0
[pid=16437] vsize: 2124
Raw data (/proc/16441/stat): 16441 (minisat+_64-bit) R 16437 16437 21452 0 -1 0 26221 0 0 0 50772 113 0 0 25 0 1 0 1855620572 105312256 24363 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16441/statm): 25711 24363 145 145 0 25566 0
[pid=16441] vsize: 102844
Current children cumulated CPU time (s) 508.86
Current children cumulated vsize (Kb) 104968

[startup+520.042 s]
Raw data (loadavg): 1.00 0.98 0.91 2/57 16441
Raw data (/proc/16437/stat): 16437 (minisat+_script) S 16436 16437 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855620567 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16437/statm): 531 226 485 147 0 384 0
[pid=16437] vsize: 2124
Raw data (/proc/16441/stat): 16441 (minisat+_64-bit) R 16437 16437 21452 0 -1 0 26274 0 0 0 51772 113 0 0 25 0 1 0 1855620572 105533440 24416 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16441/statm): 25765 24416 145 145 0 25620 0
[pid=16441] vsize: 103060
Current children cumulated CPU time (s) 518.86
Current children cumulated vsize (Kb) 105184

[startup+530.043 s]
Raw data (loadavg): 1.00 0.98 0.91 2/57 16441
Raw data (/proc/16437/stat): 16437 (minisat+_script) S 16436 16437 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855620567 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16437/statm): 531 226 485 147 0 384 0
[pid=16437] vsize: 2124
Raw data (/proc/16441/stat): 16441 (minisat+_64-bit) R 16437 16437 21452 0 -1 0 26297 0 0 0 52772 113 0 0 25 0 1 0 1855620572 105619456 24439 4294967295 134512640 135094434 3221224448 3221223108 134553489 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16441/statm): 25786 24439 145 145 0 25641 0
[pid=16441] vsize: 103144
Current children cumulated CPU time (s) 528.86
Current children cumulated vsize (Kb) 105268

[startup+540.043 s]
Raw data (loadavg): 1.00 0.98 0.91 2/57 16441
Raw data (/proc/16437/stat): 16437 (minisat+_script) S 16436 16437 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855620567 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16437/statm): 531 226 485 147 0 384 0
[pid=16437] vsize: 2124
Raw data (/proc/16441/stat): 16441 (minisat+_64-bit) R 16437 16437 21452 0 -1 0 26329 0 0 0 53771 113 0 0 25 0 1 0 1855620572 105746432 24471 4294967295 134512640 135094434 3221224448 3221223104 134558129 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16441/statm): 25817 24471 145 145 0 25672 0
[pid=16441] vsize: 103268
Current children cumulated CPU time (s) 538.85
Current children cumulated vsize (Kb) 105392

[startup+550.044 s]
Raw data (loadavg): 1.00 0.98 0.91 2/57 16441
Raw data (/proc/16437/stat): 16437 (minisat+_script) S 16436 16437 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855620567 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16437/statm): 531 226 485 147 0 384 0
[pid=16437] vsize: 2124
Raw data (/proc/16441/stat): 16441 (minisat+_64-bit) R 16437 16437 21452 0 -1 0 26442 0 0 0 54769 114 0 0 25 0 1 0 1855620572 106217472 24584 4294967295 134512640 135094434 3221224448 3221223104 134558218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16441/statm): 25932 24584 145 145 0 25787 0
[pid=16441] vsize: 103728
Current children cumulated CPU time (s) 548.84
Current children cumulated vsize (Kb) 105852

[startup+560.045 s]
Raw data (loadavg): 1.00 0.98 0.91 2/57 16441
Raw data (/proc/16437/stat): 16437 (minisat+_script) S 16436 16437 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855620567 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16437/statm): 531 226 485 147 0 384 0
[pid=16437] vsize: 2124
Raw data (/proc/16441/stat): 16441 (minisat+_64-bit) R 16437 16437 21452 0 -1 0 26659 0 0 0 55767 115 0 0 25 0 1 0 1855620572 107102208 24801 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16441/statm): 26148 24801 145 145 0 26003 0
[pid=16441] vsize: 104592
Current children cumulated CPU time (s) 558.83
Current children cumulated vsize (Kb) 106716

[startup+570.045 s]
Raw data (loadavg): 1.00 0.98 0.91 2/57 16441
Raw data (/proc/16437/stat): 16437 (minisat+_script) S 16436 16437 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855620567 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16437/statm): 531 226 485 147 0 384 0
[pid=16437] vsize: 2124
Raw data (/proc/16441/stat): 16441 (minisat+_64-bit) R 16437 16437 21452 0 -1 0 31464 0 0 0 56731 131 0 0 25 0 1 0 1855620572 140767232 29316 4294967295 134512640 135094434 3221224448 3221223236 134553491 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16441/statm): 34367 29316 145 145 0 34222 0
[pid=16441] vsize: 137468
Current children cumulated CPU time (s) 568.63
Current children cumulated vsize (Kb) 139592

[startup+580.045 s]
Raw data (loadavg): 1.00 0.98 0.91 2/57 16441
Raw data (/proc/16437/stat): 16437 (minisat+_script) S 16436 16437 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855620567 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16437/statm): 531 226 485 147 0 384 0
[pid=16437] vsize: 2124
Raw data (/proc/16441/stat): 16441 (minisat+_64-bit) R 16437 16437 21452 0 -1 0 31592 0 0 0 57729 132 0 0 25 0 1 0 1855620572 141045760 29444 4294967295 134512640 135094434 3221224448 3221223072 134557596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16441/statm): 34435 29444 145 145 0 34290 0
[pid=16441] vsize: 137740
Current children cumulated CPU time (s) 578.62
Current children cumulated vsize (Kb) 139864

[startup+590.046 s]
Raw data (loadavg): 1.00 0.98 0.91 2/57 16441
Raw data (/proc/16437/stat): 16437 (minisat+_script) S 16436 16437 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855620567 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16437/statm): 531 226 485 147 0 384 0
[pid=16437] vsize: 2124
Raw data (/proc/16441/stat): 16441 (minisat+_64-bit) R 16437 16437 21452 0 -1 0 31700 0 0 0 58729 133 0 0 25 0 1 0 1855620572 141475840 29552 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16441/statm): 34540 29552 145 145 0 34395 0
[pid=16441] vsize: 138160
Current children cumulated CPU time (s) 588.63
Current children cumulated vsize (Kb) 140284

[startup+600.047 s]
Raw data (loadavg): 1.00 0.98 0.91 2/57 16441
Raw data (/proc/16437/stat): 16437 (minisat+_script) S 16436 16437 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855620567 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16437/statm): 531 226 485 147 0 384 0
[pid=16437] vsize: 2124
Raw data (/proc/16441/stat): 16441 (minisat+_64-bit) R 16437 16437 21452 0 -1 0 31756 0 0 0 59728 133 0 0 25 0 1 0 1855620572 141705216 29608 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16441/statm): 34596 29608 145 145 0 34451 0
[pid=16441] vsize: 138384
Current children cumulated CPU time (s) 598.62
Current children cumulated vsize (Kb) 140508

[startup+610.047 s]
Raw data (loadavg): 1.00 0.98 0.91 1/57 16441
Raw data (/proc/16437/stat): 16437 (minisat+_script) S 16436 16437 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855620567 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16437/statm): 531 226 485 147 0 384 0
[pid=16437] vsize: 2124
Raw data (/proc/16441/stat): 16441 (minisat+_64-bit) T 16437 16437 21452 0 -1 0 31815 0 0 0 60727 133 0 0 25 0 1 0 1855620572 141950976 29667 4294967295 134512640 135094434 3221224448 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/16441/statm): 34656 29667 145 145 0 34511 0
[pid=16441] vsize: 138624
Current children cumulated CPU time (s) 608.61
Current children cumulated vsize (Kb) 140748

[startup+620.048 s]
Raw data (loadavg): 1.00 0.98 0.91 2/57 16441
Raw data (/proc/16437/stat): 16437 (minisat+_script) S 16436 16437 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855620567 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16437/statm): 531 226 485 147 0 384 0
[pid=16437] vsize: 2124
Raw data (/proc/16441/stat): 16441 (minisat+_64-bit) R 16437 16437 21452 0 -1 0 31904 0 0 0 61726 134 0 0 25 0 1 0 1855620572 142315520 29756 4294967295 134512640 135094434 3221224448 3221223040 134557512 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16441/statm): 34745 29756 145 145 0 34600 0
[pid=16441] vsize: 138980
Current children cumulated CPU time (s) 618.61
Current children cumulated vsize (Kb) 141104

[startup+630.049 s]
Raw data (loadavg): 1.00 0.98 0.91 2/57 16441
Raw data (/proc/16437/stat): 16437 (minisat+_script) S 16436 16437 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855620567 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16437/statm): 531 226 485 147 0 384 0
[pid=16437] vsize: 2124
Raw data (/proc/16441/stat): 16441 (minisat+_64-bit) R 16437 16437 21452 0 -1 0 31919 0 0 0 62726 134 0 0 25 0 1 0 1855620572 142376960 29771 4294967295 134512640 135094434 3221224448 3221223140 134558984 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16441/statm): 34760 29771 145 145 0 34615 0
[pid=16441] vsize: 139040
Current children cumulated CPU time (s) 628.61
Current children cumulated vsize (Kb) 141164

[startup+640.05 s]
Raw data (loadavg): 1.00 0.98 0.91 2/57 16441
Raw data (/proc/16437/stat): 16437 (minisat+_script) S 16436 16437 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855620567 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16437/statm): 531 226 485 147 0 384 0
[pid=16437] vsize: 2124
Raw data (/proc/16441/stat): 16441 (minisat+_64-bit) R 16437 16437 21452 0 -1 0 32122 0 0 0 63723 135 0 0 25 0 1 0 1855620572 143208448 29974 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16441/statm): 34963 29974 145 145 0 34818 0
[pid=16441] vsize: 139852
Current children cumulated CPU time (s) 638.59
Current children cumulated vsize (Kb) 141976

[startup+650.051 s]
Raw data (loadavg): 1.00 0.98 0.91 2/57 16441
Raw data (/proc/16437/stat): 16437 (minisat+_script) S 16436 16437 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855620567 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16437/statm): 531 226 485 147 0 384 0
[pid=16437] vsize: 2124
Raw data (/proc/16441/stat): 16441 (minisat+_64-bit) R 16437 16437 21452 0 -1 0 32183 0 0 0 64722 136 0 0 25 0 1 0 1855620572 143454208 30035 4294967295 134512640 135094434 3221224448 3221223104 134558004 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16441/statm): 35023 30035 145 145 0 34878 0
[pid=16441] vsize: 140092
Current children cumulated CPU time (s) 648.59
Current children cumulated vsize (Kb) 142216

[startup+660.052 s]
Raw data (loadavg): 1.00 0.98 0.91 2/57 16441
Raw data (/proc/16437/stat): 16437 (minisat+_script) S 16436 16437 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855620567 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16437/statm): 531 226 485 147 0 384 0
[pid=16437] vsize: 2124
Raw data (/proc/16441/stat): 16441 (minisat+_64-bit) R 16437 16437 21452 0 -1 0 32243 0 0 0 65722 136 0 0 25 0 1 0 1855620572 143699968 30095 4294967295 134512640 135094434 3221224448 3221223072 134557696 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16441/statm): 35083 30095 145 145 0 34938 0
[pid=16441] vsize: 140332
Current children cumulated CPU time (s) 658.59
Current children cumulated vsize (Kb) 142456

[startup+670.053 s]
Raw data (loadavg): 1.00 0.98 0.91 2/57 16441
Raw data (/proc/16437/stat): 16437 (minisat+_script) S 16436 16437 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855620567 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16437/statm): 531 226 485 147 0 384 0
[pid=16437] vsize: 2124
Raw data (/proc/16441/stat): 16441 (minisat+_64-bit) R 16437 16437 21452 0 -1 0 32328 0 0 0 66720 137 0 0 25 0 1 0 1855620572 144044032 30180 4294967295 134512640 135094434 3221224448 3221223072 134557596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16441/statm): 35167 30180 145 145 0 35022 0
[pid=16441] vsize: 140668
Current children cumulated CPU time (s) 668.58
Current children cumulated vsize (Kb) 142792

[startup+680.053 s]
Raw data (loadavg): 1.00 0.98 0.91 2/57 16441
Raw data (/proc/16437/stat): 16437 (minisat+_script) S 16436 16437 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855620567 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16437/statm): 531 226 485 147 0 384 0
[pid=16437] vsize: 2124
Raw data (/proc/16441/stat): 16441 (minisat+_64-bit) R 16437 16437 21452 0 -1 0 32407 0 0 0 67718 138 0 0 25 0 1 0 1855620572 144367616 30259 4294967295 134512640 135094434 3221224448 3221223096 134558037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16441/statm): 35246 30259 145 145 0 35101 0
[pid=16441] vsize: 140984
Current children cumulated CPU time (s) 678.57
Current children cumulated vsize (Kb) 143108

[startup+690.055 s]
Raw data (loadavg): 1.00 0.98 0.91 2/57 16441
Raw data (/proc/16437/stat): 16437 (minisat+_script) S 16436 16437 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855620567 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16437/statm): 531 226 485 147 0 384 0
[pid=16437] vsize: 2124
Raw data (/proc/16441/stat): 16441 (minisat+_64-bit) R 16437 16437 21452 0 -1 0 32490 0 0 0 68716 139 0 0 25 0 1 0 1855620572 144703488 30342 4294967295 134512640 135094434 3221224448 3221223040 134556851 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16441/statm): 35328 30342 145 145 0 35183 0
[pid=16441] vsize: 141312
Current children cumulated CPU time (s) 688.56
Current children cumulated vsize (Kb) 143436

[startup+700.056 s]
Raw data (loadavg): 1.00 0.98 0.91 2/57 16441
Raw data (/proc/16437/stat): 16437 (minisat+_script) S 16436 16437 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855620567 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16437/statm): 531 226 485 147 0 384 0
[pid=16437] vsize: 2124
Raw data (/proc/16441/stat): 16441 (minisat+_64-bit) R 16437 16437 21452 0 -1 0 32630 0 0 0 69713 140 0 0 25 0 1 0 1855620572 145260544 30482 4294967295 134512640 135094434 3221224448 3221223040 134557230 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16441/statm): 35464 30482 145 145 0 35319 0
[pid=16441] vsize: 141856
Current children cumulated CPU time (s) 698.54
Current children cumulated vsize (Kb) 143980

[startup+710.057 s]
Raw data (loadavg): 1.00 0.98 0.91 2/57 16441
Raw data (/proc/16437/stat): 16437 (minisat+_script) S 16436 16437 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855620567 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16437/statm): 531 226 485 147 0 384 0
[pid=16437] vsize: 2124
Raw data (/proc/16441/stat): 16441 (minisat+_64-bit) R 16437 16437 21452 0 -1 0 33101 0 0 0 70703 145 0 0 25 0 1 0 1855620572 147181568 30953 4294967295 134512640 135094434 3221224448 3221223040 134557180 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16441/statm): 35933 30953 145 145 0 35788 0
[pid=16441] vsize: 143732
Current children cumulated CPU time (s) 708.49
Current children cumulated vsize (Kb) 145856

[startup+720.058 s]
Raw data (loadavg): 1.00 0.98 0.91 2/57 16441
Raw data (/proc/16437/stat): 16437 (minisat+_script) S 16436 16437 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855620567 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16437/statm): 531 226 485 147 0 384 0
[pid=16437] vsize: 2124
Raw data (/proc/16441/stat): 16441 (minisat+_64-bit) R 16437 16437 21452 0 -1 0 33804 0 0 0 71698 148 0 0 25 0 1 0 1855620572 148533248 31366 4294967295 134512640 135094434 3221224448 3221222000 134677307 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16441/statm): 36263 31366 145 145 0 36118 0
[pid=16441] vsize: 145052
Current children cumulated CPU time (s) 718.47
Current children cumulated vsize (Kb) 147176

[startup+730.059 s]
Raw data (loadavg): 1.00 0.98 0.91 2/57 16441
Raw data (/proc/16437/stat): 16437 (minisat+_script) S 16436 16437 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855620567 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16437/statm): 531 226 485 147 0 384 0
[pid=16437] vsize: 2124
Raw data (/proc/16441/stat): 16441 (minisat+_64-bit) R 16437 16437 21452 0 -1 0 33815 0 0 0 72698 148 0 0 25 0 1 0 1855620572 148598784 31377 4294967295 134512640 135094434 3221224448 3221223104 134557893 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16441/statm): 36279 31377 145 145 0 36134 0
[pid=16441] vsize: 145116
Current children cumulated CPU time (s) 728.47
Current children cumulated vsize (Kb) 147240

[startup+740.061 s]
Raw data (loadavg): 1.00 0.98 0.91 2/57 16441
Raw data (/proc/16437/stat): 16437 (minisat+_script) S 16436 16437 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855620567 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16437/statm): 531 226 485 147 0 384 0
[pid=16437] vsize: 2124
Raw data (/proc/16441/stat): 16441 (minisat+_64-bit) R 16437 16437 21452 0 -1 0 33815 0 0 0 73698 149 0 0 25 0 1 0 1855620572 148598784 31377 4294967295 134512640 135094434 3221224448 3221223072 134557593 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16441/statm): 36279 31377 145 145 0 36134 0
[pid=16441] vsize: 145116
Current children cumulated CPU time (s) 738.48
Current children cumulated vsize (Kb) 147240

[startup+750.061 s]
Raw data (loadavg): 1.00 0.98 0.91 2/57 16441
Raw data (/proc/16437/stat): 16437 (minisat+_script) S 16436 16437 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855620567 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16437/statm): 531 226 485 147 0 384 0
[pid=16437] vsize: 2124
Raw data (/proc/16441/stat): 16441 (minisat+_64-bit) R 16437 16437 21452 0 -1 0 33816 0 0 0 74697 149 0 0 25 0 1 0 1855620572 148598784 31378 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16441/statm): 36279 31378 145 145 0 36134 0
[pid=16441] vsize: 145116
Current children cumulated CPU time (s) 748.47
Current children cumulated vsize (Kb) 147240

[startup+760.063 s]
Raw data (loadavg): 1.00 0.98 0.91 2/57 16441
Raw data (/proc/16437/stat): 16437 (minisat+_script) S 16436 16437 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855620567 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16437/statm): 531 226 485 147 0 384 0
[pid=16437] vsize: 2124
Raw data (/proc/16441/stat): 16441 (minisat+_64-bit) R 16437 16437 21452 0 -1 0 33816 0 0 0 75697 150 0 0 25 0 1 0 1855620572 148598784 31378 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16441/statm): 36279 31378 145 145 0 36134 0
[pid=16441] vsize: 145116
Current children cumulated CPU time (s) 758.48
Current children cumulated vsize (Kb) 147240

[startup+770.065 s]
Raw data (loadavg): 1.00 0.98 0.91 2/57 16441
Raw data (/proc/16437/stat): 16437 (minisat+_script) S 16436 16437 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855620567 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16437/statm): 531 226 485 147 0 384 0
[pid=16437] vsize: 2124
Raw data (/proc/16441/stat): 16441 (minisat+_64-bit) R 16437 16437 21452 0 -1 0 33816 0 0 0 76696 150 0 0 25 0 1 0 1855620572 148598784 31378 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16441/statm): 36279 31378 145 145 0 36134 0
[pid=16441] vsize: 145116
Current children cumulated CPU time (s) 768.47
Current children cumulated vsize (Kb) 147240

[startup+780.065 s]
Raw data (loadavg): 1.00 0.98 0.91 2/57 16441
Raw data (/proc/16437/stat): 16437 (minisat+_script) S 16436 16437 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855620567 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16437/statm): 531 226 485 147 0 384 0
[pid=16437] vsize: 2124
Raw data (/proc/16441/stat): 16441 (minisat+_64-bit) R 16437 16437 21452 0 -1 0 33817 0 0 0 77696 151 0 0 25 0 1 0 1855620572 148598784 31379 4294967295 134512640 135094434 3221224448 3221223040 134556866 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16441/statm): 36279 31379 145 145 0 36134 0
[pid=16441] vsize: 145116
Current children cumulated CPU time (s) 778.48
Current children cumulated vsize (Kb) 147240

[startup+790.066 s]
Raw data (loadavg): 1.00 0.98 0.91 2/57 16441
Raw data (/proc/16437/stat): 16437 (minisat+_script) S 16436 16437 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855620567 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16437/statm): 531 226 485 147 0 384 0
[pid=16437] vsize: 2124
Raw data (/proc/16441/stat): 16441 (minisat+_64-bit) R 16437 16437 21452 0 -1 0 33817 0 0 0 78695 152 0 0 25 0 1 0 1855620572 148598784 31379 4294967295 134512640 135094434 3221224448 3221223104 134558426 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16441/statm): 36279 31379 145 145 0 36134 0
[pid=16441] vsize: 145116
Current children cumulated CPU time (s) 788.48
Current children cumulated vsize (Kb) 147240

[startup+800.067 s]
Raw data (loadavg): 1.00 0.98 0.91 2/57 16441
Raw data (/proc/16437/stat): 16437 (minisat+_script) S 16436 16437 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855620567 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16437/statm): 531 226 485 147 0 384 0
[pid=16437] vsize: 2124
Raw data (/proc/16441/stat): 16441 (minisat+_64-bit) R 16437 16437 21452 0 -1 0 33818 0 0 0 79694 153 0 0 25 0 1 0 1855620572 148598784 31380 4294967295 134512640 135094434 3221224448 3221223108 134553515 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16441/statm): 36279 31380 145 145 0 36134 0
[pid=16441] vsize: 145116
Current children cumulated CPU time (s) 798.48
Current children cumulated vsize (Kb) 147240

[startup+810.069 s]
Raw data (loadavg): 1.00 0.98 0.91 2/57 16441
Raw data (/proc/16437/stat): 16437 (minisat+_script) S 16436 16437 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855620567 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16437/statm): 531 226 485 147 0 384 0
[pid=16437] vsize: 2124
Raw data (/proc/16441/stat): 16441 (minisat+_64-bit) R 16437 16437 21452 0 -1 0 33876 0 0 0 80693 153 0 0 25 0 1 0 1855620572 148811776 31438 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16441/statm): 36331 31438 145 145 0 36186 0
[pid=16441] vsize: 145324
Current children cumulated CPU time (s) 808.47
Current children cumulated vsize (Kb) 147448

[startup+820.069 s]
Raw data (loadavg): 1.00 0.98 0.91 2/57 16441
Raw data (/proc/16437/stat): 16437 (minisat+_script) S 16436 16437 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855620567 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16437/statm): 531 226 485 147 0 384 0
[pid=16437] vsize: 2124
Raw data (/proc/16441/stat): 16441 (minisat+_64-bit) R 16437 16437 21452 0 -1 0 33881 0 0 0 81693 154 0 0 25 0 1 0 1855620572 148832256 31443 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16441/statm): 36336 31443 145 145 0 36191 0
[pid=16441] vsize: 145344
Current children cumulated CPU time (s) 818.48
Current children cumulated vsize (Kb) 147468

[startup+830.07 s]
Raw data (loadavg): 1.00 0.98 0.91 2/57 16441
Raw data (/proc/16437/stat): 16437 (minisat+_script) S 16436 16437 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855620567 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16437/statm): 531 226 485 147 0 384 0
[pid=16437] vsize: 2124
Raw data (/proc/16441/stat): 16441 (minisat+_64-bit) R 16437 16437 21452 0 -1 0 34077 0 0 0 82689 156 0 0 25 0 1 0 1855620572 149626880 31639 4294967295 134512640 135094434 3221224448 3221223040 134557028 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16441/statm): 36530 31639 145 145 0 36385 0
[pid=16441] vsize: 146120
Current children cumulated CPU time (s) 828.46
Current children cumulated vsize (Kb) 148244

[startup+840.072 s]
Raw data (loadavg): 1.00 0.98 0.91 2/57 16441
Raw data (/proc/16437/stat): 16437 (minisat+_script) S 16436 16437 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855620567 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16437/statm): 531 226 485 147 0 384 0
[pid=16437] vsize: 2124
Raw data (/proc/16441/stat): 16441 (minisat+_64-bit) R 16437 16437 21452 0 -1 0 34314 0 0 0 83686 157 0 0 25 0 1 0 1855620572 150589440 31876 4294967295 134512640 135094434 3221224448 3221223136 134554788 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16441/statm): 36765 31876 145 145 0 36620 0
[pid=16441] vsize: 147060
Current children cumulated CPU time (s) 838.44
Current children cumulated vsize (Kb) 149184

[startup+850.072 s]
Raw data (loadavg): 1.00 0.98 0.91 2/57 16441
Raw data (/proc/16437/stat): 16437 (minisat+_script) S 16436 16437 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855620567 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16437/statm): 531 226 485 147 0 384 0
[pid=16437] vsize: 2124
Raw data (/proc/16441/stat): 16441 (minisat+_64-bit) R 16437 16437 21452 0 -1 0 34374 0 0 0 84685 158 0 0 25 0 1 0 1855620572 150835200 31936 4294967295 134512640 135094434 3221224448 3221223120 134555574 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16441/statm): 36825 31936 145 145 0 36680 0
[pid=16441] vsize: 147300
Current children cumulated CPU time (s) 848.44
Current children cumulated vsize (Kb) 149424

[startup+860.073 s]
Raw data (loadavg): 1.00 0.98 0.91 2/57 16441
Raw data (/proc/16437/stat): 16437 (minisat+_script) S 16436 16437 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855620567 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16437/statm): 531 226 485 147 0 384 0
[pid=16437] vsize: 2124
Raw data (/proc/16441/stat): 16441 (minisat+_64-bit) R 16437 16437 21452 0 -1 0 34434 0 0 0 85684 158 0 0 25 0 1 0 1855620572 151076864 31996 4294967295 134512640 135094434 3221224448 3221223072 134557565 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16441/statm): 36884 31996 145 145 0 36739 0
[pid=16441] vsize: 147536
Current children cumulated CPU time (s) 858.43
Current children cumulated vsize (Kb) 149660

[startup+870.074 s]
Raw data (loadavg): 1.00 0.98 0.91 2/57 16441
Raw data (/proc/16437/stat): 16437 (minisat+_script) S 16436 16437 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855620567 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16437/statm): 531 226 485 147 0 384 0
[pid=16437] vsize: 2124
Raw data (/proc/16441/stat): 16441 (minisat+_64-bit) R 16437 16437 21452 0 -1 0 34531 0 0 0 86684 158 0 0 25 0 1 0 1855620572 151465984 32093 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16441/statm): 36979 32093 145 145 0 36834 0
[pid=16441] vsize: 147916
Current children cumulated CPU time (s) 868.43
Current children cumulated vsize (Kb) 150040

[startup+880.074 s]
Raw data (loadavg): 1.00 0.98 0.91 2/57 16441
Raw data (/proc/16437/stat): 16437 (minisat+_script) S 16436 16437 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855620567 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16437/statm): 531 226 485 147 0 384 0
[pid=16437] vsize: 2124
Raw data (/proc/16441/stat): 16441 (minisat+_64-bit) R 16437 16437 21452 0 -1 0 34600 0 0 0 87683 159 0 0 25 0 1 0 1855620572 151748608 32162 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16441/statm): 37048 32162 145 145 0 36903 0
[pid=16441] vsize: 148192
Current children cumulated CPU time (s) 878.43
Current children cumulated vsize (Kb) 150316

[startup+890.075 s]
Raw data (loadavg): 1.00 0.98 0.91 2/57 16441
Raw data (/proc/16437/stat): 16437 (minisat+_script) S 16436 16437 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855620567 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16437/statm): 531 226 485 147 0 384 0
[pid=16437] vsize: 2124
Raw data (/proc/16441/stat): 16441 (minisat+_64-bit) R 16437 16437 21452 0 -1 0 34683 0 0 0 88682 160 0 0 25 0 1 0 1855620572 152084480 32245 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16441/statm): 37130 32245 145 145 0 36985 0
[pid=16441] vsize: 148520
Current children cumulated CPU time (s) 888.43
Current children cumulated vsize (Kb) 150644

[startup+900.076 s]
Raw data (loadavg): 1.00 0.98 0.91 2/57 16441
Raw data (/proc/16437/stat): 16437 (minisat+_script) S 16436 16437 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855620567 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16437/statm): 531 226 485 147 0 384 0
[pid=16437] vsize: 2124
Raw data (/proc/16441/stat): 16441 (minisat+_64-bit) R 16437 16437 21452 0 -1 0 34781 0 0 0 89681 161 0 0 25 0 1 0 1855620572 152485888 32343 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16441/statm): 37228 32343 145 145 0 37083 0
[pid=16441] vsize: 148912
Current children cumulated CPU time (s) 898.43
Current children cumulated vsize (Kb) 151036

[startup+910.077 s]
Raw data (loadavg): 1.00 0.98 0.91 2/57 16441
Raw data (/proc/16437/stat): 16437 (minisat+_script) S 16436 16437 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855620567 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16437/statm): 531 226 485 147 0 384 0
[pid=16437] vsize: 2124
Raw data (/proc/16441/stat): 16441 (minisat+_64-bit) R 16437 16437 21452 0 -1 0 34883 0 0 0 90679 161 0 0 25 0 1 0 1855620572 152899584 32445 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16441/statm): 37329 32445 145 145 0 37184 0
[pid=16441] vsize: 149316
Current children cumulated CPU time (s) 908.41
Current children cumulated vsize (Kb) 151440

[startup+920.077 s]
Raw data (loadavg): 1.00 0.98 0.91 2/57 16441
Raw data (/proc/16437/stat): 16437 (minisat+_script) S 16436 16437 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855620567 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16437/statm): 531 226 485 147 0 384 0
[pid=16437] vsize: 2124
Raw data (/proc/16441/stat): 16441 (minisat+_64-bit) R 16437 16437 21452 0 -1 0 34979 0 0 0 91677 162 0 0 25 0 1 0 1855620572 153292800 32541 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16441/statm): 37425 32541 145 145 0 37280 0
[pid=16441] vsize: 149700
Current children cumulated CPU time (s) 918.4
Current children cumulated vsize (Kb) 151824

[startup+930.078 s]
Raw data (loadavg): 1.00 0.98 0.91 2/57 16441
Raw data (/proc/16437/stat): 16437 (minisat+_script) S 16436 16437 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855620567 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16437/statm): 531 226 485 147 0 384 0
[pid=16437] vsize: 2124
Raw data (/proc/16441/stat): 16441 (minisat+_64-bit) R 16437 16437 21452 0 -1 0 35053 0 0 0 92676 163 0 0 25 0 1 0 1855620572 153591808 32615 4294967295 134512640 135094434 3221224448 3221223104 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16441/statm): 37498 32615 145 145 0 37353 0
[pid=16441] vsize: 149992
Current children cumulated CPU time (s) 928.4
Current children cumulated vsize (Kb) 152116

[startup+940.079 s]
Raw data (loadavg): 1.00 0.98 0.91 2/57 16441
Raw data (/proc/16437/stat): 16437 (minisat+_script) S 16436 16437 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855620567 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16437/statm): 531 226 485 147 0 384 0
[pid=16437] vsize: 2124
Raw data (/proc/16441/stat): 16441 (minisat+_64-bit) R 16437 16437 21452 0 -1 0 35096 0 0 0 93676 163 0 0 25 0 1 0 1855620572 153767936 32658 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16441/statm): 37541 32658 145 145 0 37396 0
[pid=16441] vsize: 150164
Current children cumulated CPU time (s) 938.4
Current children cumulated vsize (Kb) 152288

[startup+950.08 s]
Raw data (loadavg): 1.00 0.98 0.91 2/57 16441
Raw data (/proc/16437/stat): 16437 (minisat+_script) S 16436 16437 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855620567 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16437/statm): 531 226 485 147 0 384 0
[pid=16437] vsize: 2124
Raw data (/proc/16441/stat): 16441 (minisat+_64-bit) R 16437 16437 21452 0 -1 0 35132 0 0 0 94675 163 0 0 25 0 1 0 1855620572 153911296 32694 4294967295 134512640 135094434 3221224448 3221223040 134557230 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16441/statm): 37576 32694 145 145 0 37431 0
[pid=16441] vsize: 150304
Current children cumulated CPU time (s) 948.39
Current children cumulated vsize (Kb) 152428

[startup+960.08 s]
Raw data (loadavg): 1.00 0.98 0.91 2/57 16441
Raw data (/proc/16437/stat): 16437 (minisat+_script) S 16436 16437 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855620567 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16437/statm): 531 226 485 147 0 384 0
[pid=16437] vsize: 2124
Raw data (/proc/16441/stat): 16441 (minisat+_64-bit) R 16437 16437 21452 0 -1 0 35182 0 0 0 95675 164 0 0 25 0 1 0 1855620572 154107904 32744 4294967295 134512640 135094434 3221224448 3221223072 134557650 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16441/statm): 37624 32744 145 145 0 37479 0
[pid=16441] vsize: 150496
Current children cumulated CPU time (s) 958.4
Current children cumulated vsize (Kb) 152620

[startup+970.081 s]
Raw data (loadavg): 1.00 0.98 0.91 2/57 16441
Raw data (/proc/16437/stat): 16437 (minisat+_script) S 16436 16437 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855620567 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16437/statm): 531 226 485 147 0 384 0
[pid=16437] vsize: 2124
Raw data (/proc/16441/stat): 16441 (minisat+_64-bit) R 16437 16437 21452 0 -1 0 35222 0 0 0 96674 165 0 0 25 0 1 0 1855620572 154267648 32784 4294967295 134512640 135094434 3221224448 3221223108 134553497 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16441/statm): 37663 32784 145 145 0 37518 0
[pid=16441] vsize: 150652
Current children cumulated CPU time (s) 968.4
Current children cumulated vsize (Kb) 152776

[startup+980.082 s]
Raw data (loadavg): 1.00 0.98 0.91 2/57 16441
Raw data (/proc/16437/stat): 16437 (minisat+_script) S 16436 16437 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855620567 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16437/statm): 531 226 485 147 0 384 0
[pid=16437] vsize: 2124
Raw data (/proc/16441/stat): 16441 (minisat+_64-bit) R 16437 16437 21452 0 -1 0 35341 0 0 0 97671 166 0 0 25 0 1 0 1855620572 154746880 32903 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16441/statm): 37780 32903 145 145 0 37635 0
[pid=16441] vsize: 151120
Current children cumulated CPU time (s) 978.38
Current children cumulated vsize (Kb) 153244

[startup+990.082 s]
Raw data (loadavg): 1.00 0.98 0.91 2/57 16441
Raw data (/proc/16437/stat): 16437 (minisat+_script) S 16436 16437 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855620567 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16437/statm): 531 226 485 147 0 384 0
[pid=16437] vsize: 2124
Raw data (/proc/16441/stat): 16441 (minisat+_64-bit) R 16437 16437 21452 0 -1 0 35575 0 0 0 98666 168 0 0 25 0 1 0 1855620572 155693056 33137 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16441/statm): 38011 33137 145 145 0 37866 0
[pid=16441] vsize: 152044
Current children cumulated CPU time (s) 988.35
Current children cumulated vsize (Kb) 154168

[startup+1000.08 s]
Raw data (loadavg): 1.00 0.98 0.91 2/57 16441
Raw data (/proc/16437/stat): 16437 (minisat+_script) S 16436 16437 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855620567 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16437/statm): 531 226 485 147 0 384 0
[pid=16437] vsize: 2124
Raw data (/proc/16441/stat): 16441 (minisat+_64-bit) R 16437 16437 21452 0 -1 0 35794 0 0 0 99662 170 0 0 25 0 1 0 1855620572 156577792 33356 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16441/statm): 38227 33356 145 145 0 38082 0
[pid=16441] vsize: 152908
Current children cumulated CPU time (s) 998.33
Current children cumulated vsize (Kb) 155032

[startup+1010.08 s]
Raw data (loadavg): 1.00 0.98 0.91 2/57 16441
Raw data (/proc/16437/stat): 16437 (minisat+_script) S 16436 16437 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855620567 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16437/statm): 531 226 485 147 0 384 0
[pid=16437] vsize: 2124
Raw data (/proc/16441/stat): 16441 (minisat+_64-bit) R 16437 16437 21452 0 -1 0 35960 0 0 0 100659 172 0 0 25 0 1 0 1855620572 157249536 33522 4294967295 134512640 135094434 3221224448 3221223108 134553480 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16441/statm): 38391 33522 145 145 0 38246 0
[pid=16441] vsize: 153564
Current children cumulated CPU time (s) 1008.32
Current children cumulated vsize (Kb) 155688

[startup+1020.09 s]
Raw data (loadavg): 1.00 0.98 0.91 2/57 16441
Raw data (/proc/16437/stat): 16437 (minisat+_script) S 16436 16437 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855620567 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16437/statm): 531 226 485 147 0 384 0
[pid=16437] vsize: 2124
Raw data (/proc/16441/stat): 16441 (minisat+_64-bit) R 16437 16437 21452 0 -1 0 35986 0 0 0 101659 172 0 0 25 0 1 0 1855620572 157392896 33548 4294967295 134512640 135094434 3221224448 3221223072 134557596 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16441/statm): 38426 33548 145 145 0 38281 0
[pid=16441] vsize: 153704
Current children cumulated CPU time (s) 1018.32
Current children cumulated vsize (Kb) 155828

[startup+1030.09 s]
Raw data (loadavg): 1.00 0.98 0.91 2/57 16441
Raw data (/proc/16437/stat): 16437 (minisat+_script) S 16436 16437 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855620567 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16437/statm): 531 226 485 147 0 384 0
[pid=16437] vsize: 2124
Raw data (/proc/16441/stat): 16441 (minisat+_64-bit) R 16437 16437 21452 0 -1 0 36086 0 0 0 102656 173 0 0 25 0 1 0 1855620572 157798400 33648 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16441/statm): 38525 33648 145 145 0 38380 0
[pid=16441] vsize: 154100
Current children cumulated CPU time (s) 1028.3
Current children cumulated vsize (Kb) 156224

[startup+1040.09 s]
Raw data (loadavg): 1.00 0.98 0.91 2/57 16441
Raw data (/proc/16437/stat): 16437 (minisat+_script) S 16436 16437 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855620567 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16437/statm): 531 226 485 147 0 384 0
[pid=16437] vsize: 2124
Raw data (/proc/16441/stat): 16441 (minisat+_64-bit) R 16437 16437 21452 0 -1 0 36205 0 0 0 103655 174 0 0 25 0 1 0 1855620572 158281728 33767 4294967295 134512640 135094434 3221224448 3221223104 134558254 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16441/statm): 38643 33767 145 145 0 38498 0
[pid=16441] vsize: 154572
Current children cumulated CPU time (s) 1038.3
Current children cumulated vsize (Kb) 156696

[startup+1050.09 s]
Raw data (loadavg): 1.00 0.98 0.91 2/57 16441
Raw data (/proc/16437/stat): 16437 (minisat+_script) S 16436 16437 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855620567 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16437/statm): 531 226 485 147 0 384 0
[pid=16437] vsize: 2124
Raw data (/proc/16441/stat): 16441 (minisat+_64-bit) R 16437 16437 21452 0 -1 0 36303 0 0 0 104653 175 0 0 25 0 1 0 1855620572 158683136 33865 4294967295 134512640 135094434 3221224448 3221223108 134553536 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16441/statm): 38741 33865 145 145 0 38596 0
[pid=16441] vsize: 154964
Current children cumulated CPU time (s) 1048.29
Current children cumulated vsize (Kb) 157088

[startup+1060.09 s]
Raw data (loadavg): 1.00 0.98 0.91 2/57 16441
Raw data (/proc/16437/stat): 16437 (minisat+_script) S 16436 16437 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855620567 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16437/statm): 531 226 485 147 0 384 0
[pid=16437] vsize: 2124
Raw data (/proc/16441/stat): 16441 (minisat+_64-bit) R 16437 16437 21452 0 -1 0 36304 0 0 0 105653 176 0 0 25 0 1 0 1855620572 158683136 33866 4294967295 134512640 135094434 3221224448 3221223104 134557948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16441/statm): 38741 33866 145 145 0 38596 0
[pid=16441] vsize: 154964
Current children cumulated CPU time (s) 1058.3
Current children cumulated vsize (Kb) 157088

[startup+1070.09 s]
Raw data (loadavg): 1.00 0.98 0.91 2/57 16441
Raw data (/proc/16437/stat): 16437 (minisat+_script) S 16436 16437 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855620567 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16437/statm): 531 226 485 147 0 384 0
[pid=16437] vsize: 2124
Raw data (/proc/16441/stat): 16441 (minisat+_64-bit) R 16437 16437 21452 0 -1 0 36327 0 0 0 106652 176 0 0 25 0 1 0 1855620572 158777344 33889 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16441/statm): 38764 33889 145 145 0 38619 0
[pid=16441] vsize: 155056
Current children cumulated CPU time (s) 1068.29
Current children cumulated vsize (Kb) 157180

[startup+1080.09 s]
Raw data (loadavg): 1.00 0.98 0.91 2/57 16441
Raw data (/proc/16437/stat): 16437 (minisat+_script) S 16436 16437 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855620567 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16437/statm): 531 226 485 147 0 384 0
[pid=16437] vsize: 2124
Raw data (/proc/16441/stat): 16441 (minisat+_64-bit) R 16437 16437 21452 0 -1 0 36358 0 0 0 107652 176 0 0 25 0 1 0 1855620572 158900224 33920 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16441/statm): 38794 33920 145 145 0 38649 0
[pid=16441] vsize: 155176
Current children cumulated CPU time (s) 1078.29
Current children cumulated vsize (Kb) 157300

[startup+1090.09 s]
Raw data (loadavg): 1.00 0.98 0.91 2/57 16441
Raw data (/proc/16437/stat): 16437 (minisat+_script) S 16436 16437 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855620567 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16437/statm): 531 226 485 147 0 384 0
[pid=16437] vsize: 2124
Raw data (/proc/16441/stat): 16441 (minisat+_64-bit) R 16437 16437 21452 0 -1 0 36384 0 0 0 108652 177 0 0 25 0 1 0 1855620572 159002624 33946 4294967295 134512640 135094434 3221224448 3221223072 134557734 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16441/statm): 38819 33946 145 145 0 38674 0
[pid=16441] vsize: 155276
Current children cumulated CPU time (s) 1088.3
Current children cumulated vsize (Kb) 157400

[startup+1100.09 s]
Raw data (loadavg): 1.00 0.98 0.91 2/57 16441
Raw data (/proc/16437/stat): 16437 (minisat+_script) S 16436 16437 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855620567 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16437/statm): 531 226 485 147 0 384 0
[pid=16437] vsize: 2124
Raw data (/proc/16441/stat): 16441 (minisat+_64-bit) R 16437 16437 21452 0 -1 0 36433 0 0 0 109651 177 0 0 25 0 1 0 1855620572 159199232 33995 4294967295 134512640 135094434 3221224448 3221223104 134557823 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16441/statm): 38867 33995 145 145 0 38722 0
[pid=16441] vsize: 155468
Current children cumulated CPU time (s) 1098.29
Current children cumulated vsize (Kb) 157592

[startup+1110.09 s]
Raw data (loadavg): 1.00 0.98 0.91 2/57 16441
Raw data (/proc/16437/stat): 16437 (minisat+_script) S 16436 16437 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855620567 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16437/statm): 531 226 485 147 0 384 0
[pid=16437] vsize: 2124
Raw data (/proc/16441/stat): 16441 (minisat+_64-bit) R 16437 16437 21452 0 -1 0 37025 0 0 0 110648 179 0 0 25 0 1 0 1855620572 159358976 34035 4294967295 134512640 135094434 3221224448 3221221824 134600915 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16441/statm): 38906 34035 145 145 0 38761 0
[pid=16441] vsize: 155624
Current children cumulated CPU time (s) 1108.28
Current children cumulated vsize (Kb) 157748

[startup+1120.1 s]
Raw data (loadavg): 1.00 0.98 0.91 2/57 16441
Raw data (/proc/16437/stat): 16437 (minisat+_script) S 16436 16437 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855620567 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16437/statm): 531 226 485 147 0 384 0
[pid=16437] vsize: 2124
Raw data (/proc/16441/stat): 16441 (minisat+_64-bit) R 16437 16437 21452 0 -1 0 37078 0 0 0 111647 179 0 0 25 0 1 0 1855620572 159436800 34054 4294967295 134512640 135094434 3221224448 3221223108 134553482 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16441/statm): 38925 34054 145 145 0 38780 0
[pid=16441] vsize: 155700
Current children cumulated CPU time (s) 1118.27
Current children cumulated vsize (Kb) 157824

[startup+1130.1 s]
Raw data (loadavg): 1.00 0.98 0.91 2/57 16441
Raw data (/proc/16437/stat): 16437 (minisat+_script) S 16436 16437 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855620567 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16437/statm): 531 226 485 147 0 384 0
[pid=16437] vsize: 2124
Raw data (/proc/16441/stat): 16441 (minisat+_64-bit) R 16437 16437 21452 0 -1 0 37082 0 0 0 112647 180 0 0 25 0 1 0 1855620572 159453184 34058 4294967295 134512640 135094434 3221224448 3221223108 134553515 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16441/statm): 38929 34058 145 145 0 38784 0
[pid=16441] vsize: 155716
Current children cumulated CPU time (s) 1128.28
Current children cumulated vsize (Kb) 157840

[startup+1140.1 s]
Raw data (loadavg): 1.00 0.98 0.91 2/57 16441
Raw data (/proc/16437/stat): 16437 (minisat+_script) S 16436 16437 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855620567 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16437/statm): 531 226 485 147 0 384 0
[pid=16437] vsize: 2124
Raw data (/proc/16441/stat): 16441 (minisat+_64-bit) R 16437 16437 21452 0 -1 0 37101 0 0 0 113646 180 0 0 25 0 1 0 1855620572 159531008 34077 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16441/statm): 38948 34077 145 145 0 38803 0
[pid=16441] vsize: 155792
Current children cumulated CPU time (s) 1138.27
Current children cumulated vsize (Kb) 157916

[startup+1150.1 s]
Raw data (loadavg): 1.00 0.98 0.91 2/57 16441
Raw data (/proc/16437/stat): 16437 (minisat+_script) S 16436 16437 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855620567 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16437/statm): 531 226 485 147 0 384 0
[pid=16437] vsize: 2124
Raw data (/proc/16441/stat): 16441 (minisat+_64-bit) R 16437 16437 21452 0 -1 0 37130 0 0 0 114646 180 0 0 25 0 1 0 1855620572 159645696 34106 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16441/statm): 38976 34106 145 145 0 38831 0
[pid=16441] vsize: 155904
Current children cumulated CPU time (s) 1148.27
Current children cumulated vsize (Kb) 158028

[startup+1160.1 s]
Raw data (loadavg): 1.00 0.98 0.91 2/57 16441
Raw data (/proc/16437/stat): 16437 (minisat+_script) S 16436 16437 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855620567 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16437/statm): 531 226 485 147 0 384 0
[pid=16437] vsize: 2124
Raw data (/proc/16441/stat): 16441 (minisat+_64-bit) R 16437 16437 21452 0 -1 0 37163 0 0 0 115646 180 0 0 25 0 1 0 1855620572 160305152 34139 4294967295 134512640 135094434 3221224448 3221223104 134557846 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16441/statm): 39137 34139 145 145 0 38992 0
[pid=16441] vsize: 156548
Current children cumulated CPU time (s) 1158.27
Current children cumulated vsize (Kb) 158672

[startup+1170.1 s]
Raw data (loadavg): 1.00 0.98 0.91 2/57 16441
Raw data (/proc/16437/stat): 16437 (minisat+_script) S 16436 16437 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855620567 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16437/statm): 531 226 485 147 0 384 0
[pid=16437] vsize: 2124
Raw data (/proc/16441/stat): 16441 (minisat+_64-bit) R 16437 16437 21452 0 -1 0 37781 0 0 0 116643 182 0 0 25 0 1 0 1855620572 160534528 34196 4294967295 134512640 135094434 3221224448 3221221824 134676539 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16441/statm): 39193 34196 145 145 0 39048 0
[pid=16441] vsize: 156772
Current children cumulated CPU time (s) 1168.26
Current children cumulated vsize (Kb) 158896

[startup+1180.1 s]
Raw data (loadavg): 1.00 0.98 0.91 2/57 16441
Raw data (/proc/16437/stat): 16437 (minisat+_script) S 16436 16437 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855620567 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16437/statm): 531 226 485 147 0 384 0
[pid=16437] vsize: 2124
Raw data (/proc/16441/stat): 16441 (minisat+_64-bit) R 16437 16437 21452 0 -1 0 37814 0 0 0 117642 182 0 0 25 0 1 0 1855620572 160555008 34196 4294967295 134512640 135094434 3221224448 3221223108 134553446 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16441/statm): 39198 34196 145 145 0 39053 0
[pid=16441] vsize: 156792
Current children cumulated CPU time (s) 1178.25
Current children cumulated vsize (Kb) 158916

[startup+1190.1 s]
Raw data (loadavg): 1.00 0.98 0.91 2/57 16441
Raw data (/proc/16437/stat): 16437 (minisat+_script) S 16436 16437 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855620567 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16437/statm): 531 226 485 147 0 384 0
[pid=16437] vsize: 2124
Raw data (/proc/16441/stat): 16441 (minisat+_64-bit) R 16437 16437 21452 0 -1 0 37821 0 0 0 118643 183 0 0 25 0 1 0 1855620572 160555008 34203 4294967295 134512640 135094434 3221224448 3221223104 134558289 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16441/statm): 39198 34203 145 145 0 39053 0
[pid=16441] vsize: 156792
Current children cumulated CPU time (s) 1188.27
Current children cumulated vsize (Kb) 158916

[startup+1200.1 s]
Raw data (loadavg): 1.00 0.98 0.91 2/57 16441
Raw data (/proc/16437/stat): 16437 (minisat+_script) S 16436 16437 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855620567 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16437/statm): 531 226 485 147 0 384 0
[pid=16437] vsize: 2124
Raw data (/proc/16441/stat): 16441 (minisat+_64-bit) R 16437 16437 21452 0 -1 0 37903 0 0 0 119641 183 0 0 25 0 1 0 1855620572 160878592 34285 4294967295 134512640 135094434 3221224448 3221223100 134558255 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16441/statm): 39277 34285 145 145 0 39132 0
[pid=16441] vsize: 157108
Current children cumulated CPU time (s) 1198.25
Current children cumulated vsize (Kb) 159232

[startup+1210.1 s]
Raw data (loadavg): 1.00 0.98 0.91 2/57 16441
Raw data (/proc/16437/stat): 16437 (minisat+_script) S 16436 16437 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855620567 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16437/statm): 531 226 485 147 0 384 0
[pid=16437] vsize: 2124
Raw data (/proc/16441/stat): 16441 (minisat+_64-bit) R 16437 16437 21452 0 -1 0 37990 0 0 0 120640 184 0 0 25 0 1 0 1855620572 161234944 34372 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16441/statm): 39364 34372 145 145 0 39219 0
[pid=16441] vsize: 157456
Current children cumulated CPU time (s) 1208.25
Current children cumulated vsize (Kb) 159580



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.1 s]
Raw data (loadavg): 1.00 0.98 0.91 2/57 16441
Raw data (/proc/16437/stat): 16437 (minisat+_script) S 16436 16437 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855620567 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16437/statm): 531 226 485 147 0 384 0
[pid=16437] vsize: 2124
Raw data (/proc/16441/stat): 16441 (minisat+_64-bit) R 16437 16437 21452 0 -1 0 37990 0 0 0 120640 184 0 0 25 0 1 0 1855620572 161234944 34372 4294967295 134512640 135094434 3221224448 3221223100 134558255 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16441/statm): 39364 34372 145 145 0 39219 0
[pid=16441] vsize: 157456
Current children cumulated CPU time (s) 1208.25
Current children cumulated vsize (Kb) 159580

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

Child status: 10
Real time (s): 1210.18
CPU time (s): 1208.32
CPU user time (s): 1206.4
CPU system time (s): 1.91571
CPU usage (%): 99.8465
Max. virtual memory (cumulated for all children) (Kb): 159580

Verifier Data

ERROR: no interpretation found !