Some explanations

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

General information on the benchmark

Namemps-v2-13-7/MIPLIB/miplib3/normalized-mps-v2-13-7-p0282.opb
MD5SUM1a8deb577df7e72871b7e1004c098336
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 benchmark50.1794
Number of variables282
Total number of constraints523
Number of constraints which are clauses177
Number of constraints which are cardinality constraints (but not clauses)282
Number of constraints which are nor clauses,nor cardinality constraints64
Minimum length of a constraint1
Maximum length of a constraint57

Trace number 6223

Launcher Data

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

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        907284 kB
Buffers:         18952 kB
Cached:          80984 kB
SwapCached:        840 kB
Active:          27972 kB
Inactive:        74568 kB
HighTotal:      131008 kB
HighFree:        48944 kB
LowTotal:       903652 kB
LowFree:        858340 kB
SwapTotal:     2097136 kB
SwapFree:      2095788 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5668 kB
Slab:            19188 kB
Committed_AS:    64168 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-09-20 04:52:47 (client local time) WITH STATUS 10 IN 1209.25 SECONDS
stats: 3381 7 1209.25 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 ---[ 223]---> Sorter-cost:  850     Base: 5 2 3 3
c ---[ 222]---> Sorter-cost:  712     Base: 5 2 3 3
c ---[ 221]---> Sorter-cost: 1135     Base: 2 5 5
c ---[ 220]---> Sorter-cost:  908     Base: 2 5 5
c ---[ 219]---> Sorter-cost: 1099     Base: 2 5 3 2
c ---[ 218]---> Sorter-cost:  882     Base: 2 5 3 3
c ---[ 217]---> Sorter-cost:  908     Base: 2 5 5
c ---[ 216]---> Sorter-cost:  909     Base: 2 5 5
c ---[ 215]---> Sorter-cost: 1016     Base: 2 5 3
c ---[ 214]---> Sorter-cost:  898     Base: 2 5 3 3
c ---[ 213]---> Sorter-cost: 1146     Base: 2 5 3 3
c ---[ 211]---> Sorter-cost:  996     Base: 2 5 3 3
c ---[ 209]---> Sorter-cost:  943     Base: 2 5 3 3
c ---[ 208]---> Sorter-cost:  760     Base: 2 5 3 3
c ---[ 207]---> Sorter-cost:  769     Base: 5 2 3 3
c ---[ 206]---> Sorter-cost:  713     Base: 5 2 3 3
c ---[ 205]---> Sorter-cost: 1005     Base: 2 5 5
c ---[ 204]---> Sorter-cost:  908     Base: 2 5 5
c ---[ 203]---> Sorter-cost: 1072     Base: 2 5 3
c ---[ 202]---> Sorter-cost:  885     Base: 2 5 3 2
c ---[ 201]---> Sorter-cost:  712     Base: 5 2 3 3
c ---[ 199]---> Sorter-cost:  908     Base: 2 5 5
c ---[ 198]---> Sorter-cost:  909     Base: 2 5 5
c ---[ 197]---> Sorter-cost:  938     Base: 2 5 3 2
c ---[ 196]---> Sorter-cost:  852     Base: 2 5 3 3
c ---[ 195]---> Sorter-cost: 1059     Base: 2 5 3 3
c ---[ 194]---> Sorter-cost:  949     Base: 2 5 3 3
c ---[ 193]---> Sorter-cost:  844     Base: 2 5 3 3
c ---[ 192]---> Sorter-cost:  841     Base: 2 5 3 3
c ---[ 191]---> Sorter-cost: 1081     Base: 2 5 3 3
c ---[ 190]---> Sorter-cost:  996     Base: 2 5 3 2
c ---[ 189]---> Sorter-cost:  995     Base: 2 5 3 3
c ---[ 188]---> Sorter-cost:  985     Base: 2 5 3 2
c ---[ 187]---> BDD-cost:   56
c ---[ 186]---> BDD-cost:   10
c ---[ 185]---> BDD-cost:   56
c ---[ 184]---> BDD-cost:   56
c ---[ 183]---> BDD-cost:   16
c ---[ 182]---> BDD-cost:   26
c ---[ 181]---> BDD-cost:    8
c ---[ 180]---> BDD-cost:    4
c ---[   2]---> Sorter-cost:  678     Base: 2 5 3
c ---[   1]---> Sorter-cost:  694     Base: 2 5 3
c ---[   0]---> BDD-cost:   12
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 ==============================================================================
c Found solution: 881867
c ---[   0]---> Sorter-cost:77310     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 |        94 |  288858   675684 |   96286      88      654     7.4 |  0.000 % |
c |       195 |  288627   675172 |  105914     184     1358     7.4 |  0.198 % |
c |       347 |  288591   675094 |  116506     333     2602     7.8 |  0.208 % |
c |       573 |  288578   675066 |  128156     558     4285     7.7 |  0.212 % |
c ==============================================================================
c Found solution: 798158
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 |       595 |  289292   677295 |   96430     580     4464     7.7 |  0.212 % |
c |       695 |  289229   677156 |  106073     677     5230     7.7 |  0.228 % |
c |       845 |  289229   677156 |  116680     827    11071    13.4 |  0.228 % |
c |      1070 |  289229   677156 |  128348    1052    12272    11.7 |  0.228 % |
c |      1407 |  289229   677156 |  141183    1389    16783    12.1 |  0.228 % |
c |      1913 |  289229   677156 |  155301    1895    22562    11.9 |  0.228 % |
c |      2673 |  289075   676811 |  170831    2651    36393    13.7 |  0.268 % |
c ==============================================================================
c Found solution: 491204
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 |      3485 |  289830   678675 |   96610    3463    53869    15.6 |  0.268 % |
c |      3588 |  289830   678675 |  106271    3566    56114    15.7 |  0.268 % |
c |      3738 |  289830   678675 |  116898    3716    57041    15.4 |  0.268 % |
c |      3964 |  289830   678675 |  128587    3942    58762    14.9 |  0.268 % |
c |      4302 |  289497   677924 |  141446    4259    65556    15.4 |  0.359 % |
c |      4808 |  289486   677901 |  155591    4764    76531    16.1 |  0.362 % |
c |      5570 |  289486   677901 |  171150    5526    92145    16.7 |  0.362 % |
c |      6709 |  289269   677414 |  188265    6660   147337    22.1 |  0.421 % |
c |      8420 |  289226   677317 |  207092    8370   195883    23.4 |  0.433 % |
c |     10982 |  288502   675683 |  227801   10882   251129    23.1 |  0.639 % |
c |     14827 |  288119   674823 |  250581   14713   432249    29.4 |  0.746 % |
c ==============================================================================
c Found solution: 436562
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 |     16547 |  288672   676183 |   96224   16433   539492    32.8 |  0.746 % |
c |     16647 |  288672   676183 |  105846   16533   540183    32.7 |  0.744 % |
c |     16798 |  288672   676183 |  116431   16684   541629    32.5 |  0.744 % |
c |     17024 |  288672   676183 |  128074   16910   550880    32.6 |  0.744 % |
c |     17362 |  288672   676183 |  140881   17248   558318    32.4 |  0.744 % |
c |     17868 |  288672   676183 |  154969   17754   566864    31.9 |  0.744 % |
c |     18629 |  288542   675891 |  170466   18512   573030    31.0 |  0.778 % |
c |     19768 |  288542   675891 |  187513   19651   616919    31.4 |  0.778 % |
c |     21478 |  288517   675836 |  206264   21359   721335    33.8 |  0.785 % |
c ==============================================================================
c Found solution: 435105
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 |     22186 |  288522   676084 |   96174   22015   748548    34.0 |  0.785 % |
c |     22286 |  288522   676084 |  105791   22115   750097    33.9 |  0.886 % |
c |     22437 |  288522   676084 |  116370   22266   750817    33.7 |  0.886 % |
c |     22662 |  288522   676084 |  128007   22491   752052    33.4 |  0.886 % |
c |     22999 |  288522   676084 |  140808   22828   754156    33.0 |  0.886 % |
c |     23505 |  288522   676084 |  154889   23334   777295    33.3 |  0.886 % |
c |     24266 |  288458   675940 |  170378   24094   804215    33.4 |  0.902 % |
c |     25405 |  288430   675876 |  187415   25231   822738    32.6 |  0.910 % |
c |     27116 |  288321   675631 |  206157   26937   846652    31.4 |  0.940 % |
c |     29681 |  288251   675472 |  226773   29492  1007488    34.2 |  0.960 % |
c ==============================================================================
c Found solution: 376947
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 |     31856 |  288251   675561 |   96083   31666  1138561    36.0 |  0.960 % |
c |     31957 |  288251   675561 |  105691   31767  1139909    35.9 |  0.971 % |
c |     32108 |  288251   675561 |  116260   31918  1140918    35.7 |  0.971 % |
c |     32333 |  288145   675322 |  127886   32142  1144235    35.6 |  1.000 % |
c |     32670 |  287939   674860 |  140675   32454  1155638    35.6 |  1.055 % |
c |     33176 |  287939   674860 |  154742   32960  1220439    37.0 |  1.056 % |
c |     33936 |  287939   674860 |  170216   33720  1267260    37.6 |  1.055 % |
c |     35075 |  287807   674558 |  187238   34853  1287014    36.9 |  1.095 % |
c ==============================================================================
c Found solution: 376622
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 |     35698 |  287822   674602 |   95940   35476  1359098    38.3 |  1.095 % |
c |     35798 |  287822   674602 |  105534   35576  1365673    38.4 |  1.096 % |
c |     35949 |  287822   674602 |  116087   35727  1372000    38.4 |  1.096 % |
c |     36174 |  287822   674602 |  127696   35952  1376958    38.3 |  1.096 % |
c |     36512 |  287822   674602 |  140465   36290  1395290    38.4 |  1.096 % |
c ==============================================================================
c Found solution: 354913
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 |     36822 |  287792   674547 |   95930   36599  1404305    38.4 |  1.096 % |
c |     36922 |  287792   674547 |  105523   36699  1405521    38.3 |  1.108 % |
c |     37073 |  287792   674547 |  116075   36850  1406497    38.2 |  1.108 % |
c |     37300 |  287792   674547 |  127682   37077  1420087    38.3 |  1.108 % |
c |     37637 |  287792   674547 |  140451   37414  1438814    38.5 |  1.108 % |
c |     38143 |  287792   674547 |  154496   37920  1448278    38.2 |  1.108 % |
c |     38902 |  287682   674299 |  169945   38677  1480337    38.3 |  1.138 % |
c |     40042 |  287644   674215 |  186940   39816  1638384    41.1 |  1.148 % |
c |     41750 |  287644   674215 |  205634   41524  1686397    40.6 |  1.148 % |
c |     44312 |  287644   674215 |  226197   44086  1953984    44.3 |  1.148 % |
c |     48157 |  287510   673913 |  248817   47929  2297892    47.9 |  1.183 % |
c ==============================================================================
c Found solution: 354908
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 |     48837 |  287329   673517 |   95776   48605  2325753    47.9 |  1.183 % |
c |     48937 |  287329   673517 |  105353   48705  2331070    47.9 |  1.232 % |
c |     49087 |  287329   673517 |  115888   48855  2338335    47.9 |  1.232 % |
c |     49312 |  287325   673508 |  127477   49079  2340723    47.7 |  1.233 % |
c |     49649 |  287289   673426 |  140225   49415  2349449    47.5 |  1.244 % |
c |     50156 |  287289   673426 |  154248   49922  2366434    47.4 |  1.244 % |
c |     50915 |  287289   673426 |  169673   50681  2372878    46.8 |  1.244 % |
c |     52055 |  287289   673426 |  186640   51821  2416696    46.6 |  1.244 % |
c |     53763 |  287265   673372 |  205304   53528  2515819    47.0 |  1.252 % |
c ==============================================================================
c Found solution: 354907
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 |     54985 |  287199   673349 |   95733   54748  2617771    47.8 |  1.252 % |
c |     55087 |  287199   673349 |  105306   54850  2618381    47.7 |  1.274 % |
c |     55238 |  287102   673132 |  115836   54999  2628353    47.8 |  1.302 % |
c |     55463 |  287102   673132 |  127420   55224  2648900    48.0 |  1.302 % |
c |     55800 |  287102   673132 |  140162   55561  2658612    47.9 |  1.302 % |
c |     56308 |  286962   672814 |  154178   56048  2666934    47.6 |  1.342 % |
c |     57068 |  286958   672805 |  169596   56807  2740203    48.2 |  1.343 % |
c |     58207 |  286941   672768 |  186556   57945  2841513    49.0 |  1.348 % |
c |     59916 |  286941   672768 |  205212   59654  2921875    49.0 |  1.348 % |
c |     62478 |  286920   672722 |  225733   62215  3171421    51.0 |  1.354 % |
c ==============================================================================
c Found solution: 354893
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 |     64209 |  286932   672754 |   95644   63946  3295032    51.5 |  1.354 % |
c |     64310 |  286932   672754 |  105208   64047  3295611    51.5 |  1.355 % |
c |     64461 |  286932   672754 |  115729   64198  3303094    51.5 |  1.355 % |
c |     64686 |  286932   672754 |  127302   64423  3312052    51.4 |  1.355 % |
c |     65024 |  286932   672754 |  140032   64761  3314663    51.2 |  1.355 % |
c |     65533 |  286932   672754 |  154035   65270  3354188    51.4 |  1.355 % |
c |     66292 |  286932   672754 |  169439   66029  3386946    51.3 |  1.355 % |
c |     67432 |  286932   672754 |  186383   67169  3429370    51.1 |  1.355 % |
c |     69140 |  286932   672754 |  205021   68877  3498751    50.8 |  1.355 % |
c ==============================================================================
c Found solution: 351999
c ---[   0]---> Sorter-cost:    5     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 |     69370 |  286939   672772 |   95646   69107  3514837    50.9 |  1.355 % |
c |     69470 |  286939   672772 |  105210   69207  3517481    50.8 |  1.356 % |
c ==============================================================================
c Found solution: 325754
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 |     69603 |  286918   672729 |   95639   69339  3525718    50.8 |  1.356 % |
c |     69703 |  286892   672670 |  105202   69438  3526373    50.8 |  1.370 % |
c |     69853 |  286892   672670 |  115723   69588  3547742    51.0 |  1.370 % |
c |     70079 |  286892   672670 |  127295   69814  3569348    51.1 |  1.370 % |
c |     70416 |  286892   672670 |  140025   70151  3584009    51.1 |  1.370 % |
c |     70924 |  286892   672670 |  154027   70659  3654183    51.7 |  1.370 % |
c |     71683 |  286892   672670 |  169430   71418  3667043    51.3 |  1.370 % |
c |     72822 |  286847   672568 |  186373   72554  3696020    50.9 |  1.382 % |
c |     74530 |  286730   672304 |  205010   74256  3740046    50.4 |  1.415 % |
c |     77092 |  286632   672083 |  225511   76816  4009626    52.2 |  1.440 % |
c ==============================================================================
c Found solution: 325267
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 |     79868 |  286603   672024 |   95534   79590  4117132    51.7 |  1.440 % |
c |     79968 |  286505   671805 |  105087   79688  4120996    51.7 |  1.482 % |
c |     80118 |  286505   671805 |  115596   79838  4127671    51.7 |  1.482 % |
c |     80345 |  286505   671805 |  127155   80065  4142188    51.7 |  1.482 % |
c ==============================================================================
c Found solution: 324891
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 |     80640 |  286523   671924 |   95507   80360  4169092    51.9 |  1.482 % |
c |     80740 |  286523   671924 |  105057   80460  4169528    51.8 |  1.483 % |
c |     80890 |  286523   671924 |  115563   80610  4174709    51.8 |  1.483 % |
c |     81115 |  286523   671924 |  127119   80835  4178907    51.7 |  1.483 % |
c |     81452 |  286523   671924 |  139831   81172  4190033    51.6 |  1.483 % |
c |     81958 |  286523   671924 |  153814   81678  4215423    51.6 |  1.483 % |
c |     82717 |  286523   671924 |  169196   82437  4248696    51.5 |  1.483 % |
c |     83856 |  286523   671924 |  186116   83576  4378185    52.4 |  1.483 % |
c |     85565 |  286472   671808 |  204727   85284  4571724    53.6 |  1.496 % |
c |     88129 |  286472   671808 |  225200   87848  4870692    55.4 |  1.496 % |
c |     91973 |  286472   671808 |  247720   91692  5330851    58.1 |  1.496 % |
c ==============================================================================
c Found solution: 324675
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 |     94793 |  286465   671793 |   95488   94511  5591844    59.2 |  1.496 % |
c |     94894 |  286465   671793 |  105036   94612  5592545    59.1 |  1.504 % |
c |     95044 |  286465   671793 |  115540   94762  5594717    59.0 |  1.504 % |
c |     95269 |  286465   671793 |  127094   94987  5596716    58.9 |  1.504 % |
c |     95606 |  286465   671793 |  139803   95324  5616092    58.9 |  1.504 % |
c |     96113 |  286465   671793 |  153784   95831  5651619    59.0 |  1.504 % |
c |     96872 |  286465   671793 |  169162   96590  5684967    58.9 |  1.504 % |
c ==============================================================================
c Found solution: 322839
c ---[   0]---> Sorter-cost:    5     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 |     97234 |  286471   671807 |   95490   96952  5711630    58.9 |  1.504 % |
c |     97334 |  286471   671807 |  105039   97052  5717178    58.9 |  1.505 % |
c |     97484 |  286471   671807 |  115542   97202  5734519    59.0 |  1.505 % |
c |     97709 |  286471   671807 |  127097   97427  5742109    58.9 |  1.505 % |
c |     98046 |  286471   671807 |  139806   97764  5793815    59.3 |  1.505 % |
c |     98554 |  286471   671807 |  153787   98272  5827995    59.3 |  1.505 % |
c |     99315 |  286471   671807 |  169166   99033  5883452    59.4 |  1.505 % |
c |    100454 |  286471   671807 |  186082  100172  5970295    59.6 |  1.505 % |
c |    102162 |  286471   671807 |  204691  101880  6133092    60.2 |  1.505 % |
c ==============================================================================
c Found solution: 322838
c ---[   0]---> Sorter-cost:    4     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 |    102452 |  286404   671657 |   95468  102169  6157887    60.3 |  1.505 % |
c |    102552 |  286404   671657 |  105014   31986  1235638    38.6 |  1.526 % |
c |    102705 |  286404   671657 |  115516   32139  1236710    38.5 |  1.526 % |
c |    102930 |  286404   671657 |  127067   32364  1251376    38.7 |  1.526 % |
c |    103267 |  286404   671657 |  139774   32701  1270087    38.8 |  1.526 % |
c ==============================================================================
c Found solution: 322837
c ---[   0]---> Sorter-cost:    5     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 |    103418 |  286367   671574 |   95455   32851  1280341    39.0 |  1.526 % |
c |    103519 |  286367   671574 |  105000   32952  1293027    39.2 |  1.540 % |
c |    103669 |  286367   671574 |  115500   33102  1300251    39.3 |  1.540 % |
c |    103895 |  286367   671574 |  127050   33328  1319175    39.6 |  1.540 % |
c |    104232 |  286367   671574 |  139755   33665  1337270    39.7 |  1.540 % |
c ==============================================================================
c Found solution: 322815
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 |    104482 |  286377   671676 |   95459   33915  1366281    40.3 |  1.540 % |
c |    104582 |  286377   671676 |  105004   34015  1372203    40.3 |  1.541 % |
c |    104734 |  286377   671676 |  115505   34167  1378933    40.4 |  1.541 % |
c |    104959 |  286377   671676 |  127055   34392  1386271    40.3 |  1.541 % |
c |    105297 |  286377   671676 |  139761   34730  1407505    40.5 |  1.541 % |
c |    105805 |  286377   671676 |  153737   35238  1445714    41.0 |  1.541 % |
c ==============================================================================
c Found solution: 322803
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 |    106109 |  286389   671708 |   95463   35542  1464879    41.2 |  1.541 % |
c |    106209 |  286389   671708 |  105009   35642  1465756    41.1 |  1.542 % |
c |    106359 |  286389   671708 |  115510   35792  1466498    41.0 |  1.542 % |
c |    106585 |  286389   671708 |  127061   36018  1486837    41.3 |  1.542 % |
c |    106923 |  286389   671708 |  139767   36356  1523724    41.9 |  1.542 % |
c |    107429 |  286389   671708 |  153744   36862  1551729    42.1 |  1.542 % |
c |    108189 |  286389   671708 |  169118   37622  1594362    42.4 |  1.542 % |
c |    109329 |  286389   671708 |  186030   38762  1800693    46.5 |  1.542 % |
c |    111038 |  286389   671708 |  204633   40471  1924175    47.5 |  1.542 % |
c ==============================================================================
c Found solution: 322758
c ---[   0]---> Sorter-cost:    8     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 |    111639 |  286398   671731 |   95466   41072  1983502    48.3 |  1.542 % |
c |    111741 |  286398   671731 |  105012   41174  1991568    48.4 |  1.543 % |
c |    111892 |  286398   671731 |  115513   41325  1999481    48.4 |  1.543 % |
c |    112120 |  286398   671731 |  127065   41553  2036891    49.0 |  1.543 % |
c |    112460 |  286392   671717 |  139771   41892  2039196    48.7 |  1.545 % |
c |    112967 |  286249   671395 |  153748   42358  2072777    48.9 |  1.583 % |
c ==============================================================================
c Found solution: 322756
c ---[   0]---> Sorter-cost:    8     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 |    113407 |  286258   671420 |   95419   42798  2163613    50.6 |  1.583 % |
c |    113507 |  286258   671420 |  104960   42898  2164127    50.4 |  1.583 % |
c |    113658 |  286258   671420 |  115456   43049  2168960    50.4 |  1.583 % |
c |    113884 |  286258   671420 |  127002   43275  2185067    50.5 |  1.583 % |
c ==============================================================================
c Found solution: 322749
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 |    114012 |  286267   671443 |   95422   43403  2215288    51.0 |  1.583 % |
c |    114113 |  286267   671443 |  104964   43504  2217181    51.0 |  1.584 % |
c |    114264 |  286237   671377 |  115460   43654  2230119    51.1 |  1.592 % |
c |    114490 |  286237   671377 |  127006   43880  2242532    51.1 |  1.592 % |
c |    114829 |  286237   671377 |  139707   44219  2259868    51.1 |  1.592 % |
c |    115337 |  286233   671369 |  153678   44726  2305115    51.5 |  1.594 % |
c ==============================================================================
c Found solution: 321363
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 |    115687 |  286244   671397 |   95414   45076  2358047    52.3 |  1.594 % |
c |    115787 |  286244   671397 |  104955   45176  2358575    52.2 |  1.595 % |
c |    115938 |  286244   671397 |  115450   45327  2365104    52.2 |  1.595 % |
c ==============================================================================
c Found solution: 321360
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 |    116085 |  286258   671432 |   95419   45474  2385540    52.5 |  1.595 % |
c |    116185 |  286258   671432 |  104960   45574  2387910    52.4 |  1.596 % |
c |    116337 |  286258   671432 |  115456   45726  2399983    52.5 |  1.596 % |
c |    116563 |  286258   671432 |  127002   45952  2434724    53.0 |  1.596 % |
c |    116900 |  286237   671386 |  139702   46288  2472885    53.4 |  1.602 % |
c |    117406 |  286237   671386 |  153673   46794  2485584    53.1 |  1.602 % |
c ==============================================================================
c Found solution: 319923
c ---[   0]---> Sorter-cost:    5     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 |    118136 |  286211   671329 |   95403   47523  2581249    54.3 |  1.602 % |
c |    118237 |  286211   671329 |  104943   47624  2582560    54.2 |  1.612 % |
c |    118389 |  286211   671329 |  115437   47776  2590145    54.2 |  1.612 % |
c |    118614 |  286211   671329 |  126981   48001  2612706    54.4 |  1.612 % |
c |    118956 |  286211   671329 |  139679   48343  2625316    54.3 |  1.612 % |

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/27473/stat): 27473 (minisat+_script) R 27472 27473 5299 0 -1 0 19 0 0 0 0 0 0 0 22 0 1 0 1855693918 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 0 0 0
Raw data (/proc/27473/statm): 174 3 169 147 0 27 0
[pid=27473] 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=27474
New process pid=27475
New process pid=27476
execve syscall for /bin/sed executable
One traced child (pid=27475) 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=27476) exited with status: 0
One traced child (pid=27474) exited with status: 0
New process pid=27477
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc23/normalized-mps-v2-13-7-p0282.opb

