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

Nameweb/www.ps.uni-sb.de/~walser/benchmarks/radar/normalized-10:20:4.5:0.5:100.opb
MD5SUMfeaa96df552ef9989407735877840272
Bench Categoryoptimization, small integers (OPTSMALLINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function 12
Optimality of the best value was proved NO
Number of terms in the objective function 776
Biggest coefficient in the objective function 474
Number of bits for the biggest coefficient in the objective function 9
Sum of the numbers in the objective function 2127
Number of bits of the sum of numbers in the objective function 12
Biggest number in a constraint 474
Number of bits of the biggest number in a constraint 9
Biggest sum of numbers in a constraint 2127
Number of bits of the biggest sum of numbers12
Best result obtained on this benchmarkSAT
Best CPU time to get the best result obtained on this benchmark1213.45
Number of variables776
Total number of constraints1642
Number of constraints which are clauses701
Number of constraints which are cardinality constraints (but not clauses)941
Number of constraints which are nor clauses,nor cardinality constraints0
Minimum length of a constraint1
Maximum length of a constraint20

Trace number 2357

Launcher Data

LAUNCH ON wulflinc12 THE 2005-09-18 19:10:59 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=2738 boxname=wulflinc12 idbench=394 idsolver=3 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  feaa96df552ef9989407735877840272  /oldhome/oroussel/tmp/wulflinc12/normalized-10:20:4.5:0.5:100.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc12/normalized-10:20:4.5:0.5:100.opb
IDLAUNCH: 2738
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.091
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 888.83

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.091
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:        898456 kB
Buffers:         38676 kB
Cached:          57408 kB
SwapCached:        544 kB
Active:          66960 kB
Inactive:        41380 kB
HighTotal:      131008 kB
HighFree:        73556 kB
LowTotal:       903652 kB
LowFree:        824900 kB
SwapTotal:     2097136 kB
SwapFree:      2096072 kB
Dirty:              24 kB
Writeback:           0 kB
Mapped:           5884 kB
Slab:            22272 kB
Committed_AS:    64164 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-09-18 19:31:10 (client local time) WITH STATUS 10 IN 1208.79 SECONDS
stats: 2738 7 1208.79 10

Solver Data

c Parsing PB file...
c Converting 866 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): .............................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ---[ 172]---> BDD-cost:   14
c ---[ 171]---> BDD-cost:   17
c ---[ 170]---> BDD-cost:   20
c ---[ 169]---> BDD-cost:   20
c ---[ 168]---> BDD-cost:   23
c ---[ 167]---> BDD-cost:   23
c ---[ 166]---> BDD-cost:   29
c ---[ 165]---> BDD-cost:   29
c ---[ 164]---> BDD-cost:   32
c ---[ 163]---> BDD-cost:   38
c ---[ 162]---> BDD-cost:   44
c ---[ 161]---> BDD-cost:   44
c ---[ 160]---> BDD-cost:   50
c ---[ 159]---> BDD-cost:   44
c ---[ 158]---> BDD-cost:   47
c ---[ 157]---> BDD-cost:   44
c ---[ 156]---> BDD-cost:   41
c ---[ 155]---> BDD-cost:   29
c ---[ 154]---> BDD-cost:   20
c ---[ 153]---> BDD-cost:   11
c ---[ 152]---> BDD-cost:    9
c ---[ 151]---> BDD-cost:   17
c ---[ 150]---> BDD-cost:   20
c ---[ 149]---> BDD-cost:   20
c ---[ 148]---> BDD-cost:   26
c ---[ 147]---> BDD-cost:   29
c ---[ 146]---> BDD-cost:   27
c ---[ 145]---> BDD-cost:   29
c ---[ 144]---> BDD-cost:   32
c ---[ 143]---> BDD-cost:   41
c ---[ 142]---> BDD-cost:   47
c ---[ 141]---> BDD-cost:   47
c ---[ 140]---> BDD-cost:   50
c ---[ 139]---> BDD-cost:   50
c ---[ 138]---> BDD-cost:   50
c ---[ 137]---> BDD-cost:   47
c ---[ 136]---> BDD-cost:   41
c ---[ 135]---> BDD-cost:   35
c ---[ 134]---> BDD-cost:   23
c ---[ 133]---> BDD-cost:   12
c ---[ 132]---> BDD-cost:   11
c ---[ 131]---> BDD-cost:   17
c ---[ 130]---> BDD-cost:   23
c ---[ 129]---> BDD-cost:   23
c ---[ 128]---> BDD-cost:   26
c ---[ 127]---> BDD-cost:   29
c ---[ 126]---> BDD-cost:   35
c ---[ 125]---> BDD-cost:   27
c ---[ 124]---> BDD-cost:   35
c ---[ 123]---> BDD-cost:   41
c ---[ 122]---> BDD-cost:   45
c ---[ 121]---> BDD-cost:   47
c ---[ 120]---> BDD-cost:   50
c ---[ 119]---> BDD-cost:   53
c ---[ 118]---> BDD-cost:   53
c ---[ 117]---> BDD-cost:   47
c ---[ 116]---> BDD-cost:   41
c ---[ 115]---> BDD-cost:   35
c ---[ 114]---> BDD-cost:   21
c ---[ 113]---> BDD-cost:   14
c ---[ 112]---> BDD-cost:   11
c ---[ 111]---> BDD-cost:   20
c ---[ 110]---> BDD-cost:   23
c ---[ 109]---> BDD-cost:   23
c ---[ 108]---> BDD-cost:   20
c ---[ 107]---> BDD-cost:   26
c ---[ 106]---> BDD-cost:   23
c ---[ 105]---> BDD-cost:   29
c ---[ 104]---> BDD-cost:   29
c ---[ 103]---> BDD-cost:   38
c ---[ 102]---> BDD-cost:   41
c ---[ 101]---> BDD-cost:   47
c ---[ 100]---> BDD-cost:   45
c ---[  99]---> BDD-cost:   53
c ---[  98]---> BDD-cost:   44
c ---[  97]---> BDD-cost:   47
c ---[  96]---> BDD-cost:   41
c ---[  95]---> BDD-cost:   35
c ---[  94]---> BDD-cost:   26
c ---[  93]---> BDD-cost:   17
c ---[  92]---> BDD-cost:    5
c ---[  91]---> BDD-cost:   20
c ---[  90]---> BDD-cost:   17
c ---[  89]---> BDD-cost:   20
c ---[  88]---> BDD-cost:   11
c ---[  87]---> BDD-cost:   14
c ---[  86]---> BDD-cost:    8
c ---[  85]---> BDD-cost:   20
c ---[  84]---> BDD-cost:   17
c ---[  83]---> BDD-cost:   32
c ---[  82]---> BDD-cost:   29
c ---[  81]---> BDD-cost:   38
c ---[  80]---> BDD-cost:   29
c ---[  79]---> BDD-cost:   44
c ---[  78]---> BDD-cost:   38
c ---[  77]---> BDD-cost:   41
c ---[  76]---> BDD-cost:   32
c ---[  75]---> BDD-cost:   23
c ---[  74]---> BDD-cost:   17
c ---[  73]---> BDD-cost:   20
c ---[  72]---> BDD-cost:    8
c ---[  71]---> BDD-cost:    9
c ---[  70]---> BDD-cost:   11
c ---[  69]---> BDD-cost:   11
c ---[  68]---> BDD-cost:    7
c ---[  67]---> BDD-cost:    8
c ---[  66]---> BDD-cost:    5
c ---[  65]---> BDD-cost:    5
c ---[  64]---> BDD-cost:   17
c ---[  63]---> BDD-cost:   20
c ---[  62]---> BDD-cost:   20
c ---[  61]---> BDD-cost:   17
c ---[  60]---> BDD-cost:   32
c ---[  59]---> BDD-cost:   20
c ---[  58]---> BDD-cost:   29
c ---[  57]---> BDD-cost:   23
c ---[  56]---> BDD-cost:   26
c ---[  55]---> BDD-cost:   11
c ---[  54]---> BDD-cost:    7
c ---[  52]---> BDD-cost:   11
c ---[  51]---> BDD-cost:   11
c ---[  50]---> BDD-cost:   11
c ---[  48]---> BDD-cost:    8
c ---[  47]---> BDD-cost:    9
c ---[  46]---> BDD-cost:    8
c ---[  44]---> BDD-cost:    9
c ---[  43]---> BDD-cost:    5
c ---[  42]---> BDD-cost:   14
c ---[  41]---> BDD-cost:    7
c ---[  40]---> BDD-cost:   11
c ---[  39]---> BDD-cost:    7
c ---[  38]---> BDD-cost:   14
c ---[  35]---> BDD-cost:    5
c ---[  34]---> BDD-cost:   11
c ---[  33]---> BDD-cost:   11
c ---[  32]---> BDD-cost:   11
c ---[  31]---> BDD-cost:    3
c ---[  30]---> BDD-cost:    7
c ---[  29]---> BDD-cost:    5
c ---[  28]---> BDD-cost:    8
c ---[  27]---> BDD-cost:   11
c ---[  25]---> BDD-cost:    7
c ---[  24]---> BDD-cost:    5
c ---[  22]---> BDD-cost:    3
c ---[  21]---> BDD-cost:    8
c ---[  20]---> BDD-cost:   11
c ---[  19]---> BDD-cost:   11
c ---[  18]---> BDD-cost:    3
c ---[  17]---> BDD-cost:   11
c ---[  16]---> BDD-cost:    8
c ---[  15]---> BDD-cost:    5
c ---[  14]---> BDD-cost:    5
c ---[  12]---> BDD-cost:    3
c ---[  11]---> BDD-cost:    3
c ---[  10]---> BDD-cost:    3
c ---[   9]---> BDD-cost:    3
c ---[   8]---> BDD-cost:    8
c ---[   7]---> BDD-cost:    5
c ---[   6]---> BDD-cost:    3
c ---[   5]---> BDD-cost:    6
c ---[   4]---> BDD-cost:    5
c ---[   3]---> BDD-cost:    3
c ---[   2]---> BDD-cost:    5
c ---[   1]---> BDD-cost:    0
c ---[   0]---> BDD-cost:    3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |    9120    26089 |    3040       0        0     nan |  0.000 % |
c ==============================================================================
c Found solution: 762
c ---[   0]---> Sorter-cost:55537     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   78358   188367 |   26119       0        0     nan |  0.000 % |
c |       101 |   78117   187877 |   28730      93     1716    18.5 |  0.575 % |
c ==============================================================================
c Found solution: 59
c ---[   0]---> Sorter-cost:    2     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       152 |  107305   256100 |   35768     143     2524    17.7 |  0.575 % |
c |       252 |  107197   255852 |   39344     242     3434    14.2 |  0.685 % |
c |       403 |  107146   255749 |   43279     391     5026    12.9 |  0.734 % |
c |       628 |  106679   254725 |   47607     591    15618    26.4 |  1.106 % |
c |       965 |  106679   254725 |   52367     928    19299    20.8 |  1.106 % |
c |      1473 |  106284   253852 |   57604    1423    32871    23.1 |  1.513 % |
c |      2232 |  106079   253390 |   63365    2178    71254    32.7 |  1.661 % |
c |      3371 |  105849   252864 |   69701    3305    82651    25.0 |  1.822 % |
c |      5079 |  105536   252160 |   76671    5001   102675    20.5 |  2.042 % |
c |      7642 |  104895   250715 |   84339    7523   149395    19.9 |  2.539 % |
c |     11487 |  104887   250697 |   92772   11366   263825    23.2 |  2.543 % |
c |     17253 |  104215   249156 |  102050   17080   375171    22.0 |  3.071 % |
c |     25902 |  103982   248623 |  112255   25693   678106    26.4 |  3.266 % |
c |     38878 |  103935   248522 |  123480   38658  1202967    31.1 |  3.317 % |
c |     58340 |  103533   247609 |  135828   58088  5020404    86.4 |  3.663 % |
c ==============================================================================
c Found solution: 54
c ---[   0]---> Sorter-cost:    1     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     79313 |  103589   247774 |   34529   79061  8055656   101.9 |  3.663 % |
c |     79414 |  103589   247774 |   37981   18273  2365870   129.5 |  3.662 % |
c |     79565 |  103589   247774 |   41780   18424  2369792   128.6 |  3.662 % |
c |     79790 |  103589   247774 |   45958   18649  2371476   127.2 |  3.662 % |
c |     80127 |  103581   247756 |   50553   18979  2374128   125.1 |  3.666 % |
c |     80633 |  103581   247756 |   55609   19485  2385425   122.4 |  3.666 % |
c |     81392 |  103581   247756 |   61170   20244  2396965   118.4 |  3.666 % |
c |     82533 |  103581   247756 |   67287   21385  2443100   114.2 |  3.666 % |
c |     84241 |  103581   247756 |   74015   23093  2486928   107.7 |  3.666 % |
c |     86803 |  103569   247728 |   81417   25653  2555338    99.6 |  3.673 % |
c |     90647 |  103509   247594 |   89559   29474  2657142    90.2 |  3.744 % |
c |     96413 |  103433   247424 |   98515   35233  2893777    82.1 |  3.833 % |
c |    105064 |  103433   247424 |  108366   43884  3859552    87.9 |  3.833 % |
c ==============================================================================
c Found solution: 51
c ---[   0]---> Sorter-cost:    2     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    115370 |  103369   247283 |   34456   54184  5009811    92.5 |  3.833 % |
c |    115472 |  103369   247283 |   37901   19025  1552846    81.6 |  3.880 % |
c |    115626 |  103369   247283 |   41691   19179  1555460    81.1 |  3.880 % |
c |    115851 |  103369   247283 |   45860   19404  1558001    80.3 |  3.880 % |
c |    116188 |  103339   247217 |   50447   19553  1559070    79.7 |  3.914 % |
c |    116694 |  103339   247217 |   55491   20059  1567634    78.2 |  3.914 % |
c |    117454 |  103339   247217 |   61040   20819  1584364    76.1 |  3.914 % |
c |    118593 |  103339   247217 |   67144   21958  1607737    73.2 |  3.914 % |
c |    120301 |  103339   247217 |   73859   23666  1690288    71.4 |  3.914 % |
c |    122864 |  103268   247064 |   81245   26224  1762345    67.2 |  3.992 % |
c |    126708 |  103235   246993 |   89369   30066  1885060    62.7 |  4.028 % |
c ==============================================================================
c Found solution: 46
c ---[   0]---> Sorter-cost:    1     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    130268 |  103265   247098 |   34421   33620  2093071    62.3 |  4.028 % |
c |    130369 |  103265   247098 |   37863   33721  2094104    62.1 |  4.042 % |
c |    130519 |  103265   247098 |   41649   33871  2098978    62.0 |  4.042 % |
c |    130744 |  103265   247098 |   45814   34096  2101462    61.6 |  4.042 % |
c |    131081 |  103265   247098 |   50395   34433  2108066    61.2 |  4.042 % |
c |    131587 |  103265   247098 |   55435   34939  2120201    60.7 |  4.042 % |
c |    132347 |  103265   247098 |   60978   35699  2132256    59.7 |  4.042 % |
c |    133486 |  103257   247080 |   67076   36831  2171985    59.0 |  4.046 % |
c |    135194 |  103247   247058 |   73784   38534  2230934    57.9 |  4.057 % |
c |    137756 |  103245   247054 |   81162   41093  2339305    56.9 |  4.059 % |
c |    141600 |  103245   247054 |   89279   44937  2493251    55.5 |  4.059 % |
c |    147366 |  103201   246956 |   98207   50695  2727322    53.8 |  4.093 % |
c |    156015 |  103127   246792 |  108027   59328  3406223    57.4 |  4.178 % |
c |    168989 |  103127   246792 |  118830   72302  6008985    83.1 |  4.178 % |
c ==============================================================================
c Found solution: 36
c ---[   0]---> Sorter-cost:    1     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    184940 |  102664   245770 |   34221   88175  7010762    79.5 |  4.178 % |
c |    185040 |  102635   245705 |   37643   23523   930122    39.5 |  4.622 % |
c |    185190 |  102635   245705 |   41407   23673   931813    39.4 |  4.622 % |
c |    185415 |  102635   245705 |   45548   23898   936406    39.2 |  4.622 % |
c |    185753 |  102635   245705 |   50102   24236   943152    38.9 |  4.622 % |
c |    186261 |  102635   245705 |   55113   24744   959954    38.8 |  4.622 % |
c |    187020 |  102597   245618 |   60624   25500   972573    38.1 |  4.647 % |
c |    188160 |  102597   245618 |   66687   26640  1011974    38.0 |  4.647 % |
c |    189868 |  102597   245618 |   73355   28348  1073849    37.9 |  4.647 % |
c |    192430 |  102597   245618 |   80691   30910  1196120    38.7 |  4.647 % |
c |    196274 |  102591   245606 |   88760   34752  1333916    38.4 |  4.653 % |
c |    202040 |  102591   245606 |   97636   40518  1586792    39.2 |  4.653 % |
c |    210691 |  102591   245606 |  107400   49169  1800019    36.6 |  4.653 % |
c |    223667 |  102591   245606 |  118140   62145  2837805    45.7 |  4.653 % |
c |    243128 |  102591   245606 |  129954   81606  5607252    68.7 |  4.653 % |
c ==============================================================================
c Found solution: 27
c ---[   0]---> Sorter-cost:    2     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    252867 |  102647   245768 |   34215   91345  6466967    70.8 |  4.653 % |
c |    252969 |  102647   245768 |   37636   24176  1473265    60.9 |  4.651 % |
c |    253119 |  102647   245768 |   41400   24326  1476562    60.7 |  4.651 % |
c |    253345 |  102647   245768 |   45540   24552  1483153    60.4 |  4.651 % |
c |    253682 |  102647   245768 |   50094   24889  1496566    60.1 |  4.651 % |
c |    254188 |  102647   245768 |   55103   25395  1536884    60.5 |  4.651 % |
c |    254947 |  102647   245768 |   60613   26154  1554276    59.4 |  4.651 % |
c |    256087 |  102647   245768 |   66675   27294  1588653    58.2 |  4.651 % |
c |    257796 |  102647   245768 |   73342   29003  1630466    56.2 |  4.651 % |
c |    260358 |  102525   245486 |   80677   31558  1753312    55.6 |  4.780 % |
c |    264203 |  102446   245313 |   88744   35398  1915675    54.1 |  4.869 % |
c |    269969 |  102446   245313 |   97619   41164  2915278    70.8 |  4.869 % |
c |    278620 |  102446   245313 |  107381   49815  5075380   101.9 |  4.869 % |
c |    291594 |  102446   245313 |  118119   62789  6711273   106.9 |  4.869 % |
c |    311057 |  102446   245313 |  129931   82252  8879602   108.0 |  4.869 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v -v756 -v693 v588 v262 -v241 v56 -v38 v692 v590 -v486 v263 -v246 -v55 -v37 v757 v700 v589 -v485 -v439 -v266 -v245 -v54 -v39 -v758 v694 v594 -v487 -v444 -v264 -v52 v40 v761 v695 -v612 v593 -v488 -v443 -v265 -v248 -v53 -v47 v759 -v696 v611 -v591 v489 -v401 -v249 -v41 -v2 -v760 v613 -v592 -v496 v446 v421 -v400 -v252 -v198 -v171 -v42 -v1 -v734 -v616 v490 v447 v420 -v406 -v385 -v250 -v176 -v43 -v3 -v733 v615 v491 -v450 v422 -v405 -v384 -v273 -v251 -v197 -v175 v137 -v4 v620 v492 -v448 -v425 -v407 -v386 -v366 -v278 -v201 -v155 v136 -v18 -v5 -v735 -v619 -v559 -v510 -v449 v424 v411 -v387 -v365 -v277 -v178 -v154 v138 -v87 -v17 -v12 -v737 -v650 -v617 -v515 v429 -v410 v388 -v202 -v179 -v156 v141 -v86 -v23 -v6 -v649 -v618 -v558 -v514 -v466 v428 -v408 -v395 -v367 -v280 v182 -v157 v140 -v88 -v66 -v22 -v7 -v738 -v562 v426 -v409 -v389 -v369 -v281 v180 v158 -v145 -v91 -v71 -v24 -v8 -v740 v651 v517 -v469 -v427 -v390 -v318 -v284 -v223 -v181 -v165 -v144 -v121 v90 -v70 -v28 -v741 -v653 -v635 -v563 v518 -v470 -v391 -v370 -v317 -v282 v159 -v142 v95 -v27 -v634 -v521 -v372 -v347 -v319 -v283 -v222 v160 -v143 -v120 v94 v73 -v25 -v654 -v519 -v373 -v351 v322 v226 -v161 -v92 v74 -v26 v656 -v636 -v520 v321 -v124 -v93 -v75 v657 v639 v323 -v227 -v125 -v76 -v753 -v703 v64 -v755 v704 v587 -v267 -v240 v60 v754 -v699 -v602 -v242 v59 v50 v762 v598 -v438 -v247 v51 -v710 -v697 -v597 v499 v440 v244 -v46 -v714 v500 -v445 -v253 -v495 v442 -v44 -v729 v614 -v451 v402 -v170 -v728 -v628 -v493 v403 -v199 -v172 -v15 v624 v423 v404 -v361 -v272 -v203 -v177 -v16 -v736 v623 -v437 -v415 v398 v360 -v274 v174 -v11 -v739 -v645 -v509 v433 v399 -v279 v183 v139 -v19 -v743 -v644 -v560 -v511 -v465 v432 -v394 -v368 -v276 -v205 -v168 v153 -v20 -v9 -v742 -v564 -v516 -v371 -v285 -v206 -v169 -v149 -v89 -v65 -v21 v652 v513 -v471 -v392 v375 -v164 -v148 -v116 -v103 -v67 -v32 v655 -v630 v522 -v374 v99 -v72 v659 -v629 -v566 -v346 -v224 -v162 -v122 v98 v69 v658 -v567 -v350 -v320 v228 v77 -v637 -v474 v331 -v126 v638 -v327 -v701 -v599 -v105 v63 v49 v752 -v601 -v271 v48 v770 -v498 -v270 v57 v766 -v497 -v243 -v765 -v709 -v698 -v595 v261 v58 -v713 v441 -v257 -v193 -v625 -v596 v459 v302 -v256 -v192 -v45 -v14 -v627 v455 -v13 -v494 v454 -v434 -v418 -v397 v200 -v730 -v554 -v436 -v419 v396 -v204 -v173 -v731 v621 -v553 -v461 -v414 -v208 -v191 -v167 v150 -v732 v362 -v275 -v207 -v187 -v166 v152 -v747 v622 -v561 -v467 v430 -v412 v363 -v293 -v186 -v100 -v35 -v10 -v646 -v565 -v512 v364 -v289 -v218 -v102 -v36 -v685 -v647 -v569 -v530 -v472 v431 -v393 v379 -v288 v217 -v146 -v31 v648 -v568 v526 -v115 -v68 -v663 -v525 v475 -v348 v328 -v225 -v163 -v147 -v117 v96 v85 -v29 -v631 v473 -v352 v330 v229 -v123 -v81 -v632 v230 -v119 -v97 -v80 v633 -v326 v231 -v127 -v767 -v702 -v600 v333 -v104 v61 v769 -v268 -v258 v260 -v763 -v711 v456 v299 -v269 v715 -v626 v458 -v764 -v417 v301 -v254 -v435 -v416 v194 v717 -v452 -v255 v195 -v188 v718 v196 -v190 v151 -v750 -v453 -v290 -v212 -v34 -v751 -v555 -v460 -v292 -v101 -v33 -v746 v681 -v556 -v527 -v462 -v413 -v382 -v184 v557 -v529 -v468 -v383 -v343 -v744 -v684 -v666 -v573 v464 -v378 v342 -v286 -v185 -v82 -v667 v476 -v329 v219 v84 -v662 -v534 -v523 -v376 -v349 -v287 v220 -v30 v538 -v353 v221 -v118 -v660 -v642 -v604 -v524 v354 v235 -v135 -v78 -v643 -v608 v355 -v324 -v131 -v768 v332 v106 -v62 v706 -v259 v705 v457 v712 v298 -v108 v716 v720 v303 v719 -v189 -v749 v215 -v748 -v291 v216 v677 -v381 v306 -v211 -v528 -v380 v680 -v665 v576 -v209 -v664 v577 v463 -v83 -v745 -v686 -v572 v484 v480 v344 -v641 -v570 -v533 v479 -v377 v345 v238 -v132 -v640 v537 v239 -v134 -v689 -v661 -v603 v234 -v79 -v607 -v325 -v130 v502 -v295 -v109 v707 -v107 v708 v546 -v335 v300 v771 v724 v304 -v214 v213 -v673 v307 v305 -v772 v676 -v773 v575 v574 v682 -v481 -v210 v483 -v687 v237 v236 -v133 -v690 -v571 v535 -v477 v358 -v688 v539 v359 -v605 -v478 v232 -v609 -v128 -v110 v501 -v336 -v334 -v294 v727 v545 -v296 v723 v308 v721 -v672 -v582 -v482 v683 v532 v679 v531 -v357 -v691 -v356 v536 v540 v606 -v233 v610 -v129 -v337 -v114 v726 v503 -v113 v725 v547 -v297 -v669 -v506 v316 v312 v722 v674

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/25374/stat): 25374 (minisat+_script) R 25373 25374 8263 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1785432262 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 0 0 0
Raw data (/proc/25374/statm): 174 3 169 147 0 27 0
[pid=25374] 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=25375
New process pid=25376
New process pid=25377
execve syscall for /bin/sed executable
One traced child (pid=25376) 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=25377) exited with status: 0
One traced child (pid=25375) exited with status: 0
New process pid=25378
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc12/normalized-10:20:4.5:0.5:100.opb

