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-20-10/MIPLIB/miplib3/normalized-mps-v2-20-10-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.5843
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 4541

Launcher Data

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.242
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:        879824 kB
Buffers:         36816 kB
Cached:          91544 kB
SwapCached:       1044 kB
Active:          64248 kB
Inactive:        66824 kB
HighTotal:      131008 kB
HighFree:        43848 kB
LowTotal:       903652 kB
LowFree:        835976 kB
SwapTotal:     2097136 kB
SwapFree:      2095568 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5664 kB
Slab:            18148 kB
Committed_AS:    64168 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-09-19 18:26:15 (client local time) WITH STATUS 10 IN 1209.26 SECONDS
stats: 2997 7 1209.26 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 % |
c |    119463 |  286211   671329 |  153647   48850  2652967    54.3 |  1.612 % |
c |    120223 |  286211   671329 |  169012   49610  2714939    54.7 |  1.612 % |
c |    121362 |  286211   671329 |  185913   50749  2870613    56.6 |  1.612 % |
c ==============================================================================
c Found solution: 318464
c ---[   0]---> Sorter-cost:    2     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 |    122535 |  286224   671362 |   95408   51922  2972933    57.3 |  1.612 % |
c |    122636 |  286224   671362 |  104948   52023  2978542    57.3 |  1.613 % |
c |    122786 |  286224   671362 |  115443   52173  2987829    57.3 |  1.613 % |

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/15004/stat): 15004 (minisat+_script) R 15003 15004 30740 0 -1 0 19 0 0 0 0 0 0 0 22 0 1 0 1793695849 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 0 0 0
Raw data (/proc/15004/statm): 174 3 169 147 0 27 0
[pid=15004] 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=15005
New process pid=15006
New process pid=15007
execve syscall for /bin/sed executable
One traced child (pid=15006) 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=15007) exited with status: 0
One traced child (pid=15005) exited with status: 0
New process pid=15008
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc9/normalized-mps-v2-20-10-p0282.opb

[startup+10.0033 s]
Raw data (loadavg): 0.93 0.96 0.88 2/57 15008
Raw data (/proc/15004/stat): 15004 (minisat+_script) S 15003 15004 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793695849 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15004/statm): 531 226 485 147 0 384 0
[pid=15004] vsize: 2124
Raw data (/proc/15008/stat): 15008 (minisat+_64-bit) R 15004 15004 30740 0 -1 0 8650 0 0 0 928 34 0 0 25 0 1 0 1793695854 38129664 8294 4294967295 134512640 135094434 3221224432 3221221728 134677138 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15008/statm): 9309 8294 145 145 0 9164 0
[pid=15008] vsize: 37236
Current children cumulated CPU time (s) 9.63
Current children cumulated vsize (Kb) 39360

[startup+20.0051 s]
Raw data (loadavg): 0.94 0.96 0.88 2/57 15008
Raw data (/proc/15004/stat): 15004 (minisat+_script) S 15003 15004 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793695849 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15004/statm): 531 226 485 147 0 384 0
[pid=15004] vsize: 2124
Raw data (/proc/15008/stat): 15008 (minisat+_64-bit) R 15004 15004 30740 0 -1 0 8720 0 0 0 1925 36 0 0 25 0 1 0 1793695854 38387712 8364 4294967295 134512640 135094434 3221224432 3221223088 134561757 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15008/statm): 9372 8364 145 145 0 9227 0
[pid=15008] vsize: 37488
Current children cumulated CPU time (s) 19.62
Current children cumulated vsize (Kb) 39612

[startup+30.0079 s]
Raw data (loadavg): 0.95 0.96 0.88 2/57 15008
Raw data (/proc/15004/stat): 15004 (minisat+_script) S 15003 15004 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793695849 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15004/statm): 531 226 485 147 0 384 0
[pid=15004] vsize: 2124
Raw data (/proc/15008/stat): 15008 (minisat+_64-bit) R 15004 15004 30740 0 -1 0 8795 0 0 0 2923 37 0 0 25 0 1 0 1793695854 38682624 8439 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15008/statm): 9444 8439 145 145 0 9299 0
[pid=15008] vsize: 37776
Current children cumulated CPU time (s) 29.61
Current children cumulated vsize (Kb) 39900

[startup+40.0096 s]
Raw data (loadavg): 0.96 0.96 0.88 2/57 15008
Raw data (/proc/15004/stat): 15004 (minisat+_script) S 15003 15004 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793695849 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15004/statm): 531 226 485 147 0 384 0
[pid=15004] vsize: 2124
Raw data (/proc/15008/stat): 15008 (minisat+_64-bit) R 15004 15004 30740 0 -1 0 8850 0 0 0 3922 38 0 0 25 0 1 0 1793695854 38903808 8494 4294967295 134512640 135094434 3221224432 3221223104 134555260 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15008/statm): 9498 8494 145 145 0 9353 0
[pid=15008] vsize: 37992
Current children cumulated CPU time (s) 39.61
Current children cumulated vsize (Kb) 40116

[startup+50.0104 s]
Raw data (loadavg): 0.96 0.96 0.88 2/57 15008
Raw data (/proc/15004/stat): 15004 (minisat+_script) S 15003 15004 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793695849 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15004/statm): 531 226 485 147 0 384 0
[pid=15004] vsize: 2124
Raw data (/proc/15008/stat): 15008 (minisat+_64-bit) R 15004 15004 30740 0 -1 0 8932 0 0 0 4921 38 0 0 25 0 1 0 1793695854 39260160 8576 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15008/statm): 9585 8576 145 145 0 9440 0
[pid=15008] vsize: 38340
Current children cumulated CPU time (s) 49.6
Current children cumulated vsize (Kb) 40464

[startup+60.0111 s]
Raw data (loadavg): 0.97 0.96 0.88 2/57 15008
Raw data (/proc/15004/stat): 15004 (minisat+_script) S 15003 15004 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793695849 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15004/statm): 531 226 485 147 0 384 0
[pid=15004] vsize: 2124
Raw data (/proc/15008/stat): 15008 (minisat+_64-bit) R 15004 15004 30740 0 -1 0 8975 0 0 0 5921 38 0 0 25 0 1 0 1793695854 39428096 8619 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15008/statm): 9626 8619 145 145 0 9481 0
[pid=15008] vsize: 38504
Current children cumulated CPU time (s) 59.6
Current children cumulated vsize (Kb) 40628

[startup+70.0129 s]
Raw data (loadavg): 0.97 0.96 0.88 2/57 15008
Raw data (/proc/15004/stat): 15004 (minisat+_script) S 15003 15004 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793695849 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15004/statm): 531 226 485 147 0 384 0
[pid=15004] vsize: 2124
Raw data (/proc/15008/stat): 15008 (minisat+_64-bit) R 15004 15004 30740 0 -1 0 9062 0 0 0 6919 39 0 0 25 0 1 0 1793695854 39780352 8706 4294967295 134512640 135094434 3221224432 3221223024 134557002 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15008/statm): 9712 8706 145 145 0 9567 0
[pid=15008] vsize: 38848
Current children cumulated CPU time (s) 69.59
Current children cumulated vsize (Kb) 40972

[startup+80.0137 s]
Raw data (loadavg): 0.98 0.96 0.88 2/57 15008
Raw data (/proc/15004/stat): 15004 (minisat+_script) S 15003 15004 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793695849 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15004/statm): 531 226 485 147 0 384 0
[pid=15004] vsize: 2124
Raw data (/proc/15008/stat): 15008 (minisat+_64-bit) R 15004 15004 30740 0 -1 0 9195 0 0 0 7916 41 0 0 25 0 1 0 1793695854 40312832 8839 4294967295 134512640 135094434 3221224432 3221223088 134557890 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15008/statm): 9842 8839 145 145 0 9697 0
[pid=15008] vsize: 39368
Current children cumulated CPU time (s) 79.58
Current children cumulated vsize (Kb) 41492

[startup+90.0145 s]
Raw data (loadavg): 0.98 0.96 0.89 2/57 15008
Raw data (/proc/15004/stat): 15004 (minisat+_script) S 15003 15004 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793695849 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15004/statm): 531 226 485 147 0 384 0
[pid=15004] vsize: 2124
Raw data (/proc/15008/stat): 15008 (minisat+_64-bit) R 15004 15004 30740 0 -1 0 9257 0 0 0 8915 41 0 0 25 0 1 0 1793695854 40566784 8901 4294967295 134512640 135094434 3221224432 3221223056 134557612 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15008/statm): 9904 8901 145 145 0 9759 0
[pid=15008] vsize: 39616
Current children cumulated CPU time (s) 89.57
Current children cumulated vsize (Kb) 41740

[startup+100.015 s]
Raw data (loadavg): 0.98 0.96 0.89 2/57 15008
Raw data (/proc/15004/stat): 15004 (minisat+_script) S 15003 15004 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793695849 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15004/statm): 531 226 485 147 0 384 0
[pid=15004] vsize: 2124
Raw data (/proc/15008/stat): 15008 (minisat+_64-bit) R 15004 15004 30740 0 -1 0 9320 0 0 0 9914 42 0 0 25 0 1 0 1793695854 40812544 8964 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15008/statm): 9964 8964 145 145 0 9819 0
[pid=15008] vsize: 39856
Current children cumulated CPU time (s) 99.57
Current children cumulated vsize (Kb) 41980

[startup+110.016 s]
Raw data (loadavg): 0.98 0.97 0.89 2/57 15008
Raw data (/proc/15004/stat): 15004 (minisat+_script) S 15003 15004 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793695849 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15004/statm): 531 226 485 147 0 384 0
[pid=15004] vsize: 2124
Raw data (/proc/15008/stat): 15008 (minisat+_64-bit) R 15004 15004 30740 0 -1 0 9373 0 0 0 10913 43 0 0 25 0 1 0 1793695854 41078784 9017 4294967295 134512640 135094434 3221224432 3221223124 134558984 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15008/statm): 10029 9017 145 145 0 9884 0
[pid=15008] vsize: 40116
Current children cumulated CPU time (s) 109.57
Current children cumulated vsize (Kb) 42240

[startup+120.017 s]
Raw data (loadavg): 0.99 0.97 0.89 2/57 15008
Raw data (/proc/15004/stat): 15004 (minisat+_script) S 15003 15004 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793695849 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15004/statm): 531 226 485 147 0 384 0
[pid=15004] vsize: 2124
Raw data (/proc/15008/stat): 15008 (minisat+_64-bit) R 15004 15004 30740 0 -1 0 9453 0 0 0 11912 43 0 0 25 0 1 0 1793695854 41394176 9097 4294967295 134512640 135094434 3221224432 3221223104 134556454 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15008/statm): 10106 9097 145 145 0 9961 0
[pid=15008] vsize: 40424
Current children cumulated CPU time (s) 119.56
Current children cumulated vsize (Kb) 42548

