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

Namesubmitted/een/normalized-p0282.opb
MD5SUMdd62132555621025f45a5a6099c90742
Bench Categoryoptimization, medium integers (OPTMEDINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function 258411
Optimality of the best value was proved YES
Number of terms in the objective function 282
Biggest coefficient in the objective function 160646
Number of bits for the biggest coefficient in the objective function 18
Sum of the numbers in the objective function 1302615
Number of bits of the sum of numbers in the objective function 21
Biggest number in a constraint 160646
Number of bits of the biggest number in a constraint 18
Biggest sum of numbers in a constraint 1302615
Number of bits of the biggest sum of numbers21
Best result obtained on this benchmarkOPTIMUM FOUND
Best CPU time to get the best result obtained on this benchmark24.5993
Number of variables282
Total number of constraints221
Number of constraints which are clauses177
Number of constraints which are cardinality constraints (but not clauses)0
Number of constraints which are nor clauses,nor cardinality constraints44
Minimum length of a constraint2
Maximum length of a constraint57

Trace number 2263

Launcher Data

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

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        912344 kB
Buffers:         35380 kB
Cached:          58308 kB
SwapCached:        832 kB
Active:          66684 kB
Inactive:        29624 kB
HighTotal:      131008 kB
HighFree:        69412 kB
LowTotal:       903652 kB
LowFree:        842932 kB
SwapTotal:     2097892 kB
SwapFree:      2096604 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5732 kB
Slab:            20456 kB
Committed_AS:    64140 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-09-18 18:45:06 (client local time) WITH STATUS 10 IN 1209.3 SECONDS
stats: 2618 7 1209.3 10

Solver Data

c Parsing PB file...
c Converting 221 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): .................................................................................................................................................................................sss
c ---[  46]---> BDD-cost:    4
c ---[  45]---> BDD-cost:    8
c ---[  44]---> BDD-cost:   10
c ---[  43]---> BDD-cost:   16
c ---[  42]---> Sorter-cost: 1109     Base: 2 5 3 3
c ---[  41]---> Sorter-cost:  898     Base: 2 5 3 2
c ---[  40]---> Sorter-cost: 1116     Base: 2 5 5
c ---[  38]---> Sorter-cost: 1010     Base: 2 5 5
c ---[  37]---> Sorter-cost:  909     Base: 2 5 5
c ---[  36]---> Sorter-cost:  998     Base: 2 5 3 2
c ---[  35]---> Sorter-cost:  852     Base: 2 5 3 3
c ---[  34]---> Sorter-cost:  842     Base: 5 2 3 3
c ---[  33]---> Sorter-cost:  712     Base: 5 2 3 3
c ---[  32]---> Sorter-cost:  946     Base: 2 5 3 3
c ---[  31]---> Sorter-cost:  841     Base: 2 5 3 3
c ---[  30]---> Sorter-cost:  909     Base: 2 5 5
c ---[  29]---> Sorter-cost:  935     Base: 2 5 3 2
c ---[  28]---> Sorter-cost:  998     Base: 2 5 3
c ---[  27]---> Sorter-cost:  762     Base: 5 2 3 3
c ---[  26]---> Sorter-cost:  908     Base: 2 5 5
c ---[  25]---> Sorter-cost:  907     Base: 2 5 5
c ---[  24]---> Sorter-cost:  713     Base: 5 2 3 3
c ---[  23]---> Sorter-cost:  908     Base: 2 5 5
c ---[  22]---> Sorter-cost:  909     Base: 2 5 5
c ---[  21]---> Sorter-cost: 1008     Base: 2 5 3
c ---[  20]---> Sorter-cost:  898     Base: 2 5 3 3
c ---[  19]---> Sorter-cost:  841     Base: 2 5 3 3
c ---[  18]---> Sorter-cost:  760     Base: 2 5 3 3
c ---[  17]---> Sorter-cost:  713     Base: 5 2 3 3
c ---[  16]---> Sorter-cost: 1071     Base: 2 5 3 3
c ---[  15]---> Sorter-cost:  949     Base: 2 5 3 3
c ---[  14]---> BDD-cost:   26
c ---[  13]---> Sorter-cost: 1108     Base: 2 5 3 3
c ---[  11]---> Sorter-cost: 1081     Base: 2 5 3 3
c ---[  10]---> Sorter-cost:  999     Base: 2 5 3 2
c ---[   9]---> Sorter-cost:  995     Base: 2 5 3 3
c ---[   8]---> Sorter-cost:  982     Base: 2 5 3 2
c ---[   7]---> Sorter-cost:  996     Base: 2 5 3 3
c ---[   5]---> BDD-cost:   56
c ---[   4]---> BDD-cost:   56
c ---[   3]---> BDD-cost:   56
c ---[   2]---> BDD-cost:   12
c ---[   1]---> Sorter-cost:  717     Base: 2 5 3
c ---[   0]---> Sorter-cost:  655     Base: 2 5 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   70255   164891 |   23418       0        0     nan |  0.000 % |
c |       100 |   69917   164139 |   25759      93      577     6.2 |  0.539 % |
c ==============================================================================
c Found solution: 628263
c ---[   0]---> Sorter-cost:77312     Base: 3 3 3 3 2 3 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       154 |  289324   676780 |   96441     145     1012     7.0 |  0.539 % |
c |       254 |  289196   676496 |  106085     241     7343    30.5 |  0.195 % |
c |       404 |  289140   676372 |  116693     389     8935    23.0 |  0.210 % |
c |       629 |  289026   676117 |  128362     613    10286    16.8 |  0.239 % |
c |       967 |  288994   676045 |  141199     949    19599    20.7 |  0.248 % |
c |      1473 |  288994   676045 |  155319    1455    26362    18.1 |  0.248 % |
c |      2232 |  288994   676045 |  170851    2214    33093    14.9 |  0.248 % |
c |      3371 |  288854   675733 |  187936    3345   114434    34.2 |  0.285 % |
c |      5080 |  288563   675077 |  206729    5053   138020    27.3 |  0.356 % |
c ==============================================================================
c Found solution: 566001
c ---[   0]---> Sorter-cost:   10     Base: 3 3 3 3 2 3 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      5423 |  288839   675889 |   96279    5395   169300    31.4 |  0.356 % |
c |      5523 |  288839   675889 |  105906    5495   170399    31.0 |  0.359 % |
c |      5674 |  288839   675889 |  116497    5646   171301    30.3 |  0.359 % |
c |      5899 |  288743   675673 |  128147    5869   175852    30.0 |  0.384 % |
c |      6236 |  288743   675673 |  140962    6206   177830    28.7 |  0.384 % |
c |      6742 |  288688   675549 |  155058    6711   181373    27.0 |  0.399 % |
c |      7501 |  288688   675549 |  170564    7470   186837    25.0 |  0.399 % |
c |      8640 |  288688   675549 |  187620    8609   216152    25.1 |  0.399 % |
c ==============================================================================
c Found solution: 484674
c ---[   0]---> Sorter-cost:   13     Base: 3 3 3 3 2 3 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     10092 |  288996   676700 |   96332   10053   237028    23.6 |  0.399 % |
c |     10193 |  288996   676700 |  105965   10154   237467    23.4 |  0.473 % |
c |     10343 |  288996   676700 |  116561   10304   238188    23.1 |  0.473 % |
c |     10568 |  288996   676700 |  128217   10529   239895    22.8 |  0.473 % |
c |     10905 |  288996   676700 |  141039   10866   248577    22.9 |  0.473 % |
c |     11412 |  288996   676700 |  155143   11373   259298    22.8 |  0.473 % |
c |     12171 |  288851   676374 |  170658   12127   270935    22.3 |  0.512 % |
c |     13310 |  288847   676365 |  187723   13265   320224    24.1 |  0.513 % |
c ==============================================================================
c Found solution: 445249
c ---[   0]---> Sorter-cost:   11     Base: 3 3 3 3 2 3 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     14034 |  289183   677345 |   96394   13931   345351    24.8 |  0.513 % |
c |     14134 |  289183   677345 |  106033   14031   345862    24.6 |  0.575 % |
c |     14285 |  289162   677300 |  116636   14181   351345    24.8 |  0.582 % |
c |     14510 |  289162   677300 |  128300   14406   356420    24.7 |  0.582 % |
c |     14847 |  289100   677161 |  141130   14740   360896    24.5 |  0.601 % |
c |     15353 |  288611   676053 |  155243   15228   370340    24.3 |  0.741 % |
c |     16112 |  288611   676053 |  170767   15987   409928    25.6 |  0.741 % |
c |     17255 |  288391   675554 |  187844   17122   447923    26.2 |  0.803 % |
c |     18963 |  288078   674859 |  206629   18820   529203    28.1 |  0.890 % |
c |     21525 |  288034   674761 |  227292   21380   570591    26.7 |  0.902 % |
c |     25371 |  288034   674761 |  250021   25226   640379    25.4 |  0.902 % |
c ==============================================================================
c Found solution: 444335
c ---[   0]---> Sorter-cost:   13     Base: 3 3 3 3 2 3 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     26271 |  288407   675860 |   96135   26126   763005    29.2 |  0.902 % |
c |     26371 |  288407   675860 |  105748   26226   763504    29.1 |  0.901 % |
c |     26521 |  288407   675860 |  116323   26375   770197    29.2 |  0.907 % |
c |     26746 |  288386   675814 |  127955   26600   778032    29.2 |  0.907 % |
c |     27085 |  288363   675762 |  140751   26938   780776    29.0 |  0.915 % |
c |     27591 |  288316   675654 |  154826   27443   802878    29.3 |  0.930 % |
c |     28350 |  288316   675654 |  170309   28202   825991    29.3 |  0.930 % |
c |     29489 |  288316   675654 |  187339   29341   845911    28.8 |  0.930 % |
c ==============================================================================
c Found solution: 436563
c ---[   0]---> Sorter-cost:    7     Base: 3 3 3 3 2 3 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     30056 |  288324   675691 |   96108   29908   872577    29.2 |  0.930 % |
c |     30156 |  288275   675585 |  105718   30004   876794    29.2 |  0.945 % |
c |     30306 |  288275   675585 |  116290   30154   888553    29.5 |  0.945 % |
c |     30532 |  288203   675424 |  127919   30379   901516    29.7 |  0.964 % |
c |     30870 |  288163   675336 |  140711   30716   915078    29.8 |  0.975 % |
c |     31376 |  288163   675336 |  154782   31222   924876    29.6 |  0.975 % |
c |     32137 |  287950   674856 |  170261   31949   937478    29.3 |  1.036 % |
c |     33276 |  287871   674673 |  187287   33082   954844    28.9 |  1.063 % |
c |     34984 |  287756   674415 |  206016   34788   981681    28.2 |  1.093 % |
c |     37548 |  287736   674370 |  226617   37351  1248671    33.4 |  1.098 % |
c |     41392 |  287637   674148 |  249279   41193  1343488    32.6 |  1.123 % |
c ==============================================================================
c Found solution: 436402
c ---[   0]---> Sorter-cost:    7     Base: 3 3 3 3 2 3 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     43764 |  287605   674082 |   95868   43564  1447376    33.2 |  1.123 % |
c |     43867 |  287605   674082 |  105454   43667  1448737    33.2 |  1.133 % |
c |     44018 |  287605   674082 |  116000   43818  1449657    33.1 |  1.133 % |
c |     44244 |  287605   674082 |  127600   44044  1460157    33.2 |  1.133 % |
c |     44581 |  287560   673982 |  140360   44380  1479136    33.3 |  1.145 % |
c |     45088 |  287560   673982 |  154396   44887  1496111    33.3 |  1.145 % |
c |     45848 |  287223   673220 |  169836   45621  1520809    33.3 |  1.238 % |
c |     46988 |  287163   673084 |  186819   46758  1538696    32.9 |  1.256 % |
c |     48697 |  287039   672805 |  205501   48465  1592787    32.9 |  1.289 % |
c |     51261 |  286990   672696 |  226051   51028  1898314    37.2 |  1.303 % |
c |     55105 |  286990   672696 |  248656   54872  2298636    41.9 |  1.303 % |
c |     60871 |  286990   672696 |  273522   60638  2869733    47.3 |  1.303 % |
c ==============================================================================
c Found solution: 435910
c ---[   0]---> Sorter-cost:   12     Base: 3 3 3 3 2 3 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     63492 |  286856   672401 |   95618   63256  3040113    48.1 |  1.303 % |
c |     63592 |  286856   672401 |  105179   63356  3040956    48.0 |  1.340 % |
c |     63743 |  286856   672401 |  115697   63507  3046265    48.0 |  1.340 % |
c |     63968 |  286856   672401 |  127267   63732  3058484    48.0 |  1.340 % |
c |     64306 |  286815   672308 |  139994   64069  3075581    48.0 |  1.350 % |
c ==============================================================================
c Found solution: 435909
c ---[   0]---> Sorter-cost:   13     Base: 3 3 3 3 2 3 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     64468 |  286827   672341 |   95609   64231  3084273    48.0 |  1.350 % |
c |     64568 |  286827   672341 |  105169   64331  3085548    48.0 |  1.351 % |
c |     64718 |  286452   671488 |  115686   64436  3086303    47.9 |  1.456 % |
c |     64943 |  286452   671488 |  127255   64661  3088405    47.8 |  1.456 % |
c |     65280 |  286452   671488 |  139981   64998  3091356    47.6 |  1.456 % |
c |     65786 |  286440   671461 |  153979   65501  3105468    47.4 |  1.459 % |
c ==============================================================================
c Found solution: 433675
c ---[   0]---> Sorter-cost:    9     Base: 3 3 3 3 2 3 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     66530 |  286450   671528 |   95483   66245  3144016    47.5 |  1.459 % |
c |     66630 |  286450   671528 |  105031   66345  3144764    47.4 |  1.460 % |
c |     66780 |  286450   671528 |  115534   66495  3147292    47.3 |  1.460 % |
c |     67005 |  286450   671528 |  127087   66720  3168130    47.5 |  1.460 % |
c |     67342 |  286396   671405 |  139796   67054  3206859    47.8 |  1.474 % |
c |     67848 |  286396   671405 |  153776   67560  3222948    47.7 |  1.474 % |
c |     68607 |  286396   671405 |  169153   68319  3233174    47.3 |  1.474 % |
c |     69746 |  286396   671405 |  186069   69458  3332574    48.0 |  1.474 % |
c |     71454 |  286372   671351 |  204676   71165  3432460    48.2 |  1.482 % |
c ==============================================================================
c Found solution: 429382
c ---[   0]---> Sorter-cost:   10     Base: 3 3 3 3 2 3 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     72160 |  286384   671380 |   95461   71871  3458870    48.1 |  1.482 % |
c |     72260 |  286384   671380 |  105007   71971  3461748    48.1 |  1.483 % |
c |     72411 |  286340   671278 |  115507   72120  3463828    48.0 |  1.497 % |
c |     72636 |  286340   671278 |  127058   72345  3469925    48.0 |  1.497 % |
c |     72973 |  286340   671278 |  139764   72682  3483184    47.9 |  1.497 % |
c |     73479 |  286340   671278 |  153740   73188  3502426    47.9 |  1.497 % |
c |     74238 |  286340   671278 |  169114   73947  3510471    47.5 |  1.497 % |
c |     75377 |  286340   671278 |  186026   75086  3755391    50.0 |  1.497 % |
c |     77086 |  286143   670826 |  204629   76775  3812101    49.7 |  1.558 % |
c |     79648 |  286064   670648 |  225092   79322  3887526    49.0 |  1.579 % |
c ==============================================================================
c Found solution: 389989
c ---[   0]---> Sorter-cost:    9     Base: 3 3 3 3 2 3 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     82574 |  286093   670721 |   95364   82248  4017147    48.8 |  1.579 % |
c |     82675 |  286093   670721 |  104900   82349  4018604    48.8 |  1.580 % |
c |     82827 |  285926   670342 |  115390   82480  4019751    48.7 |  1.627 % |
c |     83052 |  285926   670342 |  126929   82705  4020916    48.6 |  1.627 % |
c |     83389 |  285926   670342 |  139622   83042  4067516    49.0 |  1.627 % |
c |     83895 |  285926   670342 |  153584   83548  4081876    48.9 |  1.627 % |
c |     84654 |  285906   670297 |  168943   84306  4136077    49.1 |  1.633 % |
c |     85794 |  285906   670297 |  185837   85446  4266042    49.9 |  1.633 % |
c |     87505 |  285861   670194 |  204421   87135  4307281    49.4 |  1.647 % |
c ==============================================================================
c Found solution: 380037
c ---[   0]---> Sorter-cost:   12     Base: 3 3 3 3 2 3 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     88132 |  285880   670357 |   95293   87762  4424781    50.4 |  1.647 % |
c |     88233 |  285880   670357 |  104822   87863  4425663    50.4 |  1.647 % |
c |     88383 |  285880   670357 |  115304   88013  4426722    50.3 |  1.647 % |
c |     88608 |  285880   670357 |  126834   88238  4434089    50.3 |  1.647 % |
c |     88947 |  285880   670357 |  139518   88577  4448639    50.2 |  1.647 % |
c |     89453 |  285880   670357 |  153470   89083  4552809    51.1 |  1.647 % |
c |     90212 |  285880   670357 |  168817   89842  4625864    51.5 |  1.647 % |
c |     91351 |  285880   670357 |  185699   90981  4649981    51.1 |  1.647 % |
c |     93061 |  285809   670195 |  204269   92673  4689988    50.6 |  1.668 % |
c |     95623 |  285809   670195 |  224695   95235  4809300    50.5 |  1.668 % |
c |     99467 |  285809   670195 |  247165   99079  5424523    54.7 |  1.668 % |
c ==============================================================================
c Found solution: 376742
c ---[   0]---> Sorter-cost:   15     Base: 3 3 3 3 2 3 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    102944 |  285767   670104 |   95255  102555  5563757    54.3 |  1.668 % |
c |    103044 |  285767   670104 |  104780   31949  1034771    32.4 |  1.684 % |
c ==============================================================================
c Found solution: 370710
c ---[   0]---> Sorter-cost:    9     Base: 3 3 3 3 2 3 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    103120 |  285749   670068 |   95249   32023  1036273    32.4 |  1.684 % |
c |    103221 |  285749   670068 |  104773   32124  1038051    32.3 |  1.693 % |
c |    103371 |  285749   670068 |  115251   32274  1038728    32.2 |  1.693 % |
c |    103596 |  285749   670068 |  126776   32499  1055537    32.5 |  1.693 % |
c |    103933 |  285749   670068 |  139454   32836  1067491    32.5 |  1.693 % |
c |    104439 |  285749   670068 |  153399   33342  1100316    33.0 |  1.693 % |
c |    105198 |  285749   670068 |  168739   34101  1126293    33.0 |  1.693 % |
c |    106337 |  285698   669949 |  185613   35239  1187793    33.7 |  1.708 % |
c ==============================================================================
c Found solution: 369981
c ---[   0]---> Sorter-cost:    6     Base: 3 3 3 3 2 3 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    107949 |  285682   669915 |   95227   36850  1504973    40.8 |  1.708 % |
c |    108052 |  285682   669915 |  104749   36953  1506173    40.8 |  1.717 % |
c |    108202 |  285682   669915 |  115224   37103  1507610    40.6 |  1.717 % |
c |    108428 |  285682   669915 |  126747   37329  1515140    40.6 |  1.717 % |
c |    108765 |  285682   669915 |  139421   37666  1529271    40.6 |  1.717 % |
c |    109271 |  285682   669915 |  153364   38172  1556483    40.8 |  1.717 % |
c |    110032 |  285682   669915 |  168700   38933  1603181    41.2 |  1.717 % |
c ==============================================================================
c Found solution: 369979
c ---[   0]---> Sorter-cost:   11     Base: 3 3 3 3 2 3 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    110278 |  285690   669939 |   95230   39179  1612569    41.2 |  1.717 % |
c |    110379 |  285633   669810 |  104753   39279  1615846    41.1 |  1.732 % |
c |    110529 |  285633   669810 |  115228   39429  1617918    41.0 |  1.732 % |
c |    110755 |  285506   669522 |  126751   39644  1619251    40.8 |  1.767 % |
c |    111094 |  285506   669522 |  139426   39983  1642570    41.1 |  1.767 % |
c |    111600 |  285506   669522 |  153368   40489  1711038    42.3 |  1.767 % |
c |    112359 |  285506   669522 |  168705   41248  1757059    42.6 |  1.767 % |
c ==============================================================================
c Found solution: 366578
c ---[   0]---> Sorter-cost:   12     Base: 3 3 3 3 2 3 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    113082 |  285514   669547 |   95171   41971  1829234    43.6 |  1.767 % |
c |    113183 |  285468   669444 |  104688   42069  1831438    43.5 |  1.780 % |
c |    113335 |  285468   669444 |  115156   42221  1834165    43.4 |  1.780 % |
c |    113561 |  285468   669444 |  126672   42447  1845787    43.5 |  1.780 % |
c |    113899 |  285449   669402 |  139339   42784  1869641    43.7 |  1.785 % |
c |    114406 |  285430   669360 |  153273   43290  1904924    44.0 |  1.790 % |
c |    115165 |  285430   669360 |  168601   44049  1959172    44.5 |  1.790 % |
c |    116304 |  285430   669360 |  185461   45188  2046279    45.3 |  1.790 % |
c |    118014 |  285430   669360 |  204007   46898  2170140    46.3 |  1.790 % |
c |    120577 |  285430   669360 |  224408   49461  2316819    46.8 |  1.790 % |
c |    124422 |  285317   669105 |  246849   53304  2510434    47.1 |  1.818 % |
c |    130188 |  285317   669105 |  271533   59070  2821596    47.8 |  1.818 % |
c ==============================================================================
c Found solution: 366570
c ---[   0]---> Sorter-cost:   12     Base: 3 3 3 3 2 3 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    131845 |  285328   669136 |   95109   60727  2949783    48.6 |  1.818 % |
c |    131946 |  285328   669136 |  104619   60828  2953165    48.5 |  1.819 % |
c |    132096 |  285328   669136 |  115081   60978  2961053    48.6 |  1.819 % |
c |    132321 |  285328   669136 |  126590   61203  2971592    48.6 |  1.819 % |
c |    132658 |  285328   669136 |  139249   61540  2979009    48.4 |  1.819 % |
c |    133164 |  285328   669136 |  153173   62046  3021918    48.7 |  1.819 % |
c |    133924 |  285298   669070 |  168491   62805  3109161    49.5 |  1.827 % |
c |    135063 |  285298   669070 |  185340   63944  3194490    50.0 |  1.827 % |
c |    136771 |  285204   668861 |  203874   65650  3399419    51.8 |  1.853 % |
c ==============================================================================
c Found solution: 365125
c ---[   0]---> Sorter-cost:   11     Base: 3 3 3 3 2 3 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    137522 |  285218   668892 |   95072   66401  3415093    51.4 |  1.853 % |
c |    137623 |  285218   668892 |  104579   66502  3415717    51.4 |  1.854 % |
c |    137773 |  285218   668892 |  115037   66652  3416706    51.3 |  1.854 % |
c |    137999 |  285218   668892 |  126540   66878  3418322    51.1 |  1.854 % |
c |    138336 |  285218   668892 |  139194   67215  3440255    51.2 |  1.854 % |
c |    138842 |  285218   668892 |  153114   67721  3480470    51.4 |  1.854 % |
c |    139602 |  285218   668892 |  168425   68481  3545219    51.8 |  1.854 % |
c ==============================================================================
c Found solution: 360746
c ---[   0]---> Sorter-cost:    6     Base: 3 3 3 3 2 3 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    139957 |  285208   668877 |   95069   68835  3617548    52.6 |  1.854 % |
c |    140057 |  285208   668877 |  104575   68935  3621012    52.5 |  1.861 % |
c |    140207 |  285208   668877 |  115033   69085  3622746    52.4 |  1.861 % |
c |    140432 |  285208   668877 |  126536   69310  3635414    52.5 |  1.861 % |
c |    140769 |  285208   668877 |  139190   69647  3648677    52.4 |  1.861 % |
c |    141275 |  285208   668877 |  153109   70153  3672456    52.3 |  1.861 % |
c |    142035 |  285208   668877 |  168420   70913  3706877    52.3 |  1.861 % |
c |    143174 |  285208   668877 |  185262   72052  3785458    52.5 |  1.861 % |

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/13194/stat): 13194 (minisat+_script) R 13193 13194 2660 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1843395303 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 1 0 0
Raw data (/proc/13194/statm): 174 3 169 147 0 27 0
[pid=13194] 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=13195
New process pid=13196
New process pid=13197
execve syscall for /bin/sed executable
One traced child (pid=13196) 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=13197) exited with status: 0
One traced child (pid=13195) exited with status: 0
New process pid=13198
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc20/normalized-p0282.opb