[startup+10.0035 s]
Raw data (loadavg): 0.93 0.97 0.91 2/57 25378
Raw data (/proc/25374/stat): 25374 (minisat+_script) S 25373 25374 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785432262 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25374/statm): 531 226 485 147 0 384 0
[pid=25374] vsize: 2124
Raw data (/proc/25378/stat): 25378 (minisat+_64-bit) R 25374 25374 8263 0 -1 0 4478 0 0 0 959 18 0 0 25 0 1 0 1785432267 18919424 4314 4294967295 134512640 135094434 3221224432 3221223056 134557565 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25378/statm): 4619 4314 145 145 0 4474 0
[pid=25378] vsize: 18476
Current children cumulated CPU time (s) 9.77
Current children cumulated vsize (Kb) 20600

[startup+20.0043 s]
Raw data (loadavg): 0.94 0.97 0.91 2/57 25378
Raw data (/proc/25374/stat): 25374 (minisat+_script) S 25373 25374 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785432262 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25374/statm): 531 226 485 147 0 384 0
[pid=25374] vsize: 2124
Raw data (/proc/25378/stat): 25378 (minisat+_64-bit) R 25374 25374 8263 0 -1 0 4621 0 0 0 1956 20 0 0 25 0 1 0 1785432267 19529728 4457 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25378/statm): 4768 4457 145 145 0 4623 0
[pid=25378] vsize: 19072
Current children cumulated CPU time (s) 19.76
Current children cumulated vsize (Kb) 21196