[startup+130.018 s]
Raw data (loadavg): 0.99 0.97 0.89 2/57 15008
Raw data (/proc/15004/stat): 15004 (minisat+_script) S 15003 15004 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793695849 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15004/statm): 531 226 485 147 0 384 0
[pid=15004] vsize: 2124
Raw data (/proc/15008/stat): 15008 (minisat+_64-bit) R 15004 15004 30740 0 -1 0 9541 0 0 0 12911 44 0 0 25 0 1 0 1793695854 41750528 9185 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15008/statm): 10193 9185 145 145 0 10048 0
[pid=15008] vsize: 40772
Current children cumulated CPU time (s) 129.56
Current children cumulated vsize (Kb) 42896

[startup+140.019 s]
Raw data (loadavg): 0.99 0.97 0.89 2/57 15008
Raw data (/proc/15004/stat): 15004 (minisat+_script) S 15003 15004 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793695849 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15004/statm): 531 226 485 147 0 384 0
[pid=15004] vsize: 2124
Raw data (/proc/15008/stat): 15008 (minisat+_64-bit) R 15004 15004 30740 0 -1 0 9614 0 0 0 13909 44 0 0 25 0 1 0 1793695854 42049536 9258 4294967295 134512640 135094434 3221224432 3221222176 134541428 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15008/statm): 10266 9258 145 145 0 10121 0
[pid=15008] vsize: 41064
Current children cumulated CPU time (s) 139.54
Current children cumulated vsize (Kb) 43188

[startup+150.02 s]
Raw data (loadavg): 0.99 0.97 0.89 2/57 15008
Raw data (/proc/15004/stat): 15004 (minisat+_script) S 15003 15004 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793695849 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15004/statm): 531 226 485 147 0 384 0
[pid=15004] vsize: 2124
Raw data (/proc/15008/stat): 15008 (minisat+_64-bit) R 15004 15004 30740 0 -1 0 9659 0 0 0 14909 45 0 0 25 0 1 0 1793695854 42205184 9303 4294967295 134512640 135094434 3221224432 3221223056 134562104 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15008/statm): 10304 9303 145 145 0 10159 0
[pid=15008] vsize: 41216
Current children cumulated CPU time (s) 149.55
Current children cumulated vsize (Kb) 43340

[startup+160.02 s]
Raw data (loadavg): 0.99 0.97 0.89 2/57 15008
Raw data (/proc/15004/stat): 15004 (minisat+_script) S 15003 15004 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793695849 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15004/statm): 531 226 485 147 0 384 0
[pid=15004] vsize: 2124
Raw data (/proc/15008/stat): 15008 (minisat+_64-bit) R 15004 15004 30740 0 -1 0 9761 0 0 0 15907 45 0 0 25 0 1 0 1793695854 42602496 9405 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15008/statm): 10401 9405 145 145 0 10256 0
[pid=15008] vsize: 41604
Current children cumulated CPU time (s) 159.53
Current children cumulated vsize (Kb) 43728

[startup+170.021 s]
Raw data (loadavg): 0.99 0.97 0.89 2/57 15008
Raw data (/proc/15004/stat): 15004 (minisat+_script) S 15003 15004 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793695849 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15004/statm): 531 226 485 147 0 384 0
[pid=15004] vsize: 2124
Raw data (/proc/15008/stat): 15008 (minisat+_64-bit) R 15004 15004 30740 0 -1 0 9896 0 0 0 16903 47 0 0 25 0 1 0 1793695854 43151360 9540 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15008/statm): 10535 9540 145 145 0 10390 0
[pid=15008] vsize: 42140
Current children cumulated CPU time (s) 169.51
Current children cumulated vsize (Kb) 44264

[startup+180.022 s]
Raw data (loadavg): 0.99 0.97 0.89 2/57 15008
Raw data (/proc/15004/stat): 15004 (minisat+_script) S 15003 15004 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793695849 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15004/statm): 531 226 485 147 0 384 0
[pid=15004] vsize: 2124
Raw data (/proc/15008/stat): 15008 (minisat+_64-bit) R 15004 15004 30740 0 -1 0 9964 0 0 0 17902 48 0 0 25 0 1 0 1793695854 43425792 9608 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15008/statm): 10602 9608 145 145 0 10457 0
[pid=15008] vsize: 42408
Current children cumulated CPU time (s) 179.51
Current children cumulated vsize (Kb) 44532

[startup+190.022 s]
Raw data (loadavg): 0.99 0.97 0.90 2/57 15008
Raw data (/proc/15004/stat): 15004 (minisat+_script) S 15003 15004 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793695849 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15004/statm): 531 226 485 147 0 384 0
[pid=15004] vsize: 2124
Raw data (/proc/15008/stat): 15008 (minisat+_64-bit) R 15004 15004 30740 0 -1 0 10080 0 0 0 18901 48 0 0 25 0 1 0 1793695854 43888640 9724 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15008/statm): 10715 9724 145 145 0 10570 0
[pid=15008] vsize: 42860
Current children cumulated CPU time (s) 189.5
Current children cumulated vsize (Kb) 44984

[startup+200.023 s]
Raw data (loadavg): 0.99 0.97 0.90 2/57 15008
Raw data (/proc/15004/stat): 15004 (minisat+_script) S 15003 15004 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793695849 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15004/statm): 531 226 485 147 0 384 0
[pid=15004] vsize: 2124
Raw data (/proc/15008/stat): 15008 (minisat+_64-bit) R 15004 15004 30740 0 -1 0 10153 0 0 0 19900 49 0 0 25 0 1 0 1793695854 44314624 9797 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15008/statm): 10819 9797 145 145 0 10674 0
[pid=15008] vsize: 43276
Current children cumulated CPU time (s) 199.5
Current children cumulated vsize (Kb) 45400

[startup+210.024 s]
Raw data (loadavg): 0.99 0.97 0.90 2/57 15008
Raw data (/proc/15004/stat): 15004 (minisat+_script) S 15003 15004 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793695849 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15004/statm): 531 226 485 147 0 384 0
[pid=15004] vsize: 2124
Raw data (/proc/15008/stat): 15008 (minisat+_64-bit) R 15004 15004 30740 0 -1 0 10216 0 0 0 20898 49 0 0 25 0 1 0 1793695854 44568576 9860 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15008/statm): 10881 9860 145 145 0 10736 0
[pid=15008] vsize: 43524
Current children cumulated CPU time (s) 209.48
Current children cumulated vsize (Kb) 45648

[startup+220.025 s]
Raw data (loadavg): 0.99 0.97 0.90 2/57 15008
Raw data (/proc/15004/stat): 15004 (minisat+_script) S 15003 15004 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793695849 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15004/statm): 531 226 485 147 0 384 0
[pid=15004] vsize: 2124
Raw data (/proc/15008/stat): 15008 (minisat+_64-bit) R 15004 15004 30740 0 -1 0 10353 0 0 0 21897 50 0 0 25 0 1 0 1793695854 45240320 9997 4294967295 134512640 135094434 3221224432 3221221904 134676311 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15008/statm): 11045 9997 145 145 0 10900 0
[pid=15008] vsize: 44180
Current children cumulated CPU time (s) 219.48
Current children cumulated vsize (Kb) 46304

[startup+230.025 s]
Raw data (loadavg): 0.99 0.97 0.90 2/57 15008
Raw data (/proc/15004/stat): 15004 (minisat+_script) S 15003 15004 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793695849 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15004/statm): 531 226 485 147 0 384 0
[pid=15004] vsize: 2124
Raw data (/proc/15008/stat): 15008 (minisat+_64-bit) R 15004 15004 30740 0 -1 0 10372 0 0 0 22897 50 0 0 25 0 1 0 1793695854 45305856 10016 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15008/statm): 11061 10016 145 145 0 10916 0
[pid=15008] vsize: 44244
Current children cumulated CPU time (s) 229.48
Current children cumulated vsize (Kb) 46368

[startup+240.026 s]
Raw data (loadavg): 0.99 0.97 0.90 2/57 15008
Raw data (/proc/15004/stat): 15004 (minisat+_script) S 15003 15004 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793695849 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15004/statm): 531 226 485 147 0 384 0
[pid=15004] vsize: 2124
Raw data (/proc/15008/stat): 15008 (minisat+_64-bit) R 15004 15004 30740 0 -1 0 10422 0 0 0 23897 51 0 0 25 0 1 0 1793695854 45506560 10066 4294967295 134512640 135094434 3221224432 3221223088 134558286 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15008/statm): 11110 10066 145 145 0 10965 0
[pid=15008] vsize: 44440
Current children cumulated CPU time (s) 239.49
Current children cumulated vsize (Kb) 46564

[startup+250.027 s]
Raw data (loadavg): 0.99 0.97 0.90 2/57 15008
Raw data (/proc/15004/stat): 15004 (minisat+_script) S 15003 15004 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793695849 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15004/statm): 531 226 485 147 0 384 0
[pid=15004] vsize: 2124
Raw data (/proc/15008/stat): 15008 (minisat+_64-bit) R 15004 15004 30740 0 -1 0 10475 0 0 0 24896 52 0 0 25 0 1 0 1793695854 45719552 10119 4294967295 134512640 135094434 3221224432 3221223056 134562088 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15008/statm): 11162 10119 145 145 0 11017 0
[pid=15008] vsize: 44648
Current children cumulated CPU time (s) 249.49
Current children cumulated vsize (Kb) 46772

[startup+260.028 s]
Raw data (loadavg): 0.99 0.97 0.90 2/57 15008
Raw data (/proc/15004/stat): 15004 (minisat+_script) S 15003 15004 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793695849 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15004/statm): 531 226 485 147 0 384 0
[pid=15004] vsize: 2124
Raw data (/proc/15008/stat): 15008 (minisat+_64-bit) R 15004 15004 30740 0 -1 0 10605 0 0 0 25894 53 0 0 25 0 1 0 1793695854 46247936 10249 4294967295 134512640 135094434 3221224432 3221223024 134556843 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15008/statm): 11291 10249 145 145 0 11146 0
[pid=15008] vsize: 45164
Current children cumulated CPU time (s) 259.48
Current children cumulated vsize (Kb) 47288

