Some explanations

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

General information on the benchmark

Namemps-v2-13-7/MIPLIB/miplib/normalized-mps-v2-13-7-p0282.opb
MD5SUMa733e9fa1e4e3ac90baf85249f7c3e9a
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.5803
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 6100

Launcher Data

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

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        922128 kB
Buffers:          5164 kB
Cached:          78336 kB
SwapCached:        820 kB
Active:          18908 kB
Inactive:        67208 kB
HighTotal:      131008 kB
HighFree:        48496 kB
LowTotal:       903652 kB
LowFree:        873632 kB
SwapTotal:     2097892 kB
SwapFree:      2096508 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5640 kB
Slab:            20600 kB
Committed_AS:    64168 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-09-20 03:38:44 (client local time) WITH STATUS 10 IN 1209.27 SECONDS
stats: 3259 7 1209.27 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 % |

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

[startup+10.0033 s]
Raw data (loadavg): 0.93 0.95 0.90 2/57 28421
Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28417/statm): 531 226 485 147 0 384 0
[pid=28417] vsize: 2124
Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 8650 0 0 0 927 33 0 0 25 0 1 0 1855238669 38129664 8294 4294967295 134512640 135094434 3221224432 3221221892 134677077 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28421/statm): 9309 8294 145 145 0 9164 0
[pid=28421] vsize: 37236
Current children cumulated CPU time (s) 9.6
Current children cumulated vsize (Kb) 39360

[startup+20.005 s]
Raw data (loadavg): 0.94 0.96 0.91 2/57 28421
Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28417/statm): 531 226 485 147 0 384 0
[pid=28417] vsize: 2124
Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 8720 0 0 0 1926 33 0 0 25 0 1 0 1855238669 38387712 8364 4294967295 134512640 135094434 3221224432 3221223056 134557717 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28421/statm): 9372 8364 145 145 0 9227 0
[pid=28421] vsize: 37488
Current children cumulated CPU time (s) 19.59
Current children cumulated vsize (Kb) 39612

[startup+30.0058 s]
Raw data (loadavg): 0.95 0.96 0.91 2/57 28421
Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28417/statm): 531 226 485 147 0 384 0
[pid=28417] vsize: 2124
Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 8795 0 0 0 2926 34 0 0 25 0 1 0 1855238669 38682624 8439 4294967295 134512640 135094434 3221224432 3221223056 134557565 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28421/statm): 9444 8439 145 145 0 9299 0
[pid=28421] vsize: 37776
Current children cumulated CPU time (s) 29.6
Current children cumulated vsize (Kb) 39900

[startup+40.0065 s]
Raw data (loadavg): 0.95 0.96 0.91 2/57 28421
Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28417/statm): 531 226 485 147 0 384 0
[pid=28417] vsize: 2124
Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 8849 0 0 0 3924 34 0 0 25 0 1 0 1855238669 38899712 8493 4294967295 134512640 135094434 3221224432 3221223056 134557650 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28421/statm): 9497 8493 145 145 0 9352 0
[pid=28421] vsize: 37988
Current children cumulated CPU time (s) 39.58
Current children cumulated vsize (Kb) 40112

[startup+50.0082 s]
Raw data (loadavg): 0.96 0.96 0.91 2/57 28421
Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28417/statm): 531 226 485 147 0 384 0
[pid=28417] vsize: 2124
Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 8930 0 0 0 4923 35 0 0 25 0 1 0 1855238669 39251968 8574 4294967295 134512640 135094434 3221224432 3221223088 134558405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28421/statm): 9583 8574 145 145 0 9438 0
[pid=28421] vsize: 38332
Current children cumulated CPU time (s) 49.58
Current children cumulated vsize (Kb) 40456

[startup+60.0089 s]
Raw data (loadavg): 0.97 0.96 0.91 2/57 28421
Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28417/statm): 531 226 485 147 0 384 0
[pid=28417] vsize: 2124
Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 8974 0 0 0 5922 36 0 0 25 0 1 0 1855238669 39424000 8618 4294967295 134512640 135094434 3221224432 3221223092 134553530 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28421/statm): 9625 8618 145 145 0 9480 0
[pid=28421] vsize: 38500
Current children cumulated CPU time (s) 59.58
Current children cumulated vsize (Kb) 40624

[startup+70.0106 s]
Raw data (loadavg): 0.97 0.96 0.91 2/57 28421
Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28417/statm): 531 226 485 147 0 384 0
[pid=28417] vsize: 2124
Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 9059 0 0 0 6921 36 0 0 25 0 1 0 1855238669 39768064 8703 4294967295 134512640 135094434 3221224432 3221223092 134553494 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28421/statm): 9709 8703 145 145 0 9564 0
[pid=28421] vsize: 38836
Current children cumulated CPU time (s) 69.57
Current children cumulated vsize (Kb) 40960

[startup+80.0114 s]
Raw data (loadavg): 0.98 0.96 0.91 2/57 28421
Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28417/statm): 531 226 485 147 0 384 0
[pid=28417] vsize: 2124
Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 9191 0 0 0 7918 38 0 0 25 0 1 0 1855238669 40296448 8835 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28421/statm): 9838 8835 145 145 0 9693 0
[pid=28421] vsize: 39352
Current children cumulated CPU time (s) 79.56
Current children cumulated vsize (Kb) 41476

[startup+90.0121 s]
Raw data (loadavg): 0.98 0.96 0.91 2/57 28421
Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28417/statm): 531 226 485 147 0 384 0
[pid=28417] vsize: 2124
Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 9252 0 0 0 8918 38 0 0 25 0 1 0 1855238669 40546304 8896 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28421/statm): 9899 8896 145 145 0 9754 0
[pid=28421] vsize: 39596
Current children cumulated CPU time (s) 89.56
Current children cumulated vsize (Kb) 41720

[startup+100.013 s]
Raw data (loadavg): 0.98 0.96 0.91 2/57 28421
Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28417/statm): 531 226 485 147 0 384 0
[pid=28417] vsize: 2124
Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 9315 0 0 0 9916 40 0 0 25 0 1 0 1855238669 40792064 8959 4294967295 134512640 135094434 3221224432 3221223068 134557560 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28421/statm): 9959 8959 145 145 0 9814 0
[pid=28421] vsize: 39836
Current children cumulated CPU time (s) 99.56
Current children cumulated vsize (Kb) 41960

[startup+110.014 s]
Raw data (loadavg): 0.98 0.96 0.91 2/57 28421
Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28417/statm): 531 226 485 147 0 384 0
[pid=28417] vsize: 2124
Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 9367 0 0 0 10915 41 0 0 25 0 1 0 1855238669 41054208 9011 4294967295 134512640 135094434 3221224432 3221223088 134557835 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28421/statm): 10023 9011 145 145 0 9878 0
[pid=28421] vsize: 40092
Current children cumulated CPU time (s) 109.56
Current children cumulated vsize (Kb) 42216

[startup+120.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28421
Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28417/statm): 531 226 485 147 0 384 0
[pid=28417] vsize: 2124
Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 9447 0 0 0 11913 42 0 0 25 0 1 0 1855238669 41369600 9091 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28421/statm): 10100 9091 145 145 0 9955 0
[pid=28421] vsize: 40400
Current children cumulated CPU time (s) 119.55
Current children cumulated vsize (Kb) 42524