[startup+30.0051 s]
Raw data (loadavg): 0.95 0.97 0.91 2/57 25378
Raw data (/proc/25374/stat): 25374 (minisat+_script) S 25373 25374 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785432262 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25374/statm): 531 226 485 147 0 384 0
[pid=25374] vsize: 2124
Raw data (/proc/25378/stat): 25378 (minisat+_64-bit) R 25374 25374 8263 0 -1 0 4751 0 0 0 2953 21 0 0 25 0 1 0 1785432267 20049920 4587 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25378/statm): 4895 4587 145 145 0 4750 0
[pid=25378] vsize: 19580
Current children cumulated CPU time (s) 29.74
Current children cumulated vsize (Kb) 21704

[startup+40.007 s]
Raw data (loadavg): 0.96 0.97 0.91 2/57 25378
Raw data (/proc/25374/stat): 25374 (minisat+_script) S 25373 25374 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785432262 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25374/statm): 531 226 485 147 0 384 0
[pid=25374] vsize: 2124
Raw data (/proc/25378/stat): 25378 (minisat+_64-bit) R 25374 25374 8263 0 -1 0 4910 0 0 0 3950 22 0 0 25 0 1 0 1785432267 20742144 4746 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25378/statm): 5064 4746 145 145 0 4919 0
[pid=25378] vsize: 20256
Current children cumulated CPU time (s) 39.72
Current children cumulated vsize (Kb) 22380

[startup+50.0088 s]
Raw data (loadavg): 0.96 0.97 0.91 2/57 25378
Raw data (/proc/25374/stat): 25374 (minisat+_script) S 25373 25374 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785432262 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25374/statm): 531 226 485 147 0 384 0
[pid=25374] vsize: 2124
Raw data (/proc/25378/stat): 25378 (minisat+_64-bit) R 25374 25374 8263 0 -1 0 5131 0 0 0 4945 25 0 0 25 0 1 0 1785432267 21626880 4967 4294967295 134512640 135094434 3221224432 3221223088 134557860 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25378/statm): 5280 4967 145 145 0 5135 0
[pid=25378] vsize: 21120
Current children cumulated CPU time (s) 49.7
Current children cumulated vsize (Kb) 23244

[startup+60.0096 s]
Raw data (loadavg): 0.97 0.97 0.91 2/57 25378
Raw data (/proc/25374/stat): 25374 (minisat+_script) S 25373 25374 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785432262 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25374/statm): 531 226 485 147 0 384 0
[pid=25374] vsize: 2124
Raw data (/proc/25378/stat): 25378 (minisat+_64-bit) R 25374 25374 8263 0 -1 0 5290 0 0 0 5942 27 0 0 25 0 1 0 1785432267 22261760 5126 4294967295 134512640 135094434 3221224432 3221223088 134557879 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25378/statm): 5435 5126 145 145 0 5290 0
[pid=25378] vsize: 21740
Current children cumulated CPU time (s) 59.69
Current children cumulated vsize (Kb) 23864

[startup+70.0115 s]
Raw data (loadavg): 0.97 0.97 0.91 2/57 25378
Raw data (/proc/25374/stat): 25374 (minisat+_script) S 25373 25374 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785432262 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25374/statm): 531 226 485 147 0 384 0
[pid=25374] vsize: 2124
Raw data (/proc/25378/stat): 25378 (minisat+_64-bit) R 25374 25374 8263 0 -1 0 5566 0 0 0 6937 29 0 0 25 0 1 0 1785432267 23375872 5402 4294967295 134512640 135094434 3221224432 3221223056 134557714 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25378/statm): 5707 5402 145 145 0 5562 0
[pid=25378] vsize: 22828
Current children cumulated CPU time (s) 69.66
Current children cumulated vsize (Kb) 24952

[startup+80.0133 s]
Raw data (loadavg): 0.98 0.97 0.91 2/57 25378
Raw data (/proc/25374/stat): 25374 (minisat+_script) S 25373 25374 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785432262 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25374/statm): 531 226 485 147 0 384 0
[pid=25374] vsize: 2124
Raw data (/proc/25378/stat): 25378 (minisat+_64-bit) R 25374 25374 8263 0 -1 0 5829 0 0 0 7932 31 0 0 25 0 1 0 1785432267 24571904 5665 4294967295 134512640 135094434 3221224432 3221223104 134556507 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25378/statm): 5999 5665 145 145 0 5854 0
[pid=25378] vsize: 23996
Current children cumulated CPU time (s) 79.63
Current children cumulated vsize (Kb) 26120

[startup+90.0152 s]
Raw data (loadavg): 0.98 0.97 0.91 2/57 25378
Raw data (/proc/25374/stat): 25374 (minisat+_script) S 25373 25374 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785432262 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25374/statm): 531 226 485 147 0 384 0
[pid=25374] vsize: 2124
Raw data (/proc/25378/stat): 25378 (minisat+_64-bit) R 25374 25374 8263 0 -1 0 5994 0 0 0 8928 33 0 0 25 0 1 0 1785432267 25231360 5830 4294967295 134512640 135094434 3221224432 3221223056 134557593 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25378/statm): 6160 5830 145 145 0 6015 0
[pid=25378] vsize: 24640
Current children cumulated CPU time (s) 89.61
Current children cumulated vsize (Kb) 26764

[startup+100.016 s]
Raw data (loadavg): 0.98 0.97 0.91 2/57 25378
Raw data (/proc/25374/stat): 25374 (minisat+_script) S 25373 25374 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785432262 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25374/statm): 531 226 485 147 0 384 0
[pid=25374] vsize: 2124
Raw data (/proc/25378/stat): 25378 (minisat+_64-bit) R 25374 25374 8263 0 -1 0 6293 0 0 0 9924 34 0 0 25 0 1 0 1785432267 26456064 6129 4294967295 134512640 135094434 3221224432 3221223088 134561479 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25378/statm): 6459 6129 145 145 0 6314 0
[pid=25378] vsize: 25836
Current children cumulated CPU time (s) 99.58
Current children cumulated vsize (Kb) 27960

[startup+110.017 s]
Raw data (loadavg): 0.98 0.97 0.91 2/57 25378
Raw data (/proc/25374/stat): 25374 (minisat+_script) S 25373 25374 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785432262 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25374/statm): 531 226 485 147 0 384 0
[pid=25374] vsize: 2124
Raw data (/proc/25378/stat): 25378 (minisat+_64-bit) R 25374 25374 8263 0 -1 0 6515 0 0 0 10920 37 0 0 25 0 1 0 1785432267 27353088 6351 4294967295 134512640 135094434 3221224432 3221223024 134556862 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25378/statm): 6678 6351 145 145 0 6533 0
[pid=25378] vsize: 26712
Current children cumulated CPU time (s) 109.57
Current children cumulated vsize (Kb) 28836

[startup+120.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25378
Raw data (/proc/25374/stat): 25374 (minisat+_script) S 25373 25374 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785432262 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25374/statm): 531 226 485 147 0 384 0
[pid=25374] vsize: 2124
Raw data (/proc/25378/stat): 25378 (minisat+_64-bit) R 25374 25374 8263 0 -1 0 6863 0 0 0 11913 39 0 0 25 0 1 0 1785432267 28766208 6699 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25378/statm): 7023 6699 145 145 0 6878 0
[pid=25378] vsize: 28092
Current children cumulated CPU time (s) 119.52
Current children cumulated vsize (Kb) 30216

[startup+130.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25378
Raw data (/proc/25374/stat): 25374 (minisat+_script) S 25373 25374 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785432262 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25374/statm): 531 226 485 147 0 384 0
[pid=25374] vsize: 2124
Raw data (/proc/25378/stat): 25378 (minisat+_64-bit) R 25374 25374 8263 0 -1 0 7287 0 0 0 12907 43 0 0 25 0 1 0 1785432267 30498816 7123 4294967295 134512640 135094434 3221224432 3221223024 134557334 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25378/statm): 7446 7123 145 145 0 7301 0
[pid=25378] vsize: 29784
Current children cumulated CPU time (s) 129.5
Current children cumulated vsize (Kb) 31908

[startup+140.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25378
Raw data (/proc/25374/stat): 25374 (minisat+_script) S 25373 25374 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785432262 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25374/statm): 531 226 485 147 0 384 0
[pid=25374] vsize: 2124
Raw data (/proc/25378/stat): 25378 (minisat+_64-bit) R 25374 25374 8263 0 -1 0 7725 0 0 0 13899 45 0 0 25 0 1 0 1785432267 32284672 7561 4294967295 134512640 135094434 3221224432 3221223024 134557416 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25378/statm): 7882 7561 145 145 0 7737 0
[pid=25378] vsize: 31528
Current children cumulated CPU time (s) 139.44
Current children cumulated vsize (Kb) 33652

[startup+150.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25378
Raw data (/proc/25374/stat): 25374 (minisat+_script) S 25373 25374 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785432262 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25374/statm): 531 226 485 147 0 384 0
[pid=25374] vsize: 2124
Raw data (/proc/25378/stat): 25378 (minisat+_64-bit) R 25374 25374 8263 0 -1 0 8211 0 0 0 14893 48 0 0 25 0 1 0 1785432267 34271232 8047 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25378/statm): 8367 8047 145 145 0 8222 0
[pid=25378] vsize: 33468
Current children cumulated CPU time (s) 149.41
Current children cumulated vsize (Kb) 35592

[startup+160.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25378
Raw data (/proc/25374/stat): 25374 (minisat+_script) S 25373 25374 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785432262 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25374/statm): 531 226 485 147 0 384 0
[pid=25374] vsize: 2124
Raw data (/proc/25378/stat): 25378 (minisat+_64-bit) R 25374 25374 8263 0 -1 0 8703 0 0 0 15886 51 0 0 25 0 1 0 1785432267 36282368 8539 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25378/statm): 8858 8539 145 145 0 8713 0
[pid=25378] vsize: 35432
Current children cumulated CPU time (s) 159.37
Current children cumulated vsize (Kb) 37556

[startup+170.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25378
Raw data (/proc/25374/stat): 25374 (minisat+_script) S 25373 25374 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785432262 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25374/statm): 531 226 485 147 0 384 0
[pid=25374] vsize: 2124
Raw data (/proc/25378/stat): 25378 (minisat+_64-bit) R 25374 25374 8263 0 -1 0 9192 0 0 0 16878 53 0 0 25 0 1 0 1785432267 38281216 9028 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25378/statm): 9346 9028 145 145 0 9201 0
[pid=25378] vsize: 37384
Current children cumulated CPU time (s) 169.31
Current children cumulated vsize (Kb) 39508

[startup+180.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25378
Raw data (/proc/25374/stat): 25374 (minisat+_script) S 25373 25374 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785432262 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25374/statm): 531 226 485 147 0 384 0
[pid=25374] vsize: 2124
Raw data (/proc/25378/stat): 25378 (minisat+_64-bit) R 25374 25374 8263 0 -1 0 9673 0 0 0 17870 56 0 0 25 0 1 0 1785432267 40247296 9509 4294967295 134512640 135094434 3221224432 3221223024 134557357 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25378/statm): 9826 9509 145 145 0 9681 0
[pid=25378] vsize: 39304
Current children cumulated CPU time (s) 179.26
Current children cumulated vsize (Kb) 41428

[startup+190.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25378
Raw data (/proc/25374/stat): 25374 (minisat+_script) S 25373 25374 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785432262 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25374/statm): 531 226 485 147 0 384 0
[pid=25374] vsize: 2124
Raw data (/proc/25378/stat): 25378 (minisat+_64-bit) R 25374 25374 8263 0 -1 0 9958 0 0 0 18864 59 0 0 25 0 1 0 1785432267 41406464 9794 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25378/statm): 10109 9794 145 145 0 9964 0
[pid=25378] vsize: 40436
Current children cumulated CPU time (s) 189.23
Current children cumulated vsize (Kb) 42560

[startup+200.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25378
Raw data (/proc/25374/stat): 25374 (minisat+_script) S 25373 25374 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785432262 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25374/statm): 531 226 485 147 0 384 0
[pid=25374] vsize: 2124
Raw data (/proc/25378/stat): 25378 (minisat+_64-bit) R 25374 25374 8263 0 -1 0 10197 0 0 0 19859 61 0 0 25 0 1 0 1785432267 42373120 10033 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25378/statm): 10345 10033 145 145 0 10200 0
[pid=25378] vsize: 41380
Current children cumulated CPU time (s) 199.2
Current children cumulated vsize (Kb) 43504

[startup+210.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25378
Raw data (/proc/25374/stat): 25374 (minisat+_script) S 25373 25374 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785432262 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25374/statm): 531 226 485 147 0 384 0
[pid=25374] vsize: 2124
Raw data (/proc/25378/stat): 25378 (minisat+_64-bit) R 25374 25374 8263 0 -1 0 10418 0 0 0 20854 63 0 0 25 0 1 0 1785432267 43270144 10254 4294967295 134512640 135094434 3221224432 3221223056 134557696 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25378/statm): 10564 10254 145 145 0 10419 0
[pid=25378] vsize: 42256
Current children cumulated CPU time (s) 209.17
Current children cumulated vsize (Kb) 44380

