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/plato.asu.edu/pub/fctp/normalized-mps-v2-13-7-bal8x12.opb
MD5SUM69e7430fb77e7d40f128bdde5f7776a3
Bench Categoryoptimization, medium integers (OPTMEDINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function 11587075
Optimality of the best value was proved NO
Number of terms in the objective function 2016
Biggest coefficient in the objective function 402653184
Number of bits for the biggest coefficient in the objective function 29
Sum of the numbers in the objective function 34444990400
Number of bits of the sum of numbers in the objective function 36
Biggest number in a constraint 402653184
Number of bits of the biggest number in a constraint 29
Biggest sum of numbers in a constraint 34444990400
Number of bits of the biggest sum of numbers36
Best result obtained on this benchmarkSAT
Best CPU time to get the best result obtained on this benchmark1195.56
Number of variables2016
Total number of constraints116
Number of constraints which are clauses0
Number of constraints which are cardinality constraints (but not clauses)0
Number of constraints which are nor clauses,nor cardinality constraints116
Minimum length of a constraint21
Maximum length of a constraint240

Trace number 6274

Launcher Data

LAUNCH ON wulflinc22 THE 2005-09-20 05:04:42 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3433 boxname=wulflinc22 idbench=1089 idsolver=3 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  69e7430fb77e7d40f128bdde5f7776a3  /oldhome/oroussel/tmp/wulflinc22/normalized-mps-v2-13-7-bal8x12.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc22/normalized-mps-v2-13-7-bal8x12.opb
IDLAUNCH: 3433
/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:        887544 kB
Buffers:         14036 kB
Cached:         106248 kB
SwapCached:        552 kB
Active:          16792 kB
Inactive:       106132 kB
HighTotal:      131008 kB
HighFree:        23856 kB
LowTotal:       903652 kB
LowFree:        863688 kB
SwapTotal:     2097892 kB
SwapFree:      2096768 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5788 kB
Slab:            18420 kB
Committed_AS:    64264 kB
PageTables:        332 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-09-20 05:24:52 (client local time) WITH STATUS 10 IN 1207.27 SECONDS
stats: 3433 7 1207.27 10

Solver Data

c Parsing PB file...
c Converting 136 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ####################
c   -- Clauses(.)/Splits(s): (none)
c ---[ 134]---> Adder-cost: 240   maxlim: 20596   bits: 15/15
c ---[ 132]---> Adder-cost: 254   maxlim: 32244   bits: 16/15
c ---[ 130]---> Adder-cost: 254   maxlim: 33140   bits: 16/16
c ---[ 128]---> Adder-cost: 254   maxlim: 34420   bits: 16/16
c ---[ 126]---> Adder-cost: 254   maxlim: 31604   bits: 16/15
c ---[ 124]---> Adder-cost: 254   maxlim: 34420   bits: 16/16
c ---[ 122]---> Adder-cost: 240   maxlim: 21236   bits: 15/15
c ---[ 120]---> Adder-cost: 254   maxlim: 31604   bits: 16/15
c ---[ 118]---> Sorter-cost: 1497     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 116]---> Sorter-cost: 1321     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 114]---> Sorter-cost: 1321     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 112]---> Sorter-cost: 1187     Base: 2 2 2 2 2 2 2 2 2
c ---[ 110]---> Sorter-cost: 1497     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 108]---> Sorter-cost: 1321     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 106]---> Sorter-cost: 1187     Base: 2 2 2 2 2 2 2 2 2
c ---[ 104]---> Sorter-cost: 1497     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 102]---> Sorter-cost: 1497     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 100]---> Sorter-cost: 1321     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  98]---> Sorter-cost: 1525     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[  96]---> Sorter-cost: 1497     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  95]---> BDD-cost:   15
c ---[  94]---> BDD-cost:   15
c ---[  93]---> BDD-cost:   14
c ---[  92]---> BDD-cost:   13
c ---[  91]---> BDD-cost:   15
c ---[  90]---> BDD-cost:   15
c ---[  89]---> BDD-cost:   15
c ---[  88]---> BDD-cost:   15
c ---[  87]---> BDD-cost:   13
c ---[  86]---> BDD-cost:   15
c ---[  85]---> BDD-cost:   15
c ---[  84]---> BDD-cost:   14
c ---[  83]---> BDD-cost:   15
c ---[  82]---> BDD-cost:   15
c ---[  81]---> BDD-cost:   15
c ---[  80]---> BDD-cost:   14
c ---[  79]---> BDD-cost:   13
c ---[  78]---> BDD-cost:   15
c ---[  77]---> BDD-cost:   15
c ---[  76]---> BDD-cost:   15
c ---[  75]---> BDD-cost:   15
c ---[  74]---> BDD-cost:   13
c ---[  73]---> BDD-cost:   15
c ---[  72]---> BDD-cost:   15
c ---[  71]---> BDD-cost:   16
c ---[  70]---> BDD-cost:   14
c ---[  69]---> BDD-cost:   19
c ---[  68]---> BDD-cost:   17
c ---[  67]---> BDD-cost:   14
c ---[  66]---> BDD-cost:   13
c ---[  65]---> BDD-cost:   15
c ---[  64]---> BDD-cost:   15
c ---[  63]---> BDD-cost:   15
c ---[  62]---> BDD-cost:   15
c ---[  61]---> BDD-cost:   13
c ---[  60]---> BDD-cost:   13
c ---[  59]---> BDD-cost:   15
c ---[  58]---> BDD-cost:   16
c ---[  57]---> BDD-cost:   14
c ---[  56]---> BDD-cost:   19
c ---[  55]---> BDD-cost:   17
c ---[  54]---> BDD-cost:   14
c ---[  53]---> BDD-cost:   13
c ---[  52]---> BDD-cost:   15
c ---[  51]---> BDD-cost:   15
c ---[  50]---> BDD-cost:   15
c ---[  49]---> BDD-cost:   15
c ---[  48]---> BDD-cost:   15
c ---[  47]---> BDD-cost:   13
c ---[  46]---> BDD-cost:   15
c ---[  45]---> BDD-cost:   17
c ---[  44]---> BDD-cost:   14
c ---[  43]---> BDD-cost:   17
c ---[  42]---> BDD-cost:   17
c ---[  41]---> BDD-cost:   14
c ---[  40]---> BDD-cost:   13
c ---[  39]---> BDD-cost:   15
c ---[  38]---> BDD-cost:   15
c ---[  37]---> BDD-cost:   15
c ---[  36]---> BDD-cost:   15
c ---[  35]---> BDD-cost:   15
c ---[  34]---> BDD-cost:   13
c ---[  33]---> BDD-cost:   15
c ---[  32]---> BDD-cost:   16
c ---[  31]---> BDD-cost:   14
c ---[  30]---> BDD-cost:   19
c ---[  29]---> BDD-cost:   17
c ---[  28]---> BDD-cost:   14
c ---[  27]---> BDD-cost:   14
c ---[  26]---> BDD-cost:   13
c ---[  25]---> BDD-cost:   14
c ---[  24]---> BDD-cost:   14
c ---[  23]---> BDD-cost:   14
c ---[  22]---> BDD-cost:   14
c ---[  21]---> BDD-cost:   13
c ---[  20]---> BDD-cost:   14
c ---[  19]---> BDD-cost:   14
c ---[  18]---> BDD-cost:   14
c ---[  17]---> BDD-cost:   15
c ---[  16]---> BDD-cost:   14
c ---[  15]---> BDD-cost:   14
c ---[  14]---> BDD-cost:   14
c ---[  13]---> BDD-cost:   13
c ---[  12]---> BDD-cost:   15
c ---[  11]---> BDD-cost:   15
c ---[  10]---> BDD-cost:   15
c ---[   9]---> BDD-cost:   15
c ---[   8]---> BDD-cost:   13
c ---[   7]---> BDD-cost:   15
c ---[   6]---> BDD-cost:   15
c ---[   5]---> BDD-cost:   17
c ---[   4]---> BDD-cost:   14
c ---[   3]---> BDD-cost:   17
c ---[   2]---> BDD-cost:   17
c ---[   1]---> BDD-cost:   14
c ---[   0]---> BDD-cost:   13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   55709   147365 |   18569       0        0     nan |  0.000 % |
c |       100 |   55555   147016 |   20425      82      384     4.7 | 11.217 % |
c |       250 |   55555   147016 |   22468     232      943     4.1 | 11.217 % |
c |       475 |   55533   146967 |   24715     451     1719     3.8 | 11.254 % |
c |       812 |   55465   146813 |   27186     782     3119     4.0 | 11.355 % |
c |      1318 |   55407   146681 |   29905    1286     5149     4.0 | 11.441 % |
c |      2077 |   55407   146681 |   32896    2045     8718     4.3 | 11.441 % |
c |      3216 |   55099   145961 |   36185    3164    13652     4.3 | 11.930 % |
c |      4924 |   54901   145474 |   39804    4850    22225     4.6 | 12.229 % |
c |      7487 |   54380   144082 |   43784    7362    37124     5.0 | 12.990 % |
c ==============================================================================
c Found solution: 27016468
c ---[   0]---> Adder-cost: 9016   maxlim: 83422892   bits: 27/27
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     10119 |  117250   368847 |   39083    9987    53254     5.3 | 12.990 % |
c |     10219 |  117250   368847 |   42991   10087    53825     5.3 |  8.959 % |
c |     10369 |  117250   368847 |   47290   10237    54916     5.4 |  8.959 % |
c |     10594 |  117250   368847 |   52019   10462    56263     5.4 |  8.959 % |
c |     10931 |  117250   368847 |   57221   10799    57838     5.4 |  8.959 % |
c |     11438 |  117168   368600 |   62943   11294    79467     7.0 |  9.027 % |
c |     12197 |  117129   368473 |   69237   12047    84799     7.0 |  9.052 % |
c |     13336 |  116895   367799 |   76161   13152    93195     7.1 |  9.257 % |
c ==============================================================================
c Found solution: 26351641
c ---[   0]---> Adder-cost: 0   maxlim: 84087719   bits: 27/27
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     14450 |  116886   367911 |   38962   14260   103032     7.2 |  9.257 % |
c |     14550 |  116869   367871 |   42858   14358   103457     7.2 |  9.340 % |
c |     14701 |  116869   367871 |   47144   14509   104089     7.2 |  9.340 % |
c |     14926 |  116817   367752 |   51858   14727   105151     7.1 |  9.401 % |
c |     15263 |  116807   367729 |   57044   15063   107523     7.1 |  9.415 % |
c |     15769 |  116702   367483 |   62748   15558   111579     7.2 |  9.538 % |
c |     16528 |  116534   367080 |   69023   16290   118881     7.3 |  9.724 % |
c ==============================================================================
c Found solution: 26297506
c ---[   0]---> Adder-cost: 0   maxlim: 84141854   bits: 27/27
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     17097 |  116550   367312 |   38850   16859   128515     7.6 |  9.724 % |
c |     17197 |  116512   367223 |   42735   16957   128906     7.6 |  9.796 % |
c |     17347 |  116496   367171 |   47008   17103   129778     7.6 |  9.806 % |
c |     17572 |  116489   367148 |   51709   17326   132151     7.6 |  9.810 % |
c |     17909 |  116489   367148 |   56880   17663   135033     7.6 |  9.810 % |
c |     18416 |  116489   367148 |   62568   18170   187303    10.3 |  9.810 % |
c |     19175 |  116408   366951 |   68825   18913   195169    10.3 |  9.907 % |
c ==============================================================================
c Found solution: 25048271
c ---[   0]---> Adder-cost: 0   maxlim: 85391089   bits: 27/27
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     19998 |  116425   367188 |   38808   19735   243565    12.3 |  9.907 % |
c |     20098 |  116425   367188 |   42688   19835   244289    12.3 |  9.958 % |
c |     20248 |  116425   367188 |   46957   19985   245594    12.3 |  9.958 % |
c |     20473 |  116425   367188 |   51653   20210   249672    12.4 |  9.958 % |
c |     20812 |  116425   367188 |   56818   20549   323157    15.7 |  9.958 % |
c |     21318 |  116403   367138 |   62500   21053   330284    15.7 |  9.983 % |
c |     22077 |  116394   367109 |   68750   21811   353612    16.2 |  9.990 % |
c |     23216 |  116394   367109 |   75625   22950   375987    16.4 |  9.990 % |
c |     24924 |  116355   367021 |   83188   24657   755026    30.6 | 10.026 % |
c ==============================================================================
c Found solution: 24959335
c ---[   0]---> Adder-cost: 0   maxlim: 85480025   bits: 27/27
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     26510 |  116365   367173 |   38788   26243  1023172    39.0 | 10.026 % |
c |     26610 |  116365   367173 |   42666   26343  1024071    38.9 | 10.051 % |
c |     26760 |  116365   367173 |   46933   26493  1026268    38.7 | 10.051 % |
c |     26985 |  116365   367173 |   51626   26718  1028175    38.5 | 10.051 % |
c |     27322 |  116365   367173 |   56789   27055  1046266    38.7 | 10.051 % |
c |     27828 |  116365   367173 |   62468   27561  1066774    38.7 | 10.051 % |
c |     28587 |  116330   367094 |   68715   28317  1108925    39.2 | 10.091 % |
c |     29727 |  116297   367017 |   75586   29454  1129772    38.4 | 10.127 % |
c ==============================================================================
c Found solution: 24820883
c ---[   0]---> Adder-cost: 0   maxlim: 85618477   bits: 27/27
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     30922 |  116316   367237 |   38772   30649  1193284    38.9 | 10.127 % |
c |     31024 |  116316   367237 |   42649   30751  1198413    39.0 | 10.159 % |
c |     31175 |  116316   367237 |   46914   30902  1199533    38.8 | 10.159 % |
c |     31401 |  116316   367237 |   51605   31128  1201429    38.6 | 10.159 % |
c |     31738 |  116316   367237 |   56766   31465  1211676    38.5 | 10.159 % |
c |     32246 |  116316   367237 |   62442   31973  1227881    38.4 | 10.159 % |
c |     33005 |  116301   367203 |   68686   32730  1241343    37.9 | 10.174 % |
c |     34144 |  116291   367180 |   75555   33867  1386768    40.9 | 10.184 % |
c ==============================================================================
c Found solution: 21919935
c ---[   0]---> Adder-cost: 0   maxlim: 88519425   bits: 27/27
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     35199 |  116305   367318 |   38768   34922  1421117    40.7 | 10.184 % |
c |     35300 |  116305   367318 |   42644   35023  1422571    40.6 | 10.211 % |
c |     35450 |  116305   367318 |   46909   35173  1425440    40.5 | 10.211 % |
c |     35675 |  116305   367318 |   51600   35398  1452544    41.0 | 10.211 % |
c |     36012 |  116265   367227 |   56760   35727  1456865    40.8 | 10.254 % |
c |     36518 |  116265   367227 |   62436   36233  1476401    40.7 | 10.254 % |
c |     37279 |  116265   367227 |   68679   36994  1499792    40.5 | 10.254 % |
c |     38418 |  116265   367227 |   75547   38133  1549603    40.6 | 10.254 % |
c |     40127 |  116250   367174 |   83102   39840  1617198    40.6 | 10.258 % |
c |     42689 |  116240   367151 |   91412   42401  2204079    52.0 | 10.269 % |
c |     46534 |  116240   367151 |  100554   46246  3329116    72.0 | 10.269 % |
c |     52301 |  116152   366947 |  110609   51997  3586477    69.0 | 10.358 % |
c ==============================================================================
c Found solution: 20098343
c ---[   0]---> Adder-cost: 0   maxlim: 90341017   bits: 27/27
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     54707 |  116164   367132 |   38721   54400  3710224    68.2 | 10.358 % |
c |     54807 |  116164   367132 |   42593   21018  1537966    73.2 | 10.397 % |
c |     54957 |  116164   367132 |   46852   21168  1539261    72.7 | 10.397 % |
c |     55182 |  116164   367132 |   51537   21393  1548441    72.4 | 10.397 % |
c |     55519 |  116147   367092 |   56691   21728  1551262    71.4 | 10.415 % |
c |     56025 |  116147   367092 |   62360   22234  1575039    70.8 | 10.415 % |
c |     56784 |  116147   367092 |   68596   22993  1591214    69.2 | 10.415 % |
c |     57923 |  116147   367092 |   75456   24132  1624206    67.3 | 10.415 % |
c |     59631 |  116046   366858 |   83001   25826  1681307    65.1 | 10.540 % |
c |     62193 |  116031   366824 |   91302   28387  1971269    69.4 | 10.558 % |
c |     66038 |  116031   366824 |  100432   32232  2087700    64.8 | 10.558 % |
c |     71805 |  115982   366713 |  110475   37994  3139223    82.6 | 10.619 % |
c |     80456 |  115982   366713 |  121523   46645  3724239    79.8 | 10.619 % |
c ==============================================================================
c Found solution: 17569321
c ---[   0]---> Adder-cost: 0   maxlim: 92870039   bits: 27/27
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     80989 |  115995   366859 |   38665   47178  3741822    79.3 | 10.619 % |
c |     81090 |  115995   366859 |   42531   19172  1077340    56.2 | 10.647 % |
c |     81241 |  115959   366776 |   46784   19319  1078292    55.8 | 10.689 % |
c |     81466 |  115959   366776 |   51463   19544  1079800    55.2 | 10.689 % |
c |     81803 |  115959   366776 |   56609   19881  1082118    54.4 | 10.689 % |
c |     82309 |  115931   366712 |   62270   20384  1088389    53.4 | 10.718 % |
c |     83068 |  115855   366535 |   68497   21135  1099826    52.0 | 10.804 % |
c |     84207 |  115855   366535 |   75347   22274  1135609    51.0 | 10.804 % |
c |     85915 |  115810   366432 |   82881   23975  1162949    48.5 | 10.865 % |
c |     88478 |  115485   365681 |   91170   26523  1316452    49.6 | 11.244 % |
c |     92322 |  115485   365681 |  100287   30367  2736219    90.1 | 11.244 % |
c |     98088 |  115478   365658 |  110315   36131  3008753    83.3 | 11.248 % |
c |    106737 |  115471   365642 |  121347   44779  3674625    82.1 | 11.255 % |
c |    119711 |  115438   365566 |  133482   57752  4932903    85.4 | 11.291 % |
c |    139173 |  115438   365566 |  146830   77214 11296170   146.3 | 11.291 % |
c |    168366 |  115432   365552 |  161513  106406 14957006   140.6 | 11.298 % |
c |    212155 |  115432   365552 |  177664  150195 20355875   135.5 | 11.298 % |
c |    277839 |  115398   365473 |  195431   54617 10142303   185.7 | 11.334 % |
c |    376367 |  115304   365248 |  214974  153136 25171743   164.4 | 11.438 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v -X0_bit_7 -X0_bit_6 -X0_bit_5 -X0_bit_4 -X0_bit_3 -X0_bit_2 -X0_bit_1 -X0_bit0 -X0_bit1 -X0_bit2 -X0_bit3 -X0_bit4 -X0_bit5 -X0_bit6 -X0_bit7 -X0_bit8 -X0_bit9 -X0_bit10 -X0_bit11 -X0_bit12 X1_bit_7 X1_bit_6 X1_bit_5 X1_bit_4 -X1_bit_3 -X1_bit_2 -X1_bit_1 -X1_bit0 X1_bit1 -X1_bit2 -X1_bit3 -X1_bit4 -X1_bit5 -X1_bit6 -X1_bit7 -X1_bit8 -X1_bit9 -X1_bit10 -X1_bit11 -X1_bit12 -X2_bit_7 -X2_bit_6 -X2_bit_5 -X2_bit_4 -X2_bit_3 -X2_bit_2 -X2_bit_1 -X2_bit0 -X2_bit1 -X2_bit2 -X2_bit3 -X2_bit4 -X2_bit5 -X2_bit6 -X2_bit7 -X2_bit8 -X2_bit9 -X2_bit10 -X2_bit11 -X2_bit12 X3_bit_7 X3_bit_6 X3_bit_5 -X3_bit_4 X3_bit_3 -X3_bit_2 -X3_bit_1 -X3_bit0 -X3_bit1 -X3_bit2 X3_bit3 -X3_bit4 -X3_bit5 -X3_bit6 -X3_bit7 -X3_bit8 -X3_bit9 -X3_bit10 -X3_bit11 -X3_bit12 -X4_bit_7 -X4_bit_6 -X4_bit_5 -X4_bit_4 -X4_bit_3 -X4_bit_2 -X4_bit_1 -X4_bit0 -X4_bit1 -X4_bit2 -X4_bit3 -X4_bit4 -X4_bit5 -X4_bit6 -X4_bit7 -X4_bit8 -X4_bit9 -X4_bit10 -X4_bit11 -X4_bit12 X5_bit_7 X5_bit_6 -X5_bit_5 -X5_bit_4 X5_bit_3 -X5_bit_2 X5_bit_1 -X5_bit0 -X5_bit1 -X5_bit2 -X5_bit3 -X5_bit4 -X5_bit5 -X5_bit6 -X5_bit7 -X5_bit8 -X5_bit9 -X5_bit10 -X5_bit11 -X5_bit12 -X6_bit_7 -X6_bit_6 -X6_bit_5 -X6_bit_4 -X6_bit_3 -X6_bit_2 -X6_bit_1 -X6_bit0 -X6_bit1 -X6_bit2 -X6_bit3 -X6_bit4 -X6_bit5 -X6_bit6 -X6_bit7 -X6_bit8 -X6_bit9 -X6_bit10 -X6_bit11 -X6_bit12 -X7_bit_7 -X7_bit_6 -X7_bit_5 -X7_bit_4 -X7_bit_3 -X7_bit_2 -X7_bit_1 -X7_bit0 -X7_bit1 -X7_bit2 -X7_bit3 -X7_bit4 -X7_bit5 -X7_bit6 -X7_bit7 -X7_bit8 -X7_bit9 -X7_bit10 -X7_bit11 -X7_bit12 -X8_bit_7 -X8_bit_6 -X8_bit_5 -X8_bit_4 -X8_bit_3 -X8_bit_2 -X8_bit_1 -X8_bit0 -X8_bit1 -X8_bit2 -X8_bit3 -X8_bit4 -X8_bit5 -X8_bit6 -X8_bit7 -X8_bit8 -X8_bit9 -X8_bit10 -X8_bit11 -X8_bit12 X9_bit_7 X9_bit_6 X9_bit_5 -X9_bit_4 -X9_bit_3 -X9_bit_2 -X9_bit_1 -X9_bit0 -X9_bit1 X9_bit2 -X9_bit3 -X9_bit4 -X9_bit5 -X9_bit6 -X9_bit7 -X9_bit8 -X9_bit9 -X9_bit10 -X9_bit11 -X9_bit12 -X10_bit_7 -X10_bit_6 -X10_bit_5 -X10_bit_4 -X10_bit_3 -X10_bit_2 -X10_bit_1 -X10_bit0 -X10_bit1 -X10_bit2 -X10_bit3 -X10_bit4 -X10_bit5 -X10_bit6 -X10_bit7 -X10_bit8 -X10_bit9 -X10_bit10 -X10_bit11 -X10_bit12 -X11_bit_7 -X11_bit_6 -X11_bit_5 -X11_bit_4 -X11_bit_3 -X11_bit_2 -X11_bit_1 -X11_bit0 -X11_bit1 -X11_bit2 -X11_bit3 -X11_bit4 -X11_bit5 -X11_bit6 -X11_bit7 -X11_bit8 -X11_bit9 -X11_bit10 -X11_bit11 -X11_bit12 -X12_bit_7 -X12_bit_6 -X12_bit_5 -X12_bit_4 -X12_bit_3 -X12_bit_2 -X12_bit_1 -X12_bit0 -X12_bit1 -X12_bit2 -X12_bit3 -X12_bit4 -X12_bit5 -X12_bit6 -X12_bit7 -X12_bit8 -X12_bit9 -X12_bit10 -X12_bit11 -X12_bit12 -X13_bit_7 -X13_bit_6 -X13_bit_5 -X13_bit_4 -X13_bit_3 X13_bit_2 X13_bit_1 X13_bit0 -X13_bit1 -X13_bit2 -X13_bit3 -X13_bit4 -X13_bit5 -X13_bit6 -X13_bit7 -X13_bit8 -X13_bit9 -X13_bit10 -X13_bit11 -X13_bit12 X14_bit_7 X14_bit_6 X14_bit_5 X14_bit_4 X14_bit_3 X14_bit_2 X14_bit_1 X14_bit0 X14_bit1 -X14_bit2 -X14_bit3 -X14_bit4 -X14_bit5 -X14_bit6 -X14_bit7 -X14_bit8 -X14_bit9 -X14_bit10 -X14_bit11 -X14_bit12 -X15_bit_7 -X15_bit_6 -X15_bit_5 -X15_bit_4 -X15_bit_3 -X15_bit_2 -X15_bit_1 -X15_bit0 -X15_bit1 -X15_bit2 -X15_bit3 -X15_bit4 -X15_bit5 -X15_bit6 -X15_bit7 -X15_bit8 -X15_bit9 -X15_bit10 -X15_bit11 -X15_bit12 -X16_bit_7 -X16_bit_6 -X16_bit_5 -X16_bit_4 -X16_bit_3 -X16_bit_2 -X16_bit_1 -X16_bit0 -X16_bit1 -X16_bit2 -X16_bit3 -X16_bit4 -X16_bit5 -X16_bit6 -X16_bit7 -X16_bit8 -X16_bit9 -X16_bit10 -X16_bit11 -X16_bit12 -X17_bit_7 -X17_bit_6 -X17_bit_5 -X17_bit_4 -X17_bit_3 -X17_bit_2 -X17_bit_1 -X17_bit0 -X17_bit1 -X17_bit2 -X17_bit3 -X17_bit4 -X17_bit5 -X17_bit6 -X17_bit7 -X17_bit8 -X17_bit9 -X17_bit10 -X17_bit11 -X17_bit12 -X18_bit_7 -X18_bit_6 -X18_bit_5 -X18_bit_4 -X18_bit_3 -X18_bit_2 -X18_bit_1 -X18_bit0 -X18_bit1 -X18_bit2 -X18_bit3 -X18_bit4 -X18_bit5 -X18_bit6 -X18_bit7 -X18_bit8 -X18_bit9 -X18_bit10 -X18_bit11 -X18_bit12 -X19_bit_7 -X19_bit_6 -X19_bit_5 -X19_bit_4 -X19_bit_3 -X19_bit_2 -X19_bit_1 -X19_bit0 -X19_bit1 -X19_bit2 -X19_bit3 -X19_bit4 -X19_bit5 -X19_bit6 -X19_bit7 -X19_bit8 -X19_bit9 -X19_bit10 -X19_bit11 -X19_bit12 X20_bit_7 -X20_bit_6 -X20_bit_5 -X20_bit_4 -X20_bit_3 -X20_bit_2 -X20_bit_1 -X20_bit0 -X20_bit1 -X20_bit2 X20_bit3 -X20_bit4 -X20_bit5 -X20_bit6 -X20_bit7 -X20_bit8 -X20_bit9 -X20_bit10 -X20_bit11 -X20_bit12 X21_bit_7 -X21_bit_6 X21_bit_5 X21_bit_4 -X21_bit_3 X21_bit_2 X21_bit_1 X21_bit0 -X21_bit1 X21_bit2 -X21_bit3 -X21_bit4 -X21_bit5 -X21_bit6 -X21_bit7 -X21_bit8 -X21_bit9 -X21_bit10 -X21_bit11 -X21_bit12 -X22_bit_7 -X22_bit_6 -X22_bit_5 -X22_bit_4 -X22_bit_3 -X22_bit_2 -X22_bit_1 -X22_bit0 -X22_bit1 -X22_bit2 -X22_bit3 -X22_bit4 -X22_bit5 -X22_bit6 -X22_bit7 -X22_bit8 -X22_bit9 -X22_bit10 -X22_bit11 -X22_bit12 X23_bit_7 X23_bit_6 -X23_bit_5 -X23_bit_4 X23_bit_3 X23_bit_2 -X23_bit_1 -X23_bit0 -X23_bit1 -X23_bit2 -X23_bit3 -X23_bit4 -X23_bit5 -X23_bit6 -X23_bit7 -X23_bit8 -X23_bit9 -X23_bit10 -X23_bit11 -X23_bit12 X24_bit_7 -X24_bit_6 -X24_bit_5 -X24_bit_4 X24_bit_3 X24_bit_2 X24_bit_1 X24_bit0 X24_bit1 -X24_bit2 X24_bit3 -X24_bit4 -X24_bit5 -X24_bit6 -X24_bit7 -X24_bit8 -X24_bit9 -X24_bit10 -X24_bit11 -X24_bit12 -X25_bit_7 -X25_bit_6 -X25_bit_5 -X25_bit_4 -X25_bit_3 -X25_bit_2 -X25_bit_1 -X25_bit0 -X25_bit1 -X25_bit2 -X25_bit3 -X25_bit4 -X25_bit5 -X25_bit6 -X25_bit7 -X25_bit8 -X25_bit9 -X25_bit10 -X25_bit11 -X25_bit12 -X26_bit_7 -X26_bit_6 -X26_bit_5 -X26_bit_4 -X26_bit_3 -X26_bit_2 -X26_bit_1 -X26_bit0 -X26_bit1 -X26_bit2 -X26_bit3 -X26_bit4 -X26_bit5 -X26_bit6 -X26_bit7 -X26_bit8 -X26_bit9 -X26_bit10 -X26_bit11 -X26_bit12 -X27_bit_7 -X27_bit_6 -X27_bit_5 -X27_bit_4 -X27_bit_3 -X27_bit_2 -X27_bit_1 -X27_bit0 -X27_bit1 -X27_bit2 -X27_bit3 -X27_bit4 -X27_bit5 -X27_bit6 -X27_bit7 -X27_bit8 -X27_bit9 -X27_bit10 -X27_bit11 -X27_bit12 -X28_bit_7 -X28_bit_6 -X28_bit_5 -X28_bit_4 -X28_bit_3 -X28_bit_2 -X28_bit_1 -X28_bit0 -X28_bit1 -X28_bit2 -X28_bit3 -X28_bit4 -X28_bit5 -X28_bit6 -X28_bit7 -X28_bit8 -X28_bit9 -X28_bit10 -X28_bit11 -X28_bit12 -X29_bit_7 -X29_bit_6 -X29_bit_5 -X29_bit_4 -X29_bit_3 -X29_bit_2 -X29_bit_1 -X29_bit0 -X29_bit1 -X29_bit2 -X29_bit3 -X29_bit4 -X29_bit5 -X29_bit6 -X29_bit7 -X29_bit8 -X29_bit9 -X29_bit10 -X29_bit11 -X29_bit12 -X30_bit_7 -X30_bit_6 -X30_bit_5 -X30_bit_4 -X30_bit_3 -X30_bit_2 -X30_bit_1 -X30_bit0 -X30_bit1 -X30_bit2 -X30_bit3 -X30_bit4 -X30_bit5 -X30_bit6 -X30_bit7 -X30_bit8 -X30_bit9 -X30_bit10 -X30_bit11 -X30_bit12 -X31_bit_7 -X31_bit_6 -X31_bit_5 -X31_bit_4 -X31_bit_3 -X31_bit_2 -X31_bit_1 -X31_bit0 -X31_bit1 -X31_bit2 -X31_bit3 -X31_bit4 -X31_bit5 -X31_bit6 -X31_bit7 -X31_bit8 -X31_bit9 -X31_bit10 -X31_bit11 -X31_bit12 X32_bit_7 -X32_bit_6 -X32_bit_5 -X32_bit_4 X32_bit_3 -X32_bit_2 -X32_bit_1 X32_bit0 -X32_bit1 X32_bit2 X32_bit3 -X32_bit4 -X32_bit5 -X32_bit6 -X32_bit7 -X32_bit8 -X32_bit9 -X32_bit10 -X32_bit11 -X32_bit12 X33_bit_7 X33_bit_6 X33_bit_5 X33_bit_4 -X33_bit_3 X33_bit_2 X33_bit_1 X33_bit0 X33_bit1 X33_bit2 -X33_bit3 -X33_bit4 -X33_bit5 -X33_bit6 -X33_bit7 -X33_bit8 -X33_bit9 -X33_bit10 -X33_bit11 -X33_bit12 -X34_bit_7 -X34_bit_6 -X34_bit_5 -X34_bit_4 X34_bit_3 X34_bit_2 -X34_bit_1 -X34_bit0 -X34_bit1 -X34_bit2 X34_bit3 -X34_bit4 -X34_bit5 -X34_bit6 -X34_bit7 -X34_bit8 -X34_bit9 -X34_bit10 -X34_bit11 -X34_bit12 X35_bit_7 X35_bit_6 X35_bit_5 X35_bit_4 X35_bit_3 -X35_bit_2 X35_bit_1 X35_bit0 X35_bit1 -X35_bit2 -X35_bit3 -X35_bit4 -X35_bit5 -X35_bit6 -X35_bit7 -X35_bit8 -X35_bit9 -X35_bit10 -X35_bit11 -X35_bit12 X36_bit_7 -X36_bit_6 X36_bit_5 X36_bit_4 X36_bit_3 X36_bit_2 X36_bit_1 X36_bit0 X36_bit1 X36_bit2 -X36_bit3 -X36_bit4 -X36_bit5 -X36_bit6 -X36_bit7 -X36_bit8 -X36_bit9 -X36_bit10 -X36_bit11 -X36_bit12 X37_bit_7 X37_bit_6 X37_bit_5 X37_bit_4 -X37_bit_3 X37_bit_2 -X37_bit_1 -X37_bit0 X37_bit1 -X37_bit2 -X37_bit3 -X37_bit4 -X37_bit5 -X37_bit6 -X37_bit7 -X37_bit8 -X37_bit9 -X37_bit10 -X37_bit11 -X37_bit12 X38_bit_7 -X38_bit_6 X38_bit_5 X38_bit_4 -X38_bit_3 X38_bit_2 -X38_bit_1 X38_bit0 -X38_bit1 X38_bit2 X38_bit3 -X38_bit4 -X38_bit5 -X38_bit6 -X38_bit7 -X38_bit8 -X38_bit9 -X38_bit10 -X38_bit11 -X38_bit12 X39_bit_7 X39_bit_6 X39_bit_5 X39_bit_4 -X39_bit_3 -X39_bit_2 -X39_bit_1 -X39_bit0 -X39_bit1 -X39_bit2 -X39_bit3 -X39_bit4 -X39_bit5 -X39_bit6 -X39_bit7 -X39_bit8 -X39_bit9 -X39_bit10 -X39_bit11 -X39_bit12 X40_bit_7 X40_bit_6 X40_bit_5 -X40_bit_4 X40_bit_3 X40_bit_2 X40_bit_1 -X40_bit0 -X40_bit1 -X40_bit2 -X40_bit3 -X40_bit4 -X40_bit5 -X40_bit6 -X40_bit7 -X40_bit8 -X40_bit9 -X40_bit10 -X40_bit11 -X40_bit12 X41_bit_7 X41_bit_6 -X41_bit_5 X41_bit_4 -X41_bit_3 X41_bit_2 -X41_bit_1 -X41_bit0 -X41_bit1 -X41_bit2 X41_bit3 -X41_bit4 -X41_bit5 -X41_bit6 -X41_bit7 -X41_bit8 -X41_bit9 -X41_bit10 -X41_bit11 -X41_bit12 -X42_bit_7 -X42_bit_6 -X42_bit_5 -X42_bit_4 -X42_bit_3 -X42_bit_2 -X42_bit_1 -X42_bit0 -X42_bit1 -X42_bit2 -X42_bit3 -X42_bit4 -X42_bit5 -X42_bit6 -X42_bit7 -X42_bit8 -X42_bit9 -X42_bit10 -X42_bit11 -X42_bit12 X43_bit_7 X43_bit_6 X43_bit_5 X43_bit_4 -X43_bit_3 X43_bit_2 -X43_bit_1 X43_bit0 -X43_bit1 -X43_bit2 -X43_bit3 -X43_bit4 -X43_bit5 -X43_bit6 -X43_bit7 -X43_bit8 -X43_bit9 -X43_bit10 -X43_bit11 -X43_bit12 -X44_bit_7 -X44_bit_6 -X44_bit_5 -X44_bit_4 -X44_bit_3 -X44_bit_2 -X44_bit_1 -X44_bit0 -X44_bit1 -X44_bit2 -X44_bit3 -X44_bit4 -X44_bit5 -X44_bit6 -X44_bit7 -X44_bit8 -X44_bit9 -X44_bit10 -X44_bit11 -X44_bit12 -X45_bit_7 -X45_bit_6 -X45_bit_5 -X45_bit_4 -X45_bit_3 -X45_bit_2 -X45_bit_1 -X45_bit0 -X45_bit1 -X45_bit2 -X45_bit3 -X45_bit4 -X45_bit5 -X45_bit6 -X45_bit7 -X45_bit8 -X45_bit9 -X45_bit10 -X45_bit11 -X45_bit12 -X46_bit_7 -X46_bit_6 -X46_bit_5 -X46_bit_4 -X46_bit_3 -X46_bit_2 -X46_bit_1 -X46_bit0 -X46_bit1 -X46_bit2 -X46_bit3 -X46_bit4 -X46_bit5 -X46_bit6 -X46_bit7 -X46_bit8 -X46_bit9 -X46_bit10 -X46_bit11 -X46_bit12 X47_bit_7 X47_bit_6 X47_bit_5 -X47_bit_4 -X47_bit_3 -X47_bit_2 X47_bit_1 -X47_bit0 -X47_bit1 -X47_bit2 -X47_bit3 -X47_bit4 -X47_bit5 -X47_bit6 -X47_bit7 -X47_bit8 -X47_bit9 -X47_bit10 -X47_bit11 -X47_bit12 -X48_bit_7 X48_bit_6 X48_bit_5 -X48_bit_4 -X48_bit_3 -X48_bit_2 -X48_bit_1 -X48_bit0 -X48_bit1 -X48_bit2 -X48_bit3 -X48_bit4 -X48_bit5 -X48_bit6 -X48_bit7 -X48_bit8 -X48_bit9 -X48_bit10 -X48_bit11 -X48_bit12 -X49_bit_7 -X49_bit_6 -X49_bit_5 -X49_bit_4 -X49_bit_3 -X49_bit_2 -X49_bit_1 -X49_bit0 -X49_bit1 -X49_bit2 -X49_bit3 -X49_bit4 -X49_bit5 -X49_bit6 -X49_bit7 -X49_bit8 -X49_bit9 -X49_bit10 -X49_bit11 -X49_bit12 -X50_bit_7 -X50_bit_6 -X50_bit_5 -X50_bit_4 -X50_bit_3 -X50_bit_2 -X50_bit_1 -X50_bit0 -X50_bit1 -X50_bit2 -X50_bit3 -X50_bit4 -X50_bit5 -X50_bit6 -X50_bit7 -X50_bit8 -X50_bit9 -X50_bit10 -X50_bit11 -X50_bit12 -X51_bit_7 -X51_bit_6 X51_bit_5 X51_bit_4 -X51_bit_3 -X51_bit_2 -X51_bit_1 -X51_bit0 -X51_bit1 X51_bit2 -X51_bit3 -X51_bit4 -X51_bit5 -X51_bit6 -X51_bit7 -X51_bit8 -X51_bit9 -X51_bit10 -X51_bit11 -X51_bit12 X52_bit_7 -X52_bit_6 -X52_bit_5 X52_bit_4 -X52_bit_3 -X52_bit_2 -X52_bit_1 -X52_bit0 -X52_bit1 X52_bit2 -X52_bit3 -X52_bit4 -X52_bit5 -X52_bit6 -X52_bit7 -X52_bit8 -X52_bit9 -X52_bit10 -X52_bit11 -X52_bit12 -X53_bit_7 -X53_bit_6 -X53_bit_5 -X53_bit_4 -X53_bit_3 -X53_bit_2 -X53_bit_1 -X53_bit0 -X53_bit1 -X53_bit2 -X53_bit3 -X53_bit4 -X53_bit5 -X53_bit6 -X53_bit7 -X53_bit8 -X53_bit9 -X53_bit10 -X53_bit11 -X53_bit12 -X54_bit_7 X54_bit_6 -X54_bit_5 -X54_bit_4 -X54_bit_3 X54_bit_2 X54_bit_1 -X54_bit0 -X54_bit1 -X54_bit2 -X54_bit3 X54_bit4 -X54_bit5 -X54_bit6 -X54_bit7 -X54_bit8 -X54_bit9 -X54_bit10 -X54_bit11 -X54_bit12 -X55_bit_7 -X55_bit_6 -X55_bit_5 -X55_bit_4 -X55_bit_3 -X55_bit_2 -X55_bit_1 -X55_bit0 -X55_bit1 -X55_bit2 -X55_bit3 -X55_bit4 -X55_bit5 -X55_bit6 -X55_bit7 -X55_bit8 -X55_bit9 -X55_bit10 -X55_bit11 -X55_bit12 -X56_bit_7 -X56_bit_6 -X56_bit_5 -X56_bit_4 -X56_bit_3 -X56_bit_2 -X56_bit_1 -X56_bit0 -X56_bit1 -X56_bit2 -X56_bit3 -X56_bit4 -X56_bit5 -X56_bit6 -X56_bit7 -X56_bit8 -X56_bit9 -X56_bit10 -X56_bit11 -X56_bit12 -X57_bit_7 -X57_bit_6 -X57_bit_5 -X57_bit_4 -X57_bit_3 -X57_bit_2 -X57_bit_1 -X57_bit0 -X57_bit1 -X57_bit2 -X57_bit3 -X57_bit4 -X57_bit5 -X57_bit6 -X57_bit7 -X57_bit8 -X57_bit9 -X57_bit10 -X57_bit11 -X57_bit12 -X58_bit_7 -X58_bit_6 -X58_bit_5 -X58_bit_4 -X58_bit_3 -X58_bit_2 -X58_bit_1 -X58_bit0 -X58_bit1 -X58_bit2 -X58_bit3 -X58_bit4 -X58_bit5 -X58_bit6 -X58_bit7 -X58_bit8 -X58_bit9 -X58_bit10 -X58_bit11 -X58_bit12 X59_bit_7 X59_bit_6 -X59_bit_5 -X59_bit_4 -X59_bit_3 -X59_bit_2 -X59_bit_1 -X59_bit0 -X59_bit1 -X59_bit2 -X59_bit3 -X59_bit4 -X59_bit5 -X59_bit6 -X59_bit7 -X59_bit8 -X59_bit9 -X59_bit10 -X59_bit11 -X59_bit12 -X60_bit_7 -X60_bit_6 -X60_bit_5 -X60_bit_4 -X60_bit_3 -X60_bit_2 -X60_bit_1 -X60_bit0 -X60_bit1 -X60_bit2 -X60_bit3 -X60_bit4 -X60_bit5 -X60_bit6 -X60_bit7 -X60_bit8 -X60_bit9 -X60_bit10 -X60_bit11 -X60_bit12 -X61_bit_7 -X61_bit_6 X61_bit_5 -X61_bit_4 X61_bit_3 -X61_bit_2 X61_bit_1 -X61_bit0 -X61_bit1 -X61_bit2 -X61_bit3 -X61_bit4 -X61_bit5 -X61_bit6 -X61_bit7 -X61_bit8 -X61_bit9 -X61_bit10 -X61_bit11 -X61_bit12 -X62_bit_7 -X62_bit_6 X62_bit_5 -X62_bit_4 X62_bit_3 -X62_bit_2 X62_bit_1 -X62_bit0 X62_bit1 -X62_bit2 -X62_bit3 -X62_bit4 -X62_bit5 -X62_bit6 -X62_bit7 -X62_bit8 -X62_bit9 -X62_bit10 -X62_bit11 -X62_bit12 -X63_bit_7 -X63_bit_6 -X63_bit_5 -X63_bit_4 -X63_bit_3 -X63_bit_2 -X63_bit_1 -X63_bit0 -X63_bit1 -X63_bit2 -X63_bit3 -X63_bit4 -X63_bit5 -X63_bit6 -X63_bit7 -X63_bit8 -X63_bit9 -X63_bit10 -X63_bit11 -X63_bit12 -X64_bit_7 -X64_bit_6 -X64_bit_5 -X64_bit_4 -X64_bit_3 -X64_bit_2 -X64_bit_1 -X64_bit0 -X64_bit1 -X64_bit2 -X64_bit3 -X64_bit4 -X64_bit5 -X64_bit6 -X64_bit7 -X64_bit8 -X64_bit9 -X64_bit10 -X64_bit11 -X64_bit12 X65_bit_7 -X65_bit_6 -X65_bit_5 X65_bit_4 X65_bit_3 X65_bit_2 X65_bit_1 -X65_bit0 -X65_bit1 -X65_bit2 X65_bit3 -X65_bit4 -X65_bit5 -X65_bit6 -X65_bit7 -X65_bit8 -X65_bit9 -X65_bit10 -X65_bit11 -X65_bit12 -X66_bit_7 -X66_bit_6 -X66_bit_5 -X66_bit_4 -X66_bit_3 -X66_bit_2 -X66_bit_1 -X66_bit0 -X66_bit1 -X66_bit2 -X66_bit3 -X66_bit4 -X66_bit5 -X66_bit6 -X66_bit7 -X66_bit8 -X66_bit9 -X66_bit10 -X66_bit11 -X66_bit12 X67_bit_7 -X67_bit_6 -X67_bit_5 -X67_bit_4 X67_bit_3 -X67_bit_2 X67_bit_1 -X67_bit0 -X67_bit1 -X67_bit2 X67_bit3 -X67_bit4 -X67_bit5 -X67_bit6 -X67_bit7 -X67_bit8 -X67_bit9 -X67_bit10 -X67_bit11 -X67_bit12 -X68_bit_7 -X68_bit_6 -X68_bit_5 -X68_bit_4 X68_bit_3 X68_bit_2 X68_bit_1 -X68_bit0 X68_bit1 -X68_bit2 X68_bit3 -X68_bit4 -X68_bit5 -X68_bit6 -X68_bit7 -X68_bit8 -X68_bit9 -X68_bit10 -X68_bit11 -X68_bit12 -X69_bit_7 X69_bit_6 X69_bit_5 X69_bit_4 X69_bit_3 -X69_bit_2 -X69_bit_1 X69_bit0 X69_bit1 -X69_bit2 -X69_bit3 -X69_bit4 -X69_bit5 -X69_bit6 -X69_bit7 -X69_bit8 -X69_bit9 -X69_bit10 -X69_bit11 -X69_bit12 -X70_bit_7 -X70_bit_6 -X70_bit_5 -X70_bit_4 -X70_bit_3 -X70_bit_2 -X70_bit_1 -X70_bit0 -X70_bit1 -X70_bit2 -X70_bit3 -X70_bit4 -X70_bit5 -X70_bit6 -X70_bit7 -X70_bit8 -X70_bit9 -X70_bit10 -X70_bit11 -X70_bit12 -X71_bit_7 -X71_bit_6 -X71_bit_5 -X71_bit_4 -X71_bit_3 -X71_bit_2 -X71_bit_1 -X71_bit0 -X71_bit1 -X71_bit2 -X71_bit3 -X71_bit4 -X71_bit5 -X71_bit6 -X71_bit7 -X71_bit8 -X71_bit9 -X71_bit10 -X71_bit11 -X71_bit12 -X72_bit_7 -X72_bit_6 X72_bit_5 X72_bit_4 -X72_bit_3 -X72_bit_2 -X72_bit_1 -X72_bit0 -X72_bit1 -X72_bit2 -X72_bit3 -X72_bit4 -X72_bit5 -X72_bit6 -X72_bit7 -X72_bit8 -X72_bit9 -X72_bit10 -X72_bit11 -X72_bit12 X73_bit_7 X73_bit_6 X73_bit_5 X73_bit_4 -X73_bit_3 -X73_bit_2 -X73_bit_1 -X73_bit0 -X73_bit1 -X73_bit2 -X73_bit3 -X73_bit4 -X73_bit5 -X73_bit6 -X73_bit7 -X73_bit8 -X73_bit9 -X73_bit10 -X73_bit11 -X73_bit12 -X74_bit_7 -X74_bit_6 -X74_bit_5 -X74_bit_4 -X74_bit_3 -X74_bit_2 -X74_bit_1 -X74_bit0 -X74_bit1 -X74_bit2 -X74_bit3 -X74_bit4 -X74_bit5 -X74_bit6 -X74_bit7 -X74_bit8 -X74_bit9 -X74_bit10 -X74_bit11 -X74_bit12 X75_bit_7 X75_bit_6 X75_bit_5 X75_bit_4 -X75_bit_3 -X75_bit_2 -X75_bit_1 -X75_bit0 -X75_bit1 -X75_bit2 -X75_bit3 -X75_bit4 -X75_bit5 -X75_bit6 -X75_bit7 -X75_bit8 -X75_bit9 -X75_bit10 -X75_bit11 -X75_bit12 -X76_bit_7 -X76_bit_6 -X76_bit_5 -X76_bit_4 -X76_bit_3 -X76_bit_2 -X76_bit_1 -X76_bit0 -X76_bit1 -X76_bit2 -X76_bit3 -X76_bit4 -X76_bit5 -X76_bit6 -X76_bit7 -X76_bit8 -X76_bit9 -X76_bit10 -X76_bit11 -X76_bit12 X77_bit_7 X77_bit_6 X77_bit_5 X77_bit_4 -X77_bit_3 -X77_bit_2 -X77_bit_1 -X77_bit0 -X77_bit1 -X77_bit2 -X77_bit3 -X77_bit4 -X77_bit5 -X77_bit6 -X77_bit7 -X77_bit8 -X77_bit9 -X77_bit10 -X77_bit11 -X77_bit12 X78_bit_7 X78_bit_6 -X78_bit_5 -X78_bit_4 -X78_bit_3 X78_bit_2 -X78_bit_1 X78_bit0 -X78_bit1 -X78_bit2 X78_bit3 -X78_bit4 -X78_bit5 -X78_bit6 -X78_bit7 -X78_bit8 -X78_bit9 -X78_bit10 -X78_bit11 -X78_bit12 -X79_bit_7 -X79_bit_6 -X79_bit_5 -X79_bit_4 -X79_bit_3 -X79_bit_2 -X79_bit_1 -X79_bit0 -X79_bit1 -X79_bit2 -X79_bit3 -X79_bit4 -X79_bit5 -X79_bit6 -X79_bit7 -X79_bit8 -X79_bit9 -X79_bit10 -X79_bit11 -X79_bit12 -X80_bit_7 -X80_bit_6 -X80_bit_5 -X80_bit_4 -X80_bit_3 -X80_bit_2 -X80_bit_1 -X80_bit0 -X80_bit1 -X80_bit2 -X80_bit3 -X80_bit4 -X80_bit5 -X80_bit6 -X80_bit7 -X80_bit8 -X80_bit9 -X80_bit10 -X80_bit11 -X80_bit12 -X81_bit_7 -X81_bit_6 -X81_bit_5 -X81_bit_4 -X81_bit_3 -X81_bit_2 -X81_bit_1 -X81_bit0 -X81_bit1 -X81_bit2 -X81_bit3 -X81_bit4 -X81_bit5 -X81_bit6 -X81_bit7 -X81_bit8 -X81_bit9 -X81_bit10 -X81_bit11 -X81_bit12 -X82_bit_7 -X82_bit_6 -X82_bit_5 -X82_bit_4 -X82_bit_3 -X82_bit_2 -X82_bit_1 -X82_bit0 -X82_bit1 -X82_bit2 -X82_bit3 -X82_bit4 -X82_bit5 -X82_bit6 -X82_bit7 -X82_bit8 -X82_bit9 -X82_bit10 -X82_bit11 -X82_bit12 -X83_bit_7 -X83_bit_6 X83_bit_5 -X83_bit_4 -X83_bit_3 X83_bit_2 -X83_bit_1 -X83_bit0 -X83_bit1 -X83_bit2 -X83_bit3 -X83_bit4 -X83_bit5 -X83_bit6 -X83_bit7 -X83_bit8 -X83_bit9 -X83_bit10 -X83_bit11 -X83_bit12 -X84_bit_7 -X84_bit_6 -X84_bit_5 -X84_bit_4 -X84_bit_3 -X84_bit_2 -X84_bit_1 -X84_bit0 -X84_bit1 -X84_bit2 -X84_bit3 -X84_bit4 -X84_bit5 -X84_bit6 -X84_bit7 -X84_bit8 -X84_bit9 -X84_bit10 -X84_bit11 -X84_bit12 X85_bit_7 X85_bit_6 X85_bit_5 X85_bit_4 X85_bit_3 X85_bit_2 X85_bit_1 X85_bit0 X85_bit1 X85_bit2 -X85_bit3 -X85_bit4 -X85_bit5 -X85_bit6 -X85_bit7 -X85_bit8 -X85_bit9 -X85_bit10 -X85_bit11 -X85_bit12 -X86_bit_7 -X86_bit_6 -X86_bit_5 -X86_bit_4 -X86_bit_3 -X86_bit_2 -X86_bit_1 -X86_bit0 -X86_bit1 -X86_bit2 -X86_bit3 -X86_bit4 -X86_bit5 -X86_bit6 -X86_bit7 -X86_bit8 -X86_bit9 -X86_bit10 -X86_bit11 -X86_bit12 X87_bit_7 X87_bit_6 X87_bit_5 X87_bit_4 X87_bit_3 X87_bit_2 -X87_bit_1 -X87_bit0 X87_bit1 -X87_bit2 -X87_bit3 -X87_bit4 -X87_bit5 -X87_bit6 -X87_bit7 -X87_bit8 -X87_bit9 -X87_bit10 -X87_bit11 -X87_bit12 -X88_bit_7 -X88_bit_6 -X88_bit_5 -X88_bit_4 -X88_bit_3 -X88_bit_2 -X88_bit_1 -X88_bit0 -X88_bit1 -X88_bit2 -X88_bit3 -X88_bit4 -X88_bit5 -X88_bit6 -X88_bit7 -X88_bit8 -X88_bit9 -X88_bit10 -X88_bit11 -X88_bit12 -X89_bit_7 X89_bit_6 -X89_bit_5 X89_bit_4 X89_bit_3 X89_bit_2 X89_bit_1 X89_bit0 -X89_bit1 -X89_bit2 -X89_bit3 -X89_bit4 -X89_bit5 -X89_bit6 -X89_bit7 -X89_bit8 -X89_bit9 -X89_bit10 -X89_bit11 -X89_bit12 X90_bit_7 X90_bit_6 -X90_bit_5 X90_bit_4 X90_bit_3 X90_bit_2 X90_bit_1 X90_bit0 X90_bit1 -X90_bit2 -X90_bit3 -X90_bit4 -X90_bit5 -X90_bit6 -X90_bit7 -X90_bit8 -X90_bit9 -X90_bit10 -X90_bit11 -X90_bit12 -X91_bit_7 -X91_bit_6 -X91_bit_5 -X91_bit_4 -X91_bit_3 -X91_bit_2 -X91_bit_1 -X91_bit0 -X91_bit1 -X91_bit2 -X91_bit3 -X91_bit4 -X91_bit5 -X91_bit6 -X91_bit7 -X91_bit8 -X91_bit9 -X91_bit10 -X91_bit11 -X91_bit12 -X92_bit_7 X92_bit_6 X92_bit_5 X92_bit_4 X92_bit_3 X92_bit_2 X92_bit_1 -X92_bit0 X92_bit1 -X92_bit2 -X92_bit3 -X92_bit4 -X92_bit5 -X92_bit6 -X92_bit7 -X92_bit8 -X92_bit9 -X92_bit10 -X92_bit11 -X92_bit12 X93_bit_7 X93_bit_6 X93_bit_5 X93_bit_4 X93_bit_3 X93_bit_2 X93_bit_1 X93_bit0 X93_bit1 -X93_bit2 -X93_bit3 -X93_bit4 -X93_bit5 -X93_bit6 -X93_bit7 -X93_bit8 -X93_bit9 -X93_bit10 -X93_bit11 -X93_bit12 -X94_bit_7 -X94_bit_6 -X94_bit_5 -X94_bit_4 X94_bit_3 -X94_bit_2 X94_bit_1 X94_bit0 -X94_bit1 -X94_bit2 -X94_bit3 -X94_bit4 -X94_bit5 -X94_bit6 -X94_bit7 -X94_bit8 -X94_bit9 -X94_bit10 -X94_bit11 -X94_bit12 -X95_bit_7 -X95_bit_6 -X95_bit_5 -X95_bit_4 -X95_bit_3 -X95_bit_2 -X95_bit_1 -X95_bit0 -X95_bit1 -X95_bit2 -X95_bit3 -X95_bit4 -X95_bit5 -X95_bit6 -X95_bit7 -X95_bit8 -X95_bit9 -X95_bit10 -X95_bit11 -X95_bit12 -Y0_bit0 Y1_bit0 -Y2_bit0 Y3_bit0 -Y4_bit0 Y5_bit0 -Y6_bit0 -Y7_bit0 -Y8_bit0 Y9_bit0 -Y10_bit0 -Y11_bit0 -Y12_bit0 Y13_bit0 Y14_bit0 -Y15_bit0 -Y16_bit0 -Y17_bit0 -Y18_bit0 -Y19_bit0 Y20_bit0 Y21_bit0 -Y22_bit0 Y23_bit0 Y24_bit0 -Y25_bit0 -Y26_bit0 -Y27_bit0 -Y28_bit0 -Y29_bit0 -Y30_bit0 -Y31_bit0 Y32_bit0 Y33_bit0 Y34_bit0 Y35_bit0 Y36_bit0 Y37_bit0 Y38_bit0 Y39_bit0 Y40_bit0 Y41_bit0 -Y42_bit0 Y43_bit0 -Y44_bit0 -Y45_bit0 -Y46_bit0 Y47_bit0 Y48_bit0 -Y49_bit0 -Y50_bit0 Y51_bit0 Y52_bit0 -Y53_bit0 Y54_bit0 Y55_bit0 Y56_bit0 -Y57_bit0 -Y58_bit0 Y59_bit0 -Y60_bit0 Y61_bit0 Y62_bit0 -Y63_bit0 -Y64_bit0 Y65_bit0 -Y66_bit0 Y67_bit0 Y68_bit0 Y69_bit0 -Y70_bit0 -Y71_bit0 Y72_bit0 Y73_bit0 -Y74_bit0 Y75_bit0 -Y7

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/16775/stat): 16775 (minisat+_script) R 16774 16775 21452 0 -1 0 19 0 0 0 0 0 0 0 22 0 1 0 1855876225 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 0 0 0
Raw data (/proc/16775/statm): 174 3 169 147 0 27 0
[pid=16775] 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=16776
New process pid=16777
New process pid=16778
execve syscall for /bin/sed executable
One traced child (pid=16777) 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=16778) exited with status: 0
One traced child (pid=16776) exited with status: 0
New process pid=16779
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-bal8x12.opb