[startup+10.004 s]
Raw data (loadavg): 0.94 0.98 0.97 2/57 13198
Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13194/statm): 531 226 485 147 0 384 0
[pid=13194] vsize: 2124
Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 8526 0 0 0 928 35 0 0 25 0 1 0 1843395308 37228544 8171 4294967295 134512640 135094434 3221224448 3221223084 134557560 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13198/statm): 9089 8171 145 145 0 8944 0
[pid=13198] vsize: 36356
Current children cumulated CPU time (s) 9.63
Current children cumulated vsize (Kb) 38480

[startup+20.0048 s]
Raw data (loadavg): 0.95 0.98 0.97 2/57 13198
Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13194/statm): 531 226 485 147 0 384 0
[pid=13194] vsize: 2124
Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 8710 0 0 0 1925 37 0 0 25 0 1 0 1843395308 37838848 8355 4294967295 134512640 135094434 3221224448 3221223072 134557596 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13198/statm): 9238 8355 145 145 0 9093 0
[pid=13198] vsize: 36952
Current children cumulated CPU time (s) 19.62
Current children cumulated vsize (Kb) 39076

[startup+30.0055 s]
Raw data (loadavg): 0.95 0.98 0.97 2/57 13198
Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13194/statm): 531 226 485 147 0 384 0
[pid=13194] vsize: 2124
Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 8897 0 0 0 2923 37 0 0 25 0 1 0 1843395308 38522880 8542 4294967295 134512640 135094434 3221224448 3221223100 134558255 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13198/statm): 9405 8542 145 145 0 9260 0
[pid=13198] vsize: 37620
Current children cumulated CPU time (s) 29.6
Current children cumulated vsize (Kb) 39744