[startup+270.028 s]
Raw data (loadavg): 0.99 0.97 0.90 2/57 15008
Raw data (/proc/15004/stat): 15004 (minisat+_script) S 15003 15004 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793695849 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15004/statm): 531 226 485 147 0 384 0
[pid=15004] vsize: 2124
Raw data (/proc/15008/stat): 15008 (minisat+_64-bit) R 15004 15004 30740 0 -1 0 10709 0 0 0 26892 54 0 0 25 0 1 0 1793695854 46665728 10353 4294967295 134512640 135094434 3221224432 3221223024 134556851 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15008/statm): 11393 10353 145 145 0 11248 0
[pid=15008] vsize: 45572
Current children cumulated CPU time (s) 269.47
Current children cumulated vsize (Kb) 47696

[startup+280.029 s]
Raw data (loadavg): 0.99 0.97 0.90 2/57 15008
Raw data (/proc/15004/stat): 15004 (minisat+_script) S 15003 15004 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793695849 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15004/statm): 531 226 485 147 0 384 0
[pid=15004] vsize: 2124
Raw data (/proc/15008/stat): 15008 (minisat+_64-bit) R 15004 15004 30740 0 -1 0 10781 0 0 0 27892 54 0 0 25 0 1 0 1793695854 46956544 10425 4294967295 134512640 135094434 3221224432 3221223056 134557681 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15008/statm): 11464 10425 145 145 0 11319 0
[pid=15008] vsize: 45856
Current children cumulated CPU time (s) 279.47
Current children cumulated vsize (Kb) 47980

[startup+290.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15008
Raw data (/proc/15004/stat): 15004 (minisat+_script) S 15003 15004 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793695849 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15004/statm): 531 226 485 147 0 384 0
[pid=15004] vsize: 2124
Raw data (/proc/15008/stat): 15008 (minisat+_64-bit) R 15004 15004 30740 0 -1 0 10870 0 0 0 28891 54 0 0 25 0 1 0 1793695854 47316992 10514 4294967295 134512640 135094434 3221224432 3221223104 134555574 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15008/statm): 11552 10514 145 145 0 11407 0
[pid=15008] vsize: 46208
Current children cumulated CPU time (s) 289.46
Current children cumulated vsize (Kb) 48332

[startup+300.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15008
Raw data (/proc/15004/stat): 15004 (minisat+_script) S 15003 15004 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793695849 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15004/statm): 531 226 485 147 0 384 0
[pid=15004] vsize: 2124
Raw data (/proc/15008/stat): 15008 (minisat+_64-bit) R 15004 15004 30740 0 -1 0 10947 0 0 0 29889 55 0 0 25 0 1 0 1793695854 47632384 10591 4294967295 134512640 135094434 3221224432 3221223088 134558395 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15008/statm): 11629 10591 145 145 0 11484 0
[pid=15008] vsize: 46516
Current children cumulated CPU time (s) 299.45
Current children cumulated vsize (Kb) 48640

[startup+310.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15008
Raw data (/proc/15004/stat): 15004 (minisat+_script) S 15003 15004 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793695849 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15004/statm): 531 226 485 147 0 384 0
[pid=15004] vsize: 2124
Raw data (/proc/15008/stat): 15008 (minisat+_64-bit) R 15004 15004 30740 0 -1 0 11062 0 0 0 30887 56 0 0 25 0 1 0 1793695854 48099328 10706 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15008/statm): 11743 10706 145 145 0 11598 0
[pid=15008] vsize: 46972
Current children cumulated CPU time (s) 309.44
Current children cumulated vsize (Kb) 49096

[startup+320.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15008
Raw data (/proc/15004/stat): 15004 (minisat+_script) S 15003 15004 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793695849 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15004/statm): 531 226 485 147 0 384 0
[pid=15004] vsize: 2124
Raw data (/proc/15008/stat): 15008 (minisat+_64-bit) R 15004 15004 30740 0 -1 0 11153 0 0 0 31885 56 0 0 25 0 1 0 1793695854 48467968 10797 4294967295 134512640 135094434 3221224432 3221223088 134557920 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15008/statm): 11833 10797 145 145 0 11688 0
[pid=15008] vsize: 47332
Current children cumulated CPU time (s) 319.42
Current children cumulated vsize (Kb) 49456

[startup+330.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15008
Raw data (/proc/15004/stat): 15004 (minisat+_script) S 15003 15004 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793695849 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15004/statm): 531 226 485 147 0 384 0
[pid=15004] vsize: 2124
Raw data (/proc/15008/stat): 15008 (minisat+_64-bit) R 15004 15004 30740 0 -1 0 11246 0 0 0 32884 57 0 0 25 0 1 0 1793695854 48844800 10890 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15008/statm): 11925 10890 145 145 0 11780 0
[pid=15008] vsize: 47700
Current children cumulated CPU time (s) 329.42
Current children cumulated vsize (Kb) 49824

[startup+340.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15008
Raw data (/proc/15004/stat): 15004 (minisat+_script) S 15003 15004 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793695849 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15004/statm): 531 226 485 147 0 384 0
[pid=15004] vsize: 2124
Raw data (/proc/15008/stat): 15008 (minisat+_64-bit) R 15004 15004 30740 0 -1 0 11334 0 0 0 33882 58 0 0 25 0 1 0 1793695854 49201152 10978 4294967295 134512640 135094434 3221224432 3221223120 134554796 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15008/statm): 12012 10978 145 145 0 11867 0
[pid=15008] vsize: 48048
Current children cumulated CPU time (s) 339.41
Current children cumulated vsize (Kb) 50172

[startup+350.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15008
Raw data (/proc/15004/stat): 15004 (minisat+_script) S 15003 15004 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793695849 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15004/statm): 531 226 485 147 0 384 0
[pid=15004] vsize: 2124
Raw data (/proc/15008/stat): 15008 (minisat+_64-bit) R 15004 15004 30740 0 -1 0 11377 0 0 0 34882 58 0 0 25 0 1 0 1793695854 49373184 11021 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15008/statm): 12054 11021 145 145 0 11909 0
[pid=15008] vsize: 48216
Current children cumulated CPU time (s) 349.41
Current children cumulated vsize (Kb) 50340

[startup+360.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15008
Raw data (/proc/15004/stat): 15004 (minisat+_script) S 15003 15004 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793695849 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15004/statm): 531 226 485 147 0 384 0
[pid=15004] vsize: 2124
Raw data (/proc/15008/stat): 15008 (minisat+_64-bit) R 15004 15004 30740 0 -1 0 11425 0 0 0 35881 58 0 0 25 0 1 0 1793695854 49569792 11069 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15008/statm): 12102 11069 145 145 0 11957 0
[pid=15008] vsize: 48408
Current children cumulated CPU time (s) 359.4
Current children cumulated vsize (Kb) 50532

[startup+370.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15008
Raw data (/proc/15004/stat): 15004 (minisat+_script) S 15003 15004 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793695849 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15004/statm): 531 226 485 147 0 384 0
[pid=15004] vsize: 2124
Raw data (/proc/15008/stat): 15008 (minisat+_64-bit) R 15004 15004 30740 0 -1 0 11504 0 0 0 36880 59 0 0 25 0 1 0 1793695854 49881088 11148 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15008/statm): 12178 11148 145 145 0 12033 0
[pid=15008] vsize: 48712
Current children cumulated CPU time (s) 369.4
Current children cumulated vsize (Kb) 50836

[startup+380.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15008
Raw data (/proc/15004/stat): 15004 (minisat+_script) S 15003 15004 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793695849 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15004/statm): 531 226 485 147 0 384 0
[pid=15004] vsize: 2124
Raw data (/proc/15008/stat): 15008 (minisat+_64-bit) R 15004 15004 30740 0 -1 0 11592 0 0 0 37879 60 0 0 25 0 1 0 1793695854 50241536 11236 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15008/statm): 12266 11236 145 145 0 12121 0
[pid=15008] vsize: 49064
Current children cumulated CPU time (s) 379.4
Current children cumulated vsize (Kb) 51188

[startup+390.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15008
Raw data (/proc/15004/stat): 15004 (minisat+_script) S 15003 15004 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793695849 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15004/statm): 531 226 485 147 0 384 0
[pid=15004] vsize: 2124
Raw data (/proc/15008/stat): 15008 (minisat+_64-bit) R 15004 15004 30740 0 -1 0 11668 0 0 0 38878 60 0 0 25 0 1 0 1793695854 50548736 11312 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15008/statm): 12341 11312 145 145 0 12196 0
[pid=15008] vsize: 49364
Current children cumulated CPU time (s) 389.39
Current children cumulated vsize (Kb) 51488

[startup+400.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15008
Raw data (/proc/15004/stat): 15004 (minisat+_script) S 15003 15004 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793695849 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15004/statm): 531 226 485 147 0 384 0
[pid=15004] vsize: 2124
Raw data (/proc/15008/stat): 15008 (minisat+_64-bit) R 15004 15004 30740 0 -1 0 11764 0 0 0 39877 60 0 0 25 0 1 0 1793695854 50937856 11408 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15008/statm): 12436 11408 145 145 0 12291 0
[pid=15008] vsize: 49744
Current children cumulated CPU time (s) 399.38
Current children cumulated vsize (Kb) 51868

[startup+410.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15008
Raw data (/proc/15004/stat): 15004 (minisat+_script) S 15003 15004 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793695849 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15004/statm): 531 226 485 147 0 384 0
[pid=15004] vsize: 2124
Raw data (/proc/15008/stat): 15008 (minisat+_64-bit) R 15004 15004 30740 0 -1 0 11808 0 0 0 40877 61 0 0 25 0 1 0 1793695854 51109888 11452 4294967295 134512640 135094434 3221224432 3221223088 134558221 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15008/statm): 12478 11452 145 145 0 12333 0
[pid=15008] vsize: 49912
Current children cumulated CPU time (s) 409.39
Current children cumulated vsize (Kb) 52036

[startup+420.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15008
Raw data (/proc/15004/stat): 15004 (minisat+_script) S 15003 15004 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793695849 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15004/statm): 531 226 485 147 0 384 0
[pid=15004] vsize: 2124
Raw data (/proc/15008/stat): 15008 (minisat+_64-bit) R 15004 15004 30740 0 -1 0 11905 0 0 0 41876 61 0 0 25 0 1 0 1793695854 51507200 11549 4294967295 134512640 135094434 3221224432 3221223104 134555940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15008/statm): 12575 11549 145 145 0 12430 0
[pid=15008] vsize: 50300
Current children cumulated CPU time (s) 419.38
Current children cumulated vsize (Kb) 52424