[startup+220.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25378
Raw data (/proc/25374/stat): 25374 (minisat+_script) S 25373 25374 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785432262 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25374/statm): 531 226 485 147 0 384 0
[pid=25374] vsize: 2124
Raw data (/proc/25378/stat): 25378 (minisat+_64-bit) R 25374 25374 8263 0 -1 0 10655 0 0 0 21850 65 0 0 25 0 1 0 1785432267 44494848 10491 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25378/statm): 10863 10491 145 145 0 10718 0
[pid=25378] vsize: 43452
Current children cumulated CPU time (s) 219.15
Current children cumulated vsize (Kb) 45576

[startup+230.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25378
Raw data (/proc/25374/stat): 25374 (minisat+_script) S 25373 25374 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785432262 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25374/statm): 531 226 485 147 0 384 0
[pid=25374] vsize: 2124
Raw data (/proc/25378/stat): 25378 (minisat+_64-bit) R 25374 25374 8263 0 -1 0 10905 0 0 0 22846 66 0 0 25 0 1 0 1785432267 45510656 10741 4294967295 134512640 135094434 3221224432 3221223024 134552003 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25378/statm): 11111 10741 145 145 0 10966 0
[pid=25378] vsize: 44444
Current children cumulated CPU time (s) 229.12
Current children cumulated vsize (Kb) 46568

[startup+240.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25378
Raw data (/proc/25374/stat): 25374 (minisat+_script) S 25373 25374 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785432262 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25374/statm): 531 226 485 147 0 384 0
[pid=25374] vsize: 2124
Raw data (/proc/25378/stat): 25378 (minisat+_64-bit) R 25374 25374 8263 0 -1 0 11149 0 0 0 23842 67 0 0 25 0 1 0 1785432267 46510080 10985 4294967295 134512640 135094434 3221224432 3221223024 134557208 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25378/statm): 11355 10985 145 145 0 11210 0
[pid=25378] vsize: 45420
Current children cumulated CPU time (s) 239.09
Current children cumulated vsize (Kb) 47544

[startup+250.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25378
Raw data (/proc/25374/stat): 25374 (minisat+_script) S 25373 25374 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785432262 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25374/statm): 531 226 485 147 0 384 0
[pid=25374] vsize: 2124
Raw data (/proc/25378/stat): 25378 (minisat+_64-bit) R 25374 25374 8263 0 -1 0 11460 0 0 0 24837 69 0 0 25 0 1 0 1785432267 47775744 11296 4294967295 134512640 135094434 3221224432 3221223024 134556851 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25378/statm): 11664 11296 145 145 0 11519 0
[pid=25378] vsize: 46656
Current children cumulated CPU time (s) 249.06
Current children cumulated vsize (Kb) 48780

[startup+260.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25378
Raw data (/proc/25374/stat): 25374 (minisat+_script) S 25373 25374 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785432262 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25374/statm): 531 226 485 147 0 384 0
[pid=25374] vsize: 2124
Raw data (/proc/25378/stat): 25378 (minisat+_64-bit) R 25374 25374 8263 0 -1 0 11719 0 0 0 25833 70 0 0 25 0 1 0 1785432267 48828416 11555 4294967295 134512640 135094434 3221224432 3221223056 134557717 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25378/statm): 11921 11555 145 145 0 11776 0
[pid=25378] vsize: 47684
Current children cumulated CPU time (s) 259.03
Current children cumulated vsize (Kb) 49808

[startup+270.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25378
Raw data (/proc/25374/stat): 25374 (minisat+_script) S 25373 25374 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785432262 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25374/statm): 531 226 485 147 0 384 0
[pid=25374] vsize: 2124
Raw data (/proc/25378/stat): 25378 (minisat+_64-bit) R 25374 25374 8263 0 -1 0 12227 0 0 0 26825 73 0 0 25 0 1 0 1785432267 50900992 12063 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25378/statm): 12427 12063 145 145 0 12282 0
[pid=25378] vsize: 49708
Current children cumulated CPU time (s) 268.98
Current children cumulated vsize (Kb) 51832

[startup+280.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25378
Raw data (/proc/25374/stat): 25374 (minisat+_script) S 25373 25374 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785432262 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25374/statm): 531 226 485 147 0 384 0
[pid=25374] vsize: 2124
Raw data (/proc/25378/stat): 25378 (minisat+_64-bit) R 25374 25374 8263 0 -1 0 12731 0 0 0 27817 77 0 0 25 0 1 0 1785432267 52961280 12567 4294967295 134512640 135094434 3221224432 3221223088 134557818 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25378/statm): 12930 12567 145 145 0 12785 0
[pid=25378] vsize: 51720
Current children cumulated CPU time (s) 278.94
Current children cumulated vsize (Kb) 53844

[startup+290.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25378
Raw data (/proc/25374/stat): 25374 (minisat+_script) S 25373 25374 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785432262 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25374/statm): 531 226 485 147 0 384 0
[pid=25374] vsize: 2124
Raw data (/proc/25378/stat): 25378 (minisat+_64-bit) R 25374 25374 8263 0 -1 0 13116 0 0 0 28810 80 0 0 25 0 1 0 1785432267 54517760 12952 4294967295 134512640 135094434 3221224432 3221223056 134557612 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25378/statm): 13310 12952 145 145 0 13165 0
[pid=25378] vsize: 53240
Current children cumulated CPU time (s) 288.9
Current children cumulated vsize (Kb) 55364

[startup+300.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25378
Raw data (/proc/25374/stat): 25374 (minisat+_script) S 25373 25374 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785432262 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25374/statm): 531 226 485 147 0 384 0
[pid=25374] vsize: 2124
Raw data (/proc/25378/stat): 25378 (minisat+_64-bit) R 25374 25374 8263 0 -1 0 13116 0 0 0 29809 81 0 0 25 0 1 0 1785432267 54517760 12952 4294967295 134512640 135094434 3221224432 3221223056 134557696 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25378/statm): 13310 12952 145 145 0 13165 0
[pid=25378] vsize: 53240
Current children cumulated CPU time (s) 298.9
Current children cumulated vsize (Kb) 55364

[startup+310.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25378
Raw data (/proc/25374/stat): 25374 (minisat+_script) S 25373 25374 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785432262 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25374/statm): 531 226 485 147 0 384 0
[pid=25374] vsize: 2124
Raw data (/proc/25378/stat): 25378 (minisat+_64-bit) R 25374 25374 8263 0 -1 0 13116 0 0 0 30809 81 0 0 25 0 1 0 1785432267 54517760 12952 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25378/statm): 13310 12952 145 145 0 13165 0
[pid=25378] vsize: 53240
Current children cumulated CPU time (s) 308.9
Current children cumulated vsize (Kb) 55364

[startup+320.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25378
Raw data (/proc/25374/stat): 25374 (minisat+_script) S 25373 25374 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785432262 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25374/statm): 531 226 485 147 0 384 0
[pid=25374] vsize: 2124
Raw data (/proc/25378/stat): 25378 (minisat+_64-bit) R 25374 25374 8263 0 -1 0 13116 0 0 0 31809 82 0 0 25 0 1 0 1785432267 54517760 12952 4294967295 134512640 135094434 3221224432 3221223088 134558029 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25378/statm): 13310 12952 145 145 0 13165 0
[pid=25378] vsize: 53240
Current children cumulated CPU time (s) 318.91
Current children cumulated vsize (Kb) 55364

[startup+330.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25378
Raw data (/proc/25374/stat): 25374 (minisat+_script) S 25373 25374 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785432262 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25374/statm): 531 226 485 147 0 384 0
[pid=25374] vsize: 2124
Raw data (/proc/25378/stat): 25378 (minisat+_64-bit) R 25374 25374 8263 0 -1 0 13116 0 0 0 32808 82 0 0 25 0 1 0 1785432267 54517760 12952 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25378/statm): 13310 12952 145 145 0 13165 0
[pid=25378] vsize: 53240
Current children cumulated CPU time (s) 328.9
Current children cumulated vsize (Kb) 55364

[startup+340.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25378
Raw data (/proc/25374/stat): 25374 (minisat+_script) S 25373 25374 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785432262 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25374/statm): 531 226 485 147 0 384 0
[pid=25374] vsize: 2124
Raw data (/proc/25378/stat): 25378 (minisat+_64-bit) R 25374 25374 8263 0 -1 0 13116 0 0 0 33808 82 0 0 25 0 1 0 1785432267 54517760 12952 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25378/statm): 13310 12952 145 145 0 13165 0
[pid=25378] vsize: 53240
Current children cumulated CPU time (s) 338.9
Current children cumulated vsize (Kb) 55364

[startup+350.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25378
Raw data (/proc/25374/stat): 25374 (minisat+_script) S 25373 25374 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785432262 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25374/statm): 531 226 485 147 0 384 0
[pid=25374] vsize: 2124
Raw data (/proc/25378/stat): 25378 (minisat+_64-bit) R 25374 25374 8263 0 -1 0 13116 0 0 0 34809 82 0 0 25 0 1 0 1785432267 54517760 12952 4294967295 134512640 135094434 3221224432 3221223088 134557860 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25378/statm): 13310 12952 145 145 0 13165 0
[pid=25378] vsize: 53240
Current children cumulated CPU time (s) 348.91
Current children cumulated vsize (Kb) 55364

[startup+360.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25378
Raw data (/proc/25374/stat): 25374 (minisat+_script) S 25373 25374 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785432262 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25374/statm): 531 226 485 147 0 384 0
[pid=25374] vsize: 2124
Raw data (/proc/25378/stat): 25378 (minisat+_64-bit) R 25374 25374 8263 0 -1 0 13116 0 0 0 35809 83 0 0 25 0 1 0 1785432267 54517760 12952 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25378/statm): 13310 12952 145 145 0 13165 0
[pid=25378] vsize: 53240
Current children cumulated CPU time (s) 358.92
Current children cumulated vsize (Kb) 55364

[startup+370.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25378
Raw data (/proc/25374/stat): 25374 (minisat+_script) S 25373 25374 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785432262 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25374/statm): 531 226 485 147 0 384 0
[pid=25374] vsize: 2124
Raw data (/proc/25378/stat): 25378 (minisat+_64-bit) R 25374 25374 8263 0 -1 0 13116 0 0 0 36809 83 0 0 25 0 1 0 1785432267 54517760 12952 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25378/statm): 13310 12952 145 145 0 13165 0
[pid=25378] vsize: 53240
Current children cumulated CPU time (s) 368.92
Current children cumulated vsize (Kb) 55364

[startup+380.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25378
Raw data (/proc/25374/stat): 25374 (minisat+_script) S 25373 25374 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785432262 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25374/statm): 531 226 485 147 0 384 0
[pid=25374] vsize: 2124
Raw data (/proc/25378/stat): 25378 (minisat+_64-bit) R 25374 25374 8263 0 -1 0 13116 0 0 0 37809 83 0 0 25 0 1 0 1785432267 54517760 12952 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25378/statm): 13310 12952 145 145 0 13165 0
[pid=25378] vsize: 53240
Current children cumulated CPU time (s) 378.92
Current children cumulated vsize (Kb) 55364

[startup+390.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25378
Raw data (/proc/25374/stat): 25374 (minisat+_script) S 25373 25374 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785432262 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25374/statm): 531 226 485 147 0 384 0
[pid=25374] vsize: 2124
Raw data (/proc/25378/stat): 25378 (minisat+_64-bit) R 25374 25374 8263 0 -1 0 13116 0 0 0 38809 83 0 0 25 0 1 0 1785432267 54517760 12952 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25378/statm): 13310 12952 145 145 0 13165 0
[pid=25378] vsize: 53240
Current children cumulated CPU time (s) 388.92
Current children cumulated vsize (Kb) 55364

[startup+400.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25378
Raw data (/proc/25374/stat): 25374 (minisat+_script) S 25373 25374 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785432262 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25374/statm): 531 226 485 147 0 384 0
[pid=25374] vsize: 2124
Raw data (/proc/25378/stat): 25378 (minisat+_64-bit) R 25374 25374 8263 0 -1 0 13116 0 0 0 39810 83 0 0 25 0 1 0 1785432267 54517760 12952 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25378/statm): 13310 12952 145 145 0 13165 0
[pid=25378] vsize: 53240
Current children cumulated CPU time (s) 398.93
Current children cumulated vsize (Kb) 55364

[startup+410.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25378
Raw data (/proc/25374/stat): 25374 (minisat+_script) S 25373 25374 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785432262 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25374/statm): 531 226 485 147 0 384 0
[pid=25374] vsize: 2124
Raw data (/proc/25378/stat): 25378 (minisat+_64-bit) R 25374 25374 8263 0 -1 0 13116 0 0 0 40810 83 0 0 25 0 1 0 1785432267 54517760 12952 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25378/statm): 13310 12952 145 145 0 13165 0
[pid=25378] vsize: 53240
Current children cumulated CPU time (s) 408.93
Current children cumulated vsize (Kb) 55364

[startup+420.051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25378
Raw data (/proc/25374/stat): 25374 (minisat+_script) S 25373 25374 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785432262 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25374/statm): 531 226 485 147 0 384 0
[pid=25374] vsize: 2124
Raw data (/proc/25378/stat): 25378 (minisat+_64-bit) R 25374 25374 8263 0 -1 0 13116 0 0 0 41810 83 0 0 25 0 1 0 1785432267 54345728 12910 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25378/statm): 13268 12910 145 145 0 13123 0
[pid=25378] vsize: 53072
Current children cumulated CPU time (s) 418.93
Current children cumulated vsize (Kb) 55196