[startup+10.0035 s]
Raw data (loadavg): 0.93 0.96 0.96 2/57 27477
Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27473/statm): 531 226 485 147 0 384 0
[pid=27473] vsize: 2124
Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 8650 0 0 0 925 37 0 0 25 0 1 0 1855693923 38129664 8294 4294967295 134512640 135094434 3221224432 3221221616 134600246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27477/statm): 9309 8294 145 145 0 9164 0
[pid=27477] vsize: 37236
Current children cumulated CPU time (s) 9.63
Current children cumulated vsize (Kb) 39360

[startup+20.0042 s]
Raw data (loadavg): 0.94 0.96 0.96 2/57 27477
Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27473/statm): 531 226 485 147 0 384 0
[pid=27473] vsize: 2124
Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 8718 0 0 0 1924 38 0 0 25 0 1 0 1855693923 38379520 8362 4294967295 134512640 135094434 3221224432 3221223120 134554700 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27477/statm): 9370 8362 145 145 0 9225 0
[pid=27477] vsize: 37480
Current children cumulated CPU time (s) 19.63
Current children cumulated vsize (Kb) 39604

[startup+30.0058 s]
Raw data (loadavg): 0.95 0.96 0.96 2/57 27477
Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27473/statm): 531 226 485 147 0 384 0
[pid=27473] vsize: 2124
Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 8791 0 0 0 2922 39 0 0 25 0 1 0 1855693923 38666240 8435 4294967295 134512640 135094434 3221224432 3221223088 134557893 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27477/statm): 9440 8435 145 145 0 9295 0
[pid=27477] vsize: 37760
Current children cumulated CPU time (s) 29.62
Current children cumulated vsize (Kb) 39884