[startup+430.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15008
Raw data (/proc/15004/stat): 15004 (minisat+_script) S 15003 15004 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793695849 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15004/statm): 531 226 485 147 0 384 0
[pid=15004] vsize: 2124
Raw data (/proc/15008/stat): 15008 (minisat+_64-bit) R 15004 15004 30740 0 -1 0 11992 0 0 0 42874 62 0 0 25 0 1 0 1793695854 51859456 11636 4294967295 134512640 135094434 3221224432 3221223024 134556987 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15008/statm): 12661 11636 145 145 0 12516 0
[pid=15008] vsize: 50644
Current children cumulated CPU time (s) 429.37
Current children cumulated vsize (Kb) 52768

[startup+440.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15008
Raw data (/proc/15004/stat): 15004 (minisat+_script) S 15003 15004 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793695849 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15004/statm): 531 226 485 147 0 384 0
[pid=15004] vsize: 2124
Raw data (/proc/15008/stat): 15008 (minisat+_64-bit) R 15004 15004 30740 0 -1 0 12036 0 0 0 43874 62 0 0 25 0 1 0 1793695854 52035584 11680 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15008/statm): 12704 11680 145 145 0 12559 0
[pid=15008] vsize: 50816
Current children cumulated CPU time (s) 439.37
Current children cumulated vsize (Kb) 52940

[startup+450.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15008
Raw data (/proc/15004/stat): 15004 (minisat+_script) S 15003 15004 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793695849 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15004/statm): 531 226 485 147 0 384 0
[pid=15004] vsize: 2124
Raw data (/proc/15008/stat): 15008 (minisat+_64-bit) R 15004 15004 30740 0 -1 0 12079 0 0 0 44873 63 0 0 25 0 1 0 1793695854 52207616 11723 4294967295 134512640 135094434 3221224432 3221223088 134558019 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15008/statm): 12746 11723 145 145 0 12601 0
[pid=15008] vsize: 50984
Current children cumulated CPU time (s) 449.37
Current children cumulated vsize (Kb) 53108

[startup+460.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15008
Raw data (/proc/15004/stat): 15004 (minisat+_script) S 15003 15004 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793695849 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15004/statm): 531 226 485 147 0 384 0
[pid=15004] vsize: 2124
Raw data (/proc/15008/stat): 15008 (minisat+_64-bit) R 15004 15004 30740 0 -1 0 12146 0 0 0 45872 63 0 0 25 0 1 0 1793695854 52482048 11790 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15008/statm): 12813 11790 145 145 0 12668 0
[pid=15008] vsize: 51252
Current children cumulated CPU time (s) 459.36
Current children cumulated vsize (Kb) 53376

[startup+470.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15008
Raw data (/proc/15004/stat): 15004 (minisat+_script) S 15003 15004 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793695849 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15004/statm): 531 226 485 147 0 384 0
[pid=15004] vsize: 2124
Raw data (/proc/15008/stat): 15008 (minisat+_64-bit) R 15004 15004 30740 0 -1 0 12228 0 0 0 46871 64 0 0 25 0 1 0 1793695854 52813824 11872 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15008/statm): 12894 11872 145 145 0 12749 0
[pid=15008] vsize: 51576
Current children cumulated CPU time (s) 469.36
Current children cumulated vsize (Kb) 53700

[startup+480.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15008
Raw data (/proc/15004/stat): 15004 (minisat+_script) S 15003 15004 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793695849 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15004/statm): 531 226 485 147 0 384 0
[pid=15004] vsize: 2124
Raw data (/proc/15008/stat): 15008 (minisat+_64-bit) R 15004 15004 30740 0 -1 0 12309 0 0 0 47870 65 0 0 25 0 1 0 1793695854 53141504 11953 4294967295 134512640 135094434 3221224432 3221223024 134556806 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15008/statm): 12974 11953 145 145 0 12829 0
[pid=15008] vsize: 51896
Current children cumulated CPU time (s) 479.36
Current children cumulated vsize (Kb) 54020

[startup+490.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15008
Raw data (/proc/15004/stat): 15004 (minisat+_script) S 15003 15004 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793695849 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15004/statm): 531 226 485 147 0 384 0
[pid=15004] vsize: 2124
Raw data (/proc/15008/stat): 15008 (minisat+_64-bit) R 15004 15004 30740 0 -1 0 12379 0 0 0 48869 65 0 0 25 0 1 0 1793695854 53428224 12023 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15008/statm): 13044 12023 145 145 0 12899 0
[pid=15008] vsize: 52176
Current children cumulated CPU time (s) 489.35
Current children cumulated vsize (Kb) 54300

[startup+500.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15008
Raw data (/proc/15004/stat): 15004 (minisat+_script) S 15003 15004 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793695849 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15004/statm): 531 226 485 147 0 384 0
[pid=15004] vsize: 2124
Raw data (/proc/15008/stat): 15008 (minisat+_64-bit) R 15004 15004 30740 0 -1 0 12515 0 0 0 49868 66 0 0 25 0 1 0 1793695854 53977088 12159 4294967295 134512640 135094434 3221224432 3221221728 134676280 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15008/statm): 13178 12159 145 145 0 13033 0
[pid=15008] vsize: 52712
Current children cumulated CPU time (s) 499.35
Current children cumulated vsize (Kb) 54836

[startup+510.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15008
Raw data (/proc/15004/stat): 15004 (minisat+_script) S 15003 15004 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793695849 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15004/statm): 531 226 485 147 0 384 0
[pid=15004] vsize: 2124
Raw data (/proc/15008/stat): 15008 (minisat+_64-bit) R 15004 15004 30740 0 -1 0 12562 0 0 0 50867 66 0 0 25 0 1 0 1793695854 54165504 12206 4294967295 134512640 135094434 3221224432 3221223088 134558187 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15008/statm): 13224 12206 145 145 0 13079 0
[pid=15008] vsize: 52896
Current children cumulated CPU time (s) 509.34
Current children cumulated vsize (Kb) 55020

[startup+520.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15008
Raw data (/proc/15004/stat): 15004 (minisat+_script) S 15003 15004 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793695849 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15004/statm): 531 226 485 147 0 384 0
[pid=15004] vsize: 2124
Raw data (/proc/15008/stat): 15008 (minisat+_64-bit) R 15004 15004 30740 0 -1 0 12607 0 0 0 51866 67 0 0 25 0 1 0 1793695854 54607872 12251 4294967295 134512640 135094434 3221224432 3221223056 134557658 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15008/statm): 13332 12251 145 145 0 13187 0
[pid=15008] vsize: 53328
Current children cumulated CPU time (s) 519.34
Current children cumulated vsize (Kb) 55452

[startup+530.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15008
Raw data (/proc/15004/stat): 15004 (minisat+_script) S 15003 15004 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793695849 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15004/statm): 531 226 485 147 0 384 0
[pid=15004] vsize: 2124
Raw data (/proc/15008/stat): 15008 (minisat+_64-bit) R 15004 15004 30740 0 -1 0 12663 0 0 0 52864 68 0 0 25 0 1 0 1793695854 54837248 12307 4294967295 134512640 135094434 3221224432 3221223088 134557860 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15008/statm): 13388 12307 145 145 0 13243 0
[pid=15008] vsize: 53552
Current children cumulated CPU time (s) 529.33
Current children cumulated vsize (Kb) 55676

[startup+540.051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15008
Raw data (/proc/15004/stat): 15004 (minisat+_script) S 15003 15004 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793695849 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15004/statm): 531 226 485 147 0 384 0
[pid=15004] vsize: 2124
Raw data (/proc/15008/stat): 15008 (minisat+_64-bit) R 15004 15004 30740 0 -1 0 12709 0 0 0 53864 68 0 0 25 0 1 0 1793695854 55021568 12353 4294967295 134512640 135094434 3221224432 3221223024 134557196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15008/statm): 13433 12353 145 145 0 13288 0
[pid=15008] vsize: 53732
Current children cumulated CPU time (s) 539.33
Current children cumulated vsize (Kb) 55856

[startup+550.052 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15008
Raw data (/proc/15004/stat): 15004 (minisat+_script) S 15003 15004 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793695849 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15004/statm): 531 226 485 147 0 384 0
[pid=15004] vsize: 2124
Raw data (/proc/15008/stat): 15008 (minisat+_64-bit) R 15004 15004 30740 0 -1 0 12759 0 0 0 54864 68 0 0 25 0 1 0 1793695854 55222272 12403 4294967295 134512640 135094434 3221224432 3221223044 134563046 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15008/statm): 13482 12403 145 145 0 13337 0
[pid=15008] vsize: 53928
Current children cumulated CPU time (s) 549.33
Current children cumulated vsize (Kb) 56052

[startup+560.053 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15008
Raw data (/proc/15004/stat): 15004 (minisat+_script) S 15003 15004 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793695849 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15004/statm): 531 226 485 147 0 384 0
[pid=15004] vsize: 2124
Raw data (/proc/15008/stat): 15008 (minisat+_64-bit) R 15004 15004 30740 0 -1 0 12809 0 0 0 55864 68 0 0 25 0 1 0 1793695854 55422976 12453 4294967295 134512640 135094434 3221224432 3221223024 134556847 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15008/statm): 13531 12453 145 145 0 13386 0
[pid=15008] vsize: 54124
Current children cumulated CPU time (s) 559.33
Current children cumulated vsize (Kb) 56248

[startup+570.053 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15008
Raw data (/proc/15004/stat): 15004 (minisat+_script) S 15003 15004 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793695849 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15004/statm): 531 226 485 147 0 384 0
[pid=15004] vsize: 2124
Raw data (/proc/15008/stat): 15008 (minisat+_64-bit) R 15004 15004 30740 0 -1 0 12865 0 0 0 56863 68 0 0 25 0 1 0 1793695854 55648256 12509 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15008/statm): 13586 12509 145 145 0 13441 0
[pid=15008] vsize: 54344
Current children cumulated CPU time (s) 569.32
Current children cumulated vsize (Kb) 56468

[startup+580.054 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15008
Raw data (/proc/15004/stat): 15004 (minisat+_script) S 15003 15004 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793695849 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15004/statm): 531 226 485 147 0 384 0
[pid=15004] vsize: 2124
Raw data (/proc/15008/stat): 15008 (minisat+_64-bit) R 15004 15004 30740 0 -1 0 12983 0 0 0 57861 70 0 0 25 0 1 0 1793695854 56119296 12627 4294967295 134512640 135094434 3221224432 3221223056 134557574 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15008/statm): 13701 12627 145 145 0 13556 0
[pid=15008] vsize: 54804
Current children cumulated CPU time (s) 579.32
Current children cumulated vsize (Kb) 56928