[startup+430.051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25378
Raw data (/proc/25374/stat): 25374 (minisat+_script) S 25373 25374 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785432262 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25374/statm): 531 226 485 147 0 384 0
[pid=25374] vsize: 2124
Raw data (/proc/25378/stat): 25378 (minisat+_64-bit) R 25374 25374 8263 0 -1 0 13116 0 0 0 42810 83 0 0 25 0 1 0 1785432267 54345728 12910 4294967295 134512640 135094434 3221224432 3221223056 134557650 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25378/statm): 13268 12910 145 145 0 13123 0
[pid=25378] vsize: 53072
Current children cumulated CPU time (s) 428.93
Current children cumulated vsize (Kb) 55196

[startup+440.053 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25378
Raw data (/proc/25374/stat): 25374 (minisat+_script) S 25373 25374 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785432262 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25374/statm): 531 226 485 147 0 384 0
[pid=25374] vsize: 2124
Raw data (/proc/25378/stat): 25378 (minisat+_64-bit) R 25374 25374 8263 0 -1 0 13116 0 0 0 43810 83 0 0 25 0 1 0 1785432267 54345728 12910 4294967295 134512640 135094434 3221224432 3221223024 134557500 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25378/statm): 13268 12910 145 145 0 13123 0
[pid=25378] vsize: 53072
Current children cumulated CPU time (s) 438.93
Current children cumulated vsize (Kb) 55196

[startup+450.054 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25378
Raw data (/proc/25374/stat): 25374 (minisat+_script) S 25373 25374 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785432262 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25374/statm): 531 226 485 147 0 384 0
[pid=25374] vsize: 2124
Raw data (/proc/25378/stat): 25378 (minisat+_64-bit) R 25374 25374 8263 0 -1 0 13118 0 0 0 44811 83 0 0 25 0 1 0 1785432267 54345728 12912 4294967295 134512640 135094434 3221224432 3221223088 134558420 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25378/statm): 13268 12912 145 145 0 13123 0
[pid=25378] vsize: 53072
Current children cumulated CPU time (s) 448.94
Current children cumulated vsize (Kb) 55196

[startup+460.055 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25378
Raw data (/proc/25374/stat): 25374 (minisat+_script) S 25373 25374 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785432262 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25374/statm): 531 226 485 147 0 384 0
[pid=25374] vsize: 2124
Raw data (/proc/25378/stat): 25378 (minisat+_64-bit) R 25374 25374 8263 0 -1 0 13118 0 0 0 45811 83 0 0 25 0 1 0 1785432267 54345728 12912 4294967295 134512640 135094434 3221224432 3221223056 134557630 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25378/statm): 13268 12912 145 145 0 13123 0
[pid=25378] vsize: 53072
Current children cumulated CPU time (s) 458.94
Current children cumulated vsize (Kb) 55196

[startup+470.057 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25378
Raw data (/proc/25374/stat): 25374 (minisat+_script) S 25373 25374 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785432262 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25374/statm): 531 226 485 147 0 384 0
[pid=25374] vsize: 2124
Raw data (/proc/25378/stat): 25378 (minisat+_64-bit) R 25374 25374 8263 0 -1 0 13118 0 0 0 46810 84 0 0 25 0 1 0 1785432267 54345728 12912 4294967295 134512640 135094434 3221224432 3221223088 134558016 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25378/statm): 13268 12912 145 145 0 13123 0
[pid=25378] vsize: 53072
Current children cumulated CPU time (s) 468.94
Current children cumulated vsize (Kb) 55196

[startup+480.058 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25378
Raw data (/proc/25374/stat): 25374 (minisat+_script) S 25373 25374 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785432262 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25374/statm): 531 226 485 147 0 384 0
[pid=25374] vsize: 2124
Raw data (/proc/25378/stat): 25378 (minisat+_64-bit) R 25374 25374 8263 0 -1 0 13118 0 0 0 47810 85 0 0 25 0 1 0 1785432267 54345728 12912 4294967295 134512640 135094434 3221224432 3221223024 134557219 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25378/statm): 13268 12912 145 145 0 13123 0
[pid=25378] vsize: 53072
Current children cumulated CPU time (s) 478.95
Current children cumulated vsize (Kb) 55196

[startup+490.058 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25378
Raw data (/proc/25374/stat): 25374 (minisat+_script) S 25373 25374 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785432262 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25374/statm): 531 226 485 147 0 384 0
[pid=25374] vsize: 2124
Raw data (/proc/25378/stat): 25378 (minisat+_64-bit) R 25374 25374 8263 0 -1 0 13118 0 0 0 48809 85 0 0 25 0 1 0 1785432267 54345728 12912 4294967295 134512640 135094434 3221224432 3221223072 134558269 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25378/statm): 13268 12912 145 145 0 13123 0
[pid=25378] vsize: 53072
Current children cumulated CPU time (s) 488.94
Current children cumulated vsize (Kb) 55196

[startup+500.059 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25378
Raw data (/proc/25374/stat): 25374 (minisat+_script) S 25373 25374 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785432262 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25374/statm): 531 226 485 147 0 384 0
[pid=25374] vsize: 2124
Raw data (/proc/25378/stat): 25378 (minisat+_64-bit) R 25374 25374 8263 0 -1 0 13118 0 0 0 49809 86 0 0 25 0 1 0 1785432267 54345728 12912 4294967295 134512640 135094434 3221224432 3221223088 134557866 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25378/statm): 13268 12912 145 145 0 13123 0
[pid=25378] vsize: 53072
Current children cumulated CPU time (s) 498.95
Current children cumulated vsize (Kb) 55196

[startup+510.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25378
Raw data (/proc/25374/stat): 25374 (minisat+_script) S 25373 25374 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785432262 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25374/statm): 531 226 485 147 0 384 0
[pid=25374] vsize: 2124
Raw data (/proc/25378/stat): 25378 (minisat+_64-bit) R 25374 25374 8263 0 -1 0 13118 0 0 0 50809 86 0 0 25 0 1 0 1785432267 54345728 12912 4294967295 134512640 135094434 3221224432 3221223088 134558225 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25378/statm): 13268 12912 145 145 0 13123 0
[pid=25378] vsize: 53072
Current children cumulated CPU time (s) 508.95
Current children cumulated vsize (Kb) 55196

[startup+520.062 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25378
Raw data (/proc/25374/stat): 25374 (minisat+_script) S 25373 25374 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785432262 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25374/statm): 531 226 485 147 0 384 0
[pid=25374] vsize: 2124
Raw data (/proc/25378/stat): 25378 (minisat+_64-bit) R 25374 25374 8263 0 -1 0 13118 0 0 0 51809 86 0 0 25 0 1 0 1785432267 54345728 12912 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25378/statm): 13268 12912 145 145 0 13123 0
[pid=25378] vsize: 53072
Current children cumulated CPU time (s) 518.95
Current children cumulated vsize (Kb) 55196

[startup+530.063 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25378
Raw data (/proc/25374/stat): 25374 (minisat+_script) S 25373 25374 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785432262 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25374/statm): 531 226 485 147 0 384 0
[pid=25374] vsize: 2124
Raw data (/proc/25378/stat): 25378 (minisat+_64-bit) R 25374 25374 8263 0 -1 0 13118 0 0 0 52808 86 0 0 25 0 1 0 1785432267 54345728 12912 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25378/statm): 13268 12912 145 145 0 13123 0
[pid=25378] vsize: 53072
Current children cumulated CPU time (s) 528.94
Current children cumulated vsize (Kb) 55196

[startup+540.065 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25378
Raw data (/proc/25374/stat): 25374 (minisat+_script) S 25373 25374 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785432262 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25374/statm): 531 226 485 147 0 384 0
[pid=25374] vsize: 2124
Raw data (/proc/25378/stat): 25378 (minisat+_64-bit) R 25374 25374 8263 0 -1 0 13118 0 0 0 53808 86 0 0 25 0 1 0 1785432267 54345728 12912 4294967295 134512640 135094434 3221224432 3221223104 134555842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25378/statm): 13268 12912 145 145 0 13123 0
[pid=25378] vsize: 53072
Current children cumulated CPU time (s) 538.94
Current children cumulated vsize (Kb) 55196

[startup+550.065 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25378
Raw data (/proc/25374/stat): 25374 (minisat+_script) S 25373 25374 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785432262 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25374/statm): 531 226 485 147 0 384 0
[pid=25374] vsize: 2124
Raw data (/proc/25378/stat): 25378 (minisat+_64-bit) R 25374 25374 8263 0 -1 0 13118 0 0 0 54808 87 0 0 25 0 1 0 1785432267 54345728 12912 4294967295 134512640 135094434 3221224432 3221223068 134557560 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25378/statm): 13268 12912 145 145 0 13123 0
[pid=25378] vsize: 53072
Current children cumulated CPU time (s) 548.95
Current children cumulated vsize (Kb) 55196

[startup+560.066 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25378
Raw data (/proc/25374/stat): 25374 (minisat+_script) S 25373 25374 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785432262 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25374/statm): 531 226 485 147 0 384 0
[pid=25374] vsize: 2124
Raw data (/proc/25378/stat): 25378 (minisat+_64-bit) R 25374 25374 8263 0 -1 0 13118 0 0 0 55809 87 0 0 25 0 1 0 1785432267 54345728 12912 4294967295 134512640 135094434 3221224432 3221223088 134558402 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25378/statm): 13268 12912 145 145 0 13123 0
[pid=25378] vsize: 53072
Current children cumulated CPU time (s) 558.96
Current children cumulated vsize (Kb) 55196

[startup+570.068 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25378
Raw data (/proc/25374/stat): 25374 (minisat+_script) S 25373 25374 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785432262 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25374/statm): 531 226 485 147 0 384 0
[pid=25374] vsize: 2124
Raw data (/proc/25378/stat): 25378 (minisat+_64-bit) R 25374 25374 8263 0 -1 0 13118 0 0 0 56809 87 0 0 25 0 1 0 1785432267 54345728 12912 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25378/statm): 13268 12912 145 145 0 13123 0
[pid=25378] vsize: 53072
Current children cumulated CPU time (s) 568.96
Current children cumulated vsize (Kb) 55196

[startup+580.069 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25378
Raw data (/proc/25374/stat): 25374 (minisat+_script) S 25373 25374 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785432262 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25374/statm): 531 226 485 147 0 384 0
[pid=25374] vsize: 2124
Raw data (/proc/25378/stat): 25378 (minisat+_64-bit) R 25374 25374 8263 0 -1 0 13118 0 0 0 57809 87 0 0 25 0 1 0 1785432267 54345728 12912 4294967295 134512640 135094434 3221224432 3221223088 134558011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25378/statm): 13268 12912 145 145 0 13123 0
[pid=25378] vsize: 53072
Current children cumulated CPU time (s) 578.96
Current children cumulated vsize (Kb) 55196

[startup+590.071 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25378
Raw data (/proc/25374/stat): 25374 (minisat+_script) S 25373 25374 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785432262 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25374/statm): 531 226 485 147 0 384 0
[pid=25374] vsize: 2124
Raw data (/proc/25378/stat): 25378 (minisat+_64-bit) R 25374 25374 8263 0 -1 0 13118 0 0 0 58809 87 0 0 25 0 1 0 1785432267 54345728 12912 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25378/statm): 13268 12912 145 145 0 13123 0
[pid=25378] vsize: 53072
Current children cumulated CPU time (s) 588.96
Current children cumulated vsize (Kb) 55196

[startup+600.072 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25378
Raw data (/proc/25374/stat): 25374 (minisat+_script) S 25373 25374 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785432262 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25374/statm): 531 226 485 147 0 384 0
[pid=25374] vsize: 2124
Raw data (/proc/25378/stat): 25378 (minisat+_64-bit) R 25374 25374 8263 0 -1 0 13118 0 0 0 59810 87 0 0 25 0 1 0 1785432267 54345728 12912 4294967295 134512640 135094434 3221224432 3221223024 134552008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25378/statm): 13268 12912 145 145 0 13123 0
[pid=25378] vsize: 53072
Current children cumulated CPU time (s) 598.97
Current children cumulated vsize (Kb) 55196

[startup+610.072 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25378
Raw data (/proc/25374/stat): 25374 (minisat+_script) S 25373 25374 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785432262 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25374/statm): 531 226 485 147 0 384 0
[pid=25374] vsize: 2124
Raw data (/proc/25378/stat): 25378 (minisat+_64-bit) R 25374 25374 8263 0 -1 0 13118 0 0 0 60810 87 0 0 25 0 1 0 1785432267 54345728 12912 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25378/statm): 13268 12912 145 145 0 13123 0
[pid=25378] vsize: 53072
Current children cumulated CPU time (s) 608.97
Current children cumulated vsize (Kb) 55196

[startup+620.073 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25378
Raw data (/proc/25374/stat): 25374 (minisat+_script) S 25373 25374 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785432262 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25374/statm): 531 226 485 147 0 384 0
[pid=25374] vsize: 2124
Raw data (/proc/25378/stat): 25378 (minisat+_64-bit) R 25374 25374 8263 0 -1 0 13118 0 0 0 61810 87 0 0 25 0 1 0 1785432267 54345728 12912 4294967295 134512640 135094434 3221224432 3221223088 134557893 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25378/statm): 13268 12912 145 145 0 13123 0
[pid=25378] vsize: 53072
Current children cumulated CPU time (s) 618.97
Current children cumulated vsize (Kb) 55196