[startup+10.0039 s]
Raw data (loadavg): 0.97 0.98 0.91 2/57 16779
Raw data (/proc/16775/stat): 16775 (minisat+_script) S 16774 16775 21452 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855876225 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16775/statm): 531 226 485 147 0 384 0
[pid=16775] vsize: 2124
Raw data (/proc/16779/stat): 16779 (minisat+_64-bit) R 16775 16775 21452 0 -1 0 1926 0 0 0 980 6 0 0 25 0 1 0 1855876230 8769536 1829 4294967295 134512640 135094434 3221224432 3221223088 134557925 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16779/statm): 2141 1829 145 145 0 1996 0
[pid=16779] vsize: 8564
Current children cumulated CPU time (s) 9.87
Current children cumulated vsize (Kb) 10688

[startup+20.0046 s]
Raw data (loadavg): 0.98 0.98 0.91 2/57 16779
Raw data (/proc/16775/stat): 16775 (minisat+_script) S 16774 16775 21452 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855876225 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16775/statm): 531 226 485 147 0 384 0
[pid=16775] vsize: 2124
Raw data (/proc/16779/stat): 16779 (minisat+_64-bit) R 16775 16775 21452 0 -1 0 2315 0 0 0 1978 7 0 0 25 0 1 0 1855876230 10428416 2176 4294967295 134512640 135094434 3221224432 3221221456 134600267 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16779/statm): 2546 2176 145 145 0 2401 0
[pid=16779] vsize: 10184
Current children cumulated CPU time (s) 19.86
Current children cumulated vsize (Kb) 12308

