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-ran10x10b.opb
MD5SUMc76102ddcf7f5ab3b2677033d320eaa3
Bench Categoryoptimization, medium integers (OPTMEDINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function 756736
Optimality of the best value was proved NO
Number of terms in the objective function 2100
Biggest coefficient in the objective function 4718592
Number of bits for the biggest coefficient in the objective function 23
Sum of the numbers in the objective function 502612132
Number of bits of the sum of numbers in the objective function 29
Biggest number in a constraint 4718592
Number of bits of the biggest number in a constraint 23
Biggest sum of numbers in a constraint 502612132
Number of bits of the biggest sum of numbers29
Best result obtained on this benchmarkSAT
Best CPU time to get the best result obtained on this benchmark1189.02
Number of variables2100
Total number of constraints120
Number of constraints which are clauses0
Number of constraints which are cardinality constraints (but not clauses)0
Number of constraints which are nor clauses,nor cardinality constraints120
Minimum length of a constraint21
Maximum length of a constraint200

Trace number 6254

Launcher Data

LAUNCH ON wulflinc10 THE 2005-09-20 04:55:04 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3421 boxname=wulflinc10 idbench=1077 idsolver=3 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  c76102ddcf7f5ab3b2677033d320eaa3  /oldhome/oroussel/tmp/wulflinc10/normalized-mps-v2-13-7-ran10x10b.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc10/normalized-mps-v2-13-7-ran10x10b.opb
IDLAUNCH: 3421
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 450.999
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	: 2
cpu MHz		: 450.999
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:        785068 kB
Buffers:         38524 kB
Cached:         183676 kB
SwapCached:        228 kB
Active:          83884 kB
Inactive:       141300 kB
HighTotal:      131008 kB
HighFree:         6160 kB
LowTotal:       903652 kB
LowFree:        778908 kB
SwapTotal:     2097136 kB
SwapFree:      2096756 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6280 kB
Slab:            18804 kB
Committed_AS:    64128 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-09-20 05:15:14 (client local time) WITH STATUS 10 IN 1208 SECONDS
stats: 3421 7 1208 10

Solver Data

c Parsing PB file...
c Converting 140 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ####################
c   -- Clauses(.)/Splits(s): (none)
c ---[ 138]---> Sorter-cost: 2002     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 136]---> Sorter-cost: 1844     Base: 2 2 2 2 2 2 2 2
c ---[ 134]---> Sorter-cost: 1844     Base: 2 2 2 2 2 2 2 2
c ---[ 132]---> Sorter-cost: 2002     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 130]---> Sorter-cost: 1844     Base: 2 2 2 2 2 2 2 2
c ---[ 128]---> Sorter-cost: 1985     Base: 2 2 2 2 2 2 2 2 2
c ---[ 126]---> Sorter-cost: 1985     Base: 2 2 2 2 2 2 2 2 2
c ---[ 124]---> Sorter-cost: 1780     Base: 2 2 2 2 2 2 2
c ---[ 122]---> Sorter-cost: 1844     Base: 2 2 2 2 2 2 2 2
c ---[ 120]---> Sorter-cost: 2002     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 118]---> Sorter-cost: 1658     Base: 2 2 2 2 2 2 2 2
c ---[ 116]---> Sorter-cost: 2002     Base: 2 2 2 2 2 2 2 2 2
c ---[ 114]---> Adder-cost: 180   maxlim: 8950   bits: 14/14
c ---[ 112]---> Sorter-cost: 2083     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 110]---> Sorter-cost: 2083     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 108]---> Sorter-cost: 1658     Base: 2 2 2 2 2 2 2 2
c ---[ 106]---> Sorter-cost: 2083     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 104]---> Sorter-cost: 2002     Base: 2 2 2 2 2 2 2 2 2
c ---[ 102]---> Sorter-cost: 1442     Base: 2 2 2 2 2 2 2
c ---[ 100]---> Sorter-cost: 2002     Base: 2 2 2 2 2 2 2 2 2
c ---[  99]---> BDD-cost:   11
c ---[  98]---> BDD-cost:   15
c ---[  97]---> BDD-cost:   11
c ---[  96]---> BDD-cost:   13
c ---[  95]---> BDD-cost:   12
c ---[  94]---> BDD-cost:   13
c ---[  93]---> BDD-cost:   13
c ---[  92]---> BDD-cost:   11
c ---[  91]---> BDD-cost:   13
c ---[  90]---> BDD-cost:   13
c ---[  89]---> BDD-cost:    9
c ---[  88]---> BDD-cost:   13
c ---[  87]---> BDD-cost:   12
c ---[  86]---> BDD-cost:   11
c ---[  85]---> BDD-cost:   11
c ---[  84]---> BDD-cost:   11
c ---[  83]---> BDD-cost:   11
c ---[  82]---> BDD-cost:   11
c ---[  81]---> BDD-cost:   11
c ---[  80]---> BDD-cost:   11
c ---[  79]---> BDD-cost:   11
c ---[  78]---> BDD-cost:    9
c ---[  77]---> BDD-cost:   11
c ---[  76]---> BDD-cost:   13
c ---[  75]---> BDD-cost:   11
c ---[  74]---> BDD-cost:   15
c ---[  73]---> BDD-cost:   12
c ---[  72]---> BDD-cost:   17
c ---[  71]---> BDD-cost:   17
c ---[  70]---> BDD-cost:   11
c ---[  69]---> BDD-cost:   17
c ---[  68]---> BDD-cost:   15
c ---[  67]---> BDD-cost:    9
c ---[  66]---> BDD-cost:   15
c ---[  65]---> BDD-cost:   13
c ---[  64]---> BDD-cost:   11
c ---[  63]---> BDD-cost:   13
c ---[  62]---> BDD-cost:   13
c ---[  61]---> BDD-cost:   13
c ---[  60]---> BDD-cost:   13
c ---[  59]---> BDD-cost:   11
c ---[  58]---> BDD-cost:   13
c ---[  57]---> BDD-cost:   13
c ---[  56]---> BDD-cost:    9
c ---[  55]---> BDD-cost:   13
c ---[  54]---> BDD-cost:   11
c ---[  53]---> BDD-cost:   11
c ---[  52]---> BDD-cost:   13
c ---[  51]---> BDD-cost:   12
c ---[  50]---> BDD-cost:   13
c ---[  49]---> BDD-cost:   13
c ---[  48]---> BDD-cost:   11
c ---[  47]---> BDD-cost:   13
c ---[  46]---> BDD-cost:   15
c ---[  45]---> BDD-cost:    9
c ---[  44]---> BDD-cost:   15
c ---[  43]---> BDD-cost:   13
c ---[  42]---> BDD-cost:   11
c ---[  41]---> BDD-cost:   15
c ---[  40]---> BDD-cost:   12
c ---[  39]---> BDD-cost:   15
c ---[  38]---> BDD-cost:   15
c ---[  37]---> BDD-cost:   11
c ---[  36]---> BDD-cost:   15
c ---[  35]---> BDD-cost:   15
c ---[  34]---> BDD-cost:    9
c ---[  33]---> BDD-cost:   15
c ---[  32]---> BDD-cost:   15
c ---[  31]---> BDD-cost:   11
c ---[  30]---> BDD-cost:   11
c ---[  29]---> BDD-cost:   11
c ---[  28]---> BDD-cost:   11
c ---[  27]---> BDD-cost:   11
c ---[  26]---> BDD-cost:   11
c ---[  25]---> BDD-cost:   11
c ---[  24]---> BDD-cost:   11
c ---[  23]---> BDD-cost:    9
c ---[  22]---> BDD-cost:   11
c ---[  21]---> BDD-cost:    9
c ---[  20]---> BDD-cost:   11
c ---[  19]---> BDD-cost:   11
c ---[  18]---> BDD-cost:   11
c ---[  17]---> BDD-cost:   11
c ---[  16]---> BDD-cost:   11
c ---[  15]---> BDD-cost:   11
c ---[  14]---> BDD-cost:   11
c ---[  13]---> BDD-cost:   11
c ---[  12]---> BDD-cost:    9
c ---[  11]---> BDD-cost:   11
c ---[  10]---> BDD-cost:   15
c ---[   9]---> BDD-cost:   11
c ---[   8]---> BDD-cost:   15
c ---[   7]---> BDD-cost:   12
c ---[   6]---> BDD-cost:   16
c ---[   5]---> BDD-cost:   17
c ---[   4]---> BDD-cost:   11
c ---[   3]---> BDD-cost:   17
c ---[   2]---> BDD-cost:   15
c ---[   1]---> BDD-cost:    9
c ---[   0]---> BDD-cost:   15
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   94440   224184 |   31480       0        0     nan |  0.000 % |
c |       101 |   94437   224178 |   34628     100      570     5.7 |  7.012 % |
c |       252 |   94437   224178 |   38090     251     1345     5.4 |  7.012 % |
c |       477 |   94437   224178 |   41899     476     2436     5.1 |  7.012 % |
c |       815 |   94437   224178 |   46089     814     4318     5.3 |  7.012 % |
c |      1321 |   94364   224012 |   50698    1315     7319     5.6 |  7.070 % |
c |      2080 |   94364   224012 |   55768    2074    13413     6.5 |  7.070 % |
c ==============================================================================
c Found solution: 3361005
c ---[   0]---> Adder-cost: 3932   maxlim: 748215   bits: 21/20
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2827 |  121769   321931 |   40589    2820    18795     6.7 |  7.070 % |
c |      2927 |  121769   321931 |   44647    2920    19181     6.6 |  6.370 % |
c |      3077 |  121769   321931 |   49112    3070    19960     6.5 |  6.370 % |
c |      3302 |  121759   321908 |   54023    3294    21345     6.5 |  6.378 % |
c |      3639 |  121712   321803 |   59426    3629    22935     6.3 |  6.412 % |
c |      4146 |  121626   321610 |   65368    4125    28733     7.0 |  6.475 % |
c |      4905 |  121542   321421 |   71905    4876    34042     7.0 |  6.536 % |
c |      6044 |  121474   321266 |   79096    6005    39965     6.7 |  6.586 % |
c ==============================================================================
c Found solution: 3321878
c ---[   0]---> Adder-cost: 0   maxlim: 787342   bits: 21/20
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      6703 |  121285   320978 |   40428    6639    58563     8.8 |  6.586 % |
c |      6804 |  121285   320978 |   44470    6740    59057     8.8 |  6.766 % |
c |      6957 |  121285   320978 |   48917    6893    62729     9.1 |  6.766 % |
c |      7182 |  121285   320978 |   53809    7118    64454     9.1 |  6.766 % |
c |      7519 |  121169   320707 |   59190    7417    65940     8.9 |  6.859 % |
c |      8026 |  121169   320707 |   65109    7924    68826     8.7 |  6.859 % |
c ==============================================================================
c Found solution: 3034933
c ---[   0]---> Adder-cost: 2   maxlim: 1074287   bits: 22/21
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      8656 |  121194   320855 |   40398    8552    75550     8.8 |  6.859 % |
c |      8756 |  121194   320855 |   44437    8652    76113     8.8 |  6.878 % |
c |      8908 |  121194   320855 |   48881    8804    77091     8.8 |  6.878 % |
c |      9133 |  121152   320760 |   53769    9024    78322     8.7 |  6.912 % |
c |      9470 |  121152   320760 |   59146    9361    80758     8.6 |  6.912 % |
c |      9977 |  121143   320731 |   65061    9867    83509     8.5 |  6.917 % |
c |     10738 |  120912   320196 |   71567   10605   108938    10.3 |  7.102 % |
c |     11878 |  120790   319922 |   78724   11737   136105    11.6 |  7.192 % |
c |     13586 |  120728   319779 |   86596   13439   318010    23.7 |  7.239 % |
c ==============================================================================
c Found solution: 2741413
c ---[   0]---> Adder-cost: 0   maxlim: 1367807   bits: 22/21
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     14526 |  120415   319084 |   40138   14363   328514    22.9 |  7.239 % |
c |     14626 |  120291   318801 |   44151   14448   328931    22.8 |  7.599 % |
c |     14776 |  120291   318801 |   48566   14598   329878    22.6 |  7.599 % |
c |     15001 |  120291   318801 |   53423   14823   331411    22.4 |  7.599 % |
c |     15339 |  120196   318579 |   58766   15153   334444    22.1 |  7.668 % |
c |     15845 |  120196   318579 |   64642   15659   358958    22.9 |  7.668 % |
c ==============================================================================
c Found solution: 2139517
c ---[   0]---> Adder-cost: 0   maxlim: 1969703   bits: 22/21
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     16297 |  120178   318611 |   40059   16106   369090    22.9 |  7.668 % |
c |     16397 |  120178   318611 |   44064   16206   369595    22.8 |  7.711 % |
c |     16548 |  120151   318551 |   48471   16356   370428    22.6 |  7.729 % |
c |     16774 |  120151   318551 |   53318   16582   372967    22.5 |  7.729 % |
c |     17111 |  120151   318551 |   58650   16919   375249    22.2 |  7.729 % |
c |     17618 |  120109   318454 |   64515   17425   380618    21.8 |  7.758 % |
c |     18377 |  119996   318197 |   70966   18169   391139    21.5 |  7.843 % |
c |     19517 |  119952   318097 |   78063   19307   426757    22.1 |  7.874 % |
c |     21226 |  119894   317962 |   85870   20993   569764    27.1 |  7.916 % |
c |     23789 |  119764   317666 |   94457   23537   682312    29.0 |  8.025 % |
c |     27633 |  119564   317200 |  103902   27363   825435    30.2 |  8.170 % |
c ==============================================================================
c Found solution: 2113156
c ---[   0]---> Adder-cost: 0   maxlim: 1996064   bits: 22/21
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     28733 |  119550   317247 |   39850   28462   885214    31.1 |  8.170 % |
c |     28834 |  119550   317247 |   43835   28563   887914    31.1 |  8.204 % |
c |     28986 |  119550   317247 |   48218   28715   892015    31.1 |  8.204 % |
c |     29211 |  119536   317215 |   53040   28939   893555    30.9 |  8.215 % |
c |     29548 |  119536   317215 |   58344   29276   897025    30.6 |  8.215 % |
c |     30054 |  119520   317163 |   64178   29779   900477    30.2 |  8.223 % |
c |     30814 |  119510   317141 |   70596   30538   959301    31.4 |  8.231 % |
c |     31957 |  119364   316810 |   77656   31665  1002720    31.7 |  8.336 % |
c |     33666 |  119141   316297 |   85422   33358  1184902    35.5 |  8.526 % |
c |     36229 |  119138   316291 |   93964   35920  1272971    35.4 |  8.529 % |
c |     40073 |  119138   316291 |  103360   39764  1694680    42.6 |  8.529 % |
c ==============================================================================
c Found solution: 1952025
c ---[   0]---> Adder-cost: 0   maxlim: 2157195   bits: 22/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     42094 |  118990   315750 |   39663   41553  1778469    42.8 |  8.529 % |
c |     42195 |  118990   315750 |   43629   41654  1779031    42.7 |  8.644 % |
c |     42345 |  118990   315750 |   47992   41804  1779955    42.6 |  8.644 % |
c |     42570 |  118969   315702 |   52791   42028  1784395    42.5 |  8.660 % |
c |     42908 |  118969   315702 |   58070   42366  1801515    42.5 |  8.660 % |
c |     43416 |  118969   315702 |   63877   42874  1808231    42.2 |  8.660 % |
c |     44176 |  118969   315702 |   70265   43634  1870338    42.9 |  8.660 % |
c |     45315 |  118962   315687 |   77291   44772  2076825    46.4 |  8.665 % |
c |     47023 |  118910   315571 |   85021   46476  2136601    46.0 |  8.707 % |
c |     49586 |  118762   315232 |   93523   49028  2291729    46.7 |  8.820 % |
c |     53430 |  118565   314772 |  102875   52851  2489507    47.1 |  8.971 % |
c |     59197 |  118420   314432 |  113163   58590  2915808    49.8 |  9.084 % |
c |     67846 |  118390   314365 |  124479   67236  3610523    53.7 |  9.108 % |
c |     80821 |  118313   314184 |  136927   80197  4438935    55.4 |  9.174 % |
c |    100283 |  118144   313795 |  150620   99633 11034769   110.8 |  9.316 % |
c |    129476 |  117905   313241 |  165682  128795 13936639   108.2 |  9.492 % |
c ==============================================================================
c Found solution: 1916946
c ---[   0]---> Adder-cost: 0   maxlim: 2192274   bits: 22/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    168420 |  117896   313332 |   39298  167734 22410520   133.6 |  9.492 % |
c |    168520 |  117870   313270 |   43227   20819  4079432   195.9 |  9.560 % |
c |    168670 |  117870   313270 |   47550   20969  4081339   194.6 |  9.560 % |
c |    168898 |  117870   313270 |   52305   21197  4084562   192.7 |  9.560 % |
c |    169236 |  117870   313270 |   57536   21535  4086594   189.8 |  9.560 % |
c |    169742 |  117870   313270 |   63289   22041  4089391   185.5 |  9.560 % |
c |    170501 |  117870   313270 |   69618   22800  4104055   180.0 |  9.560 % |
c |    171640 |  117791   313088 |   76580   23934  4125283   172.4 |  9.615 % |
c |    173349 |  117745   312985 |   84238   25638  4191141   163.5 |  9.649 % |
c |    175911 |  117704   312889 |   92662   28195  4449613   157.8 |  9.683 % |
c |    179755 |  117577   312586 |  101928   32025  4659052   145.5 |  9.770 % |
c |    185522 |  117567   312564 |  112121   37791  5194372   137.4 |  9.778 % |
c ==============================================================================
c Found solution: 1886130
c ---[   0]---> Adder-cost: 0   maxlim: 2223090   bits: 22/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    187250 |  117587   312745 |   39195   39519  5355132   135.5 |  9.778 % |
c |    187350 |  117587   312745 |   43114   39619  5357166   135.2 |  9.805 % |
c |    187500 |  117576   312721 |   47425   39768  5357889   134.7 |  9.813 % |
c |    187725 |  117576   312721 |   52168   39993  5364068   134.1 |  9.813 % |
c |    188062 |  117576   312721 |   57385   40330  5376881   133.3 |  9.813 % |
c |    188568 |  117576   312721 |   63123   40836  5393883   132.1 |  9.813 % |
c |    189327 |  117513   312554 |   69436   41584  5416974   130.3 |  9.857 % |
c |    190467 |  117513   312554 |   76379   42724  5452110   127.6 |  9.857 % |
c |    192177 |  117478   312474 |   84017   44432  5499810   123.8 |  9.884 % |
c ==============================================================================
c Found solution: 1389200
c ---[   0]---> Adder-cost: 0   maxlim: 2720020   bits: 22/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    192899 |  117488   312570 |   39162   45154  5579341   123.6 |  9.884 % |
c |    192999 |  117488   312570 |   43078   19622   904548    46.1 |  9.899 % |
c |    193151 |  117488   312570 |   47386   19774   905793    45.8 |  9.899 % |
c |    193377 |  117488   312570 |   52124   20000   909419    45.5 |  9.899 % |
c |    193715 |  117488   312570 |   57337   20338   941855    46.3 |  9.899 % |
c |    194222 |  117477   312545 |   63070   20844   952724    45.7 |  9.907 % |
c |    194982 |  117427   312430 |   69377   21600   987252    45.7 |  9.947 % |
c |    196123 |  117427   312430 |   76315   22741  1022205    44.9 |  9.947 % |
c |    197831 |  117364   312288 |   83947   24439  1119745    45.8 |  9.999 % |
c |    200393 |  117364   312288 |   92341   27001  1354141    50.2 |  9.999 % |
c |    204237 |  117322   312184 |  101576   30832  1677457    54.4 | 10.031 % |
c |    210003 |  117322   312184 |  111733   36598  2155397    58.9 | 10.031 % |
c |    218653 |  117306   312147 |  122907   45247  2729443    60.3 | 10.044 % |
c |    231629 |  117306   312147 |  135197   58223  7709688   132.4 | 10.044 % |
c |    251090 |  117271   312067 |  148717   77678  8752573   112.7 | 10.073 % |
c |    280282 |  117139   311758 |  163589  106864 12479821   116.8 | 10.178 % |
c |    324072 |  116978   311385 |  179948  150630 17457633   115.9 | 10.302 % |
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 -X96_bit_7 -X96_bit_6 -X96_bit_5 -X96_bit_4 -X96_bit_3 -X96_bit_2 -X96_bit_1 -X96_bit0 -X96_bit1 -X96_bit2 -X96_bit3 -X96_bit4 -X96_bit5 -X96_bit6 -X96_bit7 -X96_bit8 -X96_bit9 -X96_bit10 -X96_bit11 -X96_bit12 X97_bit_7 X97_bit_6 X97_bit_5 X97_bit_4 -X97_bit_3 -X97_bit_2 X97_bit_1 -X97_bit0 -X97_bit1 -X97_bit2 X97_bit3 -X97_bit4 -X97_bit5 -X97_bit6 -X97_bit7 -X97_bit8 -X97_bit9 -X97_bit10 -X97_bit11 -X97_bit12 X98_bit_7 X98_bit_6 X98_bit_5 X98_bit_4 -X98_bit_3 -X98_bit_2 X98_bit_1 -X98_bit0 -X98_bit1 -X98_bit2 -X98_bit3 -X98_bit4 -X98_bit5 -X98_bit6 -X98_bit7 -X98_bit8 -X98_bit9 -X98_bit10 -X98_bit11 -X98_bit12 X99_bit_7 X99_bi

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/14757/stat): 14757 (minisat+_script) R 14756 14757 22582 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1797626896 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 1 0 0
Raw data (/proc/14757/statm): 174 3 169 147 0 27 0
[pid=14757] 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=14758
New process pid=14759
New process pid=14760
execve syscall for /bin/sed executable
One traced child (pid=14759) 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=14760) exited with status: 0
One traced child (pid=14758) exited with status: 0
New process pid=14761
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc10/normalized-mps-v2-13-7-ran10x10b.opb