[startup+40.0062 s]
Raw data (loadavg): 0.96 0.98 0.97 2/57 13198
Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13194/statm): 531 226 485 147 0 384 0
[pid=13194] vsize: 2124
Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 8977 0 0 0 3923 38 0 0 25 0 1 0 1843395308 38858752 8622 4294967295 134512640 135094434 3221224448 3221223072 134557702 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13198/statm): 9487 8622 145 145 0 9342 0
[pid=13198] vsize: 37948
Current children cumulated CPU time (s) 39.61
Current children cumulated vsize (Kb) 40072

[startup+50.0079 s]
Raw data (loadavg): 0.97 0.98 0.97 2/57 13198
Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13194/statm): 531 226 485 147 0 384 0
[pid=13194] vsize: 2124
Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 9050 0 0 0 4922 38 0 0 25 0 1 0 1843395308 39145472 8695 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13198/statm): 9557 8695 145 145 0 9412 0
[pid=13198] vsize: 38228
Current children cumulated CPU time (s) 49.6
Current children cumulated vsize (Kb) 40352

[startup+60.0086 s]
Raw data (loadavg): 0.97 0.98 0.97 2/57 13198
Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13194/statm): 531 226 485 147 0 384 0
[pid=13194] vsize: 2124
Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 9131 0 0 0 5922 38 0 0 25 0 1 0 1843395308 39485440 8776 4294967295 134512640 135094434 3221224448 3221221648 134600232 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13198/statm): 9640 8776 145 145 0 9495 0
[pid=13198] vsize: 38560
Current children cumulated CPU time (s) 59.6
Current children cumulated vsize (Kb) 40684

[startup+70.0094 s]
Raw data (loadavg): 0.98 0.98 0.97 2/57 13198
Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13194/statm): 531 226 485 147 0 384 0
[pid=13194] vsize: 2124
Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 9146 0 0 0 6921 38 0 0 25 0 1 0 1843395308 39522304 8791 4294967295 134512640 135094434 3221224448 3221223140 134558984 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13198/statm): 9649 8791 145 145 0 9504 0
[pid=13198] vsize: 38596
Current children cumulated CPU time (s) 69.59
Current children cumulated vsize (Kb) 40720

[startup+80.0111 s]
Raw data (loadavg): 0.98 0.98 0.97 2/57 13198
Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13194/statm): 531 226 485 147 0 384 0
[pid=13194] vsize: 2124
Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 9219 0 0 0 7920 39 0 0 25 0 1 0 1843395308 39870464 8864 4294967295 134512640 135094434 3221224448 3221223120 134556415 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13198/statm): 9734 8864 145 145 0 9589 0
[pid=13198] vsize: 38936
Current children cumulated CPU time (s) 79.59
Current children cumulated vsize (Kb) 41060

[startup+90.0118 s]
Raw data (loadavg): 0.98 0.98 0.97 2/57 13198
Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13194/statm): 531 226 485 147 0 384 0
[pid=13194] vsize: 2124
Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 9283 0 0 0 8919 39 0 0 25 0 1 0 1843395308 40128512 8928 4294967295 134512640 135094434 3221224448 3221223104 134558178 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13198/statm): 9797 8928 145 145 0 9652 0
[pid=13198] vsize: 39188
Current children cumulated CPU time (s) 89.58
Current children cumulated vsize (Kb) 41312

[startup+100.013 s]
Raw data (loadavg): 0.98 0.98 0.97 2/57 13198
Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13194/statm): 531 226 485 147 0 384 0
[pid=13194] vsize: 2124
Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 9398 0 0 0 9917 40 0 0 25 0 1 0 1843395308 40583168 9043 4294967295 134512640 135094434 3221224448 3221223100 134558255 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13198/statm): 9908 9043 145 145 0 9763 0
[pid=13198] vsize: 39632
Current children cumulated CPU time (s) 99.57
Current children cumulated vsize (Kb) 41756