[startup+130.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28421
Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28417/statm): 531 226 485 147 0 384 0
[pid=28417] vsize: 2124
Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 9531 0 0 0 12912 43 0 0 25 0 1 0 1855238669 41709568 9175 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28421/statm): 10183 9175 145 145 0 10038 0
[pid=28421] vsize: 40732
Current children cumulated CPU time (s) 129.55
Current children cumulated vsize (Kb) 42856

[startup+140.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28421
Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28417/statm): 531 226 485 147 0 384 0
[pid=28417] vsize: 2124
Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 9614 0 0 0 13910 43 0 0 25 0 1 0 1855238669 42049536 9258 4294967295 134512640 135094434 3221224432 3221221280 134677307 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28421/statm): 10266 9258 145 145 0 10121 0
[pid=28421] vsize: 41064
Current children cumulated CPU time (s) 139.53
Current children cumulated vsize (Kb) 43188

[startup+150.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28421
Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28417/statm): 531 226 485 147 0 384 0
[pid=28417] vsize: 2124
Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 9648 0 0 0 14909 44 0 0 25 0 1 0 1855238669 42160128 9292 4294967295 134512640 135094434 3221224432 3221223064 134557561 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28421/statm): 10293 9292 145 145 0 10148 0
[pid=28421] vsize: 41172
Current children cumulated CPU time (s) 149.53
Current children cumulated vsize (Kb) 43296

[startup+160.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28421
Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28417/statm): 531 226 485 147 0 384 0
[pid=28417] vsize: 2124
Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 9744 0 0 0 15907 45 0 0 25 0 1 0 1855238669 42532864 9388 4294967295 134512640 135094434 3221224432 3221223104 134556468 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28421/statm): 10384 9388 145 145 0 10239 0
[pid=28421] vsize: 41536
Current children cumulated CPU time (s) 159.52
Current children cumulated vsize (Kb) 43660

[startup+170.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28421
Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28417/statm): 531 226 485 147 0 384 0
[pid=28417] vsize: 2124
Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 9873 0 0 0 16905 45 0 0 25 0 1 0 1855238669 43057152 9517 4294967295 134512640 135094434 3221224432 3221223088 134558411 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28421/statm): 10512 9517 145 145 0 10367 0
[pid=28421] vsize: 42048
Current children cumulated CPU time (s) 169.5
Current children cumulated vsize (Kb) 44172

[startup+180.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28421
Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28417/statm): 531 226 485 147 0 384 0
[pid=28417] vsize: 2124
Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 9951 0 0 0 17903 46 0 0 25 0 1 0 1855238669 43372544 9595 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28421/statm): 10589 9595 145 145 0 10444 0
[pid=28421] vsize: 42356
Current children cumulated CPU time (s) 179.49
Current children cumulated vsize (Kb) 44480

[startup+190.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28421
Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28417/statm): 531 226 485 147 0 384 0
[pid=28417] vsize: 2124
Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 10080 0 0 0 18902 47 0 0 25 0 1 0 1855238669 43888640 9724 4294967295 134512640 135094434 3221224432 3221222256 134677049 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28421/statm): 10715 9724 145 145 0 10570 0
[pid=28421] vsize: 42860
Current children cumulated CPU time (s) 189.49
Current children cumulated vsize (Kb) 44984

[startup+200.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28421
Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28417/statm): 531 226 485 147 0 384 0
[pid=28417] vsize: 2124
Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 10149 0 0 0 19902 47 0 0 25 0 1 0 1855238669 44298240 9793 4294967295 134512640 135094434 3221224432 3221223056 134557696 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28421/statm): 10815 9793 145 145 0 10670 0
[pid=28421] vsize: 43260
Current children cumulated CPU time (s) 199.49
Current children cumulated vsize (Kb) 45384

[startup+210.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28421
Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28417/statm): 531 226 485 147 0 384 0
[pid=28417] vsize: 2124
Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 10213 0 0 0 20901 48 0 0 25 0 1 0 1855238669 44556288 9857 4294967295 134512640 135094434 3221224432 3221223056 134562104 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28421/statm): 10878 9857 145 145 0 10733 0
[pid=28421] vsize: 43512
Current children cumulated CPU time (s) 209.49
Current children cumulated vsize (Kb) 45636

[startup+220.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28421
Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28417/statm): 531 226 485 147 0 384 0
[pid=28417] vsize: 2124
Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 10290 0 0 0 21900 49 0 0 25 0 1 0 1855238669 44879872 9934 4294967295 134512640 135094434 3221224432 3221223024 134557016 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28421/statm): 10957 9934 145 145 0 10812 0
[pid=28421] vsize: 43828
Current children cumulated CPU time (s) 219.49
Current children cumulated vsize (Kb) 45952

[startup+230.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28421
Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28417/statm): 531 226 485 147 0 384 0
[pid=28417] vsize: 2124
Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 10365 0 0 0 22900 49 0 0 25 0 1 0 1855238669 45277184 10009 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28421/statm): 11054 10009 145 145 0 10909 0
[pid=28421] vsize: 44216
Current children cumulated CPU time (s) 229.49
Current children cumulated vsize (Kb) 46340

[startup+240.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28421
Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28417/statm): 531 226 485 147 0 384 0
[pid=28417] vsize: 2124
Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 10406 0 0 0 23899 49 0 0 25 0 1 0 1855238669 45441024 10050 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28421/statm): 11094 10050 145 145 0 10949 0
[pid=28421] vsize: 44376
Current children cumulated CPU time (s) 239.48
Current children cumulated vsize (Kb) 46500

[startup+250.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28421
Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28417/statm): 531 226 485 147 0 384 0
[pid=28417] vsize: 2124
Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 10470 0 0 0 24898 50 0 0 19 0 1 0 1855238669 45699072 10114 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28421/statm): 11157 10114 145 145 0 11012 0
[pid=28421] vsize: 44628
Current children cumulated CPU time (s) 249.48
Current children cumulated vsize (Kb) 46752

[startup+260.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28421
Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28417/statm): 531 226 485 147 0 384 0
[pid=28417] vsize: 2124
Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 10566 0 0 0 25896 51 0 0 25 0 1 0 1855238669 46092288 10210 4294967295 134512640 135094434 3221224432 3221223056 134557717 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28421/statm): 11253 10210 145 145 0 11108 0
[pid=28421] vsize: 45012
Current children cumulated CPU time (s) 259.47
Current children cumulated vsize (Kb) 47136

[startup+270.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28421
Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28417/statm): 531 226 485 147 0 384 0
[pid=28417] vsize: 2124
Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 10688 0 0 0 26895 52 0 0 25 0 1 0 1855238669 46579712 10332 4294967295 134512640 135094434 3221224432 3221223056 134557577 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28421/statm): 11372 10332 145 145 0 11227 0
[pid=28421] vsize: 45488
Current children cumulated CPU time (s) 269.47
Current children cumulated vsize (Kb) 47612