[startup+10.0032 s]
Raw data (loadavg): 0.93 0.98 0.91 2/57 14761
Raw data (/proc/14757/stat): 14757 (minisat+_script) S 14756 14757 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797626896 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14757/statm): 531 226 485 147 0 384 0
[pid=14757] vsize: 2124
Raw data (/proc/14761/stat): 14761 (minisat+_64-bit) R 14757 14757 22582 0 -1 0 5914 0 0 0 957 19 0 0 25 0 1 0 1797626901 24330240 5175 4294967295 134512640 135094434 3221224432 3221223088 134558286 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14761/statm): 5940 5175 145 145 0 5795 0
[pid=14761] vsize: 23760
Current children cumulated CPU time (s) 9.77
Current children cumulated vsize (Kb) 25884

[startup+20.0038 s]
Raw data (loadavg): 0.94 0.98 0.91 2/57 14761
Raw data (/proc/14757/stat): 14757 (minisat+_script) S 14756 14757 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797626896 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14757/statm): 531 226 485 147 0 384 0
[pid=14757] vsize: 2124
Raw data (/proc/14761/stat): 14761 (minisat+_64-bit) R 14757 14757 22582 0 -1 0 6197 0 0 0 1954 21 0 0 25 0 1 0 1797626901 25337856 5425 4294967295 134512640 135094434 3221224432 3221223044 134563130 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14761/statm): 6186 5425 145 145 0 6041 0
[pid=14761] vsize: 24744
Current children cumulated CPU time (s) 19.76
Current children cumulated vsize (Kb) 26868

[startup+30.0053 s]
Raw data (loadavg): 0.95 0.98 0.91 2/57 14761
Raw data (/proc/14757/stat): 14757 (minisat+_script) S 14756 14757 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797626896 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14757/statm): 531 226 485 147 0 384 0
[pid=14757] vsize: 2124
Raw data (/proc/14761/stat): 14761 (minisat+_64-bit) R 14757 14757 22582 0 -1 0 6438 0 0 0 2951 23 0 0 25 0 1 0 1797626901 26001408 5589 4294967295 134512640 135094434 3221224432 3221223056 134557642 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14761/statm): 6348 5589 145 145 0 6203 0
[pid=14761] vsize: 25392
Current children cumulated CPU time (s) 29.75
Current children cumulated vsize (Kb) 27516

[startup+40.0059 s]
Raw data (loadavg): 0.96 0.98 0.91 2/57 14761
Raw data (/proc/14757/stat): 14757 (minisat+_script) S 14756 14757 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797626896 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14757/statm): 531 226 485 147 0 384 0
[pid=14757] vsize: 2124
Raw data (/proc/14761/stat): 14761 (minisat+_64-bit) R 14757 14757 22582 0 -1 0 6927 0 0 0 3943 26 0 0 25 0 1 0 1797626901 28004352 6078 4294967295 134512640 135094434 3221224432 3221223056 134562146 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14761/statm): 6837 6078 145 145 0 6692 0
[pid=14761] vsize: 27348
Current children cumulated CPU time (s) 39.7
Current children cumulated vsize (Kb) 29472

[startup+50.0064 s]
Raw data (loadavg): 0.96 0.98 0.91 2/57 14761
Raw data (/proc/14757/stat): 14757 (minisat+_script) S 14756 14757 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797626896 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14757/statm): 531 226 485 147 0 384 0
[pid=14757] vsize: 2124
Raw data (/proc/14761/stat): 14761 (minisat+_64-bit) R 14757 14757 22582 0 -1 0 7169 0 0 0 4939 28 0 0 25 0 1 0 1797626901 28835840 6281 4294967295 134512640 135094434 3221224432 3221223076 134562166 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14761/statm): 7040 6281 145 145 0 6895 0
[pid=14761] vsize: 28160
Current children cumulated CPU time (s) 49.68
Current children cumulated vsize (Kb) 30284