[startup+630.074 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25378
Raw data (/proc/25374/stat): 25374 (minisat+_script) S 25373 25374 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785432262 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25374/statm): 531 226 485 147 0 384 0
[pid=25374] vsize: 2124
Raw data (/proc/25378/stat): 25378 (minisat+_64-bit) R 25374 25374 8263 0 -1 0 13121 0 0 0 62810 87 0 0 25 0 1 0 1785432267 54345728 12915 4294967295 134512640 135094434 3221224432 3221223104 134555574 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25378/statm): 13268 12915 145 145 0 13123 0
[pid=25378] vsize: 53072
Current children cumulated CPU time (s) 628.97
Current children cumulated vsize (Kb) 55196

[startup+640.076 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25378
Raw data (/proc/25374/stat): 25374 (minisat+_script) S 25373 25374 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785432262 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25374/statm): 531 226 485 147 0 384 0
[pid=25374] vsize: 2124
Raw data (/proc/25378/stat): 25378 (minisat+_64-bit) R 25374 25374 8263 0 -1 0 13125 0 0 0 63810 87 0 0 25 0 1 0 1785432267 54345728 12919 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25378/statm): 13268 12919 145 145 0 13123 0
[pid=25378] vsize: 53072
Current children cumulated CPU time (s) 638.97
Current children cumulated vsize (Kb) 55196

[startup+650.077 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25378
Raw data (/proc/25374/stat): 25374 (minisat+_script) S 25373 25374 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785432262 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25374/statm): 531 226 485 147 0 384 0
[pid=25374] vsize: 2124
Raw data (/proc/25378/stat): 25378 (minisat+_64-bit) R 25374 25374 8263 0 -1 0 13126 0 0 0 64810 88 0 0 25 0 1 0 1785432267 54345728 12920 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25378/statm): 13268 12920 145 145 0 13123 0
[pid=25378] vsize: 53072
Current children cumulated CPU time (s) 648.98
Current children cumulated vsize (Kb) 55196

[startup+660.077 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25378
Raw data (/proc/25374/stat): 25374 (minisat+_script) S 25373 25374 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785432262 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25374/statm): 531 226 485 147 0 384 0
[pid=25374] vsize: 2124
Raw data (/proc/25378/stat): 25378 (minisat+_64-bit) R 25374 25374 8263 0 -1 0 13127 0 0 0 65810 88 0 0 25 0 1 0 1785432267 54345728 12921 4294967295 134512640 135094434 3221224432 3221223056 134557696 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25378/statm): 13268 12921 145 145 0 13123 0
[pid=25378] vsize: 53072
Current children cumulated CPU time (s) 658.98
Current children cumulated vsize (Kb) 55196

[startup+670.078 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25378
Raw data (/proc/25374/stat): 25374 (minisat+_script) S 25373 25374 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785432262 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25374/statm): 531 226 485 147 0 384 0
[pid=25374] vsize: 2124
Raw data (/proc/25378/stat): 25378 (minisat+_64-bit) R 25374 25374 8263 0 -1 0 13127 0 0 0 66811 88 0 0 25 0 1 0 1785432267 54345728 12921 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25378/statm): 13268 12921 145 145 0 13123 0
[pid=25378] vsize: 53072
Current children cumulated CPU time (s) 668.99
Current children cumulated vsize (Kb) 55196

[startup+680.079 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25378
Raw data (/proc/25374/stat): 25374 (minisat+_script) S 25373 25374 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785432262 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25374/statm): 531 226 485 147 0 384 0
[pid=25374] vsize: 2124
Raw data (/proc/25378/stat): 25378 (minisat+_64-bit) R 25374 25374 8263 0 -1 0 13127 0 0 0 67811 88 0 0 25 0 1 0 1785432267 54345728 12921 4294967295 134512640 135094434 3221224432 3221223088 134557884 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25378/statm): 13268 12921 145 145 0 13123 0
[pid=25378] vsize: 53072
Current children cumulated CPU time (s) 678.99
Current children cumulated vsize (Kb) 55196

[startup+690.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25378
Raw data (/proc/25374/stat): 25374 (minisat+_script) S 25373 25374 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785432262 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25374/statm): 531 226 485 147 0 384 0
[pid=25374] vsize: 2124
Raw data (/proc/25378/stat): 25378 (minisat+_64-bit) R 25374 25374 8263 0 -1 0 13127 0 0 0 68811 88 0 0 25 0 1 0 1785432267 54345728 12921 4294967295 134512640 135094434 3221224432 3221223064 134557638 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25378/statm): 13268 12921 145 145 0 13123 0
[pid=25378] vsize: 53072
Current children cumulated CPU time (s) 688.99
Current children cumulated vsize (Kb) 55196

[startup+700.081 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25378
Raw data (/proc/25374/stat): 25374 (minisat+_script) S 25373 25374 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785432262 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25374/statm): 531 226 485 147 0 384 0
[pid=25374] vsize: 2124
Raw data (/proc/25378/stat): 25378 (minisat+_64-bit) R 25374 25374 8263 0 -1 0 13127 0 0 0 69811 88 0 0 25 0 1 0 1785432267 54345728 12921 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25378/statm): 13268 12921 145 145 0 13123 0
[pid=25378] vsize: 53072
Current children cumulated CPU time (s) 698.99
Current children cumulated vsize (Kb) 55196

[startup+710.082 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25378
Raw data (/proc/25374/stat): 25374 (minisat+_script) S 25373 25374 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785432262 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25374/statm): 531 226 485 147 0 384 0
[pid=25374] vsize: 2124
Raw data (/proc/25378/stat): 25378 (minisat+_64-bit) R 25374 25374 8263 0 -1 0 13127 0 0 0 70811 88 0 0 25 0 1 0 1785432267 54345728 12921 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25378/statm): 13268 12921 145 145 0 13123 0
[pid=25378] vsize: 53072
Current children cumulated CPU time (s) 708.99
Current children cumulated vsize (Kb) 55196

[startup+720.082 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25378
Raw data (/proc/25374/stat): 25374 (minisat+_script) S 25373 25374 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785432262 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25374/statm): 531 226 485 147 0 384 0
[pid=25374] vsize: 2124
Raw data (/proc/25378/stat): 25378 (minisat+_64-bit) R 25374 25374 8263 0 -1 0 13127 0 0 0 71811 88 0 0 25 0 1 0 1785432267 54345728 12921 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25378/statm): 13268 12921 145 145 0 13123 0
[pid=25378] vsize: 53072
Current children cumulated CPU time (s) 718.99
Current children cumulated vsize (Kb) 55196

[startup+730.083 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25378
Raw data (/proc/25374/stat): 25374 (minisat+_script) S 25373 25374 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785432262 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25374/statm): 531 226 485 147 0 384 0
[pid=25374] vsize: 2124
Raw data (/proc/25378/stat): 25378 (minisat+_64-bit) R 25374 25374 8263 0 -1 0 13127 0 0 0 72811 88 0 0 25 0 1 0 1785432267 54345728 12921 4294967295 134512640 135094434 3221224432 3221223056 134557696 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25378/statm): 13268 12921 145 145 0 13123 0
[pid=25378] vsize: 53072
Current children cumulated CPU time (s) 728.99
Current children cumulated vsize (Kb) 55196

[startup+740.084 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25378
Raw data (/proc/25374/stat): 25374 (minisat+_script) S 25373 25374 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785432262 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25374/statm): 531 226 485 147 0 384 0
[pid=25374] vsize: 2124
Raw data (/proc/25378/stat): 25378 (minisat+_64-bit) R 25374 25374 8263 0 -1 0 13127 0 0 0 73812 88 0 0 25 0 1 0 1785432267 54345728 12921 4294967295 134512640 135094434 3221224432 3221223056 134557681 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25378/statm): 13268 12921 145 145 0 13123 0
[pid=25378] vsize: 53072
Current children cumulated CPU time (s) 739
Current children cumulated vsize (Kb) 55196

[startup+750.085 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25378
Raw data (/proc/25374/stat): 25374 (minisat+_script) S 25373 25374 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785432262 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25374/statm): 531 226 485 147 0 384 0
[pid=25374] vsize: 2124
Raw data (/proc/25378/stat): 25378 (minisat+_64-bit) R 25374 25374 8263 0 -1 0 13127 0 0 0 74812 89 0 0 25 0 1 0 1785432267 54345728 12921 4294967295 134512640 135094434 3221224432 3221223024 134557163 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25378/statm): 13268 12921 145 145 0 13123 0
[pid=25378] vsize: 53072
Current children cumulated CPU time (s) 749.01
Current children cumulated vsize (Kb) 55196

[startup+760.086 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25378
Raw data (/proc/25374/stat): 25374 (minisat+_script) S 25373 25374 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785432262 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25374/statm): 531 226 485 147 0 384 0
[pid=25374] vsize: 2124
Raw data (/proc/25378/stat): 25378 (minisat+_64-bit) R 25374 25374 8263 0 -1 0 13127 0 0 0 75812 89 0 0 25 0 1 0 1785432267 54345728 12921 4294967295 134512640 135094434 3221224432 3221223088 134558178 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25378/statm): 13268 12921 145 145 0 13123 0
[pid=25378] vsize: 53072
Current children cumulated CPU time (s) 759.01
Current children cumulated vsize (Kb) 55196

[startup+770.087 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25378
Raw data (/proc/25374/stat): 25374 (minisat+_script) S 25373 25374 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785432262 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25374/statm): 531 226 485 147 0 384 0
[pid=25374] vsize: 2124
Raw data (/proc/25378/stat): 25378 (minisat+_64-bit) R 25374 25374 8263 0 -1 0 13127 0 0 0 76812 89 0 0 25 0 1 0 1785432267 54345728 12921 4294967295 134512640 135094434 3221224432 3221223056 134557619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25378/statm): 13268 12921 145 145 0 13123 0
[pid=25378] vsize: 53072
Current children cumulated CPU time (s) 769.01
Current children cumulated vsize (Kb) 55196

[startup+780.087 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25378
Raw data (/proc/25374/stat): 25374 (minisat+_script) S 25373 25374 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785432262 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25374/statm): 531 226 485 147 0 384 0
[pid=25374] vsize: 2124
Raw data (/proc/25378/stat): 25378 (minisat+_64-bit) R 25374 25374 8263 0 -1 0 13127 0 0 0 77812 89 0 0 25 0 1 0 1785432267 54345728 12921 4294967295 134512640 135094434 3221224432 3221223120 134554709 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25378/statm): 13268 12921 145 145 0 13123 0
[pid=25378] vsize: 53072
Current children cumulated CPU time (s) 779.01
Current children cumulated vsize (Kb) 55196

[startup+790.088 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25378
Raw data (/proc/25374/stat): 25374 (minisat+_script) S 25373 25374 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785432262 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25374/statm): 531 226 485 147 0 384 0
[pid=25374] vsize: 2124
Raw data (/proc/25378/stat): 25378 (minisat+_64-bit) R 25374 25374 8263 0 -1 0 13127 0 0 0 78813 89 0 0 25 0 1 0 1785432267 54345728 12921 4294967295 134512640 135094434 3221224432 3221223044 134563046 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25378/statm): 13268 12921 145 145 0 13123 0
[pid=25378] vsize: 53072
Current children cumulated CPU time (s) 789.02
Current children cumulated vsize (Kb) 55196

[startup+800.089 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25378
Raw data (/proc/25374/stat): 25374 (minisat+_script) S 25373 25374 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785432262 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25374/statm): 531 226 485 147 0 384 0
[pid=25374] vsize: 2124
Raw data (/proc/25378/stat): 25378 (minisat+_64-bit) R 25374 25374 8263 0 -1 0 13127 0 0 0 79813 89 0 0 25 0 1 0 1785432267 54345728 12921 4294967295 134512640 135094434 3221224432 3221223024 134556862 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25378/statm): 13268 12921 145 145 0 13123 0
[pid=25378] vsize: 53072
Current children cumulated CPU time (s) 799.02
Current children cumulated vsize (Kb) 55196

[startup+810.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25378
Raw data (/proc/25374/stat): 25374 (minisat+_script) S 25373 25374 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785432262 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25374/statm): 531 226 485 147 0 384 0
[pid=25374] vsize: 2124
Raw data (/proc/25378/stat): 25378 (minisat+_64-bit) R 25374 25374 8263 0 -1 0 13127 0 0 0 80813 89 0 0 25 0 1 0 1785432267 54345728 12921 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25378/statm): 13268 12921 145 145 0 13123 0
[pid=25378] vsize: 53072
Current children cumulated CPU time (s) 809.02
Current children cumulated vsize (Kb) 55196

[startup+820.092 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25378
Raw data (/proc/25374/stat): 25374 (minisat+_script) S 25373 25374 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785432262 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25374/statm): 531 226 485 147 0 384 0
[pid=25374] vsize: 2124
Raw data (/proc/25378/stat): 25378 (minisat+_64-bit) R 25374 25374 8263 0 -1 0 13127 0 0 0 81813 89 0 0 25 0 1 0 1785432267 54345728 12921 4294967295 134512640 135094434 3221224432 3221223104 134556242 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25378/statm): 13268 12921 145 145 0 13123 0
[pid=25378] vsize: 53072
Current children cumulated CPU time (s) 819.02
Current children cumulated vsize (Kb) 55196