[startup+280.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28421
Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28417/statm): 531 226 485 147 0 384 0
[pid=28417] vsize: 2124
Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 10760 0 0 0 27894 52 0 0 25 0 1 0 1855238669 46870528 10404 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28421/statm): 11443 10404 145 145 0 11298 0
[pid=28421] vsize: 45772
Current children cumulated CPU time (s) 279.46
Current children cumulated vsize (Kb) 47896

[startup+290.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28421
Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28417/statm): 531 226 485 147 0 384 0
[pid=28417] vsize: 2124
Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 10851 0 0 0 28893 53 0 0 25 0 1 0 1855238669 47243264 10495 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28421/statm): 11534 10495 145 145 0 11389 0
[pid=28421] vsize: 46136
Current children cumulated CPU time (s) 289.46
Current children cumulated vsize (Kb) 48260

[startup+300.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28421
Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28417/statm): 531 226 485 147 0 384 0
[pid=28417] vsize: 2124
Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 10940 0 0 0 29892 53 0 0 25 0 1 0 1855238669 47607808 10584 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28421/statm): 11623 10584 145 145 0 11478 0
[pid=28421] vsize: 46492
Current children cumulated CPU time (s) 299.45
Current children cumulated vsize (Kb) 48616

[startup+310.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28421
Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28417/statm): 531 226 485 147 0 384 0
[pid=28417] vsize: 2124
Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 11020 0 0 0 30892 53 0 0 25 0 1 0 1855238669 47927296 10664 4294967295 134512640 135094434 3221224432 3221223056 134557648 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28421/statm): 11701 10664 145 145 0 11556 0
[pid=28421] vsize: 46804
Current children cumulated CPU time (s) 309.45
Current children cumulated vsize (Kb) 48928

[startup+320.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28421
Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28417/statm): 531 226 485 147 0 384 0
[pid=28417] vsize: 2124
Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 11130 0 0 0 31890 54 0 0 25 0 1 0 1855238669 48373760 10774 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28421/statm): 11810 10774 145 145 0 11665 0
[pid=28421] vsize: 47240
Current children cumulated CPU time (s) 319.44
Current children cumulated vsize (Kb) 49364

[startup+330.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28421
Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28417/statm): 531 226 485 147 0 384 0
[pid=28417] vsize: 2124
Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 11215 0 0 0 32889 55 0 0 25 0 1 0 1855238669 48717824 10859 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28421/statm): 11894 10859 145 145 0 11749 0
[pid=28421] vsize: 47576
Current children cumulated CPU time (s) 329.44
Current children cumulated vsize (Kb) 49700

[startup+340.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28421
Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28417/statm): 531 226 485 147 0 384 0
[pid=28417] vsize: 2124
Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 11312 0 0 0 33887 56 0 0 25 0 1 0 1855238669 49111040 10956 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28421/statm): 11990 10956 145 145 0 11845 0
[pid=28421] vsize: 47960
Current children cumulated CPU time (s) 339.43
Current children cumulated vsize (Kb) 50084

[startup+350.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28421
Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28417/statm): 531 226 485 147 0 384 0
[pid=28417] vsize: 2124
Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 11365 0 0 0 34886 57 0 0 25 0 1 0 1855238669 49328128 11009 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28421/statm): 12043 11009 145 145 0 11898 0
[pid=28421] vsize: 48172
Current children cumulated CPU time (s) 349.43
Current children cumulated vsize (Kb) 50296

[startup+360.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28421
Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28417/statm): 531 226 485 147 0 384 0
[pid=28417] vsize: 2124
Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 11425 0 0 0 35885 57 0 0 25 0 1 0 1855238669 49569792 11069 4294967295 134512640 135094434 3221224432 3221223240 134553433 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28421/statm): 12102 11069 145 145 0 11957 0
[pid=28421] vsize: 48408
Current children cumulated CPU time (s) 359.42
Current children cumulated vsize (Kb) 50532

[startup+370.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28421
Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28417/statm): 531 226 485 147 0 384 0
[pid=28417] vsize: 2124
Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 11460 0 0 0 36884 58 0 0 25 0 1 0 1855238669 49704960 11104 4294967295 134512640 135094434 3221224432 3221223104 134556323 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28421/statm): 12135 11104 145 145 0 11990 0
[pid=28421] vsize: 48540
Current children cumulated CPU time (s) 369.42
Current children cumulated vsize (Kb) 50664

[startup+380.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28421
Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28417/statm): 531 226 485 147 0 384 0
[pid=28417] vsize: 2124
Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 11571 0 0 0 37881 60 0 0 25 0 1 0 1855238669 50155520 11215 4294967295 134512640 135094434 3221224432 3221223024 134557334 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28421/statm): 12245 11215 145 145 0 12100 0
[pid=28421] vsize: 48980
Current children cumulated CPU time (s) 379.41
Current children cumulated vsize (Kb) 51104

[startup+390.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28421
Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28417/statm): 531 226 485 147 0 384 0
[pid=28417] vsize: 2124
Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 11648 0 0 0 38879 61 0 0 25 0 1 0 1855238669 50466816 11292 4294967295 134512640 135094434 3221224432 3221223088 134557945 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28421/statm): 12321 11292 145 145 0 12176 0
[pid=28421] vsize: 49284
Current children cumulated CPU time (s) 389.4
Current children cumulated vsize (Kb) 51408

[startup+400.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28421
Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28417/statm): 531 226 485 147 0 384 0
[pid=28417] vsize: 2124
Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 11764 0 0 0 39877 62 0 0 25 0 1 0 1855238669 50937856 11408 4294967295 134512640 135094434 3221224432 3221223220 134553515 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28421/statm): 12436 11408 145 145 0 12291 0
[pid=28421] vsize: 49744
Current children cumulated CPU time (s) 399.39
Current children cumulated vsize (Kb) 51868

[startup+410.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28421
Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28417/statm): 531 226 485 147 0 384 0
[pid=28417] vsize: 2124
Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 11788 0 0 0 40876 63 0 0 25 0 1 0 1855238669 51032064 11432 4294967295 134512640 135094434 3221224432 3221223064 134557561 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28421/statm): 12459 11432 145 145 0 12314 0
[pid=28421] vsize: 49836
Current children cumulated CPU time (s) 409.39
Current children cumulated vsize (Kb) 51960

[startup+420.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28421
Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28417/statm): 531 226 485 147 0 384 0
[pid=28417] vsize: 2124
Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 11877 0 0 0 41875 63 0 0 25 0 1 0 1855238669 51392512 11521 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28421/statm): 12547 11521 145 145 0 12402 0
[pid=28421] vsize: 50188
Current children cumulated CPU time (s) 419.38
Current children cumulated vsize (Kb) 52312

[startup+430.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28421
Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28417/statm): 531 226 485 147 0 384 0
[pid=28417] vsize: 2124
Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 11958 0 0 0 42874 64 0 0 25 0 1 0 1855238669 51720192 11602 4294967295 134512640 135094434 3221224432 3221223024 134557401 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28421/statm): 12627 11602 145 145 0 12482 0
[pid=28421] vsize: 50508
Current children cumulated CPU time (s) 429.38
Current children cumulated vsize (Kb) 52632