[startup+110.013 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 13198
Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13194/statm): 531 226 485 147 0 384 0
[pid=13194] vsize: 2124
Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 9646 0 0 0 10914 42 0 0 25 0 1 0 1843395308 41582592 9291 4294967295 134512640 135094434 3221224448 3221221040 134676280 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13198/statm): 10152 9291 145 145 0 10007 0
[pid=13198] vsize: 40608
Current children cumulated CPU time (s) 109.56
Current children cumulated vsize (Kb) 42732

[startup+120.014 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 13198
Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13194/statm): 531 226 485 147 0 384 0
[pid=13194] vsize: 2124
Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 9684 0 0 0 11913 42 0 0 25 0 1 0 1843395308 41709568 9329 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13198/statm): 10183 9329 145 145 0 10038 0
[pid=13198] vsize: 40732
Current children cumulated CPU time (s) 119.55
Current children cumulated vsize (Kb) 42856

[startup+130.015 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 13198
Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13194/statm): 531 226 485 147 0 384 0
[pid=13194] vsize: 2124
Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 9747 0 0 0 12912 43 0 0 25 0 1 0 1843395308 41959424 9392 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13198/statm): 10244 9392 145 145 0 10099 0
[pid=13198] vsize: 40976
Current children cumulated CPU time (s) 129.55
Current children cumulated vsize (Kb) 43100

[startup+140.015 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 13198
Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13194/statm): 531 226 485 147 0 384 0
[pid=13194] vsize: 2124
Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 9802 0 0 0 13911 43 0 0 25 0 1 0 1843395308 42172416 9447 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13198/statm): 10296 9447 145 145 0 10151 0
[pid=13198] vsize: 41184
Current children cumulated CPU time (s) 139.54
Current children cumulated vsize (Kb) 43308

[startup+150.017 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 13198
Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13194/statm): 531 226 485 147 0 384 0
[pid=13194] vsize: 2124
Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 9845 0 0 0 14911 43 0 0 25 0 1 0 1843395308 42344448 9490 4294967295 134512640 135094434 3221224448 3221223136 134554731 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13198/statm): 10338 9490 145 145 0 10193 0
[pid=13198] vsize: 41352
Current children cumulated CPU time (s) 149.54
Current children cumulated vsize (Kb) 43476

[startup+160.018 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 13198
Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13194/statm): 531 226 485 147 0 384 0
[pid=13194] vsize: 2124
Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 9942 0 0 0 15909 44 0 0 25 0 1 0 1843395308 42860544 9587 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13198/statm): 10464 9587 145 145 0 10319 0
[pid=13198] vsize: 41856
Current children cumulated CPU time (s) 159.53
Current children cumulated vsize (Kb) 43980

[startup+170.019 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 13198
Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13194/statm): 531 226 485 147 0 384 0
[pid=13194] vsize: 2124
Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 10087 0 0 0 16907 45 0 0 25 0 1 0 1843395308 43450368 9732 4294967295 134512640 135094434 3221224448 3221223104 134558426 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13198/statm): 10608 9732 145 145 0 10463 0
[pid=13198] vsize: 42432
Current children cumulated CPU time (s) 169.52
Current children cumulated vsize (Kb) 44556

[startup+180.019 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 13198
Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13194/statm): 531 226 485 147 0 384 0
[pid=13194] vsize: 2124
Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 10199 0 0 0 17905 46 0 0 25 0 1 0 1843395308 43905024 9844 4294967295 134512640 135094434 3221224448 3221223104 134558298 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13198/statm): 10719 9844 145 145 0 10574 0
[pid=13198] vsize: 42876
Current children cumulated CPU time (s) 179.51
Current children cumulated vsize (Kb) 45000

[startup+190.02 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 13198
Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13194/statm): 531 226 485 147 0 384 0
[pid=13194] vsize: 2124
Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 10305 0 0 0 18903 46 0 0 25 0 1 0 1843395308 44322816 9950 4294967295 134512640 135094434 3221224448 3221223104 134557849 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13198/statm): 10821 9950 145 145 0 10676 0
[pid=13198] vsize: 43284
Current children cumulated CPU time (s) 189.49
Current children cumulated vsize (Kb) 45408

[startup+200.021 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 13198
Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13194/statm): 531 226 485 147 0 384 0
[pid=13194] vsize: 2124
Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 10356 0 0 0 19903 47 0 0 25 0 1 0 1843395308 44531712 10001 4294967295 134512640 135094434 3221224448 3221223104 134557872 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13198/statm): 10872 10001 145 145 0 10727 0
[pid=13198] vsize: 43488
Current children cumulated CPU time (s) 199.5
Current children cumulated vsize (Kb) 45612

[startup+210.021 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 13198
Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13194/statm): 531 226 485 147 0 384 0
[pid=13194] vsize: 2124
Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 10459 0 0 0 20901 47 0 0 25 0 1 0 1843395308 44945408 10104 4294967295 134512640 135094434 3221224448 3221221004 134677228 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13198/statm): 10973 10104 145 145 0 10828 0
[pid=13198] vsize: 43892
Current children cumulated CPU time (s) 209.48
Current children cumulated vsize (Kb) 46016

[startup+220.022 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 13198
Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13194/statm): 531 226 485 147 0 384 0
[pid=13194] vsize: 2124
Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 10479 0 0 0 21901 47 0 0 25 0 1 0 1843395308 45015040 10124 4294967295 134512640 135094434 3221224448 3221223040 134551702 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13198/statm): 10990 10124 145 145 0 10845 0
[pid=13198] vsize: 43960
Current children cumulated CPU time (s) 219.48
Current children cumulated vsize (Kb) 46084

[startup+230.023 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 13198
Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13194/statm): 531 226 485 147 0 384 0
[pid=13194] vsize: 2124
Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 10544 0 0 0 22901 48 0 0 25 0 1 0 1843395308 45273088 10189 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13198/statm): 11053 10189 145 145 0 10908 0
[pid=13198] vsize: 44212
Current children cumulated CPU time (s) 229.49
Current children cumulated vsize (Kb) 46336

[startup+240.024 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 13198
Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13194/statm): 531 226 485 147 0 384 0
[pid=13194] vsize: 2124
Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 10616 0 0 0 23900 48 0 0 25 0 1 0 1843395308 45613056 10261 4294967295 134512640 135094434 3221224448 3221223104 134557879 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13198/statm): 11136 10261 145 145 0 10991 0
[pid=13198] vsize: 44544
Current children cumulated CPU time (s) 239.48
Current children cumulated vsize (Kb) 46668

[startup+250.025 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 13198
Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13194/statm): 531 226 485 147 0 384 0
[pid=13194] vsize: 2124
Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 10721 0 0 0 24899 49 0 0 25 0 1 0 1843395308 46018560 10366 4294967295 134512640 135094434 3221224448 3221223040 134556812 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13198/statm): 11235 10366 145 145 0 11090 0
[pid=13198] vsize: 44940
Current children cumulated CPU time (s) 249.48
Current children cumulated vsize (Kb) 47064

[startup+260.026 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 13198
Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13194/statm): 531 226 485 147 0 384 0
[pid=13194] vsize: 2124
Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 10868 0 0 0 25897 50 0 0 25 0 1 0 1843395308 46620672 10513 4294967295 134512640 135094434 3221224448 3221223120 134555579 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13198/statm): 11382 10513 145 145 0 11237 0
[pid=13198] vsize: 45528
Current children cumulated CPU time (s) 259.47
Current children cumulated vsize (Kb) 47652

[startup+270.027 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 13198
Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13194/statm): 531 226 485 147 0 384 0
[pid=13194] vsize: 2124
Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 10990 0 0 0 26895 50 0 0 25 0 1 0 1843395308 47112192 10635 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13198/statm): 11502 10635 145 145 0 11357 0
[pid=13198] vsize: 46008
Current children cumulated CPU time (s) 269.45
Current children cumulated vsize (Kb) 48132

[startup+280.028 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 13198
Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13194/statm): 531 226 485 147 0 384 0
[pid=13194] vsize: 2124
Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 11128 0 0 0 27893 52 0 0 25 0 1 0 1843395308 47673344 10773 4294967295 134512640 135094434 3221224448 3221223072 134557568 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13198/statm): 11639 10773 145 145 0 11494 0
[pid=13198] vsize: 46556
Current children cumulated CPU time (s) 279.45
Current children cumulated vsize (Kb) 48680

[startup+290.028 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 13198
Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13194/statm): 531 226 485 147 0 384 0
[pid=13194] vsize: 2124
Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 11227 0 0 0 28892 52 0 0 25 0 1 0 1843395308 48074752 10872 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13198/statm): 11737 10872 145 145 0 11592 0
[pid=13198] vsize: 46948
Current children cumulated CPU time (s) 289.44
Current children cumulated vsize (Kb) 49072

[startup+300.029 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 13198
Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13194/statm): 531 226 485 147 0 384 0
[pid=13194] vsize: 2124
Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 11309 0 0 0 29890 53 0 0 25 0 1 0 1843395308 48406528 10954 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13198/statm): 11818 10954 145 145 0 11673 0
[pid=13198] vsize: 47272
Current children cumulated CPU time (s) 299.43
Current children cumulated vsize (Kb) 49396

[startup+310.03 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 13198
Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13194/statm): 531 226 485 147 0 384 0
[pid=13194] vsize: 2124
Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 11375 0 0 0 30890 54 0 0 25 0 1 0 1843395308 48672768 11020 4294967295 134512640 135094434 3221224448 3221223040 134556812 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13198/statm): 11883 11020 145 145 0 11738 0
[pid=13198] vsize: 47532
Current children cumulated CPU time (s) 309.44
Current children cumulated vsize (Kb) 49656

[startup+320.03 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 13198
Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13194/statm): 531 226 485 147 0 384 0
[pid=13194] vsize: 2124
Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 11438 0 0 0 31889 54 0 0 25 0 1 0 1843395308 48930816 11083 4294967295 134512640 135094434 3221224448 3221223040 134556851 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13198/statm): 11946 11083 145 145 0 11801 0
[pid=13198] vsize: 47784
Current children cumulated CPU time (s) 319.43
Current children cumulated vsize (Kb) 49908