[startup+60.007 s]
Raw data (loadavg): 0.97 0.98 0.91 2/57 14761
Raw data (/proc/14757/stat): 14757 (minisat+_script) S 14756 14757 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797626896 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14757/statm): 531 226 485 147 0 384 0
[pid=14757] vsize: 2124
Raw data (/proc/14761/stat): 14761 (minisat+_64-bit) R 14757 14757 22582 0 -1 0 7515 0 0 0 5934 31 0 0 25 0 1 0 1797626901 30363648 6627 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14761/statm): 7413 6627 145 145 0 7268 0
[pid=14761] vsize: 29652
Current children cumulated CPU time (s) 59.66
Current children cumulated vsize (Kb) 31776

[startup+70.0076 s]
Raw data (loadavg): 0.97 0.98 0.91 2/57 14761
Raw data (/proc/14757/stat): 14757 (minisat+_script) S 14756 14757 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797626896 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14757/statm): 531 226 485 147 0 384 0
[pid=14757] vsize: 2124
Raw data (/proc/14761/stat): 14761 (minisat+_64-bit) R 14757 14757 22582 0 -1 0 8016 0 0 0 6926 34 0 0 25 0 1 0 1797626901 32399360 7128 4294967295 134512640 135094434 3221224432 3221223104 134555943 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14761/statm): 7910 7128 145 145 0 7765 0
[pid=14761] vsize: 31640
Current children cumulated CPU time (s) 69.61
Current children cumulated vsize (Kb) 33764

[startup+80.0091 s]
Raw data (loadavg): 0.98 0.98 0.91 2/57 14761
Raw data (/proc/14757/stat): 14757 (minisat+_script) S 14756 14757 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797626896 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14757/statm): 531 226 485 147 0 384 0
[pid=14757] vsize: 2124
Raw data (/proc/14761/stat): 14761 (minisat+_64-bit) R 14757 14757 22582 0 -1 0 8375 0 0 0 7920 36 0 0 25 0 1 0 1797626901 33714176 7452 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14761/statm): 8231 7452 145 145 0 8086 0
[pid=14761] vsize: 32924
Current children cumulated CPU time (s) 79.57
Current children cumulated vsize (Kb) 35048

[startup+90.0097 s]
Raw data (loadavg): 0.98 0.98 0.91 2/57 14761
Raw data (/proc/14757/stat): 14757 (minisat+_script) S 14756 14757 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797626896 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14757/statm): 531 226 485 147 0 384 0
[pid=14757] vsize: 2124
Raw data (/proc/14761/stat): 14761 (minisat+_64-bit) R 14757 14757 22582 0 -1 0 8796 0 0 0 8913 39 0 0 25 0 1 0 1797626901 35409920 7873 4294967295 134512640 135094434 3221224432 3221223088 134558178 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14761/statm): 8645 7873 145 145 0 8500 0
[pid=14761] vsize: 34580
Current children cumulated CPU time (s) 89.53
Current children cumulated vsize (Kb) 36704

[startup+100.009 s]
Raw data (loadavg): 0.98 0.98 0.91 2/57 14761
Raw data (/proc/14757/stat): 14757 (minisat+_script) S 14756 14757 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797626896 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14757/statm): 531 226 485 147 0 384 0
[pid=14757] vsize: 2124
Raw data (/proc/14761/stat): 14761 (minisat+_64-bit) R 14757 14757 22582 0 -1 0 9125 0 0 0 9909 41 0 0 25 0 1 0 1797626901 36749312 8202 4294967295 134512640 135094434 3221224432 3221223024 134557202 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14761/statm): 8972 8202 145 145 0 8827 0
[pid=14761] vsize: 35888
Current children cumulated CPU time (s) 99.51
Current children cumulated vsize (Kb) 38012

[startup+110.01 s]
Raw data (loadavg): 0.98 0.98 0.91 2/57 14761
Raw data (/proc/14757/stat): 14757 (minisat+_script) S 14756 14757 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797626896 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14757/statm): 531 226 485 147 0 384 0
[pid=14757] vsize: 2124
Raw data (/proc/14761/stat): 14761 (minisat+_64-bit) R 14757 14757 22582 0 -1 0 9526 0 0 0 10901 44 0 0 25 0 1 0 1797626901 38371328 8603 4294967295 134512640 135094434 3221224432 3221223024 134557025 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14761/statm): 9368 8603 145 145 0 9223 0
[pid=14761] vsize: 37472
Current children cumulated CPU time (s) 109.46
Current children cumulated vsize (Kb) 39596

[startup+120.01 s]
Raw data (loadavg): 0.99 0.98 0.91 1/57 14761
Raw data (/proc/14757/stat): 14757 (minisat+_script) S 14756 14757 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797626896 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14757/statm): 531 226 485 147 0 384 0
[pid=14757] vsize: 2124
Raw data (/proc/14761/stat): 14761 (minisat+_64-bit) T 14757 14757 22582 0 -1 0 9899 0 0 0 11894 48 0 0 25 0 1 0 1797626901 40136704 8976 4294967295 134512640 135094434 3221224432 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/14761/statm): 9799 8976 145 145 0 9654 0
[pid=14761] vsize: 39196
Current children cumulated CPU time (s) 119.43
Current children cumulated vsize (Kb) 41320

[startup+130.011 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 14761
Raw data (/proc/14757/stat): 14757 (minisat+_script) S 14756 14757 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797626896 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14757/statm): 531 226 485 147 0 384 0
[pid=14757] vsize: 2124
Raw data (/proc/14761/stat): 14761 (minisat+_64-bit) R 14757 14757 22582 0 -1 0 10288 0 0 0 12886 51 0 0 25 0 1 0 1797626901 41709568 9365 4294967295 134512640 135094434 3221224432 3221223088 134557937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14761/statm): 10183 9365 145 145 0 10038 0
[pid=14761] vsize: 40732
Current children cumulated CPU time (s) 129.38
Current children cumulated vsize (Kb) 42856

[startup+140.011 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 14761
Raw data (/proc/14757/stat): 14757 (minisat+_script) S 14756 14757 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797626896 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14757/statm): 531 226 485 147 0 384 0
[pid=14757] vsize: 2124
Raw data (/proc/14761/stat): 14761 (minisat+_64-bit) R 14757 14757 22582 0 -1 0 10640 0 0 0 13880 54 0 0 25 0 1 0 1797626901 43139072 9717 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14761/statm): 10532 9717 145 145 0 10387 0
[pid=14761] vsize: 42128
Current children cumulated CPU time (s) 139.35
Current children cumulated vsize (Kb) 44252

[startup+150.012 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 14761
Raw data (/proc/14757/stat): 14757 (minisat+_script) S 14756 14757 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797626896 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14757/statm): 531 226 485 147 0 384 0
[pid=14757] vsize: 2124
Raw data (/proc/14761/stat): 14761 (minisat+_64-bit) R 14757 14757 22582 0 -1 0 11040 0 0 0 14872 56 0 0 25 0 1 0 1797626901 44761088 10117 4294967295 134512640 135094434 3221224432 3221223088 134557945 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14761/statm): 10928 10117 145 145 0 10783 0
[pid=14761] vsize: 43712
Current children cumulated CPU time (s) 149.29
Current children cumulated vsize (Kb) 45836

[startup+160.013 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 14761
Raw data (/proc/14757/stat): 14757 (minisat+_script) S 14756 14757 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797626896 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14757/statm): 531 226 485 147 0 384 0
[pid=14757] vsize: 2124
Raw data (/proc/14761/stat): 14761 (minisat+_64-bit) R 14757 14757 22582 0 -1 0 11335 0 0 0 15867 59 0 0 25 0 1 0 1797626901 45985792 10412 4294967295 134512640 135094434 3221224432 3221223024 134557263 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14761/statm): 11227 10412 145 145 0 11082 0
[pid=14761] vsize: 44908
Current children cumulated CPU time (s) 159.27
Current children cumulated vsize (Kb) 47032

[startup+170.012 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 14761
Raw data (/proc/14757/stat): 14757 (minisat+_script) S 14756 14757 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797626896 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14757/statm): 531 226 485 147 0 384 0
[pid=14757] vsize: 2124
Raw data (/proc/14761/stat): 14761 (minisat+_64-bit) R 14757 14757 22582 0 -1 0 11977 0 0 0 16859 62 0 0 25 0 1 0 1797626901 48607232 11054 4294967295 134512640 135094434 3221224432 3221223024 134557375 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14761/statm): 11867 11054 145 145 0 11722 0
[pid=14761] vsize: 47468
Current children cumulated CPU time (s) 169.22
Current children cumulated vsize (Kb) 49592

[startup+180.014 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 14761
Raw data (/proc/14757/stat): 14757 (minisat+_script) S 14756 14757 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797626896 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14757/statm): 531 226 485 147 0 384 0
[pid=14757] vsize: 2124
Raw data (/proc/14761/stat): 14761 (minisat+_64-bit) R 14757 14757 22582 0 -1 0 12727 0 0 0 17850 66 0 0 25 0 1 0 1797626901 51675136 11804 4294967295 134512640 135094434 3221224432 3221223024 134557377 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14761/statm): 12616 11804 145 145 0 12471 0
[pid=14761] vsize: 50464
Current children cumulated CPU time (s) 179.17
Current children cumulated vsize (Kb) 52588

[startup+190.014 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 14761
Raw data (/proc/14757/stat): 14757 (minisat+_script) S 14756 14757 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797626896 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14757/statm): 531 226 485 147 0 384 0
[pid=14757] vsize: 2124
Raw data (/proc/14761/stat): 14761 (minisat+_64-bit) R 14757 14757 22582 0 -1 0 13454 0 0 0 18843 70 0 0 25 0 1 0 1797626901 54640640 12531 4294967295 134512640 135094434 3221224432 3221223024 134557025 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14761/statm): 13340 12531 145 145 0 13195 0
[pid=14761] vsize: 53360
Current children cumulated CPU time (s) 189.14
Current children cumulated vsize (Kb) 55484

[startup+200.014 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 14761
Raw data (/proc/14757/stat): 14757 (minisat+_script) S 14756 14757 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797626896 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14757/statm): 531 226 485 147 0 384 0
[pid=14757] vsize: 2124
Raw data (/proc/14761/stat): 14761 (minisat+_64-bit) R 14757 14757 22582 0 -1 0 14159 0 0 0 19834 73 0 0 25 0 1 0 1797626901 57516032 13236 4294967295 134512640 135094434 3221224432 3221223104 134555599 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14761/statm): 14042 13236 145 145 0 13897 0
[pid=14761] vsize: 56168
Current children cumulated CPU time (s) 199.08
Current children cumulated vsize (Kb) 58292

[startup+210.015 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 14761
Raw data (/proc/14757/stat): 14757 (minisat+_script) S 14756 14757 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797626896 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14757/statm): 531 226 485 147 0 384 0
[pid=14757] vsize: 2124
Raw data (/proc/14761/stat): 14761 (minisat+_64-bit) R 14757 14757 22582 0 -1 0 15007 0 0 0 20824 77 0 0 25 0 1 0 1797626901 60985344 14084 4294967295 134512640 135094434 3221224432 3221223024 134556739 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14761/statm): 14889 14084 145 145 0 14744 0
[pid=14761] vsize: 59556
Current children cumulated CPU time (s) 209.02
Current children cumulated vsize (Kb) 61680

[startup+220.015 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 14761
Raw data (/proc/14757/stat): 14757 (minisat+_script) S 14756 14757 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797626896 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14757/statm): 531 226 485 147 0 384 0
[pid=14757] vsize: 2124
Raw data (/proc/14761/stat): 14761 (minisat+_64-bit) R 14757 14757 22582 0 -1 0 15771 0 0 0 21816 81 0 0 25 0 1 0 1797626901 64102400 14848 4294967295 134512640 135094434 3221224432 3221223024 134557407 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14761/statm): 15650 14848 145 145 0 15505 0
[pid=14761] vsize: 62600
Current children cumulated CPU time (s) 218.98
Current children cumulated vsize (Kb) 64724

[startup+230.016 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 14761
Raw data (/proc/14757/stat): 14757 (minisat+_script) S 14756 14757 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797626896 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14757/statm): 531 226 485 147 0 384 0
[pid=14757] vsize: 2124
Raw data (/proc/14761/stat): 14761 (minisat+_64-bit) R 14757 14757 22582 0 -1 0 16457 0 0 0 22809 84 0 0 25 0 1 0 1797626901 66895872 15534 4294967295 134512640 135094434 3221224432 3221223024 134557004 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14761/statm): 16332 15534 145 145 0 16187 0
[pid=14761] vsize: 65328
Current children cumulated CPU time (s) 228.94
Current children cumulated vsize (Kb) 67452

[startup+240.017 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 14761
Raw data (/proc/14757/stat): 14757 (minisat+_script) S 14756 14757 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797626896 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14757/statm): 531 226 485 147 0 384 0
[pid=14757] vsize: 2124
Raw data (/proc/14761/stat): 14761 (minisat+_64-bit) R 14757 14757 22582 0 -1 0 17120 0 0 0 23801 89 0 0 25 0 1 0 1797626901 69603328 16197 4294967295 134512640 135094434 3221224432 3221223024 134556975 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14761/statm): 16993 16197 145 145 0 16848 0
[pid=14761] vsize: 67972
Current children cumulated CPU time (s) 238.91
Current children cumulated vsize (Kb) 70096