[startup+440.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28421
Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28417/statm): 531 226 485 147 0 384 0
[pid=28417] vsize: 2124
Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 12021 0 0 0 43873 65 0 0 25 0 1 0 1855238669 51974144 11665 4294967295 134512640 135094434 3221224432 3221223024 134556864 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28421/statm): 12689 11665 145 145 0 12544 0
[pid=28421] vsize: 50756
Current children cumulated CPU time (s) 439.38
Current children cumulated vsize (Kb) 52880

[startup+450.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28421
Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28417/statm): 531 226 485 147 0 384 0
[pid=28417] vsize: 2124
Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 12058 0 0 0 44872 65 0 0 25 0 1 0 1855238669 52125696 11702 4294967295 134512640 135094434 3221224432 3221223056 134557675 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28421/statm): 12726 11702 145 145 0 12581 0
[pid=28421] vsize: 50904
Current children cumulated CPU time (s) 449.37
Current children cumulated vsize (Kb) 53028

[startup+460.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28421
Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28417/statm): 531 226 485 147 0 384 0
[pid=28417] vsize: 2124
Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 12111 0 0 0 45871 65 0 0 25 0 1 0 1855238669 52338688 11755 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28421/statm): 12778 11755 145 145 0 12633 0
[pid=28421] vsize: 51112
Current children cumulated CPU time (s) 459.36
Current children cumulated vsize (Kb) 53236

[startup+470.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28421
Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28417/statm): 531 226 485 147 0 384 0
[pid=28417] vsize: 2124
Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 12194 0 0 0 46870 66 0 0 25 0 1 0 1855238669 52674560 11838 4294967295 134512640 135094434 3221224432 3221223024 134556862 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28421/statm): 12860 11838 145 145 0 12715 0
[pid=28421] vsize: 51440
Current children cumulated CPU time (s) 469.36
Current children cumulated vsize (Kb) 53564

[startup+480.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28421
Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28417/statm): 531 226 485 147 0 384 0
[pid=28417] vsize: 2124
Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 12275 0 0 0 47870 66 0 0 25 0 1 0 1855238669 53002240 11919 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28421/statm): 12940 11919 145 145 0 12795 0
[pid=28421] vsize: 51760
Current children cumulated CPU time (s) 479.36
Current children cumulated vsize (Kb) 53884

[startup+490.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28421
Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28417/statm): 531 226 485 147 0 384 0
[pid=28417] vsize: 2124
Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 12351 0 0 0 48869 67 0 0 25 0 1 0 1855238669 53313536 11995 4294967295 134512640 135094434 3221224432 3221223024 134556868 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28421/statm): 13016 11995 145 145 0 12871 0
[pid=28421] vsize: 52064
Current children cumulated CPU time (s) 489.36
Current children cumulated vsize (Kb) 54188

[startup+500.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28421
Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28417/statm): 531 226 485 147 0 384 0
[pid=28417] vsize: 2124
Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 12442 0 0 0 49867 68 0 0 25 0 1 0 1855238669 53686272 12086 4294967295 134512640 135094434 3221224432 3221223064 134557561 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28421/statm): 13107 12086 145 145 0 12962 0
[pid=28421] vsize: 52428
Current children cumulated CPU time (s) 499.35
Current children cumulated vsize (Kb) 54552

[startup+510.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28421
Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28417/statm): 531 226 485 147 0 384 0
[pid=28417] vsize: 2124
Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 12516 0 0 0 50867 68 0 0 25 0 1 0 1855238669 53977088 12160 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28421/statm): 13178 12160 145 145 0 13033 0
[pid=28421] vsize: 52712
Current children cumulated CPU time (s) 509.35
Current children cumulated vsize (Kb) 54836

[startup+520.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28421
Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28417/statm): 531 226 485 147 0 384 0
[pid=28417] vsize: 2124
Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 12586 0 0 0 51865 69 0 0 25 0 1 0 1855238669 54521856 12230 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28421/statm): 13311 12230 145 145 0 13166 0
[pid=28421] vsize: 53244
Current children cumulated CPU time (s) 519.34
Current children cumulated vsize (Kb) 55368

[startup+530.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28421
Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28417/statm): 531 226 485 147 0 384 0
[pid=28417] vsize: 2124
Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 12640 0 0 0 52864 69 0 0 25 0 1 0 1855238669 54738944 12284 4294967295 134512640 135094434 3221224432 3221223088 134558210 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28421/statm): 13364 12284 145 145 0 13219 0
[pid=28421] vsize: 53456
Current children cumulated CPU time (s) 529.33
Current children cumulated vsize (Kb) 55580

[startup+540.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28421
Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28417/statm): 531 226 485 147 0 384 0
[pid=28417] vsize: 2124
Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 12683 0 0 0 53863 70 0 0 25 0 1 0 1855238669 54915072 12327 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28421/statm): 13407 12327 145 145 0 13262 0
[pid=28421] vsize: 53628
Current children cumulated CPU time (s) 539.33
Current children cumulated vsize (Kb) 55752

[startup+550.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28421
Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28417/statm): 531 226 485 147 0 384 0
[pid=28417] vsize: 2124
Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 12729 0 0 0 54863 70 0 0 25 0 1 0 1855238669 55099392 12373 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28421/statm): 13452 12373 145 145 0 13307 0
[pid=28421] vsize: 53808
Current children cumulated CPU time (s) 549.33
Current children cumulated vsize (Kb) 55932

[startup+560.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28421
Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28417/statm): 531 226 485 147 0 384 0
[pid=28417] vsize: 2124
Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 12792 0 0 0 55863 70 0 0 25 0 1 0 1855238669 55353344 12436 4294967295 134512640 135094434 3221224432 3221223136 134559017 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28421/statm): 13514 12436 145 145 0 13369 0
[pid=28421] vsize: 54056
Current children cumulated CPU time (s) 559.33
Current children cumulated vsize (Kb) 56180

[startup+570.051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28421
Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28417/statm): 531 226 485 147 0 384 0
[pid=28417] vsize: 2124
Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 12833 0 0 0 56863 71 0 0 25 0 1 0 1855238669 55521280 12477 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28421/statm): 13555 12477 145 145 0 13410 0
[pid=28421] vsize: 54220
Current children cumulated CPU time (s) 569.34
Current children cumulated vsize (Kb) 56344

[startup+580.052 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28421
Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28417/statm): 531 226 485 147 0 384 0
[pid=28417] vsize: 2124
Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 12913 0 0 0 57862 71 0 0 25 0 1 0 1855238669 55844864 12557 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28421/statm): 13634 12557 145 145 0 13489 0
[pid=28421] vsize: 54536
Current children cumulated CPU time (s) 579.33
Current children cumulated vsize (Kb) 56660

[startup+590.052 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28421
Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28417/statm): 531 226 485 147 0 384 0
[pid=28417] vsize: 2124
Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 13012 0 0 0 58860 72 0 0 25 0 1 0 1855238669 56233984 12656 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28421/statm): 13729 12656 145 145 0 13584 0
[pid=28421] vsize: 54916
Current children cumulated CPU time (s) 589.32
Current children cumulated vsize (Kb) 57040