[startup+590.055 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15008
Raw data (/proc/15004/stat): 15004 (minisat+_script) S 15003 15004 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793695849 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15004/statm): 531 226 485 147 0 384 0
[pid=15004] vsize: 2124
Raw data (/proc/15008/stat): 15008 (minisat+_64-bit) R 15004 15004 30740 0 -1 0 13041 0 0 0 58860 71 0 0 25 0 1 0 1793695854 56356864 12685 4294967295 134512640 135094434 3221224432 3221223056 134557565 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15008/statm): 13759 12685 145 145 0 13614 0
[pid=15008] vsize: 55036
Current children cumulated CPU time (s) 589.32
Current children cumulated vsize (Kb) 57160

[startup+600.056 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15008
Raw data (/proc/15004/stat): 15004 (minisat+_script) S 15003 15004 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793695849 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15004/statm): 531 226 485 147 0 384 0
[pid=15004] vsize: 2124
Raw data (/proc/15008/stat): 15008 (minisat+_64-bit) R 15004 15004 30740 0 -1 0 13137 0 0 0 59859 72 0 0 25 0 1 0 1793695854 56737792 12781 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15008/statm): 13852 12781 145 145 0 13707 0
[pid=15008] vsize: 55408
Current children cumulated CPU time (s) 599.32
Current children cumulated vsize (Kb) 57532

[startup+610.056 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15008
Raw data (/proc/15004/stat): 15004 (minisat+_script) S 15003 15004 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793695849 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15004/statm): 531 226 485 147 0 384 0
[pid=15004] vsize: 2124
Raw data (/proc/15008/stat): 15008 (minisat+_64-bit) R 15004 15004 30740 0 -1 0 13196 0 0 0 60858 72 0 0 25 0 1 0 1793695854 56983552 12840 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15008/statm): 13912 12840 145 145 0 13767 0
[pid=15008] vsize: 55648
Current children cumulated CPU time (s) 609.31
Current children cumulated vsize (Kb) 57772

[startup+620.057 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15008
Raw data (/proc/15004/stat): 15004 (minisat+_script) S 15003 15004 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793695849 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15004/statm): 531 226 485 147 0 384 0
[pid=15004] vsize: 2124
Raw data (/proc/15008/stat): 15008 (minisat+_64-bit) R 15004 15004 30740 0 -1 0 13269 0 0 0 61857 74 0 0 25 0 1 0 1793695854 57278464 12913 4294967295 134512640 135094434 3221224432 3221223056 134557565 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15008/statm): 13984 12913 145 145 0 13839 0
[pid=15008] vsize: 55936
Current children cumulated CPU time (s) 619.32
Current children cumulated vsize (Kb) 58060

[startup+630.058 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15008
Raw data (/proc/15004/stat): 15004 (minisat+_script) S 15003 15004 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793695849 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15004/statm): 531 226 485 147 0 384 0
[pid=15004] vsize: 2124
Raw data (/proc/15008/stat): 15008 (minisat+_64-bit) R 15004 15004 30740 0 -1 0 13358 0 0 0 62855 75 0 0 25 0 1 0 1793695854 57634816 13002 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15008/statm): 14071 13002 145 145 0 13926 0
[pid=15008] vsize: 56284
Current children cumulated CPU time (s) 629.31
Current children cumulated vsize (Kb) 58408

[startup+640.059 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15008
Raw data (/proc/15004/stat): 15004 (minisat+_script) S 15003 15004 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793695849 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15004/statm): 531 226 485 147 0 384 0
[pid=15004] vsize: 2124
Raw data (/proc/15008/stat): 15008 (minisat+_64-bit) R 15004 15004 30740 0 -1 0 13419 0 0 0 63854 76 0 0 25 0 1 0 1793695854 57880576 13063 4294967295 134512640 135094434 3221224432 3221223024 134556789 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15008/statm): 14131 13063 145 145 0 13986 0
[pid=15008] vsize: 56524
Current children cumulated CPU time (s) 639.31
Current children cumulated vsize (Kb) 58648

[startup+650.059 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15008
Raw data (/proc/15004/stat): 15004 (minisat+_script) S 15003 15004 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793695849 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15004/statm): 531 226 485 147 0 384 0
[pid=15004] vsize: 2124
Raw data (/proc/15008/stat): 15008 (minisat+_64-bit) R 15004 15004 30740 0 -1 0 13486 0 0 0 64853 77 0 0 25 0 1 0 1793695854 58155008 13130 4294967295 134512640 135094434 3221224432 3221223056 134562104 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15008/statm): 14198 13130 145 145 0 14053 0
[pid=15008] vsize: 56792
Current children cumulated CPU time (s) 649.31
Current children cumulated vsize (Kb) 58916

[startup+660.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15008
Raw data (/proc/15004/stat): 15004 (minisat+_script) S 15003 15004 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793695849 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15004/statm): 531 226 485 147 0 384 0
[pid=15004] vsize: 2124
Raw data (/proc/15008/stat): 15008 (minisat+_64-bit) R 15004 15004 30740 0 -1 0 13519 0 0 0 65852 77 0 0 25 0 1 0 1793695854 58286080 13163 4294967295 134512640 135094434 3221224432 3221223056 134562139 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15008/statm): 14230 13163 145 145 0 14085 0
[pid=15008] vsize: 56920
Current children cumulated CPU time (s) 659.3
Current children cumulated vsize (Kb) 59044

[startup+670.061 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15008
Raw data (/proc/15004/stat): 15004 (minisat+_script) S 15003 15004 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793695849 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15004/statm): 531 226 485 147 0 384 0
[pid=15004] vsize: 2124
Raw data (/proc/15008/stat): 15008 (minisat+_64-bit) R 15004 15004 30740 0 -1 0 13551 0 0 0 66852 77 0 0 25 0 1 0 1793695854 58413056 13195 4294967295 134512640 135094434 3221224432 3221223056 134557585 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15008/statm): 14261 13195 145 145 0 14116 0
[pid=15008] vsize: 57044
Current children cumulated CPU time (s) 669.3
Current children cumulated vsize (Kb) 59168

[startup+680.062 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15008
Raw data (/proc/15004/stat): 15004 (minisat+_script) S 15003 15004 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793695849 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15004/statm): 531 226 485 147 0 384 0
[pid=15004] vsize: 2124
Raw data (/proc/15008/stat): 15008 (minisat+_64-bit) R 15004 15004 30740 0 -1 0 13601 0 0 0 67851 78 0 0 25 0 1 0 1793695854 58613760 13245 4294967295 134512640 135094434 3221224432 3221223056 134557650 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15008/statm): 14310 13245 145 145 0 14165 0
[pid=15008] vsize: 57240
Current children cumulated CPU time (s) 679.3
Current children cumulated vsize (Kb) 59364

[startup+690.062 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15008
Raw data (/proc/15004/stat): 15004 (minisat+_script) S 15003 15004 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793695849 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15004/statm): 531 226 485 147 0 384 0
[pid=15004] vsize: 2124
Raw data (/proc/15008/stat): 15008 (minisat+_64-bit) R 15004 15004 30740 0 -1 0 13658 0 0 0 68850 79 0 0 25 0 1 0 1793695854 58851328 13302 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15008/statm): 14368 13302 145 145 0 14223 0
[pid=15008] vsize: 57472
Current children cumulated CPU time (s) 689.3
Current children cumulated vsize (Kb) 59596

[startup+700.063 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15008
Raw data (/proc/15004/stat): 15004 (minisat+_script) S 15003 15004 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793695849 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15004/statm): 531 226 485 147 0 384 0
[pid=15004] vsize: 2124
Raw data (/proc/15008/stat): 15008 (minisat+_64-bit) R 15004 15004 30740 0 -1 0 13757 0 0 0 69849 79 0 0 25 0 1 0 1793695854 59252736 13401 4294967295 134512640 135094434 3221224432 3221223088 134557893 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15008/statm): 14466 13401 145 145 0 14321 0
[pid=15008] vsize: 57864
Current children cumulated CPU time (s) 699.29
Current children cumulated vsize (Kb) 59988

[startup+710.064 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15008
Raw data (/proc/15004/stat): 15004 (minisat+_script) S 15003 15004 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793695849 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15004/statm): 531 226 485 147 0 384 0
[pid=15004] vsize: 2124
Raw data (/proc/15008/stat): 15008 (minisat+_64-bit) R 15004 15004 30740 0 -1 0 13819 0 0 0 70846 81 0 0 25 0 1 0 1793695854 59502592 13463 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15008/statm): 14527 13463 145 145 0 14382 0
[pid=15008] vsize: 58108
Current children cumulated CPU time (s) 709.28
Current children cumulated vsize (Kb) 60232

[startup+720.065 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15008
Raw data (/proc/15004/stat): 15004 (minisat+_script) S 15003 15004 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793695849 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15004/statm): 531 226 485 147 0 384 0
[pid=15004] vsize: 2124
Raw data (/proc/15008/stat): 15008 (minisat+_64-bit) R 15004 15004 30740 0 -1 0 13891 0 0 0 71844 81 0 0 25 0 1 0 1793695854 59797504 13535 4294967295 134512640 135094434 3221224432 3221223024 134556851 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15008/statm): 14599 13535 145 145 0 14454 0
[pid=15008] vsize: 58396
Current children cumulated CPU time (s) 719.26
Current children cumulated vsize (Kb) 60520

[startup+730.066 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15008
Raw data (/proc/15004/stat): 15004 (minisat+_script) S 15003 15004 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793695849 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15004/statm): 531 226 485 147 0 384 0
[pid=15004] vsize: 2124
Raw data (/proc/15008/stat): 15008 (minisat+_64-bit) R 15004 15004 30740 0 -1 0 13971 0 0 0 72843 82 0 0 25 0 1 0 1793695854 60121088 13615 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15008/statm): 14678 13615 145 145 0 14533 0
[pid=15008] vsize: 58712
Current children cumulated CPU time (s) 729.26
Current children cumulated vsize (Kb) 60836

[startup+740.067 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15008
Raw data (/proc/15004/stat): 15004 (minisat+_script) S 15003 15004 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793695849 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15004/statm): 531 226 485 147 0 384 0
[pid=15004] vsize: 2124
Raw data (/proc/15008/stat): 15008 (minisat+_64-bit) R 15004 15004 30740 0 -1 0 14058 0 0 0 73842 83 0 0 25 0 1 0 1793695854 60469248 13702 4294967295 134512640 135094434 3221224432 3221223088 134557896 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15008/statm): 14763 13702 145 145 0 14618 0
[pid=15008] vsize: 59052
Current children cumulated CPU time (s) 739.26
Current children cumulated vsize (Kb) 61176