[startup+830.093 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25378
Raw data (/proc/25374/stat): 25374 (minisat+_script) S 25373 25374 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785432262 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25374/statm): 531 226 485 147 0 384 0
[pid=25374] vsize: 2124
Raw data (/proc/25378/stat): 25378 (minisat+_64-bit) R 25374 25374 8263 0 -1 0 13128 0 0 0 82813 89 0 0 25 0 1 0 1785432267 54345728 12922 4294967295 134512640 135094434 3221224432 3221223024 134557230 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25378/statm): 13268 12922 145 145 0 13123 0
[pid=25378] vsize: 53072
Current children cumulated CPU time (s) 829.02
Current children cumulated vsize (Kb) 55196

[startup+840.095 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25378
Raw data (/proc/25374/stat): 25374 (minisat+_script) S 25373 25374 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785432262 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25374/statm): 531 226 485 147 0 384 0
[pid=25374] vsize: 2124
Raw data (/proc/25378/stat): 25378 (minisat+_64-bit) R 25374 25374 8263 0 -1 0 13128 0 0 0 83814 89 0 0 25 0 1 0 1785432267 54345728 12922 4294967295 134512640 135094434 3221224432 3221223024 134556862 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25378/statm): 13268 12922 145 145 0 13123 0
[pid=25378] vsize: 53072
Current children cumulated CPU time (s) 839.03
Current children cumulated vsize (Kb) 55196

[startup+850.095 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25378
Raw data (/proc/25374/stat): 25374 (minisat+_script) S 25373 25374 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785432262 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25374/statm): 531 226 485 147 0 384 0
[pid=25374] vsize: 2124
Raw data (/proc/25378/stat): 25378 (minisat+_64-bit) R 25374 25374 8263 0 -1 0 13128 0 0 0 84814 89 0 0 25 0 1 0 1785432267 54345728 12922 4294967295 134512640 135094434 3221224432 3221223088 134555975 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25378/statm): 13268 12922 145 145 0 13123 0
[pid=25378] vsize: 53072
Current children cumulated CPU time (s) 849.03
Current children cumulated vsize (Kb) 55196

[startup+860.095 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25378
Raw data (/proc/25374/stat): 25374 (minisat+_script) S 25373 25374 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785432262 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25374/statm): 531 226 485 147 0 384 0
[pid=25374] vsize: 2124
Raw data (/proc/25378/stat): 25378 (minisat+_64-bit) R 25374 25374 8263 0 -1 0 13128 0 0 0 85814 89 0 0 25 0 1 0 1785432267 54345728 12922 4294967295 134512640 135094434 3221224432 3221223088 134558162 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25378/statm): 13268 12922 145 145 0 13123 0
[pid=25378] vsize: 53072
Current children cumulated CPU time (s) 859.03
Current children cumulated vsize (Kb) 55196

[startup+870.096 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25378
Raw data (/proc/25374/stat): 25374 (minisat+_script) S 25373 25374 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785432262 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25374/statm): 531 226 485 147 0 384 0
[pid=25374] vsize: 2124
Raw data (/proc/25378/stat): 25378 (minisat+_64-bit) R 25374 25374 8263 0 -1 0 13128 0 0 0 86814 89 0 0 25 0 1 0 1785432267 54345728 12922 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25378/statm): 13268 12922 145 145 0 13123 0
[pid=25378] vsize: 53072
Current children cumulated CPU time (s) 869.03
Current children cumulated vsize (Kb) 55196

[startup+880.097 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25378
Raw data (/proc/25374/stat): 25374 (minisat+_script) S 25373 25374 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785432262 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25374/statm): 531 226 485 147 0 384 0
[pid=25374] vsize: 2124
Raw data (/proc/25378/stat): 25378 (minisat+_64-bit) R 25374 25374 8263 0 -1 0 13129 0 0 0 87814 89 0 0 25 0 1 0 1785432267 54345728 12923 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25378/statm): 13268 12923 145 145 0 13123 0
[pid=25378] vsize: 53072
Current children cumulated CPU time (s) 879.03
Current children cumulated vsize (Kb) 55196

[startup+890.098 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25378
Raw data (/proc/25374/stat): 25374 (minisat+_script) S 25373 25374 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785432262 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25374/statm): 531 226 485 147 0 384 0
[pid=25374] vsize: 2124
Raw data (/proc/25378/stat): 25378 (minisat+_64-bit) R 25374 25374 8263 0 -1 0 13131 0 0 0 88815 89 0 0 25 0 1 0 1785432267 54345728 12925 4294967295 134512640 135094434 3221224432 3221223104 134555568 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25378/statm): 13268 12925 145 145 0 13123 0
[pid=25378] vsize: 53072
Current children cumulated CPU time (s) 889.04
Current children cumulated vsize (Kb) 55196

[startup+900.098 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25378
Raw data (/proc/25374/stat): 25374 (minisat+_script) S 25373 25374 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785432262 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25374/statm): 531 226 485 147 0 384 0
[pid=25374] vsize: 2124
Raw data (/proc/25378/stat): 25378 (minisat+_64-bit) R 25374 25374 8263 0 -1 0 13131 0 0 0 89815 89 0 0 25 0 1 0 1785432267 54345728 12925 4294967295 134512640 135094434 3221224432 3221223024 134557230 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25378/statm): 13268 12925 145 145 0 13123 0
[pid=25378] vsize: 53072
Current children cumulated CPU time (s) 899.04
Current children cumulated vsize (Kb) 55196

[startup+910.099 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25378
Raw data (/proc/25374/stat): 25374 (minisat+_script) S 25373 25374 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785432262 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25374/statm): 531 226 485 147 0 384 0
[pid=25374] vsize: 2124
Raw data (/proc/25378/stat): 25378 (minisat+_64-bit) R 25374 25374 8263 0 -1 0 13131 0 0 0 90815 89 0 0 25 0 1 0 1785432267 54345728 12925 4294967295 134512640 135094434 3221224432 3221223024 134557273 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25378/statm): 13268 12925 145 145 0 13123 0
[pid=25378] vsize: 53072
Current children cumulated CPU time (s) 909.04
Current children cumulated vsize (Kb) 55196

[startup+920.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25378
Raw data (/proc/25374/stat): 25374 (minisat+_script) S 25373 25374 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785432262 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25374/statm): 531 226 485 147 0 384 0
[pid=25374] vsize: 2124
Raw data (/proc/25378/stat): 25378 (minisat+_64-bit) R 25374 25374 8263 0 -1 0 13131 0 0 0 91815 89 0 0 25 0 1 0 1785432267 54345728 12925 4294967295 134512640 135094434 3221224432 3221223120 134554750 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25378/statm): 13268 12925 145 145 0 13123 0
[pid=25378] vsize: 53072
Current children cumulated CPU time (s) 919.04
Current children cumulated vsize (Kb) 55196

[startup+930.101 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25378
Raw data (/proc/25374/stat): 25374 (minisat+_script) S 25373 25374 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785432262 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25374/statm): 531 226 485 147 0 384 0
[pid=25374] vsize: 2124
Raw data (/proc/25378/stat): 25378 (minisat+_64-bit) R 25374 25374 8263 0 -1 0 13131 0 0 0 92815 89 0 0 25 0 1 0 1785432267 54345728 12925 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25378/statm): 13268 12925 145 145 0 13123 0
[pid=25378] vsize: 53072
Current children cumulated CPU time (s) 929.04
Current children cumulated vsize (Kb) 55196

[startup+940.103 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25378
Raw data (/proc/25374/stat): 25374 (minisat+_script) S 25373 25374 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785432262 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25374/statm): 531 226 485 147 0 384 0
[pid=25374] vsize: 2124
Raw data (/proc/25378/stat): 25378 (minisat+_64-bit) R 25374 25374 8263 0 -1 0 13131 0 0 0 93816 89 0 0 25 0 1 0 1785432267 54345728 12925 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25378/statm): 13268 12925 145 145 0 13123 0
[pid=25378] vsize: 53072
Current children cumulated CPU time (s) 939.05
Current children cumulated vsize (Kb) 55196

[startup+950.104 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25378
Raw data (/proc/25374/stat): 25374 (minisat+_script) S 25373 25374 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785432262 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25374/statm): 531 226 485 147 0 384 0
[pid=25374] vsize: 2124
Raw data (/proc/25378/stat): 25378 (minisat+_64-bit) R 25374 25374 8263 0 -1 0 13131 0 0 0 94816 89 0 0 25 0 1 0 1785432267 54345728 12925 4294967295 134512640 135094434 3221224432 3221223120 134554723 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25378/statm): 13268 12925 145 145 0 13123 0
[pid=25378] vsize: 53072
Current children cumulated CPU time (s) 949.05
Current children cumulated vsize (Kb) 55196

[startup+960.105 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25378
Raw data (/proc/25374/stat): 25374 (minisat+_script) S 25373 25374 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785432262 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25374/statm): 531 226 485 147 0 384 0
[pid=25374] vsize: 2124
Raw data (/proc/25378/stat): 25378 (minisat+_64-bit) R 25374 25374 8263 0 -1 0 13131 0 0 0 95816 89 0 0 25 0 1 0 1785432267 54345728 12925 4294967295 134512640 135094434 3221224432 3221223056 134562085 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25378/statm): 13268 12925 145 145 0 13123 0
[pid=25378] vsize: 53072
Current children cumulated CPU time (s) 959.05
Current children cumulated vsize (Kb) 55196

[startup+970.105 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25378
Raw data (/proc/25374/stat): 25374 (minisat+_script) S 25373 25374 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785432262 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25374/statm): 531 226 485 147 0 384 0
[pid=25374] vsize: 2124
Raw data (/proc/25378/stat): 25378 (minisat+_64-bit) R 25374 25374 8263 0 -1 0 13131 0 0 0 96816 89 0 0 25 0 1 0 1785432267 54345728 12925 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25378/statm): 13268 12925 145 145 0 13123 0
[pid=25378] vsize: 53072
Current children cumulated CPU time (s) 969.05
Current children cumulated vsize (Kb) 55196

[startup+980.106 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25378
Raw data (/proc/25374/stat): 25374 (minisat+_script) S 25373 25374 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785432262 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25374/statm): 531 226 485 147 0 384 0
[pid=25374] vsize: 2124
Raw data (/proc/25378/stat): 25378 (minisat+_64-bit) R 25374 25374 8263 0 -1 0 13132 0 0 0 97816 89 0 0 25 0 1 0 1785432267 54345728 12926 4294967295 134512640 135094434 3221224432 3221223024 134556862 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25378/statm): 13268 12926 145 145 0 13123 0
[pid=25378] vsize: 53072
Current children cumulated CPU time (s) 979.05
Current children cumulated vsize (Kb) 55196

[startup+990.106 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25378
Raw data (/proc/25374/stat): 25374 (minisat+_script) S 25373 25374 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785432262 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25374/statm): 531 226 485 147 0 384 0
[pid=25374] vsize: 2124
Raw data (/proc/25378/stat): 25378 (minisat+_64-bit) R 25374 25374 8263 0 -1 0 13132 0 0 0 98817 89 0 0 25 0 1 0 1785432267 54345728 12926 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25378/statm): 13268 12926 145 145 0 13123 0
[pid=25378] vsize: 53072
Current children cumulated CPU time (s) 989.06
Current children cumulated vsize (Kb) 55196

[startup+1000.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25378
Raw data (/proc/25374/stat): 25374 (minisat+_script) S 25373 25374 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785432262 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25374/statm): 531 226 485 147 0 384 0
[pid=25374] vsize: 2124
Raw data (/proc/25378/stat): 25378 (minisat+_64-bit) R 25374 25374 8263 0 -1 0 13132 0 0 0 99817 89 0 0 25 0 1 0 1785432267 54345728 12926 4294967295 134512640 135094434 3221224432 3221223104 134556317 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25378/statm): 13268 12926 145 145 0 13123 0
[pid=25378] vsize: 53072
Current children cumulated CPU time (s) 999.06
Current children cumulated vsize (Kb) 55196

[startup+1010.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25378
Raw data (/proc/25374/stat): 25374 (minisat+_script) S 25373 25374 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785432262 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25374/statm): 531 226 485 147 0 384 0
[pid=25374] vsize: 2124
Raw data (/proc/25378/stat): 25378 (minisat+_64-bit) R 25374 25374 8263 0 -1 0 13132 0 0 0 100817 89 0 0 25 0 1 0 1785432267 54345728 12926 4294967295 134512640 135094434 3221224432 3221223024 134556931 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25378/statm): 13268 12926 145 145 0 13123 0
[pid=25378] vsize: 53072
Current children cumulated CPU time (s) 1009.06
Current children cumulated vsize (Kb) 55196

[startup+1020.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25378
Raw data (/proc/25374/stat): 25374 (minisat+_script) S 25373 25374 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785432262 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25374/statm): 531 226 485 147 0 384 0
[pid=25374] vsize: 2124
Raw data (/proc/25378/stat): 25378 (minisat+_64-bit) R 25374 25374 8263 0 -1 0 13132 0 0 0 101817 89 0 0 25 0 1 0 1785432267 54345728 12926 4294967295 134512640 135094434 3221224432 3221223088 134558426 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25378/statm): 13268 12926 145 145 0 13123 0
[pid=25378] vsize: 53072
Current children cumulated CPU time (s) 1019.06
Current children cumulated vsize (Kb) 55196