[startup+600.054 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28421
Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28417/statm): 531 226 485 147 0 384 0
[pid=28417] vsize: 2124
Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 13076 0 0 0 59860 72 0 0 25 0 1 0 1855238669 56492032 12720 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28421/statm): 13792 12720 145 145 0 13647 0
[pid=28421] vsize: 55168
Current children cumulated CPU time (s) 599.32
Current children cumulated vsize (Kb) 57292

[startup+610.054 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28421
Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28417/statm): 531 226 485 147 0 384 0
[pid=28417] vsize: 2124
Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 13161 0 0 0 60858 73 0 0 25 0 1 0 1855238669 56836096 12805 4294967295 134512640 135094434 3221224432 3221223088 134558402 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28421/statm): 13876 12805 145 145 0 13731 0
[pid=28421] vsize: 55504
Current children cumulated CPU time (s) 609.31
Current children cumulated vsize (Kb) 57628

[startup+620.055 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28421
Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28417/statm): 531 226 485 147 0 384 0
[pid=28417] vsize: 2124
Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 13221 0 0 0 61858 74 0 0 25 0 1 0 1855238669 57081856 12865 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28421/statm): 13936 12865 145 145 0 13791 0
[pid=28421] vsize: 55744
Current children cumulated CPU time (s) 619.32
Current children cumulated vsize (Kb) 57868

[startup+630.056 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28421
Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28417/statm): 531 226 485 147 0 384 0
[pid=28417] vsize: 2124
Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 13299 0 0 0 62857 74 0 0 25 0 1 0 1855238669 57401344 12943 4294967295 134512640 135094434 3221224432 3221223044 134563055 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28421/statm): 14014 12943 145 145 0 13869 0
[pid=28421] vsize: 56056
Current children cumulated CPU time (s) 629.31
Current children cumulated vsize (Kb) 58180

[startup+640.056 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28421
Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28417/statm): 531 226 485 147 0 384 0
[pid=28417] vsize: 2124
Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 13384 0 0 0 63856 74 0 0 25 0 1 0 1855238669 57741312 13028 4294967295 134512640 135094434 3221224432 3221223024 134557398 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28421/statm): 14097 13028 145 145 0 13952 0
[pid=28421] vsize: 56388
Current children cumulated CPU time (s) 639.3
Current children cumulated vsize (Kb) 58512

[startup+650.057 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28421
Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28417/statm): 531 226 485 147 0 384 0
[pid=28417] vsize: 2124
Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 13437 0 0 0 64856 75 0 0 25 0 1 0 1855238669 57954304 13081 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28421/statm): 14149 13081 145 145 0 14004 0
[pid=28421] vsize: 56596
Current children cumulated CPU time (s) 649.31
Current children cumulated vsize (Kb) 58720

[startup+660.058 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28421
Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28417/statm): 531 226 485 147 0 384 0
[pid=28417] vsize: 2124
Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 13487 0 0 0 65855 75 0 0 25 0 1 0 1855238669 58155008 13131 4294967295 134512640 135094434 3221224432 3221223104 134555953 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28421/statm): 14198 13131 145 145 0 14053 0
[pid=28421] vsize: 56792
Current children cumulated CPU time (s) 659.3
Current children cumulated vsize (Kb) 58916

[startup+670.058 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28421
Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28417/statm): 531 226 485 147 0 384 0
[pid=28417] vsize: 2124
Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 13550 0 0 0 66854 76 0 0 25 0 1 0 1855238669 58413056 13194 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28421/statm): 14261 13194 145 145 0 14116 0
[pid=28421] vsize: 57044
Current children cumulated CPU time (s) 669.3
Current children cumulated vsize (Kb) 59168

[startup+680.059 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28421
Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28417/statm): 531 226 485 147 0 384 0
[pid=28417] vsize: 2124
Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 13578 0 0 0 67854 76 0 0 25 0 1 0 1855238669 58523648 13222 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28421/statm): 14288 13222 145 145 0 14143 0
[pid=28421] vsize: 57152
Current children cumulated CPU time (s) 679.3
Current children cumulated vsize (Kb) 59276

[startup+690.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28421
Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28417/statm): 531 226 485 147 0 384 0
[pid=28417] vsize: 2124
Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) T 28417 28417 2660 0 -1 0 13617 0 0 0 68853 77 0 0 25 0 1 0 1855238669 58683392 13261 4294967295 134512640 135094434 3221224432 3221222796 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/28421/statm): 14327 13261 145 145 0 14182 0
[pid=28421] vsize: 57308
Current children cumulated CPU time (s) 689.3
Current children cumulated vsize (Kb) 59432

[startup+700.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28421
Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28417/statm): 531 226 485 147 0 384 0
[pid=28417] vsize: 2124
Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 13691 0 0 0 69851 78 0 0 25 0 1 0 1855238669 58982400 13335 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28421/statm): 14400 13335 145 145 0 14255 0
[pid=28421] vsize: 57600
Current children cumulated CPU time (s) 699.29
Current children cumulated vsize (Kb) 59724

[startup+710.061 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28421
Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28417/statm): 531 226 485 147 0 384 0
[pid=28417] vsize: 2124
Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 13775 0 0 0 70849 80 0 0 25 0 1 0 1855238669 59322368 13419 4294967295 134512640 135094434 3221224432 3221223088 134558178 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28421/statm): 14483 13419 145 145 0 14338 0
[pid=28421] vsize: 57932
Current children cumulated CPU time (s) 709.29
Current children cumulated vsize (Kb) 60056

[startup+720.062 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28421
Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28417/statm): 531 226 485 147 0 384 0
[pid=28417] vsize: 2124
Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 13838 0 0 0 71848 80 0 0 25 0 1 0 1855238669 59580416 13482 4294967295 134512640 135094434 3221224432 3221223024 134557404 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28421/statm): 14546 13482 145 145 0 14401 0
[pid=28421] vsize: 58184
Current children cumulated CPU time (s) 719.28
Current children cumulated vsize (Kb) 60308

[startup+730.063 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28421
Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28417/statm): 531 226 485 147 0 384 0
[pid=28417] vsize: 2124
Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 13913 0 0 0 72847 81 0 0 25 0 1 0 1855238669 59883520 13557 4294967295 134512640 135094434 3221224432 3221223024 134556802 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28421/statm): 14620 13557 145 145 0 14475 0
[pid=28421] vsize: 58480
Current children cumulated CPU time (s) 729.28
Current children cumulated vsize (Kb) 60604

[startup+740.063 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28421
Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28417/statm): 531 226 485 147 0 384 0
[pid=28417] vsize: 2124
Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 13997 0 0 0 73846 82 0 0 25 0 1 0 1855238669 60227584 13641 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28421/statm): 14704 13641 145 145 0 14559 0
[pid=28421] vsize: 58816
Current children cumulated CPU time (s) 739.28
Current children cumulated vsize (Kb) 60940

[startup+750.065 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28421
Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28417/statm): 531 226 485 147 0 384 0
[pid=28417] vsize: 2124
Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 14082 0 0 0 74844 83 0 0 25 0 1 0 1855238669 60567552 13726 4294967295 134512640 135094434 3221224432 3221223056 134562057 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28421/statm): 14787 13726 145 145 0 14642 0
[pid=28421] vsize: 59148
Current children cumulated CPU time (s) 749.27
Current children cumulated vsize (Kb) 61272