[startup+750.068 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15008
Raw data (/proc/15004/stat): 15004 (minisat+_script) S 15003 15004 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793695849 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15004/statm): 531 226 485 147 0 384 0
[pid=15004] vsize: 2124
Raw data (/proc/15008/stat): 15008 (minisat+_64-bit) R 15004 15004 30740 0 -1 0 14138 0 0 0 74841 83 0 0 25 0 1 0 1793695854 60796928 13782 4294967295 134512640 135094434 3221224432 3221223024 134556862 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15008/statm): 14843 13782 145 145 0 14698 0
[pid=15008] vsize: 59372
Current children cumulated CPU time (s) 749.25
Current children cumulated vsize (Kb) 61496

[startup+760.068 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15008
Raw data (/proc/15004/stat): 15004 (minisat+_script) S 15003 15004 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793695849 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15004/statm): 531 226 485 147 0 384 0
[pid=15004] vsize: 2124
Raw data (/proc/15008/stat): 15008 (minisat+_64-bit) R 15004 15004 30740 0 -1 0 14236 0 0 0 75840 84 0 0 25 0 1 0 1793695854 61194240 13880 4294967295 134512640 135094434 3221224432 3221223056 134557711 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15008/statm): 14940 13880 145 145 0 14795 0
[pid=15008] vsize: 59760
Current children cumulated CPU time (s) 759.25
Current children cumulated vsize (Kb) 61884

[startup+770.069 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15008
Raw data (/proc/15004/stat): 15004 (minisat+_script) S 15003 15004 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793695849 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15004/statm): 531 226 485 147 0 384 0
[pid=15004] vsize: 2124
Raw data (/proc/15008/stat): 15008 (minisat+_64-bit) R 15004 15004 30740 0 -1 0 14295 0 0 0 76838 85 0 0 25 0 1 0 1793695854 61444096 13939 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15008/statm): 15001 13939 145 145 0 14856 0
[pid=15008] vsize: 60004
Current children cumulated CPU time (s) 769.24
Current children cumulated vsize (Kb) 62128

[startup+780.069 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15008
Raw data (/proc/15004/stat): 15004 (minisat+_script) S 15003 15004 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793695849 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15004/statm): 531 226 485 147 0 384 0
[pid=15004] vsize: 2124
Raw data (/proc/15008/stat): 15008 (minisat+_64-bit) R 15004 15004 30740 0 -1 0 14509 0 0 0 77835 86 0 0 25 0 1 0 1793695854 62308352 14153 4294967295 134512640 135094434 3221224432 3221223056 134562104 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15008/statm): 15212 14153 145 145 0 15067 0
[pid=15008] vsize: 60848
Current children cumulated CPU time (s) 779.22
Current children cumulated vsize (Kb) 62972

[startup+790.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15008
Raw data (/proc/15004/stat): 15004 (minisat+_script) S 15003 15004 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793695849 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15004/statm): 531 226 485 147 0 384 0
[pid=15004] vsize: 2124
Raw data (/proc/15008/stat): 15008 (minisat+_64-bit) R 15004 15004 30740 0 -1 0 14599 0 0 0 78834 87 0 0 25 0 1 0 1793695854 62672896 14243 4294967295 134512640 135094434 3221224432 3221223060 134557564 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15008/statm): 15301 14243 145 145 0 15156 0
[pid=15008] vsize: 61204
Current children cumulated CPU time (s) 789.22
Current children cumulated vsize (Kb) 63328

[startup+800.071 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15008
Raw data (/proc/15004/stat): 15004 (minisat+_script) S 15003 15004 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793695849 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15004/statm): 531 226 485 147 0 384 0
[pid=15004] vsize: 2124
Raw data (/proc/15008/stat): 15008 (minisat+_64-bit) R 15004 15004 30740 0 -1 0 14676 0 0 0 79833 87 0 0 25 0 1 0 1793695854 62984192 14320 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15008/statm): 15377 14320 145 145 0 15232 0
[pid=15008] vsize: 61508
Current children cumulated CPU time (s) 799.21
Current children cumulated vsize (Kb) 63632

[startup+810.072 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15008
Raw data (/proc/15004/stat): 15004 (minisat+_script) S 15003 15004 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793695849 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15004/statm): 531 226 485 147 0 384 0
[pid=15004] vsize: 2124
Raw data (/proc/15008/stat): 15008 (minisat+_64-bit) R 15004 15004 30740 0 -1 0 14809 0 0 0 80831 88 0 0 25 0 1 0 1793695854 63537152 14453 4294967295 134512640 135094434 3221224432 3221223088 134558221 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15008/statm): 15512 14453 145 145 0 15367 0
[pid=15008] vsize: 62048
Current children cumulated CPU time (s) 809.2
Current children cumulated vsize (Kb) 64172

[startup+820.072 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15008
Raw data (/proc/15004/stat): 15004 (minisat+_script) S 15003 15004 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793695849 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15004/statm): 531 226 485 147 0 384 0
[pid=15004] vsize: 2124
Raw data (/proc/15008/stat): 15008 (minisat+_64-bit) R 15004 15004 30740 0 -1 0 14934 0 0 0 81830 89 0 0 25 0 1 0 1793695854 64057344 14578 4294967295 134512640 135094434 3221224432 3221223056 134557726 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15008/statm): 15639 14578 145 145 0 15494 0
[pid=15008] vsize: 62556
Current children cumulated CPU time (s) 819.2
Current children cumulated vsize (Kb) 64680

[startup+830.073 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15008
Raw data (/proc/15004/stat): 15004 (minisat+_script) S 15003 15004 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793695849 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15004/statm): 531 226 485 147 0 384 0
[pid=15004] vsize: 2124
Raw data (/proc/15008/stat): 15008 (minisat+_64-bit) R 15004 15004 30740 0 -1 0 15081 0 0 0 82829 89 0 0 25 0 1 0 1793695854 64651264 14725 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15008/statm): 15784 14725 145 145 0 15639 0
[pid=15008] vsize: 63136
Current children cumulated CPU time (s) 829.19
Current children cumulated vsize (Kb) 65260

[startup+840.074 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15008
Raw data (/proc/15004/stat): 15004 (minisat+_script) S 15003 15004 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793695849 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15004/statm): 531 226 485 147 0 384 0
[pid=15004] vsize: 2124
Raw data (/proc/15008/stat): 15008 (minisat+_64-bit) R 15004 15004 30740 0 -1 0 15135 0 0 0 83828 90 0 0 25 0 1 0 1793695854 64868352 14779 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15008/statm): 15837 14779 145 145 0 15692 0
[pid=15008] vsize: 63348
Current children cumulated CPU time (s) 839.19
Current children cumulated vsize (Kb) 65472

[startup+850.075 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15008
Raw data (/proc/15004/stat): 15004 (minisat+_script) S 15003 15004 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793695849 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15004/statm): 531 226 485 147 0 384 0
[pid=15004] vsize: 2124
Raw data (/proc/15008/stat): 15008 (minisat+_64-bit) R 15004 15004 30740 0 -1 0 15228 0 0 0 84827 90 0 0 25 0 1 0 1793695854 65261568 14872 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15008/statm): 15933 14872 145 145 0 15788 0
[pid=15008] vsize: 63732
Current children cumulated CPU time (s) 849.18
Current children cumulated vsize (Kb) 65856

[startup+860.076 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15008
Raw data (/proc/15004/stat): 15004 (minisat+_script) S 15003 15004 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793695849 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15004/statm): 531 226 485 147 0 384 0
[pid=15004] vsize: 2124
Raw data (/proc/15008/stat): 15008 (minisat+_64-bit) R 15004 15004 30740 0 -1 0 15280 0 0 0 85827 91 0 0 25 0 1 0 1793695854 65470464 14924 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15008/statm): 15984 14924 145 145 0 15839 0
[pid=15008] vsize: 63936
Current children cumulated CPU time (s) 859.19
Current children cumulated vsize (Kb) 66060

[startup+870.076 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15008
Raw data (/proc/15004/stat): 15004 (minisat+_script) S 15003 15004 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793695849 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15004/statm): 531 226 485 147 0 384 0
[pid=15004] vsize: 2124
Raw data (/proc/15008/stat): 15008 (minisat+_64-bit) R 15004 15004 30740 0 -1 0 15332 0 0 0 86826 91 0 0 25 0 1 0 1793695854 65679360 14976 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15008/statm): 16035 14976 145 145 0 15890 0
[pid=15008] vsize: 64140
Current children cumulated CPU time (s) 869.18
Current children cumulated vsize (Kb) 66264

[startup+880.077 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15008
Raw data (/proc/15004/stat): 15004 (minisat+_script) S 15003 15004 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793695849 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15004/statm): 531 226 485 147 0 384 0
[pid=15004] vsize: 2124
Raw data (/proc/15008/stat): 15008 (minisat+_64-bit) R 15004 15004 30740 0 -1 0 15387 0 0 0 87826 91 0 0 25 0 1 0 1793695854 65912832 15031 4294967295 134512640 135094434 3221224432 3221223120 134554723 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15008/statm): 16092 15031 145 145 0 15947 0
[pid=15008] vsize: 64368
Current children cumulated CPU time (s) 879.18
Current children cumulated vsize (Kb) 66492

[startup+890.079 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15008
Raw data (/proc/15004/stat): 15004 (minisat+_script) S 15003 15004 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793695849 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15004/statm): 531 226 485 147 0 384 0
[pid=15004] vsize: 2124
Raw data (/proc/15008/stat): 15008 (minisat+_64-bit) R 15004 15004 30740 0 -1 0 15449 0 0 0 88825 92 0 0 25 0 1 0 1793695854 66166784 15093 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15008/statm): 16154 15093 145 145 0 16009 0
[pid=15008] vsize: 64616
Current children cumulated CPU time (s) 889.18
Current children cumulated vsize (Kb) 66740

[startup+900.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15008
Raw data (/proc/15004/stat): 15004 (minisat+_script) S 15003 15004 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793695849 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15004/statm): 531 226 485 147 0 384 0
[pid=15004] vsize: 2124
Raw data (/proc/15008/stat): 15008 (minisat+_64-bit) R 15004 15004 30740 0 -1 0 15522 0 0 0 89823 93 0 0 25 0 1 0 1793695854 66461696 15166 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15008/statm): 16226 15166 145 145 0 16081 0
[pid=15008] vsize: 64904
Current children cumulated CPU time (s) 899.17
Current children cumulated vsize (Kb) 67028