[startup+1030.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25378
Raw data (/proc/25374/stat): 25374 (minisat+_script) S 25373 25374 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785432262 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25374/statm): 531 226 485 147 0 384 0
[pid=25374] vsize: 2124
Raw data (/proc/25378/stat): 25378 (minisat+_64-bit) R 25374 25374 8263 0 -1 0 13132 0 0 0 102817 89 0 0 25 0 1 0 1785432267 54345728 12926 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25378/statm): 13268 12926 145 145 0 13123 0
[pid=25378] vsize: 53072
Current children cumulated CPU time (s) 1029.06
Current children cumulated vsize (Kb) 55196

[startup+1040.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25378
Raw data (/proc/25374/stat): 25374 (minisat+_script) S 25373 25374 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785432262 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25374/statm): 531 226 485 147 0 384 0
[pid=25374] vsize: 2124
Raw data (/proc/25378/stat): 25378 (minisat+_64-bit) R 25374 25374 8263 0 -1 0 13132 0 0 0 103817 90 0 0 25 0 1 0 1785432267 54345728 12926 4294967295 134512640 135094434 3221224432 3221223104 134555606 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25378/statm): 13268 12926 145 145 0 13123 0
[pid=25378] vsize: 53072
Current children cumulated CPU time (s) 1039.07
Current children cumulated vsize (Kb) 55196

[startup+1050.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25378
Raw data (/proc/25374/stat): 25374 (minisat+_script) S 25373 25374 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785432262 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25374/statm): 531 226 485 147 0 384 0
[pid=25374] vsize: 2124
Raw data (/proc/25378/stat): 25378 (minisat+_64-bit) R 25374 25374 8263 0 -1 0 13132 0 0 0 104818 90 0 0 25 0 1 0 1785432267 54345728 12926 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25378/statm): 13268 12926 145 145 0 13123 0
[pid=25378] vsize: 53072
Current children cumulated CPU time (s) 1049.08
Current children cumulated vsize (Kb) 55196

[startup+1060.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25378
Raw data (/proc/25374/stat): 25374 (minisat+_script) S 25373 25374 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785432262 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25374/statm): 531 226 485 147 0 384 0
[pid=25374] vsize: 2124
Raw data (/proc/25378/stat): 25378 (minisat+_64-bit) R 25374 25374 8263 0 -1 0 13132 0 0 0 105818 90 0 0 25 0 1 0 1785432267 54345728 12926 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25378/statm): 13268 12926 145 145 0 13123 0
[pid=25378] vsize: 53072
Current children cumulated CPU time (s) 1059.08
Current children cumulated vsize (Kb) 55196

[startup+1070.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25378
Raw data (/proc/25374/stat): 25374 (minisat+_script) S 25373 25374 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785432262 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25374/statm): 531 226 485 147 0 384 0
[pid=25374] vsize: 2124
Raw data (/proc/25378/stat): 25378 (minisat+_64-bit) R 25374 25374 8263 0 -1 0 13132 0 0 0 106817 91 0 0 25 0 1 0 1785432267 54345728 12926 4294967295 134512640 135094434 3221224432 3221223104 134555574 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25378/statm): 13268 12926 145 145 0 13123 0
[pid=25378] vsize: 53072
Current children cumulated CPU time (s) 1069.08
Current children cumulated vsize (Kb) 55196

[startup+1080.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25378
Raw data (/proc/25374/stat): 25374 (minisat+_script) S 25373 25374 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785432262 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25374/statm): 531 226 485 147 0 384 0
[pid=25374] vsize: 2124
Raw data (/proc/25378/stat): 25378 (minisat+_64-bit) R 25374 25374 8263 0 -1 0 13132 0 0 0 107817 91 0 0 25 0 1 0 1785432267 54345728 12926 4294967295 134512640 135094434 3221224432 3221223088 134557840 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25378/statm): 13268 12926 145 145 0 13123 0
[pid=25378] vsize: 53072
Current children cumulated CPU time (s) 1079.08
Current children cumulated vsize (Kb) 55196

[startup+1090.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25378
Raw data (/proc/25374/stat): 25374 (minisat+_script) S 25373 25374 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785432262 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25374/statm): 531 226 485 147 0 384 0
[pid=25374] vsize: 2124
Raw data (/proc/25378/stat): 25378 (minisat+_64-bit) R 25374 25374 8263 0 -1 0 13132 0 0 0 108817 92 0 0 25 0 1 0 1785432267 54345728 12926 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25378/statm): 13268 12926 145 145 0 13123 0
[pid=25378] vsize: 53072
Current children cumulated CPU time (s) 1089.09
Current children cumulated vsize (Kb) 55196

[startup+1100.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25378
Raw data (/proc/25374/stat): 25374 (minisat+_script) S 25373 25374 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785432262 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25374/statm): 531 226 485 147 0 384 0
[pid=25374] vsize: 2124
Raw data (/proc/25378/stat): 25378 (minisat+_64-bit) R 25374 25374 8263 0 -1 0 13147 0 0 0 109816 92 0 0 25 0 1 0 1785432267 54407168 12941 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25378/statm): 13283 12941 145 145 0 13138 0
[pid=25378] vsize: 53132
Current children cumulated CPU time (s) 1099.08
Current children cumulated vsize (Kb) 55256

[startup+1110.12 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25378
Raw data (/proc/25374/stat): 25374 (minisat+_script) S 25373 25374 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785432262 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25374/statm): 531 226 485 147 0 384 0
[pid=25374] vsize: 2124
Raw data (/proc/25378/stat): 25378 (minisat+_64-bit) T 25374 25374 8263 0 -1 0 13458 0 0 0 110809 95 0 0 25 0 1 0 1785432267 55681024 13252 4294967295 134512640 135094434 3221224432 3221222796 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/25378/statm): 13594 13252 145 145 0 13449 0
[pid=25378] vsize: 54376
Current children cumulated CPU time (s) 1109.04
Current children cumulated vsize (Kb) 56500

[startup+1120.12 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25378
Raw data (/proc/25374/stat): 25374 (minisat+_script) S 25373 25374 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785432262 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25374/statm): 531 226 485 147 0 384 0
[pid=25374] vsize: 2124
Raw data (/proc/25378/stat): 25378 (minisat+_64-bit) R 25374 25374 8263 0 -1 0 13719 0 0 0 111803 98 0 0 25 0 1 0 1785432267 56750080 13513 4294967295 134512640 135094434 3221224432 3221223056 134557565 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25378/statm): 13855 13513 145 145 0 13710 0
[pid=25378] vsize: 55420
Current children cumulated CPU time (s) 1119.01
Current children cumulated vsize (Kb) 57544

[startup+1130.12 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25378
Raw data (/proc/25374/stat): 25374 (minisat+_script) S 25373 25374 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785432262 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25374/statm): 531 226 485 147 0 384 0
[pid=25374] vsize: 2124
Raw data (/proc/25378/stat): 25378 (minisat+_64-bit) R 25374 25374 8263 0 -1 0 13992 0 0 0 112797 101 0 0 25 0 1 0 1785432267 57868288 13786 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25378/statm): 14128 13786 145 145 0 13983 0
[pid=25378] vsize: 56512
Current children cumulated CPU time (s) 1128.98
Current children cumulated vsize (Kb) 58636

[startup+1140.12 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25378
Raw data (/proc/25374/stat): 25374 (minisat+_script) S 25373 25374 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785432262 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25374/statm): 531 226 485 147 0 384 0
[pid=25374] vsize: 2124
Raw data (/proc/25378/stat): 25378 (minisat+_64-bit) R 25374 25374 8263 0 -1 0 14307 0 0 0 113791 103 0 0 25 0 1 0 1785432267 59158528 14101 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25378/statm): 14443 14101 145 145 0 14298 0
[pid=25378] vsize: 57772
Current children cumulated CPU time (s) 1138.94
Current children cumulated vsize (Kb) 59896

[startup+1150.12 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25378
Raw data (/proc/25374/stat): 25374 (minisat+_script) S 25373 25374 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785432262 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25374/statm): 531 226 485 147 0 384 0
[pid=25374] vsize: 2124
Raw data (/proc/25378/stat): 25378 (minisat+_64-bit) R 25374 25374 8263 0 -1 0 14606 0 0 0 114786 106 0 0 25 0 1 0 1785432267 60383232 14400 4294967295 134512640 135094434 3221224432 3221223120 134554709 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25378/statm): 14742 14400 145 145 0 14597 0
[pid=25378] vsize: 58968
Current children cumulated CPU time (s) 1148.92
Current children cumulated vsize (Kb) 61092

[startup+1160.12 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25378
Raw data (/proc/25374/stat): 25374 (minisat+_script) S 25373 25374 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785432262 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25374/statm): 531 226 485 147 0 384 0
[pid=25374] vsize: 2124
Raw data (/proc/25378/stat): 25378 (minisat+_64-bit) R 25374 25374 8263 0 -1 0 14895 0 0 0 115780 108 0 0 25 0 1 0 1785432267 61571072 14689 4294967295 134512640 135094434 3221224432 3221223056 134557565 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25378/statm): 15032 14689 145 145 0 14887 0
[pid=25378] vsize: 60128
Current children cumulated CPU time (s) 1158.88
Current children cumulated vsize (Kb) 62252

[startup+1170.12 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25378
Raw data (/proc/25374/stat): 25374 (minisat+_script) S 25373 25374 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785432262 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25374/statm): 531 226 485 147 0 384 0
[pid=25374] vsize: 2124
Raw data (/proc/25378/stat): 25378 (minisat+_64-bit) R 25374 25374 8263 0 -1 0 15069 0 0 0 116778 109 0 0 25 0 1 0 1785432267 62283776 14863 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25378/statm): 15206 14863 145 145 0 15061 0
[pid=25378] vsize: 60824
Current children cumulated CPU time (s) 1168.87
Current children cumulated vsize (Kb) 62948

[startup+1180.12 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25378
Raw data (/proc/25374/stat): 25374 (minisat+_script) S 25373 25374 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785432262 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25374/statm): 531 226 485 147 0 384 0
[pid=25374] vsize: 2124
Raw data (/proc/25378/stat): 25378 (minisat+_64-bit) R 25374 25374 8263 0 -1 0 15222 0 0 0 117776 110 0 0 25 0 1 0 1785432267 62910464 15016 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25378/statm): 15359 15016 145 145 0 15214 0
[pid=25378] vsize: 61436
Current children cumulated CPU time (s) 1178.86
Current children cumulated vsize (Kb) 63560

[startup+1190.12 s]
Raw data (loadavg): 0.99 0.97 0.91 1/57 25378
Raw data (/proc/25374/stat): 25374 (minisat+_script) S 25373 25374 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785432262 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25374/statm): 531 226 485 147 0 384 0
[pid=25374] vsize: 2124
Raw data (/proc/25378/stat): 25378 (minisat+_64-bit) T 25374 25374 8263 0 -1 0 15572 0 0 0 118770 113 0 0 25 0 1 0 1785432267 64344064 15366 4294967295 134512640 135094434 3221224432 3221222796 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/25378/statm): 15709 15366 145 145 0 15564 0
[pid=25378] vsize: 62836
Current children cumulated CPU time (s) 1188.83
Current children cumulated vsize (Kb) 64960

[startup+1200.12 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25378
Raw data (/proc/25374/stat): 25374 (minisat+_script) S 25373 25374 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785432262 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25374/statm): 531 226 485 147 0 384 0
[pid=25374] vsize: 2124
Raw data (/proc/25378/stat): 25378 (minisat+_64-bit) R 25374 25374 8263 0 -1 0 16006 0 0 0 119763 115 0 0 25 0 1 0 1785432267 66121728 15800 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25378/statm): 16143 15800 145 145 0 15998 0
[pid=25378] vsize: 64572
Current children cumulated CPU time (s) 1198.78
Current children cumulated vsize (Kb) 66696

[startup+1210.12 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25378
Raw data (/proc/25374/stat): 25374 (minisat+_script) S 25373 25374 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785432262 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25374/statm): 531 226 485 147 0 384 0
[pid=25374] vsize: 2124
Raw data (/proc/25378/stat): 25378 (minisat+_64-bit) R 25374 25374 8263 0 -1 0 16414 0 0 0 120756 118 0 0 25 0 1 0 1785432267 67784704 16208 4294967295 134512640 135094434 3221224432 3221223024 134557175 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25378/statm): 16549 16208 145 145 0 16404 0
[pid=25378] vsize: 66196
Current children cumulated CPU time (s) 1208.74
Current children cumulated vsize (Kb) 68320



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.12 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25378
Raw data (/proc/25374/stat): 25374 (minisat+_script) S 25373 25374 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785432262 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25374/statm): 531 226 485 147 0 384 0
[pid=25374] vsize: 2124
Raw data (/proc/25378/stat): 25378 (minisat+_64-bit) R 25374 25374 8263 0 -1 0 16414 0 0 0 120756 118 0 0 25 0 1 0 1785432267 67784704 16208 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25378/statm): 16549 16208 145 145 0 16404 0
[pid=25378] vsize: 66196
Current children cumulated CPU time (s) 1208.74
Current children cumulated vsize (Kb) 68320

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

Child status: 10
Real time (s): 1210.16
CPU time (s): 1208.79
CPU user time (s): 1207.57
CPU system time (s): 1.21481
CPU usage (%): 99.8864
Max. virtual memory (cumulated for all children) (Kb): 68320

Verifier Data

ERROR: no interpretation found !