[startup+760.066 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28421
Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28417/statm): 531 226 485 147 0 384 0
[pid=28417] vsize: 2124
Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 14165 0 0 0 75843 84 0 0 25 0 1 0 1855238669 60903424 13809 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28421/statm): 14869 13809 145 145 0 14724 0
[pid=28421] vsize: 59476
Current children cumulated CPU time (s) 759.27
Current children cumulated vsize (Kb) 61600

[startup+770.067 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28421
Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28417/statm): 531 226 485 147 0 384 0
[pid=28417] vsize: 2124
Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 14249 0 0 0 76842 84 0 0 25 0 1 0 1855238669 61247488 13893 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28421/statm): 14953 13893 145 145 0 14808 0
[pid=28421] vsize: 59812
Current children cumulated CPU time (s) 769.26
Current children cumulated vsize (Kb) 61936

[startup+780.068 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28421
Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28417/statm): 531 226 485 147 0 384 0
[pid=28417] vsize: 2124
Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 14310 0 0 0 77841 85 0 0 25 0 1 0 1855238669 61501440 13954 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28421/statm): 15015 13954 145 145 0 14870 0
[pid=28421] vsize: 60060
Current children cumulated CPU time (s) 779.26
Current children cumulated vsize (Kb) 62184

[startup+790.068 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28421
Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28417/statm): 531 226 485 147 0 384 0
[pid=28417] vsize: 2124
Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 14554 0 0 0 78838 86 0 0 25 0 1 0 1855238669 62492672 14198 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28421/statm): 15257 14198 145 145 0 15112 0
[pid=28421] vsize: 61028
Current children cumulated CPU time (s) 789.24
Current children cumulated vsize (Kb) 63152

[startup+800.069 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28421
Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28417/statm): 531 226 485 147 0 384 0
[pid=28417] vsize: 2124
Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 14614 0 0 0 79837 86 0 0 25 0 1 0 1855238669 62734336 14258 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28421/statm): 15316 14258 145 145 0 15171 0
[pid=28421] vsize: 61264
Current children cumulated CPU time (s) 799.23
Current children cumulated vsize (Kb) 63388

[startup+810.069 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28421
Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28417/statm): 531 226 485 147 0 384 0
[pid=28417] vsize: 2124
Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 14700 0 0 0 80835 87 0 0 25 0 1 0 1855238669 63086592 14344 4294967295 134512640 135094434 3221224432 3221223104 134555568 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28421/statm): 15402 14344 145 145 0 15257 0
[pid=28421] vsize: 61608
Current children cumulated CPU time (s) 809.22
Current children cumulated vsize (Kb) 63732

[startup+820.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28421
Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28417/statm): 531 226 485 147 0 384 0
[pid=28417] vsize: 2124
Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 14834 0 0 0 81834 88 0 0 25 0 1 0 1855238669 63655936 14478 4294967295 134512640 135094434 3221224432 3221223024 134556826 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28421/statm): 15541 14478 145 145 0 15396 0
[pid=28421] vsize: 62164
Current children cumulated CPU time (s) 819.22
Current children cumulated vsize (Kb) 64288

[startup+830.071 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28421
Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28417/statm): 531 226 485 147 0 384 0
[pid=28417] vsize: 2124
Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 14980 0 0 0 82832 89 0 0 25 0 1 0 1855238669 64241664 14624 4294967295 134512640 135094434 3221224432 3221223024 134557423 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28421/statm): 15684 14624 145 145 0 15539 0
[pid=28421] vsize: 62736
Current children cumulated CPU time (s) 829.21
Current children cumulated vsize (Kb) 64860

[startup+840.072 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28421
Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28417/statm): 531 226 485 147 0 384 0
[pid=28417] vsize: 2124
Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 15081 0 0 0 83830 90 0 0 25 0 1 0 1855238669 64651264 14725 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28421/statm): 15784 14725 145 145 0 15639 0
[pid=28421] vsize: 63136
Current children cumulated CPU time (s) 839.2
Current children cumulated vsize (Kb) 65260

[startup+850.072 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28421
Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28417/statm): 531 226 485 147 0 384 0
[pid=28417] vsize: 2124
Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 15142 0 0 0 84830 90 0 0 25 0 1 0 1855238669 64897024 14786 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28421/statm): 15844 14786 145 145 0 15699 0
[pid=28421] vsize: 63376
Current children cumulated CPU time (s) 849.2
Current children cumulated vsize (Kb) 65500

[startup+860.073 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28421
Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28417/statm): 531 226 485 147 0 384 0
[pid=28417] vsize: 2124
Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 15228 0 0 0 85828 91 0 0 25 0 1 0 1855238669 65261568 14872 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28421/statm): 15933 14872 145 145 0 15788 0
[pid=28421] vsize: 63732
Current children cumulated CPU time (s) 859.19
Current children cumulated vsize (Kb) 65856

[startup+870.075 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28421
Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28417/statm): 531 226 485 147 0 384 0
[pid=28417] vsize: 2124
Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 15290 0 0 0 86827 91 0 0 25 0 1 0 1855238669 65511424 14934 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28421/statm): 15994 14934 145 145 0 15849 0
[pid=28421] vsize: 63976
Current children cumulated CPU time (s) 869.18
Current children cumulated vsize (Kb) 66100

[startup+880.075 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28421
Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28417/statm): 531 226 485 147 0 384 0
[pid=28417] vsize: 2124
Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 15336 0 0 0 87827 92 0 0 25 0 1 0 1855238669 65695744 14980 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28421/statm): 16039 14980 145 145 0 15894 0
[pid=28421] vsize: 64156
Current children cumulated CPU time (s) 879.19
Current children cumulated vsize (Kb) 66280

[startup+890.076 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28421
Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28417/statm): 531 226 485 147 0 384 0
[pid=28417] vsize: 2124
Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 15396 0 0 0 88826 92 0 0 25 0 1 0 1855238669 65949696 15040 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28421/statm): 16101 15040 145 145 0 15956 0
[pid=28421] vsize: 64404
Current children cumulated CPU time (s) 889.18
Current children cumulated vsize (Kb) 66528

[startup+900.077 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28421
Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28417/statm): 531 226 485 147 0 384 0
[pid=28417] vsize: 2124
Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 15453 0 0 0 89825 93 0 0 25 0 1 0 1855238669 66183168 15097 4294967295 134512640 135094434 3221224432 3221223056 134557574 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28421/statm): 16158 15097 145 145 0 16013 0
[pid=28421] vsize: 64632
Current children cumulated CPU time (s) 899.18
Current children cumulated vsize (Kb) 66756

[startup+910.078 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28421
Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28417/statm): 531 226 485 147 0 384 0
[pid=28417] vsize: 2124
Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 15525 0 0 0 90824 93 0 0 25 0 1 0 1855238669 66473984 15169 4294967295 134512640 135094434 3221224432 3221223088 134558187 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28421/statm): 16229 15169 145 145 0 16084 0
[pid=28421] vsize: 64916
Current children cumulated CPU time (s) 909.17
Current children cumulated vsize (Kb) 67040