[startup+30.0064 s]
Raw data (loadavg): 0.98 0.98 0.91 2/57 16779
Raw data (/proc/16775/stat): 16775 (minisat+_script) S 16774 16775 21452 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855876225 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16775/statm): 531 226 485 147 0 384 0
[pid=16775] vsize: 2124
Raw data (/proc/16779/stat): 16779 (minisat+_64-bit) R 16775 16775 21452 0 -1 0 8100 0 0 0 2943 27 0 0 25 0 1 0 1855876230 30035968 6633 4294967295 134512640 135094434 3221224432 3221223056 134557565 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16779/statm): 7333 6633 145 145 0 7188 0
[pid=16779] vsize: 29332
Current children cumulated CPU time (s) 29.71
Current children cumulated vsize (Kb) 31456

[startup+40.0071 s]
Raw data (loadavg): 0.98 0.98 0.91 2/57 16779
Raw data (/proc/16775/stat): 16775 (minisat+_script) S 16774 16775 21452 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855876225 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16775/statm): 531 226 485 147 0 384 0
[pid=16775] vsize: 2124
Raw data (/proc/16779/stat): 16779 (minisat+_64-bit) R 16775 16775 21452 0 -1 0 8329 0 0 0 3941 28 0 0 25 0 1 0 1855876230 30572544 6756 4294967295 134512640 135094434 3221224432 3221221524 134676335 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16779/statm): 7464 6756 145 145 0 7319 0
[pid=16779] vsize: 29856
Current children cumulated CPU time (s) 39.7
Current children cumulated vsize (Kb) 31980