[startup+910.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15008
Raw data (/proc/15004/stat): 15004 (minisat+_script) S 15003 15004 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793695849 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15004/statm): 531 226 485 147 0 384 0
[pid=15004] vsize: 2124
Raw data (/proc/15008/stat): 15008 (minisat+_64-bit) R 15004 15004 30740 0 -1 0 15591 0 0 0 90822 93 0 0 25 0 1 0 1793695854 66740224 15235 4294967295 134512640 135094434 3221224432 3221223056 134557565 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15008/statm): 16294 15235 145 145 0 16149 0
[pid=15008] vsize: 65176
Current children cumulated CPU time (s) 909.16
Current children cumulated vsize (Kb) 67300

[startup+920.081 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15008
Raw data (/proc/15004/stat): 15004 (minisat+_script) S 15003 15004 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793695849 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15004/statm): 531 226 485 147 0 384 0
[pid=15004] vsize: 2124
Raw data (/proc/15008/stat): 15008 (minisat+_64-bit) R 15004 15004 30740 0 -1 0 15682 0 0 0 91821 93 0 0 25 0 1 0 1793695854 67108864 15326 4294967295 134512640 135094434 3221224432 3221223044 134563046 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15008/statm): 16384 15326 145 145 0 16239 0
[pid=15008] vsize: 65536
Current children cumulated CPU time (s) 919.15
Current children cumulated vsize (Kb) 67660

[startup+930.082 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15008
Raw data (/proc/15004/stat): 15004 (minisat+_script) S 15003 15004 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793695849 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15004/statm): 531 226 485 147 0 384 0
[pid=15004] vsize: 2124
Raw data (/proc/15008/stat): 15008 (minisat+_64-bit) R 15004 15004 30740 0 -1 0 15731 0 0 0 92821 94 0 0 25 0 1 0 1793695854 67309568 15375 4294967295 134512640 135094434 3221224432 3221223088 134558286 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15008/statm): 16433 15375 145 145 0 16288 0
[pid=15008] vsize: 65732
Current children cumulated CPU time (s) 929.16
Current children cumulated vsize (Kb) 67856

[startup+940.083 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15008
Raw data (/proc/15004/stat): 15004 (minisat+_script) S 15003 15004 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793695849 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15004/statm): 531 226 485 147 0 384 0
[pid=15004] vsize: 2124
Raw data (/proc/15008/stat): 15008 (minisat+_64-bit) R 15004 15004 30740 0 -1 0 15731 0 0 0 93821 94 0 0 25 0 1 0 1793695854 67309568 15375 4294967295 134512640 135094434 3221224432 3221223088 134557792 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15008/statm): 16433 15375 145 145 0 16288 0
[pid=15008] vsize: 65732
Current children cumulated CPU time (s) 939.16
Current children cumulated vsize (Kb) 67856

[startup+950.084 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15008
Raw data (/proc/15004/stat): 15004 (minisat+_script) S 15003 15004 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793695849 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15004/statm): 531 226 485 147 0 384 0
[pid=15004] vsize: 2124
Raw data (/proc/15008/stat): 15008 (minisat+_64-bit) R 15004 15004 30740 0 -1 0 15731 0 0 0 94821 94 0 0 25 0 1 0 1793695854 67309568 15375 4294967295 134512640 135094434 3221224432 3221221456 134676539 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15008/statm): 16433 15375 145 145 0 16288 0
[pid=15008] vsize: 65732
Current children cumulated CPU time (s) 949.16
Current children cumulated vsize (Kb) 67856

[startup+960.085 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15008
Raw data (/proc/15004/stat): 15004 (minisat+_script) S 15003 15004 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793695849 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15004/statm): 531 226 485 147 0 384 0
[pid=15004] vsize: 2124
Raw data (/proc/15008/stat): 15008 (minisat+_64-bit) R 15004 15004 30740 0 -1 0 15732 0 0 0 95821 94 0 0 25 0 1 0 1793695854 67309568 15376 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15008/statm): 16433 15376 145 145 0 16288 0
[pid=15008] vsize: 65732
Current children cumulated CPU time (s) 959.16
Current children cumulated vsize (Kb) 67856

[startup+970.085 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15008
Raw data (/proc/15004/stat): 15004 (minisat+_script) S 15003 15004 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793695849 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15004/statm): 531 226 485 147 0 384 0
[pid=15004] vsize: 2124
Raw data (/proc/15008/stat): 15008 (minisat+_64-bit) R 15004 15004 30740 0 -1 0 15732 0 0 0 96821 94 0 0 25 0 1 0 1793695854 67309568 15376 4294967295 134512640 135094434 3221224432 3221223056 134557685 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15008/statm): 16433 15376 145 145 0 16288 0
[pid=15008] vsize: 65732
Current children cumulated CPU time (s) 969.16
Current children cumulated vsize (Kb) 67856

[startup+980.086 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15008
Raw data (/proc/15004/stat): 15004 (minisat+_script) S 15003 15004 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793695849 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15004/statm): 531 226 485 147 0 384 0
[pid=15004] vsize: 2124
Raw data (/proc/15008/stat): 15008 (minisat+_64-bit) R 15004 15004 30740 0 -1 0 15732 0 0 0 97822 94 0 0 25 0 1 0 1793695854 67309568 15376 4294967295 134512640 135094434 3221224432 3221223056 134557593 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15008/statm): 16433 15376 145 145 0 16288 0
[pid=15008] vsize: 65732
Current children cumulated CPU time (s) 979.17
Current children cumulated vsize (Kb) 67856

[startup+990.088 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15008
Raw data (/proc/15004/stat): 15004 (minisat+_script) S 15003 15004 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793695849 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15004/statm): 531 226 485 147 0 384 0
[pid=15004] vsize: 2124
Raw data (/proc/15008/stat): 15008 (minisat+_64-bit) R 15004 15004 30740 0 -1 0 15732 0 0 0 98822 94 0 0 25 0 1 0 1793695854 67309568 15376 4294967295 134512640 135094434 3221224432 3221223088 134557804 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15008/statm): 16433 15376 145 145 0 16288 0
[pid=15008] vsize: 65732
Current children cumulated CPU time (s) 989.17
Current children cumulated vsize (Kb) 67856

[startup+1000.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15008
Raw data (/proc/15004/stat): 15004 (minisat+_script) S 15003 15004 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793695849 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15004/statm): 531 226 485 147 0 384 0
[pid=15004] vsize: 2124
Raw data (/proc/15008/stat): 15008 (minisat+_64-bit) R 15004 15004 30740 0 -1 0 15732 0 0 0 99822 94 0 0 25 0 1 0 1793695854 67309568 15376 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15008/statm): 16433 15376 145 145 0 16288 0
[pid=15008] vsize: 65732
Current children cumulated CPU time (s) 999.17
Current children cumulated vsize (Kb) 67856

[startup+1010.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15008
Raw data (/proc/15004/stat): 15004 (minisat+_script) S 15003 15004 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793695849 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15004/statm): 531 226 485 147 0 384 0
[pid=15004] vsize: 2124
Raw data (/proc/15008/stat): 15008 (minisat+_64-bit) R 15004 15004 30740 0 -1 0 15732 0 0 0 100822 94 0 0 25 0 1 0 1793695854 67309568 15376 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15008/statm): 16433 15376 145 145 0 16288 0
[pid=15008] vsize: 65732
Current children cumulated CPU time (s) 1009.17
Current children cumulated vsize (Kb) 67856

[startup+1020.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15008
Raw data (/proc/15004/stat): 15004 (minisat+_script) S 15003 15004 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793695849 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15004/statm): 531 226 485 147 0 384 0
[pid=15004] vsize: 2124
Raw data (/proc/15008/stat): 15008 (minisat+_64-bit) R 15004 15004 30740 0 -1 0 15732 0 0 0 101823 94 0 0 25 0 1 0 1793695854 67309568 15376 4294967295 134512640 135094434 3221224432 3221223072 134538540 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15008/statm): 16433 15376 145 145 0 16288 0
[pid=15008] vsize: 65732
Current children cumulated CPU time (s) 1019.18
Current children cumulated vsize (Kb) 67856

[startup+1030.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15008
Raw data (/proc/15004/stat): 15004 (minisat+_script) S 15003 15004 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793695849 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15004/statm): 531 226 485 147 0 384 0
[pid=15004] vsize: 2124
Raw data (/proc/15008/stat): 15008 (minisat+_64-bit) R 15004 15004 30740 0 -1 0 15732 0 0 0 102823 94 0 0 25 0 1 0 1793695854 67309568 15376 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15008/statm): 16433 15376 145 145 0 16288 0
[pid=15008] vsize: 65732
Current children cumulated CPU time (s) 1029.18
Current children cumulated vsize (Kb) 67856

[startup+1040.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15008
Raw data (/proc/15004/stat): 15004 (minisat+_script) S 15003 15004 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793695849 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15004/statm): 531 226 485 147 0 384 0
[pid=15004] vsize: 2124
Raw data (/proc/15008/stat): 15008 (minisat+_64-bit) R 15004 15004 30740 0 -1 0 15732 0 0 0 103823 94 0 0 25 0 1 0 1793695854 67309568 15376 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15008/statm): 16433 15376 145 145 0 16288 0
[pid=15008] vsize: 65732
Current children cumulated CPU time (s) 1039.18
Current children cumulated vsize (Kb) 67856

[startup+1050.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15008
Raw data (/proc/15004/stat): 15004 (minisat+_script) S 15003 15004 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793695849 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15004/statm): 531 226 485 147 0 384 0
[pid=15004] vsize: 2124
Raw data (/proc/15008/stat): 15008 (minisat+_64-bit) R 15004 15004 30740 0 -1 0 15732 0 0 0 104823 95 0 0 25 0 1 0 1793695854 67309568 15376 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15008/statm): 16433 15376 145 145 0 16288 0
[pid=15008] vsize: 65732
Current children cumulated CPU time (s) 1049.19
Current children cumulated vsize (Kb) 67856

[startup+1060.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15008
Raw data (/proc/15004/stat): 15004 (minisat+_script) S 15003 15004 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793695849 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15004/statm): 531 226 485 147 0 384 0
[pid=15004] vsize: 2124
Raw data (/proc/15008/stat): 15008 (minisat+_64-bit) R 15004 15004 30740 0 -1 0 15732 0 0 0 105823 95 0 0 25 0 1 0 1793695854 67309568 15376 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15008/statm): 16433 15376 145 145 0 16288 0
[pid=15008] vsize: 65732
Current children cumulated CPU time (s) 1059.19
Current children cumulated vsize (Kb) 67856