[startup+40.0065 s]
Raw data (loadavg): 0.96 0.96 0.96 2/57 27477
Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27473/statm): 531 226 485 147 0 384 0
[pid=27473] vsize: 2124
Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 8843 0 0 0 3921 40 0 0 25 0 1 0 1855693923 38875136 8487 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27477/statm): 9491 8487 145 145 0 9346 0
[pid=27477] vsize: 37964
Current children cumulated CPU time (s) 39.62
Current children cumulated vsize (Kb) 40088

[startup+50.0081 s]
Raw data (loadavg): 0.96 0.96 0.96 2/57 27477
Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27473/statm): 531 226 485 147 0 384 0
[pid=27473] vsize: 2124
Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 8930 0 0 0 4919 41 0 0 25 0 1 0 1855693923 39251968 8574 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27477/statm): 9583 8574 145 145 0 9438 0
[pid=27477] vsize: 38332
Current children cumulated CPU time (s) 49.61
Current children cumulated vsize (Kb) 40456

[startup+60.0087 s]
Raw data (loadavg): 0.97 0.96 0.96 2/57 27477
Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27473/statm): 531 226 485 147 0 384 0
[pid=27473] vsize: 2124
Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 8965 0 0 0 5918 41 0 0 25 0 1 0 1855693923 39391232 8609 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27477/statm): 9617 8609 145 145 0 9472 0
[pid=27477] vsize: 38468
Current children cumulated CPU time (s) 59.6
Current children cumulated vsize (Kb) 40592

[startup+70.0094 s]
Raw data (loadavg): 0.97 0.96 0.96 2/57 27477
Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27473/statm): 531 226 485 147 0 384 0
[pid=27473] vsize: 2124
Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 9050 0 0 0 6916 42 0 0 25 0 1 0 1855693923 39731200 8694 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27477/statm): 9700 8694 145 145 0 9555 0
[pid=27477] vsize: 38800
Current children cumulated CPU time (s) 69.59
Current children cumulated vsize (Kb) 40924

[startup+80.01 s]
Raw data (loadavg): 0.98 0.96 0.96 2/57 27477
Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27473/statm): 531 226 485 147 0 384 0
[pid=27473] vsize: 2124
Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) T 27473 27473 5299 0 -1 0 9172 0 0 0 7914 43 0 0 25 0 1 0 1855693923 40222720 8816 4294967295 134512640 135094434 3221224432 3221222796 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/27477/statm): 9820 8816 145 145 0 9675 0
[pid=27477] vsize: 39280
Current children cumulated CPU time (s) 79.58
Current children cumulated vsize (Kb) 41404

[startup+90.0106 s]
Raw data (loadavg): 0.98 0.96 0.96 2/57 27477
Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27473/statm): 531 226 485 147 0 384 0
[pid=27473] vsize: 2124
Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 9228 0 0 0 8912 44 0 0 25 0 1 0 1855693923 40448000 8872 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27477/statm): 9875 8872 145 145 0 9730 0
[pid=27477] vsize: 39500
Current children cumulated CPU time (s) 89.57
Current children cumulated vsize (Kb) 41624

[startup+100.011 s]
Raw data (loadavg): 0.98 0.96 0.96 2/57 27477
Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27473/statm): 531 226 485 147 0 384 0
[pid=27473] vsize: 2124
Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 9302 0 0 0 9911 44 0 0 25 0 1 0 1855693923 40738816 8946 4294967295 134512640 135094434 3221224432 3221223076 134558261 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27477/statm): 9946 8946 145 145 0 9801 0
[pid=27477] vsize: 39784
Current children cumulated CPU time (s) 99.56
Current children cumulated vsize (Kb) 41908

[startup+110.012 s]
Raw data (loadavg): 0.98 0.97 0.96 2/57 27477
Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27473/statm): 531 226 485 147 0 384 0
[pid=27473] vsize: 2124
Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 9360 0 0 0 10911 45 0 0 25 0 1 0 1855693923 41025536 9004 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27477/statm): 10016 9004 145 145 0 9871 0
[pid=27477] vsize: 40064
Current children cumulated CPU time (s) 109.57
Current children cumulated vsize (Kb) 42188

[startup+120.013 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 27477
Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27473/statm): 531 226 485 147 0 384 0
[pid=27473] vsize: 2124
Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 9427 0 0 0 11909 45 0 0 25 0 1 0 1855693923 41291776 9071 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27477/statm): 10081 9071 145 145 0 9936 0
[pid=27477] vsize: 40324
Current children cumulated CPU time (s) 119.55
Current children cumulated vsize (Kb) 42448

[startup+130.013 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 27477
Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27473/statm): 531 226 485 147 0 384 0
[pid=27473] vsize: 2124
Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 9508 0 0 0 12909 46 0 0 25 0 1 0 1855693923 41619456 9152 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27477/statm): 10161 9152 145 145 0 10016 0
[pid=27477] vsize: 40644
Current children cumulated CPU time (s) 129.56
Current children cumulated vsize (Kb) 42768