[startup+50.0078 s]
Raw data (loadavg): 0.98 0.98 0.91 2/57 16779
Raw data (/proc/16775/stat): 16775 (minisat+_script) S 16774 16775 21452 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855876225 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16775/statm): 531 226 485 147 0 384 0
[pid=16775] vsize: 2124
Raw data (/proc/16779/stat): 16779 (minisat+_64-bit) R 16775 16775 21452 0 -1 0 8356 0 0 0 4941 28 0 0 25 0 1 0 1855876230 30547968 6750 4294967295 134512640 135094434 3221224432 3221222160 134677307 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16779/statm): 7458 6750 145 145 0 7313 0
[pid=16779] vsize: 29832
Current children cumulated CPU time (s) 49.7
Current children cumulated vsize (Kb) 31956

[startup+60.0085 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 16779
Raw data (/proc/16775/stat): 16775 (minisat+_script) S 16774 16775 21452 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855876225 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16775/statm): 531 226 485 147 0 384 0
[pid=16775] vsize: 2124
Raw data (/proc/16779/stat): 16779 (minisat+_64-bit) R 16775 16775 21452 0 -1 0 8580 0 0 0 5937 30 0 0 25 0 1 0 1855876230 31031296 6900 4294967295 134512640 135094434 3221224432 3221221280 134676539 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16779/statm): 7576 6900 145 145 0 7431 0
[pid=16779] vsize: 30304
Current children cumulated CPU time (s) 59.68
Current children cumulated vsize (Kb) 32428

[startup+70.0092 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 16779
Raw data (/proc/16775/stat): 16775 (minisat+_script) S 16774 16775 21452 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855876225 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16775/statm): 531 226 485 147 0 384 0
[pid=16775] vsize: 2124
Raw data (/proc/16779/stat): 16779 (minisat+_64-bit) R 16775 16775 21452 0 -1 0 8629 0 0 0 6935 31 0 0 25 0 1 0 1855876230 31240192 6949 4294967295 134512640 135094434 3221224432 3221219872 134518536 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16779/statm): 7627 6949 145 145 0 7482 0
[pid=16779] vsize: 30508
Current children cumulated CPU time (s) 69.67
Current children cumulated vsize (Kb) 32632

[startup+80.0109 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 16779
Raw data (/proc/16775/stat): 16775 (minisat+_script) S 16774 16775 21452 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855876225 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16775/statm): 531 226 485 147 0 384 0
[pid=16775] vsize: 2124
Raw data (/proc/16779/stat): 16779 (minisat+_64-bit) R 16775 16775 21452 0 -1 0 8848 0 0 0 7933 33 0 0 25 0 1 0 1855876230 31567872 7029 4294967295 134512640 135094434 3221224432 3221221280 134677307 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16779/statm): 7707 7029 145 145 0 7562 0
[pid=16779] vsize: 30828
Current children cumulated CPU time (s) 79.67
Current children cumulated vsize (Kb) 32952

[startup+90.0116 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 16779
Raw data (/proc/16775/stat): 16775 (minisat+_script) S 16774 16775 21452 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855876225 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16775/statm): 531 226 485 147 0 384 0
[pid=16775] vsize: 2124
Raw data (/proc/16779/stat): 16779 (minisat+_64-bit) R 16775 16775 21452 0 -1 0 8937 0 0 0 8933 33 0 0 25 0 1 0 1855876230 31531008 7020 4294967295 134512640 135094434 3221224432 3221222056 134676334 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16779/statm): 7698 7020 145 145 0 7553 0
[pid=16779] vsize: 30792
Current children cumulated CPU time (s) 89.67
Current children cumulated vsize (Kb) 32916

[startup+100.012 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 16779
Raw data (/proc/16775/stat): 16775 (minisat+_script) S 16774 16775 21452 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855876225 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16775/statm): 531 226 485 147 0 384 0
[pid=16775] vsize: 2124
Raw data (/proc/16779/stat): 16779 (minisat+_64-bit) R 16775 16775 21452 0 -1 0 9306 0 0 0 9928 34 0 0 25 0 1 0 1855876230 32768000 7327 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16779/statm): 8000 7327 145 145 0 7855 0
[pid=16779] vsize: 32000
Current children cumulated CPU time (s) 99.63
Current children cumulated vsize (Kb) 34124

[startup+110.013 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 16779
Raw data (/proc/16775/stat): 16775 (minisat+_script) S 16774 16775 21452 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855876225 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16775/statm): 531 226 485 147 0 384 0
[pid=16775] vsize: 2124
Raw data (/proc/16779/stat): 16779 (minisat+_64-bit) R 16775 16775 21452 0 -1 0 9946 0 0 0 10921 38 0 0 25 0 1 0 1855876230 34963456 7861 4294967295 134512640 135094434 3221224432 3221220848 134677059 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16779/statm): 8536 7861 145 145 0 8391 0
[pid=16779] vsize: 34144
Current children cumulated CPU time (s) 109.6
Current children cumulated vsize (Kb) 36268

[startup+120.014 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 16779
Raw data (/proc/16775/stat): 16775 (minisat+_script) S 16774 16775 21452 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855876225 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16775/statm): 531 226 485 147 0 384 0
[pid=16775] vsize: 2124
Raw data (/proc/16779/stat): 16779 (minisat+_64-bit) R 16775 16775 21452 0 -1 0 10031 0 0 0 11921 38 0 0 25 0 1 0 1855876230 34922496 7850 4294967295 134512640 135094434 3221224432 3221221984 134677307 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16779/statm): 8526 7850 145 145 0 8381 0
[pid=16779] vsize: 34104
Current children cumulated CPU time (s) 119.6
Current children cumulated vsize (Kb) 36228

[startup+130.014 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 16779
Raw data (/proc/16775/stat): 16775 (minisat+_script) S 16774 16775 21452 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855876225 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16775/statm): 531 226 485 147 0 384 0
[pid=16775] vsize: 2124
Raw data (/proc/16779/stat): 16779 (minisat+_64-bit) R 16775 16775 21452 0 -1 0 10225 0 0 0 12919 39 0 0 25 0 1 0 1855876230 35434496 7979 4294967295 134512640 135094434 3221224432 3221223024 134557219 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16779/statm): 8651 7979 145 145 0 8506 0
[pid=16779] vsize: 34604
Current children cumulated CPU time (s) 129.59
Current children cumulated vsize (Kb) 36728

[startup+140.015 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 16779
Raw data (/proc/16775/stat): 16775 (minisat+_script) S 16774 16775 21452 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855876225 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16775/statm): 531 226 485 147 0 384 0
[pid=16775] vsize: 2124
Raw data (/proc/16779/stat): 16779 (minisat+_64-bit) R 16775 16775 21452 0 -1 0 10454 0 0 0 13918 39 0 0 25 0 1 0 1855876230 35807232 8070 4294967295 134512640 135094434 3221224432 3221221632 134677307 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16779/statm): 8742 8070 145 145 0 8597 0
[pid=16779] vsize: 34968
Current children cumulated CPU time (s) 139.58
Current children cumulated vsize (Kb) 37092

[startup+150.016 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 16779
Raw data (/proc/16775/stat): 16775 (minisat+_script) S 16774 16775 21452 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855876225 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16775/statm): 531 226 485 147 0 384 0
[pid=16775] vsize: 2124
Raw data (/proc/16779/stat): 16779 (minisat+_64-bit) R 16775 16775 21452 0 -1 0 10660 0 0 0 14917 40 0 0 25 0 1 0 1855876230 36241408 8146 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16779/statm): 8848 8146 145 145 0 8703 0
[pid=16779] vsize: 35392
Current children cumulated CPU time (s) 149.58
Current children cumulated vsize (Kb) 37516

[startup+160.017 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 16779
Raw data (/proc/16775/stat): 16775 (minisat+_script) S 16774 16775 21452 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855876225 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16775/statm): 531 226 485 147 0 384 0
[pid=16775] vsize: 2124
Raw data (/proc/16779/stat): 16779 (minisat+_64-bit) R 16775 16775 21452 0 -1 0 10967 0 0 0 15914 42 0 0 25 0 1 0 1855876230 37056512 8347 4294967295 134512640 135094434 3221224432 3221221280 134677271 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16779/statm): 9047 8347 145 145 0 8902 0
[pid=16779] vsize: 36188
Current children cumulated CPU time (s) 159.57
Current children cumulated vsize (Kb) 38312

[startup+170.017 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 16779
Raw data (/proc/16775/stat): 16775 (minisat+_script) S 16774 16775 21452 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855876225 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16775/statm): 531 226 485 147 0 384 0
[pid=16775] vsize: 2124
Raw data (/proc/16779/stat): 16779 (minisat+_64-bit) R 16775 16775 21452 0 -1 0 11125 0 0 0 16913 42 0 0 25 0 1 0 1855876230 37203968 8380 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16779/statm): 9083 8380 145 145 0 8938 0
[pid=16779] vsize: 36332
Current children cumulated CPU time (s) 169.56
Current children cumulated vsize (Kb) 38456