[startup+330.032 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 13198
Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13194/statm): 531 226 485 147 0 384 0
[pid=13194] vsize: 2124
Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 11498 0 0 0 32888 55 0 0 25 0 1 0 1843395308 49172480 11143 4294967295 134512640 135094434 3221224448 3221223040 134557269 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13198/statm): 12005 11143 145 145 0 11860 0
[pid=13198] vsize: 48020
Current children cumulated CPU time (s) 329.43
Current children cumulated vsize (Kb) 50144

[startup+340.033 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 13198
Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13194/statm): 531 226 485 147 0 384 0
[pid=13194] vsize: 2124
Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 11552 0 0 0 33887 55 0 0 25 0 1 0 1843395308 49393664 11197 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13198/statm): 12059 11197 145 145 0 11914 0
[pid=13198] vsize: 48236
Current children cumulated CPU time (s) 339.42
Current children cumulated vsize (Kb) 50360

[startup+350.034 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 13198
Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13194/statm): 531 226 485 147 0 384 0
[pid=13194] vsize: 2124
Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 11617 0 0 0 34885 56 0 0 25 0 1 0 1843395308 49655808 11262 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13198/statm): 12123 11262 145 145 0 11978 0
[pid=13198] vsize: 48492
Current children cumulated CPU time (s) 349.41
Current children cumulated vsize (Kb) 50616

[startup+360.034 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 13198
Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13194/statm): 531 226 485 147 0 384 0
[pid=13194] vsize: 2124
Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 11688 0 0 0 35884 57 0 0 25 0 1 0 1843395308 49946624 11333 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13198/statm): 12194 11333 145 145 0 12049 0
[pid=13198] vsize: 48776
Current children cumulated CPU time (s) 359.41
Current children cumulated vsize (Kb) 50900

[startup+370.034 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 13198
Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13194/statm): 531 226 485 147 0 384 0
[pid=13194] vsize: 2124
Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 11771 0 0 0 36882 58 0 0 25 0 1 0 1843395308 50282496 11416 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13198/statm): 12276 11416 145 145 0 12131 0
[pid=13198] vsize: 49104
Current children cumulated CPU time (s) 369.4
Current children cumulated vsize (Kb) 51228

[startup+380.035 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 13198
Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13194/statm): 531 226 485 147 0 384 0
[pid=13194] vsize: 2124
Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 11837 0 0 0 37881 58 0 0 25 0 1 0 1843395308 50548736 11482 4294967295 134512640 135094434 3221224448 3221223040 134556851 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13198/statm): 12341 11482 145 145 0 12196 0
[pid=13198] vsize: 49364
Current children cumulated CPU time (s) 379.39
Current children cumulated vsize (Kb) 51488

[startup+390.035 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 13198
Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13194/statm): 531 226 485 147 0 384 0
[pid=13194] vsize: 2124
Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 11908 0 0 0 38880 59 0 0 25 0 1 0 1843395308 50839552 11553 4294967295 134512640 135094434 3221224448 3221223040 134556870 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13198/statm): 12412 11553 145 145 0 12267 0
[pid=13198] vsize: 49648
Current children cumulated CPU time (s) 389.39
Current children cumulated vsize (Kb) 51772

[startup+400.037 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 13198
Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13194/statm): 531 226 485 147 0 384 0
[pid=13194] vsize: 2124
Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 11980 0 0 0 39879 59 0 0 25 0 1 0 1843395308 51130368 11625 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13198/statm): 12483 11625 145 145 0 12338 0
[pid=13198] vsize: 49932
Current children cumulated CPU time (s) 399.38
Current children cumulated vsize (Kb) 52056

[startup+410.038 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 13198
Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13194/statm): 531 226 485 147 0 384 0
[pid=13194] vsize: 2124
Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 12022 0 0 0 40877 60 0 0 25 0 1 0 1843395308 51302400 11667 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13198/statm): 12525 11667 145 145 0 12380 0
[pid=13198] vsize: 50100
Current children cumulated CPU time (s) 409.37
Current children cumulated vsize (Kb) 52224

[startup+420.038 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 13198
Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13194/statm): 531 226 485 147 0 384 0
[pid=13194] vsize: 2124
Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 12086 0 0 0 41876 60 0 0 25 0 1 0 1843395308 51560448 11731 4294967295 134512640 135094434 3221224448 3221223108 134553508 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13198/statm): 12588 11731 145 145 0 12443 0
[pid=13198] vsize: 50352
Current children cumulated CPU time (s) 419.36
Current children cumulated vsize (Kb) 52476

[startup+430.038 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 13198
Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13194/statm): 531 226 485 147 0 384 0
[pid=13194] vsize: 2124
Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 12198 0 0 0 42874 61 0 0 25 0 1 0 1843395308 52015104 11843 4294967295 134512640 135094434 3221224448 3221221648 134677346 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13198/statm): 12699 11843 145 145 0 12554 0
[pid=13198] vsize: 50796
Current children cumulated CPU time (s) 429.35
Current children cumulated vsize (Kb) 52920

[startup+440.039 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 13198
Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13194/statm): 531 226 485 147 0 384 0
[pid=13194] vsize: 2124
Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 12218 0 0 0 43874 62 0 0 25 0 1 0 1843395308 52092928 11863 4294967295 134512640 135094434 3221224448 3221223072 134557612 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13198/statm): 12718 11863 145 145 0 12573 0
[pid=13198] vsize: 50872
Current children cumulated CPU time (s) 439.36
Current children cumulated vsize (Kb) 52996

[startup+450.04 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 13198
Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13194/statm): 531 226 485 147 0 384 0
[pid=13194] vsize: 2124
Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 12259 0 0 0 44874 62 0 0 25 0 1 0 1843395308 52256768 11904 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13198/statm): 12758 11904 145 145 0 12613 0
[pid=13198] vsize: 51032
Current children cumulated CPU time (s) 449.36
Current children cumulated vsize (Kb) 53156

[startup+460.041 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 13198
Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13194/statm): 531 226 485 147 0 384 0
[pid=13194] vsize: 2124
Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 12331 0 0 0 45873 62 0 0 25 0 1 0 1843395308 52805632 11976 4294967295 134512640 135094434 3221224448 3221223104 134558411 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13198/statm): 12892 11976 145 145 0 12747 0
[pid=13198] vsize: 51568
Current children cumulated CPU time (s) 459.35
Current children cumulated vsize (Kb) 53692

[startup+470.041 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 13198
Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13194/statm): 531 226 485 147 0 384 0
[pid=13194] vsize: 2124
Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 12412 0 0 0 46872 62 0 0 25 0 1 0 1843395308 53129216 12057 4294967295 134512640 135094434 3221224448 3221223104 134557866 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13198/statm): 12971 12057 145 145 0 12826 0
[pid=13198] vsize: 51884
Current children cumulated CPU time (s) 469.34
Current children cumulated vsize (Kb) 54008

[startup+480.042 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 13198
Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13194/statm): 531 226 485 147 0 384 0
[pid=13194] vsize: 2124
Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 12523 0 0 0 47870 63 0 0 25 0 1 0 1843395308 53579776 12168 4294967295 134512640 135094434 3221224448 3221223072 134557596 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13198/statm): 13081 12168 145 145 0 12936 0
[pid=13198] vsize: 52324
Current children cumulated CPU time (s) 479.33
Current children cumulated vsize (Kb) 54448

[startup+490.043 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 13198
Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13194/statm): 531 226 485 147 0 384 0
[pid=13194] vsize: 2124
Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 12580 0 0 0 48870 64 0 0 25 0 1 0 1843395308 53809152 12225 4294967295 134512640 135094434 3221224448 3221223104 134558169 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13198/statm): 13137 12225 145 145 0 12992 0
[pid=13198] vsize: 52548
Current children cumulated CPU time (s) 489.34
Current children cumulated vsize (Kb) 54672

[startup+500.044 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 13198
Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13194/statm): 531 226 485 147 0 384 0
[pid=13194] vsize: 2124
Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 12646 0 0 0 49869 64 0 0 25 0 1 0 1843395308 54075392 12291 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13198/statm): 13202 12291 145 145 0 13057 0
[pid=13198] vsize: 52808
Current children cumulated CPU time (s) 499.33
Current children cumulated vsize (Kb) 54932

[startup+510.045 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 13198
Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13194/statm): 531 226 485 147 0 384 0
[pid=13194] vsize: 2124
Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 12689 0 0 0 50869 64 0 0 25 0 1 0 1843395308 54247424 12334 4294967295 134512640 135094434 3221224448 3221223104 134557860 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13198/statm): 13244 12334 145 145 0 13099 0
[pid=13198] vsize: 52976
Current children cumulated CPU time (s) 509.33
Current children cumulated vsize (Kb) 55100

[startup+520.046 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 13198
Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13194/statm): 531 226 485 147 0 384 0
[pid=13194] vsize: 2124
Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 12791 0 0 0 51868 65 0 0 25 0 1 0 1843395308 54661120 12436 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13198/statm): 13345 12436 145 145 0 13200 0
[pid=13198] vsize: 53380
Current children cumulated CPU time (s) 519.33
Current children cumulated vsize (Kb) 55504

[startup+530.047 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 13198
Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13194/statm): 531 226 485 147 0 384 0
[pid=13194] vsize: 2124
Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 12979 0 0 0 52865 66 0 0 25 0 1 0 1843395308 55427072 12624 4294967295 134512640 135094434 3221224448 3221223104 134557875 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13198/statm): 13532 12624 145 145 0 13387 0
[pid=13198] vsize: 54128
Current children cumulated CPU time (s) 529.31
Current children cumulated vsize (Kb) 56252

[startup+540.047 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 13198
Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13194/statm): 531 226 485 147 0 384 0
[pid=13194] vsize: 2124
Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 13022 0 0 0 53864 66 0 0 25 0 1 0 1843395308 55599104 12667 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13198/statm): 13574 12667 145 145 0 13429 0
[pid=13198] vsize: 54296
Current children cumulated CPU time (s) 539.3
Current children cumulated vsize (Kb) 56420

[startup+550.049 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 13198
Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13194/statm): 531 226 485 147 0 384 0
[pid=13194] vsize: 2124
Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 13086 0 0 0 54863 67 0 0 25 0 1 0 1843395308 55853056 12731 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13198/statm): 13636 12731 145 145 0 13491 0
[pid=13198] vsize: 54544
Current children cumulated CPU time (s) 549.3
Current children cumulated vsize (Kb) 56668