[startup+140.014 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 27477
Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27473/statm): 531 226 485 147 0 384 0
[pid=27473] vsize: 2124
Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 9566 0 0 0 13908 47 0 0 25 0 1 0 1855693923 41852928 9210 4294967295 134512640 135094434 3221224432 3221223088 134557852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27477/statm): 10218 9210 145 145 0 10073 0
[pid=27477] vsize: 40872
Current children cumulated CPU time (s) 139.56
Current children cumulated vsize (Kb) 42996

[startup+150.015 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 27477
Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27473/statm): 531 226 485 147 0 384 0
[pid=27473] vsize: 2124
Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 9623 0 0 0 14907 47 0 0 25 0 1 0 1855693923 42057728 9267 4294967295 134512640 135094434 3221224432 3221223024 134557175 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27477/statm): 10268 9267 145 145 0 10123 0
[pid=27477] vsize: 41072
Current children cumulated CPU time (s) 149.55
Current children cumulated vsize (Kb) 43196

[startup+160.016 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 27477
Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27473/statm): 531 226 485 147 0 384 0
[pid=27473] vsize: 2124
Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) T 27473 27473 5299 0 -1 0 9709 0 0 0 15905 48 0 0 25 0 1 0 1855693923 42397696 9353 4294967295 134512640 135094434 3221224432 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/27477/statm): 10351 9353 145 145 0 10206 0
[pid=27477] vsize: 41404
Current children cumulated CPU time (s) 159.54
Current children cumulated vsize (Kb) 43528

[startup+170.017 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 27477
Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27473/statm): 531 226 485 147 0 384 0
[pid=27473] vsize: 2124
Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 9809 0 0 0 16903 49 0 0 25 0 1 0 1855693923 42799104 9453 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27477/statm): 10449 9453 145 145 0 10304 0
[pid=27477] vsize: 41796
Current children cumulated CPU time (s) 169.53
Current children cumulated vsize (Kb) 43920

[startup+180.018 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 27477
Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27473/statm): 531 226 485 147 0 384 0
[pid=27473] vsize: 2124
Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 9924 0 0 0 17900 50 0 0 25 0 1 0 1855693923 43266048 9568 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27477/statm): 10563 9568 145 145 0 10418 0
[pid=27477] vsize: 42252
Current children cumulated CPU time (s) 179.51
Current children cumulated vsize (Kb) 44376

[startup+190.019 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 27477
Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27473/statm): 531 226 485 147 0 384 0
[pid=27473] vsize: 2124
Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 9987 0 0 0 18899 51 0 0 25 0 1 0 1855693923 43520000 9631 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27477/statm): 10625 9631 145 145 0 10480 0
[pid=27477] vsize: 42500
Current children cumulated CPU time (s) 189.51
Current children cumulated vsize (Kb) 44624

[startup+200.02 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 27477
Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27473/statm): 531 226 485 147 0 384 0
[pid=27473] vsize: 2124
Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 10080 0 0 0 19898 52 0 0 25 0 1 0 1855693923 43888640 9724 4294967295 134512640 135094434 3221224432 3221223088 134557813 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27477/statm): 10715 9724 145 145 0 10570 0
[pid=27477] vsize: 42860
Current children cumulated CPU time (s) 199.51
Current children cumulated vsize (Kb) 44984

[startup+210.02 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 27477
Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27473/statm): 531 226 485 147 0 384 0
[pid=27473] vsize: 2124
Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 10193 0 0 0 20896 52 0 0 25 0 1 0 1855693923 44478464 9837 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27477/statm): 10859 9837 145 145 0 10714 0
[pid=27477] vsize: 43436
Current children cumulated CPU time (s) 209.49
Current children cumulated vsize (Kb) 45560

[startup+220.02 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 27477
Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27473/statm): 531 226 485 147 0 384 0
[pid=27473] vsize: 2124
Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 10221 0 0 0 21896 53 0 0 25 0 1 0 1855693923 44584960 9865 4294967295 134512640 135094434 3221224432 3221223056 134557565 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27477/statm): 10885 9865 145 145 0 10740 0
[pid=27477] vsize: 43540
Current children cumulated CPU time (s) 219.5
Current children cumulated vsize (Kb) 45664

[startup+230.021 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 27477
Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27473/statm): 531 226 485 147 0 384 0
[pid=27473] vsize: 2124
Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 10355 0 0 0 22895 54 0 0 25 0 1 0 1855693923 45240320 9999 4294967295 134512640 135094434 3221224432 3221223252 134558984 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27477/statm): 11045 9999 145 145 0 10900 0
[pid=27477] vsize: 44180
Current children cumulated CPU time (s) 229.5
Current children cumulated vsize (Kb) 46304

[startup+240.021 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 27477
Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27473/statm): 531 226 485 147 0 384 0
[pid=27473] vsize: 2124
Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 10404 0 0 0 23894 54 0 0 25 0 1 0 1855693923 45436928 10048 4294967295 134512640 135094434 3221224432 3221221984 134600314 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27477/statm): 11093 10048 145 145 0 10948 0
[pid=27477] vsize: 44372
Current children cumulated CPU time (s) 239.49
Current children cumulated vsize (Kb) 46496

[startup+250.022 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 27477
Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27473/statm): 531 226 485 147 0 384 0
[pid=27473] vsize: 2124
Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 10426 0 0 0 24893 54 0 0 25 0 1 0 1855693923 45522944 10070 4294967295 134512640 135094434 3221224432 3221223088 134557879 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27477/statm): 11114 10070 145 145 0 10969 0
[pid=27477] vsize: 44456
Current children cumulated CPU time (s) 249.48
Current children cumulated vsize (Kb) 46580

[startup+260.023 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 27477
Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27473/statm): 531 226 485 147 0 384 0
[pid=27473] vsize: 2124
Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 10478 0 0 0 25893 55 0 0 25 0 1 0 1855693923 45731840 10122 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27477/statm): 11165 10122 145 145 0 11020 0
[pid=27477] vsize: 44660
Current children cumulated CPU time (s) 259.49
Current children cumulated vsize (Kb) 46784

[startup+270.023 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 27477
Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27473/statm): 531 226 485 147 0 384 0
[pid=27473] vsize: 2124
Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 10602 0 0 0 26891 55 0 0 25 0 1 0 1855693923 46235648 10246 4294967295 134512640 135094434 3221224432 3221223088 134558395 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27477/statm): 11288 10246 145 145 0 11143 0
[pid=27477] vsize: 45152
Current children cumulated CPU time (s) 269.47
Current children cumulated vsize (Kb) 47276

[startup+280.024 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 27477
Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27473/statm): 531 226 485 147 0 384 0
[pid=27473] vsize: 2124
Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 10707 0 0 0 27889 56 0 0 25 0 1 0 1855693923 46657536 10351 4294967295 134512640 135094434 3221224432 3221223056 134557737 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27477/statm): 11391 10351 145 145 0 11246 0
[pid=27477] vsize: 45564
Current children cumulated CPU time (s) 279.46
Current children cumulated vsize (Kb) 47688

[startup+290.024 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 27477
Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27473/statm): 531 226 485 147 0 384 0
[pid=27473] vsize: 2124
Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 10779 0 0 0 28889 57 0 0 25 0 1 0 1855693923 46948352 10423 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27477/statm): 11462 10423 145 145 0 11317 0
[pid=27477] vsize: 45848
Current children cumulated CPU time (s) 289.47
Current children cumulated vsize (Kb) 47972

[startup+300.026 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 27477
Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27473/statm): 531 226 485 147 0 384 0
[pid=27473] vsize: 2124
Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 10862 0 0 0 29888 57 0 0 25 0 1 0 1855693923 47284224 10506 4294967295 134512640 135094434 3221224432 3221223088 134558210 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27477/statm): 11544 10506 145 145 0 11399 0
[pid=27477] vsize: 46176
Current children cumulated CPU time (s) 299.46
Current children cumulated vsize (Kb) 48300

[startup+310.027 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 27477
Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27473/statm): 531 226 485 147 0 384 0
[pid=27473] vsize: 2124
Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 10942 0 0 0 30887 58 0 0 25 0 1 0 1855693923 47611904 10586 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27477/statm): 11624 10586 145 145 0 11479 0
[pid=27477] vsize: 46496
Current children cumulated CPU time (s) 309.46
Current children cumulated vsize (Kb) 48620

[startup+320.026 s]
Raw data (loadavg): 0.99 0.97 0.96 1/57 27477
Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27473/statm): 531 226 485 147 0 384 0
[pid=27473] vsize: 2124
Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) T 27473 27473 5299 0 -1 0 11033 0 0 0 31885 59 0 0 25 0 1 0 1855693923 47980544 10677 4294967295 134512640 135094434 3221224432 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/27477/statm): 11714 10677 145 145 0 11569 0
[pid=27477] vsize: 46856
Current children cumulated CPU time (s) 319.45
Current children cumulated vsize (Kb) 48980

[startup+330.028 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 27477
Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27473/statm): 531 226 485 147 0 384 0
[pid=27473] vsize: 2124
Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 11139 0 0 0 32884 59 0 0 25 0 1 0 1855693923 48410624 10783 4294967295 134512640 135094434 3221224432 3221223088 134558004 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27477/statm): 11819 10783 145 145 0 11674 0
[pid=27477] vsize: 47276
Current children cumulated CPU time (s) 329.44
Current children cumulated vsize (Kb) 49400

[startup+340.029 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 27477
Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27473/statm): 531 226 485 147 0 384 0
[pid=27473] vsize: 2124
Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 11219 0 0 0 33882 60 0 0 25 0 1 0 1855693923 48734208 10863 4294967295 134512640 135094434 3221224432 3221223072 134562165 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27477/statm): 11898 10863 145 145 0 11753 0
[pid=27477] vsize: 47592
Current children cumulated CPU time (s) 339.43
Current children cumulated vsize (Kb) 49716

[startup+350.029 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 27477
Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27473/statm): 531 226 485 147 0 384 0
[pid=27473] vsize: 2124
Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 11310 0 0 0 34880 62 0 0 25 0 1 0 1855693923 49102848 10954 4294967295 134512640 135094434 3221224432 3221223024 134556851 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27477/statm): 11988 10954 145 145 0 11843 0
[pid=27477] vsize: 47952
Current children cumulated CPU time (s) 349.43
Current children cumulated vsize (Kb) 50076

[startup+360.03 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 27477
Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27473/statm): 531 226 485 147 0 384 0
[pid=27473] vsize: 2124
Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 11363 0 0 0 35878 63 0 0 25 0 1 0 1855693923 49319936 11007 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27477/statm): 12041 11007 145 145 0 11896 0
[pid=27477] vsize: 48164
Current children cumulated CPU time (s) 359.42
Current children cumulated vsize (Kb) 50288