[startup+920.078 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28421
Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28417/statm): 531 226 485 147 0 384 0
[pid=28417] vsize: 2124
Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 15599 0 0 0 91823 94 0 0 25 0 1 0 1855238669 66772992 15243 4294967295 134512640 135094434 3221224432 3221223088 134558426 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28421/statm): 16302 15243 145 145 0 16157 0
[pid=28421] vsize: 65208
Current children cumulated CPU time (s) 919.17
Current children cumulated vsize (Kb) 67332

[startup+930.079 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28421
Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28417/statm): 531 226 485 147 0 384 0
[pid=28417] vsize: 2124
Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 15687 0 0 0 92822 95 0 0 25 0 1 0 1855238669 67129344 15331 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28421/statm): 16389 15331 145 145 0 16244 0
[pid=28421] vsize: 65556
Current children cumulated CPU time (s) 929.17
Current children cumulated vsize (Kb) 67680

[startup+940.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28421
Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28417/statm): 531 226 485 147 0 384 0
[pid=28417] vsize: 2124
Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 15731 0 0 0 93821 95 0 0 25 0 1 0 1855238669 67309568 15375 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28421/statm): 16433 15375 145 145 0 16288 0
[pid=28421] vsize: 65732
Current children cumulated CPU time (s) 939.16
Current children cumulated vsize (Kb) 67856

[startup+950.082 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28421
Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28417/statm): 531 226 485 147 0 384 0
[pid=28417] vsize: 2124
Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 15731 0 0 0 94821 95 0 0 25 0 1 0 1855238669 67309568 15375 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28421/statm): 16433 15375 145 145 0 16288 0
[pid=28421] vsize: 65732
Current children cumulated CPU time (s) 949.16
Current children cumulated vsize (Kb) 67856

[startup+960.082 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28421
Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28417/statm): 531 226 485 147 0 384 0
[pid=28417] vsize: 2124
Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 15731 0 0 0 95822 95 0 0 25 0 1 0 1855238669 67309568 15375 4294967295 134512640 135094434 3221224432 3221221456 134676539 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28421/statm): 16433 15375 145 145 0 16288 0
[pid=28421] vsize: 65732
Current children cumulated CPU time (s) 959.17
Current children cumulated vsize (Kb) 67856

[startup+970.083 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28421
Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28417/statm): 531 226 485 147 0 384 0
[pid=28417] vsize: 2124
Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 15732 0 0 0 96822 95 0 0 25 0 1 0 1855238669 67309568 15376 4294967295 134512640 135094434 3221224432 3221223088 134558029 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28421/statm): 16433 15376 145 145 0 16288 0
[pid=28421] vsize: 65732
Current children cumulated CPU time (s) 969.17
Current children cumulated vsize (Kb) 67856

[startup+980.084 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28421
Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28417/statm): 531 226 485 147 0 384 0
[pid=28417] vsize: 2124
Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 15732 0 0 0 97822 96 0 0 25 0 1 0 1855238669 67309568 15376 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28421/statm): 16433 15376 145 145 0 16288 0
[pid=28421] vsize: 65732
Current children cumulated CPU time (s) 979.18
Current children cumulated vsize (Kb) 67856

[startup+990.085 s]
Raw data (loadavg): 0.99 0.97 0.91 3/57 28421
Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28417/statm): 531 226 485 147 0 384 0
[pid=28417] vsize: 2124
Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 15732 0 0 0 98822 96 0 0 25 0 1 0 1855238669 67309568 15376 4294967295 134512640 135094434 3221224432 3221223120 134554705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28421/statm): 16433 15376 145 145 0 16288 0
[pid=28421] vsize: 65732
Current children cumulated CPU time (s) 989.18
Current children cumulated vsize (Kb) 67856

[startup+1000.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28421
Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28417/statm): 531 226 485 147 0 384 0
[pid=28417] vsize: 2124
Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 15732 0 0 0 99822 96 0 0 25 0 1 0 1855238669 67309568 15376 4294967295 134512640 135094434 3221224432 3221223024 134556862 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28421/statm): 16433 15376 145 145 0 16288 0
[pid=28421] vsize: 65732
Current children cumulated CPU time (s) 999.18
Current children cumulated vsize (Kb) 67856

[startup+1010.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28421
Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28417/statm): 531 226 485 147 0 384 0
[pid=28417] vsize: 2124
Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 15732 0 0 0 100822 96 0 0 25 0 1 0 1855238669 67309568 15376 4294967295 134512640 135094434 3221224432 3221223084 134558255 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28421/statm): 16433 15376 145 145 0 16288 0
[pid=28421] vsize: 65732
Current children cumulated CPU time (s) 1009.18
Current children cumulated vsize (Kb) 67856

[startup+1020.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28421
Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28417/statm): 531 226 485 147 0 384 0
[pid=28417] vsize: 2124
Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 15732 0 0 0 101823 96 0 0 25 0 1 0 1855238669 67309568 15376 4294967295 134512640 135094434 3221224432 3221223072 134558264 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28421/statm): 16433 15376 145 145 0 16288 0
[pid=28421] vsize: 65732
Current children cumulated CPU time (s) 1019.19
Current children cumulated vsize (Kb) 67856

[startup+1030.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28421
Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28417/statm): 531 226 485 147 0 384 0
[pid=28417] vsize: 2124
Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 15732 0 0 0 102823 96 0 0 25 0 1 0 1855238669 67309568 15376 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28421/statm): 16433 15376 145 145 0 16288 0
[pid=28421] vsize: 65732
Current children cumulated CPU time (s) 1029.19
Current children cumulated vsize (Kb) 67856

[startup+1040.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28421
Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28417/statm): 531 226 485 147 0 384 0
[pid=28417] vsize: 2124
Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 15732 0 0 0 103823 96 0 0 25 0 1 0 1855238669 67309568 15376 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28421/statm): 16433 15376 145 145 0 16288 0
[pid=28421] vsize: 65732
Current children cumulated CPU time (s) 1039.19
Current children cumulated vsize (Kb) 67856

[startup+1050.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28421
Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28417/statm): 531 226 485 147 0 384 0
[pid=28417] vsize: 2124
Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 15732 0 0 0 104823 96 0 0 25 0 1 0 1855238669 67309568 15376 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28421/statm): 16433 15376 145 145 0 16288 0
[pid=28421] vsize: 65732
Current children cumulated CPU time (s) 1049.19
Current children cumulated vsize (Kb) 67856

[startup+1060.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28421
Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28417/statm): 531 226 485 147 0 384 0
[pid=28417] vsize: 2124
Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 15732 0 0 0 105823 96 0 0 25 0 1 0 1855238669 67309568 15376 4294967295 134512640 135094434 3221224432 3221223088 134557866 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28421/statm): 16433 15376 145 145 0 16288 0
[pid=28421] vsize: 65732
Current children cumulated CPU time (s) 1059.19
Current children cumulated vsize (Kb) 67856

[startup+1070.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28421
Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28417/statm): 531 226 485 147 0 384 0
[pid=28417] vsize: 2124
Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 15732 0 0 0 106823 96 0 0 25 0 1 0 1855238669 67309568 15376 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28421/statm): 16433 15376 145 145 0 16288 0
[pid=28421] vsize: 65732
Current children cumulated CPU time (s) 1069.19
Current children cumulated vsize (Kb) 67856