[startup+1070.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15008
Raw data (/proc/15004/stat): 15004 (minisat+_script) S 15003 15004 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793695849 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15004/statm): 531 226 485 147 0 384 0
[pid=15004] vsize: 2124
Raw data (/proc/15008/stat): 15008 (minisat+_64-bit) R 15004 15004 30740 0 -1 0 15732 0 0 0 106824 95 0 0 25 0 1 0 1793695854 67309568 15376 4294967295 134512640 135094434 3221224432 3221223024 134556862 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15008/statm): 16433 15376 145 145 0 16288 0
[pid=15008] vsize: 65732
Current children cumulated CPU time (s) 1069.2
Current children cumulated vsize (Kb) 67856

[startup+1080.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15008
Raw data (/proc/15004/stat): 15004 (minisat+_script) S 15003 15004 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793695849 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15004/statm): 531 226 485 147 0 384 0
[pid=15004] vsize: 2124
Raw data (/proc/15008/stat): 15008 (minisat+_64-bit) R 15004 15004 30740 0 -1 0 15734 0 0 0 107824 95 0 0 25 0 1 0 1793695854 67309568 15378 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15008/statm): 16433 15378 145 145 0 16288 0
[pid=15008] vsize: 65732
Current children cumulated CPU time (s) 1079.2
Current children cumulated vsize (Kb) 67856

[startup+1090.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15008
Raw data (/proc/15004/stat): 15004 (minisat+_script) S 15003 15004 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793695849 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15004/statm): 531 226 485 147 0 384 0
[pid=15004] vsize: 2124
Raw data (/proc/15008/stat): 15008 (minisat+_64-bit) R 15004 15004 30740 0 -1 0 15734 0 0 0 108824 95 0 0 25 0 1 0 1793695854 67309568 15378 4294967295 134512640 135094434 3221224432 3221223088 134558016 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15008/statm): 16433 15378 145 145 0 16288 0
[pid=15008] vsize: 65732
Current children cumulated CPU time (s) 1089.2
Current children cumulated vsize (Kb) 67856

[startup+1100.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15008
Raw data (/proc/15004/stat): 15004 (minisat+_script) S 15003 15004 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793695849 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15004/statm): 531 226 485 147 0 384 0
[pid=15004] vsize: 2124
Raw data (/proc/15008/stat): 15008 (minisat+_64-bit) R 15004 15004 30740 0 -1 0 15734 0 0 0 109825 95 0 0 25 0 1 0 1793695854 67309568 15378 4294967295 134512640 135094434 3221224432 3221223088 134558221 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15008/statm): 16433 15378 145 145 0 16288 0
[pid=15008] vsize: 65732
Current children cumulated CPU time (s) 1099.21
Current children cumulated vsize (Kb) 67856

[startup+1110.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15008
Raw data (/proc/15004/stat): 15004 (minisat+_script) S 15003 15004 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793695849 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15004/statm): 531 226 485 147 0 384 0
[pid=15004] vsize: 2124
Raw data (/proc/15008/stat): 15008 (minisat+_64-bit) R 15004 15004 30740 0 -1 0 15734 0 0 0 110825 95 0 0 25 0 1 0 1793695854 67309568 15378 4294967295 134512640 135094434 3221224432 3221223056 134557696 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15008/statm): 16433 15378 145 145 0 16288 0
[pid=15008] vsize: 65732
Current children cumulated CPU time (s) 1109.21
Current children cumulated vsize (Kb) 67856

[startup+1120.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15008
Raw data (/proc/15004/stat): 15004 (minisat+_script) S 15003 15004 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793695849 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15004/statm): 531 226 485 147 0 384 0
[pid=15004] vsize: 2124
Raw data (/proc/15008/stat): 15008 (minisat+_64-bit) R 15004 15004 30740 0 -1 0 15734 0 0 0 111825 95 0 0 25 0 1 0 1793695854 67309568 15378 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15008/statm): 16433 15378 145 145 0 16288 0
[pid=15008] vsize: 65732
Current children cumulated CPU time (s) 1119.21
Current children cumulated vsize (Kb) 67856

[startup+1130.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15008
Raw data (/proc/15004/stat): 15004 (minisat+_script) S 15003 15004 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793695849 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15004/statm): 531 226 485 147 0 384 0
[pid=15004] vsize: 2124
Raw data (/proc/15008/stat): 15008 (minisat+_64-bit) R 15004 15004 30740 0 -1 0 15734 0 0 0 112825 95 0 0 25 0 1 0 1793695854 67309568 15378 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15008/statm): 16433 15378 145 145 0 16288 0
[pid=15008] vsize: 65732
Current children cumulated CPU time (s) 1129.21
Current children cumulated vsize (Kb) 67856

[startup+1140.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15008
Raw data (/proc/15004/stat): 15004 (minisat+_script) S 15003 15004 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793695849 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15004/statm): 531 226 485 147 0 384 0
[pid=15004] vsize: 2124
Raw data (/proc/15008/stat): 15008 (minisat+_64-bit) R 15004 15004 30740 0 -1 0 15734 0 0 0 113825 95 0 0 25 0 1 0 1793695854 67309568 15378 4294967295 134512640 135094434 3221224432 3221223088 134558405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15008/statm): 16433 15378 145 145 0 16288 0
[pid=15008] vsize: 65732
Current children cumulated CPU time (s) 1139.21
Current children cumulated vsize (Kb) 67856

[startup+1150.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15008
Raw data (/proc/15004/stat): 15004 (minisat+_script) S 15003 15004 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793695849 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15004/statm): 531 226 485 147 0 384 0
[pid=15004] vsize: 2124
Raw data (/proc/15008/stat): 15008 (minisat+_64-bit) R 15004 15004 30740 0 -1 0 15735 0 0 0 114825 95 0 0 25 0 1 0 1793695854 67309568 15379 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15008/statm): 16433 15379 145 145 0 16288 0
[pid=15008] vsize: 65732
Current children cumulated CPU time (s) 1149.21
Current children cumulated vsize (Kb) 67856

[startup+1160.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15008
Raw data (/proc/15004/stat): 15004 (minisat+_script) S 15003 15004 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793695849 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15004/statm): 531 226 485 147 0 384 0
[pid=15004] vsize: 2124
Raw data (/proc/15008/stat): 15008 (minisat+_64-bit) R 15004 15004 30740 0 -1 0 15735 0 0 0 115826 95 0 0 25 0 1 0 1793695854 67309568 15379 4294967295 134512640 135094434 3221224432 3221223024 134556862 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15008/statm): 16433 15379 145 145 0 16288 0
[pid=15008] vsize: 65732
Current children cumulated CPU time (s) 1159.22
Current children cumulated vsize (Kb) 67856

[startup+1170.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15008
Raw data (/proc/15004/stat): 15004 (minisat+_script) S 15003 15004 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793695849 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15004/statm): 531 226 485 147 0 384 0
[pid=15004] vsize: 2124
Raw data (/proc/15008/stat): 15008 (minisat+_64-bit) R 15004 15004 30740 0 -1 0 15735 0 0 0 116826 95 0 0 25 0 1 0 1793695854 67309568 15379 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15008/statm): 16433 15379 145 145 0 16288 0
[pid=15008] vsize: 65732
Current children cumulated CPU time (s) 1169.22
Current children cumulated vsize (Kb) 67856

[startup+1180.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15008
Raw data (/proc/15004/stat): 15004 (minisat+_script) S 15003 15004 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793695849 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15004/statm): 531 226 485 147 0 384 0
[pid=15004] vsize: 2124
Raw data (/proc/15008/stat): 15008 (minisat+_64-bit) R 15004 15004 30740 0 -1 0 15735 0 0 0 117826 95 0 0 25 0 1 0 1793695854 67309568 15379 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15008/statm): 16433 15379 145 145 0 16288 0
[pid=15008] vsize: 65732
Current children cumulated CPU time (s) 1179.22
Current children cumulated vsize (Kb) 67856

[startup+1190.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15008
Raw data (/proc/15004/stat): 15004 (minisat+_script) S 15003 15004 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793695849 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15004/statm): 531 226 485 147 0 384 0
[pid=15004] vsize: 2124
Raw data (/proc/15008/stat): 15008 (minisat+_64-bit) R 15004 15004 30740 0 -1 0 15735 0 0 0 118826 95 0 0 25 0 1 0 1793695854 67309568 15379 4294967295 134512640 135094434 3221224432 3221223056 134557717 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15008/statm): 16433 15379 145 145 0 16288 0
[pid=15008] vsize: 65732
Current children cumulated CPU time (s) 1189.22
Current children cumulated vsize (Kb) 67856

[startup+1200.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15008
Raw data (/proc/15004/stat): 15004 (minisat+_script) S 15003 15004 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793695849 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15004/statm): 531 226 485 147 0 384 0
[pid=15004] vsize: 2124
Raw data (/proc/15008/stat): 15008 (minisat+_64-bit) R 15004 15004 30740 0 -1 0 15735 0 0 0 119826 95 0 0 25 0 1 0 1793695854 67309568 15379 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15008/statm): 16433 15379 145 145 0 16288 0
[pid=15008] vsize: 65732
Current children cumulated CPU time (s) 1199.22
Current children cumulated vsize (Kb) 67856

[startup+1210.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15008
Raw data (/proc/15004/stat): 15004 (minisat+_script) S 15003 15004 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793695849 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15004/statm): 531 226 485 147 0 384 0
[pid=15004] vsize: 2124
Raw data (/proc/15008/stat): 15008 (minisat+_64-bit) R 15004 15004 30740 0 -1 0 15735 0 0 0 120826 95 0 0 25 0 1 0 1793695854 67309568 15379 4294967295 134512640 135094434 3221224432 3221223024 134556812 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15008/statm): 16433 15379 145 145 0 16288 0
[pid=15008] 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.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15008
Raw data (/proc/15004/stat): 15004 (minisat+_script) S 15003 15004 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793695849 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15004/statm): 531 226 485 147 0 384 0
[pid=15004] vsize: 2124
Raw data (/proc/15008/stat): 15008 (minisat+_64-bit) R 15004 15004 30740 0 -1 0 15735 0 0 0 120826 95 0 0 25 0 1 0 1793695854 67309568 15379 4294967295 134512640 135094434 3221224432 3221223120 134554685 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15008/statm): 16433 15379 145 145 0 16288 0
[pid=15008] vsize: 65732
Current children cumulated CPU time (s) 1209.22
Current children cumulated vsize (Kb) 67856

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

Child status: 10
Real time (s): 1210.15
CPU time (s): 1209.26
CPU user time (s): 1208.27
CPU system time (s): 0.98585
CPU usage (%): 99.9266
Max. virtual memory (cumulated for all children) (Kb): 67856

Verifier Data

ERROR: no interpretation found !