[startup+370.031 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 27477
Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27473/statm): 531 226 485 147 0 384 0
[pid=27473] vsize: 2124
Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 11425 0 0 0 36877 64 0 0 25 0 1 0 1855693923 49569792 11069 4294967295 134512640 135094434 3221224432 3221221984 134677366 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27477/statm): 12102 11069 145 145 0 11957 0
[pid=27477] vsize: 48408
Current children cumulated CPU time (s) 369.42
Current children cumulated vsize (Kb) 50532

[startup+380.031 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 27477
Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27473/statm): 531 226 485 147 0 384 0
[pid=27473] vsize: 2124
Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 11445 0 0 0 37877 64 0 0 25 0 1 0 1855693923 49647616 11089 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27477/statm): 12121 11089 145 145 0 11976 0
[pid=27477] vsize: 48484
Current children cumulated CPU time (s) 379.42
Current children cumulated vsize (Kb) 50608

[startup+390.032 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 27477
Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27473/statm): 531 226 485 147 0 384 0
[pid=27473] vsize: 2124
Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 11556 0 0 0 38874 66 0 0 25 0 1 0 1855693923 50094080 11200 4294967295 134512640 135094434 3221224432 3221223088 134558289 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27477/statm): 12230 11200 145 145 0 12085 0
[pid=27477] vsize: 48920
Current children cumulated CPU time (s) 389.41
Current children cumulated vsize (Kb) 51044

[startup+400.033 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 27477
Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27473/statm): 531 226 485 147 0 384 0
[pid=27473] vsize: 2124
Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 11637 0 0 0 39873 67 0 0 25 0 1 0 1855693923 50421760 11281 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27477/statm): 12310 11281 145 145 0 12165 0
[pid=27477] vsize: 49240
Current children cumulated CPU time (s) 399.41
Current children cumulated vsize (Kb) 51364

[startup+410.033 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 27477
Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27473/statm): 531 226 485 147 0 384 0
[pid=27473] vsize: 2124
Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 11735 0 0 0 40871 68 0 0 25 0 1 0 1855693923 50819072 11379 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27477/statm): 12407 11379 145 145 0 12262 0
[pid=27477] vsize: 49628
Current children cumulated CPU time (s) 409.4
Current children cumulated vsize (Kb) 51752

[startup+420.034 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 27477
Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27473/statm): 531 226 485 147 0 384 0
[pid=27473] vsize: 2124
Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 11773 0 0 0 41871 68 0 0 25 0 1 0 1855693923 50974720 11417 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27477/statm): 12445 11417 145 145 0 12300 0
[pid=27477] vsize: 49780
Current children cumulated CPU time (s) 419.4
Current children cumulated vsize (Kb) 51904

[startup+430.034 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 27477
Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27473/statm): 531 226 485 147 0 384 0
[pid=27473] vsize: 2124
Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 11846 0 0 0 42870 69 0 0 25 0 1 0 1855693923 51265536 11490 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27477/statm): 12516 11490 145 145 0 12371 0
[pid=27477] vsize: 50064
Current children cumulated CPU time (s) 429.4
Current children cumulated vsize (Kb) 52188

[startup+440.035 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 27477
Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27473/statm): 531 226 485 147 0 384 0
[pid=27473] vsize: 2124
Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 11925 0 0 0 43869 70 0 0 25 0 1 0 1855693923 51585024 11569 4294967295 134512640 135094434 3221224432 3221223056 134557565 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27477/statm): 12594 11569 145 145 0 12449 0
[pid=27477] vsize: 50376
Current children cumulated CPU time (s) 439.4
Current children cumulated vsize (Kb) 52500

[startup+450.037 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 27477
Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27473/statm): 531 226 485 147 0 384 0
[pid=27473] vsize: 2124
Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 12002 0 0 0 44867 71 0 0 25 0 1 0 1855693923 51900416 11646 4294967295 134512640 135094434 3221224432 3221223060 134557564 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27477/statm): 12671 11646 145 145 0 12526 0
[pid=27477] vsize: 50684
Current children cumulated CPU time (s) 449.39
Current children cumulated vsize (Kb) 52808

[startup+460.037 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 27477
Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27473/statm): 531 226 485 147 0 384 0
[pid=27473] vsize: 2124
Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 12043 0 0 0 45867 72 0 0 25 0 1 0 1855693923 52064256 11687 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27477/statm): 12711 11687 145 145 0 12566 0
[pid=27477] vsize: 50844
Current children cumulated CPU time (s) 459.4
Current children cumulated vsize (Kb) 52968

[startup+470.037 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 27477
Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27473/statm): 531 226 485 147 0 384 0
[pid=27473] vsize: 2124
Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 12086 0 0 0 46866 72 0 0 25 0 1 0 1855693923 52236288 11730 4294967295 134512640 135094434 3221224432 3221223088 134558395 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27477/statm): 12753 11730 145 145 0 12608 0
[pid=27477] vsize: 51012
Current children cumulated CPU time (s) 469.39
Current children cumulated vsize (Kb) 53136

[startup+480.039 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 27477
Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27473/statm): 531 226 485 147 0 384 0
[pid=27473] vsize: 2124
Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 12154 0 0 0 47865 73 0 0 25 0 1 0 1855693923 52510720 11798 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27477/statm): 12820 11798 145 145 0 12675 0
[pid=27477] vsize: 51280
Current children cumulated CPU time (s) 479.39
Current children cumulated vsize (Kb) 53404

[startup+490.039 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 27477
Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27473/statm): 531 226 485 147 0 384 0
[pid=27473] vsize: 2124
Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 12233 0 0 0 48864 74 0 0 25 0 1 0 1855693923 52834304 11877 4294967295 134512640 135094434 3221224432 3221223104 134555931 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27477/statm): 12899 11877 145 145 0 12754 0
[pid=27477] vsize: 51596
Current children cumulated CPU time (s) 489.39
Current children cumulated vsize (Kb) 53720

[startup+500.04 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 27477
Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27473/statm): 531 226 485 147 0 384 0
[pid=27473] vsize: 2124
Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 12309 0 0 0 49863 75 0 0 25 0 1 0 1855693923 53141504 11953 4294967295 134512640 135094434 3221224432 3221223184 134559282 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27477/statm): 12974 11953 145 145 0 12829 0
[pid=27477] vsize: 51896
Current children cumulated CPU time (s) 499.39
Current children cumulated vsize (Kb) 54020

[startup+510.041 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 27477
Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27473/statm): 531 226 485 147 0 384 0
[pid=27473] vsize: 2124
Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 12379 0 0 0 50861 75 0 0 25 0 1 0 1855693923 53428224 12023 4294967295 134512640 135094434 3221224432 3221223056 134557724 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27477/statm): 13044 12023 145 145 0 12899 0
[pid=27477] vsize: 52176
Current children cumulated CPU time (s) 509.37
Current children cumulated vsize (Kb) 54300

[startup+520.04 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 27477
Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27473/statm): 531 226 485 147 0 384 0
[pid=27473] vsize: 2124
Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 12484 0 0 0 51859 76 0 0 25 0 1 0 1855693923 53850112 12128 4294967295 134512640 135094434 3221224432 3221223044 134563046 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27477/statm): 13147 12128 145 145 0 13002 0
[pid=27477] vsize: 52588
Current children cumulated CPU time (s) 519.36
Current children cumulated vsize (Kb) 54712

[startup+530.041 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 27477
Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27473/statm): 531 226 485 147 0 384 0
[pid=27473] vsize: 2124
Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 12553 0 0 0 52858 77 0 0 25 0 1 0 1855693923 54128640 12197 4294967295 134512640 135094434 3221224432 3221223024 134557037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27477/statm): 13215 12197 145 145 0 13070 0
[pid=27477] vsize: 52860
Current children cumulated CPU time (s) 529.36
Current children cumulated vsize (Kb) 54984

[startup+540.042 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 27477
Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27473/statm): 531 226 485 147 0 384 0
[pid=27473] vsize: 2124
Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 12601 0 0 0 53857 77 0 0 25 0 1 0 1855693923 54583296 12245 4294967295 134512640 135094434 3221224432 3221223088 134558289 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27477/statm): 13326 12245 145 145 0 13181 0
[pid=27477] vsize: 53304
Current children cumulated CPU time (s) 539.35
Current children cumulated vsize (Kb) 55428

[startup+550.043 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 27477
Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27473/statm): 531 226 485 147 0 384 0
[pid=27473] vsize: 2124
Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 12655 0 0 0 54856 78 0 0 25 0 1 0 1855693923 54804480 12299 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27477/statm): 13380 12299 145 145 0 13235 0
[pid=27477] vsize: 53520
Current children cumulated CPU time (s) 549.35
Current children cumulated vsize (Kb) 55644

[startup+560.044 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 27477
Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27473/statm): 531 226 485 147 0 384 0
[pid=27473] vsize: 2124
Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 12697 0 0 0 55856 78 0 0 25 0 1 0 1855693923 54972416 12341 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27477/statm): 13421 12341 145 145 0 13276 0
[pid=27477] vsize: 53684
Current children cumulated CPU time (s) 559.35
Current children cumulated vsize (Kb) 55808

[startup+570.044 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 27477
Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27473/statm): 531 226 485 147 0 384 0
[pid=27473] vsize: 2124
Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 12738 0 0 0 56855 79 0 0 25 0 1 0 1855693923 55136256 12382 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27477/statm): 13461 12382 145 145 0 13316 0
[pid=27477] vsize: 53844
Current children cumulated CPU time (s) 569.35
Current children cumulated vsize (Kb) 55968

[startup+580.045 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 27477
Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27473/statm): 531 226 485 147 0 384 0
[pid=27473] vsize: 2124
Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 12809 0 0 0 57854 79 0 0 25 0 1 0 1855693923 55422976 12453 4294967295 134512640 135094434 3221224432 3221221632 134676539 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27477/statm): 13531 12453 145 145 0 13386 0
[pid=27477] vsize: 54124
Current children cumulated CPU time (s) 579.34
Current children cumulated vsize (Kb) 56248

[startup+590.046 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 27477
Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27473/statm): 531 226 485 147 0 384 0
[pid=27473] vsize: 2124
Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 12840 0 0 0 58853 80 0 0 25 0 1 0 1855693923 55549952 12484 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27477/statm): 13562 12484 145 145 0 13417 0
[pid=27477] vsize: 54248
Current children cumulated CPU time (s) 589.34
Current children cumulated vsize (Kb) 56372