[startup+180.018 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 16779
Raw data (/proc/16775/stat): 16775 (minisat+_script) S 16774 16775 21452 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855876225 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16775/statm): 531 226 485 147 0 384 0
[pid=16775] vsize: 2124
Raw data (/proc/16779/stat): 16779 (minisat+_64-bit) R 16775 16775 21452 0 -1 0 11423 0 0 0 17908 45 0 0 25 0 1 0 1855876230 38379520 8678 4294967295 134512640 135094434 3221224432 3221223024 134557419 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16779/statm): 9370 8678 145 145 0 9225 0
[pid=16779] vsize: 37480
Current children cumulated CPU time (s) 179.54
Current children cumulated vsize (Kb) 39604

[startup+190.019 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 16779
Raw data (/proc/16775/stat): 16775 (minisat+_script) S 16774 16775 21452 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855876225 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16775/statm): 531 226 485 147 0 384 0
[pid=16775] vsize: 2124
Raw data (/proc/16779/stat): 16779 (minisat+_64-bit) R 16775 16775 21452 0 -1 0 12223 0 0 0 18895 50 0 0 25 0 1 0 1855876230 41644032 9478 4294967295 134512640 135094434 3221224432 3221223088 134557860 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16779/statm): 10167 9478 145 145 0 10022 0
[pid=16779] vsize: 40668
Current children cumulated CPU time (s) 189.46
Current children cumulated vsize (Kb) 42792

[startup+200.018 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 16779
Raw data (/proc/16775/stat): 16775 (minisat+_script) S 16774 16775 21452 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855876225 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16775/statm): 531 226 485 147 0 384 0
[pid=16775] vsize: 2124
Raw data (/proc/16779/stat): 16779 (minisat+_64-bit) R 16775 16775 21452 0 -1 0 13036 0 0 0 19884 54 0 0 25 0 1 0 1855876230 44965888 10291 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16779/statm): 10978 10291 145 145 0 10833 0
[pid=16779] vsize: 43912
Current children cumulated CPU time (s) 199.39
Current children cumulated vsize (Kb) 46036

[startup+210.019 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 16779
Raw data (/proc/16775/stat): 16775 (minisat+_script) S 16774 16775 21452 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855876225 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16775/statm): 531 226 485 147 0 384 0
[pid=16775] vsize: 2124
Raw data (/proc/16779/stat): 16779 (minisat+_64-bit) R 16775 16775 21452 0 -1 0 13361 0 0 0 20879 58 0 0 25 0 1 0 1855876230 46272512 10616 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16779/statm): 11297 10616 145 145 0 11152 0
[pid=16779] vsize: 45188
Current children cumulated CPU time (s) 209.38
Current children cumulated vsize (Kb) 47312

[startup+220.02 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 16779
Raw data (/proc/16775/stat): 16775 (minisat+_script) S 16774 16775 21452 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855876225 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16775/statm): 531 226 485 147 0 384 0
[pid=16775] vsize: 2124
Raw data (/proc/16779/stat): 16779 (minisat+_64-bit) R 16775 16775 21452 0 -1 0 13658 0 0 0 21876 59 0 0 25 0 1 0 1855876230 47050752 10807 4294967295 134512640 135094434 3221224432 3221221440 134600241 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16779/statm): 11487 10807 145 145 0 11342 0
[pid=16779] vsize: 45948
Current children cumulated CPU time (s) 219.36
Current children cumulated vsize (Kb) 48072

[startup+230.021 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 16779
Raw data (/proc/16775/stat): 16775 (minisat+_script) S 16774 16775 21452 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855876225 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16775/statm): 531 226 485 147 0 384 0
[pid=16775] vsize: 2124
Raw data (/proc/16779/stat): 16779 (minisat+_64-bit) R 16775 16775 21452 0 -1 0 13858 0 0 0 22875 60 0 0 25 0 1 0 1855876230 47050752 10808 4294967295 134512640 135094434 3221224432 3221222912 134562841 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16779/statm): 11487 10808 145 145 0 11342 0
[pid=16779] vsize: 45948
Current children cumulated CPU time (s) 229.36
Current children cumulated vsize (Kb) 48072

[startup+240.021 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 16779
Raw data (/proc/16775/stat): 16775 (minisat+_script) S 16774 16775 21452 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855876225 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16775/statm): 531 226 485 147 0 384 0
[pid=16775] vsize: 2124
Raw data (/proc/16779/stat): 16779 (minisat+_64-bit) R 16775 16775 21452 0 -1 0 13858 0 0 0 23875 60 0 0 25 0 1 0 1855876230 47050752 10808 4294967295 134512640 135094434 3221224432 3221223056 134562057 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16779/statm): 11487 10808 145 145 0 11342 0
[pid=16779] vsize: 45948
Current children cumulated CPU time (s) 239.36
Current children cumulated vsize (Kb) 48072

[startup+250.022 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 16779
Raw data (/proc/16775/stat): 16775 (minisat+_script) S 16774 16775 21452 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855876225 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16775/statm): 531 226 485 147 0 384 0
[pid=16775] vsize: 2124
Raw data (/proc/16779/stat): 16779 (minisat+_64-bit) R 16775 16775 21452 0 -1 0 13858 0 0 0 24876 60 0 0 25 0 1 0 1855876230 47050752 10808 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16779/statm): 11487 10808 145 145 0 11342 0
[pid=16779] vsize: 45948
Current children cumulated CPU time (s) 249.37
Current children cumulated vsize (Kb) 48072

[startup+260.023 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 16779
Raw data (/proc/16775/stat): 16775 (minisat+_script) S 16774 16775 21452 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855876225 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16775/statm): 531 226 485 147 0 384 0
[pid=16775] vsize: 2124
Raw data (/proc/16779/stat): 16779 (minisat+_64-bit) R 16775 16775 21452 0 -1 0 13858 0 0 0 25876 60 0 0 25 0 1 0 1855876230 47050752 10808 4294967295 134512640 135094434 3221224432 3221223024 134557413 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16779/statm): 11487 10808 145 145 0 11342 0
[pid=16779] vsize: 45948
Current children cumulated CPU time (s) 259.37
Current children cumulated vsize (Kb) 48072

[startup+270.024 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 16779
Raw data (/proc/16775/stat): 16775 (minisat+_script) S 16774 16775 21452 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855876225 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16775/statm): 531 226 485 147 0 384 0
[pid=16775] vsize: 2124
Raw data (/proc/16779/stat): 16779 (minisat+_64-bit) R 16775 16775 21452 0 -1 0 13858 0 0 0 26876 60 0 0 25 0 1 0 1855876230 47050752 10808 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16779/statm): 11487 10808 145 145 0 11342 0
[pid=16779] vsize: 45948
Current children cumulated CPU time (s) 269.37
Current children cumulated vsize (Kb) 48072

[startup+280.024 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 16779
Raw data (/proc/16775/stat): 16775 (minisat+_script) S 16774 16775 21452 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855876225 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16775/statm): 531 226 485 147 0 384 0
[pid=16775] vsize: 2124
Raw data (/proc/16779/stat): 16779 (minisat+_64-bit) R 16775 16775 21452 0 -1 0 13858 0 0 0 27876 60 0 0 25 0 1 0 1855876230 47050752 10808 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16779/statm): 11487 10808 145 145 0 11342 0
[pid=16779] vsize: 45948
Current children cumulated CPU time (s) 279.37
Current children cumulated vsize (Kb) 48072

[startup+290.025 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 16779
Raw data (/proc/16775/stat): 16775 (minisat+_script) S 16774 16775 21452 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855876225 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16775/statm): 531 226 485 147 0 384 0
[pid=16775] vsize: 2124
Raw data (/proc/16779/stat): 16779 (minisat+_64-bit) R 16775 16775 21452 0 -1 0 14068 0 0 0 28875 61 0 0 25 0 1 0 1855876230 47443968 10903 4294967295 134512640 135094434 3221224432 3221220752 134676471 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16779/statm): 11583 10903 145 145 0 11438 0
[pid=16779] vsize: 46332
Current children cumulated CPU time (s) 289.37
Current children cumulated vsize (Kb) 48456

[startup+300.026 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 16779
Raw data (/proc/16775/stat): 16775 (minisat+_script) S 16774 16775 21452 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855876225 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16775/statm): 531 226 485 147 0 384 0
[pid=16775] vsize: 2124
Raw data (/proc/16779/stat): 16779 (minisat+_64-bit) T 16775 16775 21452 0 -1 0 14198 0 0 0 29874 61 0 0 25 0 1 0 1855876230 47484928 10911 4294967295 134512640 135094434 3221224432 3221221196 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/16779/statm): 11593 10911 145 145 0 11448 0
[pid=16779] vsize: 46372
Current children cumulated CPU time (s) 299.36
Current children cumulated vsize (Kb) 48496

[startup+310.026 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 16779
Raw data (/proc/16775/stat): 16775 (minisat+_script) S 16774 16775 21452 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855876225 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16775/statm): 531 226 485 147 0 384 0
[pid=16775] vsize: 2124
Raw data (/proc/16779/stat): 16779 (minisat+_64-bit) R 16775 16775 21452 0 -1 0 14257 0 0 0 30873 61 0 0 25 0 1 0 1855876230 47587328 10937 4294967295 134512640 135094434 3221224432 3221223120 134554728 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16779/statm): 11618 10937 145 145 0 11473 0
[pid=16779] vsize: 46472
Current children cumulated CPU time (s) 309.35
Current children cumulated vsize (Kb) 48596

[startup+320.027 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 16779
Raw data (/proc/16775/stat): 16775 (minisat+_script) S 16774 16775 21452 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855876225 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16775/statm): 531 226 485 147 0 384 0
[pid=16775] vsize: 2124
Raw data (/proc/16779/stat): 16779 (minisat+_64-bit) R 16775 16775 21452 0 -1 0 14257 0 0 0 31874 61 0 0 25 0 1 0 1855876230 47587328 10937 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16779/statm): 11618 10937 145 145 0 11473 0
[pid=16779] vsize: 46472
Current children cumulated CPU time (s) 319.36
Current children cumulated vsize (Kb) 48596

[startup+330.029 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 16779
Raw data (/proc/16775/stat): 16775 (minisat+_script) S 16774 16775 21452 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855876225 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16775/statm): 531 226 485 147 0 384 0
[pid=16775] vsize: 2124
Raw data (/proc/16779/stat): 16779 (minisat+_64-bit) R 16775 16775 21452 0 -1 0 14257 0 0 0 32874 61 0 0 25 0 1 0 1855876230 47587328 10937 4294967295 134512640 135094434 3221224432 3221223024 134557004 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16779/statm): 11618 10937 145 145 0 11473 0
[pid=16779] vsize: 46472
Current children cumulated CPU time (s) 329.36
Current children cumulated vsize (Kb) 48596

[startup+340.029 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 16779
Raw data (/proc/16775/stat): 16775 (minisat+_script) S 16774 16775 21452 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855876225 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16775/statm): 531 226 485 147 0 384 0
[pid=16775] vsize: 2124
Raw data (/proc/16779/stat): 16779 (minisat+_64-bit) R 16775 16775 21452 0 -1 0 14257 0 0 0 33874 61 0 0 25 0 1 0 1855876230 47587328 10937 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16779/statm): 11618 10937 145 145 0 11473 0
[pid=16779] vsize: 46472
Current children cumulated CPU time (s) 339.36
Current children cumulated vsize (Kb) 48596

[startup+350.03 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 16779
Raw data (/proc/16775/stat): 16775 (minisat+_script) S 16774 16775 21452 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855876225 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16775/statm): 531 226 485 147 0 384 0
[pid=16775] vsize: 2124
Raw data (/proc/16779/stat): 16779 (minisat+_64-bit) R 16775 16775 21452 0 -1 0 14257 0 0 0 34875 61 0 0 25 0 1 0 1855876230 47587328 10937 4294967295 134512640 135094434 3221224432 3221223088 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16779/statm): 11618 10937 145 145 0 11473 0
[pid=16779] vsize: 46472
Current children cumulated CPU time (s) 349.37
Current children cumulated vsize (Kb) 48596

[startup+360.032 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 16779
Raw data (/proc/16775/stat): 16775 (minisat+_script) S 16774 16775 21452 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855876225 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16775/statm): 531 226 485 147 0 384 0
[pid=16775] vsize: 2124
Raw data (/proc/16779/stat): 16779 (minisat+_64-bit) R 16775 16775 21452 0 -1 0 14448 0 0 0 35871 64 0 0 25 0 1 0 1855876230 48353280 11128 4294967295 134512640 135094434 3221224432 3221223044 134563134 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16779/statm): 11805 11128 145 145 0 11660 0
[pid=16779] vsize: 47220
Current children cumulated CPU time (s) 359.36
Current children cumulated vsize (Kb) 49344

[startup+370.033 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 16779
Raw data (/proc/16775/stat): 16775 (minisat+_script) S 16774 16775 21452 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855876225 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16775/statm): 531 226 485 147 0 384 0
[pid=16775] vsize: 2124
Raw data (/proc/16779/stat): 16779 (minisat+_64-bit) R 16775 16775 21452 0 -1 0 15029 0 0 0 36861 68 0 0 25 0 1 0 1855876230 50733056 11709 4294967295 134512640 135094434 3221224432 3221223024 134557537 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16779/statm): 12386 11709 145 145 0 12241 0
[pid=16779] vsize: 49544
Current children cumulated CPU time (s) 369.3
Current children cumulated vsize (Kb) 51668

[startup+380.033 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 16779
Raw data (/proc/16775/stat): 16775 (minisat+_script) S 16774 16775 21452 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855876225 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16775/statm): 531 226 485 147 0 384 0
[pid=16775] vsize: 2124
Raw data (/proc/16779/stat): 16779 (minisat+_64-bit) R 16775 16775 21452 0 -1 0 15535 0 0 0 37852 72 0 0 25 0 1 0 1855876230 52793344 12215 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16779/statm): 12889 12215 145 145 0 12744 0
[pid=16779] vsize: 51556
Current children cumulated CPU time (s) 379.25
Current children cumulated vsize (Kb) 53680

[startup+390.034 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 16779
Raw data (/proc/16775/stat): 16775 (minisat+_script) S 16774 16775 21452 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855876225 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16775/statm): 531 226 485 147 0 384 0
[pid=16775] vsize: 2124
Raw data (/proc/16779/stat): 16779 (minisat+_64-bit) R 16775 16775 21452 0 -1 0 16335 0 0 0 38842 76 0 0 25 0 1 0 1855876230 56057856 13015 4294967295 134512640 135094434 3221224432 3221223104 134556317 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16779/statm): 13686 13015 145 145 0 13541 0
[pid=16779] vsize: 54744
Current children cumulated CPU time (s) 389.19
Current children cumulated vsize (Kb) 56868

[startup+400.035 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 16779
Raw data (/proc/16775/stat): 16775 (minisat+_script) S 16774 16775 21452 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855876225 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16775/statm): 531 226 485 147 0 384 0
[pid=16775] vsize: 2124
Raw data (/proc/16779/stat): 16779 (minisat+_64-bit) R 16775 16775 21452 0 -1 0 17122 0 0 0 39829 82 0 0 25 0 1 0 1855876230 59273216 13802 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16779/statm): 14471 13802 145 145 0 14326 0
[pid=16779] vsize: 57884
Current children cumulated CPU time (s) 399.12
Current children cumulated vsize (Kb) 60008

[startup+410.036 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 16779
Raw data (/proc/16775/stat): 16775 (minisat+_script) S 16774 16775 21452 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855876225 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16775/statm): 531 226 485 147 0 384 0
[pid=16775] vsize: 2124
Raw data (/proc/16779/stat): 16779 (minisat+_64-bit) R 16775 16775 21452 0 -1 0 17865 0 0 0 40819 86 0 0 25 0 1 0 1855876230 62308352 14545 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16779/statm): 15212 14545 145 145 0 15067 0
[pid=16779] vsize: 60848
Current children cumulated CPU time (s) 409.06
Current children cumulated vsize (Kb) 62972

[startup+420.036 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 16779
Raw data (/proc/16775/stat): 16775 (minisat+_script) S 16774 16775 21452 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855876225 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16775/statm): 531 226 485 147 0 384 0
[pid=16775] vsize: 2124
Raw data (/proc/16779/stat): 16779 (minisat+_64-bit) R 16775 16775 21452 0 -1 0 18611 0 0 0 41808 91 0 0 25 0 1 0 1855876230 65617920 15291 4294967295 134512640 135094434 3221224432 3221223024 134557202 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16779/statm): 16020 15291 145 145 0 15875 0
[pid=16779] vsize: 64080
Current children cumulated CPU time (s) 419
Current children cumulated vsize (Kb) 66204

[startup+430.038 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 16779
Raw data (/proc/16775/stat): 16775 (minisat+_script) S 16774 16775 21452 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855876225 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16775/statm): 531 226 485 147 0 384 0
[pid=16775] vsize: 2124
Raw data (/proc/16779/stat): 16779 (minisat+_64-bit) R 16775 16775 21452 0 -1 0 19333 0 0 0 42799 96 0 0 25 0 1 0 1855876230 68567040 16013 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16779/statm): 16740 16013 145 145 0 16595 0
[pid=16779] vsize: 66960
Current children cumulated CPU time (s) 428.96
Current children cumulated vsize (Kb) 69084