[startup+560.05 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 13198
Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13194/statm): 531 226 485 147 0 384 0
[pid=13194] vsize: 2124
Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 13198 0 0 0 55861 68 0 0 25 0 1 0 1843395308 56303616 12843 4294967295 134512640 135094434 3221224448 3221223104 134558004 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13198/statm): 13746 12843 145 145 0 13601 0
[pid=13198] vsize: 54984
Current children cumulated CPU time (s) 559.29
Current children cumulated vsize (Kb) 57108

[startup+570.05 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 13198
Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13194/statm): 531 226 485 147 0 384 0
[pid=13194] vsize: 2124
Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 13343 0 0 0 56859 69 0 0 25 0 1 0 1843395308 56885248 12988 4294967295 134512640 135094434 3221224448 3221223072 134557596 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13198/statm): 13888 12988 145 145 0 13743 0
[pid=13198] vsize: 55552
Current children cumulated CPU time (s) 569.28
Current children cumulated vsize (Kb) 57676

[startup+580.051 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 13198
Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13194/statm): 531 226 485 147 0 384 0
[pid=13194] vsize: 2124
Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 13372 0 0 0 57859 69 0 0 25 0 1 0 1843395308 57004032 13017 4294967295 134512640 135094434 3221224448 3221223072 134557728 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13198/statm): 13917 13017 145 145 0 13772 0
[pid=13198] vsize: 55668
Current children cumulated CPU time (s) 579.28
Current children cumulated vsize (Kb) 57792

[startup+590.052 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 13198
Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13194/statm): 531 226 485 147 0 384 0
[pid=13194] vsize: 2124
Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 13449 0 0 0 58857 70 0 0 25 0 1 0 1843395308 57315328 13094 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13198/statm): 13993 13094 145 145 0 13848 0
[pid=13198] vsize: 55972
Current children cumulated CPU time (s) 589.27
Current children cumulated vsize (Kb) 58096

[startup+600.053 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 13198
Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13194/statm): 531 226 485 147 0 384 0
[pid=13194] vsize: 2124
Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 13544 0 0 0 59857 70 0 0 25 0 1 0 1843395308 57700352 13189 4294967295 134512640 135094434 3221224448 3221223040 134557273 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13198/statm): 14087 13189 145 145 0 13942 0
[pid=13198] vsize: 56348
Current children cumulated CPU time (s) 599.27
Current children cumulated vsize (Kb) 58472

[startup+610.053 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 13198
Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13194/statm): 531 226 485 147 0 384 0
[pid=13194] vsize: 2124
Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 13617 0 0 0 60855 71 0 0 25 0 1 0 1843395308 57991168 13262 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13198/statm): 14158 13262 145 145 0 14013 0
[pid=13198] vsize: 56632
Current children cumulated CPU time (s) 609.26
Current children cumulated vsize (Kb) 58756

[startup+620.054 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 13198
Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13194/statm): 531 226 485 147 0 384 0
[pid=13194] vsize: 2124
Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 13768 0 0 0 61854 72 0 0 25 0 1 0 1843395308 58609664 13413 4294967295 134512640 135094434 3221224448 3221223236 134553536 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13198/statm): 14309 13413 145 145 0 14164 0
[pid=13198] vsize: 57236
Current children cumulated CPU time (s) 619.26
Current children cumulated vsize (Kb) 59360

[startup+630.055 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 13198
Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13194/statm): 531 226 485 147 0 384 0
[pid=13194] vsize: 2124
Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 13815 0 0 0 62853 72 0 0 25 0 1 0 1843395308 58798080 13460 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13198/statm): 14355 13460 145 145 0 14210 0
[pid=13198] vsize: 57420
Current children cumulated CPU time (s) 629.25
Current children cumulated vsize (Kb) 59544

[startup+640.056 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 13198
Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13194/statm): 531 226 485 147 0 384 0
[pid=13194] vsize: 2124
Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 13931 0 0 0 63852 73 0 0 25 0 1 0 1843395308 59269120 13576 4294967295 134512640 135094434 3221224448 3221223084 134557639 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13198/statm): 14470 13576 145 145 0 14325 0
[pid=13198] vsize: 57880
Current children cumulated CPU time (s) 639.25
Current children cumulated vsize (Kb) 60004

[startup+650.057 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 13198
Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13194/statm): 531 226 485 147 0 384 0
[pid=13194] vsize: 2124
Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 13990 0 0 0 64851 73 0 0 25 0 1 0 1843395308 59506688 13635 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13198/statm): 14528 13635 145 145 0 14383 0
[pid=13198] vsize: 58112
Current children cumulated CPU time (s) 649.24
Current children cumulated vsize (Kb) 60236

[startup+660.058 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 13198
Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13194/statm): 531 226 485 147 0 384 0
[pid=13194] vsize: 2124
Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 14038 0 0 0 65850 73 0 0 25 0 1 0 1843395308 59695104 13683 4294967295 134512640 135094434 3221224448 3221223072 134557596 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13198/statm): 14574 13683 145 145 0 14429 0
[pid=13198] vsize: 58296
Current children cumulated CPU time (s) 659.23
Current children cumulated vsize (Kb) 60420

[startup+670.059 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 13198
Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13194/statm): 531 226 485 147 0 384 0
[pid=13194] vsize: 2124
Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 14144 0 0 0 66848 74 0 0 25 0 1 0 1843395308 60133376 13789 4294967295 134512640 135094434 3221224448 3221223104 134557879 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13198/statm): 14681 13789 145 145 0 14536 0
[pid=13198] vsize: 58724
Current children cumulated CPU time (s) 669.22
Current children cumulated vsize (Kb) 60848

[startup+680.06 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 13198
Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13194/statm): 531 226 485 147 0 384 0
[pid=13194] vsize: 2124
Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 14233 0 0 0 67847 75 0 0 25 0 1 0 1843395308 60493824 13878 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13198/statm): 14769 13878 145 145 0 14624 0
[pid=13198] vsize: 59076
Current children cumulated CPU time (s) 679.22
Current children cumulated vsize (Kb) 61200

[startup+690.061 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 13198
Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13194/statm): 531 226 485 147 0 384 0
[pid=13194] vsize: 2124
Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 14327 0 0 0 68846 75 0 0 25 0 1 0 1843395308 60874752 13972 4294967295 134512640 135094434 3221224448 3221223104 134557813 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13198/statm): 14862 13972 145 145 0 14717 0
[pid=13198] vsize: 59448
Current children cumulated CPU time (s) 689.21
Current children cumulated vsize (Kb) 61572

[startup+700.063 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 13198
Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13194/statm): 531 226 485 147 0 384 0
[pid=13194] vsize: 2124
Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 14486 0 0 0 69843 76 0 0 25 0 1 0 1843395308 61526016 14131 4294967295 134512640 135094434 3221224448 3221223040 134556975 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13198/statm): 15021 14131 145 145 0 14876 0
[pid=13198] vsize: 60084
Current children cumulated CPU time (s) 699.19
Current children cumulated vsize (Kb) 62208

[startup+710.064 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 13198
Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13194/statm): 531 226 485 147 0 384 0
[pid=13194] vsize: 2124
Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 14622 0 0 0 70842 77 0 0 25 0 1 0 1843395308 62078976 14267 4294967295 134512640 135094434 3221224448 3221223100 134558255 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13198/statm): 15156 14267 145 145 0 15011 0
[pid=13198] vsize: 60624
Current children cumulated CPU time (s) 709.19
Current children cumulated vsize (Kb) 62748

[startup+720.063 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 13198
Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13194/statm): 531 226 485 147 0 384 0
[pid=13194] vsize: 2124
Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 14806 0 0 0 71840 78 0 0 25 0 1 0 1843395308 62828544 14451 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13198/statm): 15339 14451 145 145 0 15194 0
[pid=13198] vsize: 61356
Current children cumulated CPU time (s) 719.18
Current children cumulated vsize (Kb) 63480

[startup+730.064 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 13198
Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13194/statm): 531 226 485 147 0 384 0
[pid=13194] vsize: 2124
Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 14889 0 0 0 72839 78 0 0 25 0 1 0 1843395308 63168512 14534 4294967295 134512640 135094434 3221224448 3221223040 134556802 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13198/statm): 15422 14534 145 145 0 15277 0
[pid=13198] vsize: 61688
Current children cumulated CPU time (s) 729.17
Current children cumulated vsize (Kb) 63812

[startup+740.065 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 13198
Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13194/statm): 531 226 485 147 0 384 0
[pid=13194] vsize: 2124
Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 14981 0 0 0 73838 79 0 0 25 0 1 0 1843395308 63524864 14626 4294967295 134512640 135094434 3221224448 3221223060 134563083 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13198/statm): 15509 14626 145 145 0 15364 0
[pid=13198] vsize: 62036
Current children cumulated CPU time (s) 739.17
Current children cumulated vsize (Kb) 64160

[startup+750.066 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 13198
Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13194/statm): 531 226 485 147 0 384 0
[pid=13194] vsize: 2124
Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 15013 0 0 0 74838 79 0 0 25 0 1 0 1843395308 63651840 14658 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13198/statm): 15540 14658 145 145 0 15395 0
[pid=13198] vsize: 62160
Current children cumulated CPU time (s) 749.17
Current children cumulated vsize (Kb) 64284

[startup+760.066 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 13198
Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13194/statm): 531 226 485 147 0 384 0
[pid=13194] vsize: 2124
Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 15013 0 0 0 75838 79 0 0 25 0 1 0 1843395308 63651840 14658 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13198/statm): 15540 14658 145 145 0 15395 0
[pid=13198] vsize: 62160
Current children cumulated CPU time (s) 759.17
Current children cumulated vsize (Kb) 64284

[startup+770.067 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 13198
Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13194/statm): 531 226 485 147 0 384 0
[pid=13194] vsize: 2124
Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 15013 0 0 0 76838 79 0 0 25 0 1 0 1843395308 63651840 14658 4294967295 134512640 135094434 3221224448 3221223120 134555574 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13198/statm): 15540 14658 145 145 0 15395 0
[pid=13198] vsize: 62160
Current children cumulated CPU time (s) 769.17
Current children cumulated vsize (Kb) 64284