[startup+600.046 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 27477
Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27473/statm): 531 226 485 147 0 384 0
[pid=27473] vsize: 2124
Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 12925 0 0 0 59852 81 0 0 25 0 1 0 1855693923 55889920 12569 4294967295 134512640 135094434 3221224432 3221223120 134554750 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27477/statm): 13645 12569 145 145 0 13500 0
[pid=27477] vsize: 54580
Current children cumulated CPU time (s) 599.34
Current children cumulated vsize (Kb) 56704

[startup+610.047 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 27477
Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27473/statm): 531 226 485 147 0 384 0
[pid=27473] vsize: 2124
Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 13020 0 0 0 60850 81 0 0 25 0 1 0 1855693923 56266752 12664 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27477/statm): 13737 12664 145 145 0 13592 0
[pid=27477] vsize: 54948
Current children cumulated CPU time (s) 609.32
Current children cumulated vsize (Kb) 57072

[startup+620.048 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 27477
Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27473/statm): 531 226 485 147 0 384 0
[pid=27473] vsize: 2124
Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 13091 0 0 0 61849 82 0 0 25 0 1 0 1855693923 56553472 12735 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27477/statm): 13807 12735 145 145 0 13662 0
[pid=27477] vsize: 55228
Current children cumulated CPU time (s) 619.32
Current children cumulated vsize (Kb) 57352

[startup+630.048 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 27477
Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27473/statm): 531 226 485 147 0 384 0
[pid=27473] vsize: 2124
Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 13163 0 0 0 62848 82 0 0 25 0 1 0 1855693923 56844288 12807 4294967295 134512640 135094434 3221224432 3221223056 134562104 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27477/statm): 13878 12807 145 145 0 13733 0
[pid=27477] vsize: 55512
Current children cumulated CPU time (s) 629.31
Current children cumulated vsize (Kb) 57636

[startup+640.049 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 27477
Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27473/statm): 531 226 485 147 0 384 0
[pid=27473] vsize: 2124
Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 13223 0 0 0 63847 82 0 0 25 0 1 0 1855693923 57090048 12867 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27477/statm): 13938 12867 145 145 0 13793 0
[pid=27477] vsize: 55752
Current children cumulated CPU time (s) 639.3
Current children cumulated vsize (Kb) 57876

[startup+650.051 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 27477
Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27473/statm): 531 226 485 147 0 384 0
[pid=27473] vsize: 2124
Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 13300 0 0 0 64846 83 0 0 25 0 1 0 1855693923 57405440 12944 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27477/statm): 14015 12944 145 145 0 13870 0
[pid=27477] vsize: 56060
Current children cumulated CPU time (s) 649.3
Current children cumulated vsize (Kb) 58184

[startup+660.051 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 27477
Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27473/statm): 531 226 485 147 0 384 0
[pid=27473] vsize: 2124
Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 13381 0 0 0 65845 83 0 0 25 0 1 0 1855693923 57729024 13025 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27477/statm): 14094 13025 145 145 0 13949 0
[pid=27477] vsize: 56376
Current children cumulated CPU time (s) 659.29
Current children cumulated vsize (Kb) 58500

[startup+670.052 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 27477
Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27473/statm): 531 226 485 147 0 384 0
[pid=27473] vsize: 2124
Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 13433 0 0 0 66845 84 0 0 25 0 1 0 1855693923 57937920 13077 4294967295 134512640 135094434 3221224432 3221223076 134558261 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27477/statm): 14145 13077 145 145 0 14000 0
[pid=27477] vsize: 56580
Current children cumulated CPU time (s) 669.3
Current children cumulated vsize (Kb) 58704

[startup+680.053 s]
Raw data (loadavg): 1.07 0.99 0.96 2/57 27477
Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27473/statm): 531 226 485 147 0 384 0
[pid=27473] vsize: 2124
Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 13486 0 0 0 67845 84 0 0 25 0 1 0 1855693923 58155008 13130 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27477/statm): 14198 13130 145 145 0 14053 0
[pid=27477] vsize: 56792
Current children cumulated CPU time (s) 679.3
Current children cumulated vsize (Kb) 58916

[startup+690.053 s]
Raw data (loadavg): 1.14 1.00 0.97 2/57 27477
Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27473/statm): 531 226 485 147 0 384 0
[pid=27473] vsize: 2124
Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 13550 0 0 0 68844 85 0 0 25 0 1 0 1855693923 58413056 13194 4294967295 134512640 135094434 3221224432 3221221860 134676608 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27477/statm): 14261 13194 145 145 0 14116 0
[pid=27477] vsize: 57044
Current children cumulated CPU time (s) 689.3
Current children cumulated vsize (Kb) 59168

[startup+700.054 s]
Raw data (loadavg): 1.11 1.00 0.97 2/57 27477
Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27473/statm): 531 226 485 147 0 384 0
[pid=27473] vsize: 2124
Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 13566 0 0 0 69844 85 0 0 25 0 1 0 1855693923 58474496 13210 4294967295 134512640 135094434 3221224432 3221223024 134556817 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27477/statm): 14276 13210 145 145 0 14131 0
[pid=27477] vsize: 57104
Current children cumulated CPU time (s) 699.3
Current children cumulated vsize (Kb) 59228

[startup+710.054 s]
Raw data (loadavg): 1.10 1.00 0.97 2/57 27477
Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27473/statm): 531 226 485 147 0 384 0
[pid=27473] vsize: 2124
Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 13607 0 0 0 70843 85 0 0 25 0 1 0 1855693923 58642432 13251 4294967295 134512640 135094434 3221224432 3221223088 134557866 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27477/statm): 14317 13251 145 145 0 14172 0
[pid=27477] vsize: 57268
Current children cumulated CPU time (s) 709.29
Current children cumulated vsize (Kb) 59392

[startup+720.055 s]
Raw data (loadavg): 1.08 1.00 0.97 2/57 27477
Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27473/statm): 531 226 485 147 0 384 0
[pid=27473] vsize: 2124
Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 13674 0 0 0 71843 86 0 0 25 0 1 0 1855693923 58916864 13318 4294967295 134512640 135094434 3221224432 3221223024 134556964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27477/statm): 14384 13318 145 145 0 14239 0
[pid=27477] vsize: 57536
Current children cumulated CPU time (s) 719.3
Current children cumulated vsize (Kb) 59660

[startup+730.056 s]
Raw data (loadavg): 1.07 1.00 0.97 2/57 27477
Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27473/statm): 531 226 485 147 0 384 0
[pid=27473] vsize: 2124
Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 13757 0 0 0 72842 86 0 0 25 0 1 0 1855693923 59252736 13401 4294967295 134512640 135094434 3221224432 3221223056 134557717 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27477/statm): 14466 13401 145 145 0 14321 0
[pid=27477] vsize: 57864
Current children cumulated CPU time (s) 729.29
Current children cumulated vsize (Kb) 59988

[startup+740.056 s]
Raw data (loadavg): 1.06 1.00 0.97 2/57 27477
Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27473/statm): 531 226 485 147 0 384 0
[pid=27473] vsize: 2124
Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 13821 0 0 0 73841 86 0 0 25 0 1 0 1855693923 59510784 13465 4294967295 134512640 135094434 3221224432 3221223088 134558007 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27477/statm): 14529 13465 145 145 0 14384 0
[pid=27477] vsize: 58116
Current children cumulated CPU time (s) 739.28
Current children cumulated vsize (Kb) 60240

[startup+750.057 s]
Raw data (loadavg): 1.05 1.00 0.97 2/57 27477
Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27473/statm): 531 226 485 147 0 384 0
[pid=27473] vsize: 2124
Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 13891 0 0 0 74841 86 0 0 25 0 1 0 1855693923 59797504 13535 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27477/statm): 14599 13535 145 145 0 14454 0
[pid=27477] vsize: 58396
Current children cumulated CPU time (s) 749.28
Current children cumulated vsize (Kb) 60520

[startup+760.058 s]
Raw data (loadavg): 1.04 1.00 0.97 2/57 27477
Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27473/statm): 531 226 485 147 0 384 0
[pid=27473] vsize: 2124
Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 13971 0 0 0 75839 88 0 0 25 0 1 0 1855693923 60121088 13615 4294967295 134512640 135094434 3221224432 3221223024 134556802 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27477/statm): 14678 13615 145 145 0 14533 0
[pid=27477] vsize: 58712
Current children cumulated CPU time (s) 759.28
Current children cumulated vsize (Kb) 60836

[startup+770.058 s]
Raw data (loadavg): 1.03 1.00 0.97 2/57 27477
Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27473/statm): 531 226 485 147 0 384 0
[pid=27473] vsize: 2124
Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 14052 0 0 0 76837 89 0 0 25 0 1 0 1855693923 60444672 13696 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27477/statm): 14757 13696 145 145 0 14612 0
[pid=27477] vsize: 59028
Current children cumulated CPU time (s) 769.27
Current children cumulated vsize (Kb) 61152

[startup+780.059 s]
Raw data (loadavg): 1.03 1.00 0.97 2/57 27477
Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27473/statm): 531 226 485 147 0 384 0
[pid=27473] vsize: 2124
Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 14132 0 0 0 77836 89 0 0 25 0 1 0 1855693923 60772352 13776 4294967295 134512640 135094434 3221224432 3221223056 134557598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27477/statm): 14837 13776 145 145 0 14692 0
[pid=27477] vsize: 59348
Current children cumulated CPU time (s) 779.26
Current children cumulated vsize (Kb) 61472

[startup+790.06 s]
Raw data (loadavg): 1.02 1.00 0.97 2/57 27477
Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27473/statm): 531 226 485 147 0 384 0
[pid=27473] vsize: 2124
Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 14224 0 0 0 78835 90 0 0 25 0 1 0 1855693923 61145088 13868 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27477/statm): 14928 13868 145 145 0 14783 0
[pid=27477] vsize: 59712
Current children cumulated CPU time (s) 789.26
Current children cumulated vsize (Kb) 61836

[startup+800.061 s]
Raw data (loadavg): 1.02 1.00 0.97 2/57 27477
Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27473/statm): 531 226 485 147 0 384 0
[pid=27473] vsize: 2124
Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 14286 0 0 0 79834 90 0 0 25 0 1 0 1855693923 61399040 13930 4294967295 134512640 135094434 3221224432 3221223056 134562057 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27477/statm): 14990 13930 145 145 0 14845 0
[pid=27477] vsize: 59960
Current children cumulated CPU time (s) 799.25
Current children cumulated vsize (Kb) 62084

[startup+810.062 s]
Raw data (loadavg): 1.02 1.00 0.97 2/57 27477
Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27473/statm): 531 226 485 147 0 384 0
[pid=27473] vsize: 2124
Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 14457 0 0 0 80832 91 0 0 25 0 1 0 1855693923 62095360 14101 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27477/statm): 15160 14101 145 145 0 15015 0
[pid=27477] vsize: 60640
Current children cumulated CPU time (s) 809.24
Current children cumulated vsize (Kb) 62764