[startup+1080.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28421
Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28417/statm): 531 226 485 147 0 384 0
[pid=28417] vsize: 2124
Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 15732 0 0 0 107824 96 0 0 25 0 1 0 1855238669 67309568 15376 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28421/statm): 16433 15376 145 145 0 16288 0
[pid=28421] vsize: 65732
Current children cumulated CPU time (s) 1079.2
Current children cumulated vsize (Kb) 67856

[startup+1090.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28421
Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28417/statm): 531 226 485 147 0 384 0
[pid=28417] vsize: 2124
Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 15734 0 0 0 108824 96 0 0 25 0 1 0 1855238669 67309568 15378 4294967295 134512640 135094434 3221224432 3221221984 134677307 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28421/statm): 16433 15378 145 145 0 16288 0
[pid=28421] 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 28421
Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28417/statm): 531 226 485 147 0 384 0
[pid=28417] vsize: 2124
Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 15734 0 0 0 109824 96 0 0 25 0 1 0 1855238669 67309568 15378 4294967295 134512640 135094434 3221224432 3221222160 134677307 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28421/statm): 16433 15378 145 145 0 16288 0
[pid=28421] vsize: 65732
Current children cumulated CPU time (s) 1099.2
Current children cumulated vsize (Kb) 67856

[startup+1110.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28421
Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28417/statm): 531 226 485 147 0 384 0
[pid=28417] vsize: 2124
Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 15734 0 0 0 110824 97 0 0 25 0 1 0 1855238669 67309568 15378 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28421/statm): 16433 15378 145 145 0 16288 0
[pid=28421] vsize: 65732
Current children cumulated CPU time (s) 1109.21
Current children cumulated vsize (Kb) 67856

[startup+1120.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28421
Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28417/statm): 531 226 485 147 0 384 0
[pid=28417] vsize: 2124
Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 15734 0 0 0 111824 97 0 0 25 0 1 0 1855238669 67309568 15378 4294967295 134512640 135094434 3221224432 3221221876 134677085 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28421/statm): 16433 15378 145 145 0 16288 0
[pid=28421] vsize: 65732
Current children cumulated CPU time (s) 1119.21
Current children cumulated vsize (Kb) 67856

[startup+1130.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28421
Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28417/statm): 531 226 485 147 0 384 0
[pid=28417] vsize: 2124
Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 15734 0 0 0 112824 97 0 0 25 0 1 0 1855238669 67309568 15378 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28421/statm): 16433 15378 145 145 0 16288 0
[pid=28421] vsize: 65732
Current children cumulated CPU time (s) 1129.21
Current children cumulated vsize (Kb) 67856

[startup+1140.1 s]
Raw data (loadavg): 0.99 0.97 0.91 3/57 28421
Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28417/statm): 531 226 485 147 0 384 0
[pid=28417] vsize: 2124
Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 15734 0 0 0 113824 97 0 0 25 0 1 0 1855238669 67309568 15378 4294967295 134512640 135094434 3221224432 3221223088 134558162 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28421/statm): 16433 15378 145 145 0 16288 0
[pid=28421] vsize: 65732
Current children cumulated CPU time (s) 1139.21
Current children cumulated vsize (Kb) 67856

[startup+1150.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28421
Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28417/statm): 531 226 485 147 0 384 0
[pid=28417] vsize: 2124
Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 15734 0 0 0 114825 97 0 0 25 0 1 0 1855238669 67309568 15378 4294967295 134512640 135094434 3221224432 3221223088 134557846 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28421/statm): 16433 15378 145 145 0 16288 0
[pid=28421] vsize: 65732
Current children cumulated CPU time (s) 1149.22
Current children cumulated vsize (Kb) 67856

[startup+1160.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28421
Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28417/statm): 531 226 485 147 0 384 0
[pid=28417] vsize: 2124
Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 15735 0 0 0 115825 97 0 0 25 0 1 0 1855238669 67309568 15379 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28421/statm): 16433 15379 145 145 0 16288 0
[pid=28421] vsize: 65732
Current children cumulated CPU time (s) 1159.22
Current children cumulated vsize (Kb) 67856

[startup+1170.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28421
Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28417/statm): 531 226 485 147 0 384 0
[pid=28417] vsize: 2124
Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 15735 0 0 0 116825 97 0 0 25 0 1 0 1855238669 67309568 15379 4294967295 134512640 135094434 3221224432 3221223024 134557366 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28421/statm): 16433 15379 145 145 0 16288 0
[pid=28421] vsize: 65732
Current children cumulated CPU time (s) 1169.22
Current children cumulated vsize (Kb) 67856

[startup+1180.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28421
Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28417/statm): 531 226 485 147 0 384 0
[pid=28417] vsize: 2124
Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 15735 0 0 0 117825 97 0 0 25 0 1 0 1855238669 67309568 15379 4294967295 134512640 135094434 3221224432 3221223056 134562125 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28421/statm): 16433 15379 145 145 0 16288 0
[pid=28421] vsize: 65732
Current children cumulated CPU time (s) 1179.22
Current children cumulated vsize (Kb) 67856

[startup+1190.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28421
Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28417/statm): 531 226 485 147 0 384 0
[pid=28417] vsize: 2124
Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 15735 0 0 0 118825 97 0 0 25 0 1 0 1855238669 67309568 15379 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28421/statm): 16433 15379 145 145 0 16288 0
[pid=28421] vsize: 65732
Current children cumulated CPU time (s) 1189.22
Current children cumulated vsize (Kb) 67856

[startup+1200.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28421
Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28417/statm): 531 226 485 147 0 384 0
[pid=28417] vsize: 2124
Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 15735 0 0 0 119825 97 0 0 25 0 1 0 1855238669 67309568 15379 4294967295 134512640 135094434 3221224432 3221223024 134556993 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28421/statm): 16433 15379 145 145 0 16288 0
[pid=28421] 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 28421
Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28417/statm): 531 226 485 147 0 384 0
[pid=28417] vsize: 2124
Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 15735 0 0 0 120826 97 0 0 25 0 1 0 1855238669 67309568 15379 4294967295 134512640 135094434 3221224432 3221223088 134558178 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28421/statm): 16433 15379 145 145 0 16288 0
[pid=28421] vsize: 65732
Current children cumulated CPU time (s) 1209.23
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 28421
Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28417/statm): 531 226 485 147 0 384 0
[pid=28417] vsize: 2124
Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 15735 0 0 0 120826 97 0 0 25 0 1 0 1855238669 67309568 15379 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28421/statm): 16433 15379 145 145 0 16288 0
[pid=28421] vsize: 65732
Current children cumulated CPU time (s) 1209.23
Current children cumulated vsize (Kb) 67856

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

Child status: 10
Real time (s): 1210.14
CPU time (s): 1209.27
CPU user time (s): 1208.26
CPU system time (s): 1.00585
CPU usage (%): 99.928
Max. virtual memory (cumulated for all children) (Kb): 67856

Verifier Data

ERROR: no interpretation found !