[startup+440.039 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 16779
Raw data (/proc/16775/stat): 16775 (minisat+_script) S 16774 16775 21452 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855876225 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16775/statm): 531 226 485 147 0 384 0
[pid=16775] vsize: 2124
Raw data (/proc/16779/stat): 16779 (minisat+_64-bit) R 16775 16775 21452 0 -1 0 19993 0 0 0 43789 100 0 0 25 0 1 0 1855876230 71262208 16673 4294967295 134512640 135094434 3221224432 3221223088 134557996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16779/statm): 17398 16673 145 145 0 17253 0
[pid=16779] vsize: 69592
Current children cumulated CPU time (s) 438.9
Current children cumulated vsize (Kb) 71716

[startup+450.039 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 16779
Raw data (/proc/16775/stat): 16775 (minisat+_script) S 16774 16775 21452 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855876225 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16775/statm): 531 226 485 147 0 384 0
[pid=16775] vsize: 2124
Raw data (/proc/16779/stat): 16779 (minisat+_64-bit) R 16775 16775 21452 0 -1 0 20642 0 0 0 44779 104 0 0 25 0 1 0 1855876230 73912320 17322 4294967295 134512640 135094434 3221224432 3221223024 134557219 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16779/statm): 18045 17322 145 145 0 17900 0
[pid=16779] vsize: 72180
Current children cumulated CPU time (s) 448.84
Current children cumulated vsize (Kb) 74304

[startup+460.04 s]
Raw data (loadavg): 0.99 0.98 0.91 1/57 16779
Raw data (/proc/16775/stat): 16775 (minisat+_script) S 16774 16775 21452 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855876225 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16775/statm): 531 226 485 147 0 384 0
[pid=16775] vsize: 2124
Raw data (/proc/16779/stat): 16779 (minisat+_64-bit) T 16775 16775 21452 0 -1 0 21284 0 0 0 45771 107 0 0 25 0 1 0 1855876230 76533760 17964 4294967295 134512640 135094434 3221224432 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/16779/statm): 18685 17964 145 145 0 18540 0
[pid=16779] vsize: 74740
Current children cumulated CPU time (s) 458.79
Current children cumulated vsize (Kb) 76864

[startup+470.041 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 16779
Raw data (/proc/16775/stat): 16775 (minisat+_script) S 16774 16775 21452 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855876225 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16775/statm): 531 226 485 147 0 384 0
[pid=16775] vsize: 2124
Raw data (/proc/16779/stat): 16779 (minisat+_64-bit) R 16775 16775 21452 0 -1 0 21913 0 0 0 46762 112 0 0 25 0 1 0 1855876230 79101952 18593 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16779/statm): 19312 18593 145 145 0 19167 0
[pid=16779] vsize: 77248
Current children cumulated CPU time (s) 468.75
Current children cumulated vsize (Kb) 79372

[startup+480.043 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 16779
Raw data (/proc/16775/stat): 16775 (minisat+_script) S 16774 16775 21452 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855876225 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16775/statm): 531 226 485 147 0 384 0
[pid=16775] vsize: 2124
Raw data (/proc/16779/stat): 16779 (minisat+_64-bit) R 16775 16775 21452 0 -1 0 22406 0 0 0 47752 116 0 0 25 0 1 0 1855876230 81096704 19086 4294967295 134512640 135094434 3221224432 3221223104 134555983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16779/statm): 19799 19086 145 145 0 19654 0
[pid=16779] vsize: 79196
Current children cumulated CPU time (s) 478.69
Current children cumulated vsize (Kb) 81320

[startup+490.043 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 16779
Raw data (/proc/16775/stat): 16775 (minisat+_script) S 16774 16775 21452 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855876225 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16775/statm): 531 226 485 147 0 384 0
[pid=16775] vsize: 2124
Raw data (/proc/16779/stat): 16779 (minisat+_64-bit) R 16775 16775 21452 0 -1 0 22768 0 0 0 48746 119 0 0 25 0 1 0 1855876230 82558976 19448 4294967295 134512640 135094434 3221224432 3221223088 134557950 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16779/statm): 20156 19448 145 145 0 20011 0
[pid=16779] vsize: 80624
Current children cumulated CPU time (s) 488.66
Current children cumulated vsize (Kb) 82748

[startup+500.044 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 16779
Raw data (/proc/16775/stat): 16775 (minisat+_script) S 16774 16775 21452 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855876225 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16775/statm): 531 226 485 147 0 384 0
[pid=16775] vsize: 2124
Raw data (/proc/16779/stat): 16779 (minisat+_64-bit) R 16775 16775 21452 0 -1 0 23080 0 0 0 49740 122 0 0 25 0 1 0 1855876230 83824640 19760 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16779/statm): 20465 19760 145 145 0 20320 0
[pid=16779] vsize: 81860
Current children cumulated CPU time (s) 498.63
Current children cumulated vsize (Kb) 83984

[startup+510.045 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 16779
Raw data (/proc/16775/stat): 16775 (minisat+_script) S 16774 16775 21452 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855876225 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16775/statm): 531 226 485 147 0 384 0
[pid=16775] vsize: 2124
Raw data (/proc/16779/stat): 16779 (minisat+_64-bit) R 16775 16775 21452 0 -1 0 23524 0 0 0 50731 126 0 0 25 0 1 0 1855876230 85630976 20204 4294967295 134512640 135094434 3221224432 3221223024 134557236 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16779/statm): 20906 20204 145 145 0 20761 0
[pid=16779] vsize: 83624
Current children cumulated CPU time (s) 508.58
Current children cumulated vsize (Kb) 85748

[startup+520.045 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 16779
Raw data (/proc/16775/stat): 16775 (minisat+_script) S 16774 16775 21452 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855876225 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16775/statm): 531 226 485 147 0 384 0
[pid=16775] vsize: 2124
Raw data (/proc/16779/stat): 16779 (minisat+_64-bit) R 16775 16775 21452 0 -1 0 24167 0 0 0 51721 130 0 0 25 0 1 0 1855876230 88252416 20847 4294967295 134512640 135094434 3221224432 3221223088 134558007 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16779/statm): 21546 20847 145 145 0 21401 0
[pid=16779] vsize: 86184
Current children cumulated CPU time (s) 518.52
Current children cumulated vsize (Kb) 88308

[startup+530.046 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 16779
Raw data (/proc/16775/stat): 16775 (minisat+_script) S 16774 16775 21452 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855876225 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16775/statm): 531 226 485 147 0 384 0
[pid=16775] vsize: 2124
Raw data (/proc/16779/stat): 16779 (minisat+_64-bit) R 16775 16775 21452 0 -1 0 24758 0 0 0 52712 134 0 0 25 0 1 0 1855876230 90660864 21438 4294967295 134512640 135094434 3221224432 3221223088 134558126 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16779/statm): 22134 21438 145 145 0 21989 0
[pid=16779] vsize: 88536
Current children cumulated CPU time (s) 528.47
Current children cumulated vsize (Kb) 90660

[startup+540.048 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 16779
Raw data (/proc/16775/stat): 16775 (minisat+_script) S 16774 16775 21452 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855876225 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16775/statm): 531 226 485 147 0 384 0
[pid=16775] vsize: 2124
Raw data (/proc/16779/stat): 16779 (minisat+_64-bit) R 16775 16775 21452 0 -1 0 25445 0 0 0 53700 139 0 0 25 0 1 0 1855876230 93462528 22125 4294967295 134512640 135094434 3221224432 3221223024 134556904 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16779/statm): 22818 22125 145 145 0 22673 0
[pid=16779] vsize: 91272
Current children cumulated CPU time (s) 538.4
Current children cumulated vsize (Kb) 93396

[startup+550.048 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 16779
Raw data (/proc/16775/stat): 16775 (minisat+_script) S 16774 16775 21452 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855876225 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16775/statm): 531 226 485 147 0 384 0
[pid=16775] vsize: 2124
Raw data (/proc/16779/stat): 16779 (minisat+_64-bit) R 16775 16775 21452 0 -1 0 25894 0 0 0 54691 143 0 0 25 0 1 0 1855876230 95281152 22574 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16779/statm): 23262 22574 145 145 0 23117 0
[pid=16779] vsize: 93048
Current children cumulated CPU time (s) 548.35
Current children cumulated vsize (Kb) 95172

[startup+560.049 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 16779
Raw data (/proc/16775/stat): 16775 (minisat+_script) S 16774 16775 21452 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855876225 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16775/statm): 531 226 485 147 0 384 0
[pid=16775] vsize: 2124
Raw data (/proc/16779/stat): 16779 (minisat+_64-bit) R 16775 16775 21452 0 -1 0 26539 0 0 0 55682 146 0 0 25 0 1 0 1855876230 97910784 23219 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16779/statm): 23904 23219 145 145 0 23759 0
[pid=16779] vsize: 95616
Current children cumulated CPU time (s) 558.29
Current children cumulated vsize (Kb) 97740

[startup+570.05 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 16779
Raw data (/proc/16775/stat): 16775 (minisat+_script) S 16774 16775 21452 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855876225 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16775/statm): 531 226 485 147 0 384 0
[pid=16775] vsize: 2124
Raw data (/proc/16779/stat): 16779 (minisat+_64-bit) R 16775 16775 21452 0 -1 0 27163 0 0 0 56671 151 0 0 25 0 1 0 1855876230 100433920 23843 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16779/statm): 24520 23843 145 145 0 24375 0
[pid=16779] vsize: 98080
Current children cumulated CPU time (s) 568.23
Current children cumulated vsize (Kb) 100204

[startup+580.051 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 16779
Raw data (/proc/16775/stat): 16775 (minisat+_script) S 16774 16775 21452 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855876225 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16775/statm): 531 226 485 147 0 384 0
[pid=16775] vsize: 2124
Raw data (/proc/16779/stat): 16779 (minisat+_64-bit) R 16775 16775 21452 0 -1 0 27723 0 0 0 57661 155 0 0 25 0 1 0 1855876230 102707200 24403 4294967295 134512640 135094434 3221224432 3221223024 134557219 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16779/statm): 25075 24403 145 145 0 24930 0
[pid=16779] vsize: 100300
Current children cumulated CPU time (s) 578.17
Current children cumulated vsize (Kb) 102424

[startup+590.051 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 16779
Raw data (/proc/16775/stat): 16775 (minisat+_script) S 16774 16775 21452 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855876225 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16775/statm): 531 226 485 147 0 384 0
[pid=16775] vsize: 2124
Raw data (/proc/16779/stat): 16779 (minisat+_64-bit) R 16775 16775 21452 0 -1 0 28360 0 0 0 58652 159 0 0 25 0 1 0 1855876230 105828352 25040 4294967295 134512640 135094434 3221224432 3221223024 134557273 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16779/statm): 25837 25040 145 145 0 25692 0
[pid=16779] vsize: 103348
Current children cumulated CPU time (s) 588.12
Current children cumulated vsize (Kb) 105472

[startup+600.052 s]
Raw data (loadavg): 1.07 1.00 0.92 2/57 16779
Raw data (/proc/16775/stat): 16775 (minisat+_script) S 16774 16775 21452 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855876225 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16775/statm): 531 226 485 147 0 384 0
[pid=16775] vsize: 2124
Raw data (/proc/16779/stat): 16779 (minisat+_64-bit) R 16775 16775 21452 0 -1 0 29081 0 0 0 59640 164 0 0 25 0 1 0 1855876230 108773376 25761 4294967295 134512640 135094434 3221224432 3221223024 134556978 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16779/statm): 26556 25761 145 145 0 26411 0
[pid=16779] vsize: 106224
Current children cumulated CPU time (s) 598.05
Current children cumulated vsize (Kb) 108348

[startup+610.054 s]
Raw data (loadavg): 1.06 1.00 0.92 2/57 16779
Raw data (/proc/16775/stat): 16775 (minisat+_script) S 16774 16775 21452 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855876225 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16775/statm): 531 226 485 147 0 384 0
[pid=16775] vsize: 2124
Raw data (/proc/16779/stat): 16779 (minisat+_64-bit) R 16775 16775 21452 0 -1 0 29743 0 0 0 60630 167 0 0 25 0 1 0 1855876230 111484928 26423 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16779/statm): 27218 26423 145 145 0 27073 0
[pid=16779] vsize: 108872
Current children cumulated CPU time (s) 607.98
Current children cumulated vsize (Kb) 110996

[startup+620.054 s]
Raw data (loadavg): 1.05 1.00 0.92 2/57 16779
Raw data (/proc/16775/stat): 16775 (minisat+_script) S 16774 16775 21452 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855876225 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16775/statm): 531 226 485 147 0 384 0
[pid=16775] vsize: 2124
Raw data (/proc/16779/stat): 16779 (minisat+_64-bit) R 16775 16775 21452 0 -1 0 30233 0 0 0 61622 171 0 0 25 0 1 0 1855876230 113487872 26913 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16779/statm): 27707 26913 145 145 0 27562 0
[pid=16779] vsize: 110828
Current children cumulated CPU time (s) 617.94
Current children cumulated vsize (Kb) 112952

[startup+630.056 s]
Raw data (loadavg): 1.04 1.00 0.92 2/57 16779
Raw data (/proc/16775/stat): 16775 (minisat+_script) S 16774 16775 21452 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855876225 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16775/statm): 531 226 485 147 0 384 0
[pid=16775] vsize: 2124
Raw data (/proc/16779/stat): 16779 (minisat+_64-bit) R 16775 16775 21452 0 -1 0 30680 0 0 0 62615 174 0 0 25 0 1 0 1855876230 115318784 27360 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16779/statm): 28154 27360 145 145 0 28009 0
[pid=16779] vsize: 112616
Current children cumulated CPU time (s) 627.9
Current children cumulated vsize (Kb) 114740

[startup+640.058 s]
Raw data (loadavg): 1.03 1.00 0.92 2/57 16779
Raw data (/proc/16775/stat): 16775 (minisat+_script) S 16774 16775 21452 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855876225 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16775/statm): 531 226 485 147 0 384 0
[pid=16775] vsize: 2124
Raw data (/proc/16779/stat): 16779 (minisat+_64-bit) R 16775 16775 21452 0 -1 0 31256 0 0 0 63604 179 0 0 25 0 1 0 1855876230 117665792 27936 4294967295 134512640 135094434 3221224432 3221223024 134557227 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16779/statm): 28727 27936 145 145 0 28582 0
[pid=16779] vsize: 114908
Current children cumulated CPU time (s) 637.84
Current children cumulated vsize (Kb) 117032

[startup+650.059 s]
Raw data (loadavg): 1.03 1.00 0.92 2/57 16779
Raw data (/proc/16775/stat): 16775 (minisat+_script) S 16774 16775 21452 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855876225 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16775/statm): 531 226 485 147 0 384 0
[pid=16775] vsize: 2124
Raw data (/proc/16779/stat): 16779 (minisat+_64-bit) R 16775 16775 21452 0 -1 0 31592 0 0 0 64598 182 0 0 25 0 1 0 1855876230 119025664 28272 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16779/statm): 29059 28272 145 145 0 28914 0
[pid=16779] vsize: 116236
Current children cumulated CPU time (s) 647.81
Current children cumulated vsize (Kb) 118360

[startup+660.06 s]
Raw data (loadavg): 1.02 1.00 0.92 2/57 16779
Raw data (/proc/16775/stat): 16775 (minisat+_script) S 16774 16775 21452 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855876225 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16775/statm): 531 226 485 147 0 384 0
[pid=16775] vsize: 2124
Raw data (/proc/16779/stat): 16779 (minisat+_64-bit) R 16775 16775 21452 0 -1 0 31964 0 0 0 65592 184 0 0 25 0 1 0 1855876230 120545280 28644 4294967295 134512640 135094434 3221224432 3221223088 134557964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16779/statm): 29430 28644 145 145 0 29285 0
[pid=16779] vsize: 117720
Current children cumulated CPU time (s) 657.77
Current children cumulated vsize (Kb) 119844

[startup+670.061 s]
Raw data (loadavg): 1.02 1.00 0.92 2/57 16779
Raw data (/proc/16775/stat): 16775 (minisat+_script) S 16774 16775 21452 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855876225 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16775/statm): 531 226 485 147 0 384 0
[pid=16775] vsize: 2124
Raw data (/proc/16779/stat): 16779 (minisat+_64-bit) R 16775 16775 21452 0 -1 0 32417 0 0 0 66584 188 0 0 25 0 1 0 1855876230 122392576 29097 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16779/statm): 29881 29097 145 145 0 29736 0
[pid=16779] vsize: 119524
Current children cumulated CPU time (s) 667.73
Current children cumulated vsize (Kb) 121648

[startup+680.062 s]
Raw data (loadavg): 1.02 1.00 0.92 2/57 16779
Raw data (/proc/16775/stat): 16775 (minisat+_script) S 16774 16775 21452 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855876225 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16775/statm): 531 226 485 147 0 384 0
[pid=16775] vsize: 2124
Raw data (/proc/16779/stat): 16779 (minisat+_64-bit) R 16775 16775 21452 0 -1 0 32850 0 0 0 67576 192 0 0 25 0 1 0 1855876230 124153856 29530 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16779/statm): 30311 29530 145 145 0 30166 0
[pid=16779] vsize: 121244
Current children cumulated CPU time (s) 677.69
Current children cumulated vsize (Kb) 123368

[startup+690.062 s]
Raw data (loadavg): 1.01 1.00 0.92 2/57 16779
Raw data (/proc/16775/stat): 16775 (minisat+_script) S 16774 16775 21452 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855876225 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16775/statm): 531 226 485 147 0 384 0
[pid=16775] vsize: 2124
Raw data (/proc/16779/stat): 16779 (minisat+_64-bit) R 16775 16775 21452 0 -1 0 33514 0 0 0 68563 197 0 0 25 0 1 0 1855876230 126857216 30194 4294967295 134512640 135094434 3221224432 3221223088 134558002 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16779/statm): 30971 30194 145 145 0 30826 0
[pid=16779] vsize: 123884
Current children cumulated CPU time (s) 687.61
Current children cumulated vsize (Kb) 126008