[startup+820.062 s]
Raw data (loadavg): 1.01 1.00 0.97 2/57 27477
Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27473/statm): 531 226 485 147 0 384 0
[pid=27473] vsize: 2124
Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 14584 0 0 0 81829 92 0 0 25 0 1 0 1855693923 62611456 14228 4294967295 134512640 135094434 3221224432 3221223104 134555574 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27477/statm): 15286 14228 145 145 0 15141 0
[pid=27477] vsize: 61144
Current children cumulated CPU time (s) 819.22
Current children cumulated vsize (Kb) 63268

[startup+830.063 s]
Raw data (loadavg): 1.01 1.00 0.97 2/57 27477
Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27473/statm): 531 226 485 147 0 384 0
[pid=27473] vsize: 2124
Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 14655 0 0 0 82829 93 0 0 25 0 1 0 1855693923 62902272 14299 4294967295 134512640 135094434 3221224432 3221223024 134557423 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27477/statm): 15357 14299 145 145 0 15212 0
[pid=27477] vsize: 61428
Current children cumulated CPU time (s) 829.23
Current children cumulated vsize (Kb) 63552

[startup+840.064 s]
Raw data (loadavg): 1.01 1.00 0.97 2/57 27477
Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27473/statm): 531 226 485 147 0 384 0
[pid=27473] vsize: 2124
Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 14787 0 0 0 83827 94 0 0 25 0 1 0 1855693923 63447040 14431 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27477/statm): 15490 14431 145 145 0 15345 0
[pid=27477] vsize: 61960
Current children cumulated CPU time (s) 839.22
Current children cumulated vsize (Kb) 64084

[startup+850.065 s]
Raw data (loadavg): 1.01 1.00 0.97 2/57 27477
Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27473/statm): 531 226 485 147 0 384 0
[pid=27473] vsize: 2124
Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 14883 0 0 0 84826 94 0 0 25 0 1 0 1855693923 63848448 14527 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27477/statm): 15588 14527 145 145 0 15443 0
[pid=27477] vsize: 62352
Current children cumulated CPU time (s) 849.21
Current children cumulated vsize (Kb) 64476

[startup+860.066 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 27477
Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27473/statm): 531 226 485 147 0 384 0
[pid=27473] vsize: 2124
Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 15081 0 0 0 85823 95 0 0 25 0 1 0 1855693923 64651264 14725 4294967295 134512640 135094434 3221224432 3221221104 134677307 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27477/statm): 15784 14725 145 145 0 15639 0
[pid=27477] vsize: 63136
Current children cumulated CPU time (s) 859.19
Current children cumulated vsize (Kb) 65260

[startup+870.066 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 27477
Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27473/statm): 531 226 485 147 0 384 0
[pid=27473] vsize: 2124
Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 15098 0 0 0 86823 95 0 0 25 0 1 0 1855693923 64716800 14742 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27477/statm): 15800 14742 145 145 0 15655 0
[pid=27477] vsize: 63200
Current children cumulated CPU time (s) 869.19
Current children cumulated vsize (Kb) 65324

[startup+880.066 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 27477
Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27473/statm): 531 226 485 147 0 384 0
[pid=27473] vsize: 2124
Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 15175 0 0 0 87822 96 0 0 25 0 1 0 1855693923 65048576 14819 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27477/statm): 15881 14819 145 145 0 15736 0
[pid=27477] vsize: 63524
Current children cumulated CPU time (s) 879.19
Current children cumulated vsize (Kb) 65648

[startup+890.067 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 27477
Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27473/statm): 531 226 485 147 0 384 0
[pid=27473] vsize: 2124
Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 15237 0 0 0 88821 96 0 0 25 0 1 0 1855693923 65294336 14881 4294967295 134512640 135094434 3221224432 3221223084 134675707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27477/statm): 15941 14881 145 145 0 15796 0
[pid=27477] vsize: 63764
Current children cumulated CPU time (s) 889.18
Current children cumulated vsize (Kb) 65888

[startup+900.069 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 27477
Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27473/statm): 531 226 485 147 0 384 0
[pid=27473] vsize: 2124
Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 15305 0 0 0 89821 97 0 0 25 0 1 0 1855693923 65572864 14949 4294967295 134512640 135094434 3221224432 3221223024 134557175 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27477/statm): 16009 14949 145 145 0 15864 0
[pid=27477] vsize: 64036
Current children cumulated CPU time (s) 899.19
Current children cumulated vsize (Kb) 66160

[startup+910.069 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 27477
Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27473/statm): 531 226 485 147 0 384 0
[pid=27473] vsize: 2124
Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 15345 0 0 0 90820 97 0 0 25 0 1 0 1855693923 65732608 14989 4294967295 134512640 135094434 3221224432 3221223088 134557893 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27477/statm): 16048 14989 145 145 0 15903 0
[pid=27477] vsize: 64192
Current children cumulated CPU time (s) 909.18
Current children cumulated vsize (Kb) 66316

[startup+920.07 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 27477
Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27473/statm): 531 226 485 147 0 384 0
[pid=27473] vsize: 2124
Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 15411 0 0 0 91819 98 0 0 25 0 1 0 1855693923 66007040 15055 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27477/statm): 16115 15055 145 145 0 15970 0
[pid=27477] vsize: 64460
Current children cumulated CPU time (s) 919.18
Current children cumulated vsize (Kb) 66584

[startup+930.071 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 27477
Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27473/statm): 531 226 485 147 0 384 0
[pid=27473] vsize: 2124
Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 15461 0 0 0 92819 99 0 0 25 0 1 0 1855693923 66215936 15105 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27477/statm): 16166 15105 145 145 0 16021 0
[pid=27477] vsize: 64664
Current children cumulated CPU time (s) 929.19
Current children cumulated vsize (Kb) 66788

[startup+940.071 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 27477
Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27473/statm): 531 226 485 147 0 384 0
[pid=27473] vsize: 2124
Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 15543 0 0 0 93817 99 0 0 25 0 1 0 1855693923 66547712 15187 4294967295 134512640 135094434 3221224432 3221223104 134556327 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27477/statm): 16247 15187 145 145 0 16102 0
[pid=27477] vsize: 64988
Current children cumulated CPU time (s) 939.17
Current children cumulated vsize (Kb) 67112

[startup+950.073 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 27477
Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27473/statm): 531 226 485 147 0 384 0
[pid=27473] vsize: 2124
Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 15618 0 0 0 94814 101 0 0 25 0 1 0 1855693923 66846720 15262 4294967295 134512640 135094434 3221224432 3221223120 134554793 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27477/statm): 16320 15262 145 145 0 16175 0
[pid=27477] vsize: 65280
Current children cumulated CPU time (s) 949.16
Current children cumulated vsize (Kb) 67404

[startup+960.073 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 27477
Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27473/statm): 531 226 485 147 0 384 0
[pid=27473] vsize: 2124
Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 15699 0 0 0 95813 103 0 0 25 0 1 0 1855693923 67178496 15343 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27477/statm): 16401 15343 145 145 0 16256 0
[pid=27477] vsize: 65604
Current children cumulated CPU time (s) 959.17
Current children cumulated vsize (Kb) 67728

[startup+970.074 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 27477
Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27473/statm): 531 226 485 147 0 384 0
[pid=27473] vsize: 2124
Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 15731 0 0 0 96812 103 0 0 25 0 1 0 1855693923 67309568 15375 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27477/statm): 16433 15375 145 145 0 16288 0
[pid=27477] vsize: 65732
Current children cumulated CPU time (s) 969.16
Current children cumulated vsize (Kb) 67856

[startup+980.075 s]
Raw data (loadavg): 1.08 1.02 0.97 3/57 27477
Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27473/statm): 531 226 485 147 0 384 0
[pid=27473] vsize: 2124
Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 15731 0 0 0 97812 103 0 0 25 0 1 0 1855693923 67309568 15375 4294967295 134512640 135094434 3221224432 3221223076 134558261 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27477/statm): 16433 15375 145 145 0 16288 0
[pid=27477] vsize: 65732
Current children cumulated CPU time (s) 979.16
Current children cumulated vsize (Kb) 67856

[startup+990.075 s]
Raw data (loadavg): 1.14 1.03 0.98 2/57 27477
Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27473/statm): 531 226 485 147 0 384 0
[pid=27473] vsize: 2124
Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 15731 0 0 0 98812 104 0 0 25 0 1 0 1855693923 67309568 15375 4294967295 134512640 135094434 3221224432 3221221904 134677007 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27477/statm): 16433 15375 145 145 0 16288 0
[pid=27477] vsize: 65732
Current children cumulated CPU time (s) 989.17
Current children cumulated vsize (Kb) 67856

[startup+1000.08 s]
Raw data (loadavg): 1.12 1.03 0.98 2/57 27477
Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27473/statm): 531 226 485 147 0 384 0
[pid=27473] vsize: 2124
Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 15732 0 0 0 99812 104 0 0 25 0 1 0 1855693923 67309568 15376 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27477/statm): 16433 15376 145 145 0 16288 0
[pid=27477] vsize: 65732
Current children cumulated CPU time (s) 999.17
Current children cumulated vsize (Kb) 67856

[startup+1010.08 s]
Raw data (loadavg): 1.10 1.03 0.98 2/57 27477
Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27473/statm): 531 226 485 147 0 384 0
[pid=27473] vsize: 2124
Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 15732 0 0 0 100812 104 0 0 25 0 1 0 1855693923 67309568 15376 4294967295 134512640 135094434 3221224432 3221223024 134557328 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27477/statm): 16433 15376 145 145 0 16288 0
[pid=27477] vsize: 65732
Current children cumulated CPU time (s) 1009.17
Current children cumulated vsize (Kb) 67856

[startup+1020.08 s]
Raw data (loadavg): 1.08 1.03 0.98 2/57 27477
Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27473/statm): 531 226 485 147 0 384 0
[pid=27473] vsize: 2124
Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 15732 0 0 0 101812 104 0 0 25 0 1 0 1855693923 67309568 15376 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27477/statm): 16433 15376 145 145 0 16288 0
[pid=27477] vsize: 65732
Current children cumulated CPU time (s) 1019.17
Current children cumulated vsize (Kb) 67856