[startup+250.017 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 14761
Raw data (/proc/14757/stat): 14757 (minisat+_script) S 14756 14757 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797626896 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14757/statm): 531 226 485 147 0 384 0
[pid=14757] vsize: 2124
Raw data (/proc/14761/stat): 14761 (minisat+_64-bit) R 14757 14757 22582 0 -1 0 17580 0 0 0 24796 91 0 0 25 0 1 0 1797626901 71483392 16657 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14761/statm): 17452 16657 145 145 0 17307 0
[pid=14761] vsize: 69808
Current children cumulated CPU time (s) 248.88
Current children cumulated vsize (Kb) 71932

[startup+260.017 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 14761
Raw data (/proc/14757/stat): 14757 (minisat+_script) S 14756 14757 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797626896 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14757/statm): 531 226 485 147 0 384 0
[pid=14757] vsize: 2124
Raw data (/proc/14761/stat): 14761 (minisat+_64-bit) R 14757 14757 22582 0 -1 0 17809 0 0 0 25793 93 0 0 25 0 1 0 1797626901 72417280 16886 4294967295 134512640 135094434 3221224432 3221223088 134557896 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14761/statm): 17680 16886 145 145 0 17535 0
[pid=14761] vsize: 70720
Current children cumulated CPU time (s) 258.87
Current children cumulated vsize (Kb) 72844

[startup+270.018 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 14761
Raw data (/proc/14757/stat): 14757 (minisat+_script) S 14756 14757 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797626896 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14757/statm): 531 226 485 147 0 384 0
[pid=14757] vsize: 2124
Raw data (/proc/14761/stat): 14761 (minisat+_64-bit) R 14757 14757 22582 0 -1 0 18344 0 0 0 26783 97 0 0 25 0 1 0 1797626901 74596352 17421 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14761/statm): 18212 17421 145 145 0 18067 0
[pid=14761] vsize: 72848
Current children cumulated CPU time (s) 268.81
Current children cumulated vsize (Kb) 74972

[startup+280.018 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 14761
Raw data (/proc/14757/stat): 14757 (minisat+_script) S 14756 14757 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797626896 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14757/statm): 531 226 485 147 0 384 0
[pid=14757] vsize: 2124
Raw data (/proc/14761/stat): 14761 (minisat+_64-bit) R 14757 14757 22582 0 -1 0 18972 0 0 0 27775 101 0 0 25 0 1 0 1797626901 77156352 18049 4294967295 134512640 135094434 3221224432 3221223092 134553536 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14761/statm): 18837 18049 145 145 0 18692 0
[pid=14761] vsize: 75348
Current children cumulated CPU time (s) 278.77
Current children cumulated vsize (Kb) 77472

[startup+290.019 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 14761
Raw data (/proc/14757/stat): 14757 (minisat+_script) S 14756 14757 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797626896 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14757/statm): 531 226 485 147 0 384 0
[pid=14757] vsize: 2124
Raw data (/proc/14761/stat): 14761 (minisat+_64-bit) R 14757 14757 22582 0 -1 0 19266 0 0 0 28770 103 0 0 25 0 1 0 1797626901 78364672 18343 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14761/statm): 19132 18343 145 145 0 18987 0
[pid=14761] vsize: 76528
Current children cumulated CPU time (s) 288.74
Current children cumulated vsize (Kb) 78652

[startup+300.018 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 14761
Raw data (/proc/14757/stat): 14757 (minisat+_script) S 14756 14757 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797626896 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14757/statm): 531 226 485 147 0 384 0
[pid=14757] vsize: 2124
Raw data (/proc/14761/stat): 14761 (minisat+_64-bit) R 14757 14757 22582 0 -1 0 19540 0 0 0 29766 105 0 0 25 0 1 0 1797626901 79462400 18617 4294967295 134512640 135094434 3221224432 3221223024 134557244 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14761/statm): 19400 18617 145 145 0 19255 0
[pid=14761] vsize: 77600
Current children cumulated CPU time (s) 298.72
Current children cumulated vsize (Kb) 79724

[startup+310.019 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 14761
Raw data (/proc/14757/stat): 14757 (minisat+_script) S 14756 14757 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797626896 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14757/statm): 531 226 485 147 0 384 0
[pid=14757] vsize: 2124
Raw data (/proc/14761/stat): 14761 (minisat+_64-bit) R 14757 14757 22582 0 -1 0 19883 0 0 0 30760 107 0 0 25 0 1 0 1797626901 80859136 18960 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14761/statm): 19741 18960 145 145 0 19596 0
[pid=14761] vsize: 78964
Current children cumulated CPU time (s) 308.68
Current children cumulated vsize (Kb) 81088

[startup+320.019 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 14761
Raw data (/proc/14757/stat): 14757 (minisat+_script) S 14756 14757 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797626896 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14757/statm): 531 226 485 147 0 384 0
[pid=14757] vsize: 2124
Raw data (/proc/14761/stat): 14761 (minisat+_64-bit) R 14757 14757 22582 0 -1 0 20144 0 0 0 31755 109 0 0 25 0 1 0 1797626901 81911808 19221 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14761/statm): 19998 19221 145 145 0 19853 0
[pid=14761] vsize: 79992
Current children cumulated CPU time (s) 318.65
Current children cumulated vsize (Kb) 82116

[startup+330.021 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 14761
Raw data (/proc/14757/stat): 14757 (minisat+_script) S 14756 14757 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797626896 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14757/statm): 531 226 485 147 0 384 0
[pid=14757] vsize: 2124
Raw data (/proc/14761/stat): 14761 (minisat+_64-bit) R 14757 14757 22582 0 -1 0 20457 0 0 0 32748 112 0 0 25 0 1 0 1797626901 83185664 19534 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14761/statm): 20309 19534 145 145 0 20164 0
[pid=14761] vsize: 81236
Current children cumulated CPU time (s) 328.61
Current children cumulated vsize (Kb) 83360

[startup+340.022 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 14761
Raw data (/proc/14757/stat): 14757 (minisat+_script) S 14756 14757 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797626896 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14757/statm): 531 226 485 147 0 384 0
[pid=14757] vsize: 2124
Raw data (/proc/14761/stat): 14761 (minisat+_64-bit) R 14757 14757 22582 0 -1 0 20709 0 0 0 33743 114 0 0 25 0 1 0 1797626901 84217856 19786 4294967295 134512640 135094434 3221224432 3221223024 134551908 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14761/statm): 20561 19786 145 145 0 20416 0
[pid=14761] vsize: 82244
Current children cumulated CPU time (s) 338.58
Current children cumulated vsize (Kb) 84368

[startup+350.022 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 14761
Raw data (/proc/14757/stat): 14757 (minisat+_script) S 14756 14757 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797626896 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14757/statm): 531 226 485 147 0 384 0
[pid=14757] vsize: 2124
Raw data (/proc/14761/stat): 14761 (minisat+_64-bit) R 14757 14757 22582 0 -1 0 20910 0 0 0 34740 117 0 0 25 0 1 0 1797626901 85028864 19987 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14761/statm): 20759 19987 145 145 0 20614 0
[pid=14761] vsize: 83036
Current children cumulated CPU time (s) 348.58
Current children cumulated vsize (Kb) 85160

[startup+360.023 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 14761
Raw data (/proc/14757/stat): 14757 (minisat+_script) S 14756 14757 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797626896 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14757/statm): 531 226 485 147 0 384 0
[pid=14757] vsize: 2124
Raw data (/proc/14761/stat): 14761 (minisat+_64-bit) R 14757 14757 22582 0 -1 0 21098 0 0 0 35737 118 0 0 25 0 1 0 1797626901 86343680 20175 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14761/statm): 21080 20175 145 145 0 20935 0
[pid=14761] vsize: 84320
Current children cumulated CPU time (s) 358.56
Current children cumulated vsize (Kb) 86444

[startup+370.022 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 14761
Raw data (/proc/14757/stat): 14757 (minisat+_script) S 14756 14757 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797626896 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14757/statm): 531 226 485 147 0 384 0
[pid=14757] vsize: 2124
Raw data (/proc/14761/stat): 14761 (minisat+_64-bit) R 14757 14757 22582 0 -1 0 21356 0 0 0 36732 120 0 0 25 0 1 0 1797626901 87379968 20433 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14761/statm): 21333 20433 145 145 0 21188 0
[pid=14761] vsize: 85332
Current children cumulated CPU time (s) 368.53
Current children cumulated vsize (Kb) 87456

[startup+380.023 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 14761
Raw data (/proc/14757/stat): 14757 (minisat+_script) S 14756 14757 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797626896 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14757/statm): 531 226 485 147 0 384 0
[pid=14757] vsize: 2124
Raw data (/proc/14761/stat): 14761 (minisat+_64-bit) T 14757 14757 22582 0 -1 0 21752 0 0 0 37726 122 0 0 25 0 1 0 1797626901 88981504 20829 4294967295 134512640 135094434 3221224432 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/14761/statm): 21724 20829 145 145 0 21579 0
[pid=14761] vsize: 86896
Current children cumulated CPU time (s) 378.49
Current children cumulated vsize (Kb) 89020

[startup+390.023 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 14761
Raw data (/proc/14757/stat): 14757 (minisat+_script) S 14756 14757 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797626896 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14757/statm): 531 226 485 147 0 384 0
[pid=14757] vsize: 2124
Raw data (/proc/14761/stat): 14761 (minisat+_64-bit) R 14757 14757 22582 0 -1 0 22403 0 0 0 38715 127 0 0 25 0 1 0 1797626901 91635712 21480 4294967295 134512640 135094434 3221224432 3221223024 134557500 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14761/statm): 22372 21480 145 145 0 22227 0
[pid=14761] vsize: 89488
Current children cumulated CPU time (s) 388.43
Current children cumulated vsize (Kb) 91612

[startup+400.023 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 14761
Raw data (/proc/14757/stat): 14757 (minisat+_script) S 14756 14757 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797626896 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14757/statm): 531 226 485 147 0 384 0
[pid=14757] vsize: 2124
Raw data (/proc/14761/stat): 14761 (minisat+_64-bit) R 14757 14757 22582 0 -1 0 23091 0 0 0 39704 131 0 0 25 0 1 0 1797626901 94445568 22168 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14761/statm): 23058 22168 145 145 0 22913 0
[pid=14761] vsize: 92232
Current children cumulated CPU time (s) 398.36
Current children cumulated vsize (Kb) 94356

[startup+410.024 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 14761
Raw data (/proc/14757/stat): 14757 (minisat+_script) S 14756 14757 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797626896 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14757/statm): 531 226 485 147 0 384 0
[pid=14757] vsize: 2124
Raw data (/proc/14761/stat): 14761 (minisat+_64-bit) R 14757 14757 22582 0 -1 0 23763 0 0 0 40696 134 0 0 25 0 1 0 1797626901 97189888 22840 4294967295 134512640 135094434 3221224432 3221223024 134557219 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14761/statm): 23728 22840 145 145 0 23583 0
[pid=14761] vsize: 94912
Current children cumulated CPU time (s) 408.31
Current children cumulated vsize (Kb) 97036

[startup+420.024 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 14761
Raw data (/proc/14757/stat): 14757 (minisat+_script) S 14756 14757 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797626896 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14757/statm): 531 226 485 147 0 384 0
[pid=14757] vsize: 2124
Raw data (/proc/14761/stat): 14761 (minisat+_64-bit) R 14757 14757 22582 0 -1 0 24421 0 0 0 41685 138 0 0 25 0 1 0 1797626901 99872768 23498 4294967295 134512640 135094434 3221224432 3221223088 134558218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14761/statm): 24383 23498 145 145 0 24238 0
[pid=14761] vsize: 97532
Current children cumulated CPU time (s) 418.24
Current children cumulated vsize (Kb) 99656

[startup+430.025 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 14761
Raw data (/proc/14757/stat): 14757 (minisat+_script) S 14756 14757 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797626896 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14757/statm): 531 226 485 147 0 384 0
[pid=14757] vsize: 2124
Raw data (/proc/14761/stat): 14761 (minisat+_64-bit) R 14757 14757 22582 0 -1 0 25096 0 0 0 42675 142 0 0 25 0 1 0 1797626901 102633472 24173 4294967295 134512640 135094434 3221224432 3221223024 134557435 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14761/statm): 25057 24173 145 145 0 24912 0
[pid=14761] vsize: 100228
Current children cumulated CPU time (s) 428.18
Current children cumulated vsize (Kb) 102352

[startup+440.025 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 14761
Raw data (/proc/14757/stat): 14757 (minisat+_script) S 14756 14757 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797626896 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14757/statm): 531 226 485 147 0 384 0
[pid=14757] vsize: 2124
Raw data (/proc/14761/stat): 14761 (minisat+_64-bit) R 14757 14757 22582 0 -1 0 25456 0 0 0 43670 145 0 0 25 0 1 0 1797626901 104112128 24533 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14761/statm): 25418 24533 145 145 0 25273 0
[pid=14761] vsize: 101672
Current children cumulated CPU time (s) 438.16
Current children cumulated vsize (Kb) 103796