[startup+700.063 s]
Raw data (loadavg): 1.01 1.00 0.92 2/57 16779
Raw data (/proc/16775/stat): 16775 (minisat+_script) S 16774 16775 21452 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855876225 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16775/statm): 531 226 485 147 0 384 0
[pid=16775] vsize: 2124
Raw data (/proc/16779/stat): 16779 (minisat+_64-bit) R 16775 16775 21452 0 -1 0 34110 0 0 0 69554 201 0 0 25 0 1 0 1855876230 129273856 30790 4294967295 134512640 135094434 3221224432 3221223088 134557945 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16779/statm): 31561 30790 145 145 0 31416 0
[pid=16779] vsize: 126244
Current children cumulated CPU time (s) 697.56
Current children cumulated vsize (Kb) 128368

[startup+710.065 s]
Raw data (loadavg): 1.01 1.00 0.92 2/57 16779
Raw data (/proc/16775/stat): 16775 (minisat+_script) S 16774 16775 21452 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855876225 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16775/statm): 531 226 485 147 0 384 0
[pid=16775] vsize: 2124
Raw data (/proc/16779/stat): 16779 (minisat+_64-bit) R 16775 16775 21452 0 -1 0 34561 0 0 0 70547 204 0 0 25 0 1 0 1855876230 131100672 31241 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16779/statm): 32007 31241 145 145 0 31862 0
[pid=16779] vsize: 128028
Current children cumulated CPU time (s) 707.52
Current children cumulated vsize (Kb) 130152

[startup+720.066 s]
Raw data (loadavg): 1.01 1.00 0.92 2/57 16779
Raw data (/proc/16775/stat): 16775 (minisat+_script) S 16774 16775 21452 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855876225 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16775/statm): 531 226 485 147 0 384 0
[pid=16775] vsize: 2124
Raw data (/proc/16779/stat): 16779 (minisat+_64-bit) R 16775 16775 21452 0 -1 0 34841 0 0 0 71542 205 0 0 25 0 1 0 1855876230 132247552 31521 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16779/statm): 32287 31521 145 145 0 32142 0
[pid=16779] vsize: 129148
Current children cumulated CPU time (s) 717.48
Current children cumulated vsize (Kb) 131272

[startup+730.066 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 16779
Raw data (/proc/16775/stat): 16775 (minisat+_script) S 16774 16775 21452 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855876225 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16775/statm): 531 226 485 147 0 384 0
[pid=16775] vsize: 2124
Raw data (/proc/16779/stat): 16779 (minisat+_64-bit) R 16775 16775 21452 0 -1 0 35238 0 0 0 72534 209 0 0 25 0 1 0 1855876230 133861376 31918 4294967295 134512640 135094434 3221224432 3221223088 134558420 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16779/statm): 32681 31918 145 145 0 32536 0
[pid=16779] vsize: 130724
Current children cumulated CPU time (s) 727.44
Current children cumulated vsize (Kb) 132848

[startup+740.067 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 16779
Raw data (/proc/16775/stat): 16775 (minisat+_script) S 16774 16775 21452 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855876225 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16775/statm): 531 226 485 147 0 384 0
[pid=16775] vsize: 2124
Raw data (/proc/16779/stat): 16779 (minisat+_64-bit) R 16775 16775 21452 0 -1 0 35686 0 0 0 73526 213 0 0 25 0 1 0 1855876230 135684096 32366 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16779/statm): 33126 32366 145 145 0 32981 0
[pid=16779] vsize: 132504
Current children cumulated CPU time (s) 737.4
Current children cumulated vsize (Kb) 134628

[startup+750.068 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 16779
Raw data (/proc/16775/stat): 16775 (minisat+_script) S 16774 16775 21452 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855876225 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16775/statm): 531 226 485 147 0 384 0
[pid=16775] vsize: 2124
Raw data (/proc/16779/stat): 16779 (minisat+_64-bit) R 16775 16775 21452 0 -1 0 36167 0 0 0 74518 216 0 0 25 0 1 0 1855876230 137646080 32847 4294967295 134512640 135094434 3221224432 3221223056 134557565 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16779/statm): 33605 32847 145 145 0 33460 0
[pid=16779] vsize: 134420
Current children cumulated CPU time (s) 747.35
Current children cumulated vsize (Kb) 136544

[startup+760.069 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 16779
Raw data (/proc/16775/stat): 16775 (minisat+_script) S 16774 16775 21452 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855876225 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16775/statm): 531 226 485 147 0 384 0
[pid=16775] vsize: 2124
Raw data (/proc/16779/stat): 16779 (minisat+_64-bit) R 16775 16775 21452 0 -1 0 36449 0 0 0 75513 219 0 0 25 0 1 0 1855876230 138797056 33129 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16779/statm): 33886 33129 145 145 0 33741 0
[pid=16779] vsize: 135544
Current children cumulated CPU time (s) 757.33
Current children cumulated vsize (Kb) 137668

[startup+770.07 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 16779
Raw data (/proc/16775/stat): 16775 (minisat+_script) S 16774 16775 21452 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855876225 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16775/statm): 531 226 485 147 0 384 0
[pid=16775] vsize: 2124
Raw data (/proc/16779/stat): 16779 (minisat+_64-bit) R 16775 16775 21452 0 -1 0 36449 0 0 0 76513 219 0 0 25 0 1 0 1855876230 138797056 33129 4294967295 134512640 135094434 3221224432 3221223104 134555568 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16779/statm): 33886 33129 145 145 0 33741 0
[pid=16779] vsize: 135544
Current children cumulated CPU time (s) 767.33
Current children cumulated vsize (Kb) 137668

[startup+780.071 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 16779
Raw data (/proc/16775/stat): 16775 (minisat+_script) S 16774 16775 21452 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855876225 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16775/statm): 531 226 485 147 0 384 0
[pid=16775] vsize: 2124
Raw data (/proc/16779/stat): 16779 (minisat+_64-bit) R 16775 16775 21452 0 -1 0 36449 0 0 0 77512 220 0 0 25 0 1 0 1855876230 138797056 33129 4294967295 134512640 135094434 3221224432 3221223088 134558221 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16779/statm): 33886 33129 145 145 0 33741 0
[pid=16779] vsize: 135544
Current children cumulated CPU time (s) 777.33
Current children cumulated vsize (Kb) 137668

[startup+790.072 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 16779
Raw data (/proc/16775/stat): 16775 (minisat+_script) S 16774 16775 21452 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855876225 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16775/statm): 531 226 485 147 0 384 0
[pid=16775] vsize: 2124
Raw data (/proc/16779/stat): 16779 (minisat+_64-bit) R 16775 16775 21452 0 -1 0 36449 0 0 0 78511 221 0 0 25 0 1 0 1855876230 138797056 33129 4294967295 134512640 135094434 3221224432 3221223024 134557230 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16779/statm): 33886 33129 145 145 0 33741 0
[pid=16779] vsize: 135544
Current children cumulated CPU time (s) 787.33
Current children cumulated vsize (Kb) 137668

[startup+800.072 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 16779
Raw data (/proc/16775/stat): 16775 (minisat+_script) S 16774 16775 21452 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855876225 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16775/statm): 531 226 485 147 0 384 0
[pid=16775] vsize: 2124
Raw data (/proc/16779/stat): 16779 (minisat+_64-bit) R 16775 16775 21452 0 -1 0 36449 0 0 0 79511 221 0 0 25 0 1 0 1855876230 138797056 33129 4294967295 134512640 135094434 3221224432 3221223024 134557273 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16779/statm): 33886 33129 145 145 0 33741 0
[pid=16779] vsize: 135544
Current children cumulated CPU time (s) 797.33
Current children cumulated vsize (Kb) 137668

[startup+810.074 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 16779
Raw data (/proc/16775/stat): 16775 (minisat+_script) S 16774 16775 21452 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855876225 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16775/statm): 531 226 485 147 0 384 0
[pid=16775] vsize: 2124
Raw data (/proc/16779/stat): 16779 (minisat+_64-bit) R 16775 16775 21452 0 -1 0 36449 0 0 0 80510 222 0 0 25 0 1 0 1855876230 138797056 33129 4294967295 134512640 135094434 3221224432 3221223024 134557042 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16779/statm): 33886 33129 145 145 0 33741 0
[pid=16779] vsize: 135544
Current children cumulated CPU time (s) 807.33
Current children cumulated vsize (Kb) 137668

[startup+820.076 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 16779
Raw data (/proc/16775/stat): 16775 (minisat+_script) S 16774 16775 21452 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855876225 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16775/statm): 531 226 485 147 0 384 0
[pid=16775] vsize: 2124
Raw data (/proc/16779/stat): 16779 (minisat+_64-bit) R 16775 16775 21452 0 -1 0 36449 0 0 0 81510 222 0 0 25 0 1 0 1855876230 138797056 33129 4294967295 134512640 135094434 3221224432 3221223024 134556862 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16779/statm): 33886 33129 145 145 0 33741 0
[pid=16779] vsize: 135544
Current children cumulated CPU time (s) 817.33
Current children cumulated vsize (Kb) 137668

[startup+830.076 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 16779
Raw data (/proc/16775/stat): 16775 (minisat+_script) S 16774 16775 21452 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855876225 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16775/statm): 531 226 485 147 0 384 0
[pid=16775] vsize: 2124
Raw data (/proc/16779/stat): 16779 (minisat+_64-bit) R 16775 16775 21452 0 -1 0 36449 0 0 0 82510 222 0 0 25 0 1 0 1855876230 138797056 33129 4294967295 134512640 135094434 3221224432 3221223104 134556317 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16779/statm): 33886 33129 145 145 0 33741 0
[pid=16779] vsize: 135544
Current children cumulated CPU time (s) 827.33
Current children cumulated vsize (Kb) 137668

[startup+840.076 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 16779
Raw data (/proc/16775/stat): 16775 (minisat+_script) S 16774 16775 21452 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855876225 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16775/statm): 531 226 485 147 0 384 0
[pid=16775] vsize: 2124
Raw data (/proc/16779/stat): 16779 (minisat+_64-bit) R 16775 16775 21452 0 -1 0 36449 0 0 0 83511 222 0 0 25 0 1 0 1855876230 138797056 33129 4294967295 134512640 135094434 3221224432 3221223088 134558227 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16779/statm): 33886 33129 145 145 0 33741 0
[pid=16779] vsize: 135544
Current children cumulated CPU time (s) 837.34
Current children cumulated vsize (Kb) 137668

[startup+850.077 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 16779
Raw data (/proc/16775/stat): 16775 (minisat+_script) S 16774 16775 21452 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855876225 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16775/statm): 531 226 485 147 0 384 0
[pid=16775] vsize: 2124
Raw data (/proc/16779/stat): 16779 (minisat+_64-bit) R 16775 16775 21452 0 -1 0 36449 0 0 0 84511 222 0 0 25 0 1 0 1855876230 138797056 33129 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16779/statm): 33886 33129 145 145 0 33741 0
[pid=16779] vsize: 135544
Current children cumulated CPU time (s) 847.34
Current children cumulated vsize (Kb) 137668

[startup+860.078 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 16779
Raw data (/proc/16775/stat): 16775 (minisat+_script) S 16774 16775 21452 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855876225 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16775/statm): 531 226 485 147 0 384 0
[pid=16775] vsize: 2124
Raw data (/proc/16779/stat): 16779 (minisat+_64-bit) R 16775 16775 21452 0 -1 0 36449 0 0 0 85511 222 0 0 25 0 1 0 1855876230 138797056 33129 4294967295 134512640 135094434 3221224432 3221223088 134558004 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16779/statm): 33886 33129 145 145 0 33741 0
[pid=16779] vsize: 135544
Current children cumulated CPU time (s) 857.34
Current children cumulated vsize (Kb) 137668

[startup+870.078 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 16779
Raw data (/proc/16775/stat): 16775 (minisat+_script) S 16774 16775 21452 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855876225 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16775/statm): 531 226 485 147 0 384 0
[pid=16775] vsize: 2124
Raw data (/proc/16779/stat): 16779 (minisat+_64-bit) R 16775 16775 21452 0 -1 0 36449 0 0 0 86511 222 0 0 25 0 1 0 1855876230 138797056 33129 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16779/statm): 33886 33129 145 145 0 33741 0
[pid=16779] vsize: 135544
Current children cumulated CPU time (s) 867.34
Current children cumulated vsize (Kb) 137668

[startup+880.079 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 16779
Raw data (/proc/16775/stat): 16775 (minisat+_script) S 16774 16775 21452 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855876225 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16775/statm): 531 226 485 147 0 384 0
[pid=16775] vsize: 2124
Raw data (/proc/16779/stat): 16779 (minisat+_64-bit) R 16775 16775 21452 0 -1 0 36449 0 0 0 87511 222 0 0 25 0 1 0 1855876230 138797056 33129 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16779/statm): 33886 33129 145 145 0 33741 0
[pid=16779] vsize: 135544
Current children cumulated CPU time (s) 877.34
Current children cumulated vsize (Kb) 137668

[startup+890.08 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 16779
Raw data (/proc/16775/stat): 16775 (minisat+_script) S 16774 16775 21452 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855876225 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16775/statm): 531 226 485 147 0 384 0
[pid=16775] vsize: 2124
Raw data (/proc/16779/stat): 16779 (minisat+_64-bit) R 16775 16775 21452 0 -1 0 36449 0 0 0 88511 222 0 0 25 0 1 0 1855876230 138797056 33129 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16779/statm): 33886 33129 145 145 0 33741 0
[pid=16779] vsize: 135544
Current children cumulated CPU time (s) 887.34
Current children cumulated vsize (Kb) 137668

[startup+900.081 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 16779
Raw data (/proc/16775/stat): 16775 (minisat+_script) S 16774 16775 21452 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855876225 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16775/statm): 531 226 485 147 0 384 0
[pid=16775] vsize: 2124
Raw data (/proc/16779/stat): 16779 (minisat+_64-bit) R 16775 16775 21452 0 -1 0 36449 0 0 0 89511 222 0 0 25 0 1 0 1855876230 138797056 33129 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16779/statm): 33886 33129 145 145 0 33741 0
[pid=16779] vsize: 135544
Current children cumulated CPU time (s) 897.34
Current children cumulated vsize (Kb) 137668

[startup+910.081 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 16779
Raw data (/proc/16775/stat): 16775 (minisat+_script) S 16774 16775 21452 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855876225 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16775/statm): 531 226 485 147 0 384 0
[pid=16775] vsize: 2124
Raw data (/proc/16779/stat): 16779 (minisat+_64-bit) R 16775 16775 21452 0 -1 0 36449 0 0 0 90511 222 0 0 25 0 1 0 1855876230 138797056 33129 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16779/statm): 33886 33129 145 145 0 33741 0
[pid=16779] vsize: 135544
Current children cumulated CPU time (s) 907.34
Current children cumulated vsize (Kb) 137668

[startup+920.082 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 16779
Raw data (/proc/16775/stat): 16775 (minisat+_script) S 16774 16775 21452 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855876225 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16775/statm): 531 226 485 147 0 384 0
[pid=16775] vsize: 2124
Raw data (/proc/16779/stat): 16779 (minisat+_64-bit) R 16775 16775 21452 0 -1 0 36449 0 0 0 91511 222 0 0 25 0 1 0 1855876230 138797056 33129 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16779/statm): 33886 33129 145 145 0 33741 0
[pid=16779] vsize: 135544
Current children cumulated CPU time (s) 917.34
Current children cumulated vsize (Kb) 137668

[startup+930.082 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 16779
Raw data (/proc/16775/stat): 16775 (minisat+_script) S 16774 16775 21452 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855876225 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16775/statm): 531 226 485 147 0 384 0
[pid=16775] vsize: 2124
Raw data (/proc/16779/stat): 16779 (minisat+_64-bit) R 16775 16775 21452 0 -1 0 36449 0 0 0 92512 222 0 0 25 0 1 0 1855876230 138797056 33129 4294967295 134512640 135094434 3221224432 3221223024 134557230 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16779/statm): 33886 33129 145 145 0 33741 0
[pid=16779] vsize: 135544
Current children cumulated CPU time (s) 927.35
Current children cumulated vsize (Kb) 137668

[startup+940.082 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 16779
Raw data (/proc/16775/stat): 16775 (minisat+_script) S 16774 16775 21452 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855876225 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16775/statm): 531 226 485 147 0 384 0
[pid=16775] vsize: 2124
Raw data (/proc/16779/stat): 16779 (minisat+_64-bit) R 16775 16775 21452 0 -1 0 36449 0 0 0 93512 222 0 0 25 0 1 0 1855876230 138797056 33129 4294967295 134512640 135094434 3221224432 3221223024 134552008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16779/statm): 33886 33129 145 145 0 33741 0
[pid=16779] vsize: 135544
Current children cumulated CPU time (s) 937.35
Current children cumulated vsize (Kb) 137668

[startup+950.083 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 16779
Raw data (/proc/16775/stat): 16775 (minisat+_script) S 16774 16775 21452 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855876225 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16775/statm): 531 226 485 147 0 384 0
[pid=16775] vsize: 2124
Raw data (/proc/16779/stat): 16779 (minisat+_64-bit) R 16775 16775 21452 0 -1 0 36449 0 0 0 94512 222 0 0 25 0 1 0 1855876230 138797056 33129 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16779/statm): 33886 33129 145 145 0 33741 0
[pid=16779] vsize: 135544
Current children cumulated CPU time (s) 947.35
Current children cumulated vsize (Kb) 137668

[startup+960.085 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 16779
Raw data (/proc/16775/stat): 16775 (minisat+_script) S 16774 16775 21452 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855876225 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16775/statm): 531 226 485 147 0 384 0
[pid=16775] vsize: 2124
Raw data (/proc/16779/stat): 16779 (minisat+_64-bit) R 16775 16775 21452 0 -1 0 36449 0 0 0 95512 222 0 0 25 0 1 0 1855876230 138797056 33129 4294967295 134512640 135094434 3221224432 3221223104 134555602 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16779/statm): 33886 33129 145 145 0 33741 0
[pid=16779] vsize: 135544
Current children cumulated CPU time (s) 957.35
Current children cumulated vsize (Kb) 137668