[startup+780.069 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 13198
Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13194/statm): 531 226 485 147 0 384 0
[pid=13194] vsize: 2124
Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 15013 0 0 0 77837 80 0 0 25 0 1 0 1843395308 63651840 14658 4294967295 134512640 135094434 3221224448 3221223104 134557866 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13198/statm): 15540 14658 145 145 0 15395 0
[pid=13198] vsize: 62160
Current children cumulated CPU time (s) 779.17
Current children cumulated vsize (Kb) 64284

[startup+790.069 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 13198
Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13194/statm): 531 226 485 147 0 384 0
[pid=13194] vsize: 2124
Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 15013 0 0 0 78837 80 0 0 25 0 1 0 1843395308 63651840 14658 4294967295 134512640 135094434 3221224448 3221223104 134557872 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13198/statm): 15540 14658 145 145 0 15395 0
[pid=13198] vsize: 62160
Current children cumulated CPU time (s) 789.17
Current children cumulated vsize (Kb) 64284

[startup+800.071 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 13198
Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13194/statm): 531 226 485 147 0 384 0
[pid=13194] vsize: 2124
Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 15013 0 0 0 79836 80 0 0 25 0 1 0 1843395308 63651840 14658 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13198/statm): 15540 14658 145 145 0 15395 0
[pid=13198] vsize: 62160
Current children cumulated CPU time (s) 799.16
Current children cumulated vsize (Kb) 64284

[startup+810.073 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 13198
Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13194/statm): 531 226 485 147 0 384 0
[pid=13194] vsize: 2124
Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 15013 0 0 0 80837 80 0 0 25 0 1 0 1843395308 63651840 14658 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13198/statm): 15540 14658 145 145 0 15395 0
[pid=13198] vsize: 62160
Current children cumulated CPU time (s) 809.17
Current children cumulated vsize (Kb) 64284

[startup+820.073 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 13198
Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13194/statm): 531 226 485 147 0 384 0
[pid=13194] vsize: 2124
Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 15013 0 0 0 81837 80 0 0 25 0 1 0 1843395308 63651840 14658 4294967295 134512640 135094434 3221224448 3221223104 134558221 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13198/statm): 15540 14658 145 145 0 15395 0
[pid=13198] vsize: 62160
Current children cumulated CPU time (s) 819.17
Current children cumulated vsize (Kb) 64284

[startup+830.074 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 13198
Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13194/statm): 531 226 485 147 0 384 0
[pid=13194] vsize: 2124
Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 15013 0 0 0 82837 80 0 0 25 0 1 0 1843395308 63651840 14658 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13198/statm): 15540 14658 145 145 0 15395 0
[pid=13198] vsize: 62160
Current children cumulated CPU time (s) 829.17
Current children cumulated vsize (Kb) 64284

[startup+840.075 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 13198
Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13194/statm): 531 226 485 147 0 384 0
[pid=13194] vsize: 2124
Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 15014 0 0 0 83838 80 0 0 25 0 1 0 1843395308 63651840 14659 4294967295 134512640 135094434 3221224448 3221221472 134676489 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13198/statm): 15540 14659 145 145 0 15395 0
[pid=13198] vsize: 62160
Current children cumulated CPU time (s) 839.18
Current children cumulated vsize (Kb) 64284

[startup+850.077 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 13198
Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13194/statm): 531 226 485 147 0 384 0
[pid=13194] vsize: 2124
Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 15016 0 0 0 84838 80 0 0 25 0 1 0 1843395308 63651840 14661 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13198/statm): 15540 14661 145 145 0 15395 0
[pid=13198] vsize: 62160
Current children cumulated CPU time (s) 849.18
Current children cumulated vsize (Kb) 64284

[startup+860.077 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 13198
Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13194/statm): 531 226 485 147 0 384 0
[pid=13194] vsize: 2124
Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 15017 0 0 0 85838 80 0 0 25 0 1 0 1843395308 63651840 14662 4294967295 134512640 135094434 3221224448 3221223104 134558013 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13198/statm): 15540 14662 145 145 0 15395 0
[pid=13198] vsize: 62160
Current children cumulated CPU time (s) 859.18
Current children cumulated vsize (Kb) 64284

[startup+870.078 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 13198
Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13194/statm): 531 226 485 147 0 384 0
[pid=13194] vsize: 2124
Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 15017 0 0 0 86838 80 0 0 25 0 1 0 1843395308 63651840 14662 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13198/statm): 15540 14662 145 145 0 15395 0
[pid=13198] vsize: 62160
Current children cumulated CPU time (s) 869.18
Current children cumulated vsize (Kb) 64284

[startup+880.08 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 13198
Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13194/statm): 531 226 485 147 0 384 0
[pid=13194] vsize: 2124
Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 15017 0 0 0 87838 80 0 0 25 0 1 0 1843395308 63651840 14662 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13198/statm): 15540 14662 145 145 0 15395 0
[pid=13198] vsize: 62160
Current children cumulated CPU time (s) 879.18
Current children cumulated vsize (Kb) 64284

[startup+890.081 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 13198
Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13194/statm): 531 226 485 147 0 384 0
[pid=13194] vsize: 2124
Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 15017 0 0 0 88839 80 0 0 25 0 1 0 1843395308 63651840 14662 4294967295 134512640 135094434 3221224448 3221223104 134557832 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13198/statm): 15540 14662 145 145 0 15395 0
[pid=13198] vsize: 62160
Current children cumulated CPU time (s) 889.19
Current children cumulated vsize (Kb) 64284

[startup+900.081 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 13198
Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13194/statm): 531 226 485 147 0 384 0
[pid=13194] vsize: 2124
Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 15017 0 0 0 89839 80 0 0 25 0 1 0 1843395308 63651840 14662 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13198/statm): 15540 14662 145 145 0 15395 0
[pid=13198] vsize: 62160
Current children cumulated CPU time (s) 899.19
Current children cumulated vsize (Kb) 64284

[startup+910.082 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 13198
Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13194/statm): 531 226 485 147 0 384 0
[pid=13194] vsize: 2124
Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 15017 0 0 0 90839 81 0 0 25 0 1 0 1843395308 63651840 14662 4294967295 134512640 135094434 3221224448 3221223072 134557737 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13198/statm): 15540 14662 145 145 0 15395 0
[pid=13198] vsize: 62160
Current children cumulated CPU time (s) 909.2
Current children cumulated vsize (Kb) 64284

[startup+920.083 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 13198
Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13194/statm): 531 226 485 147 0 384 0
[pid=13194] vsize: 2124
Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 15017 0 0 0 91839 81 0 0 25 0 1 0 1843395308 63651840 14662 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13198/statm): 15540 14662 145 145 0 15395 0
[pid=13198] vsize: 62160
Current children cumulated CPU time (s) 919.2
Current children cumulated vsize (Kb) 64284

[startup+930.083 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 13198
Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13194/statm): 531 226 485 147 0 384 0
[pid=13194] vsize: 2124
Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 15017 0 0 0 92839 81 0 0 25 0 1 0 1843395308 63651840 14662 4294967295 134512640 135094434 3221224448 3221223104 134558187 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13198/statm): 15540 14662 145 145 0 15395 0
[pid=13198] vsize: 62160
Current children cumulated CPU time (s) 929.2
Current children cumulated vsize (Kb) 64284

[startup+940.084 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 13198
Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13194/statm): 531 226 485 147 0 384 0
[pid=13194] vsize: 2124
Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 15017 0 0 0 93840 81 0 0 25 0 1 0 1843395308 63651840 14662 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13198/statm): 15540 14662 145 145 0 15395 0
[pid=13198] vsize: 62160
Current children cumulated CPU time (s) 939.21
Current children cumulated vsize (Kb) 64284

[startup+950.086 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 13198
Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13194/statm): 531 226 485 147 0 384 0
[pid=13194] vsize: 2124
Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 15017 0 0 0 94840 81 0 0 25 0 1 0 1843395308 63651840 14662 4294967295 134512640 135094434 3221224448 3221223136 134554723 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13198/statm): 15540 14662 145 145 0 15395 0
[pid=13198] vsize: 62160
Current children cumulated CPU time (s) 949.21
Current children cumulated vsize (Kb) 64284

[startup+960.087 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 13198
Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13194/statm): 531 226 485 147 0 384 0
[pid=13194] vsize: 2124
Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 15017 0 0 0 95839 81 0 0 25 0 1 0 1843395308 63651840 14662 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13198/statm): 15540 14662 145 145 0 15395 0
[pid=13198] vsize: 62160
Current children cumulated CPU time (s) 959.2
Current children cumulated vsize (Kb) 64284

[startup+970.087 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 13198
Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13194/statm): 531 226 485 147 0 384 0
[pid=13194] vsize: 2124
Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 15017 0 0 0 96839 81 0 0 25 0 1 0 1843395308 63651840 14662 4294967295 134512640 135094434 3221224448 3221223104 134557988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13198/statm): 15540 14662 145 145 0 15395 0
[pid=13198] vsize: 62160
Current children cumulated CPU time (s) 969.2
Current children cumulated vsize (Kb) 64284

[startup+980.088 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 13198
Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13194/statm): 531 226 485 147 0 384 0
[pid=13194] vsize: 2124
Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 15017 0 0 0 97839 81 0 0 25 0 1 0 1843395308 63651840 14662 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13198/statm): 15540 14662 145 145 0 15395 0
[pid=13198] vsize: 62160
Current children cumulated CPU time (s) 979.2
Current children cumulated vsize (Kb) 64284

[startup+990.089 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 13198
Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13194/statm): 531 226 485 147 0 384 0
[pid=13194] vsize: 2124
Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 15017 0 0 0 98839 81 0 0 25 0 1 0 1843395308 63651840 14662 4294967295 134512640 135094434 3221224448 3221223120 134556317 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13198/statm): 15540 14662 145 145 0 15395 0
[pid=13198] vsize: 62160
Current children cumulated CPU time (s) 989.2
Current children cumulated vsize (Kb) 64284

[startup+1000.09 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 13198
Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13194/statm): 531 226 485 147 0 384 0
[pid=13194] vsize: 2124
Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 15017 0 0 0 99839 81 0 0 25 0 1 0 1843395308 63651840 14662 4294967295 134512640 135094434 3221224448 3221223104 134558210 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13198/statm): 15540 14662 145 145 0 15395 0
[pid=13198] vsize: 62160
Current children cumulated CPU time (s) 999.2
Current children cumulated vsize (Kb) 64284