[startup+450.026 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 14761
Raw data (/proc/14757/stat): 14757 (minisat+_script) S 14756 14757 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797626896 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14757/statm): 531 226 485 147 0 384 0
[pid=14757] vsize: 2124
Raw data (/proc/14761/stat): 14761 (minisat+_64-bit) R 14757 14757 22582 0 -1 0 25636 0 0 0 44667 146 0 0 25 0 1 0 1797626901 104837120 24713 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14761/statm): 25595 24713 145 145 0 25450 0
[pid=14761] vsize: 102380
Current children cumulated CPU time (s) 448.14
Current children cumulated vsize (Kb) 104504

[startup+460.026 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 14761
Raw data (/proc/14757/stat): 14757 (minisat+_script) S 14756 14757 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797626896 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14757/statm): 531 226 485 147 0 384 0
[pid=14757] vsize: 2124
Raw data (/proc/14761/stat): 14761 (minisat+_64-bit) R 14757 14757 22582 0 -1 0 25944 0 0 0 45662 148 0 0 25 0 1 0 1797626901 106086400 25021 4294967295 134512640 135094434 3221224432 3221223024 134557219 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14761/statm): 25900 25021 145 145 0 25755 0
[pid=14761] vsize: 103600
Current children cumulated CPU time (s) 458.11
Current children cumulated vsize (Kb) 105724

[startup+470.027 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 14761
Raw data (/proc/14757/stat): 14757 (minisat+_script) S 14756 14757 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797626896 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14757/statm): 531 226 485 147 0 384 0
[pid=14757] vsize: 2124
Raw data (/proc/14761/stat): 14761 (minisat+_64-bit) R 14757 14757 22582 0 -1 0 26601 0 0 0 46652 152 0 0 25 0 1 0 1797626901 108765184 25678 4294967295 134512640 135094434 3221224432 3221223088 134558016 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14761/statm): 26554 25678 145 145 0 26409 0
[pid=14761] vsize: 106216
Current children cumulated CPU time (s) 468.05
Current children cumulated vsize (Kb) 108340

[startup+480.027 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 14761
Raw data (/proc/14757/stat): 14757 (minisat+_script) S 14756 14757 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797626896 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14757/statm): 531 226 485 147 0 384 0
[pid=14757] vsize: 2124
Raw data (/proc/14761/stat): 14761 (minisat+_64-bit) R 14757 14757 22582 0 -1 0 27303 0 0 0 47644 154 0 0 25 0 1 0 1797626901 111636480 26380 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14761/statm): 27255 26380 145 145 0 27110 0
[pid=14761] vsize: 109020
Current children cumulated CPU time (s) 477.99
Current children cumulated vsize (Kb) 111144

[startup+490.028 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 14761
Raw data (/proc/14757/stat): 14757 (minisat+_script) S 14756 14757 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797626896 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14757/statm): 531 226 485 147 0 384 0
[pid=14757] vsize: 2124
Raw data (/proc/14761/stat): 14761 (minisat+_64-bit) R 14757 14757 22582 0 -1 0 27990 0 0 0 48634 159 0 0 25 0 1 0 1797626901 114446336 27067 4294967295 134512640 135094434 3221224432 3221223024 134557357 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14761/statm): 27941 27067 145 145 0 27796 0
[pid=14761] vsize: 111764
Current children cumulated CPU time (s) 487.94
Current children cumulated vsize (Kb) 113888

[startup+500.028 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 14761
Raw data (/proc/14757/stat): 14757 (minisat+_script) S 14756 14757 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797626896 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14757/statm): 531 226 485 147 0 384 0
[pid=14757] vsize: 2124
Raw data (/proc/14761/stat): 14761 (minisat+_64-bit) R 14757 14757 22582 0 -1 0 28648 0 0 0 49624 163 0 0 25 0 1 0 1797626901 117133312 27725 4294967295 134512640 135094434 3221224432 3221223024 134557199 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14761/statm): 28597 27725 145 145 0 28452 0
[pid=14761] vsize: 114388
Current children cumulated CPU time (s) 497.88
Current children cumulated vsize (Kb) 116512

[startup+510.028 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 14761
Raw data (/proc/14757/stat): 14757 (minisat+_script) S 14756 14757 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797626896 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14757/statm): 531 226 485 147 0 384 0
[pid=14757] vsize: 2124
Raw data (/proc/14761/stat): 14761 (minisat+_64-bit) R 14757 14757 22582 0 -1 0 29214 0 0 0 50616 166 0 0 25 0 1 0 1797626901 119447552 28291 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14761/statm): 29162 28291 145 145 0 29017 0
[pid=14761] vsize: 116648
Current children cumulated CPU time (s) 507.83
Current children cumulated vsize (Kb) 118772

[startup+520.029 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 14761
Raw data (/proc/14757/stat): 14757 (minisat+_script) S 14756 14757 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797626896 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14757/statm): 531 226 485 147 0 384 0
[pid=14757] vsize: 2124
Raw data (/proc/14761/stat): 14761 (minisat+_64-bit) R 14757 14757 22582 0 -1 0 29750 0 0 0 51610 168 0 0 25 0 1 0 1797626901 121475072 28788 4294967295 134512640 135094434 3221224432 3221222224 134562886 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14761/statm): 29657 28788 145 145 0 29512 0
[pid=14761] vsize: 118628
Current children cumulated CPU time (s) 517.79
Current children cumulated vsize (Kb) 120752

[startup+530.029 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 14761
Raw data (/proc/14757/stat): 14757 (minisat+_script) S 14756 14757 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797626896 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14757/statm): 531 226 485 147 0 384 0
[pid=14757] vsize: 2124
Raw data (/proc/14761/stat): 14761 (minisat+_64-bit) R 14757 14757 22582 0 -1 0 29750 0 0 0 52608 169 0 0 25 0 1 0 1797626901 121475072 28788 4294967295 134512640 135094434 3221224432 3221223084 134675707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14761/statm): 29657 28788 145 145 0 29512 0
[pid=14761] vsize: 118628
Current children cumulated CPU time (s) 527.78
Current children cumulated vsize (Kb) 120752

[startup+540.03 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 14761
Raw data (/proc/14757/stat): 14757 (minisat+_script) S 14756 14757 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797626896 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14757/statm): 531 226 485 147 0 384 0
[pid=14757] vsize: 2124
Raw data (/proc/14761/stat): 14761 (minisat+_64-bit) R 14757 14757 22582 0 -1 0 29750 0 0 0 53608 169 0 0 25 0 1 0 1797626901 121475072 28788 4294967295 134512640 135094434 3221224432 3221223024 134556773 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14761/statm): 29657 28788 145 145 0 29512 0
[pid=14761] vsize: 118628
Current children cumulated CPU time (s) 537.78
Current children cumulated vsize (Kb) 120752

[startup+550.029 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 14761
Raw data (/proc/14757/stat): 14757 (minisat+_script) S 14756 14757 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797626896 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14757/statm): 531 226 485 147 0 384 0
[pid=14757] vsize: 2124
Raw data (/proc/14761/stat): 14761 (minisat+_64-bit) R 14757 14757 22582 0 -1 0 29750 0 0 0 54608 169 0 0 25 0 1 0 1797626901 121475072 28788 4294967295 134512640 135094434 3221224432 3221223104 134556071 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14761/statm): 29657 28788 145 145 0 29512 0
[pid=14761] vsize: 118628
Current children cumulated CPU time (s) 547.78
Current children cumulated vsize (Kb) 120752

[startup+560.03 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 14761
Raw data (/proc/14757/stat): 14757 (minisat+_script) S 14756 14757 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797626896 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14757/statm): 531 226 485 147 0 384 0
[pid=14757] vsize: 2124
Raw data (/proc/14761/stat): 14761 (minisat+_64-bit) R 14757 14757 22582 0 -1 0 29750 0 0 0 55609 169 0 0 25 0 1 0 1797626901 121475072 28788 4294967295 134512640 135094434 3221224432 3221223092 134553491 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14761/statm): 29657 28788 145 145 0 29512 0
[pid=14761] vsize: 118628
Current children cumulated CPU time (s) 557.79
Current children cumulated vsize (Kb) 120752

[startup+570.03 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 14761
Raw data (/proc/14757/stat): 14757 (minisat+_script) S 14756 14757 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797626896 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14757/statm): 531 226 485 147 0 384 0
[pid=14757] vsize: 2124
Raw data (/proc/14761/stat): 14761 (minisat+_64-bit) R 14757 14757 22582 0 -1 0 29751 0 0 0 56609 169 0 0 25 0 1 0 1797626901 121475072 28789 4294967295 134512640 135094434 3221224432 3221223068 134557560 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14761/statm): 29657 28789 145 145 0 29512 0
[pid=14761] vsize: 118628
Current children cumulated CPU time (s) 567.79
Current children cumulated vsize (Kb) 120752

[startup+580.031 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 14761
Raw data (/proc/14757/stat): 14757 (minisat+_script) S 14756 14757 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797626896 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14757/statm): 531 226 485 147 0 384 0
[pid=14757] vsize: 2124
Raw data (/proc/14761/stat): 14761 (minisat+_64-bit) R 14757 14757 22582 0 -1 0 29751 0 0 0 57609 169 0 0 25 0 1 0 1797626901 121475072 28789 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14761/statm): 29657 28789 145 145 0 29512 0
[pid=14761] vsize: 118628
Current children cumulated CPU time (s) 577.79
Current children cumulated vsize (Kb) 120752

[startup+590.032 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 14761
Raw data (/proc/14757/stat): 14757 (minisat+_script) S 14756 14757 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797626896 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14757/statm): 531 226 485 147 0 384 0
[pid=14757] vsize: 2124
Raw data (/proc/14761/stat): 14761 (minisat+_64-bit) R 14757 14757 22582 0 -1 0 29751 0 0 0 58609 169 0 0 25 0 1 0 1797626901 121475072 28789 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14761/statm): 29657 28789 145 145 0 29512 0
[pid=14761] vsize: 118628
Current children cumulated CPU time (s) 587.79
Current children cumulated vsize (Kb) 120752

[startup+600.032 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 14761
Raw data (/proc/14757/stat): 14757 (minisat+_script) S 14756 14757 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797626896 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14757/statm): 531 226 485 147 0 384 0
[pid=14757] vsize: 2124
Raw data (/proc/14761/stat): 14761 (minisat+_64-bit) R 14757 14757 22582 0 -1 0 29751 0 0 0 59609 169 0 0 25 0 1 0 1797626901 121475072 28789 4294967295 134512640 135094434 3221224432 3221223024 134557273 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14761/statm): 29657 28789 145 145 0 29512 0
[pid=14761] vsize: 118628
Current children cumulated CPU time (s) 597.79
Current children cumulated vsize (Kb) 120752

[startup+610.033 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 14761
Raw data (/proc/14757/stat): 14757 (minisat+_script) S 14756 14757 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797626896 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14757/statm): 531 226 485 147 0 384 0
[pid=14757] vsize: 2124
Raw data (/proc/14761/stat): 14761 (minisat+_64-bit) R 14757 14757 22582 0 -1 0 29751 0 0 0 60610 169 0 0 25 0 1 0 1797626901 121475072 28789 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14761/statm): 29657 28789 145 145 0 29512 0
[pid=14761] vsize: 118628
Current children cumulated CPU time (s) 607.8
Current children cumulated vsize (Kb) 120752

[startup+620.033 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 14761
Raw data (/proc/14757/stat): 14757 (minisat+_script) S 14756 14757 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797626896 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14757/statm): 531 226 485 147 0 384 0
[pid=14757] vsize: 2124
Raw data (/proc/14761/stat): 14761 (minisat+_64-bit) R 14757 14757 22582 0 -1 0 29751 0 0 0 61610 169 0 0 25 0 1 0 1797626901 121475072 28789 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14761/statm): 29657 28789 145 145 0 29512 0
[pid=14761] vsize: 118628
Current children cumulated CPU time (s) 617.8
Current children cumulated vsize (Kb) 120752

[startup+630.035 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 14761
Raw data (/proc/14757/stat): 14757 (minisat+_script) S 14756 14757 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797626896 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14757/statm): 531 226 485 147 0 384 0
[pid=14757] vsize: 2124
Raw data (/proc/14761/stat): 14761 (minisat+_64-bit) R 14757 14757 22582 0 -1 0 29751 0 0 0 62610 169 0 0 25 0 1 0 1797626901 121475072 28789 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14761/statm): 29657 28789 145 145 0 29512 0
[pid=14761] vsize: 118628
Current children cumulated CPU time (s) 627.8
Current children cumulated vsize (Kb) 120752