[startup+1030.08 s]
Raw data (loadavg): 1.07 1.03 0.98 2/57 27477
Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27473/statm): 531 226 485 147 0 384 0
[pid=27473] vsize: 2124
Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 15732 0 0 0 102812 105 0 0 25 0 1 0 1855693923 67309568 15376 4294967295 134512640 135094434 3221224432 3221223088 134557882 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27477/statm): 16433 15376 145 145 0 16288 0
[pid=27477] vsize: 65732
Current children cumulated CPU time (s) 1029.18
Current children cumulated vsize (Kb) 67856

[startup+1040.08 s]
Raw data (loadavg): 1.06 1.03 0.98 2/57 27477
Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27473/statm): 531 226 485 147 0 384 0
[pid=27473] vsize: 2124
Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 15732 0 0 0 103812 105 0 0 25 0 1 0 1855693923 67309568 15376 4294967295 134512640 135094434 3221224432 3221223104 134556317 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27477/statm): 16433 15376 145 145 0 16288 0
[pid=27477] vsize: 65732
Current children cumulated CPU time (s) 1039.18
Current children cumulated vsize (Kb) 67856

[startup+1050.08 s]
Raw data (loadavg): 1.05 1.02 0.98 2/57 27477
Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27473/statm): 531 226 485 147 0 384 0
[pid=27473] vsize: 2124
Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 15732 0 0 0 104812 105 0 0 25 0 1 0 1855693923 67309568 15376 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27477/statm): 16433 15376 145 145 0 16288 0
[pid=27477] vsize: 65732
Current children cumulated CPU time (s) 1049.18
Current children cumulated vsize (Kb) 67856

[startup+1060.08 s]
Raw data (loadavg): 1.04 1.02 0.98 2/57 27477
Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27473/statm): 531 226 485 147 0 384 0
[pid=27473] vsize: 2124
Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 15732 0 0 0 105812 105 0 0 25 0 1 0 1855693923 67309568 15376 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27477/statm): 16433 15376 145 145 0 16288 0
[pid=27477] vsize: 65732
Current children cumulated CPU time (s) 1059.18
Current children cumulated vsize (Kb) 67856

[startup+1070.08 s]
Raw data (loadavg): 1.04 1.02 0.98 2/57 27477
Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27473/statm): 531 226 485 147 0 384 0
[pid=27473] vsize: 2124
Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 15732 0 0 0 106812 105 0 0 25 0 1 0 1855693923 67309568 15376 4294967295 134512640 135094434 3221224432 3221223024 134557037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27477/statm): 16433 15376 145 145 0 16288 0
[pid=27477] vsize: 65732
Current children cumulated CPU time (s) 1069.18
Current children cumulated vsize (Kb) 67856

[startup+1080.08 s]
Raw data (loadavg): 1.03 1.02 0.98 2/57 27477
Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27473/statm): 531 226 485 147 0 384 0
[pid=27473] vsize: 2124
Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 15732 0 0 0 107813 105 0 0 25 0 1 0 1855693923 67309568 15376 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27477/statm): 16433 15376 145 145 0 16288 0
[pid=27477] vsize: 65732
Current children cumulated CPU time (s) 1079.19
Current children cumulated vsize (Kb) 67856

[startup+1090.08 s]
Raw data (loadavg): 1.02 1.02 0.98 2/57 27477
Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27473/statm): 531 226 485 147 0 384 0
[pid=27473] vsize: 2124
Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 15732 0 0 0 108812 106 0 0 25 0 1 0 1855693923 67309568 15376 4294967295 134512640 135094434 3221224432 3221223056 134557737 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27477/statm): 16433 15376 145 145 0 16288 0
[pid=27477] vsize: 65732
Current children cumulated CPU time (s) 1089.19
Current children cumulated vsize (Kb) 67856

[startup+1100.08 s]
Raw data (loadavg): 1.02 1.02 0.98 2/57 27477
Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27473/statm): 531 226 485 147 0 384 0
[pid=27473] vsize: 2124
Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 15732 0 0 0 109813 106 0 0 25 0 1 0 1855693923 67309568 15376 4294967295 134512640 135094434 3221224432 3221221688 134676461 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27477/statm): 16433 15376 145 145 0 16288 0
[pid=27477] vsize: 65732
Current children cumulated CPU time (s) 1099.2
Current children cumulated vsize (Kb) 67856

[startup+1110.08 s]
Raw data (loadavg): 1.02 1.02 0.98 2/57 27477
Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27473/statm): 531 226 485 147 0 384 0
[pid=27473] vsize: 2124
Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 15732 0 0 0 110813 106 0 0 25 0 1 0 1855693923 67309568 15376 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27477/statm): 16433 15376 145 145 0 16288 0
[pid=27477] vsize: 65732
Current children cumulated CPU time (s) 1109.2
Current children cumulated vsize (Kb) 67856

[startup+1120.08 s]
Raw data (loadavg): 1.01 1.02 0.98 2/57 27477
Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27473/statm): 531 226 485 147 0 384 0
[pid=27473] vsize: 2124
Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 15734 0 0 0 111813 106 0 0 25 0 1 0 1855693923 67309568 15378 4294967295 134512640 135094434 3221224432 3221223024 134556851 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27477/statm): 16433 15378 145 145 0 16288 0
[pid=27477] vsize: 65732
Current children cumulated CPU time (s) 1119.2
Current children cumulated vsize (Kb) 67856

[startup+1130.08 s]
Raw data (loadavg): 1.01 1.02 0.98 2/57 27477
Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27473/statm): 531 226 485 147 0 384 0
[pid=27473] vsize: 2124
Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 15734 0 0 0 112812 106 0 0 25 0 1 0 1855693923 67309568 15378 4294967295 134512640 135094434 3221224432 3221223104 134556073 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27477/statm): 16433 15378 145 145 0 16288 0
[pid=27477] vsize: 65732
Current children cumulated CPU time (s) 1129.19
Current children cumulated vsize (Kb) 67856

[startup+1140.08 s]
Raw data (loadavg): 1.01 1.02 0.98 2/57 27477
Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27473/statm): 531 226 485 147 0 384 0
[pid=27473] vsize: 2124
Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 15734 0 0 0 113813 106 0 0 25 0 1 0 1855693923 67309568 15378 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27477/statm): 16433 15378 145 145 0 16288 0
[pid=27477] vsize: 65732
Current children cumulated CPU time (s) 1139.2
Current children cumulated vsize (Kb) 67856

[startup+1150.08 s]
Raw data (loadavg): 1.01 1.01 0.98 2/57 27477
Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27473/statm): 531 226 485 147 0 384 0
[pid=27473] vsize: 2124
Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 15734 0 0 0 114813 106 0 0 25 0 1 0 1855693923 67309568 15378 4294967295 134512640 135094434 3221224432 3221223088 134557914 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27477/statm): 16433 15378 145 145 0 16288 0
[pid=27477] vsize: 65732
Current children cumulated CPU time (s) 1149.2
Current children cumulated vsize (Kb) 67856

[startup+1160.08 s]
Raw data (loadavg): 1.01 1.01 0.98 2/57 27477
Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27473/statm): 531 226 485 147 0 384 0
[pid=27473] vsize: 2124
Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 15734 0 0 0 115813 106 0 0 25 0 1 0 1855693923 67309568 15378 4294967295 134512640 135094434 3221224432 3221221708 134677081 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27477/statm): 16433 15378 145 145 0 16288 0
[pid=27477] vsize: 65732
Current children cumulated CPU time (s) 1159.2
Current children cumulated vsize (Kb) 67856

[startup+1170.08 s]
Raw data (loadavg): 1.00 1.01 0.98 2/57 27477
Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27473/statm): 531 226 485 147 0 384 0
[pid=27473] vsize: 2124
Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 15734 0 0 0 116813 107 0 0 25 0 1 0 1855693923 67309568 15378 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27477/statm): 16433 15378 145 145 0 16288 0
[pid=27477] vsize: 65732
Current children cumulated CPU time (s) 1169.21
Current children cumulated vsize (Kb) 67856

[startup+1180.08 s]
Raw data (loadavg): 1.00 1.01 0.98 2/57 27477
Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27473/statm): 531 226 485 147 0 384 0
[pid=27473] vsize: 2124
Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 15734 0 0 0 117813 107 0 0 25 0 1 0 1855693923 67309568 15378 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27477/statm): 16433 15378 145 145 0 16288 0
[pid=27477] vsize: 65732
Current children cumulated CPU time (s) 1179.21
Current children cumulated vsize (Kb) 67856

[startup+1190.08 s]
Raw data (loadavg): 1.00 1.01 0.98 2/57 27477
Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27473/statm): 531 226 485 147 0 384 0
[pid=27473] vsize: 2124
Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 15734 0 0 0 118813 107 0 0 25 0 1 0 1855693923 67309568 15378 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27477/statm): 16433 15378 145 145 0 16288 0
[pid=27477] vsize: 65732
Current children cumulated CPU time (s) 1189.21
Current children cumulated vsize (Kb) 67856

[startup+1200.08 s]
Raw data (loadavg): 1.00 1.01 0.98 2/57 27477
Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27473/statm): 531 226 485 147 0 384 0
[pid=27473] vsize: 2124
Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 15735 0 0 0 119813 107 0 0 25 0 1 0 1855693923 67309568 15379 4294967295 134512640 135094434 3221224432 3221223088 134557900 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27477/statm): 16433 15379 145 145 0 16288 0
[pid=27477] vsize: 65732
Current children cumulated CPU time (s) 1199.21
Current children cumulated vsize (Kb) 67856

[startup+1210.09 s]
Raw data (loadavg): 1.00 1.01 0.98 2/57 27477
Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27473/statm): 531 226 485 147 0 384 0
[pid=27473] vsize: 2124
Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 15735 0 0 0 120814 107 0 0 25 0 1 0 1855693923 67309568 15379 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27477/statm): 16433 15379 145 145 0 16288 0
[pid=27477] vsize: 65732
Current children cumulated CPU time (s) 1209.22
Current children cumulated vsize (Kb) 67856



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.09 s]
Raw data (loadavg): 1.00 1.01 0.98 2/57 27477
Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27473/statm): 531 226 485 147 0 384 0
[pid=27473] vsize: 2124
Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 15735 0 0 0 120814 107 0 0 25 0 1 0 1855693923 67309568 15379 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27477/statm): 16433 15379 145 145 0 16288 0
[pid=27477] vsize: 65732
Current children cumulated CPU time (s) 1209.22
Current children cumulated vsize (Kb) 67856

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

Child status: 10
Real time (s): 1210.12
CPU time (s): 1209.25
CPU user time (s): 1208.14
CPU system time (s): 1.10583
CPU usage (%): 99.928
Max. virtual memory (cumulated for all children) (Kb): 67856

Verifier Data

ERROR: no interpretation found !