[startup+1010.09 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 13198
Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13194/statm): 531 226 485 147 0 384 0
[pid=13194] vsize: 2124
Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 15017 0 0 0 100840 81 0 0 25 0 1 0 1843395308 63651840 14662 4294967295 134512640 135094434 3221224448 3221223104 134557875 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13198/statm): 15540 14662 145 145 0 15395 0
[pid=13198] vsize: 62160
Current children cumulated CPU time (s) 1009.21
Current children cumulated vsize (Kb) 64284

[startup+1020.09 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 13198
Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13194/statm): 531 226 485 147 0 384 0
[pid=13194] vsize: 2124
Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 15017 0 0 0 101840 81 0 0 25 0 1 0 1843395308 63651840 14662 4294967295 134512640 135094434 3221224448 3221223040 134557537 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13198/statm): 15540 14662 145 145 0 15395 0
[pid=13198] vsize: 62160
Current children cumulated CPU time (s) 1019.21
Current children cumulated vsize (Kb) 64284

[startup+1030.09 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 13198
Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13194/statm): 531 226 485 147 0 384 0
[pid=13194] vsize: 2124
Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 15017 0 0 0 102840 81 0 0 25 0 1 0 1843395308 63651840 14662 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13198/statm): 15540 14662 145 145 0 15395 0
[pid=13198] vsize: 62160
Current children cumulated CPU time (s) 1029.21
Current children cumulated vsize (Kb) 64284

[startup+1040.09 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 13198
Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13194/statm): 531 226 485 147 0 384 0
[pid=13194] vsize: 2124
Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 15017 0 0 0 103840 81 0 0 25 0 1 0 1843395308 63651840 14662 4294967295 134512640 135094434 3221224448 3221223104 134558289 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13198/statm): 15540 14662 145 145 0 15395 0
[pid=13198] vsize: 62160
Current children cumulated CPU time (s) 1039.21
Current children cumulated vsize (Kb) 64284

[startup+1050.1 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 13198
Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13194/statm): 531 226 485 147 0 384 0
[pid=13194] vsize: 2124
Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 15017 0 0 0 104841 81 0 0 25 0 1 0 1843395308 63651840 14662 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13198/statm): 15540 14662 145 145 0 15395 0
[pid=13198] vsize: 62160
Current children cumulated CPU time (s) 1049.22
Current children cumulated vsize (Kb) 64284

[startup+1060.1 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 13198
Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13194/statm): 531 226 485 147 0 384 0
[pid=13194] vsize: 2124
Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 15017 0 0 0 105841 81 0 0 25 0 1 0 1843395308 63651840 14662 4294967295 134512640 135094434 3221224448 3221223104 134557978 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13198/statm): 15540 14662 145 145 0 15395 0
[pid=13198] vsize: 62160
Current children cumulated CPU time (s) 1059.22
Current children cumulated vsize (Kb) 64284

[startup+1070.1 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 13198
Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13194/statm): 531 226 485 147 0 384 0
[pid=13194] vsize: 2124
Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 15018 0 0 0 106841 81 0 0 25 0 1 0 1843395308 63651840 14663 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13198/statm): 15540 14663 145 145 0 15395 0
[pid=13198] vsize: 62160
Current children cumulated CPU time (s) 1069.22
Current children cumulated vsize (Kb) 64284

[startup+1080.1 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 13198
Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13194/statm): 531 226 485 147 0 384 0
[pid=13194] vsize: 2124
Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 15018 0 0 0 107841 81 0 0 25 0 1 0 1843395308 63651840 14663 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13198/statm): 15540 14663 145 145 0 15395 0
[pid=13198] vsize: 62160
Current children cumulated CPU time (s) 1079.22
Current children cumulated vsize (Kb) 64284

[startup+1090.1 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 13198
Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13194/statm): 531 226 485 147 0 384 0
[pid=13194] vsize: 2124
Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 15018 0 0 0 108842 81 0 0 25 0 1 0 1843395308 63651840 14663 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13198/statm): 15540 14663 145 145 0 15395 0
[pid=13198] vsize: 62160
Current children cumulated CPU time (s) 1089.23
Current children cumulated vsize (Kb) 64284

[startup+1100.1 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 13198
Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13194/statm): 531 226 485 147 0 384 0
[pid=13194] vsize: 2124
Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 15018 0 0 0 109842 81 0 0 25 0 1 0 1843395308 63651840 14663 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13198/statm): 15540 14663 145 145 0 15395 0
[pid=13198] vsize: 62160
Current children cumulated CPU time (s) 1099.23
Current children cumulated vsize (Kb) 64284

[startup+1110.1 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 13198
Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13194/statm): 531 226 485 147 0 384 0
[pid=13194] vsize: 2124
Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 15018 0 0 0 110842 81 0 0 25 0 1 0 1843395308 63651840 14663 4294967295 134512640 135094434 3221224448 3221223040 134557034 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13198/statm): 15540 14663 145 145 0 15395 0
[pid=13198] vsize: 62160
Current children cumulated CPU time (s) 1109.23
Current children cumulated vsize (Kb) 64284

[startup+1120.1 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 13198
Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13194/statm): 531 226 485 147 0 384 0
[pid=13194] vsize: 2124
Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 15018 0 0 0 111842 81 0 0 25 0 1 0 1843395308 63651840 14663 4294967295 134512640 135094434 3221224448 3221221216 134677138 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13198/statm): 15540 14663 145 145 0 15395 0
[pid=13198] vsize: 62160
Current children cumulated CPU time (s) 1119.23
Current children cumulated vsize (Kb) 64284

[startup+1130.1 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 13198
Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13194/statm): 531 226 485 147 0 384 0
[pid=13194] vsize: 2124
Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 15018 0 0 0 112843 82 0 0 25 0 1 0 1843395308 63651840 14663 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13198/statm): 15540 14663 145 145 0 15395 0
[pid=13198] vsize: 62160
Current children cumulated CPU time (s) 1129.25
Current children cumulated vsize (Kb) 64284

[startup+1140.1 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 13198
Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13194/statm): 531 226 485 147 0 384 0
[pid=13194] vsize: 2124
Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 15018 0 0 0 113843 82 0 0 25 0 1 0 1843395308 63651840 14663 4294967295 134512640 135094434 3221224448 3221223108 134553536 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13198/statm): 15540 14663 145 145 0 15395 0
[pid=13198] vsize: 62160
Current children cumulated CPU time (s) 1139.25
Current children cumulated vsize (Kb) 64284

[startup+1150.11 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 13198
Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13194/statm): 531 226 485 147 0 384 0
[pid=13194] vsize: 2124
Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 15018 0 0 0 114843 82 0 0 25 0 1 0 1843395308 63651840 14663 4294967295 134512640 135094434 3221224448 3221221648 134677307 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13198/statm): 15540 14663 145 145 0 15395 0
[pid=13198] vsize: 62160
Current children cumulated CPU time (s) 1149.25
Current children cumulated vsize (Kb) 64284

[startup+1160.11 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 13198
Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13194/statm): 531 226 485 147 0 384 0
[pid=13194] vsize: 2124
Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 15019 0 0 0 115843 82 0 0 25 0 1 0 1843395308 63651840 14664 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13198/statm): 15540 14664 145 145 0 15395 0
[pid=13198] vsize: 62160
Current children cumulated CPU time (s) 1159.25
Current children cumulated vsize (Kb) 64284

[startup+1170.11 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 13198
Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13194/statm): 531 226 485 147 0 384 0
[pid=13194] vsize: 2124
Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 15019 0 0 0 116844 82 0 0 25 0 1 0 1843395308 63651840 14664 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13198/statm): 15540 14664 145 145 0 15395 0
[pid=13198] vsize: 62160
Current children cumulated CPU time (s) 1169.26
Current children cumulated vsize (Kb) 64284

[startup+1180.11 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 13198
Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13194/statm): 531 226 485 147 0 384 0
[pid=13194] vsize: 2124
Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 15019 0 0 0 117844 82 0 0 25 0 1 0 1843395308 63651840 14664 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13198/statm): 15540 14664 145 145 0 15395 0
[pid=13198] vsize: 62160
Current children cumulated CPU time (s) 1179.26
Current children cumulated vsize (Kb) 64284

[startup+1190.11 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 13198
Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13194/statm): 531 226 485 147 0 384 0
[pid=13194] vsize: 2124
Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 15019 0 0 0 118844 82 0 0 25 0 1 0 1843395308 63651840 14664 4294967295 134512640 135094434 3221224448 3221223040 134557180 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13198/statm): 15540 14664 145 145 0 15395 0
[pid=13198] vsize: 62160
Current children cumulated CPU time (s) 1189.26
Current children cumulated vsize (Kb) 64284

[startup+1200.11 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 13198
Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13194/statm): 531 226 485 147 0 384 0
[pid=13194] vsize: 2124
Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 15019 0 0 0 119844 82 0 0 25 0 1 0 1843395308 63651840 14664 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13198/statm): 15540 14664 145 145 0 15395 0
[pid=13198] vsize: 62160
Current children cumulated CPU time (s) 1199.26
Current children cumulated vsize (Kb) 64284

[startup+1210.11 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 13198
Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13194/statm): 531 226 485 147 0 384 0
[pid=13194] vsize: 2124
Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 15019 0 0 0 120844 82 0 0 25 0 1 0 1843395308 63651840 14664 4294967295 134512640 135094434 3221224448 3221223072 134562088 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13198/statm): 15540 14664 145 145 0 15395 0
[pid=13198] vsize: 62160
Current children cumulated CPU time (s) 1209.26
Current children cumulated vsize (Kb) 64284



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.11 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 13198
Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13194/statm): 531 226 485 147 0 384 0
[pid=13194] vsize: 2124
Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 15019 0 0 0 120845 82 0 0 25 0 1 0 1843395308 63651840 14664 4294967295 134512640 135094434 3221224448 3221223120 134555413 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13198/statm): 15540 14664 145 145 0 15395 0
[pid=13198] vsize: 62160
Current children cumulated CPU time (s) 1209.27
Current children cumulated vsize (Kb) 64284

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

Child status: 10
Real time (s): 1210.14
CPU time (s): 1209.3
CPU user time (s): 1208.45
CPU system time (s): 0.85087
CPU usage (%): 99.9304
Max. virtual memory (cumulated for all children) (Kb): 64284

Verifier Data

ERROR: no interpretation found !