[startup+640.035 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 14761
Raw data (/proc/14757/stat): 14757 (minisat+_script) S 14756 14757 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797626896 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14757/statm): 531 226 485 147 0 384 0
[pid=14757] vsize: 2124
Raw data (/proc/14761/stat): 14761 (minisat+_64-bit) R 14757 14757 22582 0 -1 0 29751 0 0 0 63610 169 0 0 25 0 1 0 1797626901 121475072 28789 4294967295 134512640 135094434 3221224432 3221223024 134556802 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14761/statm): 29657 28789 145 145 0 29512 0
[pid=14761] vsize: 118628
Current children cumulated CPU time (s) 637.8
Current children cumulated vsize (Kb) 120752

[startup+650.035 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 14761
Raw data (/proc/14757/stat): 14757 (minisat+_script) S 14756 14757 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797626896 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14757/statm): 531 226 485 147 0 384 0
[pid=14757] vsize: 2124
Raw data (/proc/14761/stat): 14761 (minisat+_64-bit) R 14757 14757 22582 0 -1 0 29751 0 0 0 64610 169 0 0 25 0 1 0 1797626901 121475072 28789 4294967295 134512640 135094434 3221224432 3221223024 134551908 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14761/statm): 29657 28789 145 145 0 29512 0
[pid=14761] vsize: 118628
Current children cumulated CPU time (s) 647.8
Current children cumulated vsize (Kb) 120752

[startup+660.035 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 14761
Raw data (/proc/14757/stat): 14757 (minisat+_script) S 14756 14757 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797626896 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14757/statm): 531 226 485 147 0 384 0
[pid=14757] vsize: 2124
Raw data (/proc/14761/stat): 14761 (minisat+_64-bit) R 14757 14757 22582 0 -1 0 29751 0 0 0 65611 169 0 0 25 0 1 0 1797626901 121475072 28789 4294967295 134512640 135094434 3221224432 3221223056 134557711 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14761/statm): 29657 28789 145 145 0 29512 0
[pid=14761] vsize: 118628
Current children cumulated CPU time (s) 657.81
Current children cumulated vsize (Kb) 120752

[startup+670.036 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 14761
Raw data (/proc/14757/stat): 14757 (minisat+_script) S 14756 14757 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797626896 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14757/statm): 531 226 485 147 0 384 0
[pid=14757] vsize: 2124
Raw data (/proc/14761/stat): 14761 (minisat+_64-bit) R 14757 14757 22582 0 -1 0 29751 0 0 0 66611 169 0 0 25 0 1 0 1797626901 121475072 28789 4294967295 134512640 135094434 3221224432 3221223056 134557606 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14761/statm): 29657 28789 145 145 0 29512 0
[pid=14761] vsize: 118628
Current children cumulated CPU time (s) 667.81
Current children cumulated vsize (Kb) 120752

[startup+680.037 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 14761
Raw data (/proc/14757/stat): 14757 (minisat+_script) S 14756 14757 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797626896 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14757/statm): 531 226 485 147 0 384 0
[pid=14757] vsize: 2124
Raw data (/proc/14761/stat): 14761 (minisat+_64-bit) R 14757 14757 22582 0 -1 0 29751 0 0 0 67611 169 0 0 25 0 1 0 1797626901 121475072 28789 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14761/statm): 29657 28789 145 145 0 29512 0
[pid=14761] vsize: 118628
Current children cumulated CPU time (s) 677.81
Current children cumulated vsize (Kb) 120752

[startup+690.038 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 14761
Raw data (/proc/14757/stat): 14757 (minisat+_script) S 14756 14757 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797626896 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14757/statm): 531 226 485 147 0 384 0
[pid=14757] vsize: 2124
Raw data (/proc/14761/stat): 14761 (minisat+_64-bit) R 14757 14757 22582 0 -1 0 29751 0 0 0 68611 169 0 0 25 0 1 0 1797626901 121475072 28789 4294967295 134512640 135094434 3221224432 3221223024 134557518 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14761/statm): 29657 28789 145 145 0 29512 0
[pid=14761] vsize: 118628
Current children cumulated CPU time (s) 687.81
Current children cumulated vsize (Kb) 120752

[startup+700.038 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 14761
Raw data (/proc/14757/stat): 14757 (minisat+_script) S 14756 14757 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797626896 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14757/statm): 531 226 485 147 0 384 0
[pid=14757] vsize: 2124
Raw data (/proc/14761/stat): 14761 (minisat+_64-bit) R 14757 14757 22582 0 -1 0 29751 0 0 0 69612 169 0 0 25 0 1 0 1797626901 121475072 28789 4294967295 134512640 135094434 3221224432 3221223024 134557319 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14761/statm): 29657 28789 145 145 0 29512 0
[pid=14761] vsize: 118628
Current children cumulated CPU time (s) 697.82
Current children cumulated vsize (Kb) 120752

[startup+710.038 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 14761
Raw data (/proc/14757/stat): 14757 (minisat+_script) S 14756 14757 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797626896 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14757/statm): 531 226 485 147 0 384 0
[pid=14757] vsize: 2124
Raw data (/proc/14761/stat): 14761 (minisat+_64-bit) R 14757 14757 22582 0 -1 0 29751 0 0 0 70612 169 0 0 25 0 1 0 1797626901 121475072 28789 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14761/statm): 29657 28789 145 145 0 29512 0
[pid=14761] vsize: 118628
Current children cumulated CPU time (s) 707.82
Current children cumulated vsize (Kb) 120752

[startup+720.039 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 14761
Raw data (/proc/14757/stat): 14757 (minisat+_script) S 14756 14757 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797626896 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14757/statm): 531 226 485 147 0 384 0
[pid=14757] vsize: 2124
Raw data (/proc/14761/stat): 14761 (minisat+_64-bit) R 14757 14757 22582 0 -1 0 29751 0 0 0 71612 169 0 0 25 0 1 0 1797626901 121475072 28789 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14761/statm): 29657 28789 145 145 0 29512 0
[pid=14761] vsize: 118628
Current children cumulated CPU time (s) 717.82
Current children cumulated vsize (Kb) 120752

[startup+730.039 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 14761
Raw data (/proc/14757/stat): 14757 (minisat+_script) S 14756 14757 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797626896 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14757/statm): 531 226 485 147 0 384 0
[pid=14757] vsize: 2124
Raw data (/proc/14761/stat): 14761 (minisat+_64-bit) R 14757 14757 22582 0 -1 0 29752 0 0 0 72612 169 0 0 25 0 1 0 1797626901 121475072 28790 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14761/statm): 29657 28790 145 145 0 29512 0
[pid=14761] vsize: 118628
Current children cumulated CPU time (s) 727.82
Current children cumulated vsize (Kb) 120752

[startup+740.04 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 14761
Raw data (/proc/14757/stat): 14757 (minisat+_script) S 14756 14757 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797626896 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14757/statm): 531 226 485 147 0 384 0
[pid=14757] vsize: 2124
Raw data (/proc/14761/stat): 14761 (minisat+_64-bit) R 14757 14757 22582 0 -1 0 29752 0 0 0 73613 169 0 0 25 0 1 0 1797626901 121475072 28790 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14761/statm): 29657 28790 145 145 0 29512 0
[pid=14761] vsize: 118628
Current children cumulated CPU time (s) 737.83
Current children cumulated vsize (Kb) 120752

[startup+750.04 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 14761
Raw data (/proc/14757/stat): 14757 (minisat+_script) S 14756 14757 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797626896 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14757/statm): 531 226 485 147 0 384 0
[pid=14757] vsize: 2124
Raw data (/proc/14761/stat): 14761 (minisat+_64-bit) R 14757 14757 22582 0 -1 0 29752 0 0 0 74613 169 0 0 25 0 1 0 1797626901 121475072 28790 4294967295 134512640 135094434 3221224432 3221223120 134554733 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14761/statm): 29657 28790 145 145 0 29512 0
[pid=14761] vsize: 118628
Current children cumulated CPU time (s) 747.83
Current children cumulated vsize (Kb) 120752

[startup+760.041 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 14761
Raw data (/proc/14757/stat): 14757 (minisat+_script) S 14756 14757 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797626896 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14757/statm): 531 226 485 147 0 384 0
[pid=14757] vsize: 2124
Raw data (/proc/14761/stat): 14761 (minisat+_64-bit) R 14757 14757 22582 0 -1 0 29752 0 0 0 75613 169 0 0 25 0 1 0 1797626901 121475072 28790 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14761/statm): 29657 28790 145 145 0 29512 0
[pid=14761] vsize: 118628
Current children cumulated CPU time (s) 757.83
Current children cumulated vsize (Kb) 120752

[startup+770.042 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 14761
Raw data (/proc/14757/stat): 14757 (minisat+_script) S 14756 14757 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797626896 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14757/statm): 531 226 485 147 0 384 0
[pid=14757] vsize: 2124
Raw data (/proc/14761/stat): 14761 (minisat+_64-bit) R 14757 14757 22582 0 -1 0 29752 0 0 0 76613 169 0 0 25 0 1 0 1797626901 121475072 28790 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14761/statm): 29657 28790 145 145 0 29512 0
[pid=14761] vsize: 118628
Current children cumulated CPU time (s) 767.83
Current children cumulated vsize (Kb) 120752

[startup+780.042 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 14761
Raw data (/proc/14757/stat): 14757 (minisat+_script) S 14756 14757 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797626896 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14757/statm): 531 226 485 147 0 384 0
[pid=14757] vsize: 2124
Raw data (/proc/14761/stat): 14761 (minisat+_64-bit) R 14757 14757 22582 0 -1 0 29752 0 0 0 77614 169 0 0 25 0 1 0 1797626901 121475072 28790 4294967295 134512640 135094434 3221224432 3221223056 134557717 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14761/statm): 29657 28790 145 145 0 29512 0
[pid=14761] vsize: 118628
Current children cumulated CPU time (s) 777.84
Current children cumulated vsize (Kb) 120752

[startup+790.043 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 14761
Raw data (/proc/14757/stat): 14757 (minisat+_script) S 14756 14757 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797626896 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14757/statm): 531 226 485 147 0 384 0
[pid=14757] vsize: 2124
Raw data (/proc/14761/stat): 14761 (minisat+_64-bit) R 14757 14757 22582 0 -1 0 29752 0 0 0 78614 169 0 0 25 0 1 0 1797626901 121475072 28790 4294967295 134512640 135094434 3221224432 3221223056 134557737 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14761/statm): 29657 28790 145 145 0 29512 0
[pid=14761] vsize: 118628
Current children cumulated CPU time (s) 787.84
Current children cumulated vsize (Kb) 120752

[startup+800.042 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 14761
Raw data (/proc/14757/stat): 14757 (minisat+_script) S 14756 14757 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797626896 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14757/statm): 531 226 485 147 0 384 0
[pid=14757] vsize: 2124
Raw data (/proc/14761/stat): 14761 (minisat+_64-bit) R 14757 14757 22582 0 -1 0 29752 0 0 0 79614 169 0 0 25 0 1 0 1797626901 121475072 28790 4294967295 134512640 135094434 3221224432 3221223024 134557416 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14761/statm): 29657 28790 145 145 0 29512 0
[pid=14761] vsize: 118628
Current children cumulated CPU time (s) 797.84
Current children cumulated vsize (Kb) 120752

[startup+810.043 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 14761
Raw data (/proc/14757/stat): 14757 (minisat+_script) S 14756 14757 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797626896 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14757/statm): 531 226 485 147 0 384 0
[pid=14757] vsize: 2124
Raw data (/proc/14761/stat): 14761 (minisat+_64-bit) R 14757 14757 22582 0 -1 0 29752 0 0 0 80614 169 0 0 25 0 1 0 1797626901 121475072 28790 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14761/statm): 29657 28790 145 145 0 29512 0
[pid=14761] vsize: 118628
Current children cumulated CPU time (s) 807.84
Current children cumulated vsize (Kb) 120752

[startup+820.043 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 14761
Raw data (/proc/14757/stat): 14757 (minisat+_script) S 14756 14757 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797626896 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14757/statm): 531 226 485 147 0 384 0
[pid=14757] vsize: 2124
Raw data (/proc/14761/stat): 14761 (minisat+_64-bit) R 14757 14757 22582 0 -1 0 29753 0 0 0 81614 169 0 0 25 0 1 0 1797626901 121475072 28791 4294967295 134512640 135094434 3221224432 3221223088 134557920 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14761/statm): 29657 28791 145 145 0 29512 0
[pid=14761] vsize: 118628
Current children cumulated CPU time (s) 817.84
Current children cumulated vsize (Kb) 120752

[startup+830.044 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 14761
Raw data (/proc/14757/stat): 14757 (minisat+_script) S 14756 14757 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797626896 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14757/statm): 531 226 485 147 0 384 0
[pid=14757] vsize: 2124
Raw data (/proc/14761/stat): 14761 (minisat+_64-bit) R 14757 14757 22582 0 -1 0 29753 0 0 0 82615 169 0 0 25 0 1 0 1797626901 121475072 28791 4294967295 134512640 135094434 3221224432 3221223088 134557860 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14761/statm): 29657 28791 145 145 0 29512 0
[pid=14761] vsize: 118628
Current children cumulated CPU time (s) 827.85
Current children cumulated vsize (Kb) 120752