[startup+970.086 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 16779
Raw data (/proc/16775/stat): 16775 (minisat+_script) S 16774 16775 21452 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855876225 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16775/statm): 531 226 485 147 0 384 0
[pid=16775] vsize: 2124
Raw data (/proc/16779/stat): 16779 (minisat+_64-bit) R 16775 16775 21452 0 -1 0 36449 0 0 0 96513 222 0 0 25 0 1 0 1855876230 138797056 33129 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16779/statm): 33886 33129 145 145 0 33741 0
[pid=16779] vsize: 135544
Current children cumulated CPU time (s) 967.36
Current children cumulated vsize (Kb) 137668

[startup+980.086 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 16779
Raw data (/proc/16775/stat): 16775 (minisat+_script) S 16774 16775 21452 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855876225 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16775/statm): 531 226 485 147 0 384 0
[pid=16775] vsize: 2124
Raw data (/proc/16779/stat): 16779 (minisat+_64-bit) R 16775 16775 21452 0 -1 0 36449 0 0 0 97513 222 0 0 25 0 1 0 1855876230 138797056 33129 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16779/statm): 33886 33129 145 145 0 33741 0
[pid=16779] vsize: 135544
Current children cumulated CPU time (s) 977.36
Current children cumulated vsize (Kb) 137668

[startup+990.087 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 16779
Raw data (/proc/16775/stat): 16775 (minisat+_script) S 16774 16775 21452 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855876225 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16775/statm): 531 226 485 147 0 384 0
[pid=16775] vsize: 2124
Raw data (/proc/16779/stat): 16779 (minisat+_64-bit) R 16775 16775 21452 0 -1 0 36449 0 0 0 98513 222 0 0 25 0 1 0 1855876230 138797056 33129 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16779/statm): 33886 33129 145 145 0 33741 0
[pid=16779] vsize: 135544
Current children cumulated CPU time (s) 987.36
Current children cumulated vsize (Kb) 137668

[startup+1000.09 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 16779
Raw data (/proc/16775/stat): 16775 (minisat+_script) S 16774 16775 21452 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855876225 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16775/statm): 531 226 485 147 0 384 0
[pid=16775] vsize: 2124
Raw data (/proc/16779/stat): 16779 (minisat+_64-bit) R 16775 16775 21452 0 -1 0 36449 0 0 0 99513 222 0 0 25 0 1 0 1855876230 138797056 33129 4294967295 134512640 135094434 3221224432 3221223088 134557917 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16779/statm): 33886 33129 145 145 0 33741 0
[pid=16779] vsize: 135544
Current children cumulated CPU time (s) 997.36
Current children cumulated vsize (Kb) 137668

[startup+1010.09 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 16779
Raw data (/proc/16775/stat): 16775 (minisat+_script) S 16774 16775 21452 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855876225 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16775/statm): 531 226 485 147 0 384 0
[pid=16775] vsize: 2124
Raw data (/proc/16779/stat): 16779 (minisat+_64-bit) R 16775 16775 21452 0 -1 0 36449 0 0 0 100514 222 0 0 25 0 1 0 1855876230 138797056 33129 4294967295 134512640 135094434 3221224432 3221223024 134557219 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16779/statm): 33886 33129 145 145 0 33741 0
[pid=16779] vsize: 135544
Current children cumulated CPU time (s) 1007.37
Current children cumulated vsize (Kb) 137668

[startup+1020.09 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 16779
Raw data (/proc/16775/stat): 16775 (minisat+_script) S 16774 16775 21452 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855876225 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16775/statm): 531 226 485 147 0 384 0
[pid=16775] vsize: 2124
Raw data (/proc/16779/stat): 16779 (minisat+_64-bit) R 16775 16775 21452 0 -1 0 36449 0 0 0 101514 222 0 0 25 0 1 0 1855876230 138797056 33129 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16779/statm): 33886 33129 145 145 0 33741 0
[pid=16779] vsize: 135544
Current children cumulated CPU time (s) 1017.37
Current children cumulated vsize (Kb) 137668

[startup+1030.09 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 16779
Raw data (/proc/16775/stat): 16775 (minisat+_script) S 16774 16775 21452 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855876225 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16775/statm): 531 226 485 147 0 384 0
[pid=16775] vsize: 2124
Raw data (/proc/16779/stat): 16779 (minisat+_64-bit) R 16775 16775 21452 0 -1 0 36449 0 0 0 102514 222 0 0 25 0 1 0 1855876230 138797056 33129 4294967295 134512640 135094434 3221224432 3221223076 134562166 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16779/statm): 33886 33129 145 145 0 33741 0
[pid=16779] vsize: 135544
Current children cumulated CPU time (s) 1027.37
Current children cumulated vsize (Kb) 137668

[startup+1040.09 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 16779
Raw data (/proc/16775/stat): 16775 (minisat+_script) S 16774 16775 21452 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855876225 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16775/statm): 531 226 485 147 0 384 0
[pid=16775] vsize: 2124
Raw data (/proc/16779/stat): 16779 (minisat+_64-bit) R 16775 16775 21452 0 -1 0 36449 0 0 0 103514 222 0 0 25 0 1 0 1855876230 138797056 33129 4294967295 134512640 135094434 3221224432 3221223088 134558019 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16779/statm): 33886 33129 145 145 0 33741 0
[pid=16779] vsize: 135544
Current children cumulated CPU time (s) 1037.37
Current children cumulated vsize (Kb) 137668

[startup+1050.09 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 16779
Raw data (/proc/16775/stat): 16775 (minisat+_script) S 16774 16775 21452 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855876225 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16775/statm): 531 226 485 147 0 384 0
[pid=16775] vsize: 2124
Raw data (/proc/16779/stat): 16779 (minisat+_64-bit) R 16775 16775 21452 0 -1 0 36449 0 0 0 104515 222 0 0 25 0 1 0 1855876230 138797056 33129 4294967295 134512640 135094434 3221224432 3221223024 134556712 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16779/statm): 33886 33129 145 145 0 33741 0
[pid=16779] vsize: 135544
Current children cumulated CPU time (s) 1047.38
Current children cumulated vsize (Kb) 137668

[startup+1060.09 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 16779
Raw data (/proc/16775/stat): 16775 (minisat+_script) S 16774 16775 21452 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855876225 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16775/statm): 531 226 485 147 0 384 0
[pid=16775] vsize: 2124
Raw data (/proc/16779/stat): 16779 (minisat+_64-bit) R 16775 16775 21452 0 -1 0 36449 0 0 0 105515 222 0 0 25 0 1 0 1855876230 138797056 33129 4294967295 134512640 135094434 3221224432 3221223088 134558016 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16779/statm): 33886 33129 145 145 0 33741 0
[pid=16779] vsize: 135544
Current children cumulated CPU time (s) 1057.38
Current children cumulated vsize (Kb) 137668

[startup+1070.09 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 16779
Raw data (/proc/16775/stat): 16775 (minisat+_script) S 16774 16775 21452 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855876225 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16775/statm): 531 226 485 147 0 384 0
[pid=16775] vsize: 2124
Raw data (/proc/16779/stat): 16779 (minisat+_64-bit) R 16775 16775 21452 0 -1 0 36449 0 0 0 106515 222 0 0 25 0 1 0 1855876230 138797056 33129 4294967295 134512640 135094434 3221224432 3221223024 134551897 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16779/statm): 33886 33129 145 145 0 33741 0
[pid=16779] vsize: 135544
Current children cumulated CPU time (s) 1067.38
Current children cumulated vsize (Kb) 137668

[startup+1080.09 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 16779
Raw data (/proc/16775/stat): 16775 (minisat+_script) S 16774 16775 21452 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855876225 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16775/statm): 531 226 485 147 0 384 0
[pid=16775] vsize: 2124
Raw data (/proc/16779/stat): 16779 (minisat+_64-bit) R 16775 16775 21452 0 -1 0 36449 0 0 0 107515 222 0 0 25 0 1 0 1855876230 138797056 33129 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16779/statm): 33886 33129 145 145 0 33741 0
[pid=16779] vsize: 135544
Current children cumulated CPU time (s) 1077.38
Current children cumulated vsize (Kb) 137668

[startup+1090.09 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 16779
Raw data (/proc/16775/stat): 16775 (minisat+_script) S 16774 16775 21452 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855876225 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16775/statm): 531 226 485 147 0 384 0
[pid=16775] vsize: 2124
Raw data (/proc/16779/stat): 16779 (minisat+_64-bit) R 16775 16775 21452 0 -1 0 36450 0 0 0 108516 222 0 0 25 0 1 0 1855876230 138797056 33130 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16779/statm): 33886 33130 145 145 0 33741 0
[pid=16779] vsize: 135544
Current children cumulated CPU time (s) 1087.39
Current children cumulated vsize (Kb) 137668

[startup+1100.09 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 16779
Raw data (/proc/16775/stat): 16775 (minisat+_script) S 16774 16775 21452 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855876225 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16775/statm): 531 226 485 147 0 384 0
[pid=16775] vsize: 2124
Raw data (/proc/16779/stat): 16779 (minisat+_64-bit) R 16775 16775 21452 0 -1 0 36450 0 0 0 109516 222 0 0 25 0 1 0 1855876230 138797056 33130 4294967295 134512640 135094434 3221224432 3221223088 134558126 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16779/statm): 33886 33130 145 145 0 33741 0
[pid=16779] vsize: 135544
Current children cumulated CPU time (s) 1097.39
Current children cumulated vsize (Kb) 137668

[startup+1110.09 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 16779
Raw data (/proc/16775/stat): 16775 (minisat+_script) S 16774 16775 21452 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855876225 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16775/statm): 531 226 485 147 0 384 0
[pid=16775] vsize: 2124
Raw data (/proc/16779/stat): 16779 (minisat+_64-bit) R 16775 16775 21452 0 -1 0 36450 0 0 0 110516 222 0 0 25 0 1 0 1855876230 138797056 33130 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16779/statm): 33886 33130 145 145 0 33741 0
[pid=16779] vsize: 135544
Current children cumulated CPU time (s) 1107.39
Current children cumulated vsize (Kb) 137668

[startup+1120.1 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 16779
Raw data (/proc/16775/stat): 16775 (minisat+_script) S 16774 16775 21452 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855876225 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16775/statm): 531 226 485 147 0 384 0
[pid=16775] vsize: 2124
Raw data (/proc/16779/stat): 16779 (minisat+_64-bit) R 16775 16775 21452 0 -1 0 36450 0 0 0 111516 222 0 0 25 0 1 0 1855876230 138797056 33130 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16779/statm): 33886 33130 145 145 0 33741 0
[pid=16779] vsize: 135544
Current children cumulated CPU time (s) 1117.39
Current children cumulated vsize (Kb) 137668

[startup+1130.1 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 16779
Raw data (/proc/16775/stat): 16775 (minisat+_script) S 16774 16775 21452 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855876225 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16775/statm): 531 226 485 147 0 384 0
[pid=16775] vsize: 2124
Raw data (/proc/16779/stat): 16779 (minisat+_64-bit) R 16775 16775 21452 0 -1 0 36450 0 0 0 112516 222 0 0 25 0 1 0 1855876230 138797056 33130 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16779/statm): 33886 33130 145 145 0 33741 0
[pid=16779] vsize: 135544
Current children cumulated CPU time (s) 1127.39
Current children cumulated vsize (Kb) 137668

[startup+1140.1 s]
Raw data (loadavg): 1.00 1.00 0.92 1/57 16779
Raw data (/proc/16775/stat): 16775 (minisat+_script) S 16774 16775 21452 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855876225 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16775/statm): 531 226 485 147 0 384 0
[pid=16775] vsize: 2124
Raw data (/proc/16779/stat): 16779 (minisat+_64-bit) T 16775 16775 21452 0 -1 0 36628 0 0 0 113514 223 0 0 25 0 1 0 1855876230 139526144 33308 4294967295 134512640 135094434 3221224432 3221222796 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/16779/statm): 34064 33308 145 145 0 33919 0
[pid=16779] vsize: 136256
Current children cumulated CPU time (s) 1137.38
Current children cumulated vsize (Kb) 138380

[startup+1150.1 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 16779
Raw data (/proc/16775/stat): 16775 (minisat+_script) S 16774 16775 21452 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855876225 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16775/statm): 531 226 485 147 0 384 0
[pid=16775] vsize: 2124
Raw data (/proc/16779/stat): 16779 (minisat+_64-bit) R 16775 16775 21452 0 -1 0 37002 0 0 0 114508 226 0 0 25 0 1 0 1855876230 141062144 33682 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16779/statm): 34439 33682 145 145 0 34294 0
[pid=16779] vsize: 137756
Current children cumulated CPU time (s) 1147.35
Current children cumulated vsize (Kb) 139880

[startup+1160.1 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 16779
Raw data (/proc/16775/stat): 16775 (minisat+_script) S 16774 16775 21452 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855876225 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16775/statm): 531 226 485 147 0 384 0
[pid=16775] vsize: 2124
Raw data (/proc/16779/stat): 16779 (minisat+_64-bit) R 16775 16775 21452 0 -1 0 37189 0 0 0 115505 228 0 0 25 0 1 0 1855876230 141836288 33869 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16779/statm): 34628 33869 145 145 0 34483 0
[pid=16779] vsize: 138512
Current children cumulated CPU time (s) 1157.34
Current children cumulated vsize (Kb) 140636

[startup+1170.1 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 16779
Raw data (/proc/16775/stat): 16775 (minisat+_script) S 16774 16775 21452 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855876225 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16775/statm): 531 226 485 147 0 384 0
[pid=16775] vsize: 2124
Raw data (/proc/16779/stat): 16779 (minisat+_64-bit) R 16775 16775 21452 0 -1 0 37484 0 0 0 116500 229 0 0 25 0 1 0 1855876230 143069184 34164 4294967295 134512640 135094434 3221224432 3221223056 134562057 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16779/statm): 34929 34164 145 145 0 34784 0
[pid=16779] vsize: 139716
Current children cumulated CPU time (s) 1167.3
Current children cumulated vsize (Kb) 141840

[startup+1180.1 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 16779
Raw data (/proc/16775/stat): 16775 (minisat+_script) S 16774 16775 21452 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855876225 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16775/statm): 531 226 485 147 0 384 0
[pid=16775] vsize: 2124
Raw data (/proc/16779/stat): 16779 (minisat+_64-bit) R 16775 16775 21452 0 -1 0 37820 0 0 0 117495 231 0 0 25 0 1 0 1855876230 144445440 34500 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16779/statm): 35265 34500 145 145 0 35120 0
[pid=16779] vsize: 141060
Current children cumulated CPU time (s) 1177.27
Current children cumulated vsize (Kb) 143184

[startup+1190.1 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 16779
Raw data (/proc/16775/stat): 16775 (minisat+_script) S 16774 16775 21452 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855876225 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16775/statm): 531 226 485 147 0 384 0
[pid=16775] vsize: 2124
Raw data (/proc/16779/stat): 16779 (minisat+_64-bit) R 16775 16775 21452 0 -1 0 37907 0 0 0 118493 232 0 0 25 0 1 0 1855876230 144809984 34587 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16779/statm): 35354 34587 145 145 0 35209 0
[pid=16779] vsize: 141416
Current children cumulated CPU time (s) 1187.26
Current children cumulated vsize (Kb) 143540

[startup+1200.1 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 16779
Raw data (/proc/16775/stat): 16775 (minisat+_script) S 16774 16775 21452 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855876225 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16775/statm): 531 226 485 147 0 384 0
[pid=16775] vsize: 2124
Raw data (/proc/16779/stat): 16779 (minisat+_64-bit) R 16775 16775 21452 0 -1 0 38115 0 0 0 119490 234 0 0 25 0 1 0 1855876230 145661952 34795 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16779/statm): 35562 34795 145 145 0 35417 0
[pid=16779] vsize: 142248
Current children cumulated CPU time (s) 1197.25
Current children cumulated vsize (Kb) 144372

[startup+1210.1 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 16779
Raw data (/proc/16775/stat): 16775 (minisat+_script) S 16774 16775 21452 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855876225 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16775/statm): 531 226 485 147 0 384 0
[pid=16775] vsize: 2124
Raw data (/proc/16779/stat): 16779 (minisat+_64-bit) R 16775 16775 21452 0 -1 0 38729 0 0 0 120481 238 0 0 25 0 1 0 1855876230 148176896 35409 4294967295 134512640 135094434 3221224432 3221223088 134557925 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16779/statm): 36176 35409 145 145 0 36031 0
[pid=16779] vsize: 144704
Current children cumulated CPU time (s) 1207.2
Current children cumulated vsize (Kb) 146828



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.1 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 16779
Raw data (/proc/16775/stat): 16775 (minisat+_script) S 16774 16775 21452 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855876225 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16775/statm): 531 226 485 147 0 384 0
[pid=16775] vsize: 2124
Raw data (/proc/16779/stat): 16779 (minisat+_64-bit) R 16775 16775 21452 0 -1 0 38729 0 0 0 120481 238 0 0 25 0 1 0 1855876230 148176896 35409 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16779/statm): 36176 35409 145 145 0 36031 0
[pid=16779] vsize: 144704
Current children cumulated CPU time (s) 1207.2
Current children cumulated vsize (Kb) 146828

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

Child status: 10
Real time (s): 1210.18
CPU time (s): 1207.27
CPU user time (s): 1204.82
CPU system time (s): 2.45063
CPU usage (%): 99.7597
Max. virtual memory (cumulated for all children) (Kb): 146828

Verifier Data

ERROR: no interpretation found !