[startup+840.044 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 14761
Raw data (/proc/14757/stat): 14757 (minisat+_script) S 14756 14757 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797626896 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14757/statm): 531 226 485 147 0 384 0
[pid=14757] vsize: 2124
Raw data (/proc/14761/stat): 14761 (minisat+_64-bit) R 14757 14757 22582 0 -1 0 29754 0 0 0 83615 169 0 0 25 0 1 0 1797626901 121475072 28792 4294967295 134512640 135094434 3221224432 3221223024 134556941 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14761/statm): 29657 28792 145 145 0 29512 0
[pid=14761] vsize: 118628
Current children cumulated CPU time (s) 837.85
Current children cumulated vsize (Kb) 120752

[startup+850.044 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 14761
Raw data (/proc/14757/stat): 14757 (minisat+_script) S 14756 14757 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797626896 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14757/statm): 531 226 485 147 0 384 0
[pid=14757] vsize: 2124
Raw data (/proc/14761/stat): 14761 (minisat+_64-bit) R 14757 14757 22582 0 -1 0 29754 0 0 0 84615 169 0 0 25 0 1 0 1797626901 121475072 28792 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14761/statm): 29657 28792 145 145 0 29512 0
[pid=14761] vsize: 118628
Current children cumulated CPU time (s) 847.85
Current children cumulated vsize (Kb) 120752

[startup+860.045 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 14761
Raw data (/proc/14757/stat): 14757 (minisat+_script) S 14756 14757 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797626896 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14757/statm): 531 226 485 147 0 384 0
[pid=14757] vsize: 2124
Raw data (/proc/14761/stat): 14761 (minisat+_64-bit) R 14757 14757 22582 0 -1 0 29754 0 0 0 85615 169 0 0 25 0 1 0 1797626901 121475072 28792 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14761/statm): 29657 28792 145 145 0 29512 0
[pid=14761] vsize: 118628
Current children cumulated CPU time (s) 857.85
Current children cumulated vsize (Kb) 120752

[startup+870.045 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 14761
Raw data (/proc/14757/stat): 14757 (minisat+_script) S 14756 14757 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797626896 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14757/statm): 531 226 485 147 0 384 0
[pid=14757] vsize: 2124
Raw data (/proc/14761/stat): 14761 (minisat+_64-bit) R 14757 14757 22582 0 -1 0 29754 0 0 0 86616 169 0 0 25 0 1 0 1797626901 121475072 28792 4294967295 134512640 135094434 3221224432 3221223088 134558246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14761/statm): 29657 28792 145 145 0 29512 0
[pid=14761] vsize: 118628
Current children cumulated CPU time (s) 867.86
Current children cumulated vsize (Kb) 120752

[startup+880.046 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 14761
Raw data (/proc/14757/stat): 14757 (minisat+_script) S 14756 14757 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797626896 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14757/statm): 531 226 485 147 0 384 0
[pid=14757] vsize: 2124
Raw data (/proc/14761/stat): 14761 (minisat+_64-bit) R 14757 14757 22582 0 -1 0 29754 0 0 0 87616 169 0 0 25 0 1 0 1797626901 121475072 28792 4294967295 134512640 135094434 3221224432 3221223088 134558218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14761/statm): 29657 28792 145 145 0 29512 0
[pid=14761] vsize: 118628
Current children cumulated CPU time (s) 877.86
Current children cumulated vsize (Kb) 120752

[startup+890.046 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 14761
Raw data (/proc/14757/stat): 14757 (minisat+_script) S 14756 14757 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797626896 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14757/statm): 531 226 485 147 0 384 0
[pid=14757] vsize: 2124
Raw data (/proc/14761/stat): 14761 (minisat+_64-bit) R 14757 14757 22582 0 -1 0 29754 0 0 0 88616 169 0 0 25 0 1 0 1797626901 121475072 28792 4294967295 134512640 135094434 3221224432 3221223056 134557565 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14761/statm): 29657 28792 145 145 0 29512 0
[pid=14761] vsize: 118628
Current children cumulated CPU time (s) 887.86
Current children cumulated vsize (Kb) 120752

[startup+900.047 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 14761
Raw data (/proc/14757/stat): 14757 (minisat+_script) S 14756 14757 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797626896 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14757/statm): 531 226 485 147 0 384 0
[pid=14757] vsize: 2124
Raw data (/proc/14761/stat): 14761 (minisat+_64-bit) R 14757 14757 22582 0 -1 0 29754 0 0 0 89616 169 0 0 25 0 1 0 1797626901 121475072 28792 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14761/statm): 29657 28792 145 145 0 29512 0
[pid=14761] vsize: 118628
Current children cumulated CPU time (s) 897.86
Current children cumulated vsize (Kb) 120752

[startup+910.047 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 14761
Raw data (/proc/14757/stat): 14757 (minisat+_script) S 14756 14757 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797626896 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14757/statm): 531 226 485 147 0 384 0
[pid=14757] vsize: 2124
Raw data (/proc/14761/stat): 14761 (minisat+_64-bit) R 14757 14757 22582 0 -1 0 29754 0 0 0 90617 169 0 0 25 0 1 0 1797626901 121475072 28792 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14761/statm): 29657 28792 145 145 0 29512 0
[pid=14761] vsize: 118628
Current children cumulated CPU time (s) 907.87
Current children cumulated vsize (Kb) 120752

[startup+920.048 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 14761
Raw data (/proc/14757/stat): 14757 (minisat+_script) S 14756 14757 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797626896 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14757/statm): 531 226 485 147 0 384 0
[pid=14757] vsize: 2124
Raw data (/proc/14761/stat): 14761 (minisat+_64-bit) R 14757 14757 22582 0 -1 0 29754 0 0 0 91617 169 0 0 25 0 1 0 1797626901 121475072 28792 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14761/statm): 29657 28792 145 145 0 29512 0
[pid=14761] vsize: 118628
Current children cumulated CPU time (s) 917.87
Current children cumulated vsize (Kb) 120752

[startup+930.05 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 14761
Raw data (/proc/14757/stat): 14757 (minisat+_script) S 14756 14757 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797626896 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14757/statm): 531 226 485 147 0 384 0
[pid=14757] vsize: 2124
Raw data (/proc/14761/stat): 14761 (minisat+_64-bit) R 14757 14757 22582 0 -1 0 29754 0 0 0 92617 169 0 0 25 0 1 0 1797626901 121475072 28792 4294967295 134512640 135094434 3221224432 3221223088 134557890 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14761/statm): 29657 28792 145 145 0 29512 0
[pid=14761] vsize: 118628
Current children cumulated CPU time (s) 927.87
Current children cumulated vsize (Kb) 120752

[startup+940.05 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 14761
Raw data (/proc/14757/stat): 14757 (minisat+_script) S 14756 14757 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797626896 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14757/statm): 531 226 485 147 0 384 0
[pid=14757] vsize: 2124
Raw data (/proc/14761/stat): 14761 (minisat+_64-bit) R 14757 14757 22582 0 -1 0 29754 0 0 0 93617 169 0 0 25 0 1 0 1797626901 121475072 28792 4294967295 134512640 135094434 3221224432 3221223088 134558029 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14761/statm): 29657 28792 145 145 0 29512 0
[pid=14761] vsize: 118628
Current children cumulated CPU time (s) 937.87
Current children cumulated vsize (Kb) 120752

[startup+950.05 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 14761
Raw data (/proc/14757/stat): 14757 (minisat+_script) S 14756 14757 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797626896 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14757/statm): 531 226 485 147 0 384 0
[pid=14757] vsize: 2124
Raw data (/proc/14761/stat): 14761 (minisat+_64-bit) R 14757 14757 22582 0 -1 0 29754 0 0 0 94618 169 0 0 25 0 1 0 1797626901 121475072 28792 4294967295 134512640 135094434 3221224432 3221223024 134557219 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14761/statm): 29657 28792 145 145 0 29512 0
[pid=14761] vsize: 118628
Current children cumulated CPU time (s) 947.88
Current children cumulated vsize (Kb) 120752

[startup+960.051 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 14761
Raw data (/proc/14757/stat): 14757 (minisat+_script) S 14756 14757 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797626896 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14757/statm): 531 226 485 147 0 384 0
[pid=14757] vsize: 2124
Raw data (/proc/14761/stat): 14761 (minisat+_64-bit) R 14757 14757 22582 0 -1 0 29754 0 0 0 95618 169 0 0 25 0 1 0 1797626901 121475072 28792 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14761/statm): 29657 28792 145 145 0 29512 0
[pid=14761] vsize: 118628
Current children cumulated CPU time (s) 957.88
Current children cumulated vsize (Kb) 120752

[startup+970.052 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 14761
Raw data (/proc/14757/stat): 14757 (minisat+_script) S 14756 14757 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797626896 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14757/statm): 531 226 485 147 0 384 0
[pid=14757] vsize: 2124
Raw data (/proc/14761/stat): 14761 (minisat+_64-bit) R 14757 14757 22582 0 -1 0 29754 0 0 0 96618 169 0 0 25 0 1 0 1797626901 121475072 28792 4294967295 134512640 135094434 3221224432 3221223088 134557872 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14761/statm): 29657 28792 145 145 0 29512 0
[pid=14761] vsize: 118628
Current children cumulated CPU time (s) 967.88
Current children cumulated vsize (Kb) 120752

[startup+980.052 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 14761
Raw data (/proc/14757/stat): 14757 (minisat+_script) S 14756 14757 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797626896 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14757/statm): 531 226 485 147 0 384 0
[pid=14757] vsize: 2124
Raw data (/proc/14761/stat): 14761 (minisat+_64-bit) R 14757 14757 22582 0 -1 0 29754 0 0 0 97619 169 0 0 25 0 1 0 1797626901 121475072 28792 4294967295 134512640 135094434 3221224432 3221223104 134556465 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14761/statm): 29657 28792 145 145 0 29512 0
[pid=14761] vsize: 118628
Current children cumulated CPU time (s) 977.89
Current children cumulated vsize (Kb) 120752

[startup+990.054 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 14761
Raw data (/proc/14757/stat): 14757 (minisat+_script) S 14756 14757 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797626896 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14757/statm): 531 226 485 147 0 384 0
[pid=14757] vsize: 2124
Raw data (/proc/14761/stat): 14761 (minisat+_64-bit) R 14757 14757 22582 0 -1 0 29754 0 0 0 98619 169 0 0 25 0 1 0 1797626901 121475072 28792 4294967295 134512640 135094434 3221224432 3221223056 134557565 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14761/statm): 29657 28792 145 145 0 29512 0
[pid=14761] vsize: 118628
Current children cumulated CPU time (s) 987.89
Current children cumulated vsize (Kb) 120752

[startup+1000.05 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 14761
Raw data (/proc/14757/stat): 14757 (minisat+_script) S 14756 14757 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797626896 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14757/statm): 531 226 485 147 0 384 0
[pid=14757] vsize: 2124
Raw data (/proc/14761/stat): 14761 (minisat+_64-bit) R 14757 14757 22582 0 -1 0 29754 0 0 0 99619 169 0 0 25 0 1 0 1797626901 121475072 28792 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14761/statm): 29657 28792 145 145 0 29512 0
[pid=14761] vsize: 118628
Current children cumulated CPU time (s) 997.89
Current children cumulated vsize (Kb) 120752

[startup+1010.05 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 14761
Raw data (/proc/14757/stat): 14757 (minisat+_script) S 14756 14757 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797626896 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14757/statm): 531 226 485 147 0 384 0
[pid=14757] vsize: 2124
Raw data (/proc/14761/stat): 14761 (minisat+_64-bit) R 14757 14757 22582 0 -1 0 29754 0 0 0 100619 169 0 0 25 0 1 0 1797626901 121475072 28792 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14761/statm): 29657 28792 145 145 0 29512 0
[pid=14761] vsize: 118628
Current children cumulated CPU time (s) 1007.89
Current children cumulated vsize (Kb) 120752

[startup+1020.05 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 14761
Raw data (/proc/14757/stat): 14757 (minisat+_script) S 14756 14757 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797626896 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14757/statm): 531 226 485 147 0 384 0
[pid=14757] vsize: 2124
Raw data (/proc/14761/stat): 14761 (minisat+_64-bit) R 14757 14757 22582 0 -1 0 29754 0 0 0 101620 169 0 0 25 0 1 0 1797626901 121475072 28792 4294967295 134512640 135094434 3221224432 3221223104 134555574 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14761/statm): 29657 28792 145 145 0 29512 0
[pid=14761] vsize: 118628
Current children cumulated CPU time (s) 1017.9
Current children cumulated vsize (Kb) 120752

[startup+1030.06 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 14761
Raw data (/proc/14757/stat): 14757 (minisat+_script) S 14756 14757 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797626896 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14757/statm): 531 226 485 147 0 384 0
[pid=14757] vsize: 2124
Raw data (/proc/14761/stat): 14761 (minisat+_64-bit) R 14757 14757 22582 0 -1 0 29754 0 0 0 102620 169 0 0 25 0 1 0 1797626901 121475072 28792 4294967295 134512640 135094434 3221224432 3221223088 134558240 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14761/statm): 29657 28792 145 145 0 29512 0
[pid=14761] vsize: 118628
Current children cumulated CPU time (s) 1027.9
Current children cumulated vsize (Kb) 120752

[startup+1040.06 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 14761
Raw data (/proc/14757/stat): 14757 (minisat+_script) S 14756 14757 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797626896 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14757/statm): 531 226 485 147 0 384 0
[pid=14757] vsize: 2124
Raw data (/proc/14761/stat): 14761 (minisat+_64-bit) R 14757 14757 22582 0 -1 0 29754 0 0 0 103620 169 0 0 25 0 1 0 1797626901 121475072 28792 4294967295 134512640 135094434 3221224432 3221223024 134556941 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14761/statm): 29657 28792 145 145 0 29512 0
[pid=14761] vsize: 118628
Current children cumulated CPU time (s) 1037.9
Current children cumulated vsize (Kb) 120752

[startup+1050.06 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 14761
Raw data (/proc/14757/stat): 14757 (minisat+_script) S 14756 14757 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797626896 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14757/statm): 531 226 485 147 0 384 0
[pid=14757] vsize: 2124
Raw data (/proc/14761/stat): 14761 (minisat+_64-bit) R 14757 14757 22582 0 -1 0 29754 0 0 0 104620 169 0 0 25 0 1 0 1797626901 121475072 28792 4294967295 134512640 135094434 3221224432 3221223104 134555755 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14761/statm): 29657 28792 145 145 0 29512 0
[pid=14761] vsize: 118628
Current children cumulated CPU time (s) 1047.9
Current children cumulated vsize (Kb) 120752

[startup+1060.06 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 14761
Raw data (/proc/14757/stat): 14757 (minisat+_script) S 14756 14757 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797626896 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14757/statm): 531 226 485 147 0 384 0
[pid=14757] vsize: 2124
Raw data (/proc/14761/stat): 14761 (minisat+_64-bit) R 14757 14757 22582 0 -1 0 29754 0 0 0 105621 169 0 0 25 0 1 0 1797626901 121475072 28792 4294967295 134512640 135094434 3221224432 3221223044 134563083 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14761/statm): 29657 28792 145 145 0 29512 0
[pid=14761] vsize: 118628
Current children cumulated CPU time (s) 1057.91
Current children cumulated vsize (Kb) 120752

[startup+1070.06 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 14761
Raw data (/proc/14757/stat): 14757 (minisat+_script) S 14756 14757 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797626896 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14757/statm): 531 226 485 147 0 384 0
[pid=14757] vsize: 2124
Raw data (/proc/14761/stat): 14761 (minisat+_64-bit) R 14757 14757 22582 0 -1 0 29754 0 0 0 106621 169 0 0 25 0 1 0 1797626901 121475072 28792 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14761/statm): 29657 28792 145 145 0 29512 0
[pid=14761] vsize: 118628
Current children cumulated CPU time (s) 1067.91
Current children cumulated vsize (Kb) 120752

[startup+1080.06 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 14761
Raw data (/proc/14757/stat): 14757 (minisat+_script) S 14756 14757 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797626896 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14757/statm): 531 226 485 147 0 384 0
[pid=14757] vsize: 2124
Raw data (/proc/14761/stat): 14761 (minisat+_64-bit) R 14757 14757 22582 0 -1 0 29754 0 0 0 107621 169 0 0 25 0 1 0 1797626901 121475072 28792 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14761/statm): 29657 28792 145 145 0 29512 0
[pid=14761] vsize: 118628
Current children cumulated CPU time (s) 1077.91
Current children cumulated vsize (Kb) 120752

[startup+1090.06 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 14761
Raw data (/proc/14757/stat): 14757 (minisat+_script) S 14756 14757 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797626896 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14757/statm): 531 226 485 147 0 384 0
[pid=14757] vsize: 2124
Raw data (/proc/14761/stat): 14761 (minisat+_64-bit) R 14757 14757 22582 0 -1 0 29754 0 0 0 108621 169 0 0 25 0 1 0 1797626901 121475072 28792 4294967295 134512640 135094434 3221224432 3221223184 134559282 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14761/statm): 29657 28792 145 145 0 29512 0
[pid=14761] vsize: 118628
Current children cumulated CPU time (s) 1087.91
Current children cumulated vsize (Kb) 120752

[startup+1100.06 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 14761
Raw data (/proc/14757/stat): 14757 (minisat+_script) S 14756 14757 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797626896 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14757/statm): 531 226 485 147 0 384 0
[pid=14757] vsize: 2124
Raw data (/proc/14761/stat): 14761 (minisat+_64-bit) R 14757 14757 22582 0 -1 0 29754 0 0 0 109621 170 0 0 25 0 1 0 1797626901 121475072 28792 4294967295 134512640 135094434 3221224432 3221223088 134558402 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14761/statm): 29657 28792 145 145 0 29512 0
[pid=14761] vsize: 118628
Current children cumulated CPU time (s) 1097.92
Current children cumulated vsize (Kb) 120752

[startup+1110.06 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 14761
Raw data (/proc/14757/stat): 14757 (minisat+_script) S 14756 14757 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797626896 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14757/statm): 531 226 485 147 0 384 0
[pid=14757] vsize: 2124
Raw data (/proc/14761/stat): 14761 (minisat+_64-bit) R 14757 14757 22582 0 -1 0 29754 0 0 0 110621 170 0 0 25 0 1 0 1797626901 121475072 28792 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14761/statm): 29657 28792 145 145 0 29512 0
[pid=14761] vsize: 118628
Current children cumulated CPU time (s) 1107.92
Current children cumulated vsize (Kb) 120752

[startup+1120.06 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 14761
Raw data (/proc/14757/stat): 14757 (minisat+_script) S 14756 14757 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797626896 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14757/statm): 531 226 485 147 0 384 0
[pid=14757] vsize: 2124
Raw data (/proc/14761/stat): 14761 (minisat+_64-bit) R 14757 14757 22582 0 -1 0 29754 0 0 0 111622 170 0 0 25 0 1 0 1797626901 121475072 28792 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14761/statm): 29657 28792 145 145 0 29512 0
[pid=14761] vsize: 118628
Current children cumulated CPU time (s) 1117.93
Current children cumulated vsize (Kb) 120752

[startup+1130.06 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 14761
Raw data (/proc/14757/stat): 14757 (minisat+_script) S 14756 14757 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797626896 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14757/statm): 531 226 485 147 0 384 0
[pid=14757] vsize: 2124
Raw data (/proc/14761/stat): 14761 (minisat+_64-bit) R 14757 14757 22582 0 -1 0 29754 0 0 0 112622 170 0 0 25 0 1 0 1797626901 121475072 28792 4294967295 134512640 135094434 3221224432 3221223088 134557914 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14761/statm): 29657 28792 145 145 0 29512 0
[pid=14761] vsize: 118628
Current children cumulated CPU time (s) 1127.93
Current children cumulated vsize (Kb) 120752

[startup+1140.06 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 14761
Raw data (/proc/14757/stat): 14757 (minisat+_script) S 14756 14757 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797626896 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14757/statm): 531 226 485 147 0 384 0
[pid=14757] vsize: 2124
Raw data (/proc/14761/stat): 14761 (minisat+_64-bit) R 14757 14757 22582 0 -1 0 29754 0 0 0 113622 170 0 0 25 0 1 0 1797626901 121475072 28792 4294967295 134512640 135094434 3221224432 3221223056 134557648 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14761/statm): 29657 28792 145 145 0 29512 0
[pid=14761] vsize: 118628
Current children cumulated CPU time (s) 1137.93
Current children cumulated vsize (Kb) 120752

[startup+1150.06 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 14761
Raw data (/proc/14757/stat): 14757 (minisat+_script) S 14756 14757 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797626896 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14757/statm): 531 226 485 147 0 384 0
[pid=14757] vsize: 2124
Raw data (/proc/14761/stat): 14761 (minisat+_64-bit) R 14757 14757 22582 0 -1 0 29754 0 0 0 114622 170 0 0 25 0 1 0 1797626901 121475072 28792 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14761/statm): 29657 28792 145 145 0 29512 0
[pid=14761] vsize: 118628
Current children cumulated CPU time (s) 1147.93
Current children cumulated vsize (Kb) 120752

[startup+1160.06 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 14761
Raw data (/proc/14757/stat): 14757 (minisat+_script) S 14756 14757 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797626896 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14757/statm): 531 226 485 147 0 384 0
[pid=14757] vsize: 2124
Raw data (/proc/14761/stat): 14761 (minisat+_64-bit) R 14757 14757 22582 0 -1 0 29754 0 0 0 115623 170 0 0 25 0 1 0 1797626901 121475072 28792 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14761/statm): 29657 28792 145 145 0 29512 0
[pid=14761] vsize: 118628
Current children cumulated CPU time (s) 1157.94
Current children cumulated vsize (Kb) 120752

[startup+1170.06 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 14761
Raw data (/proc/14757/stat): 14757 (minisat+_script) S 14756 14757 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797626896 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14757/statm): 531 226 485 147 0 384 0
[pid=14757] vsize: 2124
Raw data (/proc/14761/stat): 14761 (minisat+_64-bit) R 14757 14757 22582 0 -1 0 29754 0 0 0 116623 170 0 0 25 0 1 0 1797626901 121475072 28792 4294967295 134512640 135094434 3221224432 3221223056 134557627 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14761/statm): 29657 28792 145 145 0 29512 0
[pid=14761] vsize: 118628
Current children cumulated CPU time (s) 1167.94
Current children cumulated vsize (Kb) 120752

[startup+1180.07 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 14761
Raw data (/proc/14757/stat): 14757 (minisat+_script) S 14756 14757 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797626896 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14757/statm): 531 226 485 147 0 384 0
[pid=14757] vsize: 2124
Raw data (/proc/14761/stat): 14761 (minisat+_64-bit) R 14757 14757 22582 0 -1 0 29754 0 0 0 117623 170 0 0 25 0 1 0 1797626901 121475072 28792 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14761/statm): 29657 28792 145 145 0 29512 0
[pid=14761] vsize: 118628
Current children cumulated CPU time (s) 1177.94
Current children cumulated vsize (Kb) 120752

[startup+1190.07 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 14761
Raw data (/proc/14757/stat): 14757 (minisat+_script) S 14756 14757 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797626896 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14757/statm): 531 226 485 147 0 384 0
[pid=14757] vsize: 2124
Raw data (/proc/14761/stat): 14761 (minisat+_64-bit) R 14757 14757 22582 0 -1 0 29756 0 0 0 118623 170 0 0 25 0 1 0 1797626901 121475072 28794 4294967295 134512640 135094434 3221224432 3221223024 134557219 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14761/statm): 29657 28794 145 145 0 29512 0
[pid=14761] vsize: 118628
Current children cumulated CPU time (s) 1187.94
Current children cumulated vsize (Kb) 120752

[startup+1200.07 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 14761
Raw data (/proc/14757/stat): 14757 (minisat+_script) S 14756 14757 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797626896 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14757/statm): 531 226 485 147 0 384 0
[pid=14757] vsize: 2124
Raw data (/proc/14761/stat): 14761 (minisat+_64-bit) R 14757 14757 22582 0 -1 0 29760 0 0 0 119623 170 0 0 25 0 1 0 1797626901 121475072 28798 4294967295 134512640 135094434 3221224432 3221223088 134557890 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14761/statm): 29657 28798 145 145 0 29512 0
[pid=14761] vsize: 118628
Current children cumulated CPU time (s) 1197.94
Current children cumulated vsize (Kb) 120752

[startup+1210.07 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 14761
Raw data (/proc/14757/stat): 14757 (minisat+_script) S 14756 14757 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797626896 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14757/statm): 531 226 485 147 0 384 0
[pid=14757] vsize: 2124
Raw data (/proc/14761/stat): 14761 (minisat+_64-bit) R 14757 14757 22582 0 -1 0 29764 0 0 0 120624 170 0 0 25 0 1 0 1797626901 121475072 28802 4294967295 134512640 135094434 3221224432 3221223088 134558235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14761/statm): 29657 28802 145 145 0 29512 0
[pid=14761] vsize: 118628
Current children cumulated CPU time (s) 1207.95
Current children cumulated vsize (Kb) 120752



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.07 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 14761
Raw data (/proc/14757/stat): 14757 (minisat+_script) S 14756 14757 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1797626896 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14757/statm): 531 226 485 147 0 384 0
[pid=14757] vsize: 2124
Raw data (/proc/14761/stat): 14761 (minisat+_64-bit) R 14757 14757 22582 0 -1 0 29764 0 0 0 120624 170 0 0 25 0 1 0 1797626901 121475072 28802 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14761/statm): 29657 28802 145 145 0 29512 0
[pid=14761] vsize: 118628
Current children cumulated CPU time (s) 1207.95
Current children cumulated vsize (Kb) 120752

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

Child status: 10
Real time (s): 1210.13
CPU time (s): 1208
CPU user time (s): 1206.25
CPU system time (s): 1.75473
CPU usage (%): 99.824
Max. virtual memory (cumulated for all children) (Kb): 120752

Verifier Data

ERROR: no interpretation found !